From 46600a3e2df667fda329550cf06496e361d055d2 Mon Sep 17 00:00:00 2001 From: aryaethn <47050616+aryaethn@users.noreply.github.com> Date: Fri, 26 Jun 2026 15:47:49 +0300 Subject: [PATCH] Bind useful_bits + const_pin into statement digest; pin hash walkers Addresses two items from the security audit (#1): - statement_digest() now absorbs useful_bits and const_pin (tag bumped v0 -> v1, with a length-unambiguous Option encoding). Both fields change the lincheck / padding semantics, so omitting them left a statement-substitution gap in the Fiat-Shamir binding. - Blake3LincheckCircuit / Sha2LincheckCircuit now override const_pin_col() -> Some(Z_CONST_POS), so the lincheck beta-pin term is not silently dropped when those circuits are used directly. Adds regression tests: digest-change coverage for both fields, and walker-vs-sparse constant-pin alignment for both hashes. Full suite green (337 tests). Co-Authored-By: Claude Opus 4.8 (1M context) --- crates/flock-core/src/r1cs.rs | 68 ++++++++++++++++++- crates/flock-prover/src/r1cs_hashes/blake3.rs | 17 +++++ crates/flock-prover/src/r1cs_hashes/sha2.rs | 17 +++++ 3 files changed, 100 insertions(+), 2 deletions(-) diff --git a/crates/flock-core/src/r1cs.rs b/crates/flock-core/src/r1cs.rs index b84e1b4..858ff63 100644 --- a/crates/flock-core/src/r1cs.rs +++ b/crates/flock-core/src/r1cs.rs @@ -181,7 +181,8 @@ impl BlockR1cs { apply_block_diag_packed(&self.c_0, z_packed, self.m, self.k_log) } - /// BLAKE3 hash of the R1CS instance (parameters + sparse matrices). + /// BLAKE3 hash of the R1CS instance: the shape parameters (`m`, `k_log`, + /// `k_skip`, `useful_bits`, `const_pin`) and the sparse matrices. /// Stable across runs; used to bind the Fiat-Shamir transcript to the /// statement being proved. /// @@ -191,10 +192,27 @@ impl BlockR1cs { pub fn statement_digest(&self) -> [u8; 32] { *self.digest_cache.get_or_init(|| { let mut h = blake3::Hasher::new(); - h.update(b"flock-r1cs-stmt-v0"); + // Tag bumped v0 -> v1 when useful_bits/const_pin were added to the + // absorbed fields, so a v0 transcript can never collide with a v1. + h.update(b"flock-r1cs-stmt-v1"); h.update(&(self.m as u64).to_le_bytes()); h.update(&(self.k_log as u64).to_le_bytes()); h.update(&(self.k_skip as u64).to_le_bytes()); + // Padding boundary: which rows carry witness vs. zero padding. It + // changes the lincheck equation, so it is part of the statement. + h.update(&(self.useful_bits as u64).to_le_bytes()); + // Constant-wire pin column, which drives the lincheck β-pin term. + // Length-unambiguous Option encoding: 1-byte present/absent tag, + // then the column index when present. + match self.const_pin { + Some(col) => { + h.update(&[1u8]); + h.update(&(col as u64).to_le_bytes()); + } + None => { + h.update(&[0u8]); + } + } absorb_matrix(&mut h, &self.a_0); absorb_matrix(&mut h, &self.b_0); absorb_matrix(&mut h, &self.c_0); @@ -705,4 +723,50 @@ mod tests { z_nonzero[5] = true; assert!(!r1cs.satisfies(&z_nonzero)); } + + #[test] + fn statement_digest_binds_useful_bits_and_const_pin() { + // Two instances identical except for `useful_bits` (resp. `const_pin`) + // must produce different digests: both change the lincheck / padding + // semantics, so the Fiat-Shamir transcript must depend on them. See + // statement_digest's v1 tag bump. + let k_log = 3; + let m = 6; + let base = || BlockR1cs { + m, + k_log, + k_skip: 2, + useful_bits: 1 << k_log, + a_0: identity(1 << k_log), + b_0: identity(1 << k_log), + c_0: identity(1 << k_log), + const_pin: None, + digest_cache: std::sync::OnceLock::new(), + csc_cache: std::sync::OnceLock::new(), + }; + + let d0 = base().statement_digest(); + // Determinism: same instance ⇒ same digest. + assert_eq!(d0, base().statement_digest()); + + // useful_bits is bound. + let mut r_ub = base(); + r_ub.useful_bits = (1 << k_log) - 1; + assert_ne!(d0, r_ub.statement_digest(), "useful_bits not bound"); + + // const_pin presence is bound (None vs Some). + let mut r_pin = base(); + r_pin.const_pin = Some(0); + assert_ne!(d0, r_pin.statement_digest(), "const_pin not bound"); + + // const_pin *column index* is bound (Some(0) vs Some(1)), not just + // presence — the Option encoding absorbs the value too. + let mut r_pin1 = base(); + r_pin1.const_pin = Some(1); + assert_ne!( + r_pin.statement_digest(), + r_pin1.statement_digest(), + "const_pin column index not bound" + ); + } } diff --git a/crates/flock-prover/src/r1cs_hashes/blake3.rs b/crates/flock-prover/src/r1cs_hashes/blake3.rs index cae665a..85c1b39 100644 --- a/crates/flock-prover/src/r1cs_hashes/blake3.rs +++ b/crates/flock-prover/src/r1cs_hashes/blake3.rs @@ -689,6 +689,15 @@ impl flock_core::lincheck::LincheckCircuit for Blake3LincheckCircuit { K } + /// Advertise the constant-wire pin so lincheck adds the β-pin term when + /// this walker is used directly. The matrix-based circuit carries it via + /// `BlockR1cs::{sparse,csc}_lincheck_circuit` (`const_pin = + /// Some(Z_CONST_POS)`); the walker must match, or the all-zero-witness + /// soundness gap reopens. See `docs/const-wire-pin.md`. + fn const_pin_col(&self) -> Option { + Some(Z_CONST_POS) + } + fn fold_alpha_batched(&self, alpha: F128, eq_inner: &[F128]) -> Vec { assert_eq!(eq_inner.len(), K, "eq_inner length must equal n_cols = K"); let mut comb = vec![F128::ZERO; K]; @@ -1888,6 +1897,14 @@ mod tests { let walker = Blake3LincheckCircuit; assert_eq!(sparse.n_cols(), walker.n_cols()); + // The walker must advertise the same constant-wire pin the live matrix + // circuit carries (the setup sets const_pin = Some(Z_CONST_POS)), or + // the lincheck β-pin term is silently dropped when the walker is used + // directly, reopening the all-zero-witness gap. + let pinned = SparseMatrixCircuit::new(&a_0, &b_0).with_const_pin(Some(Z_CONST_POS)); + assert_eq!(walker.const_pin_col(), Some(Z_CONST_POS)); + assert_eq!(walker.const_pin_col(), pinned.const_pin_col()); + let n_cols = walker.n_cols(); let alpha = F128 { lo: ((rng.next_u32() as u64) << 32) | rng.next_u32() as u64, diff --git a/crates/flock-prover/src/r1cs_hashes/sha2.rs b/crates/flock-prover/src/r1cs_hashes/sha2.rs index 839cc23..aca7d3a 100644 --- a/crates/flock-prover/src/r1cs_hashes/sha2.rs +++ b/crates/flock-prover/src/r1cs_hashes/sha2.rs @@ -712,6 +712,15 @@ impl flock_core::lincheck::LincheckCircuit for Sha2LincheckCircuit { K } + /// Advertise the constant-wire pin so lincheck adds the β-pin term when + /// this walker is used directly. The matrix-based circuit carries it via + /// `BlockR1cs::{sparse,csc}_lincheck_circuit` (`const_pin = + /// Some(Z_CONST_POS)`); the walker must match, or the all-zero-witness + /// soundness gap reopens. See `docs/const-wire-pin.md`. + fn const_pin_col(&self) -> Option { + Some(Z_CONST_POS) + } + fn fold_alpha_batched(&self, alpha: F128, eq_inner: &[F128]) -> Vec { assert_eq!(eq_inner.len(), K, "eq_inner length must equal n_cols = K"); let mut comb = vec![F128::ZERO; K]; @@ -2052,6 +2061,14 @@ mod tests { let walker = Sha2LincheckCircuit; assert_eq!(sparse.n_cols(), walker.n_cols()); + // The walker must advertise the same constant-wire pin the live matrix + // circuit carries (the setup sets const_pin = Some(Z_CONST_POS)), or + // the lincheck β-pin term is silently dropped when the walker is used + // directly, reopening the all-zero-witness gap. + let pinned = SparseMatrixCircuit::new(&a_0, &b_0).with_const_pin(Some(Z_CONST_POS)); + assert_eq!(walker.const_pin_col(), Some(Z_CONST_POS)); + assert_eq!(walker.const_pin_col(), pinned.const_pin_col()); + let n_cols = walker.n_cols(); let alpha = F128 { lo: ((rng.next_u32() as u64) << 32) | rng.next_u32() as u64,