Add DAG-based kernel typechecker

Ix/Address.lean

@@ -14,6 +14,7 @@ structure Address where
 /-- Compute the Blake3 hash of a `ByteArray`, returning an `Address`. -/
 def Address.blake3 (x: ByteArray) : Address := ⟨(Blake3.hash x).val⟩
 
+
 /-- Convert a nibble (0--15) to its lowercase hexadecimal character. -/
 def hexOfNat : Nat -> Option Char
 | 0 => .some '0'

Ix/Cli/CheckCmd.lean

@@ -0,0 +1,122 @@
+import Cli
+import Ix.Common
+import Ix.Kernel
+import Ix.Meta
+import Ix.CompileM
+import Lean
+
+open System (FilePath)
+
+/-- If the project depends on Mathlib, download the Mathlib cache. -/
+private def fetchMathlibCache (cwd : Option FilePath) : IO Unit := do
+  let root := cwd.getD "."
+  let manifest := root / "lake-manifest.json"
+  let contents ← IO.FS.readFile manifest
+  if contents.containsSubstr "leanprover-community/mathlib4" then
+    let mathlibBuild := root / ".lake" / "packages" / "mathlib" / ".lake" / "build"
+    if ← mathlibBuild.pathExists then
+      println! "Mathlib cache already present, skipping fetch."
+      return
+    println! "Detected Mathlib dependency. Fetching Mathlib cache..."
+    let child ← IO.Process.spawn {
+      cmd := "lake"
+      args := #["exe", "cache", "get"]
+      cwd := cwd
+      stdout := .inherit
+      stderr := .inherit
+    }
+    let exitCode ← child.wait
+    if exitCode != 0 then
+      throw $ IO.userError "lake exe cache get failed"
+
+/-- Build the Lean module at the given file path using Lake. -/
+private def buildFile (path : FilePath) : IO Unit := do
+  let path ← IO.FS.realPath path
+  let some moduleName := path.fileStem
+    | throw $ IO.userError s!"cannot determine module name from {path}"
+  fetchMathlibCache path.parent
+  let child ← IO.Process.spawn {
+    cmd := "lake"
+    args := #["build", moduleName]
+    cwd := path.parent
+    stdout := .inherit
+    stderr := .inherit
+  }
+  let exitCode ← child.wait
+  if exitCode != 0 then
+    throw $ IO.userError "lake build failed"
+
+/-- Run the Lean NbE kernel checker. -/
+private def runLeanCheck (leanEnv : Lean.Environment) : IO UInt32 := do
+  println! "Compiling to Ixon..."
+  let compileStart ← IO.monoMsNow
+  let ixonEnv ← Ix.CompileM.rsCompileEnv leanEnv
+  let compileElapsed := (← IO.monoMsNow) - compileStart
+  let numConsts := ixonEnv.consts.size
+  println! "Compiled {numConsts} constants in {compileElapsed.formatMs}"
+
+  println! "Converting Ixon → Kernel..."
+  let convertStart ← IO.monoMsNow
+  match Ix.Kernel.Convert.convertEnv .meta ixonEnv with
+  | .error e =>
+    println! "Conversion error: {e}"
+    return 1
+  | .ok (kenv, prims, quotInit) =>
+    let convertElapsed := (← IO.monoMsNow) - convertStart
+    println! "Converted {kenv.size} constants in {convertElapsed.formatMs}"
+
+    println! "Typechecking..."
+    let checkStart ← IO.monoMsNow
+    match Ix.Kernel.typecheckAll kenv prims quotInit with
+    | .error e =>
+      let elapsed := (← IO.monoMsNow) - checkStart
+      println! "Kernel check failed in {elapsed.formatMs}: {e}"
+      return 1
+    | .ok () =>
+      let elapsed := (← IO.monoMsNow) - checkStart
+      println! "Checked {kenv.size} constants in {elapsed.formatMs}"
+      return 0
+
+/-- Run the Rust kernel checker. -/
+private def runRustCheck (leanEnv : Lean.Environment) : IO UInt32 := do
+  let totalConsts := leanEnv.constants.toList.length
+  println! "Total constants: {totalConsts}"
+
+  let start ← IO.monoMsNow
+  let errors ← Ix.Kernel.rsCheckEnv leanEnv
+  let elapsed := (← IO.monoMsNow) - start
+
+  if errors.isEmpty then
+    println! "Checked {totalConsts} constants in {elapsed.formatMs}"
+    return 0
+  else
+    println! "Kernel check failed with {errors.size} error(s) in {elapsed.formatMs}:"
+    for (name, err) in errors[:min 50 errors.size] do
+      println! "  {repr name}: {repr err}"
+    return 1
+
+def runCheckCmd (p : Cli.Parsed) : IO UInt32 := do
+  let some path := p.flag? "path"
+    | p.printError "error: must specify --path"
+      return 1
+  let pathStr := path.as! String
+  let useLean := p.hasFlag "lean"
+
+  buildFile pathStr
+  let leanEnv ← getFileEnv pathStr
+
+  if useLean then
+    println! "Running Lean NbE kernel checker on {pathStr}"
+    runLeanCheck leanEnv
+  else
+    println! "Running Rust kernel checker on {pathStr}"
+    runRustCheck leanEnv
+
+def checkCmd : Cli.Cmd := `[Cli|
+  check VIA runCheckCmd;
+  "Type-check Lean file with kernel"
+
+  FLAGS:
+    path : String; "Path to file to check"
+    lean; "Use Lean NbE kernel instead of Rust kernel"
+]

Ix/CompileM.lean

@@ -1604,11 +1604,10 @@ def compileEnv (env : Ix.Environment) (blocks : Ix.CondensedBlocks) (dbg : Bool
 
   -- Build reverse index and names map, storing name string components as blobs
   -- Seed with blockNames collected during compilation (binder names, level params, etc.)
-  let (addrToNameMap, namesMap, nameBlobs) :=
-    compileEnv.nameToNamed.fold (init := ({}, blockNames, {})) fun (addrMap, namesMap, blobs) name named =>
-      let addrMap := addrMap.insert named.addr name
+  let (namesMap, nameBlobs) :=
+    compileEnv.nameToNamed.fold (init := (blockNames, {})) fun (namesMap, blobs) name _named =>
       let (namesMap, blobs) := Ixon.RawEnv.addNameComponentsWithBlobs namesMap blobs name
-      (addrMap, namesMap, blobs)
+      (namesMap, blobs)
 
   -- Merge name string blobs into the main blobs map
   let allBlobs := nameBlobs.fold (fun m k v => m.insert k v) compileEnv.blobs
@@ -1619,7 +1618,6 @@ def compileEnv (env : Ix.Environment) (blocks : Ix.CondensedBlocks) (dbg : Bool
     blobs := allBlobs
     names := namesMap
     comms := {}
-    addrToName := addrToNameMap
   }
 
   return .ok (ixonEnv, compileEnv.totalBytes)
@@ -1890,11 +1888,10 @@ def compileEnvParallel (env : Ix.Environment) (blocks : Ix.CondensedBlocks)
 
   -- Build reverse index and names map, storing name string components as blobs
   -- Seed with blockNames collected during compilation (binder names, level params, etc.)
-  let (addrToNameMap, namesMap, nameBlobs) :=
-    nameToNamed.fold (init := ({}, blockNames, {})) fun (addrMap, namesMap, nameBlobs) name named =>
-      let addrMap := addrMap.insert named.addr name
+  let (namesMap, nameBlobs) :=
+    nameToNamed.fold (init := (blockNames, {})) fun (namesMap, nameBlobs) name _named =>
       let (namesMap, nameBlobs) := Ixon.RawEnv.addNameComponentsWithBlobs namesMap nameBlobs name
-      (addrMap, namesMap, nameBlobs)
+      (namesMap, nameBlobs)
 
   -- Merge name string blobs into the main blobs map
   let blockBlobCount := blobs.size
@@ -1912,7 +1909,6 @@ def compileEnvParallel (env : Ix.Environment) (blocks : Ix.CondensedBlocks)
     blobs := allBlobs
     names := namesMap
     comms := {}
-    addrToName := addrToNameMap
   }
 
   return .ok (ixonEnv, totalBytes)

Ix/DecompileM.lean

@@ -117,12 +117,6 @@ def lookupNameAddrOrAnon (addr : Address) : DecompileM Ix.Name := do
   | some n => pure n
   | none => pure Ix.Name.mkAnon
 
-/-- Resolve constant Address → Ix.Name via addrToName. -/
-def lookupConstName (addr : Address) : DecompileM Ix.Name := do
-  match (← getEnv).ixonEnv.addrToName.get? addr with
-  | some n => pure n
-  | none => throw (.missingAddress addr)
-
 def lookupBlob (addr : Address) : DecompileM ByteArray := do
   match (← getEnv).ixonEnv.blobs.get? addr with
   | some blob => pure blob
@@ -390,18 +384,14 @@ partial def decompileExpr (e : Ixon.Expr) (arenaIdx : UInt64) : DecompileM Ix.Ex
     pure (applyMdata (Ix.Expr.mkLit (.strVal s)) mdataLayers)
 
   -- Ref with arena metadata
-  | .ref nameAddr, .ref refIdx univIndices => do
-    let name ← match (← getEnv).ixonEnv.names.get? nameAddr with
-      | some n => pure n
-      | none => getRef refIdx >>= lookupConstName
+  | .ref nameAddr, .ref _refIdx univIndices => do
+    let name ← lookupNameAddr nameAddr
     let lvls ← decompileUnivIndices univIndices
     pure (applyMdata (Ix.Expr.mkConst name lvls) mdataLayers)
 
   -- Ref without arena metadata
-  | _, .ref refIdx univIndices => do
-    let name ← getRef refIdx >>= lookupConstName
-    let lvls ← decompileUnivIndices univIndices
-    pure (applyMdata (Ix.Expr.mkConst name lvls) mdataLayers)
+  | _, .ref _refIdx _univIndices => do
+    throw (.badConstantFormat "ref without arena metadata")
 
   -- Rec with arena metadata
   | .ref nameAddr, .recur recIdx univIndices => do
@@ -472,10 +462,8 @@ partial def decompileExpr (e : Ixon.Expr) (arenaIdx : UInt64) : DecompileM Ix.Ex
     let valExpr ← decompileExpr val child
     pure (applyMdata (Ix.Expr.mkProj typeName fieldIdx.toNat valExpr) mdataLayers)
 
-  | _, .prj typeRefIdx fieldIdx val => do
-    let typeName ← getRef typeRefIdx >>= lookupConstName
-    let valExpr ← decompileExpr val UInt64.MAX
-    pure (applyMdata (Ix.Expr.mkProj typeName fieldIdx.toNat valExpr) mdataLayers)
+  | _, .prj _typeRefIdx _fieldIdx _val => do
+    throw (.badConstantFormat "prj without arena metadata")
 
   | _, .share _ => throw (.badConstantFormat "unexpected Share in decompileExpr")
 

Ix/Ixon.lean

@@ -1380,12 +1380,10 @@ structure Env where
   named : Std.HashMap Ix.Name Named := {}
   /-- Raw data blobs: Address → bytes -/
   blobs : Std.HashMap Address ByteArray := {}
-  /-- Hash-consed name components: Address → Ix.Name -/
-  names : Std.HashMap Address Ix.Name := {}
   /-- Cryptographic commitments: Address → Comm -/
   comms : Std.HashMap Address Comm := {}
-  /-- Reverse index: constant Address → Ix.Name -/
-  addrToName : Std.HashMap Address Ix.Name := {}
+  /-- Hash-consed name components: Address → Ix.Name -/
+  names : Std.HashMap Address Ix.Name := {}
   deriving Inhabited
 
 namespace Env
@@ -1401,8 +1399,7 @@ def getConst? (env : Env) (addr : Address) : Option Constant :=
 /-- Register a name with full Named metadata. -/
 def registerName (env : Env) (name : Ix.Name) (named : Named) : Env :=
   { env with
-    named := env.named.insert name named
-    addrToName := env.addrToName.insert named.addr name }
+    named := env.named.insert name named }
 
 /-- Register a name with just an address (empty metadata). -/
 def registerNameAddr (env : Env) (name : Ix.Name) (addr : Address) : Env :=
@@ -1416,10 +1413,6 @@ def getAddr? (env : Env) (name : Ix.Name) : Option Address :=
 def getNamed? (env : Env) (name : Ix.Name) : Option Named :=
   env.named.get? name
 
-/-- Look up an address's name. -/
-def getName? (env : Env) (addr : Address) : Option Ix.Name :=
-  env.addrToName.get? addr
-
 /-- Store a blob and return its content address. -/
 def storeBlob (env : Env) (bytes : ByteArray) : Env × Address :=
   let addr := Address.blake3 bytes
@@ -1742,8 +1735,7 @@ def getEnv : GetM Env := do
     | some name =>
       let namedEntry : Named := ⟨constAddr, constMeta⟩
       env := { env with
-        named := env.named.insert name namedEntry
-        addrToName := env.addrToName.insert constAddr name }
+        named := env.named.insert name namedEntry }
     | none =>
       throw s!"getEnv: named entry references unknown name address {reprStr (toString nameAddr)}"
 

Ix/Kernel.lean

@@ -0,0 +1,44 @@
+import Lean
+import Ix.Environment
+import Ix.Kernel.Types
+import Ix.Kernel.Datatypes
+import Ix.Kernel.Level
+import Ix.Kernel.TypecheckM
+import Ix.Kernel.Eval
+import Ix.Kernel.Equal
+import Ix.Kernel.Infer
+import Ix.Kernel.Convert
+
+namespace Ix.Kernel
+
+/-- Type-checking errors from the Rust kernel, mirroring `TcError` in Rust. -/
+inductive CheckError where
+  | typeExpected (expr : Ix.Expr) (inferred : Ix.Expr)
+  | functionExpected (expr : Ix.Expr) (inferred : Ix.Expr)
+  | typeMismatch (expected : Ix.Expr) (found : Ix.Expr) (expr : Ix.Expr)
+  | defEqFailure (lhs : Ix.Expr) (rhs : Ix.Expr)
+  | unknownConst (name : Ix.Name)
+  | duplicateUniverse (name : Ix.Name)
+  | freeBoundVariable (idx : UInt64)
+  | kernelException (msg : String)
+  deriving Repr
+
+/-- FFI: Run Rust kernel type-checker over all declarations in a Lean environment. -/
+@[extern "rs_check_env"]
+opaque rsCheckEnvFFI : @& List (Lean.Name × Lean.ConstantInfo) → IO (Array (Ix.Name × CheckError))
+
+/-- Check all declarations in a Lean environment using the Rust kernel.
+    Returns an array of (name, error) pairs for any declarations that fail. -/
+def rsCheckEnv (leanEnv : Lean.Environment) : IO (Array (Ix.Name × CheckError)) :=
+  rsCheckEnvFFI leanEnv.constants.toList
+
+/-- FFI: Type-check a single constant by dotted name string. -/
+@[extern "rs_check_const"]
+opaque rsCheckConstFFI : @& List (Lean.Name × Lean.ConstantInfo) → @& String → IO (Option CheckError)
+
+/-- Check a single constant by name using the Rust kernel.
+    Returns `none` on success, `some err` on failure. -/
+def rsCheckConst (leanEnv : Lean.Environment) (name : String) : IO (Option CheckError) :=
+  rsCheckConstFFI leanEnv.constants.toList name
+
+end Ix.Kernel