logUp grouping

Cargo.toml

@@ -51,7 +51,7 @@ libc = "0.2"
 log = "0.4"
 memmap2 = "0.9"
 mimalloc = { version = "0.1", default-features = false }
-multi-stark = { git = "https://github.com/argumentcomputer/multi-stark.git", rev = "be1755e216691a2a7856c818ee83f5488cd2d90f" }
+multi-stark = { git = "https://github.com/argumentcomputer/multi-stark.git", rev = "e2c13449e63410bcfee95d7bfc83df2866f6bfbc" }
 nom = "7.1.3"
 num-bigint = "0.4.6"
 quickcheck = "1.0.3"

Ix/Aiur/Stages/Bytecode.lean

@@ -98,9 +98,15 @@ def FunctionLayout.width (l : FunctionLayout) : Nat :=
   l.inputSize + l.selectors + l.auxiliaries
 
 def FunctionLayout.totalWidth (l : FunctionLayout) : Nat :=
-  -- Stage 2 commits max(L, 1) chained partial accumulators (no message
-  -- inverses); see `multi_stark::lookup::stage2_width`.
-  l.width + G.extensionDegree * (max l.lookups 1)
+  -- Stage 2 commits max(⌈L/k⌉, 1) chained partial accumulators (no message
+  -- inverses); see `multi_stark::lookup::stage2_width`. Mirrors the
+  -- synthesis grouping rule (`crates/aiur/src/synthesis.rs`): branchless
+  -- functions (one selector) have raw degree-1 lookup arguments, so their
+  -- lookups are grouped 2 per accumulator step.
+  let slots := if l.selectors == 1 && l.lookups >= 2
+    then (l.lookups + 1) / 2
+    else max l.lookups 1
+  l.width + G.extensionDegree * slots
 
 structure Function where
   body : Block

Ix/MultiStark/SystemDeserialize.lean

@@ -20,7 +20,9 @@ flat base-field node graph, so this reader parses that compiled form:
   constraint_count, stage_2_width, num_publics, and lookup_prefix_len are
   all recomputed from the counts below):
     - u16 main_width, u16 preprocessed_width, u32 preprocessed_height,
-      u16 max_constraint_degree (combined user + logUp), u16 node_count
+      u16 max_constraint_degree (combined user + logUp),
+      u8 lookup_group_size (k: lookups per chained accumulator step),
+      u16 node_count
     - `node_count` tagged nodes (dense v5: u16 children, never sub-trees):
       0 ConstSmall(u16) · 1 ConstBig(u64) · 2 Public(u8) ·
       3 IsFirstRow · 4 IsLastRow · 5 IsTransition ·
@@ -42,10 +44,10 @@ over the whole arena, bound to the public `system_digest`) is what makes
 the bytes meaningful. Per-node degrees are neither serialized nor needed
 (the node sweep just evaluates the graph).
 
-The Fiat-Shamir shape limbs are unchanged from v2: `observe_shape` still
-feeds the challenger the circuit count then, per circuit, the six words
-constraint_count, max_constraint_degree, preprocessed_height,
-preprocessed_width, main_width, stage_2_width (as 8-byte LE limbs).
+The Fiat-Shamir shape limbs (`observe_shape`): the circuit count then,
+per circuit, the seven words constraint_count, max_constraint_degree,
+preprocessed_height, preprocessed_width, main_width, stage_2_width,
+lookup_group_size (as 8-byte LE limbs).
 -/
 
 public section
