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

.github/workflows/pr_main.yaml

@@ -330,6 +330,24 @@ jobs:
         run: |
           make compile-programs-rust
 
+      - name: Cache compiled recursion guest ELF artifacts
+        id: cache-recursion-elfs
+        uses: actions/cache@v4
+        with:
+          path: executor/program_artifacts/recursion
+          key: recursion-elf-artifacts-${{ hashFiles('bench_vs/lambda/**', 'prover/src/**', 'prover/Cargo.toml', 'crypto/**/src/**', 'crypto/**/Cargo.toml', 'executor/src/**', 'executor/Cargo.toml', 'syscalls/**', 'executor/programs/riscv64im-lambda-vm-elf.json', 'Makefile') }}
+          restore-keys: |
+            recursion-elf-artifacts-
+
+      - name: Setup Rust Environment (recursion ELFs)
+        if: steps.cache-recursion-elfs.outputs.cache-hit != 'true' && steps.cache-rust-elfs.outputs.cache-hit == 'true'
+        uses: ./.github/actions/setup-rust
+
+      - name: Compile recursion guest ELFs
+        if: steps.cache-recursion-elfs.outputs.cache-hit != 'true'
+        run: |
+          make compile-recursion-elfs
+
       - name: Install nextest
         uses: taiki-e/install-action@v2
         with:

Makefile

