From aae68adf07748f62c8486cc47419e6576d5df93a Mon Sep 17 00:00:00 2001 From: Nicole Date: Wed, 1 Jul 2026 11:52:13 -0300 Subject: [PATCH 01/14] fix private input --- docs/continuations_design.md | 92 ++++++--- prover/src/continuation.rs | 306 ++++++++++++++++++++++------ prover/src/statement.rs | 10 +- prover/src/tables/global_memory.rs | 13 +- prover/src/tests/statement_tests.rs | 27 ++- 5 files changed, 353 insertions(+), 95 deletions(-) diff --git a/docs/continuations_design.md b/docs/continuations_design.md index 9c3f54747..a985a1223 100644 --- a/docs/continuations_design.md +++ b/docs/continuations_design.md @@ -61,8 +61,11 @@ makes the proof fail. - across epochs, on the **GlobalMemory bus**, it carries each cell's "where did this value come from / where is it going" claims. - **global_memory** — the *anchors* on the GlobalMemory bus: - - **genesis**: a cell's starting value, read from the **ELF** (preprocessed, - so the verifier recomputes it — the prover cannot choose initial memory). + - **genesis**: a cell's starting value. For ELF/runtime pages it is **preprocessed** + (read from the ELF, so the verifier recomputes it — the prover cannot choose initial + memory). For **private-input pages** it is a **committed** (non-preprocessed) column + the verifier never recomputes — the private bytes stay private and are pinned by the + bus instead (see §3.6); this mirrors the monolithic PAGE table. - **finalization**: a cell's final value after the last epoch that touched it. ### A single L2G row @@ -231,6 +234,39 @@ This is a **completeness** fix: it changes no constraint and nothing the verifie accepts — only how the driver slices cycles. A debug-assert enforces the "intermediate epoch ⟹ power-of-two cycle count" invariant. +### 3.6 Private-input genesis (committed, not ELF-bound) + +Genesis for ELF/runtime pages is preprocessed, so the verifier recomputes it from the +ELF — that is what stops a prover from choosing initial memory (§2). But **private +input** is, by definition, *not* in the ELF and must **stay private** from the verifier. +So a private-input page's genesis cannot be ELF-recomputed. + +Fix (mirrors the monolithic PAGE table exactly): build the `global_memory` AIR for a +private-input page **non-preprocessed**, so its `INIT` (genesis) is a **committed +main-trace column** the verifier never recomputes or sees. Correctness is enforced by +the same bus chain as everything else: the genesis token telescopes into the first +touching epoch's L2G `init`, which is pinned on the epoch-local Memory bus to MEMW's +true first-read value. A forged genesis would leave an unmatched Memory-bus term. This +is the same "output pinned by a complete chain" argument as the finalization (§4): the +private genesis is prover-supplied *by design* (it is the private input), so the proof +attests "**there exists** a private input producing this output" — the intended +semantics, identical to the monolithic prover. + +**Which pages are private** is decided by **count**, not by the raw byte range: the +first `num_private_input_pages` pages from `PRIVATE_INPUT_START_INDEX` (the page-aligned +span the input occupies), exactly matching the monolithic verifier's +`page_configs_from_elf_and_runtime`. The count is a public value in the bundle: +bound-checked against the max, absorbed into the global Fiat-Shamir statement (§7), and +additionally pinned by the committed AIR shape — a wrong count flips a *touched* page's +preprocessed mode, so the rebuilt AIR no longer matches the committed trace and the +proof fails. The verifier is given **only the count**, never the private bytes +(`verify_continuation` takes `elf + bundle` alone). + +Before this, the continuation bundle shipped the raw `private_inputs` and the verifier +recomputed the private genesis from them — which both **leaked** the input and +contradicted the memory spec (`memory.md`: prover/private input is a *committed* column, +not verifier-recomputed). §3.6 removes both problems. + --- ## 4. Design X vs Design Y — *where* `MU` is applied @@ -294,11 +330,14 @@ when it's really `f2`. A false statement, proven. (For a *middle* epoch, reroute the later init to consume the earlier fini, skipping the middle one.) The root cause is the **input/output asymmetry** of the anchors: genesis is the -*input* and is ELF-bound (fixed), but the finalization is the *output* — a prover -column. The finalization is only trustworthy if the chain is **complete** so that -the last fini is *forced* to be consumed by it. A complete chain pins the -finalization; a truncatable chain leaves it free. Design X forces completeness -(via `MU=1` on every touched cell); Design Y does not. +*input* — a single per-cell **source** that must be consumed — while the finalization +is the *output*, a prover column that must be *forced* to consume the chain's tail. The +finalization is only trustworthy if the chain is **complete** so that the last fini is +forced into it. A complete chain pins the finalization; a truncatable chain leaves it +free. Design X forces completeness (via `MU=1` on every touched cell); Design Y does +not. (Genesis's *value* is ELF-recomputed for ELF/runtime pages and prover-committed for +private-input pages (§3.6), but either way it is the one source token the first-touch +epoch must consume, so this completeness argument is unchanged.) ### Statement S (why Design X is sound, and what Y broke) @@ -440,8 +479,10 @@ 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). -- The **global** proof absorbs: a (distinct) domain tag, the ELF digest, and the - **epoch count**. +- The **global** proof absorbs: a (distinct) domain tag, the ELF digest, the + **epoch count**, and the **private-input page count** (§3.6) — so the genesis AIR + layout (which pages are non-preprocessed) is pinned in the statement, matching the + monolithic path's `absorb_statement`. The monolithic encoding is unchanged (same function, monolithic tag, no label). The genesis / register / memory anchor values are *additionally* bound via the @@ -466,8 +507,9 @@ The bundle is prover-supplied and therefore **untrusted**. Per epoch it carries `MultiProof`, the `public_output` slice, `table_counts`, `num_private_input_pages`, `runtime_page_ranges`, the bound `reg_fini` (`R_{i+1}`), the epoch `l2g_root`, and the touched-cell `boundary`; plus the global `MultiProof` -and the `private_inputs`. Everything the integrated path reused from prover memory -becomes an **explicit verifier action**: +and a top-level `num_private_input_pages` **count** (§3.6). It does **not** carry the +raw private input — the verifier never sees it. Everything the integrated path reused +from prover memory 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 @@ -480,8 +522,10 @@ becomes an **explicit verifier action**: rebuilding the AIR from the previous FINI* (via the shared `build_epoch_airs`), not merely true-by-construction. The commit-bus `start_index` is taken from the carried `register_init[508]`, not a free scalar. -- **Genesis from the ELF.** `verify_global` rebuilds the memory genesis from the ELF - (+ bundle private inputs) and closes the GlobalMemory bus; +- **Genesis from the ELF (private input excepted).** `verify_global` rebuilds the + ELF/runtime genesis from the ELF alone (no private bytes) and closes the GlobalMemory + bus; private-input pages are built non-preprocessed (§3.6), so their genesis is a + committed, bus-pinned column the verifier neither recomputes nor sees. `verify_l2g_commitment_binding` ties each epoch's `l2g_root` to the corresponding global-proof sub-table root — which is what makes the prover-supplied `boundary` trustworthy. @@ -519,10 +563,10 @@ recursion/aggregation layer (deferred). - Implemented and tested: range checks (§3.1), `fini_epoch` constant (§3.2), ordering check (§3.3), the `MU` selector (§3.4), the **power-of-two epoch size** - (§3.5), **cross-epoch registers** (§6), the **commit index x254** across epochs - (§6), the **Fiat-Shamir statement binding** (§7), and the **standalone split - prover/verifier** (§8) — bundle serialized with `bincode` and driven from the CLI - (`prove`/`verify --continuations`). + (§3.5), **private-input genesis kept private** (§3.6), **cross-epoch registers** + (§6), the **commit index x254** across epochs (§6), the **Fiat-Shamir statement + binding** (§7), and the **standalone split prover/verifier** (§8) — bundle serialized + with `bincode` and driven from the CLI (`prove`/`verify --continuations`). - **The committed code implements Design X** (`MU` gates every L2G interaction), which is the sound design. Design Y was implemented briefly, then found unsound (§4, the chain-truncation attack) and **reverted**. Do not re-introduce the @@ -530,10 +574,12 @@ recursion/aggregation layer (deferred). - Deferred: - **Succinctness.** The split verifier is non-succinct (N+1 proofs, §8). A single small proof needs a recursion/aggregation layer — a separate, larger effort. - - **Private-input binding.** The genesis image depends on `private_inputs`, which - the bundle carries in the clear; binding them into the statement (so "which input - produced this output" is pinned) is a follow-up that also touches the monolithic - proof. + - **Private-input *content* binding.** The bundle no longer carries the private input + in the clear (§3.6 — it carries only the page count, and the verifier never sees the + bytes). What remains deferred is pinning *which specific input* produced the output: + the proof attests only that *some* private input does. A guest that needs "this exact + input" must commit a hash of it to the public output — the framework provides no such + binding on either the continuation or monolithic path. --- @@ -542,8 +588,8 @@ recursion/aggregation layer (deferred). - `prover/src/tables/local_to_global.rs` — L2G columns, trace generation, the Memory/GlobalMemory bus interactions, range checks, the ordering lookup, and the per-row selector. -- `prover/src/tables/global_memory.rs` — the genesis (ELF-bound) and - finalization anchors. +- `prover/src/tables/global_memory.rs` — the genesis (ELF-bound for ELF/runtime pages, + committed/private for private-input pages, §3.6) and finalization anchors. - `prover/src/tables/register.rs` — the REGISTER table: REG-C1/REG-C2 Memory-bus tokens, the preprocessed FINI commitment (`compute_precomputed_commitment_with_fini`, `NUM_PREPROCESSED_COLS_WITH_FINI`), and `fini_from_trace`. diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index ccdd5a6f9..ba0439847 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -5,9 +5,13 @@ //! and proves one cross-epoch "global memory" LogUp that links every epoch's //! `fini` to the next epoch's `init` (so `fini(epoch i) == init(epoch i+1)`). //! -//! The global proof's genesis anchor is bound to the ELF: the verifier -//! recomputes the per-page preprocessed init commitment from the ELF in -//! `verify_global`, so the starting memory cannot be prover-supplied. +//! The global proof's genesis anchor is bound to the ELF: for ELF/runtime pages the +//! verifier recomputes the per-page preprocessed init commitment from the ELF in +//! `verify_global`, so the starting memory cannot be prover-supplied. Private-input +//! pages are the one exception — their genesis is committed (non-preprocessed) and +//! kept private, exactly as the monolithic prover does, with correctness enforced by +//! the GlobalMemory bus rather than ELF recomputation (so the verifier never sees the +//! raw private input). //! //! The local-to-global columns are range-checked in the epoch proof (which //! carries the BITWISE provider): values are bytes, and the cross-epoch-only @@ -98,9 +102,18 @@ fn epoch_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 { +fn global_transcript( + elf_bytes: &[u8], + num_epochs: usize, + num_private_input_pages: usize, +) -> 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, + num_private_input_pages, + ); transcript } @@ -173,11 +186,17 @@ fn l2g_memory_air( /// GLOBAL_MEMORY AIR for one touched page (the cross-epoch analog of PAGE). /// /// It sends each cell's genesis init and receives its finalization on the -/// GlobalMemory bus. The genesis `init` column is preprocessed, so the verifier -/// recomputes its commitment from the ELF — exactly PAGE's binding mechanism: -/// ELF-data pages via `page::compute_precomputed_commitment`, zero-init pages -/// (stack/heap) via the static zero-page commitment. The prover cannot choose -/// the genesis values. +/// GlobalMemory bus. For ELF/runtime pages the genesis `init` column is +/// preprocessed, so the verifier recomputes its commitment from the ELF — exactly +/// PAGE's binding mechanism: ELF-data pages via `page::compute_precomputed_commitment`, +/// zero-init pages (stack/heap) via the static zero-page commitment. The prover +/// cannot choose those genesis values. +/// +/// Private-input pages are built NON-preprocessed (mirrors the monolithic PAGE in +/// `VmAirs::new`): INIT is a committed main-trace column the verifier never recomputes, +/// so the verifier never sees the private genesis bytes. Correctness is enforced by +/// the GlobalMemory bus (the genesis token must telescope into the epochs' reads), not +/// by recomputation from the ELF. fn global_memory_air( opts: &ProofOptions, config: &PageConfig, @@ -191,6 +210,9 @@ fn global_memory_air( 1, empty_constraints(), ); + if config.is_private_input { + return air; + } let commitment = if config.init_values.is_some() { page::compute_precomputed_commitment(config, opts) } else { @@ -199,23 +221,37 @@ fn global_memory_air( air.with_preprocessed(commitment, global_memory::NUM_PREPROCESSED_COLS) } -/// The touched pages (sorted) and their ELF-derived genesis configs, rebuilt -/// identically by prover and verifier from the ELF + private input. Each cell -/// the program touched lives on one of these pages; a page in the ELF/input -/// image carries its bytes as `init`, every other (stack/heap) page is zero-init. +/// The touched pages (sorted) and their genesis configs, for the VERIFIER: built from +/// the ELF alone (no private bytes). Each cell the program touched lives on one of +/// these pages; an ELF data page carries its bytes as `init`, every other (stack/heap) +/// page is zero-init. +/// +/// Private-input pages are built NON-preprocessed, so the verifier never recomputes +/// their genesis from the ELF and never needs the raw private bytes. They are +/// identified EXACTLY as the monolithic verifier does — the first +/// `num_private_input_pages` pages from `PRIVATE_INPUT_START_INDEX` (see +/// [`is_private_input_page`]). fn global_memory_configs( boundaries: &[Vec], elf: &Elf, - private_inputs: &[u8], + num_private_input_pages: usize, ) -> Vec { - let image = build_initial_image_paged(elf, private_inputs); + // No private bytes: the verifier only builds the AIRs, and private-input pages are + // non-preprocessed (their INIT is never recomputed). + let image = build_initial_image_paged(elf, &[]); let init_page_data = build_init_page_data(&image); - global_memory_configs_from_init_page_data(boundaries, &init_page_data) + global_memory_configs_from_init_page_data(boundaries, &init_page_data, num_private_input_pages) } +/// Shared genesis-config builder for prover and verifier. `init_page_data` holds each +/// page's genesis bytes (ELF + private input on the prover side; ELF only on the verifier +/// side). Private-input pages are built NON-preprocessed: on the prover their committed +/// INIT column carries the genesis bytes from `init_page_data`; on the verifier the AIR +/// is non-preprocessed so those bytes are irrelevant. fn global_memory_configs_from_init_page_data( boundaries: &[Vec], init_page_data: &HashMap>, + num_private_input_pages: usize, ) -> Vec { let touched_pages: std::collections::BTreeSet = boundaries .iter() @@ -224,13 +260,48 @@ fn global_memory_configs_from_init_page_data( .collect(); touched_pages .into_iter() - .map(|page_base| match init_page_data.get(&page_base) { - Some(data) => PageConfig::with_data(page_base, data.clone()), - None => PageConfig::zero_init(page_base), + .map(|page_base| { + if is_private_input_page(page_base, num_private_input_pages) { + let data = init_page_data.get(&page_base).cloned().unwrap_or_default(); + PageConfig::with_private_input(page_base, data) + } else { + match init_page_data.get(&page_base) { + Some(data) => PageConfig::with_data(page_base, data.clone()), + None => PageConfig::zero_init(page_base), + } + } }) .collect() } +/// Whether `page_base` is one of the first `num_private_input_pages` pages starting at +/// `PRIVATE_INPUT_START_INDEX` — the page-aligned span private input actually occupies. +/// This matches the monolithic verifier's `page_configs_from_elf_and_runtime` exactly, +/// so the continuation classifies private pages identically to the monolithic path and +/// only ever marks pages that private input actually occupies. Classifying by the count +/// (not the raw `[START, START+MAX_PRIVATE_INPUT_SIZE)` byte range) also keeps this sound +/// regardless of whether the region end is page-aligned: a byte-range test would mark a +/// partial end page private even with no private input, dropping the ELF genesis binding +/// for any program data in that page's tail beyond the region. +fn is_private_input_page(page_base: u64, num_private_input_pages: usize) -> bool { + use executor::vm::memory::PRIVATE_INPUT_START_INDEX; + let page_size = page::DEFAULT_PAGE_SIZE as u64; + let end = PRIVATE_INPUT_START_INDEX + num_private_input_pages as u64 * page_size; + (PRIVATE_INPUT_START_INDEX..end).contains(&page_base) +} + +/// Number of pages the private input occupies, starting at `PRIVATE_INPUT_START_INDEX`. +/// Mirrors the monolithic prover (`from_elf_and_logs`): the wire format is a 4-byte +/// length prefix plus the data, and `PRIVATE_INPUT_START_INDEX` is page-aligned, so the +/// span is `ceil((4 + len) / page_size)` consecutive pages (0 when there is no input). +fn private_input_page_count(private_inputs: &[u8]) -> usize { + if private_inputs.is_empty() { + return 0; + } + let total_bytes = 4 + private_inputs.len(); + total_bytes.div_ceil(page::DEFAULT_PAGE_SIZE) +} + /// Per-epoch register state and label. struct EpochStart<'a> { register_init: &'a [u32], @@ -274,8 +345,14 @@ struct EpochProof { } /// A self-contained continuation proof: the per-epoch proofs in execution order, -/// the one cross-epoch global-memory proof, and the private inputs (needed to -/// rebuild the genesis image — bound by the global proof's genesis-from-ELF check). +/// the one cross-epoch global-memory proof, and the number of private-input pages. +/// +/// The raw private input is NOT carried (mirrors `VmProof.num_private_input_pages`): +/// private-input genesis lives in committed, bus-enforced GLOBAL_MEMORY columns the +/// verifier never recomputes, so the bytes stay private. The count selects which touched +/// pages are built non-preprocessed and is bound into the global proof's Fiat-Shamir +/// statement (like the monolithic path), so any wrong value diverges the verifier's +/// challenges and is rejected; it is also bound-checked up front. /// /// `verify_continuation` checks this using only the bundle and the ELF. It derives /// serde, so it round-trips through `bincode` exactly like a monolithic `VmProof`. @@ -283,7 +360,7 @@ struct EpochProof { pub struct ContinuationProof { epochs: Vec, global: MultiProof, - private_inputs: Vec, + num_private_input_pages: usize, } impl ContinuationProof { @@ -530,6 +607,7 @@ fn prove_global( boundaries: &[Vec], elf_bytes: &[u8], init_page_data: &HashMap>, + num_private_input_pages: usize, opts: &ProofOptions, ) -> Result, Error> { // Each cell's final state (boundaries are in epoch order, so the last fini wins). @@ -546,7 +624,11 @@ fn prove_global( } } - let gm_configs = global_memory_configs_from_init_page_data(boundaries, init_page_data); + let gm_configs = global_memory_configs_from_init_page_data( + boundaries, + init_page_data, + num_private_input_pages, + ); let mut l2g_traces: Vec> = boundaries .iter() @@ -577,7 +659,7 @@ fn prove_global( Prover::multi_prove( pairs, - &mut global_transcript(elf_bytes, boundaries.len()), + &mut global_transcript(elf_bytes, boundaries.len(), num_private_input_pages), #[cfg(feature = "disk-spill")] stark::storage_mode::StorageMode::Ram, ) @@ -589,7 +671,7 @@ fn verify_global( proof: &MultiProof, elf: &Elf, elf_bytes: &[u8], - private_inputs: &[u8], + num_private_input_pages: usize, opts: &ProofOptions, ) -> bool { // One L2G air per epoch, each with its own 1-based `fini_epoch` constant — @@ -597,10 +679,15 @@ 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(); - // 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. - let gm_configs = global_memory_configs(boundaries, elf, private_inputs); + // Rebuild the genesis configs FROM THE ELF (no private bytes) and recompute their + // commitments: this is the binding for ELF/runtime pages — a prover that claimed + // different genesis values would commit a different root and fail to verify. + // Private-input pages (the first `num_private_input_pages` from + // PRIVATE_INPUT_START_INDEX) are built non-preprocessed, so the verifier never + // recomputes (or sees) their genesis bytes; the GlobalMemory bus enforces them. A + // wrong `num_private_input_pages` flips a touched page's preprocessed mode, so the + // rebuilt AIR no longer matches the committed trace and `multi_verify` rejects. + let gm_configs = global_memory_configs(boundaries, elf, num_private_input_pages); let gm_airs: Vec<_> = gm_configs .iter() .map(|config| global_memory_air(opts, config)) @@ -614,7 +701,7 @@ fn verify_global( Verifier::multi_verify( &refs, proof, - &mut global_transcript(elf_bytes, boundaries.len()), + &mut global_transcript(elf_bytes, boundaries.len(), num_private_input_pages), &FieldElement::zero(), ) } @@ -751,12 +838,19 @@ pub fn prove_continuation( // One global LogUp over all the (kept) local-to-global 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 num_private_input_pages = private_input_page_count(private_inputs); + let global = prove_global( + &all_boundaries, + elf_bytes, + &init_page_data, + num_private_input_pages, + opts, + )?; Ok(ContinuationProof { epochs, global, - private_inputs: private_inputs.to_vec(), + num_private_input_pages, }) } @@ -782,10 +876,17 @@ pub fn verify_continuation( bundle: &ContinuationProof, opts: &ProofOptions, ) -> Result>, Error> { - if bundle.private_inputs.len() as u64 > MAX_PRIVATE_INPUT_SIZE { + // Bound the claimed private-input page count before using it to size/allocate AIRs + // (mirrors `verify_with_options`). The count is also bound into the global proof's + // Fiat-Shamir statement (`absorb_continuation_global_statement`), so any wrong value + // diverges the verifier's challenges and `verify_global`'s `multi_verify` rejects — + // on top of the committed-AIR-shape mismatch a wrong count causes on a touched page. + let max_private_input_pages = + (MAX_PRIVATE_INPUT_SIZE as usize + 4).div_ceil(page::DEFAULT_PAGE_SIZE) + 1; + if bundle.num_private_input_pages > max_private_input_pages { return Err(Error::InvalidTableCounts(format!( - "private input size ({}) exceeds max ({MAX_PRIVATE_INPUT_SIZE})", - bundle.private_inputs.len() + "num_private_input_pages ({}) exceeds max ({max_private_input_pages})", + bundle.num_private_input_pages ))); } @@ -836,8 +937,10 @@ pub fn verify_continuation( 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 for ELF/runtime pages is rebuilt FROM THE ELF + // (no private bytes), so the starting memory cannot be prover-chosen; the bus + // telescopes fini→init. Private-input pages are committed, non-preprocessed (genesis + // stays private), bus-enforced. let all_boundaries: Vec> = bundle.epochs.iter().map(|e| e.boundary.clone()).collect(); if !verify_global( @@ -845,7 +948,7 @@ pub fn verify_continuation( &bundle.global, &elf, elf_bytes, - &bundle.private_inputs, + bundle.num_private_input_pages, opts, ) { return Ok(None); @@ -1141,21 +1244,65 @@ mod tests { ); } - // Negative: the verifier rebuilds private-input genesis from bundle bytes. - // Changing those bytes after proving changes the global-memory preprocessed - // genesis commitment, so the standalone verifier must reject. + // Private input must stay private under continuations. The bundle carries no raw + // private bytes (only `num_private_input_pages`), yet a multi-epoch continuation of + // a program that reads private input verifies from the bundle + ELF ALONE and + // reconstructs the committed output. Regression for the genesis leak: the global + // proof's private-input genesis is a committed, bus-enforced column, not a + // preprocessed value the verifier would have to recompute from the raw bytes. #[test] - fn test_split_verify_rejects_tampered_private_input_genesis() { + fn test_continuation_private_input_verifies_without_bytes() { let _ = env_logger::builder().is_test(true).try_init(); let elf_bytes = asm_elf_bytes("test_private_input_xpage"); - let private_inputs: Vec = (0u8..16).collect(); - let mut bundle = prove_continuation( - &elf_bytes, - &private_inputs, - 4, - &ProofOptions::default_test_options(), - ) - .unwrap(); + let input: Vec = (0u8..16).collect(); + let expected = input[4..12].to_vec(); + + // Smallest epochs (2^2 = 4 cycles) so the short program splits across epochs. + let bundle = + prove_continuation(&elf_bytes, &input, 2, &ProofOptions::default_test_options()) + .unwrap(); + assert!( + bundle.num_epochs() > 1, + "4-cycle epochs must split the run into multiple epochs" + ); + assert!( + bundle.num_private_input_pages > 0, + "a program that reads private input must have a private-input page in the global proof" + ); + + // The serialized bundle must carry no raw private bytes: it survives a bincode + // round-trip and still verifies using ONLY the bundle + ELF (no private input + // is passed to `verify_continuation`). + let bytes = bincode::serialize(&bundle).unwrap(); + let restored: ContinuationProof = bincode::deserialize(&bytes).unwrap(); + let out = verify_continuation(&elf_bytes, &restored, &ProofOptions::default_test_options()) + .unwrap(); + assert_eq!( + out.as_deref(), + Some(&expected[..]), + "continuation with private input must verify from the bundle + ELF alone" + ); + } + + // Negative: `num_private_input_pages` is pinned by the committed AIR shape for TOUCHED + // pages. Deflating it to 0 for a program that reads private input makes the verifier + // build that touched page preprocessed (ELF-recomputed → zero-init commitment) while + // the prover committed it non-preprocessed, so the rebuilt AIR no longer matches the + // committed trace and verification rejects. This is the replacement for the removed + // tampered-genesis test: it guards the security claim that a wrong count flipping a + // touched page's preprocessed mode cannot be accepted. + #[test] + fn test_split_verify_rejects_deflated_num_private_input_pages() { + let _ = env_logger::builder().is_test(true).try_init(); + let elf_bytes = asm_elf_bytes("test_private_input_xpage"); + let input: Vec = (0u8..16).collect(); + let mut bundle = + prove_continuation(&elf_bytes, &input, 2, &ProofOptions::default_test_options()) + .unwrap(); + assert!( + bundle.num_private_input_pages > 0, + "baseline must have a touched private-input page" + ); assert!( verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()) .unwrap() @@ -1163,23 +1310,66 @@ mod tests { "baseline must verify before tampering" ); - bundle.private_inputs[4] ^= 0xFF; + bundle.num_private_input_pages = 0; assert!( verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()) .unwrap() - .is_none() + .is_none(), + "deflating the count flips a touched page's preprocessed mode → must reject" + ); + } + + // Private-input page classification is count-based (the first `n` pages from + // PRIVATE_INPUT_START_INDEX), matching the monolithic verifier — the classification + // depends ONLY on the count, never on the raw private-input byte range. This is what + // keeps the continuation from ever marking more pages private than the monolithic + // path would: with no private input, no page in the region is private, so program + // data anywhere in the private-input address space keeps its ELF genesis binding. + #[test] + fn test_private_input_page_classification_is_count_based() { + use executor::vm::memory::{MAX_PRIVATE_INPUT_SIZE, PRIVATE_INPUT_START_INDEX}; + let page_size = page::DEFAULT_PAGE_SIZE as u64; + let start = PRIVATE_INPUT_START_INDEX; + + // With no private input, NO page in the private-input region is private — not the + // first page, not the last. Classification is by count alone, not the region span. + let region_pages = MAX_PRIVATE_INPUT_SIZE / page_size; + let last_region_page = start + (region_pages - 1) * page_size; + assert!(!is_private_input_page(start, 0)); + assert!(!is_private_input_page(last_region_page, 0)); + + // Count n → exactly the first n pages from start. + assert!(is_private_input_page(start, 1)); + assert!(!is_private_input_page(start + page_size, 1)); + assert!(is_private_input_page(start + page_size, 2)); + // Pages below the region are never private. + assert!(!is_private_input_page(start - page_size, 10)); + + // private_input_page_count: wire format is [len:4][data], region is page-aligned. + assert_eq!(private_input_page_count(&[]), 0); + assert_eq!(private_input_page_count(&[0u8; 16]), 1); + // 4-byte prefix + (page_size - 4) data exactly fills one page. + assert_eq!( + private_input_page_count(&vec![0u8; page::DEFAULT_PAGE_SIZE - 4]), + 1 + ); + // One more byte spills into a second page. + assert_eq!( + private_input_page_count(&vec![0u8; page::DEFAULT_PAGE_SIZE - 3]), + 2 ); } - // Negative: verifier-side private inputs are deserialized/untrusted, so reject - // oversized bundles before rebuilding genesis page configs from them. + // Negative: `num_private_input_pages` is deserialized/untrusted, so reject a bundle + // whose count exceeds the max before using it to size/build the global AIRs. #[test] - fn test_split_verify_rejects_oversized_private_inputs() { + fn test_split_verify_rejects_oversized_num_private_input_pages() { let _ = env_logger::builder().is_test(true).try_init(); let elf_bytes = asm_elf_bytes("all_loadstore_32"); let mut bundle = - prove_continuation(&elf_bytes, &[], 8, &ProofOptions::default_test_options()).unwrap(); - bundle.private_inputs = vec![0; MAX_PRIVATE_INPUT_SIZE as usize + 1]; + prove_continuation(&elf_bytes, &[], 3, &ProofOptions::default_test_options()).unwrap(); + let max_pages = (MAX_PRIVATE_INPUT_SIZE as usize + 4).div_ceil(page::DEFAULT_PAGE_SIZE) + 1; + bundle.num_private_input_pages = max_pages + 1; assert!(matches!( verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()), Err(Error::InvalidTableCounts(_)) diff --git a/prover/src/statement.rs b/prover/src/statement.rs index cca961be5..f4a27ff62 100644 --- a/prover/src/statement.rs +++ b/prover/src/statement.rs @@ -123,15 +123,19 @@ 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 -/// (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. +/// 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), +/// and the private-input page count (so the global proof's AIR layout — which touched +/// pages are built non-preprocessed — is canonically pinned, like the monolithic +/// path's `absorb_statement`). 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, + num_private_input_pages: usize, ) { 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(&(num_private_input_pages as u64).to_le_bytes()); } diff --git a/prover/src/tables/global_memory.rs b/prover/src/tables/global_memory.rs index 81f6ea630..ce343df5e 100644 --- a/prover/src/tables/global_memory.rs +++ b/prover/src/tables/global_memory.rs @@ -8,10 +8,15 @@ //! touched it). Untouched bytes send and receive the identical token, so they //! cancel — exactly as PAGE's init/fini bookend does on the epoch-local bus. //! -//! Because the genesis value lives in a PREPROCESSED column (OFFSET + INIT, -//! byte-for-byte identical to PAGE's), the verifier recomputes the same -//! commitment from the ELF via [`page::compute_precomputed_commitment`]. This -//! binds the program's initial memory to the ELF binary. +//! For ELF/runtime pages the genesis value lives in a PREPROCESSED column (OFFSET + +//! INIT, byte-for-byte identical to PAGE's), so the verifier recomputes the same +//! commitment from the ELF via [`page::compute_precomputed_commitment`]. This binds +//! the program's initial memory to the ELF binary. +//! +//! Private-input pages are the exception: the AIR is built NON-preprocessed (see +//! `continuation::global_memory_air`), so INIT is a committed main-trace column the +//! verifier never recomputes — the private genesis bytes stay private and correctness +//! is enforced by the GlobalMemory bus, exactly as the monolithic PAGE does. //! //! ## Columns //! diff --git a/prover/src/tests/statement_tests.rs b/prover/src/tests/statement_tests.rs index 73944e262..f8759f529 100644 --- a/prover/src/tests/statement_tests.rs +++ b/prover/src/tests/statement_tests.rs @@ -163,16 +163,29 @@ 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, num_private_input_pages: usize) -> [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, num_private_input_pages); 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_private_pages() { + let baseline = global_state(b"elf", 3, 1); + assert_eq!(baseline, global_state(b"elf", 3, 1)); // deterministic + assert_ne!( + baseline, + global_state(b"elf", 4, 1), + "must bind epoch count" + ); + assert_ne!( + baseline, + global_state(b"other-elf", 3, 1), + "must bind the ELF" + ); + assert_ne!( + baseline, + global_state(b"elf", 3, 2), + "must bind the private-input page count" + ); } From e724c31ae31c3eacfa0e2665c449ce1a56e8f3bc Mon Sep 17 00:00:00 2001 From: Nicole Date: Wed, 1 Jul 2026 14:29:18 -0300 Subject: [PATCH 02/14] Enforce the private-input region reservation in Elf::load --- docs/continuations_design.md | 10 ++++ executor/src/elf.rs | 91 ++++++++++++++++++++++++++++++++++++ prover/src/continuation.rs | 36 ++++++++------ 3 files changed, 123 insertions(+), 14 deletions(-) diff --git a/docs/continuations_design.md b/docs/continuations_design.md index a985a1223..48155fd61 100644 --- a/docs/continuations_design.md +++ b/docs/continuations_design.md @@ -252,6 +252,16 @@ private genesis is prover-supplied *by design* (it is the private input), so the attests "**there exists** a private input producing this output" — the intended semantics, identical to the monolithic prover. +**One prerequisite — the region must hold only private input.** Skipping the ELF +recomputation is safe *only* if no ELF-declared data lives in the private-input region; +otherwise a prover could classify that page private and forge the ELF byte's genesis +(the value would be committed but never checked against the ELF). This reservation is +**enforced by the loader**: `Elf::load` rejects any `PT_LOAD` segment overlapping +`[PRIVATE_INPUT_START_INDEX, +MAX_PRIVATE_INPUT_SIZE)` (`ElfError::SegmentInPrivateInputRegion`). +Turning the reservation from convention into an enforced invariant closes this gap for +**both** the continuation and monolithic paths (they share the loader and the same +non-preprocessed-private-page design). + **Which pages are private** is decided by **count**, not by the raw byte range: the first `num_private_input_pages` pages from `PRIVATE_INPUT_START_INDEX` (the page-aligned span the input occupies), exactly matching the monolithic verifier's diff --git a/executor/src/elf.rs b/executor/src/elf.rs index ed79fb983..98a6f7391 100644 --- a/executor/src/elf.rs +++ b/executor/src/elf.rs @@ -246,6 +246,8 @@ pub enum ElfError { UnalignedVAddr, #[error("Program Header address is too large")] AddrTooLarge, + #[error("Program Header overlaps the reserved private-input region")] + SegmentInPrivateInputRegion, #[error("Program Header offset is invalid")] InvalidOffset, #[error("Executable Header size is invalid")] @@ -290,6 +292,22 @@ impl Elf { if !program_header.p_vaddr.is_multiple_of(WORD_SIZE) { return Err(ElfError::UnalignedVAddr); } + // Reject any loadable segment that overlaps the reserved private-input region + // `[PRIVATE_INPUT_START_INDEX, +MAX_PRIVATE_INPUT_SIZE)`. Genesis for pages in + // that region is prover-committed and NOT recomputed from the ELF (so private + // input stays private); ELF data placed there would have an unbound, prover- + // forgeable genesis. Forbidding the overlap turns "the region holds only private + // input" from a convention into an enforced invariant. `store_private_inputs` + // writes the runtime private input separately, so this does not affect it. + if program_header.p_memsz > 0 { + use crate::vm::memory::{MAX_PRIVATE_INPUT_SIZE, PRIVATE_INPUT_START_INDEX}; + let seg_start = program_header.p_vaddr; + let seg_end = seg_start.saturating_add(program_header.p_memsz); + let region_end = PRIVATE_INPUT_START_INDEX.saturating_add(MAX_PRIVATE_INPUT_SIZE); + if seg_start < region_end && seg_end > PRIVATE_INPUT_START_INDEX { + return Err(ElfError::SegmentInPrivateInputRegion); + } + } let mut values = Vec::new(); for i in (0..program_header.p_memsz).step_by(WORD_SIZE as usize) { let word = if i < program_header.p_filesz { @@ -558,3 +576,76 @@ impl SymbolTable { self.functions.len() } } + +#[cfg(test)] +mod tests { + use super::*; + use crate::vm::memory::{MAX_PRIVATE_INPUT_SIZE, PRIVATE_INPUT_START_INDEX}; + + /// Build a minimal valid RISC-V ET_EXEC ELF with a single PT_LOAD segment at + /// `p_vaddr` of `p_memsz` bytes (all BSS: `p_filesz = 0`). Enough for `Elf::load`, + /// which only parses the executable header + program headers. + fn minimal_elf_with_segment(p_vaddr: u64, p_memsz: u64) -> Vec { + let mut buf = vec![0u8; EXECUTABLE_HEADER_SIZE + PROGRAM_HEADER_SIZE]; + // e_ident + buf[0..4].copy_from_slice(&[0x7F, b'E', b'L', b'F']); + buf[4] = ELF_64_BIT; + buf[5] = ELF_LITTLE_ENDIAN; + buf[6] = ELF_CURRENT_VERSION; + buf[16..18].copy_from_slice(&ET_EXEC.to_le_bytes()); + buf[18..20].copy_from_slice(&EM_RISCV.to_le_bytes()); + buf[20..24].copy_from_slice(&1u32.to_le_bytes()); // e_version + buf[24..32].copy_from_slice(&0x10000u64.to_le_bytes()); // e_entry (word-aligned) + buf[32..40].copy_from_slice(&(EXECUTABLE_HEADER_SIZE as u64).to_le_bytes()); // e_phoff + buf[52..54].copy_from_slice(&(EXECUTABLE_HEADER_SIZE as u16).to_le_bytes()); // e_ehsize + buf[54..56].copy_from_slice(&(PROGRAM_HEADER_SIZE as u16).to_le_bytes()); // e_phentsize + buf[56..58].copy_from_slice(&1u16.to_le_bytes()); // e_phnum + // single program header + let ph = EXECUTABLE_HEADER_SIZE; + buf[ph..ph + 4].copy_from_slice(&PT_LOAD.to_le_bytes()); + buf[ph + 4..ph + 8].copy_from_slice(&PF_X.to_le_bytes()); + buf[ph + 16..ph + 24].copy_from_slice(&p_vaddr.to_le_bytes()); // p_vaddr + buf[ph + 40..ph + 48].copy_from_slice(&p_memsz.to_le_bytes()); // p_memsz + buf + } + + #[test] + fn rejects_segment_inside_private_input_region() { + // An ELF data segment placed inside the reserved region would get a prover-chosen, + // ELF-unbound genesis (private-input pages are non-preprocessed) — must be rejected. + let elf = minimal_elf_with_segment(PRIVATE_INPUT_START_INDEX, 4); + assert!(matches!( + Elf::load(&elf), + Err(ElfError::SegmentInPrivateInputRegion) + )); + } + + #[test] + fn rejects_segment_straddling_region_start() { + // Ends 4 bytes into the region → overlaps → rejected. + let elf = minimal_elf_with_segment(PRIVATE_INPUT_START_INDEX - 4, 8); + assert!(matches!( + Elf::load(&elf), + Err(ElfError::SegmentInPrivateInputRegion) + )); + } + + #[test] + fn accepts_segment_below_region() { + assert!(Elf::load(&minimal_elf_with_segment(0x10000, 4)).is_ok()); + } + + #[test] + fn accepts_segment_ending_exactly_at_region_start() { + // seg_end == PRIVATE_INPUT_START_INDEX (exclusive) → no overlap → accepted. + let elf = minimal_elf_with_segment(PRIVATE_INPUT_START_INDEX - 4, 4); + assert!(Elf::load(&elf).is_ok()); + } + + #[test] + fn accepts_segment_at_region_end() { + // Starts exactly at the region end → no overlap → accepted. + let region_end = PRIVATE_INPUT_START_INDEX + MAX_PRIVATE_INPUT_SIZE; + assert!(Elf::load(&minimal_elf_with_segment(region_end, 4)).is_ok()); + } +} diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index ba0439847..7488d1dcc 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -276,13 +276,18 @@ fn global_memory_configs_from_init_page_data( /// Whether `page_base` is one of the first `num_private_input_pages` pages starting at /// `PRIVATE_INPUT_START_INDEX` — the page-aligned span private input actually occupies. -/// This matches the monolithic verifier's `page_configs_from_elf_and_runtime` exactly, -/// so the continuation classifies private pages identically to the monolithic path and -/// only ever marks pages that private input actually occupies. Classifying by the count -/// (not the raw `[START, START+MAX_PRIVATE_INPUT_SIZE)` byte range) also keeps this sound -/// regardless of whether the region end is page-aligned: a byte-range test would mark a -/// partial end page private even with no private input, dropping the ELF genesis binding -/// for any program data in that page's tail beyond the region. +/// This matches the monolithic verifier's `page_configs_from_elf_and_runtime` exactly, so +/// the continuation classifies private pages identically to the monolithic path. Classifying +/// by the count (not the raw `[START, START+MAX_PRIVATE_INPUT_SIZE)` byte range) keeps prover +/// and verifier in lockstep regardless of whether the region end is page-aligned. +/// +/// NOTE (shared with the monolithic path): a page classified private is built +/// non-preprocessed, so its genesis is NOT recomputed from the ELF. This is safe because +/// the private-input region is reserved for private input and the reservation is enforced: +/// `Elf::load` rejects any loadable segment overlapping +/// `[PRIVATE_INPUT_START_INDEX, +MAX_PRIVATE_INPUT_SIZE)` +/// (`ElfError::SegmentInPrivateInputRegion`), so no ELF-declared data can live there and +/// have its genesis go unbound. fn is_private_input_page(page_base: u64, num_private_input_pages: usize) -> bool { use executor::vm::memory::PRIVATE_INPUT_START_INDEX; let page_size = page::DEFAULT_PAGE_SIZE as u64; @@ -600,9 +605,11 @@ fn verify_epoch( /// 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. +/// cell's genesis init and receives its final value. For ELF/runtime pages the genesis +/// is preprocessed (the verifier recomputes it from the ELF); private-input pages are +/// non-preprocessed (committed, bus-enforced genesis — see `global_memory_air` / §3.6). +/// The bus balances iff every `fini` matches the next epoch's `init` and every genesis +/// matches its source (the ELF for ELF/runtime pages). fn prove_global( boundaries: &[Vec], elf_bytes: &[u8], @@ -1321,10 +1328,11 @@ mod tests { // Private-input page classification is count-based (the first `n` pages from // PRIVATE_INPUT_START_INDEX), matching the monolithic verifier — the classification - // depends ONLY on the count, never on the raw private-input byte range. This is what - // keeps the continuation from ever marking more pages private than the monolithic - // path would: with no private input, no page in the region is private, so program - // data anywhere in the private-input address space keeps its ELF genesis binding. + // depends ONLY on the count, never on the raw private-input byte range. So with no + // private input, no page in the region is classified private (checked below), keeping + // the continuation from ever marking more pages private than the monolithic path would. + // (ELF data cannot be placed *inside* the reserved region: `Elf::load` rejects any + // segment overlapping it, so a private page never holds ELF-bound data.) #[test] fn test_private_input_page_classification_is_count_based() { use executor::vm::memory::{MAX_PRIVATE_INPUT_SIZE, PRIVATE_INPUT_START_INDEX}; From 3cab6b6f450fce1b913025a6cf0561c84bbd60d7 Mon Sep 17 00:00:00 2001 From: Nicole Date: Wed, 1 Jul 2026 15:26:00 -0300 Subject: [PATCH 03/14] Reserve the full classifiable private-input span in Elf::load --- docs/continuations_design.md | 7 +++-- executor/src/elf.rs | 55 +++++++++++++++++++++++++----------- prover/src/continuation.rs | 9 +++--- 3 files changed, 48 insertions(+), 23 deletions(-) diff --git a/docs/continuations_design.md b/docs/continuations_design.md index 48155fd61..3289a69fc 100644 --- a/docs/continuations_design.md +++ b/docs/continuations_design.md @@ -256,8 +256,11 @@ semantics, identical to the monolithic prover. recomputation is safe *only* if no ELF-declared data lives in the private-input region; otherwise a prover could classify that page private and forge the ELF byte's genesis (the value would be committed but never checked against the ELF). This reservation is -**enforced by the loader**: `Elf::load` rejects any `PT_LOAD` segment overlapping -`[PRIVATE_INPUT_START_INDEX, +MAX_PRIVATE_INPUT_SIZE)` (`ElfError::SegmentInPrivateInputRegion`). +**enforced by the loader**: `Elf::load` rejects any `PT_LOAD` segment reaching at or above +`PRIVATE_INPUT_START_INDEX` (`ElfError::SegmentInPrivateInputRegion`) — covering every page +the verifier can classify private, which slightly exceeds `[base, base+MAX_PRIVATE_INPUT_SIZE)` +(the length prefix pushes an honest max-size input onto one more page, plus a page of +count-bound slack). Turning the reservation from convention into an enforced invariant closes this gap for **both** the continuation and monolithic paths (they share the loader and the same non-preprocessed-private-page design). diff --git a/executor/src/elf.rs b/executor/src/elf.rs index 98a6f7391..e019d54a1 100644 --- a/executor/src/elf.rs +++ b/executor/src/elf.rs @@ -292,19 +292,25 @@ impl Elf { if !program_header.p_vaddr.is_multiple_of(WORD_SIZE) { return Err(ElfError::UnalignedVAddr); } - // Reject any loadable segment that overlaps the reserved private-input region - // `[PRIVATE_INPUT_START_INDEX, +MAX_PRIVATE_INPUT_SIZE)`. Genesis for pages in - // that region is prover-committed and NOT recomputed from the ELF (so private - // input stays private); ELF data placed there would have an unbound, prover- - // forgeable genesis. Forbidding the overlap turns "the region holds only private - // input" from a convention into an enforced invariant. `store_private_inputs` - // writes the runtime private input separately, so this does not affect it. + // Reject any loadable segment that reaches at or above `PRIVATE_INPUT_START_INDEX` + // — the base of the reserved high-memory private-input area. Genesis for pages in + // that area is prover-committed and NOT recomputed from the ELF (so private input + // stays private); ELF data placed there would have an unbound, prover-forgeable + // genesis. The verifier can classify any page from the base up to the maximum + // private-input page count as private — a span that slightly exceeds + // `MAX_PRIVATE_INPUT_SIZE` (the length prefix pushes an honest max-size input onto + // one more page, and the page-count bound adds a page of slack), so we reserve the + // whole high area rather than exactly `[base, base+MAX)`. Nothing legitimate loads + // here: ELF code/data live at low addresses, and the stack (`STACK_TOP`) and + // private input are runtime regions written outside `load_program`, so this does + // not affect them. Turns "the private-input area holds only private input" from a + // convention into an enforced invariant. if program_header.p_memsz > 0 { - use crate::vm::memory::{MAX_PRIVATE_INPUT_SIZE, PRIVATE_INPUT_START_INDEX}; - let seg_start = program_header.p_vaddr; - let seg_end = seg_start.saturating_add(program_header.p_memsz); - let region_end = PRIVATE_INPUT_START_INDEX.saturating_add(MAX_PRIVATE_INPUT_SIZE); - if seg_start < region_end && seg_end > PRIVATE_INPUT_START_INDEX { + use crate::vm::memory::PRIVATE_INPUT_START_INDEX; + let seg_end = program_header + .p_vaddr + .saturating_add(program_header.p_memsz); + if seg_end > PRIVATE_INPUT_START_INDEX { return Err(ElfError::SegmentInPrivateInputRegion); } } @@ -643,9 +649,26 @@ mod tests { } #[test] - fn accepts_segment_at_region_end() { - // Starts exactly at the region end → no overlap → accepted. - let region_end = PRIVATE_INPUT_START_INDEX + MAX_PRIVATE_INPUT_SIZE; - assert!(Elf::load(&minimal_elf_with_segment(region_end, 4)).is_ok()); + fn rejects_segment_at_max_size_boundary() { + // The `[base, base+MAX)` byte cap ends here, but an honest max-size input (plus its + // 4-byte length prefix) spills onto this page, so the verifier can classify it private. + // It must therefore be rejected too — the reservation covers the full classifiable + // span, not just `[base, base+MAX)`. + let boundary = PRIVATE_INPUT_START_INDEX + MAX_PRIVATE_INPUT_SIZE; + assert!(matches!( + Elf::load(&minimal_elf_with_segment(boundary, 4)), + Err(ElfError::SegmentInPrivateInputRegion) + )); + } + + #[test] + fn rejects_segment_far_above_region() { + // Any segment reaching at/above the private-input base is rejected — nothing + // legitimate loads that high (ELF is low; stack/private input are runtime). + let high = PRIVATE_INPUT_START_INDEX + MAX_PRIVATE_INPUT_SIZE + (16 << 20); + assert!(matches!( + Elf::load(&minimal_elf_with_segment(high, 4)), + Err(ElfError::SegmentInPrivateInputRegion) + )); } } diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index 7488d1dcc..5565a00ed 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -283,11 +283,10 @@ fn global_memory_configs_from_init_page_data( /// /// NOTE (shared with the monolithic path): a page classified private is built /// non-preprocessed, so its genesis is NOT recomputed from the ELF. This is safe because -/// the private-input region is reserved for private input and the reservation is enforced: -/// `Elf::load` rejects any loadable segment overlapping -/// `[PRIVATE_INPUT_START_INDEX, +MAX_PRIVATE_INPUT_SIZE)` -/// (`ElfError::SegmentInPrivateInputRegion`), so no ELF-declared data can live there and -/// have its genesis go unbound. +/// the private-input area is reserved and the reservation is enforced: `Elf::load` rejects +/// any loadable segment reaching at/above `PRIVATE_INPUT_START_INDEX` +/// (`ElfError::SegmentInPrivateInputRegion`) — covering every page this function can +/// classify private — so no ELF-declared data can live there and have its genesis go unbound. fn is_private_input_page(page_base: u64, num_private_input_pages: usize) -> bool { use executor::vm::memory::PRIVATE_INPUT_START_INDEX; let page_size = page::DEFAULT_PAGE_SIZE as u64; From b7476a4d58371a2f3ba3164a9d39a37e223aacf4 Mon Sep 17 00:00:00 2001 From: Nicole Date: Wed, 1 Jul 2026 15:35:20 -0300 Subject: [PATCH 04/14] Add test and drop the always-zero EpochProof.num_private_input_pages --- prover/src/continuation.rs | 51 ++++++++++++++++++++++++++++---------- 1 file changed, 38 insertions(+), 13 deletions(-) diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index 5565a00ed..44954578c 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -83,7 +83,6 @@ fn epoch_transcript( elf_bytes: &[u8], public_output: &[u8], table_counts: &TableCounts, - num_private_input_pages: usize, runtime_page_ranges: &[RuntimePageRange], epoch_label: u64, ) -> DefaultTranscript { @@ -94,7 +93,9 @@ fn epoch_transcript( elf_bytes, public_output, table_counts, - num_private_input_pages, + // Continuation epochs skip PAGE (the L2G bookend replaces it), so they never + // have private-input pages — the private-input count is always 0 here. + 0, runtime_page_ranges, ); transcript @@ -330,9 +331,6 @@ struct EpochProof { public_output: Vec, /// Statement values the epoch transcript is seeded with (re-derived on verify). table_counts: TableCounts, - /// Always zero for continuation epochs: PAGE is replaced by L2G, and private - /// input genesis is carried by the continuation bundle for global verification. - num_private_input_pages: usize, /// Always empty for continuation epochs: PAGE tables are skipped, so runtime /// pages are not part of the epoch AIR statement. runtime_page_ranges: Vec, @@ -447,11 +445,6 @@ fn prove_epoch( let table_counts = traces.table_counts(); let public_output = traces.public_output_bytes.clone(); let runtime_page_ranges = traces.runtime_page_ranges(); - let num_private_input_pages = traces - .page_configs - .iter() - .filter(|c| c.is_private_input) - .count(); let airs = build_epoch_airs( elf, @@ -469,7 +462,6 @@ fn prove_epoch( elf_bytes, &public_output, &table_counts, - num_private_input_pages, &runtime_page_ranges, label, ) @@ -503,7 +495,6 @@ fn prove_epoch( proof, public_output, table_counts, - num_private_input_pages, runtime_page_ranges, reg_fini, l2g_root, @@ -564,7 +555,6 @@ fn verify_epoch( elf_bytes, &epoch.public_output, &epoch.table_counts, - epoch.num_private_input_pages, &epoch.runtime_page_ranges, label, ) @@ -1325,6 +1315,41 @@ mod tests { ); } + // Negative: inflating `num_private_input_pages` to an in-range but wrong value must also + // reject. Inflation only enlarges the private-page *range* over untouched pages (no + // touched page's preprocessed mode flips, so the committed-AIR-shape check alone would + // NOT catch it) — the count is absorbed into the global proof's Fiat-Shamir statement, so + // the verifier's challenges diverge from the prover's and `verify_global` rejects. Guards + // the FS-binding of the count (complements the deflation test's AIR-shape-mismatch path). + #[test] + fn test_split_verify_rejects_inflated_num_private_input_pages() { + let _ = env_logger::builder().is_test(true).try_init(); + let elf_bytes = asm_elf_bytes("test_private_input_xpage"); + let input: Vec = (0u8..16).collect(); + let mut bundle = + prove_continuation(&elf_bytes, &input, 2, &ProofOptions::default_test_options()) + .unwrap(); + assert_eq!( + bundle.num_private_input_pages, 1, + "16 bytes of private input fits in one page" + ); + assert!( + verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()) + .unwrap() + .is_some(), + "baseline must verify before tampering" + ); + + // In-range (well under the max bound) but one more than the true count. + bundle.num_private_input_pages = 2; + assert!( + verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()) + .unwrap() + .is_none(), + "an inflated count diverges the global Fiat-Shamir statement → must reject" + ); + } + // Private-input page classification is count-based (the first `n` pages from // PRIVATE_INPUT_START_INDEX), matching the monolithic verifier — the classification // depends ONLY on the count, never on the raw private-input byte range. So with no From f7777b1206c4f3fcf01d19c4fb47526c9bb16a22 Mon Sep 17 00:00:00 2001 From: Nicole Date: Wed, 1 Jul 2026 17:06:35 -0300 Subject: [PATCH 05/14] Stop shipping touched-cell values (including private-input bytes) in the continuation bundle by dropping EpochProof.boundary and instead carrying only the value-free, sorted touched page-base set the verifier needs, derived from a single source shared with the committed GLOBAL_MEMORY tables, canonicalized on the verify side, and bound into the global Fiat-Shamir statement. --- prover/src/continuation.rs | 256 ++++++++++++++++++++++------ prover/src/statement.rs | 17 +- prover/src/tests/statement_tests.rs | 37 +++- 3 files changed, 243 insertions(+), 67 deletions(-) diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index 44954578c..290f12559 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -107,6 +107,7 @@ fn global_transcript( elf_bytes: &[u8], num_epochs: usize, num_private_input_pages: usize, + touched_page_bases: &[u64], ) -> DefaultTranscript { let mut transcript = DefaultTranscript::::new(&[]); absorb_continuation_global_statement( @@ -114,6 +115,7 @@ fn global_transcript( elf_bytes, num_epochs, num_private_input_pages, + touched_page_bases, ); transcript } @@ -222,18 +224,46 @@ fn global_memory_air( air.with_preprocessed(commitment, global_memory::NUM_PREPROCESSED_COLS) } -/// The touched pages (sorted) and their genesis configs, for the VERIFIER: built from -/// the ELF alone (no private bytes). Each cell the program touched lives on one of -/// these pages; an ELF data page carries its bytes as `init`, every other (stack/heap) -/// page is zero-init. +/// The sorted, deduped set of page bases the touched cells fall on — the SINGLE source +/// of truth for which GLOBAL_MEMORY tables exist. The prover builds the committed tables +/// from this list, ships the identical list in the bundle (`ContinuationProof.touched_page_bases`), +/// and the verifier rebuilds the same tables from it. Sorted (BTreeSet order) so prover +/// and verifier iterate the identical sequence — `multi_verify` matches AIRs to sub-proofs +/// positionally. Carries page bases ONLY: no cell values, so private-input bytes never +/// enter the bundle (unlike the full `CellBoundary`, whose `init.value` is a private byte). +fn touched_page_bases(boundaries: &[Vec]) -> Vec { + boundaries + .iter() + .flatten() + .map(|b| page::page_base_for_address(b.address)) + .collect::>() + .into_iter() + .collect() +} + +/// Canonicalize a possibly-untrusted, out-of-order page-base list to the same sorted, +/// deduped form the prover produces via [`touched_page_bases`], so the verifier rebuilds +/// tables in the committed order regardless of the wire order (a shuffled-but-same-set +/// list still verifies; a different set fails via bus imbalance / AIR-count mismatch). +fn canonical_page_bases(page_bases: &[u64]) -> Vec { + page_bases + .iter() + .copied() + .collect::>() + .into_iter() + .collect() +} + +/// The touched pages' genesis configs, for the VERIFIER: built from the ELF alone (no +/// private bytes). `page_bases` is the canonical touched-page-base list. An ELF data page +/// carries its bytes as `init`, every other (stack/heap) page is zero-init. /// -/// Private-input pages are built NON-preprocessed, so the verifier never recomputes -/// their genesis from the ELF and never needs the raw private bytes. They are -/// identified EXACTLY as the monolithic verifier does — the first -/// `num_private_input_pages` pages from `PRIVATE_INPUT_START_INDEX` (see -/// [`is_private_input_page`]). +/// Private-input pages are built NON-preprocessed, so the verifier never recomputes their +/// genesis from the ELF and never needs the raw private bytes. They are identified EXACTLY +/// as the monolithic verifier does — the first `num_private_input_pages` pages from +/// `PRIVATE_INPUT_START_INDEX` (see [`is_private_input_page`]). fn global_memory_configs( - boundaries: &[Vec], + page_bases: &[u64], elf: &Elf, num_private_input_pages: usize, ) -> Vec { @@ -241,27 +271,23 @@ fn global_memory_configs( // non-preprocessed (their INIT is never recomputed). let image = build_initial_image_paged(elf, &[]); let init_page_data = build_init_page_data(&image); - global_memory_configs_from_init_page_data(boundaries, &init_page_data, num_private_input_pages) + global_memory_configs_from_init_page_data(page_bases, &init_page_data, num_private_input_pages) } -/// Shared genesis-config builder for prover and verifier. `init_page_data` holds each -/// page's genesis bytes (ELF + private input on the prover side; ELF only on the verifier -/// side). Private-input pages are built NON-preprocessed: on the prover their committed -/// INIT column carries the genesis bytes from `init_page_data`; on the verifier the AIR -/// is non-preprocessed so those bytes are irrelevant. +/// Shared genesis-config builder for prover and verifier, one `PageConfig` per page base +/// in `page_bases` (which must be canonical: sorted + deduped). `init_page_data` holds +/// each page's genesis bytes (ELF + private input on the prover side; ELF only on the +/// verifier side). Private-input pages are built NON-preprocessed: on the prover their +/// committed INIT column carries the genesis bytes; on the verifier the AIR is +/// non-preprocessed so those bytes are irrelevant. fn global_memory_configs_from_init_page_data( - boundaries: &[Vec], + page_bases: &[u64], init_page_data: &HashMap>, num_private_input_pages: usize, ) -> Vec { - let touched_pages: std::collections::BTreeSet = boundaries + page_bases .iter() - .flatten() - .map(|b| page::page_base_for_address(b.address)) - .collect(); - touched_pages - .into_iter() - .map(|page_base| { + .map(|&page_base| { if is_private_input_page(page_base, num_private_input_pages) { let data = init_page_data.get(&page_base).cloned().unwrap_or_default(); PageConfig::with_private_input(page_base, data) @@ -341,20 +367,22 @@ struct EpochProof { /// The committed L2G table root, tied to the global proof by /// [`verify_l2g_commitment_binding`]. l2g_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, } -/// A self-contained continuation proof: the per-epoch proofs in execution order, -/// the one cross-epoch global-memory proof, and the number of private-input pages. +/// A self-contained continuation proof: the per-epoch proofs in execution order, the one +/// cross-epoch global-memory proof, the number of private-input pages, and the touched +/// page-base set. /// -/// The raw private input is NOT carried (mirrors `VmProof.num_private_input_pages`): -/// private-input genesis lives in committed, bus-enforced GLOBAL_MEMORY columns the -/// verifier never recomputes, so the bytes stay private. The count selects which touched -/// pages are built non-preprocessed and is bound into the global proof's Fiat-Shamir -/// statement (like the monolithic path), so any wrong value diverges the verifier's -/// challenges and is rejected; it is also bound-checked up front. +/// NO cell values are carried. The raw private input is not bundled (mirrors +/// `VmProof.num_private_input_pages`), and — since the per-epoch `CellBoundary` list +/// (whose `init.value` is a private-input byte for private reads) is NOT serialized — +/// touched-cell values never leave the prover either. The verifier only ever needed the +/// epoch count and the touched page-base set from those boundaries; both are preserved +/// (`epochs.len()` and `touched_page_bases`) at page granularity, value-free. Private-input +/// genesis lives in committed, bus-enforced GLOBAL_MEMORY columns the verifier never +/// recomputes. Both public values (`num_private_input_pages`, `touched_page_bases`) are +/// bound into the global Fiat-Shamir statement and pinned by the GlobalMemory bus / +/// AIR-count checks, so a wrong value is rejected; the count is also bound-checked up front. /// /// `verify_continuation` checks this using only the bundle and the ELF. It derives /// serde, so it round-trips through `bincode` exactly like a monolithic `VmProof`. @@ -363,6 +391,12 @@ pub struct ContinuationProof { epochs: Vec, global: MultiProof, num_private_input_pages: usize, + /// Sorted, deduped page bases the run touched — the verifier's minimal input for + /// rebuilding the GLOBAL_MEMORY AIR set. Carries page bases ONLY (no cell values), so + /// private-input bytes never appear in the bundle. Prover- supplied but bus-enforced: + /// a wrong set imbalances the GlobalMemory bus / mismatches the AIR count, and it is + /// bound into the global Fiat-Shamir statement (canonicalized on ingest). + touched_page_bases: Vec, } impl ContinuationProof { @@ -498,7 +532,6 @@ fn prove_epoch( runtime_page_ranges, reg_fini, l2g_root, - boundary: boundary.to_vec(), }) } @@ -603,6 +636,7 @@ fn prove_global( boundaries: &[Vec], elf_bytes: &[u8], init_page_data: &HashMap>, + page_bases: &[u64], num_private_input_pages: usize, opts: &ProofOptions, ) -> Result, Error> { @@ -621,7 +655,7 @@ fn prove_global( } let gm_configs = global_memory_configs_from_init_page_data( - boundaries, + page_bases, init_page_data, num_private_input_pages, ); @@ -655,7 +689,12 @@ fn prove_global( Prover::multi_prove( pairs, - &mut global_transcript(elf_bytes, boundaries.len(), num_private_input_pages), + &mut global_transcript( + elf_bytes, + boundaries.len(), + num_private_input_pages, + page_bases, + ), #[cfg(feature = "disk-spill")] stark::storage_mode::StorageMode::Ram, ) @@ -663,7 +702,8 @@ fn prove_global( } fn verify_global( - boundaries: &[Vec], + num_epochs: usize, + page_bases: &[u64], proof: &MultiProof, elf: &Elf, elf_bytes: &[u8], @@ -672,7 +712,7 @@ fn verify_global( ) -> bool { // One L2G air per epoch, each with its own 1-based `fini_epoch` constant — // must match the order/labels the global proof committed in `prove_global`. - let l2g_airs: Vec<_> = (0..boundaries.len()) + let l2g_airs: Vec<_> = (0..num_epochs) .map(|i| l2g_global_air(opts, local_to_global::epoch_label(i as u64))) .collect(); // Rebuild the genesis configs FROM THE ELF (no private bytes) and recompute their @@ -683,7 +723,7 @@ fn verify_global( // recomputes (or sees) their genesis bytes; the GlobalMemory bus enforces them. A // wrong `num_private_input_pages` flips a touched page's preprocessed mode, so the // rebuilt AIR no longer matches the committed trace and `multi_verify` rejects. - let gm_configs = global_memory_configs(boundaries, elf, num_private_input_pages); + let gm_configs = global_memory_configs(page_bases, elf, num_private_input_pages); let gm_airs: Vec<_> = gm_configs .iter() .map(|config| global_memory_air(opts, config)) @@ -697,7 +737,7 @@ fn verify_global( Verifier::multi_verify( &refs, proof, - &mut global_transcript(elf_bytes, boundaries.len(), num_private_input_pages), + &mut global_transcript(elf_bytes, num_epochs, num_private_input_pages, page_bases), &FieldElement::zero(), ) } @@ -744,6 +784,11 @@ pub fn prove_continuation( local_to_global::genesis_provenance(image.iter().map(|(a, v)| (a, v as u64))); let mut epochs: Vec = Vec::new(); + // Full per-epoch boundaries, kept prover-local for `prove_global` (L2G traces + + // final-state). Deliberately NOT stored in `EpochProof`/the bundle — `CellBoundary` + // holds cell values (private-input bytes for private reads); only the value-free + // page-base set is shipped (see `touched_page_bases`). + let mut all_boundaries: 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; @@ -824,6 +869,7 @@ pub fn prove_continuation( image.set(cell.address, (cell.fini.value & 0xFF) as u8); } epochs.push(epoch); + all_boundaries.push(boundary); if is_final { break; @@ -831,14 +877,17 @@ pub fn prove_continuation( index += 1; } - // One global LogUp over all the (kept) local-to-global tables. - let all_boundaries: Vec> = - epochs.iter().map(|e| e.boundary.clone()).collect(); + // One global LogUp over all the (kept) local-to-global tables. `all_boundaries` was + // accumulated locally in the loop (never round-tripped through the bundle). let num_private_input_pages = private_input_page_count(private_inputs); + // SINGLE source of truth: the same page-base list drives the committed GLOBAL_MEMORY + // tables and is shipped in the bundle, so the two can never diverge in set or order. + let touched_page_bases = touched_page_bases(&all_boundaries); let global = prove_global( &all_boundaries, elf_bytes, &init_page_data, + &touched_page_bases, num_private_input_pages, opts, )?; @@ -847,6 +896,7 @@ pub fn prove_continuation( epochs, global, num_private_input_pages, + touched_page_bases, }) } @@ -936,11 +986,14 @@ pub fn verify_continuation( // Cross-epoch global memory: genesis for ELF/runtime pages is rebuilt FROM THE ELF // (no private bytes), so the starting memory cannot be prover-chosen; the bus // telescopes fini→init. Private-input pages are committed, non-preprocessed (genesis - // stays private), bus-enforced. - let all_boundaries: Vec> = - bundle.epochs.iter().map(|e| e.boundary.clone()).collect(); + // stays private), bus-enforced. The verifier needs only the epoch count and the + // touched page-base set (never cell values); the bundle carries the latter directly. + // Canonicalize the (untrusted) list so a shuffled-but-same-set list still verifies, + // while a different set fails via GlobalMemory-bus imbalance / AIR-count mismatch. + let page_bases = canonical_page_bases(&bundle.touched_page_bases); if !verify_global( - &all_boundaries, + n, + &page_bases, &bundle.global, &elf, elf_bytes, @@ -1408,13 +1461,104 @@ mod tests { )); } - // The bundle's `boundary` field is used only to rebuild the global AIRs' touched- - // PAGE set (genesis is recomputed from the ELF). The cross-epoch memory values - // live in the committed L2G traces, tied to the epoch proofs by - // `verify_l2g_commitment_binding` (exercised by test_split_verify_rejects_tampered_l2g_root - // below). Tampering a boundary value is therefore inconsequential; omitting/adding - // a touched page is caught by the GlobalMemory bus (unmatched fini / air count - // mismatch). So there is no meaningful "tamper a boundary value" negative test. + // Privacy regression for the touched-cell value leak. Pre-fix, `EpochProof.boundary` + // serialized each touched cell's `init.value`/`fini.value` as a u64, so a private + // byte `b` appeared in the bundle as the 8-byte window `[b,0,0,0,0,0,0,0]`. The fix + // drops `boundary` from the bundle entirely (only the value-free `touched_page_bases` + // ships), so those windows must be gone. We mark distinctive TOUCHED byte values + // (0xC7..) — their u64-LE encodings are astronomically unlikely to occur as any honest + // field/count/root byte-run — and assert none appear in the serialized bundle. (The + // committed `public_output` serializes bytes RAW, not as u64s, so it cannot produce + // these windows even for the committed markers.) + #[test] + fn test_bundle_carries_no_touched_cell_values() { + let _ = env_logger::builder().is_test(true).try_init(); + let elf_bytes = asm_elf_bytes("test_private_input_xpage"); + let mut input: Vec = (0u8..16).collect(); + let markers = [0xC7u8, 0xC8, 0xC9]; + input[4] = markers[0]; + input[5] = markers[1]; + input[6] = markers[2]; + + let bundle = + prove_continuation(&elf_bytes, &input, 2, &ProofOptions::default_test_options()) + .unwrap(); + let bytes = bincode::serialize(&bundle).unwrap(); + for m in markers { + let needle = (m as u64).to_le_bytes(); // [m,0,0,0,0,0,0,0] + assert!( + !bytes.windows(8).any(|w| w == needle), + "byte 0x{m:02X} appears as a u64 in the bundle — a touched-cell value leaked" + ); + } + // Sanity: still verifies from bundle + ELF alone. + assert!( + verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()) + .unwrap() + .is_some() + ); + } + + // The verifier canonicalizes (sorts/dedups) the shipped `touched_page_bases`, so a + // list that is reordered AND has duplicates — but describes the same set — still + // verifies. (Page-count-independent: duplicating then reversing exercises both dedup + // and reordering even when the program touches a single page.) + #[test] + fn test_split_verify_tolerates_reordered_touched_page_bases() { + let _ = env_logger::builder().is_test(true).try_init(); + let elf_bytes = asm_elf_bytes("all_loadstore_32"); + let mut bundle = + prove_continuation(&elf_bytes, &[], 3, &ProofOptions::default_test_options()).unwrap(); + assert!( + !bundle.touched_page_bases.is_empty(), + "baseline must have touched pages" + ); + assert!( + verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()) + .unwrap() + .is_some(), + "baseline must verify" + ); + // Same set, but duplicated and reversed → canonicalization must recover it. + let mut scrambled = bundle.touched_page_bases.clone(); + scrambled.extend(bundle.touched_page_bases.clone()); + scrambled.reverse(); + bundle.touched_page_bases = scrambled; + assert!( + verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()) + .unwrap() + .is_some(), + "a reordered/duplicated same-set page-base list must still verify (canonicalized)" + ); + } + + // Negative: dropping a genuinely-touched page base removes its GLOBAL_MEMORY table on + // the verify side, so that page's L2G fini token has no receiver → GlobalMemory bus + // imbalance (and the global Fiat-Shamir statement diverges) → reject. + #[test] + fn test_split_verify_rejects_dropped_touched_page_base() { + let _ = env_logger::builder().is_test(true).try_init(); + let elf_bytes = asm_elf_bytes("all_loadstore_32"); + let mut bundle = + prove_continuation(&elf_bytes, &[], 3, &ProofOptions::default_test_options()).unwrap(); + assert!( + !bundle.touched_page_bases.is_empty(), + "baseline must have touched pages" + ); + assert!( + verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()) + .unwrap() + .is_some(), + "baseline must verify before tampering" + ); + bundle.touched_page_bases.pop(); + assert!( + verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()) + .unwrap() + .is_none(), + "a missing touched page base must be rejected" + ); + } // Negative: corrupting an epoch's claimed L2G table root must be rejected — // `verify_l2g_commitment_binding` compares each epoch's `l2g_root` against the diff --git a/prover/src/statement.rs b/prover/src/statement.rs index f4a27ff62..3eae6b609 100644 --- a/prover/src/statement.rs +++ b/prover/src/statement.rs @@ -125,17 +125,28 @@ 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), the epoch count (so a /// global proof from a run with a different number of epochs cannot be spliced in), -/// and the private-input page count (so the global proof's AIR layout — which touched -/// pages are built non-preprocessed — is canonically pinned, like the monolithic -/// path's `absorb_statement`). Prove and verify must call this with identical arguments. +/// the private-input page count (so the global proof's AIR layout — which touched pages +/// are built non-preprocessed — is canonically pinned, like the monolithic path's +/// `absorb_statement`), and the touched page-base set (which GLOBAL_MEMORY tables exist). +/// 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, num_private_input_pages: usize, + touched_page_bases: &[u64], ) { 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(&(num_private_input_pages as u64).to_le_bytes()); + + // Touched page-base set: count-prefixed, each fixed-width u64. Binds the exact set + // (and order) of GLOBAL_MEMORY tables the verifier rebuilds, so a tampered list + // diverges the challenges. Prover and verifier pass the identical canonical + // (ascending, deduped) list. + t.append_bytes(&(touched_page_bases.len() as u64).to_le_bytes()); + for base in touched_page_bases { + t.append_bytes(&base.to_le_bytes()); + } } diff --git a/prover/src/tests/statement_tests.rs b/prover/src/tests/statement_tests.rs index f8759f529..679c9d369 100644 --- a/prover/src/tests/statement_tests.rs +++ b/prover/src/tests/statement_tests.rs @@ -163,29 +163,50 @@ fn continuation_epoch_differs_from_monolithic_statement() { assert_ne!(monolithic, epoch_state(b"elf", 1)); } -fn global_state(elf: &[u8], num_epochs: usize, num_private_input_pages: usize) -> [u8; 32] { +fn global_state( + elf: &[u8], + num_epochs: usize, + num_private_input_pages: usize, + touched_page_bases: &[u64], +) -> [u8; 32] { let mut t = DefaultTranscript::::new(&[]); - absorb_continuation_global_statement(&mut t, elf, num_epochs, num_private_input_pages); + absorb_continuation_global_statement( + &mut t, + elf, + num_epochs, + num_private_input_pages, + touched_page_bases, + ); t.state() } #[test] -fn continuation_global_state_binds_program_epoch_count_and_private_pages() { - let baseline = global_state(b"elf", 3, 1); - assert_eq!(baseline, global_state(b"elf", 3, 1)); // deterministic +fn continuation_global_state_binds_program_epoch_count_pages_and_touched_set() { + let baseline = global_state(b"elf", 3, 1, &[0x1000, 0x2000]); + assert_eq!(baseline, global_state(b"elf", 3, 1, &[0x1000, 0x2000])); // deterministic assert_ne!( baseline, - global_state(b"elf", 4, 1), + global_state(b"elf", 4, 1, &[0x1000, 0x2000]), "must bind epoch count" ); assert_ne!( baseline, - global_state(b"other-elf", 3, 1), + global_state(b"other-elf", 3, 1, &[0x1000, 0x2000]), "must bind the ELF" ); assert_ne!( baseline, - global_state(b"elf", 3, 2), + global_state(b"elf", 3, 2, &[0x1000, 0x2000]), "must bind the private-input page count" ); + assert_ne!( + baseline, + global_state(b"elf", 3, 1, &[0x1000, 0x3000]), + "must bind the touched page-base set" + ); + assert_ne!( + baseline, + global_state(b"elf", 3, 1, &[0x1000]), + "must bind the touched page-base count" + ); } From 7f108b30d3f39c2cc461cfc7a6106cfd30a4dfae Mon Sep 17 00:00:00 2001 From: Nicole Date: Wed, 1 Jul 2026 17:28:19 -0300 Subject: [PATCH 06/14] update doc --- docs/continuations_design.md | 32 +++++++++++++++++++++----------- 1 file changed, 21 insertions(+), 11 deletions(-) diff --git a/docs/continuations_design.md b/docs/continuations_design.md index 3289a69fc..011dbdc73 100644 --- a/docs/continuations_design.md +++ b/docs/continuations_design.md @@ -493,9 +493,10 @@ 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). - The **global** proof absorbs: a (distinct) domain tag, the ELF digest, the - **epoch count**, and the **private-input page count** (§3.6) — so the genesis AIR - layout (which pages are non-preprocessed) is pinned in the statement, matching the - monolithic path's `absorb_statement`. + **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 + non-preprocessed) is pinned in the statement, matching the monolithic path's + `absorb_statement`. The monolithic encoding is unchanged (same function, monolithic tag, no label). The genesis / register / memory anchor values are *additionally* bound via the @@ -517,12 +518,18 @@ The integrated `prove_and_verify_continuation` is now a thin wrapper likewise split into `prove_epoch` + `verify_epoch`. The bundle is prover-supplied and therefore **untrusted**. Per epoch it carries the -`MultiProof`, the `public_output` slice, `table_counts`, -`num_private_input_pages`, `runtime_page_ranges`, the bound `reg_fini` (`R_{i+1}`), -the epoch `l2g_root`, and the touched-cell `boundary`; plus the global `MultiProof` -and a top-level `num_private_input_pages` **count** (§3.6). It does **not** carry the -raw private input — the verifier never sees it. Everything the integrated path reused -from prover memory becomes an **explicit verifier action**: +`MultiProof`, the `public_output` slice, `table_counts`, `runtime_page_ranges`, the bound +`reg_fini` (`R_{i+1}`), and the epoch `l2g_root`; plus the global `MultiProof`, a top-level +`num_private_input_pages` **count** (§3.6), and the top-level **`touched_page_bases`** — the +sorted, deduped set of page bases the run touched. It carries **no cell values**: not the +raw private input, and — since the per-epoch `CellBoundary` list is *not* serialized — not +the touched-cell values either (a `CellBoundary.init.value` is a private-input byte for a +private read, so shipping it would leak the input in plaintext even though the raw blob is +gone). The verifier only ever needed the epoch count and the touched page-base set from +those boundaries; `touched_page_bases` supplies exactly that, value-free and at page +granularity. The full boundaries stay prover-local (they build the L2G traces and +final-state inside `prove_global`). Everything the integrated path reused from prover memory +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 @@ -540,8 +547,11 @@ from prover memory becomes an **explicit verifier action**: bus; private-input pages are built non-preprocessed (§3.6), so their genesis is a committed, bus-pinned column the verifier neither recomputes nor sees. `verify_l2g_commitment_binding` ties each epoch's `l2g_root` to the corresponding - global-proof sub-table root — which is what makes the prover-supplied `boundary` - trustworthy. + global-proof sub-table root. The prover-supplied `touched_page_bases` is canonicalized + (sorted/deduped) on ingest and pinned the same way the old `boundary` addresses were: a + wrong set imbalances the GlobalMemory bus / mismatches the AIR count, and it is bound + into the global Fiat-Shamir statement — so a reordered-but-same-set list still verifies + while any different set is rejected. - **Reconstruct the output** by concatenating the per-epoch commit slices (each commit-bus-bound, contiguous via the x254 chain). - The verifier also `validate()`s `table_counts` and never trusts a prover-supplied From c10ba950d99692fc59f1bb247cbf973cb9f76039 Mon Sep 17 00:00:00 2001 From: Nicole Date: Thu, 2 Jul 2026 12:34:00 -0300 Subject: [PATCH 07/14] Remove the extra +1 slack page --- prover/src/continuation.rs | 6 ++++-- prover/src/lib.rs | 7 ++++--- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index 290f12559..349476f68 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -927,8 +927,10 @@ pub fn verify_continuation( // Fiat-Shamir statement (`absorb_continuation_global_statement`), so any wrong value // diverges the verifier's challenges and `verify_global`'s `multi_verify` rejects — // on top of the committed-AIR-shape mismatch a wrong count causes on a touched page. + // The tight max is the honest span of a MAX-size input including its 4-byte length + // prefix: `ceil((MAX_PRIVATE_INPUT_SIZE + 4) / page_size)` pages (no slack). let max_private_input_pages = - (MAX_PRIVATE_INPUT_SIZE as usize + 4).div_ceil(page::DEFAULT_PAGE_SIZE) + 1; + (MAX_PRIVATE_INPUT_SIZE as usize + 4).div_ceil(page::DEFAULT_PAGE_SIZE); if bundle.num_private_input_pages > max_private_input_pages { return Err(Error::InvalidTableCounts(format!( "num_private_input_pages ({}) exceeds max ({max_private_input_pages})", @@ -1453,7 +1455,7 @@ mod tests { let elf_bytes = asm_elf_bytes("all_loadstore_32"); let mut bundle = prove_continuation(&elf_bytes, &[], 3, &ProofOptions::default_test_options()).unwrap(); - let max_pages = (MAX_PRIVATE_INPUT_SIZE as usize + 4).div_ceil(page::DEFAULT_PAGE_SIZE) + 1; + let max_pages = (MAX_PRIVATE_INPUT_SIZE as usize + 4).div_ceil(page::DEFAULT_PAGE_SIZE); bundle.num_private_input_pages = max_pages + 1; assert!(matches!( verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()), diff --git a/prover/src/lib.rs b/prover/src/lib.rs index 760383003..4ff59d339 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -960,12 +960,13 @@ pub fn verify_with_options( // A malicious prover could set counts to 0, removing entire constraint sets. vm_proof.table_counts.validate()?; - // Bound num_private_input_pages before allocating PageConfigs. - // MAX_PRIVATE_INPUT_SIZE fits in ~257 pages of DEFAULT_PAGE_SIZE. + // Bound num_private_input_pages before allocating PageConfigs. The tight max is the + // honest span of a MAX-size input plus its 4-byte length prefix: + // ceil((MAX_PRIVATE_INPUT_SIZE + 4) / DEFAULT_PAGE_SIZE) pages (no slack). { use crate::tables::page::DEFAULT_PAGE_SIZE; use executor::vm::memory::MAX_PRIVATE_INPUT_SIZE; - let max_pages = (MAX_PRIVATE_INPUT_SIZE as usize + 4).div_ceil(DEFAULT_PAGE_SIZE) + 1; + let max_pages = (MAX_PRIVATE_INPUT_SIZE as usize + 4).div_ceil(DEFAULT_PAGE_SIZE); if vm_proof.num_private_input_pages > max_pages { return Err(Error::InvalidTableCounts(format!( "num_private_input_pages ({}) exceeds max ({max_pages})", From 852dd0f1a6ba970813bf4dd2dfc95b2921a5cc31 Mon Sep 17 00:00:00 2001 From: Nicole Date: Thu, 2 Jul 2026 12:50:07 -0300 Subject: [PATCH 08/14] Use checked_add in Elf::load --- executor/src/elf.rs | 26 ++++++++++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) diff --git a/executor/src/elf.rs b/executor/src/elf.rs index e019d54a1..1d00eff4e 100644 --- a/executor/src/elf.rs +++ b/executor/src/elf.rs @@ -307,9 +307,13 @@ impl Elf { // convention into an enforced invariant. if program_header.p_memsz > 0 { use crate::vm::memory::PRIVATE_INPUT_START_INDEX; + // `checked_add` (not saturating): an overflowing `p_vaddr + p_memsz` is a + // malformed segment and is rejected explicitly as `AddrTooLarge`, rather than + // saturating to `u64::MAX` and being reported under the wrong error. let seg_end = program_header .p_vaddr - .saturating_add(program_header.p_memsz); + .checked_add(program_header.p_memsz) + .ok_or(ElfError::AddrTooLarge)?; if seg_end > PRIVATE_INPUT_START_INDEX { return Err(ElfError::SegmentInPrivateInputRegion); } @@ -322,7 +326,17 @@ impl Elf { let len = remaining.min(WORD_SIZE); let mut word = 0u32; for j in 0..len { - let offset = (program_header.p_offset + i + j) as usize; + // `checked_add` (not plain `+`): `p_offset` is an unbounded file + // offset, so `p_offset + i + j` could overflow — which would panic in + // debug and silently wrap in release. In practice the monotonic + // bounds check (`input.get` below) fires first, but don't rely on + // evaluation order: reject an overflow explicitly. + let offset = program_header + .p_offset + .checked_add(i) + .and_then(|o| o.checked_add(j)) + .ok_or(ElfError::InvalidOffset)? + as usize; let byte = input.get(offset).ok_or(ElfError::InvalidOffset)?; word |= (*byte as u32) .checked_shl((j as u32).checked_mul(8).ok_or(ElfError::InvalidProgram)?) @@ -626,6 +640,14 @@ mod tests { )); } + #[test] + fn rejects_segment_with_overflowing_vaddr_span() { + // p_vaddr + p_memsz overflows u64 → rejected explicitly as AddrTooLarge (not + // saturated to u64::MAX and mis-reported, and no panic/wrap). + let elf = minimal_elf_with_segment(0xFFFF_FFFF_FFFF_F000, 0x2000); + assert!(matches!(Elf::load(&elf), Err(ElfError::AddrTooLarge))); + } + #[test] fn rejects_segment_straddling_region_start() { // Ends 4 bytes into the region → overlaps → rejected. From bab015ba90dbab6de1140ff228c205b97a7496f5 Mon Sep 17 00:00:00 2001 From: Nicole Date: Thu, 2 Jul 2026 13:02:44 -0300 Subject: [PATCH 09/14] Add a multi-page private-input continuation regression test --- .../asm/test_private_input_multipage.s | 28 ++++++++++++ prover/src/continuation.rs | 45 +++++++++++++++++++ 2 files changed, 73 insertions(+) create mode 100644 executor/programs/asm/test_private_input_multipage.s diff --git a/executor/programs/asm/test_private_input_multipage.s b/executor/programs/asm/test_private_input_multipage.s new file mode 100644 index 000000000..bba65dff0 --- /dev/null +++ b/executor/programs/asm/test_private_input_multipage.s @@ -0,0 +1,28 @@ + .attribute 5, "rv64i2p1" + .globl main +main: + # Reads private input across TWO pages of the memory-mapped private-input + # region and commits 8 bytes from the second page. Exercises multi-page + # private input: two touched private pages => two non-preprocessed + # GLOBAL_MEMORY tables in the continuation global proof. + # + # Layout: [len:u32 LE] at 0xFF000000, data follows. Page size = 1<<18 = 0x40000. + # Page 0 = [0xFF000000, 0xFF040000); page 1 = [0xFF040000, 0xFF080000). + + li t0, 0xFF000000 # page 0 base + lw t3, 0(t0) # touch page 0 (read length) + + li t2, 0xFF040000 # page 1 base (0xFF000000 + 0x40000) + ld t4, 0(t2) # touch page 1 (read 8 bytes) + + # Commit 8 bytes from page 1 (0xFF040000), so the output depends on page 1. + mv a1, t2 # buf_addr = 0xFF040000 + li a0, 1 # fd = 1 + li a2, 8 # count = 8 + li a7, 64 # syscall = Commit + ecall + + # Halt + li a0, 0 # exit_code = 0 + li a7, 93 # syscall = Halt + ecall diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index 349476f68..8ee2de914 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -1501,6 +1501,51 @@ mod tests { ); } + // Multi-page private input: the program reads private input across TWO pages + // (page 0 for the length, page 1 for the committed bytes), so the run touches two + // private pages → `num_private_input_pages >= 2` and two NON-preprocessed + // GLOBAL_MEMORY tables in the global proof. Verifies from bundle + ELF alone and the + // output equals the page-1 bytes. Exercises the count-based classification and the + // committed private genesis across more than one page. + #[test] + fn test_continuation_multipage_private_input() { + use executor::vm::memory::PRIVATE_INPUT_START_INDEX; + let _ = env_logger::builder().is_test(true).try_init(); + let elf_bytes = asm_elf_bytes("test_private_input_multipage"); + + // Page 1 starts at memory address START + page_size = 0xFF040000, which is data + // index `page_size - 4` (the 4-byte length prefix sits at START). The program + // commits the 8 bytes there, so the input must extend through that. + let page_size = page::DEFAULT_PAGE_SIZE; + let commit_off = page_size - 4; + let mut input = vec![0u8; commit_off + 8]; + let expected: [u8; 8] = [0xA1, 0xB2, 0xC3, 0xD4, 0xE5, 0xF6, 0x07, 0x18]; + input[commit_off..commit_off + 8].copy_from_slice(&expected); + + let bundle = + prove_continuation(&elf_bytes, &input, 4, &ProofOptions::default_test_options()) + .unwrap(); + assert!( + bundle.num_private_input_pages >= 2, + "input spanning two pages must give >=2 private pages" + ); + let start = PRIVATE_INPUT_START_INDEX; + let ps = page_size as u64; + assert!( + bundle.touched_page_bases.contains(&start) + && bundle.touched_page_bases.contains(&(start + ps)), + "both private page 0 and page 1 must be touched (two GLOBAL_MEMORY tables)" + ); + + let out = verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()) + .unwrap(); + assert_eq!( + out.as_deref(), + Some(&expected[..]), + "committed output must be the 8 bytes read from private page 1" + ); + } + // The verifier canonicalizes (sorts/dedups) the shipped `touched_page_bases`, so a // list that is reordered AND has duplicates — but describes the same set — still // verifies. (Page-count-independent: duplicating then reversing exercises both dedup From dbac7707132d21e693f3667b1fd58f8144aabff4 Mon Sep 17 00:00:00 2001 From: Nicole Date: Thu, 2 Jul 2026 13:13:50 -0300 Subject: [PATCH 10/14] add an explicit non-ZK caveat --- docs/continuations_design.md | 36 +++++++++++++++++++++--------- prover/src/continuation.rs | 31 +++++++++++++++---------- prover/src/tables/global_memory.rs | 6 +++-- 3 files changed, 48 insertions(+), 25 deletions(-) diff --git a/docs/continuations_design.md b/docs/continuations_design.md index 011dbdc73..f5c64849d 100644 --- a/docs/continuations_design.md +++ b/docs/continuations_design.md @@ -64,8 +64,9 @@ makes the proof fail. - **genesis**: a cell's starting value. For ELF/runtime pages it is **preprocessed** (read from the ELF, so the verifier recomputes it — the prover cannot choose initial memory). For **private-input pages** it is a **committed** (non-preprocessed) column - the verifier never recomputes — the private bytes stay private and are pinned by the - bus instead (see §3.6); this mirrors the monolithic PAGE table. + the verifier never recomputes from the ELF — the raw private input is neither bundled + nor reconstructed by the verifier, and the value is pinned by the bus instead (see + §3.6); this mirrors the monolithic PAGE table. (Not a ZK/hiding guarantee — see §3.6.) - **finalization**: a cell's final value after the last epoch that touched it. ### A single L2G row @@ -238,12 +239,13 @@ accepts — only how the driver slices cycles. A debug-assert enforces the Genesis for ELF/runtime pages is preprocessed, so the verifier recomputes it from the ELF — that is what stops a prover from choosing initial memory (§2). But **private -input** is, by definition, *not* in the ELF and must **stay private** from the verifier. -So a private-input page's genesis cannot be ELF-recomputed. +input** is, by definition, *not* in the ELF, so it must not be verifier-recomputed and +must not be shipped in the proof bundle. So a private-input page's genesis cannot be +ELF-recomputed. Fix (mirrors the monolithic PAGE table exactly): build the `global_memory` AIR for a private-input page **non-preprocessed**, so its `INIT` (genesis) is a **committed -main-trace column** the verifier never recomputes or sees. Correctness is enforced by +main-trace column** the verifier never recomputes from the ELF. Correctness is enforced by the same bus chain as everything else: the genesis token telescopes into the first touching epoch's L2G `init`, which is pinned on the epoch-local Memory bus to MEMW's true first-read value. A forged genesis would leave an unmatched Memory-bus term. This @@ -252,6 +254,15 @@ private genesis is prover-supplied *by design* (it is the private input), so the attests "**there exists** a private input producing this output" — the intended semantics, identical to the monolithic prover. +**Scope of the guarantee (not zero-knowledge).** What this buys is that the raw private +input is **neither bundled in the proof nor recomputed by the verifier** — not that it is +cryptographically hidden. This proving stack is a non-ZK STARK: the committed private +`INIT` column, like every committed column, is opened at FRI query positions, so a +verifier does learn some trace evaluations. Cryptographic hiding of the private input +would require a ZK/blinded proof system (a separate, larger change). Phrase any external +claim as "raw private input is not bundled or recomputed by the verifier," not "the +verifier never sees it." + **One prerequisite — the region must hold only private input.** Skipping the ELF recomputation is safe *only* if no ELF-declared data lives in the private-input region; otherwise a prover could classify that page private and forge the ELF byte's genesis @@ -586,7 +597,7 @@ recursion/aggregation layer (deferred). - Implemented and tested: range checks (§3.1), `fini_epoch` constant (§3.2), ordering check (§3.3), the `MU` selector (§3.4), the **power-of-two epoch size** - (§3.5), **private-input genesis kept private** (§3.6), **cross-epoch registers** + (§3.5), **private-input genesis not bundled/recomputed** (§3.6), **cross-epoch registers** (§6), the **commit index x254** across epochs (§6), the **Fiat-Shamir statement binding** (§7), and the **standalone split prover/verifier** (§8) — bundle serialized with `bincode` and driven from the CLI (`prove`/`verify --continuations`). @@ -598,11 +609,14 @@ recursion/aggregation layer (deferred). - **Succinctness.** The split verifier is non-succinct (N+1 proofs, §8). A single small proof needs a recursion/aggregation layer — a separate, larger effort. - **Private-input *content* binding.** The bundle no longer carries the private input - in the clear (§3.6 — it carries only the page count, and the verifier never sees the - bytes). What remains deferred is pinning *which specific input* produced the output: - the proof attests only that *some* private input does. A guest that needs "this exact - input" must commit a hash of it to the public output — the framework provides no such - binding on either the continuation or monolithic path. + in the clear (§3.6 — it carries only the page count; the raw input is neither bundled + nor recomputed by the verifier). What remains deferred is pinning *which specific input* + produced the output: the proof attests only that *some* private input does. A guest that + needs "this exact input" must commit a hash of it to the public output — the framework + provides no such binding on either the continuation or monolithic path. + - **Zero-knowledge / hiding.** As noted in §3.6, this is a non-ZK STARK: committed private + columns are opened at query positions, so the private input is not cryptographically + hidden. Cryptographic hiding would need a ZK/blinded proof system. --- diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index 8ee2de914..73898d669 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -8,10 +8,16 @@ //! The global proof's genesis anchor is bound to the ELF: for ELF/runtime pages the //! verifier recomputes the per-page preprocessed init commitment from the ELF in //! `verify_global`, so the starting memory cannot be prover-supplied. Private-input -//! pages are the one exception — their genesis is committed (non-preprocessed) and -//! kept private, exactly as the monolithic prover does, with correctness enforced by -//! the GlobalMemory bus rather than ELF recomputation (so the verifier never sees the -//! raw private input). +//! pages are the one exception — their genesis is committed (non-preprocessed), exactly +//! as the monolithic prover does, with correctness enforced by the GlobalMemory bus +//! rather than ELF recomputation, so the raw private input is neither carried in the +//! proof bundle nor reconstructed by the verifier. +//! +//! Scope of the privacy guarantee: this is NOT zero-knowledge. Like every non-ZK STARK +//! column, the committed private genesis is opened at FRI query positions, so this does +//! not cryptographically hide the private input — it only guarantees the raw input is +//! not bundled and not recomputed by the verifier. Cryptographic hiding would require a +//! ZK/blinded proof system. //! //! The local-to-global columns are range-checked in the epoch proof (which //! carries the BITWISE provider): values are bytes, and the cross-epoch-only @@ -196,10 +202,11 @@ fn l2g_memory_air( /// cannot choose those genesis values. /// /// Private-input pages are built NON-preprocessed (mirrors the monolithic PAGE in -/// `VmAirs::new`): INIT is a committed main-trace column the verifier never recomputes, -/// so the verifier never sees the private genesis bytes. Correctness is enforced by -/// the GlobalMemory bus (the genesis token must telescope into the epochs' reads), not -/// by recomputation from the ELF. +/// `VmAirs::new`): INIT is a committed main-trace column the verifier never recomputes +/// from the ELF, so the raw private input is neither bundled nor reconstructed by the +/// verifier. Correctness is enforced by the GlobalMemory bus (the genesis token must +/// telescope into the epochs' reads), not by ELF recomputation. (Not a ZK/hiding claim — +/// the committed column is still opened at STARK query positions.) fn global_memory_air( opts: &ProofOptions, config: &PageConfig, @@ -720,7 +727,7 @@ fn verify_global( // different genesis values would commit a different root and fail to verify. // Private-input pages (the first `num_private_input_pages` from // PRIVATE_INPUT_START_INDEX) are built non-preprocessed, so the verifier never - // recomputes (or sees) their genesis bytes; the GlobalMemory bus enforces them. A + // recomputes their genesis from the ELF; the GlobalMemory bus enforces them. A // wrong `num_private_input_pages` flips a touched page's preprocessed mode, so the // rebuilt AIR no longer matches the committed trace and `multi_verify` rejects. let gm_configs = global_memory_configs(page_bases, elf, num_private_input_pages); @@ -988,7 +995,7 @@ pub fn verify_continuation( // Cross-epoch global memory: genesis for ELF/runtime pages is rebuilt FROM THE ELF // (no private bytes), so the starting memory cannot be prover-chosen; the bus // telescopes fini→init. Private-input pages are committed, non-preprocessed (genesis - // stays private), bus-enforced. The verifier needs only the epoch count and the + // not bundled/ELF-recomputed), bus-enforced. The verifier needs only the epoch count and the // touched page-base set (never cell values); the bundle carries the latter directly. // Canonicalize the (untrusted) list so a shuffled-but-same-set list still verifies, // while a different set fails via GlobalMemory-bus imbalance / AIR-count mismatch. @@ -1295,8 +1302,8 @@ mod tests { ); } - // Private input must stay private under continuations. The bundle carries no raw - // private bytes (only `num_private_input_pages`), yet a multi-epoch continuation of + // The raw private input must not be bundled under continuations. The bundle carries no + // raw private bytes (only `num_private_input_pages`), yet a multi-epoch continuation of // a program that reads private input verifies from the bundle + ELF ALONE and // reconstructs the committed output. Regression for the genesis leak: the global // proof's private-input genesis is a committed, bus-enforced column, not a diff --git a/prover/src/tables/global_memory.rs b/prover/src/tables/global_memory.rs index ce343df5e..de6d95d7d 100644 --- a/prover/src/tables/global_memory.rs +++ b/prover/src/tables/global_memory.rs @@ -15,8 +15,10 @@ //! //! Private-input pages are the exception: the AIR is built NON-preprocessed (see //! `continuation::global_memory_air`), so INIT is a committed main-trace column the -//! verifier never recomputes — the private genesis bytes stay private and correctness -//! is enforced by the GlobalMemory bus, exactly as the monolithic PAGE does. +//! verifier never recomputes from the ELF — the raw private input is neither bundled nor +//! reconstructed by the verifier, and correctness is enforced by the GlobalMemory bus, +//! exactly as the monolithic PAGE does. (This is not zero-knowledge: the committed column +//! is still opened at STARK query positions; it is not a cryptographic hiding guarantee.) //! //! ## Columns //! From 529756db5605fb5c0a5231b538c49841aa48ad82 Mon Sep 17 00:00:00 2001 From: Nicole Date: Fri, 3 Jul 2026 11:50:30 -0300 Subject: [PATCH 11/14] Reject non-page-aligned touched_page_bases entries and fix doc --- prover/src/continuation.rs | 44 ++++++++++++++++++++++++++++ prover/src/tables/local_to_global.rs | 5 +++- prover/src/tables/page.rs | 8 ++++- 3 files changed, 55 insertions(+), 2 deletions(-) diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index 73898d669..319b6ac03 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -1000,6 +1000,20 @@ pub fn verify_continuation( // Canonicalize the (untrusted) list so a shuffled-but-same-set list still verifies, // while a different set fails via GlobalMemory-bus imbalance / AIR-count mismatch. let page_bases = canonical_page_bases(&bundle.touched_page_bases); + // Every honest base is produced by `page::page_base_for_address`, so it is page-aligned; a + // non-aligned base is only reachable via a hand-crafted bundle. Left unchecked, such a base + // still falls in the private-input range (`is_private_input_page`), so it would be built + // NON-preprocessed with a prover-controlled genesis. The GlobalMemory bus already prevents + // forging any real cell (no MEMW access exists at a non-aligned fake address, so no L2G row + // consumes its genesis token), but a self-cancelling junk page could otherwise ride along in + // an accepted proof. Reject here so the verifier's page set is exactly the aligned set the + // prover could honestly derive. + if page_bases + .iter() + .any(|&b| b != page::page_base_for_address(b)) + { + return Ok(None); + } if !verify_global( n, &page_bases, @@ -1614,6 +1628,36 @@ mod tests { ); } + // Negative: a non-page-aligned base is only reachable via a hand-crafted bundle (honest + // bases come from `page_base_for_address`). The verifier rejects it up front so a base in + // the private-input range can't be built NON-preprocessed with a prover-controlled genesis + // and ride along as a self-cancelling junk page. Page-count-independent: perturbing any one + // base by +1 makes it non-aligned. + #[test] + fn test_split_verify_rejects_non_page_aligned_touched_page_base() { + let _ = env_logger::builder().is_test(true).try_init(); + let elf_bytes = asm_elf_bytes("all_loadstore_32"); + let mut bundle = + prove_continuation(&elf_bytes, &[], 3, &ProofOptions::default_test_options()).unwrap(); + assert!( + !bundle.touched_page_bases.is_empty(), + "baseline must have touched pages" + ); + assert!( + verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()) + .unwrap() + .is_some(), + "baseline must verify before tampering" + ); + bundle.touched_page_bases[0] += 1; + assert!( + verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()) + .unwrap() + .is_none(), + "a non-page-aligned touched page base must be rejected" + ); + } + // Negative: corrupting an epoch's claimed L2G table root must be rejected — // `verify_l2g_commitment_binding` compares each epoch's `l2g_root` against the // corresponding sub-proof root in the global proof, so a mismatched root causes diff --git a/prover/src/tables/local_to_global.rs b/prover/src/tables/local_to_global.rs index ada19baf5..6ff1e3284 100644 --- a/prover/src/tables/local_to_global.rs +++ b/prover/src/tables/local_to_global.rs @@ -89,7 +89,10 @@ pub struct InitClaim { pub value: u64, /// Epoch that last wrote the cell (or [`GENESIS_EPOCH`]). pub originating_epoch: u64, - /// Timestamp of that originating write. + /// Timestamp of that originating write. Provenance-tracked for symmetry with + /// [`FiniClaim`] and asserted by the telescoping tests, but intentionally NOT + /// constrained: the L2G init token is pinned to `ts=0` (timestamps are epoch-local; + /// cross-epoch links are ordered by epoch label, not timestamp). pub timestamp: u64, } diff --git a/prover/src/tables/page.rs b/prover/src/tables/page.rs index 2d1059bcc..e02a46a80 100644 --- a/prover/src/tables/page.rs +++ b/prover/src/tables/page.rs @@ -138,7 +138,13 @@ impl PageConfig { } /// Create a page with initial values from private input data. - /// These pages are NOT preprocessed — the verifier never sees the init values. + /// + /// These pages are built NON-preprocessed, so INIT is a committed main-trace column + /// enforced by the GlobalMemory bus rather than recomputed from the ELF. Privacy comes + /// from that (the raw input is neither bundled nor recomputed by the verifier), NOT from + /// this constructor: the verifier rebuilds the config from the ELF alone and never consults + /// the `data` argument for a private page (it passes an empty vec). Not a ZK/hiding claim — + /// the committed column is still opened at STARK query positions. pub fn with_private_input(page_base: u64, data: Vec) -> Self { assert!(data.len() <= DEFAULT_PAGE_SIZE, "Data exceeds page size"); Self { From dd4b884a0baaab024c8f8c04f0e9720b1640c39d Mon Sep 17 00:00:00 2001 From: MauroFab Date: Fri, 3 Jul 2026 15:13:52 -0300 Subject: [PATCH 12/14] Address review findings: dedupe private-input page math, drop leaky serde derives, fix stale docs - Extract private_input_page_count / is_private_input_page / private_input_page_bases / max_private_input_pages into tables::page as the single source of truth; the monolithic trace builder, monolithic verifier bound, continuation prover, and continuation verifier all previously re-derived the same wire-format math independently and could drift. - Add PRIVATE_INPUT_LENGTH_PREFIX_BYTES to executor::vm::memory next to the wire-format writer and use it everywhere instead of a bare 4. - Remove the now-unused serde derives from InitClaim/FiniClaim/CellBoundary: nothing serializes them since the bundle dropped EpochProof.boundary, and keeping them off makes re-introducing the value leak a compile error. - Make the verifier-side private-page config explicitly data-free (include_private_genesis flag) instead of a dead init_page_data lookup. - Reject a non-page-aligned touched_page_bases entry as a malformed bundle (new Error::MalformedContinuationBundle) instead of Ok(None), matching the count bound's Err semantics for structural validation of untrusted fields. - Fix bin/cli/README.md, which still claimed the continuation bundle ships the raw private input bytes. --- bin/cli/README.md | 12 ++- executor/src/vm/memory.rs | 10 ++- prover/src/continuation.rs | 125 ++++++++++++--------------- prover/src/lib.rs | 15 ++-- prover/src/tables/local_to_global.rs | 16 +++- prover/src/tables/page.rs | 62 +++++++++++++ prover/src/tables/trace_builder.rs | 31 +++---- 7 files changed, 165 insertions(+), 106 deletions(-) diff --git a/bin/cli/README.md b/bin/cli/README.md index bc5eb9d53..267fc61b7 100644 --- a/bin/cli/README.md +++ b/bin/cli/README.md @@ -118,10 +118,14 @@ As rough ethrex 10-transfer distinct-account reference points from a local sweep about 26.8 GB. For a new workload, use the highest value the machine can run without swapping. -Continuation proof bundles are self-contained for standalone verification. When -`--private-input` is used, the serialized continuation proof includes the raw -private input bytes so the verifier can rebuild the genesis memory commitment. -Do not treat continuation proof files as confidential-input hiding artifacts. +Continuation proof bundles are self-contained for standalone verification: the +verifier needs only the proof file and the ELF. When `--private-input` is used, +the serialized proof does **not** include the raw private input bytes — it +carries only the private-input page count; the private genesis lives in +committed, bus-enforced columns the verifier never recomputes (see +`docs/continuations_design.md` §3.6). This is not a zero-knowledge guarantee, +though: committed columns are still opened at STARK query positions, so do not +treat proof files as cryptographically hiding the private input. ## Guest Program Flamegraphs diff --git a/executor/src/vm/memory.rs b/executor/src/vm/memory.rs index f349eeae6..d4f8d1cee 100644 --- a/executor/src/vm/memory.rs +++ b/executor/src/vm/memory.rs @@ -51,6 +51,11 @@ pub const MAX_PRIVATE_INPUT_SIZE: u64 = 64 * 1024 * 1024; /// Layout: 4-byte LE length prefix at `PRIVATE_INPUT_START_INDEX`, then data at +4. /// Must match `PRIVATE_INPUT_START` in `syscalls/src/syscalls.rs`. pub const PRIVATE_INPUT_START_INDEX: u64 = 0xFF000000; +/// Size in bytes of the private input's wire-format length prefix (the `u32` LE +/// written at `PRIVATE_INPUT_START_INDEX` by [`Memory::store_private_inputs`]; the +/// data follows at `+ PRIVATE_INPUT_LENGTH_PREFIX_BYTES`). Single source of truth +/// for every page-span computation over the private-input region. +pub const PRIVATE_INPUT_LENGTH_PREFIX_BYTES: usize = size_of::(); #[derive(Default, Debug, Clone)] pub struct Memory { @@ -231,7 +236,10 @@ impl Memory { let len_u32 = u32::try_from(inputs.len()).map_err(|_| MemoryError::PrivateInputSizeExceeded)?; self.store_word(PRIVATE_INPUT_START_INDEX, len_u32)?; - self.set_bytes_aligned(PRIVATE_INPUT_START_INDEX + 4, &inputs)?; + self.set_bytes_aligned( + PRIVATE_INPUT_START_INDEX + PRIVATE_INPUT_LENGTH_PREFIX_BYTES as u64, + &inputs, + )?; Ok(()) } diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index 319b6ac03..ea1e2c8a8 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -49,7 +49,6 @@ use std::collections::HashMap; use crypto::fiat_shamir::default_transcript::DefaultTranscript; use executor::elf::Elf; use executor::vm::execution::Executor; -use executor::vm::memory::MAX_PRIVATE_INPUT_SIZE; use math::field::element::FieldElement; use stark::config::Commitment; use stark::lookup::{AirWithBuses, AuxiliaryTraceBuildData, NullBoundaryConstraintBuilder}; @@ -268,7 +267,7 @@ fn canonical_page_bases(page_bases: &[u64]) -> Vec { /// Private-input pages are built NON-preprocessed, so the verifier never recomputes their /// genesis from the ELF and never needs the raw private bytes. They are identified EXACTLY /// as the monolithic verifier does — the first `num_private_input_pages` pages from -/// `PRIVATE_INPUT_START_INDEX` (see [`is_private_input_page`]). +/// `PRIVATE_INPUT_START_INDEX` (see [`page::is_private_input_page`]). fn global_memory_configs( page_bases: &[u64], elf: &Elf, @@ -278,25 +277,40 @@ fn global_memory_configs( // non-preprocessed (their INIT is never recomputed). let image = build_initial_image_paged(elf, &[]); let init_page_data = build_init_page_data(&image); - global_memory_configs_from_init_page_data(page_bases, &init_page_data, num_private_input_pages) + global_memory_configs_from_init_page_data( + page_bases, + &init_page_data, + num_private_input_pages, + false, + ) } /// Shared genesis-config builder for prover and verifier, one `PageConfig` per page base /// in `page_bases` (which must be canonical: sorted + deduped). `init_page_data` holds /// each page's genesis bytes (ELF + private input on the prover side; ELF only on the -/// verifier side). Private-input pages are built NON-preprocessed: on the prover their -/// committed INIT column carries the genesis bytes; on the verifier the AIR is -/// non-preprocessed so those bytes are irrelevant. +/// verifier side). +/// +/// `include_private_genesis` — whether a private-input page's genesis bytes are loaded +/// from `init_page_data` into its config. The PROVER passes `true`: those bytes become +/// the committed INIT column. The VERIFIER passes `false`: its AIR for a private page is +/// non-preprocessed and never consults `init_values` (and its `init_page_data` is built +/// from the ELF alone, so there is nothing to load) — the config carries an explicitly +/// empty vec so no code path can silently start depending on verifier-side private data. fn global_memory_configs_from_init_page_data( page_bases: &[u64], init_page_data: &HashMap>, num_private_input_pages: usize, + include_private_genesis: bool, ) -> Vec { page_bases .iter() .map(|&page_base| { - if is_private_input_page(page_base, num_private_input_pages) { - let data = init_page_data.get(&page_base).cloned().unwrap_or_default(); + if page::is_private_input_page(page_base, num_private_input_pages) { + let data = if include_private_genesis { + init_page_data.get(&page_base).cloned().unwrap_or_default() + } else { + Vec::new() + }; PageConfig::with_private_input(page_base, data) } else { match init_page_data.get(&page_base) { @@ -308,38 +322,6 @@ fn global_memory_configs_from_init_page_data( .collect() } -/// Whether `page_base` is one of the first `num_private_input_pages` pages starting at -/// `PRIVATE_INPUT_START_INDEX` — the page-aligned span private input actually occupies. -/// This matches the monolithic verifier's `page_configs_from_elf_and_runtime` exactly, so -/// the continuation classifies private pages identically to the monolithic path. Classifying -/// by the count (not the raw `[START, START+MAX_PRIVATE_INPUT_SIZE)` byte range) keeps prover -/// and verifier in lockstep regardless of whether the region end is page-aligned. -/// -/// NOTE (shared with the monolithic path): a page classified private is built -/// non-preprocessed, so its genesis is NOT recomputed from the ELF. This is safe because -/// the private-input area is reserved and the reservation is enforced: `Elf::load` rejects -/// any loadable segment reaching at/above `PRIVATE_INPUT_START_INDEX` -/// (`ElfError::SegmentInPrivateInputRegion`) — covering every page this function can -/// classify private — so no ELF-declared data can live there and have its genesis go unbound. -fn is_private_input_page(page_base: u64, num_private_input_pages: usize) -> bool { - use executor::vm::memory::PRIVATE_INPUT_START_INDEX; - let page_size = page::DEFAULT_PAGE_SIZE as u64; - let end = PRIVATE_INPUT_START_INDEX + num_private_input_pages as u64 * page_size; - (PRIVATE_INPUT_START_INDEX..end).contains(&page_base) -} - -/// Number of pages the private input occupies, starting at `PRIVATE_INPUT_START_INDEX`. -/// Mirrors the monolithic prover (`from_elf_and_logs`): the wire format is a 4-byte -/// length prefix plus the data, and `PRIVATE_INPUT_START_INDEX` is page-aligned, so the -/// span is `ceil((4 + len) / page_size)` consecutive pages (0 when there is no input). -fn private_input_page_count(private_inputs: &[u8]) -> usize { - if private_inputs.is_empty() { - return 0; - } - let total_bytes = 4 + private_inputs.len(); - total_bytes.div_ceil(page::DEFAULT_PAGE_SIZE) -} - /// Per-epoch register state and label. struct EpochStart<'a> { register_init: &'a [u32], @@ -665,6 +647,7 @@ fn prove_global( page_bases, init_page_data, num_private_input_pages, + true, ); let mut l2g_traces: Vec> = boundaries @@ -886,7 +869,7 @@ pub fn prove_continuation( // One global LogUp over all the (kept) local-to-global tables. `all_boundaries` was // accumulated locally in the loop (never round-tripped through the bundle). - let num_private_input_pages = private_input_page_count(private_inputs); + let num_private_input_pages = page::private_input_page_count(private_inputs); // SINGLE source of truth: the same page-base list drives the committed GLOBAL_MEMORY // tables and is shipped in the bundle, so the two can never diverge in set or order. let touched_page_bases = touched_page_bases(&all_boundaries); @@ -909,8 +892,9 @@ pub fn prove_continuation( /// Verify a [`ContinuationProof`] using ONLY the bundle and the ELF — nothing from /// the prover's memory. Returns `Ok(Some(public_output))` (the run-wide committed -/// bytes, reconstructed from the per-epoch bound slices) iff every check holds, else -/// `Ok(None)`. +/// bytes, reconstructed from the per-epoch bound slices) iff every check holds, +/// `Ok(None)` if a well-formed proof fails verification, and `Err` if the bundle is +/// structurally malformed (fails validation before any proof is checked). /// /// The verifier (1) enumerates epochs itself, assigning `epoch_label` and `is_final` /// by position (a trusted enumeration); (2) verifies each epoch, deriving its @@ -934,10 +918,7 @@ pub fn verify_continuation( // Fiat-Shamir statement (`absorb_continuation_global_statement`), so any wrong value // diverges the verifier's challenges and `verify_global`'s `multi_verify` rejects — // on top of the committed-AIR-shape mismatch a wrong count causes on a touched page. - // The tight max is the honest span of a MAX-size input including its 4-byte length - // prefix: `ceil((MAX_PRIVATE_INPUT_SIZE + 4) / page_size)` pages (no slack). - let max_private_input_pages = - (MAX_PRIVATE_INPUT_SIZE as usize + 4).div_ceil(page::DEFAULT_PAGE_SIZE); + let max_private_input_pages = page::max_private_input_pages(); if bundle.num_private_input_pages > max_private_input_pages { return Err(Error::InvalidTableCounts(format!( "num_private_input_pages ({}) exceeds max ({max_private_input_pages})", @@ -1002,17 +983,21 @@ pub fn verify_continuation( let page_bases = canonical_page_bases(&bundle.touched_page_bases); // Every honest base is produced by `page::page_base_for_address`, so it is page-aligned; a // non-aligned base is only reachable via a hand-crafted bundle. Left unchecked, such a base - // still falls in the private-input range (`is_private_input_page`), so it would be built - // NON-preprocessed with a prover-controlled genesis. The GlobalMemory bus already prevents - // forging any real cell (no MEMW access exists at a non-aligned fake address, so no L2G row - // consumes its genesis token), but a self-cancelling junk page could otherwise ride along in - // an accepted proof. Reject here so the verifier's page set is exactly the aligned set the - // prover could honestly derive. + // still falls in the private-input range (`page::is_private_input_page`), so it would be + // built NON-preprocessed with a prover-controlled genesis. The GlobalMemory bus already + // prevents forging any real cell (no MEMW access exists at a non-aligned fake address, so no + // L2G row consumes its genesis token), but a self-cancelling junk page could otherwise ride + // along in an accepted proof. Reject here so the verifier's page set is exactly the aligned + // set the prover could honestly derive. Like the count bound above, this is structural + // validation of an untrusted bundle field, so it is an `Err` (malformed bundle), not + // `Ok(None)` (well-formed proof that failed verification). if page_bases .iter() .any(|&b| b != page::page_base_for_address(b)) { - return Ok(None); + return Err(Error::MalformedContinuationBundle( + "touched_page_bases contains a non-page-aligned entry".to_string(), + )); } if !verify_global( n, @@ -1443,27 +1428,27 @@ mod tests { // first page, not the last. Classification is by count alone, not the region span. let region_pages = MAX_PRIVATE_INPUT_SIZE / page_size; let last_region_page = start + (region_pages - 1) * page_size; - assert!(!is_private_input_page(start, 0)); - assert!(!is_private_input_page(last_region_page, 0)); + assert!(!page::is_private_input_page(start, 0)); + assert!(!page::is_private_input_page(last_region_page, 0)); // Count n → exactly the first n pages from start. - assert!(is_private_input_page(start, 1)); - assert!(!is_private_input_page(start + page_size, 1)); - assert!(is_private_input_page(start + page_size, 2)); + assert!(page::is_private_input_page(start, 1)); + assert!(!page::is_private_input_page(start + page_size, 1)); + assert!(page::is_private_input_page(start + page_size, 2)); // Pages below the region are never private. - assert!(!is_private_input_page(start - page_size, 10)); + assert!(!page::is_private_input_page(start - page_size, 10)); // private_input_page_count: wire format is [len:4][data], region is page-aligned. - assert_eq!(private_input_page_count(&[]), 0); - assert_eq!(private_input_page_count(&[0u8; 16]), 1); + assert_eq!(page::private_input_page_count(&[]), 0); + assert_eq!(page::private_input_page_count(&[0u8; 16]), 1); // 4-byte prefix + (page_size - 4) data exactly fills one page. assert_eq!( - private_input_page_count(&vec![0u8; page::DEFAULT_PAGE_SIZE - 4]), + page::private_input_page_count(&vec![0u8; page::DEFAULT_PAGE_SIZE - 4]), 1 ); // One more byte spills into a second page. assert_eq!( - private_input_page_count(&vec![0u8; page::DEFAULT_PAGE_SIZE - 3]), + page::private_input_page_count(&vec![0u8; page::DEFAULT_PAGE_SIZE - 3]), 2 ); } @@ -1476,8 +1461,7 @@ mod tests { let elf_bytes = asm_elf_bytes("all_loadstore_32"); let mut bundle = prove_continuation(&elf_bytes, &[], 3, &ProofOptions::default_test_options()).unwrap(); - let max_pages = (MAX_PRIVATE_INPUT_SIZE as usize + 4).div_ceil(page::DEFAULT_PAGE_SIZE); - bundle.num_private_input_pages = max_pages + 1; + bundle.num_private_input_pages = page::max_private_input_pages() + 1; assert!(matches!( verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()), Err(Error::InvalidTableCounts(_)) @@ -1651,10 +1635,11 @@ mod tests { ); bundle.touched_page_bases[0] += 1; assert!( - verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()) - .unwrap() - .is_none(), - "a non-page-aligned touched page base must be rejected" + matches!( + verify_continuation(&elf_bytes, &bundle, &ProofOptions::default_test_options()), + Err(Error::MalformedContinuationBundle(_)) + ), + "a non-page-aligned touched page base is a malformed bundle → must be an Err" ); } diff --git a/prover/src/lib.rs b/prover/src/lib.rs index 4ff59d339..7008619ef 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -192,6 +192,9 @@ pub enum Error { InvalidContinuationEpochSize(String), /// Continuation proof construction hit an internal invariant failure. ContinuationInvariant(String), + /// Continuation bundle is structurally malformed (fails validation before + /// any proof is checked). + MalformedContinuationBundle(String), /// A non-final continuation epoch contains the program-terminating /// instruction. The terminating instruction must be in the final epoch. HaltInNonFinalEpoch, @@ -214,6 +217,9 @@ impl fmt::Display for Error { Error::ContinuationInvariant(msg) => { write!(f, "continuation invariant failed: {msg}") } + Error::MalformedContinuationBundle(msg) => { + write!(f, "malformed continuation bundle: {msg}") + } Error::HaltInNonFinalEpoch => { write!( f, @@ -960,13 +966,10 @@ pub fn verify_with_options( // A malicious prover could set counts to 0, removing entire constraint sets. vm_proof.table_counts.validate()?; - // Bound num_private_input_pages before allocating PageConfigs. The tight max is the - // honest span of a MAX-size input plus its 4-byte length prefix: - // ceil((MAX_PRIVATE_INPUT_SIZE + 4) / DEFAULT_PAGE_SIZE) pages (no slack). + // Bound num_private_input_pages before allocating PageConfigs — the tight honest + // max, shared with the continuation verifier (see `page::max_private_input_pages`). { - use crate::tables::page::DEFAULT_PAGE_SIZE; - use executor::vm::memory::MAX_PRIVATE_INPUT_SIZE; - let max_pages = (MAX_PRIVATE_INPUT_SIZE as usize + 4).div_ceil(DEFAULT_PAGE_SIZE); + let max_pages = crate::tables::page::max_private_input_pages(); if vm_proof.num_private_input_pages > max_pages { return Err(Error::InvalidTableCounts(format!( "num_private_input_pages ({}) exceeds max ({max_pages})", diff --git a/prover/src/tables/local_to_global.rs b/prover/src/tables/local_to_global.rs index 6ff1e3284..668dc1353 100644 --- a/prover/src/tables/local_to_global.rs +++ b/prover/src/tables/local_to_global.rs @@ -83,7 +83,12 @@ pub const GENESIS_EPOCH: u64 = 0; pub const MAX_EPOCHS: u64 = 1 << 20; /// A cell's state when an epoch first touches it. -#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +// +// Deliberately NOT serde-derived: `value` is a private-input byte for a private +// first-read, so these types must never be serialized into a proof bundle (the +// bundle ships only the value-free `touched_page_bases`). Keeping the derives off +// makes re-introducing that leak a compile error, not a silent regression. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] pub struct InitClaim { /// Value the cell held when this epoch first touched it. pub value: u64, @@ -97,7 +102,8 @@ pub struct InitClaim { } /// A cell's state at the end of the epoch that touched it. -#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +/// (Not serde-derived — see [`InitClaim`].) +#[derive(Debug, Clone, Copy, PartialEq, Eq)] pub struct FiniClaim { /// Value the cell holds at this epoch's end. pub value: u64, @@ -107,8 +113,10 @@ pub struct FiniClaim { pub timestamp: u64, } -/// The init/fini boundary claims for a single touched cell. -#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +/// The init/fini boundary claims for a single touched cell. Prover-local only: +/// it holds cell values, so it is never serialized (not serde-derived — see +/// [`InitClaim`]). +#[derive(Debug, Clone, Copy, PartialEq, Eq)] pub struct CellBoundary { pub address: u64, pub init: InitClaim, diff --git a/prover/src/tables/page.rs b/prover/src/tables/page.rs index e02a46a80..f17338f41 100644 --- a/prover/src/tables/page.rs +++ b/prover/src/tables/page.rs @@ -155,6 +155,68 @@ impl PageConfig { } } +// ========================================================================= +// Private-input page math (shared by the monolithic and continuation paths) +// ========================================================================= + +/// Number of pages the private input occupies, starting at +/// `PRIVATE_INPUT_START_INDEX`. The wire format is the 4-byte length prefix plus +/// the data ([`Memory::store_private_inputs`]), and `PRIVATE_INPUT_START_INDEX` is +/// page-aligned, so the span is `ceil((prefix + len) / page_size)` consecutive +/// pages (0 when there is no input). +/// +/// SINGLE source of truth: the monolithic trace builder, the continuation prover, +/// and both verifiers' classification all derive from this count — a divergence +/// would make one path build a private page preprocessed (ELF-recomputed) while +/// the other commits it, which is a soundness bug, so do not reimplement it. +/// +/// [`Memory::store_private_inputs`]: executor::vm::memory::Memory::store_private_inputs +pub fn private_input_page_count(private_inputs: &[u8]) -> usize { + use executor::vm::memory::PRIVATE_INPUT_LENGTH_PREFIX_BYTES; + if private_inputs.is_empty() { + return 0; + } + (PRIVATE_INPUT_LENGTH_PREFIX_BYTES + private_inputs.len()).div_ceil(DEFAULT_PAGE_SIZE) +} + +/// Whether `page_base` is one of the first `num_private_input_pages` pages starting +/// at `PRIVATE_INPUT_START_INDEX` — the page-aligned span private input actually +/// occupies (see [`private_input_page_count`]). Classifying by the count (not the +/// raw `[START, START+MAX_PRIVATE_INPUT_SIZE)` byte range) keeps prover and +/// verifier in lockstep regardless of whether the region end is page-aligned. +/// +/// NOTE: a page classified private is built non-preprocessed, so its genesis is NOT +/// recomputed from the ELF. This is safe because the private-input area is reserved +/// and the reservation is enforced: `Elf::load` rejects any loadable segment +/// reaching at/above `PRIVATE_INPUT_START_INDEX` +/// (`ElfError::SegmentInPrivateInputRegion`) — covering every page this function +/// can classify private — so no ELF-declared data can live there and have its +/// genesis go unbound. +pub fn is_private_input_page(page_base: u64, num_private_input_pages: usize) -> bool { + use executor::vm::memory::PRIVATE_INPUT_START_INDEX; + let page_size = DEFAULT_PAGE_SIZE as u64; + let end = PRIVATE_INPUT_START_INDEX + num_private_input_pages as u64 * page_size; + (PRIVATE_INPUT_START_INDEX..end).contains(&page_base) +} + +/// The page bases of the first `num_private_input_pages` private-input pages, in +/// ascending order — the enumeration counterpart of [`is_private_input_page`] +/// (`is_private_input_page(b, n)` holds exactly for the aligned bases this yields). +pub fn private_input_page_bases(num_private_input_pages: usize) -> impl Iterator { + use executor::vm::memory::PRIVATE_INPUT_START_INDEX; + let page_size = DEFAULT_PAGE_SIZE as u64; + (0..num_private_input_pages as u64).map(move |i| PRIVATE_INPUT_START_INDEX + i * page_size) +} + +/// Upper bound on `num_private_input_pages` any honest proof can claim: the span of +/// a MAX-size input including its length prefix — no slack (an honest max-size +/// input occupies exactly this many pages). Both the monolithic and continuation +/// verifiers bound the deserialized, untrusted count with this before sizing AIRs. +pub fn max_private_input_pages() -> usize { + use executor::vm::memory::{MAX_PRIVATE_INPUT_SIZE, PRIVATE_INPUT_LENGTH_PREFIX_BYTES}; + (MAX_PRIVATE_INPUT_SIZE as usize + PRIVATE_INPUT_LENGTH_PREFIX_BYTES).div_ceil(DEFAULT_PAGE_SIZE) +} + // ========================================================================= // Trace generation // ========================================================================= diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index f3ca090d7..44bbdf3be 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -2457,19 +2457,12 @@ fn generate_page_tables( let mut pages = Vec::new(); let mut page_configs = Vec::new(); - // Determine which page bases hold private input data. - let private_input_page_bases: std::collections::BTreeSet = if !private_input.is_empty() { - use executor::vm::memory::PRIVATE_INPUT_START_INDEX; - let total_bytes = 4 + private_input.len(); // length prefix + data - (0..total_bytes) - .map(|i| page::page_base_for_address(PRIVATE_INPUT_START_INDEX + i as u64)) - .collect() - } else { - std::collections::BTreeSet::new() - }; + // Determine which page bases hold private input data — count-based, via the + // shared helpers (single source of truth with the continuation path). + let num_private_input_pages = page::private_input_page_count(private_input); for &page_base in &page_bases { - let config = if private_input_page_bases.contains(&page_base) { + let config = if page::is_private_input_page(page_base, num_private_input_pages) { let init_data = init_page_data.get(&page_base).cloned().unwrap_or_default(); PageConfig::with_private_input(page_base, init_data) } else if let Some(init_data) = init_page_data.get(&page_base) { @@ -3871,16 +3864,12 @@ impl Traces { } // Add private-input pages (non-preprocessed, verifier doesn't know init values) - if num_private_input_pages > 0 { - use executor::vm::memory::PRIVATE_INPUT_START_INDEX; - let first_page_base = page::page_base_for_address(PRIVATE_INPUT_START_INDEX); - for i in 0..num_private_input_pages { - configs.push(PageConfig { - page_base: first_page_base + i as u64 * page_size as u64, - init_values: None, // Verifier doesn't know these - is_private_input: true, - }); - } + for page_base in page::private_input_page_bases(num_private_input_pages) { + configs.push(PageConfig { + page_base, + init_values: None, // Verifier doesn't know these + is_private_input: true, + }); } configs.sort_by_key(|c| c.page_base); From 4b527324e49bbfded1c1c59b2d8f4266d947057c Mon Sep 17 00:00:00 2001 From: MauroFab Date: Fri, 3 Jul 2026 15:19:04 -0300 Subject: [PATCH 13/14] Run cargo fmt --- prover/src/tables/page.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/prover/src/tables/page.rs b/prover/src/tables/page.rs index f17338f41..5907be201 100644 --- a/prover/src/tables/page.rs +++ b/prover/src/tables/page.rs @@ -214,7 +214,8 @@ pub fn private_input_page_bases(num_private_input_pages: usize) -> impl Iterator /// verifiers bound the deserialized, untrusted count with this before sizing AIRs. pub fn max_private_input_pages() -> usize { use executor::vm::memory::{MAX_PRIVATE_INPUT_SIZE, PRIVATE_INPUT_LENGTH_PREFIX_BYTES}; - (MAX_PRIVATE_INPUT_SIZE as usize + PRIVATE_INPUT_LENGTH_PREFIX_BYTES).div_ceil(DEFAULT_PAGE_SIZE) + (MAX_PRIVATE_INPUT_SIZE as usize + PRIVATE_INPUT_LENGTH_PREFIX_BYTES) + .div_ceil(DEFAULT_PAGE_SIZE) } // ========================================================================= From 69ffc548b6d9f72f467e84b07f3bd4d0f0b3daf1 Mon Sep 17 00:00:00 2001 From: Nicole Date: Fri, 3 Jul 2026 16:11:16 -0300 Subject: [PATCH 14/14] add unit tests and fix doc --- docs/continuations_design.md | 4 +- executor/src/elf.rs | 7 ++-- executor/src/vm/memory.rs | 35 +++++++++++++++++ prover/src/continuation.rs | 73 ++++++++++++++++++++++++++++++++++++ prover/src/tables/page.rs | 10 +++-- 5 files changed, 120 insertions(+), 9 deletions(-) diff --git a/docs/continuations_design.md b/docs/continuations_design.md index f5c64849d..f788d7f71 100644 --- a/docs/continuations_design.md +++ b/docs/continuations_design.md @@ -270,8 +270,8 @@ otherwise a prover could classify that page private and forge the ELF byte's gen **enforced by the loader**: `Elf::load` rejects any `PT_LOAD` segment reaching at or above `PRIVATE_INPUT_START_INDEX` (`ElfError::SegmentInPrivateInputRegion`) — covering every page the verifier can classify private, which slightly exceeds `[base, base+MAX_PRIVATE_INPUT_SIZE)` -(the length prefix pushes an honest max-size input onto one more page, plus a page of -count-bound slack). +because the length prefix pushes an honest max-size input onto one more page (the count +bound is that tight span, with no extra slack). Turning the reservation from convention into an enforced invariant closes this gap for **both** the continuation and monolithic paths (they share the loader and the same non-preprocessed-private-page design). diff --git a/executor/src/elf.rs b/executor/src/elf.rs index 1d00eff4e..fa525b80c 100644 --- a/executor/src/elf.rs +++ b/executor/src/elf.rs @@ -298,9 +298,10 @@ impl Elf { // stays private); ELF data placed there would have an unbound, prover-forgeable // genesis. The verifier can classify any page from the base up to the maximum // private-input page count as private — a span that slightly exceeds - // `MAX_PRIVATE_INPUT_SIZE` (the length prefix pushes an honest max-size input onto - // one more page, and the page-count bound adds a page of slack), so we reserve the - // whole high area rather than exactly `[base, base+MAX)`. Nothing legitimate loads + // `MAX_PRIVATE_INPUT_SIZE` because the length prefix pushes an honest max-size + // input onto one more page (the page-count bound is that tight span, with no + // extra slack), so we reserve the whole high area rather than exactly + // `[base, base+MAX)`. Nothing legitimate loads // here: ELF code/data live at low addresses, and the stack (`STACK_TOP`) and // private input are runtime regions written outside `load_program`, so this does // not affect them. Turns "the private-input area holds only private input" from a diff --git a/executor/src/vm/memory.rs b/executor/src/vm/memory.rs index d4f8d1cee..ea3b06c20 100644 --- a/executor/src/vm/memory.rs +++ b/executor/src/vm/memory.rs @@ -294,3 +294,38 @@ pub enum MemoryError { #[error("Failed to allocate memory for load_bytes")] AllocationFailed, } + +#[cfg(test)] +mod tests { + use super::*; + + // The wire-format writer and every private-input page-span computation assume the + // length prefix is exactly a 4-byte LE `u32`; pin that so a change to the constant + // is caught rather than silently drifting from the page math. + #[test] + fn private_input_length_prefix_is_a_le_u32() { + assert_eq!(PRIVATE_INPUT_LENGTH_PREFIX_BYTES, 4); + assert_eq!(PRIVATE_INPUT_LENGTH_PREFIX_BYTES, size_of::()); + } + + // `store_private_inputs` must write a LE length prefix at the region base and the data + // immediately after it, at `+ PRIVATE_INPUT_LENGTH_PREFIX_BYTES`. + #[test] + fn store_private_inputs_writes_le_length_prefix_then_data() { + let mut memory = Memory::default(); + let inputs = vec![0xAAu8, 0xBB, 0xCC]; + memory.store_private_inputs(inputs.clone()).unwrap(); + + assert_eq!( + memory.load_word(PRIVATE_INPUT_START_INDEX).unwrap(), + inputs.len() as u32 + ); + let data = memory + .load_bytes( + PRIVATE_INPUT_START_INDEX + PRIVATE_INPUT_LENGTH_PREFIX_BYTES as u64, + inputs.len() as u64, + ) + .unwrap(); + assert_eq!(data, inputs); + } +} diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index ea1e2c8a8..2030e3738 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -1453,6 +1453,79 @@ mod tests { ); } + // `private_input_page_bases` must enumerate exactly the aligned bases that + // `is_private_input_page` classifies private, in ascending, page_size-spaced order. + #[test] + fn test_private_input_page_bases_enumeration() { + use executor::vm::memory::PRIVATE_INPUT_START_INDEX; + let page_size = page::DEFAULT_PAGE_SIZE as u64; + let start = PRIVATE_INPUT_START_INDEX; + + // Count 0 yields nothing. + assert_eq!(page::private_input_page_bases(0).count(), 0); + + // Ascending, exact page_size spacing from the region start. + let bases: Vec = page::private_input_page_bases(3).collect(); + assert_eq!(bases, vec![start, start + page_size, start + 2 * page_size]); + + // The enumeration and the predicate agree: every yielded base classifies + // private for that count, and the first base past them does not. + for n in 0..4usize { + for base in page::private_input_page_bases(n) { + assert!(page::is_private_input_page(base, n)); + } + assert!(!page::is_private_input_page( + start + n as u64 * page_size, + n + )); + } + } + + // The deserialized-count bound is the tight honest max: exactly the pages a MAX-size + // input occupies, with no slack. Pin the value and the tightness (checked via the byte + // span so we don't allocate a 64 MiB test input). + #[test] + fn test_max_private_input_pages_is_tight() { + use executor::vm::memory::{MAX_PRIVATE_INPUT_SIZE, PRIVATE_INPUT_LENGTH_PREFIX_BYTES}; + let page_size = page::DEFAULT_PAGE_SIZE; + let max = page::max_private_input_pages(); + + // (64 MiB + 4-byte prefix) / 256 KiB page = 257 pages (256 full data pages plus + // the one page the length prefix spills into). Pinned so a size/page change is caught. + assert_eq!(max, 257); + + // No slack: an honest MAX-size input needs the whole last page (the bound is not + // padded), and never overflows into an extra one. + let honest_bytes = MAX_PRIVATE_INPUT_SIZE as usize + PRIVATE_INPUT_LENGTH_PREFIX_BYTES; + assert!((max - 1) * page_size < honest_bytes); + assert!(honest_bytes <= max * page_size); + } + + // The verifier builds private-page configs with `include_private_genesis=false`, which + // must yield an explicitly empty genesis (never the looked-up bytes) so no verifier path + // can start depending on private data; the prover's `true` still loads the committed bytes. + #[test] + fn test_global_memory_configs_private_genesis_inclusion() { + use executor::vm::memory::PRIVATE_INPUT_START_INDEX; + let private_base = PRIVATE_INPUT_START_INDEX; + let genesis = vec![1u8, 2, 3, 4]; + let mut init_page_data = HashMap::new(); + init_page_data.insert(private_base, genesis.clone()); + + // Verifier side: empty genesis even though bytes are present in the map. + let verifier = + global_memory_configs_from_init_page_data(&[private_base], &init_page_data, 1, false); + assert_eq!(verifier.len(), 1); + assert!(verifier[0].is_private_input); + assert_eq!(verifier[0].init_values, Some(Vec::new())); + + // Prover side: the same call loads the genesis bytes into the committed config. + let prover = + global_memory_configs_from_init_page_data(&[private_base], &init_page_data, 1, true); + assert!(prover[0].is_private_input); + assert_eq!(prover[0].init_values, Some(genesis)); + } + // Negative: `num_private_input_pages` is deserialized/untrusted, so reject a bundle // whose count exceeds the max before using it to size/build the global AIRs. #[test] diff --git a/prover/src/tables/page.rs b/prover/src/tables/page.rs index 5907be201..5cba30435 100644 --- a/prover/src/tables/page.rs +++ b/prover/src/tables/page.rs @@ -171,7 +171,7 @@ impl PageConfig { /// the other commits it, which is a soundness bug, so do not reimplement it. /// /// [`Memory::store_private_inputs`]: executor::vm::memory::Memory::store_private_inputs -pub fn private_input_page_count(private_inputs: &[u8]) -> usize { +pub(crate) fn private_input_page_count(private_inputs: &[u8]) -> usize { use executor::vm::memory::PRIVATE_INPUT_LENGTH_PREFIX_BYTES; if private_inputs.is_empty() { return 0; @@ -192,7 +192,7 @@ pub fn private_input_page_count(private_inputs: &[u8]) -> usize { /// (`ElfError::SegmentInPrivateInputRegion`) — covering every page this function /// can classify private — so no ELF-declared data can live there and have its /// genesis go unbound. -pub fn is_private_input_page(page_base: u64, num_private_input_pages: usize) -> bool { +pub(crate) fn is_private_input_page(page_base: u64, num_private_input_pages: usize) -> bool { use executor::vm::memory::PRIVATE_INPUT_START_INDEX; let page_size = DEFAULT_PAGE_SIZE as u64; let end = PRIVATE_INPUT_START_INDEX + num_private_input_pages as u64 * page_size; @@ -202,7 +202,9 @@ pub fn is_private_input_page(page_base: u64, num_private_input_pages: usize) -> /// The page bases of the first `num_private_input_pages` private-input pages, in /// ascending order — the enumeration counterpart of [`is_private_input_page`] /// (`is_private_input_page(b, n)` holds exactly for the aligned bases this yields). -pub fn private_input_page_bases(num_private_input_pages: usize) -> impl Iterator { +pub(crate) fn private_input_page_bases( + num_private_input_pages: usize, +) -> impl Iterator { use executor::vm::memory::PRIVATE_INPUT_START_INDEX; let page_size = DEFAULT_PAGE_SIZE as u64; (0..num_private_input_pages as u64).map(move |i| PRIVATE_INPUT_START_INDEX + i * page_size) @@ -212,7 +214,7 @@ pub fn private_input_page_bases(num_private_input_pages: usize) -> impl Iterator /// a MAX-size input including its length prefix — no slack (an honest max-size /// input occupies exactly this many pages). Both the monolithic and continuation /// verifiers bound the deserialized, untrusted count with this before sizing AIRs. -pub fn max_private_input_pages() -> usize { +pub(crate) fn max_private_input_pages() -> usize { use executor::vm::memory::{MAX_PRIVATE_INPUT_SIZE, PRIVATE_INPUT_LENGTH_PREFIX_BYTES}; (MAX_PRIVATE_INPUT_SIZE as usize + PRIVATE_INPUT_LENGTH_PREFIX_BYTES) .div_ceil(DEFAULT_PAGE_SIZE)