From 4960a815c1d26735ee15559e89dafdab5736bc03 Mon Sep 17 00:00:00 2001 From: Nicole Date: Tue, 13 Oct 2026 16:03:46 -0300 Subject: [PATCH 1/8] Pin the final register file in the verifier so execution cannot continue past the exit ecall --- executor/programs/asm/poc_halt_continue.s | 29 ++ prover/src/continuation.rs | 19 ++ prover/src/lib.rs | 20 +- prover/src/tables/register.rs | 33 +- prover/src/tests/halt_continuation_poc.rs | 143 +++++++++ prover/src/tests/halt_pc_forgery_poc.rs | 293 ++++++++++++++++++ prover/src/tests/mod.rs | 2 + prover/src/tests/page_offset_forgery_poc.rs | 14 +- .../src/tests/recursion_soundness_gap_poc.rs | 7 +- 9 files changed, 553 insertions(+), 7 deletions(-) create mode 100644 executor/programs/asm/poc_halt_continue.s create mode 100644 prover/src/tests/halt_continuation_poc.rs create mode 100644 prover/src/tests/halt_pc_forgery_poc.rs diff --git a/executor/programs/asm/poc_halt_continue.s b/executor/programs/asm/poc_halt_continue.s new file mode 100644 index 000000000..544b70716 --- /dev/null +++ b/executor/programs/asm/poc_halt_continue.s @@ -0,0 +1,29 @@ + .text + .attribute 5, "rv64i2p1" + .globl main +main: + # Exit with a NON-ZERO code. HALT enforces x10 == 0, so an honest prover + # cannot prove this program. + li a0, 1 + li a7, 93 # syscall = Halt + ecall + + # Never reached by an honest execution. The HALT PoC runs these rows AFTER + # the exit ecall to zero x10 before the trace ends. + li a0, 0 + nop + nop + nop + nop + nop + nop + nop + nop + nop + nop + nop + nop + + # Lets the PoC's patched copy (first ecall -> nop) terminate in the executor. + li a7, 93 + ecall diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index 5b16fcd29..f37718b2e 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -1665,6 +1665,21 @@ fn verify_continuation_view( let l2g_root = epoch.l2g_root(); let epoch_public_output = epoch.public_output(); + // The final epoch's `reg_fini` has no next epoch to bind it, so pin it to + // the halted register file (as the monolithic verifier does): this ends the + // PC chain on `pc = 1`, so execution cannot continue past the exit ecall. + // x254 counts every byte committed across the run. + if is_final { + let Ok(committed_bytes) = + u32::try_from(public_output.len() + epoch_public_output.len()) + else { + return Ok(None); + }; + if epoch.reg_fini()? != register::halted_fini(committed_bytes) { + return Ok(None); + } + } + if !verify_epoch( &elf, elf_bytes, @@ -1801,6 +1816,10 @@ pub(crate) mod test_fault { pub(crate) const FAIL_INDEX: u64 = 3; } +#[cfg(test)] +#[path = "tests/halt_continuation_poc.rs"] +mod halt_continuation_poc; + #[cfg(test)] mod tests { use super::*; diff --git a/prover/src/lib.rs b/prover/src/lib.rs index 2a1772d0d..48d472be0 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -1347,6 +1347,8 @@ pub fn prove_with_options_and_inputs( let __sp = stark::instruments::span("air_construction"); let table_counts = traces.table_counts(); + let committed_bytes = u32::try_from(traces.public_output_bytes.len()) + .expect("trace build bounds the commit index to u32"); let airs = VmAirs::new( &program, proof_options, @@ -1357,7 +1359,11 @@ pub fn prove_with_options_and_inputs( true, None, None, - None, + Some(register::halted_preprocessed( + proof_options, + program.entry_point, + committed_bytes, + )), ); #[cfg(feature = "instruments")] @@ -1587,6 +1593,12 @@ fn verify_proof_parts( ))); } + // The final register file is verifier-known: pinning it ends the PC chain on + // `pc = 1` (see `register::halted_fini`). + // An honest run cannot commit more bytes than x254 counts. + let Ok(committed_bytes) = u32::try_from(public_output.len()) else { + return Ok(false); + }; let airs = VmAirs::new( program, proof_options, @@ -1597,7 +1609,11 @@ fn verify_proof_parts( true, None, page_commitments, - None, + Some(register::halted_preprocessed( + proof_options, + program.entry_point, + committed_bytes, + )), ); // Recompute the COMMIT output bus offset from the public output. diff --git a/prover/src/tables/register.rs b/prover/src/tables/register.rs index 34bda3e74..a4138a105 100644 --- a/prover/src/tables/register.rs +++ b/prover/src/tables/register.rs @@ -62,8 +62,8 @@ pub const NUM_PREPROCESSED_COLS: usize = 2; /// recomputes the commitment from it, the REG-C2 Memory-bus token forces it to /// equal the true final registers, and the next epoch reuses the same `R_{i+1}` /// as its preprocessed INIT — binding `init(epoch i+1) == fini(epoch i)` with no -/// extra bus. The monolithic prover keeps FINI as a main-trace column (it has no -/// verifier-known final state), using `NUM_PREPROCESSED_COLS` instead. +/// extra bus. The monolithic prover preprocesses FINI too, against the +/// verifier-known halted state (see [`halted_fini`]). pub const NUM_PREPROCESSED_COLS_WITH_FINI: usize = 3; // ========================================================================= @@ -168,6 +168,35 @@ pub(crate) fn register_init_from_entry_point(entry_point: u64) -> Vec { .collect() } +/// The final register file of every run that halts, as the verifier knows it +/// (`fini_from_trace` order): HALT zeroizes x1-x31 (x10 is read as 0), x0 is never +/// written, x254 counts the committed bytes, and the PC ends on the padding value +/// `pc = 1` (spec `halt.typ`: the verifier knows the final PC token). +/// +/// Pinning FINI is what stops the PC chain from ending anywhere but `pc = 1`. +/// HALT's `pc` column is free, so with a free FINI a prover could cancel HALT's +/// consume/emit and keep executing past the exit ecall, ending the chain on the +/// last post-exit `next_pc` (see `tests/halt_pc_forgery_poc.rs`). +pub fn halted_fini(committed_bytes: u32) -> Vec { + let mut fini = vec![0u32; NUM_REGISTER_ADDRESSES]; + fini[X254_INDEX] = committed_bytes; + fini[PC_LO_INDEX] = super::cpu::CPU_PADDING_PC as u32; + fini +} + +/// REGISTER preprocessing for a monolithic proof: OFFSET, INIT from the entry +/// point, and FINI pinned to [`halted_fini`]. +pub fn halted_preprocessed( + options: &ProofOptions, + entry_point: u64, + committed_bytes: u32, +) -> (Commitment, usize) { + let init = register_init_from_entry_point(entry_point); + let commitment = + compute_precomputed_commitment_with_fini(options, &init, &halted_fini(committed_bytes)); + (commitment, NUM_PREPROCESSED_COLS_WITH_FINI) +} + /// Build the register init map from an epoch's boundary register snapshot: the /// executor `Registers` (x1-x31, including SP) plus the program counter (x255). /// x0 and the synthetic commit index (x254) are zero in the naive version. diff --git a/prover/src/tests/halt_continuation_poc.rs b/prover/src/tests/halt_continuation_poc.rs new file mode 100644 index 000000000..88c56b9a0 --- /dev/null +++ b/prover/src/tests/halt_continuation_poc.rs @@ -0,0 +1,143 @@ +//! PoC: the HALT continue-past-exit forgery (see `halt_pc_forgery_poc`) against a +//! continuation proof. +//! +//! A continuation epoch preprocesses FINI against the bundle's `reg_fini`, which +//! the prover supplies. The verifier reuses it as the next epoch's INIT, but the +//! final epoch has no next epoch, so `verify_continuation` pins the final +//! `reg_fini` to the halted register file (`register::halted_fini`). Without that +//! check the final epoch could end its PC chain anywhere. +//! +//! Declared as a child of `continuation` so it can drive the private epoch/global +//! provers directly: a single (final) epoch, built sequentially from forged logs. + +use std::collections::HashMap; +use std::sync::Arc; + +use executor::elf::Elf; +use executor::vm::logs::Log; + +use super::*; +use crate::test_utils::asm_elf_bytes; +use crate::tests::halt_pc_forgery_poc::{ + FULL_ATTACK, GUEST, Tamper, apply_tamper, forged_logs, opts, patched_elf, run_logs, +}; + +/// A one-epoch continuation bundle for `logs`, built like `prove_continuation` +/// but with `tamper` applied to the epoch's traces before proving. `reg_fini` is +/// read from the (tampered) REGISTER trace, exactly as `prove_epoch` does. +fn craft_bundle( + elf_bytes: &[u8], + logs: &[Log], + tamper: Tamper, +) -> Result { + let opts = opts(); + let elf = Elf::load(elf_bytes).expect("ELF load"); + let decode_commitment = + crate::tables::decode::commitment_from_elf(&elf, &opts).expect("DECODE commitment"); + let decode_artifacts = DecodeArtifacts::from_elf(&elf)?; + let image = build_initial_image_paged(&elf, &[]); + let init_page_data = build_init_page_data(&image); + let mut provenance = + local_to_global::genesis_provenance(image.iter().map(|(a, v)| (a, v as u64))); + + let register_init = register::register_init_from_entry_point(elf.entry_point); + let label = local_to_global::epoch_label(0); + let collected = Traces::collect_epoch(&decode_artifacts, &image, ®ister_init, logs, true)?; + let boundary = Arc::new(local_to_global::epoch_boundary( + &mut provenance, + label, + &collected.touched_memory_cells(), + )); + let mut traces = Traces::build_from_collected( + &decode_artifacts, + collected, + None::<&HashMap>, + ®ister_init, + &MaxRowsConfig::default(), + &[], + true, + true, + #[cfg(feature = "disk-spill")] + stark::storage_mode::StorageMode::Ram, + )?; + apply_tamper(&mut traces, logs, tamper); + + let epoch = prove_epoch( + &elf, + elf_bytes, + &EpochStart { + register_init: ®ister_init, + label, + }, + traces, + true, + &boundary, + &opts, + decode_commitment, + )?; + + let boundaries = vec![boundary]; + let touched = touched_page_bases(&boundaries); + let num_private_input_pages = page::private_input_page_count(&[]); + let global = prove_global( + &boundaries, + elf_bytes, + &init_page_data, + &touched, + num_private_input_pages, + &opts, + )?; + + Ok(ContinuationProof { + epochs: vec![epoch], + global, + num_private_input_pages, + touched_page_bases: touched, + }) +} + +/// A prover-side error counts as "not accepted". +fn accepted(crafted: Result, elf: &[u8]) -> bool { + match crafted { + Ok(bundle) => verify_continuation(elf, &bundle, &opts()) + .expect("verifier must not error") + .is_some(), + Err(_) => false, + } +} + +/// POSITIVE CONTROL: the hand-built one-epoch bundle of an honest run verifies. +#[test] +fn poc_control_patched_program_continuation_verifies() { + let patched = patched_elf(&asm_elf_bytes(GUEST)); + let logs = run_logs(&patched); + assert!(accepted( + craft_bundle(&patched, &logs, Tamper::default()), + &patched + )); +} + +/// NEGATIVE CONTROL: `exit(1)` honestly is rejected. +#[test] +fn poc_control_honest_exit_one_continuation_is_rejected() { + let elf = asm_elf_bytes(GUEST); + let logs = run_logs(&elf); + assert!(!accepted( + craft_bundle(&elf, &logs, Tamper::default()), + &elf + )); +} + +/// THE BUG, continuation edition: HALT `PC = (1, 0)`, run past `exit(1)`, zero +/// x10, and end the PC chain on the last post-exit `next_pc` through the final +/// epoch's prover-supplied `reg_fini`. Must be rejected. +#[test] +fn continuation_continue_past_exit_is_rejected() { + let elf = asm_elf_bytes(GUEST); + let logs = forged_logs(&elf); + assert!( + !accepted(craft_bundle(&elf, &logs, FULL_ATTACK), &elf), + "SOUNDNESS BUG: the continuation verifier accepted a final epoch that runs \ + past the exit ecall and turns exit(1) into exit(0)" + ); +} diff --git a/prover/src/tests/halt_pc_forgery_poc.rs b/prover/src/tests/halt_pc_forgery_poc.rs new file mode 100644 index 000000000..3a9e31f9e --- /dev/null +++ b/prover/src/tests/halt_pc_forgery_poc.rs @@ -0,0 +1,293 @@ +//! PoC: execution can continue past the exit ecall. +//! +//! HALT consumes the halting row's `next_pc` token and re-emits `pc = 1` for the +//! padding chain, both at `halt_ts + 1`. Its `PC_0/PC_1` columns are not tied to +//! anything, so a prover can set them to `(1, 0)`: HALT then consumes the `1` it +//! emits itself, and the real `next_pc` token is left for another CPU row to pick +//! up. The trace keeps executing after `exit` and HALT's x10 == 0 check reads x10 +//! at `ts = 2^64 - 1`, not at the exit call. +//! +//! The guest calls `exit(1)`, which no honest prover can prove. The forgery runs +//! `li a0, 0` (+ nops) after the exit and must not verify against the same ELF. +//! +//! Production proof options, as in `page_offset_forgery_poc`. + +use crypto::fiat_shamir::default_transcript::DefaultTranscript; +use executor::elf::Elf; +use executor::vm::execution::Executor; +use executor::vm::logs::Log; +use stark::proof::options::ProofOptions; +use stark::prover::{IsStarkProver, Prover}; + +use crate::statement::{StatementKind, absorb_statement}; +use crate::tables::halt::cols as halt_cols; +use crate::tables::register::{self, cols as reg_cols}; +use crate::tables::trace_builder::Traces; +use crate::tables::types::{FE, VmTable}; +use crate::test_utils::{E, asm_elf_bytes}; +use crate::{MaxRowsConfig, VmAirs, VmProof}; + +pub(crate) const GUEST: &str = "poc_halt_continue"; + +/// `li a7, 93; ecall` — the first occurrence is the `exit(1)` call. +const EXIT_SEQ: [u8; 8] = [0x93, 0x08, 0xd0, 0x05, 0x73, 0x00, 0x00, 0x00]; +/// `addi x0, x0, 0`. +const NOP: [u8; 4] = [0x13, 0x00, 0x00, 0x00]; + +/// Rows the forged trace has: a power of two, so the CPU table gets no padding +/// rows and the last real row's `next_pc` goes straight to the REGISTER table. +const FORGED_ROWS: usize = 16; + +pub(crate) fn opts() -> ProofOptions { + crate::GoldilocksCubicProofOptions::with_blowup(2).expect("blowup=2 is valid") +} + +/// The guest with its first `ecall` replaced by a nop, so the executor runs the +/// post-exit rows and produces their logs. +pub(crate) fn patched_elf(honest: &[u8]) -> Vec { + let at = honest + .windows(EXIT_SEQ.len()) + .position(|w| w == EXIT_SEQ) + .expect("exit sequence not found"); + let mut patched = honest.to_vec(); + patched[at + 4..at + 8].copy_from_slice(&NOP); + patched +} + +pub(crate) fn run_logs(elf_bytes: &[u8]) -> Vec { + let elf = Elf::load(elf_bytes).expect("ELF load"); + Executor::new(&elf, vec![]) + .expect("executor") + .run() + .expect("run") + .logs +} + +/// The honest logs up to and including `exit(1)`, followed by the post-exit rows +/// taken from the patched run, cut at `FORGED_ROWS` (before the second ecall). +pub(crate) fn forged_logs(honest: &[u8]) -> Vec { + let honest_logs = run_logs(honest); + let exit_row = honest_logs.len() - 1; + assert_eq!( + honest_logs[exit_row].src1_val, 93, + "honest run ends on exit" + ); + + let patched_logs = run_logs(&patched_elf(honest)); + let mut logs = honest_logs; + logs.extend_from_slice(&patched_logs[exit_row + 1..FORGED_ROWS]); + assert_eq!(logs.len(), FORGED_ROWS); + assert_eq!( + logs[exit_row + 1].current_pc, + logs[exit_row].current_pc + 4, + "first post-exit row runs the instruction after the ecall" + ); + logs +} + +/// How the malicious prover deviates from the honest traces. +#[derive(Clone, Copy, Default)] +pub(crate) struct Tamper { + /// HALT `PC = (1, 0)`, so HALT's consume/emit cancel. + pub(crate) halt_pc: bool, + /// Move the REGISTER final x255 token to the last post-exit row's write + /// timestamp. Main-trace columns. + pub(crate) register_ts: bool, + /// Set the REGISTER final x255 value to the last post-exit `next_pc`. A + /// main-trace column on `main`; preprocessed (pinned to `pc = 1`) by the fix. + pub(crate) register_fini: bool, +} + +/// Every tamper of the attack: HALT PC plus the REGISTER final PC token. +pub(crate) const FULL_ATTACK: Tamper = Tamper { + halt_pc: true, + register_ts: true, + register_fini: true, +}; + +/// Apply `tamper` to traces built from `logs` (the forged post-exit run). +pub(crate) fn apply_tamper(traces: &mut Traces, logs: &[Log], tamper: Tamper) { + // Last real row writes next_pc at its timestamp + 1 (timestamps are 4i + 4). + let last_ts = (logs.len() as u64) * 4; + let last_next_pc = logs.last().unwrap().next_pc; + let reg = &mut traces.register.main_table; + let mut x255_rows = 0; + for row in 0..reg.height { + let word = match reg.get(row, reg_cols::OFFSET).to_raw() { + 510 => last_next_pc & 0xFFFF_FFFF, + 511 => last_next_pc >> 32, + _ => continue, + }; + if tamper.register_fini { + reg.set(row, reg_cols::FINI, FE::from(word)); + } + if tamper.register_ts { + reg.set(row, reg_cols::TIMESTAMP_LO, FE::from(last_ts + 1)); + reg.set(row, reg_cols::TIMESTAMP_HI, FE::zero()); + } + x255_rows += 1; + } + assert_eq!(x255_rows, 2, "x255 has two REGISTER rows"); + if tamper.halt_pc { + traces.halt.main_table.set_dword_wl(0, halt_cols::PC_0, 1); + } +} + +fn craft_proof( + elf_bytes: &[u8], + logs: &[Log], + tamper: Tamper, +) -> Result { + let options = opts(); + let program = Elf::load(elf_bytes).expect("ELF load"); + let max_rows = MaxRowsConfig::default(); + let mut traces = Traces::from_elf_and_logs( + &program, + logs, + &max_rows, + &[], + #[cfg(feature = "disk-spill")] + stark::storage_mode::StorageMode::Ram, + ) + .expect("trace build"); + + apply_tamper(&mut traces, logs, tamper); + + let table_counts = traces.table_counts(); + let airs = VmAirs::new( + &program, + &options, + false, + &traces.page_configs, + &table_counts, + None, + true, + None, + None, + // As the production prover: FINI pinned to the halted register file. + Some(register::halted_preprocessed( + &options, + program.entry_point, + u32::try_from(traces.public_output_bytes.len()).unwrap(), + )), + ); + let runtime_page_ranges = traces.runtime_page_ranges(); + let num_private_input_pages = traces + .page_configs + .iter() + .filter(|c| c.is_private_input) + .count(); + + let mut transcript = DefaultTranscript::::new(&[]); + absorb_statement( + &mut transcript, + StatementKind::Monolithic, + elf_bytes, + &traces.public_output_bytes, + &table_counts, + num_private_input_pages, + &runtime_page_ranges, + options.fri_final_poly_log_degree, + ); + + let proof = Prover::multi_prove( + airs.air_trace_pairs(&mut traces), + &mut transcript, + #[cfg(feature = "disk-spill")] + stark::storage_mode::StorageMode::Ram, + )?; + + Ok(VmProof { + proof, + runtime_page_ranges, + table_counts, + public_output: traces.public_output_bytes.clone(), + num_private_input_pages, + }) +} + +/// A prover-side error counts as "not accepted". +fn accepted(crafted: Result, elf: &[u8]) -> bool { + match crafted { + Ok(proof) => crate::verify_with_options(&proof, elf, &opts(), None, None) + .expect("verifier must not error"), + Err(_) => false, + } +} + +/// POSITIVE CONTROL: the harness itself produces valid proofs. The patched ELF +/// (no first ecall) exits 0 honestly at its second ecall. +#[test] +fn poc_control_patched_program_verifies() { + let patched = patched_elf(&asm_elf_bytes(GUEST)); + let logs = run_logs(&patched); + assert!(accepted( + craft_proof(&patched, &logs, Tamper::default()), + &patched + )); +} + +/// NEGATIVE CONTROL: `exit(1)` honestly is rejected (x10 != 0 at HALT). +#[test] +fn poc_control_honest_exit_one_is_rejected() { + let elf = asm_elf_bytes(GUEST); + let logs = run_logs(&elf); + assert!(!accepted(craft_proof(&elf, &logs, Tamper::default()), &elf)); +} + +/// NEGATIVE CONTROL: running past the exit while HALT's PC stays honest is +/// rejected — HALT consumes the real `next_pc` token, so the first post-exit +/// row has nothing to read. Isolates HALT's free PC column as the hole. +#[test] +fn poc_control_continue_without_halt_pc_tamper_is_rejected() { + let elf = asm_elf_bytes(GUEST); + let logs = forged_logs(&elf); + assert!(!accepted( + craft_proof( + &elf, + &logs, + Tamper { + halt_pc: false, + ..FULL_ATTACK + } + ), + &elf + )); +} + +/// THE BUG: set HALT `PC = (1, 0)`, keep executing after `exit(1)`, zero x10, +/// stop. Must be rejected; if this test fails the verifier accepted a proof +/// that `exit(1)` exited with code 0. +#[test] +fn continue_past_exit_via_halt_pc_is_rejected() { + let elf = asm_elf_bytes(GUEST); + let logs = forged_logs(&elf); + assert!( + !accepted(craft_proof(&elf, &logs, FULL_ATTACK), &elf), + "SOUNDNESS BUG: the verifier accepted a trace that runs past the exit ecall \ + (HALT PC = (1, 0)) and turns exit(1) into exit(0)" + ); +} + +/// THE BUG, respecting the fix's pinned FINI: HALT `PC = (1, 0)` and the final +/// x255 token moved to the end of the post-exit rows, but its value left at +/// `pc = 1`. Touches main-trace columns only, so the prover must build the +/// proof; the verifier must reject it because no real row writes `next_pc = 1`. +#[test] +fn continue_past_exit_with_pinned_fini_is_rejected() { + let elf = asm_elf_bytes(GUEST); + let logs = forged_logs(&elf); + let crafted = craft_proof( + &elf, + &logs, + Tamper { + register_fini: false, + ..FULL_ATTACK + }, + ); + assert!(crafted.is_ok(), "main-trace-only tamper must still prove"); + assert!( + !accepted(crafted, &elf), + "SOUNDNESS BUG: the PC chain ran past the exit ecall and still ended on pc = 1" + ); +} diff --git a/prover/src/tests/mod.rs b/prover/src/tests/mod.rs index 73ff6ee45..6ec729635 100644 --- a/prover/src/tests/mod.rs +++ b/prover/src/tests/mod.rs @@ -47,6 +47,8 @@ pub mod ecsm_tests; #[cfg(test)] pub mod eq_tests; #[cfg(test)] +pub mod halt_pc_forgery_poc; +#[cfg(test)] pub mod hint_tests; #[cfg(test)] pub mod ir_stats_dump; diff --git a/prover/src/tests/page_offset_forgery_poc.rs b/prover/src/tests/page_offset_forgery_poc.rs index 5e2e24d78..340e665f7 100644 --- a/prover/src/tests/page_offset_forgery_poc.rs +++ b/prover/src/tests/page_offset_forgery_poc.rs @@ -181,7 +181,12 @@ fn craft_proof( true, None, None, - None, + // As the production prover: FINI pinned to the halted register file. + Some(crate::tables::register::halted_preprocessed( + &options, + program.entry_point, + u32::try_from(traces.public_output_bytes.len()).unwrap(), + )), ); let runtime_page_ranges = traces.runtime_page_ranges(); @@ -692,7 +697,12 @@ fn craft_proof_with_duplicate_page( true, None, None, - None, + // As the production prover: FINI pinned to the halted register file. + Some(crate::tables::register::halted_preprocessed( + &options, + program.entry_point, + u32::try_from(traces.public_output_bytes.len()).unwrap(), + )), ); let mut transcript = DefaultTranscript::::new(&[]); diff --git a/prover/src/tests/recursion_soundness_gap_poc.rs b/prover/src/tests/recursion_soundness_gap_poc.rs index 73410ff62..92d410dbd 100644 --- a/prover/src/tests/recursion_soundness_gap_poc.rs +++ b/prover/src/tests/recursion_soundness_gap_poc.rs @@ -157,7 +157,12 @@ fn custom_prove_with_statement_elf( true, None, None, - None, + // As the production prover: FINI pinned to the halted register file. + Some(crate::tables::register::halted_preprocessed( + opts, + program.entry_point, + u32::try_from(traces.public_output_bytes.len()).unwrap(), + )), ); let runtime_page_ranges = traces.runtime_page_ranges(); From a2f7b8379e1998aa5ab921b098d78d29e1aea3d2 Mon Sep 17 00:00:00 2001 From: Nicole Date: Wed, 14 Oct 2026 11:22:20 -0300 Subject: [PATCH 2/8] Remove the two-column REGISTER layout so every proof pins its final register file --- prover/src/continuation.rs | 7 +- prover/src/lib.rs | 40 ++----- prover/src/tables/register.rs | 79 ++++--------- prover/src/tables/trace_builder.rs | 4 +- prover/src/test_utils.rs | 27 +++++ prover/src/tests/halt_pc_forgery_poc.rs | 11 +- prover/src/tests/page_offset_forgery_poc.rs | 18 ++- prover/src/tests/prove_elfs_tests.rs | 108 +++++++++++------- .../src/tests/recursion_soundness_gap_poc.rs | 7 +- prover/src/tests/register_tests.rs | 3 - prover/src/tests/skip_empty_tables_tests.rs | 10 +- 11 files changed, 152 insertions(+), 162 deletions(-) diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index f37718b2e..b3744963d 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -661,10 +661,6 @@ fn build_epoch_airs( // final register file is a verifier-known public value bound by the REG-C2 // Memory-bus token; reusing the same R_{i+1} as the next epoch's INIT binds // init(epoch i+1) == fini(epoch i). - let register_preprocessed = Some(( - register::compute_precomputed_commitment_with_fini(opts, register_init, reg_fini), - register::NUM_PREPROCESSED_COLS_WITH_FINI, - )); VmAirs::new( elf, opts, @@ -674,8 +670,7 @@ fn build_epoch_airs( decode_commitment, is_final, None, - None, - register_preprocessed, + register::compute_precomputed_commitment_with_fini(opts, register_init, reg_fini), ) } diff --git a/prover/src/lib.rs b/prover/src/lib.rs index 48d472be0..3238182b8 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -840,6 +840,10 @@ impl VmAirs { /// caller-constant root is rejected (mismatches the proof root or diverges /// Fiat-Shamir); a consistent prover-supplied mismatch is NOT — such /// callers must bind identity externally (see `recursion::check_attestation`). + /// + /// `register_commitment` is the REGISTER preprocessed root (OFFSET, INIT, + /// FINI): [`register::halted_commitment`] for a monolithic proof, or the + /// epoch's `R_i`/`R_{i+1}` for a continuation epoch. #[allow(clippy::too_many_arguments)] pub fn new( elf: &Elf, @@ -849,9 +853,8 @@ impl VmAirs { table_counts: &TableCounts, decode_commitment: Option, include_halt: bool, - register_init: Option<&[u32]>, page_commitments: Option<&[(u64, Commitment)]>, - register_preprocessed: Option<(Commitment, usize)>, + register_commitment: Commitment, ) -> Self { let cpus: Vec<_> = (0..table_counts.cpu) .map(|i| { @@ -971,21 +974,10 @@ impl VmAirs { 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( - create_register_air(proof_options) - .with_preprocessed(commitment, num_preprocessed_cols), - ) - } else { - let register_init = register_init - .map(<[u32]>::to_vec) - .unwrap_or_else(|| register::register_init_from_entry_point(elf.entry_point)); - Box::new(create_register_air(proof_options).with_preprocessed( - register::preprocessed_commitment(proof_options, ®ister_init), - register::NUM_PREPROCESSED_COLS, - )) - }; + let register: VmAir = Box::new(create_register_air(proof_options).with_preprocessed( + register_commitment, + register::NUM_PREPROCESSED_COLS_WITH_FINI, + )); // Every zero-init page shares one preprocessed commitment: OFFSET is // page-relative and INIT is all-zero, so it depends only on // (blowup, coset) — all fixed here. Compute it once (static const @@ -1358,12 +1350,7 @@ pub fn prove_with_options_and_inputs( None, true, None, - None, - Some(register::halted_preprocessed( - proof_options, - program.entry_point, - committed_bytes, - )), + register::halted_commitment(proof_options, program.entry_point, committed_bytes), ); #[cfg(feature = "instruments")] @@ -1607,13 +1594,8 @@ fn verify_proof_parts( table_counts, decode_commitment, true, - None, page_commitments, - Some(register::halted_preprocessed( - proof_options, - program.entry_point, - committed_bytes, - )), + register::halted_commitment(proof_options, program.entry_point, committed_bytes), ); // Recompute the COMMIT output bus offset from the public output. diff --git a/prover/src/tables/register.rs b/prover/src/tables/register.rs index a4138a105..75be02394 100644 --- a/prover/src/tables/register.rs +++ b/prover/src/tables/register.rs @@ -51,19 +51,16 @@ pub const WORDS_PER_REGISTER: usize = 2; /// -1 because x254 is single-word (1 address instead of 2). pub const NUM_REGISTER_ADDRESSES: usize = NUM_REGISTERS * WORDS_PER_REGISTER - 1; -/// Number of preprocessed columns (OFFSET, INIT) for the monolithic prover. -/// OFFSET encodes the Word address, INIT holds the initial value. -/// Program-dependent: x255 init = ELF entry point. -pub const NUM_PREPROCESSED_COLS: usize = 2; - -/// Number of preprocessed columns (OFFSET, INIT, FINI) for continuation epochs. -/// A continuation epoch additionally preprocesses FINI so the epoch's final -/// register file becomes a verifier-known public value (`R_{i+1}`): the verifier -/// recomputes the commitment from it, the REG-C2 Memory-bus token forces it to -/// equal the true final registers, and the next epoch reuses the same `R_{i+1}` -/// as its preprocessed INIT — binding `init(epoch i+1) == fini(epoch i)` with no -/// extra bus. The monolithic prover preprocesses FINI too, against the -/// verifier-known halted state (see [`halted_fini`]). +/// Number of preprocessed columns (OFFSET, INIT, FINI). OFFSET encodes the Word +/// address, INIT the initial value and FINI the final one, so both register files +/// are verifier-known public values: the verifier recomputes the commitment from +/// them and the REG-C2 Memory-bus token forces FINI to equal the true final +/// registers. +/// +/// A continuation epoch preprocesses FINI = `R_{i+1}` and the next epoch reuses it +/// as its INIT, binding `init(epoch i+1) == fini(epoch i)` with no extra bus. A +/// monolithic proof (and the final epoch) pins FINI to the halted state (see +/// [`halted_fini`]). pub const NUM_PREPROCESSED_COLS_WITH_FINI: usize = 3; // ========================================================================= @@ -184,17 +181,15 @@ pub fn halted_fini(committed_bytes: u32) -> Vec { fini } -/// REGISTER preprocessing for a monolithic proof: OFFSET, INIT from the entry -/// point, and FINI pinned to [`halted_fini`]. -pub fn halted_preprocessed( +/// REGISTER preprocessed commitment for a monolithic proof: OFFSET, INIT from the +/// entry point, and FINI pinned to [`halted_fini`]. +pub fn halted_commitment( options: &ProofOptions, entry_point: u64, committed_bytes: u32, -) -> (Commitment, usize) { +) -> Commitment { let init = register_init_from_entry_point(entry_point); - let commitment = - compute_precomputed_commitment_with_fini(options, &init, &halted_fini(committed_bytes)); - (commitment, NUM_PREPROCESSED_COLS_WITH_FINI) + compute_precomputed_commitment_with_fini(options, &init, &halted_fini(committed_bytes)) } /// Build the register init map from an epoch's boundary register snapshot: the @@ -323,33 +318,13 @@ pub fn fini_from_final_state(final_state: &FinalRegisterStateMap, init: &[u32]) // Preprocessed commitment // ========================================================================= -/// Computes the Merkle root commitment over the LDE of REGISTER precomputed columns. -/// -/// Program-dependent: x255 (PC) init = entry_point. -/// OFFSET encodes the Word address (0..63 for x0-x31, 508 for x254, 510-511 for x255). -/// INIT holds the initial value (SP=STACK_TOP, PC=entry_point, rest=0). -pub fn compute_precomputed_commitment(options: &ProofOptions, init: &[u32]) -> Commitment { - let num_rows = NUM_REGISTER_ADDRESSES.next_power_of_two(); - let addr_list = register_word_address_list(); - - let mut offset_col = crate::tables::types::zeroed_fe_vec(num_rows); - let mut init_col = crate::tables::types::zeroed_fe_vec(num_rows); - - for i in 0..NUM_REGISTER_ADDRESSES { - offset_col[i] = FE::from(addr_list[i]); - init_col[i] = FE::from(init.get(i).copied().unwrap_or(0) as u64); - } - - commit_register_columns(options, vec![offset_col, init_col]) -} - -/// Continuation variant: commits OFFSET + INIT + FINI, so the verifier recomputes -/// the commitment from the public `init` (`R_i`) and `fini` (`R_{i+1}`) and the -/// proof's FINI column is locked to `R_{i+1}`. `fini` is the vector produced by -/// `fini_from_trace` (entry `i` = the register at `register_word_address_list()[i]`). -/// Used by continuation epochs with `NUM_PREPROCESSED_COLS_WITH_FINI`; must match -/// the column order of the REGISTER trace (OFFSET, INIT, FINI), and FINI on padding -/// rows is 0 (as the trace builds it). +/// Computes the Merkle root commitment over the LDE of the REGISTER preprocessed +/// columns: OFFSET (the Word address: 0..63 for x0-x31, 508 for x254, 510-511 for +/// x255), INIT and FINI, so the verifier recomputes it from the public `init` and +/// `fini` and the proof's FINI column is locked to `fini`. `fini` is the vector +/// produced by `fini_from_trace` (entry `i` = the register at +/// `register_word_address_list()[i]`). Must match the column order of the REGISTER +/// trace (OFFSET, INIT, FINI), and FINI on padding rows is 0 (as the trace builds it). pub fn compute_precomputed_commitment_with_fini( options: &ProofOptions, init: &[u32], @@ -373,8 +348,7 @@ pub fn compute_precomputed_commitment_with_fini( } /// LDE + bit-reverse + Merkle-commit the given preprocessed columns (in column -/// order). Shared by the monolithic (OFFSET, INIT) and continuation -/// (OFFSET, INIT, FINI) preprocessed commitments. +/// order). fn commit_register_columns(options: &ProofOptions, columns: Vec>) -> Commitment { let num_rows = NUM_REGISTER_ADDRESSES.next_power_of_two(); let polys: Vec> = columns @@ -400,13 +374,6 @@ fn commit_register_columns(options: &ProofOptions, columns: Vec>) -> Com root } -/// Returns the preprocessed commitment for the REGISTER table. -/// -/// Program-dependent (entry_point varies per ELF), so not globally cached. -pub fn preprocessed_commitment(options: &ProofOptions, init: &[u32]) -> Commitment { - compute_precomputed_commitment(options, init) -} - // ========================================================================= // Bus interactions // ========================================================================= diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index c3b695a80..29c612513 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -4189,7 +4189,7 @@ impl Traces { /// `main_area` — for apples-to-apples comparison with other zkVMs. /// /// Preprocessed columns (committed in a separate PCS round during setup, not at - /// proving time) are excluded: BITWISE (11), DECODE (5), REGISTER (2), PAGE (2). + /// proving time) are excluded: BITWISE (11), DECODE (5), REGISTER (3), PAGE (2). pub fn total_field_elements(&self) -> u64 { use super::bitwise::NUM_PRECOMPUTED_COLS as BITWISE_PRECOMPUTED; use super::bitwise::cols::NUM_COLUMNS as BITWISE_COLS; @@ -4218,7 +4218,7 @@ impl Traces { use super::mul::cols::NUM_COLUMNS as MUL_COLS; use super::page::NUM_PREPROCESSED_COLS as PAGE_PREPROCESSED; use super::page::cols::NUM_COLUMNS as PAGE_COLS; - use super::register::NUM_PREPROCESSED_COLS as REGISTER_PREPROCESSED; + use super::register::NUM_PREPROCESSED_COLS_WITH_FINI as REGISTER_PREPROCESSED; use super::register::cols::NUM_COLUMNS as REGISTER_COLS; use super::shift::cols::NUM_COLUMNS as SHIFT_COLS; use super::store::cols::NUM_COLUMNS as STORE_COLS; diff --git a/prover/src/test_utils.rs b/prover/src/test_utils.rs index 5b4206356..f1a2dac8a 100644 --- a/prover/src/test_utils.rs +++ b/prover/src/test_utils.rs @@ -220,6 +220,33 @@ pub fn is_halfword_sender_columns(interactions: &[BusInteraction]) -> Vec .collect() } +// ============================================================================= +// REGISTER Commitment Helpers +// ============================================================================= + +/// REGISTER commitment for a monolithic proof of `elf` that committed +/// `public_output`: FINI pinned to the halted state, as the production prover and +/// verifier build it. +pub fn halted_register_commitment( + options: &ProofOptions, + elf: &Elf, + public_output: &[u8], +) -> stark::config::Commitment { + let committed_bytes = u32::try_from(public_output.len()).expect("public output fits in u32"); + crate::tables::register::halted_commitment(options, elf.entry_point, committed_bytes) +} + +/// REGISTER commitment for the traces of a non-final epoch: INIT `init` and FINI +/// as the REGISTER trace holds it, as a continuation epoch commits it. +pub fn epoch_register_commitment( + options: &ProofOptions, + init: &[u32], + traces: &crate::tables::trace_builder::Traces, +) -> stark::config::Commitment { + let fini = crate::tables::register::fini_from_trace(&traces.register); + crate::tables::register::compute_precomputed_commitment_with_fini(options, init, &fini) +} + // ============================================================================= // ELF Execution Helpers // ============================================================================= diff --git a/prover/src/tests/halt_pc_forgery_poc.rs b/prover/src/tests/halt_pc_forgery_poc.rs index 3a9e31f9e..1c0fc9a25 100644 --- a/prover/src/tests/halt_pc_forgery_poc.rs +++ b/prover/src/tests/halt_pc_forgery_poc.rs @@ -21,7 +21,7 @@ use stark::prover::{IsStarkProver, Prover}; use crate::statement::{StatementKind, absorb_statement}; use crate::tables::halt::cols as halt_cols; -use crate::tables::register::{self, cols as reg_cols}; +use crate::tables::register::cols as reg_cols; use crate::tables::trace_builder::Traces; use crate::tables::types::{FE, VmTable}; use crate::test_utils::{E, asm_elf_bytes}; @@ -163,13 +163,12 @@ fn craft_proof( None, true, None, - None, // As the production prover: FINI pinned to the halted register file. - Some(register::halted_preprocessed( + crate::test_utils::halted_register_commitment( &options, - program.entry_point, - u32::try_from(traces.public_output_bytes.len()).unwrap(), - )), + &program, + &traces.public_output_bytes, + ), ); let runtime_page_ranges = traces.runtime_page_ranges(); let num_private_input_pages = traces diff --git a/prover/src/tests/page_offset_forgery_poc.rs b/prover/src/tests/page_offset_forgery_poc.rs index 340e665f7..9993ceb7c 100644 --- a/prover/src/tests/page_offset_forgery_poc.rs +++ b/prover/src/tests/page_offset_forgery_poc.rs @@ -180,13 +180,12 @@ fn craft_proof( None, true, None, - None, // As the production prover: FINI pinned to the halted register file. - Some(crate::tables::register::halted_preprocessed( + crate::test_utils::halted_register_commitment( &options, - program.entry_point, - u32::try_from(traces.public_output_bytes.len()).unwrap(), - )), + &program, + &traces.public_output_bytes, + ), ); let runtime_page_ranges = traces.runtime_page_ranges(); @@ -696,13 +695,12 @@ fn craft_proof_with_duplicate_page( None, true, None, - None, // As the production prover: FINI pinned to the halted register file. - Some(crate::tables::register::halted_preprocessed( + crate::test_utils::halted_register_commitment( &options, - program.entry_point, - u32::try_from(traces.public_output_bytes.len()).unwrap(), - )), + &program, + &traces.public_output_bytes, + ), ); let mut transcript = DefaultTranscript::::new(&[]); diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index 2707e67af..9c2e5c3d1 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -105,8 +105,14 @@ pub(crate) fn weigh_the_bus( let _ = env_logger::builder().is_test(true).try_init(); let proof_options = ProofOptions::default_test_options(); - // Create all AIRs including PAGE and REGISTER tables + // Create all AIRs including PAGE and REGISTER tables. REGISTER FINI is read + // off the trace, not pinned to the halted state: a forgery that drops the + // committed output would otherwise also fail the REGISTER preprocessed root + // (x254 != output length), and the bus balance is what is being weighed here. let table_counts = traces.table_counts(); + let register_init = crate::tables::register::register_init_from_entry_point(elf.entry_point); + let register_commitment = + crate::test_utils::epoch_register_commitment(&proof_options, ®ister_init, traces); let airs = VmAirs::new( elf, &proof_options, @@ -116,8 +122,7 @@ pub(crate) fn weigh_the_bus( None, true, None, - None, - None, + register_commitment, ); // Build air_trace_pairs for all tables @@ -208,8 +213,11 @@ fn prove_vm_minimal(elf_bytes: &[u8], private_inputs: &[u8], max_rows: &MaxRowsC None, true, None, - None, - None, + crate::test_utils::halted_register_commitment( + &proof_options, + &elf, + &traces.public_output_bytes, + ), ); let runtime_page_ranges = traces.runtime_page_ranges(); let proof = multi_prove_ram( @@ -253,8 +261,11 @@ fn verify_vm_minimal(vm_proof: &VmProof, elf_bytes: &[u8]) -> bool { None, true, None, - None, - None, + crate::test_utils::halted_register_commitment( + &proof_options, + &elf, + &vm_proof.public_output, + ), ); let air_refs = airs.air_refs(); let views: Vec> = vm_proof @@ -1787,8 +1798,11 @@ fn test_prove_elfs_test_commit_4_wrong_pages_rejected() { None, true, None, - None, - None, + crate::test_utils::halted_register_commitment( + &proof_options, + &elf, + &traces.public_output_bytes, + ), ); let proof = multi_prove_ram( prover_airs.air_trace_pairs(&mut traces), @@ -1808,8 +1822,11 @@ fn test_prove_elfs_test_commit_4_wrong_pages_rejected() { None, true, None, - None, - None, + crate::test_utils::halted_register_commitment( + &proof_options, + &elf, + &traces.public_output_bytes, + ), ); let verifier_air_refs = verifier_airs.air_refs(); let views: Vec> = @@ -2544,8 +2561,11 @@ fn test_deep_stack_runtime_pages_roundtrip() { None, true, None, - None, - None, + crate::test_utils::halted_register_commitment( + &proof_options, + &elf, + &traces.public_output_bytes, + ), ); let proof = multi_prove_ram( prover_airs.air_trace_pairs(&mut traces), @@ -2565,8 +2585,11 @@ fn test_deep_stack_runtime_pages_roundtrip() { None, true, None, - None, - None, + crate::test_utils::halted_register_commitment( + &proof_options, + &elf, + &traces.public_output_bytes, + ), ); let verifier_air_refs = verifier_airs.air_refs(); let views: Vec> = @@ -2621,8 +2644,11 @@ fn test_deep_stack_missing_pages_rejected() { None, true, None, - None, - None, + crate::test_utils::halted_register_commitment( + &proof_options, + &elf, + &traces.public_output_bytes, + ), ); let proof = multi_prove_ram( prover_airs.air_trace_pairs(&mut traces), @@ -2641,8 +2667,11 @@ fn test_deep_stack_missing_pages_rejected() { None, true, None, - None, - None, + crate::test_utils::halted_register_commitment( + &proof_options, + &elf, + &traces.public_output_bytes, + ), ); let verifier_air_refs = verifier_airs.air_refs(); let views: Vec> = @@ -2732,8 +2761,11 @@ fn test_heap_alloc_runtime_pages_roundtrip() { None, true, None, - None, - None, + crate::test_utils::halted_register_commitment( + &proof_options, + &elf, + &traces.public_output_bytes, + ), ); let proof = multi_prove_ram( prover_airs.air_trace_pairs(&mut traces), @@ -2753,8 +2785,11 @@ fn test_heap_alloc_runtime_pages_roundtrip() { None, true, None, - None, - None, + crate::test_utils::halted_register_commitment( + &proof_options, + &elf, + &traces.public_output_bytes, + ), ); let verifier_air_refs = verifier_airs.air_refs(); let views: Vec> = @@ -2946,8 +2981,7 @@ fn test_crafted_zero_count_proof_must_not_verify() { None, true, None, - None, - None, + crate::test_utils::halted_register_commitment(&proof_options, &elf, &[]), ); let verifier_air_refs = airs.air_refs(); @@ -3429,8 +3463,7 @@ fn test_prove_first_epoch_without_halt() { None, false, None, - None, - None, + crate::test_utils::epoch_register_commitment(&proof_options, ®ister_init, &traces), ); let multi_proof = multi_prove_ram( @@ -3517,9 +3550,8 @@ fn test_prove_second_epoch_from_snapshot() { &table_counts, None, false, - Some(®ister_init), - None, None, + crate::test_utils::epoch_register_commitment(&proof_options, ®ister_init, &traces), ); let multi_proof = multi_prove_ram( @@ -3614,8 +3646,7 @@ fn test_epoch_proof_commits_l2g() { None, false, None, - None, - None, + crate::test_utils::epoch_register_commitment(&proof_options, ®ister_init, &traces), ); // Inert L2G AIR: commits the trace columns, but no bus and no constraints. @@ -3763,11 +3794,6 @@ fn test_continuation_pipeline_end_to_end() { .unwrap(); let table_counts = traces.table_counts(); - let register_init_arg = if i == 0 { - None - } else { - Some(register_inits[i].as_slice()) - }; let airs = VmAirs::new( &elf, &proof_options, @@ -3776,9 +3802,12 @@ fn test_continuation_pipeline_end_to_end() { &table_counts, None, is_final, - register_init_arg, - None, None, + crate::test_utils::epoch_register_commitment( + &proof_options, + ®ister_inits[i], + &traces, + ), ); let mut l2g_trace = local_to_global::generate_local_to_global_trace(&boundaries[i]); @@ -3914,8 +3943,7 @@ fn test_epoch_memory_bus_with_l2g_bookend() { None, false, None, - None, - None, + crate::test_utils::epoch_register_commitment(&proof_options, ®ister_init, &traces), ); // L2G air on the epoch-local Memory bus (the bookend that replaces PAGE). diff --git a/prover/src/tests/recursion_soundness_gap_poc.rs b/prover/src/tests/recursion_soundness_gap_poc.rs index 92d410dbd..d91af5044 100644 --- a/prover/src/tests/recursion_soundness_gap_poc.rs +++ b/prover/src/tests/recursion_soundness_gap_poc.rs @@ -156,13 +156,8 @@ fn custom_prove_with_statement_elf( None, true, None, - None, // As the production prover: FINI pinned to the halted register file. - Some(crate::tables::register::halted_preprocessed( - opts, - program.entry_point, - u32::try_from(traces.public_output_bytes.len()).unwrap(), - )), + crate::test_utils::halted_register_commitment(opts, &program, &traces.public_output_bytes), ); let runtime_page_ranges = traces.runtime_page_ranges(); diff --git a/prover/src/tests/register_tests.rs b/prover/src/tests/register_tests.rs index 66dcd2662..abe7daf2d 100644 --- a/prover/src/tests/register_tests.rs +++ b/prover/src/tests/register_tests.rs @@ -129,9 +129,6 @@ fn test_precomputed_commitment_with_fini_binds_fini() { // fails the verifier's preprocessed-root check. assert_eq!(root_a, root_a2); assert_ne!(root_a, root_b); - - // The 3-column (with-fini) commitment differs from the 2-column monolithic one. - assert_ne!(root_a, compute_precomputed_commitment(&opts, &init)); } /// `fini_from_final_state` must return exactly what `fini_from_trace` reads off diff --git a/prover/src/tests/skip_empty_tables_tests.rs b/prover/src/tests/skip_empty_tables_tests.rs index 8fef3d190..49f4e2947 100644 --- a/prover/src/tests/skip_empty_tables_tests.rs +++ b/prover/src/tests/skip_empty_tables_tests.rs @@ -110,8 +110,11 @@ fn every_table_participates_in_the_bus() { None, true, None, - None, - None, + crate::test_utils::halted_register_commitment( + &ProofOptions::default_test_options(), + &elf, + &traces.public_output_bytes, + ), ); let without_bus: Vec<&str> = airs @@ -344,8 +347,7 @@ fn dropping_a_used_table_through_the_real_verifier_is_rejected() { None, true, None, - None, - None, + crate::test_utils::halted_register_commitment(&opts, &elf, &vm_proof.public_output), ); let mul_at = airs .air_refs() From 92ebfbbf2fd8586e5e60228e3969f43ef9d3f5bf Mon Sep 17 00:00:00 2001 From: Nicole Date: Wed, 14 Oct 2026 11:25:41 -0300 Subject: [PATCH 3/8] Update the continuation design doc: monolithic proofs now pin FINI to the halted state --- docs/continuations_design.md | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/docs/continuations_design.md b/docs/continuations_design.md index 0c1095cb0..ba1658d92 100644 --- a/docs/continuations_design.md +++ b/docs/continuations_design.md @@ -469,8 +469,11 @@ locks compose: Compose them: public `R_{i+1}` = trace FINI = real last write. So the value handed to the next epoch is pinned to real execution. -The **monolithic prover is unchanged**: it keeps FINI as a main-trace column (it -has no verifier-known final state) and preprocesses 2 columns, not 3. +The **monolithic prover** preprocesses the same 3 columns, with FINI pinned to the +halted register file (`register::halted_fini`): x1-x31 = 0, x254 = the committed +byte count, and the PC = 1. The final epoch's `R_{i+1}` must equal that same +halted state. Pinning it ends the PC chain on `pc = 1`, so execution cannot +continue past the exit ecall. ### Commit index (x254) From eb0c8a642654107ec819dc93f939fb59d056ecfa Mon Sep 17 00:00:00 2001 From: Nicole Date: Wed, 14 Oct 2026 12:48:14 -0300 Subject: [PATCH 4/8] Make the halt PoCs reach the verifier and cover a two-epoch forgery --- docs/continuations_design.md | 10 +- executor/programs/asm/poc_halt_continue.s | 7 + prover/src/lib.rs | 4 +- prover/src/tables/register.rs | 22 ++- prover/src/test_utils.rs | 8 +- prover/src/tests/halt_continuation_poc.rs | 169 ++++++++++++++++------ prover/src/tests/halt_pc_forgery_poc.rs | 99 ++++++++----- prover/src/tests/prove_elfs_tests.rs | 12 +- 8 files changed, 224 insertions(+), 107 deletions(-) diff --git a/docs/continuations_design.md b/docs/continuations_design.md index ba1658d92..d571bc255 100644 --- a/docs/continuations_design.md +++ b/docs/continuations_design.md @@ -440,9 +440,9 @@ global telescoping — we bind the whole snapshot directly. **Mechanism (no new bus).** The REGISTER table is the register analog of PAGE — it already puts each register's init/fini tokens on the epoch-local Memory bus -(REG-C1 init, REG-C2 fini, matched against MEMW). For continuation epochs we -**also preprocess the FINI column** = the epoch's final register file `R_{i+1}` -(on top of the already-preprocessed INIT = `R_i`). "Preprocessed" means +(REG-C1 init, REG-C2 fini, matched against MEMW). Every REGISTER table +**preprocesses the FINI column** as well as INIT. For a continuation epoch, FINI +is the epoch's final register file `R_{i+1}` (and INIT = `R_i`). "Preprocessed" means *verifier-known*: the verifier recomputes the column's commitment, so the prover cannot choose it. The verifier reuses the **same** `R_{i+1}` as epoch *i*'s FINI and epoch *i+1*'s INIT, so `init(i+1) == fini(i)` **by construction** — no equality @@ -644,7 +644,9 @@ recursion/aggregation layer (deferred). committed/private for private-input pages, §3.6) and finalization anchors. - `prover/src/tables/register.rs` — the REGISTER table: REG-C1/REG-C2 Memory-bus tokens, the preprocessed FINI commitment (`compute_precomputed_commitment_with_fini`, - `NUM_PREPROCESSED_COLS_WITH_FINI`), and `fini_from_trace`. + `NUM_PREPROCESSED_COLS_WITH_FINI`), `fini_from_trace`, and the halted register + file that monolithic proofs and the final epoch pin FINI to (`halted_fini`, + `halted_commitment`). - `prover/src/statement.rs` — the Fiat-Shamir statement absorbers (`absorb_statement` with `StatementKind`, `absorb_continuation_global_statement`). - `prover/src/continuation.rs` — the split prover/verifier: `prove_continuation` / diff --git a/executor/programs/asm/poc_halt_continue.s b/executor/programs/asm/poc_halt_continue.s index 544b70716..9405ee55c 100644 --- a/executor/programs/asm/poc_halt_continue.s +++ b/executor/programs/asm/poc_halt_continue.s @@ -2,6 +2,11 @@ .attribute 5, "rv64i2p1" .globl main main: + # Two rows before the exit sequence, so the rows before the exit ecall fill a + # power-of-two continuation epoch (4 rows) on their own. + nop + nop + # Exit with a NON-ZERO code. HALT enforces x10 == 0, so an honest prover # cannot prove this program. li a0, 1 @@ -23,6 +28,8 @@ main: nop nop nop + nop + nop # Lets the PoC's patched copy (first ecall -> nop) terminate in the executor. li a7, 93 diff --git a/prover/src/lib.rs b/prover/src/lib.rs index 3238182b8..0cd67930a 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -1581,8 +1581,8 @@ fn verify_proof_parts( } // The final register file is verifier-known: pinning it ends the PC chain on - // `pc = 1` (see `register::halted_fini`). - // An honest run cannot commit more bytes than x254 counts. + // `pc = 1` (see `register::halted_fini`). x254 is a u32 byte count, so a longer + // public output cannot be honest. let Ok(committed_bytes) = u32::try_from(public_output.len()) else { return Ok(false); }; diff --git a/prover/src/tables/register.rs b/prover/src/tables/register.rs index 75be02394..de9ee5064 100644 --- a/prover/src/tables/register.rs +++ b/prover/src/tables/register.rs @@ -13,10 +13,14 @@ //! //! | Column | Type | Description | //! |--------|------|-------------| -//! | offset | RowIndex | Byte offset within register space | -//! | init | Word | Initial value (0 for all registers at start) | -//! | fini | Word | Final value after execution | +//! | offset | RowIndex | Word address within register space (preprocessed) | +//! | init | Word | Initial value (preprocessed) | +//! | fini | Word | Final value (preprocessed) | //! | timestamp | DWordWL | Final timestamp (1 if never accessed) | +//! +//! OFFSET, INIT and FINI are preprocessed, so the verifier knows both register +//! files. A monolithic proof (and the final continuation epoch) pins FINI to the +//! halted state ([`halted_fini`]); a non-final epoch's FINI is the next epoch's INIT. use std::collections::HashMap; @@ -71,10 +75,10 @@ pub mod cols { /// offset: Row index / byte address within register space pub const OFFSET: usize = 0; - /// init: Initial byte value (0 for all registers) + /// init: Initial Word value (preprocessed) pub const INIT: usize = 1; - /// fini: Final byte value after execution + /// fini: Final Word value (preprocessed) pub const FINI: usize = 2; /// timestamp[0]: Final timestamp low word (1 if never accessed, matching REG-C1 init) @@ -168,12 +172,18 @@ pub(crate) fn register_init_from_entry_point(entry_point: u64) -> Vec { /// The final register file of every run that halts, as the verifier knows it /// (`fini_from_trace` order): HALT zeroizes x1-x31 (x10 is read as 0), x0 is never /// written, x254 counts the committed bytes, and the PC ends on the padding value -/// `pc = 1` (spec `halt.typ`: the verifier knows the final PC token). +/// `pc = 1`. /// /// Pinning FINI is what stops the PC chain from ending anywhere but `pc = 1`. /// HALT's `pc` column is free, so with a free FINI a prover could cancel HALT's /// consume/emit and keep executing past the exit ecall, ending the chain on the /// last post-exit `next_pc` (see `tests/halt_pc_forgery_poc.rs`). +/// +/// Only the final PC *value* is pinned; its timestamp (REGISTER TIMESTAMP) stays +/// prover-chosen, unlike spec `halt.typ`, which has the verifier know the final +/// padding-PC timestamp. The value is enough: no real row writes `next_pc = 1` +/// (instruction addresses are even and BRANCH clears the LSB), so a token with +/// value 1 can only come from HALT's emit or a padding row after it. pub fn halted_fini(committed_bytes: u32) -> Vec { let mut fini = vec![0u32; NUM_REGISTER_ADDRESSES]; fini[X254_INDEX] = committed_bytes; diff --git a/prover/src/test_utils.rs b/prover/src/test_utils.rs index f1a2dac8a..d2a569e6d 100644 --- a/prover/src/test_utils.rs +++ b/prover/src/test_utils.rs @@ -236,9 +236,11 @@ pub fn halted_register_commitment( crate::tables::register::halted_commitment(options, elf.entry_point, committed_bytes) } -/// REGISTER commitment for the traces of a non-final epoch: INIT `init` and FINI -/// as the REGISTER trace holds it, as a continuation epoch commits it. -pub fn epoch_register_commitment( +/// REGISTER commitment matching `traces`: INIT `init` and FINI as the REGISTER +/// trace holds it. This is what a prover commits for its own trace (a non-final +/// continuation epoch does it honestly; a forged run gets a root the halted +/// verifier does not recompute). +pub fn trace_register_commitment( options: &ProofOptions, init: &[u32], traces: &crate::tables::trace_builder::Traces, diff --git a/prover/src/tests/halt_continuation_poc.rs b/prover/src/tests/halt_continuation_poc.rs index 88c56b9a0..50de6b654 100644 --- a/prover/src/tests/halt_continuation_poc.rs +++ b/prover/src/tests/halt_continuation_poc.rs @@ -8,7 +8,8 @@ //! check the final epoch could end its PC chain anywhere. //! //! Declared as a child of `continuation` so it can drive the private epoch/global -//! provers directly: a single (final) epoch, built sequentially from forged logs. +//! provers directly: epochs built sequentially from forged logs, as +//! `prove_continuation` builds them. use std::collections::HashMap; use std::sync::Arc; @@ -19,64 +20,94 @@ use executor::vm::logs::Log; use super::*; use crate::test_utils::asm_elf_bytes; use crate::tests::halt_pc_forgery_poc::{ - FULL_ATTACK, GUEST, Tamper, apply_tamper, forged_logs, opts, patched_elf, run_logs, + FORGED_ROWS, FULL_ATTACK, GUEST, Tamper, apply_tamper, forged_logs, opts, patched_elf, run_logs, }; -/// A one-epoch continuation bundle for `logs`, built like `prove_continuation` -/// but with `tamper` applied to the epoch's traces before proving. `reg_fini` is -/// read from the (tampered) REGISTER trace, exactly as `prove_epoch` does. +/// Rows of the guest before its exit ecall: a power of two, so they fill a +/// non-final epoch on their own and the exit lands in the next one. +const PRE_EXIT_ROWS: usize = 4; + +/// A continuation bundle for `logs`, built like `prove_continuation`: one epoch per +/// entry of `epoch_lens` (non-final epochs a power of two), with `tamper` applied +/// to the final epoch's traces before proving. Each `reg_fini` is read from the +/// (tampered) REGISTER trace, exactly as `prove_epoch` does. fn craft_bundle( elf_bytes: &[u8], logs: &[Log], + epoch_lens: &[usize], tamper: Tamper, ) -> Result { + assert_eq!(epoch_lens.iter().sum::(), logs.len()); let opts = opts(); let elf = Elf::load(elf_bytes).expect("ELF load"); let decode_commitment = crate::tables::decode::commitment_from_elf(&elf, &opts).expect("DECODE commitment"); let decode_artifacts = DecodeArtifacts::from_elf(&elf)?; - let image = build_initial_image_paged(&elf, &[]); + let mut image = build_initial_image_paged(&elf, &[]); let init_page_data = build_init_page_data(&image); let mut provenance = local_to_global::genesis_provenance(image.iter().map(|(a, v)| (a, v as u64))); - let register_init = register::register_init_from_entry_point(elf.entry_point); - let label = local_to_global::epoch_label(0); - let collected = Traces::collect_epoch(&decode_artifacts, &image, ®ister_init, logs, true)?; - let boundary = Arc::new(local_to_global::epoch_boundary( - &mut provenance, - label, - &collected.touched_memory_cells(), - )); - let mut traces = Traces::build_from_collected( - &decode_artifacts, - collected, - None::<&HashMap>, - ®ister_init, - &MaxRowsConfig::default(), - &[], - true, - true, - #[cfg(feature = "disk-spill")] - stark::storage_mode::StorageMode::Ram, - )?; - apply_tamper(&mut traces, logs, tamper); + let mut register_init = register::register_init_from_entry_point(elf.entry_point); + let mut epochs = Vec::with_capacity(epoch_lens.len()); + let mut boundaries = Vec::with_capacity(epoch_lens.len()); + let mut start = 0; + for (index, &len) in epoch_lens.iter().enumerate() { + let is_final = index == epoch_lens.len() - 1; + let epoch_logs = &logs[start..start + len]; + start += len; - let epoch = prove_epoch( - &elf, - elf_bytes, - &EpochStart { - register_init: ®ister_init, + let label = local_to_global::epoch_label(index as u64); + let collected = Traces::collect_epoch( + &decode_artifacts, + &image, + ®ister_init, + epoch_logs, + is_final, + )?; + let boundary = Arc::new(local_to_global::epoch_boundary( + &mut provenance, label, - }, - traces, - true, - &boundary, - &opts, - decode_commitment, - )?; + &collected.touched_memory_cells(), + )); + let next_register_init = collected.register_fini(®ister_init); + for cell in boundary.iter() { + image.set(cell.address, (cell.fini.value & 0xFF) as u8); + } + + let mut traces = Traces::build_from_collected( + &decode_artifacts, + collected, + None::<&HashMap>, + ®ister_init, + &MaxRowsConfig::default(), + &[], + is_final, + true, + #[cfg(feature = "disk-spill")] + stark::storage_mode::StorageMode::Ram, + )?; + if is_final { + apply_tamper(&mut traces, epoch_logs, tamper); + } + + epochs.push(prove_epoch( + &elf, + elf_bytes, + &EpochStart { + register_init: ®ister_init, + label, + }, + traces, + is_final, + &boundary, + &opts, + decode_commitment, + )?); + boundaries.push(boundary); + register_init = next_register_init; + } - let boundaries = vec![boundary]; let touched = touched_page_bases(&boundaries); let num_private_input_pages = page::private_input_page_count(&[]); let global = prove_global( @@ -89,7 +120,7 @@ fn craft_bundle( )?; Ok(ContinuationProof { - epochs: vec![epoch], + epochs, global, num_private_input_pages, touched_page_bases: touched, @@ -106,13 +137,37 @@ fn accepted(crafted: Result, elf: &[u8]) -> bool { } } +/// The forged bundle must build, so the rejection comes from the verifier and not +/// from the prover refusing the trace. +fn assert_verifier_rejects(crafted: Result, elf: &[u8], msg: &str) { + assert!(crafted.is_ok(), "the forged bundle must build"); + assert!(!accepted(crafted, elf), "{msg}"); +} + /// POSITIVE CONTROL: the hand-built one-epoch bundle of an honest run verifies. #[test] fn poc_control_patched_program_continuation_verifies() { let patched = patched_elf(&asm_elf_bytes(GUEST)); let logs = run_logs(&patched); assert!(accepted( - craft_bundle(&patched, &logs, Tamper::default()), + craft_bundle(&patched, &logs, &[logs.len()], Tamper::default()), + &patched + )); +} + +/// POSITIVE CONTROL: the two-epoch split the forgery below uses verifies for an +/// honest run. +#[test] +fn poc_control_patched_program_two_epochs_verifies() { + let patched = patched_elf(&asm_elf_bytes(GUEST)); + let logs = run_logs(&patched); + assert!(accepted( + craft_bundle( + &patched, + &logs, + &[PRE_EXIT_ROWS, logs.len() - PRE_EXIT_ROWS], + Tamper::default() + ), &patched )); } @@ -123,7 +178,7 @@ fn poc_control_honest_exit_one_continuation_is_rejected() { let elf = asm_elf_bytes(GUEST); let logs = run_logs(&elf); assert!(!accepted( - craft_bundle(&elf, &logs, Tamper::default()), + craft_bundle(&elf, &logs, &[logs.len()], Tamper::default()), &elf )); } @@ -134,10 +189,30 @@ fn poc_control_honest_exit_one_continuation_is_rejected() { #[test] fn continuation_continue_past_exit_is_rejected() { let elf = asm_elf_bytes(GUEST); - let logs = forged_logs(&elf); - assert!( - !accepted(craft_bundle(&elf, &logs, FULL_ATTACK), &elf), + let logs = forged_logs(&elf, FORGED_ROWS); + assert_verifier_rejects( + craft_bundle(&elf, &logs, &[FORGED_ROWS], FULL_ATTACK), + &elf, "SOUNDNESS BUG: the continuation verifier accepted a final epoch that runs \ - past the exit ecall and turns exit(1) into exit(0)" + past the exit ecall and turns exit(1) into exit(0)", + ); +} + +/// THE BUG in the final epoch of a two-epoch bundle: an honest first epoch, then +/// the exit ecall and the post-exit rows in the final one, whose INIT is the +/// first epoch's `reg_fini`. Must be rejected like the one-epoch case. +#[test] +fn continuation_continue_past_exit_in_final_of_two_epochs_is_rejected() { + let elf = asm_elf_bytes(GUEST); + let logs = forged_logs(&elf, PRE_EXIT_ROWS + FORGED_ROWS); + assert_eq!( + logs[PRE_EXIT_ROWS].src1_val, 93, + "the final epoch starts on the exit ecall" + ); + assert_verifier_rejects( + craft_bundle(&elf, &logs, &[PRE_EXIT_ROWS, FORGED_ROWS], FULL_ATTACK), + &elf, + "SOUNDNESS BUG: the continuation verifier accepted a final epoch (after an \ + honest one) that runs past the exit ecall", ); } diff --git a/prover/src/tests/halt_pc_forgery_poc.rs b/prover/src/tests/halt_pc_forgery_poc.rs index 1c0fc9a25..4e2caf984 100644 --- a/prover/src/tests/halt_pc_forgery_poc.rs +++ b/prover/src/tests/halt_pc_forgery_poc.rs @@ -36,7 +36,7 @@ const NOP: [u8; 4] = [0x13, 0x00, 0x00, 0x00]; /// Rows the forged trace has: a power of two, so the CPU table gets no padding /// rows and the last real row's `next_pc` goes straight to the REGISTER table. -const FORGED_ROWS: usize = 16; +pub(crate) const FORGED_ROWS: usize = 16; pub(crate) fn opts() -> ProofOptions { crate::GoldilocksCubicProofOptions::with_blowup(2).expect("blowup=2 is valid") @@ -64,8 +64,8 @@ pub(crate) fn run_logs(elf_bytes: &[u8]) -> Vec { } /// The honest logs up to and including `exit(1)`, followed by the post-exit rows -/// taken from the patched run, cut at `FORGED_ROWS` (before the second ecall). -pub(crate) fn forged_logs(honest: &[u8]) -> Vec { +/// taken from the patched run, cut at `rows` (before the second exit sequence). +pub(crate) fn forged_logs(honest: &[u8], rows: usize) -> Vec { let honest_logs = run_logs(honest); let exit_row = honest_logs.len() - 1; assert_eq!( @@ -75,8 +75,12 @@ pub(crate) fn forged_logs(honest: &[u8]) -> Vec { let patched_logs = run_logs(&patched_elf(honest)); let mut logs = honest_logs; - logs.extend_from_slice(&patched_logs[exit_row + 1..FORGED_ROWS]); - assert_eq!(logs.len(), FORGED_ROWS); + logs.extend_from_slice(&patched_logs[exit_row + 1..rows]); + assert_eq!(logs.len(), rows); + assert!( + logs[exit_row + 1..].iter().all(|log| log.src1_val != 93), + "no post-exit row is the second exit" + ); assert_eq!( logs[exit_row + 1].current_pc, logs[exit_row].current_pc + 4, @@ -94,7 +98,8 @@ pub(crate) struct Tamper { /// timestamp. Main-trace columns. pub(crate) register_ts: bool, /// Set the REGISTER final x255 value to the last post-exit `next_pc`. A - /// main-trace column on `main`; preprocessed (pinned to `pc = 1`) by the fix. + /// main-trace column on `main`; preprocessed by the fix, so the forged root no + /// longer matches the halted one the verifier recomputes. pub(crate) register_fini: bool, } @@ -163,11 +168,12 @@ fn craft_proof( None, true, None, - // As the production prover: FINI pinned to the halted register file. - crate::test_utils::halted_register_commitment( + // A malicious prover commits to its own (tampered) REGISTER trace. For an + // untampered FINI this is the halted root the production prover uses. + crate::test_utils::trace_register_commitment( &options, - &program, - &traces.public_output_bytes, + &crate::tables::register::register_init_from_entry_point(program.entry_point), + &traces, ), ); let runtime_page_ranges = traces.runtime_page_ranges(); @@ -214,6 +220,17 @@ fn accepted(crafted: Result, elf: &[u8]) - } } +/// The forged proof must build, so the rejection comes from the verifier and not +/// from the prover refusing the trace. +fn assert_verifier_rejects( + crafted: Result, + elf: &[u8], + msg: &str, +) { + assert!(crafted.is_ok(), "the forged proof must build"); + assert!(!accepted(crafted, elf), "{msg}"); +} + /// POSITIVE CONTROL: the harness itself produces valid proofs. The patched ELF /// (no first ecall) exits 0 honestly at its second ecall. #[test] @@ -236,57 +253,61 @@ fn poc_control_honest_exit_one_is_rejected() { /// NEGATIVE CONTROL: running past the exit while HALT's PC stays honest is /// rejected — HALT consumes the real `next_pc` token, so the first post-exit -/// row has nothing to read. Isolates HALT's free PC column as the hole. +/// row has nothing to read. FINI is left at the halted `pc = 1`, so this +/// isolates HALT's free PC column as the hole. #[test] fn poc_control_continue_without_halt_pc_tamper_is_rejected() { let elf = asm_elf_bytes(GUEST); - let logs = forged_logs(&elf); - assert!(!accepted( + let logs = forged_logs(&elf, FORGED_ROWS); + assert_verifier_rejects( craft_proof( &elf, &logs, Tamper { halt_pc: false, + register_fini: false, ..FULL_ATTACK - } + }, ), - &elf - )); + &elf, + "running past the exit without the HALT PC tamper must not verify", + ); } -/// THE BUG: set HALT `PC = (1, 0)`, keep executing after `exit(1)`, zero x10, -/// stop. Must be rejected; if this test fails the verifier accepted a proof -/// that `exit(1)` exited with code 0. +/// THE BUG, as it verified on `main`: set HALT `PC = (1, 0)`, keep executing +/// after `exit(1)`, zero x10, and end the PC chain on the last post-exit +/// `next_pc` (REGISTER FINI and its timestamp). The prover commits to that FINI; +/// the verifier must reject it because it pins FINI to the halted `pc = 1`. #[test] fn continue_past_exit_via_halt_pc_is_rejected() { let elf = asm_elf_bytes(GUEST); - let logs = forged_logs(&elf); - assert!( - !accepted(craft_proof(&elf, &logs, FULL_ATTACK), &elf), + let logs = forged_logs(&elf, FORGED_ROWS); + assert_verifier_rejects( + craft_proof(&elf, &logs, FULL_ATTACK), + &elf, "SOUNDNESS BUG: the verifier accepted a trace that runs past the exit ecall \ - (HALT PC = (1, 0)) and turns exit(1) into exit(0)" + (HALT PC = (1, 0)) and turns exit(1) into exit(0)", ); } -/// THE BUG, respecting the fix's pinned FINI: HALT `PC = (1, 0)` and the final -/// x255 token moved to the end of the post-exit rows, but its value left at -/// `pc = 1`. Touches main-trace columns only, so the prover must build the -/// proof; the verifier must reject it because no real row writes `next_pc = 1`. +/// THE BUG, with FINI left at the halted `pc = 1`: HALT `PC = (1, 0)` and the +/// final x255 token moved to the end of the post-exit rows. The REGISTER root +/// matches, so the verifier must reject it on the bus: no real row writes +/// `next_pc = 1`. #[test] fn continue_past_exit_with_pinned_fini_is_rejected() { let elf = asm_elf_bytes(GUEST); - let logs = forged_logs(&elf); - let crafted = craft_proof( + let logs = forged_logs(&elf, FORGED_ROWS); + assert_verifier_rejects( + craft_proof( + &elf, + &logs, + Tamper { + register_fini: false, + ..FULL_ATTACK + }, + ), &elf, - &logs, - Tamper { - register_fini: false, - ..FULL_ATTACK - }, - ); - assert!(crafted.is_ok(), "main-trace-only tamper must still prove"); - assert!( - !accepted(crafted, &elf), - "SOUNDNESS BUG: the PC chain ran past the exit ecall and still ended on pc = 1" + "SOUNDNESS BUG: the PC chain ran past the exit ecall and still ended on pc = 1", ); } diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index 9c2e5c3d1..f2a2c5476 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -112,7 +112,7 @@ pub(crate) fn weigh_the_bus( let table_counts = traces.table_counts(); let register_init = crate::tables::register::register_init_from_entry_point(elf.entry_point); let register_commitment = - crate::test_utils::epoch_register_commitment(&proof_options, ®ister_init, traces); + crate::test_utils::trace_register_commitment(&proof_options, ®ister_init, traces); let airs = VmAirs::new( elf, &proof_options, @@ -3463,7 +3463,7 @@ fn test_prove_first_epoch_without_halt() { None, false, None, - crate::test_utils::epoch_register_commitment(&proof_options, ®ister_init, &traces), + crate::test_utils::trace_register_commitment(&proof_options, ®ister_init, &traces), ); let multi_proof = multi_prove_ram( @@ -3551,7 +3551,7 @@ fn test_prove_second_epoch_from_snapshot() { None, false, None, - crate::test_utils::epoch_register_commitment(&proof_options, ®ister_init, &traces), + crate::test_utils::trace_register_commitment(&proof_options, ®ister_init, &traces), ); let multi_proof = multi_prove_ram( @@ -3646,7 +3646,7 @@ fn test_epoch_proof_commits_l2g() { None, false, None, - crate::test_utils::epoch_register_commitment(&proof_options, ®ister_init, &traces), + crate::test_utils::trace_register_commitment(&proof_options, ®ister_init, &traces), ); // Inert L2G AIR: commits the trace columns, but no bus and no constraints. @@ -3803,7 +3803,7 @@ fn test_continuation_pipeline_end_to_end() { None, is_final, None, - crate::test_utils::epoch_register_commitment( + crate::test_utils::trace_register_commitment( &proof_options, ®ister_inits[i], &traces, @@ -3943,7 +3943,7 @@ fn test_epoch_memory_bus_with_l2g_bookend() { None, false, None, - crate::test_utils::epoch_register_commitment(&proof_options, ®ister_init, &traces), + crate::test_utils::trace_register_commitment(&proof_options, ®ister_init, &traces), ); // L2G air on the epoch-local Memory bus (the bookend that replaces PAGE). From c5386f88d32142039ae0a4cbf3dc4a13bf0f94ae Mon Sep 17 00:00:00 2001 From: Nicole Date: Thu, 15 Oct 2026 11:36:05 -0300 Subject: [PATCH 5/8] drop redundant suffix, note that no real row may write next_pc = 1 --- docs/continuations_design.md | 4 ++-- prover/src/constraints/cpu.rs | 4 +++- prover/src/continuation.rs | 2 +- prover/src/lib.rs | 8 ++++---- prover/src/tables/branch.rs | 4 ++++ prover/src/tables/register.rs | 6 +++--- prover/src/tables/trace_builder.rs | 2 +- prover/src/test_utils.rs | 2 +- prover/src/tests/register_tests.rs | 8 ++++---- 9 files changed, 23 insertions(+), 17 deletions(-) diff --git a/docs/continuations_design.md b/docs/continuations_design.md index d571bc255..687a19607 100644 --- a/docs/continuations_design.md +++ b/docs/continuations_design.md @@ -643,8 +643,8 @@ recursion/aggregation layer (deferred). - `prover/src/tables/global_memory.rs` — the genesis (ELF-bound for ELF/runtime pages, committed/private for private-input pages, §3.6) and finalization anchors. - `prover/src/tables/register.rs` — the REGISTER table: REG-C1/REG-C2 Memory-bus - tokens, the preprocessed FINI commitment (`compute_precomputed_commitment_with_fini`, - `NUM_PREPROCESSED_COLS_WITH_FINI`), `fini_from_trace`, and the halted register + tokens, the preprocessed FINI commitment (`compute_precomputed_commitment`, + `NUM_PREPROCESSED_COLS`), `fini_from_trace`, and the halted register file that monolithic proofs and the final epoch pin FINI to (`halted_fini`, `halted_commitment`). - `prover/src/statement.rs` — the Fiat-Shamir statement absorbers diff --git a/prover/src/constraints/cpu.rs b/prover/src/constraints/cpu.rs index afb7fb07b..1b3030827 100644 --- a/prover/src/constraints/cpu.rs +++ b/prover/src/constraints/cpu.rs @@ -355,7 +355,9 @@ impl ConstraintSet for CpuConstraints { emit_branch_cond(b, idx); idx += 1; - // idx 33,34: next_pc = pc + instruction_length. + // idx 33,34: next_pc = pc + instruction_length. With pc even and an even + // length, next_pc stays even, so no real row writes `next_pc = 1` (the final + // PC pinned in `register::halted_fini`). emit_next_pc_add_pair(b, idx); idx += 2; diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index b3744963d..02581e569 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -670,7 +670,7 @@ fn build_epoch_airs( decode_commitment, is_final, None, - register::compute_precomputed_commitment_with_fini(opts, register_init, reg_fini), + register::compute_precomputed_commitment(opts, register_init, reg_fini), ) } diff --git a/prover/src/lib.rs b/prover/src/lib.rs index 0cd67930a..4ef6787dc 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -974,10 +974,10 @@ impl VmAirs { Box::new(create_hint_air(proof_options).with_name(&format!("HINT[{i}]"))) as VmAir }) .collect(); - let register: VmAir = Box::new(create_register_air(proof_options).with_preprocessed( - register_commitment, - register::NUM_PREPROCESSED_COLS_WITH_FINI, - )); + let register: VmAir = Box::new( + create_register_air(proof_options) + .with_preprocessed(register_commitment, register::NUM_PREPROCESSED_COLS), + ); // Every zero-init page shares one preprocessed commitment: OFFSET is // page-relative and INIT is all-zero, so it depends only on // (blowup, coset) — all fixed here. Compute it once (static const diff --git a/prover/src/tables/branch.rs b/prover/src/tables/branch.rs index 0d3c2e206..6b6d56924 100644 --- a/prover/src/tables/branch.rs +++ b/prover/src/tables/branch.rs @@ -97,6 +97,10 @@ pub mod cols { const SHIFT_8: u64 = 1 << 8; /// Mask value 254 = 0xFE (clears LSB) +/// +/// Soundness relies on this: a branch target is always even, so no BRANCH row can +/// write `next_pc = CPU_PADDING_PC` (1), the final PC the verifier pins in +/// `register::halted_fini`. const MASK_254: u64 = 254; // ========================================================================= diff --git a/prover/src/tables/register.rs b/prover/src/tables/register.rs index de9ee5064..c701c3db4 100644 --- a/prover/src/tables/register.rs +++ b/prover/src/tables/register.rs @@ -65,7 +65,7 @@ pub const NUM_REGISTER_ADDRESSES: usize = NUM_REGISTERS * WORDS_PER_REGISTER - 1 /// as its INIT, binding `init(epoch i+1) == fini(epoch i)` with no extra bus. A /// monolithic proof (and the final epoch) pins FINI to the halted state (see /// [`halted_fini`]). -pub const NUM_PREPROCESSED_COLS_WITH_FINI: usize = 3; +pub const NUM_PREPROCESSED_COLS: usize = 3; // ========================================================================= // Column indices for REGISTER table @@ -199,7 +199,7 @@ pub fn halted_commitment( committed_bytes: u32, ) -> Commitment { let init = register_init_from_entry_point(entry_point); - compute_precomputed_commitment_with_fini(options, &init, &halted_fini(committed_bytes)) + compute_precomputed_commitment(options, &init, &halted_fini(committed_bytes)) } /// Build the register init map from an epoch's boundary register snapshot: the @@ -335,7 +335,7 @@ pub fn fini_from_final_state(final_state: &FinalRegisterStateMap, init: &[u32]) /// produced by `fini_from_trace` (entry `i` = the register at /// `register_word_address_list()[i]`). Must match the column order of the REGISTER /// trace (OFFSET, INIT, FINI), and FINI on padding rows is 0 (as the trace builds it). -pub fn compute_precomputed_commitment_with_fini( +pub fn compute_precomputed_commitment( options: &ProofOptions, init: &[u32], fini: &[u32], diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 29c612513..c37ee5dee 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -4218,7 +4218,7 @@ impl Traces { use super::mul::cols::NUM_COLUMNS as MUL_COLS; use super::page::NUM_PREPROCESSED_COLS as PAGE_PREPROCESSED; use super::page::cols::NUM_COLUMNS as PAGE_COLS; - use super::register::NUM_PREPROCESSED_COLS_WITH_FINI as REGISTER_PREPROCESSED; + use super::register::NUM_PREPROCESSED_COLS as REGISTER_PREPROCESSED; use super::register::cols::NUM_COLUMNS as REGISTER_COLS; use super::shift::cols::NUM_COLUMNS as SHIFT_COLS; use super::store::cols::NUM_COLUMNS as STORE_COLS; diff --git a/prover/src/test_utils.rs b/prover/src/test_utils.rs index d2a569e6d..58895f94b 100644 --- a/prover/src/test_utils.rs +++ b/prover/src/test_utils.rs @@ -246,7 +246,7 @@ pub fn trace_register_commitment( traces: &crate::tables::trace_builder::Traces, ) -> stark::config::Commitment { let fini = crate::tables::register::fini_from_trace(&traces.register); - crate::tables::register::compute_precomputed_commitment_with_fini(options, init, &fini) + crate::tables::register::compute_precomputed_commitment(options, init, &fini) } // ============================================================================= diff --git a/prover/src/tests/register_tests.rs b/prover/src/tests/register_tests.rs index abe7daf2d..df4445a89 100644 --- a/prover/src/tests/register_tests.rs +++ b/prover/src/tests/register_tests.rs @@ -110,7 +110,7 @@ fn test_fini_from_trace_reads_every_register() { } #[test] -fn test_precomputed_commitment_with_fini_binds_fini() { +fn test_precomputed_commitment_binds_fini() { let opts = ProofOptions::default_test_options(); let init = register_init_from_entry_point(0x1000); // Fini vectors in register_word_address_list order (index = address for a < 64). @@ -120,9 +120,9 @@ fn test_precomputed_commitment_with_fini_binds_fini() { let mut fini_b = fini_a.clone(); fini_b[10] = 0x43; // a different final value at one address - let root_a = compute_precomputed_commitment_with_fini(&opts, &init, &fini_a); - let root_a2 = compute_precomputed_commitment_with_fini(&opts, &init, &fini_a); - let root_b = compute_precomputed_commitment_with_fini(&opts, &init, &fini_b); + let root_a = compute_precomputed_commitment(&opts, &init, &fini_a); + let root_a2 = compute_precomputed_commitment(&opts, &init, &fini_a); + let root_b = compute_precomputed_commitment(&opts, &init, &fini_b); // Deterministic, and sensitive to every fini value: a tampered R_{i+1} yields a // different preprocessed root, so a trace whose FINI != the committed R_{i+1} From e774e1507f1a5711d049af3b3806631bdc326410 Mon Sep 17 00:00:00 2001 From: Nicole Graus Date: Fri, 23 Oct 2026 16:56:24 -0300 Subject: [PATCH 6/8] Fix: Preprocess the CPU timestamp (#1025) * Preprocess the CPU timestamp as the spec defines it * Fix some low findings * Pin the PoC verifier to the halted register commitment --- bin/cli/src/main.rs | 12 + docs/continuations_design.md | 16 +- executor/programs/asm/poc_pc_double_read.s | 14 + prover/src/auto_storage.rs | 4 +- prover/src/bin/compute_static_commitments.rs | 28 +- prover/src/constraints/cpu.rs | 5 +- prover/src/continuation.rs | 142 +++++- prover/src/lib.rs | 106 ++++- prover/src/tables/cpu.rs | 344 +++++++++----- .../src/tables/cpu_timestamp_commitments.rs | 345 ++++++++++++++ prover/src/tables/halt.rs | 84 ++-- prover/src/tables/memw.rs | 3 +- prover/src/tables/register.rs | 87 +++- prover/src/tables/trace_builder.rs | 72 ++- prover/src/test_utils.rs | 72 ++- prover/src/tests/auto_storage_tests.rs | 2 +- .../tests/constraint_program_device_tests.rs | 4 +- prover/src/tests/constraint_program_tests.rs | 4 +- prover/src/tests/constraints_tests.rs | 4 +- prover/src/tests/cpu_tests.rs | 101 ++++- prover/src/tests/cpu_timestamp_tests.rs | 209 +++++++++ prover/src/tests/halt_pc_forgery_poc.rs | 11 +- prover/src/tests/ir_stats_dump.rs | 4 +- prover/src/tests/mod.rs | 4 + prover/src/tests/ood_window_ir_tests.rs | 4 +- prover/src/tests/page_offset_forgery_poc.rs | 2 + prover/src/tests/pc_double_read_poc.rs | 424 ++++++++++++++++++ prover/src/tests/prove_elfs_tests.rs | 22 + .../src/tests/recursion_soundness_gap_poc.rs | 1 + prover/src/tests/register_tests.rs | 51 ++- prover/src/tests/skip_empty_tables_tests.rs | 7 + prover/src/tests/static_commitments_tests.rs | 64 ++- prover/tests/gpu_constraint_interp_real.rs | 4 +- 33 files changed, 2027 insertions(+), 229 deletions(-) create mode 100644 executor/programs/asm/poc_pc_double_read.s create mode 100644 prover/src/tables/cpu_timestamp_commitments.rs create mode 100644 prover/src/tests/cpu_timestamp_tests.rs create mode 100644 prover/src/tests/pc_double_read_poc.rs diff --git a/bin/cli/src/main.rs b/bin/cli/src/main.rs index 656c05966..4c83b6c00 100644 --- a/bin/cli/src/main.rs +++ b/bin/cli/src/main.rs @@ -1001,6 +1001,12 @@ fn continuation_epoch_size(epoch_size_log2: u32) -> Result { "--epoch-size-log2 must be at least {MIN_CONTINUATION_EPOCH_SIZE_LOG2} for CLI proving" )); } + let max = prover::tables::cpu::MAX_EPOCH_SIZE_LOG2; + if epoch_size_log2 > max { + return Err(format!( + "--epoch-size-log2 must be at most {max} (an epoch has fewer than 2^30 CPU rows)" + )); + } 1usize.checked_shl(epoch_size_log2).ok_or_else(|| { format!("--epoch-size-log2 {epoch_size_log2} is too large for this platform") }) @@ -1146,6 +1152,12 @@ mod tests { assert!(continuation_epoch_size(17).is_err()); } + #[test] + fn continuation_epoch_size_rejects_epochs_over_the_cpu_row_bound() { + assert!(continuation_epoch_size(prover::tables::cpu::MAX_EPOCH_SIZE_LOG2).is_ok()); + assert!(continuation_epoch_size(prover::tables::cpu::MAX_EPOCH_SIZE_LOG2 + 1).is_err()); + } + #[test] fn continuation_epoch_size_uses_exact_power_of_two() { assert_eq!(continuation_epoch_size(20).unwrap(), 1 << 20); diff --git a/docs/continuations_design.md b/docs/continuations_design.md index 687a19607..79f5d0834 100644 --- a/docs/continuations_design.md +++ b/docs/continuations_design.md @@ -93,6 +93,15 @@ an epoch. The cross-epoch chain is ordered by the **epoch number** (§3.3), so t GlobalMemory bus carries no timestamp at all (see §2 telescoping). `fini_timestamp` stays only because the epoch-local **Memory bus** needs it (matched against MEMW). +The CPU timestamp is a **preprocessed** column (spec `Timestamp`): row `i` of every +CPU table holds `4·(i + 1)`. An epoch splits its CPU rows over several tables, so +table `k` adds `4·S_k` to every timestamp it sends, where `S_k` is the total +height of tables `0..k`. The verifier reads the heights off the epoch proof, so +every CPU timestamp, and the final PC timestamp `4·N + 1` (`N` = all CPU rows of +the epoch), is verifier-known. The verifier rejects an epoch with more than +`2^30 − 1` CPU rows: the last row's accesses reach `4·N + 2`, which must stay +below HALT's `2^32 − 1`. + ### Cross-epoch telescoping For a cell touched in epochs 1, 2, 3, the GlobalMemory bus checks: @@ -469,12 +478,17 @@ locks compose: Compose them: public `R_{i+1}` = trace FINI = real last write. So the value handed to the next epoch is pinned to real execution. -The **monolithic prover** preprocesses the same 3 columns, with FINI pinned to the +The **monolithic prover** preprocesses the same columns, with FINI pinned to the halted register file (`register::halted_fini`): x1-x31 = 0, x254 = the committed byte count, and the PC = 1. The final epoch's `R_{i+1}` must equal that same halted state. Pinning it ends the PC chain on `pc = 1`, so execution cannot continue past the exit ecall. +REGISTER also preprocesses `IS_PC` (1 on the two x255 rows). REG-C2 sends the x255 +final token at the verifier-known final PC timestamp `4·N + 1` instead of the +`timestamp` column (spec `halt.typ`), so both the value and the timestamp the PC +chain ends on are verifier-known. + ### Commit index (x254) The COMMIT chip's running output index lives in a synthetic single-word register diff --git a/executor/programs/asm/poc_pc_double_read.s b/executor/programs/asm/poc_pc_double_read.s new file mode 100644 index 000000000..5e58638b6 --- /dev/null +++ b/executor/programs/asm/poc_pc_double_read.s @@ -0,0 +1,14 @@ + .text + .attribute 5, "rv64i2p1" + .globl main +main: + # Exits with code 5. HALT enforces x10 == 0, so an honest prover cannot + # prove this program. + li a0, 5 + # The PoC proves this row with pc_double_read = 1 one timestamp after the + # previous row, so its read of a0 lands before the write above and returns + # the stale initial a0 = 0. + mv a1, a0 + mv a0, a1 + li a7, 93 # syscall = Halt + ecall diff --git a/prover/src/auto_storage.rs b/prover/src/auto_storage.rs index 8cc437edd..4cb719d45 100644 --- a/prover/src/auto_storage.rs +++ b/prover/src/auto_storage.rs @@ -120,7 +120,7 @@ fn table_specs(lengths: &TableLengths) -> Vec { ( lengths.cpu_padded_rows, CPU_COLS as u64, - aux_cols(cpu_buses().len()), + aux_cols(cpu_buses(0).len()), 1, ), ( @@ -203,7 +203,7 @@ fn table_specs(lengths: &TableLengths) -> Vec { ( register_rows, REGISTER_COLS as u64, - aux_cols(register_buses().len()), + aux_cols(register_buses(0).len()), 2, ), ]; diff --git a/prover/src/bin/compute_static_commitments.rs b/prover/src/bin/compute_static_commitments.rs index a4de1ddaa..e16628838 100644 --- a/prover/src/bin/compute_static_commitments.rs +++ b/prover/src/bin/compute_static_commitments.rs @@ -2,6 +2,8 @@ //! for a fixed set of `blowup_factor` values. The output is pasted into the //! `static_commitment` match bodies in `prover/src/tables/{bitwise,keccak_rc}.rs` //! and the `static_zero_page_commitment` match body in `prover/src/tables/page.rs`. +//! It then prints the CPU timestamp table, pasted over +//! `prover/src/tables/cpu_timestamp_commitments.rs`. //! The `static_commitments_tests` test suite pins the values so any drift in //! the AIR or FFT pipeline is caught at test time. //! @@ -13,7 +15,7 @@ //! `keccak_rc.rs` and `static_zero_page_commitment` in `page.rs` for when //! it's actually appropriate to bless new bytes. -use lambda_vm_prover::tables::{STATIC_BLOWUP_FACTORS, bitwise, keccak_rc, page}; +use lambda_vm_prover::tables::{STATIC_BLOWUP_FACTORS, bitwise, cpu, keccak_rc, max_rows, page}; use stark::config::Commitment; use stark::proof::options::GoldilocksCubicProofOptions; @@ -72,4 +74,28 @@ fn main() { private_page_fmt = format_commitment(&private_page), ); } + + // ---- CPU timestamp (one commitment per table height): + println!( + "// Generated by `cargo run --bin compute_static_commitments --release`.\n\ + // Do not edit by hand; see `static_timestamp_commitment`.\n\n\ + /// `(blowup_factor, [commitment for log2(height) = MIN_LOG_HEIGHT..])`.\n\ + const CPU_TIMESTAMP_COMMITMENTS: &[(u8, &[Commitment])] = &[" + ); + for &blowup in STATIC_BLOWUP_FACTORS { + let Ok(options) = GoldilocksCubicProofOptions::with_blowup(blowup) else { + continue; + }; + println!(" (\n {blowup},\n &["); + for log_height in cpu::MIN_LOG_HEIGHT..=max_rows::CPU.trailing_zeros() { + let commitment = cpu::compute_timestamp_commitment(&options, 1 << log_height); + println!(" // 2^{log_height}"); + println!( + " {},", + format_commitment(&commitment).replace("\n ", "\n ") + ); + } + println!(" ],\n ),"); + } + println!("];"); } diff --git a/prover/src/constraints/cpu.rs b/prover/src/constraints/cpu.rs index 1b3030827..5af6fdc3a 100644 --- a/prover/src/constraints/cpu.rs +++ b/prover/src/constraints/cpu.rs @@ -37,7 +37,6 @@ pub const BIT_FLAG_COLUMNS: &[usize] = &[ cols::BRANCH, cols::ECALL, cols::PC_DOUBLE_READ, - cols::PREV_PC_TIMESTAMP_BORROW, ]; // ========================================================================= @@ -45,7 +44,7 @@ pub const BIT_FLAG_COLUMNS: &[usize] = &[ // ========================================================================= /// Total number of CPU transition constraints (excludes bus lookups): -/// - IS_BIT: 12 +/// - IS_BIT: 11 /// - decode mutex: 6 (`word_instr · {MEMORY, BRANCH, ECALL, WRITE_REGISTER, /// READ_REGISTER1, READ_REGISTER2}`) /// - ADD pair: 2, SUB pair: 2 @@ -56,7 +55,7 @@ pub const BIT_FLAG_COLUMNS: &[usize] = &[ /// - branch_cond: 1 /// - next_pc: 2 /// - assumptions: 4 (MEMORY·BRANCH mutex 1 + arg2 exclusivity 2 + mem_flags IS_BIT 1) -pub const NUM_CPU_CONSTRAINTS: usize = 12 + 6 + 2 + 2 + 2 + 4 + 2 + 2 + 1 + 2 + 4; +pub const NUM_CPU_CONSTRAINTS: usize = 11 + 6 + 2 + 2 + 2 + 4 + 2 + 2 + 1 + 2 + 4; // ========================================================================= // Single-body emit functions (ConstraintBuilder front-end) diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index 02581e569..f4eb639d4 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -652,6 +652,7 @@ fn build_epoch_airs( opts: &ProofOptions, page_configs: &[PageConfig], table_counts: &TableCounts, + cpu_heights: &[usize], register_init: &[u32], reg_fini: &[u32], is_final: bool, @@ -667,6 +668,7 @@ fn build_epoch_airs( false, page_configs, table_counts, + cpu_heights, decode_commitment, is_final, None, @@ -709,6 +711,8 @@ fn prove_epoch( let reg_fini = register::fini_from_trace(&traces.register); let table_counts = traces.table_counts(); + let cpu_heights = crate::cpu_heights_from_traces(&traces); + crate::tables::cpu::validate_heights(&cpu_heights)?; let public_output = traces.public_output_bytes.clone(); let runtime_page_ranges = traces.runtime_page_ranges(); @@ -717,6 +721,7 @@ fn prove_epoch( opts, &[], &table_counts, + &cpu_heights, start.register_init, ®_fini, is_final, @@ -824,6 +829,15 @@ fn verify_epoch( return Ok(false); } + // Every CPU timestamp of the epoch, and the final PC timestamp, follow from + // the CPU heights; reject an epoch over the per-epoch row bound. + let Some(cpu_heights) = crate::cpu_heights_from_proofs(proof, &table_counts, is_final) else { + return Ok(false); + }; + if crate::tables::cpu::validate_heights(&cpu_heights).is_err() { + return Ok(false); + } + let reg_fini = epoch.reg_fini()?; let runtime_page_ranges = epoch.runtime_page_ranges()?; let public_output = epoch.public_output(); @@ -833,6 +847,7 @@ fn verify_epoch( opts, &[], &table_counts, + &cpu_heights, register_init, ®_fini, is_final, @@ -1069,12 +1084,38 @@ pub fn prove_continuation( private_inputs: &[u8], epoch_size_log2: u32, opts: &ProofOptions, +) -> Result { + prove_continuation_with_max_rows( + elf_bytes, + private_inputs, + epoch_size_log2, + opts, + &MaxRowsConfig::default(), + ) +} + +/// [`prove_continuation`] with explicit per-table row limits, so an epoch can be +/// split over several CPU tables (tests use [`MaxRowsConfig::small`]). +pub(crate) fn prove_continuation_with_max_rows( + elf_bytes: &[u8], + private_inputs: &[u8], + epoch_size_log2: u32, + opts: &ProofOptions, + max_rows: &MaxRowsConfig, ) -> Result { if epoch_size_log2 < 2 { return Err(Error::InvalidContinuationEpochSize( "epoch_size_log2 must be at least 2 (4 cycles)".to_string(), )); } + // An epoch over the per-epoch CPU row bound fails here, not after its run. + if epoch_size_log2 > crate::tables::cpu::MAX_EPOCH_SIZE_LOG2 { + return Err(Error::InvalidContinuationEpochSize(format!( + "epoch_size_log2 {epoch_size_log2} exceeds the maximum {}", + crate::tables::cpu::MAX_EPOCH_SIZE_LOG2 + ))); + } + crate::tables::cpu::validate_max_rows(max_rows.cpu)?; let epoch_size = 1usize.checked_shl(epoch_size_log2).ok_or_else(|| { Error::InvalidContinuationEpochSize(format!( "epoch_size_log2 {epoch_size_log2} is too large for this platform" @@ -1243,7 +1284,7 @@ pub fn prove_continuation( // only image consumers in the build) are skipped. None::<&std::collections::HashMap>, &job.register_init, - &MaxRowsConfig::default(), + max_rows, private_inputs, job.is_final, true, @@ -2338,6 +2379,105 @@ mod tests { )); } + /// `2^30` cycles would put the epoch's last CPU row at timestamp `2^32`; + /// refused before the (empty) ELF is even loaded. + #[test] + fn test_continuation_rejects_epoch_over_cpu_row_bound() { + let max = crate::tables::cpu::MAX_EPOCH_SIZE_LOG2; + assert!((1u64 << max) <= crate::tables::cpu::MAX_CPU_ROWS); + assert!(matches!( + prove_continuation(&[], &[], max + 1, &ProofOptions::default_test_options()), + Err(Error::InvalidContinuationEpochSize(_)) + )); + } + + /// A CPU chunk size the verifier would refuse fails before execution. + #[test] + fn test_continuation_rejects_invalid_cpu_max_rows() { + for cpu in [0, 6, crate::tables::max_rows::CPU * 2] { + let max_rows = MaxRowsConfig { + cpu, + ..MaxRowsConfig::small() + }; + assert!(matches!( + prove_continuation_with_max_rows( + &[], + &[], + 4, + &ProofOptions::default_test_options(), + &max_rows + ), + Err(Error::InvalidTableCounts(_)) + )); + } + } + + /// Epochs split over several CPU tables: every table after the first sends + /// its timestamps from a non-zero base, the intermediate epochs (no HALT) read + /// their CPU heights from a shifted sub-proof index, and REGISTER consumes x255 + /// at `4·N + 1` over all of the epoch's tables. + #[test] + fn test_continuation_with_several_cpu_tables_per_epoch_verifies() { + let _ = env_logger::builder().is_test(true).try_init(); + let elf_bytes = asm_elf_bytes("all_instructions_64"); + let max_rows = MaxRowsConfig::small(); + let epoch_size_log2 = max_rows.cpu.trailing_zeros() + 1; + let opts = ProofOptions::default_test_options(); + let bundle = + prove_continuation_with_max_rows(&elf_bytes, &[], epoch_size_log2, &opts, &max_rows) + .unwrap(); + assert!( + bundle.epochs.len() >= 2, + "need an intermediate epoch, got {} epochs", + bundle.epochs.len() + ); + for epoch in &bundle.epochs[..bundle.epochs.len() - 1] { + assert!( + epoch.table_counts.cpu >= 2, + "every intermediate epoch spans several CPU tables" + ); + } + assert!( + verify_continuation(&elf_bytes, &bundle, &opts) + .unwrap() + .is_some() + ); + } + + /// Hostile CPU heights in an intermediate epoch (no HALT, so its CPU + /// sub-proofs start one index earlier): heights `validate_heights` refuses + /// and a valid but wrong height are both rejected, without panicking. + #[test] + fn test_continuation_rejects_hostile_epoch_cpu_heights() { + let elf_bytes = asm_elf_bytes("all_instructions_64"); + let max_rows = MaxRowsConfig::small(); + let epoch_size_log2 = max_rows.cpu.trailing_zeros() + 1; + let opts = ProofOptions::default_test_options(); + let mut bundle = + prove_continuation_with_max_rows(&elf_bytes, &[], epoch_size_log2, &opts, &max_rows) + .unwrap(); + // Epoch 0 must be intermediate (no HALT) for `cpu_proof_start(false, ..)`. + assert!(bundle.epochs.len() >= 2, "need an intermediate epoch"); + let cpu = crate::cpu_proof_start(false, &bundle.epochs[0].table_counts); + assert_eq!( + bundle.epochs[0].proof.proofs[cpu].trace_length, + max_rows.cpu + ); + for height in [6, 2 * crate::tables::max_rows::CPU, 2 * max_rows.cpu] { + bundle.epochs[0].proof.proofs[cpu].trace_length = height; + assert!( + !matches!(verify_continuation(&elf_bytes, &bundle, &opts), Ok(Some(_))), + "height {height}" + ); + } + bundle.epochs[0].proof.proofs[cpu].trace_length = max_rows.cpu; + assert!( + verify_continuation(&elf_bytes, &bundle, &opts) + .unwrap() + .is_some() + ); + } + // ---- Standalone (split) prover/verifier ---- // Round-trip: a bundle from prove_continuation verifies on its own (only the diff --git a/prover/src/lib.rs b/prover/src/lib.rs index 4ef6787dc..c005c0116 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -572,6 +572,45 @@ type AirTracePair<'a> = ( &'a (), ); +/// Sub-proof index of the first CPU table: [`VmAirs::air_refs`] puts the four +/// fixed tables, HALT (when included) and the accelerator tables first. +fn cpu_start(include_halt: bool, accelerator_counts: [usize; 6]) -> usize { + 4 + usize::from(include_halt) + accelerator_counts.iter().sum::() +} + +/// [`cpu_start`] for a proof's declared `table_counts`. +pub(crate) fn cpu_proof_start(include_halt: bool, table_counts: &TableCounts) -> usize { + cpu_start( + include_halt, + [ + table_counts.commit, + table_counts.keccak, + table_counts.keccak_rnd, + table_counts.ecsm, + table_counts.ecdas, + table_counts.hint, + ], + ) +} + +/// The CPU tables' heights as a proof declares them (the sub-proofs' trace +/// lengths), for [`VmAirs::new`]. `None` if the proof has fewer sub-proofs than +/// `table_counts` places CPU tables at. +pub(crate) fn cpu_heights_from_proofs( + proofs: MultiProofView<'_, F, E, ()>, + table_counts: &TableCounts, + include_halt: bool, +) -> Option> { + let start = cpu_proof_start(include_halt, table_counts); + let end = start.checked_add(table_counts.cpu)?; + (end <= proofs.len()).then(|| (start..end).map(|i| proofs.get(i).trace_length()).collect()) +} + +/// The CPU tables' heights of a built trace set, for [`VmAirs::new`]. +pub(crate) fn cpu_heights_from_traces(traces: &Traces) -> Vec { + traces.cpus.iter().map(|t| t.num_rows()).collect() +} + /// All VM AIR instances, grouped by table. pub(crate) struct VmAirs { pub cpus: Vec, @@ -777,6 +816,21 @@ impl VmAirs { refs.push(air.as_ref()); } + debug_assert_eq!( + refs.len(), + cpu_start( + self.include_halt, + [ + self.commits.len(), + self.keccaks.len(), + self.keccak_rnds.len(), + self.ecsms.len(), + self.ecdases.len(), + self.hints.len(), + ], + ), + "cpu_proof_start must match the air_refs layout" + ); for air in &self.cpus { refs.push(air.as_ref()); } @@ -842,8 +896,15 @@ impl VmAirs { /// callers must bind identity externally (see `recursion::check_attestation`). /// /// `register_commitment` is the REGISTER preprocessed root (OFFSET, INIT, - /// FINI): [`register::halted_commitment`] for a monolithic proof, or the + /// FINI, IS_PC): [`register::halted_commitment`] for a monolithic proof, or the /// epoch's `R_i`/`R_{i+1}` for a continuation epoch. + /// + /// `cpu_heights` are the CPU tables' heights, in order (`table_counts.cpu` of + /// them; the trace heights on the prove side, the sub-proofs' trace lengths on + /// the verify side, see [`cpu_heights_from_proofs`]). They fix each CPU + /// table's preprocessed TIMESTAMP commitment and timestamp base, and the final + /// PC timestamp REGISTER consumes x255 at. Callers check them with + /// [`tables::cpu::validate_heights`] first. #[allow(clippy::too_many_arguments)] pub fn new( elf: &Elf, @@ -851,16 +912,34 @@ impl VmAirs { minimal_bitwise: bool, page_configs: &[crate::tables::page::PageConfig], table_counts: &TableCounts, + cpu_heights: &[usize], decode_commitment: Option, include_halt: bool, page_commitments: Option<&[(u64, Commitment)]>, register_commitment: Commitment, ) -> Self { - let cpus: Vec<_> = (0..table_counts.cpu) - .map(|i| { - Box::new(create_cpu_air(proof_options).with_name(&format!("CPU[{}]", i))) as VmAir + assert_eq!( + cpu_heights.len(), + table_counts.cpu, + "one height per CPU table" + ); + let cpus: Vec<_> = cpu_heights + .iter() + .zip(tables::cpu::timestamp_bases(cpu_heights)) + .enumerate() + .map(|(i, (&height, ts_base))| { + Box::new( + create_cpu_air(proof_options, ts_base) + .with_name(&format!("CPU[{}]", i)) + .with_preprocessed( + tables::cpu::timestamp_commitment(proof_options, height), + tables::cpu::NUM_PRECOMPUTED_COLS, + ), + ) as VmAir }) .collect(); + let total_cpu_rows: u64 = cpu_heights.iter().map(|&h| h as u64).sum(); + let final_pc_ts = tables::cpu::final_pc_timestamp(total_cpu_rows); let bitwise: VmAir = if minimal_bitwise { // TEST-ONLY BRANCH — must never be reached in production. // @@ -975,7 +1054,7 @@ impl VmAirs { }) .collect(); let register: VmAir = Box::new( - create_register_air(proof_options) + create_register_air(proof_options, final_pc_ts) .with_preprocessed(register_commitment, register::NUM_PREPROCESSED_COLS), ); // Every zero-init page shares one preprocessed commitment: OFFSET is @@ -1279,6 +1358,9 @@ pub fn prove_with_options_and_inputs( #[cfg(feature = "instruments")] let heap_before = stark::instruments::heap_bytes(); + // A CPU chunk size the verifier would refuse fails here, not after the run. + tables::cpu::validate_max_rows(max_rows.cpu)?; + // Phase 1: Execute (ELF load + run) #[cfg(feature = "instruments")] let phase_start = std::time::Instant::now(); @@ -1291,6 +1373,8 @@ pub fn prove_with_options_and_inputs( let result = executor .run() .map_err(|e| Error::Execution(format!("{e}")))?; + // A run over the per-proof CPU row bound fails here, before the trace build. + tables::cpu::validate_heights(&tables::cpu::table_heights(result.logs.len(), max_rows.cpu))?; #[cfg(feature = "instruments")] drop(__sp); @@ -1339,6 +1423,8 @@ pub fn prove_with_options_and_inputs( let __sp = stark::instruments::span("air_construction"); let table_counts = traces.table_counts(); + let cpu_heights = cpu_heights_from_traces(&traces); + tables::cpu::validate_heights(&cpu_heights)?; let committed_bytes = u32::try_from(traces.public_output_bytes.len()) .expect("trace build bounds the commit index to u32"); let airs = VmAirs::new( @@ -1347,6 +1433,7 @@ pub fn prove_with_options_and_inputs( false, &traces.page_configs, &table_counts, + &cpu_heights, None, true, None, @@ -1586,12 +1673,21 @@ fn verify_proof_parts( let Ok(committed_bytes) = u32::try_from(public_output.len()) else { return Ok(false); }; + // The CPU heights fix every CPU timestamp (preprocessed TIMESTAMP plus a + // per-table base) and the final PC timestamp, so they must respect the + // per-epoch row bound before they size anything. + let cpu_heights = cpu_heights_from_proofs(proofs, table_counts, true).ok_or_else(|| { + Error::InvalidTableCounts("proof has fewer sub-proofs than CPU tables".to_string()) + })?; + tables::cpu::validate_heights(&cpu_heights)?; + let airs = VmAirs::new( program, proof_options, false, &page_configs, table_counts, + &cpu_heights, decode_commitment, true, page_commitments, diff --git a/prover/src/tables/cpu.rs b/prover/src/tables/cpu.rs index fc4c2f976..ebde9e8e2 100644 --- a/prover/src/tables/cpu.rs +++ b/prover/src/tables/cpu.rs @@ -1,7 +1,7 @@ //! CPU table for the 64-bit VM. //! //! The CPU table is the central execution table. Following `spec/src/cpu.toml` -//! it is narrow (~39 columns): there are no per-opcode one-hot ALU selectors and +//! it is narrow (37 columns): there are no per-opcode one-hot ALU selectors and //! no `*_ext_bit`/`arg1` columns. Instead each row carries: //! - top-level flags `ALU/ADD/SUB/MEMORY/BRANCH/ECALL` (+ `word_instr`), //! - the packed `alu_flags`/`mem_flags` bytes (the chips unpack them), and @@ -24,14 +24,19 @@ //! JALR bit (the memory-width bits are 0), so `mem_flags ∈ {0,1} = JALR` and the //! `mem_flags` column is used directly as `JALR` wherever it is gated by `BRANCH`. -use super::types::{BusId, DecodeEntry, GoldilocksExtension, GoldilocksField, VmTable, alu_op}; +use super::types::{BusId, DecodeEntry, FE, GoldilocksExtension, GoldilocksField, VmTable, alu_op}; use crate::Error; use executor::vm::{ instruction::{decoding::Instruction, execution::SyscallNumbers}, logs::Log, memory::U64HashMap, }; +use math::polynomial::Polynomial; +use stark::commitment::{ROWS_PER_LEAF, commit_bit_reversed}; +use stark::config::Commitment; use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; +use stark::proof::options::ProofOptions; +use stark::prover::evaluate_polynomial_on_lde_domain; use stark::trace::TraceTable; /// PC value used for CPU padding rows. Per spec this is an odd address @@ -39,6 +44,168 @@ use stark::trace::TraceTable; /// padding entry at this PC (all flags 0, `half_instruction_length = 0`). pub const CPU_PADDING_PC: u64 = 1; +/// Number of preprocessed columns: `TIMESTAMP` (column 0). +/// +/// Row `i` of every CPU table holds `4·(i + 1)`, as spec `config.toml` defines +/// the `Timestamp` type. An epoch (or a monolithic proof) splits its CPU rows +/// over several tables, so table `k` adds the constant `4·S_k` to every +/// timestamp it sends, where `S_k` is the total height of tables `0..k` (see +/// [`timestamp_bases`]). The verifier reads the heights off the proof, so every +/// CPU timestamp is verifier-known. +pub const NUM_PRECOMPUTED_COLS: usize = 1; + +/// Timestamp slots per CPU row (spec `memory.typ`, granularity aside). +pub const TIMESTAMP_STRIDE: u64 = 4; + +/// Maximum number of CPU rows (padding included) in an epoch or a monolithic +/// proof. The last row's accesses reach `4·N + 2`, which must stay below the +/// HALT timestamp `2^32 - 1` (spec `streaming.typ`: an epoch should not exceed +/// `2^30` cycles; `N = 2^30` would put the last timestamp at `2^32`). +pub const MAX_CPU_ROWS: u64 = (1 << 30) - 1; + +/// Largest continuation epoch, `log2` of its cycle count: `2^29` is the largest +/// power of two within [`MAX_CPU_ROWS`]. +pub const MAX_EPOCH_SIZE_LOG2: u32 = 29; + +/// Timestamp the final PC token is written at: the last CPU row (`4·N`) emits +/// `next_pc` at `4·N + 1`. Spec `halt.typ`: the verifier knows it. +pub fn final_pc_timestamp(total_rows: u64) -> u64 { + TIMESTAMP_STRIDE * total_rows + 1 +} + +/// The constant each CPU table adds to its preprocessed timestamps: +/// `4·(h_0 + … + h_{k-1})` for table `k`. +pub fn timestamp_bases(heights: &[usize]) -> Vec { + heights + .iter() + .scan(0u64, |rows, &h| { + let base = TIMESTAMP_STRIDE * *rows; + *rows += h as u64; + Some(base) + }) + .collect() +} + +/// Checks the CPU table heights of an epoch or monolithic proof: each a power +/// of two in `[4, max_rows::CPU]` (the range the static timestamp commitments +/// cover) and at most [`MAX_CPU_ROWS`] in total. +pub fn validate_heights(heights: &[usize]) -> Result<(), Error> { + let mut total: u64 = 0; + for &h in heights { + if !h.is_power_of_two() || !(4..=super::max_rows::CPU).contains(&h) { + return Err(Error::InvalidTableCounts(format!( + "CPU table height must be a power of two in [4, {}], got {h}", + super::max_rows::CPU + ))); + } + total += h as u64; + } + if total > MAX_CPU_ROWS { + return Err(Error::InvalidTableCounts(format!( + "{total} CPU rows exceed the per-epoch maximum {MAX_CPU_ROWS}" + ))); + } + Ok(()) +} + +/// The CPU table heights the trace builder produces for `rows` executed cycles +/// split into chunks of `max_rows_cpu`: full chunks, then the last one padded to +/// a power of two (at least 4). Lets the prover check [`validate_heights`] right +/// after execution, before building any trace. +pub fn table_heights(rows: usize, max_rows_cpu: usize) -> Vec { + (0..rows) + .step_by(max_rows_cpu.max(1)) + .map(|start| (rows - start).min(max_rows_cpu).next_power_of_two().max(4)) + .collect() +} + +/// Checks a prover's CPU chunk size before execution: every CPU table but the +/// last has exactly `max_rows_cpu` rows, so it must be a height +/// [`validate_heights`] accepts. Fails before the run instead of after the +/// trace build. +pub fn validate_max_rows(max_rows_cpu: usize) -> Result<(), Error> { + validate_heights(&[max_rows_cpu]) +} + +/// The preprocessed `TIMESTAMP` commitment of a CPU table of `height` rows. +/// Static for the standard options (see [`static_timestamp_commitment`]), +/// recomputed otherwise. +pub fn timestamp_commitment(options: &ProofOptions, height: usize) -> Commitment { + debug_assert!( + height.is_power_of_two(), + "CPU table height {height} must be checked by validate_heights first" + ); + if options.coset_offset == 3 + && let Some(commitment) = + static_timestamp_commitment(options.blowup_factor, height.trailing_zeros()) + { + return commitment; + } + // Once per process: the verifier asks for one commitment per CPU table. + static WARNED: std::sync::Once = std::sync::Once::new(); + WARNED.call_once(|| { + log::warn!( + "CPU timestamp commitment not static for (blowup={}, coset={}); \ + falling back to recompute. Add it to `CPU_TIMESTAMP_COMMITMENTS` by running \ + `cargo run --bin compute_static_commitments --release`.", + options.blowup_factor, + options.coset_offset, + ); + }); + compute_timestamp_commitment(options, height) +} + +/// Recomputes the preprocessed `TIMESTAMP` commitment of a CPU table of `height` +/// rows: the column `4·(i + 1)`, low-degree extended and committed exactly as +/// the prover commits a table's precomputed columns. +pub fn compute_timestamp_commitment(options: &ProofOptions, height: usize) -> Commitment { + let column: Vec = (0..height as u64) + .map(|i| FE::from(TIMESTAMP_STRIDE * (i + 1))) + .collect(); + commit_timestamp_column(options, &column) +} + +/// Commits a CPU `TIMESTAMP` column as the prover commits a table's precomputed +/// columns. Soundness tests use it to commit a forged column. +pub(crate) fn commit_timestamp_column(options: &ProofOptions, column: &[FE]) -> Commitment { + let poly = Polynomial::interpolate_fft::(column) + .expect("FFT interpolation failed for CPU timestamp column"); + let lde = evaluate_polynomial_on_lde_domain( + &poly, + options.blowup_factor as usize, + column.len(), + &FE::from(options.coset_offset), + ) + .expect("LDE evaluation failed for CPU timestamp column"); + let (_, root) = commit_bit_reversed(&[lde], ROWS_PER_LEAF) + .expect("Failed to build Merkle tree for CPU timestamp LDE"); + root +} + +/// Static CPU timestamp commitments for `log2(height)` in +/// `2..=log2(max_rows::CPU)`, per standard blowup factor (coset offset 3). +/// +/// # Regenerating +/// +/// Only after a deliberate change to the timestamp column or the FFT / LDE / +/// Merkle pipeline: `cargo run --bin compute_static_commitments --release`, +/// then paste the printed table over [`CPU_TIMESTAMP_COMMITMENTS`]. A failing +/// drift test (`static_commitments_tests`) is a reason to ask why the bytes +/// changed, not to regenerate them. +pub fn static_timestamp_commitment(blowup_factor: u8, log_height: u32) -> Option { + let (_, by_height) = CPU_TIMESTAMP_COMMITMENTS + .iter() + .find(|(blowup, _)| *blowup == blowup_factor)?; + by_height + .get(log_height.checked_sub(MIN_LOG_HEIGHT)? as usize) + .copied() +} + +/// Smallest CPU table height is `2^2` (`generate_cpu_trace` pads to at least 4). +pub const MIN_LOG_HEIGHT: u32 = 2; + +include!("cpu_timestamp_commitments.rs"); + // ========================================================================= // Column indices for the CPU table // ========================================================================= @@ -49,7 +216,8 @@ pub mod cols { // Input columns (from DECODE) // ------------------------------------------------------------------------- - /// timestamp: Timestamp for memory argument coordination. + /// timestamp: Timestamp for memory argument coordination. Preprocessed: row + /// `i` holds `4·(i + 1)` (spec type `Timestamp`); see [`super::NUM_PRECOMPUTED_COLS`]. pub const TIMESTAMP: usize = 0; /// pc: program counter (DWordWL, 2 words). @@ -109,36 +277,33 @@ pub mod cols { // Auxiliary columns // ------------------------------------------------------------------------- - /// prev_pc_timestamp_borrow: borrow bit for the inline-PC `timestamp - 3` - /// subtraction (fires when `timestamp_lo < 3` and `pc_double_read = 0`). - pub const PREV_PC_TIMESTAMP_BORROW: usize = 25; /// pc_double_read: PC is read as a general register (`rs1 = 255`) this cycle /// (AUIPC/JAL) (Bit). - pub const PC_DOUBLE_READ: usize = 26; + pub const PC_DOUBLE_READ: usize = 25; /// rv1: value of register rs1 (DWordWL, 2 words). - pub const RV1_0: usize = 27; - pub const RV1_1: usize = 28; + pub const RV1_0: usize = 26; + pub const RV1_1: usize = 27; /// rv2: value of register rs2 (DWordWL, 2 words). - pub const RV2_0: usize = 29; - pub const RV2_1: usize = 30; + pub const RV2_0: usize = 28; + pub const RV2_1: usize = 29; /// arg2: multiplexed second ALU argument (DWordWL, 2 words). - pub const ARG2_0: usize = 31; - pub const ARG2_1: usize = 32; + pub const ARG2_0: usize = 30; + pub const ARG2_1: usize = 31; /// res: ALU result (DWordHL, 4 halves → 2 words via `cast`). - pub const RES_0: usize = 33; - pub const RES_1: usize = 34; - pub const RES_2: usize = 35; - pub const RES_3: usize = 36; + pub const RES_0: usize = 32; + pub const RES_1: usize = 33; + pub const RES_2: usize = 34; + pub const RES_3: usize = 35; /// branch_cond: whether the branch/jump is taken (Bit). - pub const BRANCH_COND: usize = 37; + pub const BRANCH_COND: usize = 36; /// Total number of columns. - pub const NUM_COLUMNS: usize = 38; + pub const NUM_COLUMNS: usize = 37; /// res half columns as an array (DWordHL). pub const RES: [usize; 4] = [RES_0, RES_1, RES_2, RES_3]; @@ -439,6 +604,11 @@ impl CpuOperation { // Trace generation // ========================================================================= +/// Preprocessed `TIMESTAMP` of `row`: `4·(row + 1)`. +fn local_timestamp(row: usize) -> u64 { + TIMESTAMP_STRIDE * (row as u64 + 1) +} + /// Generates the CPU trace table from a list of operations. /// /// Each operation becomes one row; the table is padded to the next power of 2. @@ -462,7 +632,10 @@ pub fn generate_cpu_trace( // suppressed (CPU32 owns them); only the PC-advancing columns are set. let effective = |flag: bool| !word && flag; - table.set_u64(row_idx, cols::TIMESTAMP, op.timestamp); + // Preprocessed: the table-local `4·(row + 1)`, whatever `op.timestamp` is. + // The rest of the trace builder sends `op.timestamp`, which an honest + // build makes `base + 4·(row + 1)` (see `timestamp_bases`). + table.set_u64(row_idx, cols::TIMESTAMP, local_timestamp(row_idx)); table.set_dword_wl(row_idx, cols::PC_0, op.decode.pc); // rs1/rs2/rd and read/write flags are only present on non-word rows. @@ -535,26 +708,21 @@ pub fn generate_cpu_trace( table.set_bool(row_idx, cols::BRANCH_COND, op.branch_cond); - // Inline-PC coordination columns. + // Inline-PC coordination column. let pc_double_read = !word && f.read_register1 && f.rs1 == 255; - let ts_lo = op.timestamp & 0xFFFF_FFFF; - let prev_pc_ts_borrow = !pc_double_read && ts_lo < 3; table.set_bool(row_idx, cols::PC_DOUBLE_READ, pc_double_read); - table.set_bool(row_idx, cols::PREV_PC_TIMESTAMP_BORROW, prev_pc_ts_borrow); } // Padding rows: pc = next_pc = 1 (odd, unreachable), half_instruction_length = 0 so // next_pc = pc + 0 = pc, all flags 0. The DECODE table has the matching padding // entry at pc = 1. Per spec, padding rows participate in the inline-PC `memory` // chain: each reads pc=1 at `timestamp - 3` and writes pc=1 at `timestamp + 1`, - // so their timestamps must continue the +4 cadence from the last real row (the - // halting ECALL). pc_double_read and prev_pc_timestamp_borrow stay 0, giving - // prev_ts = timestamp - 3. The first padding read (timestamp = last_ts + 4) then - // lands on last_ts + 1, where the HALT chip's emit_pc deposited pc = 1. - let last_ts = operations.last().map(|op| op.timestamp).unwrap_or(0); + // continuing the preprocessed +4 cadence from the last real row (the halting + // ECALL). pc_double_read stays 0, giving prev_ts = timestamp - 3. The first + // padding read then lands on the halting row's timestamp + 1, where the HALT + // chip's emit_pc deposited pc = 1. for row_idx in n..num_rows { - let j = (row_idx - n + 1) as u64; - table.set_u64(row_idx, cols::TIMESTAMP, last_ts + 4 * j); + table.set_u64(row_idx, cols::TIMESTAMP, local_timestamp(row_idx)); table.set_u64(row_idx, cols::PC_0, CPU_PADDING_PC); table.set_u64(row_idx, cols::NEXT_PC_0, CPU_PADDING_PC); } @@ -629,8 +797,27 @@ fn res_cast_wl() -> BusValue { } } -/// Returns the bus interactions for the CPU table. -pub fn bus_interactions() -> Vec { +/// `timestamp + ts_base + offset` as linear terms. +fn timestamp_terms(ts_base: u64, offset: i64) -> Vec { + let base = i64::try_from(ts_base).expect("CPU timestamp base fits in i64"); + vec![ + LinearTerm::Column { + coefficient: 1, + column: cols::TIMESTAMP, + }, + LinearTerm::Constant(base + offset), + ] +} + +/// `timestamp + ts_base + offset`: a timestamp slot of this row as one bus +/// element (the low word; the high word is 0, CPU timestamps fit in 32 bits). +fn timestamp_slot(ts_base: u64, offset: i64) -> BusValue { + BusValue::linear(timestamp_terms(ts_base, offset)) +} + +/// Returns the bus interactions for a CPU table whose timestamps start at +/// `ts_base` (`4·S_k` for table `k`, see [`timestamp_bases`]). +pub fn bus_interactions(ts_base: u64) -> Vec { use super::types::packed_decode_shrunk as pd; let mut interactions = Vec::with_capacity(24); @@ -702,10 +889,7 @@ pub fn bus_interactions() -> Vec { BusId::Cpu32, Multiplicity::Column(cols::WORD_INSTR), vec![ - BusValue::Packed { - start_column: cols::TIMESTAMP, - packing: Packing::Direct, - }, + timestamp_slot(ts_base, 0), BusValue::constant(0), // timestamp_hi (CPU timestamps fit in 32 bits) BusValue::Packed { start_column: cols::PC_0, @@ -727,14 +911,14 @@ pub fn bus_interactions() -> Vec { cols::RS1, cols::RV1_0, cols::RV1_1, - 0, + timestamp_slot(ts_base, 0), )); interactions.push(memw_register_read( cols::READ_REGISTER2, cols::RS2, cols::RV2_0, cols::RV2_1, - 1, + timestamp_slot(ts_base, 1), )); // Register write of rvd at timestamp+2 (16 elements, no `old`). interactions.push(BusInteraction::sender( @@ -761,14 +945,7 @@ pub fn bus_interactions() -> Vec { BusValue::constant(0), BusValue::constant(0), BusValue::constant(0), - // timestamp+2 - BusValue::linear(vec![ - LinearTerm::Column { - coefficient: 1, - column: cols::TIMESTAMP, - }, - LinearTerm::Constant(2), - ]), + timestamp_slot(ts_base, 2), BusValue::constant(0), BusValue::constant(1), // write2 (register access = 2 words) BusValue::constant(0), @@ -784,10 +961,7 @@ pub fn bus_interactions() -> Vec { BusId::MemoryOp, Multiplicity::Column(cols::MEMORY), vec![ - BusValue::Packed { - start_column: cols::TIMESTAMP, - packing: Packing::Direct, - }, + timestamp_slot(ts_base, 0), BusValue::constant(0), // timestamp_hi res_cast_wl(), // address (2 words) BusValue::Packed { @@ -810,29 +984,22 @@ pub fn bus_interactions() -> Vec { // previous timestamp, write next_pc at timestamp+1. x255 lives at addresses // 510/511. Padding rows participate too (they carry PC=1 and chain their // timestamps); the HALT chip's consume_pc/emit_pc bridges the last real write - // to the padding chain. See `docs/cpu-rework-deviations.md` (D-PAD). + // to the padding chain. + // + // The timestamp is preprocessed, so `timestamp - 3` never underflows (the + // first row of an epoch reads the REGISTER init token at 1) and + // `pc_double_read` needs no constraint beyond IS_BIT (spec `cpu.typ`): with + // it set, the read lands on this row's own `rs1 = x255` read at `timestamp`, + // and nothing else writes x255 there. // ------------------------------------------------------------------------- let pc_mult = Multiplicity::One; - // prev_ts_lo = timestamp - 3*(1 - pc_double_read) + 2^32 * borrow - let prev_ts_lo = BusValue::linear(vec![ - LinearTerm::Column { - coefficient: 1, - column: cols::TIMESTAMP, - }, - LinearTerm::Constant(-3), - LinearTerm::Column { - coefficient: 3, - column: cols::PC_DOUBLE_READ, - }, - LinearTerm::Column { - coefficient: 1i64 << 32, - column: cols::PREV_PC_TIMESTAMP_BORROW, - }, - ]); - let prev_ts_hi = BusValue::linear(vec![LinearTerm::Column { - coefficient: -1, - column: cols::PREV_PC_TIMESTAMP_BORROW, - }]); + // prev_ts = ts_base + timestamp - 3*(1 - pc_double_read) + let mut prev_ts_terms = timestamp_terms(ts_base, -3); + prev_ts_terms.push(LinearTerm::Column { + coefficient: 3, + column: cols::PC_DOUBLE_READ, + }); + let prev_ts = BusValue::linear(prev_ts_terms); for i in 0..2u64 { let pc_col = if i == 0 { cols::PC_0 } else { cols::PC_1 }; let next_pc_col = if i == 0 { @@ -848,8 +1015,8 @@ pub fn bus_interactions() -> Vec { BusValue::constant(1), BusValue::constant(510 + i), BusValue::constant(0), - prev_ts_lo.clone(), - prev_ts_hi.clone(), + prev_ts.clone(), + BusValue::constant(0), BusValue::Packed { start_column: pc_col, packing: Packing::Direct, @@ -864,13 +1031,7 @@ pub fn bus_interactions() -> Vec { BusValue::constant(1), BusValue::constant(510 + i), BusValue::constant(0), - BusValue::linear(vec![ - LinearTerm::Column { - coefficient: 1, - column: cols::TIMESTAMP, - }, - LinearTerm::Constant(1), - ]), + timestamp_slot(ts_base, 1), BusValue::constant(0), BusValue::Packed { start_column: next_pc_col, @@ -971,10 +1132,7 @@ pub fn bus_interactions() -> Vec { BusId::Ecall, Multiplicity::Column(cols::ECALL), vec![ - BusValue::Packed { - start_column: cols::TIMESTAMP, - packing: Packing::Direct, - }, + timestamp_slot(ts_base, 0), BusValue::constant(0), BusValue::Packed { start_column: cols::RV1_0, @@ -994,7 +1152,7 @@ fn memw_register_read( rs_col: usize, rv_lo_col: usize, rv_hi_col: usize, - ts_offset: i64, + ts: BusValue, ) -> BusInteraction { let value_lo = || BusValue::Packed { start_column: rv_lo_col, @@ -1004,20 +1162,6 @@ fn memw_register_read( start_column: rv_hi_col, packing: Packing::Direct, }; - let ts = if ts_offset == 0 { - BusValue::Packed { - start_column: cols::TIMESTAMP, - packing: Packing::Direct, - } - } else { - BusValue::linear(vec![ - LinearTerm::Column { - coefficient: 1, - column: cols::TIMESTAMP, - }, - LinearTerm::Constant(ts_offset), - ]) - }; BusInteraction::sender( BusId::Memw, Multiplicity::Column(read_flag_col), diff --git a/prover/src/tables/cpu_timestamp_commitments.rs b/prover/src/tables/cpu_timestamp_commitments.rs new file mode 100644 index 000000000..81663a705 --- /dev/null +++ b/prover/src/tables/cpu_timestamp_commitments.rs @@ -0,0 +1,345 @@ +// Generated by `cargo run --bin compute_static_commitments --release`. +// Do not edit by hand; see `static_timestamp_commitment`. + +/// `(blowup_factor, [commitment for log2(height) = MIN_LOG_HEIGHT..])`. +const CPU_TIMESTAMP_COMMITMENTS: &[(u8, &[Commitment])] = &[ + ( + 2, + &[ + // 2^2 + [ + 0xfd, 0x8b, 0x4b, 0x51, 0xe3, 0x95, 0x89, 0x04, 0x74, 0xfe, 0x74, 0x1d, 0x7e, 0x87, + 0xf2, 0xfc, 0x93, 0x3e, 0x68, 0x4d, 0xc5, 0x9e, 0x5b, 0xdd, 0xdb, 0x72, 0xb9, 0xb3, + 0x28, 0xcb, 0x02, 0x6f, + ], + // 2^3 + [ + 0x49, 0x9a, 0x26, 0xf7, 0x40, 0x0a, 0x85, 0xa2, 0xa1, 0x91, 0x82, 0xf7, 0x04, 0xeb, + 0x24, 0x84, 0xf1, 0x4f, 0x9e, 0xd4, 0xe6, 0xd0, 0x92, 0x6b, 0xeb, 0xe3, 0x76, 0xfc, + 0xce, 0xd1, 0x74, 0xa0, + ], + // 2^4 + [ + 0x4c, 0x97, 0x30, 0x4d, 0x72, 0xa6, 0x2a, 0x87, 0xb3, 0xeb, 0x0d, 0x8e, 0x42, 0x49, + 0xf5, 0x93, 0x80, 0x92, 0x9a, 0x84, 0x65, 0xd5, 0x16, 0xc8, 0x37, 0xa8, 0xe5, 0xaa, + 0xf6, 0xd4, 0x34, 0x36, + ], + // 2^5 + [ + 0xbd, 0x1d, 0x27, 0xf8, 0x1b, 0x7e, 0x91, 0x64, 0x57, 0x53, 0xc2, 0x83, 0xc1, 0x14, + 0xb7, 0x19, 0x5a, 0x91, 0x85, 0xb6, 0xe4, 0x6a, 0x83, 0x99, 0x4a, 0x03, 0x7b, 0x5a, + 0xb2, 0x2e, 0x69, 0xd4, + ], + // 2^6 + [ + 0xf4, 0x06, 0xca, 0x8a, 0xf0, 0xad, 0xc9, 0x4b, 0x4f, 0x95, 0x10, 0x62, 0x01, 0x0d, + 0x5f, 0x17, 0xc8, 0xac, 0xe4, 0xaa, 0xc0, 0xfb, 0xfd, 0x05, 0x48, 0x65, 0xd2, 0x78, + 0xdc, 0xa5, 0xe3, 0x36, + ], + // 2^7 + [ + 0x75, 0xd3, 0x04, 0x50, 0x29, 0x46, 0xbb, 0x1c, 0x1e, 0xc4, 0xc8, 0xf3, 0x31, 0xce, + 0xdf, 0x75, 0x34, 0x9f, 0x29, 0xba, 0x45, 0xc2, 0xb8, 0xac, 0x39, 0xdf, 0xdd, 0xd7, + 0x3b, 0x94, 0x8f, 0x11, + ], + // 2^8 + [ + 0xf9, 0xc0, 0x17, 0x76, 0x62, 0x77, 0x37, 0xeb, 0x79, 0x2d, 0x69, 0x1a, 0xa3, 0x23, + 0xd2, 0x5d, 0x7c, 0xdc, 0x37, 0xec, 0xa0, 0x9d, 0x58, 0x88, 0x6e, 0xb2, 0x6e, 0x9d, + 0x10, 0xfe, 0xac, 0x05, + ], + // 2^9 + [ + 0xbd, 0x3e, 0x4f, 0xa7, 0x6b, 0x1c, 0x3f, 0x86, 0x7d, 0xb7, 0x22, 0xaa, 0x77, 0x22, + 0x19, 0xfc, 0xe7, 0x84, 0xe6, 0x49, 0x3f, 0xb2, 0x5d, 0x44, 0x05, 0xe7, 0x38, 0x3d, + 0x7f, 0x04, 0x6e, 0x6a, + ], + // 2^10 + [ + 0xca, 0x03, 0xf5, 0x3b, 0x2b, 0x4a, 0x22, 0x5c, 0x0f, 0x95, 0x83, 0x07, 0xc6, 0x84, + 0x01, 0xe7, 0x77, 0x6e, 0xc1, 0x76, 0x05, 0x27, 0xca, 0xe2, 0xd6, 0x9a, 0x8c, 0x7e, + 0xf7, 0x10, 0xd6, 0x9d, + ], + // 2^11 + [ + 0xa7, 0x7c, 0x7e, 0x08, 0xf2, 0x91, 0xae, 0x0e, 0x29, 0x79, 0x54, 0x49, 0x4a, 0x58, + 0x0a, 0x30, 0xf8, 0x15, 0x27, 0x04, 0x8f, 0xd5, 0x19, 0xc7, 0xea, 0xf3, 0xa4, 0x11, + 0x37, 0xee, 0x3c, 0x56, + ], + // 2^12 + [ + 0x5a, 0x10, 0x18, 0x2a, 0x89, 0xb6, 0x81, 0x40, 0xc9, 0xe8, 0xb1, 0x1f, 0x29, 0x2c, + 0x49, 0xfc, 0x6f, 0xdb, 0x7a, 0x9b, 0x0f, 0x59, 0x69, 0x29, 0x36, 0x01, 0x63, 0x69, + 0x2e, 0xc0, 0x57, 0x6a, + ], + // 2^13 + [ + 0x78, 0xad, 0xd9, 0xc4, 0x4b, 0x3f, 0x8c, 0xd7, 0xa9, 0x16, 0x1f, 0xea, 0xcc, 0xe3, + 0xed, 0xcb, 0x54, 0xe8, 0x97, 0xb2, 0x42, 0x0c, 0x91, 0x7a, 0x87, 0xc5, 0xf0, 0x92, + 0xdc, 0x8d, 0x72, 0x06, + ], + // 2^14 + [ + 0x91, 0x5a, 0xe0, 0xe9, 0x0a, 0x63, 0x07, 0x38, 0xcc, 0x37, 0x30, 0xbb, 0x34, 0x94, + 0x8f, 0xc9, 0x31, 0x08, 0x55, 0xad, 0xd6, 0x83, 0x23, 0xa8, 0x41, 0x76, 0xcb, 0x4e, + 0x4d, 0x43, 0xb2, 0x43, + ], + // 2^15 + [ + 0x79, 0x06, 0x8e, 0xcd, 0xba, 0x71, 0x66, 0xd0, 0x97, 0x4b, 0xa4, 0x15, 0xf7, 0xe7, + 0x13, 0xed, 0x74, 0xbb, 0xe8, 0x30, 0xc3, 0x1a, 0x3c, 0xfa, 0xac, 0x63, 0xb9, 0x2b, + 0x40, 0x85, 0xcb, 0x0e, + ], + // 2^16 + [ + 0x68, 0x8a, 0xbc, 0x2a, 0x54, 0x31, 0xd9, 0x6a, 0x06, 0xa7, 0x7d, 0xbd, 0xab, 0x20, + 0x85, 0xe8, 0x69, 0x0d, 0x8e, 0xa9, 0x9b, 0x48, 0x8e, 0x50, 0xad, 0xed, 0x7d, 0xc8, + 0x8e, 0x64, 0xb1, 0xeb, + ], + // 2^17 + [ + 0xd3, 0x14, 0xcb, 0x64, 0x69, 0x87, 0x5f, 0x17, 0xdb, 0x16, 0x52, 0x64, 0x73, 0xfd, + 0x80, 0xba, 0x8e, 0xe1, 0x99, 0xc2, 0x4a, 0x58, 0xbf, 0xc7, 0x7a, 0x70, 0x2f, 0x7c, + 0xec, 0x95, 0xc3, 0x90, + ], + // 2^18 + [ + 0x34, 0x6d, 0xaf, 0xc2, 0xcd, 0x01, 0x17, 0x5c, 0xd2, 0x94, 0xb8, 0x5e, 0x22, 0x26, + 0x52, 0x48, 0x37, 0xfe, 0xd0, 0x22, 0x33, 0x25, 0x2c, 0xe5, 0x76, 0x51, 0x47, 0xa0, + 0xf8, 0x2b, 0xc7, 0xe2, + ], + // 2^19 + [ + 0xcc, 0xcb, 0x01, 0xe3, 0xba, 0x8d, 0x22, 0x17, 0x3a, 0xf2, 0x27, 0xe0, 0x96, 0x4e, + 0x43, 0xc5, 0xad, 0xe2, 0xa5, 0x2f, 0xde, 0xf1, 0x2f, 0x06, 0xd8, 0xb6, 0x11, 0xa5, + 0x1c, 0x2e, 0x5f, 0x38, + ], + ], + ), + ( + 4, + &[ + // 2^2 + [ + 0x72, 0xfb, 0x27, 0x34, 0x7e, 0x41, 0x05, 0x71, 0x69, 0x09, 0x4b, 0xec, 0x84, 0xac, + 0xba, 0x2f, 0xc2, 0xc6, 0xe0, 0xc9, 0xd2, 0xe5, 0x31, 0xfb, 0x8b, 0x28, 0xab, 0xaf, + 0x98, 0x9b, 0xd7, 0x2a, + ], + // 2^3 + [ + 0x21, 0x02, 0x0b, 0x76, 0x14, 0xb4, 0x95, 0xe4, 0xd9, 0x12, 0x36, 0x10, 0xf9, 0x22, + 0xe7, 0xb5, 0x25, 0x85, 0x4d, 0xc8, 0x67, 0x7f, 0xf2, 0xb9, 0x48, 0xd1, 0x63, 0xd5, + 0x96, 0x2a, 0x22, 0x7a, + ], + // 2^4 + [ + 0xc6, 0x94, 0x7a, 0x1e, 0x5f, 0xd6, 0xfd, 0x1e, 0x74, 0x5a, 0xc1, 0xb9, 0x96, 0xa5, + 0xad, 0x1b, 0x22, 0x08, 0xcf, 0xe2, 0x63, 0x75, 0x27, 0x82, 0xb2, 0xdf, 0x34, 0x9b, + 0xaa, 0x79, 0xbf, 0x35, + ], + // 2^5 + [ + 0x16, 0x97, 0x32, 0x3b, 0x4d, 0x1e, 0x52, 0x9b, 0x15, 0xdf, 0x44, 0xad, 0x52, 0x06, + 0x8d, 0x75, 0xbc, 0x6b, 0xc9, 0xf6, 0x2c, 0x1c, 0x7b, 0x9a, 0x37, 0x50, 0x25, 0x12, + 0x75, 0x0b, 0xc1, 0xd0, + ], + // 2^6 + [ + 0x01, 0x20, 0x61, 0xdf, 0x58, 0xe2, 0xfa, 0x8e, 0x1b, 0xcf, 0x6e, 0xe7, 0xc9, 0x59, + 0xc7, 0x9b, 0xd8, 0xb3, 0xad, 0x72, 0x31, 0x0d, 0xe8, 0x8a, 0x86, 0xff, 0xea, 0x57, + 0xa6, 0xc3, 0x77, 0x3f, + ], + // 2^7 + [ + 0x72, 0x22, 0x3a, 0x03, 0x6b, 0x0c, 0x2f, 0x7f, 0x77, 0xe1, 0xce, 0xb5, 0x83, 0x07, + 0x00, 0xdc, 0xef, 0x01, 0x2b, 0xd0, 0x06, 0xbf, 0x68, 0x3d, 0x13, 0x04, 0x6d, 0x47, + 0x0c, 0x87, 0xd0, 0x80, + ], + // 2^8 + [ + 0x60, 0x65, 0x01, 0x60, 0xc8, 0xc4, 0x09, 0x68, 0x3d, 0x64, 0xbc, 0x88, 0xaa, 0xd0, + 0x80, 0xff, 0xb0, 0xac, 0x3b, 0x77, 0x25, 0x38, 0x09, 0x1d, 0xa2, 0x0e, 0xb5, 0x54, + 0x54, 0x81, 0x5c, 0x76, + ], + // 2^9 + [ + 0x8a, 0x15, 0x89, 0xb7, 0xef, 0xb3, 0xdb, 0x94, 0x14, 0x89, 0x51, 0x1f, 0x9d, 0x7d, + 0x08, 0xbf, 0xea, 0x3f, 0xb7, 0xa2, 0x79, 0xe8, 0xb4, 0x41, 0x6b, 0x7d, 0xd2, 0xa0, + 0x8b, 0x2d, 0xcc, 0xb5, + ], + // 2^10 + [ + 0xa3, 0xa6, 0x4e, 0x9e, 0x84, 0x87, 0x5d, 0x40, 0xb7, 0x2d, 0xe0, 0x01, 0x52, 0x64, + 0x3f, 0xa1, 0xa3, 0x3f, 0xd5, 0x16, 0x37, 0x79, 0x53, 0xcc, 0x0a, 0x92, 0x3c, 0x48, + 0xed, 0x44, 0x44, 0x28, + ], + // 2^11 + [ + 0x30, 0xca, 0x16, 0x42, 0xf4, 0xdf, 0x7b, 0xe6, 0x9e, 0xe1, 0x2b, 0xa7, 0x9f, 0x90, + 0x6a, 0x20, 0x29, 0x15, 0x9a, 0xdb, 0xca, 0xa4, 0x92, 0xe2, 0x46, 0x84, 0x75, 0x92, + 0x0d, 0x8d, 0x84, 0x41, + ], + // 2^12 + [ + 0xc5, 0x98, 0xfe, 0xdb, 0x5a, 0x88, 0x83, 0x9f, 0x6b, 0x56, 0x0c, 0xd2, 0x74, 0x14, + 0xbd, 0xa6, 0x24, 0xf0, 0x8e, 0x4d, 0x99, 0xc1, 0x19, 0x14, 0xc5, 0x60, 0x54, 0x09, + 0x62, 0x98, 0x50, 0xcb, + ], + // 2^13 + [ + 0x96, 0xd1, 0xc2, 0x6b, 0x13, 0x17, 0x13, 0x74, 0x55, 0xc3, 0xbd, 0x03, 0x12, 0x14, + 0xd0, 0x79, 0x58, 0x86, 0x6b, 0x6c, 0x3b, 0x96, 0xb7, 0x5b, 0x82, 0x91, 0x3f, 0x61, + 0x17, 0x00, 0xf1, 0x3d, + ], + // 2^14 + [ + 0xa5, 0xe7, 0xb9, 0xf8, 0x53, 0x00, 0x7a, 0xb8, 0xe8, 0x0f, 0x6d, 0xd7, 0x8e, 0x5e, + 0x03, 0x0f, 0x02, 0xb5, 0x54, 0x93, 0x9c, 0x79, 0x15, 0xe5, 0x23, 0xe0, 0x22, 0x77, + 0x2a, 0xca, 0x61, 0xc1, + ], + // 2^15 + [ + 0x88, 0x06, 0xdf, 0x8b, 0x12, 0xd1, 0x1a, 0x3e, 0x2e, 0x5f, 0x51, 0x04, 0x1d, 0xc5, + 0xcc, 0x59, 0xcf, 0x9a, 0x41, 0x6f, 0x01, 0x94, 0xb1, 0x72, 0xed, 0x8d, 0xa5, 0x42, + 0x76, 0xa3, 0x00, 0x41, + ], + // 2^16 + [ + 0xaf, 0x29, 0x3c, 0x38, 0xa8, 0x99, 0xff, 0x34, 0x03, 0x99, 0xd9, 0xf2, 0x0e, 0xd1, + 0xb8, 0x97, 0xbb, 0xfe, 0xdd, 0x7c, 0xde, 0x73, 0x58, 0xc7, 0xb4, 0x55, 0x9e, 0xd4, + 0xd2, 0x60, 0x52, 0x70, + ], + // 2^17 + [ + 0x50, 0x65, 0x02, 0xb2, 0x27, 0x17, 0xa4, 0x11, 0x20, 0xbd, 0xe7, 0x4c, 0xb2, 0x6e, + 0x60, 0x38, 0x43, 0x63, 0x8c, 0xac, 0x93, 0xae, 0x3e, 0x5f, 0xdf, 0x2a, 0x80, 0xcf, + 0x11, 0xad, 0x33, 0x22, + ], + // 2^18 + [ + 0xf1, 0x41, 0x4b, 0x26, 0xf4, 0x8b, 0x56, 0x57, 0x6c, 0xf2, 0xd2, 0x94, 0xb0, 0x14, + 0x96, 0xea, 0x1e, 0x29, 0x40, 0xf4, 0xbc, 0x39, 0xfa, 0x67, 0xbf, 0x95, 0xfc, 0xc7, + 0x97, 0xc7, 0xf4, 0x5f, + ], + // 2^19 + [ + 0x24, 0x8d, 0xb4, 0x2e, 0x6c, 0x0c, 0x82, 0xde, 0xdb, 0x42, 0x39, 0xc7, 0x2e, 0x7f, + 0x54, 0x2b, 0x43, 0xb7, 0x8b, 0xb0, 0xa3, 0x99, 0x0d, 0x27, 0x22, 0x8e, 0x0f, 0x3b, + 0xbe, 0x50, 0xba, 0x80, + ], + ], + ), + ( + 8, + &[ + // 2^2 + [ + 0x98, 0xc7, 0xf8, 0x35, 0x47, 0xce, 0x3d, 0x35, 0xd0, 0xc4, 0xf3, 0x9a, 0x73, 0x80, + 0x8d, 0x7e, 0x6a, 0xd5, 0xcd, 0x43, 0x77, 0x57, 0x10, 0x9f, 0xd8, 0xf6, 0x7f, 0xe8, + 0x99, 0xe3, 0x19, 0xe7, + ], + // 2^3 + [ + 0x5b, 0xb8, 0x15, 0xd7, 0x98, 0xc9, 0xd5, 0x64, 0x45, 0x13, 0x22, 0x04, 0x4c, 0xe4, + 0x8d, 0xac, 0xa3, 0x8b, 0x48, 0x3f, 0x44, 0xc5, 0xe0, 0xa2, 0xb0, 0xf9, 0x65, 0x91, + 0x75, 0x3f, 0xb7, 0xb3, + ], + // 2^4 + [ + 0x5a, 0x94, 0x7f, 0xd5, 0x59, 0xb3, 0xb6, 0x95, 0xc2, 0x26, 0x74, 0x06, 0x2b, 0x93, + 0x3b, 0xb9, 0xd6, 0x1e, 0x57, 0xb1, 0x0c, 0x11, 0x74, 0x53, 0xe3, 0x5e, 0x45, 0xb9, + 0x90, 0x61, 0x82, 0x7a, + ], + // 2^5 + [ + 0xb6, 0xe5, 0x3f, 0x5a, 0xc5, 0x88, 0x33, 0x63, 0xdb, 0xd8, 0x56, 0xc9, 0xf5, 0xc9, + 0x17, 0x35, 0x9f, 0x10, 0xd3, 0xd8, 0xfd, 0x76, 0x45, 0xd7, 0x0c, 0x08, 0x54, 0x25, + 0xc7, 0xaa, 0xec, 0x7b, + ], + // 2^6 + [ + 0xc2, 0x9b, 0x84, 0x12, 0x3c, 0x40, 0x5d, 0x4b, 0xf6, 0x5b, 0x02, 0x25, 0x04, 0x2e, + 0x1d, 0x05, 0x06, 0x25, 0x16, 0xfb, 0x19, 0x7f, 0xa1, 0x48, 0x13, 0x4f, 0xb2, 0xaf, + 0x36, 0x5c, 0x7d, 0xec, + ], + // 2^7 + [ + 0x77, 0x8e, 0x69, 0x8a, 0xde, 0x86, 0xee, 0xaf, 0x95, 0xa3, 0xfb, 0x01, 0x9f, 0x7b, + 0xbe, 0x1d, 0x67, 0xe2, 0x02, 0x83, 0x51, 0xb8, 0x83, 0xbf, 0x70, 0x8b, 0x95, 0x43, + 0x5c, 0x29, 0x4f, 0x5c, + ], + // 2^8 + [ + 0xbf, 0xc4, 0x7f, 0x00, 0xd9, 0x4b, 0x6a, 0xc3, 0x85, 0x01, 0xbe, 0x0f, 0x75, 0x8f, + 0xb4, 0xd6, 0x0e, 0xf2, 0x93, 0xc3, 0x92, 0x74, 0x96, 0xa5, 0xef, 0x05, 0xe3, 0x05, + 0xce, 0x57, 0x44, 0xb6, + ], + // 2^9 + [ + 0xc3, 0x28, 0x64, 0xac, 0xd1, 0xc7, 0x85, 0x0c, 0x9b, 0xf0, 0xdf, 0x3e, 0x55, 0x84, + 0xbb, 0x19, 0x6f, 0x9d, 0xe7, 0x12, 0x0f, 0x7d, 0x83, 0x8e, 0x2c, 0xd1, 0x2c, 0xda, + 0xfe, 0x93, 0xd1, 0xd9, + ], + // 2^10 + [ + 0xe0, 0x1c, 0x59, 0x0e, 0x4e, 0xf3, 0xbf, 0xb2, 0x94, 0xc1, 0xe0, 0xa5, 0x6d, 0x06, + 0x4e, 0xd6, 0x0e, 0x59, 0x63, 0x18, 0x24, 0xfb, 0x18, 0xea, 0xf6, 0x5d, 0xb9, 0x41, + 0x85, 0x6d, 0x85, 0x2e, + ], + // 2^11 + [ + 0xe7, 0x1e, 0x5b, 0x58, 0x79, 0x59, 0x2f, 0x67, 0x95, 0x23, 0x99, 0x51, 0x02, 0x4d, + 0xf8, 0x72, 0xd4, 0x3c, 0x41, 0x16, 0xaa, 0x01, 0xc4, 0xaf, 0x88, 0x30, 0x2d, 0x95, + 0xc7, 0xec, 0x81, 0xc3, + ], + // 2^12 + [ + 0x52, 0x36, 0x52, 0x5e, 0x1f, 0x1a, 0x6b, 0xbe, 0x39, 0x7f, 0x92, 0x93, 0x92, 0x2f, + 0xcc, 0x34, 0x8f, 0x16, 0x91, 0xfc, 0xd4, 0x56, 0xc2, 0xe3, 0x96, 0xa9, 0x4e, 0x31, + 0x9c, 0x42, 0x00, 0x36, + ], + // 2^13 + [ + 0xd9, 0xe3, 0xd8, 0x18, 0xaa, 0x8f, 0x5d, 0xbd, 0xc0, 0xf5, 0x43, 0x31, 0x8b, 0xe5, + 0x32, 0x06, 0xad, 0x54, 0xe1, 0x65, 0x61, 0xec, 0x42, 0x9c, 0x72, 0xac, 0x09, 0x7c, + 0x7d, 0xb7, 0xc0, 0x4c, + ], + // 2^14 + [ + 0xc7, 0x8e, 0x04, 0x79, 0xb7, 0x17, 0x4b, 0xdf, 0x50, 0xd4, 0x81, 0xa2, 0xa8, 0x23, + 0xcb, 0x13, 0x3e, 0xad, 0x7b, 0xe4, 0x3b, 0x41, 0x1b, 0x08, 0x81, 0x5e, 0xde, 0xf5, + 0xc4, 0x02, 0x2c, 0xdb, + ], + // 2^15 + [ + 0x78, 0xb3, 0x81, 0xf0, 0x7f, 0xa3, 0xda, 0x3d, 0xf8, 0xd8, 0x7a, 0x7c, 0xdb, 0x50, + 0x72, 0x2b, 0x13, 0x6a, 0x60, 0x96, 0x1e, 0xfb, 0xff, 0xf3, 0x2a, 0xe2, 0x7a, 0x4e, + 0x3a, 0xf5, 0xdc, 0x70, + ], + // 2^16 + [ + 0xcc, 0x75, 0x75, 0xba, 0x3f, 0x0f, 0xfe, 0x0e, 0x25, 0x2c, 0x66, 0xc0, 0x64, 0xfc, + 0xc5, 0xd3, 0x56, 0x67, 0xf9, 0x63, 0x7c, 0xe2, 0xc8, 0x4c, 0xa7, 0x3e, 0xca, 0xfa, + 0x9a, 0x6f, 0x99, 0x7c, + ], + // 2^17 + [ + 0x77, 0xfa, 0x2e, 0x51, 0xe5, 0x57, 0xbf, 0x89, 0xbd, 0x3f, 0xf2, 0x3f, 0x93, 0xde, + 0x89, 0xdb, 0xb5, 0x5e, 0xb3, 0x84, 0xca, 0xce, 0x33, 0xc5, 0x28, 0x27, 0x4e, 0x27, + 0x2d, 0x26, 0x39, 0xa9, + ], + // 2^18 + [ + 0xce, 0x49, 0x07, 0x32, 0xb5, 0x54, 0x0f, 0x96, 0xea, 0xad, 0x27, 0xff, 0x0c, 0x72, + 0xa5, 0xab, 0x1f, 0x72, 0xf0, 0x57, 0x96, 0x24, 0xb0, 0x7c, 0xce, 0x66, 0xe5, 0x2d, + 0xd7, 0xde, 0xf6, 0x29, + ], + // 2^19 + [ + 0xcb, 0xa5, 0xef, 0x03, 0x64, 0xe1, 0x49, 0xcb, 0x87, 0xa5, 0x66, 0x76, 0xf7, 0x71, + 0xb0, 0x80, 0x12, 0x6f, 0x85, 0xcb, 0x84, 0x9d, 0xac, 0xe1, 0x15, 0xeb, 0x49, 0x45, + 0x17, 0x3b, 0x06, 0x40, + ], + ], + ), +]; diff --git a/prover/src/tables/halt.rs b/prover/src/tables/halt.rs index 675e10170..24bb41be1 100644 --- a/prover/src/tables/halt.rs +++ b/prover/src/tables/halt.rs @@ -11,7 +11,7 @@ //! ## Bus Interactions //! - **Receiver**: ECALL bus - receives `[timestamp, cast(rv1, DWordWL)]` from CPU //! when the ECALL flag is set (rv1 must be 93 = sys_exit) -//! - **Sender**: MEMW bus - 31 register finalization interactions at `ts = 2^64-1`: +//! - **Sender**: MEMW bus - 31 register finalization interactions at `ts = 2^32-1`: //! - x1-x9: write 0 (zeroize lo GPRs) //! - x10: read with old=0 (enforce exit_code=0; non-zero → bus imbalance → proof failure) //! - x11-x31: write 0 (zeroize hi GPRs) @@ -20,7 +20,11 @@ //! the halting instruction and *re-emits* `pc = 1`. This bridges the last real PC //! write to the CPU padding rows (which all carry PC=1); the padding chain then //! carries PC=1 to the REGISTER table's final token. x255 is therefore NOT -//! finalized via MEMW at `2^64-1` anymore. +//! finalized via MEMW at `2^32-1` anymore. +//! +//! `2^32-1` is the largest `Word` timestamp (spec `halt.toml`). Every CPU +//! timestamp stays below it: an epoch has at most +//! [`super::cpu::MAX_CPU_ROWS`] CPU rows, whose last access is at `4·N + 2`. //! //! Corresponding MEMW table rows are generated in trace_builder. //! @@ -36,6 +40,10 @@ use super::types::{BusId, GoldilocksExtension, GoldilocksField, VmTable}; // Column indices for HALT table // ========================================================================= +/// Timestamp of HALT's register finalization: `2^32 - 1`, the maximum `Word` +/// timestamp (spec `halt.toml`), after every CPU access. +pub const HALT_TIMESTAMP: u64 = (1 << 32) - 1; + /// Column definitions for the HALT table. pub mod cols { /// timestamp[0]: Word (lower 32 bits of halt timestamp) @@ -106,22 +114,22 @@ fn halt_read_bus_values(base_addr: u64) -> Vec { BusValue::constant(0), BusValue::constant(0), // input (same 16 elements as write format) - BusValue::constant(1), // is_register = 1 - BusValue::constant(base_addr), // base_address[0] - BusValue::constant(0), // base_address[1] - BusValue::constant(0), // value[0] = 0 - BusValue::constant(0), // value[1] - BusValue::constant(0), // value[2] - BusValue::constant(0), // value[3] - BusValue::constant(0), // value[4] - BusValue::constant(0), // value[5] - BusValue::constant(0), // value[6] - BusValue::constant(0), // value[7] - BusValue::constant(0xFFFF_FFFF), // timestamp[0] = lo(2^64-1) - BusValue::constant(0xFFFF_FFFF), // timestamp[1] = hi(2^64-1) - BusValue::constant(1), // write2 = 1 - BusValue::constant(0), // write4 = 0 - BusValue::constant(0), // write8 = 0 + BusValue::constant(1), // is_register = 1 + BusValue::constant(base_addr), // base_address[0] + BusValue::constant(0), // base_address[1] + BusValue::constant(0), // value[0] = 0 + BusValue::constant(0), // value[1] + BusValue::constant(0), // value[2] + BusValue::constant(0), // value[3] + BusValue::constant(0), // value[4] + BusValue::constant(0), // value[5] + BusValue::constant(0), // value[6] + BusValue::constant(0), // value[7] + BusValue::constant(HALT_TIMESTAMP), // timestamp[0] = 2^32-1 + BusValue::constant(0), // timestamp[1] + BusValue::constant(1), // write2 = 1 + BusValue::constant(0), // write4 = 0 + BusValue::constant(0), // write8 = 0 ] } @@ -131,29 +139,29 @@ fn halt_read_bus_values(base_addr: u64) -> Vec { /// timestamp[0..1], write2, write4, write8]`. fn halt_write_bus_values(base_addr: u64, value_lo: u64) -> Vec { vec![ - BusValue::constant(1), // is_register = 1 - BusValue::constant(base_addr), // base_address[0] - BusValue::constant(0), // base_address[1] - BusValue::constant(value_lo), // value[0] - BusValue::constant(0), // value[1] - BusValue::constant(0), // value[2] - BusValue::constant(0), // value[3] - BusValue::constant(0), // value[4] - BusValue::constant(0), // value[5] - BusValue::constant(0), // value[6] - BusValue::constant(0), // value[7] - BusValue::constant(0xFFFF_FFFF), // timestamp[0] = lo(2^64-1) - BusValue::constant(0xFFFF_FFFF), // timestamp[1] = hi(2^64-1) - BusValue::constant(1), // write2 = 1 - BusValue::constant(0), // write4 = 0 - BusValue::constant(0), // write8 = 0 + BusValue::constant(1), // is_register = 1 + BusValue::constant(base_addr), // base_address[0] + BusValue::constant(0), // base_address[1] + BusValue::constant(value_lo), // value[0] + BusValue::constant(0), // value[1] + BusValue::constant(0), // value[2] + BusValue::constant(0), // value[3] + BusValue::constant(0), // value[4] + BusValue::constant(0), // value[5] + BusValue::constant(0), // value[6] + BusValue::constant(0), // value[7] + BusValue::constant(HALT_TIMESTAMP), // timestamp[0] = 2^32-1 + BusValue::constant(0), // timestamp[1] + BusValue::constant(1), // write2 = 1 + BusValue::constant(0), // write4 = 0 + BusValue::constant(0), // write8 = 0 ] } /// Creates all bus interactions for the HALT table. /// /// - **ECALL receiver**: receives `[timestamp, cast(rv1, DWordWL)]` from CPU -/// - **MEMW senders** (31 total): register finalization at `ts = 2^64-1` +/// - **MEMW senders** (31 total): register finalization at `ts = 2^32-1` /// - x1-x9: write 0 (zeroize lo GPRs) /// - x10: read with old=0 (enforce exit_code=0) /// - x11-x31: write 0 (zeroize hi GPRs) @@ -181,7 +189,7 @@ pub fn bus_interactions() -> Vec { ], )); - // x1-x9: write 0 at ts=2^64-1 (zeroize lo registers) + // x1-x9: write 0 at ts=2^32-1 (zeroize lo registers) for i in 1..=9u64 { interactions.push(BusInteraction::sender( BusId::Memw, @@ -190,7 +198,7 @@ pub fn bus_interactions() -> Vec { )); } - // x10: read with old=0 at ts=2^64-1 (verify exit code = 0) + // x10: read with old=0 at ts=2^32-1 (verify exit code = 0) // Per spec halt:c:read_zero_exit_code: enforces that x10 was 0 at halt. // Non-zero exit code → bus imbalance → proof failure. interactions.push(BusInteraction::sender( @@ -199,7 +207,7 @@ pub fn bus_interactions() -> Vec { halt_read_bus_values(20), )); - // x11-x31: write 0 at ts=2^64-1 (zeroize hi registers) + // x11-x31: write 0 at ts=2^32-1 (zeroize hi registers) for i in 11..=31u64 { interactions.push(BusInteraction::sender( BusId::Memw, diff --git a/prover/src/tables/memw.rs b/prover/src/tables/memw.rs index 282b0c312..ee17a4c8f 100644 --- a/prover/src/tables/memw.rs +++ b/prover/src/tables/memw.rs @@ -121,8 +121,7 @@ pub struct MemwOperation { /// Previous values at the addresses (filled by memory model). Same element /// domain as `value` (byte or 32-bit register half) → `[u32; 8]`. pub old: [u32; 8], - /// Previous timestamps at the addresses (filled by memory model). Timestamps - /// can reach u64::MAX (HALT), so these stay `[u64; 8]`. + /// Previous timestamps at the addresses (filled by memory model). pub old_timestamp: [u64; 8], } diff --git a/prover/src/tables/register.rs b/prover/src/tables/register.rs index c701c3db4..9e1f24fde 100644 --- a/prover/src/tables/register.rs +++ b/prover/src/tables/register.rs @@ -7,7 +7,9 @@ //! ## Token Model //! //! - **REG-C1**: Receives initial token `(1, address, ts=1, init)` - balances MEMW's send on first access -//! - **REG-C2**: Sends final token `(1, address, timestamp, fini)` - balances MEMW's receive on last access +//! - **REG-C2**: Sends final token `(1, address, timestamp, fini)` - balances MEMW's receive on last access. +//! For the PC (x255) the timestamp is the verifier-known `final_pc_ts` instead +//! of the `timestamp` column (spec `halt.typ`). //! //! ## Columns //! @@ -16,9 +18,10 @@ //! | offset | RowIndex | Word address within register space (preprocessed) | //! | init | Word | Initial value (preprocessed) | //! | fini | Word | Final value (preprocessed) | -//! | timestamp | DWordWL | Final timestamp (1 if never accessed) | +//! | is_pc | Bit | 1 on the two x255 rows (preprocessed) | +//! | timestamp | DWordWL | Final timestamp (1 if never accessed; unused on x255 rows) | //! -//! OFFSET, INIT and FINI are preprocessed, so the verifier knows both register +//! OFFSET, INIT, FINI and IS_PC are preprocessed, so the verifier knows both register //! files. A monolithic proof (and the final continuation epoch) pins FINI to the //! halted state ([`halted_fini`]); a non-final epoch's FINI is the next epoch's INIT. @@ -55,17 +58,18 @@ pub const WORDS_PER_REGISTER: usize = 2; /// -1 because x254 is single-word (1 address instead of 2). pub const NUM_REGISTER_ADDRESSES: usize = NUM_REGISTERS * WORDS_PER_REGISTER - 1; -/// Number of preprocessed columns (OFFSET, INIT, FINI). OFFSET encodes the Word -/// address, INIT the initial value and FINI the final one, so both register files -/// are verifier-known public values: the verifier recomputes the commitment from -/// them and the REG-C2 Memory-bus token forces FINI to equal the true final -/// registers. +/// Number of preprocessed columns (OFFSET, INIT, FINI, IS_PC). OFFSET encodes the +/// Word address, INIT the initial value and FINI the final one, so both register +/// files are verifier-known public values: the verifier recomputes the commitment +/// from them and the REG-C2 Memory-bus token forces FINI to equal the true final +/// registers. IS_PC selects the x255 rows, whose final token REG-C2 sends at the +/// verifier-known final PC timestamp. /// /// A continuation epoch preprocesses FINI = `R_{i+1}` and the next epoch reuses it /// as its INIT, binding `init(epoch i+1) == fini(epoch i)` with no extra bus. A /// monolithic proof (and the final epoch) pins FINI to the halted state (see /// [`halted_fini`]). -pub const NUM_PREPROCESSED_COLS: usize = 3; +pub const NUM_PREPROCESSED_COLS: usize = 4; // ========================================================================= // Column indices for REGISTER table @@ -81,14 +85,17 @@ pub mod cols { /// fini: Final Word value (preprocessed) pub const FINI: usize = 2; + /// is_pc: 1 on the x255 (PC) rows, 0 elsewhere (preprocessed) + pub const IS_PC: usize = 3; + /// timestamp[0]: Final timestamp low word (1 if never accessed, matching REG-C1 init) - pub const TIMESTAMP_LO: usize = 3; + pub const TIMESTAMP_LO: usize = 4; /// timestamp[1]: Final timestamp high word - pub const TIMESTAMP_HI: usize = 4; + pub const TIMESTAMP_HI: usize = 5; /// Total number of columns - pub const NUM_COLUMNS: usize = 5; + pub const NUM_COLUMNS: usize = 6; } // ========================================================================= @@ -179,11 +186,11 @@ pub(crate) fn register_init_from_entry_point(entry_point: u64) -> Vec { /// consume/emit and keep executing past the exit ecall, ending the chain on the /// last post-exit `next_pc` (see `tests/halt_pc_forgery_poc.rs`). /// -/// Only the final PC *value* is pinned; its timestamp (REGISTER TIMESTAMP) stays -/// prover-chosen, unlike spec `halt.typ`, which has the verifier know the final -/// padding-PC timestamp. The value is enough: no real row writes `next_pc = 1` -/// (instruction addresses are even and BRANCH clears the LSB), so a token with -/// value 1 can only come from HALT's emit or a padding row after it. +/// The final PC timestamp is pinned too (REG-C2 consumes x255 at the +/// verifier-known `final_pc_ts`, spec `halt.typ`), but the value alone already +/// suffices: no real row writes `next_pc = 1` (instruction addresses are even +/// and BRANCH clears the LSB), so a token with value 1 can only come from +/// HALT's emit or a padding row after it. pub fn halted_fini(committed_bytes: u32) -> Vec { let mut fini = vec![0u32; NUM_REGISTER_ADDRESSES]; fini[X254_INDEX] = committed_bytes; @@ -278,6 +285,7 @@ pub fn generate_register_trace( }; table.set_word(row, cols::FINI, fini_value); + table.set_bool(row, cols::IS_PC, is_pc_address(word_addr)); table.set_dword_wl(row, cols::TIMESTAMP_LO, timestamp); } @@ -330,11 +338,12 @@ pub fn fini_from_final_state(final_state: &FinalRegisterStateMap, init: &[u32]) /// Computes the Merkle root commitment over the LDE of the REGISTER preprocessed /// columns: OFFSET (the Word address: 0..63 for x0-x31, 508 for x254, 510-511 for -/// x255), INIT and FINI, so the verifier recomputes it from the public `init` and -/// `fini` and the proof's FINI column is locked to `fini`. `fini` is the vector +/// x255), INIT, FINI and IS_PC, so the verifier recomputes it from the public `init` +/// and `fini` and the proof's FINI column is locked to `fini`. `fini` is the vector /// produced by `fini_from_trace` (entry `i` = the register at /// `register_word_address_list()[i]`). Must match the column order of the REGISTER -/// trace (OFFSET, INIT, FINI), and FINI on padding rows is 0 (as the trace builds it). +/// trace (OFFSET, INIT, FINI, IS_PC), and FINI and IS_PC on padding rows are 0 (as +/// the trace builds them). pub fn compute_precomputed_commitment( options: &ProofOptions, init: &[u32], @@ -347,14 +356,16 @@ pub fn compute_precomputed_commitment( let mut offset_col = crate::tables::types::zeroed_fe_vec(num_rows); let mut init_col = crate::tables::types::zeroed_fe_vec(num_rows); let mut fini_col = crate::tables::types::zeroed_fe_vec(num_rows); + let mut is_pc_col = crate::tables::types::zeroed_fe_vec(num_rows); for i in 0..NUM_REGISTER_ADDRESSES { offset_col[i] = FE::from(addr_list[i]); init_col[i] = FE::from(init.get(i).copied().unwrap_or(0) as u64); fini_col[i] = FE::from(fini[i] as u64); + is_pc_col[i] = FE::from(u64::from(is_pc_address(addr_list[i]))); } - commit_register_columns(options, vec![offset_col, init_col, fini_col]) + commit_register_columns(options, vec![offset_col, init_col, fini_col, is_pc_col]) } /// LDE + bit-reverse + Merkle-commit the given preprocessed columns (in column @@ -393,10 +404,15 @@ fn commit_register_columns(options: &ProofOptions, columns: Vec>) -> Com /// ## Bus Interactions /// /// - REG-C1: memory[1, address, 1, init] - receiver, multiplicity -1 -/// - REG-C2: memory[1, address, timestamp, fini] - sender, multiplicity 1 +/// - REG-C2: memory[1, address, timestamp, fini] - sender, multiplicity `1 - is_pc` +/// - REG-C2 (PC): memory[1, address, final_pc_ts, fini] - sender, multiplicity `is_pc` +/// +/// `final_pc_ts` is where the last CPU row writes `next_pc` +/// ([`super::cpu::final_pc_timestamp`]). The verifier derives it from the CPU +/// table heights, so the PC chain's end is verifier-known (spec `halt.typ`). /// /// Note: is_register=1 (constant) to distinguish from memory (is_register=0). -pub fn bus_interactions() -> Vec { +pub fn bus_interactions(final_pc_ts: u64) -> Vec { // Address is just the offset in register space. // Stored in low word, high word is 0 let address_lo = BusValue::Packed { @@ -431,11 +447,29 @@ pub fn bus_interactions() -> Vec { }, ], ), + // REG-C2 (PC): memory[1, address, final_pc_ts, fini] - send the final PC + // token at the verifier-known timestamp. Balances the last CPU row's + // inline-PC write. + BusInteraction::sender( + BusId::Memory, + Multiplicity::Column(cols::IS_PC), + vec![ + BusValue::constant(1), + address_lo.clone(), + address_hi.clone(), + BusValue::constant(final_pc_ts), + BusValue::constant(0), + BusValue::Packed { + start_column: cols::FINI, + packing: Packing::Direct, + }, + ], + ), // REG-C2: memory[1, address, timestamp, fini] - send final token // Balances MEMW's last receive on this address BusInteraction::sender( BusId::Memory, - Multiplicity::One, + Multiplicity::Negated(cols::IS_PC), vec![ // is_register = 1 BusValue::constant(1), @@ -467,6 +501,11 @@ pub fn bus_interactions() -> Vec { // Helper functions // ========================================================================= +/// Whether `word_addr` is one of the two x255 (PC) Word addresses. +fn is_pc_address(word_addr: u64) -> bool { + word_addr == 510 || word_addr == 511 +} + /// Compute the base address for a register index. pub fn register_base_address(reg_idx: u8) -> u64 { match reg_idx { diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index c37ee5dee..914052e85 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -1376,7 +1376,7 @@ fn collect_commit_memw_ops( /// Collects HALT finalization MEMW operations for all 33 registers. /// -/// Per spec (halt.toml): at timestamp 2^64-1, HALT finalizes the GP registers: +/// Per spec (halt.toml): at timestamp 2^32-1, HALT finalizes the GP registers: /// - x1-x9, x11-x31: write 0 (zeroize) /// - x10: read (verify exit code = 0; if x10 ≠ 0, proof fails via bus mismatch) /// @@ -1387,7 +1387,7 @@ fn collect_commit_memw_ops( /// the finalized GP register values. fn collect_halt_ops(register_state: &mut RegisterState) -> Vec { let mut ops = Vec::with_capacity(32); - let ts = u64::MAX; + let ts = halt::HALT_TIMESTAMP; // x1-x9: write 0 for i in 1..=9u8 { @@ -1400,7 +1400,7 @@ fn collect_halt_ops(register_state: &mut RegisterState) -> Vec { register_state.write(i, 0, ts); } - // x10: read with old=0 at ts=2^64-1 (enforce exit_code=0) + // x10: read with old=0 at ts=2^32-1 (enforce exit_code=0) // Per spec halt:c:read_zero_exit_code: old=0 enforces x10 was 0 at halt. // Non-zero exit code → bus imbalance → proof failure. { @@ -1425,7 +1425,7 @@ fn collect_halt_ops(register_state: &mut RegisterState) -> Vec { } // x255 (PC) is finalized via the inline-PC `memory` bus + REGISTER table, not - // via a MEMW write at 2^64-1. See `collect_halt_ops` doc and the PC finalization + // via a MEMW write at 2^32-1. See `collect_halt_ops` doc and the PC finalization // in the caller. ops @@ -3055,7 +3055,7 @@ fn collect_all_ops( register_state: &mut RegisterState, is_final: bool, ) -> CollectedOps { - // HALT finalization: 33 register MEMW operations at timestamp u64::MAX. + // HALT finalization: 33 register MEMW operations at timestamp 2^32-1. // Must come before Phase 3 (LT from MEMW) so HALT ops get timestamp checks. // Only the final epoch terminates; intermediate epochs keep their boundary // register state (no zeroizing) so it can seed the next epoch. @@ -3419,8 +3419,10 @@ fn build_traces( // pc=1 and chain the inline-PC `memory` tokens with a +4 timestamp cadence // starting from the HALT chip's emit_pc at `halt_timestamp + 1`; the last // padding write therefore lands at `halt_timestamp + 4*num_padding_rows + 1` - // (= `halt_timestamp + 1` when there is no padding). The REGISTER final token - // must match that last write to balance the memory argument. + // (= `halt_timestamp + 1` when there is no padding), which is the + // verifier-known `cpu::final_pc_timestamp` REGISTER consumes x255 at. Only + // the value 1 reaches the bus (as FINI); REGISTER does not read the x255 + // rows' timestamp columns. register_state.write_pc(1, halt_op.timestamp + 4 * num_padding_rows as u64 + 1); (halt_op.timestamp, halt_op.next_pc) } else { @@ -4189,7 +4191,8 @@ impl Traces { /// `main_area` — for apples-to-apples comparison with other zkVMs. /// /// Preprocessed columns (committed in a separate PCS round during setup, not at - /// proving time) are excluded: BITWISE (11), DECODE (5), REGISTER (3), PAGE (2). + /// proving time) are excluded: BITWISE (11), DECODE (5), REGISTER (4), PAGE (2), + /// CPU (1, `TIMESTAMP`). pub fn total_field_elements(&self) -> u64 { use super::bitwise::NUM_PRECOMPUTED_COLS as BITWISE_PRECOMPUTED; use super::bitwise::cols::NUM_COLUMNS as BITWISE_COLS; @@ -4258,7 +4261,7 @@ impl Traces { let mut total: u64 = 0; for t in cpus { - total += (t.num_rows() * CPU_COLS) as u64; + total += (t.num_rows() * (CPU_COLS - super::cpu::NUM_PRECOMPUTED_COLS)) as u64; } total += (bitwise.num_rows() * (BITWISE_COLS - BITWISE_PRECOMPUTED)) as u64; for t in lts { @@ -4340,7 +4343,7 @@ impl Traces { n.div_ceil(2) } - let n_cpu = aux_cols(super::cpu::bus_interactions().len()); + let n_cpu = aux_cols(super::cpu::bus_interactions(0).len()); let n_bitwise = aux_cols(super::bitwise::bus_interactions().len()); let n_lt = aux_cols(super::lt::bus_interactions().len()); let n_shift = aux_cols(super::shift::bus_interactions().len()); @@ -4353,7 +4356,7 @@ impl Traces { let n_branch = aux_cols(super::branch::bus_interactions().len()); let n_halt = aux_cols(super::halt::bus_interactions().len()); let n_commit = aux_cols(super::commit::bus_interactions().len()); - let n_register = aux_cols(super::register::bus_interactions().len()); + let n_register = aux_cols(super::register::bus_interactions(0).len()); // page::bus_interactions count is constant regardless of page_base. let n_page = aux_cols(super::page::bus_interactions(0).len()); let n_memw_r = aux_cols(super::memw_register::bus_interactions().len()); @@ -4813,6 +4816,21 @@ impl Traces { #[cfg(feature = "instruments")] drop(__sp); + Ok(Self::collect_epoch_from_cpu_ops( + cpu_ops, + initial_image, + register_init, + is_final, + )) + } + + /// Phase 2 of [`Self::collect_epoch`], over already-built CPU operations. + fn collect_epoch_from_cpu_ops( + cpu_ops: Vec, + initial_image: &I, + register_init: &[u32], + is_final: bool, + ) -> CollectedEpoch { // Phase 2: Collect + route all ops let mut memory_state = MemoryState::from_image(initial_image); let mut register_state = RegisterState::from_init(register_init); @@ -4855,11 +4873,39 @@ impl Traces { #[cfg(feature = "instruments")] drop(__sp); - Ok(CollectedEpoch { + CollectedEpoch { ops, memory_state, register_state, - }) + } + } + + /// Monolithic traces built from caller-supplied CPU operations, in the given + /// row order and with their own timestamps. Lets soundness tests feed the + /// trace builder a run no honest prover would produce. + #[cfg(test)] + pub(crate) fn from_elf_and_cpu_ops( + elf: &Elf, + cpu_ops: Vec, + max_rows: &super::MaxRowsConfig, + ) -> Result { + let initial_image = build_initial_image(elf, &[]); + let register_init = register::register_init_from_entry_point(elf.entry_point); + let artifacts = DecodeArtifacts::from_elf(elf)?; + let collected = + Self::collect_epoch_from_cpu_ops(cpu_ops, &initial_image, ®ister_init, true); + Self::build_from_collected( + &artifacts, + collected, + Some(&initial_image), + ®ister_init, + max_rows, + &[], + true, + false, + #[cfg(feature = "disk-spill")] + StorageMode::Ram, + ) } /// The epoch-local half of an epoch's trace build: table generation diff --git a/prover/src/test_utils.rs b/prover/src/test_utils.rs index 58895f94b..74eac50da 100644 --- a/prover/src/test_utils.rs +++ b/prover/src/test_utils.rs @@ -681,10 +681,34 @@ fn build_air + Clone + Send + Sync + 'static>( step_size: usize, constraint_set: CS, name: &str, +) -> AirWithBuses { + build_air_maybe_cached( + num_columns, + interactions, + proof_options, + step_size, + constraint_set, + name, + true, + ) +} + +/// [`build_air`], bypassing [`air_prototype_cache`] when `cache` is false. For +/// AIRs whose name embeds a value derived from proof-declared heights, so a +/// verifier fed many proofs cannot grow the never-evicted cache with one entry +/// per distinct value. +fn build_air_maybe_cached + Clone + Send + Sync + 'static>( + num_columns: usize, + interactions: Vec, + proof_options: &ProofOptions, + step_size: usize, + constraint_set: CS, + name: &str, + cache: bool, ) -> AirWithBuses { type Proto = AirWithBuses; let key = air_proto_key(name, proof_options); - { + if cache { let cache = air_prototype_cache().lock().unwrap(); if let Some(proto) = cache.get(&key).and_then(|p| p.downcast_ref::>()) { return proto.clone(); @@ -704,22 +728,32 @@ fn build_air + Clone + Send + Sync + 'static>( // calls `constraint_program()`. #[cfg(not(target_arch = "riscv64"))] let _ = air.constraint_program(); - air_prototype_cache() - .lock() - .unwrap() - .insert(key, Box::new(air.clone())); + if cache { + air_prototype_cache() + .lock() + .unwrap() + .insert(key, Box::new(air.clone())); + } air } -/// Create CPU AIR with all constraints and bus interactions. -pub fn create_cpu_air(proof_options: &ProofOptions) -> ConcreteVmAir { - build_air( +/// Create CPU AIR with all constraints and bus interactions, for a CPU table +/// whose timestamps start at `ts_base` (see [`crate::tables::cpu::timestamp_bases`]). +/// Not preprocessed: callers add the `TIMESTAMP` commitment with `with_preprocessed`. +/// +/// Only the bases an honest prover produces (multiples of a full table, +/// `4·max_rows::CPU`, at most 2^11 of them) are cached; any other base is built +/// fresh, so proof-declared heights cannot grow the prototype cache. +pub fn create_cpu_air(proof_options: &ProofOptions, ts_base: u64) -> ConcreteVmAir { + let full_table = crate::tables::cpu::TIMESTAMP_STRIDE * crate::tables::max_rows::CPU as u64; + build_air_maybe_cached( cpu_cols::NUM_COLUMNS, - cpu_bus_interactions(), + cpu_bus_interactions(ts_base), proof_options, 1, CpuConstraints, - "CPU", + &format!("CPU@{ts_base}"), + ts_base.is_multiple_of(full_table), ) } @@ -977,18 +1011,26 @@ pub fn create_page_air( ) } -/// Create REGISTER AIR with bus interactions. +/// Create REGISTER AIR with bus interactions; the final PC token is consumed at +/// `final_pc_ts` (see [`crate::tables::cpu::final_pc_timestamp`]). /// /// The REGISTER table provides initial and final tokens for register accesses /// on the Memory bus (is_register=1). -pub fn create_register_air(proof_options: &ProofOptions) -> ConcreteVmAir { - build_air( +/// +/// Never cached: `final_pc_ts` changes with every proof's CPU row count, and the +/// table is small enough to build per proof. +pub fn create_register_air( + proof_options: &ProofOptions, + final_pc_ts: u64, +) -> ConcreteVmAir { + build_air_maybe_cached( register_cols::NUM_COLUMNS, - register_bus_interactions(), + register_bus_interactions(final_pc_ts), proof_options, 1, EmptyConstraints, - "REGISTER", + &format!("REGISTER@{final_pc_ts}"), + false, ) } diff --git a/prover/src/tests/auto_storage_tests.rs b/prover/src/tests/auto_storage_tests.rs index e26674d27..0049f367f 100644 --- a/prover/src/tests/auto_storage_tests.rs +++ b/prover/src/tests/auto_storage_tests.rs @@ -33,7 +33,7 @@ fn peak_bytes_per_table_increment_is_exact() { let bumped = peak_bytes(&lengths, blowup, ALL_TABLES); let cpu_main = CPU_COLS as u64; - let cpu_aux = cpu_buses().len().div_ceil(2) as u64; + let cpu_aux = cpu_buses(0).len().div_ceil(2) as u64; let per_row_persistent = cpu_main * GOLDILOCKS_BYTES * (1 + b) + cpu_aux * CUBIC_EXT_BYTES * (1 + b) + 2 * b * KECCAK_NODE_BYTES // main Merkle (1 tree) diff --git a/prover/src/tests/constraint_program_device_tests.rs b/prover/src/tests/constraint_program_device_tests.rs index a29a7cb49..784b77cfc 100644 --- a/prover/src/tests/constraint_program_device_tests.rs +++ b/prover/src/tests/constraint_program_device_tests.rs @@ -156,7 +156,7 @@ fn check_air_device( fn all_table_programs_lower_and_match_folders() { let opts = GoldilocksCubicProofOptions::with_blowup(2).expect("blowup=2 valid"); - check_air_device(&create_cpu_air(&opts), "CPU"); + check_air_device(&create_cpu_air(&opts, 0), "CPU"); check_air_device(&create_bitwise_air(&opts), "BITWISE"); check_air_device(&create_lt_air(&opts), "LT"); check_air_device(&create_shift_air(&opts), "SHIFT"); @@ -175,7 +175,7 @@ fn all_table_programs_lower_and_match_folders() { check_air_device(&create_halt_air(&opts), "HALT"); check_air_device(&create_commit_air(&opts), "COMMIT"); check_air_device(&create_page_air(&opts, 0x1000), "PAGE"); - check_air_device(&create_register_air(&opts), "REGISTER"); + check_air_device(&create_register_air(&opts, 0), "REGISTER"); check_air_device(&create_keccak_air(&opts), "KECCAK"); check_air_device(&create_keccak_rnd_air(&opts), "KECCAK_RND"); check_air_device(&create_keccak_rc_air(&opts), "KECCAK_RC"); diff --git a/prover/src/tests/constraint_program_tests.rs b/prover/src/tests/constraint_program_tests.rs index e227da53d..8ef864719 100644 --- a/prover/src/tests/constraint_program_tests.rs +++ b/prover/src/tests/constraint_program_tests.rs @@ -154,7 +154,7 @@ fn check_air(air: &dyn AIR fn all_table_programs_match_folders() { let opts = GoldilocksCubicProofOptions::with_blowup(2).expect("blowup=2 valid"); - check_air(&create_cpu_air(&opts), "CPU"); + check_air(&create_cpu_air(&opts, 0), "CPU"); check_air(&create_bitwise_air(&opts), "BITWISE"); check_air(&create_lt_air(&opts), "LT"); check_air(&create_shift_air(&opts), "SHIFT"); @@ -173,7 +173,7 @@ fn all_table_programs_match_folders() { check_air(&create_halt_air(&opts), "HALT"); check_air(&create_commit_air(&opts), "COMMIT"); check_air(&create_page_air(&opts, 0x1000), "PAGE"); - check_air(&create_register_air(&opts), "REGISTER"); + check_air(&create_register_air(&opts, 0), "REGISTER"); check_air(&create_keccak_air(&opts), "KECCAK"); check_air(&create_keccak_rnd_air(&opts), "KECCAK_RND"); check_air(&create_keccak_rc_air(&opts), "KECCAK_RC"); diff --git a/prover/src/tests/constraints_tests.rs b/prover/src/tests/constraints_tests.rs index 0caf71264..f79d83506 100644 --- a/prover/src/tests/constraints_tests.rs +++ b/prover/src/tests/constraints_tests.rs @@ -459,8 +459,8 @@ use stark::constraints::builder::{ConstraintSet, num_base_from_meta}; #[test] fn test_cpu_bit_flag_columns_count() { - // 10 top-level flags + pc_double_read + prev_pc_timestamp_borrow + non_padding. - assert_eq!(BIT_FLAG_COLUMNS.len(), 12); + // 10 top-level flags + pc_double_read. + assert_eq!(BIT_FLAG_COLUMNS.len(), 11); } #[test] diff --git a/prover/src/tests/cpu_tests.rs b/prover/src/tests/cpu_tests.rs index 3381d1821..85e19369d 100644 --- a/prover/src/tests/cpu_tests.rs +++ b/prover/src/tests/cpu_tests.rs @@ -2,9 +2,14 @@ //! //! Unit tests for the reworked `CpuOperation::from_log` (arg2 multiplex, res, //! rvd, branch decision, word-instruction delegation), `generate_cpu_trace` -//! (column layout, padding, word-row masking), and `collect_bitwise_ops`. +//! (column layout, padding, word-row masking), `collect_bitwise_ops`, and the +//! preprocessed timestamp layout (`timestamp_bases`, `validate_heights`). -use crate::tables::cpu::{CPU_PADDING_PC, CpuOperation, cols, generate_cpu_trace}; +use crate::tables::cpu::{ + CPU_PADDING_PC, CpuOperation, MAX_CPU_ROWS, cols, final_pc_timestamp, generate_cpu_trace, + table_heights, timestamp_bases, validate_heights, +}; +use crate::tables::max_rows; use crate::tables::types::DecodeEntry; use executor::vm::{ @@ -245,7 +250,7 @@ fn test_trace_width_and_real_row() { }); let trace = generate_cpu_trace(&ops); assert_eq!(trace.main_table.width, cols::NUM_COLUMNS); - assert_eq!(cols::NUM_COLUMNS, 38); + assert_eq!(cols::NUM_COLUMNS, 37); assert_eq!(trace.main_table.height, 4); let row = trace.main_table.get_row(0); assert_eq!(row[cols::PC_0], (PC).into()); @@ -362,3 +367,93 @@ fn test_collect_bitwise_ops_word_row_zeroed() { assert_eq!(ops[1].x, 0, "rd zeroed"); assert_eq!(ops[1].y, 2, "half_instruction_length retained"); } + +// ========================================================================= +// Preprocessed timestamp +// ========================================================================= + +/// TIMESTAMP is the preprocessed `4·(row + 1)` on real and padding rows, +/// whatever timestamp the operations carry (a chunk's ops carry `base + 4·(row + 1)`). +#[test] +fn test_trace_timestamp_is_preprocessed_column() { + let mut ops = ops4(Instruction::Arith { + dst: 3, + src1: 1, + src2: 2, + op: ArithOp::Add, + }); + ops.truncate(3); + for (i, op) in ops.iter_mut().enumerate() { + op.timestamp = 1000 + 7 * i as u64; + } + let trace = generate_cpu_trace(&ops); + assert_eq!(trace.main_table.height, 4); + for row in 0..4 { + assert_eq!( + *trace.main_table.get(row, cols::TIMESTAMP), + (4 * (row as u64 + 1)).into(), + "row {row}" + ); + } +} + +#[test] +fn test_timestamp_bases_are_cumulative_heights() { + assert_eq!(timestamp_bases(&[]), Vec::::new()); + assert_eq!(timestamp_bases(&[8]), vec![0]); + assert_eq!(timestamp_bases(&[32, 32, 8]), vec![0, 128, 256]); + // Consecutive tables continue the cadence: the last row of table k is at + // base_k + 4·h_k, the first row of table k+1 at base_{k+1} + 4 = that + 4. + let heights = [16, 4]; + let bases = timestamp_bases(&heights); + assert_eq!(bases[0] + 4 * heights[0] as u64 + 4, bases[1] + 4); +} + +#[test] +fn test_final_pc_timestamp_follows_last_row() { + assert_eq!(final_pc_timestamp(4), 17); + assert_eq!(final_pc_timestamp(MAX_CPU_ROWS), (1 << 32) - 3); +} + +#[test] +fn test_validate_heights_accepts_honest_layouts() { + assert!(validate_heights(&[4]).is_ok()); + assert!(validate_heights(&[max_rows::CPU, max_rows::CPU, 64]).is_ok()); + // Largest layout under the bound: (2^11 - 1) full tables + one of 2^18 rows. + let mut heights = vec![max_rows::CPU; (1 << 11) - 1]; + heights.push(max_rows::CPU / 2); + assert!(validate_heights(&heights).is_ok()); +} + +#[test] +fn test_validate_heights_rejects_bad_heights() { + for bad in [0, 1, 2, 3, 12, max_rows::CPU * 2] { + assert!(validate_heights(&[bad]).is_err(), "height {bad}"); + } + assert!(validate_heights(&[max_rows::CPU, 6]).is_err()); +} + +/// `2^30` rows would put the last row at `4·2^30 = 2^32`, outside a `Word` +/// and past HALT's `2^32 - 1`. +#[test] +fn test_validate_heights_rejects_epoch_over_row_bound() { + let heights = vec![max_rows::CPU; 1 << 11]; + assert_eq!(heights.iter().sum::() as u64, MAX_CPU_ROWS + 1); + assert!(validate_heights(&heights).is_err()); +} + +/// `table_heights` mirrors the trace builder's chunking: full chunks, then the +/// remainder padded to a power of two, at least 4. +#[test] +fn test_table_heights_matches_chunking() { + assert_eq!(table_heights(0, 32), Vec::::new()); + assert_eq!(table_heights(1, 32), vec![4]); + assert_eq!(table_heights(5, 32), vec![8]); + assert_eq!(table_heights(32, 32), vec![32]); + assert_eq!(table_heights(33, 32), vec![32, 4]); + assert_eq!(table_heights(70, 32), vec![32, 32, 8]); + // One cycle over the bound: exactly 2^11 full tables of 2^19 rows. + let rows = 1usize << 30; + assert!(validate_heights(&table_heights(rows, max_rows::CPU)).is_err()); + assert!(validate_heights(&table_heights(rows - (1 << 18), max_rows::CPU)).is_ok()); +} diff --git a/prover/src/tests/cpu_timestamp_tests.rs b/prover/src/tests/cpu_timestamp_tests.rs new file mode 100644 index 000000000..6fea0fb79 --- /dev/null +++ b/prover/src/tests/cpu_timestamp_tests.rs @@ -0,0 +1,209 @@ +//! End-to-end tests of the preprocessed CPU timestamp across several CPU tables. +//! +//! Every CPU table commits the same preprocessed column `4·(i + 1)` and adds +//! `4·S_k` (the total height of the tables before it) to the timestamps it +//! sends. These tests split one run over several CPU tables and check that an +//! honest proof verifies, and that a prover cannot move a CPU table to another +//! position: two full tables have the same preprocessed commitment, so only the +//! per-table base tells them apart. Without it the buses are permutation +//! invariant and the reordered tables would balance. They also check that the +//! verifier reads the CPU heights from the right sub-proofs and rejects hostile +//! ones cleanly. + +use crypto::fiat_shamir::default_transcript::DefaultTranscript; +use executor::elf::Elf; +use stark::prover::{IsStarkProver, Prover}; + +use super::halt_pc_forgery_poc::{opts, run_logs}; +use crate::statement::{StatementKind, absorb_statement}; +use crate::tables::MaxRowsConfig; +use crate::tables::trace_builder::Traces; +use crate::test_utils::{E, asm_elf_bytes}; +use crate::{VmAirs, VmProof}; + +const GUEST: &str = "all_instructions_64"; + +/// Prove `elf` split over 32-row CPU tables, after `tamper` edits the traces. +fn craft_proof( + elf_bytes: &[u8], + tamper: impl FnOnce(&mut Traces), +) -> Result { + let options = opts(); + let program = Elf::load(elf_bytes).expect("ELF load"); + let mut traces = Traces::from_elf_and_logs( + &program, + &run_logs(elf_bytes), + &MaxRowsConfig::small(), + &[], + #[cfg(feature = "disk-spill")] + stark::storage_mode::StorageMode::Ram, + ) + .expect("trace build"); + tamper(&mut traces); + + let table_counts = traces.table_counts(); + let airs = VmAirs::new( + &program, + &options, + false, + &traces.page_configs, + &table_counts, + &crate::cpu_heights_from_traces(&traces), + None, + true, + None, + crate::test_utils::halted_register_commitment( + &options, + &program, + &traces.public_output_bytes, + ), + ); + let runtime_page_ranges = traces.runtime_page_ranges(); + + let mut transcript = DefaultTranscript::::new(&[]); + absorb_statement( + &mut transcript, + StatementKind::Monolithic, + elf_bytes, + &traces.public_output_bytes, + &table_counts, + 0, + &runtime_page_ranges, + options.fri_final_poly_log_degree, + ); + let proof = Prover::multi_prove( + airs.air_trace_pairs(&mut traces), + &mut transcript, + #[cfg(feature = "disk-spill")] + stark::storage_mode::StorageMode::Ram, + )?; + + Ok(VmProof { + proof, + runtime_page_ranges, + table_counts, + public_output: traces.public_output_bytes.clone(), + num_private_input_pages: 0, + }) +} + +fn verifies(crafted: Result, elf: &[u8]) -> bool { + let proof = crafted.expect("the crafted proof must build"); + crate::verify_with_options(&proof, elf, &opts(), None, None).expect("verifier must not error") +} + +/// POSITIVE CONTROL: a run split over several CPU tables verifies, the later +/// tables continuing the first one's timestamp cadence. +#[test] +fn split_cpu_tables_verify() { + let elf = asm_elf_bytes(GUEST); + let rows = run_logs(&elf).len(); + let mut full_tables = 0; + let crafted = craft_proof(&elf, |traces| { + full_tables = traces + .cpus + .iter() + .filter(|t| t.num_rows() == MaxRowsConfig::small().cpu) + .count(); + // The heights the prover checks right after execution are the ones the + // trace builder produces. + assert_eq!( + crate::tables::cpu::table_heights(rows, MaxRowsConfig::small().cpu), + crate::cpu_heights_from_traces(traces) + ); + }); + assert!( + full_tables >= 2, + "need two full CPU tables, got {full_tables}" + ); + assert!(verifies(crafted, &elf)); +} + +/// Two full CPU tables swapped: same preprocessed commitments, same heights, +/// same rows — only their timestamp bases differ. +#[test] +fn swapped_cpu_tables_are_rejected() { + let elf = asm_elf_bytes(GUEST); + let crafted = craft_proof(&elf, |traces| traces.cpus.swap(0, 1)); + assert!( + !verifies(crafted, &elf), + "CPU tables verified at each other's timestamp base" + ); +} + +/// Hostile CPU heights in an honest proof: heights `validate_heights` refuses are +/// an error before any AIR is built; a valid but wrong height picks a different +/// preprocessed root and the proof is rejected. None of them panics. +#[test] +fn hostile_cpu_heights_are_rejected_by_the_verifier() { + let elf = asm_elf_bytes(GUEST); + let honest = craft_proof(&elf, |_| {}).expect("honest proof"); + assert!(crate::verify_with_options(&honest, &elf, &opts(), None, None).unwrap()); + let cpu = crate::cpu_proof_start(true, &honest.table_counts); + assert_eq!( + honest.proof.proofs[cpu].trace_length, + MaxRowsConfig::small().cpu + ); + + let with_height = |height: usize| { + let mut proof = honest.clone(); + proof.proof.proofs[cpu].trace_length = height; + crate::verify_with_options(&proof, &elf, &opts(), None, None) + }; + for height in [0, 2, 3, 6, crate::tables::max_rows::CPU * 2, usize::MAX] { + assert!( + matches!( + with_height(height), + Err(crate::Error::InvalidTableCounts(_)) + ), + "height {height}" + ); + } + for height in [16, 64] { + assert!(!with_height(height).unwrap(), "height {height}"); + } +} + +/// `cpu_proof_start` (which the verifier reads CPU heights with) matches the +/// `air_refs` layout for every HALT / accelerator combination. Checked in +/// release builds too, unlike the `debug_assert` in `air_refs`. +#[test] +fn cpu_proof_start_matches_air_refs_layout() { + let elf = asm_elf_bytes(GUEST); + let program = Elf::load(&elf).unwrap(); + let options = opts(); + let honest = craft_proof(&elf, |_| {}).expect("honest proof"); + for include_halt in [false, true] { + for mask in 0u8..64 { + let mut counts = honest.table_counts.clone(); + let bit = |i: u8| usize::from(mask >> i & 1); + counts.commit = bit(0); + counts.keccak = bit(1); + counts.keccak_rnd = bit(2); + counts.ecsm = bit(3); + counts.ecdas = bit(4); + counts.hint = bit(5); + let airs = VmAirs::new( + &program, + &options, + false, + &[], + &counts, + &vec![4; counts.cpu], + None, + include_halt, + None, + [0u8; 32], + ); + let refs = airs.air_refs(); + let start = crate::cpu_proof_start(include_halt, &counts); + for k in 0..counts.cpu { + assert_eq!( + refs[start + k].name(), + format!("CPU[{k}]"), + "halt={include_halt} accelerators={mask:06b}" + ); + } + } + } +} diff --git a/prover/src/tests/halt_pc_forgery_poc.rs b/prover/src/tests/halt_pc_forgery_poc.rs index 4e2caf984..15b4f603f 100644 --- a/prover/src/tests/halt_pc_forgery_poc.rs +++ b/prover/src/tests/halt_pc_forgery_poc.rs @@ -5,7 +5,7 @@ //! anything, so a prover can set them to `(1, 0)`: HALT then consumes the `1` it //! emits itself, and the real `next_pc` token is left for another CPU row to pick //! up. The trace keeps executing after `exit` and HALT's x10 == 0 check reads x10 -//! at `ts = 2^64 - 1`, not at the exit call. +//! at `ts = 2^32 - 1`, not at the exit call. //! //! The guest calls `exit(1)`, which no honest prover can prove. The forgery runs //! `li a0, 0` (+ nops) after the exit and must not verify against the same ELF. @@ -94,8 +94,12 @@ pub(crate) fn forged_logs(honest: &[u8], rows: usize) -> Vec { pub(crate) struct Tamper { /// HALT `PC = (1, 0)`, so HALT's consume/emit cancel. pub(crate) halt_pc: bool, - /// Move the REGISTER final x255 token to the last post-exit row's write - /// timestamp. Main-trace columns. + /// Move the REGISTER final x255 timestamp to the last post-exit row's write + /// timestamp. Main-trace columns. Needed before the CPU timestamp was + /// preprocessed; REGISTER now consumes x255 at the verifier-known + /// `final_pc_ts` and never reads these cells on the x255 rows, so this tamper + /// changes nothing. The attack still lines up: with [`FORGED_ROWS`] rows the + /// forged chain ends at `final_pc_ts = 4·16 + 1`. pub(crate) register_ts: bool, /// Set the REGISTER final x255 value to the last post-exit `next_pc`. A /// main-trace column on `main`; preprocessed by the fix, so the forged root no @@ -165,6 +169,7 @@ fn craft_proof( false, &traces.page_configs, &table_counts, + &crate::cpu_heights_from_traces(&traces), None, true, None, diff --git a/prover/src/tests/ir_stats_dump.rs b/prover/src/tests/ir_stats_dump.rs index a269127d9..ac7c930b5 100644 --- a/prover/src/tests/ir_stats_dump.rs +++ b/prover/src/tests/ir_stats_dump.rs @@ -105,7 +105,7 @@ fn stats(air: &dyn AIR, la fn dump_ir_stats() { let opts = GoldilocksCubicProofOptions::with_blowup(2).expect("blowup=2 valid"); - stats(&create_cpu_air(&opts), "CPU"); + stats(&create_cpu_air(&opts, 0), "CPU"); stats(&create_bitwise_air(&opts), "BITWISE"); stats(&create_lt_air(&opts), "LT"); stats(&create_shift_air(&opts), "SHIFT"); @@ -124,7 +124,7 @@ fn dump_ir_stats() { stats(&create_halt_air(&opts), "HALT"); stats(&create_commit_air(&opts), "COMMIT"); stats(&create_page_air(&opts, 0x1000), "PAGE"); - stats(&create_register_air(&opts), "REGISTER"); + stats(&create_register_air(&opts, 0), "REGISTER"); stats(&create_keccak_air(&opts), "KECCAK"); stats(&create_keccak_rnd_air(&opts), "KECCAK_RND"); stats(&create_keccak_rc_air(&opts), "KECCAK_RC"); diff --git a/prover/src/tests/mod.rs b/prover/src/tests/mod.rs index 6ec729635..116cd0c96 100644 --- a/prover/src/tests/mod.rs +++ b/prover/src/tests/mod.rs @@ -33,6 +33,8 @@ pub mod cpu32_tests; #[cfg(test)] pub mod cpu_tests; #[cfg(test)] +pub mod cpu_timestamp_tests; +#[cfg(test)] pub mod decode_layout_tests; #[cfg(test)] pub mod decode_tests; @@ -79,6 +81,8 @@ pub mod page_offset_forgery_poc; #[cfg(test)] pub mod page_tests; #[cfg(test)] +pub mod pc_double_read_poc; +#[cfg(test)] pub mod prove_elfs_tests; #[cfg(test)] pub mod recursion_smoke_test; diff --git a/prover/src/tests/ood_window_ir_tests.rs b/prover/src/tests/ood_window_ir_tests.rs index 29d224627..9671d9621 100644 --- a/prover/src/tests/ood_window_ir_tests.rs +++ b/prover/src/tests/ood_window_ir_tests.rs @@ -89,7 +89,7 @@ fn assert_ood_window_matches_ir( fn all_table_windows_match_captured_ir() { let opts = GoldilocksCubicProofOptions::with_blowup(2).expect("blowup=2 valid"); - assert_ood_window_matches_ir(&create_cpu_air(&opts), true, "CPU"); + assert_ood_window_matches_ir(&create_cpu_air(&opts, 0), true, "CPU"); assert_ood_window_matches_ir(&create_bitwise_air(&opts), true, "BITWISE"); assert_ood_window_matches_ir(&create_lt_air(&opts), true, "LT"); assert_ood_window_matches_ir(&create_shift_air(&opts), true, "SHIFT"); @@ -108,7 +108,7 @@ fn all_table_windows_match_captured_ir() { assert_ood_window_matches_ir(&create_halt_air(&opts), true, "HALT"); assert_ood_window_matches_ir(&create_commit_air(&opts), true, "COMMIT"); assert_ood_window_matches_ir(&create_page_air(&opts, 0x1000), true, "PAGE"); - assert_ood_window_matches_ir(&create_register_air(&opts), true, "REGISTER"); + assert_ood_window_matches_ir(&create_register_air(&opts, 0), true, "REGISTER"); assert_ood_window_matches_ir(&create_keccak_air(&opts), true, "KECCAK"); assert_ood_window_matches_ir(&create_keccak_rnd_air(&opts), true, "KECCAK_RND"); assert_ood_window_matches_ir(&create_keccak_rc_air(&opts), true, "KECCAK_RC"); diff --git a/prover/src/tests/page_offset_forgery_poc.rs b/prover/src/tests/page_offset_forgery_poc.rs index 9993ceb7c..5da7d1955 100644 --- a/prover/src/tests/page_offset_forgery_poc.rs +++ b/prover/src/tests/page_offset_forgery_poc.rs @@ -177,6 +177,7 @@ fn craft_proof( false, &traces.page_configs, &table_counts, + &crate::cpu_heights_from_traces(&traces), None, true, None, @@ -692,6 +693,7 @@ fn craft_proof_with_duplicate_page( false, &traces.page_configs, &table_counts, + &crate::cpu_heights_from_traces(&traces), None, true, None, diff --git a/prover/src/tests/pc_double_read_poc.rs b/prover/src/tests/pc_double_read_poc.rs new file mode 100644 index 000000000..47844a389 --- /dev/null +++ b/prover/src/tests/pc_double_read_poc.rs @@ -0,0 +1,424 @@ +//! PoC: a free CPU `TIMESTAMP` lets `pc_double_read` reorder register accesses. +//! +//! Each CPU row reads the PC at `timestamp - 3 + 3 * pc_double_read` and writes +//! `next_pc` at `timestamp + 1`. `pc_double_read` is only bit-checked. With a +//! prover-chosen timestamp, row B can sit at `ts_B = ts_A + 1` with +//! `pc_double_read = 1`: its PC read lands on A's `next_pc` write directly, and +//! its `rs1` read at `ts_A + 1` sorts before A's `rd` write at `ts_A + 2`, so B +//! reads the register value from before A ran. +//! +//! The guest runs `li a0, 5; mv a1, a0; mv a0, a1; exit`, i.e. `exit(5)`, which +//! no honest prover can prove. The forgery has `mv a1, a0` read the stale +//! `a0 = 0` and proves `exit(0)`. The spec makes the timestamp a preprocessed +//! column (`4 * (i + 1)`), which leaves the prover no room for `ts_A + 1`. +//! +//! The forged run is shifted by −3 from B on, so two verifier pins reject it: +//! the TIMESTAMP column is not the preprocessed one, and the PC chain ends at +//! `4·N − 2` instead of the verifier-known `4·N + 1` REGISTER consumes x255 at. +//! The tests build the forgery against the pins the prover would choose (its own +//! TIMESTAMP root and final PC timestamp, as before the fix) and swap the honest +//! pins back one at a time, so each rejection has a single cause. +//! +//! Production proof options, as in `halt_pc_forgery_poc`. + +use crypto::fiat_shamir::default_transcript::DefaultTranscript; +use executor::elf::Elf; +use executor::vm::logs::Log; +use stark::config::Commitment; +use stark::proof::view::MultiProofView; +use stark::prover::{IsStarkProver, Prover}; +use stark::verifier::{IsStarkVerifier, Verifier}; + +use super::halt_pc_forgery_poc::{opts, run_logs}; +use crate::statement::{StatementKind, absorb_statement}; +use crate::tables::cpu::{self, CpuOperation, cols as cpu_cols}; +use crate::tables::trace_builder::Traces; +use crate::tables::types::VmTable; +use crate::tables::{decode, register}; +use crate::test_utils::{E, asm_elf_bytes, create_cpu_air, create_register_air}; +use crate::{MaxRowsConfig, VmAirs, VmProof}; + +const GUEST: &str = "poc_pc_double_read"; + +/// `li a0, 5` and `li a0, 0` (`addi a0, zero, imm`). +const LI_A0_5: [u8; 4] = [0x13, 0x05, 0x50, 0x00]; +const LI_A0_0: [u8; 4] = [0x13, 0x05, 0x00, 0x00]; + +/// Row A writes `a0`, row B (`mv a1, a0`) reads it, row C (`mv a0, a1`) copies it back. +const ROW_A: usize = 0; +const ROW_B: usize = 1; +const ROW_C: usize = 2; + +/// The guest with `li a0, 5` replaced by `li a0, 0`: honestly provable. +fn patched_elf(honest: &[u8]) -> Vec { + let at = honest + .windows(LI_A0_5.len()) + .position(|w| w == LI_A0_5) + .expect("li a0, 5 not found"); + let mut patched = honest.to_vec(); + patched[at..at + 4].copy_from_slice(&LI_A0_0); + patched +} + +/// CPU operations with the honest timestamps `4 * (i + 1)`, in program order. +fn honest_ops(program: &Elf, logs: &[Log]) -> Vec { + let instructions = decode::instructions_from_elf(program).expect("decode"); + logs.iter() + .enumerate() + .map(|(i, log)| { + CpuOperation::from_log_and_instruction( + log, + 4 * (i as u64 + 1), + instructions[&log.current_pc], + ) + }) + .collect() +} + +/// The forged run: B and C see the stale `a0 = 0`, B sits at `ts_A + 1` and every +/// later row moves down by 3 so the PC chain stays connected. B is listed before +/// A, so the trace builder's register walk serves B's read before A's write; row +/// order is otherwise irrelevant to the buses. +fn forged_ops(program: &Elf, logs: &[Log]) -> Vec { + let mut logs = logs.to_vec(); + assert_eq!(logs[ROW_B].src1_val, 5, "B honestly reads a0 = 5"); + for row in [ROW_B, ROW_C] { + logs[row].src1_val = 0; + logs[row].dst_val = 0; + } + let instructions = decode::instructions_from_elf(program).expect("decode"); + let mut ops: Vec = logs + .iter() + .enumerate() + .map(|(i, log)| { + let honest_ts = 4 * (i as u64 + 1); + let ts = if i == ROW_A { honest_ts } else { honest_ts - 3 }; + CpuOperation::from_log_and_instruction(log, ts, instructions[&log.current_pc]) + }) + .collect(); + ops.swap(ROW_A, ROW_B); + ops +} + +/// How the malicious prover deviates from the traces built from its ops. +#[derive(Clone, Copy, Default)] +struct Tamper { + /// `pc_double_read = 1` on B (CPU row 0 after the swap). + double_read: bool, + /// Overwrite every CPU `TIMESTAMP` cell with the trace the builder wrote before + /// the fix: the ops' own timestamps on the real rows, then padding continuing + /// the +4 cadence from the last real row. With `double_read` this is exactly the + /// CPU trace that verified on the base. + timestamp_column: bool, +} + +const FULL_ATTACK: Tamper = Tamper { + double_read: true, + timestamp_column: true, +}; + +/// What the CPU table's TIMESTAMP column and REGISTER's x255 final token are +/// pinned to. The verifier always uses [`Crafted::honest`]; the forgery is +/// committed against [`Crafted::forged`]. +#[derive(Clone, Copy)] +struct Pins { + timestamp_root: Commitment, + final_pc_ts: u64, +} + +/// A traced run, ready to be proven and verified against chosen pins. +struct Crafted { + elf_bytes: Vec, + program: Elf, + traces: Traces, + /// The verifier's pins: the preprocessed `4·(i + 1)` column and `4·N + 1`. + honest: Pins, + /// The pins the trace itself implies: the root of its TIMESTAMP column and the + /// timestamp its last row writes `next_pc` at. + forged: Pins, +} + +fn craft(elf_bytes: &[u8], ops: Vec, tamper: Tamper) -> Crafted { + let options = opts(); + let program = Elf::load(elf_bytes).expect("ELF load"); + let timestamps: Vec = ops.iter().map(|op| op.timestamp).collect(); + let mut traces = Traces::from_elf_and_cpu_ops(&program, ops, &MaxRowsConfig::default()) + .expect("trace build"); + assert_eq!(traces.cpus.len(), 1, "one CPU table"); + let cpu = &mut traces.cpus[0].main_table; + if tamper.double_read { + cpu.set_bool(0, cpu_cols::PC_DOUBLE_READ, true); + } + if tamper.timestamp_column { + let last_ts = *timestamps.last().expect("at least one row"); + let padding = (1..).map(|j| last_ts + 4 * j); + for (row, ts) in timestamps + .iter() + .copied() + .chain(padding) + .take(cpu.height) + .enumerate() + { + cpu.set_u64(row, cpu_cols::TIMESTAMP, ts); + } + } + let height = cpu.height; + let column: Vec<_> = (0..height) + .map(|row| *cpu.get(row, cpu_cols::TIMESTAMP)) + .collect(); + let last_ts = column.last().expect("non-empty table").to_raw(); + let honest = Pins { + timestamp_root: cpu::timestamp_commitment(&options, height), + final_pc_ts: cpu::final_pc_timestamp(height as u64), + }; + let forged = Pins { + timestamp_root: cpu::commit_timestamp_column(&options, &column), + final_pc_ts: last_ts + 1, + }; + let crafted = Crafted { + elf_bytes: elf_bytes.to_vec(), + program, + traces, + honest, + forged, + }; + // HALT zeroizes x1-x31 on every run here, forged or not, so the trace's FINI is + // the halted register file the production verifier pins. + assert_eq!( + crate::test_utils::trace_register_commitment( + &opts(), + ®ister::register_init_from_entry_point(crafted.program.entry_point), + &crafted.traces, + ), + crafted.register_commitment(), + "the run must end in the halted register file" + ); + crafted +} + +impl Crafted { + /// The production AIR set with the CPU TIMESTAMP root and the REGISTER final + /// PC timestamp replaced by `pins`. + fn airs(&self, pins: Pins) -> VmAirs { + let options = opts(); + let table_counts = self.traces.table_counts(); + let mut airs = VmAirs::new( + &self.program, + &options, + false, + &self.traces.page_configs, + &table_counts, + &crate::cpu_heights_from_traces(&self.traces), + None, + true, + None, + self.register_commitment(), + ); + airs.cpus[0] = Box::new( + create_cpu_air(&options, 0) + .with_name("CPU[0]") + .with_preprocessed(pins.timestamp_root, cpu::NUM_PRECOMPUTED_COLS), + ); + airs.register = Box::new( + create_register_air(&options, pins.final_pc_ts) + .with_preprocessed(self.register_commitment(), register::NUM_PREPROCESSED_COLS), + ); + airs + } + + /// As the production verifier: REGISTER FINI pinned to the halted register file. + fn register_commitment(&self) -> Commitment { + let committed_bytes = u32::try_from(self.traces.public_output_bytes.len()) + .expect("public output fits in u32"); + register::halted_commitment(&opts(), self.program.entry_point, committed_bytes) + } + + fn transcript(&self) -> DefaultTranscript { + let mut transcript = DefaultTranscript::::new(&[]); + absorb_statement( + &mut transcript, + StatementKind::Monolithic, + &self.elf_bytes, + &self.traces.public_output_bytes, + &self.traces.table_counts(), + 0, + &self.traces.runtime_page_ranges(), + opts().fri_final_poly_log_degree, + ); + transcript + } + + /// Prove against `pins`. The CPU TIMESTAMP root is whatever `pins` says, so + /// with `forged` pins the prover commits its own column consistently. + fn prove(mut self, pins: Pins) -> (Self, Result) { + let airs = self.airs(pins); + let mut transcript = self.transcript(); + let proof = Prover::multi_prove( + airs.air_trace_pairs(&mut self.traces), + &mut transcript, + #[cfg(feature = "disk-spill")] + stark::storage_mode::StorageMode::Ram, + ) + .map(|proof| VmProof { + proof, + runtime_page_ranges: self.traces.runtime_page_ranges(), + table_counts: self.traces.table_counts(), + public_output: self.traces.public_output_bytes.clone(), + num_private_input_pages: 0, + }); + (self, proof) + } + + /// Verify `proof` against `pins`, with every other check of the production + /// verifier. + fn verifies(&self, proof: &VmProof, pins: Pins) -> bool { + let airs = self.airs(pins); + let refs = airs.air_refs(); + let view = MultiProofView::Owned(&proof.proof); + let Some(expected) = crate::compute_expected_commit_bus_balance_view( + &refs, + view, + &proof.public_output, + 0, + &mut self.transcript(), + ) else { + return false; + }; + Verifier::multi_verify_views(&refs, view, &mut self.transcript(), &expected) + } +} + +/// The forgery, proven against the pins it implies (what a free TIMESTAMP and a +/// prover-chosen final PC timestamp allowed before the fix). +fn forged_proof(tamper: Tamper) -> (Crafted, VmProof) { + let elf = asm_elf_bytes(GUEST); + let program = Elf::load(&elf).unwrap(); + let crafted = craft(&elf, forged_ops(&program, &run_logs(&elf)), tamper); + let pins = crafted.forged; + let (crafted, proof) = crafted.prove(pins); + ( + crafted, + proof.expect("the forgery is consistent with its own pins"), + ) +} + +/// A verdict of the production verifier. A prover refusal counts as "not +/// accepted" only when it is the preprocessed TIMESTAMP root disagreeing with the +/// forged column (cold precomputed-tree cache; with a warm cache the honest tree is +/// substituted and the verifier rejects instead). +fn production_accepts( + proof: Result, + elf: &[u8], + tamper: Tamper, +) -> bool { + match proof { + Ok(proof) => crate::verify_with_options(&proof, elf, &opts(), None, None) + .expect("verifier must not error"), + Err(e) => { + assert!( + tamper.timestamp_column + && matches!( + e, + stark::prover::ProvingError::PrecomputedCommitmentMismatch + ), + "only the TIMESTAMP tamper may be refused, and only for its \ + preprocessed commitment: {e:?}" + ); + false + } + } +} + +/// POSITIVE CONTROL: the harness builds valid proofs from its own CPU ops. +#[test] +fn poc_control_patched_program_verifies() { + let patched = patched_elf(&asm_elf_bytes(GUEST)); + let program = Elf::load(&patched).unwrap(); + let crafted = craft( + &patched, + honest_ops(&program, &run_logs(&patched)), + Tamper::default(), + ); + let pins = crafted.honest; + let (_, proof) = crafted.prove(pins); + assert!(production_accepts(proof, &patched, Tamper::default())); +} + +/// NEGATIVE CONTROL: `exit(5)` honestly is rejected (x10 != 0 at HALT). +#[test] +fn poc_control_honest_exit_five_is_rejected() { + let elf = asm_elf_bytes(GUEST); + let program = Elf::load(&elf).unwrap(); + let crafted = craft( + &elf, + honest_ops(&program, &run_logs(&elf)), + Tamper::default(), + ); + let pins = crafted.honest; + let (_, proof) = crafted.prove(pins); + assert!(!production_accepts(proof, &elf, Tamper::default())); +} + +/// THE BUG, as it was before the fix: against the pins the prover chooses, the +/// forged `exit(0)` is a valid proof. Everything but the two pins is the +/// production verifier. +#[test] +fn poc_forgery_verifies_against_prover_chosen_pins() { + let (crafted, proof) = forged_proof(FULL_ATTACK); + assert_ne!(crafted.forged.timestamp_root, crafted.honest.timestamp_root); + assert_eq!(crafted.forged.final_pc_ts + 3, crafted.honest.final_pc_ts); + assert!(crafted.verifies(&proof, crafted.forged)); +} + +/// NEGATIVE CONTROL: the same forgery without `pc_double_read` is rejected even +/// against the prover-chosen pins — B reads the PC at `ts_A - 2`, where no token +/// was written. The double-read bit is the lever. +#[test] +fn poc_control_forgery_without_double_read_is_rejected() { + let (crafted, proof) = forged_proof(Tamper { + double_read: false, + ..FULL_ATTACK + }); + assert!(!crafted.verifies(&proof, crafted.forged)); +} + +/// The preprocessed TIMESTAMP alone rejects the forgery: only the CPU root is +/// switched back to the verifier's `4·(i + 1)`. +#[test] +fn preprocessed_timestamp_alone_rejects_the_forgery() { + let (crafted, proof) = forged_proof(FULL_ATTACK); + let pins = Pins { + timestamp_root: crafted.honest.timestamp_root, + ..crafted.forged + }; + assert!(!crafted.verifies(&proof, pins)); +} + +/// The final PC pin alone rejects the forgery: only REGISTER's x255 final token +/// is moved back to the verifier's `4·N + 1`. +#[test] +fn final_pc_pin_alone_rejects_the_forgery() { + let (crafted, proof) = forged_proof(FULL_ATTACK); + let pins = Pins { + final_pc_ts: crafted.honest.final_pc_ts, + ..crafted.forged + }; + assert!(!crafted.verifies(&proof, pins)); +} + +/// THE BUG through the production prover and verifier: the exact CPU trace that +/// verified on the base is rejected (the prover refuses its TIMESTAMP column, or +/// the verifier rejects the proof). +#[test] +fn stale_register_read_via_pc_double_read_is_rejected() { + let elf = asm_elf_bytes(GUEST); + let program = Elf::load(&elf).unwrap(); + let crafted = craft(&elf, forged_ops(&program, &run_logs(&elf)), FULL_ATTACK); + let pins = crafted.honest; + let (_, proof) = crafted.prove(pins); + assert!( + !production_accepts(proof, &elf, FULL_ATTACK), + "SOUNDNESS BUG: a row with pc_double_read = 1 one timestamp after the \ + previous row read a register before that row wrote it (exit(5) -> exit(0))" + ); +} diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index f2a2c5476..82527f9b2 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -119,6 +119,7 @@ pub(crate) fn weigh_the_bus( true, &traces.page_configs, &table_counts, + &crate::cpu_heights_from_traces(traces), None, true, None, @@ -210,6 +211,7 @@ fn prove_vm_minimal(elf_bytes: &[u8], private_inputs: &[u8], max_rows: &MaxRowsC true, &traces.page_configs, &table_counts, + &crate::cpu_heights_from_traces(&traces), None, true, None, @@ -258,6 +260,12 @@ fn verify_vm_minimal(vm_proof: &VmProof, elf_bytes: &[u8]) -> bool { true, &page_configs, &vm_proof.table_counts, + &crate::cpu_heights_from_proofs( + stark::proof::view::MultiProofView::Owned(&vm_proof.proof), + &vm_proof.table_counts, + true, + ) + .unwrap(), None, true, None, @@ -1795,6 +1803,7 @@ fn test_prove_elfs_test_commit_4_wrong_pages_rejected() { true, &traces.page_configs, &table_counts, + &crate::cpu_heights_from_traces(&traces), None, true, None, @@ -1819,6 +1828,7 @@ fn test_prove_elfs_test_commit_4_wrong_pages_rejected() { true, &wrong_configs, &table_counts, + &crate::cpu_heights_from_traces(&traces), None, true, None, @@ -2558,6 +2568,7 @@ fn test_deep_stack_runtime_pages_roundtrip() { true, &traces.page_configs, &table_counts, + &crate::cpu_heights_from_traces(&traces), None, true, None, @@ -2582,6 +2593,7 @@ fn test_deep_stack_runtime_pages_roundtrip() { true, &verifier_configs, &table_counts, + &crate::cpu_heights_from_traces(&traces), None, true, None, @@ -2641,6 +2653,7 @@ fn test_deep_stack_missing_pages_rejected() { true, &traces.page_configs, &table_counts, + &crate::cpu_heights_from_traces(&traces), None, true, None, @@ -2664,6 +2677,7 @@ fn test_deep_stack_missing_pages_rejected() { true, &wrong_configs, &table_counts, + &crate::cpu_heights_from_traces(&traces), None, true, None, @@ -2758,6 +2772,7 @@ fn test_heap_alloc_runtime_pages_roundtrip() { true, &traces.page_configs, &table_counts, + &crate::cpu_heights_from_traces(&traces), None, true, None, @@ -2782,6 +2797,7 @@ fn test_heap_alloc_runtime_pages_roundtrip() { true, &verifier_configs, &table_counts, + &crate::cpu_heights_from_traces(&traces), None, true, None, @@ -2978,6 +2994,7 @@ fn test_crafted_zero_count_proof_must_not_verify() { true, &[], &zero_counts, + &[], None, true, None, @@ -3460,6 +3477,7 @@ fn test_prove_first_epoch_without_halt() { true, &traces.page_configs, &table_counts, + &crate::cpu_heights_from_traces(&traces), None, false, None, @@ -3548,6 +3566,7 @@ fn test_prove_second_epoch_from_snapshot() { true, &traces.page_configs, &table_counts, + &crate::cpu_heights_from_traces(&traces), None, false, None, @@ -3643,6 +3662,7 @@ fn test_epoch_proof_commits_l2g() { true, &traces.page_configs, &table_counts, + &crate::cpu_heights_from_traces(&traces), None, false, None, @@ -3800,6 +3820,7 @@ fn test_continuation_pipeline_end_to_end() { true, &traces.page_configs, &table_counts, + &crate::cpu_heights_from_traces(&traces), None, is_final, None, @@ -3940,6 +3961,7 @@ fn test_epoch_memory_bus_with_l2g_bookend() { true, &traces.page_configs, &table_counts, + &crate::cpu_heights_from_traces(&traces), None, false, None, diff --git a/prover/src/tests/recursion_soundness_gap_poc.rs b/prover/src/tests/recursion_soundness_gap_poc.rs index d91af5044..d2fb38e87 100644 --- a/prover/src/tests/recursion_soundness_gap_poc.rs +++ b/prover/src/tests/recursion_soundness_gap_poc.rs @@ -153,6 +153,7 @@ fn custom_prove_with_statement_elf( false, &traces.page_configs, &table_counts, + &crate::cpu_heights_from_traces(&traces), None, true, None, diff --git a/prover/src/tests/register_tests.rs b/prover/src/tests/register_tests.rs index df4445a89..2c4d02e51 100644 --- a/prover/src/tests/register_tests.rs +++ b/prover/src/tests/register_tests.rs @@ -82,8 +82,8 @@ fn test_generate_register_trace_with_access() { #[test] fn test_bus_interactions() { - let interactions = bus_interactions(); - assert_eq!(interactions.len(), 2); // C1, C2 + let interactions = bus_interactions(0); + assert_eq!(interactions.len(), 3); // C1, C2 (PC), C2 } #[test] @@ -170,3 +170,50 @@ fn fini_from_final_state_matches_trace() { fini_from_trace(&trace) ); } + +/// IS_PC (preprocessed) marks exactly the two x255 rows. +#[test] +fn test_is_pc_marks_only_the_pc_rows() { + let trace = generate_register_trace( + &FinalRegisterStateMap::new(), + ®ister_init_from_entry_point(0x1000), + ); + for row in 0..trace.num_rows() { + let offset = trace.main_table.get(row, cols::OFFSET).to_raw(); + let is_pc = row < NUM_REGISTER_ADDRESSES && (offset == 510 || offset == 511); + assert_eq!( + *trace.main_table.get(row, cols::IS_PC), + FE::from(u64::from(is_pc)), + "row {row} (offset {offset})" + ); + } +} + +/// REG-C2 splits on IS_PC: x255 is finalized at the verifier's `final_pc_ts`, +/// every other register at its TIMESTAMP column (spec `halt.typ`). +#[test] +fn test_pc_final_token_uses_verifier_timestamp() { + use stark::lookup::Multiplicity; + let final_pc_ts = 4 * 1024 + 1; + let interactions = bus_interactions(final_pc_ts); + let pc_fini = interactions + .iter() + .find(|i| matches!(i.multiplicity, Multiplicity::Column(c) if c == cols::IS_PC)) + .expect("x255 final token"); + assert!(pc_fini.is_sender); + assert!( + format!("{:?}", pc_fini.values[3]).contains(&format!("Constant({final_pc_ts})")), + "x255 final timestamp is the constant final_pc_ts: {:?}", + pc_fini.values[3] + ); + let gp_fini = interactions + .iter() + .find(|i| matches!(i.multiplicity, Multiplicity::Negated(c) if c == cols::IS_PC)) + .expect("general register final token"); + assert!( + format!("{:?}", gp_fini.values[3]) + .contains(&format!("start_column: {}", cols::TIMESTAMP_LO)), + "{:?}", + gp_fini.values[3] + ); +} diff --git a/prover/src/tests/skip_empty_tables_tests.rs b/prover/src/tests/skip_empty_tables_tests.rs index 49f4e2947..f943a34a6 100644 --- a/prover/src/tests/skip_empty_tables_tests.rs +++ b/prover/src/tests/skip_empty_tables_tests.rs @@ -107,6 +107,7 @@ fn every_table_participates_in_the_bus() { true, &traces.page_configs, &table_counts, + &vec![4; table_counts.cpu], None, true, None, @@ -344,6 +345,12 @@ fn dropping_a_used_table_through_the_real_verifier_is_rejected() { false, &page_configs, &vm_proof.table_counts, + &crate::cpu_heights_from_proofs( + stark::proof::view::MultiProofView::Owned(&vm_proof.proof), + &vm_proof.table_counts, + true, + ) + .unwrap(), None, true, None, diff --git a/prover/src/tests/static_commitments_tests.rs b/prover/src/tests/static_commitments_tests.rs index 7b3d38e12..8441e7aae 100644 --- a/prover/src/tests/static_commitments_tests.rs +++ b/prover/src/tests/static_commitments_tests.rs @@ -1,6 +1,6 @@ //! Drift-detection and lookup-dispatch tests for the static preprocessed-table -//! commitments shipped in `bitwise`, `keccak_rc`, and `page` (the shared -//! zero-init page commitment). +//! commitments shipped in `bitwise`, `keccak_rc`, `page` (the shared +//! zero-init page commitment) and `cpu` (the per-height TIMESTAMP column). //! //! - The drift tests recompute the commitment for every blowup in //! `STATIC_BLOWUP_FACTORS` (the list shared with the generator binary) and @@ -22,7 +22,7 @@ use stark::proof::options::GoldilocksCubicProofOptions; -use crate::tables::{STATIC_BLOWUP_FACTORS, bitwise, keccak_rc, page}; +use crate::tables::{STATIC_BLOWUP_FACTORS, bitwise, cpu, keccak_rc, max_rows, page}; fn options_for(blowup: u8) -> stark::proof::options::ProofOptions { GoldilocksCubicProofOptions::with_blowup(blowup).expect("blowup must be a valid power of 2") @@ -296,3 +296,61 @@ fn bitwise_non_three_coset_recomputes_and_differs_from_static() { ); } } + +#[test] +fn cpu_timestamp_static_matches_recompute_for_all_heights_and_blowups() { + for &blowup in STATIC_BLOWUP_FACTORS { + let options = options_for(blowup); + for log_height in cpu::MIN_LOG_HEIGHT..=max_rows::CPU.trailing_zeros() { + let height = 1 << log_height; + assert_eq!( + cpu::static_timestamp_commitment(blowup, log_height), + Some(cpu::compute_timestamp_commitment(&options, height)), + "CPU timestamp commitment drifted for blowup={blowup}, height=2^{log_height}; \ + see `static_timestamp_commitment` before regenerating", + ); + assert_eq!( + cpu::timestamp_commitment(&options, height), + cpu::compute_timestamp_commitment(&options, height), + ); + } + } +} + +#[test] +fn cpu_timestamp_has_no_static_value_outside_the_cpu_height_range() { + for &blowup in STATIC_BLOWUP_FACTORS { + assert_eq!(cpu::static_timestamp_commitment(blowup, 0), None); + assert_eq!(cpu::static_timestamp_commitment(blowup, 1), None); + assert_eq!( + cpu::static_timestamp_commitment(blowup, max_rows::CPU.trailing_zeros() + 1), + None + ); + } + assert_eq!(cpu::static_timestamp_commitment(NON_STATIC_BLOWUP, 4), None); +} + +#[test] +fn cpu_timestamp_non_static_blowup_recomputes_via_fallback() { + let options = options_for(NON_STATIC_BLOWUP); + assert_eq!( + cpu::timestamp_commitment(&options, 1 << 6), + cpu::compute_timestamp_commitment(&options, 1 << 6), + ); +} + +#[test] +fn cpu_timestamp_non_three_coset_recomputes_and_differs_from_static() { + for &blowup in STATIC_BLOWUP_FACTORS { + let options = options_with_coset(blowup, NON_STANDARD_COSET); + let from_wrapper = cpu::timestamp_commitment(&options, 1 << 6); + assert_eq!( + from_wrapper, + cpu::compute_timestamp_commitment(&options, 1 << 6) + ); + assert_ne!( + from_wrapper, + cpu::timestamp_commitment(&options_with_coset(blowup, STANDARD_COSET), 1 << 6), + ); + } +} diff --git a/prover/tests/gpu_constraint_interp_real.rs b/prover/tests/gpu_constraint_interp_real.rs index 4446fb446..beb64c459 100644 --- a/prover/tests/gpu_constraint_interp_real.rs +++ b/prover/tests/gpu_constraint_interp_real.rs @@ -246,7 +246,7 @@ fn check_air(air: &dyn AIR, fn all_table_programs_gpu_match_cpu_oracle() { let opts = GoldilocksCubicProofOptions::with_blowup(2).expect("blowup=2 valid"); - check_air(&create_cpu_air(&opts), "CPU"); + check_air(&create_cpu_air(&opts, 0), "CPU"); check_air(&create_bitwise_air(&opts), "BITWISE"); check_air(&create_lt_air(&opts), "LT"); check_air(&create_shift_air(&opts), "SHIFT"); @@ -265,7 +265,7 @@ fn all_table_programs_gpu_match_cpu_oracle() { check_air(&create_halt_air(&opts), "HALT"); check_air(&create_commit_air(&opts), "COMMIT"); check_air(&create_page_air(&opts, 0x1000), "PAGE"); - check_air(&create_register_air(&opts), "REGISTER"); + check_air(&create_register_air(&opts, 0), "REGISTER"); check_air(&create_keccak_air(&opts), "KECCAK"); check_air(&create_keccak_rnd_air(&opts), "KECCAK_RND"); check_air(&create_keccak_rc_air(&opts), "KECCAK_RC"); From 65a9f201118581d8deb4d933685d0fd084d614a4 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Fri, 23 Oct 2026 17:00:31 -0300 Subject: [PATCH 7/8] Note that the halted register file pins x254's high word After the final-register pin, COPY's commit index cannot carry into x254's high word in a proof that verifies: FINI fixes it to 0 and the verifier refuses an output of 2^32 bytes or more. --- prover/src/tables/copy.rs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/prover/src/tables/copy.rs b/prover/src/tables/copy.rs index 98caeb1a8..e9893ef83 100644 --- a/prover/src/tables/copy.rs +++ b/prover/src/tables/copy.rs @@ -109,8 +109,11 @@ //! One consequence of that last column divergence is worth stating here rather than //! leaving for a reader to find: the `Commit` bus carries the index as `dst[0]` //! alone, while the verifier enumerates `start_index + i` over a `u64`. The two -//! agree only while the running commit index stays below `2^32`, and `x254`'s high -//! word is pinned to zero by the trace builder rather than by a constraint. +//! agree only while the running commit index stays below `2^32`. COPY puts no +//! constraint on `x254`'s high word, but the verifier pins the run's final register +//! file (`register::halted_fini`: x254 is the output length, high word 0) and refuses +//! an output of `2^32` bytes or more, so a run whose index carried into the high word +//! does not verify. //! //! What keeps that safe is not the prover's own range check -- that is a backstop //! for a bug, and it is unreachable. It is the executor: `commit_public_output` From 1342fb64d1806353e30a8d856d66ba22845b4949 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Fri, 23 Oct 2026 17:47:48 -0300 Subject: [PATCH 8/8] Correct the x254 high-word notes and count CPU's two Merkle trees - copy.rs: COPY keeps the commit index non-decreasing but does not force x254's high word to zero; the halted final register file does. The executor's 1 MiB cap only keeps honest runs provable. - prove_elfs_tests.rs: the forged high word is refused by COPY's dst_res ADD and the MEMW bus, not by REGISTER. - auto_storage.rs: the CPU table's TIMESTAMP is preprocessed, so the prover builds two Merkle trees for it; the RAM estimate counts both. - tables/mod.rs: CPU is 37 columns, effective width 97. - prove_with_options_and_inputs: an oversized public output is an error, not a panic; the layout test calls its masks optional tables. --- prover/src/auto_storage.rs | 10 +++++----- prover/src/lib.rs | 2 +- prover/src/tables/copy.rs | 24 +++++++++++++----------- prover/src/tables/mod.rs | 4 ++-- prover/src/tests/auto_storage_tests.rs | 2 +- prover/src/tests/cpu_timestamp_tests.rs | 4 ++-- prover/src/tests/prove_elfs_tests.rs | 11 ++++++----- 7 files changed, 30 insertions(+), 27 deletions(-) diff --git a/prover/src/auto_storage.rs b/prover/src/auto_storage.rs index 5ead5c369..2931bfa40 100644 --- a/prover/src/auto_storage.rs +++ b/prover/src/auto_storage.rs @@ -121,7 +121,7 @@ fn table_specs(lengths: &TableLengths) -> Vec { lengths.cpu_padded_rows, CPU_COLS as u64, aux_cols(cpu_buses(0).len()), - 1, + 2, // TIMESTAMP is preprocessed: see the note above BITWISE ), ( lengths.memw_padded_rows, @@ -183,10 +183,10 @@ fn table_specs(lengths: &TableLengths) -> Vec { aux_cols(copy_buses().len()), 1, ), - // BITWISE / DECODE / PAGE / REGISTER take the preprocessed-trace commit - // path: it extracts ALL columns into the LDE and builds two Merkle trees - // (precomputed_tree + mult_tree), so main_cols = full NUM_COLUMNS and - // main_trees = 2. + // BITWISE / DECODE / PAGE / REGISTER, and CPU above, take the + // preprocessed-trace commit path: it extracts ALL columns into the LDE and + // builds two Merkle trees (precomputed_tree + mult_tree), so main_cols = + // full NUM_COLUMNS and main_trees = 2. ( bitwise_rows, BITWISE_COLS as u64, diff --git a/prover/src/lib.rs b/prover/src/lib.rs index 7d4c9e8e9..f24bc7a61 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -1447,7 +1447,7 @@ pub fn prove_with_options_and_inputs( let cpu_heights = cpu_heights_from_traces(&traces); tables::cpu::validate_heights(&cpu_heights)?; let committed_bytes = u32::try_from(traces.public_output_bytes.len()) - .expect("trace build bounds the commit index to u32"); + .map_err(|_| Error::Prover("public output exceeds u32 range".to_string()))?; let airs = VmAirs::new( &program, proof_options, diff --git a/prover/src/tables/copy.rs b/prover/src/tables/copy.rs index 2b4198806..b41cce063 100644 --- a/prover/src/tables/copy.rs +++ b/prover/src/tables/copy.rs @@ -109,19 +109,21 @@ //! One consequence of that last column divergence is worth stating here rather than //! leaving for a reader to find: the `Commit` bus carries the index as `dst[0]` //! alone, while the verifier enumerates `start_index + i` over a `u64`. The two -//! agree only while the running commit index stays below `2^32`. COPY puts no -//! constraint on `x254`'s high word, but the verifier pins the run's final register -//! file (`register::halted_fini`: x254 is the output length, high word 0) and refuses -//! an output of `2^32` bytes or more, so a run whose index carried into the high word +//! agree only while the running commit index stays below `2^32`. Nothing in COPY +//! forces `x254`'s high word to zero: `copy:c:dst_res_is_write` only makes the +//! value written back `dst + count`, so the index never decreases and a carry into +//! the high word stays there. The verifier pins the run's final register file +//! (`register::halted_fini`: x254 is the output length, high word 0) and refuses an +//! output of `2^32` bytes or more, so a run whose index carried into the high word //! does not verify. //! -//! What keeps that safe is not the prover's own range check -- that is a backstop -//! for a bug, and it is unreachable. It is the executor: `commit_public_output` -//! caps the total committed output at `MAX_PUBLIC_OUTPUT_TOTAL_SIZE`, one mebibyte, -//! so the index of an honest run stays four orders of magnitude below `2^32`. A run -//! that tried to pass the cap fails in the executor, long before any trace exists. -//! Raising that cap is what would make this a live question, and the domain-2 write -//! is what retires it. +//! The executor is what keeps an honest run inside that bound: +//! `commit_public_output` caps the total committed output at +//! `MAX_PUBLIC_OUTPUT_TOTAL_SIZE`, one mebibyte, so the index of an honest run stays +//! four orders of magnitude below `2^32`. A run that tried to pass the cap fails in +//! the executor, long before any trace exists, and the prover's own range check is a +//! backstop for a bug, unreachable. Raising the cap past `2^32` bytes would make such +//! runs unprovable, not unsound; the domain-2 write is what would lift the bound. use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; use stark::trace::TraceTable; diff --git a/prover/src/tables/mod.rs b/prover/src/tables/mod.rs index 620fa65d4..97d46b90d 100644 --- a/prover/src/tables/mod.rs +++ b/prover/src/tables/mod.rs @@ -76,7 +76,7 @@ pub const STATIC_BLOWUP_FACTORS: &[u8] = &[2, 4, 8]; /// |---------|------|-----|-----------|----------| /// | MEMW | 49 | 26 | 127 | 2^19 | /// | MEMW_A | 29 | 20 | 89 | 2^19 * | -/// | CPU | 38 | 20 | 98 | 2^19 | +/// | CPU | 37 | 20 | 97 | 2^19 | /// | DVRM | 34 | 35 | 139 | 2^19 | /// | MUL | 26 | 25 | 101 | 2^20 † | /// | LT | 17 | 10 | 47 | 2^20 | @@ -85,7 +85,7 @@ pub const STATIC_BLOWUP_FACTORS: &[u8] = &[2, 4, 8]; /// | BRANCH | 14 | 6 | 32 | 2^20 | /// | MEMW_R | 10 | 7 | 31 | 2^20 | pub mod max_rows { - pub const CPU: usize = 1 << 19; // 524,288 — eff. width 98 + pub const CPU: usize = 1 << 19; // 524,288 — eff. width 97 pub const MEMW: usize = 1 << 19; // 524,288 — eff. width 127 (baseline) pub const MEMW_A: usize = 1 << 19; // 524,288 — eff. width 89 pub const DVRM: usize = 1 << 19; // 524,288 — eff. width 139 diff --git a/prover/src/tests/auto_storage_tests.rs b/prover/src/tests/auto_storage_tests.rs index 0049f367f..efe844018 100644 --- a/prover/src/tests/auto_storage_tests.rs +++ b/prover/src/tests/auto_storage_tests.rs @@ -36,7 +36,7 @@ fn peak_bytes_per_table_increment_is_exact() { let cpu_aux = cpu_buses(0).len().div_ceil(2) as u64; let per_row_persistent = cpu_main * GOLDILOCKS_BYTES * (1 + b) + cpu_aux * CUBIC_EXT_BYTES * (1 + b) - + 2 * b * KECCAK_NODE_BYTES // main Merkle (1 tree) + + 2 * 2 * b * KECCAK_NODE_BYTES // precomputed + mult Merkle trees + 2 * b * KECCAK_NODE_BYTES; // aux Merkle let per_row_transient = b * CUBIC_EXT_BYTES // constraint_evaluations + 2 * b * CUBIC_EXT_BYTES // composition LDE (2 parts, d=2) diff --git a/prover/src/tests/cpu_timestamp_tests.rs b/prover/src/tests/cpu_timestamp_tests.rs index 7be270efb..b8c714790 100644 --- a/prover/src/tests/cpu_timestamp_tests.rs +++ b/prover/src/tests/cpu_timestamp_tests.rs @@ -165,7 +165,7 @@ fn hostile_cpu_heights_are_rejected_by_the_verifier() { } /// `cpu_proof_start` (which the verifier reads CPU heights with) matches the -/// `air_refs` layout for every HALT / accelerator combination. Checked in +/// `air_refs` layout for every HALT / accelerator / IS_WH combination. Checked in /// release builds too, unlike the `debug_assert` in `air_refs`. #[test] fn cpu_proof_start_matches_air_refs_layout() { @@ -201,7 +201,7 @@ fn cpu_proof_start_matches_air_refs_layout() { assert_eq!( refs[start + k].name(), format!("CPU[{k}]"), - "halt={include_halt} accelerators={mask:06b}" + "halt={include_halt} optional={mask:06b}" ); } } diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index 28e20df78..62baad6e9 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -1773,11 +1773,12 @@ fn test_prove_commit_forged_index_rejected() { /// The high word of the commit index. /// /// `copy:c:read_dst` writes the full `DWordWL` of `dst_res` back to x254, but the -/// `Commit` bus carries the index as `dst[0]` alone and the trace builder pins x254's -/// high word to zero rather than a constraint doing it. That makes the high half the -/// one place where the register file and the COMMIT bus could drift apart, so it is -/// worth pinning that a forged high word is caught — by the REGISTER side, since -/// nothing in COPY looks at it. +/// `Commit` bus carries the index as `dst[0]` alone, which makes the high half the +/// one place where the register file and the COMMIT bus could drift apart. The +/// verifier pins x254's final high word to zero (`register::halted_fini`), but this +/// harness commits the trace's own FINI, so what refuses the forged high word here +/// is COPY's `copy:c:dst_res_is_write` (the `ADD`'s high carry is no longer a bit) +/// and the MEMW bus, where the forged x254 update no longer matches the honest one. #[test] fn test_prove_commit_forged_index_high_word_rejected() { use crate::tables::copy::cols as mm_cols;