[Acentelles]

Summary

This branch builds on #1911's recursion example, whose guest verifies one Akita proof of an inner Jolt proof inside Jolt. It makes that verifier guest execute 43.2% fewer trace rows at inner $2^{12}$ (44,896,354 against #1911's 79,032,888) and 41.4% fewer at inner $2^{20}$. No change alters what the verifier checks or the Jolt proof format; every change sits behind a feature of the recursion example and can be turned off.

What changes

Jolt verifier and field code (feature of the recursion example in brackets; dropping it turns the change off):

• BLAKE2b prefix reuse (always on, jolt-inlines/blake2): packed Spongefish prefix compressions are computed once and reused.
• Word decoding (word-decode): Fp128 proof elements are decoded from fixed 16-byte tuples with register-sized accumulators, with the same canonicality checks.
• RAF public inputs reused (always on, stage 5): the instruction read RAF public inputs are computed once.
• Word memory routines (word-memory): exact RV64 doubleword memcpy and memcmp, linked as strong symbols; misaligned copies combine aligned loads by shifts, tails are byte-exact.
• Row pointers kept in registers (rowptr-registers): the field-inline weighted dot keeps each block's row base pointers in registers instead of reloading them on every term.
• Weighted dot by Horner's rule (weighted-dot-horner): when the 64 weights are the powers $1, \alpha, \dots, \alpha^{63}$ and there are at least five rows, each row is evaluated by Horner's rule with $\alpha$ in a register; any other input takes the existing path.
• Three coefficients per Horner step (weighted-dot-horner-triplet, implies the previous one): full five-row blocks of 64 two-limb elements advance three coefficients per step through the existing load-accumulate offsets; other shapes keep the one-coefficient path.
• Immutable recipes for stage claims (immutable-recipes, enabled by the build command, not a Cargo default): the host verifies each embedded proof natively and compiles the closed form of every stage claim expression into the guest as a coefficient table; the guest evaluates claims from the table and falls back to the expression tree for any missing key, too-wide term, zero-knowledge mode or other field. If native verification fails, the tables are empty.
• Terminal relations contracted (terminal-contraction, forwarded to Akita): terminal ring relations are contracted with signed 16-bit coefficients, and the hot weighted-dot kernels and Akita's fused setup-scan job are forced inline.
• Prevalidated catalog view (prevalidated-catalog, forwarded to Akita): the host validates the setup's one-hot catalog view with Akita's canonical loader and records the validated values; the guest reuses them only when the bytes it reads equal the recorded ones, and otherwise runs the validating loader. The generated file stores the recorded view bytes in an 8-byte-aligned static. The setup copy they are compared with is also 8-aligned, so the guest's memcmp always takes its doubleword loop, whatever the data layout of the guest image. The bytes and checks are unchanged.
• Lazy setup-scan errors (lazy-scan-errors, forwarded to Akita): Akita's setup-scan kernels and fused scan job build InvalidProof only on the failure path instead of building it and dropping it on success; same results, checks and first error.
• Digests without a zero fill (digest-nozero, implies prevalidated-catalog, forwarded to Akita): the prevalidated verifier view rebuild takes the row digests as the 32-byte chunks of the view bytes instead of zero-filling a vector and overwriting it.
• Doubleword Golomb-Rice decode (golomb-word, forwarded to Akita): the terminal $z$ decoder uses a doubleword trailing-ones table and packed doubleword stores of four i16 values, with the same checks, conversion order and first error.
• Direct flag-class index in the bytecode fold (bytecode-fold, jolt-claims): the stage 6b bytecode read-RAF fold finds each flag class through a direct word table keyed by the packed instruction tag instead of hashing, with open addressing kept for larger keys; same classes, sums and first error.
• One scale load per equality-fill run (fill-ingress, jolt-field and Akita): new Field::scale_slice_into computes dst[i] = src[i] * scale; the field-inline Fp128 guest loads the scale into a field register once per slice, and Akita's bounded equality fill scales each run through it. The zero and one shortcuts and the checks are unchanged.
• Setup lanes streamed (setup-lane-streams, forwarded to Akita, implies terminal-contraction): the root multi-group setup scan accumulates each lane of a setup segment as one stream, scaling its row weight once per lane, instead of dispatching every setup weight through the per-weight role combination; same field values, checks and errors.
• Compiled carry-state graphs (carry-graph, forwarded to Akita): before building the verifier guest, the host reads the padded trace length shared by the embedded inner proofs and emits Akita's fixed carry-state graphs for that size into a generated source file that the guest compiles in. The guest then evaluates the eq-pair tensor recurrences of the Akita verifier by following these graphs instead of rediscovering the carry states at run time. The graphs depend only on the trace size, never on proof values. If the proofs do not share one supported size, or with RECURSION_CARRY_GRAPH=off, the file holds no graph and every evaluation takes the existing recurrence path; any shape mismatch also falls back. Same field values, checks and errors.
• MLE leaf tiles (mle-leaf-tiles, forwarded to Akita): Akita evaluates the multilinear extensions of low-variable tables through fixed leaf tiles instead of the generic halving fold. Same field values, checks and errors.
• Signed-byte challenge evaluation (signed-byte-sum, jolt-field and Akita): new Field::sum_signed_bytes computes $\sum_i c_i v_i$ for signed byte coefficients $c_i$ (including $-128$; the empty sum is zero). The field-inline Fp128 guest accumulates each nonzero term in the field accumulator register, one operand load per term, and Akita evaluates a sparse challenge at powers through it instead of converting every coefficient to a field element and multiplying. Same field values, checks and errors.
• Setup-weight tiles (setup-weight-tiles, jolt-field and Akita): new Field::add_scaled_slice adds scale * src[i] to dst[i] over the shorter slice. The field-inline Fp128 guest keeps the scale in a field register and adds each product to its destination with the field register add, four elements per tile, then checks every result as a canonical value; Akita's direct setup scan takes its setup weights through it in fixed tiles instead of one weight at a time. Same field values, checks and errors.
• Word-level challenge decode (challenge-word-decode, forwarded to Akita): sampling a signed sparse fold challenge reads the SHAKE output a 64-bit word at a time and decodes positions and signs from the word instead of byte by byte. Same stream consumption, rejections and challenges.

