Aiur hash circuits: value-based keccak-256, inlined calls, self-recursive rounds, and a generalized chain-rotate gadget by arthurpaulino · Pull Request #488 · argumentcomputer/ix

arthurpaulino · 2026-07-13T15:07:42Z

Summary

This branch is an optimization arc over the three hash functions proven by
IxVM's Aiur circuits — blake3, sha256 and keccak-256 — targeting the two
costs that matter: total circuit width (columns committed per proof)
and proving throughput (bytes/s). It also lands the compiler and
benchmarking infrastructure the optimizations needed.

Final state on a 64-core Xeon 6975P-C (512 KiB proven per largest case):

hash	total width	throughput	dominant circuit
blake3	2,510	~68 KiB/s	`blake3_g_function` (206 wide)
sha256	4,043	~30 KiB/s	`sha256_round` (342 wide, 64 rows/block)
keccak-256	5,018	~28 KiB/s	`keccak_round` (3,414 wide, 24 rows/perm)

Highlights along the way: keccak-256 replaced a pointer-heavy
implementation with a value-based one that is 78x cheaper, and the
closing optimization trio (chain-rotate gadget generalization + the two
self-recursive round restructures) cuts keccak's width by a further
53% while raising its throughput 19%, and cuts blake3's width by
21% at unchanged throughput.

What's in here

1. Compiler groundwork.
@fn(args) inlined calls: the callee's body is spliced into the caller at
compile time — no separate circuit, no call interface, no output-column
materialization. Hot inner routines (rotations, carry chains, chi/sigma
combinators) are written once and expanded into the circuits that use
them. The pass is total (bottom-up over the inline-call DAG), alpha-renames
callee locals so nested @-calls can't capture bindings, and hoists
spliced let-chains out of strict argument positions.

2. sha256.
Round-body word ops become byte ops, the message schedule moves into the
block circuit as a memoized shared circuit, ch/maj and the multi-word
additions fuse their carries into single passes with free field adds, and
the 64 rounds run as one narrow called circuit (64 rows/block) instead of
inlining 64x into the block circuit.

3. keccak-256.
Rewritten value-based: lanes and the 25-lane state are plain values — no
pointers, no memory traffic; the rate block is absorbed directly from the
byte stream. All 24 rounds share one keccak_round circuit.

4. blake3.
G-function word ops extracted into @-inlined helpers; its three-word
adds fuse into one carry pass.

5. Measurement + this round of optimizations.

A shared bench harness (lake exe bench-{blake3,sha256,keccak}) prints
per-circuit width/height/FFT-cost statistics and the total circuit width
before the timed runs, over LCG-seeded non-periodic inputs on a
4K/32K/128K x 1/4-hash grid (512 KiB max per proof — on the throughput
plateau, fast to iterate).
The chain-rotate byte-pair gadget generalizes from fixed rotr7/rotr4 to
any k in 1..=7 (u8_chain_rotr(k, hi, lo)), making a 64-bit lane
rotation cost 4 lookups for any bit offset.
keccak_round tail-recurses on a round index (iota constants selected
by a shared-column match), deleting the keccak_f driver and its
24 x 202 call-site columns; rho runs on the chain gadget:
width 10,604 -> 5,018 (-53%), throughput 23.4 -> 27.9 KiB/s (+19%).
blake3_compress_inner_j likewise self-recurses over its 7 rounds:
width 3,173 -> 2,510 (-21%), throughput unchanged.
The statistics cost model's memory-circuit width is corrected to match
the Rust prover (size + 7, not size + 11), and kernel-check FFT
pins are refreshed accordingly.

Notes for reviewers

The Bytecode.Op change (u8ChainRotr k replacing the two fixed ops)
shifts the FFI constructor tags of debug/u8RangeCheck/
unconstrainedBigUintDivMod down by one; the Rust decoder is updated in
the same commit.
The Bytes2 gadget table grows from 10+16 to 15+31 columns (fixed 65,536
rows) to serve all seven rotation amounts on channels 13..19.
The codegen'd IxVM kernel is regenerated in the final commit; until
then it compiles through legacy fixed-amount aliases.
A rejected experiment worth knowing about: making sha256's 64 rounds
self-recursive (rolling 16-word schedule window) halves sha256's width
to ~1,850 but costs 26% throughput — measured, not modeled — so it was
dropped under the "never regress throughput" rule. The write-up lives in
the branch discussion.

Testing

lake test -- --ignored aiur-hashes — 195 checks: execute, interpret,
prove and verify for all blake3/sha256/keccak vectors (including rate-
and block-boundary sizes).
lake test -- --ignored aiur (483 checks) and lake test -- aiur-cross
(340 checks) — op-level vectors incl. the chain-rotate ops, and
interpreter/bytecode agreement.
lake test -- --ignored ixvm — 599 checks: kernel-check FFT pins and
codegen/bytecode parity over the regenerated kernel.
Every commit builds; the two synthetic split points were build-checked
explicitly for bisectability.

Follow-up (not in this PR)

