From 76faeb28b5376f0a5acddbfacb8cf9144937227d Mon Sep 17 00:00:00 2001 From: MauroFab Date: Fri, 26 Jun 2026 18:34:05 -0300 Subject: [PATCH] Polish continuation verification and CLI --- bin/cli/README.md | 15 +- bin/cli/src/main.rs | 160 ++++++++------ prover/src/continuation.rs | 122 +++++++++-- prover/src/lib.rs | 21 +- prover/src/tables/global_memory.rs | 21 +- prover/src/tables/local_to_global.rs | 27 ++- prover/src/tables/trace_builder.rs | 7 +- prover/src/tests/local_to_global_bus_tests.rs | 207 +++++++++++++++++- prover/src/tests/prove_elfs_tests.rs | 17 ++ 9 files changed, 462 insertions(+), 135 deletions(-) diff --git a/bin/cli/README.md b/bin/cli/README.md index 7849a52c9..bc5eb9d53 100644 --- a/bin/cli/README.md +++ b/bin/cli/README.md @@ -57,8 +57,8 @@ cargo run -p cli --release -- prove -o proof.bin [flags] | `--private-input ` | Pass private input bytes to the guest. | | `--blowup ` | FRI blowup factor (power of 2). Higher = fewer queries, smaller proof, slower proving. [default: 2] | | `--time` | Print total proving time. | -| `--cycles` | Run one extra execution outside the timer and print the dynamic instruction count. | -| `--elements` | Build traces and print main-trace and aux-trace field element counts. | +| `--cycles` | Run one extra execution outside the timer and print the dynamic instruction count. Also supported with `--continuations`. | +| `--elements` | Build traces and print main-trace and aux-trace field element counts. Monolithic proving only; conflicts with `--continuations`. | | `--continuations` | Prove as a continuation bundle split into fixed-size epochs. | | `--epoch-size-log2 ` | Continuation epoch size as `2^N` cycles. Requires `--continuations`. Defaults to `20`; values below `18` are rejected. | @@ -76,7 +76,8 @@ cargo run -p cli --release -- verify [flags] | `--time` | Print verification time. | | `--continuations` | Verify a continuation proof bundle produced by `prove --continuations`. | -Returns exit code `0` on successful verification, `1` on failure. +Returns exit code `0` on successful verification, `1` on failure. `--blowup` must +match the value used during proving. ### Count Elements @@ -103,6 +104,9 @@ cargo run -p cli --release -- verify /tmp/proof.bin executor/program_artifacts/a cargo run -p cli --release -- prove program.elf -o /tmp/cont.bin --continuations --epoch-size-log2 20 cargo run -p cli --release -- verify /tmp/cont.bin program.elf --continuations +# Generate a continuation proof and print total dynamic instruction count +cargo run -p cli --release -- prove program.elf -o /tmp/cont.bin --continuations --cycles + # Prove with private input and print metrics cargo run -p cli --release -- prove program.elf -o /tmp/proof.bin --private-input input.bin --time --cycles ``` @@ -114,6 +118,11 @@ As rough ethrex 10-transfer distinct-account reference points from a local sweep about 26.8 GB. For a new workload, use the highest value the machine can run without swapping. +Continuation proof bundles are self-contained for standalone verification. When +`--private-input` is used, the serialized continuation proof includes the raw +private input bytes so the verifier can rebuild the genesis memory commitment. +Do not treat continuation proof files as confidential-input hiding artifacts. + ## Guest Program Flamegraphs Generate flamegraphs showing where the guest RISC-V program spends its execution time (by instruction count). diff --git a/bin/cli/src/main.rs b/bin/cli/src/main.rs index 1358fabe7..f42cb0b55 100644 --- a/bin/cli/src/main.rs +++ b/bin/cli/src/main.rs @@ -133,7 +133,7 @@ enum Commands { /// Blowup factor (power of 2). Higher = fewer queries, smaller proof, slower proving. #[arg(long, default_value = "2")] - blowup: Option, + blowup: u8, /// Print proving time #[arg(long)] @@ -145,7 +145,7 @@ enum Commands { /// Build traces and print total main-trace field elements (rows × columns summed across /// all tables) and aux-trace field elements (committed EF columns × rows) - #[arg(long)] + #[arg(long, conflicts_with = "continuations")] elements: bool, /// Prove with continuations (split execution into epochs; flat peak memory) @@ -175,7 +175,7 @@ enum Commands { /// Blowup factor used during proving (must match) #[arg(long, default_value = "2")] - blowup: Option, + blowup: u8, /// Print verification time #[arg(long)] @@ -221,7 +221,15 @@ fn main() -> ExitCode { epoch_size_log2, } => { if continuations { - cmd_prove_continuation(elf, output, private_input, epoch_size_log2, blowup, time) + cmd_prove_continuation( + elf, + output, + private_input, + epoch_size_log2, + blowup, + time, + cycles, + ) } else { cmd_prove(elf, output, private_input, blowup, time, cycles, elements) } @@ -253,6 +261,17 @@ fn read_private_input(path: Option<&PathBuf>) -> Result, String> { } } +fn count_cycles(elf_data: &[u8], private_inputs: &[u8]) -> Result { + let program = + Elf::load(elf_data).map_err(|e| format!("Failed to load ELF for cycle count: {e:?}"))?; + let executor = Executor::new(&program, private_inputs.to_vec()) + .map_err(|e| format!("Failed to create executor for cycle count: {e:?}"))?; + executor + .run() + .map(|result| result.logs.len() as u64) + .map_err(|e| format!("Execution failed during cycle count: {e:?}")) +} + fn cmd_execute( elf_path: PathBuf, private_input_path: Option, @@ -360,7 +379,7 @@ fn cmd_prove( elf_path: PathBuf, output_path: PathBuf, private_input_path: Option, - blowup: Option, + blowup: u8, time: bool, cycles: bool, elements: bool, @@ -386,24 +405,10 @@ fn cmd_prove( // Mirrors SP1's cycle-count pass so both provers report the same kind of // number without inflating the measured proving time. let cycle_count = if cycles { - let program = match Elf::load(&elf_data) { - Ok(p) => p, + match count_cycles(&elf_data, &private_inputs) { + Ok(count) => Some(count), Err(e) => { - eprintln!("Failed to load ELF for cycle count: {:?}", e); - return ExitCode::FAILURE; - } - }; - let executor = match Executor::new(&program, private_inputs.clone()) { - Ok(e) => e, - Err(e) => { - eprintln!("Failed to create executor for cycle count: {:?}", e); - return ExitCode::FAILURE; - } - }; - match executor.run() { - Ok(result) => Some(result.logs.len() as u64), - Err(e) => { - eprintln!("Execution failed during cycle count: {:?}", e); + eprintln!("{e}"); return ExitCode::FAILURE; } } @@ -434,31 +439,23 @@ fn cmd_prove( }); let start = Instant::now(); - let proof = match blowup { - Some(b) => { - let opts = match GoldilocksCubicProofOptions::with_blowup(b) { - Ok(opts) => opts, - Err(e) => { - eprintln!("Invalid proof options: {e}"); - return ExitCode::FAILURE; - } - }; - eprintln!( - "Generating proof (blowup={b}, queries={})...", - opts.fri_number_of_queries - ); - prover::prove_with_options_and_inputs( - &elf_data, - &private_inputs, - &opts, - &Default::default(), - ) - } - None => { - eprintln!("Generating proof..."); - prover::prove_with_inputs(&elf_data, &private_inputs) + let opts = match GoldilocksCubicProofOptions::with_blowup(blowup) { + Ok(opts) => opts, + Err(e) => { + eprintln!("Invalid proof options: {e}"); + return ExitCode::FAILURE; } }; + eprintln!( + "Generating proof (blowup={blowup}, queries={})...", + opts.fri_number_of_queries + ); + let proof = prover::prove_with_options_and_inputs( + &elf_data, + &private_inputs, + &opts, + &Default::default(), + ); let prove_elapsed = start.elapsed(); let proof = match proof { Ok(proof) => proof, @@ -510,7 +507,7 @@ fn cmd_prove( ExitCode::SUCCESS } -fn cmd_verify(proof_path: PathBuf, elf_path: PathBuf, blowup: Option, time: bool) -> ExitCode { +fn cmd_verify(proof_path: PathBuf, elf_path: PathBuf, blowup: u8, time: bool) -> ExitCode { eprintln!("Reading ELF file..."); let elf_data = match std::fs::read(&elf_path) { Ok(data) => data, @@ -539,19 +536,14 @@ fn cmd_verify(proof_path: PathBuf, elf_path: PathBuf, blowup: Option, time: eprintln!("Verifying proof..."); let start = Instant::now(); - let result = match blowup { - Some(b) => { - let opts = match GoldilocksCubicProofOptions::with_blowup(b) { - Ok(opts) => opts, - Err(e) => { - eprintln!("Invalid proof options: {e}"); - return ExitCode::FAILURE; - } - }; - prover::verify_with_options(&proof, &elf_data, &opts, None, None) + let opts = match GoldilocksCubicProofOptions::with_blowup(blowup) { + Ok(opts) => opts, + Err(e) => { + eprintln!("Invalid proof options: {e}"); + return ExitCode::FAILURE; } - None => prover::verify(&proof, &elf_data), }; + let result = prover::verify_with_options(&proof, &elf_data, &opts, None, None); let verify_elapsed = start.elapsed(); let result = match result { Ok(valid) => valid, @@ -568,7 +560,7 @@ fn cmd_verify(proof_path: PathBuf, elf_path: PathBuf, blowup: Option, time: } ExitCode::SUCCESS } else { - eprintln!("Verification failed!"); + eprintln!("Verification failed! Ensure --blowup matches the value used for proving."); ExitCode::FAILURE } } @@ -578,8 +570,9 @@ fn cmd_prove_continuation( output_path: PathBuf, private_input_path: Option, epoch_size_log2: Option, - blowup: Option, + blowup: u8, time: bool, + cycles: bool, ) -> ExitCode { eprintln!("Reading ELF file..."); let elf_data = match std::fs::read(&elf_path) { @@ -598,6 +591,18 @@ fn cmd_prove_continuation( } }; + let cycle_count = if cycles { + match count_cycles(&elf_data, &private_inputs) { + Ok(count) => Some(count), + Err(e) => { + eprintln!("{e}"); + return ExitCode::FAILURE; + } + } + } else { + None + }; + let epoch_size_log2 = epoch_size_log2.unwrap_or(DEFAULT_CONTINUATION_EPOCH_SIZE_LOG2); let epoch_size = match continuation_epoch_size(epoch_size_log2) { Ok(size) => size, @@ -607,7 +612,6 @@ fn cmd_prove_continuation( } }; - let blowup = blowup.unwrap_or(2); let opts = match GoldilocksCubicProofOptions::with_blowup(blowup) { Ok(opts) => opts, Err(e) => { @@ -656,6 +660,9 @@ fn cmd_prove_continuation( } eprintln!("Proof written to {:?}", output_path); + if let Some(c) = cycle_count { + println!("Cycles: {}", c); + } println!("Epochs: {}", bundle.num_epochs()); if time { println!("Proving time: {:.3}s", prove_elapsed.as_secs_f64()); @@ -666,7 +673,7 @@ fn cmd_prove_continuation( fn cmd_verify_continuation( proof_path: PathBuf, elf_path: PathBuf, - blowup: Option, + blowup: u8, time: bool, ) -> ExitCode { eprintln!("Reading ELF file..."); @@ -694,7 +701,6 @@ fn cmd_verify_continuation( } }; - let blowup = blowup.unwrap_or(2); let opts = match GoldilocksCubicProofOptions::with_blowup(blowup) { Ok(opts) => opts, Err(e) => { @@ -719,7 +725,7 @@ fn cmd_verify_continuation( ExitCode::SUCCESS } Ok(None) => { - eprintln!("Verification failed!"); + eprintln!("Verification failed! Ensure --blowup matches the value used for proving."); ExitCode::FAILURE } Err(e) => { @@ -819,6 +825,34 @@ mod tests { assert!(r.is_ok()); } + #[test] + fn cycles_accepts_continuations() { + let r = Cli::command().try_get_matches_from([ + "cli", + "prove", + "prog.elf", + "-o", + "out", + "--continuations", + "--cycles", + ]); + assert!(r.is_ok()); + } + + #[test] + fn elements_conflicts_with_continuations() { + let r = Cli::command().try_get_matches_from([ + "cli", + "prove", + "prog.elf", + "-o", + "out", + "--continuations", + "--elements", + ]); + assert!(r.is_err()); + } + #[test] fn epoch_size_log2_rejects_tiny_cli_values() { let r = Cli::command().try_get_matches_from([ diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index 01a9edbf3..94e109664 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -11,11 +11,11 @@ //! //! The local-to-global columns are range-checked in the epoch proof (which //! carries the BITWISE provider): values are bytes, and the cross-epoch-only -//! quantities (epoch, init-timestamp) are built from `IsHalfword`-checked -//! halfwords. Address and fini-timestamp need no extra check — they are matched -//! against MEMW on the epoch-local Memory bus, exactly as PAGE relies on MEMW. -//! The global proof commits the identical trace, so it inherits the guarantee -//! via the commitment binding. +//! `init_epoch` is built from `IsHalfword`-checked halfwords. Address and +//! fini-timestamp need no extra check — they are matched against MEMW on the +//! epoch-local Memory bus, exactly as PAGE relies on MEMW. The global proof +//! commits the identical trace, so it inherits the guarantee via the commitment +//! binding. There is no cross-epoch timestamp; the chain is ordered by epoch. //! //! Cross-epoch registers are bound the same way: each continuation epoch //! preprocesses its REGISTER `FINI` column to the epoch's final register file @@ -39,6 +39,7 @@ use std::collections::HashMap; use crypto::fiat_shamir::default_transcript::DefaultTranscript; use executor::elf::Elf; use executor::vm::execution::Executor; +use executor::vm::memory::MAX_PRIVATE_INPUT_SIZE; use math::field::element::FieldElement; use stark::config::Commitment; use stark::lookup::{AirWithBuses, AuxiliaryTraceBuildData, NullBoundaryConstraintBuilder}; @@ -57,8 +58,8 @@ use crate::tables::trace_builder::{Traces, build_init_page_data, build_initial_i use crate::tables::types::{GoldilocksExtension, GoldilocksField}; use crate::tables::{MaxRowsConfig, global_memory}; use crate::{ - Error, RuntimePageRange, TableCounts, VmAirs, compute_expected_commit_bus_balance, - verify_l2g_commitment_binding, + Error, FIXED_TABLE_COUNT, RuntimePageRange, TableCounts, VmAirs, + compute_expected_commit_bus_balance, verify_l2g_commitment_binding, }; type F = GoldilocksField; @@ -247,7 +248,11 @@ struct EpochProof { public_output: Vec, /// Statement values the epoch transcript is seeded with (re-derived on verify). table_counts: TableCounts, + /// Always zero for continuation epochs: PAGE is replaced by L2G, and private + /// input genesis is carried by the continuation bundle for global verification. num_private_input_pages: usize, + /// Always empty for continuation epochs: PAGE tables are skipped, so runtime + /// pages are not part of the epoch AIR statement. runtime_page_ranges: Vec, /// The epoch's final register file `R_{i+1}` (its preprocessed FINI), which the /// driver/verifier reuses as the next epoch's derived INIT — the cross-epoch @@ -299,7 +304,15 @@ fn build_epoch_airs( is_final: bool, ) -> VmAirs { let register_init_arg = if is_first { None } else { Some(register_init) }; - let mut airs = VmAirs::new( + // Continuation epochs preprocess FINI = R_{i+1} too (not just INIT = R_i), so the + // 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, false, @@ -309,16 +322,8 @@ fn build_epoch_airs( is_final, register_init_arg, None, - ); - // Continuation epochs preprocess FINI = R_{i+1} too (not just INIT = R_i), so the - // 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). - airs.register = crate::test_utils::create_register_air(opts).with_preprocessed( - register::compute_precomputed_commitment_with_fini(opts, register_init, reg_fini), - register::NUM_PREPROCESSED_COLS_WITH_FINI, - ); - airs + register_preprocessed, + ) } /// Prove one epoch (prove half only). Commits its local-to-global table (built from @@ -447,6 +452,19 @@ fn verify_epoch( return false; } + // Cross-check table_counts before building AIRs from bundle data. Continuation + // epochs have no PAGE proofs, and append one epoch-local L2G proof after the VM + // tables. HALT is present only on the final epoch. + let fixed_tables = if is_final { + FIXED_TABLE_COUNT + } else { + FIXED_TABLE_COUNT - 1 + }; + let expected_proof_count = epoch.table_counts.total() + fixed_tables + 1; + if expected_proof_count != epoch.proof.proofs.len() { + return false; + } + let airs = build_epoch_airs( elf, opts, @@ -742,6 +760,13 @@ pub fn verify_continuation( bundle: &ContinuationProof, opts: &ProofOptions, ) -> Result>, Error> { + if bundle.private_inputs.len() as u64 > MAX_PRIVATE_INPUT_SIZE { + return Err(Error::InvalidTableCounts(format!( + "private input size ({}) exceeds max ({MAX_PRIVATE_INPUT_SIZE})", + bundle.private_inputs.len() + ))); + } + let elf = Elf::load(elf_bytes).map_err(|e| Error::ElfLoad(format!("{e}")))?; let n = bundle.epochs.len(); @@ -1079,6 +1104,67 @@ mod tests { ); } + // Negative: table_counts are bundle data. Inflating a positive count must be + // rejected before the verifier builds AIRs from the malformed shape. + #[test] + fn test_split_verify_rejects_inflated_epoch_table_count() { + let _ = env_logger::builder().is_test(true).try_init(); + let elf_bytes = asm_elf_bytes("all_loadstore_32"); + let mut bundle = + prove_continuation(&elf_bytes, &[], 8, &ProofOptions::default_test_options()).unwrap(); + bundle.epochs[0].table_counts.cpu += 1; + assert!( + verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()) + .unwrap() + .is_none() + ); + } + + // Negative: the verifier rebuilds private-input genesis from bundle bytes. + // Changing those bytes after proving changes the global-memory preprocessed + // genesis commitment, so the standalone verifier must reject. + #[test] + fn test_split_verify_rejects_tampered_private_input_genesis() { + let _ = env_logger::builder().is_test(true).try_init(); + let elf_bytes = asm_elf_bytes("test_private_input_xpage"); + let private_inputs: Vec = (0u8..16).collect(); + let mut bundle = prove_continuation( + &elf_bytes, + &private_inputs, + 4, + &ProofOptions::default_test_options(), + ) + .unwrap(); + assert!( + verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()) + .unwrap() + .is_some(), + "baseline must verify before tampering" + ); + + bundle.private_inputs[4] ^= 0xFF; + assert!( + verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()) + .unwrap() + .is_none() + ); + } + + // Negative: verifier-side private inputs are deserialized/untrusted, so reject + // oversized bundles before rebuilding genesis page configs from them. + #[test] + fn test_split_verify_rejects_oversized_private_inputs() { + let _ = env_logger::builder().is_test(true).try_init(); + let elf_bytes = asm_elf_bytes("all_loadstore_32"); + let mut bundle = + prove_continuation(&elf_bytes, &[], 8, &ProofOptions::default_test_options()).unwrap(); + bundle.private_inputs = vec![0; MAX_PRIVATE_INPUT_SIZE as usize + 1]; + assert!(matches!( + verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()), + Err(Error::InvalidTableCounts(_)) + )); + } + // The bundle's `boundary` field is used only to rebuild the global AIRs' touched- // PAGE set (genesis is recomputed from the ELF). The cross-epoch memory values // live in the committed L2G traces, tied to the epoch proofs by diff --git a/prover/src/lib.rs b/prover/src/lib.rs index 5799fbaea..eb52cbcb5 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -439,6 +439,7 @@ impl VmAirs { include_halt: bool, register_init: Option<&[u32]>, page_commitments: Option<&[(u64, Commitment)]>, + register_preprocessed: Option<(Commitment, usize)>, ) -> Self { let cpus: Vec<_> = (0..table_counts.cpu) .map(|i| create_cpu_air(proof_options).with_name(&format!("CPU[{}]", i))) @@ -489,16 +490,20 @@ impl VmAirs { tables::keccak_rc::preprocessed_commitment(proof_options), tables::keccak_rc::NUM_PRECOMPUTED_COLS, ); - let register_init = register_init - .map(<[u32]>::to_vec) - .unwrap_or_else(|| register::register_init_from_entry_point(elf.entry_point)); let ecsm = create_ecsm_air(proof_options); let ec_scalar = create_ec_scalar_air(proof_options); let ecdas = create_ecdas_air(proof_options); - let register = create_register_air(proof_options).with_preprocessed( - register::preprocessed_commitment(proof_options, ®ister_init), - register::NUM_PREPROCESSED_COLS, - ); + let register = if let Some((commitment, num_preprocessed_cols)) = register_preprocessed { + 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)); + create_register_air(proof_options).with_preprocessed( + register::preprocessed_commitment(proof_options, ®ister_init), + 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 @@ -826,6 +831,7 @@ pub fn prove_with_options_and_inputs( true, None, None, + None, ); #[cfg(feature = "instruments")] @@ -987,6 +993,7 @@ pub fn verify_with_options( true, None, page_commitments, + None, ); // Recompute the COMMIT output bus offset from VmProof.public_output. diff --git a/prover/src/tables/global_memory.rs b/prover/src/tables/global_memory.rs index bcc7066c5..b3f22b172 100644 --- a/prover/src/tables/global_memory.rs +++ b/prover/src/tables/global_memory.rs @@ -36,10 +36,10 @@ use std::collections::HashMap; -use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; +use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity}; use stark::trace::TraceTable; -use super::local_to_global::GENESIS_EPOCH; +use super::local_to_global::{GENESIS_EPOCH, direct}; use super::page::{DEFAULT_PAGE_SIZE, PageConfig}; use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField}; @@ -102,7 +102,7 @@ pub type FiniStateMap = HashMap; /// Generates a GLOBAL_MEMORY trace for a single page. /// /// `config` supplies `page_base` and the genesis `init_values` (from the ELF); -/// `final_state` maps each touched byte to its final value/epoch/timestamp. +/// `final_state` maps each touched byte to its final value and last-touch epoch. pub fn generate_global_trace( config: &PageConfig, final_state: &FiniStateMap, @@ -184,10 +184,7 @@ pub fn bus_interactions(page_base: u64) -> Vec { vec![ address_lo.clone(), address_hi.clone(), - BusValue::Packed { - start_column: cols::INIT, - packing: Packing::Direct, - }, + direct(cols::INIT), BusValue::constant(GENESIS_EPOCH), ], ), @@ -198,14 +195,8 @@ pub fn bus_interactions(page_base: u64) -> Vec { vec![ address_lo, address_hi, - BusValue::Packed { - start_column: cols::FINI, - packing: Packing::Direct, - }, - BusValue::Packed { - start_column: cols::FINI_EPOCH, - packing: Packing::Direct, - }, + direct(cols::FINI), + direct(cols::FINI_EPOCH), ], ), ] diff --git a/prover/src/tables/local_to_global.rs b/prover/src/tables/local_to_global.rs index 77bf215a3..eb91b36f3 100644 --- a/prover/src/tables/local_to_global.rs +++ b/prover/src/tables/local_to_global.rs @@ -37,15 +37,14 @@ //! every row of an epoch's table, so it is supplied as a per-table constant (not //! a column) by [`bus_interactions`]. //! -//! The columns that live ONLY on the cross-epoch `GlobalMemory` bus have no MEMW -//! partner: `init_epoch` and `init_timestamp` (the epoch-local `init` token is -//! seeded at timestamp 0, so `init_timestamp` never reaches the Memory bus). -//! These are stored as 16-bit halfword columns, each checked via `IsHalfword`, -//! and the 32-bit value the bus matches on is rebuilt from them by a linear -//! combination (see [`word`]). The checks are emitted on the epoch-local table -//! (which has the BITWISE provider); the global proof commits the identical +//! The only column that lives ONLY on the cross-epoch `GlobalMemory` bus has no +//! MEMW partner: `init_epoch`. It is stored as two 16-bit halfword columns, each +//! checked via `IsHalfword`, and the 32-bit bus value is rebuilt from them by a +//! linear combination (see [`word`]). The checks are emitted on the epoch-local +//! table (which has the BITWISE provider); the global proof commits the identical //! trace (the commitment binding compares their roots), so it inherits the same -//! guarantee. +//! guarantee. There is no `init_timestamp` column: timestamps are epoch-local, and +//! the cross-epoch chain is ordered by epoch. //! //! ## Padding //! @@ -187,11 +186,11 @@ pub fn genesis_provenance(genesis: impl IntoIterator) -> Prov /// Column indices for the local-to-global table: one row per touched cell. /// /// `address` and `fini_timestamp` are plain 32-bit columns (matched on the Memory -/// bus against MEMW). The cross-epoch-only quantities `init_epoch` and -/// `init_timestamp` are stored as 16-bit halfword columns ([`RANGE_CHECKED_HALFWORDS`]) -/// checked via `IsHalfword` and rebuilt into their 32-bit bus value via [`word`]. -/// The value bytes get the batched `AreBytes` check. `fini_epoch` is a per-table -/// constant (not a column). `MU` is the real-row selector / multiplicity. +/// bus against MEMW). The cross-epoch-only `init_epoch` is stored as 16-bit +/// halfword columns ([`RANGE_CHECKED_HALFWORDS`]), checked via `IsHalfword`, and +/// rebuilt into its 32-bit bus value via [`word`]. The value bytes get the +/// batched `AreBytes` check. `fini_epoch` is a per-table constant (not a column). +/// `MU` is the real-row selector / multiplicity. pub mod cols { /// address_lo: 32-bit; matched on the Memory bus against MEMW. pub const ADDRESS_LO: usize = 0; @@ -290,7 +289,7 @@ fn word(lo_col: usize, hi_col: usize) -> BusValue { } /// A column read directly as a single field element (a 32-bit word or a byte). -fn direct(column: usize) -> BusValue { +pub(crate) fn direct(column: usize) -> BusValue { BusValue::Packed { start_column: column, packing: Packing::Direct, diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 3365eec5a..a124d60ae 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -2101,13 +2101,10 @@ fn collect_bitwise_from_commit(commit_ops: &[CommitOperation]) -> Vec BitwiseOperation { BitwiseOperation::halfword( BitwiseOperationType::IsHalf, diff --git a/prover/src/tests/local_to_global_bus_tests.rs b/prover/src/tests/local_to_global_bus_tests.rs index b62512466..66724c27a 100644 --- a/prover/src/tests/local_to_global_bus_tests.rs +++ b/prover/src/tests/local_to_global_bus_tests.rs @@ -22,6 +22,7 @@ use stark::trace::TraceTable; use stark::traits::AIR; use stark::verifier::{IsStarkVerifier, Verifier}; +use crate::tables::bitwise::{BitwiseOperation, BitwiseOperationType}; use crate::tables::local_to_global::{ self, CellBoundary, GENESIS_EPOCH, epoch_boundaries, generate_local_to_global_trace, }; @@ -140,6 +141,19 @@ mod memw_sub_cols { pub const NUM_COLUMNS: usize = 6; } +/// Minimal BITWISE-receiver substitute for the L2G range-check buses. It receives +/// the same AreBytes, IsHalfword, and IsB20 tokens that the real BITWISE table +/// would receive, but only for rows supplied by the test. +mod range_recv_cols { + pub const X: usize = 0; + pub const Y: usize = 1; + pub const Z: usize = 2; + pub const MU_ARE_BYTES: usize = 3; + pub const MU_IS_HALF: usize = 4; + pub const MU_IS_B20: usize = 5; + pub const NUM_COLUMNS: usize = 6; +} + /// MEMW-substitute air: counterpart to `memory_bus_interactions`. Sends each /// cell's init token at ts=0 (cancelling L2G's init-receive) and receives each /// cell's fini token at the last timestamp (cancelling L2G's fini-send). @@ -206,6 +220,102 @@ fn memw_sub_air( ) } +fn l2g_range_air( + proof_options: &ProofOptions, + epoch_label: u64, +) -> AirWithBuses { + let transition_constraints: Vec>> = vec![]; + AirWithBuses::new( + local_to_global::cols::NUM_COLUMNS, + AuxiliaryTraceBuildData { + interactions: local_to_global::range_check_interactions(epoch_label), + }, + proof_options, + 1, + transition_constraints, + ) +} + +fn range_receiver_air( + proof_options: &ProofOptions, +) -> AirWithBuses { + let transition_constraints: Vec>> = vec![]; + let interactions = vec![ + BusInteraction::receiver( + BusId::AreBytes, + Multiplicity::Column(range_recv_cols::MU_ARE_BYTES), + vec![ + BusValue::Packed { + start_column: range_recv_cols::X, + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: range_recv_cols::Y, + packing: Packing::Direct, + }, + ], + ), + BusInteraction::receiver( + BusId::IsHalfword, + Multiplicity::Column(range_recv_cols::MU_IS_HALF), + vec![BusValue::linear(vec![ + stark::lookup::LinearTerm::Column { + coefficient: 1, + column: range_recv_cols::X, + }, + stark::lookup::LinearTerm::Column { + coefficient: 256, + column: range_recv_cols::Y, + }, + ])], + ), + BusInteraction::receiver( + BusId::IsB20, + Multiplicity::Column(range_recv_cols::MU_IS_B20), + vec![BusValue::linear(vec![ + stark::lookup::LinearTerm::Column { + coefficient: 1, + column: range_recv_cols::X, + }, + stark::lookup::LinearTerm::Column { + coefficient: 256, + column: range_recv_cols::Y, + }, + stark::lookup::LinearTerm::Column { + coefficient: 65536, + column: range_recv_cols::Z, + }, + ])], + ), + ]; + AirWithBuses::new( + range_recv_cols::NUM_COLUMNS, + AuxiliaryTraceBuildData { interactions }, + proof_options, + 1, + transition_constraints, + ) +} + +fn range_receiver_trace(ops: &[BitwiseOperation]) -> TraceTable { + let num_rows = ops.len().next_power_of_two().max(4); + let mut data = vec![FE::zero(); num_rows * range_recv_cols::NUM_COLUMNS]; + for (i, op) in ops.iter().enumerate() { + let base = i * range_recv_cols::NUM_COLUMNS; + data[base + range_recv_cols::X] = FE::from(op.x as u64); + data[base + range_recv_cols::Y] = FE::from(op.y as u64); + data[base + range_recv_cols::Z] = FE::from(op.z as u64); + let mu_col = match op.lookup_type { + BitwiseOperationType::AreBytes => range_recv_cols::MU_ARE_BYTES, + BitwiseOperationType::IsHalf => range_recv_cols::MU_IS_HALF, + BitwiseOperationType::IsB20 => range_recv_cols::MU_IS_B20, + _ => panic!("unexpected L2G range-check lookup"), + }; + data[base + mu_col] = FE::one(); + } + TraceTable::new_main(data, range_recv_cols::NUM_COLUMNS, 1) +} + fn memw_sub_trace(boundary: &[CellBoundary]) -> TraceTable { let num_rows = boundary.len().next_power_of_two().max(4); let mut data = vec![FE::zero(); num_rows * memw_sub_cols::NUM_COLUMNS]; @@ -245,6 +355,34 @@ fn prove_verify_memory(l2g_boundary: &[CellBoundary], memw_boundary: &[CellBound ) } +fn prove_verify_l2g_range_with_trace( + l2g_trace: &mut TraceTable, + range_ops: &[BitwiseOperation], + epoch_label: u64, +) -> bool { + let proof_options = ProofOptions::default_test_options(); + let l2g = l2g_range_air(&proof_options, epoch_label); + let receiver = range_receiver_air(&proof_options); + let mut receiver_trace = range_receiver_trace(range_ops); + let pairs: Vec<( + &dyn AIR, + _, + _, + )> = vec![ + (&l2g, l2g_trace, &()), + (&receiver, &mut receiver_trace, &()), + ]; + let proof = multi_prove_ram(pairs, &mut DefaultTranscript::::new(&[])).unwrap(); + let airs: Vec<&dyn AIR> = + vec![&l2g, &receiver]; + Verifier::multi_verify( + &airs, + &proof, + &mut DefaultTranscript::::new(&[]), + &FieldElement::zero(), + ) +} + /// Inert L2G AIR: commits the trace columns with no bus and no constraints — /// the deterministic commitment an epoch proof publishes for its L2G table. The /// main-trace Merkle root is over the main columns only, so it matches the L2G @@ -690,13 +828,13 @@ fn test_l2g_mu_nonboolean_rejects_global_bus() { /// complete BITWISE sub-proof here would require replicating `prove_epoch`'s /// full table set, which is out of scope for a unit bus test. /// -/// What we CAN assert at this level: the arithmetic property that makes the -/// attack fail. `test_ordering_rejects_future_reference` in +/// This test asserts the arithmetic property that makes the attack fail. +/// `test_ordering_rejects_future_reference` in /// `local_to_global.rs::tests` (line 831) already verifies that the field /// value `fini_epoch − 1 − init_epoch` wraps to a value ≥ 2^20 for both -/// self-references and future-references, so no IsB20 row matches. This test -/// documents the gap and its justification — the ordering property is fully -/// covered by that unit test plus the continuation integration tests. +/// self-references and future-references, so no IsB20 row matches. The +/// proof-level bus path is covered by +/// `test_l2g_init_epoch_ordering_live_is_b20_rejects` below. /// /// Variants that ARE expressible without the full bitwise table: /// - Self-reference (init_epoch == fini_epoch) and future-reference @@ -705,11 +843,8 @@ fn test_l2g_mu_nonboolean_rejects_global_bus() { /// checks that tokens match across epochs. The IsB20 sender is wired /// exclusively on the epoch-local table (which carries the BITWISE provider). /// -/// Skipping the full prove+verify here; the unit test at -/// `local_to_global::tests::test_ordering_rejects_future_reference` (line 831) -/// is the normative coverage for this invariant. A full integration test would -/// require wiring the BITWISE table, which is tested end-to-end by the -/// continuation tests in `continuation.rs::tests`. +/// The paired live-bus test wires an L2G range-check AIR to a minimal BITWISE +/// receiver table and proves that a self-reference rejects through IsB20. #[test] fn test_l2g_init_epoch_ordering_field_arithmetic() { // Verify the arithmetic property that underlies the IsB20 soundness argument @@ -746,6 +881,58 @@ fn test_l2g_init_epoch_ordering_field_arithmetic() { ); } +#[test] +fn test_l2g_init_epoch_ordering_live_is_b20_rejects() { + // Epoch 1 consumes epoch 0's fini for cell 10. Honest ordering has + // init_epoch=1, fini_epoch=2, so 2 - 1 - 1 = 0 is a valid IsB20 lookup. + let initial_memory = HashMap::new(); + let epochs = vec![vec![(10, 7, 3)], vec![(10, 8, 10)]]; + let boundaries = epoch_boundaries(&initial_memory, &epochs); + let boundary = &boundaries[1]; + let epoch_label = boundary[0].fini.epoch; + assert_eq!(epoch_label, 2); + + let mut honest_trace = generate_local_to_global_trace(boundary); + let honest_ops = local_to_global::collect_bitwise_from_l2g(boundary); + assert!( + prove_verify_l2g_range_with_trace(&mut honest_trace, &honest_ops, epoch_label), + "honest L2G range checks must balance against BITWISE receivers" + ); + + // Forge a self-reference: init_epoch == fini_epoch. The halfword lookups are + // still satisfiable, so the receiver table below includes them. The missing + // piece is exactly IsB20[2 - 1 - 2], which underflows in the field and has no + // valid 20-bit receiver row. + let mut forged_trace = generate_local_to_global_trace(boundary); + forged_trace.main_table.set( + 0, + local_to_global::cols::INIT_EPOCH_0, + FE::from(epoch_label), + ); + forged_trace + .main_table + .set(0, local_to_global::cols::INIT_EPOCH_1, FE::zero()); + + let cell = boundary[0]; + let forged_ops = vec![ + BitwiseOperation::byte_op( + BitwiseOperationType::AreBytes, + (cell.init.value & 0xFF) as u8, + (cell.fini.value & 0xFF) as u8, + ), + BitwiseOperation::halfword( + BitwiseOperationType::IsHalf, + (epoch_label & 0xFF) as u8, + ((epoch_label >> 8) & 0xFF) as u8, + ), + BitwiseOperation::halfword(BitwiseOperationType::IsHalf, 0, 0), + ]; + assert!( + !prove_verify_l2g_range_with_trace(&mut forged_trace, &forged_ops, epoch_label), + "self-referential init_epoch must fail through the live IsB20 bus" + ); +} + // ========================================================================= // Soundness regression tests: Design-Y orphan attack // ========================================================================= diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index 22ed73dc4..10013b5ed 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -62,6 +62,7 @@ fn prove_and_verify_vm_minimal(elf: &Elf, traces: &mut Traces) -> bool { true, None, None, + None, ); // Build air_trace_pairs for all tables @@ -116,6 +117,7 @@ fn prove_vm_minimal(elf_bytes: &[u8], private_inputs: &[u8], max_rows: &MaxRowsC true, None, None, + None, ); let runtime_page_ranges = traces.runtime_page_ranges(); let proof = multi_prove_ram( @@ -158,6 +160,7 @@ fn verify_vm_minimal(vm_proof: &VmProof, elf_bytes: &[u8]) -> bool { true, None, None, + None, ); let air_refs = airs.air_refs(); let mut replay_transcript = DefaultTranscript::::new(&[]); @@ -1348,6 +1351,7 @@ fn test_prove_elfs_test_commit_4_wrong_pages_rejected() { true, None, None, + None, ); let proof = multi_prove_ram( prover_airs.air_trace_pairs(&mut traces), @@ -1367,6 +1371,7 @@ fn test_prove_elfs_test_commit_4_wrong_pages_rejected() { true, None, None, + None, ); let verifier_air_refs = verifier_airs.air_refs(); let mut replay_transcript = DefaultTranscript::::new(&[]); @@ -2102,6 +2107,7 @@ fn test_deep_stack_runtime_pages_roundtrip() { true, None, None, + None, ); let proof = multi_prove_ram( prover_airs.air_trace_pairs(&mut traces), @@ -2120,6 +2126,7 @@ fn test_deep_stack_runtime_pages_roundtrip() { true, None, None, + None, ); let verifier_air_refs = verifier_airs.air_refs(); let mut replay_transcript = DefaultTranscript::::new(&[]); @@ -2173,6 +2180,7 @@ fn test_deep_stack_missing_pages_rejected() { true, None, None, + None, ); let proof = multi_prove_ram( prover_airs.air_trace_pairs(&mut traces), @@ -2191,6 +2199,7 @@ fn test_deep_stack_missing_pages_rejected() { true, None, None, + None, ); let verifier_air_refs = verifier_airs.air_refs(); let mut replay_transcript = DefaultTranscript::::new(&[]); @@ -2279,6 +2288,7 @@ fn test_heap_alloc_runtime_pages_roundtrip() { true, None, None, + None, ); let proof = multi_prove_ram( prover_airs.air_trace_pairs(&mut traces), @@ -2297,6 +2307,7 @@ fn test_heap_alloc_runtime_pages_roundtrip() { true, None, None, + None, ); let verifier_air_refs = verifier_airs.air_refs(); let mut replay_transcript = DefaultTranscript::::new(&[]); @@ -2465,6 +2476,7 @@ fn test_crafted_zero_count_proof_must_not_verify() { true, None, None, + None, ); let verifier_air_refs = airs.air_refs(); @@ -2947,6 +2959,7 @@ fn test_prove_first_epoch_without_halt() { false, None, None, + None, ); let multi_proof = multi_prove_ram( @@ -3030,6 +3043,7 @@ fn test_prove_second_epoch_from_snapshot() { false, Some(®ister_init), None, + None, ); let multi_proof = multi_prove_ram( @@ -3120,6 +3134,7 @@ fn test_epoch_proof_commits_l2g() { false, None, None, + None, ); // Inert L2G AIR: commits the trace columns, but no bus and no constraints. @@ -3273,6 +3288,7 @@ fn test_continuation_pipeline_end_to_end() { is_final, register_init_arg, None, + None, ); let mut l2g_trace = local_to_global::generate_local_to_global_trace(&boundaries[i]); @@ -3397,6 +3413,7 @@ fn test_epoch_memory_bus_with_l2g_bookend() { false, None, None, + None, ); // L2G air on the epoch-local Memory bus (the bookend that replaces PAGE).