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,16 @@ 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) — so it's built as two named artifacts
+# from the same crate dir, not via the generic %.elf pattern rule.
+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
@@ -148,7 +155,7 @@ compile-bench: prepare-sysroot $(BENCH_ARTIFACTS)
 # compiling until the tests are fast enough to run in CI.
 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 +174,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 +200,33 @@ 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)
+
+# Both presets build the same crate to the same CARGO_TARGET_DIR / same
+# release/recursion-bench, so the post-lock cp races under `make -j` (one
+# preset's cp reads the file while the other overwrites it). Serialize them.
+.NOTPARALLEL: $(RECURSION_VERIFIER_ARTIFACTS)
+
+# The recursion verifier's `min`/`blowup8` presets: same crate dir, same
+# built-binary filename, different Cargo feature -> different artifact name.
+# Not a pattern rule (the stem "recursion-min" wouldn't match the crate dir
+# "recursion") — see the comment on RECURSION_VERIFIER_PRESETS above.
+$(RECURSION_ARTIFACTS_DIR)/recursion-min.elf: FORCE | prepare-sysroot $(RECURSION_ARTIFACTS_DIR)
+	$(call build_guest_elf,$(RECURSION_GUESTS_DIR)/recursion,recursion-bench,--features min)
+
+$(RECURSION_ARTIFACTS_DIR)/recursion-blowup8.elf: FORCE | prepare-sysroot $(RECURSION_ARTIFACTS_DIR)
+	$(call build_guest_elf,$(RECURSION_GUESTS_DIR)/recursion,recursion-bench,--features blowup8)
 
 clean-asm:
 	-rm -rf $(ASM_ARTIFACTS_DIR)
@@ -261,12 +285,13 @@ 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

bench_vs/lambda/recursion/Cargo.toml

