Prove-and-retire prover (Approach 1), per-table and batched

Makefile

@@ -73,8 +73,15 @@ RECURSION_VERIFIER_PRESETS := min blowup2 blowup4 blowup8
 # `continuation` feature: verify a multi-epoch ContinuationProof bundle instead
 # of a monolithic VmProof. Only the presets the benchmarks actually measure.
 RECURSION_CONT_PRESETS := min blowup2 blowup4
+# `batched` feature: verify a BatchedProof (one FRI per domain height) instead
+# of a monolithic VmProof.
+RECURSION_BATCHED_PRESETS := min blowup2
+# `owned` feature: the monolithic proof, deserialized instead of read in place.
+RECURSION_OWNED_PRESETS := blowup2
 RECURSION_VERIFIER_ARTIFACTS := $(addprefix $(RECURSION_ARTIFACTS_DIR)/recursion-, $(addsuffix .elf, $(RECURSION_VERIFIER_PRESETS))) \
-	$(addprefix $(RECURSION_ARTIFACTS_DIR)/recursion-cont-, $(addsuffix .elf, $(RECURSION_CONT_PRESETS)))
+	$(addprefix $(RECURSION_ARTIFACTS_DIR)/recursion-cont-, $(addsuffix .elf, $(RECURSION_CONT_PRESETS))) \
+	$(addprefix $(RECURSION_ARTIFACTS_DIR)/recursion-batched-, $(addsuffix .elf, $(RECURSION_BATCHED_PRESETS))) \
+	$(addprefix $(RECURSION_ARTIFACTS_DIR)/recursion-owned-, $(addsuffix .elf, $(RECURSION_OWNED_PRESETS)))
 
 # Override with: make ... SYSROOT_DIR=$HOME/.lambda-vm-sysroot
 # to install the sysroot in a user-writable location and avoid sudo.
@@ -248,6 +255,22 @@ $(RECURSION_ARTIFACTS_DIR)/recursion-cont-$(1).elf: FORCE | prepare-sysroot $(RE
 endef
 $(foreach preset,$(RECURSION_CONT_PRESETS),$(eval $(call recursion_cont_verifier_rule,$(preset))))
 
+# Batched variants: same crate, `batched` feature on top of the preset feature
+# -> recursion-batched-<preset>-bench -> recursion-batched-<preset>.elf.
+define recursion_batched_verifier_rule
+$(RECURSION_ARTIFACTS_DIR)/recursion-batched-$(1).elf: FORCE | prepare-sysroot $(RECURSION_ARTIFACTS_DIR)
+	$$(call build_guest_elf,$$(RECURSION_GUESTS_DIR)/recursion,recursion-batched-$(1)-bench,--features "batched $(1)")
+endef
+$(foreach preset,$(RECURSION_BATCHED_PRESETS),$(eval $(call recursion_batched_verifier_rule,$(preset))))
+
+# Owned variants: same crate and the same blob as the default guest, read via
+# one rkyv deserialize instead of in place.
+define recursion_owned_verifier_rule
+$(RECURSION_ARTIFACTS_DIR)/recursion-owned-$(1).elf: FORCE | prepare-sysroot $(RECURSION_ARTIFACTS_DIR)
+	$$(call build_guest_elf,$$(RECURSION_GUESTS_DIR)/recursion,recursion-owned-$(1)-bench,--features "owned $(1)")
+endef
+$(foreach preset,$(RECURSION_OWNED_PRESETS),$(eval $(call recursion_owned_verifier_rule,$(preset))))
+
 clean-asm:
 	-rm -rf $(ASM_ARTIFACTS_DIR)
 

bench_vs/lambda/recursion/Cargo.toml

@@ -21,6 +21,15 @@ blowup8 = []
 # memory-bounded inner prove) instead of a monolithic VmProof. Selects the
 # `recursion-cont-<preset>-bench` bins below.
 continuation = []
+# Orthogonal to the presets: verify a BatchedProof (one FRI per domain height
+# instead of one per table) instead of a monolithic VmProof. Selects the
+# `recursion-batched-<preset>-bench` bins below. Mutually exclusive with
+# `continuation` — main.rs guards it.
+batched = []
+# Orthogonal to the presets: verify the same monolithic VmProof as the default
+# guest, but deserialized into owned values instead of read in place. Exists to
+# price zero-copy against an owned copy in guest cycles.
+owned = []
 
 # 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
@@ -60,6 +69,21 @@ name = "recursion-cont-blowup4-bench"
 path = "src/main.rs"
 required-features = ["continuation", "blowup4"]
 
+[[bin]]
+name = "recursion-batched-min-bench"
+path = "src/main.rs"
+required-features = ["batched", "min"]
+
+[[bin]]
+name = "recursion-batched-blowup2-bench"
+path = "src/main.rs"
+required-features = ["batched", "blowup2"]
+
+[[bin]]
+name = "recursion-owned-blowup2-bench"
+path = "src/main.rs"
+required-features = ["owned", "blowup2"]
+
 [dependencies]
 lambda-vm-prover = { path = "../../../prover", default-features = false, features = [
     "profile-markers",

bench_vs/lambda/recursion/src/main.rs

@@ -53,6 +53,12 @@ compile_error!("select exactly one of the `min`/`blowup2`/`blowup4`/`blowup8` fe
     all(feature = "blowup4", feature = "blowup8"),
 ))]
 compile_error!("select exactly one of the `min`/`blowup2`/`blowup4`/`blowup8` features");
+#[cfg(any(
+    all(feature = "continuation", feature = "batched"),
+    all(feature = "continuation", feature = "owned"),
+    all(feature = "batched", feature = "owned"),
+))]
+compile_error!("`continuation`, `batched` and `owned` are mutually exclusive proof layouts");
 
 /// The build preset fixing the inner `ProofOptions` (see the module docs).
 #[cfg(feature = "min")]
