mirror of
https://github.com/logos-storage/plonky2.git
synced 2026-01-04 06:43:07 +00:00
Merge pull request #708 from mir-protocol/per_table_recursion
Per table recursion
This commit is contained in:
commit
992692b04d
@ -65,7 +65,7 @@ impl<F: RichField + Extendable<D>, const D: usize> AllStark<F, D> {
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Debug, Copy, Clone)]
|
||||
#[derive(Debug, Copy, Clone, Eq, PartialEq)]
|
||||
pub enum Table {
|
||||
Cpu = 0,
|
||||
Keccak = 1,
|
||||
@ -185,12 +185,12 @@ mod tests {
|
||||
use plonky2::field::types::{Field, PrimeField64};
|
||||
use plonky2::iop::witness::PartialWitness;
|
||||
use plonky2::plonk::circuit_builder::CircuitBuilder;
|
||||
use plonky2::plonk::circuit_data::CircuitConfig;
|
||||
use plonky2::plonk::circuit_data::{CircuitConfig, VerifierCircuitData};
|
||||
use plonky2::plonk::config::{GenericConfig, PoseidonGoldilocksConfig};
|
||||
use plonky2::util::timing::TimingTree;
|
||||
use rand::{thread_rng, Rng};
|
||||
|
||||
use crate::all_stark::AllStark;
|
||||
use crate::all_stark::{AllStark, NUM_TABLES};
|
||||
use crate::config::StarkConfig;
|
||||
use crate::cpu::cpu_stark::CpuStark;
|
||||
use crate::cpu::kernel::aggregator::KERNEL;
|
||||
@ -203,8 +203,10 @@ mod tests {
|
||||
use crate::memory::NUM_CHANNELS;
|
||||
use crate::proof::{AllProof, PublicValues};
|
||||
use crate::prover::prove_with_traces;
|
||||
use crate::recursive_verifier::tests::recursively_verify_all_proof;
|
||||
use crate::recursive_verifier::{
|
||||
add_virtual_all_proof, set_all_proof_target, verify_proof_circuit,
|
||||
add_virtual_recursive_all_proof, all_verifier_data_recursive_stark_proof,
|
||||
set_recursive_all_proof_target, RecursiveAllProof,
|
||||
};
|
||||
use crate::stark::Stark;
|
||||
use crate::util::{limb_from_bits_le, trace_rows_to_poly_values};
|
||||
@ -232,7 +234,7 @@ mod tests {
|
||||
) -> Vec<PolynomialValues<F>> {
|
||||
keccak_memory_stark.generate_trace(
|
||||
vec![],
|
||||
1 << config.fri_config.cap_height,
|
||||
config.fri_config.num_cap_elements(),
|
||||
&mut TimingTree::default(),
|
||||
)
|
||||
}
|
||||
@ -359,6 +361,7 @@ mod tests {
|
||||
let row: &mut cpu::columns::CpuColumnsView<F> = cpu_trace_rows[clock].borrow_mut();
|
||||
row.clock = F::from_canonical_usize(clock);
|
||||
|
||||
dbg!(channel, row.mem_channels.len());
|
||||
let channel = &mut row.mem_channels[channel];
|
||||
channel.used = F::ONE;
|
||||
channel.is_read = memory_trace[memory::columns::IS_READ].values[i];
|
||||
@ -754,34 +757,42 @@ mod tests {
|
||||
let (all_stark, proof) = get_proof(&config)?;
|
||||
verify_proof(all_stark.clone(), proof.clone(), &config)?;
|
||||
|
||||
recursive_proof(all_stark, proof, &config, true)
|
||||
recursive_proof(all_stark, proof, &config)
|
||||
}
|
||||
|
||||
fn recursive_proof(
|
||||
inner_all_stark: AllStark<F, D>,
|
||||
inner_proof: AllProof<F, C, D>,
|
||||
inner_config: &StarkConfig,
|
||||
print_gate_counts: bool,
|
||||
) -> Result<()> {
|
||||
let circuit_config = CircuitConfig::standard_recursion_config();
|
||||
let recursive_all_proof = recursively_verify_all_proof(
|
||||
&inner_all_stark,
|
||||
&inner_proof,
|
||||
inner_config,
|
||||
&circuit_config,
|
||||
)?;
|
||||
|
||||
let verifier_data: [VerifierCircuitData<F, C, D>; NUM_TABLES] =
|
||||
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::<F, D>::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(
|
||||
let recursive_all_proof_target =
|
||||
add_virtual_recursive_all_proof(&mut builder, &verifier_data);
|
||||
set_recursive_all_proof_target(&mut pw, &recursive_all_proof_target, &recursive_all_proof);
|
||||
RecursiveAllProof::verify_circuit(
|
||||
&mut builder,
|
||||
&inner_all_stark,
|
||||
recursive_all_proof_target,
|
||||
&verifier_data,
|
||||
inner_all_stark.cross_table_lookups,
|
||||
inner_config,
|
||||
°ree_bits,
|
||||
&nums_ctl_zs,
|
||||
);
|
||||
set_all_proof_target(&mut pw, &pt, &inner_proof, builder.zero());
|
||||
|
||||
verify_proof_circuit::<F, C, D>(&mut builder, inner_all_stark, pt, inner_config);
|
||||
|
||||
if print_gate_counts {
|
||||
builder.print_gate_counts(0);
|
||||
}
|
||||
|
||||
let data = builder.build::<C>();
|
||||
let proof = data.prove(pw)?;
|
||||
|
||||
@ -191,6 +191,15 @@ impl<F: Field> CrossTableLookup<F> {
|
||||
default,
|
||||
}
|
||||
}
|
||||
|
||||
pub(crate) fn num_ctl_zs(ctls: &[Self], table: Table, num_challenges: usize) -> usize {
|
||||
let mut num_ctls = 0;
|
||||
for ctl in ctls {
|
||||
let all_tables = std::iter::once(&ctl.looked_table).chain(&ctl.looking_tables);
|
||||
num_ctls += all_tables.filter(|twc| twc.table == table).count();
|
||||
}
|
||||
num_ctls * num_challenges
|
||||
}
|
||||
}
|
||||
|
||||
/// Cross-table lookup data for one table.
|
||||
@ -450,24 +459,24 @@ pub struct CtlCheckVarsTarget<'a, F: Field, const D: usize> {
|
||||
}
|
||||
|
||||
impl<'a, F: Field, const D: usize> CtlCheckVarsTarget<'a, F, D> {
|
||||
pub(crate) fn from_proofs(
|
||||
proofs: &[StarkProofTarget<D>; NUM_TABLES],
|
||||
pub(crate) fn from_proof(
|
||||
table: Table,
|
||||
proof: &StarkProofTarget<D>,
|
||||
cross_table_lookups: &'a [CrossTableLookup<F>],
|
||||
ctl_challenges: &'a GrandProductChallengeSet<Target>,
|
||||
num_permutation_zs: &[usize; NUM_TABLES],
|
||||
) -> [Vec<Self>; NUM_TABLES] {
|
||||
let mut ctl_zs = proofs
|
||||
.iter()
|
||||
.zip(num_permutation_zs)
|
||||
.map(|(p, &num_perms)| {
|
||||
let openings = &p.openings;
|
||||
let ctl_zs = openings.permutation_ctl_zs.iter().skip(num_perms);
|
||||
let ctl_zs_next = openings.permutation_ctl_zs_next.iter().skip(num_perms);
|
||||
ctl_zs.zip(ctl_zs_next)
|
||||
})
|
||||
.collect::<Vec<_>>();
|
||||
num_permutation_zs: usize,
|
||||
) -> Vec<Self> {
|
||||
let mut ctl_zs = {
|
||||
let openings = &proof.openings;
|
||||
let ctl_zs = openings.permutation_ctl_zs.iter().skip(num_permutation_zs);
|
||||
let ctl_zs_next = openings
|
||||
.permutation_ctl_zs_next
|
||||
.iter()
|
||||
.skip(num_permutation_zs);
|
||||
ctl_zs.zip(ctl_zs_next)
|
||||
};
|
||||
|
||||
let mut ctl_vars_per_table = [0; NUM_TABLES].map(|_| vec![]);
|
||||
let mut ctl_vars = vec![];
|
||||
for CrossTableLookup {
|
||||
looking_tables,
|
||||
looked_table,
|
||||
@ -475,28 +484,33 @@ impl<'a, F: Field, const D: usize> CtlCheckVarsTarget<'a, F, D> {
|
||||
} in cross_table_lookups
|
||||
{
|
||||
for &challenges in &ctl_challenges.challenges {
|
||||
for table in looking_tables {
|
||||
let (looking_z, looking_z_next) = ctl_zs[table.table as usize].next().unwrap();
|
||||
ctl_vars_per_table[table.table as usize].push(Self {
|
||||
local_z: *looking_z,
|
||||
next_z: *looking_z_next,
|
||||
challenges,
|
||||
columns: &table.columns,
|
||||
filter_column: &table.filter_column,
|
||||
});
|
||||
for looking_table in looking_tables {
|
||||
if looking_table.table == table {
|
||||
let (looking_z, looking_z_next) = ctl_zs.next().unwrap();
|
||||
ctl_vars.push(Self {
|
||||
local_z: *looking_z,
|
||||
next_z: *looking_z_next,
|
||||
challenges,
|
||||
columns: &looking_table.columns,
|
||||
filter_column: &looking_table.filter_column,
|
||||
});
|
||||
}
|
||||
}
|
||||
|
||||
let (looked_z, looked_z_next) = ctl_zs[looked_table.table as usize].next().unwrap();
|
||||
ctl_vars_per_table[looked_table.table as usize].push(Self {
|
||||
local_z: *looked_z,
|
||||
next_z: *looked_z_next,
|
||||
challenges,
|
||||
columns: &looked_table.columns,
|
||||
filter_column: &looked_table.filter_column,
|
||||
});
|
||||
if looked_table.table == table {
|
||||
let (looked_z, looked_z_next) = ctl_zs.next().unwrap();
|
||||
ctl_vars.push(Self {
|
||||
local_z: *looked_z,
|
||||
next_z: *looked_z_next,
|
||||
challenges,
|
||||
columns: &looked_table.columns,
|
||||
filter_column: &looked_table.filter_column,
|
||||
});
|
||||
}
|
||||
}
|
||||
}
|
||||
ctl_vars_per_table
|
||||
assert!(ctl_zs.next().is_none());
|
||||
ctl_vars
|
||||
}
|
||||
}
|
||||
|
||||
@ -568,18 +582,12 @@ pub(crate) fn verify_cross_table_lookups<
|
||||
const D: usize,
|
||||
>(
|
||||
cross_table_lookups: Vec<CrossTableLookup<F>>,
|
||||
proofs: &[StarkProof<F, C, D>; NUM_TABLES],
|
||||
ctl_zs_lasts: [Vec<F>; NUM_TABLES],
|
||||
degrees_bits: [usize; NUM_TABLES],
|
||||
challenges: GrandProductChallengeSet<F>,
|
||||
config: &StarkConfig,
|
||||
) -> Result<()> {
|
||||
let degrees_bits = proofs
|
||||
.iter()
|
||||
.map(|p| p.recover_degree_bits(config))
|
||||
.collect::<Vec<_>>();
|
||||
let mut ctl_zs_openings = proofs
|
||||
.iter()
|
||||
.map(|p| p.openings.ctl_zs_last.iter())
|
||||
.collect::<Vec<_>>();
|
||||
let mut ctl_zs_openings = ctl_zs_lasts.iter().map(|v| v.iter()).collect::<Vec<_>>();
|
||||
for (
|
||||
i,
|
||||
CrossTableLookup {
|
||||
@ -626,18 +634,12 @@ pub(crate) fn verify_cross_table_lookups_circuit<
|
||||
>(
|
||||
builder: &mut CircuitBuilder<F, D>,
|
||||
cross_table_lookups: Vec<CrossTableLookup<F>>,
|
||||
proofs: &[StarkProofTarget<D>; NUM_TABLES],
|
||||
ctl_zs_lasts: [Vec<Target>; NUM_TABLES],
|
||||
degrees_bits: [usize; NUM_TABLES],
|
||||
challenges: GrandProductChallengeSet<Target>,
|
||||
inner_config: &StarkConfig,
|
||||
) {
|
||||
let degrees_bits = proofs
|
||||
.iter()
|
||||
.map(|p| p.recover_degree_bits(inner_config))
|
||||
.collect::<Vec<_>>();
|
||||
let mut ctl_zs_openings = proofs
|
||||
.iter()
|
||||
.map(|p| p.openings.ctl_zs_last.iter())
|
||||
.collect::<Vec<_>>();
|
||||
let mut ctl_zs_openings = ctl_zs_lasts.iter().map(|v| v.iter()).collect::<Vec<_>>();
|
||||
for (
|
||||
i,
|
||||
CrossTableLookup {
|
||||
|
||||
@ -116,7 +116,7 @@ pub(crate) fn generate_traces<F: RichField + Extendable<D>, const D: usize>(
|
||||
let keccak_trace = all_stark.keccak_stark.generate_trace(keccak_inputs, timing);
|
||||
let keccak_memory_trace = all_stark.keccak_memory_stark.generate_trace(
|
||||
keccak_memory_inputs,
|
||||
1 << config.fri_config.cap_height,
|
||||
config.fri_config.num_cap_elements(),
|
||||
timing,
|
||||
);
|
||||
let logic_trace = all_stark.logic_stark.generate_trace(logic_ops, timing);
|
||||
|
||||
@ -5,11 +5,11 @@ use plonky2::iop::challenger::{Challenger, RecursiveChallenger};
|
||||
use plonky2::plonk::circuit_builder::CircuitBuilder;
|
||||
use plonky2::plonk::config::{AlgebraicHasher, GenericConfig};
|
||||
|
||||
use crate::all_stark::AllStark;
|
||||
use crate::all_stark::{AllStark, NUM_TABLES};
|
||||
use crate::config::StarkConfig;
|
||||
use crate::permutation::{
|
||||
get_grand_product_challenge_set, get_grand_product_challenge_set_target,
|
||||
get_n_grand_product_challenge_sets, get_n_grand_product_challenge_sets_target,
|
||||
get_grand_product_challenge_set, get_n_grand_product_challenge_sets,
|
||||
get_n_grand_product_challenge_sets_target,
|
||||
};
|
||||
use crate::proof::*;
|
||||
|
||||
@ -36,6 +36,7 @@ impl<F: RichField + Extendable<D>, C: GenericConfig<D, F = F>, const D: usize> A
|
||||
|
||||
AllProofChallenges {
|
||||
stark_challenges: std::array::from_fn(|i| {
|
||||
challenger.compact();
|
||||
self.stark_proofs[i].get_challenges(
|
||||
&mut challenger,
|
||||
num_permutation_zs[i] > 0,
|
||||
@ -46,40 +47,40 @@ impl<F: RichField + Extendable<D>, C: GenericConfig<D, F = F>, const D: usize> A
|
||||
ctl_challenges,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<const D: usize> AllProofTarget<D> {
|
||||
pub(crate) fn get_challenges<F: RichField + Extendable<D>, C: GenericConfig<D, F = F>>(
|
||||
#[allow(unused)] // TODO: should be used soon
|
||||
pub(crate) fn get_challenger_states(
|
||||
&self,
|
||||
builder: &mut CircuitBuilder<F, D>,
|
||||
all_stark: &AllStark<F, D>,
|
||||
config: &StarkConfig,
|
||||
) -> AllProofChallengesTarget<D>
|
||||
where
|
||||
C::Hasher: AlgebraicHasher<F>,
|
||||
{
|
||||
let mut challenger = RecursiveChallenger::<F, C::Hasher, D>::new(builder);
|
||||
) -> AllChallengerState<F, D> {
|
||||
let mut challenger = Challenger::<F, C::Hasher>::new();
|
||||
|
||||
for proof in &self.stark_proofs {
|
||||
challenger.observe_cap(&proof.trace_cap);
|
||||
}
|
||||
|
||||
// TODO: Observe public values.
|
||||
|
||||
let ctl_challenges =
|
||||
get_grand_product_challenge_set_target(builder, &mut challenger, config.num_challenges);
|
||||
get_grand_product_challenge_set(&mut challenger, config.num_challenges);
|
||||
|
||||
let num_permutation_zs = all_stark.nums_permutation_zs(config);
|
||||
let num_permutation_batch_sizes = all_stark.permutation_batch_sizes();
|
||||
|
||||
AllProofChallengesTarget {
|
||||
stark_challenges: std::array::from_fn(|i| {
|
||||
self.stark_proofs[i].get_challenges::<F, C>(
|
||||
builder,
|
||||
&mut challenger,
|
||||
num_permutation_zs[i] > 0,
|
||||
num_permutation_batch_sizes[i],
|
||||
config,
|
||||
)
|
||||
}),
|
||||
let mut challenger_states = vec![challenger.compact()];
|
||||
for i in 0..NUM_TABLES {
|
||||
self.stark_proofs[i].get_challenges(
|
||||
&mut challenger,
|
||||
num_permutation_zs[i] > 0,
|
||||
num_permutation_batch_sizes[i],
|
||||
config,
|
||||
);
|
||||
challenger_states.push(challenger.compact());
|
||||
}
|
||||
|
||||
AllChallengerState {
|
||||
states: challenger_states.try_into().unwrap(),
|
||||
ctl_challenges,
|
||||
}
|
||||
}
|
||||
|
||||
@ -1,5 +1,7 @@
|
||||
//! Permutation arguments.
|
||||
|
||||
use std::fmt::Debug;
|
||||
|
||||
use itertools::Itertools;
|
||||
use maybe_rayon::*;
|
||||
use plonky2::field::batch_util::batch_multiply_inplace;
|
||||
@ -42,14 +44,14 @@ impl PermutationPair {
|
||||
}
|
||||
|
||||
/// A single instance of a permutation check protocol.
|
||||
pub(crate) struct PermutationInstance<'a, T: Copy> {
|
||||
pub(crate) struct PermutationInstance<'a, T: Copy + Eq + PartialEq + Debug> {
|
||||
pub(crate) pair: &'a PermutationPair,
|
||||
pub(crate) challenge: GrandProductChallenge<T>,
|
||||
}
|
||||
|
||||
/// Randomness for a single instance of a permutation check protocol.
|
||||
#[derive(Copy, Clone)]
|
||||
pub(crate) struct GrandProductChallenge<T: Copy> {
|
||||
#[derive(Copy, Clone, Eq, PartialEq, Debug)]
|
||||
pub(crate) struct GrandProductChallenge<T: Copy + Eq + PartialEq + Debug> {
|
||||
/// Randomness used to combine multiple columns into one.
|
||||
pub(crate) beta: T,
|
||||
/// Random offset that's added to the beta-reduced column values.
|
||||
@ -92,8 +94,8 @@ impl GrandProductChallenge<Target> {
|
||||
}
|
||||
|
||||
/// Like `PermutationChallenge`, but with `num_challenges` copies to boost soundness.
|
||||
#[derive(Clone)]
|
||||
pub(crate) struct GrandProductChallengeSet<T: Copy> {
|
||||
#[derive(Clone, Eq, PartialEq, Debug)]
|
||||
pub(crate) struct GrandProductChallengeSet<T: Copy + Eq + PartialEq + Debug> {
|
||||
pub(crate) challenges: Vec<GrandProductChallenge<T>>,
|
||||
}
|
||||
|
||||
@ -261,7 +263,7 @@ pub(crate) fn get_n_grand_product_challenge_sets_target<
|
||||
/// Before batching, each permutation pair leads to `num_challenges` permutation arguments, so we
|
||||
/// start with the cartesian product of `permutation_pairs` and `0..num_challenges`. Then we
|
||||
/// chunk these arguments based on our batch size.
|
||||
pub(crate) fn get_permutation_batches<'a, T: Copy>(
|
||||
pub(crate) fn get_permutation_batches<'a, T: Copy + Eq + PartialEq + Debug>(
|
||||
permutation_pairs: &'a [PermutationPair],
|
||||
permutation_challenge_sets: &[GrandProductChallengeSet<T>],
|
||||
num_challenges: usize,
|
||||
|
||||
@ -8,6 +8,7 @@ use plonky2::fri::structure::{
|
||||
FriOpeningBatch, FriOpeningBatchTarget, FriOpenings, FriOpeningsTarget,
|
||||
};
|
||||
use plonky2::hash::hash_types::{MerkleCapTarget, RichField};
|
||||
use plonky2::hash::hashing::SPONGE_WIDTH;
|
||||
use plonky2::hash::merkle_tree::MerkleCap;
|
||||
use plonky2::iop::ext_target::ExtensionTarget;
|
||||
use plonky2::iop::target::Target;
|
||||
@ -28,10 +29,6 @@ impl<F: RichField + Extendable<D>, C: GenericConfig<D, F = F>, const D: usize> A
|
||||
pub fn degree_bits(&self, config: &StarkConfig) -> [usize; NUM_TABLES] {
|
||||
std::array::from_fn(|i| self.stark_proofs[i].recover_degree_bits(config))
|
||||
}
|
||||
|
||||
pub fn nums_ctl_zs(&self) -> [usize; NUM_TABLES] {
|
||||
std::array::from_fn(|i| self.stark_proofs[i].openings.ctl_zs_last.len())
|
||||
}
|
||||
}
|
||||
|
||||
pub(crate) struct AllProofChallenges<F: RichField + Extendable<D>, const D: usize> {
|
||||
@ -39,6 +36,14 @@ pub(crate) struct AllProofChallenges<F: RichField + Extendable<D>, const D: usiz
|
||||
pub ctl_challenges: GrandProductChallengeSet<F>,
|
||||
}
|
||||
|
||||
#[allow(unused)] // TODO: should be used soon
|
||||
pub(crate) struct AllChallengerState<F: RichField + Extendable<D>, const D: usize> {
|
||||
/// Sponge state of the challenger before starting each proof,
|
||||
/// along with the final state after all proofs are done. This final state isn't strictly needed.
|
||||
pub states: [[F; SPONGE_WIDTH]; NUM_TABLES + 1],
|
||||
pub ctl_challenges: GrandProductChallengeSet<F>,
|
||||
}
|
||||
|
||||
pub struct AllProofTarget<const D: usize> {
|
||||
pub stark_proofs: [StarkProofTarget<D>; NUM_TABLES],
|
||||
pub public_values: PublicValuesTarget,
|
||||
@ -94,11 +99,6 @@ pub struct BlockMetadataTarget {
|
||||
pub block_base_fee: Target,
|
||||
}
|
||||
|
||||
pub(crate) struct AllProofChallengesTarget<const D: usize> {
|
||||
pub stark_challenges: [StarkProofChallengesTarget<D>; NUM_TABLES],
|
||||
pub ctl_challenges: GrandProductChallengeSet<Target>,
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub struct StarkProof<F: RichField + Extendable<D>, C: GenericConfig<D, F = F>, const D: usize> {
|
||||
/// Merkle cap of LDEs of trace values.
|
||||
@ -123,6 +123,10 @@ impl<F: RichField + Extendable<D>, C: GenericConfig<D, F = F>, const D: usize> S
|
||||
let lde_bits = config.fri_config.cap_height + initial_merkle_proof.siblings.len();
|
||||
lde_bits - config.fri_config.rate_bits
|
||||
}
|
||||
|
||||
pub fn num_ctl_zs(&self) -> usize {
|
||||
self.openings.ctl_zs_last.len()
|
||||
}
|
||||
}
|
||||
|
||||
pub struct StarkProofTarget<const D: usize> {
|
||||
|
||||
@ -201,6 +201,8 @@ where
|
||||
"FRI total reduction arity is too large.",
|
||||
);
|
||||
|
||||
challenger.compact();
|
||||
|
||||
// Permutation arguments.
|
||||
let permutation_challenges = stark.uses_permutation_args().then(|| {
|
||||
get_n_grand_product_challenge_sets(
|
||||
|
||||
@ -1,29 +1,44 @@
|
||||
use std::fmt::Debug;
|
||||
|
||||
use anyhow::{ensure, Result};
|
||||
use itertools::Itertools;
|
||||
use plonky2::field::extension::Extendable;
|
||||
use plonky2::field::types::Field;
|
||||
use plonky2::fri::witness_util::set_fri_proof_target;
|
||||
use plonky2::hash::hash_types::RichField;
|
||||
use plonky2::hash::hash_types::{HashOut, RichField};
|
||||
use plonky2::hash::hashing::SPONGE_WIDTH;
|
||||
use plonky2::iop::challenger::{Challenger, RecursiveChallenger};
|
||||
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::circuit_data::{CircuitConfig, VerifierCircuitData, VerifierCircuitTarget};
|
||||
use plonky2::plonk::config::Hasher;
|
||||
use plonky2::plonk::config::{AlgebraicHasher, GenericConfig};
|
||||
use plonky2::plonk::proof::{ProofWithPublicInputs, ProofWithPublicInputsTarget};
|
||||
use plonky2::util::reducing::ReducingFactorTarget;
|
||||
use plonky2::with_context;
|
||||
|
||||
use crate::all_stark::NUM_TABLES;
|
||||
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::cross_table_lookup::{
|
||||
verify_cross_table_lookups, verify_cross_table_lookups_circuit, CrossTableLookup,
|
||||
CtlCheckVarsTarget,
|
||||
};
|
||||
use crate::keccak::keccak_stark::KeccakStark;
|
||||
use crate::keccak_memory::keccak_memory_stark::KeccakMemoryStark;
|
||||
use crate::logic::LogicStark;
|
||||
use crate::memory::memory_stark::MemoryStark;
|
||||
use crate::permutation::PermutationCheckDataTarget;
|
||||
use crate::permutation::{
|
||||
get_grand_product_challenge_set, get_grand_product_challenge_set_target, GrandProductChallenge,
|
||||
GrandProductChallengeSet, PermutationCheckDataTarget,
|
||||
};
|
||||
use crate::proof::{
|
||||
AllProof, AllProofChallengesTarget, AllProofTarget, BlockMetadata, BlockMetadataTarget,
|
||||
PublicValues, PublicValuesTarget, StarkOpeningSetTarget, StarkProof,
|
||||
StarkProofChallengesTarget, StarkProofTarget, TrieRoots, TrieRootsTarget,
|
||||
AllProof, AllProofTarget, BlockMetadata, BlockMetadataTarget, PublicValues, PublicValuesTarget,
|
||||
StarkOpeningSetTarget, StarkProof, StarkProofChallengesTarget, StarkProofTarget, TrieRoots,
|
||||
TrieRootsTarget,
|
||||
};
|
||||
use crate::stark::Stark;
|
||||
use crate::util::h160_limbs;
|
||||
@ -34,118 +49,342 @@ use crate::{
|
||||
util::h256_limbs,
|
||||
};
|
||||
|
||||
pub fn verify_proof_circuit<
|
||||
/// Table-wise recursive proofs of an `AllProof`.
|
||||
pub struct RecursiveAllProof<
|
||||
F: RichField + Extendable<D>,
|
||||
C: GenericConfig<D, F = F>,
|
||||
const D: usize,
|
||||
> {
|
||||
pub recursive_proofs: [ProofWithPublicInputs<F, C, D>; NUM_TABLES],
|
||||
}
|
||||
|
||||
pub struct RecursiveAllProofTargetWithData<const D: usize> {
|
||||
pub recursive_proofs: [ProofWithPublicInputsTarget<D>; NUM_TABLES],
|
||||
pub verifier_data: [VerifierCircuitTarget; NUM_TABLES],
|
||||
}
|
||||
|
||||
struct PublicInputs<T: Copy + Eq + PartialEq + Debug> {
|
||||
trace_cap: Vec<Vec<T>>,
|
||||
ctl_zs_last: Vec<T>,
|
||||
ctl_challenges: GrandProductChallengeSet<T>,
|
||||
challenger_state_before: [T; SPONGE_WIDTH],
|
||||
challenger_state_after: [T; SPONGE_WIDTH],
|
||||
}
|
||||
|
||||
/// Similar to the unstable `Iterator::next_chunk`. Could be replaced with that when it's stable.
|
||||
fn next_chunk<T: Debug, const N: usize>(iter: &mut impl Iterator<Item = T>) -> [T; N] {
|
||||
(0..N)
|
||||
.flat_map(|_| iter.next())
|
||||
.collect_vec()
|
||||
.try_into()
|
||||
.expect("Not enough elements")
|
||||
}
|
||||
|
||||
impl<T: Copy + Eq + PartialEq + Debug> PublicInputs<T> {
|
||||
fn from_vec(v: &[T], config: &StarkConfig) -> Self {
|
||||
let mut iter = v.iter().copied();
|
||||
let trace_cap = (0..1 << config.fri_config.cap_height)
|
||||
.map(|_| next_chunk::<_, 4>(&mut iter).to_vec())
|
||||
.collect();
|
||||
let ctl_challenges = GrandProductChallengeSet {
|
||||
challenges: (0..config.num_challenges)
|
||||
.map(|_| GrandProductChallenge {
|
||||
beta: iter.next().unwrap(),
|
||||
gamma: iter.next().unwrap(),
|
||||
})
|
||||
.collect(),
|
||||
};
|
||||
let challenger_state_before = next_chunk(&mut iter);
|
||||
let challenger_state_after = next_chunk(&mut iter);
|
||||
let ctl_zs_last = iter.collect();
|
||||
|
||||
Self {
|
||||
trace_cap,
|
||||
ctl_zs_last,
|
||||
ctl_challenges,
|
||||
challenger_state_before,
|
||||
challenger_state_after,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<F: RichField + Extendable<D>, C: GenericConfig<D, F = F>, const D: usize>
|
||||
RecursiveAllProof<F, C, D>
|
||||
{
|
||||
/// Verify every recursive proof.
|
||||
pub fn verify(
|
||||
self,
|
||||
verifier_data: &[VerifierCircuitData<F, C, D>; NUM_TABLES],
|
||||
cross_table_lookups: Vec<CrossTableLookup<F>>,
|
||||
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].public_inputs, inner_config)
|
||||
});
|
||||
|
||||
let mut challenger = Challenger::<F, C::Hasher>::new();
|
||||
for pi in &pis {
|
||||
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);
|
||||
}
|
||||
|
||||
let state = challenger.compact();
|
||||
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| verifier_data[i].common.degree_bits);
|
||||
verify_cross_table_lookups::<F, C, D>(
|
||||
cross_table_lookups,
|
||||
pis.map(|p| p.ctl_zs_last),
|
||||
degrees_bits,
|
||||
ctl_challenges,
|
||||
inner_config,
|
||||
)?;
|
||||
|
||||
// Verify the proofs.
|
||||
for (proof, verifier_data) in self.recursive_proofs.into_iter().zip(verifier_data) {
|
||||
verifier_data.verify(proof)?;
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
|
||||
/// Recursively verify every recursive proof.
|
||||
pub fn verify_circuit(
|
||||
builder: &mut CircuitBuilder<F, D>,
|
||||
recursive_all_proof_target: RecursiveAllProofTargetWithData<D>,
|
||||
verifier_data: &[VerifierCircuitData<F, C, D>; NUM_TABLES],
|
||||
cross_table_lookups: Vec<CrossTableLookup<F>>,
|
||||
inner_config: &StarkConfig,
|
||||
) where
|
||||
[(); C::Hasher::HASH_SIZE]:,
|
||||
<C as GenericConfig<D>>::Hasher: AlgebraicHasher<F>,
|
||||
{
|
||||
let RecursiveAllProofTargetWithData {
|
||||
recursive_proofs,
|
||||
verifier_data: verifier_data_target,
|
||||
} = recursive_all_proof_target;
|
||||
let pis: [_; NUM_TABLES] = std::array::from_fn(|i| {
|
||||
PublicInputs::from_vec(&recursive_proofs[i].public_inputs, inner_config)
|
||||
});
|
||||
|
||||
let mut challenger = RecursiveChallenger::<F, C::Hasher, D>::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,
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
let state = challenger.compact(builder);
|
||||
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| verifier_data[i].common.degree_bits);
|
||||
verify_cross_table_lookups_circuit::<F, C, D>(
|
||||
builder,
|
||||
cross_table_lookups,
|
||||
pis.map(|p| p.ctl_zs_last),
|
||||
degrees_bits,
|
||||
ctl_challenges,
|
||||
inner_config,
|
||||
);
|
||||
for (i, (recursive_proof, verifier_data_target)) in recursive_proofs
|
||||
.into_iter()
|
||||
.zip(verifier_data_target)
|
||||
.enumerate()
|
||||
{
|
||||
builder.verify_proof(
|
||||
recursive_proof,
|
||||
&verifier_data_target,
|
||||
&verifier_data[i].common,
|
||||
);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// Returns the verifier data for the recursive Stark circuit.
|
||||
fn verifier_data_recursive_stark_proof<
|
||||
F: RichField + Extendable<D>,
|
||||
C: GenericConfig<D, F = F>,
|
||||
S: Stark<F, D>,
|
||||
const D: usize,
|
||||
>(
|
||||
table: Table,
|
||||
stark: S,
|
||||
degree_bits: usize,
|
||||
cross_table_lookups: &[CrossTableLookup<F>],
|
||||
inner_config: &StarkConfig,
|
||||
circuit_config: &CircuitConfig,
|
||||
) -> VerifierCircuitData<F, C, D>
|
||||
where
|
||||
[(); S::COLUMNS]:,
|
||||
[(); C::Hasher::HASH_SIZE]:,
|
||||
C::Hasher: AlgebraicHasher<F>,
|
||||
{
|
||||
let mut builder = CircuitBuilder::<F, D>::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::<Vec<_>>(),
|
||||
);
|
||||
|
||||
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::<F, C::Hasher, D>::from_state(challenger_state);
|
||||
let challenges = proof_target.get_challenges::<F, C>(
|
||||
&mut builder,
|
||||
&mut challenger,
|
||||
num_permutation_zs > 0,
|
||||
num_permutation_batch_size,
|
||||
inner_config,
|
||||
);
|
||||
let challenger_state = challenger.compact(&mut builder);
|
||||
builder.register_public_inputs(&challenger_state);
|
||||
|
||||
builder.register_public_inputs(&proof_target.openings.ctl_zs_last);
|
||||
|
||||
verify_stark_proof_with_challenges_circuit::<F, C, _, D>(
|
||||
&mut builder,
|
||||
&stark,
|
||||
&proof_target,
|
||||
&challenges,
|
||||
&ctl_vars,
|
||||
inner_config,
|
||||
);
|
||||
|
||||
builder.build_verifier::<C>()
|
||||
}
|
||||
|
||||
/// Returns the recursive Stark circuit verifier data for every Stark in `AllStark`.
|
||||
pub fn all_verifier_data_recursive_stark_proof<
|
||||
F: RichField + Extendable<D>,
|
||||
C: GenericConfig<D, F = F>,
|
||||
const D: usize,
|
||||
>(
|
||||
builder: &mut CircuitBuilder<F, D>,
|
||||
all_stark: AllStark<F, D>,
|
||||
all_proof: AllProofTarget<D>,
|
||||
all_stark: &AllStark<F, D>,
|
||||
degree_bits: [usize; NUM_TABLES],
|
||||
inner_config: &StarkConfig,
|
||||
) where
|
||||
circuit_config: &CircuitConfig,
|
||||
) -> [VerifierCircuitData<F, C, D>; NUM_TABLES]
|
||||
where
|
||||
[(); CpuStark::<F, D>::COLUMNS]:,
|
||||
[(); KeccakStark::<F, D>::COLUMNS]:,
|
||||
[(); KeccakMemoryStark::<F, D>::COLUMNS]:,
|
||||
[(); LogicStark::<F, D>::COLUMNS]:,
|
||||
[(); MemoryStark::<F, D>::COLUMNS]:,
|
||||
[(); C::Hasher::HASH_SIZE]:,
|
||||
C::Hasher: AlgebraicHasher<F>,
|
||||
{
|
||||
let AllProofChallengesTarget {
|
||||
stark_challenges,
|
||||
ctl_challenges,
|
||||
} = all_proof.get_challenges::<F, C>(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::<F, C, _, D>(
|
||||
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],
|
||||
[
|
||||
verifier_data_recursive_stark_proof(
|
||||
Table::Cpu,
|
||||
all_stark.cpu_stark,
|
||||
degree_bits[Table::Cpu as usize],
|
||||
&all_stark.cross_table_lookups,
|
||||
inner_config,
|
||||
)
|
||||
);
|
||||
with_context!(
|
||||
builder,
|
||||
"verify Keccak proof",
|
||||
verify_stark_proof_with_challenges_circuit::<F, C, _, D>(
|
||||
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],
|
||||
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,
|
||||
)
|
||||
);
|
||||
with_context!(
|
||||
builder,
|
||||
"verify Keccak memory proof",
|
||||
verify_stark_proof_with_challenges_circuit::<F, C, _, D>(
|
||||
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],
|
||||
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,
|
||||
)
|
||||
);
|
||||
with_context!(
|
||||
builder,
|
||||
"verify logic proof",
|
||||
verify_stark_proof_with_challenges_circuit::<F, C, _, D>(
|
||||
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],
|
||||
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,
|
||||
)
|
||||
);
|
||||
with_context!(
|
||||
builder,
|
||||
"verify memory proof",
|
||||
verify_stark_proof_with_challenges_circuit::<F, C, _, D>(
|
||||
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],
|
||||
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,
|
||||
)
|
||||
);
|
||||
|
||||
with_context!(
|
||||
builder,
|
||||
"verify cross-table lookups",
|
||||
verify_cross_table_lookups_circuit::<F, C, D>(
|
||||
builder,
|
||||
cross_table_lookups,
|
||||
&all_proof.stark_proofs,
|
||||
ctl_challenges,
|
||||
inner_config,
|
||||
)
|
||||
);
|
||||
circuit_config,
|
||||
),
|
||||
]
|
||||
}
|
||||
|
||||
/// Recursively verifies an inner proof.
|
||||
@ -156,7 +395,7 @@ fn verify_stark_proof_with_challenges_circuit<
|
||||
const D: usize,
|
||||
>(
|
||||
builder: &mut CircuitBuilder<F, D>,
|
||||
stark: S,
|
||||
stark: &S,
|
||||
proof: &StarkProofTarget<D>,
|
||||
challenges: &StarkProofChallengesTarget<D>,
|
||||
ctl_vars: &[CtlCheckVarsTarget<F, D>],
|
||||
@ -212,7 +451,7 @@ fn verify_stark_proof_with_challenges_circuit<
|
||||
"evaluate vanishing polynomial",
|
||||
eval_vanishing_poly_circuit::<F, C, S, D>(
|
||||
builder,
|
||||
&stark,
|
||||
stark,
|
||||
inner_config,
|
||||
vars,
|
||||
permutation_data,
|
||||
@ -286,35 +525,35 @@ pub fn add_virtual_all_proof<F: RichField + Extendable<D>, const D: usize>(
|
||||
let stark_proofs = [
|
||||
add_virtual_stark_proof(
|
||||
builder,
|
||||
all_stark.cpu_stark,
|
||||
&all_stark.cpu_stark,
|
||||
config,
|
||||
degree_bits[Table::Cpu as usize],
|
||||
nums_ctl_zs[Table::Cpu as usize],
|
||||
),
|
||||
add_virtual_stark_proof(
|
||||
builder,
|
||||
all_stark.keccak_stark,
|
||||
&all_stark.keccak_stark,
|
||||
config,
|
||||
degree_bits[Table::Keccak as usize],
|
||||
nums_ctl_zs[Table::Keccak as usize],
|
||||
),
|
||||
add_virtual_stark_proof(
|
||||
builder,
|
||||
all_stark.keccak_memory_stark,
|
||||
&all_stark.keccak_memory_stark,
|
||||
config,
|
||||
degree_bits[Table::KeccakMemory as usize],
|
||||
nums_ctl_zs[Table::KeccakMemory as usize],
|
||||
),
|
||||
add_virtual_stark_proof(
|
||||
builder,
|
||||
all_stark.logic_stark,
|
||||
&all_stark.logic_stark,
|
||||
config,
|
||||
degree_bits[Table::Logic as usize],
|
||||
nums_ctl_zs[Table::Logic as usize],
|
||||
),
|
||||
add_virtual_stark_proof(
|
||||
builder,
|
||||
all_stark.memory_stark,
|
||||
&all_stark.memory_stark,
|
||||
config,
|
||||
degree_bits[Table::Memory as usize],
|
||||
nums_ctl_zs[Table::Memory as usize],
|
||||
@ -328,6 +567,33 @@ pub fn add_virtual_all_proof<F: RichField + Extendable<D>, const D: usize>(
|
||||
}
|
||||
}
|
||||
|
||||
/// Returns `RecursiveAllProofTargetWithData` where the proofs targets are virtual and the
|
||||
/// verifier data targets are constants.
|
||||
pub fn add_virtual_recursive_all_proof<F: RichField + Extendable<D>, H, C, const D: usize>(
|
||||
builder: &mut CircuitBuilder<F, D>,
|
||||
verifier_data: &[VerifierCircuitData<F, C, D>; NUM_TABLES],
|
||||
) -> RecursiveAllProofTargetWithData<D>
|
||||
where
|
||||
H: Hasher<F, Hash = HashOut<F>>,
|
||||
C: GenericConfig<D, F = F, Hasher = H>,
|
||||
{
|
||||
let recursive_proofs = std::array::from_fn(|i| {
|
||||
let verifier_data = &verifier_data[i];
|
||||
builder.add_virtual_proof_with_pis(&verifier_data.common)
|
||||
});
|
||||
let verifier_data = std::array::from_fn(|i| {
|
||||
let verifier_data = &verifier_data[i];
|
||||
VerifierCircuitTarget {
|
||||
constants_sigmas_cap: builder
|
||||
.constant_merkle_cap(&verifier_data.verifier_only.constants_sigmas_cap),
|
||||
}
|
||||
});
|
||||
RecursiveAllProofTargetWithData {
|
||||
recursive_proofs,
|
||||
verifier_data,
|
||||
}
|
||||
}
|
||||
|
||||
pub fn add_virtual_public_values<F: RichField + Extendable<D>, const D: usize>(
|
||||
builder: &mut CircuitBuilder<F, D>,
|
||||
) -> PublicValuesTarget {
|
||||
@ -377,7 +643,7 @@ pub fn add_virtual_block_metadata<F: RichField + Extendable<D>, const D: usize>(
|
||||
|
||||
pub fn add_virtual_stark_proof<F: RichField + Extendable<D>, S: Stark<F, D>, const D: usize>(
|
||||
builder: &mut CircuitBuilder<F, D>,
|
||||
stark: S,
|
||||
stark: &S,
|
||||
config: &StarkConfig,
|
||||
degree_bits: usize,
|
||||
num_ctl_zs: usize,
|
||||
@ -397,14 +663,14 @@ pub fn add_virtual_stark_proof<F: RichField + Extendable<D>, S: Stark<F, D>, con
|
||||
trace_cap: builder.add_virtual_cap(cap_height),
|
||||
permutation_ctl_zs_cap: permutation_zs_cap,
|
||||
quotient_polys_cap: builder.add_virtual_cap(cap_height),
|
||||
openings: add_stark_opening_set::<F, S, D>(builder, stark, num_ctl_zs, config),
|
||||
openings: add_virtual_stark_opening_set::<F, S, D>(builder, stark, num_ctl_zs, config),
|
||||
opening_proof: builder.add_virtual_fri_proof(&num_leaves_per_oracle, &fri_params),
|
||||
}
|
||||
}
|
||||
|
||||
fn add_stark_opening_set<F: RichField + Extendable<D>, S: Stark<F, D>, const D: usize>(
|
||||
fn add_virtual_stark_opening_set<F: RichField + Extendable<D>, S: Stark<F, D>, const D: usize>(
|
||||
builder: &mut CircuitBuilder<F, D>,
|
||||
stark: S,
|
||||
stark: &S,
|
||||
num_ctl_zs: usize,
|
||||
config: &StarkConfig,
|
||||
) -> StarkOpeningSetTarget<D> {
|
||||
@ -422,6 +688,22 @@ fn add_stark_opening_set<F: RichField + Extendable<D>, S: Stark<F, D>, const D:
|
||||
}
|
||||
}
|
||||
|
||||
pub fn set_recursive_all_proof_target<F, C: GenericConfig<D, F = F>, W, const D: usize>(
|
||||
witness: &mut W,
|
||||
recursive_all_proof_target: &RecursiveAllProofTargetWithData<D>,
|
||||
all_proof: &RecursiveAllProof<F, C, D>,
|
||||
) where
|
||||
F: RichField + Extendable<D>,
|
||||
C::Hasher: AlgebraicHasher<F>,
|
||||
W: Witness<F>,
|
||||
{
|
||||
for i in 0..NUM_TABLES {
|
||||
witness.set_proof_with_pis_target(
|
||||
&recursive_all_proof_target.recursive_proofs[i],
|
||||
&all_proof.recursive_proofs[i],
|
||||
);
|
||||
}
|
||||
}
|
||||
pub fn set_all_proof_target<F, C: GenericConfig<D, F = F>, W, const D: usize>(
|
||||
witness: &mut W,
|
||||
all_proof_target: &AllProofTarget<D>,
|
||||
@ -556,3 +838,219 @@ pub fn set_block_metadata_target<F, W, const D: usize>(
|
||||
F::from_canonical_u64(block_metadata.block_base_fee.as_u64()),
|
||||
);
|
||||
}
|
||||
|
||||
#[cfg(test)]
|
||||
pub(crate) mod tests {
|
||||
use anyhow::Result;
|
||||
use plonky2::field::extension::Extendable;
|
||||
use plonky2::hash::hash_types::RichField;
|
||||
use plonky2::hash::hashing::SPONGE_WIDTH;
|
||||
use plonky2::iop::challenger::RecursiveChallenger;
|
||||
use plonky2::iop::witness::{PartialWitness, Witness};
|
||||
use plonky2::plonk::circuit_builder::CircuitBuilder;
|
||||
use plonky2::plonk::circuit_data::{CircuitConfig, VerifierCircuitData};
|
||||
use plonky2::plonk::config::Hasher;
|
||||
use plonky2::plonk::config::{AlgebraicHasher, GenericConfig};
|
||||
use plonky2::plonk::proof::ProofWithPublicInputs;
|
||||
|
||||
use crate::all_stark::{AllStark, Table};
|
||||
use crate::config::StarkConfig;
|
||||
use crate::cpu::cpu_stark::CpuStark;
|
||||
use crate::cross_table_lookup::{CrossTableLookup, CtlCheckVarsTarget};
|
||||
use crate::keccak::keccak_stark::KeccakStark;
|
||||
use crate::keccak_memory::keccak_memory_stark::KeccakMemoryStark;
|
||||
use crate::logic::LogicStark;
|
||||
use crate::memory::memory_stark::MemoryStark;
|
||||
use crate::permutation::{GrandProductChallenge, GrandProductChallengeSet};
|
||||
use crate::proof::{AllChallengerState, AllProof, StarkProof};
|
||||
use crate::recursive_verifier::{
|
||||
add_virtual_stark_proof, set_stark_proof_target,
|
||||
verify_stark_proof_with_challenges_circuit, RecursiveAllProof,
|
||||
};
|
||||
use crate::stark::Stark;
|
||||
|
||||
/// Recursively verify a Stark proof.
|
||||
/// Outputs the recursive proof and the associated verifier data.
|
||||
fn recursively_verify_stark_proof<
|
||||
F: RichField + Extendable<D>,
|
||||
C: GenericConfig<D, F = F>,
|
||||
S: Stark<F, D>,
|
||||
const D: usize,
|
||||
>(
|
||||
table: Table,
|
||||
stark: S,
|
||||
proof: &StarkProof<F, C, D>,
|
||||
cross_table_lookups: &[CrossTableLookup<F>],
|
||||
ctl_challenges: &GrandProductChallengeSet<F>,
|
||||
challenger_state_before_vals: [F; SPONGE_WIDTH],
|
||||
inner_config: &StarkConfig,
|
||||
circuit_config: &CircuitConfig,
|
||||
) -> Result<(ProofWithPublicInputs<F, C, D>, VerifierCircuitData<F, C, D>)>
|
||||
where
|
||||
[(); S::COLUMNS]:,
|
||||
[(); C::Hasher::HASH_SIZE]:,
|
||||
C::Hasher: AlgebraicHasher<F>,
|
||||
{
|
||||
let mut builder = CircuitBuilder::<F, D>::new(circuit_config.clone());
|
||||
let mut pw = PartialWitness::new();
|
||||
|
||||
let num_permutation_zs = stark.num_permutation_batches(inner_config);
|
||||
let num_permutation_batch_size = stark.permutation_batch_size();
|
||||
let proof_target = add_virtual_stark_proof(
|
||||
&mut builder,
|
||||
&stark,
|
||||
inner_config,
|
||||
proof.recover_degree_bits(inner_config),
|
||||
proof.num_ctl_zs(),
|
||||
);
|
||||
set_stark_proof_target(&mut pw, &proof_target, proof, builder.zero());
|
||||
builder.register_public_inputs(
|
||||
&proof_target
|
||||
.trace_cap
|
||||
.0
|
||||
.iter()
|
||||
.flat_map(|h| h.elements)
|
||||
.collect::<Vec<_>>(),
|
||||
);
|
||||
|
||||
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(),
|
||||
};
|
||||
for i in 0..inner_config.num_challenges {
|
||||
pw.set_target(
|
||||
ctl_challenges_target.challenges[i].beta,
|
||||
ctl_challenges.challenges[i].beta,
|
||||
);
|
||||
pw.set_target(
|
||||
ctl_challenges_target.challenges[i].gamma,
|
||||
ctl_challenges.challenges[i].gamma,
|
||||
);
|
||||
}
|
||||
|
||||
let ctl_vars = CtlCheckVarsTarget::from_proof(
|
||||
table,
|
||||
&proof_target,
|
||||
cross_table_lookups,
|
||||
&ctl_challenges_target,
|
||||
num_permutation_zs,
|
||||
);
|
||||
|
||||
let challenger_state_before = std::array::from_fn(|_| builder.add_virtual_public_input());
|
||||
pw.set_target_arr(challenger_state_before, challenger_state_before_vals);
|
||||
let mut challenger =
|
||||
RecursiveChallenger::<F, C::Hasher, D>::from_state(challenger_state_before);
|
||||
let challenges = proof_target.get_challenges::<F, C>(
|
||||
&mut builder,
|
||||
&mut challenger,
|
||||
num_permutation_zs > 0,
|
||||
num_permutation_batch_size,
|
||||
inner_config,
|
||||
);
|
||||
let challenger_state_after = challenger.compact(&mut builder);
|
||||
builder.register_public_inputs(&challenger_state_after);
|
||||
|
||||
builder.register_public_inputs(&proof_target.openings.ctl_zs_last);
|
||||
|
||||
verify_stark_proof_with_challenges_circuit::<F, C, _, D>(
|
||||
&mut builder,
|
||||
&stark,
|
||||
&proof_target,
|
||||
&challenges,
|
||||
&ctl_vars,
|
||||
inner_config,
|
||||
);
|
||||
|
||||
let data = builder.build::<C>();
|
||||
Ok((data.prove(pw)?, data.verifier_data()))
|
||||
}
|
||||
|
||||
/// Recursively verify every Stark proof in an `AllProof`.
|
||||
pub fn recursively_verify_all_proof<
|
||||
F: RichField + Extendable<D>,
|
||||
C: GenericConfig<D, F = F>,
|
||||
const D: usize,
|
||||
>(
|
||||
all_stark: &AllStark<F, D>,
|
||||
all_proof: &AllProof<F, C, D>,
|
||||
inner_config: &StarkConfig,
|
||||
circuit_config: &CircuitConfig,
|
||||
) -> Result<RecursiveAllProof<F, C, D>>
|
||||
where
|
||||
[(); CpuStark::<F, D>::COLUMNS]:,
|
||||
[(); KeccakStark::<F, D>::COLUMNS]:,
|
||||
[(); KeccakMemoryStark::<F, D>::COLUMNS]:,
|
||||
[(); LogicStark::<F, D>::COLUMNS]:,
|
||||
[(); MemoryStark::<F, D>::COLUMNS]:,
|
||||
[(); C::Hasher::HASH_SIZE]:,
|
||||
C::Hasher: AlgebraicHasher<F>,
|
||||
{
|
||||
let AllChallengerState {
|
||||
states,
|
||||
ctl_challenges,
|
||||
} = all_proof.get_challenger_states(all_stark, inner_config);
|
||||
Ok(RecursiveAllProof {
|
||||
recursive_proofs: [
|
||||
recursively_verify_stark_proof(
|
||||
Table::Cpu,
|
||||
all_stark.cpu_stark,
|
||||
&all_proof.stark_proofs[Table::Cpu as usize],
|
||||
&all_stark.cross_table_lookups,
|
||||
&ctl_challenges,
|
||||
states[0],
|
||||
inner_config,
|
||||
circuit_config,
|
||||
)?
|
||||
.0,
|
||||
recursively_verify_stark_proof(
|
||||
Table::Keccak,
|
||||
all_stark.keccak_stark,
|
||||
&all_proof.stark_proofs[Table::Keccak as usize],
|
||||
&all_stark.cross_table_lookups,
|
||||
&ctl_challenges,
|
||||
states[1],
|
||||
inner_config,
|
||||
circuit_config,
|
||||
)?
|
||||
.0,
|
||||
recursively_verify_stark_proof(
|
||||
Table::KeccakMemory,
|
||||
all_stark.keccak_memory_stark,
|
||||
&all_proof.stark_proofs[Table::KeccakMemory as usize],
|
||||
&all_stark.cross_table_lookups,
|
||||
&ctl_challenges,
|
||||
states[2],
|
||||
inner_config,
|
||||
circuit_config,
|
||||
)?
|
||||
.0,
|
||||
recursively_verify_stark_proof(
|
||||
Table::Logic,
|
||||
all_stark.logic_stark,
|
||||
&all_proof.stark_proofs[Table::Logic as usize],
|
||||
&all_stark.cross_table_lookups,
|
||||
&ctl_challenges,
|
||||
states[3],
|
||||
inner_config,
|
||||
circuit_config,
|
||||
)?
|
||||
.0,
|
||||
recursively_verify_stark_proof(
|
||||
Table::Memory,
|
||||
all_stark.memory_stark,
|
||||
&all_proof.stark_proofs[Table::Memory as usize],
|
||||
&all_stark.cross_table_lookups,
|
||||
&ctl_challenges,
|
||||
states[4],
|
||||
inner_config,
|
||||
circuit_config,
|
||||
)?
|
||||
.0,
|
||||
],
|
||||
})
|
||||
}
|
||||
}
|
||||
|
||||
@ -95,9 +95,12 @@ where
|
||||
config,
|
||||
)?;
|
||||
|
||||
verify_cross_table_lookups(
|
||||
let degrees_bits =
|
||||
std::array::from_fn(|i| all_proof.stark_proofs[i].recover_degree_bits(config));
|
||||
verify_cross_table_lookups::<F, C, D>(
|
||||
cross_table_lookups,
|
||||
&all_proof.stark_proofs,
|
||||
all_proof.stark_proofs.map(|p| p.openings.ctl_zs_last),
|
||||
degrees_bits,
|
||||
ctl_challenges,
|
||||
config,
|
||||
)
|
||||
|
||||
@ -46,6 +46,10 @@ impl FriConfig {
|
||||
reduction_arity_bits,
|
||||
}
|
||||
}
|
||||
|
||||
pub fn num_cap_elements(&self) -> usize {
|
||||
1 << self.cap_height
|
||||
}
|
||||
}
|
||||
|
||||
/// FRI parameters, including generated parameters which are specific to an instance size, in
|
||||
|
||||
@ -146,6 +146,14 @@ impl<F: RichField, H: Hasher<F>> Challenger<F, H> {
|
||||
self.output_buffer
|
||||
.extend_from_slice(&self.sponge_state[0..SPONGE_RATE]);
|
||||
}
|
||||
|
||||
pub fn compact(&mut self) -> [F; SPONGE_WIDTH] {
|
||||
if !self.input_buffer.is_empty() {
|
||||
self.duplexing();
|
||||
}
|
||||
self.output_buffer.clear();
|
||||
self.sponge_state
|
||||
}
|
||||
}
|
||||
|
||||
impl<F: RichField, H: AlgebraicHasher<F>> Default for Challenger<F, H> {
|
||||
@ -176,6 +184,14 @@ impl<F: RichField + Extendable<D>, H: AlgebraicHasher<F>, const D: usize>
|
||||
}
|
||||
}
|
||||
|
||||
pub fn from_state(sponge_state: [Target; SPONGE_WIDTH]) -> Self {
|
||||
RecursiveChallenger {
|
||||
sponge_state,
|
||||
input_buffer: vec![],
|
||||
output_buffer: vec![],
|
||||
}
|
||||
}
|
||||
|
||||
pub(crate) fn observe_element(&mut self, target: Target) {
|
||||
// Any buffered outputs are now invalid, since they wouldn't reflect this input.
|
||||
self.output_buffer.clear();
|
||||
@ -183,7 +199,7 @@ impl<F: RichField + Extendable<D>, H: AlgebraicHasher<F>, 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);
|
||||
}
|
||||
@ -272,6 +288,12 @@ impl<F: RichField + Extendable<D>, H: AlgebraicHasher<F>, const D: usize>
|
||||
|
||||
self.input_buffer.clear();
|
||||
}
|
||||
|
||||
pub fn compact(&mut self, builder: &mut CircuitBuilder<F, D>) -> [Target; SPONGE_WIDTH] {
|
||||
self.absorb_buffered_inputs(builder);
|
||||
self.output_buffer.clear();
|
||||
self.sponge_state
|
||||
}
|
||||
}
|
||||
|
||||
#[cfg(test)]
|
||||
|
||||
@ -23,8 +23,9 @@ use crate::gates::gate::{CurrentSlot, Gate, GateInstance, GateRef};
|
||||
use crate::gates::noop::NoopGate;
|
||||
use crate::gates::public_input::PublicInputGate;
|
||||
use crate::gates::selectors::selector_polynomials;
|
||||
use crate::hash::hash_types::{HashOutTarget, MerkleCapTarget, RichField};
|
||||
use crate::hash::hash_types::{HashOut, HashOutTarget, MerkleCapTarget, RichField};
|
||||
use crate::hash::merkle_proofs::MerkleProofTarget;
|
||||
use crate::hash::merkle_tree::MerkleCap;
|
||||
use crate::iop::ext_target::ExtensionTarget;
|
||||
use crate::iop::generator::{
|
||||
ConstantGenerator, CopyGenerator, RandomValueGenerator, SimpleGenerator, WitnessGenerator,
|
||||
@ -208,6 +209,13 @@ impl<F: RichField + Extendable<D>, const D: usize> CircuitBuilder<F, D> {
|
||||
b
|
||||
}
|
||||
|
||||
/// Add a virtual target and register it as a public input.
|
||||
pub fn add_virtual_public_input(&mut self) -> Target {
|
||||
let t = self.add_virtual_target();
|
||||
self.register_public_input(t);
|
||||
t
|
||||
}
|
||||
|
||||
/// Adds a gate to the circuit, and returns its index.
|
||||
pub fn add_gate<G: Gate<F, D>>(&mut self, gate_type: G, mut constants: Vec<F>) -> usize {
|
||||
self.check_gate_compatibility(&gate_type);
|
||||
@ -361,6 +369,19 @@ impl<F: RichField + Extendable<D>, const D: usize> CircuitBuilder<F, D> {
|
||||
}
|
||||
}
|
||||
|
||||
pub fn constant_hash(&mut self, h: HashOut<F>) -> HashOutTarget {
|
||||
HashOutTarget {
|
||||
elements: h.elements.map(|x| self.constant(x)),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn constant_merkle_cap<H: Hasher<F, Hash = HashOut<F>>>(
|
||||
&mut self,
|
||||
cap: &MerkleCap<F, H>,
|
||||
) -> MerkleCapTarget {
|
||||
MerkleCapTarget(cap.0.iter().map(|h| self.constant_hash(*h)).collect())
|
||||
}
|
||||
|
||||
/// If the given target is a constant (i.e. it was created by the `constant(F)` method), returns
|
||||
/// its constant value. Otherwise, returns `None`.
|
||||
pub fn target_as_constant(&self, target: Target) -> Option<F> {
|
||||
@ -835,15 +856,8 @@ impl<F: RichField + Extendable<D>, const D: usize> CircuitBuilder<F, D> {
|
||||
[(); C::Hasher::HASH_SIZE]:,
|
||||
{
|
||||
// TODO: Can skip parts of this.
|
||||
let CircuitData {
|
||||
prover_only,
|
||||
common,
|
||||
..
|
||||
} = self.build();
|
||||
ProverCircuitData {
|
||||
prover_only,
|
||||
common,
|
||||
}
|
||||
let circuit_data = self.build();
|
||||
circuit_data.prover_data()
|
||||
}
|
||||
|
||||
/// Builds a "verifier circuit", with data needed to verify proofs but not generate them.
|
||||
@ -852,14 +866,7 @@ impl<F: RichField + Extendable<D>, const D: usize> CircuitBuilder<F, D> {
|
||||
[(); C::Hasher::HASH_SIZE]:,
|
||||
{
|
||||
// TODO: Can skip parts of this.
|
||||
let CircuitData {
|
||||
verifier_only,
|
||||
common,
|
||||
..
|
||||
} = self.build();
|
||||
VerifierCircuitData {
|
||||
verifier_only,
|
||||
common,
|
||||
}
|
||||
let circuit_data = self.build();
|
||||
circuit_data.verifier_data()
|
||||
}
|
||||
}
|
||||
|
||||
@ -140,6 +140,30 @@ impl<F: RichField + Extendable<D>, C: GenericConfig<D, F = F>, const D: usize>
|
||||
{
|
||||
compressed_proof_with_pis.verify(&self.verifier_only, &self.common)
|
||||
}
|
||||
|
||||
pub fn verifier_data(self) -> VerifierCircuitData<F, C, D> {
|
||||
let CircuitData {
|
||||
verifier_only,
|
||||
common,
|
||||
..
|
||||
} = self;
|
||||
VerifierCircuitData {
|
||||
verifier_only,
|
||||
common,
|
||||
}
|
||||
}
|
||||
|
||||
pub fn prover_data(self) -> ProverCircuitData<F, C, D> {
|
||||
let CircuitData {
|
||||
prover_only,
|
||||
common,
|
||||
..
|
||||
} = self;
|
||||
ProverCircuitData {
|
||||
prover_only,
|
||||
common,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// Circuit data required by the prover. This may be thought of as a proving key, although it
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user