From 7efebe660402d415b18201c5043aca80e23c9853 Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Wed, 24 Jun 2026 10:32:23 -0700 Subject: [PATCH 1/5] 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 5fee59188..56987ed75 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 d73e870d1..45ae64e1a 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 bae332ef0f7e8083da35828b87ee52a1798f2005 Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Sat, 27 Jun 2026 11:06:32 -0700 Subject: [PATCH 2/5] =?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 7412c6e42..fa06ded8e 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 b9cbd972d..881ee9f2e 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 56987ed75..32854a8ad 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 7122431a6..47c6fa57e 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 45ae64e1a..86bf6ff7c 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 64390ad140146b4f9c4c78eb902923061e05edb3 Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Sat, 27 Jun 2026 15:38:37 -0700 Subject: [PATCH 3/5] 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 1aff93d50..55e29ce17 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 32854a8ad..5d038da40 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 47c6fa57e..ccfc9d152 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 86bf6ff7c..46af36c53 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 := From 1fb0dd13e9c60a4fd9c6c2910c63659f99c66511 Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Thu, 2 Jul 2026 07:59:15 -0700 Subject: [PATCH 4/5] IxVM Blake3: inline blake3_flat at its two call sites MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `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. --- Ix/IxVM/Blake3.lean | 35 +++++++++++-------- Tests/Ix/IxVM.lean | 84 ++++++++++++++++++++++----------------------- 2 files changed, 62 insertions(+), 57 deletions(-) diff --git a/Ix/IxVM/Blake3.lean b/Ix/IxVM/Blake3.lean index fa06ded8e..673f063cd 100644 --- a/Ix/IxVM/Blake3.lean +++ b/Ix/IxVM/Blake3.lean @@ -45,24 +45,21 @@ 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); + 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]], + expected); () } @@ -71,7 +68,15 @@ def blake3 := ⟦ -- 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)) + 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]]) } fn blake3_next_layer(layer: Layer, digest: [[U8; 4]; 8], root: G) -> (MaybeDigest, Layer) { diff --git a/Tests/Ix/IxVM.lean b/Tests/Ix/IxVM.lean index 46af36c53..c915d34ac 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_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), + ("HEq", 1_716_476), + ("HEq.rec", 2_678_518), + ("Eq.rec", 2_573_362), + ("Nat", 1_859_043), + ("Nat.add", 12_940_971), + ("Nat.add_comm", 54_034_851), + ("Nat.decEq", 68_193_672), + ("Nat.decLe", 189_689_247), + ("Nat.sub_le_of_le_add", 510_810_753), -- Newly-unlocked targets (level_leq Géran normalize). - ("Trans.mk", 2_858_426), - ("Array.append_assoc", 2_537_478_644), - ("Vector.append", 2_607_925_682), + ("Trans.mk", 2_858_098), + ("Array.append_assoc", 2_537_268_602), + ("Vector.append", 2_607_707_384), -- Primitive reduction theorems (`IxVMPrim`) - ("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), + ("IxVMPrim.nat_add_lit", 27_956_627), + ("IxVMPrim.nat_sub_lit", 33_564_651), + ("IxVMPrim.nat_mul_lit", 24_539_380), + ("IxVMPrim.nat_mul_big", 24_041_970), + ("IxVMPrim.nat_div_lit", 363_760_965), + ("IxVMPrim.nat_mod_lit", 372_452_500), + ("IxVMPrim.nat_succ_lit", 7_303_982), + ("IxVMPrim.nat_pred_lit", 14_675_191), + ("IxVMPrim.nat_gcd_lit", 599_734_613), + ("IxVMPrim.nat_land_lit", 1_009_577_758), + ("IxVMPrim.nat_lor_lit", 1_010_380_511), + ("IxVMPrim.nat_xor_lit", 1_019_001_840), + ("IxVMPrim.nat_shl_lit", 34_655_734), + ("IxVMPrim.nat_shr_lit", 369_099_356), + ("IxVMPrim.nat_pow_big", 71_540_935), + ("IxVMPrim.nat_beq_lit", 24_050_432), + ("IxVMPrim.nat_ble_lit", 22_378_650), + ("IxVMPrim.nat_dec_le", 196_221_114), + ("IxVMPrim.nat_dec_lt", 200_167_450), + ("IxVMPrim.nat_dec_eq", 81_855_497), + ("IxVMPrim.str_size_lit", 716_747_374), + ("IxVMPrim.bv_to_nat_lit", 571_385_143), -- Mutual block + multi-member recursors - ("IxVMInd.Even", 25_857_751), - ("IxVMInd.Odd", 25_617_894), - ("IxVMInd.Even.rec", 31_430_086), - ("IxVMInd.Odd.rec", 31_429_183), + ("IxVMInd.Even", 25_849_023), + ("IxVMInd.Odd", 25_609_442), + ("IxVMInd.Even.rec", 31_420_238), + ("IxVMInd.Odd.rec", 31_419_335), -- Nested inductive + aux recursor (Tree.mk : List Tree → Tree) - ("IxVMInd.Tree", 2_641_130), - ("IxVMInd.Tree.rec", 4_866_817), + ("IxVMInd.Tree", 2_640_146), + ("IxVMInd.Tree.rec", 4_865_455), -- Edge cases from prelude - ("String.Internal.append", 708_332_683), - ("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 1_064_762_809), + ("String.Internal.append", 708_226_297), + ("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 1_064_618_151), ] private def nameOfString (str : String) : Lean.Name := From b84a500f7fe92d7ecd7f55bc4b6be0dbd191e36e Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Thu, 2 Jul 2026 11:33:31 -0700 Subject: [PATCH 5/5] IxVM kernel: KLevel = &KLevelNode (pass universes by pointer) 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. --- Ix/IxVM.lean | 88 +++++++----------- Ix/IxVM/Convert.lean | 18 ++-- Ix/IxVM/Ingress.lean | 2 +- Ix/IxVM/Kernel/CanonicalCheck.lean | 62 ++++++------- Ix/IxVM/Kernel/Check.lean | 20 ++-- Ix/IxVM/Kernel/DefEq.lean | 14 +-- Ix/IxVM/Kernel/Inductive.lean | 88 +++++++++--------- Ix/IxVM/Kernel/Infer.lean | 20 ++-- Ix/IxVM/Kernel/Levels.lean | 144 ++++++++++++++--------------- Ix/IxVM/Kernel/Primitive.lean | 18 ++-- Ix/IxVM/Kernel/Subst.lean | 2 +- Ix/IxVM/Kernel/Whnf.lean | 16 ++-- Ix/IxVM/KernelTypes.lean | 32 ++++--- Tests/Ix/IxVM.lean | 84 ++++++++--------- 14 files changed, 295 insertions(+), 313 deletions(-) diff --git a/Ix/IxVM.lean b/Ix/IxVM.lean index 112e7abc4..9d7679ab4 100644 --- a/Ix/IxVM.lean +++ b/Ix/IxVM.lean @@ -45,89 +45,69 @@ def entrypoints := ⟦ } fn level_cmp_tests() { + let zero = store(KLevelNode.Zero); + let p0 = store(KLevelNode.Param(0)); + let p1 = store(KLevelNode.Param(1)); + let succ_p0 = store(KLevelNode.Succ(p0)); + let succ_zero = store(KLevelNode.Succ(zero)); + -- Zero ≤ anything - assert_eq!(level_leq(KLevel.Zero, KLevel.Param(0)), 1); + assert_eq!(level_leq(zero, p0), 1); -- Param(u) ≤ Param(u) (reflexivity) - assert_eq!(level_leq(KLevel.Param(0), KLevel.Param(0)), 1); + assert_eq!(level_leq(p0, p0), 1); -- Param(u) ≤ Param(v) fails (u ≠ v, set u > v) - assert_eq!(level_leq(KLevel.Param(0), KLevel.Param(1)), 0); + assert_eq!(level_leq(p0, p1), 0); -- Succ(u) ≤ Succ(u) (peel both succs) - assert_eq!(level_leq( - KLevel.Succ(store(KLevel.Param(0))), - KLevel.Succ(store(KLevel.Param(0)))), 1); + assert_eq!(level_leq(succ_p0, succ_p0), 1); -- Succ(u) ≤ u fails (u+1 > u at any assignment) - assert_eq!(level_leq( - KLevel.Succ(store(KLevel.Param(0))), - KLevel.Param(0)), 0); - - -- === level_leq: Param ≤ Succ reduction === - - -- Param(u) ≤ Succ(Param(u)) (u ≤ u+1, reduces to u ≤ u) - assert_eq!(level_leq( - KLevel.Param(0), - KLevel.Succ(store(KLevel.Param(0)))), 1); + assert_eq!(level_leq(succ_p0, p0), 0); - -- === level_leq: Max distribution === + -- Param(u) ≤ Succ(Param(u)) (u ≤ u+1) + assert_eq!(level_leq(p0, succ_p0), 1); -- max(u, v) ≤ max(u, v) (reflexivity via distribution) - let max_uv = KLevel.Max(store(KLevel.Param(0)), store(KLevel.Param(1))); + let max_uv = store(KLevelNode.Max(p0, p1)); assert_eq!(level_leq(max_uv, max_uv), 1); - -- u ≤ max(u, v) (try-each-branch: first branch succeeds) - assert_eq!(level_leq(KLevel.Param(0), max_uv), 1); + -- u ≤ max(u, v) + assert_eq!(level_leq(p0, max_uv), 1); - -- max(u, v) ≤ u fails (set v > u) - assert_eq!(level_leq(max_uv, KLevel.Param(0)), 0); + -- max(u, v) ≤ u fails + assert_eq!(level_leq(max_uv, p0), 0); - -- === level_leq: IMax case-splitting === - - -- imax(u, v) ≤ max(u, v) (case-split on v: v=0 gives 0 ≤ max(0,0)=0; v>0 gives max=max) - let imax_uv = KLevel.IMax(store(KLevel.Param(0)), store(KLevel.Param(1))); + -- imax(u, v) ≤ max(u, v) + let imax_uv = store(KLevelNode.IMax(p0, p1)); assert_eq!(level_leq(imax_uv, max_uv), 1); - -- max(u, v) ≤ imax(u, v) fails (set v=0: max(u,0) = u but imax(u,0) = 0; take u=1) + -- max(u, v) ≤ imax(u, v) fails assert_eq!(level_leq(max_uv, imax_uv), 0); - -- === level_leq: Succ ≤ Max with IMax child (the case-split fix) === - - -- u+1 = max(1, imax(u+1, u)): equal for all σ - -- σ(u)=0: 1 = max(1, imax(1,0)) = max(1,0) = 1 - -- σ(u)=n>0: n+1 = max(1, max(n+1,n)) = n+1 - -- This is the case that requires case-splitting through Max when - -- neither branch (Succ(Zero) or IMax) alone dominates Succ(Param(u)). - let a = KLevel.Succ(store(KLevel.Param(0))); - let b = KLevel.Max( - store(KLevel.Succ(store(KLevel.Zero))), - store(KLevel.IMax( - store(KLevel.Succ(store(KLevel.Param(0)))), - store(KLevel.Param(0))))); + -- u+1 = max(1, imax(u+1, u)): equal for all σ (case-split fix) + let a = succ_p0; + let b = store(KLevelNode.Max( + succ_zero, + store(KLevelNode.IMax(succ_p0, p0)))); assert_eq!(level_equal(a, b), 1); - -- === level_equal: semantic equality === - - -- imax(u, u) = u (when u=0: imax(0,0)=0=u; when u>0: max(u,u)=u) - assert_eq!(level_equal( - KLevel.IMax(store(KLevel.Param(0)), store(KLevel.Param(0))), - KLevel.Param(0)), 1); + -- imax(u, u) = u + assert_eq!(level_equal(store(KLevelNode.IMax(p0, p0)), p0), 1); -- max(u, 0) = u - assert_eq!(level_equal( - KLevel.Max(store(KLevel.Param(0)), store(KLevel.Zero)), - KLevel.Param(0)), 1); + assert_eq!(level_equal(store(KLevelNode.Max(p0, zero)), p0), 1); -- level_imax reduces imax(u, 1+v) to max(u, 1+v) and imax(u, 0) to 0 - let succ_v = KLevel.Succ(store(KLevel.Param(1))); + let succ_v = store(KLevelNode.Succ(p1)); assert_eq!(level_eq( - level_imax(KLevel.Param(0), succ_v), - KLevel.Max(store(KLevel.Param(0)), store(succ_v))), 1); + level_imax(p0, succ_v), + store(KLevelNode.Max(p0, succ_v))), 1); assert_eq!(level_eq( - level_imax(KLevel.Param(0), KLevel.Zero), - KLevel.Zero), 1); + level_imax(p0, zero), + zero), 1); } pub fn kernel_unit_tests() { diff --git a/Ix/IxVM/Convert.lean b/Ix/IxVM/Convert.lean index 881ee9f2e..36a237448 100644 --- a/Ix/IxVM/Convert.lean +++ b/Ix/IxVM/Convert.lean @@ -59,23 +59,23 @@ def convert := ⟦ -- 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.Var(idx) => KLevel.Param(flatten_u64(idx)), + Univ.Zero => store(KLevelNode.Zero), + Univ.Succ(inner) => store(KLevelNode.Succ(convert_univ(inner))), + Univ.Max(a, b) => store(KLevelNode.Max(convert_univ(a), convert_univ(b))), + Univ.IMax(a, b) => store(KLevelNode.IMax(convert_univ(a), convert_univ(b))), + Univ.Var(idx) => store(KLevelNode.Param(flatten_u64(idx))), } } - -- Resolve a list of universe indices to a List‹&KLevel› - fn convert_univ_idxs(idxs: List‹U64›, univs: List‹&Univ›) -> List‹&KLevel› { + -- Resolve a list of universe indices to a List‹KLevel› + fn convert_univ_idxs(idxs: List‹U64›, univs: List‹&Univ›) -> List‹KLevel› { match load(idxs) { ListNode.Nil => store(ListNode.Nil), 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_ref = list_lookup(univs, flatten_u64(idx)); - store(ListNode.Cons(store(convert_univ(u_ref)), convert_univ_idxs(rest, univs))), + store(ListNode.Cons(convert_univ(u_ref), convert_univ_idxs(rest, univs))), } } @@ -154,7 +154,7 @@ def convert := ⟦ -- field-indexed walk (see `convert_univ_idxs`): avoids the per-step -- U64 predecessor of `list_lookup_u64` on this hot universe lookup. let u_ref = list_lookup(univs, flatten_u64(univ_idx)); - store(KExprNode.Srt(store(convert_univ(u_ref)))), + store(KExprNode.Srt(convert_univ(u_ref))), Expr.Var(idx) => store(KExprNode.BVar(flatten_u64(idx))), diff --git a/Ix/IxVM/Ingress.lean b/Ix/IxVM/Ingress.lean index 5d038da40..ecf7f281f 100644 --- a/Ix/IxVM/Ingress.lean +++ b/Ix/IxVM/Ingress.lean @@ -1654,7 +1654,7 @@ def ingress := ⟦ -- its true position; the stub is only consulted otherwise. fn synthetic_primitive_entries() -> (List‹&KConstantInfo›, List‹Addr›) { let addrs = synthetic_primitive_addrs(); - let stub_ty = store(KExprNode.Srt(store(KLevel.Zero))); + let stub_ty = store(KExprNode.Srt(store(KLevelNode.Zero))); let stub = store(KConstantInfo.Axiom(0, stub_ty, 0)); let consts = list_repeat_stub(stub, list_addr_length(addrs)); (consts, addrs) diff --git a/Ix/IxVM/Kernel/CanonicalCheck.lean b/Ix/IxVM/Kernel/CanonicalCheck.lean index a3d8f4e1c..f45f260ee 100644 --- a/Ix/IxVM/Kernel/CanonicalCheck.lean +++ b/Ix/IxVM/Kernel/CanonicalCheck.lean @@ -113,61 +113,61 @@ def canonicalCheck := ⟦ -- IMax < Param. -- ============================================================================ fn compare_kuniv(x: KLevel, y: KLevel) -> G { - match x { - KLevel.Zero => - match y { - KLevel.Zero => 1, + match load(x) { + KLevelNode.Zero => + match load(y) { + KLevelNode.Zero => 1, _ => 0, }, - KLevel.Succ(&xa) => - match y { - KLevel.Zero => 2, - KLevel.Succ(&ya) => compare_kuniv(xa, ya), + KLevelNode.Succ(xa) => + match load(y) { + KLevelNode.Zero => 2, + KLevelNode.Succ(ya) => compare_kuniv(xa, ya), _ => 0, }, - KLevel.Max(&xl, &xr) => - match y { - KLevel.Zero => 2, - KLevel.Succ(_) => 2, - KLevel.Max(&yl, &yr) => + KLevelNode.Max(xl, xr) => + match load(y) { + KLevelNode.Zero => 2, + KLevelNode.Succ(_) => 2, + KLevelNode.Max(yl, yr) => ord_then(compare_kuniv(xl, yl), compare_kuniv(xr, yr)), _ => 0, }, - KLevel.IMax(&xl, &xr) => - match y { - KLevel.Zero => 2, - KLevel.Succ(_) => 2, - KLevel.Max(_, _) => 2, - KLevel.IMax(&yl, &yr) => + KLevelNode.IMax(xl, xr) => + match load(y) { + KLevelNode.Zero => 2, + KLevelNode.Succ(_) => 2, + KLevelNode.Max(_, _) => 2, + KLevelNode.IMax(yl, yr) => ord_then(compare_kuniv(xl, yl), compare_kuniv(xr, yr)), - KLevel.Param(_) => 0, + KLevelNode.Param(_) => 0, }, - KLevel.Param(xi) => - match y { - KLevel.Param(yi) => ord_cmp_g(xi, yi), + KLevelNode.Param(xi) => + match load(y) { + KLevelNode.Param(yi) => ord_cmp_g(xi, yi), _ => 2, }, } } - fn compare_kuniv_list(xs: List‹&KLevel›, ys: List‹&KLevel›) -> G { + fn compare_kuniv_list(xs: List‹KLevel›, ys: List‹KLevel›) -> G { match load(xs) { ListNode.Nil => match load(ys) { ListNode.Nil => 1, _ => 0, }, - ListNode.Cons(&xh, xt) => + ListNode.Cons(xh, xt) => match load(ys) { ListNode.Nil => 2, - ListNode.Cons(&yh, yt) => + ListNode.Cons(yh, yt) => ord_then(compare_kuniv(xh, yh), compare_kuniv_list(xt, yt)), }, } } -- SOrd-returning variant; universes are structural so always strong. - fn compare_kuniv_list_sord(xs: List‹&KLevel›, ys: List‹&KLevel›) -> (G, G) { + fn compare_kuniv_list_sord(xs: List‹KLevel›, ys: List‹KLevel›) -> (G, G) { sord_of_g(compare_kuniv_list(xs, ys)) } @@ -192,10 +192,10 @@ def canonicalCheck := ⟦ KExprNode.BVar(yi) => ord_cmp_g(xi, yi), _ => 0, }, - KExprNode.Srt(&xu) => + KExprNode.Srt(xu) => match y { KExprNode.BVar(_) => 2, - KExprNode.Srt(&yu) => compare_kuniv(xu, yu), + KExprNode.Srt(yu) => compare_kuniv(xu, yu), _ => 0, }, KExprNode.Const(xid, xls) => @@ -285,10 +285,10 @@ def canonicalCheck := ⟦ KExprNode.BVar(yi) => sord_of_g(ord_cmp_g(xi, yi)), _ => sord_lt_strong(), }, - KExprNode.Srt(&xu) => + KExprNode.Srt(xu) => match y { KExprNode.BVar(_) => sord_gt_strong(), - KExprNode.Srt(&yu) => sord_of_g(compare_kuniv(xu, yu)), + KExprNode.Srt(yu) => sord_of_g(compare_kuniv(xu, yu)), _ => sord_lt_strong(), }, KExprNode.Const(xid, xls) => diff --git a/Ix/IxVM/Kernel/Check.lean b/Ix/IxVM/Kernel/Check.lean index efe1a9ef6..f30a9078f 100644 --- a/Ix/IxVM/Kernel/Check.lean +++ b/Ix/IxVM/Kernel/Check.lean @@ -89,25 +89,25 @@ def check := ⟦ -- Walks a KLevel asserting `Param(i)` has `i < bound`. Aiur's `store`/ -- `load` deduplication subsumes Rust's seen-set. fn validate_univ_params_seen(u: KLevel, bound: G) { - match u { - KLevel.Zero => (), - KLevel.Succ(&inner) => validate_univ_params_seen(inner, bound), - KLevel.Max(&a, &b) => + match load(u) { + KLevelNode.Zero => (), + KLevelNode.Succ(inner) => validate_univ_params_seen(inner, bound), + KLevelNode.Max(a, b) => let _ = validate_univ_params_seen(a, bound); validate_univ_params_seen(b, bound), - KLevel.IMax(&a, &b) => + KLevelNode.IMax(a, b) => let _ = validate_univ_params_seen(a, bound); validate_univ_params_seen(b, bound), - KLevel.Param(i) => + KLevelNode.Param(i) => assert_eq!(u32_less_than(i, bound), 1); (), } } - fn validate_univ_params_list(lvls: List‹&KLevel›, bound: G) { + fn validate_univ_params_list(lvls: List‹KLevel›, bound: G) { match load(lvls) { ListNode.Nil => (), - ListNode.Cons(&u, rest) => + ListNode.Cons(u, rest) => let _ = validate_univ_params_seen(u, bound); validate_univ_params_list(rest, bound), } @@ -122,7 +122,7 @@ def check := ⟦ KExprNode.BVar(i) => assert_eq!(u32_less_than(i, depth), 1); (), - KExprNode.Srt(&l) => validate_univ_params_seen(l, bound), + KExprNode.Srt(l) => validate_univ_params_seen(l, bound), KExprNode.Const(idx, lvls) => let ci = load(list_lookup(top, idx)); let expected = const_num_lvls(ci); @@ -219,7 +219,7 @@ def check := ⟦ KConstantInfo.Thm(_, ty, val) => -- Mirror: src/ix/kernel/check.rs:135. Theorem type must be Sort 0. let lvl = k_ensure_sort(ty, store(ListNode.Nil), top, addrs); - assert_eq!(level_equal(load(lvl), KLevel.Zero), 1); + assert_eq!(level_equal(lvl, store(KLevelNode.Zero)), 1); let _ = assert_safety(u, ty, top); let _ = assert_safety(u, val, top); let _ = k_check(val, ty, store(ListNode.Nil), top, addrs); diff --git a/Ix/IxVM/Kernel/DefEq.lean b/Ix/IxVM/Kernel/DefEq.lean index 451c7151c..64725adc3 100644 --- a/Ix/IxVM/Kernel/DefEq.lean +++ b/Ix/IxVM/Kernel/DefEq.lean @@ -134,7 +134,7 @@ def defEq := ⟦ match load(a) { KExprNode.Srt(la) => match load(b) { - KExprNode.Srt(lb) => level_equal(load(la), load(lb)), + KExprNode.Srt(lb) => level_equal(la, lb), _ => 0, }, KExprNode.Lam(ty_a, body_a) => @@ -183,7 +183,7 @@ def defEq := ⟦ match load(sort_w) { KExprNode.Srt(l) => match load(l) { - KLevel.Zero => 1, + KLevelNode.Zero => 1, _ => 0, }, _ => 0, @@ -429,7 +429,7 @@ def defEq := ⟦ match load(a) { KExprNode.Srt(la) => match load(b) { - KExprNode.Srt(lb) => level_equal(load(la), load(lb)), + KExprNode.Srt(lb) => level_equal(la, lb), KExprNode.Lam(ty_b, body_b) => try_eta_expand(ty_b, body_b, a, types, top, addrs), _ => 0, }, @@ -557,7 +557,7 @@ def defEq := ⟦ -- ============================================================================ -- Level list equality. -- ============================================================================ - fn k_is_def_eq_levels(a: List‹&KLevel›, b: List‹&KLevel›) -> G { + fn k_is_def_eq_levels(a: List‹KLevel›, b: List‹KLevel›) -> G { match load(a) { ListNode.Nil => match load(b) { @@ -568,7 +568,7 @@ def defEq := ⟦ match load(b) { ListNode.Nil => 0, ListNode.Cons(lb, rb) => - let l_eq = level_equal(load(la), load(lb)); + let l_eq = level_equal(la, lb); match l_eq { 1 => k_is_def_eq_levels(ra, rb), 0 => 0, @@ -765,8 +765,8 @@ def defEq := ⟦ -- Const-vs-Const spine congruence: same idx, def-eq levels, same arity, -- pairwise def-eq args. Inner of try_lazy_delta_app without the head -- loads (caller already did them). - fn try_const_app_congruence(ai: G, al: List‹&KLevel›, aa: List‹KExpr›, - bi: G, bl: List‹&KLevel›, bb: List‹KExpr›, + fn try_const_app_congruence(ai: G, al: List‹KLevel›, aa: List‹KExpr›, + bi: G, bl: List‹KLevel›, bb: List‹KExpr›, types: List‹KExpr›, top: List‹&KConstantInfo›, addrs: List‹Addr›) -> G { match ai - bi { diff --git a/Ix/IxVM/Kernel/Inductive.lean b/Ix/IxVM/Kernel/Inductive.lean index 50b39f844..1fa5e8dc1 100644 --- a/Ix/IxVM/Kernel/Inductive.lean +++ b/Ix/IxVM/Kernel/Inductive.lean @@ -60,7 +60,7 @@ def inductive_check := ⟦ } -- Each `lvls[i]` must be `Param(expected_start + i)` for i in 0..count. - fn assert_lvls_are_params(lvls: List‹&KLevel›, count: G, idx: G) { + fn assert_lvls_are_params(lvls: List‹KLevel›, count: G, idx: G) { match count { 0 => -- Mirror: src/ix/kernel/inductive.rs:2018: us.len() == ind_lvls. @@ -69,9 +69,9 @@ def inductive_check := ⟦ (), _ => match load(lvls) { - ListNode.Cons(&l, rest) => - match l { - KLevel.Param(i) => + ListNode.Cons(l, rest) => + match load(l) { + KLevelNode.Param(i) => assert_eq!(i, idx); let _ = assert_lvls_are_params(rest, count - 1, idx + 1); (), @@ -113,7 +113,7 @@ def inductive_check := ⟦ match n { 0 => match load(ind_ty) { - KExprNode.Srt(&l) => l, + KExprNode.Srt(l) => l, }, _ => match load(ind_ty) { @@ -134,8 +134,8 @@ def inductive_check := ⟦ types: List‹KExpr›, top: List‹&KConstantInfo›, addrs: List‹Addr›) { -- Skip if inductive is Prop. - match ind_level { - KLevel.Zero => (), + match load(ind_level) { + KLevelNode.Zero => (), _ => check_field_universes_skip_params(ctor_ty, n_params, ind_level, types, top, addrs), } } @@ -160,7 +160,7 @@ def inductive_check := ⟦ match load(ty) { KExprNode.Forall(dom, body) => let dom_level = k_ensure_sort(dom, types, top, addrs); - let ok = level_leq(load(dom_level), ind_level); + let ok = level_leq(dom_level, ind_level); assert_eq!(ok, 1); let types2 = store(ListNode.Cons(dom, types)); check_field_universes_inner(body, ind_level, types2, top, addrs), @@ -568,7 +568,7 @@ def inductive_check := ⟦ match load(ty) { KExprNode.Forall(dom, body) => let lvl = k_ensure_sort(dom, types, top, addrs); - let is_data = 1 - level_equal(load(lvl), KLevel.Zero); + let is_data = 1 - level_equal(lvl, store(KLevelNode.Zero)); let bvar_idx = n_fields - 1 - field_idx; let new_bvars = match is_data { 0 => data_bvars, @@ -621,7 +621,7 @@ def inductive_check := ⟦ -- recursor-param BVars. fn build_motive_type_flat(ind_idx: G, ind_ty: KExpr, n_own_params: G, n_indices: G, - occurrence_us: List‹&KLevel›, + occurrence_us: List‹KLevel›, elim_level: KLevel, n_rec_params: G, is_aux: G, spec_params: List‹KExpr›) -> KExpr { @@ -633,7 +633,7 @@ def inductive_check := ⟦ let with_args = build_major_args_for_member(head, n_rec_params, n_indices, is_aux, spec_params); let major_ty = build_major_indices(with_args, n_indices, 0); - let sort_e = store(KExprNode.Srt(store(elim_level))); + let sort_e = store(KExprNode.Srt(elim_level)); let with_major = store(KExprNode.Forall(major_ty, sort_e)); wrap_foralls(with_major, index_doms) } @@ -754,13 +754,13 @@ def inductive_check := ⟦ } } - -- [Param(start), Param(start+1), ..., Param(start+count-1)] as List‹&KLevel›. - fn build_param_lvls_range(start: G, count: G, i: G) -> List‹&KLevel› { + -- [Param(start), Param(start+1), ..., Param(start+count-1)] as List‹KLevel›. + fn build_param_lvls_range(start: G, count: G, i: G) -> List‹KLevel› { match count - i { 0 => store(ListNode.Nil), _ => store(ListNode.Cons( - store(KLevel.Param(start + i)), + store(KLevelNode.Param(start + i)), build_param_lvls_range(start, count, i + 1))), } } @@ -813,7 +813,7 @@ def inductive_check := ⟦ -- ============================================================================ fn build_minor_at_depth(ind_idx: G, ctor_idx: G, ctor_ty: KExpr, is_aux: G, spec_params: List‹KExpr›, - occurrence_us: List‹&KLevel›, flat_idxs: List‹G›, + occurrence_us: List‹KLevel›, flat_idxs: List‹G›, flat_own_params: List‹G›, n_rec_params: G, n_motives: G, prev_minors: G, motive_base: G, @@ -1106,7 +1106,7 @@ def inductive_check := ⟦ -- to use for the ctor head; flat_idxs is used for rec field detection. fn build_minor_doms(ctor_indices: List‹G›, ind_idx: G, is_aux: G, spec_params: List‹KExpr›, - occurrence_us: List‹&KLevel›, flat_idxs: List‹G›, + occurrence_us: List‹KLevel›, flat_idxs: List‹G›, flat_own_params: List‹G›, n_rec_params: G, n_motives: G, motive_base: G, @@ -1139,7 +1139,7 @@ def inductive_check := ⟦ -- with elim_level + univ_offset shared. Motive j (j>0) lifted by j to -- account for the j prior motives bound between params and motive j -- (mirror src/ix/kernel/inductive.rs:3074-3082). - fn build_all_motives(flat: List‹(G, G, List‹KExpr›, List‹&KLevel›)›, + fn build_all_motives(flat: List‹(G, G, List‹KExpr›, List‹KLevel›)›, n_params: G, ind_lvls: G, elim_level: KLevel, univ_offset: G, n_rec_params: G, @@ -1148,7 +1148,7 @@ def inductive_check := ⟦ univ_offset, n_rec_params, top, 0) } - fn build_all_motives_walk(flat: List‹(G, G, List‹KExpr›, List‹&KLevel›)›, + fn build_all_motives_walk(flat: List‹(G, G, List‹KExpr›, List‹KLevel›)›, n_params: G, ind_lvls: G, elim_level: KLevel, univ_offset: G, n_rec_params: G, @@ -1183,7 +1183,7 @@ def inductive_check := ⟦ -- through so each minor's depth math is correct. flat carries (ind_idx, -- is_aux, spec_params) so aux ctors can substitute spec_params during -- their own-param peel. - fn build_all_minors(flat: List‹(G, G, List‹KExpr›, List‹&KLevel›)›, + fn build_all_minors(flat: List‹(G, G, List‹KExpr›, List‹KLevel›)›, flat_idxs: List‹G›, flat_own_params: List‹G›, n_rec_params: G, n_motives: G, ind_lvls: G, univ_offset: G, motive_base: G, @@ -1245,8 +1245,8 @@ def inductive_check := ⟦ let result_level = get_result_sort_level(ind_ty, self_own_params + n_indices); let is_large = is_large_eliminator(result_level, ctor_indices, top, addrs); let elim_level = match is_large { - 1 => KLevel.Param(0), - 0 => KLevel.Zero, + 1 => store(KLevelNode.Param(0)), + 0 => store(KLevelNode.Zero), }; let univ_offset = is_large; let block_member_idxs = derive_block_member_idxs(primary_ind_idx, top); @@ -1333,7 +1333,7 @@ def inductive_check := ⟦ param_doms: List‹KExpr›, peer_recs: List‹G›, flat_idxs: List‹G›, flat_own_params: List‹G›, is_aux: G, spec_params: List‹KExpr›, - occurrence_us: List‹&KLevel›, + occurrence_us: List‹KLevel›, top: List‹&KConstantInfo›, addrs: List‹Addr›) -> KExpr { let rec_lvls_list = build_rec_lvls(ind_lvls + univ_offset, 0); let ctor_ty_inst = expr_inst_levels(ctor_ty, occurrence_us); @@ -1384,12 +1384,12 @@ def inductive_check := ⟦ } -- Recursor's univ params: [Param(0), ..., Param(total_lvls-1)]. - fn build_rec_lvls(total: G, i: G) -> List‹&KLevel› { + fn build_rec_lvls(total: G, i: G) -> List‹KLevel› { match total - i { 0 => store(ListNode.Nil), _ => store(ListNode.Cons( - store(KLevel.Param(i)), + store(KLevelNode.Param(i)), build_rec_lvls(total, i + 1))), } } @@ -1414,7 +1414,7 @@ def inductive_check := ⟦ field_doms: List‹KExpr›, peer_recs: List‹G›, flat_own_params: List‹G›, n_params: G, n_motives: G, n_minors: G, n_fields: G, - rec_lvls_list: List‹&KLevel›, types: List‹KExpr›, + rec_lvls_list: List‹KLevel›, types: List‹KExpr›, top: List‹&KConstantInfo›, addrs: List‹Addr›, k: G) -> KExpr { match load(rec_indices) { ListNode.Nil => head, @@ -1644,7 +1644,7 @@ def inductive_check := ⟦ match list_length(block_members) - 1 { 0 => let result_level = get_result_sort_level(ind_ty, n_params + n_indices); - match level_equal(result_level, KLevel.Zero) { + match level_equal(result_level, store(KLevelNode.Zero)) { 0 => 0, 1 => match list_length(ctor_indices) - 1 { @@ -1693,8 +1693,8 @@ def inductive_check := ⟦ let result_level = get_result_sort_level(self_ind_ty, self_own_params + self_n_indices); let univ_offset = is_large_eliminator(result_level, self_ctor_indices, top, addrs); let elim_level = match univ_offset { - 1 => KLevel.Param(0), - 0 => KLevel.Zero, + 1 => store(KLevelNode.Param(0)), + 0 => store(KLevelNode.Zero), }; let block_member_idxs = derive_block_member_idxs(ind_idx, top); let flat = build_flat_block(block_member_idxs, univ_offset, top); @@ -1749,7 +1749,7 @@ def inductive_check := ⟦ -- Mirror: src/ix/kernel/inductive.rs:490-601 build_flat_block. fn build_flat_block(block_member_idxs: List‹G›, univ_offset: G, top: List‹&KConstantInfo›) - -> List‹(G, G, List‹KExpr›, List‹&KLevel›)› { + -> List‹(G, G, List‹KExpr›, List‹KLevel›)› { let originals = build_flat_originals(block_member_idxs, univ_offset, top); let nested = gather_block_nested(block_member_idxs, block_member_idxs, top); let auxes = build_flat_auxes(nested); @@ -1758,7 +1758,7 @@ def inductive_check := ⟦ fn build_flat_originals(block_member_idxs: List‹G›, univ_offset: G, top: List‹&KConstantInfo›) - -> List‹(G, G, List‹KExpr›, List‹&KLevel›)› { + -> List‹(G, G, List‹KExpr›, List‹KLevel›)› { match load(block_member_idxs) { ListNode.Nil => store(ListNode.Nil), ListNode.Cons(idx, rest) => @@ -1775,8 +1775,8 @@ def inductive_check := ⟦ } } - fn build_flat_auxes(nested: List‹(G, List‹KExpr›, List‹&KLevel›)›) - -> List‹(G, G, List‹KExpr›, List‹&KLevel›)› { + fn build_flat_auxes(nested: List‹(G, List‹KExpr›, List‹KLevel›)›) + -> List‹(G, G, List‹KExpr›, List‹KLevel›)› { match load(nested) { ListNode.Nil => store(ListNode.Nil), ListNode.Cons(p, rest) => @@ -1789,7 +1789,7 @@ def inductive_check := ⟦ } -- Project per-member ind_idx from flat list. - fn flat_ind_idxs(flat: List‹(G, G, List‹KExpr›, List‹&KLevel›)›) -> List‹G› { + fn flat_ind_idxs(flat: List‹(G, G, List‹KExpr›, List‹KLevel›)›) -> List‹G› { match load(flat) { ListNode.Nil => store(ListNode.Nil), ListNode.Cons(m, rest) => @@ -1801,8 +1801,8 @@ def inductive_check := ⟦ } -- Look up nth flat member. - fn flat_member_at(flat: List‹(G, G, List‹KExpr›, List‹&KLevel›)›, n: G) - -> (G, G, List‹KExpr›, List‹&KLevel›) { + fn flat_member_at(flat: List‹(G, G, List‹KExpr›, List‹KLevel›)›, n: G) + -> (G, G, List‹KExpr›, List‹KLevel›) { match load(flat) { ListNode.Nil => (0, 0, store(ListNode.Nil), store(ListNode.Nil)), ListNode.Cons(m, rest) => @@ -1826,7 +1826,7 @@ def inductive_check := ⟦ } -- For each flat member, look up its own_params from top. - fn flat_own_params_of(flat: List‹(G, G, List‹KExpr›, List‹&KLevel›)›, + fn flat_own_params_of(flat: List‹(G, G, List‹KExpr›, List‹KLevel›)›, top: List‹&KConstantInfo›) -> List‹G› { match load(flat) { ListNode.Nil => store(ListNode.Nil), @@ -1954,7 +1954,7 @@ def inductive_check := ⟦ -- block_idxs, record (ext_idx, spec_params). fn detect_nested_in_orig(orig_idx: G, block_idxs: List‹G›, top: List‹&KConstantInfo›) - -> List‹(G, List‹KExpr›, List‹&KLevel›)› { + -> List‹(G, List‹KExpr›, List‹KLevel›)› { let orig_ci = load(list_lookup(top, orig_idx)); match orig_ci { KConstantInfo.Induct(_, _, n_params, _, ctor_indices, _, _, _, _, _) => @@ -1966,7 +1966,7 @@ def inductive_check := ⟦ fn detect_nested_in_ctors(ctor_indices: List‹G›, n_params: G, block_idxs: List‹G›, top: List‹&KConstantInfo›) - -> List‹(G, List‹KExpr›, List‹&KLevel›)› { + -> List‹(G, List‹KExpr›, List‹KLevel›)› { match load(ctor_indices) { ListNode.Nil => store(ListNode.Nil), ListNode.Cons(ctor_idx, rest) => @@ -1984,7 +1984,7 @@ def inductive_check := ⟦ fn detect_nested_in_field_chain(ty: KExpr, block_idxs: List‹G›, top: List‹&KConstantInfo›) - -> List‹(G, List‹KExpr›, List‹&KLevel›)› { + -> List‹(G, List‹KExpr›, List‹KLevel›)› { match load(ty) { KExprNode.Forall(dom, body) => let from_dom = detect_nested_in_dom(dom, block_idxs, top); @@ -1996,7 +1996,7 @@ def inductive_check := ⟦ fn detect_nested_in_dom(dom: KExpr, block_idxs: List‹G›, top: List‹&KConstantInfo›) - -> List‹(G, List‹KExpr›, List‹&KLevel›)› { + -> List‹(G, List‹KExpr›, List‹KLevel›)› { match peel_leading_foralls(dom) { (_doms, body) => match collect_spine(body) { @@ -2104,7 +2104,7 @@ def inductive_check := ⟦ -- Collect detected nested occurrences across all non-aux originals in block. fn gather_block_nested(walk_idxs: List‹G›, all_block_idxs: List‹G›, top: List‹&KConstantInfo›) - -> List‹(G, List‹KExpr›, List‹&KLevel›)› { + -> List‹(G, List‹KExpr›, List‹KLevel›)› { match load(walk_idxs) { ListNode.Nil => store(ListNode.Nil), ListNode.Cons(idx, rest) => @@ -2120,7 +2120,7 @@ def inductive_check := ⟦ -- Walk auxes in block; for each, assert it matches some nested occurrence. fn validate_auxes_walk(walk_idxs: List‹G›, - nested_list: List‹(G, List‹KExpr›, List‹&KLevel›)›, + nested_list: List‹(G, List‹KExpr›, List‹KLevel›)›, n_block_params: G, block_param_doms: List‹KExpr›, top: List‹&KConstantInfo›) { @@ -2146,7 +2146,7 @@ def inductive_check := ⟦ -- Returns 1 iff aux's ind_ty matches (block_params Pi → ext.ind_ty[α := spec_params]) -- AND ctor count matches AND each ctor ty matches likewise. fn try_match_aux(aux_ind_ty: KExpr, aux_ctor_indices: List‹G›, - nested_list: List‹(G, List‹KExpr›, List‹&KLevel›)›, + nested_list: List‹(G, List‹KExpr›, List‹KLevel›)›, n_block_params: G, block_param_doms: List‹KExpr›, top: List‹&KConstantInfo›) -> G { @@ -2231,7 +2231,7 @@ def inductive_check := ⟦ param_doms: List‹KExpr›, peer_recs: List‹G›, flat_idxs: List‹G›, flat_own_params: List‹G›, is_aux: G, spec_params: List‹KExpr›, - occurrence_us: List‹&KLevel›, + occurrence_us: List‹KLevel›, top: List‹&KConstantInfo›, addrs: List‹Addr›, ctor_pos: G) -> List‹KRecRule› { match load(ctor_indices) { diff --git a/Ix/IxVM/Kernel/Infer.lean b/Ix/IxVM/Kernel/Infer.lean index a911c2407..ef08b7a27 100644 --- a/Ix/IxVM/Kernel/Infer.lean +++ b/Ix/IxVM/Kernel/Infer.lean @@ -71,7 +71,7 @@ def infer := ⟦ -- has to compare `Succ(IMax 0 1)` against `Succ(Succ Zero)` -- structurally and the case-split paths can diverge. KExprNode.Srt(l) => - store(KExprNode.Srt(store(level_reduce(KLevel.Succ(l))))), + store(KExprNode.Srt(level_reduce(store(KLevelNode.Succ(l))))), -- Mirror: src/ix/kernel/check.rs:110-120 universe-arity validation. -- Validates `lvls.len() == num_lvls(ci)`. @@ -107,7 +107,7 @@ def infer := ⟦ let u1 = k_ensure_sort(ty, types, top, addrs); let types2 = store(ListNode.Cons(ty, types)); let u2 = k_ensure_sort(body, types2, top, addrs); - store(KExprNode.Srt(store(level_imax(load(u1), load(u2))))), + store(KExprNode.Srt(level_imax(u1, u2))), KExprNode.Let(ty, val, body) => let _ = k_ensure_sort(ty, types, top, addrs); @@ -194,7 +194,7 @@ def infer := ⟦ } fn k_ensure_sort(e: KExpr, types: List‹KExpr›, - top: List‹&KConstantInfo›, addrs: List‹Addr›) -> &KLevel { + top: List‹&KConstantInfo›, addrs: List‹Addr›) -> KLevel { let ty = k_infer(e, types, top, addrs); -- Mirror: src/ix/kernel/infer.rs:454-478 syntactic Sort fast-path. match load(ty) { @@ -275,7 +275,7 @@ def infer := ⟦ match load(e) { KExprNode.BVar(i) => types_lookup(types, i), KExprNode.Srt(l) => - store(KExprNode.Srt(store(level_reduce(KLevel.Succ(l))))), + store(KExprNode.Srt(level_reduce(store(KLevelNode.Succ(l))))), KExprNode.Const(idx, lvls) => let ci = load(list_lookup(top, idx)); let expected = const_num_lvls(ci); @@ -304,7 +304,7 @@ def infer := ⟦ let u1 = k_ensure_sort_only(ty, types, top, addrs); let types2 = store(ListNode.Cons(ty, types)); let u2 = k_ensure_sort_only(body, types2, top, addrs); - store(KExprNode.Srt(store(level_imax(load(u1), load(u2))))), + store(KExprNode.Srt(level_imax(u1, u2))), KExprNode.Let(_, val, body) => let body_substed = expr_inst1(body, val, 0); k_infer_only(body_substed, types, top, addrs), @@ -344,7 +344,7 @@ def infer := ⟦ } fn k_ensure_sort_only(e: KExpr, types: List‹KExpr›, - top: List‹&KConstantInfo›, addrs: List‹Addr›) -> &KLevel { + top: List‹&KConstantInfo›, addrs: List‹Addr›) -> KLevel { let ty = k_infer_only(e, types, top, addrs); match load(ty) { KExprNode.Srt(l) => l, @@ -447,7 +447,7 @@ def infer := ⟦ 0 => (), _ => let lvl = k_ensure_sort(dom, types, top, addrs); - match level_equal(load(lvl), KLevel.Zero) { + match level_equal(lvl, store(KLevelNode.Zero)) { 1 => (), _ => -- data field; body must have no loose bvars. @@ -475,13 +475,13 @@ def infer := ⟦ -- Mirror: src/ix/kernel/infer.rs:488-520 inductive_app_is_prop. -- Returns 1 iff the inductive lives in Prop (peeled past params + indices, -- result sort = Zero). - fn is_inductive_prop(ind_ty: KExpr, lvls: List‹&KLevel›, n_skip: G, + fn is_inductive_prop(ind_ty: KExpr, lvls: List‹KLevel›, n_skip: G, types: List‹KExpr›, top: List‹&KConstantInfo›, addrs: List‹Addr›) -> G { let ind_ty_inst = expr_inst_levels(ind_ty, lvls); let result = peel_n_alls_whnf(ind_ty_inst, n_skip, types, top, addrs); match load(result) { - KExprNode.Srt(l) => level_equal(load(l), KLevel.Zero), + KExprNode.Srt(l) => level_equal(l, store(KLevelNode.Zero)), _ => 0, } } @@ -495,7 +495,7 @@ def infer := ⟦ 0 => (), _ => let lvl = k_ensure_sort(dom, types, top, addrs); - assert_eq!(level_equal(load(lvl), KLevel.Zero), 1); + assert_eq!(level_equal(lvl, store(KLevelNode.Zero)), 1); (), } } diff --git a/Ix/IxVM/Kernel/Levels.lean b/Ix/IxVM/Kernel/Levels.lean index 403484feb..5ff68e3ad 100644 --- a/Ix/IxVM/Kernel/Levels.lean +++ b/Ix/IxVM/Kernel/Levels.lean @@ -15,43 +15,43 @@ src/ix/kernel/expr.rs. Self-contained; new kernel modules def levels := ⟦ fn level_is_not_zero(l: KLevel) -> G { - match l { - KLevel.Zero => 0, - KLevel.Param(_) => 0, - KLevel.Succ(_) => 1, - KLevel.Max(&a, &b) => match (level_is_not_zero(a), level_is_not_zero(b)) { + match load(l) { + KLevelNode.Zero => 0, + KLevelNode.Param(_) => 0, + KLevelNode.Succ(_) => 1, + KLevelNode.Max(a, b) => match (level_is_not_zero(a), level_is_not_zero(b)) { (0, 0) => 0, _ => 1, }, - KLevel.IMax(_, &b) => level_is_not_zero(b), + KLevelNode.IMax(_, b) => level_is_not_zero(b), } } fn level_eq(a: KLevel, b: KLevel) -> G { - match a { - KLevel.Zero => - match b { - KLevel.Zero => 1, + match load(a) { + KLevelNode.Zero => + match load(b) { + KLevelNode.Zero => 1, _ => 0, }, - KLevel.Succ(&a1) => - match b { - KLevel.Succ(&b1) => level_eq(a1, b1), + KLevelNode.Succ(a1) => + match load(b) { + KLevelNode.Succ(b1) => level_eq(a1, b1), _ => 0, }, - KLevel.Max(&a1, &a2) => - match b { - KLevel.Max(&b1, &b2) => level_eq(a1, b1) * level_eq(a2, b2), + KLevelNode.Max(a1, a2) => + match load(b) { + KLevelNode.Max(b1, b2) => level_eq(a1, b1) * level_eq(a2, b2), _ => 0, }, - KLevel.IMax(&a1, &a2) => - match b { - KLevel.IMax(&b1, &b2) => level_eq(a1, b1) * level_eq(a2, b2), + KLevelNode.IMax(a1, a2) => + match load(b) { + KLevelNode.IMax(b1, b2) => level_eq(a1, b1) * level_eq(a2, b2), _ => 0, }, - KLevel.Param(i) => - match b { - KLevel.Param(j) => eq_zero(i - j), + KLevelNode.Param(i) => + match load(b) { + KLevelNode.Param(j) => eq_zero(i - j), _ => 0, }, } @@ -337,13 +337,13 @@ def levels := ⟦ -- replicate the aux IMax-shape cases verbatim, as in level.rs). fn normalize_aux(l: KLevel, path: List‹G›, k: G, acc: List‹&NLEntry›) -> List‹&NLEntry› { - match l { - KLevel.Zero => nl_add_const(acc, path, k), - KLevel.Succ(&inner) => normalize_aux(inner, path, k + 1, acc), - KLevel.Max(&a, &b) => + match load(l) { + KLevelNode.Zero => nl_add_const(acc, path, k), + KLevelNode.Succ(inner) => normalize_aux(inner, path, k + 1, acc), + KLevelNode.Max(a, b) => normalize_aux(b, path, k, normalize_aux(a, path, k, acc)), - KLevel.IMax(&u, &b) => normalize_imax_dispatch(u, b, path, k, acc), - KLevel.Param(idx) => + KLevelNode.IMax(u, b) => normalize_imax_dispatch(u, b, path, k, acc), + KLevelNode.Param(idx) => match glist_ordered_insert(idx, path) { (1, new_path) => nl_add_var(nl_add_const(acc, path, k), new_path, idx, k), @@ -360,19 +360,19 @@ def levels := ⟦ -- imax = max; max/imax distribute; param conditions the path. fn normalize_imax_dispatch(a: KLevel, b: KLevel, path: List‹G›, k: G, acc: List‹&NLEntry›) -> List‹&NLEntry› { - match b { - KLevel.Zero => nl_add_const(acc, path, k), - KLevel.Succ(&v) => + match load(b) { + KLevelNode.Zero => nl_add_const(acc, path, k), + KLevelNode.Succ(v) => normalize_aux(v, path, k + 1, normalize_aux(a, path, k, acc)), - KLevel.Max(&v, &w) => + KLevelNode.Max(v, w) => -- imax(a, max(v, w)) = max(imax(a, v), imax(a, w)) normalize_imax_dispatch(a, w, path, k, normalize_imax_dispatch(a, v, path, k, acc)), - KLevel.IMax(&v, &w) => + KLevelNode.IMax(v, w) => -- imax(a, imax(v, w)) = max(imax(a, w), imax(v, w)) normalize_imax_dispatch(v, w, path, k, normalize_imax_dispatch(a, w, path, k, acc)), - KLevel.Param(idx) => + KLevelNode.Param(idx) => match glist_ordered_insert(idx, path) { (1, new_path) => -- param(idx) = 0 branch: imax(a, 0) = 0, contributing k. @@ -616,8 +616,8 @@ def levels := ⟦ match level_eq(a, b) { 1 => 1, 0 => - match a { - KLevel.Zero => 1, + match load(a) { + KLevelNode.Zero => 1, _ => nl_le(level_normalize(a), level_normalize(b)), }, } @@ -635,23 +635,23 @@ def levels := ⟦ } fn level_max(a: KLevel, b: KLevel) -> KLevel { - match a { - KLevel.Zero => b, + match load(a) { + KLevelNode.Zero => b, _ => - match b { - KLevel.Zero => a, + match load(b) { + KLevelNode.Zero => a, _ => let eq = level_eq(a, b); match eq { 1 => a, 0 => - match a { - KLevel.Succ(&a1) => - match b { - KLevel.Succ(&b1) => KLevel.Succ(store(level_max(a1, b1))), - _ => KLevel.Max(store(a), store(b)), + match load(a) { + KLevelNode.Succ(a1) => + match load(b) { + KLevelNode.Succ(b1) => store(KLevelNode.Succ(level_max(a1, b1))), + _ => store(KLevelNode.Max(a, b)), }, - _ => KLevel.Max(store(a), store(b)), + _ => store(KLevelNode.Max(a, b)), }, }, }, @@ -659,21 +659,21 @@ def levels := ⟦ } fn level_imax(a: KLevel, b: KLevel) -> KLevel { - match b { - KLevel.Zero => KLevel.Zero, - KLevel.Succ(_) => level_max(a, b), + match load(b) { + KLevelNode.Zero => store(KLevelNode.Zero), + KLevelNode.Succ(_) => level_max(a, b), _ => let not_zero = level_is_not_zero(b); match not_zero { 1 => level_max(a, b), 0 => - match a { - KLevel.Zero => b, + match load(a) { + KLevelNode.Zero => b, _ => let eq = level_eq(a, b); match eq { 1 => a, - 0 => KLevel.IMax(store(a), store(b)), + 0 => store(KLevelNode.IMax(a, b)), }, }, }, @@ -681,38 +681,38 @@ def levels := ⟦ } fn level_reduce(l: KLevel) -> KLevel { - match l { - KLevel.Zero => KLevel.Zero, - KLevel.Param(i) => KLevel.Param(i), - KLevel.Succ(&u) => KLevel.Succ(store(level_reduce(u))), - KLevel.Max(&a, &b) => level_max(level_reduce(a), level_reduce(b)), - KLevel.IMax(&a, &b) => level_imax(level_reduce(a), level_reduce(b)), + match load(l) { + KLevelNode.Zero => store(KLevelNode.Zero), + KLevelNode.Param(i) => store(KLevelNode.Param(i)), + KLevelNode.Succ(u) => store(KLevelNode.Succ(level_reduce(u))), + KLevelNode.Max(a, b) => level_max(level_reduce(a), level_reduce(b)), + KLevelNode.IMax(a, b) => level_imax(level_reduce(a), level_reduce(b)), } } - fn level_inst_params(l: KLevel, params: List‹&KLevel›) -> KLevel { - match l { - KLevel.Zero => KLevel.Zero, - KLevel.Succ(&u) => KLevel.Succ(store(level_inst_params(u, params))), - KLevel.Max(&a, &b) => + fn level_inst_params(l: KLevel, params: List‹KLevel›) -> KLevel { + match load(l) { + KLevelNode.Zero => store(KLevelNode.Zero), + KLevelNode.Succ(u) => store(KLevelNode.Succ(level_inst_params(u, params))), + KLevelNode.Max(a, b) => level_max(level_inst_params(a, params), level_inst_params(b, params)), - KLevel.IMax(&a, &b) => + KLevelNode.IMax(a, b) => level_imax(level_inst_params(a, params), level_inst_params(b, params)), - KLevel.Param(i) => load(list_lookup(params, i)), + KLevelNode.Param(i) => list_lookup(params, i), } } - fn level_list_inst(lvls: List‹&KLevel›, params: List‹&KLevel›) -> List‹&KLevel› { + fn level_list_inst(lvls: List‹KLevel›, params: List‹KLevel›) -> List‹KLevel› { match load(lvls) { ListNode.Nil => store(ListNode.Nil), - ListNode.Cons(&l, rest) => + ListNode.Cons(l, rest) => store(ListNode.Cons( - store(level_inst_params(l, params)), + level_inst_params(l, params), level_list_inst(rest, params))), } } - fn expr_inst_levels(e: KExpr, params: List‹&KLevel›) -> KExpr { + fn expr_inst_levels(e: KExpr, params: List‹KLevel›) -> KExpr { -- Fast path: empty param list = identity. Common when caller's lvls -- list is Nil (constants with no universe params). match load(params) { @@ -721,11 +721,11 @@ def levels := ⟦ } } - fn expr_inst_levels_walk(e: KExpr, params: List‹&KLevel›) -> KExpr { + fn expr_inst_levels_walk(e: KExpr, params: List‹KLevel›) -> KExpr { match load(e) { KExprNode.BVar(i) => store(KExprNode.BVar(i)), - KExprNode.Srt(&l) => - store(KExprNode.Srt(store(level_inst_params(l, params)))), + KExprNode.Srt(l) => + store(KExprNode.Srt(level_inst_params(l, params))), KExprNode.Const(idx, lvls) => store(KExprNode.Const(idx, level_list_inst(lvls, params))), KExprNode.App(f, a) => diff --git a/Ix/IxVM/Kernel/Primitive.lean b/Ix/IxVM/Kernel/Primitive.lean index 2254f08b4..4fc70c9cd 100644 --- a/Ix/IxVM/Kernel/Primitive.lean +++ b/Ix/IxVM/Kernel/Primitive.lean @@ -1942,7 +1942,7 @@ def primitive := ⟦ -- first arg. Requires `types` to be the local context so k_infer is -- valid under binders. fn try_reduce_decidable(head_addr: Addr, head_idx: G, - head_lvls: List‹&KLevel›, + head_lvls: List‹KLevel›, spine: List‹KExpr›, types: List‹KExpr›, top: List‹&KConstantInfo›, @@ -2015,7 +2015,7 @@ def primitive := ⟦ -- For Int.decEq/decLe/decLt: whnf both args, extract Int literals, -- rebuild canonical form `App(Const(int_dec_*), int_of_nat n, int_neg_succ k, ...)`. -- Bails if both args already canonical (no normalization needed). - fn try_normalize_int_decidable(head_idx: G, head_lvls: List‹&KLevel›, + fn try_normalize_int_decidable(head_idx: G, head_lvls: List‹KLevel›, spine: List‹KExpr›, types: List‹KExpr›, top: List‹&KConstantInfo›, addrs: List‹Addr›) -> (G, KExpr) { @@ -2036,7 +2036,7 @@ def primitive := ⟦ } } - fn normalize_int_dec_rebuild(head_idx: G, head_lvls: List‹&KLevel›, + fn normalize_int_dec_rebuild(head_idx: G, head_lvls: List‹KLevel›, spine: List‹KExpr›, a0: KExpr, a1: KExpr, types: List‹KExpr›, top: List‹&KConstantInfo›, addrs: List‹Addr›) -> (G, KExpr) { @@ -2066,7 +2066,7 @@ def primitive := ⟦ } fn decidable_dispatch(is_dec_le: G, is_dec_eq: G, is_dec_lt: G, - head_idx: G, head_lvls: List‹&KLevel›, + head_idx: G, head_lvls: List‹KLevel›, spine: List‹KExpr›, types: List‹KExpr›, top: List‹&KConstantInfo›, addrs: List‹Addr›) -> (G, KExpr) { @@ -2103,7 +2103,7 @@ def primitive := ⟦ } fn decidable_dispatch_le_eq(is_dec_le: G, is_dec_eq: G, - head_idx: G, head_lvls: List‹&KLevel›, + head_idx: G, head_lvls: List‹KLevel›, spine: List‹KExpr›, types: List‹KExpr›, top: List‹&KConstantInfo›, addrs: List‹Addr›) -> (G, KExpr) { @@ -2133,7 +2133,7 @@ def primitive := ⟦ -- k_infer over the original call expression in `decidable_finish`. fn decidable_build_proof(is_dec_le: G, is_dec_eq: G, verdict: G, n_e: KExpr, m_e: KExpr, - head_idx: G, head_lvls: List‹&KLevel›, + head_idx: G, head_lvls: List‹KLevel›, spine: List‹KExpr›, types: List‹KExpr›, top: List‹&KConstantInfo›, @@ -2154,7 +2154,7 @@ def primitive := ⟦ match bool_lit_pair { (0, _) => (0, store(KExprNode.BVar(0))), (1, bool_lit_idx) => - let one_lvl = store(KLevel.Succ(store(KLevel.Zero))); + let one_lvl = store(KLevelNode.Succ(store(KLevelNode.Zero))); let lvls = store(ListNode.Cons(one_lvl, store(ListNode.Nil))); let eq_refl_const = store(KExprNode.Const(eq_refl_idx, lvls)); let bool_const = store(KExprNode.Const(bool_idx, store(ListNode.Nil))); @@ -2199,7 +2199,7 @@ def primitive := ⟦ } fn decidable_finish(verdict: G, proof: KExpr, head_idx: G, - head_lvls: List‹&KLevel›, spine: List‹KExpr›, + head_lvls: List‹KLevel›, spine: List‹KExpr›, types: List‹KExpr›, top: List‹&KConstantInfo›, addrs: List‹Addr›) -> (G, KExpr) { let dec_addr = match verdict { @@ -2419,7 +2419,7 @@ def primitive := ⟦ match find_addr_idx_safe(string_of_list_addr(), addrs, 0) { (0, _) => (0, store(KExprNode.BVar(0))), (1, str_idx) => - let zero_lvl = store(KLevel.Zero); + let zero_lvl = store(KLevelNode.Zero); let ulvls = store(ListNode.Cons(zero_lvl, store(ListNode.Nil))); let nil_const = store(KExprNode.Const(nil_idx, ulvls)); let cons_const = store(KExprNode.Const(cons_idx, ulvls)); diff --git a/Ix/IxVM/Kernel/Subst.lean b/Ix/IxVM/Kernel/Subst.lean index 17bc657fd..c97b9375d 100644 --- a/Ix/IxVM/Kernel/Subst.lean +++ b/Ix/IxVM/Kernel/Subst.lean @@ -25,7 +25,7 @@ Aiur memoization caches calls automatically; no explicit cache table. `KExprNode` lives in `Ix/IxVM/KernelTypes.lean`: ``` enum KExprNode { - BVar(G), Srt(&KLevel), Const(G, List‹&KLevel›), + BVar(G), Srt(KLevel), Const(G, List‹KLevel›), App(KExpr, KExpr), Lam(KExpr, KExpr), Forall(KExpr, KExpr), Let(KExpr, KExpr, KExpr), Lit(KLiteral), Proj(G, G, KExpr), } diff --git a/Ix/IxVM/Kernel/Whnf.lean b/Ix/IxVM/Kernel/Whnf.lean index c43f40f49..639f82df3 100644 --- a/Ix/IxVM/Kernel/Whnf.lean +++ b/Ix/IxVM/Kernel/Whnf.lean @@ -215,7 +215,7 @@ def whnf := ⟦ -- decidable, in order. Returns (1, reduced) on the first family that matches -- and reduces, else (0, _). Factored out so `prim_any_addr` can gate the -- whole chain for non-primitive heads in one shot. - fn try_address_primitives(head_addr: Addr, idx: G, lvls: List‹&KLevel›, + fn try_address_primitives(head_addr: Addr, idx: G, lvls: List‹KLevel›, spine: List‹KExpr›, types: List‹KExpr›, top: List‹&KConstantInfo›, addrs: List‹Addr›) -> (G, KExpr) { match try_nat_dispatch(head_addr, spine, types, top, addrs) { @@ -243,7 +243,7 @@ def whnf := ⟦ -- Const-head WHNF dispatch, split out of `whnf_with_spine` (see its Const arm). -- `head` is the original `Const(idx, lvls)` KExpr, passed for the stuck -- `apply_spine(head, spine)` fallbacks. - fn whnf_const_head(idx: G, lvls: List‹&KLevel›, head: KExpr, spine: List‹KExpr›, + fn whnf_const_head(idx: G, lvls: List‹KLevel›, head: KExpr, spine: List‹KExpr›, types: List‹KExpr›, top: List‹&KConstantInfo›, addrs: List‹Addr›) -> KExpr { let head_addr = list_lookup(addrs, idx); let ci = load(list_lookup(top, idx)); @@ -400,7 +400,7 @@ def whnf := ⟦ -- The difference from `whnf_const_head`: Defn arm returns stuck instead of -- unfolding. Iota, quot, primitives, proj-defs still apply. - fn whnf_nd_const_head(idx: G, lvls: List‹&KLevel›, head: KExpr, spine: List‹KExpr›, + fn whnf_nd_const_head(idx: G, lvls: List‹KLevel›, head: KExpr, spine: List‹KExpr›, types: List‹KExpr›, top: List‹&KConstantInfo›, addrs: List‹Addr›) -> KExpr { let head_addr = list_lookup(addrs, idx); let ci = load(list_lookup(top, idx)); @@ -467,7 +467,7 @@ def whnf := ⟦ -- ============================================================================ -- Iota (recursor on ctor) -- ============================================================================ - fn try_iota(lvls: List‹&KLevel›, spine: List‹KExpr›, + fn try_iota(lvls: List‹KLevel›, spine: List‹KExpr›, num_lvls: G, num_params: G, num_indices: G, num_motives: G, num_minors: G, rules: List‹KRecRule›, k_flag: G, types: List‹KExpr›, @@ -573,7 +573,7 @@ def whnf := ⟦ } } - fn try_iota_with_major(lvls: List‹&KLevel›, spine: List‹KExpr›, + fn try_iota_with_major(lvls: List‹KLevel›, spine: List‹KExpr›, num_params: G, num_motives: G, num_minors: G, major_idx: G, rules: List‹KRecRule›, k_flag: G, types: List‹KExpr›, @@ -754,7 +754,7 @@ def whnf := ⟦ fn try_struct_eta_iota(spine: List‹KExpr›, num_params: G, num_motives: G, num_minors: G, major_idx: G, rules: List‹KRecRule›, - lvls: List‹&KLevel›, types: List‹KExpr›, + lvls: List‹KLevel›, types: List‹KExpr›, top: List‹&KConstantInfo›, addrs: List‹Addr›) -> (G, KExpr) { let n_rules = list_length(rules); match n_rules { @@ -976,10 +976,10 @@ def whnf := ⟦ } } - fn ensure_sort_post_whnf(e: KExpr) -> (G, &KLevel) { + fn ensure_sort_post_whnf(e: KExpr) -> (G, KLevel) { match load(e) { KExprNode.Srt(l) => (1, l), - _ => (0, store(KLevel.Zero)), + _ => (0, store(KLevelNode.Zero)), } } diff --git a/Ix/IxVM/KernelTypes.lean b/Ix/IxVM/KernelTypes.lean index b4a57b34f..9f0151cc2 100644 --- a/Ix/IxVM/KernelTypes.lean +++ b/Ix/IxVM/KernelTypes.lean @@ -10,14 +10,16 @@ def kernelTypes := ⟦ -- Universe Levels -- ============================================================================ - enum KLevel { + enum KLevelNode { Zero, - Succ(&KLevel), - Max(&KLevel, &KLevel), - IMax(&KLevel, &KLevel), + Succ(KLevel), + Max(KLevel, KLevel), + IMax(KLevel, KLevel), Param(G) } + type KLevel = &KLevelNode + -- ============================================================================ -- Literals -- ============================================================================ @@ -38,8 +40,8 @@ def kernelTypes := ⟦ enum KExprNode { BVar(G), - Srt(&KLevel), - Const(G, List‹&KLevel›), + Srt(KLevel), + Const(G, List‹KLevel›), App(KExpr, KExpr), Lam(KExpr, KExpr), Forall(KExpr, KExpr), @@ -73,19 +75,19 @@ def kernelTypes := ⟦ -- ============================================================================ enum KValNode { - Srt(&KLevel), + Srt(KLevel), Lit(KLiteral), Lam(KVal, KExpr, KValEnv), Pi(KVal, KExpr, KValEnv), - Ctor(G, List‹&KLevel›, G, List‹KVal›), + Ctor(G, List‹KLevel›, G, List‹KVal›), FVar(G, KVal, List‹KVal›), - Axiom(G, List‹&KLevel›, List‹KVal›), - Defn(G, List‹&KLevel›, List‹KVal›), - Thm(G, List‹&KLevel›, List‹KVal›), - Opaque(G, List‹&KLevel›, List‹KVal›), - Quot(G, List‹&KLevel›, List‹KVal›), - Induct(G, List‹&KLevel›, List‹KVal›), - Rec(G, List‹&KLevel›, List‹KVal›), + Axiom(G, List‹KLevel›, List‹KVal›), + Defn(G, List‹KLevel›, List‹KVal›), + Thm(G, List‹KLevel›, List‹KVal›), + Opaque(G, List‹KLevel›, List‹KVal›), + Quot(G, List‹KLevel›, List‹KVal›), + Induct(G, List‹KLevel›, List‹KVal›), + Rec(G, List‹KLevel›, List‹KVal›), Proj(G, G, KVal, List‹KVal›), Thunk(KExpr, KValEnv) } diff --git a/Tests/Ix/IxVM.lean b/Tests/Ix/IxVM.lean index c915d34ac..e4dce3a9d 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_476), - ("HEq.rec", 2_678_518), - ("Eq.rec", 2_573_362), - ("Nat", 1_859_043), - ("Nat.add", 12_940_971), - ("Nat.add_comm", 54_034_851), - ("Nat.decEq", 68_193_672), - ("Nat.decLe", 189_689_247), - ("Nat.sub_le_of_le_add", 510_810_753), + ("HEq", 1_713_377), + ("HEq.rec", 2_673_812), + ("Eq.rec", 2_569_093), + ("Nat", 1_856_206), + ("Nat.add", 12_913_896), + ("Nat.add_comm", 53_941_716), + ("Nat.decEq", 68_096_944), + ("Nat.decLe", 189_429_058), + ("Nat.sub_le_of_le_add", 510_307_972), -- Newly-unlocked targets (level_leq Géran normalize). - ("Trans.mk", 2_858_098), - ("Array.append_assoc", 2_537_268_602), - ("Vector.append", 2_607_707_384), + ("Trans.mk", 2_846_339), + ("Array.append_assoc", 2_533_794_863), + ("Vector.append", 2_604_106_735), -- Primitive reduction theorems (`IxVMPrim`) - ("IxVMPrim.nat_add_lit", 27_956_627), - ("IxVMPrim.nat_sub_lit", 33_564_651), - ("IxVMPrim.nat_mul_lit", 24_539_380), - ("IxVMPrim.nat_mul_big", 24_041_970), - ("IxVMPrim.nat_div_lit", 363_760_965), - ("IxVMPrim.nat_mod_lit", 372_452_500), - ("IxVMPrim.nat_succ_lit", 7_303_982), - ("IxVMPrim.nat_pred_lit", 14_675_191), - ("IxVMPrim.nat_gcd_lit", 599_734_613), - ("IxVMPrim.nat_land_lit", 1_009_577_758), - ("IxVMPrim.nat_lor_lit", 1_010_380_511), - ("IxVMPrim.nat_xor_lit", 1_019_001_840), - ("IxVMPrim.nat_shl_lit", 34_655_734), - ("IxVMPrim.nat_shr_lit", 369_099_356), - ("IxVMPrim.nat_pow_big", 71_540_935), - ("IxVMPrim.nat_beq_lit", 24_050_432), - ("IxVMPrim.nat_ble_lit", 22_378_650), - ("IxVMPrim.nat_dec_le", 196_221_114), - ("IxVMPrim.nat_dec_lt", 200_167_450), - ("IxVMPrim.nat_dec_eq", 81_855_497), - ("IxVMPrim.str_size_lit", 716_747_374), - ("IxVMPrim.bv_to_nat_lit", 571_385_143), + ("IxVMPrim.nat_add_lit", 27_892_351), + ("IxVMPrim.nat_sub_lit", 33_496_649), + ("IxVMPrim.nat_mul_lit", 24_496_901), + ("IxVMPrim.nat_mul_big", 23_999_554), + ("IxVMPrim.nat_div_lit", 363_376_868), + ("IxVMPrim.nat_mod_lit", 372_058_694), + ("IxVMPrim.nat_succ_lit", 7_291_627), + ("IxVMPrim.nat_pred_lit", 14_654_021), + ("IxVMPrim.nat_gcd_lit", 599_139_076), + ("IxVMPrim.nat_land_lit", 1_008_587_524), + ("IxVMPrim.nat_lor_lit", 1_009_390_333), + ("IxVMPrim.nat_xor_lit", 1_017_980_364), + ("IxVMPrim.nat_shl_lit", 34_588_323), + ("IxVMPrim.nat_shr_lit", 368_712_426), + ("IxVMPrim.nat_pow_big", 71_440_452), + ("IxVMPrim.nat_beq_lit", 24_003_617), + ("IxVMPrim.nat_ble_lit", 22_333_231), + ("IxVMPrim.nat_dec_le", 195_956_041), + ("IxVMPrim.nat_dec_lt", 199_899_015), + ("IxVMPrim.nat_dec_eq", 81_741_042), + ("IxVMPrim.str_size_lit", 715_801_486), + ("IxVMPrim.bv_to_nat_lit", 570_773_030), -- Mutual block + multi-member recursors - ("IxVMInd.Even", 25_849_023), - ("IxVMInd.Odd", 25_609_442), - ("IxVMInd.Even.rec", 31_420_238), - ("IxVMInd.Odd.rec", 31_419_335), + ("IxVMInd.Even", 25_782_173), + ("IxVMInd.Odd", 25_542_593), + ("IxVMInd.Even.rec", 31_350_868), + ("IxVMInd.Odd.rec", 31_349_966), -- Nested inductive + aux recursor (Tree.mk : List Tree → Tree) - ("IxVMInd.Tree", 2_640_146), - ("IxVMInd.Tree.rec", 4_865_455), + ("IxVMInd.Tree", 2_634_029), + ("IxVMInd.Tree.rec", 4_857_081), -- Edge cases from prelude - ("String.Internal.append", 708_226_297), - ("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 1_064_618_151), + ("String.Internal.append", 707_266_965), + ("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 1_063_187_671), ] private def nameOfString (str : String) : Lean.Name :=