diff --git a/provekit/common/src/lib.rs b/provekit/common/src/lib.rs index f54249a79..c2b0e3a9f 100644 --- a/provekit/common/src/lib.rs +++ b/provekit/common/src/lib.rs @@ -19,7 +19,7 @@ pub use { acir::FieldElement as NoirElement, ark_bn254::Fr as FieldElement, noir_proof_scheme::{NoirProof, NoirProofScheme}, - prefix_covector::{OffsetCovector, PrefixCovector}, + prefix_covector::{OffsetCovector, PrefixCovector, SparseCovector}, prover::Prover, r1cs::R1CS, verifier::Verifier, diff --git a/provekit/common/src/prefix_covector.rs b/provekit/common/src/prefix_covector.rs index 75683db01..c7ab3cd72 100644 --- a/provekit/common/src/prefix_covector.rs +++ b/provekit/common/src/prefix_covector.rs @@ -235,6 +235,100 @@ pub fn compute_public_eval( eval } +/// Covector with non-zero weights at arbitrary (possibly non-contiguous) +/// positions. Used for challenge binding where Fiat-Shamir challenge +/// witnesses may be scattered throughout the w2 polynomial. +pub struct SparseCovector { + entries: Vec<(usize, FieldElement)>, + domain_size: usize, +} + +impl SparseCovector { + /// Create a new `SparseCovector` from `(position, weight)` pairs and a + /// domain size. + pub fn new(entries: Vec<(usize, FieldElement)>, domain_size: usize) -> Self { + assert!(domain_size.is_power_of_two()); + assert!( + entries.iter().all(|&(pos, _)| pos < domain_size), + "SparseCovector: all entry positions must be < domain_size ({domain_size})" + ); + Self { + entries, + domain_size, + } + } +} + +impl LinearForm for SparseCovector { + fn size(&self) -> usize { + self.domain_size + } + + fn mle_evaluate(&self, point: &[FieldElement]) -> FieldElement { + let n = point.len(); + let mut result = FieldElement::zero(); + for &(idx, w) in &self.entries { + if w.is_zero() { + continue; + } + let mut basis = FieldElement::one(); + for (k, pk) in point.iter().enumerate() { + if (idx >> (n - 1 - k)) & 1 == 1 { + basis *= pk; + } else { + basis *= FieldElement::one() - pk; + } + } + result += w * basis; + } + result + } + + fn accumulate(&self, accumulator: &mut [FieldElement], scalar: FieldElement) { + for &(pos, w) in &self.entries { + accumulator[pos] += scalar * w; + } + } +} + +/// Build a [`SparseCovector`] that extracts the challenge positions from a w2 +/// polynomial, weighted by successive powers of `x`. +#[must_use] +pub fn make_challenge_weight( + x: FieldElement, + challenge_offsets: &[usize], + m: usize, +) -> SparseCovector { + let domain_size = 1usize << m; + let mut x_pow = FieldElement::one(); + let entries: Vec<(usize, FieldElement)> = challenge_offsets + .iter() + .map(|&pos| { + let entry = (pos, x_pow); + x_pow *= x; + entry + }) + .collect(); + SparseCovector::new(entries, domain_size) +} + +/// Evaluate `Σ xⁱ · polynomial[challenge_offsets[i]]` — the challenge binding +/// value that the prover sends as a transcript-bound message. +#[must_use] +pub fn compute_challenge_eval( + x: FieldElement, + challenge_offsets: &[usize], + polynomial: &[FieldElement], +) -> FieldElement { + let mut result = FieldElement::zero(); + let mut x_pow = FieldElement::one(); + for &pos in challenge_offsets { + result += x_pow * polynomial[pos]; + x_pow *= x; + } + result +} + #[cfg(test)] mod tests { use {super::*, whir::algebra::multilinear_extend}; @@ -430,4 +524,69 @@ mod tests { // offset + weights.len() = 7 + 2 = 9 > 8 let _ = OffsetCovector::new(vec![fe(1), fe(2)], 7, 8); } + + #[test] + fn sparse_covector_mle_matches_dense() { + let entries = vec![(0, fe(3)), (3, fe(7))]; + let sc = SparseCovector::new(entries, 4); + let mut dense = vec![FieldElement::zero(); 4]; + dense[0] = fe(3); + dense[3] = fe(7); + let pc = PrefixCovector::new(dense, 4); + let point = vec![fe(2), fe(5)]; + assert_eq!(sc.mle_evaluate(&point), pc.mle_evaluate(&point)); + } + + #[test] + fn sparse_covector_accumulate() { + let entries = vec![(1, fe(4)), (3, fe(2))]; + let sc = SparseCovector::new(entries, 4); + let mut acc = vec![FieldElement::zero(); 4]; + sc.accumulate(&mut acc, fe(3)); + assert_eq!(acc[0], FieldElement::zero()); + assert_eq!(acc[1], fe(12)); + assert_eq!(acc[2], FieldElement::zero()); + assert_eq!(acc[3], fe(6)); + } + + #[test] + fn make_challenge_weight_consistency() { + let x = fe(11); + let offsets = vec![2, 5, 9]; + let cw = make_challenge_weight(x, &offsets, 4); + assert_eq!(cw.size(), 16); + let mut poly = vec![FieldElement::zero(); 16]; + poly[2] = fe(100); + poly[5] = fe(200); + poly[9] = fe(300); + let eval = compute_challenge_eval(x, &offsets, &poly); + let mut acc = vec![FieldElement::zero(); 16]; + cw.accumulate(&mut acc, FieldElement::one()); + let dot: FieldElement = acc.iter().zip(poly.iter()).map(|(a, b)| *a * *b).sum(); + assert_eq!(eval, dot); + } + + #[test] + fn compute_challenge_eval_basic() { + let x = fe(3); + let offsets = vec![0, 2]; + let poly = vec![fe(10), fe(20), fe(30)]; + let eval = compute_challenge_eval(x, &offsets, &poly); + assert_eq!(eval, fe(10) + fe(3) * fe(30)); + } + + #[test] + fn sparse_covector_empty_entries() { + let sc = SparseCovector::new(vec![], 8); + let point = vec![fe(1), fe(2), fe(3)]; + assert_eq!(sc.mle_evaluate(&point), FieldElement::zero()); + } + + #[test] + fn sparse_covector_single_entry_matches_prefix() { + let sc = SparseCovector::new(vec![(0, fe(5))], 4); + let pc = PrefixCovector::new(vec![fe(5), FieldElement::zero()], 4); + let point = vec![fe(7), fe(11)]; + assert_eq!(sc.mle_evaluate(&point), pc.mle_evaluate(&point)); + } } diff --git a/provekit/common/src/whir_r1cs.rs b/provekit/common/src/whir_r1cs.rs index 02febb6dd..8b64a6e29 100644 --- a/provekit/common/src/whir_r1cs.rs +++ b/provekit/common/src/whir_r1cs.rs @@ -29,6 +29,7 @@ pub struct WhirR1CSScheme { pub m_0: usize, pub a_num_terms: usize, pub num_challenges: usize, + pub challenge_offsets: Vec, pub has_public_inputs: bool, pub whir_witness: WhirZkConfig, } diff --git a/provekit/common/src/witness/witness_builder.rs b/provekit/common/src/witness/witness_builder.rs index 0628fc2e3..06b0f65ee 100644 --- a/provekit/common/src/witness/witness_builder.rs +++ b/provekit/common/src/witness/witness_builder.rs @@ -295,7 +295,15 @@ impl WitnessBuilder { r1cs: R1CS, witness_map: Vec>, acir_public_inputs_indices_set: HashSet, - ) -> Result<(SplitWitnessBuilders, R1CS, Vec>, usize), SplitError> { + ) -> Result< + ( + SplitWitnessBuilders, + R1CS, + Vec>, + Vec, + ), + SplitError, + > { if witness_builders.is_empty() { return Ok(( SplitWitnessBuilders { @@ -305,7 +313,7 @@ impl WitnessBuilder { }, r1cs, witness_map, - 0, + Vec::new(), )); } @@ -358,12 +366,15 @@ impl WitnessBuilder { scheduler.build_layers() }; - let num_challenges = w2_layers + let challenge_offsets: Vec = w2_layers .layers .iter() .flat_map(|layer| &layer.witness_builders) - .filter(|b| matches!(b, WitnessBuilder::Challenge(_))) - .count(); + .filter_map(|b| match b { + WitnessBuilder::Challenge(idx) => Some(*idx - w1_size), + _ => None, + }) + .collect(); Ok(( SplitWitnessBuilders { @@ -373,7 +384,7 @@ impl WitnessBuilder { }, remapped_r1cs, remapped_witness_map, - num_challenges, + challenge_offsets, )) } } diff --git a/provekit/prover/src/whir_r1cs.rs b/provekit/prover/src/whir_r1cs.rs index 1e67a62c8..4ad07e24c 100644 --- a/provekit/prover/src/whir_r1cs.rs +++ b/provekit/prover/src/whir_r1cs.rs @@ -4,8 +4,9 @@ use { ark_std::{One, Zero}, provekit_common::{ prefix_covector::{ - build_prefix_covectors, compute_alpha_evals, compute_public_eval, expand_powers, - make_public_weight, OffsetCovector, + build_prefix_covectors, compute_alpha_evals, compute_challenge_eval, + compute_public_eval, expand_powers, make_challenge_weight, make_public_weight, + OffsetCovector, }, utils::{ pad_to_power_of_two, @@ -223,6 +224,18 @@ impl WhirR1CSProver for WhirR1CSScheme { None }; + // Challenge binding: compute eval of challenge positions in w2 and + // send as transcript-bound message so the verifier can check that + // the committed w2 polynomial contains the correct Fiat-Shamir + // challenges. + let challenge_eval = if !self.challenge_offsets.is_empty() { + let ce = compute_challenge_eval(x, &self.challenge_offsets, &c2.polynomial); + merlin.prover_message(&ce); + Some(ce) + } else { + None + }; + let WhirR1CSCommitment { witness: w1, polynomial: p1, @@ -264,12 +277,20 @@ impl WhirR1CSProver for WhirR1CSScheme { } = c2; { let weights = build_prefix_covectors(self.m, alphas_2); - let evaluations: Vec = evals_2; + let mut evaluations: Vec = evals_2; - let boxed_weights: Vec>> = weights + let mut boxed_weights: Vec>> = weights .into_iter() .map(|w| Box::new(w) as Box>) .collect(); + + if let Some(ce) = challenge_eval { + let challenge_weight = + make_challenge_weight(x, &self.challenge_offsets, self.m); + boxed_weights.push(Box::new(challenge_weight)); + evaluations.push(ce); + } + let _ = self.whir_witness.prove( &mut merlin, vec![Cow::Borrowed(p2.as_slice())], diff --git a/provekit/r1cs-compiler/src/noir_proof_scheme.rs b/provekit/r1cs-compiler/src/noir_proof_scheme.rs index b89a87847..ac0edb419 100644 --- a/provekit/r1cs-compiler/src/noir_proof_scheme.rs +++ b/provekit/r1cs-compiler/src/noir_proof_scheme.rs @@ -67,13 +67,14 @@ impl NoirProofSchemeBuilder for NoirProofScheme { let has_public_inputs = !acir_public_inputs_indices_set.is_empty(); // Split witness builders and remap indices for sound challenge generation - let (split_witness_builders, remapped_r1cs, remapped_witness_map, num_challenges) = + let (split_witness_builders, remapped_r1cs, remapped_witness_map, challenge_offsets) = WitnessBuilder::split_and_prepare_layers( &witness_builders, r1cs, witness_map, acir_public_inputs_indices_set, )?; + let num_challenges = challenge_offsets.len(); info!( "Witness split: w1 size = {}, w2 size = {}", split_witness_builders.w1_size, @@ -92,6 +93,7 @@ impl NoirProofSchemeBuilder for NoirProofScheme { &remapped_r1cs, split_witness_builders.w1_size, num_challenges, + challenge_offsets, has_public_inputs, ); diff --git a/provekit/r1cs-compiler/src/whir_r1cs.rs b/provekit/r1cs-compiler/src/whir_r1cs.rs index 330809d94..02654dad4 100644 --- a/provekit/r1cs-compiler/src/whir_r1cs.rs +++ b/provekit/r1cs-compiler/src/whir_r1cs.rs @@ -11,6 +11,7 @@ pub trait WhirR1CSSchemeBuilder { r1cs: &R1CS, w1_size: usize, num_challenges: usize, + challenge_offsets: Vec, has_public_inputs: bool, ) -> Self; @@ -22,8 +23,15 @@ impl WhirR1CSSchemeBuilder for WhirR1CSScheme { r1cs: &R1CS, w1_size: usize, num_challenges: usize, + challenge_offsets: Vec, has_public_inputs: bool, ) -> Self { + assert_eq!( + num_challenges, + challenge_offsets.len(), + "num_challenges ({num_challenges}) must equal challenge_offsets.len() ({})", + challenge_offsets.len() + ); let total_witnesses = r1cs.num_witnesses(); assert!( w1_size <= total_witnesses, @@ -49,6 +57,7 @@ impl WhirR1CSSchemeBuilder for WhirR1CSScheme { m_0, a_num_terms: next_power_of_two(r1cs.a().iter().count()), num_challenges, + challenge_offsets, whir_witness: Self::new_whir_zk_config_for_size(m_raw, 1), has_public_inputs, } diff --git a/provekit/verifier/src/whir_r1cs.rs b/provekit/verifier/src/whir_r1cs.rs index d3a148b9a..18eaf187d 100644 --- a/provekit/verifier/src/whir_r1cs.rs +++ b/provekit/verifier/src/whir_r1cs.rs @@ -3,7 +3,8 @@ use { ark_std::{One, Zero}, provekit_common::{ prefix_covector::{ - build_prefix_covectors, expand_powers, make_public_weight, OffsetCovector, + build_prefix_covectors, expand_powers, make_challenge_weight, make_public_weight, + OffsetCovector, }, utils::sumcheck::{ calculate_eq, eval_cubic_poly, multiply_transposed_by_eq_alpha, transpose_r1cs_matrices, @@ -55,16 +56,19 @@ impl WhirR1CSVerifier for WhirR1CSScheme { .receive_commitments(&mut arthur, 1) .map_err(|_| anyhow::anyhow!("Failed to parse commitment 1"))?; - let commitment_2 = if self.num_challenges > 0 { - let _logup_challenges: Vec = + let (commitment_2, logup_challenges) = if self.num_challenges > 0 { + let logup_challenges: Vec = arthur.verifier_message_vec(self.num_challenges); - Some( - self.whir_witness - .receive_commitments(&mut arthur, 1) - .map_err(|_| anyhow::anyhow!("Failed to parse commitment 2"))?, + ( + Some( + self.whir_witness + .receive_commitments(&mut arthur, 1) + .map_err(|_| anyhow::anyhow!("Failed to parse commitment 2"))?, + ), + logup_challenges, ) } else { - None + (None, Vec::new()) }; let (transposed, sumcheck_result) = rayon::join( @@ -140,7 +144,21 @@ impl WhirR1CSVerifier for WhirR1CSScheme { evals_1.to_vec() }; evaluations_1.push(blinding_eval); - let evaluations_2 = evals_2.to_vec(); + let mut evaluations_2 = evals_2.to_vec(); + + // Challenge binding: read the prover's claimed evaluation and verify + // that it matches the expected inner product of challenges with the + // committed w2 polynomial. + let challenge_weight = if !self.challenge_offsets.is_empty() { + let challenge_eval: FieldElement = arthur + .prover_message() + .map_err(|_| anyhow::anyhow!("Failed to read challenge eval"))?; + verify_challenge_binding(challenge_eval, x, &logup_challenges)?; + evaluations_2.push(challenge_eval); + Some(make_challenge_weight(x, &self.challenge_offsets, self.m)) + } else { + None + }; let mut weight_refs_1: Vec<&dyn LinearForm> = weights_1 .iter() @@ -152,10 +170,13 @@ impl WhirR1CSVerifier for WhirR1CSScheme { .verify(&mut arthur, &weight_refs_1, &evaluations_1, &commitment_1) .map_err(|_| anyhow::anyhow!("WHIR verification failed for c1"))?; - let weight_refs_2: Vec<&dyn LinearForm> = weights_2 + let mut weight_refs_2: Vec<&dyn LinearForm> = weights_2 .iter() .map(|w| w as &dyn LinearForm) .collect(); + if let Some(ref cw) = challenge_weight { + weight_refs_2.push(cw as &dyn LinearForm); + } self.whir_witness .verify(&mut arthur, &weight_refs_2, &evaluations_2, &commitment_2) .map_err(|_| anyhow::anyhow!("WHIR verification failed for c2"))?; @@ -269,3 +290,29 @@ pub fn run_sumcheck_verifier( f_at_alpha, }) } + +/// 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, + x: FieldElement, + challenges: &[FieldElement], +) -> Result<()> { + let mut expected = FieldElement::zero(); + let mut x_pow = FieldElement::one(); + for &ch in challenges { + expected += x_pow * ch; + x_pow *= x; + } + ensure!( + challenge_eval == expected, + "Challenge binding check failed: prover's challenge_eval does not match expected value" + ); + Ok(()) +}