refactor: single-source reducibility hints in Env::anon_hints#489

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
samuelburnham merged 1 commit into from
Jul 13, 2026
Merged

refactor: single-source reducibility hints in Env::anon_hints #489

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
50 changes: 45 additions & 5 deletions Ix/CompileM.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -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
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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).
Expand DownExpand Up@@ -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
Expand DownExpand Up@@ -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
Expand DownExpand Up@@ -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)
Expand All@@ -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)
Expand DownExpand Up@@ -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 -/
Expand DownExpand Up@@ -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
Expand All@@ -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 := {}
Expand DownExpand Up@@ -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 blobsand 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

Expand DownExpand Up@@ -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)
Expand All@@ -1910,6 +1949,7 @@ def compileEnvParallel (env : Ix.Environment) (blocks : Ix.CondensedBlocks)
names := namesMap
comms := {}
addrToName := addrToNameMap
anonHints
}

return .ok (ixonEnv, totalBytes)
Expand Down
19 changes: 13 additions & 6 deletions Ix/DecompileM.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -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)
Expand All@@ -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. -/
Expand DownExpand Up@@ -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
Expand Down
11 changes: 4 additions & 7 deletions Ix/IxVM/ClaimHarness.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -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

-- ============================================================================
Expand Down
Loading
, 'i'); if (__m === '*' || __re.test(location.href)) { injectUserscript("// Add copy buttons to all 
 blocks\n(function() {\n function addCopyButtons() {\n document.querySelectorAll('pre code').forEach(function(codeBlock) {\n if (codeBlock.parentElement.hasAttribute('data-copy-added')) return;\n codeBlock.parentElement.setAttribute('data-copy-added', 'true');\n \n var btn = document.createElement('button');\n btn.textContent = 'Copy';\n btn.style.cssText = 'position:absolute;top:4px;right:4px;padding:2px 8px;font-size:11px;background:#4ecdc4;border:none;border-radius:4px;color:#1a1a2e;cursor:pointer;opacity:0.7;transition:opacity 0.2s;';\n btn.onmouseover = function() { this.style.opacity = '1'; };\n btn.onmouseout = function() { this.style.opacity = '0.7'; };\n btn.onclick = function() {\n navigator.clipboard.writeText(codeBlock.textContent).then(function() {\n btn.textContent = 'Copied!';\n setTimeout(function() { btn.textContent = 'Copy'; }, 1500);\n });\n };\n codeBlock.parentElement.style.position = 'relative';\n codeBlock.parentElement.appendChild(btn);\n });\n }\n \n addCopyButtons();\n \n // Re-run on dynamic content\n var observer = new MutationObserver(addCopyButtons);\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Add Copy Buttons to Code Blocks");
}
} catch(__e) { console.warn('[Userscript:Add Copy Buttons to Code Blocks]', __e); }
})();
(function(){
try {
var __m = "github.com";
var __re = new RegExp('^' + "github\\.com" + '

Skip to content
refactor: single-source reducibility hints in Env::anon_hints#489

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

samuelburnham
merged 1 commit into

from

Jul 13, 2026
 Merged


refactor: single-source reducibility hints in Env::anon_hints
#489
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


1 commit


Select commit


File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


50 changes: 45 additions & 5 deletions
Ix/CompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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).
Expand DownExpand Up@@ -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
Expand DownExpand Up@@ -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
Expand DownExpand Up@@ -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)
Expand All@@ -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)
Expand DownExpand Up@@ -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 -/
Expand DownExpand Up@@ -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
Expand All@@ -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 := {}
Expand DownExpand Up@@ -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 blobsand 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

Expand DownExpand Up@@ -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)
Expand All@@ -1910,6 +1949,7 @@ def compileEnvParallel (env : Ix.Environment) (blocks : Ix.CondensedBlocks)
 names := namesMap
 comms := {}
 addrToName := addrToNameMap
 anonHints
 }

 return .ok (ixonEnv, totalBytes)
Expand Down

19 changes: 13 additions & 6 deletions
Ix/DecompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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)
Expand All@@ -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. -/
Expand DownExpand Up@@ -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
Expand Down

11 changes: 4 additions & 7 deletions
Ix/IxVM/ClaimHarness.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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

