Skip to content

Commit

Permalink
Update the root circuit to conditionally verify Keccak proofs (#652)
Browse files Browse the repository at this point in the history 
* refactoring

* fix clippy

* fix clippy

* wip

* wip

* wip

* cleanup

* prove one segment

* polish the code

* cleanup

* Revert "cleanup"

This reverts commit f63363b.

* add [ignore]

* add challenger state check

* add more checks

* cleanup

* fix

* polish the comments

* update tests

* fix ci

* fix ci

* fix ci

* empty payload and no keccak op check

* refactor

* Update evm_arithmetization/src/fixed_recursive_verifier.rs

Co-authored-by: Robin Salen <30937548+Nashtare@users.noreply.github.com>

* Update evm_arithmetization/src/fixed_recursive_verifier.rs

Co-authored-by: Robin Salen <30937548+Nashtare@users.noreply.github.com>

* empty payload and no keccak op check

* fmt

* fix test

* fix ci error with "cdk_erigon"

---------

Co-authored-by: Robin Salen <30937548+Nashtare@users.noreply.github.com>
  • Loading branch information
@sai-deng @Nashtare
sai-deng and Nashtare authored Oct 7, 2024
1 parent c39341d commit 1816253
Show file tree
Hide file tree
Showing 3 changed files with 107 additions and 21 deletions.
4 changes: 4 additions & 0 deletions evm_arithmetization/src/all_stark.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -106,6 +106,10 @@ pub const NUM_TABLES: usize = if cfg!(feature = "cdk_erigon") {
Table::MemAfter as usize + 1
};

/// Indices of Keccak Tables
pub const KECCAK_TABLES_INDICES: [usize; 2] =
[Table::Keccak as usize, Table::KeccakSponge as usize];

impl Table {
/// Returns all STARK table indices.
pub(crate) const fn all() -> [Self; NUM_TABLES] {
Expand Down
120 changes: 99 additions & 21 deletions evm_arithmetization/src/fixed_recursive_verifier.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,9 @@ use starky::lookup::{get_grand_product_challenge_set_target, GrandProductChallen
use starky::proof::StarkProofWithMetadata;
use starky::stark::Stark;

use crate::all_stark::{all_cross_table_lookups, AllStark, Table, NUM_TABLES};
use crate::all_stark::{
all_cross_table_lookups, AllStark, Table, KECCAK_TABLES_INDICES, NUM_TABLES,
};
use crate::cpu::kernel::aggregator::KERNEL;
use crate::generation::segments::{GenerationSegmentData, SegmentDataIterator};
use crate::generation::{GenerationInputs, TrimmedGenerationInputs};
Expand Down Expand Up @@ -151,6 +153,8 @@ where
/// for EVM root proofs; the circuit has them just to match the
/// structure of aggregation proofs.
cyclic_vk: VerifierCircuitTarget,
/// We can skip verifying Keccak tables when they are not in use.
use_keccak_tables: BoolTarget,
}

impl<F, C, const D: usize> RootCircuitData<F, C, D>
Expand All @@ -173,6 +177,7 @@ where
}
self.public_values.to_buffer(buffer)?;
buffer.write_target_verifier_circuit(&self.cyclic_vk)?;
buffer.write_target_bool(self.use_keccak_tables)?;
Ok(())
}

Expand All @@ -192,13 +197,15 @@ where
}
let public_values = PublicValuesTarget::from_buffer(buffer)?;
let cyclic_vk = buffer.read_target_verifier_circuit()?;
let use_keccak_tables = buffer.read_target_bool()?;

Ok(Self {
circuit,
proof_with_pis: proof_with_pis.try_into().unwrap(),
index_verifier_data: index_verifier_data.try_into().unwrap(),
public_values,
cyclic_vk,
use_keccak_tables,
})
}
}
Expand Down Expand Up @@ -807,6 +814,8 @@ where

let mut builder = CircuitBuilder::new(CircuitConfig::standard_recursion_config());

let use_keccak_tables = builder.add_virtual_bool_target_safe();
let skip_keccak_tables = builder.not(use_keccak_tables);
let public_values = add_virtual_public_values_public_input(&mut builder);

let recursive_proofs =
Expand All @@ -826,6 +835,16 @@ where
}
}

// Ensures that the trace cap is set to 0 when skipping Keccak tables.
for i in KECCAK_TABLES_INDICES {
for h in &pis[i].trace_cap {
for t in h {
let trace_cap_check = builder.mul(skip_keccak_tables.target, *t);
builder.assert_zero(trace_cap_check);
}
}
}

observe_public_values_target::<F, C, D>(&mut challenger, &public_values);

let ctl_challenges = get_grand_product_challenge_set_target(
Expand All @@ -834,16 +853,31 @@ where
stark_config.num_challenges,
);
// Check that the correct CTL challenges are used in every proof.
for pi in &pis {
for i in 0..stark_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,
);
for (i, pi) in pis.iter().enumerate() {
for j in 0..stark_config.num_challenges {
if KECCAK_TABLES_INDICES.contains(&i) {
// Ensures that the correct CTL challenges are used in Keccak tables when
// `enable_keccak_tables` is true.
builder.conditional_assert_eq(
use_keccak_tables.target,
ctl_challenges.challenges[j].beta,
pi.ctl_challenges.challenges[j].beta,
);
builder.conditional_assert_eq(
use_keccak_tables.target,
ctl_challenges.challenges[j].gamma,
pi.ctl_challenges.challenges[j].gamma,
);
} else {
builder.connect(
ctl_challenges.challenges[j].beta,
pi.ctl_challenges.challenges[j].beta,
);
builder.connect(
ctl_challenges.challenges[j].gamma,
pi.ctl_challenges.challenges[j].gamma,
);
}
}
}

