diff --git a/Ix/IxVM/Convert.lean b/Ix/IxVM/Convert.lean index 05b0e80e..4917ec0f 100644 --- a/Ix/IxVM/Convert.lean +++ b/Ix/IxVM/Convert.lean @@ -136,14 +136,14 @@ def convert := ⟦ } fn convert_expr( - e: Expr, + e: &Expr, sharing: List‹&Expr›, ref_idxs: List‹G›, recur_idxs: List‹G›, lit_blobs: List‹ByteStream›, univs: List‹&Univ› ) -> KExpr { - match e { + match load(e) { Expr.Srt(univ_idx) => let u = load(list_lookup_u64(univs, univ_idx)); store(KExprNode.Srt(store(convert_univ(u)))), @@ -161,7 +161,7 @@ def convert := ⟦ let levels = convert_univ_idxs(univ_idxs, univs); store(KExprNode.Const(const_idx, levels)), - Expr.Prj(type_ref_idx, field_idx, &inner) => + Expr.Prj(type_ref_idx, field_idx, inner) => let type_idx = list_lookup(ref_idxs, flatten_u64(type_ref_idx)); store(KExprNode.Proj( type_idx, @@ -177,34 +177,33 @@ def convert := ⟦ let limbs = bytes_to_limbs(bs); store(KExprNode.Lit(KLiteral.Nat(limbs))), - Expr.App(&f, &a) => + Expr.App(f, a) => store(KExprNode.App( convert_expr(f, sharing, ref_idxs, recur_idxs, lit_blobs, univs), convert_expr(a, sharing, ref_idxs, recur_idxs, lit_blobs, univs))), - Expr.Lam(&ty, &body) => + Expr.Lam(ty, body) => store(KExprNode.Lam( convert_expr(ty, sharing, ref_idxs, recur_idxs, lit_blobs, univs), convert_expr(body, sharing, ref_idxs, recur_idxs, lit_blobs, univs))), - Expr.All(&ty, &body) => + Expr.All(ty, body) => store(KExprNode.Forall( convert_expr(ty, sharing, ref_idxs, recur_idxs, lit_blobs, univs), convert_expr(body, sharing, ref_idxs, recur_idxs, lit_blobs, univs))), - Expr.Let(_, &ty, &val, &body) => + Expr.Let(_, ty, val, body) => store(KExprNode.Let( convert_expr(ty, sharing, ref_idxs, recur_idxs, lit_blobs, univs), convert_expr(val, sharing, ref_idxs, recur_idxs, lit_blobs, univs), convert_expr(body, sharing, ref_idxs, recur_idxs, lit_blobs, univs))), Expr.Share(idx) => - let shared = load(list_lookup_u64(sharing, idx)); - convert_expr(shared, sharing, ref_idxs, recur_idxs, lit_blobs, univs), + convert_expr(list_lookup_u64(sharing, idx), sharing, ref_idxs, recur_idxs, lit_blobs, univs), } } - fn ctx_convert_expr(e: Expr, ctx: ConvertCtx) -> KExpr { + 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), @@ -226,7 +225,7 @@ def convert := ⟦ ListNode.Nil => store(ListNode.Nil), ListNode.Cons(rule, rest_rules) => match rule { - RecursorRule.Mk(nfields, &rhs) => + RecursorRule.Mk(nfields, rhs) => match load(rule_ctor_idxs) { ListNode.Cons(ctor_idx, rest_ctor_idxs) => let krhs = ctx_convert_expr(rhs, ctx); @@ -245,7 +244,7 @@ def convert := ⟦ fn convert_definition(d: Definition, ctx: ConvertCtx, hint: G) -> KConstantInfo { match d { - Definition.Mk(kind, safety, lvls, &typ, &value) => + Definition.Mk(kind, safety, lvls, typ, value) => let ktyp = ctx_convert_expr(typ, ctx); let kval = ctx_convert_expr(value, ctx); match kind { @@ -266,7 +265,7 @@ def convert := ⟦ fn convert_axiom(a: Axiom, ctx: ConvertCtx) -> KConstantInfo { match a { - Axiom.Mk(is_unsafe, lvls, &typ) => + Axiom.Mk(is_unsafe, lvls, typ) => let ktyp = ctx_convert_expr(typ, ctx); KConstantInfo.Axiom(flatten_u64(lvls), ktyp, is_unsafe), } @@ -274,7 +273,7 @@ def convert := ⟦ fn convert_quotient(q: Quotient, ctx: ConvertCtx) -> KConstantInfo { match q { - Quotient.Mk(kind, lvls, &typ) => + Quotient.Mk(kind, lvls, typ) => let ktyp = ctx_convert_expr(typ, ctx); KConstantInfo.Quot(flatten_u64(lvls), ktyp, kind), } @@ -283,7 +282,7 @@ def convert := ⟦ 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) => + 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( @@ -296,7 +295,7 @@ def convert := ⟦ 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, _) => + 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), @@ -306,7 +305,7 @@ def convert := ⟦ fn convert_constructor(c: Constructor, ctx: ConvertCtx, induct_idx: G) -> KConstantInfo { match c { - Constructor.Mk(is_unsafe, lvls, cidx, params, fields, &typ) => + 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), diff --git a/Ix/IxVM/Ingress.lean b/Ix/IxVM/Ingress.lean index 6d8cb074..6630cc33 100644 --- a/Ix/IxVM/Ingress.lean +++ b/Ix/IxVM/Ingress.lean @@ -103,37 +103,32 @@ def ingress := ⟦ -- 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_set: RBTreeMap‹G›) -> List‹ByteStream› { + 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_set); + 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_set))), + store(ListNode.Cons(bs, build_lit_blobs(rest, addr_pos_map))), 0 => - store(ListNode.Cons(store(ListNode.Nil), build_lit_blobs(rest, addr_set))), + store(ListNode.Cons(store(ListNode.Nil), build_lit_blobs(rest, addr_pos_map))), }, } } - -- Check if an address is a blob: it's a blob if it's NOT in the constant address set. - -- Blob addresses and constant addresses are different by design (different hash preimage structures). - -- O(log N) tree lookup replaces the prior O(N) linear scan. - fn is_blob(addr: Addr, addr_set: RBTreeMap‹G›) -> G { - 1 - rbtree_map_lookup_or_default(ptr_val(addr), addr_set, 0) - } - - -- Build a set of all constant addresses (RBTreeMap keyed by ptr_val(addr) - -- → 1). Used by `is_blob` and any other membership check that needs - -- O(log N) rather than O(N) linear scan. - fn build_addr_set(addrs: List‹Addr›) -> RBTreeMap‹G› { - match load(addrs) { - ListNode.Nil => RBTreeMap.Nil, - ListNode.Cons(a, rest) => - let rest_set = build_addr_set(rest); - rbtree_map_insert(ptr_val(a), 1, rest_set), + -- 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. + 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, + _ => 0, } } @@ -157,105 +152,6 @@ def ingress := ⟦ } } - -- Find the Muts block address by scanning a constant's refs for any - -- projection constant (IPrj, CPrj, RPrj, DPrj). Used for standalone - -- recursors to locate their inductive's block. - fn find_block_addr_from_refs(refs: List‹Addr›, addr_set: RBTreeMap‹G›) -> Addr { - match load(refs) { - ListNode.Nil => store([0u8; 32]), - ListNode.Cons(addr, rest) => - let blob = is_blob(addr, addr_set); - match blob { - 1 => find_block_addr_from_refs(rest, addr_set), - 0 => - let c = load_verified_constant(addr); - match c { - Constant.Mk(info, _, _, _) => - match info { - ConstantInfo.IPrj(prj) => - match prj { InductiveProj.Mk(_, block_addr) => block_addr, }, - ConstantInfo.CPrj(prj) => - match prj { ConstructorProj.Mk(_, _, block_addr) => block_addr, }, - ConstantInfo.RPrj(prj) => - match prj { RecursorProj.Mk(_, block_addr) => block_addr, }, - ConstantInfo.DPrj(prj) => - match prj { DefinitionProj.Mk(_, block_addr) => block_addr, }, - _ => find_block_addr_from_refs(rest, addr_set), - }, - }, - }, - } - } - - fn recr_rule_count(recr: Recursor) -> G { - match recr { - Recursor.Mk(_, _, _, _, _, _, _, _, rules) => - count_recr_rules(rules), - } - } - - -- Count recursor rules - fn count_recr_rules(rules: List‹RecursorRule›) -> G { - match load(rules) { - ListNode.Nil => 0, - ListNode.Cons(_, rest) => count_recr_rules(rest) + 1, - } - } - - -- Count constructors in a Muts block's first inductive - fn count_block_ctors(members: List‹MutConst›) -> G { - match load(members) { - ListNode.Nil => 0, - ListNode.Cons(mc, rest) => - match mc { - MutConst.Indc(ind) => - match ind { - Inductive.Mk(_, _, _, _, _, _, _, _, ctors) => - list_length(ctors), - }, - _ => count_block_ctors(rest), - }, - } - } - - -- Find the correct block address for a standalone recursor by matching - -- the number of recursor rules to the number of constructors in the block. - fn find_matching_block_addr(refs: List‹Addr›, addr_set: RBTreeMap‹G›, nrules: G) -> Addr { - match load(refs) { - ListNode.Nil => store([0u8; 32]), - ListNode.Cons(addr, rest) => - let blob = is_blob(addr, addr_set); - match blob { - 1 => find_matching_block_addr(rest, addr_set, nrules), - 0 => - let c = load_verified_constant(addr); - match c { - Constant.Mk(info, _, _, _) => - match info { - ConstantInfo.IPrj(prj) => - match prj { - InductiveProj.Mk(_, block_addr) => - let bc = load_verified_constant(block_addr); - match bc { - Constant.Mk(bi, _, _, _) => - match bi { - ConstantInfo.Muts(members) => - let nctors = count_block_ctors(members); - match nctors - nrules { - 0 => block_addr, - _ => find_matching_block_addr(rest, addr_set, nrules), - }, - _ => find_matching_block_addr(rest, addr_set, nrules), - }, - }, - }, - _ => find_matching_block_addr(rest, addr_set, nrules), - }, - }, - }, - } - } - -- ============================================================================ -- Position map: maps loaded addresses to kernel constant positions. -- @@ -304,8 +200,28 @@ def ingress := ⟦ } } - -- Look up the kernel position for an address using parallel lists. - fn lookup_addr_pos(target: Addr, all_addrs: List‹Addr›, pos_map: List‹G›) -> G { + -- Look up the kernel position for an address. Fast path: a ptr_val hit + -- in the interned `addr_pos_map` (values stored as pos+1, so 0 = absent). + -- Sound because ptr_val equality ⟹ content equality (the POSITIVE + -- direction; see the invariant on `build_addr_pos_map`). On a miss — a + -- de-interned pointer, or a genuine non-constant such as a blob ref — + -- 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. + 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), + _ => hit - 1, + } + } + + -- Content-based fallback for `lookup_addr_pos`: O(N) parallel-list scan + -- via `address_eq` (full 32-byte compare, sound under de-intern). + -- Returns 0 if absent. Structurally identical to `lookup_block_start`; + -- Aiur merges the two into one circuit. + fn lookup_addr_pos_linear(target: Addr, all_addrs: List‹Addr›, pos_map: List‹G›) -> G { match load(all_addrs) { ListNode.Nil => 0, ListNode.Cons(addr, rest_addrs) => @@ -314,12 +230,42 @@ def ingress := ⟦ let eq = address_eq(target, addr); match eq { 1 => pos, - 0 => lookup_addr_pos(target, rest_addrs, rest_pos), + 0 => lookup_addr_pos_linear(target, rest_addrs, rest_pos), }, }, } } + -- Build the `ptr_val(addr) → (pos+1)` map keyed by every constant + -- address. Serves two roles: `lookup_addr_pos`'s fast path (returns the + -- kernel position) and `is_blob`'s membership test (present ⟺ constant). + -- pos+1 so the lookup default 0 unambiguously means "absent". Head is + -- inserted last (recurse first), so on any duplicate ptr_val the head + -- wins — matching the linear scan's first-match. + -- + -- ptr_val-key SOUNDNESS INVARIANT: a pointer maps to exactly one stored + -- value (memory consistency), so ptr_val collision across DISTINCT + -- contents is impossible — distinct addresses can never be conflated. + -- A malicious prover's only freedom is de-interning (one content stored + -- at several pointers), which makes a present key read as ABSENT. So a + -- ptr_val-keyed map is sound ONLY where a false "absent" is conservative. + -- `is_blob` is fine: a de-interned constant reads as a blob, content-bound + -- and harmless. `lookup_addr_pos` is NOT fine on its own — a miss yields a + -- usable position — so it falls back to the content-based `address_eq` + -- scan on miss. Each Addr is also blake3-bound to its content and the + -- checkEnv claim merkle-commits the address set. + fn build_addr_pos_map(all_addrs: List‹Addr›, pos_map: List‹G›) -> RBTreeMap‹G› { + match load(all_addrs) { + ListNode.Nil => RBTreeMap.Nil, + ListNode.Cons(addr, rest_addrs) => + match load(pos_map) { + ListNode.Cons(pos, rest_pos) => + rbtree_map_insert(ptr_val(addr), pos + 1, + build_addr_pos_map(rest_addrs, rest_pos)), + }, + } + } + -- 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) { @@ -624,12 +570,13 @@ def ingress := ⟦ -- Ref index building using position map -- ============================================================================ - fn build_ref_idxs_mapped(refs: List‹Addr›, all_addrs: List‹Addr›, pos_map: List‹G›) -> List‹G› { + fn build_ref_idxs_mapped(refs: List‹Addr›, addr_pos_map: &RBTreeMap‹G›, + all_addrs: List‹Addr›, pos_map: List‹G›) -> List‹G› { match load(refs) { ListNode.Nil => store(ListNode.Nil), ListNode.Cons(addr, rest) => - let pos = lookup_addr_pos(addr, all_addrs, pos_map); - store(ListNode.Cons(pos, build_ref_idxs_mapped(rest, all_addrs, pos_map))), + 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))), } } @@ -1059,14 +1006,15 @@ def ingress := ⟦ consts: List‹&Constant›, cur_addrs: List‹Addr›, all_addrs: List‹Addr›, - addr_set: RBTreeMap‹G›, pos_map: List‹G›, canon_addrs: List‹Addr›, block_addrs: List‹Addr›, block_starts: List‹G›, pos: G ) -> List‹&ConvertInput› { - build_convert_inputs_walk(consts, cur_addrs, all_addrs, addr_set, pos_map, + -- 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)); + build_convert_inputs_walk(consts, cur_addrs, all_addrs, addr_pos_map, pos_map, canon_addrs, block_addrs, block_starts, pos, store(ListNode.Nil)) } @@ -1075,7 +1023,7 @@ def ingress := ⟦ consts: List‹&Constant›, cur_addrs: List‹Addr›, all_addrs: List‹Addr›, - addr_set: RBTreeMap‹G›, + addr_pos_map: &RBTreeMap‹G›, pos_map: List‹G›, canon_addrs: List‹Addr›, block_addrs: List‹Addr›, @@ -1102,7 +1050,7 @@ def ingress := ⟦ -- Duplicate Muts: skip emission (canonical Muts already -- 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_set, pos_map, + build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_pos_map, pos_map, canon_addrs, block_addrs, block_starts, pos, seen_mptrs), 0 => let new_seen = match mptr { @@ -1110,52 +1058,52 @@ def ingress := ⟦ _ => store(ListNode.Cons(mptr, seen_mptrs)), }; let size = block_kernel_size(members); - let canon_block_start = lookup_addr_pos(head_addr, all_addrs, pos_map); + 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, all_addrs, pos_map); - let lit_blobs = build_lit_blobs(refs, addr_set); + 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 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); - let more = build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_set, pos_map, + 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); list_concat(expanded, more), }, ConstantInfo.IPrj(_) => - build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_set, 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_addrs, block_addrs, block_starts, pos, seen_mptrs), ConstantInfo.CPrj(_) => - build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_set, 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_addrs, block_addrs, block_starts, pos, seen_mptrs), ConstantInfo.RPrj(_) => - build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_set, 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_addrs, block_addrs, block_starts, pos, seen_mptrs), ConstantInfo.DPrj(_) => - build_convert_inputs_walk(rest, rest_addrs, all_addrs, addr_set, 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_addrs, block_addrs, block_starts, pos, seen_mptrs), ConstantInfo.Defn(defn) => - let ref_idxs = build_ref_idxs_mapped(refs, all_addrs, pos_map); - let lit_blobs = build_lit_blobs(refs, addr_set); + 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 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_set, 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_addrs, block_addrs, block_starts, pos + 1, seen_mptrs))), ConstantInfo.Axio(axio) => - let ref_idxs = build_ref_idxs_mapped(refs, all_addrs, pos_map); - let lit_blobs = build_lit_blobs(refs, addr_set); + 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 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_set, 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_addrs, block_addrs, block_starts, pos + 1, seen_mptrs))), ConstantInfo.Quot(quot) => - let ref_idxs = build_ref_idxs_mapped(refs, all_addrs, pos_map); - let lit_blobs = build_lit_blobs(refs, addr_set); + 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 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_set, 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_addrs, block_addrs, block_starts, pos + 1, seen_mptrs))), ConstantInfo.Recr(recr) => - let ref_idxs = build_ref_idxs_mapped(refs, all_addrs, pos_map); - let lit_blobs = build_lit_blobs(refs, addr_set); + 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 @@ -1185,7 +1133,7 @@ def ingress := ⟦ 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_set, 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_addrs, block_addrs, block_starts, pos + 1, seen_mptrs))), }, }, }, @@ -1282,12 +1230,11 @@ def ingress := ⟦ fn ingress(target_addr: Addr) -> List‹&KConstantInfo› { let (all_addrs, all_consts) = load_with_deps( target_addr, store(ListNode.Nil), store(ListNode.Nil), store(ListNode.Nil), RBTreeMap.Nil); - let addr_set = build_addr_set(all_addrs); 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 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, addr_set, pos_map, canon_addrs, block_addrs, block_starts, 0); + let inputs = build_convert_inputs(all_consts, all_addrs, all_addrs, pos_map, canon_addrs, block_addrs, block_starts, 0); convert_all(inputs) } @@ -1597,14 +1544,34 @@ def ingress := ⟦ fn ingress_with_primitives(target_addr: Addr) -> (List‹&KConstantInfo›, List‹Addr›) { let (all_addrs, all_consts) = load_with_deps( target_addr, store(ListNode.Nil), store(ListNode.Nil), store(ListNode.Nil), RBTreeMap.Nil); - let addr_set = build_addr_set(all_addrs); + finish_ingress(all_addrs, all_consts) + } + + -- Ingress the UNION closure of all env leaves in a single pass. One + -- `load_with_deps` over leaves[0] as target with the remaining leaves as + -- the initial worklist loads every leaf + its transitive deps; then the + -- shared `finish_ingress` pipeline runs ONCE over the union, rather than + -- being re-run per leaf as CheckEnv previously did. + fn ingress_env(leaves: List‹Addr›) -> (List‹&KConstantInfo›, List‹Addr›) { + match load(leaves) { + ListNode.Nil => synthetic_primitive_entries(), + ListNode.Cons(first, rest) => + let (all_addrs, all_consts) = load_with_deps( + first, rest, store(ListNode.Nil), store(ListNode.Nil), RBTreeMap.Nil); + finish_ingress(all_addrs, all_consts), + } + } + + -- Shared post-load pipeline: layout, conversion, addr table, primitives. + 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); -- 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, addr_set, pos_map, canon_addrs, block_addrs, block_starts, 0); + let inputs = build_convert_inputs(all_consts, all_addrs, all_addrs, pos_map, canon_addrs, block_addrs, block_starts, 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²) diff --git a/Ix/IxVM/Kernel/Claim.lean b/Ix/IxVM/Kernel/Claim.lean index 7a965a72..27c9a0ca 100644 --- a/Ix/IxVM/Kernel/Claim.lean +++ b/Ix/IxVM/Kernel/Claim.lean @@ -854,29 +854,21 @@ def claim := ⟦ () } + -- Ingress the union closure of all env leaves ONCE, then check every + -- constant in it (skipping assumption leaves) via the same + -- `check_all_skipping` path `run_check` uses. Structurally a + -- `run_check` over a closure that happens to be the whole env, so the + -- soundness rides on that existing pattern; the union order is verified by + -- the single `check_canonical_block_sort(top)` inside `check_all_skipping` + -- (a stronger global order than the per-leaf closures it replaces). fn run_check_env(env_root: Addr, asm: Option‹Addr›) { let env_leaves = load_assumption_tree(env_root); - let asm_leaves = match asm { - Option.None => store(ListNode.Nil), - Option.Some(asm_root) => load_assumption_tree(asm_root), - }; - check_env_iter(env_leaves, asm_leaves) - } - - fn check_env_iter(env_leaves: List‹Addr›, asm_leaves: List‹Addr›) { - match load(env_leaves) { - ListNode.Nil => (), - ListNode.Cons(leaf, rest) => - match addr_in_list(leaf, asm_leaves) { - 1 => - check_env_iter(rest, asm_leaves), - _ => - let (k_consts, addrs) = ingress_with_primitives(leaf); - let target_pos = find_addr_idx(leaf, addrs, 0); - let ci = load(list_lookup(k_consts, target_pos)); - let _ = check_const(ci, target_pos, k_consts, addrs); - check_env_iter(rest, asm_leaves), - }, + let (k_consts, addrs) = ingress_env(env_leaves); + match asm { + Option.None => check_all(k_consts, k_consts, addrs), + Option.Some(asm_root) => + let asm_leaves = load_assumption_tree(asm_root); + check_all_skipping(k_consts, k_consts, addrs, asm_leaves), } } diff --git a/Ix/IxVM/RBTreeMap.lean b/Ix/IxVM/RBTreeMap.lean index 933f1e42..16c4d8b5 100644 --- a/Ix/IxVM/RBTreeMap.lean +++ b/Ix/IxVM/RBTreeMap.lean @@ -12,31 +12,49 @@ def rbTreeMap := ⟦ Nil } - -- Okasaki-style balance: fixes red-red violations after insertion + -- Okasaki-style balance: fixes red-red violations after insertion. + -- + -- A violation can only occur under a BLACK parent (color 1); a red + -- parent never rebalances. The 4 rebalance cases are WIDE (they deref a + -- red grandchild and rebuild 3 nodes), so they're factored into the cold + -- `rbtree_map_balance_fix`. Aiur lays a function's width as the max over + -- match arms, so keeping the hot path (red parent / black parent with no + -- violation) here as a narrow color-dispatch keeps `balance` itself + -- narrow; the wide rebalance machinery only taxes the rows that actually + -- reach `_fix` (black parents). fn rbtree_map_balance‹V›(color: G, key: G, value: V, left: RBTreeMap‹V›, right: RBTreeMap‹V›) -> RBTreeMap‹V› { - match (color, left, right) { + match color { + 1 => rbtree_map_balance_fix(key, value, left, right), + _ => RBTreeMap.Node(color, key, value, store(left), store(right)), + } + } + + -- Cold path: parent is black (color 1). Match the 4 red-red grandchild + -- configurations; the fall-through is "black parent, no violation". + fn rbtree_map_balance_fix‹V›(key: G, value: V, left: RBTreeMap‹V›, right: RBTreeMap‹V›) -> RBTreeMap‹V› { + match (left, right) { -- Case 1: left child red, left-left grandchild red - (1, RBTreeMap.Node(0, yk, yv, &RBTreeMap.Node(0, xk, xv, a, b), c), d) => + (RBTreeMap.Node(0, yk, yv, &RBTreeMap.Node(0, xk, xv, a, b), c), d) => RBTreeMap.Node(0, yk, yv, store(RBTreeMap.Node(1, xk, xv, a, b)), store(RBTreeMap.Node(1, key, value, c, store(d)))), -- Case 2: left child red, left-right grandchild red - (1, RBTreeMap.Node(0, xk, xv, a, &RBTreeMap.Node(0, yk, yv, b, c)), d) => + (RBTreeMap.Node(0, xk, xv, a, &RBTreeMap.Node(0, yk, yv, b, c)), d) => RBTreeMap.Node(0, yk, yv, store(RBTreeMap.Node(1, xk, xv, a, b)), store(RBTreeMap.Node(1, key, value, c, store(d)))), -- Case 3: right child red, right-left grandchild red - (1, a, RBTreeMap.Node(0, zk, zv, &RBTreeMap.Node(0, yk, yv, b, c), d)) => + (a, RBTreeMap.Node(0, zk, zv, &RBTreeMap.Node(0, yk, yv, b, c), d)) => RBTreeMap.Node(0, yk, yv, store(RBTreeMap.Node(1, key, value, store(a), b)), store(RBTreeMap.Node(1, zk, zv, c, d))), -- Case 4: right child red, right-right grandchild red - (1, a, RBTreeMap.Node(0, yk, yv, b, &RBTreeMap.Node(0, zk, zv, c, d))) => + (a, RBTreeMap.Node(0, yk, yv, b, &RBTreeMap.Node(0, zk, zv, c, d))) => RBTreeMap.Node(0, yk, yv, store(RBTreeMap.Node(1, key, value, store(a), b)), store(RBTreeMap.Node(1, zk, zv, c, d))), - -- No violation - _ => RBTreeMap.Node(color, key, value, store(left), store(right)), + -- No violation (black parent) + _ => RBTreeMap.Node(1, key, value, store(left), store(right)), } } @@ -50,10 +68,14 @@ def rbTreeMap := ⟦ match lt { 1 => rbtree_map_balance(color, k, v, rbtree_map_ins(key, value, left), right), _ => - let gt = u32_less_than(k, key); - match gt { - 1 => rbtree_map_balance(color, k, v, left, rbtree_map_ins(key, value, right)), - _ => RBTreeMap.Node(color, key, value, store(left), store(right)), + -- key not < k. Distinguish equal (overwrite) from greater + -- (recurse right) with a field subtraction instead of a second + -- u32_less_than (which would cost +12 aux / +6 lookups). Keys + -- are u32-range field elements, so `key - k == 0` iff equal. + let eq = key - k; + match eq { + 0 => RBTreeMap.Node(color, key, value, store(left), store(right)), + _ => rbtree_map_balance(color, k, v, left, rbtree_map_ins(key, value, right)), }, }, } @@ -77,10 +99,10 @@ def rbTreeMap := ⟦ match lt { 1 => rbtree_map_lookup(key, left), _ => - let gt = u32_less_than(k, key); - match gt { - 1 => rbtree_map_lookup(key, right), - _ => v, + let eq = key - k; + match eq { + 0 => v, + _ => rbtree_map_lookup(key, right), }, }, } @@ -97,10 +119,10 @@ def rbTreeMap := ⟦ match lt { 1 => rbtree_map_lookup_or_default(key, left, default), _ => - let gt = u32_less_than(k, key); - match gt { - 1 => rbtree_map_lookup_or_default(key, right, default), - _ => v, + let eq = key - k; + match eq { + 0 => v, + _ => rbtree_map_lookup_or_default(key, right, default), }, }, }