feat(recursion): supply DECODE/global-memory-genesis roots via private input for continuation verify

[Oppen]

Summary

Mirrors #782's monolithic mechanism for the continuation path: a caller (the recursion guest) can supply the DECODE preprocessed root and each touched data page's genesis root instead of the verifier recomputing them from the ELF, skipping the in-VM FFT + Merkle build. Supplied roots are used verbatim; the binding shifts to the consumer's recompute-and-compare of the folded identity, exactly like the monolithic path.

• verify_global's genesis-page classification (ELF-backed vs zero-init) is derived from ELF segment address ranges instead of materializing a full byte-level image when roots are supplied, since the real bytes are never read once a root covers that page.
• Page lookups are keyed by page number (page_base >> log2(page_size)) rather than the raw page-aligned address, since the low bits are always zero.
• verify_continuation keeps its existing signature (trustless recompute); verify_continuation_with_roots is the new supplied-roots entry point, and continuation_precomputed_commitments lets a caller derive the roots to supply for a given bundle.

This PR does not change the wire format or add a guest-facing API — that's perf/continuation-rkyv-zero-copy, stacked on top of this one.

Test plan

• cargo test -p lambda-vm-prover --lib (515 passed)
• New test: test_verify_continuation_with_supplied_roots — supplied-roots verify matches the trustless recompute, and a tampered supplied root is rejected
• cargo clippy --all-targets -- -D warnings / cargo fmt --check

[Oppen]

/ai-review

[github-actions]

Codex Code Review

• Medium — continuation.rs:797: Missing page commitments trigger debug_assert!, allowing malformed/untrusted supplied roots to panic debug verifiers. Release builds instead silently substitute the empty-page commitment. Validate completeness normally and reject with false/Err consistently.

[claude]

Review — supplied-roots continuation verify

