From d0d9fdcb75fa2d91b0e8957bccc14c4e757ee45f Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 8 Sep 2026 17:15:50 -0300 Subject: [PATCH 01/10] Fix four test premises the padding chunk hid --- prover/src/tests/prove_elfs_tests.rs | 60 ++++++++++++++++++++-------- 1 file changed, 44 insertions(+), 16 deletions(-) diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index e45c7b927..1b294efa1 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -42,6 +42,23 @@ type E = GoldilocksExtension; // Prover test helpers // ============================================================================= +/// Total MEMW rows across the table's chunks. A program that never reaches MEMW +/// gets no MEMW table at all, so a chunk count of zero is normal. +fn memw_rows(traces: &Traces) -> usize { + traces.memws.iter().map(|t| t.main_table.height).sum() +} + +/// Every `(chunk, row)` of the MEMW table, over however many chunks it has — +/// including none. +fn memw_chunk_rows( + traces: &Traces, +) -> impl Iterator, usize)> { + traces + .memws + .iter() + .flat_map(|t| (0..t.num_rows()).map(move |row| (t, row))) +} + /// Run multi_prove and multi_verify for all VM tables. /// /// Includes: CPU + Bitwise + LT + MEMW + LOAD + DECODE + MUL + BRANCH + HALT + REGISTER + PAGEs @@ -289,11 +306,11 @@ fn test_prove_elfs_sub_neg_result_fast() { Traces::from_logs_minimal(&logs, instructions.clone(), &Default::default()).unwrap(); println!( - "Fast SUB_NEG: CPU {} rows, Bitwise {} rows, MEMW {} tables ({} rows in first), REGISTER {} rows", + "Fast SUB_NEG: CPU {} rows, Bitwise {} rows, MEMW {} tables ({} rows), REGISTER {} rows", traces.cpus[0].main_table.height, traces.bitwise.main_table.height, traces.memws.len(), - traces.memws[0].main_table.height, + memw_rows(&traces), traces.register.main_table.height, ); @@ -938,8 +955,9 @@ fn test_prove_elfs_test_sb_sh_8() { let mut traces = Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap(); assert!( - !traces.memws.is_empty(), - "test_sb_sh_8 should produce MEMW rows for byte/halfword memory accesses" + !traces.stores.is_empty() && !traces.memw_aligneds.is_empty(), + "test_sb_sh_8 should produce STORE and MEMW_A rows for its byte/halfword \ + memory accesses (MEMW carries neither)" ); assert!( prove_and_verify_vm_minimal(&elf, &mut traces), @@ -1035,12 +1053,16 @@ fn test_prove_elfs_all_instructions_64() { // Includes SLT/SLTU instructions - need LT table println!( - "all_instructions_64 (fast): CPU {} rows, Bitwise {} rows, MEMW {} tables ({} rows in first), LOAD {} rows", + "all_instructions_64 (fast): CPU {} rows, Bitwise {} rows, MEMW {} tables ({} rows), LOAD {} rows", traces.cpus[0].main_table.height, traces.bitwise.main_table.height, traces.memws.len(), - traces.memws[0].main_table.height, - traces.loads[0].main_table.height + memw_rows(&traces), + traces + .loads + .iter() + .map(|t| t.main_table.height) + .sum::() ); assert!( prove_and_verify_vm_minimal(&elf, &mut traces), @@ -1813,11 +1835,10 @@ fn test_debug_memory_bus_tokens() { let traces = Traces::from_logs_minimal(&logs, instructions.clone(), &Default::default()).unwrap(); - let memw = &traces.memws[0]; // Small test: single MEMW chunk println!("DEBUG TABLE SIZES:"); println!( " MEMW: {} rows ({} tables)", - memw.num_rows(), + memw_rows(&traces), traces.memws.len() ); println!(" REGISTER: {} rows", traces.register.num_rows()); @@ -1831,7 +1852,7 @@ fn test_debug_memory_bus_tokens() { // === MEMW tokens (for register rows only) === println!("\n=== MEMW Memory Bus Tokens (register rows) ==="); - for row in 0..memw.num_rows() { + for (memw, row) in memw_chunk_rows(&traces) { let is_reg = memw.main_table.get(row, memw_cols::IS_REGISTER).to_raw(); if is_reg == 0 { continue; // Skip memory rows (multiplicity = 0) @@ -1971,7 +1992,7 @@ fn test_debug_memory_bus_tokens() { let mut total_sum: f64 = 0.0; // MEMW tokens - for row in 0..memw.num_rows() { + for (memw, row) in memw_chunk_rows(&traces) { let is_reg = memw.main_table.get(row, memw_cols::IS_REGISTER).to_raw(); if is_reg == 0 { continue; @@ -2085,11 +2106,10 @@ fn test_debug_memory_tokens_sb_sh() { ) .unwrap(); - let memw = &traces.memws[0]; // Small test: single MEMW chunk println!("DEBUG: test_sb_sh_8 Memory bus tokens (FULL)"); println!( " MEMW rows: {} ({} tables)", - memw.num_rows(), + memw_rows(&traces), traces.memws.len() ); println!(" REGISTER rows: {}", traces.register.num_rows()); @@ -2153,7 +2173,7 @@ fn test_debug_memory_tokens_sb_sh() { println!("\n=== MEMW Memory Bus Tokens (ALL rows) ==="); let mut memw_register_rows = 0; let mut memw_memory_rows = 0; - for row in 0..memw.num_rows() { + for (memw, row) in memw_chunk_rows(&traces) { let is_reg = memw.main_table.get(row, memw_cols::IS_REGISTER).to_raw(); // Count row types @@ -2781,7 +2801,11 @@ fn test_verify_rejects_zero_cpu_count() { assert!(result.is_err(), "Got {:?}", result); } -/// Verify rejects table_counts with memw=0. +/// Verify rejects a `table_counts` that under-reports a table the proof carries: +/// the counts drive the AIR set, so they must match the sub-proof count. +/// +/// MEMW_A rather than MEMW because `sub` reaches no MEMW rows at all, and a +/// count that is already zero is not something to tamper with. #[test] fn test_verify_rejects_zero_memw_count() { let elf_bytes = crate::test_utils::asm_elf_bytes("sub"); @@ -2789,10 +2813,14 @@ fn test_verify_rejects_zero_memw_count() { let vm_proof = crate::prove_with_options(&elf_bytes, &proof_options, &Default::default()) .expect("Prover should succeed on valid program"); + assert!( + vm_proof.table_counts.memw_aligned > 0, + "the program must carry the table this test zeroes out" + ); let tampered_proof = crate::VmProof { table_counts: crate::TableCounts { - memw: 0, + memw_aligned: 0, ..vm_proof.table_counts.clone() }, ..vm_proof From a1477cf24f2668120ccf154b55229e60b0fef419 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 8 Sep 2026 17:15:53 -0300 Subject: [PATCH 02/10] Leave unused chip tables out of the proof --- prover/src/lib.rs | 40 ++--- prover/src/tables/trace_builder.rs | 108 +++++++---- prover/src/tests/mod.rs | 3 + prover/src/tests/skip_empty_tables_tests.rs | 187 ++++++++++++++++++++ 4 files changed, 287 insertions(+), 51 deletions(-) create mode 100644 prover/src/tests/skip_empty_tables_tests.rs diff --git a/prover/src/lib.rs b/prover/src/lib.rs index 79ef4c715..b5ed2de9a 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -125,31 +125,29 @@ impl TableCounts { + self.cpu32 } - /// Validate that all required tables have at least one chunk. + /// Validate that the structurally-required tables have at least one chunk. /// - /// A zero count for any table would remove its constraints from verification, - /// allowing a malicious prover to bypass soundness checks. + /// CPU drives the run and MEMW_R carries the register file, so a proof + /// without them describes no execution at all and is rejected here. + /// + /// Every other chip is allowed a zero count: an epoch that runs no + /// multiplication has no MUL table, and paying a padded sub-proof for it + /// costs a full commitment, FRI chain and OOD opening set. + /// + /// What keeps a zero count honest is the LogUp bus, not this check. A chip + /// influences the run only through its bus interactions, and no chip carries + /// boundary constraints of its own, so a chip with no rows contributes zero + /// to the bus and removing it changes nothing. A prover that omits a table + /// whose operations *did* execute leaves the CPU's sends unmatched, and the + /// bus-balance check — summed over the tables that are present — rejects the + /// proof. That argument needs each omitted table to be a bus participant; + /// `every_table_participates_in_the_bus` pins it down for the whole AIR set. pub fn validate(&self) -> Result<(), Error> { - let checks = [ - ("cpu", self.cpu), - ("lt", self.lt), - ("memw", self.memw), - ("memw_aligned", self.memw_aligned), - ("load", self.load), - ("mul", self.mul), - ("dvrm", self.dvrm), - ("shift", self.shift), - ("branch", self.branch), - ("memw_register", self.memw_register), - ("eq", self.eq), - ("bytewise", self.bytewise), - ("store", self.store), - ("cpu32", self.cpu32), - ]; - for (name, count) in checks { + let required = [("cpu", self.cpu), ("memw_register", self.memw_register)]; + for (name, count) in required { if count == 0 { return Err(Error::InvalidTableCounts(format!( - "{name} count is 0 — every table must have at least 1 chunk" + "{name} count is 0 — required table must have at least 1 chunk" ))); } } diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index d3560826a..9344ae095 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -2919,9 +2919,10 @@ struct CollectedOps { hint_ops: Vec, } -/// Chunk raw ops and generate one trace table per chunk. When `storage_mode` -/// is `Disk`, each chunk's main table is spilled to mmap before the next chunk -/// is built so peak heap usage stays bounded. +/// Chunk raw ops and generate one trace table per chunk, padding an empty `ops` +/// to a single chunk so the table is always present in the proof. +/// +/// For tables that may be omitted entirely, use [`chunk_and_generate_optional`]. fn chunk_and_generate( ops: &[T], max_rows: usize, @@ -2933,6 +2934,46 @@ fn chunk_and_generate( } else { ops.chunks(max_rows).collect() }; + generate_chunks( + op_chunks, + generate, + #[cfg(feature = "disk-spill")] + storage_mode, + ) +} + +/// Like [`chunk_and_generate`], but an empty `ops` yields no table at all: the +/// chip is left out of the proof instead of costing a padded sub-proof. +/// `slice::chunks` already yields nothing for an empty slice, so this is the +/// plain chunking with no special case. +/// +/// Sound because a chip contributes to the run only through its LogUp bus, and a +/// chip with no rows contributes zero. A prover that omits a table whose ops did +/// execute leaves its counterparty's sends unmatched, and the bus-balance check +/// over the tables that *are* present rejects the proof. See +/// `TableCounts::validate`. +fn chunk_and_generate_optional( + ops: &[T], + max_rows: usize, + generate: impl Fn(&[T]) -> TraceTable + Send + Sync, + #[cfg(feature = "disk-spill")] storage_mode: StorageMode, +) -> Result>, Error> { + generate_chunks( + ops.chunks(max_rows).collect(), + generate, + #[cfg(feature = "disk-spill")] + storage_mode, + ) +} + +/// Generate one trace table per already-chunked op slice. When `storage_mode` is +/// `Disk`, each chunk's main table is spilled to mmap before the next chunk is +/// built so peak heap usage stays bounded. +fn generate_chunks( + op_chunks: Vec<&[T]>, + generate: impl Fn(&[T]) -> TraceTable + Send + Sync, + #[cfg(feature = "disk-spill")] storage_mode: StorageMode, +) -> Result>, Error> { // Disk mode generates one chunk at a time so each spills before the next // allocates, keeping trace memory bounded. #[cfg(feature = "disk-spill")] @@ -3363,7 +3404,7 @@ fn build_traces( ) }; let gen_memws = || { - chunk_and_generate( + chunk_and_generate_optional( &memw_ops, max_rows.memw, memw::generate_memw_trace, @@ -3372,7 +3413,7 @@ fn build_traces( ) }; let gen_memw_aligneds = || { - chunk_and_generate( + chunk_and_generate_optional( &memw_aligned_ops, max_rows.memw_aligned, memw_aligned::generate_memw_aligned_trace, @@ -3392,7 +3433,7 @@ fn build_traces( ) }; let gen_loads = || { - chunk_and_generate( + chunk_and_generate_optional( &load_ops, max_rows.load, load::generate_load_trace, @@ -3401,7 +3442,7 @@ fn build_traces( ) }; let gen_lts = || { - chunk_and_generate( + chunk_and_generate_optional( <_ops, max_rows.lt, lt::generate_lt_trace, @@ -3410,7 +3451,7 @@ fn build_traces( ) }; let gen_shifts = || { - chunk_and_generate( + chunk_and_generate_optional( &shift_ops, max_rows.shift, shift::generate_shift_trace, @@ -3419,7 +3460,7 @@ fn build_traces( ) }; let gen_muls = || { - chunk_and_generate( + chunk_and_generate_optional( &mul_ops, max_rows.mul, mul::generate_mul_trace, @@ -3428,7 +3469,7 @@ fn build_traces( ) }; let gen_dvrms = || { - chunk_and_generate( + chunk_and_generate_optional( &dvrm_ops, max_rows.dvrm, dvrm::generate_dvrm_trace, @@ -3437,7 +3478,7 @@ fn build_traces( ) }; let gen_branches = || { - chunk_and_generate( + chunk_and_generate_optional( &branch_ops, max_rows.branch, branch::generate_branch_trace, @@ -3445,11 +3486,10 @@ fn build_traces( storage_mode, ) }; - // Auxiliary ALU / memory / CPU32 dispatch chips. Not yet driven by the CPU - // dispatch, so they are generated empty — one padded (μ=0) chunk each, which - // contributes nothing to any bus. + // Auxiliary ALU / memory / CPU32 dispatch chips, each filtered out of the CPU + // ops above. let gen_eqs = || { - chunk_and_generate::( + chunk_and_generate_optional::( &eq_ops, max_rows.eq, eq::generate_eq_trace, @@ -3458,7 +3498,7 @@ fn build_traces( ) }; let gen_bytewises = || { - chunk_and_generate::( + chunk_and_generate_optional::( &bytewise_ops, max_rows.bytewise, bytewise::generate_bytewise_trace, @@ -3467,7 +3507,7 @@ fn build_traces( ) }; let gen_stores = || { - chunk_and_generate::( + chunk_and_generate_optional::( &store_ops, max_rows.store, store::generate_store_trace, @@ -3476,7 +3516,7 @@ fn build_traces( ) }; let gen_cpu32s = || { - chunk_and_generate::( + chunk_and_generate_optional::( &cpu32_ops, max_rows.cpu32, cpu32::generate_cpu32_trace, @@ -3730,14 +3770,19 @@ fn build_traces( }) } -/// Padded row count after chunking. +/// Padded row count after chunking, for a table that is always present: an +/// empty op list still allocates one 4-row padded chunk. #[cfg(feature = "disk-spill")] fn padded_chunked_rows(ops_count: usize, max_rows: usize) -> u64 { + padded_chunked_rows_optional(ops_count, max_rows).max(4) +} + +/// Padded row count after chunking, for a table left out of the proof when +/// unused. Mirrors [`chunk_and_generate_optional`]: no ops, no rows. +#[cfg(feature = "disk-spill")] +fn padded_chunked_rows_optional(ops_count: usize, max_rows: usize) -> u64 { // `max_rows <= 0` would loop forever. Called internally with const values > 0. assert!(max_rows > 0, "max_rows must be positive"); - if ops_count == 0 { - return 4; // empty-chunk tables still allocate one 4-row padded chunk - } let mut total: u64 = 0; let mut remaining = ops_count; while remaining > 0 { @@ -3958,15 +4003,18 @@ pub fn count_table_lengths( Ok(TableLengths { cpu_padded_rows: padded_chunked_rows(cpu_count, max_rows.cpu), - memw_padded_rows: padded_chunked_rows(memw_count, max_rows.memw), - memw_aligned_padded_rows: padded_chunked_rows(memw_aligned_count, max_rows.memw_aligned), + memw_padded_rows: padded_chunked_rows_optional(memw_count, max_rows.memw), + memw_aligned_padded_rows: padded_chunked_rows_optional( + memw_aligned_count, + max_rows.memw_aligned, + ), memw_register_padded_rows: padded_chunked_rows(memw_register_count, max_rows.memw_register), - load_padded_rows: padded_chunked_rows(load_count, max_rows.load), - lt_padded_rows: padded_chunked_rows(lt_count, max_rows.lt), - shift_padded_rows: padded_chunked_rows(shift_count, max_rows.shift), - 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), + load_padded_rows: padded_chunked_rows_optional(load_count, max_rows.load), + lt_padded_rows: padded_chunked_rows_optional(lt_count, max_rows.lt), + shift_padded_rows: padded_chunked_rows_optional(shift_count, max_rows.shift), + mul_padded_rows: padded_chunked_rows_optional(mul_count, max_rows.mul), + dvrm_padded_rows: padded_chunked_rows_optional(dvrm_count, max_rows.dvrm), + branch_padded_rows: padded_chunked_rows_optional(branch_count, max_rows.branch), commit_padded_rows: commit_count .checked_next_power_of_two() .unwrap_or(usize::MAX) diff --git a/prover/src/tests/mod.rs b/prover/src/tests/mod.rs index 9288cf2ac..73ff6ee45 100644 --- a/prover/src/tests/mod.rs +++ b/prover/src/tests/mod.rs @@ -86,6 +86,9 @@ pub mod recursion_soundness_gap_poc; pub mod register_tests; #[cfg(test)] pub mod shift_tests; + +#[cfg(test)] +pub mod skip_empty_tables_tests; #[cfg(test)] pub mod statement_tests; #[cfg(test)] diff --git a/prover/src/tests/skip_empty_tables_tests.rs b/prover/src/tests/skip_empty_tables_tests.rs new file mode 100644 index 000000000..239c815a3 --- /dev/null +++ b/prover/src/tests/skip_empty_tables_tests.rs @@ -0,0 +1,187 @@ +//! A chip the run never reaches is left out of the proof entirely. +//! +//! Every table used to cost a padded sub-proof — a full commitment, FRI chain +//! and OOD opening set — whether or not the program executed a single one of its +//! operations. These tests cover both directions of dropping them: an unused +//! chip is absent and the proof still verifies, and a chip whose operations +//! *did* run cannot be dropped, because the LogUp bus no longer balances. + +use crypto::fiat_shamir::default_transcript::DefaultTranscript; +use stark::proof::options::ProofOptions; +use stark::proof::view::StarkProofView; +use stark::verifier::{IsStarkVerifier, Verifier}; + +use executor::elf::Elf; + +use crate::VmAirs; +use crate::tables::trace_builder::Traces; +use crate::test_utils::{E, F, multi_prove_ram, run_asm_elf}; + +/// Prove and verify `traces` with the AIR set that its own table counts +/// describe, so an absent chip is absent on both sides — exactly how the +/// production prover and verifier reconstruct the shape. +fn prove_and_verify(elf: &Elf, traces: &mut Traces) -> bool { + let proof_options = ProofOptions::default_test_options(); + let table_counts = traces.table_counts(); + let airs = VmAirs::new( + elf, + &proof_options, + true, + &traces.page_configs, + &table_counts, + None, + true, + None, + None, + None, + ); + + let multi_proof = match multi_prove_ram( + airs.air_trace_pairs(traces), + &mut DefaultTranscript::::new(&[]), + ) { + Ok(proof) => proof, + Err(_) => return false, + }; + let views: Vec> = multi_proof + .proofs + .iter() + .map(StarkProofView::Owned) + .collect(); + + let expected_bus_balance = match crate::compute_expected_commit_bus_balance_view( + &airs.air_refs(), + &views, + &traces.public_output_bytes, + 0, + &mut DefaultTranscript::::new(&[]), + ) { + Some(balance) => balance, + None => return false, + }; + + Verifier::multi_verify_views( + &airs.air_refs(), + &views, + &mut DefaultTranscript::::new(&[]), + &expected_bus_balance, + ) +} + +/// The premise `TableCounts::validate` now leans on: a chip influences the run +/// only through its bus interactions, so an absent chip is caught by the +/// bus-balance check. A table with no interactions is skipped by that sum +/// (`Verifier::multi_verify` filters on `has_trace_interaction`), so adding one +/// would let a prover drop it unnoticed. Nothing in the AIR set may be in that +/// position. +#[test] +fn every_table_participates_in_the_bus() { + let (elf, logs, _instructions) = run_asm_elf("test_mul_8"); + let traces = Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap(); + let table_counts = traces.table_counts(); + let airs = VmAirs::new( + &elf, + &ProofOptions::default_test_options(), + true, + &traces.page_configs, + &table_counts, + None, + true, + None, + None, + None, + ); + + let without_bus: Vec<&str> = airs + .air_refs() + .iter() + .filter(|air| !air.has_trace_interaction()) + .map(|air| air.name()) + .collect(); + assert!( + without_bus.is_empty(), + "these tables carry no bus interactions, so dropping them would go undetected: {without_bus:?}" + ); +} + +/// A program that never multiplies or divides gets no MUL and no DVRM table, +/// and still verifies. +#[test] +fn a_run_without_multiplication_omits_the_mul_table() { + let (elf, logs, _instructions) = run_asm_elf("xori"); + let mut traces = + Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap(); + + let table_counts = traces.table_counts(); + assert_eq!(table_counts.mul, 0, "xori executes no multiplication"); + assert_eq!(table_counts.dvrm, 0, "xori executes no division"); + assert!(traces.muls.is_empty()); + assert!(traces.dvrms.is_empty()); + assert!( + table_counts.validate().is_ok(), + "zero counts on unused chips are legitimate" + ); + + assert!( + prove_and_verify(&elf, &mut traces), + "a proof without the unused chips must still verify" + ); +} + +/// The forgery the relaxed `validate` has to survive: keep the CPU trace that +/// executed the multiplications, drop the MUL table, and declare `mul = 0`. +/// Both sides then agree on the reduced shape — the transcript replays, every +/// sub-proof is internally sound — and the only thing left to catch it is the +/// bus balance, whose sum over the *present* tables no longer matches once the +/// CPU's MUL sends have no receiver. +#[test] +fn omitting_a_table_whose_ops_ran_fails_the_bus_balance() { + let (elf, logs, _instructions) = run_asm_elf("test_mul_8"); + let mut traces = + Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap(); + assert!( + !traces.muls.is_empty(), + "test_mul_8 must exercise MUL for this to be a forgery" + ); + + assert!( + prove_and_verify(&elf, &mut traces), + "the honest proof must verify first, or the negative below proves nothing" + ); + + traces.muls.clear(); + assert_eq!(traces.table_counts().mul, 0); + assert!( + traces.table_counts().validate().is_ok(), + "validate deliberately lets this through — the bus is what rejects it" + ); + + assert!( + !prove_and_verify(&elf, &mut traces), + "dropping MUL while the CPU still sends MUL requests must not verify" + ); +} + +/// What `validate` still refuses: a proof with no CPU describes no execution, +/// and one with no register file has nothing to carry register state. +#[test] +fn validate_still_requires_cpu_and_the_register_file() { + let (elf, logs, _instructions) = run_asm_elf("test_mul_8"); + let traces = Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap(); + let honest = traces.table_counts(); + assert!(honest.validate().is_ok()); + + let mut no_cpu = honest.clone(); + no_cpu.cpu = 0; + assert!( + no_cpu.validate().is_err(), + "a proof with no CPU is rejected" + ); + + let mut no_registers = honest.clone(); + no_registers.memw_register = 0; + assert!( + no_registers.validate().is_err(), + "a proof with no register file is rejected" + ); +} From faeca76866ac73e75996ce12e48d5270393677a7 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 8 Sep 2026 18:33:22 -0300 Subject: [PATCH 03/10] Prove epochs decide table presence on their own --- prover/src/continuation.rs | 94 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 94 insertions(+) diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index df764ff18..9b4f8e5d6 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -1958,6 +1958,100 @@ mod tests { } // A memory-heavy multi-epoch continuation. `all_loadstore_32` is ~34 cycles, so + /// Each epoch drops the chips it never reaches, and it decides that on its + /// own: a table missing from one epoch still shows up in another that does + /// use it. The skip is not a property of the run, it is a property of the + /// epoch — computing it over the whole run instead would drag every table + /// used anywhere into every epoch. + #[test] + fn table_presence_is_decided_per_epoch() { + let _ = env_logger::builder().is_test(true).try_init(); + let elf_bytes = asm_elf_bytes("all_loadstore_32"); + let epoch_size_log2 = 3; + let opts = ProofOptions::default_test_options(); + + let bundle = prove_continuation(&elf_bytes, &[], epoch_size_log2, &opts).unwrap(); + // Guard against silent degradation: one epoch cannot disagree with another. + assert!( + bundle.epochs.len() >= 2, + "need at least two epochs, got {}", + bundle.epochs.len() + ); + + // `(name, count)` per epoch, in a fixed order so the rows line up. + let per_epoch: Vec> = bundle + .epochs + .iter() + .map(|e| { + let c = &e.table_counts; + vec![ + ("lt", c.lt), + ("memw", c.memw), + ("memw_aligned", c.memw_aligned), + ("load", c.load), + ("mul", c.mul), + ("dvrm", c.dvrm), + ("shift", c.shift), + ("branch", c.branch), + ("eq", c.eq), + ("bytewise", c.bytewise), + ("store", c.store), + ("cpu32", c.cpu32), + ] + }) + .collect(); + let layout = || { + per_epoch + .iter() + .enumerate() + .map(|(i, row)| { + let present: Vec<&str> = row + .iter() + .filter(|(_, n)| *n > 0) + .map(|(t, _)| *t) + .collect(); + format!("epoch {i}: {present:?}") + }) + .collect::>() + .join("\n ") + }; + + // Something is actually being skipped, or the rest proves nothing. + assert!( + per_epoch.iter().any(|row| row.iter().any(|(_, n)| *n == 0)), + "no epoch skipped any table:\n {}", + layout() + ); + + // And the epochs disagree: some table is in one and out of another. + let disagreeing: Vec<&str> = per_epoch[0] + .iter() + .enumerate() + .filter(|(i, (_, first))| { + per_epoch + .iter() + .any(|row| (row[*i].1 == 0) != (*first == 0)) + }) + .map(|(_, (name, _))| *name) + .collect(); + assert!( + !disagreeing.is_empty(), + "every epoch carries the same tables, so per-epoch granularity is \ + untested here — pick a program or epoch size that varies:\n {}", + layout() + ); + println!("tables present in some epochs but not others: {disagreeing:?}"); + println!(" {}", layout()); + + // The mixed-shape bundle has to verify end to end. + assert!( + verify_continuation(&elf_bytes, &bundle, &opts) + .unwrap() + .is_some(), + "a bundle whose epochs carry different table sets must still verify" + ); + } + // `epoch_size_log2 = 3` (8 cycles) yields several intermediate epochs (each an // exact power-of-two cycle count → no CPU padding rows) plus a final epoch. #[test] From c119153b4962f9cdcdbd1c01701ef7fb2b57f408 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 8 Sep 2026 18:33:26 -0300 Subject: [PATCH 04/10] Skip the accelerator tables a run never calls --- prover/src/continuation.rs | 6 + prover/src/lib.rs | 134 ++++++--- prover/src/statement.rs | 16 +- prover/src/tables/trace_builder.rs | 259 ++++++++++++------ .../tests/count_table_lengths_drift_tests.rs | 3 +- prover/src/tests/prove_elfs_tests.rs | 28 +- prover/src/tests/skip_empty_tables_tests.rs | 72 +++++ prover/src/tests/statement_tests.rs | 6 + 8 files changed, 397 insertions(+), 127 deletions(-) diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index 9b4f8e5d6..f90a9062e 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -1997,6 +1997,12 @@ mod tests { ("bytewise", c.bytewise), ("store", c.store), ("cpu32", c.cpu32), + ("keccak", c.keccak), + ("keccak_rnd", c.keccak_rnd), + ("ecsm", c.ecsm), + ("ecdas", c.ecdas), + ("hint", c.hint), + ("commit", c.commit), ] }) .collect(); diff --git a/prover/src/lib.rs b/prover/src/lib.rs index b5ed2de9a..7b2cfe0a2 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -81,9 +81,10 @@ 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. The +/// accelerator chips are counted instead — a run that never calls one carries +/// no table for it. +pub const FIXED_TABLE_COUNT: usize = 5; /// Number of chunks for each split table. /// The verifier needs this to reconstruct matching AIRs. @@ -104,6 +105,15 @@ pub struct TableCounts { pub bytewise: usize, pub store: usize, pub cpu32: usize, + // Accelerator chips. One table each when the run reaches them, none when it + // does not; they are counted rather than fixed so the count can later become + // a real chunk count without moving the statement encoding again. + pub keccak: usize, + pub keccak_rnd: usize, + pub ecsm: usize, + pub ecdas: usize, + pub hint: usize, + pub commit: usize, } impl TableCounts { @@ -123,6 +133,12 @@ impl TableCounts { + self.bytewise + self.store + self.cpu32 + + self.keccak + + self.keccak_rnd + + self.ecsm + + self.ecdas + + self.hint + + self.commit } /// Validate that the structurally-required tables have at least one chunk. @@ -514,13 +530,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, @@ -540,18 +556,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, &())); @@ -615,18 +643,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()); @@ -784,16 +824,44 @@ 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( @@ -908,13 +976,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..fa94808e8 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,7 +167,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_V2"; +const CONTINUATION_EPOCH_TAG: &[u8] = b"LAMBDAVM_CONTINUATION_EPOCH_V3"; const CONTINUATION_GLOBAL_TAG: &[u8] = b"LAMBDAVM_CONTINUATION_GLOBAL_V2"; /// Statement bound into the cross-epoch **global** proof's transcript before diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 9344ae095..e2bbafabe 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -2852,26 +2852,30 @@ 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 table for write syscall (byte-by-byte commit with recursive bus). + /// Empty when the run commits no bytes. + pub commits: Vec>, - /// KECCAK core table (one row per keccak permutation call) - pub keccak: TraceTable, + /// KECCAK core table (one row per keccak permutation call). Empty when the + /// run makes no keccak call. + pub keccaks: Vec>, - /// KECCAK_RND round table (24 rows per keccak call) - pub keccak_rnd: TraceTable, + /// KECCAK_RND round table (24 rows per keccak call). Empty alongside KECCAK. + 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 table (one row per scalar-multiplication ecall). Empty when the + /// run makes no ECSM call. + pub ecsms: Vec>, - /// ECDAS double/add table (variable rows per ecall) - pub ecdas: TraceTable, + /// ECDAS double/add table (variable rows per ecall). Empty alongside ECSM. + pub ecdases: Vec>, - /// HINT table (one row per non-constraining hint ecall). - pub hint: TraceTable, + /// HINT table (one row per non-constraining hint ecall). Empty when the run + /// makes no hint ecall. + pub hints: Vec>, /// MEMW_R register-only fast-path traces (split into chunks of max_rows::MEMW_R) pub memw_registers: Vec>, @@ -2966,6 +2970,26 @@ fn chunk_and_generate_optional( ) } +/// Generate a single trace table for `ops`, or none at all when `ops` is empty. +/// +/// The accelerator chips are not chunked: one call means one table. What they do +/// share with the chunked chips is that an empty op list should cost nothing, so +/// this returns an empty `Vec` and the table drops out of the proof. Soundness +/// rests on the same LogUp argument as [`chunk_and_generate_optional`]. +fn generate_optional( + ops: &[T], + generate: impl Fn(&[T]) -> TraceTable + Send + Sync, + #[cfg(feature = "disk-spill")] storage_mode: StorageMode, +) -> Result>, Error> { + let op_chunks: Vec<&[T]> = if ops.is_empty() { vec![] } else { vec![ops] }; + generate_chunks( + op_chunks, + generate, + #[cfg(feature = "disk-spill")] + storage_mode, + ) +} + /// Generate one trace table per already-chunked op slice. When `storage_mode` is /// `Disk`, each chunk's main table is spilled to mmap before the next chunk is /// built so peak heap usage stays bounded. @@ -3540,9 +3564,23 @@ 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 = || { + generate_optional( + &commit_ops, + commit::generate_commit_trace, + #[cfg(feature = "disk-spill")] + storage_mode, + ) + }; + let gen_keccaks = || { + generate_optional( + &keccak_ops, + 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 { @@ -3551,7 +3589,12 @@ fn build_traces( output: op.output, }) .collect(); - keccak_rnd::generate_keccak_rnd_trace(&keccak_rnd_ops) + generate_optional( + &keccak_rnd_ops, + 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(); @@ -3570,23 +3613,44 @@ 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 = || { + generate_optional( + &ecsm_ops, + ecsm::generate_ecsm_trace, + #[cfg(feature = "disk-spill")] + storage_mode, + ) + }; + let gen_ecdases = || { + generate_optional( + &ecdas_ops, + 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 = || { + generate_optional( + &hint_ops, + 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")); @@ -3616,19 +3680,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()); @@ -3643,9 +3707,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()); @@ -3654,9 +3718,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"; @@ -3678,10 +3742,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); @@ -3689,9 +3752,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. @@ -3705,10 +3768,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() @@ -3753,13 +3812,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, @@ -4015,10 +4074,14 @@ pub fn count_table_lengths( mul_padded_rows: padded_chunked_rows_optional(mul_count, max_rows.mul), dvrm_padded_rows: padded_chunked_rows_optional(dvrm_count, max_rows.dvrm), branch_padded_rows: padded_chunked_rows_optional(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: if commit_count == 0 { + 0 + } else { + commit_count + .checked_next_power_of_two() + .unwrap_or(usize::MAX) + .max(4) as u64 + }, decode_rows, unique_page_count, cycle_count, @@ -4081,10 +4144,10 @@ impl Traces { // place (L2G range-check lookups) after the build, which would leave // a stale device copy to be committed. tables.push(&mut self.decode); - tables.push(&mut self.keccak); - tables.push(&mut self.keccak_rnd); - tables.push(&mut self.ecsm); - tables.push(&mut self.ecdas); + tables.extend(self.keccaks.iter_mut()); + tables.extend(self.keccak_rnds.iter_mut()); + tables.extend(self.ecsms.iter_mut()); + tables.extend(self.ecdases.iter_mut()); let bytes_of = |t: &TraceTable| { t.num_rows() * t.num_main_columns * 8 @@ -4159,13 +4222,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, @@ -4208,7 +4271,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; @@ -4216,8 +4281,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; @@ -4231,9 +4300,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 } @@ -4292,13 +4367,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, @@ -4341,7 +4416,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; @@ -4349,8 +4426,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; @@ -4364,9 +4445,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 } @@ -4387,6 +4474,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/count_table_lengths_drift_tests.rs b/prover/src/tests/count_table_lengths_drift_tests.rs index 7337f0790..b2ebddfff 100644 --- a/prover/src/tests/count_table_lengths_drift_tests.rs +++ b/prover/src/tests/count_table_lengths_drift_tests.rs @@ -47,7 +47,8 @@ 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!( diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index 1b294efa1..d285747ed 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -1349,9 +1349,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), @@ -1389,7 +1389,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), @@ -1408,7 +1408,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), @@ -1584,9 +1584,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), @@ -1612,7 +1612,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), @@ -1651,7 +1651,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), @@ -2770,6 +2770,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 }; @@ -2853,6 +2859,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/skip_empty_tables_tests.rs b/prover/src/tests/skip_empty_tables_tests.rs index 239c815a3..5542ec8b8 100644 --- a/prover/src/tests/skip_empty_tables_tests.rs +++ b/prover/src/tests/skip_empty_tables_tests.rs @@ -185,3 +185,75 @@ fn validate_still_requires_cpu_and_the_register_file() { "a proof with no register file is rejected" ); } + +/// The accelerators are the ones a run most often never reaches, and each cost a +/// four-row sub-proof regardless. A program with no keccak, no EC and no hint +/// ecall now carries none of the six. +#[test] +fn a_run_without_accelerators_omits_all_six() { + let (elf, logs, _instructions) = run_asm_elf("xori"); + let mut traces = + Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap(); + + let counts = traces.table_counts(); + for (name, count) in [ + ("keccak", counts.keccak), + ("keccak_rnd", counts.keccak_rnd), + ("ecsm", counts.ecsm), + ("ecdas", counts.ecdas), + ("hint", counts.hint), + ("commit", counts.commit), + ] { + assert_eq!( + count, 0, + "{name} should be absent from a plain xori program" + ); + } + assert!(counts.validate().is_ok()); + + assert!( + prove_and_verify(&elf, &mut traces), + "a proof without any accelerator table must still verify" + ); +} + +/// The accelerator counterpart of the forgery above: HINT is the softest table +/// in the set — it constrains nothing about the hinted value — so it is the one +/// worth showing cannot simply be dropped. The CPU's ecall send has no receiver +/// without it, and the bus balance is what notices. +#[test] +fn omitting_a_used_accelerator_fails_the_bus_balance() { + let workspace_root = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .parent() + .expect("workspace root") + .to_path_buf(); + let elf_bytes = + match std::fs::read(workspace_root.join("executor/program_artifacts/rust/hint_min.elf")) { + Ok(bytes) => bytes, + // Built by `make compile-programs-rust`; skip rather than fail when the + // artifact is absent, matching the other guest-ELF tests. + Err(_) => return, + }; + let elf = Elf::load(&elf_bytes).expect("ELF load"); + let executor = executor::vm::execution::Executor::new(&elf, Vec::new()).expect("executor"); + let result = executor.run().expect("execution"); + let mut traces = + Traces::from_elf_and_logs_minimal(&elf, &result.logs, &Default::default(), &[]).unwrap(); + assert!( + !traces.hints.is_empty(), + "hint_min must make a hint ecall for this to be a forgery" + ); + + assert!( + prove_and_verify(&elf, &mut traces), + "the honest proof must verify first, or the negative below proves nothing" + ); + + traces.hints.clear(); + assert_eq!(traces.table_counts().hint, 0); + + assert!( + !prove_and_verify(&elf, &mut traces), + "dropping HINT while the CPU still sends its ecall must not verify" + ); +} 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 a7cf2f0d90d587ecf58e2a0f65d468f51d1c1444 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Wed, 9 Sep 2026 14:59:47 -0300 Subject: [PATCH 05/10] Put back the comment the new test split in two --- prover/src/continuation.rs | 66 +++++++++++++++++++------------------- 1 file changed, 33 insertions(+), 33 deletions(-) diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index f90a9062e..637807d33 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -1958,6 +1958,39 @@ mod tests { } // A memory-heavy multi-epoch continuation. `all_loadstore_32` is ~34 cycles, so + // `epoch_size_log2 = 3` (8 cycles) yields several intermediate epochs (each an + // exact power-of-two cycle count → no CPU padding rows) plus a final epoch. + #[test] + fn test_prove_and_verify_continuation() { + let _ = env_logger::builder().is_test(true).try_init(); + let elf_bytes = asm_elf_bytes("all_loadstore_32"); + let epoch_size_log2 = 3; + let epoch_size = 8; + // Guard against silent degradation: the program must be longer than one + // epoch, otherwise this collapses to a single final epoch and stops testing + // the cross-epoch (intermediate-epoch) path. + let total = Executor::new(&Elf::load(&elf_bytes).unwrap(), vec![]) + .unwrap() + .run() + .unwrap() + .logs + .len(); + assert!( + total > epoch_size, + "program too short ({total} cycles) to exercise intermediate epochs" + ); + assert!( + prove_and_verify_continuation( + &elf_bytes, + &[], + epoch_size_log2, + &ProofOptions::default_test_options() + ) + .unwrap() + .is_some() + ); + } + /// Each epoch drops the chips it never reaches, and it decides that on its /// own: a table missing from one epoch still shows up in another that does /// use it. The skip is not a property of the run, it is a property of the @@ -2058,39 +2091,6 @@ mod tests { ); } - // `epoch_size_log2 = 3` (8 cycles) yields several intermediate epochs (each an - // exact power-of-two cycle count → no CPU padding rows) plus a final epoch. - #[test] - fn test_prove_and_verify_continuation() { - let _ = env_logger::builder().is_test(true).try_init(); - let elf_bytes = asm_elf_bytes("all_loadstore_32"); - let epoch_size_log2 = 3; - let epoch_size = 8; - // Guard against silent degradation: the program must be longer than one - // epoch, otherwise this collapses to a single final epoch and stops testing - // the cross-epoch (intermediate-epoch) path. - let total = Executor::new(&Elf::load(&elf_bytes).unwrap(), vec![]) - .unwrap() - .run() - .unwrap() - .logs - .len(); - assert!( - total > epoch_size, - "program too short ({total} cycles) to exercise intermediate epochs" - ); - assert!( - prove_and_verify_continuation( - &elf_bytes, - &[], - epoch_size_log2, - &ProofOptions::default_test_options() - ) - .unwrap() - .is_some() - ); - } - // Supplied genesis roots must verify identically to the trustless recompute, // and a tampered root (DECODE or a page) must be rejected. `data_page_touch` // touches a real ELF `.data` page, unlike this file's stack-only fixtures. From 44dff2e6d93dbaebc937e5670d4b37156ea6f7c0 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Wed, 9 Sep 2026 14:59:48 -0300 Subject: [PATCH 06/10] Make the new tests check what they claim --- prover/src/tests/prove_elfs_tests.rs | 14 ++- prover/src/tests/skip_empty_tables_tests.rs | 111 ++++++++------------ 2 files changed, 52 insertions(+), 73 deletions(-) diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index d285747ed..7d8101e17 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -64,7 +64,7 @@ fn memw_chunk_rows( /// 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(); @@ -89,7 +89,9 @@ fn prove_and_verify_vm_minimal(elf: &Elf, traces: &mut Traces) -> bool { let multi_proof = match multi_prove_ram(air_trace_pairs, &mut DefaultTranscript::::new(&[])) { Ok(proof) => proof, - Err(_) => return false, + // Panic rather than return false: `false` is reserved for "the verifier + // rejected", so a negative test cannot pass because proving fell over. + Err(e) => panic!("prover failed, which is not a verifier rejection: {e:?}"), }; // Compute the verifier-side expected COMMIT bus balance from public output bytes @@ -2810,10 +2812,12 @@ fn test_verify_rejects_zero_cpu_count() { /// Verify rejects a `table_counts` that under-reports a table the proof carries: /// the counts drive the AIR set, so they must match the sub-proof count. /// -/// MEMW_A rather than MEMW because `sub` reaches no MEMW rows at all, and a -/// count that is already zero is not something to tamper with. +/// Named for the invariant rather than the table: it zeroes MEMW_A because `sub` +/// reaches no MEMW rows at all and a count already at zero is not something to +/// tamper with, and a name tied to one table goes stale the moment that choice +/// changes. #[test] -fn test_verify_rejects_zero_memw_count() { +fn test_verify_rejects_undercounted_table_count() { let elf_bytes = crate::test_utils::asm_elf_bytes("sub"); let proof_options = ProofOptions::default_test_options(); diff --git a/prover/src/tests/skip_empty_tables_tests.rs b/prover/src/tests/skip_empty_tables_tests.rs index 5542ec8b8..cc0262b8b 100644 --- a/prover/src/tests/skip_empty_tables_tests.rs +++ b/prover/src/tests/skip_empty_tables_tests.rs @@ -6,67 +6,14 @@ //! chip is absent and the proof still verifies, and a chip whose operations //! *did* run cannot be dropped, because the LogUp bus no longer balances. -use crypto::fiat_shamir::default_transcript::DefaultTranscript; use stark::proof::options::ProofOptions; -use stark::proof::view::StarkProofView; -use stark::verifier::{IsStarkVerifier, Verifier}; use executor::elf::Elf; use crate::VmAirs; use crate::tables::trace_builder::Traces; -use crate::test_utils::{E, F, multi_prove_ram, run_asm_elf}; - -/// Prove and verify `traces` with the AIR set that its own table counts -/// describe, so an absent chip is absent on both sides — exactly how the -/// production prover and verifier reconstruct the shape. -fn prove_and_verify(elf: &Elf, traces: &mut Traces) -> bool { - let proof_options = ProofOptions::default_test_options(); - let table_counts = traces.table_counts(); - let airs = VmAirs::new( - elf, - &proof_options, - true, - &traces.page_configs, - &table_counts, - None, - true, - None, - None, - None, - ); - - let multi_proof = match multi_prove_ram( - airs.air_trace_pairs(traces), - &mut DefaultTranscript::::new(&[]), - ) { - Ok(proof) => proof, - Err(_) => return false, - }; - let views: Vec> = multi_proof - .proofs - .iter() - .map(StarkProofView::Owned) - .collect(); - - let expected_bus_balance = match crate::compute_expected_commit_bus_balance_view( - &airs.air_refs(), - &views, - &traces.public_output_bytes, - 0, - &mut DefaultTranscript::::new(&[]), - ) { - Some(balance) => balance, - None => return false, - }; - - Verifier::multi_verify_views( - &airs.air_refs(), - &views, - &mut DefaultTranscript::::new(&[]), - &expected_bus_balance, - ) -} +use crate::test_utils::run_asm_elf; +use crate::tests::prove_elfs_tests::prove_and_verify_vm_minimal; /// The premise `TableCounts::validate` now leans on: a chip influences the run /// only through its bus interactions, so an absent chip is caught by the @@ -74,11 +21,41 @@ fn prove_and_verify(elf: &Elf, traces: &mut Traces) -> bool { /// (`Verifier::multi_verify` filters on `has_trace_interaction`), so adding one /// would let a prover drop it unnoticed. Nothing in the AIR set may be in that /// position. +/// +/// Declaring interactions is necessary but not sufficient: a chip whose bus +/// footprint cancelled against itself would contribute zero however many rows it +/// carried, and dropping it would also go unnoticed. No chip is built that way — +/// each one receives its dispatch and sends its own lookups — but this test does +/// not prove that part, and there is no cheap structural check that would. #[test] fn every_table_participates_in_the_bus() { let (elf, logs, _instructions) = run_asm_elf("test_mul_8"); let traces = Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap(); - let table_counts = traces.table_counts(); + // One chunk of every table, not the counts this program happens to produce: + // a zero count builds no AIR, so driving the set off a single program would + // leave the very tables this change makes droppable out of the check. + let table_counts = crate::TableCounts { + cpu: 1, + lt: 1, + memw: 1, + memw_aligned: 1, + load: 1, + mul: 1, + dvrm: 1, + shift: 1, + branch: 1, + memw_register: 1, + eq: 1, + bytewise: 1, + store: 1, + cpu32: 1, + keccak: 1, + keccak_rnd: 1, + ecsm: 1, + ecdas: 1, + hint: 1, + commit: 1, + }; let airs = VmAirs::new( &elf, &ProofOptions::default_test_options(), @@ -123,7 +100,7 @@ fn a_run_without_multiplication_omits_the_mul_table() { ); assert!( - prove_and_verify(&elf, &mut traces), + prove_and_verify_vm_minimal(&elf, &mut traces), "a proof without the unused chips must still verify" ); } @@ -145,7 +122,7 @@ fn omitting_a_table_whose_ops_ran_fails_the_bus_balance() { ); assert!( - prove_and_verify(&elf, &mut traces), + prove_and_verify_vm_minimal(&elf, &mut traces), "the honest proof must verify first, or the negative below proves nothing" ); @@ -157,7 +134,7 @@ fn omitting_a_table_whose_ops_ran_fails_the_bus_balance() { ); assert!( - !prove_and_verify(&elf, &mut traces), + !prove_and_verify_vm_minimal(&elf, &mut traces), "dropping MUL while the CPU still sends MUL requests must not verify" ); } @@ -212,7 +189,7 @@ fn a_run_without_accelerators_omits_all_six() { assert!(counts.validate().is_ok()); assert!( - prove_and_verify(&elf, &mut traces), + prove_and_verify_vm_minimal(&elf, &mut traces), "a proof without any accelerator table must still verify" ); } @@ -227,13 +204,11 @@ fn omitting_a_used_accelerator_fails_the_bus_balance() { .parent() .expect("workspace root") .to_path_buf(); + // Hard failure, not a skip: this is the only negative test covering the + // accelerator direction, so a missing artifact has to be loud. let elf_bytes = - match std::fs::read(workspace_root.join("executor/program_artifacts/rust/hint_min.elf")) { - Ok(bytes) => bytes, - // Built by `make compile-programs-rust`; skip rather than fail when the - // artifact is absent, matching the other guest-ELF tests. - Err(_) => return, - }; + std::fs::read(workspace_root.join("executor/program_artifacts/rust/hint_min.elf")) + .expect("need hint_min.elf — run `make compile-programs-rust`"); let elf = Elf::load(&elf_bytes).expect("ELF load"); let executor = executor::vm::execution::Executor::new(&elf, Vec::new()).expect("executor"); let result = executor.run().expect("execution"); @@ -245,7 +220,7 @@ fn omitting_a_used_accelerator_fails_the_bus_balance() { ); assert!( - prove_and_verify(&elf, &mut traces), + prove_and_verify_vm_minimal(&elf, &mut traces), "the honest proof must verify first, or the negative below proves nothing" ); @@ -253,7 +228,7 @@ fn omitting_a_used_accelerator_fails_the_bus_balance() { assert_eq!(traces.table_counts().hint, 0); assert!( - !prove_and_verify(&elf, &mut traces), + !prove_and_verify_vm_minimal(&elf, &mut traces), "dropping HINT while the CPU still sends its ecall must not verify" ); } From a888946fedceee88bc61c7714cb7bd79061971f1 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Thu, 10 Sep 2026 16:29:20 -0300 Subject: [PATCH 07/10] Reject table counts whose sum wraps --- prover/src/continuation.rs | 10 +++- prover/src/lib.rs | 66 +++++++++++++-------- prover/src/tests/skip_empty_tables_tests.rs | 35 +++++++++++ 3 files changed, 86 insertions(+), 25 deletions(-) diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index 637807d33..92f0a7534 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -803,7 +803,15 @@ fn verify_epoch( FIXED_TABLE_COUNT - 1 }; let proof = epoch.proof(); - let expected_proof_count = table_counts.total() + fixed_tables + 1; + // Checked: the counts are prover-supplied and a wrapped sum would let one + // field stay huge and still match `proof.len()`. + let Some(expected_proof_count) = table_counts + .total() + .and_then(|t| t.checked_add(fixed_tables)) + .and_then(|t| t.checked_add(1)) + else { + return Ok(false); + }; if expected_proof_count != proof.len() { return Ok(false); } diff --git a/prover/src/lib.rs b/prover/src/lib.rs index 7b2cfe0a2..820ea1d6e 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -117,28 +117,38 @@ pub struct TableCounts { } impl TableCounts { - /// Sum of all chunk counts across the split tables. - pub fn total(&self) -> usize { - self.cpu - + self.lt - + self.memw - + self.memw_aligned - + self.load - + self.mul - + self.dvrm - + self.shift - + self.branch - + self.memw_register - + self.eq - + self.bytewise - + self.store - + self.cpu32 - + self.keccak - + self.keccak_rnd - + self.ecsm - + self.ecdas - + self.hint - + self.commit + /// Sum of all chunk counts across the split tables, or `None` if they + /// overflow. + /// + /// The counts are prover-supplied and release builds wrap on overflow, so a + /// plain sum is not enough: the sub-proof cross-check compares only this + /// total, and a wrapped one lets a single astronomically large field pass it + /// and reach `VmAirs::new`, which sizes a `Vec` from that field directly. + pub fn total(&self) -> Option { + [ + self.cpu, + self.lt, + self.memw, + self.memw_aligned, + self.load, + self.mul, + self.dvrm, + self.shift, + self.branch, + self.memw_register, + self.eq, + self.bytewise, + self.store, + self.cpu32, + self.keccak, + self.keccak_rnd, + self.ecsm, + self.ecdas, + self.hint, + self.commit, + ] + .into_iter() + .try_fold(0usize, usize::checked_add) } /// Validate that the structurally-required tables have at least one chunk. @@ -1456,11 +1466,19 @@ fn verify_proof_parts( // Cross-check: table_counts must match the number of sub-proofs. // FIXED_TABLE_COUNT always-present tables, plus page tables. - let expected_proof_count = table_counts.total() + FIXED_TABLE_COUNT + page_configs.len(); + let Some(expected_proof_count) = table_counts + .total() + .and_then(|t| t.checked_add(FIXED_TABLE_COUNT)) + .and_then(|t| t.checked_add(page_configs.len())) + else { + return Err(Error::InvalidTableCounts( + "declared table counts overflow usize".to_string(), + )); + }; if expected_proof_count != proofs.len() { return Err(Error::InvalidTableCounts(format!( "table_counts total ({}) + {FIXED_TABLE_COUNT} fixed + {} pages = {}, but proof contains {} sub-proofs", - table_counts.total(), + expected_proof_count - FIXED_TABLE_COUNT - page_configs.len(), page_configs.len(), expected_proof_count, proofs.len(), diff --git a/prover/src/tests/skip_empty_tables_tests.rs b/prover/src/tests/skip_empty_tables_tests.rs index cc0262b8b..423af3ade 100644 --- a/prover/src/tests/skip_empty_tables_tests.rs +++ b/prover/src/tests/skip_empty_tables_tests.rs @@ -163,6 +163,41 @@ fn validate_still_requires_cpu_and_the_register_file() { ); } +/// The counts ride in the proof, so they are the prover's to choose, and the +/// sub-proof cross-check compares only their sum. A plain `+` wraps silently in +/// release (the workspace sets no `overflow-checks`), so an attacker can park +/// one field near `usize::MAX`, pick a second to carry the sum around to +/// whatever `proofs.len()` is, and pass that check with the huge field intact — +/// straight into `VmAirs::new`, which sizes a `Vec` from it. +#[test] +fn counts_that_wrap_have_no_total() { + let (elf, logs, _instructions) = run_asm_elf("test_mul_8"); + let traces = Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap(); + let honest = traces.table_counts(); + let honest_total = honest.total().expect("an honest run has a total"); + + let mut wrapped = honest.clone(); + wrapped.mul += usize::MAX - honest_total; + assert!( + wrapped.validate().is_ok(), + "validate looks at two fields, not at the sum" + ); + assert_eq!( + wrapped.total(), + Some(usize::MAX), + "one below the wrap still totals" + ); + + // One more takes the *sum* past the end, not the field: `mul` itself stays + // below `usize::MAX` because the other counts hold the difference. + wrapped.mul += 1; + assert_eq!( + wrapped.total(), + None, + "a wrapped sum must not be reported as a small one" + ); +} + /// The accelerators are the ones a run most often never reaches, and each cost a /// four-row sub-proof regardless. A program with no keccak, no EC and no hint /// ecall now carries none of the six. From 9c466d2b21b48d7e043dd35e870ee362fbcc4712 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Thu, 10 Sep 2026 16:29:20 -0300 Subject: [PATCH 08/10] Name the check that rejects a dropped table --- prover/src/tests/prove_elfs_tests.rs | 72 +++++- prover/src/tests/skip_empty_tables_tests.rs | 259 +++++++++++++++++--- 2 files changed, 300 insertions(+), 31 deletions(-) diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index 7d8101e17..92e27528a 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -65,6 +65,42 @@ fn memw_chunk_rows( /// /// Uses minimal bitwise (no full 2^20 preprocessed table) but DECODE is always preprocessed. pub(crate) fn prove_and_verify_vm_minimal(elf: &Elf, traces: &mut Traces) -> bool { + weigh_the_bus(elf, traces, false).accepted +} + +/// What the verifier did with a proof, split so a negative test can name the +/// check that rejected it instead of just observing that something did. +/// +/// `multi_verify_views` returns `false` from about ten places — the +/// bus_public_inputs presence symmetry, a missing `public_inputs()`, any +/// table's rounds 2-4 — so a bare `assert!(!verified)` cannot tell "the bus +/// balance caught the forgery" from "the forged proof fell over somewhere +/// else". `target_moved` is what separates them. +pub(crate) struct BusOutcome { + /// `multi_verify_views` against the target the verifier computes itself. + pub accepted: bool, + /// Σ `table_contribution` over the tables the bus sums, exactly as the + /// verifier computes it. + pub contribution_sum: FieldElement, + /// The target that sum has to match. + pub target: FieldElement, + /// The same proof re-verified with the target moved to `contribution_sum`. + /// When this is true and `accepted` is false, every other check passed and + /// the balance is the *only* reason for the rejection. + pub accepted_with_target_moved: bool, + /// Per-table contribution, for the tables the sum above ranges over. A + /// table that contributes zero is one the bus cannot notice the absence of. + pub per_table: Vec<(String, FieldElement)>, +} + +/// Prove and verify as `prove_and_verify_vm_minimal`, and weigh the bus while +/// at it. `recheck_with_moved_target` costs a second full verification, so the +/// plain wrapper above leaves it off. +pub(crate) fn weigh_the_bus( + elf: &Elf, + traces: &mut Traces, + recheck_with_moved_target: bool, +) -> BusOutcome { let _ = env_logger::builder().is_test(true).try_init(); let proof_options = ProofOptions::default_test_options(); @@ -111,12 +147,42 @@ pub(crate) fn prove_and_verify_vm_minimal(elf: &Elf, traces: &mut Traces) -> boo .expect("fingerprint collision in test"); // Verify using centralized air_refs() which includes all tables - Verifier::multi_verify_views( - &airs.air_refs(), + let air_refs = airs.air_refs(); + let accepted = Verifier::multi_verify_views( + &air_refs, &views, &mut DefaultTranscript::::new(&[]), &expected_bus_balance, - ) + ); + + // The verifier's own sum, recomputed here so a test can compare it against + // the target instead of guessing why a proof was rejected. + let mut contribution_sum = FieldElement::::zero(); + let mut per_table = Vec::new(); + for (air, view) in air_refs.iter().zip(views.iter()) { + if air.has_trace_interaction() + && let Some(contribution) = view.bus_table_contribution() + { + contribution_sum += contribution; + per_table.push((air.name().to_string(), contribution)); + } + } + + let accepted_with_target_moved = recheck_with_moved_target + && Verifier::multi_verify_views( + &air_refs, + &views, + &mut DefaultTranscript::::new(&[]), + &contribution_sum, + ); + + BusOutcome { + accepted, + contribution_sum, + target: expected_bus_balance, + accepted_with_target_moved, + per_table, + } } /// Like [`crate::prove_with_options_and_inputs`] but trims the bitwise table to the diff --git a/prover/src/tests/skip_empty_tables_tests.rs b/prover/src/tests/skip_empty_tables_tests.rs index 423af3ade..a8d1d08f0 100644 --- a/prover/src/tests/skip_empty_tables_tests.rs +++ b/prover/src/tests/skip_empty_tables_tests.rs @@ -6,14 +6,58 @@ //! chip is absent and the proof still verifies, and a chip whose operations //! *did* run cannot be dropped, because the LogUp bus no longer balances. +use math::field::element::FieldElement; use stark::proof::options::ProofOptions; use executor::elf::Elf; +use executor::vm::execution::ExecutionResult; use crate::VmAirs; use crate::tables::trace_builder::Traces; +use crate::tables::types::GoldilocksExtension; use crate::test_utils::run_asm_elf; -use crate::tests::prove_elfs_tests::prove_and_verify_vm_minimal; +use crate::tests::prove_elfs_tests::{BusOutcome, prove_and_verify_vm_minimal, weigh_the_bus}; + +/// Load and run one of the compiled Rust guest programs. +/// +/// Hard failure, not a skip: a missing artifact would turn a negative test +/// green having asserted nothing. +fn run_rust_elf(name: &str) -> (Elf, ExecutionResult) { + let workspace_root = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .parent() + .expect("workspace root") + .to_path_buf(); + let path = workspace_root.join(format!("executor/program_artifacts/rust/{name}.elf")); + let elf_bytes = std::fs::read(&path) + .unwrap_or_else(|_| panic!("need {name}.elf — run `make compile-programs-rust`")); + let elf = Elf::load(&elf_bytes).expect("ELF load"); + let executor = executor::vm::execution::Executor::new(&elf, Vec::new()).expect("executor"); + let result = executor.run().expect("execution"); + (elf, result) +} + +/// The claim every drop-forgery below makes, in one place. +/// +/// `multi_verify_views` returns `false` from about ten places, so +/// `assert!(!accepted)` on its own would pass just as happily if the forged +/// proof fell over in rounds 2-4 or tripped the bus_public_inputs presence +/// check — the opposite of what these tests say they demonstrate. Moving the +/// target onto the sum the forgery actually produced is what separates them: if +/// the same proof then verifies, the balance was the only objection. +fn assert_only_the_bus_rejected(outcome: &BusOutcome, what: &str) { + assert!(!outcome.accepted, "dropping {what} must not verify"); + assert_ne!( + outcome.contribution_sum, outcome.target, + "dropping {what} left the bus balanced, so the rejection came from \ + elsewhere and the bus did not notice the forgery at all" + ); + assert!( + outcome.accepted_with_target_moved, + "with the target moved onto the forged sum the proof still failed, so \ + something other than the bus balance rejected {what} and this test is \ + not showing what it claims" + ); +} /// The premise `TableCounts::validate` now leans on: a chip influences the run /// only through its bus interactions, so an absent chip is caught by the @@ -22,11 +66,12 @@ use crate::tests::prove_elfs_tests::prove_and_verify_vm_minimal; /// would let a prover drop it unnoticed. Nothing in the AIR set may be in that /// position. /// -/// Declaring interactions is necessary but not sufficient: a chip whose bus -/// footprint cancelled against itself would contribute zero however many rows it -/// carried, and dropping it would also go unnoticed. No chip is built that way — -/// each one receives its dispatch and sends its own lookups — but this test does -/// not prove that part, and there is no cheap structural check that would. +/// This is the *necessary* half, and it cannot fail for any chip that exists +/// today: `has_trace_interaction()` reads a list fixed at construction and +/// every `create_*_air` passes a non-empty one. It is a tripwire for a future +/// chip built like `test_utils::busless_air`, not evidence about this change. +/// The sufficient half — that a present table's contribution is actually +/// nonzero — is [`no_present_table_contributes_zero_to_the_bus`]. #[test] fn every_table_participates_in_the_bus() { let (elf, logs, _instructions) = run_asm_elf("test_mul_8"); @@ -81,6 +126,115 @@ fn every_table_participates_in_the_bus() { ); } +/// The half the test above cannot reach: declaring interactions is necessary, +/// but a chip whose bus footprint cancelled against itself would contribute +/// zero however many rows it carried, and dropping *that* would move the sum by +/// nothing. The chained chips are the candidates — ECDAS receives an +/// accumulator state and sends the updated one back on the same bus, COMMIT +/// telescopes on `CommitNextByte`, KECCAK_RND chains rounds — and each is +/// supposed to be anchored by a term that does not telescope away with it. +/// +/// There is nothing structural to inspect, but there is a cheap dynamic check: +/// the contribution is a public input of every sub-proof, so proving a program +/// that reaches a chip says outright what that chip puts on the bus. A zero +/// here is a table that can be dropped undetected. +#[test] +fn no_present_table_contributes_zero_to_the_bus() { + let asm = [ + "all_instructions_64", + "all_loadstore_32", + "test_keccak", + "test_ecsm", + "test_commit_4", + ]; + + // Only the tables a prover can declare away are at risk. The always-present + // ones (BITWISE, DECODE, KECCAK_RC, REGISTER, HALT, the PAGEs, L2G) have no + // `TableCounts` field, and they legitimately contribute zero when the run + // never reaches them — KECCAK_RC does exactly that in a program with no + // keccak, which is the padding this change is about and cannot be dropped. + let droppable = [ + "CPU", + "MEMW_R", + "LT", + "MEMW", + "MEMW_A", + "LOAD", + "MUL", + "DVRM", + "SHIFT", + "BRANCH", + "EQ", + "BYTEWISE", + "STORE", + "CPU32", + "KECCAK", + "KECCAK_RND", + "ECSM", + "ECDAS", + "HINT", + "COMMIT", + ]; + + let mut seen: Vec = Vec::new(); + let mut fixed_seen: Vec = Vec::new(); + let mut zero: Vec<(String, String)> = Vec::new(); + + let mut weigh = |program: &str, elf: &Elf, traces: &mut Traces| { + let outcome = weigh_the_bus(elf, traces, false); + assert!( + outcome.accepted, + "{program} must prove and verify honestly first" + ); + for (table, contribution) in &outcome.per_table { + let base = table.split('[').next().unwrap_or(table).to_string(); + let list = if droppable.contains(&base.as_str()) { + &mut seen + } else { + &mut fixed_seen + }; + if !list.contains(&base) { + list.push(base.clone()); + } + if droppable.contains(&base.as_str()) + && *contribution == FieldElement::::zero() + { + zero.push((program.to_string(), table.clone())); + } + } + }; + + for program in asm { + let (elf, logs, _instructions) = run_asm_elf(program); + let mut traces = + Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap(); + weigh(program, &elf, &mut traces); + } + let (elf, result) = run_rust_elf("hint_min"); + let mut traces = + Traces::from_elf_and_logs_minimal(&elf, &result.logs, &Default::default(), &[]).unwrap(); + weigh("hint_min", &elf, &mut traces); + + assert!( + zero.is_empty(), + "these tables contribute nothing to the bus, so dropping them would go \ + unnoticed however many rows they carry: {zero:?}" + ); + + // Coverage is the weak point of a dynamic check: a table no program here + // reaches is simply unexamined. Pin the ones covered today so the check + // cannot quietly stop covering them. + for table in droppable { + assert!( + seen.iter().any(|s| s == table), + "{table} is no longer reached by any program here, so its \ + contribution is unexamined; seen: {seen:?}" + ); + } + println!("droppable tables weighed on the bus: {seen:?}"); + println!("always-present tables, not at risk here: {fixed_seen:?}"); +} + /// A program that never multiplies or divides gets no MUL and no DVRM table, /// and still verifies. #[test] @@ -92,8 +246,6 @@ fn a_run_without_multiplication_omits_the_mul_table() { let table_counts = traces.table_counts(); assert_eq!(table_counts.mul, 0, "xori executes no multiplication"); assert_eq!(table_counts.dvrm, 0, "xori executes no division"); - assert!(traces.muls.is_empty()); - assert!(traces.dvrms.is_empty()); assert!( table_counts.validate().is_ok(), "zero counts on unused chips are legitimate" @@ -127,16 +279,12 @@ fn omitting_a_table_whose_ops_ran_fails_the_bus_balance() { ); traces.muls.clear(); - assert_eq!(traces.table_counts().mul, 0); assert!( traces.table_counts().validate().is_ok(), "validate deliberately lets this through — the bus is what rejects it" ); - assert!( - !prove_and_verify_vm_minimal(&elf, &mut traces), - "dropping MUL while the CPU still sends MUL requests must not verify" - ); + assert_only_the_bus_rejected(&weigh_the_bus(&elf, &mut traces, true), "MUL"); } /// What `validate` still refuses: a proof with no CPU describes no execution, @@ -235,18 +383,7 @@ fn a_run_without_accelerators_omits_all_six() { /// without it, and the bus balance is what notices. #[test] fn omitting_a_used_accelerator_fails_the_bus_balance() { - let workspace_root = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR")) - .parent() - .expect("workspace root") - .to_path_buf(); - // Hard failure, not a skip: this is the only negative test covering the - // accelerator direction, so a missing artifact has to be loud. - let elf_bytes = - std::fs::read(workspace_root.join("executor/program_artifacts/rust/hint_min.elf")) - .expect("need hint_min.elf — run `make compile-programs-rust`"); - let elf = Elf::load(&elf_bytes).expect("ELF load"); - let executor = executor::vm::execution::Executor::new(&elf, Vec::new()).expect("executor"); - let result = executor.run().expect("execution"); + let (elf, result) = run_rust_elf("hint_min"); let mut traces = Traces::from_elf_and_logs_minimal(&elf, &result.logs, &Default::default(), &[]).unwrap(); assert!( @@ -260,10 +397,76 @@ fn omitting_a_used_accelerator_fails_the_bus_balance() { ); traces.hints.clear(); - assert_eq!(traces.table_counts().hint, 0); + assert_only_the_bus_rejected(&weigh_the_bus(&elf, &mut traces, true), "HINT"); +} +/// The dispatch above is CPU-to-chip. KECCAK_RND is reached from KECCAK, not +/// from the CPU, so dropping it exercises a chip-to-chip bus: the anchor whose +/// terms go unmatched sits in another accelerator's contribution, not in the +/// CPU's. +#[test] +fn omitting_a_chip_dispatched_by_another_chip_fails_the_bus_balance() { + let (elf, logs, _instructions) = run_asm_elf("test_keccak"); + let mut traces = + Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap(); assert!( - !prove_and_verify_vm_minimal(&elf, &mut traces), - "dropping HINT while the CPU still sends its ecall must not verify" + !traces.keccaks.is_empty() && !traces.keccak_rnds.is_empty(), + "test_keccak must exercise both keccak tables for this to be a forgery" + ); + + assert!( + prove_and_verify_vm_minimal(&elf, &mut traces), + "the honest proof must verify first, or the negative below proves nothing" + ); + + traces.keccak_rnds.clear(); + assert_only_the_bus_rejected(&weigh_the_bus(&elf, &mut traces, true), "KECCAK_RND"); +} + +/// COMMIT is the one newly-optional table whose bus target is not zero: the +/// verifier computes it from the public output the prover supplies +/// (`compute_expected_commit_bus_balance_view`), and nothing requires +/// `commit > 0` when that output is non-empty. Before this change the COMMIT +/// sub-proof was structurally mandatory; now its presence is a number the +/// prover picks, and the balance is the only thing standing behind it. +#[test] +fn omitting_the_commit_table_fails_the_bus_balance() { + let (elf, logs, _instructions) = run_asm_elf("test_commit_4"); + let mut traces = + Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap(); + assert!( + !traces.commits.is_empty() && !traces.public_output_bytes.is_empty(), + "test_commit_4 must commit output for this to be a forgery" + ); + + assert!( + prove_and_verify_vm_minimal(&elf, &mut traces), + "the honest proof must verify first, or the negative below proves nothing" + ); + + traces.commits.clear(); + assert_only_the_bus_rejected(&weigh_the_bus(&elf, &mut traces, true), "COMMIT"); +} + +/// The variant the test above does not cover: a prover who drops COMMIT can +/// also drop the output it committed, and that moves the verifier's *target* +/// rather than the sum — the balance is recomputed for an empty output. The +/// CPU's commit ecalls are still in the trace with no receiver, so the two +/// sides still have to disagree. +#[test] +fn omitting_the_commit_table_and_its_output_fails_the_bus_balance() { + let (elf, logs, _instructions) = run_asm_elf("test_commit_4"); + let mut traces = + Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap(); + let honest_target = weigh_the_bus(&elf, &mut traces, false).target; + + traces.commits.clear(); + traces.public_output_bytes.clear(); + let outcome = weigh_the_bus(&elf, &mut traces, true); + assert_ne!( + outcome.target, honest_target, + "clearing the public output must move the target, or this test is the \ + previous one over again" ); + assert_only_the_bus_rejected(&outcome, "COMMIT together with its output"); } From d8739e9f0e8ac9e55133c39439fc3c7b2715bd3d Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Thu, 10 Sep 2026 16:29:21 -0300 Subject: [PATCH 09/10] Probe every table count in the statement --- prover/src/tests/statement_tests.rs | 95 ++++++++++++++++++++++++++--- 1 file changed, 88 insertions(+), 7 deletions(-) diff --git a/prover/src/tests/statement_tests.rs b/prover/src/tests/statement_tests.rs index 2a7aea502..e30a87dad 100644 --- a/prover/src/tests/statement_tests.rs +++ b/prover/src/tests/statement_tests.rs @@ -67,6 +67,92 @@ fn state_after_absorb( t.state() } +/// A `&mut` handle to every count, for tests that have to move each one. +/// +/// The exhaustive destructure makes a new `TableCounts` field a compile error +/// here, and `deny(unused_variables)` makes *destructuring it and then not +/// returning it* an error too — which is the hole a plain destructure leaves: +/// `absorb_statement` has the same exhaustive pattern, but the array it feeds +/// the transcript is written out separately, so a field can be destructured +/// there and quietly dropped before it reaches the sponge. +#[deny(unused_variables)] +fn each_count_mut(counts: &mut TableCounts) -> Vec<(&'static str, &mut usize)> { + let TableCounts { + cpu, + lt, + memw, + memw_aligned, + load, + mul, + dvrm, + shift, + branch, + memw_register, + eq, + bytewise, + store, + cpu32, + keccak, + keccak_rnd, + ecsm, + ecdas, + hint, + commit, + } = counts; + vec![ + ("cpu", cpu), + ("lt", lt), + ("memw", memw), + ("memw_aligned", memw_aligned), + ("load", load), + ("mul", mul), + ("dvrm", dvrm), + ("shift", shift), + ("branch", branch), + ("memw_register", memw_register), + ("eq", eq), + ("bytewise", bytewise), + ("store", store), + ("cpu32", cpu32), + ("keccak", keccak), + ("keccak_rnd", keccak_rnd), + ("ecsm", ecsm), + ("ecdas", ecdas), + ("hint", hint), + ("commit", commit), + ] +} + +/// Every count has to reach the transcript, not just the one a test happened +/// to pick. The V4 encoding added six accelerator counts; a field that is +/// destructured in `absorb_statement` and then left out of the array it +/// absorbs compiles clean and changes nothing about the state, which is a +/// prover-chosen number the verifier would no longer be bound to. +#[test] +fn state_depends_on_every_table_count() { + let baseline = state_after_absorb(b"elf", b"out", &sample_counts(), 1, &sample_ranges(), 7); + + let names: Vec<&str> = each_count_mut(&mut sample_counts()) + .into_iter() + .map(|(name, _)| name) + .collect(); + assert_eq!(names.len(), 20, "every count must be probed"); + + for name in names { + let mut counts = sample_counts(); + for (candidate, slot) in each_count_mut(&mut counts) { + if candidate == name { + *slot += 1; + } + } + assert_ne!( + baseline, + state_after_absorb(b"elf", b"out", &counts, 1, &sample_ranges(), 7), + "state must depend on table_counts.{name}", + ); + } +} + #[test] fn state_is_deterministic() { let a = state_after_absorb(b"elf", b"out", &sample_counts(), 3, &sample_ranges(), 7); @@ -103,13 +189,8 @@ fn state_depends_on_every_field() { "state must depend on public_output", ); - let mut counts2 = sample_counts(); - counts2.branch += 1; - assert_ne!( - baseline, - state_after_absorb(b"elf", b"out", &counts2, 1, &sample_ranges(), 7), - "state must depend on table_counts", - ); + // table_counts gets its own test: one field moving the state says nothing + // about the other nineteen. See `state_depends_on_every_table_count`. assert_ne!( baseline, From 7bb2820072e99976471164844b52e6f85058fea8 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Thu, 10 Sep 2026 16:29:21 -0300 Subject: [PATCH 10/10] Cover a table set that varies by epoch --- prover/src/continuation.rs | 116 ++++++++++++++++++++++- prover/src/tests/recursion_smoke_test.rs | 66 +++++++++++++ 2 files changed, 177 insertions(+), 5 deletions(-) diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index 92f0a7534..6994a9e8e 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -490,6 +490,13 @@ impl ContinuationProof { pub fn num_epochs(&self) -> usize { self.epochs.len() } + + /// What each epoch declared it carries, for tests that have to show the + /// epochs disagree. `epochs` itself stays private. + #[cfg(test)] + pub(crate) fn epoch_table_counts(&self) -> Vec<&TableCounts> { + self.epochs.iter().map(|e| &e.table_counts).collect() + } } /// Borrowed view over an [`EpochProof`] (owned or archived-in-place). Lets @@ -2071,11 +2078,23 @@ mod tests { ); // And the epochs disagree: some table is in one and out of another. - let disagreeing: Vec<&str> = per_epoch[0] + // + // Among the *non-final* epochs only. The final epoch is the one that + // carries HALT and the one where a program's output is committed, so a + // difference that involves it can be structural — a whole-run table set + // would still produce it, and this assertion would pass while measuring + // nothing about per-epoch granularity. + assert!( + per_epoch.len() >= 3, + "need at least two non-final epochs to compare, got {} epochs", + per_epoch.len() + ); + let non_final = &per_epoch[..per_epoch.len() - 1]; + let disagreeing: Vec<&str> = non_final[0] .iter() .enumerate() .filter(|(i, (_, first))| { - per_epoch + non_final .iter() .any(|row| (row[*i].1 == 0) != (*first == 0)) }) @@ -2083,11 +2102,39 @@ mod tests { .collect(); assert!( !disagreeing.is_empty(), - "every epoch carries the same tables, so per-epoch granularity is \ - untested here — pick a program or epoch size that varies:\n {}", + "the non-final epochs all carry the same tables, so per-epoch \ + granularity is untested here — pick a program or epoch size that \ + varies:\n {}", layout() ); - println!("tables present in some epochs but not others: {disagreeing:?}"); + + // Sharper: a table that is present, goes away, and comes back cannot be + // produced by any scheme that computes one set over the run or over a + // prefix of it. Counting the blocks of consecutive epochs a table + // appears in, more than one block is exactly that shape. + let blocks = |i: usize| { + let present: Vec = per_epoch.iter().map(|row| row[i].1 > 0).collect(); + present + .iter() + .enumerate() + .filter(|(k, p)| **p && (*k == 0 || !present[k - 1])) + .count() + }; + let reappearing: Vec<&str> = per_epoch[0] + .iter() + .enumerate() + .filter(|(i, _)| blocks(*i) > 1) + .map(|(_, (name, _))| *name) + .collect(); + assert!( + !reappearing.is_empty(), + "no table leaves and comes back, so a union or prefix scheme would \ + produce this same layout — the test cannot tell them apart:\n {}", + layout() + ); + + println!("tables present in some non-final epochs but not others: {disagreeing:?}"); + println!("tables that leave and come back: {reappearing:?}"); println!(" {}", layout()); // The mixed-shape bundle has to verify end to end. @@ -2397,6 +2444,65 @@ mod tests { ); } + /// The continuation counterpart of the monolithic + /// `test_verify_rejects_undercounted_table_count`: an epoch that declares + /// away a table it actually carries. Both branches of the cross-check are + /// exercised, because the fixed-table term differs between a non-final + /// epoch (`FIXED_TABLE_COUNT - 1`, no HALT) and the final one — and + /// `verify_epoch` swallows the mismatch as `Ok(false)` rather than an + /// error, so a regression in that arithmetic would be silent. + #[test] + fn test_split_verify_rejects_undercounted_epoch_table_count() { + let _ = env_logger::builder().is_test(true).try_init(); + let elf_bytes = asm_elf_bytes("all_loadstore_32"); + let opts = ProofOptions::default_test_options(); + let mut bundle = prove_continuation(&elf_bytes, &[], 3, &opts).unwrap(); + assert!( + bundle.epochs.len() >= 2, + "need a non-final and a final epoch, got {}", + bundle.epochs.len() + ); + let last = bundle.epochs.len() - 1; + for epoch in [0, last] { + // Whatever this epoch does carry: the point is declaring one of its + // own tables away, not which one. + let counts = &mut bundle.epochs[epoch].table_counts; + let (name, restore) = if counts.load > 0 { + ("load", std::mem::replace(&mut counts.load, 0)) + } else if counts.store > 0 { + ("store", std::mem::replace(&mut counts.store, 0)) + } else { + ("lt", std::mem::replace(&mut counts.lt, 0)) + }; + assert!( + restore > 0, + "epoch {epoch} carries no optional table to declare away" + ); + assert!( + verify_continuation(&elf_bytes, &bundle, &opts) + .unwrap() + .is_none(), + "epoch {epoch} declaring away its {name} table must be rejected" + ); + let counts = &mut bundle.epochs[epoch].table_counts; + match name { + "load" => counts.load = restore, + "store" => counts.store = restore, + _ => counts.lt = restore, + } + } + + // The control, and the reason the rejections above mean something: put + // the counts back and the same bundle verifies. One verify, at the end, + // rather than one before and one after — each costs a full pass. + assert!( + verify_continuation(&elf_bytes, &bundle, &opts) + .unwrap() + .is_some(), + "restoring the counts must bring the bundle back" + ); + } + // The raw private input must not be bundled under continuations. The bundle carries no // raw private bytes (only `num_private_input_pages`), yet a multi-epoch continuation of // a program that reads private input verifies from the bundle + ELF ALONE and diff --git a/prover/src/tests/recursion_smoke_test.rs b/prover/src/tests/recursion_smoke_test.rs index 90482a3a4..6003e3993 100644 --- a/prover/src/tests/recursion_smoke_test.rs +++ b/prover/src/tests/recursion_smoke_test.rs @@ -750,6 +750,72 @@ fn test_recursion_continuation_blob_decodes_and_verifies_on_host() { ); } +/// The recursion path over a bundle whose epochs carry *different* table sets. +/// +/// Every other continuation fixture here proves fibonacci, whose epochs all do +/// the same work and therefore all declare the same tables. A uniform bundle +/// cannot tell a per-epoch table set from a whole-run one, and it never +/// exercises `verify_epoch`'s cross-check against a count that changes from one +/// epoch to the next — which is the arithmetic this change rewrote. +/// `all_loadstore_32` at 8-cycle epochs has a table that is present, goes away +/// and comes back. +#[test] +fn test_recursion_accepts_a_bundle_whose_epochs_carry_different_tables() { + let elf_bytes = crate::test_utils::asm_elf_bytes("all_loadstore_32"); + + let bundle = crate::continuation::prove_continuation(&elf_bytes, &[], 3, &MIN_PROOF_OPTIONS) + .expect("continuation prove should succeed"); + assert!( + bundle.num_epochs() > 1, + "8-cycle epochs must split all_loadstore_32 for this test to bite" + ); + + // The premise: the epochs really do disagree. Without this the test is the + // fibonacci one again, with a slower program. + let present_per_epoch: Vec> = bundle + .epoch_table_counts() + .iter() + .map(|c| vec![c.load > 0, c.store > 0, c.memw > 0, c.lt > 0, c.branch > 0]) + .collect(); + let disagrees = (0..present_per_epoch[0].len()).any(|i| { + present_per_epoch + .iter() + .any(|row| row[i] != present_per_epoch[0][i]) + }); + assert!( + disagrees, + "every epoch declares the same tables, so this bundle does not exercise \ + a variable table set: {present_per_epoch:?}" + ); + + // Ground truth from the host path, then the same bundle through the guest's. + let expected_output = + crate::continuation::verify_continuation(&elf_bytes, &bundle, &MIN_PROOF_OPTIONS) + .expect("verify_continuation errored") + .expect("a mixed-shape bundle must verify"); + let (expected_decode, expected_pages) = + crate::continuation::continuation_precomputed_commitments( + &elf_bytes, + &bundle, + &MIN_PROOF_OPTIONS, + ) + .expect("continuation_precomputed_commitments errored"); + let expected_id = recursion::program_id_from_elf(&elf_bytes, &expected_decode, &expected_pages) + .expect("program_id_from_elf errored"); + + let blob = recursion::encode_continuation_guest_input(bundle, &elf_bytes, &MIN_PROOF_OPTIONS) + .expect("encode_continuation_guest_input failed"); + let attestation = recursion::verify_continuation_and_attest(&blob, &MIN_PROOF_OPTIONS) + .expect("verify_continuation_and_attest errored") + .expect("a mixed-shape bundle must survive the guest path too"); + let (id, output) = recursion::split_attestation(&attestation).expect("attestation too short"); + assert_eq!( + id, expected_id, + "attested id must match the honest recompute" + ); + assert_eq!(output, &expected_output[..], "attested output must match"); +} + /// Corrupting a private-input commitment on an *honest* proof makes /// verification fail (`Ok(false)`). Necessary but not sufficient alone — a /// custom prover can supply consistent mismatched roots (see