@@ -5,6 +5,12 @@ 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.
+min = []
+blowup8 = []
+
 [dependencies]
 lambda-vm-prover = { path = "../../../prover", default-features = false, features = [
     "profile-markers",

bench_vs/lambda/recursion/src/main.rs

@@ -1,44 +1,98 @@
 //! 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): `(VmProof, Vec<u8>, Commitment, Vec<(u64, Commitment)>)`
+//! — the inner program's ELF bytes plus its precomputed DECODE and
+//! ELF-data-page commitments, supplied instead of recomputed in-VM.
+//! `verify_with_options` does NOT bind the supplied roots to `inner_elf`; that
+//! binding is established by folding them into `program_id` (below) and having
+//! the host recompute that id and compare. That recompute is expensive, so it
+//! happens once at the top level in the host, never in the guest — see
+//! `program_id` in the prover's `statement` module.
 //!
-//! 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, 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_elf, decode_commitment,
+//! page_commitments) || inner_public_output` — the program identity (a fold
+//! pinning the ELF together with the roots it was verified against) plus the
+//! result the inner proof attested.
+//!
+//! 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};
+#[cfg(feature = "blowup8")]
+use lambda_vm_prover::GoldilocksCubicProofOptions;
+use lambda_vm_prover::{Commitment, ProofOptions, VmProof};
+
+#[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");
+
+/// Smallest possible proof options (blowup=2, 1 query). Intentionally
+/// insecure — for cheap diagnostics, not soundness.
+#[cfg(feature = "min")]
+fn recursion_proof_options() -> ProofOptions {
+    ProofOptions {
+        blowup_factor: 2,
+        fri_number_of_queries: 1,
+        coset_offset: 3,
+        grinding_factor: 1,
+        fri_final_poly_log_degree: 7,
+    }
+}
+
+/// 128-bit security (multi-query).
+#[cfg(feature = "blowup8")]
+fn recursion_proof_options() -> ProofOptions {
+    GoldilocksCubicProofOptions::with_blowup(8).expect("blowup=8 is always valid")
+}
 
 #[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) =
-        postcard::from_bytes(&blob).expect("failed to deserialize recursion input");
+    let (vm_proof, inner_elf, decode_commitment, page_commitments): (
+        VmProof,
+        Vec<u8>,
+        Commitment,
+        Vec<(u64, Commitment)>,
+    ) = 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");
+    let options = recursion_proof_options();
+    let ok = lambda_vm_prover::verify_with_options(
+        &vm_proof,
+        &inner_elf,
+        &options,
+        Some(decode_commitment),
+        Some(&page_commitments),
+    )
+    .expect("verify errored");
     assert!(ok, "inner proof failed verification");
 
-    lambda_vm_syscalls::syscalls::commit(&[1u8]);
+    // program_id is not self-enforcing: a consumer must recompute it natively
+    // and reject on mismatch. Commit the inner output alongside it.
+    let id = lambda_vm_prover::statement::program_id_from_elf(
+        &inner_elf,
+        &decode_commitment,
+        &page_commitments,
+    )
+    .expect("program_id");
+    let mut output = id.to_vec();
+    output.extend_from_slice(&vm_proof.public_output);
+    lambda_vm_syscalls::syscalls::commit(&output);
     lambda_vm_syscalls::syscalls::sys_halt();
 }

prover/src/lib.rs

@@ -20,7 +20,7 @@ mod debug_report;
 pub mod instruments;
 mod paged_mem;
 pub use stark::profile_markers;
-mod statement;
+pub mod statement;
 pub mod tables;
 pub mod test_utils;
 #[cfg(test)]
@@ -33,7 +33,6 @@ use crypto::fiat_shamir::is_transcript::IsTranscript;
 use executor::elf::Elf;
 use executor::vm::execution::Executor;
 use math::field::element::FieldElement;
-use stark::config::Commitment;
 use stark::prover::{IsStarkProver, Prover};
 #[cfg(feature = "disk-spill")]
 use stark::storage_mode::StorageMode;
@@ -61,6 +60,7 @@ use crate::test_utils::{
 
 // Re-exported so downstream verifier guests (e.g. the in-VM recursion guest) can
 // name the proof-options type carried in their private input alongside `VmProof`.
+pub use stark::config::Commitment;
 pub use stark::proof::options::{GoldilocksCubicProofOptions, ProofOptions};
 use stark::proof::stark::MultiProof;
 
@@ -417,36 +417,20 @@ impl VmAirs {
         refs
     }
 
-    /// Create all VM AIR instances. `minimal_bitwise` controls whether the full
-    /// 2^20 bitwise preprocessed table is included (false = full, true = minimal).
-    /// DECODE is always preprocessed.
+    /// Create all VM AIR instances. `minimal_bitwise` picks the minimal vs full
+    /// 2^20 bitwise preprocessed table. DECODE is always preprocessed.
+    /// `page_configs`/`table_counts` give the PAGE bases and split-table chunk
+    /// counts.
     ///
-    /// `page_configs` provides the page base addresses for creating PAGE AIRs.
-    /// `table_counts` specifies how many chunks for each split table.
+    /// `decode_commitment`/`page_commitments`, when `Some`, are used directly
+    /// (skipping the FFT + Merkle build) for the DECODE root and any matching
+    /// ELF-data page (keyed by `page_base`); `None` or unmatched pages recompute
+    /// from the ELF. Zero-init pages always use the shared compile-time constant.
     ///
-    /// `decode_commitment` is an optional precomputed DECODE preprocessed
-    /// commitment. When `Some`, the supplied value is used directly and the
-    /// FFT + Merkle build is skipped — useful for callers who have already
-    /// computed the commitment offline and embedded it as a compile-time
-    /// constant (e.g. the recursion guest, where the in-VM recompute is too
-    /// expensive). When `None`, the commitment is computed from the ELF.
-    ///
-    /// `page_commitments` is an optional list of precomputed ELF-data-page
-    /// preprocessed commitments, keyed by `page_base`. For each ELF data page
-    /// the verifier constructs, if a matching `(page_base, commitment)` pair
-    /// is supplied, it is used directly and that page's FFT + Merkle build is
-    /// skipped. Pages not in the list — including all zero-init pages and
-    /// pages without a match — take the normal compute path (zero-init pages
-    /// hit a compile-time constant via
-    /// `page::zero_init_preprocessed_commitment`; ELF data pages recompute
-    /// from the ELF). When `None`, every ELF data page recomputes from
-    /// scratch.
-    ///
-    /// The trust anchor for both `decode_commitment` and `page_commitments`
-    /// is the caller's compiled binary — never accept prover-supplied bytes
-    /// here. A wrong value is rejected, never silently accepted: it either
-    /// mismatches the prover's committed precomputed root (an explicit
-    /// verifier check) or yields diverging Fiat-Shamir challenges.
+    /// Supplied roots are used verbatim and NOT checked against `elf`. A wrong
+    /// caller-constant root is rejected (mismatches the proof root or diverges
+    /// Fiat-Shamir); a consistent prover-supplied mismatch is NOT — such
+    /// callers must bind identity externally (see `statement::program_id`).
     #[allow(clippy::too_many_arguments)]
     pub fn new(
         elf: &Elf,
@@ -1008,28 +992,19 @@ pub fn verify(vm_proof: &VmProof, elf_bytes: &[u8]) -> Result<bool, Error> {
 /// ignoring the options embedded in the proof bundle. This prevents a
 /// malicious prover from weakening the security level.
 ///
-/// `decode_commitment` is an optional precomputed DECODE preprocessed
-/// commitment. When `Some`, the supplied value is used directly and the
-/// in-verifier FFT + Merkle build for the DECODE preprocessed columns is
-/// skipped — useful for callers (e.g. the recursion guest) that embed the
-/// commitment as a compile-time constant to avoid the in-VM recompute
-/// cost. When `None`, the verifier computes the commitment from the ELF.
-///
-/// `page_commitments` is an optional list of precomputed ELF-data-page
-/// preprocessed commitments, keyed by `page_base`. For each ELF data page
-/// the verifier constructs, if a matching `(page_base, commitment)` pair is
-/// supplied, the FFT + Merkle build for that page is skipped. Pages without
-/// a match — including all zero-init pages — take the normal compute path
-/// (zero-init pages hit a compile-time constant via
-/// `page::zero_init_preprocessed_commitment`; ELF data pages recompute
-/// from the ELF). When `None`, every ELF data page recomputes from scratch.
+/// `decode_commitment`/`page_commitments`, when `Some`, are used directly
+/// (skipping the in-verifier FFT + Merkle build) for the DECODE root and any
+/// ELF-data page matching by `page_base`; `None` or unmatched pages recompute
+/// from the ELF, and zero-init pages always use the shared compile-time
+/// constant. Callers (e.g. the recursion guest) supply these to avoid the
+/// in-VM recompute cost.
 ///
-/// Trust model: both `decode_commitment` and `page_commitments`, when
-/// supplied, must come from the caller's compiled binary (e.g. a
-/// `const [u8; 32]` and a `const [(u64, [u8; 32])]`), never from prover-
-/// supplied bytes. A wrong value is rejected, never silently accepted: it
-/// either mismatches the prover's committed precomputed root (an explicit
-/// verifier check) or yields diverging Fiat-Shamir challenges.
+/// Trust model: a supplied root is used verbatim — this function does NOT
+/// check it against `elf_bytes`. If it is a caller constant (from the compiled
+/// binary), a wrong value is rejected (it mismatches the proof's precomputed
+/// root or diverges Fiat-Shamir). If it is prover-supplied (e.g. the recursion
+/// guest's private input), a consistent mismatched root is NOT rejected here;
+/// the caller must bind identity externally (see `statement::program_id`).
 pub fn verify_with_options(
     vm_proof: &VmProof,
     elf_bytes: &[u8],