Akita verifier changes, through the Akita pin: factored compression weights (l3-compression-weights), a terminal quotient certificate (l2-terminal-quotient), batched reduced setup rows, signed sparse challenge evaluation, static operator-norm tables, no-carry tensor contraction (tensor-no-carry), tensor equality run accumulation (tensor-eq-runs), structured setup-scan sums of products (setup-sop-structured) a segment-wise shared setup scan (segment-setup), and the Akita halves of the lazy setup-scan errors, digests without a zero fill, doubleword Golomb-Rice decode, equality-fill scaling and streamed setup lanes above, the compiled carry-state graphs (akita-algebra/carry-graph), the MLE leaf tiles (akita-algebra/mle-leaf-tiles), the signed-byte challenge evaluation (akita-challenges/signed-byte-sum), the setup-weight tiles (akita-verifier/setup-weight-tiles) and the word-level challenge decode (akita-challenges/challenge-word-decode).

Verifier guest build, host side only:

• Build settings (guest-codegen; RECURSION_GUEST_CODEGEN=off): one codegen unit, no debug information, inline threshold 1750 and a set of LLVM code-generation options (GVN hoisting, DFA jump threading, ExtTSP block placement without tail merging, size-oriented spill splitting, no RISC-V cost-per-use model, PHI-elimination edge splitting, spill-copy elimination, post-RA scheduling). Inner guests keep the workspace release profile.
• Link order (RECURSION_GUEST_LINK_ORDER=off): the verifier guest is linked with a one-line lld symbol ordering file that places __default_main_entry next to ZeroOS's __main_entry stub, whose j reaches only 1 MiB. No guest or ZeroOS code changes.
• Tooling (RECURSION_WRITE_IF_CHANGED=off): unchanged generated sources are not rewritten; an optional cache (RECURSION_GUEST_ELF_CACHE=<dir>) skips rebuilding an unchanged verifier guest.

