wire format

CHANGELOG.md

@@ -13,6 +13,7 @@ Major revision: unified API, one verifier, one proof type, 7 provers, SIMD accel
 - **Single proof type** — `SumcheckProof<F>` replaces `Sumcheck<F>` and `ProductSumcheck<F>`.
 - **Transcript redesigned** — `send()`/`receive()`/`challenge()` replace `read()`/`write()`.
 - **Legacy entry points demoted** — use `runner::sumcheck()` with a prover type.
+- **Wire format: EvalsInfty.** `d` values per round instead of `d + 1`; consistency is now structural. Details in [docs/design.md §7a](docs/design.md).
 
 ### Added
 

README.md

@@ -104,6 +104,7 @@ Each prover comes in two variants:
 | `MultilinearProver` | `MultilinearProverLSB` |
 | `InnerProductProver` | `InnerProductProverLSB` |
 | `CoefficientProver` | `CoefficientProverLSB` |
+| `EqFactoredProver` | — |
 | `GkrProver` | — |
 
 See [`docs/design.md`](docs/design.md) for details.

docs/design.md

@@ -330,18 +330,54 @@ where
 
 ```rust
 pub struct SumcheckProof<F: Field> {
-    /// g_j evaluations per round: round_polys[j] has degree + 1 entries.
-    pub round_polynomials: Vec<Vec<F>>,
+    /// Round polynomial values per round, EvalsInfty wire format.
+    /// `round_polys[j]` has `d = degree()` entries (see §7a).
+    pub round_polys: Vec<Vec<F>>,
     /// Verifier challenges r_1, ..., r_v.
     pub challenges: Vec<F>,
     /// g(r_1, ..., r_v) -- the prover's claimed final evaluation.
     pub final_value: F,
 }
 ```
 
