diff --git a/evm/src/all_stark.rs b/evm/src/all_stark.rs index fd9ce01f..e4f93c62 100644 --- a/evm/src/all_stark.rs +++ b/evm/src/all_stark.rs @@ -172,6 +172,7 @@ mod tests { use anyhow::Result; use ethereum_types::U256; use itertools::Itertools; + use log::debug; use plonky2::field::polynomial::PolynomialValues; use plonky2::field::types::{Field, PrimeField64}; use plonky2::iop::witness::PartialWitness; @@ -755,13 +756,12 @@ mod tests { let circuit_config = CircuitConfig::standard_recursion_config(); let mut builder = CircuitBuilder::::new(circuit_config); - // let mut pw = PartialWitness::new(); - recursive_all_proof.verify(inner_config) - // recursive_all_proof.verify_circuit(&mut builder, &mut pw); - // - // let data = builder.build::(); - // let proof = data.prove(pw)?; - // data.verify(proof) + let mut pw = PartialWitness::new(); + recursive_all_proof.verify_circuit(&mut builder, &mut pw, inner_config); + + let data = builder.build::(); + let proof = data.prove(pw)?; + data.verify(proof) } fn init_logger() { diff --git a/evm/src/cross_table_lookup.rs b/evm/src/cross_table_lookup.rs index 118b7f09..24b8059c 100644 --- a/evm/src/cross_table_lookup.rs +++ b/evm/src/cross_table_lookup.rs @@ -673,18 +673,12 @@ pub(crate) fn verify_cross_table_lookups_circuit< >( builder: &mut CircuitBuilder, cross_table_lookups: Vec>, - proofs: &[StarkProofTarget; NUM_TABLES], + ctl_zs_lasts: [Vec; NUM_TABLES], + degrees_bits: [usize; NUM_TABLES], challenges: GrandProductChallengeSet, inner_config: &StarkConfig, ) { - let degrees_bits = proofs - .iter() - .map(|p| p.recover_degree_bits(inner_config)) - .collect::>(); - let mut ctl_zs_openings = proofs - .iter() - .map(|p| p.openings.ctl_zs_last.iter()) - .collect::>(); + let mut ctl_zs_openings = ctl_zs_lasts.iter().map(|v| v.iter()).collect::>(); for ( i, CrossTableLookup { diff --git a/evm/src/recursive_verifier.rs b/evm/src/recursive_verifier.rs index 394d4f33..95d8cd80 100644 --- a/evm/src/recursive_verifier.rs +++ b/evm/src/recursive_verifier.rs @@ -1,3 +1,5 @@ +use std::fmt::Debug; + use anyhow::{ensure, Result}; use itertools::Itertools; use plonky2::field::extension::Extendable; @@ -33,8 +35,8 @@ use crate::keccak_memory::keccak_memory_stark::KeccakMemoryStark; use crate::logic::LogicStark; use crate::memory::memory_stark::MemoryStark; use crate::permutation::{ - get_grand_product_challenge_set, GrandProductChallenge, GrandProductChallengeSet, - PermutationCheckDataTarget, + get_grand_product_challenge_set, get_grand_product_challenge_set_target, GrandProductChallenge, + GrandProductChallengeSet, PermutationCheckDataTarget, }; use crate::proof::{ AllChallengerState, AllProof, AllProofChallengesTarget, AllProofTarget, BlockMetadata, @@ -58,25 +60,21 @@ pub struct RecursiveAllProof< pub cross_table_lookups: Vec>, } -struct PublicInputs, C: GenericConfig, const D: usize> { - trace_cap: MerkleCap, - ctl_zs_last: Vec, - ctl_challenges: GrandProductChallengeSet, - challenger_state_before: [F; SPONGE_WIDTH], - challenger_state_after: [F; SPONGE_WIDTH], +struct PublicInputs { + trace_cap: Vec>, + ctl_zs_last: Vec, + ctl_challenges: GrandProductChallengeSet, + challenger_state_before: [T; SPONGE_WIDTH], + challenger_state_after: [T; SPONGE_WIDTH], } -impl, C: GenericConfig, const D: usize> - PublicInputs -{ - fn from_vec(v: &[F], config: &StarkConfig) -> Self { +impl PublicInputs { + fn from_vec(v: &[T], config: &StarkConfig) -> Self { let mut start = 0; - let trace_cap = MerkleCap( - v[start..4 * (1 << config.fri_config.cap_height)] - .chunks(4) - .map(|chunk| >::Hash::from_vec(chunk)) - .collect(), - ); + let trace_cap = v[start..4 * (1 << config.fri_config.cap_height)] + .chunks(4) + .map(|chunk| chunk.to_vec()) + .collect(); start += 4 * (1 << config.fri_config.cap_height); let ctl_challenges = GrandProductChallengeSet { challenges: (0..config.num_challenges) @@ -114,27 +112,31 @@ impl, C: GenericConfig, const D: usize> [(); C::Hasher::HASH_SIZE]:, { let pis: [_; NUM_TABLES] = std::array::from_fn(|i| { - PublicInputs::::from_vec( - &self.recursive_proofs[i].0.public_inputs, - inner_config, - ) + PublicInputs::from_vec(&self.recursive_proofs[i].0.public_inputs, inner_config) }); let mut challenger = Challenger::::new(); for pi in &pis { - challenger.observe_cap(&pi.trace_cap); + for h in &pi.trace_cap { + challenger.observe_elements(h); + } } let ctl_challenges = get_grand_product_challenge_set(&mut challenger, inner_config.num_challenges); + // Check that the correct CTL challenges are used in every proof. for pi in &pis { ensure!(ctl_challenges == pi.ctl_challenges); } + challenger.duplexing(); let state = challenger.state(); ensure!(state == pis[0].challenger_state_before); + // Check that the challenger state is consistent between proofs. for i in 1..NUM_TABLES { ensure!(pis[i].challenger_state_before == pis[i - 1].challenger_state_after); } + + // Verify the CTL checks. let degrees_bits = std::array::from_fn(|i| self.recursive_proofs[i].1.common.degree_bits); verify_cross_table_lookups::( self.cross_table_lookups, @@ -143,6 +145,8 @@ impl, C: GenericConfig, const D: usize> ctl_challenges, inner_config, )?; + + // Verify the proofs. for (proof, verifier_data) in self.recursive_proofs { verifier_data.verify(proof)?; } @@ -150,13 +154,19 @@ impl, C: GenericConfig, const D: usize> } /// Recursively verify every recursive proof. - pub fn verify_circuit(&self, builder: &mut CircuitBuilder, pw: &mut W) - where + pub fn verify_circuit( + self, + builder: &mut CircuitBuilder, + pw: &mut W, + inner_config: &StarkConfig, + ) where W: Witness, [(); C::Hasher::HASH_SIZE]:, >::Hasher: AlgebraicHasher, { - for (proof, verifier_data) in &self.recursive_proofs { + let proofs_target: [_; NUM_TABLES] = std::array::from_fn(|i| { + let verifier_data = &self.recursive_proofs[i].1; + let proof = &self.recursive_proofs[i].0; let pt = builder.add_virtual_proof_with_pis(&verifier_data.common); pw.set_proof_with_pis_target(&pt, proof); let inner_data = VerifierCircuitTarget { @@ -167,7 +177,69 @@ impl, C: GenericConfig, const D: usize> &inner_data.constants_sigmas_cap, &verifier_data.verifier_only.constants_sigmas_cap, ); - builder.verify_proof(pt, &inner_data, &verifier_data.common); + (pt, inner_data) + }); + + let pis: [_; NUM_TABLES] = std::array::from_fn(|i| { + PublicInputs::from_vec(&proofs_target[i].0.public_inputs, inner_config) + }); + + let mut challenger = RecursiveChallenger::::new(builder); + for pi in &pis { + for h in &pi.trace_cap { + challenger.observe_elements(h); + } + } + let ctl_challenges = get_grand_product_challenge_set_target( + builder, + &mut challenger, + inner_config.num_challenges, + ); + // Check that the correct CTL challenges are used in every proof. + for pi in &pis { + for i in 0..inner_config.num_challenges { + builder.connect( + ctl_challenges.challenges[i].beta, + pi.ctl_challenges.challenges[i].beta, + ); + builder.connect( + ctl_challenges.challenges[i].gamma, + pi.ctl_challenges.challenges[i].gamma, + ); + } + } + + challenger.duplexing(builder); + let state = challenger.state(); + for k in 0..SPONGE_WIDTH { + builder.connect(state[k], pis[0].challenger_state_before[k]); + } + // Check that the challenger state is consistent between proofs. + for i in 1..NUM_TABLES { + for k in 0..SPONGE_WIDTH { + builder.connect( + pis[i].challenger_state_before[k], + pis[i - 1].challenger_state_after[k], + ); + } + } + + // Verify the CTL checks. + let degrees_bits = std::array::from_fn(|i| self.recursive_proofs[i].1.common.degree_bits); + verify_cross_table_lookups_circuit::( + builder, + self.cross_table_lookups, + pis.map(|p| p.ctl_zs_last), + degrees_bits, + ctl_challenges, + inner_config, + ); + for (i, (proof_target, inner_data)) in proofs_target.into_iter().enumerate() { + builder.verify_proof( + proof_target, + &inner_data, + &self.recursive_proofs[i].1.common, + ); } } } @@ -353,119 +425,119 @@ where }) } -pub fn verify_proof_circuit< - F: RichField + Extendable, - C: GenericConfig, - const D: usize, ->( - builder: &mut CircuitBuilder, - all_stark: AllStark, - all_proof: AllProofTarget, - inner_config: &StarkConfig, -) where - [(); CpuStark::::COLUMNS]:, - [(); KeccakStark::::COLUMNS]:, - [(); KeccakMemoryStark::::COLUMNS]:, - [(); LogicStark::::COLUMNS]:, - [(); MemoryStark::::COLUMNS]:, - C::Hasher: AlgebraicHasher, -{ - 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, - keccak_memory_stark, - logic_stark, - memory_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, - ); - - with_context!( - builder, - "verify CPU proof", - verify_stark_proof_with_challenges_circuit::( - builder, - &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, - ) - ); - with_context!( - builder, - "verify Keccak proof", - 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, - ) - ); - with_context!( - builder, - "verify Keccak memory proof", - verify_stark_proof_with_challenges_circuit::( - builder, - &keccak_memory_stark, - &all_proof.stark_proofs[Table::KeccakMemory as usize], - &stark_challenges[Table::KeccakMemory as usize], - &ctl_vars_per_table[Table::KeccakMemory as usize], - inner_config, - ) - ); - with_context!( - builder, - "verify logic proof", - verify_stark_proof_with_challenges_circuit::( - builder, - &logic_stark, - &all_proof.stark_proofs[Table::Logic as usize], - &stark_challenges[Table::Logic as usize], - &ctl_vars_per_table[Table::Logic as usize], - inner_config, - ) - ); - with_context!( - builder, - "verify memory proof", - verify_stark_proof_with_challenges_circuit::( - builder, - &memory_stark, - &all_proof.stark_proofs[Table::Memory as usize], - &stark_challenges[Table::Memory as usize], - &ctl_vars_per_table[Table::Memory as usize], - inner_config, - ) - ); - - with_context!( - builder, - "verify cross-table lookups", - verify_cross_table_lookups_circuit::( - builder, - cross_table_lookups, - &all_proof.stark_proofs, - ctl_challenges, - inner_config, - ) - ); -} +// pub fn verify_proof_circuit< +// F: RichField + Extendable, +// C: GenericConfig, +// const D: usize, +// >( +// builder: &mut CircuitBuilder, +// all_stark: AllStark, +// all_proof: AllProofTarget, +// inner_config: &StarkConfig, +// ) where +// [(); CpuStark::::COLUMNS]:, +// [(); KeccakStark::::COLUMNS]:, +// [(); KeccakMemoryStark::::COLUMNS]:, +// [(); LogicStark::::COLUMNS]:, +// [(); MemoryStark::::COLUMNS]:, +// C::Hasher: AlgebraicHasher, +// { +// 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, +// keccak_memory_stark, +// logic_stark, +// memory_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, +// ); +// +// with_context!( +// builder, +// "verify CPU proof", +// verify_stark_proof_with_challenges_circuit::( +// builder, +// &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, +// ) +// ); +// with_context!( +// builder, +// "verify Keccak proof", +// 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, +// ) +// ); +// with_context!( +// builder, +// "verify Keccak memory proof", +// verify_stark_proof_with_challenges_circuit::( +// builder, +// &keccak_memory_stark, +// &all_proof.stark_proofs[Table::KeccakMemory as usize], +// &stark_challenges[Table::KeccakMemory as usize], +// &ctl_vars_per_table[Table::KeccakMemory as usize], +// inner_config, +// ) +// ); +// with_context!( +// builder, +// "verify logic proof", +// verify_stark_proof_with_challenges_circuit::( +// builder, +// &logic_stark, +// &all_proof.stark_proofs[Table::Logic as usize], +// &stark_challenges[Table::Logic as usize], +// &ctl_vars_per_table[Table::Logic as usize], +// inner_config, +// ) +// ); +// with_context!( +// builder, +// "verify memory proof", +// verify_stark_proof_with_challenges_circuit::( +// builder, +// &memory_stark, +// &all_proof.stark_proofs[Table::Memory as usize], +// &stark_challenges[Table::Memory as usize], +// &ctl_vars_per_table[Table::Memory as usize], +// inner_config, +// ) +// ); +// +// with_context!( +// builder, +// "verify cross-table lookups", +// verify_cross_table_lookups_circuit::( +// builder, +// cross_table_lookups, +// &all_proof.stark_proofs, +// ctl_challenges, +// inner_config, +// ) +// ); +// } /// Recursively verifies an inner proof. fn verify_stark_proof_with_challenges_circuit< diff --git a/plonky2/src/iop/challenger.rs b/plonky2/src/iop/challenger.rs index 1a9e3f13..eeb18038 100644 --- a/plonky2/src/iop/challenger.rs +++ b/plonky2/src/iop/challenger.rs @@ -196,7 +196,7 @@ impl, H: AlgebraicHasher, const D: usize> self.input_buffer.push(target); } - pub(crate) fn observe_elements(&mut self, targets: &[Target]) { + pub fn observe_elements(&mut self, targets: &[Target]) { for &target in targets { self.observe_element(target); }