Aiur inlined function calls (@fn(args)) + blake3 G-function cleanup#500
Open
arthurpaulino wants to merge 2 commits into
Open
Aiur inlined function calls (@fn(args)) + blake3 G-function cleanup#500arthurpaulino wants to merge 2 commits into
@fn(args)) + blake3 G-function cleanup#500arthurpaulino wants to merge 2 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. Includes the regenerated Aiur kernel (`lake exe ix codegen`). All 56 kernel-check FFT costs unchanged (full `lake test -- --ignored ixvm` run green).
arthurpaulino
force-pushed
the
ap/aiur-inline-calls
branch
from
July 17, 2026 23:58
9a10452 to
b450039
Compare
arthurpaulino
enabled auto-merge (squash)
July 17, 2026 23:59
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
1 participant
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.
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 — 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 —
inlineCallseliminates.inlinedbefore typechecking. Interpreters match the mode as_(aninlined call executes identically to a normal one), so evaluation is
unchanged. Callee params and body are alpha-renamed to fresh
inl#Nlocals before argument binding, so nested
@-calls cannot capture callerbindings.
Aiur blake3: extract G-function word-ops into @-inlined helpers
blake3_g_functionwas ~100 lines of inlined byte arithmetic: sixlittle-endian carry chains, the add/xor/rotate quarter-round steps spelled
out per byte. Rewritten as its eight-step dataflow over
@-inlined wordops: ByteStream's existing
u32_add/u32_xor, plus fourright-rotations
u32_rotr16/u32_rotr8(byte moves) andu32_rotr12/u32_rotr7(byte move + chained gadget), added to ByteStreamnext to the other unsigned-int ops. Still one circuit, byte-identical
work. Includes the regenerated Aiur kernel.
Verification
lake test -- --ignored ixvmrun green (codegen/bytecode parity suiteincluded). The refactor is cost-neutral by construction; the pins prove it.