Portable, single-threaded native verifier

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, with `hash::portable` the RFC's code alone, which the native verifier and the streaming `Hasher` (the program and tree digests) take. A transcript hashes by its `fiat_shamir::Hashing` backend, `Native` for the prover and `Portable` for the native verifier, the same bytes either way. 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.
 
 ## Layout
 
@@ -226,7 +226,7 @@ The opening's weight is never stored: the first WHIR pass fills it one chunk at
 
 No rayon. Every parallel site is "N independent items, each writing its own disjoint slice", so the pool is a claim counter, not a work-stealing deque: `NUM_THREADS-1` workers plus the dispatcher inline, and a dispatch allocates nothing (a reduction allocates its per-worker slots once per call, the slot type being the caller's). Primitives: `for_each{,_chunk}`, `chunks_mut{,2,_zip}`, `ChunkView`, `fill`, `map_collect`, `map_reduce`, `fold_reduce`, `map_reduce_with_state`, `find_first`, `SendPtr`.
 
-- **Nested dispatch panics**, because it would deadlock the dispatch lock.
+- **Nested dispatch panics**, because it would deadlock the dispatch lock. So does any dispatch while a `parallel::serial()` guard lives, whatever the pool's size: the native verifier holds one.
 - **Both core clusters share one queue** (P at `USER_INTERACTIVE`, E at `UTILITY`); guided self-scheduling means a slow core claims fewer batches. Do not add a second pool: that was `primitives::epool`, now deleted.
 - **The default holds back one performance worker when efficiency workers exist.**
 
@@ -238,6 +238,8 @@ Ring-switch claims' weights are built by `ring_switch::DeferredWeight::batch`, w
 
 The native verifier (`leanvm::cpu::Program::verify`) and the recursive verifier (`leanvm::rec::verifier`) run the same core over `fiat_shamir::arith`. `Arith` and `Verifier` execute natively over `VerifierState` or build rows over the circuit builder and the in-circuit transcript. The shared core covers GKR, bus decomposition, the table sumcheck, the program claim, flock reductions, and the opening over `pcs::verifier::OpeningVerifier`. `Verifier::scope` names a stage under which the rows report a failed check. `rec::verifier::tests` checks that the rows leave the native `DeferredClaims` value for value and that forged proofs fail at the expected stage.
 
+**The native verifier is portable and single-threaded, always.** It runs on the calling thread with no SIMD intrinsic, no inline assembly and no pool dispatch, so it computes the same way on every target; correctness and simplicity matter more than its speed. Its backend is `fiat_shamir::arith::Portable`: its arithmetic the `*_portable` field methods, its hashing (`fiat_shamir::Hashing`: the duplex and proof of work; `pcs::merkle::MerkleHashing`: Merkle openings) `primitives::hash::portable`. `VerifierState<'_, A>` computes and hashes by its backend; the public entry points fix it to `Portable`, and a prover replaying what it is handed (`Program::verify_recording` and `rec::proof::CircuitKey::verify`, over `pcs::verifier::Recording`) runs it on `Native`, which nothing trusts but the proof it feeds. Nothing the prover runs takes the portable code, apart from setup both sides compute once (session identifiers, the program and tree digests). A constant the verifier needs is a `const` computed by the portable products (`SkipDomain`, the zerocheck's medium challenges, the ring switch's roots of `x`), or is built by them (`pcs::ntt::NovelBasis`). Every public native entry point (`Program::verify`, `verify_core`, `check_deferred`, `Tree::verify`, `Tree::verify_claims`), a zero-knowledge leaf's (its recorder and `zk::KeyCommitment::verify_outer` included) and a tree's over zero-knowledge leaves alike, holds a `primitives::portable::Section`: a dispatch inside it panics always, and under `primitives`' `guard` feature, which the CLI's dev-dependencies turn on so that `cargo testall` arms it while no benchmark build pays for it, so does every SIMD or assembly kernel. So verifier code never calls a dispatching helper (`F192 * F192`, `mle_eval_par`, `multilinear::eq_table`, `hash::hash`): write it over `Arith` and `Hashing` and run it on `Portable`. The CLI's `verification_is_portable_and_single_threaded` checks the guard is armed, and `the_public_verifier_is_the_portable_one` that a `Native` replay is refused where the public verifier passes.
+
 Verification has two parts: `verify_core` checks the proof and returns claims on polynomials fixed by the program or the VM's circuits (`cpu::DeferredClaims`); `check_deferred` evaluates those claims. A recursive verifier carries them out of the proof instead of evaluating them. A caller of `verify_core` must never drop them. `check_deferred` refuses malformed claims with `CpuError::MalformedClaim`, never a panic. The recursion machine reads the very proof the native verifier accepted, with every Merkle opening that verifier authenticated (`rec::transcript::ProofSource::Proof(proof, openings)`): the prover verifies a leaf with `cpu::Program::verify_recording` and a child with `rec::proof::CircuitKey::verify`, both over `pcs::verifier::Recording`, so each hint is decoded and hashed once, natively, and the rows take its full paths (`pcs::merkle::Openings`, flat buffers) as free wires.
 
 Query positions are stratified (`pcs::whir::Stratum::batch`, Annex B's `def:strata`): each binary digit of the query count is a group whose `j`-th query has its top bits fixed to `j`. This keeps the i.i.d. query bound and lets the rows hash the top subtree once and each query's path only below it (`rec::verifier::Rows::authenticate`). Native and recursive verification share the WHIR configuration and its integer level ladder, so no floating point reaches a proof. The floating-point soundness derivation is test-only (`pcs::whir::config::tests`): `the_table_is_the_derivation` pins `WHIR_QUERIES` to it. Changing a constant the derivation reads (the security target, a folding factor, the grinding bits, the size window) fails that test, whose message holds the replacement rows for the Rust table. Moving the size window also changes the table's type: give each rate that many rows first (`&[]` will do) so that `pcs` compiles.

bins/leanvm/Cargo.toml

@@ -37,3 +37,7 @@ tracing.workspace = true
 clap = { version = "4", features = ["derive"] }
 # The pinned cases' benchmarks, merged with this process's.
 serde_json = "1"
+
+[dev-dependencies]
+# Arms the portable verifier's guard in every workspace test build (`primitives::portable`), and in no benchmark's.
+primitives = { workspace = true, features = ["guard"] }

bins/leanvm/src/workload.rs

@@ -236,7 +236,9 @@ impl Workload {
 #[cfg(test)]
 mod tests {
     use super::*;
-    use leanvm::Rate;
+    use leanvm::aggregate::{Capacity, ClaimGroup, ClaimLeaf, ClaimSet, ClaimShape, Leaf, LeafShape, Tree, TreeShape};
+    use leanvm::asm::Ld;
+    use leanvm::{Proof, Randomness, Rate};
 
     #[test]
     fn the_workloads_prove() {
@@ -263,4 +265,120 @@ mod tests {
             assert_eq!(stats.proven_rows, exec.proven_rows, "{}", workload.title);
         }
     }
+
+    /// Verification is portable and single-threaded: every native verifier holds a `primitives::portable::Section`, in
+    /// which this crate's tests (the `guard` feature) make a pool dispatch and every SIMD or assembly kernel panic.
+    /// A verifier that reached either fails here, and so does a guard that stopped refusing them.
+    #[test]
+    fn verification_is_portable_and_single_threaded() {
+        const { assert!(primitives::portable::GUARDED, "the CLI's tests arm the guard") };
+        let refused = |f: fn()| {
+            std::panic::catch_unwind(|| {
+                let _portable = primitives::portable::enter();
+                f();
+            })
+            .is_err()
+        };
+        assert!(refused(|| parallel::for_each(1, |_| {})));
+        #[cfg(any(
+            all(target_arch = "x86_64", target_feature = "pclmulqdq"),
+            all(target_arch = "aarch64", target_feature = "aes")
+        ))]
+        assert!(refused(|| {
+            let y = std::hint::black_box(primitives::field::F192::Y);
+            std::hint::black_box(y * y);
+        }));
+        #[cfg(target_arch = "x86_64")]
+        assert!(refused(|| _ = std::hint::black_box(hash(b"leanvm"))));
+
+        // A leaf proof, a tampered copy of it, a two-leaf tree over it, the same over a zero-knowledge leaf, and a claim-set
+        // root, each verified in the guard.
+        let leaf = Workload::fibonacci(1_000);
+        let prover = Prover::new(Rate::MIN);
+        let proved = leaf.prove(&prover);
+        leaf.program
+            .verify(proved.output, &proved.proof)
+            .expect("an honest proof");
+        let mut bytes = proved.proof.to_bytes();
+        let middle = bytes.len() / 2;
+        bytes[middle] ^= 1;
+        if let Ok(tampered) = Proof::from_bytes(&bytes) {
+            assert!(leaf.program.verify(proved.output, &tampered).is_err());
+        }
+        let shape = TreeShape {
+            leaf: LeafShape::measured(&leaf.measure(), Rate::MIN),
+            arity_0: 2,
+            arity: 2,
+            rate: Rate::MIN,
+            claims: None,
+        };
+        let tree = Tree::new(&leaf.program, shape).expect("a tree");
+        let root = tree
+            .prove(&[Leaf::new(&proved.proof, proved.output); 2])
+            .expect("honest leaves");
+        tree.verify(&root, &[proved.output; 2]).expect("the root");
+        assert!(tree.verify(&root, &[proved.output, Output::new([1, 2, 3, 4])]).is_err());
+
+        // A zero-knowledge leaf, its outer proof included, and a tree over two of them.
+        let hidden = leaf.prove(&prover.zero_knowledge(Randomness::Fixed([3; 32])));
+        leaf.program
+            .verify(hidden.output, &hidden.proof)
+            .expect("an honest zero-knowledge proof");
+        let mut bytes = hidden.proof.to_bytes();
+        let middle = bytes.len() / 2;
+        bytes[middle] ^= 1;
+        if let Ok(tampered) = Proof::from_bytes(&bytes) {
+            assert!(leaf.program.verify(hidden.output, &tampered).is_err());
+        }
+        let shape = TreeShape {
+            leaf: LeafShape::of(&hidden.proof).expect("a canonical announcement"),
+            arity_0: 2,
+            arity: 2,
+            rate: Rate::MIN,
+            claims: None,
+        };
+        let tree = Tree::new(&leaf.program, shape).expect("a tree");
+        let root = tree
+            .prove(&[Leaf::new(&hidden.proof, hidden.output); 2])
+            .expect("honest zero-knowledge leaves");
+        tree.verify(&root, &[hidden.output; 2]).expect("the root");
+
+        // A leaf that outputs its advice, the hash of its set's digest, after a loop that reads every framework block.
+        let text = Asm::new()
+            .li(Reg::T0, Region::ADVICE.base())
+            .load(Ld, Reg::A0, 0, Reg::T0)
+            .load(Ld, Reg::A1, 8, Reg::T0)
+            .load(Ld, Reg::A2, 16, Reg::T0)
+            .load(Ld, Reg::A3, 24, Reg::T0)
+            .li(Reg::T1, 9)
+            .label("loop")
+            .i(Addi, Reg::T1, Reg::T1, -1)
+            .branch(Bne, Reg::T1, Reg::ZERO, "loop")
+            .exit()
+            .finish();
+        let program = Program::new(&text, Region::TEXT.base(), vec![3, 5], 2, 2).expect("a valid program");
+        let set = ClaimSet {
+            groups: vec![ClaimGroup {
+                label: [1, 9, 0, 0, 0, 1],
+                members: vec![[1, 8, 1 << 9, 0x5eed ^ 1]],
+            }],
+        };
+        let words: Vec<u8> = set.digest().iter().flat_map(|w| w.to_le_bytes()).collect();
+        let run = (prover.prove(&program, &digest_words(&hash(&words)))).expect("the run halts");
+        let shape = TreeShape {
+            leaf: LeafShape::of(&run.proof).expect("a canonical announcement"),
+            arity_0: 1,
+            arity: 3,
+            rate: Rate::MIN,
+            claims: Some(ClaimShape {
+                capacity: Capacity { claims: 12, groups: 4 },
+                small: None,
+            }),
+        };
+        let tree = Tree::new(&program, shape).expect("a tree");
+        let first = (tree.aggregate_leaves(&[ClaimLeaf::new(Leaf::new(&run.proof, run.output), &set)], None))
+            .expect("an honest leaf");
+        tree.verify_claims(&first.proof, &first.claims).expect("the root");
+        assert!(tree.verify_claims(&first.proof, &ClaimSet { groups: vec![] }).is_err());
+    }
 }