fix(page): private-input PAGE OFFSET is unconstrained — forgeable memory contents (two invariants, both with exploits)

[MauroToscano]

Summary

Private-input PAGE and GLOBAL_MEMORY tables are built without a preprocessed commitment, so
their OFFSET column is a free, prover-chosen main-trace column. Since the memory-bus token address
is address_lo = page_base_lo + OFFSET, a malicious prover can point a page row at an address of
its choosing and forge that address's genesis value.

This is a memory-soundness break, and therefore a VM-soundness break. A proof that
verifies against the unmodified ELF can attest a public_output the program cannot produce.
It is demonstrated end to end in this branch, under the production proof options.

The spec got this right — this is an implementation deviation, not a spec gap.
spec/src/page.toml declares offset as type = "RowIndex", which spec/src/config.toml defines as
"A preprocessed column holding the row index (zero-indexed)" with preprocessed = true. Both
properties this bug breaks are therefore mandated by the landed spec, and page.toml never
contemplates a private-page exception. See The spec already requires this.

Closing it needs two invariants, not one — the first fix here restores one of them and a second
working forgery survives it:

invariant	how it was broken	fix
one row per address, within a page	free OFFSET on private pages	af33896d — preprocess OFFSET
one page per address	runtime_page_ranges never deduped	2bdc8968 — reject duplicate bases

Route 1 — free OFFSET on private pages

The only mechanism that binds a PAGE's OFFSET/INIT is in the verifier
(crypto/stark/src/verifier.rs:1184-1213):

if air.is_preprocessed() {
    let expected = air.precomputed_commitment();
    // reject unless the proof's precomputed root == expected
    transcript.append_bytes(&expected);                            // FS-bound to the CORRECT columns
    transcript.append_bytes(proof.lde_trace_main_merkle_root());
} else {
    transcript.append_bytes(proof.lde_trace_main_merkle_root());   // nothing pinned
}

is_preprocessed() is true only when with_preprocessed(...) was called — and prover/src/lib.rs
deliberately skipped it for config.is_private_input, as did global_memory_air in
prover/src/continuation.rs. There is no backstop: PAGE uses EmptyConstraints,
NullBoundaryConstraintBuilder returns vec![], no PageConstraints type exists, and no constraint
anywhere referenced cols::OFFSET.

Nothing external pins it either. prover/src/statement.rs absorbs the ELF digest, public output,
table counts and num_private_input_pages — a count — but no digest of the private input's
contents or layout, and verify(vm_proof, elf_bytes) is never given the private input. That is by
design (the input is private), which means soundness rested entirely on address confinement —
exactly what a free OFFSET removes.

The spec already requires this

spec/src/page.toml declares the column as

[[variables.input]]
name = "offset"
type = "RowIndex"
desc = "The offset from the page base address."

and spec/src/config.toml defines that type as

[[variables.types]]
label = "RowIndex"
subtypes = ["Word"]
desc = "A preprocessed column holding the row index (zero-indexed)."
preprocessed = true

So the spec mandates both properties this bug broke: offset must be preprocessed, and it must
hold the row index. page.toml also never mentions private-input pages — the is_private_input
bypass has no basis in the spec at all. This is an implementation deviation from the landed spec, not
a gap in it, and af33896d restores what type = "RowIndex" already specified.

Root cause in one sentence: Blum-style offline memory checking is fork-resistant only because
the init/final sets hold exactly one entry per address, and it is the preprocessed dense OFFSET
enumeration that supplied that invariant.

prover/src/tables/page.rs also documented the false assumption this grew from — that all columns
"including OFFSET and INIT" are "constrained via the memory bus". The bus constrains the values a
token carries against its counterpart; it never constrains which address a row names.

The forgery

Displacement, one row, for a target address A read at time t with real byte r:

• the honest page row provides (A, 0, r) and is set to consume (A, t, X)
• the repointed private row (OFFSET := A − page_base, INIT := X, FINI := r, TIMESTAMP := 0)
  provides (A, 0, X) and consumes (A, 0, r)
• MEMW consumes (A, 0, X) and provides (A, t, X)

The multisets are equal, so the Memory bus balances. AreBytes[INIT, FINI] is satisfied because X
is a byte; the only extra cost is moving one MU_ARE_BYTES unit between two BITWISE rows.

TIMESTAMP = 0 is available because PAGE's TIMESTAMP columns are unconstrained, and PAGE-C3
hardcodes ts = 0, which is what a first access needs.