-This matches the protocol description exactly. The verifier can
-reconstruct any round's consistency check from `round_polynomials`
-and `challenges`.
+The verifier can reconstruct any round's consistency check from
+`round_polys` and `challenges`.
+
+### 7a. Wire format: EvalsInfty
+
+All provers emit round polynomials in **EvalsInfty** form — `d` values
+per round for a degree-`d` polynomial, one fewer than a full
+evaluation table:
+
+| d | Wire | Verifier recovers |
+|---|------|-------------------|
+| 1 | `[h(0)]` | `h(1) = claim − h(0)` |
+| ≥ 2 | `[h(0), h(∞), h(2), ..., h(d−1)]` | `h(1) = claim − h(0)` |
+
+`h(∞)` is the leading coefficient (coefficient of `x^d`). The
+verifier reconstructs `h(r)` by Lagrange-interpolating the
+degree-`(d−1)` residual `q(x) = h(x) − h(∞)·x^d` over the finite
+points `{0, 1, ..., d−1}` and then adding `h(∞)·r^d`.
+
+**Why this shape.**
+
+1. *Cheapest for product-structured summands.* The leading
+   coefficient is a difference-of-shifted-evaluations form
+   (see [BDDT25](https://eprint.iacr.org/2025/1117.pdf), Algorithm 3),
+   which is the minimal additional work beyond computing `h(0)`.
+2. *Consistency is structural.* The check `h(0) + h(1) = claim` is
+   enforced by the wire format rather than a runtime equality test.
+   The consequence is that a dishonest prover's misbehaviour no
+   longer surfaces as a mid-protocol `ConsistencyCheck` error — it
+   surfaces at the caller's oracle check, where `final_claim`
+   diverges from `proof.final_value`. Soundness is preserved; the
+   detection point moves by one step.
+3. *One byte saved per round* (compared to sending `d + 1`
+   evaluations), worth noting for transcript-size-sensitive callers.
+
+The runner and the verifier are both written once against this
+format; every concrete prover (multilinear, inner-product, GKR,
+eq-factored, coefficient of any degree, MSB or LSB) produces it.
 
 ## 8. The verifier
 
@@ -351,8 +387,11 @@ polynomial's degree:
 ```rust
 /// Verify a sum-check proof against a claimed sum.
 ///
-/// Checks per round: g_j(0) + g_j(1) = previous claim, and
-/// deg(g_j) <= expected_degree.
+/// Per round (EvalsInfty wire — see §7a): receives `d` values,
+/// derives `h_j(1) = claim − h_j(0)` from the consistency constraint,
+/// reconstructs the round polynomial from the received finite-point
+/// evaluations plus the leading coefficient, and evaluates at the
+/// challenge `r_j` to obtain the next round's claim.
 ///
 /// Returns the final claimed value and the challenge vector on success.
 /// The caller is responsible for the oracle check: verifying that
@@ -539,7 +578,7 @@ impl SumcheckInstanceProver<F, T> for Adapter<P> {
   performance. The adapter converts via `Into<F>` at the boundary.
 
 - **Return type**: Jolt expects `UniPoly<F>` (coefficients). Our trait
-  returns evaluations at {0, 1, ..., d}. Convert via interpolation or
+  returns the EvalsInfty wire (§7a). Convert via reconstruction or
   have the prover return coefficients directly.
 
 - **Batching**: Jolt's `BatchedSumcheck::prove` combines multiple instances
@@ -587,9 +626,9 @@ and use Toom-Cook to reduce the number of ss multiplications from
 
 **Trait compatibility**: this is entirely internal to `round()`. The prover
 maintains richer internal state (categorized accumulator tables) and uses
-cheaper multiplication routines, but returns the same `Vec<F>` of degree+1
-evaluations. A `SmallValueProver<F>` implements `SumcheckProver<F>` with
-unchanged `degree()` and `final_value()`.
+cheaper multiplication routines, but returns the same EvalsInfty wire (§7a).
+A `SmallValueProver<F>` implements `SumcheckProver<F>` with unchanged
+`degree()` and `final_value()`.
 
 ### Algorithms 5--6: EqPoly optimization
 

docs/slides.md

@@ -159,8 +159,9 @@ pub fn sumcheck_verify<F: SumcheckField, T: VerifierTranscript<F>>(
 ) -> Result<SumcheckResult<F>, SumcheckError>
 ```
 
-- Checks g_j(0) + g_j(1) = claim each round
-- Evaluates g_j(r_j) via Lagrange interpolation (any degree)
+- Receives `d` values per round (EvalsInfty wire format — next slide)
+- Consistency `g_j(0) + g_j(1) = claim` is structural, not a runtime check
+- Evaluates g_j(r_j) via polynomial reconstruction (any degree)
 - Returns `SumcheckResult { challenges, final_claim }`
 
 The verifier doesn't know g ([Thaler Remark 4.2](https://people.cs.georgetown.edu/jthaler/ProofsArgsAndZK.pdf)), so the oracle check
@@ -174,11 +175,34 @@ next_claim = result.final_claim;                   // WHIR, GKR (next layer)
 
 ---
 
+## Wire Format — EvalsInfty
+
+All provers emit round polynomials in the **EvalsInfty** format:
+`d` values per round for a degree-`d` polynomial, one fewer than a
+full evaluation table.
+
+| d | Wire | Recovered by verifier |
+|---|------|-----------------------|
+| 1 | `[h(0)]` | `h(1) = claim − h(0)` |
+| ≥ 2 | `[h(0), h(∞), h(2), …, h(d−1)]` | `h(1) = claim − h(0)` |
+
+`h(∞)` is the leading coefficient (coefficient of `x^d`).
+
+- **Cheapest for product-structured summands** — the leading
+  coefficient is a difference-of-shifted-evaluations form
+  ([BDDT25](https://eprint.iacr.org/2025/1117.pdf), Algorithm 3).
+- **Consistency is structural.** `h(0) + h(1) = claim` is enforced by
+  the wire format rather than a runtime check — a dishonest prover's
+  misbehavior surfaces at the caller's oracle check rather than
+  mid-protocol.
+
+---
+
 ## Unified Proof Type
 
 ```rust
 pub struct SumcheckProof<F: SumcheckField> {
-    pub round_polys: Vec<Vec<F>>,  // g_j at {0,1,...,d}
+    pub round_polys: Vec<Vec<F>>,  // g_j in EvalsInfty wire format
     pub challenges: Vec<F>,        // r_1, ..., r_v
     pub final_value: F,            // g(r_1, ..., r_v)
 }
@@ -199,8 +223,10 @@ lives on the prover via `&mut P` ownership, not in the proof.
 | `InnerProductProver` | 2 | `final_evaluations() -> (F, F)` |
 | `CoefficientProver` | d | — |
 | `GkrProver` | 2 | `claimed_w_values() -> (F, F)` |
+| `EqFactoredProver` *(available)* | 2 | `final_factors() -> (F, F)` |
 
-Each has MSB and LSB variants (except GkrProver: MSB only).
+MSB and LSB variants exist for the first three; `GkrProver` and
+`EqFactoredProver` are MSB-only.
 
 Same runner. Same verifier. Same proof type.
 
@@ -331,6 +357,69 @@ Reduce-to-one is a separate composable sub-protocol (Thaler §4.5.2).
 
 ---
 
+## Eq-Factored Sumcheck *(available)*
+
+Proves `H = Σ_{x ∈ {0,1}^v} eq(w, x) · p(x)` for fixed `w ∈ F^v` and
+multilinear `p`. Degree 2. Shows up in lookup arguments and any
+reduction that couples a public point to a witness polynomial via the
+multilinear equality predicate.
+
+```rust
+let mut prover = EqFactoredProver::new(w, p_evals);
+let proof = sumcheck(&mut prover, v, &mut t, noop_hook);
+let (p_r, eq_wr) = prover.final_factors();
+// proof.final_value == p_r · eq_wr
+```
+
+**Split-Value Optimization ([BDDT25](https://eprint.iacr.org/2025/1117.pdf) Algorithm 5).**
+`eq` factors over any split of the variables:
+
+```
+eq(w, x) = eq(w_L, x_L) · eq(w_R, x_R)
+```
+
+`eq(w, ·)` is stored as two half-tables of `2^{v/2}` entries each
+rather than a single `2^v` table, and round-polynomial contributions
+are streamed through a nested-sum kernel without materializing the
+product.
+
+- **Eq storage:** `O(2^v)` → `O(2^{v/2})`
+- First `v_L` rounds fold `eq_L`; remaining `v_R` rounds fold `eq_R`.
+- After the last round, `eq(w, r) = eq_L[0] · eq_R[0]`.
+
+---
+
+## BatchedEqFactoredProver *(future possibility)*
+
+WHIR's covector is an RLC of equality polynomials:
+
+```
+b(x) = Σ_i α_i · eq(ρ_i, x)
+```
+
+A batched split-value prover would take `Vec<(ρ_i, α_i)>` + witness
+`a` instead of a materialized covector, store each `eq(ρ_i, ·)` in
+split form, and stream all `k` factors through the nested-sum kernel
+per round.
+
+| | Time | Memory |
+|---|------|--------|
+| Current WHIR (`InnerProductProver` + materialized `b`) | `O(k · 2^v)` | `O(2^v)` |
+| Batched split-value | `O(k · 2^v)` | `O(k · 2^{v/2})` |
+
+- **Memory win** when `k < 2^{v/2}` — typical for WHIR (`v ~ 20`, `k`
+  in the dozens).
+- **Time essentially unchanged.** You skip the upfront covector
+  build but pay `k×` more per sumcheck round. Split-value is a
+  space optimization, not a time optimization — per-round
+  multiplication count is the same.
+
+**Status.** Not implemented. Requires coordination with the WHIR crate
+to thread `(ρ, α)` pairs through `update_covector` rather than RLC'ing
+into a flat table each round.
+
+---
+
 ## Two Orthogonal Axes
 
 Prover design has two independent choices:

src/proof.rs

@@ -16,8 +16,14 @@ use core::fmt;
 /// `final_value == g(r_1, ..., r_v)`) is the caller's responsibility.
 #[derive(Clone, Debug)]
 pub struct SumcheckProof<F: SumcheckField> {
-    /// Round polynomial evaluations: `round_polys[j]` contains
-    /// `g_j(0), g_j(1), ..., g_j(degree)`.
+    /// Round polynomial values, EvalsInfty wire format: `round_polys[j]`
+    /// contains `d = degree` values per round.
+    ///
+    /// - `d == 1`: `[g_j(0)]`. `g_j(1)` is derived from the consistency
+    ///   check `g_j(0) + g_j(1) = claim`.
+    /// - `d >= 2`: `[g_j(0), g_j(∞), g_j(2), g_j(3), ..., g_j(d-1)]` where
+    ///   `g_j(∞)` is the leading coefficient (coefficient of `x^d`).
+    ///   `g_j(1)` is derived from the consistency check as above.
     pub round_polys: Vec<Vec<F>>,
 
     /// Verifier challenges `r_1, ..., r_v`.

src/provers/coefficient.rs

@@ -261,10 +261,20 @@ where
         }
 
         let coeffs = self.evaluate_coefficients();
-
-        let mut evals = Vec::with_capacity(self.deg + 1);
-        for i in 0..=self.deg {
-            evals.push(eval_poly_at(&coeffs, F::from(i as u64)));
+        let d = self.deg;
+
+        // EvalsInfty wire format:
+        //   d == 0: [h(0)]
+        //   d == 1: [h(0)]                               (h(∞) derived from claim)
+        //   d >= 2: [h(0), h(∞), h(2), h(3), ..., h(d-1)]
+        if d <= 1 {
+            return vec![eval_poly_at(&coeffs, F::ZERO)];
+        }
+        let mut evals = Vec::with_capacity(d);
+        evals.push(eval_poly_at(&coeffs, F::ZERO)); // h(0) = coeffs[0]
+        evals.push(coeffs[d]); // h(∞) = leading coefficient
+        for i in 2..d {
+            evals.push(eval_poly_at(&coeffs, F::from(i as u64))); // h(i)
         }
         evals
     }
@@ -340,15 +350,13 @@ mod tests {
         let mut t = SanityTranscript::new(&mut trng);
         let proof = sumcheck(&mut prover, 4, &mut t, |_, _| {});
 
-        assert_eq!(
-            proof.round_polys[0][0] + proof.round_polys[0][1],
-            claimed_sum
-        );
-
+        // EvalsInfty: degree-1 round poly → wire is [h(0)]; h(1) = claim - h(0).
         let mut claim = claimed_sum;
         for (rp, &r) in proof.round_polys.iter().zip(&proof.challenges) {
-            assert_eq!(rp[0] + rp[1], claim);
-            claim = rp[0] + r * (rp[1] - rp[0]);
+            assert_eq!(rp.len(), 1, "EvalsInfty degree-1 wire length");
+            let h0 = rp[0];
+            let h1 = claim - h0;
+            claim = h0 + r * (h1 - h0);
         }
         assert_eq!(proof.final_value, claim);
     }
@@ -378,15 +386,16 @@ mod tests {
         // Same challenges (same transcript seed).
         assert_eq!(ml_proof.challenges, cp_proof.challenges);
 
-        // Same round polynomial evaluations.
+        // Same wire (EvalsInfty): both provers emit [h(0)] per round.
         for (i, (ml_rp, cp_rp)) in ml_proof
             .round_polys
             .iter()
             .zip(&cp_proof.round_polys)
             .enumerate()
         {
-            assert_eq!(ml_rp[0], cp_rp[0], "round {i}: q(0) mismatch");
-            assert_eq!(ml_rp[1], cp_rp[1], "round {i}: q(1) mismatch");
+            assert_eq!(ml_rp.len(), 1, "round {i}: EvalsInfty degree-1 wire length");
+            assert_eq!(cp_rp.len(), 1, "round {i}: EvalsInfty degree-1 wire length");
+            assert_eq!(ml_rp[0], cp_rp[0], "round {i}: h(0) mismatch");
         }
     }
 }