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: [