recursion: supply DECODE/page commitments via private input; bind them to the inner ELF via a program_id fold

[Oppen]

Summary

The recursion verifier guest verifies an inner lambda-vm proof in-VM. It receives the inner program's (VmProof, elf, decode_commitment, page_commitments) via private input and passes the precomputed DECODE/ELF-data-page roots to verify_with_options — skipping the in-VM FFT+Merkle rebuild.

On success it commits program_id(inner_elf, decode, pages) || inner_public_output, where program_id is a domain-tagged Keccak fold of elf_digest || pc_start || decode_root || sorted(page_base || page_commitment).

Soundness

verify_with_options does not bind the supplied roots to inner_elf: the verifier's preprocessed-root check compares the proof's root against the supplied root, and when the supplied root is prover-controlled (as it is here) both sides are attacker-chosen. A custom prover can therefore constrain program Y while absorbing elf_digest(X) into the statement, and verify returns Ok(true). This is demonstrated by recursion_soundness_gap_poc.

The program_id fold closes this: because the supplied roots are folded into the committed identity, a substituted root yields a program_id that differs from the one an honest native recompute for the intended program produces. The binding is established outside the guest — the top-level host recomputes program_id from the trusted ELF (an expensive FFT+Merkle pass, done once, off-VM) and rejects on mismatch. The guest itself does not self-enforce the id; it only commits it. Committing inner_public_output alongside makes the attestation cover the result, not just identity (bound via the COMMIT bus-balance check, not merely the transcript).

ProofOptions is not private input — it is fixed per build via one of two mutually-exclusive Cargo features (min / blowup8), producing recursion-min.elf / recursion-blowup8.elf. Otherwise a malicious input could pick trivially weak options. Only blowup8 is sound; min (blowup 2 / 1 query) is an intentionally-insecure diagnostic under bench_vs/.

Scope

This is a single-step verifier guest and is sound under the trust model above (host recomputes program_id and checks the output). It is not multi-level recursion: the guest commits its immediate inner program's identity, not a base-program claim threaded up a chain. Sound multi-level recursion (IVC) additionally requires a carried claim + a verifier-identity anchor; that is a separate, future change.

Measurements

• recursion-min (empty inner, 1 query): 116.9M cycles — unchanged vs the precomputed-roots baseline; the fold adds only a few Keccaks.
• recursion-blowup8 (empty inner, 128-bit): ~3.0B cycles.
• Fibonacci inner committed 40 bytes (32-byte program_id + 8-byte output); empty committed 32; in-VM verify accepted in both.

Test plan

• recursion_soundness_gap_poc — a custom prover commits elf_digest(X) while constraining Y; asserts verify_with_options accepts (verify is not the binding) and that the program_id fold makes the substitution detectable (forged_id != honest_id). Includes a not-vacuous guard and an honest-recompute (None,None) negative control.
• recursion_smoke_test — blob round-trip + host verify; corrupted-commitment rejection; execute/prove pipelines assert the guest commits program_id || output byte-for-byte.
• cargo clippy / cargo fmt --check clean on the prover crate.

Build

• Recursion-elf presets serialized with .NOTPARALLEL (both build the same crate to the same target dir; the post-lock cp could race under make -j).
• test-fast / test-prover now build the recursion ELFs, and the artifact-gated recursion tests are no longer #[ignore]d (needing a build artifact is not a reason to skip a test).

[Oppen]

/ai-review

[github-actions]

Codex Code Review

Findings

• High: prover-controlled preprocessed commitments break recursion soundness in main.rs. The guest now deserializes decode_commitment and page_commitments from private input and passes them to verify_with_options at main.rs. That verifier path is only sound when those commitments are trusted verifier parameters; otherwise a malicious proof can be generated against arbitrary DECODE/PAGE preprocessed roots while the guest still commits elf_digest(inner_elf). The ELF digest in the transcript does not prove those supplied roots were derived from that ELF. The new corruption test only mutates commitments for an honestly generated proof, so it misses the malicious-proof case. Fix by recomputing these commitments from inner_elf in the guest, or by changing the statement so the guest no longer claims to verify a specific ELF unless the preprocessed roots are independently bound to it.

