From 7f80c64110d9dc21f6df0c183e9011ca1b89c26f Mon Sep 17 00:00:00 2001 From: scaraven Date: Wed, 30 Sep 2026 10:57:28 +0100 Subject: [PATCH] Derive the public-input limb claims instead of transmitting them The public-input round squeezed r_pi, then had the prover send the two low memory limbs' evaluations at (r_pi, 0, ..., 0), which the verifier checked against the public-input line before pooling them with a zero top limb as claims on MEM_LO, MEM_HI and MEM_TOP. Each is the line through the public input's own limbs, which the verifier already has, so both sides now compute it: limb i claims interp_k(pi[0].c_i, pi[1].c_i, r_pi), and nothing is transmitted. r_pi is still squeezed at the same transcript position, after the commitment and the table sumcheck, so the committed memory cannot depend on it, and the squeeze still ratchets the state for flock's challenges. The claim values are functions of the seeded statement and r_pi, so they are fixed before the opening's batching challenge. All three verifiers move together: - Rust: bind_pi_claim evaluates the limb lines from the layout's public input on both sides; the line check and its two stream reads go. - Python: step 5 evaluates the limb lines; the dead Y constant goes. - Guest: canonical_limbs hints each public word's low limb and binds both limbs with assert_in_k, replacing two fs_next absorbs (two BLAKE2s compressions per verified child) and the reassembly assert. The proof stream is two scalars shorter. The spec (sec:e2e-pi) and the comments that said every pooled value rode the stream are updated. a_proof_binds_the_memory_to_the_public_input runs the prover on the real input but seeds its transcript with another (prove_claiming, doc-hidden) and requires the opening to reject it, for a low-limb and a high-limb difference. It fails if the public-input claims are dropped from finish_claims, which no honest-prover test notices. Co-authored-by: Claude Opus 5.5 --- crates/lean_compiler/tests/suite/vm_proofs.rs | 18 +++- crates/leanvm_core/src/cpu/mod.rs | 82 +++++++++---------- crates/leanvm_core/src/pcs.rs | 12 +-- crates/pcs/src/stack_open.rs | 4 +- .../rec_aggregation/guests/lean_ethereum.py | 37 +++++---- crates/rec_aggregation/src/aggregation.rs | 2 +- doc/leanvm/body/08-end-to-end-protocol.tex | 12 +-- python-verifier/verifier.py | 8 +- 8 files changed, 99 insertions(+), 76 deletions(-) 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))