diff --git a/crates/lean_compiler/src/lower.rs b/crates/lean_compiler/src/lower.rs index 3e41dfe89..8af5f9237 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 }); } @@ -230,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); @@ -342,12 +406,30 @@ 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. + 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`. @@ -504,11 +586,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); @@ -620,7 +706,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 => {} } @@ -640,6 +729,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 @@ -894,7 +1006,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)); @@ -1608,7 +1723,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, } @@ -1787,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)); @@ -1821,6 +1942,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 { @@ -2140,6 +2275,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 })); } @@ -2186,7 +2326,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") { @@ -2588,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 @@ -2612,6 +2761,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/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..ac88f4e92 --- /dev/null +++ b/crates/lean_compiler/tests/suite/soundness/cases.rs @@ -0,0 +1,379 @@ +//! 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)`. +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), +]; + +/// 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]); +} + +/// 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 +", + ); +} + +/// 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 +", + ); +} 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..a756ac715 --- /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), 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. + +#![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..618c768be --- /dev/null +++ b/crates/lean_compiler/tests/suite/soundness/pairs.rs @@ -0,0 +1,451 @@ +//! 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]]) +} + +/// 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)), + ], + }); +} + +/// 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)), + ], + }); +} + +/// 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]]) +} 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. 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..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)) } @@ -494,6 +499,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 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/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..6b92d0262 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. @@ -555,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`). /// @@ -642,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; @@ -682,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; } @@ -865,17 +867,17 @@ 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 )); } // 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 ({})", @@ -940,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, @@ -950,7 +953,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 +986,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)) @@ -1021,10 +1022,9 @@ 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_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 0e7bca3ce..5b1a301b1 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, @@ -1370,7 +1385,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 @@ -1687,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, @@ -2009,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; @@ -2055,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, @@ -2074,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()); @@ -2252,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 { 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} 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} diff --git a/python-verifier/verifier.py b/python-verifier/verifier.py index 850eee3ae..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) @@ -1266,7 +1270,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 +1837,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))