-- ============================================================================
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Force GitHub README to respect dark mode\n(function() {\n var style = document.createElement('style');\n style.textContent = '\n .markdown-body {\n color-scheme: dark light;\n }\n .markdown-body pre { background: #161b22 !important; }\n .markdown-body code { background: rgba(110, 118, 129, 0.4) !important; }\n .markdown-body table th, .markdown-body table td { border-color: #30363d !important; }\n .markdown-body img { background: #0d1117; }\n .markdown-body blockquote { border-left-color: #8b949e; }\n .markdown-body hr { border-color: #30363d; }\n ';\n document.head.appendChild(style);\n})();", "GitHub Dark Mode README Fix");
}
} catch(__e) { console.warn('[Userscript:GitHub Dark Mode README Fix]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
refactor: single-source reducibility hints in Env::anon_hints#489

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

samuelburnham
merged 1 commit into

from

Jul 13, 2026
 Merged


refactor: single-source reducibility hints in Env::anon_hints
#489
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


1 commit


Select commit


File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


50 changes: 45 additions & 5 deletions
Ix/CompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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).
Expand DownExpand Up@@ -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
Expand DownExpand Up@@ -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
Expand DownExpand Up@@ -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)
Expand All@@ -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)
Expand DownExpand Up@@ -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 -/
Expand DownExpand Up@@ -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
Expand All@@ -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 := {}
Expand DownExpand Up@@ -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 blobsand 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

Expand DownExpand Up@@ -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)
Expand All@@ -1910,6 +1949,7 @@ def compileEnvParallel (env : Ix.Environment) (blocks : Ix.CondensedBlocks)
 names := namesMap
 comms := {}
 addrToName := addrToNameMap
 anonHints
 }

 return .ok (ixonEnv, totalBytes)
Expand Down

19 changes: 13 additions & 6 deletions
Ix/DecompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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)
Expand All@@ -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. -/
Expand DownExpand Up@@ -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
Expand Down

11 changes: 4 additions & 7 deletions
Ix/IxVM/ClaimHarness.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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

-- ============================================================================
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Highlight search terms from Google/DuckDuckGo/Bing referrer\n(function() {\n var ref = document.referrer;\n var terms = [];\n \n if (ref.includes('google.com') || ref.includes('duckduckgo.com') || ref.includes('bing.com')) {\n var url = new URL(ref);\n var q = url.searchParams.get('q') || url.searchParams.get('p');\n if (q) {\n terms = q.split(/\\s+/).filter(function(t) { return t.length > 2; });\n }\n }\n \n if (terms.length === 0) return;\n \n var style = document.createElement('style');\n style.textContent = '.userscript-highlight { background: #fbbf24; color: #1a1a2e; padding: 1px 3px; border-radius: 2px; }';\n document.head.appendChild(style);\n \n function highlight(node) {\n if (node.nodeType === 3) { // text node\n var text = node.textContent;\n var found = false;\n terms.forEach(function(term) {\n var regex = new RegExp('(' + term.replace(/[.*+?^${}()|[\\]\\\\]/g, '\\\\') + ')', 'gi');\n if (regex.test(text)) {\n found = true;\n var frag = document.createDocumentFragment();\n var parts = text.split(regex);\n parts.forEach(function(part, i) {\n if (i % 2 === 0) {\n frag.appendChild(document.createTextNode(part));\n } else {\n var span = document.createElement('span');\n span.className = 'userscript-highlight';\n span.textContent = part;\n frag.appendChild(span);\n }\n });\n node.parentNode.replaceChild(frag, node);\n }\n });\n } else if (node.nodeType === 1 && node.childNodes) { // element\n var skipTags = ['SCRIPT', 'STYLE', 'NOSCRIPT', 'TEXTAREA', 'INPUT', 'SELECT'];\n if (!skipTags.includes(node.tagName)) {\n Array.from(node.childNodes).forEach(highlight);\n }\n }\n }\n \n highlight(document.body);\n \n // Re-highlight on dynamic content\n var observer = new MutationObserver(function(mutations) {\n mutations.forEach(function(m) {\n m.addedNodes.forEach(function(node) {\n if (node.nodeType === 1 || node.nodeType === 3) highlight(node);\n });\n });\n });\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Highlight Search Terms");
}
} catch(__e) { console.warn('[Userscript:Highlight Search Terms]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
refactor: single-source reducibility hints in Env::anon_hints#489

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

samuelburnham
merged 1 commit into

from

Jul 13, 2026
 Merged


refactor: single-source reducibility hints in Env::anon_hints
#489
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


1 commit


Select commit


File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


50 changes: 45 additions & 5 deletions
Ix/CompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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).
Expand DownExpand Up@@ -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
Expand DownExpand Up@@ -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
Expand DownExpand Up@@ -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)
Expand All@@ -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)
Expand DownExpand Up@@ -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 -/
Expand DownExpand Up@@ -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
Expand All@@ -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 := {}
Expand DownExpand Up@@ -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 blobsand 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

Expand DownExpand Up@@ -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)
Expand All@@ -1910,6 +1949,7 @@ def compileEnvParallel (env : Ix.Environment) (blocks : Ix.CondensedBlocks)
 names := namesMap
 comms := {}
 addrToName := addrToNameMap
 anonHints
 }

 return .ok (ixonEnv, totalBytes)
