From c2c45df3bf87ec315b5b409fb95d0b799ecbd6c6 Mon Sep 17 00:00:00 2001 From: acentelles Date: Tue, 20 Oct 2026 20:14:19 +0100 Subject: [PATCH 01/22] perf(blake2): reuse packed Spongefish prefix compressions --- jolt-inlines/blake2/src/digest_adapter.rs | 35 +++++++++++++- jolt-inlines/blake2/src/exec.rs | 21 +++++--- jolt-inlines/blake2/src/lib.rs | 2 + jolt-inlines/blake2/src/sdk.rs | 57 ++++++++++++++++++++++ specs/recursion-guest.md | 58 +++++++++++++++++++---- 5 files changed, 156 insertions(+), 17 deletions(-) diff --git a/jolt-inlines/blake2/src/digest_adapter.rs b/jolt-inlines/blake2/src/digest_adapter.rs index 1d4ba6db67..d6d8cb2131 100644 --- a/jolt-inlines/blake2/src/digest_adapter.rs +++ b/jolt-inlines/blake2/src/digest_adapter.rs @@ -1,8 +1,8 @@ //! [`digest`] trait adapter over the inline Blake2b. //! //! `Digest`-generic consumers (Fiat-Shamir transcripts) get the same bytes as -//! the `blake2` crate's `Blake2b`, computed with one inline compress -//! per 128-byte block on a guest and in software on a host. +//! the `blake2` crate's `Blake2b`. Blocks use the inline on a guest +//! and software on a host; known Spongefish prefixes reuse constant states. use core::marker::PhantomData; @@ -111,4 +111,35 @@ mod tests { } } } + + #[test] + fn spongefish_prefixes_preserve_digest_parameters_and_streaming() { + for tag in 0..=3 { + for suffix_len in [0, 1, 64, 128, 129, 257] { + let mut data = vec![0; 128]; + data[127] = tag; + data.extend(input(suffix_len)); + // Every changed prefix byte must still affect the digest. + for changed_byte in 0..=128 { + if changed_byte < 128 { + data[changed_byte] ^= 0x80; + } + for split in [0, 63, 127, 128, data.len()] { + let mut ours = Blake2b::::new(); + ours.update(&data[..split]); + ours.update(&data[split..]); + assert_eq!(ours.finalize(), Blake2b512::digest(&data)); + + let mut short = Blake2b::::new(); + short.update(&data[..split]); + short.update(&data[split..]); + assert_eq!(short.finalize(), ReferenceBlake2b::::digest(&data)); + } + if changed_byte < 128 { + data[changed_byte] ^= 0x80; + } + } + } + } + } } diff --git a/jolt-inlines/blake2/src/exec.rs b/jolt-inlines/blake2/src/exec.rs index 7a29dae846..a7b99f5a62 100644 --- a/jolt-inlines/blake2/src/exec.rs +++ b/jolt-inlines/blake2/src/exec.rs @@ -1,9 +1,13 @@ use crate::{IV, SIGMA}; -pub fn execute_blake2b_compression(state: &mut [u64; 8], message_words: &[u64; 18]) { +pub const fn execute_blake2b_compression(state: &mut [u64; 8], message_words: &[u64; 18]) { let mut v = [0u64; 16]; - v[0..8].copy_from_slice(state); - v[8..16].copy_from_slice(&IV); + let mut i = 0; + while i < 8 { + v[i] = state[i]; + v[i + 8] = IV[i]; + i += 1; + } v[12] ^= message_words[16]; @@ -11,7 +15,9 @@ pub fn execute_blake2b_compression(state: &mut [u64; 8], message_words: &[u64; 1 v[14] = !v[14]; } - for s in SIGMA { + let mut round = 0; + while round < SIGMA.len() { + let s = SIGMA[round]; g( &mut v, 0, @@ -85,14 +91,17 @@ pub fn execute_blake2b_compression(state: &mut [u64; 8], message_words: &[u64; 1 message_words[s[14]], message_words[s[15]], ); + round += 1; } - for i in 0..8 { + let mut i = 0; + while i < 8 { state[i] ^= v[i] ^ v[i + 8]; + i += 1; } } -fn g(v: &mut [u64; 16], a: usize, b: usize, c: usize, d: usize, x: u64, y: u64) { +const fn g(v: &mut [u64; 16], a: usize, b: usize, c: usize, d: usize, x: u64, y: u64) { v[a] = v[a].wrapping_add(v[b]).wrapping_add(x); v[d] = (v[d] ^ v[a]).rotate_right(32); v[c] = v[c].wrapping_add(v[d]); diff --git a/jolt-inlines/blake2/src/lib.rs b/jolt-inlines/blake2/src/lib.rs index a698afc6e5..59ece8b7c4 100644 --- a/jolt-inlines/blake2/src/lib.rs +++ b/jolt-inlines/blake2/src/lib.rs @@ -14,6 +14,8 @@ pub mod digest_adapter; #[cfg(feature = "host")] pub mod exec; +#[cfg(not(feature = "host"))] +mod exec; #[cfg(feature = "host")] pub mod sequence_builder; diff --git a/jolt-inlines/blake2/src/sdk.rs b/jolt-inlines/blake2/src/sdk.rs index 01f9f16c1e..0d66777038 100644 --- a/jolt-inlines/blake2/src/sdk.rs +++ b/jolt-inlines/blake2/src/sdk.rs @@ -5,6 +5,10 @@ //! copies and fills lower to libc `memcpy`/`memset` calls that move data in //! sub-word accesses, each a multi-row sequence; the word paths below load //! and store whole aligned words. +//! +//! Known public Spongefish domain prefixes reuse precomputed compression +//! states. The high-level hasher therefore has content-dependent execution; +//! it is not a constant-time API. use crate::{ BLOCK_INPUT_SIZE_IN_BYTES, IV, MSG_BLOCK_LEN, PERSONA_SIZE_IN_BYTES, SALT_SIZE_IN_BYTES, STATE_VECTOR_LEN, @@ -16,6 +20,21 @@ const INITIAL_STATE: [u64; STATE_VECTOR_LEN] = { h[0] ^= 0x01010000 ^ (OUTPUT_SIZE as u64); h }; +// Spongefish starts each phase with 127 zero bytes and a domain byte. +// These are nonfinal blocks at counter 128, computed by the same compression +// function that executes the inline on the host. +const SPONGEFISH_PREFIX_STATES: [[u64; STATE_VECTOR_LEN]; 3] = { + let mut states = [INITIAL_STATE; 3]; + let mut tag = 0; + while tag < states.len() { + let mut block = [0; MSG_BLOCK_LEN + 2]; + block[MSG_BLOCK_LEN - 1] = (tag as u64) << 56; + block[MSG_BLOCK_LEN] = BLOCK_INPUT_SIZE_IN_BYTES as u64; + crate::exec::execute_blake2b_compression(&mut states[tag], &block); + tag += 1; + } + states +}; /// One compression input: 16 message words, the byte counter, and the final /// flag, laid out as the 18 consecutive words the inline reads. @@ -41,6 +60,12 @@ impl CompressionBlock { #[inline(always)] fn compress(&mut self, state: &mut [u64; STATE_VECTOR_LEN], is_final: bool) { + if !is_final && self.counter == BLOCK_INPUT_SIZE_IN_BYTES as u64 { + if let Some(prefix) = self.spongefish_prefix(state) { + *state = prefix; + return; + } + } self.final_flag = u64::from(is_final); // SAFETY: repr(C) lays out the 16 message words, the counter, and the // flag as exactly the 18 aligned words the inline reads. @@ -48,6 +73,30 @@ impl CompressionBlock { blake2b_compress(state.as_mut_ptr(), core::ptr::from_ref(self).cast::()); } } + + #[inline(always)] + fn spongefish_prefix( + &self, + state: &[u64; STATE_VECTOR_LEN], + ) -> Option<[u64; STATE_VECTOR_LEN]> { + let tag = match self.words[MSG_BLOCK_LEN - 1] { + 0 => 0, + 0x0100_0000_0000_0000 => 1, + 0x0200_0000_0000_0000 => 2, + _ => return None, + }; + // Inspect the packed words: a bytewise mask comparison costs more + // guest rows than the compression it saves. The complete initial + // state check excludes other digest lengths, salt and personalization. + let nonzero = self.words[..MSG_BLOCK_LEN - 1] + .iter() + .fold(0, |acc, word| acc | word); + let changed = state + .iter() + .zip(INITIAL_STATE) + .fold(0, |acc, (word, initial)| acc | (word ^ initial)); + (nonzero | changed == 0).then_some(SPONGEFISH_PREFIX_STATES[tag]) + } } const _: () = assert!(core::mem::size_of::() == (MSG_BLOCK_LEN + 2) * 8); @@ -551,6 +600,14 @@ mod params_tests { "new_with_params streaming mismatch: salt={salt:?}, persona={persona:?}, length={length}" ); } + for tag in 0..3 { + let mut input = [0; 192]; + input[127] = tag; + assert_eq!( + Blake2b::digest_with_params(salt, persona, &input), + reference_with_params(salt, persona, &input), + ); + } } } diff --git a/specs/recursion-guest.md b/specs/recursion-guest.md index d448b3a51d..2631ce36af 100644 --- a/specs/recursion-guest.md +++ b/specs/recursion-guest.md @@ -4,7 +4,7 @@ The recursion example executes Jolt's Akita verifier as a RISC-V guest: it verifies an inner Akita, field-inline proof and reports the verdict. The cost of interest is the guest's **total trace rows**, the length an outer proof of that execution would have to cover, including setup and proof decoding. The working -target is a Fibonacci inner proof below 2^26 rows; this revision is 11,924,024 +target is a Fibonacci inner proof below 2^26 rows; this revision is 11,158,718 rows above it (see [Measurements](#measurements)). This document records the mechanisms the guest uses, the trust they rely on, and where the rows go. @@ -205,10 +205,12 @@ companion; the last row traces a fresh proof at this revision. | Merge `main`: native Akita trace batching (#2012), Akita `d98400c5` (#175), fresh proof | 78,896,208 | | Akita review revisions of LayerZero-Labs/akita#186-#190 on Akita `main` `401e7972`, spongefish's own Blake2b sponge, lent-accumulator `signed_sum`, fresh proof | 79,348,402 | | Merge `main`: Akita `318c3221` (#193), unified trace rows (#1996), fallible chunked decode and live-entry residual tables, fresh proof (77,245,072 verification cycles) | 79,335,454 | -| **Merge `main`: Akita `cf95fd05` (BlockDigits dense commit, #236-#242), whole-table bytecode (#2030), fresh proof** (76,947,621 verification cycles) | **79,032,888** | +| Merge `main`: Akita `cf95fd05` (BlockDigits dense commit, #236-#242), whole-table bytecode (#2030), fresh proof (76,947,621 verification cycles) | 79,032,888 | +| **Packed-word recognition of constant BLAKE2b prefixes**, same inner proof (76,182,318 verification cycles) | **78,267,582** | The first row was rebuilt and re-measured from its archived sources and -reproduces its recorded numbers exactly. Input mode, which reads the setup +reproduces its recorded numbers exactly. At the #1911 baseline +(`125fa70aa`), input mode, which reads the setup from the guest input, accepts at 86,461,879 rows. A proof with one bit flipped in its Akita opening proof is rejected after 60,136,155 rows, inside the PCS verifier. @@ -219,14 +221,52 @@ fold (`verify_root`, 14.56M to 24.46M rows): its relation-matrix evaluation and direct setup-contribution scan run over the natively batched trace columns. The terminal checks are unchanged. -The last row's 452,194-row increase nets two measured effects, besides the -boot-time modulus binding. Replacing the +The review-revision increase from 78,896,208 to 79,348,402 rows nets two +measured effects, besides the boot-time modulus binding. Replacing the hand-written transcript sponge, which reused each phase's compressed mask block, with spongefish's sponge over the inline adapter costs about 1.16M rows, and the remaining review revisions save about 0.71M. The `signed_sum` accumulator guard -costs about 9,000 rows. Recovering the mask compressions through a digest that -recognizes the mask blocks cost more rows (0.36M) than it saved, because the -128-byte check runs bytewise in the guest. +costs about 9,000 rows. A prior recognizer for the mask blocks cost more rows (0.36M) than it +saved, because its 128-byte check ran bytewise in the guest. + +### Constant BLAKE2b prefixes (2026-10-20) + +Spongefish's three public domain masks are full 128-byte blocks. The SDK now +recognizes them after packing into sixteen words, and reuses their compression +outputs computed at compile time by the existing BLAKE2b implementation. The +fast path requires a nonfinal first block at counter 128, the complete +BLAKE2b-512 initial state, and an exact match of all message words. This preserves +all hash bytes, including final-block, shorter-digest, salt and personalization +semantics. Other blocks still use the inline; Spongefish itself is unchanged. +The high-level hash API has content-dependent execution, not a constant-time +contract. The prefixes optimized in recursion are public. + +A short squeeze-to-absorb-to-squeeze transition now needs four dynamic +compressions instead of seven. The complete verifier improvement is smaller: +**765,306 fewer rows, or 0.9683%**, on the same checksum-sealed inner proof. +Verification uses 931,381 fewer virtual instructions and 166,078 more ordinary +RV64IMAC instructions, accounting for the recognition overhead. Both the +baseline and candidate remain in the $2^{27}$ padded domain; this alone does +not reach the $2^{26}$ target. + +The same typed opening-tamper fixture still rejects without a panic: its total +trace falls from 60,136,155 to 59,512,842 rows (623,313 saved). Both source states +return 1 for the valid proof and 0 for the tampered proof. Fixture checksums +were verified unchanged after both candidate runs. + +The baseline was independently reproduced at `125fa70aa657e78bce49f58f701f2756d52a69da`, +with Akita `ee03aa30`. Both arms ran on a Linux AMD EPYC 7K62 host, Rust 1.95.0, +CI-profile host and release guest, embedded setup, the same inner proof, and +`RAYON_NUM_THREADS=1`. Separate guest target directories prevent cross-arm +artifact reuse. All 14 BLAKE2b nextest tests passed, including independent digest +compatibility and inline execution checks; formatting and both workspace Clippy +modes (`host`, `host,zk`) passed. This is a trace-count result, not a native +elapsed-time or outer recursive-proof measurement. + +The successor branch retains #1911's public recursion companion. Merging +current main's runtime-catalog policy (#2091) and Spongefish migration (#2095) +requires companion integration and fresh validation; these counts do not +represent that future merge. ## Levers not taken here @@ -260,7 +300,7 @@ recognizes the mask blocks cost more rows (0.36M) than it saved, because the ## Reproduction ```bash -export RAYON_NUM_THREADS=1 RUST_MIN_STACK=268435456 CARGO_BUILD_JOBS=1 +export RUST_LOG=info RAYON_NUM_THREADS=1 RUST_MIN_STACK=268435456 CARGO_BUILD_JOBS=1 cargo run --release -p recursion --features akita,field-inline,ntt-inline -- \ generate --example fibonacci --workdir /tmp/recursion cargo run --release -p recursion --features akita,field-inline,ntt-inline -- \ From cab29542adefeb486b8450c99e1d017b63f87703 Mon Sep 17 00:00:00 2001 From: Alberto Centelles Date: Thu, 22 Oct 2026 23:37:01 +0100 Subject: [PATCH 02/22] perf(recursion): forward Akita's factored compression-weight feature l3-compression-weights on jolt-akita, the recursion host and the recursion guest selects Akita's factored evaluation of the compression relation weights (same field values). Feature-off guests compile byte for byte as before: only Cargo feature tables and host-only code change. --- crates/jolt-akita/Cargo.toml | 3 +++ examples/recursion/Cargo.toml | 3 +++ examples/recursion/guest/Cargo.toml | 2 ++ examples/recursion/src/main.rs | 2 ++ 4 files changed, 10 insertions(+) diff --git a/crates/jolt-akita/Cargo.toml b/crates/jolt-akita/Cargo.toml index 1785cefc01..16e2ba36fc 100644 --- a/crates/jolt-akita/Cargo.toml +++ b/crates/jolt-akita/Cargo.toml @@ -22,6 +22,9 @@ keccak-inline = ["akita-pcs/keccak-inline"] # Enables field-inline schedule coverage alongside the prover's field profile. field-inline = [] profiling = ["parallel"] +# L3 recursion experiment (default off): Akita evaluates the compression +# relation weights by factor (same field values; see akita-types). +l3-compression-weights = ["akita-types/l3-compression-weights"] [dependencies] # Jolt keeps its own catalogs for Jolt-specific trace shapes; Akita's shipped diff --git a/examples/recursion/Cargo.toml b/examples/recursion/Cargo.toml index 48cc6a7f81..c244d8068f 100644 --- a/examples/recursion/Cargo.toml +++ b/examples/recursion/Cargo.toml @@ -19,6 +19,9 @@ akita = [ "dep:jolt-witness", "dep:tracer", ] +# L3 recursion experiment: the verifier guest (and the host's Akita) evaluate +# the compression relation weights by factor; same field values. +l3-compression-weights = ["akita", "jolt-akita/l3-compression-weights"] [dependencies] jolt-akita = { path = "../../crates/jolt-akita", optional = true } diff --git a/examples/recursion/guest/Cargo.toml b/examples/recursion/guest/Cargo.toml index f1c3c03498..efb15f66e5 100644 --- a/examples/recursion/guest/Cargo.toml +++ b/examples/recursion/guest/Cargo.toml @@ -24,6 +24,8 @@ hash-inlines = [ "jolt-akita?/blake2-inline", "jolt-akita?/keccak-inline", ] +# L3 recursion experiment: factorized compression-weight evaluation. +l3-compression-weights = ["akita", "jolt-akita/l3-compression-weights"] [package.metadata.cargo-machete] # The jolt-field edge selects the guest's field-inline arithmetic; generated diff --git a/examples/recursion/src/main.rs b/examples/recursion/src/main.rs index 71b1b6662c..247915575a 100644 --- a/examples/recursion/src/main.rs +++ b/examples/recursion/src/main.rs @@ -876,6 +876,8 @@ fn configured_recursion_program(memory_config: MemoryConfig) -> Program { program.add_guest_feature("ntt-inline"); program.add_guest_feature("fast-alloc"); program.add_guest_feature("hash-inlines"); + #[cfg(feature = "l3-compression-weights")] + program.add_guest_feature("l3-compression-weights"); program.set_memory_config(memory_config); program } From 7a72d0f143bc90501eae73e94defebf834904a75 Mon Sep 17 00:00:00 2001 From: acentelles Date: Fri, 23 Oct 2026 02:31:54 +0100 Subject: [PATCH 03/22] perf(recursion): turn factored compression weights on by default The recursion example enables l3-compression-weights by default. The feature forwards weakly (jolt-akita?/l3-compression-weights) and the host adds the guest feature only together with akita, so Dory builds are unchanged. --no-default-features turns it off. Host-side Cargo and cfg changes only. --- examples/recursion/Cargo.toml | 8 +++++--- examples/recursion/src/main.rs | 2 +- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/examples/recursion/Cargo.toml b/examples/recursion/Cargo.toml index c244d8068f..f1d1e5c8dd 100644 --- a/examples/recursion/Cargo.toml +++ b/examples/recursion/Cargo.toml @@ -19,9 +19,11 @@ akita = [ "dep:jolt-witness", "dep:tracer", ] -# L3 recursion experiment: the verifier guest (and the host's Akita) evaluate -# the compression relation weights by factor; same field values. -l3-compression-weights = ["akita", "jolt-akita/l3-compression-weights"] +# L3 compression-weight factoring, default on: with `akita`, the verifier +# guest (and the host's Akita) evaluate the compression relation weights by +# factor; same field values. Turn it off with --no-default-features. +default = ["l3-compression-weights"] +l3-compression-weights = ["jolt-akita?/l3-compression-weights"] [dependencies] jolt-akita = { path = "../../crates/jolt-akita", optional = true } diff --git a/examples/recursion/src/main.rs b/examples/recursion/src/main.rs index 247915575a..8f776390c5 100644 --- a/examples/recursion/src/main.rs +++ b/examples/recursion/src/main.rs @@ -876,7 +876,7 @@ fn configured_recursion_program(memory_config: MemoryConfig) -> Program { program.add_guest_feature("ntt-inline"); program.add_guest_feature("fast-alloc"); program.add_guest_feature("hash-inlines"); - #[cfg(feature = "l3-compression-weights")] + #[cfg(all(feature = "akita", feature = "l3-compression-weights"))] program.add_guest_feature("l3-compression-weights"); program.set_memory_config(memory_config); program From 987289c6f7a0026d544b7704e681bccac9e28f1f Mon Sep 17 00:00:00 2001 From: acentelles Date: Thu, 22 Oct 2026 23:32:46 +0100 Subject: [PATCH 04/22] perf(recursion): forward Akita's terminal quotient certificate feature Adds l2-terminal-quotient to jolt-akita (enabling akita-pcs's feature), the recursion host and the verifier guest, the host's guest-feature line, and a tamper-l2 tool for the rejection fixtures (quotient flip, noncanonical, extra, short, response flip). Feature-off guest sources are untouched. --- crates/jolt-akita/Cargo.toml | 4 + examples/recursion/Cargo.toml | 3 + examples/recursion/guest/Cargo.toml | 2 + examples/recursion/src/main.rs | 126 ++++++++++++++++++++++++++++ 4 files changed, 135 insertions(+) diff --git a/crates/jolt-akita/Cargo.toml b/crates/jolt-akita/Cargo.toml index 16e2ba36fc..e479bf12ea 100644 --- a/crates/jolt-akita/Cargo.toml +++ b/crates/jolt-akita/Cargo.toml @@ -21,6 +21,10 @@ ntt-inline = ["akita-pcs/ntt-inline"] keccak-inline = ["akita-pcs/keccak-inline"] # Enables field-inline schedule coverage alongside the prover's field profile. field-inline = [] +# L2 terminal quotient certificate (recursion lever, default off): the +# terminal A rows are checked at two points against a sent quotient, under +# Akita protocol identifier v7-l2tq1. +l2-terminal-quotient = ["akita-pcs/l2-terminal-quotient"] profiling = ["parallel"] # L3 recursion experiment (default off): Akita evaluates the compression # relation weights by factor (same field values; see akita-types). diff --git a/examples/recursion/Cargo.toml b/examples/recursion/Cargo.toml index f1d1e5c8dd..5bbb940205 100644 --- a/examples/recursion/Cargo.toml +++ b/examples/recursion/Cargo.toml @@ -24,6 +24,9 @@ akita = [ # factor; same field values. Turn it off with --no-default-features. default = ["l3-compression-weights"] l3-compression-weights = ["jolt-akita?/l3-compression-weights"] +# L2 terminal quotient certificate: the inner Akita proofs carry the terminal +# A-row quotient and the guest verifies it instead of the exact product. +l2-terminal-quotient = ["akita", "jolt-akita/l2-terminal-quotient"] [dependencies] jolt-akita = { path = "../../crates/jolt-akita", optional = true } diff --git a/examples/recursion/guest/Cargo.toml b/examples/recursion/guest/Cargo.toml index efb15f66e5..3a7c3950e9 100644 --- a/examples/recursion/guest/Cargo.toml +++ b/examples/recursion/guest/Cargo.toml @@ -18,6 +18,8 @@ akita = [ "dep:jolt-transcript", ] fast-alloc = ["jolt_sdk/guest-size-class-alloc"] +# L2 terminal quotient certificate (see the host feature). +l2-terminal-quotient = ["akita", "jolt-akita/l2-terminal-quotient"] hash-inlines = [ "jolt_sdk/blake2-inline", "jolt-transcript?/blake2-inline", diff --git a/examples/recursion/src/main.rs b/examples/recursion/src/main.rs index 8f776390c5..073c793589 100644 --- a/examples/recursion/src/main.rs +++ b/examples/recursion/src/main.rs @@ -115,6 +115,24 @@ enum Commands { #[arg(long)] output: PathBuf, }, + /// L2 lever: write a proof stream whose first inner Akita proof has its + /// terminal quotient or terminal response altered (rejection cases). + #[cfg(feature = "l2-terminal-quotient")] + TamperL2 { + #[arg(long)] + example: String, + #[arg(long)] + workdir: PathBuf, + #[arg(long)] + output: PathBuf, + /// quotient-flip, quotient-noncanonical, quotient-extra, + /// quotient-short or response-flip + #[arg(long)] + mode: String, + /// Bytes of the quotient at the end of the Akita proof body + #[arg(long)] + quotient_bytes: usize, + }, /// Generate proofs for guest programs Generate { /// Example to run (fibonacci or muldiv) @@ -874,6 +892,8 @@ fn configured_recursion_program(memory_config: MemoryConfig) -> Program { program.add_guest_feature("akita"); #[cfg(feature = "ntt-inline")] program.add_guest_feature("ntt-inline"); + #[cfg(feature = "l2-terminal-quotient")] + program.add_guest_feature("l2-terminal-quotient"); program.add_guest_feature("fast-alloc"); program.add_guest_feature("hash-inlines"); #[cfg(all(feature = "akita", feature = "l3-compression-weights"))] @@ -926,6 +946,101 @@ fn tamper_opening(guest: GuestProgram, workdir: &Path, output: &Path) { save_proof_data(guest, &tampered, output); } +/// Bincode's standard varint length prefix. +#[cfg(feature = "l2-terminal-quotient")] +fn push_varint_len(out: &mut Vec, len: usize) { + let len = len as u64; + if len < 251 { + out.push(len as u8); + } else if len <= u64::from(u16::MAX) { + out.push(251); + out.extend_from_slice(&(len as u16).to_le_bytes()); + } else if len <= u64::from(u32::MAX) { + out.push(252); + out.extend_from_slice(&(len as u32).to_le_bytes()); + } else { + out.push(253); + out.extend_from_slice(&len.to_le_bytes()); + } +} + +/// L2 rejection fixtures. The quotient is the last message of the Akita +/// proof body (after the terminal `z` payload), `quotient_bytes` long. +#[cfg(feature = "l2-terminal-quotient")] +fn tamper_l2( + guest: GuestProgram, + workdir: &Path, + output: &Path, + mode: &str, + quotient_bytes: usize, +) { + // p = 2^128 - 2^32 + 22537, little endian: a noncanonical encoding of 0. + const MODULUS_LE: [u8; 16] = [ + 9, 88, 0, 0, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, + ]; + const ATOM: usize = 16; + let bytes = load_proof_data(guest, workdir); + let mut offset = 0; + let _: GuestVerifierPreprocessing = read_record(&bytes, &mut offset).unwrap(); + let payloads: u32 = read_record(&bytes, &mut offset).unwrap(); + for _ in 0..payloads { + let _ = read_raw(&bytes, &mut offset).unwrap(); + } + let count: u32 = read_record(&bytes, &mut offset).unwrap(); + assert!(count > 0, "tamper fixture requires a proof"); + let mut tampered = bytes[..offset].to_vec(); + for index in 0..count { + let mut proof: GuestProof = read_record(&bytes, &mut offset).unwrap(); + let device: JoltDevice = read_record(&bytes, &mut offset).unwrap(); + if index == 0 { + let config = bincode::config::standard(); + let encoded = + bincode::serde::encode_to_vec(&proof.joint_opening_proof, config).unwrap(); + let body_len = proof.joint_opening_proof.backend_proof_body_size(); + let header_len = encoded.len() - body_len; + let mut length_prefix = Vec::new(); + push_varint_len(&mut length_prefix, body_len); + assert!( + encoded[..header_len].ends_with(&length_prefix), + "Akita batch proof layout is not selection, length, body" + ); + let selection_len = header_len - length_prefix.len(); + let mut body = encoded[header_len..].to_vec(); + assert!( + quotient_bytes > 0 + && quotient_bytes.is_multiple_of(ATOM) + && body.len() > quotient_bytes, + "quotient length" + ); + let start = body.len() - quotient_bytes; + info!("L2 tamper: body {body_len} bytes, quotient at {start}..{body_len}"); + match mode { + "quotient-flip" => body[start] ^= 1, + "quotient-noncanonical" => { + let last = body.len() - ATOM; + body[last..].copy_from_slice(&MODULUS_LE); + } + "quotient-extra" => body.extend_from_slice(&[0u8; ATOM]), + "quotient-short" => body.truncate(body.len() - ATOM), + "response-flip" => body[start - 1] ^= 1, + other => panic!("unknown tamper-l2 mode {other}"), + } + let mut rebuilt = encoded[..selection_len].to_vec(); + push_varint_len(&mut rebuilt, body.len()); + rebuilt.extend_from_slice(&body); + proof.joint_opening_proof = bincode::serde::decode_from_slice(&rebuilt, config) + .unwrap() + .0; + } + push_record(&mut tampered, &proof); + push_record(&mut tampered, &device); + } + assert_eq!(offset, bytes.len(), "trailing proof stream bytes"); + assert_eq!(check_data_integrity(&tampered).proof_count, count); + std::fs::create_dir(output).expect("fresh tampered proof directory"); + save_proof_data(guest, &tampered, output); +} + fn run_recursion_proof( guest: GuestProgram, run_config: RunConfig, @@ -1060,6 +1175,17 @@ fn main() { let guest = GuestProgram::from_str(example).expect("supported guest example"); tamper_opening(guest, workdir, output); } + #[cfg(feature = "l2-terminal-quotient")] + Some(Commands::TamperL2 { + example, + workdir, + output, + mode, + quotient_bytes, + }) => { + let guest = GuestProgram::from_str(example).expect("supported guest example"); + tamper_l2(guest, workdir, output, mode, *quotient_bytes); + } Some(Commands::Generate { example, workdir, From 68990a272e191fd026ab89f9d4867eb4d666ab16 Mon Sep 17 00:00:00 2001 From: acentelles Date: Fri, 23 Oct 2026 03:15:33 +0100 Subject: [PATCH 05/22] perf(recursion): turn the terminal quotient certificate on by default The recursion example enables l2-terminal-quotient by default next to l3-compression-weights. The feature forwards weakly (jolt-akita?/l2-terminal-quotient), and the host's guest-feature line, the tamper-l2 command and its helpers are compiled only together with akita, so Dory builds are unchanged and Akita builds prove and verify with the quotient certificate. --no-default-features turns both off. Host-side Cargo and cfg changes only. --- examples/recursion/Cargo.toml | 16 +++++++++------- examples/recursion/src/main.rs | 10 +++++----- 2 files changed, 14 insertions(+), 12 deletions(-) diff --git a/examples/recursion/Cargo.toml b/examples/recursion/Cargo.toml index 5bbb940205..7ae8659448 100644 --- a/examples/recursion/Cargo.toml +++ b/examples/recursion/Cargo.toml @@ -19,14 +19,16 @@ akita = [ "dep:jolt-witness", "dep:tracer", ] -# L3 compression-weight factoring, default on: with `akita`, the verifier -# guest (and the host's Akita) evaluate the compression relation weights by -# factor; same field values. Turn it off with --no-default-features. -default = ["l3-compression-weights"] +# L3 compression-weight factoring and the L2 terminal quotient certificate, +# both default on and both effective only with `akita`. L3: the verifier guest +# (and the host's Akita) evaluate the compression relation weights by factor; +# same field values. L2: the inner Akita proofs carry the terminal A-row +# quotient (protocol identifier v7-l2tq1) and the guest checks it at two +# points instead of the exact product. Turn both off with +# --no-default-features. +default = ["l3-compression-weights", "l2-terminal-quotient"] l3-compression-weights = ["jolt-akita?/l3-compression-weights"] -# L2 terminal quotient certificate: the inner Akita proofs carry the terminal -# A-row quotient and the guest verifies it instead of the exact product. -l2-terminal-quotient = ["akita", "jolt-akita/l2-terminal-quotient"] +l2-terminal-quotient = ["jolt-akita?/l2-terminal-quotient"] [dependencies] jolt-akita = { path = "../../crates/jolt-akita", optional = true } diff --git a/examples/recursion/src/main.rs b/examples/recursion/src/main.rs index 073c793589..5b186500a6 100644 --- a/examples/recursion/src/main.rs +++ b/examples/recursion/src/main.rs @@ -117,7 +117,7 @@ enum Commands { }, /// L2 lever: write a proof stream whose first inner Akita proof has its /// terminal quotient or terminal response altered (rejection cases). - #[cfg(feature = "l2-terminal-quotient")] + #[cfg(all(feature = "akita", feature = "l2-terminal-quotient"))] TamperL2 { #[arg(long)] example: String, @@ -892,7 +892,7 @@ fn configured_recursion_program(memory_config: MemoryConfig) -> Program { program.add_guest_feature("akita"); #[cfg(feature = "ntt-inline")] program.add_guest_feature("ntt-inline"); - #[cfg(feature = "l2-terminal-quotient")] + #[cfg(all(feature = "akita", feature = "l2-terminal-quotient"))] program.add_guest_feature("l2-terminal-quotient"); program.add_guest_feature("fast-alloc"); program.add_guest_feature("hash-inlines"); @@ -947,7 +947,7 @@ fn tamper_opening(guest: GuestProgram, workdir: &Path, output: &Path) { } /// Bincode's standard varint length prefix. -#[cfg(feature = "l2-terminal-quotient")] +#[cfg(all(feature = "akita", feature = "l2-terminal-quotient"))] fn push_varint_len(out: &mut Vec, len: usize) { let len = len as u64; if len < 251 { @@ -966,7 +966,7 @@ fn push_varint_len(out: &mut Vec, len: usize) { /// L2 rejection fixtures. The quotient is the last message of the Akita /// proof body (after the terminal `z` payload), `quotient_bytes` long. -#[cfg(feature = "l2-terminal-quotient")] +#[cfg(all(feature = "akita", feature = "l2-terminal-quotient"))] fn tamper_l2( guest: GuestProgram, workdir: &Path, @@ -1175,7 +1175,7 @@ fn main() { let guest = GuestProgram::from_str(example).expect("supported guest example"); tamper_opening(guest, workdir, output); } - #[cfg(feature = "l2-terminal-quotient")] + #[cfg(all(feature = "akita", feature = "l2-terminal-quotient"))] Some(Commands::TamperL2 { example, workdir, From 142bf1f96fe8fb182df650fe8c21398b9517ce55 Mon Sep 17 00:00:00 2001 From: acentelles Date: Fri, 23 Oct 2026 22:24:22 +0100 Subject: [PATCH 06/22] perf(field,transcript): word-sized Fp128 decoding and transcript scalars Adds the word-decode and word-transcript features: Fp128 proof elements are deserialized from fixed 16-byte tuples with register-sized accumulators, and transcript scalars can be absorbed as whole words. Both are off by default. --- crates/jolt-akita/Cargo.toml | 5 ++ crates/jolt-field/Cargo.toml | 4 + crates/jolt-field/src/solinas/fp128.rs | 16 ++++ .../src/solinas/fp128_word_decode.rs | 54 ++++++++++++ .../jolt-field/tests/fp128_word_encoding.rs | 70 +++++++++++++++ crates/jolt-transcript/Cargo.toml | 4 + crates/jolt-transcript/src/digest.rs | 16 +++- crates/jolt-transcript/src/legacy.rs | 42 ++++++--- .../jolt-transcript/tests/word_transcript.rs | 85 +++++++++++++++++++ examples/recursion/Cargo.toml | 5 ++ examples/recursion/guest/Cargo.toml | 4 + examples/recursion/src/main.rs | 6 ++ 12 files changed, 297 insertions(+), 14 deletions(-) create mode 100644 crates/jolt-field/src/solinas/fp128_word_decode.rs create mode 100644 crates/jolt-field/tests/fp128_word_encoding.rs create mode 100644 crates/jolt-transcript/tests/word_transcript.rs diff --git a/crates/jolt-akita/Cargo.toml b/crates/jolt-akita/Cargo.toml index e479bf12ea..b6b2c9c577 100644 --- a/crates/jolt-akita/Cargo.toml +++ b/crates/jolt-akita/Cargo.toml @@ -30,6 +30,11 @@ profiling = ["parallel"] # relation weights by factor (same field values; see akita-types). l3-compression-weights = ["akita-types/l3-compression-weights"] +# Byte-preserving recursion experiments, default off. +word-transcript = ["jolt-transcript/word-transcript"] +word-decode = ["jolt-field/word-decode"] +ont-static-base = ["akita-challenges/ont-static-base"] + [dependencies] # Jolt keeps its own catalogs for Jolt-specific trace shapes; Akita's shipped # catalogs do not cover this adapter's complete production and test grids. diff --git a/crates/jolt-field/Cargo.toml b/crates/jolt-field/Cargo.toml index fd01f80536..16f889127e 100644 --- a/crates/jolt-field/Cargo.toml +++ b/crates/jolt-field/Cargo.toml @@ -48,6 +48,10 @@ field-inline-guest = ["dep:jolt-riscv"] field-inline-guest-bn254 = ["field-inline-guest"] field-inline-guest-fp128 = ["field-inline-guest"] +# Byte-preserving recursion experiments, default off. +word-transcript = [] +word-decode = [] + [dev-dependencies] # The spine test's oracle field must satisfy `JoltField`, which requires # `Allocative` under the `allocative` feature; integration tests do not see diff --git a/crates/jolt-field/src/solinas/fp128.rs b/crates/jolt-field/src/solinas/fp128.rs index 2524409555..f830e696d4 100644 --- a/crates/jolt-field/src/solinas/fp128.rs +++ b/crates/jolt-field/src/solinas/fp128.rs @@ -1157,6 +1157,13 @@ impl CanonicalBytes for Fp128