@@ -52,9 +52,18 @@ BENCH_ARTIFACTS := $(addprefix $(BENCH_ARTIFACTS_DIR)/, $(addsuffix .elf, $(BENC
 # rather than executor/programs/. The recursion guest is the in-VM STARK verifier.
 RECURSION_GUESTS_DIR=./bench_vs/lambda
 RECURSION_ARTIFACTS_DIR=./executor/program_artifacts/recursion
-RECURSION_GUESTS := empty fibonacci recursion
+RECURSION_GUESTS := empty fibonacci
 RECURSION_ARTIFACTS := $(addprefix $(RECURSION_ARTIFACTS_DIR)/, $(addsuffix .elf, $(RECURSION_GUESTS)))
 
+# The recursion verifier itself (bench_vs/lambda/recursion) requires picking
+# exactly one of its `min`/`blowup8` Cargo features at build time (fixes the
+# inner ProofOptions — see main.rs). Each preset builds its own distinctly
+# named [[bin]] (recursion-<preset>-bench) to its own artifact, via the
+# define/foreach/eval below rather than the generic %.elf pattern rule. The
+# distinct bin names also make the two `cp`s race-free under `make -j`.
+RECURSION_VERIFIER_PRESETS := min blowup8
+RECURSION_VERIFIER_ARTIFACTS := $(addprefix $(RECURSION_ARTIFACTS_DIR)/recursion-, $(addsuffix .elf, $(RECURSION_VERIFIER_PRESETS)))
+
 # Override with: make ... SYSROOT_DIR=$HOME/.lambda-vm-sysroot
 # to install the sysroot in a user-writable location and avoid sudo.
 SYSROOT_DIR ?= /opt/lambda-vm-sysroot
@@ -142,13 +151,13 @@ compile-programs-rust: prepare-sysroot $(RUST_ARTIFACTS)
 
 compile-bench: prepare-sysroot $(BENCH_ARTIFACTS)
 
-# NOTE: the recursion smoke tests are #[ignore]d (not run by `make test` /
-# `test-executor`) because they're too slow for CI today; only `test-prover-all`
-# runs them. We still compile their guest ELFs on every build so they keep
-# compiling until the tests are fast enough to run in CI.
+# NOTE: the recursion smoke tests read these prebuilt guest ELFs. The fast ones
+# run on every `cargo test` (so `make test`, which depends on this target, needs
+# them); the slow ones stay #[ignore]d (only `test-prover-all` runs them). We
+# compile the guest ELFs on every build so the tests always have them ready.
 compile-programs: compile-programs-asm compile-programs-rust compile-bench compile-recursion-elfs
 
-compile-recursion-elfs: prepare-sysroot $(RECURSION_ARTIFACTS)
+compile-recursion-elfs: prepare-sysroot $(RECURSION_ARTIFACTS) $(RECURSION_VERIFIER_ARTIFACTS)
 
 $(RECURSION_ARTIFACTS_DIR):
 	mkdir -p $@
@@ -167,21 +176,23 @@ $(BENCH_ARTIFACTS_DIR):
 FORCE:
 
 # The guest .elf rules all share one canned recipe: the cargo build invocation is
-# identical across the rust, bench, and recursion guests. They differ only in the
-# source directory ($(1)) and the built-binary name suffix ($(2): empty when the
-# binary == crate name, `-bench` for the recursion suite, whose crates are named
-# <name>-bench). cargo owns the dep graph (see FORCE above), so the recipe always
-# runs and lets cargo decide what to actually rebuild.
+# identical across the rust, bench, and recursion guests. They differ in the
+# crate directory ($(1), the full path — callers interpolate $* themselves, so
+# a target's stem needn't match its crate dir name, e.g. the recursion-verifier
+# presets below), the built binary's filename ($(2)), and optional extra cargo
+# args ($(3), e.g. `--features min`). cargo owns the dep graph (see FORCE
+# above), so the recipe always runs and lets cargo decide what to rebuild.
 define build_guest_elf
-cd $(1)/$* && \
+cd $(1) && \
 	CARGO_TARGET_DIR=$(abspath $(SHARED_TARGET_DIR)) \
 	CFLAGS_riscv64im_lambda_vm_elf="$(SYSROOT_CFLAGS)" \
 	rustup run nightly-2026-02-01 cargo build --release \
 		--target $(RV64_TARGET_SPEC) \
 		-Z build-std=core,alloc,std,compiler_builtins,panic_abort \
 		-Z build-std-features=compiler-builtins-mem \
-		-Z json-target-spec
-cp $(SHARED_TARGET_DIR)/riscv64im-lambda-vm-elf/release/$*$(2) $@
+		-Z json-target-spec \
+		$(3)
+cp $(SHARED_TARGET_DIR)/riscv64im-lambda-vm-elf/release/$(2) $@
 endef
 
 # Compile rust (64-bit)
@@ -191,18 +202,39 @@ endef
 # and fail to compile guest C dependencies). Order-only because prepare-sysroot is
 # .PHONY — a normal prereq would force a rebuild every time; its recipe is idempotent.
 $(RUST_ARTIFACTS_DIR)/%.elf: FORCE | prepare-sysroot $(RUST_ARTIFACTS_DIR)
-	$(call build_guest_elf,$(RUST_PROGRAMS_DIR),)
+	$(call build_guest_elf,$(RUST_PROGRAMS_DIR)/$*,$*)
 
 # Compile rust benches (64-bit)
 $(BENCH_ARTIFACTS_DIR)/%.elf: FORCE | prepare-sysroot $(BENCH_ARTIFACTS_DIR)
-	$(call build_guest_elf,$(BENCH_PROGRAMS_DIR),)
+	$(call build_guest_elf,$(BENCH_PROGRAMS_DIR)/$*,$*)
 
 # Recursion-suite guests (bench_vs/lambda/): the crate's binary is <name>-bench, so
 # copy <name>-bench -> <name>.elf. std-inclusive build-std covers both the no_std
 # inner guests and the std recursion verifier. Prover tests read these prebuilt
 # artifacts like every other program (see prover/src/tests/recursion_smoke_test.rs).
 $(RECURSION_ARTIFACTS_DIR)/%.elf: FORCE | prepare-sysroot $(RECURSION_ARTIFACTS_DIR)
-	$(call build_guest_elf,$(RECURSION_GUESTS_DIR),-bench)
+	$(call build_guest_elf,$(RECURSION_GUESTS_DIR)/$*,$*-bench)
+
+# The recursion verifier's `min`/`blowup8` presets: same crate dir, one
+# differently named [[bin]] per preset (recursion-<preset>-bench, gated on that
+# preset's Cargo feature) -> a differently named artifact. Generated per preset
+# from RECURSION_VERIFIER_PRESETS via define/foreach/eval rather than a pattern
+# rule (the stem "recursion-min" wouldn't match the crate dir "recursion") and
+# rather than copy-paste (the presets list is the single source of truth).
+# $(1) is the preset; the recipe uses $$ so `$$(call build_guest_elf,...)`
+# survives the $(call ...) expansion and is expanded at recipe-run time (where
+# $@ is defined). Because the two bins have distinct filenames the post-build
+# `cp`s read different files, so the `make -j` cp race is gone structurally and
+# no `.NOTPARALLEL` is needed: cargo's target-dir lock already serializes the
+# compiles, and `.NOTPARALLEL` with prerequisites was wrong on every make
+# version anyway (it serializes the whole build on GNU make <= 4.3 — macOS ships
+# 3.81, ubuntu-latest 4.3 — and on >= 4.4 serializes only the listed targets'
+# own prerequisites, never the two ELF targets against each other).
+define recursion_verifier_rule
+$(RECURSION_ARTIFACTS_DIR)/recursion-$(1).elf: FORCE | prepare-sysroot $(RECURSION_ARTIFACTS_DIR)
+	$$(call build_guest_elf,$$(RECURSION_GUESTS_DIR)/recursion,recursion-$(1)-bench,--features $(1))
+endef
+$(foreach preset,$(RECURSION_VERIFIER_PRESETS),$(eval $(call recursion_verifier_rule,$(preset))))
 
 clean-asm:
 	-rm -rf $(ASM_ARTIFACTS_DIR)
@@ -261,21 +293,25 @@ test: compile-programs
 
 # === Quick test shortcuts ===
 
-# Fast prover tests (skips ignored slow tests)
-test-fast:
+# Fast prover tests (skips ignored slow tests). Recursion smoke/PoC tests read
+# prebuilt guest ELFs, so build them first.
+test-fast: compile-recursion-elfs
 	cargo test -p lambda-vm-prover -p stark -p executor -F stark/parallel
 
 # Prover tests only
-test-prover:
+test-prover: compile-recursion-elfs
 	cargo test -p lambda-vm-prover
 
-# Prover tests including slow ones. The recursion smoke tests (#[ignore]d) read
-# prebuilt guest ELFs from executor/program_artifacts/recursion/, so build them first.
+# Prover tests including slow ones. The recursion smoke tests read prebuilt
+# guest ELFs from executor/program_artifacts/recursion/ — the fast ones on every
+# run, the slow ones (still #[ignore]d) only under --include-ignored — so build
+# them first.
 test-prover-all: compile-recursion-elfs
 	cargo test -p lambda-vm-prover -- --include-ignored
 
-# Prover tests with debug-checks (shows bus balance report)
-test-prover-debug:
+# Prover tests with debug-checks (shows bus balance report). Also unfiltered, so
+# it runs the non-ignored recursion tests that read prebuilt guest ELFs.
+test-prover-debug: compile-recursion-elfs
 	cargo test -p lambda-vm-prover --features debug-checks -- --nocapture
 
 # Disk-spill tests (stark + prover). FORCE_DISK_SPILL is required by the prover tests.
@@ -305,7 +341,9 @@ test-cuda-fallback:
 # GPU + nvcc). The GPU CI counterpart of CPU CI's sharded prover tests. Single-threaded: the
 # GPU serializes proves and the dispatch counters are process-global. cuda on prover cascades
 # to stark; crypto/ecsm build without it (they have no GPU path).
-test-prover-cuda:
+# compile-recursion-elfs: this unfiltered run executes the non-ignored recursion
+# smoke tests, which read prebuilt guest ELFs; scripts/gpu_test.sh otherwise never builds them.
+test-prover-cuda: compile-recursion-elfs
 	cargo test --release -p lambda-vm-prover -p stark -p crypto -p ecsm \
 	    --features lambda-vm-prover/cuda -- --test-threads=1
 

bench_vs/lambda/recursion/Cargo.toml

@@ -5,6 +5,30 @@ name = "recursion-bench"
 version = "0.1.0"
 edition = "2024"
 
+[features]
+# Exactly one selects the fixed ProofOptions (see main.rs) — hardcoded, not
+# private input, so a malicious input can't downgrade the security level.
+# Cargo features are additive by design, so the compile_error! mutual-exclusion
+# guard in main.rs is the loud failure that stops a mislabeled artifact if both
+# ever get enabled at once (e.g. under `--all-features`). The crate must stay a
+# standalone `[workspace]` (not a root-workspace member) so root-level feature
+# unification can never turn both on.
+min = []
+blowup8 = []
+
+# One distinctly named binary per preset (selected by its feature) so a parallel
+# `make -j` builds them to different filenames — structurally race-free, no cp
+# clobbering. Both use src/main.rs; required-features gates each to its preset.
+[[bin]]
+name = "recursion-min-bench"
+path = "src/main.rs"
+required-features = ["min"]
+
+[[bin]]
+name = "recursion-blowup8-bench"
+path = "src/main.rs"
+required-features = ["blowup8"]
+
 [dependencies]
 lambda-vm-prover = { path = "../../../prover", default-features = false, features = [
     "profile-markers",

bench_vs/lambda/recursion/src/main.rs

@@ -1,44 +1,69 @@
 //! Naive recursion guest: verifies an inner lambda-vm proof inside the VM.
 //!
-//! Private input layout (postcard-encoded):
-//!   `(VmProof, Vec<u8>, ProofOptions)`
-//! where the `Vec<u8>` holds the inner program's ELF bytes and `ProofOptions`
-//! specifies the parameters the inner prover used. Commits `[1]` on success.
+//! Private input (postcard): `lambda_vm_prover::recursion::GuestInput` — the
+//! inner proof, the inner program's ELF bytes, and its precomputed DECODE and
+//! ELF-data-page commitments, supplied instead of recomputed in-VM.
 //!
-//! Not `no_std` (std/alloc are available — `build-std` provides them, and the
-//! prover links as a normal std crate; its prove-side code is dead-code
-//! eliminated since we only call `verify`). Like every other allocating guest
-//! it is `#![no_main]` and uses the syscalls crate's global allocator (a large
-//! `TlsfHeap`), initialized first thing in `main` — `verify` allocates far more
-//! than the target's default heap provides.
+//! `ProofOptions` is fixed by the `min`/`blowup8` Cargo feature (a `Preset`),
+//! not private input — an attacker could otherwise pick trivially weak options
+//! and have the guest accept as if a real proof had been checked.
+//!
+//! On success commits `program_id || inner_public_output` via
+//! `recursion::verify_and_attest` (a single ELF parse and a single full-ELF
+//! Keccak, shared between the statement absorb and the `program_id` fold). The
+//! attestation is not self-enforcing: the binding is established by the
+//! consumer via `recursion::check_attestation` (a host-side recompute+compare),
+//! never in-guest.
+//!
+//! std (not `no_std`): `build-std` provides it, prove-side code is DCE'd.
+//! `#![no_main]`; inits the syscalls global allocator first thing in `main`.
 
 #![no_main]
 
-use lambda_vm_prover::{ProofOptions, VmProof};
+use lambda_vm_prover::recursion::{GuestInput, Preset};
+
+#[cfg(not(any(feature = "min", feature = "blowup8")))]
+compile_error!("select exactly one of the `min`/`blowup8` features");
+#[cfg(all(feature = "min", feature = "blowup8"))]
+compile_error!("select exactly one of the `min`/`blowup8` features");
+
+/// The build preset fixing the inner `ProofOptions` (see the module docs).
+#[cfg(feature = "min")]
+const PRESET: Preset = Preset::Min;
+#[cfg(feature = "blowup8")]
+const PRESET: Preset = Preset::Blowup8;
 
 #[unsafe(export_name = "main")]
 pub fn main() -> ! {
     lambda_vm_syscalls::allocator::init_allocator();
 
-    // Install panic handler to make sure any OOM is because verifying itself is
-    // expensive rather than panics causing stack unwinding, which itself is very
-    // expensive in the guest.
+    // Panic -> sys_panic; unwinding is very expensive in-guest.
     const PANIC_MSG: &str = "PANICKED";
     std::panic::set_hook(Box::new(|_| unsafe {
         lambda_vm_syscalls::syscalls::sys_panic(PANIC_MSG.as_ptr(), PANIC_MSG.len())
     }));
 
     let blob = lambda_vm_syscalls::syscalls::get_private_input();
-    let (vm_proof, inner_elf, options): (VmProof, Vec<u8>, ProofOptions) =
+    let (vm_proof, inner_elf, decode_commitment, page_commitments): GuestInput =
         postcard::from_bytes(&blob).expect("failed to deserialize recursion input");
     lambda_vm_prover::profile_markers::step_marker::<
         { lambda_vm_prover::profile_markers::STEP_DECODE_DONE },
     >();
 
-    let ok = lambda_vm_prover::verify_with_options(&vm_proof, &inner_elf, &options, None, None)
-        .expect("verify errored");
-    assert!(ok, "inner proof failed verification");
-
-    lambda_vm_syscalls::syscalls::commit(&[1u8]);
+    // The guest's whole job: verify the inner proof against the supplied roots
+    // and, on success, produce `program_id || inner_public_output`. The id fold
+    // is what the consumer rebinds to a trusted ELF (`check_attestation`); it is
+    // not self-enforcing here.
+    let options = PRESET.options();
+    let attestation = lambda_vm_prover::recursion::verify_and_attest(
+        &vm_proof,
+        &inner_elf,
+        &options,
+        decode_commitment,
+        &page_commitments,
+    )
+    .expect("verify errored")
+    .expect("inner proof failed verification");
+    lambda_vm_syscalls::syscalls::commit(&attestation);
     lambda_vm_syscalls::syscalls::sys_halt();
 }

prover/Cargo.toml

@@ -21,6 +21,9 @@ math = { path = "../crypto/math" }
 executor = { path = "../executor" }
 ecsm = { path = "../crypto/ecsm" }
 serde = { version = "1.0", features = ["derive"] }
+# The recursion guest-input blob codec (see `recursion::encode_guest_input`);
+# no_std+alloc, so the in-VM guest build (default-features = false) is fine.
+postcard = { version = "1.0", features = ["alloc"] }
 rayon = { version = "1.8.0", optional = true }
 sysinfo = { version = "0.31", default-features = false, features = ["system"] }
 log = "0.4"
@@ -30,7 +33,6 @@ sha3 = { version = "0.10.8", default-features = false }
 env_logger = "*"
 criterion = { version = "0.5", default-features = false }
 bincode = "1"
-postcard = { version = "1.0", features = ["alloc"] }
 tikv-jemallocator = "0.6"
 tikv-jemalloc-ctl = { version = "0.6", features = ["stats"] }
 tiny-keccak = { version = "2.0", features = ["keccak"] }