LogUp batching in multi-stark: each lookup currently costs a dedicated
stage-2 extension column (2 base columns) — ~58% of keccak_round's
width. Folding fraction pairs into one column would cut every circuit's
width by up to ~30% and halve stage-2 commitment work.
Chunked byte streams: the per-byte take_byte/memory[3] walk is ~5%
of keccak's cost and ~15% of blake3's.

arthurpaulino · 2026-07-13T15:58:12Z

!benchmark

argument-ci-bot · 2026-07-13T16:15:22Z

`!benchmark` — main vs `3a5e363`

backends: aiur=prove · envs: InitStd · set: primary · shard: 0

`aiur` · `InitStd` · `prove` — main from: bencher @ `16455ba` + base run (1 new)

constant	prove-time (main)	prove-time (PR)	Δ%	throughput (main)	throughput (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)	Δ%
`ByteArray.utf8DecodeChar?_utf8EncodeChar_append`	54.933 s	52.614 s	-4.2% 🟢	52.610	54.930	+4.4% 🟢	100.89 GiB	99.11 GiB	-1.8%	11.817 s	11.880 s	+0.5%	208.4 ms	241.0 ms	+15.7% (1.16× slower) ⚠️	33.27 MiB	32.77 MiB	-1.5%	42.43B	40.84B	-3.7% 🟢
`Array.extract_append`	53.157 s	51.143 s	-3.8% 🟢	32.090	33.360	+4.0% 🟢	92.86 GiB	92.00 GiB	-0.9%	12.727 s	12.504 s	-1.8%	210.3 ms	233.7 ms	+11.1% (1.11× slower) ⚠️	33.27 MiB	32.77 MiB	-1.5%	40.03B	38.96B	-2.7%
`Char.ofOrdinal_le_of_le`	43.097 s	40.682 s	-5.6% (1.06× faster) 🟢	66.410	70.350	+5.9% (1.06× faster) 🟢	76.04 GiB	74.64 GiB	-1.8%	8.947 s	8.986 s	+0.4%	209.1 ms	212.6 ms	+1.7%	33.27 MiB	32.77 MiB	-1.5%	32.73B	31.52B	-3.7% 🟢
`Vector.extract_append._proof_2`	31.148 s	30.005 s	-3.7% 🟢	46.260	48.030	+3.8% 🟢	53.50 GiB	52.99 GiB	-0.9%	6.820 s	6.796 s	-0.4%	215.8 ms	278.1 ms	+28.9% (1.29× slower) ⚠️	33.19 MiB	32.68 MiB	-1.5%	23.34B	22.65B	-2.9%
`_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq`	26.216 s	24.503 s	-6.5% (1.07× faster) 🟢	75.260	80.520	+7.0% (1.07× faster) 🟢	48.88 GiB	47.79 GiB	-2.2%	4.401 s	4.419 s	+0.4%	205.7 ms	214.2 ms	+4.2% ⚠️	33.19 MiB	32.68 MiB	-1.5%	17.43B	16.75B	-3.9% 🟢
`String.split`	24.576 s	23.680 s	-3.6% 🟢	79.300	82.300	+3.8% 🟢	47.09 GiB	46.22 GiB	-1.9%	4.030 s	4.089 s	+1.5%	205.0 ms	202.8 ms	-1.1%	33.19 MiB	32.68 MiB	-1.5%	15.99B	15.38B	-3.8% 🟢
`List.mergeSort`	16.628 s	16.048 s	-3.5% 🟢	96.100	99.580	+3.6% 🟢	29.84 GiB	29.53 GiB	-1.0%	2.782 s	2.782 s	-0.0%	205.2 ms	204.6 ms	-0.3%	33.19 MiB	32.68 MiB	-1.5%	11.63B	11.16B	-4.0% 🟢
`Vector.append`	5.218 s	5.235 s	+0.3%	108.480	108.130	-0.3%	8.72 GiB	8.94 GiB	+2.4%	529.2 ms	534.5 ms	+1.0%	203.3 ms	216.0 ms	+6.3% (1.06× slower) ⚠️	32.96 MiB	32.45 MiB	-1.5%	2.60B	2.50B	-3.7% 🟢
`Nat.gcd_comm`	4.158 s	4.109 s	-1.2%	99.800	101	+1.2%	7.09 GiB	7.12 GiB	+0.5%	349.0 ms	356.7 ms	+2.2%	218.0 ms	208.4 ms	-4.4% 🟢	32.96 MiB	32.45 MiB	-1.5%	1.75B	1.68B	-4.4% 🟢
`String.append`	2.973 s	2.974 s	+0.0%	118.750	118.700	-0.0%	4.42 GiB	4.50 GiB	+1.8%	186.0 ms	191.9 ms	+3.2% ⚠️	201.0 ms	200.4 ms	-0.3%	32.89 MiB	32.38 MiB	-1.5%	967.65M	925.97M	-4.3% 🟢
`Int.gcd`	2.350 s	2.371 s	+0.9%	97.430	96.580	-0.9%	3.25 GiB	3.25 GiB	-0.1%	121.2 ms	121.4 ms	+0.2%	203.0 ms	195.7 ms	-3.6% 🟢	32.89 MiB	32.38 MiB	-1.5%	605.84M	579.56M	-4.3% 🟢
`Nat.sub_le_of_le_add`	2.347 s	2.231 s	-5.0% (1.05× faster) 🟢	80.940	85.170	+5.2% (1.05× faster) 🟢	3.06 GiB	3.04 GiB	-0.6%	95.2 ms	100.7 ms	+5.8% (1.06× slower) ⚠️	204.7 ms	191.9 ms	-6.2% (1.07× faster) 🟢	32.89 MiB	32.38 MiB	-1.5%	510.60M	488.67M	-4.3% 🟢
`Nat.add_comm`	1.156 s	1.161 s	+0.4%	44.100	43.910	-0.4%	1.43 GiB	1.50 GiB	+5.1% (1.05× larger) ⚠️	15.5 ms	14.1 ms	-8.9% (1.10× faster) 🟢	194.5 ms	206.8 ms	+6.3% (1.06× slower) ⚠️	32.76 MiB	32.25 MiB	-1.5%	53.90M	51.29M	-4.8% (1.05× fewer) 🟢
`Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual`	OOM	OOM	n/a	OOM	OOM	n/a	OOM	OOM	n/a	1m 18.4s	1m 18.0s	-0.4%	OOM	OOM	n/a	OOM	OOM	n/a	261.03B	253.93B	-2.7%

14 constants · 8 regressed · 5 improved (|Δ| > 3.0% on any metric).

Workflow logs

Byte 6 of the result returned the pre-carry `sum1` (u64[6] + bs[0]) instead of `sum1_with_carry`, silently dropping a carry propagating from byte 7 into byte 6. The carry was still folded into the higher bytes via carry2, so only byte 6 itself was wrong, and only when u64[7] + bs[1] overflows. No current caller hits that path (they add pre-chunked amounts whose low byte never carries at that position), so digests are unchanged, but the helper was latently incorrect for a general 2-byte big-endian add.

Each of the 17 u32_* helper calls per round (u32_xor 5, u32_and 5, u32_be_add 7) cost 4 output auxiliaries + 1 lookup at the call site plus a row in the helper's 26-35-wide circuit — 84% of total FFT sat in three helper circuits. Rewrite the 64-round fold body with inline u8_xor / u8_and ops and explicit big-endian u8_add carry chains (carry-out is a free compound expression; mutually-exclusive carries fold with field `+`, mirroring u32_be_add's internals). u32_and is left with zero callers anywhere and is deleted from ByteStream. Probed with a scratch execute-only stats driver (sha256_bench input model with non-periodic LCG bytes so no memoization flatters the numbers; 1 hash over 2048 bytes): total FFT cost 25,573,236 -> 11,046,080 (-56.8%). `lake test -- --ignored aiur-hashes` green (execute, claim, prove/verify, all sizes).

@i

`define_W_i` cost 4 output aux + 1 lookup per call site plus a 210-wide row per (W_i-2, W_i-7, W_i-15, W_i-16) tuple in its own circuit — 48 rows per block at a taller height's log2, re-paying its 16 input columns per row, all through u32_xor/u32_be_add calls. In-block, the schedule rides rows that already exist at log2(blocks), with the word ops inlined as byte ops. The final Davies-Meyer state addition loses its 8 u32_be_add calls the same way. u32_xor and u32_be_add are left with zero callers anywhere and are deleted from ByteStream. shr10's top byte is the constant 0, so s1's byte 0 xors two operands instead of three. The schedule fold indexes W[i-2]/W[i-7]/W[i-15]/W[i-16], which the fold macro could not express: add an `arr[@i - k]` form (literal offset, resolved to a static index during unrolling). The unrolled body needs maxRecDepth 65536 to elaborate. Scratch probe (sha256_bench model, non-periodic LCG bytes, 1 hash over 2048 bytes): total FFT cost 11,046,080 -> 5,906,938 (-46.5%, zero cache hits; -76.9% from the branch baseline's 25,573,236), now 10% below blake3's 6,575,392 on the same input. fill_W_and_run_rounds is 93% of remaining cost (width 33,038 x 33 rows). `lake test -- --ignored aiur-hashes` green (execute, claim, prove/verify, all sizes).

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.

The round and message schedule were walls of inlined byte arithmetic — repeated big-endian carry chains, per-word rotation recompositions, ch/maj blobs. With `@`-inlined calls costing nothing, factor them into named helpers: u32_be_add, u32_xor, u32_and, u32_not, ch, maj, and the four sigmas (big_sigma0/1, small_sigma0/1, each decomposing its word's bytes once and recomposing the rotations). The round and schedule fold bodies become legible dataflow calling them `@`-inlined; the whole compression still compiles to one block circuit. Probe (1 hash, 2048 bytes, non-periodic LCG): 5,906,938 FFT, byte-identical to the hand-inlined version — extraction is free. `aiur-hashes` sha256 cases green (execute/claim/prove-verify).

`ch` and `maj` xor bitwise-disjoint terms, so the xors are free field adds (no u8_xor lookup): ch = (e&f) + (~e&g); maj = (a&b) + (c & (a^b)) with a^b = (a+b) - 2(a&b) recomposed for free. Two u32_ands each instead of ch's 2-and+1-xor and maj's 3-and+2-xor. Sums stay <= 255 (disjointness), so u8_from_field_unsafe is sound. Cuts fill_W_and_run_rounds by 1024 lookups (8889 -> 7865), width 33038 -> 29966 (-9.3%); sha256_bench total FFT 5,906,938 -> 5,395,557 (-8.7%). Digests verified against the Rust reference across padding-boundary sizes.

The round's temp1 = h + Sigma1 + ch + K + W (5 words) and the schedule's W_i = W_16 + sigma0 + W_7 + sigma1 (4 words) were chained `u32_be_add`s, re-propagating carries each step. `u32_be_add4`/`u32_be_add5` accumulate each byte column with chained `u8_add` (partial stays < 256) and fold the 0/1 carry bits into the next column with a free field add: 15 u8_adds vs 21 for a 4-word sum, 19 vs 28 for a 5-word sum. Column carry is floor(sum/256) <= 4, safe to feed back to `u8_add`. fill_W_and_run_rounds lookups 7865 -> 7001, width 29966 -> 27374; sha256_bench total FFT 5,395,557 -> 4,964,080. With the ch/maj change, sha256 FFT is down 16% from 5,906,938. Digests verified across padding-boundary sizes.

fill_W_and_run_rounds inlined the 64-round compression and 48-word message schedule into one 27,374-column circuit -- the same pathological trace width as keccak's inlined permutation. Factor out `sha256_round` and `sha256_schedule` as calls (their sigma/ch/maj/add helpers stay inlined), so the rounds/words share narrow circuits run as rows. fill_W_and_run_rounds 27,374 -> 2,734 wide (sha256_round 342, schedule 192); total committed width 28,153 -> 4,047 (7x smaller). FFT proxy rises 4.96M -> 12.07M (over-weights the taller trace) but real proving is much faster: sha256_bench average throughput 4.59 -> 7.74 KiB/s (+68%). Digests verified against the Rust reference across padding-boundary sizes.

Ix/MultiStark/Keccak.lean optimizes for circuit narrowness, which the FFT cost model (width x height x log2(height)) punishes: lanes live behind pointers (3 memory lookups per xor8 call), every word op is a helper-circuit call, each rotation builds a 64-node linked bit list walked with per-bit list_drops, and keccak_round runs as a separate circuit 24x per permutation. Probed at 1 hash over 2048 bytes of non-periodic LCG data: 1,415,128,681 total FFT — 85% of it list_drop / build_rot / memory[3] rows. Ix/IxVM/Keccak.lean reshapes it for the model: lanes and the 25-lane state are plain values, word ops are inline u8 byte ops, rho+pi rotations are static recompositions (decompose bytes once, recompose at compile-time bit offsets; multiples-of-8 rotations are free byte shuffles), theta's rotl-by-1 needs no decomposition at all (`u8_add(b, b)` = (2b mod 256, msb), the even low byte absorbs the neighbor's carry via free field add), and iota indexes a constant RC table. Each round runs as two circuits (theta | rho+pi+chi+iota) of height 24 x permutations — a single fully-unrolled permutation circuit is cheaper still on paper, but its macro-expanded body overflows the Lean elaborator stack (as do 8-name array-destructure patterns at scale, hence bits are indexed from array-bound decompositions). The rho+pi wiring is generated programmatically and asserted against the MultiStark listing. Same probe: 18,105,233 total FFT (-98.7%, 78x). New `aiur-hashes` cases pin correctness against the Rust FFI oracle (Keccak.hash) at the rate boundaries 0/1/32/135/136/137/271/272/273/1200 — execute, claim, and prove/verify all green.

A lane rotation by 8q+s previously always paid 8 u8_bit_decompositions (64 aux + 8 lookups) regardless of s. Only s=4 genuinely needs the decomposition. For s in {1,2,3}, chain rotl-by-1 via the u8_add doubling trick already used in theta ((b+b) = (2b mod 256, msb); the even low byte absorbs the neighbor's msb through a free field add), 8 aux+lookups per step. For s in {5,6,7}, chain rotr-by-1 via u8_shift_right (the dropped lsb is recovered as b - 2*(b>>1) and recomposed into the neighbor's high bit, also free). 18 of the 24 rotations take a cheaper path; only the six s in {0,4} keep the byte shuffle / decomposition. Probe (1 hash, 2048 bytes, non-periodic LCG): 18,105,233 -> 16,206,377 (-10.5%); keccak_rho_chi_iota width 3198 -> 2622. `aiur-hashes` keccak cases green (rate boundaries 0..273 + 1200, execute/claim/prove-verify) against the Rust FFI oracle.

read_block copied each 136-byte rate block into an intermediate linked list (136 stores/block), which rate_lane then re-walked with list_drop per lane — pure memory traffic (read_block 545k + list_drop 409k + rate_lane 112k + half of memory[3] FFT). Replace with take_byte, which reads the stream directly and injects pad10*1 inline when the message is exhausted (no store on the real-byte path), pulled 8 at a time by take_lane. The pad flag `first_pad` threads through the walk; a block recurses only if 136 real bytes were consumed, so it also decides the extra all-padding block for message lengths that are a multiple of 136. take_lane is a factored circuit rather than 136 inline take_byte lets: the whole toplevel elaborates as one Source.Toplevel AST, and inlining the walk overflows the elaborator. Probe (1 hash, 2048 bytes, non-periodic LCG): 16,206,377 -> 15,292,607 (-5.6%); memory[3] rows 4224 -> 2049. `aiur-hashes` keccak cases green (rate boundaries + prove/verify) against the Rust oracle.

…rals The round ran as two circuits (theta | rho+pi+chi+iota) because one full round overflowed the elaborator when unrolled. The cheap rotations shrank rho enough that a single merged round now fits, so keccak_roundN does the whole permutation round in one circuit: keccak_f calls it 24x (per permutation) instead of calling two half-circuits 48x, halving the state-rematerialization interface (keccak_f width 9902 -> 5054) and giving the merged circuit one shared column layout instead of two. keccak_f now bakes the 24 round constants as literal lane arguments (no RC array + no fold index), which also drops the RC-array column traffic. keccak_roundN is emitted with per-round name suffixes so it can hold N rounds; N=2 already overflows the elaborator, so it stays at one round per circuit (height 384). Inlining all 24 rounds into one height-16 circuit — the remaining ~2x — needs the round AST built programmatically instead of through the quasiquote macro. Probe (1 hash, 2048 bytes, non-periodic LCG): 15,292,607 -> 14,303,230 (-6.5%). `aiur-hashes` keccak cases green (rate boundaries + prove/verify) against the Rust oracle.

keccak_f now applies the round 24 times as `@keccak_round(s, rc)` inlined calls, so all 24 rounds splice into a single straight-line circuit: one row per keccak-f call (height = block count, 16 for a 2048-byte message) instead of the round circuit's height 384 (24 rounds x 16 permutations). The log2(height) factor drops from ~8.6 to 4, and the per-round state-rematerialization interface disappears. The round body is written once (still script-generated for the 24 distinct rho+pi bit wirings); the elaborator only ever sees one round plus 24 call sites, so the earlier stack overflow / >30-min unroll is gone — the 24x expansion happens in the compiler's inline pass at compile time, not in Lean elaboration. Build stays ~4s. Probe (1 hash, 2048 bytes, non-periodic LCG): 14,303,230 -> 6,723,868 (-53%), now within 2% of blake3 (6,575,392) on the same input — 210x below the original MultiStark implementation. keccak_f is one circuit, width 89,678 x height 16. `aiur-hashes` keccak cases green including prove/verify, against the Rust FFI oracle.

