fix: R1CS binding in transcript [LA - I]

Cargo.toml

@@ -135,6 +135,7 @@ seq-macro = "0.3.6"
 serde = { version = "1.0", features = ["derive"] }
 serde_json = "1.0"
 sha2 = { version = "0.10.9", features = ["asm"] }
+sha3 = "0.10"
 test-case = "3.3.1"
 tikv-jemallocator = "0.6"
 toml = "0.8.8"

noir-examples/babyjubjub/src/escalar_mul_fix.nr

@@ -24,10 +24,10 @@ fn segment_mul_fix_generator<let N: u32>(
 
     Then we calculate S1 = 2*2^246*B + (1 + a0)*B + (2^3 + a1)*B + .....+ (2^243 + a81)*B
 
-    And Finaly we compute the result: RES = SQ - Q
+    And Finally we compute the result: RES = SQ - Q
 
     As you can see the input of the adders cannot be equal nor zero, except for the last
-    substraction that it's done in montgomery.
+    subtraction that it's done in montgomery.
 
     A good way to see it is that the accumulator input of the adder >= 2^247*B and the other input
     is the output of the windows that it's going to be <= 2^246*B

provekit/common/Cargo.toml

@@ -40,6 +40,7 @@ rayon.workspace = true
 ruint.workspace = true
 serde.workspace = true
 serde_json.workspace = true
+sha3.workspace = true
 tracing.workspace = true
 zerocopy.workspace = true
 

provekit/common/src/lib.rs

@@ -32,7 +32,7 @@ pub use {
     r1cs::R1CS,
     transcript_sponge::TranscriptSponge,
     verifier::Verifier,
-    whir_r1cs::{WhirConfig, WhirR1CSProof, WhirR1CSScheme, WhirZkConfig},
+    whir_r1cs::{R1csHash, WhirConfig, WhirR1CSProof, WhirR1CSScheme, WhirZkConfig},
     witness::PublicInputs,
 };
 

provekit/common/src/r1cs.rs

@@ -4,6 +4,7 @@ use {
     },
     ark_ff::Zero,
     serde::{Deserialize, Serialize},
+    sha3::{Digest, Sha3_256},
     std::collections::HashMap,
 };
 
@@ -108,6 +109,16 @@ impl R1CS {
         self.a.num_cols
     }
 
