Derive the public-input limb claims instead of transmitting them

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.

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<ColumnClaim>,
     table_claims: &[constraints::Claims],
     r_pi: F192,
-    pi_limbs: [F192; 3],
 ) -> Vec<pcs::SlotClaim> {
     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

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.

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);
 

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

crates/rec_aggregation/src/aggregation.rs

@@ -2651,7 +2651,7 @@ fn placeholder_map(kbc: usize) -> BTreeMap<String, String> {
     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()));

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}

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))