Ixon: lazy, zero-copy anon env load for the Aiur check path (#445)

`ix check --ixe` deserialized the whole env eagerly: the Rust FFI
materialized every constant and the Lean side built an object graph for
all of them up front, even to check one lemma. On mathlib.ixe (2.97 GB)
that was ~104 GB peak RSS / ~159 s just to load.

Make the Lean `Ixon.Env` constants lazy and load them without copying:

- `LazyConstant` is now an offset window `(buf, off, len)` into a shared
  backing buffer (+ optional materialized cache for the build path),
  parsed on demand. Only the checked closure is ever materialized.
- New `rs_de_env_lazy` FFI: `Env::parse_lazy_index` walks the env once
  (reusing the existing parser, so every metadata variant incl.
  `CallSite` is handled) and returns per-const `(addr, offset, len)`
  windows into the buffer Lean passed in, plus `name -> addr` and
  per-`Defn` reducibility hints. No constant body is parsed or copied at
  load time. `deEnvAnon` reconstructs an `Env` of byte-window
  `LazyConstant`s over that same buffer.
- This is anon-aligned with the circuit: binder metadata (the
  `ExprMetaArena`) is parsed-and-discarded, since the typecheck circuit
  only consumes anonymous constants, blobs, and the per-`Defn` hint. The
  CLI's `name -> addr` map is kept so targets can still be named.
- Pure-Lean `getEnv`/`deEnv`/`rsDeEnv` keep their full-metadata behavior
  for round-trip and the non-check loaders; only the check path
  (`CheckCmd`) switches to `deEnvAnon`.

Consumers updated for the lazy const type: closure walk, IOBuffer
ingress (ships `rawBytes` windows directly), shard partitioning,
decompile, and the compile/commit env builders.

Measured on mathlib.ixe (same file, same target): 104.5 GB -> 4.5 GB
peak RSS, 159 s -> 13.5 s, and the lazy run additionally typechecks the
target rather than only resolving its address. Nothing in circuit
changes: same closure bytes, same in-circuit blake3 verification, same
proof.

Author: samuelburnham

Ix/Cli/CheckCmd.lean

@@ -183,7 +183,10 @@ def forEachClaim
   match ixePath with
   | some path =>
     let bytes ← IO.FS.readBinFile path
-    let ixonEnv ← match Ixon.rsDeEnv bytes with
+    -- Anon load: lazy zero-copy constants, binder metadata dropped. The Aiur
+    -- check circuit consumes only anonymous constants, blobs, and per-Defn
+    -- reducibility hints — mirrors the Rust kernel's `get_anon_mmap`.
+    let ixonEnv ← match Ixon.deEnvAnon bytes with
       | .error e =>
         IO.eprintln s!"Failed to deserialize {path}: {e}"; return 1
       | .ok env => pure env
@@ -331,7 +334,8 @@ private def blockAddrOf (addr : Address) (c : Ixon.Constant) : Address :=
 def ownedConstsForBlocks (ixonEnv : Ixon.Env) (blocks : Array Address) : Array Address := Id.run do
   let blockSet : Std.HashSet Address := blocks.foldl (·.insert ·) {}
   let mut o : Array Address := #[]
-  for (addr, c) in ixonEnv.consts do
+  for (addr, lc) in ixonEnv.consts do
+    let some c := lc.get? | continue
     if blockSet.contains (blockAddrOf addr c) then o := o.push addr
   return o
 
@@ -348,7 +352,7 @@ def loadEnvAndShards (manifestPath ixePath : String) :
     IO (Except String (Ixon.Env × Array (Array Address))) := do
   match parseIxesAllShards (← IO.FS.readBinFile manifestPath) with
   | .error e => return .error s!"manifest parse failed: {e}"
-  | .ok shards => match Ixon.rsDeEnv (← IO.FS.readBinFile ixePath) with
+  | .ok shards => match Ixon.deEnvAnon (← IO.FS.readBinFile ixePath) with
     | .error e => return .error s!"deserialize {ixePath} failed: {e}"
     | .ok env => return .ok (env, shards)
 
@@ -405,7 +409,8 @@ def shardsCover (ixonEnv : Ixon.Env) (shards : Array (Array Address)) : IO Bool
   -- assign every const to a shard via its block; count + detect unowned.
   let mut counts : Array Nat := Array.replicate shards.size 0
   let mut unowned : Nat := 0
-  for (addr, c) in ixonEnv.consts do
+  for (addr, lc) in ixonEnv.consts do
+    let some c := lc.get? | continue
     match blockToShard.get? (blockAddrOf addr c) with
     | some k => counts := counts.modify k (· + 1)  -- total: no-op if out of range
     | none => unowned := unowned + 1

Ix/Commit.lean

@@ -28,7 +28,8 @@ open Ixon (PutM runPut putConstant putExpr Comm)
 def mkCompileEnv (phases : Ix.CompileM.CompilePhases) : Ix.CompileM.CompileEnv :=
   { env := phases.rawEnv
   , nameToNamed := phases.compileEnv.named
-  , constants := phases.compileEnv.consts
+  , constants := phases.compileEnv.consts.fold (init := {})
+      fun m a lc => m.insert a (lc.get?.getD default)
   , blobs := phases.compileEnv.blobs
   , totalBytes := 0 }
 

Ix/CompileM.lean

@@ -1615,7 +1615,8 @@ def compileEnv (env : Ix.Environment) (blocks : Ix.CondensedBlocks) (dbg : Bool
   let allBlobs := nameBlobs.fold (fun m k v => m.insert k v) compileEnv.blobs
 
   let ixonEnv : Ixon.Env := {
-    consts := compileEnv.constants
+    consts := compileEnv.constants.fold (init := {})
+      fun m a c => m.insert a (Ixon.LazyConstant.ofConstant c)
     named := compileEnv.nameToNamed
     blobs := allBlobs
     names := namesMap
@@ -1908,7 +1909,8 @@ def compileEnvParallel (env : Ix.Environment) (blocks : Ix.CondensedBlocks)
     IO.println s!"  [Lean Compile] Blobs: {blockBlobCount} from blocks, {nameBlobCount} from names, {overlapCount} overlap, {finalBlobCount} final"
 
   let ixonEnv : Ixon.Env := {
-    consts := constants
+    consts := constants.fold (init := {})
+      fun m a c => m.insert a (Ixon.LazyConstant.ofConstant c)
     named := nameToNamed
     blobs := allBlobs
     names := namesMap

Ix/DecompileM.lean

@@ -712,7 +712,7 @@ def decompileProjection (cnst : Constant) (cMeta : ConstantMeta)
 def decompileOne (env : DecompileEnv) (ixonEnv : Ixon.Env)
     (_ixName : Ix.Name) (named : Ixon.Named)
     : Except String (Array (Ix.Name × Ix.ConstantInfo)) :=
-  match ixonEnv.consts.get? named.addr with
+  match ixonEnv.getConst? named.addr with
   | none => .ok #[]
   | some cnst =>
     let m : DecompileM (Array (Ix.Name × Ix.ConstantInfo)) :=
@@ -730,17 +730,17 @@ def decompileOne (env : DecompileEnv) (ixonEnv : Ixon.Env)
         let info ← decompileRecursor rec cnst named.constMeta
         pure #[(info.getCnst.name, info)]
       | .dPrj proj =>
-        match ixonEnv.consts.get? proj.block with
+        match ixonEnv.getConst? proj.block with
         | some { info := .muts mutuals, sharing, refs, univs } =>
           decompileProjection cnst named.constMeta mutuals sharing refs univs
         | _ => pure #[]
       | .iPrj proj =>
-        match ixonEnv.consts.get? proj.block with
+        match ixonEnv.getConst? proj.block with
         | some { info := .muts mutuals, sharing, refs, univs } =>
           decompileProjection cnst named.constMeta mutuals sharing refs univs
         | _ => pure #[]
       | .rPrj proj =>
-        match ixonEnv.consts.get? proj.block with
+        match ixonEnv.getConst? proj.block with
         | some { info := .muts mutuals, sharing, refs, univs } =>
           decompileProjection cnst named.constMeta mutuals sharing refs univs
         | _ => pure #[]

Ix/IxVM/ClaimHarness.lean

@@ -97,7 +97,7 @@ partial def closureFrom (env : Ixon.Env) (target : Address) : Std.HashSet Addres
     worklist := worklist.pop
     if visited.contains addr then continue
     visited := visited.insert addr
-    let some c := env.consts.get? addr | continue
+    let some c := env.getConst? addr | continue
     for r in c.refs do worklist := worklist.push r
     match c.info with
     | .iPrj p | .cPrj p => worklist := worklist.push p.block
@@ -111,8 +111,9 @@ partial def closureFrom (env : Ixon.Env) (target : Address) : Std.HashSet Addres
     one entry per const, keyed by its index. Returns the buffer and the
     count `n` (which the Aiur entrypoint receives as input). -/
 def buildSerdeIOBuffer (ixonEnv : Ixon.Env) : Aiur.IOBuffer × Nat :=
-  ixonEnv.consts.valuesIter.fold (init := (default, 0)) fun (ioBuffer, i) c =>
-    let (_, bytes) := Ixon.Serialize.put c |>.run default
+  ixonEnv.consts.valuesIter.fold (init := (default, 0)) fun (ioBuffer, i) lc =>
+    -- The lazy entry already holds the serialized bytes; no re-serialization.
+    let bytes := lc.rawBytes
     (ioBuffer.extend 0 #[.ofNat i] (bytes.data.map .ofUInt8), i + 1)
 
 /-- Encode a `Lean.ReducibilityHints` as a single `G` per the convention
@@ -139,9 +140,11 @@ private def hintToG : Lean.ReducibilityHints → Aiur.G
 def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool)
     (ioBuffer : Aiur.IOBuffer) : Aiur.IOBuffer := Id.run do
   let mut ioBuffer := ioBuffer
-  for (addr, c) in ixonEnv.consts do
+  for (addr, lc) in ixonEnv.consts do
     if !keep addr then continue
-    let (_, bytes) := Ixon.Serialize.put c |>.run default
+    -- The kernel re-hashes these bytes against the key, so feed the exact
+    -- serialized form the lazy entry holds — no materialization needed.
+    let bytes := lc.rawBytes
     let key : Array Aiur.G := addr.hash.data.map .ofUInt8
     ioBuffer := ioBuffer.extend 0 key (bytes.data.map .ofUInt8)
   for (addr, rawBytes) in ixonEnv.blobs do