It needs no private input, and no guest cooperation

num_private_input_pages is a VmProof field. verify_proof_parts bounds it only against
max_private_input_pages() (2049) and then appends that many non-preprocessed pages. The verifier
has no private input to compare against. Even without touching the wire format,
build_initial_image plants the bytes whenever private_input is non-empty, so one dummy byte
through the public prove API creates the page — for any program.

Reach: address_hi is a per-page constant and private bases give address_hi ∈ {0, 1}, i.e. the
whole low 4 GiB — .text/.rodata/.data/.bss and the heap. The stack is out of reach
(STACK_TOP = 0xFFFF_FFFF_FFFF_FFF0 ⇒ address_hi = 0xFFFF_FFFF). Instructions come from the
separately-committed DECODE table, so this is data forgery, not code injection — but for any
program whose result depends on its own constants, static data or zero-initialised memory, it yields
an arbitrary accepted result.

The workloads that matter are the exposed ones: the ethrex block guest reads its entire
ProgramInput via get_private_input(), and the recursion verifier's whole blob (inner ELF + inner
proof) lives in private-input pages.

Fix

Preprocess OFFSET alone for private pages, leaving INIT in the main trace. OFFSET is a
dense 0..page_size−1 enumeration — entirely content-independent — so committing it publishes
nothing about the private input. cols::OFFSET = 0 in both PAGE and GLOBAL_MEMORY and
with_preprocessed's contract is "columns 0..n are precomputed", so n = 1 isolates it with no
column reordering.

This is not a new mechanism. The verifier already enforces exactly this binding, and ELF-data and
zero-init pages already depend on it. Private pages bypassed it; the fix stops bypassing it for the
one column that is public. Zero added constraint degree; one extra Merkle root per private page.

Static constants for blowup 2/4/8 are generated with the existing compute_static_commitments
binary, with the standard recompute fallback. private_page_static_matches_recompute_for_all_blowups
also asserts the OFFSET-only root differs from the OFFSET+INIT root — equal bytes would
mean a call site is committing the wrong column count, which is the regression that would silently
reopen this.

Route 2 — duplicate page coverage (survives the route-1 fix)

Pinning OFFSET restores "one row per address within a page". It does not restore "one page per
address", and the same fork is reachable without any free column.

page_configs_from_elf_and_runtime appended one PageConfig::zero_init per runtime_page_ranges
entry and sorted by base — a Vec, never deduped — while verify_proof_parts validated only
table_counts and num_private_input_pages, passing runtime_page_ranges through untouched with a
free u64 base.

So a prover declares RuntimePageRange { base: <a real ELF .data page base>, count: 1 }. That
address is then covered by two PAGE tables, and both carry correct, verifier-recomputed
preprocessed commitments — the injected one is an ordinary zero-init page whose OFFSET and
INIT match the shipped static_zero_page_commitment. Nothing is forged at the commitment layer,
which is precisely why the route-1 fix does not touch it. Two genesis tokens at one address; the two
rows swap which token each consumes.

Severity is lower than route 1 — the injected value is always 0, since zero-init is the only page
kind conjurable at a chosen base, so the primitive is "force a chosen address to read 0 at
genesis" rather than "arbitrary byte at arbitrary address". No route back to arbitrary values was
found. Still a forged execution: zeroing a length, a bound, a chain-id byte or a root byte is
enough. And it is independent of the private-input feature entirely.

Fix

3ee45cb5 validates runtime_page_ranges (alignment, zero count, address-space overflow) and
bounds the total page count before materialising configs; 2bdc8968 rejects duplicate bases via
a single adjacent-equality scan after the existing sort, which covers the ELF, runtime and private
sources at once.

Two design notes:

• page_configs_from_elf_and_runtime is now fallible and takes a max_pages cap, rather than
  adding a separate validator the verifier must remember to call. It is the only production caller,
  so putting enforcement inside the reconstruction means a future caller cannot skip it.
• The cap is proofs.len(), not a new policy constant. Every page config needs its own sub-proof, so
  a layout wanting more pages than the proof carries can never verify — the bound is exact and
  provably cannot reject honest output.

⚠️ The two commits are not independent in one direction. The alignment check in 3ee45cb5 is
what makes 2bdc8968's equality check a complete overlap check: page-aligned pages of one size
either share a base or are disjoint, so there is no partial-overlap case. Reverting 3ee45cb5 alone
would silently weaken 2bdc8968. Noted in both commit messages.

