Skip to content

constraints: derive one sumcheck endpoint from the running claim #6

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
TomWambsgans wants to merge 1 commit into
base: main
Choose a base branch
from
Open

constraints: derive one sumcheck endpoint from the running claim #6

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
108 changes: 82 additions & 26 deletions crates/lean_vm/src/constraints.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down Expand Up @@ -82,7 +82,15 @@ pub fn eta_offsets(n_constraints: impl Iterator<Item = usize>) -> Vec<usize> {
.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
Expand All @@ -98,39 +106,39 @@ fn table_message<T: ColVal, C: std::ops::Deref<Target = [T]> + 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
Expand Down Expand Up @@ -162,6 +170,9 @@ pub fn prove(
let mut folded: Vec<Option<Vec<ArenaVec<F192>>>> = (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
Expand All @@ -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
Expand All @@ -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;
Expand Down Expand Up @@ -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<Vec<Vec<F64>>> = 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<F192> = 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<Vec<&[F64]>> = 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]
Expand Down
Loading