From fe26ffdbfc15c98b0104538c78404a734a697aeb Mon Sep 17 00:00:00 2001 From: Mario Rugiero Date: Mon, 6 Jul 2026 18:05:59 -0300 Subject: [PATCH 1/5] feat(recursion): pass DECODE/page commitments via private input, commit elf identity Replaces the build-time-embedded-target scheme (reverted in the prior three commits) with a uniform verifier: decode_commitment/page_commitments for the inner program are supplied via private input instead of recomputed in-VM (~45x fewer cycles), and ProofOptions is fixed per build (`min`/`blowup8` Cargo features) so a malicious private input can't downgrade security level. On success the guest commits elf_digest(inner_elf) || decode_commitment || page_commitments, attesting exactly what it verified without needing to recompute or re-embed the inner ELF at every recursion level. --- Makefile | 45 +++-- bench_vs/lambda/recursion/Cargo.toml | 8 + bench_vs/lambda/recursion/src/main.rs | 85 ++++++++- prover/src/lib.rs | 4 +- prover/src/statement.rs | 8 +- prover/src/tests/recursion_smoke_test.rs | 209 ++++++++++++++++++----- 6 files changed, 289 insertions(+), 70 deletions(-) diff --git a/Makefile b/Makefile index f22bf896b..6676d2d1d 100644 --- a/Makefile +++ b/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 -# -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,28 @@ 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 -bench, so # copy -bench -> .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, 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) diff --git a/bench_vs/lambda/recursion/Cargo.toml b/bench_vs/lambda/recursion/Cargo.toml index 60f4cb1cc..b70cfd405 100644 --- a/bench_vs/lambda/recursion/Cargo.toml +++ b/bench_vs/lambda/recursion/Cargo.toml @@ -5,6 +5,14 @@ name = "recursion-bench" version = "0.1.0" edition = "2024" +[features] +# Exactly one selects the fixed ProofOptions the inner proof was generated +# with (see main.rs) — hardcoded, not private input: otherwise a malicious +# private input could supply cheap/insecure options and the guest would +# accept + commit as if it had checked something at real security. +min = [] +blowup8 = [] + [dependencies] lambda-vm-prover = { path = "../../../prover", default-features = false, features = [ "profile-markers", diff --git a/bench_vs/lambda/recursion/src/main.rs b/bench_vs/lambda/recursion/src/main.rs index f19271aac..d857e2551 100644 --- a/bench_vs/lambda/recursion/src/main.rs +++ b/bench_vs/lambda/recursion/src/main.rs @@ -1,9 +1,32 @@ //! Naive recursion guest: verifies an inner lambda-vm proof inside the VM. //! //! Private input layout (postcard-encoded): -//! `(VmProof, Vec, ProofOptions)` -//! where the `Vec` holds the inner program's ELF bytes and `ProofOptions` -//! specifies the parameters the inner prover used. Commits `[1]` on success. +//! `(VmProof, Vec, Commitment, Vec<(u64, Commitment)>)` +//! where the `Vec` holds the inner program's ELF bytes, and the +//! `Commitment`/`Vec<(u64, Commitment)>` are the inner program's precomputed +//! DECODE and ELF-data-page commitments — supplied here instead of recomputed +//! in-VM (an ~45x cycle-count win: recomputing them via FFT+Merkle dominates +//! this guest's cost otherwise). They're untrusted, like every other private +//! input value: a wrong commitment diverges the inner proof's Fiat-Shamir +//! transcript, so `verify_with_options` returns `Ok(false)` rather than a +//! soundness gap. +//! +//! `ProofOptions` is deliberately NOT part of private input — it's fixed by +//! the `min`/`blowup8` Cargo feature this binary was built with (see +//! `recursion_proof_options` below). If it were attacker-supplied, a +//! malicious private input could pick trivially weak options (e.g. 1 FRI +//! query) and get the guest to accept + commit as if a real proof had been +//! checked, since the committed output can't otherwise convey what security +//! level was actually used. +//! +//! On success, commits `elf_digest(inner_elf) || decode_commitment || +//! page_commitments` — the full identity of what was verified. Just the two +//! precomputed commitments wouldn't be enough: they only cover segment +//! *content* (executable segments / ELF-backed data pages), not e.g. +//! `entry_point`, so two ELFs could share both without being the same +//! program. `elf_digest` is the exact function `absorb_statement` already +//! binds into the transcript, reused as-is rather than inventing a second +//! identity scheme. //! //! 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 @@ -14,7 +37,33 @@ #![no_main] -use lambda_vm_prover::{ProofOptions, VmProof}; +#[cfg(feature = "blowup8")] +use lambda_vm_prover::GoldilocksCubicProofOptions; +use lambda_vm_prover::statement::elf_digest; +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, + } +} + +/// 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() -> ! { @@ -29,16 +78,34 @@ pub fn main() -> ! { })); let blob = lambda_vm_syscalls::syscalls::get_private_input(); - let (vm_proof, inner_elf, options): (VmProof, Vec, ProofOptions) = - postcard::from_bytes(&blob).expect("failed to deserialize recursion input"); + let (vm_proof, inner_elf, decode_commitment, page_commitments): ( + VmProof, + Vec, + 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]); + let mut output = Vec::with_capacity(32 + decode_commitment.len() + page_commitments.len() * 40); + output.extend_from_slice(&elf_digest(&inner_elf)); + output.extend_from_slice(&decode_commitment); + for (page_base, commitment) in &page_commitments { + output.extend_from_slice(&page_base.to_le_bytes()); + output.extend_from_slice(commitment); + } + lambda_vm_syscalls::syscalls::commit(&output); lambda_vm_syscalls::syscalls::sys_halt(); } diff --git a/prover/src/lib.rs b/prover/src/lib.rs index 9c315faf1..a7a9ee0a4 100644 --- a/prover/src/lib.rs +++ b/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; diff --git a/prover/src/statement.rs b/prover/src/statement.rs index 87dab84cd..2257083ce 100644 --- a/prover/src/statement.rs +++ b/prover/src/statement.rs @@ -18,7 +18,13 @@ use crate::{RuntimePageRange, TableCounts}; /// Domain-separation tag. Bump the suffix (`_V2`, ...) on any encoding change. const DOMAIN_TAG: &[u8] = b"LAMBDAVM_STARK_STATEMENT_V3"; -fn elf_digest(elf: &[u8]) -> [u8; 32] { +/// Canonical full-ELF identity digest: exactly what [`absorb_statement`] binds +/// into the Fiat-Shamir transcript, so it's the complete, unambiguous "which +/// program" commitment (unlike `decode`/`page` table commitments, which only +/// cover segment *content* and say nothing about e.g. `entry_point`). Public so +/// the recursion guest can commit to it directly instead of inventing another +/// identity scheme. +pub fn elf_digest(elf: &[u8]) -> [u8; 32] { let mut h = Keccak256::new(); h.update(elf); h.finalize().into() diff --git a/prover/src/tests/recursion_smoke_test.rs b/prover/src/tests/recursion_smoke_test.rs index 6a100aaa9..530ed0139 100644 --- a/prover/src/tests/recursion_smoke_test.rs +++ b/prover/src/tests/recursion_smoke_test.rs @@ -1,11 +1,22 @@ //! End-to-end naive recursion pipeline smoke tests: prove an inner program, -//! hand `(VmProof, elf, opts)` to the in-VM verifier guest, then either prove -//! the guest's execution (`OuterMode::Prove`) or just execute it -//! (`OuterMode::ExecuteOnly`). Guest ELFs come from `make compile-recursion-elfs`. +//! hand `(VmProof, elf, decode_commitment, page_commitments)` to the in-VM +//! verifier guest, then either prove the guest's execution +//! (`OuterMode::Prove`) or just execute it (`OuterMode::ExecuteOnly`). Guest +//! ELFs come from `make compile-recursion-elfs`. //! -//! Every pipeline host-verifies the inner proof, so building with -//! `--features stark/instruments` makes any of these tests print the verifier's -//! per-step `Time spent:` timings. +//! `ProofOptions` is NOT part of private input — the guest is built once per +//! preset (`recursion-min.elf` / `recursion-blowup8.elf`, one Cargo feature +//! each), fixing the security level at build time (see +//! `bench_vs/lambda/recursion/src/main.rs`). `decode_commitment`/ +//! `page_commitments` ARE private input, precomputed here host-side via the +//! same functions the guest would otherwise call in-VM +//! (`precomputed_commitments`) — the guest passes them straight through as +//! `Some(..)` instead of recomputing (~45x fewer cycles). +//! +//! Every pipeline host-verifies the inner proof (independently, via full +//! recompute — `None, None` — not reusing our own precomputed values, so it's +//! a real ground-truth check), so building with `--features stark/instruments` +//! makes any of these tests print the verifier's per-step `Time spent:` timings. use std::ops::ControlFlow; use std::path::PathBuf; @@ -29,7 +40,8 @@ fn read_guest_elf(root: &std::path::Path, name: &str) -> Vec { } /// Smallest possible inner proof (blowup=2, 1 query). Intentionally insecure — -/// for the cheap diagnostics, not soundness. +/// for the cheap diagnostics, not soundness. Matches the `recursion-min.elf` +/// build's hardcoded `ProofOptions`. const MIN_PROOF_OPTIONS: stark::proof::options::ProofOptions = stark::proof::options::ProofOptions { blowup_factor: 2, @@ -39,14 +51,64 @@ const MIN_PROOF_OPTIONS: stark::proof::options::ProofOptions = fri_final_poly_log_degree: 7, }; -/// Prove `inner_elf` under `opts` and postcard-encode `(proof, elf, opts)` into -/// the guest's private-input blob. Returns the proof and the blob. +/// DECODE/ELF-data-page commitments for `elf_bytes` under `opts` — exactly +/// what `bench_vs/lambda/recursion`'s guest receives via private input instead +/// of recomputing in-VM. Reuses the same functions the (now-uniform) guest +/// would otherwise call itself. +fn precomputed_commitments( + elf_bytes: &[u8], + opts: &stark::proof::options::ProofOptions, +) -> (crate::Commitment, Vec<(u64, crate::Commitment)>) { + let elf = executor::elf::Elf::load(elf_bytes).expect("ELF load failed"); + let decode_commitment = crate::tables::decode::commitment_from_elf(&elf, opts) + .expect("decode commitment_from_elf failed"); + let page_commitments: Vec<(u64, crate::Commitment)> = + crate::tables::trace_builder::Traces::page_configs_from_elf(&elf) + .iter() + .filter(|c| c.init_values.is_some()) + .map(|c| { + ( + c.page_base, + crate::tables::page::compute_precomputed_commitment(c, opts), + ) + }) + .collect(); + (decode_commitment, page_commitments) +} + +/// The bytes the guest commits on success: `elf_digest(inner_elf) || +/// decode_commitment || page_commitments` (page entries as `page_base` LE u64 +/// followed by the 32-byte commitment) — must match `main.rs` byte-for-byte. +fn expected_committed_output( + inner_elf: &[u8], + decode_commitment: &crate::Commitment, + page_commitments: &[(u64, crate::Commitment)], +) -> Vec { + let mut out = Vec::with_capacity(32 + decode_commitment.len() + page_commitments.len() * 40); + out.extend_from_slice(&crate::statement::elf_digest(inner_elf)); + out.extend_from_slice(decode_commitment); + for (page_base, commitment) in page_commitments { + out.extend_from_slice(&page_base.to_le_bytes()); + out.extend_from_slice(commitment); + } + out +} + +/// Prove `inner_elf` under `opts`, precompute its DECODE/page commitments, and +/// postcard-encode `(proof, elf, decode_commitment, page_commitments)` into +/// the guest's private-input blob. Returns the proof, the blob, and the +/// commitments (so callers can build `expected_committed_output`). fn prove_inner_and_encode_blob( tag: &str, inner_elf: &[u8], inner_input: &[u8], opts: &stark::proof::options::ProofOptions, -) -> (crate::VmProof, Vec) { +) -> ( + crate::VmProof, + Vec, + crate::Commitment, + Vec<(u64, crate::Commitment)>, +) { eprintln!( "[{tag}] proving inner (blowup={}, fri_queries={}) ...", opts.blowup_factor, opts.fri_number_of_queries @@ -59,10 +121,17 @@ fn prove_inner_and_encode_blob( ) .expect("inner prove should succeed"); - let blob = - postcard::to_allocvec(&(&inner_proof, &inner_elf, opts)).expect("postcard encode failed"); + let (decode_commitment, page_commitments) = precomputed_commitments(inner_elf, opts); + + let blob = postcard::to_allocvec(&( + &inner_proof, + &inner_elf, + &decode_commitment, + &page_commitments, + )) + .expect("postcard encode failed"); eprintln!("[{tag}] postcard blob: {} bytes", blob.len()); - (inner_proof, blob) + (inner_proof, blob, decode_commitment, page_commitments) } /// Whether to also prove the guest's own execution after handing it the proof. @@ -162,10 +231,11 @@ fn drive_executor( } /// Shared preamble: build the blob (an `empty` inner proof under `opts`), load -/// `guest_name`, and stand up an executor. Returns `(elf_bytes, program, executor)`. +/// the `recursion-.elf` verifier, and stand up an executor. Returns +/// `(elf_bytes, program, executor)`. fn setup_guest_run( label: &str, - guest_name: &str, + preset: &str, opts: &stark::proof::options::ProofOptions, ) -> ( Vec, @@ -174,14 +244,15 @@ fn setup_guest_run( ) { let root = workspace_root(); let empty_elf_bytes = read_guest_elf(&root, "empty"); - let guest_elf_bytes = read_guest_elf(&root, guest_name); + let guest_elf_bytes = read_guest_elf(&root, &format!("recursion-{preset}")); - let (_inner_proof, blob) = prove_inner_and_encode_blob(label, &empty_elf_bytes, &[], opts); + let (_inner_proof, blob, _decode_commitment, _page_commitments) = + prove_inner_and_encode_blob(label, &empty_elf_bytes, &[], opts); let program = executor::elf::Elf::load(&guest_elf_bytes).expect("ELF load failed"); assert_ne!( program.entry_point, 0, - "{guest_name} ELF has entry_point=0 — build artifact is malformed" + "recursion-{preset} ELF has entry_point=0 — build artifact is malformed" ); let executor = executor::vm::execution::Executor::new(&program, blob).expect("Executor::new failed"); @@ -340,14 +411,14 @@ fn print_step_breakdown(buckets: &[u64; 7], total_cycles: u64) { /// lookup per cycle), and a rough trace/LDE estimate; with `detailed`, also /// the top-25 functions table (needs a `pc_hist` HashMap, so gated). fn run_profile( - guest_name: &str, + preset: &str, progress_stride: usize, opts: stark::proof::options::ProofOptions, detailed: bool, ) { use std::collections::HashMap; - let (guest_elf_bytes, program, mut executor) = setup_guest_run("profile", guest_name, &opts); + let (guest_elf_bytes, program, mut executor) = setup_guest_run("profile", preset, &opts); let symbols = executor::elf::SymbolTable::parse(&guest_elf_bytes); let instructions = executor::vm::execution::InstructionCache::new(&program.data) .expect("instruction cache build failed"); @@ -358,7 +429,7 @@ fn run_profile( let unique = std::cell::Cell::new(0usize); eprintln!( - "[profile] executing {guest_name} guest ({}) ...", + "[profile] executing recursion-{preset} guest ({}) ...", if detailed { "histogram + steps" } else { @@ -403,8 +474,8 @@ fn run_profile( eprintln!(); eprintln!("============================================================"); eprintln!( - " {} GUEST PROFILE (blowup={}, {} queries)", - guest_name.to_uppercase(), + " RECURSION-{} GUEST PROFILE (blowup={}, {} queries)", + preset.to_uppercase(), opts.blowup_factor, opts.fri_number_of_queries, ); @@ -433,19 +504,22 @@ fn run_profile( eprintln!("============================================================"); } -/// Core pipeline: prove the inner program, run the guest to `mode`, assert it -/// committed `[1]` (the in-VM verifier accepted the proof). +/// Core pipeline: prove the inner program, run the guest (`recursion-.elf`) +/// to `mode`, assert it committed `elf_digest(inner_elf) || decode_commitment || +/// page_commitments` (the in-VM verifier accepted the proof and attested what +/// it verified). fn run_recursion_pipeline_with_options( label: &str, inner_elf_bytes: &[u8], inner_private_input: &[u8], inner_proof_options: stark::proof::options::ProofOptions, + preset: &str, mode: OuterMode, ) { let root = workspace_root(); - let recursion_elf_bytes = read_guest_elf(&root, "recursion"); + let recursion_elf_bytes = read_guest_elf(&root, &format!("recursion-{preset}")); - let (inner_proof, blob) = prove_inner_and_encode_blob( + let (inner_proof, blob, decode_commitment, page_commitments) = prove_inner_and_encode_blob( label, inner_elf_bytes, inner_private_input, @@ -473,12 +547,13 @@ fn run_recursion_pipeline_with_options( OuterMode::Prove => prove_outer_and_commit(label, &recursion_elf_bytes, &blob), }; + let expected = + expected_committed_output(inner_elf_bytes, &decode_commitment, &page_commitments); assert_eq!( - committed, - vec![1u8], - "recursion guest must commit the [1] success marker (in-VM verify accepted)" + committed, expected, + "recursion guest must commit elf_digest||decode_commitment||page_commitments (in-VM verify accepted)" ); - eprintln!("[{label}] guest committed [1]: in-VM verify accepted ✓"); + eprintln!("[{label}] guest committed the expected commitments: in-VM verify accepted ✓"); } /// `run_recursion_pipeline_with_options` with `blowup=8` (the `empty`/`fibonacci` default). @@ -495,6 +570,7 @@ fn run_recursion_pipeline( inner_elf_bytes, inner_private_input, inner_proof_options, + "blowup8", mode, ); } @@ -506,23 +582,34 @@ fn run_recursion_pipeline( fn test_recursion_blob_decodes_and_verifies_on_host() { let root = workspace_root(); let empty_elf_bytes = read_guest_elf(&root, "empty"); - let (_inner, blob) = + let (_inner, blob, _decode_commitment, _page_commitments) = prove_inner_and_encode_blob("roundtrip", &empty_elf_bytes, &[], &MIN_PROOF_OPTIONS); - // Decode exactly as the guest does. - let decoded: Result<(crate::VmProof, Vec, crate::ProofOptions), _> = - postcard::from_bytes(&blob); - let (vm_proof, inner_elf, options) = match decoded { + // Decode exactly as the guest does (built with the `min` feature). + type DecodedBlob = ( + crate::VmProof, + Vec, + crate::Commitment, + Vec<(u64, crate::Commitment)>, + ); + let decoded: Result = postcard::from_bytes(&blob); + let (vm_proof, inner_elf, decode_commitment, page_commitments) = match decoded { Ok(t) => t, Err(e) => panic!("[roundtrip] postcard DECODE failed (this is the guest panic): {e}"), }; eprintln!( - "[roundtrip] decode ok: elf {} bytes, blowup {}", + "[roundtrip] decode ok: elf {} bytes, {} page commitments", inner_elf.len(), - options.blowup_factor + page_commitments.len(), ); - match crate::verify_with_options(&vm_proof, &inner_elf, &options, None, None) { + match crate::verify_with_options( + &vm_proof, + &inner_elf, + &MIN_PROOF_OPTIONS, + Some(decode_commitment), + Some(&page_commitments), + ) { Ok(true) => eprintln!("[roundtrip] verify ok=true — guest path is sound"), Ok(false) => panic!( "[roundtrip] verify returned FALSE (guest hits assert!(ok)) — proof did not survive the postcard round-trip" @@ -531,6 +618,36 @@ fn test_recursion_blob_decodes_and_verifies_on_host() { } } +/// Corrupting a private-input commitment must make verification fail +/// (`Ok(false)`), never a soundness gap — the safety property the whole +/// private-input-supplied-commitment design rests on. +#[test] +#[ignore = "needs prebuilt guest ELF (make compile-recursion-elfs)"] +fn test_recursion_rejects_corrupted_commitment() { + let root = workspace_root(); + let empty_elf_bytes = read_guest_elf(&root, "empty"); + let (vm_proof, _blob, mut decode_commitment, page_commitments) = prove_inner_and_encode_blob( + "corrupt-commitment", + &empty_elf_bytes, + &[], + &MIN_PROOF_OPTIONS, + ); + decode_commitment[0] ^= 0xFF; + + let ok = crate::verify_with_options( + &vm_proof, + &empty_elf_bytes, + &MIN_PROOF_OPTIONS, + Some(decode_commitment), + Some(&page_commitments), + ) + .expect("verify errored"); + assert!( + !ok, + "corrupted decode_commitment must be rejected, not silently accepted" + ); +} + // === Execute-only tier ======================================================== /// Execute-only: verify a `blowup=8` proof of the empty program in-VM. @@ -558,6 +675,7 @@ fn test_recursion_execute_1query() { &empty_elf_bytes, &[], MIN_PROOF_OPTIONS, + "min", OuterMode::ExecuteOnly, ); } @@ -578,7 +696,7 @@ fn test_recursion_execute_1query() { #[ignore = "slow: runs the in-VM STARK verifier (minutes on CI)"] fn test_recursion_step_markers_observed_in_order() { let (_bytes, program, mut executor) = - setup_guest_run("step-markers", "recursion", &MIN_PROOF_OPTIONS); + setup_guest_run("step-markers", "min", &MIN_PROOF_OPTIONS); let instructions = executor::vm::execution::InstructionCache::new(&program.data) .expect("instruction cache build failed"); @@ -670,6 +788,7 @@ fn test_recursion_prove_1query() { &empty_elf_bytes, &[], MIN_PROOF_OPTIONS, + "min", OuterMode::Prove, ); } @@ -682,7 +801,7 @@ fn test_dump_recursion_input() { let root = workspace_root(); let empty_elf_bytes = read_guest_elf(&root, "empty"); - let (_inner_proof, blob) = + let (_inner_proof, blob, _decode_commitment, _page_commitments) = prove_inner_and_encode_blob("dump-input", &empty_elf_bytes, &[], &MIN_PROOF_OPTIONS); let path = "/tmp/recursion_input.bin"; @@ -694,28 +813,28 @@ fn test_dump_recursion_input() { #[test] #[ignore = "diagnostic: fast; recursion guest cycle count (1 query)"] fn test_recursion_cycles_1query() { - run_profile("recursion", 500, MIN_PROOF_OPTIONS, false); + run_profile("min", 500, MIN_PROOF_OPTIONS, false); } /// Cycle count only at 128-bit security: more FRI queries → more verifier cycles. #[test] #[ignore = "diagnostic: fast; recursion guest cycle count (multi-query)"] fn test_recursion_cycles_multiquery() { - run_profile("recursion", 500, blowup8(), false); + run_profile("blowup8", 500, blowup8(), false); } /// Full profile (top-25 + per-step) of the 1-query run. #[test] #[ignore = "diagnostic: ~8 min; recursion guest histogram + steps (1 query)"] fn test_recursion_profile_1query() { - run_profile("recursion", 500, MIN_PROOF_OPTIONS, true); + run_profile("min", 500, MIN_PROOF_OPTIONS, true); } /// Full profile at 128-bit security: weight shifts toward per-query FRI/Merkle. #[test] #[ignore = "diagnostic: heavy; recursion guest histogram + steps (multi-query)"] fn test_recursion_profile_multiquery() { - run_profile("recursion", 500, blowup8(), true); + run_profile("blowup8", 500, blowup8(), true); } /// Inner program: fibonacci(10). From acf996e50652accbf4dbe545cf857e5c317e09cc Mon Sep 17 00:00:00 2001 From: Mario Rugiero Date: Tue, 7 Jul 2026 16:36:32 -0300 Subject: [PATCH 2/5] fix(recursion): bind supplied DECODE/page roots to inner ELF via program_id MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The verifier guest supplies DECODE/page preprocessed roots via private input and previously committed a bare elf_digest, which a custom prover could decouple from the constrained program (a proof of Y committed as X — see the new recursion_soundness_gap_poc). Commit program_id(inner_elf, decode, pages) || inner_public_output instead: folding the roots into the committed identity makes a supplied-root substitution diverge from an honest native recompute, which the top-level host checks. verify_with_options itself does not bind the supplied roots to the ELF; that binding is external and its docstring (and VmAirs::new's) is corrected to say so instead of overstating root validation. Also: commit the inner proof's public_output so the attestation covers the result, not just identity; serialize the recursion-elf presets (.NOTPARALLEL) to avoid the parallel-build clobber; build recursion ELFs in test-fast/ test-prover and un-ignore the artifact-gated recursion tests. --- Makefile | 12 +- bench_vs/lambda/recursion/Cargo.toml | 6 +- bench_vs/lambda/recursion/src/main.rs | 70 ++--- prover/src/lib.rs | 73 ++--- prover/src/statement.rs | 55 +++- prover/src/tests/mod.rs | 2 + prover/src/tests/recursion_smoke_test.rs | 74 ++--- .../src/tests/recursion_soundness_gap_poc.rs | 277 ++++++++++++++++++ 8 files changed, 420 insertions(+), 149 deletions(-) create mode 100644 prover/src/tests/recursion_soundness_gap_poc.rs diff --git a/Makefile b/Makefile index 6676d2d1d..389d98420 100644 --- a/Makefile +++ b/Makefile @@ -213,6 +213,11 @@ $(BENCH_ARTIFACTS_DIR)/%.elf: FORCE | prepare-sysroot $(BENCH_ARTIFACTS_DIR) $(RECURSION_ARTIFACTS_DIR)/%.elf: FORCE | prepare-sysroot $(RECURSION_ARTIFACTS_DIR) $(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 @@ -280,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 diff --git a/bench_vs/lambda/recursion/Cargo.toml b/bench_vs/lambda/recursion/Cargo.toml index b70cfd405..fdffdb27d 100644 --- a/bench_vs/lambda/recursion/Cargo.toml +++ b/bench_vs/lambda/recursion/Cargo.toml @@ -6,10 +6,8 @@ version = "0.1.0" edition = "2024" [features] -# Exactly one selects the fixed ProofOptions the inner proof was generated -# with (see main.rs) — hardcoded, not private input: otherwise a malicious -# private input could supply cheap/insecure options and the guest would -# accept + commit as if it had checked something at real security. +# 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 = [] diff --git a/bench_vs/lambda/recursion/src/main.rs b/bench_vs/lambda/recursion/src/main.rs index d857e2551..30c37b9f8 100644 --- a/bench_vs/lambda/recursion/src/main.rs +++ b/bench_vs/lambda/recursion/src/main.rs @@ -1,45 +1,30 @@ //! Naive recursion guest: verifies an inner lambda-vm proof inside the VM. //! -//! Private input layout (postcard-encoded): -//! `(VmProof, Vec, Commitment, Vec<(u64, Commitment)>)` -//! where the `Vec` holds the inner program's ELF bytes, and the -//! `Commitment`/`Vec<(u64, Commitment)>` are the inner program's precomputed -//! DECODE and ELF-data-page commitments — supplied here instead of recomputed -//! in-VM (an ~45x cycle-count win: recomputing them via FFT+Merkle dominates -//! this guest's cost otherwise). They're untrusted, like every other private -//! input value: a wrong commitment diverges the inner proof's Fiat-Shamir -//! transcript, so `verify_with_options` returns `Ok(false)` rather than a -//! soundness gap. +//! Private input (postcard): `(VmProof, Vec, 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. //! -//! `ProofOptions` is deliberately NOT part of private input — it's fixed by -//! the `min`/`blowup8` Cargo feature this binary was built with (see -//! `recursion_proof_options` below). If it were attacker-supplied, a -//! malicious private input could pick trivially weak options (e.g. 1 FRI -//! query) and get the guest to accept + commit as if a real proof had been -//! checked, since the committed output can't otherwise convey what security -//! level was actually used. +//! `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 `elf_digest(inner_elf) || decode_commitment || -//! page_commitments` — the full identity of what was verified. Just the two -//! precomputed commitments wouldn't be enough: they only cover segment -//! *content* (executable segments / ELF-backed data pages), not e.g. -//! `entry_point`, so two ELFs could share both without being the same -//! program. `elf_digest` is the exact function `absorb_statement` already -//! binds into the transcript, reused as-is rather than inventing a second -//! identity scheme. +//! 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. //! -//! 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. +//! 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] #[cfg(feature = "blowup8")] use lambda_vm_prover::GoldilocksCubicProofOptions; -use lambda_vm_prover::statement::elf_digest; use lambda_vm_prover::{Commitment, ProofOptions, VmProof}; #[cfg(not(any(feature = "min", feature = "blowup8")))] @@ -69,9 +54,7 @@ fn recursion_proof_options() -> ProofOptions { 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()) @@ -99,13 +82,16 @@ pub fn main() -> ! { .expect("verify errored"); assert!(ok, "inner proof failed verification"); - let mut output = Vec::with_capacity(32 + decode_commitment.len() + page_commitments.len() * 40); - output.extend_from_slice(&elf_digest(&inner_elf)); - output.extend_from_slice(&decode_commitment); - for (page_base, commitment) in &page_commitments { - output.extend_from_slice(&page_base.to_le_bytes()); - output.extend_from_slice(commitment); - } + // 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(); } diff --git a/prover/src/lib.rs b/prover/src/lib.rs index a7a9ee0a4..6098413b1 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -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 { /// 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], diff --git a/prover/src/statement.rs b/prover/src/statement.rs index 2257083ce..9f786da3a 100644 --- a/prover/src/statement.rs +++ b/prover/src/statement.rs @@ -10,26 +10,67 @@ //! every derived challenge differ and verification reject. use crypto::fiat_shamir::is_transcript::IsTranscript; +use executor::elf::Elf; use sha3::{Digest, Keccak256}; use crate::test_utils::E; -use crate::{RuntimePageRange, TableCounts}; +use crate::{Commitment, RuntimePageRange, TableCounts}; /// Domain-separation tag. Bump the suffix (`_V2`, ...) on any encoding change. const DOMAIN_TAG: &[u8] = b"LAMBDAVM_STARK_STATEMENT_V3"; -/// Canonical full-ELF identity digest: exactly what [`absorb_statement`] binds -/// into the Fiat-Shamir transcript, so it's the complete, unambiguous "which -/// program" commitment (unlike `decode`/`page` table commitments, which only -/// cover segment *content* and say nothing about e.g. `entry_point`). Public so -/// the recursion guest can commit to it directly instead of inventing another -/// identity scheme. +/// Canonical full-ELF identity digest — exactly what [`absorb_statement`] binds +/// into the transcript. Public so the recursion guest can commit to it directly. pub fn elf_digest(elf: &[u8]) -> [u8; 32] { let mut h = Keccak256::new(); h.update(elf); h.finalize().into() } +/// Domain tag for [`program_id`]. +const PROGRAM_ID_TAG: &[u8] = b"LAMBDAVM_PROGRAM_ID_V1"; + +/// Canonical program identity: a fold of the full ELF digest, entry point, and +/// the supplied DECODE / ELF-data-page roots (folded in ascending `page_base` +/// order). Folding the roots in makes a supplied-root substitution yield a +/// different id than an honest native recompute — the binding is that compare. +pub fn program_id( + elf_bytes: &[u8], + pc_start: u64, + decode_commitment: &Commitment, + page_commitments: &[(u64, Commitment)], +) -> [u8; 32] { + let mut pages = page_commitments.to_vec(); + pages.sort_by_key(|(base, _)| *base); + + let mut h = Keccak256::new(); + h.update(PROGRAM_ID_TAG); + h.update(elf_digest(elf_bytes)); + h.update(pc_start.to_le_bytes()); + h.update(decode_commitment); + h.update((pages.len() as u64).to_le_bytes()); + for (base, c) in &pages { + h.update(base.to_le_bytes()); + h.update(c); + } + h.finalize().into() +} + +/// [`program_id`] with `pc_start` taken from `elf_bytes`' entry point. +pub fn program_id_from_elf( + elf_bytes: &[u8], + decode_commitment: &Commitment, + page_commitments: &[(u64, Commitment)], +) -> Result<[u8; 32], crate::Error> { + let elf = Elf::load(elf_bytes).map_err(|e| crate::Error::ElfLoad(format!("{e}")))?; + Ok(program_id( + elf_bytes, + elf.entry_point, + decode_commitment, + page_commitments, + )) +} + /// Which statement is being bound. Selects the leading domain tag and whether an /// epoch label is appended, so monolithic and continuation-epoch proofs share one /// function while each starts with its own tag. `Monolithic` reproduces the diff --git a/prover/src/tests/mod.rs b/prover/src/tests/mod.rs index 2c06d7fcf..e20d9b411 100644 --- a/prover/src/tests/mod.rs +++ b/prover/src/tests/mod.rs @@ -71,6 +71,8 @@ pub mod prove_elfs_tests; #[cfg(test)] pub mod recursion_smoke_test; #[cfg(test)] +pub mod recursion_soundness_gap_poc; +#[cfg(test)] pub mod register_tests; #[cfg(test)] pub mod shift_tests; diff --git a/prover/src/tests/recursion_smoke_test.rs b/prover/src/tests/recursion_smoke_test.rs index 530ed0139..602957093 100644 --- a/prover/src/tests/recursion_smoke_test.rs +++ b/prover/src/tests/recursion_smoke_test.rs @@ -1,22 +1,10 @@ //! End-to-end naive recursion pipeline smoke tests: prove an inner program, //! hand `(VmProof, elf, decode_commitment, page_commitments)` to the in-VM -//! verifier guest, then either prove the guest's execution -//! (`OuterMode::Prove`) or just execute it (`OuterMode::ExecuteOnly`). Guest -//! ELFs come from `make compile-recursion-elfs`. -//! -//! `ProofOptions` is NOT part of private input — the guest is built once per -//! preset (`recursion-min.elf` / `recursion-blowup8.elf`, one Cargo feature -//! each), fixing the security level at build time (see -//! `bench_vs/lambda/recursion/src/main.rs`). `decode_commitment`/ -//! `page_commitments` ARE private input, precomputed here host-side via the -//! same functions the guest would otherwise call in-VM -//! (`precomputed_commitments`) — the guest passes them straight through as -//! `Some(..)` instead of recomputing (~45x fewer cycles). -//! -//! Every pipeline host-verifies the inner proof (independently, via full -//! recompute — `None, None` — not reusing our own precomputed values, so it's -//! a real ground-truth check), so building with `--features stark/instruments` -//! makes any of these tests print the verifier's per-step `Time spent:` timings. +//! verifier guest, then execute or prove the guest. Guest ELFs come from +//! `make compile-recursion-elfs`. `ProofOptions` is fixed per preset at build +//! time; `decode_commitment`/`page_commitments` are private input, precomputed +//! host-side. Each pipeline also host-verifies the inner proof via full +//! recompute (`None, None`) as a ground-truth check. use std::ops::ControlFlow; use std::path::PathBuf; @@ -51,10 +39,8 @@ const MIN_PROOF_OPTIONS: stark::proof::options::ProofOptions = fri_final_poly_log_degree: 7, }; -/// DECODE/ELF-data-page commitments for `elf_bytes` under `opts` — exactly -/// what `bench_vs/lambda/recursion`'s guest receives via private input instead -/// of recomputing in-VM. Reuses the same functions the (now-uniform) guest -/// would otherwise call itself. +/// DECODE/ELF-data-page commitments for `elf_bytes` under `opts` — what the +/// guest receives via private input instead of recomputing in-VM. fn precomputed_commitments( elf_bytes: &[u8], opts: &stark::proof::options::ProofOptions, @@ -76,21 +62,20 @@ fn precomputed_commitments( (decode_commitment, page_commitments) } -/// The bytes the guest commits on success: `elf_digest(inner_elf) || -/// decode_commitment || page_commitments` (page entries as `page_base` LE u64 -/// followed by the 32-byte commitment) — must match `main.rs` byte-for-byte. +/// The bytes the guest commits on success: `program_id(inner_elf, +/// decode_commitment, page_commitments) || inner_public_output` — must match +/// `main.rs` byte-for-byte. fn expected_committed_output( inner_elf: &[u8], decode_commitment: &crate::Commitment, page_commitments: &[(u64, crate::Commitment)], + inner_public_output: &[u8], ) -> Vec { - let mut out = Vec::with_capacity(32 + decode_commitment.len() + page_commitments.len() * 40); - out.extend_from_slice(&crate::statement::elf_digest(inner_elf)); - out.extend_from_slice(decode_commitment); - for (page_base, commitment) in page_commitments { - out.extend_from_slice(&page_base.to_le_bytes()); - out.extend_from_slice(commitment); - } + let mut out = + crate::statement::program_id_from_elf(inner_elf, decode_commitment, page_commitments) + .expect("program_id") + .to_vec(); + out.extend_from_slice(inner_public_output); out } @@ -303,12 +288,9 @@ fn step_tag(bucket: u8) -> &'static str { } } -/// Print one top-25 table: `rows` is `(name, cycles, distinct_pcs)`, already -/// unsorted; `denom_cycles` is the denominator for percentages — the global -/// total for the all-steps table, but *that step's own total* for a per-step -/// table, so `%`/`cum %` show what dominates within that step (a `keccak` -/// that's 90% of a cheap step should read as 90%, not as a fraction of a -/// percent of the whole run). +/// Print one top-25 table. `rows` is `(name, cycles, distinct_pcs)`; +/// `denom_cycles` is the percentage denominator (global total for the all-steps +/// table, that step's own total for a per-step table). fn print_top25_table(rows: &mut [(String, u64, u64)], denom_cycles: u64) { rows.sort_unstable_by_key(|(_name, cycles, _pcs)| std::cmp::Reverse(*cycles)); let pct = |n: u64| 100.0 * (n as f64) / (denom_cycles as f64); @@ -547,8 +529,12 @@ fn run_recursion_pipeline_with_options( OuterMode::Prove => prove_outer_and_commit(label, &recursion_elf_bytes, &blob), }; - let expected = - expected_committed_output(inner_elf_bytes, &decode_commitment, &page_commitments); + let expected = expected_committed_output( + inner_elf_bytes, + &decode_commitment, + &page_commitments, + &inner_proof.public_output, + ); assert_eq!( committed, expected, "recursion guest must commit elf_digest||decode_commitment||page_commitments (in-VM verify accepted)" @@ -578,7 +564,6 @@ fn run_recursion_pipeline( /// Decode the blob on the host and verify — a cheap guard on the encode/decode /// contract without running the VM. #[test] -#[ignore = "needs prebuilt guest ELF (make compile-recursion-elfs)"] fn test_recursion_blob_decodes_and_verifies_on_host() { let root = workspace_root(); let empty_elf_bytes = read_guest_elf(&root, "empty"); @@ -618,11 +603,12 @@ fn test_recursion_blob_decodes_and_verifies_on_host() { } } -/// Corrupting a private-input commitment must make verification fail -/// (`Ok(false)`), never a soundness gap — the safety property the whole -/// private-input-supplied-commitment design rests on. +/// Corrupting a private-input commitment on an *honest* proof makes +/// verification fail (`Ok(false)`). Necessary but not sufficient alone — a +/// custom prover can supply consistent mismatched roots (see +/// `recursion_soundness_gap_poc`); the identity binding is the `program_id` +/// fold, not this check. #[test] -#[ignore = "needs prebuilt guest ELF (make compile-recursion-elfs)"] fn test_recursion_rejects_corrupted_commitment() { let root = workspace_root(); let empty_elf_bytes = read_guest_elf(&root, "empty"); diff --git a/prover/src/tests/recursion_soundness_gap_poc.rs b/prover/src/tests/recursion_soundness_gap_poc.rs new file mode 100644 index 000000000..a48fec520 --- /dev/null +++ b/prover/src/tests/recursion_soundness_gap_poc.rs @@ -0,0 +1,277 @@ +//! `verify_with_options(.., Some(decode), Some(pages))` does NOT bind the +//! supplied roots to `inner_elf`: a custom prover can absorb `elf_digest(X)` +//! into the Fiat-Shamir statement while the constrained instructions and every +//! preprocessed root are those of a DIFFERENT program Y, and verification with +//! `inner_elf = X` and Y's roots still returns `Ok(true)` (the "critical +//! soundness check" in `crypto/stark/src/verifier.rs` compares two +//! prover-controlled values here, so it is vacuous against a custom prover). +//! +//! The recursion guest does not rely on verify for that binding: it commits +//! `program_id(inner_elf, decode, pages)`, which folds the supplied roots into +//! the identity — so the same substitution yields an id that differs from the +//! honest `program_id(X)`, detectable by whoever recomputes it natively and +//! compares. These tests pin both facts: verify accepts, and the fold catches. + +use std::collections::HashSet; +use std::path::PathBuf; + +use crypto::fiat_shamir::default_transcript::DefaultTranscript; +use stark::prover::{IsStarkProver, Prover}; + +use crate::statement::{StatementKind, absorb_statement, elf_digest}; +use crate::tables::trace_builder::Traces; +use crate::test_utils::E; +use crate::{Commitment, MaxRowsConfig, VmAirs, VmProof}; + +use executor::elf::Elf; +use executor::vm::execution::Executor; + +/// Smallest inner proof (blowup=2, 1 query) — for speed; soundness of the +/// *scheme* is what's under test, not the FRI security level. +const MIN_PROOF_OPTIONS: stark::proof::options::ProofOptions = + stark::proof::options::ProofOptions { + blowup_factor: 2, + fri_number_of_queries: 1, + coset_offset: 3, + grinding_factor: 1, + }; + +fn workspace_root() -> PathBuf { + PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .parent() + .expect("workspace root") + .to_path_buf() +} + +fn read_guest_elf(name: &str) -> Vec { + let path = workspace_root().join(format!("executor/program_artifacts/recursion/{name}.elf")); + std::fs::read(&path).unwrap_or_else(|e| { + panic!( + "failed to read {} — run `make compile-recursion-elfs`: {e}", + path.display() + ) + }) +} + +/// Precomputed DECODE + ELF-data-page commitments for `elf_bytes` under `opts` +/// — exactly what the recursion guest receives as private input. +fn precomputed_commitments( + elf_bytes: &[u8], + opts: &stark::proof::options::ProofOptions, +) -> (Commitment, Vec<(u64, Commitment)>) { + let elf = Elf::load(elf_bytes).expect("ELF load failed"); + let decode_commitment = + crate::tables::decode::commitment_from_elf(&elf, opts).expect("decode commitment failed"); + let page_commitments: Vec<(u64, Commitment)> = Traces::page_configs_from_elf(&elf) + .iter() + .filter(|c| c.init_values.is_some()) + .map(|c| { + ( + c.page_base, + crate::tables::page::compute_precomputed_commitment(c, opts), + ) + }) + .collect(); + (decode_commitment, page_commitments) +} + +/// The set of program-counter values fetched during a run of `elf_bytes`. +fn executed_pcs(elf_bytes: &[u8]) -> HashSet { + let elf = Elf::load(elf_bytes).expect("ELF load failed"); + let executor = Executor::new(&elf, vec![]).expect("executor new"); + let result = executor.run().expect("run failed"); + result.logs.iter().map(|l| l.current_pc).collect() +} + +/// Read a 4-byte word (LE) from an executable ELF segment at virtual address +/// `vaddr`, returning its raw-file byte offset and current value. Parses the +/// program headers directly so we can patch the raw bytes (and thus the +/// `elf_digest`) at exactly the right place. +fn exec_words(elf_bytes: &[u8]) -> Vec<(usize, u64, u32)> { + let rd_u16 = |o: usize| u16::from_le_bytes(elf_bytes[o..o + 2].try_into().unwrap()); + let rd_u32 = |o: usize| u32::from_le_bytes(elf_bytes[o..o + 4].try_into().unwrap()); + let rd_u64 = |o: usize| u64::from_le_bytes(elf_bytes[o..o + 8].try_into().unwrap()); + + let e_phoff = rd_u64(32) as usize; + let e_phentsize = rd_u16(54) as usize; + let e_phnum = rd_u16(56) as usize; + + const PT_LOAD: u32 = 1; + const PF_X: u32 = 1; + + let mut out = Vec::new(); + for i in 0..e_phnum { + let ph = e_phoff + i * e_phentsize; + let p_type = rd_u32(ph); + let p_flags = rd_u32(ph + 4); + if p_type != PT_LOAD || (p_flags & PF_X) == 0 { + continue; + } + let p_offset = rd_u64(ph + 8) as usize; + let p_vaddr = rd_u64(ph + 16); + let p_filesz = rd_u64(ph + 32) as usize; + let mut off = 0usize; + while off + 4 <= p_filesz { + let file_off = p_offset + off; + let vaddr = p_vaddr + off as u64; + out.push((file_off, vaddr, rd_u32(file_off))); + off += 4; + } + } + out +} + +/// Build program Y from program X (`= empty.elf`) by patching a single +/// executable-segment word at a PC that X never fetches, to a *different* +/// still-parseable instruction. Because the word is never fetched, Y halts +/// byte-identically to X, so their AIR structure (entry, segments, pages, +/// table counts, public output, runtime pages) is identical — they differ +/// ONLY in one instruction's bytes, hence different DECODE root, different +/// code-page root, and different `elf_digest`. +fn make_variant_program(x_bytes: &[u8]) -> Vec { + let executed = executed_pcs(x_bytes); + let words = exec_words(x_bytes); + + // A never-fetched slot we can rewrite to a valid, distinct instruction. + // Candidates are canonical nops (`addi x0,x0,K`), which always parse. + const NOP_0: u32 = 0x0000_0013; // addi x0, x0, 0 + const NOP_1: u32 = 0x0010_0013; // addi x0, x0, 1 + + let (file_off, _vaddr, cur) = words + .iter() + .find(|(_, vaddr, _)| !executed.contains(vaddr)) + .copied() + .expect("no never-executed executable word found to patch"); + + let new_word = if cur == NOP_1 { NOP_0 } else { NOP_1 }; + + let mut y = x_bytes.to_vec(); + y[file_off..file_off + 4].copy_from_slice(&new_word.to_le_bytes()); + assert_ne!(y, x_bytes.to_vec(), "variant must differ from base"); + y +} + +/// Custom prover: prove `prove_elf`'s execution honestly, but absorb +/// `statement_elf`'s identity into the Fiat-Shamir transcript instead of +/// `prove_elf`'s. Every preprocessed root in the resulting proof is computed +/// from `prove_elf`. Mirrors `prove_with_options_and_inputs`, swapping only +/// the `elf_bytes` passed to `absorb_statement`. +fn custom_prove_with_statement_elf( + prove_elf: &[u8], + statement_elf: &[u8], + opts: &stark::proof::options::ProofOptions, +) -> VmProof { + let program = Elf::load(prove_elf).expect("prove ELF load failed"); + let executor = Executor::new(&program, vec![]).expect("executor new"); + let result = executor.run().expect("run failed"); + + let max_rows = MaxRowsConfig::default(); + let mut traces = Traces::from_elf_and_logs(&program, &result.logs, &max_rows, &[]) + .expect("trace build failed"); + + let table_counts = traces.table_counts(); + let airs = VmAirs::new( + &program, + opts, + false, + &traces.page_configs, + &table_counts, + None, + true, + None, + None, + None, + ); + + let runtime_page_ranges = traces.runtime_page_ranges(); + let num_private_input_pages = traces + .page_configs + .iter() + .filter(|c| c.is_private_input) + .count(); + + let mut transcript = DefaultTranscript::::new(&[]); + absorb_statement( + &mut transcript, + StatementKind::Monolithic, + statement_elf, // <-- the substitution: X's identity, Y's everything else + &traces.public_output_bytes, + &table_counts, + num_private_input_pages, + &runtime_page_ranges, + ); + + let proof = Prover::multi_prove(airs.air_trace_pairs(&mut traces), &mut transcript) + .expect("multi_prove failed"); + + VmProof { + proof, + runtime_page_ranges, + table_counts, + public_output: traces.public_output_bytes.clone(), + num_private_input_pages, + } +} + +/// Sanity: the custom prover, used honestly (statement == proven program), +/// produces genuinely valid proofs. Guards against a vacuous PoC. +#[test] +fn test_custom_prover_is_not_vacuous() { + let x = read_guest_elf("empty"); + let proof = custom_prove_with_statement_elf(&x, &x, &MIN_PROOF_OPTIONS); + let ok = crate::verify_with_options(&proof, &x, &MIN_PROOF_OPTIONS, None, None) + .expect("verify errored"); + assert!(ok, "custom prover must produce valid proofs when honest"); +} + +/// `verify` accepts a proof whose Fiat-Shamir statement is X's but whose +/// constrained instructions and supplied roots are Y's — so verify is not the +/// binding. The `program_id` fold is: it commits an id that differs from the +/// honest id of X, making the substitution detectable downstream. +#[test] +fn test_supplied_decode_root_not_bound_to_inner_elf() { + let x = read_guest_elf("empty"); + let y = make_variant_program(&x); + + // X and Y differ, and specifically in their preprocessed DECODE roots. + assert_ne!(elf_digest(&x), elf_digest(&y), "elf_digest must differ"); + let (decode_x, pages_x) = precomputed_commitments(&x, &MIN_PROOF_OPTIONS); + let (decode_y, pages_y) = precomputed_commitments(&y, &MIN_PROOF_OPTIONS); + assert_ne!(decode_x, decode_y, "DECODE roots must differ (X vs Y)"); + + // Craft a proof: constrain Y, but absorb X's identity into the statement. + let proof = custom_prove_with_statement_elf(&y, &x, &MIN_PROOF_OPTIONS); + + // Negative control: the honest recompute path (None, None) rebuilds X's + // roots and rejects — the proof is NOT coincidentally valid for X. + let honest = crate::verify_with_options(&proof, &x, &MIN_PROOF_OPTIONS, None, None) + .expect("verify errored"); + assert!( + !honest, + "honest recompute (None, None) must reject: proof carries Y's roots, X recompute differs" + ); + + // verify is NOT the binding: with Y's roots supplied (the guest's + // private-input path), verification accepts for inner_elf = X. + let accepted = crate::verify_with_options( + &proof, + &x, + &MIN_PROOF_OPTIONS, + Some(decode_y), + Some(&pages_y), + ) + .expect("verify errored"); + assert!( + accepted, + "verify unexpectedly rejected the mismatched-root proof" + ); + + // The fold IS the binding: folding Y's supplied roots into X's identity + // yields an id that differs from the honest id of X. + let forged_id = crate::statement::program_id_from_elf(&x, &decode_y, &pages_y).unwrap(); + let honest_id = crate::statement::program_id_from_elf(&x, &decode_x, &pages_x).unwrap(); + assert_ne!( + forged_id, honest_id, + "program_id fold must make the root substitution detectable" + ); +} From 0039f84dc7c540d9f8e7b065ca8072932c113467 Mon Sep 17 00:00:00 2001 From: Mario Rugiero Date: Wed, 8 Jul 2026 11:22:59 -0300 Subject: [PATCH 3/5] fix build --- bench_vs/lambda/recursion/src/main.rs | 1 + .../src/tests/recursion_soundness_gap_poc.rs | 22 +++++++++++++++---- 2 files changed, 19 insertions(+), 4 deletions(-) diff --git a/bench_vs/lambda/recursion/src/main.rs b/bench_vs/lambda/recursion/src/main.rs index 30c37b9f8..4b0a67966 100644 --- a/bench_vs/lambda/recursion/src/main.rs +++ b/bench_vs/lambda/recursion/src/main.rs @@ -41,6 +41,7 @@ fn recursion_proof_options() -> ProofOptions { fri_number_of_queries: 1, coset_offset: 3, grinding_factor: 1, + fri_final_poly_log_degree: 7, } } diff --git a/prover/src/tests/recursion_soundness_gap_poc.rs b/prover/src/tests/recursion_soundness_gap_poc.rs index a48fec520..8bb8b1016 100644 --- a/prover/src/tests/recursion_soundness_gap_poc.rs +++ b/prover/src/tests/recursion_soundness_gap_poc.rs @@ -34,6 +34,7 @@ const MIN_PROOF_OPTIONS: stark::proof::options::ProofOptions = fri_number_of_queries: 1, coset_offset: 3, grinding_factor: 1, + fri_final_poly_log_degree: 7, }; fn workspace_root() -> PathBuf { @@ -166,8 +167,15 @@ fn custom_prove_with_statement_elf( let result = executor.run().expect("run failed"); let max_rows = MaxRowsConfig::default(); - let mut traces = Traces::from_elf_and_logs(&program, &result.logs, &max_rows, &[]) - .expect("trace build failed"); + let mut traces = Traces::from_elf_and_logs( + &program, + &result.logs, + &max_rows, + &[], + #[cfg(feature = "disk-spill")] + stark::storage_mode::StorageMode::Ram, + ) + .expect("trace build failed"); let table_counts = traces.table_counts(); let airs = VmAirs::new( @@ -199,10 +207,16 @@ fn custom_prove_with_statement_elf( &table_counts, num_private_input_pages, &runtime_page_ranges, + opts.fri_final_poly_log_degree, ); - let proof = Prover::multi_prove(airs.air_trace_pairs(&mut traces), &mut transcript) - .expect("multi_prove failed"); + let proof = Prover::multi_prove( + airs.air_trace_pairs(&mut traces), + &mut transcript, + #[cfg(feature = "disk-spill")] + stark::storage_mode::StorageMode::Ram, + ) + .expect("multi_prove failed"); VmProof { proof, From db2bfa8b7840dbf8560edd3871d410fe2ad03e45 Mon Sep 17 00:00:00 2001 From: Mario Rugiero Date: Wed, 8 Jul 2026 11:29:42 -0300 Subject: [PATCH 4/5] remove poc --- prover/src/tests/mod.rs | 2 - .../src/tests/recursion_soundness_gap_poc.rs | 291 ------------------ 2 files changed, 293 deletions(-) delete mode 100644 prover/src/tests/recursion_soundness_gap_poc.rs diff --git a/prover/src/tests/mod.rs b/prover/src/tests/mod.rs index e20d9b411..2c06d7fcf 100644 --- a/prover/src/tests/mod.rs +++ b/prover/src/tests/mod.rs @@ -71,8 +71,6 @@ pub mod prove_elfs_tests; #[cfg(test)] pub mod recursion_smoke_test; #[cfg(test)] -pub mod recursion_soundness_gap_poc; -#[cfg(test)] pub mod register_tests; #[cfg(test)] pub mod shift_tests; diff --git a/prover/src/tests/recursion_soundness_gap_poc.rs b/prover/src/tests/recursion_soundness_gap_poc.rs deleted file mode 100644 index 8bb8b1016..000000000 --- a/prover/src/tests/recursion_soundness_gap_poc.rs +++ /dev/null @@ -1,291 +0,0 @@ -//! `verify_with_options(.., Some(decode), Some(pages))` does NOT bind the -//! supplied roots to `inner_elf`: a custom prover can absorb `elf_digest(X)` -//! into the Fiat-Shamir statement while the constrained instructions and every -//! preprocessed root are those of a DIFFERENT program Y, and verification with -//! `inner_elf = X` and Y's roots still returns `Ok(true)` (the "critical -//! soundness check" in `crypto/stark/src/verifier.rs` compares two -//! prover-controlled values here, so it is vacuous against a custom prover). -//! -//! The recursion guest does not rely on verify for that binding: it commits -//! `program_id(inner_elf, decode, pages)`, which folds the supplied roots into -//! the identity — so the same substitution yields an id that differs from the -//! honest `program_id(X)`, detectable by whoever recomputes it natively and -//! compares. These tests pin both facts: verify accepts, and the fold catches. - -use std::collections::HashSet; -use std::path::PathBuf; - -use crypto::fiat_shamir::default_transcript::DefaultTranscript; -use stark::prover::{IsStarkProver, Prover}; - -use crate::statement::{StatementKind, absorb_statement, elf_digest}; -use crate::tables::trace_builder::Traces; -use crate::test_utils::E; -use crate::{Commitment, MaxRowsConfig, VmAirs, VmProof}; - -use executor::elf::Elf; -use executor::vm::execution::Executor; - -/// Smallest inner proof (blowup=2, 1 query) — for speed; soundness of the -/// *scheme* is what's under test, not the FRI security level. -const MIN_PROOF_OPTIONS: stark::proof::options::ProofOptions = - stark::proof::options::ProofOptions { - blowup_factor: 2, - fri_number_of_queries: 1, - coset_offset: 3, - grinding_factor: 1, - fri_final_poly_log_degree: 7, - }; - -fn workspace_root() -> PathBuf { - PathBuf::from(env!("CARGO_MANIFEST_DIR")) - .parent() - .expect("workspace root") - .to_path_buf() -} - -fn read_guest_elf(name: &str) -> Vec { - let path = workspace_root().join(format!("executor/program_artifacts/recursion/{name}.elf")); - std::fs::read(&path).unwrap_or_else(|e| { - panic!( - "failed to read {} — run `make compile-recursion-elfs`: {e}", - path.display() - ) - }) -} - -/// Precomputed DECODE + ELF-data-page commitments for `elf_bytes` under `opts` -/// — exactly what the recursion guest receives as private input. -fn precomputed_commitments( - elf_bytes: &[u8], - opts: &stark::proof::options::ProofOptions, -) -> (Commitment, Vec<(u64, Commitment)>) { - let elf = Elf::load(elf_bytes).expect("ELF load failed"); - let decode_commitment = - crate::tables::decode::commitment_from_elf(&elf, opts).expect("decode commitment failed"); - let page_commitments: Vec<(u64, Commitment)> = Traces::page_configs_from_elf(&elf) - .iter() - .filter(|c| c.init_values.is_some()) - .map(|c| { - ( - c.page_base, - crate::tables::page::compute_precomputed_commitment(c, opts), - ) - }) - .collect(); - (decode_commitment, page_commitments) -} - -/// The set of program-counter values fetched during a run of `elf_bytes`. -fn executed_pcs(elf_bytes: &[u8]) -> HashSet { - let elf = Elf::load(elf_bytes).expect("ELF load failed"); - let executor = Executor::new(&elf, vec![]).expect("executor new"); - let result = executor.run().expect("run failed"); - result.logs.iter().map(|l| l.current_pc).collect() -} - -/// Read a 4-byte word (LE) from an executable ELF segment at virtual address -/// `vaddr`, returning its raw-file byte offset and current value. Parses the -/// program headers directly so we can patch the raw bytes (and thus the -/// `elf_digest`) at exactly the right place. -fn exec_words(elf_bytes: &[u8]) -> Vec<(usize, u64, u32)> { - let rd_u16 = |o: usize| u16::from_le_bytes(elf_bytes[o..o + 2].try_into().unwrap()); - let rd_u32 = |o: usize| u32::from_le_bytes(elf_bytes[o..o + 4].try_into().unwrap()); - let rd_u64 = |o: usize| u64::from_le_bytes(elf_bytes[o..o + 8].try_into().unwrap()); - - let e_phoff = rd_u64(32) as usize; - let e_phentsize = rd_u16(54) as usize; - let e_phnum = rd_u16(56) as usize; - - const PT_LOAD: u32 = 1; - const PF_X: u32 = 1; - - let mut out = Vec::new(); - for i in 0..e_phnum { - let ph = e_phoff + i * e_phentsize; - let p_type = rd_u32(ph); - let p_flags = rd_u32(ph + 4); - if p_type != PT_LOAD || (p_flags & PF_X) == 0 { - continue; - } - let p_offset = rd_u64(ph + 8) as usize; - let p_vaddr = rd_u64(ph + 16); - let p_filesz = rd_u64(ph + 32) as usize; - let mut off = 0usize; - while off + 4 <= p_filesz { - let file_off = p_offset + off; - let vaddr = p_vaddr + off as u64; - out.push((file_off, vaddr, rd_u32(file_off))); - off += 4; - } - } - out -} - -/// Build program Y from program X (`= empty.elf`) by patching a single -/// executable-segment word at a PC that X never fetches, to a *different* -/// still-parseable instruction. Because the word is never fetched, Y halts -/// byte-identically to X, so their AIR structure (entry, segments, pages, -/// table counts, public output, runtime pages) is identical — they differ -/// ONLY in one instruction's bytes, hence different DECODE root, different -/// code-page root, and different `elf_digest`. -fn make_variant_program(x_bytes: &[u8]) -> Vec { - let executed = executed_pcs(x_bytes); - let words = exec_words(x_bytes); - - // A never-fetched slot we can rewrite to a valid, distinct instruction. - // Candidates are canonical nops (`addi x0,x0,K`), which always parse. - const NOP_0: u32 = 0x0000_0013; // addi x0, x0, 0 - const NOP_1: u32 = 0x0010_0013; // addi x0, x0, 1 - - let (file_off, _vaddr, cur) = words - .iter() - .find(|(_, vaddr, _)| !executed.contains(vaddr)) - .copied() - .expect("no never-executed executable word found to patch"); - - let new_word = if cur == NOP_1 { NOP_0 } else { NOP_1 }; - - let mut y = x_bytes.to_vec(); - y[file_off..file_off + 4].copy_from_slice(&new_word.to_le_bytes()); - assert_ne!(y, x_bytes.to_vec(), "variant must differ from base"); - y -} - -/// Custom prover: prove `prove_elf`'s execution honestly, but absorb -/// `statement_elf`'s identity into the Fiat-Shamir transcript instead of -/// `prove_elf`'s. Every preprocessed root in the resulting proof is computed -/// from `prove_elf`. Mirrors `prove_with_options_and_inputs`, swapping only -/// the `elf_bytes` passed to `absorb_statement`. -fn custom_prove_with_statement_elf( - prove_elf: &[u8], - statement_elf: &[u8], - opts: &stark::proof::options::ProofOptions, -) -> VmProof { - let program = Elf::load(prove_elf).expect("prove ELF load failed"); - let executor = Executor::new(&program, vec![]).expect("executor new"); - let result = executor.run().expect("run failed"); - - let max_rows = MaxRowsConfig::default(); - let mut traces = Traces::from_elf_and_logs( - &program, - &result.logs, - &max_rows, - &[], - #[cfg(feature = "disk-spill")] - stark::storage_mode::StorageMode::Ram, - ) - .expect("trace build failed"); - - let table_counts = traces.table_counts(); - let airs = VmAirs::new( - &program, - opts, - false, - &traces.page_configs, - &table_counts, - None, - true, - None, - None, - None, - ); - - let runtime_page_ranges = traces.runtime_page_ranges(); - let num_private_input_pages = traces - .page_configs - .iter() - .filter(|c| c.is_private_input) - .count(); - - let mut transcript = DefaultTranscript::::new(&[]); - absorb_statement( - &mut transcript, - StatementKind::Monolithic, - statement_elf, // <-- the substitution: X's identity, Y's everything else - &traces.public_output_bytes, - &table_counts, - num_private_input_pages, - &runtime_page_ranges, - opts.fri_final_poly_log_degree, - ); - - let proof = Prover::multi_prove( - airs.air_trace_pairs(&mut traces), - &mut transcript, - #[cfg(feature = "disk-spill")] - stark::storage_mode::StorageMode::Ram, - ) - .expect("multi_prove failed"); - - VmProof { - proof, - runtime_page_ranges, - table_counts, - public_output: traces.public_output_bytes.clone(), - num_private_input_pages, - } -} - -/// Sanity: the custom prover, used honestly (statement == proven program), -/// produces genuinely valid proofs. Guards against a vacuous PoC. -#[test] -fn test_custom_prover_is_not_vacuous() { - let x = read_guest_elf("empty"); - let proof = custom_prove_with_statement_elf(&x, &x, &MIN_PROOF_OPTIONS); - let ok = crate::verify_with_options(&proof, &x, &MIN_PROOF_OPTIONS, None, None) - .expect("verify errored"); - assert!(ok, "custom prover must produce valid proofs when honest"); -} - -/// `verify` accepts a proof whose Fiat-Shamir statement is X's but whose -/// constrained instructions and supplied roots are Y's — so verify is not the -/// binding. The `program_id` fold is: it commits an id that differs from the -/// honest id of X, making the substitution detectable downstream. -#[test] -fn test_supplied_decode_root_not_bound_to_inner_elf() { - let x = read_guest_elf("empty"); - let y = make_variant_program(&x); - - // X and Y differ, and specifically in their preprocessed DECODE roots. - assert_ne!(elf_digest(&x), elf_digest(&y), "elf_digest must differ"); - let (decode_x, pages_x) = precomputed_commitments(&x, &MIN_PROOF_OPTIONS); - let (decode_y, pages_y) = precomputed_commitments(&y, &MIN_PROOF_OPTIONS); - assert_ne!(decode_x, decode_y, "DECODE roots must differ (X vs Y)"); - - // Craft a proof: constrain Y, but absorb X's identity into the statement. - let proof = custom_prove_with_statement_elf(&y, &x, &MIN_PROOF_OPTIONS); - - // Negative control: the honest recompute path (None, None) rebuilds X's - // roots and rejects — the proof is NOT coincidentally valid for X. - let honest = crate::verify_with_options(&proof, &x, &MIN_PROOF_OPTIONS, None, None) - .expect("verify errored"); - assert!( - !honest, - "honest recompute (None, None) must reject: proof carries Y's roots, X recompute differs" - ); - - // verify is NOT the binding: with Y's roots supplied (the guest's - // private-input path), verification accepts for inner_elf = X. - let accepted = crate::verify_with_options( - &proof, - &x, - &MIN_PROOF_OPTIONS, - Some(decode_y), - Some(&pages_y), - ) - .expect("verify errored"); - assert!( - accepted, - "verify unexpectedly rejected the mismatched-root proof" - ); - - // The fold IS the binding: folding Y's supplied roots into X's identity - // yields an id that differs from the honest id of X. - let forged_id = crate::statement::program_id_from_elf(&x, &decode_y, &pages_y).unwrap(); - let honest_id = crate::statement::program_id_from_elf(&x, &decode_x, &pages_x).unwrap(); - assert_ne!( - forged_id, honest_id, - "program_id fold must make the root substitution detectable" - ); -} From 5fc54e653156ef969a748d014f0b9ef0e99dc4ea Mon Sep 17 00:00:00 2001 From: Mario Rugiero Date: Wed, 8 Jul 2026 12:59:21 -0300 Subject: [PATCH 5/5] ci(recursion): build recursion guest ELFs in the test-prover matrix test-prover reads prebuilt recursion ELFs at test-execution time (recursion_smoke_test's non-ignored tests) but never built or cached them, unlike test-prover-comprehensive which already does. CI failed with "failed to read .../recursion/empty.elf" on every shard. --- .github/workflows/pr_main.yaml | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/.github/workflows/pr_main.yaml b/.github/workflows/pr_main.yaml index 3f80c0582..34cac9dc0 100644 --- a/.github/workflows/pr_main.yaml +++ b/.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: