Blake3 circuit optimizations + Aiur inlined function calls#497
Closed
arthurpaulino wants to merge 4 commits into
Closed
Blake3 circuit optimizations + Aiur inlined function calls#497arthurpaulino wants to merge 4 commits into
arthurpaulino wants to merge 4 commits into
Conversation
Replace `Source.Term.app`'s `unconstrained : Bool` with a `CallMode` (normal | unconstrained | inlined). `@fn(args)` marks an inlined call: `Toplevel.inlineCalls`, run first in `compile`, splices the callee's body into the caller — each input Local bound to its argument via a let, the (recursively inline-expanded) body as the value. Inlining is forbidden for callees that are transitively inline-recursive. An inlined call compiles to no separate circuit and no call interface (no lookup, no output columns): the callee's work joins the caller's straight-line circuit. This lets a hot inner routine be written once and expanded into a single wide circuit, instead of paying the per-call state-rematerialization and the taller callee-circuit height. The mode only exists in the Source stage — `inlineCalls` eliminates `.inlined` before typechecking, and Check maps normal->false / unconstrained->true into the existing downstream bool. Interpreters match the mode as `_` (an inlined call executes identically to a normal one), so evaluation is unchanged. The pass expands bottom-up over the inline-call DAG (Kahn topo order), so it is fuel-free and total. At each inline site the callee's inputs and body are alpha-renamed to fresh `inl#N` locals before argument binding, so nested `@`-calls cannot capture caller bindings; spliced let-chains are hoisted out of strict argument positions (array elements, operator operands, app arguments), which lowering would otherwise reject. Also drops a `simp` arg in `compile_stages_of_ok` that the final pipeline shape no longer needs.
blake3_g_function was ~100 lines of inlined byte arithmetic: six little-endian carry chains, the add/xor/rotate quarter-round steps spelled out per byte. Rewrite it as its eight-step dataflow over `@`-inlined word ops: ByteStream's existing u32_add / u32_xor, plus the four right-rotations u32_rotr16/u32_rotr8 (byte moves) and u32_rotr12/u32_rotr7 (byte move + chained gadget), added to ByteStream next to the other unsigned-int ops. Still one circuit, byte-identical work. Probe (1 hash, 2048 bytes, non-periodic LCG): 6,575,392 FFT, unchanged. `aiur-hashes` blake3 cases green (execute/claim/prove-verify).
Each `blake3_g_function` does two 3-word additions (a + b + x and a + b + y) as chained `u32_add`s. `u32_add3` accumulates each byte column with chained `u8_add` and folds the 0/1 carry bits with a free field add: 11 u8_adds vs 14 for two chained adds. Column carry is floor(sum/256) <= 2. blake3_g_function lookups 63 -> 57, width 224 -> 206; blake3_bench total FFT 6,575,392 -> 6,214,420 (-5.5%). Digests verified against the Rust reference across chunk/block-boundary sizes.
blake3_compress_inner_j recurses on the round index, permuting the message half between rounds and returning after round 6, so blake3_compress pays one 128-output call site instead of seven (1118 -> 338 columns). Regenerate the Aiur kernel (`lake exe ix codegen`) and re-pin all 56 kernel-check FFT costs from a full `lake test -- --ignored ixvm` run (all green). Nat.add_comm: 53,748,034 -> 52,451,949 total FFT vs main.
arthurpaulino
force-pushed
the
ap/blake3-distill
branch
from
July 17, 2026 20:02
b3ade3c to
6c04bae
Compare
Member
Author
|
!benchmark aiur-recursive |
|
| 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 |
30.975 s | 31.242 s | +0.9% | 74.67 GiB | 74.35 GiB | -0.4% | 15.84 MiB | 15.31 MiB | -3.3% 🟢 | 112.0 ms | 105.9 ms | -5.5% (1.06× faster) 🟢 | 8.987 s | 8.967 s | -0.2% | 17.86B | 17.97B | +0.6% | 197.9 ms | 240.2 ms | +21.4% (1.21× slower) |
848.61 KiB | 848.61 KiB | +0.0% | 6.4 ms | 6.4 ms | +0.3% | 413.64 MiB | 416.13 MiB | +0.6% |
square-q100-b1 |
22.404 s | 23.096 s | +3.1% |
43.55 GiB | 43.16 GiB | -0.9% | 15.76 MiB | 15.23 MiB | -3.3% 🟢 | 95.6 ms | 104.1 ms | +9.0% (1.09× slower) |
7.605 s | 8.125 s | +6.8% (1.07× slower) |
15.36B | 15.43B | +0.4% | 170.0 ms | 198.1 ms | +16.5% (1.17× slower) |
782.05 KiB | 782.05 KiB | +0.0% | 5.5 ms | 5.6 ms | +2.2% | 309.19 MiB | 326.14 MiB | +5.5% (1.05× larger) |
2 proofs · 2 with regressions · 2 with improvements (|Δ| > 3.0% on any metric).
Member
|
!benchmark |
|
| constant | prove-time (main) | prove-time (PR) | Δ% | throughput (const/s) (main) | throughput (const/s) (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | execute-time (main) | execute-time (PR) | Δ% | verify-time (main) | verify-time (PR) | Δ% | proof-size (main) | proof-size (PR) | Δ% | fft-cost (main) | fft-cost (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Array.extract_append |
55.513 s | 58.356 s | +5.1% (1.05× slower) |
30.730 | 29.230 | -4.9% (1.05× slower) |
92.52 GiB | 91.62 GiB | -1.0% | 12.978 s | 13.023 s | +0.3% | 227.5 ms | 247.0 ms | +8.6% (1.09× slower) |
34.43 MiB | 33.90 MiB | -1.5% | 39.96B | 39.62B | -0.8% |
ByteArray.utf8DecodeChar?_utf8EncodeChar_append |
57.297 s | 58.354 s | +1.8% | 50.440 | 49.530 | -1.8% | 100.44 GiB | 98.60 GiB | -1.8% | 11.966 s | 12.300 s | +2.8% | 238.4 ms | 223.0 ms | -6.4% (1.07× faster) 🟢 | 34.43 MiB | 33.90 MiB | -1.5% | 42.29B | 41.52B | -1.8% |
Char.ofOrdinal_le_of_le |
45.008 s | 46.057 s | +2.3% | 63.590 | 62.140 | -2.3% | 75.26 GiB | 73.92 GiB | -1.8% | 9.153 s | 9.108 s | -0.5% | 226.7 ms | 239.9 ms | +5.8% (1.06× slower) |
34.43 MiB | 33.90 MiB | -1.5% | 32.54B | 31.97B | -1.8% |
Vector.extract_append._proof_2 |
32.424 s | 33.817 s | +4.3% |
44.440 | 42.610 | -4.1% |
53.19 GiB | 52.67 GiB | -1.0% | 6.991 s | 7.149 s | +2.3% | 215.7 ms | 232.2 ms | +7.6% (1.08× slower) |
34.35 MiB | 33.82 MiB | -1.5% | 23.29B | 23.05B | -1.0% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
27.034 s | 27.426 s | +1.4% | 72.980 | 71.940 | -1.4% | 48.20 GiB | 47.26 GiB | -1.9% | 4.431 s | 4.559 s | +2.9% | 213.8 ms | 241.2 ms | +12.8% (1.13× slower) |
34.35 MiB | 33.82 MiB | -1.5% | 17.35B | 17.01B | -2.0% |
String.split |
25.902 s | 26.440 s | +2.1% | 75.240 | 73.710 | -2.0% | 46.56 GiB | 45.67 GiB | -1.9% | 4.150 s | 4.193 s | +1.0% | 214.8 ms | 230.9 ms | +7.5% (1.07× slower) |
34.35 MiB | 33.82 MiB | -1.5% | 15.89B | 15.59B | -1.9% |
List.mergeSort |
17.432 s | 18.209 s | +4.5% |
91.670 | 87.760 | -4.3% |
29.50 GiB | 29.16 GiB | -1.1% | 2.804 s | 2.882 s | +2.8% | 211.4 ms | 243.6 ms | +15.2% (1.15× slower) |
34.35 MiB | 33.82 MiB | -1.5% | 11.58B | 11.34B | -2.0% |
Vector.append |
5.316 s | 5.740 s | +8.0% (1.08× slower) |
106.470 | 98.600 | -7.4% (1.08× slower) |
8.77 GiB | 8.67 GiB | -1.2% | 535.8 ms | 537.7 ms | +0.4% | 221.5 ms | 213.5 ms | -3.6% 🟢 | 34.12 MiB | 33.59 MiB | -1.5% | 2.58B | 2.54B | -1.9% |
Nat.gcd_comm |
4.355 s | 4.542 s | +4.3% |
95.290 | 91.360 | -4.1% |
6.89 GiB | 6.94 GiB | +0.7% | 354.3 ms | 369.1 ms | +4.2% |
215.0 ms | 223.3 ms | +3.9% |
34.12 MiB | 33.59 MiB | -1.5% | 1.75B | 1.71B | -2.4% |
String.append |
2.949 s | 3.265 s | +10.7% (1.11× slower) |
119.700 | 108.130 | -9.7% (1.11× slower) |
4.38 GiB | 4.19 GiB | -4.2% 🟢 | 188.7 ms | 198.9 ms | +5.4% (1.05× slower) |
210.8 ms | 214.4 ms | +1.7% | 34.05 MiB | 33.52 MiB | -1.5% | 963.43M | 941.35M | -2.3% |
Int.gcd |
2.424 s | 2.487 s | +2.6% | 94.490 | 92.060 | -2.6% | 3.10 GiB | 3.01 GiB | -3.1% 🟢 | 130.0 ms | 128.5 ms | -1.1% | 207.8 ms | 220.8 ms | +6.3% (1.06× slower) |
34.05 MiB | 33.52 MiB | -1.5% | 604.12M | 590.24M | -2.3% |
Nat.sub_le_of_le_add |
2.251 s | 2.380 s | +5.8% (1.06× slower) |
84.410 | 79.820 | -5.4% (1.06× slower) |
2.85 GiB | 2.80 GiB | -1.6% | 98.4 ms | 98.4 ms | -0.0% | 208.1 ms | 217.7 ms | +4.6% |
34.05 MiB | 33.52 MiB | -1.5% | 509.28M | 497.81M | -2.3% |
Nat.add_comm |
1.098 s | 1.236 s | +12.5% (1.12× slower) |
46.430 | 41.280 | -11.1% (1.12× slower) |
1.27 GiB | 1.27 GiB | +0.1% | 13.2 ms | 13.7 ms | +4.4% |
204.1 ms | 224.7 ms | +10.1% (1.10× slower) |
33.91 MiB | 33.39 MiB | -1.6% | 53.75M | 52.45M | -2.4% |
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual |
OOM | OOM | n/a | OOM | OOM | n/a | OOM | OOM | n/a | 1m 21.1s | 1m 22.2s | +1.3% | OOM | OOM | n/a | OOM | OOM | n/a | 260.46B | 257.02B | -1.3% |
14 constants · 12 with regressions · 4 with improvements (|Δ| > 3.0% on any metric).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Distills the blake3 work from
ap/aiur-hash-widthontomain: the@-inliningcompiler feature plus three blake3 circuit optimizations. Excludes the
chain-rotr gadget generalization (blake3 only needs the existing fixed
u8_chain_rotr4/u8_chain_rotr7ops), the keccak/sha256 work, and the benchharness changes.
Commits
Aiur: inlined function calls (
@fn(args))Replaces
Source.Term.app'sunconstrained : Boolwith aCallMode(normal | unconstrained | inlined).
@fn(args)marks an inlined call:Toplevel.inlineCalls, run first incompile, splices the callee's bodyinto the caller. An inlined call compiles to no separate circuit and no
call interface — the callee's work joins the caller's straight-line
circuit. The mode only exists in the Source stage; evaluation is unchanged.
Aiur blake3: extract G-function word-ops into @-inlined helpers
blake3_g_functionwas ~100 lines of inlined byte arithmetic. Rewrittenas its eight-step dataflow over
@-inlined word ops: ByteStream'sexisting
u32_add/u32_xor, plus four right-rotationsu32_rotr16/u32_rotr8(byte moves) andu32_rotr12/u32_rotr7(byte move + chained gadget), added to ByteStream next to the other
unsigned-int ops. Still one circuit, byte-identical work; FFT unchanged.
blake3: fuse the G-function's 3-word adds into one carry pass
u32_add3(ByteStream) accumulates each byte column with chainedu8_addand folds the 0/1 carry bits with a free field add: 11 u8_adds vs 14 for
two chained adds. G-function lookups 63 → 57, width 224 → 206.
blake3: self-recursive compress rounds
blake3_compress_inner_jrecurses on the round index, permuting themessage half between rounds and returning after round 6, so
blake3_compresspays one 128-output call site instead of seven(1118 → 338 columns). Includes the regenerated Aiur kernel
(
lake exe ix codegen) and the 56 re-pinned kernel-check FFT costs.Results
lake exe ix check Nat.add_comm(blake3 drives every kernel-check's hashing):All 56 pinned kernel-check FFT costs re-measured from a full
lake test -- --ignored ixvmrun (suite green, codegen/bytecode parityincluded).