feat(aiur): Measured-ingress sharding

.github/workflows/bencher-thresholds-reset.yml

@@ -22,7 +22,7 @@ name: Bencher thresholds reset
 #     cancel by removing it before merge. Naming convention: one label per token,
 #     `bencher-thresholds-reset:<token>` where <token> is a workload (a backend
 #     testbed in Ix/Cli/BenchCmd.lean (backendSpecs) minus its runner-arch suffix:
-#     `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
+#     `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `aiur-shard`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
 #     `all` (the merge step expands an `all` label into every workload). Labeling
 #     requires Triage+, so PR authors from forks cannot self-queue a reset. The
 #     label shares the command/workflow name; the ref it moves is
@@ -44,7 +44,7 @@ on:
         # GitHub requires literal choice options, so this list stays static:
         # keep it (and the jobs' valid= lists below) in sync with the
         # backend testbeds in Ix/Cli/BenchCmd.lean (backendSpecs).
-        options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
+        options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, aiur-shard, zisk-check-execute, sp1-check-execute, ooc-check, all]
       sha:
         description: "Commit to anchor to (default: HEAD)"
         required: false
@@ -77,7 +77,7 @@ jobs:
           # (backendSpecs) minus the runner-arch suffix. Static because this
           # job runs on a cheap runner with no built `ix`; keep in sync when
           # adding a backend.
-          valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
+          valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive aiur-shard ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
           if [ "$EVENT" = workflow_dispatch ]; then
             # Reset the chosen workload(s) at the given commit; no PR scan.
             sha="${INPUT_SHA:-$HEAD_SHA}"
@@ -133,7 +133,7 @@ jobs:
           # which the merge job expands into every workload). Same static
           # list as the reset job; keep both in sync with backendSpecs in
           # Ix/Cli/BenchCmd.lean.