Why and benefit

Recursion cost is the number of RISC-V trace rows the verifier guest executes, since that sets the size of the outer proof. Most rows went to the Akita verifier: evaluating the public setup at every fold level, compression and tensor equality weights, re-validating data the host already validated, and field arithmetic with poor register use. The changes remove repeated work, replace arithmetic by cheaper identities that give the same values, and let the compiler keep hot values in registers.

Total trace rows (real plus virtual) of the verifier guest, measured on this branch as published:

	Inner $2^{12}$	Inner $2^{20}$
#1911	79,032,888	not measured
#1911 plus the BLAKE2b prefix reuse (c2c45df3b)	78,267,582	175,797,419
This branch	44,896,354	102,933,720
Reduction	43.2% below #1911	41.45% below c2c45df3b

Per change, measured cumulatively on local builds (Akita from a local checkout; each delta is the change's effect at that point of the stack):

Change	$2^{12}$ rows	Delta	$2^{20}$ rows	Delta
BLAKE2b prefix reuse	78,267,582	-765,306	175,797,419
Factored compression weights, terminal quotient certificate (Akita)	68,927,710	-9,339,872	167,526,238	-8,271,181
Word decoding	68,380,552	-547,158	166,866,977	-659,261
Further Akita verifier changes, RAF reuse	64,137,452	-4,243,100	157,806,316	-9,060,661
Word memory routines	62,367,771	-1,769,681	155,491,473	-2,314,843
Build: inline threshold, GVN hoisting, DFA jump threading, ExtTSP placement, one codegen unit	58,017,137	-4,350,634	148,001,366	-7,490,107
Build: size-oriented spill splitting	57,927,886	-89,251	147,794,518	-206,848
Build: no RISC-V cost-per-use model	57,813,926	-113,960	147,659,422	-135,096
No-carry tensor contraction (Akita)	57,804,752	-9,174	147,597,159	-62,263
Build: split every critical edge in PHI elimination	57,616,581	-188,171	146,936,965	-660,194
Row pointers kept in registers	56,311,592	-1,304,989	142,535,697	-4,401,268
Build: spill-copy elimination, post-RA scheduling, PHI live-out checks	56,218,243	-93,349	142,383,864	-151,833
Build: no debug information	56,217,844	-399	142,383,272	-592
Tensor equality run accumulation (Akita)	55,811,239	-406,605	139,008,802	-3,374,470
Structured setup-scan sums of products (Akita)	54,893,301	-917,938	132,614,570	-6,394,232
Segment-wise shared setup scan (Akita)	53,526,889	-1,366,412	129,678,204	-2,936,366
Weighted dot by Horner's rule	52,555,194	-971,695	125,901,324	-3,776,880
Immutable recipes	51,401,338	-1,153,856	124,690,416	-1,210,908
Terminal contraction, forced inlining (Jolt and Akita)	50,563,175	-838,163	124,193,424	-496,992
Prevalidated catalog view (Jolt and Akita)	49,843,682	-719,493	123,412,491	-780,933
Three coefficients per Horner step	49,136,468	-707,214	120,874,234	-2,538,257
Lazy setup-scan errors, digests without a zero fill, doubleword Golomb-Rice decode, direct flag-class index, one scale load per fill run	48,512,734	-623,734	119,070,883	-1,803,351
Setup lanes streamed (Jolt and Akita)	47,399,234	-1,113,500	112,998,741	-6,072,142
Compiled carry-state graphs (Jolt and Akita)	46,421,484	-977,750	109,528,355	-3,470,386
Catalog view 8-aligned in the local build (as already published)	46,282,585	-138,899	109,387,128	-141,227
MLE leaf tiles, signed-byte challenge evaluation (Jolt and Akita)	45,441,375	-841,210	108,107,329	-1,279,799
Setup-weight tiles, word-level challenge decode (Jolt and Akita)	44,897,729	-543,646	102,935,503	-5,171,826

The last eight rows reach the main entry by a far call instead of the link order (+1 row). Measured separately at inner $2^{12}$, the first three changes of the fifth-to-last row save about 337,000 rows together and its last two about 287,000. The local build of the compiled carry-state graphs predates the alignment of the generated catalog view (see testing): its view landed at an address 2 modulo 8, so its memcmp took the byte loop; the next row adds the alignment. On the published tree, where the view is always 8-aligned, the compiled carry-state graphs saved 1,116,663 rows at inner $2^{12}$ and 3,611,627 at $2^{20}$, the MLE leaf tiles with the signed-byte challenge evaluation saved 842,544 and 1,281,541 against their previous head, and the setup-weight tiles with the word-level challenge decode save 543,132 and 5,171,312 against the previous head (see testing). The published tree is 1,375 rows below the local build at inner $2^{12}$ and 1,783 at $2^{20}$.

Proof sizes: the Jolt proof format is unchanged. The Akita proof is 72,672 bytes at inner $2^{12}$ and 75,817 at $2^{20}$, unchanged by every change after the terminal quotient certificate. The terminal quotient certificate (l2-terminal-quotient) is the one change that grows the Akita proof: it adds 2,992 and 3,056 bytes on this branch, and removes about 6.6 million trace rows at both sizes. Rebased onto current Jolt and Akita main, where Akita's parameters changed, it adds 4,025 bytes at inner $2^{12}$ and 4,009 at $2^{20}$ (about 5% of the Akita proof) and removes 9,784,020 and 9,945,515 trace rows. It is kept deliberately as an accepted trade; every other change leaves the Akita proof size unchanged. Trace rows are not prover time.

How it was tested

• CI runs on this head (link below). The measurements below are of this head. On it, cargo fmt --all --check, the repository's style checker and Clippy with -D warnings (recursion feature sets, default and --no-default-features workspace graphs) pass, and Akita's own Clippy with -D warnings, with Jolt's crates patched in, passes on the pinned Akita commit with its new features off and on.
• Published-tree measurement: a fresh clone of this branch, with Akita and ZeroOS fetched by Cargo at their pins and no local overrides, built and traced once per size on a 16-core AMD Ryzen 9 9950X cloud host, plus a repeat run at inner $2^{12}$ that gave identical rows, guest ELF and proof. All fifteen checks equivalent to CI (style, formatting, the four Jolt Clippy runs, jolt-field Clippy with solinas,signed-byte-sum and with solinas,setup-weight-tiles, and Akita's Clippy without and with the new features, the latter also on akita-challenges and akita-pcs, and with each of the two newest features on its own crate) passed on that host:

  cargo build --locked --profile ci -p recursion --features akita,field-inline,ntt-inline,immutable-recipes
  target/ci/recursion generate --example fibonacci --workdir wd
  RAYON_NUM_THREADS=1 target/ci/recursion trace --embed --expect accept --example fibonacci --workdir wd
  

  Inner $2^{20}$ uses a host-only input override (RECURSION_FIB_N=74858) that is not in this branch.
• The honest proof is accepted at both sizes; a proof with one flipped opening bit is rejected (after 38,746,701 rows). The inner proofs are byte-identical to those of the previous head, and the Akita proof is 72,672 and 75,817 bytes as before; the previous head, built and run on the same host, gives the same inner proofs and Akita bytes and 45,439,486 / 108,105,032 rows, equal to its published figures.
• RV64 equivalence fixture: a RISC-V test guest compares the field-inline weighted dot against an independent reference (powers by repeated multiplication) on 2,060 cases for the three-coefficient step and 112 for the Horner path, for $\alpha \in {0, 1, -1, 17}$, block boundaries and all-zero inputs; all pass with the features on and off. For the streamed setup lanes, an Akita unit test compares the new root setup scan against the direct per-row evaluation at 2,048 random points, plus zero and one challenge cases, and passes with the feature off, on, on with parallel, and on with lazy-scan-errors. For the compiled carry-state graphs, an Akita unit test compiles every graph used at inner $2^{12}$ and $2^{20}$ and compares its evaluation with the recurrence on 2,048 random inputs per graph (135,168 cases) plus constant, alternating and endpoint inputs; other tests check that misses and the work budget keep the fallback. On the published build the graph source the host writes for the guest is byte-identical, at both sizes, to the output of a separately built emitter. For the MLE leaf tiles, an Akita test compares the evaluation with an independent product-of-affine-factors ground truth for up to ten variables and 16 points each and checks that non-domains are rejected; for the signed-byte challenge evaluation, the Akita eval_at_pows tests (seven, including a comparison with the dense polynomial at boundary points) pass on the new module, and a jolt-field test checks the integer contract of sum_signed_bytes for every coefficient from $-128$ to $127$ and the empty sum for both 128-bit Solinas primes. For the setup-weight tiles, a jolt-field test compares add_scaled_slice with the plain loop on random and boundary inputs (scales 0, 1 and $-1$, lengths up to 257, shorter destinations) for both primes, with and without jolt-field's default features, and the Akita root setup scan tests (the 2,048-point row oracle and both lane-stream tests) pass with the tiles on, with and without parallel. For the word-level challenge decode, the Akita sampler and fold-draw tests pass with the feature off, on, and on with parallel, and three new tests check word reads against canonical SHAKE output at every lane and rate boundary, rejection against the byte reference with the same stream position, and signs against the scalar path with exact consumption. New tests also cover word encoding, the word transcript and the word memory routines (jolt-platform/tests/word_memory.c).
• Features off: building this head with setup-weight-tiles and challenge-word-decode off gives 45,441,307 rows at inner $2^{12}$ and 108,107,261 at $2^{20}$, with the same proofs: 1,821 and 2,229 rows above the previous head. That difference comes with the new Akita pin, not with the features: the previous head with only the pin moved gives exactly the same rows (a new Akita package id moves the guest image layout), and its guest ELF differs from the feature-off build in only 4 bytes. Against this feature-off build the two features save 544,953 and 5,173,541 rows, 1,307 and 1,715 more than in the local build; against the previous head the published change is 543,132 and 5,171,312 rows. With tensor-eq-runs, setup-sop-structured, segment-setup, weighted-dot-horner or immutable-recipes off, the guest ELF is byte-identical to the build without that change; RECURSION_GUEST_CODEGEN=off reproduced the earlier rows and ELF exactly.
• Link-order control: with RECURSION_GUEST_LINK_ORDER=off the same build fails to link, because the stub's j to __default_main_entry would need 1,109,678 bytes of reach; with the ordering file it links at both sizes.
• Local-build figure: the same changes built from a local Akita checkout, with the main entry reached by a far call instead of the link order, gave 46,421,484 rows at inner $2^{12}$ and 109,528,355 at $2^{20}$ before the last two features (the compiled carry-state graphs save 977,750 and 3,470,386 rows there; with the catalog view aligned, the MLE leaf tiles and signed-byte challenge evaluation save 841,210 and 1,279,799, and the setup-weight tiles with the word-level challenge decode 543,646 and 5,171,826). The local build gives 44,897,729 rows at inner $2^{12}$ and 102,935,503 at $2^{20}$; the published tree is 1,375 and 1,783 rows below it. Proofs are identical.
• Published-versus-local gap, now fixed. At the previous head the published tree ran 138,358 and 140,686 rows above the local build. A per-function row count of both builds traced the whole gap to data layout. 138,899 and 141,227 of those rows came from one memcmp: it compares the generated catalog view (11,471 bytes at inner $2^{12}$, 11,658 at $2^{20}$) with its copy in the embedded setup. The generated view was a byte array with alignment 1. In the published image the linker happened to place it at an address 2 modulo 8, while the setup copy is 8-aligned. With the two pointers misaligned relative to each other, memcmp used its byte loop, about 13 rows per byte against under 1 on the doubleword loop. The remaining 541 rows were two smaller memcpy layout effects and the entry stub. The code was the same on both sides. The view bytes are now 8-aligned. In both guest images both copies sit at addresses divisible by 8, and the generator has unit tests for the alignment and the generated text.

Risks

• Unmerged Akita pin. Akita is pinned at 13128559, a commit on a fork fetched through the LayerZero-Labs/akita URL. Seven of its changes are in the open Reduce recursive verifier rows and update the Jolt pin LayerZero-Labs/akita#277. Everything else in the pin is not yet in an Akita PR, notably the terminal quotient certificate (kept out of feat: Jolt logo #277 because it adds bytes to the Akita proof), the segment-wise setup scan, the inline fused setup-scan job, the prevalidated verifier view, and the five commits that add the Akita side of the lazy setup-scan errors, digests without a zero fill, doubleword Golomb-Rice decode and equality-fill scaling (plus one comment-only commit), the two commits that add the streamed setup lanes, the commit that adds the compiled carry-state graphs, the commit that adds the MLE leaf tiles and signed-byte challenge evaluation, and the two commits that add the setup-weight tiles and the word-level challenge decode. The pin should be moved to merged Akita before or soon after this merges.
• Terminal quotient certificate changes the inner Akita proof format (new protocol identifier, +2,992 / +3,056 bytes). Turn off l2-terminal-quotient to keep the earlier format.
• Link order relies on lld's --symbol-ordering-file and Rust's per-function sections, for the verifier guest only. A ZeroOS entry stub with longer reach (for example a tail call) would make it unnecessary. The guest target path must not contain whitespace; the host checks this.
• Compiled records are not yet bound by an outer proof. The recipe tables, the prevalidated catalog record and the carry-state graphs are derived by the host and compiled into the guest. A clean rebuild reproduces them, a stream with another proof size's setup is rejected, and mismatched tables fall back to the canonical path. Binding the compiled guest and its records inside an outer proof statement is owed once this example has an outer proving path.
• Tuned by measurement. The build settings and forced inlining were chosen by measuring rows on this guest; they may not help other guests, and a toolchain upgrade can change their effect (inline thresholds of 2000 and above fail to link). Only the inner Fibonacci example at $2^{12}$ and $2^{20}$ was measured.
• Eleven more verifier features, default on. Each was measured to keep the proofs, transcripts and Akita proof bytes; the doubleword Golomb-Rice decode and the fill scaling change guest code paths that only the accept, reject and repeat runs cover (no dedicated RV64 fixture), and the streamed setup lanes, the compiled carry-state graphs, the MLE leaf tiles, the signed-byte challenge evaluation, the setup-weight tiles and the word-level challenge decode are covered by the host-side unit tests above, not by an RV64 fixture. The field-inline Fp128 sum_signed_bytes and add_scaled_slice run only in the guest and are covered by the accept, reject and repeat runs.
• word-memory overlaps perf(runtime): accelerate general RV64 guest memcpy and memmove #2142 on memcpy; with both, this branch's memcpy becomes perf(runtime): accelerate general RV64 guest memcpy and memmove #2142's fallback.

How to turn it off

• Everything: build with --no-default-features --features akita,field-inline,ntt-inline.
• One change: drop its feature from the default set (l3-compression-weights, l2-terminal-quotient, word-decode, word-memory, guest-codegen, tensor-no-carry, rowptr-registers, tensor-eq-runs, setup-sop-structured, segment-setup, weighted-dot-horner, weighted-dot-horner-triplet, terminal-contraction, prevalidated-catalog, lazy-scan-errors, digest-nozero, golomb-word, bytecode-fold, fill-ingress, setup-lane-streams, carry-graph, mle-leaf-tiles, signed-byte-sum, setup-weight-tiles, challenge-word-decode; digest-nozero needs prevalidated-catalog, setup-lane-streams needs terminal-contraction); turning off the Horner rule means dropping both Horner features.
• Immutable recipes: omit immutable-recipes, or set RECURSION_IMMUTABLE_RECIPES=off to build with empty tables.
• At run time: RECURSION_GUEST_CODEGEN=off, RECURSION_GUEST_LINK_ORDER=off (links only while less than 1 MiB of code precedes the main entry, so not with prevalidated-catalog), RECURSION_WRITE_IF_CHANGED=off and RECURSION_CARRY_GRAPH=off (no graph: the recurrence path). A caller's ZEROOS_GUEST_RUSTFLAGS overrides the build settings.

Evidence

https://github.com/a16z/jolt/pull/2143/checks