Reviewed for safety/soundness, bugs, performance, and readability. This is a careful, well-documented change that faithfully mirrors the monolithic supplied-roots path (PR #782) onto the continuation verifier. No critical/high issues found.

Soundness (looks correct)

• Verbatim supplied roots don't weaken in-call verification. The DECODE and per-page genesis roots are used unbound, but the epoch/global Fiat-Shamir transcripts still seed from elf_bytes, and each supplied root must match the prover's committed trace — a wrong/mismatched root diverges FS or fails to match the committed AIR, so multi_verify rejects. You can't make a bad proof (or a proof for a different ELF) verify by choosing roots. The recursion-attestation binding via consumer recompute is out of scope here, as documented.
• Classify-only classification is consistent with the byte-level path. PagedMem::set marks a cell occupied regardless of value, so build_init_page_data gives an entry to every page overlapping an ELF segment (even all-zero regions), matching byte-level with_data. elf_page_has_data uses the same [base_addr, base_addr + values.len()*4) range with a matching half-open overlap test, and the private-page check runs first in both paths. So the supplied set from continuation_precomputed_commitments exactly covers the classify-needed set — no missing entries in honest use.
• Overflow at STACK_TOP handled via saturating_add; reg_fini length / num_private_input_pages bounds are unchanged and still enforced up front.

Minor

• One inline note on the A missing entry here would silently recompute (slow) comment: on the classify-only path a missing entry actually computes a zero-init root over the empty init_values (spurious rejection), not a slow-but-correct recompute. Outcome is safe; the wording just undersells why the debug_assert! matters.

Nits (non-blocking)

• page_number's alignment debug_assert and the PAGE_SIZE_LOG2 const _ assert are nice touches.
• Good negative-test coverage (tampered DECODE root rejected; supplied-roots output equals the recompute path).

Nothing blocking from my side.

[github-actions]

AI Review

PR #844 · 2 changed files

Findings

Status	Sev	Location	Finding	Found by
confirmed	low	executor/programs/asm/data_page_touch.s:19	Misleading instruction numbering in data_page_touch.s	moonmath zro/minimax-m3
confirmed	low	prover/src/continuation.rs:215	Doc comment for new preprocessed parameter appended to unrelated AIR-design doc block	moonmath zro/minimax-m3
confirmed	low	prover/src/continuation.rs:1131	No negative test for non-page-aligned entries in page_genesis_commitments	moonmath zro/minimax-m3

Status column reflects the verdict from the verifier: deepseek-verifier (openrouter/deepseek/deepseek-v4-pro).

AI-003: Misleading instruction numbering in data_page_touch.s

• Status: confirmed
• Severity: low
• Location: executor/programs/asm/data_page_touch.s:19
• Found by: moonmath:zro/minimax-m3
• Verified by: deepseek-verifier:openrouter/deepseek/deepseek-v4-pro
• Rejected by: -

Claim

The numbering comments only label the four main instructions (# 1–4) and then jump to "# 5: Halt" on the ecall, even though three explicit instructions (li a0, 0, li a7, 93, ecall) sit between # 4 and the ecall. A reader skimming the comments will undercount the program length and the touched cells (each li/ecall is its own CPU row, and ecall is the Halt syscall that ends the run).

Evidence

Lines 12–19: comments "# 1", "# 2", "# 3", "# 4" precede 4 instructions, then li a0, 0, li a7, 93, ecall # 5: Halt are three more lines. The "# 5" is on the ecall line, not at instruction 5.

Suggested fix

Rename the trailing comment to # Halt (no number), or number every instruction. Either keeps the fixture self-explanatory for the next reader.

AI-004: Doc comment for new `preprocessed` parameter appended to unrelated AIR-design doc block

• Status: confirmed
• Severity: low
• Location: prover/src/continuation.rs:215
• Found by: moonmath:zro/minimax-m3
• Verified by: deepseek-verifier:openrouter/deepseek/deepseek-v4-pro
• Rejected by: -

Claim

The new doc for preprocessed is appended to the AIR's design doc, mixing AIR semantics with a parameter description. The result reads as one continuous doc but the two paragraphs cover unrelated concerns (AIR invariants vs. an API parameter); a reader looking at the parameter's docs may not realize they belong to a different section.

Evidence

Lines 200–214: existing AIR design doc. Lines 215–218: new preprocessed parameter doc, concatenated into the same /// block with no blank /// line, no heading, and no explicit Arguments: section.

Suggested fix

Either start a new /// paragraph with a heading like /// # Arguments (or /// Parameters), or split the new content into a separate doc comment block on the parameter itself. Cosmetic; not a correctness issue.

AI-009: No negative test for non-page-aligned entries in page_genesis_commitments

• Status: confirmed
• Severity: low
• Location: prover/src/continuation.rs:1131
• Found by: moonmath:zro/minimax-m3
• Verified by: deepseek-verifier:openrouter/deepseek/deepseek-v4-pro
• Rejected by: -

Claim

verify_continuation_with_roots adds a structural validation rejecting a page_genesis_commitments entry whose page_base isn't page-aligned (mirrors the touched_page_bases check at line 1121), but there is no test that exercises this branch. The analogous touched_page_bases rejection is covered by test_split_verify_rejects_non_page_aligned_touched_page_base.

Evidence

Lines 1131–1139 are new code in this PR (let-chain check) without a matching test_* case; the existing negative tests in the same mod tests block do not perturb page_genesis_commitments.

Suggested fix

Add a sibling test (e.g. test_verify_continuation_with_supplied_roots_rejects_non_aligned_base) that perturbs one entry of page_commitments by +1 and asserts Err(Error::MalformedContinuationBundle(_)), matching the pattern of test_split_verify_rejects_non_page_aligned_touched_page_base.

Reviewer Lanes

Lane	Model	Prompt	Status	Findings
glm	openrouter/z-ai/glm-5.2	general	success	0
kimi	openrouter/moonshotai/kimi-k2.7-code	general	success	0
minimax	minimax/MiniMax-M3	general	error: opencode failed (provider/auth/runtime error) and no findings were submitted	0
moonmath	zro/minimax-m3	general	success	4
nemotron	openrouter/nvidia/nemotron-3-ultra-550b-a55b	general	success	5

Verification Lanes

Lane	Model	Status	Confirmed	Rejected	Uncertain
deepseek-verifier	openrouter/deepseek/deepseek-v4-pro	success	3	5	0

Native Codex and Claude reviews run separately and post their own comments. They are not included in this structured provenance report.

Discarded candidates (5) — rejected by the verifier

• Classification-only path may diverge from byte-level classification in edge cases (prover/src/continuation.rs:305, found by nemotron:openrouter/nvidia/nemotron-3-ultra-550b-a55b) — The PR introduces a dedicated test test_classify_only_matches_byte_level_classification that asserts equivalence between the two classification paths on two fixtures (data_page_touch and all_loadstore_32). The test checks that page_base, is_private_input, and init_values presence match between byte-level and classify-only paths. The claim about BSS/p_filesz divergence is purely speculative without a concrete counterexample, and the ELF loader's elf.data field is populated from PT_LOAD segments with actual data. The test coverage is explicit guard against this concern.
• Extra supplied roots for zero-init and private pages are silently ignored (prover/src/continuation.rs:806, found by nemotron:openrouter/nvidia/nemotron-3-ultra-550b-a55b) — The page_genesis_commitments parameter is explicitly documented as being for 'touched data pages' (lines 1025-1027), and continuation_precomputed_commitments (lines 1186-1189) only generates entries for non-private pages with init_values. The code at lines 798-805 already validates that every expected data page has a corresponding entry — extra entries for other page types are genuinely harmless (they don't affect which pages are built or how preprocessed commitments are selected). Silently ignoring extra entries in a map is standard, benign API behavior.
• elf_page_has_data uses segment.values.len() * 4 assuming u32 words; verify this matches ELF loading (prover/src/continuation.rs:334, found by nemotron:openrouter/nvidia/nemotron-3-ultra-550b-a55b) — The * 4 assumption is explicitly documented in a comment at line 333: '4 bytes/word (Segment::values: Vec<u32>)'. The exact same assumption (i as u64 * 4) is used in build_initial_image_paged at line 2050 of trace_builder.rs when consuming the same segment.values. Both code paths are internally consistent, and the type is documented. This is not a fragile assumption but consistent code with a clear comment.
• prove_epoch always passes None for decode_commitment (parameter is dead on prover path) (prover/src/continuation.rs:533, found by moonmath:zro/minimax-m3) — The decode_commitment parameter was intentionally added to build_epoch_airs for use on the verifier path (the recursion guest skips in-VM recompute). On the prover path (prove_epoch), the DECODE commitment is computed locally by VmAirs::new from the ELF, so passing None is by design. The PR adds #[allow(clippy::too_many_arguments)] to address the lint. A parameter being unused on one path is not a bug — it's a well-documented API that serves the verifier.
• verify_continuation_with_roots trust model could be more prominently documented (prover/src/continuation.rs:1033, found by nemotron:openrouter/nvidia/nemotron-3-ultra-550b-a55b) — The doc comment at lines 1024-1032 puts the VERBATIM warning in the second paragraph in ALL CAPS: 'Supplied roots are used VERBATIM — they are NOT bound to elf_bytes here'. It also explicitly cross-references the monolithic path's verify_with_options supplied roots for parity. The claim that this is 'buried in the third paragraph' is incorrect — it's the second paragraph, prominently capitalized, and the entire doc block is only 3 paragraphs (~8 lines total). The documentation is clear and sufficiently prominent.

Raw lane outputs, candidates, final issues, and model metrics are uploaded as workflow artifacts.

[Oppen]

/ai-review

[github-actions]

Codex Code Review

• Medium – unnecessary full page FFT/Merkle computation (continuation.rs): zero_init_preprocessed_commitment(opts) is computed unconditionally, even when gm_configs contains no zero-initialized page. For non-static proof options this builds a 256K-row page commitment, undermining the supplied-roots optimization. Compute it lazily only when a zero-init config is encountered.

[claude]

Reviewed the full diff with a focus on the supplied-roots soundness. No significant issues found — this is a clean, well-tested change.

What I verified:

• Classify-only ⟺ byte-level equivalence holds robustly. elf_page_has_data's range overlap matches the byte-level init_page_data classification: build_initial_image_paged sets every byte of every segment word (zeros/BSS included, since the loader extends values to p_memsz), and PagedMem::iter() yields all set cells regardless of value. The one edge case that would break this — a zero-length segment whose base sits strictly inside a page — can't occur because empty segments are filtered at load (executor/src/elf.rs:355). Prover, verifier byte-level, and verifier classify-only all classify each page identically, which is what test_classify_only_matches_byte_level_classification locks in.
• Missing-entry rejection is correct: with_data(base, Vec::new()) gives init_values: Some(vec![]), so the !is_private_input && init_values.is_some() filter catches every classified-data page and rejects a missing supplied root explicitly instead of silently falling back to the zero-init root.
• Verbatim roots + downstream binding mirror the monolithic page_commitments path; the alignment/keying (raw page_base) is internally consistent across build, lookup, and validation; tampered page/DECODE roots are rejected via trace mismatch (covered by the new test).

Minor (optional, non-blocking): extra page_genesis_commitments entries whose bases don't correspond to a classified-data page (typo base, or a base for a zero-init/private page) are silently ignored rather than rejected. Soundness is preserved by the downstream recompute-and-compare, and this matches the monolithic path's leniency, so no change is required — just noting the interface accepts unmatched entries without complaint.

[Oppen]

On Codex feedback:

1. We do that everywhere AFAIK
2. No real program has no zero-init pages: they all use the stack, and most have at least some zero-init global, not a realistic problem
3. We control the blowup and match it to real usage