diff --git a/evm/src/all_stark.rs b/evm/src/all_stark.rs index ab105449..0448ab52 100644 --- a/evm/src/all_stark.rs +++ b/evm/src/all_stark.rs @@ -51,6 +51,9 @@ mod tests { use anyhow::Result; use plonky2::field::field_types::Field; use plonky2::field::polynomial::PolynomialValues; + use plonky2::iop::witness::PartialWitness; + use plonky2::plonk::circuit_builder::CircuitBuilder; + use plonky2::plonk::circuit_data::CircuitConfig; use plonky2::plonk::config::{GenericConfig, PoseidonGoldilocksConfig}; use plonky2::util::timing::TimingTree; use rand::{thread_rng, Rng}; @@ -60,17 +63,18 @@ mod tests { use crate::cpu::cpu_stark::CpuStark; use crate::cross_table_lookup::CrossTableLookup; use crate::keccak::keccak_stark::KeccakStark; + use crate::proof::AllProof; use crate::prover::prove; + use crate::recursive_verifier::{ + add_virtual_all_proof, set_all_proof_target, verify_proof_circuit, + }; use crate::verifier::verify_proof; - #[test] - fn test_all_stark() -> Result<()> { - const D: usize = 2; - type C = PoseidonGoldilocksConfig; - type F = >::F; - - let config = StarkConfig::standard_fast_config(); + const D: usize = 2; + type C = PoseidonGoldilocksConfig; + type F = >::F; + fn get_proof(config: &StarkConfig) -> Result<(AllStark, AllProof)> { let cpu_stark = CpuStark:: { f: Default::default(), }; @@ -118,12 +122,65 @@ mod tests { let proof = prove::( &all_stark, - &config, + config, vec![cpu_trace, keccak_trace], vec![vec![]; 2], &mut TimingTree::default(), )?; + Ok((all_stark, proof)) + } + + #[test] + fn test_all_stark() -> Result<()> { + let config = StarkConfig::standard_fast_config(); + let (all_stark, proof) = get_proof(&config)?; verify_proof(all_stark, proof, &config) } + + #[test] + fn test_all_stark_recursive_verifier() -> Result<()> { + init_logger(); + + let config = StarkConfig::standard_fast_config(); + let (all_stark, proof) = get_proof(&config)?; + verify_proof(all_stark.clone(), proof.clone(), &config)?; + + recursive_proof(all_stark, proof, &config, true) + } + + fn recursive_proof( + inner_all_stark: AllStark, + inner_proof: AllProof, + inner_config: &StarkConfig, + print_gate_counts: bool, + ) -> Result<()> { + let circuit_config = CircuitConfig::standard_recursion_config(); + let mut builder = CircuitBuilder::::new(circuit_config); + let mut pw = PartialWitness::new(); + let degree_bits = inner_proof.degree_bits(inner_config); + let nums_ctl_zs = inner_proof.nums_ctl_zs(); + let pt = add_virtual_all_proof( + &mut builder, + &inner_all_stark, + inner_config, + °ree_bits, + &nums_ctl_zs, + ); + set_all_proof_target(&mut pw, &pt, &inner_proof, builder.zero()); + + verify_proof_circuit::(&mut builder, inner_all_stark, pt, inner_config); + + if print_gate_counts { + builder.print_gate_counts(0); + } + + let data = builder.build::(); + let proof = data.prove(pw)?; + data.verify(proof) + } + + fn init_logger() { + let _ = env_logger::builder().format_timestamp(None).try_init(); + } } diff --git a/evm/src/cross_table_lookup.rs b/evm/src/cross_table_lookup.rs index d111fc9f..d29958be 100644 --- a/evm/src/cross_table_lookup.rs +++ b/evm/src/cross_table_lookup.rs @@ -5,17 +5,20 @@ use plonky2::field::packed_field::PackedField; use plonky2::field::polynomial::PolynomialValues; use plonky2::hash::hash_types::RichField; use plonky2::iop::challenger::Challenger; +use plonky2::iop::ext_target::ExtensionTarget; +use plonky2::iop::target::Target; +use plonky2::plonk::circuit_builder::CircuitBuilder; use plonky2::plonk::config::GenericConfig; use crate::all_stark::Table; use crate::config::StarkConfig; -use crate::constraint_consumer::ConstraintConsumer; +use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; use crate::permutation::{ get_grand_product_challenge_set, GrandProductChallenge, GrandProductChallengeSet, }; -use crate::proof::StarkProofWithPublicInputs; +use crate::proof::{StarkProofWithPublicInputs, StarkProofWithPublicInputsTarget}; use crate::stark::Stark; -use crate::vars::StarkEvaluationVars; +use crate::vars::{StarkEvaluationTargets, StarkEvaluationVars}; #[derive(Clone)] pub struct CrossTableLookup { @@ -230,6 +233,106 @@ pub(crate) fn eval_cross_table_lookup_checks { + pub(crate) local_z: ExtensionTarget, + pub(crate) next_z: ExtensionTarget, + pub(crate) challenges: GrandProductChallenge, + pub(crate) columns: &'a [usize], +} + +impl<'a, const D: usize> CtlCheckVarsTarget<'a, D> { + pub(crate) fn from_proofs( + proofs: &[StarkProofWithPublicInputsTarget], + cross_table_lookups: &'a [CrossTableLookup], + ctl_challenges: &'a GrandProductChallengeSet, + num_permutation_zs: &[usize], + ) -> Vec> { + debug_assert_eq!(proofs.len(), num_permutation_zs.len()); + let mut ctl_zs = proofs + .iter() + .zip(num_permutation_zs) + .map(|(p, &num_perms)| { + let openings = &p.proof.openings; + let ctl_zs = openings.permutation_ctl_zs.iter().skip(num_perms); + let ctl_zs_right = openings.permutation_ctl_zs_right.iter().skip(num_perms); + ctl_zs.zip(ctl_zs_right) + }) + .collect::>(); + + let mut ctl_vars_per_table = vec![vec![]; proofs.len()]; + for CrossTableLookup { + looking_table, + looking_columns, + looked_table, + looked_columns, + .. + } in cross_table_lookups + { + for &challenges in &ctl_challenges.challenges { + let (looking_z, looking_z_next) = ctl_zs[*looking_table as usize].next().unwrap(); + ctl_vars_per_table[*looking_table as usize].push(Self { + local_z: *looking_z, + next_z: *looking_z_next, + challenges, + columns: looking_columns, + }); + + let (looked_z, looked_z_next) = ctl_zs[*looked_table as usize].next().unwrap(); + ctl_vars_per_table[*looked_table as usize].push(Self { + local_z: *looked_z, + next_z: *looked_z_next, + challenges, + columns: looked_columns, + }); + } + } + ctl_vars_per_table + } +} + +pub(crate) fn eval_cross_table_lookup_checks_circuit< + S: Stark, + F: RichField + Extendable, + const D: usize, +>( + builder: &mut CircuitBuilder, + vars: StarkEvaluationTargets, + ctl_vars: &[CtlCheckVarsTarget], + consumer: &mut RecursiveConstraintConsumer, +) { + for lookup_vars in ctl_vars { + let CtlCheckVarsTarget { + local_z, + next_z, + challenges, + columns, + } = lookup_vars; + + // Check value of `Z(1)` + let combined_local = challenges.combine_circuit( + builder, + &columns + .iter() + .map(|&i| vars.local_values[i]) + .collect::>(), + ); + let first_row = builder.sub_extension(*local_z, combined_local); + consumer.constraint_first_row(builder, first_row); + // Check `Z(gw) = combination * Z(w)` + let combined_next = challenges.combine_circuit( + builder, + &columns + .iter() + .map(|&i| vars.next_values[i]) + .collect::>(), + ); + let mut transition = builder.mul_extension(*local_z, combined_next); + transition = builder.sub_extension(*next_z, transition); + consumer.constraint_transition(builder, transition); + } +} + pub(crate) fn verify_cross_table_lookups< F: RichField + Extendable, C: GenericConfig, @@ -273,3 +376,49 @@ pub(crate) fn verify_cross_table_lookups< Ok(()) } + +pub(crate) fn verify_cross_table_lookups_circuit< + F: RichField + Extendable, + C: GenericConfig, + const D: usize, +>( + builder: &mut CircuitBuilder, + cross_table_lookups: Vec>, + proofs: &[StarkProofWithPublicInputsTarget], + challenges: GrandProductChallengeSet, + inner_config: &StarkConfig, +) { + let degrees_bits = proofs + .iter() + .map(|p| p.proof.recover_degree_bits(inner_config)) + .collect::>(); + let mut ctl_zs_openings = proofs + .iter() + .map(|p| p.proof.openings.ctl_zs_last.iter()) + .collect::>(); + for ( + i, + CrossTableLookup { + looking_table, + looked_table, + default, + .. + }, + ) in cross_table_lookups.into_iter().enumerate() + { + let looking_degree = 1 << degrees_bits[looking_table as usize]; + let looked_degree = 1 << degrees_bits[looked_table as usize]; + let looking_z = *ctl_zs_openings[looking_table as usize].next().unwrap(); + let looked_z = *ctl_zs_openings[looked_table as usize].next().unwrap(); + let challenge = challenges.challenges[i % inner_config.num_challenges]; + let default = default + .into_iter() + .map(|x| builder.constant(x)) + .collect::>(); + let combined_default = challenge.combine_base_circuit(builder, &default); + + let pad = builder.exp_u64(combined_default, looking_degree - looked_degree); + let padded_looked_z = builder.mul(looked_z, pad); + builder.connect(looking_z, padded_looked_z); + } +} diff --git a/evm/src/get_challenges.rs b/evm/src/get_challenges.rs index 6293a6f3..2e7d8dcb 100644 --- a/evm/src/get_challenges.rs +++ b/evm/src/get_challenges.rs @@ -1,6 +1,6 @@ use itertools::izip; use plonky2::field::extension_field::Extendable; -use plonky2::fri::proof::FriProof; +use plonky2::fri::proof::{FriProof, FriProofTarget}; use plonky2::hash::hash_types::RichField; use plonky2::iop::challenger::{Challenger, RecursiveChallenger}; use plonky2::plonk::circuit_builder::CircuitBuilder; @@ -9,11 +9,10 @@ use plonky2::plonk::config::{AlgebraicHasher, GenericConfig}; use crate::all_stark::AllStark; use crate::config::StarkConfig; use crate::permutation::{ - get_grand_product_challenge_set, get_n_grand_product_challenge_sets, - get_n_permutation_challenge_sets_target, + get_grand_product_challenge_set, get_grand_product_challenge_set_target, + get_n_grand_product_challenge_sets, get_n_grand_product_challenge_sets_target, }; use crate::proof::*; -use crate::stark::Stark; impl, C: GenericConfig, const D: usize> AllProof { /// Computes all Fiat-Shamir challenges used in the STARK proof. @@ -46,6 +45,46 @@ impl, C: GenericConfig, const D: usize> A } } +impl AllProofTarget { + pub(crate) fn get_challenges, C: GenericConfig>( + &self, + builder: &mut CircuitBuilder, + all_stark: &AllStark, + config: &StarkConfig, + ) -> AllProofChallengesTarget + where + C::Hasher: AlgebraicHasher, + { + let mut challenger = RecursiveChallenger::::new(builder); + + for proof in &self.stark_proofs { + challenger.observe_cap(&proof.proof.trace_cap); + } + + let ctl_challenges = + get_grand_product_challenge_set_target(builder, &mut challenger, config.num_challenges); + + AllProofChallengesTarget { + stark_challenges: izip!( + &self.stark_proofs, + all_stark.nums_permutation_zs(config), + all_stark.permutation_batch_sizes() + ) + .map(|(proof, num_perm, batch_size)| { + proof.get_challenges::( + builder, + &mut challenger, + num_perm > 0, + batch_size, + config, + ) + }) + .collect(), + ctl_challenges, + } + } +} + impl StarkProofWithPublicInputs where F: RichField + Extendable, @@ -110,48 +149,60 @@ where } impl StarkProofWithPublicInputsTarget { - pub(crate) fn get_challenges< - F: RichField + Extendable, - C: GenericConfig, - S: Stark, - >( + pub(crate) fn get_challenges, C: GenericConfig>( &self, builder: &mut CircuitBuilder, - stark: &S, + challenger: &mut RecursiveChallenger, + stark_use_permutation: bool, + stark_permutation_batch_size: usize, config: &StarkConfig, ) -> StarkProofChallengesTarget where C::Hasher: AlgebraicHasher, { - let proof = &self.proof; - let opening_proof = &proof.opening_proof; + let StarkProofTarget { + permutation_ctl_zs_cap, + quotient_polys_cap, + openings, + opening_proof: + FriProofTarget { + commit_phase_merkle_caps, + final_poly, + pow_witness, + .. + }, + .. + } = &self.proof; + let num_challenges = config.num_challenges; - let mut challenger = RecursiveChallenger::::new(builder); - challenger.observe_cap(&proof.trace_cap); - let permutation_challenge_sets = - proof.permutation_zs_cap.as_ref().map(|permutation_zs_cap| { - let tmp = get_n_permutation_challenge_sets_target( - builder, - &mut challenger, - num_challenges, - stark.permutation_batch_size(), - ); - challenger.observe_cap(permutation_zs_cap); - tmp - }); + + let permutation_challenge_sets = stark_use_permutation.then(|| { + get_n_grand_product_challenge_sets_target( + builder, + challenger, + num_challenges, + stark_permutation_batch_size, + ) + }); + + challenger.observe_cap(permutation_ctl_zs_cap); + let stark_alphas = challenger.get_n_challenges(builder, num_challenges); - challenger.observe_cap(&proof.quotient_polys_cap); + + challenger.observe_cap(quotient_polys_cap); let stark_zeta = challenger.get_extension_challenge(builder); - challenger.observe_openings(&proof.openings.to_fri_openings()); + + challenger.observe_openings(&openings.to_fri_openings(builder.zero())); + StarkProofChallengesTarget { permutation_challenge_sets, stark_alphas, stark_zeta, fri_challenges: challenger.fri_challenges::( builder, - &opening_proof.commit_phase_merkle_caps, - &opening_proof.final_poly, - opening_proof.pow_witness, + commit_phase_merkle_caps, + final_poly, + *pow_witness, &config.fri_config, ), } diff --git a/evm/src/permutation.rs b/evm/src/permutation.rs index 6f4c6ca2..35bd92e5 100644 --- a/evm/src/permutation.rs +++ b/evm/src/permutation.rs @@ -12,7 +12,9 @@ use plonky2::iop::ext_target::ExtensionTarget; use plonky2::iop::target::Target; use plonky2::plonk::circuit_builder::CircuitBuilder; use plonky2::plonk::config::{AlgebraicHasher, GenericConfig, Hasher}; -use plonky2::plonk::plonk_common::reduce_with_powers; +use plonky2::plonk::plonk_common::{ + reduce_with_powers, reduce_with_powers_circuit, reduce_with_powers_ext_circuit, +}; use plonky2::util::reducing::{ReducingFactor, ReducingFactorTarget}; use rayon::prelude::*; @@ -68,6 +70,27 @@ impl GrandProductChallenge { } } +impl GrandProductChallenge { + pub(crate) fn combine_circuit, const D: usize>( + &self, + builder: &mut CircuitBuilder, + terms: &[ExtensionTarget], + ) -> ExtensionTarget { + let reduced = reduce_with_powers_ext_circuit(builder, terms, self.beta); + let gamma = builder.convert_to_ext(self.gamma); + builder.add_extension(reduced, gamma) + } + + pub(crate) fn combine_base_circuit, const D: usize>( + &self, + builder: &mut CircuitBuilder, + terms: &[Target], + ) -> Target { + let reduced = reduce_with_powers_circuit(builder, terms, self.beta); + builder.add(reduced, self.gamma) + } +} + /// Like `PermutationChallenge`, but with `num_challenges` copies to boost soundness. #[derive(Clone)] pub(crate) struct GrandProductChallengeSet { @@ -190,7 +213,7 @@ pub(crate) fn get_n_grand_product_challenge_sets>( .collect() } -fn get_permutation_challenge_target< +fn get_grand_product_challenge_target< F: RichField + Extendable, H: AlgebraicHasher, const D: usize, @@ -203,7 +226,7 @@ fn get_permutation_challenge_target< GrandProductChallenge { beta, gamma } } -fn get_permutation_challenge_set_target< +pub(crate) fn get_grand_product_challenge_set_target< F: RichField + Extendable, H: AlgebraicHasher, const D: usize, @@ -213,12 +236,12 @@ fn get_permutation_challenge_set_target< num_challenges: usize, ) -> GrandProductChallengeSet { let challenges = (0..num_challenges) - .map(|_| get_permutation_challenge_target(builder, challenger)) + .map(|_| get_grand_product_challenge_target(builder, challenger)) .collect(); GrandProductChallengeSet { challenges } } -pub(crate) fn get_n_permutation_challenge_sets_target< +pub(crate) fn get_n_grand_product_challenge_sets_target< F: RichField + Extendable, H: AlgebraicHasher, const D: usize, @@ -229,7 +252,7 @@ pub(crate) fn get_n_permutation_challenge_sets_target< num_sets: usize, ) -> Vec> { (0..num_sets) - .map(|_| get_permutation_challenge_set_target(builder, challenger, num_challenges)) + .map(|_| get_grand_product_challenge_set_target(builder, challenger, num_challenges)) .collect() } diff --git a/evm/src/proof.rs b/evm/src/proof.rs index d03bc397..7816224f 100644 --- a/evm/src/proof.rs +++ b/evm/src/proof.rs @@ -22,11 +22,36 @@ pub struct AllProof, C: GenericConfig, co pub stark_proofs: Vec>, } +impl, C: GenericConfig, const D: usize> AllProof { + pub fn degree_bits(&self, config: &StarkConfig) -> Vec { + self.stark_proofs + .iter() + .map(|proof| proof.proof.recover_degree_bits(config)) + .collect() + } + + pub fn nums_ctl_zs(&self) -> Vec { + self.stark_proofs + .iter() + .map(|proof| proof.proof.openings.ctl_zs_last.len()) + .collect() + } +} + pub(crate) struct AllProofChallenges, const D: usize> { pub stark_challenges: Vec>, pub ctl_challenges: GrandProductChallengeSet, } +pub struct AllProofTarget { + pub stark_proofs: Vec>, +} + +pub(crate) struct AllProofChallengesTarget { + pub stark_challenges: Vec>, + pub ctl_challenges: GrandProductChallengeSet, +} + #[derive(Debug, Clone)] pub struct StarkProof, C: GenericConfig, const D: usize> { /// Merkle cap of LDEs of trace values. @@ -55,7 +80,7 @@ impl, C: GenericConfig, const D: usize> S pub struct StarkProofTarget { pub trace_cap: MerkleCapTarget, - pub permutation_zs_cap: Option, + pub permutation_ctl_zs_cap: MerkleCapTarget, pub quotient_polys_cap: MerkleCapTarget, pub openings: StarkOpeningSetTarget, pub opening_proof: FriProofTarget, @@ -203,38 +228,38 @@ impl, const D: usize> StarkOpeningSet { .copied() .collect_vec(), }; - let mut batches = vec![zeta_batch, zeta_right_batch]; + debug_assert!(!self.ctl_zs_last.is_empty()); + let ctl_last_batch = FriOpeningBatch { + values: self + .ctl_zs_last + .iter() + .copied() + .map(F::Extension::from_basefield) + .collect(), + }; - if !self.ctl_zs_last.is_empty() { - batches.push(FriOpeningBatch { - values: self - .ctl_zs_last - .iter() - .copied() - .map(F::Extension::from_basefield) - .collect(), - }); + FriOpenings { + batches: vec![zeta_batch, zeta_right_batch, ctl_last_batch], } - - FriOpenings { batches } } } pub struct StarkOpeningSetTarget { pub local_values: Vec>, pub next_values: Vec>, - pub permutation_zs: Option>>, - pub permutation_zs_right: Option>>, + pub permutation_ctl_zs: Vec>, + pub permutation_ctl_zs_right: Vec>, + pub ctl_zs_last: Vec, pub quotient_polys: Vec>, } impl StarkOpeningSetTarget { - pub(crate) fn to_fri_openings(&self) -> FriOpeningsTarget { + pub(crate) fn to_fri_openings(&self, zero: Target) -> FriOpeningsTarget { let zeta_batch = FriOpeningBatchTarget { values: self .local_values .iter() - .chain(self.permutation_zs.iter().flatten()) + .chain(&self.permutation_ctl_zs) .chain(&self.quotient_polys) .copied() .collect_vec(), @@ -243,12 +268,22 @@ impl StarkOpeningSetTarget { values: self .next_values .iter() - .chain(self.permutation_zs_right.iter().flatten()) + .chain(&self.permutation_ctl_zs_right) .copied() .collect_vec(), }; + debug_assert!(!self.ctl_zs_last.is_empty()); + let ctl_last_batch = FriOpeningBatchTarget { + values: self + .ctl_zs_last + .iter() + .copied() + .map(|t| t.to_ext_target(zero)) + .collect(), + }; + FriOpeningsTarget { - batches: vec![zeta_batch, zeta_right_batch], + batches: vec![zeta_batch, zeta_right_batch, ctl_last_batch], } } } diff --git a/evm/src/recursive_verifier.rs b/evm/src/recursive_verifier.rs index af395fdb..55f5d13a 100644 --- a/evm/src/recursive_verifier.rs +++ b/evm/src/recursive_verifier.rs @@ -1,60 +1,92 @@ -use std::iter::once; - -use anyhow::{ensure, Result}; use itertools::Itertools; use plonky2::field::extension_field::Extendable; use plonky2::field::field_types::Field; use plonky2::fri::witness_util::set_fri_proof_target; use plonky2::hash::hash_types::RichField; use plonky2::iop::ext_target::ExtensionTarget; +use plonky2::iop::target::Target; use plonky2::iop::witness::Witness; use plonky2::plonk::circuit_builder::CircuitBuilder; use plonky2::plonk::config::{AlgebraicHasher, GenericConfig}; use plonky2::util::reducing::ReducingFactorTarget; use plonky2::with_context; +use crate::all_stark::{AllStark, Table}; use crate::config::StarkConfig; use crate::constraint_consumer::RecursiveConstraintConsumer; +use crate::cpu::cpu_stark::CpuStark; +use crate::cross_table_lookup::{verify_cross_table_lookups_circuit, CtlCheckVarsTarget}; +use crate::keccak::keccak_stark::KeccakStark; use crate::permutation::PermutationCheckDataTarget; use crate::proof::{ - StarkOpeningSetTarget, StarkProof, StarkProofChallengesTarget, StarkProofTarget, - StarkProofWithPublicInputs, StarkProofWithPublicInputsTarget, + AllProof, AllProofChallengesTarget, AllProofTarget, StarkOpeningSetTarget, StarkProof, + StarkProofChallengesTarget, StarkProofTarget, StarkProofWithPublicInputs, + StarkProofWithPublicInputsTarget, }; use crate::stark::Stark; use crate::vanishing_poly::eval_vanishing_poly_circuit; use crate::vars::StarkEvaluationTargets; -pub fn verify_stark_proof_circuit< +pub fn verify_proof_circuit< F: RichField + Extendable, C: GenericConfig, - S: Stark, const D: usize, >( builder: &mut CircuitBuilder, - stark: S, - proof_with_pis: StarkProofWithPublicInputsTarget, + all_stark: AllStark, + all_proof: AllProofTarget, inner_config: &StarkConfig, ) where + [(); CpuStark::::COLUMNS]:, + [(); CpuStark::::PUBLIC_INPUTS]:, + [(); KeccakStark::::COLUMNS]:, + [(); KeccakStark::::PUBLIC_INPUTS]:, C::Hasher: AlgebraicHasher, - [(); S::COLUMNS]:, - [(); S::PUBLIC_INPUTS]:, { - assert_eq!(proof_with_pis.public_inputs.len(), S::PUBLIC_INPUTS); - let degree_bits = proof_with_pis.proof.recover_degree_bits(inner_config); - let challenges = with_context!( - builder, - "compute challenges", - proof_with_pis.get_challenges::(builder, &stark, inner_config) + let AllProofChallengesTarget { + stark_challenges, + ctl_challenges, + } = all_proof.get_challenges::(builder, &all_stark, inner_config); + + let nums_permutation_zs = all_stark.nums_permutation_zs(inner_config); + + let AllStark { + cpu_stark, + keccak_stark, + cross_table_lookups, + } = all_stark; + + let ctl_vars_per_table = CtlCheckVarsTarget::from_proofs( + &all_proof.stark_proofs, + &cross_table_lookups, + &ctl_challenges, + &nums_permutation_zs, ); - verify_stark_proof_with_challenges_circuit::( + verify_stark_proof_with_challenges_circuit::( builder, - stark, - proof_with_pis, - challenges, + cpu_stark, + &all_proof.stark_proofs[Table::Cpu as usize], + &stark_challenges[Table::Cpu as usize], + &ctl_vars_per_table[Table::Cpu as usize], inner_config, - degree_bits, ); + verify_stark_proof_with_challenges_circuit::( + builder, + keccak_stark, + &all_proof.stark_proofs[Table::Keccak as usize], + &stark_challenges[Table::Keccak as usize], + &ctl_vars_per_table[Table::Keccak as usize], + inner_config, + ); + + verify_cross_table_lookups_circuit::( + builder, + cross_table_lookups, + &all_proof.stark_proofs, + ctl_challenges, + inner_config, + ) } /// Recursively verifies an inner proof. @@ -66,40 +98,43 @@ fn verify_stark_proof_with_challenges_circuit< >( builder: &mut CircuitBuilder, stark: S, - proof_with_pis: StarkProofWithPublicInputsTarget, - challenges: StarkProofChallengesTarget, + proof_with_pis: &StarkProofWithPublicInputsTarget, + challenges: &StarkProofChallengesTarget, + ctl_vars: &[CtlCheckVarsTarget], inner_config: &StarkConfig, - degree_bits: usize, ) where C::Hasher: AlgebraicHasher, [(); S::COLUMNS]:, [(); S::PUBLIC_INPUTS]:, { - check_permutation_options(&stark, &proof_with_pis, &challenges).unwrap(); + let zero = builder.zero(); let one = builder.one_extension(); let StarkProofWithPublicInputsTarget { proof, public_inputs, } = proof_with_pis; + assert_eq!(public_inputs.len(), S::PUBLIC_INPUTS); let StarkOpeningSetTarget { local_values, next_values, - permutation_zs, - permutation_zs_right, + permutation_ctl_zs, + permutation_ctl_zs_right, + ctl_zs_last, quotient_polys, } = &proof.openings; let vars = StarkEvaluationTargets { local_values: &local_values.to_vec().try_into().unwrap(), next_values: &next_values.to_vec().try_into().unwrap(), public_inputs: &public_inputs - .into_iter() - .map(|t| builder.convert_to_ext(t)) + .iter() + .map(|&t| builder.convert_to_ext(t)) .collect::>() .try_into() .unwrap(), }; + let degree_bits = proof.recover_degree_bits(inner_config); let zeta_pow_deg = builder.exp_power_of_2_extension(challenges.stark_zeta, degree_bits); let z_h_zeta = builder.sub_extension(zeta_pow_deg, one); let (l_1, l_last) = @@ -110,18 +145,19 @@ fn verify_stark_proof_with_challenges_circuit< let mut consumer = RecursiveConstraintConsumer::::new( builder.zero_extension(), - challenges.stark_alphas, + challenges.stark_alphas.clone(), z_last, l_1, l_last, ); + let num_permutation_zs = stark.num_permutation_batches(inner_config); let permutation_data = stark .uses_permutation_args() .then(|| PermutationCheckDataTarget { - local_zs: permutation_zs.as_ref().unwrap().clone(), - next_zs: permutation_zs_right.as_ref().unwrap().clone(), - permutation_challenge_sets: challenges.permutation_challenge_sets.unwrap(), + local_zs: permutation_ctl_zs[..num_permutation_zs].to_vec(), + next_zs: permutation_ctl_zs_right[..num_permutation_zs].to_vec(), + permutation_challenge_sets: challenges.permutation_challenge_sets.clone().unwrap(), }); with_context!( @@ -133,6 +169,7 @@ fn verify_stark_proof_with_challenges_circuit< inner_config, vars, permutation_data, + ctl_vars, &mut consumer, ) ); @@ -149,20 +186,23 @@ fn verify_stark_proof_with_challenges_circuit< builder.connect_extension(vanishing_polys_zeta[i], computed_vanishing_poly); } - let merkle_caps = once(proof.trace_cap) - .chain(proof.permutation_zs_cap) - .chain(once(proof.quotient_polys_cap)) - .collect_vec(); + let merkle_caps = vec![ + proof.trace_cap.clone(), + proof.permutation_ctl_zs_cap.clone(), + proof.quotient_polys_cap.clone(), + ]; let fri_instance = stark.fri_instance_target( builder, challenges.stark_zeta, F::primitive_root_of_unity(degree_bits), + degree_bits, + ctl_zs_last.len(), inner_config, ); builder.verify_fri_proof::( &fri_instance, - &proof.openings.to_fri_openings(), + &proof.openings.to_fri_openings(zero), &challenges.fri_challenges, &merkle_caps, &proof.opening_proof, @@ -189,6 +229,48 @@ fn eval_l_1_and_l_last_circuit, const D: usize>( ) } +pub fn add_virtual_all_proof, const D: usize>( + builder: &mut CircuitBuilder, + all_stark: &AllStark, + config: &StarkConfig, + degree_bits: &[usize], + nums_ctl_zs: &[usize], +) -> AllProofTarget { + let stark_proofs = vec![ + { + let proof = add_virtual_stark_proof( + builder, + all_stark.cpu_stark, + config, + degree_bits[Table::Cpu as usize], + nums_ctl_zs[Table::Cpu as usize], + ); + let public_inputs = builder.add_virtual_targets(CpuStark::::PUBLIC_INPUTS); + StarkProofWithPublicInputsTarget { + proof, + public_inputs, + } + }, + { + let proof = add_virtual_stark_proof( + builder, + all_stark.keccak_stark, + config, + degree_bits[Table::Keccak as usize], + nums_ctl_zs[Table::Keccak as usize], + ); + let public_inputs = builder.add_virtual_targets(KeccakStark::::PUBLIC_INPUTS); + StarkProofWithPublicInputsTarget { + proof, + public_inputs, + } + }, + ]; + + assert_eq!(stark_proofs.len(), Table::num_tables()); + AllProofTarget { stark_proofs } +} + pub fn add_virtual_stark_proof_with_pis< F: RichField + Extendable, S: Stark, @@ -198,8 +280,9 @@ pub fn add_virtual_stark_proof_with_pis< stark: S, config: &StarkConfig, degree_bits: usize, + num_ctl_zs: usize, ) -> StarkProofWithPublicInputsTarget { - let proof = add_virtual_stark_proof::(builder, stark, config, degree_bits); + let proof = add_virtual_stark_proof::(builder, stark, config, degree_bits, num_ctl_zs); let public_inputs = builder.add_virtual_targets(S::PUBLIC_INPUTS); StarkProofWithPublicInputsTarget { proof, @@ -212,28 +295,24 @@ pub fn add_virtual_stark_proof, S: Stark, con stark: S, config: &StarkConfig, degree_bits: usize, + num_ctl_zs: usize, ) -> StarkProofTarget { let fri_params = config.fri_params(degree_bits); let cap_height = fri_params.config.cap_height; - let num_leaves_per_oracle = once(S::COLUMNS) - .chain( - stark - .uses_permutation_args() - .then(|| stark.num_permutation_batches(config)), - ) - .chain(once(stark.quotient_degree_factor() * config.num_challenges)) - .collect_vec(); + let num_leaves_per_oracle = vec![ + S::COLUMNS, + stark.num_permutation_batches(config) + num_ctl_zs, + stark.quotient_degree_factor() * config.num_challenges, + ]; - let permutation_zs_cap = stark - .uses_permutation_args() - .then(|| builder.add_virtual_cap(cap_height)); + let permutation_zs_cap = builder.add_virtual_cap(cap_height); StarkProofTarget { trace_cap: builder.add_virtual_cap(cap_height), - permutation_zs_cap, + permutation_ctl_zs_cap: permutation_zs_cap, quotient_polys_cap: builder.add_virtual_cap(cap_height), - openings: add_stark_opening_set::(builder, stark, config), + openings: add_stark_opening_set::(builder, stark, num_ctl_zs, config), opening_proof: builder.add_virtual_fri_proof(&num_leaves_per_oracle, &fri_params), } } @@ -241,27 +320,47 @@ pub fn add_virtual_stark_proof, S: Stark, con fn add_stark_opening_set, S: Stark, const D: usize>( builder: &mut CircuitBuilder, stark: S, + num_ctl_zs: usize, config: &StarkConfig, ) -> StarkOpeningSetTarget { let num_challenges = config.num_challenges; StarkOpeningSetTarget { local_values: builder.add_virtual_extension_targets(S::COLUMNS), next_values: builder.add_virtual_extension_targets(S::COLUMNS), - permutation_zs: stark - .uses_permutation_args() - .then(|| builder.add_virtual_extension_targets(stark.num_permutation_batches(config))), - permutation_zs_right: stark - .uses_permutation_args() - .then(|| builder.add_virtual_extension_targets(stark.num_permutation_batches(config))), + permutation_ctl_zs: builder + .add_virtual_extension_targets(stark.num_permutation_batches(config) + num_ctl_zs), + permutation_ctl_zs_right: builder + .add_virtual_extension_targets(stark.num_permutation_batches(config) + num_ctl_zs), + ctl_zs_last: builder.add_virtual_targets(num_ctl_zs), quotient_polys: builder .add_virtual_extension_targets(stark.quotient_degree_factor() * num_challenges), } } +pub fn set_all_proof_target, W, const D: usize>( + witness: &mut W, + all_proof_target: &AllProofTarget, + all_proof: &AllProof, + zero: Target, +) where + F: RichField + Extendable, + C::Hasher: AlgebraicHasher, + W: Witness, +{ + for (pt, p) in all_proof_target + .stark_proofs + .iter() + .zip_eq(&all_proof.stark_proofs) + { + set_stark_proof_with_pis_target(witness, pt, p, zero); + } +} + pub fn set_stark_proof_with_pis_target, W, const D: usize>( witness: &mut W, stark_proof_with_pis_target: &StarkProofWithPublicInputsTarget, stark_proof_with_pis: &StarkProofWithPublicInputs, + zero: Target, ) where F: RichField + Extendable, C::Hasher: AlgebraicHasher, @@ -281,13 +380,14 @@ pub fn set_stark_proof_with_pis_target, W, const D witness.set_target(pi_t, pi); } - set_stark_proof_target(witness, pt, proof); + set_stark_proof_target(witness, pt, proof, zero); } pub fn set_stark_proof_target, W, const D: usize>( witness: &mut W, proof_target: &StarkProofTarget, proof: &StarkProof, + zero: Target, ) where F: RichField + Extendable, C::Hasher: AlgebraicHasher, @@ -297,35 +397,14 @@ pub fn set_stark_proof_target, W, const D: usize>( witness.set_cap_target(&proof_target.quotient_polys_cap, &proof.quotient_polys_cap); witness.set_fri_openings( - &proof_target.openings.to_fri_openings(), + &proof_target.openings.to_fri_openings(zero), &proof.openings.to_fri_openings(), ); - if let Some(permutation_zs_cap_target) = &proof_target.permutation_zs_cap { - witness.set_cap_target(permutation_zs_cap_target, &proof.permutation_ctl_zs_cap); - } + witness.set_cap_target( + &proof_target.permutation_ctl_zs_cap, + &proof.permutation_ctl_zs_cap, + ); set_fri_proof_target(witness, &proof_target.opening_proof, &proof.opening_proof); } - -/// Utility function to check that all permutation data wrapped in `Option`s are `Some` iff -/// the Stark uses a permutation argument. -fn check_permutation_options, S: Stark, const D: usize>( - stark: &S, - proof_with_pis: &StarkProofWithPublicInputsTarget, - challenges: &StarkProofChallengesTarget, -) -> Result<()> { - let options_is_some = [ - proof_with_pis.proof.permutation_zs_cap.is_some(), - proof_with_pis.proof.openings.permutation_zs.is_some(), - proof_with_pis.proof.openings.permutation_zs_right.is_some(), - challenges.permutation_challenge_sets.is_some(), - ]; - ensure!( - options_is_some - .into_iter() - .all(|b| b == stark.uses_permutation_args()), - "Permutation data doesn't match with Stark configuration." - ); - Ok(()) -} diff --git a/evm/src/stark.rs b/evm/src/stark.rs index 20404341..99532d0f 100644 --- a/evm/src/stark.rs +++ b/evm/src/stark.rs @@ -1,5 +1,3 @@ -use std::iter::once; - use plonky2::field::extension_field::{Extendable, FieldExtension}; use plonky2::field::field_types::Field; use plonky2::field::packed_field::PackedField; @@ -97,24 +95,16 @@ pub trait Stark, const D: usize>: Sync { FriPolynomialInfo::from_range(oracle_indices.next().unwrap(), 0..Self::COLUMNS); let num_permutation_batches = self.num_permutation_batches(config); - let permutation_ctl_zs_info = (num_permutation_batches + num_ctl_zs > 0).then(|| { - let permutation_ctl_index = oracle_indices.next().unwrap(); - FriPolynomialInfo::from_range( - permutation_ctl_index, - 0..num_permutation_batches + num_ctl_zs, - ) - }); + let permutation_ctl_index = oracle_indices.next().unwrap(); + let permutation_ctl_zs_info = FriPolynomialInfo::from_range( + permutation_ctl_index, + 0..num_permutation_batches + num_ctl_zs, + ); - let ctl_zs_info = (num_ctl_zs > 0).then(|| { - let index = permutation_ctl_zs_info - .as_ref() - .map(|info| info[0].oracle_index) - .unwrap_or_else(|| oracle_indices.next().unwrap()); - FriPolynomialInfo::from_range( - index, - num_permutation_batches..num_permutation_batches + num_ctl_zs, - ) - }); + let ctl_zs_info = FriPolynomialInfo::from_range( + permutation_ctl_index, + num_permutation_batches..num_permutation_batches + num_ctl_zs, + ); let quotient_info = FriPolynomialInfo::from_range( oracle_indices.next().unwrap(), @@ -123,29 +113,24 @@ pub trait Stark, const D: usize>: Sync { let zeta_batch = FriBatchInfo { point: zeta, - polynomials: once(trace_info.clone()) - .chain(permutation_ctl_zs_info.clone()) - .chain(once(quotient_info)) - .collect::>() - .concat(), + polynomials: [ + trace_info.clone(), + permutation_ctl_zs_info.clone(), + quotient_info, + ] + .concat(), }; let zeta_right_batch = FriBatchInfo { point: zeta.scalar_mul(g), - polynomials: once(trace_info) - .chain(permutation_ctl_zs_info) - .collect::>() - .concat(), + polynomials: [trace_info, permutation_ctl_zs_info].concat(), }; - let ctl_last_batch = ctl_zs_info.map(|info| FriBatchInfo { + let ctl_last_batch = FriBatchInfo { point: F::Extension::primitive_root_of_unity(degree_bits).inverse(), - polynomials: info, - }); + polynomials: ctl_zs_info, + }; FriInstanceInfo { oracles: vec![no_blinding_oracle; oracle_indices.next().unwrap()], - batches: once(zeta_batch) - .chain(once(zeta_right_batch)) - .chain(ctl_last_batch) - .collect::>(), + batches: vec![zeta_batch, zeta_right_batch, ctl_last_batch], } } @@ -155,7 +140,9 @@ pub trait Stark, const D: usize>: Sync { builder: &mut CircuitBuilder, zeta: ExtensionTarget, g: F, - config: &StarkConfig, + degree_bits: usize, + num_ctl_zs: usize, + inner_config: &StarkConfig, ) -> FriInstanceInfoTarget { let no_blinding_oracle = FriOracleInfo { blinding: false }; let mut oracle_indices = 0..; @@ -163,25 +150,28 @@ pub trait Stark, const D: usize>: Sync { let trace_info = FriPolynomialInfo::from_range(oracle_indices.next().unwrap(), 0..Self::COLUMNS); - let permutation_zs_info = if self.uses_permutation_args() { - FriPolynomialInfo::from_range( - oracle_indices.next().unwrap(), - 0..self.num_permutation_batches(config), - ) - } else { - vec![] - }; + let num_permutation_batches = self.num_permutation_batches(inner_config); + let permutation_ctl_index = oracle_indices.next().unwrap(); + let permutation_ctl_zs_info = FriPolynomialInfo::from_range( + permutation_ctl_index, + 0..num_permutation_batches + num_ctl_zs, + ); + + let ctl_zs_info = FriPolynomialInfo::from_range( + permutation_ctl_index, + num_permutation_batches..num_permutation_batches + num_ctl_zs, + ); let quotient_info = FriPolynomialInfo::from_range( oracle_indices.next().unwrap(), - 0..self.quotient_degree_factor() * config.num_challenges, + 0..self.quotient_degree_factor() * inner_config.num_challenges, ); let zeta_batch = FriBatchInfoTarget { point: zeta, polynomials: [ trace_info.clone(), - permutation_zs_info.clone(), + permutation_ctl_zs_info.clone(), quotient_info, ] .concat(), @@ -189,11 +179,16 @@ pub trait Stark, const D: usize>: Sync { let zeta_right = builder.mul_const_extension(g, zeta); let zeta_right_batch = FriBatchInfoTarget { point: zeta_right, - polynomials: [trace_info, permutation_zs_info].concat(), + polynomials: [trace_info, permutation_ctl_zs_info].concat(), + }; + let ctl_last_batch = FriBatchInfoTarget { + point: builder + .constant_extension(F::Extension::primitive_root_of_unity(degree_bits).inverse()), + polynomials: ctl_zs_info, }; FriInstanceInfoTarget { oracles: vec![no_blinding_oracle; oracle_indices.next().unwrap()], - batches: vec![zeta_batch, zeta_right_batch], + batches: vec![zeta_batch, zeta_right_batch, ctl_last_batch], } } diff --git a/evm/src/vanishing_poly.rs b/evm/src/vanishing_poly.rs index 37b1b5ab..31e1ffa9 100644 --- a/evm/src/vanishing_poly.rs +++ b/evm/src/vanishing_poly.rs @@ -6,7 +6,10 @@ use plonky2::plonk::config::GenericConfig; use crate::config::StarkConfig; use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; -use crate::cross_table_lookup::{eval_cross_table_lookup_checks, CtlCheckVars}; +use crate::cross_table_lookup::{ + eval_cross_table_lookup_checks, eval_cross_table_lookup_checks_circuit, CtlCheckVars, + CtlCheckVarsTarget, +}; use crate::permutation::{ eval_permutation_checks, eval_permutation_checks_circuit, PermutationCheckDataTarget, PermutationCheckVars, @@ -47,6 +50,7 @@ pub(crate) fn eval_vanishing_poly_circuit( config: &StarkConfig, vars: StarkEvaluationTargets, permutation_data: Option>, + ctl_vars: &[CtlCheckVarsTarget], consumer: &mut RecursiveConstraintConsumer, ) where F: RichField + Extendable, @@ -66,4 +70,5 @@ pub(crate) fn eval_vanishing_poly_circuit( consumer, ); } + eval_cross_table_lookup_checks_circuit::(builder, vars, ctl_vars, consumer); } diff --git a/evm/src/verifier.rs b/evm/src/verifier.rs index 76e739a2..debd055c 100644 --- a/evm/src/verifier.rs +++ b/evm/src/verifier.rs @@ -29,6 +29,7 @@ where [(); CpuStark::::COLUMNS]:, [(); CpuStark::::PUBLIC_INPUTS]:, [(); KeccakStark::::COLUMNS]:, + [(); KeccakStark::::PUBLIC_INPUTS]:, [(); C::Hasher::HASH_SIZE]:, { let AllProofChallenges { @@ -95,6 +96,7 @@ where proof, public_inputs, } = proof_with_pis; + ensure!(public_inputs.len() == S::PUBLIC_INPUTS); let StarkOpeningSet { local_values, next_values, diff --git a/plonky2/src/iop/ext_target.rs b/plonky2/src/iop/ext_target.rs index 4ae92ea1..8af1c6f7 100644 --- a/plonky2/src/iop/ext_target.rs +++ b/plonky2/src/iop/ext_target.rs @@ -120,9 +120,7 @@ impl, const D: usize> CircuitBuilder { pub fn convert_to_ext(&mut self, t: Target) -> ExtensionTarget { let zero = self.zero(); - let mut arr = [zero; D]; - arr[0] = t; - ExtensionTarget(arr) + t.to_ext_target(zero) } pub fn convert_to_ext_algebra(&mut self, et: ExtensionTarget) -> ExtensionAlgebraTarget { diff --git a/plonky2/src/iop/target.rs b/plonky2/src/iop/target.rs index d26782da..bda1a47c 100644 --- a/plonky2/src/iop/target.rs +++ b/plonky2/src/iop/target.rs @@ -1,5 +1,6 @@ use std::ops::Range; +use crate::iop::ext_target::ExtensionTarget; use crate::iop::wire::Wire; use crate::plonk::circuit_data::CircuitConfig; @@ -37,6 +38,13 @@ impl Target { Target::VirtualTarget { index } => degree * num_wires + index, } } + + /// Conversion to an `ExtensionTarget`. + pub fn to_ext_target(self, zero: Self) -> ExtensionTarget { + let mut arr = [zero; D]; + arr[0] = self; + ExtensionTarget(arr) + } } /// A `Target` which has already been constrained such that it can only be 0 or 1. diff --git a/plonky2/src/plonk/plonk_common.rs b/plonky2/src/plonk/plonk_common.rs index 1cf14cda..42b9f90a 100644 --- a/plonky2/src/plonk/plonk_common.rs +++ b/plonky2/src/plonk/plonk_common.rs @@ -4,6 +4,7 @@ use plonky2_field::packed_field::PackedField; use crate::fri::oracle::SALT_SIZE; use crate::fri::structure::FriOracleInfo; +use crate::gates::arithmetic_base::ArithmeticGate; use crate::hash::hash_types::RichField; use crate::iop::ext_target::ExtensionTarget; use crate::iop::target::Target; @@ -138,6 +139,23 @@ where sum } +pub fn reduce_with_powers_circuit, const D: usize>( + builder: &mut CircuitBuilder, + terms: &[Target], + alpha: Target, +) -> Target { + if terms.len() <= ArithmeticGate::new_from_config(&builder.config).num_ops + 1 { + terms + .iter() + .rev() + .fold(builder.zero(), |acc, &t| builder.mul_add(alpha, acc, t)) + } else { + let alpha = builder.convert_to_ext(alpha); + let mut alpha = ReducingFactorTarget::new(alpha); + alpha.reduce_base(terms, builder).0[0] + } +} + pub fn reduce_with_powers_ext_circuit, const D: usize>( builder: &mut CircuitBuilder, terms: &[ExtensionTarget],