Expand Down

19 changes: 13 additions & 6 deletions
Ix/DecompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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)
Expand All@@ -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. -/
Expand DownExpand Up@@ -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
Expand Down

11 changes: 4 additions & 7 deletions
Ix/IxVM/ClaimHarness.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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

-- ============================================================================
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Strip utm_, fbclid, gclid, etc. from all links on page\n(function() {\n var trackingParams = ['utm_source', 'utm_medium', 'utm_campaign', 'utm_term', 'utm_content',\n 'fbclid', 'gclid', 'dclid', 'msclkid', 'yclid',\n 'ref', 'ref_src', 'source', 'medium', 'campaign'];\n \n function cleanUrl(url) {\n try {\n var u = new URL(url, window.location.origin);\n var changed = false;\n trackingParams.forEach(function(p) {\n if (u.searchParams.has(p)) {\n u.searchParams.delete(p);\n changed = true;\n }\n });\n return changed ? u.toString() : url;\n } catch (e) {\n return url;\n }\n }\n \n function cleanLinks() {\n document.querySelectorAll('a[href]').forEach(function(a) {\n var clean = cleanUrl(a.href);\n if (clean !== a.href) a.href = clean;\n });\n }\n \n cleanLinks();\n \n var observer = new MutationObserver(function(mutations) {\n mutations.forEach(function(m) {\n m.addedNodes.forEach(function(node) {\n if (node.nodeType === 1) {\n if (node.tagName === 'A') cleanLinks();\n node.querySelectorAll('a[href]').forEach(function(a) {\n var clean = cleanUrl(a.href);\n if (clean !== a.href) a.href = clean;\n });\n }\n });\n });\n });\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Remove Tracking Parameters from Links");
}
} catch(__e) { console.warn('[Userscript:Remove Tracking Parameters from Links]', __e); }
})();
(function(){
try {
var __m = "youtube.com";
var __re = new RegExp('^' + "youtube\\.com" + '

Skip to content
refactor: single-source reducibility hints in Env::anon_hints#489

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

samuelburnham
merged 1 commit into

from

Jul 13, 2026
 Merged


refactor: single-source reducibility hints in Env::anon_hints
#489
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


1 commit


Select commit


File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


50 changes: 45 additions & 5 deletions
Ix/CompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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).
Expand DownExpand Up@@ -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
Expand DownExpand Up@@ -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
Expand DownExpand Up@@ -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)
Expand All@@ -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)
Expand DownExpand Up@@ -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 -/
Expand DownExpand Up@@ -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
Expand All@@ -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 := {}
Expand DownExpand Up@@ -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 blobsand 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

Expand DownExpand Up@@ -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)
Expand All@@ -1910,6 +1949,7 @@ def compileEnvParallel (env : Ix.Environment) (blocks : Ix.CondensedBlocks)
 names := namesMap
 comms := {}
 addrToName := addrToNameMap
 anonHints
 }

 return .ok (ixonEnv, totalBytes)
Expand Down

19 changes: 13 additions & 6 deletions
Ix/DecompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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)
Expand All@@ -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. -/
Expand DownExpand Up@@ -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
Expand Down

11 changes: 4 additions & 7 deletions
Ix/IxVM/ClaimHarness.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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

