cleanup: dead code, duplication and comment slop across the workspace

A review pass over every crate, then applied per crate. Net -2.9k lines
(95 files, +3585/-7523, of which 1036 lines moved into three new files
rather than disappearing).

Removed: unused pub items, fields and enum variants; superseded kernels
and benchmark-only variants; write-only accumulators and debug
scaffolding; a dead compiler macro and a never-called guest function the
compiler was lowering into the bytecode regardless.

Deduplicated: eight copies of the OOD/fold transcript replay in ligerito;
prover/verifier `_base`/`_ext` function pairs behind small traits; the
four `memory*` flush builders; `col_kappas`, now derived from
`col_kappa_sources` instead of hand-maintained alongside it; two
compile-time integer evaluators in the parser; and fifteen hand-rolled
test PRNGs, now one helper over `rand::StdRng` behind a `test-util`
feature so `rand` stays out of the production graph.

Split `ligerito.rs` (4150 lines) into itself plus `ligerito_ntt_ext.rs`
and `ligerito_induce.rs`.

Tests: deleted those that restate a constructor or call a pure function
twice, and folded standalone tamper tests into the table that already
runs at two sizes. Ported the one uncovered case out of a deleted
program first.

Behavior is unchanged and pinned as such: bytecode byte-identical for
all test programs and both guests, proof wire format byte-identical,
FAMILY_DIGEST unchanged, guest cycles unchanged.

Three hot paths are deliberately left duplicated, with comments saying
so, because merging them cost measurable time: the per-arch inv_table
SIMD kernels (a trait stopped them inlining into flock under thin LTO,
worth 2.3%), the interpreter's memory accessors, and `table_message`.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Author: TomWambsgans

AGENTS.md

@@ -25,7 +25,7 @@ Dependency order, leaves first:
 | `flock`           | batched R1CS over GF(2) for BLAKE3: zerocheck + lincheck               |
 | `lean_vm`         | arithmetization: tables, bus, constraints, `cpu::prove`/`verify`       |
 | `lean_compiler`   | zkDSL (Python subset) → ISA                                            |
-| `xmss`            | XMSS over BLAKE3                     |
+| `xmss`            | XMSS over BLAKE3; an independent leaf, consumed only by `rec_aggregation` |
 | `rec_aggregation` | the three workloads + the N→1 recursion harness                        |
 
 `src/main.rs` is the CLI; guests are zkDSL under `crates/rec_aggregation/guests/`.
@@ -36,12 +36,12 @@ Dependency order, leaves first:
 - always run in `--release` mode any test or benchmark touching the VM (the zkDSL compiler stack-overflows in `debug` mode)
 
 ```bash
-cargo testall                     # = test --all --release; 314 tests, seconds
+cargo testall                     # = test --all --release; whole suite in seconds
 cargo clippy --release --all-targets
 cargo fmt --all                   # max_width = 120
 ```
 
-Heavy benches are `#[ignore]`d; run by name with `-- --ignored --nocapture` (`blake3_batch`, `pcs_throughput`, `recursion_soundness_binds`, `recursion_generic_many`).
+Heavy benches and measurement harnesses are `#[ignore]`d; run by name with `-- --ignored --nocapture`: `blake3_batch_prove_verify`, `pcs_throughput`, `recursion_soundness_binds`, `recursion_generic_many`, `recursion_guest_profile`, `print_ligerito_query_counts`, `encoding_grinding_bits`.
 
 ## Benchmarking
 
