Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions crates/circuit_params/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ circuit-registry.workspace = true
leaf-prover.workspace = true

cairo-air.workspace = true
cairo-program-runner-lib.workspace = true
circuit-cairo-verifier.workspace = true
circuits-stark-verifier.workspace = true
circuit-common = { workspace = true, features = ["prover"] }
Expand Down
72 changes: 54 additions & 18 deletions crates/circuit_params/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,11 +12,12 @@
//! the multiverifier circuit once (for the largest trace size), all padded to those targets.

use std::collections::BTreeMap;
use std::path::PathBuf;
use std::path::{Path, PathBuf};
use std::process::ExitCode;
use std::sync::Arc;

use cairo_air::verifier::INTERACTION_POW_BITS;
use cairo_program_runner_lib::utils::get_program;
use circuit_cairo_verifier::privacy::get_pcs_config;
use circuit_cairo_verifier::statement::MEMORY_VALUES_LIMBS;
use circuit_cairo_verifier::verify::{CairoVerifierConfig, build_cairo_verifier_circuit};
Expand All @@ -41,7 +42,7 @@ use clap::Parser;
use leaf_prover::consts::DISABLED_COMPONENTS_CANONICAL_PREPROCESSED;
use leaf_prover::prove_leaf::{LeafVerifierComponents, leaf_verifier_components};
use stwo_cairo_common::preprocessed_columns::preprocessed_trace::PreProcessedTraceVariant;
use stwo_cairo_common::prover_types::cpu::M31;
use stwo_cairo_common::prover_types::cpu::{Felt252, M31};
use stwo_cairo_prover::stwo::core::pcs::PcsConfig;
use stwo_cairo_prover::stwo::core::poly::circle::CanonicCoset;
use stwo_cairo_prover::stwo::core::vcs_lifted::blake2_merkle::Blake2sM31MerkleChannel;
Expand Down Expand Up @@ -70,6 +71,11 @@ struct Args {
/// Log blowup factor of the verified Cairo proof (1, 2, or 3), passed to `get_pcs_config`.
#[clap(long = "log_blowup_factor", default_value_t = 1)]
log_blowup_factor: u32,
/// Path to the compiled program (Cairo compiled-program JSON) verified by the leaf circuit.
/// The program is hardcoded into the circuit and affects its topology. This is typically a
/// bootloader program, as the circuit cairo verifier expects a specific calling convention.
#[clap(long = "program")]
program: PathBuf,
/// Output a JSON circuit registry: a circuit-config map, the leaf verifiers (one per trace
/// size) and the multiverifier, each with its preprocessed root. All circuits are padded to
/// the shared target component sizes (the max of the leaf and multiverifier circuits at the
Expand Down Expand Up @@ -148,6 +154,7 @@ fn format_sizes(raw: &RawSizes, padded: &ComponentSizes) -> String {
fn build_leaf_verifier_context(
trace_log_size: u32,
log_blowup_factor: u32,
program: &Arc<[[M31; MEMORY_VALUES_LIMBS]]>,
) -> FinalizedContext<NoValue> {
let preprocessed_trace_variant = PreProcessedTraceVariant::Canonical;

Expand All @@ -164,22 +171,29 @@ fn build_leaf_verifier_context(
INTERACTION_POW_BITS,
);

// TODO(ilya): Use a real program for the circuit construction.
// Pass a dummy program for the circuit construction.
let program: Arc<[[M31; MEMORY_VALUES_LIMBS]]> =
std::iter::repeat_n([M31::from(0u32); MEMORY_VALUES_LIMBS], 128).collect();

let verifier_config = CairoVerifierConfig {
proof_config,
enabled_bits,
program,
program: program.clone(),
preprocessed_root: [0u32; 8].into(),
preprocessed_trace_variant,
};

build_cairo_verifier_circuit(&verifier_config)
}

/// Loads the compiled bootloader program at `path` and encodes its memory segment as the leaf
/// circuit's `program` value: one entry per data word, each a felt encoded as `MEMORY_VALUES_LIMBS`
/// nine-bit M31 limbs. Mirrors `leaf_prover`'s `program_felts`.
fn load_program(path: &Path) -> Result<Arc<[[M31; MEMORY_VALUES_LIMBS]]>, String> {
let program = get_program(path)
.map_err(|err| format!("Cannot get program from {}: {err}", path.display()))?;
Ok(program
.iter_data()
.map(|value| Felt252::from(value.get_int().unwrap()).get_limbs())
.collect())
}

/// Builds the multiverifier circuit topology that verifies two proofs of `preprocessed_leaf`.
///
/// Mirrors `circuit_multiverifier`'s test-only `get_preprocessed_multiverifier_from_circuit`:
Expand Down Expand Up @@ -219,8 +233,12 @@ fn build_multiverifier_context(

/// Builds the leaf verifier circuit for the given verified trace log size and returns its
/// component sizes.
fn leaf_component_sizes(trace_log_size: u32, log_blowup_factor: u32) -> (RawSizes, ComponentSizes) {
let context = build_leaf_verifier_context(trace_log_size, log_blowup_factor);
fn leaf_component_sizes(
trace_log_size: u32,
log_blowup_factor: u32,
program: &Arc<[[M31; MEMORY_VALUES_LIMBS]]>,
) -> (RawSizes, ComponentSizes) {
let context = build_leaf_verifier_context(trace_log_size, log_blowup_factor, program);
component_sizes(&context)
}

Expand All @@ -229,8 +247,9 @@ fn leaf_component_sizes(trace_log_size: u32, log_blowup_factor: u32) -> (RawSize
fn build_multiverifier_context_for_trace(
trace_log_size: u32,
log_blowup_factor: u32,
program: &Arc<[[M31; MEMORY_VALUES_LIMBS]]>,
) -> FinalizedContext<NoValue> {
let mut leaf_context = build_leaf_verifier_context(trace_log_size, log_blowup_factor);
let mut leaf_context = build_leaf_verifier_context(trace_log_size, log_blowup_factor, program);

// The multiverifier verifies proofs of the (preprocessed) leaf circuit, proven at the leaf
// circuit's own trace log size.
Expand All @@ -244,8 +263,13 @@ fn build_multiverifier_context_for_trace(
fn multiverifier_component_sizes(
trace_log_size: u32,
log_blowup_factor: u32,
program: &Arc<[[M31; MEMORY_VALUES_LIMBS]]>,
) -> (RawSizes, ComponentSizes) {
component_sizes(&build_multiverifier_context_for_trace(trace_log_size, log_blowup_factor))
component_sizes(&build_multiverifier_context_for_trace(
trace_log_size,
log_blowup_factor,
program,
))
}

/// Computes the Merkle root of a circuit's preprocessed trace, as eight little-endian Blake2s
Expand Down Expand Up @@ -290,6 +314,8 @@ fn main() -> ExitCode {
fn run() -> Result<(), String> {
let args = Args::parse();

let program = load_program(&args.program)?;

let output = if args.registry {
// Currently a single log blowup factor is used across the system.
let circuit_log_blowup_factor = args.log_blowup_factor;
Expand All @@ -302,9 +328,13 @@ fn run() -> Result<(), String> {
let leaf_sizes = compute_padded_sizes(&build_leaf_verifier_context(
args.max_trace_log_size,
args.log_blowup_factor,
&program,
));
let (_mv_raw, multiverifier_sizes) =
multiverifier_component_sizes(args.max_trace_log_size, args.log_blowup_factor);
let (_mv_raw, multiverifier_sizes) = multiverifier_component_sizes(
args.max_trace_log_size,
args.log_blowup_factor,
&program,
);
let target_sizes = max_component_sizes(&leaf_sizes, &multiverifier_sizes);

// All circuits are padded to `target_sizes` and proven with
Expand All @@ -320,7 +350,8 @@ fn run() -> Result<(), String> {

let leaf_verifiers = (args.min_trace_log_size..=args.max_trace_log_size)
.map(|trace_log_size| {
let context = build_leaf_verifier_context(trace_log_size, args.log_blowup_factor);
let context =
build_leaf_verifier_context(trace_log_size, args.log_blowup_factor, &program);
LeafVerifier {
config: CONFIG_ID.to_string(),
trace_log_size,
Expand All @@ -344,6 +375,7 @@ fn run() -> Result<(), String> {
build_multiverifier_context_for_trace(
args.max_trace_log_size,
args.log_blowup_factor,
&program,
),
&target_sizes,
circuit_log_blowup_factor,
Expand All @@ -359,16 +391,20 @@ fn run() -> Result<(), String> {
// (`max_trace_log_size`), which bounds the multiverifier size across the range.
let leaf_lines: Vec<String> = (args.min_trace_log_size..=args.max_trace_log_size)
.map(|trace_log_size| {
let (raw, padded) = leaf_component_sizes(trace_log_size, args.log_blowup_factor);
let (raw, padded) =
leaf_component_sizes(trace_log_size, args.log_blowup_factor, &program);
format!("{}: {}", trace_log_size, format_sizes(&raw, &padded))
})
.collect();
let leaf_section = format!("leaf:\n{}", leaf_lines.join("\n"));

// We report a single multiverifier line, as the multiverifier is about the same for
// all trace log sizes.
let (mv_raw, mv_padded) =
multiverifier_component_sizes(args.max_trace_log_size, args.log_blowup_factor);
let (mv_raw, mv_padded) = multiverifier_component_sizes(
args.max_trace_log_size,
args.log_blowup_factor,
&program,
);
let multiverifier_line = format!("multiverifier:\n{}", format_sizes(&mv_raw, &mv_padded));

format!("{leaf_section}\n\n{multiverifier_line}")
Expand Down
9 changes: 8 additions & 1 deletion crates/circuit_params/tests/cli_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,14 @@ use std::process::Command;
/// report.
fn run(registry: bool) -> String {
let binary = env!("CARGO_BIN_EXE_circuit-params");
let mut args = vec!["--min_trace_log_size", "25", "--max_trace_log_size", "25"];
// Any compiled Cairo program works for measuring the circuit's topology; this is a plain test
// program (exercising all opcodes and builtins), not a real bootloader.
let program = concat!(
env!("CARGO_MANIFEST_DIR"),
"/../leaf_prover/tests/data/use_all_opcodes_and_builtins_compiled.json"
);
let mut args =
vec!["--min_trace_log_size", "25", "--max_trace_log_size", "25", "--program", program];
if registry {
args.push("--registry");
}
Expand Down
Loading