Send sumcheck round polynomials whole to the consumers, minimal on the wire

Every sumcheck round polynomial has one evaluation the running claim already
fixes: h(0) + h(1) = claim, or (1 + r)·h(0) + r·h(1) = claim where the round's
eq weight was factored out. Three of the four sumchecks exploited that, each
hand-rolling it in its own notation and its own basis; the table sumcheck in
constraints.rs did not, and sent a value it then checked was redundant.

Name it once. Transmitter::add_round_poly takes the whole polynomial as
evaluations, h(0) first, and drops h(0) from the wire; Receiver::next_round_poly
reads the rest, recovers h(0), and binds all of it. Every site now speaks the
one convention, so the wire is minimal everywhere, including the 18 rounds of
the table sumcheck that were not.

The sponge binds every evaluation, so RawProof carries every evaluation, and
the two consumers that read RawProof become plain textbook sumcheck: read the
round polynomial, check it answers the claim, evaluate at the challenge. No
reconstruction, no eq-split algebra, no basis conversion. That deletes an
in-circuit field inversion per zerocheck round from the guest and the
ONE_PLUS_CHALLENGE_INV table that fed it.

Paying for that means the provers now track their running claim, since they
have to bind an h(0) the verifier will recompute. whir mirrors the verifier's
(claim, quad) pair, which it had a field for but never maintained; lincheck
takes one O(k) inner product for round 0; zerocheck reuses the interpolation it
already computes.

The recursion harness no longer touches the wire proof at all. It reads the
verifier's raw stream, so gen_verify lost its Proof parameter and run_recursion
stopped carrying one.

Measured on the pinning test: 1206 wire scalars against 1278 raw, the 72-scalar
gap being exactly one per sumcheck round. Guest cycles 727,970 -> 728,287
(+0.04%): three more stream reads per round against one fewer inversion.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Author: TomWambsgans

crates/fiat_shamir/src/transcript.rs

@@ -49,18 +49,19 @@ pub struct Proof {
 }
 
 /// The proof the recursion guest and the Python verifier consume: nothing
-/// shared, nothing pruned.
+/// shared, nothing pruned, nothing to reconstruct.
 ///
-/// Same protocol, redundant encoding. Each query carries its own full Merkle
-/// path instead of an octopus over the batch, so a consumer walks one path per
-/// query with no dedup bookkeeping, which is the difference between a page of
-/// index arithmetic and a loop in the zkDSL. [`Proof`] is what goes over the
-/// wire; a verifier run produces this as a by-product
-/// ([`VerifierState::into_raw_proof`]), so the expansion is written once.
+/// Same protocol, redundant encoding. [`Proof`] is minimal because it drops
+/// every value a verifier can recompute; this is the same proof with all of
+/// them written out, which is what lets a consumer be one read-and-absorb loop.
+/// A verifier run produces it as a by-product
+/// ([`VerifierState::into_raw_proof`]), so each expansion is written once, in
+/// Rust, instead of three times in three languages.
 #[derive(Clone, Debug, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
 pub struct RawProof {
-    /// Identical to [`Proof::stream`]: no scalar is omitted from the wire form
-    /// today. Carried here anyway so a consumer needs this struct alone.
+    /// Every scalar a verifier reads AND binds, in binding order. Longer than
+    /// [`Proof::stream`] by one evaluation per sumcheck round, the `h(0)` the
+    /// wire omits.
     pub stream: Vec<F192>,
     /// One opening per query, phases concatenated in the order they ran.
     pub merkle_openings: Vec<MerkleOpening>,
@@ -118,6 +119,18 @@ pub trait Transmitter: Challenger {
     fn add_root(&mut self, root: &Hash) {
         self.add_scalars(&hash_to_scalars(root));
     }
+
+    /// Send one sumcheck round polynomial, as its evaluations with `h(0)` FIRST.
+    ///
+    /// `h(0)` does not ride the wire: the running claim already fixes it (see
+    /// [`Receiver::next_round_poly`]), and a minimal proof never repeats a value
+    /// the verifier can recompute. It IS bound, along with every other
+    /// evaluation, in this order.
+    fn add_round_poly(&mut self, evals: &[F192]) {
+        assert!(evals.len() >= 2, "a round polynomial has at least h(0) and h(1)");
+        self.observe_scalar(evals[0]);
+        self.add_scalars(&evals[1..]);
+    }
 }
 
 /// The verifier half, mirroring [`Transmitter`] call for call.
@@ -141,6 +154,15 @@ pub trait Receiver: Challenger {
     fn next_root(&mut self) -> Result<Hash, Error> {
         scalars_to_hash(&[self.next_scalar()?, self.next_scalar()?])
     }
+
+    /// Mirror of [`Transmitter::add_round_poly`]: read the `n_evals - 1`
+    /// transmitted evaluations, recover `h(0)`, and bind the whole polynomial.
+    ///
+    /// The running `claim` is what fixes `h(0)`. A plain round splits it as
+    /// `h(0) + h(1) = claim` (char 2), so `h(0) = claim + h(1)`. A round whose
+    /// `eq` weight `r` the caller factored out of `h` splits it as
+    /// `(1 + r)·h(0) + r·h(1) = claim` instead.
+    fn next_round_poly(&mut self, n_evals: usize, claim: F192, eq: Option<F192>) -> Result<Vec<F192>, Error>;
     fn grind_check(&mut self, bits: u32) -> Result<(), Error>;
 }
 
@@ -177,6 +199,7 @@ pub struct VerifierState<'a> {
     offset: usize,
     merkle_paths: &'a [MerklePaths],
     phase: usize,
+    raw_stream: Vec<F192>,
     raw_openings: Vec<MerkleOpening>,
 }
 
