IxVM kernel: RBTreeMap-backed ingress + aligned ix prove/ix check CLI

Check.lean

@@ -0,0 +1,33 @@
+/-
+  `lake exe check`: thin Cli shim around `Ix.Cli.CheckCmd.runCheckCmd`.
+
+  The Aiur kernel typechecking logic lives in `Ix/Cli/CheckCmd.lean`
+  and is the implementation behind `ix check`. This binary exists so
+  that day-to-day Lean iteration can rebuild a small exe (`lake exe
+  check`) instead of the full `ix` binary while still hitting the
+  identical code path.
+
+  All flags + behavior match `ix check` 1:1. See its help for details.
+-/
+import Cli
+import Ix.Cli.CheckCmd
+
+open Cli
+
+def kernelCmd : Cli.Cmd := `[Cli|
+  kernel VIA Ix.Cli.CheckCmd.runCheckCmd;
+  "Typecheck Lean / `.ixe` constants through the IxVM Aiur kernel"
+
+  FLAGS:
+    interp;                 "Use the Aiur interpreter (richer per-execution error diagnostics) instead of the compiled bytecode runner."
+    "keep-going";           "Continue past failures and report them at the end instead of halting on the first."
+    "ixe"       : String;   "Path to a serialized `.ixe` env. When set, the binary reads the env from disk instead of using the compiled-in Lean env."
+    "claim"     : String;   "32-byte hex address of a persisted `Ix.Claim` in `~/.ix/store/`. When set, runs the `verify_claim` entrypoint once over the claim's witness against the `--ixe` env (single execution, skips per-const iteration)."
+    "stats-out" : String;   "Redirect the per-circuit statistics dump to this file (only used when exactly one constant is targeted)."
+
+  ARGS:
+    ...names : String; "Fully-qualified Lean.Name(s) to check. With none, iterate every named constant in the env (sorted)."
+]
+
+def main (args : List String) : IO UInt32 :=
+  kernelCmd.validate args

Ix/Claim.lean

@@ -554,4 +554,89 @@ end Claim
 
 end Ix
 
+-- ============================================================================
+-- Ixon.Proof — wraps a Claim with its opaque ZK proof bytes.
+-- Mirrors `src/ix/ixon/proof.rs:173`. Lives under flag 0xF (vs claims
+-- under 0xE) so the first serialized byte alone disambiguates kind.
+-- ============================================================================
+
+namespace Ixon
+
+structure Proof where
+  claim : Ix.Claim
+  proof : ByteArray
+  deriving Inhabited
+
+namespace Proof
+
+/-- The proof-variant size matching this claim, used as the Tag4 size
+    field under `FLAG_PROOF = 0xF`. -/
+def variantOf : Ix.Claim → UInt64
+  | .eval _ _ _     => Ix.Claim.VARIANT_EVAL_PROOF
+  | .check _ _      => Ix.Claim.VARIANT_CHECK_PROOF
+  | .checkEnv _ _   => Ix.Claim.VARIANT_CHECK_ENV_PROOF
+  | .reveal _ _     => Ix.Claim.VARIANT_REVEAL_PROOF
+  | .contains _ _   => Ix.Claim.VARIANT_CONTAINS_PROOF
+
+def put (p : Proof) : PutM Unit := do
+  putTag4 ⟨Ix.Claim.FLAG_PROOF, variantOf p.claim⟩
+  match p.claim with
+  | .eval input output asm => do
+    Serialize.put input
+    Serialize.put output
+    Ix.Claim.putOptAddr asm
+  | .check addr asm => do
+    Serialize.put addr
+    Ix.Claim.putOptAddr asm
+  | .checkEnv root asm => do
+    Serialize.put root
+    Ix.Claim.putOptAddr asm
+  | .reveal comm info => do
+    Serialize.put comm
+    Ix.RevealConstantInfo.put info
+  | .contains tree target => do
+    Serialize.put tree
+    Serialize.put target
+  putTag0 ⟨p.proof.size.toUInt64⟩
+  putBytes p.proof
+
+def get : GetM Proof := do
+  let tag ← getTag4
+  if tag.flag != Ix.Claim.FLAG_PROOF then
+    throw s!"Ixon.Proof.get: expected flag 0xF, got {tag.flag}"
+  let claim : Ix.Claim ←
+    if tag.size == Ix.Claim.VARIANT_EVAL_PROOF then do
+      let input ← Serialize.get
+      let output ← Serialize.get
+      let asm ← Ix.Claim.getOptAddr
+      pure (.eval input output asm)
+    else if tag.size == Ix.Claim.VARIANT_CHECK_PROOF then do
+      let addr ← Serialize.get
+      let asm ← Ix.Claim.getOptAddr
+      pure (.check addr asm)
+    else if tag.size == Ix.Claim.VARIANT_CHECK_ENV_PROOF then do
+      let root ← Serialize.get
+      let asm ← Ix.Claim.getOptAddr
+      pure (.checkEnv root asm)
+    else if tag.size == Ix.Claim.VARIANT_REVEAL_PROOF then do
+      let comm ← Serialize.get
+      let info ← Ix.RevealConstantInfo.get
+      pure (.reveal comm info)
+    else if tag.size == Ix.Claim.VARIANT_CONTAINS_PROOF then do
+      let tree ← Serialize.get
+      let target ← Serialize.get
+      pure (.contains tree target)
+    else
+      throw s!"Ixon.Proof.get: invalid proof variant {tag.size}"
+  let lenTag ← getTag0
+  let bytes ← getBytes lenTag.size.toNat
+  pure { claim, proof := bytes }
+
+def ser (p : Proof) : ByteArray := runPut (put p)
+def de (bytes : ByteArray) : Except String Proof := runGet get bytes
+
+end Proof
+
+end Ixon
+
 end

Ix/Cli/AddrOfCmd.lean

@@ -0,0 +1,76 @@
+/-
+  `ix addr-of <Lean.Name> [--ixe <path>]`: resolve a Lean.Name to its
+  32-byte content address. Without `--ixe`, the lookup compiles the
+  name's transitive closure from the compiled-in Lean env (via
+  `IxVM.ClaimHarness.loadIxonEnv` → `lookupAddr`). With `--ixe`, the
+  lookup reads the env from disk and dispatches `Ixon.Env.getAddr?`.
+
+  Prints the resulting address hex on stdout (one line, no prefix), so
+  the output can be piped into `ix claim check $(ix addr-of …)` etc.
+-/
+module
+public import Cli
+public import Std.Internal.UV.System
+public import Ix.Address
+public import Ix.Common
+public import Ix.Environment
+public import Ix.IxVM.ClaimHarness
+public import Ix.Ixon
+public import Ix.Meta
+
+public section
+
+namespace Ix.Cli.AddrOfCmd
+
+private def parseName (arg : String) : Lean.Name :=
+  arg.splitOn "." |>.foldl (init := .anonymous)
+    fun acc s => match s.toNat? with
+      | some n => Lean.Name.mkNum acc n
+      | none   => Lean.Name.mkStr acc s
+
+def runAddrOfCmd (p : Cli.Parsed) : IO UInt32 := do
+  -- Suppress Rust-side `[compile_env]` scheduler noise; the only
+  -- signal this command emits is the address on stdout.
+  Std.Internal.UV.System.osSetenv "IX_QUIET" "1"
+  let some nameArg := p.positionalArg? "name"
+    | p.printError "error: must specify <Lean.Name>"; return 1
+  let name := parseName (nameArg.as! String)
+  let ixePath : Option String :=
+    (p.flag? "ixe").map (·.as! String)
+  match ixePath with
+  | some path =>
+    let bytes ← IO.FS.readBinFile path
+    let ixonEnv ← match Ixon.rsDeEnv bytes with
+      | .error e =>
+        IO.eprintln s!"error: failed to deserialize {path}: {e}"; return 1
+      | .ok env => pure env
+    match ixonEnv.getAddr? (Ix.Name.fromLeanName name) with
+    | none =>
+      IO.eprintln s!"error: {name} not found in {path}"; return 1
+    | some addr =>
+      IO.println (toString addr); return 0
+  | none =>
+    let env ← get_env!
+    if !env.constants.contains name then
+      IO.eprintln s!"error: {name} not found in compiled-in Lean env"
+      return 1
+    let ixonEnv ← IxVM.ClaimHarness.loadIxonEnv name env
+    let addr ← IxVM.ClaimHarness.lookupAddr ixonEnv name
+    IO.println (toString addr)
+    return 0
+
+end Ix.Cli.AddrOfCmd
+
+open Ix.Cli.AddrOfCmd in
+def addrOfCmd : Cli.Cmd := `[Cli|
+  "addr-of" VIA runAddrOfCmd;
+  "Resolve a Lean.Name to its content address (in a `.ixe` or in the compiled-in env)"
+
+  FLAGS:
+    "ixe" : String; "Path to a serialized `.ixe` env to resolve the name in. Without this, the name is looked up in the compiled-in Lean env (via `loadIxonEnv` → `lookupAddr`)."
+
+  ARGS:
+    name : String; "Fully-qualified Lean.Name to resolve (e.g. `Nat.add_comm` or `Tests.Ix.Kernel.TutorialDefs.basicDef`)."
+]
+
+end