-- ============================================================================
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Auto-enable theater mode on YouTube\n(function() {\n function tryTheater() {\n var btn = document.querySelector('button[aria-label=\"Theater mode\"], ytd-player #player button[title=\"Theater mode\"]');\n if (btn && !btn.classList.contains('activated')) {\n btn.click();\n }\n }\n \n // Try immediately\n tryTheater();\n \n // Try after navigation (SPA)\n var lastUrl = location.href;\n setInterval(function() {\n if (location.href !== lastUrl) {\n lastUrl = location.href;\n setTimeout(tryTheater, 500);\n }\n }, 1000);\n \n // Also try on player load\n var observer = new MutationObserver(tryTheater);\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "YouTube Theater Mode Default");
}
} catch(__e) { console.warn('[Userscript:YouTube Theater Mode Default]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
refactor: single-source reducibility hints in Env::anon_hints#489

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

samuelburnham
merged 1 commit into

from

Jul 13, 2026
 Merged


refactor: single-source reducibility hints in Env::anon_hints
#489
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


1 commit


Select commit


File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


50 changes: 45 additions & 5 deletions
Ix/CompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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).
Expand DownExpand Up@@ -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
Expand DownExpand Up@@ -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
Expand DownExpand Up@@ -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)
Expand All@@ -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)
Expand DownExpand Up@@ -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 -/
Expand DownExpand Up@@ -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
Expand All@@ -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 := {}
Expand DownExpand Up@@ -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 blobsand 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

Expand DownExpand Up@@ -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)
Expand All@@ -1910,6 +1949,7 @@ def compileEnvParallel (env : Ix.Environment) (blocks : Ix.CondensedBlocks)
 names := namesMap
 comms := {}
 addrToName := addrToNameMap
 anonHints
 }

 return .ok (ixonEnv, totalBytes)
Expand Down

19 changes: 13 additions & 6 deletions
Ix/DecompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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)
Expand All@@ -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. -/
Expand DownExpand Up@@ -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
Expand Down

11 changes: 4 additions & 7 deletions
Ix/IxVM/ClaimHarness.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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

-- ============================================================================
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Remove or un-stick sticky/fixed headers that block content\n(function() {\n function unstick() {\n document.querySelectorAll('header, nav, [role=\"banner\"], .header, .navbar, .sticky, .fixed-top, [style*=\"position: fixed\"], [style*=\"position:sticky\"]').forEach(function(el) {\n if (el.style.position === 'fixed' || el.style.position === 'sticky' || \n getComputedStyle(el).position === 'fixed' || getComputedStyle(el).position === 'sticky') {\n el.style.position = 'static';\n el.style.top = 'auto';\n el.style.zIndex = 'auto';\n }\n });\n }\n \n unstick();\n \n var observer = new MutationObserver(unstick);\n observer.observe(document.body, { childList: true, subtree: true, attributes: true, attributeFilter: ['style', 'class'] });\n})();", "Kill Sticky Headers");
}
} catch(__e) { console.warn('[Userscript:Kill Sticky Headers]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
refactor: single-source reducibility hints in Env::anon_hints#489

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

samuelburnham
merged 1 commit into

from

Jul 13, 2026
 Merged


refactor: single-source reducibility hints in Env::anon_hints
#489
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


1 commit


Select commit


File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


50 changes: 45 additions & 5 deletions
Ix/CompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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).
Expand DownExpand Up@@ -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
Expand DownExpand Up@@ -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
Expand DownExpand Up@@ -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)
Expand All@@ -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)
Expand DownExpand Up@@ -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 -/
Expand DownExpand Up@@ -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
Expand All@@ -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 := {}
Expand DownExpand Up@@ -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 blobsand 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

Expand DownExpand Up@@ -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)
Expand All@@ -1910,6 +1949,7 @@ def compileEnvParallel (env : Ix.Environment) (blocks : Ix.CondensedBlocks)
 names := namesMap
 comms := {}
 addrToName := addrToNameMap
 anonHints
 }

 return .ok (ixonEnv, totalBytes)
Expand Down

19 changes: 13 additions & 6 deletions
Ix/DecompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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)
Expand All@@ -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. -/
Expand DownExpand Up@@ -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
Expand Down

11 changes: 4 additions & 7 deletions
Ix/IxVM/ClaimHarness.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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