@@ -190,32 +213,44 @@ impl<'a> VerifierState<'a> {
             offset: 0,
             merkle_paths: &proof.merkle_paths,
             phase: 0,
+            raw_stream: Vec::new(),
             raw_openings: Vec::new(),
         }
     }
 
-    /// Advance the stream cursor by one **without** binding into the sponge: the
-    /// read counterpart of the raw nonce push in [`ProverState::grind`].
+    /// Advance the wire cursor by one **without** binding or recording: the read
+    /// counterpart of the raw nonce push in [`ProverState::grind`], and the
+    /// first half of reading a round polynomial (whose evaluations bind only
+    /// once `h(0)` is known).
     fn take_raw(&mut self) -> Result<F192, Error> {
         let x = *self.stream.get(self.offset).ok_or(Error::ExceededStream)?;
         self.offset += 1;
         Ok(x)
     }
 
+    /// Bind a scalar read off the wire, and record it: [`RawProof::stream`] IS
+    /// the sequence of these, in this order.
+    #[inline]
+    fn bind(&mut self, x: F192) {
+        self.sponge.observe(x);
+        self.raw_stream.push(x);
+    }
+
     /// The redundant form of the proof just verified: every scalar it read, plus
     /// one unpruned opening per query in phase order. Meaningful only after a
     /// verification that accepted, since a rejected one stops part way.
     pub fn into_raw_proof(self) -> RawProof {
         RawProof {
-            stream: self.stream.to_vec(),
+            stream: self.raw_stream,
             merkle_openings: self.raw_openings,
         }
     }
 
-    /// How many stream words have been read so far: the cursor a caller needs
-    /// to locate a sub-protocol's scalars without counting back from the tail.
+    /// How many scalars have been read and bound so far: the cursor into
+    /// [`RawProof::stream`] a caller needs to locate a sub-protocol's scalars
+    /// without counting back from the tail.
     pub fn stream_offset(&self) -> usize {
-        self.offset
+        self.raw_stream.len()
     }
 
     /// Assert the whole proof was consumed (no trailing/extra data).