-          valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
+          valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive aiur-shard ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
           accepted="$valid all"
           # Parse the workload token(s) after the command, lowercased.
           workloads=$(printf '%s' "$BODY" \

Ix/Aiur/Protocol.lean

@@ -138,14 +138,22 @@ def proveAddrWithEnv (system : @& AiurSystem)
 
 @[extern "rs_aiur_system_shard_prove_with_env"]
 private opaque shardProveWithEnv' : @& AiurSystem →
-  @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
-    Except String ProveEnvResult
-
-/-- Per-shard prove against a Rust-owned `EnvHandle`. -/
+  @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → @& ByteArray →
+  @& ByteArray → @& String → Except String ProveEnvResult
+
+/-- Per-shard prove against a Rust-owned `EnvHandle`. `stubbedBlob` names the
+    blocks ingressed as type-only axioms; only the partition knows which those
+    are, so it travels from the `.ixes` manifest. `consultCacheDir` (empty =
+    disabled) is the keyed stub-consultation cache directory (normally
+    `~/.ix/cache/stub-consults`, one file per claim digest); a hit skips the
+    classification execute. -/
 def shardProveWithEnv (system : @& AiurSystem)
-  (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
+  (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
+  (ownedBlob foreignBlob stubbedBlob : ByteArray)
+  (consultCacheDir : String := "") :
     Except String (ByteArray × Proof × IOBuffer) :=
-  (shardProveWithEnv' system funIdx envHandle ownedBlob).map
+  (shardProveWithEnv' system funIdx envHandle ownedBlob foreignBlob
+    stubbedBlob consultCacheDir).map
     fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)
 
 @[extern "rs_aiur_system_verify"]

Ix/Aiur/Semantics/BytecodeFfi.lean

@@ -186,7 +186,8 @@ private opaque checkAddrWithEnv' : @& Bytecode.Toplevel →
 
 @[extern "rs_aiur_toplevel_shard_check_with_env"]
 private opaque shardCheckWithEnv' : @& Bytecode.Toplevel →
-  @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Bool →
+  @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → @& ByteArray →
+  @& ByteArray → Bool →
     Except String ExecuteResult
 
 /-- Per-claim check against a Rust-owned `EnvHandle`. `useBytecode`
@@ -206,9 +207,10 @@ def checkAddrWithEnv (toplevel : @& Bytecode.Toplevel)
     `checkAddrWithEnv` for `useBytecode` semantics. -/
 def shardCheckWithEnv (toplevel : @& Bytecode.Toplevel)
   (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
-  (ownedBlob : ByteArray) (useBytecode : Bool := false)
+  (ownedBlob foreignBlob stubbedBlob : ByteArray) (useBytecode : Bool := false)
   : Except String (Array G × IOBuffer × Array QueryCount) :=
-  (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob useBytecode).map
+  (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob foreignBlob
+    stubbedBlob useBytecode).map
     fun r => (r.output, .ofArrays r.ioData r.ioMap, r.queryCounts)
 
 end Bytecode.Toplevel

Ix/Claim.lean

@@ -137,11 +137,27 @@ Five variants in three families:
   the merkle tree rooted at `tree`. Used by aggregation to discharge
   leaves from a conditional claim's assumption set. Carries no
   assumptions.
+
+`checkEnv` carries a second root, `stubbed`, naming the subset of
+`assumptions` the claim ingressed as type-only axioms: their bodies were
+withheld, so the claim holds given only their TYPES, and no reduction
+passed through them.
+
+The two roots are genuinely different sets, which is why one cannot serve
+for both. A shard skips checking everything it does not own, but it must
+still ingress in FULL anything it reduces through — a definition it
+unfolds, or an inductive whose recursor rules it applies — even though
+another shard is responsible for checking that constant. Those blocks are
+in `assumptions` but NOT in `stubbed`. Folding them into the owned set
+instead is not possible: owned sets partition the environment so each
+constant is checked exactly once, and two shards may reduce through the
+same constant.
 -/
 inductive Claim where
   | eval     (input output : Address) (assumptions : Option Address)
   | check    (const : Address) (assumptions : Option Address)
   | checkEnv (root : Address) (assumptions : Option Address)
+             (stubbed : Option Address)
   | reveal   (comm : Address) (info : RevealConstantInfo)
   | contains (tree : Address) (const : Address)
   deriving BEq, Repr, Inhabited
@@ -494,10 +510,11 @@ def put : Claim → PutM Unit
     putTag4 ⟨FLAG_CLAIM, VARIANT_CHECK_CLAIM⟩
     Serialize.put const
     putOptAddr assumptions
-  | .checkEnv root assumptions => do
+  | .checkEnv root assumptions stubbed => do
     putTag4 ⟨FLAG_CLAIM, VARIANT_CHECK_ENV_CLAIM⟩
     Serialize.put root
     putOptAddr assumptions
+    putOptAddr stubbed
   | .reveal comm info => do
     putTag4 ⟨FLAG_CLAIM, VARIANT_REVEAL_CLAIM⟩
     Serialize.put comm
@@ -523,7 +540,8 @@ def get : GetM Claim := do
   else if tag.size == VARIANT_CHECK_ENV_CLAIM then
     let root ← Serialize.get
     let asm ← getOptAddr
-    return .checkEnv root asm
+    let stubbed ← getOptAddr
+    return .checkEnv root asm stubbed
   else if tag.size == VARIANT_REVEAL_CLAIM then
     return .reveal (← Serialize.get) (← RevealConstantInfo.get)
   else if tag.size == VARIANT_CONTAINS_CLAIM then
@@ -538,7 +556,7 @@ instance : ToString Claim where
   toString c := match c with
     | .eval i o asm => s!"Eval({i}, {o}, {asm})"
     | .check v asm => s!"Check({v}, {asm})"
-    | .checkEnv r asm => s!"CheckEnv({r}, {asm})"
+    | .checkEnv r asm st => s!"CheckEnv({r}, {asm}, {st})"
     | .reveal comm info => s!"Reveal({comm}, {repr info})"
     | .contains t c => s!"Contains({t}, {c})"
 
@@ -566,7 +584,7 @@ namespace Proof
 def variantOf : Ix.Claim → UInt64
   | .eval _ _ _     => Ix.Claim.VARIANT_EVAL_PROOF
   | .check _ _      => Ix.Claim.VARIANT_CHECK_PROOF
-  | .checkEnv _ _   => Ix.Claim.VARIANT_CHECK_ENV_PROOF
+  | .checkEnv _ _ _ => Ix.Claim.VARIANT_CHECK_ENV_PROOF
   | .reveal _ _     => Ix.Claim.VARIANT_REVEAL_PROOF
   | .contains _ _   => Ix.Claim.VARIANT_CONTAINS_PROOF
 
@@ -580,9 +598,10 @@ def put (p : Proof) : PutM Unit := do
   | .check addr asm => do
     Serialize.put addr
     Ix.Claim.putOptAddr asm
-  | .checkEnv root asm => do
+  | .checkEnv root asm stubbed => do
     Serialize.put root
     Ix.Claim.putOptAddr asm
+    Ix.Claim.putOptAddr stubbed
   | .reveal comm info => do
     Serialize.put comm
     Ix.RevealConstantInfo.put info
@@ -609,7 +628,8 @@ def get : GetM Proof := do
     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)
+      let stubbed ← Ix.Claim.getOptAddr
+      pure (.checkEnv root asm stubbed)
     else if tag.size == Ix.Claim.VARIANT_REVEAL_PROOF then do
       let comm ← Serialize.get
       let info ← Ix.RevealConstantInfo.get