Expand All @@ -852,12 +886,28 @@ where
builder.connect(before, s);
}
// Check that the challenger state is consistent between proofs.
let mut prev_state = pis[0].challenger_state_after.as_ref().to_vec();
let state_len = prev_state.len();
for i in 1..NUM_TABLES {
for (&before, &after) in zip_eq(
pis[i].challenger_state_before.as_ref(),
pis[i - 1].challenger_state_after.as_ref(),
) {
builder.connect(before, after);
let current_state_before = pis[i].challenger_state_before.as_ref();
let current_state_after = pis[i].challenger_state_after.as_ref();
for j in 0..state_len {
if KECCAK_TABLES_INDICES.contains(&i) {
// Ensure the challenger state:
// 1) prev == current_before when using Keccak
builder.conditional_assert_eq(
use_keccak_tables.target,
prev_state[j],
current_state_before[j],
);
// 2) Update prev <- current_after when using Keccak
// 3) Keep prev <- prev when skipping Keccak
prev_state[j] =
builder.select(use_keccak_tables, current_state_after[j], prev_state[j]);
} else {
builder.connect(prev_state[j], current_state_before[j]);
prev_state[j] = current_state_after[j];
}
}
}

Expand All @@ -877,6 +927,15 @@ where
})
.collect_vec();

// Ensure that when Keccak tables are skipped, the Keccak tables' ctl_zs_first
// are all zeros.
for &i in KECCAK_TABLES_INDICES.iter() {
for &t in pis[i].ctl_zs_first.iter() {
let ctl_check = builder.mul(skip_keccak_tables.target, t);
builder.assert_zero(ctl_check);
}
}

// Verify the CTL checks.
verify_cross_table_lookups_circuit::<F, D, NUM_TABLES>(
&mut builder,
Expand Down Expand Up @@ -906,11 +965,22 @@ where
let inner_verifier_data =
builder.random_access_verifier_data(index_verifier_data[i], possible_vks);

builder.verify_proof::<C>(
&recursive_proofs[i],
&inner_verifier_data,
inner_common_data[i],
);
if KECCAK_TABLES_INDICES.contains(&i) {
builder
.conditionally_verify_proof_or_dummy::<C>(
use_keccak_tables,
&recursive_proofs[i],
&inner_verifier_data,
inner_common_data[i],
)
.expect("Unable conditionally verify Keccak proofs in the root circuit");
} else {
builder.verify_proof::<C>(
&recursive_proofs[i],
&inner_verifier_data,
inner_common_data[i],
);
}
}

let merkle_before =
Expand Down Expand Up @@ -941,6 +1011,7 @@ where
index_verifier_data,
public_values,
cyclic_vk,
use_keccak_tables,
}
}

Expand Down Expand Up @@ -1841,6 +1912,7 @@ where
timing,
abort_signal.clone(),
)?;

let mut root_inputs = PartialWitness::new();

for table in 0..NUM_TABLES {
Expand Down Expand Up @@ -1886,6 +1958,9 @@ where
anyhow::Error::msg("Invalid conversion when setting public values targets.")
})?;

// TODO(sdeng): Set to false when this segment contains no Keccak operations.
root_inputs.set_bool_target(self.root.use_keccak_tables, true);

let root_proof = self.root.circuit.prove(root_inputs)?;

Ok(ProverOutputData {
Expand Down Expand Up @@ -1986,6 +2061,9 @@ where
anyhow::Error::msg("Invalid conversion when setting public values targets.")
})?;

// TODO(sdeng): Set to false when this segment contains no Keccak operations.
root_inputs.set_bool_target(self.root.use_keccak_tables, true);

let root_proof = self.root.circuit.prove(root_inputs)?;

Ok(ProofWithPublicValues {
Expand Down
4 changes: 4 additions & 0 deletions evm_arithmetization/src/recursive_verifier.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ use core::fmt::Debug;
use anyhow::Result;
use ethereum_types::{BigEndianHash, U256};
use plonky2::field::extension::Extendable;
use plonky2::gates::constant::ConstantGate;
use plonky2::gates::exponentiation::ExponentiationGate;
use plonky2::gates::gate::GateRef;
use plonky2::gates::noop::NoopGate;
Expand Down Expand Up @@ -326,6 +327,9 @@ pub(crate) fn add_common_recursion_gates<F: RichField + Extendable<D>, const D:
builder.add_gate_to_gate_set(GateRef::new(ExponentiationGate::new_from_config(
&builder.config,
)));
builder.add_gate_to_gate_set(GateRef::new(ConstantGate::new(
builder.config.num_constants,
)));
}

/// Recursive version of `get_memory_extra_looking_sum`.
Expand Down

0 comments on commit 1816253

Please sign in to comment.