@@ -289,17 +324,43 @@ impl<'a> Receiver for VerifierState<'a> {
     /// Read the next scalar, binding it into the sponge (mirrors `add_scalar`).
     #[inline]
     fn next_scalar(&mut self) -> Result<F192, Error> {
-        let x = *self.stream.get(self.offset).ok_or(Error::ExceededStream)?;
-        self.offset += 1;
-        self.sponge.observe(x);
+        let x = self.take_raw()?;
+        self.bind(x);
         Ok(x)
     }
 
+    fn next_round_poly(&mut self, n_evals: usize, claim: F192, eq: Option<F192>) -> Result<Vec<F192>, Error> {
+        assert!(n_evals >= 2, "a round polynomial has at least h(0) and h(1)");
+        let mut evals = vec![F192::ZERO; n_evals];
+        for e in &mut evals[1..] {
+            *e = self.take_raw()?;
+        }
+        evals[0] = match eq {
+            None => claim + evals[1],
+            // `(1 + r)·h(0) + r·h(1) = claim`. At `r = 1` that leaves h(0) free,
+            // so it is not a usable weight; every caller's `r` is a challenge.
+            Some(r) => {
+                let one_plus_r = F192::ONE + r;
+                if one_plus_r.is_zero() {
+                    return Err(Error::NonCanonicalEncoding);
+                }
+                (claim + r * evals[1]) * one_plus_r.inv()
+            }
+        };
+        for &e in &evals {
+            self.bind(e);
+        }
+        Ok(evals)
+    }
+
     /// Verifier mirror of [`Transmitter::grind`]: read the transmitted nonce and
     /// check it clears the `bits` proof-of-work, then bind it (so the sponge
     /// stays in lockstep). Rejects a proof that skipped or under-did the grind.
     fn grind_check(&mut self, bits: u32) -> Result<(), Error> {
         let nonce = self.take_raw()?;
+        // Bound by the PoW absorb inside `verify_pow_field` rather than by
+        // `observe`, but still a scalar the consumer reads at this position.
+        self.raw_stream.push(nonce);
         if self.sponge.verify_pow_field(nonce, bits) {
             Ok(())
         } else {

crates/flock/src/lincheck.rs

@@ -1226,10 +1226,16 @@ pub fn prove_padded_capture_s_hat_v(
         // round's message falls out of binding the previous round (fold +
         // next-eval fused into one pass, see `sumcheck_bind_both_and_eval_next`).
         let (mut e1, mut einf) = sumcheck_round_eval_par(&comb_vec, &z_vec);
+        // The running claim, mirrored from the verifier: `q(0) + q(1) = claim`
+        // is what lets the wire drop `q(0)`, so the prover has to know it too.
+        // Round 0's claim is the whole inner product, one O(k) pass over the
+        // column vectors and negligible beside the sumcheck itself.
+        let mut running = inner_product_ext(&comb_vec, &z_vec);
         for t in 0..inner_rest_len {
-            ps.add_scalar(e1);
-            ps.add_scalar(einf);
+            let e0 = running + e1;
+            ps.add_round_poly(&[e0, e1, einf]);
             let r = ps.sample();
+            running = (einf * r + (e0 + e1 + einf)) * r + e0;
             r_rounds.push(r);
             if t + 1 < inner_rest_len {
                 // Fused: bind both tables at r AND compute round (t+1)'s message.
@@ -1351,11 +1357,11 @@ pub fn verify(
     let mut running = target;
     let mut r_rounds = Vec::with_capacity(inner_rest_len);
     for _ in 0..inner_rest_len {
-        let e1 = vs.next_scalar().map_err(VerifyError::Transcript)?;
-        let einf = vs.next_scalar().map_err(VerifyError::Transcript)?;
+        // `q(0) + q(1) = claim` in char 2, so `q(0)` never rides the wire.
+        let q = vs.next_round_poly(3, running, None).map_err(VerifyError::Transcript)?;
+        let (e0, e1, einf) = (q[0], q[1], q[2]);
         let r = vs.sample();
-        // q(0) = claim + q(1) in char 2; q(X) = einf·X² + c1·X + e0.
-        let e0 = running + e1;
+        // q(X) = einf·X² + c1·X + e0.
         let c1 = e0 + e1 + einf;
         running = (einf * r + c1) * r + e0;
         r_rounds.push(r);

crates/flock/src/zerocheck.rs

@@ -119,6 +119,18 @@ pub enum VerifyError {
 // API: prove / verify.
 // ---------------------------------------------------------------------------
 
+/// Send one multilinear round and advance the running claim, the prover mirror
+/// of the verifier's loop. `G(0)` never rides the wire: the eq split
+/// `(1 + r_eq)·G(0) + r_eq·G(1) = claim` fixes it. All three evaluations bind.
+fn send_round(ps: &mut impl Transmitter, claim: F192, r_eq: F192, g1: F192, g_inf: F192, rhos: &mut Vec<F192>) -> F192 {
+    let g0 = (claim + r_eq * g1) * (F192::ONE + r_eq).inv();
+    ps.add_round_poly(&[g0, g1, g_inf]);
+    let rho = ps.sample();
+    rhos.push(rho);
+    // G(X) = G(0)·(1+X) + G(1)·X + G(inf)·X·(1+X).
+    g0 + rho * (g0 + g1 + (F192::ONE + rho) * g_inf)
+}
+
 /// THE zerocheck prover entry: proves `a·b ⊕ c = 0` over the padded cube and
 /// ALSO returns the canonical `s_hat_v_c` produced by the fused two-bank
 /// round-1 kernel
@@ -221,10 +233,15 @@ pub fn prove_packed_padded_capture_s_hat_v_c(
         );
     }
     let t_tail = std::time::Instant::now();
-    ps.add_scalar(msg_1);
-    ps.add_scalar(msg_inf);
+    // The running claim, mirrored from the verifier exactly (same interpolation
+    // of the same round-1 values at the same z). `(1+r)·G(0) + r·G(1) = claim`
+    // is what lets the wire drop `G(0)`, so the prover has to know it too.
+    let mut c_running = {
+        let combined: Vec<F192> = round1_ab.iter().zip(&round1_c).map(|(x, y)| *x + *y).collect();
+        interpolate_at_z_combined(&combined, k_skip, z) + final_c_eval
+    };
     let mut mlv_rhos: Vec<F192> = Vec::with_capacity(n_mlv);
-    mlv_rhos.push(ps.sample());
+    c_running = send_round(ps, c_running, r_rest[0], msg_1, msg_inf, &mut mlv_rhos);
 
     // ---- Rounds 3..(n_mlv + 1): AB only (c is done) ----
     //
@@ -283,9 +300,7 @@ pub fn prove_packed_padded_capture_s_hat_v_c(
             round_pair_naive(&a_mlv, &b_mlv, r_eq)
         };
 
-        ps.add_scalar(m1);
-        ps.add_scalar(mi);
-        mlv_rhos.push(ps.sample());
+        c_running = send_round(ps, c_running, r_rest[i + 1], m1, mi, &mut mlv_rhos);
     }
 
     // ---- Final binding at ρ_{n_mlv} (the last challenge) ----
@@ -399,14 +414,11 @@ pub fn verify(log_n: usize, vs: &mut VerifierState<'_>) -> Result<ZerocheckClaim
     //      interpolation through G(0), G(1), G(∞)).
     let mut mlv_rhos: Vec<F192> = Vec::with_capacity(n_mlv);
     for i in 0..n_mlv {
-        let msg_1 = vs.next_scalar().map_err(VerifyError::Transcript)?;
-        let msg_inf = vs.next_scalar().map_err(VerifyError::Transcript)?;
         let r_eq = r_rest[i];
-        let one_plus_r_eq = F192::ONE + r_eq;
-
-        let g1 = msg_1;
-        let g_inf = msg_inf;
-        let g0 = (c_running + r_eq * g1) * one_plus_r_eq.inv();
+        let g = vs
+            .next_round_poly(3, c_running, Some(r_eq))
+            .map_err(VerifyError::Transcript)?;
+        let (g0, g1, g_inf) = (g[0], g[1], g[2]);
 
         let rho = vs.sample();
         mlv_rhos.push(rho);

crates/lean_vm/src/constraints.rs

@@ -53,7 +53,6 @@ pub struct Claims {
 #[derive(Clone, Debug, PartialEq, Eq)]
 pub enum Error {
     Truncated,
-    RoundInconsistent { round: usize },
     FinalMismatch,
 }
 
@@ -195,7 +194,8 @@ pub fn prove(
         let p4 = [msg[0], msg[1], msg[2], lagrange_eval(&nd, &msg, q[3])];
         let h: [F192; 4] = std::array::from_fn(|i| (F192::ONE + zeta[m] + q[i]) * p4[i] + q[i] * u);
         // A separate pass: the challenge only exists once the message is bound.
-        ps.add_scalars(&h);
+        // `h(0)` does not ride the wire; `h(0) + h(1) = claim` fixes it.
+        ps.add_round_poly(&h);
         let rk = ps.sample();
         rho[m] = rk;
         k *= rk;
@@ -264,10 +264,9 @@ pub fn verify(
     let mut rho = vec![F192::ZERO; n];
     for j in 0..n {
         let m = n - 1 - j;
-        let h = vs.next_scalars(4).map_err(|_| Error::Truncated)?;
-        if h[0] + h[1] != claim {
-            return Err(Error::RoundInconsistent { round: j });
-        }
+        // `h(0)` is derived from the running claim rather than transmitted, so
+        // the round-consistency check it used to enable holds by construction.
+        let h = vs.next_round_poly(4, claim, None).map_err(|_| Error::Truncated)?;
         let rk = vs.sample();
         rho[m] = rk;
         claim = lagrange_eval(&nd, &h, rk);