Uh oh!
There was an error while loading. Please reload this page.
IxVM ingress: blob-ref index, sidecar→rbtree, IOBuffer interface - #457
Merged
Conversation
arthurpaulinoforce-pushed
the
ap/ingress-refactor
branch
from
June 30, 2026 19:24
9c2eb23 to
ee4da06Compare`lookup_addr_pos`'s rbtree (`addr_pos_map`) only contained const addresses. Every blob ref (literal-blob payload pointers in `Constant.refs`) probed the map, missed, and fell through to the O(N) linear scan over `all_addrs` which also returned 0. Wasted work proportional to (blob refs × shard closure size). Add a third value class to the same rbtree: the sentinel `4294967295` (beyond any honest `pos+1`), inserted by walking each const's `refs` once via `augment_with_blob_refs`. Any ref not already mapped to a const-position gets the sentinel. `lookup_addr_pos` becomes a 3-way match: `0` → fall back to linear scan (now only fires under the de-intern soundness corner-case, ~never in practice); `SENTINEL` → return 0 directly (known blob); `pos+1` → return `pos`. `is_blob` mirrors the same match. Soundness preserved: every probe still relies on the positive direction `ptr_val` equality ⇒ content equality (Aiur Store's content-addressing invariant). The linear fallback stays put for the (still theoretical) malicious de-intern, where it uses content-based `address_eq`. `lake exe ix check --ixe init.ixe --ixes init.ixes --shard 51` (`ulimit -v 23000000`, with the kernel's blake3 paths in `load_verified_constant` / `load_verified_blob` / `load_verified_claim` stubbed for profiling): 119_152_044_062 → 102_190_540_489 FFT (-14.2%). Tests/Ix/IxVM.lean: 42 pin shifts absorbing the per-ingress augment-walk overhead.
A consolidated refactor of the ingress pipeline guided by a 5-reviewer synthesis of accidental complexity sites. Three families of change: PLUMBING * `Blake3.lean`: `verify_bytes_against(bytes, expected)` + `bytes_to_addr(bytes)` + `blake3_flat(input)` centralise the 24-line `[h[i][j]]` digest reshape that was hand-unrolled at 7 sites. ~100 lines of boilerplate deleted. * `Ingress.lean`: `load_payload_const`/`blob`/`hint` + `ch_const`/`blob`/`hint` factor the `io_get_info` + `#read_byte_stream` boilerplate at 6 sites. `load_verified_blob` no longer double-`load(addr)`s. * `sentinel_blob_ref()` named const replaces one bare `4294967295`. SIDECAR LISTS → RBTREE * `lookup_canon_addr`: O(N) parallel-list walk → O(log N) rbtree probe via new `build_canon_addr_map`. `canon_addrs: List<Addr>` arg replaced by `canon_addr_map: &RBTreeMap<Addr>` (one threaded ptr). * `lookup_block_start`: O(N) parallel-list walk → O(log N) rbtree probe via new `build_block_start_map`. `block_addrs` / `block_starts` args replaced by `block_start_map: &RBTreeMap<G>` across ~12 fn signatures. * `build_aux_recr_ctor_idxs` returns `(idxs, block_addr)` so the standalone-Recr caller in `build_convert_inputs_walk` doesn't redo the `rec_typ_to_inductive_addr` + `load_verified_constant` chain to recover `block_addr` — `build_aux_recr_ctor_idxs` already computed it internally. * `build_ref_idxs_and_blobs` fuses the two separate walks (`build_ref_idxs_mapped` + `build_lit_blobs`) into one — single rbtree probe per ref produces both `ref_idxs` and `lit_blobs`. 5 caller sites simplified. PTR-PASSING (per `reference_aiur_pass_pointer_not_value`) * `convert_univ(u: &Univ)`: per-row input width drops from 5-variant union to one G column. Caller `convert_univ_idxs` already produces the `&Univ` via `list_lookup(univs, idx)` — no extra `store`. * `convert_one(input: &ConvertInput)`: caller `convert_all` already has `&input` from the `ListNode.Cons` destructure. DEAD CODE DELETED `address_in_list`, `apply_ctor_overrides`, `lookup_override`, `build_lit_blobs`, `build_ref_idxs_mapped`, `is_blob`, `ctx_convert_expr` — all unused after the migrations above. TRIED + REVERTED (left as notes in code where instructive): * Fused `build_addr_pos_map` + `augment_with_blob_refs` single-pass. Lost to Aiur's per-row width tax — two narrower passes cheaper than one merged wide pass. * `convert_expr(ctx: &ConvertCtx)` ptr. Per-arm `load(ctx)` cost > raw-arg threading. * `compute_layout_walk` seen-mptrs/seen-poses → rbtree. Small regression on typical shards (few enough Muts blocks that O(N) list scan is already cheap; rbtree value column tax > savings). * `block_members_map` to skip per-projection `load_verified_constant`. Lost because Aiur memoises `load_verified_constant` automatically — the new rbtree probe's width tax exceeded the savings from the eliminated match cascade. * `ctx` everywhere as `&ConvertCtx` (with `store(...)` at 5 construction sites). The added `store` rows offset the per-row savings — wash. `lake test -- --ignored ixvm`: 42 pin shifts, all measurable wins vs the `ap/blob-ref-rbtree-augment` tip. Cumulative on heavy consts: * `Nat.add_comm`: 54_369_745 → 54_049_773 FFT (-0.59%) * `Nat.sub_le_of_le_add`: 515_331_420 → 510_843_459 FFT (-0.87%) * `Array.append_assoc`: 2_567_087_893 → 2_537_360_311 FFT (-1.16%) * `Vector.append`: 2_639_286_078 → 2_607_800_745 FFT (-1.19%) * `String.Internal.append`: 718_803_075 → 708_296_270 FFT (-1.46%) * `IxVMInd.Even.rec`: 31_659_493 → 31_434_525 FFT (-0.71%) * `_private....extractMainModule._unsafe_rec`: 1_081_617_705 → 1_064_689_765 FFT (-1.57%)
Replaces channel 0's tagged-union (claim / tree / const bytes / empty- blob-marker, distinguished only by key content-hash collision- impossibility) with one channel per value kind. Channel reorganization is cost-neutral — all six per-channel `io_get_info` + `#read_byte_stream` pairs are inlined at the single consumer of each channel, so no fn-call row gets added. New layout, tiered by access pattern: | Tier | Channel | Purpose | Key | Value | |-------|---------|--------------------------|-------------------------|----------------------| | Ctrl | 0 | claim wire bytes | `blake3(claim_bytes)` | claim bytes | | Ctrl | 1 | assumption tree bytes | `tree.root` | tree bytes | | Const | 2 | constant wire bytes | const addr | const bytes | | Const | 3 | Defn reducibility hint | Defn addr | single G | | Blob | 4 | blob discriminator | addr | one byte (1=const, 0=blob) | | Blob | 5 | blob raw bytes | blob addr | raw bytes | Tier 1 = one-per-`verify_claim`. Tier 2 = per-const. Tier 3 = per-blob. `io_get_info(channel, key)` is now unambiguous by channel alone. Aiur side (`Ingress.lean`, `Kernel/Claim.lean`): * `load_verified_constant` inlines `io_get_info(2, raw)` + `#read_byte_stream(2, ...)` (was ch 0). * `load_verified_blob` inlines ch 5 read (was ch 1). * `load_constant_hint` inlines ch 3 read (was ch 2). * `load_with_deps` inlines a ch 4 discriminator probe replacing the former `io_get_info(0, addr).len == 0 ⟹ blob` hack on ch 0. One read_byte for the per-addr discriminator byte. * `load_verified_claim` inlines ch 0 (was using a shared `load_payload_const` helper on ch 0). * `load_assumption_tree` inlines ch 1 (was using same `load_payload_const` helper on ch 0). * Helper wrappers (`load_payload_claim/tree/const/hint/blob`, `load_discriminator`, `ch_*` constants) all removed — every channel has exactly one consumer site and the inlined dispatch costs no fn call. * Top-of-file `IxVM IOBuffer interface` doc block documents the layout + soundness model. Lean side (`ClaimHarness.lean`): * `addEntries` writes per channel — consts → ch 2 + per-addr discriminator `[1]` on ch 4; blobs → ch 5 + per-addr discriminator `[0]` on ch 4; Defn hints → ch 3. * `seedTreeAt` writes tree bytes to ch 1 (was ch 0). * `buildClaimWitness` writes claim bytes to ch 0 (unchanged). * Drops the empty-marker write on ch 0 for blob addrs — the ch 4 discriminator covers blob/const classification explicitly. * Top-of-section `IxVM IOBuffer interface` doc block mirrors the Aiur-side comment. Soundness model unchanged. ch 0/1/2/5 byte streams are blake3-verified by the kernel against their content-addressed keys. ch 3 hint is semantically optional (controls WHNF reduction heuristic only; def-eq is sound either way). ch 4 discriminator is sound by erasure- correctness — a lying byte flips the const/blob decision and the wrong-path load downstream fails (a "const" blob triggers a ch 2 read that returns empty → blake3 verify against the non-empty addr fails; a "blob" const dangles references → typecheck fail). `lake test -- --ignored ixvm` green; 42 pins shifted within ±0.010% (noise-tier) vs the pre-shuffle baseline — channel reorganization is cost-neutral as required, the discriminator's one read_byte trades against the eliminated `io_get_info(0, ...).len` check.
arthurpaulinoforce-pushed
the
ap/ingress-refactor
branch
from
July 2, 2026 14:44
ee4da06 to
64390adCompare`blake3_flat` was a pure array-reshaping wrapper around `blake3` used by `verify_bytes_against` and `bytes_to_addr`. Inline the reshape at both call sites. `blake3`'s memoization key is the input ByteStream, so the 74 cache hits that `blake3_flat` recorded migrate cleanly to `blake3` — dedup preserved. Measured with `lake exe ix check Std.Time.Week.Offset.ofMilliseconds`: - Total FFT cost: 12,430,898,064 → 12,430,154,083 (−743,981) - Total width: 33,755 → 33,714 (−41) - `blake3_flat` (41w × 1692h, 74 hits, 743,981 FFT) — removed - `blake3` (92w × 1692h, 0 hits, ...) → now 74 hits Same experiment for `bytes_to_addr` inline was neutral (−5k FFT, +92 width across 4 call sites) — kept as a wrapper.
arthurpaulinoforce-pushed
the
ap/ingress-refactor
branch
from
July 2, 2026 15:06
ac54eef to
1fb0dd1Comparearthurpaulino
marked this pull request as ready for review
July 2, 2026 15:06
arthurpaulino
enabled auto-merge (squash)
July 2, 2026 15:06
Mirror the Expr port pattern (`KExpr = &KExprNode`) for universe levels.
Kernel-side universe reps flip from unboxed enum values to pointer
aliases:
Before:
enum KLevel {
Zero,
Succ(&KLevel),
Max(&KLevel, &KLevel),
IMax(&KLevel, &KLevel),
Param(G)
}
After:
enum KLevelNode {
Zero,
Succ(KLevel),
Max(KLevel, KLevel),
IMax(KLevel, KLevel),
Param(G)
}
type KLevel = &KLevelNode
Callers switch from passing whole enum values to passing pointers.
Every match on a KLevel arg gains a `load()`; every value construction
that fills a KLevel arg or return slot gets a `store()`. `KExprNode.Srt`,
`KConstantInfo.{Ctor,Axiom,Defn,Thm,Opaque,Quot,Induct,Rec}` universe
fields all use the aliased `KLevel` now.
Motivation: pass-by-pointer shrinks per-row input width on every level-
manipulating function (`level_eq`, `level_leq`, `level_reduce`,
`level_inst_params`, ...), same trick as
`reference_aiur_pass_pointer_not_value`. Compared to the Expr port the
delta is smaller because level fns are already narrow, but it stacks.
Measured with `lake exe ix check Std.Time.Week.Offset.ofMilliseconds`:
- Total FFT cost: 12,430,154,083 -> 12,418,344,860 (-11,809,223)
- Total width: 33,714 -> 33,532 (-182)
Re-pin every FFT cost shifted by the port.gabriel-barrett
approved these changes
Jul 2, 2026
Uh oh!
There was an error while loading. Please reload this page.
johnchandlerburnham pushed a commit
that referenced
this pull request
Jul 21, 2026
…505) * IxVM: drop dead KValNode/KVal/KValEnv From ap/kernel 828fb85 (Arthur Paulino): the NbE value domain is defined but referenced nowhere — the live kernel runs on de-Bruijn KExpr; vestigial from an abandoned NbE direction. (The closed-term context normalization from that commit was measured separately and not taken: the per-call expr_lbr probe cost +2.9% FFT on recursor loops for a 0.5% record reduction.) * IxVM: memoized prim_family dispatch + width-safe offset-stuck placement Three coordinated changes to Const-head whnf dispatch (cherry-pick of 130f30b, adapted to post-#450/#457 main): 1. prim_family(addr) classifies a head address into the one reducer family that could fire on it (nat/str/bitvec/native/decidable; the sets are disjoint). Keyed on the ADDRESS ALONE it memoizes to one row per distinct constant address per run, and whnf_const_head calls at most one family reducer. The previous gauntlet ran every reducer in sequence for guaranteed misses. 2. The symbolic-Nat offset-stuck check moves from a delta-arm probe into try_nat_dispatch's miss path as a cold function (try_nat_offset_dispatch, verdict 2 = "already stuck, do not re-whnf"), with the offset construction shared via mk_nat_offset_stuck (also used by the linear-rec collapse). 3. nat_lit_to_ctor_or_self exposes ONE constructor layer (n -> succ(Lit(n-1))) instead of materializing the full succ chain. Adaptations vs the original patch: - whnf_nd_const_head (no-delta WHNF, added on main after the patch) converted to the same family dispatch. - Kept main's cold-extracted try_nat_binop_dispatch and routed the symbolic-base case to try_nat_offset_dispatch from its miss arm. Measured (lake exe ix check Nat.add_comm): total width 34820 -> 34806, FFT cost 49571210 -> 48860647 (-1.43%). All 53 ixvm-suite FFT pins decreased (-0.19%..-1.43%); parity and claim smokes pass. Pins updated; crates/ixvm-codegen/src/aiur_ixvm.rs regenerated via `lake exe ix codegen`. * IxVM: port jcb/fixes H-14 — ptr_val skip map + lockstep addr cursor Two quadratic/constant-factor fixes to check_all_skipping, ported from jcb/fixes (3763356, John C. Burnham); cherry-pick of 2d83be1 adapted to post-#457 main: - The assumption-leaf skip set keys on ptr_val instead of the first 4 address bytes: one tree lookup per constant, no per-lookup address load, no confirming address_eq. Sound by the build_addr_pos_map interning invariant (one pointer, one content): a ptr hit implies the address IS a leaf; a de-interned pointer reads as absent and the constant just gets checked — fail-closed. - The iterator walks the addrs list in LOCKSTEP with consts (cur_addrs suffix) instead of list_lookup(addrs, pos) per constant, which re-walked the prefix every iteration — a standalone O(closure^2). Adaptations: kept main's two-arg check_canonical_block_sort call; addr_key retained (the Inductive.lean block-membership table added on main after this patch still uses it), comment updated. Measured (lake exe ix check Nat.add_comm): total width 34806 -> 34781, FFT cost unchanged (plain checks never take the skip path). Full ixvm suite green incl. the frontier-assumption claim smoke; all FFT pins unchanged. crates/ixvm-codegen/src/aiur_ixvm.rs regenerated. --------- Co-authored-by: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
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 freeto 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.
Three commits on top of
mainthat cut ingress FFT cost on heavy shards and land a documented IxVM IOBuffer interface.Measurement methodology — read first
Shard 51 with unstubbed blake3 currently OOMs at all practical
ulimitsettings on the dev machine. To get past memory exhaustion and produce a comparative measurement, the kernel's blake3 verification paths inload_verified_constant/load_verified_blob/load_verified_claimwere stubbed to no-ops for profiling. The stubs are not part of any committed code in this PR — they were applied locally during measurement and reverted.What this means for the numbers below:
Every shard-51 number below is a "blake3-stubbed trace" measurement. Per-const numbers from
lake test -- --ignored ixvm(no stubs) are unaffected and reflect real production cost.Headline
Vector.append(production, unstubbed)Array.append_assoc(production)_private...extractMainModule._unsafe_rec(production)Per-const wins are end-to-end on the real (unstubbed) kernel; the shard-51 delta is real on the non-blake3 portion of the trace.
Commits
1.
120001d— IxVM kernel: augmentaddr_pos_mapwith blob-ref sentinelslookup_addr_pos's rbtree only contained const addresses. Every blob ref (literal-blob payload pointers inConstant.refs) probed the map, missed, and fell through to the O(N) linear scan overall_addrswhich also returned 0. Wasted work proportional to (blob refs × shard closure size).This commit adds a third value class to the same rbtree: a sentinel
4294967295(beyond any honestpos+1), inserted by walking each const'srefsonce viaaugment_with_blob_refs.lookup_addr_posbecomes a 3-way match:0→ fall back to linear scan (now only fires under the de-intern soundness corner-case, ~never in practice);SENTINEL→ return 0 directly (known blob);pos+1→ returnpos.Shard 51 (blake3-stubbed): 119_152_044_062 → 102_190_540_489 — −14.2% on the non-blake3 portion.
address_eqrow count drops from ~10.3M to ~3.4M (−67%);lookup_addr_pos_linearfalls out of the top-25 cost table. The augment-walk's added rbtree probes (~430M FFT in the stubbed trace) are paid back many times over by the ~17B FFT saved on lookups.Soundness: every probe still relies on the positive direction
ptr_valequality ⇒ content equality (Aiur Store content-addressing invariant). The linear fallback stays for the (still theoretical) malicious de-intern, where it uses content-basedaddress_eq.2.
9acbd58— IxVM ingress: plumbing helpers + sidecar→rbtree migrations + ptr-passingA 5-reviewer synthesis of ingress accidental complexity drove this consolidated refactor. Three families of change.
Plumbing helpers:
verify_bytes_against(bytes, expected)+bytes_to_addr(bytes)+blake3_flat(input)centralise the 24-line[h[i][j]]digest reshape that was hand-unrolled at 7 sites. ~100 lines of boilerplate deleted.io_get_info+#read_byte_streamboilerplate at 6 sites.load_verified_blobno longer double-load(addr)s.sentinel_blob_ref()named const replaces one bare4294967295.Sidecar lists → rbtree:
lookup_canon_addr: O(N) parallel-list walk → O(log N) rbtree probe via newbuild_canon_addr_map.canon_addrs: List<Addr>arg replaced bycanon_addr_map: &RBTreeMap<Addr>(one threaded ptr).lookup_block_start: O(N) parallel-list walk → O(log N) rbtree probe via newbuild_block_start_map.block_addrs/block_startsargs replaced byblock_start_map: &RBTreeMap<G>across ~12 fn signatures.build_aux_recr_ctor_idxsreturns(idxs, block_addr)so the standalone-Recr caller doesn't redo therec_typ_to_inductive_addr+load_verified_constantchain to recoverblock_addr.build_ref_idxs_and_blobsfuses the two separate walks (build_ref_idxs_mapped+build_lit_blobs) into one — single rbtree probe per ref produces bothref_idxsandlit_blobs. 5 caller sites simplified.Pointer-passing (per Aiur's
inputSize→widthcost model):convert_univ(u: &Univ): per-row input width drops from 5-variant union to one G column. Callerconvert_univ_idxsalready produces the&Univvialist_lookup(univs, idx)— no extrastore.convert_one(input: &ConvertInput): callerconvert_allalready has&inputfrom theListNode.Consdestructure.Dead code deleted:
address_in_list,apply_ctor_overrides,lookup_override,build_lit_blobs,build_ref_idxs_mapped,is_blob,ctx_convert_expr.Shard 51 (blake3-stubbed): 102_190_540_489 → 93_939_967_063 — −8.07% on the non-blake3 portion on top of
120001d.Per-const wins on heavy production targets (unstubbed
lake test):Nat.add_commNat.sub_le_of_le_addNat.decLeArray.append_assocVector.appendIxVMInd.Even.recIxVMInd.Odd.recString.Internal.append_private...extractMainModule._unsafe_reclake test -- --ignored ixvmgreen; 42 pins re-pinned.3.
9c2eb23— IxVM: per-kind IOBuffer channels with documented interfaceThe pre-existing IOBuffer multiplexed claim bytes, assumption tree bytes, constant wire bytes, and a per-blob-addr empty-marker on a single channel 0, distinguished only by blake3 content-hash collision-impossibility. A new contributor reading
load_payload_const(key)couldn't tell from the helper whether they were getting a const, a claim, or a tree — only the caller knew the intent.This commit splits channel 0 into per-kind channels and lands a documented IxVM IOBuffer interface block (mirrored on both Aiur and Lean sides).
blake3(claim_bytes)tree.rootTier 1 fires once per
verify_claim. Tier 2 fires per constant traversed duringload_with_deps. Tier 3 fires per blob ref encountered duringbuild_ref_idxs_and_blobs.The blob discriminator (ch 4) replaces the previous
io_get_info(0, addr).len == 0 ⟹ blobhack insideload_with_depswith an explicit per-addr one-byte payload. No morelen-as-meaning overload.Every per-channel
io_get_info+#read_byte_streampair is inlined at the single consumer of each channel — no fn-call row gets added for the reorganization. Channel reorganization is cost-neutral by design, confirmed by measurement: per-const pin shifts vs9acbd58land within ±0.010% (noise-tier; the ch-4 discriminator's oneread_bytetrades against the eliminatedio_get_info(0, addr).lencheck).The win here is review-time clarity, not FFT —
io_get_info(channel, key)now has one value shape per channel and a doc block both kernel and harness reference.Soundness: ch 0/1/2/5 byte streams are blake3-verified by the kernel against their content-addressed keys. ch 3 hint is semantically optional (controls WHNF reduction heuristic only; def-eq is sound either way). ch 4 discriminator is sound by erasure-correctness — a lying byte flips the const/blob decision and the wrong-path load downstream fails (a "const" blob triggers a ch 2 read that returns empty → blake3 verify against the non-empty addr fails; a "blob" const dangles references → typecheck fail).
Cumulative measurement (vs
main)Nat.add_commNat.decLeNat.sub_le_of_le_addArray.append_assocVector.appendString.Internal.append_private...extractMainModule._unsafe_recTest plan
lake buildcleanlake test -- --ignored ixvmgreen at every commit