|
| 1 | +//! Generate the soundcalc SP1 TOML config from SP1. |
| 2 | +//! |
| 3 | +//! Run with: |
| 4 | +//! cargo run --release -p sp1-prover --bin gen_soundcalc_toml -- --output <path> |
| 5 | +
|
| 6 | +use std::path::PathBuf; |
| 7 | + |
| 8 | +use clap::Parser; |
| 9 | +use slop_air::BaseAir; |
| 10 | +use slop_algebra::Field; |
| 11 | +use slop_basefold::BATCH_GRINDING_BITS; |
| 12 | +use sp1_core_executor::ELEMENT_THRESHOLD; |
| 13 | +use sp1_core_machine::riscv::RiscvAir; |
| 14 | +use sp1_hypercube::{air::MachineAir, Machine, GKR_GRINDING_BITS, MAX_CONSTRAINT_DEGREE}; |
| 15 | +use sp1_primitives::{ |
| 16 | + fri_params::{ |
| 17 | + unique_decoding_queries, CORE_LOG_BLOWUP, RECURSION_LOG_BLOWUP, SP1_PROOF_OF_WORK_BITS, |
| 18 | + }, |
| 19 | + SP1Field, |
| 20 | +}; |
| 21 | +use sp1_prover::{ |
| 22 | + CompressAir, CORE_LOG_STACKING_HEIGHT, CORE_MAX_LOG_ROW_COUNT, RECURSION_LOG_TRACE_AREA, |
| 23 | +}; |
| 24 | +use sp1_verifier::compressed::{RECURSION_LOG_STACKING_HEIGHT, RECURSION_MAX_LOG_ROW_COUNT}; |
| 25 | +use tracing_subscriber::EnvFilter; |
| 26 | + |
| 27 | +const SP1_VERSION: &str = env!("CARGO_PKG_VERSION"); |
| 28 | +const DEFAULT_OUTPUT: &str = concat!(env!("CARGO_MANIFEST_DIR"), "/scripts/sp1.toml"); |
| 29 | + |
| 30 | +#[derive(Parser)] |
| 31 | +#[command( |
| 32 | + about = "Generate soundcalc TOML file from SP1", |
| 33 | + long_about = None, |
| 34 | +)] |
| 35 | +struct Args { |
| 36 | + #[arg(short, long, default_value = DEFAULT_OUTPUT)] |
| 37 | + output: PathBuf, |
| 38 | +} |
| 39 | + |
| 40 | +struct CircuitData { |
| 41 | + trace_columns: usize, |
| 42 | + num_constraints: usize, |
| 43 | + num_lookups_m: usize, |
| 44 | + num_columns_s: usize, |
| 45 | +} |
| 46 | + |
| 47 | +fn get_circuit_data<F: Field, A>(machine: Machine<F, A>) -> CircuitData |
| 48 | +where |
| 49 | + A: sp1_hypercube::air::MachineAir<F>, |
| 50 | +{ |
| 51 | + let mut max_cols = 0usize; |
| 52 | + let mut max_constr = 0usize; |
| 53 | + let mut max_inter = 0usize; |
| 54 | + for cluster in &machine.shape().chip_clusters { |
| 55 | + let mut cols = 0usize; |
| 56 | + let mut constr = 0usize; |
| 57 | + let mut inter = 0usize; |
| 58 | + for chip in cluster { |
| 59 | + constr += chip.num_constraints; |
| 60 | + cols += chip.preprocessed_width() + chip.width(); |
| 61 | + inter += chip.receives().len() + chip.sends().len(); |
| 62 | + } |
| 63 | + max_cols = max_cols.max(cols); |
| 64 | + max_constr = max_constr.max(constr); |
| 65 | + max_inter = max_inter.max(inter); |
| 66 | + } |
| 67 | + let max_values_len = machine |
| 68 | + .chips() |
| 69 | + .iter() |
| 70 | + .flat_map(|chip| chip.receives().iter().chain(chip.sends().iter())) |
| 71 | + .map(|interaction| interaction.values.len()) |
| 72 | + .max() |
| 73 | + .unwrap_or(0); |
| 74 | + CircuitData { |
| 75 | + trace_columns: max_cols, |
| 76 | + num_constraints: max_constr, |
| 77 | + num_lookups_m: max_inter, |
| 78 | + num_columns_s: max_values_len + 1, |
| 79 | + } |
| 80 | +} |
| 81 | + |
| 82 | +fn folding_factors(log_stacking_height: u32) -> String { |
| 83 | + let items = std::iter::repeat_n("2", log_stacking_height as usize).collect::<Vec<_>>(); |
| 84 | + format!("[{}]", items.join(", ")) |
| 85 | +} |
| 86 | + |
| 87 | +fn format_rho(blowup_factor: u32) -> String { |
| 88 | + let rho = 1.0_f64 / f64::from(blowup_factor); |
| 89 | + let s = format!("{rho}"); |
| 90 | + if s.contains('.') { |
| 91 | + s |
| 92 | + } else { |
| 93 | + format!("{s}.0") |
| 94 | + } |
| 95 | +} |
| 96 | + |
| 97 | +fn main() { |
| 98 | + tracing_subscriber::fmt() |
| 99 | + .with_env_filter( |
| 100 | + EnvFilter::try_from_default_env().unwrap_or_else(|_| EnvFilter::new("info")), |
| 101 | + ) |
| 102 | + .init(); |
| 103 | + |
| 104 | + let args = Args::parse(); |
| 105 | + |
| 106 | + let core = get_circuit_data(RiscvAir::<SP1Field>::machine()); |
| 107 | + let compress = get_circuit_data(CompressAir::<SP1Field>::compress_machine()); |
| 108 | + |
| 109 | + let core_blowup = 1u32 << CORE_LOG_BLOWUP; |
| 110 | + let recursion_blowup = 1u32 << RECURSION_LOG_BLOWUP; |
| 111 | + let core_trace_len: u64 = 1u64 << CORE_MAX_LOG_ROW_COUNT; |
| 112 | + let recursion_trace_len: u64 = 1u64 << RECURSION_MAX_LOG_ROW_COUNT; |
| 113 | + let core_dense_len: u64 = 1u64 << CORE_LOG_STACKING_HEIGHT; |
| 114 | + let recursion_dense_len: u64 = 1u64 << RECURSION_LOG_STACKING_HEIGHT; |
| 115 | + let core_queries = unique_decoding_queries(CORE_LOG_BLOWUP); |
| 116 | + let recursion_queries = unique_decoding_queries(RECURSION_LOG_BLOWUP); |
| 117 | + let core_rho = format_rho(core_blowup); |
| 118 | + let recursion_rho = format_rho(recursion_blowup); |
| 119 | + let core_folding = folding_factors(CORE_LOG_STACKING_HEIGHT); |
| 120 | + let recursion_folding = folding_factors(RECURSION_LOG_STACKING_HEIGHT); |
| 121 | + let core_dense_batch: u64 = ELEMENT_THRESHOLD / (1u64 << CORE_LOG_STACKING_HEIGHT) + 1; |
| 122 | + let recursion_dense_batch: u64 = |
| 123 | + (1u64 << RECURSION_LOG_TRACE_AREA) / (1u64 << RECURSION_LOG_STACKING_HEIGHT); |
| 124 | + |
| 125 | + let toml = format!( |
| 126 | + "\ |
| 127 | +# SP1 Hypercube VM Configuration |
| 128 | +# Auto-generated by `cargo run --release -p sp1-prover --bin gen_soundcalc_toml`. |
| 129 | +
|
| 130 | +[zkevm] |
| 131 | +name = \"SP1\" |
| 132 | +protocol_family = \"JAGGED\" |
| 133 | +field = \"KoalaBear^4\" |
| 134 | +version = \"{SP1_VERSION}\" |
| 135 | +hash_size_bits = 248 |
| 136 | +
|
| 137 | +[[circuits]] |
| 138 | +name = \"core\" |
| 139 | +udr_only = true |
| 140 | +blowup_factor = {core_blowup} |
| 141 | +rho = {core_rho} |
| 142 | +trace_length = {core_trace_len} # 2^{CORE_MAX_LOG_ROW_COUNT} |
| 143 | +trace_columns = {core_trace_columns} |
| 144 | +dense_length = {core_dense_len} # 2^{CORE_LOG_STACKING_HEIGHT} |
| 145 | +dense_batch = {core_dense_batch} |
| 146 | +num_constraints = {core_num_constraints} |
| 147 | +air_max_degree = {MAX_CONSTRAINT_DEGREE} |
| 148 | +# SP1 has no \"next row\" constraints. |
| 149 | +opening_points = 1 |
| 150 | +# We batch using the random `eq` polynomials. |
| 151 | +power_batching = false |
| 152 | +multilinear_batching = true |
| 153 | +multilinear_zerocheck = true |
| 154 | +num_queries = {core_queries} |
| 155 | +fri_folding_factors = {core_folding} |
| 156 | +fri_early_stop_degree = {core_blowup} |
| 157 | +grinding_batching_phase = {BATCH_GRINDING_BITS} |
| 158 | +grinding_query_phase = {SP1_PROOF_OF_WORK_BITS} |
| 159 | +
|
| 160 | +[[circuits.lookups]] |
| 161 | +name = \"lookup\" |
| 162 | +logup_type = \"multivariate\" |
| 163 | +rows_L = {core_trace_len} |
| 164 | +rows_T = 0 |
| 165 | +num_columns_S = {core_num_columns_s} |
| 166 | +num_lookups_M = {core_num_lookups_m} |
| 167 | +grinding_bits_lookup = {GKR_GRINDING_BITS} |
| 168 | +multilinear_fingerprint = true |
| 169 | +
|
| 170 | +
|
| 171 | +[[circuits]] |
| 172 | +name = \"compress\" |
| 173 | +udr_only = true |
| 174 | +blowup_factor = {recursion_blowup} |
| 175 | +rho = {recursion_rho} |
| 176 | +trace_length = {recursion_trace_len} # 2^{RECURSION_MAX_LOG_ROW_COUNT} |
| 177 | +trace_columns = {recursion_trace_columns} |
| 178 | +dense_length = {recursion_dense_len} # 2^{RECURSION_LOG_STACKING_HEIGHT} |
| 179 | +dense_batch = {recursion_dense_batch} |
| 180 | +num_constraints = {recursion_num_constraints} |
| 181 | +air_max_degree = {MAX_CONSTRAINT_DEGREE} |
| 182 | +# SP1 has no \"next row\" constraints. |
| 183 | +opening_points = 1 |
| 184 | +# We batch using the random `eq` polynomials. |
| 185 | +power_batching = false |
| 186 | +multilinear_batching = true |
| 187 | +multilinear_zerocheck = true |
| 188 | +num_queries = {recursion_queries} |
| 189 | +fri_folding_factors = {recursion_folding} |
| 190 | +fri_early_stop_degree = {recursion_blowup} |
| 191 | +grinding_batching_phase = {BATCH_GRINDING_BITS} |
| 192 | +grinding_query_phase = {SP1_PROOF_OF_WORK_BITS} |
| 193 | +
|
| 194 | +[[circuits.lookups]] |
| 195 | +name = \"lookup\" |
| 196 | +logup_type = \"multivariate\" |
| 197 | +rows_L = {recursion_trace_len} |
| 198 | +rows_T = 0 |
| 199 | +num_columns_S = {recursion_num_columns_s} |
| 200 | +num_lookups_M = {recursion_num_lookups_m} |
| 201 | +grinding_bits_lookup = {GKR_GRINDING_BITS} |
| 202 | +multilinear_fingerprint = true |
| 203 | +", |
| 204 | + core_trace_columns = core.trace_columns, |
| 205 | + core_num_constraints = core.num_constraints, |
| 206 | + core_num_lookups_m = core.num_lookups_m, |
| 207 | + core_num_columns_s = core.num_columns_s, |
| 208 | + recursion_trace_columns = compress.trace_columns, |
| 209 | + recursion_num_constraints = compress.num_constraints, |
| 210 | + recursion_num_lookups_m = compress.num_lookups_m, |
| 211 | + recursion_num_columns_s = compress.num_columns_s, |
| 212 | + ); |
| 213 | + |
| 214 | + if let Some(parent) = args.output.parent() { |
| 215 | + std::fs::create_dir_all(parent).expect("create output dir"); |
| 216 | + } |
| 217 | + std::fs::write(&args.output, toml).expect("write toml"); |
| 218 | + tracing::info!("wrote {}", args.output.display()); |
| 219 | +} |
0 commit comments