fix: public inputs binding to transcript [LA - B]

noir-examples/basic-4/Nargo.toml

@@ -0,0 +1,5 @@
+[package]
+name = "basic"
+type = "bin"
+authors = [""]
+compiler_version = ">=0.22.0"

noir-examples/basic-4/Prover.toml

@@ -0,0 +1,2 @@
+a = "5"
+b = "3"

noir-examples/basic-4/src/main.nr

@@ -0,0 +1,9 @@
+// Basic arithmetic: addition, subtraction, multiplication.
+// Proves knowledge of (a, b) such that (a + b) * (a - b) == result.
+// Mathematically: result = a^2 - b^2.
+// Honest inputs: a = 5, b = 3 -> result = 16.
+fn main(a: Field, b: Field) -> pub Field {
+    let sum = a + b;
+    let diff = a - b;
+    sum * diff
+}

provekit/common/src/prefix_covector.rs

@@ -1,3 +1,4 @@
+
 use {
     crate::FieldElement,
     ark_std::{One, Zero},
@@ -167,16 +168,17 @@ pub fn expand_powers<const D: usize>(values: &[FieldElement]) -> Vec<FieldElemen
 
 /// Create a public weight [`PrefixCovector`] from Fiat-Shamir randomness `x`.
 ///
-/// Builds the vector `[1, x, x², …, x^{n-1}]` padded to a power of two,
-/// where `n = public_inputs_len`.
+/// Builds the vector `[1, x, x², …, x^{n-1}]` where `n = num_public_inputs +
+/// 1`.
 #[must_use]
-pub fn make_public_weight(x: FieldElement, public_inputs_len: usize, m: usize) -> PrefixCovector {
+pub fn make_public_weight(x: FieldElement, num_public_inputs: usize, m: usize) -> PrefixCovector {
+    let n = num_public_inputs + 1;
     let domain_size = 1 << m;
-    let prefix_len = public_inputs_len.next_power_of_two().max(2);
+    let prefix_len = n.next_power_of_two().max(2);
     let mut public_weights = vec![FieldElement::zero(); prefix_len];
 
     let mut current_pow = FieldElement::one();
-    for slot in public_weights.iter_mut().take(public_inputs_len) {
+    for slot in public_weights.iter_mut().take(n) {
         *slot = current_pow;
         current_pow *= x;
     }
@@ -218,17 +220,19 @@ pub fn compute_alpha_evals<const N: usize>(
         .collect()
 }
 
-/// Compute the public weight evaluation `⟨[1, x, x², …], poly⟩` without
-/// allocating a [`PrefixCovector`].
+/// Compute the public weight evaluation `⟨[1, x, x², …, x^N], poly[0..=N]⟩`
+/// without allocating a [`PrefixCovector`]. Covers the R1CS constant at
+/// position 0 and `num_public_inputs` public input positions.
 #[must_use]
 pub fn compute_public_eval(
     x: FieldElement,
-    public_inputs_len: usize,
+    num_public_inputs: usize,
     polynomial: &[FieldElement],
 ) -> FieldElement {
+    let n = num_public_inputs + 1;
     let mut eval = FieldElement::zero();
     let mut x_pow = FieldElement::one();
-    for &p in polynomial.iter().take(public_inputs_len) {
+    for &p in polynomial.iter().take(n) {
         eval += x_pow * p;
         x_pow *= x;
     }

provekit/verifier/src/whir_r1cs.rs

@@ -149,6 +149,7 @@ impl WhirR1CSVerifier for WhirR1CSScheme {
                 let public_1: FieldElement = arthur
                     .prover_message()
                     .map_err(|_| anyhow::anyhow!("Failed to read public_1"))?;
+                verify_public_input_binding(public_1, x, public_inputs)?;
                 weights_1.insert(0, make_public_weight(x, public_inputs.len(), self.m));
                 vec![public_1, evals_1[0], evals_1[1], evals_1[2]]
             } else {
@@ -216,6 +217,7 @@ impl WhirR1CSVerifier for WhirR1CSScheme {
                 let public_eval: FieldElement = arthur
                     .prover_message()
                     .map_err(|_| anyhow::anyhow!("Failed to read public eval"))?;
+                verify_public_input_binding(public_eval, x, public_inputs)?;
                 weights.insert(0, make_public_weight(x, public_inputs.len(), self.m));
                 vec![public_eval, evals[0], evals[1], evals[2]]
             } else {
@@ -309,28 +311,23 @@ pub fn run_sumcheck_verifier(
     })
 }
 
-/// Verify that `challenge_eval == Σ xⁱ · challenges[i]`.
-///
-/// The prover sends `challenge_eval` as a transcript-bound message, and WHIR
-/// verifies that it equals the inner product of `make_challenge_weight(x, …)`
-/// with the committed w2 polynomial.  This function independently recomputes
-/// the expected value from the Fiat-Shamir `challenges` (which the verifier
-/// already knows) and checks equality, ensuring the committed w2 polynomial
-/// stores the correct challenge values at the declared offsets.
-fn verify_challenge_binding(
-    challenge_eval: FieldElement,
+/// Verify that the prover's claimed public evaluation matches the known public
+/// inputs. The weight covers positions `[0, 1, ..., N]` where position 0 is the
+/// R1CS constant `1` and positions `1..=N` are the public inputs.
+fn verify_public_input_binding(
+    public_eval: FieldElement,
     x: FieldElement,
-    challenges: &[FieldElement],
+    public_inputs: &PublicInputs,
 ) -> Result<()> {
-    let mut expected = FieldElement::zero();
-    let mut x_pow = FieldElement::one();
-    for &ch in challenges {
-        expected += x_pow * ch;
+    let mut expected = FieldElement::one();
+    let mut x_pow = x;
+    for &pi in &public_inputs.0 {
+        expected += x_pow * pi;
         x_pow *= x;
     }
     ensure!(
-        challenge_eval == expected,
-        "Challenge binding check failed: prover's challenge_eval does not match expected value"
+        public_eval == expected,
+        "Public input binding check failed: expected {expected:?}, got {public_eval:?}"
     );
     Ok(())
 }

tooling/provekit-bench/tests/compiler.rs

@@ -86,3 +86,49 @@ pub fn compile_workspace(workspace_path: impl AsRef<Path>) -> Result<Workspace>
 fn case(path: &str) {
     test_compiler(path);
 }
+
+/// Verify that the verifier rejects a proof whose public inputs have been
+/// tampered with.
+#[test]
+fn test_public_input_binding_exploit() {
+    use provekit_common::{witness::PublicInputs, FieldElement};
+
+    let test_case_path = Path::new("../../noir-examples/basic-4");
+
+    compile_workspace(test_case_path).expect("Compiling workspace");
+
+    let nargo_toml_path = test_case_path.join("Nargo.toml");
+    let nargo_toml = std::fs::read_to_string(&nargo_toml_path).expect("Reading Nargo.toml");
+    let nargo_toml: NargoToml = toml::from_str(&nargo_toml).expect("Deserializing Nargo.toml");
+    let package_name = nargo_toml.package.name;
+
+    let circuit_path = test_case_path.join(format!("target/{package_name}.json"));
+    let witness_file_path = test_case_path.join("Prover.toml");
+
+    let schema = NoirProofScheme::from_file(&circuit_path).expect("Reading proof scheme");
+    let prover = Prover::from_noir_proof_scheme(schema.clone());
+    let mut verifier = Verifier::from_noir_proof_scheme(schema.clone());
+
+    // Prove honestly (a=5, b=3 -> result = (5+3)*(5-3) = 16)
+    let mut proof = prover
+        .prove(&witness_file_path)
+        .expect("While proving Noir program statement");
+
+    // Sanity: honest proof should verify
+    {
+        let mut honest_verifier = Verifier::from_noir_proof_scheme(schema);
+        honest_verifier
+            .verify(&proof)
+            .expect("Honest proof should verify");
+    }
+
+    // Tamper: the committed polynomial encodes result=16 at position 1, but we
+    // claim result=42. The verifier should reject this.
+    proof.public_inputs = PublicInputs::from_vec(vec![FieldElement::from(42u64)]);
+
+    let result = verifier.verify(&proof);
+    assert!(
+        result.is_err(),
+        "Verification should fail when public inputs are tampered, but it succeeded",
+    );
+}