verification: the Rust WHIR verifier refines the Lean model, via Aeneas

README.md

@@ -25,7 +25,7 @@
 
 leanVM is designed for security:
 
- * 128-bit ROM (64-bit QROM) soundness
+ * a 128-bit ROM (64-bit QROM) soundness target, not a proved deployed security level
  * no proximity gap conjecture
  * end-to-end formal verification
  * a traditional hash function
@@ -180,3 +180,17 @@ Each instruction class's circuit proven alone by flock, on `2^FLOCK_N_LOG` rando
 - [WHIR](https://eprint.iacr.org/2024/1586) PCS, aka [Ligerito](https://eprint.iacr.org/2025/1187)
 - [Flock](https://github.com/succinctlabs/flock/tree/main) hash proving
 - [Binius](https://github.com/IrreducibleOSS/binius)/[Binius64](https://github.com/binius-zk/binius64) ring switching, M3 arithmetisation, and more (see [DP23](https://eprint.iacr.org/2023/1784) and [DP24](https://eprint.iacr.org/2024/504))
+
+### Immutable PCS commitment anchors
+
+PCS commitment identity is now the complete immutable Merkle root, public shape, exact pre-commit transcript chaining value, normalized pending bytes and byte count, first-block flag and previous and current squeeze cursors, commitment-time extension-field point and advertised MLE value. Capturing that context does not flush, hash, sample, allocate or emit recursive rows. A valid duplex state's cached output is derivable from its chaining value and cursor; snapshots are read-only and cannot inject arbitrary states. `CommittedStack::new` binds the `whir-anchor-v1` marker, dimension/interleaving/rate tuple and occupied lane count before the root and the one anchor challenge. `StackCommitment::receive` checks the same context, derives that point once and reads its value. CPU proofs use `LVMP18` and the `leanvm-rv64im-14` program domain; tree proofs use `LVMT20` and the `leanvm-tree-17` domain. These identities are above current upstream. Legacy proofs are not accepted.
+
+Every public stacked opening requires this complete record. Its `whir-opening-v1` frame binds and compares the shape, raw 32-byte root, raw 32-byte original chaining value, pending-byte metadata and normalized buffer, point and advertised value before any opening batching challenge. Cursor metadata precedes pending bytes, packed as three little endian words per scalar with canonical final padding. This permits opening the same immutable record in a fresh session without receiving it again or resampling its point. Root-only WHIR kernels and dense-weight interfaces are crate-private protocol building blocks, not alternate public PCS verification paths. Callers must bind their complete opening statement before entry: values must already be observed or public, coordinates must be public constants or earlier verifier challenges, and addressing and shape must follow the bound layout. The identity frame does not bind arbitrary external claims. Omitted lanes remain mandated zero, and the anchor's linear weight is restricted to the occupied prefix in both native and row arithmetic.
+
+The crate-private terminal weight provider dispatches statically and is consumed once at the terminal point after rotating fold challenges into witness-coordinate order. Named weight values borrow their existing inputs without callback allocation.
+
+The separate Lean investigation proves ideal interactive uniform anchor candidate uniqueness with a commitment-fixed list, including arbitrary malicious advertised values and cross-session reuse. Its anchor ambiguity term is separate from opening, Fiat-Shamir, Merkle and concrete cryptographic losses. This branch normally merges upstream #607 at `d3c7f9d9a6ad4f7b88f917284076b34430502ae2`: session-IV derivation, public-instance absorption, raw-byte roots, the new codecs, proof-of-work and squeezed final digests. Proof PR #551's existing duplex refinement chain models the historical pre-#607 #552 transcript. Its checked adaptive ideal-compression coupling has loss `min(1,(2Q^2-Q)/2^256)`, but the conditional `2^-42` historical unanchored endpoint does not currently apply to the deployed #607 transcript or these new anchor inputs without the missing source adapters and composition. Its checked reset knowledge extractor is interactive only, not a Fiat-Shamir knowledge result. This cutover claims no proved whole-system security level, unconditional deterministic BLAKE2s security or universal Rust-to-Lean equivalence.
+
+A hiding commitment, which zero-knowledge proofs take for their stack and their key commitment, carries no anchor: its advertised value would be one more evaluation of the hidden witness, which the hiding argument does not cover. `CommittedStack::new_hiding` and `StackCommitment::hiding` stay root-only; `StackCommitment::receive` refuses a padding configuration and `StackCommitment::hiding` a plain one with `WhirError::Anchoring`, and weighted openings, which only the key commitment takes, are refused on an anchored commitment.
+
+The typed stacked receiver retains upstream's aligned plain-selector, checked strided-width and slot guards, including #608's machine-width checks. Native and Rows use the same typed verifier and record frame. The security theorem and a universal source correspondence must still discharge their stated model and caller-binding hypotheses.

crates/fiat_shamir/src/arith.rs

@@ -32,14 +32,6 @@ pub trait Arith {
     /// `a^(2^128)`: two Frobenius maps of `E` over `K`, which take `a` to `a^(2^-64)`.
     fn frobenius2(&mut self, a: Self::E) -> Self::E;
 
-    /// The multilinear extension of public `K` words at `point`, lowest coordinate first.
-    fn public_mle(&mut self, values: &[F64], point: &[Self::E]) -> Self::E {
-        assert_eq!(values.len(), 1 << point.len(), "a column has a word per vertex");
-        let eq = self.eq_table(point);
-        let zero = self.zero();
-        (eq.iter().zip(values)).fold(zero, |acc, (&e, &v)| self.mul_const_add(e, F192::from(v), acc))
-    }
-
     /// The constant zero.
     fn zero(&mut self) -> Self::E {
         self.constant(F192::ZERO)
@@ -76,13 +68,23 @@ pub trait Arith {
     /// `prod_i factors_i`.
     fn product(&mut self, factors: &[Self::E]) -> Self::E {
         let one = self.one();
-        factors.iter().fold(one, |acc, &f| self.mul(acc, f))
+        let mut acc = one;
+        for &f in factors {
+            acc = self.mul(acc, f);
+        }
+        acc
     }
 
     /// `sum_i c_i x^i`, by Horner, constant first.
     fn poly_eval(&mut self, coeffs: &[Self::E], x: Self::E) -> Self::E {
         let zero = self.zero();
-        coeffs.iter().rev().fold(zero, |acc, &c| self.mul_add(acc, x, c))
+        let mut acc = zero;
+        let mut i = coeffs.len();
+        while i > 0 {
+            i -= 1;
+            acc = self.mul_add(acc, x, coeffs[i]);
+        }
+        acc
     }
 
     /// The line through `(0, lo)` and `(1, hi)` at `t`: `lo + t·(lo + hi)`.
@@ -100,10 +102,12 @@ pub trait Arith {
     fn eq_eval(&mut self, x: &[Self::E], y: &[Self::E]) -> Self::E {
         assert_eq!(x.len(), y.len(), "two points of one cube");
         let one = self.one();
-        x.iter().zip(y).fold(one, |acc, (&u, &v)| {
-            let s = self.add(u, v);
-            self.times_one_plus(acc, s)
-        })
+        let mut acc = one;
+        for i in 0..x.len() {
+            let s = self.add(x[i], y[i]);
+            acc = self.times_one_plus(acc, s);
+        }
+        acc
     }
 
     /// `eq(bits, point)` for public bits, lowest first: `prod_j (bit_j ? z_j : 1 + z_j)`.
@@ -112,13 +116,17 @@ pub trait Arith {
     /// Why: selectors of nearby offsets share their high bits, so in rows their common partial products are made once.
     fn eq_bits(&mut self, bits: usize, point: &[Self::E]) -> Self::E {
         let one = self.one();
-        (point.iter().enumerate()).rev().fold(one, |acc, (j, &z)| {
-            if bits >> j & 1 == 1 {
-                self.mul(acc, z)
+        let mut acc = one;
+        let mut j = point.len();
+        while j > 0 {
+            j -= 1;
+            acc = if bits >> j & 1 == 1 {
+                self.mul(acc, point[j])
             } else {
-                self.times_one_plus(acc, z)
-            }
-        })
+                self.times_one_plus(acc, point[j])
+            };
+        }
+        acc
     }
 
     /// `eq(point, x)` for every vertex `x`, lowest coordinate first.
@@ -129,17 +137,26 @@ pub trait Arith {
     /// `eq(point, x)` for the first `len` vertices `x`, lowest coordinate first, with no work for the others.
     fn eq_table_prefix(&mut self, point: &[Self::E], len: usize) -> Vec<Self::E> {
         assert!(len <= 1 << point.len(), "a prefix of the cube");
-        let mut table = vec![self.one()];
-        for (i, &r) in point.iter().enumerate() {
+        let mut table = Vec::with_capacity(1);
+        table.push(self.one());
+        let mut i = 0;
+        while i < point.len() {
+            let r = point[i];
             let need = len.min(2 << i);
-            let high: Vec<Self::E> = table[..need.saturating_sub(table.len())]
-                .iter()
-                .map(|&v| self.mul(v, r))
-                .collect();
-            for v in &mut table {
-                *v = self.times_one_plus(*v, r);
+            let count = need.saturating_sub(table.len());
+            let mut high = Vec::with_capacity(count);
+            let mut j = 0;
+            while j < count {
+                high.push(self.mul(table[j], r));
+                j += 1;
+            }
+            let mut j = 0;
+            while j < table.len() {
+                table[j] = self.times_one_plus(table[j], r);
+                j += 1;
             }
             table.extend(high);
+            i += 1;
         }
         table.truncate(len);
         table
@@ -150,7 +167,14 @@ pub trait Arith {
         assert_eq!(values.len(), 1 << point.len(), "a value per vertex");
         let mut folded = values.to_vec();
         for &x in point {
-            folded = folded.chunks(2).map(|pair| self.interp(pair[0], pair[1], x)).collect();
+            let len = folded.len();
+            let mut next = Vec::with_capacity(len / 2 + len % 2);
+            let mut i = 0;
+            while i < len {
+                next.push(self.interp(folded[i], folded[i + 1], x));
+                i += 2;
+            }
+            folded = next;
         }
         folded[0]
     }
@@ -169,15 +193,46 @@ pub trait Arith {
     /// The integer index column `base ^ (z << shift)` at `point`: `base + sum_i point_i 2^(i + shift)`.
     fn int_index(&mut self, base: F64, shift: u32, point: &[Self::E]) -> Self::E {
         let base = self.constant(F192::from(base));
-        (point.iter().enumerate()).fold(base, |acc, (i, &z)| {
-            self.mul_const_add(z, F192::from(F64(1 << (i as u32 + shift))), acc)
-        })
+        let mut acc = base;
+        for (i, &z) in point.iter().enumerate() {
+            acc = self.mul_const_add(z, F192::from(F64(1 << (i as u32 + shift))), acc);
+        }
+        acc
     }
 }
 
-/// A verifier: arithmetic, a transcript to read and draw from, and equalities to check.
-///
-/// Natively the transcript is the proof's; in rows it is the circuit's replay of it.
+/// Arithmetic that also evaluates multilinear extensions of public columns.
+pub trait PublicMle: Arith {
+    /// The multilinear extension of public `K` words at `point`, lowest coordinate first.
+    fn public_mle(&mut self, values: &[F64], point: &[Self::E]) -> Self::E {
+        assert_eq!(values.len(), 1 << point.len(), "a column has a word per vertex");
+        let eq = self.eq_table(point);
+        let zero = self.zero();
+        let mut acc = zero;
+        for i in 0..eq.len().min(values.len()) {
+            acc = self.mul_const_add(eq[i], F192::from(values[i]), acc);
+        }
+        acc
+    }
+}
+
+/// Named stages of the generic verifier, independent of its native or row representation.
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum Stage {
+    Announcement,
+    BusAndTables,
+    Flock,
+    Lincheck,
+    Opening,
+    Rows,
+    Target,
+    Terminal,
+    Transcript,
+    Whir,
+    Zerocheck,
+}
+
+/// A verifier: arithmetic, a transcript to read and sample, and equalities to check.
 pub trait Verifier: Arith {
     /// The next prover message, an element of `E`, read and absorbed.
     ///
@@ -227,26 +282,41 @@ pub trait Verifier: Arith {
         false
     }
 
-    /// Run `f` as a named stage of the verifier.
+    /// Start a named stage of the verifier.
     ///
-    /// A verifier that records its failed checks rather than refusing reports each under its stages' names.
-    fn scope<T>(&mut self, name: &'static str, f: impl FnOnce(&mut Self) -> T) -> T {
-        let _ = name;
-        f(self)
-    }
+    /// A verifier that records failed checks reports them under the active stages.
+    /// The caller must evaluate the stage's result, end the stage, then propagate errors.
+    /// A panicking body leaves the stage active.
+    fn begin_scope(&mut self, stage: Stage);
+
+    /// End the most recently started stage.
+    fn end_scope(&mut self);
 
     /// The next `n` prover messages.
     ///
     /// # Errors
     ///
     /// Returns an error past the end of the proof.
     fn prover_messages(&mut self, n: usize) -> Result<Vec<Self::E>, TranscriptError> {
-        (0..n).map(|_| self.prover_message()).collect()
+        // An index loop rather than a collecting closure, so no closure captures the verifier.
+        let mut out = Vec::with_capacity(n);
+        let mut i = 0;
+        while i < n {
+            out.push(self.prover_message()?);
+            i += 1;
+        }
+        Ok(out)
     }
 
     /// `n` verifier messages.
     fn verifier_messages(&mut self, n: usize) -> Vec<Self::E> {
-        (0..n).map(|_| self.verifier_message()).collect()
+        let mut out = Vec::with_capacity(n);
+        let mut i = 0;
+        while i < n {
+            out.push(self.verifier_message());
+            i += 1;
+        }
+        out
     }
 
     /// Read one sumcheck round's polynomial of `n_coeffs` coefficients, constant first.
@@ -278,9 +348,15 @@ pub trait Verifier: Arith {
         let mut coeffs = self.prover_messages(n_coeffs - 1)?;
         coeffs.insert(fixed, claim);
 
-        // The coefficients past the fixed one, summed.
+        // The coefficients past the fixed one, summed in order.
+        // An index loop rather than a folding closure, so no closure captures the verifier.
         let zero = self.zero();
-        let tail = coeffs[fixed + 1..].iter().fold(zero, |acc, &c| self.add(acc, c));
+        let mut tail = zero;
+        let mut i = fixed + 1;
+        while i < coeffs.len() {
+            tail = self.add(tail, coeffs[i]);
+            i += 1;
+        }
 
         // c_1 = claim + sum_{i>=2} c_i, or c_0 = claim + r sum_{i>=1} c_i.
         coeffs[fixed] = match eq {
@@ -342,7 +418,9 @@ impl Arith for Native {
     fn frobenius2(&mut self, a: F192) -> F192 {
         a.frobenius().frobenius()
     }
+}
 
+impl PublicMle for Native {
     fn public_mle(&mut self, values: &[F64], point: &[F192]) -> F192 {
         mle_eval_par(values, point)
     }
@@ -375,7 +453,9 @@ impl Arith for VerifierState<'_> {
     fn frobenius2(&mut self, a: F192) -> F192 {
         Native.frobenius2(a)
     }
+}
 
+impl PublicMle for VerifierState<'_> {
     fn public_mle(&mut self, values: &[F64], point: &[F192]) -> F192 {
         Native.public_mle(values, point)
     }
@@ -402,6 +482,12 @@ impl Verifier for VerifierState<'_> {
         Self::check_eof(self)
     }
 
+    #[inline]
+    fn begin_scope(&mut self, _: Stage) {}
+
+    #[inline]
+    fn end_scope(&mut self) {}
+
     fn set_hidden(&mut self, hidden: bool) {
         Self::set_hidden(self, hidden);
     }

crates/fiat_shamir/src/duplex.rs

@@ -133,6 +133,31 @@ impl Blake2sDuplex {
         T::from_uniform(repr)
     }
 
+    /// Capture the immutable logical state without flushing, hashing, squeezing, or allocating.
+    ///
+    /// A live cached output suffix is determined by the chaining value and squeeze cursor; inactive cached output has no effect on future operations.
+    #[must_use]
+    pub fn context(&self) -> crate::TranscriptContext<primitives::field::F64, [u8; 32]> {
+        let mut pending = [None; 8];
+        let (words, remainder) = self.pending[..self.n_pending].as_chunks::<8>();
+        for (slot, bytes) in pending.iter_mut().zip(words) {
+            *slot = Some(primitives::field::F64(u64::from_le_bytes(*bytes)));
+        }
+        if !remainder.is_empty() {
+            let mut padded = [0; 8];
+            padded[..remainder.len()].copy_from_slice(remainder);
+            pending[words.len()] = Some(primitives::field::F64(u64::from_le_bytes(padded)));
+        }
+        crate::TranscriptContext {
+            state: state_bytes(self.cv),
+            pending,
+            pending_bytes: self.n_pending,
+            first: self.first,
+            previous: self.previous,
+            squeezed: self.squeezed,
+        }
+    }
+
     /// Compress the pending block into the chaining value.
     ///
     /// `last` says whether it closes its absorb run.
@@ -336,6 +361,51 @@ mod tests {
         }
     }
 
+    #[test]
+    fn context_preserves_partial_absorb_and_squeeze_continuations() {
+        let input: [u8; 129] = std::array::from_fn(|i| (i + 1) as u8);
+        for pending_bytes in 0..=64 {
+            for squeezed in 0..=65 {
+                let mut sponge = Blake2sDuplex::new([17; 32]);
+                if squeezed > 0 {
+                    sponge.absorb(&input[..65]);
+                    sponge.squeeze(&mut [0; 65][..squeezed]);
+                }
+                sponge.absorb(&input[..pending_bytes]);
+                let mut before = sponge.clone();
+                let context = sponge.context();
+                assert_eq!(context, sponge.context());
+                assert_eq!(context.state, state_bytes(before.cv));
+                assert_eq!(context.pending_bytes, before.n_pending);
+                assert_eq!(context.first, before.first);
+                assert_eq!(context.previous, before.previous);
+                assert_eq!(context.squeezed, before.squeezed);
+                for (i, word) in context.pending.iter().enumerate() {
+                    let start = 8 * i;
+                    if start < pending_bytes {
+                        let end = (start + 8).min(pending_bytes);
+                        let mut padded = [0; 8];
+                        padded[..end - start].copy_from_slice(&input[start..end]);
+                        assert_eq!(*word, Some(primitives::field::F64(u64::from_le_bytes(padded))));
+                    } else {
+                        assert_eq!(*word, None);
+                    }
+                }
+                let mut actual = [0; 97];
+                let mut expected = [0; 97];
+                sponge.squeeze(&mut actual);
+                before.squeeze(&mut expected);
+                assert_eq!(actual, expected);
+                sponge.absorb(&input[..19]);
+                before.absorb(&input[..19]);
+                sponge.squeeze(&mut actual);
+                before.squeeze(&mut expected);
+                assert_eq!(actual, expected);
+                assert_eq!(sponge.context(), before.context());
+            }
+        }
+    }
+
     #[test]
     fn padding_and_squeeze_counts_are_bound() {
         // The framing tells apart transcripts a plain concatenation would merge.