Skip to content

Commit

Permalink
add auxilery memory address verification (#418)
Browse files Browse the repository at this point in the history
  • Loading branch information
ohad-starkware authored Feb 4, 2025
1 parent 538afee commit aad7b33
Show file tree
Hide file tree
Showing 3 changed files with 28 additions and 15 deletions.
16 changes: 14 additions & 2 deletions stwo_cairo_prover/crates/prover/src/cairo_air/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,8 @@ use stwo_prover::core::prover::{prove, verify, ProvingError, VerificationError};
use thiserror::Error;
use tracing::{span, Level};

use crate::components::memory::LOG_MEMORY_ADDRESS_BOUND;
use crate::components::memory_address_to_id::component::MEMORY_ADDRESS_TO_ID_SPLIT;
use crate::input::ProverInput;

// TODO(Ohad): decide dynamically.
Expand Down Expand Up @@ -126,8 +128,15 @@ pub fn verify_cairo<MC: MerkleChannel>(
stark_proof,
}: CairoProof<MC::H>,
) -> Result<(), CairoVerificationError> {
// Verify.
// TODO(Ohad): Propogate config from CLI args.
// Auxiliary verifications.
// Assert that ADDRESS->ID component does not overflow.
assert!(
(1 << claim.memory_address_to_id.log_size) * MEMORY_ADDRESS_TO_ID_SPLIT
<= (1 << LOG_MEMORY_ADDRESS_BOUND)
);

// Setup STARK protocol.
// TODO(Ohad): Propagate config from CLI args.
let config = PcsConfig {
pow_bits: 0,
fri_config: FriConfig {
Expand All @@ -147,6 +156,8 @@ pub fn verify_cairo<MC: MerkleChannel>(
claim.mix_into(channel);
commitment_scheme_verifier.commit(stark_proof.commitments[1], &log_sizes[1], channel);
let interaction_elements = CairoInteractionElements::draw(channel);

// Verify lookup argument.
if lookup_sum(&claim, &interaction_elements, &interaction_claim) != SecureField::zero() {
return Err(CairoVerificationError::InvalidLogupSum);
}
Expand All @@ -157,6 +168,7 @@ pub fn verify_cairo<MC: MerkleChannel>(
CairoComponents::new(&claim, &interaction_elements, &interaction_claim);
let components = component_generator.components();

// Verify stark.
verify(
&components,
channel,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -15,19 +15,20 @@ use crate::relations;
/// Split the (ID , Multiplicity) columns to shorter chunks. This is done to improve the performance
/// during The merkle commitment and FRI, as this component is usually the tallest in the Cairo AIR.
///
/// 1. The ID and Multiplicity vectors are split to 'N_SPLIT_CHUNKS' chunks of size
/// `ids.len()`/`N_SPLIT_CHUNKS`.
/// 1. The ID and Multiplicity vectors are split to 'MEMORY_ADDRESS_TO_ID_SPLIT' chunks of size
/// `ids.len()`/`MEMORY_ADDRESS_TO_ID_SPLIT`.
/// 2. The chunks are padded with 0s to the next power of 2.
///
/// # Example
/// ID = [id0..id10], N_SPLIT_CHUNKS = 4:
/// ID = [id0..id10], MEMORY_ADDRESS_TO_ID_SPLIT = 4:
/// ID0 = [id0, id1, id2, 0]
/// ID1 = [id3, id4, id5, 0]
/// ID2 = [id6, id7, id8, 0]
/// ID3 = [id9, id10, 0, 0]
pub(super) const N_SPLIT_CHUNKS: usize = 8;
pub const MEMORY_ADDRESS_TO_ID_SPLIT: usize = 8;
pub(super) const N_ID_AND_MULT_COLUMNS_PER_CHUNK: usize = 2;
pub(super) const N_TRACE_COLUMNS: usize = N_SPLIT_CHUNKS * N_ID_AND_MULT_COLUMNS_PER_CHUNK;
pub(super) const N_TRACE_COLUMNS: usize =
MEMORY_ADDRESS_TO_ID_SPLIT * N_ID_AND_MULT_COLUMNS_PER_CHUNK;

pub type Component = FrameworkComponent<Eval>;

Expand Down Expand Up @@ -63,7 +64,7 @@ impl FrameworkEval for Eval {
// Addresses are offseted by 1, as 0 address is reserved.
let seq_plus_one =
eval.get_preprocessed_column(Seq::new(self.log_size()).id()) + E::F::from(M31(1));
for i in 0..N_SPLIT_CHUNKS {
for i in 0..MEMORY_ADDRESS_TO_ID_SPLIT {
let id = eval.next_trace_mask();
let multiplicity = eval.next_trace_mask();
let address =
Expand All @@ -89,7 +90,7 @@ impl Claim {
let preprocessed_log_sizes = vec![self.log_size];
let trace_log_sizes = vec![self.log_size; N_TRACE_COLUMNS];
let interaction_log_sizes =
vec![self.log_size; SECURE_EXTENSION_DEGREE * N_SPLIT_CHUNKS.div_ceil(2)];
vec![self.log_size; SECURE_EXTENSION_DEGREE * MEMORY_ADDRESS_TO_ID_SPLIT.div_ceil(2)];
TreeVec::new(vec![
preprocessed_log_sizes,
trace_log_sizes,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ use stwo_prover::core::pcs::TreeBuilder;
use stwo_prover::core::poly::circle::{CanonicCoset, CircleEvaluation};
use stwo_prover::core::poly::BitReversedOrder;

use super::component::{Claim, InteractionClaim, N_SPLIT_CHUNKS};
use super::component::{Claim, InteractionClaim, MEMORY_ADDRESS_TO_ID_SPLIT};
use crate::cairo_air::preprocessed::Seq;
use crate::components::memory_address_to_id::component::{
N_ID_AND_MULT_COLUMNS_PER_CHUNK, N_TRACE_COLUMNS,
Expand Down Expand Up @@ -121,7 +121,7 @@ impl ClaimGenerator {
SimdBackend: BackendForChannel<MC>,
{
let size = std::cmp::max(
(self.address_to_raw_id.len() / N_SPLIT_CHUNKS).next_power_of_two(),
(self.address_to_raw_id.len() / MEMORY_ADDRESS_TO_ID_SPLIT).next_power_of_two(),
N_LANES,
);
let n_packed_rows = size.div_ceil(N_LANES);
Expand All @@ -146,9 +146,9 @@ impl ClaimGenerator {
}

// Lookup data.
let ids: [_; N_SPLIT_CHUNKS] =
let ids: [_; MEMORY_ADDRESS_TO_ID_SPLIT] =
std::array::from_fn(|i| trace[i * N_ID_AND_MULT_COLUMNS_PER_CHUNK].data.clone());
let multiplicities: [_; N_SPLIT_CHUNKS] =
let multiplicities: [_; MEMORY_ADDRESS_TO_ID_SPLIT] =
std::array::from_fn(|i| trace[1 + i * N_ID_AND_MULT_COLUMNS_PER_CHUNK].data.clone());

// Commit on trace.
Expand All @@ -173,8 +173,8 @@ impl ClaimGenerator {
}

pub struct InteractionClaimGenerator {
pub ids: [Vec<PackedM31>; N_SPLIT_CHUNKS],
pub multiplicities: [Vec<PackedM31>; N_SPLIT_CHUNKS],
pub ids: [Vec<PackedM31>; MEMORY_ADDRESS_TO_ID_SPLIT],
pub multiplicities: [Vec<PackedM31>; MEMORY_ADDRESS_TO_ID_SPLIT],
}
impl InteractionClaimGenerator {
pub fn write_interaction_trace<MC: MerkleChannel>(
Expand Down

0 comments on commit aad7b33

Please sign in to comment.