@@ -88,7 +94,7 @@ pub fn main() -> ! {
     // not self-enforcing here.
     let options = PRESET.options();
 
-    #[cfg(not(feature = "continuation"))]
+    #[cfg(not(any(feature = "continuation", feature = "batched", feature = "owned")))]
     let attestation = lambda_vm_prover::recursion::verify_and_attest_blob(blob, &options)
         .expect("verify errored")
         .expect("inner proof failed verification");
@@ -98,6 +104,16 @@ pub fn main() -> ! {
         .expect("verify errored")
         .expect("inner continuation proof failed verification");
 
+    #[cfg(feature = "batched")]
+    let attestation = lambda_vm_prover::recursion::verify_batched_and_attest(blob, &options)
+        .expect("verify errored")
+        .expect("inner batched proof failed verification");
+
+    #[cfg(feature = "owned")]
+    let attestation = lambda_vm_prover::recursion::verify_owned_and_attest(blob, &options)
+        .expect("verify errored")
+        .expect("inner proof failed verification");
+
     lambda_vm_syscalls::syscalls::commit(&attestation);
     lambda_vm_syscalls::syscalls::sys_halt();
 }

bin/cli/Cargo.toml

@@ -5,6 +5,7 @@ edition = "2024"
 license.workspace = true
 
 [dependencies]
+serde_cbor = "0.11"
 executor = { path = "../../executor" }
 prover = { path = "../../prover", package = "lambda-vm-prover" }
 stark = { path = "../../crypto/stark" }
@@ -13,11 +14,19 @@ clap = { version = "4.3.10", features = ["derive"] }
 rkyv = { version = "0.8.10", default-features = false, features = ["alloc", "bytecheck", "aligned", "pointer_width_64"] }
 tempfile = "3"
 tikv-jemallocator = "0.6"
-tikv-jemalloc-ctl = { version = "0.6", features = ["stats"], optional = true }
+# No `stats` by default: that feature propagates to tikv-jemalloc-sys and builds
+# jemalloc with `--enable-stats`, i.e. counters on the malloc fast path, for every
+# binary. `keep_large_buffers_warm` needs only `raw`/`mallctl`; the heap tracker is
+# what needs the counters, and it is behind `jemalloc-stats`.
+tikv-jemalloc-ctl = { version = "0.6" }
+tikv-jemalloc-sys = "0.6"
 env_logger = "0.11"
+# Used by `keep_large_buffers_warm`, whose body is Linux-only — so a macOS build
+# will not catch its absence.
+log = "0.4"
 
 [features]
-jemalloc-stats = ["dep:tikv-jemalloc-ctl"]
+jemalloc-stats = ["tikv-jemalloc-ctl/stats"]
 disk-spill = ["prover/disk-spill"]
 instruments = ["prover/instruments", "stark/instruments"]
 # GPU profiling build (Nsight): CUDA prover + instruments spans + NVTX ranges.

bin/cli/examples/cmp_proofs.rs

@@ -0,0 +1,102 @@
+//! Compare two `VmProof` files table by table: `cmp_proofs A.proof B.proof`.
+//!
+//! A diagnostic for the streaming prover: which table, and which part of it,
+//! first departs from the monolithic prover's proof of the same execution.
+
+use std::os::unix::fs::FileExt;
+
+use prover::VmProof;
+
+fn read(path: &str) -> VmProof {
+    let file = std::fs::File::open(path).expect("open");
+    let len = file.metadata().expect("metadata").len() as usize;
+    let mut buf = rkyv::util::AlignedVec::<16>::with_capacity(len);
+    buf.resize(len, 0);
+    file.read_exact_at(&mut buf, 0).expect("read");
+    rkyv::from_bytes::<VmProof, rkyv::rancor::Error>(&buf).expect("deserialize")
+}
+
+fn main() {
+    let args: Vec<String> = std::env::args().collect();
+    let (a, b) = (read(&args[1]), read(&args[2]));
+    println!(
+        "tables: {} vs {}",
+        a.proof.proofs.len(),
+        b.proof.proofs.len()
+    );
+    println!(
+        "table_counts equal: {}",
+        format!("{:?}", a.table_counts) == format!("{:?}", b.table_counts)
+    );
+    println!("counts A: {:?}", a.table_counts);
+    println!("counts B: {:?}", b.table_counts);
+    println!(
+        "runtime_page_ranges equal: {}",
+        format!("{:?}", a.runtime_page_ranges) == format!("{:?}", b.runtime_page_ranges)
+    );
+    println!(
+        "num_private_input_pages: {} vs {}",
+        a.num_private_input_pages, b.num_private_input_pages
+    );
+    println!(
+        "public_output equal: {}",
+        a.public_output == b.public_output
+    );
+    let mut shown = 0;
+    for (i, (x, y)) in a.proof.proofs.iter().zip(b.proof.proofs.iter()).enumerate() {
+        let mut diffs = Vec::new();
+        if x.trace_length != y.trace_length {
+            diffs.push(format!(
+                "trace_length {} vs {}",
+                x.trace_length, y.trace_length
+            ));
+        }
+        if x.lde_trace_main_merkle_root != y.lde_trace_main_merkle_root {
+            diffs.push("main root".into());
+        }
+        if x.lde_trace_precomputed_merkle_root != y.lde_trace_precomputed_merkle_root {
+            diffs.push("precomputed root".into());
+        }
+        if x.lde_trace_aux_merkle_root != y.lde_trace_aux_merkle_root {
+            diffs.push("aux root".into());
+        }
+        if format!("{:?}", x.trace_ood_evaluations) != format!("{:?}", y.trace_ood_evaluations) {
+            diffs.push("ood".into());
+        }
+        if x.composition_poly_root != y.composition_poly_root {
+            diffs.push("composition root".into());
+        }
+        if x.fri_layers_merkle_roots != y.fri_layers_merkle_roots {
+            diffs.push("fri roots".into());
+        }
+        if x.fri_final_poly_coeffs != y.fri_final_poly_coeffs {
+            diffs.push("fri final".into());
+        }
+        if x.query_list.len() != y.query_list.len() {
+            diffs.push(format!(
+                "queries {} vs {}",
+                x.query_list.len(),
+                y.query_list.len()
+            ));
+        }
+        if !diffs.is_empty() && shown < 40 {
+            println!("table {i}: {}", diffs.join(", "));
+            shown += 1;
+        }
+    }
+    println!("(showing at most 40 differing tables)");
+    let main_diff: Vec<usize> = a
+        .proof
+        .proofs
+        .iter()
+        .zip(b.proof.proofs.iter())
+        .enumerate()
+        .filter(|(_, (x, y))| x.lde_trace_main_merkle_root != y.lde_trace_main_merkle_root)
+        .map(|(i, _)| i)
+        .collect();
+    println!(
+        "tables whose MAIN root differs ({}): {:?}",
+        main_diff.len(),
+        main_diff
+    );
+}