stop observing some transcript twice in fiat shamir

Author: TomWambsgans

crates/fiat_shamir/src/transcript.rs

@@ -1,4 +1,4 @@
-//! Fiat-Shamir proof transport. `add_scalar` and `next_scalar` transmit and bind together. `observe_scalar` is only for public values both sides derive. Merkle hints are authenticated by their trees and are not absorbed separately.
+//! Fiat-Shamir proof transport. `add_scalar` and `next_scalar` transmit and bind together, which is the only way anything enters the state: a transmitted value needs no separate absorb, a value derived from transmitted ones needs none either, and the statement rides the seed the state starts from. So there is no absorb-only method at all. Merkle hints are authenticated by their trees and are not absorbed separately.
 
 use crate::FiatShamirState;
 use crate::merkle::{Hash, PrunedMerklePaths, RawMerklePath, hash_to_scalars, scalars_to_hash};
@@ -36,18 +36,6 @@ pub enum Error {
 pub trait Challenger {
     fn sample(&mut self) -> F192;
     fn sample_vec(&mut self, n: usize) -> Vec<F192>;
-    /// Bind a value both sides derive themselves (never transmitted), so it is
-    /// side-agnostic and lives here rather than on the two halves below.
-    fn observe_scalar(&mut self, x: F192);
-
-    /// Bind a root both sides already hold (a commitment that is part of the
-    /// statement) as its two scalars, not as a byte string, so the recursion
-    /// guest replays one shape for every digest.
-    fn observe_root(&mut self, root: &Hash) {
-        for s in hash_to_scalars(root) {
-            self.observe_scalar(s);
-        }
-    }
 }
 
 /// The prover half of a transmitting sub-protocol (WHIR and its sumchecks):
@@ -323,9 +311,6 @@ impl Challenger for ProverState {
     fn sample_vec(&mut self, n: usize) -> Vec<F192> {
         self.fs.sample_vec(n)
     }
-    fn observe_scalar(&mut self, x: F192) {
-        self.fs.observe(x);
-    }
 }
 
 impl Challenger for VerifierState<'_> {
@@ -335,12 +320,6 @@ impl Challenger for VerifierState<'_> {
     fn sample_vec(&mut self, n: usize) -> Vec<F192> {
         self.fs.sample_vec(n)
     }
-    /// Absorb a value both parties compute themselves (never transmitted):
-    /// protocol steps that bind derived values before sampling, e.g. the
-    /// stacked-bytecode claim reduction (`leaf::verify_balance`).
-    fn observe_scalar(&mut self, x: F192) {
-        self.fs.observe(x);
-    }
 }
 
 #[cfg(test)]

crates/flock/src/lib.rs

@@ -25,8 +25,8 @@
 //! gadgets, forwards and transposed, kept separate because the fused
 //! three-operand adder's bit boundaries are the subtlest thing here.
 
-pub mod hash;
 mod gf2;
+pub mod hash;
 pub mod lincheck;
 /// The circuit driven through the whole reduction. A `src` module rather than
 /// its own test binary so it shares the process, and so the slow

crates/lean_compiler/tests/suite/inline_expr.rs

@@ -7,8 +7,8 @@
 //! `let`.
 
 use lean_compiler::{compile, parse};
-use lean_vm::hash_flock::warm_setup;
 use lean_vm::cpu::{prove, verify};
+use lean_vm::hash_flock::warm_setup;
 use primitives::field::{F64, F192};
 
 #[test]

crates/lean_compiler/tests/suite/pack64x2.rs

@@ -1,6 +1,6 @@
 use lean_compiler::{compile, parse};
-use lean_vm::hash_flock::warm_setup;
 use lean_vm::cpu::{prove, verify};
+use lean_vm::hash_flock::warm_setup;
 use primitives::field::{F64, F192};
 
 use crate::common::mix;

crates/lean_compiler/tests/suite/print_debug.rs

@@ -2,8 +2,8 @@
 //! witness generation, and leave proving/verification untouched.
 
 use lean_compiler::{compile, parse};
-use lean_vm::hash_flock::warm_setup;
 use lean_vm::cpu::{prove, verify};
+use lean_vm::hash_flock::warm_setup;
 use primitives::field::{F64, F192};
 
 #[test]

crates/lean_compiler/tests/suite/stack_buf.rs

@@ -10,8 +10,8 @@
 //!: the reference `compress` is fed that lane layout.
 
 use lean_compiler::{compile, parse};
-use lean_vm::hash_flock::{compression, digest, metadata, unpack_metadata, warm_setup};
 use lean_vm::cpu::{Op, prove, verify};
+use lean_vm::hash_flock::{compression, digest, metadata, unpack_metadata, warm_setup};
 use lean_vm::vmhash::compress;
 use primitives::field::{F64, F192};
 