@@ -81,7 +83,7 @@ def systemDeserialize := ⟦
   -- A compiled lookup: multiplicity node id + argument node ids (all into
   -- the graph's lookup prefix). Drives the direct logUp evaluation.
   enum SysLookup { Mk(G, List‹G›) }
-  enum SysCircuit { Mk(List‹SysNode›, G, List‹G›, G, List‹SysLookup›) }   -- nodes, node_count, zeros, max_constraint_degree, lookups
+  enum SysCircuit { Mk(List‹SysNode›, G, List‹G›, G, List‹SysLookup›, G) }   -- nodes, node_count, zeros, max_constraint_degree, lookups, lookup_group_size
 
   -- log_blowup, cap_height, log_final_poly_len, max_log_arity, num_queries,
   -- commit_proof_of_work_bits, query_proof_of_work_bits — the commitment + FRI
@@ -255,52 +257,68 @@ def systemDeserialize := ⟦
     }
   }
 
+  -- ⌈n/k⌉ by walking the lookups with a within-group countdown (`rem`,
+  -- 0 = a new group starts on the next lookup). No in-circuit division.
+  fn lookup_groups_count(n: G, rem: G, k: G) -> G {
+    match n {
+      0 => 0,
+      _ => match rem {
+        0 => 1 + lookup_groups_count(n - 1, k - 1, k),
+        _ => lookup_groups_count(n - 1, rem - 1, k),
+      },
+    }
+  }
+
   -- One circuit record: a u32 length prefix then the contiguous record. The
   -- 8-word header, the node stream, the zeros, and the compiled lookups
   -- (which drive the direct logUp evaluation) are all parsed. Besides the
