From 5c619bad8341559aa8b10e6e010fb8f6256424b0 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Mon, 13 Jul 2026 16:05:52 -0400 Subject: [PATCH] refactor: single-source reducibility hints in Env::anon_hints MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Remove the hints field from ConstantMeta::Def (Rust, Lean, the FFI constructor slots, and the .ixe named-section encoding). Reducibility hints now live only in the env-level anon_hints map, keyed by constant address. - The compiler is the sole producer: compile_definition records each definition's hints per name (CompileState::def_hints), and finalize_hints resolves them through the registered Named entries into env.anon_hints via Env::register_hint once addresses are final. The Lean compiler mirror (BlockState.defHints + Ixon.mergeHints) does the same. Alias collisions merge order-independently (min by (tag, height)), so parallel workers and both mirrors agree byte-for-byte. - Writers serialize the map directly; the derive-from-Named fallback is deleted from Env::put / put_file / serialized_size_breakdown and both Lean writers. This removes the serial full-decode of every demoted Named entry that regressed ix compile by 5-14%: the derivation loop called Named::meta() per entry, which re-decodes demoted metadata (the IX_COMPILE_DEMOTE default) on every call. - Kernel ingress reads hints from anon_hints in both anon and meta modes; the hints_override parameter threading is gone. Decompile (both languages) and the IxVM claim harness look hints up by address. The lazy check path transports the hints section on RawEnvLazy instead of fabricating per-name Def metas (RawNamedLite.toConstMeta is removed). - anon_hints becomes an IxonMap like the other env maps; Env now derives Clone (the riscv64 IxonMap wrapper gained Clone, replacing the manual per-map Clone impl). Format change (pre-alpha, no compat shims): Def metadata loses its hints byte in the named sections, so every hint is stored once instead of two or three times (hints section + named meta + aux originals) — the whole-stdlib env shrinks by ~232 KB. InitStd compile-time returns to its pre-hints-section cost (median 7.3s -> 5.7s locally vs the derivation code), with byte-exact Lean/Rust writer parity at 505,674,085 bytes on the whole-stdlib env. Behavior note: a hint-only change now reports as a pure hintsChanged row in ix diff; it previously also surfaced as a Def metadata diff. --- Ix/CompileM.lean | 50 ++++- Ix/DecompileM.lean | 19 +- Ix/IxVM/ClaimHarness.lean | 11 +- Ix/Ixon.lean | 109 ++++------ Tests/FFI/Ixon.lean | 22 ++- Tests/Gen/Ixon.lean | 2 +- Tests/Ix/Compile.lean | 5 +- crates/compile/src/compile.rs | 30 ++- crates/compile/src/compile/env.rs | 2 + crates/compile/src/decompile.rs | 20 +- crates/ffi/src/lean.rs | 10 +- crates/ffi/src/lean_ixon/env.rs | 38 ++-- crates/ffi/src/lean_ixon/meta.rs | 24 +-- crates/ffi/src/lean_ixon/serialize.rs | 26 +-- crates/ixon/src/diff.rs | 29 +-- crates/ixon/src/env.rs | 143 +++++++------- crates/ixon/src/map.rs | 2 +- crates/ixon/src/metadata.rs | 15 +- crates/ixon/src/serialize.rs | 198 +++++++------------ crates/ixvm-codegen/src/aiur_ixvm_witness.rs | 2 +- crates/kernel/src/anon_work.rs | 8 +- crates/kernel/src/ingress.rs | 67 +++---- docs/Ixon.md | 21 +- 23 files changed, 398 insertions(+), 455 deletions(-) diff --git a/Ix/CompileM.lean b/Ix/CompileM.lean index 701608a55..a39fe51fd 100644 --- a/Ix/CompileM.lean +++ b/Ix/CompileM.lean @@ -84,6 +84,10 @@ structure BlockState where blockBlobs : Std.HashMap Address ByteArray := {} /-- Name components collected during block compilation -/ blockNames : Std.HashMap Address Ix.Name := {} + /-- Reducibility hints per definition name compiled in this block. + Hints are not part of `ConstantMeta`; the driver resolves this + map into `Ixon.Env.anonHints` once addresses are final. -/ + defHints : Std.HashMap Name Lean.ReducibilityHints := {} /-- Arena-based expression metadata for the current constant -/ arena : Ixon.ExprMetaArena := {} deriving Inhabited @@ -310,6 +314,10 @@ def storeString (s : String) : CompileM Address := do modifyBlockState fun c => { c with blockBlobs := c.blockBlobs.insert addr bytes } pure addr +/-- Record a definition's reducibility hints (see `BlockState.defHints`). -/ +def recordDefHints (name : Name) (hints : Lean.ReducibilityHints) : CompileM Unit := + modifyBlockState fun c => { c with defHints := c.defHints.insert name hints } + /-- Compile a name: store all string components as blobs and track name components in blockNames for deduplication. This matches Rust's compile_name behavior. -/ @@ -889,7 +897,8 @@ def compileDefinition (d : DefinitionVal) : CompileM (Ixon.Definition × Ixon.Co typ := typeExpr value := valueExpr } - let constMeta := Ixon.ConstantMeta.defn nameAddr lvlAddrs d.hints allAddrs ctxAddrs arena typeRoot valueRoot + recordDefHints d.cnst.name d.hints + let constMeta := Ixon.ConstantMeta.defn nameAddr lvlAddrs allAddrs ctxAddrs arena typeRoot valueRoot pure (defn, constMeta, typeExpr, valueExpr) /-- Compile a theorem to Ixon.Definition with metadata. -/ @@ -919,7 +928,8 @@ def compileTheorem (d : TheoremVal) : CompileM (Ixon.Definition × Ixon.Constant typ := typeExpr value := valueExpr } - let constMeta := Ixon.ConstantMeta.defn nameAddr lvlAddrs .opaque allAddrs ctxAddrs arena typeRoot valueRoot + recordDefHints d.cnst.name .opaque + let constMeta := Ixon.ConstantMeta.defn nameAddr lvlAddrs allAddrs ctxAddrs arena typeRoot valueRoot pure (defn, constMeta, typeExpr, valueExpr) /-- Compile an opaque to Ixon.Definition with metadata. -/ @@ -949,7 +959,8 @@ def compileOpaque (d : OpaqueVal) : CompileM (Ixon.Definition × Ixon.ConstantMe typ := typeExpr value := valueExpr } - let constMeta := Ixon.ConstantMeta.defn nameAddr lvlAddrs .opaque allAddrs ctxAddrs arena typeRoot valueRoot + recordDefHints d.cnst.name .opaque + let constMeta := Ixon.ConstantMeta.defn nameAddr lvlAddrs allAddrs ctxAddrs arena typeRoot valueRoot pure (defn, constMeta, typeExpr, valueExpr) /-- Compile an axiom to Ixon.Axiom with metadata. -/ @@ -1155,7 +1166,8 @@ def compileDefinitionData (d : Def) : CompileM (Ixon.Definition × Ixon.Constant | .defn => d.hints | .thm => .opaque | .opaq => .opaque - let constMeta := Ixon.ConstantMeta.defn nameAddr lvlAddrs hints allAddrs ctxAddrs arena typeRoot valueRoot + recordDefHints d.name hints + let constMeta := Ixon.ConstantMeta.defn nameAddr lvlAddrs allAddrs ctxAddrs arena typeRoot valueRoot pure (defn, constMeta, typeExpr, valueExpr) /-- Compile inductive data for an Ind structure (from Mutual.lean). @@ -1510,6 +1522,7 @@ def compileEnv (env : Ix.Environment) (blocks : Ix.CondensedBlocks) (dbg : Bool -- Initialize compilation state let mut compileEnv := CompileEnv.new env let mut blockNames : Std.HashMap Address Ix.Name := {} + let mut defHints : Std.HashMap Name Lean.ReducibilityHints := {} -- Build work queue data structures let totalBlocks := blocks.blocks.size @@ -1554,6 +1567,7 @@ def compileEnv (env : Ix.Environment) (blocks : Ix.CondensedBlocks) (dbg : Bool blobs := cache.blockBlobs.fold (fun m k v => m.insert k v) compileEnv.blobs } blockNames := cache.blockNames.fold (fun m k v => m.insert k v) blockNames + defHints := cache.defHints.fold (fun m k v => m.insert k v) defHints -- If there are projections, store them and map names to projection addresses if result.projections.isEmpty then @@ -1608,6 +1622,17 @@ def compileEnv (env : Ix.Environment) (blocks : Ix.CondensedBlocks) (dbg : Bool -- Merge name string blobs into the main blobs map let allBlobs := nameBlobs.fold (fun m k v => m.insert k v) compileEnv.blobs + -- Resolve per-name hints to each name's registered constant address + -- (the projection address for mutual-block members — exactly the + -- address the kernel looks hints up under). Alias collisions merge + -- order-independently, matching Rust `CompileState::finalize_hints`. + let anonHints := compileEnv.nameToNamed.fold (init := {}) fun m name named => + match defHints.get? name with + | some h => m.alter named.addr fun + | some h₀ => some (Ixon.mergeHints h₀ h) + | none => some h + | none => m + let ixonEnv : Ixon.Env := { consts := compileEnv.constants.fold (init := {}) fun m a c => m.insert a (Ixon.LazyConstant.ofConstant c) @@ -1616,6 +1641,7 @@ def compileEnv (env : Ix.Environment) (blocks : Ix.CondensedBlocks) (dbg : Bool names := namesMap comms := {} addrToName := addrToNameMap + anonHints } return .ok (ixonEnv, compileEnv.totalBytes) @@ -1705,6 +1731,7 @@ structure WaveBlockResult where projections : Array (Name × Ixon.Constant × Address × Ixon.ConstantMeta) blobs : Std.HashMap Address ByteArray names : Std.HashMap Address Ix.Name + defHints : Std.HashMap Name Lean.ReducibilityHints totalBytes : Nat /-- Work item for a worker thread -/ @@ -1793,6 +1820,7 @@ def compileEnvParallel (env : Ix.Environment) (blocks : Ix.CondensedBlocks) projections := projsNoBytes blobs := cache.blockBlobs names := cache.blockNames + defHints := cache.defHints totalBytes := projBytes } discard <| resultChan.send result @@ -1808,6 +1836,7 @@ def compileEnvParallel (env : Ix.Environment) (blocks : Ix.CondensedBlocks) let mut constants : Std.HashMap Address Ixon.Constant := {} let mut blobs : Std.HashMap Address ByteArray := {} let mut blockNames : Std.HashMap Address Ix.Name := {} + let mut defHints : Std.HashMap Name Lean.ReducibilityHints := {} let mut totalBytes : Nat := 0 let mut remaining : Set Name := {} @@ -1864,9 +1893,10 @@ def compileEnvParallel (env : Ix.Environment) (blocks : Ix.CondensedBlocks) for (name, proj, addr, constMeta) in result.projections do constants := constants.insert addr proj nameToNamed := nameToNamed.insert name { addr, constMeta } - -- Store blobs and names + -- Store blobs, names, and hints blobs := result.blobs.fold (fun m k v => m.insert k v) blobs blockNames := result.names.fold (fun m k v => m.insert k v) blockNames + defHints := result.defHints.fold (fun m k v => m.insert k v) defHints totalBytes := totalBytes + result.totalBytes compiled := compiled + 1 @@ -1902,6 +1932,15 @@ def compileEnvParallel (env : Ix.Environment) (blocks : Ix.CondensedBlocks) if dbg then IO.println s!" [Lean Compile] Blobs: {blockBlobCount} from blocks, {nameBlobCount} from names, {overlapCount} overlap, {finalBlobCount} final" + -- Resolve per-name hints to registered constant addresses (see the + -- serial driver / Rust `CompileState::finalize_hints`). + let anonHints := nameToNamed.fold (init := {}) fun m name named => + match defHints.get? name with + | some h => m.alter named.addr fun + | some h₀ => some (Ixon.mergeHints h₀ h) + | none => some h + | none => m + let ixonEnv : Ixon.Env := { consts := constants.fold (init := {}) fun m a c => m.insert a (Ixon.LazyConstant.ofConstant c) @@ -1910,6 +1949,7 @@ def compileEnvParallel (env : Ix.Environment) (blocks : Ix.CondensedBlocks) names := namesMap comms := {} addrToName := addrToNameMap + anonHints } return .ok (ixonEnv, totalBytes) diff --git a/Ix/DecompileM.lean b/Ix/DecompileM.lean index 81ba6c133..e2f548a93 100644 --- a/Ix/DecompileM.lean +++ b/Ix/DecompileM.lean @@ -507,7 +507,7 @@ def getLvlAddrs : ConstantMeta → Array Address | .empty | .muts _ => #[] def getArenaAndTypeRoot : ConstantMeta → ExprMetaArena × UInt64 - | .defn _ _ _ _ _ arena typeRoot _ => (arena, typeRoot) + | .defn _ _ _ _ arena typeRoot _ => (arena, typeRoot) | .axio _ _ arena typeRoot => (arena, typeRoot) | .quot _ _ arena typeRoot => (arena, typeRoot) | .indc _ _ _ _ _ arena typeRoot => (arena, typeRoot) @@ -516,11 +516,11 @@ def getArenaAndTypeRoot : ConstantMeta → ExprMetaArena × UInt64 | .empty | .muts _ => ({}, 0) def getAllAddrs : ConstantMeta → Array Address - | .defn _ _ _ all .. => all | .indc _ _ _ all .. => all + | .defn _ _ all .. => all | .indc _ _ _ all .. => all | .recr _ _ _ all .. => all | _ => #[] def getCtxAddrs : ConstantMeta → Array Address - | .defn _ _ _ _ ctx .. => ctx | .indc _ _ _ _ ctx .. => ctx + | .defn _ _ _ ctx .. => ctx | .indc _ _ _ _ ctx .. => ctx | .recr _ _ _ _ ctx .. => ctx | _ => #[] /-- Resolve name from ConstantMeta. -/ @@ -571,9 +571,16 @@ def decompileDefinition (d : Ixon.Definition) (cnst : Constant) (cMeta : Constan let univParams ← decompileMetaLevels cMeta let allNames ← decompileMetaAll cMeta name let mutCtx ← decompileMetaCtx cMeta - let (hints, valueRoot) := match cMeta with - | .defn _ _ hints _ _ _ _ valueRoot => (hints, valueRoot) - | _ => (.opaque, (0 : UInt64)) + let valueRoot := match cMeta with + | .defn _ _ _ _ _ _ valueRoot => valueRoot + | _ => (0 : UInt64) + -- Hints live in `Env.anonHints`, keyed by the constant address the + -- name resolves to; absent entry → `.opaque`, matching the + -- compiler's treatment of theorems and opaques. + let ixonEnv := (← getEnv).ixonEnv + let hints := match ixonEnv.named.get? name with + | some named => (ixonEnv.anonHints.get? named.addr).getD .opaque + | none => .opaque let (arena, typeRoot) := getArenaAndTypeRoot cMeta withFreshBlock cnst mutCtx univParams arena do let typeExpr ← decompileExpr d.typ typeRoot diff --git a/Ix/IxVM/ClaimHarness.lean b/Ix/IxVM/ClaimHarness.lean index 55e29ce17..52cb70c4f 100644 --- a/Ix/IxVM/ClaimHarness.lean +++ b/Ix/IxVM/ClaimHarness.lean @@ -181,13 +181,10 @@ def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool) 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 3 key #[hintToG hints] - | _ => pure () + for (addr, hints) in ixonEnv.anonHints do + if !keep addr then continue + let key : Array Aiur.G := addr.hash.data.map .ofUInt8 + ioBuffer := ioBuffer.extend 3 key #[hintToG hints] return ioBuffer -- ============================================================================ diff --git a/Ix/Ixon.lean b/Ix/Ixon.lean index 626337ac8..1be0476ee 100644 --- a/Ix/Ixon.lean +++ b/Ix/Ixon.lean @@ -475,7 +475,7 @@ def ExprMetaArena.mdataItemCount (arena : ExprMetaArena) : Nat := that constant, plus root indices pointing into the arena. -/ inductive ConstantMeta where | empty - | defn (name : Address) (lvls : Array Address) (hints : Lean.ReducibilityHints) + | defn (name : Address) (lvls : Array Address) (all : Array Address) (ctx : Array Address) (arena : ExprMetaArena) (typeRoot : UInt64) (valueRoot : UInt64) | axio (name : Address) (lvls : Array Address) @@ -497,7 +497,7 @@ inductive ConstantMeta where /-- Count total arena nodes in this ConstantMeta. -/ def ConstantMeta.exprMetaCount : ConstantMeta → Nat | .empty => 0 - | .defn _ _ _ _ _ arena _ _ => arena.nodes.size + | .defn _ _ _ _ arena _ _ => arena.nodes.size | .axio _ _ arena _ => arena.nodes.size | .quot _ _ arena _ => arena.nodes.size | .indc _ _ _ _ _ arena _ => arena.nodes.size @@ -508,7 +508,7 @@ def ConstantMeta.exprMetaCount : ConstantMeta → Nat /-- Count total arena nodes and mdata items in this ConstantMeta. -/ def ConstantMeta.exprMetaStats : ConstantMeta → Nat × Nat | .empty => (0, 0) - | .defn _ _ _ _ _ arena _ _ => (arena.nodes.size, arena.mdataItemCount) + | .defn _ _ _ _ arena _ _ => (arena.nodes.size, arena.mdataItemCount) | .axio _ _ arena _ => (arena.nodes.size, arena.mdataItemCount) | .quot _ _ arena _ => (arena.nodes.size, arena.mdataItemCount) | .indc _ _ _ _ _ arena _ => (arena.nodes.size, arena.mdataItemCount) @@ -522,7 +522,7 @@ def ConstantMeta.exprMetaByType : ConstantMeta → Nat × Nat × Nat × Nat × N | .empty => (0, 0, 0, 0, 0) | cm => let arena := match cm with - | .defn _ _ _ _ _ a _ _ => a + | .defn _ _ _ _ a _ _ => a | .axio _ _ a _ => a | .quot _ _ a _ => a | .indc _ _ _ _ _ a _ => a @@ -1181,6 +1181,22 @@ def getReducibilityHints : GetM Lean.ReducibilityHints := do | 2 => pure (.regular (← getTag0).size.toUInt32) | x => throw s!"invalid ReducibilityHints {x}" +/-- Order-independent merge for hint registration: alpha-equivalent + definitions share one constant address but may carry different + reducibility hints (e.g. one alias marked `@[reducible]`), and the + winner must not depend on registration order. Keeps the minimum + under `(tag, height)` with `opaque < abbrev < regular h` — + commutative, associative, idempotent. Mirrors Rust + `Env::register_hint`. -/ +def mergeHints (a b : Lean.ReducibilityHints) : Lean.ReducibilityHints := + let key : Lean.ReducibilityHints → Nat × Nat + | .opaque => (0, 0) + | .abbrev => (1, 0) + | .regular n => (2, n.toNat) + let (a₁, a₂) := key a + let (b₁, b₂) := key b + if b₁ < a₁ || (b₁ == a₁ && b₂ < a₂) then b else a + /-- Serialize DataValue with indexed addresses. OfString/OfNat/OfInt/OfSyntax use raw 32-byte addresses (blob addresses, not in name index). -/ def putDataValueIndexed (dv : DataValue) (idx : NameIndex) : PutM Unit := do @@ -1315,11 +1331,10 @@ def getExprMetaArenaIndexed (rev : NameReverseIndex) : GetM ExprMetaArena := do def putConstantMetaIndexed (cm : ConstantMeta) (idx : NameIndex) : PutM Unit := do match cm with | .empty => putU8 255 - | .defn name lvls hints all ctx arena typeRoot valueRoot => + | .defn name lvls all ctx arena typeRoot valueRoot => putU8 0 putIdx name idx putIdxVec lvls idx - putReducibilityHints hints putIdxVec all idx putIdxVec ctx idx putExprMetaArenaIndexed arena idx @@ -1389,13 +1404,12 @@ def getConstantMetaIndexed (rev : NameReverseIndex) : GetM ConstantMeta := do | 0 => let name ← getIdx rev let lvls ← getIdxVec rev - let hints ← getReducibilityHints let all ← getIdxVec rev let ctx ← getIdxVec rev let arena ← getExprMetaArenaIndexed rev let typeRoot := (← getTag0).size let valueRoot := (← getTag0).size - pure (.defn name lvls hints all ctx arena typeRoot valueRoot) + pure (.defn name lvls all ctx arena typeRoot valueRoot) | 1 => let name ← getIdx rev let lvls ← getIdxVec rev @@ -1530,9 +1544,10 @@ structure Env where as a strictly ascending leaf list; `Ix.Merkle.merkleRootCanonical` over it reproduces the root a `Claim.assumptions` commits to. -/ assumptions : Std.HashSet Address := {} - /-- Reducibility hints (§3, the canonical hint channel for anon/lazy - readers). When empty, `putEnv` derives the section from Named - `.defn` metadata at write time. Mirrors Rust `Env.anon_hints`. -/ + /-- Reducibility hints, keyed by constant address — the single home + for hints (they do not appear in `ConstantMeta`). The compiler + populates this map; `putEnv` serializes it as the hints section + and `getEnv` reads it back. Mirrors Rust `Env.anon_hints`. -/ anonHints : Std.HashMap Address Lean.ReducibilityHints := {} deriving Inhabited @@ -1871,28 +1886,10 @@ def putEnv (env : Env) : PutM Unit := do -- Section 3: anon_hints — the canonical hint channel for the -- anon/lazy readers, placed before the metadata sections so they can - -- stop right after it. When the in-memory map is empty (the compile - -- path: hints live in Named metadata), the section is derived from - -- `named`. `named` is sorted here (the §5 canonical order, by name - -- hash) and reused for §5 below; the sorted iteration makes the - -- first-wins dedup by constant address deterministic. Matches Rust - -- `Env::put`. - let named := env.named.toList.toArray.qsort fun a b => (compare a.1 b.1).isLT - let hintPairs : Array (Address × Lean.ReducibilityHints) := - if env.anonHints.isEmpty then Id.run do - let mut seen : Std.HashSet Address := {} - let mut pairs : Array (Address × Lean.ReducibilityHints) := #[] - for (_, namedEntry) in named do - match namedEntry.constMeta with - | .defn _ _ hints _ _ _ _ _ => - if !seen.contains namedEntry.addr then - seen := seen.insert namedEntry.addr - pairs := pairs.push (namedEntry.addr, hints) - | _ => pure () - return pairs - else - env.anonHints.toList.toArray - let hintPairs := hintPairs.qsort fun a b => (compare a.1 b.1).isLT + -- stop right after it. Serialized straight from `env.anonHints`, the + -- single home for hints. Matches Rust `Env::put`. + let hintPairs := env.anonHints.toList.toArray.qsort + fun a b => (compare a.1 b.1).isLT putTag0 ⟨hintPairs.size.toUInt64⟩ for (addr, hints) in hintPairs do Serialize.put addr @@ -1910,6 +1907,7 @@ def putEnv (env : Env) : PutM Unit := do putNameComponent name -- Section 5: Named (name Address -> Named with metadata) + let named := env.named.toList.toArray.qsort fun a b => (compare a.1 b.1).isLT putTag0 ⟨named.size.toUInt64⟩ for (name, namedEntry) in named do -- Use the name's stored hash, which matches how it was stored in env.names @@ -2102,22 +2100,8 @@ def envSectionSizes (env : Env) : Nat × Nat × Nat × Nat × Nat × Nat := Id.r -- anon_hints section (mirrors putEnv's derive-from-named rule) let hintsBytes := runPut do - let named := env.named.toList.toArray.qsort fun a b => (compare a.1 b.1).isLT - let hintPairs : Array (Address × Lean.ReducibilityHints) := - if env.anonHints.isEmpty then Id.run do - let mut seen : Std.HashSet Address := {} - let mut pairs : Array (Address × Lean.ReducibilityHints) := #[] - for (_, namedEntry) in named do - match namedEntry.constMeta with - | .defn _ _ hints _ _ _ _ _ => - if !seen.contains namedEntry.addr then - seen := seen.insert namedEntry.addr - pairs := pairs.push (namedEntry.addr, hints) - | _ => pure () - return pairs - else - env.anonHints.toList.toArray - let hintPairs := hintPairs.qsort fun a b => (compare a.1 b.1).isLT + let hintPairs := env.anonHints.toList.toArray.qsort + fun a b => (compare a.1 b.1).isLT putTag0 ⟨hintPairs.size.toUInt64⟩ for (addr, hints) in hintPairs do Serialize.put addr @@ -2196,17 +2180,14 @@ structure RawConstSlice where len : UInt64 deriving Inhabited -/-- A named entry reduced to `name → addr` plus an encoded reducibility hint - (`hintKind`: 0 = none, 1 = opaque, 2 = abbrev, 3 = regular `hintVal`). -/ +/-- A named entry reduced to `name → addr`. -/ structure RawNamedLite where name : Ix.Name addr : Address - hintKind : UInt64 - hintVal : UInt64 deriving Inhabited /-- Metadata-light env returned by `rs_de_env_lazy`. Field order - matters: the Rust builder addresses constructor slots 0-4. -/ + matters: the Rust builder addresses constructor slots 0-5. -/ structure RawEnvLazy where consts : Array RawConstSlice named : Array RawNamedLite @@ -2215,33 +2196,25 @@ structure RawEnvLazy where main : Option Address := none /-- Bundle trust boundary (`Env.assumptions`), in header order. -/ assumptions : Array Address := #[] + /-- Reducibility hints (`Env.anonHints`) from the hints section. -/ + anonHints : Array (Address × Lean.ReducibilityHints) := #[] deriving Inhabited -/-- Decode an encoded reducibility hint into the `ConstantMeta` the check path - expects: a stripped `.defn` carrying just the hint (so `addEntries` finds it - via `.defn _ _ hints …`), or `.empty` for non-`Defn` entries. -/ -def RawNamedLite.toConstMeta (n : RawNamedLite) : ConstantMeta := - let mkDefn (h : Lean.ReducibilityHints) : ConstantMeta := - .defn default #[] h #[] #[] {} 0 0 - match n.hintKind with - | 1 => mkDefn .opaque - | 2 => mkDefn .abbrev - | 3 => mkDefn (.regular n.hintVal.toUInt32) - | _ => .empty - /-- Reconstruct an `Env` from a `RawEnvLazy` and the original buffer `buf`. Constants become `LazyConstant.ofSlice buf offset len` — zero-copy windows that share `buf`. `buf` MUST be the exact buffer passed to `rs_de_env_lazy` (offsets are relative to it). -/ def RawEnvLazy.toEnv (raw : RawEnvLazy) (buf : ByteArray) : Env := Id.run do let mut env : Env := { main := raw.main - assumptions := raw.assumptions.foldl (·.insert ·) {} } + assumptions := raw.assumptions.foldl (·.insert ·) {} + anonHints := raw.anonHints.foldl + (fun m (a, h) => m.insert a h) {} } for ⟨addr, offset, len⟩ in raw.consts do env := { env with consts := env.consts.insert addr (LazyConstant.ofSlice buf offset.toNat len.toNat) } for n in raw.named do - env := env.registerName n.name { addr := n.addr, constMeta := n.toConstMeta } + env := env.registerName n.name { addr := n.addr, constMeta := .empty } for ⟨addr, bytes⟩ in raw.blobs do env := { env with blobs := env.blobs.insert addr bytes } return env diff --git a/Tests/FFI/Ixon.lean b/Tests/FFI/Ixon.lean index b0107c69d..6f660965a 100644 --- a/Tests/FFI/Ixon.lean +++ b/Tests/FFI/Ixon.lean @@ -175,8 +175,8 @@ def constantMetaTests : TestSeq := let smallArena : ExprMetaArena := { nodes := #[.leaf, .app 0 0, .ref testAddr] } checkIO "ConstantMeta.empty" (roundtripIxonConstantMeta .empty == .empty) ++ checkIO "ConstantMeta.defn" (roundtripIxonConstantMeta - (.defn testAddr #[testAddr] .opaque #[] #[] smallArena 0 1) == - .defn testAddr #[testAddr] .opaque #[] #[] smallArena 0 1) ++ + (.defn testAddr #[testAddr] #[] #[] smallArena 0 1) == + .defn testAddr #[testAddr] #[] #[] smallArena 0 1) ++ checkIO "ConstantMeta.axio" (roundtripIxonConstantMeta (.axio testAddr #[] emptyArena 0) == .axio testAddr #[] emptyArena 0) ++ @@ -282,15 +282,16 @@ def envDiffTests : TestSeq := { info := .defn { kind := .defn, safety := .safe, lvls := 0, typ := .var 3, value } sharing := #[], refs := #[], univs := #[] } - -- Named metadata carries the hint; `anonHints` stays empty so the - -- writer derives §3 from the named `Def` metadata. + -- Hints live in `env.anonHints`, keyed by constant address; the + -- writer serializes that map as the hints section. let mkEnv (c : Constant) (h : Lean.ReducibilityHints) : Env := Id.run do let addr := Address.blake3 (serConstant c) let mut env : Env := {} env := env.storeConst addr c env := { env with names := RawEnv.addNameComponents env.names fooName } env := env.registerName fooName - { addr, constMeta := .defn fooName.getHash #[] h #[] #[] {} 0 0 } + { addr, constMeta := .defn fooName.getHash #[] #[] #[] {} 0 0 } + env := { env with anonHints := env.anonHints.insert addr h } return env let constA := mkConst (.var 0) let constB := mkConst (.var 1) @@ -356,16 +357,17 @@ def envDiffTests : TestSeq := d.namedChanged.size == 2 && (d.namedChanged.find? (·.name == "foo")).any (·.rippled == false) && (d.namedChanged.find? (·.name == "bar")).any (·.rippled == true)) ++ - -- Hints derive into anon §3, so a hint tweak is visible in the - -- default anon mode; the metadata carrying it only shows under meta. + -- Hints live only in the env-level hints section, so a hint tweak + -- is a pure `hintsChanged` row — no metadata difference in either + -- mode (the named entries are identical). test "EnvDiff: hint change visible in anon mode" ((runDiff envBase envHintChanged).any fun d => d.hintsChanged == #[(addrA, "regular(5)", "regular(6)")] && d.namedMetaOnly.isEmpty && d.namedChanged.isEmpty) ++ - test "EnvDiff: hint change flags metadata under meta mode" + test "EnvDiff: hint change is not a metadata change" ((runDiff envBase envHintChanged true).any fun d => - d.hintsChanged.size == 1 - && d.namedMetaOnly == #[("foo", #["meta.info"])]) ++ + d.hintsChanged.size == 1 && d.namedMetaOnly.isEmpty + && d.namedChanged.isEmpty) ++ test "EnvDiff: main change" ((runDiff { envBase with main := some addrA } envBase).any fun d => d.mainChanged == some (some addrA, none)) ++ diff --git a/Tests/Gen/Ixon.lean b/Tests/Gen/Ixon.lean index b001c0372..f89ebc961 100644 --- a/Tests/Gen/Ixon.lean +++ b/Tests/Gen/Ixon.lean @@ -356,7 +356,7 @@ def genConstantMeta : Gen ConstantMeta := do frequency [ (10, pure .empty), (15, ConstantMeta.defn <$> genAddress <*> genSmallArray genAddress - <*> genReducibilityHints <*> genSmallArray genAddress <*> genSmallArray genAddress + <*> genSmallArray genAddress <*> genSmallArray genAddress <*> pure arena <*> genRoot <*> genRoot), (15, ConstantMeta.axio <$> genAddress <*> genSmallArray genAddress <*> pure arena <*> genRoot), diff --git a/Tests/Ix/Compile.lean b/Tests/Ix/Compile.lean index 7efdf0003..f32d232d1 100644 --- a/Tests/Ix/Compile.lean +++ b/Tests/Ix/Compile.lean @@ -222,7 +222,7 @@ def testCrossImpl : TestSeq := IO.println s!" [{i}] {reprStr arena.nodes[i]!}" let dumpMeta (label : String) (cm : Ixon.ConstantMeta) : IO Unit := do match cm with - | .defn _ _ _ _ _ arena typeRoot valueRoot => do + | .defn _ _ _ _ arena typeRoot valueRoot => do dumpArena label "arena" arena IO.println s!" {label} typeRoot={typeRoot} valueRoot={valueRoot}" | .axio _ _ arena typeRoot => do @@ -261,10 +261,9 @@ def testCrossImpl : TestSeq := IO.println s!" variant: {leanTag}" -- Field-by-field comparison for common variants match leanCM, rustCM with - | .defn ln ll lh la lc larena ltr lvr, .defn rn rl rh ra rc rarena rtr rvr => do + | .defn ln ll la lc larena ltr lvr, .defn rn rl ra rc rarena rtr rvr => do if ln != rn then IO.println s!" name DIFFERS: Lean={ln} Rust={rn}" if ll != rl then IO.println s!" lvls DIFFERS: Lean={ll.size} Rust={rl.size}" - if lh != rh then IO.println s!" hints DIFFERS" if la != ra then IO.println s!" all DIFFERS: Lean={la} Rust={ra}" if lc != rc then IO.println s!" ctx DIFFERS: Lean={lc} Rust={rc}" if larena != rarena then IO.println s!" arena DIFFERS: Lean={larena.nodes.size} Rust={rarena.nodes.size}" diff --git a/crates/compile/src/compile.rs b/crates/compile/src/compile.rs index 63a4cc6b4..993314bde 100644 --- a/crates/compile/src/compile.rs +++ b/crates/compile/src/compile.rs @@ -20,8 +20,9 @@ use ix_common::env::{ AxiomVal, BinderInfo, ConstantInfo as LeanConstantInfo, ConstructorVal, DataValue as LeanDataValue, Env as LeanEnv, Expr as LeanExpr, ExprData, InductiveVal, Level, LevelData, Literal, Name, NameData, QuotVal, - RecursorRule as LeanRecursorRule, SourceInfo as LeanSourceInfo, - Substring as LeanSubstring, Syntax as LeanSyntax, SyntaxPreresolved, + RecursorRule as LeanRecursorRule, ReducibilityHints, + SourceInfo as LeanSourceInfo, Substring as LeanSubstring, + Syntax as LeanSyntax, SyntaxPreresolved, }; use ix_common::strong_ordering::SOrd; @@ -168,6 +169,13 @@ pub struct CompileState { /// right after `aux_gen::generate_aux_patches`. Blocks without nested /// auxiliaries simply aren't inserted. pub aux_perms: DashMap, + /// Reducibility hints per definition NAME, recorded by + /// `compile_definition` (the only place the Lean-side hints are in + /// scope — hints are not part of `ConstantMeta`). The constant + /// address a name resolves to isn't final until its `Named` entry is + /// registered, so [`Self::finalize_hints`] resolves this map through + /// `env.named` into `env.anon_hints` once compilation completes. + pub def_hints: DashMap, } /// Cached compiled expression with arena root index. @@ -228,6 +236,7 @@ impl Default for CompileState { brec_on_call_site_plans: Default::default(), below_call_site_plans: Default::default(), aux_perms: Default::default(), + def_hints: Default::default(), } } } @@ -264,6 +273,21 @@ impl CompileState { self.resolve_addr_aux(name, true) } + /// Resolve the per-name hints recorded by `compile_definition` into + /// `env.anon_hints`, keyed by each name's registered constant address + /// (`Named.addr` — the projection address for mutual-block members, + /// i.e. exactly the address the kernel looks hints up under). Runs + /// once after the scheduler drains: addresses aren't final until the + /// `Named` entries are registered. Alias collisions resolve through + /// `Env::register_hint`'s order-independent merge. + pub fn finalize_hints(&self) { + for entry in self.env.named.iter() { + if let Some(h) = self.def_hints.get(entry.key()) { + self.env.register_hint(entry.value().addr.clone(), *h.value()); + } + } + } + /// Promote a constant from `aux_name_to_addr` to `name_to_addr`, setting /// `Named.original` to the given `(orig_addr, orig_meta)` from the /// ephemeral no-aux compilation. The existing aux_gen `Named` entry keeps @@ -2219,7 +2243,6 @@ pub fn compile_definition( let mut meta = ConstantMeta::new(ConstantMetaInfo::Def { name: name_addr, lvls: lvl_addrs, - hints: def.hints, all: all_addrs, ctx: ctx_addrs, arena, @@ -2227,6 +2250,7 @@ pub fn compile_definition( value_root, }); meta.meta_sharing = surgery_sharing; + stt.def_hints.insert(def.name.clone(), def.hints); Ok((data, meta)) } diff --git a/crates/compile/src/compile/env.rs b/crates/compile/src/compile/env.rs index 1afba1661..ca7b4d636 100644 --- a/crates/compile/src/compile/env.rs +++ b/crates/compile/src/compile/env.rs @@ -972,6 +972,8 @@ pub fn compile_env_with_options( }); } + stt.finalize_hints(); + if !*IX_QUIET { let total_elapsed = compile_start.elapsed().as_secs_f64(); eprintln!( diff --git a/crates/compile/src/decompile.rs b/crates/compile/src/decompile.rs index 536b13816..db94ac238 100644 --- a/crates/compile/src/decompile.rs +++ b/crates/compile/src/decompile.rs @@ -1351,14 +1351,25 @@ fn decompile_definition( dstt, )?; - let (hints, all) = match &meta.info { - ConstantMetaInfo::Def { hints, all, .. } => { + let all = match &meta.info { + ConstantMetaInfo::Def { all, .. } => { let all_names: Result, _> = all.iter().map(|a| decompile_name(a, stt)).collect(); - (*hints, all_names?) + all_names? }, - _ => (ReducibilityHints::Opaque, vec![]), + _ => vec![], }; + // Hints live in `env.anon_hints`, keyed by the constant address the + // name resolves to (for aux originals, the canonical address — the + // original was compiled from the same Lean definition, so the hints + // coincide). Absent entry → `Opaque`, matching the compiler's + // treatment of theorems and opaques. + let hints = stt + .env + .named + .get(&name) + .and_then(|n| stt.env.anon_hints.get(&n.value().addr).map(|r| *r)) + .unwrap_or(ReducibilityHints::Opaque); let cnst = ConstantVal { name, level_params, typ }; @@ -5473,7 +5484,6 @@ mod tests { let mut meta = ConstantMeta::new(ConstantMetaInfo::Def { name: f_addr_name.clone(), lvls: vec![], - hints: ReducibilityHints::Opaque, all: vec![f_addr_name.clone()], ctx: vec![f_addr_name.clone()], arena, diff --git a/crates/ffi/src/lean.rs b/crates/ffi/src/lean.rs index dab1d3e74..20ae247ab 100644 --- a/crates/ffi/src/lean.rs +++ b/crates/ffi/src/lean.rs @@ -56,11 +56,11 @@ lean_ffi::lean_inductive! { LeanIxonRawEnv [ { num_obj: 8 } ]; // Lazy/anon deserialization (`rs_de_env_lazy`): zero-copy const windows - // (addr + offset + len), name->addr + hint, copied blobs, and the - // bundle header fields (main, assumptions). + // (addr + offset + len), name->addr, copied blobs, the bundle header + // fields (main, assumptions), and the hints-section pairs. LeanIxonRawConstSlice [ { num_obj: 1, num_64: 2 } ]; - LeanIxonRawNamedLite [ { num_obj: 2, num_64: 2 } ]; - LeanIxonRawEnvLazy [ { num_obj: 5 } ]; + LeanIxonRawNamedLite [ { num_obj: 2 } ]; + LeanIxonRawEnvLazy [ { num_obj: 6 } ]; // Env diff report (`rs_diff_envs`). Slot counts MUST match the Lean // structures in Ix/Ixon.lean (Ixon.EnvStats / NamedDiff / EnvDiff). @@ -110,7 +110,7 @@ lean_ffi::lean_inductive! { LeanIxonConstantMeta [ { }, // tag 0: empty (scalar) - { num_obj: 6, num_64: 2 }, // tag 1: defn + { num_obj: 5, num_64: 2 }, // tag 1: defn { num_obj: 3, num_64: 1 }, // tag 2: axio { num_obj: 3, num_64: 1 }, // tag 3: quot { num_obj: 6, num_64: 1 }, // tag 4: indc diff --git a/crates/ffi/src/lean_ixon/env.rs b/crates/ffi/src/lean_ixon/env.rs index e2a5dcd88..39ab800de 100644 --- a/crates/ffi/src/lean_ixon/env.rs +++ b/crates/ffi/src/lean_ixon/env.rs @@ -337,7 +337,7 @@ pub fn set_raw_env_bundle_fields( assumptions_arr.set(i, LeanIxAddress::build(addr)); } let mut hints: Vec<(Address, ReducibilityHints)> = - env.anon_hints.iter().map(|(a, h)| (a.clone(), *h)).collect(); + env.anon_hints.iter().map(|e| (e.key().clone(), *e.value())).collect(); hints.sort_unstable_by(|a, b| a.0.cmp(&b.0)); let hints_arr = LeanArray::alloc(hints.len()); for (i, (addr, hint)) in hints.iter().enumerate() { @@ -486,7 +486,7 @@ pub fn ixon_env_to_decoded(env: &IxonEnv) -> Result { let mut assumptions: Vec
= env.assumptions.iter().cloned().collect(); assumptions.sort_unstable(); let mut anon_hints: Vec<(Address, ReducibilityHints)> = - env.anon_hints.iter().map(|(a, h)| (a.clone(), *h)).collect(); + env.anon_hints.iter().map(|e| (e.key().clone(), *e.value())).collect(); anon_hints.sort_unstable_by(|a, b| a.0.cmp(&b.0)); Ok(DecodedRawEnv { consts, @@ -608,17 +608,6 @@ pub extern "C" fn rs_de_env_anon( // closure it actually checks. See `Ix.Ixon.deEnvAnon`. // ============================================================================= -/// Encode an optional reducibility hint as `(kind, val)` for the FFI: -/// `0` = none (not a Defn), `1` = Opaque, `2` = Abbrev, `3` = Regular(val). -fn encode_hint(hint: &Option) -> (u64, u64) { - match hint { - None => (0, 0), - Some(ReducibilityHints::Opaque) => (1, 0), - Some(ReducibilityHints::Abbrev) => (2, 0), - Some(ReducibilityHints::Regular(n)) => (3, u64::from(*n)), - } -} - impl LeanIxonRawConstSlice { /// Build `Ixon.RawConstSlice { addr, offset, len }`. pub fn build(addr: &Address, offset: usize, len: usize) -> Self { @@ -631,19 +620,15 @@ impl LeanIxonRawConstSlice { } impl LeanIxonRawNamedLite { - /// Build `Ixon.RawNamedLite { name, addr, hintKind, hintVal }`. + /// Build `Ixon.RawNamedLite { name, addr }`. pub fn build( cache: &mut LeanBuildCache, name: &Name, addr: &Address, - hint: &Option, ) -> Self { - let (kind, val) = encode_hint(hint); let ctor = LeanIxonRawNamedLite::alloc(0); ctor.set_obj(0, LeanIxName::build(cache, name)); ctor.set_obj(1, LeanIxAddress::build(addr)); - ctor.set_num_64(0, kind); - ctor.set_num_64(1, val); ctor } } @@ -659,10 +644,7 @@ fn build_raw_env_lazy(index: &LazyIndex) -> LeanIxonRawEnvLazy { let named_arr = LeanArray::alloc(index.named.len()); for (i, n) in index.named.iter().enumerate() { - named_arr.set( - i, - LeanIxonRawNamedLite::build(&mut cache, &n.name, &n.addr, &n.hint), - ); + named_arr.set(i, LeanIxonRawNamedLite::build(&mut cache, &n.name, &n.addr)); } let blobs_arr = LeanArray::alloc(index.blobs.len()); @@ -679,12 +661,24 @@ fn build_raw_env_lazy(index: &LazyIndex) -> LeanIxonRawEnvLazy { assumptions_arr.set(i, LeanIxAddress::build(addr)); } + let hints_arr = LeanArray::alloc(index.hints.len()); + for (i, (addr, hint)) in index.hints.iter().enumerate() { + hints_arr.set( + i, + LeanProd::new( + LeanIxAddress::build(addr), + LeanIxReducibilityHints::build(hint), + ), + ); + } + let ctor = LeanIxonRawEnvLazy::alloc(0); ctor.set_obj(0, consts_arr); ctor.set_obj(1, named_arr); ctor.set_obj(2, blobs_arr); ctor.set_obj(3, main_obj); ctor.set_obj(4, assumptions_arr); + ctor.set_obj(5, hints_arr); ctor } diff --git a/crates/ffi/src/lean_ixon/meta.rs b/crates/ffi/src/lean_ixon/meta.rs index 5c8af7c00..844a68277 100644 --- a/crates/ffi/src/lean_ixon/meta.rs +++ b/crates/ffi/src/lean_ixon/meta.rs @@ -3,9 +3,8 @@ //! Includes: DataValue, KVMap, ExprMetaData, ExprMetaArena, ConstantMeta, Named, Comm use crate::lean::{ - LeanIxReducibilityHints, LeanIxonComm, LeanIxonConstantMeta, - LeanIxonDataValue, LeanIxonExprMetaArena, LeanIxonExprMetaData, - LeanIxonNamed, + LeanIxonComm, LeanIxonConstantMeta, LeanIxonDataValue, LeanIxonExprMetaArena, + LeanIxonExprMetaData, LeanIxonNamed, }; use ix_common::address::Address; use ix_common::env::BinderInfo; @@ -349,7 +348,7 @@ impl LeanIxonConstantMeta { /// | Variant | Tag | Obj fields | Scalar bytes | /// |---------|-----|-----------|-------------| /// | empty | 0 | 0 | 0 | - /// | defn | 1 | 6 (name, lvls, hints, all, ctx, arena) | 16 (2× u64) | + /// | defn | 1 | 5 (name, lvls, all, ctx, arena) | 16 (2× u64) | /// | axio | 2 | 3 (name, lvls, arena) | 8 (1× u64) | /// | quot | 3 | 3 (name, lvls, arena) | 8 (1× u64) | /// | indc | 4 | 6 (name, lvls, ctors, all, ctx, arena) | 8 (1× u64) | @@ -363,7 +362,6 @@ impl LeanIxonConstantMeta { ConstantMetaInfo::Def { name, lvls, - hints, all, ctx, arena, @@ -373,10 +371,9 @@ impl LeanIxonConstantMeta { let ctor = LeanIxonConstantMeta::alloc(1); ctor.set_obj(0, LeanIxAddress::build(name)); ctor.set_obj(1, LeanIxAddress::build_array(lvls)); - ctor.set_obj(2, LeanIxReducibilityHints::build(hints)); - ctor.set_obj(3, LeanIxAddress::build_array(all)); - ctor.set_obj(4, LeanIxAddress::build_array(ctx)); - ctor.set_obj(5, LeanIxonExprMetaArena::build(arena)); + ctor.set_obj(2, LeanIxAddress::build_array(all)); + ctor.set_obj(3, LeanIxAddress::build_array(ctx)); + ctor.set_obj(4, LeanIxonExprMetaArena::build(arena)); ctor.set_num_64(0, *type_root); ctor.set_num_64(1, *value_root); ctor @@ -486,18 +483,15 @@ impl LeanIxonConstantMeta { LeanIxAddress::from_borrowed(self.get_obj(0).as_byte_array()) .decode(); let lvls = decode_address_array(self.get_obj(1).as_array()); - let hints = - LeanIxReducibilityHints::new(self.get_obj(2).to_owned_ref()).decode(); - let all = decode_address_array(self.get_obj(3).as_array()); - let ctx = decode_address_array(self.get_obj(4).as_array()); + let all = decode_address_array(self.get_obj(2).as_array()); + let ctx = decode_address_array(self.get_obj(3).as_array()); let arena = - LeanIxonExprMetaArena::new(self.get_obj(5).to_owned_ref()).decode(); + LeanIxonExprMetaArena::new(self.get_obj(4).to_owned_ref()).decode(); let type_root = self.get_num_64(0); let value_root = self.get_num_64(1); ConstantMeta::new(ConstantMetaInfo::Def { name, lvls, - hints, all, ctx, arena, diff --git a/crates/ffi/src/lean_ixon/serialize.rs b/crates/ffi/src/lean_ixon/serialize.rs index e681802ac..ef29caafd 100644 --- a/crates/ffi/src/lean_ixon/serialize.rs +++ b/crates/ffi/src/lean_ixon/serialize.rs @@ -258,26 +258,18 @@ pub extern "C" fn rs_eq_env_serialization( return false; } - // Hints: the writers derive §3 from Named `Def` metadata when the - // explicit map is empty, so the parsed env's hints must equal the - // same derivation over the decoded RawEnv. + // Hints: `anon_hints` is the single home for hints (the writers + // serialize the map directly), so the parsed env's map must equal + // the decoded RawEnv's hints verbatim. let expected_hints: rustc_hash::FxHashMap< Address, ix_common::env::ReducibilityHints, - > = if decoded.anon_hints.is_empty() { - let mut derived = rustc_hash::FxHashMap::default(); - for rn in &decoded.named { - if let ixon::metadata::ConstantMetaInfo::Def { hints, .. } = - &rn.const_meta.info - { - derived.entry(rn.addr.clone()).or_insert(*hints); - } - } - derived - } else { - decoded.anon_hints.iter().cloned().collect() - }; - if rust_env.anon_hints != expected_hints { + > = decoded.anon_hints.iter().cloned().collect(); + let hints_match = rust_env.anon_hints.len() == expected_hints.len() + && expected_hints + .iter() + .all(|(a, h)| rust_env.anon_hints.get(a).map(|r| *r) == Some(*h)); + if !hints_match { if debug { eprintln!( "[rs_eq_env_serialization] anon_hints mismatch: rust={}, expected={}", diff --git a/crates/ixon/src/diff.rs b/crates/ixon/src/diff.rs index 70d2911c7..7981cc7af 100644 --- a/crates/ixon/src/diff.rs +++ b/crates/ixon/src/diff.rs @@ -1248,20 +1248,22 @@ fn diff_envs_impl( // Hints, joined on constants present in both envs. let shared = |addr: &Address| a.consts.contains_key(addr) && b.consts.contains_key(addr); - for (addr, ha) in &a.anon_hints { + for entry in a.anon_hints.iter() { + let (addr, ha) = (entry.key(), entry.value()); if !shared(addr) { continue; } - let hb = b.anon_hints.get(addr); - if hb != Some(ha) { + let hb = b.anon_hints.get(addr).map(|r| *r); + if hb != Some(*ha) { d.hints_changed.push(( addr.clone(), hint_label(Some(ha)), - hint_label(hb), + hint_label(hb.as_ref()), )); } } - for (addr, hb) in &b.anon_hints { + for entry in b.anon_hints.iter() { + let (addr, hb) = (entry.key(), entry.value()); if shared(addr) && !a.anon_hints.contains_key(addr) { d.hints_changed.push(( addr.clone(), @@ -1597,7 +1599,6 @@ mod tests { let info = ConstantMetaInfo::Def { name: Address::hash(b"nm"), lvls: vec![], - hints: ReducibilityHints::Regular(1), all: vec![], ctx: vec![], arena: ExprMeta::default(), @@ -2323,15 +2324,17 @@ mod tests { addr } - fn def_meta(name_addr: Address, hint: u32) -> ConstantMeta { + /// `variant` lands in `type_root`, so two calls with different + /// variants produce metas that differ while the constant (and its + /// address) stays identical — a metadata-only difference. + fn def_meta(name_addr: Address, variant: u32) -> ConstantMeta { ConstantMeta::new(ConstantMetaInfo::Def { name: name_addr, lvls: vec![], - hints: ReducibilityHints::Regular(hint), all: vec![], ctx: vec![], arena: ExprMeta::default(), - type_root: 0, + type_root: u64::from(variant), value_root: 0, }) } @@ -2347,8 +2350,8 @@ mod tests { #[test] fn meta_sweep_matches_full_reader() { let build = |foo_value: Arc, - foo_hint: u32, - monly_hint: u32, + foo_variant: u32, + monly_variant: u32, foo_original: bool| -> Vec { let env = Env::new(); @@ -2357,7 +2360,7 @@ mod tests { let c = defn_c(Expr::var(3), foo_value); let addr = store_canonical(&env, &c); let mut foo_named = - Named::new(addr.clone(), def_meta(foo_comp, foo_hint)); + Named::new(addr.clone(), def_meta(foo_comp, foo_variant)); if foo_original { foo_named.set_original(addr, ConstantMeta::default()); } @@ -2369,7 +2372,7 @@ mod tests { let stable_addr = store_canonical(&env, &stable); env.register_name( monly.clone(), - Named::new(stable_addr, def_meta(monly_comp, monly_hint)), + Named::new(stable_addr, def_meta(monly_comp, monly_variant)), ); let mut bytes = Vec::new(); env.put(&mut bytes).expect("put failed"); diff --git a/crates/ixon/src/env.rs b/crates/ixon/src/env.rs index c4a036a65..a4bb3a1b8 100644 --- a/crates/ixon/src/env.rs +++ b/crates/ixon/src/env.rs @@ -1,6 +1,6 @@ //! Environment for storing Ixon data. -use rustc_hash::{FxHashMap, FxHashSet}; +use rustc_hash::FxHashSet; use std::collections::VecDeque; use std::sync::Arc; @@ -165,15 +165,14 @@ pub struct LazyConstSlice { pub len: usize, } -/// One named entry in a [`LazyIndex`]: just the `name → addr` mapping plus the -/// per-`Defn` reducibility hint (the only metadata the typecheck circuit -/// consumes). The heavy `ExprMetaArena` is parsed (to advance the cursor and -/// handle every metadata variant, e.g. `CallSite`) but discarded. +/// One named entry in a [`LazyIndex`]: just the `name → addr` mapping. +/// The heavy `ExprMetaArena` is parsed (to advance the cursor and +/// handle every metadata variant, e.g. `CallSite`) but discarded; +/// hints live on [`LazyIndex::hints`]. #[derive(Debug, Clone)] pub struct LazyNamed { pub name: Name, pub addr: Address, - pub hint: Option, } /// `IX_COMPILE_DEMOTE` (default **on**; set `0` to disable): store the @@ -227,7 +226,7 @@ pub struct LazyIndex { /// - `blobs`: Raw data (strings, nats, files) /// - `names`: Hash-consed Lean.Name components (Address -> Name) /// - `comms`: Cryptographic commitments (secrets) -#[derive(Debug, Default)] +#[derive(Debug, Default, Clone)] pub struct Env { /// Alpha-invariant constants: Address -> LazyConstant (raw bytes + /// optional materialized cache; see [`LazyConstant`]). @@ -240,20 +239,21 @@ pub struct Env { pub names: IxonMap, /// Cryptographic commitments: commitment Address -> Comm pub comms: IxonMap, - /// Reducibility hints sidecar harvested by [`Env::get_anon`] from the - /// otherwise-discarded Named section. Keyed by the constant's - /// projection/standalone address (i.e. `Named.addr` — the address the - /// kernel sees, **not** the name-hash address). Empty for envs loaded - /// via [`Env::get`] / [`Env::new`] / `store_*`; meta-mode ingress - /// pulls hints directly from `Named.meta` and ignores this field. + /// Reducibility hints, keyed by the constant's projection/standalone + /// address (i.e. `Named.addr` — the address the kernel sees, **not** + /// the name-hash address). The SINGLE home for hints: the compiler + /// registers them here ([`Env::register_hint`]), every writer + /// serializes this map as the file's hints section, and every reader + /// populates it from that section. Hints do not appear in `Named` + /// metadata. /// - /// Anon-mode ingress passes these hints through to - /// `ingress_defn` so the kernel's lazy-delta tiebreak - /// (`def_eq::def_rank_id`) sees realistic heights instead of the - /// constant `Regular(0)` fallback. Hints are performance advice — - /// supplying them in anon mode does not relax the kernel's - /// metadata-free correctness model. - pub anon_hints: FxHashMap, + /// Ingress passes these hints through to `ingress_defn` so the + /// kernel's lazy-delta tiebreak (`def_eq::def_rank_id`) sees + /// realistic heights instead of the constant `Regular(0)` fallback. + /// Hints are performance advice — supplying them does not relax the + /// kernel's metadata-free correctness model — and are intentionally + /// NOT covered by the consts merkle root. + pub anon_hints: IxonMap, /// Distinguished root constant for bundle envs; `None` for whole /// environments. A pointer, not a proof: nothing in the file /// authenticates it, so readers check `main ∈ consts` and consumers @@ -276,7 +276,7 @@ impl Env { blobs: IxonMap::new(), names: IxonMap::new(), comms: IxonMap::new(), - anon_hints: FxHashMap::default(), + anon_hints: IxonMap::new(), main: None, assumptions: FxHashSet::default(), } @@ -300,6 +300,38 @@ impl Env { self.blobs.get(addr).map(|r| r.clone()) } + /// Register a constant's reducibility hints (the compile-time + /// producer of [`Self::anon_hints`]; readers populate the map from + /// the file's hints section instead). + /// + /// Alpha-equivalent definitions share one constant address but may + /// carry different hints (e.g. one alias marked `@[reducible]`), and + /// parallel compile workers may race on the entry — so the winner + /// must not depend on arrival order. The merge keeps the minimum + /// under `(tag, height)` with `Opaque < Abbrev < Regular(h)`: + /// commutative, associative, idempotent, hence order-independent. + /// The Lean compiler mirror applies the same rule. + #[cfg(not(target_arch = "riscv64"))] + pub fn register_hint(&self, addr: Address, hints: ReducibilityHints) { + fn rank(h: &ReducibilityHints) -> (u8, u32) { + match h { + ReducibilityHints::Opaque => (0, 0), + ReducibilityHints::Abbrev => (1, 0), + ReducibilityHints::Regular(x) => (2, *x), + } + } + match self.anon_hints.entry(addr) { + dashmap::mapref::entry::Entry::Occupied(mut e) => { + if rank(&hints) < rank(e.get()) { + e.insert(hints); + } + }, + dashmap::mapref::entry::Entry::Vacant(e) => { + e.insert(hints); + }, + } + } + /// Store a structured constant under `addr`. /// /// Serializes the constant once. With demotion disabled, @@ -928,49 +960,6 @@ impl Env { } } -impl Clone for Env { - // `mut` is only needed on `riscv64` where `IxonMap` wraps `FxHashMap` and - // `insert` takes `&mut self`; on host `DashMap::insert` takes `&self`. - #[cfg_attr(not(target_arch = "riscv64"), allow(unused_mut))] - fn clone(&self) -> Self { - let mut consts = IxonMap::new(); - for entry in self.consts.iter() { - consts.insert(entry.key().clone(), entry.value().clone()); - } - - let mut named = IxonMap::new(); - for entry in self.named.iter() { - named.insert(entry.key().clone(), entry.value().clone()); - } - - let mut blobs = IxonMap::new(); - for entry in self.blobs.iter() { - blobs.insert(entry.key().clone(), entry.value().clone()); - } - - let mut names = IxonMap::new(); - for entry in self.names.iter() { - names.insert(entry.key().clone(), entry.value().clone()); - } - - let mut comms = IxonMap::new(); - for entry in self.comms.iter() { - comms.insert(entry.key().clone(), entry.value().clone()); - } - - Env { - consts, - named, - blobs, - names, - comms, - anon_hints: self.anon_hints.clone(), - main: self.main.clone(), - assumptions: self.assumptions.clone(), - } - } -} - #[cfg(test)] mod tests { use super::*; @@ -1495,7 +1484,6 @@ mod tests { let mut meta = ConstantMeta::new(ConstantMetaInfo::Def { name: name_addr.clone(), lvls: vec![], - hints: ReducibilityHints::Regular(3), all: vec![], ctx: vec![], arena: ExprMeta::default(), @@ -1504,6 +1492,7 @@ mod tests { }); meta.meta_refs.push(meta_blob.clone()); env.register_name(name.clone(), Named::new(a.clone(), meta)); + env.register_hint(a.clone(), ReducibilityHints::Regular(3)); let bundle = env.prune_to_closure(&a, &FxHashSet::default()).unwrap(); assert!(bundle.named.get(&name).is_some(), "named entry carried"); @@ -1522,12 +1511,15 @@ mod tests { bundle.get_blob(&Address::hash(b"Bundled")), Some(b"Bundled".to_vec()) ); - // Hints derive from the carried Def meta on serialization; the - // anon reader sees them without touching metadata sections. + // Hints are carried per constant by the prune; the anon reader + // sees them from the hints section without touching metadata. let mut buf = Vec::new(); bundle.put(&mut buf).unwrap(); let anon = Env::get_anon(&mut buf.as_slice()).unwrap(); - assert_eq!(anon.anon_hints.get(&a), Some(&ReducibilityHints::Regular(3))); + assert_eq!( + anon.anon_hints.get(&a).map(|r| *r), + Some(ReducibilityHints::Regular(3)) + ); } /// Fixture for the streaming/anon prune tests: `a` (the main) named @@ -1552,7 +1544,6 @@ mod tests { let mut meta = ConstantMeta::new(ConstantMetaInfo::Def { name: foo_addr, lvls: vec![u_addr], - hints: ReducibilityHints::Regular(2), all: vec![], ctx: vec![], arena: ExprMeta::default(), @@ -1563,6 +1554,7 @@ mod tests { let mut foo_named = Named::new(a.clone(), meta); foo_named.set_original(b.clone(), ConstantMeta::default()); env.register_name(foo, foo_named); + env.register_hint(a.clone(), ReducibilityHints::Regular(2)); let bar = n("Bar"); let bar_addr = Address::from_blake3_hash(*bar.get_hash()); env.store_name(bar_addr, bar.clone()); @@ -1646,9 +1638,11 @@ mod tests { !bundle.consts.contains_key(&b), "metadata-only edges must not be walked in anon mode" ); - // §3 hints derive from the source's Named Def metadata at write - // time and ride the lazy env's anon_hints into the bundle. - assert_eq!(bundle.anon_hints.get(&a), Some(&ReducibilityHints::Regular(2))); + // Hints ride the lazy env's anon_hints into the bundle. + assert_eq!( + bundle.anon_hints.get(&a).map(|r| *r), + Some(ReducibilityHints::Regular(2)) + ); bundle.validate_closed().unwrap(); let mut buf = Vec::new(); @@ -1662,6 +1656,9 @@ mod tests { assert!(back.names.len() <= 1, "§4 carries at most the anon entry"); assert_eq!(back.main, Some(a.clone())); let anon = Env::get_anon(&mut buf.as_slice()).unwrap(); - assert_eq!(anon.anon_hints.get(&a), Some(&ReducibilityHints::Regular(2))); + assert_eq!( + anon.anon_hints.get(&a).map(|r| *r), + Some(ReducibilityHints::Regular(2)) + ); } } diff --git a/crates/ixon/src/map.rs b/crates/ixon/src/map.rs index 748ebafb1..5d514782f 100644 --- a/crates/ixon/src/map.rs +++ b/crates/ixon/src/map.rs @@ -20,7 +20,7 @@ mod riscv_impl { use rustc_hash::FxHashMap; - #[derive(Debug)] + #[derive(Debug, Clone)] pub struct IxonMap(FxHashMap); impl Default for IxonMap { diff --git a/crates/ixon/src/metadata.rs b/crates/ixon/src/metadata.rs index d6557f372..315be9750 100644 --- a/crates/ixon/src/metadata.rs +++ b/crates/ixon/src/metadata.rs @@ -121,7 +121,6 @@ pub enum ConstantMetaInfo { Def { name: Address, lvls: Vec
, - hints: ReducibilityHints, all: Vec
, ctx: Vec
, arena: ExprMeta, @@ -1154,20 +1153,10 @@ impl ConstantMetaInfo { ) -> Result<(), String> { match self { Self::Empty => put_u8(255, buf), - Self::Def { - name, - lvls, - hints, - all, - ctx, - arena, - type_root, - value_root, - } => { + Self::Def { name, lvls, all, ctx, arena, type_root, value_root } => { put_u8(0, buf); put_idx(name, idx, buf)?; put_idx_vec(lvls, idx, buf)?; - hints.put_ser(buf); put_idx_vec(all, idx, buf)?; put_idx_vec(ctx, idx, buf)?; arena.put_with(idx, buf)?; @@ -1260,7 +1249,6 @@ impl ConstantMetaInfo { 0 => Ok(Self::Def { name: get_idx(buf, rev)?, lvls: get_idx_vec(buf, rev)?, - hints: ReducibilityHints::get_ser(buf)?, all: get_idx_vec(buf, rev)?, ctx: get_idx_vec(buf, rev)?, arena: ExprMeta::get_with(buf, rev)?, @@ -1399,7 +1387,6 @@ mod tests { let meta = ConstantMeta::new(ConstantMetaInfo::Def { name: addr1.clone(), lvls: vec![addr2.clone(), addr3.clone()], - hints: ReducibilityHints::Regular(10), all: vec![addr1.clone()], ctx: vec![addr2.clone()], arena, diff --git a/crates/ixon/src/serialize.rs b/crates/ixon/src/serialize.rs index 436574f13..e4981eeaf 100644 --- a/crates/ixon/src/serialize.rs +++ b/crates/ixon/src/serialize.rs @@ -1424,47 +1424,17 @@ impl Env { // ───────────────────────────────────────────────────────────────────── // Section 3: anon_hints (Address -> ReducibilityHints) // - // The canonical hint channel for the anon/lazy readers, placed - // before the metadata sections so `get_anon`/`get_anon_mmap` can - // stop right after it (they never touch names/named/comms). When - // the in-memory map is empty (the compile path: hints live in - // Named metadata), the section is derived from `named` — the same - // harvest `get_anon` historically did at read time, moved to - // write time. Hints are performance-only advice and intentionally + // The canonical hint channel, placed before the metadata sections + // so `get_anon`/`get_anon_mmap` can stop right after it (they + // never touch names/named/comms). `anon_hints` is the single home + // for hints: the compiler registers them per constant address + // (`Env::register_hint`) and readers fill the map from this very + // section. Hints are performance-only advice and intentionally // NOT covered by the consts merkle root. - // - // `named_keys` is collected and sorted here (by name hash — the - // Section 5 canonical order) and reused for Section 5 below; the - // sorted iteration makes the first-wins dedup by constant address - // deterministic when alpha-equivalent names share one constant. // ───────────────────────────────────────────────────────────────────── let sec_start = std::time::Instant::now(); - let mut named_keys: Vec = - self.named.iter().map(|e| e.key().clone()).collect(); - #[cfg(not(target_arch = "riscv64"))] - named_keys.par_sort_unstable_by(|a, b| { - a.get_hash().as_bytes().cmp(b.get_hash().as_bytes()) - }); - #[cfg(target_arch = "riscv64")] - named_keys.sort_unstable_by(|a, b| { - a.get_hash().as_bytes().cmp(b.get_hash().as_bytes()) - }); let mut hint_pairs: Vec<(Address, ReducibilityHints)> = - if self.anon_hints.is_empty() { - let mut derived: FxHashMap = - FxHashMap::default(); - for name in &named_keys { - if let Some(entry) = self.named.get(name) - && let super::metadata::ConstantMetaInfo::Def { hints, .. } = - &entry.value().meta().info - { - derived.entry(entry.value().addr.clone()).or_insert(*hints); - } - } - derived.into_iter().collect() - } else { - self.anon_hints.iter().map(|(a, h)| (a.clone(), *h)).collect() - }; + self.anon_hints.iter().map(|e| (e.key().clone(), *e.value())).collect(); hint_pairs.sort_unstable_by(|a, b| a.0.cmp(&b.0)); put_u64(hint_pairs.len() as u64, buf); for (addr, hints) in &hint_pairs { @@ -1527,13 +1497,24 @@ impl Env { // with metadata arenas), so the streaming pattern's win is greatest // here: on Mathlib, avoiding the clone-into-Vec saves ~30 GB peak RAM. // - // `named_keys` was collected and sorted (by cached name hash bytes) - // up in Section 3, where the hint derivation needs the same - // canonical order. + // Key clone cost: a `Name` is `Arc`, so each clone is a + // single atomic refcount increment (<1s for 733k). let sec_start = std::time::Instant::now(); if !quiet { eprintln!("[Env::put] section 5/6 named: {} entries", self.named.len(),); } + let mut named_keys: Vec = + self.named.iter().map(|e| e.key().clone()).collect(); + // Sort by the cached name hash bytes — the section's canonical + // order (ascending name hash, which is exactly `Name`'s `Ord`). + #[cfg(not(target_arch = "riscv64"))] + named_keys.par_sort_unstable_by(|a, b| { + a.get_hash().as_bytes().cmp(b.get_hash().as_bytes()) + }); + #[cfg(target_arch = "riscv64")] + named_keys.sort_unstable_by(|a, b| { + a.get_hash().as_bytes().cmp(b.get_hash().as_bytes()) + }); let put_start = std::time::Instant::now(); put_u64(named_keys.len() as u64, buf); for name in &named_keys { @@ -1676,31 +1657,10 @@ impl Env { written += bytes.len() as u64; } } - // Section 3: anon_hints — the canonical hint channel. Always - // emitted; when the in-memory map is empty it is derived from Named - // `Def` metadata in hash-sorted name order, mirroring `Env::put` - // exactly (same iteration order → same `or_insert` winners). - let mut named_keys: Vec = - self.named.iter().map(|e| e.key().clone()).collect(); - named_keys.par_sort_unstable_by(|a, b| { - a.get_hash().as_bytes().cmp(b.get_hash().as_bytes()) - }); + // Section 3: anon_hints — the canonical hint channel, serialized + // straight from the map (see `Env::put`). let mut hint_pairs: Vec<(Address, ReducibilityHints)> = - if self.anon_hints.is_empty() { - let mut derived: FxHashMap = - FxHashMap::default(); - for name in &named_keys { - if let Some(entry) = self.named.get(name) - && let super::metadata::ConstantMetaInfo::Def { hints, .. } = - &entry.value().meta().info - { - derived.entry(entry.value().addr.clone()).or_insert(*hints); - } - } - derived.into_iter().collect() - } else { - self.anon_hints.iter().map(|(a, h)| (a.clone(), *h)).collect() - }; + self.anon_hints.iter().map(|e| (e.key().clone(), *e.value())).collect(); hint_pairs.sort_unstable_by(|a, b| a.0.cmp(&b.0)); put_u64(hint_pairs.len() as u64, &mut buf); for (addr, hints) in &hint_pairs { @@ -1726,6 +1686,11 @@ impl Env { // and re-encode through the name index). Chunks encode in parallel // into per-entry buffers and drain to the writer in order; the // chunk size bounds staged memory to a few MiB. + let mut named_keys: Vec = + self.named.iter().map(|e| e.key().clone()).collect(); + named_keys.par_sort_unstable_by(|a, b| { + a.get_hash().as_bytes().cmp(b.get_hash().as_bytes()) + }); put_u64(named_keys.len() as u64, &mut buf); emit!(); for chunk in named_keys.chunks(4096) { @@ -1957,13 +1922,9 @@ impl Env { index.consts.push(LazyConstSlice { addr, offset, len }); } - // Section 3: anon_hints — the canonical hint channel (the writer - // always emits it, deriving from Named metadata when needed), so - // `LazyNamed.hint` is a plain lookup instead of a metadata harvest. - // Kept verbatim on the index for full-reader parity. + // Section 3: anon_hints — kept verbatim on the index for + // full-reader parity. index.hints = read_hints_section(&mut buf)?; - let hints_map: FxHashMap = - index.hints.iter().cloned().collect(); // Section 4: Names — parsed to build the index for metadata // decoding. The reverse index is retained on the LazyIndex so §5 @@ -1983,10 +1944,10 @@ impl Env { } index.name_reverse_index = name_reverse_index; - // Section 5: Named — keep `name → addr` plus the §3 hint for that - // address; the full ConstantMeta (arena, CallSite, ...) is parsed - // then discarded. The section offset is recorded so a - // [`NamedMetaCursor`] can re-walk it without re-parsing §1–§4. + // Section 5: Named — keep `name → addr`; the full ConstantMeta + // (arena, CallSite, ...) is parsed then discarded. The section + // offset is recorded so a [`NamedMetaCursor`] can re-walk it + // without re-parsing the earlier sections. index.named_section_offset = data.len() - buf.len(); let num_named = get_u64(&mut buf)?; for _ in 0..num_named { @@ -1995,8 +1956,7 @@ impl Env { let name = names_lookup.get(&name_addr).cloned().ok_or_else(|| { format!("parse_lazy_index: missing name for addr {:?}", name_addr) })?; - let hint = hints_map.get(&named.addr).copied(); - index.named.push(LazyNamed { name, addr: named.addr, hint }); + index.named.push(LazyNamed { name, addr: named.addr }); } // Section 6: Comms — carried verbatim (tiny; empty for @@ -2404,23 +2364,10 @@ impl Env { } let consts_size = buf.len() - before_consts; - // Section 3: anon_hints (mirrors Env::put's derive-from-named rule) + // Section 3: anon_hints (serialized straight from the map) let before_hints = buf.len(); let mut hint_pairs: Vec<(Address, ReducibilityHints)> = - if self.anon_hints.is_empty() { - let mut derived: FxHashMap = - FxHashMap::default(); - for entry in self.named.iter() { - if let super::metadata::ConstantMetaInfo::Def { hints, .. } = - &entry.value().meta().info - { - derived.entry(entry.value().addr.clone()).or_insert(*hints); - } - } - derived.into_iter().collect() - } else { - self.anon_hints.iter().map(|(a, h)| (a.clone(), *h)).collect() - }; + self.anon_hints.iter().map(|e| (e.key().clone(), *e.value())).collect(); hint_pairs.sort_unstable_by(|a, b| a.0.cmp(&b.0)); put_u64(hint_pairs.len() as u64, &mut buf); for (addr, hints) in &hint_pairs { @@ -2730,11 +2677,8 @@ mod tests { env.assumptions.insert(Address::arbitrary(g)); } - // Explicit anon_hints (keyed by arbitrary addresses — the map is - // advisory). When left empty, `Env::put` derives §3 from Named - // metadata instead; gen_env metas are all `Empty`, so that - // derivation contributes nothing and roundtrip equality holds - // either way. + // anon_hints (keyed by arbitrary addresses — the map is advisory + // and the hints section is serialized straight from it). let num_hints = gen_range(g, 0..4); for _ in 0..num_hints { let variant: u8 = Arbitrary::arbitrary(g); @@ -2858,7 +2802,11 @@ mod tests { ); return false; } - if env.anon_hints != recovered.anon_hints { + let hints_match = env.anon_hints.len() == recovered.anon_hints.len() + && env.anon_hints.iter().all(|e| { + recovered.anon_hints.get(e.key()).map(|r| *r) == Some(*e.value()) + }); + if !hints_match { eprintln!( "anon_hints mismatch: {} vs {} entries", env.anon_hints.len(), @@ -3365,46 +3313,44 @@ mod tests { /// §3 is the canonical hint channel: with an empty `anon_hints` map /// the writer derives the section from Named `Def` metadata, and an /// env carrying the same hints explicitly serializes byte-identically. + /// The hints section round-trips through both the anon and full + /// readers, and `register_hint`'s merge is order-independent on + /// address collisions. #[test] - fn env_hints_derived_from_named_metadata() { - use crate::env::Named; - use crate::metadata::{ConstantMetaInfo, ExprMeta}; - + fn env_hints_roundtrip_and_merge_deterministic() { let env = Env::new(); let const_addr = store_canonical(&env, defn_const(vec![])); - let name = Name::str(Name::anon(), "hinted".to_string()); - let name_addr = Address::from_blake3_hash(*name.get_hash()); - env.names.insert(name_addr.clone(), name.clone()); - let meta = ConstantMeta::new(ConstantMetaInfo::Def { - name: name_addr, - lvls: vec![], - hints: ReducibilityHints::Regular(7), - all: vec![], - ctx: vec![], - arena: ExprMeta::default(), - type_root: 0, - value_root: 0, - }); - env.named.insert(name, Named::new(const_addr.clone(), meta)); + env.register_hint(const_addr.clone(), ReducibilityHints::Regular(7)); - // Empty map → §3 derived from Named at write time; the anon - // reader picks it up without ever parsing the Named section. let mut buf = Vec::new(); env.put(&mut buf).unwrap(); let anon = Env::get_anon(&mut buf.as_slice()).unwrap(); assert_eq!( - anon.anon_hints.get(&const_addr), - Some(&ReducibilityHints::Regular(7)) + anon.anon_hints.get(&const_addr).map(|r| *r), + Some(ReducibilityHints::Regular(7)) + ); + let full = Env::get(&mut buf.as_slice()).unwrap(); + assert_eq!( + full.anon_hints.get(&const_addr).map(|r| *r), + Some(ReducibilityHints::Regular(7)) ); - // Explicit map with identical content → identical bytes. - let mut env2 = env.clone(); - env2.anon_hints.insert(const_addr, ReducibilityHints::Regular(7)); - let mut buf2 = Vec::new(); - env2.put(&mut buf2).unwrap(); + // Alias collision: registration order must not affect the winner. + let a = Env::new(); + let ca = store_canonical(&a, defn_const(vec![])); + a.register_hint(ca.clone(), ReducibilityHints::Regular(9)); + a.register_hint(ca.clone(), ReducibilityHints::Abbrev); + let b = Env::new(); + let cb = store_canonical(&b, defn_const(vec![])); + b.register_hint(cb.clone(), ReducibilityHints::Abbrev); + b.register_hint(cb.clone(), ReducibilityHints::Regular(9)); + assert_eq!( + a.anon_hints.get(&ca).map(|r| *r), + b.anon_hints.get(&cb).map(|r| *r) + ); assert_eq!( - buf, buf2, - "derived and explicit hint sections should serialize identically" + a.anon_hints.get(&ca).map(|r| *r), + Some(ReducibilityHints::Abbrev) ); } } diff --git a/crates/ixvm-codegen/src/aiur_ixvm_witness.rs b/crates/ixvm-codegen/src/aiur_ixvm_witness.rs index ead830954..cda5885ca 100644 --- a/crates/ixvm-codegen/src/aiur_ixvm_witness.rs +++ b/crates/ixvm-codegen/src/aiur_ixvm_witness.rs @@ -191,7 +191,7 @@ fn add_entries_parallel( // Hints come from env.anon_hints (sidecar). Collect per chunk. for addr in chunk { if let Some(h) = env.anon_hints.get(addr) { - p.hints.push((addr_key(addr), hint_to_g(h))); + p.hints.push((addr_key(addr), hint_to_g(&h))); } } p diff --git a/crates/kernel/src/anon_work.rs b/crates/kernel/src/anon_work.rs index 5ffe10377..138aacbc1 100644 --- a/crates/kernel/src/anon_work.rs +++ b/crates/kernel/src/anon_work.rs @@ -232,7 +232,7 @@ pub fn build_sub_env( #[cfg(not(target_arch = "riscv64"))] fn sub_env_of(source: &IxonEnv, roots: &[Address]) -> IxonEnv { let closure = closure_addrs(source, roots); - let mut sub = IxonEnv::new(); + let sub = IxonEnv::new(); for addr in &closure { if let Some(bytes) = source.get_const_bytes(addr) { sub.store_const_lazy(addr.clone(), bytes); @@ -241,10 +241,8 @@ fn sub_env_of(source: &IxonEnv, roots: &[Address]) -> IxonEnv { } // else: external ref absent from `source` — omit; stays an open assumption. // Carry the constant's reducibility hint so the guest reproduces vanilla - // kernel behavior. The sub-env has no Named section to derive the §3 - // hints from at serialization time, so populate the map explicitly; - // without hints the kernel forces `Regular(0)` and does extra def-eq - // work (the ~30% check overhead). + // kernel behavior; without hints the kernel forces `Regular(0)` and does + // extra def-eq work (the ~30% check overhead). if let Some(h) = source.anon_hints.get(addr) { sub.anon_hints.insert(addr.clone(), *h); } diff --git a/crates/kernel/src/ingress.rs b/crates/kernel/src/ingress.rs index ad6660daa..7d7ad8fe1 100644 --- a/crates/kernel/src/ingress.rs +++ b/crates/kernel/src/ingress.rs @@ -1396,45 +1396,30 @@ fn ingress_defn( // projection addresses; passing `Some(_)` skips the metadata-derived // `build_mut_ctx` call. Meta callers pass `None`. mut_ctx_override: Option>>, - // Anon callers may supply `Some(hints)` to override the default - // `Regular(0)` fall-through when the .ixe carries `Env::anon_hints` - // (harvested by `Env::get_anon` from the otherwise-discarded Named - // metadata). Meta callers pass `None` and pull hints from - // `meta.info` like usual. The override only takes effect when - // `meta.info` is not `Def` (i.e. anon path with empty meta). - hints_override: Option, ) -> Result, KConst)>, String> { let mut cache: ExprCache = FxHashMap::default(); let mut univ_cache: UnivCache = FxHashMap::default(); - let (level_params, arena, type_root, value_root, hints, safety, all_addrs) = - match &meta.info { - ConstantMetaInfo::Def { - lvls, - arena, - type_root, - value_root, - hints, - all, - .. - } => ( - resolve_level_params(lvls, names), - arena, - *type_root, - *value_root, - *hints, - def.safety, - all.clone(), - ), - _ => ( - vec![], - &DEFAULT_ARENA, - 0, - 0, - hints_override.unwrap_or(ReducibilityHints::Regular(0)), - def.safety, - vec![], - ), - }; + // Hints live only in `Env::anon_hints`, keyed by the constant's own + // address, in both anon and meta modes. Without an entry the kernel + // falls back to `Regular(0)` — always correct, just more def-eq work. + let hints = ixon_env + .anon_hints + .get(&self_id.addr) + .map_or(ReducibilityHints::Regular(0), |r| *r); + let safety = def.safety; + let (level_params, arena, type_root, value_root, all_addrs) = match &meta.info + { + ConstantMetaInfo::Def { + lvls, arena, type_root, value_root, all, .. + } => ( + resolve_level_params(lvls, names), + arena, + *type_root, + *value_root, + all.clone(), + ), + _ => (vec![], &DEFAULT_ARENA, 0, 0, vec![]), + }; let mut_ctx = match mut_ctx_override { Some(m) => m, @@ -1656,7 +1641,6 @@ fn ingress_standalone( intern, stats, None, - None, ), IxonCI::Axio(ax) => { @@ -2052,7 +2036,6 @@ fn ingress_muts_block( intern, stats, None, - None, )?); }, } @@ -3683,8 +3666,8 @@ fn drop_ixon_env(_ixon_env: IxonEnv, _quiet: bool) { #[cfg(not(target_arch = "riscv64"))] fn drop_ixon_env(ixon_env: IxonEnv, quiet: bool) { let total_start = Instant::now(); - // `anon_hints` is a small FxHashMap (one entry per Def from the .ixe's - // hints section); `main`/`assumptions` are a single address and a small + // `anon_hints` is small (one entry per Def from the .ixe's hints + // section); `main`/`assumptions` are a single address and a small // set. Dropping them inline alongside the bookkeeping below is // negligible compared to the DashMap dropdance. // `..` covers the env's private fields. @@ -4246,7 +4229,6 @@ fn ingress_anon_standalone( let empty_n2a: FxHashMap = FxHashMap::default(); let mut convert_stats = ConvertStats::new(false); let self_id: KId = KId::new(addr.clone(), ()); - let hints_override = anon_env.anon_hints.get(addr).copied(); let entries = match &constant.info { IxonCI::Defn(def) => ingress_defn::( @@ -4263,7 +4245,6 @@ fn ingress_anon_standalone( &mut kenv.intern, &mut convert_stats, Some(vec![self_id.clone()]), - hints_override, )?, IxonCI::Recr(rec) => ingress_recursor::( rec, @@ -4474,7 +4455,6 @@ pub fn ingress_anon_block( )?; let self_id = KId::::new(proj_addr.clone(), ()); member_kids.push(self_id.clone()); - let hints_override = anon_env.anon_hints.get(&proj_addr).copied(); let entries = ingress_defn::( def, @@ -4490,7 +4470,6 @@ pub fn ingress_anon_block( &mut kenv.intern, &mut convert_stats, Some(mut_ctx.clone()), - hints_override, )?; all_entries.extend(entries); }, diff --git a/docs/Ixon.md b/docs/Ixon.md index 52cedb067..558e4df4a 100644 --- a/docs/Ixon.md +++ b/docs/Ixon.md @@ -34,7 +34,7 @@ Every `Constant` in Ixon is serialized and hashed with blake3. The resulting 256 The Ixon format separates: - **Alpha-invariant data** (`Constant`): The mathematical content, hashed for addressing -- **Metadata** (`ConstantMeta`, `ExprMeta`): Names, binder info, reducibility hints—stored separately +- **Metadata** (`ConstantMeta`, `ExprMeta`): Names and binder info—stored separately (reducibility hints live at the environment level, in `Env::anon_hints`) This separation means cosmetic changes (renaming variables) don't change the constant's address. @@ -690,7 +690,7 @@ Per-constant metadata. Each variant stores a name, universe parameter names, an ```rust pub enum ConstantMeta { Empty, // tag 255 - Def { name, lvls, hints, all, ctx, + Def { name, lvls, all, ctx, arena, type_root, value_root }, // tag 0 Axio { name, lvls, arena, type_root }, // tag 1 Quot { name, lvls, arena, type_root }, // tag 2 @@ -706,7 +706,7 @@ pub enum ConstantMeta { | Tag | Variant | Payload | |-----|---------|---------| -| 0 | Def | name_idx, lvl_idxs, hints, all_idxs, ctx_idxs, arena, type_root, value_root | +| 0 | Def | name_idx, lvl_idxs, all_idxs, ctx_idxs, arena, type_root, value_root | | 1 | Axio | name_idx, lvl_idxs, arena, type_root | | 2 | Quot | name_idx, lvl_idxs, arena, type_root | | 3 | Indc | name_idx, lvl_idxs, ctor_idxs, all_idxs, ctx_idxs, arena, type_root | @@ -863,13 +863,13 @@ count (Tag0) [Address (32 bytes) + ReducibilityHints]* ``` -The canonical hint channel for the anon/lazy readers, keyed by -constant address and sorted ascending. Writers ALWAYS emit this -section: when the in-memory hint map is empty (the compile path — -hints live in Named metadata), the section is derived from the Named -entries' `Def` metadata at write time. Hints are performance-only -advice (the `Regular(0)` fallback is always correct) and are -intentionally outside the consts merkle root. +The canonical (and only) hint channel, keyed by constant address and +sorted ascending. Hints never appear in `ConstantMeta`: the compiler +registers each definition's hints into `Env::anon_hints` +(`Env::register_hint`, an order-independent merge on alias +collisions), writers serialize that map here, and readers load it +back. Hints are performance-only advice (the `Regular(0)` fallback is +always correct) and are intentionally outside the consts merkle root. **Section 4: Names** (Address → NameComponent, topologically sorted) ``` @@ -1312,7 +1312,6 @@ Named { meta: ConstantMeta::Def { name: addr_of_name("double"), lvls: [], - hints: ReducibilityHints::Regular(1), all: [addr_of_name("double")], ctx: [], arena: ExprMeta { nodes: [