feat(aiur): Accurate whole-env sharding based on execution measurements

Ix/Aiur/Protocol.lean

@@ -104,6 +104,27 @@ opaque vkBytes : @& AiurSystem → ByteArray
 @[extern "rs_aiur_system_circuit_shapes"]
 opaque circuitShapes : @& AiurSystem → Array CircuitShape
 
+/-- Scan-and-cut sharding against a Rust-owned `EnvHandle`, cutting on
+    the system's analytic peak-prove-RAM prediction (the system carries
+    the toplevel, so none is passed). Numeric params are decimal strings:
+    budget (GiB), eps (percent), workers (0 = autoscale), fail-fast ("0"
+    skips kernel-rejected blocks into a `.failed.csv`). Writes the `.ixes`
+    manifest and its costs sidecar to the output path. -/
+@[extern "rs_aiur_scan_shards_with_env"]
+opaque scanShardsWithEnv : @& AiurSystem →
+  @& Bytecode.FunIdx → @& EnvHandle → @& String → @& String → @& String →
+  @& String → @& String → @& String → @& String → Except String Unit
+
+/-- The child side of the scan's process pool: run the stdin/stdout
+    worker loop until EOF (see `crates/ffi/src/aiur/scan.rs`,
+    `scan_worker`). Spawned by the parent scan as `ix shard-worker`;
+    numeric params are decimal strings: cut (GiB), batch blocks, soft
+    record cut (GiB), schedule pieces, exec-only ("1"/"0"). -/
+@[extern "rs_aiur_scan_worker"]
+opaque scanWorker : @& AiurSystem →
+  @& Bytecode.FunIdx → @& EnvHandle → @& String → @& String → @& String →
+  @& String → @& String → Except String Unit
+
 @[extern "rs_aiur_system_prove"]
 private opaque prove' : @& AiurSystem →
   @& Bytecode.FunIdx → @& Array G →

Ix/Aiur/Semantics/BytecodeFfi.lean

@@ -211,6 +211,16 @@ def shardCheckWithEnv (toplevel : @& Bytecode.Toplevel)
   (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob useBytecode).map
     fun r => (r.output, .ofArrays r.ioData r.ioMap, r.queryCounts)
 
+/-- Execute-only whole-env check through the codegen'd Aiur kernel: no
+    partition, no manifest — the check verdict plus measured totals,
+    reported on stderr. Args: workers (0 = autoscale), fail-fast ("0"
+    records and skips kernel-rejected blocks; anything else aborts on
+    the first). -/
+@[extern "rs_aiur_execute_env_with_env"]
+opaque executeEnvWithEnv : @& Bytecode.Toplevel →
+  @& Bytecode.FunIdx → @& EnvHandle → @& String → @& String → @& String →
+  @& String → Except String Unit
+
 end Bytecode.Toplevel
 
 end Aiur

Ix/Cli/AddrOfCmd.lean

@@ -1,12 +1,15 @@
 /-
-  `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
+  `ix addr-of <Lean.Name> [--ixe <path>] [--ixes <manifest>]`: 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.
+  With `--ixes` (requires `--ixe`), a second line reports which shard of
+  the manifest's partition owns the name's check-schedule block — the
+  shard whose prove type-checks this constant.
 -/
 module
 public import Cli
@@ -16,6 +19,7 @@ public import Ix.Environment
 public import Ix.IxVM.ClaimHarness
 public import Ix.Ixon
 public import Ix.Meta
+public import Ix.Cli.CheckCmd
 public import Ix.Cli.NameResolve
 
 public section
@@ -42,7 +46,33 @@ def runAddrOfCmd (p : Cli.Parsed) : IO UInt32 := do
     | none =>
       IO.eprintln s!"error: {name} not found in {path}"; return 1
     | some addr =>
-      IO.println (toString addr); return 0
+      IO.println (toString addr)
+      if let some manifestPath := (p.flag? "ixes").map (·.as! String) then
+        -- Owning-shard lookup: the constant's check-schedule block (a
+        -- projection collapses to its SCC/Muts wrapper), searched in the
+        -- manifest's owned-block lists.
+        let c? : Option Ixon.Constant := Id.run do
+          for (a, lc) in ixonEnv.consts do
+            if a == addr then return lc.get?
+          return none
+        let some c := c?
+          | IO.eprintln s!"error: {addr} has no parseable constant in {path}"
+            return 1
+        let block := Ix.Cli.CheckCmd.blockAddrOf addr c
+        match Ix.Cli.CheckCmd.parseIxesShards
+            (← IO.FS.readBinFile manifestPath) with
+        | .error e =>
+          IO.eprintln s!"error: {manifestPath}: {e}"; return 1
+        | .ok shards =>
+          match (shards.mapIdx (fun k s => (s, k))).find?
+              (fun (s, _) => s.blocks.contains block) with
+          | some (s, k) =>
+            IO.println s!"block {block} → shard {k} \
+              ({s.blocks.size} blocks, cost {s.cost})"
+          | none =>
+            IO.println s!"block {block} → no owning shard \
+              (excluded from the partition)"
+      return 0
   | none =>
     let env ← get_env!
     if !env.constants.contains name then
@@ -62,6 +92,7 @@ def addrOfCmd : Cli.Cmd := `[Cli|
 
   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`)."
+    "ixes" : String; "Path to a `.ixes` shard manifest (requires --ixe): also report which shard owns the name's check-schedule block — the shard whose prove type-checks this constant."
 
   ARGS:
     name : String; "Fully-qualified Lean.Name to resolve (e.g. `Nat.add_comm` or `Tests.Ix.Kernel.TutorialDefs.basicDef`)."