fix: public input binding verification

[ashpect]

Problem

The verifier hashes public_inputs to derive the Fiat-Shamir challenge x, but the check for public_eval, the inner product ⟨[1, x, x², …], committed_poly⟩ matching those inputs was missing. The prover sends public_eval as a prover_hint_ark (not absorbed into the transcript), so a malicious prover can commit to one set of values and claim another as public output. Verification passes because WHIR only checks the evaluation claims it receives, not where they came from.

Two bugs:

1. public_eval was not transcript-bound. Sent via prover_hint_ark instead of prover_message, so it was never absorbed into Fiat-Shamir. A prover could swap it without affecting subsequent challenges.

2. Off-by-one in public weight length. make_public_weight and compute_public_eval received public_inputs.len() but the witness layout has an R1CS constant 1 at position 0 before the public inputs, so the weight vector was one element short.

Fix

Changed prover_hint_ark to prover_message for public_eval in both prover and verifier so the value is absorbed into the Fiat-Shamir transcript.

make_public_weight / compute_public_eval now internally add +1 to account for the R1CS constant at position 0. Parameter renamed to num_public_inputs to clarify semantics.

Added verify_public_input_binding() in the verifier that recomputes the expected evaluation from known public inputs and rejects if it doesn't match the prover's claim.

Added test_public_input_binding_exploit that proves honestly, then tampers public_inputs to a wrong value and asserts the verifier rejects.

[Bisht13]

/claude-review

[github-actions]

Code review

No issues found. Checked for bugs and CLAUDE.md compliance.

[Bisht13]

@claude what does this PR change?

[Bisht13]

/claude-review

[github-actions]

Claude finished @Bisht13's task in 41s —— View job

---

What this PR changes

This PR fixes a soundness vulnerability in the WHIR-based R1CS proof system where a malicious prover could substitute arbitrary public outputs without detection.

---

Bug 1: public_eval was not transcript-bound

Before: The prover sent public_eval (the inner product ⟨[1, x, x², …], witness_poly⟩) via prover_hint_ark, which is not absorbed into the Fiat-Shamir transcript. A malicious prover could swap this value after committing to the polynomial without affecting any subsequent challenges.

After: Changed to prover_message in both prover (whir_r1cs.rs:269, 314) and verifier (whir_r1cs.rs:139, 185), so the value is absorbed into the transcript and bound to the proof.

---

Bug 2: Off-by-one in public weight length

Before: make_public_weight and compute_public_eval used public_inputs.len() as the weight vector length, but the R1CS witness layout has a constant 1 at position 0 (before the public inputs). The weight vector was one element short, so the constant term was excluded.

After: Both functions now internally add +1 to account for the R1CS constant at position 0 (prefix_covector.rs:174, 231). The parameter was renamed from an implicit count to num_public_inputs to make the semantics explicit.

---

Fix 3: Added verify_public_input_binding() in the verifier

A new function (verifier/src/whir_r1cs.rs:282–295) recomputes the expected public_eval from the known public inputs and rejects if the prover's claimed value doesn't match:

fn verify_public_input_binding(public_eval, x, public_inputs) -> Result<()> {
    // Independently recomputes: 1 + x*pi[0] + x²*pi[1] + ...
    // and checks it equals the prover's claimed public_eval
}

This is called at lines 141 and 187 in the verifier for both the single-commitment and dual-commitment paths.

---

Test: test_public_input_binding_exploit

Added to tooling/provekit-bench/tests/compiler.rs — proves an honest computation (a=5, b=3 → result=16), then tampers public_inputs to claim result=42, and asserts the verifier rejects the tampered proof.

---

Summary: Before this fix, the binding between committed polynomial values and claimed public outputs was unverified, allowing a prover to commit to one set of values and claim a different public output. This PR closes that gap by transcript-binding the evaluation claim and adding an independent recomputation check in the verifier.

[github-actions]

Code review

No issues found. Checked for bugs and CLAUDE.md compliance.

[Bisht13]

/claude-review

[Bisht13]

/claude-review

[github-actions]