+    /// Compute a SHA3-256 hash of the serialized R1CS matrices.
+    ///
+    /// Panics if postcard serialization fails, which should not happen for a
+    /// well-formed `R1CS` (all fields implement `Serialize`).
+    #[must_use]
+    pub fn hash(&self) -> crate::R1csHash {
+        let bytes = postcard::to_stdvec(self).expect("R1CS serialization should not fail");
+        crate::R1csHash::new(Sha3_256::digest(&bytes).into())
+    }
+
     // Increase the size of the R1CS matrices to the specified dimensions.
     pub fn grow_matrices(&mut self, num_rows: usize, num_cols: usize) {
         self.a.grow(num_rows, num_cols);

provekit/common/src/whir_r1cs.rs

@@ -18,6 +18,24 @@ pub type WhirZkConfig = GenericWhirZkConfig<FieldElement>;
 /// Type alias for the whir domain separator used in provekit's outer protocol.
 type WhirDomainSeparator = transcript::DomainSeparator<'static, ()>;
 
+/// SHA3-256 hash of a serialized R1CS instance, used to bind the Fiat-Shamir
+/// transcript to a concrete circuit.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
+pub struct R1csHash([u8; 32]);
+
+impl R1csHash {
+    /// Sentinel value for paths that don't have an R1CS at construction time
+    /// (e.g. `new_from_dimensions`). Will trigger a debug assertion if used
+    /// in `create_domain_separator`.
+    pub const UNSET: Self = Self([0u8; 32]);
+
+    /// Wrap a raw 32-byte digest.
+    #[must_use]
+    pub const fn new(bytes: [u8; 32]) -> Self {
+        Self(bytes)
+    }
+}
+
 #[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
 pub struct WhirR1CSScheme {
     pub m:                 usize,
@@ -28,11 +46,21 @@ pub struct WhirR1CSScheme {
     pub challenge_offsets: Vec<usize>,
     pub has_public_inputs: bool,
     pub whir_witness:      WhirZkConfig,
+    pub r1cs_hash:         R1csHash,
 }
 
 impl WhirR1CSScheme {
     /// Create a domain separator for the provekit outer protocol.
+    ///
+    /// The domain separator serializes the entire scheme (including
+    /// `r1cs_hash`) into the protocol ID, binding the Fiat-Shamir
+    /// transcript to the concrete R1CS instance.
     pub fn create_domain_separator(&self) -> WhirDomainSeparator {
+        debug_assert_ne!(
+            self.r1cs_hash,
+            R1csHash::UNSET,
+            "R1CS hash is uninitialized — transcript will not be bound to a concrete circuit"
+        );
         transcript::DomainSeparator::protocol(self)
     }
 }

provekit/common/src/witness/mod.rs

@@ -11,7 +11,7 @@ use {
         utils::{serde_ark, serde_ark_vec},
         FieldElement,
     },
-    ark_ff::{BigInt, One, PrimeField},
+    ark_ff::{BigInt, BigInteger, One, PrimeField},
     serde::{Deserialize, Serialize},
 };
 pub use {
@@ -95,6 +95,19 @@ impl PublicInputs {
             _ => self.0.iter().copied().reduce(compress).unwrap(),
         }
     }
+
+    /// Compute the public-inputs hash as a 32-byte array (little-endian).
+    ///
+    /// Used to bind public inputs to the Fiat-Shamir transcript instance.
+    #[must_use]
+    pub fn hash_bytes(&self) -> [u8; 32] {
+        let hash = self.hash();
+        let bytes = hash.into_bigint().to_bytes_le();
+        let mut result = [0u8; 32];
+        let len = bytes.len().min(32);
+        result[..len].copy_from_slice(&bytes[..len]);
+        result
+    }
 }
 
 impl Default for PublicInputs {

provekit/prover/src/lib.rs

@@ -5,14 +5,15 @@ use {
         r1cs::{CompressedLayers, CompressedR1CS},
         whir_r1cs::WhirR1CSProver,
     },
-    acir::native_types::WitnessMap,
+    acir::native_types::{Witness, WitnessMap},
     anyhow::{Context, Result},
     provekit_common::{
-        FieldElement, NoirElement, NoirProof, NoirProver, Prover, PublicInputs, TranscriptSponge,
+        utils::noir_to_native, FieldElement, NoirElement, NoirProof, NoirProver, Prover,
+        PublicInputs, TranscriptSponge,
     },
     std::mem::size_of,
     tracing::{debug, info_span, instrument},
-    whir::transcript::{codecs::Empty, ProverState},
+    whir::transcript::ProverState,
 };
 #[cfg(all(feature = "witness-generation", not(target_arch = "wasm32")))]
 use {
@@ -104,7 +105,23 @@ impl Prove for NoirProver {
     ) -> Result<NoirProof> {
         provekit_common::register_ntt();
 
-        let num_public_inputs = self.program.functions[0].public_inputs().indices().len();
+        let mut public_input_indices = self.program.functions[0].public_inputs().indices();
+        public_input_indices.sort_unstable();
+        let public_inputs = if public_input_indices.is_empty() {
+            PublicInputs::new()
+        } else {
+            let values = public_input_indices
+                .iter()
+                .map(|&idx| {
+                    let noir_val = acir_witness_idx_to_value_map
+                        .get(&Witness::from(idx))
+                        .ok_or_else(|| anyhow::anyhow!("Missing public input at index {idx}"))?;
+                    Ok(noir_to_native(*noir_val))
+                })
+                .collect::<Result<Vec<_>>>()?;
+            PublicInputs::from_vec(values)
+        };
+
         drop(self.program);
         drop(self.witness_generator);
 
@@ -115,18 +132,17 @@ impl Prove for NoirProver {
         let num_witnesses = compressed_r1cs.num_witnesses();
         let num_constraints = compressed_r1cs.num_constraints();
 
-        // Set up transcript with sponge selected by hash_config.
+        // Set up transcript with public inputs bound to the instance.
+        let instance = public_inputs.hash_bytes();
         let ds = self
             .whir_for_witness
             .create_domain_separator()
-            .instance(&Empty);
+            .instance(&instance);
         let mut merlin = ProverState::new(&ds, TranscriptSponge::from_config(self.hash_config));
 
         let mut witness: Vec<Option<FieldElement>> = vec![None; num_witnesses];
 
         // Solve w1 (or all witnesses if no challenges).
-        // Outer span captures memory AFTER w1_layers parameter is freed
-        // (parameter drop happens before outer span close).
         {
             let _s = info_span!("solve_w1").entered();
             crate::r1cs::solve_witness_vec(
@@ -215,17 +231,6 @@ impl Prove for NoirProver {
         r1cs.test_witness_satisfaction(&witness.iter().map(|w| w.unwrap()).collect::<Vec<_>>())
             .context("While verifying R1CS instance")?;
 
-        let public_inputs = if num_public_inputs == 0 {
-            PublicInputs::new()
-        } else {
-            PublicInputs::from_vec(
-                witness[1..=num_public_inputs]
-                    .iter()
-                    .map(|w| w.ok_or_else(|| anyhow::anyhow!("Missing public input witness")))
-                    .collect::<Result<Vec<FieldElement>>>()?,
-            )
-        };
-
         let full_witness: Vec<FieldElement> = witness
             .into_iter()
             .enumerate()
@@ -258,10 +263,19 @@ impl Prove for MavrosProver {
             &params,
         );
 
+        let num_public_inputs = self.num_public_inputs;
+        let public_inputs = if num_public_inputs == 0 {
+            PublicInputs::new()
+        } else {
+            PublicInputs::from_vec(phase1.out_wit_pre_comm[1..=num_public_inputs].to_vec())
+        };
+
+        // Set up transcript with public inputs bound to the instance.
+        let instance = public_inputs.hash_bytes();
         let ds = self
             .whir_for_witness
             .create_domain_separator()
-            .instance(&Empty);
+            .instance(&instance);
         let mut merlin = ProverState::new(&ds, TranscriptSponge::from_config(self.hash_config));
 
         let commitment_1 = self
@@ -275,7 +289,7 @@ impl Prove for MavrosProver {
             )
             .context("While committing to w1")?;
 
-        let (commitments, witgen_result) = if self.whir_for_witness.num_challenges > 0 {
+        let commitments = if self.whir_for_witness.num_challenges > 0 {
             let challenges: Vec<FieldElement> = (0..self.witness_layout.challenges_size)
                 .map(|_| merlin.verifier_message())
                 .collect();
@@ -298,22 +312,15 @@ impl Prove for MavrosProver {
                 )
                 .context("While committing to w2")?;
 
-            (vec![commitment_1, commitment_2], witgen_result)
+            vec![commitment_1, commitment_2]
         } else {
-            let witgen_result = mavros_interpreter::run_phase2(
+            mavros_interpreter::run_phase2(
                 phase1.clone(),
                 &[],
                 self.witness_layout,
                 self.constraints_layout,
             );
-            (vec![commitment_1], witgen_result)
-        };
-
-        let num_public_inputs = self.num_public_inputs;
-        let public_inputs = if num_public_inputs == 0 {
-            PublicInputs::new()
-        } else {
-            PublicInputs::from_vec(witgen_result.out_wit_pre_comm[1..=num_public_inputs].to_vec())
+            vec![commitment_1]
         };
 
         let whir_r1cs_proof = self

provekit/r1cs-compiler/src/noir_proof_scheme.rs

@@ -164,16 +164,17 @@ impl MavrosCompiler {
         // In Mavros, challenges occupy the first `challenges_size` positions of
         // w2 (immediately after the pre-commitment boundary).
         let challenge_offsets: Vec<usize> = (0..challenges_size).collect();
-        let whir_for_witness = WhirR1CSScheme::new_from_mavros_r1cs(
+        let r1cs = convert_mavros_r1cs_to_provekit(&mavros_r1cs);
+
+        let mut whir_for_witness = WhirR1CSScheme::new_from_mavros_r1cs(
             &mavros_r1cs,
             mavros_r1cs.witness_layout.pre_commitment_size(),
             challenges_size,
             challenge_offsets,
             num_public_inputs > 0,
             hash_config.engine_id(),
         );
-
-        let r1cs = convert_mavros_r1cs_to_provekit(&mavros_r1cs);
+        whir_for_witness.r1cs_hash = r1cs.hash();
 
         Ok(NoirProofScheme::Mavros(MavrosSchemeData {
             abi,

provekit/r1cs-compiler/src/whir_r1cs.rs

@@ -1,6 +1,6 @@
 use {
     mavros_artifacts::R1CS as MavrosR1CS,
-    provekit_common::{utils::next_power_of_two, WhirR1CSScheme, WhirZkConfig, R1CS},
+    provekit_common::{utils::next_power_of_two, R1csHash, WhirR1CSScheme, WhirZkConfig, R1CS},
     whir::{engines::EngineId, parameters::ProtocolParameters},
 };
 
@@ -87,6 +87,7 @@ impl WhirR1CSSchemeBuilder for WhirR1CSScheme {
             challenge_offsets,
             whir_witness: Self::new_whir_zk_config_for_size(m_raw, 1, hash_id),
             has_public_inputs,
+            r1cs_hash: r1cs.hash(),
         }
     }
 
@@ -175,6 +176,7 @@ impl WhirR1CSSchemeBuilder for WhirR1CSScheme {
             num_challenges,
             challenge_offsets,
             has_public_inputs,
+            r1cs_hash: R1csHash::UNSET,
         }
     }
 }

provekit/verifier/src/whir_r1cs.rs

@@ -15,7 +15,7 @@ use {
     tracing::instrument,
     whir::{
         algebra::linear_form::LinearForm,
-        transcript::{codecs::Empty, Proof, VerifierMessage, VerifierState},
+        transcript::{Proof, VerifierMessage, VerifierState},
     },
 };
 
@@ -45,7 +45,16 @@ impl WhirR1CSVerifier for WhirR1CSScheme {
         r1cs: &R1CS,
         hash_config: HashConfig,
     ) -> Result<()> {
-        let ds = self.create_domain_separator().instance(&Empty);
+        let actual_r1cs_hash = r1cs.hash();
+        anyhow::ensure!(
+            self.r1cs_hash == actual_r1cs_hash,
+            "R1CS hash mismatch: scheme expects {:?}, got {:?}",
+            self.r1cs_hash,
+            actual_r1cs_hash
+        );
+
+        let instance = public_inputs.hash_bytes();
+        let ds = self.create_domain_separator().instance(&instance);
         let whir_proof = Proof {
             narg_string: proof.narg_string.clone(),
             hints: proof.hints.clone(),