From 21723da9e07128d429067aa6a8ea475a52a94bd6 Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Tue, 9 Jun 2026 05:22:39 -0700 Subject: [PATCH] Sharding: per-shard check / prove / verify on the IxVM kernel Wire the `.ixes` manifest into the proving path: a sharded environment can now be checked, proven, and verified as independent per-shard CheckEnv claims that compose off-circuit into a whole-environment "well-typed" verdict. No kernel changes -- a shard is the existing `Claim.CheckEnv(env_root, asm)`: `run_check_env` ingresses the shard's reference closure and `check_all_skipping` checks exactly the owned constants, trusting (skipping) the frontier. CLI: `check`, `prove`, and `verify` all gain the same shape -- `--ixe --ixes [--shard K]`: ``` ix check --ixe E --ixes M --shard K check shard K (Aiur bytecode) ix check --ixe E --ixes M check every shard concurrently after a coverage check (--jobs N caps RAM) ix prove --ixe E --ixes M --shard K STARK-prove shard K ix prove --ixe E --ixes M prove every shard (sequential) ix verify --ixe E --ixes M coverage verdict (disjoint cover) ix verify --ixe E --ixes M --shard K [P] shard K's claim digest, or bind+verify P ix verify --ixe E --ixes M P0 P1 ... composed verdict: every proof bound to a shard, every shard covered, + coverage ix verify P0 P1 ... plain proof verification ``` Shard -> claim. A shard's owned set is every env constant whose check-schedule block is owned by that shard, where a projection collapses to its SCC/Muts wrapper and everything else is its own block (mirrors `check_schedule_block_addr`). The CheckEnv claim is reconstructed deterministically from (env, owned) -- canonical trees sort addresses -- so the digest a `prove --shard K` commits is reproducible, and `verify` binds a proof to its shard by digest equality. Soundness is off-circuit: every constant's block must be owned by exactly one shard (disjoint cover) -- then each constant is checked once and every shard's frontier is owned (checked) by another shard. Full ingress pins types via the per-constant blake3, so no cross-shard type matching is needed; coverage alone suffices for `check`, coverage + per-shard proof verification for `verify`. `check` parallelizes across shards (independent read-only bytecode runs, one dedicated task each); `--jobs N` caps the number in flight, since each shard re-ingests its closure into its own IO buffer. `prove` stays sequential (each STARK proof is RAM-heavy). Other: - `.ixes` parser is a bounds-checked StateT cursor: a truncated/malformed manifest yields a clean error, never an index-out-of-bounds panic. - ClaimHarness: `shardCheckEnvClaim` (claim + closure + assumption trees, no IO buffer -- cheap reconstruction for binding) and `buildShardCheckEnvWitness` (the witness, IO buffer restricted to the shard closure). - `lake exe arena-exclude --out ` writes the exclude list to a file instead of stdout, so callers don't need a shell redirect. Validated end-to-end on a small kernel-arena env (profile -> shard 4 -> prove all -> composed verify), including the negative cases (wrong-shard binding and coverage gaps rejected). --- Ix/Cli/CheckCmd.lean | 204 +++++++++++++++++++++++++++++- Ix/Cli/ProveCmd.lean | 12 +- Ix/Cli/VerifyCmd.lean | 133 +++++++++++++++---- Ix/IxVM/ClaimHarness.lean | 42 ++++++ Tests/Ix/Kernel/ArenaExclude.lean | 25 +++- 5 files changed, 383 insertions(+), 33 deletions(-) diff --git a/Ix/Cli/CheckCmd.lean b/Ix/Cli/CheckCmd.lean index 142caf0e..8e72bc75 100644 --- a/Ix/Cli/CheckCmd.lean +++ b/Ix/Cli/CheckCmd.lean @@ -242,6 +242,190 @@ def forEachClaim for n in failures do IO.eprintln s!" {n}" pure 1 +-- Bounds-checked little-endian cursor over a `.ixes` byte buffer. Every read +-- verifies the buffer has enough bytes and returns `.error` on underflow — no +-- `b[p]!` panics on a truncated/malformed manifest. +private abbrev IxesP := StateT (ByteArray × Nat) (Except String) + +private def ixesU8 : IxesP UInt8 := do + let (b, p) ← get + if h : p < b.size then + modify (fun _ => (b, p + 1)) + pure b[p] + else throw "ixes: truncated (expected a byte)" + +private def ixesU32 : IxesP UInt32 := do + let a ← ixesU8; let b ← ixesU8; let c ← ixesU8; let d ← ixesU8 + pure (a.toUInt32 ||| (b.toUInt32 <<< 8) ||| (c.toUInt32 <<< 16) ||| (d.toUInt32 <<< 24)) + +private def ixesSkip (n : Nat) : IxesP Unit := do + let (b, p) ← get + if p + n ≤ b.size then modify (fun _ => (b, p + n)) else throw s!"ixes: truncated (skip {n})" + +private def ixesAddr : IxesP Address := do + let (b, p) ← get + if p + 32 ≤ b.size then modify (fun _ => (b, p + 32)); pure ⟨b.extract p (p + 32)⟩ + else throw "ixes: truncated (expected a 32-byte address)" + +/-- Parse every shard's owned block addresses from a serialized `.ixes` + manifest (`ShardManifest::to_bytes`, `src/ix/shard.rs`): + magic(8) ‖ total_cross_ingress(u128) ‖ num_shards(u32) ‖ per shard + { id(u32) ‖ heartbeats(u64) ‖ own_size(u64) ‖ cross_ingress(u64) ‖ + assumption_root(u8 tag + 32?) ‖ blocks(u32 len + 32·len) ‖ + foreign_blocks(u32 len + 32·len) }. + Bounds-checked: a truncated/malformed file yields `.error`, never a panic. -/ +def parseIxesAllShards (bytes : ByteArray) : Except String (Array (Array Address)) := + let go : IxesP (Array (Array Address)) := do + let m0 ← ixesU8; let m1 ← ixesU8; let m2 ← ixesU8; let m3 ← ixesU8 + if !(m0 == 0x49 && m1 == 0x58 && m2 == 0x45 && m3 == 0x53) then + throw "not an .ixes file (bad magic)" + ixesSkip 4 -- rest of the 8-byte magic + ixesSkip 16 -- total_cross_ingress (u128) + let n ← ixesU32 + let mut shards : Array (Array Address) := #[] + for _ in [0:n.toNat] do + ixesSkip (4 + 8 + 8 + 8) -- id + heartbeats + own_size + cross_ingress + if (← ixesU8) == 1 then ixesSkip 32 -- assumption_root present + let blen ← ixesU32 + let mut blocks : Array Address := #[] + for _ in [0:blen.toNat] do + blocks := blocks.push (← ixesAddr) + ixesSkip ((← ixesU32).toNat * 32) -- skip foreign_blocks + shards := shards.push blocks + pure shards + go.run' (bytes, 0) + +/-- The check-schedule block address of a constant: a projection collapses + to its SCC/Muts wrapper (`p.block`); everything else is its own block. + Mirrors `check_schedule_block_addr` (`src/ffi/kernel.rs`). -/ +private def blockAddrOf (addr : Address) (c : Ixon.Constant) : Address := + match c.info with + | .iPrj prj => prj.block + | .cPrj prj => prj.block + | .rPrj prj => prj.block + | .dPrj prj => prj.block + | _ => addr + +/-- Owned constants of a shard: every env constant whose check-schedule block + is in `blocks`. -/ +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 + if blockSet.contains (blockAddrOf addr c) then o := o.push addr + return o + +/-- The `CheckEnv` claim digest a shard's proof commits to — reconstructed + deterministically from the env + the shard's owned blocks. Matches the + digest `prove --shard K` produced, so a proof can be bound to its shard. -/ +def shardClaimDigest (ixonEnv : Ixon.Env) (blocks : Array Address) : Except String Address := do + let (claim, _, _) ← IxVM.ClaimHarness.shardCheckEnvClaim ixonEnv (ownedConstsForBlocks ixonEnv blocks) + pure (Address.blake3 (Ix.Claim.ser claim)) + +/-- Load the `.ixe` env and the `.ixes` shard partition together (each file + read once). Shared by every manifest-driven shard path. -/ +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 + | .error e => return .error s!"deserialize {ixePath} failed: {e}" + | .ok env => return .ok (env, shards) + +/-- Run the shard operation for one shard, given the already-loaded env and the + shard's owned `blocks`: build the `CheckEnv` witness over the owned consts + (ingress their closure, skip the frontier) and dispatch `runOne`. -/ +def runShardOwned (ixonEnv : Ixon.Env) (blocks : Array Address) (shardK : Nat) + (runOne : Ix.Claim → IxVM.ClaimHarness.ClaimWitness → String → IO UInt32) : IO UInt32 := do + let owned := ownedConstsForBlocks ixonEnv blocks + IO.println s!"[shard] shard {shardK}: {blocks.size} owned blocks → \ + {owned.size}/{ixonEnv.consts.size} owned consts" + match IxVM.ClaimHarness.buildShardCheckEnvWitness ixonEnv owned with + | .error e => IO.eprintln s!"shard witness build failed: {e}"; return 1 + | .ok (claim, witness) => runOne claim witness s!"shard {shardK}" + +/-- Manifest-driven check/prove of one shard `shardK` of the partition. -/ +def runShardCheckManifest (manifestPath ixePath : String) (shardK : Nat) + (runOne : Ix.Claim → IxVM.ClaimHarness.ClaimWitness → String → IO UInt32) : IO UInt32 := do + match (← loadEnvAndShards manifestPath ixePath) with + | .error e => IO.eprintln e; return 1 + | .ok (ixonEnv, shards) => match shards[shardK]? with + | none => IO.eprintln s!"shard {shardK} out of range ({shards.size} shards)"; return 1 + | some blocks => runShardOwned ixonEnv blocks shardK runOne + +/-- Run the shard operation over EVERY shard — the whole-partition behavior of + `--ixes` with no `--shard` (used by `prove`). Loads the env once. Returns 1 + if any shard fails, else 0. -/ +def runShardManifestAll (manifestPath ixePath : String) + (runOne : Ix.Claim → IxVM.ClaimHarness.ClaimWitness → String → IO UInt32) : IO UInt32 := do + match (← loadEnvAndShards manifestPath ixePath) with + | .error e => IO.eprintln e; return 1 + | .ok (ixonEnv, shards) => + let mut rc : UInt32 := 0 + for (blocks, k) in shards.mapIdx (fun k b => (b, k)) do + if (← runShardOwned ixonEnv blocks k runOne) != 0 then rc := 1 + pure rc + +/-- Coverage check over already-loaded env + shards: every constant's + check-schedule block is owned by **exactly one** shard. That is the whole + soundness condition for the check case — each constant is type-checked + once, and every shard's frontier (closure minus owned) is therefore owned + (checked) by some other shard. Prints the per-shard report; returns whether + the partition is a valid disjoint cover (no block owned by two shards, no + constant whose block no shard owns). -/ +def shardsCover (ixonEnv : Ixon.Env) (shards : Array (Array Address)) : IO Bool := do + -- block → shard, detecting blocks claimed by more than one shard. + let mut blockToShard : Std.HashMap Address Nat := {} + let mut dup : Nat := 0 + for (blocks, k) in shards.mapIdx (fun k b => (b, k)) do + for blk in blocks do + match blockToShard.get? blk with + | some _ => dup := dup + 1 + | none => blockToShard := blockToShard.insert blk k + -- 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 + 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 + IO.println s!"[shards] {shards.size} shards, {ixonEnv.consts.size} consts" + for (blocks, k) in shards.mapIdx (fun k b => (b, k)) do + IO.println s!" shard {k}: {blocks.size} blocks, {(counts[k]?).getD 0} consts" + if dup != 0 then + IO.eprintln s!"[shards] FAIL: {dup} block(s) owned by >1 shard (not disjoint)" + if unowned != 0 then + IO.eprintln s!"[shards] FAIL: {unowned} const(s) with no owning shard (coverage gap)" + let ok := dup == 0 && unowned == 0 + if ok then + IO.println s!"[shards] OK: partition covers all {ixonEnv.consts.size} consts, disjoint" + pure ok + +/-- Check EVERY shard of the partition concurrently (shards are independent + bytecode runs) after verifying coverage — the whole-partition behavior of + `check --ixes` with no `--shard`. At most `jobs` shards run at once + (`none` ⇒ all of them); cap it to bound peak RAM, since each in-flight + shard's IO buffer re-ingests its whole closure. Returns 1 on a coverage gap + or any shard failure. -/ +def runShardCheckAll (manifestPath ixePath : String) (jobs? : Option Nat) + (runOne : Ix.Claim → IxVM.ClaimHarness.ClaimWitness → String → IO UInt32) : IO UInt32 := do + let (ixonEnv, shards) ← match (← loadEnvAndShards manifestPath ixePath) with + | .error e => IO.eprintln e; return 1 + | .ok r => pure r + if !(← shardsCover ixonEnv shards) then return 1 + -- The env + compiled toplevel are read-only, so each shard runs on its own + -- dedicated task; chunk by `jobs` to cap the number in flight at once. + let maxJobs := max 1 (jobs?.getD shards.size) + let mut rc : UInt32 := 0 + for chunk in (shards.mapIdx (fun k b => (b, k))).toList.toChunks maxJobs do + let tasks ← chunk.mapM fun (blocks, k) => + IO.asTask (prio := .dedicated) (runShardOwned ixonEnv blocks k runOne) + for t in tasks do + match t.get with + | .ok r => if r != 0 then rc := 1 + | .error e => IO.eprintln s!"shard check task failed: {e}"; rc := 1 + pure rc + def runCheckCmd (p : Cli.Parsed) : IO UInt32 := do -- Always silence the Rust-side `[compile_env]` progress logs. The -- per-name labels + stats are signal enough at this layer. @@ -255,7 +439,11 @@ def runCheckCmd (p : Cli.Parsed) : IO UInt32 := do let claimHex : Option String := (p.flag? "claim").map (·.as! String) let names := (p.variableArgsAs! String).toList - let printStats := names.length == 1 || claimHex.isSome + let ixesPath := (p.flag? "ixes").map (·.as! String) + let shardK := (p.flag? "shard").map (·.as! Nat) + -- a single targeted constant, a `--claim`, or a single shard each print + -- per-circuit stats; whole-env / whole-partition iteration suppresses them. + let printStats := names.length == 1 || claimHex.isSome || (ixesPath.isSome && shardK.isSome) let toplevel ← match IxVM.ixVM with | .error e => IO.eprintln s!"Toplevel merging failed: {e}"; return 1 | .ok t => pure t @@ -270,8 +458,15 @@ def runCheckCmd (p : Cli.Parsed) : IO UInt32 := do | .error e => IO.eprintln s!"Compilation failed: {e}"; return 1 | .ok c => pure c pure (runCompiled compiled printStats statsOut) - forEachClaim ixePath claimHex names keepGoing "check" - (fun _ w l => runOne w l) + match ixePath, ixesPath, shardK with + | some ixe, some manifest, some k => + return (← runShardCheckManifest manifest ixe k (fun _c w l => runOne w l)) + | some ixe, some manifest, none => + return (← runShardCheckAll manifest ixe ((p.flag? "jobs").map (·.as! Nat)) + (fun _c w l => runOne w l)) + | _, _, _ => + forEachClaim ixePath claimHex names keepGoing "check" + (fun _ w l => runOne w l) end Ix.Cli.CheckCmd @@ -286,6 +481,9 @@ def checkCmd : Cli.Cmd := `[Cli| "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)." + "ixes" : String; "Path to a `.ixes` shard manifest (with --ixe). With --shard K: check the constants owned by shard K (ingress their closure, skip the frontier). Without --shard: check every shard of the partition concurrently, after a coverage check." + "shard" : Nat; "0-based shard index K (with --ixe + --ixes): check the constants owned by shard K of the manifest's partition." + "jobs" : Nat; "Max shards to check concurrently when checking a whole partition (--ixes without --shard). Default: all at once. Lower it to bound peak RAM — each in-flight shard re-ingests its closure into its own IO buffer." ARGS: ...names : String; "Fully-qualified Lean.Name(s) to check. With none, iterate every named constant in the env (sorted)." diff --git a/Ix/Cli/ProveCmd.lean b/Ix/Cli/ProveCmd.lean index 2afe1287..5b1fb25a 100644 --- a/Ix/Cli/ProveCmd.lean +++ b/Ix/Cli/ProveCmd.lean @@ -94,8 +94,14 @@ def runProveCmd (p : Cli.Parsed) : IO UInt32 := do | .error e => IO.eprintln s!"compilation failed: {e}"; return 1 | .ok c => pure c let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters - Ix.Cli.CheckCmd.forEachClaim ixePath claimHex names keepGoing "prove" - (proveOne aiurSystem compiled) + let runOne := proveOne aiurSystem compiled + match ixePath, (p.flag? "ixes").map (·.as! String), (p.flag? "shard").map (·.as! Nat) with + | some ixe, some manifest, some k => + Ix.Cli.CheckCmd.runShardCheckManifest manifest ixe k runOne + | some ixe, some manifest, none => + Ix.Cli.CheckCmd.runShardManifestAll manifest ixe runOne + | _, _, _ => + Ix.Cli.CheckCmd.forEachClaim ixePath claimHex names keepGoing "prove" runOne end Ix.Cli.ProveCmd @@ -108,6 +114,8 @@ def proveCmd : Cli.Cmd := `[Cli| "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, proves the persisted claim against the `--ixe` env (single proof, skips per-const iteration)." + "ixes" : String; "Path to a `.ixes` shard manifest (with --ixe). With --shard K: prove shard K. Without --shard: prove every shard in the partition." + "shard" : Nat; "0-based shard index K (with --ixes and --ixe): prove that one shard's CheckEnv claim." ARGS: ...names : String; "Fully-qualified Lean.Name(s) to prove. With none, iterate every named constant in the env (sorted)." diff --git a/Ix/Cli/VerifyCmd.lean b/Ix/Cli/VerifyCmd.lean index d0774d67..e66b5548 100644 --- a/Ix/Cli/VerifyCmd.lean +++ b/Ix/Cli/VerifyCmd.lean @@ -18,6 +18,7 @@ public import Ix.Common public import Ix.IxVM public import Ix.IxVM.ClaimHarness public import Ix.Store +public import Ix.Cli.CheckCmd public section @@ -46,30 +47,14 @@ private def friParameters : Aiur.FriParameters := { queryProofOfWorkBits := 0 } -def runVerifyCmd (p : Cli.Parsed) : IO UInt32 := do - let some proofArg := p.positionalArg? "proof" - | p.printError "error: must specify "; return 1 - let proofAddr ← addrOfHex! "proof" (proofArg.as! String) - - -- 1. Load + decode the wrapper from the store. +/-- Verify one persisted `Ixon.Proof` wrapper (by store address) against its + bundled claim, using an already-built Aiur backend. -/ +def verifyOneProof (aiurSystem : Aiur.AiurSystem) (compiled : Aiur.CompiledToplevel) + (proofAddr : Address) : IO UInt32 := do let bytes ← StoreIO.toIO (Store.read proofAddr) let wrapper ← IO.ofExcept (Ixon.Proof.de bytes) - - -- 2. Recover the Aiur Proof object from the opaque bytes. let proof := Aiur.Proof.ofBytes wrapper.proof - - -- 3. Rebuild the Aiur backend (must match the proving side). - let toplevel ← match IxVM.ixVM with - | .error e => IO.eprintln s!"toplevel merging failed: {e}"; return 1 - | .ok t => pure t - let compiled ← match toplevel.compile with - | .error e => IO.eprintln s!"compilation failed: {e}"; return 1 - | .ok c => pure c - let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters - - -- 4. Reconstruct the Aiur-level public input from the wrapper's - -- claim. `verify_claim` takes a 32-G blake3 digest of the - -- serialized claim bytes (see `IxVM.ClaimHarness.buildClaimWitness`). + -- `verify_claim` takes the 32-G blake3 digest of the serialized claim. let claimDigest := Address.blake3 (Ix.Claim.ser wrapper.claim) let funIdx ← match compiled.getFuncIdx `verify_claim with | some i => pure i @@ -78,8 +63,6 @@ def runVerifyCmd (p : Cli.Parsed) : IO UInt32 := do return 1 let input : Array Aiur.G := claimDigest.hash.data.map .ofUInt8 let aiurClaim := Aiur.buildClaim funIdx input #[] - - -- 5. Verify. match aiurSystem.verify friParameters aiurClaim proof with | .ok () => IO.println s!"ok: proof {proofAddr} verifies claim {claimDigest}" @@ -88,15 +71,115 @@ def runVerifyCmd (p : Cli.Parsed) : IO UInt32 := do IO.eprintln s!"error: verification failed: {e}" return 1 +/-- Build the Aiur backend (toplevel → compile → system), matching the proving + side. Shared by every proof-verifying path. -/ +def buildBackend : IO (Except String (Aiur.AiurSystem × Aiur.CompiledToplevel)) := do + match IxVM.ixVM with + | .error e => return .error s!"toplevel merging failed: {e}" + | .ok toplevel => match toplevel.compile with + | .error e => return .error s!"compilation failed: {e}" + | .ok compiled => + return .ok (Aiur.AiurSystem.build compiled.bytecode commitmentParameters, compiled) + +/-- Shard-aware verification (parity with `check`/`prove`): + - `--shard K`, no proof: print shard K's reconstructed `CheckEnv` claim + digest (the public input its proof must commit). + - `--shard K` + proof(s): verify each proof AND bind it to shard K (its + bundled claim must equal shard K's reconstructed claim). + - no `--shard`, no proof: off-circuit coverage verdict (disjoint cover). + - no `--shard` + proofs: composed verdict — coverage, every proof bound to a + shard, and every shard covered by a valid proof. -/ +def verifyShardComposition (ixePath manifestPath : String) (shardK? : Option Nat) + (proofs : List String) : IO UInt32 := do + let (ixonEnv, shards) ← match (← Ix.Cli.CheckCmd.loadEnvAndShards manifestPath ixePath) with + | .error e => IO.eprintln e; return 1 + | .ok r => pure r + let digestOf (k : Nat) : IO (Option Address) := do + match shards[k]? with + | none => IO.eprintln s!"shard {k} out of range ({shards.size} shards)"; pure none + | some blocks => match Ix.Cli.CheckCmd.shardClaimDigest ixonEnv blocks with + | .error e => IO.eprintln s!"reconstruct shard {k} claim failed: {e}"; pure none + | .ok d => pure (some d) + let claimDigestOfProof (hex : String) : IO (Address × Address) := do + let proofAddr ← addrOfHex! "proof" hex + let wrapper ← IO.ofExcept (Ixon.Proof.de (← StoreIO.toIO (Store.read proofAddr))) + pure (proofAddr, Address.blake3 (Ix.Claim.ser wrapper.claim)) + match shardK? with + | some k => + let some expected ← digestOf k | return 1 + if proofs.isEmpty then + IO.println s!"shard {k} CheckEnv claim digest: {expected}" + return 0 + let (aiurSystem, compiled) ← match (← buildBackend) with + | .error e => IO.eprintln e; return 1 + | .ok b => pure b + let mut rc : UInt32 := 0 + for hex in proofs do + let (proofAddr, d) ← claimDigestOfProof hex + if d != expected then + IO.eprintln s!"[verify] FAIL: proof {proofAddr} (claim {d}) is not shard {k} (claim {expected})" + rc := 1 + else if (← verifyOneProof aiurSystem compiled proofAddr) != 0 then rc := 1 + return rc + | none => + if !(← Ix.Cli.CheckCmd.shardsCover ixonEnv shards) then return 1 + if proofs.isEmpty then return 0 + let mut digestToShard : Std.HashMap Address Nat := {} + for k in [0:shards.size] do + let some d ← digestOf k | return 1 + digestToShard := digestToShard.insert d k + let (aiurSystem, compiled) ← match (← buildBackend) with + | .error e => IO.eprintln e; return 1 + | .ok b => pure b + let mut covered : Std.HashSet Nat := {} + let mut rc : UInt32 := 0 + for hex in proofs do + let (proofAddr, d) ← claimDigestOfProof hex + match digestToShard.get? d with + | none => IO.eprintln s!"[verify] FAIL: proof {proofAddr} (claim {d}) matches no shard"; rc := 1 + | some k => + if (← verifyOneProof aiurSystem compiled proofAddr) != 0 then rc := 1 + else covered := covered.insert k + let missing := (List.range shards.size).filter (fun k => !covered.contains k) + if !missing.isEmpty then + IO.eprintln s!"[verify] FAIL: shards lacking a valid proof: {missing}" + rc := 1 + if rc == 0 then + IO.println s!"[verify] OK: composed verdict — all {shards.size} shards proven + disjoint cover" + return rc + +def runVerifyCmd (p : Cli.Parsed) : IO UInt32 := do + let proofs := (p.variableArgsAs! String).toList + match (p.flag? "ixe").map (·.as! String), (p.flag? "ixes").map (·.as! String) with + | some ixe, some manifest => + verifyShardComposition ixe manifest ((p.flag? "shard").map (·.as! Nat)) proofs + | _, _ => + if proofs.isEmpty then + p.printError "error: must specify ... (or --ixe + --ixes for a shard partition)" + return 1 + let (aiurSystem, compiled) ← match (← buildBackend) with + | .error e => IO.eprintln e; return 1 + | .ok b => pure b + let mut rc : UInt32 := 0 + for hex in proofs do + let proofAddr ← addrOfHex! "proof" hex + if (← verifyOneProof aiurSystem compiled proofAddr) != 0 then rc := 1 + return rc + end Ix.Cli.VerifyCmd open Ix.Cli.VerifyCmd in def verifyCmd : Cli.Cmd := `[Cli| verify VIA runVerifyCmd; - "Verify a STARK proof against its bundled claim" + "Verify STARK proof(s) against their bundled claims, or a `.ixes` shard partition" + + FLAGS: + "ixe" : String; "Path to a serialized `.ixe` env (with --ixes). With no proof args and no --shard: verify the partition off-circuit (every constant owned by exactly one shard)." + "ixes" : String; "Path to a `.ixes` shard manifest (with --ixe)." + "shard" : Nat; "0-based shard index K (with --ixe + --ixes). No proof: print shard K's reconstructed CheckEnv claim digest. With proof(s): bind each to shard K and verify." ARGS: - proof : String; "32-byte hex address of the persisted `Ixon.Proof` wrapper in `~/.ix/store/`." + ...proofs : String; "32-byte hex address(es) of persisted `Ixon.Proof` wrappers in `~/.ix/store/`. Omit when using --ixe + --ixes." ] end diff --git a/Ix/IxVM/ClaimHarness.lean b/Ix/IxVM/ClaimHarness.lean index 30afdadd..d3d92d10 100644 --- a/Ix/IxVM/ClaimHarness.lean +++ b/Ix/IxVM/ClaimHarness.lean @@ -242,6 +242,48 @@ def buildClaimWitness (env : Ixon.Env) (claim : Ix.Claim) return { funcName := `verify_claim input := digestKey, inputIOBuffer := ioBuffer } +/-- Reconstruct a shard's `CheckEnv` claim, its reference closure, and the + assumption trees (env-root + optional frontier) — everything **except** the + IO buffer. Deterministic in `owned` (canonical trees sort addresses), so the + claim digest reproduces exactly what `prove`d — used to bind a proof to a + shard during verification, cheaply (no buffer serialization). -/ +def shardCheckEnvClaim (env : Ixon.Env) (owned : Array Address) : + Except String (Ix.Claim × Std.HashSet Address × Std.HashMap Address Ix.AssumptionTree) := do + let ownedSet : Std.HashSet Address := owned.foldl (·.insert ·) {} + let closure : Std.HashSet Address := Id.run do + let mut s : Std.HashSet Address := {} + for a in owned do + for x in (closureFrom env a).toArray do + s := s.insert x + return s + let frontier : Array Address := + closure.toArray.filter (fun a => !ownedSet.contains a) + let some envTree := Ix.AssumptionTree.canonical closure.toArray + | .error "shardCheckEnvClaim: empty shard closure" + let asmTree? := Ix.AssumptionTree.canonical frontier + let claim := Ix.Claim.checkEnv envTree.root (asmTree?.map (·.root)) + let mut trees : Std.HashMap Address Ix.AssumptionTree := + ({} : Std.HashMap Address Ix.AssumptionTree).insert envTree.root envTree + match asmTree? with + | some asmTree => trees := trees.insert asmTree.root asmTree + | none => pure () + pure (claim, closure, trees) + +def buildShardCheckEnvWitness (env : Ixon.Env) (owned : Array Address) : + Except String (Ix.Claim × ClaimWitness) := do + let (claim, closure, trees) ← shardCheckEnvClaim env owned + let claimBytes := Ix.Claim.ser claim + let digestKey := addrKey (Address.blake3 claimBytes) + let mut ioBuffer : Aiur.IOBuffer := default + ioBuffer := ioBuffer.extend 0 digestKey (claimBytes.data.map .ofUInt8) + -- Ship only the shard closure (consts + blobs + Defn hints). + ioBuffer := addEntries env closure.contains ioBuffer + -- Seed the env-root and (when present) frontier assumption trees. + for (root, _) in trees do + ioBuffer ← seedTreeAt root trees ioBuffer + return (claim, { funcName := `verify_claim + input := digestKey, inputIOBuffer := ioBuffer }) + /-- Canonical merkle tree over every const address in `env`. Returns `none` for an empty env. Convenience for callers that want to issue a `CheckEnv` claim against the env's canonical merkle root. -/ diff --git a/Tests/Ix/Kernel/ArenaExclude.lean b/Tests/Ix/Kernel/ArenaExclude.lean index 5abdab1a..634ece97 100644 --- a/Tests/Ix/Kernel/ArenaExclude.lean +++ b/Tests/Ix/Kernel/ArenaExclude.lean @@ -11,6 +11,10 @@ Output: one fully-qualified Lean name per line, suitable for feeding to `ix compile --exclude-file`. + + With `--out ` the list is written to that file (one name per line, + trailing newline) instead of stdout, so callers don't need a shell + redirect. The build log on stderr stays out of the way either way. -/ import Ix.Meta import Tests.Ix.Kernel.TutorialMeta @@ -19,7 +23,16 @@ import Tests.Ix.Kernel.Arena open Tests.Ix.Kernel.TutorialMeta open Tests.Ix.Kernel.Arena (knownIncompatible) -def main : IO UInt32 := do +/-- Parse `--out ` / `--out=` from the arg list. Last one wins. -/ +private def outPath? : List String → Option String + | [] => none + | "--out" :: path :: rest => (outPath? rest).orElse (fun _ => some path) + | arg :: rest => + if arg.startsWith "--out=" then + (outPath? rest).orElse (fun _ => some (arg.drop "--out=".length).toString) + else outPath? rest + +def main (args : List String) : IO UInt32 := do let env ← get_env! let mut excludes : Std.HashSet Lean.Name := knownIncompatible.foldl (init := {}) (fun s (n, _) => s.insert n) @@ -30,6 +43,12 @@ def main : IO UInt32 := do for n in tc.decls do excludes := excludes.insert n let sorted := excludes.toArray.qsort (fun a b => toString a < toString b) - for n in sorted do - IO.println (toString n) + match outPath? args with + | some path => + let body := String.intercalate "\n" (sorted.map toString).toList + IO.FS.writeFile path (body ++ "\n") + IO.eprintln s!"[arena-exclude] wrote {sorted.size} excluded names to {path}" + | none => + for n in sorted do + IO.println (toString n) pure 0