crates/lean_compiler/tests/suite/vm_proofs.rs

@@ -7,8 +7,8 @@
 //! duplicating their knowledge of what a dummy row looks like.
 
 use lean_compiler::{compile, parse};
-use lean_vm::hash_flock::warm_setup;
 use lean_vm::cpu::{Error, Proof, prove, verify};
+use lean_vm::hash_flock::warm_setup;
 use lean_vm::vmhash::compress;
 use primitives::field::{F64, F192};
 

crates/lean_vm/src/cpu/mod.rs

@@ -832,11 +832,7 @@ mod tests {
                 ins: [2, 3, 4, 5],
                 cv: 0,
                 out: 6,
-                metadata: crate::hash_flock::metadata(
-                    crate::hash_flock::PINNED_T,
-                    crate::hash_flock::FINAL_FLAG,
-                    0,
-                ),
+                metadata: crate::hash_flock::metadata(crate::hash_flock::PINNED_T, crate::hash_flock::FINAL_FLAG, 0),
             },
         ]; // c → cells 6,7
         // 16 slots: 5 executed, then 10 filler SETs step the pc to 15, whose slot is
@@ -923,11 +919,7 @@ mod tests {
                 ins: [2, 3, 2, 3],
                 cv: 0,
                 out: 4,
-                metadata: crate::hash_flock::metadata(
-                    crate::hash_flock::PINNED_T,
-                    crate::hash_flock::FINAL_FLAG,
-                    0,
-                ),
+                metadata: crate::hash_flock::metadata(crate::hash_flock::PINNED_T, crate::hash_flock::FINAL_FLAG, 0),
             },
         ];
         // 8 slots: 3 executed, 4 filler SETs stepping the pc, then the sentinel.

crates/lean_vm/src/lib.rs

@@ -20,11 +20,11 @@
 //! - [`hash_flock`]: the `BLAKE2s` glue: flock's R1CS validity proof over the same commitment.
 //! - [`vmhash`]: VM-native hashing (one-block compression and standard BLAKE2s slice hashing).
 
-pub mod hash_flock;
 pub mod colval;
 pub mod constraints;
 pub mod cpu;
 pub mod gkr;
+pub mod hash_flock;
 pub mod leaf;
 pub mod pcs;
 pub mod tables;

crates/pcs/src/stack_open.rs

@@ -31,9 +31,10 @@
 //! ## Transcript order (identical on both sides)
 //!
 //! label -> shared linear map sampled ([`super::ring_switch`]'s own label; the
-//! claims' slices were bound by the caller, so none are sent here) -> per point
-//! claim (label + value observed) -> lambda (ONE challenge for both families) ->
-//! WHIR, with domain-separated labels for every phase.
+//! claims' slices were bound by the caller, so none are sent here) -> lambda (ONE
+//! challenge for both families) -> WHIR, with domain-separated labels for every
+//! phase. No claim value is observed here: each was bound by the stream read that
+//! produced it, so lambda already depends on every one of them.
 //!
 //! ## The combined weight
 //!
@@ -393,11 +394,9 @@ pub fn open_batch_mixed_whir_stacked(
     let map_challenges = ring_switch::sample_map_challenges(ps);
     let coordinate_weights = ring_switch::build_coordinate_weights(&map_challenges);
 
-    // 2. Point-claim values, then the ONE batching challenge both families take
-    //    disjoint power ranges of.
-    for claim in point_claims {
-        ps.observe_scalar(claim.value());
-    }
+    // 2. The ONE batching challenge both families take disjoint power ranges of. Nothing is
+    //    observed first: every claim value reached the caller through a binding stream read, so
+    //    the challenge already depends on all of them (`lean_vm::pcs::open`).
     let lambdas = powers(ps.sample(), ring.claims.len() + point_claims.len());
     let (lambdas_rs, lambdas_pd) = lambdas.split_at(ring.claims.len());
 
@@ -514,11 +513,8 @@ pub fn verify_opening_batch_mixed_whir_stacked(
     let map_challenges = ring_switch::sample_map_challenges(vs);
     let coordinate_weights = ring_switch::build_coordinate_weights(&map_challenges);
 
-    // 2. Point-claim values, then the one batching challenge, then fold both
-    //    families into the target over disjoint power ranges.
-    for claim in point_claims {
-        vs.observe_scalar(claim.value());
-    }
+    // 2. The one batching challenge (see the opener: the claim values are bound by the read that
+    //    produced them), then fold both families into the target over disjoint power ranges.
     let lambdas = powers(vs.sample(), n_rs + point_claims.len());
     let (lambdas_rs, lambdas_pd) = lambdas.split_at(n_rs);