Jcb/kernel sharding

Ix/Cli/ProfileCmd.lean

@@ -0,0 +1,67 @@
+/-
+  `ix profile <path.ixe>`: run the Ix kernel out of circuit over a serialized
+  `.ixe` environment, recording per-block heartbeats and the delta-unfold graph
+  into a `.ixesp` sidecar. This is the cost model consumed by `ix shard`
+  (see `plans/sharding.md`).
+
+  Recording defaults to *cache-isolated* mode: the kernel clears its
+  cross-constant reduction-memo caches between constants so every delta-unfold
+  re-executes (sound recording) and recorded heartbeats reflect the in-circuit
+  (un-memoized) cost. `--keep-caches` trades fidelity for speed.
+-/
+module
+public import Cli
+public import Ix.Common
+public import Ix.KernelCheck
+public import Std.Internal.UV.System
+
+public section
+
+open Ix.KernelCheck
+
+namespace Ix.Cli.ProfileCmd
+
+def runProfileCmd (p : Cli.Parsed) : IO UInt32 := do
+  let some pathArg := p.positionalArg? "path"
+    | p.printError "error: must specify <path> to a .ixe file"
+      return 1
+  let envPath := pathArg.as! String
+  let outPath : String :=
+    match p.flag? "out" with
+    | some flag => flag.as! String
+    | none      => envPath ++ ".ixesp"
+  let isolate := !(p.flag? "keep-caches" |>.isSome)
+  let quiet   := !(p.flag? "verbose" |>.isSome)
+
+  if let some flag := p.flag? "workers" then
+    let n := flag.as! Nat
+    if n == 0 then
+      p.printError "error: --workers must be > 0"
+      return 1
+    Std.Internal.UV.System.osSetenv "IX_KERNEL_CHECK_WORKERS" (toString n)
+
+  IO.println s!"Profiling {envPath} → {outPath} (isolate={isolate})"
+  let start ← IO.monoMsNow
+  rsProfileAnonFFI envPath outPath isolate quiet
+  let elapsed := (← IO.monoMsNow) - start
+  IO.println s!"[profile] wrote {outPath} in {elapsed.formatMs}"
+  return 0
+
+end Ix.Cli.ProfileCmd
+
+open Ix.Cli.ProfileCmd in
+def profileCmd : Cli.Cmd := `[Cli|
+  "profile" VIA runProfileCmd;
+  "Profile a `.ixe` out of circuit → `.ixesp` (sharding cost + delta graph)"
+
+  FLAGS:
+    out           : String; "Output .ixesp path (default: <path>.ixesp)"
+    "keep-caches";          "Keep cross-constant caches: faster, lower-fidelity, may under-record"
+    workers       : Nat;    "Parallel kernel workers (default: available_parallelism). Plumbs IX_KERNEL_CHECK_WORKERS."
+    verbose;                "Log every constant (default: quiet)"
+
+  ARGS:
+    path : String; "Path to a serialized .ixe environment"
+]
+
+end

Ix/Cli/ShardCmd.lean

@@ -0,0 +1,62 @@
+/-
+  `ix shard <path.ixesp> --shards N`: partition a profiled environment into `N`
+  shards via recursive balanced min-cut bisection, minimizing cross-shard
+  delta-unfold ingress (see `plans/sharding.md`).
+
+  Reads the `.ixesp` produced by `ix profile` (pure offline graph work, so `N`
+  is cheap to re-tune without re-running the kernel). Writes a `.ixes` manifest
+  and prints a what-if report (per-shard heartbeat balance + total cross-shard
+  ingress). The partitioner is self-contained — no external graph-library
+  dependency.
+-/
+module
+public import Cli
+public import Ix.KernelCheck
+
+public section
+
+open Ix.KernelCheck
+
+namespace Ix.Cli.ShardCmd
+
+def runShardCmd (p : Cli.Parsed) : IO UInt32 := do
+  let some pathArg := p.positionalArg? "path"
+    | p.printError "error: must specify <path> to a .ixesp file"
+      return 1
+  let espPath := pathArg.as! String
+  let numShards : Nat :=
+    match p.flag? "shards" with
+    | some flag => flag.as! Nat
+    | none      => 1
+  let balancePct : Nat :=
+    match p.flag? "balance" with
+    | some flag => flag.as! Nat
+    | none      => 5
+  let outPath : String :=
+    match p.flag? "out" with
+    | some flag => flag.as! String
+    | none      => espPath ++ ".ixes"
+
+  IO.println s!"Sharding {espPath} into {numShards} shards (balance ±{balancePct}%)"
+  rsShardEspFFI espPath (toString numShards) (toString balancePct) outPath
+  if !outPath.isEmpty then
+    IO.println s!"[shard] wrote {outPath}"
+  return 0
+
+end Ix.Cli.ShardCmd
+
+open Ix.Cli.ShardCmd in
+def shardCmd : Cli.Cmd := `[Cli|
+  "shard" VIA runShardCmd;
+  "Partition a `.ixesp` into N balanced shards minimizing cross-shard delta"
+
+  FLAGS:
+    shards  : Nat;    "Number of shards N (default 1 = a single shard)"
+    balance : Nat;    "Per-bisection balance tolerance, percent (default 5)"
+    out     : String; "Output .ixes manifest path (default: <path>.ixes)"
+
+  ARGS:
+    path : String; "Path to a .ixesp produced by `ix profile`"
+]
+
+end

Ix/KernelCheck.lean

@@ -142,6 +142,30 @@ opaque rsCheckAnonFFI :
     @& String →                          -- fail-out path ("" = none)
     IO (Array (String × Option CheckError))
 
+/-- FFI: profile a `.ixe` out of circuit, writing a `.ixesp` sidecar with
+    per-block heartbeats + the delta-unfold graph (the sharding cost model,
+    see `plans/sharding.md`). Runs the anon kernel over every checkable target.
+    `isolate` clears the kernel's reduction-memo caches between constants for
+    sound/faithful recording; `quiet` suppresses per-constant progress. -/
+@[extern "rs_kernel_profile_anon"]
+opaque rsProfileAnonFFI :
+    @& String →                          -- .ixe path
+    @& String →                          -- .ixesp output path
+    @& Bool →                            -- isolate caches
+    @& Bool →                            -- quiet
+    IO Unit
+
+/-- FFI: partition a `.ixesp` into `numShards` shards, writing a `.ixes`
+    manifest. `numShards` and `balancePct` are decimal strings (kept ABI-simple).
+    Empty `outPath` skips the manifest. Prints a what-if report to stderr. -/
+@[extern "rs_shard_esp"]
+opaque rsShardEspFFI :
+    @& String →                          -- .ixesp path
+    @& String →                          -- num_shards (N)
+    @& String →                          -- balance percent
+    @& String →                          -- .ixes output path ("" = skip)
+    IO Unit
+
 end Ix.KernelCheck
 
 end

Main.lean

@@ -5,7 +5,9 @@ import Ix.Cli.CheckRsCmd
 import Ix.Cli.ClaimCmd
 import Ix.Cli.CompileCmd
 import Ix.Cli.IngressCmd
+import Ix.Cli.ProfileCmd
 import Ix.Cli.ProveCmd
+import Ix.Cli.ShardCmd
 import Ix.Cli.TreeCmd
 import Ix.Cli.ValidateCmd
 import Ix.Cli.VerifyCmd
@@ -27,7 +29,9 @@ def ixCmd : Cli.Cmd := `[Cli|
     checkRsCmd;
     claimCmd;
     treeCmd;
+    profileCmd;
     proveCmd;
+    shardCmd;
     verifyCmd;
     addrOfCmd;
     ingressCmd;