From 6cf6b56aa0fbb6529be1050f5ca4f872189f1e05 Mon Sep 17 00:00:00 2001 From: wborgeaud Date: Mon, 26 Sep 2022 15:47:35 +0200 Subject: [PATCH] Method to compute verifier data without proving --- evm/src/all_stark.rs | 14 ++- evm/src/cross_table_lookup.rs | 15 +++ evm/src/recursive_verifier.rs | 200 +++++++++++++++++++++++++++++----- 3 files changed, 201 insertions(+), 28 deletions(-) diff --git a/evm/src/all_stark.rs b/evm/src/all_stark.rs index 7d7b0932..b160a425 100644 --- a/evm/src/all_stark.rs +++ b/evm/src/all_stark.rs @@ -194,7 +194,9 @@ mod tests { use crate::memory::NUM_CHANNELS; use crate::proof::{AllProof, PublicValues}; use crate::prover::prove_with_traces; - use crate::recursive_verifier::recursively_verify_all_proof; + use crate::recursive_verifier::{ + all_verifier_data_recursive_stark_proof, recursively_verify_all_proof, + }; use crate::stark::Stark; use crate::util::{limb_from_bits_le, trace_rows_to_poly_values}; use crate::verifier::verify_proof; @@ -750,13 +752,19 @@ mod tests { &inner_all_stark, &inner_proof, inner_config, - circuit_config, + &circuit_config, )?; + let verifier_data = all_verifier_data_recursive_stark_proof( + &inner_all_stark, + inner_proof.degree_bits(inner_config), + inner_config, + &circuit_config, + ); let circuit_config = CircuitConfig::standard_recursion_config(); let mut builder = CircuitBuilder::::new(circuit_config); let mut pw = PartialWitness::new(); - recursive_all_proof.verify_circuit(&mut builder, &mut pw, inner_config); + recursive_all_proof.verify_circuit(&mut builder, &mut pw, &verifier_data, inner_config); let data = builder.build::(); let proof = data.prove(pw)?; diff --git a/evm/src/cross_table_lookup.rs b/evm/src/cross_table_lookup.rs index 429a4fce..1b42801f 100644 --- a/evm/src/cross_table_lookup.rs +++ b/evm/src/cross_table_lookup.rs @@ -191,6 +191,21 @@ impl CrossTableLookup { default, } } + + pub(crate) fn num_ctl_zs(ctls: &[Self], table: Table, num_challenges: usize) -> usize { + let mut ans = 0; + for ctl in ctls { + ans += ctl + .looking_tables + .iter() + .filter_map(|twc| (twc.table == table).then_some(num_challenges)) + .sum::(); + ans += (ctl.looked_table.table == table) + .then_some(num_challenges) + .unwrap_or_default(); + } + ans + } } /// Cross-table lookup data for one table. diff --git a/evm/src/recursive_verifier.rs b/evm/src/recursive_verifier.rs index fd52c218..03d4e4bd 100644 --- a/evm/src/recursive_verifier.rs +++ b/evm/src/recursive_verifier.rs @@ -52,8 +52,7 @@ pub struct RecursiveAllProof< C: GenericConfig, const D: usize, > { - pub recursive_proofs: - [(ProofWithPublicInputs, VerifierCircuitData); NUM_TABLES], + pub recursive_proofs: [ProofWithPublicInputs; NUM_TABLES], pub cross_table_lookups: Vec>, } @@ -104,12 +103,16 @@ impl, C: GenericConfig, const D: usize> RecursiveAllProof { /// Verify every recursive proof. - pub fn verify(self, inner_config: &StarkConfig) -> Result<()> + pub fn verify( + self, + verifier_data: &[VerifierCircuitData; NUM_TABLES], + inner_config: &StarkConfig, + ) -> Result<()> where [(); 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].public_inputs, inner_config) }); let mut challenger = Challenger::::new(); @@ -134,7 +137,7 @@ impl, C: GenericConfig, const D: usize> } // Verify the CTL checks. - let degrees_bits = std::array::from_fn(|i| self.recursive_proofs[i].1.common.degree_bits); + let degrees_bits = std::array::from_fn(|i| verifier_data[i].common.degree_bits); verify_cross_table_lookups::( self.cross_table_lookups, pis.map(|p| p.ctl_zs_last), @@ -144,7 +147,7 @@ impl, C: GenericConfig, const D: usize> )?; // Verify the proofs. - for (proof, verifier_data) in self.recursive_proofs { + for (proof, verifier_data) in self.recursive_proofs.into_iter().zip(verifier_data) { verifier_data.verify(proof)?; } Ok(()) @@ -155,6 +158,7 @@ impl, C: GenericConfig, const D: usize> self, builder: &mut CircuitBuilder, pw: &mut W, + verifier_data: &[VerifierCircuitData; NUM_TABLES], inner_config: &StarkConfig, ) where W: Witness, @@ -162,8 +166,8 @@ impl, C: GenericConfig, const D: usize> >::Hasher: AlgebraicHasher, { 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 verifier_data = &verifier_data[i]; + let proof = &self.recursive_proofs[i]; let pt = builder.add_virtual_proof_with_pis(&verifier_data.common); pw.set_proof_with_pis_target(&pt, proof); let inner_data = VerifierCircuitTarget { @@ -222,7 +226,7 @@ impl, C: GenericConfig, const D: usize> } // Verify the CTL checks. - let degrees_bits = std::array::from_fn(|i| self.recursive_proofs[i].1.common.degree_bits); + let degrees_bits = std::array::from_fn(|i| verifier_data[i].common.degree_bits); verify_cross_table_lookups_circuit::( builder, self.cross_table_lookups, @@ -232,11 +236,7 @@ impl, C: GenericConfig, const D: usize> 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, - ); + builder.verify_proof(proof_target, &inner_data, &verifier_data[i].common); } } } @@ -341,6 +341,151 @@ where Ok((data.prove(pw)?, data.verifier_data())) } +/// Returns the verifier data for the recursively Stark circuit. +fn verifier_data_recursive_stark_proof< + F: RichField + Extendable, + C: GenericConfig, + S: Stark, + const D: usize, +>( + table: Table, + stark: S, + degree_bits: usize, + cross_table_lookups: &[CrossTableLookup], + inner_config: &StarkConfig, + circuit_config: &CircuitConfig, +) -> VerifierCircuitData +where + [(); S::COLUMNS]:, + [(); C::Hasher::HASH_SIZE]:, + C::Hasher: AlgebraicHasher, +{ + let mut builder = CircuitBuilder::::new(circuit_config.clone()); + + let num_permutation_zs = stark.num_permutation_batches(inner_config); + let num_permutation_batch_size = stark.permutation_batch_size(); + let num_ctl_zs = + CrossTableLookup::num_ctl_zs(cross_table_lookups, table, inner_config.num_challenges); + let proof_target = + add_virtual_stark_proof(&mut builder, &stark, inner_config, degree_bits, num_ctl_zs); + builder.register_public_inputs( + &proof_target + .trace_cap + .0 + .iter() + .flat_map(|h| h.elements) + .collect::>(), + ); + + let ctl_challenges_target = GrandProductChallengeSet { + challenges: (0..inner_config.num_challenges) + .map(|_| GrandProductChallenge { + beta: builder.add_virtual_public_input(), + gamma: builder.add_virtual_public_input(), + }) + .collect(), + }; + + let ctl_vars = CtlCheckVarsTarget::from_proof( + table, + &proof_target, + cross_table_lookups, + &ctl_challenges_target, + num_permutation_zs, + ); + + let challenger_state = std::array::from_fn(|_| builder.add_virtual_public_input()); + let mut challenger = RecursiveChallenger::::from_state(challenger_state); + let challenges = proof_target.get_challenges::( + &mut builder, + &mut challenger, + num_permutation_zs > 0, + num_permutation_batch_size, + inner_config, + ); + challenger.duplexing(&mut builder); + let challenger_state = challenger.state(); + builder.register_public_inputs(&challenger_state); + + builder.register_public_inputs(&proof_target.openings.ctl_zs_last); + + verify_stark_proof_with_challenges_circuit::( + &mut builder, + &stark, + &proof_target, + &challenges, + &ctl_vars, + inner_config, + ); + + let data = builder.build::(); + data.verifier_data() +} + +/// Recursively verify every Stark proof in an `AllProof`. +pub fn all_verifier_data_recursive_stark_proof< + F: RichField + Extendable, + C: GenericConfig, + const D: usize, +>( + all_stark: &AllStark, + degree_bits: [usize; NUM_TABLES], + inner_config: &StarkConfig, + circuit_config: &CircuitConfig, +) -> [VerifierCircuitData; NUM_TABLES] +where + [(); CpuStark::::COLUMNS]:, + [(); KeccakStark::::COLUMNS]:, + [(); KeccakMemoryStark::::COLUMNS]:, + [(); LogicStark::::COLUMNS]:, + [(); MemoryStark::::COLUMNS]:, + [(); C::Hasher::HASH_SIZE]:, + C::Hasher: AlgebraicHasher, +{ + [ + verifier_data_recursive_stark_proof( + Table::Cpu, + all_stark.cpu_stark, + degree_bits[Table::Cpu as usize], + &all_stark.cross_table_lookups, + inner_config, + circuit_config, + ), + verifier_data_recursive_stark_proof( + Table::Keccak, + all_stark.keccak_stark, + degree_bits[Table::Keccak as usize], + &all_stark.cross_table_lookups, + inner_config, + circuit_config, + ), + verifier_data_recursive_stark_proof( + Table::KeccakMemory, + all_stark.keccak_memory_stark, + degree_bits[Table::KeccakMemory as usize], + &all_stark.cross_table_lookups, + inner_config, + circuit_config, + ), + verifier_data_recursive_stark_proof( + Table::Logic, + all_stark.logic_stark, + degree_bits[Table::Logic as usize], + &all_stark.cross_table_lookups, + inner_config, + circuit_config, + ), + verifier_data_recursive_stark_proof( + Table::Memory, + all_stark.memory_stark, + degree_bits[Table::Memory as usize], + &all_stark.cross_table_lookups, + inner_config, + circuit_config, + ), + ] +} + /// Recursively verify every Stark proof in an `AllProof`. pub fn recursively_verify_all_proof< F: RichField + Extendable, @@ -350,7 +495,7 @@ pub fn recursively_verify_all_proof< all_stark: &AllStark, all_proof: &AllProof, inner_config: &StarkConfig, - circuit_config: CircuitConfig, + circuit_config: &CircuitConfig, ) -> Result> where [(); CpuStark::::COLUMNS]:, @@ -375,8 +520,9 @@ where &ctl_challenges, states[0], inner_config, - &circuit_config, - )?, + circuit_config, + )? + .0, recursively_verify_stark_proof( Table::Keccak, all_stark.keccak_stark, @@ -385,8 +531,9 @@ where &ctl_challenges, states[1], inner_config, - &circuit_config, - )?, + circuit_config, + )? + .0, recursively_verify_stark_proof( Table::KeccakMemory, all_stark.keccak_memory_stark, @@ -395,8 +542,9 @@ where &ctl_challenges, states[2], inner_config, - &circuit_config, - )?, + circuit_config, + )? + .0, recursively_verify_stark_proof( Table::Logic, all_stark.logic_stark, @@ -405,8 +553,9 @@ where &ctl_challenges, states[3], inner_config, - &circuit_config, - )?, + circuit_config, + )? + .0, recursively_verify_stark_proof( Table::Memory, all_stark.memory_stark, @@ -415,8 +564,9 @@ where &ctl_challenges, states[4], inner_config, - &circuit_config, - )?, + circuit_config, + )? + .0, ], cross_table_lookups: all_stark.cross_table_lookups.clone(), })