Recursive verification of Ix proofs at kernel scale by arthurpaulino · Pull Request #503 · argumentcomputer/ix

arthurpaulino · 2026-07-20T14:43:23Z

This branch makes the MultiStark verifier runnable inside IxVM — as an
Aiur program whose execution can itself be proven — and then optimizes
recursive verification from "never finishes" to a complete, sound,
end-to-end run: a kernel-scale proof of Nat.add_comm is proven,
recursively verified in-circuit, and the verifier's execution proven in
4:00 wall clock at 315.9 GiB peak RSS on a 495 GiB host, producing a
12.3 MB outer proof that natively verifies in 94 ms.

What's here

Foundation (67dcde3): ix codegen generates Rust for the
Ix/MultiStark verifier circuits, and the IOBuffer (proof bytes +
verifying key) is populated natively in Rust, so the recursive verifier
runs as compiled code over IO advice instead of interpreted source.

Optimization campaign, each step gated on the reference-vector
self-tests, the e2e accept/tamper/codegen-parity suite, the kernel FFT
pins, and toy + kernel-scale canaries:

Native Goldilocks arithmetic (5335a17, execute 5.3×): the Aiur
native field is Goldilocks, so field ops become native ops with
byte decomposition kept only where the protocol needs canonical bytes.
Indexed proof reads with unconstrained byte fetches (d674f97):
proof-stream bytes arrive by indexed io_read instead of walking a
per-byte list; fetching is unconstrained, with soundness recovered by
the challenger binding.
Direct blake3 for Merkle 2-to-1 compressions (b96eb37) and
lane-granularity leaf hashing (f6a62b1): MMCS hashing works on
64-byte blocks and u64 lanes instead of byte streams.
Linear challenger observation (f89658f): observation buffers are
prepend-built and concatenated once — the quadratic snoc-per-item
transcript growth was the original "never finishes" cause.
Segmented, hugepage-backed, hash-caching QueryMap (9161a9f):
mmap'd fixed segments with MADV_HUGEPAGE before first touch and
stored per-entry hashes, removing the memoization table as the
system-level bottleneck.
Toplevel pruning (8aca57e): production VMs keep only the
reachable closure of their entrypoints.
Verifying-key ingestion by IO slices and indexed reads
(e7c83f1, execute −12%): the vk is hashed straight from the IO
arena in 64-byte blocks and parsed via indexed reads.
Native extension-field representation (7d12c1f, execute −40%,
FFT −27%): Ext becomes a native (G, G) pair inside the arithmetic
core; canonical bytes survive only at true protocol boundaries
(ingest, challenger observation, digest comparison).
Concat-free leaf hashing (555af77): the lane hasher walks
rows-of-lanes directly instead of materializing a concatenated list
per FRI query.
Sparse kernel proofs (2c6267c, inner proof −33%): adopts
multi-stark's per-proof circuit activation — circuits the checked
claim never touches emit empty traces and are neither committed,
opened, accumulated, nor constraint-evaluated. The activation bitmap
is bound into the Fiat-Shamir transcript before any challenge; the vk
stays canonical so the recursion statement's system_digest binding
is unchanged.
Trivial-helper inlining (25479ff): relic constant helpers from
the byte-array era become literals; verifier width −172 columns.
Split-streams vk encoding (ccaaa05, vk 7.8× smaller): the old
format was 96% fixed-width padding around 3% payload. Each field
class now lives in a per-circuit fixed-width segment (1-byte packed
tags, u16 indices, size-classed constants, u32 metadata; derivable
degree_multiple dropped), so every in-circuit read stays a
static-size io_read. This removed the dominant blake3 cost — the
vk digest binding — and is what lets the outer prove fit in memory.

Measurements (kernel-scale `Nat.add_comm`, q=100, logBlowup=2)

Recursive execution of the in-circuit verifier:

Milestone	Execute	FFT cost	Inner proof	vk
Campaign start	never finishes	—	35.02 MB	8.38 MB
Linear challenger + native G + IO reads	59.7 s	229.5B	35.02 MB	8.38 MB
vk ingestion overhaul	52.7 s	222.0B	35.02 MB	8.38 MB
Native extension field	31.5 s	162.0B	35.02 MB	8.38 MB
Concat-free leaf hashing	29.0 s	158.6B	35.02 MB	8.38 MB
Sparse proofs	26.0 s	149.9B	23.29 MB	8.38 MB
Split-streams vk (final)	18.9 s	99.8B	23.29 MB	1.08 MB

