From 571205a6b10d906977e5c82122194006807bf640 Mon Sep 17 00:00:00 2001 From: Tom Wambsgans Date: Sat, 22 Aug 2026 15:02:42 +0200 Subject: [PATCH 01/13] Compiler-soundness test infrastructure A dropped constraint is the compiler's quietest failure: the happy path passes, nothing is diagnosed, and the only symptom is a proof of something weaker than the source says. Positive tests cannot catch it, so attack the absence of a constraint from three sides. - Perturbation (soundness/cases.rs), the shape of ../leanVM's own test_soundness_suite: one valid trial per program plus a table of single-cell pokes at the public input or a witness stream, each of which must make the run fail. Six cases covering the arithmetic relations, both assert forms, the division back-solve, the exponent range check, match_range dispatch, an if/else join, a mul_range loop with a runtime bound, pack64x2's K-range assertion, and the digest-as-verification idiom. - Equivalence (soundness/pairs.rs): two spellings zkDSL.md documents as interchangeable must accept exactly the same trials. This is the layer that finds dropped stores. A dropped store is invisible alone, since the program still runs and its honest witness still passes; it is obvious against a spelling that kept it, and the more permissive side is the buggy one. Each pair carries the promise it tests, to be quoted in the bug report. - Unconstrained reads (Execution::unconstrained_reads, asserted in cpu::prove): a cell an instruction read that nothing ever wrote. zkDSL.md says don't; this is what says whether the emitted code did. Read off the count and written vectors after the run rather than recorded in Mem::get, which is in the opcode loop, so it costs the prover nothing. Scoped to the program's own cells, below where the fill's frames begin: fill rows read cells nobody writes as a matter of course and are soundness-neutral for it. A hard assert rather than a debug_assert, since release is the only profile the VM runs in. The invariant holds today for every program in the repo, including the recursion guest: aggregate_one_signer and aggregate_two_to_one prove clean under it. Co-Authored-By: Claude Opus 5 (1M context) --- AGENTS.md | 10 + crates/lean_compiler/tests/suite/main.rs | 1 + .../tests/suite/soundness/cases.rs | 272 ++++++++++++++++++ .../tests/suite/soundness/mod.rs | 263 +++++++++++++++++ .../tests/suite/soundness/pairs.rs | 188 ++++++++++++ crates/lean_vm/src/cpu/execute.rs | 35 +++ crates/lean_vm/src/cpu/mod.rs | 14 + 7 files changed, 783 insertions(+) create mode 100644 crates/lean_compiler/tests/suite/soundness/cases.rs create mode 100644 crates/lean_compiler/tests/suite/soundness/mod.rs create mode 100644 crates/lean_compiler/tests/suite/soundness/pairs.rs diff --git a/AGENTS.md b/AGENTS.md index ba2288189..21256aee9 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -38,6 +38,16 @@ Dependency order, leaves first: - always run in `--release` mode any test or benchmark touching the VM (the zkDSL compiler stack-overflows in `debug` mode) - **One test binary per crate, not one per file:** new `lean_compiler` integration tests go in `tests/suite/main.rs`, one linked executable instead of seventeen. Exception: a test opening an arena phase (`lean_vm::init_prover`) needs its own binary. Phases are process-global, so two in one process reclaim each other's `ArenaVec`s and the symptom is a proof that stops verifying, never a crash (`rec_aggregation/tests/arena_prove.rs`). +## Compiler soundness + +A dropped constraint is the compiler's worst failure mode and its quietest: the happy path passes, no diagnostic is emitted, and the only symptom is a proof of something weaker than the source says. Positive tests cannot catch it, so `lean_compiler/tests/suite/soundness/` attacks the *absence* of a constraint from three sides. Every compiler fix in this area lands with a test in whichever layer catches it. + +- **Perturbation** (`soundness/cases.rs`): one valid trial per program, then a table of single-cell pokes at the public input or a witness stream, each of which must make the run fail. A poke that is accepted names the missing constraint. Same shape as `../leanVM`'s own `test_soundness_suite`. +- **Equivalence** (`soundness/pairs.rs`): two spellings `zkDSL.md` documents as interchangeable must accept exactly the same trials. This is the layer that finds dropped stores, because a dropped store is invisible alone and obvious against a spelling that kept it: the more permissive side is the buggy one. Each `Pair` carries the promise it tests in its `why` field. +- **Unconstrained reads** (`Execution::unconstrained_reads`, asserted in `cpu::prove`): a cell an instruction read that nothing ever wrote. Such a value is ZERO under the interpreter and prover-chosen in a proof, since memory is a committed array and the bus only forces accesses to one address to *agree*, never that the address was written. Scoped to the program's own cells: the fill blocks read cells nobody writes as a matter of course, and are soundness-neutral for it. + +The three are complementary. Layer 3 sees a dropped store whose cell is then *read*; layer 2 sees one whose cell is then *ignored*, the value coming from the alias while the physical write is orphaned, which layer 3 cannot see because nothing reads the orphan. Layer 1 needs a program whose assertion a poke can violate, and in exchange needs no second spelling. + An x86-only arm never compiles on an Apple dev machine, so a typo in one ships. Type-check the other target before pushing anything `cfg`-gated: ```bash diff --git a/crates/lean_compiler/tests/suite/main.rs b/crates/lean_compiler/tests/suite/main.rs index ec42628d8..ce3a0c991 100644 --- a/crates/lean_compiler/tests/suite/main.rs +++ b/crates/lean_compiler/tests/suite/main.rs @@ -25,6 +25,7 @@ mod pack64x2; mod print_debug; mod py_source; mod range_check; +mod soundness; mod stack_buf; mod transcript_helpers; mod vm_proofs; diff --git a/crates/lean_compiler/tests/suite/soundness/cases.rs b/crates/lean_compiler/tests/suite/soundness/cases.rs new file mode 100644 index 000000000..54f0b8da2 --- /dev/null +++ b/crates/lean_compiler/tests/suite/soundness/cases.rs @@ -0,0 +1,272 @@ +//! Layer 1: perturbation. Each case is one program with one valid trial and a +//! table of single-cell pokes that must break it. +//! +//! Coverage is by *lowering*, not by feature list: every case exercises a +//! construct whose lowering could plausibly drop the check it stands for, and +//! every poke names one constraint. A poke that is accepted says which one is +//! missing. +//! +//! The pokes lean on witness streams rather than the public input, because two +//! public words is all there is and because the streams are where a real guest's +//! untrusted data actually enters. + +use super::{Case, Trial, check_case, g, k, pi, wit}; +use primitives::field::F192; + +/// `XOR`/`MUL` relations, both assert forms, and the division back-solve. The +/// quotient cell is written by nothing but the back-solve, so this case also +/// pins the one legitimate way a cell may be read before any instruction writes +/// it. +#[test] +fn arithmetic_and_asserts() { + check_case(&Case { + name: "arithmetic_and_asserts", + src: "\ +def main(): + v = StackBuf(3) + hint_witness(v, \"w\") + assert v[0] * v[1] == v[2] + assert v[0] != v[1] + q = v[2] / v[0] + assert q == v[1] + p = GEN ** 0 + p[1] = v[2] + p[GEN] = v[0] + v[1] + return +", + valid: Trial::new([g(8), g(3) + g(5)]).stream("w", vec![vec![g(3), g(5), g(8)]]), + pokes: vec![ + // Each of the three hinted cells breaks the product relation. + wit("w", 0, g(4)), + wit("w", 1, g(6)), + wit("w", 2, g(9)), + // Equal operands: the product relation would still need v[2] = g^10, + // but this is the poke that `assert !=` exists for. + wit("w", 0, g(5)), + // Both published words. + pi(0, g(9)), + pi(1, g(3) + g(6)), + ], + }); +} + +/// The exponent range check and `match_range` dispatch. The dispatch is only +/// sound because the matched value was range-checked first (doc §Match +/// statements), so a poke past the bound must be caught by the check rather than +/// land at an attacker-chosen arm. +#[test] +fn range_check_and_dispatch() { + check_case(&Case { + name: "range_check_and_dispatch", + src: "\ +def main(): + v = StackBuf(2) + hint_witness(v, \"w\") + assert log(v[0]) < 8 + r = match_range(log(v[0]), range(0, 8), lambda i: sq(i)) + assert r == v[1] + p = GEN ** 0 + p[1] = v[0] + p[GEN] = r + return + + +def sq(x): + return x * x +", + // Arm 3 runs: sq(3) = 3·3 in K = (x+1)^2 = x^2+1 = 5. + valid: Trial::new([g(3), k(5)]).stream("w", vec![vec![g(3), k(5)]]), + pokes: vec![ + // Past the bound: the range check's complement DEREF must catch it. + wit("w", 0, g(8)), + wit("w", 0, g(63)), + // A different arm runs, so the claimed square is wrong. + wit("w", 0, g(4)), + // The claimed square itself. + wit("w", 1, k(6)), + pi(0, g(4)), + pi(1, k(6)), + ], + }); +} + +/// `if`/`else` communicating through a write-once heap cell: only one arm runs, +/// so both may write it and the join reads it back. A lowering that lets the +/// join read anything other than the taken arm's value shows up as a poke that +/// selects the other arm and is still accepted. +#[test] +fn branch_join() { + check_case(&Case { + name: "branch_join", + src: "\ +def main(): + v = StackBuf(2) + hint_witness(v, \"w\") + assert log(v[0]) < 4 + r = HeapBuf(1) + if v[0] == GEN ** 2: + r[1] = v[1] * GEN + else: + r[1] = v[1] * GEN ** 3 + p = GEN ** 0 + p[1] = r[1] + p[GEN] = v[0] + return +", + valid: Trial::new([g(6), g(2)]).stream("w", vec![vec![g(2), g(5)]]), + pokes: vec![ + // Takes the else arm, which multiplies by g^3 instead of g. + wit("w", 0, g(1)), + wit("w", 0, g(3)), + // Past the bound. + wit("w", 0, g(4)), + // The value the taken arm shifts. + wit("w", 1, g(4)), + pi(0, g(7)), + pi(1, g(3)), + ], + }); +} + +/// A `mul_range` loop with a runtime bound and heap-carried state. The bound is +/// hinted, so the loop terminates only because its log was checked first; the +/// pokes cover both a bound that changes the trip count and one past the check. +#[test] +fn loop_with_runtime_bound() { + check_case(&Case { + name: "loop_with_runtime_bound", + src: "\ +def main(): + v = StackBuf(1) + hint_witness(v, \"n\") + assert log(v[0]) < 8 + acc = HeapBuf(16) + acc[1] = GEN ** 0 + for i in mul_range(1, v[0]): + acc[i * GEN] = acc[i] * GEN ** 2 + p = GEN ** 0 + p[1] = acc[v[0]] + p[GEN] = v[0] + return +", + // n = g^5: five iterations, acc[j] = g^{2j}, so acc[5] = g^10. + valid: Trial::new([g(10), g(5)]).stream("n", vec![vec![g(5)]]), + pokes: vec![ + // Fewer and more iterations: acc[n] is then g^8 and g^12. + wit("n", 0, g(4)), + wit("n", 0, g(6)), + // Past the bound. + wit("n", 0, g(8)), + pi(0, g(11)), + pi(1, g(4)), + ], + }); +} + +/// `pack64x2`'s range assertion: both sources must lie in K. The interpreter +/// enforces it directly, and the memory bus enforces it in a proof through the +/// tuple's literal-zero upper limbs. +#[test] +fn pack64x2_range_assertion() { + check_case(&Case { + name: "pack64x2_range_assertion", + src: "\ +def main(): + v = StackBuf(2) + hint_witness(v, \"w\") + c = pack64x2(v[0], v[1]) + p = GEN ** 0 + p[1] = c + p[GEN] = v[0] + return +", + valid: Trial::new([F192::new(5, 7, 0), k(5)]).stream("w", vec![vec![k(5), k(7)]]), + pokes: vec![ + // Either source outside K. + wit("w", 0, F192::new(5, 1, 0)), + wit("w", 0, F192::new(5, 0, 1)), + wit("w", 1, F192::new(7, 1, 0)), + // In K, but not the packing that was published. + wit("w", 0, k(6)), + wit("w", 1, k(8)), + pi(0, F192::new(5, 8, 0)), + pi(1, k(6)), + ], + }); +} + +/// The digest-as-verification idiom: a hinted preimage, hashed, and the result +/// pinned against a hinted digest through a heap store. This is the shape a +/// signature verifier has, so it is the one that most needs a regression test. +/// +/// The digest constant comes from [`print_blake2s_digest`], not from a hand +/// computation: what the case tests is that a *wrong* digest is rejected, and +/// for that the honest value only has to be honest. +#[test] +fn digest_pins_its_preimage() { + check_case(&Case { + name: "digest_pins_its_preimage", + src: BLAKE2S_PIN_SRC, + valid: Trial::new([k(5), k(7)]) + .stream("msg", vec![vec![k(5), k(7), F192::ZERO, F192::ZERO]]) + .stream("dig", vec![vec![DIGEST_5_7[0], DIGEST_5_7[1]]]), + pokes: vec![ + // A different preimage hashes to something else. + wit("msg", 0, k(6)), + wit("msg", 1, k(8)), + wit("msg", 2, k(1)), + wit("msg", 3, k(1)), + // A wrong digest is what the write-once store has to catch. + wit("dig", 0, F192::ZERO), + wit("dig", 1, F192::ZERO), + wit("dig", 0, DIGEST_5_7[0] + F192::ONE), + wit("dig", 1, DIGEST_5_7[1] + F192::ONE), + // The published preimage words. + pi(0, k(6)), + pi(1, k(8)), + ], + }); +} + +const BLAKE2S_PIN_SRC: &str = "\ +def main(): + m = StackBuf(4) + hint_witness(m, \"msg\") + d = StackBuf(2) + blake2s(m[0:2], m[2:4], d) + e = HeapBuf(2) + hint_witness(e[0:2], \"dig\") + e[1] = d[0] + e[GEN] = d[1] + p = GEN ** 0 + p[1] = m[0] + p[GEN] = m[1] + return +"; + +/// BLAKE2s of the 64-byte block whose four canonical cells are `(5, 7, 0, 0)`. +const DIGEST_5_7: [F192; 2] = [ + F192::new(0xbbc8_c175_8cb7_7642, 0xf299_5d40_1fad_f4ff, 0), + F192::new(0x83ea_6ade_289a_53c8, 0x57e6_e523_12ec_734b, 0), +]; + +/// Regenerate [`DIGEST_5_7`]: `cargo test --release -p lean_compiler +/// print_blake2s_digest -- --ignored --nocapture`. Kept so the constant above is +/// reproducible rather than folklore. +#[test] +#[ignore = "prints a constant; not a check"] +fn print_blake2s_digest() { + let src = "\ +def main(): + m = StackBuf(4) + hint_witness(m, \"msg\") + d = StackBuf(2) + blake2s(m[0:2], m[2:4], d) + print(d[0]) + print(d[1]) + return +"; + let mut p = super::build(src); + p.set_witness("msg", vec![vec![k(5), k(7), F192::ZERO, F192::ZERO]]); + p.execute([F192::ZERO, F192::ZERO]); +} diff --git a/crates/lean_compiler/tests/suite/soundness/mod.rs b/crates/lean_compiler/tests/suite/soundness/mod.rs new file mode 100644 index 000000000..a43b4abb0 --- /dev/null +++ b/crates/lean_compiler/tests/suite/soundness/mod.rs @@ -0,0 +1,263 @@ +//! Compiler-soundness harness: does the emitted bytecode still carry every +//! constraint the source asked for? +//! +//! A dropped constraint is invisible to ordinary tests. The happy path passes +//! either way, the compiler emits no diagnostic, and the symptom only appears as +//! a proof that accepts something it should not. So the three checks below all +//! attack the *absence* of a constraint rather than the presence of a value. +//! +//! 1. [`check_case`] — **perturbation**. One valid trial that must run, and a +//! table of single-cell pokes at the public input or a witness stream, each of +//! which must make the run fail. A dropped assertion shows up as a poke that +//! is accepted. (This is the shape of `leanVM`'s own soundness suite.) +//! 2. [`check_pair`] — **equivalence**. Two spellings the language documents as +//! interchangeable must accept exactly the same trials. Every dropped-constraint +//! bug found so far is an *asymmetry*: an assertion that survives one spelling +//! and vanishes in the other, so comparing the two finds it without anyone +//! having to guess which side is wrong. +//! 3. [`Execution::unconstrained_reads`] — **unconstrained reads**, asserted on +//! every accepting run of both layers above. A cell an instruction read that +//! nothing ever wrote is a live value from outside the constraint system. +//! +//! The three are complementary, and a fix should land with whichever one catches +//! it. Layer 3 sees a dropped store whose cell is then *read* (the value came from +//! nowhere); layer 2 sees a dropped store whose cell is then *ignored* (the value +//! came from the alias instead, and the physical write is orphaned) — layer 3 is +//! blind to that one, because nothing reads the orphan. Layer 1 needs a program +//! whose assertion the poke can violate, and in exchange it needs no second +//! spelling to compare against. + +#![allow(dead_code)] + +use lean_compiler::{compile_without_filler, parse}; +use lean_vm::cpu::Program; +use primitives::field::{F64, F192, g_pow}; + +mod cases; +mod pairs; + +/// `g^k` as a machine word, the way every index, address and counter is written. +pub fn g(k: usize) -> F192 { + F192::from(g_pow(k)) +} + +/// A K-valued literal in the low lane. +pub fn k(x: u64) -> F192 { + F192::from(F64(x)) +} + +/// One `hint_witness` stream: the name, then one entry per call naming it. +pub type Stream = (&'static str, Vec>); + +/// Everything a run consumes: the public statement and the prover's advice. +#[derive(Clone)] +pub struct Trial { + pub pi: [F192; 2], + pub streams: Vec, +} + +impl Trial { + pub fn new(pi: [F192; 2]) -> Self { + Self { + pi, + streams: Vec::new(), + } + } + + /// Add a stream whose every call takes one entry of `cells`. + pub fn stream(mut self, name: &'static str, entries: Vec>) -> Self { + self.streams.push((name, entries)); + self + } + + fn poke(&self, p: &Poke) -> Self { + let mut t = self.clone(); + match *p { + Poke::Pi { slot, to } => t.pi[slot] = to, + Poke::Wit { name, entry, cell, to } => { + let s = t + .streams + .iter_mut() + .find(|(n, _)| *n == name) + .unwrap_or_else(|| panic!("no stream `{name}` in this trial")); + s.1[entry][cell] = to; + } + } + t + } +} + +/// A single-cell mutation of a trial. One cell, so a poke that is accepted names +/// exactly the constraint that is missing. +#[derive(Clone, Copy)] +pub enum Poke { + /// Public-input word 0 or 1. + Pi { slot: usize, to: F192 }, + /// Cell `cell` of entry `entry` of witness stream `name`. + Wit { + name: &'static str, + entry: usize, + cell: usize, + to: F192, + }, +} + +impl Poke { + fn label(&self) -> String { + match self { + Poke::Pi { slot, to } => format!("pi[{slot}] := {:x}:{:x}:{:x}", to.c2, to.c1, to.c0), + Poke::Wit { name, entry, cell, to } => { + format!("{name}[{entry}][{cell}] := {:x}:{:x}:{:x}", to.c2, to.c1, to.c0) + } + } + } +} + +/// Poke a public-input word. +pub fn pi(slot: usize, to: F192) -> Poke { + Poke::Pi { slot, to } +} + +/// Poke cell `cell` of the first entry of stream `name`. +pub fn wit(name: &'static str, cell: usize, to: F192) -> Poke { + Poke::Wit { + name, + entry: 0, + cell, + to, + } +} + +/// Poke cell `cell` of entry `entry` of stream `name`. +pub fn wit_at(name: &'static str, entry: usize, cell: usize, to: F192) -> Poke { + Poke::Wit { name, entry, cell, to } +} + +/// What an honest run of the emitted bytecode did. +pub enum Ran { + /// It completed. Carries the cells it read that nothing ever wrote, which + /// must be empty for the program to mean what its source says. + Ok { unconstrained: Vec }, + /// It aborted: a write-once conflict (which is how every `assert` fails), a + /// wild dereference, or any other interpreter panic. + Rejected, +} + +impl Ran { + pub fn accepted(&self) -> bool { + matches!(self, Ran::Ok { .. }) + } + fn verb(&self) -> &'static str { + if self.accepted() { "ACCEPTED" } else { "rejected" } + } +} + +/// Compile once. Kept out of [`run`] so a compiler panic is a loud test failure +/// rather than a silent "rejected". +pub fn build(src: &str) -> Program { + compile_without_filler(&parse(src).expect("parse")) +} + +/// Run `program` on `t`. The fill blocks are irrelevant to what the program +/// asserts, so this executes the unfilled build. +pub fn run(program: &Program, t: &Trial) -> Ran { + let mut p = program.clone(); + for (name, entries) in &t.streams { + p.set_witness(*name, entries.clone()); + } + let pi = t.pi; + match std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| p.execute(pi))) { + Ok(exec) => Ran::Ok { + unconstrained: exec.unconstrained_reads, + }, + Err(_) => Ran::Rejected, + } +} + +// --------------------------------------------------------------------------- +// Layer 1: perturbation +// --------------------------------------------------------------------------- + +/// One program, one valid trial, and the pokes that must break it. +pub struct Case { + pub name: &'static str, + pub src: &'static str, + pub valid: Trial, + pub pokes: Vec, +} + +pub fn check_case(c: &Case) { + let program = build(c.src); + match run(&program, &c.valid) { + Ran::Ok { unconstrained } => assert!( + unconstrained.is_empty(), + "{}: the valid trial reads cells nothing writes: {unconstrained:?}. \ + A live value came from outside the constraint system, so the lowering \ + dropped a store the source asked for.", + c.name + ), + Ran::Rejected => panic!("{}: the valid trial must run, and did not", c.name), + } + assert!(!c.pokes.is_empty(), "{}: a case with no pokes checks nothing", c.name); + for p in &c.pokes { + assert!( + !run(&program, &c.valid.poke(p)).accepted(), + "{}: poke `{}` was ACCEPTED. The constraint that should have caught it \ + is not in the emitted bytecode.", + c.name, + p.label() + ); + } +} + +// --------------------------------------------------------------------------- +// Layer 2: equivalence +// --------------------------------------------------------------------------- + +/// Two spellings the language documents as interchangeable, and the trials that +/// have to agree. `why` names the guarantee, so a failure reads as a broken +/// promise rather than as a diff. +pub struct Pair<'a> { + pub name: &'static str, + pub why: &'static str, + pub a: &'a str, + pub b: &'a str, + pub trials: Vec, +} + +pub fn check_pair(p: &Pair<'_>) { + let (pa, pb) = (build(p.a), build(p.b)); + assert!(!p.trials.is_empty(), "{}: a pair with no trials checks nothing", p.name); + let mut agreed_reject = false; + for (i, t) in p.trials.iter().enumerate() { + let (ra, rb) = (run(&pa, t), run(&pb, t)); + assert_eq!( + ra.accepted(), + rb.accepted(), + "{}: trial {i}: spelling A {} but spelling B {}.\n {}\n\ + One of the two dropped a constraint; the more permissive side is the buggy one.", + p.name, + ra.verb(), + rb.verb(), + p.why + ); + for (which, r) in [("A", &ra), ("B", &rb)] { + if let Ran::Ok { unconstrained } = r { + assert!( + unconstrained.is_empty(), + "{}: trial {i}: spelling {which} reads cells nothing writes: {unconstrained:?}", + p.name + ); + } + } + agreed_reject |= !ra.accepted(); + } + // A pair whose every trial is accepted by both would also pass if both + // spellings dropped everything, so require at least one rejection. + assert!( + agreed_reject, + "{}: every trial was accepted by both spellings, so this pair would pass even \ + if both sides dropped the constraint. Add a trial that must be rejected.", + p.name + ); +} diff --git a/crates/lean_compiler/tests/suite/soundness/pairs.rs b/crates/lean_compiler/tests/suite/soundness/pairs.rs new file mode 100644 index 000000000..05416789d --- /dev/null +++ b/crates/lean_compiler/tests/suite/soundness/pairs.rs @@ -0,0 +1,188 @@ +//! Layer 2: equivalence. Two spellings the language documents as interchangeable +//! must accept exactly the same trials. +//! +//! This is the layer that finds dropped constraints without anyone having to +//! guess where they went. A dropped store is invisible on its own: the program +//! still runs, and its one honest witness still passes. It becomes visible the +//! moment you have a second spelling of the same intent that *kept* the store, +//! because then one side rejects a witness the other accepts, and the more +//! permissive side is the buggy one. +//! +//! Every pair here is a promise `zkDSL.md` makes. When one fails, quote the +//! promise in the bug report; the `why` field is there to be quoted. + +use super::{Pair, Trial, check_pair, g, k}; +use primitives::field::F192; + +/// One hinted pair of cells, published so the trial's public input pins them. +fn two(a: F192, b: F192) -> Trial { + Trial::new([a, b]).stream("w", vec![vec![a, b]]) +} + +/// `@inline` is documented as a pure call-site expansion: "the body is inlined at +/// each call site" with the same semantics as the call. So a function's +/// observable behaviour cannot depend on whether it carries the decorator. +#[test] +fn inline_and_plain_calls_agree() { + let body = "\ +def main(): + v = StackBuf(2) + hint_witness(v, \"w\") + assert shift(v[0]) == v[1] + p = GEN ** 0 + p[1] = v[0] + p[GEN] = v[1] + return + + +@INLINE +def shift(x): + return x * GEN +"; + check_pair(&Pair { + name: "inline_and_plain_calls_agree", + why: "zkDSL.md §`@inline`: inlining is a call-site expansion, not a change of meaning.", + a: &body.replace("@INLINE\n", "@inline\n"), + b: &body.replace("@INLINE\n", ""), + trials: vec![ + two(g(3), g(4)), // shift(g^3) = g^4 + two(g(3), g(5)), // rejected by both + two(g(0), g(1)), + two(g(7), g(7)), + ], + }); +} + +/// Write-once memory is the assertion mechanism, so `assert a == b` and two +/// stores of `a` and `b` into one heap cell are the same statement. `zkDSL.md` +/// §Memory: "a second write of the same value is a no-op, of a different value a +/// proof failure. This turns stores into equality assertions". +#[test] +fn assert_eq_and_double_heap_store_agree() { + check_pair(&Pair { + name: "assert_eq_and_double_heap_store_agree", + why: "zkDSL.md §Memory: a store into an already-written cell IS an equality assertion.", + a: "\ +def main(): + v = StackBuf(2) + hint_witness(v, \"w\") + assert v[0] == v[1] + p = GEN ** 0 + p[1] = v[0] + p[GEN] = v[1] + return +", + b: "\ +def main(): + v = StackBuf(2) + hint_witness(v, \"w\") + h = HeapBuf(1) + h[1] = v[0] + h[1] = v[1] + p = GEN ** 0 + p[1] = v[0] + p[GEN] = v[1] + return +", + trials: vec![ + two(g(3), g(3)), + two(g(3), g(4)), + two(F192::ZERO, F192::ZERO), + two(F192::ZERO, k(1)), + ], + }); +} + +/// `zkDSL.md` §field: "`/` is runtime field division … the compiler leaves the +/// quotient cell unset and emits the checked relation `quotient · b == a`". So +/// dividing and then comparing must equal comparing the product, wherever the +/// divisor is nonzero (division by zero is documented undefined, so no trial +/// takes it there). +#[test] +fn division_and_checked_product_agree() { + check_pair(&Pair { + name: "division_and_checked_product_agree", + why: "zkDSL.md §field: `a / b` emits exactly the relation `quotient · b == a`.", + a: "\ +def main(): + v = StackBuf(3) + hint_witness(v, \"w\") + q = v[1] / v[0] + assert q == v[2] + p = GEN ** 0 + p[1] = v[0] + p[GEN] = v[2] + return +", + b: "\ +def main(): + v = StackBuf(3) + hint_witness(v, \"w\") + assert v[2] * v[0] == v[1] + p = GEN ** 0 + p[1] = v[0] + p[GEN] = v[2] + return +", + trials: vec![ + three(g(3), g(8), g(5)), // g^8 / g^3 = g^5 + three(g(3), g(8), g(6)), // rejected by both + three(k(1), g(9), g(9)), + three(g(2), g(2), g(0)), + ], + }); +} + +fn three(a: F192, b: F192, c: F192) -> Trial { + Trial::new([a, c]).stream("w", vec![vec![a, b, c]]) +} + +/// `unroll` is documented as compile-time unrolling, so a loop and its expansion +/// are the same program. A structural pair: it pins the loop machinery itself +/// rather than any one assertion, which is what catches a lowering that +/// mis-addresses one iteration. +#[test] +fn unroll_and_expansion_agree() { + check_pair(&Pair { + name: "unroll_and_expansion_agree", + why: "zkDSL.md §unroll: the loop is expanded at compile time, so it IS the expansion.", + a: "\ +def main(): + v = StackBuf(1) + hint_witness(v, \"w\") + a = HeapBuf(4) + a[1] = v[0] + for i in unroll(0, 3): + a[GEN ** (i + 1)] = a[GEN ** i] * GEN + p = GEN ** 0 + p[1] = a[GEN ** 3] + p[GEN] = v[0] + return +", + b: "\ +def main(): + v = StackBuf(1) + hint_witness(v, \"w\") + a = HeapBuf(4) + a[1] = v[0] + a[GEN] = a[1] * GEN + a[GEN ** 2] = a[GEN] * GEN + a[GEN ** 3] = a[GEN ** 2] * GEN + p = GEN ** 0 + p[1] = a[GEN ** 3] + p[GEN] = v[0] + return +", + trials: vec![ + one(g(3), g(0)), // a[3] = g^0·g^3 + one(g(4), g(0)), // rejected by both + one(g(8), g(5)), + one(g(5), g(5)), + ], + }); +} + +/// A published pair whose first word is the claim and whose second is the hint. +fn one(published: F192, hint: F192) -> Trial { + Trial::new([published, hint]).stream("w", vec![vec![hint]]) +} diff --git a/crates/lean_vm/src/cpu/execute.rs b/crates/lean_vm/src/cpu/execute.rs index 4ef216614..7b3d16b3b 100644 --- a/crates/lean_vm/src/cpu/execute.rs +++ b/crates/lean_vm/src/cpu/execute.rs @@ -16,6 +16,20 @@ pub struct Execution { /// Rows per table before the fill blocks ran: the work the program itself does, as /// against the power-of-two heights that get proven. Cost measurements want this one. pub base_counts: [usize; crate::tables::N_TABLES], + /// Cells an instruction read that nothing ever wrote, so the value it read was + /// ZERO here and prover-chosen in a proof: memory is a committed array and the + /// bus only forces accesses to one address to *agree*, never that the address + /// was written. `zkDSL.md` says don't; this is what says whether the emitted + /// code did. A non-empty list means a live value came from outside the + /// constraint system, so an `assert` on it is vacuous and a published value is + /// free, which is a compiler bug and not a program one: the lowering dropped a + /// store its source asked for. + /// + /// Legitimate unconstrained cells are absent by construction, not by + /// exemption: a range-check touch's two cells are resolved to ZERO by the + /// deferred fixup before this is taken, and an arithmetic back-solve writes its + /// operand before reading it. + pub unconstrained_reads: Vec, pub(crate) trace: Trace, // rows + final access-count columns, emitted in the same walk } @@ -161,6 +175,14 @@ impl Program { // Rows per table before the fill runs, captured when the chain halts. let mut base_counts: Option<[usize; crate::tables::N_TABLES]> = None; + // Where the fill's frames begin, captured at the same moment, so + // `unconstrained_reads` can speak about the program's own cells only. The + // fill's rows exist to reach a power-of-two height and are soundness-neutral + // (doc §Filling the tables), so they read cells nobody writes as a matter of + // course; the program's own cells are all below this mark, since the + // allocator serves them and a range check's absolute write lands under + // `2^MIN_LOG_MEM`. + let mut fill_base = usize::MAX; // Per-opcode trace rows, accumulated during the walk and assembled into the // `Trace` once the run finishes (alongside the final count columns). @@ -305,6 +327,7 @@ impl Program { pack64x2.len(), ]; base_counts = Some(counts); + fill_base = (1usize << crate::cpu::MIN_LOG_MEM).max(next_free as usize); // A frame per cycle, from the same bump allocator that serves `Alloc` // but never below the memory floor: a range check's `DEREF` writes the // absolute cell its bound names, which can be any cell under @@ -885,6 +908,17 @@ impl Program { m.put(a3, F192::ZERO); } + // Cells an instruction touched that nothing ever wrote. Read off the two + // dense vectors rather than recorded in `Mem::get`, which is in the opcode + // loop: an access bumps the count, so `count != ONE` means touched, and + // `written` is already there. Taken AFTER the deferred fixup, so a + // range-check touch, whose cells are legitimately unconstrained and were + // just fixed to ZERO, does not appear. + let unconstrained_reads: Vec = (0..m.cells.len().min(fill_base)) + .filter(|&c| !m.written[c] && m.count[c] != F64::ONE) + .map(|c| c as u32) + .collect(); + // Pad memory to a power of two (the boundary tables read a dense image), // at least 2^MIN_LOG_MEM cells (doc §Memory). let mem_used = m.cells.len(); @@ -910,6 +944,7 @@ impl Program { // Taken when the chain halted, which every run does before it can leave the // loop at all. base_counts: base_counts.expect("the run halted, so its own counts were taken"), + unconstrained_reads, trace, } } diff --git a/crates/lean_vm/src/cpu/mod.rs b/crates/lean_vm/src/cpu/mod.rs index bf500f04c..bb55041c5 100644 --- a/crates/lean_vm/src/cpu/mod.rs +++ b/crates/lean_vm/src/cpu/mod.rs @@ -494,6 +494,20 @@ pub fn prove(program: &Program, public_input: [F192; 2], log_inv_rate: usize) -> // so it survives the next phase. let _phase = zk_alloc::enter_phase(); let exec = crate::stage!("Execute program", || program.execute_to_floor(public_input)); + // A live value that came from outside the constraint system means the emitted + // bytecode asserts less than its source asked for, so the proof would be about a + // weaker statement than the program text. That is a compiler bug and never a + // program one, so it is caught here, on the one path every proof takes, rather + // than left to whichever test happens to look. A hard assert, not a + // `debug_assert`: this is what makes the invariant hold in release, which is the + // only profile the VM is ever run in. + assert!( + exec.unconstrained_reads.is_empty(), + "the program read {} cell(s) nothing ever writes, first at {:?}: a constraint was \ + dropped in lowering (see `Execution::unconstrained_reads`)", + exec.unconstrained_reads.len(), + &exec.unconstrained_reads[..exec.unconstrained_reads.len().min(8)] + ); // The BLAKE2s R1CS setup (circuit construction) is a ~hundreds-of-ms cost that // depends only on the compression count (the circuit *shape*), not the witness, // but it is otherwise built synchronously inside the final reduction, adding From aa8c2e550ce7539be8187c6450a5677af9d672dd Mon Sep 17 00:00:00 2001 From: Tom Wambsgans Date: Sat, 22 Aug 2026 15:05:06 +0200 Subject: [PATCH 02/13] Follow the alias when an inline StackBuf return is used inline `take_inline_ret_cell` handed back `RetBind::Stack(base, 1)`'s raw frame cell while its `RetBind::Gaddr` sibling arm materialized. If the `@inline` body had filled that cell with a deferred copy or constant, `stack_store` emitted nothing, so no instruction ever wrote it and every expression-position consumer read a cell outside the constraint system: `expr`'s call arm (an `assert` operand), `expr_into`'s call arm (any store RHS), and `lower_match_range`'s inline-arm join, whose `copy` also reads its source raw. An unwritten cell is not zero, it is free. Memory is a committed array and the memory bus only forces accesses to one address to agree, never that the address was written, so the prover fixes it at commit time and the honest runner back-solves it to whatever the statement demands. Before this commit `assert pick(v[0]) != v[1]` with `v[0] == v[1]` proved and verified, and the same program published three different values for `pick(v[0])` under one witness. The `let` spelling of the same source rejected all of it, which is the asymmetry: `ret_binding` hands over a `Binding::Stack` whose reads go through `word_src`, and an expression use has to agree with it. Fix is that one call, in both consumers. No instance existed in the shipped guest, whose `@inline` StackBuf returns are all two cells, so nothing previously provable changes. Regression test: soundness::pairs::inline_stackbuf_return_in_expression_position. Both of the new infrastructure's relevant layers catch it, which is why the pair is the whole test: the equivalence check sees the two spellings disagree on an equal-valued witness, and the unconstrained-read check sees the raw cell on every trial including the accepting ones. Co-Authored-By: Claude Opus 5 (1M context) --- crates/lean_compiler/src/lower.rs | 12 ++++- .../tests/suite/soundness/pairs.rs | 44 +++++++++++++++++++ 2 files changed, 54 insertions(+), 2 deletions(-) diff --git a/crates/lean_compiler/src/lower.rs b/crates/lean_compiler/src/lower.rs index 3e41dfe89..e5f655a48 100644 --- a/crates/lean_compiler/src/lower.rs +++ b/crates/lean_compiler/src/lower.rs @@ -620,7 +620,10 @@ impl FnLower<'_> { } RetBind::Stack(base, size) => { assert_eq!(size, 1, "a multi-cell StackBuf return cannot cross a match_range join"); - s.copy(base, rc); + // `copy` reads its source raw, so resolve the arm's + // deferred alias first (as `take_inline_ret_cell` does). + let src = s.word_src(base); + s.copy(src, rc); } RetBind::Scalar => {} } @@ -1608,7 +1611,12 @@ impl FnLower<'_> { size, 1, "a multi-cell StackBuf return needs a `let` binding, not an expression use" ); - base + // Through `word_src`, like every other read of a stack cell: the body may + // have filled this cell with a deferred copy or constant, which emits no + // instruction, and the raw cell would then be one no instruction writes. + // The `let` consumer follows the alias by taking a `Binding::Stack` + // ([`ret_binding`]), and an expression use has to agree with it. + self.word_src(base) } _ => dst, } diff --git a/crates/lean_compiler/tests/suite/soundness/pairs.rs b/crates/lean_compiler/tests/suite/soundness/pairs.rs index 05416789d..52588e197 100644 --- a/crates/lean_compiler/tests/suite/soundness/pairs.rs +++ b/crates/lean_compiler/tests/suite/soundness/pairs.rs @@ -186,3 +186,47 @@ def main(): fn one(published: F192, hint: F192) -> Trial { Trial::new([published, hint]).stream("w", vec![vec![hint]]) } + +/// An `@inline` function returning a one-cell `StackBuf`, used in expression +/// position, must hold the value its body stored. `zkDSL.md` §`@inline` makes the +/// decorator a call-site expansion, and §StackBuf makes `s[0]` the cell the body +/// wrote, so binding the call with `let` and using it inline are the same program. +/// +/// Regression test: `take_inline_ret_cell` used to hand back the raw frame cell +/// rather than following the deferred-copy alias, so the caller read a cell no +/// instruction ever wrote. The `assert` then compared that cell instead of the +/// value, which made it vacuous, and the honest runner back-solved the cell to +/// whatever the public statement demanded. +#[test] +fn inline_stackbuf_return_in_expression_position() { + let body = "\ +def main(): + v = StackBuf(2) + hint_witness(v, \"w\") + ASSERTION + p = GEN ** 0 + p[1] = v[0] + p[GEN] = v[1] + return + + +@inline +def pick(x): + s = StackBuf(1) + s[0] = x + return s +"; + check_pair(&Pair { + name: "inline_stackbuf_return_in_expression_position", + why: "zkDSL.md §`@inline` + §StackBuf: `pick(x)[0]` is the cell the body stored `x` into, \ + whether the caller binds the call or writes it inline.", + a: &body.replace("ASSERTION", "assert pick(v[0]) != v[1]"), + b: &body.replace("ASSERTION", "r = pick(v[0])\n assert r[0] != v[1]"), + trials: vec![ + two(g(3), g(5)), // distinct: accepted by both + two(g(3), g(3)), // equal and nonzero: the inequality must fail for both + two(k(1), k(1)), + two(g(7), g(2)), + ], + }); +} From d6f2bca1a14f8dabc024def707250a65847a81a8 Mon Sep 17 00:00:00 2001 From: Tom Wambsgans Date: Sat, 22 Aug 2026 15:11:16 +0200 Subject: [PATCH 03/13] Make a StackBuf store an assertion once the cell holds a value MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `stack_store` deferred a copy-or-constant RHS as an `Alias` unconditionally and emitted nothing, while the two consumers that name a stack run by its physical cells did not follow the alias: the `BLAKE2s` output arm and `hint_witness`'s destination. So the physical cell and the alias source were joined by no constraint, and a `StackBuf` store was never the write-once equality assertion that zkDSL.md §Memory promises and §BLAKE2s recommends by name ("If `out` was already written, the statement *asserts* the digest equals it ... which is exactly what a signature verifier wants"). It did not. Pinning a hint with `s[k] = ` dropped the check, a pre-written `StackBuf` digest was written where nothing read it, and two stores of different values to one cell produced no conflict at all. The alias is sound only while nothing else gives the cell a value, so track that and stop the two from colliding, in both orders: - `emit` records the stack cells an instruction writes (`Deref`'s local cell included, since the interpreter fills whichever side of its equality is unset), and `stack_store` emits instead of aliasing when `dst` is one of them. That is the store-after-write order. - `materialize_run` gives a raw destination run real values in its own cells before a consumer names them, and marks the run written. That is the write-after-store order. Called from the `BLAKE2s` output arm, `hint_witness`, and `hint_f192_limbs`, which is the third consumer of the same shape and had the same defect. zkDSL.md said both things in different places; it now states the precondition where it describes the alias, so the two halves agree. Nothing in the shipped guest collided, so the emitted bytecode is unchanged there: the whole workspace passes, including aggregate_two_to_one and the adversarial aggregate_statement_binds / aggregate_hints_bind. Regression tests: soundness::pairs::stack_store_pins_a_hint_like_a_heap_store and ::prewritten_blake2s_out_asserts_the_digest, both verified red before this commit. The first publishes the PIN rather than the hint on purpose: publishing the hint hides a dropped pin, because the publication then forwards through the very alias that dropped it and both spellings agree by accident. Co-Authored-By: Claude Opus 5 (1M context) --- crates/lean_compiler/src/lower.rs | 68 +++++++++- .../tests/suite/soundness/cases.rs | 2 +- .../tests/suite/soundness/pairs.rs | 117 ++++++++++++++++++ crates/lean_compiler/zkDSL.md | 4 +- 4 files changed, 185 insertions(+), 6 deletions(-) diff --git a/crates/lean_compiler/src/lower.rs b/crates/lean_compiler/src/lower.rs index e5f655a48..1c40b3a18 100644 --- a/crates/lean_compiler/src/lower.rs +++ b/crates/lean_compiler/src/lower.rs @@ -4,6 +4,7 @@ use super::*; use crate::filler::FillerOp; use lean_vm::cpu::filler::Block; +use std::collections::HashSet; /// [`FnLower::specialized_body`]'s pieces: runtime param names, runtime args, /// the `Const`-substituted body, and the callee's return arity. @@ -167,6 +168,14 @@ struct FnLower<'a> { inline_stack_ret: Option>, /// Deferred stack-cell copies/zeros ([`Alias`]), forwarded at use. alias: HashMap, + /// Stack cells something already gives a real value to: an emitted + /// instruction's destination, a `BLAKE2s` output, or a hint destination. A + /// store into one of these cannot defer as an [`Alias`], because the store is + /// then the write-once equality assertion of `zkDSL.md` §Memory rather than an + /// assembly copy, and an alias would drop it. Accumulated monotonically, and + /// deliberately NOT restored across a branch: if either arm gives the cell a + /// value, a later store to it is an assertion on whichever arm ran. + phys: HashSet, /// Where the fill blocks begin in `code`, once emitted. filler_start: Option, /// Hints queued to attach to the next emitted instruction. @@ -201,10 +210,45 @@ impl FnLower<'_> { } fn emit(&mut self, op: LOp) { + // Record the stack cells this instruction gives a real value to, so + // [`Self::stack_store`] will not defer an alias onto one of them: the alias + // would win every later read and the store's write-once equality assertion, + // which is what `zkDSL.md` §Memory promises a second write is, would vanish. + // `Deref`'s local cell counts, since the interpreter fills whichever side of + // the equality it names is still unset. + match op { + LOp::Set { o, .. } => self.phys.insert(o), + LOp::Xor { c, .. } | LOp::Mul { c, .. } | LOp::Pack64x2 { c, .. } => self.phys.insert(c), + LOp::Deref { gamma, .. } => self.phys.insert(gamma), + LOp::Blake2s { c, .. } => { + self.phys.insert(c); + self.phys.insert(c + 1) + } + LOp::Jump { .. } => false, + }; let hints = std::mem::take(&mut self.pending); self.code.push(LInstr { op, hints }); } + /// Prepare a stack run that a consumer is about to name by its *physical* + /// cells: a `BLAKE2s` output, or a hint destination. Those consumers do not go + /// through [`Self::word_src`], so a cell still carrying a deferred alias would + /// have the consumer's write land where nothing reads it, and the equality + /// assertion the source wrote would be gone. Materializing the alias first puts + /// a real value in the cell, which is what turns the consumer's write back into + /// that assertion; marking the run `phys` covers the other order, where the + /// store comes after the consumer. + fn materialize_run(&mut self, base: Off, len: u32) { + for o in base..base + len { + if self.alias.contains_key(&o) { + let src = self.word_src(o); + self.alias.remove(&o); + self.copy(src, o); + } + self.phys.insert(o); + } + } + fn set(&mut self, o: Off, k: KVal) { self.emit(LOp::Set { o, k }); } @@ -342,7 +386,13 @@ impl FnLower<'_> { /// deferred as an [`Alias`] and forwarded at its uses (write-once, so the /// source cell keeps its value): the assembling `MUL`/`SET` is never emitted. fn stack_store(&mut self, dst: Off, val: &Expr) { - if let Some(a) = self.copy_alias(val) { + // Deferring is only sound while nothing else has given `dst` a value. Once + // something has, the store IS the write-once equality assertion of + // `zkDSL.md` §Memory, so it has to be emitted: an alias would silently + // redirect every later read to the source and drop the assertion. This is + // what makes `s[k] = ` pin a hint, and what makes a + // pre-written `blake2s` output assert the digest. + if let Some(a) = self.copy_alias(val).filter(|_| !self.phys.contains(&dst)) { self.alias.insert(dst, a); } else { self.alias.remove(&dst); @@ -897,7 +947,10 @@ impl FnLower<'_> { fn lower_hint_witness(&mut self, dest: &Expr, name: &str) { let name = name.to_string(); let hint = match self.cell_run(dest) { - CellRun::Stack { base, len } => RHint::WitnessStack { name, base, len }, + CellRun::Stack { base, len } => { + self.materialize_run(base, len); + RHint::WitnessStack { name, base, len } + } CellRun::Heap { ptr, lo, len } => RHint::WitnessHeap { name, ptr, lo, len }, }; self.pending.push(Hint::Resolved(hint)); @@ -2148,6 +2201,11 @@ impl FnLower<'_> { ); let value = self.expr(&args[1]); let value = self.word_src(value); + // Names the physical cells, as the two consumers above do, so the run + // has to hold real values before the hint fills it. The common + // destination is a list literal (`limbs = [0, 0, 0]`), whose every + // element goes through `stack_store` and so defers. + self.materialize_run(base, len); self.pending .push(Hint::Resolved(RHint::FieldLimbs { value, base, len })); } @@ -2194,7 +2252,10 @@ impl FnLower<'_> { let a = self.blake2s_input(&args[0]); let b = self.blake2s_input(&args[1]); let (c, heap_out) = match self.blake2s_operand(&args[2]) { - CellRun::Stack { base, .. } => (base, None), + CellRun::Stack { base, .. } => { + self.materialize_run(base, 2); + (base, None) + } CellRun::Heap { ptr, lo, .. } => (self.alloc_stack(2), Some((ptr, lo))), }; let cv = if let Some(value) = kwargs.get("cv") { @@ -2620,6 +2681,7 @@ pub(crate) fn lower_func( inline_ret: None, inline_stack_ret: None, alias: HashMap::new(), + phys: HashSet::new(), pending: Vec::new(), inline_calls: Vec::new(), queue, diff --git a/crates/lean_compiler/tests/suite/soundness/cases.rs b/crates/lean_compiler/tests/suite/soundness/cases.rs index 54f0b8da2..cb2cd04aa 100644 --- a/crates/lean_compiler/tests/suite/soundness/cases.rs +++ b/crates/lean_compiler/tests/suite/soundness/cases.rs @@ -245,7 +245,7 @@ def main(): "; /// BLAKE2s of the 64-byte block whose four canonical cells are `(5, 7, 0, 0)`. -const DIGEST_5_7: [F192; 2] = [ +pub const DIGEST_5_7: [F192; 2] = [ F192::new(0xbbc8_c175_8cb7_7642, 0xf299_5d40_1fad_f4ff, 0), F192::new(0x83ea_6ade_289a_53c8, 0x57e6_e523_12ec_734b, 0), ]; diff --git a/crates/lean_compiler/tests/suite/soundness/pairs.rs b/crates/lean_compiler/tests/suite/soundness/pairs.rs index 52588e197..bbc60405a 100644 --- a/crates/lean_compiler/tests/suite/soundness/pairs.rs +++ b/crates/lean_compiler/tests/suite/soundness/pairs.rs @@ -230,3 +230,120 @@ def pick(x): ], }); } + +/// A store into a cell something already gave a value to is the write-once +/// equality assertion of `zkDSL.md` §Memory ("a second write ... of a different +/// value a proof failure. This turns stores into equality assertions"), whether +/// the cell is a `StackBuf` cell or a `HeapBuf` cell. +/// +/// Regression test: `stack_store` deferred a copy-or-constant RHS as an alias +/// unconditionally, so a `StackBuf` store never pinned a hint. `hint_witness` +/// named the raw cells while every read forwarded past them, and the check the +/// author wrote was applied to nothing. +#[test] +fn stack_store_pins_a_hint_like_a_heap_store() { + check_pair(&Pair { + name: "stack_store_pins_a_hint_like_a_heap_store", + why: "zkDSL.md §Memory: a store into an already-written cell IS an equality assertion, \ + and §Hints: `s[k] = ` is how a program pins prover advice.", + a: "\ +def main(): + s = StackBuf(2) + hint_witness(s, \"w\") + s[0] = GEN ** 3 + p = GEN ** 0 + p[1] = s[0] + p[GEN] = s[1] + return +", + b: "\ +def main(): + s = StackBuf(2) + hint_witness(s, \"w\") + h = HeapBuf(1) + h[1] = s[0] + h[1] = GEN ** 3 + p = GEN ** 0 + p[1] = s[0] + p[GEN] = s[1] + return +", + trials: vec![ + pinned(g(3), g(9)), // the hint agrees with the pin + pinned(g(4), g(9)), // it does not: both must reject + pinned(F192::ZERO, g(1)), + pinned(g(2), g(3)), + ], + }); +} + +/// A trial for the pinning pair above: the public input carries the PIN, not the +/// hint. Publishing the hint would hide a dropped pin, since the publication then +/// forwards through the very alias that dropped it and both spellings agree by +/// accident. Publishing the pin makes a dropped pin visible as a program that +/// accepts every hint. +fn pinned(hint0: F192, hint1: F192) -> Trial { + Trial::new([g(3), hint1]).stream("w", vec![vec![hint0, hint1]]) +} + +/// `zkDSL.md` §BLAKE2s: "If `out` was already written, the statement *asserts* +/// the digest equals it, write-once turning the hash into a verification, which +/// is exactly what a signature verifier wants." That has to hold for a `StackBuf` +/// `out` as much as for a `HeapBuf` one, since the doc recommends the idiom +/// without qualifying which. +/// +/// Regression test: the `BLAKE2s` output arm named the raw run, so a `StackBuf` +/// `out` whose cells had been pre-written by copies or constants had its digest +/// written where nothing read it. The "verification" checked nothing, and the +/// prover could put any message under the hash. +#[test] +fn prewritten_blake2s_out_asserts_the_digest() { + check_pair(&Pair { + name: "prewritten_blake2s_out_asserts_the_digest", + why: "zkDSL.md §BLAKE2s: a pre-written `out` turns the hash into a verification.", + a: "\ +def main(): + v = StackBuf(2) + hint_witness(v, \"w\") + m = StackBuf(4) + m[0] = 5 + m[1] = 7 + m[2] = 0 + m[3] = 0 + d = StackBuf(2) + d[0] = v[0] + d[1] = v[1] + blake2s(m[0:2], m[2:4], d) + p = GEN ** 0 + p[1] = v[0] + p[GEN] = v[1] + return +", + b: "\ +def main(): + v = StackBuf(2) + hint_witness(v, \"w\") + m = StackBuf(4) + m[0] = 5 + m[1] = 7 + m[2] = 0 + m[3] = 0 + d = HeapBuf(2) + d[1] = v[0] + d[GEN] = v[1] + blake2s(m[0:2], m[2:4], d[0:2]) + p = GEN ** 0 + p[1] = v[0] + p[GEN] = v[1] + return +", + trials: vec![ + // The real digest of the block whose cells are (5, 7, 0, 0). + two(super::cases::DIGEST_5_7[0], super::cases::DIGEST_5_7[1]), + // Anything else must be rejected by both spellings. + two(F192::ZERO, F192::ZERO), + two(super::cases::DIGEST_5_7[0], F192::ZERO), + two(g(3), g(5)), + ], + }); +} diff --git a/crates/lean_compiler/zkDSL.md b/crates/lean_compiler/zkDSL.md index 14920204c..6a62439af 100644 --- a/crates/lean_compiler/zkDSL.md +++ b/crates/lean_compiler/zkDSL.md @@ -186,7 +186,7 @@ Three families of binding are folded and carried **virtually**, costing no instr - **g-powers and shifted pointers**: a cursor like `s = s * GEN` or a pointer view `p = buf * GEN ** k`. The offset folds into the `DEREF` address of each access; only a scalar use materializes it. - **field constants**: a value built from literals / `GEN ** k` by field `+` and `*`, e.g. a running weight `w = w * CHAIN_LENGTH` in an unrolled loop. The arithmetic that advances it is compile-time (zero instructions); each use is one `SET` of the folded constant. -- **stack-cell copies and zeros**: a store `sa[k] = other` or `sa[k] = 0` is recorded as an alias rather than emitting a `MUL`/`SET`; every read of `sa[k]` forwards to the real source (write-once keeps it valid). This is what makes assembling a `BLAKE2s` operand from scattered values free (see "BLAKE2s"). +- **stack-cell copies and zeros**: a store `sa[k] = other` or `sa[k] = 0` is recorded as an alias rather than emitting a `MUL`/`SET`; every read of `sa[k]` forwards to the real source (write-once keeps it valid). This is what makes assembling a `BLAKE2s` operand from scattered values free (see "BLAKE2s"). It applies only while **nothing else gives the cell a value**: once an instruction, a `BLAKE2s` output or a hint destination has written `sa[k]`, a store into it is the write-once equality *assertion* below rather than an assembly copy, so it is emitted. That is what makes `s[k] = ` pin a hint and a pre-written `blake2s` output verify a digest, and it holds in either order (the assembling store may come first, in which case the consumer materializes it). ## Debugging @@ -422,7 +422,7 @@ The metadata is packed as `counter:u64 | f0:u32 | f1:u32`, little-endian, and is Operands are size-2 `StackBuf`s or 2-cell slices: - **stack operands** are read/written in place, at zero copies; a self-hash `blake2s(h, h, out)` aliases one 2-cell pair into both inputs; -- the instruction addresses its **four canonical 128-bit message chunks independently** (each is a full F192 memory cell constrained at this use to the BLAKE2s subspace `c2 = 0`), so when a 256-bit operand is *assembled* from values that live in different places (the idiom `p = StackBuf(2); p[0] = t0; p[1] = t1; blake2s(p, …)`), the copies vanish: a stack store of a plain copy or a zero is forwarded to its source (see "Variables"), and `BLAKE2s` reads each chunk where it already is; +- the instruction addresses its **four canonical 128-bit message chunks independently** (each is a full F192 memory cell constrained at this use to the BLAKE2s subspace `c2 = 0`), so when a 256-bit operand is *assembled* from values that live in different places (the idiom `p = StackBuf(2); p[0] = t0; p[1] = t1; blake2s(p, …)`), the copies vanish: a stack store of a plain copy or a zero is forwarded to its source (see "Variables"), and `BLAKE2s` reads each chunk where it already is. The saving is for *assembly* only: if `out`'s cells were assembled this way, the digest write would have nowhere to land, so the compiler materializes them first and the store below stays an assertion; - the chaining value has only one opcode offset and therefore must be consecutive. If a 2-cell `cv` was assembled from non-adjacent copied cells, the compiler materializes those two cells into a fresh consecutive run; - **heap slices** are still bridged through the stack for the *input pull* (the operand's words come from the heap): +1 `DEREF` per heap cell, and the output, if a heap slice, is stored after: write-once memory fills whichever side is unset. From 88cfbca67f2bb0c233fa2ec85895fda17a11387a Mon Sep 17 00:00:00 2001 From: Tom Wambsgans Date: Sat, 22 Aug 2026 15:28:25 +0200 Subject: [PATCH 04/13] A store into a cell that already has a value is an assertion MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two defects with one root, both in the deferred-alias path. A second store into a cell whose value was itself deferred just replaced the first alias, so the two values never met: `s[0] = a; s[0] = b` emitted a single `SET` of `b` and asserted nothing, where the same pair of stores into a HeapBuf cell is the write-once equality assertion zkDSL.md §Memory promises. The previous commit's message listed this case while describing the bug, but its fix only covered a store into a PHYSICALLY written cell; a store into a deferred one stayed silent. This is that case. `scoped` then inherited it. A branch storing into a cell that carried a pre-branch alias took the replace path, so the branch's value lived only in the branch-local alias; `scoped` materialized it at the join and immediately restored the pre-branch alias over it, leaving the write orphaned and every post-join read forwarding to the pre-branch source. The published value was the pre-branch one whichever arm ran. The rule that fixes both: a store into a cell that already has a value, deferred or physical, is the assertion, so materialize what the cell already stood for and then emit. Assembly is untouched, since assembling a BLAKE2s operand or a list literal stores each cell once. `scoped` needs no change of its own: the in-branch store now asserts against the pre-branch value on both arms symmetrically, which is what makes restoring the pre-branch alias correct rather than lossy, since the assertion is exactly what says the two agree. Also sort `branch_outputs` before emitting its copies. It was iterating a HashMap, so two builds of one source could emit them in different orders and produce different bytecode. The bytecode digest leads the Fiat--Shamir transcript, so that is a verifier that disagrees with itself across processes. Guest unaffected: bytecode byte-identical (DBG_PROF_DUMP diff clean) and the recursion benchmark unchanged at 321,127 instructions / 796,006 cycles. Regression tests: soundness::pairs::two_stack_stores_to_one_cell_assert_equality and ::store_inside_a_branch_asserts_against_the_pre_branch_value, both verified red before this commit. Co-Authored-By: Claude Opus 5 (1M context) --- crates/lean_compiler/src/lower.rs | 24 ++++- .../tests/suite/soundness/pairs.rs | 102 ++++++++++++++++++ 2 files changed, 122 insertions(+), 4 deletions(-) diff --git a/crates/lean_compiler/src/lower.rs b/crates/lean_compiler/src/lower.rs index 1c40b3a18..757caa89f 100644 --- a/crates/lean_compiler/src/lower.rs +++ b/crates/lean_compiler/src/lower.rs @@ -392,12 +392,24 @@ impl FnLower<'_> { // redirect every later read to the source and drop the assertion. This is // what makes `s[k] = ` pin a hint, and what makes a // pre-written `blake2s` output assert the digest. - if let Some(a) = self.copy_alias(val).filter(|_| !self.phys.contains(&dst)) { + let aliased = self.alias.contains_key(&dst); + if !aliased + && !self.phys.contains(&dst) + && let Some(a) = self.copy_alias(val) + { self.alias.insert(dst, a); - } else { + return; + } + if aliased { + // Give the cell the value it already stood for, so the store below is a + // second write of that cell and therefore the assertion. Without this the + // second alias would simply replace the first and the two values would + // never meet. + let src = self.word_src(dst); self.alias.remove(&dst); - self.expr_into(val, dst); + self.copy(src, dst); } + self.expr_into(val, dst); } /// Terminate `main`: jump to the halt sentinel `g^{B-1}` with `fp = g^0`. @@ -554,11 +566,15 @@ impl FnLower<'_> { f(self); // A deferred store into a buffer declared outside the branch must be // materialized on that path before the branch-local aliases are dropped. - let branch_outputs: Vec = self + let mut branch_outputs: Vec = self .alias .iter() .filter_map(|(&dst, alias)| (dst < branch_start && saved_aliases.get(&dst) != Some(alias)).then_some(dst)) .collect(); + // Sorted, because the emitted copies must not depend on `HashMap` iteration + // order: the bytecode digest leads the Fiat--Shamir transcript, so two builds + // of one source have to be the same program. + branch_outputs.sort_unstable(); for dst in branch_outputs { let src = self.word_src(dst); self.alias.remove(&dst); diff --git a/crates/lean_compiler/tests/suite/soundness/pairs.rs b/crates/lean_compiler/tests/suite/soundness/pairs.rs index bbc60405a..618c768be 100644 --- a/crates/lean_compiler/tests/suite/soundness/pairs.rs +++ b/crates/lean_compiler/tests/suite/soundness/pairs.rs @@ -347,3 +347,105 @@ def main(): ], }); } + +/// Two stores of different values into one cell is the write-once equality +/// assertion of `zkDSL.md` §Memory, on a `StackBuf` cell as much as on a `HeapBuf` +/// cell. The doc draws no distinction, and the whole "stores are assertions" +/// promise rests on there being none. +#[test] +fn two_stack_stores_to_one_cell_assert_equality() { + check_pair(&Pair { + name: "two_stack_stores_to_one_cell_assert_equality", + why: "zkDSL.md §Memory: a second write of a different value is a proof failure.", + a: "\ +def main(): + v = StackBuf(2) + hint_witness(v, \"w\") + s = StackBuf(1) + s[0] = v[0] + s[0] = v[1] + p = GEN ** 0 + p[1] = v[0] + p[GEN] = v[1] + return +", + b: "\ +def main(): + v = StackBuf(2) + hint_witness(v, \"w\") + h = HeapBuf(1) + h[1] = v[0] + h[1] = v[1] + p = GEN ** 0 + p[1] = v[0] + p[GEN] = v[1] + return +", + trials: vec![two(g(3), g(3)), two(g(3), g(4)), two(g(0), g(0)), two(g(5), g(9))], + }); +} + +/// A store made inside a runtime branch into a cell that already carried a value +/// from before the branch is the same assertion whether the cell is a `StackBuf` +/// cell or a `HeapBuf` cell. `zkDSL.md` §`if`: "branches communicate through +/// write-once cells: only one branch executes, so both may write the *same* cell", +/// and §Memory makes a second write of a different value a failure. +/// +/// Regression test: `scoped` materialized the branch's value into the cell and +/// then restored the pre-branch alias over it, so post-join reads forwarded to the +/// pre-branch source on every path and the materialized write was orphaned. The +/// published value was the pre-branch one whichever arm ran. +#[test] +fn store_inside_a_branch_asserts_against_the_pre_branch_value() { + check_pair(&Pair { + name: "store_inside_a_branch_asserts_against_the_pre_branch_value", + why: "zkDSL.md §`if` + §Memory: both arms may write one cell, and a second write \ + of a different value is a proof failure.", + a: "\ +def main(): + v = StackBuf(3) + hint_witness(v, \"w\") + s = StackBuf(1) + s[0] = v[0] + if v[1] == v[2]: + s[0] = v[1] + else: + s[0] = v[2] + p = GEN ** 0 + p[1] = s[0] + p[GEN] = v[0] + return +", + b: "\ +def main(): + v = StackBuf(3) + hint_witness(v, \"w\") + h = HeapBuf(1) + h[1] = v[0] + if v[1] == v[2]: + h[1] = v[1] + else: + h[1] = v[2] + p = GEN ** 0 + p[1] = h[1] + p[GEN] = v[0] + return +", + trials: vec![ + // else arm, and v[0] != v[2]: the assertion must fail for both. + branch3(g(1), g(2), g(3)), + // else arm, and v[0] == v[2]: accepted by both. + branch3(g(1), g(2), g(1)), + // then arm, and v[0] == v[1]: accepted by both. + branch3(g(1), g(1), g(1)), + // then arm, and v[0] != v[1] (v[1] == v[2] picks it): must fail. + branch3(g(1), g(4), g(4)), + ], + }); +} + +/// A trial for the branch pair: publishes `s[0]` and `v[0]`, which the assertion +/// makes equal on every accepting path. +fn branch3(a: F192, b: F192, c: F192) -> Trial { + Trial::new([a, a]).stream("w", vec![vec![a, b, c]]) +} From faa9f6eb625bda9aa6d95436647df3237ce9a927 Mon Sep 17 00:00:00 2001 From: Tom Wambsgans Date: Sat, 22 Aug 2026 15:32:21 +0200 Subject: [PATCH 05/13] Check callee return arity on the fused match_range path `lower_dispatched_call`'s join emits one `DEREF` per bound name without ever comparing that count to any callee's declared arity, while the non-fused path enforces exactly that (`call_into`). So one source was rejected by one lowering of `match_range` and silently miscompiled by the other. A name past a callee's arity reads a callee-frame offset nothing on the taken path writes, and because the shared frame is sized to the LARGEST callee the offset exists inside the allocation: the surplus name binds a prover-chosen word. Memory is a committed array and the memory bus only forces accesses to one address to agree, never that the address was written. Broader than mixed-arity arms, which is how it was first described: a SINGLE over-bound callee fuses with no diagnostic too, and that is the shape all three guest sites use, so the guest was correct only because its author counted right, with nothing checking. The check has to look the callee up in the queue as well as in `defs`, which is the reason a `defs`-only version of it passes on everything: `specialize` registers a `Const` specialization in the queue under a mangled name and never puts it in `defs`, and a dispatched `match_range` names specializations exclusively. `return_shapes_of` covers both. Regression tests: soundness::cases::dispatched_call_rejects_a_mixed_arity_arm and ::dispatched_call_rejects_an_over_bound_callee. Co-Authored-By: Claude Opus 5 (1M context) --- crates/lean_compiler/src/lower.rs | 37 +++++++++++++ .../tests/suite/soundness/cases.rs | 54 +++++++++++++++++++ 2 files changed, 91 insertions(+) diff --git a/crates/lean_compiler/src/lower.rs b/crates/lean_compiler/src/lower.rs index 757caa89f..6c1e7d44e 100644 --- a/crates/lean_compiler/src/lower.rs +++ b/crates/lean_compiler/src/lower.rs @@ -709,6 +709,29 @@ impl FnLower<'_> { /// per-arm frame setup, call, or return jump. fn lower_dispatched_call(&mut self, names: &[String], x: &Expr, callees: &[String], rt_args: &[Expr]) { let n_args = rt_args.len() as u32; + // The join below reads one return cell per bound name, so every callee has + // to declare exactly that many. Unchecked, a name past a callee's arity + // `DEREF`s a frame offset nothing on that path writes, and since the shared + // frame is sized to the LARGEST callee the offset exists: the surplus name + // binds a prover-chosen word. The non-fused path enforces this + // ([`Self::call_into`]), so leaving it out here means one source is rejected + // by one lowering of `match_range` and silently miscompiled by the other. + for callee in callees { + let Some(shapes) = self.return_shapes_of(callee) else { + continue; + }; + assert_eq!( + shapes.len(), + names.len(), + "`{callee}` returns {} values, dispatched call binds {}", + shapes.len(), + names.len() + ); + assert!( + shapes.iter().all(|s| *s == ReturnShape::Scalar), + "`{callee}`: a multi-cell StackBuf return cannot cross a dispatched join" + ); + } let rcells: Vec = names.iter().map(|_| self.fresh()).collect(); // Shared callee frame: args, retfp, and retpc = the join (so the callee @@ -1898,6 +1921,20 @@ impl FnLower<'_> { /// arguments (literals, `GEN ** k`, or literal-bound names) substitute into /// a copy of the callee, queued once per distinct constant tuple and named /// `callee__L5_G3`-style, and only the runtime arguments remain. + /// A callee's declared return shapes, looked up wherever it lives: an + /// ordinary definition sits in `defs`, while a `Const` specialization is + /// registered by [`Self::specialize`] in the queue under its mangled name and + /// never reaches `defs`. A dispatched `match_range` names specializations, so a + /// check that consults only `defs` silently passes on every one of them. + fn return_shapes_of(&self, callee: &str) -> Option> { + self.defs.get(callee).map(|d| d.return_shapes.clone()).or_else(|| { + self.queue + .iter() + .find(|f| f.name == callee) + .map(|f| f.return_shapes.clone()) + }) + } + fn specialize(&mut self, callee: &str, args: &[Expr]) -> (String, Vec) { let defs: &HashMap = self.defs; let Some(def) = defs.get(callee) else { diff --git a/crates/lean_compiler/tests/suite/soundness/cases.rs b/crates/lean_compiler/tests/suite/soundness/cases.rs index cb2cd04aa..bd9473c54 100644 --- a/crates/lean_compiler/tests/suite/soundness/cases.rs +++ b/crates/lean_compiler/tests/suite/soundness/cases.rs @@ -270,3 +270,57 @@ def main(): p.set_witness("msg", vec![vec![k(5), k(7), F192::ZERO, F192::ZERO]]); p.execute([F192::ZERO, F192::ZERO]); } + +/// The fused `match_range` path must reject a call that binds more names than +/// the callee returns, exactly as the non-fused path does. Before this check the +/// surplus name `DEREF`ed a callee-frame offset nothing on the taken path wrote, +/// and since the shared frame is sized to the largest callee that offset exists, +/// so the name bound a prover-chosen word. +/// +/// Fusion needs every arm to be a call to the same function with identical +/// runtime arguments, so the two programs below are the fused shape: one over +/// mixed-arity callees, one over a single over-bound callee. +#[test] +#[should_panic(expected = "dispatched call binds")] +fn dispatched_call_rejects_a_mixed_arity_arm() { + super::build( + "\ +def main(): + x = GEN ** 2 + a, b, c = match_range(log(x), range(0, 2), lambda i: three(x, i), range(2, 4), lambda i: one(x, i)) + p = GEN ** 0 + p[1] = b + p[GEN] = c + return + + +def three(v, k: Const): + q = v * GEN ** k + return q, q * q, q * q * q + + +def one(v, k: Const): + return v * GEN ** k +", + ); +} + +#[test] +#[should_panic(expected = "dispatched call binds")] +fn dispatched_call_rejects_an_over_bound_callee() { + super::build( + "\ +def main(): + x = GEN ** 1 + a, b = match_range(log(x), range(0, 4), lambda i: one(x, i)) + p = GEN ** 0 + p[1] = a + p[GEN] = b + return + + +def one(v, k: Const): + return v * GEN ** k +", + ); +} From ebbbd2f79c8eda61864597bd6dcf00cfffeb5b36 Mon Sep 17 00:00:00 2001 From: Tom Wambsgans Date: Sat, 22 Aug 2026 15:34:47 +0200 Subject: [PATCH 06/13] Reject a local or parameter that shadows a constant array MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit zkDSL.md §Global constants reserves a top-level constant's name: "do not reuse it as a parameter or local name". A SCALAR constant enforced that by construction, since the parser substitutes its value textually and the shadowing binding becomes a literal, which fails loudly. A constant ARRAY is carried to lowering instead, where `const_array_elem` resolves `NAME[i]` against `const_arrays` without consulting the scope and `expr` folds constants before its index arm could see the local. So the collision was silent, and the local's compile-time-indexed reads were folded to baked literals. That is the catastrophic direction for a hint. A `hint_witness` into a shadowed buffer had its range check evaluated against the constant: `Q = [8, 32]` with a local `Q = StackBuf(2)` compiled `assert log(Q[0]) < 8` into the 3-cycle gadget applied to the literal `g^3`, which passes, while the actual witness `g^40` was never bounded and its cells never read. Checked at the three places a name is bound: `rebind` for locals and assignments, the inline-callee parameter binds, and the function-entry parameter binds. Rejecting is right rather than letting the local win, since picking a winner silently changes the meaning of existing sources and the doc already says the name is not available. The guest defines many constant arrays (the LIG_* tables) and collides with none of them. Regression tests: soundness::cases::a_local_may_not_shadow_a_constant_array and ::a_parameter_may_not_shadow_a_constant_array. Co-Authored-By: Claude Opus 5 (1M context) --- crates/lean_compiler/src/lower.rs | 27 ++++++++++ .../tests/suite/soundness/cases.rs | 53 +++++++++++++++++++ 2 files changed, 80 insertions(+) diff --git a/crates/lean_compiler/src/lower.rs b/crates/lean_compiler/src/lower.rs index 6c1e7d44e..8af5f9237 100644 --- a/crates/lean_compiler/src/lower.rs +++ b/crates/lean_compiler/src/lower.rs @@ -274,12 +274,32 @@ impl FnLower<'_> { self.set_const(o, F192::ZERO); } + /// A top-level constant name is reserved (`zkDSL.md` §Global constants: "do not + /// reuse it as a parameter or local name"). A scalar constant enforces that by + /// construction, since the parser substitutes its value textually and a + /// shadowing binding becomes a literal, which fails loudly. A constant ARRAY is + /// carried to lowering instead, and [`Self::const_array_elem`] resolves + /// `NAME[i]` against it without consulting the scope, while `expr` folds + /// constants before its index arm could see the local. So a colliding local + /// silently has its compile-time-indexed reads folded to baked literals, + /// including reads of a `hint_witness` destination, whose asserts and range + /// checks then run on the constant instead of on the witness. Reject the + /// collision rather than pick a winner. + fn check_not_reserved(&self, name: &str) { + assert!( + !self.const_arrays.contains_key(name), + "`{name}` is a top-level constant array, so the name is reserved: rename the local \ + or parameter (zkDSL.md §Global constants)" + ); + } + /// Bind `name` to `b`, dropping whatever the other three maps held for it: /// they are consulted independently, so a stale binding of another kind /// would shadow this one. `consts` is deliberately NOT touched, since a /// name can keep its compile-time index role across such a rebind; callers /// that must drop it do so themselves. fn rebind(&mut self, name: &str, b: Binding) { + self.check_not_reserved(name); self.scope.vars.remove(name); self.scope.stacks.remove(name); self.scope.gaddrs.remove(name); @@ -1887,6 +1907,7 @@ impl FnLower<'_> { std::mem::take(&mut self.scope.fconsts), ); for (p, b) in binds { + self.check_not_reserved(&p); match b { Bind::Stack(base, size) => { self.scope.stacks.insert(p, (base, size)); @@ -2710,6 +2731,12 @@ pub(crate) fn lower_func( ) -> Lowered { let mut vars = HashMap::new(); for (i, p) in f.params.iter().enumerate() { + assert!( + !const_arrays.contains_key(p), + "`{}`: parameter `{p}` collides with a top-level constant array, whose name is \ + reserved (zkDSL.md §Global constants)", + f.name + ); vars.insert(p.clone(), 2 + i as u32); } // Reserve [0,1] retpc/retfp, params, then the flattened return area, then diff --git a/crates/lean_compiler/tests/suite/soundness/cases.rs b/crates/lean_compiler/tests/suite/soundness/cases.rs index bd9473c54..ac88f4e92 100644 --- a/crates/lean_compiler/tests/suite/soundness/cases.rs +++ b/crates/lean_compiler/tests/suite/soundness/cases.rs @@ -324,3 +324,56 @@ def one(v, k: Const): ", ); } + +/// A local whose name collides with a top-level constant array must be rejected. +/// `zkDSL.md` §Global constants reserves the name; a scalar constant enforces that +/// by construction (the parser substitutes its value, so the shadowing binding +/// becomes a literal and fails loudly), but a constant array was carried to +/// lowering, where `const_array_elem` resolved `NAME[i]` against it without +/// consulting the scope and `expr` folded it before the local could be seen. +/// +/// The consequence was the catastrophic direction for a hint: the range check +/// below ran against the baked constant `g^3` and passed, while the actual witness +/// `g^40` was never bounded and never read. +#[test] +#[should_panic(expected = "reserved")] +fn a_local_may_not_shadow_a_constant_array() { + super::build( + "\ +Q = [8, 32] + + +def main(): + Q = StackBuf(2) + hint_witness(Q, \"w\") + assert log(Q[0]) < 8 + p = GEN ** 0 + p[1] = Q[0] + p[GEN] = Q[1] + return +", + ); +} + +/// Same rule for a parameter, which is the other half of what the doc reserves. +#[test] +#[should_panic(expected = "reserved")] +fn a_parameter_may_not_shadow_a_constant_array() { + super::build( + "\ +Q = [8, 32] + + +def main(): + r = pick(GEN ** 2) + p = GEN ** 0 + p[1] = r + p[GEN] = r + return + + +def pick(Q): + return Q * GEN +", + ); +} From 93e1a91ab5765231246671fb2d4a0b05c13c072e Mon Sep 17 00:00:00 2001 From: Tom Wambsgans Date: Sat, 22 Aug 2026 15:53:52 +0200 Subject: [PATCH 07/13] Check the committed size against one declared window, in all three verifiers A proof announces table heights, a memory size and a rate. Each was capped on its own, but what the PCS has to be configured for is the stacked size 2^mu they IMPLY, and the caps do not bound it: maxing all of them gives mu = 41, and the memory cap alone gives 35 while the bytecode cap alone gives 33. So the documented instance caps describe shapes the WHIR ladder has no config for at all, and nothing checked it: the missing config surfaced as a panic inside the opening. `pcs::MAX_MU` is the single knob, and everything else derives from it. `cpu::read_public` checks `MIN_MU..=MAX_MU` before any reduction runs against the layout, and `rec_aggregation::MU_MAX` IS `pcs::MAX_MU`, so the recursion guest's compiled opening arms follow the knob through its existing placeholder (`LIG_N_LOG_SIZES`) with nothing to keep in step by hand. Verified by moving it: at 29 the guest recompiles to 364,481 instructions from 321,127, the four extra arms, and the whole suite passes. `python-verifier` is standalone and dependency-free, so it cannot read the Rust constant and keeps a literal. `whir_query_table.rs` already dumped its two ends without comparing them; it now asserts them against the Rust constants and its failure message names the edit. MAX_MU = 28 is a policy cap, not the ladder's ceiling, which is higher and rate-dependent (36 at log_inv_rate 1, 32 at 4). A test keeps the window inside what the ladder supports at every rate, which is what lets a plain range check stand in for re-deriving it. Note that 28 leaves one bit over the non-recursive XMSS path, which commits 2^26.195 at 900 signatures and scales linearly with the signature count: doubling that workload needs the knob raised, and raising it costs ~4 guest opening arms of ~12k instructions per size. Co-Authored-By: Claude Opus 5 (1M context) --- AGENTS.md | 10 --------- crates/lean_vm/src/cpu/mod.rs | 5 +++++ crates/lean_vm/src/pcs.rs | 22 +++++++++++++++++++ .../tests/verifiers/whir_query_table.rs | 11 ++++++++++ crates/rec_aggregation/src/aggregation.rs | 4 +++- python-verifier/verifier.py | 8 ++++++- 6 files changed, 48 insertions(+), 12 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index 21256aee9..ba2288189 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -38,16 +38,6 @@ Dependency order, leaves first: - always run in `--release` mode any test or benchmark touching the VM (the zkDSL compiler stack-overflows in `debug` mode) - **One test binary per crate, not one per file:** new `lean_compiler` integration tests go in `tests/suite/main.rs`, one linked executable instead of seventeen. Exception: a test opening an arena phase (`lean_vm::init_prover`) needs its own binary. Phases are process-global, so two in one process reclaim each other's `ArenaVec`s and the symptom is a proof that stops verifying, never a crash (`rec_aggregation/tests/arena_prove.rs`). -## Compiler soundness - -A dropped constraint is the compiler's worst failure mode and its quietest: the happy path passes, no diagnostic is emitted, and the only symptom is a proof of something weaker than the source says. Positive tests cannot catch it, so `lean_compiler/tests/suite/soundness/` attacks the *absence* of a constraint from three sides. Every compiler fix in this area lands with a test in whichever layer catches it. - -- **Perturbation** (`soundness/cases.rs`): one valid trial per program, then a table of single-cell pokes at the public input or a witness stream, each of which must make the run fail. A poke that is accepted names the missing constraint. Same shape as `../leanVM`'s own `test_soundness_suite`. -- **Equivalence** (`soundness/pairs.rs`): two spellings `zkDSL.md` documents as interchangeable must accept exactly the same trials. This is the layer that finds dropped stores, because a dropped store is invisible alone and obvious against a spelling that kept it: the more permissive side is the buggy one. Each `Pair` carries the promise it tests in its `why` field. -- **Unconstrained reads** (`Execution::unconstrained_reads`, asserted in `cpu::prove`): a cell an instruction read that nothing ever wrote. Such a value is ZERO under the interpreter and prover-chosen in a proof, since memory is a committed array and the bus only forces accesses to one address to *agree*, never that the address was written. Scoped to the program's own cells: the fill blocks read cells nobody writes as a matter of course, and are soundness-neutral for it. - -The three are complementary. Layer 3 sees a dropped store whose cell is then *read*; layer 2 sees one whose cell is then *ignored*, the value coming from the alias while the physical write is orphaned, which layer 3 cannot see because nothing reads the orphan. Layer 1 needs a program whose assertion a poke can violate, and in exchange needs no second spelling. - An x86-only arm never compiles on an Apple dev machine, so a typo in one ships. Type-check the other target before pushing anything `cfg`-gated: ```bash diff --git a/crates/lean_vm/src/cpu/mod.rs b/crates/lean_vm/src/cpu/mod.rs index bb55041c5..9dccadcbd 100644 --- a/crates/lean_vm/src/cpu/mod.rs +++ b/crates/lean_vm/src/cpu/mod.rs @@ -154,6 +154,11 @@ fn read_public(vs: &mut VerifierState, prog: &Program, public_input: &[F192; 2]) return Err(Error::PublicInput); } let l = layout(&prog.prog, log_mem, taus, *public_input); + // The caps bound each announced log on its own; what the PCS is configured for + // is the stacked size they imply, which they do not bound. + if !(pcs::MIN_MU..=pcs::MAX_MU).contains(&l.shape.mu) { + return Err(Error::PublicInput); + } Ok((l, log_inv_rate)) } diff --git a/crates/lean_vm/src/pcs.rs b/crates/lean_vm/src/pcs.rs index 73f1c310a..e9f6d16c1 100644 --- a/crates/lean_vm/src/pcs.rs +++ b/crates/lean_vm/src/pcs.rs @@ -48,6 +48,12 @@ const _: () = assert!(::pcs::whir::SECURITY_BITS == crate::SECURITY_BITS as usiz /// one-level margin. `witness::placements_of` zero-pads smaller stacks up to /// this floor (256 KB of F64, negligible; real workloads are far above it). pub const MIN_MU: usize = 15; +/// Largest committed size, and the one knob that sets it. A policy cap rather than +/// the ladder's limit (which is higher, and rate-dependent): every verifier admits +/// `MIN_MU..=MAX_MU`, the recursion guest compiles one opening arm per size in it, +/// and `rec_aggregation::MU_MAX` is this constant. Raising it costs guest bytecode, +/// ~4 arms per size; the test below keeps it inside what the ladder supports. +pub const MAX_MU: usize = 28; /// The WHIR (prover, verifier) config pair for a `2^μ`-word witness, /// derived from the security analysis and memoized per `(μ, log_inv_rate)`. @@ -170,3 +176,19 @@ pub fn verify( .then_some(()) .ok_or(Error::Whir) } + +#[cfg(test)] +mod tests { + use super::*; + + /// What lets all three verifiers check a plain range instead of re-deriving + /// the ladder: every size in the window is configurable at every rate. + #[test] + fn the_window_is_configurable() { + for rate in ::pcs::whir::MIN_LOG_INV_RATE..=::pcs::whir::MAX_LOG_INV_RATE { + for mu in MIN_MU..=MAX_MU { + assert!(configs_for_rate(mu, rate).is_ok(), "mu={mu} rate={rate}"); + } + } + } +} diff --git a/crates/lean_vm/tests/verifiers/whir_query_table.rs b/crates/lean_vm/tests/verifiers/whir_query_table.rs index 816e9d4d3..3de64f68f 100644 --- a/crates/lean_vm/tests/verifiers/whir_query_table.rs +++ b/crates/lean_vm/tests/verifiers/whir_query_table.rs @@ -38,6 +38,17 @@ fn whir_query_table_matches_rust() { let mut range = lines.next().expect("range line").split_whitespace(); let mut next_bound = || range.next().expect("a bound").parse::().expect("a bound"); let (min_log, max_log) = (next_bound(), next_bound()); + // Every verifier admits the same committed-size window, and `pcs::MAX_MU` is the + // one knob that sets it. `python-verifier` is standalone and dependency-free, so + // it cannot read the Rust constant and keeps a literal; this is what stops the + // two drifting, and names the edit when the knob moves. + assert_eq!( + (min_log, max_log), + (lean_vm::pcs::MIN_MU, lean_vm::pcs::MAX_MU), + "set MIN_STACKED_LOG / MAX_STACKED_LOG in python-verifier/verifier.py to {} / {}", + lean_vm::pcs::MIN_MU, + lean_vm::pcs::MAX_MU + ); let mut checked = 0; for line in lines { diff --git a/crates/rec_aggregation/src/aggregation.rs b/crates/rec_aggregation/src/aggregation.rs index 0e7bca3ce..6dd4897d1 100644 --- a/crates/rec_aggregation/src/aggregation.rs +++ b/crates/rec_aggregation/src/aggregation.rs @@ -1370,7 +1370,9 @@ fn gen_verify( /// candidate `mu` in `MU_MIN..=MU_MAX` (mirrored by the soundness test's /// residual-log cap). const MU_MIN: usize = 22; -const MU_MAX: usize = 28; +const MU_MAX: usize = lean_vm::pcs::MAX_MU; + +const _: () = assert!(MU_MIN >= lean_vm::pcs::MIN_MU); /// The guest's baked buffer caps, which `placeholder_map` compiles in and /// `gen_verify` admits against: one definition, so a hinted shape can never diff --git a/python-verifier/verifier.py b/python-verifier/verifier.py index 850eee3ae..b919c5816 100644 --- a/python-verifier/verifier.py +++ b/python-verifier/verifier.py @@ -1266,7 +1266,7 @@ def virtual_slot(column: int) -> int | None: QUERY_GRINDING_BITS = 17 MIN_STACKED_LOG = 15 -MAX_STACKED_LOG = 32 +MAX_STACKED_LOG = 28 WHIR_QUERIES = (((223,56,36), (223,56,37), (223,56,37), (224,56,37,28), (224,56,37,28), (224,56,38,28), (224,56,38,28,22), (225,56,38,28,23), (225,56,38,28,23), (225,56,38,28,23,19), (226,56,38,28,23,19), (226,56,38,28,23,19), (227,56,38,28,23,19,16), (228,56,38,28,23,19,16), (228,56,38,28,23,19,16), (229,57,38,28,23,19,17,14), (230,57,38,29,23,19,17,14), (232,57,38,29,23,19,17,15)), ((112,45,31), (112,45,32), (112,45,32), (112,45,32,25), (112,45,32,25), (112,45,32,25), (112,45,32,25,20), (112,45,32,25,21), (112,45,32,25,21), (113,45,32,25,21,17), (113,45,32,25,21,18), (113,45,32,25,21,18), (113,45,32,25,21,18,15), (113,45,32,25,21,18,15), (114,45,32,25,21,18,15), (114,45,33,25,21,18,15,14), (114,45,33,25,21,18,16,14), (115,46,33,25,21,18,16,14)), ((75,37,28), (75,37,28), (75,38,28), (75,38,28,22), (75,38,28,23), (75,38,28,23), (75,38,28,23,19), (75,38,28,23,19), (75,38,28,23,19), (75,38,28,23,19,16), (75,38,28,23,19,16), (75,38,28,23,19,16), (75,38,28,23,19,17,14), (76,38,29,23,19,17,14), (76,38,29,23,19,17,15), (76,38,29,23,19,17,15,13), (76,38,29,23,19,17,15,13), (77,38,29,23,19,17,15,13)), ((56,32,25), (56,32,25), (56,32,25), (56,32,25,20), (56,32,25,21), (56,32,25,21), (56,32,25,21,17), (56,32,25,21,18), (56,32,25,21,18), (57,32,25,21,18,15), (57,32,25,21,18,15), (57,32,25,21,18,15), (57,33,25,21,18,15,14), (57,33,25,21,18,16,14), (57,33,25,21,18,16,14), (57,33,26,21,18,16,14,12), (57,33,26,21,18,16,14,13), (58,33,26,21,18,16,14,13))) # fmt: skip @@ -1833,6 +1833,12 @@ def verify_execution(bytecode: Sequence[K], public_input: Digest, proof: Proof) log_inverse_rate = int(announced[-1].c0) require(1 <= log_inverse_rate <= 4, "invalid PCS inverse rate") layout = build_layout(bytecode, log_memory, table_logs) + # The announced sizes bound themselves, but what the PCS has to be configured + # for is the stacked size they IMPLY, and the instance caps admit a `stack_log` + # far past the largest the WHIR ladder is feasible for. Checked here, before any + # reduction runs against the layout, and against the same window the Rust + # verifier's `pcs::{MIN_MU, MAX_MU}` and the recursion guest declare. + require(MIN_STACKED_LOG <= layout.stack_log <= MAX_STACKED_LOG, "committed size outside the PCS window") # 2] WHIR commitment: one Merkle root (No OOD, our PCS is only List-binding). root = Digest.from_halves(*transcript.scalars(2)) From 37ff5088b11b9cc96a3d93eb1f7eb2def93e64f1 Mon Sep 17 00:00:00 2001 From: Tom Wambsgans Date: Sat, 22 Aug 2026 16:13:00 +0200 Subject: [PATCH 08/13] Validate an aggregate cheaply before doing its expensive work `from_parts` recomputed the two deferred claims before anything else, so deserializing ran a pass over the whole stacked bytecode plus a walk of the BLAKE2s circuit on points a peer chose. Anything decidable without that has to be decided first: `recompute` already checked the point dimensions, and `check_signer_set` now runs ahead of it, so a malformed signer set costs a sort check instead of the two evaluations. `verify` still checks it too, since `aggregate` builds the object directly rather than through `from_parts`. Also reject trailing bytes. `bincode`'s free functions allow them, so every padding of an aggregate's encoding decoded to the same aggregate, and anything downstream that dedupes or indexes on the serialized bytes could be shown one aggregate as many. `wire()` keeps the same fixed-width integer encoding and rejects the trailing bytes; the encoding was checked to be byte-identical to what the free function produces, since a wire-format change would have to move every encoder and decoder with it. Co-Authored-By: Claude Opus 5 (1M context) --- crates/rec_aggregation/src/aggregation.rs | 23 +++++++++++++++++++---- 1 file changed, 19 insertions(+), 4 deletions(-) diff --git a/crates/rec_aggregation/src/aggregation.rs b/crates/rec_aggregation/src/aggregation.rs index 6dd4897d1..86a4ee5e5 100644 --- a/crates/rec_aggregation/src/aggregation.rs +++ b/crates/rec_aggregation/src/aggregation.rs @@ -23,6 +23,7 @@ //! `cpu::layout` of the inner program and the summary of a real `cpu::verify` //! run, so there is no hand-mirrored copy of the protocol to drift. +use bincode::Options as _; use std::collections::BTreeMap; use std::ops::Range; @@ -374,6 +375,14 @@ pub enum AggregateError { /// Everything but the signer set, which a receiver may already hold. type WireCore = (xmss::Message, u32, Vec, Vec, lean_vm::cpu::Proof); +/// The wire encoding: bincode's fixed-width integers, as the free functions use, +/// but rejecting trailing bytes, which they do not. Without that an accepted +/// aggregate has unboundedly many encodings, so anything downstream that dedupes +/// or indexes on the serialized bytes can be made to see one aggregate as many. +fn wire() -> impl bincode::Options { + bincode::DefaultOptions::new().with_fixint_encoding() +} + /// Reject a signer set that the coverage argument does not cover: strict sorting /// is what makes "every declared key signed" mean `public_keys.len()` distinct /// signers rather than one signer counted many times. @@ -400,18 +409,20 @@ impl AggregateSignature { /// points, and the VM proof. The claim *values* are not transmitted; /// [`Self::from_bytes`] recomputes them, so there is nothing to lie about. pub fn to_bytes(&self) -> Vec { - bincode::serialize(&(&self.public_keys, self.core())).expect("an aggregate serializes") + wire() + .serialize(&(&self.public_keys, self.core())) + .expect("an aggregate serializes") } pub fn from_bytes(bytes: &[u8]) -> Option { - let (public_keys, core): (Vec, WireCore) = bincode::deserialize(bytes).ok()?; + let (public_keys, core): (Vec, WireCore) = wire().deserialize(bytes).ok()?; Self::from_parts(public_keys, core) } /// Without the signer set, for a receiver that already knows it. A set other /// than the one aggregated fails verification. pub fn to_bytes_without_pubkeys(&self) -> Vec { - bincode::serialize(&self.core()).expect("an aggregate serializes") + wire().serialize(&self.core()).expect("an aggregate serializes") } pub(crate) fn proof(&self) -> &lean_vm::cpu::Proof { @@ -419,7 +430,7 @@ impl AggregateSignature { } pub fn from_bytes_without_pubkeys(bytes: &[u8], public_keys: Vec) -> Option { - Self::from_parts(public_keys, bincode::deserialize(bytes).ok()?) + Self::from_parts(public_keys, wire().deserialize(bytes).ok()?) } fn core(&self) -> WireCore { @@ -434,6 +445,10 @@ impl AggregateSignature { fn from_parts(public_keys: Vec, core: WireCore) -> Option { let (message, epoch, bytecode_point, matrix_point, proof) = core; + // Cheap rejections first. `recompute` below is a pass over the whole stacked + // bytecode plus a walk of the BLAKE2s circuit, on points a peer chose, so + // anything decidable without it has to be decided before it. + check_signer_set(&public_keys).ok()?; Some(Self { message, epoch, From 3ccbf2e0f657acedad3cbf9b75eaddb15a39b22a Mon Sep 17 00:00:00 2001 From: Tom Wambsgans Date: Sat, 22 Aug 2026 16:33:09 +0200 Subject: [PATCH 09/13] Delete fold-challenge grinding It was zero everywhere and had never run. The only two sources of `fold_grinding_bits` were `vec![0usize; n_levels]` in the fallback config and the literal `0` in the production derivation, and two assertions pinned it there, so four implementations of the mechanism (the prover, the native verifier, the recursive verifier, and the guest's zkDSL) had never executed a single time in any test. Untested code that claims a security capability is worse than absent code, because it reads as coverage. It is also not the lever it looks like. The eta search keeps the proximity-gap term at or above the 128-bit target on its own across every feasible size (measured: min pg_bits is 128..137 over the whole ladder at every rate), so grinding the fold challenges had nothing to close. Where the ladder does stop, it stops because no eta satisfies the Johnson terms simultaneously, at committed sizes well past anything reachable here: every leaf has to be guest-verifiable, so MU_MAX = 28 caps the whole topology while fold grinding would only have bought roughly 32 to 37. Removal is transcript-neutral by construction, since every grind sat behind `if bits > 0` and the bits were always 0. Confirmed: bytecode 321,127 instructions and 796,006 cycles for the recursion benchmark, 2^26.195 committed for the XMSS one, all byte-identical to before, and the adversarial aggregate_statement_binds / aggregate_hints_bind / aggregate_three_levels pass. Query-phase grinding is untouched: it is a live, load-bearing 17 bits. Side effect worth noting: `pow_bits_ok`'s `debug_assert!(bits < 64)` precondition now has one caller instead of two, and the survivor is a compile-time constant. Co-Authored-By: Claude Opus 5 (1M context) --- crates/pcs/src/whir.rs | 34 ++++------------------ crates/pcs/src/whir_config.rs | 29 +++++------------- crates/rec_aggregation/guests/aggregate.py | 12 ++------ crates/rec_aggregation/src/aggregation.rs | 15 ---------- 4 files changed, 15 insertions(+), 75 deletions(-) diff --git a/crates/pcs/src/whir.rs b/crates/pcs/src/whir.rs index 8fed575de..c4c2ca10e 100644 --- a/crates/pcs/src/whir.rs +++ b/crates/pcs/src/whir.rs @@ -1324,7 +1324,6 @@ pub fn recursive_prover_with_basis( }; ps.observe_root(&initial_root); - let fold_bits = |lvl: usize| -> u32 { config.fold_grinding_bits.get(lvl).copied().unwrap_or(0) as u32 }; let ood_count = |lvl: usize| -> usize { config.ood_samples.get(lvl).copied().unwrap_or(0) }; let _t = std::time::Instant::now(); @@ -1335,13 +1334,6 @@ pub fn recursive_prover_with_basis( let mut r_lane_fold = Vec::with_capacity(initial_k); for j in 0..initial_k { - // Tapered fold-challenge grinding: round j of the lane fold needs - // (fold_bits - j) bits (worst round j=0 carries the full budget); see - // the original's App. C.3 `mca-commutes` comment. - let bits = fold_bits(0).saturating_sub(j as u32); - if bits > 0 { - ps.grind(bits); - } let r_j = ps.sample(); let msg = sumcheck_span.in_scope(|| sc_prover.fold_lane(r_j, lane_block, j + 1 == initial_k)); send_msg(ps, msg, sc_prover.claim()); @@ -1432,13 +1424,7 @@ pub fn recursive_prover_with_basis( let mut level_rs = Vec::with_capacity(k_i); let _t = std::time::Instant::now(); let sumcheck_span = tracing::info_span!("Sumcheck"); - for j in 0..k_i { - // These folds fold level i+1's commitment; tapered grinding as in - // the L0 loop. - let bits = fold_bits(i + 1).saturating_sub(j as u32); - if bits > 0 { - ps.grind(bits); - } + for _ in 0..k_i { let ri = ps.sample(); let msg = sumcheck_span.in_scope(|| sc_prover.fold(ri)); send_msg(ps, msg, sc_prover.claim()); @@ -1662,16 +1648,11 @@ impl PrevLevel { fn replay_fold_rounds( vs: &mut impl Receiver, k: usize, - level_fold_bits: u32, t_r: &mut F192, running_quad: &mut RoundQuad, ) -> Option> { let mut rs = Vec::with_capacity(k); - for j in 0..k { - let bits = level_fold_bits.saturating_sub(j as u32); - if bits > 0 { - vs.grind_check(bits).ok()?; - } + for _ in 0..k { let ri = vs.sample(); rs.push(ri); *t_r = running_quad.eval(ri); @@ -1774,11 +1755,10 @@ pub fn recursive_verifier_with_basis( return false; }; - let fold_bits = |lvl: usize| -> u32 { config.fold_grinding_bits.get(lvl).copied().unwrap_or(0) as u32 }; let ood_count = |lvl: usize| -> usize { config.ood_samples.get(lvl).copied().unwrap_or(0) }; let mut ood_bases: Vec<(Vec, usize, F192)> = Vec::new(); - let Some(r_lane_fold) = replay_fold_rounds(vs, initial_k, fold_bits(0), &mut t_r, &mut running_quad) else { + let Some(r_lane_fold) = replay_fold_rounds(vs, initial_k, &mut t_r, &mut running_quad) else { return false; }; @@ -1869,7 +1849,7 @@ pub fn recursive_verifier_with_basis( if n_current < k_i { return false; } - let Some(level_rs) = replay_fold_rounds(vs, k_i, fold_bits(i + 1), &mut t_r, &mut running_quad) else { + let Some(level_rs) = replay_fold_rounds(vs, k_i, &mut t_r, &mut running_quad) else { return false; }; ris.extend_from_slice(&level_rs); @@ -2116,7 +2096,6 @@ where return false; }; - let fold_bits = |lvl: usize| -> u32 { config.fold_grinding_bits.get(lvl).copied().unwrap_or(0) as u32 }; let ood_count = |lvl: usize| -> usize { config.ood_samples.get(lvl).copied().unwrap_or(0) }; struct OodCtx { z: Vec, @@ -2125,7 +2104,7 @@ where } let mut ood_ctxs: Vec = Vec::new(); - let Some(r_lane_fold) = replay_fold_rounds(vs, initial_k, fold_bits(0), &mut t_r, &mut running_quad) else { + let Some(r_lane_fold) = replay_fold_rounds(vs, initial_k, &mut t_r, &mut running_quad) else { return false; }; @@ -2216,7 +2195,7 @@ where if n_current < k_i { return false; } - let Some(level_rs) = replay_fold_rounds(vs, k_i, fold_bits(i + 1), &mut t_r, &mut running_quad) else { + let Some(level_rs) = replay_fold_rounds(vs, k_i, &mut t_r, &mut running_quad) else { return false; }; ris.extend_from_slice(&level_rs); @@ -2511,7 +2490,6 @@ mod tests { assert_eq!(pc.ood_samples[0], 0); assert!(pc.ood_samples.iter().skip(1).all(|&s| s >= 1)); assert!(pc.grinding_bits.iter().all(|&b| b == QUERY_GRINDING_BITS)); - assert!(pc.fold_grinding_bits.iter().all(|&b| b == 0)); // And log_n = 12 is below the production ladder's feasibility floor, so // the tests there use the default_config fallback. assert!(configs_for(12).is_err()); diff --git a/crates/pcs/src/whir_config.rs b/crates/pcs/src/whir_config.rs index 998d9e7bf..e3f54c7b5 100644 --- a/crates/pcs/src/whir_config.rs +++ b/crates/pcs/src/whir_config.rs @@ -108,12 +108,6 @@ pub struct ProverConfig { /// post-commit/pre-queries. Length = level_steps + 1. Each bit here /// substitutes for ~1/log₂(1/(1−γ)) queries at that level. pub grinding_bits: Vec, - /// Per-level **fold-challenge** PoW grinding bits (L0, ..., L_r), ground - /// immediately before EACH of the level's fold challenges (so a level - /// with `k` folds does `k` grinds of this many bits). Boosts the - /// proximity-gap term, which lives on the fold challenges. Length = - /// level_steps + 1. - pub fold_grinding_bits: Vec, /// Per-commit-level out-of-domain samples (L0, ..., L_r), taken right /// after the level's Merkle root enters the transcript. `[0]` must be 0: /// L0 is bound by the opening's own (post-commit, random-point) @@ -225,7 +219,6 @@ pub fn default_config(log_n: usize, log_batch_size: usize, log_inv_rate: usize) initial_k, level_ks: shape.k_levels[1..].to_vec(), grinding_bits: vec![0usize; n_levels], - fold_grinding_bits: vec![0usize; n_levels], ood_samples: vec![0usize; n_levels], }) } @@ -328,8 +321,9 @@ fn derive_ladder_shape(log_n: usize, initial_k: usize, log_inv_rate: usize) -> R // That analysis is always the Johnson radius with explicit slack `eta` // (gamma = (1 - sqrt(rho)) - eta) WITH out-of-domain binding (`doc/leanvm/body/b-polynomial-commitment-scheme.tex`, // Thm `thm:rbr`). The MCA theorem (`thm:mca-johnson` = BCHKS25 Thm 4.6) gives -// the proximity-gap exceptional set `a = O_rho(n / eta^5)`, so a level's -// `fold_grinding_bits` must be at least `target_bits - log2(q/a)`. Binding to a +// the proximity-gap exceptional set `a = O_rho(n / eta^5)`, and the eta search +// keeps `log2(q/a)` above the target on its own rather than grinding the fold +// challenges for it. Binding to a // single codeword of the (Johnson-bounded) interleaved list is via // `ood_samples` explicit multilinear OOD evaluations, except at L0, where the // opening's own post-commit random evaluation claim plays the OOD role (union @@ -366,11 +360,6 @@ pub struct WhirLevelConfig { /// **Query-phase** PoW grinding bits, ground post-commit/pre-queries. /// Each bit substitutes for ~1/log₂(1/(1−γ)) queries at this level. pub grinding_bits: usize, - /// **Fold-challenge** PoW grinding bits, ground immediately before EACH - /// of this level's `k` fold challenges. Boosts the - /// proximity-gap term (which lives on the fold challenges): - /// `eps_pg + fold_grinding_bits ≥ target`. - pub fold_grinding_bits: usize, /// Out-of-domain samples taken right after this level's commit enters /// the transcript. Each binds the prover to a single codeword of the /// interleaved list via a multilinear evaluation claim. @@ -396,8 +385,7 @@ pub struct FinalBlockConfig { /// /// **Validation invariants** (checked by [`Self::validate`]): /// 1. `initial_k + Σ levels[1..].k + final_block.yr_log_n == log_n`. -/// 2. Each level's proximity-gap bits plus its `fold_grinding_bits` reach -/// `target_security_bits`. +/// 2. Each level's proximity-gap bits reach `target_security_bits`. /// 3. Each level's query soundness reaches `target_security_bits − /// grinding_bits` (queries cover what grinding doesn't). /// 4. `eta` is finite and inside the Johnson range for the level's rate. @@ -865,10 +853,10 @@ impl WhirSecurityConfig { // reach target. (The pg bad event lives on the fold challenges, // so only the fold grind (done before each fold challenge) // boosts it; the query-phase grind does not.) - if pg_pred + lv.fold_grinding_bits as f64 + 1e-12 < lv.target_security_bits as f64 { + if pg_pred + 1e-12 < lv.target_security_bits as f64 { return Err(format!( - "L{i}: proximity-gap soundness ({pg_pred:.2} bits) + fold_grinding ({}) < target ({})", - lv.fold_grinding_bits, lv.target_security_bits + "L{i}: proximity-gap soundness ({pg_pred:.2} bits) < target ({})", + lv.target_security_bits )); } @@ -950,7 +938,6 @@ impl WhirSecurityConfig { eta: optimized.eta, queries: optimized.queries, grinding_bits: query_grind, - fold_grinding_bits: 0, ood_samples: optimized.ood_samples, target_security_bits: target_bits, }); @@ -984,7 +971,6 @@ impl WhirSecurityConfig { level_ks: self.levels.iter().skip(1).map(|lv| lv.k).collect(), queries: self.levels.iter().map(|lv| lv.queries).collect(), grinding_bits: self.levels.iter().map(|lv| lv.grinding_bits).collect(), - fold_grinding_bits: self.levels.iter().map(|lv| lv.fold_grinding_bits).collect(), ood_samples: self.levels.iter().map(|lv| lv.ood_samples).collect(), }; Ok((config.clone(), config)) @@ -1024,7 +1010,6 @@ mod tests { let algebraic_bits = johnson_algebraic_bits(level); min_pg_bits = min_pg_bits.min(pg_bits); assert_eq!(level.grinding_bits, QUERY_GRINDING_BITS); - assert_eq!(level.fold_grinding_bits, 0); assert!(query_bits + level.grinding_bits as f64 >= 128.0); assert!(pg_bits >= 128.0); assert!(ood_bits >= 128.0); diff --git a/crates/rec_aggregation/guests/aggregate.py b/crates/rec_aggregation/guests/aggregate.py index ff3c7da1f..a125caa64 100644 --- a/crates/rec_aggregation/guests/aggregate.py +++ b/crates/rec_aggregation/guests/aggregate.py @@ -136,9 +136,8 @@ # match_range. The LIG_* tables carry one row per (rate, m), emitted from the # same derive_profile/level_shapes the prover uses. # Scalars index as TBL[m_idx]; per-level values as TBL[m_idx * LIG_MAX_LEVELS + lvl], -# where m_idx is the flattened (rate, size) configuration index; per-fold grind -# schedules with the LIG_MAX_TOTAL_FOLDS stride; the subspace vanishing constants -# with the LIG_MAX_VANISH_LEN stride. +# where m_idx is the flattened (rate, size) configuration index; the subspace +# vanishing constants with the LIG_MAX_VANISH_LEN stride. # Opening dispatch: baked committed log-size, candidate range, g^-LIG_MIN_LOG_SIZE. LIG_MIN_LOG_SIZE = LIG_MIN_LOG_SIZE_PLACEHOLDER LIG_N_LOG_SIZES = LIG_N_LOG_SIZES_PLACEHOLDER @@ -151,7 +150,6 @@ PCS_MIN_MU = PCS_MIN_MU_PLACEHOLDER # Per-candidate opening tables (P3b): row (m - LIG_MIN_LOG_SIZE) drives that arm. LIG_MAX_LEVELS = LIG_MAX_LEVELS_PLACEHOLDER -LIG_MAX_TOTAL_FOLDS = LIG_MAX_TOTAL_FOLDS_PLACEHOLDER LIG_MAX_VANISH_LEN = LIG_MAX_VANISH_LEN_PLACEHOLDER LIG_MAX_OOD_SAMPLES = LIG_MAX_OOD_SAMPLES_PLACEHOLDER # Global maxima (StackBuf frame sizes are parse-time). @@ -188,7 +186,6 @@ LIG_ROWS_OFF = LIG_ROWS_OFF_PLACEHOLDER LIG_PATHS_OFF = LIG_PATHS_OFF_PLACEHOLDER LIG_VANISH_OFF = LIG_VANISH_OFF_PLACEHOLDER -LIG_FOLD_GRIND_BITS = LIG_FOLD_GRIND_BITS_PLACEHOLDER LIG_VANISH_VALS = LIG_VANISH_VALS_PLACEHOLDER LIG_VANISH_INVS = LIG_VANISH_INVS_PLACEHOLDER LIG_N_CANDIDATES = LIG_N_CANDIDATES_PLACEHOLDER @@ -764,11 +761,6 @@ def open_stacked(m_idx: Const, fs0, fs1, target, commit_root_0, commit_root_1, c for lvl in unroll(0, LIG_N_LEVELS[m_idx]): for j in unroll(0, LIG_FOLDS[m_idx * LIG_MAX_LEVELS + lvl]): fold_idx = LIG_FOLDS_OFF[m_idx * LIG_MAX_LEVELS + lvl] + j - if LIG_FOLD_GRIND_BITS[m_idx * LIG_MAX_TOTAL_FOLDS + fold_idx] != 0: - nonce_v = msg_cursor[GEN ** 0] # raw transport word: bound by the DS_POW_NONCE absorb below - msg_cursor = msg_cursor * GEN - grind_check(fs[0], fs[1], nonce_v, GEN ** LIG_FOLD_GRIND_BITS[m_idx * LIG_MAX_TOTAL_FOLDS + fold_idx]) - fs = absorb_nonce(fs, nonce_v) fs, fold_challenge = squeeze(fs) fold_challenges[GEN ** fold_idx] = fold_challenge sumcheck_target = (round_quad_a * fold_challenge + round_quad_b) * fold_challenge + round_quad_c # evaluate this level's folded quadratic at the fold challenge diff --git a/crates/rec_aggregation/src/aggregation.rs b/crates/rec_aggregation/src/aggregation.rs index 86a4ee5e5..5b1a301b1 100644 --- a/crates/rec_aggregation/src/aggregation.rs +++ b/crates/rec_aggregation/src/aggregation.rs @@ -1704,7 +1704,6 @@ struct OpeningShape { squeezes: Vec, interleaving: Vec, query_grinding_bits: Vec, - fold_grinding_bits: Vec, row_offsets: Vec, path_offsets: Vec, positions_offsets: Vec, @@ -2026,13 +2025,6 @@ fn placeholder_map(kbc: usize) -> BTreeMap { }), "recursive WHIR guest supports whole-block Merkle rows of at most one 1024-byte BLAKE2s chunk" ); - let cfgb = |lvl: usize| vc.fold_grinding_bits.get(lvl).copied().unwrap_or(0) as i64; - let mut cfb: Vec = Vec::new(); - for (lvl, &k) in ck.iter().enumerate().take(cn) { - for j in 0..k { - cfb.push((cfgb(lvl) - j as i64).max(0) as usize); - } - } let psum = |f: &dyn Fn(usize) -> usize| -> Vec { let mut o = Vec::with_capacity(cn); let mut acc = 0; @@ -2072,7 +2064,6 @@ fn placeholder_map(kbc: usize) -> BTreeMap { squeezes: cs, interleaving: cni, query_grinding_bits: cqb, - fold_grinding_bits: cfb, row_offsets: c_rowoff, path_offsets: c_pathoff, positions_offsets: c_qpoff, @@ -2091,11 +2082,9 @@ fn placeholder_map(kbc: usize) -> BTreeMap { .flat_map(|r| (minm..=maxm).map(move |m| oshape(m, r))) .collect(); let maxlev = cands.iter().map(|c| c.n_levels).max().unwrap(); - let maxfolds = cands.iter().map(|c| c.fold_grinding_bits.len()).max().unwrap(); let maxsvk = cands.iter().map(|c| c.vanish_values.len()).max().unwrap(); let maxood = cands.iter().flat_map(|c| &c.ood_samples).copied().max().unwrap_or(0); ps("LIG_MAX_LEVELS", maxlev.to_string()); - ps("LIG_MAX_TOTAL_FOLDS", maxfolds.to_string()); ps("LIG_MAX_VANISH_LEN", maxsvk.to_string()); ps("LIG_MAX_OOD_SAMPLES", maxood.to_string()); ps("LIG_MIN_LOG_SIZE", minm.to_string()); @@ -2269,10 +2258,6 @@ fn placeholder_map(kbc: usize) -> BTreeMap { ps("LIG_ROWS_OFF", ints(&flat(&|c| c.row_offsets.clone(), maxlev))); ps("LIG_PATHS_OFF", ints(&flat(&|c| c.path_offsets.clone(), maxlev))); ps("LIG_VANISH_OFF", ints(&flat(&|c| c.vanish_offsets.clone(), maxlev))); - ps( - "LIG_FOLD_GRIND_BITS", - ints(&flat(&|c| c.fold_grinding_bits.clone(), maxfolds)), - ); let mut svk2 = Vec::new(); let mut ivk2 = Vec::new(); for c in &cands { From 295593497d7c4516a7b4bc2ffb31d600642e160a Mon Sep 17 00:00:00 2001 From: Tom Wambsgans Date: Sat, 22 Aug 2026 16:36:58 +0200 Subject: [PATCH 10/13] Cap the bytecode length in the Python verifier `lean_vm::cpu::read_public` rejects a bytecode that is not a power of two or longer than 2^MAX_LOG_BYTECODE; `python-verifier` checked neither. The power-of-two half was reachable only through `Framework.log_bytecode`, a property, so it fired wherever that was first read rather than up front, and nothing bounded the length at all. Checked in `build_layout`, with the memory-size, table-height and BLAKE2s-floor caps it belongs to. `0 <= log_bytecode` also rejects a bytecode shorter than one bus row, which used to yield a negative log and carry on. The 2^32 ceiling is not exercisable in a test: reaching it needs 2^36 K-words of stacked bytecode. Same on the Rust side. Co-Authored-By: Claude Opus 5 (1M context) --- python-verifier/verifier.py | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/python-verifier/verifier.py b/python-verifier/verifier.py index b919c5816..269016f79 100644 --- a/python-verifier/verifier.py +++ b/python-verifier/verifier.py @@ -1210,8 +1210,12 @@ def _flushes_pack(table: Table) -> Flushes: def build_layout(bytecode: Sequence[K], log_memory: int, table_log_heights: Sequence[int]) -> Layout: + log_bytecode = log2_strict(len(bytecode)) - BUS_BITS require( - 16 <= log_memory <= 32 and all(0 <= log_height <= 32 for log_height in table_log_heights) and table_log_heights[BLAKE2S.opcode] >= 3, + 16 <= log_memory <= 32 + and all(0 <= log_height <= 32 for log_height in table_log_heights) + and table_log_heights[BLAKE2S.opcode] >= 3 + and 0 <= log_bytecode <= 32, "invalid announced table sizes", ) table_log_heights = list(table_log_heights) From db7ffbaf87f43401ef673818694802f59058ff84 Mon Sep 17 00:00:00 2001 From: Tom Wambsgans Date: Sat, 22 Aug 2026 17:02:01 +0200 Subject: [PATCH 11/13] Annex B: the final level as it is implemented Protocol 1 step 4 described a final level that checks `Enc(f_final)[x_q] == c_q` for each query directly. All three verifiers instead turn each consistency check into a weighted claim about `f_final`, which Lemma `lem:colweight` already says it is, batch those with the residual claim under a fresh lambda drawn after the columns and their opened rows are bound, and discharge the batch with the level's remaining sumcheck rounds, closing on one evaluation of the transmitted table. That is one evaluation of `f_final` where the written version is `n_q` encodings of it. Same claims, so the case analysis is unchanged; it now ends by putting `f_final` in violation of one of the `n_q + 1` batched claims rather than failing a check outright. The extra batching challenge the implementations draw was missing from `thm:rbr`, so add its term: `n_q / |E|`, with no union over a list, since `f_final` is a single transmitted table rather than one of the codewords near an oracle. At the query counts in use that term is far below the 128-bit target, so the security level does not move; the point is that the theorem now accounts for every challenge the protocol draws. The RBR invariant gains the matching step, since the transcript no longer ends at the final query message. Co-Authored-By: Claude Opus 5 (1M context) --- crates/lean_compiler/tests/suite/soundness/mod.rs | 8 ++++---- doc/leanvm/body/b-polynomial-commitment-scheme.tex | 11 +++++++---- 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/crates/lean_compiler/tests/suite/soundness/mod.rs b/crates/lean_compiler/tests/suite/soundness/mod.rs index a43b4abb0..a756ac715 100644 --- a/crates/lean_compiler/tests/suite/soundness/mod.rs +++ b/crates/lean_compiler/tests/suite/soundness/mod.rs @@ -6,23 +6,23 @@ //! a proof that accepts something it should not. So the three checks below all //! attack the *absence* of a constraint rather than the presence of a value. //! -//! 1. [`check_case`] — **perturbation**. One valid trial that must run, and a +//! 1. [`check_case`], **perturbation**: one valid trial that must run, and a //! table of single-cell pokes at the public input or a witness stream, each of //! which must make the run fail. A dropped assertion shows up as a poke that //! is accepted. (This is the shape of `leanVM`'s own soundness suite.) -//! 2. [`check_pair`] — **equivalence**. Two spellings the language documents as +//! 2. [`check_pair`], **equivalence**: two spellings the language documents as //! interchangeable must accept exactly the same trials. Every dropped-constraint //! bug found so far is an *asymmetry*: an assertion that survives one spelling //! and vanishes in the other, so comparing the two finds it without anyone //! having to guess which side is wrong. -//! 3. [`Execution::unconstrained_reads`] — **unconstrained reads**, asserted on +//! 3. [`Execution::unconstrained_reads`], **unconstrained reads**, asserted on //! every accepting run of both layers above. A cell an instruction read that //! nothing ever wrote is a live value from outside the constraint system. //! //! The three are complementary, and a fix should land with whichever one catches //! it. Layer 3 sees a dropped store whose cell is then *read* (the value came from //! nowhere); layer 2 sees a dropped store whose cell is then *ignored* (the value -//! came from the alias instead, and the physical write is orphaned) — layer 3 is +//! came from the alias instead, and the physical write is orphaned), and layer 3 is //! blind to that one, because nothing reads the orphan. Layer 1 needs a program //! whose assertion the poke can violate, and in exchange it needs no second //! spelling to compare against. diff --git a/doc/leanvm/body/b-polynomial-commitment-scheme.tex b/doc/leanvm/body/b-polynomial-commitment-scheme.tex index 167fbb178..a63de894f 100644 --- a/doc/leanvm/body/b-polynomial-commitment-scheme.tex +++ b/doc/leanvm/body/b-polynomial-commitment-scheme.tex @@ -117,7 +117,7 @@ \subsection{The protocol}\label{sec:protocol} \item \emph{(query)} $\mathbf{V}$ sends $\nq_i$ i.i.d.\ columns $\qset_i = (x_q)_{q = 1, \dots, \nq_i} \leftarrow \dom_i$; it reads $\orc^{(i)}[\cdot, x_q]$ and computes $c_q := \sum_{u} \eq(\fc, u)\, \orc^{(i)}[u, x_q] = \orc^{(i)}_\fc[x_q]$; honestly $c_q = \Enc_i(f^{(i+1)})[x_q]$, by Fact~\ref{fact:fold-decode}. \item Claims for level $i+1$ (so $J_{i+1} := \nq_i + 2$): the residual claim $(W', c')$, the OOD claim $(\eq(z, \cdot), \cood)$, and the $\nq_i$ \emph{consistency claims} $(W^{(i)}_{x_q}, c_q)$, where $W^{(i)}_x$ are the column weights of $\Enc_i$ (\S\ref{sec:binary-rs}): the $q$-th asserts $\Enc_i(f^{(i+1)})[x_q] = c_q$. \end{enumerate} -\item If $i = \nlev - 1$: \emph{(final)} $\mathbf{P}$ sends the multilinear $\ffinal : \cube{\nv_\nlev} \to \E$; $\mathbf{V}$ sends $\nq_{\nlev-1}$ i.i.d.\ columns $\qset_{\nlev-1} \leftarrow \dom_{\nlev-1}$, computes $c_q$ from $\orc^{(\nlev-1)}$ as in 3(c), and checks $\sum_{x \in \cube{\nv_\nlev}} W'(x)\, \ffinal(x) \qeq c'$ and $\Enc_{\nlev-1}(\ffinal)[x_q] \qeq c_q$ for all $q = 1, \dots, \nq_{\nlev-1}$. +\item If $i = \nlev - 1$: \emph{(final)} $\mathbf{P}$ sends the multilinear $\ffinal : \cube{\nv_\nlev} \to \E$; $\mathbf{V}$ sends $\nq_{\nlev-1}$ i.i.d.\ columns $\qset_{\nlev-1} \leftarrow \dom_{\nlev-1}$ and computes $c_q$ from $\orc^{(\nlev-1)}$ as in 3(c). Consistency is again a weighted claim, $\Enc_{\nlev-1}(\ffinal)[x_q] = \inner{W^{(\nlev-1)}_{x_q}}{\ffinal}$ (Lemma~\ref{lem:colweight}), so the level closes like the others: $\mathbf{V}$ samples and sends $\lambda \leftarrow \E$, batching the $\nq_{\nlev-1}$ consistency claims with the residual claim $(W', c')$ into one claim about $\ffinal$; $\nv_\nlev$ further sumcheck rounds discharge it, and $\mathbf{V}$ closes by evaluating $\mle{\ffinal}$ at their point from the table it holds. \end{enumerate} $\mathbf{V}$ accepts iff every check above passed. \end{protocol} @@ -143,7 +143,9 @@ \subsection{Round-by-round soundness}\label{sec:soundness} \textnormal{batching, level } i: & \varepsilon^{\mathrm{batch}}_i &=& \dfrac{(J_i - 1)\, L_i}{|\E|} , \\[2ex] \textnormal{fold challenge } \fc_j, \textnormal{ level } i: & \varepsilon^{\mathrm{fold}}_{i,j} &=& \dfrac{2 L_i}{|\E|} + 2^{\ell_i - j}\, \epsilon_i , \\[2ex] \textnormal{OOD challenge entering level } i \ge 1: & \varepsilon^{\mathrm{ood}}_i &=& \dbinom{L_i}{2} \cdot \dfrac{\nv_i}{|\E|} , \\[2ex] -\textnormal{query message } \qset_i: & \varepsilon^{\mathrm{query}}_i &=& (1 - \rad_i)^{\nq_i} . +\textnormal{query message } \qset_i: & \varepsilon^{\mathrm{query}}_i &=& (1 - \rad_i)^{\nq_i} , \\[2ex] +\textnormal{final batching challenge } \lambda: & \varepsilon^{\mathrm{fin}} &=& \dfrac{\nq_{\nlev-1}}{|\E|} , \\[2ex] +\textnormal{each of the } \nv_\nlev \textnormal{ closing rounds}: & \varepsilon^{\mathrm{tail}} &=& \dfrac{2}{|\E|} . \end{array} \] Here $J_0$ is the number of input claims and $J_i = \nq_{i-1} + 2$ for $i \ge 1$. The \emph{RBR error}, which governs the Fiat--Shamir compilation (\S\ref{sec:iopcs}), is the maximum of these entries over all rounds. @@ -216,7 +218,8 @@ \subsubsection{Proof of the main theorem}\label{pcs:proof} \item \emph{Start of level $i$} (before any message for $i = 0$, after the query message $J_{i-1}$ otherwise): every $U \in \lst_{\rad_i}(\orc^{(i)})$ violates at least one of the level's $J_i$ claims (the input claims for $i = 0$, the claims of step 3(d) of Protocol~\ref{fig:protocol} otherwise). \item \emph{After the batching challenge $\lambda$ of level $i$, and after each of its fold challenges $\fc_j$:} every $U \in \lst_{\rad_i}(\orc^{(i)}_{\fc^{\le j}})$ violates the round-$j$ claim ($\lambda$ being the case $j = 0$). \item \emph{After the OOD challenge $z$ closing level $i$ ($i < \nlev-1$):} the round-$\ell_i$ instance above holds, and the multilinear extensions decoded from $\lst_{\rad_{i+1}}(\orc^{(i+1)})$ are pairwise distinct at $z$. -\item \emph{After the final query message $\qset_{\nlev-1}$ (complete transcript):} the escape clause alone, i.e.\ some verifier check fails, so the verifier rejects. +\item \emph{After the final query message $\qset_{\nlev-1}$:} $\ffinal$ violates one of the level's $\nq_{\nlev-1}+1$ claims. +\item \emph{After the final $\lambda$, and after each of the $\nv_\nlev$ rounds that follow (complete transcript):} $\ffinal$ violates the running claim. The terminal one $\mathbf{V}$ checks against $\mle{\ffinal}$ itself, so it rejects. \end{itemize} Conditions (i), (ii), (iv) of Definition~\ref{def:rbr} hold by inspection: on a false statement, the first item is exactly the failure of $\relopen$; a prover message changes nothing an instance depends on, except possibly failing a check, which only switches the escape clause on; and the last item is precisely ``some check failed'', so such a complete transcript is rejected. The separation clause of the OOD instance is there because the query message consumes it: it pins the new oracle's list to at most one candidate consistent with the prover's answer. It remains to bound the escape probabilities (iii); in the proof below we assume all checks so far pass, since otherwise the escape clause already holds. @@ -263,7 +266,7 @@ \subsubsection{Proof of the main theorem}\label{pcs:proof} Except with probability $(1 - \rad_i)^{\nq_i}$, every member of $\lst_{\rad_{i+1}}(\orc^{(i+1)})$ thus violates at least one of the $J_{i+1}$ claims, which is exactly the assumption of the batching step at level $i + 1$. \medskip\noindent\emph{Final level.} -At level $\nlev - 1$ the fold challenges end as above: every codeword within $\rad_{\nlev-1}$ of $c := \orc^{(\nlev-1)}_\fc$ violates the residual claim. The prover sends the plaintext multilinear $\ffinal$. If $\Enc_{\nlev-1}(\ffinal)$ agrees with $c$ on at least $(1 - \rad_{\nlev-1}) \blen_{\nlev-1}$ coordinates, then $\Enc_{\nlev-1}(\ffinal) \in \lst_{\rad_{\nlev-1}}(c)$, so $\inner{W'}{\ffinal} \neq c'$: the check $\sum_{x \in \cube{\nv_\nlev}} W'(x)\, \ffinal(x) = c'$ fails whatever $\qset_{\nlev-1}$ is, i.e.\ the escape clause holds and rejection is certain. Otherwise the checks $\Enc_{\nlev-1}(\ffinal)[x_q] = c_q$ can all pass only if every one of the $\nq_{\nlev-1}$ i.i.d.\ queries lands in the agreement set, an event of probability less than $(1 - \rad_{\nlev-1})^{\nq_{\nlev-1}}$. +At level $\nlev - 1$ the fold challenges end as above: every codeword within $\rad_{\nlev-1}$ of $c := \orc^{(\nlev-1)}_\fc$ violates the residual claim. The prover sends $\ffinal$. If $\Enc_{\nlev-1}(\ffinal)$ agrees with $c$ on at least $(1 - \rad_{\nlev-1}) \blen_{\nlev-1}$ coordinates then $\Enc_{\nlev-1}(\ffinal) \in \lst_{\rad_{\nlev-1}}(c)$, so $\ffinal$ violates the residual claim; otherwise, except with probability $(1 - \rad_{\nlev-1})^{\nq_{\nlev-1}}$, some query disagrees and $\ffinal$ violates that consistency claim. Either way it violates one of the $\nq_{\nlev-1}+1$ batched claims, hence the batch itself except with probability $\nq_{\nlev-1}/|\E|$ (Lemma~\ref{lem:sz}), with no union over a list: $\ffinal$ is transmitted, not one of the codewords near an oracle. The $\nv_\nlev$ rounds that follow are a plain sumcheck (Fact~\ref{fact:sumcheck}) on a polynomial $\mathbf{V}$ holds, so the terminal check against $\mle{\ffinal}$ fails. \end{proof} From d91e6fc2ca682489889124f7c925b728222e249f Mon Sep 17 00:00:00 2001 From: Tom Wambsgans Date: Sat, 22 Aug 2026 17:07:06 +0200 Subject: [PATCH 12/13] wip --- doc/leanvm/body/02-vm-specification.tex | 4 ++-- doc/leanvm/body/10-isa-programming.tex | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/leanvm/body/02-vm-specification.tex b/doc/leanvm/body/02-vm-specification.tex index b2d1f771e..21919077e 100644 --- a/doc/leanvm/body/02-vm-specification.tex +++ b/doc/leanvm/body/02-vm-specification.tex @@ -63,7 +63,7 @@ \section{VM specification}\label{sec:vm} \] The \texttt{deref\_pc} and \texttt{deref\_fp} modes let a caller save its return address and frame so a callee can later return and restore them, the basis for function calls. The skip of two is the call's return target: place the \texttt{DEREF} that saves $\gen^{2}\cdot\pc$ immediately before the \texttt{JUMP} that transfers control, and $\gen^{2}\cdot\pc$ names the instruction just after that \texttt{JUMP}. -\texttt{JUMP} reads a condition $c=\loc{o_c}$, an arbitrary $192$-bit word, and branches on whether it is zero. When $c\neq0$ it transfers control, $\pc\gets\loc{o_d}$ and $\fp\gets\loc{o_f}$; when $c=0$ it falls through, $\pc\gets\gen\cdot\pc$ and $\fp\gets\fp$. +\texttt{JUMP} reads a condition $c=\loc{o_c}$, a $\K$-element, and branches on whether it is zero. When $c\neq0$ it transfers control, $\pc\gets\loc{o_d}$ and $\fp\gets\loc{o_f}$; when $c=0$ it falls through, $\pc\gets\gen\cdot\pc$ and $\fp\gets\fp$. -\paragraph{Words used as addresses.} A memory word is $192$-bit, while $\pc$, $\fp$, and addresses are in $\K$. Some instructions (\texttt{DEREF}, \texttt{JUMP}) interpret memory words as address or registers. The VM then requires those words to be stricly in $\K$ (i.e. the two top lanes are zero). For \texttt{JUMP} the requirement is unconditional: $\loc{o_d}$ and $\loc{o_f}$ must be in $\K$ on every execution of the instruction, not only when the branch is taken, which is what lets the table commit one lane of each (\S\ref{sec:tab-jump}). +\paragraph{Words used as addresses.} A memory word is $192$-bit, while $\pc$, $\fp$, and addresses are in $\K$. Some instructions (\texttt{DEREF}, \texttt{JUMP}) interpret memory words as address or registers. The VM then requires those words to be stricly in $\K$ (i.e. the two top lanes are zero). For \texttt{JUMP} the requirement is unconditional: $\loc{o_d}$ and $\loc{o_f}$ must be in $\K$ on every execution of the instruction, not only when the branch is taken. Its condition is $\K$-valued too, though nothing reads it as an address; all three are committed one lane each, the memory interaction zeroing the rest (\S\ref{sec:tab-jump}). diff --git a/doc/leanvm/body/10-isa-programming.tex b/doc/leanvm/body/10-isa-programming.tex index cfacc0c93..c7e9a13d7 100644 --- a/doc/leanvm/body/10-isa-programming.tex +++ b/doc/leanvm/body/10-isa-programming.tex @@ -11,7 +11,7 @@ \subsection{Division and inequality}\label{sec:prog-div-ne} The zkDSL's single-slash division $q=a/b$ uses write-once back-solving: it emits \texttt{MUL\_NATIVE} with $q$ as the one unset input and $a$ as the already-written output. Witness generation fills $q=a\,b^{-1}$, while the ordinary multiplication table proves $q b=a$. It costs one VM instruction. Division by zero is undefined. Double slash \texttt{//} remains compile-time integer floor division for sizes and indices; it is not a field operation. -The assertion \texttt{assert a != b} computes $x=a+b$ with \texttt{XOR}, takes a hinted $w=x^{-1}$, forms $p=x\,w$ with \texttt{MUL\_NATIVE}, and writes $1$ to $p$ with \texttt{SET\_CONSTANT}. Memory being write-once, the two writes to $p$ agree only if $p=1$, and $x=0$ forces $p=0$ whatever the hint. Three instructions, and no branch: the condition of a \texttt{JUMP} would be the $\E$-valued $x$, whereas every branch a program actually needs compares $\gen$-powers. +The assertion \texttt{assert a != b} computes $x=a+b$ with \texttt{XOR}, takes a hinted $w=x^{-1}$, forms $p=x\,w$ with \texttt{MUL\_NATIVE}, and writes $1$ to $p$ with \texttt{SET\_CONSTANT}. Memory being write-once, the two writes to $p$ agree only if $p=1$, and $x=0$ forces $p=0$ whatever the hint. \subsection{Functions}\label{sec:prog-functions} From 8cc7e3d0e29e4ae7af3dcc212ceaa3c203f50a32 Mon Sep 17 00:00:00 2001 From: Tom Wambsgans Date: Sat, 22 Aug 2026 17:16:56 +0200 Subject: [PATCH 13/13] Batch the right claim count in the Johnson algebraic bound `johnson_algebraic_bits_for` took the level's OWN query count as the degree of its batching polynomial. The claims that batch carries are the ones the PREVIOUS level's query phase raised: `thm:rbr` has `J_i = n_{i-1} + 2`, one per query plus the residual and the OOD claim. Query counts fall with depth (at rate 1/2, log_n 28: 228, 56, 38, 28, 23, 19, 16), so the level's own count is the smaller one, and substituting it understates the degree and overstates the bound, by about 2 bits at L1. Thread the previous level's count through instead: the eta search takes it as a parameter, and `validate()` and the production-profile test read it off the level list. Inert either way today, which is the reason to fix it rather than leave it: the degree is `max(RING_SWITCH_SOUNDNESS_DEGREE, prev_queries + ood_samples, 2)`, and the ring-switch map's degree is about 2^31, some 23 bits above any query count, so it takes the max at every level. A wrong term with no effect is the kind that survives a refactor; if that degree is ever tightened, or a level skips ring switching, the bound now degrades correctly. Derivation unchanged, and checked rather than assumed: `whir_query_table_matches_rust` compares the derived query counts against the pinned table at every rate and size in the window, and still passes. L0 is passed 0 and still does not model `J_0`, which is the outer protocol's claim pool rather than a query count. Recorded in the comment; accounting for it would mean teaching `whir_config` about `lean_vm`'s pool. Co-Authored-By: Claude Opus 5 (1M context) --- crates/pcs/src/whir_config.rs | 35 +++++++++++++++++++++++++---------- 1 file changed, 25 insertions(+), 10 deletions(-) diff --git a/crates/pcs/src/whir_config.rs b/crates/pcs/src/whir_config.rs index e3f54c7b5..6b92d0262 100644 --- a/crates/pcs/src/whir_config.rs +++ b/crates/pcs/src/whir_config.rs @@ -543,33 +543,46 @@ fn johnson_interleaved_list_log2(log_inv_rate: usize, log_msg_cols: usize, eta: /// - the total degree of the GF64-to-GF192 ring-switch batching map (L0 only, /// but included at every level so the bound also dominates the claim batch /// entering the next level's list, whatever its query count); -/// - `J − 1 = queries + ood_samples`, the batch polynomial's degree in the -/// level's single lambda (residual + OOD + one claim per query); and +/// - `J − 1 = prev_queries + ood_samples`, the batch polynomial's degree in the +/// level's single lambda. The claims it batches are the ones the PREVIOUS +/// level's query phase raised (`thm:rbr`: `J_i = n_{i-1} + 2`, one per query +/// plus the residual and the OOD claim), so this level's own query count is +/// the wrong quantity: query counts fall with depth, so using it would +/// understate the degree and overstate the bound. At L0 there is no previous +/// level and `J_0` is set by the outer protocol's claim pool rather than by a +/// query count, so 0 is passed; that pool is a few hundred claims, orders below +/// the ring-switch degree the `max` takes anyway; and /// - 2 for quadratic sumcheck. fn johnson_algebraic_bits_for( log_inv_rate: usize, log_msg_cols: usize, eta: f64, - queries: usize, + prev_queries: usize, ood_samples: usize, ) -> f64 { let log2_l = johnson_interleaved_list_log2(log_inv_rate, log_msg_cols, eta); let degree = crate::ring_switch::RING_SWITCH_SOUNDNESS_DEGREE - .max(queries + ood_samples) + .max(prev_queries + ood_samples) .max(2); ANALYSIS_LOG_Q - (degree as f64).log2() - log2_l } -fn johnson_algebraic_bits(level: &WhirLevelConfig) -> f64 { +/// `prev_queries` is `levels[i-1].queries`, and 0 for `i = 0`. +fn johnson_algebraic_bits(level: &WhirLevelConfig, prev_queries: usize) -> f64 { johnson_algebraic_bits_for( level.log_inv_rate, level.log_msg_cols, level.eta, - level.queries, + prev_queries, level.ood_samples, ) } +/// The query count the batch at `levels[i]` carries claims from. +fn prev_queries_at(levels: &[WhirLevelConfig], i: usize) -> usize { + if i == 0 { 0 } else { levels[i - 1].queries } +} + /// OOD binding bits for a level. `mu_vars` is the level's multilinear /// variable count (`log_msg_cols + log_num_interleaved`). /// @@ -630,6 +643,7 @@ fn optimize_johnson_level( log_num_interleaved: usize, target_bits: usize, query_grinding_bits: usize, + prev_queries: usize, ) -> Result { let target = target_bits as f64; let query_target = target_bits.saturating_sub(query_grinding_bits).max(1) as f64; @@ -670,7 +684,7 @@ fn optimize_johnson_level( }; let eps_ood = paper_ood_bits(log_inv_rate, log_msg_cols, eta, mu, ood_samples); if eps_ood + 1e-12 < target - || johnson_algebraic_bits_for(log_inv_rate, log_msg_cols, eta, queries, ood_samples) + 1e-12 < target + || johnson_algebraic_bits_for(log_inv_rate, log_msg_cols, eta, prev_queries, ood_samples) + 1e-12 < target { continue; } @@ -863,7 +877,7 @@ impl WhirSecurityConfig { // The largest list-unioned algebraic identity test (currently the // composed ring-switch batching map) is not grindable and must // clear the target. - let algebraic = johnson_algebraic_bits(lv); + let algebraic = johnson_algebraic_bits(lv, prev_queries_at(&self.levels, i)); if algebraic + 1e-12 < lv.target_security_bits as f64 { return Err(format!( "L{i}: list-unioned algebraic soundness ({algebraic:.2} bits) < target ({})", @@ -928,7 +942,8 @@ impl WhirSecurityConfig { let rate = shape.log_inv_rates[i]; let cols = shape.log_msg_cols[i]; let ilv = shape.log_num_interleaved[i]; - let optimized = optimize_johnson_level(i, rate, cols, ilv, target_bits, query_grind)?; + let prev_queries = prev_queries_at(&levels, i); + let optimized = optimize_johnson_level(i, rate, cols, ilv, target_bits, query_grind, prev_queries)?; levels.push(WhirLevelConfig { log_inv_rate: rate, @@ -1007,7 +1022,7 @@ mod tests { for (i, level) in cfg.levels.iter().enumerate() { let (pg_bits, query_bits) = level.paper_predicted_bits(); let ood_bits = level.paper_predicted_ood_bits(); - let algebraic_bits = johnson_algebraic_bits(level); + let algebraic_bits = johnson_algebraic_bits(level, prev_queries_at(&cfg.levels, i)); min_pg_bits = min_pg_bits.min(pg_bits); assert_eq!(level.grinding_bits, QUERY_GRINDING_BITS); assert!(query_bits + level.grinding_bits as f64 >= 128.0);