WHIR proof is not bound to the caller-supplied statement

[Cameudis]

In the current implementation, prove() and verify() treat the caller-supplied statement as an external parameter rather than authenticated proof input.
The prover samples the initial combination challenge gamma from the transcript before observing the statement:

multilinear-toolkit/whir/src/open.rs

Line 542 in b7ceae6

statement.splice(0..0, ood_statements);

The verifier derives the same gamma from the proof transcript alone, without ever authenticating the statement:

multilinear-toolkit/whir/src/verify.rs

Lines 110 to 118 in b7ceae6

	// Combine OODS and statement constraints to claimed_sum
	let constraints: Vec<_> = prev_commitment
	.oods_constraints()
	.into_iter()
	.chain(statement)
	.collect();
	let combination_randomness =
	self.combine_constraints(verifier_state, &mut claimed_sum, &constraints)?;
	round_constraints.push((combination_randomness, constraints));

As a result, a valid proof is not cryptographically tied to the statement it is supposed to attest to.
On top of that, combine_constraints() reduces all claims to a single random linear combination and the final check validates only that aggregate:

multilinear-toolkit/whir/src/verify.rs

Lines 222 to 241 in b7ceae6

	pub(crate) fn combine_constraints(
	&self,
	verifier_state: &mut impl FSVerifier<EF>,
	claimed_sum: &mut EF,
	constraints: &[SparseStatement<EF>],
	) -> ProofResult<Vec<EF>> {
	let combination_randomness_gen: EF = verifier_state.sample();
	let mut combination_randomness = vec![EF::ONE];
	for smt in constraints {
	for e in &smt.values {
	let combination_randomness_pow = *combination_randomness.last().unwrap();
	*claimed_sum += combination_randomness_pow * e.value;
	combination_randomness
	.push(combination_randomness_pow * combination_randomness_gen);
	}
	}
	combination_randomness.pop().unwrap();
	Ok(combination_randomness)
	}

multilinear-toolkit/whir/src/verify.rs

Lines 210 to 211 in b7ceae6

	let evaluation_of_weights =
	self.eval_constraints_poly(&round_constraints, folding_randomness.clone());

This means extra claims with false values can be appended as long as they cancel each other under the combination, and the verifier still returns Ok. Concretely, a valid proof for an honest statement can be replayed against a forged statement — including injected false claims — and verification succeeds unchanged.

Suggested fix

Serialize and absorb the full statement into the Fiat-Shamir transcript before combination_randomness_gen is sampled, on both prover and verifier sides. Also add negative tests asserting that replaying a proof against a modified statement always returns Err(ProofError::InvalidProof).