3ee45cb5 also closes a verifier DoS: the old for i in 0..count loop ran with an unbounded
u64 from the proof before the expected_proof_count check that would have rejected it, so
RuntimePageRange { base: 0, count: u64::MAX } made the verifier allocate until it died.

Tests

b6101a68 carries end-to-end forged-proof regression tests for both routes, under
GoldilocksCubicProofOptions::with_blowup(2) — what public verify uses — through the production
multi_prove / verify_with_options path.

dup_duplicate_page_forgery_is_rejected                             ... ok
dup_negative_control_without_compensating_row_fails                ... ok
dup_structural_duplicate_page_coverage_is_rejected                 ... ok
forged_private_page_offset_is_rejected                             ... ok
poc_control_honest_harness_verifies                                ... ok
poc_negative_control_direct_init_tamper_on_preprocessed_page_fails ... ok
poc_negative_control_forged_run_without_repointed_row_fails        ... ok
poc_real_ethrex_inputs_produce_private_input_pages                 ... ok

Both forged_private_page_offset_is_rejected and dup_duplicate_page_forgery_is_rejected assert
rejection of proofs that were accepted on origin/main, so each is a genuine pass→fail hinge on
its fix.

The controls are what make the set non-vacuous, and they earned their place:

• poc_control_honest_harness_verifies — honest use of the same harness must still produce a valid
  proof. This caught a real bug in the first draft of the DoS guard, which bounded the range's
  exclusive end; the stack's top page legitimately sits at 0xfffffffffffc0000, where that end is
  exactly 2^64, so every honest proof was rejected. With only "the forgery is rejected" criteria
  that would have read as success. Fixed to bound the last byte, pinned by
  the_top_page_of_the_address_space_is_accepted.
• poc_negative_control_direct_init_tamper_on_preprocessed_page_fails — the same forged execution,
  but INIT overwritten directly on the target's own ELF-data page. The bus balances perfectly, so
  the only possible rejector is that page's preprocessed commitment — and it rejects. That isolates
  the mechanism: route 1 was precisely its absence on private pages, not a flaw in it.
• poc_negative_control_forged_run_without_repointed_row_fails and
  dup_negative_control_without_compensating_row_fails — the forged execution without its
  compensating row is rejected, so the harness discriminates rather than accepting everything.

Plus page_layout_tests (10 tests) covering ELF-page aliasing, identical and overlapping ranges,
unaligned bases, u64::MAX / u64::MAX/2 / 2^40 counts, one-over-the-cap, zero count, and two
overflow shapes.

Full sweep: 539 passed (-p lambda-vm-prover), executor lib 29, crypto/ethrex-crypto 14,
make lint exit 0. The 5 remaining failures are the known missing
program_artifacts/recursion/*.elf set. Every continuation test passes, including
test_continuation_multipage_private_input, test_split_verify_rejects_{inflated,deflated,oversized}_num_private_input_pages
and test_commit_across_epochs_verifies; and both honest paths most exposed to the new layout
validation run green — test_prove_ef_io_demo_concatenates (private input) and
test_deep_stack_runtime_pages_roundtrip (runtime pages).

Scope of the class

Seven tables use EmptyConstraints: bitwise, bytewise, decode, halt, page, register, keccak_rc. All
receive with_preprocessed in VmAirs::new except bytewise and halt, and both are benign
here:

• HALT's Memory-bus tokens use BusValue::constant(1) for is_register and a constant address — it
  cannot name an attacker-chosen address.
• BYTEWISE is not on the Memory bus at all, and its columns are pinned by lookups into the
  preprocessed BYTE_ALU table.

So PAGE and GLOBAL_MEMORY were the only instances.

Two follow-ups, documented but not fixed here

• minimal_bitwise has a non-preprocessed branch, currently reachable only from tests because
  all three production call sites pass false. A non-preprocessed BITWISE AIR would be a broader
  hole than this one: BITWISE backs AreBytes, so an unpinned table would let a witness prove an
  arbitrary field element is a byte. A comment at the branch now spells this out, and that a fourth
  caller passing true must give the minimal table its own commitment first.
• The prover's precomputed-tree cache is keyed by the expected root and skips the rebuild check
  on a hit (crypto/stark/src/prover.rs:1161-1170). So a cold cache makes the prover refuse a
  tampered trace while a warm cache silently substitutes the correct tree and leaves rejection to the
  verifier. Soundness is unaffected — the verifier catches it either way — but "the prover would
  refuse" is not a safe assumption, and tests relying on it are order-dependent.