Hash the flock R1CS matrices densely, and rename the digest

The circuit digest absorbed the matrices in sparse form, eight bytes per
nonzero, which at 13% to 20% density was seven times longer than the dense
bit image: ~715 MB hashed against ~101 MB. Absorb the dense image instead,
a row at a time so the scatter stays L1-resident and the 96 MiB image is
never materialized. Computing the digest drops from 890 ms to 196 ms.

The dense form is also canonical. Over GF(2) a repeated column index cancels
and a reordered row is the same matrix, so the sparse form committed to an
encoding rather than to the matrix.

"Family" is renamed to "r1cs" throughout (FAMILY_DIGEST, family_digest, and
the prose in lean_vm, rec_aggregation and the end-to-end doc section). What
the word was carrying, that the digest omits the instance count and so covers
every block-diagonal instance over these matrices, is now said outright in
the doc comment. The in-hash domain tag becomes flock-r1cs-digest-v2, v2
because v1 named the sparse encoding.

Also inlines the python verifier's transcript_statement into its one caller.

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

Author: TomWambsgans

crates/flock/src/blake2s.rs

@@ -357,16 +357,16 @@ fn build_matrices() -> (SparseBinaryMatrix, SparseBinaryMatrix) {
     (to_mat(a_rows), to_mat(b_rows))
 }
 
-/// [`BlockR1cs::family_digest`] of this module's circuit, baked as a constant:
+/// [`BlockR1cs::r1cs_digest`] of this module's circuit, baked as a constant:
 /// recomputing it means building ~89M matrix entries and hashing their 96 MiB
 /// bit image, which embedding protocols would otherwise pay inside their first
-/// prove. The `family_digest_matches_baked` test recomputes and compares: a
+/// prove. The `r1cs_digest_matches_baked` test recomputes and compares: a
 /// circuit change fails it until this constant is updated alongside. The same
 /// digest is mirrored in `python-verifier/verifier.py`, which cannot rebuild
 /// the matrices at all.
