From 1ccc431360f7b58401f1770f29e0cdb6f5d3eee9 Mon Sep 17 00:00:00 2001 From: Tej Qu Nair Date: Fri, 9 Aug 2024 18:38:51 -0700 Subject: [PATCH 1/3] (wip, doesn't compile) making verify circuit more generic --- recursion/circuit-v2/src/challenger.rs | 38 +++++++------ recursion/circuit-v2/src/fri.rs | 70 +++++++++++++---------- recursion/circuit-v2/src/lib.rs | 78 +++++++++++++++++++++++++- recursion/circuit-v2/src/stark.rs | 5 +- 4 files changed, 141 insertions(+), 50 deletions(-) diff --git a/recursion/circuit-v2/src/challenger.rs b/recursion/circuit-v2/src/challenger.rs index 730467d592..f8e51472b4 100644 --- a/recursion/circuit-v2/src/challenger.rs +++ b/recursion/circuit-v2/src/challenger.rs @@ -34,6 +34,8 @@ pub trait FeltChallenger: CanObserveVariable> + CanSampleVariable> + CanSampleBitsVariable { fn sample_ext(&mut self, builder: &mut Builder) -> Ext; + + fn check_witness(&mut self, builder: &mut Builder, nb_bits: usize, witness: Felt); } pub trait CanSampleBitsVariable { @@ -128,14 +130,6 @@ impl DuplexChallengerVariable { .expect("output buffer should be non-empty") } - pub fn sample_ext(&mut self, builder: &mut Builder) -> Ext { - let a = self.sample(builder); - let b = self.sample(builder); - let c = self.sample(builder); - let d = self.sample(builder); - builder.ext_from_base_slice(&[a, b, c, d]) - } - pub fn sample_bits(&mut self, builder: &mut Builder, nb_bits: usize) -> Vec> { assert!(nb_bits <= NUM_BITS); let rand_f = self.sample(builder); @@ -143,14 +137,6 @@ impl DuplexChallengerVariable { rand_f_bits.truncate(nb_bits); rand_f_bits } - - pub fn check_witness(&mut self, builder: &mut Builder, nb_bits: usize, witness: Felt) { - self.observe(builder, witness); - let element_bits = self.sample_bits(builder, nb_bits); - for bit in element_bits { - builder.assert_felt_eq(bit, C::F::zero()); - } - } } impl CanObserveVariable> for DuplexChallengerVariable { @@ -212,7 +198,24 @@ impl CanObserveVariable> for DuplexChallen impl FeltChallenger for DuplexChallengerVariable { fn sample_ext(&mut self, builder: &mut Builder) -> Ext { - DuplexChallengerVariable::sample_ext(self, builder) + let a = self.sample(builder); + let b = self.sample(builder); + let c = self.sample(builder); + let d = self.sample(builder); + builder.ext_from_base_slice(&[a, b, c, d]) + } + + fn check_witness( + &mut self, + builder: &mut Builder, + nb_bits: usize, + witness: Felt<::F>, + ) { + self.observe(builder, witness); + let element_bits = self.sample_bits(builder, nb_bits); + for bit in element_bits { + builder.assert_felt_eq(bit, C::F::zero()); + } } } @@ -238,6 +241,7 @@ pub(crate) mod tests { use sp1_recursion_core_v2::Runtime; use crate::challenger::DuplexChallengerVariable; + use crate::challenger::FeltChallenger; use crate::witness::Witness; use sp1_core::utils::run_test_machine; diff --git a/recursion/circuit-v2/src/fri.rs b/recursion/circuit-v2/src/fri.rs index 71cccbc161..d28e7422e4 100644 --- a/recursion/circuit-v2/src/fri.rs +++ b/recursion/circuit-v2/src/fri.rs @@ -14,20 +14,21 @@ use std::{ ops::{Add, Mul}, }; -use crate::challenger::DuplexChallengerVariable; +use crate::challenger::CanSampleBitsVariable; +use crate::challenger::FeltChallenger; use crate::*; -pub fn verify_shape_and_sample_challenges( +pub fn verify_shape_and_sample_challenges>( builder: &mut Builder, - config: &FriConfig, + config: &FriConfig>, proof: &FriProofVariable, - challenger: &mut DuplexChallengerVariable, + challenger: &mut SC::FriChallengerVariable, ) -> FriChallenges { let betas = proof .commit_phase_commits .iter() .map(|&commitment| { - challenger.observe_commitment(builder, commitment); + challenger.observe_slice(builder, commitment); challenger.sample_ext(builder) }) .collect(); @@ -53,17 +54,17 @@ pub fn verify_shape_and_sample_challenges( } } -pub fn verify_two_adic_pcs( +pub fn verify_two_adic_pcs>( builder: &mut Builder, - config: &FriConfig, + config: &FriConfig>, proof: &TwoAdicPcsProofVariable, - challenger: &mut DuplexChallengerVariable, + challenger: &mut SC::FriChallengerVariable, rounds: Vec>, ) { let alpha = challenger.sample_ext(builder); let fri_challenges = - verify_shape_and_sample_challenges(builder, config, &proof.fri_proof, challenger); + verify_shape_and_sample_challenges::(builder, config, &proof.fri_proof, challenger); let log_global_max_height = proof.fri_proof.commit_phase_commits.len() + config.log_blowup; @@ -73,12 +74,11 @@ pub fn verify_two_adic_pcs( .zip(&fri_challenges.query_indices) .map(|(query_opening, index_bits)| { // The powers of alpha, where the ith element is alpha^i. - let mut alpha_pows: Vec> = - [builder.constant(C::EF::one()); 32].to_vec(); + let mut alpha_pows: [Ext; 32] = [builder.constant(C::EF::one()); 32]; let mut ro: [Ext; 32] = [builder.eval(SymbolicExt::from_f(C::EF::zero())); 32]; - for (batch_opening, round) in izip!(query_opening, rounds.iter().cloned()) { + for (batch_opening, round) in zip(query_opening, rounds.iter().cloned()) { let batch_commit = round.batch_commit; let mats = round.mats; let batch_heights = mats @@ -96,7 +96,7 @@ pub fn verify_two_adic_pcs( let reduced_index_bits = index_bits[bits_reduced..].to_vec(); - verify_batch::( + verify_batch::( builder, batch_commit, batch_dims, @@ -104,6 +104,7 @@ pub fn verify_two_adic_pcs( batch_opening.opened_values.clone(), batch_opening.opening_proof.clone(), ); + for (mat_opening, mat) in izip!(&batch_opening.opened_values, mats) { let mat_domain = mat.domain; let mat_points = mat.points; @@ -137,7 +138,7 @@ pub fn verify_two_adic_pcs( }) .collect::>(); - verify_challenges( + verify_challenges::( builder, config, &proof.fri_proof, @@ -146,9 +147,9 @@ pub fn verify_two_adic_pcs( ); } -pub fn verify_challenges( +pub fn verify_challenges>( builder: &mut Builder, - config: &FriConfig, + config: &FriConfig>, proof: &FriProofVariable, challenges: &FriChallenges, reduced_openings: Vec<[Ext; 32]>, @@ -160,7 +161,7 @@ pub fn verify_challenges( .zip(&proof.query_proofs) .zip(reduced_openings) { - let folded_eval = verify_query( + let folded_eval = verify_query::( builder, proof.commit_phase_commits.clone(), index_bits, @@ -174,7 +175,7 @@ pub fn verify_challenges( } } -pub fn verify_query( +pub fn verify_query>( builder: &mut Builder, commit_phase_commits: Vec>, index_bits: &[Felt], @@ -219,7 +220,7 @@ pub fn verify_query( width: 2, height: (1 << log_folded_height), }]; - verify_batch::( + verify_batch::( builder, commit, dims.to_vec(), @@ -238,7 +239,7 @@ pub fn verify_query( folded_eval } -pub fn verify_batch( +pub fn verify_batch, const D: usize>( builder: &mut Builder, commit: DigestVariable, dimensions: Vec, @@ -312,10 +313,9 @@ where C: Config, R: Variable + Into<>::Expression> + 'a, S: Variable + Into<>::Expression> + 'a, - >::Expression: AbstractField + 'a, + >::Expression: AbstractField, >::Expression: Add>::Expression> - + Mul<>::Expression, Output = >::Expression> - + 'a, + + Mul<>::Expression, Output = >::Expression>, { let should_swap: >::Expression = should_swap.into(); let one = >::Expression::one(); @@ -560,7 +560,7 @@ mod tests { .into_iter() .map(|p| p.map(|x| builder.eval(x))) .collect(); - verify_batch::<_, 1>( + verify_batch::<_, SC, 1>( &mut builder, commit, large_mat_dims @@ -633,11 +633,15 @@ mod tests { let mut challenger = DuplexChallengerVariable::new(&mut builder); let commit: [_; DIGEST_SIZE] = commit.into(); - let commit = commit.map(|x| builder.eval(x)); - challenger.observe_commitment(&mut builder, commit); + let commit: [Felt; DIGEST_SIZE] = commit.map(|x| builder.eval(x)); + challenger.observe_slice(&mut builder, commit); let _ = challenger.sample_ext(&mut builder); - let fri_challenges = - verify_shape_and_sample_challenges(&mut builder, &config, &fri_proof, &mut challenger); + let fri_challenges = verify_shape_and_sample_challenges::( + &mut builder, + &config, + &fri_proof, + &mut challenger, + ); for i in 0..fri_challenges_gt.betas.len() { builder.assert_ext_eq( @@ -719,11 +723,17 @@ mod tests { let proof = const_two_adic_pcs_proof(&mut builder, proof); let (commit, rounds) = const_two_adic_pcs_rounds(&mut builder, commit.into(), os); let mut challenger = DuplexChallengerVariable::new(&mut builder); - challenger.observe_commitment(&mut builder, commit); + challenger.observe_slice(&mut builder, commit); let x2 = challenger.sample_ext(&mut builder); let x1: Ext<_, _> = builder.constant(x1); builder.assert_ext_eq(x1, x2); - verify_two_adic_pcs(&mut builder, &config, &proof, &mut challenger, rounds); + verify_two_adic_pcs::<_, BabyBearPoseidon2>( + &mut builder, + &config, + &proof, + &mut challenger, + rounds, + ); run_test_recursion(builder.operations, std::iter::empty()); // let mut backend = ConstraintCompiler::::default(); diff --git a/recursion/circuit-v2/src/lib.rs b/recursion/circuit-v2/src/lib.rs index cac1d8aafb..e93a31ff63 100644 --- a/recursion/circuit-v2/src/lib.rs +++ b/recursion/circuit-v2/src/lib.rs @@ -1,7 +1,11 @@ //! Copied from [`sp1_recursion_program`]. +use challenger::{CanObserveVariable, DuplexChallengerVariable, FeltChallenger}; use p3_commit::TwoAdicMultiplicativeCoset; -use sp1_recursion_compiler::ir::{Config, Ext, Felt}; +use sp1_recursion_compiler::{ + config::InnerConfig, + ir::{Config, Ext, Felt}, +}; use sp1_recursion_core_v2::DIGEST_SIZE; pub mod build_wrap_v2; @@ -66,3 +70,75 @@ pub struct TwoAdicPcsMatsVariable { pub points: Vec>, pub values: Vec>>, } + +use p3_challenger::{CanObserve, CanSample, FieldChallenger, GrindingChallenger}; +use p3_commit::{ExtensionMmcs, Mmcs}; +use p3_dft::Radix2DitParallel; +use p3_fri::{FriConfig, TwoAdicFriPcs}; +use p3_matrix::dense::RowMajorMatrix; +use sp1_recursion_core::stark::config::{BabyBearPoseidon2Outer, OuterValMmcs}; + +use p3_baby_bear::BabyBear; +use sp1_core::{ + stark::{PcsProverData, StarkGenericConfig}, + utils::BabyBearPoseidon2, +}; + +type EF = ::Challenge; + +pub type PcsConfig = FriConfig< + ExtensionMmcs< + ::Val, + ::Challenge, + ::ValMmcs, + >, +>; + +pub type FriMmcs = ExtensionMmcs::ValMmcs>; + +pub trait BabyBearFriConfig: + StarkGenericConfig< + Val = BabyBear, + Challenge = EF, + Challenger = Self::FriChallenger, + Pcs = TwoAdicFriPcs< + BabyBear, + Radix2DitParallel, + Self::ValMmcs, + ExtensionMmcs, + >, +> +{ + type ValMmcs: Mmcs; + // type RowMajorProverData: Clone; + type FriChallenger: CanObserve<>::Commitment> + + CanSample + + GrindingChallenger + + FieldChallenger; +} + +// TODO write subtrait that enables use of the Variable variants +// consider merging this into the above trait +pub trait BabyBearFriConfigVariable: BabyBearFriConfig { + // Is this is the best place to put this? + type C: Config; + type FriChallengerVariable: FeltChallenger; +} + +impl BabyBearFriConfig for BabyBearPoseidon2 { + type ValMmcs = sp1_core::utils::baby_bear_poseidon2::ValMmcs; + // type RowMajorProverData = PcsProverData; + type FriChallenger = ::Challenger; +} + +impl BabyBearFriConfigVariable for BabyBearPoseidon2 { + type C = InnerConfig; + + type FriChallengerVariable = DuplexChallengerVariable; +} + +impl BabyBearFriConfig for BabyBearPoseidon2Outer { + type ValMmcs = OuterValMmcs; + // type RowMajorProverData = PcsProverData; + type FriChallenger = ::Challenger; +} diff --git a/recursion/circuit-v2/src/stark.rs b/recursion/circuit-v2/src/stark.rs index 2534b86793..13c1a4145b 100644 --- a/recursion/circuit-v2/src/stark.rs +++ b/recursion/circuit-v2/src/stark.rs @@ -27,6 +27,7 @@ use utils::get_sorted_indices; use crate::challenger::*; use crate::domain::*; +use crate::fri::verify_two_adic_pcs; use crate::*; // use crate::commit::PolynomialSpaceVariable; // use crate::fri::types::TwoAdicPcsMatsVariable; @@ -152,7 +153,7 @@ impl<'a, SC: StarkGenericConfig, A: MachineAir> VerifyingKeyHint<'a, SC } } -impl StarkVerifier +impl StarkVerifier where C::F: TwoAdicField, SC: StarkGenericConfig< @@ -329,7 +330,7 @@ where // Verify the pcs proof // builder.cycle_tracker("stage-d-verify-pcs"); let config = inner_fri_config(); - crate::fri::verify_two_adic_pcs(builder, &config, opening_proof, challenger, rounds); + verify_two_adic_pcs::<_, _>(builder, &config, opening_proof, challenger, rounds); // builder.cycle_tracker("stage-d-verify-pcs"); // builder.cycle_tracker("stage-e-verify-constraints"); From 8fab0e44c6bc700227afbd021ee600b261b55fc6 Mon Sep 17 00:00:00 2001 From: Tej Qu Nair Date: Mon, 12 Aug 2024 11:57:56 -0700 Subject: [PATCH 2/3] compiles --- recursion/circuit-v2/src/lib.rs | 17 ++++++++++----- recursion/circuit-v2/src/stark.rs | 35 ++++++++++++------------------- 2 files changed, 25 insertions(+), 27 deletions(-) diff --git a/recursion/circuit-v2/src/lib.rs b/recursion/circuit-v2/src/lib.rs index e93a31ff63..33524cafe4 100644 --- a/recursion/circuit-v2/src/lib.rs +++ b/recursion/circuit-v2/src/lib.rs @@ -79,10 +79,7 @@ use p3_matrix::dense::RowMajorMatrix; use sp1_recursion_core::stark::config::{BabyBearPoseidon2Outer, OuterValMmcs}; use p3_baby_bear::BabyBear; -use sp1_core::{ - stark::{PcsProverData, StarkGenericConfig}, - utils::BabyBearPoseidon2, -}; +use sp1_core::{stark::StarkGenericConfig, utils::BabyBearPoseidon2}; type EF = ::Challenge; @@ -115,13 +112,15 @@ pub trait BabyBearFriConfig: + CanSample + GrindingChallenger + FieldChallenger; + + fn fri_config(&self) -> &FriConfig>; } // TODO write subtrait that enables use of the Variable variants // consider merging this into the above trait pub trait BabyBearFriConfigVariable: BabyBearFriConfig { // Is this is the best place to put this? - type C: Config; + type C: Config; type FriChallengerVariable: FeltChallenger; } @@ -129,6 +128,10 @@ impl BabyBearFriConfig for BabyBearPoseidon2 { type ValMmcs = sp1_core::utils::baby_bear_poseidon2::ValMmcs; // type RowMajorProverData = PcsProverData; type FriChallenger = ::Challenger; + + fn fri_config(&self) -> &FriConfig> { + self.pcs().fri_config() + } } impl BabyBearFriConfigVariable for BabyBearPoseidon2 { @@ -141,4 +144,8 @@ impl BabyBearFriConfig for BabyBearPoseidon2Outer { type ValMmcs = OuterValMmcs; // type RowMajorProverData = PcsProverData; type FriChallenger = ::Challenger; + + fn fri_config(&self) -> &FriConfig> { + self.pcs().fri_config() + } } diff --git a/recursion/circuit-v2/src/stark.rs b/recursion/circuit-v2/src/stark.rs index 13c1a4145b..1fabc461d4 100644 --- a/recursion/circuit-v2/src/stark.rs +++ b/recursion/circuit-v2/src/stark.rs @@ -5,19 +5,16 @@ use p3_commit::TwoAdicMultiplicativeCoset; use p3_field::TwoAdicField; use sp1_core::air::MachineAir; -use sp1_core::stark::Com; use sp1_core::stark::ShardProof; use sp1_core::stark::StarkGenericConfig; use sp1_core::stark::StarkMachine; +use sp1_core::stark::Val; use sp1_core::stark::{AirOpenedValues, ChipOpenedValues}; use sp1_core::stark::StarkVerifyingKey; -use sp1_core::utils::inner_fri_config; use sp1_recursion_compiler::ir::{Builder, Config, Ext, ExtConst, FromConstant, Usize}; use sp1_recursion_compiler::prelude::Felt; -use sp1_recursion_core::runtime::DIGEST_SIZE; - use sp1_recursion_program::{ commit::PolynomialSpaceVariable, stark::RecursiveVerifierConstraintFolder, types::QuotientDataValues, @@ -156,23 +153,17 @@ impl<'a, SC: StarkGenericConfig, A: MachineAir> VerifyingKeyHint<'a, SC impl StarkVerifier where C::F: TwoAdicField, - SC: StarkGenericConfig< - Val = C::F, - Challenge = C::EF, - Domain = TwoAdicMultiplicativeCoset, - >, + SC: BabyBearFriConfigVariable, { pub fn verify_shard( builder: &mut Builder, vk: &VerifyingKeyVariable, machine: &StarkMachine, - challenger: &mut DuplexChallengerVariable, + challenger: &mut SC::FriChallengerVariable, proof: &ShardProofVariable, ) where - A: MachineAir + for<'a> Air>, - C::F: TwoAdicField, - C::EF: TwoAdicField, - Com: Into<[SC::Val; DIGEST_SIZE]>, + A: MachineAir> + for<'a> Air>, + >::ProverData>: Clone, { builder.cycle_tracker("stage-c-verify-shard-setup"); let ShardProofVariable { @@ -192,11 +183,11 @@ where .map(|_| challenger.sample_ext(builder)) .collect::>(); - challenger.observe_commitment(builder, *permutation_commit); + challenger.observe_slice(builder, *permutation_commit); let _alpha = challenger.sample_ext(builder); - challenger.observe_commitment(builder, *quotient_commit); + challenger.observe_slice(builder, *quotient_commit); let zeta = challenger.sample_ext(builder); @@ -216,8 +207,8 @@ where let prep_mats: Vec> = { let mut ms = zip( &vk.preprocessed_sorted_idxs, - zip(&vk.prep_domains, machine.preprocessed_chip_ids()).map(|(&domain, chip_id)| { - { + zip(&vk.prep_domains, machine.preprocessed_chip_ids()).map( + |(&domain, chip_id): (&TwoAdicMultiplicativeCoset<_>, usize)| { // Get index within all sorted chips. let chip_sorted_id = proof.sorted_idxs[chip_id]; // Get opening from proof. @@ -239,8 +230,8 @@ where values: prep_values, points: trace_points, } - } - }), + }, + ), ) .collect::>(); // Invert the `vk.preprocessed_sorted_idxs` permutation. @@ -329,8 +320,8 @@ where // Verify the pcs proof // builder.cycle_tracker("stage-d-verify-pcs"); - let config = inner_fri_config(); - verify_two_adic_pcs::<_, _>(builder, &config, opening_proof, challenger, rounds); + let config = machine.config().fri_config(); + verify_two_adic_pcs::(builder, config, opening_proof, challenger, rounds); // builder.cycle_tracker("stage-d-verify-pcs"); // builder.cycle_tracker("stage-e-verify-constraints"); From 93cc604cf968931478c2c9d7e887983d294ed3ec Mon Sep 17 00:00:00 2001 From: Tej Qu Nair Date: Mon, 12 Aug 2024 13:10:27 -0700 Subject: [PATCH 3/3] remove some comments --- recursion/circuit-v2/src/lib.rs | 4 ---- 1 file changed, 4 deletions(-) diff --git a/recursion/circuit-v2/src/lib.rs b/recursion/circuit-v2/src/lib.rs index 33524cafe4..3a83d04060 100644 --- a/recursion/circuit-v2/src/lib.rs +++ b/recursion/circuit-v2/src/lib.rs @@ -116,8 +116,6 @@ pub trait BabyBearFriConfig: fn fri_config(&self) -> &FriConfig>; } -// TODO write subtrait that enables use of the Variable variants -// consider merging this into the above trait pub trait BabyBearFriConfigVariable: BabyBearFriConfig { // Is this is the best place to put this? type C: Config; @@ -126,7 +124,6 @@ pub trait BabyBearFriConfigVariable: BabyBearFriConfig { impl BabyBearFriConfig for BabyBearPoseidon2 { type ValMmcs = sp1_core::utils::baby_bear_poseidon2::ValMmcs; - // type RowMajorProverData = PcsProverData; type FriChallenger = ::Challenger; fn fri_config(&self) -> &FriConfig> { @@ -142,7 +139,6 @@ impl BabyBearFriConfigVariable for BabyBearPoseidon2 { impl BabyBearFriConfig for BabyBearPoseidon2Outer { type ValMmcs = OuterValMmcs; - // type RowMajorProverData = PcsProverData; type FriChallenger = ::Challenger; fn fri_config(&self) -> &FriConfig> {