logUp grouping

Cargo.toml

@@ -52,7 +52,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 = "fd03d7957fa10ff607cb027639bbb0c18bcb8745" }
+multi-stark = { git = "https://github.com/argumentcomputer/multi-stark.git", rev = "c72d32130eb084327b73849e39c92734a8829011" }
 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.lean

@@ -56,14 +56,14 @@ def entrypoints := ⟦
     let (idx, len) = io_get_info(0, [0]);
     let (proof, stop) = read_proof(idx);
     assert_eq!(stop, idx + len);
-    -- Verifying key (`System<AiurCircuit>`) from IO channel 1: bind the bytes
-    -- to the public Blake3 `system_digest` (hashed straight from the IO arena
-    -- — no byte list), then reconstruct the system via indexed reads and
-    -- assert full consumption.
+    -- Verifying key (`System<AiurCircuit>`) from IO channel 1: fetch the raw
+    -- bytes once as advice, then constrain both the hash and deserialization
+    -- against that exact byte stream (the same binding pattern as IxVM).
     let (sidx, slen) = io_get_info(1, [0]);
-    assert_eq!(b3_to_digest(b3_io(1, sidx, slen)), system_digest);
-    let (sys, send) = read_system(sidx);
-    assert_eq!(send, sidx + slen);
+    let sbytes = #read_byte_stream(1, sidx, slen);
+    assert_eq!(b3_to_digest(blake3(sbytes)), system_digest);
+    let (sys, srest) = read_system(sbytes);
+    assert_eq!(load(srest), ListNode.Nil);
     -- Public claims (`&[&[Val]]`) from IO channel 2: bind the bytes to the
     -- public Blake3 `claims_digest`, then deserialize. Binding them as a
     -- public input is what makes the lookup argument sound (a prover cannot

Ix/MultiStark/Pcs.lean

@@ -166,7 +166,9 @@ def pcs := ⟦
   -- directly to `blake3_compress` — no byte list is materialized, walked,
   -- accumulated, or re-loaded. Same flag schedule as the byte driver; the
   -- (cold, once-per-hash) ≤63-byte tail reuses `pad_block`/`bytes_to_block`.
-  -- Used for digest-binding large advice streams (the verifying key).
+  -- Kept as a differential-tested indexed IO hashing helper. Digest-bound
+  -- inputs must not hash and deserialize through separate `io_read` calls;
+  -- the production verifying-key path materializes one shared `ByteStream`.
   -- ==========================================================================
 
   -- Reverse-ordered tail accumulator (head = last byte), the shape