-  -- parsed circuit, returns its 6 shape words as u64 limbs, in
-  -- `observe_shape` order: constraint_count (user roots + (L+3)·D, read
+  -- parsed circuit, returns its 7 shape words as u64 limbs, in
+  -- `observe_shape` order: constraint_count (user roots + ⌈L/k⌉·D, read
   -- from the header), max_constraint_degree (combined),
-  -- preprocessed_height, preprocessed_width, main_width, stage_2_width.
-  fn read_sys_circuit(base: G) -> (SysCircuit, [U64; 6], G) {
+  -- preprocessed_height, preprocessed_width, main_width, stage_2_width,
+  -- lookup_group_size.
+  fn read_sys_circuit(base: G) -> (SysCircuit, [U64; 7], G) {
     let (mw, mwl, c1) = #read_vk_u16_limb(base);
     let (pw, pwl, c2) = #read_vk_u16_limb(c1);
     let (ph, phl, c3) = #read_vk_u32_limb(c2);
     let (md, mdl, c4) = #read_vk_u16_limb(c3);
-    let (ncount, c5) = #read_vk_u16(c4);
+    let (k, c4b) = #read_vk_tag(c4);
+    let (ncount, c5) = #read_vk_u16(c4b);
     let (nodes, c6) = read_nodes_n(c5, ncount);
     let (zcount, c7) = #read_vk_u16(c6);
     let (zeros, c8) = read_node_ids_n(c7, zcount);
     let (lcount, c9) = #read_vk_u16(c8);
     let (lks, c10) = read_sys_lookups_n(c9, lcount);
     -- Derived shape values (not serialized): constraint_count = user roots
-    -- + (L+3)·D and stage_2_width = (1+L)·D, their observation limbs built
-    -- by byte decomposition (both values are far below 2^32, so the
-    -- canonical decomposition IS the little-endian u64 limb).
-    -- Chained logUp: max(L, 1) accumulator slots, one constraint per slot.
-    let lslots = match lcount {
+    -- + ⌈L/k⌉·D and stage_2_width = max(⌈L/k⌉, 1)·D, their observation
+    -- limbs built by byte decomposition (both values are far below 2^32, so
+    -- the canonical decomposition IS the little-endian u64 limb).
+    -- Grouped chained logUp: one accumulator slot and one constraint per
+    -- lookup GROUP (`k` consecutive lookups; the last group may be smaller).
+    let gslots = match lcount {
       0 => 1,
-      _ => lcount,
+      _ => lookup_groups_count(lcount, 0, k),
     };
-    let ccl = gl_to_bytes(zcount + lslots + lslots);
-    let s2wl = gl_to_bytes(lslots + lslots);
-    (SysCircuit.Mk(nodes, ncount, zeros, md, lks),
-     [ccl, mdl, phl, pwl, mwl, s2wl], c10)
+    let ccl = gl_to_bytes(zcount + gslots + gslots);
+    let s2wl = gl_to_bytes(gslots + gslots);
+    let kl = gl_to_bytes(k);
+    (SysCircuit.Mk(nodes, ncount, zeros, md, lks, k),
+     [ccl, mdl, phl, pwl, mwl, s2wl, kl], c10)
   }
-  fn cons_shape6(l: [U64; 6], tail: List‹U64›) -> List‹U64› {
+  fn cons_shape7(l: [U64; 7], tail: List‹U64›) -> List‹U64› {
     store(ListNode.Cons(l[0], store(ListNode.Cons(l[1], store(ListNode.Cons(l[2],
     store(ListNode.Cons(l[3], store(ListNode.Cons(l[4], store(ListNode.Cons(l[5],
-    tail))))))))))))
+    store(ListNode.Cons(l[6], tail))))))))))))))
   }
   -- Returns the circuits plus their shape limbs (`observe_shape` order: each
-  -- circuit's 6 metadata words; the count limb is consed by `read_system`).
+  -- circuit's 7 metadata words; the count limb is consed by `read_system`).
   fn read_sys_circuits_n(i: G, n: G) -> (List‹SysCircuit›, List‹U64›, G) {
     match n {
       0 => (store(ListNode.Nil), store(ListNode.Nil), i),
       _ =>
         let (x, xl, j) = read_sys_circuit(i);
         let (rest, lrest, j2) = read_sys_circuits_n(j, n - 1);
-        (store(ListNode.Cons(x, rest)), cons_shape6(xl, lrest), j2),
+        (store(ListNode.Cons(x, rest)), cons_shape7(xl, lrest), j2),
     }
   }
 

Ix/MultiStark/Verifier.lean

@@ -623,9 +623,8 @@ def verifier := ⟦
   -- machinery, never compiled into the vk's node graph: their values at ζ
   -- are computed here from the lookup ids (evaluated through the memoized
   -- `eval_at`), the stage-2 openings, and the lookup publics, and folded
-  -- with α after the user roots — per lookup the 2 coordinates of
-  -- `(β + fingerprint(γ, args))·inv − 1`, then the first-row, transition,
-  -- and last-row accumulator constraints (2 coordinates each).
+  -- with α after the user roots — per lookup GROUP the 2 coordinates of
+  -- the chained-accumulator step constraint (see `logup_steps_fold`).
   --
   -- Coordinates: a coordinate-expanded logUp constraint is a PAIR of
   -- base-field polynomials; at ζ each coordinate is an Ext value. Pair
@@ -655,20 +654,21 @@ def verifier := ⟦
     }
   }
 
