diff --git a/docs/continuations_design.md b/docs/continuations_design.md index 71bb3577a..8115e4ca1 100644 --- a/docs/continuations_design.md +++ b/docs/continuations_design.md @@ -502,7 +502,10 @@ weaken soundness — and it pins every proof to its program and position, so a p can't be replayed elsewhere: - Each **epoch** absorbs: a domain tag, the ELF digest, the public output, the - table layout, and the **epoch label** (its position). + table layout, the **epoch label** (its position), and **`is_final`** (whether it + carries HALT). The table layout is every `TableCounts` field individually, so a + layout that moves a count from one chip to another diverges here even when the + total is unchanged. - The **global** proof absorbs: a (distinct) domain tag, the ELF digest, the **epoch count**, the **private-input page count** (§3.6), and the **touched page-base set** — so the whole genesis AIR layout (which GLOBAL_MEMORY tables exist and which are @@ -544,9 +547,16 @@ becomes an **explicit verifier action**: - **Enumerate, don't trust.** The verifier assigns each epoch's `label` and the `is_final` flag **by position** (`0..N-1`; the last is final), so the prover can't - relabel, reorder, truncate, or append epochs — a wrong label diverges that epoch's - Fiat-Shamir challenges, and a wrong `is_final` builds the HALT table in/out and - mismatches the committed proof. + relabel, reorder, truncate, or append epochs. Both are absorbed into the epoch + statement, so either one wrong diverges that epoch's Fiat-Shamir challenges. + `is_final` is additionally load-bearing three more times: it moves the expected + sub-proof count by one (`FIXED_TABLE_COUNT - 1` for non-final epochs); deleting + HALT's sub-proof to compensate drops its main Merkle root from the Phase A + absorption and re-randomizes every downstream challenge; and HALT's bus + interactions are hardcoded `Multiplicity::One`, so its contribution cannot be + missing from a balanced sum. That last one is what makes "the last epoch really + halted" a constraint rather than a convention — a truncated run's non-halting + last epoch is built *with* HALT and fails the balance. - **Derive the register / x254 chain.** Epoch 0's register INIT is derived from the ELF entry point; epoch *i+1*'s INIT is derived from epoch *i*'s bundle `reg_fini` (incl. x254 @ 508). So `init(i+1) == fini(i)` is now *enforced by the verifier diff --git a/prover/src/auto_storage.rs b/prover/src/auto_storage.rs index b4718974c..8cc437edd 100644 --- a/prover/src/auto_storage.rs +++ b/prover/src/auto_storage.rs @@ -104,7 +104,12 @@ fn aux_cols(bus_count: usize) -> u64 { bus_count.div_ceil(2) as u64 } -/// Per-table specs in the same order as `air_trace_pairs` in `prove`. +/// Per-table specs for the heap estimate. The order is not meaningful — every +/// consumer sums or sorts — and it does not track `air_trace_pairs`. +/// +/// Note this list models only the tables `TableLengths` carries: there is no +/// entry for eq, bytewise, store, cpu32, keccak, keccak_rnd, ecsm, ecdas or +/// hint, so a run dominated by one of those is under-estimated. fn table_specs(lengths: &TableLengths) -> Vec { let bitwise_rows = BITWISE_ROWS as u64; let register_rows = NUM_REGISTER_ADDRESSES.next_power_of_two() as u64; diff --git a/prover/src/lib.rs b/prover/src/lib.rs index 09d53ceb1..5030b3bb0 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -80,14 +80,20 @@ pub struct RuntimePageRange { pub count: u64, } -/// Number of tables that always contribute exactly one sub-proof, regardless -/// of `TableCounts`: bitwise, decode, halt, keccak_rc, register. The -/// accelerator chips are counted instead — a run that never calls one carries -/// no table for it. +/// Number of tables that contribute exactly one sub-proof regardless of +/// `TableCounts`: bitwise, decode, halt, keccak_rc, register. The accelerator +/// chips are counted instead — a run that never calls one carries no table for +/// it. +/// +/// HALT is the exception, and the reason this is not simply "always": a +/// continuation epoch carries it only when it is the final one, so `verify_epoch` +/// sizes non-final epochs with `FIXED_TABLE_COUNT - 1`. Any caller computing an +/// expected sub-proof count for a continuation epoch must do the same. pub const FIXED_TABLE_COUNT: usize = 5; -/// Number of chunks for each split table. -/// The verifier needs this to reconstruct matching AIRs. +/// How many sub-proofs each counted table contributes. Chunked chips report +/// their chunk count; the six accelerators are not chunked and report 0 or 1 +/// (see `validate`). The verifier needs this to reconstruct matching AIRs. #[derive(Debug, Clone, rkyv::Archive, rkyv::Serialize, rkyv::Deserialize)] pub struct TableCounts { pub cpu: usize, @@ -178,10 +184,13 @@ impl TableCounts { } } // The accelerators are not chunked: `generate_optional` emits one table - // or none, so a count above 1 is a shape no prover can produce. Rejected - // here rather than left to the sub-proof cross-check, which would only - // catch it once the counts had already sized the AIR set. If one of them - // ever becomes chunked, this list is what changes. + // or none, so a count above 1 is a shape no prover can produce. The + // sub-proof cross-check constrains only the *total*, so on its own it + // lets an inflated accelerator count through whenever another count is + // lowered to match; this pins the per-field shape instead. It is not + // load-bearing for memory safety — both verifiers run the cross-check + // before any count sizes an AIR set — and if one of them ever becomes + // chunked, this list is what changes. let at_most_one = [ ("keccak", self.keccak), ("keccak_rnd", self.keccak_rnd), @@ -1510,8 +1519,11 @@ fn verify_proof_parts( decode_commitment: Option, page_commitments: Option<&[(u64, Commitment)]>, ) -> Result { - // Validate table_counts before constructing AIRs. - // A malicious prover could set counts to 0, removing entire constraint sets. + // Validate table_counts before constructing AIRs. A zero count is legitimate + // for every chip but CPU and MEMW_R — what keeps it honest is the LogUp bus, + // not this call (see `TableCounts::validate`). This rejects the two counts + // whose absence describes no execution at all, and the accelerator shapes no + // prover can produce. table_counts.validate()?; // Bound num_private_input_pages before allocating PageConfigs — the tight honest diff --git a/prover/src/statement.rs b/prover/src/statement.rs index 057c1276f..edac11b90 100644 --- a/prover/src/statement.rs +++ b/prover/src/statement.rs @@ -162,12 +162,21 @@ pub(crate) fn absorb_statement_with_digest( // Continuation epochs additionally bind their position (replay protection) // and whether they are the final one. `is_final` decides whether HALT is in // the epoch's AIR set, so without it the transcripts of a final and a - // non-final epoch carrying the same counts are identical, and the only thing - // separating the two AIR sets is the sub-proof count arithmetic in - // `verify_epoch`. The verifier derives `is_final` from the epoch's position - // in the bundle, so a spliced bundle re-reads an epoch under the other role - // and diverges here. Monolithic proofs append nothing, so their encoding is - // unchanged. + // non-final epoch carrying the same counts are identical. The verifier + // derives `is_final` from the epoch's position in the bundle, so a spliced + // bundle re-reads an epoch under the other role and diverges here. + // + // Defense in depth, not a plugged hole: a role flip is already rejected + // without this byte, and by more than one check. Re-reading an epoch under + // the other role moves the expected sub-proof count by one (`verify_epoch`'s + // `FIXED_TABLE_COUNT - 1` arm); deleting HALT's sub-proof to compensate + // drops its main Merkle root from the Phase A absorption and re-randomizes + // every downstream challenge; and HALT's own bus interactions are hardcoded + // `Multiplicity::One`, so its contribution cannot be absent from a balanced + // sum. Binding the role here makes it an explicit statement field instead of + // an emergent consequence of those three — do not weaken any of them on the + // strength of this byte. Monolithic proofs append nothing, so their encoding + // is unchanged. if let StatementKind::ContinuationEpoch { epoch_label, is_final, diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index e896887ff..c3b695a80 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -1735,8 +1735,8 @@ fn collect_bitwise_from_lt(lt_ops: &[LtOperation]) -> Vec { /// and IS_B20 lookups for carry range checks. /// /// IS_HALF and IS_B20 are emitted once per raw op. MSB16 is deduplicated -/// per `max_rows_mul` chunk, mirroring `chunk_and_generate` — a unique signed -/// op that spans two instances is sent twice and must be tallied twice. +/// per `max_rows_mul` chunk, mirroring `chunk_and_generate_optional` — a unique +/// signed op that spans two instances is sent twice and must be tallied twice. /// /// Returns: Vec of bitwise lookups pub(crate) fn collect_bitwise_from_mul( @@ -1833,7 +1833,7 @@ pub(crate) fn collect_bitwise_from_mul( /// /// IS_HALF and ZERO (C8/C20) are emitted once per raw op. MSB16 and the /// NEG-template ZERO lookups (C3/C5) are deduplicated per `max_rows_dvrm` -/// chunk, mirroring `chunk_and_generate`. +/// chunk, mirroring `chunk_and_generate_optional`. /// /// Returns: Vec of bitwise lookups pub(crate) fn collect_bitwise_from_dvrm( @@ -2803,6 +2803,14 @@ impl CollectedEpoch { } /// All generated trace tables. +/// +/// Every `Vec` field here may be **empty**: a chip the run never reaches carries +/// no table at all, so indexing one without checking panics on a program that +/// happens not to use it. The only exceptions are `cpus` and `memw_registers`, +/// which are built through `chunk_and_generate` and always carry at least one +/// (padded) chunk — the same two `TableCounts::validate` requires. Several +/// fields below spell this out individually; the rule is the struct's, not +/// theirs. pub struct Traces { /// CPU execution traces (split into chunks of max_rows::CPU) pub cpus: Vec>, @@ -3619,7 +3627,8 @@ fn build_traces( }; let gen_register = || register::generate_register_trace(®ister_final_state, register_init); let gen_halt = || halt::generate_halt_trace(halt_timestamp, halt_next_pc); - // ECSM accelerator traces (empty/all-padding for programs that do not use ECSM). + // ECSM accelerator traces. A program that does not use ECSM carries no ECSM + // and no ECDAS table at all — not a padded one. let gen_ecsms = || { generate_optional( &ecsm_ops, @@ -3636,7 +3645,7 @@ fn build_traces( storage_mode, ) }; - // HINT table (all-padding for programs that make no hint ecalls). + // HINT table. Absent entirely for programs that make no hint ecalls. let gen_hints = || { generate_optional( &hint_ops, diff --git a/prover/src/tests/dvrm_tests.rs b/prover/src/tests/dvrm_tests.rs index 2b5abe3b9..8179a98ec 100644 --- a/prover/src/tests/dvrm_tests.rs +++ b/prover/src/tests/dvrm_tests.rs @@ -467,7 +467,8 @@ fn test_dvrm_air_wires_in_chip_constraints() { /// Regression test for the `Msb16` LogUp over-send bug. /// -/// DVRM is split into chip instances of `max_rows.dvrm` raw ops (`chunk_and_generate`) +/// DVRM is split into chip instances of `max_rows.dvrm` raw ops +/// (`chunk_and_generate_optional`) /// and each instance deduplicates only its own chunk, sending its three MSB16 sign /// lookups once per unique signed op *per instance* (multiplicity = the `SIGNED` bit). /// So `collect_bitwise_from_dvrm`, which feeds the BITWISE MSB16 multiplicity, must use diff --git a/prover/src/tests/mul_tests.rs b/prover/src/tests/mul_tests.rs index 1e2fe5b5b..0d2e22243 100644 --- a/prover/src/tests/mul_tests.rs +++ b/prover/src/tests/mul_tests.rs @@ -371,7 +371,8 @@ fn test_mul_range_checks_input_halves() { /// Regression test for the `Msb16` LogUp over-send bug. /// -/// MUL is split into chip instances of `max_rows.mul` raw ops (`chunk_and_generate`) +/// MUL is split into chip instances of `max_rows.mul` raw ops +/// (`chunk_and_generate_optional`) /// and each instance deduplicates only its own chunk, sending the MSB16 sign lookup /// once per unique signed op *per instance* (multiplicity = the `SIGNED` bit). So /// `collect_bitwise_from_mul`, which feeds the BITWISE MSB16 multiplicity, must use diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index 92e27528a..2707e67af 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -59,9 +59,10 @@ fn memw_chunk_rows( .flat_map(|t| (0..t.num_rows()).map(move |row| (t, row))) } -/// Run multi_prove and multi_verify for all VM tables. +/// Run multi_prove and multi_verify over the tables this run actually carries. /// -/// Includes: CPU + Bitwise + LT + MEMW + LOAD + DECODE + MUL + BRANCH + HALT + REGISTER + PAGEs +/// The AIR set comes from `traces.table_counts()`, so a chip the program never +/// reaches is absent from both sides rather than proved as a padded table. /// /// Uses minimal bitwise (no full 2^20 preprocessed table) but DECODE is always preprocessed. pub(crate) fn prove_and_verify_vm_minimal(elf: &Elf, traces: &mut Traces) -> bool { diff --git a/prover/src/tests/skip_empty_tables_tests.rs b/prover/src/tests/skip_empty_tables_tests.rs index 3071a7c6f..85766cced 100644 --- a/prover/src/tests/skip_empty_tables_tests.rs +++ b/prover/src/tests/skip_empty_tables_tests.rs @@ -361,15 +361,18 @@ fn validate_still_requires_cpu_and_the_register_file() { } /// The counts ride in the proof, so they are the prover's to choose, and the -/// sub-proof cross-check compares only their sum. A plain `+` wraps silently in -/// release (the workspace sets no `overflow-checks`), so an attacker can park -/// one field near `usize::MAX`, pick a second to carry the sum around to -/// whatever `proofs.len()` is, and pass that check with the huge field intact — -/// straight into `VmAirs::new`, which sizes a `Vec` from it. -/// The six accelerators are not chunked — `generate_optional` emits one table or -/// none — so any count above 1 describes a table set no prover can build. Both -/// verifiers call `validate` before the counts size anything (`verify_proof_parts` -/// and `verify_epoch`), so rejecting it here is rejecting it on every path. +/// sub-proof cross-check constrains only their *sum*. The six accelerators are +/// not chunked — `generate_optional` emits one table or none — so any count +/// above 1 describes a table set no prover can build, and the sum alone does not +/// catch it: lower another count by the same amount and the total still matches. +/// This pins the per-field shape. +/// +/// It is a shape restriction, not a memory-safety guard. Both verifiers run the +/// cross-check *before* any count sizes an AIR set (`verify_proof_parts`: +/// `validate` → total-vs-`proofs.len()` → `VmAirs::new`; `verify_epoch` the +/// same), and `total()` is checked, so an astronomical count cannot reach +/// `VmAirs::new` by wrapping the sum either — that is +/// [`counts_that_wrap_have_no_total`]'s property, not this one's. #[test] fn an_accelerator_count_above_one_is_rejected() { let (elf, logs, _instructions) = run_asm_elf("test_keccak");