fix: public input binding verification

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

@@ -167,16 +167,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 +219,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/prover/src/whir_r1cs.rs

@@ -266,7 +266,7 @@ fn prove_from_alphas(
                 &commitment.polynomial,
                 public_weight,
             );
-            merlin.prover_hint_ark(&public_eval);
+            merlin.prover_message(&public_eval);
         }
 
         let mut evaluations = compute_evaluations(&weights, &commitment.polynomial);
@@ -311,7 +311,7 @@ fn prove_from_alphas(
 
         let public_1 = if !public_inputs.is_empty() {
             let p1 = compute_public_eval(x, public_inputs.len(), &c1.polynomial);
-            merlin.prover_hint_ark(&p1);
+            merlin.prover_message(&p1);
             Some(p1)
         } else {
             None

provekit/verifier/src/whir_r1cs.rs

@@ -136,8 +136,9 @@ impl WhirR1CSVerifier for WhirR1CSScheme {
 
             let mut evaluations_1 = if !public_inputs.is_empty() {
                 let public_1: FieldElement = arthur
-                    .prover_hint_ark()
-                    .map_err(|_| anyhow::anyhow!("Failed to read public_1 hint"))?;
+                    .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 {
@@ -181,8 +182,9 @@ impl WhirR1CSVerifier for WhirR1CSScheme {
 
             let mut evaluations = if !public_inputs.is_empty() {
                 let public_eval: FieldElement = arthur
-                    .prover_hint_ark()
-                    .map_err(|_| anyhow::anyhow!("Failed to read public eval hint"))?;
+                    .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 {
@@ -273,3 +275,21 @@ pub fn run_sumcheck_verifier(
         f_at_alpha,
     })
 }
+
+/// 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,
+    public_inputs: &PublicInputs,
+) -> Result<()> {
+    let mut expected = FieldElement::one();
+    let mut x_pow = x;
+    for &pi in &public_inputs.0 {
+        expected += x_pow * pi;
+        x_pow *= x;
+    }
+    ensure!(public_eval == expected, "Public input binding check failed");
+    Ok(())
+}

tooling/provekit-bench/tests/compiler.rs

@@ -85,3 +85,50 @@ pub fn compile_workspace(workspace_path: impl AsRef<Path>) -> Result<Workspace>
 fn case_noir(path: &str) {
     test_noir_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, HashConfig};
+
+    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 = NoirCompiler::from_file(&circuit_path, HashConfig::default())
+        .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_with_toml(&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",
+    );
+}