• Medium: parallel make can produce swapped recursion verifier artifacts in Makefile. recursion-min.elf and recursion-blowup8.elf build the same crate into the same CARGO_TARGET_DIR and copy the same release/recursion-bench path with different features. Under make -j, the two recipes can race so one artifact copies the other feature build. Use separate target dirs per preset, serialize these targets, or build/copy under a shared lock.

Static review only; I did not build or run tests per the sandbox instructions.

[claude]

Review: recursion guest — private-input DECODE/page commitments + committed program identity

Read the full diff and traced the dependencies (verify_with_options, Commitment = [u8; 32], blowup8() vs the guest hardcoded GoldilocksCubicProofOptions::with_blowup(8), and the postcard tuple ordering). The design is sound and well-documented:

• Soundness: ProofOptions correctly kept out of private input (hardcoded per min/blowup8 feature) — the reasoning in the description is right. decode_commitment/page_commitments are safely untrusted: a wrong value diverges the inner Fiat-Shamir transcript, giving Ok(false), exercised by the new test_recursion_rejects_corrupted_commitment.
• Committed output: guest and host (expected_committed_output) build the same elf_digest || decode_commitment || page_commitments byte layout (page entries = LE-u64 base + 32-byte commitment); capacity math and encoding match. Adding elf_digest for full program identity is the right call.
• Consistency: guest decode tuple matches host encode tuple; test blowup8() matches the guest hardcoded blowup8 options, so the in-VM assert!(ok) will not spuriously fail.
• No dead code left behind: recursion dropped from RECURSION_GUESTS, all test call-sites migrated to recursion-<preset>.

Findings

• Low/Medium — Makefile parallel-build race (see inline comment on the two preset rules): both presets build the same crate to the same release/recursion-bench path in a shared target dir; the post-lock cp can copy the other preset binary under make -j. Serial CI is unaffected, but make -j compile-recursion-elfs locally can silently produce a mislabeled ELF. Suggest a per-preset target dir or .NOTPARALLEL.

Nothing else blocking. The intentionally-insecure min preset (1 FRI query) is clearly a diagnostic/bench artifact under bench_vs/, not a production verifier, and is well-flagged in comments.

[github-actions]

AI Review

PR #782 · 8 changed files

Findings

Status	Sev	Location	Finding	Found by
candidate	critical	prover/src/tests/recursion_soundness_gap_poc.rs:31	New test file recursion_soundness_gap_poc.rs missing fri_final_poly_log_degree in MIN_PROOF_OPTIONS struct literal	moonmath zro/minimax-m3
candidate	critical	prover/src/tests/recursion_soundness_gap_poc.rs:194	absorb_statement call in recursion_soundness_gap_poc.rs missing fri_final_poly_log_degree argument	moonmath zro/minimax-m3
candidate	low	prover/src/tests/recursion_smoke_test.rs:566	test_recursion_blob_decodes_and_verifies_on_host no longer ignored — panics if empty.elf missing	moonmath zro/minimax-m3
candidate	low	prover/src/tests/recursion_smoke_test.rs:611	test_recursion_rejects_corrupted_commitment panics if empty.elf artifact missing	moonmath zro/minimax-m3

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

AI-001: New test file recursion_soundness_gap_poc.rs missing fri_final_poly_log_degree in MIN_PROOF_OPTIONS struct literal

• Status: candidate
• Severity: critical
• Location: prover/src/tests/recursion_soundness_gap_poc.rs:31
• Found by: moonmath:zro/minimax-m3
• Verified by: -
• Rejected by: -

Claim

The MIN_PROOF_OPTIONS const struct literal at lines 31-37 only initializes 4 fields (blowup_factor, fri_number_of_queries, coset_offset, grinding_factor). ProofOptions (crypto/stark/src/proof/options.rs:44-53) requires 5 fields including fri_final_poly_log_degree: u8. Rust will reject this with "missing field fri_final_poly_log_degree", and since the file is registered via mod.rs line 47 (pub mod recursion_soundness_gap_poc;) under #[cfg(test)], cargo test -p lambda-vm-prover will fail to compile the entire prover test crate.