-pub const FAMILY_DIGEST: [u8; 32] = [
-    0x85, 0x3d, 0xce, 0x57, 0x41, 0x67, 0x01, 0x82, 0x17, 0x97, 0x55, 0xd5, 0xa0, 0x51, 0xd4, 0xf5, 0x63, 0x1b, 0x3c,
-    0x0f, 0x10, 0x3d, 0x63, 0x3d, 0xda, 0x3a, 0xce, 0xcf, 0x6a, 0x88, 0x60, 0x1e,
+pub const R1CS_DIGEST: [u8; 32] = [
+    0xec, 0x91, 0xe9, 0xd8, 0xd9, 0xca, 0x4e, 0x30, 0x62, 0x05, 0x90, 0x7a, 0x0d, 0x23, 0x6e, 0x53, 0xa6, 0xcd, 0xbd,
+    0xa0, 0x38, 0x2e, 0xf6, 0xc4, 0x33, 0xef, 0x93, 0x63, 0xed, 0xfe, 0x04, 0x2e,
 ];
 
 /// Build a [`BlockR1cs`] batching `2^n_blocks_log` independent BLAKE2s
@@ -838,7 +838,7 @@ impl Blake2sSetup {
     /// the shared transcript, reducing R1CS validity of `blocks` to two
     /// evaluation claims on the committed packed witness `q_flock`. (The
     /// statement is already transcript-bound: the embedding protocol seeds
-    /// with the circuit family digest and announces the count.) Returns:
+    /// with the R1CS digest and announces the count.) Returns:
     /// - `z_packed`: the regenerated packed witness the PCS later opens against;
     /// - the [`PackedWitnessClaims`] `(ab, c)` on `q_flock`, with ring-switch weights.
     ///
@@ -893,7 +893,7 @@ impl Blake2sSetup {
         assert_eq!(z_packed_lincheck.len(), packed_len * 8, "wrong lincheck stripe length");
 
         // No bind_statement here: the embedding protocol (leanVM-b) seeds its
-        // transcript with the circuit-FAMILY digest and binds the instance
+        // transcript with the R1CS digest and binds the instance
         // count and commitment root before any challenge, so the statement is
         // already fully transcript-bound.
 
@@ -963,7 +963,7 @@ impl Blake2sSetup {
         vs: &mut fiat_shamir::transcript::VerifierState<'_>,
     ) -> Result<ReductionReplay, verifier::VerifyError> {
         // Mirror of prove_reduction: the statement is bound by the embedding
-        // protocol's seed (family digest) + announced count + commitment root.
+        // protocol's seed (R1CS digest) + announced count + commitment root.
 
         let zc_claim = crate::zerocheck::verify(self.r1cs.m, vs).map_err(verifier::VerifyError::Zerocheck)?;
         let inner_rest_len = self.r1cs.k_log - self.r1cs.k_skip;
@@ -1060,11 +1060,11 @@ mod tests {
     }
 
     #[test]
-    fn family_digest_matches_baked() {
+    fn r1cs_digest_matches_baked() {
         assert_eq!(
-            build_block_r1cs(3).family_digest(),
-            FAMILY_DIGEST,
-            "circuit family changed - update FAMILY_DIGEST"
+            build_block_r1cs(3).r1cs_digest(),
+            R1CS_DIGEST,
+            "R1CS changed - update R1CS_DIGEST"
         );
     }
 

crates/flock/src/r1cs.rs

@@ -8,7 +8,7 @@
 //! We further specialize to **block-diagonal `A` and `B`**:
 //!   `A = I_{2^n_log} ⊗ A_0`, etc. The base matrices are `k × k` sparse
 //! boolean (`k = 2^k_log`). `C_0 = I_k` is implicit, but the materialized
-//! `c_0` matrix is still carried because [`BlockR1cs::family_digest`] absorbs
+//! `c_0` matrix is still carried because [`BlockR1cs::r1cs_digest`] absorbs
 //! it.
 
 /// Sparse boolean matrix. `rows[i]` lists the column indices where the entry is 1.
@@ -22,7 +22,7 @@ pub struct SparseBinaryMatrix {
 /// Memory/variable layout of the committed witness (address bit `i` of the
 /// packed buffer = MLE variable `i`): `addr = [k_log inner bits | n_log batch
 /// bits]`, each instance one contiguous `2^k_log`-bit block. A one-variant
-/// enum so the layout byte stays an explicit part of [`BlockR1cs::family_digest`].
+/// enum so the layout byte stays an explicit part of [`BlockR1cs::r1cs_digest`].
 #[derive(Clone, Copy, Debug, Default, PartialEq, Eq)]
 pub enum WitnessLayout {
     #[default]
@@ -53,7 +53,7 @@ pub struct BlockR1cs {
     pub b_0: SparseBinaryMatrix,
     pub c_0: SparseBinaryMatrix,
     /// Memory/variable layout of the committed witness (see [`WitnessLayout`]).
-    /// Bound into [`Self::family_digest`].
+    /// Bound into [`Self::r1cs_digest`].
     pub layout: WitnessLayout,
     /// Column of a constant-one wire to pin to 1 across all blocks, or `None`.
     /// Drives the lincheck constant-wire pin (see
@@ -136,15 +136,18 @@ impl BlockR1cs {
             .all(|((ai, bi), ci)| (*ai & *bi) == *ci)
     }
 
-    /// BLAKE2s hash of the circuit FAMILY: the per-block matrices and the
-    /// shape parameters, explicitly WITHOUT the instance count `m`. The full
-    /// instance is block-diagonal (`m` copies of these matrices), so a
+    /// BLAKE2s hash of the R1CS itself: the per-block matrices and the shape
+    /// parameters, explicitly WITHOUT the instance count `m`. It therefore
+    /// identifies every block-diagonal instance built from these matrices at
+    /// once, whatever the count. The full instance is `m` copies of them, so a
     /// protocol that binds this digest and `m` separately has bound the whole
     /// statement; embedding protocols (leanVM-b) seed their transcript with it
     /// and announce the count.
-    pub fn family_digest(&self) -> [u8; 32] {
+    pub fn r1cs_digest(&self) -> [u8; 32] {
         let mut h = primitives::blake2s::Hasher::new();
-        h.update(b"flock-r1cs-family-v1");
+        // v2: v1 absorbed the matrices in sparse form, this one absorbs their
+        // dense bit image (see `absorb_matrix`).
+        h.update(b"flock-r1cs-digest-v2");
         h.update(&(self.k_log as u64).to_le_bytes());
         h.update(&(self.k_skip as u64).to_le_bytes());
         // The layout determines which polynomial a given witness commits
@@ -167,7 +170,7 @@ impl BlockR1cs {
 /// repeated column index cancels and a reordered row is the same matrix, so the
 /// sparse form commits to an encoding rather than to the matrix. And at these
 /// densities (13% to 20%) it is seven times shorter, one bit per entry against
-/// eight bytes per nonzero, which is the whole cost of [`BlockR1cs::family_digest`].
+/// eight bytes per nonzero, which is the whole cost of [`BlockR1cs::r1cs_digest`].
 fn absorb_matrix(h: &mut primitives::blake2s::Hasher, m: &SparseBinaryMatrix) {
     assert_eq!(m.rows.len(), m.num_rows);
     h.update(&(m.num_rows as u64).to_le_bytes());

crates/lean_vm/src/blake2s_flock.rs

@@ -276,16 +276,16 @@ pub fn warm_setup(n_blocks: usize) {
     let _ = setup_for(n_blocks.max(1));
 }
 
-/// The flock BLAKE2s circuit-FAMILY digest: a hash of the per-block R1CS
-/// matrices and shape parameters ([`family_digest`] on the R1CS), independent
+/// The flock BLAKE2s R1CS digest: a hash of the per-block R1CS matrices and
+/// shape parameters ([`flock::r1cs::BlockR1cs::r1cs_digest`]), independent
 /// of the instance count. The full instance is block-diagonal (the count is
 /// announced and absorbed with the other sizes), so a transcript seeded with
 /// this digest (via [`crate::cpu::fs_seed`]) binds the whole statement up
 /// front. Baked in flock (test-guarded): recomputing it costs ~200 ms of
 /// hashing on top of building the matrices, which used to land inside the
 /// first `prove`.
-pub fn family_digest() -> [u8; 32] {
-    flock::blake2s::FAMILY_DIGEST
+pub fn r1cs_digest() -> [u8; 32] {
+    flock::blake2s::R1CS_DIGEST
 }
 
 /// **Flock reduction only** (prover): run flock's BLAKE2s zerocheck + lincheck

crates/lean_vm/src/cpu/mod.rs

@@ -63,8 +63,8 @@ const MAX_LOG_ROWS: usize = 32;
 const MAX_LOG_BYTECODE: usize = 32;
 
 /// The Fiat-Shamir seed: ONE 32-byte digest, as two field words, committing
-/// to everything fixed about the proving environment: the flock circuit
-/// family (its per-block R1CS matrices, [`crate::blake2s_flock::family_digest`])
+/// to everything fixed about the proving environment: the flock BLAKE2s R1CS
+/// (its per-block matrices, [`crate::blake2s_flock::r1cs_digest`])
 /// and the bytecode, via the hash cached on `Program`: BLAKE2s over the stacked
 /// multilinear ([`layout::bytecode_table`]) rather than over an assembler
 /// digest, so a verifier holding only that polynomial reproduces the seed. That
@@ -77,7 +77,7 @@ const MAX_LOG_BYTECODE: usize = 32;
 pub fn fs_seed(program: &Program) -> [F192; 2] {
     let mut h = primitives::blake2s::Hasher::new();
     h.update(b"leanvm-b-fs-seed-v2-blake2s");
-    h.update(&crate::blake2s_flock::family_digest());
+    h.update(&crate::blake2s_flock::r1cs_digest());
     h.update(&program.bytecode_hash);
     let d = h.finalize();
     let word = |o: usize| u64::from_le_bytes(d[o..o + 8].try_into().unwrap());

crates/rec_aggregation/guests/recursion.py

@@ -239,7 +239,7 @@
 # The seed is NOT baked into the guest: it rides the recursion's PUBLIC INPUT
 # (the fs_seed hint folded into own_pi in main), so ONE compiled guest verifies
 # proofs of any inner program of this VM — the outer statement fixes the whole
-# proving environment (circuit family + program), via own_pi.
+# proving environment (flock R1CS + program), via own_pi.
 # The arity is hinted too, as g^nsub, and absorbed by both aggregation transcripts
 # ahead of every variable-length sequence, so the outer statement fixes it as well.
 # NSUB_BOUND (nsub < NSUB_BOUND) is the compile-time range-check bound that makes
@@ -1080,7 +1080,7 @@ def verify_sub(pi_0, pi_1, seed_0, seed_1, g_logs_pow2, g_squares, defer_out):
 
     # ---- seed (statement pre-bound: hinted sub pi + baked program digest) ----
     fs = [TRANSCRIPT_SEED_0, TRANSCRIPT_SEED_1]
-    fs = obs(fs, seed_0)  # the FS seed: H(flock circuit family, inner program
+    fs = obs(fs, seed_0)  # the FS seed: H(flock BLAKE2s R1CS, inner program
     fs = obs(fs, seed_1)  # bytecode, ...) — from the recursion's public input
     fs = obs(fs, pi_0)   # bind the sub-proof's statement (its public input)
     fs = obs(fs, pi_1)
@@ -2240,7 +2240,7 @@ def main():
     assert log(nsub_g) < NSUB_BOUND
     sub_pis = HeapBuf(nsub_g * nsub_g)  # 2 statement words per sub
     # The FS seed — ONE digest of everything fixed about the inner environment
-    # (the flock circuit family, the inner program bytecode) — rides the
+    # (the flock BLAKE2s R1CS, the inner program bytecode) — rides the
     # recursion's public input: hinted here, it leads every sub's transcript
     # and is folded into own_pi below, so the outer statement fixes the whole
     # proving environment with one word pair.

crates/rec_aggregation/src/recursion.rs

@@ -543,7 +543,7 @@ fn aggregate_deferred_claims(
         assert_eq!(mrun, v_a * wam + v_b * wbm, "guest terminal-weight formulas");
     }
 
-    // The inner proving environment (flock circuit family + program bytecode)
+    // The inner proving environment (flock BLAKE2s R1CS + program bytecode)
     // is identified by ONE seed digest in the recursion's PUBLIC INPUT (not
     // baked into the guest), so one compiled guest serves any inner program.
     let seed = lean_vm::cpu::fs_seed(program);

doc/leanvm/body/08-end-to-end-protocol.tex

@@ -70,7 +70,7 @@ \subsection{The unrolled protocol}\label{sec:e2e-unrolled}
 
 Each reduction below adds evaluation claims on columns to a shared \emph{claim pool}; the final \textsc{Opening} phase proves all of them with a single PCS opening.
 
-\paragraph{Setup and statement binding.} Fixed and shared in advance (\S\ref{sec:e2e-const} through \S\ref{sec:e2e-pi}): the fields and constants; the instance caps (\S\ref{sec:memchan}); the public program and its length; the initial state $(\pc_0,\fp_0)$ and final state $(\pc_{\mathrm{final}},\fp_{\mathrm{final}})$; and the public input $\mem[0],\mem[1]$. Before any challenge, the transcript is seeded by the public input and one environment digest that binds both the exact bytecode and flock's BLAKE2s circuit family. The prover then announces the memory log-size $h$ and the seven table log-heights $\tau_j$; the verifier checks them against the caps and derives every table, stack, and leaf shape.
+\paragraph{Setup and statement binding.} Fixed and shared in advance (\S\ref{sec:e2e-const} through \S\ref{sec:e2e-pi}): the fields and constants; the instance caps (\S\ref{sec:memchan}); the public program and its length; the initial state $(\pc_0,\fp_0)$ and final state $(\pc_{\mathrm{final}},\fp_{\mathrm{final}})$; and the public input $\mem[0],\mem[1]$. Before any challenge, the transcript is seeded by the public input and one environment digest that binds both the exact bytecode and flock's BLAKE2s R1CS. The prover then announces the memory log-size $h$ and the seven table log-heights $\tau_j$; the verifier checks them against the caps and derives every table, stack, and leaf shape.
 
 \paragraph{Commitment.}
 \begin{enumerate}

python-verifier/verifier.py

@@ -292,13 +292,7 @@ def blake2s_hash(data: bytes) -> Digest:
 
 @dataclass(frozen=True, slots=True)
 class Digest:
-    """256 bits: a BLAKE2s output, a Merkle node, the sponge state, the public input.
-
-    One transcript encoding, everywhere: two 128-bit halves, each an E element
-    carrying a K pair with a spare top lane (`pcs::merkle::hash_to_scalars`).
-    128 bits is the VM's digest unit, which is what `PACK64X2` builds, so the
-    recursion guest reads every digest with the same two-cell shape.
-    """
+    """256 bits"""
 
     value: bytes
 
@@ -976,7 +970,7 @@ def verify_constraints(
 
 # VM statement, layout, and AIR -----------------------------------------------
 
-FAMILY_DIGEST = bytes.fromhex("853dce5741670182179755d5a051d4f5631b3c0f103d633dda3acecf6a88601e")
+R1CS_DIGEST = bytes.fromhex("ec91e9d8d9ca4e306205907a0d236e53a6cdbda0382ef6c433ef9363edfe042e")
 MAX_LOG_BYTECODE = 32
 
 # The bytecode's nine public columns (opcode + eight operand/immediate slots)
@@ -1004,18 +998,6 @@ def bytecode_columns(bytecode: Sequence[K]) -> tuple[tuple[tuple[K, ...], ...],
     return columns, kbc
 
 
-def transcript_statement(bytecode: Sequence[K], public_input: Sequence[E]) -> tuple[E, ...]:
-    """The public statement, bound before any challenge (`lean_vm::cpu::fs_seed`).
-
-    The seed hashes the bytecode multilinear itself, not a structured program, so
-    a verifier holding only the polynomial can reproduce it. Rust caches that
-    inner hash on `Program`, which is why it is a separate step here.
-    """
-    bytecode_hash = blake2s_hash(b"".join(word.to_bytes() for word in bytecode))
-    seed = blake2s_hash(b"leanvm-b-fs-seed-v2-blake2s" + FAMILY_DIGEST + bytecode_hash.value)
-    return (*seed.halves(), *public_input)
-
-
 # The columns no instruction table owns (doc sec:e2e-unrolled, Commitment): the
 # memory image's three limbs, the two finalize counts, and flock's packed
 # witness. They come first in the global column numbering, the tables after.
@@ -2163,7 +2145,12 @@ def linear_rows(values: Sequence[E], base: int) -> None:
 def verify_execution(bytecode: Sequence[K], public_input: Digest, proof: Proof) -> None:
     pi = public_input.halves()
     public_columns, bytecode_log = bytecode_columns(bytecode)
-    transcript = Transcript(proof, b"leanvm-b", transcript_statement(bytecode, pi))
+    # The public statement, bound before any challenge (`lean_vm::cpu::fs_seed`).
+    # The seed hashes the bytecode multilinear itself, not a structured program,
+    # so a verifier holding only the polynomial can reproduce it.
+    bytecode_hash = blake2s_hash(b"".join(word.to_bytes() for word in bytecode))
+    seed = blake2s_hash(b"leanvm-b-fs-seed-v2-blake2s" + R1CS_DIGEST + bytecode_hash.value)
+    transcript = Transcript(proof, b"leanvm-b", (*seed.halves(), *pi))
 
     # 1] Statement binding: the announced instance shape, checked against the
     # public caps before any reduction runs on it.