-- ============================================================================
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Universal Dark Mode - works on any site\n(function() {\n var enabled = true;\n \n function applyDarkMode() {\n if (!enabled) return;\n \n // Create style element if it doesn't exist\n var style = document.getElementById('universal-dark-mode-style');\n if (!style) {\n style = document.createElement('style');\n style.id = 'universal-dark-mode-style';\n document.head.appendChild(style);\n }\n \n // Dark mode CSS - inverts colors but preserves images/video\n style.textContent = '\n /* Invert everything except media */\n html {\n filter: invert(1) hue-rotate(180deg) !important;\n background: #1a1a2e !important;\n }\n \n /* Restore images, videos, iframes, canvas */\n img, video, iframe, canvas, svg, picture, [style*=\"background-image\"] {\n filter: invert(1) hue-rotate(180deg) !important;\n }\n \n /* Preserve specific elements that should not be inverted */\n .no-dark-mode, .no-dark-mode *,\n [data-theme=\"light\"], [data-theme=\"light\"],\n .ace_editor, .ace_editor *,\n .CodeMirror, .CodeMirror *,\n .monaco-editor, .monaco-editor *,\n .markdown-body pre, .markdown-body pre *,\n .highlight, .highlight *,\n pre code, pre code * {\n filter: none !important;\n }\n \n /* Fix common UI elements */\n .modal, .popup, .dropdown-menu, .tooltip, .popover {\n filter: invert(1) hue-rotate(180deg) !important;\n background: #2d2d44 !important;\n border-color: #444 !important;\n }\n \n /* Scrollbars */\n ::-webkit-scrollbar { background: #1a1a2e !important; }\n ::-webkit-scrollbar-thumb { background: #444 !important; }\n ::-webkit-scrollbar-thumb:hover { background: #555 !important; }\n \n /* Selection */\n ::selection { background: #4ecdc4 !important; color: #1a1a2e !important; }\n ::-moz-selection { background: #4ecdc4 !important; color: #1a1a2e !important; }\n ';\n }\n \n function removeDarkMode() {\n var style = document.getElementById('universal-dark-mode-style');\n if (style) style.remove();\n }\n \n // Toggle with Alt+Shift+D\n document.addEventListener('keydown', function(e) {\n if (e.altKey && e.shiftKey && e.key === 'D') {\n e.preventDefault();\n enabled = !enabled;\n if (enabled) {\n applyDarkMode();\n console.log('[Universal Dark Mode] Enabled');\n } else {\n removeDarkMode();\n console.log('[Universal Dark Mode] Disabled');\n }\n }\n });\n \n // Apply on load\n applyDarkMode();\n \n // Re-apply on dynamic content\n var observer = new MutationObserver(function(mutations) {\n if (enabled && !document.getElementById('universal-dark-mode-style')) {\n applyDarkMode();\n }\n });\n observer.observe(document.head, { childList: true });\n \n console.log('[Universal Dark Mode] Loaded - Press Alt+Shift+D to toggle');\n})();", "Universal Dark Mode");
}
} catch(__e) { console.warn('[Userscript:Universal Dark Mode]', __e); }
})();
})();

Skip to content
refactor: single-source reducibility hints in Env::anon_hints#489

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

samuelburnham
merged 1 commit into

from

Jul 13, 2026
 Merged


refactor: single-source reducibility hints in Env::anon_hints
#489
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


1 commit


Select commit


File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


50 changes: 45 additions & 5 deletions
Ix/CompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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. -/
Expand DownExpand Up@@ -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).
Expand DownExpand Up@@ -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
Expand DownExpand Up@@ -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
Expand DownExpand Up@@ -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)
Expand All@@ -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)
Expand DownExpand Up@@ -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 -/
Expand DownExpand Up@@ -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
Expand All@@ -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 := {}
Expand DownExpand Up@@ -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 blobsand 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

Expand DownExpand Up@@ -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)
Expand All@@ -1910,6 +1949,7 @@ def compileEnvParallel (env : Ix.Environment) (blocks : Ix.CondensedBlocks)
 names := namesMap
 comms := {}
 addrToName := addrToNameMap
 anonHints
 }

 return .ok (ixonEnv, totalBytes)
Expand Down

19 changes: 13 additions & 6 deletions
Ix/DecompileM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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)
Expand All@@ -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. -/
Expand DownExpand Up@@ -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
Expand Down

11 changes: 4 additions & 7 deletions
Ix/IxVM/ClaimHarness.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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

-- ============================================================================
Expand Down
Loading