diff --git a/crates/lean_compiler/tests/suite/vm_proofs.rs b/crates/lean_compiler/tests/suite/vm_proofs.rs index c8cbdffc7..a9681717e 100644 --- a/crates/lean_compiler/tests/suite/vm_proofs.rs +++ b/crates/lean_compiler/tests/suite/vm_proofs.rs @@ -7,7 +7,7 @@ //! duplicating their knowledge of what a dummy row looks like. use lean_compiler::{compile, parse}; -use leanvm_core::cpu::{CpuError, Proof, ProveError, prove, verify}; +use leanvm_core::cpu::{CpuError, Proof, ProveError, prove, prove_claiming, verify}; use leanvm_core::vmhash::compress; use primitives::field::{F64, F192}; @@ -99,6 +99,22 @@ fn a_proof_does_not_verify_against_another_program() { ); } +/// The public-input claims are all that tie the committed memory to the statement: +/// a prover that runs on the real input but seeds the transcript with another passes +/// every other check, so the opening must reject it, whichever limb differs. +#[test] +fn a_proof_binds_the_memory_to_the_public_input() { + let program = compile(&parse(HASHING).expect("parse")); + let pi = hashing_pi(); + for claimed in [[pi[0] + F192::ONE, pi[1]], [pi[0], pi[1] + F192::new(0, 1, 0)]] { + let (forged, _) = prove_claiming(&program, pi, claimed, leanvm_core::pcs::TEST_LOG_INV_RATE).unwrap(); + assert!( + matches!(verify(&program, &claimed, &forged), Err(CpuError::Open(_))), + "a proof of memory not holding the public input must be rejected" + ); + } +} + /// Out-of-process verification: everything travels in the two channels, so a proof /// serializes, crosses a process boundary and verifies, and a flipped announced size /// is caught before any reduction runs. diff --git a/crates/leanvm_core/src/cpu/mod.rs b/crates/leanvm_core/src/cpu/mod.rs index 8de21934b..c454f793c 100644 --- a/crates/leanvm_core/src/cpu/mod.rs +++ b/crates/leanvm_core/src/cpu/mod.rs @@ -552,6 +552,19 @@ impl Stats { /// the commitment. #[tracing::instrument(name = "Prove", skip_all, fields(log_inv_rate))] pub fn prove(program: &Program, public_input: [F192; 2], log_inv_rate: usize) -> Result<(Proof, Stats), ProveError> { + prove_claiming(program, public_input, public_input, log_inv_rate) +} + +/// [`prove`], running on `public_input` but seeding the transcript with `claimed`. +/// Two different inputs make a forging prover, for the test that a proof binds the +/// committed memory to the statement; never a real proof. +#[doc(hidden)] +pub fn prove_claiming( + program: &Program, + public_input: [F192; 2], + claimed: [F192; 2], + log_inv_rate: usize, +) -> Result<(Proof, Stats), ProveError> { if ::pcs::whir::validate_log_inv_rate(log_inv_rate).is_err() { return Err(ProveError::InvalidRate { log_inv_rate }); } @@ -579,11 +592,8 @@ pub fn prove(program: &Program, public_input: [F192; 2], log_inv_rate: usize) -> let committed_size = w.committed_size(); // The public statement (program digest + input) seeds the transcript, so // every challenge depends on the exact program and public input. - debug_assert!( - public_input.iter().all(|h| h.c2 == 0), - "a public input is a 256-bit digest" - ); - let mut ps = ProverState::new(digest_words(&fs_seed(program)), digest_words(&public_input)); + debug_assert!(claimed.iter().all(|h| h.c2 == 0), "a public input is a 256-bit digest"); + let mut ps = ProverState::new(digest_words(&fs_seed(program)), digest_words(&claimed)); // Announce the prover's sizes, then commit, before sampling any challenge. announce_public(&mut ps, w.log_mem, w.layout.taus, log_inv_rate); @@ -633,23 +643,15 @@ pub fn prove(program: &Program, public_input: [F192; 2], log_inv_rate: usize) -> }; let l = &w.layout; - // The PI binding transmits the two LOW memory limbs' evaluations - // (§sec:e2e-pi); the verifier checks them against the public-input line at - // `r_pi`. The top limb of both public words is zero, so its evaluation is - // zero at every `r_pi` and rides no scalar. + // The PI binding (§sec:e2e-pi) transmits nothing: its claims are the public + // input's limb lines at `r_pi`, which the verifier evaluates itself. `r_pi` + // is still a challenge, squeezed after the commitment so the memory cannot + // be chosen to fit it. let r_pi = ps.sample(); - let pi_limbs = [ - primitives::multilinear::interp_k(F64(l.pi[0].c0), F64(l.pi[1].c0), r_pi), - primitives::multilinear::interp_k(F64(l.pi[0].c1), F64(l.pi[1].c1), r_pi), - F192::ZERO, - ]; - for v in &pi_limbs[..2] { - ps.add_scalar(*v); - } // Memory binds the message, chaining-value, and output words; bytecode binds // the counter and flags. All corresponding value columns are virtual and route // to q_flock through `slot_claims`. - let slots = finish_claims(l, bus.claims, &table_claims, r_pi, pi_limbs); + let slots = finish_claims(l, bus.claims, &table_claims, r_pi); // Run flock's reduction (zerocheck + lincheck) over the prepared native // layouts retained from the fused q_flock build pass; it returns the @@ -686,7 +688,6 @@ fn finish_claims( bus_claims: Vec, table_claims: &[constraints::Claims], r_pi: F192, - pi_limbs: [F192; 3], ) -> Vec { let mut claims = bus_claims; let sch = schema(); @@ -700,22 +701,27 @@ fn finish_claims( }); } } - claims.extend(bind_pi_claim(r_pi, &l.placements, pi_limbs)); + claims.extend(bind_pi_claim(r_pi, l)); slot_claims(l, claims) } -/// The public-input binding (§sec:e2e-pi): the committed `MEM` at `(r, 0,…,0)` must -/// equal `interp(pi[0], pi[1], r)`, one transmitted evaluation per physical `K` -/// limb. The caller has already checked the three against the line; here they -/// simply become the three claims the opening discharges. `placements` comes from -/// the prover's or verifier's layout, so both sides build byte-identical claims. -fn bind_pi_claim(r: F192, placements: &[witness::Placement], limbs: [F192; 3]) -> [ColumnClaim; 3] { - let mut point = vec![F192::ZERO; placements[MEM_LO].n_vars]; +/// The public-input binding (§sec:e2e-pi): each committed `MEM` limb at +/// `(r, 0,…,0)` must equal the line through that limb of `pi[0]` and `pi[1]`. +/// The public input is the statement, so both sides evaluate the lines +/// themselves and build byte-identical claims from their layouts; the prover +/// sends nothing. The verifier has rejected a nonzero top limb, so that claim is 0. +fn bind_pi_claim(r: F192, l: &Layout) -> [ColumnClaim; 3] { + let [a, b] = l.pi; + let limbs = [(a.c0, b.c0), (a.c1, b.c1), (a.c2, b.c2)]; + let mut point = vec![F192::ZERO; l.placements[MEM_LO].n_vars]; point[0] = r; - [MEM_LO, MEM_HI, MEM_TOP].map(|col| ColumnClaim { - col, - point: point.clone(), - value: limbs[col - MEM_LO], + [MEM_LO, MEM_HI, MEM_TOP].map(|col| { + let (x, y) = limbs[col - MEM_LO]; + ColumnClaim { + col, + point: point.clone(), + value: primitives::multilinear::interp_k(F64(x), F64(y), r), + } }) } @@ -779,18 +785,10 @@ pub fn verify(program: &Program, public_input: &[F192; 2], proof: &Proof) -> Res ) .map_err(CpuError::Constraint)?; + // Squeezed after the commitment and every message before it, so the prover + // cannot choose the memory to fit it; the claims it yields read no scalar. let r_pi = vs.sample(); - let mut pi_limbs = [F192::ZERO; 3]; - for v in &mut pi_limbs[..2] { - *v = vs.next_scalar().map_err(CpuError::Transcript)?; - } - // The two claimed evaluations must sit on the public-input line, the top - // limb's being zero (§sec:e2e-pi). - let want = primitives::multilinear::interp(l.pi[0], l.pi[1], r_pi); - if pi_limbs[0] + F192::Y * pi_limbs[1] != want { - return Err(CpuError::PublicInput); - } - let slots = finish_claims(&l, bus.claims, &table_claims, r_pi, pi_limbs); + let slots = finish_claims(&l, bus.claims, &table_claims, r_pi); // Replay flock's reduction straight off the shared stream (each scalar bound // as it is read) to recover its validity claim on q_flock, then diff --git a/crates/leanvm_core/src/pcs.rs b/crates/leanvm_core/src/pcs.rs index a13f5516b..3a23e93ad 100644 --- a/crates/leanvm_core/src/pcs.rs +++ b/crates/leanvm_core/src/pcs.rs @@ -124,9 +124,10 @@ pub fn commit( // The batching challenges are just `sample()`d inside the stacked opener: every // claim they combine is already bound: the values rode the stream -// (`add_scalar`) during the bus / constraint / public-input sub-protocols, the -// points are prior challenges, and the offsets are public (reconstructed -// identically from the announced layout). +// (`add_scalar`) during the bus / constraint sub-protocols or, for the +// public-input claims, are functions of the seeded statement and a prior +// challenge, the points are prior challenges, and the offsets are public +// (reconstructed identically from the announced layout). /// Verifier counterpart of [`commit`]'s root binding: read the committed root /// from the stream at the start of verification, before sampling any challenge. @@ -139,8 +140,9 @@ pub fn read_commitment(vs: &mut VerifierState) -> Result<[u8; 32], crate::transc /// ring-switched BLAKE2s validity claim (`ring`) in ONE stacked WHIR. /// The points become the opener's `point_claims`; the opening's Merkle data /// rides the transcript's phase list, not the scalar stream. The commitment root -/// was already bound by [`commit`], and the point *values* rode the stream -/// during their sub-protocols, so nothing extra is bound here. +/// was already bound by [`commit`], and the point *values* either rode the +/// stream or derive from the statement and prior challenges, so nothing extra +/// is bound here. /// /// There is no plain (non-ring-switch) path: the witness ALWAYS carries a `q_flock` /// sub-block (≥ 1 padding instance, §cpu), so every opening is stacked. diff --git a/crates/pcs/src/stack_open.rs b/crates/pcs/src/stack_open.rs index 920d7d9fb..d2e6b9005 100644 --- a/crates/pcs/src/stack_open.rs +++ b/crates/pcs/src/stack_open.rs @@ -354,8 +354,8 @@ pub fn verify_opening_batch_mixed_whir_stacked( let map_challenges = ring_switch::sample_map_challenges(vs); let coordinate_weights = ring_switch::build_coordinate_weights(&map_challenges); - // 2. The one batching challenge (see the opener: the claim values are bound by the read that - // produced them), then fold both families into the target over disjoint power ranges. + // 2. The one batching challenge (see the opener: the caller already bound the claim values), + // then fold both families into the target over disjoint power ranges. let lambdas = powers(vs.sample(), n_rs + point_claims.len()); let (lambdas_rs, lambdas_pd) = lambdas.split_at(n_rs); diff --git a/crates/rec_aggregation/guests/lean_ethereum.py b/crates/rec_aggregation/guests/lean_ethereum.py index d38855b60..97e2cf2a1 100644 --- a/crates/rec_aggregation/guests/lean_ethereum.py +++ b/crates/rec_aggregation/guests/lean_ethereum.py @@ -455,6 +455,16 @@ def assert_canonical(word): return 0 +@inline +def canonical_limbs(word): + # assert_canonical, keeping the two limbs it binds. + lo = StackBuf(1) + hint_f192_limbs(lo, word) + hi = (word + lo[0]) * Y_INV + assert_in_k(lo[0], hi) + return lo[0], hi + + @inline def challenge_from_state(state): # Both words are BLAKE2s outputs with zero top limbs. @@ -1723,21 +1733,17 @@ def verify_tables(fs0, fs1, cursor, pi_0, pi_1, zeta, g_bus_mu, dims_g, block_ka air_acc += zc_cprod[g_zc_n / tau_g] * zc_peq[tau_g] * constraint_eval # cprod[n - tau] * peq[tau] assert air_acc == claim - # ---- public-input binding claim: MEM as ONE logical E-column ---- - # The VM's bind_pi_claim makes a SINGLE E-claim at [rm, 0..]: - # MEM(rm) = interp(pi_0, pi_1, rm) = pi_0 + rm*(pi_0 + pi_1) - # over the E-valued public input (no lane splitting, no Frobenius). Both - # public words have a zero top limb, so that limb's evaluation is zero at - # every rm; only the two low ones ride the stream and must reassemble it: - # MEM = v_lo + Y*v_hi (doc sec:e2e-pi). + # ---- public-input binding claim: one per MEM limb, read off no stream ---- + # The VM's bind_pi_claim claims each committed MEM limb at [rm, 0..] equals + # that limb's line through the public words, lo_0 + rm*(lo_0 + lo_1) and so + # on, which the statement alone determines. canonical_limbs binds each word's + # limbs and proves its top limb zero, so the top claim is zero (doc sec:e2e-pi). fs, rm = squeeze(fs) - mem = pi_0 + rm * (pi_0 + pi_1) - fs, mem_lo, cursor = fs_next(fs, cursor) - fs, mem_hi, cursor = fs_next(fs, cursor) - assert mem == mem_lo + mem_hi * Y_TOWER - claim_pool[GEN ** claim_idx] = mem_lo + lo_0, hi_0 = canonical_limbs(pi_0) + lo_1, hi_1 = canonical_limbs(pi_1) + claim_pool[GEN ** claim_idx] = lo_0 + rm * (lo_0 + lo_1) claim_idx += 1 - claim_pool[GEN ** claim_idx] = mem_hi + claim_pool[GEN ** claim_idx] = hi_0 + rm * (hi_0 + hi_1) claim_idx += 1 claim_pool[GEN ** claim_idx] = 0 claim_idx += 1 @@ -2150,8 +2156,9 @@ def verify_sub(pi_0, pi_1, seed_0, seed_1, g_logs_pow2, g_squares, defer_out): zv_lo[xt] = zr_hi[xt] # ONE batching challenge for the whole pool: N_CLAIMS - 1 fewer Fiat-Shamir # compressions than a challenge per claim, and none for the values themselves, - # `fs_next` having bound every one of them as it read it, so `lam_cl` already - # depends on all of them. Disjoint power ranges, as for the zc_xi-powers above: + # `fs_next` having bound every one it read and the public-input ones deriving + # from the seeded statement and rm, so `lam_cl` already depends on all of + # them. Disjoint power ranges, as for the zc_xi-powers above: # the ring-switch claim takes lam_cl^0, the pool lam_cl^1 onward. fs, lam_cl = squeeze(fs) target = transposed_claim diff --git a/crates/rec_aggregation/src/aggregation.rs b/crates/rec_aggregation/src/aggregation.rs index 7f8e073c6..5bf739d1a 100644 --- a/crates/rec_aggregation/src/aggregation.rs +++ b/crates/rec_aggregation/src/aggregation.rs @@ -2651,7 +2651,7 @@ fn placeholder_map(kbc: usize) -> BTreeMap { ps("N_FIXED_CHALLENGE_ROUNDS", fixed_challenges.len().to_string()); ps("PHI8_NODES", flds(&primitives::field::PHI_8_TABLE_192[..128])); // Tower F192 = F64[Y]/(Y^3+Y+1), Y = new(0,1,0). Y_TOWER embeds Y for - // AIR lane reassembly; Y_INV helps derive the top PI-memory limb. + // AIR lane reassembly; Y_INV splits a canonical word into its two K limbs. let y_tower = F192::new(0, 1, 0); ps("Y_TOWER", dsl_u128(y_tower).to_string()); ps("Y_INV", f192_literal(y_tower.inv())); diff --git a/doc/leanvm/body/08-end-to-end-protocol.tex b/doc/leanvm/body/08-end-to-end-protocol.tex index b554ae0ad..30a704e82 100644 --- a/doc/leanvm/body/08-end-to-end-protocol.tex +++ b/doc/leanvm/body/08-end-to-end-protocol.tex @@ -30,11 +30,11 @@ \subsection{Public input}\label{sec:e2e-pi} \[ \mle{\mem}(X,0,\dots,0)\;=\;(1+X)(\textsf{input}_0+\textsf{input}_1y)+X(\textsf{input}_2+\textsf{input}_3y). \] -The verifier samples $r_m\in\E$. It can evaluate the right side at $r_m$ directly. For the left side, recall that the memory $\mem\in\E^{\le1}[X_1,\dots,X_{\kmem}]$ is committed as three limbs $\mem_0,\mem_1,\mem_2\in\K^{\le1}[X_1,\dots,X_{\kmem}]$, with $\mem=\mem_0+y\,\mem_1+y^2\,\mem_2$ (\S\ref{sec:memchan}). The prover sends $c_0,c_1\in\E$, claiming $c_0=\mle{\mem_0}(r_m,0,\dots,0)$ and $c_1=\mle{\mem_1}(r_m,0,\dots,0)$. The verifier checks +Recall that the memory $\mem\in\E^{\le1}[X_1,\dots,X_{\kmem}]$ is committed as three limbs $\mem_0,\mem_1,\mem_2\in\K^{\le1}[X_1,\dots,X_{\kmem}]$, with $\mem=\mem_0+y\,\mem_1+y^2\,\mem_2$ (\S\ref{sec:memchan}). Since $1,y,y^2$ is a basis of $\E$ over $\K$, the equality holds, as polynomials in $X$, exactly when it holds limb by limb, and every limb's right side is a line the verifier knows. The verifier samples $r_m\in\E$, computes \[ - c_0+y\,c_1\;\qeq\;(1+r_m)(\textsf{input}_0+\textsf{input}_1y)+r_m(\textsf{input}_2+\textsf{input}_3y), + c_0=(1+r_m)\,\textsf{input}_0+r_m\,\textsf{input}_2,\qquad c_1=(1+r_m)\,\textsf{input}_1+r_m\,\textsf{input}_3, \] -and pools the claims $c_0,c_1,0$ on $\mem_0,\mem_1,\mem_2$ at $(r_m,0,\dots,0)$, the last being $0$ because both public cells have top limb zero. If either cell is wrong, the two sides are distinct polynomials of degree at most one in $r_m$, so the check passes with probability at most $1/|\E|$ (Lemma~\ref{lem:sz}). +and pools the claims $c_0,c_1,0$ on $\mem_0,\mem_1,\mem_2$ at $(r_m,0,\dots,0)$, the last being $0$ because both public cells have top limb zero. The prover sends nothing: the claims are functions of the public input, which seeds the transcript, and of $r_m$, drawn after the commitment. If either cell is wrong, some limb's two sides are distinct polynomials of degree at most one in $r_m$, so its claim is true with probability at most $1/|\E|$ (Lemma~\ref{lem:sz}), and the opening rejects a false claim. \subsection{Filling the tables}\label{sec:e2e-pad} @@ -84,8 +84,8 @@ \subsection{The unrolled protocol}\label{sec:e2e-unrolled} \paragraph{Public input.} \begin{enumerate} -\item \textbf{Verifier.} Sample and sends $r_m\in\E$. -\item \textbf{Prover \& Verifier.} The prover sends $c_0,c_1 \in \E$; the verifier checks $c_0+y c_1$ against $(1+r_m)(\textsf{input}_0+\textsf{input}_1y)+r_m(\textsf{input}_2+\textsf{input}_3y)$ and pools $(c_0,c_1,0)$ as claims on $\mem_0,\mem_1,\mem_2$ at $(r_m,0,\dots,0)$ (\S\ref{sec:e2e-pi}). +\item \textbf{Verifier.} Samples and sends $r_m\in\E$. +\item \textbf{Verifier.} Computes $c_0,c_1$ from the public input and pools $(c_0,c_1,0)$ as claims on $\mem_0,\mem_1,\mem_2$ at $(r_m,0,\dots,0)$ (\S\ref{sec:e2e-pi}). The prover sends nothing. \end{enumerate} \paragraph{BLAKE2s validity.} @@ -101,5 +101,5 @@ \subsection{The unrolled protocol}\label{sec:e2e-unrolled} \item \textbf{Prover \& Verifier.} Each pooled claim is one evaluation of a column at a point, its value already supplied; via the stacking selectors (\S\ref{sec:stacking}) it becomes a weighted sum $\sum_w W_j(w)\,\widetilde q(w)=c_j$ over the stacked witness. (The ring-switched claim arrives already in this form, its weight supported on the $\qflock$ region.) \item \textbf{Verifier.} Sends one batching challenge $\lambda\in\E$, drawn after every claim value is bound. Claim $j$ takes the weight $\lambda^{j-1}$, the ring-switched claim first and the pooled column claims after: the $J$ weights are distinct powers of the one challenge (Theorem~\ref{thm:rbr}). \item \textbf{Prover \& Verifier.} Fold the $J$ claims into $W_\lambda=\sum_j\lambda^{j-1} W_j$ and $C_\lambda=\sum_j\lambda^{j-1} c_j$, and run the inner-product PCS opening on $\sum_w W_\lambda(w)\,\widetilde q(w)=C_\lambda$ (Annex~\ref{annex:pcs}), the verifier evaluating $W_\lambda$ itself. This one opening discharges every pooled claim; there is no separate reduction sumcheck. -\item \textbf{Verifier.} Accepts if every check above passed: the caps, the one bus root for both sides, the nonzero count root, every sumcheck's rounds and final value, the public-input line, flock's reduction, and the PCS opening. +\item \textbf{Verifier.} Accepts if every check above passed: the caps, the one bus root for both sides, the nonzero count root, every sumcheck's rounds and final value, flock's reduction, and the PCS opening. \end{enumerate} diff --git a/python-verifier/verifier.py b/python-verifier/verifier.py index c2f3f7612..5381c02a5 100644 --- a/python-verifier/verifier.py +++ b/python-verifier/verifier.py @@ -180,7 +180,6 @@ def __repr__(self) -> str: ZERO = E(0) ONE = E(1) GEN = E(2) -Y = E(0, 1) # the tower generator, y^3 = y + 1 def powers(base: E, count: int) -> list[E]: @@ -1389,10 +1388,11 @@ def verify_execution(bytecode: Sequence[K], public_input: Digest, proof: Proof) table_sumcheck_claims = table_sumcheck(layout.table_log_heights, bus.forms, constraint_powers, form_powers, bus.point, target, transcript) claims = [*bus.claims, *table_sumcheck_claims] - # 5] binding the public input + # 5] binding the public input: each memory limb's claim is that limb's public line at the challenge, which the verifier + # evaluates itself, so the prover sends nothing. Both public words are 128-bit, so the top limb's claim is zero. public_challenge = transcript.sample() - public_limbs = (*transcript.next_scalars(2), ZERO) - require(poly_eval(public_limbs, Y) == multilinear_eval(public_input.halves(), [public_challenge]), "public input check failed") + first, second = public_input.halves() + public_limbs = tuple(multilinear_eval(pair, [public_challenge]) for pair in ((first.c0, second.c0), (first.c1, second.c1), (first.c2, second.c2))) public_point = (public_challenge, *[ZERO] * (layout.placements[MEMORY_0].variables - 1)) claims.extend(ColumnClaim(column, public_point, value) for column, value in zip((MEMORY_0, MEMORY_1, MEMORY_2), public_limbs))