leanvm: zero-knowledge leaf proofs

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 {

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<F192> {
+        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.

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

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.