diff --git a/Benchmarks/AggregatePair.lean b/Benchmarks/AggregatePair.lean new file mode 100644 index 000000000..81e451c9d --- /dev/null +++ b/Benchmarks/AggregatePair.lean @@ -0,0 +1,696 @@ +import Ix.Cli.AggregateCmd +import Ix.Cli.NameResolve +import Ix.TracingTexray +import Ix.Benchmark.Bench + +/-! +# Two-shard end-to-end production aggregation benchmark + +This is deliberately a benchmark executable rather than a production CLI +mode. It can select two shards from a validated `.ixes` manifest and benchmark +the complete proof path: + +``` +shard A -> IxVM proof A -> recursive lift A ---+ + +-> structural/flat join -> verify +shard B -> IxVM proof B -> recursive lift B ---+ +``` + +Unlike `ix aggregate`, the result is allowed to retain assumptions and need +not cover the whole environment. It therefore cannot be mistaken for a closed +full-environment aggregate. + +With no arguments it reads `init.ixe` and treats the `False` and `True` block +groups as two conditional micro-shards. They exercise the real Init environment +and production proof stack without inheriting the memory footprint of a full +RAM-planned shard. `--ixes` switches to a complete manifest and automatically +chooses its smallest direct sibling pair. Supplying `--shard-a` and `--shard-b` +instead selects any two nonempty shards from that manifest; they need not be +siblings: + +``` +lake exe bench-aggregate-pair -- \ + --ixe /path/init.ixe --name-a False --name-b True \ + --json /tmp/init-pair.json --texray + +lake exe bench-aggregate-pair -- \ + --ixe /path/init.ixe --ixes /path/init.ixes \ + --shard-a 3 --shard-b 17 --json /tmp/init-real-pair.json +``` + +`--proof-a` and `--proof-b` may be supplied together to reuse persisted base +proofs. They are an explicit warm-start mode; the default always measures base +proving as well as recursive aggregation. + +Every stage is the real production proof call, with no execution-only preflight +or memory gate. Like `bench-typecheck --recursive`, the default benchmark +profile uses 50 FRI queries and zero query PoW for both base and recursive +proofs; `--queries` can override the count. Timings and measured peak RSS are +recorded after the fact. +-/ + +open Lean (Json) + +namespace Benchmarks.AggregatePair + +open Ix +open Ix.Cli.AggregateCmd + +abbrev AggregationTree := Ix.Cli.CheckCmd.AggregationTree +abbrev FoldOp := Ix.Cli.CheckCmd.AggregationTree.FoldOp + +/-- Keep this in lockstep with `Benchmarks.Typecheck.recursiveFriParameters`. +The benchmark measures the full recursive architecture under the repository's +established tractable recursion profile, not the 100-query production policy. -/ +def benchmarkFriParameters (queries : Nat) : Aiur.FriParameters := { + logFinalPolyLen := 0 + maxLogArity := 1 + numQueries := queries + commitProofOfWorkBits := 0 + queryProofOfWorkBits := 0 +} + +def argStr (args : List String) (flag : String) : Option String := + match args.dropWhile (· != flag) with + | _ :: value :: _ => some value + | _ => none + +def argNat? (args : List String) (flag : String) : Option Nat := + (argStr args flag).bind (·.toNat?) + +def hasFlag (args : List String) (flag : String) : Bool := + args.contains flag + +def jsonRound (digits : Nat) (value : Float) : Json := + let scale := (10.0 : Float) ^ digits.toFloat + let scaled := value * scale + let mantissa : _root_.Int := + if scaled < 0 then -_root_.Int.ofNat (-scaled).round.toUInt64.toNat + else _root_.Int.ofNat scaled.round.toUInt64.toNat + Json.num ⟨mantissa, digits⟩ + +def timed (action : Unit → α) : IO (α × Float) := do + let started ← IO.monoNanosNow + let result ← blackBoxIO action () + let elapsed ← IO.monoNanosNow + pure (result, (elapsed - started).toFloat / 1e9) + +def stageJson (fields : List (String × Json)) : Json := + Json.mkObj (("status", Json.str "ok") :: fields) + +def errorJson (message : String) : Json := + Json.mkObj [("status", Json.str "error"), ("message", Json.str message)] + +def writeReport (path? : Option String) (metadata : List (String × Json)) + (status : String) (stages : Array (String × Json)) : IO Unit := do + if let some path := path? then + let report := Json.mkObj (metadata ++ + [("status", Json.str status), ("stages", Json.mkObj stages.toList)]) + IO.FS.writeFile path (report.pretty ++ "\n") + +def compileToplevel (label : String) + (source : Except Aiur.Global Aiur.Source.Toplevel) : + IO (Except String Aiur.CompiledToplevel) := do + match source with + | .error error => pure (.error s!"{label} toplevel merge failed: {error}") + | .ok top => match top.compile with + | .error error => pure (.error s!"{label} compilation failed: {error}") + | .ok compiled => pure (.ok compiled) + +def prepareShard (env : Ixon.Env) (blocks : Array Address) : + Except String PreparedShard := do + let owned := Ix.Cli.CheckCmd.ownedConstsForBlocks env blocks + let (claim, trees) ← IxVM.ClaimHarness.shardCheckEnvClaimTrees env owned + let statement ← MultiStark.CheckEnvTrees.ofClaim claim trees + pure { claim, statement } + +def blockOfAddress (env : Ixon.Env) (address : Address) : Except String Address := do + let some constant := env.getConst? address + | throw s!"constant {address} is absent or malformed" + pure <| match constant.info with + | .iPrj projection => projection.block + | .cPrj projection => projection.block + | .rPrj projection => projection.block + | .dPrj projection => projection.block + | _ => address + +def namedMicroShard (env : Ixon.Env) (name : String) : + Except String (Array Address) := do + let some address := Ix.Cli.NameResolve.resolveIxeAddr env name + | throw s!"Init micro-shard name not found: {name}" + pure #[← blockOfAddress env address] + +partial def siblingLeafPairs (tree : AggregationTree) : Array (Nat × Nat) := + match tree with + | .leaf _ => #[] + | .node left right => + let here := match left, right with + | .leaf l, .leaf r => #[(l, r)] + | _, _ => #[] + here ++ siblingLeafPairs left ++ siblingLeafPairs right + +/-- The smallest direct sibling pair by combined subject count. The manifest +tree and count array have already passed coverage/pruning validation. -/ +def smallestSiblingPair? (tree : AggregationTree) (counts : Array Nat) : + Option (Nat × Nat) := + (siblingLeafPairs tree).foldl (init := none) fun best pair => + match best with + | none => some pair + | some current => + let pairCount := counts[pair.1]! + counts[pair.2]! + let currentCount := counts[current.1]! + counts[current.2]! + if pairCount < currentCount then some pair else some current + +def loadProofWrapper (label proofAddress : String) : IO (Except String Ixon.Proof) := do + let some address := Address.fromString proofAddress + | return .error s!"{label}: expected a 64-character store address" + try + match Ixon.Proof.de (← StoreIO.toIO (Store.read address)) with + | .error error => pure (.error s!"{label}: wrapper decode failed: {error}") + | .ok wrapper => pure (.ok wrapper) + catch error => + pure (.error s!"{label}: store read failed: {error}") + +structure BenchSlot where + slot : AggregateSlot + proveSeconds : Float + +structure BaseProofBench where + wrapper : Ixon.Proof + proveSeconds : Float + +/-- Generate one ordinary shard proof through the same native EnvHandle path as +`ix prove --ixe E --ixes M --shard K`, but retain it in memory for the lift. -/ +def runBaseProof (label : String) (envHandle : Aiur.EnvHandle) + (owned : Array Address) (expectedClaim : Ix.Claim) + (ixvmSystem : Aiur.AiurSystem) (verifyIdx : Aiur.Bytecode.FunIdx) + (record : String → Json → IO Unit) : IO (Except String BaseProofBench) := do + let ownedBlob := owned.foldl (fun bytes address => bytes ++ address.hash) + ByteArray.empty + IO.println s!"[pair-bench] proving {label}" + (← IO.getStdout).flush + TracingTexray.resetPeakTreeRss + let (proved, proveSeconds) ← timed fun _ => + ixvmSystem.shardProveWithEnv verifyIdx envHandle ownedBlob + let provePeak ← TracingTexray.peakTreeRssBytes + let (claimBytes, proof) ← match proved with + | .error error => + record s!"{label}-prove" (errorJson error) + return .error s!"{label}: shardProveWithEnv failed: {error}" + | .ok (claimBytes, proof, _) => pure (claimBytes, proof) + let claim ← match Ixon.runGet Ix.Claim.get claimBytes with + | .error error => + record s!"{label}-prove" (errorJson s!"claim decode failed: {error}") + return .error s!"{label}: claim decode failed: {error}" + | .ok claim => pure claim + if claim != expectedClaim then + let error := "native shard prover returned a different CheckEnv claim" + record s!"{label}-prove" (errorJson error) + return .error s!"{label}: {error}" + let proofBytes := proof.toBytes + record s!"{label}-prove" (stageJson + [("seconds", jsonRound 6 proveSeconds), + ("peak-rss-bytes", Lean.toJson provePeak), + ("proof-bytes", Lean.toJson proofBytes.size), + ("source", Json.str "generated")]) + pure (.ok { + wrapper := { claim, proof := proofBytes } + proveSeconds + }) + +def reuseBaseProof (label address : String) (expectedClaim : Ix.Claim) + (record : String → Json → IO Unit) : IO (Except String BaseProofBench) := do + let wrapper ← match ← loadProofWrapper label address with + | .error error => return .error error + | .ok wrapper => pure wrapper + if wrapper.claim != expectedClaim then + return .error s!"{label}: persisted wrapper claim does not match the selected shard" + record s!"{label}-prove" (stageJson + [("seconds", jsonRound 6 0), + ("peak-rss-bytes", Lean.toJson (0 : Nat)), + ("proof-bytes", Lean.toJson wrapper.proof.size), + ("source", Json.str "reused")]) + pure (.ok { wrapper, proveSeconds := 0 }) + +def runLift (label : String) (prepared : PreparedShard) (wrapper : Ixon.Proof) + (spec : AggregateSlotSpec) (ixvmSystem recursionSystem : Aiur.AiurSystem) + (verifyIdx liftIdx : Aiur.Bytecode.FunIdx) (ixvmVk : ByteArray) + (record : String → Json → IO Unit) : + IO (Except String BenchSlot) := do + if wrapper.claim != prepared.claim then + return .error s!"{label}: bundled CheckEnv claim does not match the selected shard" + let innerProof ← match Aiur.Proof.ofBytesChecked wrapper.proof with + | .error error => return .error s!"{label}: inner proof decode failed: {error}" + | .ok proof => pure proof + let claimBytes := Ix.Claim.ser prepared.claim + let verifyInput := IxVM.ClaimHarness.packedDigestKey (Address.blake3 claimBytes) + let innerClaim := Aiur.buildClaim verifyIdx verifyInput #[] + + TracingTexray.resetPeakTreeRss + let (innerVerified, innerVerifySeconds) ← timed fun _ => + ixvmSystem.verify innerClaim innerProof + let innerVerifyPeak ← TracingTexray.peakTreeRssBytes + match innerVerified with + | .error error => + record s!"{label}-inner-verify" (errorJson error) + return .error s!"{label}: inner proof verification failed: {error}" + | .ok () => + record s!"{label}-inner-verify" (stageJson + [("seconds", jsonRound 6 innerVerifySeconds), + ("peak-rss-bytes", Lean.toJson innerVerifyPeak), + ("proof-bytes", Lean.toJson wrapper.proof.size)]) + + let innerClaimsBytes := MultiStark.serializeClaims #[innerClaim] + let pubInput := MultiStark.verifierPubInput ixvmVk innerClaimsBytes + IO.println s!"[pair-bench] proving {label}" + (← IO.getStdout).flush + TracingTexray.resetPeakTreeRss + let ((outerClaim, proof), proveSeconds) ← timed fun _ => + recursionSystem.proveMultiStark liftIdx pubInput wrapper.proof ixvmVk innerClaimsBytes + let provePeak ← TracingTexray.peakTreeRssBytes + if outerClaim != spec.outerClaim then + let error := "produced an unexpected outer claim" + record s!"{label}-prove" (errorJson error) + return .error s!"{label}: {error}" + let proofBytes := proof.toBytes + record s!"{label}-prove" (stageJson + [("seconds", jsonRound 6 proveSeconds), + ("peak-rss-bytes", Lean.toJson provePeak), + ("proof-bytes", Lean.toJson proofBytes.size)]) + + TracingTexray.resetPeakTreeRss + let (verified, verifySeconds) ← timed fun _ => + recursionSystem.verify outerClaim proof + let verifyPeak ← TracingTexray.peakTreeRssBytes + match verified with + | .error error => + record s!"{label}-outer-verify" (errorJson error) + return .error s!"{label}: lift proof verification failed: {error}" + | .ok () => + record s!"{label}-outer-verify" (stageJson + [("seconds", jsonRound 6 verifySeconds), + ("peak-rss-bytes", Lean.toJson verifyPeak)]) + + pure (.ok { + slot := { + statement := spec.statement + subjectCount := spec.subjectCount + outerClaim + proof + proofAddress? := none + openPreimages := #[innerClaimsBytes, claimBytes] + } + proveSeconds + }) + +def runJoin (item : ScheduledFold) (left right : AggregateSlot) + (spec : AggregateSlotSpec) (recursionSystem : Aiur.AiurSystem) + (joinIdx structuralJoinIdx : Aiur.Bytecode.FunIdx) + (recursionVk allowed : ByteArray) + (record : String → Json → IO Unit) : IO (Except String BenchSlot) := do + let output := spec.statement + let outputClaimBytes := Ix.Claim.ser output.claim + let pubInput := MultiStark.joinPubInput allowed outputClaimBytes + let leftClaimsBytes := MultiStark.serializeClaims #[left.outerClaim] + let rightClaimsBytes := MultiStark.serializeClaims #[right.outerClaim] + let preimagesBlob := MultiStark.joinPreimagesBlob + (left.openPreimages ++ right.openPreimages) + let trees := if item.structural then + MultiStark.CheckEnvTrees.structuralAdviceTrees left.statement right.statement output + else + MultiStark.CheckEnvTrees.adviceTrees left.statement right.statement output + let treesBlob := MultiStark.joinTreesBlob trees + let pathsBlob := if item.structural then + MultiStark.joinPathsBlob + (MultiStark.CheckEnvTrees.structuralPathAdvice left.statement right.statement output) + else MultiStark.joinPathsBlob #[] + let joinFunIdx := if item.structural then structuralJoinIdx else joinIdx + let label := if item.structural then "structural-join" else "flat-join" + + IO.println s!"[pair-bench] proving {label}" + (← IO.getStdout).flush + TracingTexray.resetPeakTreeRss + let (proved, proveSeconds) ← timed fun _ => + recursionSystem.proveMultiStarkJoin joinFunIdx pubInput + left.proof.toBytes right.proof.toBytes recursionVk + leftClaimsBytes rightClaimsBytes outputClaimBytes allowed + preimagesBlob treesBlob pathsBlob + let provePeak ← TracingTexray.peakTreeRssBytes + let (outerClaim, proof) ← match proved with + | .error error => + record s!"{label}-prove" (errorJson error) + return .error s!"{label}: prove failed: {error}" + | .ok result => pure result + if outerClaim != spec.outerClaim then + let error := "produced an unexpected outer claim" + record s!"{label}-prove" (errorJson error) + return .error s!"{label}: {error}" + let proofBytes := proof.toBytes + record s!"{label}-prove" (stageJson + [("seconds", jsonRound 6 proveSeconds), + ("peak-rss-bytes", Lean.toJson provePeak), + ("proof-bytes", Lean.toJson proofBytes.size)]) + + TracingTexray.resetPeakTreeRss + let (verified, verifySeconds) ← timed fun _ => + recursionSystem.verify outerClaim proof + let verifyPeak ← TracingTexray.peakTreeRssBytes + match verified with + | .error error => + record s!"{label}-verify" (errorJson error) + return .error s!"{label}: proof verification failed: {error}" + | .ok () => + record s!"{label}-verify" (stageJson + [("seconds", jsonRound 6 verifySeconds), + ("peak-rss-bytes", Lean.toJson verifyPeak)]) + + pure (.ok { + slot := { + statement := output + subjectCount := spec.subjectCount + outerClaim + proof + proofAddress? := none + openPreimages := #[outputClaimBytes] + } + proveSeconds + }) + +structure PairSelection where + leftBlocks : Array Address + rightBlocks : Array Address + leftId : Nat + rightId : Nat + leftLabel : String + rightLabel : String + expectedLeftSubjects? : Option Nat := none + expectedRightSubjects? : Option Nat := none + source : String + manifestPath? : Option String := none + +def usage : String := + "usage: bench-aggregate-pair [--ixe E] [--name-a A --name-b B] " ++ + "[--ixes M --shard-a A --shard-b B] " ++ + "[--proof-a ADDR --proof-b ADDR] " ++ + "[--queries N] [--structural-above N] [--json PATH] " ++ + "[--plan-only] [--texray]" + +def main (args : List String) : IO UInt32 := do + let ixePath := (argStr args "--ixe").getD "init.ixe" + let manifestPath? := argStr args "--ixes" + let requestedA? := argNat? args "--shard-a" + let requestedB? := argNat? args "--shard-b" + if requestedA?.isSome != requestedB?.isSome then + IO.eprintln "error: --shard-a and --shard-b must be supplied together" + IO.eprintln usage + return 2 + if let some requestedA := requestedA? then + if requestedB? == some requestedA then + IO.eprintln "error: --shard-a and --shard-b must differ" + return 2 + if manifestPath?.isNone && requestedA?.isSome then + IO.eprintln "error: --shard-a/--shard-b require --ixes" + return 2 + if manifestPath?.isSome && + ((argStr args "--name-a").isSome || (argStr args "--name-b").isSome) then + IO.eprintln "error: --name-a/--name-b select micro-shards and cannot accompany --ixes" + return 2 + let proofAHex? := argStr args "--proof-a" + let proofBHex? := argStr args "--proof-b" + if proofAHex?.isSome != proofBHex?.isSome then + IO.eprintln "error: --proof-a and --proof-b must be supplied together" + IO.eprintln usage + return 2 + let structuralAbove := (argNat? args "--structural-above").getD defaultStructuralAbove + let queries := (argNat? args "--queries").getD 50 + if queries == 0 then + IO.eprintln "error: --queries must be positive" + return 2 + let jsonPath? := argStr args "--json" + + TracingTexray.startSampler 25 + if hasFlag args "--texray" then TracingTexray.init {} + + let env ← match Ixon.deEnvAnon (← IO.FS.readBinFile ixePath) with + | .error error => IO.eprintln s!"deserialize {ixePath} failed: {error}"; return 1 + | .ok env => pure env + let selection : PairSelection ← match manifestPath? with + | none => + let nameA := (argStr args "--name-a").getD "False" + let nameB := (argStr args "--name-b").getD "True" + let leftBlocks ← match namedMicroShard env nameA with + | .error error => IO.eprintln error; return 1 + | .ok blocks => pure blocks + let rightBlocks ← match namedMicroShard env nameB with + | .error error => IO.eprintln error; return 1 + | .ok blocks => pure blocks + if leftBlocks == rightBlocks then + IO.eprintln s!"micro-shard names {nameA} and {nameB} resolve to the same block" + return 1 + pure { + leftBlocks, rightBlocks, leftId := 0, rightId := 1 + leftLabel := nameA, rightLabel := nameB + source := "init-named-microshards" + } + | some manifestPath => + let rawView ← match Ix.Cli.CheckCmd.parseIxesManifest + (← IO.FS.readBinFile manifestPath) with + | .error error => IO.eprintln s!"manifest parse failed: {error}"; return 1 + | .ok view => pure view + if !(← Ix.Cli.CheckCmd.shardsCover env rawView.shards) then return 1 + let (view, shardCounts) ← match rawView.pruneEmpty env with + | .error error => IO.eprintln error; return 1 + | .ok result => pure result + let (leftDense, rightDense) ← match requestedA?, requestedB? with + | none, none => match smallestSiblingPair? view.aggregationTree shardCounts with + | some pair => pure pair + | none => + IO.eprintln "manifest has no direct sibling leaf pair" + return 1 + | some requestedA, some requestedB => + let some denseA := view.shardIds.findIdx? (· == requestedA) + | IO.eprintln s!"manifest has no retained shard {requestedA}"; return 1 + let some denseB := view.shardIds.findIdx? (· == requestedB) + | IO.eprintln s!"manifest has no retained shard {requestedB}"; return 1 + pure (denseA, denseB) + | _, _ => + IO.eprintln "internal: partial shard override passed validation" + return 1 + let leftOriginal := view.shardIds[leftDense]! + let rightOriginal := view.shardIds[rightDense]! + pure { + leftBlocks := view.shards[leftDense]! + rightBlocks := view.shards[rightDense]! + leftId := leftOriginal + rightId := rightOriginal + leftLabel := s!"shard {leftOriginal}" + rightLabel := s!"shard {rightOriginal}" + expectedLeftSubjects? := some shardCounts[leftDense]! + expectedRightSubjects? := some shardCounts[rightDense]! + source := if requestedA?.isSome then "explicit-manifest-pair" + else "smallest-manifest-siblings" + manifestPath? := some manifestPath + } + let leftProofHex? := proofAHex? + let rightProofHex? := proofBHex? + let leftBlocks := selection.leftBlocks + let rightBlocks := selection.rightBlocks + let leftPrepared ← match prepareShard env leftBlocks with + | .error error => IO.eprintln s!"prepare {selection.leftLabel}: {error}"; return 1 + | .ok prepared => pure prepared + let rightPrepared ← match prepareShard env rightBlocks with + | .error error => IO.eprintln s!"prepare {selection.rightLabel}: {error}"; return 1 + | .ok prepared => pure prepared + if selection.expectedLeftSubjects?.any + (· != leftPrepared.statement.subjectCount) || + selection.expectedRightSubjects?.any + (· != rightPrepared.statement.subjectCount) then + IO.eprintln "internal: reconstructed subject counts differ from the manifest view" + return 1 + + let compactOps : Array FoldOp := #[.leaf 0, .leaf 1, .join 0 1] + let plan ← match schedulePlan compactOps + #[leftPrepared.statement.subjectCount, rightPrepared.statement.subjectCount] + structuralAbove with + | .error error => IO.eprintln error; return 1 + | .ok plan => pure plan + let some joinItem := plan[2]? + | IO.eprintln "internal: compact pair plan has no join slot"; return 1 + let mode := if joinItem.structural then "structural" else "flat" + let baseProofSource := if proofAHex?.isSome then "reused" else "generated" + IO.println (s!"[pair-bench] {selection.leftLabel}, {selection.rightLabel}: " ++ + s!"{leftPrepared.statement.subjectCount} + {rightPrepared.statement.subjectCount} " ++ + s!"subjects; {mode} join (threshold > {structuralAbove}); " ++ + s!"{baseProofSource} base proofs") + if hasFlag args "--plan-only" then return 0 + + let metadata : List (String × Json) := + [("schema-version", Lean.toJson (2 : Nat)), + ("ixe", Json.str ixePath), + ("ixes", selection.manifestPath?.map Json.str |>.getD Json.null), + ("left-shard", Lean.toJson selection.leftId), + ("right-shard", Lean.toJson selection.rightId), + ("left-label", Json.str selection.leftLabel), + ("right-label", Json.str selection.rightLabel), + ("left-subjects", Lean.toJson leftPrepared.statement.subjectCount), + ("right-subjects", Lean.toJson rightPrepared.statement.subjectCount), + ("pair-source", Json.str selection.source), + ("base-proof-source", Json.str baseProofSource), + ("queries", Lean.toJson queries), + ("join-mode", Json.str mode), + ("structural-above", Lean.toJson structuralAbove)] + let stagesRef ← IO.mkRef (#[] : Array (String × Json)) + let record (name : String) (row : Json) : IO Unit := do + let stages := (← stagesRef.get).push (name, row) + stagesRef.set stages + writeReport jsonPath? metadata "running" stages + IO.println s!"[pair-bench] recorded {name}" + writeReport jsonPath? metadata "running" #[] + + IO.println "[pair-bench] compiling IxVM and MultiStark systems" + let ixvmCompiled ← match ← compileToplevel "IxVM" IxVM.ixVM with + | .error error => IO.eprintln error; return 1 + | .ok compiled => pure compiled + let recursionCompiled ← match ← compileToplevel "MultiStark recursion" + MultiStark.multiStark with + | .error error => IO.eprintln error; return 1 + | .ok compiled => pure compiled + let verifyIdx := ixvmCompiled.getFuncIdx `verify_claim |>.get! + let liftIdx := recursionCompiled.getFuncIdx `verify_multi_stark_proof |>.get! + let joinIdx := recursionCompiled.getFuncIdx `join_two |>.get! + let structuralJoinIdx := recursionCompiled.getFuncIdx `join_two_structural |>.get! + let friParameters := benchmarkFriParameters queries + let recursionParameters : MultiStark.RecursionParameters := { + commitment := Aiur.defaultCommitmentParameters + fri := friParameters + } + let ixvmSystem := Aiur.AiurSystem.build ixvmCompiled.bytecode + Aiur.defaultCommitmentParameters friParameters + let recursionSystem := MultiStark.buildRecursionSystem recursionCompiled.bytecode + recursionParameters + let envHandle ← match Aiur.EnvHandle.fromIxe ixePath with + | .error error => IO.eprintln s!"EnvHandle.fromIxe {ixePath}: {error}"; return 1 + | .ok handle => pure handle + let ixvmVk := ixvmSystem.vkBytes + let recursionVk := recursionSystem.vkBytes + let allowed := MultiStark.allowedBlob ixvmVk verifyIdx recursionVk liftIdx + joinIdx structuralJoinIdx + let specs ← match buildAggregateSlotSpecs plan #[leftPrepared, rightPrepared] + ixvmVk recursionVk allowed verifyIdx liftIdx joinIdx structuralJoinIdx + recursionParameters with + | .error error => IO.eprintln s!"prepare pair slots: {error}"; return 1 + | .ok specs => pure specs + let some leftSpec := specs[0]? + | IO.eprintln "internal: pair specs have no left lift"; return 1 + let some rightSpec := specs[1]? + | IO.eprintln "internal: pair specs have no right lift"; return 1 + let some rootSpec := specs[2]? + | IO.eprintln "internal: pair specs have no join"; return 1 + + let leftBase ← match leftProofHex? with + | some proofHex => + match ← reuseBaseProof "base-left" proofHex leftPrepared.claim record with + | .error error => + IO.eprintln error + writeReport jsonPath? metadata "error" (← stagesRef.get) + return 1 + | .ok result => pure result + | none => + let owned := Ix.Cli.CheckCmd.ownedConstsForBlocks env leftBlocks + match ← runBaseProof "base-left" envHandle owned leftPrepared.claim + ixvmSystem verifyIdx record with + | .error error => + IO.eprintln error + writeReport jsonPath? metadata "error" (← stagesRef.get) + return 1 + | .ok result => pure result + let rightBase ← match rightProofHex? with + | some proofHex => + match ← reuseBaseProof "base-right" proofHex rightPrepared.claim record with + | .error error => + IO.eprintln error + writeReport jsonPath? metadata "error" (← stagesRef.get) + return 1 + | .ok result => pure result + | none => + let owned := Ix.Cli.CheckCmd.ownedConstsForBlocks env rightBlocks + match ← runBaseProof "base-right" envHandle owned rightPrepared.claim + ixvmSystem verifyIdx record with + | .error error => + IO.eprintln error + writeReport jsonPath? metadata "error" (← stagesRef.get) + return 1 + | .ok result => pure result + + let left ← match ← runLift "lift-left" leftPrepared leftBase.wrapper leftSpec + ixvmSystem recursionSystem verifyIdx liftIdx ixvmVk record with + | .error error => + IO.eprintln error + writeReport jsonPath? metadata "error" (← stagesRef.get) + return 1 + | .ok slot => pure slot + let right ← match ← runLift "lift-right" rightPrepared rightBase.wrapper rightSpec + ixvmSystem recursionSystem verifyIdx liftIdx ixvmVk record with + | .error error => + IO.eprintln error + writeReport jsonPath? metadata "error" (← stagesRef.get) + return 1 + | .ok slot => pure slot + let root ← match ← runJoin joinItem left.slot right.slot rootSpec + recursionSystem joinIdx structuralJoinIdx recursionVk allowed record with + | .error error => + IO.eprintln error + writeReport jsonPath? metadata "error" (← stagesRef.get) + return 1 + | .ok slot => pure slot + + let expectedStatement := if joinItem.structural then + leftPrepared.statement.joinStructural rightPrepared.statement + else leftPrepared.statement.join rightPrepared.statement + if root.slot.statement.claim != expectedStatement.claim then + IO.eprintln "pair root statement differs from independent host reconstruction" + writeReport jsonPath? metadata "error" (← stagesRef.get) + return 1 + + -- Cheap negative control: the valid proof must reject under a one-word + -- mutation of its exact outer claim. + let some outerWord := root.slot.outerClaim[2]? + | IO.eprintln "internal: aggregate outer claim is shorter than three words"; return 1 + let wrongOuter := root.slot.outerClaim.set! 2 (outerWord + 1) + let (wrongResult, negativeSeconds) ← timed fun _ => + recursionSystem.verify wrongOuter root.slot.proof + match wrongResult with + | .ok () => + record "negative-control" (errorJson "proof accepted a mutated outer claim") + writeReport jsonPath? metadata "error" (← stagesRef.get) + return 1 + | .error _ => + record "negative-control" (stageJson [("seconds", jsonRound 6 negativeSeconds)]) + + let baseProveSeconds := leftBase.proveSeconds + rightBase.proveSeconds + let recursiveProveSeconds := left.proveSeconds + right.proveSeconds + root.proveSeconds + let serialProveSeconds := baseProveSeconds + recursiveProveSeconds + let parallelLowerBound := + max (leftBase.proveSeconds + left.proveSeconds) + (rightBase.proveSeconds + right.proveSeconds) + root.proveSeconds + let rootBytes := root.slot.proof.toBytes + let summary := stageJson + [("base-prove-seconds", jsonRound 6 baseProveSeconds), + ("recursive-prove-seconds", jsonRound 6 recursiveProveSeconds), + ("serial-total-prove-seconds", jsonRound 6 serialProveSeconds), + ("parallel-branch-lower-bound-seconds", jsonRound 6 parallelLowerBound), + ("root-proof-bytes", Lean.toJson rootBytes.size), + ("root-proof-digest", Json.str (toString (Address.blake3 rootBytes))), + ("subjects", Lean.toJson root.slot.subjectCount), + ("retains-assumptions", Lean.toJson root.slot.statement.assumptions.isSome)] + record "summary" summary + writeReport jsonPath? metadata "ok" (← stagesRef.get) + IO.println (s!"[pair-bench] OK: serial base proving {baseProveSeconds}s; " ++ + s!"recursive proving {recursiveProveSeconds}s; total {serialProveSeconds}s; " ++ + s!"parallel branch lower bound {parallelLowerBound}s; root {rootBytes.size} bytes") + pure 0 + +end Benchmarks.AggregatePair + +def main (args : List String) : IO UInt32 := + Benchmarks.AggregatePair.main args diff --git a/Benchmarks/Typecheck.lean b/Benchmarks/Typecheck.lean index 4bdd9e125..ca0aeed41 100644 --- a/Benchmarks/Typecheck.lean +++ b/Benchmarks/Typecheck.lean @@ -1,6 +1,7 @@ import Cli import Ix.IxVM import Ix.IxVM.Toplevel +import Ix.IxVM.ClaimHarness import Ix.Aiur.Protocol import Ix.Aiur.Compiler import Ix.Aiur.Statistics @@ -42,8 +43,9 @@ lake exe bench-typecheck --ixe --consts [--consts-file

] [ deps) instead of its whole transitive closure (verify_claim, the default). Same flag as `zisk-host --skip-deps`; reserved for targets too expensive to full-closure-check. - --json write per-constant results JSON to . Off by default: - normal CLI usage prints only the human-readable summary. + --json write results JSON to (per constant, plus one pair row + with --join). Off by default: normal CLI usage prints only + the human-readable summary. --texray enable the tracing-texray timeline + RAM breakdown. With --json , per-phase span timings are also written to .spans (JSON Lines) for the CI drill-down. Off by default. @@ -71,10 +73,19 @@ lake exe bench-typecheck --ixe --consts [--consts-file

] [ proves stream the same `stark/...` span names, so the summed `phase-stark-*` fields cover the pair. Conflicts with --execute-only. + --join with --recursive and exactly two constants, benchmark the + aggregate-first flat join after both singleton-CheckEnv + proofs have been lifted. Emits one `left + right` JSON row + carrying join-execute-time, join-fft-cost, join-prove-time, + join-peak-rss, join-proof-size, and join-verify-time. This is + an explicit W0/Section-13 diagnostic, not part of the default + per-constant CI run. ``` -For each constant the harness STARK-checks `Ix.Claim.check addr none` (the full -transitive typecheck) in two phases: +By default, the harness STARK-checks `Ix.Claim.check addr none` for each +constant (the full transitive typecheck). `--join` instead uses a singleton +`CheckEnv` shard claim for each of its two children. Work proceeds in up to +four phases: 1. **Execute** (every constant): run the bytecode out-of-circuit. Cheap and deterministic, so we always record `constants` (the number of constants the @@ -91,6 +102,11 @@ transitive typecheck) in two phases: 3. **Recursive** (`--recursive` only, right after each constant's prove): feed the fresh proof + vk + claims to `verify_multi_stark_proof`, execute it, then prove the verifier execution — the end-to-end recursion cost. +4. **Join** (`--recursive --join`, exactly two constants): use each requested + constant as a one-owned-constant `CheckEnv` shard, lift both resulting + proofs, then execute/prove/verify `join_two`. The pair gets a dedicated JSON + row because the join is one shared operation, not a cost attributable to + either child independently. When `--json` is set the file is rewritten after every prove, so an external `timeout` still leaves a complete file of the results collected so far (cheapest @@ -110,6 +126,10 @@ KZG stages land), plus the pipeline ledger `"total-time"`, `"pipeline-throughput and throughput are scoped to that stage's own prove window. Any bencher-specific reshaping is the caller's job (see `.github/workflows/bench-main.yml`). + +With `--join`, the same object also contains one `"left + right"` row. It has +`status`, the sum of the two child `constants`, and the six `join-*` measures; +it intentionally has no per-child or pipeline ledger fields. -/ open Lean (Json Name) @@ -204,6 +224,34 @@ structure Result where recursiveVerifySec : Option Float := none deriving Inhabited +/-- The successfully verified lift artifact retained for the optional binary + join phase. `innerClaimsBytes` is the serialized singleton list containing + the IxVM proof's Aiur claim; `checkEnvClaimBytes` is the nested Ix claim + preimage that the join opens below it. -/ +structure LiftArtifact where + label : String + constants : Nat + statement : MultiStark.CheckEnvTrees + innerClaimsBytes : ByteArray + checkEnvClaimBytes : ByteArray + outerClaim : Array Aiur.G + proof : Aiur.Proof + +/-- Measurements for the one pair-wide `join_two` operation. Kept separate + from `Result`: copying these fields onto both child rows would count the + same join twice, while attaching them to one child would make the result + order-dependent. -/ +structure JoinResult where + name : String + constants : Nat + fftCost : Float + executeSec : Float + proveSec : Float + peakRss : Nat + proofSize : Nat + verifySec : Option Float + failed : Bool := false + /-- A `Json` number with at most `d` decimal places, rendered decimally. `Float`'s own `ToJson` prints the full binary representation (`0.02602000000000000146…`), so build the `JsonNumber` (mantissa · @@ -216,6 +264,23 @@ def jsonRound (d : Nat) (f : Float) : Json := else Int.ofNat scaled.round.toUInt64.toNat Json.num ⟨m, d⟩ +def JoinResult.toJsonEntry (r : JoinResult) : String × Json := + if r.failed then + (r.name, Json.mkObj [("status", Json.str "rejected")]) + else + let fields : List (String × Json) := + [ ("status", Json.str "ok") + , ("constants", Lean.toJson r.constants) + , ("join-fft-cost", jsonRound 0 r.fftCost) + , ("join-execute-time", jsonRound 6 r.executeSec) + , ("join-prove-time", jsonRound 6 r.proveSec) + , ("join-peak-rss", Lean.toJson r.peakRss) + , ("join-proof-size", Lean.toJson r.proofSize) ] + let fields := match r.verifySec with + | some seconds => fields ++ [("join-verify-time", jsonRound 6 seconds)] + | none => fields + (r.name, Json.mkObj fields) + /-- Flat results object: `name → { constants, … }`. No bencher-specific shaping. @@ -342,12 +407,24 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do -- Recursive: after each constant's prove, execute AND prove the in-circuit -- multi-stark verifier over the fresh proof (Phase 3). let recursive := p.hasFlag "recursive" + -- Join: retain exactly two successful recursive lifts, then benchmark one + -- production flat join over their singleton-CheckEnv statements. + let join := p.hasFlag "join" if recursive && executeOnly then IO.eprintln "error: --recursive measures the prove path; drop --execute-only" return Ix.Benchmark.Results.exitUsage + if join && !recursive then + IO.eprintln "error: --join requires --recursive" + return Ix.Benchmark.Results.exitUsage + if join && skipDeps then + IO.eprintln "error: --join requires singleton CheckEnv shards; drop --skip-deps" + return Ix.Benchmark.Results.exitUsage -- Off by default; CI passes --texray explicitly. let useTexray := p.hasFlag "texray" let useInterp := p.hasFlag "interp" + if join && useInterp then + IO.eprintln "error: --join requires the native singleton-shard prover; drop --interp" + return Ix.Benchmark.Results.exitUsage -- Start the process-tree RSS sampler so each Result's peak-rss reflects the -- true high-water mark. With --texray, install the streaming subscriber up -- front: every phase span — aiur/execute_ixvm in Phase 1 included — @@ -419,6 +496,9 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do if targets.isEmpty then IO.eprintln "no requested constants were found in the env" return 1 + if join && targets.size != 2 then + IO.eprintln s!"error: --join requires exactly two resolved constants; got {targets.size}" + return Ix.Benchmark.Results.exitUsage -- Build the env once into a Rust-owned `EnvHandle` and share it -- across both Phase 1 and Phase 2 loops. Per-target FFI calls @@ -427,6 +507,8 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do | .error e => IO.eprintln s!"EnvHandle.fromIxe {ixePath}: {e}"; return 1 | .ok h => pure h + let singletonOwnedBlob (addr : Address) : ByteArray := addr.hash + -- Phase 1: execute every constant (cheap, deterministic structural metrics). -- For full-closure check claims, use `checkAddrWithEnv` against the -- shared `envHandle`. For `--skip-deps` (`buildVerifyConst`), the @@ -455,6 +537,9 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do compiled.bytecode.execute funIdx witness.input witness.inputIOBuffer else compiled.bytecode.executeIxVM funIdx witness.input witness.inputIOBuffer + else if join then + compiled.bytecode.shardCheckWithEnv funIdx envHandle + (singletonOwnedBlob addr) useInterp else compiled.bytecode.checkAddrWithEnv funIdx envHandle addr.hash useInterp let execPeak ← TracingTexray.peakTreeRssBytes @@ -506,6 +591,17 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do let (name, row) := Result.toJsonEntry executeOnly r Ix.Benchmark.Results.writeEntry path name row | none => pure () + let writeJoinJson (result : JoinResult) : IO Unit := + match jsonOut with + | some path => + let (name, row) := result.toJsonEntry + Ix.Benchmark.Results.writeEntry path name row + | none => pure () + let writeRejectedJoin (name : String) : IO Unit := + match jsonOut with + | some path => Ix.Benchmark.Results.writeEntry path name <| + Json.mkObj [("status", Json.str "rejected")] + | none => pure () -- `--execute-only`: stop after Phase 1; the results JSON (if requested) is -- already complete with the execute metrics. @@ -523,6 +619,7 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do let mut ordered := execed.qsort (·.1.fftCost < ·.1.fftCost) writeJson (ordered.map (·.1)) let mut spent : Float := 0.0 + let mut lifted : Array LiftArtifact := #[] for i in [:ordered.size] do let (r, addr) := ordered[i]! if r.failed then continue @@ -542,8 +639,17 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do aiurSystem.prove funIdx witness.input witness.inputIOBuffer else aiurSystem.proveIxVM funIdx witness.input witness.inputIOBuffer - (.ok (claim, proof, ioBuf) : - Except String (Array Aiur.G × Aiur.Proof × Aiur.IOBuffer)) + (.ok (claim, proof, ioBuf, none) : Except String + (Array Aiur.G × Aiur.Proof × Aiur.IOBuffer × Option ByteArray)) + else if join then + match aiurSystem.shardProveWithEnv funIdx envHandle + (singletonOwnedBlob addr) with + | .error e => .error e + | .ok (claimBytes, proof, ioBuf) => + let digest := Address.blake3 claimBytes + let claim := + Aiur.buildClaim funIdx (IxVM.ClaimHarness.packedDigestKey digest) #[] + .ok (claim, proof, ioBuf, some claimBytes) else match aiurSystem.proveAddrWithEnv funIdx envHandle addr.hash useInterp with | .error e => .error e @@ -555,10 +661,11 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do let digest := Address.blake3 claimBytes let claim := Aiur.buildClaim funIdx (IxVM.ClaimHarness.packedDigestKey digest) #[] - .ok (claim, proof, ioBuf) - match (proveRes : Except String (Array Aiur.G × Aiur.Proof × Aiur.IOBuffer)) with + .ok (claim, proof, ioBuf, none) + match (proveRes : Except String + (Array Aiur.G × Aiur.Proof × Aiur.IOBuffer × Option ByteArray)) with | .error e => IO.eprintln s!" prove {r.name} failed: {e}"; continue - | .ok (claim, proof, _ioBuf) => + | .ok (claim, proof, _ioBuf, checkEnvClaimBytes?) => spent := spent + proveSec let peak ← TracingTexray.peakTreeRssBytes let proofBytes := Aiur.Proof.toBytes proof @@ -592,14 +699,14 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do if let some (vCompiled, vIdx, vSystem) := vCtx then IO.println s!" [{i + 1}/{ordered.size}] recursively verifying {r.name} …" (← IO.getStdout).flush - let claimBytes := MultiStark.serializeClaims #[claim] + let innerClaimsBytes := MultiStark.serializeClaims #[claim] let vkBytes := aiurSystem.vkBytes - let pubInput := MultiStark.verifierPubInput vkBytes claimBytes + let pubInput := MultiStark.verifierPubInput vkBytes innerClaimsBytes -- Native path: the advice buffer is built in Rust from the raw -- byte blobs and execution routes through the codegen'd verifier. let (rvRes, rvSec) ← timed fun _ => vCompiled.bytecode.executeMultiStark vIdx pubInput proofBytes - vkBytes claimBytes useInterp + vkBytes innerClaimsBytes useInterp match rvRes with | .error e => IO.eprintln s!" ❌ recursive verifier REJECTED {r.name}'s proof: {e}" @@ -625,7 +732,7 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do TracingTexray.resetPeakTreeRss let ((rvClaim, rvProof), rvProveSec) ← timed fun _ => vSystem.proveMultiStark vIdx pubInput proofBytes vkBytes - claimBytes useInterp + innerClaimsBytes useInterp let rvPeak ← TracingTexray.peakTreeRssBytes let rvProofBytes := Aiur.Proof.toBytes rvProof let (rvVerifyRes, rvVerifySec) ← timed fun _ => @@ -644,13 +751,144 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do , recursiveProofSize := some rvProofBytes.size , recursiveVerifySec := rvVerifySec? }, addr) writeJson (ordered.map (·.1)) + if join && !r.failed then + match rvVerifyRes, checkEnvClaimBytes? with + | .ok (), some checkEnvClaimBytes => + let (expectedClaim, trees) ← IO.ofExcept <| + IxVM.ClaimHarness.shardCheckEnvClaimTrees ixonEnv #[addr] + if Ix.Claim.ser expectedClaim != checkEnvClaimBytes then + throw <| IO.userError s!"join benchmark: native shard claim for \ + {r.name} differs from host reconstruction" + let statement ← IO.ofExcept <| + MultiStark.CheckEnvTrees.ofClaim expectedClaim trees + lifted := lifted.push { + label := r.name + constants := r.constants + statement + innerClaimsBytes + checkEnvClaimBytes + outerClaim := rvClaim + proof := rvProof + } + | .error _, _ => pure () + | .ok (), none => + throw <| IO.userError s!"join benchmark: missing CheckEnv claim \ + preimage for {r.name}" catch e => IO.eprintln s!" prove {r.name} threw: {e}" + -- Phase 4 (--recursive --join): one pair-wide flat aggregate join. The two + -- child rows remain ordinary IxVM/lift measurements; the shared join lands + -- under its own stable `left + right` row so it is neither duplicated nor + -- assigned arbitrarily to one child. + let mut joinRejected := false + if join then + IO.println "── Phase 4: flat join ──" + let leftLabel := targets[0]!.1 + let rightLabel := targets[1]!.1 + let pairName := s!"{leftLabel} + {rightLabel}" + let some left := lifted.find? fun artifact => artifact.label == leftLabel | do + IO.eprintln s!"join benchmark: no verified lift for {leftLabel}" + return 1 + let some right := lifted.find? fun artifact => artifact.label == rightLabel | do + IO.eprintln s!"join benchmark: no verified lift for {rightLabel}" + return 1 + let some (vCompiled, liftIdx, vSystem) := vCtx | do + IO.eprintln "join benchmark: recursion context was not built" + return 1 + let some joinIdx := vCompiled.getFuncIdx `join_two | do + IO.eprintln "join benchmark: join_two entrypoint missing" + return 1 + let some structuralJoinIdx := vCompiled.getFuncIdx `join_two_structural | do + IO.eprintln "join benchmark: join_two_structural entrypoint missing" + return 1 + let ixvmVk := aiurSystem.vkBytes + let recursionVk := vSystem.vkBytes + let allowed := MultiStark.allowedBlob ixvmVk funIdx recursionVk liftIdx + joinIdx structuralJoinIdx + let outputStatement := left.statement.join right.statement + let outputClaimBytes := Ix.Claim.ser outputStatement.claim + let pubInput := MultiStark.joinPubInput allowed outputClaimBytes + let leftOuterBytes := MultiStark.serializeClaims #[left.outerClaim] + let rightOuterBytes := MultiStark.serializeClaims #[right.outerClaim] + let preimagesBlob := MultiStark.joinPreimagesBlob + #[left.innerClaimsBytes, right.innerClaimsBytes, + left.checkEnvClaimBytes, right.checkEnvClaimBytes] + let treesBlob := MultiStark.joinTreesBlob <| + MultiStark.CheckEnvTrees.adviceTrees + left.statement right.statement outputStatement + let pathsBlob := MultiStark.joinPathsBlob #[] + IO.println s!" executing join {pairName} …" + (← IO.getStdout).flush + let (joinExecuteResult, joinExecuteSec) ← timed fun _ => + vCompiled.bytecode.executeMultiStarkJoin joinIdx pubInput + left.proof.toBytes right.proof.toBytes recursionVk + leftOuterBytes rightOuterBytes outputClaimBytes allowed + preimagesBlob treesBlob pathsBlob + let joinFftCost ← match joinExecuteResult with + | .error e => + IO.eprintln s!" ❌ join verifier REJECTED {pairName}: {e}" + writeRejectedJoin pairName + joinRejected := true + pure none + | .ok (_, queryCounts) => + let stats := Aiur.computeStats vCompiled queryCounts vSystem.circuitShapes + (logBlowup := commitParams.logBlowup) + IO.println s!" {pairName}: join-execute={joinExecuteSec}s \ + join-fft-cost={stats.totalFftCost}" + if useTexray then Aiur.printStats stats + pure (some stats.totalFftCost) + if let some joinFftCost := joinFftCost then + IO.println s!" proving join {pairName} …" + (← IO.getStdout).flush + TracingTexray.resetPeakTreeRss + let (joinProveResult, joinProveSec) ← timed fun _ => + vSystem.proveMultiStarkJoin joinIdx pubInput + left.proof.toBytes right.proof.toBytes recursionVk + leftOuterBytes rightOuterBytes outputClaimBytes allowed + preimagesBlob treesBlob pathsBlob + match joinProveResult with + | .error e => + IO.eprintln s!" prove join {pairName} failed: {e}" + return 1 + | .ok (joinClaim, joinProof) => + let expectedClaim := Aiur.buildClaim joinIdx pubInput #[] + if joinClaim != expectedClaim then + IO.eprintln s!" join {pairName} returned an unexpected outer claim" + return 1 + let joinPeak ← TracingTexray.peakTreeRssBytes + let joinProofBytes := joinProof.toBytes + let (joinVerifyResult, joinVerifySec) ← timed fun _ => + vSystem.verify joinClaim joinProof + let joinVerifySec? ← match joinVerifyResult with + | .ok () => pure (some joinVerifySec) + | .error e => + IO.eprintln s!" join verify {pairName} FAILED: {e}" + joinRejected := true + pure none + let joinResult : JoinResult := { + name := pairName + constants := left.constants + right.constants + fftCost := joinFftCost + executeSec := joinExecuteSec + proveSec := joinProveSec + peakRss := joinPeak + proofSize := joinProofBytes.size + verifySec := joinVerifySec? + failed := joinVerifySec?.isNone + } + writeJoinJson joinResult + IO.println s!" {pairName}: join-prove={joinProveSec}s \ + join-verify={joinVerifySec}s proof={joinProofBytes.size} bytes" + match jsonOut with - | some path => IO.println s!"wrote {ordered.size} benchmarks to {path} ({spent}s proving)" + | some path => + let rowCount := ordered.size + (if join && !joinRejected then 1 else 0) + IO.println s!"wrote {rowCount} benchmarks to {path} ({spent}s proving)" | none => IO.println s!"proved {ordered.size} constants ({spent}s); pass --json to emit results" - return if ordered.any (·.1.failed) then Ix.Benchmark.Results.exitRejected else 0 + return if ordered.any (·.1.failed) || joinRejected then + Ix.Benchmark.Results.exitRejected + else 0 def typecheckCmd : Cli.Cmd := `[Cli| typecheck VIA runTypecheckCmd; @@ -660,10 +898,11 @@ def typecheckCmd : Cli.Cmd := `[Cli| "ixe" : String; "Path to a serialized `Ixon.Env` (e.g. produced by `ix compile`). Required." "consts" : String; "Comma-separated fully-qualified constant names to benchmark (e.g. `Nat.add_comm,String.append`). Same flag/shape as `ix check --consts`, `zisk-host --consts`, and `sp1-host --consts`." "consts-file" : String; "Additionally read constant names from a file (one per line; `#` comments and blank lines ignored). Unions with --consts." - "json" : String; "Write per-constant results JSON to this path. Off by default; normal CLI usage prints only the human-readable summary." + "json" : String; "Write results JSON to this path (per constant, plus one pair row with --join). Off by default; normal CLI usage prints only the human-readable summary." "skip-deps"; "Check only each target itself (verify_const, trusting its deps) instead of re-checking its whole transitive closure (verify_claim). Same flag as `zisk-host --skip-deps`." "execute-only"; "Execute only (Phase 1: constants / fft-cost / execute-time) and skip proving. The fast per-PR `execute`-mode signal." "recursive"; "After each prove, execute and then prove the in-circuit multi-stark verifier over the fresh proof (the fri-verifier-* metrics; see the module docstring). Uses recursion-tuned FRI parameters. Conflicts with --execute-only." + "join"; "With --recursive and exactly two resolved constants, prove each as a singleton CheckEnv shard, lift both, then execute/prove/verify one flat aggregate join. Emits a dedicated `left + right` row with join-* metrics. Conflicts with --skip-deps, --execute-only, and --interp." "interp"; "Route execution through the generic Aiur bytecode interpreter instead of the codegen'd IxVM kernel - no `lake exe ix codegen` + cargo rebuild needed after `Ix/IxVM/*.lean` edits. Applies to Phase 1, the prove's witness generation, and both --recursive steps. Slower; execute-time rows are not comparable to codegen-mode runs (fft-cost is)." "queries" : Nat; "Override the FRI query count of the selected parameter set (default 100, or 50 with --recursive; applies to inner and outer proof alike)." texray; "Enable the tracing-texray timeline + RAM breakdown (per-prove spans on stderr). Combined with --json, per-phase span timings are additionally written to `.spans` as JSON Lines for the CI drill-down. Off by default." diff --git a/Ix/Aiur/Protocol.lean b/Ix/Aiur/Protocol.lean index 322ebad65..d1f5a913a 100644 --- a/Ix/Aiur/Protocol.lean +++ b/Ix/Aiur/Protocol.lean @@ -25,6 +25,12 @@ opaque toBytes : @& Proof → ByteArray @[extern "rs_aiur_proof_of_bytes"] opaque ofBytes : @& ByteArray → Proof +/-- Decode an untrusted serialized proof without aborting the process. Cache +and network boundaries must use this variant; `ofBytes` remains for callers +whose bytes were produced in-process or already validated. -/ +@[extern "rs_aiur_proof_of_bytes_checked"] +opaque ofBytesChecked : @& ByteArray → Except String Proof + end Proof structure CommitmentParameters where diff --git a/Ix/Cli/AggregateCmd.lean b/Ix/Cli/AggregateCmd.lean index e1f54877c..467367125 100644 --- a/Ix/Cli/AggregateCmd.lean +++ b/Ix/Cli/AggregateCmd.lean @@ -1,18 +1,20 @@ /- `ix aggregate --ixe E --ixes M ...` - Bind persisted shard proof wrappers to every shard in a manifest, lift each - IxVM proof into the Multi-STARK recursion system, then execute/prove binary - joins in the manifest's bisection-tree order. Small joins use flat canonical - subjects; joins above `--structural-above` use an O(1) root-of-roots subject - fold plus assumption-membership paths. The final persisted wrapper carries - the aggregate `CheckEnv` claim and recursive proof bytes. - - This first host driver is intentionally serial and cache-free. Its slot - model and content-addressed inputs make parallel scheduling and resumable - cache entries follow-up optimizations rather than protocol changes. + Bind persisted shard proof wrappers to every nonempty shard in a manifest, + lift each IxVM proof into the Multi-STARK recursion system, then execute/prove + any binary joins in the manifest's bisection-tree order. Small joins use flat + canonical subjects; joins above `--structural-above` use an O(1) + root-of-roots subject fold plus assumption-membership paths. The final + persisted wrapper carries the aggregate `CheckEnv` claim and recursive proof + bytes. + + The host driver schedules the fold as a dependency DAG. Ready slots run on + dedicated tasks under explicit job and RAM reservations; every completed + lift/join is persisted in a verified, content-addressed resume cache. -/ module +import Std.Sync public import Cli public import Ix.Cli.CheckCmd public import Ix.IxVM @@ -35,10 +37,29 @@ structure AggregateSlot where subjectCount : Nat outerClaim : Array Aiur.G proof : Aiur.Proof + proofAddress? : Option Address /-- Preimages needed when this slot is decoded by its parent. A lift exposes its inner claims plus `CheckEnv`; a join exposes only its output `CheckEnv`. -/ openPreimages : Array ByteArray +/-- Everything claim-derived about a slot, computed for the whole fold before +the first cache lookup or proof. -/ +structure AggregateSlotSpec where + statement : MultiStark.CheckEnvTrees + subjectCount : Nat + outerClaim : Array Aiur.G + cacheKey : Address + +structure CachedAggregateProof where + proof : Aiur.Proof + address : Address + +inductive AggregateCacheAddress where + | miss + | hit (address : Address) + | invalid (reason : String) + deriving Repr + /-- A manifest fold operation annotated with the cumulative subject count and the monotone flat/structural choice used by the prover. -/ structure ScheduledFold where @@ -47,8 +68,219 @@ structure ScheduledFold where structural : Bool deriving BEq, Repr +/-- The immutable result of simulating aggregate-slot admission. Runtime and +unit tests share the same admission function; the simulator completes the +lowest-numbered in-flight slot after every admission pass solely to make its +trace deterministic. -/ +structure AggregateScheduleTrace where + admissionOrder : Array Nat + admissionBatches : Array (Array Nat) + maxReservedBytes : Nat + deriving BEq, Repr + def defaultStructuralAbove : Nat := 4096 +def aggregateGiB : Nat := 1024 * 1024 * 1024 + +/-- Calibration-pending q=100 lift reserve from the measured §3.2 upper +bound. A slot heavier than the configured budget is admitted only by itself, +matching the existing Rust-side `RamGate` and avoiding deadlock. -/ +def aggregateLiftRamBytes : Nat := 195 * aggregateGiB + +/-- Structural joins are dominated by the same two recursive-proof checks as +lifts. Keep the conservative lift reserve until the real E2E calibration. -/ +def aggregateStructuralJoinRamBytes : Nat := aggregateLiftRamBytes + +/-- Flat joins add canonical subject-tree work to the recursive-proof base. +One MiB per subject is a deliberately conservative placeholder: at Init's +~52k-subject root it adds ~51 GiB, consistent with the §11.4 estimate. The +default structural threshold caps this term near 4 GiB in production. -/ +def aggregateFlatJoinRamPerSubjectBytes : Nat := 1024 * 1024 + +/-- Calibration-pending per-slot RAM weight used by the Lean admission gate. -/ +def aggregateSlotRamBytes (item : ScheduledFold) : Nat := + match item.op with + | .leaf _ => aggregateLiftRamBytes + | .join _ _ => + if item.structural then aggregateStructuralJoinRamBytes + else aggregateStructuralJoinRamBytes + + item.subjectCount * aggregateFlatJoinRamPerSubjectBytes + +def aggregateSlotRamWeights (plan : Array ScheduledFold) : Array Nat := + plan.map aggregateSlotRamBytes + +private def aggregateScheduleInputsValid (plan : Array ScheduledFold) + (weights : Array Nat) : Except String Unit := do + if weights.size != plan.size then + throw s!"aggregate scheduler received {weights.size} weights for {plan.size} slots" + for (item, slotIdx) in plan.mapIdx fun slotIdx item => (item, slotIdx) do + if weights[slotIdx]! == 0 then + throw s!"aggregate scheduler slot {slotIdx} has zero RAM weight" + match item.op with + | .leaf _ => pure () + | .join left right => + if left >= slotIdx || right >= slotIdx then + throw s!"aggregate scheduler slot {slotIdx} has non-prior child {left}, {right}" + +private def aggregateDependenciesComplete (item : ScheduledFold) + (completed : Array Bool) : Bool := + match item.op with + | .leaf _ => true + | .join left right => + (completed[left]?).getD false && (completed[right]?).getD false + +/-- Select one deterministic admission batch from the currently ready slots. +Candidates are ordered by descending RAM weight, then ascending slot number. +Slots that do not fit are skipped so lighter work can use the remaining +budget. An individually oversized slot may run only when nothing else is +reserved, following the Rust `RamGate` admit-when-alone rule. `jobs = 0` +means no concurrency cap beyond the number of plan slots. -/ +def admitAggregateReady (plan : Array ScheduledFold) (weights : Array Nat) + (completed inFlight : Array Bool) (reservedBytes budgetBytes jobs : Nat) : + Array Nat := Id.run do + let active := inFlight.count true + let maxJobs := if jobs == 0 then max 1 plan.size else max 1 jobs + if active >= maxJobs then return #[] + let openJobs := maxJobs - active + let mut ready : Array Nat := #[] + for slotIdx in [:plan.size] do + if !(completed[slotIdx]?).getD false && + !(inFlight[slotIdx]?).getD false then + if let some item := plan[slotIdx]? then + if aggregateDependenciesComplete item completed then + ready := ready.push slotIdx + ready := ready.qsort fun left right => + let leftWeight := (weights[left]?).getD 0 + let rightWeight := (weights[right]?).getD 0 + leftWeight > rightWeight || (leftWeight == rightWeight && left < right) + let mut admitted : Array Nat := #[] + let mut admittedBytes := 0 + for slotIdx in ready do + if admitted.size >= openJobs then break + let weight := (weights[slotIdx]?).getD 0 + let nextReserved := reservedBytes + admittedBytes + weight + if nextReserved <= budgetBytes || + (reservedBytes == 0 && admitted.isEmpty) then + admitted := admitted.push slotIdx + admittedBytes := admittedBytes + weight + return admitted + +/-- Pure deterministic exercise of the runtime admission algorithm. This is +used to gate heaviest-first ordering, dependency release, job caps, and peak +reservation without starting proof tasks. -/ +def simulateAggregateSchedule (plan : Array ScheduledFold) + (weights : Array Nat) (jobs budgetBytes : Nat) : + Except String AggregateScheduleTrace := do + aggregateScheduleInputsValid plan weights + if budgetBytes == 0 then throw "aggregate scheduler RAM budget must be positive" + let mut completed := Array.replicate plan.size false + let mut inFlight := Array.replicate plan.size false + let mut completedCount := 0 + let mut reservedBytes := 0 + let mut maxReservedBytes := 0 + let mut admissionOrder : Array Nat := #[] + let mut admissionBatches : Array (Array Nat) := #[] + while completedCount < plan.size do + let admitted := admitAggregateReady plan weights completed inFlight + reservedBytes budgetBytes jobs + if !admitted.isEmpty then + admissionBatches := admissionBatches.push admitted + for slotIdx in admitted do + inFlight := inFlight.set! slotIdx true + reservedBytes := reservedBytes + weights[slotIdx]! + admissionOrder := admissionOrder.push slotIdx + maxReservedBytes := max maxReservedBytes reservedBytes + let mut finish? : Option Nat := none + for slotIdx in [:plan.size] do + if finish?.isNone && inFlight[slotIdx]! then finish? := some slotIdx + let some finished := finish? + | throw "aggregate scheduler deadlocked with unfinished slots" + inFlight := inFlight.set! finished false + completed := completed.set! finished true + reservedBytes := reservedBytes - weights[finished]! + completedCount := completedCount + 1 + pure { admissionOrder, admissionBatches, maxReservedBytes } + +private def formatAggregateGiB (bytes : Nat) : String := + let tenths := bytes * 10 / aggregateGiB + s!"{tenths / 10}.{tenths % 10}" + +/-- Linux `MemTotal` parser kept separate so the 92% default has a pure seam. +The fallback only affects non-Linux hosts; admit-when-alone still guarantees +progress without pretending the fallback is a calibrated capacity. -/ +def aggregateMemTotalBytes (contents : String) : Option Nat := + (contents.splitOn "\n").findSome? fun line => + if line.startsWith "MemTotal:" then + ((line.splitOn " ").filter (· != "") |>.drop 1).head?.bind fun kib => + kib.toNat?.map (· * 1024) + else none + +def defaultAggregateRamBudgetBytes : IO Nat := do + let contents ← try IO.FS.readFile "/proc/meminfo" catch _ => pure "" + return match aggregateMemTotalBytes contents with + | some total => total / 100 * 92 + | none => 16 * aggregateGiB + +/-- Bump when aggregate advice framing changes without changing the recursion +verifying key. Encoded as `u64` little-endian in every cache key. -/ +def aggregateCacheVersion : Nat := 1 + +/-- +`blake3(version ‖ recursion_vk_digest ‖ fri_params_ser ‖ outer_claim_bytes)`. + +`serializeClaims #[outerClaim]` is the canonical, length-delimited outer-claim +encoding. The expected outer claim already commits to the entrypoint and public +input; joins therefore transitively pin the allowed blob and output statement. +-/ +def aggregateCacheKey (recursionVk : ByteArray) + (recursionParameters : MultiStark.RecursionParameters) + (outerClaim : Array Aiur.G) (version : Nat := aggregateCacheVersion) : Address := + let recursionVkDigest := (Address.blake3 recursionVk).hash + let outerClaimBytes := MultiStark.serializeClaims #[outerClaim] + Address.blake3 ⟨MultiStark.u64le version ++ recursionVkDigest.data ++ + recursionParameters.cacheFriBytes.data ++ outerClaimBytes.data⟩ + +/-- Resolve the global aggregate cache or a hermetic test root. -/ +def aggregateCacheDir (cacheRoot : Option System.FilePath := none) : IO System.FilePath := do + match cacheRoot with + | some root => + let dir := root / "aggregate" + IO.FS.createDirAll dir + pure dir + | none => StoreIO.toIO (Store.cacheDir "aggregate") + +/-- Read an untrusted cache-index entry without turning malformed content into +a command failure. Store loading and proof verification happen separately. -/ +def readAggregateCacheAddress (dir : System.FilePath) (key : Address) : + IO AggregateCacheAddress := do + let path := dir / toString key + if !(← path.pathExists) then return .miss + try + let raw ← IO.FS.readFile path + match Address.fromString raw.trimAscii.toString with + | some address => return .hit address + | none => return .invalid "index content is not a 64-character store address" + catch e => + return .invalid s!"index read failed: {e}" + +/-- Atomically replace one derived cache-index entry. -/ +def writeAggregateCacheAddress (dir : System.FilePath) (key address : Address) : + IO Unit := do + let tmp := dir / s!"{key}.tmp" + IO.FS.writeFile tmp s!"{address}\n" + IO.FS.rename tmp (dir / toString key) + +/-- A cached wrapper is reusable only when both its bundled `CheckEnv` claim +and its proof under the exact expected outer Aiur claim validate. -/ +def validateAggregateCacheWrapper (recursionSystem : Aiur.AiurSystem) + (expectedClaim : Ix.Claim) (expectedOuterClaim : Array Aiur.G) + (wrapper : Ixon.Proof) : Except String Aiur.Proof := do + if wrapper.claim != expectedClaim then + throw s!"bundled claim {wrapper.claim} does not match expected {expectedClaim}" + let proof ← Aiur.Proof.ofBytesChecked wrapper.proof + recursionSystem.verify expectedOuterClaim proof + pure proof + /-- Resolve subject counts and the structural threshold once, before proving. Because parent counts only grow, `count > structuralAbove` makes the mode monotone: a flat join is never scheduled above a structural child. -/ @@ -73,6 +305,64 @@ def schedulePlan (plan : Array Ix.Cli.CheckCmd.AggregationTree.FoldOp) } pure scheduled +/-- Derive every slot statement, outer claim, and cache key before proving. +This makes resume independent of execution order and lets manifest changes +invalidate only the claim-changed subtree. -/ +def buildAggregateSlotSpecs (plan : Array ScheduledFold) + (prepared : Array PreparedShard) (ixvmVk recursionVk allowed : ByteArray) + (verifyIdx liftIdx joinIdx structuralJoinIdx : Aiur.Bytecode.FunIdx) + (recursionParameters : MultiStark.RecursionParameters) : + Except String (Array AggregateSlotSpec) := do + let mut specs : Array AggregateSlotSpec := #[] + for item in plan do + match item.op with + | .leaf shard => + let some preparedShard := prepared[shard]? + | throw s!"aggregate plan references missing prepared shard {shard}" + if preparedShard.claim != preparedShard.statement.claim then + throw s!"prepared shard {shard} claim and statement disagree" + if preparedShard.statement.subjectCount != item.subjectCount then + throw s!"prepared shard {shard} has {preparedShard.statement.subjectCount} \ + subjects, but the schedule records {item.subjectCount}" + let claimBytes := Ix.Claim.ser preparedShard.claim + let verifyInput := IxVM.ClaimHarness.packedDigestKey + (Address.blake3 claimBytes) + let innerClaim := Aiur.buildClaim verifyIdx verifyInput #[] + let innerClaimsBytes := MultiStark.serializeClaims #[innerClaim] + let pubInput := MultiStark.verifierPubInput ixvmVk innerClaimsBytes + let outerClaim := Aiur.buildClaim liftIdx pubInput #[] + specs := specs.push { + statement := preparedShard.statement + subjectCount := item.subjectCount + outerClaim + cacheKey := aggregateCacheKey recursionVk recursionParameters outerClaim + } + | .join leftIdx rightIdx => + let some left := specs[leftIdx]? + | throw s!"aggregate plan references missing left spec {leftIdx}" + let some right := specs[rightIdx]? + | throw s!"aggregate plan references missing right spec {rightIdx}" + if left.subjectCount + right.subjectCount != item.subjectCount then + throw "aggregate plan has inconsistent joined subject counts" + let output := if item.structural then + left.statement.joinStructural right.statement + else + left.statement.join right.statement + if output.subjectCount != item.subjectCount then + throw s!"aggregate join reconstructs {output.subjectCount} subjects, \ + but the schedule records {item.subjectCount}" + let outputClaimBytes := Ix.Claim.ser output.claim + let pubInput := MultiStark.joinPubInput allowed outputClaimBytes + let joinFunIdx := if item.structural then structuralJoinIdx else joinIdx + let outerClaim := Aiur.buildClaim joinFunIdx pubInput #[] + specs := specs.push { + statement := output + subjectCount := item.subjectCount + outerClaim + cacheKey := aggregateCacheKey recursionVk recursionParameters outerClaim + } + pure specs + private def addrOfHex (label value : String) : Except String Address := match Address.fromString value with | some address => .ok address @@ -82,7 +372,7 @@ private def addrOfHex (label value : String) : Except String Address := private def prepareShard (env : Ixon.Env) (blocks : Array Address) : Except String PreparedShard := do let owned := Ix.Cli.CheckCmd.ownedConstsForBlocks env blocks - let (claim, _, trees) ← IxVM.ClaimHarness.shardCheckEnvClaim env owned + let (claim, trees) ← IxVM.ClaimHarness.shardCheckEnvClaimTrees env owned let statement ← MultiStark.CheckEnvTrees.ofClaim claim trees pure { claim, statement } @@ -95,7 +385,181 @@ private def compileToplevel (label : String) | .error e => return Except.error s!"{label} compilation failed: {e}" | .ok compiled => return Except.ok compiled -private def printPlan (plan : Array ScheduledFold) (structuralAbove : Nat) : IO Unit := do +/-- Execute a post-order aggregate plan as a dependency-driven DAG. The +controller is the sole owner of completion and reservation state: it admits a +heaviest-first batch, starts one dedicated task per slot, then releases child +dependencies as results arrive. `runSlot` receives an immutable snapshot in +which every declared child is complete. + +On the first failure no further work is admitted, but already-running tasks +are drained before returning. This prevents orphan proof tasks and permits +successful independent slots to finish publishing cache entries safely. -/ +def runAggregateDag (plan : Array ScheduledFold) (weights : Array Nat) + (jobs budgetBytes : Nat) + (runSlot : Nat → Array (Option α) → IO (Except String α)) + (trace : Bool := false) : IO (Except String (Array α)) := do + match aggregateScheduleInputsValid plan weights with + | .error e => return .error e + | .ok () => pure () + if budgetBytes == 0 then + return .error "aggregate scheduler RAM budget must be positive" + + let resultChan ← Std.CloseableChannel.Sync.new + (α := Nat × Nat × Except String α) + let mut tasks : Array (Task (Except IO.Error Unit)) := #[] + let mut slots : Array (Option α) := Array.replicate plan.size none + let mut completed := Array.replicate plan.size false + let mut inFlight := Array.replicate plan.size false + let mut completedCount := 0 + let mut active := 0 + let mut reservedBytes := 0 + let mut failures : Array (Nat × String) := #[] + let maxJobs := if jobs == 0 then max 1 plan.size else max 1 jobs + + while completedCount < plan.size do + if failures.isEmpty then + let admitted := admitAggregateReady plan weights completed inFlight + reservedBytes budgetBytes jobs + for slotIdx in admitted do + let weight := weights[slotIdx]! + inFlight := inFlight.set! slotIdx true + active := active + 1 + reservedBytes := reservedBytes + weight + if trace then + let overBudget := if weight > budgetBytes then "; over-budget slot runs alone" else "" + IO.println s!"[aggregate] slot {slotIdx}: admitted {formatAggregateGiB weight} GiB; \ + reserved {formatAggregateGiB reservedBytes}/{formatAggregateGiB budgetBytes} GiB; \ + active {active}/{maxJobs}{overBudget}" + let snapshot := slots + let task ← IO.asTask (prio := .dedicated) do + let result ← try runSlot slotIdx snapshot catch e => + pure (.error s!"uncaught IO error: {e}") + discard <| resultChan.send (slotIdx, weight, result) + tasks := tasks.push task + + if active == 0 then + if failures.isEmpty then + failures := failures.push + (plan.size, "aggregate scheduler deadlocked with unfinished slots") + break + + match ← resultChan.recv with + | none => + failures := failures.push + (plan.size, "aggregate scheduler result channel closed unexpectedly") + break + | some (slotIdx, weight, result) => + if !(inFlight[slotIdx]?).getD false then + failures := failures.push + (slotIdx, "aggregate scheduler received a duplicate or unknown result") + else + inFlight := inFlight.set! slotIdx false + active := active - 1 + reservedBytes := reservedBytes - weight + match result with + | .error e => failures := failures.push (slotIdx, e) + | .ok value => + slots := slots.set! slotIdx (some value) + completed := completed.set! slotIdx true + completedCount := completedCount + 1 + + -- A failure stops admission but never abandons tasks already inside an FFI + -- prove. Drain their channel results before closing and joining handles. + while active > 0 do + match ← resultChan.recv with + | none => + failures := failures.push + (plan.size, "aggregate scheduler result channel closed while draining") + active := 0 + | some (slotIdx, weight, result) => + if (inFlight[slotIdx]?).getD false then + inFlight := inFlight.set! slotIdx false + active := active - 1 + reservedBytes := reservedBytes - weight + match result with + | .error e => failures := failures.push (slotIdx, e) + | .ok value => + slots := slots.set! slotIdx (some value) + if !(completed[slotIdx]?).getD false then + completed := completed.set! slotIdx true + completedCount := completedCount + 1 + discard <| resultChan.close + for task in tasks do + match task.get with + | .ok () => pure () + | .error e => + failures := failures.push (plan.size, + s!"aggregate scheduler task failed: {e}") + + if !failures.isEmpty then + let sortedFailures := failures.qsort fun left right => left.1 < right.1 + let (slotIdx, e) := sortedFailures[0]! + return .error (if slotIdx < plan.size then s!"slot {slotIdx}: {e}" else e) + + let mut result : Array α := #[] + for slotIdx in [:plan.size] do + let some value := (slots[slotIdx]?).join + | return .error s!"aggregate scheduler completed without slot {slotIdx}" + result := result.push value + pure (.ok result) + +def loadCachedAggregateProofWith + (readStore : Address → IO ByteArray) (dir : System.FilePath) (slotIdx : Nat) + (spec : AggregateSlotSpec) (recursionSystem : Aiur.AiurSystem) : + IO (Option CachedAggregateProof) := do + match ← readAggregateCacheAddress dir spec.cacheKey with + | .miss => return none + | .invalid reason => + IO.println s!"[aggregate] slot {slotIdx}: cache miss ({reason})" + return none + | .hit address => + try + let bytes ← readStore address + if Address.blake3 bytes != address then + IO.println s!"[aggregate] slot {slotIdx}: cache miss \ + (store object {address} has a different content digest)" + return none + let wrapper ← match Ixon.Proof.de bytes with + | .ok wrapper => pure wrapper + | .error e => + IO.println s!"[aggregate] slot {slotIdx}: cache miss \ + (wrapper {address} does not decode: {e})" + return none + match validateAggregateCacheWrapper recursionSystem spec.statement.claim + spec.outerClaim wrapper with + | .ok proof => + IO.println s!"[aggregate] slot {slotIdx}: cache hit {address}" + return some { proof, address } + | .error e => + IO.println s!"[aggregate] slot {slotIdx}: cache miss \ + (wrapper {address} rejected: {e})" + return none + catch e => + IO.println s!"[aggregate] slot {slotIdx}: cache miss \ + (cannot load wrapper {address}: {e})" + return none + +private def loadCachedAggregateProof (dir : System.FilePath) (slotIdx : Nat) + (spec : AggregateSlotSpec) (recursionSystem : Aiur.AiurSystem) : + IO (Option CachedAggregateProof) := + loadCachedAggregateProofWith (fun address => StoreIO.toIO (Store.read address)) + dir slotIdx spec recursionSystem + +private def persistAggregateCacheProof (dir : System.FilePath) (slotIdx : Nat) + (spec : AggregateSlotSpec) (proof : Aiur.Proof) : IO (Option Address) := do + try + let _ ← StoreIO.toIO (Store.write (Ix.Claim.ser spec.statement.claim)) + let wrapper : Ixon.Proof := { claim := spec.statement.claim, proof := proof.toBytes } + let address ← StoreIO.toIO (Store.write (Ixon.Proof.ser wrapper)) + writeAggregateCacheAddress dir spec.cacheKey address + IO.println s!"[aggregate] slot {slotIdx}: cached proof {address}" + return some address + catch e => + IO.eprintln s!"[aggregate] slot {slotIdx}: warning: could not persist cache entry: {e}" + return none + +private def printPlan (plan : Array ScheduledFold) (shardIds : Array Nat) + (structuralAbove : Nat) : IO Unit := do let lifts := plan.countP fun item => match item.op with | .leaf _ => true | .join _ _ => false @@ -105,13 +569,148 @@ private def printPlan (plan : Array ScheduledFold) (structuralAbove : Nat) : IO for (item, slot) in plan.mapIdx fun slot item => (item, slot) do match item.op with | .leaf shard => - IO.println s!" slot {slot}: lift shard {shard} ({item.subjectCount} subjects)" + let originalShard := (shardIds[shard]?).getD shard + IO.println s!" slot {slot}: lift shard {originalShard} ({item.subjectCount} subjects)" | .join left right => let mode := if item.structural then "structural" else "flat" IO.println s!" slot {slot}: {mode} join slots {left}, {right} \ ({item.subjectCount} subjects)" -def runAggregateCmd (p : Cli.Parsed) : IO UInt32 := do +private structure AggregateProveContext where + plan : Array ScheduledFold + specs : Array AggregateSlotSpec + prepared : Array PreparedShard + proofsByShard : Std.HashMap Nat Ixon.Proof + shardIds : Array Nat + ixvmSystem : Aiur.AiurSystem + recursionSystem : Aiur.AiurSystem + ixvmVk : ByteArray + recursionVk : ByteArray + allowed : ByteArray + verifyIdx : Aiur.Bytecode.FunIdx + liftIdx : Aiur.Bytecode.FunIdx + joinIdx : Aiur.Bytecode.FunIdx + structuralJoinIdx : Aiur.Bytecode.FunIdx + cacheDir? : Option System.FilePath + +/-- Prove or resume one slot whose dependencies have already completed. The +scheduler catches IO exceptions around this function; protocol and validation +failures stay explicit so the lowest failed slot can be reported +deterministically after all admitted tasks drain. -/ +private def proveAggregateSlot (ctx : AggregateProveContext) (slotIdx : Nat) + (slots : Array (Option AggregateSlot)) : IO (Except String AggregateSlot) := do + let some item := ctx.plan[slotIdx]? + | return .error "missing scheduled fold item" + let some spec := ctx.specs[slotIdx]? + | return .error "missing prepared aggregate slot" + match item.op with + | .leaf shard => + let originalShard := (ctx.shardIds[shard]?).getD shard + let some wrapper := ctx.proofsByShard.get? shard + | return .error s!"no proof for shard {originalShard}" + let some preparedShard := ctx.prepared[shard]? + | return .error s!"no statement for shard {originalShard}" + let claimBytes := Ix.Claim.ser preparedShard.claim + let verifyInput := IxVM.ClaimHarness.packedDigestKey + (Address.blake3 claimBytes) + let innerClaim := Aiur.buildClaim ctx.verifyIdx verifyInput #[] + let innerProof ← match Aiur.Proof.ofBytesChecked wrapper.proof with + | .error e => + return Except.error s!"shard {originalShard} proof does not decode: {e}" + | .ok proof => pure proof + match ctx.ixvmSystem.verify innerClaim innerProof with + | .error e => + return Except.error s!"shard {originalShard} proof fails native verification: {e}" + | .ok () => pure () + let innerClaimsBytes := MultiStark.serializeClaims #[innerClaim] + let cached? ← match ctx.cacheDir? with + | none => pure none + | some dir => loadCachedAggregateProof dir slotIdx spec ctx.recursionSystem + let (proof, proofAddress?) ← match cached? with + | some cached => pure (cached.proof, some cached.address) + | none => + let pubInput := MultiStark.verifierPubInput ctx.ixvmVk innerClaimsBytes + IO.println s!"[aggregate] lifting shard {originalShard} into slot {slotIdx}" + (← IO.getStdout).flush + let (outerClaim, proof) := ctx.recursionSystem.proveMultiStark + ctx.liftIdx pubInput wrapper.proof ctx.ixvmVk innerClaimsBytes + if outerClaim != spec.outerClaim then + return .error "lift produced an unexpected outer claim" + let proofAddress? ← match ctx.cacheDir? with + | none => pure none + | some dir => persistAggregateCacheProof dir slotIdx spec proof + pure (proof, proofAddress?) + return .ok { + statement := spec.statement + subjectCount := spec.subjectCount + outerClaim := spec.outerClaim + proof + proofAddress? + openPreimages := #[innerClaimsBytes, claimBytes] + } + | .join leftIdx rightIdx => + let some left := (slots[leftIdx]?).join + | return .error s!"missing completed left slot {leftIdx}" + let some right := (slots[rightIdx]?).join + | return .error s!"missing completed right slot {rightIdx}" + let output := spec.statement + let outputClaimBytes := Ix.Claim.ser output.claim + let cached? ← match ctx.cacheDir? with + | none => pure none + | some dir => loadCachedAggregateProof dir slotIdx spec ctx.recursionSystem + let (proof, proofAddress?) ← match cached? with + | some cached => pure (cached.proof, some cached.address) + | none => + let pubInput := MultiStark.joinPubInput ctx.allowed outputClaimBytes + let leftClaimsBytes := MultiStark.serializeClaims #[left.outerClaim] + let rightClaimsBytes := MultiStark.serializeClaims #[right.outerClaim] + let preimagesBlob := MultiStark.joinPreimagesBlob + (left.openPreimages ++ right.openPreimages) + let trees := if item.structural then + MultiStark.CheckEnvTrees.structuralAdviceTrees + left.statement right.statement output + else + MultiStark.CheckEnvTrees.adviceTrees + left.statement right.statement output + let treesBlob := MultiStark.joinTreesBlob trees + let pathsBlob := if item.structural then + MultiStark.joinPathsBlob + (MultiStark.CheckEnvTrees.structuralPathAdvice + left.statement right.statement output) + else + MultiStark.joinPathsBlob #[] + let joinFunIdx := if item.structural then ctx.structuralJoinIdx else ctx.joinIdx + let mode := if item.structural then "structural" else "flat" + IO.println s!"[aggregate] {mode}-joining slots {leftIdx}, {rightIdx} into {slotIdx}" + (← IO.getStdout).flush + let result := ctx.recursionSystem.proveMultiStarkJoin joinFunIdx pubInput + left.proof.toBytes right.proof.toBytes ctx.recursionVk + leftClaimsBytes rightClaimsBytes outputClaimBytes ctx.allowed + preimagesBlob treesBlob pathsBlob + let (outerClaim, proof) ← match result with + | .error e => return .error e + | .ok result => pure result + if outerClaim != spec.outerClaim then + return .error "join produced an unexpected outer claim" + let proofAddress? ← match ctx.cacheDir? with + | none => pure none + | some dir => persistAggregateCacheProof dir slotIdx spec proof + pure (proof, proofAddress?) + return .ok { + statement := output + subjectCount := spec.subjectCount + outerClaim := spec.outerClaim + proof + proofAddress? + openPreimages := #[outputClaimBytes] + } + +/-- Aggregate with an explicit recursion-proof configuration. The CLI wrapper +below supplies `defaultRecursionParameters`; keeping this seam explicit lets a +future policy or cache layer select a recursion configuration without changing +the canonical IxVM proof parameters. -/ +def runAggregateCmdWith (recursionParameters : MultiStark.RecursionParameters) + (p : Cli.Parsed) : IO UInt32 := do let some ixePath := (p.flag? "ixe").map (·.as! String) | do p.printError "error: aggregate requires --ixe " return 1 @@ -119,28 +718,42 @@ def runAggregateCmd (p : Cli.Parsed) : IO UInt32 := do p.printError "error: aggregate requires --ixes " return 1 - let view ← match Ix.Cli.CheckCmd.parseIxesManifest + let rawView ← match Ix.Cli.CheckCmd.parseIxesManifest (← IO.FS.readBinFile manifestPath) with | .error e => IO.eprintln s!"manifest parse failed: {e}"; return 1 | .ok view => pure view let env ← match Ixon.deEnvAnon (← IO.FS.readBinFile ixePath) with | .error e => IO.eprintln s!"deserialize {ixePath} failed: {e}"; return 1 | .ok env => pure env - if !(← Ix.Cli.CheckCmd.shardsCover env view.shards) then return 1 - if view.shards.size < 2 then - IO.eprintln "aggregate currently requires at least two shards (single-shard lift packaging is not yet exposed)" - return 1 - let shardCounts := Ix.Cli.CheckCmd.ownedConstCountsForShards env view.shards - if shardCounts.any (· == 0) then - IO.eprintln "aggregate currently requires non-empty shards; regenerate or prune empty manifest leaves" - return 1 + if !(← Ix.Cli.CheckCmd.shardsCover env rawView.shards) then return 1 + let (view, shardCounts) ← match rawView.pruneEmpty env with + | .error e => IO.eprintln e; return 1 + | .ok pruned => pure pruned + let prunedCount := rawView.shards.size - view.shards.size + if prunedCount != 0 then + IO.println s!"[aggregate] pruned {prunedCount} zero-constant manifest shard(s)" let structuralAbove := ((p.flag? "structural-above").map (·.as! Nat)).getD defaultStructuralAbove let plan ← match schedulePlan view.aggregationTree.foldPlan shardCounts structuralAbove with | .error e => IO.eprintln e; return 1 | .ok plan => pure plan - printPlan plan structuralAbove + printPlan plan view.shardIds structuralAbove + let jobs := ((p.flag? "jobs").map (·.as! Nat)).getD 0 + let maxRamGb? := (p.flag? "max-ram").map (·.as! Nat) + if maxRamGb? == some 0 then + IO.eprintln "error: --max-ram must be positive" + return 1 + let ramBudgetBytes ← match maxRamGb? with + | some gib => pure (gib * aggregateGiB) + | none => defaultAggregateRamBudgetBytes + let slotWeights := aggregateSlotRamWeights plan + let jobsLabel := if jobs == 0 then "all ready slots" else toString jobs + let budgetSource := if maxRamGb?.isSome then "--max-ram" else "92% MemTotal" + IO.println s!"[aggregate] scheduler: jobs={jobsLabel}, RAM budget \ + {formatAggregateGiB ramBudgetBytes} GiB ({budgetSource}); \ + lift/structural reserve {formatAggregateGiB aggregateLiftRamBytes} GiB, \ + flat +1 MiB/subject (calibration pending)" if p.hasFlag "plan-only" then return 0 let proofHexes := (p.variableArgsAs! String).toList @@ -153,12 +766,14 @@ def runAggregateCmd (p : Cli.Parsed) : IO UInt32 := do let mut prepared : Array PreparedShard := #[] let mut digestToShard : Std.HashMap Address Nat := {} for (blocks, shard) in view.shards.mapIdx fun shard blocks => (blocks, shard) do + let originalShard := (view.shardIds[shard]?).getD shard let item ← match prepareShard env blocks with - | .error e => IO.eprintln s!"prepare shard {shard}: {e}"; return 1 + | .error e => IO.eprintln s!"prepare shard {originalShard}: {e}"; return 1 | .ok item => pure item let digest := Address.blake3 (Ix.Claim.ser item.claim) if digestToShard.contains digest then - IO.eprintln s!"duplicate reconstructed shard claim digest {digest}" + IO.eprintln s!"duplicate reconstructed shard claim digest {digest} \ + (manifest shard {originalShard})" return 1 digestToShard := digestToShard.insert digest shard prepared := prepared.push item @@ -180,11 +795,12 @@ def runAggregateCmd (p : Cli.Parsed) : IO UInt32 := do let some expected := prepared[shard]? | do IO.eprintln s!"internal: missing prepared shard {shard}" return 1 + let originalShard := (view.shardIds[shard]?).getD shard if wrapper.claim != expected.claim then - IO.eprintln s!"proof {proofAddress} hit a claim-digest collision for shard {shard}" + IO.eprintln s!"proof {proofAddress} hit a claim-digest collision for shard {originalShard}" return 1 if proofsByShard.contains shard then - IO.eprintln s!"more than one proof supplied for shard {shard}" + IO.eprintln s!"more than one proof supplied for shard {originalShard}" return 1 proofsByShard := proofsByShard.insert shard wrapper if proofsByShard.size != view.shards.size then @@ -204,104 +820,31 @@ def runAggregateCmd (p : Cli.Parsed) : IO UInt32 := do let structuralJoinIdx := recursionCompiled.getFuncIdx `join_two_structural |>.get! let ixvmSystem := Aiur.AiurSystem.build ixvmCompiled.bytecode Aiur.defaultCommitmentParameters Aiur.defaultFriParameters - let recursionSystem := Aiur.AiurSystem.build recursionCompiled.bytecode - Aiur.defaultCommitmentParameters Aiur.defaultFriParameters + let recursionSystem := MultiStark.buildRecursionSystem recursionCompiled.bytecode + recursionParameters let ixvmVk := ixvmSystem.vkBytes let recursionVk := recursionSystem.vkBytes let allowed := MultiStark.allowedBlob ixvmVk verifyIdx recursionVk liftIdx joinIdx structuralJoinIdx + let specs ← match buildAggregateSlotSpecs plan prepared ixvmVk recursionVk allowed + verifyIdx liftIdx joinIdx structuralJoinIdx recursionParameters with + | .error e => IO.eprintln s!"prepare aggregate slots: {e}"; return 1 + | .ok specs => pure specs + let cacheDir? ← if p.hasFlag "no-cache" then + IO.println "[aggregate] cache disabled (--no-cache)" + pure none + else + pure (some (← aggregateCacheDir)) - let mut slots : Array AggregateSlot := #[] - for (item, slotIdx) in plan.mapIdx fun slotIdx item => (item, slotIdx) do - match item.op with - | .leaf shard => - let some wrapper := proofsByShard.get? shard | do - IO.eprintln s!"internal: no proof for shard {shard}" - return 1 - let some preparedShard := prepared[shard]? | do - IO.eprintln s!"internal: no statement for shard {shard}" - return 1 - if preparedShard.statement.subjectCount != item.subjectCount then - IO.eprintln s!"internal: shard {shard} has {preparedShard.statement.subjectCount} \ - reconstructed subjects, but the schedule records {item.subjectCount}" - return 1 - let claimBytes := Ix.Claim.ser preparedShard.claim - let verifyInput := IxVM.ClaimHarness.packedDigestKey - (Address.blake3 claimBytes) - let innerClaim := Aiur.buildClaim verifyIdx verifyInput #[] - let innerProof := Aiur.Proof.ofBytes wrapper.proof - match ixvmSystem.verify innerClaim innerProof with - | .error e => - IO.eprintln s!"shard {shard} proof fails native verification: {e}" - return 1 - | .ok () => pure () - let innerClaimsBytes := MultiStark.serializeClaims #[innerClaim] - let pubInput := MultiStark.verifierPubInput ixvmVk innerClaimsBytes - IO.println s!"[aggregate] lifting shard {shard} into slot {slotIdx}" - (← IO.getStdout).flush - let (outerClaim, proof) := recursionSystem.proveMultiStark liftIdx pubInput - wrapper.proof ixvmVk innerClaimsBytes - slots := slots.push { - statement := preparedShard.statement - subjectCount := item.subjectCount - outerClaim - proof - openPreimages := #[innerClaimsBytes, claimBytes] - } - | .join leftIdx rightIdx => - let some left := slots[leftIdx]? | do - IO.eprintln s!"invalid aggregate plan: missing left slot {leftIdx}" - return 1 - let some right := slots[rightIdx]? | do - IO.eprintln s!"invalid aggregate plan: missing right slot {rightIdx}" - return 1 - if left.subjectCount + right.subjectCount != item.subjectCount then - IO.eprintln s!"internal: join slot {slotIdx} has inconsistent scheduled subject counts" - return 1 - let output := if item.structural then - left.statement.joinStructural right.statement - else - left.statement.join right.statement - if output.subjectCount != item.subjectCount then - IO.eprintln s!"internal: join slot {slotIdx} reconstructed {output.subjectCount} \ - subjects, but the schedule records {item.subjectCount}" - return 1 - let outputClaimBytes := Ix.Claim.ser output.claim - let pubInput := MultiStark.joinPubInput allowed outputClaimBytes - let leftClaimsBytes := MultiStark.serializeClaims #[left.outerClaim] - let rightClaimsBytes := MultiStark.serializeClaims #[right.outerClaim] - let preimagesBlob := MultiStark.joinPreimagesBlob - (left.openPreimages ++ right.openPreimages) - let trees := if item.structural then - MultiStark.CheckEnvTrees.structuralAdviceTrees - left.statement right.statement output - else - MultiStark.CheckEnvTrees.adviceTrees left.statement right.statement output - let treesBlob := MultiStark.joinTreesBlob trees - let pathsBlob := if item.structural then - MultiStark.joinPathsBlob - (MultiStark.CheckEnvTrees.structuralPathAdvice - left.statement right.statement output) - else - MultiStark.joinPathsBlob #[] - let joinFunIdx := if item.structural then structuralJoinIdx else joinIdx - let mode := if item.structural then "structural" else "flat" - IO.println s!"[aggregate] {mode}-joining slots {leftIdx}, {rightIdx} into {slotIdx}" - (← IO.getStdout).flush - let result := recursionSystem.proveMultiStarkJoin joinFunIdx pubInput - left.proof.toBytes right.proof.toBytes recursionVk - leftClaimsBytes rightClaimsBytes outputClaimBytes allowed - preimagesBlob treesBlob pathsBlob - let (outerClaim, proof) ← match result with - | .error e => IO.eprintln s!"join slot {slotIdx}: {e}"; return 1 - | .ok result => pure result - slots := slots.push { - statement := output - subjectCount := item.subjectCount - outerClaim - proof - openPreimages := #[outputClaimBytes] - } + let proveContext : AggregateProveContext := { + plan, specs, prepared, proofsByShard, shardIds := view.shardIds + ixvmSystem, recursionSystem, ixvmVk, recursionVk, allowed + verifyIdx, liftIdx, joinIdx, structuralJoinIdx, cacheDir? + } + let slots ← match ← runAggregateDag plan slotWeights jobs ramBudgetBytes + (proveAggregateSlot proveContext) true with + | .error e => IO.eprintln s!"aggregate failed: {e}"; return 1 + | .ok slots => pure slots let some root := slots.back? | do IO.eprintln "aggregate plan produced no root slot" @@ -322,28 +865,37 @@ def runAggregateCmd (p : Cli.Parsed) : IO UInt32 := do | .error e => IO.eprintln s!"aggregate root proof failed native verification: {e}"; return 1 | .ok () => pure () - let claim := root.statement.claim - let _ ← StoreIO.toIO (Store.write (Ix.Claim.ser claim)) - let wrapper : Ixon.Proof := { claim, proof := root.proof.toBytes } - let proofAddress ← StoreIO.toIO (Store.write (Ixon.Proof.ser wrapper)) + let proofAddress ← match root.proofAddress? with + | some address => pure address + | none => + let claim := root.statement.claim + let _ ← StoreIO.toIO (Store.write (Ix.Claim.ser claim)) + let wrapper : Ixon.Proof := { claim, proof := root.proof.toBytes } + StoreIO.toIO (Store.write (Ixon.Proof.ser wrapper)) IO.println s!"[aggregate] root proof: {proofAddress}" return 0 +def runAggregateCmd (p : Cli.Parsed) : IO UInt32 := + runAggregateCmdWith MultiStark.defaultRecursionParameters p + end Ix.Cli.AggregateCmd open Ix.Cli.AggregateCmd in def aggregateCmd : Cli.Cmd := `[Cli| aggregate VIA runAggregateCmd; - "Lift shard proofs and fold them into one recursive aggregate along a `.ixes` bisection tree" + "Lift shard proofs and fold multi-shard manifests into one recursive aggregate" FLAGS: "ixe" : String; "Path to the serialized environment whose shards were proven." "ixes" : String; "Path to the shard manifest; its bisection tree determines join order." "plan-only"; "Validate coverage and print the lift/join slot plan without loading or proving shard proofs." + "no-cache"; "Bypass aggregate cache reads and intermediate cache writes; the root wrapper is still persisted." + "jobs" : Nat; "Maximum aggregate slots proving concurrently (default 0: all ready slots, subject to the RAM gate)." + "max-ram" : Nat; "Aggregate in-flight RAM budget in GiB (default: 92% of MemTotal). An estimated-oversized slot runs alone." "structural-above" : Nat; "Use structural joins when a node contains more than N subject leaves (default 4096; 0 means every join)." ARGS: - ...proofs : String; "Persisted shard-proof wrapper addresses, in any order (exactly one per shard unless --plan-only)." + ...proofs : String; "Persisted shard-proof wrapper addresses, in any order (exactly one per nonempty shard unless --plan-only)." ] end diff --git a/Ix/Cli/BenchCmd.lean b/Ix/Cli/BenchCmd.lean index f43c9a932..0f7d52e8f 100644 --- a/Ix/Cli/BenchCmd.lean +++ b/Ix/Cli/BenchCmd.lean @@ -136,11 +136,13 @@ def workloadOf (testbed : String) : String := /-- The stage qualifiers a pipeline measure may carry ahead of its base name — one per pipeline stage, named for what the stage proves (`ixvm-`: the IxVM typecheck; `fri-verifier-`: the in-circuit FRI - verifier over the previous proof; the KZG stages add their own - entries as they land) — plus `pipeline-` for the whole run. Stripped + verifier over the previous proof; `join-`: the optional pair-wide + aggregate join; the KZG stages add their own entries as they land) — + plus `pipeline-` for the whole run. Stripped wherever a measure is interpreted by its base name (formatting kind, units) or labelled under a heading that already says the stage. -/ -def stagePrefixes : List String := ["ixvm-", "fri-verifier-", "pipeline-"] +def stagePrefixes : List String := + ["ixvm-", "fri-verifier-", "join-", "pipeline-"] /-- The stage qualifier `metric` carries, if any. -/ def stagePrefixOf (metric : String) : Option String := @@ -213,7 +215,9 @@ structure BackendSpec where def backendSpecs : List BackendSpec := [ -- aiur: the proof-pipeline benchmark (bench-typecheck --recursive) — - -- every stage of the pipeline, per constant, plus the total. The ixvm + -- every stage of the pipeline, per constant, plus the total. The optional + -- `bench-typecheck --join` W0 diagnostic contributes a separate pair row; + -- it is not part of the scheduled one-constant CI invocation. The ixvm -- stage proves the constant's IxVM typecheck; the fri-verifier stage -- executes the in-circuit multi-stark verifier over that fresh proof -- and proves THAT execution; the KZG stages will join as stages 3/4 @@ -245,6 +249,9 @@ def backendSpecs : List BackendSpec := [ "fri-verifier-throughput", "fri-verifier-peak-rss", "fri-verifier-proof-size", "fri-verifier-verify-time", "fri-verifier-fft-cost"]), + ("Aggregate flat join", + ["join-execute-time", "join-prove-time", "join-peak-rss", + "join-proof-size", "join-verify-time", "join-fft-cost"]), ("Pipeline total", ["total-time", "pipeline-throughput", "pipeline-peak-rss"])])], metrics := [("execute", ["execute-time", "throughput", "peak-rss", @@ -269,6 +276,12 @@ def backendSpecs : List BackendSpec := [ ("fri-verifier-prove-time", "0.10", "_"), ("ixvm-peak-rss", "0.10", "_"), ("fri-verifier-peak-rss", "0.10", "_"), + ("join-execute-time", "0.10", "_"), + ("join-prove-time", "0.10", "_"), + ("join-peak-rss", "0.10", "_"), + ("join-proof-size", "0.05", "_"), + ("join-verify-time", "0.10", "_"), + ("join-fft-cost", "0.25", "_"), ("pipeline-peak-rss", "0.10", "_"), ("ixvm-proof-size", "0.05", "_"), ("fri-verifier-proof-size", "0.05", "_"), @@ -418,6 +431,14 @@ def BackendSpec.envNames (b : BackendSpec) : List String := b.scheduledModes.any fun m => !(selectNames env b.name m).isEmpty +/-- Stable pair rows produced by the opt-in aggregate W0 diagnostic. These are + registered for dashboard filtering even though the scheduled aiur cell + remains one process per constant and therefore does not produce them. Keep + the order synchronized with the documented `bench-typecheck --join` + invocation: pair-row identity is deliberately order-sensitive. -/ +def aiurJoinBenchmarkNames : Array String := + #["Nat.add_comm + String.append"] + /-- The benchmark row names this backend uploads — the bencher slugs the dashboard plots and compare table key on — from its `inputs`: env-keyed backends key one row per compiled env; the per-constant backends select @@ -433,6 +454,8 @@ def BackendSpec.benchmarkNames (b : BackendSpec) (mode : String) : for env in b.envNames do if b.inputs == .perConstantWithEnv then ns := ns.push env ns := ns ++ (selectNames env b.name mode).map (·.name) + if b.name == "aiur" && mode == "prove" then + return ns ++ aiurJoinBenchmarkNames return ns /-- Default RAM watchdog ceiling (`--ceiling-gb` overrides): see diff --git a/Ix/Cli/BenchPlots.lean b/Ix/Cli/BenchPlots.lean index 2aa97bfff..b6e4447d8 100644 --- a/Ix/Cli/BenchPlots.lean +++ b/Ix/Cli/BenchPlots.lean @@ -70,6 +70,11 @@ def plotTitle (workload measure : String) : String := | "aiur", "fri-verifier-peak-rss" => "Aiur FRI Verifier Peak RAM Usage" | "aiur", "ixvm-proof-size" => "Aiur IxVM Proof Size" | "aiur", "fri-verifier-proof-size" => "Aiur FRI Verifier Proof Size" + | "aiur", "join-prove-time" => "Aiur Aggregate Join Time" + | "aiur", "join-fft-cost" => "Aiur Aggregate Join FFT Cost" + | "aiur", "join-verify-time" => "Aiur Aggregate Join Verify Time" + | "aiur", "join-peak-rss" => "Aiur Aggregate Join Peak RAM Usage" + | "aiur", "join-proof-size" => "Aiur Aggregate Join Proof Size" | "zisk-check-execute", "execute-time" => "Zisk Execute Time" | "zisk-check-execute", "throughput" => "Zisk Execute Throughput" | "zisk-check-execute", "peak-rss" => "Zisk Execute Peak RAM Usage" @@ -111,6 +116,7 @@ def plotSkips : List (String × String) := ("ix-decompile", "file-size"), ("ix-decompile", "constants"), ("aiur", "ixvm-peak-rss"), ("aiur", "ixvm-verify-time"), ("aiur", "ixvm-execute-time"), ("aiur", "fri-verifier-execute-time"), + ("aiur", "join-execute-time"), ("aiur", "ixvm-throughput"), ("aiur", "fri-verifier-throughput")] /-- Canonical units per measure slug, asserted on every sync: bencher diff --git a/Ix/Cli/CheckCmd.lean b/Ix/Cli/CheckCmd.lean index d26603d92..57d16a582 100644 --- a/Ix/Cli/CheckCmd.lean +++ b/Ix/Cli/CheckCmd.lean @@ -471,10 +471,25 @@ where let (rightIdx, ops) := go right ops (ops.size, ops.push (.join leftIdx rightIdx)) +/-- Drop removed shard leaves, contract unary nodes, and rewrite retained shard +ids to their dense indices in a pruned manifest view. The input tree has +already passed `validateAggregationTree`, so an out-of-range mapping entry is +an internal inconsistency rather than untrusted manifest input. -/ +partial def pruneAndRemap (remap : Array (Option Nat)) : + AggregationTree → Option AggregationTree + | .leaf shard => (remap[shard]?).join.map .leaf + | .node left right => + match pruneAndRemap remap left, pruneAndRemap remap right with + | some left, some right => some (.node left right) + | some tree, none | none, some tree => some tree + | none, none => none + end AggregationTree structure IxesManifestView where shards : Array (Array Address) + /-- Original manifest shard id for each (possibly pruned) dense array slot. -/ + shardIds : Array Nat aggregationTree : AggregationTree deriving BEq, Repr @@ -545,7 +560,7 @@ def parseIxesManifest (bytes : ByteArray) : Except String IxesManifestView := let (buffer, position) ← get if position != buffer.size then throw s!"ixes: {buffer.size - position} trailing bytes after aggregation tree" - pure { shards, aggregationTree := tree } + pure { shards, shardIds := Array.range n.toNat, aggregationTree := tree } go.run' (bytes, 0) /-- Backward-compatible shard-only view used by check/prove/verify paths that @@ -595,11 +610,42 @@ def ownedConstCountsForShards (ixonEnv : Ixon.Env) counts := counts.modify shard (· + 1) return counts +/-- Remove manifest shards that provably own no environment constants, then +contract and densely reindex the corresponding aggregation-tree leaves. + +Callers must run `shardsCover` on the unpruned view first. That gate establishes +that every constant is owned exactly once; the zero counts here therefore prove +that dropping these leaves cannot omit a checked subject. `shardIds` preserves +the original ids for diagnostics and for matching legacy manifests. -/ +def IxesManifestView.pruneEmpty (view : IxesManifestView) + (ixonEnv : Ixon.Env) : Except String (IxesManifestView × Array Nat) := do + if view.shards.size != view.shardIds.size then + throw "ixes: internal shard/id cardinality mismatch" + let counts := ownedConstCountsForShards ixonEnv view.shards + let mut remap : Array (Option Nat) := Array.replicate view.shards.size none + let mut shards : Array (Array Address) := #[] + let mut shardIds : Array Nat := #[] + let mut keptCounts : Array Nat := #[] + for (count, oldIdx) in counts.mapIdx fun oldIdx count => (count, oldIdx) do + if count != 0 then + let some blocks := view.shards[oldIdx]? + | throw s!"ixes: internal missing shard {oldIdx}" + let some originalId := view.shardIds[oldIdx]? + | throw s!"ixes: internal missing shard id {oldIdx}" + remap := remap.set! oldIdx (some shards.size) + shards := shards.push blocks + shardIds := shardIds.push originalId + keptCounts := keptCounts.push count + let some aggregationTree := view.aggregationTree.pruneAndRemap remap + | throw "aggregate: manifest has no shard owning an environment constant" + pure ({ shards, shardIds, aggregationTree }, keptCounts) + /-- 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) + let (claim, _) ← IxVM.ClaimHarness.shardCheckEnvClaimTrees ixonEnv + (ownedConstsForBlocks ixonEnv blocks) pure (Address.blake3 (Ix.Claim.ser claim)) /-- Load the `.ixe` env and the `.ixes` shard partition together (each file diff --git a/Ix/Cli/VerifyCmd.lean b/Ix/Cli/VerifyCmd.lean index a6490adfb..ff410f780 100644 --- a/Ix/Cli/VerifyCmd.lean +++ b/Ix/Cli/VerifyCmd.lean @@ -83,22 +83,27 @@ def buildBackend : IO (Except String (Aiur.AiurSystem × Aiur.CompiledToplevel)) structure AggregateBackend where system : Aiur.AiurSystem + ixvmVk : ByteArray + verifyClaimIdx : Aiur.Bytecode.FunIdx + liftIdx : Aiur.Bytecode.FunIdx flatJoinIdx : Aiur.Bytecode.FunIdx structuralJoinIdx : Aiur.Bytecode.FunIdx allowed : ByteArray inductive AggregateRootKind where + | lift | flat | structural deriving BEq, Repr structure ExpectedAggregate where claim : Ix.Claim - kind : AggregateRootKind + kinds : Array AggregateRootKind /-- Build the two deterministic systems whose identities are committed by an aggregate root: the IxVM vk and the combined lift/join recursion vk. -/ -private def buildAggregateBackend : +private def buildAggregateBackend + (recursionParameters : MultiStark.RecursionParameters) : IO (Except String AggregateBackend) := do let ixvmCompiled ← match IxVM.ixVM with | .error e => return .error s!"IxVM toplevel merging failed: {e}" @@ -116,13 +121,17 @@ private def buildAggregateBackend : let structuralJoinIdx := recursionCompiled.getFuncIdx `join_two_structural |>.get! let ixvmSystem := Aiur.AiurSystem.build ixvmCompiled.bytecode commitmentParameters friParameters - let recursionSystem := Aiur.AiurSystem.build recursionCompiled.bytecode - commitmentParameters friParameters + let recursionSystem := MultiStark.buildRecursionSystem recursionCompiled.bytecode + recursionParameters + let ixvmVk := ixvmSystem.vkBytes let recursionVk := recursionSystem.vkBytes - let allowed := MultiStark.allowedBlob ixvmSystem.vkBytes verifyIdx + let allowed := MultiStark.allowedBlob ixvmVk verifyIdx recursionVk liftIdx joinIdx structuralJoinIdx return .ok { system := recursionSystem + ixvmVk + verifyClaimIdx := verifyIdx + liftIdx flatJoinIdx := joinIdx structuralJoinIdx allowed @@ -131,19 +140,16 @@ private def buildAggregateBackend : private def shardStatement (env : Ixon.Env) (blocks : Array Address) : Except String MultiStark.CheckEnvTrees := do let owned := Ix.Cli.CheckCmd.ownedConstsForBlocks env blocks - let (claim, _, trees) ← IxVM.ClaimHarness.shardCheckEnvClaim env owned + let (claim, trees) ← IxVM.ClaimHarness.shardCheckEnvClaimTrees env owned MultiStark.CheckEnvTrees.ofClaim claim trees -/-- Reproduce the hybrid flat/structural statement fold from the manifest. -The threshold schedule is shared with `ix aggregate`; no proof data is needed. -/ -private def expectedFromManifest (env : Ixon.Env) +/-- Reproduce the lift/flat/structural statement fold from a coverage-validated +manifest. Zero-constant leaves are pruned exactly as in `ix aggregate`; no proof +data is needed. -/ +def expectedFromManifest (env : Ixon.Env) (view : Ix.Cli.CheckCmd.IxesManifestView) (structuralAbove : Nat) : Except String (MultiStark.CheckEnvTrees × AggregateRootKind) := do - if view.shards.size < 2 then - throw "aggregate verification requires a manifest with at least two shards" - let counts := Ix.Cli.CheckCmd.ownedConstCountsForShards env view.shards - if counts.any (· == 0) then - throw "aggregate verification requires non-empty shards" + let (view, counts) ← view.pruneEmpty env let plan ← Ix.Cli.AggregateCmd.schedulePlan view.aggregationTree.foldPlan counts structuralAbove let mut slots : Array MultiStark.CheckEnvTrees := #[] @@ -164,10 +170,29 @@ private def expectedFromManifest (env : Ixon.Env) leftStatement.join rightStatement let some root := slots.back? | throw "aggregate manifest produced no root" let some rootPlan := plan.back? | throw "aggregate manifest produced no root slot" - pure (root, if rootPlan.structural then .structural else .flat) + let kind := match rootPlan.op with + | .leaf _ => AggregateRootKind.lift + | .join _ _ => if rootPlan.structural then .structural else .flat + pure (root, kind) + +/-- Reconstruct the exact outer claim of a single-shard lift from the bundled +`CheckEnv` statement. This is the verification-side inverse of the leaf arm in +`ix aggregate`: the wrapper claim determines the nested IxVM `verify_claim`, +whose serialized singleton list determines the lift public input. -/ +def aggregateLiftOuterClaim (ixvmVk : ByteArray) + (verifyClaimIdx liftIdx : Aiur.Bytecode.FunIdx) (claim : Ix.Claim) : Array Aiur.G := + let claimBytes := Ix.Claim.ser claim + let verifyInput := IxVM.ClaimHarness.packedDigestKey (Address.blake3 claimBytes) + let innerClaim := Aiur.buildClaim verifyClaimIdx verifyInput #[] + let innerClaimsBytes := MultiStark.serializeClaims #[innerClaim] + Aiur.buildClaim liftIdx (MultiStark.verifierPubInput ixvmVk innerClaimsBytes) #[] + +private def aggregateRootKindLabel : AggregateRootKind → String + | .lift => "lift" + | .flat => "flat" + | .structural => "structural" -private def verifyAggregateProof (recursionSystem : Aiur.AiurSystem) - (flatJoinIdx structuralJoinIdx : Aiur.Bytecode.FunIdx) (allowed : ByteArray) +private def verifyAggregateProof (backend : AggregateBackend) (expected? : Option ExpectedAggregate) (proofAddr : Address) : IO UInt32 := do let wrapper ← IO.ofExcept (Ixon.Proof.de (← StoreIO.toIO (Store.read proofAddr))) let .checkEnv _ _ := wrapper.claim | do @@ -179,32 +204,28 @@ private def verifyAggregateProof (recursionSystem : Aiur.AiurSystem) IO.eprintln s!"error: aggregate claim {wrapper.claim} does not match expected {expected.claim}" return 1 | none => pure () - let claimBytes := Ix.Claim.ser wrapper.claim - let pubInput := MultiStark.joinPubInput allowed claimBytes let proof := Aiur.Proof.ofBytes wrapper.proof - let verifyAt (idx : Aiur.Bytecode.FunIdx) := - recursionSystem.verify (Aiur.buildClaim idx pubInput #[]) proof - let result : Except String AggregateRootKind := match expected? with - | some expected => - let idx := match expected.kind with - | .flat => flatJoinIdx - | .structural => structuralJoinIdx - (verifyAt idx).map fun _ => expected.kind - | none => - match verifyAt flatJoinIdx with - | .ok () => .ok .flat - | .error flatError => match verifyAt structuralJoinIdx with - | .ok () => .ok .structural - | .error structuralError => .error - s!"flat join: {flatError}; structural join: {structuralError}" - match result with - | .error e => - IO.eprintln s!"error: aggregate verification failed: {e}" - return 1 - | .ok kind => - let label := match kind with | .flat => "flat" | .structural => "structural" - IO.println s!"ok: {label} aggregate proof {proofAddr} verifies {wrapper.claim}" - return 0 + let claimBytes := Ix.Claim.ser wrapper.claim + let joinPubInput := MultiStark.joinPubInput backend.allowed claimBytes + let outerClaim : AggregateRootKind → Array Aiur.G + | .lift => aggregateLiftOuterClaim backend.ixvmVk backend.verifyClaimIdx + backend.liftIdx wrapper.claim + | .flat => Aiur.buildClaim backend.flatJoinIdx joinPubInput #[] + | .structural => Aiur.buildClaim backend.structuralJoinIdx joinPubInput #[] + let kinds := expected?.map (·.kinds) |>.getD + #[.lift, .flat, .structural] + let mut errors : Array String := #[] + for kind in kinds do + match backend.system.verify (outerClaim kind) proof with + | .ok () => + IO.println s!"ok: {aggregateRootKindLabel kind} aggregate proof \ + {proofAddr} verifies {wrapper.claim}" + return 0 + | .error e => + errors := errors.push s!"{aggregateRootKindLabel kind}: {e}" + IO.eprintln s!"error: aggregate verification failed: \ + {String.intercalate "; " errors.toList}" + return 1 /-- Shard-aware verification (parity with `check`/`prove`): - `--shard K`, no proof: print shard K's reconstructed `CheckEnv` claim @@ -273,7 +294,10 @@ def verifyShardComposition (ixePath manifestPath : String) (shardK? : Option Nat IO.println s!"[verify] OK: composed verdict — all {shards.size} shards proven + disjoint cover" return rc -def runVerifyCmd (p : Cli.Parsed) : IO UInt32 := do +/-- Verify with an explicit aggregate-recursion configuration. Ordinary IxVM +proof verification remains pinned to its independent canonical parameters. -/ +def runVerifyCmdWith (recursionParameters : MultiStark.RecursionParameters) + (p : Cli.Parsed) : IO UInt32 := do let proofs := (p.variableArgsAs! String).toList if p.hasFlag "aggregate" then if proofs.isEmpty then @@ -297,7 +321,7 @@ def runVerifyCmd (p : Cli.Parsed) : IO UInt32 := do return 1 pure (some { claim := .checkEnv expectedTree.root none - kind := .flat + kinds := #[.lift, .flat] }) | some ixePath, some manifestPath => let env ← match Ixon.deEnvAnon (← IO.FS.readBinFile ixePath) with @@ -315,16 +339,15 @@ def runVerifyCmd (p : Cli.Parsed) : IO UInt32 := do IO.eprintln s!"error: expected aggregate root retains assumptions \ {statement.assumptions.map (·.root)}" return 1 - pure (some { claim := statement.claim, kind }) + pure (some { claim := statement.claim, kinds := #[kind] }) | none, some _ => unreachable! - let backend ← match ← buildAggregateBackend with + let backend ← match ← buildAggregateBackend recursionParameters with | .error e => IO.eprintln e; return 1 | .ok backend => pure backend let mut rc : UInt32 := 0 for hex in proofs do let proofAddr ← addrOfHex! "aggregate proof" hex - if (← verifyAggregateProof backend.system backend.flatJoinIdx - backend.structuralJoinIdx backend.allowed expected? proofAddr) != 0 then + if (← verifyAggregateProof backend expected? proofAddr) != 0 then rc := 1 return rc match (p.flag? "ixe").map (·.as! String), (p.flag? "ixes").map (·.as! String) with @@ -343,6 +366,9 @@ def runVerifyCmd (p : Cli.Parsed) : IO UInt32 := do if (← verifyOneProof aiurSystem compiled proofAddr) != 0 then rc := 1 return rc +def runVerifyCmd (p : Cli.Parsed) : IO UInt32 := + runVerifyCmdWith MultiStark.defaultRecursionParameters p + end Ix.Cli.VerifyCmd open Ix.Cli.VerifyCmd in @@ -354,7 +380,7 @@ def verifyCmd : Cli.Cmd := `[Cli| "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). For aggregate roots, reproduces the manifest-relative hybrid structural root." "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." - "aggregate"; "Interpret proof arguments as aggregate-first recursive roots. With --ixe alone, expects an all-flat canonical root; add --ixes for hybrid structural roots." + "aggregate"; "Interpret proofs as aggregate-first roots. With --ixe alone, accepts a single lift or all-flat canonical root; add --ixes for the exact lift/flat/structural manifest root." "structural-above" : Nat; "For --aggregate + --ixes, reproduce structural joins above N subject leaves (default 4096; must match proving)." ARGS: diff --git a/Ix/IxVM/ClaimHarness.lean b/Ix/IxVM/ClaimHarness.lean index 4af4cd798..3ff64c994 100644 --- a/Ix/IxVM/ClaimHarness.lean +++ b/Ix/IxVM/ClaimHarness.lean @@ -400,7 +400,13 @@ composition of per-piece check-env claims" return { funcName := `verify_claim input := digestKey, inputIOBuffer := ioBuffer } -/-- the kernel shard claim with a THIN frontier: asm = the DIRECT out-of-owned +/-- The kernel shard claim and its canonical subject/assumption trees, without + constructing the witness byte closure. This is the claim-only path used by + aggregation and verification: those callers need the Merkle trees but do + not consume the dependency bytes, so walking the full closure would be + pure discarded work. + + The frontier is THIN: asm = the DIRECT out-of-owned walk edges (refs + Prj→block) of the owned constants, not the full `closure ∖ owned`. the kernel's env walk exits the shard only through a direct external edge and stops there, so everything below the first @@ -412,15 +418,9 @@ composition of per-piece check-env claims" from `env.consts` is not something the kernel walk can reach, so including it would inflate the asm tree and break digest agreement between the Rust prover and this verifier. -/ -def shardCheckEnvClaim (env : Ixon.Env) (owned : Array Address) : - Except String (Ix.Claim × Std.HashSet Address × Std.HashMap Address Ix.AssumptionTree) := do +def shardCheckEnvClaimTrees (env : Ixon.Env) (owned : Array Address) : + Except String (Ix.Claim × 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 := Id.run do let mut fs : Std.HashSet Address := {} for o in owned do @@ -457,10 +457,22 @@ def shardCheckEnvClaim (env : Ixon.Env) (owned : Array Address) : match asmTree? with | some asmTree => trees := trees.insert asmTree.root asmTree | none => pure () + pure (claim, trees) + +/-- Claim/tree construction plus the byte closure needed by a Lean-built shard + witness. Reachability distributes over root union, so one graph walk from + all owned and primitive roots is exactly the old union of one + `closureFrom` walk per owned constant, without repeatedly traversing the + same shared dependency core. -/ +def shardCheckEnvClaim (env : Ixon.Env) (owned : Array Address) : + Except String (Ix.Claim × Std.HashSet Address × Std.HashMap Address Ix.AssumptionTree) := do + let (claim, trees) ← shardCheckEnvClaimTrees env owned + let primitiveRoots := Ix.Tc.primAddrSet.toArray.filter env.consts.contains + let closure := closureFromRoots env (owned ++ primitiveRoots) pure (claim, closure, trees) /-- Variant of `buildShardCheckEnvWitness`: THIN frontier asm (see - `shardCheckEnvClaim`) with the `closureFrom` byte scope, which + `shardCheckEnvClaimTrees`) with the `closureFrom` byte scope, which carries the IPrj/CPrj/RPrj/DPrj wrappers the kernel's `get_ci` synthesizes via kernel-side blake3 as forward Muts→wrapper edges. -/ def buildShardCheckEnvWitness (env : Ixon.Env) (owned : Array Address) : diff --git a/Ix/MultiStark.lean b/Ix/MultiStark.lean index ba5be06fa..47f02a47d 100644 --- a/Ix/MultiStark.lean +++ b/Ix/MultiStark.lean @@ -132,6 +132,46 @@ digest-bound. These helpers are that recipe's single home. -/ def u64le (n : Nat) : Array UInt8 := (Array.range 8).map (fun i => UInt8.ofNat ((n >>> (8 * i)) % 256)) +/-! ## Recursion proof parameters + +IxVM proofs and aggregate recursion proofs deliberately have separate host +configuration, even while both configurations retain today's canonical values. +Keeping the recursion pair here gives aggregation and aggregate verification a +single construction path; a later policy change cannot silently update only one +side. +-/ + +/-- Commitment and FRI parameters for lift/join proofs. These parameters are +already bound by `AiurSystem.vkBytes`; this structure is host configuration, not +an additional circuit public input. -/ +structure RecursionParameters where + commitment : Aiur.CommitmentParameters + fri : Aiur.FriParameters + +/-- Compatibility default for aggregate recursion proofs. Policy changes (for +example, reducing the query count) must be explicit updates to this value and +must not change the canonical IxVM proof parameters. -/ +def defaultRecursionParameters : RecursionParameters := { + commitment := Aiur.defaultCommitmentParameters + fri := Aiur.defaultFriParameters +} + +/-- Stable 40-byte serialization used as the `fri_params_ser` component of the +future aggregate cache key: five `u64` little-endian fields in verifying-key +order. Commitment parameters need no separate cache-key component because a +change to them changes the recursion-vk digest that the key also contains. -/ +def RecursionParameters.cacheFriBytes (parameters : RecursionParameters) : ByteArray := + let fri := parameters.fri + ⟨u64le fri.logFinalPolyLen ++ u64le fri.maxLogArity ++ + u64le fri.numQueries ++ u64le fri.commitProofOfWorkBits ++ + u64le fri.queryProofOfWorkBits⟩ + +/-- Build a recursion proving/verifying system through the shared aggregate +parameter path. Both `AggregateCmd` and `VerifyCmd` use this helper. -/ +def buildRecursionSystem (bytecode : Aiur.Bytecode.Toplevel) + (parameters : RecursionParameters) : Aiur.AiurSystem := + Aiur.AiurSystem.build bytecode parameters.commitment parameters.fri + /-- Serialize public claims to `read_claims`'s wire format (which is also what the prover's Fiat-Shamir transcript observes): a length-prefixed list of length-prefixed claims, every word a little-endian `u64`. -/ diff --git a/Ix/Store.lean b/Ix/Store.lean index 08c323be4..50a6155a8 100644 --- a/Ix/Store.lean +++ b/Ix/Store.lean @@ -38,6 +38,16 @@ def storeDir : StoreIO FilePath := do IO.toEIO .ioError (IO.FS.createDirAll path) return path +/-- `~/.ix/cache/` holds wipeable, keyed indexes into the +content-addressed store. Unlike `storeDir`, filenames here are caller-defined +lookup keys and their contents must always be treated as untrusted hints. -/ +def cacheDir (namespace' : String) : StoreIO FilePath := do + let home ← getHomeDir + let path := home / ".ix" / "cache" / namespace' + if !(<- path.pathExists) then + IO.toEIO .ioError (IO.FS.createDirAll path) + return path + def storePath (addr: Address): StoreIO FilePath := do let store <- storeDir let hex := hexOfBytes addr.hash diff --git a/Tests/Ix/BenchMeasures.lean b/Tests/Ix/BenchMeasures.lean index 7a83e6276..7b2fffdf0 100644 --- a/Tests/Ix/BenchMeasures.lean +++ b/Tests/Ix/BenchMeasures.lean @@ -25,6 +25,9 @@ def testStagePrefix : TestSeq := (stagePrefixOf "ixvm-verify-time" == some "ixvm-") ++ test "fri-verifier- prefix identified" (stagePrefixOf "fri-verifier-fft-cost" == some "fri-verifier-") + ++ test "join- strips" (dropStagePrefix "join-proof-size" == "proof-size") + ++ test "join- prefix identified" + (stagePrefixOf "join-execute-time" == some "join-") ++ test "unqualified name passes through" (dropStagePrefix "execute-time" == "execute-time") ++ test "prefix without dash is not a qualifier" @@ -34,6 +37,10 @@ def testStagePrefix : TestSeq := ++ test "phase spans pass through" (dropStagePrefix "phase-stark-stage1-commit" == "phase-stark-stage1-commit") + ++ test "aiur join pair is registered for dashboard filtering" + ((backendSpecs.find? (·.name == "aiur")).any fun backend => + (backend.benchmarkNames "prove").contains + "Nat.add_comm + String.append") def suite : List TestSeq := [testStagePrefix] diff --git a/Tests/Main.lean b/Tests/Main.lean index b96e2735e..15e7eb94a 100644 --- a/Tests/Main.lean +++ b/Tests/Main.lean @@ -53,6 +53,7 @@ import Tests.Ix.CondenseM import Tests.FFI import Tests.Keccak import Tests.MultiStark +import Tests.MultiStarkActivation import Tests.Cli import Tests.ShardMap import Tests.Ix.EnvBody @@ -318,6 +319,12 @@ def main (args : List String) : IO UInt32 := do if args.contains "cli" then return ← Tests.Cli.suite + -- Section 13 WP-D diagnostic: keep the 98-case, twice-executed activation + -- matrix out of the default primary suite while making its gate explicit and + -- independent of the large compiled Lean environment used by ignored tests. + if args.contains "aggregate-activation" then + return ← Tests.MultiStark.activationAudit + let runIgnored := args.contains "--ignored" let includeIgnored := args.contains "--include-ignored" -- `--exclude=a,b,c` drops named ignored suites and runners from an unfiltered sweep. diff --git a/Tests/MultiStark.lean b/Tests/MultiStark.lean index 942e0f69b..a40acd77d 100644 --- a/Tests/MultiStark.lean +++ b/Tests/MultiStark.lean @@ -7,6 +7,7 @@ public import Ix.Aiur.Compiler public import Ix.MultiStark public import Ix.Cli.AggregateCmd public import Ix.Cli.CheckCmd +public import Ix.Cli.VerifyCmd public import Ix.Claim public import Ix.AssumptionTree public import Ix.Merkle @@ -240,13 +241,33 @@ proving the full recursive verifier (the production lift needs tens of GiB). The join still verifies two real Multi-STARK proofs and enforces their vk, entrypoint, public-input, and nested-claim bindings. -/ def joinChildProgram : Source.Toplevel := ⟦ - pub fn fake_verify_claim(_digest: [G; 8]) { () } - pub fn fake_lift(_system_digest: [G; 8], _claims_digest: [G; 8]) { () } + fn activation_height_probe(n: G) { + match n { + 0 => (), + _ => activation_height_probe(n - 1), + } + } + + fn activation_vary_height(digest: [G; 8]) { + match u32_less_than(digest[0], digest[1]) { + 1 => activation_height_probe(1), + _ => activation_height_probe(4), + } + } + + pub fn fake_verify_claim(digest: [G; 8]) { + activation_vary_height(digest) + } + pub fn fake_lift(system_digest: [G; 8], _claims_digest: [G; 8]) { + activation_vary_height(system_digest) + } pub fn fake_join(allowed_digest: [G; 8], _out_claim_digest: [G; 8]) { + activation_vary_height(allowed_digest); assert_eq!(load(store(allowed_digest[0])), allowed_digest[0]); () } pub fn fake_struct_join(allowed_digest: [G; 8], _out_claim_digest: [G; 8]) { + activation_vary_height(allowed_digest); assert_eq!(load(store(allowed_digest[1])), allowed_digest[1]); assert_eq!(load(store(allowed_digest[2])), allowed_digest[2]); () @@ -259,11 +280,42 @@ private def bytesAsGs (bytes : ByteArray) : Array Aiur.G := private def u32le4 (n : Nat) : Array UInt8 := (Array.range 4).map fun i => UInt8.ofNat ((n >>> (8 * i)) % 256) -private def minimalIxes (treeTail : Array UInt8) : ByteArray := - let shard := fun id => u32le4 id ++ Array.replicate 24 0 ++ #[0] ++ - u32le4 0 ++ u32le4 0 +private def minimalIxesFor (shards : Array (Array Address)) + (treeTail : Array UInt8) : ByteArray := + let putAddresses := fun (addresses : Array Address) => + addresses.foldl (fun out address => out ++ address.hash.data) + (u32le4 addresses.size) + let shard := fun id blocks => u32le4 id ++ Array.replicate 24 0 ++ #[0] ++ + putAddresses blocks ++ u32le4 0 + let body := (shards.mapIdx shard).foldl (· ++ ·) #[] ⟨#[0x49, 0x58, 0x45, 0x53, 0, 0, 0, 0] ++ Array.replicate 16 0 ++ - u32le4 2 ++ shard 0 ++ shard 1 ++ treeTail⟩ + u32le4 shards.size ++ body ++ treeTail⟩ + +private def minimalIxes (treeTail : Array UInt8) : ByteArray := + minimalIxesFor #[#[], #[]] treeTail + +private def singletonIxonEnv : Ixon.Env × Address := + let constant : Ixon.Constant := + ⟨.axio ⟨false, 0, .sort 0⟩, #[], #[], #[.succ .zero]⟩ + let address := Address.blake3 (Ixon.serConstant constant) + (({} : Ixon.Env).storeConst address constant, address) + +/-- Two owned constants with one shared dependency. This is the shape that made +the old shard preparation path repeatedly traverse the same large core. -/ +private def sharedClosureIxonEnv : Ixon.Env × Array Address × Address := + let shared : Ixon.Constant := + ⟨.axio ⟨false, 0, .sort 0⟩, #[], #[], #[.succ .zero]⟩ + let sharedAddress := Address.blake3 (Ixon.serConstant shared) + let left : Ixon.Constant := + ⟨.axio ⟨false, 0, .ref 0 #[]⟩, #[], #[sharedAddress], #[]⟩ + let right : Ixon.Constant := + ⟨.axio ⟨true, 0, .ref 0 #[]⟩, #[], #[sharedAddress], #[]⟩ + let leftAddress := Address.blake3 (Ixon.serConstant left) + let rightAddress := Address.blake3 (Ixon.serConstant right) + let env := (({} : Ixon.Env).storeConst sharedAddress shared) + |>.storeConst leftAddress left + |>.storeConst rightAddress right + (env, #[leftAddress, rightAddress], sharedAddress) private def canonicalTree (leaves : Array Address) : Ix.AssumptionTree := (Ix.AssumptionTree.canonical leaves).get! @@ -281,6 +333,40 @@ def joinSmokeSuite : IO UInt32 := do | .error e => IO.eprintln s!"join child compilation failed: {e}"; return 1 | .ok c => pure c let childSystem := AiurSystem.build childCompiled.bytecode recCommitParams innerFri + + -- Pin the new recursion-parameter seam before exercising the join protocol. + -- The default helper must reproduce the former direct construction exactly; + -- the stable FRI bytes are the future cache-key component from the plan. + let recursionDefaults := MultiStark.defaultRecursionParameters + let defaultRecursionSystem := + MultiStark.buildRecursionSystem childCompiled.bytecode recursionDefaults + let legacyDefaultRecursionSystem := AiurSystem.build childCompiled.bytecode + Aiur.defaultCommitmentParameters Aiur.defaultFriParameters + let expectedDefaultFriBytes : ByteArray := + ⟨u64le 0 ++ u64le 1 ++ u64le 100 ++ u64le 0 ++ u64le 20⟩ + let tunedFri : Aiur.FriParameters := + { recursionDefaults.fri with numQueries := 50 } + let tunedFriParameters : MultiStark.RecursionParameters := + { recursionDefaults with fri := tunedFri } + let tunedFriSystem := + MultiStark.buildRecursionSystem childCompiled.bytecode tunedFriParameters + let tunedCommitment : Aiur.CommitmentParameters := + { recursionDefaults.commitment with logBlowup := 3 } + let tunedCommitmentParameters : MultiStark.RecursionParameters := + { recursionDefaults with commitment := tunedCommitment } + let tunedCommitmentSystem := + MultiStark.buildRecursionSystem childCompiled.bytecode tunedCommitmentParameters + let defaultRecursionIdentityPreserved := + defaultRecursionSystem.vkBytes == legacyDefaultRecursionSystem.vkBytes + let defaultFriEncodingStable := + recursionDefaults.cacheFriBytes.size == 40 && + recursionDefaults.cacheFriBytes == expectedDefaultFriBytes + let recursionParametersIndependent := + tunedFriParameters.cacheFriBytes != recursionDefaults.cacheFriBytes && + tunedFriSystem.vkBytes != defaultRecursionSystem.vkBytes && + tunedCommitmentParameters.cacheFriBytes == recursionDefaults.cacheFriBytes && + tunedCommitmentSystem.vkBytes != defaultRecursionSystem.vkBytes + let verifyIdx := childCompiled.getFuncIdx `fake_verify_claim |>.get! let liftIdx := childCompiled.getFuncIdx `fake_lift |>.get! let childJoinIdx := childCompiled.getFuncIdx `fake_join |>.get! @@ -328,8 +414,121 @@ def joinSmokeSuite : IO UInt32 := do let recursionVk := childSystem.vkBytes let allowed := MultiStark.allowedBlob fakeIxvmVk verifyIdx recursionVk liftIdx childJoinIdx childStructuralJoinIdx + let childRecursionParameters : MultiStark.RecursionParameters := { + commitment := recCommitParams + fri := innerFri + } + let liftCacheKey := Ix.Cli.AggregateCmd.aggregateCacheKey recursionVk + childRecursionParameters leftOuter + let cacheKeyInputsBound := + liftCacheKey == Ix.Cli.AggregateCmd.aggregateCacheKey recursionVk + childRecursionParameters leftOuter && + liftCacheKey != Ix.Cli.AggregateCmd.aggregateCacheKey recursionVk + childRecursionParameters rightOuter && + liftCacheKey != Ix.Cli.AggregateCmd.aggregateCacheKey recursionVk + { childRecursionParameters with fri := tunedFri } leftOuter && + liftCacheKey != Ix.Cli.AggregateCmd.aggregateCacheKey + (recursionVk.set! 0 (recursionVk.data[0]! + 1)) + childRecursionParameters leftOuter && + liftCacheKey != Ix.Cli.AggregateCmd.aggregateCacheKey recursionVk + childRecursionParameters leftOuter + (Ix.Cli.AggregateCmd.aggregateCacheVersion + 1) + let cachedLiftWrapper : Ixon.Proof := { + claim := leftStatement.claim + proof := leftProof.toBytes + } + let validCachedLift := Ix.Cli.AggregateCmd.validateAggregateCacheWrapper + childSystem leftStatement.claim leftOuter cachedLiftWrapper + let wrongCachedStatement := Ix.Cli.AggregateCmd.validateAggregateCacheWrapper + childSystem rightStatement.claim leftOuter cachedLiftWrapper + let wrongCachedOuterClaim := Ix.Cli.AggregateCmd.validateAggregateCacheWrapper + childSystem leftStatement.claim rightOuter cachedLiftWrapper + let badCachedProofBytes := leftProof.toBytes.set! 0 + (UInt8.ofNat ((leftProof.toBytes.data[0]!.toNat + 1) % 256)) + let badCachedProof := Ix.Cli.AggregateCmd.validateAggregateCacheWrapper + childSystem leftStatement.claim leftOuter + { cachedLiftWrapper with proof := badCachedProofBytes } + + -- Exercise the wipeable index hermetically. Its content is only an address; + -- wrapper binding and cryptographic validity are checked above. + let cacheRoot ← IO.FS.createTempDir + let cacheDir ← Ix.Cli.AggregateCmd.aggregateCacheDir (some cacheRoot) + let missingCacheEntry ← + Ix.Cli.AggregateCmd.readAggregateCacheAddress cacheDir liftCacheKey + let cachedLiftAddress := Address.blake3 (Ixon.Proof.ser cachedLiftWrapper) + Ix.Cli.AggregateCmd.writeAggregateCacheAddress cacheDir liftCacheKey + cachedLiftAddress + let presentCacheEntry ← + Ix.Cli.AggregateCmd.readAggregateCacheAddress cacheDir liftCacheKey + let tempEntryExists ← (cacheDir / s!"{liftCacheKey}.tmp").pathExists + let tempEntryGone := !tempEntryExists + IO.FS.writeFile (cacheDir / toString liftCacheKey) "corrupt-cache-entry" + let corruptCacheEntry ← + Ix.Cli.AggregateCmd.readAggregateCacheAddress cacheDir liftCacheKey + Ix.Cli.AggregateCmd.writeAggregateCacheAddress cacheDir liftCacheKey + cachedLiftAddress + let recoveredCacheEntry ← + Ix.Cli.AggregateCmd.readAggregateCacheAddress cacheDir liftCacheKey + let cacheIndexRoundTrip : Bool := match missingCacheEntry, presentCacheEntry with + | .miss, .hit address => address == cachedLiftAddress && tempEntryGone + | _, _ => false + let corruptCacheIndexRejected : Bool := match corruptCacheEntry with + | .invalid _ => true + | _ => false + let corruptCacheIndexRecovers : Bool := match recoveredCacheEntry with + | .hit address => address == cachedLiftAddress + | _ => false + + let reconstructedLiftClaim := + Ix.Cli.VerifyCmd.aggregateLiftOuterClaim fakeIxvmVk verifyIdx liftIdx + leftStatement.claim + let liftClaimReconstruction := reconstructedLiftClaim == leftOuter + let reconstructedLiftVerifies := + childSystem.verify reconstructedLiftClaim leftProof let outputClaimBytes := Ix.Claim.ser outputStatement.claim let pubInput := MultiStark.joinPubInput allowed outputClaimBytes + let cachePlan : Array Ix.Cli.AggregateCmd.ScheduledFold := #[ + { op := .leaf 0, subjectCount := 2, structural := false }, + { op := .leaf 1, subjectCount := 1, structural := false }, + { op := .join 0 1, subjectCount := 3, structural := false } + ] + let cachePrepared : Array Ix.Cli.AggregateCmd.PreparedShard := #[ + { claim := leftStatement.claim, statement := leftStatement }, + { claim := rightStatement.claim, statement := rightStatement } + ] + let cacheSpecs := Ix.Cli.AggregateCmd.buildAggregateSlotSpecs cachePlan + cachePrepared fakeIxvmVk recursionVk allowed verifyIdx liftIdx childJoinIdx + childStructuralJoinIdx childRecursionParameters + let cacheSpecsComplete : Bool := match cacheSpecs with + | .ok specs => match specs[0]?, specs[1]?, specs[2]? with + | some left, some right, some root => + specs.size == 3 && left.outerClaim == leftOuter && + right.outerClaim == rightOuter && + root.statement.claim == outputStatement.claim && + root.outerClaim == Aiur.buildClaim childJoinIdx pubInput #[] && + left.cacheKey == liftCacheKey + | _, _, _ => false + | .error _ => false + let cachedLiftBytes := Ixon.Proof.ser cachedLiftWrapper + let resumedLift? ← match cacheSpecs with + | .ok specs => + match specs[0]? with + | some spec => + Ix.Cli.AggregateCmd.loadCachedAggregateProofWith + (fun _ => pure cachedLiftBytes) cacheDir 0 spec childSystem + | none => pure none + | .error _ => pure none + let corruptStoreLift? ← match cacheSpecs with + | .ok specs => + match specs[0]? with + | some spec => + Ix.Cli.AggregateCmd.loadCachedAggregateProofWith + (fun _ => pure (cachedLiftBytes.push 0xff)) + cacheDir 0 spec childSystem + | none => pure none + | .error _ => pure none + let verifiedResumeHit := resumedLift?.isSome + let corruptStoreFallsThrough := corruptStoreLift?.isNone let leftOuterBytes := MultiStark.serializeClaims #[leftOuter] let rightOuterBytes := MultiStark.serializeClaims #[rightOuter] @@ -580,6 +779,74 @@ def joinSmokeSuite : IO UInt32 := do let badProofIo := io.extend 0 zeroKey (bytesAsGs badLeftProofBytes) let badProof := compiled.bytecode.execute joinIdx pubInput badProofIo + -- Run the same two-lift/one-join proof DAG through the WP-B executor at + -- jobs=1 and jobs=2. Both leaves are admitted together in the parallel run, + -- exercising concurrent calls through the same Aiur prover used by the + -- production wrapper; the stand-in bytecode deliberately uses the ordinary + -- witness path because the specialized MultiStark witness builder has a + -- fixed production input shape. Use zero query PoW here because the pinned + -- dependency's positive-PoW grind legitimately returns whichever passing + -- witness rayon finds first, making even repeated serial proof bytes differ. + -- Zero PoW has a canonical witness, so complete-wrapper equality isolates + -- scheduling determinism rather than PoW-search nondeterminism. + let scheduledProofSystem := AiurSystem.build childCompiled.bytecode + recCommitParams { innerFri with queryProofOfWorkBits := 0 } + let scheduledProofSlot (slotIdx : Nat) + (slots : Array (Option ByteArray)) : IO (Except String ByteArray) := do + match slotIdx with + | 0 | 1 => + let claimsBytes := if slotIdx == 0 then leftInnerClaims else rightInnerClaims + let expectedOuter := if slotIdx == 0 then leftOuter else rightOuter + let liftInput := MultiStark.verifierPubInput fakeIxvmVk claimsBytes + let (outer, proof, _) := scheduledProofSystem.prove liftIdx liftInput default + if outer != expectedOuter then return .error "scheduled lift claim mismatch" + pure (.ok proof.toBytes) + | 2 => + let some leftBytes := (slots[0]?).join + | return .error "scheduled join missing left proof" + let some rightBytes := (slots[1]?).join + | return .error "scheduled join missing right proof" + let leftProof ← match Aiur.Proof.ofBytesChecked leftBytes with + | .error e => return .error e + | .ok proof => pure proof + let rightProof ← match Aiur.Proof.ofBytesChecked rightBytes with + | .error e => return .error e + | .ok proof => pure proof + match scheduledProofSystem.verify leftOuter leftProof, + scheduledProofSystem.verify rightOuter rightProof with + | .ok (), .ok () => pure () + | .error e, _ | _, .error e => return .error e + let (outer, proof, _) := scheduledProofSystem.prove childJoinIdx pubInput default + if outer != Aiur.buildClaim childJoinIdx pubInput #[] then + return .error "scheduled join claim mismatch" + pure (.ok proof.toBytes) + | _ => pure (.error "unexpected scheduled proof slot") + let scheduledWrapperBytes (proofs : Array ByteArray) : Array ByteArray := + proofs.mapIdx fun slotIdx proof => + let claim := if slotIdx == 0 then leftStatement.claim + else if slotIdx == 1 then rightStatement.claim + else outputStatement.claim + Ixon.Proof.ser { claim, proof } + let serialScheduledProofs ← Ix.Cli.AggregateCmd.runAggregateDag cachePlan + #[8, 8, 4] 1 16 scheduledProofSlot + let parallelScheduledProofs ← Ix.Cli.AggregateCmd.runAggregateDag cachePlan + #[8, 8, 4] 2 16 scheduledProofSlot + let parallelProofWrappersStable ← + match serialScheduledProofs, parallelScheduledProofs with + | .ok serial, .ok parallel => + let serialWrappers := scheduledWrapperBytes serial + let parallelWrappers := scheduledWrapperBytes parallel + if serialWrappers != parallelWrappers then + IO.eprintln s!"scheduled proof mismatch: serial={serialWrappers.map Address.blake3}, \ + parallel={parallelWrappers.map Address.blake3}" + pure (serialWrappers == parallelWrappers) + | .error e, _ => + IO.eprintln s!"serial scheduled proof failed: {e}" + pure false + | _, .error e => + IO.eprintln s!"parallel scheduled proof failed: {e}" + pure false + let hostFoldCorrect := outputSubjects.leaves == (canonicalTree #[a, b, c]).leaves && outputStatement.assumptions.map (·.leaves) == some (canonicalTree #[d]).leaves @@ -600,6 +867,50 @@ def joinSmokeSuite : IO UInt32 := do match Ix.Cli.CheckCmd.parseIxesManifest duplicate with | .error _ => true | .ok _ => false + let (singleEnv, singleAddr) := singletonIxonEnv + let singleTreeTail := #[1, 1, 0] ++ u32le4 0 ++ #[1, 0] ++ + u32le4 1 ++ #[0] ++ u32le4 2 + let singleManifest := Ix.Cli.CheckCmd.parseIxesManifest + (minimalIxesFor #[#[], #[singleAddr], #[]] singleTreeTail) + let singleCoverage ← match singleManifest with + | .ok view => Ix.Cli.CheckCmd.shardsCover singleEnv view.shards + | .error _ => pure false + let emptyPruningCorrect : Bool := match singleManifest with + | .ok view => match view.pruneEmpty singleEnv with + | .ok (pruned, counts) => + pruned.shards == #[#[singleAddr]] && pruned.shardIds == #[1] && + pruned.aggregationTree == .leaf 0 && counts == #[1] + | .error _ => false + | .error _ => false + let singleManifestLiftRoot : Bool := match singleManifest with + | .ok view => match Ix.Cli.VerifyCmd.expectedFromManifest singleEnv view 0 with + | .ok (statement, .lift) => + statement.claim == .checkEnv (canonicalTree #[singleAddr]).root none + | _ => false + | .error _ => false + let shardPrepPreservesSemantics : Bool := + let (sharedEnv, owned, sharedAddress) := sharedClosureIxonEnv + let legacyClosure : Std.HashSet Address := Id.run do + let mut closure : Std.HashSet Address := {} + for address in owned do + closure := closure.union + (IxVM.ClaimHarness.closureFrom sharedEnv address) + return closure + let expectedOwned := canonicalTree owned + let expectedFrontier := canonicalTree #[sharedAddress] + match IxVM.ClaimHarness.shardCheckEnvClaimTrees sharedEnv owned, + IxVM.ClaimHarness.shardCheckEnvClaim sharedEnv owned with + | .ok (claimOnly, treesOnly), .ok (claimFull, closure, treesFull) => + let sameClosure := closure.size == legacyClosure.size && + closure.toArray.all legacyClosure.contains + claimOnly == .checkEnv expectedOwned.root (some expectedFrontier.root) && + claimFull == claimOnly && sameClosure && + treesOnly.size == 2 && treesFull.size == 2 && + treesOnly.contains expectedOwned.root && + treesOnly.contains expectedFrontier.root && + treesFull.contains expectedOwned.root && + treesFull.contains expectedFrontier.root + | _, _ => false let mixedScheduleCorrect : Bool := match Ix.Cli.AggregateCmd.schedulePlan manifestPlan #[2, 2, 1] 4 with | .ok scheduled => @@ -610,14 +921,138 @@ def joinSmokeSuite : IO UInt32 := do | _, _ => false | .error _ => false + -- WP-B's pure admission gate: three leaves are initially ready, but the + -- heaviest 8-byte stand-in occupies the 10-byte budget alone. Once it + -- completes, the 6- and 3-byte leaves run together; joins become eligible + -- only after both declared children complete. + let schedulerPlan := Ix.Cli.AggregateCmd.schedulePlan + manifestPlan #[2, 2, 1] 4 + let fakeWeights : Array Nat := #[8, 3, 4, 6, 5] + let schedulerTrace := schedulerPlan.bind fun scheduled => + Ix.Cli.AggregateCmd.simulateAggregateSchedule scheduled fakeWeights 2 10 + let schedulerHeaviestFirst : Bool := match schedulerTrace with + | .ok trace => + trace.admissionOrder == #[0, 3, 1, 2, 4] && + trace.admissionBatches == #[#[0], #[3, 1], #[2], #[4]] + | .error _ => false + let schedulerWithinLimits : Bool := match schedulerTrace with + | .ok trace => + trace.maxReservedBytes <= 10 && + trace.admissionBatches.all (fun batch => batch.size <= 2) + | .error _ => false + let schedulerDependenciesHold : Bool := match schedulerTrace with + | .ok trace => + let position (slot : Nat) := trace.admissionOrder.findIdx? (· == slot) + match position 0, position 1, position 2, position 3, position 4 with + | some p0, some p1, some p2, some p3, some p4 => + p0 < p2 && p1 < p2 && p2 < p4 && p3 < p4 + | _, _, _, _, _ => false + | .error _ => false + let oversizedRunsAlone : Bool := match schedulerPlan.bind fun scheduled => + Ix.Cli.AggregateCmd.simulateAggregateSchedule scheduled + #[11, 3, 4, 6, 5] 2 10 with + | .ok trace => trace.admissionBatches[0]? == some #[0] && + trace.admissionBatches.all fun batch => + batch.size == 1 || batch.all fun slot => fakeWeights[slot]! <= 10 + | .error _ => false + let flatWeightAffine := + Ix.Cli.AggregateCmd.aggregateSlotRamBytes + { op := .join 0 1, subjectCount := 7, structural := false } == + Ix.Cli.AggregateCmd.aggregateStructuralJoinRamBytes + + 7 * Ix.Cli.AggregateCmd.aggregateFlatJoinRamPerSubjectBytes + let memTotalParsing := + Ix.Cli.AggregateCmd.aggregateMemTotalBytes + "MemTotal: 1024 kB\nMemFree: 512 kB\n" == some (1024 * 1024) + + -- Exercise the actual task/channel executor at jobs=1 and jobs=2. The fake + -- payload is content-derived exactly like a wrapper: leaves encode their + -- shard and slot, while joins concatenate both completed child payloads. + let fakeRun (scheduled : Array Ix.Cli.AggregateCmd.ScheduledFold) + (slotIdx : Nat) (slots : Array (Option ByteArray)) : + IO (Except String ByteArray) := do + let some item := scheduled[slotIdx]? + | return .error "missing fake slot" + match item.op with + | .leaf shard => + pure (.ok ⟨#[UInt8.ofNat shard, UInt8.ofNat slotIdx]⟩) + | .join left right => + let some leftBytes := (slots[left]?).join + | return .error "missing fake left child" + let some rightBytes := (slots[right]?).join + | return .error "missing fake right child" + pure (.ok ((leftBytes ++ rightBytes).push (UInt8.ofNat slotIdx))) + let schedulerSerialParallelParity ← match schedulerPlan with + | .error _ => pure false + | .ok scheduled => + let serial ← Ix.Cli.AggregateCmd.runAggregateDag scheduled fakeWeights + 1 10 (fakeRun scheduled) + let parallel ← Ix.Cli.AggregateCmd.runAggregateDag scheduled fakeWeights + 2 10 (fakeRun scheduled) + pure <| match serial, parallel with + | .ok serial, .ok parallel => serial == parallel + | _, _ => false + let dependentStarted ← IO.mkRef false + let failureRun (slotIdx : Nat) (_ : Array (Option Nat)) : + IO (Except String Nat) := do + if slotIdx == 0 then return .error "intentional leaf failure" + if slotIdx == 2 then dependentStarted.set true + pure (.ok slotIdx) + let schedulerStopsAfterFailure ← match schedulerPlan with + | .error _ => pure false + | .ok scheduled => + let result ← Ix.Cli.AggregateCmd.runAggregateDag scheduled fakeWeights + 2 10 failureRun + let started ← dependentStarted.get + pure <| match result with + | .error e => e.startsWith "slot 0: intentional leaf failure" && !started + | .ok _ => false + lspecIO (.ofList [("aggregate-first", [ + test "default recursion parameters preserve the legacy verifying key" + defaultRecursionIdentityPreserved, + test "recursion FRI cache encoding is the pinned 40-byte layout" + defaultFriEncodingStable, + test "FRI and commitment overrides independently change recursion identity" + recursionParametersIndependent, + test "aggregate cache key binds version, recursion vk, FRI params, and outer claim" + cacheKeyInputsBound, + test "all aggregate slot claims and cache keys are prepared before proving" + cacheSpecsComplete, + test "aggregate cache index atomically round-trips a store address" + cacheIndexRoundTrip, + test "aggregate cache treats a corrupt index as an invalid hint" + corruptCacheIndexRejected, + test "aggregate cache atomically replaces a corrupt index after re-proving" + corruptCacheIndexRecovers, + test "aggregate cache resumes from a content-addressed verified wrapper" + verifiedResumeHit, + test "aggregate cache treats corrupt store content as a miss" + corruptStoreFallsThrough, + expectOk "aggregate cache accepts an exactly bound valid wrapper" + validCachedLift, + expectErr "aggregate cache rejects a wrapper for a different CheckEnv" + wrongCachedStatement, + expectErr "aggregate cache rejects a proof under a different outer claim" + wrongCachedOuterClaim, + expectErr "aggregate cache rejects a corrupted proof" + badCachedProof, test "host fold constructs canonical union/discharge trees" hostFoldCorrect, test "manifest tree lowers to post-order binary slots" (manifestPlan == expectedPlan), test "manifest parser exposes its validated bisection tree" parsedManifestPlan, test "manifest parser rejects repeated aggregation leaves" malformedManifestRejected, + test "coverage accepts legacy zero-constant manifest leaves" singleCoverage, + test "empty manifest leaves contract and retained ids remap densely" + emptyPruningCorrect, + test "one retained shard folds to a lift root" singleManifestLiftRoot, + test "shard claim-only prep preserves trees and one-pass closure semantics" + shardPrepPreservesSemantics, test "stand-in lift/flat/structural entrypoints survive compiler dedup separately" (liftIdx != childJoinIdx && liftIdx != childStructuralJoinIdx && childJoinIdx != childStructuralJoinIdx), + test "aggregate verifier reconstructs the single-shard lift claim" + liftClaimReconstruction, + expectOk "reconstructed single-shard lift root verifies natively" + reconstructedLiftVerifies, expectOk "join accepts canonical union and cross-child discharge" honest, test "join child outer claim carries allowed/output digests" joinChildLayout, expectOk "stand-in join child proof verifies natively" joinChildNativeVerify, @@ -638,6 +1073,24 @@ def joinSmokeSuite : IO UInt32 := do transitiveStructural, test "threshold scheduling is flat below and structural above monotonically" mixedScheduleCorrect, + test "RAM-gated scheduler admits ready work heaviest-first" + schedulerHeaviestFirst, + test "RAM-gated scheduler respects job and byte budgets" + schedulerWithinLimits, + test "RAM-gated scheduler never admits joins before both children" + schedulerDependenciesHold, + test "an individually oversized scheduler slot is admitted alone" + oversizedRunsAlone, + test "flat-join RAM reserve is affine in subject leaves" + flatWeightAffine, + test "aggregate scheduler parses MemTotal for its default budget" + memTotalParsing, + test "jobs=2 DAG execution is byte-identical to jobs=1" + schedulerSerialParallelParity, + test "a failed slot drains peers without starting dependent joins" + schedulerStopsAfterFailure, + test "jobs=2 zero-PoW proof wrappers are byte-identical to jobs=1" + parallelProofWrappersStable, expectErr "structural join rejects a path to the wrong root" wrongRootPath, expectErr "structural join rejects a tampered path sibling" tamperedPath, expectErr "structural join rejects a candidate with no path choice" diff --git a/Tests/MultiStarkActivation.lean b/Tests/MultiStarkActivation.lean new file mode 100644 index 000000000..ec685a067 --- /dev/null +++ b/Tests/MultiStarkActivation.lean @@ -0,0 +1,523 @@ +module + +public import Tests.MultiStark + +/-! +# Aggregate recursion activation audit + +WP-D from `plans/aggregate-first-pipeline.md` asks for an input-shape audit of +the production lift, flat-join, and structural-join entrypoints before any +future static terminal circuit relies on an input-independent activation set. + +This runner deliberately stays separate from the normal aggregate smoke suite. +It executes a deterministic 98-case matrix twice, compares every returned +per-circuit query count, and emits a Markdown report of circuits inactive in at +least one case. It does not add dummy calls; that policy remains deferred until +a static terminal is selected. +-/ + +public section + +open Aiur + +namespace Tests.MultiStark +namespace ActivationAudit + +inductive Height where + | short + | tall + deriving BEq, Repr + +private def Height.label : Height → String + | .short => "short" + | .tall => "tall" + +inductive ChildKind where + | lift + | flat + | structural + deriving BEq, Repr + +private def ChildKind.label : ChildKind → String + | .lift => "lift" + | .flat => "flat" + | .structural => "structural" + +inductive Disposition where + | discharge + | carry + deriving BEq, Repr + +private def Disposition.label : Disposition → String + | .discharge => "discharge" + | .carry => "carry" + +inductive Entrypoint where + | lift + | flat + | structural + deriving BEq, Repr + +private def Entrypoint.label : Entrypoint → String + | .lift => "lift" + | .flat => "flat" + | .structural => "structural" + +private inductive JoinKind where + | flat + | structural + +private def JoinKind.entrypoint : JoinKind → Entrypoint + | .flat => .flat + | .structural => .structural + +private def JoinKind.label (kind : JoinKind) : String := + kind.entrypoint.label + +/-- Cheap parameters are sufficient here: the audit studies which verifier +circuits execute, not soundness calibration or proof size. -/ +private def auditFri : Aiur.FriParameters := + { logFinalPolyLen := 0, maxLogArity := 1, numQueries := 1, + commitProofOfWorkBits := 0, queryProofOfWorkBits := 0 } + +private def canonicalTree (leaves : Array Address) : Ix.AssumptionTree := + (Ix.AssumptionTree.canonical leaves).get! + +private def digestSelectsShort (digest : Array Aiur.G) : Bool := + match digest[0]?, digest[1]? with + | some a, some b => decide (a.n < b.n) + | _, _ => false + +private structure Indices where + verify : Aiur.Bytecode.FunIdx + lift : Aiur.Bytecode.FunIdx + flat : Aiur.Bytecode.FunIdx + structural : Aiur.Bytecode.FunIdx + +private structure HeightConfig where + height : Height + fakeIxvmVk : ByteArray + allowed : ByteArray + probeRows : Nat + +/-- Find a tiny fake IxVM key whose own digest and resulting allowed-blob +digest select the same branch of `activation_vary_height`. The search has +roughly 1/4 success probability per candidate for either requested branch. -/ +private def findFakeIxvmVk (childVk : ByteArray) (indices : Indices) + (height : Height) : Except String ByteArray := + let wantShort := height == .short + let candidate? := (Array.range 4096).find? fun n => + let candidate : ByteArray := ⟨Tests.MultiStark.u64le n⟩ + let allowed := MultiStark.allowedBlob candidate indices.verify childVk + indices.lift indices.flat indices.structural + digestSelectsShort (MultiStark.digestGs candidate) == wantShort && + digestSelectsShort (MultiStark.digestGs allowed) == wantShort + match candidate? with + | some n => .ok ⟨Tests.MultiStark.u64le n⟩ + | none => .error s!"activation audit: no {height.label} digest selector found" + +private def heightProbeRows (compiled : Aiur.CompiledToplevel) + (verifyIdx probeIdx : Aiur.Bytecode.FunIdx) (fakeIxvmVk : ByteArray) : + Except String Nat := do + let (_, _, counts) ← compiled.bytecode.execute verifyIdx + (MultiStark.digestGs fakeIxvmVk) default + let some count := counts[probeIdx]? + | throw s!"activation audit: missing height-probe query count {probeIdx}" + pure count.uniqueRows + +private def prepareHeightConfig (compiled : Aiur.CompiledToplevel) + (childVk : ByteArray) (indices : Indices) (probeIdx : Aiur.Bytecode.FunIdx) + (height : Height) : Except String HeightConfig := do + let fakeIxvmVk ← findFakeIxvmVk childVk indices height + let allowed := MultiStark.allowedBlob fakeIxvmVk indices.verify childVk + indices.lift indices.flat indices.structural + let probeRows ← heightProbeRows compiled indices.verify probeIdx fakeIxvmVk + pure { height, fakeIxvmVk, allowed, probeRows } + +private structure PreparedChild where + proofBytes : ByteArray + outerClaimsBytes : ByteArray + preimages : Array ByteArray + +private def prepareChild (system : Aiur.AiurSystem) (indices : Indices) + (config : HeightConfig) (kind : ChildKind) + (statement : MultiStark.CheckEnvTrees) : PreparedChild := + let claimBytes := Ix.Claim.ser statement.claim + match kind with + | .lift => + let innerClaim := Aiur.buildClaim indices.verify + (MultiStark.digestGs claimBytes) #[] + let innerClaimsBytes := MultiStark.serializeClaims #[innerClaim] + let input := MultiStark.verifierPubInput config.fakeIxvmVk innerClaimsBytes + let (outer, proof, _) := system.prove indices.lift input default + { proofBytes := proof.toBytes + outerClaimsBytes := MultiStark.serializeClaims #[outer] + preimages := #[innerClaimsBytes, claimBytes] } + | .flat | .structural => + let idx := match kind with + | .flat => indices.flat + | .structural => indices.structural + | .lift => unreachable! + let input := MultiStark.joinPubInput config.allowed claimBytes + let (outer, proof, _) := system.prove idx input default + { proofBytes := proof.toBytes + outerClaimsBytes := MultiStark.serializeClaims #[outer] + preimages := #[claimBytes] } + +private structure JoinCase where + label : String + allowed : ByteArray + left : MultiStark.CheckEnvTrees + right : MultiStark.CheckEnvTrees + leftChild : PreparedChild + rightChild : PreparedChild + +private def assumptionLabel (present : Bool) : String := + if present then "some" else "none" + +private def selectStatement (withoutAsm discharge carry : + MultiStark.CheckEnvTrees) (present : Bool) + (disposition : Disposition) : MultiStark.CheckEnvTrees := + if !present then withoutAsm + else match disposition with + | .discharge => discharge + | .carry => carry + +/-- Build the 48 join inputs shared by the flat and structural entrypoints: + +`2 heights × 2 dispositions × 2 left-asm shapes × 2 right-asm shapes + × 3 left-child kinds`. + +The right child remains a lift. Both child positions call the same decoder, so +varying one side covers all three decoder arms while retaining a mixed-shape +case for the flat and structural child kinds. -/ +private def prepareJoinCases (system : Aiur.AiurSystem) (indices : Indices) + (configs : Array HeightConfig) : Array JoinCase := Id.run do + let a := Address.blake3 "activation-subject-left".toUTF8 + let b := Address.blake3 "activation-subject-right".toUTF8 + let c := Address.blake3 "activation-carry-left".toUTF8 + let d := Address.blake3 "activation-carry-right".toUTF8 + let leftSubjects := canonicalTree #[a] + let rightSubjects := canonicalTree #[b] + let leftNone : MultiStark.CheckEnvTrees := + { subjects := leftSubjects, assumptions := none } + let leftDischarge : MultiStark.CheckEnvTrees := + { subjects := leftSubjects, assumptions := some (canonicalTree #[b]) } + let leftCarry : MultiStark.CheckEnvTrees := + { subjects := leftSubjects, assumptions := some (canonicalTree #[c]) } + let rightNone : MultiStark.CheckEnvTrees := + { subjects := rightSubjects, assumptions := none } + let rightDischarge : MultiStark.CheckEnvTrees := + { subjects := rightSubjects, assumptions := some (canonicalTree #[a]) } + let rightCarry : MultiStark.CheckEnvTrees := + { subjects := rightSubjects, assumptions := some (canonicalTree #[d]) } + let mut cases : Array JoinCase := #[] + for config in configs do + for disposition in #[Disposition.discharge, .carry] do + for leftAsm in #[false, true] do + for rightAsm in #[false, true] do + let left := selectStatement leftNone leftDischarge leftCarry + leftAsm disposition + let right := selectStatement rightNone rightDischarge rightCarry + rightAsm disposition + let rightChild := prepareChild system indices config .lift right + for childKind in #[ChildKind.lift, .flat, .structural] do + let leftChild := prepareChild system indices config childKind left + cases := cases.push { + label := s!"height={config.height.label},left-asm={assumptionLabel leftAsm},\ + right-asm={assumptionLabel rightAsm},disposition={disposition.label},\ + left-child={childKind.label},right-child=lift" + allowed := config.allowed + left + right + leftChild + rightChild + } + return cases + +private structure Sample where + label : String + entrypoint : Entrypoint + queryCounts : Array Aiur.QueryCount + +private def runLift (compiled : Aiur.CompiledToplevel) + (childSystem : Aiur.AiurSystem) (childVk : ByteArray) (indices : Indices) + (productionLiftIdx : Aiur.Bytecode.FunIdx) (config : HeightConfig) : + Except String Sample := do + let input := MultiStark.digestGs config.fakeIxvmVk + let (innerClaim, proof, _) := childSystem.prove indices.verify input default + let claimBytes := MultiStark.serializeClaims #[innerClaim] + let pubInput := MultiStark.verifierPubInput childVk claimBytes + let (_, queryCounts) ← compiled.bytecode.executeMultiStark productionLiftIdx + pubInput proof.toBytes childVk claimBytes + pure { + label := s!"lift/height={config.height.label}" + entrypoint := .lift + queryCounts + } + +private def runJoinWithVk (compiled : Aiur.CompiledToplevel) + (childVk : ByteArray) (flatIdx structuralIdx : Aiur.Bytecode.FunIdx) + (kind : JoinKind) (case : JoinCase) : Except String Sample := do + let output := match kind with + | .flat => case.left.join case.right + | .structural => case.left.joinStructural case.right + let idx := match kind with + | .flat => flatIdx + | .structural => structuralIdx + let trees := match kind with + | .flat => MultiStark.CheckEnvTrees.adviceTrees case.left case.right output + | .structural => + MultiStark.CheckEnvTrees.structuralAdviceTrees case.left case.right output + let paths := match kind with + | .flat => #[] + | .structural => + MultiStark.CheckEnvTrees.structuralPathAdvice case.left case.right output + let outputBytes := Ix.Claim.ser output.claim + let pubInput := MultiStark.joinPubInput case.allowed outputBytes + let preimagesBlob := MultiStark.joinPreimagesBlob + (case.leftChild.preimages ++ case.rightChild.preimages) + let (_, queryCounts) ← match compiled.bytecode.executeMultiStarkJoin idx + pubInput case.leftChild.proofBytes case.rightChild.proofBytes childVk + case.leftChild.outerClaimsBytes case.rightChild.outerClaimsBytes outputBytes + case.allowed preimagesBlob (MultiStark.joinTreesBlob trees) + (MultiStark.joinPathsBlob paths) with + | .ok result => pure result + | .error e => throw s!"{kind.label}/{case.label}: {e}" + pure { + label := s!"{kind.label}/{case.label}" + entrypoint := kind.entrypoint + queryCounts + } + +private def collect (compiled : Aiur.CompiledToplevel) + (childSystem : Aiur.AiurSystem) (childVk : ByteArray) (indices : Indices) + (productionLiftIdx flatIdx structuralIdx : Aiur.Bytecode.FunIdx) + (configs : Array HeightConfig) (cases : Array JoinCase) : + Except String (Array Sample) := do + let mut samples : Array Sample := #[] + for config in configs do + samples := samples.push (← runLift compiled childSystem childVk indices + productionLiftIdx config) + for case in cases do + samples := samples.push (← runJoinWithVk compiled childVk flatIdx + structuralIdx .flat case) + for case in cases do + samples := samples.push (← runJoinWithVk compiled childVk flatIdx + structuralIdx .structural case) + pure samples + +private def queryCountsEq (left right : Array Aiur.QueryCount) : Bool := + left.size == right.size && (left.zip right).all fun (a, b) => + a.uniqueRows == b.uniqueRows && a.totalHits == b.totalHits + +private def samplesEq (left right : Array Sample) : Bool := + left.size == right.size && (left.zip right).all fun (a, b) => + a.label == b.label && a.entrypoint == b.entrypoint && + queryCountsEq a.queryCounts b.queryCounts + +private structure Circuit where + name : String + queryIdx : Nat + +private def circuits (compiled : Aiur.CompiledToplevel) : Array Circuit := Id.run do + let reverseNames := compiled.nameMap.fold + (init := ({} : Std.HashMap Aiur.Bytecode.FunIdx String)) + fun names global idx => + let name := toString global + match names[idx]? with + | none => names.insert idx name + | some old => if compare name old == .lt then names.insert idx name else names + let mut result : Array Circuit := #[] + for (function, idx) in compiled.bytecode.functions.mapIdx + fun idx function => (function, idx) do + if function.constrained then + result := result.push { + name := reverseNames[idx]?.getD s!"fn[{idx}]" + queryIdx := idx + } + let functionCount := compiled.bytecode.functions.size + for (width, idx) in compiled.bytecode.memorySizes.mapIdx fun idx width => + (width, idx) do + result := result.push { + name := s!"memory[{width}]" + queryIdx := functionCount + idx + } + return result + +private structure Cell where + active : Nat + total : Nat + minActiveRows : Nat + maxActiveRows : Nat + +private def rowsAt (sample : Sample) (queryIdx : Nat) : Nat := + match sample.queryCounts[queryIdx]? with + | some count => count.uniqueRows + | none => 0 + +private def cell (samples : Array Sample) (queryIdx : Nat) : Cell := + let activeRows := samples.map (rowsAt · queryIdx) |>.filter (· != 0) + let minActiveRows := match activeRows[0]? with + | none => 0 + | some first => activeRows.foldl Nat.min first + { + active := activeRows.size + total := samples.size + minActiveRows + maxActiveRows := activeRows.foldl Nat.max 0 + } + +private def entrySamples (samples : Array Sample) (entrypoint : Entrypoint) : + Array Sample := + samples.filter fun sample => sample.entrypoint == entrypoint + +private def Cell.render (c : Cell) : String := + if c.active == 0 then s!"0/{c.total}" + else s!"{c.active}/{c.total} ({c.minActiveRows}..{c.maxActiveRows})" + +private def activationSignature (samples : Array Sample) : Address := + let lines := samples.map fun sample => + let counts := sample.queryCounts.map fun count => + s!"{count.uniqueRows}/{count.totalHits}" + sample.label ++ ":" ++ String.intercalate "," counts.toList + Address.blake3 (String.intercalate "\n" lines.toList).toUTF8 + +private def report (compiled : Aiur.CompiledToplevel) + (configs : Array HeightConfig) (samples : Array Sample) : String := + let catalog := circuits compiled + let liftSamples := entrySamples samples .lift + let flatSamples := entrySamples samples .flat + let structuralSamples := entrySamples samples .structural + let affected := catalog.filter fun circuit => + let summary := cell samples circuit.queryIdx + summary.active < summary.total + let alwaysActive := catalog.countP fun circuit => + let summary := cell samples circuit.queryIdx + summary.active == summary.total + let variableCount := catalog.countP fun circuit => + let summary := cell samples circuit.queryIdx + summary.active != 0 && summary.active < summary.total + let neverObserved := catalog.countP fun circuit => + (cell samples circuit.queryIdx).active == 0 + let configRows := configs.map fun config => + s!"| {config.height.label} | {config.probeRows} |" + let circuitRows := affected.map fun circuit => + s!"| `{circuit.name}` | {(cell liftSamples circuit.queryIdx).render} | \ + {(cell flatSamples circuit.queryIdx).render} | \ + {(cell structuralSamples circuit.queryIdx).render} |" + let introduction := #[] + |>.push "# Aggregate recursion activation audit" + |>.push "" + |>.push s!"- Matrix signature: `{activationSignature samples}`" + |>.push s!"- Accepted executions: {samples.size} \ + ({liftSamples.size} lift, {flatSamples.size} flat, \ + {structuralSamples.size} structural)" + |>.push "- Join axes: assumption root `{none,some}` independently per side; \ + `{discharge,carry}`; left child `{lift,flat,structural}` with a lift on \ + the right; and two child trace heights." + |>.push "- Counts are `active cases / total cases (min..max unique rows when active)`." + |>.push "- Catalog covers constrained function circuits and memory circuits. \ + `Bytes1`/`Bytes2` are fixed-height preprocessed circuits and are not \ + represented in the execute FFI's query-count array." + |>.push s!"- Catalog summary: {catalog.size} circuits; {alwaysActive} active \ + in every case; {variableCount} input-dependent; {neverObserved} never observed." + |>.push "- Dummy calls remain deferred until a static terminal circuit is selected." + |>.push "" + |>.push "## Trace-height control" + |>.push "" + |>.push "| Height | `activation_height_probe` unique rows |" + |>.push "|---|---:|" + let circuitHeader := (introduction ++ configRows) + |>.push "" + |>.push "## Circuits inactive in at least one audited shape" + |>.push "" + |>.push "| Circuit | Lift | Flat join | Structural join |" + |>.push "|---|---:|---:|---:|" + String.intercalate "\n" (circuitHeader ++ circuitRows).toList + +def run : IO UInt32 := do + IO.println "aggregate-activation (98-case matrix, two deterministic passes)…" + let childCompiled ← match Tests.MultiStark.joinChildProgram.compile with + | .error e => IO.eprintln s!"activation child compilation failed: {e}"; return 1 + | .ok compiled => pure compiled + let childSystem := Aiur.AiurSystem.build childCompiled.bytecode + Tests.MultiStark.recCommitParams auditFri + let childVk := childSystem.vkBytes + let some verifyIdx := childCompiled.getFuncIdx `fake_verify_claim | do + IO.eprintln "activation audit: fake_verify_claim entrypoint not found"; return 1 + let some childLiftIdx := childCompiled.getFuncIdx `fake_lift | do + IO.eprintln "activation audit: fake_lift entrypoint not found"; return 1 + let some childFlatIdx := childCompiled.getFuncIdx `fake_join | do + IO.eprintln "activation audit: fake_join entrypoint not found"; return 1 + let some childStructuralIdx := childCompiled.getFuncIdx `fake_struct_join | do + IO.eprintln "activation audit: fake_struct_join entrypoint not found"; return 1 + let some probeIdx := childCompiled.getFuncIdx `activation_height_probe | do + IO.eprintln "activation audit: height probe not found"; return 1 + let indices : Indices := { + verify := verifyIdx + lift := childLiftIdx + flat := childFlatIdx + structural := childStructuralIdx + } + let short ← match prepareHeightConfig childCompiled childVk indices probeIdx .short with + | .error e => IO.eprintln e; return 1 + | .ok config => pure config + let tall ← match prepareHeightConfig childCompiled childVk indices probeIdx .tall with + | .error e => IO.eprintln e; return 1 + | .ok config => pure config + if short.probeRows >= tall.probeRows then + IO.eprintln s!"activation audit: height controls did not vary the trace \ + ({short.probeRows} vs {tall.probeRows} rows)" + return 1 + let configs := #[short, tall] + let cases := prepareJoinCases childSystem indices configs + if cases.size != 48 then + IO.eprintln s!"activation audit: expected 48 join cases, built {cases.size}" + return 1 + + let top ← match MultiStark.multiStark with + | .error e => IO.eprintln s!"activation toplevel merge failed: {e}"; return 1 + | .ok top => pure top + let compiled ← match top.compile with + | .error e => IO.eprintln s!"activation toplevel compilation failed: {e}"; return 1 + | .ok compiled => pure compiled + let some productionLiftIdx := compiled.getFuncIdx `verify_multi_stark_proof | do + IO.eprintln "activation audit: production lift entrypoint not found"; return 1 + let some flatIdx := compiled.getFuncIdx `join_two | do + IO.eprintln "activation audit: flat join entrypoint not found"; return 1 + let some structuralIdx := compiled.getFuncIdx `join_two_structural | do + IO.eprintln "activation audit: structural join entrypoint not found"; return 1 + + let first ← match collect compiled childSystem childVk indices + productionLiftIdx flatIdx structuralIdx configs cases with + | .error e => IO.eprintln s!"activation audit pass 1 failed: {e}"; return 1 + | .ok samples => pure samples + let second ← match collect compiled childSystem childVk indices + productionLiftIdx flatIdx structuralIdx configs cases with + | .error e => IO.eprintln s!"activation audit pass 2 failed: {e}"; return 1 + | .ok samples => pure samples + if first.size != 98 then + IO.eprintln s!"activation audit: expected 98 samples, collected {first.size}" + return 1 + let expectedQueryCounts := compiled.bytecode.functions.size + + compiled.bytecode.memorySizes.size + if first.any fun sample => sample.queryCounts.size != expectedQueryCounts then + IO.eprintln s!"activation audit: a sample returned the wrong query-count \ + cardinality (expected {expectedQueryCounts})" + return 1 + if !samplesEq first second then + IO.eprintln "activation audit: query-count matrix changed between passes" + return 1 + IO.println (report compiled configs first) + IO.println "" + IO.println "[activation-audit] stable across two passes" + return 0 + +end ActivationAudit + +def activationAudit : IO UInt32 := ActivationAudit.run + +end Tests.MultiStark + +end diff --git a/crates/ffi/src/aiur/protocol.rs b/crates/ffi/src/aiur/protocol.rs index 9f9285a67..c7681563c 100644 --- a/crates/ffi/src/aiur/protocol.rs +++ b/crates/ffi/src/aiur/protocol.rs @@ -59,6 +59,27 @@ extern "C" fn rs_aiur_proof_of_bytes( LeanExternal::alloc(&AIUR_PROOF_CLASS, proof) } +/// `Aiur.Proof.ofBytesChecked : @& ByteArray → Except String Proof` +/// +/// Unlike the legacy trusted-byte constructor above, this is safe at cache and +/// network boundaries: malformed bytes become a Lean error instead of a Rust +/// panic that aborts the process. +#[unsafe(no_mangle)] +extern "C" fn rs_aiur_proof_of_bytes_checked( + byte_array: LeanByteArray>, +) -> LeanExcept { + match AiurProof::from_bytes(byte_array.as_bytes()) { + Ok(proof) => { + let lean_proof: LeanOwned = + LeanExternal::alloc(&AIUR_PROOF_CLASS, proof).into(); + LeanExcept::ok(lean_proof) + }, + Err(err) => { + LeanExcept::error_string(&format!("proof deserialization failed: {err}")) + }, + } +} + /// `Aiur.AiurSystem.vkBytes : @& AiurSystem → ByteArray` /// /// Serializes the verifying key (`System`) — see diff --git a/crates/ixon/src/proof.rs b/crates/ixon/src/proof.rs index c43846d60..efe3cc9d3 100644 --- a/crates/ixon/src/proof.rs +++ b/crates/ixon/src/proof.rs @@ -144,10 +144,10 @@ pub enum RevealConstantInfo { /// circuit to resolve a leaf from a conditional claim's assumption /// set. Carries no assumptions itself. /// -/// The `assumptions` root may be any merkle tree (canonical sorted+ -/// padded via `merkle_root_canonical`, or free-form via `merkle_join`) -/// with `Address` leaves. Verifiers recover the leaf set via the -/// `AssumptionTree` serialization when free-form. +/// Merkle commitments carried by claims — both `CheckEnv.root` and every +/// `assumptions` root — may be canonical sorted+padded trees from +/// `merkle_root_canonical` or free-form trees from `merkle_join`. Verifiers +/// recover leaves or membership evidence according to the proof protocol. #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub enum Claim { /// `input` evaluates to `output`, optionally modulo `assumptions`. @@ -1177,6 +1177,7 @@ impl Proof { #[cfg(test)] mod tests { use super::*; + use crate::merkle::{merkle_join, merkle_root_canonical}; use quickcheck::{Arbitrary, Gen}; use quickcheck_macros::quickcheck; @@ -1573,6 +1574,18 @@ mod tests { assert!(claim_roundtrip(&claim)); } + #[test] + fn test_check_env_claim_accepts_structural_root() { + let a = Address::hash(b"structural-a"); + let b = Address::hash(b"structural-b"); + let c = Address::hash(b"structural-c"); + let left = merkle_root_canonical(&[a.clone(), b.clone()]).unwrap(); + let right = merkle_root_canonical(std::slice::from_ref(&c)).unwrap(); + let root = merkle_join(&left, &right); + assert_ne!(root, merkle_root_canonical(&[a, b, c]).unwrap()); + assert!(claim_roundtrip(&Claim::CheckEnv { root, assumptions: None })); + } + #[test] fn test_contains_claim_roundtrip() { let claim = Claim::Contains { diff --git a/crates/kernel/src/claim.rs b/crates/kernel/src/claim.rs index 46d0605c8..6c5aceb2f 100644 --- a/crates/kernel/src/claim.rs +++ b/crates/kernel/src/claim.rs @@ -5,10 +5,10 @@ //! builders sit above it. They take an `Env` so they can compute the //! `assumptions` merkle root over the constant's transitive deps. //! -//! All builders default to the *canonical* merkle builder (sorted + -//! deduped leaves) — when recursive aggregation lands, free-form roots -//! from `merkle_join` will also be acceptable, but builders that start -//! from an env always produce canonical roots. +//! These env-derived builders intentionally use the *canonical* merkle builder +//! (sorted + deduped leaves). `Claim::CheckEnv` itself treats its root as an +//! opaque Merkle commitment and already accepts free-form roots produced by +//! recursive `merkle_join`; there is no canonical-root validator on claims. use rustc_hash::FxHashSet; diff --git a/crates/kernel/src/shard.rs b/crates/kernel/src/shard.rs index c06d1ae9a..00b81b61b 100644 --- a/crates/kernel/src/shard.rs +++ b/crates/kernel/src/shard.rs @@ -311,12 +311,25 @@ impl AggNode { /// `None` when nothing remains. Lets a prover fold along the tree even when /// only a subset of shards was proven (empty shards, `--only-shard`). pub fn prune(&self, keep: &impl Fn(u32) -> bool) -> Option { + self.filter_map_leaves(&|id| keep(id).then_some(id)) + } + + /// Generalized pruning used when a manifest writer drops empty shards and + /// densely renumbers the retained leaves. + fn filter_map_leaves( + &self, + map: &impl Fn(u32) -> Option, + ) -> Option { match self { - AggNode::Leaf(id) => keep(*id).then_some(AggNode::Leaf(*id)), - AggNode::Internal(l, r) => match (l.prune(keep), r.prune(keep)) { - (Some(a), Some(b)) => Some(AggNode::Internal(Box::new(a), Box::new(b))), - (Some(a), None) | (None, Some(a)) => Some(a), - (None, None) => None, + AggNode::Leaf(id) => map(*id).map(AggNode::Leaf), + AggNode::Internal(l, r) => { + match (l.filter_map_leaves(map), r.filter_map_leaves(map)) { + (Some(a), Some(b)) => { + Some(AggNode::Internal(Box::new(a), Box::new(b))) + }, + (Some(a), None) | (None, Some(a)) => Some(a), + (None, None) => None, + } }, } } @@ -1399,18 +1412,41 @@ impl ShardManifest { /// Serialize to the `.ixes` binary format. pub fn to_bytes(&self) -> Vec { + use rustc_hash::FxHashMap; + + // Older/fixed-count planners can leave block-empty shard records when the + // requested count exceeds the realizable partition. Never persist those + // leaves: omit them, contract the aggregation tree, and densely renumber + // the survivors. The Lean consumer additionally prunes zero-*constant* + // legacy leaves after validating them against the environment. + let retained: Vec<&ShardInfo> = + self.shards.iter().filter(|shard| !shard.blocks.is_empty()).collect(); + let remap: FxHashMap = retained + .iter() + .enumerate() + .map(|(new_id, shard)| (shard.id, new_id as u32)) + .collect(); + let tree = self + .tree + .as_ref() + .and_then(|tree| tree.filter_map_leaves(&|id| remap.get(&id).copied())); + let total_cross_ingress = retained + .iter() + .map(|shard| u128::from(shard.cross_ingress)) + .sum::(); + let mut out = Vec::new(); out.extend_from_slice(SHARD_MAGIC); - out.extend_from_slice(&self.total_cross_ingress.to_le_bytes()); - out.extend_from_slice(&(self.shards.len() as u32).to_le_bytes()); + out.extend_from_slice(&total_cross_ingress.to_le_bytes()); + out.extend_from_slice(&(retained.len() as u32).to_le_bytes()); let put_addrs = |out: &mut Vec, addrs: &[Address]| { out.extend_from_slice(&(addrs.len() as u32).to_le_bytes()); for a in addrs { out.extend_from_slice(a.as_bytes()); } }; - for sh in &self.shards { - out.extend_from_slice(&sh.id.to_le_bytes()); + for (new_id, sh) in retained.iter().enumerate() { + out.extend_from_slice(&(new_id as u32).to_le_bytes()); out.extend_from_slice(&sh.heartbeats.to_le_bytes()); out.extend_from_slice(&sh.own_size.to_le_bytes()); out.extend_from_slice(&sh.cross_ingress.to_le_bytes()); @@ -1427,7 +1463,7 @@ impl ShardManifest { // Trailing optional bisection-tree section: presence byte then preorder // tree. Appended after the shards so older readers that stop at the shard // count simply ignore it, and `from_bytes` treats end-of-input as `None`. - match &self.tree { + match &tree { Some(t) => { out.push(1); t.put(&mut out); @@ -2931,6 +2967,27 @@ mod tests { assert_eq!(q0.tree, None); } + #[test] + fn manifest_writer_prunes_empty_shards_and_contracts_tree() { + let p = two_clusters(); + // Keep the two clusters in old shards 0 and 2, deliberately leaving shard + // 1 empty. Serialization must emit dense ids 0/1 and contract leaf 1. + let shard_of = vec![0, 0, 0, 2, 2, 2]; + let tree = node(leaf(0), node(leaf(1), leaf(2))); + let m = ShardManifest::build(&p, &shard_of, 3).with_tree(tree); + assert!(m.shards[1].blocks.is_empty()); + + let q = ShardManifest::from_bytes(&m.to_bytes()).unwrap(); + assert_eq!(q.num_shards, 2); + assert_eq!(q.shards.len(), 2); + assert_eq!( + q.shards.iter().map(|shard| shard.id).collect::>(), + vec![0, 1] + ); + assert!(q.shards.iter().all(|shard| !shard.blocks.is_empty())); + assert_eq!(q.tree, Some(node(leaf(0), leaf(1)))); + } + #[test] fn manifest_rejects_tree_shard_mismatch() { let p = two_clusters(); diff --git a/docs/benchmarking.md b/docs/benchmarking.md index c6003c699..a30e93ca5 100644 --- a/docs/benchmarking.md +++ b/docs/benchmarking.md @@ -70,6 +70,13 @@ ix bench run --backend aiur --env InitStd --mode execute \ ix bench run --backend aiur --env InitStd --mode prove \ --consts Nat.add_comm --ixe InitStd.ixe --ceiling-gb 50 +# Optional aggregate W0 diagnostic: prove two singleton CheckEnv shards, +# lift both, then benchmark one flat join. This direct tool invocation emits +# the two child rows plus `Nat.add_comm + String.append` with join-* metrics; +# it is deliberately not part of the scheduled one-constant CI cell. +bench-typecheck --ixe InitStd.ixe \ + --consts Nat.add_comm,String.append --recursive --join --json join.json + # Compare a local run against main's numbers straight from bencher.dev # (no token needed; --consts filters to your constants — the testbed # holds every benched env's): @@ -93,7 +100,7 @@ a PR tree and compare them — exactly what the PR workflow does. | backend | what it measures | tool | |---|---|---| -| `aiur` | the Aiur proof pipeline, per constant: the `ixvm` stage proves the IxVM typecheck, the `fri-verifier` stage executes and proves the in-circuit multi-stark verifier over that fresh proof (the KZG stages fold in as they land, each with its own measure prefix), closed by the pipeline ledger (total-time, pipeline-throughput, pipeline-peak-rss). Each stage's measures carry its prefix (`ixvm-prove-time`, `fri-verifier-fft-cost`, …). The whole system runs under the recursion-tuned FRI parameters. A second mode, execute, is the fast Phase-1-only signal (fft-cost, execute-time, throughput, peak-rss) — unscheduled, local/on-demand only (`!benchmark aiur execute`) | `bench-typecheck --recursive` | +| `aiur` | the Aiur proof pipeline, per constant: the `ixvm` stage proves the IxVM typecheck, the `fri-verifier` stage executes and proves the in-circuit multi-stark verifier over that fresh proof (the KZG stages fold in as they land, each with its own measure prefix), closed by the pipeline ledger (total-time, pipeline-throughput, pipeline-peak-rss). Each stage's measures carry its prefix (`ixvm-prove-time`, `fri-verifier-fft-cost`, …). The whole system runs under the recursion-tuned FRI parameters. A second mode, execute, is the fast Phase-1-only signal (fft-cost, execute-time, throughput, peak-rss) — unscheduled, local/on-demand only (`!benchmark aiur execute`). The direct `--recursive --join` diagnostic takes exactly two constants as singleton `CheckEnv` shards and appends one pair row carrying `join-{execute-time,fft-cost,prove-time,peak-rss,proof-size,verify-time}`; it remains unscheduled until a runner can carry W0. | `bench-typecheck --recursive` | | `zisk` | ZisK VM execute: cycles, execute-time, throughput, peak-rss, constants (pre-shard closure count, same universe as aiur's), shards (the runtime-planned partition size; 1 when the closure fits) | `zisk-host` | | `sp1` | SP1 VM execute (currently disabled in the registry) | `sp1-host` | | `ooc` | out-of-circuit Rust kernel: whole-env row + one full-closure row per constant (`check-time` wraps only the check — the env loads once, outside every row's timed window) | `ix check-rs --json` | @@ -101,6 +108,21 @@ a PR tree and compare them — exactly what the PR workflow does. | `compile` | `ix compile .lean → .ixe`: compile-time, file-size, constants, throughput | `ix compile --json` | | `decompile` | inverse of compile — `ix decompile .ixe → Lean consts`: decompile-time, throughput, peak-rss, constants, file-size (input `.ixe`). Consumes the compile cell's `.ixe` rather than producing one; a malformed decompile reddens the cell. Deep roundtrip fidelity is gated by the canonical checks (`ix validate` / roundtrip tests), which need the original Lean env the `.ixe` can't supply | `ix decompile --json` | +### Aggregate W0 baselines + +The pre-E2 lift-size pin (2026-08-28) uses the 247-function production +recursion system, default q=100/PoW-20 parameters, and the verified +one-constant aggregate fixture. Its lift proof is **7,986,166 bytes**; +the containing `Ixon.Proof` wrapper is 7,986,204 bytes at store address +`090bea6f1c976ef6677fad94f86286295b2eea751fefb7af4c82ce9f84ca1535`. +Positive-PoW grinding may change the proof contents, but its structural byte +length is stable. WP-E2 measures its proof-size delta against this value. + +The box-independent `--queries 0` join wiring gate produced a 246,014-byte +flat-join proof, 10,280,903,348 FFT cost, 6.57 s prove time, 10,798,899,200-byte +peak RSS, and 1.44 ms native verification. Those are smoke values, not W0 cost +estimates; the q=50 join run remains a large-box benchmark. + All tools emit the same rows, and all the constant-driven ones take the same `--consts`/`--consts-file` grammar. The ooc and zkVM cells share per-constant **full-closure** scope, so their delta isolates in-circuit vs out-of-circuit diff --git a/lakefile.lean b/lakefile.lean index 409361693..0b6446848 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -151,6 +151,10 @@ lean_exe «bench-recursion-debug» where root := `Benchmarks.RecursionDebug supportInterpreter := true +lean_exe «bench-aggregate-pair» where + root := `Benchmarks.AggregatePair + supportInterpreter := true + /- The lean4lean replay machinery as an importable lib: the `bench-lean4lean` exe root and the ignored `lean4lean` test runner both import `Benchmarks.Lean4Lean`, and modules under `Benchmarks/` belong to