@@ -84,15 +84,22 @@ The third is worth understanding before touching the verifier. `guests/recursion
 
 ## Conventions that bite
 
+- Use comments only when necessary: uncommented but readable and simple code is better than commented slop.
+- Commit tests only that are useful in the future, to prevent regressions / failures. Don't add trivial tests that will always pass.
+- Simpler is better.
 - **Fiat-Shamir:** `add_scalar`/`next_scalar` bind into the sponge as a side effect. `observe_*` is only for the public statement. Never re-observe data that rode the stream, which silently desynchronizes the two sides.
-- **Prover and verifier derive the layout identically** from announced sizes. Changes to `placements_of`, `col_kappas` or the schema land on both sides, and `col_kappa_sources` stays in lockstep with `col_kappas`.
+- **Prover and verifier derive the layout identically** from announced sizes. Changes to `placements_of` or the schema land on both sides. `col_kappas` is derived from `col_kappa_sources` rather than written out twice, so the two can no longer drift; keep it that way.
 - **A failed guest `assert` surfaces as a write-once memory conflict**, not an assertion message, so disassemble around the reported `pc` (`DBG_DISASM`).
 - Guests are single-file; the compiler skips `from snark_lib import *`, which exists only so editors accept the file as Python.
 - **One symbol, one meaning, across the whole document.** All notation is defined in `doc/preamble/macros.tex`; define a new macro there rather than inline, and check the letter is free first. Annex B's symbols were deliberately renamed away from the letters WHIR/Ligerito/BCHKS25 use (rate is `\rate`, not `\rho`, which is a sumcheck point) and its "Symbols" table is the map back, so reintroducing a paper's letter silently collides with the main matter.
 - **Doc labels are an API.** `crates/pcs` cites `thm:rbr` and `thm:mca-johnson` by name and several crates cite `doc/main.tex` sections, so renaming a label breaks those pointers with nothing to catch it. `doc/body/NN-*.tex` prefixes match section numbers, so inserting a section renumbers the rest.
 - **No em-dashes or en-dashes in prose**, anywhere a human reads it: docs, LaTeX, comments, commit messages. Restructure with a comma, colon, parentheses, or two sentences.
 - **Never hard-wrap prose in Markdown or LaTeX.** One paragraph is one line; let the editor wrap it. Artificial line breaks make every later edit a reflow, so diffs show rewrapped lines instead of changed words. Applies to `.md` and `.tex` alike; code blocks, tables and list items keep their own line.
 
+## Soundness
+
+- in the recursion program, the prover transmits advice to the verifier, called "hints". These advice should not be truster (a malicious prover should never be able to prove an invalid witness), and carefully checked by the verifier.
+
 ## Env knobs
 
 | var                                                                                                     | effect                                           |
@@ -103,7 +110,7 @@ The third is worth understanding before touching the verifier. `guests/recursion
 | `ZK_ALLOC_STATS`                                                                                        | arena bytes/phase, high water, overflow          |
 | `BENCH_REPEAT`, `BENCH_COOLDOWN`                                                                        | `--repeat`/`--cooldown` for `#[ignore]`d benches |
 | `LEANVM_XMSS_N`, `LEANVM_HASH_N`, `LEANVM_HASH_UNROLL`                                                  | workload sizes in tests                          |
-| `FLOCK_N_LOG`, `FLOCK_PROVE_TRACE`, `FLOCK_ZC_TIMING`                                                   | flock batch size, stage traces                   |
+| `FLOCK_N_LOG`, `FLOCK_PROVE_TRACE`, `FLOCK_ZC_TIMING`, `LINCHECK_TRACE`                                 | flock batch size, stage traces                   |
 | `PCS_LOG_N`, `PCS_LOG_INV_RATE`, `PCS_MIN_MU`, `PCS_SAMPLES`                                            | PCS throughput bench                             |
 | `LIGERITO_TRACE`, `LIGERITO_NUM_VARS`, `LIGERITO_LOG_INV_RATE`                                          | Ligerito NTT/Merkle split                        |
 | `DBG_PROF{,_DUMP}`, `DBG_LOOPS`, `DBG_DISASM`, `DBG_LOWER`, `DBG_CSE`, `DBG_NO_CSE`, `DBG_PLACEHOLDERS` | compiler / guest-cycle attribution               |

Cargo.lock

@@ -24,14 +24,13 @@ edition = "2024"
 [workspace]
 members = ["crates/*"]
 
-# Hand-tuned numeric kernels (flock, pcs) legitimately index by loop variable,
-# take many arguments, and assert on constants; silence those style lints
-# workspace-wide rather than annotating every kernel.
+# Hand-tuned numeric kernels legitimately index by loop variable (26 sites in
+# primitives, pcs, flock, lean_vm) and take many arguments (12 sites in pcs,
+# flock, lean_vm); silence those two style lints workspace-wide rather than
+# annotating every kernel.
 [workspace.lints.clippy]
 needless_range_loop = "allow"
 too_many_arguments = "allow"
-assertions_on_constants = "allow"
-explicit_counter_loop = "allow"
 
 [workspace.dependencies]
 primitives = { path = "crates/primitives" }

Cargo.toml