End-to-end sound recursion (first ever completion; previously the outer
prove OOM'd the 495 GiB host):

Phase	Result
Inner prove	2.0 s, 23.29 MB proof
Recursive execute (in-circuit verify)	19.8 s
Outer prove (over that execution)	216.9 s
Outer proof	12.3 MB, native verify 94 ms
Total	4:00.42 wall, 315.9 GiB peak RSS

The remaining recursive-execute cost is dominated by MMCS/leaf/
challenger blake3 (irreducible under the blake3-PCS choice) and the FRI
query loop; the vk — formerly ~35% of FFT — is now ~7%. Merkle-izing
the vk was measured and deliberately rejected: at the new sizes, auth
paths cost as much as the inactive bytes they'd skip for kernel-scale
claims, and proof folding (the intended future) converges to full
activation where flat hashing is optimal.

Testing

lake test -- --ignored multi-stark — reference-vector self-tests +
differential hash tests.
lake test -- --ignored recursive-verifier — e2e accept, tamper
rejections, codegen↔interpreter parity.
lake test / lake test -- --ignored ixvm — kernel suites, FFT pins.
cargo test -p aiur vk_codec — codec round-trip fixpoint,
degree-recomputation equality, malformed-input rejection.
lake exe bench-recursive-verifier --queries 100 --execute-only — toy
canary (0.68 s / 3.96B FFT, RAYON_NUM_THREADS=1).
lake exe ix codegen --check — generated Rust in sync.
Measurement tooling: IX_DUMP_RECURSION_IO=<dir> dumps the
proof/vk/claims advice blobs for offline format analysis.

arthurpaulino · 2026-07-20T14:45:55Z

!benchmark aiur-recursive

argument-ci-bot · 2026-07-20T14:48:45Z

`!benchmark` — main vs `5eb7078`

backends: aiur-recursive · envs: InitStd · set: primary · shard: 0

`aiur-recursive` · `InitStd` — main from: base run @ `a75cb04` (not on bencher)

proof	recursive-prove-time (main)	recursive-prove-time (PR)	Δ%	recursive-peak-ram (main)	recursive-peak-ram (PR)	Δ%	recursive-proof-size (main)	recursive-proof-size (PR)	Δ%	recursive-verify-time (main)	recursive-verify-time (PR)	Δ%	recursive-execute-time (main)	recursive-execute-time (PR)	Δ%	recursive-fft-cost (main)	recursive-fft-cost (PR)	Δ%	prove-time (main)	prove-time (PR)	Δ%	proof-size (main)	proof-size (PR)	Δ%	verify-time (main)	verify-time (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%
`factorial-q100-b2`	31.496 s	6.370 s	-79.8% (4.94× faster) 🟢	74.73 GiB	19.22 GiB	-74.3% (3.89× smaller) 🟢	15.84 MiB	11.70 MiB	-26.1% (1.35× smaller) 🟢	113.6 ms	81.9 ms	-27.9% (1.39× faster) 🟢	9.181 s	460.6 ms	-95.0% (19.94× faster) 🟢	17.96B	3.94B	-78.1% (4.56× fewer) 🟢	214.4 ms	244.9 ms	+14.2% (1.14× slower) ⚠️	848.61 KiB	848.62 KiB	+0.0%	6.4 ms	6.4 ms	+0.5%	405.63 MiB	409.39 MiB	+0.9%
`square-q100-b1`	23.142 s	5.248 s	-77.3% (4.41× faster) 🟢	43.47 GiB	13.39 GiB	-69.2% (3.25× smaller) 🟢	15.76 MiB	11.63 MiB	-26.2% (1.35× smaller) 🟢	100.9 ms	82.3 ms	-18.5% (1.23× faster) 🟢	8.082 s	407.2 ms	-95.0% (19.85× faster) 🟢	15.65B	3.28B	-79.0% (4.77× fewer) 🟢	184.5 ms	142.0 ms	-23.1% (1.30× faster) 🟢	782.05 KiB	782.06 KiB	+0.0%	5.6 ms	5.8 ms	+2.2%	309.43 MiB	306.90 MiB	-0.8%

2 proofs · 1 with regressions · 2 with improvements (|Δ| > 3.0% on any metric).

Workflow logs

arthurpaulino · 2026-07-20T20:15:29Z

!benchmark aiur-recursive

argument-ci-bot · 2026-07-20T20:18:53Z

`!benchmark` — main vs `f24240c`

backends: aiur-recursive · envs: InitStd · set: primary · shard: 0

`aiur-recursive` · `InitStd` — main from: base run @ `77cdce3` (not on bencher)

proof	recursive-prove-time (main)	recursive-prove-time (PR)	Δ%	recursive-peak-ram (main)	recursive-peak-ram (PR)	Δ%	recursive-proof-size (main)	recursive-proof-size (PR)	Δ%	recursive-verify-time (main)	recursive-verify-time (PR)	Δ%	recursive-execute-time (main)	recursive-execute-time (PR)	Δ%	recursive-fft-cost (main)	recursive-fft-cost (PR)	Δ%	prove-time (main)	prove-time (PR)	Δ%	proof-size (main)	proof-size (PR)	Δ%	verify-time (main)	verify-time (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%
`factorial-q100-b2`	32.605 s	6.377 s	-80.4% (5.11× faster) 🟢	75.01 GiB	19.18 GiB	-74.4% (3.91× smaller) 🟢	15.84 MiB	11.39 MiB	-28.1% (1.39× smaller) 🟢	109.7 ms	83.7 ms	-23.8% (1.31× faster) 🟢	9.151 s	445.7 ms	-95.1% (20.53× faster) 🟢	17.99B	3.88B	-78.4% (4.63× fewer) 🟢	218.0 ms	221.0 ms	+1.4%	848.61 KiB	848.62 KiB	+0.0%	6.4 ms	6.0 ms	-6.8% (1.07× faster) 🟢	416.47 MiB	409.77 MiB	-1.6%
`square-q100-b1`	23.673 s	5.053 s	-78.7% (4.69× faster) 🟢	43.51 GiB	14.41 GiB	-66.9% (3.02× smaller) 🟢	15.76 MiB	11.32 MiB	-28.2% (1.39× smaller) 🟢	95.6 ms	78.7 ms	-17.7% (1.21× faster) 🟢	8.027 s	412.2 ms	-94.9% (19.48× faster) 🟢	15.31B	3.44B	-77.5% (4.45× fewer) 🟢	129.2 ms	173.2 ms	+34.1% (1.34× slower) ⚠️	782.05 KiB	782.06 KiB	+0.0%	5.6 ms	5.1 ms	-8.9% (1.10× faster) 🟢	320.54 MiB	319.54 MiB	-0.3%

2 proofs · 1 with regressions · 2 with improvements (|Δ| > 3.0% on any metric).

Workflow logs

…advice Give the recursive verifier the same two treatments the IxVM kernel already has: - `ix codegen` now emits a second target: the MultiStark toplevel compiled to `crates/ixvm-codegen/src/aiur_multi_stark.rs` (246 fns), with `--check` covering both files. The emitter is unchanged — each generated module is self-contained and module-scoped, so the two never collide. - The proof/vk/claims advice buffer is built natively in Rust (`verifier_io_buffer`: channel 0 = proof, 1 = vk, 2 = claims, key [0]) instead of boxing every byte into a Lean `G` and marshalling the whole buffer across FFI. New externs `rs_aiur_multi_stark_execute` / `rs_aiur_multi_stark_prove` take the raw byte blobs, route through the codegen'd verifier (or the interpreter via `useBytecode`), and return no buffer — the verifier only reads its advice. Wired into bench-typecheck Phase 3 (which also prints the per-circuit FFT breakdown under --texray), bench-recursive-verifier (new --use-bytecode escape hatch), and Tests/MultiStark, whose end-to-end suite now additionally asserts codegen ↔ interpreter parity on output and per-circuit query counts. Measured on the factorial toy at q=100: execute 12.4s (interpreter) → 10.2s (codegen'd). The gap is small because verifier execution is memo-table-bound, not dispatch-bound; the row-count and probe-cost reductions that actually move it are follow-up work.

… 5.3x) The verifier emulated Goldilocks on u8 limbs — every field multiply was two 64x64 schoolbook byte products (mul128 + reduce128's internal mul128-by-EPSILON), and gl_inverse was ~63 of those via Fermat — for field-agnosticism, even though Aiur's own field IS Goldilocks (aiur::G = p3_goldilocks). Those limb circuits (add16/mul1/mul128/ reduce128/add8/sub8/select8) were 63.5% of the verifier's total FFT cost. Rewrite the gl_/eg_ ops on native field arithmetic, keeping the byte-shaped interface (canonical [U8; 8] at every boundary — the transcript, blake3, and wire format consume canonical bytes): - gl_val recomposes canonical bytes to a native value (linear sum, memoized); gl_of_val decomposes back via a new unconstrained hint op, pinned by u8 range checks + a recomposition equality + a canonicality (< p) check — together forcing the unique canonical decomposition. - gl_add/sub/neg/mul/sq: recompose, one native op, decompose. - gl_inverse/eg_inverse: the inverse is hinted, never computed — pinned branchlessly by t = x*i - 1; x*t == 0; i*t == 0 (forces i = x^-1 for x != 0 and i = 0 for x = 0, matching Fermat's 0 -> 0). - eg_mul/eg_inverse compute the extension arithmetic natively end-to-end; only the two result coordinates are decomposed. - gl_reduce collapses to recompose (which wraps once for values in [p, 2^64)) + decompose; gl_is_zero/gl_eq to a single eq_zero. - The rejection-sampling canonicality test in ch_sample_field uses the new gl_lt_p (two eq_zero byte-sum tests) instead of a sub8 borrow. - The dead limb helpers are deleted (a dead fn is still a committed circuit). Two new Aiur hint ops carry the advice, computed natively by the Rust runtime (interpreter, codegen'd kernels, and trace population share the same intrinsics), producing zero trace rows: - unconstrained_g_to_bytes: the 8 LE bytes of the canonical u64 value (8 auxiliary columns, no constraints); - unconstrained_g_inverse: the field inverse with 0 -> 0 (1 auxiliary column, no constraints). Both are appended last in Bytecode.Op and the Rust Op enum (FFI decode is positional: tags 29/30). The Lean reference evaluators implement them via new G.toLeBytes/G.pow/G.inverse semantic models. Measured on bench-recursive-verifier --queries 100 --execute-only: execute 10.2s -> 1.94s (5.3x), total FFT cost 18.4B -> 6.26B (2.9x), memo-table hits 69.7M -> 2.9M. Verifier cost is now dominated by blake3 (~65%) and byte-stream cons cells (~18%). The multi-stark self-tests (reference vectors for gl/eg add/sub/mul/ inverse/div), the end-to-end recursive-verifier suite (accept, two tamper rejections, codegen-vs-interpreter parity on output and query counts), and the default test suite all pass. The IxVM kernel is untouched: aiur_ixvm.rs regenerates byte-identical, so kernel FFT pins are unaffected.

The proof deserializer materialized the whole advice stream as a per-byte ListNode chain (one memory store per byte via #read_byte_stream, then one load per byte as read_u8 walked it — at kernel scale, 35.6M of each), even though io_read can already pull fixed-size chunks straight from the IO arena by offset. The read_proof family now threads a channel-0 byte offset instead of a stream pointer and reads fixed-size chunks (io_read's length is static): 1 byte for tags, 8 for u64s, with 16/32-byte values composed from u64 reads. Variable-length content loops a fixed-size read per element, as the stream readers always did. No byte chain is ever materialized for the proof. The leaf fetch primitives (read_u8_at / read_u64_at) are invoked UNCONSTRAINED — the proof is advice, so fetching its bytes needs no rows (the same trust boundary as the former #read_byte_stream); the parse structure above them stays constrained, and the entrypoint still asserts full consumption (end offset = idx + len). The byte-stream primitives remain for the vk/claims streams, whose bytes are digest-bound and flow through blake3 as materialized streams anyway (read_claims gets its own u64-list loop back). Measured on bench-recursive-verifier --queries 100 --execute-only: execute 1.94s -> 1.65s, total FFT cost 6.26B -> 5.62B, memory[3] height 2.92M -> 2.04M. Both test suites (reference-vector self-tests; e2e accept/tamper/codegen-parity) pass; the kernel codegen is byte-identical.

mmcs_compress serialized its two 32-byte digests into a cons-list, which blake3 then walked byte-by-byte into an accumulator list and re-loaded into a block — ~4 memory ops for each of the 64 bytes, per compression, per Merkle level, per FRI query. The input is always exactly 64 bytes = one block of a single chunk, so compress it with one direct blake3_compress call using the same parameters that input takes through blake3_compress_chunks (cv = IV, counter = 0, block_len = 64, flags = CHUNK_START + CHUNK_END + ROOT), with the block words assembled straight from the digest lanes. No byte list is built, walked, accumulated, or re-materialized; the now-unused b3_digest_bytes_onto is deleted. Measured on bench-recursive-verifier --queries 100 --execute-only: execute 1.65s -> 1.23s, total FFT cost 5.62B -> 4.59B, memory[3] height 2.04M -> 767K. pcs_hash_test/pcs_merkle_test pin the compression against the Rust reference values (root + tamper) and pass, as do the e2e accept/tamper/codegen-parity suite; kernel codegen byte-identical.

mmcs_hash_row serialized its lane list into a byte cons-list that blake3 then walked, re-accumulated, and re-materialized — ~4 memory ops per byte. Leaf input is a List<U64> of 8-byte lanes, so blocks (8 lanes) can be assembled straight from the lane values at one list load per lane. b3_lanes mirrors blake3_compress_chunks/_block/_finish at block granularity with the identical flag schedule (CHUNK_START/CHUNK_END/ROOT, 16-block chunks, partial-block zero padding with the real byte length) and reuses blake3_compress and the Layer chunk-tree fold unchanged. The new lane_hash_test differentially pins b3_lanes against byte-granular blake3 at every structural boundary: empty input, partial/exact/over block, partial/exact/over chunk, a 2-chunk varied-byte row, and a 4-chunk row (deeper layer fold), with index-varied lane bytes so lane- or word-order bugs change the digest. Toy-canary neutral (leaf rows there are a few hundred bytes — under one chunk), by design: the target is kernel-scale recursion, where opened rows are ~240KB per FRI query and per-byte leaf plumbing dominates the non-compress cost. pcs_hash_test/pcs_merkle_test (Rust reference vectors) and the e2e accept/tamper/codegen-parity suite pass; kernel codegen byte-identical.

Observing a value appended it to the challenger input buffer with snoc_b8 = list_concat(input, ...), which walks and REBUILDS the entire accumulated buffer per 8-byte observation — quadratic in transcript size. Invisible on toy proofs, catastrophic at kernel scale: the post-ζ pass observes every opened value (tens of thousands of ext coordinates across ~800 circuits), and that single stage ran for 20+ minutes building billions of cons cells before the first FRI query could start. The input buffer collapses to the 32 digest bytes on every flush (HashChallenger: input := output := blake3(input)), so large inputs exist only DURING an observation batch. Each batch is now built front-to-back with the O(1) prepend helpers (round_onto / points_onto / ext_row_onto / prep_onto / accs_onto, same composition style as the seed transcript) and appended with ONE list_concat over the ~32-byte input: linear overall. The per-item observe helpers this replaces (obs_round/obs_points/obs_ext_row/obs_prep, snoc_accs) are deleted; byte order is unchanged, which pcs_challenger4_test (challenger continuation vs the Rust reference) and the e2e honest-accept (byte- exact Fiat-Shamir agreement with the prover) both pin. Kernel-scale effect (recursive verification of Nat.add_comm, execute): DID NOT FINISH before (killed at 20+ min inside the observation pass); completes in 99.9s after this change. Toy canary: 1.22s -> 1.13s, FFT 4.56B -> 4.20B. Kernel codegen byte-identical.

Three container-level costs showed up at the 100GB+ scale the kernel workloads reach: - keys/outs/mults were single Vecs: growth-doubling a multi-GB arena memmoves the whole thing and transiently needs 2x the RSS — which is what actually OOMs first. - hashbrown table growth re-hashed every key FROM the arena (full sequential passes over tens of GB, log-many times). - with 4K pages, every random probe pays a 4-level page walk on top of its DRAM miss; the process mapped zero hugepages (mimalloc commits its segments itself, so a post-hoc madvise through the global allocator never takes effect). Entries now live in fixed-size segments (2^20 entries; an entry never straddles a segment) mmap'd directly from the kernel with MADV_HUGEPAGE applied before first touch, bypassing the allocator. Growth allocates a fresh segment — no copy, no transient spike; capacity is virtual reservation only, so idle circuits stay tiny. Each entry's key hash is stored alongside (8B), making table growth a cheap sequential re-insert with no arena traffic. Public API unchanged; entry index remains insertion order (the memory-circuit pointer contract). Measured: toy verifier canary execute 1.13s -> 0.88s (FFT identical — the record contents don't change); kernel-scale recursive verification of Nat.add_comm 99.9s -> 60.9s (1.64x). Default suite + reference- vector self-tests + e2e accept/tamper/parity all pass.

Every function in a compiled toplevel becomes a committed circuit whose openings pad every proof — used or not. The merged toplevels carried test/bench entrypoints (blake3_test/bench, sha256_test/bench, rbtree_map_test, kernel_unit_tests, ixon_serde_test, ixon_serde_blake3_bench) and their exclusive call closures into every production system and its digest. Source.Toplevel.prune keeps only the functions reachable from a given root set (worklist over a Term/Pattern global collector; data types and aliases are kept wholesale — they cost nothing). Production toplevels are now pruned: - IxVM.ixVM = ixVMFull pruned to {verify_claim, verify_const}: 793 -> 761 circuits, inner proof 35.63MB -> 35.02MB. - MultiStark.multiStark = multiStarkFull pruned to {verify_multi_stark_proof}: 249 -> 231 circuits. The recursive verifier feels the kernel prune directly: 32 fewer circuits in the verifying key means 32 fewer OOD constraint evaluations per verification and fewer opened lanes hashed per FRI query. Observed recursive-fft-cost on Nat.add_comm: 233.58B after, vs 234.23B and 238.10B samples before — the direction is consistent, but single samples sit inside the documented ~±15% Merkle-path drift of the nondeterministic parallel prover, so the exact margin is not pinned here. Harnesses that run test/bench entries switch to the unpruned Full toplevels (interpreter execution): the ixvm suite splits its exec cases (kernel_unit_tests, ixon_serde_test -> full env) from the codegen-coupled checks/claims/arena/parity (pruned env, the one ix codegen mirrors); the kernel_unit_tests parity fixture is dropped (parity needs entries present in the codegen'd kernel; the 55 pinned kernel-check fixtures remain); bench-ixvm proves through the interpreter. Kernel FFT pins hold exactly (pruned circuits carried zero execution cost — the win is proof bytes, verifier-side work, and digest hygiene, compounding with any future per-proof sparse-commitment support). All suites green: default, ixvm (596), multi-stark reference vectors, recursive-verifier e2e.

The vk (channel 1, ~9.4MB at kernel scale: constraint ASTs for 761 circuits) still took the old byte path after the proof channel was overhauled: a per-byte ListNode stream, read_u8 walking (8.4M rows), and byte-wise blake3 absorption through the accumulator loop (blake3_compress_chunks, 9.7M rows — 43% of all blake3 compressions were the vk digest binding's plumbing). Two changes, mirroring the proof-channel recipe: - b3_io(ch, idx, len): blake3 straight from an IO channel arena — 64-byte io_read blocks fed directly to blake3_compress with the byte driver's exact flag schedule; the (cold, once-per-hash) sub-64-byte tail reuses pad_block/bytes_to_block. No byte list is materialized, walked, accumulated, or re-loaded. The digest binding becomes b3_io(1, sidx, slen) with a full-consumption offset assert. - read_system converted to indexed channel-1 reads: every reader threads a byte offset and pulls fixed-size chunks (1/4/8-byte leaf fetches, unconstrained — the same advice trust boundary as the proof readers; the digest binding is what makes the bytes meaningful). The now-dead stream digest/cap readers are deleted. A new io_hash_test differentially pins b3_io against byte-granular blake3 at eleven structural sizes (empty, partial/exact/over block, partial/exact/over chunk, multi-chunk layer fold) over io_write-seeded bytes; pcs_challenger4_test and the e2e honest-accept pin the Fiat-Shamir byte-exactness end to end. Kernel-scale recursive verification of Nat.add_comm: execute 59.7s -> 52.7s, FFT 229.5B -> 222.0B; blake3_compress_chunks, read_u8, and the vk's memory[3] share drop out of the top contributors (the remaining vk cost is the irreducible blake3 of its bytes). Toy canary unchanged (its vk is tiny). All suites green; kernel codegen byte-identical.

Every gl_/eg_ op eagerly decomposed its result to canonical bytes — 15.1M gl_of_val/gl_lt_p/gl_val rows at kernel scale — but computed field values almost never need bytes: opened values and sampled challenges ARRIVE as bytes (converted inward once), and computed intermediates (OOD folds, FRI folds, fingerprints, accumulators) flow only into more arithmetic or terminal eq_zero comparisons. Goldilocks is now a native field value (type Goldilocks = G) and ExtGoldilocks a native pair ([G; 2]): gl_add/sub/neg/mul/sq are single native ops, eg_mul is four native muls + adds (w74 -> w15-class), inverses stay hinted (unconstrained_g_inverse + branchless pin) with no decomposition, and gl_is_zero/gl_eq/eg_eq are plain eq_zero. Byte form survives only at true boundaries: - ingest: wire limbs fold to native with gl_val/limb_to_field (the field sum wraps mod p — recomposition IS the reduction; the old gl_reduce disappears), read_ext/read_field produce native directly, and opened base rows convert at the reduced-opening seam (lanes_to_gl); - egress: challenger observations of computed/parsed ext values and the FRI commit-phase leaf rows (flatten2) decompose per coordinate with gl_to_bytes (the pinned unconstrained_g_to_bytes gadget) — tens of K sites instead of 15M; - canon_lanes = gl_to_bytes(gl_val(x)) (leaf-hash canonicalization); two_adic_gen's table becomes native G literals; ch_sample_field still returns canonical bytes (rejection sampling + re-observation need them) and callers fold inward once. The reference-vector self-tests keep their byte vectors (folded with gl_val, injective on canonical bytes) and all pass; the e2e suite (byte-exact Fiat-Shamir accept, two tamper rejections, codegen parity on output + query counts) passes. Measured: toy canary execute 0.78s -> 0.71s, FFT 4.18B -> 3.90B; kernel-scale recursive verification of Nat.add_comm execute 52.7s -> 31.5s, FFT 222.0B -> 162.0B, verifier system width 16007 -> 11568 (ro_fold w239 -> w57, bucket_update w120 -> w36; the generated Rust shrinks 1.53MB -> 1.27MB). blake3 is now ~81% of the remaining cost — the floor under the blake3 constraint. Kernel codegen byte-identical.

leaf_hash_at materialized the concatenation of every selected row's lanes per FRI query (concat_at + concat_at_step, ~10M rows at kernel scale) and then copied it again through canon_lanes, just so the lane hasher could walk one flat list. The leaf hash now selects the target-height rows as a pointer list (select_rows, which also drops empty rows so exhaustion is a plain Nil check) and hashes their lanes directly: rows_pop pops one canonicalized lane across row boundaries, and b3_rows_chunks gathers each 64-byte block with eight cross-row pops — same flag schedule and Layer fold as the lane driver. No concatenated or canonicalized copy of the opened rows is ever built. The concat/canon/lane machinery stays defined for the differential reference: the new rows_hash_test pins b3_rows(select_rows(...)) against mmcs_hash_row(canon_lanes(concat_at(...))) across shapes (all/none/some rows selected, an empty row mixed in, exact-block totals, a multi-chunk total exercising the layer fold) — and the entrypoint-closure prune keeps it all out of the production system (230 -> 227 circuits). Measured: kernel-scale recursive verification of Nat.add_comm execute 31.5s -> 29.0s, FFT 162.0B -> 158.6B; toy canary neutral (its leaf rows are a few lanes). All suites green (12 self-tests, e2e accept/tamper/parity); kernel codegen byte-identical.

Adopt multi-stark's sparse systems (per-proof circuit activation): a circuit with no queries now yields an EMPTY trace instead of a padded height-1 one, so the prover deactivates it — it is neither committed, nor opened, nor accumulated, nor constraint-evaluated. For a kernel proof this stops paying per-query openings for every circuit the checked claim never touches. - Witness side: function and memory witness_data emit height-0 matrices for unqueried circuits (the fixed 256/65536-row byte tables stay always-active). - Wire format: Proof gains the leading activation bitmap; the Lean deserializer reads it first (u64 count + one 0/1 byte per circuit). - In-circuit verifier: the bitmap is asserted boolean, length-checked against the canonical circuit list, observed into the Fiat-Shamir replay right after the shape words (before any commitment or challenge), and the verifying key's circuit and preprocessed-index lists are filtered to the active subset ONCE — everything downstream (OOD loop, bucket/heights construction, opened-value indexing) runs on the filtered lists unchanged, since every per-circuit proof sequence is indexed by active position. The vk itself stays canonical, so the recursion statement's system_digest binding is unchanged. The multi-stark dependency is pinned to the sparse-systems rev (branch ap/sparse-systems, 7a2a3c8); repoint at main once it merges upstream. Measured on Nat.add_comm at kernel scale (q=100): inner proof 35.02MB -> 23.38MB (-33%), native verify 0.23s -> 0.15s, recursive verification execute 29.0s -> 26.0s, FFT 158.6B -> 149.9B. The claim still activates the kernel's core machinery (~2/3 of total circuit width), so the reduction tracks claim locality; smaller claims shrink further. The dominant remaining recursive cost is hashing the canonical 9.4MB vk (~84% blake3), untouched by activation by design. All suites green: multi-stark reference vectors + differential hash tests (12), e2e accept/tamper/codegen-parity (6), default suite, ixvm (596, FFT pins hold — activation does not change execution). Kernel codegen byte-identical.

gl_zero/gl_one/gl_two/gl_seven date from when Goldilocks values were byte arrays and "zero" was a real construction. With the native-field representation each body is just a literal, yet every call site still paid call plumbing columns in its caller circuit — gl_zero alone had ~56 call sites through the verifier (OOD loop, FRI fold, bucket construction). gl_is_zero was a passthrough to the eq_zero builtin. Replace every call site with the literal (or the builtin) and let toplevel pruning drop the five helper circuits. prep_count is deliberately kept: it isolates a match in a tiny circuit, and inlining it would fork verify_one_query's downstream columns across both arms — costing far more than its single call site. Verifier width 11567 -> 11395 (-172 columns, 5 fewer circuits). FFT cost and execute time are unchanged within noise (RAYON_NUM_THREADS=1 toy canary: 3.981B -> 3.980B) — the removed columns live in circuits whose heights contribute negligibly — so this lands as cleanup, not a measured speedup.

The verifying-key wire format was 8-byte scaffolding around tiny values: u32 enum tags (22% of the bytes), u64 rotation offsets that are only ever 0/1 (22%), u64 column indices (22%), and a u64 degree_multiple per compound node (19%) — actual field constants were 3%. The recursive verifier hashes every vk byte for the digest binding, making that padding the dominant blake3 cost at kernel scale. Replace it with a split-streams format: each field class lives in its own per-circuit byte segment with a single fixed width, so every in-circuit read stays a static-size io_read — no varints, no length branching. - Per-circuit records (contiguous, Merkle-leaf-ready): 5 x u32 segment lengths, then TAGS (1 byte per node: kind nibble + aux nibble packing entry kind, rotation, or constant size class), IDX (u16 column indices), C2/C8 (u16 small / u64 large constants), META (u32 counts and metadata). - degree_multiple is no longer serialized: it is fully derivable (variables by entry kind, add/sub = max, mul = sum, neg = child). The Rust decoder recomputes it via the library's degree_multiple(); the in-circuit verifier never used it, so SymExpr drops the field. - The Lean reader threads one cursor per segment and asserts each segment's exact consumption per record, binding the header lengths to the parsed structure. Fiat-Shamir is unchanged: the observed parameter/shape words are value-based, and the narrow reads pad to the same 8-byte limbs as before. - New codec tests: round-trip fixpoint, node-by-node degree recomputation equality, trailing-byte and tampered-segment-length rejection. verifier_io_buffer gains an IX_DUMP_RECURSION_IO env hook that dumps the proof/vk/claims blobs for offline measurement. Kernel-scale Nat.add_comm (q=100): vk 8,383,020 -> 1,075,477 bytes, recursive execute 25.9 -> 18.9 s, FFT 147.0B -> 99.8B (-32%). The outer prove — which OOM'd a 495 GiB host under the old format — now completes: full sound recursive verification runs end-to-end in 4:00 wall (inner prove 2.0 s, recursive execute 19.8 s, outer prove 216.9 s) at 315.9 GiB peak RSS, producing a 12.3 MB outer proof that natively verifies in 94 ms. Toy canary (RAYON_NUM_THREADS=1): FFT 3.980B -> 3.964B, width 11395 -> 11290. All suites green: vk codec round-trip (3), multi-stark reference vectors + differential hashes, recursive-verifier e2e accept/tamper/ codegen-parity, default suite, ixvm (FFT pins hold). Kernel codegen byte-identical; verifier codegen regenerated.

Infallible u16::try_from guard replaces the manual `< 2^16` check in `constant`, the rotation offset cast goes through u8::try_from, and the u16 constant decode widens with u64::from instead of `as`.

@fn

Rebase followup: the branch's unconstrained_g_to_bytes / unconstrained_g_inverse Term constructors postdate the @fn inlining machinery merged upstream, whose matches (freshen, inlineCallSites, expandOnce, hoistLets) must now cover them as plain unary wrappers. Codegen regenerated against the merged sources.

Rebase of the sb/kernel-perf kernel stack onto main (the early workspace/backend/sharding commits of this branch were superseded by their evolved forms merged in #411/#503; this carries only the novel kernel work, reconciled with main's #473 declared-flag removal and is_rec_cache): - intern-assigned uids replace per-node blake3 content hashing: KExpr/ KUniv identity is a never-reused process-global u64; InternTable keys on shallow structural keys (variant tag + child uids + payload); cache keys cannot alias across intern-table clears (a stale key can only miss). ~20% of guest cycles on reduction-heavy constants came from content hashing (app_hash 22-33% cumulative). Design + collision analysis in docs/kernel_identity.md. - adversarial hardening of the uid design: fresh_uid aborts on counter exhaustion; literal structural-equality arms compare values as well as blob addresses; uid-accepting constructors privatized so a caller-supplied uid can never enter a node. - environment-machine WHNF (design in docs/env_machine_whnf.md): Phase A — whnf_core's App arm enters a Krivine-style machine when a beta fires; beta/zeta are O(1) environment pushes and substitution materializes only at machine exits (clo_subst readback), so a beta chain ending in another beta never materializes intermediate bodies. Phase B — closure-iota at the machine's recursor exit: only the major premise materializes on the main ctor-rule path; the rule RHS re-enters the machine with original closures, so unselected minors (dropped match/Decidable branches, the UTF-8 codec class) are never substituted and never read back. - memoized prim-family dispatch in the WHNF/def-eq reduction loops: classify each head once per iteration via an allocation-free app-chain walk + per-address memo (KEnv::prim_family_cache) instead of probing all five primitive recognizers per iteration. - compact symbolic Nat offsets: Nat.add base (Lit n) / Nat.div/mod base (Lit k) stay stuck in compact form (each keeps its own head, so offset def-eq cannot equate /- and +-derived forms); linear-rec collapse; offset-aware def-eq. - H-15 whnf probe pre-filter (allocation-free spine_head_and_len before the transient-nat probes) and H-12 output-size caps on native Nat arithmetic. - suffix-aware CtxAddr keys for the is_prop / nat_succ_stuck caches; NatSuccMode::Stuck whnf cache (proves ByteArray.utf8DecodeChar?_utf8EncodeChar_append). - ixon: per-constant address verification deferred to first materialization (LazyConstant::get checks pending_addr): constants shipped in a closure but never forced by the typechecker are never hashed; everything the kernel certifies is still verified when it is forced. Guest cycles: rbmap -9.5%, natgcdcomm -6.4%, stringappend -4.2%.

arthurpaulino force-pushed the ap/recursive-verifier-codegen branch 2 times, most recently from 9589cca to d5aa3d5 Compare July 20, 2026 17:38

arthurpaulino marked this pull request as ready for review July 20, 2026 17:38

arthurpaulino force-pushed the ap/recursive-verifier-codegen branch 3 times, most recently from 670147b to ccaaa05 Compare July 20, 2026 20:09

arthurpaulino added 16 commits July 20, 2026 20:29

chore: rustfmt + clippy fixes in vk_codec

f63844b

Infallible u16::try_from guard replaces the manual `< 2^16` check in `constant`, the rotation offset cast goes through u8::try_from, and the u16 constant decode widens with u64::from instead of `as`.

arthurpaulino force-pushed the ap/recursive-verifier-codegen branch from f24240c to 186654a Compare July 20, 2026 20:45

johnchandlerburnham approved these changes Jul 20, 2026

View reviewed changes

arthurpaulino enabled auto-merge (squash) July 20, 2026 20:52

arthurpaulino merged commit 052427b into main Jul 20, 2026
10 checks passed

arthurpaulino deleted the ap/recursive-verifier-codegen branch July 20, 2026 20:55

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Recursive verification of Ix proofs at kernel scale - #503

Recursive verification of Ix proofs at kernel scale#503
arthurpaulino merged 16 commits into
mainfrom
ap/recursive-verifier-codegen

arthurpaulino commented Jul 20, 2026 •

edited

Loading

Uh oh!

arthurpaulino commented Jul 20, 2026

Uh oh!

argument-ci-bot Bot commented Jul 20, 2026 •

edited

Loading

Uh oh!

arthurpaulino commented Jul 20, 2026

Uh oh!

argument-ci-bot Bot commented Jul 20, 2026 •

edited

Loading

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

arthurpaulino commented Jul 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What's here

Measurements (kernel-scale Nat.add_comm, q=100, logBlowup=2)

Testing

Uh oh!

arthurpaulino commented Jul 20, 2026

Uh oh!

argument-ci-bot Bot commented Jul 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

!benchmark — main vs 5eb7078

aiur-recursive · InitStd — main from: base run @ a75cb04 (not on bencher)

Uh oh!

arthurpaulino commented Jul 20, 2026

Uh oh!

argument-ci-bot Bot commented Jul 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

!benchmark — main vs f24240c

aiur-recursive · InitStd — main from: base run @ 77cdce3 (not on bencher)

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

arthurpaulino commented Jul 20, 2026 •

edited

Loading

Measurements (kernel-scale `Nat.add_comm`, q=100, logBlowup=2)

argument-ci-bot Bot commented Jul 20, 2026 •

edited

Loading

`!benchmark` — main vs `5eb7078`

`aiur-recursive` · `InitStd` — main from: base run @ `a75cb04` (not on bencher)

argument-ci-bot Bot commented Jul 20, 2026 •

edited

Loading

`!benchmark` — main vs `f24240c`

`aiur-recursive` · `InitStd` — main from: base run @ `77cdce3` (not on bencher)