From c99b3618e8a13bdf0ea5defaab5be9d6b2bfe85c Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Tue, 23 Jun 2026 18:12:36 -0700 Subject: [PATCH 1/4] IxVM kernel: klimbs_pow via binary exponentiation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace `klimbs_mul(base, klimbs_pow(base, klimbs_dec(exp)))`'s O(exp) per-step memo growth with a binary-exponentiation recursion of depth O(log exp). Both `exp / 2` and `exp % 2` route through the native `unconstrained_big_uint_div_mod` op, so each level pays O(1) for the division — `log2(exp)` memo entries for `klimbs_pow` itself + the `klimbs_mul(base, base)` doublings. `lake test -- --ignored ixvm` on `IxVMPrim.nat_pow_big` (`(2 ^ 16384 : Nat) - 2 ^ 16384 = 0`, measured against the current `ap/utf8-mod-witness` baseline): 3_941_276_885 → 71_856_587 FFT (-98.2%). Tests/Ix/IxVM.lean: * new `IxVMPrim.nat_pow_big` synthetic — exercises `klimbs_pow` at a non-trivial exponent (`2 ^ 16384`) so future regressions in the body shift its FFT pin. * small pin shifts in `nat_shl_lit`, `nat_shr_lit`, `nat_div_lit`, `nat_mod_lit`, `nat_gcd_lit`, `bv_to_nat_lit` — all reduce via `klimbs_pow` / `klimbs_div_mod` and absorb the new cost shape. --- Ix/IxVM/Kernel/Primitive.lean | 19 ++++++++++++++++++- Tests/Ix/IxVM.lean | 14 +++++++++++--- 2 files changed, 29 insertions(+), 4 deletions(-) diff --git a/Ix/IxVM/Kernel/Primitive.lean b/Ix/IxVM/Kernel/Primitive.lean index 6462e3be..2254f08b 100644 --- a/Ix/IxVM/Kernel/Primitive.lean +++ b/Ix/IxVM/Kernel/Primitive.lean @@ -1152,10 +1152,27 @@ def primitive := ⟦ } } + -- Binary exponentiation. Replaces the old O(exp) recursive + -- `klimbs_mul(base, klimbs_pow(base, klimbs_dec(exp)))` body, which + -- created one per-fn memo row per exponent step and OOM'd for + -- non-trivial exponents. Recursion depth is `log2(exp)` — for + -- `exp = 2^32` that's 32 memo entries instead of 4 billion. + -- + -- Both `klimbs_div2` (= `klimbs_div(exp, 2)`) and `klimbs_is_odd` + -- (= `klimbs_mod(exp, 2) != 0`) route through `klimbs_div_mod`, which + -- is itself native (unconstrained_big_uint_div_mod) — so the + -- division per step is O(1) work. fn klimbs_pow(base: KLimbs, exp: KLimbs) -> KLimbs { match klimbs_is_zero(exp) { 1 => store(ListNode.Cons([1u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8], store(ListNode.Nil))), - 0 => klimbs_mul(base, klimbs_pow(base, klimbs_dec(exp))), + 0 => + let two = store(ListNode.Cons([2u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8], store(ListNode.Nil))); + let (half, r) = klimbs_div_mod(exp, two); + let sq = klimbs_pow(klimbs_normalize(klimbs_mul(base, base)), klimbs_normalize(half)); + match klimbs_is_zero(r) { + 1 => sq, + 0 => klimbs_mul(base, sq), + }, } } diff --git a/Tests/Ix/IxVM.lean b/Tests/Ix/IxVM.lean index 41c7ac42..d73e870d 100644 --- a/Tests/Ix/IxVM.lean +++ b/Tests/Ix/IxVM.lean @@ -44,6 +44,13 @@ public theorem nat_lor_lit : Nat.lor 0xf0 0x0f = 0xff := rfl public theorem nat_xor_lit : Nat.xor 0xff 0x0f = 0xf0 := rfl public theorem nat_shl_lit : Nat.shiftLeft 1 8 = 256 := rfl public theorem nat_shr_lit : Nat.shiftRight 256 4 = 16 := rfl +-- Synthetic: exercises `klimbs_pow` at a non-trivial exponent so the cost +-- of the current O(exp) recursive implementation shows up in the FFT pin. +-- Sized to terminate under typical caps with the current O(exp) body — a +-- proxy for the eventual binary-exponentiation rewrite. +set_option exponentiation.threshold 65536 in +set_option maxRecDepth 65536 in +public theorem nat_pow_big : (2 ^ 16384 : Nat) - (2 ^ 16384) = 0 := rfl -- Nat predicates (return Bool ctors) public theorem nat_beq_lit : Nat.beq 42 42 = true := rfl @@ -141,15 +148,16 @@ private def kernelCheckEntries : List (String × Nat) := [ ("IxVMPrim.nat_land_lit", 1_019_743_752), ("IxVMPrim.nat_lor_lit", 1_020_972_680), ("IxVMPrim.nat_xor_lit", 1_029_804_417), - ("IxVMPrim.nat_shl_lit", 34_843_370), - ("IxVMPrim.nat_shr_lit", 372_727_841), + ("IxVMPrim.nat_shl_lit", 34_836_668), + ("IxVMPrim.nat_shr_lit", 372_729_464), + ("IxVMPrim.nat_pow_big", 71_856_587), ("IxVMPrim.nat_beq_lit", 24_108_404), ("IxVMPrim.nat_ble_lit", 22_469_243), ("IxVMPrim.nat_dec_le", 198_104_580), ("IxVMPrim.nat_dec_lt", 202_076_479), ("IxVMPrim.nat_dec_eq", 82_352_518), ("IxVMPrim.str_size_lit", 733_902_817), - ("IxVMPrim.bv_to_nat_lit", 577_368_692), + ("IxVMPrim.bv_to_nat_lit", 577_322_203), -- Mutual block + multi-member recursors ("IxVMInd.Even", 25_965_406), ("IxVMInd.Odd", 25_728_543), From 27fc940bb8b6f533141151bbc81b4553abd76e06 Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Wed, 24 Jun 2026 10:32:23 -0700 Subject: [PATCH 2/4] IxVM kernel: augment addr_pos_map with blob-ref sentinels MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `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. --- Ix/IxVM/Ingress.lean | 74 ++++++++++++++++++++++++++++++++++---- Tests/Ix/IxVM.lean | 84 ++++++++++++++++++++++---------------------- 2 files changed, 109 insertions(+), 49 deletions(-) diff --git a/Ix/IxVM/Ingress.lean b/Ix/IxVM/Ingress.lean index 5fee5918..56987ed7 100644 --- a/Ix/IxVM/Ingress.lean +++ b/Ix/IxVM/Ingress.lean @@ -137,16 +137,16 @@ def ingress := ⟦ } } - -- Check if an address is a blob: it's a blob iff it's NOT a constant, - -- i.e. absent from `addr_pos_map` (which is keyed by every constant - -- address — see `build_addr_pos_map`). Membership only; the stored - -- position value (pos+1 ≥ 1) is irrelevant here, only "present vs 0". - -- Blob addresses and constant addresses are different by design - -- (different hash preimage structures). O(log N) tree lookup. + -- Check if an address is a blob via the augmented `addr_pos_map`: + -- value == 0 (absent) → conservatively blob (the historical semantics; + -- sound because a content-bound blob load downstream re-verifies); + -- value == 4294967295 (SENTINEL) → known blob ref; + -- value > 0 and < SENTINEL (pos+1) → known const. fn is_blob(addr: Addr, addr_pos_map: &RBTreeMap‹G›) -> G { let hit = rbtree_map_lookup_or_default(ptr_val(addr), load(addr_pos_map), 0); match hit { 0 => 1, + 4294967295 => 1, _ => 0, } } @@ -227,11 +227,27 @@ def ingress := ⟦ -- fall back to the content-based `address_eq` scan, which returns 0 when -- truly absent. Honest provers always intern, so the fallback adds ~0 -- rows to the honest trace; the hot path is the O(log N) tree lookup. + -- Single-map ptr_val lookup. After `build_addr_pos_map_aug`, the map + -- carries three classes of value for an address key: + -- * 0 → not registered (truly unknown OR de-interned const) + -- * SENTINEL → known blob ref (= 4294967295, beyond any honest pos+1) + -- * pos+1 → known const at position `pos` + -- The blob class is populated once per ingress by walking every + -- constant's `refs` and inserting any non-const ref with SENTINEL. + -- Blob-ref lookups (the dominant non-const-ref traffic) now hit the + -- O(log N) probe and short-circuit to 0 without scanning. + -- + -- ptr_val-key soundness: ptr equality → content equality (positive + -- direction, sound because Aiur's Store content-addresses by content). + -- Hit on either pos+1 or SENTINEL is sound by ptr equality. Miss falls + -- through to the content-based linear scan, which catches any + -- de-interned const at its true position. fn lookup_addr_pos(target: Addr, addr_pos_map: &RBTreeMap‹G›, all_addrs: List‹Addr›, pos_map: List‹G›) -> G { let hit = rbtree_map_lookup_or_default(ptr_val(target), load(addr_pos_map), 0); match hit { 0 => lookup_addr_pos_linear(target, all_addrs, pos_map), + 4294967295 => 0, _ => hit - 1, } } @@ -285,6 +301,45 @@ def ingress := ⟦ } } + -- Walk all constants' `refs`. For every ref whose ptr_val is NOT + -- already mapped to a const-position (= a true const-ref), insert it + -- with the BLOB sentinel `4294967295`. Result: every ref a const + -- carries is classified at build time; `lookup_addr_pos` short-circuits + -- O(N) linear scans on blob refs to O(log N) probes. + -- + -- Duplicate refs across consts hit the existing entry on subsequent + -- inserts; the probe-before-insert prevents overwriting a const's + -- pos+1 entry. The walk is O(R log N) where R = total refs in the + -- shard's closure, N = #consts + #unique-blob-refs. + fn augment_with_blob_refs(consts: List‹&Constant›, m: RBTreeMap‹G›) -> RBTreeMap‹G› { + match load(consts) { + ListNode.Nil => m, + ListNode.Cons(&c, rest) => + match c { + Constant.Mk(_, _, refs, _) => + let m1 = insert_refs_as_blobs(refs, m); + augment_with_blob_refs(rest, m1), + }, + } + } + + fn insert_refs_as_blobs(refs: List‹Addr›, m: RBTreeMap‹G›) -> RBTreeMap‹G› { + match load(refs) { + ListNode.Nil => m, + ListNode.Cons(addr, rest) => + let key = ptr_val(addr); + let hit = rbtree_map_lookup_or_default(key, m, 0); + match hit { + 0 => + -- Not yet registered: classify as blob ref via SENTINEL. + insert_refs_as_blobs(rest, rbtree_map_insert(key, 4294967295, m)), + _ => + -- Already a const (pos+1) or already a blob (SENTINEL): leave alone. + insert_refs_as_blobs(rest, m), + }, + } + } + -- Find the start position of a block by its block address. fn lookup_block_start(target: Addr, block_addrs: List‹Addr›, block_starts: List‹G›) -> G { match load(block_addrs) { @@ -1034,7 +1089,12 @@ def ingress := ⟦ pos: G ) -> List‹&ConvertInput› { -- Built once here; threaded as the fast-path index for `lookup_addr_pos`. - let addr_pos_map = store(build_addr_pos_map(all_addrs, pos_map)); + -- The base map carries `pos+1` for each const; `augment_with_blob_refs` + -- then walks every const's `refs` and tags every previously-unregistered + -- ref with the BLOB sentinel (4294967295), so blob-ref lookups + -- short-circuit instead of falling through to the O(N) linear scan. + let base_map = build_addr_pos_map(all_addrs, pos_map); + let addr_pos_map = store(augment_with_blob_refs(consts, base_map)); build_convert_inputs_walk(consts, cur_addrs, all_addrs, addr_pos_map, pos_map, canon_addrs, block_addrs, block_starts, pos, store(ListNode.Nil)) diff --git a/Tests/Ix/IxVM.lean b/Tests/Ix/IxVM.lean index d73e870d..45ae64e1 100644 --- a/Tests/Ix/IxVM.lean +++ b/Tests/Ix/IxVM.lean @@ -122,53 +122,53 @@ public def kernelCheck (name : Lean.Name) (env : Lean.Environment) : observed cost in the message so it can be pasted back. -/ private def kernelCheckEntries : List (String × Nat) := [ -- Stdlib - ("HEq", 1_715_513), - ("HEq.rec", 2_681_137), - ("Eq.rec", 2_575_090), - ("Nat", 1_857_572), - ("Nat.add", 12_973_039), - ("Nat.add_comm", 54_350_110), - ("Nat.decEq", 68_538_632), - ("Nat.decLe", 191_354_793), - ("Nat.sub_le_of_le_add", 515_056_158), + ("HEq", 1_715_966), + ("HEq.rec", 2_682_331), + ("Eq.rec", 2_576_284), + ("Nat", 1_858_025), + ("Nat.add", 12_983_943), + ("Nat.add_comm", 54_330_980), + ("Nat.decEq", 68_594_289), + ("Nat.decLe", 191_364_012), + ("Nat.sub_le_of_le_add", 515_130_560), -- Newly-unlocked targets (level_leq Géran normalize). - ("Trans.mk", 2_863_374), - ("Array.append_assoc", 2_588_157_538), - ("Vector.append", 2_661_244_845), + ("Trans.mk", 2_864_146), + ("Array.append_assoc", 2_566_382_883), + ("Vector.append", 2_638_552_021), -- Primitive reduction theorems (`IxVMPrim`) - ("IxVMPrim.nat_add_lit", 28_083_713), - ("IxVMPrim.nat_sub_lit", 33_755_207), - ("IxVMPrim.nat_mul_lit", 24_642_249), - ("IxVMPrim.nat_mul_big", 24_116_975), - ("IxVMPrim.nat_div_lit", 367_262_842), - ("IxVMPrim.nat_mod_lit", 375_958_840), - ("IxVMPrim.nat_succ_lit", 7_307_039), - ("IxVMPrim.nat_pred_lit", 14_682_236), - ("IxVMPrim.nat_gcd_lit", 605_514_332), - ("IxVMPrim.nat_land_lit", 1_019_743_752), - ("IxVMPrim.nat_lor_lit", 1_020_972_680), - ("IxVMPrim.nat_xor_lit", 1_029_804_417), - ("IxVMPrim.nat_shl_lit", 34_836_668), - ("IxVMPrim.nat_shr_lit", 372_729_464), - ("IxVMPrim.nat_pow_big", 71_856_587), - ("IxVMPrim.nat_beq_lit", 24_108_404), - ("IxVMPrim.nat_ble_lit", 22_469_243), - ("IxVMPrim.nat_dec_le", 198_104_580), - ("IxVMPrim.nat_dec_lt", 202_076_479), - ("IxVMPrim.nat_dec_eq", 82_352_518), - ("IxVMPrim.str_size_lit", 733_902_817), - ("IxVMPrim.bv_to_nat_lit", 577_322_203), + ("IxVMPrim.nat_add_lit", 28_082_349), + ("IxVMPrim.nat_sub_lit", 33_722_451), + ("IxVMPrim.nat_mul_lit", 24_644_737), + ("IxVMPrim.nat_mul_big", 24_146_724), + ("IxVMPrim.nat_div_lit", 366_893_945), + ("IxVMPrim.nat_mod_lit", 375_602_678), + ("IxVMPrim.nat_succ_lit", 7_314_408), + ("IxVMPrim.nat_pred_lit", 14_706_095), + ("IxVMPrim.nat_gcd_lit", 605_222_820), + ("IxVMPrim.nat_land_lit", 1_019_495_718), + ("IxVMPrim.nat_lor_lit", 1_020_299_077), + ("IxVMPrim.nat_xor_lit", 1_029_101_731), + ("IxVMPrim.nat_shl_lit", 34_802_946), + ("IxVMPrim.nat_shr_lit", 372_209_350), + ("IxVMPrim.nat_pow_big", 71_850_166), + ("IxVMPrim.nat_beq_lit", 24_145_604), + ("IxVMPrim.nat_ble_lit", 22_475_134), + ("IxVMPrim.nat_dec_le", 198_007_550), + ("IxVMPrim.nat_dec_lt", 201_972_221), + ("IxVMPrim.nat_dec_eq", 82_417_673), + ("IxVMPrim.str_size_lit", 726_987_300), + ("IxVMPrim.bv_to_nat_lit", 576_925_093), -- Mutual block + multi-member recursors - ("IxVMInd.Even", 25_965_406), - ("IxVMInd.Odd", 25_728_543), - ("IxVMInd.Even.rec", 31_629_158), - ("IxVMInd.Odd.rec", 31_628_265), + ("IxVMInd.Even", 25_974_275), + ("IxVMInd.Odd", 25_737_413), + ("IxVMInd.Even.rec", 31_628_577), + ("IxVMInd.Odd.rec", 31_627_681), -- Nested inductive + aux recursor (Tree.mk : List Tree → Tree) - ("IxVMInd.Tree", 2_634_462), - ("IxVMInd.Tree.rec", 4_870_642), + ("IxVMInd.Tree", 2_635_546), + ("IxVMInd.Tree.rec", 4_874_311), -- Edge cases from prelude - ("String.Internal.append", 725_415_461), - ("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 1_091_354_031), + ("String.Internal.append", 718_452_811), + ("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 1_081_131_375), ] private def nameOfString (str : String) : Lean.Name := From 696ee2b01ee6b93ff7fbe16e77fa86e311872928 Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Sat, 27 Jun 2026 11:06:32 -0700 Subject: [PATCH 3/4] =?UTF-8?q?IxVM=20ingress:=20plumbing=20helpers=20+=20?= =?UTF-8?q?sidecar=E2=86=92rbtree=20migrations=20+=20ptr-passing?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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` arg replaced by `canon_addr_map: &RBTreeMap` (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` 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%) --- Ix/IxVM/Blake3.lean | 29 +++ Ix/IxVM/Convert.lean | 156 +++++++------ Ix/IxVM/Ingress.lean | 455 ++++++++++++++++---------------------- Ix/IxVM/Kernel/Claim.lean | 57 +---- Tests/Ix/IxVM.lean | 84 +++---- 5 files changed, 360 insertions(+), 421 deletions(-) diff --git a/Ix/IxVM/Blake3.lean b/Ix/IxVM/Blake3.lean index 7412c6e4..fa06ded8 100644 --- a/Ix/IxVM/Blake3.lean +++ b/Ix/IxVM/Blake3.lean @@ -45,6 +45,35 @@ def blake3 := ⟦ blake3_compress_layer(load(blake3_compress_chunks(input, store(ListNode.Nil), 0, 0, store([0u8; 8]), store(IV), store(Layer.Nil)))) } + -- Flatten blake3's [[U8;4];8] output into the [U8;32] form every caller wants. + fn blake3_flat(input: ByteStream) -> [U8; 32] { + let h = blake3(input); + [h[0][0], h[0][1], h[0][2], h[0][3], + h[1][0], h[1][1], h[1][2], h[1][3], + h[2][0], h[2][1], h[2][2], h[2][3], + h[3][0], h[3][1], h[3][2], h[3][3], + h[4][0], h[4][1], h[4][2], h[4][3], + h[5][0], h[5][1], h[5][2], h[5][3], + h[6][0], h[6][1], h[6][2], h[6][3], + h[7][0], h[7][1], h[7][2], h[7][3]] + } + + -- Hash `bytes` and assert the digest equals `expected`. Used by every + -- IOBuffer-load path that verifies the pre-image of a content-addressed + -- pointer matches the bytes the prover supplied. + fn verify_bytes_against(bytes: ByteStream, expected: [U8; 32]) { + assert_eq!(blake3_flat(bytes), expected); + () + } + + -- Hash `bytes` and intern the digest into the Store. Returned pointer is + -- the canonical content-addressed `Addr` shape (`&[U8;32]`). Used by every + -- site that synthesises an address from raw bytes (e.g. `expr_addr`, + -- `leaf_hash`, `node_hash`, `cprj_content_addr`). + fn bytes_to_addr(bytes: ByteStream) -> &[U8; 32] { + store(blake3_flat(bytes)) + } + fn blake3_next_layer(layer: Layer, digest: [[U8; 4]; 8], root: G) -> (MaybeDigest, Layer) { match layer { Layer.Nil => (MaybeDigest.Some(digest), Layer.Nil), diff --git a/Ix/IxVM/Convert.lean b/Ix/IxVM/Convert.lean index b9cbd972..881ee9f2 100644 --- a/Ix/IxVM/Convert.lean +++ b/Ix/IxVM/Convert.lean @@ -53,12 +53,16 @@ def convert := ⟦ -- Universe conversion: Ixon Univ -> KLevel -- ============================================================================ - fn convert_univ(u: Univ) -> KLevel { - match u { + -- Take `&Univ` (pointer) to shrink the per-row input width — Univ is a + -- 5-variant enum, by-value passing taxes every row with the widest + -- arm's columns. Mirror the `reference_aiur_pass_pointer_not_value` + -- pattern already used for `convert_expr(e: &Expr)`. + fn convert_univ(u: &Univ) -> KLevel { + match load(u) { Univ.Zero => KLevel.Zero, - Univ.Succ(&inner) => KLevel.Succ(store(convert_univ(inner))), - Univ.Max(&a, &b) => KLevel.Max(store(convert_univ(a)), store(convert_univ(b))), - Univ.IMax(&a, &b) => KLevel.IMax(store(convert_univ(a)), store(convert_univ(b))), + Univ.Succ(inner) => KLevel.Succ(store(convert_univ(inner))), + Univ.Max(a, b) => KLevel.Max(store(convert_univ(a)), store(convert_univ(b))), + Univ.IMax(a, b) => KLevel.IMax(store(convert_univ(a)), store(convert_univ(b))), Univ.Var(idx) => KLevel.Param(flatten_u64(idx)), } } @@ -70,8 +74,8 @@ def convert := ⟦ ListNode.Cons(idx, rest) => -- universe indices are small; walk with a field index (cheap per-step -- field sub) instead of `list_lookup_u64`'s per-step U64 predecessor. - let u = load(list_lookup(univs, flatten_u64(idx))); - store(ListNode.Cons(store(convert_univ(u)), convert_univ_idxs(rest, univs))), + let u_ref = list_lookup(univs, flatten_u64(idx)); + store(ListNode.Cons(store(convert_univ(u_ref)), convert_univ_idxs(rest, univs))), } } @@ -149,8 +153,8 @@ def convert := ⟦ Expr.Srt(univ_idx) => -- field-indexed walk (see `convert_univ_idxs`): avoids the per-step -- U64 predecessor of `list_lookup_u64` on this hot universe lookup. - let u = load(list_lookup(univs, flatten_u64(univ_idx))); - store(KExprNode.Srt(store(convert_univ(u)))), + let u_ref = list_lookup(univs, flatten_u64(univ_idx)); + store(KExprNode.Srt(store(convert_univ(u_ref)))), Expr.Var(idx) => store(KExprNode.BVar(flatten_u64(idx))), @@ -208,13 +212,6 @@ def convert := ⟦ } } - fn ctx_convert_expr(e: &Expr, ctx: ConvertCtx) -> KExpr { - match ctx { - ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) => - convert_expr(e, sharing, ref_idxs, recur_idxs, lit_blobs, univs), - } - } - -- ============================================================================ -- Recursor rule conversion -- ============================================================================ @@ -233,11 +230,14 @@ def convert := ⟦ RecursorRule.Mk(nfields, rhs) => match load(rule_ctor_idxs) { ListNode.Cons(ctor_idx, rest_ctor_idxs) => - let krhs = ctx_convert_expr(rhs, ctx); - let krule = KRecRule.Mk(ctor_idx, flatten_u64(nfields), krhs); - store(ListNode.Cons( - krule, - convert_rules(rest_rules, rest_ctor_idxs, ctx))), + match ctx { + ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) => + let krhs = convert_expr(rhs, sharing, ref_idxs, recur_idxs, lit_blobs, univs); + let krule = KRecRule.Mk(ctor_idx, flatten_u64(nfields), krhs); + store(ListNode.Cons( + krule, + convert_rules(rest_rules, rest_ctor_idxs, ctx))), + }, }, }, } @@ -248,73 +248,91 @@ def convert := ⟦ -- ============================================================================ fn convert_definition(d: Definition, ctx: ConvertCtx, hint: G) -> KConstantInfo { - match d { - Definition.Mk(kind, safety, lvls, typ, value) => - let ktyp = ctx_convert_expr(typ, ctx); - let kval = ctx_convert_expr(value, ctx); - match kind { - DefKind.Definition => - KConstantInfo.Defn(flatten_u64(lvls), ktyp, kval, safety, hint), - DefKind.Opaque => - match safety { - DefinitionSafety.Unsafe => - KConstantInfo.Opaque(flatten_u64(lvls), ktyp, kval, 1), - _ => - KConstantInfo.Opaque(flatten_u64(lvls), ktyp, kval, 0), + match ctx { + ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) => + match d { + Definition.Mk(kind, safety, lvls, typ, value) => + let ktyp = convert_expr(typ, sharing, ref_idxs, recur_idxs, lit_blobs, univs); + let kval = convert_expr(value, sharing, ref_idxs, recur_idxs, lit_blobs, univs); + match kind { + DefKind.Definition => + KConstantInfo.Defn(flatten_u64(lvls), ktyp, kval, safety, hint), + DefKind.Opaque => + match safety { + DefinitionSafety.Unsafe => + KConstantInfo.Opaque(flatten_u64(lvls), ktyp, kval, 1), + _ => + KConstantInfo.Opaque(flatten_u64(lvls), ktyp, kval, 0), + }, + DefKind.Theorem => + KConstantInfo.Thm(flatten_u64(lvls), ktyp, kval), }, - DefKind.Theorem => - KConstantInfo.Thm(flatten_u64(lvls), ktyp, kval), }, } } fn convert_axiom(a: Axiom, ctx: ConvertCtx) -> KConstantInfo { - match a { - Axiom.Mk(is_unsafe, lvls, typ) => - let ktyp = ctx_convert_expr(typ, ctx); - KConstantInfo.Axiom(flatten_u64(lvls), ktyp, is_unsafe), + match ctx { + ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) => + match a { + Axiom.Mk(is_unsafe, lvls, typ) => + let ktyp = convert_expr(typ, sharing, ref_idxs, recur_idxs, lit_blobs, univs); + KConstantInfo.Axiom(flatten_u64(lvls), ktyp, is_unsafe), + }, } } fn convert_quotient(q: Quotient, ctx: ConvertCtx) -> KConstantInfo { - match q { - Quotient.Mk(kind, lvls, typ) => - let ktyp = ctx_convert_expr(typ, ctx); - KConstantInfo.Quot(flatten_u64(lvls), ktyp, kind), + match ctx { + ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) => + match q { + Quotient.Mk(kind, lvls, typ) => + let ktyp = convert_expr(typ, sharing, ref_idxs, recur_idxs, lit_blobs, univs); + KConstantInfo.Quot(flatten_u64(lvls), ktyp, kind), + }, } } fn convert_recursor(r: Recursor, ctx: ConvertCtx, rule_ctor_idxs: List‹G›, block_addr: Addr) -> KConstantInfo { - match r { - Recursor.Mk(k, is_unsafe, lvls, params, indices, motives, minors, typ, rules) => - let ktyp = ctx_convert_expr(typ, ctx); - let krules = convert_rules(rules, rule_ctor_idxs, ctx); - KConstantInfo.Rec( - flatten_u64(lvls), ktyp, flatten_u64(params), flatten_u64(indices), - flatten_u64(motives), flatten_u64(minors), - krules, k, is_unsafe, block_addr), + match ctx { + ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) => + match r { + Recursor.Mk(k, is_unsafe, lvls, params, indices, motives, minors, typ, rules) => + let ktyp = convert_expr(typ, sharing, ref_idxs, recur_idxs, lit_blobs, univs); + let krules = convert_rules(rules, rule_ctor_idxs, ctx); + KConstantInfo.Rec( + flatten_u64(lvls), ktyp, flatten_u64(params), flatten_u64(indices), + flatten_u64(motives), flatten_u64(minors), + krules, k, is_unsafe, block_addr), + }, } } fn convert_inductive(ind: Inductive, ctx: ConvertCtx, ctor_idxs: List‹G›, block_addr: Addr) -> KConstantInfo { - match ind { - Inductive.Mk(is_rec, is_refl, is_unsafe, lvls, params, indices, nested, typ, _) => - let ktyp = ctx_convert_expr(typ, ctx); - KConstantInfo.Induct( - flatten_u64(lvls), ktyp, flatten_u64(params), flatten_u64(indices), - ctor_idxs, is_rec, is_refl, is_unsafe, flatten_u64(nested), block_addr), + match ctx { + ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) => + match ind { + Inductive.Mk(is_rec, is_refl, is_unsafe, lvls, params, indices, nested, typ, _) => + let ktyp = convert_expr(typ, sharing, ref_idxs, recur_idxs, lit_blobs, univs); + KConstantInfo.Induct( + flatten_u64(lvls), ktyp, flatten_u64(params), flatten_u64(indices), + ctor_idxs, is_rec, is_refl, is_unsafe, flatten_u64(nested), block_addr), + }, } } fn convert_constructor(c: Constructor, ctx: ConvertCtx, induct_idx: G) -> KConstantInfo { - match c { - Constructor.Mk(is_unsafe, lvls, cidx, params, fields, typ) => - let ktyp = ctx_convert_expr(typ, ctx); - KConstantInfo.Ctor( - flatten_u64(lvls), ktyp, induct_idx, flatten_u64(cidx), - flatten_u64(params), flatten_u64(fields), is_unsafe), + match ctx { + ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs) => + match c { + Constructor.Mk(is_unsafe, lvls, cidx, params, fields, typ) => + let ktyp = convert_expr(typ, sharing, ref_idxs, recur_idxs, lit_blobs, univs); + KConstantInfo.Ctor( + flatten_u64(lvls), ktyp, induct_idx, flatten_u64(cidx), + flatten_u64(params), flatten_u64(fields), is_unsafe), + }, } } @@ -322,9 +340,11 @@ def convert := ⟦ -- Top-level conversion -- ============================================================================ - -- Convert a single resolved input to a KConstantInfo - fn convert_one(input: ConvertInput) -> KConstantInfo { - match input { + -- Convert a single resolved input to a KConstantInfo. Takes &ConvertInput + -- (pointer) so the per-row input width is one G column, not the full + -- ConvertInput union width. + fn convert_one(input: &ConvertInput) -> KConstantInfo { + match load(input) { ConvertInput.Mk(ctx, kind) => match kind { ConvertKind.CKDefn(d, hint) => convert_definition(d, ctx, hint), @@ -342,7 +362,7 @@ def convert := ⟦ fn convert_all(inputs: List‹&ConvertInput›) -> List‹&KConstantInfo› { match load(inputs) { ListNode.Nil => store(ListNode.Nil), - ListNode.Cons(&input, rest) => + ListNode.Cons(input, rest) => let ci = convert_one(input); store(ListNode.Cons(store(ci), convert_all(rest))), } diff --git a/Ix/IxVM/Ingress.lean b/Ix/IxVM/Ingress.lean index 56987ed7..32854a8a 100644 --- a/Ix/IxVM/Ingress.lean +++ b/Ix/IxVM/Ingress.lean @@ -7,25 +7,33 @@ public section namespace IxVM def ingress := ⟦ + -- IOBuffer channel identifiers. See `ClaimHarness.lean` for the host-side + -- counterpart that seeds these channels. + fn ch_const() -> G { 0 } + fn ch_blob() -> G { 1 } + fn ch_hint() -> G { 2 } + + -- Read the raw bytes the prover seeded at `key` on `channel`. + -- Channels and keys are documented per call site; the helper exists + -- only to centralise the `io_get_info` + `#read_byte_stream` pair. + fn load_payload_const(key: [U8; 32]) -> ByteStream { + let (idx, len) = io_get_info(0, key); + #read_byte_stream(0, idx, len) + } + fn load_payload_blob(key: [U8; 32]) -> ByteStream { + let (idx, len) = io_get_info(1, key); + #read_byte_stream(1, idx, len) + } + fn load_payload_hint(key: [U8; 32]) -> ByteStream { + let (idx, len) = io_get_info(2, key); + #read_byte_stream(2, idx, len) + } + -- Load a constant from IOBuffer by address, verify blake3, deserialize. fn load_verified_constant(addr: Addr) -> Constant { let raw = load(addr); - let (idx, len) = io_get_info(0, raw); - let bytes = #read_byte_stream(0, idx, len); - let h = blake3(bytes); - assert_eq!( - [ - h[0][0], h[0][1], h[0][2], h[0][3], - h[1][0], h[1][1], h[1][2], h[1][3], - h[2][0], h[2][1], h[2][2], h[2][3], - h[3][0], h[3][1], h[3][2], h[3][3], - h[4][0], h[4][1], h[4][2], h[4][3], - h[5][0], h[5][1], h[5][2], h[5][3], - h[6][0], h[6][1], h[6][2], h[6][3], - h[7][0], h[7][1], h[7][2], h[7][3] - ], - raw - ); + let bytes = load_payload_const(raw); + let _ = verify_bytes_against(bytes, raw); let (constant, rest) = get_constant(bytes); assert_eq!(load(rest), ListNode.Nil); constant @@ -34,22 +42,9 @@ def ingress := ⟦ -- Load a blob from IOBuffer by address, verify blake3, return raw bytes. -- Blobs live on channel 1; constants live on channel 0 with the same key. fn load_verified_blob(addr: Addr) -> ByteStream { - let (idx, len) = io_get_info(1, load(addr)); - let bytes = #read_byte_stream(1, idx, len); - let h = blake3(bytes); - assert_eq!( - [ - h[0][0], h[0][1], h[0][2], h[0][3], - h[1][0], h[1][1], h[1][2], h[1][3], - h[2][0], h[2][1], h[2][2], h[2][3], - h[3][0], h[3][1], h[3][2], h[3][3], - h[4][0], h[4][1], h[4][2], h[4][3], - h[5][0], h[5][1], h[5][2], h[5][3], - h[6][0], h[6][1], h[6][2], h[6][3], - h[7][0], h[7][1], h[7][2], h[7][3] - ], - load(addr) - ); + let raw = load(addr); + let bytes = load_payload_blob(raw); + let _ = verify_bytes_against(bytes, raw); bytes } @@ -112,44 +107,16 @@ def ingress := ⟦ -- Caller MUST only invoke this for Defn addrs; the harness only seeds -- channel 2 for defns. A missing key aborts execution (correct). fn load_constant_hint(addr: Addr) -> G { - let (idx, len) = io_get_info(2, load(addr)); - let bytes = #read_byte_stream(2, idx, len); + let bytes = load_payload_hint(load(addr)); match load(bytes) { ListNode.Cons(b, _) => to_field(b), } } - -- Build lit_blobs by loading and verifying each blob on demand. - -- A ref is a blob if it's not in all_addrs (the constant address list). - -- For constant refs, returns an empty ByteStream (never read by conversion). - fn build_lit_blobs(refs: List‹Addr›, addr_pos_map: &RBTreeMap‹G›) -> List‹ByteStream› { - match load(refs) { - ListNode.Nil => store(ListNode.Nil), - ListNode.Cons(addr, rest) => - let blob = is_blob(addr, addr_pos_map); - match blob { - 1 => - let bs = load_verified_blob(addr); - store(ListNode.Cons(bs, build_lit_blobs(rest, addr_pos_map))), - 0 => - store(ListNode.Cons(store(ListNode.Nil), build_lit_blobs(rest, addr_pos_map))), - }, - } - } - - -- Check if an address is a blob via the augmented `addr_pos_map`: - -- value == 0 (absent) → conservatively blob (the historical semantics; - -- sound because a content-bound blob load downstream re-verifies); - -- value == 4294967295 (SENTINEL) → known blob ref; - -- value > 0 and < SENTINEL (pos+1) → known const. - fn is_blob(addr: Addr, addr_pos_map: &RBTreeMap‹G›) -> G { - let hit = rbtree_map_lookup_or_default(ptr_val(addr), load(addr_pos_map), 0); - match hit { - 0 => 1, - 4294967295 => 1, - _ => 0, - } - } + -- Sentinel value stored in `addr_pos_map` for addresses known to be + -- blob refs (not constants). Beyond any honest `pos+1` so it cannot + -- collide with a real const-position encoding. + fn sentinel_blob_ref() -> G { 4294967295 } -- Extract the Muts block address from a projection ConstantInfo. -- Returns [0; 32] for non-projection constants. @@ -301,7 +268,7 @@ def ingress := ⟦ } } - -- Walk all constants' `refs`. For every ref whose ptr_val is NOT +-- Walk all constants' `refs`. For every ref whose ptr_val is NOT -- already mapped to a const-position (= a true const-ref), insert it -- with the BLOB sentinel `4294967295`. Result: every ref a const -- carries is classified at build time; `lookup_addr_pos` short-circuits @@ -332,7 +299,7 @@ def ingress := ⟦ match hit { 0 => -- Not yet registered: classify as blob ref via SENTINEL. - insert_refs_as_blobs(rest, rbtree_map_insert(key, 4294967295, m)), + insert_refs_as_blobs(rest, rbtree_map_insert(key, sentinel_blob_ref(), m)), _ => -- Already a const (pos+1) or already a blob (SENTINEL): leave alone. insert_refs_as_blobs(rest, m), @@ -340,22 +307,32 @@ def ingress := ⟦ } } - -- Find the start position of a block by its block address. - fn lookup_block_start(target: Addr, block_addrs: List‹Addr›, block_starts: List‹G›) -> G { +-- Index `block_addrs`/`block_starts` into a single ptr_val-keyed rbtree so + -- the per-call lookup is O(log N) instead of an O(N) parallel-list walk. + -- ptr_val keying is sound by Aiur Store content-addressing. + fn build_block_start_map(block_addrs: List‹Addr›, block_starts: List‹G›) -> RBTreeMap‹G› { + build_block_start_map_walk(block_addrs, block_starts, RBTreeMap.Nil) + } + + fn build_block_start_map_walk(block_addrs: List‹Addr›, block_starts: List‹G›, + acc: RBTreeMap‹G›) -> RBTreeMap‹G› { match load(block_addrs) { - ListNode.Nil => 0, + ListNode.Nil => acc, ListNode.Cons(addr, rest_addrs) => match load(block_starts) { ListNode.Cons(start, rest_starts) => - let eq = address_eq(target, addr); - match eq { - 1 => start, - 0 => lookup_block_start(target, rest_addrs, rest_starts), - }, + build_block_start_map_walk(rest_addrs, rest_starts, + rbtree_map_insert(ptr_val(addr), start, acc)), }, } } + -- O(log N) block-start probe. Returns 0 when the address isn't a known + -- block (mirrors the historical "not found → 0" semantics). + fn lookup_block_start(target: Addr, block_start_map: &RBTreeMap‹G›) -> G { + rbtree_map_lookup_or_default(ptr_val(target), load(block_start_map), 0) + } + -- ============================================================================ -- Layout pass: compute block start positions and total kernel size -- ============================================================================ @@ -522,19 +499,17 @@ def ingress := ⟦ fn build_pos_map( consts: List‹&Constant›, addrs: List‹Addr›, - block_addrs: List‹Addr›, - block_starts: List‹G›, + block_start_map: &RBTreeMap‹G›, pos: G ) -> List‹G› { - build_pos_map_walk(consts, addrs, block_addrs, block_starts, pos, + build_pos_map_walk(consts, addrs, block_start_map, pos, store(ListNode.Nil), store(ListNode.Nil)) } fn build_pos_map_walk( consts: List‹&Constant›, addrs: List‹Addr›, - block_addrs: List‹Addr›, - block_starts: List‹G›, + block_start_map: &RBTreeMap‹G›, pos: G, seen_mptrs: List‹G›, seen_poses: List‹G› @@ -557,7 +532,7 @@ def ingress := ⟦ 1 => let first_pos = first_pos_for_mptr(mptr, seen_mptrs, seen_poses); store(ListNode.Cons(first_pos, - build_pos_map_walk(rest_consts, rest_addrs, block_addrs, block_starts, pos, seen_mptrs, seen_poses))), + build_pos_map_walk(rest_consts, rest_addrs, block_start_map, pos, seen_mptrs, seen_poses))), 0 => let size = block_kernel_size(members); let new_seen_m = match mptr { @@ -569,12 +544,12 @@ def ingress := ⟦ _ => store(ListNode.Cons(pos, seen_poses)), }; store(ListNode.Cons(pos, - build_pos_map_walk(rest_consts, rest_addrs, block_addrs, block_starts, pos + size, new_seen_m, new_seen_p))), + build_pos_map_walk(rest_consts, rest_addrs, block_start_map, pos + size, new_seen_m, new_seen_p))), }, ConstantInfo.IPrj(prj) => match prj { InductiveProj.Mk(idx, block_addr) => - let block_start = lookup_block_start(block_addr, block_addrs, block_starts); + let block_start = lookup_block_start(block_addr, block_start_map); let block_const = load_verified_constant(block_addr); match block_const { Constant.Mk(block_info, _, _, _) => @@ -582,14 +557,14 @@ def ingress := ⟦ ConstantInfo.Muts(members) => let off = member_offset(members, flatten_u64(idx)); store(ListNode.Cons(block_start + off, - build_pos_map_walk(rest_consts, rest_addrs, block_addrs, block_starts, pos, seen_mptrs, seen_poses))), + build_pos_map_walk(rest_consts, rest_addrs, block_start_map, pos, seen_mptrs, seen_poses))), }, }, }, ConstantInfo.CPrj(prj) => match prj { ConstructorProj.Mk(idx, cidx, block_addr) => - let block_start = lookup_block_start(block_addr, block_addrs, block_starts); + let block_start = lookup_block_start(block_addr, block_start_map); let block_const = load_verified_constant(block_addr); match block_const { Constant.Mk(block_info, _, _, _) => @@ -597,14 +572,14 @@ def ingress := ⟦ ConstantInfo.Muts(members) => let mem_off = member_offset(members, flatten_u64(idx)); store(ListNode.Cons(block_start + mem_off + 1 + flatten_u64(cidx), - build_pos_map_walk(rest_consts, rest_addrs, block_addrs, block_starts, pos, seen_mptrs, seen_poses))), + build_pos_map_walk(rest_consts, rest_addrs, block_start_map, pos, seen_mptrs, seen_poses))), }, }, }, ConstantInfo.RPrj(prj) => match prj { RecursorProj.Mk(idx, block_addr) => - let block_start = lookup_block_start(block_addr, block_addrs, block_starts); + let block_start = lookup_block_start(block_addr, block_start_map); let block_const = load_verified_constant(block_addr); match block_const { Constant.Mk(block_info, _, _, _) => @@ -612,14 +587,14 @@ def ingress := ⟦ ConstantInfo.Muts(members) => let off = member_offset(members, flatten_u64(idx)); store(ListNode.Cons(block_start + off, - build_pos_map_walk(rest_consts, rest_addrs, block_addrs, block_starts, pos, seen_mptrs, seen_poses))), + build_pos_map_walk(rest_consts, rest_addrs, block_start_map, pos, seen_mptrs, seen_poses))), }, }, }, ConstantInfo.DPrj(prj) => match prj { DefinitionProj.Mk(idx, block_addr) => - let block_start = lookup_block_start(block_addr, block_addrs, block_starts); + let block_start = lookup_block_start(block_addr, block_start_map); let block_const = load_verified_constant(block_addr); match block_const { Constant.Mk(block_info, _, _, _) => @@ -627,13 +602,13 @@ def ingress := ⟦ ConstantInfo.Muts(members) => let off = member_offset(members, flatten_u64(idx)); store(ListNode.Cons(block_start + off, - build_pos_map_walk(rest_consts, rest_addrs, block_addrs, block_starts, pos, seen_mptrs, seen_poses))), + build_pos_map_walk(rest_consts, rest_addrs, block_start_map, pos, seen_mptrs, seen_poses))), }, }, }, _ => store(ListNode.Cons(pos, - build_pos_map_walk(rest_consts, rest_addrs, block_addrs, block_starts, pos + 1, seen_mptrs, seen_poses))), + build_pos_map_walk(rest_consts, rest_addrs, block_start_map, pos + 1, seen_mptrs, seen_poses))), }, }, }, @@ -644,13 +619,35 @@ def ingress := ⟦ -- Ref index building using position map -- ============================================================================ - fn build_ref_idxs_mapped(refs: List‹Addr›, addr_pos_map: &RBTreeMap‹G›, - all_addrs: List‹Addr›, pos_map: List‹G›) -> List‹G› { + -- Fused walk of `refs` producing both `ref_idxs` and `lit_blobs` in one + -- pass. Each ref goes through ONE rbtree probe (`addr_pos_map`) and the + -- result is interpreted as both classifications: + -- * hit == 0 (absent — de-intern soundness floor): fall back to linear + -- scan for `ref_idx`, leave `lit_blob` empty (the conservative path). + -- * hit == SENTINEL_BLOB_REF: known blob → load + decode; idx = 0. + -- * hit == pos + 1: known const → idx = pos, blob slot empty. + fn build_ref_idxs_and_blobs(refs: List‹Addr›, addr_pos_map: &RBTreeMap‹G›, + all_addrs: List‹Addr›, pos_map: List‹G›) + -> (List‹G›, List‹ByteStream›) { match load(refs) { - ListNode.Nil => store(ListNode.Nil), + ListNode.Nil => (store(ListNode.Nil), store(ListNode.Nil)), ListNode.Cons(addr, rest) => - let pos = lookup_addr_pos(addr, addr_pos_map, all_addrs, pos_map); - store(ListNode.Cons(pos, build_ref_idxs_mapped(rest, addr_pos_map, all_addrs, pos_map))), + let (rest_idxs, rest_blobs) = + build_ref_idxs_and_blobs(rest, addr_pos_map, all_addrs, pos_map); + let hit = rbtree_map_lookup_or_default(ptr_val(addr), load(addr_pos_map), 0); + match hit { + 0 => + let pos = lookup_addr_pos_linear(addr, all_addrs, pos_map); + (store(ListNode.Cons(pos, rest_idxs)), + store(ListNode.Cons(store(ListNode.Nil), rest_blobs))), + 4294967295 => + let bs = load_verified_blob(addr); + (store(ListNode.Cons(0, rest_idxs)), + store(ListNode.Cons(bs, rest_blobs))), + _ => + (store(ListNode.Cons(hit - 1, rest_idxs)), + store(ListNode.Cons(store(ListNode.Nil), rest_blobs))), + }, } } @@ -751,49 +748,51 @@ def ingress := ⟦ } } - fn canonicalize_addr_map_walk(addrs: List‹Addr›, consts: List‹&Constant›, - seen_mptrs: List‹G›, - seen_addrs: List‹Addr›) -> List‹Addr› { + -- Produce an `Addr → canon_Addr` rbtree keyed by `ptr_val(addr)`. Only + -- members of a Muts wrapper that dedupes to an earlier canonical addr + -- contribute non-trivial entries; non-Muts and primary-wrapper consts + -- map to themselves (and we skip those — `lookup_canon_addr` falls back + -- to the target unchanged on miss). + -- + -- ptr_val keying is sound because Aiur Store content-addresses every + -- pointer: a positive ptr_val match implies content equality. A miss + -- conservatively returns the target (the existing semantics for + -- non-deduped addresses). + fn build_canon_addr_map_walk(addrs: List‹Addr›, consts: List‹&Constant›, + seen_mptrs: List‹G›, + seen_addrs: List‹Addr›, + acc: RBTreeMap‹Addr›) -> RBTreeMap‹Addr› { match load(addrs) { - ListNode.Nil => store(ListNode.Nil), + ListNode.Nil => acc, ListNode.Cons(addr, rest_a) => match load(consts) { ListNode.Cons(c, rest_c) => let mptr = extract_muts_members_ptr(c); - let canon_addr = match mptr { - 0 => addr, - _ => find_canon_addr_for_mptr(mptr, seen_mptrs, seen_addrs, addr), - }; - let new_seen_mptrs = match mptr { - 0 => seen_mptrs, - _ => store(ListNode.Cons(mptr, seen_mptrs)), - }; - let new_seen_addrs = match mptr { - 0 => seen_addrs, - _ => store(ListNode.Cons(canon_addr, seen_addrs)), - }; - store(ListNode.Cons(canon_addr, - canonicalize_addr_map_walk(rest_a, rest_c, new_seen_mptrs, new_seen_addrs))), + match mptr { + 0 => build_canon_addr_map_walk(rest_a, rest_c, seen_mptrs, seen_addrs, acc), + _ => + let canon_addr = find_canon_addr_for_mptr(mptr, seen_mptrs, seen_addrs, addr); + let new_seen_mptrs = store(ListNode.Cons(mptr, seen_mptrs)); + let new_seen_addrs = store(ListNode.Cons(canon_addr, seen_addrs)); + let new_acc = rbtree_map_insert(ptr_val(addr), canon_addr, acc); + build_canon_addr_map_walk(rest_a, rest_c, new_seen_mptrs, new_seen_addrs, new_acc), + }, }, } } - fn canonicalize_addr_map(addrs: List‹Addr›, consts: List‹&Constant›) -> List‹Addr› { - canonicalize_addr_map_walk(addrs, consts, store(ListNode.Nil), store(ListNode.Nil)) + fn build_canon_addr_map(addrs: List‹Addr›, consts: List‹&Constant›) -> RBTreeMap‹Addr› { + build_canon_addr_map_walk(addrs, consts, store(ListNode.Nil), store(ListNode.Nil), RBTreeMap.Nil) } - fn lookup_canon_addr(target: Addr, all_addrs: List‹Addr›, - canon_addrs: List‹Addr›) -> Addr { - match load(all_addrs) { - ListNode.Nil => target, - ListNode.Cons(addr, rest_a) => - match load(canon_addrs) { - ListNode.Cons(canon, rest_c) => - match address_eq(target, addr) { - 1 => canon, - 0 => lookup_canon_addr(target, rest_a, rest_c), - }, - }, + -- O(log N) canon-addr probe. Miss returns target unchanged (the + -- non-deduped case is the common one). + fn lookup_canon_addr(target: Addr, canon_addr_map: &RBTreeMap‹Addr›) -> Addr { + match load(canon_addr_map) { + RBTreeMap.Nil => target, + _ => + let hit = rbtree_map_lookup_or_default(ptr_val(target), load(canon_addr_map), target); + hit, } } @@ -919,14 +918,18 @@ def ingress := ⟦ -- block by extracting the inductive's address from the recursor's typ -- (rather than heuristically matching ctor counts among refs, which fails -- when multiple in-scope inductives share the same number of ctors). + -- Returns `(rule_ctor_idxs, block_addr)`. The standalone-Recr caller + -- needs the block_addr to wrap the CKRecr input; the Muts-block caller + -- already has block_addr in scope and discards the second component. + -- Computing both together saves the standalone caller a redundant + -- `rec_typ_to_inductive_addr` + `load_verified_constant` chain. fn build_aux_recr_ctor_idxs( recr: Recursor, refs: List‹Addr›, sharing: List‹&Expr›, all_addrs: List‹Addr›, - block_addrs: List‹Addr›, - block_starts: List‹G› - ) -> List‹G› { + block_start_map: &RBTreeMap‹G› + ) -> (List‹G›, Addr) { match recr { Recursor.Mk(_, _, _, params, indices, motives, minors, &typ, _) => let n_skip = ((flatten_u64(params) + flatten_u64(motives)) @@ -944,12 +947,13 @@ def ingress := ⟦ Constant.Mk(bi, _, _, _) => match bi { ConstantInfo.Muts(other_members) => - let bs = lookup_block_start(block_addr, block_addrs, block_starts); + let bs = lookup_block_start(block_addr, block_start_map); -- Mutual block: each recursor's rules cover only -- its OWN inductive's ctors. Slice the global -- rule_ctor_idxs to just this member's ctors. - extract_member_ctor_idxs(other_members, bs, - flatten_u64(member_idx)), + let idxs = extract_member_ctor_idxs(other_members, bs, + flatten_u64(member_idx)); + (idxs, block_addr), }, }, }, @@ -998,8 +1002,7 @@ def ingress := ⟦ member_idx: G, refs: List‹Addr›, all_addrs: List‹Addr›, - block_addrs: List‹Addr›, - block_starts: List‹G›, + block_start_map: &RBTreeMap‹G›, block_addr: Addr ) -> List‹&ConvertInput› { match mc { @@ -1021,8 +1024,8 @@ def ingress := ⟦ store(ListNode.Cons(store(input), store(ListNode.Nil))), 0 => let sharing = match ctx { ConvertCtx.Mk(s, _, _, _, _) => s, }; - let rule_ctor_idxs = - build_aux_recr_ctor_idxs(recr, refs, sharing, all_addrs, block_addrs, block_starts); + let (rule_ctor_idxs, _) = + build_aux_recr_ctor_idxs(recr, refs, sharing, all_addrs, block_start_map); let input = ConvertInput.Mk(ctx, ConvertKind.CKRecr(recr, rule_ctor_idxs, block_addr)); store(ListNode.Cons(store(input), store(ListNode.Nil))), }, @@ -1052,17 +1055,16 @@ def ingress := ⟦ member_idx: G, refs: List‹Addr›, all_addrs: List‹Addr›, - block_addrs: List‹Addr›, - block_starts: List‹G›, + block_start_map: &RBTreeMap‹G›, block_addr: Addr ) -> List‹&ConvertInput› { match load(members) { ListNode.Nil => store(ListNode.Nil), ListNode.Cons(mc, rest) => let this = expand_member(mc, ctx, all_members, block_start, member_idx, - refs, all_addrs, block_addrs, block_starts, block_addr); + refs, all_addrs, block_start_map, block_addr); let more = expand_members(rest, ctx, all_members, block_start, member_idx + 1, - refs, all_addrs, block_addrs, block_starts, block_addr); + refs, all_addrs, block_start_map, block_addr); list_concat(this, more), } } @@ -1083,9 +1085,8 @@ def ingress := ⟦ cur_addrs: List‹Addr›, all_addrs: List‹Addr›, pos_map: List‹G›, - canon_addrs: List‹Addr›, - block_addrs: List‹Addr›, - block_starts: List‹G›, + canon_addr_map: &RBTreeMap‹Addr›, + block_start_map: &RBTreeMap‹G›, pos: G ) -> List‹&ConvertInput› { -- Built once here; threaded as the fast-path index for `lookup_addr_pos`. @@ -1093,10 +1094,12 @@ def ingress := ⟦ -- then walks every const's `refs` and tags every previously-unregistered -- ref with the BLOB sentinel (4294967295), so blob-ref lookups -- short-circuit instead of falling through to the O(N) linear scan. + -- A fused single-pass version was tried and lost — Aiur's per-row width + -- tax made the merged fn more expensive than two narrower passes. let base_map = build_addr_pos_map(all_addrs, pos_map); let addr_pos_map = store(augment_with_blob_refs(consts, base_map)); build_convert_inputs_walk(consts, cur_addrs, all_addrs, addr_pos_map, pos_map, - canon_addrs, block_addrs, block_starts, pos, + canon_addr_map, block_start_map, pos, store(ListNode.Nil)) } @@ -1106,9 +1109,8 @@ def ingress := ⟦ all_addrs: List‹Addr›, addr_pos_map: &RBTreeMap‹G›, pos_map: List‹G›, - canon_addrs: List‹Addr›, - block_addrs: List‹Addr›, - block_starts: List‹G›, + canon_addr_map: &RBTreeMap‹Addr›, + block_start_map: &RBTreeMap‹G›, pos: G, seen_mptrs: List‹G› ) -> List‹&ConvertInput› { @@ -1132,7 +1134,7 @@ def ingress := ⟦ -- emitted). Don't advance pos. Refs to this wrapper -- resolve to canonical pos via pos_map dedup. build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_pos_map, pos_map, - canon_addrs, block_addrs, block_starts, pos, seen_mptrs), + canon_addr_map, block_start_map, pos, seen_mptrs), 0 => let new_seen = match mptr { 0 => seen_mptrs, @@ -1140,81 +1142,63 @@ def ingress := ⟦ }; let size = block_kernel_size(members); let canon_block_start = lookup_addr_pos(head_addr, addr_pos_map, all_addrs, pos_map); - let canon_addr = lookup_canon_addr(head_addr, all_addrs, canon_addrs); - let ref_idxs = build_ref_idxs_mapped(refs, addr_pos_map, all_addrs, pos_map); - let lit_blobs = build_lit_blobs(refs, addr_pos_map); + let canon_addr = lookup_canon_addr(head_addr, canon_addr_map); + let (ref_idxs, lit_blobs) = + build_ref_idxs_and_blobs(refs, addr_pos_map, all_addrs, pos_map); let recur_idxs = build_recur_idxs(members, canon_block_start, 0); let ctx = ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs); let expanded = expand_members(members, ctx, members, canon_block_start, 0, - refs, all_addrs, block_addrs, block_starts, canon_addr); + refs, all_addrs, block_start_map, canon_addr); let more = build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_pos_map, pos_map, - canon_addrs, block_addrs, block_starts, pos + size, new_seen); + canon_addr_map, block_start_map, pos + size, new_seen); list_concat(expanded, more), }, ConstantInfo.IPrj(_) => - build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_pos_map, pos_map, canon_addrs, block_addrs, block_starts, pos, seen_mptrs), + build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_pos_map, pos_map, canon_addr_map, block_start_map, pos, seen_mptrs), ConstantInfo.CPrj(_) => - build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_pos_map, pos_map, canon_addrs, block_addrs, block_starts, pos, seen_mptrs), + build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_pos_map, pos_map, canon_addr_map, block_start_map, pos, seen_mptrs), ConstantInfo.RPrj(_) => - build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_pos_map, pos_map, canon_addrs, block_addrs, block_starts, pos, seen_mptrs), + build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_pos_map, pos_map, canon_addr_map, block_start_map, pos, seen_mptrs), ConstantInfo.DPrj(_) => - build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_pos_map, pos_map, canon_addrs, block_addrs, block_starts, pos, seen_mptrs), + build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_pos_map, pos_map, canon_addr_map, block_start_map, pos, seen_mptrs), ConstantInfo.Defn(defn) => - let ref_idxs = build_ref_idxs_mapped(refs, addr_pos_map, all_addrs, pos_map); - let lit_blobs = build_lit_blobs(refs, addr_pos_map); + let (ref_idxs, lit_blobs) = + build_ref_idxs_and_blobs(refs, addr_pos_map, all_addrs, pos_map); let recur_idxs = store(ListNode.Cons(pos, store(ListNode.Nil))); let ctx = ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs); let hint = #load_constant_hint(head_addr); let input = ConvertInput.Mk(ctx, ConvertKind.CKDefn(defn, hint)); store(ListNode.Cons(store(input), - build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_pos_map, pos_map, canon_addrs, block_addrs, block_starts, pos + 1, seen_mptrs))), + build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_pos_map, pos_map, canon_addr_map, block_start_map, pos + 1, seen_mptrs))), ConstantInfo.Axio(axio) => - let ref_idxs = build_ref_idxs_mapped(refs, addr_pos_map, all_addrs, pos_map); - let lit_blobs = build_lit_blobs(refs, addr_pos_map); + let (ref_idxs, lit_blobs) = + build_ref_idxs_and_blobs(refs, addr_pos_map, all_addrs, pos_map); let ctx = ConvertCtx.Mk(sharing, ref_idxs, store(ListNode.Nil), lit_blobs, univs); let input = ConvertInput.Mk(ctx, ConvertKind.CKAxio(axio)); store(ListNode.Cons(store(input), - build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_pos_map, pos_map, canon_addrs, block_addrs, block_starts, pos + 1, seen_mptrs))), + build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_pos_map, pos_map, canon_addr_map, block_start_map, pos + 1, seen_mptrs))), ConstantInfo.Quot(quot) => - let ref_idxs = build_ref_idxs_mapped(refs, addr_pos_map, all_addrs, pos_map); - let lit_blobs = build_lit_blobs(refs, addr_pos_map); + let (ref_idxs, lit_blobs) = + build_ref_idxs_and_blobs(refs, addr_pos_map, all_addrs, pos_map); let ctx = ConvertCtx.Mk(sharing, ref_idxs, store(ListNode.Nil), lit_blobs, univs); let input = ConvertInput.Mk(ctx, ConvertKind.CKQuot(quot)); store(ListNode.Cons(store(input), - build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_pos_map, pos_map, canon_addrs, block_addrs, block_starts, pos + 1, seen_mptrs))), + build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_pos_map, pos_map, canon_addr_map, block_start_map, pos + 1, seen_mptrs))), ConstantInfo.Recr(recr) => - let ref_idxs = build_ref_idxs_mapped(refs, addr_pos_map, all_addrs, pos_map); - let lit_blobs = build_lit_blobs(refs, addr_pos_map); - -- Resolve the recursor's inductive via typ-based lookup: - -- peel n_skip foralls of `recr.typ` to reach the major's - -- type, take its head, lookup `refs[head_ref_idx]`. The - -- ctor-count heuristic in `find_matching_block_addr` picks - -- the wrong block when multiple in-scope inductives share - -- the same ctor count. - let rule_ctor_idxs = build_aux_recr_ctor_idxs( - recr, refs, sharing, all_addrs, block_addrs, block_starts); - let n_skip = match recr { - Recursor.Mk(_, _, _, params, indices, motives, minors, _, _) => - ((flatten_u64(params) + flatten_u64(motives)) - + flatten_u64(minors)) + flatten_u64(indices), - }; - let typ = match recr { - Recursor.Mk(_, _, _, _, _, _, _, &typ, _) => typ, - }; - let ind_addr = rec_typ_to_inductive_addr(typ, n_skip, refs, sharing); - let ind_const = load_verified_constant(ind_addr); - let block_addr = match ind_const { - Constant.Mk(info, _, _, _) => - match info { - ConstantInfo.IPrj(prj) => - match prj { InductiveProj.Mk(_, ba) => ba, }, - }, - }; + let (ref_idxs, lit_blobs) = + build_ref_idxs_and_blobs(refs, addr_pos_map, all_addrs, pos_map); + -- `build_aux_recr_ctor_idxs` already does the typ-peel + + -- IPrj lookup to find the recursor's inductive block; + -- get block_addr from the same call instead of redoing + -- the `rec_typ_to_inductive_addr` + `load_verified_constant` + -- chain. + let (rule_ctor_idxs, block_addr) = build_aux_recr_ctor_idxs( + recr, refs, sharing, all_addrs, block_start_map); let recur_idxs = store(ListNode.Cons(pos, store(ListNode.Nil))); let ctx = ConvertCtx.Mk(sharing, ref_idxs, recur_idxs, lit_blobs, univs); let input = ConvertInput.Mk(ctx, ConvertKind.CKRecr(recr, rule_ctor_idxs, block_addr)); store(ListNode.Cons(store(input), - build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_pos_map, pos_map, canon_addrs, block_addrs, block_starts, pos + 1, seen_mptrs))), + build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_pos_map, pos_map, canon_addr_map, block_start_map, pos + 1, seen_mptrs))), }, }, }, @@ -1225,19 +1209,6 @@ def ingress := ⟦ -- Loading and dependency tracking -- ============================================================================ - -- Check if an address is already in a list - fn address_in_list(addr: Addr, list: List‹Addr›) -> G { - match load(list) { - ListNode.Nil => 0, - ListNode.Cons(a, rest) => - let eq = address_eq(addr, a); - match eq { - 1 => 1, - 0 => address_in_list(addr, rest), - }, - } - } - -- Recursively load constants and their transitive dependencies. -- Processes one address at a time from a worklist, deduplicating by -- checking the visited set. Blob addresses are detected via io_get_info: @@ -1312,10 +1283,11 @@ def ingress := ⟦ let (all_addrs, all_consts) = load_with_deps( target_addr, store(ListNode.Nil), store(ListNode.Nil), store(ListNode.Nil), RBTreeMap.Nil); let (block_addrs, block_starts, _total) = compute_layout(all_consts, all_addrs, 0); - let pos_map_naive = build_pos_map(all_consts, all_addrs, block_addrs, block_starts, 0); + let block_start_map = store(build_block_start_map(block_addrs, block_starts)); + let pos_map_naive = build_pos_map(all_consts, all_addrs, block_start_map, 0); let pos_map = canonicalize_pos_map(all_consts, pos_map_naive); - let canon_addrs = canonicalize_addr_map(all_addrs, all_consts); - let inputs = build_convert_inputs(all_consts, all_addrs, all_addrs, pos_map, canon_addrs, block_addrs, block_starts, 0); + let canon_addr_map = store(build_canon_addr_map(all_addrs, all_consts)); + let inputs = build_convert_inputs(all_consts, all_addrs, all_addrs, pos_map, canon_addr_map, block_start_map, 0); convert_all(inputs) } @@ -1493,7 +1465,7 @@ def ingress := ⟦ -- result or a deterministic loop counter, so the resulting addresses -- are derived from already-trusted data. fn build_ctor_overrides(all_consts: List‹&Constant›, all_addrs: List‹Addr›, - block_addrs: List‹Addr›, block_starts: List‹G›) + block_start_map: &RBTreeMap‹G›) -> List‹(G, Addr)› { match load(all_consts) { ListNode.Nil => store(ListNode.Nil), @@ -1506,7 +1478,7 @@ def ingress := ⟦ ConstantInfo.IPrj(prj) => match prj { InductiveProj.Mk(idx, block_addr) => - let block_start = lookup_block_start(block_addr, block_addrs, block_starts); + let block_start = lookup_block_start(block_addr, block_start_map); let block_const = load_verified_constant(block_addr); match block_const { Constant.Mk(bi, _, _, _) => @@ -1517,14 +1489,14 @@ def ingress := ⟦ let n_ctors = inductive_ctor_count_at(members, flatten_u64(idx)); let new_pairs = build_ctor_pairs_computed(idx, block_addr, base_pos, n_ctors, 0); list_concat(new_pairs, - build_ctor_overrides(rest_c, rest_a, block_addrs, block_starts)), + build_ctor_overrides(rest_c, rest_a, block_start_map)), _ => - build_ctor_overrides(rest_c, rest_a, block_addrs, block_starts), + build_ctor_overrides(rest_c, rest_a, block_start_map), }, }, }, _ => - build_ctor_overrides(rest_c, rest_a, block_addrs, block_starts), + build_ctor_overrides(rest_c, rest_a, block_start_map), }, }, }, @@ -1580,47 +1552,9 @@ def ingress := ⟦ store(ListNode.Nil), store(ListNode.Nil)); let bytes = put_constant(cnst, store(ListNode.Nil)); - let h = blake3(bytes); - store([h[0][0], h[0][1], h[0][2], h[0][3], - h[1][0], h[1][1], h[1][2], h[1][3], - h[2][0], h[2][1], h[2][2], h[2][3], - h[3][0], h[3][1], h[3][2], h[3][3], - h[4][0], h[4][1], h[4][2], h[4][3], - h[5][0], h[5][1], h[5][2], h[5][3], - h[6][0], h[6][1], h[6][2], h[6][3], - h[7][0], h[7][1], h[7][2], h[7][3]]) - } - - - -- Walk addrs at increasing positions; if an override exists for the - -- current position, replace the entry. Lets us inject ctor addresses - -- into the per-position address list without restructuring the rest. - fn apply_ctor_overrides(addrs: List‹Addr›, - overrides: List‹(G, Addr)›, pos: G) - -> List‹Addr› { - match load(addrs) { - ListNode.Nil => store(ListNode.Nil), - ListNode.Cons(addr, rest) => - let new_addr = lookup_override(overrides, pos, addr); - store(ListNode.Cons(new_addr, - apply_ctor_overrides(rest, overrides, pos + 1))), - } + bytes_to_addr(bytes) } - fn lookup_override(overrides: List‹(G, Addr)›, pos: G, - default: Addr) -> Addr { - match load(overrides) { - ListNode.Nil => default, - ListNode.Cons(p, rest) => - match p { - (op, oaddr) => - match op - pos { - 0 => oaddr, - _ => lookup_override(rest, pos, default), - }, - }, - } - } fn ingress_with_primitives(target_addr: Addr) -> (List‹&KConstantInfo›, List‹Addr›) { let (all_addrs, all_consts) = load_with_deps( @@ -1647,12 +1581,13 @@ def ingress := ⟦ fn finish_ingress(all_addrs: List‹Addr›, all_consts: List‹&Constant›) -> (List‹&KConstantInfo›, List‹Addr›) { let (block_addrs, block_starts, total) = compute_layout(all_consts, all_addrs, 0); - let pos_map_naive = build_pos_map(all_consts, all_addrs, block_addrs, block_starts, 0); + let block_start_map = store(build_block_start_map(block_addrs, block_starts)); + let pos_map_naive = build_pos_map(all_consts, all_addrs, block_start_map, 0); -- Canonicalize duplicate Muts wrappers (same members-Ptr) so refs -- converge AND emitted KConstantInfos share content via store dedup. let pos_map = canonicalize_pos_map(all_consts, pos_map_naive); - let canon_addrs = canonicalize_addr_map(all_addrs, all_consts); - let inputs = build_convert_inputs(all_consts, all_addrs, all_addrs, pos_map, canon_addrs, block_addrs, block_starts, 0); + let canon_addr_map = store(build_canon_addr_map(all_addrs, all_consts)); + let inputs = build_convert_inputs(all_consts, all_addrs, all_addrs, pos_map, canon_addr_map, block_start_map, 0); let k_consts = convert_all(inputs); -- Build the pos→Addr tree via two O(N) passes (non-PRJ then PRJ -- overwrites at shared positions). Replaces the prior O(N²) @@ -1662,7 +1597,7 @@ def ingress := ⟦ -- CPrj addresses via Lean's compile (non-aux ctors aren't stored in -- env.consts). We surface them via the `[3] ++ ipr_addr` IO-buffer -- side channel and inject them as tree updates. - let overrides = build_ctor_overrides(all_consts, all_addrs, block_addrs, block_starts); + let overrides = build_ctor_overrides(all_consts, all_addrs, block_start_map); let tree = apply_ctor_overrides_tree(overrides, tree); let zero_addr = store([0u8; 32]); let addrs = emit_addrs_from_tree(0, total, tree, zero_addr); diff --git a/Ix/IxVM/Kernel/Claim.lean b/Ix/IxVM/Kernel/Claim.lean index 7122431a..47c6fa57 100644 --- a/Ix/IxVM/Kernel/Claim.lean +++ b/Ix/IxVM/Kernel/Claim.lean @@ -439,22 +439,8 @@ def claim := ⟦ -- `load_verified_constant`: read bytes, recompute blake3, assert -- equality, deserialize, assert no trailing data. fn load_verified_claim(digest: [U8; 32]) -> Claim { - let (idx, len) = io_get_info(0, digest); - let bytes = #read_byte_stream(0, idx, len); - let h = blake3(bytes); - assert_eq!( - [ - h[0][0], h[0][1], h[0][2], h[0][3], - h[1][0], h[1][1], h[1][2], h[1][3], - h[2][0], h[2][1], h[2][2], h[2][3], - h[3][0], h[3][1], h[3][2], h[3][3], - h[4][0], h[4][1], h[4][2], h[4][3], - h[5][0], h[5][1], h[5][2], h[5][3], - h[6][0], h[6][1], h[6][2], h[6][3], - h[7][0], h[7][1], h[7][2], h[7][3] - ], - digest - ); + let bytes = load_payload_const(digest); + let _ = verify_bytes_against(bytes, digest); let (claim, rest) = get_claim(bytes); assert_eq!(load(rest), ListNode.Nil); claim @@ -467,17 +453,7 @@ def claim := ⟦ -- ============================================================================ fn expr_addr(e_ref: &Expr) -> Addr { let bytes = put_expr(load(e_ref), store(ListNode.Nil)); - let h = blake3(bytes); - store([ - h[0][0], h[0][1], h[0][2], h[0][3], - h[1][0], h[1][1], h[1][2], h[1][3], - h[2][0], h[2][1], h[2][2], h[2][3], - h[3][0], h[3][1], h[3][2], h[3][3], - h[4][0], h[4][1], h[4][2], h[4][3], - h[5][0], h[5][1], h[5][2], h[5][3], - h[6][0], h[6][1], h[6][2], h[6][3], - h[7][0], h[7][1], h[7][2], h[7][3] - ]) + bytes_to_addr(bytes) } -- ============================================================================ @@ -728,33 +704,13 @@ def claim := ⟦ fn leaf_hash(addr: Addr) -> Addr { let tail = put_address(addr, store(ListNode.Nil)); let bytes = store(ListNode.Cons(0u8, tail)); - let h = blake3(bytes); - store([ - h[0][0], h[0][1], h[0][2], h[0][3], - h[1][0], h[1][1], h[1][2], h[1][3], - h[2][0], h[2][1], h[2][2], h[2][3], - h[3][0], h[3][1], h[3][2], h[3][3], - h[4][0], h[4][1], h[4][2], h[4][3], - h[5][0], h[5][1], h[5][2], h[5][3], - h[6][0], h[6][1], h[6][2], h[6][3], - h[7][0], h[7][1], h[7][2], h[7][3] - ]) + bytes_to_addr(bytes) } fn node_hash(l: Addr, r: Addr) -> Addr { let tail = put_address(l, put_address(r, store(ListNode.Nil))); let bytes = store(ListNode.Cons(1u8, tail)); - let h = blake3(bytes); - store([ - h[0][0], h[0][1], h[0][2], h[0][3], - h[1][0], h[1][1], h[1][2], h[1][3], - h[2][0], h[2][1], h[2][2], h[2][3], - h[3][0], h[3][1], h[3][2], h[3][3], - h[4][0], h[4][1], h[4][2], h[4][3], - h[5][0], h[5][1], h[5][2], h[5][3], - h[6][0], h[6][1], h[6][2], h[6][3], - h[7][0], h[7][1], h[7][2], h[7][3] - ]) + bytes_to_addr(bytes) } -- ============================================================================ @@ -780,8 +736,7 @@ def claim := ⟦ fn load_assumption_tree(root: Addr) -> List‹Addr› { let raw = load(root); - let (idx, len) = io_get_info(0, raw); - let bytes = #read_byte_stream(0, idx, len); + let bytes = load_payload_const(raw); let (tag, s) = get_tag4(bytes); let (flag, size) = tag; assert_eq!(flag, 0xE); diff --git a/Tests/Ix/IxVM.lean b/Tests/Ix/IxVM.lean index 45ae64e1..86bf6ff7 100644 --- a/Tests/Ix/IxVM.lean +++ b/Tests/Ix/IxVM.lean @@ -122,53 +122,53 @@ public def kernelCheck (name : Lean.Name) (env : Lean.Environment) : observed cost in the message so it can be pasted back. -/ private def kernelCheckEntries : List (String × Nat) := [ -- Stdlib - ("HEq", 1_715_966), - ("HEq.rec", 2_682_331), - ("Eq.rec", 2_576_284), - ("Nat", 1_858_025), - ("Nat.add", 12_983_943), - ("Nat.add_comm", 54_330_980), - ("Nat.decEq", 68_594_289), - ("Nat.decLe", 191_364_012), - ("Nat.sub_le_of_le_add", 515_130_560), + ("HEq", 1_716_983), + ("HEq.rec", 2_679_377), + ("Eq.rec", 2_574_221), + ("Nat", 1_859_698), + ("Nat.add", 12_945_259), + ("Nat.add_comm", 54_049_773), + ("Nat.decEq", 68_208_022), + ("Nat.decLe", 189_723_325), + ("Nat.sub_le_of_le_add", 510_843_459), -- Newly-unlocked targets (level_leq Géran normalize). - ("Trans.mk", 2_864_146), - ("Array.append_assoc", 2_566_382_883), - ("Vector.append", 2_638_552_021), + ("Trans.mk", 2_858_716), + ("Array.append_assoc", 2_537_360_311), + ("Vector.append", 2_607_800_745), -- Primitive reduction theorems (`IxVMPrim`) - ("IxVMPrim.nat_add_lit", 28_082_349), - ("IxVMPrim.nat_sub_lit", 33_722_451), - ("IxVMPrim.nat_mul_lit", 24_644_737), - ("IxVMPrim.nat_mul_big", 24_146_724), - ("IxVMPrim.nat_div_lit", 366_893_945), - ("IxVMPrim.nat_mod_lit", 375_602_678), - ("IxVMPrim.nat_succ_lit", 7_314_408), - ("IxVMPrim.nat_pred_lit", 14_706_095), - ("IxVMPrim.nat_gcd_lit", 605_222_820), - ("IxVMPrim.nat_land_lit", 1_019_495_718), - ("IxVMPrim.nat_lor_lit", 1_020_299_077), - ("IxVMPrim.nat_xor_lit", 1_029_101_731), - ("IxVMPrim.nat_shl_lit", 34_802_946), - ("IxVMPrim.nat_shr_lit", 372_209_350), - ("IxVMPrim.nat_pow_big", 71_850_166), - ("IxVMPrim.nat_beq_lit", 24_145_604), - ("IxVMPrim.nat_ble_lit", 22_475_134), - ("IxVMPrim.nat_dec_le", 198_007_550), - ("IxVMPrim.nat_dec_lt", 201_972_221), - ("IxVMPrim.nat_dec_eq", 82_417_673), - ("IxVMPrim.str_size_lit", 726_987_300), - ("IxVMPrim.bv_to_nat_lit", 576_925_093), + ("IxVMPrim.nat_add_lit", 27_970_389), + ("IxVMPrim.nat_sub_lit", 33_579_674), + ("IxVMPrim.nat_mul_lit", 24_548_790), + ("IxVMPrim.nat_mul_big", 24_051_042), + ("IxVMPrim.nat_div_lit", 363_794_109), + ("IxVMPrim.nat_mod_lit", 372_486_475), + ("IxVMPrim.nat_succ_lit", 7_308_266), + ("IxVMPrim.nat_pred_lit", 14_682_904), + ("IxVMPrim.nat_gcd_lit", 599_766_283), + ("IxVMPrim.nat_land_lit", 1_009_603_192), + ("IxVMPrim.nat_lor_lit", 1_010_406_405), + ("IxVMPrim.nat_xor_lit", 1_019_030_740), + ("IxVMPrim.nat_shl_lit", 34_670_298), + ("IxVMPrim.nat_shr_lit", 369_132_946), + ("IxVMPrim.nat_pow_big", 71_560_887), + ("IxVMPrim.nat_beq_lit", 24_061_127), + ("IxVMPrim.nat_ble_lit", 22_388_890), + ("IxVMPrim.nat_dec_le", 196_255_925), + ("IxVMPrim.nat_dec_lt", 200_203_243), + ("IxVMPrim.nat_dec_eq", 81_874_028), + ("IxVMPrim.str_size_lit", 716_814_982), + ("IxVMPrim.bv_to_nat_lit", 571_422_589), -- Mutual block + multi-member recursors - ("IxVMInd.Even", 25_974_275), - ("IxVMInd.Odd", 25_737_413), - ("IxVMInd.Even.rec", 31_628_577), - ("IxVMInd.Odd.rec", 31_627_681), + ("IxVMInd.Even", 25_861_665), + ("IxVMInd.Odd", 25_621_808), + ("IxVMInd.Even.rec", 31_434_525), + ("IxVMInd.Odd.rec", 31_433_622), -- Nested inductive + aux recursor (Tree.mk : List Tree → Tree) - ("IxVMInd.Tree", 2_635_546), - ("IxVMInd.Tree.rec", 4_874_311), + ("IxVMInd.Tree", 2_641_542), + ("IxVMInd.Tree.rec", 4_867_794), -- Edge cases from prelude - ("String.Internal.append", 718_452_811), - ("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 1_081_131_375), + ("String.Internal.append", 708_296_270), + ("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 1_064_689_765), ] private def nameOfString (str : String) : Lean.Name := From ee4da06b6e1baea2ab8f93132225ce130e0b1d29 Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Sat, 27 Jun 2026 15:38:37 -0700 Subject: [PATCH 4/4] IxVM: per-kind IOBuffer channels with documented interface MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- Ix/IxVM/ClaimHarness.lean | 63 ++++++++++++++++++------- Ix/IxVM/Ingress.lean | 96 +++++++++++++++++++++++++-------------- Ix/IxVM/Kernel/Claim.lean | 8 +++- Tests/Ix/IxVM.lean | 84 +++++++++++++++++----------------- 4 files changed, 156 insertions(+), 95 deletions(-) diff --git a/Ix/IxVM/ClaimHarness.lean b/Ix/IxVM/ClaimHarness.lean index 1aff93d5..55e29ce1 100644 --- a/Ix/IxVM/ClaimHarness.lean +++ b/Ix/IxVM/ClaimHarness.lean @@ -124,19 +124,45 @@ private def hintToG : Lean.ReducibilityHints → Aiur.G | .abbrev => .ofNat 0xFFFFFFFF | .regular n => .ofNat (min (1 + n.toNat) 0xFFFFFFFE) +/-! ## IxVM IOBuffer interface + +The host seeds blake3-keyed payloads on six channels; the Aiur kernel +consumes them via `io_get_info` + `#read_byte_stream`. One value shape +per channel — no overloading, no in-band discriminators. + +Tiered by access pattern (matches kernel runtime order): + +| Tier | Channel | Purpose | Key (32 G) | Value shape | +|--------|---------|--------------------------|-------------------------|-------------------| +| 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 fires once per `verify_claim` invocation (claim + optional tree). +Tier 2 fires per constant traversed during `load_with_deps`. Tier 3 +fires per blob ref encountered during `build_ref_idxs_and_blobs`. + +Soundness: +* ch 0/1/2/5 — every byte stream is blake3-verified by the kernel + against its content-addressed key. +* ch 3 — semantically optional; controls WHNF reduction heuristic + only, def-eq is sound either way. +* ch 4 — sound by erasure-correctness: a lying discriminator flips + the const/blob decision and the wrong-path load downstream fails + (a "const" blob triggers a ch 2 read returning empty → blake3 + verify against the non-empty addr fails; a "blob" const dangles + references → typecheck fail). + +Channel numbers MUST stay in sync with the inlined `io_get_info` / +`#read_byte_stream` channel literals in `Ix/IxVM/Ingress.lean` and +`Ix/IxVM/Kernel/Claim.lean`. +-/ + /-- Insert all per-address entries for `addr`s satisfying `keep` into - `ioBuffer`. Each address kind lives on its own channel; the key is - always the 32-G blake3 hash, with no disambiguating suffix. - - | channel | key (32 G) | value | meaning | - |---------|------------|----------------|---------| - | 0 | `addr` | const bytes | constant data (empty marker = `addr` is a blob) | - | 1 | `addr` | raw blob bytes | referenced data (verified by Aiur via blake3) | - | 2 | `addr` | single G | Defn `ReducibilityHints` encoding | - - Blob addrs also get an empty entry on channel 0 so the kernel's - constant-vs-blob detection (`io_get_info(0, addr) ⇒ len=0`) still - works without a separate query path. -/ + `ioBuffer`. See the channel table above. -/ def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool) (ioBuffer : Aiur.IOBuffer) : Aiur.IOBuffer := Id.run do let mut ioBuffer := ioBuffer @@ -146,18 +172,21 @@ def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool) -- serialized form the lazy entry holds — no materialization needed. let bytes := lc.rawBytes let key : Array Aiur.G := addr.hash.data.map .ofUInt8 - ioBuffer := ioBuffer.extend 0 key (bytes.data.map .ofUInt8) + ioBuffer := ioBuffer.extend 2 key (bytes.data.map .ofUInt8) + -- Discriminator: this addr resolves to a constant. + ioBuffer := ioBuffer.extend 4 key #[.ofNat 1] for (addr, rawBytes) in ixonEnv.blobs do if !keep addr then continue let key : Array Aiur.G := addr.hash.data.map .ofUInt8 - ioBuffer := ioBuffer.extend 1 key (rawBytes.data.map fun b => .ofNat b.toNat) - ioBuffer := ioBuffer.extend 0 key #[] + ioBuffer := ioBuffer.extend 5 key (rawBytes.data.map fun b => .ofNat b.toNat) + -- Discriminator: this addr resolves to a blob. + ioBuffer := ioBuffer.extend 4 key #[.ofNat 0] for (_, named) in ixonEnv.named do if !keep named.addr then continue match named.constMeta with | .defn _ _ hints _ _ _ _ _ => let key : Array Aiur.G := named.addr.hash.data.map .ofUInt8 - ioBuffer := ioBuffer.extend 2 key #[hintToG hints] + ioBuffer := ioBuffer.extend 3 key #[hintToG hints] | _ => pure () return ioBuffer @@ -189,7 +218,7 @@ private def seedTreeAt (root : Address) match trees.get? root with | some tree => let bytes := Ix.AssumptionTree.ser tree - .ok (ioBuffer.extend 0 (addrKey tree.root) (bytes.data.map .ofUInt8)) + .ok (ioBuffer.extend 1 (addrKey tree.root) (bytes.data.map .ofUInt8)) | none => .error s!"no assumption tree supplied for root {root}" /-- Build the witness for `verify_claim` against `claim`. diff --git a/Ix/IxVM/Ingress.lean b/Ix/IxVM/Ingress.lean index 32854a8a..5d038da4 100644 --- a/Ix/IxVM/Ingress.lean +++ b/Ix/IxVM/Ingress.lean @@ -9,41 +9,58 @@ namespace IxVM def ingress := ⟦ -- IOBuffer channel identifiers. See `ClaimHarness.lean` for the host-side -- counterpart that seeds these channels. - fn ch_const() -> G { 0 } - fn ch_blob() -> G { 1 } - fn ch_hint() -> G { 2 } - - -- Read the raw bytes the prover seeded at `key` on `channel`. - -- Channels and keys are documented per call site; the helper exists - -- only to centralise the `io_get_info` + `#read_byte_stream` pair. - fn load_payload_const(key: [U8; 32]) -> ByteStream { - let (idx, len) = io_get_info(0, key); - #read_byte_stream(0, idx, len) - } - fn load_payload_blob(key: [U8; 32]) -> ByteStream { - let (idx, len) = io_get_info(1, key); - #read_byte_stream(1, idx, len) - } - fn load_payload_hint(key: [U8; 32]) -> ByteStream { - let (idx, len) = io_get_info(2, key); - #read_byte_stream(2, idx, len) - } + -- ============================================================================ + -- IxVM IOBuffer interface + -- + -- The host (Lean `IxVM.ClaimHarness`) seeds blake3-keyed payloads on six + -- channels; the kernel consumes them via `io_get_info` + `#read_byte_stream`. + -- One value shape per channel — no overloading, no in-band discriminators. + -- + -- Tiered by access pattern (matches kernel runtime order): + -- + -- Tier 1 — control input (one-per-run): + -- ch 0 claim wire bytes key = blake3(claim_bytes) value = claim bytes + -- ch 1 assumption tree bytes key = tree.root value = tree bytes + -- + -- Tier 2 — per-const data: + -- ch 2 constant wire bytes key = const.addr value = const bytes + -- ch 3 Defn reducibility hint key = defn.addr value = [hint_G] + -- + -- Tier 3 — per-blob data: + -- ch 4 blob discriminator key = addr value = [1=const,0=blob] + -- ch 5 blob raw bytes key = blob.addr value = raw bytes + -- + -- Soundness: every kernel-consumed byte stream is blake3-verified + -- against its key (ch 0/1/2/5). ch 3 hint is semantically optional + -- (controls WHNF heuristic only; def-eq is sound either way). ch 4 + -- discriminator is sound by erasure-correctness: lying flips the + -- const/blob decision and the wrong-path load fails downstream. + -- + -- Per-channel access patterns are inlined at each consumer (one site + -- per channel) so the dispatch never crosses a fn boundary — channel + -- choice doesn't add Aiur per-row width tax. Each `io_get_info` + + -- `#read_byte_stream` pair appears once at the producer call site. + -- Channel numbers MUST stay in sync with `Ix/IxVM/ClaimHarness.lean`. + -- ============================================================================ - -- Load a constant from IOBuffer by address, verify blake3, deserialize. + -- Load a constant from IOBuffer by address (ch 2), verify blake3, + -- deserialize. fn load_verified_constant(addr: Addr) -> Constant { let raw = load(addr); - let bytes = load_payload_const(raw); + let (idx, len) = io_get_info(2, raw); + let bytes = #read_byte_stream(2, idx, len); let _ = verify_bytes_against(bytes, raw); let (constant, rest) = get_constant(bytes); assert_eq!(load(rest), ListNode.Nil); constant } - -- Load a blob from IOBuffer by address, verify blake3, return raw bytes. - -- Blobs live on channel 1; constants live on channel 0 with the same key. + -- Load a blob from IOBuffer by address (ch 5), verify blake3, return + -- raw bytes. fn load_verified_blob(addr: Addr) -> ByteStream { let raw = load(addr); - let bytes = load_payload_blob(raw); + let (idx, len) = io_get_info(5, raw); + let bytes = #read_byte_stream(5, idx, len); let _ = verify_bytes_against(bytes, raw); bytes } @@ -99,15 +116,17 @@ def ingress := ⟦ } } - -- Load reducibility hint G for a Defn at `addr`. Lives on channel 2. - -- Encoding (mirror Lean.ReducibilityHints): + -- Load reducibility hint G for a Defn at `addr` (ch 3). Encoding + -- mirrors `Lean.ReducibilityHints`: -- 0 = Opaque -- 1 + h = Regular(h) -- 0xFFFFFFFF = Abbrev - -- Caller MUST only invoke this for Defn addrs; the harness only seeds - -- channel 2 for defns. A missing key aborts execution (correct). + -- Caller MUST only invoke this for Defn addrs; the harness only + -- seeds ch 3 for Defns. A missing key aborts execution (correct). fn load_constant_hint(addr: Addr) -> G { - let bytes = load_payload_hint(load(addr)); + let raw = load(addr); + let (idx, len) = io_get_info(3, raw); + let bytes = #read_byte_stream(3, idx, len); match load(bytes) { ListNode.Cons(b, _) => to_field(b), } @@ -1231,11 +1250,20 @@ def ingress := ⟦ load_with_deps(next, rest, visited_addrs, visited_consts, visited_set), }, _ => - -- Check if this address has constant data in IOBuffer. - -- io_get_info is unconstrained; the prover provides (0, 0) for blob addresses. - -- Soundness: if the prover lies and skips a real constant, type checking will fail. - let (_, len) = io_get_info(0, load(addr)); - match len { + -- Discriminator on ch 4: 1 = const, 0 = blob. The host + -- (`addEntries`) seeds exactly one byte per addr it ships. + -- Soundness via erasure-correctness: lying flips the const/blob + -- decision, and the wrong-path load fails downstream (a "blob" + -- const won't get its bytes ingressed → refs to it dangle → + -- typecheck fail; a "const" blob triggers a ch 2 read that + -- returns empty → blake3 verify against the non-empty addr + -- fails). + let (idx, len) = io_get_info(4, load(addr)); + let kind_bytes = #read_byte_stream(4, idx, len); + let kind = match load(kind_bytes) { + ListNode.Cons(b, _) => to_field(b), + }; + match kind { 0 => -- Blob address: skip (blob values are loaded on demand in build_lit_blobs) match load(worklist) { diff --git a/Ix/IxVM/Kernel/Claim.lean b/Ix/IxVM/Kernel/Claim.lean index 47c6fa57..ccfc9d15 100644 --- a/Ix/IxVM/Kernel/Claim.lean +++ b/Ix/IxVM/Kernel/Claim.lean @@ -438,8 +438,11 @@ def claim := ⟦ -- Load + verify a claim from the IOBuffer at key=`digest`. Mirrors -- `load_verified_constant`: read bytes, recompute blake3, assert -- equality, deserialize, assert no trailing data. + -- Load + verify a claim from IOBuffer at `digest` (ch 0). Reads bytes, + -- recomputes blake3, asserts equality, deserialises. fn load_verified_claim(digest: [U8; 32]) -> Claim { - let bytes = load_payload_const(digest); + let (idx, len) = io_get_info(0, digest); + let bytes = #read_byte_stream(0, idx, len); let _ = verify_bytes_against(bytes, digest); let (claim, rest) = get_claim(bytes); assert_eq!(load(rest), ListNode.Nil); @@ -736,7 +739,8 @@ def claim := ⟦ fn load_assumption_tree(root: Addr) -> List‹Addr› { let raw = load(root); - let bytes = load_payload_const(raw); + let (idx, len) = io_get_info(1, raw); + let bytes = #read_byte_stream(1, idx, len); let (tag, s) = get_tag4(bytes); let (flag, size) = tag; assert_eq!(flag, 0xE); diff --git a/Tests/Ix/IxVM.lean b/Tests/Ix/IxVM.lean index 86bf6ff7..46af36c5 100644 --- a/Tests/Ix/IxVM.lean +++ b/Tests/Ix/IxVM.lean @@ -122,53 +122,53 @@ public def kernelCheck (name : Lean.Name) (env : Lean.Environment) : observed cost in the message so it can be pasted back. -/ private def kernelCheckEntries : List (String × Nat) := [ -- Stdlib - ("HEq", 1_716_983), - ("HEq.rec", 2_679_377), - ("Eq.rec", 2_574_221), - ("Nat", 1_859_698), - ("Nat.add", 12_945_259), - ("Nat.add_comm", 54_049_773), - ("Nat.decEq", 68_208_022), - ("Nat.decLe", 189_723_325), - ("Nat.sub_le_of_le_add", 510_843_459), + ("HEq", 1_716_804), + ("HEq.rec", 2_678_994), + ("Eq.rec", 2_573_838), + ("Nat", 1_859_519), + ("Nat.add", 12_944_048), + ("Nat.add_comm", 54_047_004), + ("Nat.decEq", 68_205_533), + ("Nat.decLe", 189_722_204), + ("Nat.sub_le_of_le_add", 510_870_092), -- Newly-unlocked targets (level_leq Géran normalize). - ("Trans.mk", 2_858_716), - ("Array.append_assoc", 2_537_360_311), - ("Vector.append", 2_607_800_745), + ("Trans.mk", 2_858_426), + ("Array.append_assoc", 2_537_478_644), + ("Vector.append", 2_607_925_682), -- Primitive reduction theorems (`IxVMPrim`) - ("IxVMPrim.nat_add_lit", 27_970_389), - ("IxVMPrim.nat_sub_lit", 33_579_674), - ("IxVMPrim.nat_mul_lit", 24_548_790), - ("IxVMPrim.nat_mul_big", 24_051_042), - ("IxVMPrim.nat_div_lit", 363_794_109), - ("IxVMPrim.nat_mod_lit", 372_486_475), - ("IxVMPrim.nat_succ_lit", 7_308_266), - ("IxVMPrim.nat_pred_lit", 14_682_904), - ("IxVMPrim.nat_gcd_lit", 599_766_283), - ("IxVMPrim.nat_land_lit", 1_009_603_192), - ("IxVMPrim.nat_lor_lit", 1_010_406_405), - ("IxVMPrim.nat_xor_lit", 1_019_030_740), - ("IxVMPrim.nat_shl_lit", 34_670_298), - ("IxVMPrim.nat_shr_lit", 369_132_946), - ("IxVMPrim.nat_pow_big", 71_560_887), - ("IxVMPrim.nat_beq_lit", 24_061_127), - ("IxVMPrim.nat_ble_lit", 22_388_890), - ("IxVMPrim.nat_dec_le", 196_255_925), - ("IxVMPrim.nat_dec_lt", 200_203_243), - ("IxVMPrim.nat_dec_eq", 81_874_028), - ("IxVMPrim.str_size_lit", 716_814_982), - ("IxVMPrim.bv_to_nat_lit", 571_422_589), + ("IxVMPrim.nat_add_lit", 27_965_913), + ("IxVMPrim.nat_sub_lit", 33_575_354), + ("IxVMPrim.nat_mul_lit", 24_546_472), + ("IxVMPrim.nat_mul_big", 24_048_795), + ("IxVMPrim.nat_div_lit", 363_810_437), + ("IxVMPrim.nat_mod_lit", 372_503_418), + ("IxVMPrim.nat_succ_lit", 7_306_831), + ("IxVMPrim.nat_pred_lit", 14_680_455), + ("IxVMPrim.nat_gcd_lit", 599_806_695), + ("IxVMPrim.nat_land_lit", 1_009_687_743), + ("IxVMPrim.nat_lor_lit", 1_010_490_897), + ("IxVMPrim.nat_xor_lit", 1_019_114_634), + ("IxVMPrim.nat_shl_lit", 34_666_438), + ("IxVMPrim.nat_shr_lit", 369_149_913), + ("IxVMPrim.nat_pow_big", 71_556_071), + ("IxVMPrim.nat_beq_lit", 24_057_793), + ("IxVMPrim.nat_ble_lit", 22_385_742), + ("IxVMPrim.nat_dec_le", 196_255_439), + ("IxVMPrim.nat_dec_lt", 200_202_805), + ("IxVMPrim.nat_dec_eq", 81_870_937), + ("IxVMPrim.str_size_lit", 716_854_159), + ("IxVMPrim.bv_to_nat_lit", 571_458_745), -- Mutual block + multi-member recursors - ("IxVMInd.Even", 25_861_665), - ("IxVMInd.Odd", 25_621_808), - ("IxVMInd.Even.rec", 31_434_525), - ("IxVMInd.Odd.rec", 31_433_622), + ("IxVMInd.Even", 25_857_751), + ("IxVMInd.Odd", 25_617_894), + ("IxVMInd.Even.rec", 31_430_086), + ("IxVMInd.Odd.rec", 31_429_183), -- Nested inductive + aux recursor (Tree.mk : List Tree → Tree) - ("IxVMInd.Tree", 2_641_542), - ("IxVMInd.Tree.rec", 4_867_794), + ("IxVMInd.Tree", 2_641_130), + ("IxVMInd.Tree.rec", 4_866_817), -- Edge cases from prelude - ("String.Internal.append", 708_296_270), - ("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 1_064_689_765), + ("String.Internal.append", 708_332_683), + ("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 1_064_762_809), ] private def nameOfString (str : String) : Lean.Name :=