From 64880f9772a10ca7dff71dbcdf6066cf412174ed Mon Sep 17 00:00:00 2001 From: Nicole Date: Wed, 1 Jul 2026 15:37:36 -0300 Subject: [PATCH 1/2] Move the COMMIT chip's output onto the Memory bus under a domain=2 separator --- docs/continuations_design.md | 46 +- prover/src/continuation.rs | 407 +++++++++++++++--- prover/src/lib.rs | 89 ++-- prover/src/statement.rs | 10 +- prover/src/tables/commit.rs | 92 ++-- prover/src/tables/cpu.rs | 6 +- prover/src/tables/cpu32.rs | 6 +- prover/src/tables/ec_scalar.rs | 4 +- prover/src/tables/ecsm.rs | 10 +- prover/src/tables/halt.rs | 10 +- prover/src/tables/keccak.rs | 8 +- prover/src/tables/load.rs | 4 +- prover/src/tables/local_to_global.rs | 4 +- prover/src/tables/memw.rs | 54 ++- prover/src/tables/memw_aligned.rs | 42 +- prover/src/tables/memw_register.rs | 10 +- prover/src/tables/page.rs | 4 +- prover/src/tables/register.rs | 8 +- prover/src/tables/store.rs | 2 +- prover/src/tables/trace_builder.rs | 8 +- prover/src/tables/types.rs | 12 +- prover/src/test_utils.rs | 20 +- .../tests/compute_commit_bus_offset_tests.rs | 73 ++-- prover/src/tests/memw_register_tests.rs | 4 +- prover/src/tests/prove_elfs_tests.rs | 19 +- prover/src/tests/statement_tests.rs | 34 +- 26 files changed, 708 insertions(+), 278 deletions(-) diff --git a/docs/continuations_design.md b/docs/continuations_design.md index 9c3f54747..e0d5fd71e 100644 --- a/docs/continuations_design.md +++ b/docs/continuations_design.md @@ -414,19 +414,39 @@ has no verifier-known final state) and preprocesses 2 columns, not 3. The COMMIT chip's running output index lives in a synthetic single-word register **x254** (word-address 508), so it rides the **same** register binding above — epoch *i*'s `FINI[x254]` becomes epoch *i+1*'s `INIT[x254]`, pinned by the two -locks like any register. Each epoch therefore indexes its committed bytes from the -*carried* value, not from `0`: - -- the COMMIT trace seeds `current_commit_index` from x254 - (`register_state.read_index()` in `trace_builder.rs`), with a debug-assert - pinning the two in sync every step; -- the verifier's commit-bus offset (`compute_commit_bus_offset`'s `start_index`) - starts at the same carried x254. - -The driver concatenates each epoch's committed slice into the run-wide output. -Because every slice is commit-bus-bound *and* the x254 indices are forced -contiguous (`init(i+1) == fini(i)`), the concatenation equals the true output -stream — no separate global "commit output" bus is needed. +locks like any register. The COMMIT trace seeds `current_commit_index` from x254 +(`register_state.read_index()` in `trace_builder.rs`), with a debug-assert pinning +the two in sync every step, so each epoch's committed-byte indices continue the +*carried* global count rather than restarting at `0`. + +COMMIT correctness is a **global** property, closed once over the whole run rather +than per epoch: + +- The COMMIT chip emits each committed byte onto the **Memory** bus (not a + dedicated bus) as `[domain = 2, index, 0, 0, 0, value]`. `domain` is the + RAM/register domain separator (formerly named `is_register`) extended with a third + value (`commit = 2`). COMMIT emits it as the constant `2`; every other Memory-bus + participant fixes the tag to a `{0,1}` value — PAGE/REGISTER/CPU as a constant, and + MEMW/MEMW_ALIGNED pin it to `{0,1}` with an explicit `IS_BIT(domain)` constraint (so + the disjointness is local, not merely a consequence of every `Memw` dispatcher + hardcoding `{0,1}`). Hence a `domain = 2` token can only originate from COMMIT. +- The emit fires **in the global proof, not the epoch proof**. Each epoch's COMMIT + air (`create_commit_air(opts, false)`) carries only the base interactions and + closes to zero; the epoch's COMMIT main-trace root is captured and, in the global + proof, the *same* trace is re-committed under a reduced air (`commit_global_air`, + emit only) — root-bound by `verify_commit_commitment_binding` exactly as + `verify_l2g_commitment_binding` binds the L2G tables. So the emitted tokens are the + epoch's pinned `(index, value)` bytes, inherited via the commitment binding. +- The verifier closes the output bus **once**, in the global proof: + `compute_commit_bus_offset(full_output, z, alpha)` fingerprints the claimed output + at global indices `0..N` and requires the single folded LogUp balance to match. The + run-wide output is absorbed into the global statement before `z`/`alpha` are + sampled. This forces the multiset of emitted `(index, value)` tokens across all + epochs to equal `{(i, full_output[i])}` — pinning length, order, completeness, and + no-splice — so the returned output is **verifier-checked, not driver-trusted**. + +The per-epoch commit-bus close (with its per-epoch `start_index`) and the +driver-trusted slice concatenation are therefore removed. --- diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index ccdd5a6f9..10b802746 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -24,11 +24,16 @@ //! by construction, with the REG-C2 Memory bus binding `FINI` to the true final //! registers. No extra bus. //! -//! The x254 commit index is carried across epochs by that same register binding, -//! so a continuation epoch indexes its commits from the carried value: both the -//! COMMIT trace (`current_commit_index` seeded from x254) and the verifier's -//! `compute_commit_bus_offset` (a `start_index` parameter) count from it, and the -//! driver concatenates each epoch's committed bytes into the run-wide output. +//! The x254 commit index is carried across epochs by that same register binding, so the +//! COMMIT trace indexes its committed bytes from the carried global value (index 0 for the +//! first byte of the run). COMMIT correctness itself is a GLOBAL property: instead of each +//! epoch closing its own output slice, the COMMIT chip emits each byte as a Memory-bus token +//! in the `commit` domain (`domain = 2`), and — like the L2G table — each epoch's COMMIT +//! trace is re-committed in the global proof (root-bound by `verify_commit_commitment_binding`) +//! under a reduced air that carries only that emit. The verifier closes the output bus once, +//! over the whole run's output, via `compute_commit_bus_offset` (indices 0..N). The run-wide +//! output is absorbed into the global statement, so it is verifier-checked (length, order, +//! completeness, no-splice) rather than driver-trusted. //! //! The prover and verifier are split: `prove_continuation` emits a self-contained //! `ContinuationProof` bundle and `verify_continuation` checks it from the bundle @@ -58,8 +63,9 @@ 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, FIXED_TABLE_COUNT, RuntimePageRange, TableCounts, VmAirs, - compute_expected_commit_bus_balance, verify_l2g_commitment_binding, + COMMIT_TABLE_INDEX, Error, FIXED_TABLE_COUNT, RuntimePageRange, TableCounts, VmAirs, + compute_commit_bus_offset, replay_transcript_phase_a, verify_commit_commitment_binding, + verify_l2g_commitment_binding, }; type F = GoldilocksField; @@ -96,11 +102,17 @@ fn epoch_transcript( transcript } -/// Fresh transcript seeded with the global proof's statement (ELF + epoch count). -/// `prove_global` and `verify_global` both seed via this so their challenges match. -fn global_transcript(elf_bytes: &[u8], num_epochs: usize) -> DefaultTranscript { +/// Fresh transcript seeded with the global proof's statement (ELF + epoch count + the +/// run-wide committed output). `prove_global` and `verify_global` both seed via this so their +/// challenges match; absorbing `full_output` binds it to the proof (tampering it diverges the +/// challenges and breaks the output-bus close). +fn global_transcript( + elf_bytes: &[u8], + num_epochs: usize, + full_output: &[u8], +) -> DefaultTranscript { let mut transcript = DefaultTranscript::::new(&[]); - absorb_continuation_global_statement(&mut transcript, elf_bytes, num_epochs); + absorb_continuation_global_statement(&mut transcript, elf_bytes, num_epochs, full_output); transcript } @@ -146,6 +158,28 @@ fn l2g_global_air( ) } +/// Reduced COMMIT AIR for the global proof: carries ONLY the committed-output emit +/// ([`commit::output_bus_interaction`]) on the Memory bus in the `commit` domain. +/// +/// The global proof re-commits each epoch's COMMIT trace under this air; the verifier +/// closes the emitted tokens once, over the whole run's output. Uses `empty_constraints()` +/// for the same reason as [`l2g_global_air`]: the COMMIT trace's `MU`/`END`/`FIRST` bits and +/// the recursion structure that pins the emitted `(index, value)` pairs are enforced in the +/// epoch proof's COMMIT air, and `verify_commit_commitment_binding` ties this sub-table to +/// that *same* committed trace (equal main-trace roots) — so re-asserting them here would be +/// redundant, not a missing check. +fn commit_global_air(opts: &ProofOptions) -> AirWithBuses { + AirWithBuses::new( + crate::tables::commit::cols::NUM_COLUMNS, + AuxiliaryTraceBuildData { + interactions: vec![crate::tables::commit::output_bus_interaction()], + }, + opts, + 1, + empty_constraints(), + ) +} + /// Local-to-global AIR on the epoch-local Memory bus (used inside an epoch proof). /// /// Carries the column range checks and the `init_epoch < fini_epoch` ordering @@ -251,7 +285,9 @@ struct EpochStart<'a> { struct EpochProof { /// The epoch's STARK proof (its tables + the epoch-local L2G sub-table last). proof: MultiProof, - /// Bytes this epoch committed — the COMMIT-bus receiver reference. + /// Bytes this epoch committed. Concatenated in order into the run-wide output, which the + /// GLOBAL proof binds (output-bus close + COMMIT root binding) — so this slice is a data + /// source, not a per-epoch trusted claim. public_output: Vec, /// Statement values the epoch transcript is seeded with (re-derived on verify). table_counts: TableCounts, @@ -268,6 +304,11 @@ struct EpochProof { /// The committed L2G table root, tied to the global proof by /// [`verify_l2g_commitment_binding`]. l2g_root: Commitment, + /// The committed COMMIT table main-trace root, tied to the global proof by + /// [`verify_commit_commitment_binding`]. The global proof re-commits this same COMMIT + /// trace (root-bound here) and emits its output tokens there, so the run-wide output is + /// closed once, globally, instead of per epoch. + commit_root: Commitment, /// Touched-cell boundaries; the verifier rebuilds the global AIRs (touched-page /// set) from these. Values are redundant with the committed L2G trace. boundary: Vec, @@ -316,7 +357,7 @@ fn build_epoch_airs( register::compute_precomputed_commitment_with_fini(opts, register_init, reg_fini), register::NUM_PREPROCESSED_COLS_WITH_FINI, )); - VmAirs::new( + let mut airs = VmAirs::new( elf, opts, false, @@ -327,13 +368,20 @@ fn build_epoch_airs( None, None, register_preprocessed, - ) + ); + // The committed output is closed once in the global proof, not per epoch: rebuild the + // epoch's COMMIT air without the output emit (its base register/memory interactions still + // commit the trace, whose root is re-committed and bound in the global proof). See + // `commit_global_air`. + airs.commit = crate::test_utils::create_commit_air(opts, false); + airs } /// Prove one epoch (prove half only). Commits its local-to-global table (built from /// `boundary`) on the epoch-local Memory bus and its REGISTER table with FINI /// preprocessed to the epoch's final register file. Returns the [`EpochProof`] the -/// standalone verifier later re-checks; does NOT verify here. +/// standalone verifier later re-checks (does NOT verify here) plus this epoch's COMMIT +/// trace, which the caller re-commits in the global proof to close the output bus globally. #[allow(clippy::too_many_arguments)] fn prove_epoch( elf: &Elf, @@ -343,7 +391,7 @@ fn prove_epoch( is_final: bool, boundary: &[CellBoundary], opts: &ProofOptions, -) -> Result { +) -> Result<(EpochProof, TraceTable), Error> { // Count this L2G table's range-check lookups into the BITWISE table so its // AreBytes/IsHalfword multiplicities balance the range-check senders. crate::tables::bitwise::update_multiplicities( @@ -400,6 +448,12 @@ fn prove_epoch( // roots). It is appended to the proof below, not through `air_trace_pairs`. let mut l2g_trace = local_to_global::generate_local_to_global_trace(boundary); + // Snapshot the COMMIT main trace BEFORE proving: `multi_prove` appends this epoch's aux + // columns to `traces.commit` in place, but the global proof must re-commit a MAIN-ONLY + // trace (its reduced air generates its own single aux column). The main-trace data — and + // therefore its Merkle root — is identical, so `verify_commit_commitment_binding` matches. + let commit_trace = traces.commit.clone(); + let mut pairs = airs.air_trace_pairs(&mut traces); pairs.push((&l2g_air, &mut l2g_trace, &())); let proof = Prover::multi_prove( @@ -418,16 +472,30 @@ fn prove_epoch( })? .lde_trace_main_merkle_root; - Ok(EpochProof { - proof, - public_output, - table_counts, - num_private_input_pages, - runtime_page_ranges, - reg_fini, - l2g_root, - boundary: boundary.to_vec(), - }) + // The COMMIT table sits at a fixed position; its main-trace root binds the global + // proof's re-committed copy (whose reduced air emits the output tokens). + let commit_root = proof + .proofs + .get(COMMIT_TABLE_INDEX) + .ok_or_else(|| { + Error::ContinuationInvariant("epoch proof is missing the COMMIT sub-table".to_string()) + })? + .lde_trace_main_merkle_root; + + Ok(( + EpochProof { + proof, + public_output, + table_counts, + num_private_input_pages, + runtime_page_ranges, + reg_fini, + l2g_root, + commit_root, + boundary: boundary.to_vec(), + }, + commit_trace, + )) } /// Verify one epoch using ONLY the [`EpochProof`] bundle plus the verifier-derived @@ -489,45 +557,53 @@ fn verify_epoch( ) }; - // Start the commit index from the carried x254 (the derived INIT), not a free - // input — this is what binds the per-epoch commit slice to its global position. - let commit_start_index = register_init - .get(register::X254_INDEX) - .copied() - .unwrap_or(0) as u64; - - let expected = match compute_expected_commit_bus_balance( - &refs, - &epoch.proof, - &epoch.public_output, - commit_start_index, - &mut seed(), - ) { - Some(expected) => expected, - None => return false, - }; - - if !Verifier::multi_verify(&refs, &epoch.proof, &mut seed(), &expected) { + // The epoch's COMMIT air does not emit the output token (it is carried to the global + // proof and closed there), so the epoch's bus closes to zero — no per-epoch commit + // offset. The output's correctness is bound globally: `verify_commit_commitment_binding` + // + the global output-bus close over the full run-wide output. + if !Verifier::multi_verify(&refs, &epoch.proof, &mut seed(), &FieldElement::zero()) { return false; } // The claimed L2G root must be the one this proof actually committed (it is what // verify_l2g_commitment_binding later ties to the global proof). - epoch + let l2g_root_ok = epoch .proof .proofs .last() .map(|p| p.lde_trace_main_merkle_root) - == Some(epoch.l2g_root) + == Some(epoch.l2g_root); + + // Likewise the claimed COMMIT root must be the one THIS epoch proof committed — the trace + // whose `mu`/`end`/`index`/`value` columns the epoch's constraints pinned. Without this + // anchor, `epoch.commit_root` is a free bundle value tied only to the (also prover-supplied) + // global proof, so a prover could put a fabricated trace's root here, re-commit that fake + // (unconstrained, `commit_global_air`) trace in the global proof, and forge the output while + // every other check passes. Mirrors the `l2g_root` anchor above. + let commit_root_ok = epoch + .proof + .proofs + .get(COMMIT_TABLE_INDEX) + .map(|p| p.lde_trace_main_merkle_root) + == Some(epoch.commit_root); + + l2g_root_ok && commit_root_ok } -/// Build the cross-epoch global memory proof: every epoch's L2G sub-table on the -/// GlobalMemory bus, plus one GLOBAL_MEMORY table per touched page that sends each -/// cell's genesis init (preprocessed from the ELF, so the verifier recomputes it) -/// and receives its final value. The bus balances iff every `fini` matches the next -/// epoch's `init` and every genesis value matches the ELF. +/// Build the cross-epoch global proof. It commits, in this order: +/// 1. every epoch's L2G sub-table on the GlobalMemory bus (cross-epoch memory linkage); +/// 2. every epoch's COMMIT sub-table under the reduced [`commit_global_air`], which emits +/// the committed-output tokens (the run-wide output bus); +/// 3. one GLOBAL_MEMORY table per touched page, sending each cell's genesis init +/// (preprocessed from the ELF) and receiving its final value. +/// +/// The GlobalMemory bus balances iff every `fini` matches the next epoch's `init` and every +/// genesis matches the ELF; the output bus is closed by the verifier's receiver over the +/// claimed `full_output` (which is absorbed into the global statement here). fn prove_global( boundaries: &[Vec], + commit_traces: &mut [TraceTable], + full_output: &[u8], elf_bytes: &[u8], init_page_data: &HashMap>, opts: &ProofOptions, @@ -561,6 +637,11 @@ fn prove_global( let l2g_airs: Vec<_> = (0..boundaries.len()) .map(|i| l2g_global_air(opts, local_to_global::epoch_label(i as u64))) .collect(); + // One reduced COMMIT air per epoch (all identical; the emitted tokens come from the + // re-committed trace). Order/count must match the epochs so the roots bind. + let commit_airs: Vec<_> = (0..commit_traces.len()) + .map(|_| commit_global_air(opts)) + .collect(); let gm_airs: Vec<_> = gm_configs .iter() .map(|config| global_memory_air(opts, config)) @@ -571,13 +652,16 @@ fn prove_global( .zip(l2g_traces.iter_mut()) .map(|(air, t)| (air as AirRef, t, &())) .collect(); + for (air, trace) in commit_airs.iter().zip(commit_traces.iter_mut()) { + pairs.push((air as AirRef, trace, &())); + } for (air, trace) in gm_airs.iter().zip(gm_traces.iter_mut()) { pairs.push((air as AirRef, trace, &())); } Prover::multi_prove( pairs, - &mut global_transcript(elf_bytes, boundaries.len()), + &mut global_transcript(elf_bytes, boundaries.len(), full_output), #[cfg(feature = "disk-spill")] stark::storage_mode::StorageMode::Ram, ) @@ -587,6 +671,7 @@ fn prove_global( fn verify_global( boundaries: &[Vec], proof: &MultiProof, + full_output: &[u8], elf: &Elf, elf_bytes: &[u8], private_inputs: &[u8], @@ -597,6 +682,10 @@ fn verify_global( let l2g_airs: Vec<_> = (0..boundaries.len()) .map(|i| l2g_global_air(opts, local_to_global::epoch_label(i as u64))) .collect(); + // One reduced COMMIT air per epoch — same order/count as `prove_global`. + let commit_airs: Vec<_> = (0..boundaries.len()) + .map(|_| commit_global_air(opts)) + .collect(); // Rebuild the genesis configs FROM THE ELF and recompute their commitments: // this is the binding — a prover that claimed different genesis values would // commit a different root and fail to verify. @@ -606,19 +695,52 @@ fn verify_global( .map(|config| global_memory_air(opts, config)) .collect(); + // Order must match `prove_global`: L2G, then COMMIT, then GLOBAL_MEMORY. let mut refs: Vec = l2g_airs.iter().map(|a| a as AirRef).collect(); + for air in &commit_airs { + refs.push(air as AirRef); + } for air in &gm_airs { refs.push(air as AirRef); } + // The global proof closes two things via one scalar bus balance (all interactions fold + // into one LogUp sum): the GlobalMemory bus (telescopes to 0) and the committed-output + // bus (the verifier's receiver over the claimed full output). So the expected balance is + // 0 + the output offset. Recover (z, alpha) by replaying the global proof's Phase A over + // the same statement-seeded transcript the multi_verify below uses. + let mut replay_transcript = global_transcript(elf_bytes, boundaries.len(), full_output); + let expected = match compute_commit_bus_offset_via_replay( + &refs, + proof, + full_output, + &mut replay_transcript, + ) { + Some(expected) => expected, + None => return false, + }; + Verifier::multi_verify( &refs, proof, - &mut global_transcript(elf_bytes, boundaries.len()), - &FieldElement::zero(), + &mut global_transcript(elf_bytes, boundaries.len(), full_output), + &expected, ) } +/// Recover (z, alpha) from the global proof's Phase-A replay and compute the committed-output +/// bus offset over `full_output`. Factored out so the transcript fork mirrors the monolithic +/// path (`compute_expected_commit_bus_balance`). +fn compute_commit_bus_offset_via_replay( + refs: &[AirRef], + proof: &MultiProof, + full_output: &[u8], + transcript: &mut DefaultTranscript, +) -> Option> { + let (z, alpha) = replay_transcript_phase_a(refs, proof, transcript); + compute_commit_bus_offset(full_output, &z, &alpha) +} + /// Prove a full continuation and return a self-contained [`ContinuationProof`] /// (prove half only — no verification). Splits the execution into `2^epoch_size_log2` /// cycle epochs, proves each, and proves the one cross-epoch global-memory linkage. @@ -661,6 +783,9 @@ pub fn prove_continuation( local_to_global::genesis_provenance(image.iter().map(|(a, v)| (a, v as u64))); let mut epochs: Vec = Vec::new(); + // Each epoch's COMMIT trace, retained so the global proof can re-commit them and close + // the output bus once, globally (see `prove_global`). + let mut commit_traces: Vec> = Vec::new(); // The previous epoch's bound final register file R_{i+1}; epoch i+1's init is // derived from it (the cross-epoch register binding). let mut prev_fini: Option> = None; @@ -733,7 +858,8 @@ pub fn prove_continuation( register_init: ®ister_init, label, }; - let epoch = prove_epoch(&elf, elf_bytes, &start, traces, is_final, &boundary, opts)?; + let (epoch, commit_trace) = + prove_epoch(&elf, elf_bytes, &start, traces, is_final, &boundary, opts)?; prev_fini = Some(epoch.reg_fini.clone()); // Carry the image forward: this epoch's fini is the next epoch's init. @@ -741,6 +867,7 @@ pub fn prove_continuation( image.set(cell.address, (cell.fini.value & 0xFF) as u8); } epochs.push(epoch); + commit_traces.push(commit_trace); if is_final { break; @@ -748,10 +875,26 @@ pub fn prove_continuation( index += 1; } - // One global LogUp over all the (kept) local-to-global tables. + // The run-wide committed output, aggregated in epoch order. The global proof binds it + // (both its value, absorbed into the global statement, and that it equals the union of + // the re-committed COMMIT tables' emitted tokens), so it is verifier-checked rather than + // driver-trusted. + let full_output: Vec = epochs + .iter() + .flat_map(|e| e.public_output.iter().copied()) + .collect(); + + // One global LogUp over all the (kept) local-to-global tables and COMMIT tables. let all_boundaries: Vec> = epochs.iter().map(|e| e.boundary.clone()).collect(); - let global = prove_global(&all_boundaries, elf_bytes, &init_page_data, opts)?; + let global = prove_global( + &all_boundaries, + &mut commit_traces, + &full_output, + elf_bytes, + &init_page_data, + opts, + )?; Ok(ContinuationProof { epochs, @@ -811,6 +954,7 @@ pub fn verify_continuation( // Derived from the ELF for epoch 0, then from each epoch's bound fini. let mut register_init = register::register_init_from_entry_point(elf.entry_point); let mut epoch_roots: Vec = Vec::with_capacity(n); + let mut commit_roots: Vec = Vec::with_capacity(n); let mut public_output: Vec = Vec::new(); for (index, epoch) in bundle.epochs.iter().enumerate() { @@ -830,19 +974,25 @@ pub fn verify_continuation( } epoch_roots.push(epoch.l2g_root); + commit_roots.push(epoch.commit_root); + // The aggregate output; its correctness is enforced globally below (the global + // output-bus close over exactly these bytes + the COMMIT root binding), so this is + // no longer a driver-trusted concatenation. public_output.extend_from_slice(&epoch.public_output); // Next epoch's init is this epoch's bound fini — the cross-epoch register // (and x254) binding. A mismatched fini desyncs the next epoch's AIRs. register_init = epoch.reg_fini.clone(); } - // Cross-epoch global memory: genesis rebuilt FROM THE ELF (+ private inputs), - // so the starting memory cannot be prover-chosen; the bus telescopes fini→init. + // Cross-epoch global memory: genesis rebuilt FROM THE ELF (+ private inputs), so the + // starting memory cannot be prover-chosen (the bus telescopes fini→init). The same proof + // also closes the committed-output bus against `public_output` (bound into its statement). let all_boundaries: Vec> = bundle.epochs.iter().map(|e| e.boundary.clone()).collect(); if !verify_global( &all_boundaries, &bundle.global, + &public_output, &elf, elf_bytes, &bundle.private_inputs, @@ -856,6 +1006,14 @@ pub fn verify_continuation( return Ok(None); } + // Each epoch's committed COMMIT table is the same one the global proof re-committed and + // emitted output tokens from. The COMMIT sub-tables follow the `n` L2G sub-tables in the + // global proof, so they start at offset `n`. This ties the globally-closed output to the + // epochs' pinned COMMIT traces. + if !verify_commit_commitment_binding(&commit_roots, &bundle.global, n) { + return Ok(None); + } + Ok(Some(public_output)) } @@ -1215,4 +1373,133 @@ mod tests { .is_none() ); } + + // Negative: corrupting an epoch's claimed COMMIT table root must be rejected — + // `verify_commit_commitment_binding` compares each epoch's `commit_root` against the + // corresponding re-committed COMMIT sub-proof root in the global proof (at offset `n`), + // so a mismatch breaks the binding. Guards the COMMIT root↔global commitment binding, + // which is what ties the globally-closed output to the epochs' pinned COMMIT traces. + #[test] + fn test_split_verify_rejects_tampered_commit_root() { + let _ = env_logger::builder().is_test(true).try_init(); + // `test_commit_split` actually commits bytes, so the COMMIT trace is non-trivial. + let elf_bytes = asm_elf_bytes("test_commit_split"); + let mut bundle = + prove_continuation(&elf_bytes, &[], 4, &ProofOptions::default_test_options()).unwrap(); + assert!(bundle.num_epochs() > 1, "need multiple epochs"); + bundle.epochs[0].commit_root[0] ^= 0xFF; + assert!( + verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()) + .unwrap() + .is_none(), + "a tampered COMMIT root must break verify_commit_commitment_binding" + ); + } + + // Negative (the load-bearing one): `commit_root` must be anchored to the epoch proof's OWN + // COMMIT trace, not merely be internally consistent with the global proof. Here we rebuild + // the global proof over structurally-different COMMIT traces (built from the honest output + // ops, so the global bus still closes against the true output) whose Merkle roots differ + // from the epochs' real COMMIT traces, and repoint every `commit_root` at those. The global + // binding (`verify_commit_commitment_binding`) is then internally consistent — so ONLY the + // per-epoch `verify_epoch` anchor (`commit_root == proofs[COMMIT_TABLE_INDEX]`) can reject + // it. If that anchor is removed, a prover could likewise re-commit *fabricated* traces + // emitting a FORGED output and have it accepted; this test fails closed on that regression. + #[test] + fn test_split_verify_rejects_commit_root_not_anchored_to_epoch() { + use crate::tables::commit::{CommitOperation, generate_commit_trace}; + + let _ = env_logger::builder().is_test(true).try_init(); + let elf_bytes = asm_elf_bytes("test_commit_split"); + let opts = ProofOptions::default_test_options(); + let mut bundle = prove_continuation(&elf_bytes, &[], 4, &opts).unwrap(); + let n = bundle.epochs.len(); + assert!(n > 1, "need multiple epochs"); + + // Baseline: honest bundle verifies to the true output. + let full_output = verify_continuation(&elf_bytes, &bundle, &opts) + .unwrap() + .expect("honest bundle must verify"); + + // Rebuild the global proof over alternate COMMIT traces that emit the SAME output tokens + // (one op per committed byte at its true global index) but have a different layout → + // different roots. `commit_global_air` has `empty_constraints`, so only the emitted + // tokens matter for the global bus, and they still equal `{(i, full_output[i])}`. + let elf = Elf::load(&elf_bytes).unwrap(); + let image = build_initial_image_paged(&elf, &[]); + let init_page_data = build_init_page_data(&image); + let boundaries: Vec> = + bundle.epochs.iter().map(|e| e.boundary.clone()).collect(); + + let mut global_index: u64 = 0; + let mut alt_traces: Vec> = Vec::with_capacity(n); + for epoch in &bundle.epochs { + let ops: Vec = epoch + .public_output + .iter() + .enumerate() + .map(|(k, &value)| CommitOperation { + timestamp: 0, + index: global_index + k as u64, + address: 0, + count: 1, + first: k == 0, + end: false, + value, + }) + .collect(); + global_index += epoch.public_output.len() as u64; + alt_traces.push(generate_commit_trace(&ops)); + } + + let alt_global = prove_global( + &boundaries, + &mut alt_traces, + &full_output, + &elf_bytes, + &init_page_data, + &opts, + ) + .unwrap(); + + // Repoint each commit_root at the alternate global's re-committed roots (offset n) and + // swap in the alternate global proof, so the global binding stays internally consistent. + for (i, epoch) in bundle.epochs.iter_mut().enumerate() { + epoch.commit_root = alt_global.proofs[n + i].lde_trace_main_merkle_root; + } + bundle.global = alt_global; + + assert!( + verify_continuation(&elf_bytes, &bundle, &opts) + .unwrap() + .is_none(), + "a commit_root not anchored to the epoch's own COMMIT trace must be rejected" + ); + } + + // Negative: tampering an epoch's committed output bytes must be rejected. The output is + // only bound globally now (the epoch no longer closes its own commit slice), but the + // tampered slice also diverges the epoch's own statement-seeded transcript — either way + // the run must fail to verify, and the aggregate the verifier returns can never be a + // forged output. + #[test] + fn test_split_verify_rejects_tampered_output() { + let _ = env_logger::builder().is_test(true).try_init(); + let elf_bytes = asm_elf_bytes("test_commit_split"); + let mut bundle = + prove_continuation(&elf_bytes, &[], 4, &ProofOptions::default_test_options()).unwrap(); + // Find an epoch that actually committed a byte and flip it. + let epoch = bundle + .epochs + .iter_mut() + .find(|e| !e.public_output.is_empty()) + .expect("some epoch must commit a byte in test_commit_split"); + epoch.public_output[0] ^= 0xFF; + assert!( + verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()) + .unwrap() + .is_none(), + "a tampered committed byte must not verify to a forged output" + ); + } } diff --git a/prover/src/lib.rs b/prover/src/lib.rs index 760383003..8518721bc 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -80,6 +80,13 @@ pub struct RuntimePageRange { /// keccak_rc, register, ecsm, ec_scalar, ecdas. pub const FIXED_TABLE_COUNT: usize = 11; +/// Fixed position of the COMMIT sub-proof within a proof's `proofs` vector. The +/// always-present tables are committed in a fixed order (see `VmAirs::air_trace_pairs` / +/// `air_refs`): bitwise (0), decode (1), commit (2), … So the COMMIT table's main-trace +/// Merkle root is always `proof.proofs[COMMIT_TABLE_INDEX]`. Used by the continuation +/// prover to capture each epoch's COMMIT root for the global commitment binding. +pub(crate) const COMMIT_TABLE_INDEX: usize = 2; + /// Number of chunks for each split table. /// The verifier needs this to reconstruct matching AIRs. #[derive(Debug, Clone, serde::Serialize, serde::Deserialize)] @@ -495,7 +502,10 @@ impl VmAirs { .map(|i| create_branch_air(proof_options).with_name(&format!("BRANCH[{}]", i))) .collect(); let halt = create_halt_air(proof_options); - let commit = create_commit_air(proof_options); + // Emit the committed-output token in-proof by default (monolithic path). Continuation + // epochs override `commit` with an emit-free air (the output is carried to and closed + // in the global proof); see `continuation::build_epoch_airs`. + let commit = create_commit_air(proof_options, true); let keccak = create_keccak_air(proof_options); let keccak_rnd = create_keccak_rnd_air(proof_options); let keccak_rc = create_keccak_rc_air(proof_options).with_preprocessed( @@ -627,19 +637,24 @@ pub(crate) fn replay_transcript_phase_a( (z, alpha) } -/// Compute the bus balance offset for the COMMIT[index, value] bus. +/// Compute the bus balance offset for the COMMIT output on the Memory bus. /// -/// For each public output byte at index `i` with value `v`: -/// `fingerprint = z - (BusId::Commit * α^0 + i * α^1 + v * α^2)` +/// The COMMIT chip emits each committed byte as a Memory-bus token in the `commit` +/// domain (`domain = 2`); see [`tables::commit::output_bus_interaction`]. For the +/// public output byte at global index `i` with value `v`, that token is +/// `[domain = 2, addr_lo = i, addr_hi = 0, ts_lo = 0, ts_hi = 0, value = v]`, whose +/// fingerprint (bus_id at α⁰, then values at α¹, α², …) is: +/// `fingerprint = z - (BusId::Memory + 2·α + i·α² + v·α⁶)` /// `term = +1 / fingerprint` /// -/// Returns `Some(Σ term)` — the positive receiver contribution that is no -/// longer present as an in-trace table. For empty public output, returns -/// `Some(zero)`. Returns `None` on a fingerprint collision (zero divisor), -/// which the caller should treat as verification failure. +/// Returns `Some(Σ term)` — the positive receiver contribution the verifier supplies for +/// the emitted output tokens (there is no in-trace receiver). Indices are the run-global +/// 0-based commit indices, matching the x254 counter: `0` for the first committed byte, +/// so no `start_index` offset is needed (a monolithic proof and a whole continuation both +/// index from 0). For empty output, returns `Some(zero)`. Returns `None` on a fingerprint +/// collision (zero divisor), which the caller treats as verification failure. pub(crate) fn compute_commit_bus_offset( public_output: &[u8], - start_index: u64, z: &FieldElement, alpha: &FieldElement, ) -> Option> { @@ -647,20 +662,22 @@ pub(crate) fn compute_commit_bus_offset( return Some(FieldElement::zero()); } - let bus_id = FieldElement::::from(BusId::Commit as u64); + let bus_id = FieldElement::::from(BusId::Memory as u64); + // α² (index/addr_lo coefficient) and α⁶ (value coefficient); the addr_hi/ts_lo/ts_hi + // slots (α³..α⁵) are constant 0 in the commit token, so they drop out. let alpha_sq = alpha * alpha; + let alpha_pow6 = &alpha_sq * &alpha_sq * &alpha_sq; + // Constant part of the linear combination: BusId::Memory + 2·α (domain = 2). + let domain_term = &bus_id + (FieldElement::::from(2u64) * alpha); - // fingerprint_i = z - (BusId::Commit + (start_index + i)·α + value_i·α²). - // `start_index` is the carried x254: 0 for a monolithic proof or the first - // epoch, nonzero for a continuation epoch whose commits continue a prior one. + // fingerprint_i = z - (BusId::Memory + 2·α + i·α² + value_i·α⁶). let mut fingerprints: Vec> = public_output .iter() .enumerate() .map(|(i, &value)| { - let global_index = start_index + i as u64; - let linear_combination = bus_id - + (FieldElement::::from(global_index) * alpha) - + (FieldElement::::from(value as u64) * alpha_sq); + let linear_combination = &domain_term + + (FieldElement::::from(i as u64) * &alpha_sq) + + (FieldElement::::from(value as u64) * &alpha_pow6); z - linear_combination }) .collect(); @@ -678,18 +695,20 @@ pub(crate) fn compute_commit_bus_offset( /// Compute the expected COMMIT bus balance for a `MultiProof`. /// -/// Replays Phase A of the transcript to recover (z, alpha), then computes -/// the offset from the given public output bytes. Call this after `multi_prove` -/// and before `multi_verify`. +/// Replays Phase A of the transcript to recover (z, alpha), then computes the offset from +/// the given public output bytes. Commit indices are run-global 0-based (the x254 counter), +/// so no start offset is needed. Used by the monolithic verifier (the whole output is closed +/// in-proof) and by the continuation global verifier (the whole run's output is closed once, +/// over the re-committed COMMIT tables). Call this after `multi_prove` and before +/// `multi_verify`. pub(crate) fn compute_expected_commit_bus_balance( airs: &[&dyn AIR], proof: &MultiProof, public_output_bytes: &[u8], - start_index: u64, transcript: &mut DefaultTranscript, ) -> Option> { let (z, alpha) = replay_transcript_phase_a(airs, proof, transcript); - compute_commit_bus_offset(public_output_bytes, start_index, &z, &alpha) + compute_commit_bus_offset(public_output_bytes, &z, &alpha) } /// Bind the final cross-epoch GlobalMemory proof to the per-epoch proofs. @@ -713,6 +732,30 @@ pub(crate) fn verify_l2g_commitment_binding( .all(|(i, root)| final_proof.proofs[i].lde_trace_main_merkle_root == *root) } +/// Bind the global proof's re-committed COMMIT sub-tables to the per-epoch proofs. +/// +/// The global proof re-commits each epoch's COMMIT trace (under the reduced +/// `commit_global_air`, which carries only the output emit) at positions +/// `[offset, offset + N)` — after the `offset` local-to-global sub-tables. So +/// `final_proof.proofs[offset + i].lde_trace_main_merkle_root` must equal epoch `i`'s own +/// COMMIT root (`epoch_commit_roots[i]`). Equal roots prove the global output bus ran over +/// the very same COMMIT tables the epochs committed — so the pinned `MU`/`END`/`FIRST` +/// multiplicities (enforced in the epoch proof) carry over, exactly as +/// [`verify_l2g_commitment_binding`] inherits the L2G column pinning. +/// +/// Called by `continuation::verify_continuation`. +pub(crate) fn verify_commit_commitment_binding( + epoch_commit_roots: &[Commitment], + final_proof: &MultiProof, + offset: usize, +) -> bool { + final_proof.proofs.len() >= offset + epoch_commit_roots.len() + && epoch_commit_roots + .iter() + .enumerate() + .all(|(i, root)| final_proof.proofs[offset + i].lde_trace_main_merkle_root == *root) +} + // ============================================================================= // Public API: Prove / Verify // ============================================================================= @@ -1035,8 +1078,6 @@ pub fn verify_with_options( &air_refs, &vm_proof.proof, &vm_proof.public_output, - // Monolithic proof: commits are indexed from 0. - 0, &mut transcript_for_replay, ) { Some(balance) => balance, diff --git a/prover/src/statement.rs b/prover/src/statement.rs index cca961be5..2184a58f8 100644 --- a/prover/src/statement.rs +++ b/prover/src/statement.rs @@ -123,15 +123,21 @@ const CONTINUATION_EPOCH_TAG: &[u8] = b"LAMBDAVM_CONTINUATION_EPOCH_V1"; const CONTINUATION_GLOBAL_TAG: &[u8] = b"LAMBDAVM_CONTINUATION_GLOBAL_V1"; /// Statement bound into the cross-epoch **global** proof's transcript before -/// Phase A: the ELF (so the global proof is program-bound) and the epoch count +/// Phase A: the ELF (so the global proof is program-bound), the epoch count /// (so a global proof from a run with a different number of epochs cannot be -/// spliced in). Prove and verify must call this with identical arguments. +/// spliced in), and the run-wide committed output (length-prefixed) — so the output the +/// verifier closes the commit bus against is itself bound to the proof's challenges, and a +/// tampered output diverges every derived challenge. Prove and verify must call this with +/// identical arguments. pub(crate) fn absorb_continuation_global_statement( t: &mut impl IsTranscript, elf_bytes: &[u8], num_epochs: usize, + full_output: &[u8], ) { t.append_bytes(CONTINUATION_GLOBAL_TAG); t.append_bytes(&elf_digest(elf_bytes)); t.append_bytes(&(num_epochs as u64).to_le_bytes()); + t.append_bytes(&(full_output.len() as u64).to_le_bytes()); + t.append_bytes(full_output); } diff --git a/prover/src/tables/commit.rs b/prover/src/tables/commit.rs index c1663711e..7148fa4cf 100644 --- a/prover/src/tables/commit.rs +++ b/prover/src/tables/commit.rs @@ -19,7 +19,7 @@ //! - `value`: Byte — the byte being committed //! - `mu`: Bit — multiplicity (1 for real rows, 0 for padding) //! -//! ## Bus Interactions (18 total) +//! ## Bus Interactions (17 base + 1 output emit) //! - **Receiver**: Ecall bus — receives `[timestamp_lo, timestamp_hi, constant(64), constant(0)]` from CPU (mult = first) //! - **Sender**: CommitNextByte bus — sends to next row (mult = mu - end) //! - **Receiver**: CommitNextByte bus — receives from prev row (mult = mu - first) @@ -31,7 +31,17 @@ //! - **Sender**: Memw bus — read x12 register (count) at ts (mult = first) //! - **Sender**: Memw bus — read+write x254 commit index at ts (mult = first) //! - **Sender**: Memw bus — read memory byte at ts (mult = mu - end) -//! - **Sender**: Commit bus — sends committed `(index, value)` pairs (mult = mu - end) +//! +//! The above 17 interactions are the "base" set ([`bus_interactions`]); they close +//! within a single proof (Memw reads/writes, the CommitNextByte chain, range checks). +//! +//! The committed output itself is emitted separately by [`output_bus_interaction`]: +//! - **Sender**: Memory bus — `[domain = 2 (commit domain), index, 0, 0, 0, value]` +//! (mult = mu - end). This is the token the verifier closes against the claimed public +//! output. It rides the shared Memory bus under the `domain` domain separator +//! (`RAM = 0`, `register = 1`, `commit = 2`) instead of a dedicated bus, so that the +//! continuation prover can carry it up to the global proof and close it once, globally, +//! over the whole output — the same root-binding move as the local-to-global table. //! //! ## Constraints (8 total) //! - `range_first`: first * (1 - first) = 0 (degree 2) @@ -227,7 +237,11 @@ pub fn generate_commit_trace( // Bus interactions // ========================================================================= -/// Creates all bus interactions for the COMMIT table (18 total). +/// Creates the base bus interactions for the COMMIT table (17 total). +/// +/// These are the interactions that close within a single proof. The committed +/// output token is NOT here — it is emitted separately by [`output_bus_interaction`] +/// so a continuation prover can carry it up to the global proof (see that function). /// /// The COMMIT table: /// - **Receives** Ecall from CPU with `[timestamp_lo, timestamp_hi, constant(64), constant(0)]` (mult = first) @@ -431,7 +445,7 @@ pub fn bus_interactions() -> Vec { ], ), // 13. MEMW read+write x10 (fd=1 → count) at ts (mult = first) - // CO24 format: [old[8], is_register, base_addr[2], value[8], ts[2], w2, w4, w8] + // CO24 format: [old[8], domain, base_addr[2], value[8], ts[2], w2, w4, w8] // old = [1,0,...,0] (asserts x10=1=fd), value = [count_0, count_1, 0,...,0] (writes count) BusInteraction::sender( BusId::Memw, @@ -446,7 +460,7 @@ pub fn bus_interactions() -> Vec { BusValue::constant(0), BusValue::constant(0), BusValue::constant(0), - // is_register = 1 + // domain = 1 BusValue::constant(1), // base_address = [20, 0] (x10 → addr 2*10 = 20) BusValue::constant(20), @@ -501,7 +515,7 @@ pub fn bus_interactions() -> Vec { BusValue::constant(0), BusValue::constant(0), BusValue::constant(0), - // is_register = 1 + // domain = 1 BusValue::constant(1), // base_address = [22, 0] (x11 → addr 2*11 = 22) BusValue::constant(22), @@ -556,7 +570,7 @@ pub fn bus_interactions() -> Vec { BusValue::constant(0), BusValue::constant(0), BusValue::constant(0), - // is_register = 1 + // domain = 1 BusValue::constant(1), // base_address = [24, 0] (x12 → addr 2*12 = 24) BusValue::constant(24), @@ -609,7 +623,7 @@ pub fn bus_interactions() -> Vec { BusValue::constant(0), BusValue::constant(0), BusValue::constant(0), - // is_register = 1 + // domain = 1 BusValue::constant(1), // base_address = [508, 0] BusValue::constant(508), @@ -669,7 +683,7 @@ pub fn bus_interactions() -> Vec { BusValue::constant(0), BusValue::constant(0), BusValue::constant(0), - // is_register = 0 + // domain = 0 BusValue::constant(0), // base_address = [ADDRESS_0, ADDRESS_1] BusValue::Packed { @@ -707,24 +721,54 @@ pub fn bus_interactions() -> Vec { BusValue::constant(0), ], ), - // 18. COMMIT[index, value] (mult = mu - end) - BusInteraction::sender( - BusId::Commit, - mu_minus_end, - vec![ - BusValue::Packed { - start_column: cols::INDEX, - packing: Packing::Direct, - }, - BusValue::Packed { - start_column: cols::VALUE, - packing: Packing::Direct, - }, - ], - ), ] } +/// The COMMIT output emit: one Memory-bus token per committed byte (mult = mu - end). +/// +/// Token `[domain = 2, addr_lo = index, addr_hi = 0, ts_lo = 0, ts_hi = 0, value]`. +/// The `domain` field is the Memory-bus domain separator, extended to a third value +/// (`RAM = 0`, `register = 1`, `commit = 2`); `domain` carries no boolean/range +/// constraint, so no new AIR constraint is needed — domain disjointness comes from the +/// commit token only ever being closed by the verifier's output receiver, never aliasing a +/// RAM/register cell (whose chains are closed by their own PAGE/REGISTER bookends). +/// +/// `index` (the global commit index carried in x254) rides in the address_lo slot: since +/// commit tokens are domain-disjoint and never matched against real addresses, it is a pure +/// identifier and need not be a valid 32-bit word. There is no timestamp (commit output is +/// append-only, ordered by `index`, not by memory timestamp). +/// +/// This token is emitted: +/// - in a **monolithic** proof, alongside the base interactions, closed in-proof by the +/// verifier's `compute_commit_bus_offset` over the whole output; +/// - in a **continuation**, only in the reduced global commit air (NOT the epoch air), so +/// the run-wide output is closed once, globally. +pub fn output_bus_interaction() -> BusInteraction { + BusInteraction::sender( + BusId::Memory, + Multiplicity::Diff(cols::MU, cols::END), + vec![ + // domain = 2 (commit domain separator) + BusValue::constant(2), + // address_lo = index (global commit index) + BusValue::Packed { + start_column: cols::INDEX, + packing: Packing::Direct, + }, + // address_hi = 0 + BusValue::constant(0), + // timestamp_lo = 0, timestamp_hi = 0 (no timestamp: ordered by index) + BusValue::constant(0), + BusValue::constant(0), + // value = committed byte + BusValue::Packed { + start_column: cols::VALUE, + packing: Packing::Direct, + }, + ], + ) +} + // ========================================================================= // Constraints // ========================================================================= diff --git a/prover/src/tables/cpu.rs b/prover/src/tables/cpu.rs index 1752022b9..318c5adcd 100644 --- a/prover/src/tables/cpu.rs +++ b/prover/src/tables/cpu.rs @@ -733,7 +733,7 @@ pub fn bus_interactions() -> Vec { BusId::Memw, Multiplicity::Column(cols::WRITE_REGISTER), vec![ - BusValue::constant(1), // is_register + BusValue::constant(1), // domain BusValue::linear(vec![LinearTerm::Column { coefficient: 2, column: cols::RD, @@ -978,7 +978,7 @@ pub fn bus_interactions() -> Vec { interactions } -/// MEMW register-read interaction (24 elements: `old(8), is_register, base(2), +/// MEMW register-read interaction (24 elements: `old(8), domain, base(2), /// value(8), timestamp(2), w2, w4, w8`). Register values are DWordWL (the two /// value words are read directly; the remaining 6 byte slots are 0). fn memw_register_read( @@ -1023,7 +1023,7 @@ fn memw_register_read( BusValue::constant(0), BusValue::constant(0), BusValue::constant(0), - // is_register = 1 + // domain = 1 BusValue::constant(1), // base_address[0] = 2*rs, base_address[1] = 0 BusValue::linear(vec![LinearTerm::Column { diff --git a/prover/src/tables/cpu32.rs b/prover/src/tables/cpu32.rs index d7dbd5d6f..49b2501f0 100644 --- a/prover/src/tables/cpu32.rs +++ b/prover/src/tables/cpu32.rs @@ -301,7 +301,7 @@ fn timestamp_plus(offset: i64) -> Vec { ] } -/// MEMW register **read** (24 elements: `old == value`, `is_register=1`, `write2=1`). +/// MEMW register **read** (24 elements: `old == value`, `domain=1`, `write2=1`). fn reg_read( rs: usize, lo0: usize, @@ -311,7 +311,7 @@ fn reg_read( mult: usize, ) -> BusInteraction { let mut values = register_dword(lo0, lo1, hi); // old - values.push(BusValue::constant(1)); // is_register + values.push(BusValue::constant(1)); // domain values.push(BusValue::linear(vec![LinearTerm::Column { coefficient: 2, column: rs, @@ -334,7 +334,7 @@ fn reg_write( mult: usize, ) -> BusInteraction { let mut values = vec![ - BusValue::constant(1), // is_register + BusValue::constant(1), // domain BusValue::linear(vec![LinearTerm::Column { coefficient: 2, column: rd, diff --git a/prover/src/tables/ec_scalar.rs b/prover/src/tables/ec_scalar.rs index dd8d483a2..69a32dc2b 100644 --- a/prover/src/tables/ec_scalar.rs +++ b/prover/src/tables/ec_scalar.rs @@ -175,7 +175,7 @@ pub fn bus_interactions() -> Vec { } // 2. MEMW: read byte k[offset] at ptr+offset, timestamp+1, width 1 (mult = mu). - // CO24 layout: [old[8], is_register, base[2], value[8], ts[2], w2, w4, w8]. + // CO24 layout: [old[8], domain, base[2], value[8], ts[2], w2, w4, w8]. { let base_lo = BusValue::linear(vec![ LinearTerm::Column { @@ -208,7 +208,7 @@ pub fn bus_interactions() -> Vec { for _ in 1..8 { values.push(BusValue::constant(0)); } - values.push(BusValue::constant(0)); // is_register = 0 + values.push(BusValue::constant(0)); // domain = 0 values.push(base_lo); values.push(base_hi); // value[0..8]: same as old (read) diff --git a/prover/src/tables/ecsm.rs b/prover/src/tables/ecsm.rs index f8ec0859d..faef8784d 100644 --- a/prover/src/tables/ecsm.rs +++ b/prover/src/tables/ecsm.rs @@ -209,12 +209,12 @@ fn packed(col: usize) -> BusValue { } } -/// `[old[8], is_register, base_lo, base_hi, value[8], ts_lo, ts_hi, w2, w4, w8]` — +/// `[old[8], domain, base_lo, base_hi, value[8], ts_lo, ts_hi, w2, w4, w8]` — /// a 24-element MEMW **read** tuple (`old == value`). #[allow(clippy::too_many_arguments)] fn memw_read( value: [BusValue; 8], - is_register: u64, + domain: u64, base_lo: BusValue, base_hi: BusValue, ts_lo: BusValue, @@ -224,7 +224,7 @@ fn memw_read( ) -> Vec { let mut v = Vec::with_capacity(24); v.extend(value.clone()); // old == value (read) - v.push(BusValue::constant(is_register)); + v.push(BusValue::constant(domain)); v.push(base_lo); v.push(base_hi); v.extend(value); @@ -236,7 +236,7 @@ fn memw_read( v } -/// `[is_register, base_lo, base_hi, value[8], ts_lo, ts_hi, w2, w4, w8]` — +/// `[domain, base_lo, base_hi, value[8], ts_lo, ts_hi, w2, w4, w8]` — /// a 16-element MEMW **write** tuple (MEMW table supplies `old`). fn memw_write( value: [BusValue; 8], @@ -247,7 +247,7 @@ fn memw_write( w8: u64, ) -> Vec { let mut v = Vec::with_capacity(16); - v.push(BusValue::constant(0)); // is_register = 0 (memory) + v.push(BusValue::constant(0)); // domain = 0 (memory) v.push(base_lo); v.push(base_hi); v.extend(value); diff --git a/prover/src/tables/halt.rs b/prover/src/tables/halt.rs index 44bbf26cb..611658e87 100644 --- a/prover/src/tables/halt.rs +++ b/prover/src/tables/halt.rs @@ -87,7 +87,7 @@ pub fn generate_halt_trace( /// Returns the 24-element MEMW read bus values for x10 exit code verification. /// -/// Format matches CO24 (read receiver): `[old[0..7], is_register, base_addr[0..1], +/// Format matches CO24 (read receiver): `[old[0..7], domain, base_addr[0..1], /// value[0..7], timestamp[0..1], write2, write4, write8]`. /// old=0 enforces that x10 was 0 at halt time. fn halt_read_bus_values(base_addr: u64) -> Vec { @@ -102,7 +102,7 @@ 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(1), // domain = 1 BusValue::constant(base_addr), // base_address[0] BusValue::constant(0), // base_address[1] BusValue::constant(0), // value[0] = 0 @@ -123,11 +123,11 @@ fn halt_read_bus_values(base_addr: u64) -> Vec { /// Returns the 16-element MEMW write bus values for a register finalization. /// -/// Format matches CO25 (write receiver): `[is_register, base_addr[0..1], value[0..7], +/// Format matches CO25 (write receiver): `[domain, base_addr[0..1], value[0..7], /// 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(1), // domain = 1 BusValue::constant(base_addr), // base_address[0] BusValue::constant(0), // base_address[1] BusValue::constant(value_lo), // value[0] @@ -209,7 +209,7 @@ pub fn bus_interactions() -> Vec { // its real `next_pc` to x255 (addresses 510/511) at this same timestamp; we // consume it (sender, +1) and re-emit pc=1 (receiver, -1) so the CPU padding // rows — which all carry pc=1 — chain cleanly to the REGISTER final token. - // `value` layout on the bus: [is_register, addr_lo, addr_hi, ts_lo, ts_hi, value]. + // `value` layout on the bus: [domain, addr_lo, addr_hi, ts_lo, ts_hi, value]. let ts_plus_one_lo = || { BusValue::linear(vec![ LinearTerm::Column { diff --git a/prover/src/tables/keccak.rs b/prover/src/tables/keccak.rs index 0f305255b..ce2f85601 100644 --- a/prover/src/tables/keccak.rs +++ b/prover/src/tables/keccak.rs @@ -185,7 +185,7 @@ pub fn bus_interactions() -> Vec { )); // 2. MEMW read_addr: read register x10 to bind addr (per spec keccak:c:read_addr) - // Format: [old[8], is_register=1, base_addr=[20,0], value[8], ts, ts_hi, write2=1, write4=0, write8=0] + // Format: [old[8], domain=1, base_addr=[20,0], value[8], ts, ts_hi, write2=1, write4=0, write8=0] // For register read: old = value = addr as WL + 6 zeros { // addr as DWordWL from DWordBL bytes: lo32 = sum(addr[0..4] * 256^i), hi32 = sum(addr[4..8] * 256^i) @@ -232,7 +232,7 @@ pub fn bus_interactions() -> Vec { for _ in 2..8 { values.push(BusValue::constant(0)); } - // is_register = 1 + // domain = 1 values.push(BusValue::constant(1)); // base_address = 2*10 = 20 (register x10) values.push(BusValue::constant(20)); @@ -381,7 +381,7 @@ pub fn bus_interactions() -> Vec { } // 7. MEMW interactions: 25 combined read+write per lane (per spec) - // Format: [old[8], is_register, addr_lo32, addr_hi32, value[8], ts[2], w2, w4, w8] = 24 + // Format: [old[8], domain, addr_lo32, addr_hi32, value[8], ts[2], w2, w4, w8] = 24 // old = input_state (read), value = output_state (write) for lane_idx in 0..25 { let x = lane_idx % 5; @@ -417,7 +417,7 @@ pub fn bus_interactions() -> Vec { packing: Packing::Direct, }); } - // is_register = 0 + // domain = 0 values.push(BusValue::constant(0)); // address as DWordWL values.push(addr_lo); diff --git a/prover/src/tables/load.rs b/prover/src/tables/load.rs index 250d565b2..fa71a9db9 100644 --- a/prover/src/tables/load.rs +++ b/prover/src/tables/load.rs @@ -236,7 +236,7 @@ pub fn bus_interactions() -> Vec { // ------------------------------------------------------------------------- // MEMW sender (to read memory) - ENABLED // ------------------------------------------------------------------------- - // LOAD calls MEMW with is_register=0, passing res as both value and old + // LOAD calls MEMW with domain=0, passing res as both value and old // (since we're reading, value=old=the read data) // RES columns contain individual bytes, sent as Direct elements // to match the unified MEMW Read receiver format. @@ -278,7 +278,7 @@ pub fn bus_interactions() -> Vec { start_column: cols::RES[7], packing: Packing::Direct, }, - // is_register = 0 (constant) + // domain = 0 (constant) BusValue::constant(0), // base_address (DWordWL = 2 words) BusValue::Packed { diff --git a/prover/src/tables/local_to_global.rs b/prover/src/tables/local_to_global.rs index ada19baf5..80ee496b1 100644 --- a/prover/src/tables/local_to_global.rs +++ b/prover/src/tables/local_to_global.rs @@ -359,8 +359,8 @@ pub fn bus_interactions(epoch_label: u64) -> Vec { /// (the epoch-start seed, matching the first MEMW read's `old_timestamp`) and /// sends its final token at the last access timestamp. This replaces PAGE's /// init/fini bookend for touched bytes. The `Memory` token layout is -/// `[is_register, address_lo, address_hi, timestamp_lo, timestamp_hi, value]`; -/// RAM only, so `is_register = 0`, and the byte value is the LO column. +/// `[domain, address_lo, address_hi, timestamp_lo, timestamp_hi, value]`; +/// RAM only, so `domain = 0`, and the byte value is the LO column. /// /// Address, fini timestamp and the values appear here, so MEMW range-checks them /// for us — they need no L2G range check (see [`range_check_interactions`]). diff --git a/prover/src/tables/memw.rs b/prover/src/tables/memw.rs index 2b240747c..a60e50a07 100644 --- a/prover/src/tables/memw.rs +++ b/prover/src/tables/memw.rs @@ -5,7 +5,7 @@ //! //! ## Column layout (49 columns) //! -//! - `is_register`: Bit (1 = register access, 0 = memory access) +//! - `domain`: Bit (1 = register access, 0 = memory access) //! - `base_address`: DWordWL (64-bit address, 2 cols) //! - `value[8]`: BaseField[8] (8 bytes to write) //! - `timestamp`: DWordWL (64-bit timestamp, 2 cols) @@ -50,8 +50,8 @@ pub const MAX_ROWS: usize = super::max_rows::MEMW; /// Column definitions for the MEMW table. pub mod cols { // Input columns - /// is_register: Bit (1 = register, 0 = memory) - pub const IS_REGISTER: usize = 0; + /// domain: Bit (1 = register, 0 = memory) + pub const DOMAIN: usize = 0; /// base_address: DWordWL (2 words = 2 columns) pub const BASE_ADDRESS_0: usize = 1; @@ -105,7 +105,7 @@ pub mod cols { #[derive(Debug, Clone)] pub struct MemwOperation { /// Whether this is a register access (true) or memory access (false) - pub is_register: bool, + pub domain: bool, /// Base address (64-bit) pub base_address: u64, /// Values to write (8 bytes) @@ -125,7 +125,7 @@ pub struct MemwOperation { impl MemwOperation { /// Create a new MEMW operation. pub fn new( - is_register: bool, + domain: bool, base_address: u64, value: [u64; 8], timestamp: u64, @@ -133,7 +133,7 @@ impl MemwOperation { is_read: bool, ) -> Self { Self { - is_register, + domain, base_address, value, timestamp, @@ -184,7 +184,7 @@ pub fn generate_memw_trace( for (row_idx, op) in operations.iter().enumerate() { // Input columns - table.set_bool(row_idx, cols::IS_REGISTER, op.is_register); + table.set_bool(row_idx, cols::DOMAIN, op.domain); // base_address as DWordWL (2 words) let base_addr_lo = op.base_address & 0xFFFF_FFFF; @@ -259,13 +259,13 @@ pub fn bus_interactions() -> Vec { // produces a memory token at a wrong address that has no matching // PAGE/REGISTER token, causing multiset imbalance and an invalid proof. - // CM8: memory[is_register, base_address, old_timestamp[0], old[0]] with +μ_sum + // CM8: memory[domain, base_address, old_timestamp[0], old[0]] with +μ_sum interactions.push(BusInteraction::sender( BusId::Memory, Multiplicity::Sum(cols::MU_READ, cols::MU_WRITE), vec![ BusValue::Packed { - start_column: cols::IS_REGISTER, + start_column: cols::DOMAIN, packing: Packing::Direct, }, BusValue::Packed { @@ -291,13 +291,13 @@ pub fn bus_interactions() -> Vec { ], )); - // CM9: memory[is_register, base_address, timestamp, value[0]] with -μ_sum + // CM9: memory[domain, base_address, timestamp, value[0]] with -μ_sum interactions.push(BusInteraction::receiver( BusId::Memory, Multiplicity::Sum(cols::MU_READ, cols::MU_WRITE), vec![ BusValue::Packed { - start_column: cols::IS_REGISTER, + start_column: cols::DOMAIN, packing: Packing::Direct, }, BusValue::Packed { @@ -354,7 +354,7 @@ pub fn bus_interactions() -> Vec { Multiplicity::Sum3(cols::WRITE2, cols::WRITE4, cols::WRITE8), vec![ BusValue::Packed { - start_column: cols::IS_REGISTER, + start_column: cols::DOMAIN, packing: Packing::Direct, }, addr_add_0_lo.clone(), @@ -380,7 +380,7 @@ pub fn bus_interactions() -> Vec { Multiplicity::Sum3(cols::WRITE2, cols::WRITE4, cols::WRITE8), vec![ BusValue::Packed { - start_column: cols::IS_REGISTER, + start_column: cols::DOMAIN, packing: Packing::Direct, }, addr_add_0_lo, @@ -431,7 +431,7 @@ pub fn bus_interactions() -> Vec { Multiplicity::Sum(cols::WRITE4, cols::WRITE8), vec![ BusValue::Packed { - start_column: cols::IS_REGISTER, + start_column: cols::DOMAIN, packing: Packing::Direct, }, addr_add_lo.clone(), @@ -457,7 +457,7 @@ pub fn bus_interactions() -> Vec { Multiplicity::Sum(cols::WRITE4, cols::WRITE8), vec![ BusValue::Packed { - start_column: cols::IS_REGISTER, + start_column: cols::DOMAIN, packing: Packing::Direct, }, addr_add_lo, @@ -509,7 +509,7 @@ pub fn bus_interactions() -> Vec { Multiplicity::Column(cols::WRITE8), vec![ BusValue::Packed { - start_column: cols::IS_REGISTER, + start_column: cols::DOMAIN, packing: Packing::Direct, }, addr_add_lo.clone(), @@ -535,7 +535,7 @@ pub fn bus_interactions() -> Vec { Multiplicity::Column(cols::WRITE8), vec![ BusValue::Packed { - start_column: cols::IS_REGISTER, + start_column: cols::DOMAIN, packing: Packing::Direct, }, addr_add_lo, @@ -596,9 +596,9 @@ pub fn bus_interactions() -> Vec { start_column: cols::OLD[7], packing: Packing::Direct, }, - // is_register + // domain BusValue::Packed { - start_column: cols::IS_REGISTER, + start_column: cols::DOMAIN, packing: Packing::Direct, }, // base_address @@ -675,9 +675,9 @@ pub fn bus_interactions() -> Vec { BusId::Memw, Multiplicity::Column(cols::MU_WRITE), vec![ - // is_register + // domain BusValue::Packed { - start_column: cols::IS_REGISTER, + start_column: cols::DOMAIN, packing: Packing::Direct, }, // base_address @@ -942,13 +942,14 @@ impl TransitionConstraint for MemwConstrai /// Creates all constraints for the MEMW table. /// -/// 15 constraints total: +/// 16 constraints total: /// - IS_BIT<μ_sum> (1) /// - w2 => μ_sum (1) /// - IS_BIT<μ_read> (1) /// - IS_BIT<μ_write> (1) /// - IS_BIT for carry[0..6] (7) /// - IS_BIT (3) + IS_BIT (1) [spec assumption] +/// - IS_BIT (1) pub fn constraints() -> Vec>> { let mut constraints: Vec< @@ -985,6 +986,15 @@ pub fn constraints() idx += 1; } constraints.push(MemwConstraint::new(MemwConstraintKind::WidthSumIsBit, idx).boxed()); + idx += 1; + + // IS_BIT: pin the RAM/register domain tag to {0,1} locally. The Memory-bus + // commit domain (domain = 2) must never originate from MEMW; previously this held only + // indirectly (every Memw-bus dispatcher hardcodes the tag to 0/1, so a 2 leaves an unmatched + // dispatch token). Making it an explicit local constraint keeps the commit-domain separation + // robust against future refactors, mirroring how the L2G table pins MU explicitly rather + // than leaning on its cross-bus argument. + constraints.push(IsBitConstraint::unconditional(cols::DOMAIN, idx).boxed()); constraints } diff --git a/prover/src/tables/memw_aligned.rs b/prover/src/tables/memw_aligned.rs index 8042d9052..afa4534c3 100644 --- a/prover/src/tables/memw_aligned.rs +++ b/prover/src/tables/memw_aligned.rs @@ -6,7 +6,7 @@ //! //! ## Column layout (29 columns) //! -//! - `is_register`: Bit +//! - `domain`: Bit //! - `base_address[3]`: DWordWHH //! - `base_address[0]`: Half (low 16 bits) //! - `base_address[1]`: Half (mid 16 bits) @@ -53,7 +53,7 @@ pub const MAX_ROWS: usize = super::max_rows::MEMW_A; // ========================================================================= pub mod cols { - pub const IS_REGISTER: usize = 0; + pub const DOMAIN: usize = 0; /// base_address: DWordWHH (3 columns) /// base_address[0] = low half (bits 0-15) @@ -102,7 +102,7 @@ pub fn generate_memw_aligned_trace( let table = &mut trace.main_table; for (row_idx, op) in operations.iter().enumerate() { - table.set_bool(row_idx, cols::IS_REGISTER, op.is_register); + table.set_bool(row_idx, cols::DOMAIN, op.domain); table.set_dword_whh(row_idx, cols::BASE_ADDRESS[0], op.base_address); @@ -216,13 +216,13 @@ pub fn bus_interactions() -> Vec { packing: Packing::Direct, }; - // CM16: memory[is_register, base_address, old_timestamp, old[0]] with +μ_sum + // CM16: memory[domain, base_address, old_timestamp, old[0]] with +μ_sum interactions.push(BusInteraction::sender( BusId::Memory, mu_sum.clone(), vec![ BusValue::Packed { - start_column: cols::IS_REGISTER, + start_column: cols::DOMAIN, packing: Packing::Direct, }, base_addr_lo.clone(), @@ -242,13 +242,13 @@ pub fn bus_interactions() -> Vec { ], )); - // CM17: memory[is_register, base_address, timestamp, value[0]] with -μ_sum + // CM17: memory[domain, base_address, timestamp, value[0]] with -μ_sum interactions.push(BusInteraction::receiver( BusId::Memory, mu_sum, vec![ BusValue::Packed { - start_column: cols::IS_REGISTER, + start_column: cols::DOMAIN, packing: Packing::Direct, }, base_addr_lo.clone(), @@ -290,7 +290,7 @@ pub fn bus_interactions() -> Vec { w2_mult.clone(), vec![ BusValue::Packed { - start_column: cols::IS_REGISTER, + start_column: cols::DOMAIN, packing: Packing::Direct, }, addr_1_lo.clone(), @@ -315,7 +315,7 @@ pub fn bus_interactions() -> Vec { w2_mult, vec![ BusValue::Packed { - start_column: cols::IS_REGISTER, + start_column: cols::DOMAIN, packing: Packing::Direct, }, addr_1_lo, @@ -354,7 +354,7 @@ pub fn bus_interactions() -> Vec { Multiplicity::Sum(cols::WRITE4, cols::WRITE8), vec![ BusValue::Packed { - start_column: cols::IS_REGISTER, + start_column: cols::DOMAIN, packing: Packing::Direct, }, addr_i_lo.clone(), @@ -379,7 +379,7 @@ pub fn bus_interactions() -> Vec { Multiplicity::Sum(cols::WRITE4, cols::WRITE8), vec![ BusValue::Packed { - start_column: cols::IS_REGISTER, + start_column: cols::DOMAIN, packing: Packing::Direct, }, addr_i_lo, @@ -419,7 +419,7 @@ pub fn bus_interactions() -> Vec { Multiplicity::Column(cols::WRITE8), vec![ BusValue::Packed { - start_column: cols::IS_REGISTER, + start_column: cols::DOMAIN, packing: Packing::Direct, }, addr_i_lo.clone(), @@ -444,7 +444,7 @@ pub fn bus_interactions() -> Vec { Multiplicity::Column(cols::WRITE8), vec![ BusValue::Packed { - start_column: cols::IS_REGISTER, + start_column: cols::DOMAIN, packing: Packing::Direct, }, addr_i_lo, @@ -505,9 +505,9 @@ pub fn bus_interactions() -> Vec { start_column: cols::OLD[7], packing: Packing::Direct, }, - // is_register + // domain BusValue::Packed { - start_column: cols::IS_REGISTER, + start_column: cols::DOMAIN, packing: Packing::Direct, }, // base_address as DWordWL: [lo32, hi32] @@ -578,9 +578,9 @@ pub fn bus_interactions() -> Vec { BusId::Memw, Multiplicity::Column(cols::MU_WRITE), vec![ - // is_register + // domain BusValue::Packed { - start_column: cols::IS_REGISTER, + start_column: cols::DOMAIN, packing: Packing::Direct, }, // base_address as DWordWL: [lo32, hi32] @@ -723,8 +723,8 @@ impl TransitionConstraint for MemwAlignedC } } -/// Creates all constraints for the MEMW_A table (8 total). The last four are the -/// spec's defense-in-depth width-flag assumptions. +/// Creates all constraints for the MEMW_A table (9 total). Four are the spec's +/// defense-in-depth width-flag assumptions; the last pins the domain tag to {0,1}. pub fn constraints() -> Vec>> { vec![ @@ -736,5 +736,9 @@ pub fn constraints() IsBitConstraint::unconditional(cols::WRITE4, 5).boxed(), IsBitConstraint::unconditional(cols::WRITE8, 6).boxed(), MemwAlignedConstraint::new(MemwAlignedConstraintKind::WidthSumIsBit, 7).boxed(), + // IS_BIT: pin the RAM/register domain tag to {0,1} locally, so the + // Memory-bus commit domain (domain = 2) can never originate from MEMW_A. See the + // matching note in `memw::constraints`. + IsBitConstraint::unconditional(cols::DOMAIN, 8).boxed(), ] } diff --git a/prover/src/tables/memw_register.rs b/prover/src/tables/memw_register.rs index 14a696cb9..a24a420f7 100644 --- a/prover/src/tables/memw_register.rs +++ b/prover/src/tables/memw_register.rs @@ -1,7 +1,7 @@ //! MEMW_R (Memory Write/Read -- Register) table. //! //! Ultra-slim fast path for register accesses. Registers are always 2 words -//! (DWordWL), always aligned, and `is_register=1`, so this table strips out +//! (DWordWL), always aligned, and `domain=1`, so this table strips out //! all memory-specific columns (address decomposition, alignment mask, width //! flags, per-byte old_timestamps). //! @@ -177,7 +177,7 @@ pub fn bus_interactions() -> Vec { // ------------------------------------------------------------------------- // Memory bus read-old (sender, for i=0,1) - // memory[is_register=1, addr_lo=2*ADDRESS+i, addr_hi=0, + // memory[domain=1, addr_lo=2*ADDRESS+i, addr_hi=0, // OLD_TIMESTAMP_LO, TIMESTAMP_1, OLD[i]] // ------------------------------------------------------------------------- for i in 0..2 { @@ -214,7 +214,7 @@ pub fn bus_interactions() -> Vec { // ------------------------------------------------------------------------- // Memory bus write-new (receiver, for i=0,1) - // memory[is_register=1, addr_lo=2*ADDRESS+i, addr_hi=0, + // memory[domain=1, addr_lo=2*ADDRESS+i, addr_hi=0, // TIMESTAMP_0, TIMESTAMP_1, VAL[i]] // ------------------------------------------------------------------------- for i in 0..2 { @@ -276,7 +276,7 @@ pub fn bus_interactions() -> Vec { BusValue::constant(0), BusValue::constant(0), BusValue::constant(0), - // is_register = 1 + // domain = 1 BusValue::constant(1), // base_address = [2*ADDRESS, 0] addr_lo_linear.clone(), @@ -319,7 +319,7 @@ pub fn bus_interactions() -> Vec { BusId::Memw, Multiplicity::Column(cols::MU_WRITE), vec![ - // is_register = 1 + // domain = 1 BusValue::constant(1), // base_address = [2*ADDRESS, 0] addr_lo_linear, diff --git a/prover/src/tables/page.rs b/prover/src/tables/page.rs index 2d1059bcc..f97ad76c9 100644 --- a/prover/src/tables/page.rs +++ b/prover/src/tables/page.rs @@ -408,7 +408,7 @@ pub fn bus_interactions(page_base: u64) -> Vec { BusId::Memory, Multiplicity::One, vec![ - // is_register = 0 + // domain = 0 BusValue::constant(0), // address_lo = page_base_lo + offset address_lo.clone(), @@ -430,7 +430,7 @@ pub fn bus_interactions(page_base: u64) -> Vec { BusId::Memory, Multiplicity::One, vec![ - // is_register = 0 + // domain = 0 BusValue::constant(0), // address_lo = page_base_lo + offset address_lo, diff --git a/prover/src/tables/register.rs b/prover/src/tables/register.rs index 46c675b65..4ffe38650 100644 --- a/prover/src/tables/register.rs +++ b/prover/src/tables/register.rs @@ -1,6 +1,6 @@ //! REGISTER table for register initialization and finalization. //! -//! Similar to PAGE table but for registers (is_register=1). +//! Similar to PAGE table but for registers (domain=1). //! Provides initial and final tokens for the Memory bus to balance //! register read/write operations from MEMW. //! @@ -367,7 +367,7 @@ pub fn preprocessed_commitment(options: &ProofOptions, init: &[u32]) -> Commitme /// - REG-C1: memory[1, address, 1, init] - receiver, multiplicity -1 /// - REG-C2: memory[1, address, timestamp, fini] - sender, multiplicity 1 /// -/// Note: is_register=1 (constant) to distinguish from memory (is_register=0). +/// Note: domain=1 (constant) to distinguish from memory (domain=0). pub fn bus_interactions() -> Vec { // Address is just the offset in register space. // Stored in low word, high word is 0 @@ -386,7 +386,7 @@ pub fn bus_interactions() -> Vec { BusId::Memory, Multiplicity::One, vec![ - // is_register = 1 (registers, not memory) + // domain = 1 (registers, not memory) BusValue::constant(1), // address_lo = offset address_lo.clone(), @@ -409,7 +409,7 @@ pub fn bus_interactions() -> Vec { BusId::Memory, Multiplicity::One, vec![ - // is_register = 1 + // domain = 1 BusValue::constant(1), // address_lo = offset address_lo, diff --git a/prover/src/tables/store.rs b/prover/src/tables/store.rs index 1cdf0334e..764d42b99 100644 --- a/prover/src/tables/store.rs +++ b/prover/src/tables/store.rs @@ -135,7 +135,7 @@ pub fn bus_interactions() -> Vec { BusId::Memw, Multiplicity::Column(cols::MU), vec![ - BusValue::constant(0), // is_register = 0 (memory access) + BusValue::constant(0), // domain = 0 (memory access) BusValue::Packed { start_column: cols::BASE_ADDRESS_0, packing: Packing::DWordWL, diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index f3ca090d7..f86fde9ba 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -580,7 +580,7 @@ fn collect_load_op_from_cpu( // Create MEMW operation (read) let memw_op = MemwOperation::new( - false, // is_register = false + false, // domain = false base_address, res_bytes, op.timestamp, @@ -634,7 +634,7 @@ fn collect_store_op_from_cpu(op: &CpuOperation, memory_state: &mut MemoryState) // the old inline M7). It uses the base timestamp — the same the CPU sends on // the MEMORY bus — per spec store.toml. let memw_op = MemwOperation::new( - false, // is_register = false + false, // domain = false base_address, value_bytes, op.timestamp, @@ -1361,7 +1361,7 @@ fn collect_bitwise_from_memw_aligned(ops: &[MemwOperation]) -> Vec old_timestamp[0] (lower limb ordering) @@ -1370,7 +1370,7 @@ fn collect_bitwise_from_memw_aligned(ops: &[MemwOperation]) -> Vec bool { - if !op.is_register || op.width != 2 { + if !op.domain || op.width != 2 { return false; } // Both words must share old_timestamp (atomic register write assumption) diff --git a/prover/src/tables/types.rs b/prover/src/tables/types.rs index 71c83284a..a12460ebb 100644 --- a/prover/src/tables/types.rs +++ b/prover/src/tables/types.rs @@ -250,7 +250,7 @@ pub enum BusId { Memw = 14, // ID 15 (Load) is reserved: the load lookup is now dispatched through // [`MemoryOp`](BusId::MemoryOp). - /// Internal memory consistency bus: memory[is_register, address, timestamp, value] + /// Internal memory consistency bus: memory[domain, address, timestamp, value] /// Used for read/write pairing in MEMW table (M1-M8 in spec) Memory = 16, /// Branch target computation @@ -265,9 +265,10 @@ pub enum BusId { Ecall = 19, /// COMMIT self-referencing recursive bus (row N → row N+1) CommitNextByte = 20, - /// COMMIT output bus: verifier computes the receiver contribution externally - /// from `VmProof.public_output` using the shared LogUp challenges - Commit = 21, + // ID 21 (Commit) is reserved: the COMMIT output no longer has a dedicated bus. It now + // rides the [`Memory`](BusId::Memory) bus under the `domain` domain separator + // (`commit = 2`); the verifier still computes the receiver contribution externally from + // the claimed output (see `compute_commit_bus_offset`), now over the whole run's output. /// Keccak core ↔ round chip: (timestamp, round, state[200 bytes]) Keccak = 22, /// Keccak round ↔ RC lookup: (round, rc[8 bytes]) @@ -333,7 +334,6 @@ impl BusId { BusId::Decode => "Decode", BusId::Ecall => "Ecall", BusId::CommitNextByte => "CommitNextByte", - BusId::Commit => "Commit", BusId::Keccak => "Keccak", BusId::KeccakRc => "KeccakRc", BusId::ByteAlu => "ByteAlu", @@ -366,7 +366,7 @@ impl TryFrom for BusId { 18 => Ok(BusId::Decode), 19 => Ok(BusId::Ecall), 20 => Ok(BusId::CommitNextByte), - 21 => Ok(BusId::Commit), + // 21 (Commit) retired — see the enum definition. 22 => Ok(BusId::Keccak), 23 => Ok(BusId::KeccakRc), 24 => Ok(BusId::ByteAlu), diff --git a/prover/src/test_utils.rs b/prover/src/test_utils.rs index fd9d9d40c..2581f1b38 100644 --- a/prover/src/test_utils.rs +++ b/prover/src/test_utils.rs @@ -46,7 +46,7 @@ use crate::tables::bytewise::{ }; use crate::tables::commit::{ bus_interactions as commit_bus_interactions, cols as commit_cols, - create_constraints as commit_constraints, + create_constraints as commit_constraints, output_bus_interaction as commit_output_interaction, }; use crate::tables::cpu::{ CpuOperation, bus_interactions as cpu_bus_interactions, cols as cpu_cols, @@ -925,12 +925,20 @@ pub fn create_halt_air(proof_options: &ProofOptions) -> VmAir { } /// Create COMMIT AIR with constraints and bus interactions. -pub fn create_commit_air(proof_options: &ProofOptions) -> VmAir { +/// +/// `emit_output` controls whether the committed-output token +/// ([`commit_output_interaction`]) is included: +/// - `true` for a monolithic proof (the output bus is closed in-proof by the verifier); +/// - `false` for a continuation epoch (the output emit is carried up to the global proof +/// and closed there — see `commit_global_air` in `continuation.rs`). +pub fn create_commit_air(proof_options: &ProofOptions, emit_output: bool) -> VmAir { let (transition_constraints, _) = commit_constraints(0); - let auxiliary_trace_build_data = AuxiliaryTraceBuildData { - interactions: commit_bus_interactions(), - }; + let mut interactions = commit_bus_interactions(); + if emit_output { + interactions.push(commit_output_interaction()); + } + let auxiliary_trace_build_data = AuxiliaryTraceBuildData { interactions }; AirWithBuses::new( commit_cols::NUM_COLUMNS, @@ -972,7 +980,7 @@ pub fn create_page_air(proof_options: &ProofOptions, page_base: u64) -> VmAir { /// Create REGISTER AIR with bus interactions. /// /// The REGISTER table provides initial and final tokens for register accesses -/// on the Memory bus (is_register=1). +/// on the Memory bus (domain=1). pub fn create_register_air(proof_options: &ProofOptions) -> VmAir { let transition_constraints: Vec>> = vec![]; diff --git a/prover/src/tests/compute_commit_bus_offset_tests.rs b/prover/src/tests/compute_commit_bus_offset_tests.rs index ca6aab272..26d13b3de 100644 --- a/prover/src/tests/compute_commit_bus_offset_tests.rs +++ b/prover/src/tests/compute_commit_bus_offset_tests.rs @@ -3,6 +3,11 @@ //! Pins the three behaviours the verify-path helper must preserve: //! empty input short-circuit, success-path equivalence with a naive //! per-element-inverse reference, and the zero-fingerprint failure path. +//! +//! The COMMIT output rides the Memory bus in the `commit` domain +//! (`domain = 2`), token `[2, index, 0, 0, 0, value]`, so the fingerprint is +//! `z - (BusId::Memory + 2·α + index·α² + value·α⁶)` (bus_id at α⁰, then the six +//! token values at α¹..α⁶; the addr_hi/ts_lo/ts_hi slots are 0 and drop out). use math::field::element::FieldElement; @@ -16,17 +21,18 @@ type E = GoldilocksExtension; /// future refactor of the batched routine must remain equivalent to this. fn naive_offset( public_output: &[u8], - start_index: u64, z: &FieldElement, alpha: &FieldElement, ) -> Option> { - let bus_id = FieldElement::::from(BusId::Commit as u64); + let bus_id = FieldElement::::from(BusId::Memory as u64); let alpha_sq = alpha * alpha; + let alpha_pow6 = &alpha_sq * &alpha_sq * &alpha_sq; + let domain = &bus_id + (FieldElement::::from(2u64) * alpha); let mut total = FieldElement::::zero(); for (i, &value) in public_output.iter().enumerate() { - let lc = bus_id - + (FieldElement::::from(start_index + i as u64) * alpha) - + (FieldElement::::from(value as u64) * alpha_sq); + let lc = &domain + + (FieldElement::::from(i as u64) * &alpha_sq) + + (FieldElement::::from(value as u64) * &alpha_pow6); let fingerprint = z - lc; total += fingerprint.inv().ok()?; } @@ -38,7 +44,7 @@ fn test_empty_public_output_returns_zero() { let z = FieldElement::::from(7u64); let alpha = FieldElement::::from(11u64); assert_eq!( - compute_commit_bus_offset(&[], 0, &z, &alpha), + compute_commit_bus_offset(&[], &z, &alpha), Some(FieldElement::::zero()), ); } @@ -49,8 +55,8 @@ fn test_non_empty_matches_naive_per_element_inverse() { let alpha = FieldElement::::from(31_415_926u64); let public_output: [u8; 5] = [0x01, 0x02, 0xff, 0x10, 0x80]; - let batched = compute_commit_bus_offset(&public_output, 0, &z, &alpha); - let naive = naive_offset(&public_output, 0, &z, &alpha); + let batched = compute_commit_bus_offset(&public_output, &z, &alpha); + let naive = naive_offset(&public_output, &z, &alpha); assert_eq!(batched, naive); assert!(batched.is_some(), "no fingerprint should collide here"); @@ -62,44 +68,40 @@ fn test_longer_input_matches_naive() { let alpha = FieldElement::::from(0xcafe_babeu64); let public_output: Vec = (0..=255u16).map(|x| x as u8).collect(); - let batched = compute_commit_bus_offset(&public_output, 0, &z, &alpha); - let naive = naive_offset(&public_output, 0, &z, &alpha); + let batched = compute_commit_bus_offset(&public_output, &z, &alpha); + let naive = naive_offset(&public_output, &z, &alpha); assert_eq!(batched, naive); assert!(batched.is_some()); } #[test] -fn test_nonzero_start_index_matches_naive() { - // A continuation epoch whose commits continue a prior epoch: the offset must - // index from the carried x254, not 0. +fn test_index_is_bound_into_the_offset() { + // The commit index rides in the token, so the same bytes at shifted positions + // fingerprint differently. Reversing a multi-byte output must change the offset + // (each byte's α² index term changes), guarding that the index is bound in. let z = FieldElement::::from(0x1234_5678u64); let alpha = FieldElement::::from(0x9abc_def0u64); - let public_output: [u8; 3] = [0xCC, 0xDD, 0xEE]; - let start_index = 7u64; - - let batched = compute_commit_bus_offset(&public_output, start_index, &z, &alpha); - let naive = naive_offset(&public_output, start_index, &z, &alpha); - - assert_eq!(batched, naive); - assert!(batched.is_some()); + let forward: [u8; 3] = [0xCC, 0xDD, 0xEE]; + let reversed: [u8; 3] = [0xEE, 0xDD, 0xCC]; - // A different start index yields a different offset (the index is bound in). - let shifted = compute_commit_bus_offset(&public_output, start_index + 1, &z, &alpha); - assert_ne!(batched, shifted); + let a = compute_commit_bus_offset(&forward, &z, &alpha); + let b = compute_commit_bus_offset(&reversed, &z, &alpha); + assert!(a.is_some() && b.is_some()); + assert_ne!(a, b, "index must be bound into each byte's fingerprint"); } #[test] fn test_zero_fingerprint_returns_none() { - // Craft fingerprint_0 = 0: start_index = 0, value = 0, then - // fingerprint_0 = z - (BusId::Commit + 0·α + 0·α²) = z - BusId::Commit. - // Setting z = BusId::Commit forces the collision regardless of alpha. - let z = FieldElement::::from(BusId::Commit as u64); + // Craft fingerprint_0 = 0: index = 0, value = 0, then + // fingerprint_0 = z - (BusId::Memory + 2·α + 0·α² + 0·α⁶) = z - (BusId::Memory + 2α). + // Setting z to that forces the collision regardless of the higher alpha powers. let alpha = FieldElement::::from(42u64); + let z = FieldElement::::from(BusId::Memory as u64) + (FieldElement::::from(2u64) * alpha); let public_output: [u8; 1] = [0]; assert_eq!( - compute_commit_bus_offset(&public_output, 0, &z, &alpha), + compute_commit_bus_offset(&public_output, &z, &alpha), None, "zero fingerprint must propagate as None", ); @@ -110,15 +112,14 @@ fn test_zero_fingerprint_in_middle_returns_none() { // Same idea at i = 2, so some valid fingerprints precede the zero one. let alpha = FieldElement::::from(5u64); let alpha_sq = alpha * alpha; - let bus_id = FieldElement::::from(BusId::Commit as u64); - // value = 3 at index 2 → z = BusId + 2α + 3α² forces fingerprint_2 = 0. + let alpha_pow6 = alpha_sq * alpha_sq * alpha_sq; + let bus_id = FieldElement::::from(BusId::Memory as u64); + // value = 3 at index 2 → z = Memory + 2α + 2·α² + 3·α⁶ forces fingerprint_2 = 0. let z = bus_id + (FieldElement::::from(2u64) * alpha) - + (FieldElement::::from(3u64) * alpha_sq); + + (FieldElement::::from(2u64) * alpha_sq) + + (FieldElement::::from(3u64) * alpha_pow6); let public_output: [u8; 4] = [1, 2, 3, 4]; - assert_eq!( - compute_commit_bus_offset(&public_output, 0, &z, &alpha), - None, - ); + assert_eq!(compute_commit_bus_offset(&public_output, &z, &alpha), None); } diff --git a/prover/src/tests/memw_register_tests.rs b/prover/src/tests/memw_register_tests.rs index 56b8a372c..f11aa8bfc 100644 --- a/prover/src/tests/memw_register_tests.rs +++ b/prover/src/tests/memw_register_tests.rs @@ -9,7 +9,7 @@ fn test_memw_register_trace_generation() { // Create a simple register op (reg x1 = address 1, so base_address = 2) let ops = vec![ MemwOperation::new( - true, // is_register + true, // domain 2, // base_address = 2 * register_index (reg x1) [42, 7, 0, 0, 0, 0, 0, 0], 100, @@ -51,7 +51,7 @@ fn test_memw_register_trace_generation_write_op() { // Write op: is_read = false => MU_WRITE=1, MU_READ=0 let ops = vec![ MemwOperation::new( - true, // is_register + true, // domain 4, // base_address = 2 * register_index (reg x2) [99, 55, 0, 0, 0, 0, 0, 0], 200, diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index 10013b5ed..29bb31407 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -80,7 +80,6 @@ fn prove_and_verify_vm_minimal(elf: &Elf, traces: &mut Traces) -> bool { &airs.air_refs(), &multi_proof, &traces.public_output_bytes, - 0, &mut replay_transcript, ) .expect("fingerprint collision in test"); @@ -168,7 +167,6 @@ fn verify_vm_minimal(vm_proof: &VmProof, elf_bytes: &[u8]) -> bool { &air_refs, &vm_proof.proof, &vm_proof.public_output, - 0, &mut replay_transcript, ) .expect("fingerprint collision in test"); @@ -1379,7 +1377,6 @@ fn test_prove_elfs_test_commit_4_wrong_pages_rejected() { &verifier_air_refs, &proof, &traces.public_output_bytes, - 0, &mut replay_transcript, ) .expect("fingerprint collision in test"); @@ -1483,7 +1480,7 @@ fn test_debug_memory_bus_tokens() { // === MEMW tokens (for register rows only) === println!("\n=== MEMW Memory Bus Tokens (register rows) ==="); for row in 0..memw.num_rows() { - let is_reg = memw.main_table.get(row, memw_cols::IS_REGISTER).to_raw(); + let is_reg = memw.main_table.get(row, memw_cols::DOMAIN).to_raw(); if is_reg == 0 { continue; // Skip memory rows (multiplicity = 0) } @@ -1623,7 +1620,7 @@ fn test_debug_memory_bus_tokens() { // MEMW tokens for row in 0..memw.num_rows() { - let is_reg = memw.main_table.get(row, memw_cols::IS_REGISTER).to_raw(); + let is_reg = memw.main_table.get(row, memw_cols::DOMAIN).to_raw(); if is_reg == 0 { continue; } @@ -1753,7 +1750,7 @@ fn test_debug_memory_tokens_sb_sh() { let mut token_balance: HashMap)> = HashMap::new(); // === REGISTER Memory tokens === - println!("\n=== REGISTER Memory Bus Tokens (is_register=1) ==="); + println!("\n=== REGISTER Memory Bus Tokens (domain=1) ==="); for row in 0..traces.register.num_rows().min(64) { let offset = traces .register @@ -1805,7 +1802,7 @@ fn test_debug_memory_tokens_sb_sh() { let mut memw_register_rows = 0; let mut memw_memory_rows = 0; for row in 0..memw.num_rows() { - let is_reg = memw.main_table.get(row, memw_cols::IS_REGISTER).to_raw(); + let is_reg = memw.main_table.get(row, memw_cols::DOMAIN).to_raw(); // Count row types if is_reg == 1 { @@ -2134,7 +2131,6 @@ fn test_deep_stack_runtime_pages_roundtrip() { &verifier_air_refs, &proof, &traces.public_output_bytes, - 0, &mut replay_transcript, ) .expect("fingerprint collision in test"); @@ -2207,7 +2203,6 @@ fn test_deep_stack_missing_pages_rejected() { &verifier_air_refs, &proof, &traces.public_output_bytes, - 0, &mut replay_transcript, ) .expect("fingerprint collision in test"); @@ -2315,7 +2310,6 @@ fn test_heap_alloc_runtime_pages_roundtrip() { &verifier_air_refs, &proof, &traces.public_output_bytes, - 0, &mut replay_transcript, ) .expect("fingerprint collision in test"); @@ -2973,7 +2967,6 @@ fn test_prove_first_epoch_without_halt() { &airs.air_refs(), &multi_proof, &traces.public_output_bytes, - 0, &mut replay, ) .expect("fingerprint collision in test"); @@ -3057,7 +3050,6 @@ fn test_prove_second_epoch_from_snapshot() { &airs.air_refs(), &multi_proof, &traces.public_output_bytes, - 0, &mut replay, ) .expect("fingerprint collision in test"); @@ -3164,7 +3156,6 @@ fn test_epoch_proof_commits_l2g() { &refs, &multi_proof, &traces.public_output_bytes, - 0, &mut replay, ) .expect("fingerprint collision in test"); @@ -3316,7 +3307,6 @@ fn test_continuation_pipeline_end_to_end() { &refs, &multi_proof, &traces.public_output_bytes, - 0, &mut replay, ) .expect("fingerprint collision in test"); @@ -3447,7 +3437,6 @@ fn test_epoch_memory_bus_with_l2g_bookend() { &refs, &multi_proof, &traces.public_output_bytes, - 0, &mut replay, ) .expect("fingerprint collision in test"); diff --git a/prover/src/tests/statement_tests.rs b/prover/src/tests/statement_tests.rs index 73944e262..d434b6811 100644 --- a/prover/src/tests/statement_tests.rs +++ b/prover/src/tests/statement_tests.rs @@ -163,16 +163,36 @@ fn continuation_epoch_differs_from_monolithic_statement() { assert_ne!(monolithic, epoch_state(b"elf", 1)); } -fn global_state(elf: &[u8], num_epochs: usize) -> [u8; 32] { +fn global_state(elf: &[u8], num_epochs: usize, full_output: &[u8]) -> [u8; 32] { let mut t = DefaultTranscript::::new(&[]); - absorb_continuation_global_statement(&mut t, elf, num_epochs); + absorb_continuation_global_statement(&mut t, elf, num_epochs, full_output); t.state() } #[test] -fn continuation_global_state_binds_program_and_epoch_count() { - let baseline = global_state(b"elf", 3); - assert_eq!(baseline, global_state(b"elf", 3)); // deterministic - assert_ne!(baseline, global_state(b"elf", 4), "must bind epoch count"); - assert_ne!(baseline, global_state(b"other-elf", 3), "must bind the ELF"); +fn continuation_global_state_binds_program_epoch_count_and_output() { + let baseline = global_state(b"elf", 3, b"output"); + assert_eq!(baseline, global_state(b"elf", 3, b"output")); // deterministic + assert_ne!( + baseline, + global_state(b"elf", 4, b"output"), + "must bind epoch count" + ); + assert_ne!( + baseline, + global_state(b"other-elf", 3, b"output"), + "must bind the ELF" + ); + assert_ne!( + baseline, + global_state(b"elf", 3, b"OUTPUT"), + "must bind the committed output" + ); + // Length is bound, not just concatenated bytes: an output that would collide under a + // naive concat (e.g. a length-prefix boundary shift) still diverges. + assert_ne!( + global_state(b"elf", 3, b"ab"), + global_state(b"elf", 3, b"abc"), + "must bind the output length" + ); } From 6d9546db43daa0abd2e871f20f37320b0c17a651 Mon Sep 17 00:00:00 2001 From: Nicole Date: Wed, 1 Jul 2026 16:35:47 -0300 Subject: [PATCH 2/2] Fix COMMIT bus-interaction count test for the split output emit --- prover/src/tests/commit_tests.rs | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/prover/src/tests/commit_tests.rs b/prover/src/tests/commit_tests.rs index f23405b0e..2c0235e60 100644 --- a/prover/src/tests/commit_tests.rs +++ b/prover/src/tests/commit_tests.rs @@ -427,9 +427,18 @@ fn test_address_incr_halfword_carry() { #[test] fn test_bus_interactions_count() { - use crate::tables::commit::bus_interactions; + use crate::tables::commit::{bus_interactions, output_bus_interaction}; + use crate::tables::types::BusId; + + // 17 base interactions (Ecall, CommitNextByte send/receive, IsHalfword ×8, Zero, + // Memw ×5); the committed-output emit is a separate interaction. let interactions = bus_interactions(); - assert_eq!(interactions.len(), 18); + assert_eq!(interactions.len(), 17); + + // The output emit is a single Memory-bus sender in the commit domain. + let output = output_bus_interaction(); + assert!(output.is_sender); + assert_eq!(output.bus_id, u64::from(BusId::Memory)); } #[test]