-  -- Per-lookup message constraints, folding into the α accumulator as we
-  -- go and accumulating `acc_expr = acc_col + Σⱼ multⱼ·invⱼ` (as a
-  -- coordinate pair) for the accumulator constraints. `j` is the lookup
-  -- slot (inverse columns at stage-2 slots 1+j).
-  -- One chained-accumulator step per lookup (Rust
-  -- `lookup::logup_constraint_values`): stage-2 slot `j` holds `acc_j`, the
-  -- running sum entering lookup `j`'s step. Interior steps assert
-  -- `m_j·(acc_{j+1} − acc_j) − mult_j = 0`; the wrap step (j = L−1) targets
-  -- the NEXT row's slot 0 plus the boundary injection
-  -- `is_last_row·(acc_final − acc_initial)` (`inj`), which converts the
-  -- cyclic telescoped sum into the public accumulator difference.
-  -- `is_last_row` is normalized (`trace_selectors`), so no row-position
-  -- constraints exist besides the injection.
+  -- Per-GROUP chained-accumulator constraints, folding into the α
+  -- accumulator as we go (Rust `lookup::logup_constraint_values`): stage-2
+  -- slot `g` holds `acc_g`, the running sum entering group `g`'s step. A
+  -- group of `k` consecutive lookups (the last group may be smaller)
+  -- asserts `(Π_j m_j)·(acc_{g+1} − acc_g) − Σ_j mult_j·Π_{j'≠j} m_{j'}`;
+  -- the wrap step (last group) targets the NEXT row's slot 0 plus the
+  -- boundary injection `is_last_row·(acc_final − acc_initial)` (`inj`),
+  -- which converts the cyclic telescoped sum into the public accumulator
+  -- difference. Group state is built in one pass with the recurrence
+  -- `R ← R·m + mult·P; P ← P·m` (P the message product, R the mult sum);
+  -- `rem` counts the group's remaining capacity, `j` the lookup index.
+  -- Ungrouped (k = 1) closes every step: P = m, R = (mult, 0), exactly the
+  -- per-lookup chained constraint.
   fn logup_steps_fold(acc: Ext, alpha: Ext, lks: List‹SysLookup›, j: G, lcount: G,
+      g: G, rem: G, k: G, p0: Ext, p1: Ext, r0: Ext, r1: Ext,
       inj0: Ext, inj1: Ext, b0: Ext, b1: Ext, g0: Ext, g1: Ext,
       nodes: List‹SysNode›,
       main: List‹Ext›, main_next: List‹Ext›, prep: List‹Ext›, prep_next: List‹Ext›,
@@ -678,23 +678,49 @@ def verifier := ⟦
       ListNode.Nil => acc,
       ListNode.Cons(lk, rest) =>
         let SysLookup.Mk(mid, args) = lk;
-        let s0 = list_lookup(s2, j + j);
-        let s1 = list_lookup(s2, j + j + 1);
-        let (t0, t1) = match (j + 1 - lcount) {
-          0 => (eg_add(list_lookup(s2next, 0), inj0),
-                eg_add(list_lookup(s2next, 1), inj1)),
-          _ => (list_lookup(s2, j + j + 2), list_lookup(s2, j + j + 3)),
-        };
         let (f0, f1) = logup_fingerprint(args, g0, g1, nodes,
           main, main_next, prep, prep_next, s2, s2next, publics, isf, isl, ist);
-        let (c0, c1) = pair_mul(eg_add(f0, b0), eg_add(f1, b1),
-                                eg_sub(t0, s0), eg_sub(t1, s1));
+        let m0 = eg_add(f0, b0);
+        let m1 = eg_add(f1, b1);
         let mv = eval_at(nodes, mid, main, main_next, prep, prep_next, s2, s2next,
                          publics, isf, isl, ist);
-        let acc1 = ood_fold(ood_fold(acc, alpha, eg_sub(c0, mv)), alpha, c1);
-        logup_steps_fold(acc1, alpha, rest, j + 1, lcount, inj0, inj1,
-          b0, b1, g0, g1, nodes,
-          main, main_next, prep, prep_next, s2, s2next, publics, isf, isl, ist),
+        -- R ← R·m + mult·P, then P ← P·m.
+        let (rm0, rm1) = pair_mul(r0, r1, m0, m1);
+        let nr0 = eg_add(rm0, eg_mul(mv, p0));
+        let nr1 = eg_add(rm1, eg_mul(mv, p1));
+        let (np0, np1) = pair_mul(p0, p1, m0, m1);
+        match (j + 1 - lcount) {
+          0 =>
+            -- Final lookup: close the (possibly smaller) last group against
+            -- the wrap target.
+            let s0 = list_lookup(s2, g + g);
+            let s1 = list_lookup(s2, g + g + 1);
+            let t0 = eg_add(list_lookup(s2next, 0), inj0);
+            let t1 = eg_add(list_lookup(s2next, 1), inj1);
+            let (c0, c1) = pair_mul(np0, np1, eg_sub(t0, s0), eg_sub(t1, s1));
+            ood_fold(ood_fold(acc, alpha, eg_sub(c0, nr0)), alpha, eg_sub(c1, nr1)),
+          _ => match rem - 1 {
+            0 =>
+              -- Group full: close against the next slot, reset the state.
+              let s0 = list_lookup(s2, g + g);
+              let s1 = list_lookup(s2, g + g + 1);
+              let t0 = list_lookup(s2, g + g + 2);
+              let t1 = list_lookup(s2, g + g + 3);
+              let (c0, c1) = pair_mul(np0, np1, eg_sub(t0, s0), eg_sub(t1, s1));
+              let acc1 = ood_fold(ood_fold(acc, alpha, eg_sub(c0, nr0)), alpha,
+                                  eg_sub(c1, nr1));
+              logup_steps_fold(acc1, alpha, rest, j + 1, lcount,
+                g + 1, k, k, [1, 0], [0, 0], [0, 0], [0, 0],
+                inj0, inj1, b0, b1, g0, g1, nodes,
+                main, main_next, prep, prep_next, s2, s2next, publics, isf, isl, ist),
+            _ =>
+              -- Keep accumulating within the group.
+              logup_steps_fold(acc, alpha, rest, j + 1, lcount,
+                g, rem - 1, k, np0, np1, nr0, nr1,
+                inj0, inj1, b0, b1, g0, g1, nodes,
+                main, main_next, prep, prep_next, s2, s2next, publics, isf, isl, ist),
+          },
+        },
     }
   }
 
