From adb11744dad7f27428a4a4141547c17f554daa02 Mon Sep 17 00:00:00 2001 From: Thomas Coratger Date: Mon, 12 Oct 2026 00:15:43 +0100 Subject: [PATCH] leanvm: zero-knowledge leaf proofs Prover::zero_knowledge(randomness) makes proofs that reveal nothing of the advice or the run beyond the run's shape: each table's height and the rate. - ProofKind (Plain, ZeroKnowledge) is the one notion every layer takes: the witness's layout, the size check, the verifier's layout, the envelope (LVMZ for zero knowledge, so a proof of one kind is refused as the other) and the session. - A zero-knowledge layout is the hiding stack (data lanes, zero lanes, the random group, every lane padded) and grinds L0_LIST_BITS more before the bus: the key commitment is a second list every challenge before the openings is unioned over. - The final clock's free bits, the bus, the tables, flock's reductions and the opening's lane rounds travel under one-time-pad keys; the opening then reveals its claim and the rest is in the clear. - The verifier runs its own core over the padded transcript through the zk crate's recorder (Layout::record_core); each free clock bit is recorded as a bit, so a failed row's bit 41 has no place in it. - Deferred claims: the prover sends what they need of the public polynomials (each bytecode term, RAM's image, each circuit's slice weights); DeferredClaims::into_plain records each hidden claim as a linear constraint on them and batches them by one challenge into claims of the plain shape, which check_deferred settles as a plain proof's. So the core of either kind leaves the same claims, which recursion carries out alike. - The outer proof shows the keys satisfy the record, discharged by the key commitment's opening. - Program::prove_execution takes the Prover whose rate and randomness it proves with; verify, verify_core and verify_recording take either kind of proof. Aggregation trees still refuse zero-knowledge leaves, and the CLI's --zk is for single runs. Tests: an honest proof verifies, round-trips its bytes, is refused under another output or as a plain proof, and is a function of its seed; tampered bytes across the proof are refused without panic; a forged run whose final clock carries the failure bit is refused by the outer proof. Cost on leanXMSS-100 (Apple M1 Pro, 16 threads): proving 0.27 s plain, 0.29 to 0.32 s zero knowledge; proof 296 KiB to 485 KiB; verifying 3.8 ms to 7.5 ms. Every full-size workload proves and verifies in zero knowledge. Co-Authored-By: Kevaundray Wedderburn Co-Authored-By: Claude Opus 5.5 --- Cargo.lock | 2 + bench-mobile/Cargo.lock | 53 +++ bins/leanvm/src/main.rs | 16 +- crates/flock/src/lincheck.rs | 38 ++ crates/leanvm_core/Cargo.toml | 2 + crates/leanvm_core/src/cpu/error.rs | 4 + crates/leanvm_core/src/cpu/layout.rs | 121 +++-- crates/leanvm_core/src/cpu/mod.rs | 2 + crates/leanvm_core/src/cpu/program.rs | 140 ++++-- crates/leanvm_core/src/cpu/proof.rs | 46 +- crates/leanvm_core/src/cpu/prover.rs | 51 +- crates/leanvm_core/src/cpu/reduce.rs | 17 +- crates/leanvm_core/src/cpu/witness.rs | 9 +- crates/leanvm_core/src/cpu/zero_knowledge.rs | 467 +++++++++++++++++++ crates/leanvm_core/src/envelope.rs | 5 + crates/leanvm_core/src/leaf/coord.rs | 3 + crates/leanvm_core/src/leaf/decompose.rs | 14 +- crates/leanvm_core/src/leaf/mod.rs | 2 +- crates/leanvm_core/src/lib.rs | 10 + crates/leanvm_core/src/pcs.rs | 89 +++- crates/leanvm_core/src/rec/tree/mod.rs | 5 + crates/leanvm_core/src/rec/verifier/riscv.rs | 4 +- crates/leanvm_core/src/rec/verifier/tests.rs | 12 +- crates/leanvm_core/src/witness.rs | 47 +- 24 files changed, 1036 insertions(+), 123 deletions(-) create mode 100644 crates/leanvm_core/src/cpu/zero_knowledge.rs diff --git a/Cargo.lock b/Cargo.lock index fb766cf4e..e98d76643 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1470,8 +1470,10 @@ dependencies = [ "pcs", "primitives", "proptest", + "rand_core 0.9.5", "thiserror", "tracing", + "zk", ] [[package]] diff --git a/bench-mobile/Cargo.lock b/bench-mobile/Cargo.lock index b9f837da2..158c77c04 100644 --- a/bench-mobile/Cargo.lock +++ b/bench-mobile/Cargo.lock @@ -153,8 +153,10 @@ dependencies = [ "parallel", "pcs", "primitives", + "rand_core 0.9.5", "thiserror 2.0.21", "tracing", + "zk", ] [[package]] @@ -242,6 +244,15 @@ version = "0.2.17" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a89322df9ebe1c1578d689c92318e070967d1042b512afbe49518723f4e6d5cd" +[[package]] +name = "ppv-lite86" +version = "0.2.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "85eae3c4ed2f50dcfe72643da4befc30deadb458a9b590d720cde2f2b1e97da9" +dependencies = [ + "zerocopy", +] + [[package]] name = "primitives" version = "0.1.0" @@ -274,6 +285,16 @@ version = "5.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "69cdb34c158ceb288df11e18b4bd39de994f6657d83847bdffdbd7f346754b0f" +[[package]] +name = "rand_chacha" +version = "0.9.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d3022b5f1df60f26e1ffddd6c66e8aa15de382ae63b3a0c1bfc0e4d3e3f325cb" +dependencies = [ + "ppv-lite86", + "rand_core 0.9.5", +] + [[package]] name = "rand_core" version = "0.6.4" @@ -614,6 +635,26 @@ version = "0.57.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1ebf944e87a7c253233ad6766e082e3cd714b5d03812acc24c318f549614536e" +[[package]] +name = "zerocopy" +version = "0.8.62" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "86502bf56ac7c77571a32e2647bb2a15894565e981fb2a48d7bde2d91c965a9d" +dependencies = [ + "zerocopy-derive", +] + +[[package]] +name = "zerocopy-derive" +version = "0.8.62" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5457206954b06561e2608c7e19cf58b1926586d999c246eebe4502f7e2039d1a" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.119", +] + [[package]] name = "zeroize" version = "1.9.1" @@ -634,6 +675,18 @@ dependencies = [ "syn 2.0.119", ] +[[package]] +name = "zk" +version = "0.1.0" +dependencies = [ + "fiat_shamir", + "pcs", + "primitives", + "rand_chacha", + "rand_core 0.9.5", + "thiserror 2.0.21", +] + [[package]] name = "zmij" version = "1.0.23" diff --git a/bins/leanvm/src/main.rs b/bins/leanvm/src/main.rs index c356e5329..2d445b3a8 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::{NonZeroUsize, ParseIntError}; @@ -37,6 +37,10 @@ struct Cli { #[arg(long, global = true)] tracing: bool, + /// Make zero-knowledge proofs, each from fresh randomness of the operating system. + #[arg(long, global = true)] + zk: bool, + /// Measured proving passes after warmup. #[arg( long, @@ -196,7 +200,17 @@ fn main() { topology.efficiency ); } + if cli.zk && matches!(cli.command, Command::Aggregate { .. } | Command::Bench { .. }) { + refuse(format_args!( + "--zk proves single runs: no aggregation tree verifies a zero-knowledge leaf yet, and the tracked benchmarks are plain proofs" + )); + } let prover = Prover::new(cli.rate); + let prover = if cli.zk { + prover.zero_knowledge(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/crates/flock/src/lincheck.rs b/crates/flock/src/lincheck.rs index 3e13d3906..9baee7523 100644 --- a/crates/flock/src/lincheck.rs +++ b/crates/flock/src/lincheck.rs @@ -587,6 +587,21 @@ 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, so that its value is `sum_i s_hat_v[i] * weights[i]`. + /// + /// The form is linear in its slices, and the weights depend on its other coordinates alone. + #[must_use] + 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); + // Column j * n_slices + i takes eq_rest[j] times slice i. + (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. @@ -1352,6 +1367,29 @@ mod tests { } } + #[test] + fn a_form_is_its_slices_against_their_weights() { + // Invariant: the form is linear in its slices, with weights fixed by its other coordinates. + // + // evaluate(form) = sum_i s_hat_v[i] * slice_weights(form)[i] + // + // Fixture state, (k_log, k_skip): no skip, a partial skip, the whole instance skipped. + for (k_log, k_skip) in [(6, 0), (6, 3), (7, 4), (6, 6)] { + let mut rng = Rng::new(88 + (k_log * 10 + k_skip) as u64); + let f = Fixture::new(10, k_log, k_skip, 3, &mut rng); + let form = MatrixForm { + alpha: rng.ext(), + z_skip: rng.ext(), + x_inner_rest: rng.ext_vec(k_log - k_skip), + r_inner_rest: rng.ext_vec(k_log - k_skip), + s_hat_v: rng.ext_vec(1 << k_skip), + }; + let weights = form.slice_weights(&f.circuit); + let linear = (form.s_hat_v.iter().zip(&weights)).fold(F192::ZERO, |acc, (&s, &w)| acc + s * w); + assert_eq!(form.evaluate(&f.circuit), linear, "k_log={k_log}, k_skip={k_skip}"); + } + } + #[test] fn a_moved_slice_misses_the_terminal_identity() { // Invariant: every slice the sumcheck weights is pinned; moving one refuses the proof. diff --git a/crates/leanvm_core/Cargo.toml b/crates/leanvm_core/Cargo.toml index eed0ad904..c22e0a0ec 100644 --- a/crates/leanvm_core/Cargo.toml +++ b/crates/leanvm_core/Cargo.toml @@ -16,6 +16,8 @@ pcs.workspace = true flock.workspace = true tracing.workspace = true thiserror.workspace = true +zk.workspace = true +rand_core.workspace = true [dev-dependencies] proptest.workspace = true diff --git a/crates/leanvm_core/src/cpu/error.rs b/crates/leanvm_core/src/cpu/error.rs index bc80882b9..a105a06f7 100644 --- a/crates/leanvm_core/src/cpu/error.rs +++ b/crates/leanvm_core/src/cpu/error.rs @@ -11,6 +11,7 @@ use fiat_shamir::TranscriptError; use flock::FlockError; use pcs::whir::WhirError; use thiserror::Error; +use zk::OuterError; /// Why a run has no proof. /// @@ -95,6 +96,9 @@ 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 outer proof is refused. + #[error("the outer proof: {0}")] + Outer(OuterError), } /// 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 e51a6e518..7b6460df2 100644 --- a/crates/leanvm_core/src/cpu/layout.rs +++ b/crates/leanvm_core/src/cpu/layout.rs @@ -8,6 +8,7 @@ use super::error::CpuError; use super::execute::Trace; +use super::proof::ProofKind; use super::{MAX_LOG_ROWS, UNGROUND_LOG_BYTECODE}; use crate::class_flock::FlockId; use crate::constraints::{BitColumns, Claims}; @@ -723,34 +724,45 @@ impl Announcement { /// Send the announcement, which binds it into the transcript. pub(super) fn write(&self, ps: &mut ProverState) { - for size in Self::sizes(&self.taus, self.rate) { - ps.prover_message(&size); - } + Self::write_shape(&self.taus, self.rate, ps); ps.prover_message(&F192::new(self.ts_final, 0, 0)); } - /// Read an announcement off the proof, binding it, and check every value is in range. + /// Send a zero-knowledge proof's announcement: each table's height, then the rate. /// - /// The checks run before any reduction, so an out-of-range announcement costs nothing. + /// Its final clock is not announced: it is hidden. + pub(super) fn write_shape(taus: &PerTable, rate: Rate, ps: &mut ProverState) { + for size in Self::sizes(taus, rate) { + ps.prover_message(&size); + } + } + + /// Read a zero-knowledge proof's announcement, checking it as a full one is checked. /// /// # Errors /// - /// Refuses a short stream, then what decoding refuses. - pub(super) fn read(vs: &mut impl Verifier) -> Result { - let mut scalars = [F192::ZERO; Self::LEN]; + /// Refuses a short stream, a non-canonical size, a table height or a rate outside its range. + pub(super) fn read_shape(vs: &mut impl Verifier) -> Result<(PerTable, Rate), CpuError> { + let mut scalars = [F192::ZERO; N_TABLES + 1]; for x in &mut scalars { *x = vs.prover_message()?; } - Self::decode(&scalars) + Self::decode_shape(&scalars) } - /// The announcement its scalars state, every value checked in range. + /// A zero-knowledge proof's announced shape, from its scalars, checked as a full announcement is. /// /// # Errors /// - /// 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. + /// Refuses a non-canonical size, a table height or a rate outside its range. + pub(crate) fn decode_shape(scalars: &[F192; N_TABLES + 1]) -> Result<(PerTable, Rate), CpuError> { + 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; N_TABLES + 1]) -> Result<(PerTable, usize), CpuError> { let size = |x: &F192| -> Result { if x.c1 != 0 || x.c2 != 0 { return Err(CpuError::NonCanonicalSize); @@ -761,7 +773,41 @@ impl Announcement { for (t, x) in TableId::ALL.into_iter().zip(scalars) { taus[t] = size(x)?; } - let log_inv_rate = size(&scalars[N_TABLES])?; + 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 }) + } + + /// Read an announcement off the proof, binding it, and check every value is in range. + /// + /// The checks run before any reduction, so an out-of-range announcement costs nothing. + /// + /// # Errors + /// + /// Refuses a short stream, then what decoding refuses. + pub(super) fn read(vs: &mut impl Verifier) -> Result { + let mut scalars = [F192::ZERO; Self::LEN]; + for x in &mut scalars { + *x = vs.prover_message()?; + } + Self::decode(&scalars) + } + + /// The announcement its scalars state, every value checked in range. + /// + /// # Errors + /// + /// 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 { + let sizes: &[F192; N_TABLES + 1] = scalars[..=N_TABLES] + .try_into() + .expect("the sizes lead the announcement"); + let (taus, log_inv_rate) = Self::decode_sizes(sizes)?; // 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]; @@ -771,14 +817,9 @@ 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, }) } @@ -791,7 +832,7 @@ 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, ProofKind::Plain) } } @@ -801,14 +842,42 @@ impl Layout { /// # 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, kind: ProofKind) -> 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 !(crate::pcs::MIN_MU..=crate::pcs::MAX_MU).contains(&layout.shape.mu) { - return Err(CpuError::WitnessSize { mu: layout.shape.mu }); + Self::new(p, taus, 0).of_kind(kind).fits() + } + + /// The layout, if the commitment takes its stacked witness. + fn fits(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 }) + } + } + + /// The same columns, laid out for a proof of this kind. + /// + /// A zero-knowledge proof's layout differs in two ways: + /// + /// - its stack is the hiding one: lanes long enough to hide, then the zero lanes and the random group; + /// - its bus grinds one more list's worth of bits. + /// + /// Why the extra grinding: + /// + /// - A zero-knowledge proof commits its keys too, before the bus's challenges. + /// - That commitment also binds only to a list, and hidden values are what was sent minus a key. + /// - So each challenge before the openings must hold against a pair of list members, one of each list. + pub(crate) fn of_kind(self, kind: ProofKind) -> Self { + match kind { + ProofKind::Plain => self, + ProofKind::ZeroKnowledge => Self { + shape: StackShape::hiding(witness::committed_len(&self.placements)), + grinding: self.grinding + pcs::whir::L0_LIST_BITS as u32, + ..self + }, } - 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 e855c3424..c5933aecf 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 zero_knowledge; pub use deferred::{Claim, DeferredClaims, MalformedClaim, ProgramPoint}; pub use error::{CpuError, DecodeError, ProveError, VerifyError}; @@ -38,6 +39,7 @@ pub use layout::{Layout, Lookup, Q_BASE}; pub use output::Output; pub use program::{Program, Stats}; pub use proof::Proof; +pub(crate) use proof::ProofKind; pub use prover::{ProvenRun, Prover}; /// Each table holds at most `2^MAX_LOG_ROWS` rows: its class's executed instructions. diff --git a/crates/leanvm_core/src/cpu/program.rs b/crates/leanvm_core/src/cpu/program.rs index 127d22510..417c164cd 100644 --- a/crates/leanvm_core/src/cpu/program.rs +++ b/crates/leanvm_core/src/cpu/program.rs @@ -8,15 +8,18 @@ use super::error::{CpuError, ProveError, VerifyError}; use super::execute::{Execution, Recorder, RowCounter, TraceBuilder}; use super::filler::{FillBlocks, Plan}; use super::layout::{Announcement, Lookup, Schema, Sizes}; +use super::proof::ProofKind; use super::reduce::TableClaims; use super::witness::Witness; -use super::{Output, Proof}; +use super::zero_knowledge; +use super::{Output, Proof, Prover}; use crate::class_flock::FlockId; use crate::constraints::{Claims, Columns}; use crate::leaf::PublicColumns; -use crate::pcs::{Committed, Rate}; +use crate::pcs::{Committed, Rate, RingSwitch, StackClaim}; use crate::rv::{ElfError, Guest, Machine, ProgramError, Region, RiscvProgram}; use crate::tables::{ClassTable, Clock, PerTable, TableId}; +use crate::witness::StackShape; use crate::{constraints, leaf}; use fiat_shamir::arith::Native; use fiat_shamir::{ProverState, SessionId, VerifierState}; @@ -53,6 +56,9 @@ impl Program { /// The program's digest follows it in the tag, naming the relation. const SESSION_TAG: &'static [u8] = b"leanvm/rv64im-proof/blake2s-duplex/gf2-192/v2"; + /// The session tag of a zero-knowledge proof: another protocol, so no challenge of one kind is one of the other. + const ZK_SESSION_TAG: &'static [u8] = b"leanvm/rv64im-zk-proof/blake2s-duplex/gf2-192/v1"; + /// The cycles between two checks of a running trace against one commitment. const SIZE_CHECK_PERIOD: u64 = 1 << 16; @@ -183,7 +189,7 @@ impl Program { let counts = recorder.row_counts(); let heights = PerTable::from_fn(|t: TableId| t.spec().provable_height(counts[t])); if heights != checked { - self.committed_size(heights)?; + self.committed_size(heights, ProofKind::Plain)?; checked = heights; } } @@ -212,20 +218,25 @@ impl Program { proven_rows: counts.values().sum(), counts, base_counts, - committed: self.committed_size(counts)?, + committed: self.committed_size(counts, ProofKind::Plain)?, }) } - /// Prove a finished run, which a test may have forged. - pub(super) fn prove_execution(&self, exec: &Execution, rate: Rate) -> (Proof, Stats) { - let w = info_span!("Build witness").in_scope(|| Witness::build(self, exec)); + /// Prove a finished run, which a test may have forged, as `prover` proves. + pub(super) fn prove_execution(&self, exec: &Execution, prover: &Prover) -> (Proof, Stats) { + let w = info_span!("Build witness").in_scope(|| Witness::build(self, exec, prover.kind())); 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) + let output = Output::new(exec.output); + let proof = match prover.randomness() { + Some(randomness) => zero_knowledge::prove(self, w, output, prover.rate(), &randomness.seed()), + None => self.prove_witness(w, output, prover.rate()), + }; + (proof, stats) } /// Prove a built witness, which a test may have forged. @@ -247,6 +258,24 @@ impl Program { let committed = info_span!("Commit") .in_scope(|| Committed::new(&mut ps, &w.q, w.layout.shape, rate).expect("the witness matches its layout")); + let (slots, rings) = self.prove_reductions(&mut ps, &mut w, output); + info_span!("PCS open").in_scope(|| { + committed + .open(&mut ps, &w.q, &slots, &rings) + .expect("opening uses the committed witness"); + }); + Proof(ps.into_proof(), ProofKind::Plain) + } + + /// Flock's reductions, the bus and the table sumcheck over the committed witness. + /// + /// It returns 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) { // Flock's reductions, batched over every class circuit then every clock circuit under shared challenges. // // Each circuit leaves a validity claim on its packed witness, discharged in the same opening through a ring-switched region. @@ -261,7 +290,7 @@ impl Program { f.instance(column, l.taus[f.table()], tables) }) .collect(); - reduction::prove(&instances, &mut ps) + reduction::prove(&instances, ps) }); drop(reductions); @@ -271,15 +300,7 @@ impl Program { let (bus_claims, table_claims) = { let cols = w.columns(); let mut bus = info_span!("Prove bus").in_scope(|| { - 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()) @@ -314,7 +335,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)) }; @@ -327,12 +348,7 @@ impl Program { // Each producer's multiplicity column is a ring-switched region too, as is each register word. let rings = l.rings(slices, &table_claims.producers, &table_claims.summed, F192::ZERO); - info_span!("PCS open").in_scope(|| { - committed - .open(&mut ps, &w.q, &slots, &rings) - .expect("opening uses the committed witness"); - }); - Proof(ps.into_proof()) + (slots, rings) } /// Check that the proof shows this program, run on some advice, exiting with this output. @@ -362,6 +378,10 @@ impl Program { #[doc(hidden)] #[tracing::instrument(name = "Verify core", skip_all)] pub fn verify_core(&self, output: Output, proof: &Proof) -> Result { + if proof.is_zero_knowledge() { + let vs = VerifierState::new(&self.zk_session(), output.words(), &proof.0); + return zero_knowledge::verify_core(self, output, vs).map(|(_, claims)| claims); + } // The session names the program, and the output is the instance, as on the prover's side. let mut vs = VerifierState::new(&self.session(), output.words(), &proof.0); self.core(output, &mut vs) @@ -377,6 +397,12 @@ impl Program { #[tracing::instrument(name = "Verify", skip_all)] #[doc(hidden)] pub fn verify_recording(&self, output: Output, proof: &Proof) -> Result, VerifyError> { + if proof.is_zero_knowledge() { + let recording = Recording::new(VerifierState::new(&self.zk_session(), output.words(), &proof.0)); + let (recording, claims) = zero_knowledge::verify_core(self, output, recording)?; + self.check_deferred(&claims)?; + return Ok(recording.into_openings()); + } let mut recording = Recording::new(VerifierState::new(&self.session(), output.words(), &proof.0)); let claims = self.core(output, &mut recording)?; self.check_deferred(&claims)?; @@ -419,6 +445,11 @@ impl Program { SessionId::new(&[Self::SESSION_TAG, &self.digest].concat()) } + /// The session of a zero-knowledge proof: its own protocol tag, then the program's digest. + pub(crate) fn zk_session(&self) -> SessionId { + SessionId::new(&[Self::ZK_SESSION_TAG, &self.digest].concat()) + } + /// 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. @@ -432,13 +463,22 @@ impl Program { /// # Errors /// /// Refuses a stack larger than one commitment. - pub(super) fn committed_size(&self, row_counts: PerTable) -> Result { + pub(super) fn committed_size(&self, row_counts: PerTable, kind: ProofKind) -> Result { let taus = PerTable::from_fn(|t: TableId| crate::log2_strict_usize(t.spec().provable_height(row_counts[t]))); let (placements, shape) = Sizes::of(&self.rv).stack(&taus); - if shape.mu > crate::pcs::MAX_MU { + let placed = crate::witness::committed_len(&placements); + // A zero-knowledge proof commits the hiding stack: lanes long enough to hide, then the random group. + let (mu, committed) = match kind { + ProofKind::Plain => (shape.mu, placed), + ProofKind::ZeroKnowledge => { + let hiding = StackShape::hiding(placed); + (hiding.mu, hiding.committed_len()) + } + }; + if mu > crate::pcs::MAX_MU { return Err(ProveError::TooLong); } - Ok(crate::witness::committed_len(&placements)) + Ok(committed) } /// The digest of `rv`'s public statement. @@ -702,7 +742,7 @@ mod tests { /// The tuples a run leaves unmatched, as `(side, block, row)`. fn unmatched_run(program: &Program, exec: &Execution) -> Vec<(&'static str, usize, usize)> { - unmatched(&Witness::build(program, exec)) + unmatched(&Witness::build(program, exec, ProofKind::Plain)) } /// An honest run's bus balances tuple by tuple, which says more than the proof @@ -711,7 +751,7 @@ mod tests { fn an_honest_run_balances() { let text = Asm::new().i(Addi, Reg::A0, Reg::ZERO, 5).exit().finish(); let program = Program::new(&text, Region::TEXT.base(), vec![], 2, 0).expect("valid instruction program"); - let w = Witness::build(&program, &program.execute(&[]).unwrap()); + let w = Witness::build(&program, &program.execute(&[]).unwrap(), ProofKind::Plain); let unmatched = unmatched(&w); assert!( unmatched.is_empty(), @@ -745,11 +785,14 @@ mod tests { let counts = counter.row_counts(); let rows: usize = counts.values().sum(); assert!(rows < 1 << crate::pcs::MAX_MU, "{rows} rows counted"); - assert_eq!(program.committed_size(counts), Err(ProveError::TooLong)); + assert_eq!( + program.committed_size(counts, ProofKind::Plain), + Err(ProveError::TooLong) + ); // A period earlier, no table had more than these rows, and they fit. let earlier = counts.map(|c| c.saturating_sub(Program::SIZE_CHECK_PERIOD as usize)); - assert!(program.committed_size(earlier).is_ok()); + assert!(program.committed_size(earlier, ProofKind::Plain).is_ok()); } #[test] @@ -773,7 +816,7 @@ mod tests { .unwrap(); row.out = pc + 4; execution.trace.reg_fin[RegisterFile::SINK as usize] = F64(pc + 4); - let witness = Witness::build(&program, &execution); + let witness = Witness::build(&program, &execution, ProofKind::Plain); let unmatched = unmatched(&witness); // The final state on the pull side, and the ALU's state push, the push side's // first block past its four framework blocks. @@ -800,7 +843,7 @@ mod tests { /// /// The bus is unbalanced until that column is forged, and balanced after, so what refuses it is the verifier. fn forged_jump(program: &Program, forged: &Execution, row: usize, value: u64) -> CpuError { - let mut w = Witness::build(program, forged); + let mut w = Witness::build(program, forged, ProofKind::Plain); // The row's state push, and the next row's pull. let left = unmatched(&w); assert_eq!(left.len(), 2, "{left:?}"); @@ -1003,7 +1046,7 @@ mod tests { (exit.v1, exit.v2, exit.out) = (1, 1, 2); forged.trace.reg_fin[0] = F64(1); forged.trace.reg_fin[RegisterFile::SINK as usize] = F64(2); - let mut w = Witness::build(&program, &forged); + let mut w = Witness::build(&program, &forged, ProofKind::Plain); let bus = alu.class_table().flushes(); let Coord::Col(destination) = bus.pull[1][ClassTable::DESTINATION_SLOT] else { panic!("the ALU binds its destination to a column"); @@ -1060,7 +1103,7 @@ mod tests { /// The verifier's verdict on the proof of a run forged into `exec`, whose bus balances. fn verdict(program: &Program, exec: &Execution) -> Result<(), CpuError> { - let w = Witness::build(program, exec); + let w = Witness::build(program, exec, ProofKind::Plain); let unmatched = unmatched(&w); assert!(unmatched.is_empty(), "the forged run balances: {unmatched:?}"); let proof = program.prove_witness(w, exec.output.into(), Rate::MIN); @@ -1128,7 +1171,7 @@ mod tests { for (k, word) in x.c.into_iter().enumerate() { forged.trace.ram_fin[10 + k] = F64(word); } - let w = Witness::build(&program, &forged); + let w = Witness::build(&program, &forged, ProofKind::Plain); let unmatched = unmatched(&w); assert_eq!(unmatched.len(), 4, "{unmatched:?}"); assert_unbalanced(&program, w, forged.output.into()); @@ -1171,7 +1214,7 @@ mod tests { // Each of a's limbs is at `ram + 4 + 8j`, which no cell is: the row's pull and push there, and the seed push // and final pull of the word at `ram + 8j`, which the row no longer meets. - let w = Witness::build(&program, &forged); + let w = Witness::build(&program, &forged, ProofKind::Plain); let unmatched = unmatched(&w); assert_eq!(unmatched.len(), 12, "{unmatched:?}"); assert_unbalanced(&program, w, forged.output.into()); @@ -1255,7 +1298,7 @@ mod tests { let row = real(&mut forged.trace.rows[TableId::of(class).unwrap()]); row.ram.address = cell + 1; (forged.trace.ram_fin[4], forged.trace.ram_ts[4]) = (F64::ZERO, F64(Clock::SEED_CLOCK)); - let w = Witness::build(&misaligned, &forged); + let w = Witness::build(&misaligned, &forged, ProofKind::Plain); // The access's pull and push, at an address no cell has. assert_eq!(unmatched(&w).len(), 2, "{class:?}: {:?}", unmatched(&w)); assert_unbalanced(&misaligned, w, forged.output.into()); @@ -1278,7 +1321,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, &Prover::new(Rate::MIN)); program .verify(honest.output.into(), &proof) .expect("the honest run verifies"); @@ -1292,7 +1335,7 @@ mod tests { forged.output[0] = 8; forged.trace.reg_fin[Reg::A0.index()] = F64(8); // The multiplicities follow the forged gap, so no producer is left unmatched. - let w = Witness::build(&program, &forged); + let w = Witness::build(&program, &forged, ProofKind::Plain); let push = w.layout.push.len(); assert!( unmatched(&w) @@ -1313,7 +1356,7 @@ mod tests { let exec = program.execute(&[]).unwrap(); let alu = TableId::ALU; let row = exec.trace.rows[alu].iter().position(|r| r.index == 0).unwrap(); - let mut w = Witness::build(&program, &exec); + let mut w = Witness::build(&program, &exec, ProofKind::Plain); // Bytecode slot 9 binds the decoded branch target offset. let bus = alu.class_table().flushes(); let Coord::Col(branch_offset) = bus.pull[1][9] else { @@ -1345,7 +1388,7 @@ mod tests { .enumerate() { for flip in [1u64, 2, 4] { - let mut w = Witness::build(&program, &exec); + let mut w = Witness::build(&program, &exec, ProofKind::Plain); assert_eq!(w.layout.producers[p].col, col); column_mut(&mut w, col)[0].0 ^= flip; let unmatched = unmatched(&w); @@ -1379,7 +1422,7 @@ mod tests { assert_eq!(addi.prev[..2], [Clock::SEED_CLOCK, addi.ts]); addi.prev[1] = Clock::SEED_CLOCK; forged.trace.reg_ts[Reg::RA.index()] = F64(addi.ts); - let mut w = Witness::build(&program, &forged); + let mut w = Witness::build(&program, &forged, ProofKind::Plain); let table = alu.class_table(); let a1 = Schema::get().spans[alu].0 + table.register_bits().fields[0].col; virtual_mut(&mut w, a1)[row] = F64(Reg::RA.index() as u64); @@ -1409,13 +1452,16 @@ mod tests { let alu = TableId::ALU; let row = exec.trace.rows[alu].iter().position(|r| r.index == 0).unwrap(); // The ALU opens its word, which the tables of its height share after it. - let word = Witness::build(&program, &exec).layout.registers.swap_remove(0); + let word = Witness::build(&program, &exec, ProofKind::Plain) + .layout + .registers + .swap_remove(0); assert_eq!(word.tables[0], alu); assert!(word.tables.len() > 1, "the tables of one height share the word"); let bits = |t: TableId| t.class_table().register_bits().n_slices(); let used: usize = word.tables.iter().map(|&t| bits(t)).sum(); for bit in [0, bits(alu), used, 63] { - let mut w = Witness::build(&program, &exec); + let mut w = Witness::build(&program, &exec, ProofKind::Plain); column_mut(&mut w, word.col)[row].0 ^= 1 << bit; assert!( unmatched(&w).is_empty(), @@ -1543,7 +1589,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, &Prover::new(Rate::MIN)); 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 21c8987fc..d7e67cf24 100644 --- a/crates/leanvm_core/src/cpu/proof.rs +++ b/crates/leanvm_core/src/cpu/proof.rs @@ -10,19 +10,44 @@ use std::fmt::{self, Debug, Formatter}; /// The program checks it against the output. /// /// 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 struct Proof(#[doc(hidden)] pub ProofTranscript, pub(crate) ProofKind); -impl Proof { - /// The header of a proof's bytes: the magic `LVMP`, then the protocol version. +/// Whether a proof is zero knowledge. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub(crate) enum ProofKind { + /// A plain proof. + Plain, + /// A zero-knowledge proof. + ZeroKnowledge, +} + +impl ProofKind { + /// The header of a proof's bytes: the magic, then the protocol version. /// /// The version is bumped by every change to what a proof says. - const ENVELOPE: Envelope = Envelope::new(*b"LVMP", 17); + /// The magic tells the two kinds apart, so a proof of one kind is refused as the other. + const fn envelope(self) -> Envelope { + match self { + Self::Plain => Envelope::new(*b"LVMP", 17), + Self::ZeroKnowledge => Envelope::new(*b"LVMZ", 1), + } + } +} + +impl Proof { + /// Whether the proof is zero knowledge. + #[must_use] + pub fn is_zero_knowledge(&self) -> bool { + self.1 == ProofKind::ZeroKnowledge + } /// The proof's bytes. #[must_use] pub fn to_bytes(&self) -> Vec { - Self::ENVELOPE.seal(&self.0.to_bytes()) + self.1.envelope().seal(&self.0.to_bytes()) } /// The proof these bytes encode. @@ -32,10 +57,15 @@ 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 kind = if bytes.starts_with(&ProofKind::ZeroKnowledge.envelope().magic()) { + ProofKind::ZeroKnowledge + } else { + ProofKind::Plain + }; + let body = kind.envelope().open(bytes)?; ProofTranscript::from_bytes(body) - .map(Self) + .map(|t| Self(t, kind)) .ok_or(DecodeError::Malformed) } } diff --git a/crates/leanvm_core/src/cpu/prover.rs b/crates/leanvm_core/src/cpu/prover.rs index f38bc8a37..28c8166fd 100644 --- a/crates/leanvm_core/src/cpu/prover.rs +++ b/crates/leanvm_core/src/cpu/prover.rs @@ -1,8 +1,10 @@ //! The prover: it runs a program and proves the run. +use super::proof::ProofKind; use super::{Output, Program, Proof, ProveError, Stats}; use crate::pcs::Rate; use tracing::info_span; +use zk::Randomness; /// A prover: it proves runs at one commitment rate. /// @@ -10,6 +12,13 @@ use tracing::info_span; /// /// The verifier needs no rate: each proof announces its own. /// +/// # Zero knowledge +/// +/// A zero-knowledge prover 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 shape, so that the heights say nothing of the advice. +/// /// # Performance /// /// A proof touches gigabytes of memory, and frees it before returning. @@ -23,6 +32,8 @@ use tracing::info_span; pub struct Prover { /// The commitment rate every proof is made at. rate: Rate, + /// Where a zero-knowledge prover draws its randomness; none for a plain prover. + randomness: Option, } impl Prover { @@ -33,7 +44,7 @@ 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, randomness: None } } /// The commitment rate every proof is made at. @@ -42,6 +53,34 @@ impl Prover { self.rate } + /// The same prover, making zero-knowledge proofs from this randomness. + #[must_use] + pub const fn zero_knowledge(self, randomness: Randomness) -> Self { + Self { + randomness: Some(randomness), + ..self + } + } + + /// Whether the prover makes zero-knowledge proofs. + #[must_use] + pub const fn is_zero_knowledge(&self) -> bool { + self.randomness.is_some() + } + + /// Where a zero-knowledge prover draws its randomness. + pub(super) const fn randomness(&self) -> Option { + self.randomness + } + + /// The kind of proof the prover makes. + pub(super) const fn kind(&self) -> ProofKind { + match self.randomness { + Some(_) => ProofKind::ZeroKnowledge, + None => ProofKind::Plain, + } + } + /// Run the program on the advice, and prove the run. /// /// # Arguments @@ -54,11 +93,15 @@ 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_zero_knowledge()) + )] pub fn prove(&self, program: &Program, advice: &[u64]) -> Result { let exec = info_span!("Execute program").in_scope(|| program.execute(advice))?; - program.committed_size(exec.trace.row_counts())?; - let (proof, stats) = program.prove_execution(&exec, self.rate); + program.committed_size(exec.trace.row_counts(), self.kind())?; + let (proof, stats) = program.prove_execution(&exec, self); 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 d172cfb10..f81553b25 100644 --- a/crates/leanvm_core/src/cpu/reduce.rs +++ b/crates/leanvm_core/src/cpu/reduce.rs @@ -67,7 +67,23 @@ impl Layout { rate: Rate, ) -> Result, CpuError> { let commitment = Commitment::read(v, self.shape, rate)?; + let claims = self.verify_committed(v, &commitment, clock, output)?; + v.check_eof()?; + Ok(claims) + } + /// The verifier's core past the commitment's root: the flock reductions, the bus and the tables, and the opening. + /// + /// # Errors + /// + /// Returns the first stage that refuses the proof. + pub(crate) fn verify_committed( + &self, + v: &mut V, + commitment: &Commitment, + clock: V::E, + output: &[V::E; 4], + ) -> Result, CpuError> { // Flock's reductions, batched over every class circuit then every clock circuit, each leaving its matrices' form to its circuit. // They read only the commitment; their claims wait for the opening, whose challenges follow every claim. let batches = FlockId::batches(&self.taus); @@ -86,7 +102,6 @@ impl Layout { commitment.verify(v, &reduced.slots, &rings) }) .map_err(CpuError::Open)?; - v.check_eof()?; Ok(DeferredClaims { program: reduced.program, circuits, diff --git a/crates/leanvm_core/src/cpu/witness.rs b/crates/leanvm_core/src/cpu/witness.rs index 68db993e3..bd3ea7c27 100644 --- a/crates/leanvm_core/src/cpu/witness.rs +++ b/crates/leanvm_core/src/cpu/witness.rs @@ -4,6 +4,7 @@ use super::MAX_LOG_ROWS; use super::execute::Execution; use super::layout::{Layout, Lookup, Schema, Shared, q_column}; use super::program::Program; +use super::proof::ProofKind; use crate::class_flock::FlockId; use crate::tables::{ClassTable, FillContext, PerTable, TableId}; use flock::Tables; @@ -29,12 +30,14 @@ pub(crate) struct Witness { } impl Witness { - /// The witness of a finished run. + /// The witness of a finished run, laid out for a proof of this kind. + /// + /// A zero-knowledge proof's stack ends with zero lanes, which its hiding commitment completes. /// /// # 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(program: &Program, exec: &Execution, kind: ProofKind) -> 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,7 +64,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 = Layout::new(p, taus, trace.ts_final).of_kind(kind); // 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/zero_knowledge.rs b/crates/leanvm_core/src/cpu/zero_knowledge.rs new file mode 100644 index 000000000..5f709cf00 --- /dev/null +++ b/crates/leanvm_core/src/cpu/zero_knowledge.rs @@ -0,0 +1,467 @@ +//! Zero-knowledge proofs of a run: the plain proof under one-time pads, on a hiding commitment, and an outer proof. +//! +//! The transcript, after a session of its own: +//! +//! ```text +//! clear each table's height and the rate: the run's public shape +//! clear the stack's root (hiding), then the key commitment's root +//! hidden the final clock's free bits, the bus, the tables, flock's reductions, the opening's lane rounds +//! clear the rest of the opening, from its revealed claim on +//! clear the public evaluations the deferred claims need +//! hidden the outer proof's auxiliary values +//! clear the outer proof and the key commitment's opening +//! ``` +//! +//! The verifier runs its own code over the padded transcript through a recorder. +//! +//! The outer proof shows the keys satisfy what it recorded. +//! +//! # The deferred claims +//! +//! The core leaves claims on the program's polynomials and on each circuit's matrices, as a plain proof's does. +//! +//! Their points are challenges, but some of their weights and values are hidden. +//! +//! - The prover sends what the claims need of the public polynomials: each bytecode term, the image's value, each circuit's slice weights. +//! - The verifier records each hidden claim as a linear constraint on those public values. +//! - One challenge `rho` then batches the public values into claims of the plain claims' shape, which are settled as a plain proof's. +//! +//! So the core of either kind of proof leaves the same claims, and recursion carries them out alike. + +use super::deferred::{Claim, DeferredClaims, MalformedClaim, ProgramPoint}; +use super::layout::{Announcement, Layout, Lookup}; +use super::proof::ProofKind; +use super::witness::Witness; +use super::{CpuError, Output, Program, Proof}; +use crate::class_flock::{FlockId, N_FLOCKS}; +use crate::constraints::ConstraintError; +use crate::leaf::{self, N_TUPLE_BITS, PublicColumns, SparseColumn}; +use crate::pcs::{Commitment, Committed, Rate}; +use crate::tables::Clock; +use fiat_shamir::arith::{Arith, Verifier}; +use fiat_shamir::{ProofTranscript, ProverState, VerifierState}; +use flock::FlockError; +use flock::lincheck::{LincheckError, MatrixForm}; +use pcs::merkle::Hash; +use pcs::verifier::OpeningVerifier; +use primitives::field::{F64, F192}; +use std::ops::Range; +use tracing::info_span; +use zk::{KeyCommitment, Keys, OuterError, Purpose, Recorder, Seed, Value}; + +/// 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, at `rate`, every random draw from `seed`. +/// +/// # Panics +/// +/// Panics if the witness's bus does not balance, or if the outer proof outgrows the key commitment. +pub(super) fn prove(program: &Program, mut w: Witness, output: Output, rate: Rate, seed: &Seed) -> Proof { + let mut ps = ProverState::new(&program.zk_session(), output.words()); + Announcement::write_shape(&w.layout.taus, rate, &mut ps); + + // The hiding stack, then the keys, both before any challenge. + let committed = info_span!("Commit").in_scope(|| { + Committed::new_hiding( + &mut ps, + &mut w.q, + w.layout.shape, + rate, + &mut seed.stream(Purpose::Commitment), + ) + .expect("the witness matches its layout") + }); + let keys = info_span!("Commit keys").in_scope(|| Keys::commit(&mut ps, rate.log_inv_rate().into(), seed)); + + // The plain proof, every scalar padded until the opening reveals its claim after its lane fold. + ps.set_keys(keys.keys().to_vec()); + ps.set_hidden(true); + for bit in FREE_CLOCK_BITS { + ps.prover_message(&F192::from(F64(w.ts_final >> bit & 1))); + } + let (slots, rings) = program.prove_reductions(&mut ps, &mut w, output); + info_span!("PCS open").in_scope(|| { + committed + .open(&mut ps, &w.q, &slots, &rings) + .expect("opening uses the committed witness"); + }); + drop((committed, w, slots, rings)); + + // The public evaluations the claims of the prover's own core need, then the challenge that batches them. + let evaluations = info_span!("Public evaluations").in_scope(|| { + let (_, core) = replay(program, output, ps.proof()); + PublicEvaluations::of(program, &core.claims) + }); + evaluations.send(&mut ps); + let _rho: F192 = ps.verifier_message(); + + // The record of the whole padded transcript, then the outer proof. + let record = info_span!("Record").in_scope(|| { + let (mut rec, core) = replay(program, output, ps.proof()); + core.claims + .into_plain(&mut rec) + .expect("the prover's own claims are well formed"); + rec.finish().1 + }); + info_span!("Outer proof").in_scope(|| zk::outer::prove(&mut ps, &record, &keys)); + Proof(ps.into_proof(), ProofKind::ZeroKnowledge) +} + +/// The prover's replay of its own proof so far, through the verifier's recorder: the recorder, and the core it recorded. +/// +/// # Panics +/// +/// Panics if the prover's own proof is refused. +fn replay<'p>( + program: &Program, + output: Output, + proof: &'p ProofTranscript, +) -> (Recorder>, RecordedCore) { + let mut rec = Recorder::new(VerifierState::new(&program.zk_session(), output.words(), proof)); + let core = record_proof(program, &mut rec, output).expect("the prover's own proof verifies"); + (rec, core) +} + +/// Verify a zero-knowledge proof's core over a verifier reading it, returning the claims it leaves. +/// +/// They have the plain claims' shape, and are settled as a plain proof's. +/// +/// # Errors +/// +/// Returns the first stage that refuses the proof. +pub(super) fn verify_core(program: &Program, output: Output, inner: V) -> Result<(V, DeferredClaims), CpuError> +where + V: OpeningVerifier + PublicColumns, +{ + let mut rec = Recorder::new(inner); + let core = record_proof(program, &mut rec, output)?; + let claims = core.claims.into_plain(&mut rec)?; + let mut inner = zk::outer::verify(rec, &core.keys).map_err(CpuError::Outer)?; + inner.check_eof()?; + Ok((inner, claims)) +} + +/// The recorded core of a proof read natively: its announced shape, its layout, then the core. +fn record_proof>( + program: &Program, + rec: &mut Recorder, + output: Output, +) -> Result, CpuError> { + let (taus, rate) = Announcement::read_shape(rec.inner())?; + let layout = Layout::announced(program.rv(), taus, ProofKind::ZeroKnowledge)?; + let output = output.words().map(|o| rec.constant(F192::from(F64(o)))); + layout.record_core(rec, rate, &output) +} + +/// What a zero-knowledge proof's verifier records of the plain core. +pub(crate) struct RecordedCore { + /// The key commitment, which the outer proof's opening is checked against. + pub(crate) keys: KeyCommitment, + /// The claims the core leaves on the program's polynomials and the circuits' matrices, some of their parts hidden. + pub(crate) claims: DeferredClaims>, +} + +impl Layout { + /// The plain core over a padded transcript, recorded, past the announced shape. + /// + /// It reads the stack's root, the key commitment's root, the final clock's hidden bits, then runs the plain core. + /// + /// It runs over any verifier, natively or in rows. + /// + /// # Errors + /// + /// Returns the first stage that refuses the proof. + pub(crate) fn record_core( + &self, + rec: &mut Recorder, + rate: Rate, + output: &[Value; 4], + ) -> Result, CpuError> { + let commitment = Commitment::read(rec, self.shape, rate)?; + let keys = KeyCommitment::read(rec.inner(), rate.log_inv_rate().into()) + .map_err(|e| CpuError::Outer(OuterError::KeyOpening(e)))?; + + // The final clock: its live bit, and each free bit hidden and constrained to be a bit. + rec.set_hidden(true); + let mut clock = rec.constant(F192::from(F64(Clock::SEED_CLOCK))); + for bit in FREE_CLOCK_BITS { + let b = rec.prover_message()?; + rec.ensure_bit(b, || CpuError::FinalClock)?; + clock = rec.mul_const_add(b, F192::from(F64(1 << bit)), clock); + } + let claims = self.verify_committed(rec, &commitment, clock, output)?; + Ok(RecordedCore { keys, claims }) + } +} + +/// What the deferred claims need of the public polynomials, at their public points. +struct PublicEvaluations { + /// The bytecode producer's terms `D_i`, one per twist weight. + twist_terms: Vec, + /// RAM's image at the image point. + image: F192, + /// Each circuit's weight on each bit slice. + slice_weights: Vec>, +} + +impl PublicEvaluations { + /// The evaluations the prover's own claims need. + /// + /// # Panics + /// + /// Panics on a claim whose public coordinates are hidden: the prover's own claims never are. + fn of(program: &Program, claims: &DeferredClaims>) -> Self { + let rv = program.rv(); + let point = &claims.program.point; + let public = |xs: &[Value]| publics(xs).expect("a public point"); + let (bytecode, image_point) = (public(&point.bytecode), public(&point.image_point)); + let kbc = crate::log2_strict_usize(rv.entries().len()); + let (chi, alphas) = bytecode.split_at(kbc); + let weights = leaf::fingerprint_weights(alphas); + let twist_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 slice_weights = (FlockId::ALL.into_iter().zip(&claims.circuits)) + .map(|(f, c)| { + // The weights depend on the slices' count, not their values. + let form = public_form(&c.point).expect("a public form"); + let form = MatrixForm { + s_hat_v: vec![F192::ZERO; c.point.s_hat_v.len()], + ..form + }; + form.slice_weights(f.circuit()) + }) + .collect(); + Self { + twist_terms, + image, + slice_weights, + } + } + + /// Send them, in the order the verifier reads them. + fn send(&self, ps: &mut ProverState) { + ps.prover_messages(&self.twist_terms); + ps.prover_message(&self.image); + for weights in &self.slice_weights { + ps.prover_messages(weights); + } + } +} + +/// The values of elements that are all public. +fn publics(xs: &[Value]) -> Option> { + xs.iter().map(|&x| x.public()).collect() +} + +/// A matrix form with no slices, if every coordinate but the slices is public. +fn public_form(form: &MatrixForm>) -> Option> { + Some(MatrixForm { + alpha: form.alpha.public()?, + z_skip: form.z_skip.public()?, + x_inner_rest: publics(&form.x_inner_rest)?, + r_inner_rest: publics(&form.r_inner_rest)?, + s_hat_v: Vec::new(), + }) +} + +/// A value the verifier read in the clear. +fn clear(x: Value) -> E { + x.public().expect("read while hiding is off") +} + +impl DeferredClaims> { + /// The claims of the plain shape: the hidden parts settled as constraints on public evaluations, then those batched. + /// + /// It reads the public evaluations, records one constraint per claim, draws `rho`, and batches: + /// + /// ```text + /// program: twist = (1, rho, ..., rho^(L-1)), image weight rho^L, value sum_i rho^i D_i + rho^L image + /// circuit: slices = (1, rho, ...), value sum_i rho^i w_i + /// ``` + /// + /// A false public evaluation makes its batched claim false, except with probability `L / |E|` over `rho`. + /// + /// # Errors + /// + /// A claim of the wrong count or shape, or one whose point is hidden. + pub(crate) fn into_plain>( + self, + rec: &mut Recorder, + ) -> Result, CpuError> { + if self.circuits.len() != N_FLOCKS { + return Err(CpuError::MalformedClaim(MalformedClaim::CircuitCount { + expected: N_FLOCKS, + got: self.circuits.len(), + })); + } + let malformed = CpuError::MalformedClaim(MalformedClaim::ProgramPoint); + + // The program claim: its point public, then value = image_weight image + sum_i twist_i D_i. + let point = &self.program.point; + let (Some(bytecode), Some(image_point)) = (publics(&point.bytecode), publics(&point.image_point)) else { + return Err(malformed); + }; + // A multiplicity is one word, so it has at most 64 bits; the point's own lengths are checked when it is settled. + if point.twist.len() > 64 || bytecode.len() < N_TUPLE_BITS { + return Err(malformed); + } + let terms = rec.prover_messages(point.twist.len())?; + let image = rec.prover_message()?; + let mut expected = rec.mul(point.image_weight, image); + for (&mu, &d) in point.twist.iter().zip(&terms) { + expected = rec.mul_add(mu, d, expected); + } + rec.ensure_eq(expected, self.program.value, || { + CpuError::Constraint(ConstraintError::FinalMismatch) + })?; + + // Each circuit claim: its form public but its slices, then value = sum_i s_i w_i. + let mut forms = Vec::with_capacity(N_FLOCKS); + let mut weights = Vec::with_capacity(N_FLOCKS); + for (f, claim) in FlockId::ALL.into_iter().zip(&self.circuits) { + let (table, part) = (f.table().name(), f.part()); + let malformed = || CpuError::MalformedClaim(MalformedClaim::MatrixForm { table, part }); + let form = public_form(&claim.point).ok_or_else(malformed)?; + let shape = MatrixForm { + alpha: F192::ZERO, + z_skip: F192::ZERO, + x_inner_rest: vec![F192::ZERO; form.x_inner_rest.len()], + r_inner_rest: vec![F192::ZERO; form.r_inner_rest.len()], + s_hat_v: vec![F192::ZERO; claim.point.s_hat_v.len()], + }; + if !f.shape().fits(&shape) { + return Err(malformed()); + } + let w = rec.prover_messages(claim.point.s_hat_v.len())?; + let zero = rec.zero(); + let expected = (claim.point.s_hat_v.iter().zip(&w)).fold(zero, |acc, (&s, &w)| rec.mul_add(s, w, acc)); + rec.ensure_eq(expected, claim.value, || CpuError::Flock { + table, + part, + error: FlockError::Lincheck(LincheckError::SumcheckMismatch), + })?; + forms.push(form); + weights.push(w); + } + + // One challenge batches every public evaluation into the plain claims' shape. + let rho = clear(rec.verifier_message()); + let v = rec.inner(); + let batched = |v: &mut V, values: &[Value]| -> (Vec, E) { + let powers = v.powers(rho, values.len() + 1); + let zero = v.zero(); + let sum = (values.iter().zip(&powers)).fold(zero, |acc, (&x, &p)| v.mul_add(clear(x), p, acc)); + (powers, sum) + }; + let (mut twist, value) = batched(v, &terms); + let image_weight = twist.pop().expect("one more power than terms"); + let value = v.mul_add(clear(image), image_weight, value); + let program = Claim { + point: ProgramPoint { + bytecode, + twist, + image_weight, + image_point, + }, + value, + }; + let circuits = (forms.into_iter().zip(&weights)) + .map(|(form, w)| { + let (mut s_hat_v, value) = batched(v, w); + s_hat_v.pop(); + Claim { + point: MatrixForm { s_hat_v, ..form }, + value, + } + }) + .collect(); + Ok(DeferredClaims { program, circuits }) + } +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::cpu::{ProvenRun, Prover}; + use crate::rv::asm::{Addi, Asm, Reg}; + use crate::rv::{Region, RegisterFile}; + use crate::tables::TableId; + use pcs::whir::WhirError; + use std::panic::{AssertUnwindSafe, catch_unwind}; + use zk::Randomness; + + /// `a0 = 5; exit`, and a zero-knowledge proof of it under a test seed. + 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) + .zero_knowledge(Randomness::Fixed([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_zero_knowledge()); + assert_eq!(program.verify(run.output, &run.proof), Ok(())); + assert_eq!(Proof::from_bytes(&run.proof.to_bytes()), Ok(run.proof.clone())); + + // Another output is another statement. + assert!(program.verify(Output::new([6, 0, 0, 0]), &run.proof).is_err()); + + // The same body labelled plain is read under the plain session, and refused. + let relabelled = Proof(run.proof.0.clone(), ProofKind::Plain); + assert!(program.verify(run.output, &relabelled).is_err()); + + // One seed, one proof; another seed, another valid proof. + assert_eq!(proof(7).1.proof, run.proof); + let other = proof(8).1.proof; + assert_eq!(program.verify(run.output, &other), Ok(())); + } + + #[test] + fn every_part_of_a_zero_knowledge_proof_is_bound() { + // Flip one bit of every 997th message byte, then of each of the last 512: the outer proof and the key opening. + let (program, run) = proof(7); + let n = run.proof.0.narg.len(); + for i in (0..n).step_by(997).chain(n.saturating_sub(512)..n) { + let mut forged = run.proof.clone(); + forged.0.narg[i] ^= 1; + let verdict = catch_unwind(AssertUnwindSafe(|| program.verify(run.output, &forged))); + assert!( + matches!(verdict, Ok(Err(_))), + "byte {i} of {n}: tampered and not refused" + ); + } + } + + #[test] + fn a_hidden_final_clock_cannot_carry_a_failure() { + // The forged run of the plain test: the exit's write pulls the tuple it pushes, and its clock flags it. + // + // In zero knowledge the final clock is hidden, its free bits below the live bit: + // + // clock = 2^40 + sum_{5 <= i < 40} b_i 2^i, each b_i a bit + // + // The failure bit 41 has no place in it, so the bus cannot balance and the outer proof fails. + let text = Asm::new().i(Addi, Reg::A0, Reg::ZERO, 42).exit().finish(); + let program = Program::new(&text, Region::TEXT.base(), vec![], 2, 0).expect("valid instruction program"); + let mut forged = program.execute(&[]).unwrap(); + let exit = forged.trace.rows[TableId::ALU] + .iter_mut() + .find(|r| r.index == 2) + .unwrap(); + (exit.prev[2], exit.vd_old) = (exit.ts | 3, exit.out); + let sink = RegisterFile::SINK as usize; + (forged.trace.reg_ts[sink], forged.trace.reg_fin[sink]) = (F64(Clock::SEED_CLOCK), F64::ZERO); + forged.trace.ts_final |= 1 << Clock::FAIL_BIT; + let prover = Prover::new(Rate::MIN).zero_knowledge(Randomness::Fixed([3; 32])); + let (proof, _) = program.prove_execution(&forged, &prover); + // The recorded rows do not hold, so the outer proof's claims are false and the key opening refuses them. + let refused = CpuError::Outer(OuterError::KeyOpening(WhirError::TerminalMismatch)); + assert_eq!(program.verify(forged.output.into(), &proof), Err(refused.into())); + } +} diff --git a/crates/leanvm_core/src/envelope.rs b/crates/leanvm_core/src/envelope.rs index e999f4f02..ec25a0298 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 bytes 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/coord.rs b/crates/leanvm_core/src/leaf/coord.rs index 4c794e328..59ad44cbb 100644 --- a/crates/leanvm_core/src/leaf/coord.rs +++ b/crates/leanvm_core/src/leaf/coord.rs @@ -6,6 +6,7 @@ use fiat_shamir::arith::{Arith, Native}; use pcs::verifier::Recording; use primitives::field::{F64, F192}; use std::sync::{Arc, OnceLock}; +use zk::Recorder; /// One tuple coordinate as a function of the block's row `z`. #[derive(Clone, Debug)] @@ -83,6 +84,8 @@ impl PublicColumns for VerifierState<'_> {} impl PublicColumns for Recording<'_> {} +impl PublicColumns for Recorder {} + impl Coord { /// Whether the coordinate is linear in the columns: it multiplies no column by another. pub fn is_linear(&self) -> bool { diff --git a/crates/leanvm_core/src/leaf/decompose.rs b/crates/leanvm_core/src/leaf/decompose.rs index 56d2cb94f..419956f2a 100644 --- a/crates/leanvm_core/src/leaf/decompose.rs +++ b/crates/leanvm_core/src/leaf/decompose.rs @@ -73,8 +73,14 @@ 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 terms `D_i` of the public half above, for `i < n_terms`, so that it is `sum_i mu_i D_i`. +pub(crate) fn producer_twist_terms(coords: &[Coord], w: &[F192], chi: &[F192], n_terms: usize) -> Vec { let eq = primitives::multilinear::eq_table(chi); - let mut total = F192::ZERO; + let mut terms = vec![F192::ZERO; n_terms]; for (c, &weight) in coords.iter().zip(w) { let Coord::Public(PublicColumn { values: vals, .. }) = c else { continue; @@ -91,14 +97,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/leaf/mod.rs b/crates/leanvm_core/src/leaf/mod.rs index 58ae49970..27fdca52f 100644 --- a/crates/leanvm_core/src/leaf/mod.rs +++ b/crates/leanvm_core/src/leaf/mod.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/lib.rs b/crates/leanvm_core/src/lib.rs index 1f8c844d9..547a80a9e 100644 --- a/crates/leanvm_core/src/lib.rs +++ b/crates/leanvm_core/src/lib.rs @@ -26,6 +26,15 @@ //! //! What a program reads there, it must check itself. //! +//! # Zero knowledge +//! +//! A plain proof hides nothing: a verifier who guesses the advice can recompute the proof and compare. +//! +//! A prover made zero knowledge proves the same statement and reveals nothing of the advice or the run beyond its shape. +//! +//! - The shape is each table's height and the rate. +//! - A program whose advice is private must therefore prove at a fixed public shape. +//! //! # Examples //! //! ```no_run @@ -83,6 +92,7 @@ pub use rec::tree::{ FalseClaim, Kind, Leaf, LeafShape, Part, TableStats, Tier, Tree, TreeError, TreeProof, TreeShape, Unsatisfied, }; pub use rv::{ElfError, ProgramError, Region, Trap, asm}; +pub use zk::Randomness; #[doc(hidden)] pub use crate::pcs::{MAX_MU, MIN_MU}; diff --git a/crates/leanvm_core/src/pcs.rs b/crates/leanvm_core/src/pcs.rs index 7f2426f2e..fb816d29b 100644 --- a/crates/leanvm_core/src/pcs.rs +++ b/crates/leanvm_core/src/pcs.rs @@ -16,6 +16,7 @@ use pcs::verifier::OpeningVerifier; use pcs::whir::WhirError; use pcs::whir::config::ConfigError; use primitives::field::F64; +use rand_core::CryptoRng; use thiserror::Error; pub(crate) use pcs::ring_switch::{RingSwitch, SliceClaim}; @@ -97,6 +98,16 @@ pub(crate) enum WitnessError { }, } +/// The opening's profile: the hiding one for a hiding stack. +fn config(shape: StackShape, rate: Rate) -> Result { + let log_inv_rate = usize::from(rate.log_inv_rate()); + if shape.hiding { + pcs::whir::config_for_rate_hiding(shape.mu, log_inv_rate) + } else { + pcs::whir::config_for_rate(shape.mu, log_inv_rate) + } +} + /// The encoded witness and authentication tree retained for opening. /// /// The caller retains the witness words, avoiding a second full-witness allocation. @@ -122,28 +133,50 @@ impl Committed { shape: StackShape, rate: Rate, ) -> Result { + let config = Self::config(witness.len(), shape, rate)?; + // The codeword and tree use the same parameters retained for opening. + let stack = CommittedStack::new(witness, shape.mu, config); + ps.prover_message(&stack.root()); + Ok(Self { stack, shape }) + } + + /// Encodes a hiding stack and binds its root: the data lanes, then the zero lanes and the random group. + /// + /// The random group and every lane's padding are drawn from `rng`. + /// + /// # Errors + /// + /// As the plain commitment. + pub(crate) fn new_hiding( + ps: &mut ProverState, + witness: &mut [F64], + shape: StackShape, + rate: Rate, + rng: &mut impl CryptoRng, + ) -> Result { + assert!(shape.hiding, "a hiding commitment takes a hiding stack"); + let config = Self::config(witness.len(), shape, rate)?; + let stack = CommittedStack::new_hiding(witness, shape.mu, config, rng); + ps.prover_message(&stack.root()); + Ok(Self { stack, shape }) + } + + /// The opening's configuration, once the shape and the witness's length are checked. + fn config(len: usize, shape: StackShape, rate: Rate) -> Result { // Validate the dimension before shifting lengths or allocating the codeword. - let log_inv_rate = usize::from(rate.log_inv_rate()); - let config = pcs::whir::config_for_rate(shape.mu, log_inv_rate)?; + let config = config(shape, rate)?; let max = 1usize << config.initial_k(); - if !(1..=max).contains(&shape.n_lanes) { + if !(1..=max).contains(&shape.committed_lanes()) { return Err(WitnessError::LaneCount { - n_lanes: shape.n_lanes, + n_lanes: shape.committed_lanes(), max, }); } let expected = shape.committed_len(); - if witness.len() != expected { - return Err(WitnessError::Length { - expected, - got: witness.len(), - }); + if len != expected { + return Err(WitnessError::Length { expected, got: len }); } - - // The codeword and tree use the same parameters retained for opening. - let stack = CommittedStack::new(witness, shape.mu, config); - ps.prover_message(&stack.root()); - Ok(Self { stack, shape }) + Ok(config) } /// Proves the point evaluations and ring-switched circuit-validity claims together. @@ -232,8 +265,8 @@ impl Commitment { rings: &[RingSwitch], ) -> Result<(), WhirError> { // Both sides derive the opening profile from the committed witness's dimension and rate. - let config = pcs::whir::config_for_rate(self.shape.mu, usize::from(self.rate.log_inv_rate()))?; - let stack = StackCommitment::new(self.root, self.shape.mu, self.shape.n_lanes, config); + let config = config(self.shape, self.rate)?; + let stack = StackCommitment::new(self.root, self.shape.mu, self.shape.committed_lanes(), config); stack.verify(v, Statement { points, rings }) } } @@ -268,7 +301,11 @@ mod tests { // Mutation: dimensions outside the configured window, before any shift or codeword allocation. let sizes = [MIN_MU - 1, MAX_MU + 1, usize::MAX].map(|mu| { ( - StackShape { mu, n_lanes: 1 }, + StackShape { + mu, + n_lanes: 1, + hiding: false, + }, 0, WitnessError::Config(ConfigError::SizeOutOfRange { log_n: mu }), ) @@ -276,7 +313,11 @@ mod tests { // Mutation: lane counts outside a leaf and incomplete lane buffers. let lanes = [0, max_lanes + 1, usize::MAX].map(|n_lanes| { ( - StackShape { mu: MIN_MU, n_lanes }, + StackShape { + mu: MIN_MU, + n_lanes, + hiding: false, + }, 0, WitnessError::LaneCount { n_lanes, @@ -286,7 +327,11 @@ mod tests { }); let lengths = [0, lane_words - 1, lane_words + 1].map(|got| { ( - StackShape { mu: MIN_MU, n_lanes: 1 }, + StackShape { + mu: MIN_MU, + n_lanes: 1, + hiding: false, + }, got, WitnessError::Length { expected: lane_words, @@ -310,7 +355,11 @@ mod tests { #[test] fn opening_requires_the_original_committed_length() { // Fixture state: one committed lane, with space for two lanes in the supplied buffer. - let shape = StackShape { mu: MIN_MU, n_lanes: 1 }; + let shape = StackShape { + mu: MIN_MU, + n_lanes: 1, + hiding: false, + }; let lane_words = shape.committed_len(); let witness = vec![F64::ZERO; 2 * lane_words]; let committed = Committed::new( diff --git a/crates/leanvm_core/src/rec/tree/mod.rs b/crates/leanvm_core/src/rec/tree/mod.rs index 57596ea43..37ef1d671 100644 --- a/crates/leanvm_core/src/rec/tree/mod.rs +++ b/crates/leanvm_core/src/rec/tree/mod.rs @@ -365,7 +365,12 @@ impl LeafShape { } /// The shape a proof's first scalars announce, if they are a valid announcement. + /// + /// A zero-knowledge proof has none here: no node verifies one yet. fn announced(proof: &Proof) -> Option { + if proof.is_zero_knowledge() { + return None; + } let mut narg = proof.0.narg.as_slice(); let scalars: [F192; Announcement::LEN] = std::array::from_fn(|_| F192::from_narg(&mut narg).unwrap_or_default()); diff --git a/crates/leanvm_core/src/rec/verifier/riscv.rs b/crates/leanvm_core/src/rec/verifier/riscv.rs index 83ecb3d3a..be8a7d45b 100644 --- a/crates/leanvm_core/src/rec/verifier/riscv.rs +++ b/crates/leanvm_core/src/rec/verifier/riscv.rs @@ -1,7 +1,7 @@ //! The verifier's core of one RISC-V proof, in rows: every check that depends on the proof. use super::{Rows, infallible}; -use crate::cpu::{Announcement, CpuError, DeferredClaims, Layout, Program}; +use crate::cpu::{Announcement, CpuError, DeferredClaims, Layout, Program, ProofKind}; use crate::pcs::Rate; use crate::rec::circuit::{Builder, Dw, Ew, Kw}; use crate::rec::transcript::{ProofSource, Transcript}; @@ -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, ProofKind::Plain)?; Ok(Self { program, taus, diff --git a/crates/leanvm_core/src/rec/verifier/tests.rs b/crates/leanvm_core/src/rec/verifier/tests.rs index 336bbbafd..52c59f1b2 100644 --- a/crates/leanvm_core/src/rec/verifier/tests.rs +++ b/crates/leanvm_core/src/rec/verifier/tests.rs @@ -2,7 +2,9 @@ use super::recursion::RecRows; use super::{ProofShape, RecShape, Rows, infallible}; use crate::class_flock::FlockId; use crate::constraints::ConstraintError; -use crate::cpu::{CpuError, DeferredClaims, Output, Program, Proof, ProvenRun, Prover, UNGROUND_LOG_BYTECODE}; +use crate::cpu::{ + CpuError, DeferredClaims, Output, Program, Proof, ProofKind, ProvenRun, Prover, UNGROUND_LOG_BYTECODE, +}; use crate::leaf::BusError; use crate::pcs::{Commitment, Committed, Rate, RingSwitch, SliceClaim, StackClaim}; use crate::rec::RecError; @@ -103,7 +105,7 @@ impl Fixture { let messages: Vec = (0..(self.proof.narg.len() - FLOCK_START) / 24).collect(); FLOCK_START + 24 * messages.partition_point(|&m| { - let mut prefix = Proof(self.proof.clone()); + let mut prefix = Proof(self.proof.clone(), ProofKind::Plain); prefix.0.narg.truncate(FLOCK_START + 24 * m); matches!( self.program.verify_core(self.output, &prefix), @@ -615,7 +617,11 @@ fn check_opening(mu: usize, log_inv_rate: u8, seed: u64) { let what = format!("mu {mu}, log_inv_rate {log_inv_rate}"); let rate = Rate::new(log_inv_rate).expect("a supported rate"); let mut rng = Rng::new(seed); - let shape = StackShape { mu, n_lanes: N_LANES }; + let shape = StackShape { + mu, + n_lanes: N_LANES, + hiding: false, + }; let q: Vec = (0..shape.committed_len()).map(|_| F64(rng.next_u64())).collect(); let (slots, rings) = opening_claims(mu, &q, &mut rng); diff --git a/crates/leanvm_core/src/witness.rs b/crates/leanvm_core/src/witness.rs index 290e1d5f0..424231c5a 100644 --- a/crates/leanvm_core/src/witness.rs +++ b/crates/leanvm_core/src/witness.rs @@ -100,19 +100,53 @@ 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's stack is hiding: after its data lanes come zero lanes, then the uniform random group. #[derive(Clone, Copy, Debug)] pub struct StackShape { pub mu: usize, pub n_lanes: usize, + pub hiding: bool, } impl StackShape { - /// Words actually committed: the placed columns rounded up to a whole lane. + /// The lanes committed: the data's, then for a hiding stack the zero lanes and the random group. + pub const fn committed_lanes(&self) -> usize { + if self.hiding { + pcs::whir::hiding_lanes(self.n_lanes) + } else { + self.n_lanes + } + } + + /// Words actually committed: the placed columns rounded up to a whole lane, then a hiding stack's extra lanes. 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 hiding stack of `placed` words. + /// + /// - It is at least the hiding opening's smallest size. + /// - It grows until its data lanes, the zero lanes and the random group fit the lanes a commitment holds. + pub fn hiding(placed: usize) -> Self { + let lanes = 1usize << crate::pcs::LOG_BATCH; + let mut mu = primitives::log2_ceil_usize(placed.max(1)) + .max(crate::pcs::MIN_MU) + .max(pcs::whir::MIN_LOG_N_HIDING); + loop { + let n_lanes = placed.div_ceil(1 << (mu - crate::pcs::LOG_BATCH)).max(1); + if pcs::whir::hiding_lanes(n_lanes) <= lanes { + return Self { + mu, + n_lanes, + hiding: true, + }; + } + mu += 1; + } } } @@ -186,7 +220,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, + hiding: false, + }, + ) } /// Chunk width for the bulk writes below: big enough to amortize the dispatch,