@@ -1,11 +1,6 @@
 //! The shared Fiat–Shamir layer: the VM-native [`sponge::Sponge`] and the
 //! [`transcript`] wrapper states (`ProverState`/`VerifierState`) that pair it
-//! with the proof transport channels. Every protocol in this workspace — the
-//! VM's own reductions, flock's zerocheck/lincheck, and the Ligerito PCS —
-//! draws its challenges from this one transcript.
+//! with the proof transport channels.
 
 pub mod sponge;
 pub mod transcript;
-
-pub use sponge::{Sponge, TraceOp, compress, trace, trace_start, trace_take};
-pub use transcript::{Error, Proof, ProverState, VerifierState};

crates/fiat_shamir/src/lib.rs

@@ -1,8 +1,5 @@
 // CREDIT: https://github.com/signalapp/libsignal/blob/main/rust/poksho/src/shosha256.rs, AGPL-3.0-only.
-//! The VM-native Fiat–Shamir sponge: THE verifier-randomness source for the
-//! whole stack — flock's zerocheck / lincheck, the Ligerito PCS, and
-//! leanVM-b's own protocol (whose `ProverState` / `VerifierState` wrap this
-//! sponge with the proof transport channels).
+//! The VM-native Fiat–Shamir sponge.
 //!
 //! A 256-bit chaining value evolved only by the fixed 64→32 BLAKE3 compression
 //! the VM's `Blake3` opcode computes, so prover, verifier, and a recursive
@@ -20,8 +17,8 @@
 //! (`libsignal/rust/poksho/src/shosha256.rs`, © 2020 Signal Messenger, LLC,
 //! AGPL-3.0-only): a chaining value advanced by domain-separated absorb /
 //! squeeze steps. Here the underlying hash is the VM's BLAKE3 compression
-//! rather than SHA-256, inputs are `K = GF(2^64)` field words, and — because
-//! every absorb is domain-tagged per compression — no explicit double-hash
+//! rather than SHA-256, inputs are `K = GF(2^64)` field words, and, because
+//! every absorb is domain-tagged per compression, no explicit double-hash
 //! ratchet is needed.
 //!
 //! Each challenge is the random-oracle image of the whole prior transcript;
@@ -32,7 +29,7 @@
 use primitives::field::{F64, F192};
 
 /// `f(a, b) = BLAKE3(a‖b)` on two 256-bit halves laid out little-endian into 64