@@ -703,6 +729,7 @@ def verifier := ⟦
   -- directly-evaluated chained-logUp step values, all Horner-folded with α
   -- in the canonical protocol order.
   fn ood_composition(nodes: List‹SysNode›, zeros: List‹G›, lks: List‹SysLookup›,
+      k: G,
       main: List‹Ext›, main_next: List‹Ext›, prep: List‹Ext›, prep_next: List‹Ext›,
       s2: List‹Ext›, s2next: List‹Ext›, publics: List‹Ext›,
       isf: Ext, isl: Ext, ist: Ext, alpha: Ext, inorm: G) -> Ext {
@@ -727,7 +754,8 @@ def verifier := ⟦
         ood_fold(acc, alpha,
           eg_add(eg_sub(list_lookup(s2next, 1), list_lookup(s2, 1)), inj1)),
       ListNode.Cons(_h, _t) =>
-        logup_steps_fold(base, alpha, lks, 0, list_length(lks), inj0, inj1,
+        logup_steps_fold(base, alpha, lks, 0, list_length(lks),
+          0, k, k, [1, 0], [0, 0], [0, 0], [0, 0], inj0, inj1,
           b0, b1, g0, g1, nodes,
           main, main_next, prep, prep_next, s2, s2next, publics, isf, isl, ist),
     }
@@ -807,7 +835,7 @@ def verifier := ⟦
     match load(circuits) {
       ListNode.Nil => 1,
       ListNode.Cons(circ, rest) =>
-        let SysCircuit.Mk(nodes, _node_count, zeros, md, lks) = circ;
+        let SysCircuit.Mk(nodes, _node_count, zeros, md, lks, k) = circ;
         let l = to_field(list_lookup(log_degrees, i));
         let qd = quotient_degree_of(md);
         let naccp = list_lookup(accs, i);
@@ -822,7 +850,7 @@ def verifier := ⟦
         let (isf, isl, ist, invv) = trace_selectors(zeta, l);
         let publics = build_publics(lch, fch, accp, naccp);
         let inorm = gl_inverse(pow2(l) * two_adic_gen(l));
-        let comp = ood_composition(nodes, zeros, lks,
+        let comp = ood_composition(nodes, zeros, lks, k,
                                    main, main_next, prep, prep_next, s2row, s2next,
                                    publics, isf, isl, ist, alpha, inorm);
         -- circuit i's wide quotient row, its base-coordinate pairs folded back