The round body was a wall of inlined byte arithmetic (5-deep u8_xor nests, per-lane rotation recompositions, chi's not/and/xor blobs). With `@`-inlined calls costing nothing, factor it into named helpers — xor8, and8, not8, rotl1, chi_lane, and one rotl_N per distinct rho offset — and write keccak_round as legible dataflow calling them `@`-inlined. The whole permutation still compiles to a single circuit. Same probe (1 hash, 2048 bytes, non-periodic LCG): 6,723,868 FFT, byte-identical to the hand-inlined version — extraction is free. `aiur-hashes` keccak cases green (execute/claim/prove-verify) against the Rust FFI oracle.

Inlining the 24 rounds collapsed keccak_f into one 89,678-column circuit (a pathological trace width: heavy to commit and to native-compile). Calling keccak_round shares one ~3942-wide circuit across the rounds (24 rows per permutation), keeping the theta/rho/chi/iota helpers inlined within it -- the same granularity as blake3's g_function. keccak_f 89,678 -> 5,054 wide; total committed width ~90k -> 10,604 (8.5x smaller proof / trace). The FFT-cost proxy rises (6,723,868 -> 14,303,230) because it over-weights the taller trace's log-height factor, but real proving is faster: keccak256_bench average throughput 5.11 -> 5.56 KiB/s (+8.8%). Digests verified against the Rust reference across rate-boundary sizes.

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. Factor into `@`-inlined helpers — u32_le_add, u32_xor, and the four right-rotations rotr16/rotr8 (byte moves) and rotr12/rotr7 (byte move + chained gadget) — leaving the G function as its eight-step dataflow. 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_le_add`s. `u32_le_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.

arthurpaulino · 2026-07-17T18:43:53Z

!benchmark aiur-recursive

All three hash benches (blake3, sha256, and the new bench-keccak) route through Benchmarks/HashCommon.lean, which executes the largest workload once and prints Aiur circuit statistics — per-circuit width, height and FFT cost, plus the total circuit width — before the timed proving runs, so width regressions show up directly in benchmark output. Input data is LCG-seeded and non-periodic: an `(i + idx) % 256` pattern repeats every 256 bytes, so repeated schedule/compression/permutation sub-computations memoize across blocks and understate honest proving cost (sha256's per-word schedule circuit reported 240 unique rows where honest data produces 1584). The grid is 4K/32K/128K bytes x 1/4 hashes: the 512 KiB max case sits on the sustained bytes/s plateau (reached at ~128 KiB per proof) while keeping a full run fast enough to iterate on.

Mirrors crates/aiur/src/memory.rs: multiplicity + selector + pointer + size value columns, plus one lookup -> 2*(1+1) stage-2 columns. The old size + 11 over-counted every memory circuit by 4.

`u8_chain_rotr(k, hi, lo)` replaces the fixed chain_rotr7/chain_rotr4 byte-pair ops end to end: source syntax, the typed/simple/concrete stages, bytecode (`Op.u8ChainRotr k`, FFI tag 24; the debug/range-check /div-mod tags shift down by one), layout, codegen, and the three evaluators. The Bytes2 table gains one preprocessed output triple, multiplicity column and lookup per k (main 10 -> 15, preprocessed 16 -> 31 columns on the fixed 65536-row table); channels 13..19 address the seven rotation amounts. The codegen'd IxVM kernel keeps compiling through legacy fixed-amount aliases until regenerated. A chained pair costs 3 aux + 1 lookup regardless of k, so a 64-bit lane rotation is 4 chain lookups plus free field adds for ANY bit offset — the enabler for keccak's rho step, whose offsets hit every k.

keccak_round tail-recurses on a round index: a shared-column match yields the iota constant (only RC bytes 0, 1, 3 and 7 are ever non-zero, so iota xors just four state bytes), round 23 returns, and absorb_blocks calls keccak_round(s, 0) directly — deleting keccak_f, whose 24 call sites materialized 24 x (200 aux + 1 lookup) columns. rho (and theta's rotl-by-1) move from 1-4 chained u8_add/u8_shift passes per lane (24-96 columns) to 4 chain-rotr lookups per lane (20 columns); the wiring is script-generated and asserted against a reference 64-bit rotation. 512 KiB grid: total width 10604 -> 5018 (-53%), throughput 23.4 -> 27.9 KiB/s (+19%); keccak_round lands at 3414 columns.

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). 512 KiB grid: total width 3173 -> 2510 (-21%), throughput unchanged.

argument-ci-bot · 2026-07-17T18:50:59Z

`!benchmark` — main vs `ff8d1d5`

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

`aiur-recursive` · `InitStd` — main from: bencher @ `4e554d2`

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.759 s	33.006 s	+7.3% (1.07× slower) ⚠️	74.78 GiB	77.13 GiB	+3.1% ⚠️	15.84 MiB	15.33 MiB	-3.2% 🟢	95.0 ms	98.3 ms	+3.5% ⚠️	9.180 s	10.201 s	+11.1% (1.11× slower) ⚠️	17.96B	20.17B	+12.3% (1.12× more) ⚠️	247.7 ms	240.8 ms	-2.8%	848.61 KiB	872.99 KiB	+2.9%	6.4 ms	6.5 ms	+1.9%	413.77 MiB	514.83 MiB	+24.4% (1.24× larger) ⚠️
`square-q100-b1`	22.961 s	27.356 s	+19.1% (1.19× slower) ⚠️	43.99 GiB	51.79 GiB	+17.7% (1.18× larger) ⚠️	15.76 MiB	15.25 MiB	-3.2% 🟢	100.5 ms	94.1 ms	-6.4% (1.07× faster) 🟢	8.038 s	9.597 s	+19.4% (1.19× slower) ⚠️	15.68B	17.81B	+13.6% (1.14× more) ⚠️	159.7 ms	250.9 ms	+57.1% (1.57× slower) ⚠️	782.05 KiB	806.43 KiB	+3.1% ⚠️	5.4 ms	6.1 ms	+13.1% (1.13× slower) ⚠️	308.24 MiB	390.55 MiB	+26.7% (1.27× larger) ⚠️

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

Workflow logs

arthurpaulino · 2026-07-17T18:53:48Z

!benchmark

argument-ci-bot · 2026-07-17T19:10:27Z

`!benchmark` — main vs `9704022`

backends: aiur=prove · envs: InitStd · set: primary · shard: 0

`aiur` · `InitStd` · `prove` — main from: bencher @ `4e554d2` + base run (1 new)

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)	Δ%
`ByteArray.utf8DecodeChar?_utf8EncodeChar_append`	54.860 s	53.711 s	-2.1%	52.680	53.810	+2.1%	100.45 GiB	98.63 GiB	-1.8%	11.678 s	11.759 s	+0.7%	229.4 ms	217.8 ms	-5.1% (1.05× faster) 🟢	34.43 MiB	33.92 MiB	-1.5%	42.29B	40.70B	-3.8% 🟢
`Array.extract_append`	53.512 s	52.697 s	-1.5%	31.880	32.370	+1.5%	92.49 GiB	91.67 GiB	-0.9%	12.221 s	12.184 s	-0.3%	234.2 ms	207.7 ms	-11.3% (1.13× faster) 🟢	34.43 MiB	33.92 MiB	-1.5%	39.96B	38.89B	-2.7%
`Char.ofOrdinal_le_of_le`	42.256 s	42.384 s	+0.3%	67.730	67.520	-0.3%	75.32 GiB	73.97 GiB	-1.8%	8.679 s	8.792 s	+1.3%	211.9 ms	239.9 ms	+13.2% (1.13× slower) ⚠️	34.43 MiB	33.92 MiB	-1.5%	32.54B	31.34B	-3.7% 🟢
`Vector.extract_append._proof_2`	31.232 s	31.001 s	-0.7%	46.140	46.480	+0.7%	53.22 GiB	52.75 GiB	-0.9%	6.799 s	6.777 s	-0.3%	213.6 ms	209.1 ms	-2.1%	34.35 MiB	33.84 MiB	-1.5%	23.29B	22.61B	-2.9%
`_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq`	25.669 s	25.171 s	-1.9%	76.860	78.380	+2.0%	48.25 GiB	47.37 GiB	-1.8%	4.261 s	4.309 s	+1.1%	219.7 ms	220.0 ms	+0.1%	34.35 MiB	33.84 MiB	-1.5%	17.35B	16.67B	-4.0% 🟢
`String.split`	24.616 s	24.078 s	-2.2%	79.180	80.950	+2.2%	46.59 GiB	45.73 GiB	-1.8%	3.978 s	4.032 s	+1.3%	210.2 ms	207.7 ms	-1.2%	34.35 MiB	33.84 MiB	-1.5%	15.89B	15.29B	-3.8% 🟢
`List.mergeSort`	16.636 s	16.718 s	+0.5%	96.060	95.580	-0.5%	29.51 GiB	29.21 GiB	-1.0%	2.754 s	2.799 s	+1.6%	214.7 ms	209.5 ms	-2.4%	34.35 MiB	33.84 MiB	-1.5%	11.58B	11.11B	-4.0% 🟢
`Vector.append`	5.183 s	5.205 s	+0.4%	109.210	108.750	-0.4%	8.73 GiB	8.73 GiB	-0.0%	521.1 ms	546.6 ms	+4.9% ⚠️	228.8 ms	202.9 ms	-11.3% (1.13× faster) 🟢	34.12 MiB	33.61 MiB	-1.5%	2.58B	2.49B	-3.7% 🟢
`Nat.gcd_comm`	4.150 s	4.198 s	+1.1%	100	98.860	-1.1%	7.04 GiB	6.94 GiB	-1.4%	358.3 ms	362.2 ms	+1.1%	213.1 ms	203.0 ms	-4.8% 🟢	34.12 MiB	33.61 MiB	-1.5%	1.75B	1.67B	-4.4% 🟢
`String.append`	2.953 s	2.918 s	-1.2%	119.520	120.980	+1.2%	4.25 GiB	4.29 GiB	+1.0%	191.1 ms	196.6 ms	+2.9%	208.5 ms	206.3 ms	-1.1%	34.05 MiB	33.54 MiB	-1.5%	963.43M	921.75M	-4.3% 🟢
`Int.gcd`	2.268 s	2.322 s	+2.4%	100.980	98.620	-2.3%	3.07 GiB	3.07 GiB	-0.0%	126.5 ms	130.0 ms	+2.7%	204.6 ms	199.8 ms	-2.4%	34.05 MiB	33.54 MiB	-1.5%	604.12M	577.83M	-4.4% 🟢
`Nat.sub_le_of_le_add`	2.172 s	2.197 s	+1.2%	87.470	86.460	-1.2%	2.86 GiB	2.85 GiB	-0.4%	94.4 ms	97.9 ms	+3.7% ⚠️	204.8 ms	211.4 ms	+3.2% ⚠️	34.05 MiB	33.54 MiB	-1.5%	509.28M	487.34M	-4.3% 🟢
`Nat.add_comm`	1.084 s	1.192 s	+9.9% (1.10× slower) ⚠️	47.040	42.780	-9.1% (1.10× slower) ⚠️	1.28 GiB	1.35 GiB	+6.0% (1.06× larger) ⚠️	13.2 ms	17.4 ms	+31.9% (1.32× slower) ⚠️	203.1 ms	208.0 ms	+2.4%	33.91 MiB	33.41 MiB	-1.5%	53.75M	51.14M	-4.9% (1.05× fewer) 🟢
`Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual`	OOM	OOM	n/a	OOM	OOM	n/a	OOM	OOM	n/a	1m 19.2s	1m 18.7s	-0.5%	OOM	OOM	n/a	OOM	OOM	n/a	260.46B	253.36B	-2.7%

14 constants · 4 with regressions · 12 with improvements (|Δ| > 3.0% on any metric).

Workflow logs

samuelburnham · 2026-07-17T19:12:05Z

!benchmark aiur-recursive

argument-ci-bot · 2026-07-17T19:16:27Z

`!benchmark` — main vs `9704022`

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

`aiur-recursive` · `InitStd` — main from: bencher @ `4e554d2`

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.759 s	34.922 s	+13.5% (1.14× slower) ⚠️	74.78 GiB	77.37 GiB	+3.5% ⚠️	15.84 MiB	15.33 MiB	-3.2% 🟢	95.0 ms	97.7 ms	+2.9%	9.180 s	10.910 s	+18.8% (1.19× slower) ⚠️	17.96B	20.37B	+13.4% (1.13× more) ⚠️	247.7 ms	180.7 ms	-27.1% (1.37× faster) 🟢	848.61 KiB	872.99 KiB	+2.9%	6.4 ms	6.6 ms	+3.8% ⚠️	413.77 MiB	512.77 MiB	+23.9% (1.24× larger) ⚠️
`square-q100-b1`	22.961 s	28.906 s	+25.9% (1.26× slower) ⚠️	43.99 GiB	51.64 GiB	+17.4% (1.17× larger) ⚠️	15.76 MiB	15.25 MiB	-3.2% 🟢	100.5 ms	100.4 ms	-0.2%	8.038 s	9.870 s	+22.8% (1.23× slower) ⚠️	15.68B	17.88B	+14.1% (1.14× more) ⚠️	159.7 ms	209.4 ms	+31.2% (1.31× slower) ⚠️	782.05 KiB	806.43 KiB	+3.1% ⚠️	5.4 ms	5.7 ms	+5.7% (1.06× slower) ⚠️	308.24 MiB	388.75 MiB	+26.1% (1.26× larger) ⚠️

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

Workflow logs

arthurpaulino force-pushed the ap/aiur-hash-width branch 2 times, most recently from b9c313d to 3a5e363 Compare July 13, 2026 15:21

arthurpaulino force-pushed the ap/aiur-hash-width branch 2 times, most recently from d7ccbaa to 25c59d5 Compare July 14, 2026 00:13

gabriel-barrett previously approved these changes Jul 17, 2026

View reviewed changes

arthurpaulino added 17 commits July 17, 2026 11:22

arthurpaulino dismissed gabriel-barrett’s stale review via ff8d1d5 July 17, 2026 18:43

arthurpaulino force-pushed the ap/aiur-hash-width branch from 25c59d5 to ff8d1d5 Compare July 17, 2026 18:43

arthurpaulino added 3 commits July 17, 2026 11:49

aiur: correct memory circuit width in statistics (size + 7)

1a240b3

Mirrors crates/aiur/src/memory.rs: multiplicity + selector + pointer + size value columns, plus one lookup -> 2*(1+1) stage-2 columns. The old size + 11 over-counted every memory circuit by 4.

arthurpaulino added 2 commits July 17, 2026 11:49

arthurpaulino force-pushed the ap/aiur-hash-width branch from ff8d1d5 to 9704022 Compare July 17, 2026 18:50

arthurpaulino closed this Jul 17, 2026

arthurpaulino deleted the ap/aiur-hash-width branch July 17, 2026 23:16

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Aiur hash circuits: value-based keccak-256, inlined calls, self-recursive rounds, and a generalized chain-rotate gadget#488

Aiur hash circuits: value-based keccak-256, inlined calls, self-recursive rounds, and a generalized chain-rotate gadget#488
arthurpaulino wants to merge 22 commits into
mainfrom
ap/aiur-hash-width

arthurpaulino commented Jul 13, 2026 •

edited

Loading

Uh oh!

arthurpaulino commented Jul 13, 2026

Uh oh!

argument-ci-bot Bot commented Jul 13, 2026

Uh oh!

arthurpaulino commented Jul 17, 2026

Uh oh!

argument-ci-bot Bot commented Jul 17, 2026

Uh oh!

arthurpaulino commented Jul 17, 2026

Uh oh!

argument-ci-bot Bot commented Jul 17, 2026

Uh oh!

samuelburnham commented Jul 17, 2026

Uh oh!

argument-ci-bot Bot commented Jul 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

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

Uh oh!

Summary

What's in here

Notes for reviewers

Testing

Follow-up (not in this PR)

Uh oh!

arthurpaulino commented Jul 13, 2026

Uh oh!

argument-ci-bot Bot commented Jul 13, 2026

!benchmark — main vs 3a5e363

aiur · InitStd · prove — main from: bencher @ 16455ba + base run (1 new)

Uh oh!

arthurpaulino commented Jul 17, 2026

Uh oh!

argument-ci-bot Bot commented Jul 17, 2026

!benchmark — main vs ff8d1d5

aiur-recursive · InitStd — main from: bencher @ 4e554d2

Uh oh!

arthurpaulino commented Jul 17, 2026

Uh oh!

argument-ci-bot Bot commented Jul 17, 2026

!benchmark — main vs 9704022

aiur · InitStd · prove — main from: bencher @ 4e554d2 + base run (1 new)

Uh oh!

samuelburnham commented Jul 17, 2026

Uh oh!

argument-ci-bot Bot commented Jul 17, 2026

!benchmark — main vs 9704022

aiur-recursive · InitStd — main from: bencher @ 4e554d2

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

arthurpaulino commented Jul 13, 2026 •

edited

Loading

`!benchmark` — main vs `3a5e363`

`aiur` · `InitStd` · `prove` — main from: bencher @ `16455ba` + base run (1 new)

`!benchmark` — main vs `ff8d1d5`

`aiur-recursive` · `InitStd` — main from: bencher @ `4e554d2`

`!benchmark` — main vs `9704022`

`aiur` · `InitStd` · `prove` — main from: bencher @ `4e554d2` + base run (1 new)

`!benchmark` — main vs `9704022`

`aiur-recursive` · `InitStd` — main from: bencher @ `4e554d2`