diff --git a/crates/lean_vm/src/constraints.rs b/crates/lean_vm/src/constraints.rs index 5d8ec2d0..ececd51c 100644 --- a/crates/lean_vm/src/constraints.rs +++ b/crates/lean_vm/src/constraints.rs @@ -39,7 +39,7 @@ use crate::colval::ColVal; use crate::transcript::{ProverState, VerifierState}; use primitives::field::{F64, F192, F192Unreduced, powers}; use primitives::multilinear::{ - add3, eq_table_arena, fold_high_inplace, fold_high_k, lagrange_eval, quad_nodes, shrink_eq_high, tri_nodes, xor3, + eq_table_arena, fold_high_inplace, fold_high_k, lagrange_eval, quad_nodes, shrink_eq_high, tri_nodes, }; use zk_alloc::ArenaVec; @@ -82,7 +82,15 @@ pub fn eta_offsets(n_constraints: impl Iterator) -> Vec { .collect() } -/// An active round for a table: evaluate its columns at the three nodes `{0,1,g}`. +/// An active round for a table: evaluate its columns at ONE Boolean node and at `g`. +/// +/// The round's other Boolean value is never evaluated. `h(0) + h(1)` is the running +/// claim, so one endpoint of the cofactor `p` determines the other, and a row only +/// has to be read at the endpoint that is not derived. `at_one` picks it: normally +/// `p(1)`, since `h(0) = (1 + ζ_m)·p(0)` is what the claim then hands back, and at +/// `ζ_m = 1` that coefficient vanishes, so `p(0)` is evaluated and `p(1)` derived. +/// Both nodes still have to be GATHERED, `g` being their interpolation, but the +/// identity is evaluated twice per row instead of three times. /// /// Generic twice over: in the column element, `K` before a table's columns are /// folded and `E` after ([`ColVal`]), and in the container, `Vec` for the former @@ -98,39 +106,39 @@ fn table_message + Sync>( pows: &[F192], half: usize, eqr: &[F192], -) -> [F192; 3] { + at_one: bool, +) -> [F192; 2] { let ncols = cols.len(); - let summand = |i: usize, scratch: &mut [T]| -> [F192Unreduced; 3] { + let summand = |i: usize, scratch: &mut [T]| -> [F192Unreduced; 2] { let e = eqr[i]; - let (v0, rest) = scratch.split_at_mut(ncols); - let (v1, v2) = rest.split_at_mut(ncols); + let (vb, vg) = scratch.split_at_mut(ncols); for (ci, c) in cols.iter().enumerate() { let (lo, hi) = (c[i], c[i + half]); - v0[ci] = lo; - v1[ci] = hi; - v2[ci] = T::at_g(lo, hi); + vb[ci] = if at_one { hi } else { lo }; + vg[ci] = T::at_g(lo, hi); } - [ - e.mul_unreduced(eval(pows, v0)), - e.mul_unreduced(eval(pows, v1)), - e.mul_unreduced(eval(pows, v2)), - ] + [e.mul_unreduced(eval(pows, vb)), e.mul_unreduced(eval(pows, vg))] + }; + let xor2 = |mut x: [F192Unreduced; 2], y: [F192Unreduced; 2]| { + x[0] ^= y[0]; + x[1] ^= y[1]; + x }; let acc = if half >= PAR_THRESHOLD { - // The `3 * ncols` scratch is per-worker, not per-row: `map_reduce_with_state` + // The `2 * ncols` scratch is per-worker, not per-row: `map_reduce_with_state` // creates it once and threads it through every row that worker claims. parallel::map_reduce_with_state( half, - || vec![T::ZERO; 3 * ncols], - || [F192Unreduced::ZERO; 3], - |scratch, acc, i| *acc = xor3(*acc, summand(i, scratch)), - xor3, + || vec![T::ZERO; 2 * ncols], + || [F192Unreduced::ZERO; 2], + |scratch, acc, i| *acc = xor2(*acc, summand(i, scratch)), + xor2, ) } else { - let mut scratch = vec![T::ZERO; 3 * ncols]; - (0..half).fold([F192Unreduced::ZERO; 3], |acc, i| xor3(acc, summand(i, &mut scratch))) + let mut scratch = vec![T::ZERO; 2 * ncols]; + (0..half).fold([F192Unreduced::ZERO; 2], |acc, i| xor2(acc, summand(i, &mut scratch))) }; - [acc[0].reduce(), acc[1].reduce(), acc[2].reduce()] + [acc[0].reduce(), acc[1].reduce()] } /// Prove that every table's batched constraint vanishes on all of its rows, as ONE @@ -162,6 +170,9 @@ pub fn prove( let mut folded: Vec>>> = (0..airs.len()).map(|_| None).collect(); // `k`, the challenges drawn so far, common to every air that is still waiting. let mut k = F192::ONE; + // The verifier's running claim, tracked here too: it is what supplies the + // Boolean endpoint this round does not evaluate. + let mut claim = sigma.iter().fold(F192::ZERO, |acc, &s| acc + s); for j in 0..n { let m = n - 1 - j; // the variable this round binds // The waiting airs contribute the line `Y·k·Σσ`, whose slope `u` is all there @@ -173,18 +184,31 @@ pub fn prove( .filter(|(a, _)| a.tau <= m) .fold(F192::ZERO, |acc, (_, &s)| acc + s); let u = k * waiting; - let mut msg = [F192::ZERO; 3]; + // `h(0) = (1+ζ_m)·p(0)` and `h(1) = ζ_m·p(1) + u`, and the two sum to the + // claim, so the rows only have to answer for one of them. `1+ζ_m` is the + // coefficient that has to be inverted to recover `p(0)`, so the evaluated + // node flips at the one point where it vanishes. + let at_one = zeta[m] != F192::ONE; + let mut sent = [F192::ZERO; 2]; for (t, air) in airs.iter().enumerate() { if air.tau > m { let w = &pows[offsets[t]..offsets[t] + air.n_constraints]; let p = if let Some(table) = &folded[t] { - table_message(table, &*air.eval, w, 1 << m, &eqr) + table_message(table, &*air.eval, w, 1 << m, &eqr, at_one) } else { - table_message(&cols[t], &*air.eval_k, w, 1 << m, &eqr) + table_message(&cols[t], &*air.eval_k, w, 1 << m, &eqr, at_one) }; - msg = add3(msg, p.map(|x| weights[t] * x)); + sent[0] += weights[t] * p[0]; + sent[1] += weights[t] * p[1]; } } + let msg = if at_one { + let p1 = sent[0]; + [(claim + zeta[m] * p1 + u) * (F192::ONE + zeta[m]).inv(), p1, sent[1]] + } else { + // `1 + ζ_m = 0` kills `h(0)` outright, leaving `h(1)` alone to carry the claim. + [sent[0], claim + u, sent[1]] + }; shrink_eq_high(&mut eqr); // Assemble `h` and send it whole. The cofactor `p` is degree 2, so its value // at the fourth node is an interpolation of three scalars, NOT another pass @@ -194,9 +218,11 @@ pub fn prove( debug_assert_eq!(q[..3], nd[..], "the cubic's first three nodes are the cofactor's"); 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); + debug_assert_eq!(h[0] + h[1], claim, "the derived endpoint must close the round"); // A separate pass: the challenge only exists once the message is bound. ps.add_scalars(&h); let rk = ps.sample(); + claim = lagrange_eval(&q, &h, rk); rho[m] = rk; k *= rk; let eq_k = F192::ONE + zeta[m] + rk; @@ -434,6 +460,36 @@ mod tests { } } + /// `ζ_m = 1` is the one point where the round cannot derive `p(0)`, and a + /// sampled `ζ` never lands on it, so the flipped branch is only ever reached + /// here. `τ = 12` also puts the first round's half-table exactly at + /// `PAR_THRESHOLD`, covering the parallel reducer alongside the serial one. + #[test] + fn unit_eq_coordinates_verify() { + let taus = [12usize, 3, 5, 0, 1]; + let cols: Vec>> = taus.iter().enumerate().map(|(i, &t)| good_table(t, i as u64)).collect(); + let (eta, mut zeta) = eta_zeta(&taus); + // First round, a middle round, and the last: the branch has to hold wherever + // it falls, including a round in which short tables are still waiting. + for m in [11usize, 3, 0] { + zeta[m] = F192::ONE; + } + let pows = powers(eta, 3 * taus.len()); + let sigmas: Vec = taus + .iter() + .enumerate() + .map(|(t, &tau)| pows[3 * t + 2] * primitives::multilinear::mle_eval(&cols[t][1], &zeta[..tau])) + .collect(); + let airs = airs_for(&taus, true); + let target = sigmas.iter().fold(F192::ZERO, |a, &b| a + b); + let mut ps = ProverState::new(b"zc-test", &SEED); + let views: Vec> = cols.iter().map(|t| t.iter().map(|c| &c[..]).collect()).collect(); + let pclaims = prove(&airs, &views, eta, &zeta, &sigmas, &mut ps); + let proof = ps.into_proof(); + let mut vs = VerifierState::new(b"zc-test", &proof, &SEED); + assert_eq!(verify(&airs, eta, &zeta, target, &mut vs), Ok(pclaims)); + } + /// Tampering any transmitted word breaks the chain: the batch is one sumcheck, /// so there is no per-table slack. #[test]