From fe26ffdbfc15c98b0104538c78404a734a697aeb Mon Sep 17 00:00:00 2001 From: Mario Rugiero Date: Mon, 6 Jul 2026 18:05:59 -0300 Subject: [PATCH 1/7] 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/7] 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/7] 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/7] 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/7] 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: From 367e53b9e3cfabf5a2655158778de76a3cb1481b Mon Sep 17 00:00:00 2001 From: MauroFab Date: Mon, 13 Jul 2026 15:50:59 -0300 Subject: [PATCH 6/7] =?UTF-8?q?recursion:=20review=20fixes=20=E2=80=94=20C?= =?UTF-8?q?I=20artifact=20prereqs,=20race-free=20preset=20builds,=20host?= =?UTF-8?q?=20attestation=20API,=20single-pass=20digest?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Makefile/CI: test-prover-cuda and test-prover-debug run the unfiltered prover suite, so they get the compile-recursion-elfs prerequisite the other CPU targets got (the GPU merge-queue job otherwise panics on the missing empty.elf). Drop .NOTPARALLEL — with prerequisites it serializes the whole make on GNU make <= 4.3 and doesn't serialize the two preset targets on >= 4.4; the cp race is instead fixed structurally by per-preset [[bin]] names (required-features), and the preset rules are generated from RECURSION_VERIFIER_PRESETS. - prover: new `recursion` module — host+guest API for the pipeline (encode_guest_input, verify_and_attest, check_attestation, expected_program_id, Preset, MIN_PROOF_OPTIONS). The consumer-side program_id recompute+compare the trust model mandates is production code now, not a test-only recipe. `statement` is private again; program_id* moved to `recursion`. - verify: split verify_prepared out of verify_with_options and absorb the statement from a precomputed digest so the recursion guest does one Elf::load and one full-ELF Keccak per run instead of two of each. - guest: decode recursion::GuestInput, PRESET fixed by the min/blowup8 feature, single verify_and_attest call; distinct bin per preset. - tests: restore recursion_soundness_gap_poc (removed in db2bfa8b but still cited by the PR body and a comment), extended with an end-to-end check_attestation rejection of the forged id; the smoke pipeline asserts via check_attestation (the real consumer path); stale doc/assert text fixed; MIN options single-sourced. --- Makefile | 63 ++-- bench_vs/lambda/recursion/Cargo.lock | 1 + bench_vs/lambda/recursion/Cargo.toml | 18 ++ bench_vs/lambda/recursion/src/main.rs | 83 ++---- prover/Cargo.toml | 4 +- prover/src/lib.rs | 55 +++- prover/src/recursion.rs | 276 ++++++++++++++++++ prover/src/statement.rs | 81 ++--- prover/src/tests/mod.rs | 2 + prover/src/tests/recursion_smoke_test.rs | 268 +++++++---------- .../src/tests/recursion_soundness_gap_poc.rs | 274 +++++++++++++++++ 11 files changed, 816 insertions(+), 309 deletions(-) create mode 100644 prover/src/recursion.rs create mode 100644 prover/src/tests/recursion_soundness_gap_poc.rs diff --git a/Makefile b/Makefile index 389d98420..a95360e9a 100644 --- a/Makefile +++ b/Makefile @@ -57,8 +57,10 @@ RECURSION_ARTIFACTS := $(addprefix $(RECURSION_ARTIFACTS_DIR)/, $(addsuffix .elf # 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. +# inner ProofOptions — see main.rs). Each preset builds its own distinctly +# named [[bin]] (recursion--bench) to its own artifact, via the +# define/foreach/eval below rather than the generic %.elf pattern rule. The +# distinct bin names also make the two `cp`s race-free under `make -j`. RECURSION_VERIFIER_PRESETS := min blowup8 RECURSION_VERIFIER_ARTIFACTS := $(addprefix $(RECURSION_ARTIFACTS_DIR)/recursion-, $(addsuffix .elf, $(RECURSION_VERIFIER_PRESETS))) @@ -149,10 +151,10 @@ compile-programs-rust: prepare-sysroot $(RUST_ARTIFACTS) compile-bench: prepare-sysroot $(BENCH_ARTIFACTS) -# NOTE: the recursion smoke tests are #[ignore]d (not run by `make test` / -# `test-executor`) because they're too slow for CI today; only `test-prover-all` -# runs them. We still compile their guest ELFs on every build so they keep -# compiling until the tests are fast enough to run in CI. +# NOTE: the recursion smoke tests read these prebuilt guest ELFs. The fast ones +# run on every `cargo test` (so `make test`, which depends on this target, needs +# them); the slow ones stay #[ignore]d (only `test-prover-all` runs them). We +# compile the guest ELFs on every build so the tests always have them ready. compile-programs: compile-programs-asm compile-programs-rust compile-bench compile-recursion-elfs compile-recursion-elfs: prepare-sysroot $(RECURSION_ARTIFACTS) $(RECURSION_VERIFIER_ARTIFACTS) @@ -213,20 +215,26 @@ $(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 -# "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) +# The recursion verifier's `min`/`blowup8` presets: same crate dir, one +# differently named [[bin]] per preset (recursion--bench, gated on that +# preset's Cargo feature) -> a differently named artifact. Generated per preset +# from RECURSION_VERIFIER_PRESETS via define/foreach/eval rather than a pattern +# rule (the stem "recursion-min" wouldn't match the crate dir "recursion") and +# rather than copy-paste (the presets list is the single source of truth). +# $(1) is the preset; the recipe uses $$ so `$$(call build_guest_elf,...)` +# survives the $(call ...) expansion and is expanded at recipe-run time (where +# $@ is defined). Because the two bins have distinct filenames the post-build +# `cp`s read different files, so the `make -j` cp race is gone structurally and +# no `.NOTPARALLEL` is needed: cargo's target-dir lock already serializes the +# compiles, and `.NOTPARALLEL` with prerequisites was wrong on every make +# version anyway (it serializes the whole build on GNU make <= 4.3 — macOS ships +# 3.81, ubuntu-latest 4.3 — and on >= 4.4 serializes only the listed targets' +# own prerequisites, never the two ELF targets against each other). +define recursion_verifier_rule +$(RECURSION_ARTIFACTS_DIR)/recursion-$(1).elf: FORCE | prepare-sysroot $(RECURSION_ARTIFACTS_DIR) + $$(call build_guest_elf,$$(RECURSION_GUESTS_DIR)/recursion,recursion-$(1)-bench,--features $(1)) +endef +$(foreach preset,$(RECURSION_VERIFIER_PRESETS),$(eval $(call recursion_verifier_rule,$(preset)))) clean-asm: -rm -rf $(ASM_ARTIFACTS_DIR) @@ -294,13 +302,16 @@ test-fast: compile-recursion-elfs test-prover: compile-recursion-elfs cargo test -p lambda-vm-prover -# Prover tests including slow ones. The recursion smoke tests (#[ignore]d) read -# prebuilt guest ELFs from executor/program_artifacts/recursion/, so build them first. +# Prover tests including slow ones. The recursion smoke tests read prebuilt +# guest ELFs from executor/program_artifacts/recursion/ — the fast ones on every +# run, the slow ones (still #[ignore]d) only under --include-ignored — so build +# them first. test-prover-all: compile-recursion-elfs cargo test -p lambda-vm-prover -- --include-ignored -# Prover tests with debug-checks (shows bus balance report) -test-prover-debug: +# Prover tests with debug-checks (shows bus balance report). Also unfiltered, so +# it runs the non-ignored recursion tests that read prebuilt guest ELFs. +test-prover-debug: compile-recursion-elfs cargo test -p lambda-vm-prover --features debug-checks -- --nocapture # Disk-spill tests (stark + prover). FORCE_DISK_SPILL is required by the prover tests. @@ -330,7 +341,9 @@ test-cuda-fallback: # GPU + nvcc). The GPU CI counterpart of CPU CI's sharded prover tests. Single-threaded: the # GPU serializes proves and the dispatch counters are process-global. cuda on prover cascades # to stark; crypto/ecsm build without it (they have no GPU path). -test-prover-cuda: +# compile-recursion-elfs: this unfiltered run executes the non-ignored recursion +# smoke tests, which read prebuilt guest ELFs; scripts/gpu_test.sh otherwise never builds them. +test-prover-cuda: compile-recursion-elfs cargo test --release -p lambda-vm-prover -p stark -p crypto -p ecsm \ --features lambda-vm-prover/cuda -- --test-threads=1 diff --git a/bench_vs/lambda/recursion/Cargo.lock b/bench_vs/lambda/recursion/Cargo.lock index 66048ba81..88a9fb605 100644 --- a/bench_vs/lambda/recursion/Cargo.lock +++ b/bench_vs/lambda/recursion/Cargo.lock @@ -412,6 +412,7 @@ dependencies = [ "executor", "log", "math", + "postcard", "serde", "sha3", "stark", diff --git a/bench_vs/lambda/recursion/Cargo.toml b/bench_vs/lambda/recursion/Cargo.toml index fdffdb27d..4b5e1970b 100644 --- a/bench_vs/lambda/recursion/Cargo.toml +++ b/bench_vs/lambda/recursion/Cargo.toml @@ -8,9 +8,27 @@ edition = "2024" [features] # Exactly one selects the fixed ProofOptions (see main.rs) — hardcoded, not # private input, so a malicious input can't downgrade the security level. +# Cargo features are additive by design, so the compile_error! mutual-exclusion +# guard in main.rs is the loud failure that stops a mislabeled artifact if both +# ever get enabled at once (e.g. under `--all-features`). The crate must stay a +# standalone `[workspace]` (not a root-workspace member) so root-level feature +# unification can never turn both on. min = [] blowup8 = [] +# One distinctly named binary per preset (selected by its feature) so a parallel +# `make -j` builds them to different filenames — structurally race-free, no cp +# clobbering. Both use src/main.rs; required-features gates each to its preset. +[[bin]] +name = "recursion-min-bench" +path = "src/main.rs" +required-features = ["min"] + +[[bin]] +name = "recursion-blowup8-bench" +path = "src/main.rs" +required-features = ["blowup8"] + [dependencies] lambda-vm-prover = { path = "../../../prover", default-features = false, features = [ "profile-markers", diff --git a/bench_vs/lambda/recursion/src/main.rs b/bench_vs/lambda/recursion/src/main.rs index 4b0a67966..b91f2b841 100644 --- a/bench_vs/lambda/recursion/src/main.rs +++ b/bench_vs/lambda/recursion/src/main.rs @@ -1,55 +1,37 @@ //! Naive recursion guest: verifies an inner lambda-vm proof inside the VM. //! -//! Private input (postcard): `(VmProof, Vec, Commitment, Vec<(u64, Commitment)>)` -//! — the inner program's ELF bytes plus its precomputed DECODE and +//! Private input (postcard): `lambda_vm_prover::recursion::GuestInput` — the +//! inner proof, the inner program's ELF bytes, and its precomputed DECODE and //! ELF-data-page commitments, supplied instead of recomputed in-VM. -//! `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 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). +//! `ProofOptions` is fixed by the `min`/`blowup8` Cargo feature (a `Preset`), +//! not private input — an attacker could otherwise pick trivially weak options +//! and have the guest accept as if a real proof had been checked. //! -//! On success commits `program_id(inner_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. +//! On success commits `program_id || inner_public_output` via +//! `recursion::verify_and_attest` (a single ELF parse and a single full-ELF +//! Keccak, shared between the statement absorb and the `program_id` fold). The +//! attestation is not self-enforcing: the binding is established by the +//! consumer via `recursion::check_attestation` (a host-side recompute+compare), +//! never in-guest. //! //! std (not `no_std`): `build-std` provides it, prove-side code is DCE'd. //! `#![no_main]`; inits the syscalls global allocator first thing in `main`. #![no_main] -#[cfg(feature = "blowup8")] -use lambda_vm_prover::GoldilocksCubicProofOptions; -use lambda_vm_prover::{Commitment, ProofOptions, VmProof}; +use lambda_vm_prover::recursion::{GuestInput, Preset}; #[cfg(not(any(feature = "min", feature = "blowup8")))] compile_error!("select exactly one of the `min`/`blowup8` features"); #[cfg(all(feature = "min", feature = "blowup8"))] compile_error!("select exactly one of the `min`/`blowup8` features"); -/// Smallest possible proof options (blowup=2, 1 query). Intentionally -/// insecure — for cheap diagnostics, not soundness. +/// The build preset fixing the inner `ProofOptions` (see the module docs). #[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). +const PRESET: Preset = Preset::Min; #[cfg(feature = "blowup8")] -fn recursion_proof_options() -> ProofOptions { - GoldilocksCubicProofOptions::with_blowup(8).expect("blowup=8 is always valid") -} +const PRESET: Preset = Preset::Blowup8; #[unsafe(export_name = "main")] pub fn main() -> ! { @@ -62,37 +44,26 @@ pub fn main() -> ! { })); let blob = lambda_vm_syscalls::syscalls::get_private_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"); + let (vm_proof, inner_elf, decode_commitment, page_commitments): GuestInput = + postcard::from_bytes(&blob).expect("failed to deserialize recursion input"); lambda_vm_prover::profile_markers::step_marker::< { lambda_vm_prover::profile_markers::STEP_DECODE_DONE }, >(); - let options = recursion_proof_options(); - let ok = lambda_vm_prover::verify_with_options( + // The guest's whole job: verify the inner proof against the supplied roots + // and, on success, produce `program_id || inner_public_output`. The id fold + // is what the consumer rebinds to a trusted ELF (`check_attestation`); it is + // not self-enforcing here. + let options = PRESET.options(); + let attestation = lambda_vm_prover::recursion::verify_and_attest( &vm_proof, &inner_elf, &options, - Some(decode_commitment), - Some(&page_commitments), - ) - .expect("verify errored"); - assert!(ok, "inner proof failed verification"); - - // 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, + 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); + .expect("verify errored") + .expect("inner proof failed verification"); + lambda_vm_syscalls::syscalls::commit(&attestation); lambda_vm_syscalls::syscalls::sys_halt(); } diff --git a/prover/Cargo.toml b/prover/Cargo.toml index 3695689d6..8630b2d86 100644 --- a/prover/Cargo.toml +++ b/prover/Cargo.toml @@ -21,6 +21,9 @@ math = { path = "../crypto/math" } executor = { path = "../executor" } ecsm = { path = "../crypto/ecsm" } serde = { version = "1.0", features = ["derive"] } +# The recursion guest-input blob codec (see `recursion::encode_guest_input`); +# no_std+alloc, so the in-VM guest build (default-features = false) is fine. +postcard = { version = "1.0", features = ["alloc"] } rayon = { version = "1.8.0", optional = true } sysinfo = { version = "0.31", default-features = false, features = ["system"] } log = "0.4" @@ -30,7 +33,6 @@ sha3 = { version = "0.10.8", default-features = false } env_logger = "*" criterion = { version = "0.5", default-features = false } bincode = "1" -postcard = { version = "1.0", features = ["alloc"] } tikv-jemallocator = "0.6" tikv-jemalloc-ctl = { version = "0.6", features = ["stats"] } tiny-keccak = { version = "2.0", features = ["keccak"] } diff --git a/prover/src/lib.rs b/prover/src/lib.rs index 6098413b1..11c7b7a13 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -20,7 +20,8 @@ mod debug_report; pub mod instruments; mod paged_mem; pub use stark::profile_markers; -pub mod statement; +pub mod recursion; +mod statement; pub mod tables; pub mod test_utils; #[cfg(test)] @@ -39,7 +40,7 @@ use stark::storage_mode::StorageMode; use stark::traits::AIR; use stark::verifier::{IsStarkVerifier, Verifier}; -use crate::statement::{StatementKind, absorb_statement}; +use crate::statement::{StatementKind, absorb_statement, absorb_statement_with_digest}; pub use crate::tables::MaxRowsConfig; use crate::tables::bitwise; use crate::tables::decode; @@ -58,8 +59,10 @@ use crate::test_utils::{ create_register_air, create_shift_air, create_store_air, }; -// 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`. +// Re-exported for downstream hosts and verifier guests (e.g. the in-VM +// recursion guest): `Commitment` is carried in the guest's private input +// (see `recursion::GuestInput`); the proof-options types name the parameters +// fixed at guest build time (`recursion::Preset`). pub use stark::config::Commitment; pub use stark::proof::options::{GoldilocksCubicProofOptions, ProofOptions}; use stark::proof::stark::MultiProof; @@ -199,6 +202,9 @@ pub enum Error { /// A non-final continuation epoch contains the program-terminating /// instruction. The terminating instruction must be in the final epoch. HaltInNonFinalEpoch, + /// Recursion host-side helper failed (guest-input encoding or + /// commitment recompute — see the `recursion` module). + Recursion(String), } impl fmt::Display for Error { @@ -227,6 +233,7 @@ impl fmt::Display for Error { "the program-terminating instruction must be in the final epoch" ) } + Error::Recursion(msg) => write!(f, "recursion helper error: {msg}"), } } } @@ -430,7 +437,7 @@ impl VmAirs { /// 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`). + /// callers must bind identity externally (see `recursion::check_attestation`). #[allow(clippy::too_many_arguments)] pub fn new( elf: &Elf, @@ -1004,13 +1011,40 @@ pub fn verify(vm_proof: &VmProof, elf_bytes: &[u8]) -> Result { /// 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`). +/// the caller must bind identity externally (the recursion pipeline commits +/// `recursion::program_id` and the consumer checks it via +/// `recursion::check_attestation`). pub fn verify_with_options( vm_proof: &VmProof, elf_bytes: &[u8], proof_options: &ProofOptions, decode_commitment: Option, page_commitments: Option<&[(u64, Commitment)]>, +) -> Result { + let program = Elf::load(elf_bytes).map_err(|e| Error::ElfLoad(format!("{e}")))?; + let elf_digest = statement::elf_digest(elf_bytes); + verify_prepared( + vm_proof, + &program, + &elf_digest, + proof_options, + decode_commitment, + page_commitments, + ) +} + +/// [`verify_with_options`] with the ELF already parsed and digested. Callers +/// that need the parsed ELF or the digest for other purposes reuse them — the +/// recursion attestation (`recursion::verify_and_attest`) shares one +/// `Elf::load` and one full-ELF Keccak between verification and the +/// `program_id` fold, which matters in-guest where both are expensive. +pub(crate) fn verify_prepared( + vm_proof: &VmProof, + program: &Elf, + elf_digest: &[u8; 32], + proof_options: &ProofOptions, + decode_commitment: Option, + page_commitments: Option<&[(u64, Commitment)]>, ) -> Result { // Validate table_counts before constructing AIRs. // A malicious prover could set counts to 0, removing entire constraint sets. @@ -1028,9 +1062,8 @@ pub fn verify_with_options( } } - let program = Elf::load(elf_bytes).map_err(|e| Error::ElfLoad(format!("{e}")))?; let page_configs = Traces::page_configs_from_elf_and_runtime( - &program, + program, &vm_proof.runtime_page_ranges, vm_proof.num_private_input_pages, ); @@ -1050,7 +1083,7 @@ pub fn verify_with_options( } let airs = VmAirs::new( - &program, + program, proof_options, false, &page_configs, @@ -1071,10 +1104,10 @@ pub fn verify_with_options( // field makes this diverge from the prover's transcript state, so every // derived challenge differs and verification rejects. let mut transcript = DefaultTranscript::::new(&[]); - absorb_statement( + absorb_statement_with_digest( &mut transcript, StatementKind::Monolithic, - elf_bytes, + elf_digest, &vm_proof.public_output, &vm_proof.table_counts, vm_proof.num_private_input_pages, diff --git a/prover/src/recursion.rs b/prover/src/recursion.rs new file mode 100644 index 000000000..9bac79943 --- /dev/null +++ b/prover/src/recursion.rs @@ -0,0 +1,276 @@ +//! Host and guest API for the naive (single-step) recursion pipeline. +//! +//! The recursion verifier guest (`bench_vs/lambda/recursion`) verifies an +//! inner lambda-vm proof in-VM. Its private input ([`GuestInput`], built +//! host-side by [`encode_guest_input`]) carries the inner program's +//! precomputed DECODE/ELF-data-page roots so the guest skips the in-VM +//! FFT + Merkle rebuild. `verify_with_options` uses supplied roots verbatim — +//! it does NOT bind them to the inner ELF — so on success the guest commits +//! an attestation that folds them into the identity instead: +//! `program_id || inner_public_output` (see [`verify_and_attest`]). +//! +//! Trust model: the attestation is NOT self-enforcing. A consumer of the +//! outer proof MUST recompute the id from the inner ELF it trusts and +//! compare — that is [`check_attestation`]. A substituted root yields an id +//! that differs from the honest recompute ([`expected_program_id`]), so the +//! substitution `verify_with_options` cannot see is rejected here. The +//! recompute is an expensive native FFT + Merkle pass, done once at the top +//! level, never in-VM. `prover/src/tests/recursion_soundness_gap_poc.rs` +//! demonstrates the attack this compare defeats. +//! +//! [`program_id`] deliberately does not fold the `ProofOptions`: the security +//! level is pinned by which verifier guest the outer proof is checked against +//! (`recursion-min.elf` vs `recursion-blowup8.elf`, fixed at build time — see +//! [`Preset`]). A consumer must pin that outer ELF too, or a 1-query `min` +//! attestation is indistinguishable from a 128-bit `blowup8` one. + +use executor::elf::Elf; +use sha3::{Digest, Keccak256}; + +use crate::statement::elf_digest; +use crate::tables::trace_builder::Traces; +use crate::{Commitment, Error, ProofOptions, VmProof}; + +/// Smallest possible proof options (blowup=2, 1 query). Intentionally +/// insecure — for cheap diagnostics, not soundness. The single source for the +/// `recursion-min` guest build and the host tests that must match it. +pub const MIN_PROOF_OPTIONS: ProofOptions = ProofOptions { + blowup_factor: 2, + fri_number_of_queries: 1, + coset_offset: 3, + grinding_factor: 1, + fri_final_poly_log_degree: 7, +}; + +/// The recursion verifier's build presets. Each fixes the guest's +/// `ProofOptions` at build time (a Cargo feature — private input could +/// otherwise downgrade the security level) and names the ELF artifact +/// `make compile-recursion-elfs` produces. Deriving both from one value keeps +/// a host from proving the inner under options the guest wasn't built for. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Preset { + /// Blowup=2, 1 query ([`MIN_PROOF_OPTIONS`]) — insecure, diagnostics only. + Min, + /// Blowup=8, multi-query — 128-bit security. + Blowup8, +} + +impl Preset { + /// The fixed `ProofOptions` this preset's guest verifies with. + pub fn options(&self) -> ProofOptions { + match self { + Preset::Min => MIN_PROOF_OPTIONS, + Preset::Blowup8 => crate::GoldilocksCubicProofOptions::with_blowup(8) + .expect("blowup=8 is always valid"), + } + } + + /// Artifact stem under `executor/program_artifacts/recursion/` + /// (`.elf`), matching the Makefile's preset rules. + pub fn artifact_stem(&self) -> &'static str { + match self { + Preset::Min => "recursion-min", + Preset::Blowup8 => "recursion-blowup8", + } + } + + /// Short preset name (the Cargo feature that selects it). + pub fn name(&self) -> &'static str { + match self { + Preset::Min => "min", + Preset::Blowup8 => "blowup8", + } + } +} + +/// The guest's private-input layout, postcard-encoded by +/// [`encode_guest_input`] and decoded verbatim by the guest: +/// `(inner proof, inner ELF bytes, DECODE root, ELF-data-page roots)`. +pub type GuestInput = (VmProof, Vec, Commitment, Vec<(u64, Commitment)>); + +/// Precompute the DECODE and ELF-data-page preprocessed roots for `elf_bytes` +/// under `opts` — the values the guest receives via private input instead of +/// recomputing in-VM, and the values [`expected_program_id`] recomputes +/// natively. Selection matches the verifier's page construction: every ELF +/// data page (`init_values.is_some()`), keyed by `page_base`; zero-init pages +/// use a compile-time constant and are never listed. +pub fn precomputed_commitments( + elf_bytes: &[u8], + opts: &ProofOptions, +) -> Result<(Commitment, Vec<(u64, Commitment)>), Error> { + let elf = Elf::load(elf_bytes).map_err(|e| Error::ElfLoad(format!("{e}")))?; + let decode_commitment = crate::tables::decode::commitment_from_elf(&elf, opts) + .map_err(|e| Error::Recursion(format!("DECODE commitment from ELF: {e}")))?; + 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(); + Ok((decode_commitment, page_commitments)) +} + +/// Build the guest's private-input blob for `inner_proof` of `inner_elf`: +/// precomputes the roots and postcard-encodes the [`GuestInput`] tuple. +pub fn encode_guest_input( + inner_proof: &VmProof, + inner_elf: &[u8], + opts: &ProofOptions, +) -> Result, Error> { + let (decode_commitment, page_commitments) = precomputed_commitments(inner_elf, opts)?; + postcard::to_allocvec(&( + inner_proof, + inner_elf, + &decode_commitment, + &page_commitments, + )) + .map_err(|e| Error::Recursion(format!("postcard encode: {e}"))) +} + +/// Domain tag for [`program_id`]. +const PROGRAM_ID_TAG: &[u8] = b"LAMBDAVM_PROGRAM_ID_V1"; + +/// [`program_id`] from a precomputed ELF digest and entry point — the guest +/// path, sharing one full-ELF Keccak pass with the verify-side statement +/// absorb (see [`verify_and_attest`]). +pub fn program_id_from_digest( + elf_digest: &[u8; 32], + 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); + 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() +} + +/// 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 +/// ([`check_attestation`]). +pub fn program_id( + elf_bytes: &[u8], + pc_start: u64, + decode_commitment: &Commitment, + page_commitments: &[(u64, Commitment)], +) -> [u8; 32] { + program_id_from_digest( + &elf_digest(elf_bytes), + pc_start, + decode_commitment, + page_commitments, + ) +} + +/// [`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], Error> { + let elf = Elf::load(elf_bytes).map_err(|e| Error::ElfLoad(format!("{e}")))?; + Ok(program_id( + elf_bytes, + elf.entry_point, + decode_commitment, + page_commitments, + )) +} + +/// Verify an inner proof against supplied roots and, on success, produce the +/// attestation bytes the recursion guest commits: +/// `program_id(elf, roots) || inner_public_output`. `Ok(None)` means the +/// proof did not verify. This is the guest's whole job in one call; it does a +/// single `Elf::load` and a single full-ELF Keccak, shared between the +/// statement absorb and the `program_id` fold. +/// +/// The attestation binds identity only for a consumer that recomputes the id +/// from a trusted ELF ([`check_attestation`]) — see the module docs. +pub fn verify_and_attest( + vm_proof: &VmProof, + elf_bytes: &[u8], + proof_options: &ProofOptions, + decode_commitment: Commitment, + page_commitments: &[(u64, Commitment)], +) -> Result>, Error> { + let program = Elf::load(elf_bytes).map_err(|e| Error::ElfLoad(format!("{e}")))?; + let digest = elf_digest(elf_bytes); + let ok = crate::verify_prepared( + vm_proof, + &program, + &digest, + proof_options, + Some(decode_commitment), + Some(page_commitments), + )?; + if !ok { + return Ok(None); + } + let id = program_id_from_digest( + &digest, + program.entry_point, + &decode_commitment, + page_commitments, + ); + let mut attestation = id.to_vec(); + attestation.extend_from_slice(&vm_proof.public_output); + Ok(Some(attestation)) +} + +/// Split committed attestation bytes into `(program_id, inner_public_output)`. +/// `None` if too short to contain an id. +pub fn split_attestation(committed: &[u8]) -> Option<([u8; 32], &[u8])> { + if committed.len() < 32 { + return None; + } + let id: [u8; 32] = committed[..32].try_into().ok()?; + Some((id, &committed[32..])) +} + +/// The honest `program_id` for a trusted inner ELF under `opts`: recomputes +/// the DECODE/page roots natively (the expensive FFT + Merkle pass) and folds +/// them. Compute once per (ELF, opts) and reuse across proofs. +pub fn expected_program_id( + trusted_elf_bytes: &[u8], + opts: &ProofOptions, +) -> Result<[u8; 32], Error> { + let (decode_commitment, page_commitments) = precomputed_commitments(trusted_elf_bytes, opts)?; + program_id_from_elf(trusted_elf_bytes, &decode_commitment, &page_commitments) +} + +/// The mandatory consumer-side binding check (see the module docs): split the +/// guest's committed bytes, recompute the id from the ELF the *consumer* +/// trusts, and compare. `Ok(Some(inner_public_output))` on match; `Ok(None)` +/// if the bytes are malformed or attest a different (ELF, roots) identity — +/// i.e. the inner proof was not for `trusted_elf_bytes` as the consumer knows +/// it. The caller must also have verified the outer proof against the pinned +/// `recursion-.elf` with `opts = preset.options()`. +pub fn check_attestation( + committed: &[u8], + trusted_elf_bytes: &[u8], + opts: &ProofOptions, +) -> Result>, Error> { + let Some((id, inner_public_output)) = split_attestation(committed) else { + return Ok(None); + }; + if id != expected_program_id(trusted_elf_bytes, opts)? { + return Ok(None); + } + Ok(Some(inner_public_output.to_vec())) +} diff --git a/prover/src/statement.rs b/prover/src/statement.rs index 9f786da3a..617d3d33d 100644 --- a/prover/src/statement.rs +++ b/prover/src/statement.rs @@ -10,67 +10,23 @@ //! 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::{Commitment, RuntimePageRange, TableCounts}; +use crate::{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 transcript. Public so the recursion guest can commit to it directly. -pub fn elf_digest(elf: &[u8]) -> [u8; 32] { +/// into the transcript. The recursion attestation folds the same digest into +/// `program_id` (see the `recursion` module), sharing one pass over the ELF. +pub(crate) 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 @@ -93,6 +49,33 @@ pub(crate) fn absorb_statement( num_private_input_pages: usize, runtime_page_ranges: &[RuntimePageRange], fri_final_poly_log_degree: u8, +) { + absorb_statement_with_digest( + t, + kind, + &elf_digest(elf_bytes), + public_output, + table_counts, + num_private_input_pages, + runtime_page_ranges, + fri_final_poly_log_degree, + ) +} + +/// [`absorb_statement`] with the ELF digest precomputed. Callers that already +/// hold the digest reuse it instead of a second full-ELF Keccak pass — the +/// recursion attestation path shares one digest between the transcript absorb +/// and the `program_id` fold (a full-ELF hash is expensive in-guest). +#[allow(clippy::too_many_arguments)] +pub(crate) fn absorb_statement_with_digest( + t: &mut impl IsTranscript, + kind: StatementKind, + elf_digest: &[u8; 32], + public_output: &[u8], + table_counts: &TableCounts, + num_private_input_pages: usize, + runtime_page_ranges: &[RuntimePageRange], + fri_final_poly_log_degree: u8, ) { // Leading domain tag — distinct per statement kind, so a monolithic proof and // a continuation epoch proof can never share a transcript prefix. @@ -103,7 +86,7 @@ pub(crate) fn absorb_statement( t.append_bytes(domain_tag); // ELF: fixed 32-byte digest — no length prefix needed. - t.append_bytes(&elf_digest(elf_bytes)); + t.append_bytes(elf_digest); // public_output: variable length → length-prefix to prevent boundary collisions. t.append_bytes(&(public_output.len() as u64).to_le_bytes()); 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 602957093..61659a372 100644 --- a/prover/src/tests/recursion_smoke_test.rs +++ b/prover/src/tests/recursion_smoke_test.rs @@ -1,14 +1,18 @@ //! 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 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. +//! build the guest's private-input blob with `recursion::encode_guest_input`, +//! hand it to the in-VM verifier guest, then execute or prove the guest. Guest +//! ELFs come from `make compile-recursion-elfs`. `ProofOptions` is fixed per +//! preset at build time (`recursion::Preset`); `decode_commitment`/ +//! `page_commitments` are private input, precomputed host-side. Each pipeline +//! host-verifies the inner proof via full recompute (`None, None`) as a +//! ground-truth check, then runs the production consumer check +//! (`recursion::check_attestation`) over the guest's committed attestation. use std::ops::ControlFlow; use std::path::PathBuf; +use crate::recursion::{self, MIN_PROOF_OPTIONS, Preset}; + fn workspace_root() -> PathBuf { PathBuf::from(env!("CARGO_MANIFEST_DIR")) .parent() @@ -27,73 +31,16 @@ 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. Matches the `recursion-min.elf` -/// build's hardcoded `ProofOptions`. -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, - }; - -/// 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, -) -> (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: `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 = - 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 -} - -/// 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`). +/// Prove `inner_elf` under `opts` and build the guest's private-input blob via +/// [`recursion::encode_guest_input`] (which precomputes the DECODE/page roots +/// and postcard-encodes the [`recursion::GuestInput`] tuple). Returns the proof +/// and the blob. fn prove_inner_and_encode_blob( tag: &str, inner_elf: &[u8], inner_input: &[u8], opts: &stark::proof::options::ProofOptions, -) -> ( - crate::VmProof, - Vec, - crate::Commitment, - Vec<(u64, crate::Commitment)>, -) { +) -> (crate::VmProof, Vec) { eprintln!( "[{tag}] proving inner (blowup={}, fri_queries={}) ...", opts.blowup_factor, opts.fri_number_of_queries @@ -106,17 +53,10 @@ fn prove_inner_and_encode_blob( ) .expect("inner prove should succeed"); - 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"); + let blob = recursion::encode_guest_input(&inner_proof, inner_elf, opts) + .expect("recursion::encode_guest_input failed"); eprintln!("[{tag}] postcard blob: {} bytes", blob.len()); - (inner_proof, blob, decode_commitment, page_commitments) + (inner_proof, blob) } /// Whether to also prove the guest's own execution after handing it the proof. @@ -215,13 +155,12 @@ fn drive_executor( (total_cycles, start.elapsed()) } -/// Shared preamble: build the blob (an `empty` inner proof under `opts`), load -/// the `recursion-.elf` verifier, and stand up an executor. Returns -/// `(elf_bytes, program, executor)`. +/// Shared preamble: build the blob (an `empty` inner proof under the preset's +/// options), load the `recursion-.elf` verifier, and stand up an +/// executor. Returns `(elf_bytes, program, executor)`. fn setup_guest_run( label: &str, - preset: &str, - opts: &stark::proof::options::ProofOptions, + preset: Preset, ) -> ( Vec, executor::elf::Elf, @@ -229,15 +168,17 @@ 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, &format!("recursion-{preset}")); + let guest_elf_bytes = read_guest_elf(&root, preset.artifact_stem()); - let (_inner_proof, blob, _decode_commitment, _page_commitments) = - prove_inner_and_encode_blob(label, &empty_elf_bytes, &[], opts); + let (_inner_proof, blob) = + prove_inner_and_encode_blob(label, &empty_elf_bytes, &[], &preset.options()); let program = executor::elf::Elf::load(&guest_elf_bytes).expect("ELF load failed"); assert_ne!( - program.entry_point, 0, - "recursion-{preset} ELF has entry_point=0 — build artifact is malformed" + program.entry_point, + 0, + "recursion-{} ELF has entry_point=0 — build artifact is malformed", + preset.name() ); let executor = executor::vm::execution::Executor::new(&program, blob).expect("Executor::new failed"); @@ -268,11 +209,6 @@ const STEP_LABELS: [&str; 7] = [ "6. step 4: verify_trace_and_composition_openings (+ wrap-up)", ]; -/// `blowup=8` (128-bit, multi-query) options for the `multiquery` variants. -fn blowup8() -> stark::proof::options::ProofOptions { - crate::GoldilocksCubicProofOptions::with_blowup(8).expect("blowup=8 is always valid") -} - /// Short per-step tag for the function table, keyed by the same bucket index /// used in `STEP_LABELS`/`buckets`. fn step_tag(bucket: u8) -> &'static str { @@ -392,15 +328,11 @@ fn print_step_breakdown(buckets: &[u64; 7], total_cycles: u64) { /// per-step cycle breakdown (marker decode is cheap — one `InstructionCache` /// 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( - preset: &str, - progress_stride: usize, - opts: stark::proof::options::ProofOptions, - detailed: bool, -) { +fn run_profile(preset: Preset, progress_stride: usize, detailed: bool) { use std::collections::HashMap; - let (guest_elf_bytes, program, mut executor) = setup_guest_run("profile", preset, &opts); + let opts = preset.options(); + let (guest_elf_bytes, program, mut executor) = setup_guest_run("profile", preset); let symbols = executor::elf::SymbolTable::parse(&guest_elf_bytes); let instructions = executor::vm::execution::InstructionCache::new(&program.data) .expect("instruction cache build failed"); @@ -411,7 +343,8 @@ fn run_profile( let unique = std::cell::Cell::new(0usize); eprintln!( - "[profile] executing recursion-{preset} guest ({}) ...", + "[profile] executing recursion-{} guest ({}) ...", + preset.name(), if detailed { "histogram + steps" } else { @@ -457,7 +390,7 @@ fn run_profile( eprintln!("============================================================"); eprintln!( " RECURSION-{} GUEST PROFILE (blowup={}, {} queries)", - preset.to_uppercase(), + preset.name().to_uppercase(), opts.blowup_factor, opts.fri_number_of_queries, ); @@ -486,37 +419,29 @@ fn run_profile( eprintln!("============================================================"); } -/// 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). +/// Core pipeline: prove the inner program under `preset.options()`, run the +/// guest (`recursion-.elf`) to `mode`, then run the production consumer +/// check — recompute the program id from the trusted inner ELF and compare it +/// against the guest's committed attestation (`program_id || inner_public_output`) +/// via [`recursion::check_attestation`]. A match means the in-VM verifier +/// accepted the proof and the host-side identity binding holds. 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, + preset: Preset, mode: OuterMode, ) { let root = workspace_root(); - let recursion_elf_bytes = read_guest_elf(&root, &format!("recursion-{preset}")); + let recursion_elf_bytes = read_guest_elf(&root, preset.artifact_stem()); + let opts = preset.options(); - let (inner_proof, blob, decode_commitment, page_commitments) = prove_inner_and_encode_blob( - label, - inner_elf_bytes, - inner_private_input, - &inner_proof_options, - ); + let (inner_proof, blob) = + prove_inner_and_encode_blob(label, inner_elf_bytes, inner_private_input, &opts); assert!( - crate::verify_with_options( - &inner_proof, - inner_elf_bytes, - &inner_proof_options, - None, - None - ) - .expect("inner verify errored"), + crate::verify_with_options(&inner_proof, inner_elf_bytes, &opts, None, None) + .expect("inner verify errored"), "inner proof must verify on host" ); assert!( @@ -529,55 +454,50 @@ 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, - &inner_proof.public_output, - ); + // Production consumer path: recompute the id from the trusted inner ELF and + // compare against the guest's committed attestation (the real host-side + // binding). `Some(inner_public_output)` iff the recompute matches. + let inner_output = recursion::check_attestation(&committed, inner_elf_bytes, &opts) + .expect("check_attestation errored") + .expect( + "guest attestation must match the trusted inner ELF (program_id recompute+compare)", + ); assert_eq!( - committed, expected, - "recursion guest must commit elf_digest||decode_commitment||page_commitments (in-VM verify accepted)" + inner_output, inner_proof.public_output, + "attested inner public output must equal the inner proof's public output" ); - eprintln!("[{label}] guest committed the expected commitments: in-VM verify accepted ✓"); + eprintln!("[{label}] guest attestation matched the trusted inner ELF (program_id recompute) ✓"); } -/// `run_recursion_pipeline_with_options` with `blowup=8` (the `empty`/`fibonacci` default). +/// `run_recursion_pipeline_with_options` at `blowup=8` (the `empty`/`fibonacci` +/// default), i.e. [`Preset::Blowup8`]. fn run_recursion_pipeline( label: &str, inner_elf_bytes: &[u8], inner_private_input: &[u8], mode: OuterMode, ) { - let inner_proof_options = stark::proof::options::GoldilocksCubicProofOptions::with_blowup(8) - .expect("blowup=8 is always valid"); run_recursion_pipeline_with_options( label, inner_elf_bytes, inner_private_input, - inner_proof_options, - "blowup8", + Preset::Blowup8, mode, ); } -/// Decode the blob on the host and verify — a cheap guard on the encode/decode -/// contract without running the VM. +/// Decode the blob on the host and mirror the guest's verify+attest, then run +/// the consumer check — a cheap guard on the encode/decode/attest contract +/// without running the VM. #[test] 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, _decode_commitment, _page_commitments) = + let (_inner, blob) = prove_inner_and_encode_blob("roundtrip", &empty_elf_bytes, &[], &MIN_PROOF_OPTIONS); // 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 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}"), @@ -588,19 +508,33 @@ fn test_recursion_blob_decodes_and_verifies_on_host() { page_commitments.len(), ); - match crate::verify_with_options( + // Mirror the guest exactly: verify_and_attest over the supplied roots. + let attestation = match recursion::verify_and_attest( &vm_proof, &inner_elf, &MIN_PROOF_OPTIONS, - Some(decode_commitment), - Some(&page_commitments), + decode_commitment, + &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" + Ok(Some(a)) => { + eprintln!("[roundtrip] verify_and_attest accepted — guest path is sound"); + a + } + Ok(None) => panic!( + "[roundtrip] verify_and_attest returned None (guest hits the failed-verification expect) — proof did not survive the postcard round-trip" ), - Err(e) => panic!("[roundtrip] verify ERRORED (guest hits .expect): {e:?}"), - } + Err(e) => panic!("[roundtrip] verify_and_attest ERRORED (guest hits .expect): {e:?}"), + }; + + // Consumer check: the committed attestation must bind to the trusted inner + // ELF and carry the inner proof's public output. + let output = recursion::check_attestation(&attestation, &inner_elf, &MIN_PROOF_OPTIONS) + .expect("check_attestation errored") + .expect("attestation must match the trusted inner ELF (program_id recompute+compare)"); + assert_eq!( + output, vm_proof.public_output, + "attested public output must equal the inner proof's public output" + ); } /// Corrupting a private-input commitment on an *honest* proof makes @@ -612,12 +546,15 @@ fn test_recursion_blob_decodes_and_verifies_on_host() { 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( + let (vm_proof, _blob) = prove_inner_and_encode_blob( "corrupt-commitment", &empty_elf_bytes, &[], &MIN_PROOF_OPTIONS, ); + let (mut decode_commitment, page_commitments) = + recursion::precomputed_commitments(&empty_elf_bytes, &MIN_PROOF_OPTIONS) + .expect("precomputed_commitments failed"); decode_commitment[0] ^= 0xFF; let ok = crate::verify_with_options( @@ -660,8 +597,7 @@ fn test_recursion_execute_1query() { "recursion-exec-1query", &empty_elf_bytes, &[], - MIN_PROOF_OPTIONS, - "min", + Preset::Min, OuterMode::ExecuteOnly, ); } @@ -681,8 +617,7 @@ fn test_recursion_execute_1query() { #[test] #[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", "min", &MIN_PROOF_OPTIONS); + let (_bytes, program, mut executor) = setup_guest_run("step-markers", Preset::Min); let instructions = executor::vm::execution::InstructionCache::new(&program.data) .expect("instruction cache build failed"); @@ -773,8 +708,7 @@ fn test_recursion_prove_1query() { "recursion-prove-1query", &empty_elf_bytes, &[], - MIN_PROOF_OPTIONS, - "min", + Preset::Min, OuterMode::Prove, ); } @@ -787,7 +721,7 @@ fn test_dump_recursion_input() { let root = workspace_root(); let empty_elf_bytes = read_guest_elf(&root, "empty"); - let (_inner_proof, blob, _decode_commitment, _page_commitments) = + let (_inner_proof, blob) = prove_inner_and_encode_blob("dump-input", &empty_elf_bytes, &[], &MIN_PROOF_OPTIONS); let path = "/tmp/recursion_input.bin"; @@ -799,28 +733,28 @@ fn test_dump_recursion_input() { #[test] #[ignore = "diagnostic: fast; recursion guest cycle count (1 query)"] fn test_recursion_cycles_1query() { - run_profile("min", 500, MIN_PROOF_OPTIONS, false); + run_profile(Preset::Min, 500, 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("blowup8", 500, blowup8(), false); + run_profile(Preset::Blowup8, 500, 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("min", 500, MIN_PROOF_OPTIONS, true); + run_profile(Preset::Min, 500, 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("blowup8", 500, blowup8(), true); + run_profile(Preset::Blowup8, 500, true); } /// Inner program: fibonacci(10). 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..73410ff62 --- /dev/null +++ b/prover/src/tests/recursion_soundness_gap_poc.rs @@ -0,0 +1,274 @@ +//! `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 (`recursion::check_attestation`). These tests pin both facts: +//! verify accepts, and the fold-and-compare catches. + +use std::collections::HashSet; +use std::path::PathBuf; + +use crypto::fiat_shamir::default_transcript::DefaultTranscript; +use stark::prover::{IsStarkProver, Prover}; + +use crate::recursion::{MIN_PROOF_OPTIONS, precomputed_commitments}; +use crate::statement::{StatementKind, absorb_statement, elf_digest}; +use crate::tables::trace_builder::Traces; +use crate::test_utils::E; +use crate::{MaxRowsConfig, VmAirs, VmProof}; + +use executor::elf::Elf; +use executor::vm::execution::Executor; + +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() + ) + }) +} + +/// 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).expect("precomputed_commitments X"); + let (decode_y, pages_y) = + precomputed_commitments(&y, &MIN_PROOF_OPTIONS).expect("precomputed_commitments Y"); + 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::recursion::program_id_from_elf(&x, &decode_y, &pages_y).unwrap(); + let honest_id = crate::recursion::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" + ); + + // End-to-end consumer path: the guest would commit `forged_id || + // public_output`; the mandatory host-side compare (`check_attestation`) + // rejects exactly this substitution that `verify` accepts above. + let mut forged = forged_id.to_vec(); + forged.extend_from_slice(&proof.public_output); + assert!( + crate::recursion::check_attestation(&forged, &x, &MIN_PROOF_OPTIONS) + .expect("check_attestation errored") + .is_none(), + "check_attestation must reject the forged attestation the consumer would receive" + ); +} From e7c8f75a210b09aec4574746df68eadd6fdc4da7 Mon Sep 17 00:00:00 2001 From: Mario Rugiero Date: Mon, 13 Jul 2026 16:59:27 -0300 Subject: [PATCH 7/7] recursion: gate check_attestation on Preset, document program_id encoding check_attestation_for_preset refuses Preset::Min so a production consumer can't accidentally pin trust to the intentionally-insecure 1-query preset; check_attestation itself stays available for diagnostics. Also documents why program_id's fold needs no length prefix on decode_commitment (fixed-size Commitment). --- prover/src/recursion.rs | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/prover/src/recursion.rs b/prover/src/recursion.rs index 9bac79943..0c290264b 100644 --- a/prover/src/recursion.rs +++ b/prover/src/recursion.rs @@ -164,6 +164,11 @@ pub fn program_id_from_digest( /// order). Folding the roots in makes a supplied-root substitution yield a /// different id than an honest native recompute — the binding is that compare /// ([`check_attestation`]). +/// +/// `decode_commitment` needs no length prefix: [`Commitment`] is a fixed-size +/// `[u8; COMMITMENT_SIZE]`, so its boundary in the hash input is unambiguous. +/// Pages are self-delimiting too (count-prefixed, each entry a fixed +/// `u64` base + fixed-size `Commitment`). pub fn program_id( elf_bytes: &[u8], pc_start: u64, @@ -261,6 +266,11 @@ pub fn expected_program_id( /// i.e. the inner proof was not for `trusted_elf_bytes` as the consumer knows /// it. The caller must also have verified the outer proof against the pinned /// `recursion-.elf` with `opts = preset.options()`. +/// +/// This is the low-level primitive: it accepts any `opts`, including +/// [`MIN_PROOF_OPTIONS`], and is meant for diagnostics/tests that need that +/// escape hatch. Production consumers should go through +/// [`check_attestation_for_preset`] instead, which refuses `Preset::Min`. pub fn check_attestation( committed: &[u8], trusted_elf_bytes: &[u8], @@ -274,3 +284,26 @@ pub fn check_attestation( } Ok(Some(inner_public_output.to_vec())) } + +/// [`check_attestation`] gated on [`Preset`] instead of a raw [`ProofOptions`], +/// refusing `Preset::Min`: that preset (blowup=2, 1 query — [`MIN_PROOF_OPTIONS`]) +/// is intentionally insecure and exists only for cheap diagnostics. A real +/// consumer pinning its trust to `recursion-min.elf` would accept a 1-query +/// attestation as if it had 128-bit security. Diagnostics/benches that +/// legitimately need `Preset::Min` call [`check_attestation`] directly with +/// [`MIN_PROOF_OPTIONS`]. +pub fn check_attestation_for_preset( + committed: &[u8], + trusted_elf_bytes: &[u8], + preset: Preset, +) -> Result>, Error> { + if preset == Preset::Min { + return Err(Error::Recursion( + "Preset::Min (recursion-min.elf) is insecure (blowup=2, 1 query) and must not be \ + used as a production consumer's trust gate; call check_attestation directly with \ + MIN_PROOF_OPTIONS for diagnostics" + .to_string(), + )); + } + check_attestation(committed, trusted_elf_bytes, &preset.options()) +}