-/// bytes — *exactly* the VM's `Blake3` opcode: 64 input bytes → 32-byte digest,
+/// bytes, *exactly* the VM's `Blake3` opcode: 64 input bytes → 32-byte digest,
 /// split back into four field words. THE primitive; the sponge is a chain of
 /// these, so a zkDSL program replays it with one `blake3(...)` per step.
 pub fn compress(a: [F64; 4], b: [F64; 4]) -> [F64; 4] {
@@ -55,10 +52,9 @@ const DS_SQUEEZE: F64 = F64(4);
 const DS_POW: F64 = F64(5);
 
 /// `compress(base, (nonce.c0, nonce.c1, nonce.c2, DS_POW))` has its low `bits`
-/// bits zero — the
-/// grinding predicate over the VM compression. A CONTIGUOUS low-bit window
-/// (rather than byte-wise leading zeros) so a recursive verifier re-checks it
-/// with a single loop over the bit decomposition of the digest word
+/// bits zero: the grinding predicate over the VM compression. A CONTIGUOUS
+/// low-bit window (rather than byte-wise leading zeros) so a recursive verifier
+/// re-checks it with a single loop over the bit decomposition of the digest word
 /// (`grind_check` in `guests/recursion.py`). `bits` is always `< 64`.
 #[inline]
 fn pow_bits_ok(base: [F64; 4], nonce: F192, bits: u32) -> bool {
@@ -79,7 +75,7 @@ pub struct Sponge {
 impl Sponge {
     /// Seed with the domain `label` and the PUBLIC `statement` scalars (the public
     /// input). Both sides seed identically, so the whole statement is bound before
-    /// any challenge — there is no mid-protocol "observe public data" step to get
+    /// any challenge; there is no mid-protocol "observe public data" step to get
     /// wrong (or forget). (Untraced: the seed is the replay STARTING state, not an
     /// op of the recorded transcript.)
     pub fn new(label: &[u8], statement: &[F192]) -> Self {
@@ -92,12 +88,6 @@ impl Sponge {
         s
     }
 
-    /// A fresh chain at the zero state: the guest-side aggregation and export
-    /// transcripts start here (no label), and the harness mirrors them.
-    pub fn empty() -> Self {
-        Self { cv: [F64::ZERO; 4] }
-    }
-
     /// Absorb one 24-byte scalar (three little-endian `K` limbs):
     /// `cv ← compress(cv, (c0, c1, c2, DS_SCALAR))`.
     pub fn observe(&mut self, x: F192) {
@@ -130,7 +120,7 @@ impl Sponge {
 
     /// Squeeze a challenge and ratchet: the challenge's three limbs are the
     /// first three words of `compress(cv, (0, 0, DS_SQUEEZE, 0))`, whose full output
-    /// becomes the new state — domain-separated from absorbs, so a challenge
+    /// becomes the new state, domain-separated from absorbs, so a challenge
     /// cannot be confused with a continued absorb. In Fiat–Shamir everything is
     /// public; soundness comes from each challenge being a random-oracle image
     /// of the entire prior transcript.
@@ -164,12 +154,12 @@ impl Sponge {
 
     /// The grinding digest word this state yields for `nonce` (read-only preview;
     /// [`Self::verify_pow`] is the mutating check).
-    pub fn pow_digest(&self, nonce: F192) -> F64 {
+    fn pow_digest(&self, nonce: F192) -> F64 {
         compress(self.pow_base(), [F64(nonce.c0), F64(nonce.c1), F64(nonce.c2), DS_POW])[0]
     }
 
     /// Re-run recorded verifier transcript ops through this sponge, asserting
-    /// every recorded sample (and grind) matches what this state re-derives —
+    /// every recorded sample (and grind) matches what this state re-derives;
     /// any prefix of a real verify trace yields the exact state reached there.
     /// (Untraced throughout: a replay must never re-record.)
     pub fn replay(&mut self, ops: &[TraceOp]) {
@@ -233,7 +223,7 @@ impl Sponge {
 
     /// Verifier-side mirror of [`Self::grind_pow`]: check `nonce` clears the `bits`
     /// PoW against the current state, then bind it regardless (so the sponge stays
-    /// in lockstep with an honest prover — a failed check rejects at the call
+    /// in lockstep with an honest prover; a failed check rejects at the call
     /// site). `bits = 0` accepts only the canonical nonce `0`, which keeps proofs
     /// non-malleable at zero-bit grinding sites.
     pub fn verify_pow(&mut self, nonce: u64, bits: u32) -> bool {
@@ -276,7 +266,7 @@ impl Sponge {
 pub enum TraceOp {
     /// A stream word consumed without binding (grinding nonces).
     StreamRaw(F192),
-    /// An absorbed scalar (transmitted or derived — the sponge cannot tell).
+    /// An absorbed scalar (transmitted or derived: the sponge cannot tell).
     Observe(F192),
     /// `absorb_bytes` (labels, roots).
     AbsorbBytes(Vec<u8>),
@@ -359,11 +349,11 @@ mod tests {
         bytes[..8].copy_from_slice(&x.c0.to_le_bytes());
         bytes[8..16].copy_from_slice(&x.c1.to_le_bytes());
         bytes[16..].copy_from_slice(&x.c2.to_le_bytes());
-        b.absorb_bytes(&bytes);
+        b.absorb_bytes_untraced(&bytes);
         assert_ne!(a.sample(), b.sample());
     }
 
-    /// A grind clears its own PoW; a nonce that does not is rejected.
+    /// A grind clears its own PoW, and returns the SMALLEST nonce that does.
     #[test]
     fn pow_predicate() {
         let sp = Sponge::new(b"t", &[f(1)]);
@@ -373,8 +363,12 @@ mod tests {
             clone.grind_pow(8)
         };
         assert!(pow_bits_ok(base, F192::new(good, 0, 0), 8));
-        // A random wrong nonce almost surely fails an 8-bit grind.
-        assert!(!pow_bits_ok(base, F192::new(good.wrapping_add(1).wrapping_mul(3) | 1, 0, 0), 8,) || good != 0);
+        for n in 0..good {
+            assert!(
+                !pow_bits_ok(base, F192::new(n, 0, 0), 8),
+                "nonce {n} < {good} also clears"
+            );
+        }
     }
 
     /// Recursive proofs transport the nonce as one field word. Its high limb is