From 9d44dceddbb68ad94182f15c34a3e665ce1e6c0a Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Wed, 7 Oct 2026 21:54:43 +0100 Subject: [PATCH 01/14] zk: zero-knowledge leaf proofs, stages 0 to 3 in Rust (draft) An opt-in zk mode for RISC-V leaf proofs, by composition. - Stage 0: a zero-knowledge proof travels as LVMZ version 15 with its own transcript seed; the prover draws its randomness from ChaCha20 seeded by the OS or a test; Prover::zk and the CLI's --zk. Plain proofs are unchanged. - Stage 1: the hiding stacked WHIR: lanes padded past their power of two (one butterfly layer folded into the encode's first pass, the padding factor shifted so it vanishes nowhere on the domain), one uniform lane, the revealed claim after the lane fold and the padding's fold, the level-0 correction, a query table rederived for the padded code; Annex B describes it. - Stages 2 and 3: every scalar the plain protocol sends until its opening's lane fold ends travels under a one-time pad from a separate key commitment; the verifier runs its own code over a recording arithmetic whose canonical constraints a natively zero-knowledge Spartan over E proves (eq-weighted Libra mask, two dummy constraints); the final clock's free bits are hidden scalars constrained to be bits; the deferred claims become linear constraints. leanXMSS 400 at rate 1/4, single local runs at load about 5: proof 240.6 KiB plain, 350.3 KiB zk; proving 0.486 s and 0.511 s; verifying 3.5 ms and 12.0 ms. Not yet: the Python verifier's zk mode, the spec of the composition, zk variants of the integration tests, the tracked bench case. --- Cargo.lock | 2 + Cargo.toml | 2 + bins/leanvm/src/main.rs | 12 +- bins/leanvm/src/workload.rs | 3 +- crates/fiat_shamir/src/arith.rs | 15 + crates/fiat_shamir/src/transcript.rs | 65 +- crates/flock/benches/arithmetic_batch.rs | 4 +- crates/flock/benches/hash_batch.rs | 4 +- crates/flock/src/lincheck.rs | 12 + crates/leanvm/src/lib.rs | 10 +- crates/leanvm_core/Cargo.toml | 2 + crates/leanvm_core/src/cpu/deferred.rs | 84 ++- crates/leanvm_core/src/cpu/error.rs | 22 + crates/leanvm_core/src/cpu/layout.rs | 95 ++- crates/leanvm_core/src/cpu/mod.rs | 1 + crates/leanvm_core/src/cpu/program.rs | 101 ++- crates/leanvm_core/src/cpu/proof.rs | 32 +- crates/leanvm_core/src/cpu/prover.rs | 31 +- crates/leanvm_core/src/cpu/reduce.rs | 18 + crates/leanvm_core/src/cpu/witness.rs | 11 +- crates/leanvm_core/src/cpu/zk.rs | 325 ++++++++++ crates/leanvm_core/src/envelope.rs | 5 + crates/leanvm_core/src/leaf.rs | 2 +- crates/leanvm_core/src/leaf/decompose.rs | 15 +- crates/leanvm_core/src/lib.rs | 2 + crates/leanvm_core/src/pcs.rs | 68 ++- crates/leanvm_core/src/rec/proof.rs | 2 +- crates/leanvm_core/src/rec/tree/mod.rs | 5 + crates/leanvm_core/src/rec/verifier/tests.rs | 8 +- crates/leanvm_core/src/witness.rs | 40 +- crates/leanvm_core/src/zk/keys.rs | 100 +++ crates/leanvm_core/src/zk/mod.rs | 8 + crates/leanvm_core/src/zk/outer.rs | 110 ++++ crates/leanvm_core/src/zk/r1cs.rs | 84 +++ crates/leanvm_core/src/zk/randomness.rs | 86 +++ crates/leanvm_core/src/zk/spartan.rs | 328 ++++++++++ crates/leanvm_core/src/zk/sym.rs | 574 ++++++++++++++++++ crates/pcs/benches/throughput.rs | 11 +- crates/pcs/src/ntt.rs | 2 +- crates/pcs/src/ntt/additive_ntt_f64.rs | 170 +++++- crates/pcs/src/ring_switch.rs | 8 +- crates/pcs/src/stack_open.rs | 225 ++++++- crates/pcs/src/whir.rs | 20 +- crates/pcs/src/whir/commit.rs | 49 +- crates/pcs/src/whir/config.rs | 102 +++- crates/pcs/src/whir/config/tests.rs | 309 +++++++--- crates/pcs/src/whir/induce.rs | 41 ++ crates/pcs/src/whir/prove.rs | 61 +- crates/pcs/src/whir/tests.rs | 111 +++- crates/pcs/src/whir/verify.rs | 136 ++++- .../body/b-polynomial-commitment-scheme.tex | 46 ++ doc/leanvm/preamble/macros.tex | 6 + doc/leanvm/refs.bib | 16 + 53 files changed, 3330 insertions(+), 271 deletions(-) create mode 100644 crates/leanvm_core/src/cpu/zk.rs create mode 100644 crates/leanvm_core/src/zk/keys.rs create mode 100644 crates/leanvm_core/src/zk/mod.rs create mode 100644 crates/leanvm_core/src/zk/outer.rs create mode 100644 crates/leanvm_core/src/zk/r1cs.rs create mode 100644 crates/leanvm_core/src/zk/randomness.rs create mode 100644 crates/leanvm_core/src/zk/spartan.rs create mode 100644 crates/leanvm_core/src/zk/sym.rs diff --git a/Cargo.lock b/Cargo.lock index 9295ee62b..0881912c7 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1508,6 +1508,8 @@ dependencies = [ "pcs", "primitives", "proptest", + "rand_chacha 0.9.0", + "rand_core 0.9.5", "thiserror", "tracing", ] diff --git a/Cargo.toml b/Cargo.toml index 31d9802ba..174762b3a 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -49,6 +49,8 @@ proptest = { version = "1", default-features = false, features = ["std"] } serde = { version = "1", features = ["derive"] } bincode = "1" rand = "0.9" +rand_chacha = "0.9" +rand_core = { version = "0.9", features = ["os_rng"] } thiserror = { version = "2", default-features = false } tikv-jemallocator = "0.7" tracing = "0.1.26" diff --git a/bins/leanvm/src/main.rs b/bins/leanvm/src/main.rs index 4a13e7d23..cfbcbf434 100644 --- a/bins/leanvm/src/main.rs +++ b/bins/leanvm/src/main.rs @@ -4,7 +4,7 @@ use aggregate::LeafProgram; use bench::Plan; use clap::builder::RangedU64ValueParser; use clap::{Parser, Subcommand}; -use leanvm::{Prover, Rate}; +use leanvm::{Prover, Randomness, Rate}; use std::error::Error; use std::fmt::Arguments; use std::num::ParseIntError; @@ -37,6 +37,10 @@ struct Cli { #[arg(long, global = true)] tracing: bool, + /// Make zero-knowledge proofs, from fresh randomness the OS gives each proof. + #[arg(long, global = true)] + zk: bool, + /// Measured proving passes after warmup. #[arg( long, @@ -178,7 +182,13 @@ fn refuse(what: Arguments) -> ! { fn main() { let cli = Cli::parse(); + if cli.zk && matches!(cli.command, Command::Aggregate { .. } | Command::Bench { .. }) { + refuse(format_args!( + "--zk proves single runs: an aggregation tree does not verify zero-knowledge leaves, and the benchmark tracks its own zero-knowledge case" + )); + } let prover = Prover::new(cli.rate); + let prover = if cli.zk { prover.zk(Randomness::Os) } else { prover }; let leaf_prover = Prover::new(cli.leaf_rate); let plan = Plan::new(cli.repeat, cli.cooldown); if cli.tracing { diff --git a/bins/leanvm/src/workload.rs b/bins/leanvm/src/workload.rs index 7fbae43bf..ac928fc76 100644 --- a/bins/leanvm/src/workload.rs +++ b/bins/leanvm/src/workload.rs @@ -196,7 +196,8 @@ impl Workload { let cycles = stats.cycles(); let seconds = prove_time.mean(); - println!("{}", self.title); + let zk = if prover.is_zk() { ", zero knowledge" } else { "" }; + println!("{}{zk}", self.title); println!( " advice : {} words", pretty_integer(&self.advice.len()) diff --git a/crates/fiat_shamir/src/arith.rs b/crates/fiat_shamir/src/arith.rs index 6379b7930..fcd38ed79 100644 --- a/crates/fiat_shamir/src/arith.rs +++ b/crates/fiat_shamir/src/arith.rs @@ -32,6 +32,14 @@ pub trait Arith { /// `a^(2^128)`: two Frobenius maps of `E` over `K`, which take `a` to `a^(2^-64)`. fn frobenius2(&mut self, a: Self::E) -> Self::E; + /// The same element, which the caller reuses many times. + /// + /// A recording arithmetic may give it a variable of its own, so that what reuses it stays short; by default it is + /// returned as it is. + fn bind(&mut self, a: Self::E) -> Self::E { + a + } + /// The multilinear extension of public `K` words at `point`, lowest coordinate first. fn public_mle(&mut self, values: &[F64], point: &[Self::E]) -> Self::E { assert_eq!(values.len(), 1 << point.len(), "a column has a word per vertex"); @@ -231,6 +239,13 @@ pub trait Verifier: Arith { f(self) } + /// Whether the scalars read from now on travel under one-time-pad keys (doc `leanvm` §sec:zk). + /// + /// A verifier that holds values reads no padded proof, so by default this does nothing. + fn set_hidden(&mut self, hidden: bool) { + let _ = hidden; + } + /// The next `n` scalars. /// /// # Errors diff --git a/crates/fiat_shamir/src/transcript.rs b/crates/fiat_shamir/src/transcript.rs index 000ab0aac..848d390fb 100644 --- a/crates/fiat_shamir/src/transcript.rs +++ b/crates/fiat_shamir/src/transcript.rs @@ -80,6 +80,11 @@ pub trait Transmitter: Challenger { fn add_scalars(&mut self, xs: &[F192]); fn grind(&mut self, bits: u32); + /// Whether the scalars sent from now on travel under one-time-pad keys (doc `leanvm` §sec:zk). + /// + /// A prover holding no keys hides nothing. + fn set_hidden(&mut self, hidden: bool); + /// Transmit a root as its two scalars, not as a byte string. Sending it is what binds it: no verifier absorbs a root /// separately (see [`Receiver::next_root`], its mirror). fn add_root(&mut self, root: &Hash) { @@ -148,6 +153,14 @@ pub struct ProverState { fs: FiatShamirState, stream: Vec, merkle: Vec, + pad: Option, +} + +/// One-time-pad keys, one per hidden scalar, used in order. +struct Pad { + keys: Vec, + next: usize, + hidden: bool, } impl ProverState { @@ -166,6 +179,35 @@ impl ProverState { fs, stream: Vec::new(), merkle: Vec::new(), + pad: None, + } + } + + /// Hide each scalar sent while [`Transmitter::set_hidden`] holds under the next of these keys: the stream and the + /// transcript carry `x + key`. + /// + /// # Panics + /// + /// If keys were already given. + pub fn set_keys(&mut self, keys: Vec) { + assert!(self.pad.is_none(), "a prover takes its keys once"); + self.pad = Some(Pad { + keys, + next: 0, + hidden: false, + }); + } + + /// How many keys hidden scalars have used. + pub fn keys_used(&self) -> usize { + self.pad.as_ref().map_or(0, |p| p.next) + } + + /// The proof so far, which a verifier replays from the same seed. + pub fn snapshot(&self) -> ProofTranscript { + ProofTranscript { + stream: self.stream.clone(), + merkle: self.merkle.clone(), } } @@ -260,9 +302,18 @@ impl Transmitter for ProverState { } /// Transmit a scalar into the proof AND bind it into the state (the two are - /// inseparable: you cannot send without binding). + /// inseparable: you cannot send without binding). A hidden scalar travels + /// under its key. #[inline] fn add_scalar(&mut self, x: F192) { + let x = match &mut self.pad { + Some(pad) if pad.hidden => { + let key = *pad.keys.get(pad.next).expect("a key per hidden scalar"); + pad.next += 1; + x + key + } + _ => x, + }; self.fs.observe(x); self.stream.push(x); } @@ -283,6 +334,18 @@ impl Transmitter for ProverState { let nonce = self.fs.grind_pow(bits); self.stream.push(F192::new(nonce, 0, 0)); } + + fn set_hidden(&mut self, hidden: bool) { + if let Some(pad) = &mut self.pad { + pad.hidden = hidden; + } + } + + /// A root is public: it is never sent under a key. + fn add_root(&mut self, root: &Hash) { + assert!(!self.pad.as_ref().is_some_and(|p| p.hidden), "a root is never hidden"); + self.add_scalars(&hash_to_scalars(root)); + } } impl<'a> Receiver for VerifierState<'a> { diff --git a/crates/flock/benches/arithmetic_batch.rs b/crates/flock/benches/arithmetic_batch.rs index b1fbfdcd7..15381ae9e 100644 --- a/crates/flock/benches/arithmetic_batch.rs +++ b/crates/flock/benches/arithmetic_batch.rs @@ -126,6 +126,7 @@ fn bench(op: U64Op, quiet: bool) -> (usize, Timing) { &config, &[], std::slice::from_ref(&ring), + None, ); let open_s = t.elapsed().as_secs_f64(); let prove_s = t_prove.elapsed().as_secs_f64(); @@ -174,7 +175,8 @@ fn bench(op: U64Op, quiet: bool) -> (usize, Timing) { 1 << INITIAL_FOLDING_FACTOR, root, &[], - std::slice::from_ref(&ring) + std::slice::from_ref(&ring), + None ) .is_ok(), "stacked PCS opening verifies" diff --git a/crates/flock/benches/hash_batch.rs b/crates/flock/benches/hash_batch.rs index b4c9ebfd1..d48c6ed89 100644 --- a/crates/flock/benches/hash_batch.rs +++ b/crates/flock/benches/hash_batch.rs @@ -98,6 +98,7 @@ fn main() { &config, &[], std::slice::from_ref(&ring), + None, ); let open_s = t.elapsed().as_secs_f64(); let prove_s = t_prove.elapsed().as_secs_f64(); @@ -151,7 +152,8 @@ fn main() { 1 << INITIAL_FOLDING_FACTOR, root, &[], - std::slice::from_ref(&ring) + std::slice::from_ref(&ring), + None ) .is_ok(), "stacked PCS opening verifies" diff --git a/crates/flock/src/lincheck.rs b/crates/flock/src/lincheck.rs index 82e087b47..76979fb61 100644 --- a/crates/flock/src/lincheck.rs +++ b/crates/flock/src/lincheck.rs @@ -648,6 +648,18 @@ impl MatrixForm { .bilinear_form(self.alpha, &eq_inner, &w_col) .unwrap_or_else(|| inner_product(&circuit.fold_alpha_batched(self.alpha, &eq_inner), &w_col)) } + + /// The form's weight on each bit slice: [`Self::evaluate`] is `sum_i s_hat_v[i] weights[i]`, the form being linear + /// in its slices, and the weights depend on its other, public, coordinates alone. + pub fn slice_weights(&self, circuit: &dyn LincheckCircuit) -> Vec { + let n_slices = self.s_hat_v.len(); + let eq_inner = build_quirky_eq_table(self.z_skip, &self.x_inner_rest, n_slices.ilog2() as usize); + let marginal = circuit.fold_alpha_batched(self.alpha, &eq_inner); + let eq_rest = eq_table(&self.r_inner_rest); + (0..n_slices) + .map(|i| (eq_rest.iter().enumerate()).fold(F192::ZERO, |acc, (j, &e)| acc + e * marginal[j * n_slices + i])) + .collect() + } } /// What the deferred replay leaves to the circuit: the terminal identity holds exactly when the form takes the value. diff --git a/crates/leanvm/src/lib.rs b/crates/leanvm/src/lib.rs index 4837488da..c71ca262b 100644 --- a/crates/leanvm/src/lib.rs +++ b/crates/leanvm/src/lib.rs @@ -26,6 +26,12 @@ //! //! What a program reads there, it must check itself. //! +//! # Zero knowledge +//! +//! A plain proof is no secret: a verifier who can guess the advice recomputes the proof and compares. +//! A prover made with [`Prover::zk`] makes zero-knowledge proofs, which reveal nothing of the advice or the run beyond the statement and the run's shape (each table's height and the rate). +//! A program whose advice is private must therefore prove at a fixed public shape. +//! //! # Examples //! //! ```no_run @@ -44,8 +50,8 @@ //! Many proofs of one program aggregate into one proof through the aggregation module. pub use leanvm_core::{ - DecodeError, ElfError, InvalidRate, Output, Program, ProgramError, Proof, ProveError, ProvenRun, Prover, Rate, - Region, Stats, Trap, VerifyError, asm, + DecodeError, ElfError, InvalidRate, Output, Program, ProgramError, Proof, ProveError, ProvenRun, Prover, + Randomness, Rate, Region, Stats, Trap, VerifyError, asm, }; /// Aggregation trees: many proofs of one program, verified as one. diff --git a/crates/leanvm_core/Cargo.toml b/crates/leanvm_core/Cargo.toml index 250c1b2a5..1cb58d87b 100644 --- a/crates/leanvm_core/Cargo.toml +++ b/crates/leanvm_core/Cargo.toml @@ -17,6 +17,8 @@ pcs.workspace = true flock.workspace = true tracing.workspace = true thiserror.workspace = true +rand_chacha.workspace = true +rand_core.workspace = true [dev-dependencies] proptest.workspace = true diff --git a/crates/leanvm_core/src/cpu/deferred.rs b/crates/leanvm_core/src/cpu/deferred.rs index 7ac5ca0cb..bef1920fe 100644 --- a/crates/leanvm_core/src/cpu/deferred.rs +++ b/crates/leanvm_core/src/cpu/deferred.rs @@ -20,7 +20,8 @@ use crate::leaf; use crate::leaf::{BusVerify, N_TUPLE_BITS, SparseColumn}; use crate::rv::RiscvProgram; use crate::tables::{N_TABLES, Part}; -use fiat_shamir::arith::Arith; +use crate::zk::sym::{Recorder, Sym}; +use fiat_shamir::arith::{Arith, Verifier}; use flock::lincheck::{LincheckError, MatrixClaim, MatrixForm}; use flock::verifier::FlockError; use primitives::field::F192; @@ -232,6 +233,87 @@ impl Program { } Ok(()) } + + /// Settle the claims a zero-knowledge proof's core left, as constraints of the outer proof (doc `leanvm` §sec:zk). + /// + /// Every point is a challenge, so each claim's expected value is a public linear function of its hidden parts: the + /// program claim's twist and image weight, each circuit claim's bit slices. + /// + /// # Errors + /// + /// As [`Self::check_deferred`], a claim being malformed also when a coordinate that must be public is hidden. + pub(crate) fn check_deferred_hidden( + &self, + r: &mut Recorder, + claims: &DeferredClaims, + ) -> Result<(), CpuError> + where + Recorder: Verifier, + { + if claims.circuits.len() != N_FLOCKS { + return Err(CpuError::MalformedClaim(MalformedClaim::CircuitCount { + expected: N_FLOCKS, + got: claims.circuits.len(), + })); + } + + let point = &claims.program.point; + let malformed = CpuError::MalformedClaim(MalformedClaim::ProgramPoint); + let rv = self.rv(); + let kbc = crate::log2_strict_usize(rv.entries().len()); + let (Some(bytecode), Some(image_point)) = ( + Recorder::::publics(&point.bytecode), + Recorder::::publics(&point.image_point), + ) else { + return Err(malformed); + }; + if bytecode.len() != kbc + N_TUPLE_BITS || image_point.len() != rv.log_ram() || point.twist.len() > 64 { + return Err(malformed); + } + let (chi, alphas) = bytecode.split_at(kbc); + let weights = leaf::fingerprint_weights(alphas); + let terms = leaf::producer_twist_terms(&Lookup::Bytecode.tuple(rv), &weights, chi, point.twist.len()); + let image = SparseColumn::new(rv.log_ram(), &[(0, rv.image())]).eval(&image_point); + let mut expected = r.mul_const(point.image_weight, image); + for (&mu, &d) in point.twist.iter().zip(&terms) { + expected = r.mul_const_add(mu, d, expected); + } + r.ensure_eq(expected, claims.program.value, || { + CpuError::Constraint(ConstraintError::FinalMismatch) + })?; + + for (f, claim) in FlockId::ALL.into_iter().zip(&claims.circuits) { + let (table, part) = (f.table().name(), f.part()); + let form = &claim.point; + let malformed = CpuError::MalformedClaim(MalformedClaim::MatrixForm { table, part }); + let (Some([alpha, z_skip]), Some(x_inner_rest), Some(r_inner_rest)) = ( + Recorder::::publics(&[form.alpha, form.z_skip]).map(|v| [v[0], v[1]]), + Recorder::::publics(&form.x_inner_rest), + Recorder::::publics(&form.r_inner_rest), + ) else { + return Err(malformed); + }; + let public = MatrixForm { + alpha, + z_skip, + x_inner_rest, + r_inner_rest, + s_hat_v: vec![F192::ZERO; form.s_hat_v.len()], + }; + if !f.shape().fits(&public) { + return Err(malformed); + } + let zero = r.zero(); + let expected = (form.s_hat_v.iter().zip(public.slice_weights(f.circuit()))) + .fold(zero, |acc, (&s, w)| r.mul_const_add(s, w, acc)); + r.ensure_eq(expected, claim.value, || CpuError::Flock { + table, + part, + error: FlockError::Lincheck(LincheckError::SumcheckMismatch), + })?; + } + Ok(()) + } } #[cfg(test)] diff --git a/crates/leanvm_core/src/cpu/error.rs b/crates/leanvm_core/src/cpu/error.rs index c8954c8f9..7fd24abbe 100644 --- a/crates/leanvm_core/src/cpu/error.rs +++ b/crates/leanvm_core/src/cpu/error.rs @@ -96,6 +96,28 @@ pub enum CpuError { /// A deferred claim has no shape a proof of the program gives. #[error("the deferred claims: {0}")] MalformedClaim(MalformedClaim), + /// A zero-knowledge proof's padded transcript needs more keys than the key commitment holds. + #[error("the padded transcript takes {keys} keys, more than the {max} the key commitment holds")] + TooManyKeys { + /// The keys the transcript takes. + keys: usize, + /// The keys the commitment holds. + max: usize, + }, + /// A zero-knowledge proof's outer constraint system is larger than its mask allows. + #[error("the outer constraint system has 2^{log_rows} rows, more than 2^{max}")] + OuterSize { + /// The system's base-two logarithm of rows. + log_rows: usize, + /// The largest it may have. + max: usize, + }, + /// The key commitment's opening is rejected. + #[error("the key opening: {0}")] + KeyOpen(WhirError), + /// A zero-knowledge proof settles its deferred claims inside its outer proof, so it has no core to carry them out. + #[error("a zero-knowledge proof has no core to carry its claims out")] + ZkCore, } /// Why bytes decode to no proof. diff --git a/crates/leanvm_core/src/cpu/layout.rs b/crates/leanvm_core/src/cpu/layout.rs index 46274bf94..eddd2e166 100644 --- a/crates/leanvm_core/src/cpu/layout.rs +++ b/crates/leanvm_core/src/cpu/layout.rs @@ -752,18 +752,7 @@ impl Announcement { /// /// Refuses a non-canonical size, a final clock that is not live, a table height or a rate outside its range. pub(crate) fn decode(scalars: &[F192; Self::LEN]) -> Result { - // A size is a canonical integer in the first coordinate. - let size = |x: &F192| -> Result { - if x.c1 != 0 || x.c2 != 0 { - return Err(CpuError::NonCanonicalSize); - } - usize::try_from(x.c0).map_err(|_| CpuError::NonCanonicalSize) - }; - let mut taus = PerTable::default(); - for (t, x) in TableId::ALL.into_iter().zip(scalars) { - taus[t] = size(x)?; - } - let log_inv_rate = size(&scalars[N_TABLES])?; + let (taus, log_inv_rate) = Self::decode_sizes(&scalars[..=N_TABLES])?; // A live clock at slot zero: neither a padding row's clock nor a failed row's can end the run. let ts_final = scalars[N_TABLES + 1]; @@ -773,18 +762,58 @@ impl Announcement { } Layout::check_heights(&taus)?; - - // A rate the commitment supports. - let rate = (u8::try_from(log_inv_rate).ok()) - .and_then(|r| Rate::new(r).ok()) - .ok_or(CpuError::Rate { log_inv_rate })?; Ok(Self { taus, - rate, + rate: Self::decode_rate(log_inv_rate)?, ts_final: ts_final.c0, }) } + /// Write a zero-knowledge proof's announcement: its shape alone, each table's height then the rate, its final clock + /// being hidden. + pub(crate) fn write_shape(taus: &PerTable, rate: Rate, ps: &mut ProverState) { + for size in Self::sizes(taus, rate) { + ps.add_scalar(size); + } + } + + /// Read a zero-knowledge proof's announcement, its shape, and check it as [`Self::decode`] does. + /// + /// # Errors + /// + /// Refuses a short stream, a non-canonical size, a table height or a rate outside its range. + pub(crate) fn read_shape(v: &mut V) -> Result<(PerTable, Rate), CpuError> + where + V: fiat_shamir::arith::Verifier, + { + let scalars = v.next_scalars(N_TABLES + 1)?; + let (taus, log_inv_rate) = Self::decode_sizes(&scalars)?; + Layout::check_heights(&taus)?; + Ok((taus, Self::decode_rate(log_inv_rate)?)) + } + + /// Each table's height, then the rate's logarithm, each a canonical integer in the first coordinate. + fn decode_sizes(scalars: &[F192]) -> Result<(PerTable, usize), CpuError> { + let size = |x: &F192| -> Result { + if x.c1 != 0 || x.c2 != 0 { + return Err(CpuError::NonCanonicalSize); + } + usize::try_from(x.c0).map_err(|_| CpuError::NonCanonicalSize) + }; + let mut taus = PerTable::default(); + for (t, x) in TableId::ALL.into_iter().zip(scalars) { + taus[t] = size(x)?; + } + Ok((taus, size(&scalars[N_TABLES])?)) + } + + /// A rate the commitment supports. + fn decode_rate(log_inv_rate: usize) -> Result { + (u8::try_from(log_inv_rate).ok()) + .and_then(|r| Rate::new(r).ok()) + .ok_or(CpuError::Rate { log_inv_rate }) + } + /// The layout the announced heights describe for `p`, its final clock zero. /// /// The verifier adds the announced clock's share itself. @@ -806,11 +835,33 @@ impl Layout { pub(crate) fn announced(p: &RiscvProgram, taus: PerTable) -> Result { Self::check_heights(&taus)?; // The caps bound each height alone; the stacked size they imply is checked here. - let layout = Self::new(p, taus, 0); - if !(pcs::MIN_MU..=pcs::MAX_MU).contains(&layout.shape.mu) { - return Err(CpuError::WitnessSize { mu: layout.shape.mu }); + Self::new(p, taus, 0).checked() + } + + /// The layout a verifier rebuilds from a zero-knowledge proof's announced heights: the same columns, in the stack a + /// zero-knowledge proof commits. + /// + /// # Errors + /// + /// As [`Self::announced`]. + pub(crate) fn announced_hiding(p: &RiscvProgram, taus: PerTable) -> Result { + Self::check_heights(&taus)?; + Self::new(p, taus, 0).hiding().checked() + } + + /// The same columns, in the stack a zero-knowledge proof commits: lanes long enough to hide, then a random lane. + pub(crate) fn hiding(self) -> Self { + let shape = StackShape::hiding(witness::committed_len(&self.placements)); + Self { shape, ..self } + } + + /// The layout, if the commitment takes its stack. + fn checked(self) -> Result { + if (pcs::MIN_MU..=pcs::MAX_MU).contains(&self.shape.mu) { + Ok(self) + } else { + Err(CpuError::WitnessSize { mu: self.shape.mu }) } - Ok(layout) } /// Check each table's height lies between flock's instance floor and the public cap. diff --git a/crates/leanvm_core/src/cpu/mod.rs b/crates/leanvm_core/src/cpu/mod.rs index af6f8442b..39166e988 100644 --- a/crates/leanvm_core/src/cpu/mod.rs +++ b/crates/leanvm_core/src/cpu/mod.rs @@ -29,6 +29,7 @@ mod proof; mod prover; mod reduce; mod witness; +mod zk; pub use deferred::{Claim, DeferredClaims, MalformedClaim, ProgramPoint}; pub use error::{CpuError, DecodeError, ProveError, VerifyError}; diff --git a/crates/leanvm_core/src/cpu/program.rs b/crates/leanvm_core/src/cpu/program.rs index 8a7c6cd52..9d63ad96e 100644 --- a/crates/leanvm_core/src/cpu/program.rs +++ b/crates/leanvm_core/src/cpu/program.rs @@ -13,9 +13,10 @@ use super::witness::Witness; use super::{Output, Proof}; use crate::class_flock::FlockId; use crate::constraints::{Claims, Columns}; -use crate::pcs::Rate; +use crate::pcs::{Rate, RingSwitch, StackClaim}; use crate::rv::{ElfError, Guest, Machine, ProgramError, Region, RiscvProgram}; use crate::tables::{ClassTable, Clock, PerTable, TableId}; +use crate::zk::randomness::Randomness; use crate::{constraints, leaf, pcs}; use fiat_shamir::arith::Native; use fiat_shamir::transcript::{Challenger, ProverState, RawProof, Transmitter, VerifierState}; @@ -44,6 +45,9 @@ impl Program { /// The domain separator of the digest, versioned with the statement's format. const DIGEST_DOMAIN: &'static [u8] = b"leanvm-rv64im-11"; + /// The domain a zero-knowledge proof's transcript seed is hashed under, with the protocol's version. + const ZK_DOMAIN: &'static [u8] = b"leanvm-rv64im-zk"; + /// The cycles between two checks of a running trace against one commitment. const SIZE_CHECK_PERIOD: u64 = 1 << 16; @@ -207,16 +211,16 @@ impl Program { }) } - /// Prove a finished run, which a test may have forged. - pub(super) fn prove_execution(&self, exec: &Execution, rate: Rate) -> (Proof, Stats) { - let w = crate::stage!("Build witness", || Witness::build(self, exec)); + /// Prove a finished run, which a test may have forged, in zero knowledge when given its randomness. + pub(super) fn prove_execution(&self, exec: &Execution, rate: Rate, zk: Option) -> (Proof, Stats) { + let w = crate::stage!("Build witness", || Witness::build_for(self, exec, zk.is_some())); let stats = Stats { proven_rows: exec.proven_rows, counts: w.layout.taus.map(|t| 1usize << t), base_counts: exec.base_counts, committed: w.committed_size(), }; - (self.prove_witness(w, Output::new(exec.output), rate), stats) + (self.prove_witness(w, Output::new(exec.output), rate, zk), stats) } /// Prove a built witness, which a test may have forged. @@ -224,7 +228,10 @@ impl Program { /// # Panics /// /// Panics if the witness's bus does not balance: an honest run's always does. - fn prove_witness(&self, w: Witness, output: Output, rate: Rate) -> Proof { + fn prove_witness(&self, mut w: Witness, output: Output, rate: Rate, zk: Option) -> Proof { + if let Some(randomness) = zk { + return super::zk::prove(self, w, output, rate, randomness); + } // The public statement, the program's digest and the output, seeds the transcript. let mut ps = ProverState::new(self.fs_seed(), output.words().map(F64)); @@ -237,7 +244,21 @@ impl Program { }; announcement.write(&mut ps); let committed = crate::stage!("Commit", || pcs::commit(&mut ps, &w.q, w.layout.shape, log_inv_rate)); + let (slots, rings) = self.prove_reductions(&mut ps, &mut w, output); + crate::stage!("PCS open", || pcs::open( + &mut ps, &committed, &w.q, &slots, &rings, None + )); + Proof(ps.into_proof(), false) + } + /// The bus, the table sumcheck and flock's reductions over the committed witness: the opening's point claims and its + /// ring-switched regions. + pub(super) fn prove_reductions( + &self, + ps: &mut ProverState, + w: &mut Witness, + output: Output, + ) -> (Vec, Vec) { // The bus, then the linear tables' columns at its point, then the one batch over the other tables and the // producers, all reading the stack's windows in place. let spans = &Schema::get().spans; @@ -245,15 +266,7 @@ impl Program { let l = &w.layout; let cols = w.columns(); let mut bus = crate::stage!("Prove bus", || { - leaf::prove_balance( - &l.push, - &l.pull, - &l.producers, - l.grinding, - &cols, - spans.as_slice(), - &mut ps, - ) + leaf::prove_balance(&l.push, &l.pull, &l.producers, l.grinding, &cols, spans.as_slice(), ps) }); // A settled table's columns at the bus point, short of its register numbers, which the batch folds. let settled: Vec = (ClassTable::all().iter()) @@ -288,7 +301,7 @@ impl Program { .chain(producers.into_iter().map(|p| Columns::E(p.columns))) .collect(); let batch = Batch::new(l, &bus.forms, &coefficients, &bus.weights, bus.beta, powers); - constraints::prove(batch.airs(), table_cols, &bus.point, &sums, &mut ps) + constraints::prove(batch.airs(), table_cols, &bus.point, &sums, ps) }); (bus.claims, TableClaims::new(settled, summed)) }; @@ -304,7 +317,7 @@ impl Program { // // Each circuit leaves a validity claim on its packed witness, discharged in the same opening through a ring-switched region. // Each producer's multiplicity column is a ring-switched region too. - let reductions = w.reductions; + let reductions = std::mem::take(&mut w.reductions); let slices = crate::stage!("Flock reductions", || { let instances: Vec> = (FlockId::ALL.into_iter().zip(&reductions)) .map(|(f, tables)| { @@ -313,12 +326,11 @@ impl Program { f.instance(column, l.taus[f.table()], tables) }) .collect(); - reduction::prove(&instances, &mut ps) + reduction::prove(&instances, ps) }); drop(reductions); let rings = l.rings(slices, &table_claims.producers, &table_claims.summed, F192::ZERO); - crate::stage!("PCS open", || pcs::open(&mut ps, &committed, &w.q, &slots, &rings)); - Proof(ps.into_proof()) + (slots, rings) } /// Check that the proof shows this program, run on some advice, exiting with this output. @@ -332,6 +344,9 @@ impl Program { /// The proof is not one of this program and this output. #[tracing::instrument(name = "Verify", skip_all)] pub fn verify(&self, output: Output, proof: &Proof) -> Result<(), VerifyError> { + if proof.is_zk() { + return Ok(super::zk::verify(self, output, proof).map(drop)?); + } let claims = self.verify_core(output, proof)?; Ok(self.check_deferred(&claims)?) } @@ -344,11 +359,25 @@ impl Program { #[tracing::instrument(name = "Verify", skip_all)] #[doc(hidden)] pub fn verify_to_raw(&self, output: Output, proof: &Proof) -> Result { + if proof.is_zk() { + return super::zk::verify(self, output, proof); + } let (claims, raw) = self.replay(output, proof)?; self.check_deferred(&claims)?; Ok(raw) } + /// Verify a zero-knowledge proof and render the outer constraint system its verifier recorded, the form the Python + /// verifier renders too. + /// + /// # Errors + /// + /// Returns the first stage that refuses the proof. + #[doc(hidden)] + pub fn zk_constraints(&self, output: Output, proof: &Proof) -> Result { + super::zk::render_constraints(self, output, proof) + } + /// The verifier's core: every check that depends on the proof. /// /// It returns the claims the proof leaves on polynomials only the program or the VM's circuits fix. @@ -357,7 +386,8 @@ impl Program { /// /// # Errors /// - /// Returns the first stage that refuses the proof. + /// Returns the first stage that refuses the proof, and refuses a zero-knowledge proof, whose claims are settled + /// inside its outer proof. #[doc(hidden)] pub fn verify_core(&self, output: Output, proof: &Proof) -> Result { self.replay(output, proof).map(|(claims, _)| claims) @@ -366,6 +396,9 @@ impl Program { /// The verifier's core, and the proof it replayed with its Merkle paths written out. #[tracing::instrument(name = "Verify core", skip_all)] fn replay(&self, output: Output, proof: &Proof) -> Result<(DeferredClaims, RawProof), CpuError> { + if proof.is_zk() { + return Err(CpuError::ZkCore); + } // The public statement seeds the transcript, as on the prover's side. let mut vs = VerifierState::new(self.fs_seed(), &proof.0, output.words().map(F64)); @@ -400,6 +433,20 @@ impl Program { fiat_shamir::digest_words(&self.digest) } + /// The transcript's seed for a proof of either kind. + /// + /// A zero-knowledge proof's is the digest hashed under its protocol's own domain, so no challenge of one kind of proof is ever one of the other. + pub(super) fn seed(&self, zk: bool) -> [F64; 4] { + if !zk { + return self.fs_seed(); + } + let mut h = Hasher::new(); + h.update(Self::ZK_DOMAIN); + h.update(&Proof::ZK_VERSION.to_le_bytes()); + h.update(&self.digest); + fiat_shamir::digest_words(&h.finalize()) + } + /// The committed size of a run making these rows per table, each table taken at its provable height. /// /// The layout depends on the program and the heights alone, so no witness is built. @@ -641,7 +688,7 @@ mod tests { /// The prover refuses a witness whose bus does not balance: its two products differ. fn assert_unbalanced(program: &Program, w: Witness, output: Output) { - let refused = std::panic::catch_unwind(AssertUnwindSafe(|| program.prove_witness(w, output, Rate::MIN))) + let refused = std::panic::catch_unwind(AssertUnwindSafe(|| program.prove_witness(w, output, Rate::MIN, None))) .expect_err("an unbalanced bus was proven"); let message = refused.downcast_ref::().map(String::as_str).unwrap_or(""); assert!( @@ -791,7 +838,7 @@ mod tests { ); column_mut(&mut w, jump_column())[row] = F64(value); assert!(unmatched(&w).is_empty()); - let proof = program.prove_witness(w, forged.output.into(), Rate::MIN); + let proof = program.prove_witness(w, forged.output.into(), Rate::MIN, None); program .verify_core(forged.output.into(), &proof) .expect_err("a forged successor is refused") @@ -1044,7 +1091,7 @@ mod tests { let w = Witness::build(program, exec); let unmatched = unmatched(&w); assert!(unmatched.is_empty(), "the forged run balances: {unmatched:?}"); - let proof = program.prove_witness(w, exec.output.into(), Rate::MIN); + let proof = program.prove_witness(w, exec.output.into(), Rate::MIN, None); program.verify_to_raw(exec.output.into(), &proof).map(drop) } @@ -1258,7 +1305,7 @@ mod tests { let program = Program::new(&text, Region::TEXT.base(), vec![], 2, 0).expect("valid instruction program"); let honest = program.execute(&[]).unwrap(); assert_eq!(honest.output, [12, 0, 0, 0]); - let (proof, _) = program.prove_execution(&honest, Rate::MIN); + let (proof, _) = program.prove_execution(&honest, Rate::MIN, None); program .verify(honest.output.into(), &proof) .expect("the honest run verifies"); @@ -1401,7 +1448,7 @@ mod tests { unmatched(&w).is_empty(), "the bus reads the register numbers, not the word" ); - let proof = program.prove_witness(w, exec.output.into(), Rate::MIN); + let proof = program.prove_witness(w, exec.output.into(), Rate::MIN, None); assert!( matches!( program.verify_to_raw(exec.output.into(), &proof), @@ -1526,7 +1573,7 @@ mod tests { (forged.trace.reg_ts[sink], forged.trace.reg_fin[sink]) = (F64(Clock::SEED_CLOCK), F64::ZERO); forged.trace.ts_final |= 1 << Clock::FAIL_BIT; assert!(unmatched_run(&program, &forged).is_empty()); - let (proof, _) = program.prove_execution(&forged, Rate::MIN); + let (proof, _) = program.prove_execution(&forged, Rate::MIN, None); assert_eq!( program.verify(forged.output.into(), &proof), Err(CpuError::FinalClock.into()) diff --git a/crates/leanvm_core/src/cpu/proof.rs b/crates/leanvm_core/src/cpu/proof.rs index 71b707502..e5cc3de9c 100644 --- a/crates/leanvm_core/src/cpu/proof.rs +++ b/crates/leanvm_core/src/cpu/proof.rs @@ -9,9 +9,9 @@ use std::fmt::{self, Debug, Formatter}; /// /// The program checks it against the output. /// -/// It travels as bytes. +/// It travels as bytes. A zero-knowledge proof (doc `leanvm` §sec:zk) says the same and reveals nothing else of the run than its public shape. #[derive(Clone, PartialEq, Eq)] -pub struct Proof(#[doc(hidden)] pub ProofTranscript); +pub struct Proof(#[doc(hidden)] pub ProofTranscript, pub(crate) bool); impl Proof { /// The header of a proof's bytes: the magic `LVMP`, then the protocol version. @@ -19,10 +19,29 @@ impl Proof { /// The version is bumped by every change to what a proof says. const ENVELOPE: Envelope = Envelope::new(*b"LVMP", 13); + /// The header of a zero-knowledge proof's bytes: the magic `LVMZ`, then its protocol version. + /// + /// The magic is the envelope's zero-knowledge bit: a proof of either kind is refused as the other. + const ZK_ENVELOPE: Envelope = Envelope::new(*b"LVMZ", Self::ZK_VERSION); + + /// The zero-knowledge protocol's version, which also separates its transcript's seed. + pub(crate) const ZK_VERSION: u16 = 15; + + /// Whether the proof is zero knowledge. + #[must_use] + pub const fn is_zk(&self) -> bool { + self.1 + } + + /// The envelope a proof of this kind travels in. + const fn envelope(zk: bool) -> Envelope { + if zk { Self::ZK_ENVELOPE } else { Self::ENVELOPE } + } + /// The proof's bytes. #[must_use] pub fn to_bytes(&self) -> Vec { - Self::ENVELOPE.seal(&self.0.to_bytes()) + Self::envelope(self.1).seal(&self.0.to_bytes()) } /// The proof these bytes encode. @@ -32,10 +51,11 @@ impl Proof { /// - Bytes that are no proof. /// - A proof of another protocol version. pub fn from_bytes(bytes: &[u8]) -> Result { - // The header first: a foreign version is refused before its body is read. - let body = Self::ENVELOPE.open(bytes)?; + // The magic picks the kind, then the header is checked whole: a foreign version is refused before its body is read. + let zk = bytes.starts_with(&Self::ZK_ENVELOPE.magic()); + let body = Self::envelope(zk).open(bytes)?; ProofTranscript::from_bytes(body) - .map(Self) + .map(|t| Self(t, zk)) .ok_or(DecodeError::Malformed) } } diff --git a/crates/leanvm_core/src/cpu/prover.rs b/crates/leanvm_core/src/cpu/prover.rs index 6e0075c5d..92a0e090c 100644 --- a/crates/leanvm_core/src/cpu/prover.rs +++ b/crates/leanvm_core/src/cpu/prover.rs @@ -2,13 +2,19 @@ use super::{Output, Program, Proof, ProveError, Stats}; use crate::pcs::Rate; +use crate::zk::randomness::Randomness; -/// A prover: it proves runs at one commitment rate. +/// A prover: it proves runs at one commitment rate, in zero knowledge or not. /// /// The rate trades proving time for proof size. /// /// The verifier needs no rate: each proof announces its own. /// +/// # Zero knowledge +/// +/// A zero-knowledge proof (doc `leanvm` §sec:zk) hides the advice and the run, but not the run's shape: each table's height and the rate are public. +/// A program whose advice is private must prove at a fixed public shape, so that its heights say nothing about the advice. +/// /// # Performance /// /// A proof touches gigabytes of memory, and frees it before returning. @@ -22,6 +28,8 @@ use crate::pcs::Rate; pub struct Prover { /// The commitment rate every proof is made at. rate: Rate, + /// Where a zero-knowledge proof draws its randomness, for a zero-knowledge prover. + zk: Option, } impl Prover { @@ -32,7 +40,16 @@ impl Prover { pub fn new(rate: Rate) -> Self { // Spawning up front keeps the spawn cost out of the first proof. crate::init_prover(); - Self { rate } + Self { rate, zk: None } + } + + /// The same prover, making zero-knowledge proofs from this randomness. + #[must_use] + pub const fn zk(self, randomness: Randomness) -> Self { + Self { + rate: self.rate, + zk: Some(randomness), + } } /// The commitment rate every proof is made at. @@ -41,6 +58,12 @@ impl Prover { self.rate } + /// Whether the prover makes zero-knowledge proofs. + #[must_use] + pub const fn is_zk(&self) -> bool { + self.zk.is_some() + } + /// Run the program on the advice, and prove the run. /// /// # Arguments @@ -53,11 +76,11 @@ impl Prover { /// - The run traps. /// - The run is longer than one proof holds. /// - The advice is longer than the program's region. - #[tracing::instrument(name = "Prove", skip_all, fields(log_inv_rate = self.rate.log_inv_rate()))] + #[tracing::instrument(name = "Prove", skip_all, fields(log_inv_rate = self.rate.log_inv_rate(), zk = self.is_zk()))] pub fn prove(&self, program: &Program, advice: &[u64]) -> Result { let exec = crate::stage!("Execute program", || program.execute(advice))?; program.committed_size(exec.trace.row_counts())?; - let (proof, stats) = program.prove_execution(&exec, self.rate); + let (proof, stats) = program.prove_execution(&exec, self.rate, self.zk); Ok(ProvenRun { proof, output: Output::new(exec.output), diff --git a/crates/leanvm_core/src/cpu/reduce.rs b/crates/leanvm_core/src/cpu/reduce.rs index d9172c5e8..09d7e264b 100644 --- a/crates/leanvm_core/src/cpu/reduce.rs +++ b/crates/leanvm_core/src/cpu/reduce.rs @@ -67,6 +67,24 @@ impl Layout { rate: Rate, ) -> Result, CpuError> { let root = pcs::read_commitment(v)?; + self.verify_committed(v, root, clock, output, rate) + } + + /// The verifier's core past the commitment's root: the bus and the tables, the flock reductions and the opening. + /// + /// A zero-knowledge layout's opening is the hiding one, whose lane rounds end the hidden transcript. + /// + /// # Errors + /// + /// Returns the first stage that refuses the proof. + pub(crate) fn verify_committed( + &self, + v: &mut V, + root: V::Root, + clock: V::E, + output: &[V::E; 4], + rate: Rate, + ) -> Result, CpuError> { let reduced = v.scope("bus and tables", |v| self.reduce_tables(v, clock, output))?; // Flock's reductions, batched over every class circuit then every clock circuit, each leaving its matrices' form to its circuit. diff --git a/crates/leanvm_core/src/cpu/witness.rs b/crates/leanvm_core/src/cpu/witness.rs index b74058767..f3c9b72de 100644 --- a/crates/leanvm_core/src/cpu/witness.rs +++ b/crates/leanvm_core/src/cpu/witness.rs @@ -29,11 +29,19 @@ pub(crate) struct Witness { impl Witness { /// The witness of a finished run. + #[cfg(test)] + pub(crate) fn build(program: &Program, exec: &Execution) -> Self { + Self::build_for(program, exec, false) + } + + /// The witness of a finished run, in the stack a zero-knowledge proof commits when `hiding`. + /// + /// A hiding stack's last lane is left zero, for the prover to fill with its randomness. /// /// # Panics /// /// Panics if a table's rows are not a power of two at flock's floor: the fill blocks failed to fill it. - pub(crate) fn build(program: &Program, exec: &Execution) -> Self { + pub(crate) fn build_for(program: &Program, exec: &Execution, hiding: bool) -> Self { let (p, trace, schema) = (&program.rv, &exec.trace, Schema::get()); // Every table's rows are real, filled to a power of two at flock's floor, so its height is its row count. @@ -61,6 +69,7 @@ impl Witness { // The public layout comes first: it fixes each column's length, so each is allocated once. let layout = Layout::new(p, taus, trace.ts_final); + let layout = if hiding { layout.hiding() } else { layout }; // The stack is written exactly once: one window per committed column, each filled in place. let mut q = Box::new_uninit_slice(layout.shape.committed_len()); diff --git a/crates/leanvm_core/src/cpu/zk.rs b/crates/leanvm_core/src/cpu/zk.rs new file mode 100644 index 000000000..c85a04177 --- /dev/null +++ b/crates/leanvm_core/src/cpu/zk.rs @@ -0,0 +1,325 @@ +//! Zero-knowledge proofs of a run (doc `leanvm` §sec:zk): the plain proof under one-time pads on a hiding commitment, then an outer proof that the padded transcript passes the verifier's checks. +//! +//! After the zero-knowledge seed, the transcript is: +//! +//! ```text +//! clear each table's height and the rate: the run's public shape +//! clear the stack's root (every lane padded, one uniform lane last), then the key commitment's root +//! hidden the final clock's free bits, the bus, the table sumcheck, flock's reductions, the opening's lane rounds +//! clear the opening's claim after its lane fold, its padding's fold, the rest of the opening +//! hidden each product and inverse of hidden values the verifier makes +//! clear the outer proof, then the key commitment's opening +//! ``` +//! +//! A hidden scalar travels under the next key. The verifier runs its own code over the padded transcript with the recording arithmetic of [`crate::zk::sym`], and the outer proof shows the keys satisfy what it recorded. + +use super::layout::{Announcement, Layout}; +use super::witness::Witness; +use super::{CpuError, Output, Program, Proof}; +use crate::pcs::{self, LOG_BATCH, Rate}; +use crate::tables::Clock; +use crate::zk::keys::{self, KEY_MU, KeyStack, LANE, MAX_KEYS, MAX_OUTER_LOG_ROWS}; +use crate::zk::outer::constraint_system; +use crate::zk::r1cs::R1cs; +use crate::zk::randomness::{Purpose, Randomness, ZkRng}; +use crate::zk::spartan::{self, OuterClaims, SpartanError}; +use crate::zk::sym::{Form, Kind, Record, Recorder, Sym, Var}; +use ::pcs::verifier::OpeningVerifier; +use ::pcs::whir::{self, Hiding, ProverData, WhirError, config_for_rate_hiding}; +use fiat_shamir::arith::{Arith, Verifier}; +use fiat_shamir::merkle::Hash; +use fiat_shamir::transcript::{Challenger, ProverState, RawProof, Transmitter, VerifierState}; +use primitives::field::{F64, F192}; +use primitives::multilinear::{eq_table, inner_product}; +use std::ops::Range; + +/// The final clock's bits a run may set: past its slot's bits and below its live bit, which is set (§sec:state). +const FREE_CLOCK_BITS: Range = Clock::SLOT_BITS as usize..Clock::LIVE_BIT as usize; + +/// Prove a built witness in zero knowledge. +/// +/// # Panics +/// +/// Panics if the witness's bus does not balance, or if its padded transcript outgrows the key commitment. +pub(super) fn prove(program: &Program, mut w: Witness, output: Output, rate: Rate, randomness: Randomness) -> Proof { + let rng = ZkRng::new(randomness); + let log_inv_rate = rate.log_inv_rate().into(); + let seed = program.seed(true); + let public = output.words().map(F64); + let mut ps = ProverState::new(seed, public); + Announcement::write_shape(&w.layout.taus, rate, &mut ps); + + // The stack, its last lane uniform and every lane padded, then the keys, before any challenge. + let shape = w.layout.shape; + let committed = crate::stage!("Commit", || { + let lane = 1usize << (shape.mu - LOG_BATCH); + rng.fill_k(Purpose::RandomLane, &mut w.q[shape.n_lanes * lane..]); + let mut pads = vec![F64::ZERO; shape.committed_lanes() * pcs::padding(shape.mu, log_inv_rate)]; + rng.fill_k(Purpose::Pads, &mut pads); + pcs::commit_hiding(&mut ps, &w.q, shape, log_inv_rate, &pads) + }); + let stack = KeyStack::draw(&rng); + let key_data = crate::stage!("Commit keys", || { + let mut pads = vec![F64::ZERO; 2 * pcs::padding(KEY_MU, log_inv_rate)]; + rng.fill_k(Purpose::KeyPads, &mut pads); + let (commitment, data) = whir::commit_hiding(&stack.words, KEY_MU, LOG_BATCH, log_inv_rate, &pads); + ps.add_root(&commitment.root); + data + }); + + // The plain proof, every scalar it sends padded until its opening's lane fold ends. + ps.set_keys(stack.keys().to_vec()); + ps.set_hidden(true); + for bit in FREE_CLOCK_BITS { + ps.add_scalar(F192::from(F64(w.ts_final >> bit & 1))); + } + let (slots, rings) = program.prove_reductions(&mut ps, &mut w, output); + let hiding = Hiding { + k: pcs::padding(shape.mu, log_inv_rate), + hidden_claim: true, + }; + crate::stage!("PCS open", || pcs::open( + &mut ps, + &committed, + &w.q, + &slots, + &rings, + Some(hiding) + )); + drop((committed, w, slots, rings)); + + // The verifier's record of the padded transcript, which the prover replays knowing the keys. + let (record, n_keys) = crate::stage!("Record", || { + let snapshot = ps.snapshot(); + let mut rec = Recorder::with_keys(VerifierState::new(seed, &snapshot, public), stack.keys().to_vec()); + record(program, &mut rec, output).expect("the prover's own proof verifies"); + let n_keys = rec.n_keys() as usize; + (rec.finish_record().1, n_keys) + }); + // The auxiliary variables' values, in the outer system's order, each under its key. + let sent: Vec = (record.aux_order().iter()) + .map(|&j| record.aux_values[j as usize]) + .collect(); + assert!( + n_keys + sent.len() <= MAX_KEYS, + "the padded transcript outgrows the key commitment" + ); + ps.set_hidden(true); + ps.add_scalars(&sent); + ps.set_hidden(false); + let keys = stack.keys(); + let aux: Vec
= (sent.iter().enumerate()) + .map(|(r, &value)| aux_form(value + keys[n_keys + r], n_keys + r)) + .collect(); + + // The outer proof, then the key commitment's opening. + crate::stage!("Outer proof", || { + let r1cs = constraint_system(&record, &aux); + assert!( + r1cs.log_rows() <= MAX_OUTER_LOG_ROWS, + "the outer system outgrows its mask" + ); + let claims = spartan::prove(&mut ps, &r1cs, &stack.z(), stack.libra(r1cs.log_rows())); + open_keys(&mut ps, &stack, &key_data, &claims, log_inv_rate); + }); + Proof(ps.into_proof(), true) +} + +/// Verify a zero-knowledge proof, and return it with every query's Merkle path written out. +/// +/// # Errors +/// +/// Returns the first stage that refuses the proof. +pub(super) fn verify(program: &Program, output: Output, proof: &Proof) -> Result { + verify_recorded(program, output, proof).map(|(raw, _, _)| raw) +} + +/// Verify a zero-knowledge proof, and return it with every query's Merkle path written out, with what the verifier +/// recorded and the outer constraint system it stated. +fn verify_recorded(program: &Program, output: Output, proof: &Proof) -> Result<(RawProof, Record, R1cs), CpuError> { + let vs = VerifierState::new(program.seed(true), &proof.0, output.words().map(F64)); + let mut rec = Recorder::new(vs); + let (key_root, rate) = record(program, &mut rec, output)?; + + // The auxiliary variables, each a hidden scalar. + let keys = (rec.n_keys() + rec.n_aux()) as usize; + if keys > MAX_KEYS { + return Err(CpuError::TooManyKeys { keys, max: MAX_KEYS }); + } + rec.set_hidden(true); + let mut aux = Vec::with_capacity(rec.n_aux() as usize); + for _ in 0..rec.n_aux() { + let s = rec.next_scalar()?; + aux.push(rec.form(s)); + } + rec.set_hidden(false); + let (mut vs, record) = rec.finish_record(); + + let r1cs = constraint_system(&record, &aux); + if r1cs.log_rows() > MAX_OUTER_LOG_ROWS { + return Err(CpuError::OuterSize { + log_rows: r1cs.log_rows(), + max: MAX_OUTER_LOG_ROWS, + }); + } + let claims = spartan::verify(&mut vs, &r1cs).map_err(|SpartanError::Transcript(e)| CpuError::Transcript(e))?; + verify_keys(&mut vs, key_root, &claims, rate.log_inv_rate().into()).map_err(CpuError::KeyOpen)?; + vs.finish()?; + Ok((vs.into_raw_proof(), record, r1cs)) +} + +/// What the verifier of a zero-knowledge proof recorded, one line each, for the Python verifier to state the same: the +/// key and variable counts, each auxiliary variable's digest and kind in the outer system's order, then each linear +/// constraint's digest, then each bit's. +/// +/// # Errors +/// +/// Returns the first stage that refuses the proof. +pub(super) fn render_constraints(program: &Program, output: Output, proof: &Proof) -> Result { + let (_, record, r1cs) = verify_recorded(program, output, proof)?; + let hex = |d: &[u8; 32]| d.iter().map(|b| format!("{b:02x}")).collect::(); + let mut lines = vec![ + format!("keys {}", record.n_keys), + format!("auxiliary {}", record.aux.len()), + format!("rows {}", r1cs.n_rows()), + ]; + for j in record.aux_order() { + let aux = &record.aux[j as usize]; + let kind = match aux.kind { + Kind::Product => "product", + Kind::Inverse => "inverse", + Kind::Bind => "bind", + }; + lines.push(format!("{kind} {}", hex(&aux.digest))); + } + let sorted = |list: &[([u8; 32], Form)]| { + let mut digests: Vec<[u8; 32]> = list.iter().map(|(d, _)| *d).collect(); + digests.sort_unstable(); + digests + }; + lines.extend(sorted(&record.linear).iter().map(|d| format!("linear {}", hex(d)))); + lines.extend(sorted(&record.booleans).iter().map(|d| format!("bit {}", hex(d)))); + Ok(lines.join("\n")) +} + +/// The plain verifier over a padded transcript, recorded: the shape, the two roots, the final clock's bits, the core, +/// then the deferred claims. It returns the key commitment's root and the rate. +fn record(program: &Program, rec: &mut Recorder, output: Output) -> Result<(Hash, Rate), CpuError> +where + T: OpeningVerifier, +{ + let (taus, rate) = Announcement::read_shape(rec.transport())?; + let layout = Layout::announced_hiding(program.rv(), taus)?; + let root = rec.next_root()?; + let key_root = rec.next_root()?; + + // The final clock: its live bit, and each free bit hidden and a bit. + rec.set_hidden(true); + let mut clock = Sym::Pub(F192::from(F64(1 << Clock::LIVE_BIT))); + for bit in FREE_CLOCK_BITS { + let b = rec.next_scalar()?; + rec.boolean(b); + clock = rec.mul_const_add(b, F192::from(F64(1 << bit)), clock); + } + let output = output.words().map(|o| Sym::Pub(F192::from(F64(o)))); + let claims = layout.verify_committed(rec, root, clock, &output, rate)?; + program.check_deferred_hidden(rec, &claims)?; + Ok((key_root, rate)) +} + +/// The form of the auxiliary value sent as `sent` under key `key`. +fn aux_form(sent: F192, key: usize) -> Form { + Form { + constant: sent, + terms: vec![(Var::Key(u32::try_from(key).expect("a key index fits a u32")), F192::ONE)], + } +} + +/// Open the key commitment at the outer proof's claims, batched by one challenge. +fn open_keys(ps: &mut ProverState, stack: &KeyStack, data: &ProverData, claims: &OuterClaims, log_inv_rate: usize) { + let cfg = config_for_rate_hiding(KEY_MU, log_inv_rate).expect("the key commitment's size is configured"); + let lambda = ps.sample(); + let (mut weight, target) = keys::opening_claim(claims, lambda); + weight.resize(2 * LANE, F192::ZERO); + let hiding = Hiding { + k: cfg.padding(), + hidden_claim: false, + }; + whir::recursive_prover_with_basis(&cfg, KEY_MU, &stack.words, weight, target, data, Some(hiding), ps); +} + +/// Verify the key commitment's opening at the outer proof's claims. +fn verify_keys(vs: &mut VerifierState, root: Hash, claims: &OuterClaims, log_inv_rate: usize) -> Result<(), WhirError> { + let cfg = config_for_rate_hiding(KEY_MU, log_inv_rate)?; + let lambda = Challenger::sample(vs); + let (weight, target) = keys::opening_claim(claims, lambda); + let hiding = Hiding { + k: cfg.padding(), + hidden_claim: false, + }; + // The weight lives on lane 0, the stack's first `LANE` words: its low variables index the word, the rest are zero. + let weight_at = |_: &mut VerifierState, x: &[F192]| { + let low = LANE.trailing_zeros() as usize; + let lane_0 = x[low..].iter().fold(F192::ONE, |acc, &xi| acc * (F192::ONE + xi)); + lane_0 * inner_product(&weight, &eq_table(&x[..low])) + }; + whir::recursive_verifier_with_basis_succinct(vs, &cfg, KEY_MU, 2, target, root, Some(hiding), weight_at) +} + +#[cfg(test)] +mod tests { + use crate::cpu::{Program, Proof, ProvenRun, Prover}; + use crate::pcs::Rate; + use crate::rv::Region; + use crate::rv::asm::{Addi, Asm, Reg}; + use crate::zk::randomness::Randomness; + use primitives::field::F192; + use std::panic::AssertUnwindSafe; + + fn proof(seed: u8) -> (Program, ProvenRun) { + let text = Asm::new().i(Addi, Reg::A0, Reg::ZERO, 5).exit().finish(); + let program = Program::new(&text, Region::TEXT.base(), vec![], 0, 0).expect("a program"); + let run = Prover::new(Rate::MIN) + .zk(Randomness::Seed([seed; 32])) + .prove(&program, &[]) + .expect("the run exits"); + (program, run) + } + + #[test] + fn a_zero_knowledge_proof_verifies_and_is_a_function_of_its_seed() { + let (program, run) = proof(7); + assert!(run.proof.is_zk()); + program.verify(run.output, &run.proof).unwrap(); + assert_eq!(Proof::from_bytes(&run.proof.to_bytes()), Ok(run.proof.clone())); + + // A zero-knowledge proof read as a plain one is refused. + assert!(program.verify(run.output, &Proof(run.proof.0.clone(), false)).is_err()); + + // One seed, one proof; another seed reveals other scalars past the public shape. + assert_eq!(proof(7).1.proof, run.proof); + let other = proof(8).1.proof; + program.verify(run.output, &other).unwrap(); + let shared = (run.proof.0.stream.iter().zip(&other.0.stream)) + .skip(crate::tables::N_TABLES + 1) + .filter(|(a, b)| a == b) + .count(); + assert!(shared < 8, "{shared} scalars shared past the announcement"); + } + + #[test] + fn every_part_of_a_zero_knowledge_proof_is_bound() { + let (program, run) = proof(7); + let n = run.proof.0.stream.len(); + // Every 17th scalar, then the whole tail: the outer proof and the key opening. + for i in (0..n).step_by(17).chain(n.saturating_sub(64)..n) { + let mut forged = run.proof.clone(); + forged.0.stream[i] += F192::ONE; + let verdict = std::panic::catch_unwind(AssertUnwindSafe(|| program.verify(run.output, &forged))); + assert!( + matches!(verdict, Ok(Err(_))), + "scalar {i} of {n}: tampered and not refused" + ); + } + } +} diff --git a/crates/leanvm_core/src/envelope.rs b/crates/leanvm_core/src/envelope.rs index e999f4f02..498a49b91 100644 --- a/crates/leanvm_core/src/envelope.rs +++ b/crates/leanvm_core/src/envelope.rs @@ -27,6 +27,11 @@ impl Envelope { Self { magic, version } } + /// The kind of proof the envelope carries. + pub(crate) const fn magic(&self) -> [u8; 4] { + self.magic + } + /// The body, behind the header. pub(crate) fn seal(&self, body: &[u8]) -> Vec { // One allocation for the header and the body together. diff --git a/crates/leanvm_core/src/leaf.rs b/crates/leanvm_core/src/leaf.rs index c0e85a3be..a92c8e59d 100644 --- a/crates/leanvm_core/src/leaf.rs +++ b/crates/leanvm_core/src/leaf.rs @@ -26,8 +26,8 @@ mod leaves; pub(crate) use coord::PublicColumns; pub use coord::{Coord, PublicColumn, SparseColumn}; -pub(crate) use decompose::producer_public_twist; pub use decompose::{BusForm, PackedForm, SparseShare, producer_affine_evals}; +pub(crate) use decompose::{producer_public_twist, producer_twist_terms}; pub use layout::{Block, Layout, N_TUPLE_BITS, Producer, fingerprint_weights, layout, stacked_bytecode_table}; pub use leaves::{build_leaves, producer_columns}; diff --git a/crates/leanvm_core/src/leaf/decompose.rs b/crates/leanvm_core/src/leaf/decompose.rs index a48618073..e96fbd780 100644 --- a/crates/leanvm_core/src/leaf/decompose.rs +++ b/crates/leanvm_core/src/leaf/decompose.rs @@ -73,8 +73,15 @@ pub fn producer_affine_evals(a: &mut A, p: &Producer, w: &[A::E], beta /// /// That is one pass over the columns, then a fixed cost per coordinate, bit and power. pub(crate) fn producer_public_twist(coords: &[Coord], w: &[F192], chi: &[F192], twist: &[F192]) -> F192 { + (producer_twist_terms(coords, w, chi, twist.len()).iter().zip(twist)) + .fold(F192::ZERO, |acc, (&d, &mu)| acc + mu * d) +} + +/// The program columns' share of a producer's public half at `chi`, for each of `n_bits` twist weights: the `D_i` of +/// [`producer_public_twist`]. +pub(crate) fn producer_twist_terms(coords: &[Coord], w: &[F192], chi: &[F192], n_bits: usize) -> Vec { let eq = primitives::multilinear::eq_table(chi); - let mut total = F192::ZERO; + let mut terms = vec![F192::ZERO; n_bits]; for (c, &weight) in coords.iter().zip(w) { let Coord::Public(PublicColumn { values: vals, .. }) = c else { continue; @@ -91,14 +98,14 @@ pub(crate) fn producer_public_twist(coords: &[Coord], w: &[F192], chi: &[F192], // Running `2^i`-th powers of the weight and of each bit's element. let mut weight = weight; let mut basis: [F64; 64] = std::array::from_fn(|k| F64(1 << k)); - for &mu in twist { + for term in &mut terms { let sum = (slices.iter().zip(&basis)).fold(F192::ZERO, |s, (b, &g)| s + b.mul_base(g)); - total += mu * weight * sum; + *term += weight * sum; weight = weight.square(); basis.iter_mut().for_each(|g| *g = *g * *g); } } - total + terms } /// One table's bus contribution on one side, as a form over that table's committed diff --git a/crates/leanvm_core/src/lib.rs b/crates/leanvm_core/src/lib.rs index 0c56607a1..7112c80e2 100644 --- a/crates/leanvm_core/src/lib.rs +++ b/crates/leanvm_core/src/lib.rs @@ -37,6 +37,7 @@ mod rec; mod rv; mod tables; mod witness; +mod zk; pub use self::pcs::{InvalidRate, Rate}; pub use cpu::{DecodeError, Output, Program, Proof, ProveError, ProvenRun, Prover, Stats, VerifyError}; @@ -45,6 +46,7 @@ pub use rec::tree::{ TreeShape, Unsatisfied, }; pub use rv::{ElfError, ProgramError, Region, Trap, asm}; +pub use zk::randomness::Randomness; #[doc(hidden)] pub use self::pcs::{MAX_MU, MIN_MU}; diff --git a/crates/leanvm_core/src/pcs.rs b/crates/leanvm_core/src/pcs.rs index fa3a76774..fa1a3a8c7 100644 --- a/crates/leanvm_core/src/pcs.rs +++ b/crates/leanvm_core/src/pcs.rs @@ -28,7 +28,7 @@ use crate::witness::StackShape; use ::pcs::stack_open; use ::pcs::verifier::OpeningVerifier; -use ::pcs::whir::{self, ProverConfig, ProverData, WhirError, config_for_rate}; +use ::pcs::whir::{self, Hiding, ProverConfig, ProverData, WhirError, config_for_rate, config_for_rate_hiding}; use fiat_shamir::transcript::{ProverState, TranscriptError, Transmitter}; use primitives::field::F64; use thiserror::Error; @@ -93,10 +93,19 @@ pub const MIN_MU: usize = ::pcs::whir::MIN_LOG_N; /// Largest committed size accepted by all verifiers, the largest the WHIR table configures. pub const MAX_MU: usize = ::pcs::whir::MAX_LOG_N; -/// The shared WHIR config for a `2^μ`-word witness. -fn whir_config(mu: usize, log_inv_rate: usize) -> ProverConfig { - config_for_rate(mu, log_inv_rate) - .unwrap_or_else(|e| panic!("whir config for mu={mu}, log_inv_rate={log_inv_rate}: {e}")) +/// The shared WHIR config for a `2^μ`-word witness, hiding or not. +fn whir_config(mu: usize, log_inv_rate: usize, hiding: bool) -> ProverConfig { + let config = if hiding { + config_for_rate_hiding(mu, log_inv_rate) + } else { + config_for_rate(mu, log_inv_rate) + }; + config.unwrap_or_else(|e| panic!("whir config for mu={mu}, log_inv_rate={log_inv_rate}, hiding={hiding}: {e}")) +} + +/// The padding coefficients a hiding commitment of a `2^μ`-word witness takes per lane. +pub(crate) fn padding(mu: usize, log_inv_rate: usize) -> usize { + whir_config(mu, log_inv_rate, true).padding() } /// A committed `K`-valued witness plus the data needed to open it. The witness @@ -142,6 +151,31 @@ pub fn commit(ps: &mut ProverState, witness: &[F64], shape: StackShape, log_inv_ } } +/// Commit a zero-knowledge proof's witness: its lanes padded past their power of two with `pads`, `padding(mu, rate)` +/// uniform words per committed lane, its last lane uniform (doc `leanvm` Annex B, the hiding commitment). +pub fn commit_hiding( + ps: &mut ProverState, + witness: &[F64], + shape: StackShape, + log_inv_rate: usize, + pads: &[F64], +) -> Committed { + assert!(shape.random_lane, "a hiding commitment's last lane is random"); + assert_eq!( + witness.len(), + shape.committed_len(), + "witness must be the committed lanes" + ); + assert_eq!(pads.len(), shape.committed_lanes() * padding(shape.mu, log_inv_rate)); + let (commitment, prover_data) = whir::commit_hiding(witness, shape.mu, LOG_BATCH, log_inv_rate, pads); + ps.add_root(&commitment.root); + Committed { + prover_data, + mu: shape.mu, + log_inv_rate, + } +} + // The batching challenges are just `sample()`d inside the stacked opener: every // claim they combine is already bound: the values rode the stream // (`add_scalar`) during the bus / constraint sub-protocols or, for the exit @@ -169,12 +203,19 @@ pub fn read_commitment(v: &mut V) -> Result, +) { let lane_block = 1usize << (c.mu - LOG_BATCH); assert_eq!(q.len() % lane_block, 0, "witness must be whole committed lanes"); assert!(q.len() <= 1usize << c.mu, "witness must fit the announced size"); - let cfg = whir_config(c.mu, c.log_inv_rate); - stack_open::open(ps, c.mu, q, &c.prover_data, &cfg, points, rings); + let cfg = whir_config(c.mu, c.log_inv_rate, hiding.is_some()); + stack_open::open(ps, c.mu, q, &c.prover_data, &cfg, points, rings, hiding); } /// Verify the opening (mirror of [`open`]): flock's ring-switched claim @@ -194,6 +235,13 @@ pub fn verify( log_inv_rate: usize, root: V::Root, ) -> Result<(), WhirError> { - let cfg = config_for_rate(shape.mu, log_inv_rate)?; - stack_open::verify(v, &cfg, shape.mu, shape.n_lanes, root, points, rings) + // A zero-knowledge proof's stack is the hiding commitment, and every scalar before its lane fold's end is hidden. + let (cfg, hiding) = if shape.random_lane { + let cfg = config_for_rate_hiding(shape.mu, log_inv_rate)?; + let k = cfg.padding(); + (cfg, Some(Hiding { k, hidden_claim: true })) + } else { + (config_for_rate(shape.mu, log_inv_rate)?, None) + }; + stack_open::verify(v, &cfg, shape.mu, shape.committed_lanes(), root, points, rings, hiding) } diff --git a/crates/leanvm_core/src/rec/proof.rs b/crates/leanvm_core/src/rec/proof.rs index 0102afa18..1dfc5cfc6 100644 --- a/crates/leanvm_core/src/rec/proof.rs +++ b/crates/leanvm_core/src/rec/proof.rs @@ -289,7 +289,7 @@ impl Circuit { let RecWitness { q, ports, batch } = w; drop(ports); let ring = crate::stage!("Flock reduction", || batch.prove(&layout, &q, &mut ps)); - crate::stage!("PCS open", || pcs::open(&mut ps, &committed, &q, &slots, &[ring])); + crate::stage!("PCS open", || pcs::open(&mut ps, &committed, &q, &slots, &[ring], None)); Ok(ps.into_proof()) } diff --git a/crates/leanvm_core/src/rec/tree/mod.rs b/crates/leanvm_core/src/rec/tree/mod.rs index 19416605e..965f23d6c 100644 --- a/crates/leanvm_core/src/rec/tree/mod.rs +++ b/crates/leanvm_core/src/rec/tree/mod.rs @@ -257,7 +257,12 @@ impl LeafShape { } /// The shape a proof's first scalars announce, if they are a valid announcement. + /// + /// A zero-knowledge proof has none: no node verifies one yet. fn announced(proof: &Proof) -> Option { + if proof.is_zk() { + return None; + } let scalars = proof.0.stream.get(..Announcement::LEN)?.try_into().ok()?; let announcement = Announcement::decode(scalars).ok()?; Some(Self::new(announcement.taus, announcement.rate)) diff --git a/crates/leanvm_core/src/rec/verifier/tests.rs b/crates/leanvm_core/src/rec/verifier/tests.rs index c836a3735..5eb8b88dd 100644 --- a/crates/leanvm_core/src/rec/verifier/tests.rs +++ b/crates/leanvm_core/src/rec/verifier/tests.rs @@ -548,13 +548,17 @@ fn opening_rows( fn check_opening(mu: usize, log_inv_rate: usize, seed: u64) { let what = format!("mu {mu}, log_inv_rate {log_inv_rate}"); let mut rng = Rng::new(seed); - let shape = StackShape { mu, n_lanes: N_LANES }; + let shape = StackShape { + mu, + n_lanes: N_LANES, + random_lane: false, + }; let q: Vec = (0..shape.committed_len()).map(|_| F64(rng.next_u64())).collect(); let (slots, rings) = opening_claims(mu, &q, &mut rng); let mut ps = ProverState::from_label(LABEL); let committed = crate::pcs::commit(&mut ps, &q, shape, log_inv_rate); - crate::pcs::open(&mut ps, &committed, &q, &slots, &rings); + crate::pcs::open(&mut ps, &committed, &q, &slots, &rings, None); let proof = ps.into_proof(); let native = |slots: &[StackClaim], rings: &[RingSwitch], proof: &ProofTranscript| { let mut vs = VerifierState::from_label(LABEL, proof); diff --git a/crates/leanvm_core/src/witness.rs b/crates/leanvm_core/src/witness.rs index 290e1d5f0..661102590 100644 --- a/crates/leanvm_core/src/witness.rs +++ b/crates/leanvm_core/src/witness.rs @@ -100,19 +100,46 @@ impl Placement { /// commits `committed_len()` words and never encodes or hashes the zero tail past /// them. Only the prover needs `n_lanes`; the verifier's view of the commitment is /// the same `2^mu`-word witness either way. +/// +/// A zero-knowledge proof commits one more lane after them, of uniform words (`random_lane`). #[derive(Clone, Copy, Debug)] pub struct StackShape { pub mu: usize, pub n_lanes: usize, + pub random_lane: bool, } impl StackShape { - /// Words actually committed: the placed columns rounded up to a whole lane. + /// The lanes committed: the data's, then the random lane if there is one. + pub const fn committed_lanes(&self) -> usize { + self.n_lanes + self.random_lane as usize + } + + /// Words actually committed: the placed columns rounded up to a whole lane, then the random lane. pub fn committed_len(&self) -> usize { // Both fields are `pub`, and in release the shift below would mask an // underflowed amount into a plausible wrong length rather than panic. assert!(self.mu >= crate::pcs::LOG_BATCH, "a stack is at least one lane block"); - self.n_lanes << (self.mu - crate::pcs::LOG_BATCH) + self.committed_lanes() << (self.mu - crate::pcs::LOG_BATCH) + } + + /// The shape a zero-knowledge proof commits for `placed` words: its lanes long enough for one random lane to hide + /// the opening ([`::pcs::whir::config::MIN_LOG_N_HIDING`]), and room for that lane. + pub fn hiding(placed: usize) -> Self { + let mut mu = crate::log2_ceil_usize(placed.max(1)) + .max(crate::pcs::MIN_MU) + .max(::pcs::whir::config::MIN_LOG_N_HIDING); + loop { + let n_lanes = placed.div_ceil(1 << (mu - crate::pcs::LOG_BATCH)).max(1); + if n_lanes < 1 << crate::pcs::LOG_BATCH { + return Self { + mu, + n_lanes, + random_lane: true, + }; + } + mu += 1; + } } } @@ -186,7 +213,14 @@ pub fn placements_of(sources: &[Source]) -> (Vec, StackShape) { // The columns tile from 0, so the padding is the tail: round it up to a whole // lane and the lanes past that are never committed at all. let n_lanes = placed.div_ceil(1 << (mu - crate::pcs::LOG_BATCH)).max(1); - (placements, StackShape { mu, n_lanes }) + ( + placements, + StackShape { + mu, + n_lanes, + random_lane: false, + }, + ) } /// Chunk width for the bulk writes below: big enough to amortize the dispatch, diff --git a/crates/leanvm_core/src/zk/keys.rs b/crates/leanvm_core/src/zk/keys.rs new file mode 100644 index 000000000..ced539174 --- /dev/null +++ b/crates/leanvm_core/src/zk/keys.rs @@ -0,0 +1,100 @@ +//! The key commitment: every one-time-pad key, the outer proof's dummy operands and its mask, in one lane of its own stack, beside one lane of uniform words (doc `leanvm` §sec:zk). +//! +//! Its shape is fixed, so neither side counts anything before committing: +//! +//! ```text +//! lane 0 slots of E, three words each: the 6 dummy operands, the mask's room, then the keys in the order they pad +//! lane 1 uniform words +//! ``` +//! +//! Its opening's claim is public and its weight vanishes on lane 1, so the lane fold mixes the uniform lane into everything the opening reveals: it is the one commitment whose opening hides itself. + +use super::r1cs::N_DUMMIES; +use super::randomness::{Purpose, ZkRng, uniform_e}; +use super::spartan::{OuterClaims, libra_len}; +use crate::pcs::LOG_BATCH; +use primitives::field::{F64, F192}; + +/// The key stack's size: two lanes of `2^(KEY_MU - LOG_BATCH)` words, the smallest stack a hiding opening takes. +pub(crate) const KEY_MU: usize = ::pcs::whir::MIN_LOG_N_HIDING; +/// The words of a lane. +pub(crate) const LANE: usize = 1 << (KEY_MU - LOG_BATCH); + +/// The `E` slots lane 0 holds. +pub(crate) const N_SLOTS: usize = LANE / 3; + +/// The dummy operands' first slot. +pub(crate) const DUMMY_SLOT: usize = 0; + +/// The outer proof's mask's first slot. +pub(crate) const LIBRA_SLOT: usize = DUMMY_SLOT + N_DUMMIES; + +/// The outer constraint system's largest row cube, which the mask's room is sized for. +pub(crate) const MAX_OUTER_LOG_ROWS: usize = 24; + +/// The first key's slot. +pub(crate) const KEY_SLOT: usize = LIBRA_SLOT + libra_len(MAX_OUTER_LOG_ROWS); + +/// The most keys one proof uses: hidden scalars, then auxiliary values. +pub(crate) const MAX_KEYS: usize = N_SLOTS - KEY_SLOT; + +/// The prover's key stack: its slots, and the two lanes' words it commits. +pub(crate) struct KeyStack { + /// Every slot of lane 0: dummy operands, mask, keys, all uniform but the dummies' products. + pub(crate) slots: Vec, + /// Lane 0's words, then lane 1's. + pub(crate) words: Vec, +} + +impl KeyStack { + /// Draw a proof's keys, its outer proof's dummies and mask, and the uniform lane. + pub(crate) fn draw(rng: &ZkRng) -> Self { + let mut stream = rng.stream(Purpose::Keys); + let mut slots: Vec = (0..N_SLOTS).map(|_| uniform_e(&mut stream)).collect(); + let dummies = super::r1cs::dummy_values(|| uniform_e(&mut stream)); + slots[DUMMY_SLOT..DUMMY_SLOT + N_DUMMIES].copy_from_slice(&dummies); + + let mut words = vec![F64::ZERO; 2 * LANE]; + rng.fill_k(Purpose::KeyLanes, &mut words[3 * N_SLOTS..]); + for (s, slot) in slots.iter().enumerate() { + words[3 * s..3 * s + 3].copy_from_slice(&[F64(slot.c0), F64(slot.c1), F64(slot.c2)]); + } + Self { slots, words } + } + + /// The keys, in the order the hidden scalars use them. + pub(crate) fn keys(&self) -> &[F192] { + &self.slots[KEY_SLOT..] + } + + /// The outer proof's mask for a constraint system of `2^log_rows` rows. + pub(crate) fn libra(&self, log_rows: usize) -> &[F192] { + &self.slots[LIBRA_SLOT..LIBRA_SLOT + libra_len(log_rows)] + } + + /// The outer constraint system's assignment: the constant one, then every slot. + pub(crate) fn z(&self) -> Vec { + std::iter::once(F192::ONE).chain(self.slots.iter().copied()).collect() + } +} + +/// The key opening's claim: the outer proof's two claims, batched by `lambda`, as a weight on lane 0's words and a target. +pub(crate) fn opening_claim(claims: &OuterClaims, lambda: F192) -> (Vec, F192) { + assert_eq!( + claims.witness_weight.len(), + N_SLOTS, + "the outer proof's columns are the slots" + ); + let mut slots = claims.witness_weight.clone(); + for (s, &w) in slots[LIBRA_SLOT..].iter_mut().zip(&claims.libra_weight) { + *s += lambda * w; + } + let basis = [F192::new(1, 0, 0), F192::new(0, 1, 0), F192::new(0, 0, 1)]; + let mut weight = vec![F192::ZERO; LANE]; + for (s, &w) in slots.iter().enumerate() { + for (l, &y) in basis.iter().enumerate() { + weight[3 * s + l] = w * y; + } + } + (weight, claims.witness_target + lambda * claims.libra_target) +} diff --git a/crates/leanvm_core/src/zk/mod.rs b/crates/leanvm_core/src/zk/mod.rs new file mode 100644 index 000000000..207e8071d --- /dev/null +++ b/crates/leanvm_core/src/zk/mod.rs @@ -0,0 +1,8 @@ +//! Zero knowledge (doc `leanvm` §sec:zk): the outer proof that a padded transcript passes the verifier's checks. + +pub(crate) mod keys; +pub(crate) mod outer; +pub(crate) mod r1cs; +pub(crate) mod randomness; +pub(crate) mod spartan; +pub(crate) mod sym; diff --git a/crates/leanvm_core/src/zk/outer.rs b/crates/leanvm_core/src/zk/outer.rs new file mode 100644 index 000000000..3b14c71a5 --- /dev/null +++ b/crates/leanvm_core/src/zk/outer.rs @@ -0,0 +1,110 @@ +//! The outer constraint system: what the recording verifier recorded, over the key stack's slots (doc `leanvm` §sec:zk). +//! +//! Column 0 is the constant one and column `1 + s` the key stack's slot `s`. A key is its slot; an auxiliary variable is +//! the scalar the prover sent for it plus its own key, so every column is a slot and the assignment is the key stack. +//! +//! Its rows, in order: +//! +//! ```text +//! one per auxiliary variable, by digest a·b = v (a product), a·v = 1 (an inverse), (a + v)·1 = 0 (a bound value) +//! one per linear constraint, by digest l·1 = 0 +//! one per bit, by digest b·b = b +//! the two dummies +//! ``` + +use super::keys::{DUMMY_SLOT, KEY_SLOT, N_SLOTS}; +use super::r1cs::{R1cs, Row as SparseRow}; +use super::sym::{Form, Kind, Record, Var}; +use primitives::field::F192; + +/// The constraint system the record states, the auxiliary variable of rank `r` (by digest) being the form `sent[r]`: the +/// scalar sent for it plus its key. +pub(crate) fn constraint_system(record: &Record, sent: &[Form]) -> R1cs { + let order = record.aux_order(); + assert_eq!(sent.len(), order.len(), "a sent scalar per auxiliary variable"); + let mut rank = vec![0u32; order.len()]; + for (r, &j) in order.iter().enumerate() { + rank[j as usize] = u32::try_from(r).expect("fewer than 2^32 variables"); + } + let row = |f: &Form| sparse(f, &rank, sent); + let constant = |c: F192| vec![(0, c)]; + let mut r1cs = R1cs { + n_cols: 1 + N_SLOTS, + ..R1cs::default() + }; + for &j in &order { + let aux = &record.aux[j as usize]; + let v = Form { + constant: F192::ZERO, + terms: vec![(Var::Aux(j), F192::ONE)], + }; + let (a, b, c) = match aux.kind { + Kind::Product => (row(&aux.a), row(&aux.b), row(&v)), + Kind::Inverse => (row(&aux.a), row(&v), constant(F192::ONE)), + Kind::Bind => { + let mut terms = aux.a.terms.clone(); + terms.push((Var::Aux(j), F192::ONE)); + let sum = Form { + constant: aux.a.constant, + terms, + }; + (row(&sum), constant(F192::ONE), Vec::new()) + } + }; + r1cs.a.push(a); + r1cs.b.push(b); + r1cs.c.push(c); + } + let mut linear: Vec<&([u8; 32], Form)> = record.linear.iter().collect(); + linear.sort_unstable_by_key(|(d, _)| *d); + for (_, l) in linear { + r1cs.a.push(row(l)); + r1cs.b.push(constant(F192::ONE)); + r1cs.c.push(Vec::new()); + } + let mut booleans: Vec<&([u8; 32], Form)> = record.booleans.iter().collect(); + booleans.sort_unstable_by_key(|(d, _)| *d); + for (_, b) in booleans { + let b = row(b); + r1cs.a.push(b.clone()); + r1cs.b.push(b.clone()); + r1cs.c.push(b); + } + r1cs.push_dummies(1 + DUMMY_SLOT); + r1cs +} + +/// The column of a key. +fn key_column(i: u32) -> u32 { + u32::try_from(1 + KEY_SLOT).expect("a column fits a u32") + i +} + +/// A form as a sparse row, its auxiliary variables expanded to what was sent for them, its columns in order and merged. +fn sparse(form: &Form, rank: &[u32], sent: &[Form]) -> SparseRow { + let mut out: Vec<(u32, F192)> = vec![(0, form.constant)]; + for &(v, coefficient) in &form.terms { + match v { + Var::Key(i) => out.push((key_column(i), coefficient)), + Var::Aux(j) => { + let a = &sent[rank[j as usize] as usize]; + out.push((0, coefficient * a.constant)); + for &(w, c) in &a.terms { + let Var::Key(i) = w else { + unreachable!("an auxiliary variable is a sent scalar plus its key") + }; + out.push((key_column(i), coefficient * c)); + } + } + } + } + out.sort_unstable_by_key(|&(col, _)| col); + let mut merged: SparseRow = Vec::with_capacity(out.len()); + for (col, c) in out { + match merged.last_mut() { + Some((last, acc)) if *last == col => *acc += c, + _ => merged.push((col, c)), + } + } + merged.retain(|&(_, c)| c != F192::ZERO); + merged +} diff --git a/crates/leanvm_core/src/zk/r1cs.rs b/crates/leanvm_core/src/zk/r1cs.rs new file mode 100644 index 000000000..1361fdbf5 --- /dev/null +++ b/crates/leanvm_core/src/zk/r1cs.rs @@ -0,0 +1,84 @@ +//! A sparse rank-one constraint system over `E`. + +use primitives::field::F192; + +/// How many witness columns the two dummy constraints take (see [`R1cs::push_dummies`]). +pub(crate) const N_DUMMIES: usize = 6; + +/// One sparse row of a matrix: `(column, coefficient)` pairs. +pub(crate) type Row = Vec<(u32, F192)>; + +/// Rows `(A_x·z)(B_x·z) = (C_x·z)` over `z = (1, w)`: column 0 is the constant one. +/// +/// The three matrices have one row per constraint. +#[derive(Clone, Debug, Default)] +pub(crate) struct R1cs { + pub(crate) n_cols: usize, + pub(crate) a: Vec, + pub(crate) b: Vec, + pub(crate) c: Vec, +} + +impl R1cs { + pub(crate) const fn n_rows(&self) -> usize { + self.a.len() + } + + /// The variables of the row cube: at least one, the rows past [`Self::n_rows`] being zero rows. + pub(crate) const fn log_rows(&self) -> usize { + let log = self.n_rows().next_power_of_two().trailing_zeros() as usize; + if log == 0 { 1 } else { log } + } + + /// `Az`, `Bz`, `Cz`, each zero-padded to `2^log_rows`. + pub(crate) fn products(&self, z: &[F192]) -> [Vec; 3] { + assert_eq!(z.len(), self.n_cols, "a value per column"); + assert!( + self.b.len() == self.n_rows() && self.c.len() == self.n_rows(), + "three matrices of one height" + ); + let len = 1 << self.log_rows(); + [&self.a, &self.b, &self.c].map(|m| { + let mut out: Vec = m + .iter() + .map(|row| { + row.iter() + .fold(F192::ZERO, |acc, &(y, coef)| acc + coef * z[y as usize]) + }) + .collect(); + out.resize(len, F192::ZERO); + out + }) + } + + #[cfg(test)] + pub(crate) fn is_satisfied(&self, z: &[F192]) -> bool { + z.first() == Some(&F192::ONE) && { + let [az, bz, cz] = self.products(z); + (az.iter().zip(&bz).zip(&cz)).all(|((&a, &b), &c)| a * b == c) + } + } + + /// Append the two dummy constraints `z[first]·z[first+1] = z[first+2]` and `z[first+3]·z[first+4] = z[first+5]`. + /// + /// Their operands are fresh and uniform ([`dummy_values`]), which is what hides the final `(a, b, c)` of the outer + /// Spartan: each sits at a row of its own, so it adds a uniform term to each of the three evaluations. + pub(crate) fn push_dummies(&mut self, first: usize) { + assert!( + first > 0 && first + N_DUMMIES <= self.n_cols, + "the dummies are witness columns" + ); + for k in [first, first + 3] { + let unit = |y: usize| vec![(u32::try_from(y).expect("a column fits a u32"), F192::ONE)]; + self.a.push(unit(k)); + self.b.push(unit(k + 1)); + self.c.push(unit(k + 2)); + } + } +} + +/// The dummy constraints' columns: two uniform operand pairs and their products. +pub(crate) fn dummy_values(mut rand: impl FnMut() -> F192) -> [F192; N_DUMMIES] { + let [a0, b0, a1, b1] = [rand(), rand(), rand(), rand()]; + [a0, b0, a0 * b0, a1, b1, a1 * b1] +} diff --git a/crates/leanvm_core/src/zk/randomness.rs b/crates/leanvm_core/src/zk/randomness.rs new file mode 100644 index 000000000..11d610028 --- /dev/null +++ b/crates/leanvm_core/src/zk/randomness.rs @@ -0,0 +1,86 @@ +//! A zero-knowledge prover's randomness: ChaCha20 under a seed drawn from the OS, or given by a test. +//! +//! Nothing it draws ever comes from the transcript: a proof made from the transcript alone would be a deterministic function of the witness, which a verifier could recompute for each guess of the advice. + +use primitives::field::{F64, F192}; +use rand_chacha::ChaCha20Rng; +use rand_core::{OsRng, RngCore, SeedableRng, TryRngCore}; + +/// Where a zero-knowledge prover draws its randomness. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Randomness { + /// A fresh seed from the operating system for every proof. + Os, + /// One fixed seed, for reproducible tests: two proofs under one seed share their keys, so never reuse one in production. + #[doc(hidden)] + Seed([u8; 32]), +} + +/// What a stream of the prover's randomness is drawn for, each from its own ChaCha20 stream. +#[derive(Clone, Copy, Debug)] +pub(crate) enum Purpose { + /// The one-time-pad keys, the outer proof's dummy operands and its mask. + Keys = 0, + /// The padding coefficients of the main commitment's lanes. + Pads = 1, + /// The main commitment's random lane. + RandomLane = 2, + /// The key commitment's mask lane, and the two words past its slots. + KeyLanes = 3, + /// The key commitment's lanes' padding. + KeyPads = 4, +} + +/// One proof's randomness: a seed, cut into independent streams by purpose. +pub(crate) struct ZkRng { + seed: [u8; 32], +} + +impl ZkRng { + /// Words a parallel fill gives each task. + const CHUNK: usize = 1 << 14; + + /// The randomness of one proof. + /// + /// # Panics + /// + /// If the operating system gives no randomness. + pub(crate) fn new(randomness: Randomness) -> Self { + let seed = match randomness { + Randomness::Os => { + let mut seed = [0u8; 32]; + OsRng + .try_fill_bytes(&mut seed) + .expect("the operating system gives randomness"); + seed + } + Randomness::Seed(seed) => seed, + }; + Self { seed } + } + + /// The stream drawn for `purpose`. + pub(crate) fn stream(&self, purpose: Purpose) -> ChaCha20Rng { + let mut rng = ChaCha20Rng::from_seed(self.seed); + rng.set_stream(purpose as u64); + rng + } + + /// Fill `out` with uniform words of the stream drawn for `purpose`, in parallel: chunk `i` starts at its own position of the stream. + pub(crate) fn fill_k(&self, purpose: Purpose, out: &mut [F64]) { + let base = self.stream(purpose); + parallel::chunks_mut(out, Self::CHUNK, |i, chunk| { + let mut rng = base.clone(); + // A word is two of ChaCha's 32-bit words. + rng.set_word_pos((2 * i * Self::CHUNK) as u128); + for w in chunk { + *w = F64(rng.next_u64()); + } + }); + } +} + +/// A uniform element of `E`. +pub(crate) fn uniform_e(rng: &mut ChaCha20Rng) -> F192 { + F192::new(rng.next_u64(), rng.next_u64(), rng.next_u64()) +} diff --git a/crates/leanvm_core/src/zk/spartan.rs b/crates/leanvm_core/src/zk/spartan.rs new file mode 100644 index 000000000..cb904176d --- /dev/null +++ b/crates/leanvm_core/src/zk/spartan.rs @@ -0,0 +1,328 @@ +//! The outer zero-knowledge Spartan over `E`. +//! +//! It proves `sum_x eq(τ, x)·F(x) = 0` for `F = ÷B̃ + C̃`, the row products of an [`R1cs`] over a witness the caller +//! commits elsewhere, and ends in two linear claims the caller discharges with its own opening: one on the witness, +//! one on the Libra mask `g(X) = g_c + sum_j (g_{j0} + g_{j1} X_j) X_j`, which the caller commits too. +//! +//! The rows form the cube `{0,1}^ℓ`, `x = sum_i x_i 2^i`, variable 0 bound first. +//! +//! Zero knowledge needs no padding: +//! - each round's `c_1` and `c_2` are those of `F` plus `α` times the mask's fresh `(g_{i0}, g_{i1})`, the eq-weighted +//! MLE-check mask of the Binius64 whitepaper; +//! - the mask's sum `s_g` is hidden by `g_c`; +//! - the final `(a, b, c)` are hidden by the two dummy constraints ([`R1cs::push_dummies`]), whose fresh operands sit at +//! rows of their own. +//! +//! The characteristic-2 argument rests on the Binius64 whitepaper's MLE-check theorem and is unreviewed. + +use super::r1cs::R1cs; +use fiat_shamir::arith::{Arith, Native, Verifier}; +use fiat_shamir::transcript::{TranscriptError, Transmitter}; +use primitives::field::F192; +use primitives::multilinear::{eq_table, interp}; +use thiserror::Error; + +/// What the outer proof leaves to the caller's commitment opening. +#[derive(Clone, Debug, PartialEq, Eq)] +pub(crate) struct OuterClaims { + /// `⟨witness_weight, z[1..]⟩ = witness_target`. + pub(crate) witness_weight: Vec, + pub(crate) witness_target: E, + /// `⟨libra_weight, libra⟩ = libra_target`: the mask at the sumcheck's point. + pub(crate) libra_weight: Vec, + pub(crate) libra_target: E, +} + +/// Why the outer verifier refuses: it has no witness, so only a malformed stream. +#[derive(Clone, Debug, PartialEq, Eq, Error)] +pub(crate) enum SpartanError { + /// The proof stream is malformed. + #[error(transparent)] + Transcript(#[from] TranscriptError), +} + +/// The Libra mask's coefficients over `log_rows` variables: `[g_c, g_00, g_01, g_10, g_11, ...]`. +pub(crate) const fn libra_len(log_rows: usize) -> usize { + 1 + 2 * log_rows +} + +/// Prove `z` satisfies `r1cs`, with the Libra mask `libra` the caller committed. +/// +/// # Panics +/// +/// If `z` does not satisfy `r1cs`, or `libra` is not [`libra_len`] long. +pub(crate) fn prove(ps: &mut impl Transmitter, r1cs: &R1cs, z: &[F192], libra: &[F192]) -> OuterClaims { + assert_eq!(z.first(), Some(&F192::ONE), "column 0 is the constant one"); + let products = r1cs.products(z); + let [az, bz, cz] = &products; + assert!( + (az.iter().zip(bz).zip(cz)).all(|((&a, &b), &c)| a * b == c), + "the witness satisfies the system" + ); + prove_products(ps, r1cs, products, libra) +} + +/// The prover's steps on `Az`, `Bz`, `Cz`, whatever they satisfy. +fn prove_products(ps: &mut impl Transmitter, r1cs: &R1cs, products: [Vec; 3], libra: &[F192]) -> OuterClaims { + let log_rows = r1cs.log_rows(); + assert_eq!(libra.len(), libra_len(log_rows), "a mask of the system's size"); + let [mut az, mut bz, mut cz] = products; + let (g_c, g) = (libra[0], libra[1..].as_chunks::<2>().0); + + let tau = ps.sample_vec(log_rows); + // `sum_j τ_j g_j(1)`, the mask's share of the variables still free. + let mut suffix = (tau.iter().zip(g)).fold(F192::ZERO, |acc, (&t, &[g0, g1])| acc + t * (g0 + g1)); + ps.add_scalar(g_c + suffix); + let alpha = ps.sample(); + + // `g_c + sum_{j(v: &mut V, r1cs: &R1cs) -> Result, SpartanError> { + let log_rows = r1cs.log_rows(); + let tau = v.sample_vec(log_rows); + let s_g = v.next_scalar()?; + let alpha = v.sample(); + // The system's sum is zero, so the claim is the mask's alone. + let mut s = v.mul(alpha, s_g); + let mut r = Vec::with_capacity(log_rows); + for &t in &tau { + let coeffs = v.next_round_poly(3, s, Some(t))?; + let ri = v.sample(); + s = v.poly_eval(&coeffs, ri); + r.push(ri); + } + + let [a, b, c] = [v.next_scalar()?, v.next_scalar()?, v.next_scalar()?]; + // `s = F(r) + α·g(r)`. + let f = v.mul_add(a, b, c); + let masked = v.add(s, f); + let alpha_inv = v.inv(alpha); + let libra_target = v.mul(masked, alpha_inv); + let gamma = v.sample(); + let libra_weight = libra_weight(v, &r); + let eq = v.eq_table_prefix(&r, r1cs.n_rows()); + Ok(claims(v, r1cs, &eq, [a, b, c], gamma, libra_target, libra_weight)) +} + +/// `[1, r_0, r_0^2, r_1, r_1^2, ...]`, so that `⟨libra, weight⟩ = g(r)`. +fn libra_weight(ar: &mut A, r: &[A::E]) -> Vec { + let mut weight = Vec::with_capacity(libra_len(r.len())); + weight.push(ar.one()); + for &ri in r { + let sq = ar.square(ri); + weight.extend([ri, sq]); + } + weight +} + +/// The two claims, from `(a, b, c)` and `eq(r, x)` for the first `n_rows` rows `x` at least. +/// +/// `t_y = sum_x eq(r, x)(A[x][y] + γ B[x][y] + γ^2 C[x][y])` gives `⟨t, z⟩ = a + γ b + γ^2 c`, and `z_0 = 1` moves `t_0` +/// to the target. +fn claims( + ar: &mut A, + r1cs: &R1cs, + eq: &[A::E], + [a, b, c]: [A::E; 3], + gamma: A::E, + libra_target: A::E, + libra_weight: Vec, +) -> OuterClaims { + let zero = ar.zero(); + let mut t = vec![zero; r1cs.n_cols]; + for (x, &e) in eq[..r1cs.n_rows()].iter().enumerate() { + let eb = ar.mul(e, gamma); + let ec = ar.mul(eb, gamma); + for (rows, w) in [(&r1cs.a, e), (&r1cs.b, eb), (&r1cs.c, ec)] { + for &(y, coef) in &rows[x] { + t[y as usize] = ar.mul_const_add(w, coef, t[y as usize]); + } + } + } + let bc = ar.mul_add(c, gamma, b); + let abc = ar.mul_add(bc, gamma, a); + let witness_target = ar.add(abc, t[0]); + t.remove(0); + OuterClaims { + witness_weight: t, + witness_target, + libra_weight, + libra_target, + } +} + +/// Bind a table's lowest variable to `r`. +fn fold_low(table: &mut Vec, r: F192) { + let half = table.len() / 2; + for k in 0..half { + table[k] = interp(table[2 * k], table[2 * k + 1], r); + } + table.truncate(half); +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::zk::r1cs::{N_DUMMIES, dummy_values}; + use fiat_shamir::transcript::{ProofTranscript, ProverState, VerifierState}; + use primitives::test_util::Rng; + + const LABEL: &[u8] = b"zk-spartan-test"; + const N_WITNESS: usize = 200; + const N_ROWS: usize = 300; + + /// A random satisfiable system over `z = (1, w, dummies)`, its dummies pushed last. + fn instance(rng: &mut Rng) -> (R1cs, Vec) { + let n_cols = 1 + N_WITNESS + N_DUMMIES; + let mut z = vec![F192::ONE]; + z.extend(rng.ext_vec(N_WITNESS)); + z.extend(dummy_values(|| rng.ext())); + let mut r1cs = R1cs { + n_cols, + ..R1cs::default() + }; + let col = |rng: &mut Rng| (rng.next_u32() as usize % (N_WITNESS + 1)) as u32; + let row = |rng: &mut Rng, n: usize| -> Vec<(u32, F192)> { (0..n).map(|_| (col(rng), rng.ext())).collect() }; + for _ in 0..N_ROWS { + let (a, b, mut c) = (row(rng, 3), row(rng, 2), row(rng, 2)); + let value = |row: &[(u32, F192)]| row.iter().fold(F192::ZERO, |acc, &(y, k)| acc + k * z[y as usize]); + // A last entry on a nonzero witness column closes the row. + let y = 1 + rng.next_u32() as usize % N_WITNESS; + let gap = value(&a) * value(&b) + value(&c); + c.push((y as u32, gap * z[y].inv())); + r1cs.a.push(a); + r1cs.b.push(b); + r1cs.c.push(c); + } + r1cs.push_dummies(1 + N_WITNESS); + assert!(r1cs.is_satisfied(&z)); + (r1cs, z) + } + + fn libra(rng: &mut Rng, r1cs: &R1cs) -> Vec { + rng.ext_vec(libra_len(r1cs.log_rows())) + } + + fn dot(w: &[F192], v: &[F192]) -> F192 { + assert_eq!(w.len(), v.len()); + w.iter().zip(v).fold(F192::ZERO, |acc, (&a, &b)| acc + a * b) + } + + /// Whether both claims hold against the witness and the mask. + fn holds(claims: &OuterClaims, z: &[F192], libra: &[F192]) -> bool { + dot(&claims.witness_weight, &z[1..]) == claims.witness_target + && dot(&claims.libra_weight, libra) == claims.libra_target + } + + fn run(r1cs: &R1cs, z: &[F192], libra: &[F192]) -> (OuterClaims, ProofTranscript) { + let mut ps = ProverState::from_label(LABEL); + let claims = prove(&mut ps, r1cs, z, libra); + (claims, ps.into_proof()) + } + + fn check(r1cs: &R1cs, proof: &ProofTranscript) -> Result { + let mut v = VerifierState::from_label(LABEL, proof); + let claims = verify(&mut v, r1cs)?; + v.finish()?; + Ok(claims) + } + + #[test] + fn honest_claims_hold() { + let mut rng = Rng::new(1); + let (r1cs, z) = instance(&mut rng); + let libra = libra(&mut rng, &r1cs); + let (proved, proof) = run(&r1cs, &z, &libra); + let verified = check(&r1cs, &proof).unwrap(); + assert_eq!(proved, verified); + assert!(holds(&verified, &z, &libra)); + } + + #[test] + fn unsatisfied_witness_fails_a_claim() { + let mut rng = Rng::new(2); + let (r1cs, mut z) = instance(&mut rng); + let libra = libra(&mut rng, &r1cs); + // Column 1 sits in some row, so that row now fails. + z[1] += F192::ONE; + assert!(!r1cs.is_satisfied(&z)); + let mut ps = ProverState::from_label(LABEL); + prove_products(&mut ps, &r1cs, r1cs.products(&z), &libra); + let claims = check(&r1cs, &ps.into_proof()).unwrap(); + assert!(!holds(&claims, &z, &libra)); + } + + #[test] + fn tampered_proof_fails_a_claim() { + let mut rng = Rng::new(3); + let (r1cs, z) = instance(&mut rng); + let libra = libra(&mut rng, &r1cs); + let (_, proof) = run(&r1cs, &z, &libra); + // The stream is `s_g`, then `(c_1, c_2)` per round, then `(a, b, c)`. + let a = 1 + 2 * r1cs.log_rows(); + for (what, at) in [("s_g", 0), ("a round coefficient", 3), ("a", a)] { + let mut tampered = proof.clone(); + tampered.stream[at] += F192::ONE; + let refused = check(&r1cs, &tampered).map_or(true, |claims| !holds(&claims, &z, &libra)); + assert!(refused, "a tampered {what} is accepted"); + } + } + + #[test] + fn fresh_masks_share_no_scalar() { + let mut rng = Rng::new(4); + let (r1cs, z) = instance(&mut rng); + let mut z2 = z.clone(); + z2[z.len() - N_DUMMIES..].copy_from_slice(&dummy_values(|| rng.ext())); + assert!(r1cs.is_satisfied(&z2)); + let (_, first) = run(&r1cs, &z, &libra(&mut rng, &r1cs)); + let (_, second) = run(&r1cs, &z2, &libra(&mut rng, &r1cs)); + assert_eq!(first.stream.len(), second.stream.len()); + assert!(first.stream.iter().all(|x| !second.stream.contains(x))); + } +} diff --git a/crates/leanvm_core/src/zk/sym.rs b/crates/leanvm_core/src/zk/sym.rs new file mode 100644 index 000000000..c5c3d67e2 --- /dev/null +++ b/crates/leanvm_core/src/zk/sym.rs @@ -0,0 +1,574 @@ +//! The verifier over a padded transcript: the native verifier's own code, its hidden values held as affine forms over the keys and its checks on them recorded as constraints (doc `leanvm` §sec:zk). +//! +//! - A scalar read while the transcript is hidden is `c + k`: the value sent, plus the key that padded it (characteristic two). +//! - A challenge, a root, a query and every public computation stay values, checked as the native verifier checks them. +//! - A linear step on hidden values is a new form. An element is hidden exactly when its form has a term. +//! - A product of two hidden values, an inverse or a bound value of a hidden one is an auxiliary variable, which the prover supplies after the transcript. +//! - An equality with a hidden side is a linear constraint. +//! +//! What it records is canonical, so that two verifiers agree on it whatever order and scale their own arithmetic takes: +//! +//! - an auxiliary variable is defined on monic forms, its operands divided by their leading coefficient, and a variable defined twice is one variable; +//! - a variable and a linear constraint are named by their digest, the outer constraint system orders them by it, and a constraint stated twice is one constraint. +//! +//! Which values are hidden is fixed by the transcript's shape, so the prover's replay of its own proof records what the verifier records. + +use crate::leaf::PublicColumns; +use fiat_shamir::arith::{Arith, Verifier}; +use fiat_shamir::merkle::Hash; +use fiat_shamir::transcript::TranscriptError; +use pcs::verifier::OpeningVerifier; +use primitives::field::{F64, F192}; +use primitives::hash::Hasher; +use primitives::multilinear::mle_eval_par; +use std::collections::{HashMap, HashSet}; + +/// A variable of the outer constraint system. +#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord)] +pub(crate) enum Var { + /// The key of the `i`-th hidden scalar. + Key(u32), + /// The `j`-th auxiliary variable made. + Aux(u32), +} + +/// `constant + sum_v coefficient_v v`, its terms sorted by variable, none of them zero. +#[derive(Clone, Debug, Default, PartialEq, Eq)] +pub(crate) struct Form { + pub(crate) constant: F192, + pub(crate) terms: Vec<(Var, F192)>, +} + +/// An element as the recording verifier holds it: a value, or a form with a term. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub(crate) enum Sym { + /// A public value. + Pub(F192), + /// The form at this index of the recorder's arena. + Hid(u32), +} + +/// What defines an auxiliary variable, on monic forms. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub(crate) enum Kind { + /// `a·b`, its operands in digest order. + Product = 1, + /// `1 / a`. + Inverse = 2, + /// `a` itself. + Bind = 3, +} + +/// An auxiliary variable: its definition, and its digest. +#[derive(Clone, Debug)] +pub(crate) struct Aux { + pub(crate) kind: Kind, + pub(crate) a: Form, + /// The second operand of a product, empty otherwise. + pub(crate) b: Form, + pub(crate) digest: [u8; 32], +} + +/// What the recording verifier recorded. +#[derive(Default)] +pub(crate) struct Record { + pub(crate) forms: Vec, + /// Keys read. + pub(crate) n_keys: u32, + /// The auxiliary variables, in the order they were made. + pub(crate) aux: Vec, + /// On the prover's side, each auxiliary variable's value, in the order they were made. + pub(crate) aux_values: Vec, + /// Monic linear forms that must vanish, by digest. + pub(crate) linear: Vec<([u8; 32], Form)>, + /// Forms that must be bits, by digest. + pub(crate) booleans: Vec<([u8; 32], Form)>, +} + +impl Record { + /// The form an element stands for. + pub(crate) fn form(&self, s: Sym) -> Form { + match s { + Sym::Pub(c) => Form { + constant: c, + terms: Vec::new(), + }, + Sym::Hid(i) => self.forms[i as usize].clone(), + } + } + + /// The auxiliary variables in the outer system's order, by digest: entry `r` is the variable made `order[r]`-th. + pub(crate) fn aux_order(&self) -> Vec { + let mut order: Vec = (0..u32::try_from(self.aux.len()).expect("fewer than 2^32 variables")).collect(); + order.sort_unstable_by_key(|&j| self.aux[j as usize].digest); + order + } + + /// A form's terms in canonical order: keys by index, then auxiliary variables by digest. + fn canonical<'f>(&self, f: &'f Form) -> Vec<&'f (Var, F192)> { + let mut terms: Vec<&(Var, F192)> = f.terms.iter().collect(); + terms.sort_by_key(|(v, _)| match *v { + Var::Key(i) => (0u8, i, [0u8; 32]), + Var::Aux(j) => (1, 0, self.aux[j as usize].digest), + }); + terms + } + + /// BLAKE2s over a form: its constant, then each term in canonical order, a key as `0, index` and an auxiliary + /// variable as `1, digest`, each with its coefficient. An element of `E` is its three limbs, little-endian. + pub(crate) fn digest(&self, f: &Form) -> [u8; 32] { + let mut h = Hasher::new(); + absorb_e(&mut h, f.constant); + for &&(v, c) in &self.canonical(f) { + match v { + Var::Key(i) => { + h.update(&[0]); + h.update(&i.to_le_bytes()); + } + Var::Aux(j) => { + h.update(&[1]); + h.update(&self.aux[j as usize].digest); + } + } + absorb_e(&mut h, c); + } + h.finalize() + } + + /// A form with a term as its leading coefficient, the first term's in canonical order, times its monic form. + fn monic(&self, f: &Form) -> (F192, Form) { + let lead = self.canonical(f)[0].1; + let inv = lead.inv(); + let monic = Form { + constant: f.constant * inv, + terms: f.terms.iter().map(|&(v, c)| (v, c * inv)).collect(), + }; + (lead, monic) + } +} + +/// An element of `E` into a hash, its limbs little-endian. +fn absorb_e(h: &mut Hasher, x: F192) { + for limb in [x.c0, x.c1, x.c2] { + h.update(&limb.to_le_bytes()); + } +} + +/// The verifier's arithmetic and transcript over a padded proof, read through a native transport `T`. +pub(crate) struct Recorder { + t: T, + record: Record, + /// Each auxiliary variable by its digest. + by_digest: HashMap<[u8; 32], u32>, + /// The linear constraints and bits recorded, by digest. + stated: HashSet<[u8; 32]>, + /// Each form's value, on the prover's side, which knows the keys. + values: Option>, + keys: Vec, + hidden: bool, +} + +impl Recorder { + /// A verifier that knows no key. + pub(crate) fn new(t: T) -> Self { + Self { + t, + record: Record::default(), + by_digest: HashMap::new(), + stated: HashSet::new(), + values: None, + keys: Vec::new(), + hidden: false, + } + } + + /// The prover's replay of its own proof: it knows every key, so it computes each value it records. + pub(crate) fn with_keys(t: T, keys: Vec) -> Self { + let mut r = Self::new(t); + r.values = Some(Vec::new()); + r.keys = keys; + r + } + + /// The transport, to read the rest of the proof natively. + pub(crate) const fn transport(&mut self) -> &mut T { + &mut self.t + } + + /// The transport back, and what was recorded. + pub(crate) fn finish_record(self) -> (T, Record) { + (self.t, self.record) + } + + /// Keys read so far. + pub(crate) const fn n_keys(&self) -> u32 { + self.record.n_keys + } + + /// Auxiliary variables made so far. + pub(crate) fn n_aux(&self) -> u32 { + u32::try_from(self.record.aux.len()).expect("fewer than 2^32 variables") + } + + /// The form an element stands for. + pub(crate) fn form(&self, s: Sym) -> Form { + self.record.form(s) + } + + /// The value an element holds, on the prover's side. + fn value(&self, s: Sym) -> F192 { + match s { + Sym::Pub(c) => c, + Sym::Hid(i) => self.values.as_ref().map_or(F192::ZERO, |v| v[i as usize]), + } + } + + /// A form's value, on the prover's side. + fn eval(&self, f: &Form) -> F192 { + (f.terms.iter()).fold(f.constant, |acc, &(v, c)| { + acc + c * match v { + Var::Key(i) => self.keys.get(i as usize).copied().unwrap_or(F192::ZERO), + Var::Aux(j) => self.record.aux_values.get(j as usize).copied().unwrap_or(F192::ZERO), + } + }) + } + + /// Store a form: public when it has no term. + fn push(&mut self, form: Form, value: impl FnOnce(&Self) -> F192) -> Sym { + if form.terms.is_empty() { + return Sym::Pub(form.constant); + } + if self.values.is_some() { + let v = value(self); + if let Some(values) = &mut self.values { + values.push(v); + } + } + let index = u32::try_from(self.record.forms.len()).expect("fewer than 2^32 forms"); + self.record.forms.push(form); + Sym::Hid(index) + } + + /// `ca·a + cb·b`. + fn lin(&mut self, a: Sym, ca: F192, b: Sym, cb: F192) -> Sym { + let (fa, fb) = match (a, b) { + (Sym::Pub(x), Sym::Pub(y)) => return Sym::Pub(ca * x + cb * y), + _ => (self.form_ref(a), self.form_ref(b)), + }; + let mut terms = Vec::with_capacity(fa.1.len() + fb.1.len()); + let (mut i, mut j) = (0, 0); + let (ta, tb) = (fa.1, fb.1); + while i < ta.len() || j < tb.len() { + let next = match (ta.get(i), tb.get(j)) { + (Some(&(va, x)), Some(&(vb, _))) if va < vb => { + i += 1; + (va, ca * x) + } + (Some(&(va, _)), Some(&(vb, y))) if vb < va => { + j += 1; + (vb, cb * y) + } + (Some(&(v, x)), Some(&(_, y))) => { + i += 1; + j += 1; + (v, ca * x + cb * y) + } + (Some(&(v, x)), None) => { + i += 1; + (v, ca * x) + } + (None, Some(&(v, y))) => { + j += 1; + (v, cb * y) + } + (None, None) => unreachable!("one side has a term left"), + }; + if next.1 != F192::ZERO { + terms.push(next); + } + } + let form = Form { + constant: ca * fa.0 + cb * fb.0, + terms, + }; + self.push(form, |r| ca * r.value(a) + cb * r.value(b)) + } + + /// An element's constant and terms, borrowed. + fn form_ref(&self, s: Sym) -> (F192, &[(Var, F192)]) { + match s { + Sym::Pub(c) => (c, &[]), + Sym::Hid(i) => { + let f = &self.record.forms[i as usize]; + (f.constant, &f.terms) + } + } + } + + /// The auxiliary variable of this definition, made unless it exists: a monic form of it. + fn aux(&mut self, kind: Kind, a: Form, b: Form) -> Sym { + let mut h = Hasher::new(); + h.update(&[kind as u8]); + h.update(&self.record.digest(&a)); + if kind == Kind::Product { + h.update(&self.record.digest(&b)); + } + let digest = h.finalize(); + let j = match self.by_digest.get(&digest) { + Some(&j) => j, + None => { + let j = self.n_aux(); + if self.values.is_some() { + let v = match kind { + Kind::Product => self.eval(&a) * self.eval(&b), + Kind::Inverse => self.eval(&a).inv(), + Kind::Bind => self.eval(&a), + }; + self.record.aux_values.push(v); + } + self.record.aux.push(Aux { kind, a, b, digest }); + self.by_digest.insert(digest, j); + j + } + }; + let form = Form { + constant: F192::ZERO, + terms: vec![(Var::Aux(j), F192::ONE)], + }; + self.push(form, |r| { + r.record.aux_values.get(j as usize).copied().unwrap_or(F192::ZERO) + }) + } + + /// Record a statement about a form, once. + fn state(&mut self, f: Form, boolean: bool) { + if self.values.is_some() { + let v = self.eval(&f); + let holds = if boolean { v * v == v } else { v == F192::ZERO }; + debug_assert!(holds, "the prover's own proof satisfies each constraint"); + } + let mut h = Hasher::new(); + h.update(&[u8::from(boolean)]); + h.update(&self.record.digest(&f)); + let digest = h.finalize(); + if self.stated.insert(digest) { + let list = if boolean { + &mut self.record.booleans + } else { + &mut self.record.linear + }; + list.push((digest, f)); + } + } + + /// Record that a hidden value is a bit: `b·b = b`. + pub(crate) fn boolean(&mut self, b: Sym) { + let f = self.form(b); + assert!(!f.terms.is_empty(), "a bit the proof hides"); + self.state(f, true); + } + + /// Whether every element is public, and their values. + pub(crate) fn publics(xs: &[Sym]) -> Option> { + xs.iter() + .map(|&x| match x { + Sym::Pub(c) => Some(c), + Sym::Hid(_) => None, + }) + .collect() + } +} + +impl Arith for Recorder { + type E = Sym; + + fn constant(&mut self, c: F192) -> Sym { + Sym::Pub(c) + } + + fn mul_add(&mut self, a: Sym, b: Sym, d: Sym) -> Sym { + match (a, b) { + (Sym::Pub(x), Sym::Pub(y)) => self.lin(Sym::Pub(x * y), F192::ONE, d, F192::ONE), + (Sym::Pub(x), h) | (h, Sym::Pub(x)) => self.lin(h, x, d, F192::ONE), + (Sym::Hid(_), Sym::Hid(_)) => { + let (la, ma) = self.record.monic(&self.form(a)); + let (lb, mb) = self.record.monic(&self.form(b)); + let (ma, mb) = if self.record.digest(&ma) <= self.record.digest(&mb) { + (ma, mb) + } else { + (mb, ma) + }; + let p = self.aux(Kind::Product, ma, mb); + self.lin(p, la * lb, d, F192::ONE) + } + } + } + + fn add(&mut self, a: Sym, d: Sym) -> Sym { + self.lin(a, F192::ONE, d, F192::ONE) + } + + fn mul_const_add(&mut self, a: Sym, c: F192, d: Sym) -> Sym { + self.lin(a, c, d, F192::ONE) + } + + fn inv(&mut self, a: Sym) -> Sym { + match a { + Sym::Pub(x) => Sym::Pub(if x.is_zero() { F192::ZERO } else { x.inv() }), + Sym::Hid(_) => { + let (la, ma) = self.record.monic(&self.form(a)); + let y = self.aux(Kind::Inverse, ma, Form::default()); + self.lin(y, la.inv(), Sym::Pub(F192::ZERO), F192::ONE) + } + } + } + + fn frobenius2(&mut self, a: Sym) -> Sym { + match a { + Sym::Pub(x) => Sym::Pub(x.frobenius().frobenius()), + Sym::Hid(_) => unreachable!("the verifier applies the Frobenius to public values only"), + } + } + + /// A hidden element gets a variable of its own, tied to its monic form by one linear constraint. + fn bind(&mut self, a: Sym) -> Sym { + match a { + Sym::Pub(_) => a, + Sym::Hid(_) => { + let (la, ma) = self.record.monic(&self.form(a)); + let y = self.aux(Kind::Bind, ma, Form::default()); + self.lin(y, la, Sym::Pub(F192::ZERO), F192::ONE) + } + } + } + + fn public_mle(&mut self, values: &[F64], point: &[Sym]) -> Sym { + Self::publics(point).map_or_else( + || { + let eq = self.eq_table(point); + let zero = self.zero(); + (eq.iter().zip(values)).fold(zero, |acc, (&e, &v)| self.mul_const_add(e, F192::from(v), acc)) + }, + |p| Sym::Pub(mle_eval_par(values, &p)), + ) + } +} + +impl PublicColumns for Recorder {} + +impl> Verifier for Recorder { + fn next_scalar(&mut self) -> Result { + let c = self.t.next_scalar()?; + if !self.hidden { + return Ok(Sym::Pub(c)); + } + let i = self.record.n_keys; + self.record.n_keys += 1; + let form = Form { + constant: c, + terms: vec![(Var::Key(i), F192::ONE)], + }; + let key = self.keys.get(i as usize).copied().unwrap_or(F192::ZERO); + Ok(self.push(form, |_| c + key)) + } + + fn next_round_poly(&mut self, n_coeffs: usize, claim: Sym, eq: Option) -> Result, TranscriptError> { + assert!(n_coeffs >= 2, "a round polynomial has at least two coefficients"); + // The sent coefficients bind in index order, as the native reader binds them. + let fixed = usize::from(eq.is_none()); + let mut coeffs = vec![Sym::Pub(F192::ZERO); n_coeffs]; + for i in (0..n_coeffs).filter(|&i| i != fixed) { + coeffs[i] = self.next_scalar()?; + } + let zero = self.zero(); + let sum_from = |r: &mut Self, from: usize| coeffs[from..].iter().fold(zero, |acc, &c| r.add(acc, c)); + coeffs[fixed] = match eq { + None => { + let s = sum_from(self, 2); + self.add(claim, s) + } + Some(r) => { + let s = sum_from(self, 1); + self.mul_add(r, s, claim) + } + }; + Ok(coeffs) + } + + fn sample(&mut self) -> Sym { + Sym::Pub(self.t.sample()) + } + + fn grind_check(&mut self, bits: u32) -> Result<(), TranscriptError> { + self.t.grind_check(bits) + } + + /// Equal values are checked; a hidden difference is one linear constraint, on its monic form. + fn ensure_eq(&mut self, a: Sym, b: Sym, err: impl FnOnce() -> Er) -> Result<(), Er> { + match self.add(a, b) { + Sym::Pub(d) => { + if d == F192::ZERO { + Ok(()) + } else { + Err(err()) + } + } + d @ Sym::Hid(_) => { + let (_, monic) = self.record.monic(&self.form(d)); + self.state(monic, false); + Ok(()) + } + } + } + + /// The proof goes on past the inner verifier's end: the outer proof and its opening follow, so the caller finishes. + fn finish(&mut self) -> Result<(), TranscriptError> { + Ok(()) + } + + fn set_hidden(&mut self, hidden: bool) { + self.hidden = hidden; + } + + fn sample_vec(&mut self, n: usize) -> Vec { + self.t.sample_vec(n).into_iter().map(Sym::Pub).collect() + } +} + +impl> OpeningVerifier for Recorder { + type Root = Hash; + type K = F64; + type Query = usize; + + fn next_root(&mut self) -> Result { + assert!(!self.hidden, "a root is never hidden"); + self.t.next_root() + } + + fn sample_queries(&mut self, depth: usize, count: usize) -> Vec { + self.t.sample_queries(depth, count) + } + + fn open_rows( + &mut self, + root: &Hash, + depth: usize, + queries: &[usize], + row_words: usize, + leaf_words: usize, + ) -> Result>, TranscriptError> { + self.t.open_rows(root, depth, queries, row_words, leaf_words) + } + + fn mul_k_add(&mut self, a: Sym, k: F64, d: Sym) -> Sym { + self.lin(a, F192::from(k), d, F192::ONE) + } + + fn e_of_limbs(&mut self, limbs: [F64; 3]) -> Sym { + Sym::Pub(F192::new(limbs[0].0, limbs[1].0, limbs[2].0)) + } + + fn query_point(&mut self, query: &usize) -> Sym { + Sym::Pub(self.t.query_point(query)) + } +} diff --git a/crates/pcs/benches/throughput.rs b/crates/pcs/benches/throughput.rs index d48d9d338..b0ea39265 100644 --- a/crates/pcs/benches/throughput.rs +++ b/crates/pcs/benches/throughput.rs @@ -71,16 +71,7 @@ fn main() { let mut ch = ProverState::from_label(b"pcs-throughput"); let t = Instant::now(); tracing::info_span!("PCS open").in_scope(|| { - recursive_prover_with_basis( - &pc, - log_n, - &witness, - b_initial.to_vec(), - target, - &pd.codeword, - &pd.merkle_tree, - &mut ch, - ); + recursive_prover_with_basis(&pc, log_n, &witness, b_initial.to_vec(), target, &pd, None, &mut ch); }); open_t.push(t.elapsed().as_secs_f64()); black_box((cm, ch.into_proof())); diff --git a/crates/pcs/src/ntt.rs b/crates/pcs/src/ntt.rs index 4ae5080da..824567ce3 100644 --- a/crates/pcs/src/ntt.rs +++ b/crates/pcs/src/ntt.rs @@ -3,4 +3,4 @@ pub(crate) mod additive_ntt_f64; pub use additive_ntt_f64::AdditiveNttF64; -pub(crate) use additive_ntt_f64::{RowSink, transpose_lane_major}; +pub(crate) use additive_ntt_f64::{Pad, RowSink, transpose_lane_major}; diff --git a/crates/pcs/src/ntt/additive_ntt_f64.rs b/crates/pcs/src/ntt/additive_ntt_f64.rs index e2e1f657b..24fabc19a 100644 --- a/crates/pcs/src/ntt/additive_ntt_f64.rs +++ b/crates/pcs/src/ntt/additive_ntt_f64.rs @@ -66,6 +66,45 @@ fn span_get(basis: &[F64], idx: usize) -> F64 { /// Receives a finished block of codeword rows, as `(first_row, rows)`. pub(crate) type RowSink<'a> = dyn Fn(usize, &[F64]) + Sync + 'a; +/// A padding past the power of two `2^m` of each interleaved lane's message. +/// +/// - `rows` is `k` rows of the lanes, the padding's coefficient `j` of every lane in row `j`. +/// - Each lane then encodes `sum_j msg_j X_j + (W_m + offset) sum_j pad_j X_j`, of `2^m + k` coefficients in the novel basis since `X_{2^m + j} = W_m X_j`. +/// - `W_m` vanishes on the first replica's points, so only an `offset` outside `W_m`'s image of the domain leaves no point unpadded. +#[derive(Clone, Copy)] +pub(crate) struct Pad<'a> { + pub(crate) rows: &'a [F64], + pub(crate) offset: F64, +} + +/// A padding, and the factor each replica takes it with. +/// +/// `W_m` is constant on each replica's coset of the domain, so replica `c` of the message starts as the message plus `scales[c] = W_m(c 2^m) + offset` times the padding. +#[derive(Clone, Copy)] +struct Padding<'a> { + words: &'a [F64], + scales: &'a [F64], +} + +impl Padding<'_> { + /// Add replica `replica`'s padding to `dst`, which holds the replica's words from `first` on. + fn add(&self, dst: &mut [F64], replica: usize, first: usize) { + let scale = self.scales[replica]; + if let Some(tail) = self.words.get(first..) { + for (d, &p) in dst.iter_mut().zip(tail) { + *d += scale * p; + } + } + } +} + +/// Where the first pass of an encode reads its message, and the padding it adds. +#[derive(Clone, Copy)] +struct Source<'a> { + msg: SendPtr, + pad: Option>, +} + /// Additive NTT over F_{2^64} with the standard polynomial-basis subspace /// `{1, x, x², …}`: the F_2-subspace is `{0, 1, …, 2^ℓ−1}` under the natural /// integer encoding, exactly as in the extension-field version (whose domain already @@ -129,6 +168,13 @@ impl AdditiveNttF64 { [t0, a, a + d, c, c + e0, c + e1, c + e0 + e1] } + /// `W_m` on replica `c`'s coset, for an encode entering at layer `start`. + /// + /// It is what layer `start - 1`'s butterfly `u' = u + t v, v' = u' + v` gives a message `u` over a padding `v`. + fn pad_scale(&self, start: usize, replica: usize) -> F64 { + self.twiddle(start - 1, replica >> 1) + if replica & 1 == 1 { F64::ONE } else { F64::ZERO } + } + /// RS-encode a message already stored in the codeword's first replica. /// /// # Overview @@ -152,7 +198,7 @@ impl AdditiveNttF64 { pub fn encode_interleaved_in_place(&self, data: &mut [F64], num_ntts: usize, log_inv_rate: usize) { // The message is the buffer's own first replica. let msg = SendPtr(data.as_mut_ptr()); - self.transform(data, num_ntts, log_inv_rate, Some(msg), None); + self.transform(data, num_ntts, log_inv_rate, Some(msg), None, None); } /// Encode in place, handing `on_rows` every finished block of rows. @@ -161,15 +207,22 @@ impl AdditiveNttF64 { /// - Each row is handed over exactly once. /// - Blocks are aligned, and all of one power-of-two size. /// - A block is handed over while its rows are still in cache. + /// + /// With a [`Pad`], each lane encodes its `2^m + k` coefficients on the same domain: layer `r - 1` is the one butterfly that pairs the message with the padding, folded into the first pass's read. + /// + /// # Panics + /// + /// With a padding, panics unless `r >= 1`, the NTT's domain is the codeword's, and `k <= 2^m`. pub(crate) fn encode_interleaved_in_place_with( &self, data: &mut [F64], num_ntts: usize, log_inv_rate: usize, + pad: Option>, on_rows: &RowSink<'_>, ) { let msg = SendPtr(data.as_mut_ptr()); - self.transform(data, num_ntts, log_inv_rate, Some(msg), Some(on_rows)); + self.transform(data, num_ntts, log_inv_rate, Some(msg), pad, Some(on_rows)); } /// RS-encode a message held in a buffer of its own, handing `on_rows` every finished block of rows. @@ -196,7 +249,7 @@ impl AdditiveNttF64 { ); // Read-only from here on: the pointer only feeds the first pass's reads. let msg = SendPtr(msg.as_ptr().cast_mut()); - self.transform(data, num_ntts, log_inv_rate, Some(msg), Some(on_rows)); + self.transform(data, num_ntts, log_inv_rate, Some(msg), None, Some(on_rows)); } /// Run layers `start..d` of a `2^d`-row transform in as few sweeps of the buffer as possible. @@ -223,6 +276,7 @@ impl AdditiveNttF64 { /// /// - The layer-`start` blocks are not in the buffer yet: each is a copy of the message. /// - The first pass reads its rows from the message instead. + /// - With a padding, it adds each replica's share of it to the rows it reads, so the padding costs no sweep. /// /// # Why block 0 goes last /// @@ -240,6 +294,7 @@ impl AdditiveNttF64 { num_ntts: usize, start: usize, msg: Option>, + pad: Option>, on_rows: Option<&RowSink<'_>>, ) { // The buffer is 2^log_d rows of `num_ntts` words. @@ -249,6 +304,27 @@ impl AdditiveNttF64 { assert!(log_d <= self.log_domain_size()); assert!(start <= log_d); + // The padding's factor on each replica, which the layers before `start` would have given it. + let scales: Vec = pad.map_or_else(Vec::new, |pad| { + assert!(msg.is_some() && start >= 1, "a padding rides an encode's message"); + assert_eq!( + log_d, + self.log_domain_size(), + "a padding needs the codeword's own domain" + ); + assert!( + pad.rows.len().is_multiple_of(num_ntts) && pad.rows.len() <= data.len() >> start, + "a padding is at most one replica of whole rows" + ); + (0..1usize << start) + .map(|c| self.pad_scale(start, c) + pad.offset) + .collect() + }); + let pad = pad.map(|pad| Padding { + words: pad.rows, + scales: &scales, + }); + /// Below this domain the transform is too small to split across the pool. const PARALLEL_FLOOR_LOG_D: usize = 12; /// Fewest rows a deep sub-block takes when splitting for parallelism. @@ -291,7 +367,7 @@ impl AdditiveNttF64 { // Phase 1: gathered passes, each at most one L2 group of layers. // // Only the first one reads the message. - let mut msg = msg; + let mut msg = msg.map(|msg| Source { msg, pad }); let mut layer = start; while layer < deep_start { let g = (deep_start - layer).min(fit2); @@ -303,7 +379,7 @@ impl AdditiveNttF64 { // // message is block 0 of the buffer -> a task could overwrite it while others still copy it // no layer left to run -> no deep task would write the buffer at all - if let Some(m) = msg.take_if(|m| std::ptr::eq(m.0, data.as_mut_ptr()) || deep_start == log_d) { + if let Some(m) = msg.take_if(|m| std::ptr::eq(m.msg.0, data.as_mut_ptr()) || deep_start == log_d) { replicate(data, m, data.len() >> start); } @@ -335,7 +411,10 @@ impl AdditiveNttF64 { // - The external message is valid for one whole replica of words. // - It is disjoint from the codeword. // - This sub-block ends inside its replica, so the read stays in bounds. - sub.copy_from_slice(unsafe { std::slice::from_raw_parts(m.add(off), sub_len) }); + sub.copy_from_slice(unsafe { std::slice::from_raw_parts(m.msg.add(off), sub_len) }); + if let Some(pad) = m.pad { + pad.add(sub, (first_sub + i) * sub_len / block_len, off); + } self.run_layers(sub, log_d, num_ntts, deep_start, log_d, deep_start, first_sub + i); } if let Some(f) = deep_rows { @@ -392,7 +471,7 @@ impl AdditiveNttF64 { /// /// # With a message /// - /// - Every block's rows come from the message. + /// - Every block's rows come from the message, plus the block's share of the padding. /// - One task takes one residue across all blocks, block 0 last. #[allow(clippy::too_many_arguments)] fn gathered_pass( @@ -402,7 +481,7 @@ impl AdditiveNttF64 { num_ntts: usize, layer: usize, g: usize, - msg: Option>, + msg: Option>, stream: bool, ) { // A group is 2^g rows, `step` rows apart. @@ -421,6 +500,8 @@ impl AdditiveNttF64 { // Row `i` of the group, as a word offset inside its block. let row = |i: usize| (r + (i << log_step)) * num_ntts; let block_off = (block << (log_d - layer)) * num_ntts; + // The first pass enters at the message's layer, so a block is a replica. + let pad = msg.and_then(|m| m.pad).filter(|p| row(0) < p.words.len()); // Gather: the scattered rows become one contiguous 2^g-row buffer. for (i, dst) in scratch.chunks_exact_mut(num_ntts).enumerate() { // SAFETY: @@ -429,11 +510,14 @@ impl AdditiveNttF64 { // - Block 0 is written last, after every read of the message in it. let src = unsafe { match msg { - Some(m) => std::slice::from_raw_parts(m.add(row(i)), num_ntts), + Some(m) => std::slice::from_raw_parts(m.msg.add(row(i)), num_ntts), None => base.slice(block_off + row(i), num_ntts), } }; dst.copy_from_slice(src); + if let Some(pad) = pad { + pad.add(dst, block, row(i)); + } } // Transform: a (layer + g)-layer domain whose sub-block index is the global block. self.run_layers(scratch, layer + g, num_ntts, layer, layer + g, layer, block); @@ -776,14 +860,15 @@ fn with_scratch(len: usize, f: impl FnOnce(&mut [F64]) -> R) -> R { }) } -/// Fill every replica of the buffer with a copy of the message. +/// Fill every replica of the buffer with a copy of the message, plus the replica's share of any padding. /// /// - This is the unfused form of a gathered first pass. -/// - The message may be the buffer's own first replica, which is then left as it is. -fn replicate(data: &mut [F64], msg: SendPtr, msg_len: usize) { +/// - The message may be the buffer's own first replica, which then takes its share of a padding once every copy of it is made. +fn replicate(data: &mut [F64], src: Source<'_>, msg_len: usize) { // Copy granularity: small enough to spread a short message over every worker. const CHUNK: usize = 1 << 14; let replicas = data.len() / msg_len; + let msg = src.msg; let in_place = std::ptr::eq(msg.0, data.as_mut_ptr()); let chunks = msg_len.div_ceil(CHUNK); let dst = SendPtr(data.as_mut_ptr()); @@ -799,11 +884,19 @@ fn replicate(data: &mut [F64], msg: SendPtr, msg_len: usize) { // SAFETY: // - Only this task writes this range. // - The range skips replica 0, so it never overlaps a message stored there. - unsafe { - let src = std::slice::from_raw_parts(msg.add(start), len); - dst.slice(replica * msg_len + start, len).copy_from_slice(src); + let out = unsafe { + let words = std::slice::from_raw_parts(msg.add(start), len); + let out = dst.slice(replica * msg_len + start, len); + out.copy_from_slice(words); + out + }; + if let Some(pad) = src.pad { + pad.add(out, replica, start); } }); + if in_place && let Some(pad) = src.pad { + pad.add(&mut data[..msg_len], 0, 0); + } } /// Layers L and L+1 fused into one sweep over a layer-L block, four rows at a time. @@ -1269,7 +1362,7 @@ mod tests { let mut a = orig.clone(); forward_scalar_from_layer(&ntt, &mut a, 1, 0); let mut c = orig.clone(); - ntt.transform(&mut c, 1, 0, None, None); + ntt.transform(&mut c, 1, 0, None, None, None); assert_eq!(a, c, "parallel == scalar at log_d={log_d}"); ntt.inverse_transform(&mut a); @@ -1309,7 +1402,7 @@ mod tests { forward_scalar_from_layer(&ntt, &mut want, lanes, start_layer); // Under test: the pass-planning driver. let mut got = original; - ntt.transform(&mut got, lanes, start_layer, None, None); + ntt.transform(&mut got, lanes, start_layer, None, None, None); assert_eq!(got, want, "log_d={log_d}, lanes={lanes}, start_layer={start_layer}"); } @@ -1354,7 +1447,7 @@ mod tests { let mut got = vec![F64::ZERO; msg_len << log_inv_rate]; got[..msg_len].copy_from_slice(&msg); let blocks = Mutex::new(Vec::new()); - ntt.encode_interleaved_in_place_with(&mut got, lanes, log_inv_rate, &|row, rows| { + ntt.encode_interleaved_in_place_with(&mut got, lanes, log_inv_rate, None, &|row, rows| { blocks.lock().unwrap().push((row, rows.to_vec())); }); assert_eq!(got, want, "log_d={log_d}, lanes={lanes}, rate={log_inv_rate}"); @@ -1375,6 +1468,41 @@ mod tests { } } + #[test] + fn a_padded_encode_is_the_same_from_a_message_held_elsewhere() { + // Invariant: the padding lands the same whichever pass first reads the message. + // + // (log_d, lanes, rate, k) in place held elsewhere + // (7, 7, 2, 5) replicate, then deep pass deep pass copying the message + // (9, 2048, 1, 13) gathered first pass gathered first pass + // (4, 8, 4, 1) replicate, no layer left replicate, no layer left + // + // The in-place encode is checked against direct evaluation by the hiding commitment's test. + let mut rng = Rng::new(0x9AD5); + for (log_d, lanes, log_inv_rate, k) in [(7usize, 7usize, 2usize, 5usize), (9, 2048, 1, 13), (4, 8, 4, 1)] { + let ntt = AdditiveNttF64::standard(log_d); + let msg_len = (lanes << log_d) >> log_inv_rate; + let msg: Vec = (0..msg_len).map(|_| F64(rng.next_u64())).collect(); + let pad: Vec = (0..k * lanes).map(|_| F64(rng.next_u64())).collect(); + + let mut in_place = vec![F64::ZERO; msg_len << log_inv_rate]; + in_place[..msg_len].copy_from_slice(&msg); + let pad = Some(Pad { + rows: &pad, + offset: F64(rng.next_u64()), + }); + ntt.encode_interleaved_in_place_with(&mut in_place, lanes, log_inv_rate, pad, &|_, _| {}); + + let mut elsewhere = vec![F64::ZERO; msg_len << log_inv_rate]; + let src = SendPtr(msg.as_ptr().cast_mut()); + ntt.transform(&mut elsewhere, lanes, log_inv_rate, Some(src), pad, None); + assert_eq!( + elsewhere, in_place, + "log_d={log_d}, lanes={lanes}, rate={log_inv_rate}, k={k}" + ); + } + } + /// Every lane of the codeword must be exactly the single-lane RS codeword of /// that lane's contiguous message block, which is what makes a commitment over /// `n_lanes` lanes equal to the `2^log_batch_size`-lane one with a zero tail. @@ -1406,7 +1534,7 @@ mod tests { let block = n_lanes - 1 - lane; let mut want = vec![F64::ZERO; block_len]; replicate_rows(&mut want, &msg[block * rows..(block + 1) * rows]); - ntt.transform(&mut want, 1, log_inv_rate, None, None); + ntt.transform(&mut want, 1, log_inv_rate, None, None, None); for pos in 0..block_len { assert_eq!( got[pos * n_lanes + lane], @@ -1433,7 +1561,7 @@ mod tests { // The whole interleaved buffer through the planner. let mut got = soa.clone(); - ntt.transform(&mut got, lanes, 0, None, None); + ntt.transform(&mut got, lanes, 0, None, None, None); // Each lane on its own through the scalar transform. for lane in 0..lanes { @@ -1462,7 +1590,7 @@ mod tests { per_lane[lane][pos] = v; } } - ntt.transform(&mut soa, lanes, 0, None, None); + ntt.transform(&mut soa, lanes, 0, None, None, None); for (lane, lane_data) in per_lane.iter_mut().enumerate() { forward_scalar_from_layer(&ntt, lane_data, 1, 0); for pos in 0..n { diff --git a/crates/pcs/src/ring_switch.rs b/crates/pcs/src/ring_switch.rs index 2e036ca0b..9a30e2ab0 100644 --- a/crates/pcs/src/ring_switch.rs +++ b/crates/pcs/src/ring_switch.rs @@ -445,6 +445,8 @@ impl RingShare<'_, E> { *f = a.mul_add(scale, s, *f); } } + // Each slice enters every one of the map's 64 terms. + let family: Vec = family.into_iter().map(|f| a.bind(f)).collect(); self.map.target(a, &family) } @@ -901,8 +903,8 @@ pub(crate) mod tests { &packed, rs_eq_ind.to_vec(), sumcheck_claim, - &pd.codeword, - &pd.merkle_tree, + &pd, + None, &mut ps, ); E2e { @@ -948,6 +950,7 @@ pub(crate) mod tests { 1 << e.vc.initial_k(), sumcheck_claim, e.root, + None, |_, point| inner_product_ext(&rs_eq_ind, &eq_table(point)), ) .is_ok() @@ -968,6 +971,7 @@ pub(crate) mod tests { 1 << e.vc.initial_k(), sumcheck_claim, e.root, + None, |_, point| eval_rs_eq(&e.suffix_point, F192::ONE, &map, point), ) .is_ok() diff --git a/crates/pcs/src/stack_open.rs b/crates/pcs/src/stack_open.rs index efa67aa92..384dd071d 100644 --- a/crates/pcs/src/stack_open.rs +++ b/crates/pcs/src/stack_open.rs @@ -53,10 +53,22 @@ //! challenge, as the table sumcheck's xi ranges do (the batching step of `thm:rbr`). //! `lambda` is drawn after the map, so the family's error is fixed by then and is the //! constant term of the batched error, which is what lets it take `lambda^0 = 1`. +//! +//! ## The hiding opening +//! +//! A commitment made by [`super::whir::commit_hiding`] pads each committed lane past its power of two `2^m` with `k` uniform coefficients, `k = q_0 + 2` ([`super::whir::ProverConfig::padding`]), and the caller makes its last committed lane `R` uniform, outside every claim. Opened with [`Hiding`], the opening is the one above with three changes: +//! +//! - after the lane fold's last challenge, with `hidden_claim`, the prover turns its transcript's hiding off and sends the running claim `a` in the clear, which the verifier checks against the claim it holds (an expression of keyed scalars in the zero-knowledge proof) and continues from; +//! - the prover then sends `g_1[j] = sum_u eq(fold, u) pad_u[j]`, `j < k`, the padding folded as the lanes are; +//! - a level-0 query's folded row is the folded padded codeword at its point `x`, from which the verifier takes `W_m(x) sum_j g_1[j] X_j(x)` before weighting it, leaving the codeword of the folded message the rest of WHIR proves about. +//! +//! What the opening reveals is then hidden as follows (the PCS annex, `sec:pcs-zk`). Any `q_0 + 1` symbols of a padded lane are uniform, so level 0's opened rows are; a root hides each unopened leaf behind the uniform symbol each lane keeps there, in the random-oracle model. The claim's weight is zero on `R`, so the lane fold mixes `R` into the folded vector with the coefficient `eq(fold, R)`, and every later message (the round messages, `a`, the out-of-domain answers, the opened rows of later levels, the residual) is a linear functional of a vector `R` masks, and every later root a random-oracle hash of one: as long as the functionals span at most half the lane's `2^m` dimensions over `K`, they are uniform. This last step adapts VEIL's Lemma 4.7 to an `E`-fold of `K` lanes and is argued, not proven. `g_1` is uniform and independent of the rest, by the padding. use super::ring_switch::{self, RingFamily, RingSwitch, SliceClaim}; use super::verifier::OpeningVerifier; -use super::whir::{ProverConfig, ProverData, VerifierConfig, WhirError, recursive_verifier_with_basis_succinct}; +use super::whir::{ + Hiding, ProverConfig, ProverData, VerifierConfig, WhirError, recursive_verifier_with_basis_succinct, +}; use basis::StackWeight; use fiat_shamir::arith::{Arith, Native}; use fiat_shamir::transcript::Transmitter; @@ -156,6 +168,12 @@ impl StackClaim { /// exactly the weight's zero region. `config.initial_k` / `config.log_inv_rates[0]` /// must match the commit's `log_batch_size` / `log_inv_rate` (enforced by shape /// asserts inside the WHIR prover). +/// +/// With `hiding`, `prover_data` is a [`super::whir::commit_hiding`] commitment, padded by `hiding.k` coefficients a lane (the module docs). +#[expect( + clippy::too_many_arguments, + reason = "The opening keeps its independent inputs explicit." +)] pub fn open( ps: &mut impl Transmitter, log_n: usize, @@ -164,6 +182,7 @@ pub fn open( config: &ProverConfig, point_claims: &[StackClaim], rings: &[RingSwitch], + hiding: Option, ) { for ring in rings { let qflock_len = 1usize << ring.qflock_vars; @@ -239,9 +258,9 @@ pub fn open( stack, basis, target, - &prover_data.codeword, - &prover_data.merkle_tree, + prover_data, Some(initial), + hiding, ps, ); } @@ -254,9 +273,15 @@ pub fn open( /// /// The verifier is the native one or the recursion machine's rows, which run the same steps. /// +/// `hiding` is the opening's, as [`open`] was given it. +/// /// # Errors /// /// Returns a statement whose regions or claims leave the committed cube, then the WHIR verifier's refusal. +#[expect( + clippy::too_many_arguments, + reason = "The opening keeps its independent inputs explicit." +)] pub fn verify( v: &mut V, config: &VerifierConfig, @@ -265,6 +290,7 @@ pub fn verify( root: V::Root, point_claims: &[StackClaim], rings: &[RingSwitch], + hiding: Option, ) -> Result<(), WhirError> { check_statement(log_n, point_claims, rings)?; @@ -289,7 +315,7 @@ pub fn verify( }) }; v.scope("whir", |v| { - recursive_verifier_with_basis_succinct(v, config, log_n, n_lanes, target, root, weight_at) + recursive_verifier_with_basis_succinct(v, config, log_n, n_lanes, target, root, hiding, weight_at) }) } @@ -324,7 +350,10 @@ mod tests { use super::*; use crate::ring_switch::tests::s_hat_v_reference; use crate::whir::config::tests::{default_config, test_config_for}; - use crate::whir::{INITIAL_BASIS_CHUNK, commit, inner_product_base_ext}; + use crate::whir::{ + Hiding, INITIAL_BASIS_CHUNK, MIN_LOG_N_HIDING, commit, commit_hiding, config_for_rate_hiding, + inner_product_base_ext, + }; use basis::StackWeight; use fiat_shamir::merkle::Hash; use fiat_shamir::transcript::{ProofTranscript, ProverState, VerifierState}; @@ -532,7 +561,7 @@ mod tests { ); let (cm, pd) = commit(&stack, log_n, pc.initial_k(), pc.log_inv_rates()[0]); let mut ps = ProverState::from_label(DOMAIN); - open(&mut ps, log_n, &stack, &pd, &pc, &point_claims, &rings); + open(&mut ps, log_n, &stack, &pd, &pc, &point_claims, &rings, None); Instance { vc: pc, @@ -559,6 +588,7 @@ mod tests { inst.root, point_claims, rings, + None, ) .is_ok() } @@ -688,6 +718,7 @@ mod tests { &pc, &point_claims, std::slice::from_ref(&ring), + None, ); let fs = ps.into_proof(); @@ -700,7 +731,8 @@ mod tests { 1 << pc.initial_k(), cm.root, &point_claims, - std::slice::from_ref(&ring) + std::slice::from_ref(&ring), + None, ) .is_ok(), "honest crossing-regime opening rejected" @@ -718,10 +750,187 @@ mod tests { 1 << pc.initial_k(), cm.root, &point_claims, - std::slice::from_ref(&bad_ring) + std::slice::from_ref(&bad_ring), + None, ) .is_err(), "tampered crossing-regime ring slice accepted" ); } + + /// A hiding statement: data lanes, then one uniform lane `R` no claim touches. + struct HidingStatement { + log_n: usize, + config: ProverConfig, + stack: Vec, + point_claims: Vec, + rings: Vec, + } + + impl HidingStatement { + fn new(log_inv_rate: usize, n_lanes: usize, seed: u64) -> Self { + let log_n = MIN_LOG_N_HIDING; + let config = config_for_rate_hiding(log_n, log_inv_rate).unwrap(); + let lane_vars = log_n - config.initial_k(); + let mut rng = Rng::new(seed); + let stack: Vec = (0..n_lanes << lane_vars).map(|_| F64(rng.next_u64())).collect(); + // A ring-switched claim on the first two lanes, a point claim on the next: none reaches `R`, the last. + let qflock_vars = lane_vars + 1; + let suffix_point = rng.ext_vec(qflock_vars); + let s_hat_v = s_hat_v_reference(&stack[..1 << qflock_vars], &suffix_point); + let rings = vec![RingSwitch { + offset: 0, + qflock_vars, + claims: vec![SliceClaim { suffix_point, s_hat_v }], + }]; + let offset = 2 << lane_vars; + let low_point = rng.ext_vec(lane_vars); + let value = inner_product_base_ext(&stack[offset..offset + (1 << lane_vars)], &eq_table(&low_point)); + let point_claims = vec![StackClaim::Point { + offset, + low_point, + value, + }]; + assert!(n_lanes > 3, "the claims leave the last lane alone"); + Self { + log_n, + config, + stack, + point_claims, + rings, + } + } + + const fn n_lanes(&self) -> usize { + self.stack.len() >> (self.log_n - self.config.initial_k()) + } + + /// Each lane's `k` uniform padding coefficients. + fn pads(&self, seed: u64) -> Vec { + let mut rng = Rng::new(seed); + (0..self.config.padding() * self.n_lanes()) + .map(|_| F64(rng.next_u64())) + .collect() + } + + const fn hiding(&self, hidden_claim: bool) -> Hiding { + Hiding { + k: self.config.padding(), + hidden_claim, + } + } + + /// Commit with these pads and open, the prover holding `prover_pads` as the commitment's. + fn prove(&self, pads: &[F64], prover_pads: Option>, hidden_claim: bool) -> (Hash, ProofTranscript) { + let (cm, mut pd) = commit_hiding( + &self.stack, + self.log_n, + self.config.initial_k(), + self.config.log_inv_rates()[0], + pads, + ); + if let Some(prover_pads) = prover_pads { + pd.pads = prover_pads; + } + let mut ps = ProverState::from_label(DOMAIN); + open( + &mut ps, + self.log_n, + &self.stack, + &pd, + &self.config, + &self.point_claims, + &self.rings, + Some(self.hiding(hidden_claim)), + ); + (cm.root, ps.into_proof()) + } + + fn verify(&self, root: Hash, fs: &ProofTranscript, hidden_claim: bool) -> Result<(), WhirError> { + let mut vs = VerifierState::from_label(DOMAIN, fs); + verify( + &mut vs, + &self.config, + self.log_n, + self.n_lanes(), + root, + &self.point_claims, + &self.rings, + Some(self.hiding(hidden_claim)), + ) + } + + /// Where the revealed scalars start in the stream: after the first round's message and the lane rounds' but the last. + const fn revealed_at(&self) -> usize { + 2 * self.config.initial_k() + } + } + + #[test] + fn a_hiding_opening_verifies_and_binds_what_it_reveals() { + for (log_inv_rate, n_lanes, hidden_claim) in [(1usize, 5usize, false), (1, 64, true), (2, 37, true)] { + let st = HidingStatement::new(log_inv_rate, n_lanes, 0x41D + n_lanes as u64); + let pads = st.pads(7); + let (root, fs) = st.prove(&pads, None, hidden_claim); + let what = format!("rate 2^-{log_inv_rate}, {n_lanes} lanes, hidden claim {hidden_claim}"); + assert_eq!(st.verify(root, &fs, hidden_claim), Ok(()), "honest opening, {what}"); + + // The revealed claim, then each end of the padding's fold. + let k = st.config.padding(); + let g1 = st.revealed_at() + usize::from(hidden_claim); + if hidden_claim { + let mut bad = fs.clone(); + bad.stream[g1 - 1] += F192::ONE; + assert_eq!( + st.verify(root, &bad, hidden_claim), + Err(WhirError::RevealedClaim), + "tampered claim, {what}" + ); + } + for j in [g1, g1 + k - 1] { + let mut bad = fs.clone(); + bad.stream[j] += F192::ONE; + assert!(st.verify(root, &bad, hidden_claim).is_err(), "tampered g_1, {what}"); + } + + // A prover folding other pads than the committed ones sends a consistent transcript around a wrong `g_1`: the level-0 correction catches it. + let mut other = pads.clone(); + other[(n_lanes - 1) * k] += F64::ONE; + let (root, fs) = st.prove(&pads, Some(other), hidden_claim); + assert!(st.verify(root, &fs, hidden_claim).is_err(), "g_1 of other pads, {what}"); + + // The opening pads as its configuration does. + let mut vs = VerifierState::from_label(DOMAIN, &fs); + let short = Hiding { k: k - 1, hidden_claim }; + assert_eq!( + verify( + &mut vs, + &st.config, + st.log_n, + n_lanes, + root, + &st.point_claims, + &st.rings, + Some(short) + ), + Err(WhirError::Padding { k: k - 1, padding: k }) + ); + } + } + + #[test] + fn a_hiding_opening_is_a_function_of_its_pads() { + let st = HidingStatement::new(1, 6, 0x5EED); + let pads = st.pads(1); + let (root, fs) = st.prove(&pads, None, true); + assert_eq!(st.prove(&pads, None, true), (root, fs.clone()), "same pads, same proof"); + + let (other_root, other_fs) = st.prove(&st.pads(2), None, true); + assert_eq!(st.verify(other_root, &other_fs, true), Ok(())); + let g1 = st.revealed_at() + 1..st.revealed_at() + 1 + st.config.padding(); + assert!( + (fs.stream[g1.clone()].iter().zip(&other_fs.stream[g1])).all(|(a, b)| a != b), + "other pads, another g_1" + ); + } } diff --git a/crates/pcs/src/whir.rs b/crates/pcs/src/whir.rs index ae6e32537..2442fb12b 100644 --- a/crates/pcs/src/whir.rs +++ b/crates/pcs/src/whir.rs @@ -46,17 +46,27 @@ use primitives::multilinear::inner_product_base; pub use config::{ INITIAL_FOLDING_FACTOR, L0_LIST_BITS, LOG_INV_RATE_0, MAX_LOG_INV_RATE, MAX_LOG_N, MIN_LOG_INV_RATE, MIN_LOG_N, - ProverConfig, QUERY_GRINDING_BITS, RESIDUAL_MAX_LOG, RS_DOMAIN_INITIAL_REDUCTION_FACTOR, SECURITY_BITS, - SUBSEQUENT_FOLDING_FACTOR, VerifierConfig, config_for_rate, + MIN_LOG_N_HIDING, ProverConfig, QUERY_GRINDING_BITS, RESIDUAL_MAX_LOG, RS_DOMAIN_INITIAL_REDUCTION_FACTOR, + SECURITY_BITS, SUBSEQUENT_FOLDING_FACTOR, VerifierConfig, config_for_rate, config_for_rate_hiding, }; -pub use commit::{Commitment, ProverData, commit}; +pub use commit::{Commitment, ProverData, commit, commit_hiding}; pub use induce::eval_sk_at_vks; pub use prove::recursive_prover_with_basis; pub(crate) use prove::recursive_prover_with_prepared_basis; pub(crate) use sumcheck::{INITIAL_BASIS_CHUNK, initial_rounds_virtual}; -pub use verify::WhirError; -pub(crate) use verify::recursive_verifier_with_basis_succinct; +pub use verify::{WhirError, recursive_verifier_with_basis_succinct}; + +/// The opening of a commitment made by [`commit_hiding`]. +/// +/// After the lane fold's last challenge the prover sends the padding's fold `g_1`, `k` scalars, and level 0's queries take it off the folded codeword (the module docs of [`crate::stack_open`]). +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct Hiding { + /// Padding coefficients per committed lane: the configuration's [`ProverConfig::padding`]. + pub k: usize, + /// The scalars before the lane fold's end travelled under one-time keys: first turn hiding off and send the running claim in the clear, which the verifier checks against the one it holds and continues from. + pub hidden_claim: bool, +} /// Mixed inner product `Σ_i b[i] · witness[i]` (E x K via `mul_base`). The /// evaluation-claim `target` for a K-witness against an E-basis. diff --git a/crates/pcs/src/whir/commit.rs b/crates/pcs/src/whir/commit.rs index ce082d401..f7c849ace 100644 --- a/crates/pcs/src/whir/commit.rs +++ b/crates/pcs/src/whir/commit.rs @@ -7,7 +7,8 @@ //! level's extension-field encode, both Merkle-committed one leaf per row. use crate::merkle::{Hash, MerkleBuilder}; -use crate::ntt::AdditiveNttF64; +use crate::ntt::{AdditiveNttF64, Pad}; +use crate::whir::induce::padding_shift; use crate::whir::ntt_ext::encode_interleaved_ext; use primitives::field::{F64, F192}; @@ -22,6 +23,8 @@ pub struct Commitment { pub struct ProverData { pub codeword: Vec, pub merkle_tree: Vec, + /// The padding of a hiding commitment, lane block `u`'s `k` coefficients at `[u k, (u + 1) k)`; empty otherwise. + pub pads: Vec, } /// Commit to the `F64` message of a `2^log_n`-word witness: the message is its @@ -40,6 +43,26 @@ pub struct ProverData { /// rides the proof, so a verifier derives `n_lanes` from the announced layout to /// read a row and supplies the prefix itself. pub fn commit(message: &[F64], log_n: usize, log_batch_size: usize, log_inv_rate: usize) -> (Commitment, ProverData) { + commit_hiding(message, log_n, log_batch_size, log_inv_rate, &[]) +} + +/// [`commit`] with each lane padded past its power of two: the hiding commitment. +/// +/// With `m = log_n - log_batch_size`, `r = log_inv_rate` and `k = pads.len() / n_lanes`, lane block `u` encodes `P_u(X) + W_m(X + s) R_u(X)`: `P_u` its `2^m` words as novel-basis coefficients, `R_u` its padding `pads[u k..(u + 1) k]`, and `s = F64(2^(m + r))`. +/// Since `W_m(X + s) = W_m(X) + W_m(s)` and `X_{2^m + j} = W_m X_j`, that is `2^m + k` coefficients, so the codeword stays on the same `2^(m + r)` points, and the encode is the one butterfly layer more that pairs the message with the padding (`AdditiveNttF64::encode_interleaved_in_place_with`). +/// The shift by `s` keeps the factor nonzero on the whole domain, where `W_m` alone vanishes on its first `2^m` points: any `k` symbols of a lane are then uniform, whatever its message. +/// Empty `pads` is [`commit`]. +/// +/// # Panics +/// +/// Panics as [`commit`] does, or unless the padding is `k <= 2^m` coefficients for every lane. +pub fn commit_hiding( + message: &[F64], + log_n: usize, + log_batch_size: usize, + log_inv_rate: usize, + pads: &[F64], +) -> (Commitment, ProverData) { assert!(log_inv_rate >= 1, "log_inv_rate must be >= 1 for a non-trivial RS code"); assert!(log_n > log_batch_size, "witness must be wider than the interleaving"); let log_rows = log_n - log_batch_size; @@ -52,7 +75,17 @@ pub fn commit(message: &[F64], log_n: usize, log_batch_size: usize, log_inv_rate let k_code = log_rows + log_inv_rate; let n_positions = 1usize << k_code; let codeword_len = n_positions * n_lanes; - + let k = pads.len() / n_lanes; + assert_eq!(pads.len(), k * n_lanes, "every lane takes as many padding coefficients"); + assert!(k <= 1 << log_rows, "a lane's padding is at most its message's length"); + // Row `j` of the padding is coefficient `j` of every codeword lane's `R`, lane `t` being block `n_lanes - 1 - t`. + let pad_rows: Vec = (0..k * n_lanes) + .map(|w| pads[(n_lanes - 1 - w % n_lanes) * k + w / n_lanes]) + .collect(); + let pad = (k > 0).then(|| Pad { + rows: &pad_rows, + offset: padding_shift(log_rows, log_inv_rate), + }); let mut codeword = Box::new_uninit_slice(codeword_len); // Leaves are hashed as the encode finishes each block of rows. @@ -64,7 +97,7 @@ pub fn commit(message: &[F64], log_n: usize, log_batch_size: usize, log_inv_rate let codeword = unsafe { primitives::write_only(&mut codeword) }; crate::ntt::transpose_lane_major(&mut codeword[..message.len()], message, n_lanes, log_rows); let ntt = AdditiveNttF64::standard(k_code); - ntt.encode_interleaved_in_place_with(codeword, n_lanes, log_inv_rate, &|row, rows| { + ntt.encode_interleaved_in_place_with(codeword, n_lanes, log_inv_rate, pad, &|row, rows| { tree.absorb(row, rows); }); }); @@ -73,7 +106,15 @@ pub fn commit(message: &[F64], log_n: usize, log_batch_size: usize, log_inv_rate let merkle_tree = tracing::info_span!("Merkle").in_scope(|| tree.finish()); let root = *merkle_tree.last().expect("merkle tree non-empty"); - (Commitment { root }, ProverData { codeword, merkle_tree }) + let pads = pads.to_vec(); + ( + Commitment { root }, + ProverData { + codeword, + merkle_tree, + pads, + }, + ) } /// Codeword + Merkle tree for one deeper WHIR commitment level. diff --git a/crates/pcs/src/whir/config.rs b/crates/pcs/src/whir/config.rs index fcc019e01..8323c1238 100644 --- a/crates/pcs/src/whir/config.rs +++ b/crates/pcs/src/whir/config.rs @@ -31,7 +31,7 @@ pub const SECURITY_BITS: usize = 128; /// A challenge drawn between the root and the opening must hold against every list member. /// By a union bound its error grows by a factor `L_0`. /// -/// The value is `ceil(log2 L_0)` at its largest over every configured size and rate. +/// The value is `ceil(log2 L_0)` at its largest over every configured size and rate, hiding or not. /// A test pins it to the derivation. pub const L0_LIST_BITS: usize = 12; @@ -52,6 +52,9 @@ pub enum ConfigError { /// A witness size outside the tabulated range. #[error("log_n {log_n} is not in {MIN_LOG_N}..={MAX_LOG_N}")] SizeOutOfRange { log_n: usize }, + /// A witness size outside the tabulated range of the hiding opening. + #[error("log_n {log_n} is not in {MIN_LOG_N_HIDING}..={MAX_LOG_N} for a hiding opening")] + HidingSizeOutOfRange { log_n: usize }, } /// Why the level ladder has no shape for a witness size. No size [`config_for_rate`] accepts gets here; the test-only derivation and its fallback ladder, which take any size, can. @@ -129,12 +132,13 @@ pub struct ProverConfig { queries: Vec, grinding_bits: Vec, ood_samples: Vec, + padding: usize, } pub type VerifierConfig = ProverConfig; impl ProverConfig { - /// A config of `level_ks.len()` recursive levels after the lane fold. + /// A config of `level_ks.len()` recursive levels after the lane fold, its L0 lanes padded by `padding` coefficients. /// /// # Panics /// @@ -146,6 +150,7 @@ impl ProverConfig { queries: Vec, grinding_bits: Vec, ood_samples: Vec, + padding: usize, ) -> Self { let levels = level_ks.len() + 1; assert!(initial_k >= 1, "the lane fold binds at least one variable"); @@ -169,6 +174,7 @@ impl ProverConfig { queries, grinding_bits, ood_samples, + padding, } } @@ -210,6 +216,11 @@ impl ProverConfig { pub fn ood_samples(&self) -> &[usize] { &self.ood_samples } + + /// Coefficients a hiding commitment adds past each L0 lane's power of two, `k = q_0 + 2`, which the L0 query count was derived for; zero for a configuration that does not hide. + pub const fn padding(&self) -> usize { + self.padding + } } /// Level-ladder shape: the per-level inverse-rate logarithms and folds, index 0 being L0. @@ -368,18 +379,99 @@ pub fn config_for_rate(log_n: usize, log_inv_rate: usize) -> Result Result { + validate_log_inv_rate(log_inv_rate)?; + if !(MIN_LOG_N_HIDING..=MAX_LOG_N).contains(&log_n) { + return Err(ConfigError::HidingSizeOutOfRange { log_n }); + } + let queries = WHIR_QUERIES_HIDING[log_inv_rate - MIN_LOG_INV_RATE][log_n - MIN_LOG_N_HIDING]; + Ok(tabulated(log_n, log_inv_rate, queries, queries[0] + 2)) +} + +/// The production config with these query counts and this L0 padding. +fn tabulated(log_n: usize, log_inv_rate: usize, queries: &[usize], padding: usize) -> ProverConfig { let shape = derive_ladder_shape(log_n, INITIAL_FOLDING_FACTOR, log_inv_rate) .expect("the tabulated window always has a ladder"); let levels = shape.k_levels.len(); - let queries = WHIR_QUERIES[log_inv_rate - MIN_LOG_INV_RATE][log_n - MIN_LOG_N]; - Ok(ProverConfig::new( + ProverConfig::new( INITIAL_FOLDING_FACTOR, shape.k_levels[1..].to_vec(), shape.log_inv_rates, queries.to_vec(), vec![QUERY_GRINDING_BITS; levels], std::iter::once(0).chain(std::iter::repeat_n(1, levels - 1)).collect(), - )) + padding, + ) } #[cfg(test)] diff --git a/crates/pcs/src/whir/config/tests.rs b/crates/pcs/src/whir/config/tests.rs index abe0bef8c..9798a3309 100644 --- a/crates/pcs/src/whir/config/tests.rs +++ b/crates/pcs/src/whir/config/tests.rs @@ -33,9 +33,10 @@ )] use super::{ ConfigError, INITIAL_FOLDING_FACTOR, L0_LIST_BITS, LOG_INV_RATE_0, LadderError, MAX_LOG_INV_RATE, MAX_LOG_N, - MIN_LOG_INV_RATE, MIN_LOG_N, ProverConfig, QUERY_GRINDING_BITS, RS_DOMAIN_INITIAL_REDUCTION_FACTOR, - RS_DOMAIN_SUBSEQUENT_REDUCTION_FACTOR, SECURITY_BITS, WHIR_QUERIES, config_for_rate, derive_ladder, - derive_ladder_shape, validate_log_inv_rate, + MIN_LOG_INV_RATE, MIN_LOG_N, MIN_LOG_N_HIDING, ProverConfig, QUERY_GRINDING_BITS, + RS_DOMAIN_INITIAL_REDUCTION_FACTOR, RS_DOMAIN_SUBSEQUENT_REDUCTION_FACTOR, SECURITY_BITS, WHIR_QUERIES, + WHIR_QUERIES_HIDING, config_for_rate, config_for_rate_hiding, derive_ladder, derive_ladder_shape, + validate_log_inv_rate, }; use primitives::field::F64; use std::fmt::Write; @@ -188,12 +189,36 @@ pub(crate) fn default_config( queries, vec![0usize; n_levels], vec![0usize; n_levels], + 0, )) } /// The configuration the derivation gives a `2^log_n`-word witness at L0 rate `2^-log_inv_rate`, which the table must hold. fn derive_config(log_n: usize, log_inv_rate: usize) -> Result { - WhirSecurityConfig::derive_config_with_log_inv_rate(log_n + F64::DEGREE.ilog2() as usize, log_inv_rate)?.to_config() + WhirSecurityConfig::derive_config_with_log_inv_rate(log_n + F64::DEGREE.ilog2() as usize, log_inv_rate, 0)? + .to_config() +} + +/// The derivation of a hiding opening: L0's code padded by `k = q_0 + 2` past each lane's power of two, `q_0` its own query count. +/// +/// A larger code needs more queries, so `k` starts from the unpadded `q_0 + 2` and grows until the query count it gives keeps it. +fn derive_hiding_security(log_n: usize, log_inv_rate: usize) -> Result { + let m = log_n + F64::DEGREE.ilog2() as usize; + let mut padding = WhirSecurityConfig::derive_config_with_log_inv_rate(m, log_inv_rate, 0)?.levels[0].queries + 2; + loop { + let cfg = WhirSecurityConfig::derive_config_with_log_inv_rate(m, log_inv_rate, padding)?; + let next = cfg.levels[0].queries + 2; + if next == padding { + return Ok(cfg); + } + assert!(next > padding, "the padded query count grows with the padding"); + padding = next; + } +} + +/// The configuration the hiding table must hold. +fn derive_hiding_config(log_n: usize, log_inv_rate: usize) -> Result { + derive_hiding_security(log_n, log_inv_rate)?.to_config() } /// Shared config for a `2^log_n`-word witness, preferring the production profile at [`LOG_INV_RATE_0`] and falling back to [`default_config`] below its feasibility floor. @@ -241,6 +266,8 @@ struct WhirLevelConfig { /// Message dimension at this level (log of the number of field columns in /// the codeword). `log_msg_cols + log_inv_rate = log_2(block_len)`. log_msg_cols: usize, + /// Coefficients a hiding commitment adds past each lane's `2^log_msg_cols`: nonzero only at L0 of a hiding opening. + padding: usize, /// Log of lane width per Merkle leaf at this level. For L0 = `initial_k`; /// for L_i (i ≥ 1) = the previous level's `k`. log_num_interleaved: usize, @@ -309,13 +336,36 @@ struct WhirSecurityConfig { /// Extension-field size used for soundness analysis: `q = 2^192`. const ANALYSIS_LOG_Q: f64 = 192.0; +/// A level's Reed-Solomon code: block length `2^(log_msg_cols + log_inv_rate)`, dimension `2^log_msg_cols + padding`. +#[derive(Clone, Copy, Debug)] +struct Code { + log_inv_rate: usize, + log_msg_cols: usize, + padding: usize, +} + +impl Code { + const fn plain(log_inv_rate: usize, log_msg_cols: usize) -> Self { + Self { + log_inv_rate, + log_msg_cols, + padding: 0, + } + } + + /// Base-two logarithm of the block length. + const fn log_block_len(self) -> usize { + self.log_msg_cols + self.log_inv_rate + } +} + /// BCHKS25 parameter `rho = k/n` for an RS code of dimension `k + 1`. -/// Our message has `2^log_msg_cols` coefficients (degree strictly below that -/// value), so `k = 2^log_msg_cols - 1`. This differs perceptibly from the +/// Our message has `2^log_msg_cols + padding` coefficients (degree strictly below that +/// value), so `k = 2^log_msg_cols + padding - 1`. This differs perceptibly from the /// nominal code rate at the small recursive levels. -fn reduced_rate(log_inv_rate: usize, log_msg_cols: usize) -> f64 { - let dimension = (log_msg_cols as f64).exp2(); - (dimension - 1.0) / ((log_msg_cols + log_inv_rate) as f64).exp2() +fn reduced_rate(code: Code) -> f64 { + let dimension = (code.log_msg_cols as f64).exp2() + code.padding as f64; + (dimension - 1.0) / (code.log_block_len() as f64).exp2() } /// Proximity-gap exceptional set for the list-decoding (Johnson) regime, per @@ -335,17 +385,17 @@ fn reduced_rate(log_inv_rate: usize, log_msg_cols: usize) -> f64 { clippy::suboptimal_flops, reason = "Keep the rounding of the protocol parameter formulas unchanged." )] -fn paper_thm_ca_johnson_log_a(log_inv_rate: usize, eta: f64, log_msg_cols: usize) -> f64 { - let rho = reduced_rate(log_inv_rate, log_msg_cols); +fn paper_thm_ca_johnson_log_a(code: Code, eta: f64) -> f64 { + let rho = reduced_rate(code); let sqrt_rho = rho.sqrt(); let gamma = 1.0 - sqrt_rho - eta; // BCHKS25 Thm 4.6: m = ⌈√ρ/(1−√ρ−γ)⌉ = ⌈√ρ/η⌉, floored at 3. - let m_param = johnson_m_param(log_inv_rate, log_msg_cols, eta); + let m_param = johnson_m_param(code, eta); let half = m_param + 0.5; let half5 = half.powi(5); let numerator = 2.0 * half5 + 3.0 * half * gamma * rho; let denominator = 3.0 * rho.powf(1.5); - let n = ((log_msg_cols + log_inv_rate) as f64).exp2(); + let n = (code.log_block_len() as f64).exp2(); let a = (numerator / denominator) * n + half / sqrt_rho; a.log2() } @@ -356,15 +406,15 @@ fn paper_thm_ca_johnson_log_a(log_inv_rate: usize, eta: f64, log_msg_cols: usize /// Flock's Thm 8 quotes Thm 4.6 with that non-list parameter; the list form /// costs a factor 2 of slack (see the footnote in the PCS annex /// Thm `thm:mca-johnson`). -fn johnson_m_param(log_inv_rate: usize, log_msg_cols: usize, eta: f64) -> f64 { - let sqrt_rho = reduced_rate(log_inv_rate, log_msg_cols).sqrt(); +fn johnson_m_param(code: Code, eta: f64) -> f64 { + let sqrt_rho = reduced_rate(code).sqrt(); ((sqrt_rho / eta).ceil() as usize).max(3) as f64 } /// Per-query log₂(1/(1−γ)) under the Johnson regime: each query closes /// `log_2(1/(1-γ))` bits of soundness against a γ-far adversary. -fn paper_per_query_bits(log_inv_rate: usize, log_msg_cols: usize, eta: f64) -> f64 { - let rho = reduced_rate(log_inv_rate, log_msg_cols); +fn paper_per_query_bits(code: Code, eta: f64) -> f64 { + let rho = reduced_rate(code); let gamma = 1.0 - rho.sqrt() - eta; (1.0 / (1.0 - gamma)).log2() } @@ -397,9 +447,9 @@ fn udr_per_query_bits_asymptotic(log_inv_rate: usize) -> f64 { /// `θ = 1 − √ρ − η`, strictly below the Johnson radius by slack `η > 0`, so /// that regime never applies and the plain Johnson bound is both correct and /// far tighter (it dominates GGR throughout the regime RS can reach). -fn johnson_interleaved_list_log2(log_inv_rate: usize, log_msg_cols: usize, eta: f64) -> f64 { +fn johnson_interleaved_list_log2(code: Code, eta: f64) -> f64 { debug_assert!(eta > 0.0, "η must be > 0 to stay strictly below the Johnson radius"); - let rho = reduced_rate(log_inv_rate, log_msg_cols); + let rho = reduced_rate(code); let sqrt_rho = rho.sqrt(); let l_base = 1.0 / (2.0 * eta * sqrt_rho); l_base.log2() @@ -415,15 +465,8 @@ fn johnson_interleaved_list_log2(log_inv_rate: usize, log_msg_cols: usize, eta: /// 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; /// the ring switch is no term here, since this level's oracle and list come after its challenges; /// - 2 for quadratic sumcheck. -fn johnson_algebraic_bits_for( - level: usize, - log_inv_rate: usize, - log_msg_cols: usize, - eta: f64, - prev_queries: usize, - ood_samples: usize, -) -> f64 { - let log2_l = johnson_interleaved_list_log2(log_inv_rate, log_msg_cols, eta); +fn johnson_algebraic_bits_for(level: usize, code: Code, eta: f64, prev_queries: usize, ood_samples: usize) -> f64 { + let log2_l = johnson_interleaved_list_log2(code, eta); let batch_degree = if level == 0 { crate::ring_switch::tests::RING_SWITCH_SOUNDNESS_DEGREE } else { @@ -435,14 +478,7 @@ fn johnson_algebraic_bits_for( /// `prev_queries` is `levels[i-1].queries`, and 0 for `i = 0`. fn johnson_algebraic_bits(level: usize, config: &WhirLevelConfig, prev_queries: usize) -> f64 { - johnson_algebraic_bits_for( - level, - config.log_inv_rate, - config.log_msg_cols, - config.eta, - prev_queries, - config.ood_samples, - ) + johnson_algebraic_bits_for(level, config.code(), config.eta, prev_queries, config.ood_samples) } /// The query count the batch at `levels[i]` carries claims from. @@ -467,8 +503,8 @@ const fn prev_queries_at(levels: &[WhirLevelConfig], i: usize) -> usize { clippy::suboptimal_flops, reason = "Keep the rounding of the protocol parameter formulas unchanged." )] -fn paper_ood_bits(log_inv_rate: usize, log_msg_cols: usize, eta: f64, mu_vars: usize, ood_samples: usize) -> f64 { - let log2_l = johnson_interleaved_list_log2(log_inv_rate, log_msg_cols, eta); +fn paper_ood_bits(code: Code, eta: f64, mu_vars: usize, ood_samples: usize) -> f64 { + let log2_l = johnson_interleaved_list_log2(code, eta); let log2_mu = (mu_vars as f64).log2(); if ood_samples == 0 { ANALYSIS_LOG_Q - log2_l - log2_mu @@ -495,14 +531,14 @@ struct OptimizedJohnsonLevel { clippy::while_float, reason = "Advance by one ULP until the rounded theorem parameter satisfies the integer bound." )] -fn johnson_eta_for_m(log_inv_rate: usize, log_msg_cols: usize, m: usize) -> f64 { +fn johnson_eta_for_m(code: Code, m: usize) -> f64 { debug_assert!(m >= 3); - let sqrt_rho = reduced_rate(log_inv_rate, log_msg_cols).sqrt(); + let sqrt_rho = reduced_rate(code).sqrt(); let mut eta = sqrt_rho / m as f64; - while johnson_m_param(log_inv_rate, log_msg_cols, eta) > m as f64 { + while johnson_m_param(code, eta) > m as f64 { eta = f64::from_bits(eta.to_bits() + 1); } - debug_assert_eq!(johnson_m_param(log_inv_rate, log_msg_cols, eta), m as f64); + debug_assert_eq!(johnson_m_param(code, eta), m as f64); eta } @@ -512,8 +548,7 @@ fn johnson_eta_for_m(log_inv_rate: usize, log_msg_cols: usize, m: usize) -> f64 /// 128-bit term and the proximity-gap target without fold grinding. fn optimize_johnson_level( level: usize, - log_inv_rate: usize, - log_msg_cols: usize, + code: Code, log_num_interleaved: usize, target_bits: usize, query_grinding_bits: usize, @@ -521,25 +556,26 @@ fn optimize_johnson_level( ) -> Result { let target = target_bits as f64; let query_target = target_bits.saturating_sub(query_grinding_bits).max(1) as f64; - let mu = log_msg_cols + log_num_interleaved; - let block_len = 1usize << (log_msg_cols + log_inv_rate); + let mu = code.log_msg_cols + log_num_interleaved; + let block_len = 1usize << code.log_block_len(); + let log_inv_rate = code.log_inv_rate; let mut best: Option = None; for m in 3..=JOHNSON_ETA_SEARCH_MAX_M { - let eta = johnson_eta_for_m(log_inv_rate, log_msg_cols, m); - let max_eta = 1.0 - reduced_rate(log_inv_rate, log_msg_cols).sqrt(); + let eta = johnson_eta_for_m(code, m); + let max_eta = 1.0 - reduced_rate(code).sqrt(); if eta >= max_eta { continue; } - let eps_pg = ANALYSIS_LOG_Q - paper_thm_ca_johnson_log_a(log_inv_rate, eta, log_msg_cols); + let eps_pg = ANALYSIS_LOG_Q - paper_thm_ca_johnson_log_a(code, eta); // At the theorem-parameter boundaries a grows monotonically with m; // no later candidate can recover once the proximity-gap target fails. if eps_pg + 1e-12 < target { break; } - let per_q = paper_per_query_bits(log_inv_rate, log_msg_cols, eta); + let per_q = paper_per_query_bits(code, eta); if !per_q.is_finite() || per_q <= 0.0 { continue; } @@ -551,15 +587,14 @@ fn optimize_johnson_level( let ood_samples = if level == 0 { 0 } else { - match (1..=8usize).find(|&s| paper_ood_bits(log_inv_rate, log_msg_cols, eta, mu, s) + 1e-12 >= target) { + match (1..=8usize).find(|&s| paper_ood_bits(code, eta, mu, s) + 1e-12 >= target) { Some(samples) => samples, None => continue, } }; - let eps_ood = paper_ood_bits(log_inv_rate, log_msg_cols, eta, mu, ood_samples); + let eps_ood = paper_ood_bits(code, eta, mu, ood_samples); if eps_ood + 1e-12 < target - || johnson_algebraic_bits_for(level, log_inv_rate, log_msg_cols, eta, prev_queries, ood_samples) + 1e-12 - < target + || johnson_algebraic_bits_for(level, code, eta, prev_queries, ood_samples) + 1e-12 < target { continue; } @@ -578,17 +613,26 @@ fn optimize_johnson_level( } impl WhirLevelConfig { + /// The level's code. + const fn code(&self) -> Code { + Code { + log_inv_rate: self.log_inv_rate, + log_msg_cols: self.log_msg_cols, + padding: self.padding, + } + } + /// Proximity-gap and per-query soundness bits this level delivers: /// eps_pg_bits = log₂(q/a) under the Johnson threshold-a formula /// eps_query_bits = Q · log₂(1/(1−γ)) fn paper_predicted_bits(&self) -> (f64, f64) { // Why: fold row of `thm:rbr`, MCA part, the same at every round whatever the interleaving (`lem:fold-list`). - let log_a = paper_thm_ca_johnson_log_a(self.log_inv_rate, self.eta, self.log_msg_cols); + let log_a = paper_thm_ca_johnson_log_a(self.code(), self.eta); let eps_pg = ANALYSIS_LOG_Q - log_a; // Per-query soundness WITHOUT a list union bound: the OOD binding (see // `paper_ood_bits`) pins the prover to a single codeword of the // interleaved list before queries are drawn. - let per_q = paper_per_query_bits(self.log_inv_rate, self.log_msg_cols, self.eta); + let per_q = paper_per_query_bits(self.code(), self.eta); let eps_query = self.queries as f64 * per_q; (eps_pg, eps_query) } @@ -596,7 +640,7 @@ impl WhirLevelConfig { /// OOD binding bits this level delivers. See `paper_ood_bits`. fn paper_predicted_ood_bits(&self) -> f64 { let mu = self.log_msg_cols + self.log_num_interleaved; - paper_ood_bits(self.log_inv_rate, self.log_msg_cols, self.eta, mu, self.ood_samples) + paper_ood_bits(self.code(), self.eta, mu, self.ood_samples) } } @@ -679,7 +723,7 @@ impl WhirSecurityConfig { } // eta within the Johnson range for this level's (reduced) rate. - let max_eta = 1.0 - reduced_rate(lv.log_inv_rate, lv.log_msg_cols).sqrt(); + let max_eta = 1.0 - reduced_rate(lv.code()).sqrt(); if !lv.eta.is_finite() || lv.eta <= 0.0 || lv.eta >= max_eta { return Err(DerivationError::EtaOutOfRange { level, @@ -775,7 +819,9 @@ impl WhirSecurityConfig { /// soundness**, i.e. every verifier-challenge error term (pg + fold /// grinding, query + query grinding, OOD, and algebraic checks) clears the /// target individually. - fn derive_config_with_log_inv_rate(m: usize, log_inv_rate: usize) -> Result { + /// + /// L0's code is padded by `padding` coefficients past each lane's power of two, a hiding commitment's; every deeper level commits an unpadded fold. + fn derive_config_with_log_inv_rate(m: usize, log_inv_rate: usize, padding: usize) -> Result { validate_log_inv_rate(log_inv_rate)?; let target_bits = SECURITY_BITS; let query_grind: usize = QUERY_GRINDING_BITS; @@ -803,11 +849,16 @@ impl WhirSecurityConfig { let ilv = shape.k_levels[i]; cols -= ilv; let prev_queries = prev_queries_at(&levels, i); - let optimized = optimize_johnson_level(i, rate, cols, ilv, target_bits, query_grind, prev_queries)?; + let code = Code { + padding: if i == 0 { padding } else { 0 }, + ..Code::plain(rate, cols) + }; + let optimized = optimize_johnson_level(i, code, ilv, target_bits, query_grind, prev_queries)?; levels.push(WhirLevelConfig { log_inv_rate: rate, log_msg_cols: cols, + padding: code.padding, log_num_interleaved: ilv, k: shape.k_levels[i], eta: optimized.eta, @@ -840,6 +891,7 @@ impl WhirSecurityConfig { self.levels.iter().map(|lv| lv.queries).collect(), self.levels.iter().map(|lv| lv.grinding_bits).collect(), self.levels.iter().map(|lv| lv.ood_samples).collect(), + self.levels[0].padding, )) } } @@ -850,11 +902,11 @@ fn johnson_bound_uses_theorem_parameter_and_reduced_rate() { // m = ceil(sqrt(rho) / eta). The factor-two-smaller ceil(sqrt(rho) / (2 eta)) // belongs to the plain, non-list Thm 1.5; Flock's Thm 8 quotes Thm 4.6 // with that non-list parameter, which would overstate eps_pg by ~5 bits. - assert_eq!(johnson_m_param(1, 16, 0.02), 36.0); + assert_eq!(johnson_m_param(Code::plain(1, 16), 0.02), 36.0); // A message of dimension 16 has maximum degree 15, so the theorem's // reduced rate at block length 512 is 15/512, not the nominal 1/32. - assert_eq!(reduced_rate(5, 4), 15.0 / 512.0); + assert_eq!(reduced_rate(Code::plain(5, 4)), 15.0 / 512.0); } #[test] @@ -862,7 +914,7 @@ fn production_profile_is_128_bit_johnson_with_query_grinding() { let mut min_pg_bits = f64::INFINITY; for log_inv_rate in MIN_LOG_INV_RATE..=MAX_LOG_INV_RATE { for m in 22 + F64::DEGREE.ilog2() as usize..=28 + F64::DEGREE.ilog2() as usize { - let cfg = WhirSecurityConfig::derive_config_with_log_inv_rate(m, log_inv_rate).unwrap(); + let cfg = WhirSecurityConfig::derive_config_with_log_inv_rate(m, log_inv_rate, 0).unwrap(); assert_eq!(cfg.target_security_bits, 128); assert_eq!(cfg.levels[0].log_inv_rate, log_inv_rate); assert_eq!(cfg.levels[0].ood_samples, 0); @@ -890,15 +942,27 @@ fn production_profile_is_128_bit_johnson_with_query_grinding() { #[test] fn l0_list_bits_bound_every_l0_list() { - // Every configured size and rate: its L0 list, which every challenge before the opening is unioned over. - let largest = (MIN_LOG_INV_RATE..=MAX_LOG_INV_RATE) - .flat_map(|log_inv_rate| (MIN_LOG_N..=MAX_LOG_N).map(move |log_n| (log_inv_rate, log_n))) - .map(|(log_inv_rate, log_n)| { - let cfg = - WhirSecurityConfig::derive_config_with_log_inv_rate(log_n + F64::DEGREE.ilog2() as usize, log_inv_rate) - .unwrap_or_else(|e| panic!("rate 2^-{log_inv_rate}, log_n {log_n}: {e}")); + // Every configured size and rate, hiding or not: its L0 list, which every challenge before the opening is unioned over. + // The padded code has the larger rate, and the list bound its own slack. + let plain = (MIN_LOG_INV_RATE..=MAX_LOG_INV_RATE) + .flat_map(|log_inv_rate| (MIN_LOG_N..=MAX_LOG_N).map(move |log_n| (log_inv_rate, log_n, false))); + let hiding = (MIN_LOG_INV_RATE..=MAX_LOG_INV_RATE) + .flat_map(|log_inv_rate| (MIN_LOG_N_HIDING..=MAX_LOG_N).map(move |log_n| (log_inv_rate, log_n, true))); + let largest = plain + .chain(hiding) + .map(|(log_inv_rate, log_n, hides)| { + let cfg = if hides { + derive_hiding_security(log_n, log_inv_rate) + } else { + WhirSecurityConfig::derive_config_with_log_inv_rate( + log_n + F64::DEGREE.ilog2() as usize, + log_inv_rate, + 0, + ) + }; + let cfg = cfg.unwrap_or_else(|e| panic!("rate 2^-{log_inv_rate}, log_n {log_n}, hiding {hides}: {e}")); let l0 = &cfg.levels[0]; - johnson_interleaved_list_log2(l0.log_inv_rate, l0.log_msg_cols, l0.eta) + johnson_interleaved_list_log2(l0.code(), l0.eta) }) .fold(f64::NEG_INFINITY, f64::max); @@ -911,12 +975,12 @@ fn l0_list_bits_bound_every_l0_list() { ); } -/// `WHIR_QUERIES`'s rows as `config.rs` writes them, with `queries(log_inv_rate, log_n)` in each entry. -fn table_rows(queries: impl Fn(usize, usize) -> Vec) -> String { +/// A query table's rows as `config.rs` writes them, from size `2^min_log_n`, with `queries(log_inv_rate, log_n)` in each entry. +fn table_rows(min_log_n: usize, queries: impl Fn(usize, usize) -> Vec) -> String { let mut rows = String::new(); for log_inv_rate in MIN_LOG_INV_RATE..=MAX_LOG_INV_RATE { writeln!(rows, " // Rate 2^-{log_inv_rate}.\n [").unwrap(); - for log_n in MIN_LOG_N..=MAX_LOG_N { + for log_n in min_log_n..=MAX_LOG_N { let row: Vec = queries(log_inv_rate, log_n).iter().map(usize::to_string).collect(); writeln!(rows, " &[{}],", row.join(", ")).unwrap(); } @@ -932,9 +996,12 @@ fn the_table_is_the_derivation() { let derived = |log_inv_rate: usize, log_n: usize| { derive_config(log_n, log_inv_rate).unwrap_or_else(|e| panic!("rate 2^-{log_inv_rate}, log_n {log_n}: {e}")) }; - let rows = table_rows(|log_inv_rate, log_n| derived(log_inv_rate, log_n).queries().to_vec()); - let tabulated = - table_rows(|log_inv_rate, log_n| WHIR_QUERIES[log_inv_rate - MIN_LOG_INV_RATE][log_n - MIN_LOG_N].to_vec()); + let rows = table_rows(MIN_LOG_N, |log_inv_rate, log_n| { + derived(log_inv_rate, log_n).queries().to_vec() + }); + let tabulated = table_rows(MIN_LOG_N, |log_inv_rate, log_n| { + WHIR_QUERIES[log_inv_rate - MIN_LOG_INV_RATE][log_n - MIN_LOG_N].to_vec() + }); assert!( tabulated == rows, "WHIR_QUERIES is stale, replace its rows in crates/pcs/src/whir/config.rs with:\n{rows}" @@ -956,3 +1023,91 @@ fn the_table_is_the_derivation() { } } } + +/// The hiding table is the derivation with L0's code padded at its fixed point `k = q_0 + 2`, and the configuration pads by that `k`. +/// A stale table fails with the rows to paste over it. +#[test] +fn the_hiding_table_is_the_derivation() { + let derived = |log_inv_rate: usize, log_n: usize| { + derive_hiding_config(log_n, log_inv_rate) + .unwrap_or_else(|e| panic!("hiding, rate 2^-{log_inv_rate}, log_n {log_n}: {e}")) + }; + let configs: Vec> = (MIN_LOG_INV_RATE..=MAX_LOG_INV_RATE) + .map(|log_inv_rate| { + (MIN_LOG_N_HIDING..=MAX_LOG_N) + .map(|log_n| derived(log_inv_rate, log_n)) + .collect() + }) + .collect(); + let at = |log_inv_rate: usize, log_n: usize| &configs[log_inv_rate - MIN_LOG_INV_RATE][log_n - MIN_LOG_N_HIDING]; + let rows = table_rows(MIN_LOG_N_HIDING, |log_inv_rate, log_n| { + at(log_inv_rate, log_n).queries().to_vec() + }); + let tabulated = table_rows(MIN_LOG_N_HIDING, |log_inv_rate, log_n| { + WHIR_QUERIES_HIDING[log_inv_rate - MIN_LOG_INV_RATE][log_n - MIN_LOG_N_HIDING].to_vec() + }); + assert!( + tabulated == rows, + "WHIR_QUERIES_HIDING is stale, replace its rows in crates/pcs/src/whir/config.rs with:\n{rows}" + ); + for log_inv_rate in MIN_LOG_INV_RATE - 1..=MAX_LOG_INV_RATE + 1 { + for log_n in 0..=MAX_LOG_N + 8 { + let tabulated = config_for_rate_hiding(log_n, log_inv_rate); + if !(MIN_LOG_INV_RATE..=MAX_LOG_INV_RATE).contains(&log_inv_rate) { + assert_eq!(tabulated, Err(ConfigError::RateOutOfRange { log_inv_rate })); + } else if !(MIN_LOG_N_HIDING..=MAX_LOG_N).contains(&log_n) { + assert_eq!(tabulated, Err(ConfigError::HidingSizeOutOfRange { log_n })); + } else { + let derived = at(log_inv_rate, log_n); + assert_eq!( + derived.padding(), + derived.queries()[0] + 2, + "the padding is at its fixed point" + ); + assert_eq!( + tabulated.as_ref(), + Ok(derived), + "hiding, rate 2^-{log_inv_rate}, log_n {log_n}" + ); + } + } + } +} + +/// `K` dimensions a hiding opening reveals after the lane fold, three per `E` scalar: the running claim `a`, the round messages, the out-of-domain answers, level 0's folded query values, every later level's opened rows, and the residual. +fn revealed_dimensions(log_n: usize, config: &ProverConfig) -> usize { + let (queries, ks) = (config.queries(), config.level_ks()); + let residual = log_n - config.initial_k() - ks.iter().sum::(); + // `a`, then the message of the round after the lane fold. + let mut scalars = 1 + 2; + // Each committed level's out-of-domain answers, each with its intro message. + scalars += 3 * config.ood_samples()[1..].iter().sum::(); + // Level 0's folded query values and their intro message. + scalars += queries[0] + 2; + // Each later level: its fold rounds, its opened rows (a fold's worth of elements each) and their intro message. + for (i, &k) in ks.iter().enumerate() { + scalars += 2 * k + (queries[i + 1] << k) + 2; + } + // The residual, and the closing rounds but the last, which the residual answers. + scalars += (1 << residual) + 2 * residual.saturating_sub(1); + 3 * scalars +} + +/// One random lane of `2^m` uniform words masks every functional the opening reveals after the lane fold only while they span at most half its dimensions (VEIL's Lemma 4.7, adapted), which is what bounds the hiding opening below at `2^MIN_LOG_N_HIDING` words. +#[test] +fn a_hiding_opening_reveals_at_most_half_a_lane() { + for log_inv_rate in MIN_LOG_INV_RATE..=MAX_LOG_INV_RATE { + for log_n in MIN_LOG_N_HIDING..=MAX_LOG_N { + let config = config_for_rate_hiding(log_n, log_inv_rate).unwrap(); + let lane = 1usize << (log_n - config.initial_k()); + let revealed = revealed_dimensions(log_n, &config); + assert!( + 2 * revealed <= lane, + "rate 2^-{log_inv_rate}, log_n {log_n}: {revealed} dimensions revealed, lane of {lane}" + ); + } + } + // Below the hiding floor the same opening would reveal more than half a lane. + let config = config_for_rate(MIN_LOG_N_HIDING - 1, MIN_LOG_INV_RATE).unwrap(); + assert!(2 * revealed_dimensions(MIN_LOG_N_HIDING - 1, &config) > 1 << (MIN_LOG_N_HIDING - 1 - config.initial_k())); +} diff --git a/crates/pcs/src/whir/induce.rs b/crates/pcs/src/whir/induce.rs index 6bb42e902..2ac5235d7 100644 --- a/crates/pcs/src/whir/induce.rs +++ b/crates/pcs/src/whir/induce.rs @@ -91,6 +91,47 @@ fn invert_sks(sks_vks: &[F64]) -> Vec { .collect() } +/// `W_m(s)` for `s = F64(2^(m + r))`, the first basis element past a `2^(m + r)`-point domain. +/// +/// A hiding commitment's padding is `W_m(X + s) = W_m(X) + W_m(s)` times its polynomial: `W_m` vanishes on the domain's first `2^m` points and maps it onto the span of `W_m(F64(2^b))`, `m <= b < m + r`, which `W_m(s)` lies outside, so the factor vanishes nowhere on the domain. +pub(crate) fn padding_shift(log_msg_cols: usize, log_inv_rate: usize) -> F64 { + let sks_vks = eval_sk_at_vks(log_msg_cols); + let s = (0..log_msg_cols).fold(F64(1 << (log_msg_cols + log_inv_rate)), |s, b| next_s(s, sks_vks[b])); + s * sks_vks[log_msg_cols].inv() +} + +/// `Σ_i w_i W_m(q_i + s) Σ_{j F192 { + let sks_vks = eval_sk_at_vks(log_msg_cols); + let inv_sks_vks = invert_sks(&sks_vks); + let shift = padding_shift(log_msg_cols, log_inv_rate); + let mut w = vec![F64::ZERO; log_msg_cols + 1]; + let mut g = Vec::with_capacity(g1.len()); + (queries.iter().zip(weights)).fold(F192::ZERO, |acc, (&q, &weight)| { + normalized_sks_at(F64(q as u64), &sks_vks, &inv_sks_vks, &mut w); + // `Σ_j g_1[j] X_j`, folding the top bit of `j` at a time: `X_j` is the product of the `W_b` over the bits `b` of `j`. + g.clear(); + g.extend_from_slice(g1); + while g.len() > 1 { + let half = g.len().next_power_of_two() >> 1; + let w_b = w[half.trailing_zeros() as usize]; + let (lo, hi) = g.split_at_mut(half); + for (l, &h) in lo.iter_mut().zip(hi.iter()) { + *l += h.mul_base(w_b); + } + g.truncate(half); + } + let p = g.first().copied().unwrap_or(F192::ZERO); + acc + weight * p.mul_base(w[log_msg_cols] + shift) + }) +} + /// Dense induce: `basis_poly[j] = Σ_i w_i · W-hat_j(q_i)`, /// `enforced_sum = Σ_i w_i · `, for the per-query /// batching weights `w` of the level. diff --git a/crates/pcs/src/whir/prove.rs b/crates/pcs/src/whir/prove.rs index c5de28c94..a1b992cbe 100644 --- a/crates/pcs/src/whir/prove.rs +++ b/crates/pcs/src/whir/prove.rs @@ -6,15 +6,15 @@ //! The recursive prover: the lane fold, then one commit, query phase and induce //! per level, down to the residual sent in the clear. -use super::commit::ligero_commit_ext; +use super::Hiding; +use super::commit::{ProverData, ligero_commit_ext}; use super::sample_queries_ordered; use super::sumcheck::{Basis, InitialRounds, SumcheckProver, send_msg}; -use crate::merkle::Hash; use crate::ntt::AdditiveNttF64; use crate::whir::config::ProverConfig; use crate::whir::induce::{ eval_sk_at_vks, induce_sumcheck_enforced_sum, induce_sumcheck_evaluate_at_residual, induce_sumcheck_poly, - induce_sumcheck_poly_auto_base, + induce_sumcheck_poly_auto_base, padding_correction, }; use fiat_shamir::merkle::PrunedMerklePaths; use fiat_shamir::transcript::Transmitter; @@ -42,7 +42,7 @@ fn ext_row_words(row: &[F192]) -> Vec { } /// Prove `Σ_x witness(x) · b_initial(x) = target` against the L0 commitment -/// produced by [`commit`](super::commit()) (with `log_batch_size = config.initial_k()` and +/// `l0` produced by [`commit`](super::commit()) or [`commit_hiding`](super::commit_hiding()) (with `log_batch_size = config.initial_k()` and /// `log_inv_rate = config.log_inv_rates()[0]`). /// /// `witness` is borrowed: it is only READ (round-0 message + the first lane @@ -59,7 +59,13 @@ fn ext_row_words(row: &[F192]) -> Vec { /// by `stack.len()`; `ood_samples[0] == 0` is what keeps a full-tensor OOD weight /// out of these rounds. /// +/// With `hiding`, `l0` is a hiding commitment whose padding is `hiding.k` coefficients a lane, and the opening reveals the padding's lane fold after the lane fold (the module docs of [`crate::stack_open`]). +/// /// Scalars enter the shared transcript as they are transmitted, and authenticated Merkle openings travel as one phase per level. The caller has already bound the initial commitment and target. +/// +/// # Panics +/// +/// Panics on a shape the commitment does not have, or with `hiding` on a padding of another length than `hiding.k` a lane or than the configuration's. #[expect( clippy::too_many_arguments, reason = "The proof kernel keeps its independent inputs explicit." @@ -70,8 +76,8 @@ pub fn recursive_prover_with_basis( witness: &[F64], b_initial: Vec, target: F192, - l0_codeword: &[F64], - l0_tree: &[Hash], + l0: &ProverData, + hiding: Option, ps: &mut impl Transmitter, ) { recursive_prover_with_prepared_basis( @@ -80,9 +86,9 @@ pub fn recursive_prover_with_basis( witness, Basis::Dense(b_initial), target, - l0_codeword, - l0_tree, + l0, None, + hiding, ps, ); } @@ -97,11 +103,12 @@ pub(crate) fn recursive_prover_with_prepared_basis( witness: &[F64], b_initial: Basis<'_>, target: F192, - l0_codeword: &[F64], - l0_tree: &[Hash], + l0: &ProverData, initial: Option, + hiding: Option, ps: &mut impl Transmitter, ) { + let (l0_codeword, l0_tree) = (&l0.codeword[..], &l0.merkle_tree[..]); let r = config.level_steps(); let initial_k = config.initial_k(); @@ -123,6 +130,16 @@ pub(crate) fn recursive_prover_with_prepared_basis( } assert_eq!(l0_codeword.len(), block_len_0 * n_lanes); assert_eq!(l0_tree.len(), 2 * block_len_0 - 1); + let pad_k = hiding.map_or(0, |h| h.k); + assert_eq!( + l0.pads.len(), + pad_k * n_lanes, + "the commitment's padding is the opening's" + ); + assert!( + hiding.is_none_or(|h| h.k == config.padding()), + "a hiding opening pads as its configuration" + ); // Nothing is absorbed on entry. The commitment was bound by the `add_root`/`next_root` that // transmitted it, and the target is `sum_i lambda^i * claim_i` over claim values bound by their @@ -156,11 +173,27 @@ pub(crate) fn recursive_prover_with_prepared_basis( send_msg(ps, start_msg, target); let mut r_lane_fold = Vec::with_capacity(initial_k); + let mut g1 = Vec::new(); for j in 0..initial_k { 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()); r_lane_fold.push(r_j); + if j + 1 == initial_k + && let Some(h) = hiding + { + // The running claim in the clear, which every later message is public after. + if h.hidden_claim { + ps.set_hidden(false); + ps.add_scalar(sc_prover.claim()); + } + // The padding's lane fold `g_1[j] = Σ_u eq(fold, u) pad_u[j]`, with level 0's lane eq table. + let eq = eq_table(&r_lane_fold); + g1 = (0..h.k) + .map(|j| (0..n_lanes).fold(F192::ZERO, |acc, u| acc + eq[u].mul_base(l0.pads[u * h.k + j]))) + .collect(); + ps.add_scalars(&g1); + } + send_msg(ps, msg, sc_prover.claim()); } drop(sumcheck_span); @@ -209,7 +242,7 @@ pub(crate) fn recursive_prover_with_prepared_basis( // it (deeper levels stay dense), mirroring the original. let sks_vks_n1 = eval_sk_at_vks(n1); let span = tracing::info_span!("Induce", level = 0).entered(); - let (basis_0_induced, enforced_sum_0) = induce_sumcheck_poly_auto_base( + let (basis_0_induced, mut enforced_sum_0) = induce_sumcheck_poly_auto_base( n1, log_inv_rate_0, &sks_vks_n1, @@ -218,6 +251,10 @@ pub(crate) fn recursive_prover_with_prepared_basis( &queries_0, &weights_0, ); + // The rows fold the padded codeword: take the padding's share off each query, the basis unchanged. + if hiding.is_some() { + enforced_sum_0 += padding_correction(n1, log_inv_rate_0, &queries_0, &weights_0, &g1); + } drop(span); // Introduce basis_0, then batch the level's claims with powers of lambda_0. diff --git a/crates/pcs/src/whir/tests.rs b/crates/pcs/src/whir/tests.rs index 02664aada..550b1f486 100644 --- a/crates/pcs/src/whir/tests.rs +++ b/crates/pcs/src/whir/tests.rs @@ -33,16 +33,7 @@ fn prove_instance(log_n: usize, seed: u64) -> Instance { let b_initial = eq_table(&point); let target = inner_product_base_ext(&witness, &b_initial); let mut ps = ProverState::from_label(b"whir-test"); - recursive_prover_with_basis( - &pc, - log_n, - &witness, - b_initial.to_vec(), - target, - &pd.codeword, - &pd.merkle_tree, - &mut ps, - ); + recursive_prover_with_basis(&pc, log_n, &witness, b_initial.to_vec(), target, &pd, None, &mut ps); Instance { vc: pc, log_n, @@ -68,6 +59,7 @@ fn verify_with(inst: &Instance, fs: &ProofTranscript, eval_b_at: impl Fn(&[F192] 1 << inst.vc.initial_k(), inst.target, inst.root, + None, |_, point| eval_b_at(point), ) } @@ -239,16 +231,7 @@ fn truncated_lanes_match_an_explicit_zero_tail() { let prove = |msg: &[F64], b: &[F192]| { let (cm, pd) = commit(msg, log_n, pc.initial_k(), pc.log_inv_rates()[0]); let mut ps = ProverState::from_label(b"whir-test"); - recursive_prover_with_basis( - &pc, - log_n, - msg, - b.to_vec(), - target, - &pd.codeword, - &pd.merkle_tree, - &mut ps, - ); + recursive_prover_with_basis(&pc, log_n, msg, b.to_vec(), target, &pd, None, &mut ps); (cm.root, ps.into_proof()) }; let (root_trunc, fs_trunc) = prove(&witness[..used], &b_initial[..used]); @@ -276,9 +259,16 @@ fn truncated_lanes_match_an_explicit_zero_tail() { // The verifier evaluates the weight over the whole `2^log_n` cube. let verify = |fs: &ProofTranscript| { let mut vs = VerifierState::from_label(b"whir-test", fs); - recursive_verifier_with_basis_succinct(&mut vs, &pc, log_n, n_lanes, target, root_trunc, |_, point| { - dense_mle(&b_initial, point) - }) + recursive_verifier_with_basis_succinct( + &mut vs, + &pc, + log_n, + n_lanes, + target, + root_trunc, + None, + |_, point| dense_mle(&b_initial, point), + ) }; assert_eq!(verify(&fs_trunc), Ok(()), "verify failed at n_lanes = {n_lanes}"); @@ -297,6 +287,81 @@ fn truncated_lanes_match_an_explicit_zero_tail() { } } +/// The novel basis at the point of codeword position `p` (the field element `F64(p)`): `X_j(p)` for `j < 2^m`, then `W_m(p)`. +/// +/// `X_j` is the product of the normalized subspace polynomials `W_b = s_b / s_b(v_b)` over the bits `b` of `j`, `s_b = s_{b-1} (s_{b-1} + s_{b-1}(v_{b-1}))`. +fn novel_basis_at(p: usize, m: usize) -> (Vec, F64) { + let sks = eval_sk_at_vks(m); + let mut s = F64(p as u64); + let mut w = Vec::with_capacity(m + 1); + for b in 0..=m { + if b > 0 { + s *= s + sks[b - 1]; + } + w.push(s * sks[b].inv()); + } + let mut x = vec![F64::ONE]; + for &w_b in &w[..m] { + let high: Vec = x.iter().map(|&v| v * w_b).collect(); + x.extend(high); + } + (x, w[m]) +} + +/// Every lane of a hiding commitment is its `2^m + k` coefficients evaluated at every domain point: `Σ_j msg_j X_j(x) + W_m(x + s) Σ_j pad_j X_j(x)`, `s = F64(2^(m + r))`. +/// +/// The shapes take the encode's plans: replicas copied before a deep pass, and a gathered first pass at the rate layer (many lanes), at `r = 1` and beyond, the padding at most a whole lane. +#[test] +fn a_hiding_commitment_encodes_the_padded_lanes() { + let mut rng = Rng::new(0x9AD); + for (m, log_inv_rate, log_batch_size, n_lanes, k) in [ + (3usize, 1usize, 2usize, 3usize, 8usize), + (5, 2, 3, 7, 5), + (6, 4, 1, 2, 64), + (9, 1, 3, 5, 37), + (8, 1, 11, 2048, 13), + (8, 2, 11, 2048, 9), + ] { + let log_n = m + log_batch_size; + let msg: Vec = (0..n_lanes << m).map(|_| F64(rng.next_u64())).collect(); + let pads: Vec = (0..n_lanes * k).map(|_| F64(rng.next_u64())).collect(); + let (_, pd) = commit_hiding(&msg, log_n, log_batch_size, log_inv_rate, &pads); + assert_eq!(pd.pads, pads); + // Every lane of a narrow commitment; the ends and a spread of a wide one's. + let lanes: Vec = (0..n_lanes) + .filter(|&u| n_lanes < 64 || u % 97 == 0 || u + 1 == n_lanes) + .collect(); + let s = 1usize << (m + log_inv_rate); + for p in 0..s { + let (x, _) = novel_basis_at(p, m); + let (_, w_m_shifted) = novel_basis_at(p ^ s, m); + for &u in &lanes { + let at = |coeffs: &[F64]| coeffs.iter().zip(&x).fold(F64::ZERO, |acc, (&c, &x_j)| acc + c * x_j); + let want = at(&msg[u << m..(u + 1) << m]) + w_m_shifted * at(&pads[u * k..(u + 1) * k]); + assert_eq!( + pd.codeword[p * n_lanes + n_lanes - 1 - u], + want, + "lane {u}, position {p}, m={m}, rate={log_inv_rate}, n_lanes={n_lanes}, k={k}" + ); + } + } + } +} + +/// No domain point escapes the padding: a zero message padded by the constant one is nonzero everywhere. +/// +/// Padded by `W_m` alone, the first `2^m` points would show the message unmasked to any query landing there. +#[test] +fn a_hiding_commitment_pads_every_point() { + for (m, log_inv_rate) in [(3usize, 1usize), (6, 2), (10, 1), (8, 4)] { + let (_, pd) = commit_hiding(&vec![F64::ZERO; 1 << m], m + 1, 1, log_inv_rate, &[F64::ONE]); + assert!( + pd.codeword.iter().all(|&w| w != F64::ZERO), + "an unpadded point at m={m}, rate={log_inv_rate}" + ); + } +} + /// The sparse transposed-NTT induce must be byte-identical to the dense /// LCH-expansion induce (same guarantee the original pins). Covers both /// the windowed sparse-prefix path (log_block >= 12, k = 8) and the diff --git a/crates/pcs/src/whir/verify.rs b/crates/pcs/src/whir/verify.rs index 48d451950..c740b48c6 100644 --- a/crates/pcs/src/whir/verify.rs +++ b/crates/pcs/src/whir/verify.rs @@ -8,9 +8,10 @@ //! It is written once over the opening verifier's operations, so the native verifier and the recursion machine's rows run the same steps. //! Every query opens a full row whose path follows the query's bits, so the rows never depend on which rows are opened. +use super::Hiding; use crate::verifier::OpeningVerifier; use crate::whir::config::{ConfigError, VerifierConfig}; -use crate::whir::induce::eval_sk_at_vks; +use crate::whir::induce::{eval_sk_at_vks, padding_shift}; use fiat_shamir::transcript::TranscriptError; use primitives::field::{F64, F192}; use thiserror::Error; @@ -42,6 +43,12 @@ pub enum WhirError { /// The final folded value does not match the claimed evaluation. #[error("the final sumcheck claim does not match the opening")] TerminalMismatch, + /// A hiding opening pads as its configuration does not. + #[error("a hiding opening of {k} padding coefficients, and the configuration pads by {padding}")] + Padding { k: usize, padding: usize }, + /// The running claim a hiding opening reveals after the lane fold is not the one its rounds reach. + #[error("the revealed running claim does not match the lane fold")] + RevealedClaim, } /// A round's quadratic `c + b X + a X^2`. @@ -109,6 +116,13 @@ struct WhirReplay<'c, V: OpeningVerifier> { /// The level-0 rows a query batch opened, one per query, of committed words. struct BaseRows(Vec>); +/// A hiding opening's padding folded by the lane challenges, `g_1`, past lanes of `2^log_msg_cols` words, and its factor's shift [`padding_shift`]. +struct FoldedPadding { + g1: Vec, + log_msg_cols: usize, + shift: F64, +} + /// A later level's rows a query batch opened, one per query, of elements of `E`. struct ExtRows(Vec>); @@ -121,19 +135,26 @@ struct ExtRows(Vec>); /// Per-level induced bases are never materialized: a level's enforced sum is recomputed from its opened rows, and its basis taken in closed form at the terminal point. /// The L0 rows the proof stores are the committed lanes, `n_lanes` of them, which the caller derives from the announced layout. /// +/// With `hiding` the commitment is a hiding one: after the lane fold's last challenge the verifier turns hiding off, reads and checks the revealed running claim if `hidden_claim`, then reads the padding's lane fold `g_1`, which each level-0 query takes off its folded row. +/// /// # Errors /// -/// Returns a lane count a leaf cannot hold, a configuration that does not fit the witness, a malformed stream, or a terminal claim the opening does not reproduce. -pub(crate) fn recursive_verifier_with_basis_succinct( +/// Returns a lane count a leaf cannot hold, a configuration that does not fit the witness or pads otherwise than `hiding`, a malformed stream, a revealed claim the lane fold does not reach, or a terminal claim the opening does not reproduce. +#[expect( + clippy::too_many_arguments, + reason = "The verifier keeps its independent inputs explicit, as the prover does." +)] +pub fn recursive_verifier_with_basis_succinct( v: &mut V, config: &VerifierConfig, log_n: usize, n_lanes: usize, target: V::E, root: V::Root, + hiding: Option, weight_at: impl FnOnce(&mut V, &[V::E]) -> V::E, ) -> Result<(), WhirError> { - WhirReplay::run(v, config, log_n, n_lanes, target, root, weight_at) + WhirReplay::run(v, config, log_n, n_lanes, target, root, hiding, weight_at) } impl Quad { @@ -234,6 +255,10 @@ impl<'c, V: OpeningVerifier> WhirReplay<'c, V> { /// The succinct WHIR verifier. /// /// The caller's weight is evaluated once, at the terminal point indexed by witness coordinate. + #[expect( + clippy::too_many_arguments, + reason = "The verifier keeps its independent inputs explicit, as the prover does." + )] fn run( v: &mut V, config: &'c VerifierConfig, @@ -241,6 +266,7 @@ impl<'c, V: OpeningVerifier> WhirReplay<'c, V> { n_lanes: usize, target: V::E, root: V::Root, + hiding: Option, weight_at: impl FnOnce(&mut V, &[V::E]) -> V::E, ) -> Result<(), WhirError> { let initial_k = config.initial_k(); @@ -248,6 +274,14 @@ impl<'c, V: OpeningVerifier> WhirReplay<'c, V> { if n_lanes == 0 || n_lanes > max { return Err(WhirError::LaneCount { n_lanes, max }); } + if let Some(h) = hiding + && h.k != config.padding() + { + return Err(WhirError::Padding { + k: h.k, + padding: config.padding(), + }); + } let quad = Quad::recv(v, target)?; let mut w = Self { config, @@ -260,7 +294,14 @@ impl<'c, V: OpeningVerifier> WhirReplay<'c, V> { let mut n_current = log_n .checked_sub(initial_k) .ok_or(WhirError::InvalidShape { level: 0 })?; - let lane_fold = w.fold_rounds(v, initial_k)?; + // The lane fold, the padding revealed between its last challenge and the round after it. + let mut lane_fold = w.fold_rounds(v, initial_k - 1)?; + lane_fold.push(w.fold_challenge(v)); + let padding = match hiding { + Some(h) => Some(w.reveal(v, h, n_current)?), + None => None, + }; + w.quad = Quad::recv(v, w.t_r)?; let root_1 = v.next_root()?; let oods = (0..config.ood_samples()[1]) .map(|_| Ood::replay(v, n_current)) @@ -272,7 +313,7 @@ impl<'c, V: OpeningVerifier> WhirReplay<'c, V> { for row in &mut rows { row.reverse(); } - Ok(BaseRows(rows).enforced_sum(v, &lane_fold, weights)) + Ok(BaseRows(rows).enforced_sum(v, &lane_fold, weights, queries, padding.as_ref())) })?; let mut oracle = w.oracle(root_1, 0, n_current)?; @@ -324,15 +365,35 @@ impl<'c, V: OpeningVerifier> WhirReplay<'c, V> { fn fold_rounds(&mut self, v: &mut V, k: usize) -> Result, TranscriptError> { let mut rs = Vec::with_capacity(k); for _ in 0..k { - let ri = v.sample(); - self.t_r = self.quad.eval(v, ri); + rs.push(self.fold_challenge(v)); self.quad = Quad::recv(v, self.t_r)?; - rs.push(ri); } - self.ris.extend_from_slice(&rs); Ok(rs) } + /// A fold round's challenge, and the running claim it takes the round's quadratic to. + fn fold_challenge(&mut self, v: &mut V) -> V::E { + let ri = v.sample(); + self.t_r = self.quad.eval(v, ri); + self.ris.push(ri); + ri + } + + /// What a hiding opening reveals after the lane fold: with `hidden_claim`, the running claim in the clear, which must be the one the rounds reached; then the padding's lane fold. + fn reveal(&mut self, v: &mut V, hiding: Hiding, log_msg_cols: usize) -> Result, WhirError> { + if hiding.hidden_claim { + v.set_hidden(false); + let a = v.next_scalar()?; + v.ensure_eq(self.t_r, a, || WhirError::RevealedClaim)?; + self.t_r = a; + } + Ok(FoldedPadding { + g1: v.next_scalars(hiding.k)?, + log_msg_cols, + shift: padding_shift(log_msg_cols, self.config.log_inv_rates()[0]), + }) + } + /// One query batch: grind, draw the queries and their batching challenge, open them, then batch the level's claims. /// /// `enforced` opens the queries and returns their weighted sum at the level's fold point. @@ -447,20 +508,67 @@ impl<'c, V: OpeningVerifier> WhirReplay<'c, V> { } impl BaseRows { - /// The level-0 enforced sum over `K` rows: `sum_i w_i `. + /// The level-0 enforced sum over `K` rows: `sum_i w_i ( + p(q_i))`, `p` the padding's share of the folded codeword, if any. /// /// Each row's inner product is its own, so the first query's weight, one, costs no product in rows. - fn enforced_sum>(&self, v: &mut V, point: &[V::E], weights: &[V::E]) -> V::E { + fn enforced_sum>( + &self, + v: &mut V, + point: &[V::E], + weights: &[V::E], + queries: &[V::Query], + padding: Option<&FoldedPadding>, + ) -> V::E { let rows = &self.0; let eq = v.eq_table_prefix(point, rows[0].len()); let zero = v.zero(); - (rows.iter().zip(weights)).fold(zero, |acc, (row, &w)| { - let inner = (eq.iter().zip(row)).fold(zero, |s, (&e, &k)| v.mul_k_add(e, k, s)); + (rows.iter().zip(weights).zip(queries)).fold(zero, |acc, ((row, &w), query)| { + let start = padding.map_or(zero, |p| p.at(v, query)); + let inner = (eq.iter().zip(row)).fold(start, |s, (&e, &k)| v.mul_k_add(e, k, s)); v.mul_add(w, inner, acc) }) } } +impl FoldedPadding { + /// `W_m(x + s) sum_j g_1[j] X_j(x)` at a query's point `x`: the padding's share of the folded codeword there, which taking off (adding, in characteristic two) leaves the folded message's codeword. + /// + /// `X_j` is the product of the normalized subspace polynomials `W_b` over the bits `b` of `j`, so the sum folds the top bit of `j` at a time. + fn at>(&self, v: &mut V, query: &V::Query) -> E { + let m = self.log_msg_cols; + let sks = eval_sk_at_vks(m); + let normalize = |v: &mut V, s: E, b: usize| v.mul_const(s, F192::from(sks[b].inv())); + // `W_b(x)` for the bits of `j < k`, then `W_m(x)`, by the recurrence of `LevelCtx::basis_at`. + let bits = self.g1.len().next_power_of_two().trailing_zeros() as usize; + let mut s = v.query_point(query); + let mut w = Vec::with_capacity(bits); + for b in 0..=m { + if b > 0 { + let u = v.mul_const(s, F192::from(sks[b - 1])); + s = v.mul_add(s, s, u); + } + if b < bits { + w.push(normalize(v, s, b)); + } + } + let w_m = normalize(v, s, m); + let w_m = v.add_const(w_m, F192::from(self.shift)); + let mut g = self.g1.clone(); + while g.len() > 1 { + let half = g.len().next_power_of_two() >> 1; + let w_b = w[half.trailing_zeros() as usize]; + for j in 0..g.len() - half { + g[j] = v.mul_add(w_b, g[j + half], g[j]); + } + g.truncate(half); + } + match g.first() { + Some(&p) => v.mul(w_m, p), + None => v.zero(), + } + } +} + impl ExtRows { /// A later level's enforced sum over `E` rows: `sum_l eq(v, l) sum_i w_i row_i[l]`. fn enforced_sum>(&self, v: &mut V, point: &[E], weights: &[E]) -> E { diff --git a/doc/leanvm/body/b-polynomial-commitment-scheme.tex b/doc/leanvm/body/b-polynomial-commitment-scheme.tex index 449db01b3..e296ce1bf 100644 --- a/doc/leanvm/body/b-polynomial-commitment-scheme.tex +++ b/doc/leanvm/body/b-polynomial-commitment-scheme.tex @@ -41,6 +41,8 @@ \section{The polynomial commitment scheme: WHIR \slash Ligerito}\label{annex:pcs $\bfarr$ & $B$ & butterfly array\\ $\mpoly$ & $P$ & message polynomial ($P_i$ is a committed column)\\ $e_c$ & $\beta_c$ & the fixed $\Ftwo$-basis, as in Annex \ref{annex:rs}\\ +$\npad$, $\padc_u$ & (none) & padding size, row $u$'s padding (\S\ref{sec:pcs-zk})\\ +$\padfold$, $\rlane$ & (none) & folded padding, random row (\S\ref{sec:pcs-zk})\\ \hline \end{tabular} \end{center} @@ -309,6 +311,50 @@ \subsection{Optimizations}\label{sec:pcs-opt} Conclusion: at commitment, both the FFT and the Merkle leaf hashing cost are proportional to $\nstack$ (not its next power of two). Unfortunately we still pay for the padding inside the $\nstack$ field elements, because some instruction counts are not powers of two. This could be prevented using the Jagged PCS \cite{jagged_pcs}. +%===================================================================== +\subsection{The hiding commitment}\label{sec:pcs-zk} +%===================================================================== + +A leaf proved in zero knowledge commits to its stack and opens it with the hiding variant of Protocol~\ref{fig:protocol} below, after VEIL~\cite{DHRR26}: every committed row of $\orc^{(0)}$ is padded past its power of two, and one committed row is uniformly random. Only level $0$ changes; every deeper level commits an unpadded fold and runs as before. Write $\kappa := \kappa_0$ and $\rexp := \rexp_0$, so that $\dom_0 = \subsp_{\kappa + \rexp}$, and set +\[ +\npad := \nq_0 + 2, \qquad \padshift := e_{\kappa + \rexp}, +\] +the first basis element past $\dom_0$. + +\paragraph{Commit.} For each committed row $u$ the prover draws a uniform padding $\padc_u \in \K^{\npad}$ and sends +\[ +\orc^{(0)}[u, \cdot] := \Bigl(\mpoly_{f(u, \cdot)}(x) + \Wn{\kappa}(x + \padshift) \sum_{j < \npad} \padc_u[j]\, \novel_j(x)\Bigr)_{x \in \dom_0}. +\] +Its last committed row $\rlane$, $\langle \rlane \rangle = \nrows - 1$, holds uniform elements of $\K$ and is padded like the others; no input claim's weight touches it. +\begin{itemize}[itemsep=1pt,topsep=2pt] +\item \emph{The code.} $\Wn{\kappa}$ is $\Ftwo$-linear (Lemma~\ref{lem:subspace}), so $\Wn{\kappa}(X + \padshift) = \Wn{\kappa}(X) + \Wn{\kappa}(\padshift)$, and $\Wn{\kappa} \novel_j = \novel_{2^\kappa + j}$ for $j < 2^\kappa$. A row is therefore the encoding of $2^\kappa + \npad$ novel-basis coefficients ($\npad \le 2^\kappa$), a codeword of $\cpad_0 := \RS[\E, \dom_0, 2^\kappa + \npad]$ on the same domain. The additive NTT computes it with one more butterfly layer, the one at layer $\rexp - 1$ that pairs the message with the padding: the replica of the message on the coset $c + \subsp_\kappa$ of $\dom_0$ starts as the message plus $\Wn{\kappa}(c + \padshift)$ times the padding, which the encoder adds as its first pass reads the message. +\item \emph{No point is left unpadded.} $\Wn{\kappa}$ vanishes on $\subsp_\kappa$, the first $2^\kappa$ points of $\dom_0$, so a padding by $\novel_{2^\kappa + j} = \Wn{\kappa} \novel_j$ alone would leave every query landing there unmasked. $\Wn{\kappa}$ maps $\dom_0$ onto the span of $\Wn{\kappa}(e_\kappa), \dots, \Wn{\kappa}(e_{\kappa + \rexp - 1})$ and is injective on $\langle e_\kappa, \dots, e_{63} \rangle$, so $\Wn{\kappa}(\padshift)$ lies outside that span, and $\Wn{\kappa}(x + \padshift) \neq 0$ for every $x \in \dom_0$. +\item \emph{Decoding.} A polynomial of degree below $2^\kappa + \npad$ is uniquely $\mpoly_g + \Wn{\kappa}(X + \padshift) R$ with $\deg R < \npad$ (division by $\Wn{\kappa}(X + \padshift)$, of degree $2^\kappa$), and a row $U$ of a codeword of $\cpad_0$ decodes to that $g$. The claims are on $g$; the padding is no part of the committed polynomial. +\end{itemize} + +\paragraph{Open.} Right after the last lane-fold challenge $\fc_{\ell_0}$, with $c' = \rc{\ell_0}$ fixed and before the next round polynomial: +\begin{enumerate}[itemsep=1pt,topsep=2pt] +\item In the zero-knowledge proof every scalar the prover sent so far travelled under a one-time key, and $\mathbf{V}$ holds $c'$ only as an expression of keyed values. $\mathbf{P}$ sends $c'$ in the clear, $\mathbf{V}$ checks it against that expression and continues from it, and every later scalar travels in the clear. +\item $\mathbf{P}$ sends the paddings folded as the rows are, $\padfold := \sum_{u} \eq(\fc, u)\, \padc_u \in \E^{\npad}$. +\item At level $0$, step 3(c) takes the padding off each folded column: +\[ +c_q := \sum_{u} \eq(\fc, u)\, \orc^{(0)}[u, x_q] + \Wn{\kappa}(x_q + \padshift) \sum_{j < \npad} \padfold[j]\, \novel_j(x_q) +\] +(the subtraction, in characteristic $2$), which is $\Enc_0(f^{(1)})[x_q]$ for an honest prover. $\mathbf{V}$ evaluates $\Wn{\kappa}(x_q)$ and the $\novel_j(x_q)$ by the recurrence of Lemma~\ref{lem:subspace}, adds the constant $\Wn{\kappa}(\padshift)$, and folds the sum one bit of $j$ at a time: $\kappa$ squarings and fewer than $\npad$ products per query. +\end{enumerate} +Everything else is Protocol~\ref{fig:protocol}; the induced level-$1$ claims are on the $2^\kappa$ coefficients of $f^{(1)}$ as before. + +\paragraph{Soundness.} Theorem~\ref{thm:rbr} holds with level $0$'s code $\cpad_0$, of dimension $2^\kappa + \npad$ and rate $\rate_0 = (2^\kappa + \npad)\, 2^{-\kappa - \rexp}$, in every level-$0$ term: $L_0$, $\epsilon_0$, $\rad_0$ and the query term. The deeper levels keep theirs. The proof reads Protocol~\ref{fig:protocol} with $\cpad_0$ at level $0$ and changes in one place, the query step of level $0$, where $c$ becomes the corrected word $c^\star := \orc^{(0)}_\fc + \Wn{\kappa}(\cdot + \padshift)\, \mpoly_{\padfold}$, $\mpoly_{\padfold} := \sum_{j < \npad} \padfold[j] \novel_j$. If $\Enc_0(g^\ast)$ agrees with $c^\star$ on at least $(1 - \rad_0)\blen_0$ columns, then $\Enc_0(g^\ast) + \Wn{\kappa}(\cdot + \padshift)\, \mpoly_{\padfold}$ is a codeword of $\cpad_0$ within $\rad_0$ of $\orc^{(0)}_\fc$ that decodes to $g^\ast$, which therefore violates the residual claim; otherwise all $\nq_0$ queries land in the agreement set with probability less than $(1 - \rad_0)^{\nq_0}$, as before. $\padfold$ and $c'$ are prover messages and add no error term, and the random row is one more row of the stack, with no claim on it. + +The query counts are rederived by the analysis of Theorem~\ref{thm:rbr} for every size and rate, with level $0$'s rate the padded one, at the fixed point $\npad = \nq_0 + 2$: the derivation starts from the unpadded $\nq_0 + 2$ and rederives until $\nq_0$ no longer moves, which it does since a larger padding never needs fewer queries. They differ from the unpadded counts only at rate $1/2$, by a few level-$0$ queries, and most at the smallest stack. The padded code's list bound $L_0$, rederived with its own slack, stays within the $2^{12}$ every challenge before the opening pays (\S\ref{sec:e2e-ledger}). The hiding variant needs $\kappa \ge 14$, a stack of at least $2^{20}$ elements, for the reason below. + +\paragraph{Zero knowledge.} The argument is for an honest verifier and statistical, then Fiat-Shamir in the random-oracle model. Every scalar sent before the lane fold's end is uniform, each under its own key. What the opening reveals besides is simulated in three parts. +\begin{itemize}[itemsep=1pt,topsep=2pt] +\item \emph{Level-$0$ answers.} For distinct $x_1, \dots, x_t \in \dom_0$ with $t \le \npad$, the map $\padc \mapsto \bigl(\Wn{\kappa}(x_i + \padshift) \sum_{j < \npad} \padc[j] \novel_j(x_i)\bigr)_i$ is onto $\K^t$: the $\novel_j$, $j < \npad$, span the polynomials of degree below $\npad$, which take any $t \le \npad$ values at $t$ points, and every factor is nonzero. So any $\npad$ symbols of a padded row are uniform whatever its message, the $(\nq_0 + 1)$-wise independence of the padded code~\cite{DHRR26,Dia25}, and a query message opens at most $\nq_0$ distinct columns. +\item \emph{Roots.} Given the opened columns, one more symbol of each row is still uniform ($\nq_0 + 1 \le \npad$), so each unopened leaf keeps one spare uniform symbol of $\K$ per row, $64$ bits of fresh entropy, and the root and the authentication paths are simulated in the random-oracle model with no salt. +\item \emph{After the lane fold.} No claim touches $\rlane$, so the lane fold gives $f^{(1)} = \sum_{u} \eq(\fc, u)\, f(u, \cdot)$ the term $\eq(\fc, \rlane)\, f(\rlane, \cdot)$, a nonzero multiple in $\E$ of a uniform vector of $\K^{2^\kappa}$ unless some $\fc_j$ is $0$ or $1$, which has probability at most $2\ell_0/|\E|$. Every later message is a linear functional of $f^{(1)}$, or for a root a random-oracle hash of the encoding of a fold of it: $c'$, the round and intro polynomials, the OOD answers, the values $c_q$, the opened rows of the levels past $0$, and $\ffinal$. An $\E$-valued functional is three $\K$-linear functionals of $f(\rlane, \cdot)$, and the configurations keep their number at most $2^{\kappa - 1}$, three per $\E$ scalar revealed, which is what fixes $\kappa \ge 14$; under that condition the random row makes them uniform, as VEIL's random column does~\cite[Lemma~4.7]{DHRR26}. The opened level-$0$ columns and $\padfold$ together determine the $c_q$, and reveal nothing more of the messages. This last step adapts VEIL's lemma to an $\E$-fold of $\K$-valued rows, with a random row of $\K$ and fold coefficients in $\E$: it is argued here, not proven. +\end{itemize} + %===================================================================== \subsection{The Johnson bound}\label{app:johnson} diff --git a/doc/leanvm/preamble/macros.tex b/doc/leanvm/preamble/macros.tex index e4af15aad..7d56fceb4 100644 --- a/doc/leanvm/preamble/macros.tex +++ b/doc/leanvm/preamble/macros.tex @@ -154,6 +154,12 @@ \newcommand{\strh}{h_{\mathrm{st}}} % a group of stratified columns has 2^\strh columns \newcommand{\strs}{s_{\mathrm{st}}} % the top index bits a group of stratified columns fixes \newcommand{\stcov}[1]{a_{\mathrm{st},#1}} % the fraction of coset #1 of a group's fixed bits that a set covers +\newcommand{\npad}{N_{\mathrm{pad}}} % coefficients a hiding commitment pads each level-0 row with, past its power of two +\newcommand{\padc}{\mathsf{p}} % a level-0 row's padding: its \npad coefficients past the power of two +\newcommand{\padfold}{\bar{\mathsf{p}}} % the paddings folded by the lane challenges, sent after the lane fold +\newcommand{\padshift}{s_{\mathrm{pad}}} % the shift of the padding's factor: the first basis element past the domain +\newcommand{\rlane}{u_{\mathrm{rnd}}} % the uniformly random level-0 row of a hiding commitment +\newcommand{\cpad}{\mathcal{C}^{\mathrm{pad}}} % the padded level-0 code of a hiding commitment % ---------- novel basis and additive NTT (Annex D) ---------- \newcommand{\subsp}{\mathcal{U}} % F_2-subspace (was U_i) diff --git a/doc/leanvm/refs.bib b/doc/leanvm/refs.bib index 53c251e0f..3d93a0042 100644 --- a/doc/leanvm/refs.bib +++ b/doc/leanvm/refs.bib @@ -63,6 +63,22 @@ @misc{Jo26 url = {https://eprint.iacr.org/2026/891}, } +@misc{DHRR26, + author = {Rahul Dalal and Tamir Hemo and Eugene Rabinovich and Ron D. Rothblum}, + title = {{VEIL}: Lightweight Zero-Knowledge for Hash-Based Multilinear Proof Systems}, + year = {2026}, + howpublished = {Cryptology ePrint Archive, Paper 2026/683}, + url = {https://eprint.iacr.org/2026/683}, +} + +@misc{Dia25, + author = {Benjamin E. Diamond}, + title = {Zero-Knowledge Polynomial Commitment in Binary Fields}, + year = {2025}, + howpublished = {Cryptology ePrint Archive, Paper 2025/1015}, + url = {https://eprint.iacr.org/2025/1015}, +} + @inproceedings{BCS16, author = {Eli Ben-Sasson and Alessandro Chiesa and Nicholas Spooner}, title = {Interactive Oracle Proofs}, From 94e932aa5c88abe69ed45c59e2c29e3bdfe24bc5 Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sat, 10 Oct 2026 13:56:47 +0100 Subject: [PATCH 02/14] zk: drop the constraint rendering kept for a Python verifier The Python verifier is gone upstream (#537) and its zero-knowledge mirror was never started, so nothing reads Program::zk_constraints. --- crates/leanvm_core/src/cpu/program.rs | 11 ------- crates/leanvm_core/src/cpu/zk.rs | 45 ++------------------------- 2 files changed, 2 insertions(+), 54 deletions(-) diff --git a/crates/leanvm_core/src/cpu/program.rs b/crates/leanvm_core/src/cpu/program.rs index b569e7b42..935f73655 100644 --- a/crates/leanvm_core/src/cpu/program.rs +++ b/crates/leanvm_core/src/cpu/program.rs @@ -370,17 +370,6 @@ impl Program { Ok(raw) } - /// Verify a zero-knowledge proof and render the outer constraint system its verifier recorded, the form the Python - /// verifier renders too. - /// - /// # Errors - /// - /// Returns the first stage that refuses the proof. - #[doc(hidden)] - pub fn zk_constraints(&self, output: Output, proof: &Proof) -> Result { - super::zk::render_constraints(self, output, proof) - } - /// The verifier's core: every check that depends on the proof. /// /// It returns the claims the proof leaves on polynomials only the program or the VM's circuits fix. diff --git a/crates/leanvm_core/src/cpu/zk.rs b/crates/leanvm_core/src/cpu/zk.rs index cca8cb257..19c396c69 100644 --- a/crates/leanvm_core/src/cpu/zk.rs +++ b/crates/leanvm_core/src/cpu/zk.rs @@ -20,10 +20,9 @@ use crate::pcs::{self, Commitment, Committed, LOG_BATCH, Rate}; use crate::tables::Clock; use crate::zk::keys::{self, KEY_MU, KeyStack, LANE, MAX_KEYS, MAX_OUTER_LOG_ROWS}; use crate::zk::outer::constraint_system; -use crate::zk::r1cs::R1cs; use crate::zk::randomness::{Purpose, Randomness, ZkRng}; use crate::zk::spartan::{self, OuterClaims, SpartanError}; -use crate::zk::sym::{Form, Kind, Record, Recorder, Sym, Var}; +use crate::zk::sym::{Form, Recorder, Sym, Var}; use ::pcs::verifier::OpeningVerifier; use ::pcs::whir::{self, Hiding, ProverData, WhirError, config_for_rate_hiding}; use fiat_shamir::arith::{Arith, Verifier}; @@ -125,12 +124,6 @@ pub(super) fn prove(program: &Program, mut w: Witness, output: Output, rate: Rat /// /// Returns the first stage that refuses the proof. pub(super) fn verify(program: &Program, output: Output, proof: &Proof) -> Result { - verify_recorded(program, output, proof).map(|(raw, _, _)| raw) -} - -/// Verify a zero-knowledge proof, and return it with every query's Merkle path written out, with what the verifier -/// recorded and the outer constraint system it stated. -fn verify_recorded(program: &Program, output: Output, proof: &Proof) -> Result<(RawProof, Record, R1cs), CpuError> { let vs = VerifierState::new(program.seed(true), &proof.0, output.words().map(F64)); let mut rec = Recorder::new(vs); let (key_root, rate) = record(program, &mut rec, output)?; @@ -159,41 +152,7 @@ fn verify_recorded(program: &Program, output: Output, proof: &Proof) -> Result<( let claims = spartan::verify(&mut vs, &r1cs).map_err(|SpartanError::Transcript(e)| CpuError::Transcript(e))?; verify_keys(&mut vs, key_root, &claims, rate.log_inv_rate().into()).map_err(CpuError::KeyOpen)?; vs.finish()?; - Ok((vs.into_raw_proof(), record, r1cs)) -} - -/// What the verifier of a zero-knowledge proof recorded, one line each, for the Python verifier to state the same: the -/// key and variable counts, each auxiliary variable's digest and kind in the outer system's order, then each linear -/// constraint's digest, then each bit's. -/// -/// # Errors -/// -/// Returns the first stage that refuses the proof. -pub(super) fn render_constraints(program: &Program, output: Output, proof: &Proof) -> Result { - let (_, record, r1cs) = verify_recorded(program, output, proof)?; - let hex = |d: &[u8; 32]| d.iter().map(|b| format!("{b:02x}")).collect::(); - let mut lines = vec![ - format!("keys {}", record.n_keys), - format!("auxiliary {}", record.aux.len()), - format!("rows {}", r1cs.n_rows()), - ]; - for j in record.aux_order() { - let aux = &record.aux[j as usize]; - let kind = match aux.kind { - Kind::Product => "product", - Kind::Inverse => "inverse", - Kind::Bind => "bind", - }; - lines.push(format!("{kind} {}", hex(&aux.digest))); - } - let sorted = |list: &[([u8; 32], Form)]| { - let mut digests: Vec<[u8; 32]> = list.iter().map(|(d, _)| *d).collect(); - digests.sort_unstable(); - digests - }; - lines.extend(sorted(&record.linear).iter().map(|d| format!("linear {}", hex(d)))); - lines.extend(sorted(&record.booleans).iter().map(|d| format!("bit {}", hex(d)))); - Ok(lines.join("\n")) + Ok(vs.into_raw_proof()) } /// The plain verifier over a padded transcript, recorded: the shape, the two roots, the final clock's bits, the core, From 358999b53bab15cd1783fdf382ecfc440a90a3cb Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sat, 10 Oct 2026 13:59:37 +0100 Subject: [PATCH 03/14] pcs: take a hiding opening's padding from its configuration Hiding carried the padding length beside the configuration that fixes it, and every caller passed config.padding(); the verifier's check of the two against each other and its error variant go with it. The transcript is unchanged. --- crates/leanvm_core/src/cpu/zk.rs | 10 ++-------- crates/leanvm_core/src/pcs.rs | 15 +++++---------- crates/pcs/src/stack_open/mod.rs | 30 +++++------------------------- crates/pcs/src/whir/mod.rs | 4 +--- crates/pcs/src/whir/prove.rs | 14 +++++--------- crates/pcs/src/whir/verify.rs | 15 ++------------- 6 files changed, 20 insertions(+), 68 deletions(-) diff --git a/crates/leanvm_core/src/cpu/zk.rs b/crates/leanvm_core/src/cpu/zk.rs index 19c396c69..e9a5c2752 100644 --- a/crates/leanvm_core/src/cpu/zk.rs +++ b/crates/leanvm_core/src/cpu/zk.rs @@ -194,10 +194,7 @@ fn open_keys(ps: &mut ProverState, stack: &KeyStack, data: &ProverData, claims: let lambda = ps.sample(); let (mut weight, target) = keys::opening_claim(claims, lambda); weight.resize(2 * LANE, F192::ZERO); - let hiding = Hiding { - k: cfg.padding(), - hidden_claim: false, - }; + let hiding = Hiding { hidden_claim: false }; whir::recursive_prover_with_basis(&cfg, KEY_MU, &stack.words, weight, target, data, Some(hiding), ps); } @@ -206,10 +203,7 @@ fn verify_keys(vs: &mut VerifierState, root: Hash, claims: &OuterClaims, log_inv let cfg = config_for_rate_hiding(KEY_MU, log_inv_rate)?; let lambda = Challenger::sample(vs); let (weight, target) = keys::opening_claim(claims, lambda); - let hiding = Hiding { - k: cfg.padding(), - hidden_claim: false, - }; + let hiding = Hiding { hidden_claim: false }; // The weight lives on lane 0, the stack's first `LANE` words: its low variables index the word, the rest are zero. let weight_at = |_: &mut VerifierState, x: &[F192]| { let low = LANE.trailing_zeros() as usize; diff --git a/crates/leanvm_core/src/pcs.rs b/crates/leanvm_core/src/pcs.rs index b57be442d..90442dd38 100644 --- a/crates/leanvm_core/src/pcs.rs +++ b/crates/leanvm_core/src/pcs.rs @@ -107,11 +107,8 @@ fn config(shape: StackShape, rate: Rate) -> Result { } /// A zero-knowledge proof's opening of its stack: every scalar before the lane fold's end is hidden. -fn hiding(shape: StackShape, config: &ProverConfig) -> Option { - shape.random_lane.then(|| Hiding { - k: config.padding(), - hidden_claim: true, - }) +fn hiding(shape: StackShape) -> Option { + shape.random_lane.then_some(Hiding { hidden_claim: true }) } /// The padding coefficients a hiding commitment of a `2^μ`-word witness takes per lane. @@ -194,10 +191,9 @@ impl Committed { got: witness.len(), }); } - let k = hiding(shape, &config).map_or(0, |h| h.k); assert_eq!( pads.len(), - n_lanes * k, + n_lanes * config.padding(), "every committed lane takes the configured padding" ); @@ -250,7 +246,7 @@ impl Committed { &self.config, points, rings, - hiding(self.shape, &self.config), + hiding(self.shape), ); Ok(()) } @@ -300,8 +296,7 @@ impl Commitment { ) -> Result<(), WhirError> { // Both sides derive the opening profile from the committed witness's dimension and rate. let config = config(self.shape, self.rate)?; - let hiding = hiding(self.shape, &config); - let n_lanes = self.shape.committed_lanes(); + let (n_lanes, hiding) = (self.shape.committed_lanes(), hiding(self.shape)); pcs::stack_open::verify(v, &config, self.shape.mu, n_lanes, self.root, points, rings, hiding) } } diff --git a/crates/pcs/src/stack_open/mod.rs b/crates/pcs/src/stack_open/mod.rs index 53d354fcf..90be3b0eb 100644 --- a/crates/pcs/src/stack_open/mod.rs +++ b/crates/pcs/src/stack_open/mod.rs @@ -169,7 +169,7 @@ impl StackClaim { /// must match the commit's `log_batch_size` / `log_inv_rate` (enforced by shape /// asserts inside the WHIR prover). /// -/// With `hiding`, `prover_data` is a [`super::whir::commit_hiding`] commitment, padded by `hiding.k` coefficients a lane (the module docs). +/// With `hiding`, `prover_data` is a [`super::whir::commit_hiding`] commitment, padded as the configuration is (the module docs). #[expect( clippy::too_many_arguments, reason = "The opening keeps its independent inputs explicit." @@ -813,11 +813,8 @@ mod tests { .collect() } - const fn hiding(&self, hidden_claim: bool) -> Hiding { - Hiding { - k: self.config.padding(), - hidden_claim, - } + const fn hiding(hidden_claim: bool) -> Hiding { + Hiding { hidden_claim } } /// Commit with these pads and open, the prover holding `prover_pads` as the commitment's. @@ -841,7 +838,7 @@ mod tests { &self.config, &self.point_claims, &self.rings, - Some(self.hiding(hidden_claim)), + Some(Self::hiding(hidden_claim)), ); (cm.root, ps.into_proof()) } @@ -856,7 +853,7 @@ mod tests { root, &self.point_claims, &self.rings, - Some(self.hiding(hidden_claim)), + Some(Self::hiding(hidden_claim)), ) } @@ -898,23 +895,6 @@ mod tests { other[(n_lanes - 1) * k] += F64::ONE; let (root, fs) = st.prove(&pads, Some(other), hidden_claim); assert!(st.verify(root, &fs, hidden_claim).is_err(), "g_1 of other pads, {what}"); - - // The opening pads as its configuration does. - let mut vs = VerifierState::from_label(DOMAIN, &fs); - let short = Hiding { k: k - 1, hidden_claim }; - assert_eq!( - verify( - &mut vs, - &st.config, - st.log_n, - n_lanes, - root, - &st.point_claims, - &st.rings, - Some(short) - ), - Err(WhirError::Padding { k: k - 1, padding: k }) - ); } } diff --git a/crates/pcs/src/whir/mod.rs b/crates/pcs/src/whir/mod.rs index 2442fb12b..5ba3ee511 100644 --- a/crates/pcs/src/whir/mod.rs +++ b/crates/pcs/src/whir/mod.rs @@ -59,11 +59,9 @@ pub use verify::{WhirError, recursive_verifier_with_basis_succinct}; /// The opening of a commitment made by [`commit_hiding`]. /// -/// After the lane fold's last challenge the prover sends the padding's fold `g_1`, `k` scalars, and level 0's queries take it off the folded codeword (the module docs of [`crate::stack_open`]). +/// After the lane fold's last challenge the prover sends the padding's fold `g_1`, the configuration's [`ProverConfig::padding`] scalars, and level 0's queries take it off the folded codeword (the module docs of [`crate::stack_open`]). #[derive(Clone, Copy, Debug, PartialEq, Eq)] pub struct Hiding { - /// Padding coefficients per committed lane: the configuration's [`ProverConfig::padding`]. - pub k: usize, /// The scalars before the lane fold's end travelled under one-time keys: first turn hiding off and send the running claim in the clear, which the verifier checks against the one it holds and continues from. pub hidden_claim: bool, } diff --git a/crates/pcs/src/whir/prove.rs b/crates/pcs/src/whir/prove.rs index ac78408a7..7fd8d8acf 100644 --- a/crates/pcs/src/whir/prove.rs +++ b/crates/pcs/src/whir/prove.rs @@ -58,13 +58,13 @@ fn ext_row_words(row: &[F192]) -> Vec { /// by `stack.len()`; `ood_samples[0] == 0` is what keeps a full-tensor OOD weight /// out of these rounds. /// -/// With `hiding`, `l0` is a hiding commitment whose padding is `hiding.k` coefficients a lane, and the opening reveals the padding's lane fold after the lane fold (the module docs of [`crate::stack_open`]). +/// With `hiding`, `l0` is a hiding commitment padded as the configuration is, and the opening reveals the padding's lane fold after the lane fold (the module docs of [`crate::stack_open`]). /// /// Scalars enter the shared transcript as they are transmitted, and authenticated Merkle openings travel as one phase per level. The caller has already bound the initial commitment and target. /// /// # Panics /// -/// Panics on a shape the commitment does not have, or with `hiding` on a padding of another length than `hiding.k` a lane or than the configuration's. +/// Panics on a shape the commitment does not have, or on a padding of another length than the opening's: the configuration's with `hiding`, none without. #[expect( clippy::too_many_arguments, reason = "The proof kernel keeps its independent inputs explicit." @@ -129,16 +129,12 @@ pub(crate) fn recursive_prover_with_prepared_basis( } assert_eq!(l0_codeword.len(), block_len_0 * n_lanes); assert_eq!(l0_tree.len(), 2 * block_len_0 - 1); - let pad_k = hiding.map_or(0, |h| h.k); + let pad_k = if hiding.is_some() { config.padding() } else { 0 }; assert_eq!( l0.pads.len(), pad_k * n_lanes, "the commitment's padding is the opening's" ); - assert!( - hiding.is_none_or(|h| h.k == config.padding()), - "a hiding opening pads as its configuration" - ); // Nothing is absorbed on entry. The commitment was bound by the `add_root`/`next_root` that // transmitted it, and the target is `sum_i lambda^i * claim_i` over claim values bound by their @@ -187,8 +183,8 @@ pub(crate) fn recursive_prover_with_prepared_basis( } // The padding's lane fold `g_1[j] = Σ_u eq(fold, u) pad_u[j]`, with level 0's lane eq table. let eq = eq_table(&r_lane_fold); - g1 = (0..h.k) - .map(|j| (0..n_lanes).fold(F192::ZERO, |acc, u| acc + eq[u].mul_base(l0.pads[u * h.k + j]))) + g1 = (0..pad_k) + .map(|j| (0..n_lanes).fold(F192::ZERO, |acc, u| acc + eq[u].mul_base(l0.pads[u * pad_k + j]))) .collect(); ps.add_scalars(&g1); } diff --git a/crates/pcs/src/whir/verify.rs b/crates/pcs/src/whir/verify.rs index c740b48c6..8b73c577b 100644 --- a/crates/pcs/src/whir/verify.rs +++ b/crates/pcs/src/whir/verify.rs @@ -43,9 +43,6 @@ pub enum WhirError { /// The final folded value does not match the claimed evaluation. #[error("the final sumcheck claim does not match the opening")] TerminalMismatch, - /// A hiding opening pads as its configuration does not. - #[error("a hiding opening of {k} padding coefficients, and the configuration pads by {padding}")] - Padding { k: usize, padding: usize }, /// The running claim a hiding opening reveals after the lane fold is not the one its rounds reach. #[error("the revealed running claim does not match the lane fold")] RevealedClaim, @@ -139,7 +136,7 @@ struct ExtRows(Vec>); /// /// # Errors /// -/// Returns a lane count a leaf cannot hold, a configuration that does not fit the witness or pads otherwise than `hiding`, a malformed stream, a revealed claim the lane fold does not reach, or a terminal claim the opening does not reproduce. +/// Returns a lane count a leaf cannot hold, a configuration that does not fit the witness, a malformed stream, a revealed claim the lane fold does not reach, or a terminal claim the opening does not reproduce. #[expect( clippy::too_many_arguments, reason = "The verifier keeps its independent inputs explicit, as the prover does." @@ -274,14 +271,6 @@ impl<'c, V: OpeningVerifier> WhirReplay<'c, V> { if n_lanes == 0 || n_lanes > max { return Err(WhirError::LaneCount { n_lanes, max }); } - if let Some(h) = hiding - && h.k != config.padding() - { - return Err(WhirError::Padding { - k: h.k, - padding: config.padding(), - }); - } let quad = Quad::recv(v, target)?; let mut w = Self { config, @@ -388,7 +377,7 @@ impl<'c, V: OpeningVerifier> WhirReplay<'c, V> { self.t_r = a; } Ok(FoldedPadding { - g1: v.next_scalars(hiding.k)?, + g1: v.next_scalars(self.config.padding())?, log_msg_cols, shift: padding_shift(log_msg_cols, self.config.log_inv_rates()[0]), }) From 516af09c16bf186513eb6e84e2d048916b3986e2 Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sat, 10 Oct 2026 14:00:43 +0100 Subject: [PATCH 04/14] leanvm: borrow the commitment the verifier's core opens --- crates/leanvm_core/src/cpu/reduce.rs | 4 ++-- crates/leanvm_core/src/cpu/zk.rs | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/crates/leanvm_core/src/cpu/reduce.rs b/crates/leanvm_core/src/cpu/reduce.rs index 92051d29a..e485acb16 100644 --- a/crates/leanvm_core/src/cpu/reduce.rs +++ b/crates/leanvm_core/src/cpu/reduce.rs @@ -67,7 +67,7 @@ impl Layout { rate: Rate, ) -> Result, CpuError> { let commitment = Commitment::read(v, self.shape, rate)?; - self.verify_committed(v, commitment, clock, output) + self.verify_committed(v, &commitment, clock, output) } /// The verifier's core past the commitment's root: the bus and the tables, the flock reductions and the opening. @@ -80,7 +80,7 @@ impl Layout { pub(crate) fn verify_committed( &self, v: &mut V, - commitment: Commitment, + commitment: &Commitment, clock: V::E, output: &[V::E; 4], ) -> Result, CpuError> { diff --git a/crates/leanvm_core/src/cpu/zk.rs b/crates/leanvm_core/src/cpu/zk.rs index e9a5c2752..8aedac93f 100644 --- a/crates/leanvm_core/src/cpu/zk.rs +++ b/crates/leanvm_core/src/cpu/zk.rs @@ -175,7 +175,7 @@ where clock = rec.mul_const_add(b, F192::from(F64(1 << bit)), clock); } let output = output.words().map(|o| Sym::Pub(F192::from(F64(o)))); - let claims = layout.verify_committed(rec, commitment, clock, &output)?; + let claims = layout.verify_committed(rec, &commitment, clock, &output)?; program.check_deferred_hidden(rec, &claims)?; Ok((key_root, rate)) } From 62e98f3242a579e897dc8c8be4f1d4652f3095be Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sat, 10 Oct 2026 14:01:05 +0100 Subject: [PATCH 05/14] zk: refuse an outer proof with the transcript's error SpartanError had one variant, the transcript's error, which the caller unwrapped back into it. --- crates/leanvm_core/src/cpu/zk.rs | 4 ++-- crates/leanvm_core/src/zk/spartan.rs | 15 +++------------ 2 files changed, 5 insertions(+), 14 deletions(-) diff --git a/crates/leanvm_core/src/cpu/zk.rs b/crates/leanvm_core/src/cpu/zk.rs index 8aedac93f..9018ff053 100644 --- a/crates/leanvm_core/src/cpu/zk.rs +++ b/crates/leanvm_core/src/cpu/zk.rs @@ -21,7 +21,7 @@ use crate::tables::Clock; use crate::zk::keys::{self, KEY_MU, KeyStack, LANE, MAX_KEYS, MAX_OUTER_LOG_ROWS}; use crate::zk::outer::constraint_system; use crate::zk::randomness::{Purpose, Randomness, ZkRng}; -use crate::zk::spartan::{self, OuterClaims, SpartanError}; +use crate::zk::spartan::{self, OuterClaims}; use crate::zk::sym::{Form, Recorder, Sym, Var}; use ::pcs::verifier::OpeningVerifier; use ::pcs::whir::{self, Hiding, ProverData, WhirError, config_for_rate_hiding}; @@ -149,7 +149,7 @@ pub(super) fn verify(program: &Program, output: Output, proof: &Proof) -> Result max: MAX_OUTER_LOG_ROWS, }); } - let claims = spartan::verify(&mut vs, &r1cs).map_err(|SpartanError::Transcript(e)| CpuError::Transcript(e))?; + let claims = spartan::verify(&mut vs, &r1cs)?; verify_keys(&mut vs, key_root, &claims, rate.log_inv_rate().into()).map_err(CpuError::KeyOpen)?; vs.finish()?; Ok(vs.into_raw_proof()) diff --git a/crates/leanvm_core/src/zk/spartan.rs b/crates/leanvm_core/src/zk/spartan.rs index cb904176d..9ba6bc15b 100644 --- a/crates/leanvm_core/src/zk/spartan.rs +++ b/crates/leanvm_core/src/zk/spartan.rs @@ -20,7 +20,6 @@ use fiat_shamir::arith::{Arith, Native, Verifier}; use fiat_shamir::transcript::{TranscriptError, Transmitter}; use primitives::field::F192; use primitives::multilinear::{eq_table, interp}; -use thiserror::Error; /// What the outer proof leaves to the caller's commitment opening. #[derive(Clone, Debug, PartialEq, Eq)] @@ -33,14 +32,6 @@ pub(crate) struct OuterClaims { pub(crate) libra_target: E, } -/// Why the outer verifier refuses: it has no witness, so only a malformed stream. -#[derive(Clone, Debug, PartialEq, Eq, Error)] -pub(crate) enum SpartanError { - /// The proof stream is malformed. - #[error(transparent)] - Transcript(#[from] TranscriptError), -} - /// The Libra mask's coefficients over `log_rows` variables: `[g_c, g_00, g_01, g_10, g_11, ...]`. pub(crate) const fn libra_len(log_rows: usize) -> usize { 1 + 2 * log_rows @@ -121,8 +112,8 @@ fn prove_products(ps: &mut impl Transmitter, r1cs: &R1cs, products: [Vec; /// /// # Errors /// -/// Returns an error on a malformed stream. -pub(crate) fn verify(v: &mut V, r1cs: &R1cs) -> Result, SpartanError> { +/// Returns an error on a malformed stream: having no witness, the verifier refuses nothing else. +pub(crate) fn verify(v: &mut V, r1cs: &R1cs) -> Result, TranscriptError> { let log_rows = r1cs.log_rows(); let tau = v.sample_vec(log_rows); let s_g = v.next_scalar()?; @@ -265,7 +256,7 @@ mod tests { (claims, ps.into_proof()) } - fn check(r1cs: &R1cs, proof: &ProofTranscript) -> Result { + fn check(r1cs: &R1cs, proof: &ProofTranscript) -> Result { let mut v = VerifierState::from_label(LABEL, proof); let claims = verify(&mut v, r1cs)?; v.finish()?; From 07764b7cb14a958659c94330dcb77f5f07f3f7a4 Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sat, 10 Oct 2026 14:01:19 +0100 Subject: [PATCH 06/14] zk: drop references to a spec section that does not exist The specification has the hiding commitment (Annex B, sec:pcs-zk) but no sec:zk; the composition is described in the cpu::zk module docs. --- crates/fiat_shamir/src/arith.rs | 2 +- crates/fiat_shamir/src/transcript.rs | 2 +- crates/leanvm_core/src/cpu/deferred.rs | 2 +- crates/leanvm_core/src/cpu/proof.rs | 2 +- crates/leanvm_core/src/cpu/prover.rs | 2 +- crates/leanvm_core/src/cpu/zk.rs | 2 +- crates/leanvm_core/src/zk/keys.rs | 2 +- crates/leanvm_core/src/zk/mod.rs | 2 +- crates/leanvm_core/src/zk/outer.rs | 2 +- crates/leanvm_core/src/zk/sym.rs | 2 +- 10 files changed, 10 insertions(+), 10 deletions(-) diff --git a/crates/fiat_shamir/src/arith.rs b/crates/fiat_shamir/src/arith.rs index fcd38ed79..8e11be37d 100644 --- a/crates/fiat_shamir/src/arith.rs +++ b/crates/fiat_shamir/src/arith.rs @@ -239,7 +239,7 @@ pub trait Verifier: Arith { f(self) } - /// Whether the scalars read from now on travel under one-time-pad keys (doc `leanvm` §sec:zk). + /// Whether the scalars read from now on travel under one-time-pad keys. /// /// A verifier that holds values reads no padded proof, so by default this does nothing. fn set_hidden(&mut self, hidden: bool) { diff --git a/crates/fiat_shamir/src/transcript.rs b/crates/fiat_shamir/src/transcript.rs index eba573c1b..a1697e6ec 100644 --- a/crates/fiat_shamir/src/transcript.rs +++ b/crates/fiat_shamir/src/transcript.rs @@ -89,7 +89,7 @@ pub trait Transmitter: Challenger { fn add_scalars(&mut self, xs: &[F192]); fn grind(&mut self, bits: u32); - /// Whether the scalars sent from now on travel under one-time-pad keys (doc `leanvm` §sec:zk). + /// Whether the scalars sent from now on travel under one-time-pad keys. /// /// A prover holding no keys hides nothing. fn set_hidden(&mut self, hidden: bool); diff --git a/crates/leanvm_core/src/cpu/deferred.rs b/crates/leanvm_core/src/cpu/deferred.rs index 64b5a0dd1..819990121 100644 --- a/crates/leanvm_core/src/cpu/deferred.rs +++ b/crates/leanvm_core/src/cpu/deferred.rs @@ -234,7 +234,7 @@ impl Program { Ok(()) } - /// Settle the claims a zero-knowledge proof's core left, as constraints of the outer proof (doc `leanvm` §sec:zk). + /// Settle the claims a zero-knowledge proof's core left, as constraints of the outer proof. /// /// Every point is a challenge, so each claim's expected value is a public linear function of its hidden parts: the /// program claim's twist and image weight, each circuit claim's bit slices. diff --git a/crates/leanvm_core/src/cpu/proof.rs b/crates/leanvm_core/src/cpu/proof.rs index 1acf40bce..d631f5083 100644 --- a/crates/leanvm_core/src/cpu/proof.rs +++ b/crates/leanvm_core/src/cpu/proof.rs @@ -9,7 +9,7 @@ use std::fmt::{self, Debug, Formatter}; /// /// The program checks it against the output. /// -/// It travels as bytes. A zero-knowledge proof (doc `leanvm` §sec:zk) says the same and reveals nothing else of the run than its public shape. +/// It travels as bytes. A zero-knowledge proof says the same and reveals nothing else of the run than its public shape. #[derive(Clone, PartialEq, Eq)] pub struct Proof(#[doc(hidden)] pub ProofTranscript, pub(crate) bool); diff --git a/crates/leanvm_core/src/cpu/prover.rs b/crates/leanvm_core/src/cpu/prover.rs index 8792f610d..7d246ed8b 100644 --- a/crates/leanvm_core/src/cpu/prover.rs +++ b/crates/leanvm_core/src/cpu/prover.rs @@ -13,7 +13,7 @@ use tracing::info_span; /// /// # Zero knowledge /// -/// A zero-knowledge proof (doc `leanvm` §sec:zk) hides the advice and the run, but not the run's shape: each table's height and the rate are public. +/// A zero-knowledge proof hides the advice and the run, but not the run's shape: each table's height and the rate are public. /// A program whose advice is private must prove at a fixed public shape, so that its heights say nothing about the advice. /// /// # Performance diff --git a/crates/leanvm_core/src/cpu/zk.rs b/crates/leanvm_core/src/cpu/zk.rs index 9018ff053..d75e53138 100644 --- a/crates/leanvm_core/src/cpu/zk.rs +++ b/crates/leanvm_core/src/cpu/zk.rs @@ -1,4 +1,4 @@ -//! Zero-knowledge proofs of a run (doc `leanvm` §sec:zk): the plain proof under one-time pads on a hiding commitment, then an outer proof that the padded transcript passes the verifier's checks. +//! Zero-knowledge proofs of a run: the plain proof under one-time pads on a hiding commitment, then an outer proof that the padded transcript passes the verifier's checks. //! //! After the zero-knowledge seed, the transcript is: //! diff --git a/crates/leanvm_core/src/zk/keys.rs b/crates/leanvm_core/src/zk/keys.rs index ced539174..3814862a0 100644 --- a/crates/leanvm_core/src/zk/keys.rs +++ b/crates/leanvm_core/src/zk/keys.rs @@ -1,4 +1,4 @@ -//! The key commitment: every one-time-pad key, the outer proof's dummy operands and its mask, in one lane of its own stack, beside one lane of uniform words (doc `leanvm` §sec:zk). +//! The key commitment: every one-time-pad key, the outer proof's dummy operands and its mask, in one lane of its own stack, beside one lane of uniform words. //! //! Its shape is fixed, so neither side counts anything before committing: //! diff --git a/crates/leanvm_core/src/zk/mod.rs b/crates/leanvm_core/src/zk/mod.rs index 207e8071d..08e115ddb 100644 --- a/crates/leanvm_core/src/zk/mod.rs +++ b/crates/leanvm_core/src/zk/mod.rs @@ -1,4 +1,4 @@ -//! Zero knowledge (doc `leanvm` §sec:zk): the outer proof that a padded transcript passes the verifier's checks. +//! Zero knowledge: the outer proof that a padded transcript passes the verifier's checks. pub(crate) mod keys; pub(crate) mod outer; diff --git a/crates/leanvm_core/src/zk/outer.rs b/crates/leanvm_core/src/zk/outer.rs index 3b14c71a5..21da07608 100644 --- a/crates/leanvm_core/src/zk/outer.rs +++ b/crates/leanvm_core/src/zk/outer.rs @@ -1,4 +1,4 @@ -//! The outer constraint system: what the recording verifier recorded, over the key stack's slots (doc `leanvm` §sec:zk). +//! The outer constraint system: what the recording verifier recorded, over the key stack's slots. //! //! Column 0 is the constant one and column `1 + s` the key stack's slot `s`. A key is its slot; an auxiliary variable is //! the scalar the prover sent for it plus its own key, so every column is a slot and the assignment is the key stack. diff --git a/crates/leanvm_core/src/zk/sym.rs b/crates/leanvm_core/src/zk/sym.rs index c5c3d67e2..c6e6c33b5 100644 --- a/crates/leanvm_core/src/zk/sym.rs +++ b/crates/leanvm_core/src/zk/sym.rs @@ -1,4 +1,4 @@ -//! The verifier over a padded transcript: the native verifier's own code, its hidden values held as affine forms over the keys and its checks on them recorded as constraints (doc `leanvm` §sec:zk). +//! The verifier over a padded transcript: the native verifier's own code, its hidden values held as affine forms over the keys and its checks on them recorded as constraints. //! //! - A scalar read while the transcript is hidden is `c + k`: the value sent, plus the key that padded it (characteristic two). //! - A challenge, a root, a query and every public computation stay values, checked as the native verifier checks them. From b607c7fda523f03ad9c857526b62f48de7350666 Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sat, 10 Oct 2026 14:01:22 +0100 Subject: [PATCH 07/14] leanvm-cli: refuse --zk for benchmarks without claiming a tracked zero-knowledge case No tracked benchmark proves in zero knowledge. --- bins/leanvm/src/main.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/bins/leanvm/src/main.rs b/bins/leanvm/src/main.rs index 3c6ac5eb4..dc75312be 100644 --- a/bins/leanvm/src/main.rs +++ b/bins/leanvm/src/main.rs @@ -184,7 +184,7 @@ fn main() { let cli = Cli::parse(); if cli.zk && matches!(cli.command, Command::Aggregate { .. } | Command::Bench { .. }) { refuse(format_args!( - "--zk proves single runs: an aggregation tree does not verify zero-knowledge leaves, and the benchmark tracks its own zero-knowledge case" + "--zk proves single runs: no aggregation tree verifies a zero-knowledge leaf, and the tracked benchmarks are plain proofs" )); } let fixed_threads = match &cli.command { From 44a2fc946cea2bddb1d9231c677b8551539a7dbf Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sat, 10 Oct 2026 14:01:40 +0100 Subject: [PATCH 08/14] pcs: drop the test of a padded encode from a message held elsewhere Only the commitment pads an encode, always in place; its test checks every plan against direct evaluation. --- crates/pcs/src/ntt/additive_ntt_f64.rs | 35 -------------------------- 1 file changed, 35 deletions(-) diff --git a/crates/pcs/src/ntt/additive_ntt_f64.rs b/crates/pcs/src/ntt/additive_ntt_f64.rs index bf9e1620f..7226a843c 100644 --- a/crates/pcs/src/ntt/additive_ntt_f64.rs +++ b/crates/pcs/src/ntt/additive_ntt_f64.rs @@ -1730,41 +1730,6 @@ mod tests { } } - #[test] - fn a_padded_encode_is_the_same_from_a_message_held_elsewhere() { - // Invariant: the padding lands the same whichever pass first reads the message. - // - // (log_d, lanes, rate, k) in place held elsewhere - // (7, 7, 2, 5) replicate, then deep pass deep pass copying the message - // (9, 2048, 1, 13) gathered first pass gathered first pass - // (4, 8, 4, 1) replicate, no layer left replicate, no layer left - // - // The in-place encode is checked against direct evaluation by the hiding commitment's test. - let mut rng = Rng::new(0x9AD5); - for (log_d, lanes, log_inv_rate, k) in [(7usize, 7usize, 2usize, 5usize), (9, 2048, 1, 13), (4, 8, 4, 1)] { - let ntt = AdditiveNttF64::standard(log_d); - let msg_len = (lanes << log_d) >> log_inv_rate; - let msg: Vec = (0..msg_len).map(|_| F64(rng.next_u64())).collect(); - let pad: Vec = (0..k * lanes).map(|_| F64(rng.next_u64())).collect(); - - let mut in_place = vec![F64::ZERO; msg_len << log_inv_rate]; - in_place[..msg_len].copy_from_slice(&msg); - let pad = Some(Pad { - rows: &pad, - offset: F64(rng.next_u64()), - }); - ntt.encode_interleaved_in_place_with(&mut in_place, lanes, log_inv_rate, pad, &|_, _| {}); - - let mut elsewhere = vec![F64::ZERO; msg_len << log_inv_rate]; - let src = SendPtr(msg.as_ptr().cast_mut()); - ntt.transform(&mut elsewhere, lanes, log_inv_rate, Some(src), pad, None); - assert_eq!( - elsewhere, in_place, - "log_d={log_d}, lanes={lanes}, rate={log_inv_rate}, k={k}" - ); - } - } - /// Every lane of the codeword must be exactly the single-lane RS codeword of /// that lane's contiguous message block, which is what makes a commitment over /// `n_lanes` lanes equal to the `2^log_batch_size`-lane one with a zero tail. From 460550edb9e4e7574e4b4396d6b209455a3d7996 Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sat, 10 Oct 2026 14:02:02 +0100 Subject: [PATCH 09/14] fiat_shamir: drop ProverState::keys_used, which nothing calls --- crates/fiat_shamir/src/transcript.rs | 5 ----- 1 file changed, 5 deletions(-) diff --git a/crates/fiat_shamir/src/transcript.rs b/crates/fiat_shamir/src/transcript.rs index a1697e6ec..1e402dafb 100644 --- a/crates/fiat_shamir/src/transcript.rs +++ b/crates/fiat_shamir/src/transcript.rs @@ -207,11 +207,6 @@ impl ProverState { }); } - /// How many keys hidden scalars have used. - pub fn keys_used(&self) -> usize { - self.pad.as_ref().map_or(0, |p| p.next) - } - /// The proof so far, which a verifier replays from the same seed. pub fn snapshot(&self) -> ProofTranscript { ProofTranscript { From a89cf5713054e0f2d70ca2300420b54c88021ab3 Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sat, 10 Oct 2026 14:02:35 +0100 Subject: [PATCH 10/14] leanvm: one announced layout, hiding or not announced_hiding repeated announced around one step; a flag picks the stack instead, and the size check returns to upstream's form. --- crates/leanvm_core/src/cpu/layout.rs | 34 ++++++-------------- crates/leanvm_core/src/cpu/zk.rs | 2 +- crates/leanvm_core/src/rec/verifier/riscv.rs | 2 +- 3 files changed, 12 insertions(+), 26 deletions(-) diff --git a/crates/leanvm_core/src/cpu/layout.rs b/crates/leanvm_core/src/cpu/layout.rs index 3a0ad18e3..c29ff20cb 100644 --- a/crates/leanvm_core/src/cpu/layout.rs +++ b/crates/leanvm_core/src/cpu/layout.rs @@ -820,31 +820,26 @@ impl Announcement { /// /// Refuses heights whose stacked witness the commitment does not take. pub(super) fn layout(&self, p: &RiscvProgram) -> Result { - Layout::announced(p, self.taus) + Layout::announced(p, self.taus, false) } } impl Layout { - /// The layout a verifier rebuilds from announced heights, its final clock zero. + /// The layout a verifier rebuilds from announced heights, its final clock zero, in the stack a zero-knowledge proof + /// commits when `hiding`. /// /// # Errors /// /// Refuses a height outside its table's range, or heights whose stacked witness the commitment does not take. - pub(crate) fn announced(p: &RiscvProgram, taus: PerTable) -> Result { + pub(crate) fn announced(p: &RiscvProgram, taus: PerTable, hiding: bool) -> Result { Self::check_heights(&taus)?; + let layout = Self::new(p, taus, 0); + let layout = if hiding { layout.hiding() } else { layout }; // The caps bound each height alone; the stacked size they imply is checked here. - Self::new(p, taus, 0).checked() - } - - /// The layout a verifier rebuilds from a zero-knowledge proof's announced heights: the same columns, in the stack a - /// zero-knowledge proof commits. - /// - /// # Errors - /// - /// As [`Self::announced`]. - pub(crate) fn announced_hiding(p: &RiscvProgram, taus: PerTable) -> Result { - Self::check_heights(&taus)?; - Self::new(p, taus, 0).hiding().checked() + if !(crate::pcs::MIN_MU..=crate::pcs::MAX_MU).contains(&layout.shape.mu) { + return Err(CpuError::WitnessSize { mu: layout.shape.mu }); + } + Ok(layout) } /// The same columns, in the stack a zero-knowledge proof commits: lanes long enough to hide, then a random lane. @@ -853,15 +848,6 @@ impl Layout { Self { shape, ..self } } - /// The layout, if the commitment takes its stack. - fn checked(self) -> Result { - if (crate::pcs::MIN_MU..=crate::pcs::MAX_MU).contains(&self.shape.mu) { - Ok(self) - } else { - Err(CpuError::WitnessSize { mu: self.shape.mu }) - } - } - /// Check each table's height lies between flock's instance floor and the public cap. /// /// A table's rows are its class's runs, unbounded by the program's size, so it has a cap of its own. diff --git a/crates/leanvm_core/src/cpu/zk.rs b/crates/leanvm_core/src/cpu/zk.rs index d75e53138..2b788a16b 100644 --- a/crates/leanvm_core/src/cpu/zk.rs +++ b/crates/leanvm_core/src/cpu/zk.rs @@ -162,7 +162,7 @@ where T: OpeningVerifier, { let (taus, rate) = Announcement::read_shape(rec.transport())?; - let layout = Layout::announced_hiding(program.rv(), taus)?; + let layout = Layout::announced(program.rv(), taus, true)?; let commitment = Commitment::read(rec, layout.shape, rate)?; let key_root = rec.next_root()?; diff --git a/crates/leanvm_core/src/rec/verifier/riscv.rs b/crates/leanvm_core/src/rec/verifier/riscv.rs index 3c63087c3..c70d7465c 100644 --- a/crates/leanvm_core/src/rec/verifier/riscv.rs +++ b/crates/leanvm_core/src/rec/verifier/riscv.rs @@ -33,7 +33,7 @@ impl<'p> ProofShape<'p> { /// /// Refuses what the native verifier refuses of an announcement: a height out of range, or a witness the commitment does not take. pub fn new(program: &'p Program, taus: PerTable, rate: Rate) -> Result { - let layout = Layout::announced(program.rv(), taus)?; + let layout = Layout::announced(program.rv(), taus, false)?; Ok(Self { program, taus, From b4927809f64107b84835ef22b4b6a7b0d405c98a Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sat, 10 Oct 2026 14:03:01 +0100 Subject: [PATCH 11/14] leanvm: one padded commitment constructor new_hiding only asserted the random lane before new_padded, whose padding-length check already ties the pads to the stack's configuration. --- crates/leanvm_core/src/cpu/zk.rs | 2 +- crates/leanvm_core/src/pcs.rs | 20 +++++--------------- 2 files changed, 6 insertions(+), 16 deletions(-) diff --git a/crates/leanvm_core/src/cpu/zk.rs b/crates/leanvm_core/src/cpu/zk.rs index 2b788a16b..837415253 100644 --- a/crates/leanvm_core/src/cpu/zk.rs +++ b/crates/leanvm_core/src/cpu/zk.rs @@ -56,7 +56,7 @@ pub(super) fn prove(program: &Program, mut w: Witness, output: Output, rate: Rat rng.fill_k(Purpose::RandomLane, &mut w.q[shape.n_lanes * lane..]); let mut pads = vec![F64::ZERO; shape.committed_lanes() * pcs::padding(shape.mu, log_inv_rate)]; rng.fill_k(Purpose::Pads, &mut pads); - Committed::new_hiding(&mut ps, &w.q, shape, rate, &pads).expect("the witness matches its layout") + Committed::new_padded(&mut ps, &w.q, shape, rate, &pads).expect("the witness matches its layout") }); let stack = KeyStack::draw(&rng); let key_data = info_span!("Commit keys").in_scope(|| { diff --git a/crates/leanvm_core/src/pcs.rs b/crates/leanvm_core/src/pcs.rs index 90442dd38..d93b69ec5 100644 --- a/crates/leanvm_core/src/pcs.rs +++ b/crates/leanvm_core/src/pcs.rs @@ -148,8 +148,9 @@ impl Committed { Self::new_padded(ps, witness, shape, rate, &[]) } - /// Commits a zero-knowledge proof's stack: its lanes padded past their power of two with `pads`, [`padding`] uniform - /// words per committed lane, its last lane uniform (doc `leanvm` Annex B, the hiding commitment). + /// [`Self::new`] with each committed lane padded past its power of two by `pads`: the hiding commitment of doc `leanvm` Annex B. + /// + /// A zero-knowledge proof's stack, whose last lane is random, takes [`padding`] uniform words per committed lane, any other stack none. /// /// # Errors /// @@ -157,19 +158,8 @@ impl Committed { /// /// # Panics /// - /// Panics unless the shape has a random lane and `pads` is the padding of every committed lane. - pub(crate) fn new_hiding( - ps: &mut ProverState, - witness: &[F64], - shape: StackShape, - rate: Rate, - pads: &[F64], - ) -> Result { - assert!(shape.random_lane, "a hiding commitment's last lane is random"); - Self::new_padded(ps, witness, shape, rate, pads) - } - - fn new_padded( + /// Panics unless `pads` is the padding of every committed lane. + pub(crate) fn new_padded( ps: &mut ProverState, witness: &[F64], shape: StackShape, From f7962b4057d8fe22d8cfba0589a5d763d7fffc29 Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sat, 10 Oct 2026 14:04:01 +0100 Subject: [PATCH 12/14] zk: write the announced shape once, and unwrap hard-wrapped docs Announcement::write writes the shape through write_shape, then the final clock: the same scalars in the same order. The docs the zero-knowledge work added wrapped prose by hand, which the repository does not. --- crates/fiat_shamir/src/arith.rs | 3 +-- crates/fiat_shamir/src/transcript.rs | 3 +-- crates/flock/src/lincheck.rs | 3 +-- crates/leanvm_core/src/cpu/deferred.rs | 3 +-- crates/leanvm_core/src/cpu/layout.rs | 10 +++------- crates/leanvm_core/src/cpu/program.rs | 6 ++---- crates/leanvm_core/src/cpu/zk.rs | 3 +-- crates/leanvm_core/src/leaf/decompose.rs | 3 +-- crates/leanvm_core/src/witness.rs | 3 +-- crates/leanvm_core/src/zk/outer.rs | 6 ++---- crates/leanvm_core/src/zk/r1cs.rs | 3 +-- crates/leanvm_core/src/zk/spartan.rs | 13 ++++--------- crates/leanvm_core/src/zk/sym.rs | 3 +-- 13 files changed, 20 insertions(+), 42 deletions(-) diff --git a/crates/fiat_shamir/src/arith.rs b/crates/fiat_shamir/src/arith.rs index 8e11be37d..f6f281ff3 100644 --- a/crates/fiat_shamir/src/arith.rs +++ b/crates/fiat_shamir/src/arith.rs @@ -34,8 +34,7 @@ pub trait Arith { /// The same element, which the caller reuses many times. /// - /// A recording arithmetic may give it a variable of its own, so that what reuses it stays short; by default it is - /// returned as it is. + /// A recording arithmetic may give it a variable of its own, so that what reuses it stays short; by default it is returned as it is. fn bind(&mut self, a: Self::E) -> Self::E { a } diff --git a/crates/fiat_shamir/src/transcript.rs b/crates/fiat_shamir/src/transcript.rs index 1e402dafb..2d2cda243 100644 --- a/crates/fiat_shamir/src/transcript.rs +++ b/crates/fiat_shamir/src/transcript.rs @@ -192,8 +192,7 @@ impl ProverState { } } - /// Hide each scalar sent while [`Transmitter::set_hidden`] holds under the next of these keys: the stream and the - /// transcript carry `x + key`. + /// Hide each scalar sent while [`Transmitter::set_hidden`] holds under the next of these keys: the stream and the transcript carry `x + key`. /// /// # Panics /// diff --git a/crates/flock/src/lincheck.rs b/crates/flock/src/lincheck.rs index 59f0139f9..35800f959 100644 --- a/crates/flock/src/lincheck.rs +++ b/crates/flock/src/lincheck.rs @@ -588,8 +588,7 @@ impl MatrixForm { .unwrap_or_else(|| inner_product(&circuit.fold_alpha_batched(self.alpha, &eq_inner), &w_col)) } - /// The form's weight on each bit slice: [`Self::evaluate`] is `sum_i s_hat_v[i] weights[i]`, the form being linear - /// in its slices, and the weights depend on its other, public, coordinates alone. + /// The form's weight on each bit slice: [`Self::evaluate`] is `sum_i s_hat_v[i] weights[i]`, the form being linear in its slices, and the weights depend on its other, public, coordinates alone. pub fn slice_weights(&self, circuit: &dyn LincheckCircuit) -> Vec { let n_slices = self.s_hat_v.len(); let eq_inner = build_quirky_eq_table(self.z_skip, &self.x_inner_rest, n_slices.ilog2() as usize); diff --git a/crates/leanvm_core/src/cpu/deferred.rs b/crates/leanvm_core/src/cpu/deferred.rs index 819990121..ada9e73bf 100644 --- a/crates/leanvm_core/src/cpu/deferred.rs +++ b/crates/leanvm_core/src/cpu/deferred.rs @@ -236,8 +236,7 @@ impl Program { /// Settle the claims a zero-knowledge proof's core left, as constraints of the outer proof. /// - /// Every point is a challenge, so each claim's expected value is a public linear function of its hidden parts: the - /// program claim's twist and image weight, each circuit claim's bit slices. + /// Every point is a challenge, so each claim's expected value is a public linear function of its hidden parts: the program claim's twist and image weight, each circuit claim's bit slices. /// /// # Errors /// diff --git a/crates/leanvm_core/src/cpu/layout.rs b/crates/leanvm_core/src/cpu/layout.rs index c29ff20cb..870d38771 100644 --- a/crates/leanvm_core/src/cpu/layout.rs +++ b/crates/leanvm_core/src/cpu/layout.rs @@ -723,9 +723,7 @@ impl Announcement { /// Write the announcement onto the scalar stream, which binds it into the transcript. pub(super) fn write(&self, ps: &mut ProverState) { - for size in Self::sizes(&self.taus, self.rate) { - ps.add_scalar(size); - } + Self::write_shape(&self.taus, self.rate, ps); ps.add_scalar(F192::new(self.ts_final, 0, 0)); } @@ -767,8 +765,7 @@ impl Announcement { }) } - /// Write a zero-knowledge proof's announcement: its shape alone, each table's height then the rate, its final clock - /// being hidden. + /// Write a zero-knowledge proof's announcement: its shape alone, each table's height then the rate, its final clock being hidden. pub(crate) fn write_shape(taus: &PerTable, rate: Rate, ps: &mut ProverState) { for size in Self::sizes(taus, rate) { ps.add_scalar(size); @@ -825,8 +822,7 @@ impl Announcement { } impl Layout { - /// The layout a verifier rebuilds from announced heights, its final clock zero, in the stack a zero-knowledge proof - /// commits when `hiding`. + /// The layout a verifier rebuilds from announced heights, its final clock zero, in the stack a zero-knowledge proof commits when `hiding`. /// /// # Errors /// diff --git a/crates/leanvm_core/src/cpu/program.rs b/crates/leanvm_core/src/cpu/program.rs index 935f73655..299e53713 100644 --- a/crates/leanvm_core/src/cpu/program.rs +++ b/crates/leanvm_core/src/cpu/program.rs @@ -254,8 +254,7 @@ impl Program { Proof(ps.into_proof(), false) } - /// The bus, the table sumcheck and flock's reductions over the committed witness: the opening's point claims and its - /// ring-switched regions. + /// The bus, the table sumcheck and flock's reductions over the committed witness: the opening's point claims and its ring-switched regions. pub(super) fn prove_reductions( &self, ps: &mut ProverState, @@ -378,8 +377,7 @@ impl Program { /// /// # Errors /// - /// Returns the first stage that refuses the proof, and refuses a zero-knowledge proof, whose claims are settled - /// inside its outer proof. + /// Returns the first stage that refuses the proof, and refuses a zero-knowledge proof, whose claims are settled inside its outer proof. #[doc(hidden)] pub fn verify_core(&self, output: Output, proof: &Proof) -> Result { self.replay(output, proof).map(|(claims, _)| claims) diff --git a/crates/leanvm_core/src/cpu/zk.rs b/crates/leanvm_core/src/cpu/zk.rs index 837415253..3ed59584f 100644 --- a/crates/leanvm_core/src/cpu/zk.rs +++ b/crates/leanvm_core/src/cpu/zk.rs @@ -155,8 +155,7 @@ pub(super) fn verify(program: &Program, output: Output, proof: &Proof) -> Result Ok(vs.into_raw_proof()) } -/// The plain verifier over a padded transcript, recorded: the shape, the two roots, the final clock's bits, the core, -/// then the deferred claims. It returns the key commitment's root and the rate. +/// The plain verifier over a padded transcript, recorded: the shape, the two roots, the final clock's bits, the core, then the deferred claims. It returns the key commitment's root and the rate. fn record(program: &Program, rec: &mut Recorder, output: Output) -> Result<(Hash, Rate), CpuError> where T: OpeningVerifier, diff --git a/crates/leanvm_core/src/leaf/decompose.rs b/crates/leanvm_core/src/leaf/decompose.rs index e96fbd780..316beb4a3 100644 --- a/crates/leanvm_core/src/leaf/decompose.rs +++ b/crates/leanvm_core/src/leaf/decompose.rs @@ -77,8 +77,7 @@ pub(crate) fn producer_public_twist(coords: &[Coord], w: &[F192], chi: &[F192], .fold(F192::ZERO, |acc, (&d, &mu)| acc + mu * d) } -/// The program columns' share of a producer's public half at `chi`, for each of `n_bits` twist weights: the `D_i` of -/// [`producer_public_twist`]. +/// The program columns' share of a producer's public half at `chi`, for each of `n_bits` twist weights: the `D_i` of [`producer_public_twist`]. pub(crate) fn producer_twist_terms(coords: &[Coord], w: &[F192], chi: &[F192], n_bits: usize) -> Vec { let eq = primitives::multilinear::eq_table(chi); let mut terms = vec![F192::ZERO; n_bits]; diff --git a/crates/leanvm_core/src/witness.rs b/crates/leanvm_core/src/witness.rs index 661102590..6ad655d1e 100644 --- a/crates/leanvm_core/src/witness.rs +++ b/crates/leanvm_core/src/witness.rs @@ -123,8 +123,7 @@ impl StackShape { self.committed_lanes() << (self.mu - crate::pcs::LOG_BATCH) } - /// The shape a zero-knowledge proof commits for `placed` words: its lanes long enough for one random lane to hide - /// the opening ([`::pcs::whir::config::MIN_LOG_N_HIDING`]), and room for that lane. + /// The shape a zero-knowledge proof commits for `placed` words: its lanes long enough for one random lane to hide the opening ([`::pcs::whir::config::MIN_LOG_N_HIDING`]), and room for that lane. pub fn hiding(placed: usize) -> Self { let mut mu = crate::log2_ceil_usize(placed.max(1)) .max(crate::pcs::MIN_MU) diff --git a/crates/leanvm_core/src/zk/outer.rs b/crates/leanvm_core/src/zk/outer.rs index 21da07608..3ffe580c3 100644 --- a/crates/leanvm_core/src/zk/outer.rs +++ b/crates/leanvm_core/src/zk/outer.rs @@ -1,7 +1,6 @@ //! The outer constraint system: what the recording verifier recorded, over the key stack's slots. //! -//! Column 0 is the constant one and column `1 + s` the key stack's slot `s`. A key is its slot; an auxiliary variable is -//! the scalar the prover sent for it plus its own key, so every column is a slot and the assignment is the key stack. +//! Column 0 is the constant one and column `1 + s` the key stack's slot `s`. A key is its slot; an auxiliary variable is the scalar the prover sent for it plus its own key, so every column is a slot and the assignment is the key stack. //! //! Its rows, in order: //! @@ -17,8 +16,7 @@ use super::r1cs::{R1cs, Row as SparseRow}; use super::sym::{Form, Kind, Record, Var}; use primitives::field::F192; -/// The constraint system the record states, the auxiliary variable of rank `r` (by digest) being the form `sent[r]`: the -/// scalar sent for it plus its key. +/// The constraint system the record states, the auxiliary variable of rank `r` (by digest) being the form `sent[r]`: the scalar sent for it plus its key. pub(crate) fn constraint_system(record: &Record, sent: &[Form]) -> R1cs { let order = record.aux_order(); assert_eq!(sent.len(), order.len(), "a sent scalar per auxiliary variable"); diff --git a/crates/leanvm_core/src/zk/r1cs.rs b/crates/leanvm_core/src/zk/r1cs.rs index 1361fdbf5..648c2ed71 100644 --- a/crates/leanvm_core/src/zk/r1cs.rs +++ b/crates/leanvm_core/src/zk/r1cs.rs @@ -61,8 +61,7 @@ impl R1cs { /// Append the two dummy constraints `z[first]·z[first+1] = z[first+2]` and `z[first+3]·z[first+4] = z[first+5]`. /// - /// Their operands are fresh and uniform ([`dummy_values`]), which is what hides the final `(a, b, c)` of the outer - /// Spartan: each sits at a row of its own, so it adds a uniform term to each of the three evaluations. + /// Their operands are fresh and uniform ([`dummy_values`]), which is what hides the final `(a, b, c)` of the outer Spartan: each sits at a row of its own, so it adds a uniform term to each of the three evaluations. pub(crate) fn push_dummies(&mut self, first: usize) { assert!( first > 0 && first + N_DUMMIES <= self.n_cols, diff --git a/crates/leanvm_core/src/zk/spartan.rs b/crates/leanvm_core/src/zk/spartan.rs index 9ba6bc15b..08bf5f228 100644 --- a/crates/leanvm_core/src/zk/spartan.rs +++ b/crates/leanvm_core/src/zk/spartan.rs @@ -1,17 +1,13 @@ //! The outer zero-knowledge Spartan over `E`. //! -//! It proves `sum_x eq(τ, x)·F(x) = 0` for `F = ÷B̃ + C̃`, the row products of an [`R1cs`] over a witness the caller -//! commits elsewhere, and ends in two linear claims the caller discharges with its own opening: one on the witness, -//! one on the Libra mask `g(X) = g_c + sum_j (g_{j0} + g_{j1} X_j) X_j`, which the caller commits too. +//! It proves `sum_x eq(τ, x)·F(x) = 0` for `F = ÷B̃ + C̃`, the row products of an [`R1cs`] over a witness the caller commits elsewhere, and ends in two linear claims the caller discharges with its own opening: one on the witness, one on the Libra mask `g(X) = g_c + sum_j (g_{j0} + g_{j1} X_j) X_j`, which the caller commits too. //! //! The rows form the cube `{0,1}^ℓ`, `x = sum_i x_i 2^i`, variable 0 bound first. //! //! Zero knowledge needs no padding: -//! - each round's `c_1` and `c_2` are those of `F` plus `α` times the mask's fresh `(g_{i0}, g_{i1})`, the eq-weighted -//! MLE-check mask of the Binius64 whitepaper; +//! - each round's `c_1` and `c_2` are those of `F` plus `α` times the mask's fresh `(g_{i0}, g_{i1})`, the eq-weighted MLE-check mask of the Binius64 whitepaper; //! - the mask's sum `s_g` is hidden by `g_c`; -//! - the final `(a, b, c)` are hidden by the two dummy constraints ([`R1cs::push_dummies`]), whose fresh operands sit at -//! rows of their own. +//! - the final `(a, b, c)` are hidden by the two dummy constraints ([`R1cs::push_dummies`]), whose fresh operands sit at rows of their own. //! //! The characteristic-2 argument rests on the Binius64 whitepaper's MLE-check theorem and is unreviewed. @@ -153,8 +149,7 @@ fn libra_weight(ar: &mut A, r: &[A::E]) -> Vec { /// The two claims, from `(a, b, c)` and `eq(r, x)` for the first `n_rows` rows `x` at least. /// -/// `t_y = sum_x eq(r, x)(A[x][y] + γ B[x][y] + γ^2 C[x][y])` gives `⟨t, z⟩ = a + γ b + γ^2 c`, and `z_0 = 1` moves `t_0` -/// to the target. +/// `t_y = sum_x eq(r, x)(A[x][y] + γ B[x][y] + γ^2 C[x][y])` gives `⟨t, z⟩ = a + γ b + γ^2 c`, and `z_0 = 1` moves `t_0` to the target. fn claims( ar: &mut A, r1cs: &R1cs, diff --git a/crates/leanvm_core/src/zk/sym.rs b/crates/leanvm_core/src/zk/sym.rs index c6e6c33b5..29d504100 100644 --- a/crates/leanvm_core/src/zk/sym.rs +++ b/crates/leanvm_core/src/zk/sym.rs @@ -114,8 +114,7 @@ impl Record { terms } - /// BLAKE2s over a form: its constant, then each term in canonical order, a key as `0, index` and an auxiliary - /// variable as `1, digest`, each with its coefficient. An element of `E` is its three limbs, little-endian. + /// BLAKE2s over a form: its constant, then each term in canonical order, a key as `0, index` and an auxiliary variable as `1, digest`, each with its coefficient. An element of `E` is its three limbs, little-endian. pub(crate) fn digest(&self, f: &Form) -> [u8; 32] { let mut h = Hasher::new(); absorb_e(&mut h, f.constant); From 0f4bdfda7122e4da7e96fbe0dec4d6b559f26c1f Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sat, 10 Oct 2026 14:11:43 +0100 Subject: [PATCH 13/14] zk: read the outer sumcheck's pairs as arrays Clippy 1.99 refuses chunks_exact with a constant size. --- crates/leanvm_core/src/zk/spartan.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/leanvm_core/src/zk/spartan.rs b/crates/leanvm_core/src/zk/spartan.rs index 08bf5f228..6054f0bc0 100644 --- a/crates/leanvm_core/src/zk/spartan.rs +++ b/crates/leanvm_core/src/zk/spartan.rs @@ -69,7 +69,7 @@ fn prove_products(ps: &mut impl Transmitter, r1cs: &R1cs, products: [Vec; suffix += tau[i] * (g0 + g1); let eq = eq_table(&tau[i + 1..]); let mut coeffs = [F192::ZERO; 3]; - let pairs = (az.chunks_exact(2).zip(bz.chunks_exact(2))).zip(cz.chunks_exact(2)); + let pairs = (az.as_chunks::<2>().0.iter().zip(bz.as_chunks::<2>().0)).zip(cz.as_chunks::<2>().0); for (((a, b), c), &e) in pairs.zip(&eq) { let (da, db) = (a[0] + a[1], b[0] + b[1]); coeffs[0] += e * (a[0] * b[0] + c[0]); From f0322a94001abf1bd4358d319159295f0abe4461 Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sat, 10 Oct 2026 14:27:39 +0100 Subject: [PATCH 14/14] pcs: link the hiding commitment's docs to nothing test-only Rustdoc refused links to the plain commit, which is test-only now. --- crates/pcs/src/whir/commit.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/crates/pcs/src/whir/commit.rs b/crates/pcs/src/whir/commit.rs index 623925d91..e06a110ae 100644 --- a/crates/pcs/src/whir/commit.rs +++ b/crates/pcs/src/whir/commit.rs @@ -67,16 +67,16 @@ pub(crate) fn commit(message: &[F64], log_n: usize, log_batch_size: usize, log_i commit_hiding(message, log_n, log_batch_size, log_inv_rate, &[]) } -/// [`commit`] with each lane padded past its power of two: the hiding commitment. +/// The L0 commitment with each lane padded past its power of two: the hiding commitment. /// /// With `m = log_n - log_batch_size`, `r = log_inv_rate` and `k = pads.len() / n_lanes`, lane block `u` encodes `P_u(X) + W_m(X + s) R_u(X)`: `P_u` its `2^m` words as novel-basis coefficients, `R_u` its padding `pads[u k..(u + 1) k]`, and `s = F64(2^(m + r))`. /// Since `W_m(X + s) = W_m(X) + W_m(s)` and `X_{2^m + j} = W_m X_j`, that is `2^m + k` coefficients, so the codeword stays on the same `2^(m + r)` points, and the encode is the one butterfly layer more that pairs the message with the padding (`AdditiveNttF64::encode_interleaved_in_place_with`). /// The shift by `s` keeps the factor nonzero on the whole domain, where `W_m` alone vanishes on its first `2^m` points: any `k` symbols of a lane are then uniform, whatever its message. -/// Empty `pads` is [`commit`]. +/// Empty `pads` is the plain commitment. /// /// # Panics /// -/// Panics as [`commit`] does, or unless the padding is `k <= 2^m` coefficients for every lane. +/// Panics as the plain commitment does, or unless the padding is `k <= 2^m` coefficients for every lane. pub fn commit_hiding( message: &[F64], log_n: usize,