Evidence

Lines 31-37 of recursion_soundness_gap_poc.rs set only blowup_factor/fri_number_of_queries/coset_offset/grinding_factor; struct definition at crypto/stark/src/proof/options.rs:44-53 requires pub fri_final_poly_log_degree: u8,. All other call sites (statement_tests.rs:59, lib.rs:925,1082, continuation.rs:102) pass the field explicitly, and the pre-existing recursion_smoke_test.rs:39 was updated to include fri_final_poly_log_degree: 7, — confirming the new file simply forgot to do the same.

Suggested fix

Add fri_final_poly_log_degree: 7, (or the value used by the recursion guest's build-time min preset) to the MIN_PROOF_OPTIONS struct literal, matching recursion_smoke_test.rs:39.

AI-002: absorb_statement call in recursion_soundness_gap_poc.rs missing fri_final_poly_log_degree argument

• Status: candidate
• Severity: critical
• Location: prover/src/tests/recursion_soundness_gap_poc.rs:194
• Found by: moonmath:zro/minimax-m3
• Verified by: -
• Rejected by: -

Claim

The custom_prove_with_statement_elf helper calls absorb_statement with only 7 arguments (lines 194-202); the function signature in statement.rs:87-96 takes 8, with the final one being fri_final_poly_log_degree: u8. Rust will reject the call as "this function takes 8 arguments but 7 arguments were supplied". This is a separate compile error in the same file as the MIN_PROOF_OPTIONS one.

Evidence

statement.rs:86-96 declares pub(crate) fn absorb_statement(..., fri_final_poly_log_degree: u8,). Every other call site (statement_tests.rs:51-60 and 144-153, lib.rs:917-926 and 1074-1083, continuation.rs:92-103) passes 8 arguments and the last one is the fri_final_poly_log_degree. The test file at lines 194-202 closes the call after &runtime_page_ranges, without the 8th argument. opts is in scope at the call site so the fix is opts.fri_final_poly_log_degree.

Suggested fix

Add opts.fri_final_poly_log_degree as the 8th argument to the absorb_statement call at line 194.

AI-003: test_recursion_blob_decodes_and_verifies_on_host no longer ignored — panics if empty.elf missing

• Status: candidate
• Severity: low
• Location: prover/src/tests/recursion_smoke_test.rs:566
• Found by: moonmath:zro/minimax-m3
• Verified by: -
• Rejected by: -

Claim

The PR removed #[ignore = "needs prebuilt guest ELF (make compile-recursion-elfs)"] from this test, so it now runs by default. It panics on a missing executor/program_artifacts/recursion/empty.elf artifact (read_guest_elf at line 21-28 panics with "run make compile-recursion-elfs"). Anyone running cargo test -p lambda-vm-prover without first running make compile-recursion-elfs will hit a hard panic — not a clean test failure.

Evidence

Diff context shows the test was #[ignore]d before; the diff removes that attribute. The test calls prove_inner_and_encode_blob for empty.elf with MIN_PROOF_OPTIONS (a real STARK prove), so it isn't free — but the more pressing issue is that it now panics hard on missing artifacts where before it was just skipped.

Suggested fix

Either keep #[ignore] (with an updated reason that reflects the new requirement) or change read_guest_elf to return Result instead of panicking, so a missing artifact surfaces as a normal test failure rather than a process abort.

AI-004: test_recursion_rejects_corrupted_commitment panics if empty.elf artifact missing

• Status: candidate
• Severity: low
• Location: prover/src/tests/recursion_smoke_test.rs:611
• Found by: moonmath:zro/minimax-m3
• Verified by: -
• Rejected by: -

Claim

This new test (added by the PR) runs by default and calls read_guest_elf("empty"), which panics with "run make compile-recursion-elfs" if the artifact is absent. Same CI/dev-experience issue as the previous finding, but for a newly-added test where the previous behavior (the file didn't exist) means there was no prior signal that this artifact was needed.

Evidence

New test at line 611-635 added by the PR, no #[ignore] attribute, calls read_guest_elf(&root, "empty") at line 614 which panics on missing artifact.

Suggested fix

Either skip the test with a clear message when the artifact is missing (e.g., return early with eprintln! and return;), or add it to the existing ignored tier so it only runs in test-prover-all.

Reviewer Lanes

Lane	Model	Prompt	Status	Findings
glm	openrouter/z-ai/glm-5.2	general	error: opencode failed (provider/auth/runtime error) and no findings were submitted	0
kimi	openrouter/moonshotai/kimi-k2.7-code	general	error: opencode failed (provider/auth/runtime error) and no findings were submitted	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	error: opencode failed (provider/auth/runtime error) and no findings were submitted	0

Verification Lanes

Lane	Model	Status	Confirmed	Rejected	Uncertain
deepseek-verifier	openrouter/deepseek/deepseek-v4-pro	error: opencode failed (provider/auth/runtime error) and no verifications were submitted	0	0	0

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

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

[Oppen]

/ai-review

[github-actions]

Codex Code Review

Findings:

• High - recursion-blowup8.elf can be built from the min feature under make -j. Makefile uses .NOTPARALLEL: $(RECURSION_VERIFIER_ARTIFACTS), but that does not order those two sibling artifact targets under compile-recursion-elfs. Both recipes still build the same crate into the same CARGO_TARGET_DIR binary name, release/recursion-bench, then copy it to different artifact names. A parallel build can therefore copy the wrong feature build, including producing a supposedly blowup8 verifier that enforces the insecure min options. Add an explicit dependency/order between the two artifact targets or use distinct target dirs per preset.

• Bug - recursion-min guest does not compile with the current ProofOptions shape. main.rs constructs ProofOptions without fri_final_poly_log_degree, which is a required field in this checkout. make compile-recursion-elfs will fail for the --features min artifact.

• Bug - new PoC test module does not compile. recursion_soundness_gap_poc.rs has the same incomplete ProofOptions literal, and recursion_soundness_gap_poc.rs calls absorb_statement without the required fri_final_poly_log_degree argument.

I did not run builds or tests per the review constraints.

[claude]

Review — recursion: supply DECODE/page commitments via private input; bind via program_id fold

Reviewed the diff (VM verifier guest, program_id fold, verify_with_options doc/trust-model changes, Makefile presets, tests). Overall the change is coherent and the soundness reasoning holds up. No Critical/High issues found.

Soundness (confirmed OK). The design is sound under its stated trust model. verify_with_options intentionally does not bind the supplied roots to inner_elf, and the PoC test correctly demonstrates that. The program_id fold closes the gap: because the discriminating DECODE root is folded alongside elf_digest(inner_elf), a root substitution that verify accepts (decode_y != decode_x) yields forged_id != honest_id, so an external native recompute rejects it. The only way to make a forgery undetectable would require decode_y == decode_x AND matching folded page roots — i.e. identical decoded instructions and data pages, which is no meaningful substitution. Fold is sufficient.

Worth stating explicitly: this PR only makes the guest commit program_id; nothing here enforces the host-side recompute-and-compare. The tests build the expected value from the same honestly-precomputed roots fed to the guest, so they do not exercise the rejection path against a forged id — the committed program_id is only checked for self-consistency. That enforcement is (correctly) documented as out-of-scope; just flagging that the binding itself is unverified by the added tests.

Low.

• Stale test doc/assert wording (recursion_smoke_test.rs): the doc comment and assert message on run_recursion_pipeline_with_options describe the committed value as elf_digest || decode_commitment || page_commitments, but the guest commits program_id || output. Flagged inline.
• .NOTPARALLEL with prerequisites (Makefile): the target-specific form is only honored by GNU Make >= 4.4. On older Make the prerequisites are ignored and the entire Makefile becomes serial (slower, not incorrect). Fine if CI is on Make >= 4.4; noting the portability edge.

Nits (non-blocking).

• program_id folds pc_start in addition to elf_digest(elf_bytes), which already covers the entry point via the full ELF bytes — harmless redundancy.
• program_id_from_elf re-parses the ELF in-guest (verify already loaded it); one-time, not hot-path, acceptable.