Code Review - Summary: This PR fixes two genuine soundness vulnerabilities in the public-input binding protocol. (1) public_eval was not Fiat-Shamir bound - sent via prover_hint_ark, letting a malicious prover commit to one polynomial and claim a different evaluation without detection. (2) Off-by-one in public weight - make_public_weight and compute_public_eval received public_inputs.len() but the R1CS witness layout places a constant 1 at position 0, so the weight vector was one element short. Review - Correctness and Soundness: The fix is correct. prover_hint_ark to prover_message for public_eval and public_1 in both prover and verifier now absorbs these values into the Fiat-Shamir sponge. n = num_public_inputs + 1 in make_public_weight and compute_public_eval correctly covers poly[0] through poly[num_public_inputs]. verify_public_input_binding recomputes the expected evaluation from known public inputs and rejects mismatches. Both single-commitment and two-commitment paths are fixed symmetrically. Test coverage note: test_public_input_binding_exploit covers the primary attack by tampering proof.public_inputs. The transcript-binding half of the fix is not directly tested - a test forging narg_string with a swapped public_eval would close that gap. Non-blocking. Code Quality: verify_public_input_binding is private, has a doc comment, uses ensure! with anyhow::Result, no unwrap in library code. Parameter rename public_inputs_len to num_public_inputs clarifies semantics. The evals vectors staying as prover_hint_ark are correct. Minor: error message omits actual vs expected values. Suggestions (non-blocking): (1) Add actual vs expected to the binding error message. (2) Add a test forging the raw transcript to directly test the Fiat-Shamir binding change. Verdict: Approve - Clean, well-scoped fix for real soundness vulnerabilities. Math is correct, both code paths addressed, regression test included, CLAUDE.md conventions respected.

[Bisht13]

/claude-review

[github-actions]

Code Review

Summary

This PR fixes two soundness bugs in the public input binding verification. First, public_eval was sent as a prover_hint_ark (outside the Fiat-Shamir transcript), allowing a malicious prover to substitute a different value without affecting subsequent challenges. Second, make_public_weight and compute_public_eval were one element short because they omitted the R1CS constant 1 at witness position 0. Both fixes are critical for correctness.

Review

Correctness & Soundness

The fixes are sound and correctly implemented.

• Transcript binding (provekit/prover/src/whir_r1cs.rs:266,311, provekit/verifier/src/whir_r1cs.rs:138,183): Both prover and verifier consistently switch prover_hint_ark → prover_message for public_eval / public_1. The alpha evaluation hints (evals, evals_1, evals_2) correctly remain as prover_hint_ark since WHIR independently verifies those commitments — only the public eval needs to be transcript-bound because it is not otherwise covered by WHIR.

• Off-by-one fix (provekit/common/src/prefix_covector.rs:170): n = num_public_inputs + 1 correctly accounts for the R1CS constant at position 0. The rename from public_inputs_len to num_public_inputs makes the +1 semantics clear.

• verify_public_input_binding (provekit/verifier/src/whir_r1cs.rs:278-295): The function correctly reconstructs the expected inner product 1 + x·pi[0] + x²·pi[1] + … from the known public inputs and the hardcoded constant 1 at position 0. The call is inserted before the WHIR weight verification, and together the two checks form a complete soundness argument: the verifier confirms (a) the prover's claim matches known public inputs, and (b) the committed polynomial actually encodes that evaluation.

• Dual-commit path: Both the single-commit and dual-commit branches in the verifier receive verify_public_input_binding. The fix is symmetric.

Code Quality

• verify_public_input_binding is private, has a doc comment, uses ensure! / anyhow::Result, no unwraps — all compliant with CLAUDE.md.
• Error messages improved ("Failed to read public_1 hint" → "Failed to read public_1").
• No new workspace dependencies introduced.

Testing

• test_public_input_binding_exploit covers the exploit scenario end-to-end on the single-commit path and is a valuable regression test.
• The off-by-one fix is indirectly exercised by the honest prove-then-verify step in the same test (verification would fail if the weight vector were still one element short).
• Non-blocking gap: there is no test exercising the dual-commit (logup/multi-commitment) path. A program that exercises num_challenges > 0 would make the dual-commit soundness fix more explicitly covered.

Suggestions

• (Non-blocking) Add an integration test or at least a note that the dual-commit path is exercised by some existing test in the suite. If no such test exists, this is worth following up with a separate PR.
• (Non-blocking) A small unit test in prefix_covector.rs comparing compute_public_eval(x, n, poly) against make_public_weight(x, n, m) dot poly would directly document and guard the +1 invariant.

Verdict

✅ Approve — both bugs are real, the fixes are correct and consistent across prover and verifier, and a meaningful exploit regression test is included.