From 46de52cb282dcd7cb23a97dfc6a9fff84757c912 Mon Sep 17 00:00:00 2001 From: Mario Rugiero Date: Mon, 10 Aug 2026 15:00:43 -0300 Subject: [PATCH 1/2] feat(prover): chunk the accelerator tables and project them for storage KECCAK, KECCAK_RND, ECSM, ECDAS, HINT and COMMIT had no max_rows entry: each one padded its whole op list into a single table, so a keccak- or ECSM-heavy epoch built one table whose height is proportional to guest data. At epoch_size_log2=23 that is a single multi-GB allocation no storage mode can stream. KECCAK, KECCAK_RND, ECSM and ECDAS were also absent from auto_storage's projection entirely, so the Ram/Disk decision under-projected exactly the programs most likely to need Disk. Every one of these chips evaluates row-locally (no `main(1, ..)` reference), so their rows split across tables the way the core chips' do, and the buses they drive are a multiset argument that does not care which table a row sits in. KECCAK_RND splits on whole permutations, since one call is 24 contiguous rows. The limits follow the existing effective-width model, and `accelerator_max_rows_track_effective_width` pins each width to the AIR so a new column or bus cannot leave a limit stale. Breaking: the six tables move out of FIXED_TABLE_COUNT (11 -> 5) into TableCounts, which changes the sub-proof layout and the statement absorbed into the transcript (tags bumped to V4/V3). Prover and verifier must be deployed together; earlier binaries cannot verify these proofs. --- prover/src/auto_storage.rs | 50 ++++ prover/src/lib.rs | 138 ++++++--- prover/src/statement.rs | 18 +- prover/src/tables/ecdas.rs | 6 + prover/src/tables/keccak_rnd.rs | 6 +- prover/src/tables/mod.rs | 46 +++ prover/src/tables/trace_builder.rs | 264 ++++++++++++------ .../src/tests/accelerator_chunking_tests.rs | 123 ++++++++ .../tests/count_table_lengths_drift_tests.rs | 30 +- prover/src/tests/mod.rs | 2 + prover/src/tests/prove_elfs_tests.rs | 28 +- prover/src/tests/statement_tests.rs | 6 + 12 files changed, 592 insertions(+), 125 deletions(-) create mode 100644 prover/src/tests/accelerator_chunking_tests.rs diff --git a/prover/src/auto_storage.rs b/prover/src/auto_storage.rs index 6b5ed8a5d..6c1477c85 100644 --- a/prover/src/auto_storage.rs +++ b/prover/src/auto_storage.rs @@ -11,7 +11,18 @@ use crate::tables::commit::{bus_interactions as commit_buses, cols::NUM_COLUMNS use crate::tables::cpu::{bus_interactions as cpu_buses, cols::NUM_COLUMNS as CPU_COLS}; use crate::tables::decode::{bus_interactions as decode_buses, cols::NUM_COLUMNS as DECODE_COLS}; use crate::tables::dvrm::{bus_interactions as dvrm_buses, cols::NUM_COLUMNS as DVRM_COLS}; +use crate::tables::ecdas::{bus_interactions as ecdas_buses, cols::NUM_COLUMNS as ECDAS_COLS}; +use crate::tables::ecsm::{bus_interactions as ecsm_buses, cols::NUM_COLUMNS as ECSM_COLS}; use crate::tables::halt::{bus_interactions as halt_buses, cols::NUM_COLUMNS as HALT_COLS}; +use crate::tables::hint::{bus_interactions as hint_buses, cols::NUM_COLUMNS as HINT_COLS}; +use crate::tables::keccak::{bus_interactions as keccak_buses, cols::NUM_COLUMNS as KECCAK_COLS}; +use crate::tables::keccak_rc::{ + NUM_ROWS as KECCAK_RC_ROWS, bus_interactions as keccak_rc_buses, + cols::NUM_COLUMNS as KECCAK_RC_COLS, +}; +use crate::tables::keccak_rnd::{ + bus_interactions as keccak_rnd_buses, cols::NUM_COLUMNS as KECCAK_RND_COLS, +}; use crate::tables::load::{bus_interactions as load_buses, cols::NUM_COLUMNS as LOAD_COLS}; use crate::tables::lt::{bus_interactions as lt_buses, cols::NUM_COLUMNS as LT_COLS}; use crate::tables::memw::{bus_interactions as memw_buses, cols::NUM_COLUMNS as MEMW_COLS}; @@ -109,6 +120,7 @@ fn table_specs(lengths: &TableLengths) -> Vec { let bitwise_rows = BITWISE_ROWS as u64; let register_rows = NUM_REGISTER_ADDRESSES.next_power_of_two() as u64; let halt_rows = 1u64; + let keccak_rc_rows = KECCAK_RC_ROWS as u64; let page_rows = PAGE_SIZE as u64; let mut specs = vec![ @@ -178,6 +190,44 @@ fn table_specs(lengths: &TableLengths) -> Vec { aux_cols(commit_buses().len()), 1, ), + // Accelerator chips. Wide and driven by guest data, so leaving them out + // under-projects any keccak- or ECSM-heavy program. + ( + lengths.keccak_padded_rows, + KECCAK_COLS as u64, + aux_cols(keccak_buses().len()), + 1, + ), + ( + lengths.keccak_rnd_padded_rows, + KECCAK_RND_COLS as u64, + aux_cols(keccak_rnd_buses().len()), + 1, + ), + ( + keccak_rc_rows, + KECCAK_RC_COLS as u64, + aux_cols(keccak_rc_buses().len()), + 2, + ), + ( + lengths.ecsm_padded_rows, + ECSM_COLS as u64, + aux_cols(ecsm_buses().len()), + 1, + ), + ( + lengths.ecdas_padded_rows, + ECDAS_COLS as u64, + aux_cols(ecdas_buses().len()), + 1, + ), + ( + lengths.hint_padded_rows, + HINT_COLS as u64, + aux_cols(hint_buses().len()), + 1, + ), // BITWISE / DECODE / PAGE / REGISTER take the preprocessed-trace commit // path: it extracts ALL columns into the LDE and builds two Merkle trees // (precomputed_tree + mult_tree), so main_cols = full NUM_COLUMNS and diff --git a/prover/src/lib.rs b/prover/src/lib.rs index 79ef4c715..06faea2dc 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -81,9 +81,9 @@ pub struct RuntimePageRange { } /// Number of tables that always contribute exactly one sub-proof, regardless -/// of `TableCounts`: bitwise, decode, halt, commit, keccak, keccak_rnd, -/// keccak_rc, register, ecsm, ecdas, hint. -pub const FIXED_TABLE_COUNT: usize = 11; +/// of `TableCounts`: bitwise, decode, halt, keccak_rc, register. Every other +/// table's height grows with the execution, so it is chunked and counted. +pub const FIXED_TABLE_COUNT: usize = 5; /// Number of chunks for each split table. /// The verifier needs this to reconstruct matching AIRs. @@ -104,6 +104,13 @@ pub struct TableCounts { pub bytewise: usize, pub store: usize, pub cpu32: usize, + // Accelerator chips + pub keccak: usize, + pub keccak_rnd: usize, + pub ecsm: usize, + pub ecdas: usize, + pub hint: usize, + pub commit: usize, } impl TableCounts { @@ -123,6 +130,12 @@ impl TableCounts { + self.bytewise + self.store + self.cpu32 + + self.keccak + + self.keccak_rnd + + self.ecsm + + self.ecdas + + self.hint + + self.commit } /// Validate that all required tables have at least one chunk. @@ -145,6 +158,12 @@ impl TableCounts { ("bytewise", self.bytewise), ("store", self.store), ("cpu32", self.cpu32), + ("keccak", self.keccak), + ("keccak_rnd", self.keccak_rnd), + ("ecsm", self.ecsm), + ("ecdas", self.ecdas), + ("hint", self.hint), + ("commit", self.commit), ]; for (name, count) in checks { if count == 0 { @@ -516,13 +535,13 @@ pub(crate) struct VmAirs { pub dvrms: Vec, pub branches: Vec, pub halt: VmAir, - pub commit: VmAir, - pub keccak: VmAir, - pub keccak_rnd: VmAir, + pub commits: Vec, + pub keccaks: Vec, + pub keccak_rnds: Vec, pub keccak_rc: VmAir, - pub ecsm: VmAir, - pub ecdas: VmAir, - pub hint: VmAir, + pub ecsms: Vec, + pub ecdases: Vec, + pub hints: Vec, pub register: VmAir, pub pages: Vec, pub memw_registers: Vec, @@ -542,18 +561,30 @@ impl VmAirs { let mut pairs: Vec> = vec![ (self.bitwise.as_ref(), &mut traces.bitwise, &()), (self.decode.as_ref(), &mut traces.decode, &()), - (self.commit.as_ref(), &mut traces.commit, &()), - (self.keccak.as_ref(), &mut traces.keccak, &()), - (self.keccak_rnd.as_ref(), &mut traces.keccak_rnd, &()), (self.keccak_rc.as_ref(), &mut traces.keccak_rc, &()), - (self.ecsm.as_ref(), &mut traces.ecsm, &()), - (self.ecdas.as_ref(), &mut traces.ecdas, &()), - (self.hint.as_ref(), &mut traces.hint, &()), (self.register.as_ref(), &mut traces.register, &()), ]; if self.include_halt { pairs.push((self.halt.as_ref(), &mut traces.halt, &())); } + for (air, trace) in self.commits.iter().zip(traces.commits.iter_mut()) { + pairs.push((air.as_ref(), trace, &())); + } + for (air, trace) in self.keccaks.iter().zip(traces.keccaks.iter_mut()) { + pairs.push((air.as_ref(), trace, &())); + } + for (air, trace) in self.keccak_rnds.iter().zip(traces.keccak_rnds.iter_mut()) { + pairs.push((air.as_ref(), trace, &())); + } + for (air, trace) in self.ecsms.iter().zip(traces.ecsms.iter_mut()) { + pairs.push((air.as_ref(), trace, &())); + } + for (air, trace) in self.ecdases.iter().zip(traces.ecdases.iter_mut()) { + pairs.push((air.as_ref(), trace, &())); + } + for (air, trace) in self.hints.iter().zip(traces.hints.iter_mut()) { + pairs.push((air.as_ref(), trace, &())); + } for (air, trace) in self.cpus.iter().zip(traces.cpus.iter_mut()) { pairs.push((air.as_ref(), trace, &())); @@ -617,18 +648,30 @@ impl VmAirs { let mut refs: Vec<&dyn AIR> = vec![ self.bitwise.as_ref(), self.decode.as_ref(), - self.commit.as_ref(), - self.keccak.as_ref(), - self.keccak_rnd.as_ref(), self.keccak_rc.as_ref(), - self.ecsm.as_ref(), - self.ecdas.as_ref(), - self.hint.as_ref(), self.register.as_ref(), ]; if self.include_halt { refs.push(self.halt.as_ref()); } + for air in &self.commits { + refs.push(air.as_ref()); + } + for air in &self.keccaks { + refs.push(air.as_ref()); + } + for air in &self.keccak_rnds { + refs.push(air.as_ref()); + } + for air in &self.ecsms { + refs.push(air.as_ref()); + } + for air in &self.ecdases { + refs.push(air.as_ref()); + } + for air in &self.hints { + refs.push(air.as_ref()); + } for air in &self.cpus { refs.push(air.as_ref()); @@ -786,16 +829,45 @@ impl VmAirs { }) .collect(); let halt: VmAir = Box::new(create_halt_air(proof_options)); - let commit: VmAir = Box::new(create_commit_air(proof_options)); - let keccak: VmAir = Box::new(create_keccak_air(proof_options)); - let keccak_rnd: VmAir = Box::new(create_keccak_rnd_air(proof_options)); + let commits: Vec<_> = (0..table_counts.commit) + .map(|i| { + Box::new(create_commit_air(proof_options).with_name(&format!("COMMIT[{}]", i))) + as VmAir + }) + .collect(); + let keccaks: Vec<_> = (0..table_counts.keccak) + .map(|i| { + Box::new(create_keccak_air(proof_options).with_name(&format!("KECCAK[{}]", i))) + as VmAir + }) + .collect(); + let keccak_rnds: Vec<_> = (0..table_counts.keccak_rnd) + .map(|i| { + Box::new( + create_keccak_rnd_air(proof_options).with_name(&format!("KECCAK_RND[{}]", i)), + ) as VmAir + }) + .collect(); let keccak_rc: VmAir = Box::new(create_keccak_rc_air(proof_options).with_preprocessed( tables::keccak_rc::preprocessed_commitment(proof_options), tables::keccak_rc::NUM_PRECOMPUTED_COLS, )); - let ecsm: VmAir = Box::new(create_ecsm_air(proof_options)); - let ecdas: VmAir = Box::new(create_ecdas_air(proof_options)); - let hint: VmAir = Box::new(create_hint_air(proof_options)); + let ecsms: Vec<_> = (0..table_counts.ecsm) + .map(|i| { + Box::new(create_ecsm_air(proof_options).with_name(&format!("ECSM[{}]", i))) as VmAir + }) + .collect(); + let ecdases: Vec<_> = (0..table_counts.ecdas) + .map(|i| { + Box::new(create_ecdas_air(proof_options).with_name(&format!("ECDAS[{}]", i))) + as VmAir + }) + .collect(); + let hints: Vec<_> = (0..table_counts.hint) + .map(|i| { + Box::new(create_hint_air(proof_options).with_name(&format!("HINT[{}]", i))) as VmAir + }) + .collect(); let register: VmAir = if let Some((commitment, num_preprocessed_cols)) = register_preprocessed { Box::new( @@ -910,13 +982,13 @@ impl VmAirs { dvrms, branches, halt, - commit, - keccak, - keccak_rnd, + commits, + keccaks, + keccak_rnds, keccak_rc, - ecsm, - ecdas, - hint, + ecsms, + ecdases, + hints, register, pages, memw_registers, diff --git a/prover/src/statement.rs b/prover/src/statement.rs index 81c18baa5..c4ebd85f8 100644 --- a/prover/src/statement.rs +++ b/prover/src/statement.rs @@ -17,7 +17,7 @@ use crate::test_utils::E; use crate::{RuntimePageRange, TableCounts}; /// Domain-separation tag. Bump the suffix (`_V2`, ...) on any encoding change. -const DOMAIN_TAG: &[u8] = b"LAMBDAVM_STARK_STATEMENT_V3"; +const DOMAIN_TAG: &[u8] = b"LAMBDAVM_STARK_STATEMENT_V4"; /// Canonical full-ELF identity digest — exactly what [`absorb_statement`] binds /// into the transcript. The recursion attestation folds the same digest into @@ -111,6 +111,12 @@ pub(crate) fn absorb_statement_with_digest( bytewise, store, cpu32, + keccak, + keccak_rnd, + ecsm, + ecdas, + hint, + commit, } = table_counts; for count in [ cpu, @@ -127,6 +133,12 @@ pub(crate) fn absorb_statement_with_digest( bytewise, store, cpu32, + keccak, + keccak_rnd, + ecsm, + ecdas, + hint, + commit, ] { t.append_bytes(&(count as u64).to_le_bytes()); } @@ -155,8 +167,8 @@ pub(crate) fn absorb_statement_with_digest( /// Continuation domain tags. Distinct from the monolithic `DOMAIN_TAG` so a /// monolithic proof and a continuation proof can never share a transcript prefix. -const CONTINUATION_EPOCH_TAG: &[u8] = b"LAMBDAVM_CONTINUATION_EPOCH_V2"; -const CONTINUATION_GLOBAL_TAG: &[u8] = b"LAMBDAVM_CONTINUATION_GLOBAL_V2"; +const CONTINUATION_EPOCH_TAG: &[u8] = b"LAMBDAVM_CONTINUATION_EPOCH_V3"; +const CONTINUATION_GLOBAL_TAG: &[u8] = b"LAMBDAVM_CONTINUATION_GLOBAL_V3"; /// Statement bound into the cross-epoch **global** proof's transcript before /// Phase A: the ELF (so the global proof is program-bound), the epoch count (so a diff --git a/prover/src/tables/ecdas.rs b/prover/src/tables/ecdas.rs index 6d4b8a908..84befe4e3 100644 --- a/prover/src/tables/ecdas.rs +++ b/prover/src/tables/ecdas.rs @@ -70,6 +70,12 @@ pub mod cols { // Operation struct // ========================================================================= +/// Rows one ECSM call can add here, at most: the double-and-add ladder runs at +/// most one double and one add per bit of a 256-bit scalar. Used to bound the +/// table's height when sizing storage, which is why it is an upper bound and +/// not the exact per-call count (that depends on the scalar). +pub const MAX_STEPS_PER_ECSM: usize = 2 * 256; + /// One ECDAS row: a double/add step witness plus its ECALL timestamp. #[derive(Debug, Clone)] pub struct EcdasOperation { diff --git a/prover/src/tables/keccak_rnd.rs b/prover/src/tables/keccak_rnd.rs index 51b7759f3..3c866c86f 100644 --- a/prover/src/tables/keccak_rnd.rs +++ b/prover/src/tables/keccak_rnd.rs @@ -207,6 +207,10 @@ pub mod cols { // Operation struct // ========================================================================= +/// Trace rows one [`KeccakRoundOperation`] expands into, one per keccak round. +/// Chunking splits on whole operations, so a chunk limit in rows divides by this. +pub const ROUNDS_PER_OP: usize = 24; + /// One keccak permutation call's worth of data (produces 24 rows). #[derive(Debug, Clone)] pub struct KeccakRoundOperation { @@ -246,7 +250,7 @@ fn hwsl(halfword: u16, shift: u8) -> (u16, u16) { pub fn generate_keccak_rnd_trace( ops: &[KeccakRoundOperation], ) -> TraceTable { - let n_rows = (ops.len() * 24).next_power_of_two().max(4); + let n_rows = (ops.len() * ROUNDS_PER_OP).next_power_of_two().max(4); let mut trace = TraceTable::new_main( crate::tables::types::zeroed_fe_vec(n_rows * cols::NUM_COLUMNS), cols::NUM_COLUMNS, diff --git a/prover/src/tables/mod.rs b/prover/src/tables/mod.rs index f1a899f56..bdc0f5e7c 100644 --- a/prover/src/tables/mod.rs +++ b/prover/src/tables/mod.rs @@ -80,6 +80,20 @@ pub const STATIC_BLOWUP_FACTORS: &[u8] = &[2, 4, 8]; /// | LOAD | 18 | 5 | 33 | 2^20 | /// | BRANCH | 14 | 6 | 32 | 2^20 | /// | MEMW_R | 10 | 7 | 31 | 2^20 | +/// +/// The accelerator chips are sized the same way. They are wide, so their limits +/// are small; `accelerator_max_rows_track_effective_width` pins each width to +/// the AIR so a column or bus added to one of these tables cannot silently leave +/// its limit behind. +/// +/// | Table | Main | Bus | Eff.width | Max rows | +/// |------------|------|------|-----------|----------| +/// | KECCAK | 511 | 134 | 913 | 2^16 | +/// | KECCAK_RND | 1480 | 1031 | 4573 | 2^14 | +/// | ECSM | 667 | 579 | 2404 | 2^15 | +/// | ECDAS | 521 | 388 | 1685 | 2^15 | +/// | HINT | 41 | 27 | 122 | 2^19 | +/// | COMMIT | 19 | 18 | 73 | 2^20 | pub mod max_rows { pub const CPU: usize = 1 << 19; // 524,288 — eff. width 194 pub const MEMW: usize = 1 << 19; // 524,288 — eff. width 127 (baseline) @@ -96,6 +110,15 @@ pub mod max_rows { pub const BYTEWISE: usize = 1 << 20; pub const STORE: usize = 1 << 20; pub const CPU32: usize = 1 << 19; + // Accelerator chips. Row counts here are trace rows, not calls: KECCAK_RND + // emits `keccak_rnd::ROUNDS_PER_OP` rows per permutation and chunks on whole + // permutations, so its limit is the rounded-down multiple of that. + pub const KECCAK: usize = 1 << 16; + pub const KECCAK_RND: usize = 1 << 14; + pub const ECSM: usize = 1 << 15; + pub const ECDAS: usize = 1 << 15; + pub const HINT: usize = 1 << 19; + pub const COMMIT: usize = 1 << 20; } /// Per-table maximum row limits, configurable for different environments. @@ -118,6 +141,12 @@ pub struct MaxRowsConfig { pub bytewise: usize, pub store: usize, pub cpu32: usize, + pub keccak: usize, + pub keccak_rnd: usize, + pub ecsm: usize, + pub ecdas: usize, + pub hint: usize, + pub commit: usize, } impl Default for MaxRowsConfig { @@ -137,6 +166,12 @@ impl Default for MaxRowsConfig { bytewise: max_rows::BYTEWISE, store: max_rows::STORE, cpu32: max_rows::CPU32, + keccak: max_rows::KECCAK, + keccak_rnd: max_rows::KECCAK_RND, + ecsm: max_rows::ECSM, + ecdas: max_rows::ECDAS, + hint: max_rows::HINT, + commit: max_rows::COMMIT, } } } @@ -160,6 +195,17 @@ impl MaxRowsConfig { bytewise: 1 << 5, store: 1 << 5, cpu32: 1 << 5, + // The accelerator chips keep their production limits. Shrinking them + // to 2^5 would split a committed output or one ECSM ladder into + // dozens of sub-proofs, which costs every test that uses this config + // far more than the extra chunk coverage is worth + // (`accelerator_chunking_tests` shrinks them where it wants chunks). + keccak: max_rows::KECCAK, + keccak_rnd: max_rows::KECCAK_RND, + ecsm: max_rows::ECSM, + ecdas: max_rows::ECDAS, + hint: max_rows::HINT, + commit: max_rows::COMMIT, } } } diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 29874caef..61cacd473 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -942,6 +942,7 @@ fn collect_ecsm_ops( memory_state.write_bytes(addr, dword, 8, t + 2); } + debug_assert!(witness.steps.len() <= ecdas::MAX_STEPS_PER_ECSM); let ecdas_ops = witness .steps .iter() @@ -2852,26 +2853,31 @@ pub struct Traces { /// HALT single-row table for program termination pub halt: TraceTable, - /// COMMIT table for write syscall (byte-by-byte commit with recursive bus) - pub commit: TraceTable, + /// COMMIT tables for write syscall (byte-by-byte commit with recursive bus), + /// split into chunks of max_rows::COMMIT + pub commits: Vec>, - /// KECCAK core table (one row per keccak permutation call) - pub keccak: TraceTable, + /// KECCAK core tables (one row per keccak permutation call, split into + /// chunks of max_rows::KECCAK) + pub keccaks: Vec>, - /// KECCAK_RND round table (24 rows per keccak call) - pub keccak_rnd: TraceTable, + /// KECCAK_RND round tables (24 rows per keccak call, split on whole calls + /// into chunks of at most max_rows::KECCAK_RND rows) + pub keccak_rnds: Vec>, /// KECCAK_RC precomputed round constant table (32 rows) pub keccak_rc: TraceTable, - /// ECSM core table (one row per scalar-multiplication ecall) - pub ecsm: TraceTable, + /// ECSM core tables (one row per scalar-multiplication ecall, split into + /// chunks of max_rows::ECSM) + pub ecsms: Vec>, - /// ECDAS double/add table (variable rows per ecall) - pub ecdas: TraceTable, + /// ECDAS double/add tables (split into chunks of max_rows::ECDAS) + pub ecdases: Vec>, - /// HINT table (one row per non-constraining hint ecall). - pub hint: TraceTable, + /// HINT tables (one row per non-constraining hint ecall, split into chunks + /// of max_rows::HINT) + pub hints: Vec>, /// MEMW_R register-only fast-path traces (split into chunks of max_rows::MEMW_R) pub memw_registers: Vec>, @@ -3500,9 +3506,25 @@ fn build_traces( decode::update_multiplicities(&mut decode, decode_pc_to_row, &decode_lookups); decode }; - let gen_commit = || commit::generate_commit_trace(&commit_ops); - let gen_keccak = || keccak::generate_keccak_trace(&keccak_ops); - let gen_keccak_rnd = || { + let gen_commits = || { + chunk_and_generate( + &commit_ops, + max_rows.commit, + commit::generate_commit_trace, + #[cfg(feature = "disk-spill")] + storage_mode, + ) + }; + let gen_keccaks = || { + chunk_and_generate( + &keccak_ops, + max_rows.keccak, + keccak::generate_keccak_trace, + #[cfg(feature = "disk-spill")] + storage_mode, + ) + }; + let gen_keccak_rnds = || { let keccak_rnd_ops: Vec = keccak_ops .iter() .map(|op| KeccakRoundOperation { @@ -3511,7 +3533,16 @@ fn build_traces( output: op.output, }) .collect(); - keccak_rnd::generate_keccak_rnd_trace(&keccak_rnd_ops) + // A chunk holds whole permutations, so the row limit divides by the 24 + // rows each one expands into (at least one permutation per chunk). + let ops_per_chunk = (max_rows.keccak_rnd / keccak_rnd::ROUNDS_PER_OP).max(1); + chunk_and_generate( + &keccak_rnd_ops, + ops_per_chunk, + keccak_rnd::generate_keccak_rnd_trace, + #[cfg(feature = "disk-spill")] + storage_mode, + ) }; let gen_keccak_rc = || { let mut keccak_rc_trace = keccak_rc::generate_keccak_rc_trace(); @@ -3530,23 +3561,47 @@ fn build_traces( let gen_register = || register::generate_register_trace(®ister_final_state, register_init); let gen_halt = || halt::generate_halt_trace(halt_timestamp, halt_next_pc); // ECSM accelerator traces (empty/all-padding for programs that do not use ECSM). - let gen_ecsm = || ecsm::generate_ecsm_trace(&ecsm_ops); - let gen_ecdas = || ecdas::generate_ecdas_trace(&ecdas_ops); + let gen_ecsms = || { + chunk_and_generate( + &ecsm_ops, + max_rows.ecsm, + ecsm::generate_ecsm_trace, + #[cfg(feature = "disk-spill")] + storage_mode, + ) + }; + let gen_ecdases = || { + chunk_and_generate( + &ecdas_ops, + max_rows.ecdas, + ecdas::generate_ecdas_trace, + #[cfg(feature = "disk-spill")] + storage_mode, + ) + }; // HINT table (all-padding for programs that make no hint ecalls). - let gen_hint = || hint::generate_hint_trace(&hint_ops); + let gen_hints = || { + chunk_and_generate( + &hint_ops, + max_rows.hint, + hint::generate_hint_trace, + #[cfg(feature = "disk-spill")] + storage_mode, + ) + }; let (mut cpus_slot, mut memws_slot, mut memw_aligneds_slot, mut memw_registers_slot) = (None, None, None, None); let (mut loads_slot, mut lts_slot, mut shifts_slot, mut muls_slot) = (None, None, None, None); let (mut dvrms_slot, mut branches_slot, mut bitwise_slot, mut decode_slot) = (None, None, None, None); - let (mut commit_slot, mut keccak_slot, mut keccak_rnd_slot, mut keccak_rc_slot) = + let (mut commits_slot, mut keccaks_slot, mut keccak_rnds_slot, mut keccak_rc_slot) = (None, None, None, None); let (mut pages_slot, mut register_slot, mut halt_slot) = (None, None, None); let (mut eqs_slot, mut bytewises_slot, mut stores_slot, mut cpu32s_slot) = (None, None, None, None); - let (mut ecsm_slot, mut ecdas_slot) = (None, None); - let mut hint_slot = None; + let (mut ecsms_slot, mut ecdases_slot) = (None, None); + let mut hints_slot = None; #[cfg(feature = "disk-spill")] let sequential = storage_mode == StorageMode::Disk || cfg!(not(feature = "parallel")); @@ -3576,19 +3631,19 @@ fn build_traces( spawn_into!(shifts_slot, gen_shifts); spawn_into!(dvrms_slot, gen_dvrms); spawn_into!(pages_slot, gen_pages); - spawn_into!(keccak_slot, gen_keccak); - spawn_into!(keccak_rnd_slot, gen_keccak_rnd); + spawn_into!(keccaks_slot, gen_keccaks); + spawn_into!(keccak_rnds_slot, gen_keccak_rnds); spawn_into!(keccak_rc_slot, gen_keccak_rc); - spawn_into!(commit_slot, gen_commit); + spawn_into!(commits_slot, gen_commits); spawn_into!(register_slot, gen_register); spawn_into!(halt_slot, gen_halt); spawn_into!(eqs_slot, gen_eqs); spawn_into!(bytewises_slot, gen_bytewises); spawn_into!(stores_slot, gen_stores); spawn_into!(cpu32s_slot, gen_cpu32s); - spawn_into!(ecsm_slot, gen_ecsm); - spawn_into!(ecdas_slot, gen_ecdas); - spawn_into!(hint_slot, gen_hint); + spawn_into!(ecsms_slot, gen_ecsms); + spawn_into!(ecdases_slot, gen_ecdases); + spawn_into!(hints_slot, gen_hints); }); } else { cpus_slot = Some(gen_cpus()); @@ -3603,9 +3658,9 @@ fn build_traces( branches_slot = Some(gen_branches()); bitwise_slot = Some(gen_bitwise()); decode_slot = Some(gen_decode()); - commit_slot = Some(gen_commit()); - keccak_slot = Some(gen_keccak()); - keccak_rnd_slot = Some(gen_keccak_rnd()); + commits_slot = Some(gen_commits()); + keccaks_slot = Some(gen_keccaks()); + keccak_rnds_slot = Some(gen_keccak_rnds()); keccak_rc_slot = Some(gen_keccak_rc()); pages_slot = Some(gen_pages()); register_slot = Some(gen_register()); @@ -3614,9 +3669,9 @@ fn build_traces( bytewises_slot = Some(gen_bytewises()); stores_slot = Some(gen_stores()); cpu32s_slot = Some(gen_cpu32s()); - ecsm_slot = Some(gen_ecsm()); - ecdas_slot = Some(gen_ecdas()); - hint_slot = Some(gen_hint()); + ecsms_slot = Some(gen_ecsms()); + ecdases_slot = Some(gen_ecdases()); + hints_slot = Some(gen_hints()); } const PHASE5_RAN: &str = "phase 5 generation ran in one of the branches above"; @@ -3638,10 +3693,9 @@ fn build_traces( let mut bitwise = bitwise_slot.expect(PHASE5_RAN); #[allow(unused_mut)] let mut decode = decode_slot.expect(PHASE5_RAN); - #[allow(unused_mut)] - let mut commit_trace = commit_slot.expect(PHASE5_RAN); - let keccak_trace = keccak_slot.expect(PHASE5_RAN); - let keccak_rnd_trace = keccak_rnd_slot.expect(PHASE5_RAN); + let commits = commits_slot.expect(PHASE5_RAN)?; + let keccaks = keccaks_slot.expect(PHASE5_RAN)?; + let keccak_rnds = keccak_rnds_slot.expect(PHASE5_RAN)?; let keccak_rc_trace = keccak_rc_slot.expect(PHASE5_RAN); #[allow(unused_mut)] let (mut pages, page_configs) = pages_slot.expect(PHASE5_RAN); @@ -3649,9 +3703,9 @@ fn build_traces( let mut register_trace = register_slot.expect(PHASE5_RAN); #[allow(unused_mut)] let mut halt_trace = halt_slot.expect(PHASE5_RAN); - let ecsm_trace = ecsm_slot.expect(PHASE5_RAN); - let ecdas_trace = ecdas_slot.expect(PHASE5_RAN); - let hint_trace = hint_slot.expect(PHASE5_RAN); + let ecsms = ecsms_slot.expect(PHASE5_RAN)?; + let ecdases = ecdases_slot.expect(PHASE5_RAN)?; + let hints = hints_slot.expect(PHASE5_RAN)?; // Fixed-size and per-page tables aren't built through `chunk_and_generate`, // so spill them here before returning. @@ -3665,10 +3719,6 @@ fn build_traces( .main_table .spill_to_disk() .map_err(|e| Error::Prover(format!("disk-spill decode: {e}")))?; - commit_trace - .main_table - .spill_to_disk() - .map_err(|e| Error::Prover(format!("disk-spill commit: {e}")))?; register_trace .main_table .spill_to_disk() @@ -3713,13 +3763,13 @@ fn build_traces( public_output_bytes, branches, halt: halt_trace, - commit: commit_trace, - keccak: keccak_trace, - keccak_rnd: keccak_rnd_trace, + commits, + keccaks, + keccak_rnds, keccak_rc: keccak_rc_trace, - ecsm: ecsm_trace, - ecdas: ecdas_trace, - hint: hint_trace, + ecsms, + ecdases, + hints, memw_registers, local_to_global, touched_memory_cells, @@ -3763,6 +3813,11 @@ pub struct TableLengths { pub dvrm_padded_rows: u64, pub branch_padded_rows: u64, pub commit_padded_rows: u64, + pub keccak_padded_rows: u64, + pub keccak_rnd_padded_rows: u64, + pub ecsm_padded_rows: u64, + pub ecdas_padded_rows: u64, + pub hint_padded_rows: u64, pub decode_rows: u64, pub unique_page_count: u64, pub cycle_count: u64, @@ -3802,6 +3857,9 @@ pub fn count_table_lengths( let mut dvrm_count = 0usize; let mut branch_count = 0usize; let mut commit_count = 0usize; + let mut keccak_count = 0usize; + let mut ecsm_count = 0usize; + let mut hint_count = 0usize; let mut current_commit_index = 0u32; let partition_memw = |op: &MemwOperation, @@ -3893,7 +3951,15 @@ pub fn count_table_lengths( .ok_or_else(|| Error::Execution("commit index exceeds u32 range".into()))?; } + if cpu_op.ecall_keccak { + keccak_count += 1; + } + if cpu_op.ecall_ecsm { + ecsm_count += 1; + } + if cpu_op.ecall_hint { + hint_count += 1; // Mirror `collect_hint_ops`: three register reads (a0/a1/a2) and four // 8-byte output writes go through the memory argument, plus the three LT // range-checks (selector < 3, in_addr and out_addr low limbs). Replaying it @@ -3967,10 +4033,20 @@ pub fn count_table_lengths( mul_padded_rows: padded_chunked_rows(mul_count, max_rows.mul), dvrm_padded_rows: padded_chunked_rows(dvrm_count, max_rows.dvrm), branch_padded_rows: padded_chunked_rows(branch_count, max_rows.branch), - commit_padded_rows: commit_count - .checked_next_power_of_two() - .unwrap_or(usize::MAX) - .max(4) as u64, + commit_padded_rows: padded_chunked_rows(commit_count, max_rows.commit), + keccak_padded_rows: padded_chunked_rows(keccak_count, max_rows.keccak), + // 24 rows per permutation, chunked on whole permutations. + keccak_rnd_padded_rows: padded_chunked_rows( + keccak_count * keccak_rnd::ROUNDS_PER_OP, + (max_rows.keccak_rnd / keccak_rnd::ROUNDS_PER_OP).max(1) * keccak_rnd::ROUNDS_PER_OP, + ), + ecsm_padded_rows: padded_chunked_rows(ecsm_count, max_rows.ecsm), + // Upper bound: an ECSM call emits at most `ecdas::MAX_STEPS_PER_ECSM` rows. + ecdas_padded_rows: padded_chunked_rows( + ecsm_count * ecdas::MAX_STEPS_PER_ECSM, + max_rows.ecdas, + ), + hint_padded_rows: padded_chunked_rows(hint_count, max_rows.hint), decode_rows, unique_page_count, cycle_count, @@ -4034,13 +4110,13 @@ impl Traces { register, branches, halt, - commit, - keccak, - keccak_rnd, + commits, + keccaks, + keccak_rnds, keccak_rc, - ecsm, - ecdas, - hint, + ecsms, + ecdases, + hints, memw_registers, eqs, bytewises, @@ -4083,7 +4159,9 @@ impl Traces { total += (t.num_rows() * BRANCH_COLS) as u64; } total += (halt.num_rows() * HALT_COLS) as u64; - total += (commit.num_rows() * COMMIT_COLS) as u64; + for t in commits { + total += (t.num_rows() * COMMIT_COLS) as u64; + } total += (register.num_rows() * (REGISTER_COLS - REGISTER_PREPROCESSED)) as u64; for t in pages { total += (t.num_rows() * (PAGE_COLS - PAGE_PREPROCESSED)) as u64; @@ -4091,8 +4169,12 @@ impl Traces { for t in memw_registers { total += (t.num_rows() * MEMW_R_COLS) as u64; } - total += (keccak.num_rows() * KECCAK_COLS) as u64; - total += (keccak_rnd.num_rows() * KECCAK_RND_COLS) as u64; + for t in keccaks { + total += (t.num_rows() * KECCAK_COLS) as u64; + } + for t in keccak_rnds { + total += (t.num_rows() * KECCAK_RND_COLS) as u64; + } total += (keccak_rc.num_rows() * (KECCAK_RC_COLS - KECCAK_RC_PRECOMPUTED)) as u64; for t in eqs { total += (t.num_rows() * EQ_COLS) as u64; @@ -4106,9 +4188,15 @@ impl Traces { for t in cpu32s { total += (t.num_rows() * CPU32_COLS) as u64; } - total += (ecsm.num_rows() * ECSM_COLS) as u64; - total += (ecdas.num_rows() * ECDAS_COLS) as u64; - total += (hint.num_rows() * HINT_COLS) as u64; + for t in ecsms { + total += (t.num_rows() * ECSM_COLS) as u64; + } + for t in ecdases { + total += (t.num_rows() * ECDAS_COLS) as u64; + } + for t in hints { + total += (t.num_rows() * HINT_COLS) as u64; + } total } @@ -4167,13 +4255,13 @@ impl Traces { register, branches, halt, - commit, - keccak, - keccak_rnd, + commits, + keccaks, + keccak_rnds, keccak_rc, - ecsm, - ecdas, - hint, + ecsms, + ecdases, + hints, memw_registers, eqs, bytewises, @@ -4216,7 +4304,9 @@ impl Traces { total += (t.num_rows() * n_branch) as u64; } total += (halt.num_rows() * n_halt) as u64; - total += (commit.num_rows() * n_commit) as u64; + for t in commits { + total += (t.num_rows() * n_commit) as u64; + } total += (register.num_rows() * n_register) as u64; for t in pages { total += (t.num_rows() * n_page) as u64; @@ -4224,8 +4314,12 @@ impl Traces { for t in memw_registers { total += (t.num_rows() * n_memw_r) as u64; } - total += (keccak.num_rows() * n_keccak) as u64; - total += (keccak_rnd.num_rows() * n_keccak_rnd) as u64; + for t in keccaks { + total += (t.num_rows() * n_keccak) as u64; + } + for t in keccak_rnds { + total += (t.num_rows() * n_keccak_rnd) as u64; + } total += (keccak_rc.num_rows() * n_keccak_rc) as u64; for t in eqs { total += (t.num_rows() * n_eq) as u64; @@ -4239,9 +4333,15 @@ impl Traces { for t in cpu32s { total += (t.num_rows() * n_cpu32) as u64; } - total += (ecsm.num_rows() * n_ecsm) as u64; - total += (ecdas.num_rows() * n_ecdas) as u64; - total += (hint.num_rows() * n_hint) as u64; + for t in ecsms { + total += (t.num_rows() * n_ecsm) as u64; + } + for t in ecdases { + total += (t.num_rows() * n_ecdas) as u64; + } + for t in hints { + total += (t.num_rows() * n_hint) as u64; + } total } @@ -4262,6 +4362,12 @@ impl Traces { bytewise: self.bytewises.len(), store: self.stores.len(), cpu32: self.cpu32s.len(), + keccak: self.keccaks.len(), + keccak_rnd: self.keccak_rnds.len(), + ecsm: self.ecsms.len(), + ecdas: self.ecdases.len(), + hint: self.hints.len(), + commit: self.commits.len(), } } diff --git a/prover/src/tests/accelerator_chunking_tests.rs b/prover/src/tests/accelerator_chunking_tests.rs new file mode 100644 index 000000000..bf9d8a9c2 --- /dev/null +++ b/prover/src/tests/accelerator_chunking_tests.rs @@ -0,0 +1,123 @@ +//! The accelerator chips' `max_rows` limits and the chunking that enforces them. + +use crate::tables::trace_builder::Traces; +use crate::tables::{MaxRowsConfig, commit, ecdas, ecsm, hint, keccak, keccak_rnd, max_rows}; +use crate::{Elf, Executor}; + +/// `main_cols + 3 × buses`, the cost model `max_rows` is derived from (see the +/// table on [`max_rows`]). Pinning it here makes a column or bus added to one of +/// these chips a failing test rather than a silently stale row limit. +#[test] +fn accelerator_max_rows_track_effective_width() { + fn effective_width(main_cols: usize, buses: usize) -> usize { + main_cols + 3 * buses + } + + let widths = [ + ( + "KECCAK", + effective_width(keccak::cols::NUM_COLUMNS, keccak::bus_interactions().len()), + 913, + ), + ( + "COMMIT", + effective_width(commit::cols::NUM_COLUMNS, commit::bus_interactions().len()), + 73, + ), + ( + "KECCAK_RND", + effective_width( + keccak_rnd::cols::NUM_COLUMNS, + keccak_rnd::bus_interactions().len(), + ), + 4573, + ), + ( + "ECSM", + effective_width(ecsm::cols::NUM_COLUMNS, ecsm::bus_interactions().len()), + 2404, + ), + ( + "ECDAS", + effective_width(ecdas::cols::NUM_COLUMNS, ecdas::bus_interactions().len()), + 1685, + ), + ( + "HINT", + effective_width(hint::cols::NUM_COLUMNS, hint::bus_interactions().len()), + 122, + ), + ]; + let drifted: Vec = widths + .iter() + .filter(|(_, actual, documented)| actual != documented) + .map(|(name, actual, documented)| format!("{name}: {documented} -> {actual}")) + .collect(); + assert!( + drifted.is_empty(), + "effective width changed ({}) — revisit those max_rows and the table in tables::max_rows", + drifted.join(", ") + ); +} + +/// A keccak-heavy run splits KECCAK and KECCAK_RND into several chunks, each +/// within its limit, and KECCAK_RND splits on whole permutations. +#[test] +fn keccak_traces_split_into_bounded_chunks() { + let elf_bytes = crate::test_utils::asm_elf_bytes("test_keccak_multi"); + let elf = Elf::load(&elf_bytes).expect("load ELF"); + let executor = Executor::new(&elf, vec![]).expect("create executor"); + let logs = executor.run().expect("run program").logs; + + // One permutation per chunk. + let limits = MaxRowsConfig { + keccak: 1, + keccak_rnd: keccak_rnd::ROUNDS_PER_OP, + ..Default::default() + }; + let traces = Traces::from_elf_and_logs_minimal(&elf, &logs, &limits, &[]).unwrap(); + + assert!( + traces.keccaks.len() > 1, + "expected the keccak calls to span several chunks, got {}", + traces.keccaks.len() + ); + assert_eq!( + traces.keccak_rnds.len(), + traces.keccaks.len(), + "one KECCAK_RND chunk per KECCAK chunk at one call per chunk" + ); + for t in &traces.keccak_rnds { + assert_eq!( + t.num_rows(), + keccak_rnd::ROUNDS_PER_OP.next_power_of_two(), + "a chunk holds exactly one permutation's rounds, padded" + ); + } +} + +/// The default limits leave a small program in one chunk per accelerator, so the +/// chunking adds no sub-proofs to the common case. +#[test] +fn default_limits_keep_small_programs_single_chunk() { + let elf_bytes = crate::test_utils::asm_elf_bytes("test_keccak"); + let elf = Elf::load(&elf_bytes).expect("load ELF"); + let executor = Executor::new(&elf, vec![]).expect("create executor"); + let logs = executor.run().expect("run program").logs; + + let traces = Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap(); + let counts = traces.table_counts(); + assert_eq!( + ( + counts.keccak, + counts.keccak_rnd, + counts.ecsm, + counts.ecdas, + counts.hint, + counts.commit + ), + (1, 1, 1, 1, 1, 1) + ); + assert!(traces.keccaks[0].num_rows() <= max_rows::KECCAK); + assert!(traces.keccak_rnds[0].num_rows() <= max_rows::KECCAK_RND); +} diff --git a/prover/src/tests/count_table_lengths_drift_tests.rs b/prover/src/tests/count_table_lengths_drift_tests.rs index 7337f0790..a4a97e9c3 100644 --- a/prover/src/tests/count_table_lengths_drift_tests.rs +++ b/prover/src/tests/count_table_lengths_drift_tests.rs @@ -47,9 +47,30 @@ fn assert_count_table_lengths_matches(elf: &Elf, logs: &[Log]) { "shift" ); assert_eq!( - predicted.commit_padded_rows, traces.commit.main_table.height as u64, + predicted.commit_padded_rows, + sum_heights(&traces.commits), "commit" ); + assert_eq!( + predicted.keccak_padded_rows, + sum_heights(&traces.keccaks), + "keccak" + ); + assert_eq!( + predicted.keccak_rnd_padded_rows, + sum_heights(&traces.keccak_rnds), + "keccak_rnd" + ); + assert_eq!( + predicted.ecsm_padded_rows, + sum_heights(&traces.ecsms), + "ecsm" + ); + assert_eq!( + predicted.hint_padded_rows, + sum_heights(&traces.hints), + "hint" + ); assert_eq!( predicted.decode_rows, traces.decode.main_table.height as u64, "decode" @@ -80,6 +101,13 @@ fn assert_count_table_lengths_matches(elf: &Elf, logs: &[Log]) { predicted.branch_padded_rows, sum_heights(&traces.branches) ); + // ECDAS rows depend on the scalar, so the prediction uses the per-call ceiling. + assert!( + predicted.ecdas_padded_rows >= sum_heights(&traces.ecdases), + "ecdas: predicted={} actual={}", + predicted.ecdas_padded_rows, + sum_heights(&traces.ecdases) + ); // Auxiliary scalars. assert_eq!(predicted.cycle_count, logs.len() as u64, "cycle_count"); diff --git a/prover/src/tests/mod.rs b/prover/src/tests/mod.rs index 9288cf2ac..426d92e9b 100644 --- a/prover/src/tests/mod.rs +++ b/prover/src/tests/mod.rs @@ -1,3 +1,5 @@ +#[cfg(test)] +pub mod accelerator_chunking_tests; #[cfg(all(test, feature = "disk-spill"))] pub mod auto_storage_tests; #[cfg(test)] diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index bbc8d2c63..45160ab4e 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -1327,9 +1327,9 @@ fn test_prove_hint_min_inconsistent_output_rejected() { Traces::from_elf_and_logs_minimal(&elf, &result.logs, &Default::default(), &[]).unwrap(); // Forge the low byte of the output on the (single) real HINT row. - let orig = *traces.hint.main_table.get(0, hint_cols::out(0)); + let orig = *traces.hints[0].main_table.get(0, hint_cols::out(0)); let forged = orig + FieldElement::::one(); - traces.hint.main_table.set(0, hint_cols::out(0), forged); + traces.hints[0].main_table.set(0, hint_cols::out(0), forged); assert!( !prove_and_verify_vm_minimal(&elf, &mut traces), @@ -1367,7 +1367,7 @@ fn hint_min_traces() -> (Elf, Traces) { fn test_prove_hint_min_forged_selector_rejected() { use crate::tables::hint::cols as hint_cols; let (elf, mut traces) = hint_min_traces(); - traces.hint.main_table.set( + traces.hints[0].main_table.set( 0, hint_cols::SEL_0, FieldElement::::from(3u64), @@ -1386,7 +1386,7 @@ fn test_prove_hint_min_forged_selector_rejected() { fn test_prove_hint_min_forged_input_address_rejected() { use crate::tables::hint::cols as hint_cols; let (elf, mut traces) = hint_min_traces(); - traces.hint.main_table.set( + traces.hints[0].main_table.set( 0, hint_cols::ADDR_IN_0, FieldElement::::from(0xFFFF_FFFFu64), @@ -1562,9 +1562,9 @@ fn test_prove_elfs_ecsm_forged_result_rejected() { Traces::from_elf_and_logs_minimal(&elf, &result.logs, &Default::default(), &[]).unwrap(); // Forge the low byte of xR on the (single) real ECSM row. - let orig = *traces.ecsm.main_table.get(0, ecsm_cols::xr(0)); + let orig = *traces.ecsms[0].main_table.get(0, ecsm_cols::xr(0)); let forged = orig + FieldElement::::one(); - traces.ecsm.main_table.set(0, ecsm_cols::xr(0), forged); + traces.ecsms[0].main_table.set(0, ecsm_cols::xr(0), forged); assert!( !prove_and_verify_vm_minimal(&elf, &mut traces), @@ -1590,7 +1590,7 @@ fn test_prove_elfs_ecsm_forged_ecdas_mu_rejected() { Traces::from_elf_and_logs_minimal(&elf, &result.logs, &Default::default(), &[]).unwrap(); // Row 0 is a real ECDAS step (µ=1); forge µ to a non-boolean value. - traces.ecdas.main_table.set( + traces.ecdases[0].main_table.set( 0, ecdas_cols::MU, FieldElement::::from(2u64), @@ -1629,7 +1629,7 @@ fn test_prove_elfs_keccak_unaligned_state_addr() { // value outside [0, 256). The new ARE_BYTES bus sender will emit this // value with multiplicity MU=1; the ARE_BYTES preprocessed table only // contains 0..256, so the bus cannot balance. - traces.keccak.main_table.set( + traces.keccaks[0].main_table.set( 0, keccak_cols::addr(1), FieldElement::::from(257u64), @@ -2750,6 +2750,12 @@ fn test_verify_rejects_zero_table_counts() { bytewise: 0, store: 0, cpu32: 0, + keccak: 0, + keccak_rnd: 0, + ecsm: 0, + ecdas: 0, + hint: 0, + commit: 0, }, ..vm_proof }; @@ -2825,6 +2831,12 @@ fn test_crafted_zero_count_proof_must_not_verify() { bytewise: 0, store: 0, cpu32: 0, + keccak: 0, + keccak_rnd: 0, + ecsm: 0, + ecdas: 0, + hint: 0, + commit: 0, }; let airs = VmAirs::new( &elf, diff --git a/prover/src/tests/statement_tests.rs b/prover/src/tests/statement_tests.rs index d3dafc0c7..2a7aea502 100644 --- a/prover/src/tests/statement_tests.rs +++ b/prover/src/tests/statement_tests.rs @@ -23,6 +23,12 @@ fn sample_counts() -> TableCounts { bytewise: 1, store: 1, cpu32: 1, + keccak: 1, + keccak_rnd: 1, + ecsm: 1, + ecdas: 1, + hint: 1, + commit: 1, } } From b7129b0f027df67d893c1f6445fe04b512d130fd Mon Sep 17 00:00:00 2001 From: Mario Rugiero Date: Mon, 10 Aug 2026 17:02:03 -0300 Subject: [PATCH 2/2] test(prover): cover the accelerator chunking that review found unverified - Drift tests only ran guests with zero keccak/ECSM calls, so the new projection formulas were exercised at count 0 only. `count_table_lengths_matches_keccak_trace` runs a three-permutation guest, making KECCAK and KECCAK_RND non-empty. - The chunking test stopped at trace shape; a split table's buses only matter once proved. It now proves and verifies the multi-chunk trace. - The ECDAS per-call bound backs a storage projection, so exceeding it must fail in release too: debug_assert -> assert with the offending count. - Revert CONTINUATION_GLOBAL_TAG to V2: the global statement absorbs no table counts, so this change does not alter it. --- prover/src/statement.rs | 2 +- prover/src/tables/trace_builder.rs | 9 ++++++++- prover/src/tests/accelerator_chunking_tests.rs | 10 +++++++++- prover/src/tests/count_table_lengths_drift_tests.rs | 9 +++++++++ prover/src/tests/prove_elfs_tests.rs | 2 +- 5 files changed, 28 insertions(+), 4 deletions(-) diff --git a/prover/src/statement.rs b/prover/src/statement.rs index c4ebd85f8..fa94808e8 100644 --- a/prover/src/statement.rs +++ b/prover/src/statement.rs @@ -168,7 +168,7 @@ pub(crate) fn absorb_statement_with_digest( /// Continuation domain tags. Distinct from the monolithic `DOMAIN_TAG` so a /// monolithic proof and a continuation proof can never share a transcript prefix. const CONTINUATION_EPOCH_TAG: &[u8] = b"LAMBDAVM_CONTINUATION_EPOCH_V3"; -const CONTINUATION_GLOBAL_TAG: &[u8] = b"LAMBDAVM_CONTINUATION_GLOBAL_V3"; +const CONTINUATION_GLOBAL_TAG: &[u8] = b"LAMBDAVM_CONTINUATION_GLOBAL_V2"; /// Statement bound into the cross-epoch **global** proof's transcript before /// Phase A: the ELF (so the global proof is program-bound), the epoch count (so a diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 61cacd473..442bbdbb1 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -942,7 +942,14 @@ fn collect_ecsm_ops( memory_state.write_bytes(addr, dword, 8, t + 2); } - debug_assert!(witness.steps.len() <= ecdas::MAX_STEPS_PER_ECSM); + // Not a debug_assert: `count_table_lengths` projects ECDAS from this bound, so a + // longer ladder must fail here rather than silently under-project storage. + assert!( + witness.steps.len() <= ecdas::MAX_STEPS_PER_ECSM, + "ECSM ladder emitted {} ECDAS rows, above the {} bound", + witness.steps.len(), + ecdas::MAX_STEPS_PER_ECSM + ); let ecdas_ops = witness .steps .iter() diff --git a/prover/src/tests/accelerator_chunking_tests.rs b/prover/src/tests/accelerator_chunking_tests.rs index bf9d8a9c2..cc8ebe5fc 100644 --- a/prover/src/tests/accelerator_chunking_tests.rs +++ b/prover/src/tests/accelerator_chunking_tests.rs @@ -75,7 +75,7 @@ fn keccak_traces_split_into_bounded_chunks() { keccak_rnd: keccak_rnd::ROUNDS_PER_OP, ..Default::default() }; - let traces = Traces::from_elf_and_logs_minimal(&elf, &logs, &limits, &[]).unwrap(); + let mut traces = Traces::from_elf_and_logs_minimal(&elf, &logs, &limits, &[]).unwrap(); assert!( traces.keccaks.len() > 1, @@ -94,6 +94,14 @@ fn keccak_traces_split_into_bounded_chunks() { "a chunk holds exactly one permutation's rounds, padded" ); } + + // The split has to survive the buses too: KECCAK↔KECCAK_RND↔KECCAK_RC and the + // memory argument are multiset arguments, so they balance across chunks or not + // at all. + assert!( + crate::tests::prove_elfs_tests::prove_and_verify_vm_minimal(&elf, &mut traces), + "a multi-chunk keccak trace must prove and verify" + ); } /// The default limits leave a small program in one chunk per accelerator, so the diff --git a/prover/src/tests/count_table_lengths_drift_tests.rs b/prover/src/tests/count_table_lengths_drift_tests.rs index a4a97e9c3..aaac02b21 100644 --- a/prover/src/tests/count_table_lengths_drift_tests.rs +++ b/prover/src/tests/count_table_lengths_drift_tests.rs @@ -127,6 +127,15 @@ fn count_table_lengths_matches_traces() { assert_count_table_lengths_matches(&elf, &logs); } +/// The accelerator predictions above are trivially satisfied at zero calls, and the +/// only guests reaching the other cases make none. This one makes three keccak +/// permutations, so KECCAK (one row per call) and KECCAK_RND (24) are non-empty. +#[test] +fn count_table_lengths_matches_keccak_trace() { + let (elf, logs, _) = run_asm_elf("test_keccak_multi"); + assert_count_table_lengths_matches(&elf, &logs); +} + /// The `hint` ecall routes three register reads (`a0`/`a1`/`a2`) and four output /// writes through the memory argument, plus two LT range-checks (selector, in_addr). /// `count_table_lengths` must replay all of that exactly, or `memw_register` (an diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index 45160ab4e..aa98782ab 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -47,7 +47,7 @@ type E = GoldilocksExtension; /// Includes: CPU + Bitwise + LT + MEMW + LOAD + DECODE + MUL + BRANCH + HALT + REGISTER + PAGEs /// /// Uses minimal bitwise (no full 2^20 preprocessed table) but DECODE is always preprocessed. -fn prove_and_verify_vm_minimal(elf: &Elf, traces: &mut Traces) -> bool { +pub(crate) fn prove_and_verify_vm_minimal(elf: &Elf, traces: &mut Traces) -> bool { let _ = env_logger::builder().is_test(true).try_init(); let proof_options = ProofOptions::default_test_options();