Author leanVM circuits in Clean, prove them, and export them to Rust

.github/workflows/clean-circuits.yml

@@ -0,0 +1,80 @@
+name: Clean circuits
+
+on:
+  pull_request:
+    paths:
+      - verification/circuits/**
+      - crates/flock/src/clean.rs
+      - crates/leanvm_core/src/rec/clean.rs
+      - crates/leanvm_core/src/tables/clean.rs
+      - .github/workflows/clean-circuits.yml
+      - rustfmt.toml
+  push:
+    branches: [riscv-exploration, 'kw/clean-circuits-*']
+    paths:
+      - verification/circuits/**
+      - crates/flock/src/clean.rs
+      - crates/leanvm_core/src/rec/clean.rs
+      - crates/leanvm_core/src/tables/clean.rs
+      - .github/workflows/clean-circuits.yml
+      - rustfmt.toml
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  export:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: dtolnay/rust-toolchain@stable
+        with:
+          toolchain: 1.97.0
+          components: rustfmt
+      - uses: leanprover/lean-action@v1
+        with:
+          lake-package-directory: verification/circuits
+          build: 'false'
+          test: 'false'
+          lint: 'false'
+          use-mathlib-cache: 'false'
+      - name: Check source, lowering, artifact, and theorem axioms
+        working-directory: verification/circuits
+        run: |
+          lake exe cache get Mathlib.Tactic Mathlib.FieldTheory.Finite.Extension Mathlib.RingTheory.AdjoinRoot Mathlib.Algebra.Polynomial.SpecificDegree Mathlib.Algebra.MvPolynomial.Eval Mathlib.Algebra.Polynomial.Roots
+          # Keep the kernel-reduced multiplier plan and its export out of concurrent heavy builds.
+          lake build LeanVMCircuits.Multiply.Checked
+          lake build LeanVMCircuits.MulDivExport
+          lake build
+          lake env lean Audit.lean
+          test -f .lake/build/lib/lean/LeanVMCircuits.olean
+          # Stock leanchecker replays every matching module concurrently.
+          # The root has no declarations; reject any future declaration there.
+          if grep -nEv '^[[:space:]]*(module|public import LeanVMCircuits[.][A-Za-z0-9_.]+)?[[:space:]]*$' LeanVMCircuits.lean; then
+            echo "::error::LeanVMCircuits.lean must contain only its module header and public imports"
+            exit 1
+          fi
+          shopt -s globstar nullglob
+          sources=(LeanVMCircuits/**/*.lean)
+          if (( ${#sources[@]} == 0 )); then
+            echo "::error::No library source modules found for kernel checking"
+            exit 1
+          fi
+          for source in "${sources[@]}"; do
+            module="${source%.lean}"
+            if [[ ! -f ".lake/build/lib/lean/${module}.olean" ]]; then
+              echo "::error::Missing compiled library module ${module}"
+              exit 1
+            fi
+            lake env leanchecker "${module//\//.}"
+          done
+      - name: Check deterministic production export
+        working-directory: verification/circuits
+        run: |
+          lake env lean --run Generate.lean /tmp/clean-generated.rs
+          diff -u ../../crates/flock/src/clean.rs /tmp/clean-generated.rs
+          lake env lean --run GenerateRec.lean /tmp/rec-generated.rs
+          diff -u ../../crates/leanvm_core/src/rec/clean.rs /tmp/rec-generated.rs
+          lake env lean --run GenerateTables.lean /tmp/tables-generated.rs
+          diff -u ../../crates/leanvm_core/src/tables/clean.rs /tmp/tables-generated.rs

.github/workflows/rec-builder-model.yml

@@ -0,0 +1,47 @@
+name: Recursion builder model
+
+# The Lean model of the recursion circuit's builder (verification/circuits/LeanVMCircuits/Rec/Builder.lean)
+# replays the builder calls that make each tracked aggregation tree's circuits and checks it builds the same
+# circuits. Any Rust change can change what the verifier in rows calls, so every one runs it.
+
+on:
+  pull_request:
+    paths:
+      - crates/**
+      - bins/leanvm/**
+      - programs/**
+      - Cargo.toml
+      - Cargo.lock
+      - verification/circuits/**
+      - .github/workflows/rec-builder-model.yml
+  push:
+    branches: [riscv-exploration, 'kw/clean-circuits-*']
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  replay:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: dtolnay/rust-toolchain@stable
+        with:
+          toolchain: 1.97.0
+      - uses: leanprover/lean-action@v1
+        with:
+          lake-package-directory: verification/circuits
+          build: 'false'
+          test: 'false'
+          lint: 'false'
+          use-mathlib-cache: 'false'
+      - name: Dump the tracked circuits and instruction table bindings
+        run: cargo run --release -p leanvm-cli --features circuits -- circuits /tmp/circuits
+      - name: Replay the builders and check native table bindings
+        working-directory: verification/circuits
+        run: |
+          lake exe cache get Mathlib.Tactic Mathlib.FieldTheory.Finite.Extension Mathlib.RingTheory.AdjoinRoot Mathlib.Algebra.Polynomial.SpecificDegree Mathlib.Algebra.MvPolynomial.Eval Mathlib.Algebra.Polynomial.Roots
+          lake build checkrec checkflushes
+          lake exe checkrec /tmp/circuits/*.txt
+          lake exe checkflushes /tmp/circuits/table-flushes.dump

.gitignore

@@ -3,3 +3,4 @@ target
 __pycache__/
 formal/
 conformance/act4/elf/
+verification/circuits/.lake/

AGENTS.md

@@ -5,7 +5,7 @@
 A RISC-V (rv64im) virtual machine and the SNARK that proves its execution. Proofs are not zero knowledge. Every rv64im instruction is proven, plus custom ones: the BLAKE2s compression (`blake2s rs1, rs2`) and the multiplication in the extension field `E = GF(2^192)` (`extmul`, `extmac`, `extmulk`, `extmack`, each `rd, rs1, rs2` with every register an address). A program is a guest's ELF file (`programs/<name>/guest`, Rust built for `riscv64im-unknown-none-elf`, loaded by `rv::Guest::from_elf`) or a text assembled by hand with `leanvm::asm`; a run is proven on an advice (a region of memory the prover fills), and its statement is the program's digest and the output (`a0..a3` at `exit`); there is no public input. One run is one proof: a run whose witness exceeds one commitment (`pcs::MAX_MU`) is refused up front with `ProveError::TooLong` (re-exported as `leanvm::ProveError::TooLong`), continuations being unimplemented.
 
 - `doc/leanvm/` is the LaTeX project describing the machine ISA and the snark that proves it. Its root is `doc/leanvm/main.tex`; build it with `cd doc/leanvm && latexmk -pdf main.tex`, which writes to the gitignored `doc/leanvm/.build/`. Sections live in `doc/leanvm/body/`, numbered `01`..`08` plus the lettered annexes `a` (ring switching), `b` (the PCS), `c` (Flock), `d` (novel basis and additive NTT), and `e` (recursion), and every symbol is defined once in `doc/leanvm/preamble/macros.tex`. If latexmk fails oddly (a bibtex error, or a missing `main.log`) right after inputs are renamed or `refs.bib` is edited, remove `doc/leanvm/.build` and rerun; it has not reproduced on unchanged inputs. **Drafting one section:** each section file carries a `% !TeX root` comment pointing at its generated driver in `doc/leanvm/drafts/`, so the LaTeX build key (`F5`, or the extension's `cmd+alt+b`) compiles only that section, numbered as in the full document and with cross-references and citations resolved against `.build/main.aux`; in `main.tex` the same key builds everything. Run `doc/leanvm/make-drafts.sh` after adding, renaming or renumbering a section.
-- The one hash function is BLAKE2s, in `primitives::hash`: scalar, streaming, and a lane-transposed batched form for the PCS Merkle tree. The VM's compression instruction is the generic gate-list circuit in `rv::semantics::hash` (`Class::Hash.circuit()`), proven like every other class; its witness is word arithmetic in `rv::semantics::hash` (exported as `rv::circuits::blake2s_witness`), pinned to the walk of the gate list by a test.
+- The one hash function is BLAKE2s, in `primitives::hash`: scalar, streaming, and a lane-transposed batched form for the PCS Merkle tree. The VM's compression instruction is the generic gate-list circuit in `rv::semantics::hash` (`Class::Hash.circuit()`), proven like every other class; its gate list is `flock::clean::blake2s`, generated from the Clean circuit `LeanVMCircuits.Blake2s.Compress` (proven to be RFC 7693's compression, `verification/circuits/README.md`), and its witness is word arithmetic in `rv::semantics::hash` (exported as `rv::circuits::blake2s_witness`), pinned to the walk of the gate list by a test.
 
 ## Layout
 

README.md

@@ -32,6 +32,8 @@ leanVM is designed for security:
 
 **warning**: Formal verification is [in progress](https://github.com/Verified-zkEVM/leanerVM). leanVM is not (yet) production ready.
 
+The production wrapping and carry adders and the complete RV shift circuit are authored and proved in [Clean](./verification/circuits/README.md), then exported as checked-in Rust gates. Real instruction and BLAKE2s circuits consume the adder family; real RV shifts consume the complete shift artifact. The proofs cover arbitrary-witness Boolean constraint soundness and honest completeness, with the shift flag domain made explicit. The Rust interpretation and the separate cryptographic composition retain the trust boundaries documented there.
+
 ## work in progress
 
 Expect leanVM to change significantly:

bins/leanvm/Cargo.toml

@@ -18,6 +18,8 @@ workspace = true
 [features]
 # The system allocator in place of `bench::Jemalloc`, still under `bench::Counting`, for heap profilers that hook `malloc` (heaptrack). Slower: for memory questions only.
 system-alloc = []
+# `circuits`: the tracked trees' recursion circuits with the builder calls that make them, for `checkrec`.
+circuits = ["leanvm/circuit-trace"]
 
 [dependencies]
 leanvm.workspace = true

bins/leanvm/src/main.rs

@@ -147,6 +147,11 @@ enum Command {
         #[arg(long, conflicts_with = "cycles_only")]
         only: Option<String>,
     },
+    /// Write the tracked aggregation circuits and instruction table bindings (with `--features circuits`) for the Lean checkers.
+    Circuits {
+        /// The directory to write them to.
+        out: PathBuf,
+    },
 }
 
 fn parse_rate(log_inv_rate: &str) -> Result<Rate, Box<dyn Error + Send + Sync>> {
@@ -179,15 +184,15 @@ fn refuse(what: Arguments) -> ! {
 fn main() {
     let cli = Cli::parse();
     let fixed_threads = match &cli.command {
-        Command::Bench { cycles_only: true, .. } => false,
+        Command::Bench { cycles_only: true, .. } | Command::Circuits { .. } => false,
         Command::Bench { only, .. } => only.as_deref().is_some_and(|name| name.ends_with("-16thread")),
         _ => std::env::var_os("LEANVM_NUM_THREADS").is_none(),
     };
     if fixed_threads {
         parallel::init_with_threads(NonZeroUsize::new(16).unwrap())
             .unwrap_or_else(|actual| refuse(format_args!("cannot configure 16 benchmark threads: {actual:?}")));
     }
-    if !matches!(cli.command, Command::Bench { .. }) || fixed_threads {
+    if !matches!(cli.command, Command::Bench { .. } | Command::Circuits { .. }) || fixed_threads {
         let topology = parallel::topology();
         eprintln!(
             "Benchmark pool: {} threads ({} performance, {} efficiency)",
@@ -232,5 +237,9 @@ fn main() {
             &prover,
             plan,
         ),
+        #[cfg(feature = "circuits")]
+        Command::Circuits { out } => tracked::dump(&out, leaf_prover.rate(), prover.rate()),
+        #[cfg(not(feature = "circuits"))]
+        Command::Circuits { .. } => refuse(format_args!("`circuits` needs `--features circuits`")),
     }
 }

bins/leanvm/src/tracked.rs

@@ -19,6 +19,8 @@
 use crate::refuse;
 use crate::workload::{Items, Workload};
 use bench::{Heap, Metric, Plan, Timing, bencher_json};
+#[cfg(feature = "circuits")]
+use leanvm::aggregate::{Capacity, ClaimShape, Tier};
 use leanvm::aggregate::{CircuitStats, Kind, Leaf, LeafShape, Tree, TreeError, TreeProof, TreeShape};
 use leanvm::{Output, ProvenRun, Prover, Rate, Stats};
 use primitives::pretty_integer;
@@ -340,6 +342,60 @@ fn circuits(tree: &Aggregation, leaf_rate: Rate, rate: Rate) -> [(Kind, CircuitS
     Kind::ALL.map(|kind| (kind, built.stats(kind)))
 }
 
+/// Write every tracked output-tree circuit and claim-set tier position, plus native instruction table bindings.
+///
+/// CI's `rec-builder-model` workflow replays the recorded builders and checks the table slot and clock-port bindings against their Lean sources.
+#[cfg(feature = "circuits")]
+pub fn dump(out: &Path, leaf_rate: Rate, rate: Rate) {
+    let proven = [
+        Aggregation::new("aggregate-leanxmss-100-2to1", Workload::leanxmss(100), 2, 2),
+        Aggregation::new("aggregate-leanxmss-100-4to1", Workload::leanxmss(100), 4, 4),
+    ];
+    std::fs::create_dir_all(out).unwrap_or_else(|e| refuse(format_args!("{}: {e}", out.display())));
+    let path = out.join("table-flushes.dump");
+    std::fs::write(&path, leanvm::table_flushes()).unwrap_or_else(|e| refuse(format_args!("{}: {e}", path.display())));
+    for tree in counted_trees().into_iter().chain(proven) {
+        let shape = LeafShape::measured(&tree.leaf.measure(), leaf_rate);
+        let built = tree.tree(shape, rate);
+        for position in 0..built.circuit_count() {
+            let kind = if position == 0 { Kind::First } else { Kind::Node };
+            let path = out.join(format!("{}.txt", tree.node(kind).0));
+            std::fs::write(&path, built.circuit_dump(position))
+                .unwrap_or_else(|e| refuse(format_args!("{}: {e}", path.display())));
+        }
+    }
+    let leaf = Workload::leanxmss(100);
+    let measured = LeafShape::measured(&leaf.measure(), leaf_rate);
+    let capacity = Capacity { claims: 12, groups: 4 };
+    for (name, claims) in [
+        ("claimset-single-tier", ClaimShape::new(capacity)),
+        (
+            "claimset-two-tier",
+            ClaimShape {
+                capacity,
+                small: Some(Tier {
+                    arity: 2,
+                    capacity: Capacity { claims: 5, groups: 2 },
+                }),
+            },
+        ),
+    ] {
+        let shape = TreeShape {
+            leaf: measured,
+            arity_0: 1,
+            arity: 3,
+            rate,
+            claims: Some(claims),
+        };
+        let built = Tree::new(&leaf.program, shape).unwrap_or_else(|e| refuse(format_args!("{name}: {e}")));
+        for position in 0..built.circuit_count() {
+            let path = out.join(format!("{name}-circuit-{position}.txt"));
+            std::fs::write(&path, built.circuit_dump(position))
+                .unwrap_or_else(|e| refuse(format_args!("{}: {e}", path.display())));
+        }
+    }
+}
+
 /// `rows` (the circuit's own), `proven-rows` (the tables' heights, powers of two) and
 /// `committed` (the witness words): exact, the same on every machine.
 fn circuit_counts(stats: &CircuitStats) -> Vec<(&'static str, Metric)> {