{ assert_eq!(out.len(), Self::NUM_BYTES); out.copy_from_slice(&join(self.0).to_le_bytes()); } + + #[cfg(feature = "word-transcript")] + #[inline(always)] + fn to_bytes_be(&self, out: &mut [u8]) { + assert_eq!(out.len(), Self::NUM_BYTES); + out.copy_from_slice(&join(self.0).to_be_bytes()); + } } impl CanonicalEncoding for Fp128

{ @@ -1204,12 +1211,21 @@ impl CanonicalEncoding for Fp128

{ #[inline] fn from_scalar_challenge_bytes(bytes: &[u8]) -> Self { + #[cfg(feature = "word-transcript")] + if let Ok(array) = <[u8; 16]>::try_from(bytes) { + return Self::from_u128(u128::from_le_bytes(array)); + } Self::from_bytes_le_reduced(bytes) } } +#[cfg(not(feature = "word-decode"))] crate::impl_serde_bytes!(impl[const P: u128] Fp128

, 16); +#[cfg(feature = "word-decode")] +#[path = "fp128_word_decode.rs"] +mod word_decode; + impl WithAccumulator for Fp128

{ type Accumulator = Fp128Accumulator

; type SmallScalarAccumulator = Fp128SignedAccumulator

; diff --git a/crates/jolt-field/src/solinas/fp128_word_decode.rs b/crates/jolt-field/src/solinas/fp128_word_decode.rs new file mode 100644 index 0000000000..7165d8f9a6 --- /dev/null +++ b/crates/jolt-field/src/solinas/fp128_word_decode.rs @@ -0,0 +1,54 @@ +//! Fixed byte-tuple decoding with register-sized accumulators. + +use core::fmt::{Formatter, Result as FormatResult}; + +use serde::de::{Error, SeqAccess, Visitor}; +use serde::{Deserialize, Deserializer, Serialize, Serializer}; + +use super::Fp128; +use crate::{CanonicalBytes, CanonicalEncoding}; + +struct WordArrayVisitor; + +impl<'de> Visitor<'de> for WordArrayVisitor { + type Value = u128; + + fn expecting(&self, formatter: &mut Formatter) -> FormatResult { + formatter.write_str("an array of length 16") + } + + #[inline] + fn visit_seq>(self, mut seq: A) -> Result { + let mut lo = 0u64; + let mut hi = 0u64; + for i in 0..16 { + let byte = seq + .next_element::()? + .ok_or_else(|| Error::invalid_length(i, &self))?; + // Each shift is at most 56; every byte owns disjoint bits. + if i < 8 { + lo |= u64::from(byte) << (8 * i); + } else { + hi |= u64::from(byte) << (8 * (i - 8)); + } + } + Ok(u128::from(lo) | (u128::from(hi) << 64)) + } +} + +impl Serialize for Fp128

{ + fn serialize(&self, serializer: S) -> Result { + let mut bytes = [0u8; 16]; + self.to_bytes_le(&mut bytes); + bytes.serialize(serializer) + } +} + +impl<'de, const P: u128> Deserialize<'de> for Fp128

{ + fn deserialize>(deserializer: D) -> Result { + // Preserve the byte-tuple grammar, including its per-byte error order. + let value = deserializer.deserialize_tuple(16, WordArrayVisitor)?; + Self::from_u128_checked(value) + .ok_or_else(|| Error::custom("non-canonical field element encoding")) + } +} diff --git a/crates/jolt-field/tests/fp128_word_encoding.rs b/crates/jolt-field/tests/fp128_word_encoding.rs new file mode 100644 index 0000000000..f2c89d9a2c --- /dev/null +++ b/crates/jolt-field/tests/fp128_word_encoding.rs @@ -0,0 +1,70 @@ +#![expect(clippy::unwrap_used, reason = "tests construct canonical fixtures")] +#![cfg(feature = "solinas")] + +use jolt_field::solinas::Prime128OffsetA7F7 as Field; +use jolt_field::{CanonicalBytes, CanonicalEncoding}; + +const MODULUS: u128 = u128::MAX - (0xffff_a7f7 - 1); + +#[test] +fn word_canonical_tuple_boundaries_and_consumption() { + let config = bincode::config::standard(); + for value in [0, 1, (1u128 << 64) - 1, 1u128 << 64, MODULUS - 1] { + let mut input = value.to_le_bytes().to_vec(); + input.extend_from_slice(&[0xaa, 0xbb]); + let (field, consumed): (Field, usize) = + bincode::serde::decode_from_slice(&input, config).unwrap(); + assert_eq!(field.to_u128_checked(), Some(value)); + assert_eq!(consumed, 16); + assert_eq!( + bincode::serde::encode_to_vec(field, config).unwrap(), + value.to_le_bytes() + ); + let mut big_endian = [0u8; 16]; + field.to_bytes_be(&mut big_endian); + assert_eq!(big_endian, value.to_be_bytes()); + } + for value in [MODULUS, MODULUS + 1, u128::MAX] { + assert!( + bincode::serde::decode_from_slice::(&value.to_le_bytes(), config).is_err() + ); + } +} + +#[test] +fn word_truncated_and_single_bit_tuples() { + let config = bincode::config::standard(); + let input = [0u8; 16]; + for length in 0..16 { + assert!(bincode::serde::decode_from_slice::(&input[..length], config).is_err()); + } + // Every bit below the modulus is canonical, including the limb boundary. + for bit in 0..128 { + let value = 1u128 << bit; + let (field, consumed): (Field, usize) = + bincode::serde::decode_from_slice(&value.to_le_bytes(), config).unwrap(); + assert_eq!((field.to_u128_checked(), consumed), (Some(value), 16)); + } +} + +#[test] +fn word_scalar_challenge_lengths_and_reduction() { + assert_eq!( + Field::from_scalar_challenge_bytes(&[]).to_u128_checked(), + Some(0) + ); + assert_eq!( + Field::from_scalar_challenge_bytes(&[0x34, 0x12]).to_u128_checked(), + Some(0x1234) + ); + assert_eq!( + Field::from_scalar_challenge_bytes(&MODULUS.to_le_bytes()).to_u128_checked(), + Some(0) + ); + let mut wide = [0u8; 17]; + wide[16] = 1; + assert_eq!( + Field::from_scalar_challenge_bytes(&wide).to_u128_checked(), + Some(0xffff_a7f7) + ); +} diff --git a/crates/jolt-transcript/Cargo.toml b/crates/jolt-transcript/Cargo.toml index 345ca82425..6d78749092 100644 --- a/crates/jolt-transcript/Cargo.toml +++ b/crates/jolt-transcript/Cargo.toml @@ -27,6 +27,9 @@ transcript-poseidon = ["spongefish", "bn254", "dep:light-poseidon"] blake2-inline = ["dep:jolt-inlines-blake2", "jolt-inlines-blake2/digest"] +# Byte-preserving scalar buffering and encoding, default off. +word-transcript = ["jolt-field/word-transcript"] + [dependencies] jolt-inlines-blake2 = { workspace = true, optional = true } ark-bn254 = { workspace = true, optional = true } @@ -39,6 +42,7 @@ jolt-field = { path = "../jolt-field", default-features = false } rand = { workspace = true, features = ["std_rng"], optional = true } [dev-dependencies] +jolt-field = { path = "../jolt-field", default-features = false, features = ["solinas"] } criterion = { workspace = true } [[bench]] diff --git a/crates/jolt-transcript/src/digest.rs b/crates/jolt-transcript/src/digest.rs index ac0b73310f..f42da0b94b 100644 --- a/crates/jolt-transcript/src/digest.rs +++ b/crates/jolt-transcript/src/digest.rs @@ -185,9 +185,19 @@ where } fn challenge_scalar(&mut self) -> F { - let mut buf = [0u8; 16]; - self.challenge_bytes(&mut buf); - F::from_scalar_challenge_bytes(&buf) + #[cfg(feature = "word-transcript")] + { + // One scalar draw consumes one complete digest state transition. + let hash = self.round_hash(&[]); + self.update_state(hash); + F::from_scalar_challenge_bytes(hash.split_at(16).0) + } + #[cfg(not(feature = "word-transcript"))] + { + let mut buf = [0u8; 16]; + self.challenge_bytes(&mut buf); + F::from_scalar_challenge_bytes(&buf) + } } #[inline] diff --git a/crates/jolt-transcript/src/legacy.rs b/crates/jolt-transcript/src/legacy.rs index 0b765c222f..f5fc5928be 100644 --- a/crates/jolt-transcript/src/legacy.rs +++ b/crates/jolt-transcript/src/legacy.rs @@ -69,16 +69,31 @@ pub trait Transcript: Default + Sync + Send + 'static { /// /// [`append_values`]: Self::append_values fn append_scalars(&mut self, label: &'static [u8], values: &[F]) { - let mut message = Vec::with_capacity(32 + values.len() * F::NUM_BYTES); - message.extend_from_slice(&LabelWithCount(label, values.len() as u64).word()); - for value in values { - let start = message.len(); - message.resize(start + F::NUM_BYTES, 0); - let (_, encoded) = message.split_at_mut(start); - value.to_bytes_le(encoded); - encoded.reverse(); + #[cfg(feature = "word-transcript")] + { + let mut message = vec![0u8; 32 + values.len() * F::NUM_BYTES]; + let (head, body) = message.split_at_mut(32); + head.copy_from_slice(&LabelWithCount(label, values.len() as u64).word()); + if F::NUM_BYTES > 0 { + for (value, chunk) in values.iter().zip(body.chunks_exact_mut(F::NUM_BYTES)) { + value.to_bytes_be(chunk); + } + } + self.append_bytes(&message); + } + #[cfg(not(feature = "word-transcript"))] + { + let mut message = Vec::with_capacity(32 + values.len() * F::NUM_BYTES); + message.extend_from_slice(&LabelWithCount(label, values.len() as u64).word()); + for value in values { + let start = message.len(); + message.resize(start + F::NUM_BYTES, 0); + let (_, encoded) = message.split_at_mut(start); + value.to_bytes_le(encoded); + encoded.reverse(); + } + self.append_bytes(&message); } - self.append_bytes(&message); } /// Absorbs a domain label with a count followed by each value in order. @@ -156,8 +171,13 @@ impl AppendToTranscript for F { heap.resize(F::NUM_BYTES, 0); &mut heap }; - self.to_bytes_le(buf); - buf.reverse(); + #[cfg(feature = "word-transcript")] + self.to_bytes_be(buf); + #[cfg(not(feature = "word-transcript"))] + { + self.to_bytes_le(buf); + buf.reverse(); + } transcript.append_bytes(buf); } } diff --git a/crates/jolt-transcript/tests/word_transcript.rs b/crates/jolt-transcript/tests/word_transcript.rs new file mode 100644 index 0000000000..779e82f511 --- /dev/null +++ b/crates/jolt-transcript/tests/word_transcript.rs @@ -0,0 +1,85 @@ +#![expect(clippy::unwrap_used, reason = "tests construct canonical fixtures")] +use jolt_field::solinas::Prime128OffsetA7F7 as Field; +use jolt_field::CanonicalEncoding; +use jolt_transcript::{AppendToTranscript, Transcript}; + +#[derive(Default)] +struct Capture { + messages: Vec>, +} + +impl Transcript for Capture { + type Challenge = (); + + fn new(_: &'static [u8]) -> Self { + Self::default() + } + + fn append_bytes(&mut self, bytes: &[u8]) { + self.messages.push(bytes.to_vec()); + } + + fn challenge(&mut self) {} + + fn state(&self) -> [u8; 32] { + [0; 32] + } +} + +#[test] +fn word_scalar_message_matches_wire_contract() { + let value = Field::from_u128_checked(0x0102_0304_0506_0708_1112_1314_1516_1718).unwrap(); + let mut transcript = Capture::default(); + transcript.append_scalars(b"x", &[value]); + let mut expected = vec![0; 48]; + expected[0] = b'x'; + expected[31] = 1; + expected[32..].copy_from_slice(&[1, 2, 3, 4, 5, 6, 7, 8, 17, 18, 19, 20, 21, 22, 23, 24]); + assert_eq!(transcript.messages, vec![expected]); + + let mut scalar = Capture::default(); + value.append_to_transcript(&mut scalar); + assert_eq!( + scalar.messages, + vec![vec![1, 2, 3, 4, 5, 6, 7, 8, 17, 18, 19, 20, 21, 22, 23, 24,]] + ); +} + +#[test] +fn word_empty_and_multiple_scalars_keep_one_message() { + let mut empty = Capture::default(); + empty.append_scalars::(b"", &[]); + assert_eq!(empty.messages, vec![vec![0; 32]]); + + let mut transcript = Capture::default(); + let values = [ + Field::from_u128_checked(0).unwrap(), + Field::from_u128_checked(1).unwrap(), + ]; + transcript.append_scalars(b"", &values); + let mut expected = vec![0; 64]; + expected[31] = 2; + expected[63] = 1; + assert_eq!(transcript.messages, vec![expected]); +} + +#[cfg(feature = "transcript-blake2b")] +#[test] +fn word_scalar_draw_matches_existing_independent_digest_vector() { + use jolt_transcript::LegacyBlake2bTranscript; + + let mut transcript = LegacyBlake2bTranscript::::new(b"jolt transcript kat"); + transcript.append_bytes(b"jolt says hello"); + // Same independent hashlib vector as legacy_digest_tests.rs. + let state = [ + 0x25, 0xa4, 0x96, 0x91, 0x2b, 0x5b, 0x75, 0xd6, 0x50, 0x4c, 0xbc, 0x20, 0x4a, 0x25, 0xb1, + 0x3d, 0x61, 0x21, 0xe6, 0x26, 0x6a, 0xc0, 0x56, 0x58, 0x96, 0x89, 0xc4, 0x3d, 0xc0, 0x6f, + 0x91, 0x42, + ]; + let challenge = transcript.challenge_scalar(); + assert_eq!(transcript.state(), state); + assert_eq!( + challenge.to_u128_checked(), + Some(0x3db1_254a_20bc_4c50_d675_5b2b_9196_a425) + ); +} diff --git a/examples/recursion/Cargo.toml b/examples/recursion/Cargo.toml index 7ae8659448..c016f69641 100644 --- a/examples/recursion/Cargo.toml +++ b/examples/recursion/Cargo.toml @@ -30,6 +30,11 @@ default = ["l3-compression-weights", "l2-terminal-quotient"] l3-compression-weights = ["jolt-akita?/l3-compression-weights"] l2-terminal-quotient = ["jolt-akita?/l2-terminal-quotient"] +# Each arm is selected independently and forwarded to the guest. +word-transcript = ["akita", "jolt-akita/word-transcript"] +word-decode = ["akita", "jolt-akita/word-decode"] +ont-static-base = ["akita", "jolt-akita/ont-static-base"] + [dependencies] jolt-akita = { path = "../../crates/jolt-akita", optional = true } jolt-program = { path = "../../crates/jolt-program", optional = true } diff --git a/examples/recursion/guest/Cargo.toml b/examples/recursion/guest/Cargo.toml index 3a7c3950e9..c09cdd2f89 100644 --- a/examples/recursion/guest/Cargo.toml +++ b/examples/recursion/guest/Cargo.toml @@ -29,6 +29,10 @@ hash-inlines = [ # L3 recursion experiment: factorized compression-weight evaluation. l3-compression-weights = ["akita", "jolt-akita/l3-compression-weights"] +word-transcript = ["akita", "jolt-akita/word-transcript"] +word-decode = ["akita", "jolt-akita/word-decode"] +ont-static-base = ["akita", "jolt-akita/ont-static-base"] + [package.metadata.cargo-machete] # The jolt-field edge selects the guest's field-inline arithmetic; generated # embedded_bytecode.rs imports jolt-riscv types when the host prepares an diff --git a/examples/recursion/src/main.rs b/examples/recursion/src/main.rs index 5b186500a6..76303fa204 100644 --- a/examples/recursion/src/main.rs +++ b/examples/recursion/src/main.rs @@ -898,6 +898,12 @@ fn configured_recursion_program(memory_config: MemoryConfig) -> Program { program.add_guest_feature("hash-inlines"); #[cfg(all(feature = "akita", feature = "l3-compression-weights"))] program.add_guest_feature("l3-compression-weights"); + #[cfg(feature = "word-transcript")] + program.add_guest_feature("word-transcript"); + #[cfg(feature = "word-decode")] + program.add_guest_feature("word-decode"); + #[cfg(feature = "ont-static-base")] + program.add_guest_feature("ont-static-base"); program.set_memory_config(memory_config); program } From 8e8ec596d6917bfe5d88b68e14b20cd332b026b8 Mon Sep 17 00:00:00 2001 From: acentelles Date: Sat, 24 Oct 2026 00:57:21 +0100 Subject: [PATCH 07/22] Define canonical big-endian bytes for transcript feature callers --- crates/jolt-field/src/algebra.rs | 11 +++++++ .../tests/canonical_bytes_big_endian.rs | 32 +++++++++++++++++++ 2 files changed, 43 insertions(+) create mode 100644 crates/jolt-field/tests/canonical_bytes_big_endian.rs diff --git a/crates/jolt-field/src/algebra.rs b/crates/jolt-field/src/algebra.rs index b969daf799..77350f6904 100644 --- a/crates/jolt-field/src/algebra.rs +++ b/crates/jolt-field/src/algebra.rs @@ -345,6 +345,17 @@ pub trait CanonicalBytes { /// Writes the canonical little-endian encoding into `out`. fn to_bytes_le(&self, out: &mut [u8]); + /// Writes the canonical encoding in big-endian byte order into `out`. + /// + /// `out` must have length [`NUM_BYTES`](Self::NUM_BYTES). This is the + /// byte reversal of [`to_bytes_le`](Self::to_bytes_le), including for + /// non-field encodings. + #[inline] + fn to_bytes_be(&self, out: &mut [u8]) { + self.to_bytes_le(out); + out.reverse(); + } + /// Returns the canonical little-endian encoding as a vector. #[inline] fn to_bytes_le_vec(&self) -> Vec { diff --git a/crates/jolt-field/tests/canonical_bytes_big_endian.rs b/crates/jolt-field/tests/canonical_bytes_big_endian.rs new file mode 100644 index 0000000000..b931721700 --- /dev/null +++ b/crates/jolt-field/tests/canonical_bytes_big_endian.rs @@ -0,0 +1,32 @@ +use jolt_field::CanonicalBytes; + +struct LittleEndianBytes([u8; N]); + +impl CanonicalBytes for LittleEndianBytes { + const NUM_BYTES: usize = N; + + fn to_bytes_le(&self, out: &mut [u8]) { + out.copy_from_slice(&self.0); + } +} + +fn write_big_endian(value: &T, out: &mut [u8]) { + value.to_bytes_be(out); +} + +#[test] +fn canonical_bytes_default_big_endian_matches_wire_order() { + let value = LittleEndianBytes([0x78, 0x56, 0x34, 0x12]); + let mut out = [0u8; 4]; + write_big_endian(&value, &mut out); + assert_eq!(out, [0x12, 0x34, 0x56, 0x78]); + assert_eq!(value.to_bytes_le_vec(), [0x78, 0x56, 0x34, 0x12]); +} + +#[test] +fn canonical_bytes_default_big_endian_accepts_empty_encoding() { + let value = LittleEndianBytes([]); + let mut out = []; + write_big_endian(&value, &mut out); + assert!(out.is_empty()); +} From e79d6d922f44188511316e4c0c28303468983f3d Mon Sep 17 00:00:00 2001 From: acentelles Date: Sat, 24 Oct 2026 10:10:14 +0100 Subject: [PATCH 08/22] Gate Solinas encoding tests before lint expectations --- crates/jolt-field/tests/fp128_word_encoding.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/jolt-field/tests/fp128_word_encoding.rs b/crates/jolt-field/tests/fp128_word_encoding.rs index f2c89d9a2c..79032f1d41 100644 --- a/crates/jolt-field/tests/fp128_word_encoding.rs +++ b/crates/jolt-field/tests/fp128_word_encoding.rs @@ -1,5 +1,5 @@ -#![expect(clippy::unwrap_used, reason = "tests construct canonical fixtures")] #![cfg(feature = "solinas")] +#![expect(clippy::unwrap_used, reason = "tests construct canonical fixtures")] use jolt_field::solinas::Prime128OffsetA7F7 as Field; use jolt_field::{CanonicalBytes, CanonicalEncoding}; From c0722ae6e37f108fc893eb598ada60bc7b112c5a Mon Sep 17 00:00:00 2001 From: acentelles Date: Sat, 24 Oct 2026 16:52:12 +0100 Subject: [PATCH 09/22] perf(recursion): turn word decoding on by default The recursion example enables word-decode by default next to the factored compression weights and the terminal quotient certificate. The feature forwards weakly (jolt-akita?/word-decode) and the host forwards it to the guest only together with akita, so Dory builds are unchanged. --no-default-features turns all three off. Host-side Cargo and cfg changes only. --- examples/recursion/Cargo.toml | 11 ++++++----- examples/recursion/src/main.rs | 2 +- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/examples/recursion/Cargo.toml b/examples/recursion/Cargo.toml index c016f69641..22aacf840e 100644 --- a/examples/recursion/Cargo.toml +++ b/examples/recursion/Cargo.toml @@ -24,15 +24,16 @@ akita = [ # (and the host's Akita) evaluate the compression relation weights by factor; # same field values. L2: the inner Akita proofs carry the terminal A-row # quotient (protocol identifier v7-l2tq1) and the guest checks it at two -# points instead of the exact product. Turn both off with -# --no-default-features. -default = ["l3-compression-weights", "l2-terminal-quotient"] +# points instead of the exact product. Word decoding: the guest decodes +# fixed-wire field elements by word with the same canonicality checks. Turn +# all three off with --no-default-features. +default = ["l3-compression-weights", "l2-terminal-quotient", "word-decode"] l3-compression-weights = ["jolt-akita?/l3-compression-weights"] l2-terminal-quotient = ["jolt-akita?/l2-terminal-quotient"] +word-decode = ["jolt-akita?/word-decode"] -# Each arm is selected independently and forwarded to the guest. +# Each remaining arm is selected independently and forwarded to the guest. word-transcript = ["akita", "jolt-akita/word-transcript"] -word-decode = ["akita", "jolt-akita/word-decode"] ont-static-base = ["akita", "jolt-akita/ont-static-base"] [dependencies] diff --git a/examples/recursion/src/main.rs b/examples/recursion/src/main.rs index 76303fa204..7c5938b582 100644 --- a/examples/recursion/src/main.rs +++ b/examples/recursion/src/main.rs @@ -900,7 +900,7 @@ fn configured_recursion_program(memory_config: MemoryConfig) -> Program { program.add_guest_feature("l3-compression-weights"); #[cfg(feature = "word-transcript")] program.add_guest_feature("word-transcript"); - #[cfg(feature = "word-decode")] + #[cfg(all(feature = "akita", feature = "word-decode"))] program.add_guest_feature("word-decode"); #[cfg(feature = "ont-static-base")] program.add_guest_feature("ont-static-base"); From c14ac93d87463a1ab4c193e107d9734405180bba Mon Sep 17 00:00:00 2001 From: acentelles Date: Sat, 24 Oct 2026 00:56:01 +0100 Subject: [PATCH 10/22] perf(verifier): reuse instruction read RAF public inputs --- crates/jolt-verifier/src/stages/relations.rs | 48 ++-- .../src/stages/stage5/instruction_read_raf.rs | 213 +++++++++++++----- 2 files changed, 191 insertions(+), 70 deletions(-) diff --git a/crates/jolt-verifier/src/stages/relations.rs b/crates/jolt-verifier/src/stages/relations.rs index 07fee6a527..63fe2b6748 100644 --- a/crates/jolt-verifier/src/stages/relations.rs +++ b/crates/jolt-verifier/src/stages/relations.rs @@ -91,9 +91,9 @@ pub type ChallengeIdOf = as SymbolicSumcheck>::Challenge /// its proof) and the verifier (after checking it). /// /// Each relation's consumed/produced claims are split into a *Values* form (the -/// serialized wire form, the cell-generic claim struct at `F` — one value per +/// serialized wire form, the cell-generic claim struct at `F` -- one value per /// opening) and a *Points* form (the derived opening points, the same struct at -/// `Vec` — one point per opening). Methods that need only points +/// `Vec` -- one point per opening). Methods that need only points /// ([`derive_opening_points`](Self::derive_opening_points), /// [`derive_output_term`](Self::derive_output_term)) take the Points forms and run /// in both modes; methods that read values ([`input_claim`](Self::input_claim), @@ -112,7 +112,7 @@ where /// The relation's pure symbolic algebra: id types, sumcheck spec, and the /// input/output `Expr`s. The concrete instance holds its `Self::Symbolic` and /// sources its claim expressions and spec from it. The id family is the - /// symbolic relation's own — every id this trait exposes is a projection of + /// symbolic relation's own -- every id this trait exposes is a projection of /// it, so relations from any protocol family (jolt, field-inline) implement /// one trait. type Symbolic: SymbolicSumcheck; @@ -137,17 +137,17 @@ where /// /// The default draws one `challenge_scalar` per `Challenges` field, in /// declaration order, via [`SumcheckChallenges::from_transcript_values`]. This is - /// the correct draw for the common case — a relation whose challenges are each a + /// the correct draw for the common case -- a relation whose challenges are each a /// single `challenge_scalar` (and for [`NoChallenges`](::jolt_claims::NoChallenges), /// which has no fields, it draws nothing). A `challenge_scalar_powers(n)` draw /// reduces to this case: it performs exactly one squeeze and the relation keeps /// the degree-1 power, which equals that squeezed scalar. Only relations whose - /// draw is genuinely different — an extra transcript append (a domain + /// draw is genuinely different -- an extra transcript append (a domain /// separator), a value re-roll, or a powers draw whose kept value is not the - /// squeezed scalar — override this. + /// squeezed scalar -- override this. /// - /// The bound is `SumcheckChallenges` — which every `Challenges` already - /// implements — so the default needs no separate `Default` derive. It errors + /// The bound is `SumcheckChallenges` -- which every `Challenges` already + /// implements -- so the default needs no separate `Default` derive. It errors /// only if the per-field draw cannot populate the struct, which cannot happen for /// the infinite `challenge_scalar` stream the default supplies. fn draw_challenges>( @@ -169,7 +169,7 @@ where /// the generated drivers use this set three ways: the absorb skips the aliased /// ids, the shape/count arithmetic subtracts them (see /// [`wire_output_openings`](Self::wire_output_openings)), and the generated - /// `validate_aliases` — run by every `expected_final_claim` — enforces the + /// `validate_aliases` -- run by every `expected_final_claim` -- enforces the /// wire copies equal their sources. That equality check is load-bearing: the /// aliased cells are never Fiat-Shamir-absorbed and the batch fold pins only /// their random linear combination, so downstream consumers reading a copy @@ -180,7 +180,7 @@ where /// /// Point equality is NOT checked at runtime: opening points are derived (not /// wire data), and an alias is only declarable when both relations bind the - /// same batch-point slice and derive it identically — a structural invariant. + /// same batch-point slice and derive it identically -- a structural invariant. /// The declaration invariants (each aliased id owned + `Expr`-referenced by /// the declaring relation, each source absorbed by another member binding an /// identical point slice) are pinned by hand-written tests in each declaring @@ -276,7 +276,7 @@ where /// Resolve a `Derived` in this relation's **output** expression: from the input /// points, the produced openings' points (the bound point, post-binding), and the /// drawn challenges. The output claim is checked *after* binding, so the produced - /// openings' points exist — hence `output_points` is non-optional. Most `eq`/`lt` + /// openings' points exist -- hence `output_points` is non-optional. Most `eq`/`lt` /// deriveds live here (they evaluate at this sumcheck's bound point). Defaults to /// "no output deriveds"; overridden by relations that have them. fn derive_output_term( @@ -325,6 +325,20 @@ where output_values: &SumcheckOutputClaims, output_points: &SumcheckOutputPoints, challenges: &ConcreteSumcheckChallenges, + ) -> Result { + self.evaluate_output_expression(output_values, challenges, |id| { + self.derive_output_term(id, input_points, output_points, challenges) + }) + } + + /// Evaluate the canonical output expression with a per-call derived-value + /// resolver. Relations can share public computations across terms without + /// restating the expression or changing opening and challenge resolution. + fn evaluate_output_expression( + &self, + output_values: &SumcheckOutputClaims, + challenges: &ConcreteSumcheckChallenges, + derived: impl FnMut(&DerivedIdOf) -> Result, ) -> Result { self.symbolic().output_expression::().try_evaluate( |id| { @@ -337,7 +351,7 @@ where .resolve_challenge(id) .ok_or(VerifierError::MissingStageClaimChallenge { id: (*id).into() }) }, - |id| self.derive_output_term(id, input_points, output_points, challenges), + derived, ) } } @@ -423,7 +437,7 @@ where /// Enforce one member's declared cross-relation opening aliases: each aliased /// wire cell (resolved from the DECLARING member's claims) must equal its /// canonical source opening, resolved across the batch by `resolve_source` -/// (the generated batch-wide resolver). Load-bearing — aliased cells are never +/// (the generated batch-wide resolver). Load-bearing -- aliased cells are never /// Fiat-Shamir absorbed and the batch fold pins only their random linear /// combination, so downstream consumers reading a copy rely on this equality. /// Called by the generated `validate_aliases` per member. @@ -502,7 +516,7 @@ where Ok(()) } -/// Project a composite-family derived id onto one relation's own public enum — +/// Project a composite-family derived id onto one relation's own public enum -- /// the typed destructure every `derive_output_term` starts with, driven by the /// id family's generated `TryFrom` inverses of its `From` embeddings. A foreign /// relation's id is the same `MissingStageClaimDerived` miss the hand-written @@ -1262,7 +1276,7 @@ mod sumcheck_batch_derive_tests { // NO `draw_challenges` on the source struct (a stage whose member challenges // have stage-level provenance hand-assembles its aggregate; the generated draw // would squeeze at the wrong transcript position if it existed). The inherent - // `draw_challenges` below — with a deliberately incompatible signature — would + // `draw_challenges` below -- with a deliberately incompatible signature -- would // collide with a generated one, so this module compiling at all proves the // opt-out suppressed it. #[derive(SumcheckBatch)] @@ -1320,9 +1334,9 @@ mod begin_batch_tests { } /// `begin_batch` with a clear recorder must reproduce the exact head - /// Fiat-Shamir sequence `verify_clear` performed before the factoring — + /// Fiat-Shamir sequence `verify_clear` performed before the factoring -- /// per-member `input_claim` absorbed under `b"sumcheck_claim"` in - /// declaration order, then one coefficient squeeze per member — and pack + /// declaration order, then one coefficient squeeze per member -- and pack /// the prelude's engine and named views consistently. #[test] fn begin_batch_matches_head_replica_and_packs_prelude() { diff --git a/crates/jolt-verifier/src/stages/stage5/instruction_read_raf.rs b/crates/jolt-verifier/src/stages/stage5/instruction_read_raf.rs index 1b9f7abc98..3d73fa6c7e 100644 --- a/crates/jolt-verifier/src/stages/stage5/instruction_read_raf.rs +++ b/crates/jolt-verifier/src/stages/stage5/instruction_read_raf.rs @@ -101,10 +101,86 @@ pub(crate) fn reconstruct_r_address( .collect() } +struct InstructionReadRafPublicInputs { + r_address: Vec, + eq_reduction: F, +} + impl InstructionReadRaf { pub fn dimensions(&self) -> InstructionReadRafDimensions { self.dimensions } + + fn prepare_output( + &self, + input_points: &InstructionReadRafInputClaims>, + output_points: &InstructionReadRafOutputClaims>, + ) -> Result, VerifierError> { + let r_cycle = output_points.instruction_raf_flag(); + let r_address = reconstruct_r_address(output_points, r_cycle.len()); + // eq over the upstream instruction claim-reduction cycle point; all three + // consumed openings share that point, so the lookup-output input carries it. + let eq_reduction = + try_eq_mle(input_points.lookup_output(), r_cycle).map_err(public_input_failed)?; + let address_bits = self.dimensions.instruction_address_bits(); + // `upper_half_all_ones` below slices the leading half of this point, so a + // reconstruction of the wrong length would silently guard the wrong bits + // rather than fail. The point is verifier-derived, but the mis-slice is + // invisible if that ever stops being true. + if r_address.len() != address_bits { + return Err(public_input_failed(format!( + "instruction address point has {} coordinates, expected {address_bits}", + r_address.len() + ))); + } + Ok(InstructionReadRafPublicInputs { + r_address, + eq_reduction, + }) + } + + fn evaluate_public( + &self, + public: &InstructionReadRafPublic, + prepared: &InstructionReadRafPublicInputs, + challenges: &InstructionReadRafChallenges, + ) -> Result { + let address_bits = self.dimensions.instruction_address_bits(); + let r_address = &prepared.r_address; + let eq_reduction = prepared.eq_reduction; + let left = || OperandPolynomial::new(address_bits, OperandSide::Left).evaluate(r_address); + let right = || OperandPolynomial::new(address_bits, OperandSide::Right).evaluate(r_address); + let gamma = challenges.gamma; + let gamma2 = gamma * gamma; + match public { + InstructionReadRafPublic::EqTableValue(index) => { + let table = LookupTableKind::::iter() + .find(|table| table.index() == *index) + .ok_or_else(|| { + public_input_failed(format!("unknown lookup table index {index}")) + })?; + Ok(eq_reduction * table.evaluate_mle::(r_address)) + } + InstructionReadRafPublic::EqRafConstant => { + Ok(eq_reduction * (gamma * left() + gamma2 * right())) + } + InstructionReadRafPublic::EqRafFlag => { + let identity = IdentityPolynomial::new(address_bits).evaluate(r_address); + let mut raf = gamma2 * identity - gamma * left() - gamma2 * right(); + if CANONICAL_INSTRUCTION_ADDRESS { + // The input claim carries no γ³ term, so the sumcheck can only + // close if Σ_j eq(r_red,j)·RafFlag_j·U(k_j) = 0 -- i.e. no + // identity-RAF cycle has an all-ones upper address half. Every + // fp128 alias `k = r + p < 2^128` has exactly that shape, and + // `U(k) = 0` implies `k < 2^128 - 2^64 < p`, so the surviving + // address is the canonical representative of `k mod p` and the + // identity leg pins it exactly. See `CANONICAL_INSTRUCTION_ADDRESS`. + raf += gamma2 * gamma * upper_half_all_ones(r_address); + } + Ok(eq_reduction * raf) + } + } + } } impl ConcreteSumcheck for InstructionReadRaf { @@ -161,60 +237,33 @@ impl ConcreteSumcheck for InstructionReadRaf { let JoltDerivedId::InstructionReadRaf(public) = id else { return Err(VerifierError::MissingStageClaimDerived { id: (*id).into() }); }; - let r_cycle = output_points.instruction_raf_flag(); - let r_address = reconstruct_r_address(output_points, r_cycle.len()); - // eq over the upstream instruction claim-reduction cycle point; all three - // consumed openings share that point, so the lookup-output input carries it. - let eq_reduction = - try_eq_mle(input_points.lookup_output(), r_cycle).map_err(public_input_failed)?; - let address_bits = self.dimensions.instruction_address_bits(); - // `upper_half_all_ones` below slices the leading half of this point, so a - // reconstruction of the wrong length would silently guard the wrong bits - // rather than fail. The point is verifier-derived, but the mis-slice is - // invisible if that ever stops being true. - if r_address.len() != address_bits { - return Err(public_input_failed(format!( - "instruction address point has {} coordinates, expected {address_bits}", - r_address.len() - ))); - } - let left = || OperandPolynomial::new(address_bits, OperandSide::Left).evaluate(&r_address); - let right = - || OperandPolynomial::new(address_bits, OperandSide::Right).evaluate(&r_address); - let gamma = challenges.gamma; - let gamma2 = gamma * gamma; - match public { - InstructionReadRafPublic::EqTableValue(index) => { - let table = LookupTableKind::::iter() - .find(|table| table.index() == *index) - .ok_or_else(|| { - public_input_failed(format!("unknown lookup table index {index}")) - })?; - Ok(eq_reduction * table.evaluate_mle::(&r_address)) - } - InstructionReadRafPublic::EqRafConstant => { - Ok(eq_reduction * (gamma * left() + gamma2 * right())) - } - InstructionReadRafPublic::EqRafFlag => { - let identity = IdentityPolynomial::new(address_bits).evaluate(&r_address); - let mut raf = gamma2 * identity - gamma * left() - gamma2 * right(); - if CANONICAL_INSTRUCTION_ADDRESS { - // The input claim carries no γ³ term, so the sumcheck can only - // close if Σ_j eq(r_red,j)·RafFlag_j·U(k_j) = 0 — i.e. no - // identity-RAF cycle has an all-ones upper address half. Every - // fp128 alias `k = r + p < 2^128` has exactly that shape, and - // `U(k) = 0` implies `k < 2^128 - 2^64 < p`, so the surviving - // address is the canonical representative of `k mod p` and the - // identity leg pins it exactly. See `CANONICAL_INSTRUCTION_ADDRESS`. - raf += gamma2 * gamma * upper_half_all_ones(&r_address); - } - Ok(eq_reduction * raf) - } - } + let prepared = self.prepare_output(input_points, output_points)?; + self.evaluate_public(public, &prepared, challenges) + } + + fn expected_output( + &self, + input_points: &InstructionReadRafInputClaims>, + output_values: &InstructionReadRafOutputClaims, + output_points: &InstructionReadRafOutputClaims>, + challenges: &InstructionReadRafChallenges, + ) -> Result { + let mut prepared = None; + self.evaluate_output_expression(output_values, challenges, |id| { + let JoltDerivedId::InstructionReadRaf(public) = id else { + return Err(VerifierError::MissingStageClaimDerived { id: (*id).into() }); + }; + let inputs = match &prepared { + Some(inputs) => inputs, + None => prepared.insert(self.prepare_output(input_points, output_points)?), + }; + self.evaluate_public(public, inputs, challenges) + }) } } #[cfg(test)] +#[expect(clippy::unwrap_used, reason = "fixed valid dimensions in test fixtures")] mod tests { use super::*; use crate::stages::relations::ConcreteSumcheck; @@ -228,7 +277,6 @@ mod tests { /// geometry's `read_raf_output_openings` set. If they drift, the ZK /// commitment-count and clear shape-check derived from the `Expr` would be wrong. #[test] - #[expect(clippy::unwrap_used)] fn expected_output_openings_matches_geometry_shape() { let dimensions = InstructionReadRafDimensions::try_from((5, 128, 3)).unwrap(); let expected: std::collections::BTreeSet<_> = { @@ -251,14 +299,13 @@ mod tests { /// Pins the canonical-address term inside `EqRafFlag`. /// /// The term is what forces `Σ_j eq(r_red,j)·RafFlag_j·U(k_j) = 0`, and it is - /// invisible in the symbolic relation — it rides inside a derived public. A + /// invisible in the symbolic relation -- it rides inside a derived public. A /// refactor that dropped it would still typecheck, still produce a /// well-formed proof, and silently reopen the fp128 alias. Asserting the /// closed form (rather than just "nonzero") also pins the γ *power* and the /// leading-half slice, the two transposition traps. #[test] #[expect( - clippy::unwrap_used, clippy::as_conversions, clippy::indexing_slicing, clippy::integer_division, @@ -333,4 +380,64 @@ mod tests { assert_eq!(actual, eq_reduction * baseline); } } + + #[test] + fn read_raf_output_uses_the_current_point_and_rejects_malformed_points() { + let relation = InstructionReadRaf::::new( + InstructionReadRafDimensions::try_from((2, 128, 4)).unwrap(), + ); + let zero = Fr::from_u64(0); + let one = Fr::from_u64(1); + let input_points = InstructionReadRafInputClaims { + lookup_output: vec![zero; 2], + left_lookup_operand: vec![zero; 2], + right_lookup_operand: vec![zero; 2], + }; + // Interleaved operand address (left, right) = (0, 1). + let mut last_chunk = vec![zero; 31]; + last_chunk.extend([one, zero, zero]); + let mut points = InstructionReadRafOutputClaims { + lookup_table_flags: vec![vec![zero; 2]; LookupTableKind::::COUNT], + instruction_ra: vec![ + vec![zero; 34], + vec![zero; 34], + vec![zero; 34], + last_chunk, + ], + instruction_raf_flag: vec![zero; 2], + }; + let values = InstructionReadRafOutputClaims { + lookup_table_flags: vec![zero; LookupTableKind::::COUNT], + instruction_ra: vec![one; 4], + instruction_raf_flag: zero, + }; + let challenges = InstructionReadRafChallenges { + gamma: Fr::from_u64(7), + }; + assert_eq!( + relation + .expected_output(&input_points, &values, &points, &challenges) + .unwrap(), + Fr::from_u64(49) + ); + points.instruction_ra = vec![vec![zero; 34]; 4]; + assert_eq!( + relation + .expected_output(&input_points, &values, &points, &challenges) + .unwrap(), + zero + ); + points.instruction_ra.truncate(3); + assert!(matches!( + relation.expected_output(&input_points, &values, &points, &challenges), + Err(VerifierError::StageClaimPublicInputFailed { .. }) + )); + points.instruction_ra = vec![vec![zero; 34]; 4]; + points.instruction_raf_flag.truncate(1); + assert!(matches!( + relation.expected_output(&input_points, &values, &points, &challenges), + Err(VerifierError::StageClaimPublicInputFailed { .. }) + )); + } + } From 407e5de3c6c82eb891e17e4f062d1c5bdb87412f Mon Sep 17 00:00:00 2001 From: acentelles Date: Sat, 24 Oct 2026 09:27:14 +0100 Subject: [PATCH 11/22] style: rustfmt the instruction read RAF tests --- .../src/stages/stage5/instruction_read_raf.rs | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/crates/jolt-verifier/src/stages/stage5/instruction_read_raf.rs b/crates/jolt-verifier/src/stages/stage5/instruction_read_raf.rs index 3d73fa6c7e..5365fae8e4 100644 --- a/crates/jolt-verifier/src/stages/stage5/instruction_read_raf.rs +++ b/crates/jolt-verifier/src/stages/stage5/instruction_read_raf.rs @@ -263,7 +263,10 @@ impl ConcreteSumcheck for InstructionReadRaf { } #[cfg(test)] -#[expect(clippy::unwrap_used, reason = "fixed valid dimensions in test fixtures")] +#[expect( + clippy::unwrap_used, + reason = "fixed valid dimensions in test fixtures" +)] mod tests { use super::*; use crate::stages::relations::ConcreteSumcheck; @@ -398,12 +401,7 @@ mod tests { last_chunk.extend([one, zero, zero]); let mut points = InstructionReadRafOutputClaims { lookup_table_flags: vec![vec![zero; 2]; LookupTableKind::::COUNT], - instruction_ra: vec![ - vec![zero; 34], - vec![zero; 34], - vec![zero; 34], - last_chunk, - ], + instruction_ra: vec![vec![zero; 34], vec![zero; 34], vec![zero; 34], last_chunk], instruction_raf_flag: vec![zero; 2], }; let values = InstructionReadRafOutputClaims { @@ -439,5 +437,4 @@ mod tests { Err(VerifierError::StageClaimPublicInputFailed { .. }) )); } - } From fb0c01a42eacb561612f14fd72b9469e33a12b0b Mon Sep 17 00:00:00 2001 From: acentelles Date: Sun, 25 Oct 2026 06:37:51 +0000 Subject: [PATCH 12/22] Add opt-in RV64 word memory routines for recursion --- examples/recursion/Cargo.toml | 1 + examples/recursion/guest/Cargo.toml | 1 + examples/recursion/src/main.rs | 2 + jolt-platform/Cargo.toml | 1 + jolt-platform/src/lib.rs | 5 + jolt-platform/src/word_memory.S | 207 +++++++++++++++++++++++++ jolt-platform/src/word_memory.rs | 11 ++ jolt-platform/tests/run-word-memory.sh | 16 ++ jolt-platform/tests/word_memory.c | 133 ++++++++++++++++ jolt-sdk/Cargo.toml | 1 + 10 files changed, 378 insertions(+) create mode 100644 jolt-platform/src/word_memory.S create mode 100644 jolt-platform/src/word_memory.rs create mode 100644 jolt-platform/tests/run-word-memory.sh create mode 100644 jolt-platform/tests/word_memory.c diff --git a/examples/recursion/Cargo.toml b/examples/recursion/Cargo.toml index 22aacf840e..3604dab859 100644 --- a/examples/recursion/Cargo.toml +++ b/examples/recursion/Cargo.toml @@ -8,6 +8,7 @@ name = "recursion" path = "src/main.rs" [features] +word-memory = [] ntt-inline = ["akita", "dep:jolt-inlines-ntt"] # Non-default: default workspace builds must not unify field-inline into the # verifier stack. The recursion flow needs it. diff --git a/examples/recursion/guest/Cargo.toml b/examples/recursion/guest/Cargo.toml index c09cdd2f89..e9e821ae89 100644 --- a/examples/recursion/guest/Cargo.toml +++ b/examples/recursion/guest/Cargo.toml @@ -6,6 +6,7 @@ edition = "2021" [features] ntt-inline = ["akita", "jolt-akita/ntt-inline"] guest = [] +word-memory = ["jolt_sdk/word-memory"] field-inline = ["jolt_sdk/field-inline"] # The field the field-inline unit computes in: BN254 `Fr` under Dory, the # Fp128 protocol prime under Akita. The host selects the one its tracer uses. diff --git a/examples/recursion/src/main.rs b/examples/recursion/src/main.rs index 7c5938b582..101332d94c 100644 --- a/examples/recursion/src/main.rs +++ b/examples/recursion/src/main.rs @@ -895,6 +895,8 @@ fn configured_recursion_program(memory_config: MemoryConfig) -> Program { #[cfg(all(feature = "akita", feature = "l2-terminal-quotient"))] program.add_guest_feature("l2-terminal-quotient"); program.add_guest_feature("fast-alloc"); + #[cfg(feature = "word-memory")] + program.add_guest_feature("word-memory"); program.add_guest_feature("hash-inlines"); #[cfg(all(feature = "akita", feature = "l3-compression-weights"))] program.add_guest_feature("l3-compression-weights"); diff --git a/jolt-platform/Cargo.toml b/jolt-platform/Cargo.toml index 6d303d848c..5a58a3c2e6 100644 --- a/jolt-platform/Cargo.toml +++ b/jolt-platform/Cargo.toml @@ -19,6 +19,7 @@ edition = "2021" std = ["random"] random = ["dep:getrandom_v02", "dep:getrandom_v03", "dep:rand"] malloc-shim = [] +word-memory = [] [dependencies] rand = { workspace = true, default-features = false, features = [ diff --git a/jolt-platform/src/lib.rs b/jolt-platform/src/lib.rs index f9fbf0c69d..7d7bc4c78f 100644 --- a/jolt-platform/src/lib.rs +++ b/jolt-platform/src/lib.rs @@ -32,3 +32,8 @@ pub mod size_class_alloc; any(target_arch = "riscv32", target_arch = "riscv64") ))] mod malloc_shim; + +// Keep this opt-in guest module after existing lines: disabled experiments +// must preserve the frozen guest's panic locations and executable image. +#[cfg(all(feature = "word-memory", target_arch = "riscv64"))] +mod word_memory; diff --git a/jolt-platform/src/word_memory.S b/jolt-platform/src/word_memory.S new file mode 100644 index 0000000000..1b9fb0df0e --- /dev/null +++ b/jolt-platform/src/word_memory.S @@ -0,0 +1,207 @@ +/* RV64 little-endian memory routines. Only caller-saved registers are used. + * memcpy reads/writes exactly the requested ranges and returns the original + * destination. Overlapping ranges retain memcpy's ordinary undefined contract. + * memcmp returns the difference of the first unequal unsigned bytes. + */ +.text +.option push +.option norvc +.p2align 2 +.globl memcpy +.type memcpy,@function +memcpy: + beqz a2, .Lmc_done + mv t0, a0 + xor t1, a0, a1 + andi t1, t1, 7 + bnez t1, .Lmc_shift_prefix +.Lmc_align: + andi t1, t0, 7 + beqz t1, .Lmc_aligned + lbu t2, 0(a1) + sb t2, 0(t0) + addi a1, a1, 1 + addi t0, t0, 1 + addi a2, a2, -1 + bnez a2, .Lmc_align + ret +.Lmc_aligned: + li t1, 64 + bltu a2, t1, .Lmc_words +.Lmc_64: + ld t2, 0(a1) + sd t2, 0(t0) + ld t2, 8(a1) + sd t2, 8(t0) + ld t2, 16(a1) + sd t2, 16(t0) + ld t2, 24(a1) + sd t2, 24(t0) + ld t2, 32(a1) + sd t2, 32(t0) + ld t2, 40(a1) + sd t2, 40(t0) + ld t2, 48(a1) + sd t2, 48(t0) + ld t2, 56(a1) + sd t2, 56(t0) + addi a1, a1, 64 + addi t0, t0, 64 + addi a2, a2, -64 + bgeu a2, t1, .Lmc_64 +.Lmc_words: + li t1, 8 + bltu a2, t1, .Lmc_byte_check +.Lmc_word: + ld t2, 0(a1) + sd t2, 0(t0) + addi a1, a1, 8 + addi t0, t0, 8 + addi a2, a2, -8 + bgeu a2, t1, .Lmc_word + j .Lmc_byte_check + +/* Align the source first, then the destination. Thereafter floor(src/8)*8 + * is at or above the first aligned source address inside the allocation. + * If fewer bytes exist, the byte loop returns before any wide load. + */ +.Lmc_shift_prefix: + andi t1, a1, 7 + beqz t1, .Lmc_shift_align +.Lmc_source_align: + lbu t2, 0(a1) + sb t2, 0(t0) + addi a1, a1, 1 + addi t0, t0, 1 + addi a2, a2, -1 + beqz a2, .Lmc_done + andi t1, a1, 7 + bnez t1, .Lmc_source_align +.Lmc_shift_align: + andi t1, t0, 7 + beqz t1, .Lmc_shift_init + lbu t2, 0(a1) + sb t2, 0(t0) + addi a1, a1, 1 + addi t0, t0, 1 + addi a2, a2, -1 + bnez a2, .Lmc_shift_align + ret +.Lmc_shift_init: + li t1, 16 + bltu a2, t1, .Lmc_byte + andi t5, a1, 7 + slli t3, t5, 3 + li t4, 64 + sub t4, t4, t3 + andi a3, a1, -8 + ld t2, 0(a3) + li t1, 40 + bltu a2, t1, .Lmc_shift_words +/* At least 40 source bytes remain. The highest aligned read ends no later + * than src+40. Four exact destination words are produced, and the final + * source word becomes the next iteration's lower word. + */ +.Lmc_shift_32: + ld t6, 8(a3) + srl a4, t2, t3 + sll a6, t6, t4 + or a4, a4, a6 + sd a4, 0(t0) + ld t2, 16(a3) + srl a4, t6, t3 + sll a6, t2, t4 + or a4, a4, a6 + sd a4, 8(t0) + ld t6, 24(a3) + srl a4, t2, t3 + sll a6, t6, t4 + or a4, a4, a6 + sd a4, 16(t0) + ld t2, 32(a3) + srl a4, t6, t3 + sll a6, t2, t4 + or a4, a4, a6 + sd a4, 24(t0) + addi a3, a3, 32 + addi t0, t0, 32 + addi a2, a2, -32 + bgeu a2, t1, .Lmc_shift_32 +.Lmc_shift_words: + li t1, 16 + bltu a2, t1, .Lmc_shift_tail +.Lmc_shift_word: + ld t6, 8(a3) + srl a4, t2, t3 + sll a6, t6, t4 + or a4, a4, a6 + sd a4, 0(t0) + mv t2, t6 + addi a3, a3, 8 + addi t0, t0, 8 + addi a2, a2, -8 + bgeu a2, t1, .Lmc_shift_word +.Lmc_shift_tail: + add a1, a3, t5 +.Lmc_byte_check: + beqz a2, .Lmc_done +.Lmc_byte: + lbu t2, 0(a1) + sb t2, 0(t0) + addi a1, a1, 1 + addi t0, t0, 1 + addi a2, a2, -1 + bnez a2, .Lmc_byte +.Lmc_done: + ret +.size memcpy, .-memcpy + +.p2align 2 +.globl memcmp +.type memcmp,@function +memcmp: + beqz a2, .Lcmp_equal + xor t0, a0, a1 + andi t0, t0, 7 + bnez t0, .Lcmp_byte +.Lcmp_align: + andi t0, a0, 7 + beqz t0, .Lcmp_words + lbu t1, 0(a0) + lbu t2, 0(a1) + bne t1, t2, .Lcmp_different + addi a0, a0, 1 + addi a1, a1, 1 + addi a2, a2, -1 + bnez a2, .Lcmp_align + j .Lcmp_equal +.Lcmp_words: + li t0, 8 + bltu a2, t0, .Lcmp_byte_check +.Lcmp_word: + ld t1, 0(a0) + ld t2, 0(a1) + bne t1, t2, .Lcmp_byte + addi a0, a0, 8 + addi a1, a1, 8 + addi a2, a2, -8 + bgeu a2, t0, .Lcmp_word +.Lcmp_byte_check: + beqz a2, .Lcmp_equal +.Lcmp_byte: + lbu t1, 0(a0) + lbu t2, 0(a1) + bne t1, t2, .Lcmp_different + addi a0, a0, 1 + addi a1, a1, 1 + addi a2, a2, -1 + bnez a2, .Lcmp_byte +.Lcmp_equal: + li a0, 0 + ret +.Lcmp_different: + sub a0, t1, t2 + ret +.size memcmp, .-memcmp +.option pop +.section .note.GNU-stack,"",@progbits diff --git a/jolt-platform/src/word_memory.rs b/jolt-platform/src/word_memory.rs new file mode 100644 index 0000000000..253bb9e84d --- /dev/null +++ b/jolt-platform/src/word_memory.rs @@ -0,0 +1,11 @@ +//! Optional RV64 memory routines using only existing integer instructions. +//! +//! The assembly copies object representations, including uninitialized bytes, +//! without materializing them as Rust integer values. Every load and store is +//! contained in the caller's ranges; the shifted path never rounds a read +//! outside those ranges. `memcpy` retains its non-overlap precondition. +//! +//! The source is also compiled directly by tests/run-word-memory.sh on a Linux +//! RISC-V runner. No new VM instruction, proof grammar, or transcript is added. + +core::arch::global_asm!(include_str!("word_memory.S")); diff --git a/jolt-platform/tests/run-word-memory.sh b/jolt-platform/tests/run-word-memory.sh new file mode 100644 index 0000000000..10dfafb0e7 --- /dev/null +++ b/jolt-platform/tests/run-word-memory.sh @@ -0,0 +1,16 @@ +#!/usr/bin/env bash +set -euo pipefail +# Linux rental only. The test executes the same assembly that the guest links. +if [[ "$(uname -s)" != Linux ]]; then + echo "word-memory tests require the Linux validation box" >&2 + exit 2 +fi +test_dir="$(dirname "$(realpath "$0")")" +test_out="${WORD_MEMORY_TEST_OUT:-/tmp/jolt-word-memory-tests}" +mkdir -p "$test_out" +riscv64-linux-gnu-gcc -static -O2 -Wall -Wextra -Werror \ + -fno-builtin -fno-tree-loop-distribute-patterns \ + -march=rv64gc -mabi=lp64d \ + "$test_dir/word_memory.c" "$test_dir/../src/word_memory.S" \ + -o "$test_out/word-memory-tests" +qemu-riscv64 "$test_out/word-memory-tests" diff --git a/jolt-platform/tests/word_memory.c b/jolt-platform/tests/word_memory.c new file mode 100644 index 0000000000..fde8b77554 --- /dev/null +++ b/jolt-platform/tests/word_memory.c @@ -0,0 +1,133 @@ +/* Unit tests for the actual RV64 assembly, executed under qemu-riscv64. + * Compile with builtins and loop-to-libcall conversion disabled. The oracle + * reads volatile bytes, independent of either memory routine under test. + */ +#define _GNU_SOURCE +#include +#include +#include +#include +#include +#include +#include + +static void *(*volatile copy_fn)(void *, const void *, size_t) = memcpy; +static int (*volatile compare_fn)(const void *, const void *, size_t) = memcmp; + +static int byte_compare(const volatile unsigned char *a, + const volatile unsigned char *b, size_t n) { + for (size_t i = 0; i < n; ++i) { + unsigned char x = a[i], y = b[i]; + if (x != y) return (int)x - (int)y; + } + return 0; +} + +static void fill(volatile unsigned char *p, size_t n, unsigned seed) { + for (size_t i = 0; i < n; ++i) + p[i] = (unsigned char)((i * 131u + seed) ^ (i >> 3)); +} + +static void all_copy_alignments(void) { + _Alignas(64) unsigned char source[640], dest[640]; + fill(source, sizeof source, 19); + for (size_t s = 0; s < 8; ++s) { + for (size_t d = 0; d < 8; ++d) { + for (size_t n = 0; n <= 257; ++n) { + for (size_t i = 0; i < sizeof dest; ++i) dest[i] = 0xa5; + assert(copy_fn(dest + 32 + d, source + 32 + s, n) == dest + 32 + d); + for (size_t i = 0; i < sizeof dest; ++i) { + unsigned char expected = 0xa5; + if (i >= 32 + d && i - (32 + d) < n) + expected = source[32 + s + i - (32 + d)]; + assert(((volatile unsigned char *)dest)[i] == expected); + } + } + } + } + puts("PASS copy_all_alignments_lengths_and_canaries"); +} + +static void all_compare_alignments(void) { + _Alignas(64) unsigned char a[640], b[640]; + for (size_t x = 0; x < 8; ++x) { + for (size_t y = 0; y < 8; ++y) { + for (size_t n = 0; n <= 257; ++n) { + fill(a + x, n, 31); + fill(b + y, n, 31); + assert(compare_fn(a + x, b + y, n) == 0); + for (size_t i = 0; i < n; ++i) { + if (n > 65 && i != 0 && i != n / 2 && i + 1 != n) continue; + b[y + i] ^= 0x80; + assert(compare_fn(a + x, b + y, n) == byte_compare(a + x, b + y, n)); + assert(compare_fn(b + y, a + x, n) == byte_compare(b + y, a + x, n)); + b[y + i] ^= 0x80; + } + } + } + } + puts("PASS compare_all_alignments_first_difference_and_unsigned_order"); +} + +static unsigned char *guarded(size_t page) { + void *p = mmap(NULL, page * 3, PROT_NONE, MAP_PRIVATE | MAP_ANONYMOUS, -1, 0); + assert(p != MAP_FAILED); + unsigned char *middle = (unsigned char *)p + page; + assert(mprotect(middle, page, PROT_READ | PROT_WRITE) == 0); + return middle; +} + +static void guard_pages_and_long_copies(void) { + long page_result = sysconf(_SC_PAGESIZE); + assert(page_result >= 4096); + size_t page = (size_t)page_result; + unsigned char *a = guarded(page), *b = guarded(page); + for (size_t n = 0; n <= page - 16; n += (n < 160 ? 1 : 97)) { + for (size_t offset = 0; offset < 8; ++offset) { + fill(a, page, 83); + fill(b, page, 17); + unsigned char *source = a + page - n; + unsigned char *dest = b + offset; + assert(copy_fn(dest, source, n) == dest); + assert(byte_compare(dest, source, n) == 0); + assert(compare_fn(dest, source, n) == 0); + source = a + offset; + dest = b + page - n; + assert(copy_fn(dest, source, n) == dest); + assert(byte_compare(dest, source, n) == 0); + assert(compare_fn(dest, source, n) == 0); + } + } + assert(copy_fn(b, a, page) == b); + assert(byte_compare(a, b, page) == 0); + assert(compare_fn(a, b, page) == 0); + assert(compare_fn(a, a, page) == 0); + /* Zero-length calls must not dereference either inaccessible page. */ + assert(copy_fn(b - page, a - page, 0) == b - page); + assert(compare_fn(a - page, b - page, 0) == 0); + assert(munmap(a - page, page * 3) == 0); + assert(munmap(b - page, page * 3) == 0); + puts("PASS guard_pages_both_ends_long_copies_equal_alias_and_zero_length"); +} + +static void uninitialized_object_copy(void) { + unsigned char *a = malloc(4096), *b = malloc(4096); + assert(a != NULL && b != NULL); + /* Inspecting these representations as integers in Rust would be invalid. + * The assembly copies them without any language-level integer read. */ + for (size_t x = 0; x < 8; ++x) + for (size_t y = 0; y < 8; ++y) + assert(copy_fn(b + y, a + x, 2048) == b + y); + free(a); + free(b); + puts("PASS uninitialized_object_representations"); +} + +int main(void) { + all_copy_alignments(); + all_compare_alignments(); + guard_pages_and_long_copies(); + uninitialized_object_copy(); + puts("WORD_MEMORY_UNIT_TESTS_PASS"); + return 0; +} diff --git a/jolt-sdk/Cargo.toml b/jolt-sdk/Cargo.toml index a993355fca..4287e697bb 100644 --- a/jolt-sdk/Cargo.toml +++ b/jolt-sdk/Cargo.toml @@ -87,6 +87,7 @@ guest-verifier = [ ] malloc-shim = ["jolt-platform/malloc-shim"] +word-memory = ["jolt-platform/word-memory"] transcript-poseidon = ["jolt-transcript/transcript-poseidon"] transcript-keccak = ["jolt-transcript/transcript-keccak"] transcript-blake2b = ["jolt-transcript/transcript-blake2b"] From da9243b9119a61c0079116d1a6055213b817341e Mon Sep 17 00:00:00 2001 From: acentelles Date: Sun, 25 Oct 2026 07:11:05 +0000 Subject: [PATCH 13/22] Preserve assembler sections around word memory routines --- jolt-platform/src/word_memory.S | 7 +++++-- jolt-platform/tests/run-word-memory.sh | 2 +- jolt-platform/tests/word_memory.c | 3 +++ jolt-platform/tests/word_memory_with_section_probe.S | 12 ++++++++++++ 4 files changed, 21 insertions(+), 3 deletions(-) create mode 100644 jolt-platform/tests/word_memory_with_section_probe.S diff --git a/jolt-platform/src/word_memory.S b/jolt-platform/src/word_memory.S index 1b9fb0df0e..0ea8c465a7 100644 --- a/jolt-platform/src/word_memory.S +++ b/jolt-platform/src/word_memory.S @@ -3,7 +3,8 @@ * destination. Overlapping ranges retain memcpy's ordinary undefined contract. * memcmp returns the difference of the first unequal unsigned bytes. */ -.text +/* global_asm blocks share assembler state inside the linked Rust unit. */ +.pushsection .text.jolt_word_memory,"ax",@progbits .option push .option norvc .p2align 2 @@ -204,4 +205,6 @@ memcmp: ret .size memcmp, .-memcmp .option pop -.section .note.GNU-stack,"",@progbits +.popsection +.pushsection .note.GNU-stack,"",@progbits +.popsection diff --git a/jolt-platform/tests/run-word-memory.sh b/jolt-platform/tests/run-word-memory.sh index 10dfafb0e7..c3982a069e 100644 --- a/jolt-platform/tests/run-word-memory.sh +++ b/jolt-platform/tests/run-word-memory.sh @@ -11,6 +11,6 @@ mkdir -p "$test_out" riscv64-linux-gnu-gcc -static -O2 -Wall -Wextra -Werror \ -fno-builtin -fno-tree-loop-distribute-patterns \ -march=rv64gc -mabi=lp64d \ - "$test_dir/word_memory.c" "$test_dir/../src/word_memory.S" \ + "$test_dir/word_memory.c" "$test_dir/word_memory_with_section_probe.S" \ -o "$test_out/word-memory-tests" qemu-riscv64 "$test_out/word-memory-tests" diff --git a/jolt-platform/tests/word_memory.c b/jolt-platform/tests/word_memory.c index fde8b77554..a2753de3f5 100644 --- a/jolt-platform/tests/word_memory.c +++ b/jolt-platform/tests/word_memory.c @@ -13,6 +13,7 @@ static void *(*volatile copy_fn)(void *, const void *, size_t) = memcpy; static int (*volatile compare_fn)(const void *, const void *, size_t) = memcmp; +extern int word_memory_section_probe(void); static int byte_compare(const volatile unsigned char *a, const volatile unsigned char *b, size_t n) { @@ -124,6 +125,8 @@ static void uninitialized_object_copy(void) { } int main(void) { + assert(word_memory_section_probe() == 291); + puts("PASS assembler_section_restored_for_subsequent_code"); all_copy_alignments(); all_compare_alignments(); guard_pages_and_long_copies(); diff --git a/jolt-platform/tests/word_memory_with_section_probe.S b/jolt-platform/tests/word_memory_with_section_probe.S new file mode 100644 index 0000000000..7153ae9b07 --- /dev/null +++ b/jolt-platform/tests/word_memory_with_section_probe.S @@ -0,0 +1,12 @@ +/* Include the production body in a translation unit with subsequent code. + * A leaked .note.GNU-stack section makes the probe non-executable, matching + * the failure mode of later global_asm blocks in the Rust guest. + */ +.text +#include "../src/word_memory.S" +.globl word_memory_section_probe +.type word_memory_section_probe,@function +word_memory_section_probe: + li a0, 291 + ret +.size word_memory_section_probe, .-word_memory_section_probe From 8ebf215212d3cc850d1e8086dfc17564b6a73662 Mon Sep 17 00:00:00 2001 From: acentelles Date: Sun, 25 Oct 2026 08:44:34 +0000 Subject: [PATCH 14/22] perf(recursion): turn word memory routines on by default The recursion example enables word-memory by default next to the factored compression weights, the terminal quotient certificate and word decoding. The host forwards it to the guest only together with akita, so Dory builds are unchanged. --no-default-features turns all four off. Host-side Cargo and cfg changes only. --- examples/recursion/Cargo.toml | 2 +- examples/recursion/src/main.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/recursion/Cargo.toml b/examples/recursion/Cargo.toml index 3604dab859..dace2fe1a0 100644 --- a/examples/recursion/Cargo.toml +++ b/examples/recursion/Cargo.toml @@ -28,7 +28,7 @@ akita = [ # points instead of the exact product. Word decoding: the guest decodes # fixed-wire field elements by word with the same canonicality checks. Turn # all three off with --no-default-features. -default = ["l3-compression-weights", "l2-terminal-quotient", "word-decode"] +default = ["l3-compression-weights", "l2-terminal-quotient", "word-decode", "word-memory"] l3-compression-weights = ["jolt-akita?/l3-compression-weights"] l2-terminal-quotient = ["jolt-akita?/l2-terminal-quotient"] word-decode = ["jolt-akita?/word-decode"] diff --git a/examples/recursion/src/main.rs b/examples/recursion/src/main.rs index 101332d94c..d3ea3061d8 100644 --- a/examples/recursion/src/main.rs +++ b/examples/recursion/src/main.rs @@ -895,7 +895,7 @@ fn configured_recursion_program(memory_config: MemoryConfig) -> Program { #[cfg(all(feature = "akita", feature = "l2-terminal-quotient"))] program.add_guest_feature("l2-terminal-quotient"); program.add_guest_feature("fast-alloc"); - #[cfg(feature = "word-memory")] + #[cfg(all(feature = "akita", feature = "word-memory"))] program.add_guest_feature("word-memory"); program.add_guest_feature("hash-inlines"); #[cfg(all(feature = "akita", feature = "l3-compression-weights"))] From ec01b725e9c5aa2515fad9203553f59a2bc3cacc Mon Sep 17 00:00:00 2001 From: acentelles Date: Sun, 25 Oct 2026 11:22:11 +0000 Subject: [PATCH 15/22] build(akita): pin the recursion verifier changes on the Akita fork The recursion example's default features use Akita changes that are not in LayerZero-Labs/akita yet. Pin the Akita crates to the fork commit that carries them so a fresh checkout builds the measured configuration. --- Cargo.lock | 32 ++++++++++++++++---------------- Cargo.toml | 26 ++++++++++++++------------ 2 files changed, 30 insertions(+), 28 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 0f32212fd7..0135f1cb13 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -93,7 +93,7 @@ dependencies = [ [[package]] name = "akita-algebra" version = "0.1.0" -source = "git+https://github.com/LayerZero-Labs/akita.git?rev=ee03aa30544caaa3f5f2948b222790b919e9b8e7#ee03aa30544caaa3f5f2948b222790b919e9b8e7" +source = "git+https://github.com/Acentelles/akita-lz.git?rev=9db4ee25b89b1b66c42f399af983230333733c8b#9db4ee25b89b1b66c42f399af983230333733c8b" dependencies = [ "akita-error", "akita-serialization", @@ -108,7 +108,7 @@ dependencies = [ [[package]] name = "akita-challenges" version = "0.1.0" -source = "git+https://github.com/LayerZero-Labs/akita.git?rev=ee03aa30544caaa3f5f2948b222790b919e9b8e7#ee03aa30544caaa3f5f2948b222790b919e9b8e7" +source = "git+https://github.com/Acentelles/akita-lz.git?rev=9db4ee25b89b1b66c42f399af983230333733c8b#9db4ee25b89b1b66c42f399af983230333733c8b" dependencies = [ "akita-error", "akita-transcript", @@ -122,7 +122,7 @@ dependencies = [ [[package]] name = "akita-config" version = "0.1.0" -source = "git+https://github.com/LayerZero-Labs/akita.git?rev=ee03aa30544caaa3f5f2948b222790b919e9b8e7#ee03aa30544caaa3f5f2948b222790b919e9b8e7" +source = "git+https://github.com/Acentelles/akita-lz.git?rev=9db4ee25b89b1b66c42f399af983230333733c8b#9db4ee25b89b1b66c42f399af983230333733c8b" dependencies = [ "akita-challenges", "akita-error", @@ -137,7 +137,7 @@ dependencies = [ [[package]] name = "akita-cpu-backend" version = "0.1.0" -source = "git+https://github.com/LayerZero-Labs/akita.git?rev=ee03aa30544caaa3f5f2948b222790b919e9b8e7#ee03aa30544caaa3f5f2948b222790b919e9b8e7" +source = "git+https://github.com/Acentelles/akita-lz.git?rev=9db4ee25b89b1b66c42f399af983230333733c8b#9db4ee25b89b1b66c42f399af983230333733c8b" dependencies = [ "akita-algebra", "akita-challenges", @@ -158,7 +158,7 @@ dependencies = [ [[package]] name = "akita-error" version = "0.1.0" -source = "git+https://github.com/LayerZero-Labs/akita.git?rev=ee03aa30544caaa3f5f2948b222790b919e9b8e7#ee03aa30544caaa3f5f2948b222790b919e9b8e7" +source = "git+https://github.com/Acentelles/akita-lz.git?rev=9db4ee25b89b1b66c42f399af983230333733c8b#9db4ee25b89b1b66c42f399af983230333733c8b" dependencies = [ "thiserror 2.0.20", ] @@ -166,7 +166,7 @@ dependencies = [ [[package]] name = "akita-params" version = "0.1.0" -source = "git+https://github.com/LayerZero-Labs/akita.git?rev=ee03aa30544caaa3f5f2948b222790b919e9b8e7#ee03aa30544caaa3f5f2948b222790b919e9b8e7" +source = "git+https://github.com/Acentelles/akita-lz.git?rev=9db4ee25b89b1b66c42f399af983230333733c8b#9db4ee25b89b1b66c42f399af983230333733c8b" dependencies = [ "akita-algebra", "akita-challenges", @@ -184,7 +184,7 @@ dependencies = [ [[package]] name = "akita-pcs" version = "0.1.0" -source = "git+https://github.com/LayerZero-Labs/akita.git?rev=ee03aa30544caaa3f5f2948b222790b919e9b8e7#ee03aa30544caaa3f5f2948b222790b919e9b8e7" +source = "git+https://github.com/Acentelles/akita-lz.git?rev=9db4ee25b89b1b66c42f399af983230333733c8b#9db4ee25b89b1b66c42f399af983230333733c8b" dependencies = [ "akita-algebra", "akita-challenges", @@ -206,7 +206,7 @@ dependencies = [ [[package]] name = "akita-planner" version = "0.1.0" -source = "git+https://github.com/LayerZero-Labs/akita.git?rev=ee03aa30544caaa3f5f2948b222790b919e9b8e7#ee03aa30544caaa3f5f2948b222790b919e9b8e7" +source = "git+https://github.com/Acentelles/akita-lz.git?rev=9db4ee25b89b1b66c42f399af983230333733c8b#9db4ee25b89b1b66c42f399af983230333733c8b" dependencies = [ "akita-challenges", "akita-error", @@ -218,7 +218,7 @@ dependencies = [ [[package]] name = "akita-prover" version = "0.1.0" -source = "git+https://github.com/LayerZero-Labs/akita.git?rev=ee03aa30544caaa3f5f2948b222790b919e9b8e7#ee03aa30544caaa3f5f2948b222790b919e9b8e7" +source = "git+https://github.com/Acentelles/akita-lz.git?rev=9db4ee25b89b1b66c42f399af983230333733c8b#9db4ee25b89b1b66c42f399af983230333733c8b" dependencies = [ "akita-algebra", "akita-challenges", @@ -237,7 +237,7 @@ dependencies = [ [[package]] name = "akita-schedules" version = "0.1.0" -source = "git+https://github.com/LayerZero-Labs/akita.git?rev=ee03aa30544caaa3f5f2948b222790b919e9b8e7#ee03aa30544caaa3f5f2948b222790b919e9b8e7" +source = "git+https://github.com/Acentelles/akita-lz.git?rev=9db4ee25b89b1b66c42f399af983230333733c8b#9db4ee25b89b1b66c42f399af983230333733c8b" dependencies = [ "akita-challenges", "akita-error", @@ -251,7 +251,7 @@ dependencies = [ [[package]] name = "akita-serialization" version = "0.1.0" -source = "git+https://github.com/LayerZero-Labs/akita.git?rev=ee03aa30544caaa3f5f2948b222790b919e9b8e7#ee03aa30544caaa3f5f2948b222790b919e9b8e7" +source = "git+https://github.com/Acentelles/akita-lz.git?rev=9db4ee25b89b1b66c42f399af983230333733c8b#9db4ee25b89b1b66c42f399af983230333733c8b" dependencies = [ "jolt-field", "jolt-poly", @@ -261,7 +261,7 @@ dependencies = [ [[package]] name = "akita-setup" version = "0.1.0" -source = "git+https://github.com/LayerZero-Labs/akita.git?rev=ee03aa30544caaa3f5f2948b222790b919e9b8e7#ee03aa30544caaa3f5f2948b222790b919e9b8e7" +source = "git+https://github.com/Acentelles/akita-lz.git?rev=9db4ee25b89b1b66c42f399af983230333733c8b#9db4ee25b89b1b66c42f399af983230333733c8b" dependencies = [ "akita-config", "akita-cpu-backend", @@ -276,7 +276,7 @@ dependencies = [ [[package]] name = "akita-sumcheck" version = "0.1.0" -source = "git+https://github.com/LayerZero-Labs/akita.git?rev=ee03aa30544caaa3f5f2948b222790b919e9b8e7#ee03aa30544caaa3f5f2948b222790b919e9b8e7" +source = "git+https://github.com/Acentelles/akita-lz.git?rev=9db4ee25b89b1b66c42f399af983230333733c8b#9db4ee25b89b1b66c42f399af983230333733c8b" dependencies = [ "akita-algebra", "akita-error", @@ -289,7 +289,7 @@ dependencies = [ [[package]] name = "akita-transcript" version = "0.1.0" -source = "git+https://github.com/LayerZero-Labs/akita.git?rev=ee03aa30544caaa3f5f2948b222790b919e9b8e7#ee03aa30544caaa3f5f2948b222790b919e9b8e7" +source = "git+https://github.com/Acentelles/akita-lz.git?rev=9db4ee25b89b1b66c42f399af983230333733c8b#9db4ee25b89b1b66c42f399af983230333733c8b" dependencies = [ "akita-error", "jolt-field", @@ -300,7 +300,7 @@ dependencies = [ [[package]] name = "akita-types" version = "0.1.0" -source = "git+https://github.com/LayerZero-Labs/akita.git?rev=ee03aa30544caaa3f5f2948b222790b919e9b8e7#ee03aa30544caaa3f5f2948b222790b919e9b8e7" +source = "git+https://github.com/Acentelles/akita-lz.git?rev=9db4ee25b89b1b66c42f399af983230333733c8b#9db4ee25b89b1b66c42f399af983230333733c8b" dependencies = [ "akita-algebra", "akita-challenges", @@ -319,7 +319,7 @@ dependencies = [ [[package]] name = "akita-verifier" version = "0.1.0" -source = "git+https://github.com/LayerZero-Labs/akita.git?rev=ee03aa30544caaa3f5f2948b222790b919e9b8e7#ee03aa30544caaa3f5f2948b222790b919e9b8e7" +source = "git+https://github.com/Acentelles/akita-lz.git?rev=9db4ee25b89b1b66c42f399af983230333733c8b#9db4ee25b89b1b66c42f399af983230333733c8b" dependencies = [ "akita-algebra", "akita-challenges", diff --git a/Cargo.toml b/Cargo.toml index 523c2bcd2d..363283796a 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -306,18 +306,20 @@ dory = { package = "dory-pcs", version = "0.4.2", features = [ "disk-persistence", "zk", ] } -# LayerZero-Labs/akita branch markos/recursion-integration: akita cf95fd05 -# (the revision Jolt main pins) plus the recursion verifier-guest PRs -# (LayerZero-Labs/akita#186-#190). Repin to akita main once those merge. -akita-algebra = { git = "https://github.com/LayerZero-Labs/akita.git", rev = "ee03aa30544caaa3f5f2948b222790b919e9b8e7", default-features = false } -akita-config = { git = "https://github.com/LayerZero-Labs/akita.git", rev = "ee03aa30544caaa3f5f2948b222790b919e9b8e7", default-features = false } -akita-error = { git = "https://github.com/LayerZero-Labs/akita.git", rev = "ee03aa30544caaa3f5f2948b222790b919e9b8e7", default-features = false } -akita-pcs = { git = "https://github.com/LayerZero-Labs/akita.git", rev = "ee03aa30544caaa3f5f2948b222790b919e9b8e7", default-features = false } -akita-planner = { git = "https://github.com/LayerZero-Labs/akita.git", rev = "ee03aa30544caaa3f5f2948b222790b919e9b8e7", default-features = false } -akita-schedules = { git = "https://github.com/LayerZero-Labs/akita.git", rev = "ee03aa30544caaa3f5f2948b222790b919e9b8e7", default-features = false } -akita-challenges = { git = "https://github.com/LayerZero-Labs/akita.git", rev = "ee03aa30544caaa3f5f2948b222790b919e9b8e7", default-features = false } -akita-types = { git = "https://github.com/LayerZero-Labs/akita.git", rev = "ee03aa30544caaa3f5f2948b222790b919e9b8e7", default-features = false } -akita-params = { git = "https://github.com/LayerZero-Labs/akita.git", rev = "ee03aa30544caaa3f5f2948b222790b919e9b8e7", default-features = false } +# Akita markos/recursion-integration (ee03aa30, LayerZero-Labs/akita#186-#190) +# plus the recursion verifier changes on Acentelles/akita-lz: factored +# compression weights, the terminal quotient certificate, transposed quotient +# right sides, the L2 proof bound, batched reduced setup rows and signed sparse +# accumulation. Repin to LayerZero-Labs/akita once those land there. +akita-algebra = { git = "https://github.com/Acentelles/akita-lz.git", rev = "9db4ee25b89b1b66c42f399af983230333733c8b", default-features = false } +akita-config = { git = "https://github.com/Acentelles/akita-lz.git", rev = "9db4ee25b89b1b66c42f399af983230333733c8b", default-features = false } +akita-error = { git = "https://github.com/Acentelles/akita-lz.git", rev = "9db4ee25b89b1b66c42f399af983230333733c8b", default-features = false } +akita-pcs = { git = "https://github.com/Acentelles/akita-lz.git", rev = "9db4ee25b89b1b66c42f399af983230333733c8b", default-features = false } +akita-planner = { git = "https://github.com/Acentelles/akita-lz.git", rev = "9db4ee25b89b1b66c42f399af983230333733c8b", default-features = false } +akita-schedules = { git = "https://github.com/Acentelles/akita-lz.git", rev = "9db4ee25b89b1b66c42f399af983230333733c8b", default-features = false } +akita-challenges = { git = "https://github.com/Acentelles/akita-lz.git", rev = "9db4ee25b89b1b66c42f399af983230333733c8b", default-features = false } +akita-types = { git = "https://github.com/Acentelles/akita-lz.git", rev = "9db4ee25b89b1b66c42f399af983230333733c8b", default-features = false } +akita-params = { git = "https://github.com/Acentelles/akita-lz.git", rev = "9db4ee25b89b1b66c42f399af983230333733c8b", default-features = false } # Core Utilities clap = { version = "4.6.1", features = ["derive"] } From 63c4870b1a5725693d1daf539049d355357a6e37 Mon Sep 17 00:00:00 2001 From: acentelles Date: Sun, 25 Oct 2026 18:36:54 +0000 Subject: [PATCH 16/22] perf(recursion): build the recursion verifier guest with inline-threshold 1000 and one codegen unit by default The recursion host now builds the verifier guest with ZEROOS_GUEST_RUSTFLAGS=-Cllvm-args=-inline-threshold=1000 and CARGO_PROFILE_RELEASE_CODEGEN_UNITS=1 (new default feature guest-codegen). The settings apply to the verifier guest build only; the inner guests and their proofs are unchanged. A value the caller already set for either variable wins. RECURSION_GUEST_CODEGEN=off, or building without the feature (--no-default-features), restores the stock guest build. Host-side Cargo and source changes only. --- examples/recursion/Cargo.toml | 7 ++++-- examples/recursion/src/main.rs | 41 +++++++++++++++++++++++++++++++++- 2 files changed, 45 insertions(+), 3 deletions(-) diff --git a/examples/recursion/Cargo.toml b/examples/recursion/Cargo.toml index dace2fe1a0..f95ae05648 100644 --- a/examples/recursion/Cargo.toml +++ b/examples/recursion/Cargo.toml @@ -27,8 +27,11 @@ akita = [ # quotient (protocol identifier v7-l2tq1) and the guest checks it at two # points instead of the exact product. Word decoding: the guest decodes # fixed-wire field elements by word with the same canonicality checks. Turn -# all three off with --no-default-features. -default = ["l3-compression-weights", "l2-terminal-quotient", "word-decode", "word-memory"] +# all three off with --no-default-features. guest-codegen: the verifier guest +# is built with -Cllvm-args=-inline-threshold=1000 and one codegen unit (host +# side only; RECURSION_GUEST_CODEGEN=off restores the stock guest build). +default = ["l3-compression-weights", "l2-terminal-quotient", "word-decode", "word-memory", "guest-codegen"] +guest-codegen = [] l3-compression-weights = ["jolt-akita?/l3-compression-weights"] l2-terminal-quotient = ["jolt-akita?/l2-terminal-quotient"] word-decode = ["jolt-akita?/word-decode"] diff --git a/examples/recursion/src/main.rs b/examples/recursion/src/main.rs index d3ea3061d8..643796ecff 100644 --- a/examples/recursion/src/main.rs +++ b/examples/recursion/src/main.rs @@ -1049,6 +1049,45 @@ fn tamper_l2( save_proof_data(guest, &tampered, output); } +/// Guest build settings the verifier guest uses by default (feature +/// `guest-codegen`): a higher LLVM inline threshold and one codegen unit for +/// the guest's release profile. Measured as the fewest trace rows of the +/// guest build configurations screened at inner sizes 2^12 and 2^20; the inner +/// proofs are unchanged. A value the caller already set for either variable +/// wins, and `RECURSION_GUEST_CODEGEN=off` (or building without the feature) +/// restores the stock guest build. +const RECURSION_GUEST_CODEGEN: [(&str, &str); 2] = [ + ( + "ZEROOS_GUEST_RUSTFLAGS", + "-Cllvm-args=-inline-threshold=1000", + ), + ("CARGO_PROFILE_RELEASE_CODEGEN_UNITS", "1"), +]; + +/// Builds the verifier guest, applying the default guest build settings to +/// this build only (the inner guests keep the stock settings). +fn build_recursion_guest(program: &mut Program, target_dir: &str) { + let enabled = cfg!(feature = "guest-codegen") + && !matches!( + std::env::var("RECURSION_GUEST_CODEGEN").as_deref(), + Ok("off") + ); + let mut applied = Vec::new(); + if enabled { + for (key, value) in RECURSION_GUEST_CODEGEN { + if std::env::var_os(key).is_none() { + std::env::set_var(key, value); + applied.push(key); + } + } + } + info!(" recursion guest build settings: {applied:?}"); + program.build(target_dir); + for key in applied { + std::env::remove_var(key); + } +} + fn run_recursion_proof( guest: GuestProgram, run_config: RunConfig, @@ -1059,7 +1098,7 @@ fn run_recursion_proof( let target_dir = "/tmp/jolt-guest-targets"; let mut program = configured_recursion_program(memory_config); - program.build(target_dir); + build_recursion_guest(&mut program, target_dir); match run_config { RunConfig::Trace(expected) | RunConfig::TraceToFile(expected) => { let io_device = if matches!(run_config, RunConfig::Trace(_)) { From 7fe2a92de5771c1a519a290ccf5cfba123807c36 Mon Sep 17 00:00:00 2001 From: acentelles Date: Sun, 25 Oct 2026 21:23:06 +0000 Subject: [PATCH 17/22] perf(recursion): raise the recursion verifier guest inline threshold to 1750 The guest-codegen default for the recursion verifier guest build moves from -Cllvm-args=-inline-threshold=1000 to -Cllvm-args=-inline-threshold=1750, still with one codegen unit. Thresholds of 2000 and above fail to link the guest. A caller value for ZEROOS_GUEST_RUSTFLAGS still wins, and RECURSION_GUEST_CODEGEN=off restores the stock guest build. Host-side source change only; the inner guests and their proofs are unchanged. --- examples/recursion/Cargo.toml | 2 +- examples/recursion/src/main.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/recursion/Cargo.toml b/examples/recursion/Cargo.toml index f95ae05648..2aaabf85bb 100644 --- a/examples/recursion/Cargo.toml +++ b/examples/recursion/Cargo.toml @@ -28,7 +28,7 @@ akita = [ # points instead of the exact product. Word decoding: the guest decodes # fixed-wire field elements by word with the same canonicality checks. Turn # all three off with --no-default-features. guest-codegen: the verifier guest -# is built with -Cllvm-args=-inline-threshold=1000 and one codegen unit (host +# is built with -Cllvm-args=-inline-threshold=1750 and one codegen unit (host # side only; RECURSION_GUEST_CODEGEN=off restores the stock guest build). default = ["l3-compression-weights", "l2-terminal-quotient", "word-decode", "word-memory", "guest-codegen"] guest-codegen = [] diff --git a/examples/recursion/src/main.rs b/examples/recursion/src/main.rs index 643796ecff..04105479b8 100644 --- a/examples/recursion/src/main.rs +++ b/examples/recursion/src/main.rs @@ -1059,7 +1059,7 @@ fn tamper_l2( const RECURSION_GUEST_CODEGEN: [(&str, &str); 2] = [ ( "ZEROOS_GUEST_RUSTFLAGS", - "-Cllvm-args=-inline-threshold=1000", + "-Cllvm-args=-inline-threshold=1750", ), ("CARGO_PROFILE_RELEASE_CODEGEN_UNITS", "1"), ]; From e50659de352206ff4675966ec5c7503441e94781 Mon Sep 17 00:00:00 2001 From: acentelles Date: Mon, 26 Oct 2026 03:32:11 +0000 Subject: [PATCH 18/22] perf(recursion): enable GVN hoisting and DFA jump threading in the recursion verifier guest build The guest-codegen default for the recursion verifier guest build adds -Cllvm-args=-enable-gvn-hoist and -Cllvm-args=-enable-dfa-jump-thread to -Cllvm-args=-inline-threshold=1750, still with one codegen unit. A caller value for ZEROOS_GUEST_RUSTFLAGS still wins, and RECURSION_GUEST_CODEGEN=off restores the stock guest build. Host-side source change only; the inner guests and their proofs are unchanged. --- examples/recursion/Cargo.toml | 5 +++-- examples/recursion/src/main.rs | 2 +- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/examples/recursion/Cargo.toml b/examples/recursion/Cargo.toml index 2aaabf85bb..11807bd786 100644 --- a/examples/recursion/Cargo.toml +++ b/examples/recursion/Cargo.toml @@ -28,8 +28,9 @@ akita = [ # points instead of the exact product. Word decoding: the guest decodes # fixed-wire field elements by word with the same canonicality checks. Turn # all three off with --no-default-features. guest-codegen: the verifier guest -# is built with -Cllvm-args=-inline-threshold=1750 and one codegen unit (host -# side only; RECURSION_GUEST_CODEGEN=off restores the stock guest build). +# is built with -Cllvm-args=-inline-threshold=1750, -Cllvm-args=-enable-gvn-hoist, +# -Cllvm-args=-enable-dfa-jump-thread and one codegen unit (host side only; +# RECURSION_GUEST_CODEGEN=off restores the stock guest build). default = ["l3-compression-weights", "l2-terminal-quotient", "word-decode", "word-memory", "guest-codegen"] guest-codegen = [] l3-compression-weights = ["jolt-akita?/l3-compression-weights"] diff --git a/examples/recursion/src/main.rs b/examples/recursion/src/main.rs index 04105479b8..027eff12db 100644 --- a/examples/recursion/src/main.rs +++ b/examples/recursion/src/main.rs @@ -1059,7 +1059,7 @@ fn tamper_l2( const RECURSION_GUEST_CODEGEN: [(&str, &str); 2] = [ ( "ZEROOS_GUEST_RUSTFLAGS", - "-Cllvm-args=-inline-threshold=1750", + "-Cllvm-args=-inline-threshold=1750 -Cllvm-args=-enable-gvn-hoist -Cllvm-args=-enable-dfa-jump-thread", ), ("CARGO_PROFILE_RELEASE_CODEGEN_UNITS", "1"), ]; From 1a48794959ff88b976c61fa6c64c6aabb0103e68 Mon Sep 17 00:00:00 2001 From: acentelles Date: Mon, 26 Oct 2026 06:51:12 +0000 Subject: [PATCH 19/22] perf(recursion): use ExtTSP block placement without tail merging in the recursion verifier guest build The guest-codegen default for the recursion verifier guest build adds -Cllvm-args=-enable-ext-tsp-block-placement and -Cllvm-args=-enable-tail-merge=false to the existing inline threshold, GVN hoisting and DFA jump threading flags, still with one codegen unit. A caller value for ZEROOS_GUEST_RUSTFLAGS still wins, and RECURSION_GUEST_CODEGEN=off restores the stock guest build. Host-side source change only; the inner guests and their proofs are unchanged. --- examples/recursion/Cargo.toml | 3 ++- examples/recursion/src/main.rs | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/examples/recursion/Cargo.toml b/examples/recursion/Cargo.toml index 11807bd786..ae19f13f84 100644 --- a/examples/recursion/Cargo.toml +++ b/examples/recursion/Cargo.toml @@ -29,7 +29,8 @@ akita = [ # fixed-wire field elements by word with the same canonicality checks. Turn # all three off with --no-default-features. guest-codegen: the verifier guest # is built with -Cllvm-args=-inline-threshold=1750, -Cllvm-args=-enable-gvn-hoist, -# -Cllvm-args=-enable-dfa-jump-thread and one codegen unit (host side only; +# -Cllvm-args=-enable-dfa-jump-thread, -Cllvm-args=-enable-ext-tsp-block-placement, +# -Cllvm-args=-enable-tail-merge=false and one codegen unit (host side only; # RECURSION_GUEST_CODEGEN=off restores the stock guest build). default = ["l3-compression-weights", "l2-terminal-quotient", "word-decode", "word-memory", "guest-codegen"] guest-codegen = [] diff --git a/examples/recursion/src/main.rs b/examples/recursion/src/main.rs index 027eff12db..4199af6ceb 100644 --- a/examples/recursion/src/main.rs +++ b/examples/recursion/src/main.rs @@ -1059,7 +1059,7 @@ fn tamper_l2( const RECURSION_GUEST_CODEGEN: [(&str, &str); 2] = [ ( "ZEROOS_GUEST_RUSTFLAGS", - "-Cllvm-args=-inline-threshold=1750 -Cllvm-args=-enable-gvn-hoist -Cllvm-args=-enable-dfa-jump-thread", + "-Cllvm-args=-inline-threshold=1750 -Cllvm-args=-enable-gvn-hoist -Cllvm-args=-enable-dfa-jump-thread -Cllvm-args=-enable-ext-tsp-block-placement -Cllvm-args=-enable-tail-merge=false", ), ("CARGO_PROFILE_RELEASE_CODEGEN_UNITS", "1"), ]; From 85bee6f27e237a7993c6a96150f81eb441432685 Mon Sep 17 00:00:00 2001 From: acentelles Date: Mon, 26 Oct 2026 12:45:01 +0000 Subject: [PATCH 20/22] test(jolt-sdk): skip the Dory verifier fixture test under akita The verifier_api test verifies Dory fixtures with VerifierPCS (Dory). With jolt-sdk's akita feature, jolt_verifier::verify is the Akita path, whose OneHotTrace metadata bounds Dory does not implement, so the test target failed to compile (E0277) whenever akita was unified into jolt-sdk, for example through the recursion example's akita feature. Gate the test to builds without akita, like verifier_preprocessing_from_prover. --- jolt-sdk/tests/verifier_api.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/jolt-sdk/tests/verifier_api.rs b/jolt-sdk/tests/verifier_api.rs index 8111799c0b..fed7488f7c 100644 --- a/jolt-sdk/tests/verifier_api.rs +++ b/jolt-sdk/tests/verifier_api.rs @@ -1,5 +1,7 @@ #[cfg(test)] -#[cfg(feature = "host")] +// The fixtures are Dory proofs, and `VerifierPCS` is Dory. With `akita`, +// `jolt_verifier::verify` is the Akita path, whose bounds Dory does not meet. +#[cfg(all(feature = "host", not(feature = "akita")))] mod tests { use jolt_sdk::{ deserialize_verifier_object, JoltDevice, JoltVerifierPreprocessing, RV64IMACProof, From 81cbce4f07455dfd03c96fe1d5001c1992605fe5 Mon Sep 17 00:00:00 2001 From: acentelles Date: Mon, 26 Oct 2026 19:51:10 +0000 Subject: [PATCH 21/22] perf(recursion): use size-oriented spill splitting in the recursion verifier guest build The guest-codegen default for the recursion verifier guest build adds -Cllvm-args=-split-spill-mode=size to the existing inline threshold, GVN hoisting, DFA jump threading, ExtTSP block placement and no tail merging flags, still with one codegen unit. A caller value for ZEROOS_GUEST_RUSTFLAGS still wins, and RECURSION_GUEST_CODEGEN=off restores the stock guest build. Host-side source change only; the inner guests and their proofs are unchanged. --- examples/recursion/Cargo.toml | 3 ++- examples/recursion/src/main.rs | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/examples/recursion/Cargo.toml b/examples/recursion/Cargo.toml index ae19f13f84..1d5259b58c 100644 --- a/examples/recursion/Cargo.toml +++ b/examples/recursion/Cargo.toml @@ -30,7 +30,8 @@ akita = [ # all three off with --no-default-features. guest-codegen: the verifier guest # is built with -Cllvm-args=-inline-threshold=1750, -Cllvm-args=-enable-gvn-hoist, # -Cllvm-args=-enable-dfa-jump-thread, -Cllvm-args=-enable-ext-tsp-block-placement, -# -Cllvm-args=-enable-tail-merge=false and one codegen unit (host side only; +# -Cllvm-args=-enable-tail-merge=false, -Cllvm-args=-split-spill-mode=size +# and one codegen unit (host side only; # RECURSION_GUEST_CODEGEN=off restores the stock guest build). default = ["l3-compression-weights", "l2-terminal-quotient", "word-decode", "word-memory", "guest-codegen"] guest-codegen = [] diff --git a/examples/recursion/src/main.rs b/examples/recursion/src/main.rs index 4199af6ceb..db3c451ab3 100644 --- a/examples/recursion/src/main.rs +++ b/examples/recursion/src/main.rs @@ -1059,7 +1059,7 @@ fn tamper_l2( const RECURSION_GUEST_CODEGEN: [(&str, &str); 2] = [ ( "ZEROOS_GUEST_RUSTFLAGS", - "-Cllvm-args=-inline-threshold=1750 -Cllvm-args=-enable-gvn-hoist -Cllvm-args=-enable-dfa-jump-thread -Cllvm-args=-enable-ext-tsp-block-placement -Cllvm-args=-enable-tail-merge=false", + "-Cllvm-args=-inline-threshold=1750 -Cllvm-args=-enable-gvn-hoist -Cllvm-args=-enable-dfa-jump-thread -Cllvm-args=-enable-ext-tsp-block-placement -Cllvm-args=-enable-tail-merge=false -Cllvm-args=-split-spill-mode=size", ), ("CARGO_PROFILE_RELEASE_CODEGEN_UNITS", "1"), ]; From 0d918f6cbc05d858bab6a2fede23a3de2dbd8c3b Mon Sep 17 00:00:00 2001 From: acentelles Date: Mon, 26 Oct 2026 19:51:10 +0000 Subject: [PATCH 22/22] perf(recursion): disable the RISC-V register cost-per-use model in the recursion verifier guest build The guest-codegen default for the recursion verifier guest build adds -Cllvm-args=-riscv-disable-cost-per-use=true to the existing inline threshold, GVN hoisting, DFA jump threading, ExtTSP block placement, no tail merging and size-oriented spill splitting flags, still with one codegen unit. A caller value for ZEROOS_GUEST_RUSTFLAGS still wins, and RECURSION_GUEST_CODEGEN=off restores the stock guest build. Host-side source change only; the inner guests and their proofs are unchanged. --- examples/recursion/Cargo.toml | 4 ++-- examples/recursion/src/main.rs | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/examples/recursion/Cargo.toml b/examples/recursion/Cargo.toml index 1d5259b58c..6d7d379916 100644 --- a/examples/recursion/Cargo.toml +++ b/examples/recursion/Cargo.toml @@ -30,8 +30,8 @@ akita = [ # all three off with --no-default-features. guest-codegen: the verifier guest # is built with -Cllvm-args=-inline-threshold=1750, -Cllvm-args=-enable-gvn-hoist, # -Cllvm-args=-enable-dfa-jump-thread, -Cllvm-args=-enable-ext-tsp-block-placement, -# -Cllvm-args=-enable-tail-merge=false, -Cllvm-args=-split-spill-mode=size -# and one codegen unit (host side only; +# -Cllvm-args=-enable-tail-merge=false, -Cllvm-args=-split-spill-mode=size, +# -Cllvm-args=-riscv-disable-cost-per-use=true and one codegen unit (host side only; # RECURSION_GUEST_CODEGEN=off restores the stock guest build). default = ["l3-compression-weights", "l2-terminal-quotient", "word-decode", "word-memory", "guest-codegen"] guest-codegen = [] diff --git a/examples/recursion/src/main.rs b/examples/recursion/src/main.rs index db3c451ab3..48c2bb693e 100644 --- a/examples/recursion/src/main.rs +++ b/examples/recursion/src/main.rs @@ -1059,7 +1059,7 @@ fn tamper_l2( const RECURSION_GUEST_CODEGEN: [(&str, &str); 2] = [ ( "ZEROOS_GUEST_RUSTFLAGS", - "-Cllvm-args=-inline-threshold=1750 -Cllvm-args=-enable-gvn-hoist -Cllvm-args=-enable-dfa-jump-thread -Cllvm-args=-enable-ext-tsp-block-placement -Cllvm-args=-enable-tail-merge=false -Cllvm-args=-split-spill-mode=size", + "-Cllvm-args=-inline-threshold=1750 -Cllvm-args=-enable-gvn-hoist -Cllvm-args=-enable-dfa-jump-thread -Cllvm-args=-enable-ext-tsp-block-placement -Cllvm-args=-enable-tail-merge=false -Cllvm-args=-split-spill-mode=size -Cllvm-args=-riscv-disable-cost-per-use=true", ), ("CARGO_PROFILE_RELEASE_CODEGEN_UNITS", "1"), ];