feat: compress aggregate roots with SP1

Cargo.toml

@@ -10,10 +10,10 @@ members = [
   "crates/ixon",
   "crates/kernel",
 ]
-# `zisk/` and `sp1/` are their own Cargo workspaces (guest + host) built via
-# the respective zkVM toolchains; excluded so host workspace ops don't pick
-# them up.
-exclude = ["zisk", "sp1", "multi-stark"]
+# `zisk/`, `sp1/`, and `sp1-compress/` are their own Cargo workspaces built
+# via their respective zkVM toolchains; excluded so host workspace ops don't
+# pick them up.
+exclude = ["zisk", "sp1", "sp1-compress", "multi-stark"]
 resolver = "2"
 
 [profile.dev]

Ix/Aiur/Protocol.lean

@@ -418,6 +418,25 @@ abbrev functionChannel : G := .ofNat 0
 def buildClaim (funIdx : Bytecode.FunIdx) (input output : Array G) :=
   #[functionChannel, .ofNat funIdx] ++ input ++ output
 
+/-- Verify one Aiur recursion proof inside the SP1 aggregate-root guest and
+run the selected SP1 terminal stage. The public statement is the
+domain-separated recursion-vk digest, FRI parameters, and exact 18-word outer
+claim. `output` receives the SDK proof container; `onchainOutput` receives raw
+Groth16/Plonk bytes. Without the Cargo `sp1` feature this binding returns a
+descriptive error while remaining linkable. -/
+@[extern "rs_sp1_compress_aggregate_root"]
+opaque sp1CompressAggregateRoot : @& ByteArray → @& ByteArray → @& ByteArray →
+  @& FriParameters → @& String → @& String → @& String → Except String Unit
+
+/-- Verify and compress the fully audited 2026-09-03 Mathlib aggregate root
+with its version-pinned Aiur-FRI verifier guest. The historical verifying key,
+outer claim, and FRI parameters are compiled into the host; only the exact
+dated proof payload is accepted. This is an explicit compatibility entrypoint,
+never a fallback from `sp1CompressAggregateRoot`. -/
+@[extern "rs_sp1_compress_mathlib_2026_09_03"]
+opaque sp1CompressMathlib20260903 : @& ByteArray → @& String → @& String →
+  @& String → Except String Unit
+
 end Aiur
 
 end

Ix/Cli/CompressRootCmd.lean

@@ -0,0 +1,174 @@
+/-
+`ix compress-root ROOT_ADDRESS` turns one closed, persisted `ix_aggr` root
+into an SP1 proof and, by default, a final Groth16 SNARK.
+
+The default protocol rebuilds the deterministic recursion backend,
+reconstructs the uniform 18-word outer claim from the wrapper's `CheckEnv`,
+and passes exactly that key/claim/proof triple to the current SP1 guest. A
+separate, explicitly selected compatibility protocol accepts only the audited
+2026-09-03 Mathlib artifact and uses its version-pinned verifier guest.
+
+Open roots are rejected for every proof-producing mode. Execute-only profiling
+may opt into one with `--allow-open-root` so a small retained-subtree fixture
+can exercise the current guest.
+-/
+module
+public import Cli
+public import Ix.Address
+public import Ix.Aiur.Protocol
+public import Ix.Aggr
+public import Ix.Cli.AggregateCmd
+public import Ix.Cli.VerifyCmd
+public import Ix.Ixon
+public import Ix.MultiStark
+public import Ix.Store
+public import Ix.Unsigned
+
+public section
+
+namespace Ix.Cli.CompressRootCmd
+
+inductive Protocol where
+  | current
+  | mathlib20260903
+  deriving BEq, DecidableEq, Repr
+
+def Protocol.label : Protocol → String
+  | .current => "current"
+  | .mathlib20260903 => "mathlib-2026-09-03"
+
+def parseProtocol : String → Except String Protocol
+  | "current" => pure .current
+  | "mathlib-2026-09-03" => pure .mathlib20260903
+  | other => throw s!"unknown aggregate protocol `{other}` \
+(current|mathlib-2026-09-03)"
+
+def mathlib20260903AggregateAddress : Address :=
+  (Address.fromString
+    "c2fdce660eb66899efa303b41d4ca1611a62a688ef20684fdc327739d38bd67f").get!
+
+def mathlib20260903RootAddress : Address :=
+  (Address.fromString
+    "3211abb340539c10220990fb095f8763cb3a364e111ebe57fb518992d42d7382").get!
+
+/-- The legacy guest is an artifact-specific protocol, not a general old
+verifier and never an automatic fallback from the current verifier. -/
+def validateProtocolRoot (protocol : Protocol) (address : Address)
+    (claim : Ix.Claim) : Except String Unit := do
+  match protocol with
+  | .current => pure ()
+  | .mathlib20260903 =>
+    if address != mathlib20260903AggregateAddress then
+      throw s!"protocol mathlib-2026-09-03 accepts only aggregate root \
+{mathlib20260903AggregateAddress}"
+    if claim != .checkEnv mathlib20260903RootAddress none then
+      throw s!"protocol mathlib-2026-09-03 requires the pinned closed claim \
+CheckEnv({mathlib20260903RootAddress}, none)"
+
+private def addrOfHex! (label : String) (s : String) : IO Address := do
+  match Address.fromString s with
+  | some a => pure a
+  | none =>
+    throw <| IO.userError
+      s!"error: {label}: expected 64-char hex (32-byte address), got {s.length}-char {s}"
+
+/-- Canonical guest claim encoding: one little-endian u64 per Goldilocks word. -/
+def outerClaimBytes (claim : Array Aiur.G) : ByteArray :=
+  claim.foldl (init := .empty) fun bytes value => bytes ++ value.val.toLEBytes
+
+/-- Final compression accepts only closed `CheckEnv` roots. The explicit open
+escape hatch is intentionally execute-only: it exists for cycle profiling and
+cannot produce a misleading terminal proof. -/
+def validateBundledClaim (claim : Ix.Claim) (mode : String)
+    (allowOpenRoot : Bool) : Except String Unit := do
+  let .checkEnv _ assumptions := claim
+    | throw "aggregate root wrapper does not contain a CheckEnv claim"
+  if assumptions.isSome then
+    if mode == "execute" && allowOpenRoot then pure ()
+    else throw "aggregate root retains assumptions; final compression requires a closed root"
+  else if allowOpenRoot && mode != "execute" then
+    throw "--allow-open-root is restricted to --mode execute"
+
+def runCompressRootCmd (p : Cli.Parsed) : IO UInt32 := do
+  let roots := (p.variableArgsAs! String).toList
+  let rootHex ← match roots with
+    | [root] => pure root
+    | [] => p.printError "error: expected one aggregate root address"; return 1
+    | _ => p.printError "error: expected exactly one aggregate root address"; return 1
+  let mode := (p.flag? "mode").map (·.as! String) |>.getD "groth16"
+  let protocolName :=
+    (p.flag? "protocol").map (·.as! String) |>.getD "current"
+  let protocol ← match parseProtocol protocolName with
+    | .ok protocol => pure protocol
+    | .error error => IO.eprintln s!"error: {error}"; return 1
+  let allowOpenRoot := p.hasFlag "allow-open-root"
+  let output := (p.flag? "output").map (·.as! String) |>.getD ""
+  let onchainOutput := (p.flag? "onchain-output").map (·.as! String) |>.getD ""
+  let rootAddress ← addrOfHex! "aggregate root" rootHex
+  let wrapper ← match Ixon.Proof.de (← StoreIO.toIO (Store.read rootAddress)) with
+    | .ok wrapper => pure wrapper
+    | .error error =>
+      IO.eprintln s!"error: aggregate wrapper {rootAddress} does not decode: {error}"
+      return 1
+  match validateBundledClaim wrapper.claim mode allowOpenRoot with
+  | .ok () => pure ()
+  | .error error => IO.eprintln s!"error: {error}"; return 1
+  match validateProtocolRoot protocol rootAddress wrapper.claim with
+  | .ok () => pure ()
+  | .error error => IO.eprintln s!"error: {error}"; return 1
+  if protocol == .mathlib20260903 && allowOpenRoot then
+    IO.eprintln "error: --allow-open-root applies only to the current protocol"
+    return 1
+
+  IO.println s!"Compressing aggregate root {rootAddress} with SP1 ({mode})"
+  IO.println s!"  protocol: {protocol.label}"
+  IO.println s!"  bundled claim: {wrapper.claim}"
+  let result ← match protocol with
+    | .current => do
+      let recursionParameters := MultiStark.defaultRecursionParameters
+      let backend ← match ← Ix.Cli.VerifyCmd.buildAggregateBackend recursionParameters with
+        | .ok backend => pure backend
+        | .error error => IO.eprintln s!"error: {error}"; return 1
+      let outerClaim := Ix.Cli.AggregateCmd.aggregateOuterClaim
+        backend.allowed backend.aggrIdx wrapper.claim
+      if outerClaim.size != 18 then
+        IO.eprintln s!"error: internal ix_aggr claim width is {outerClaim.size}, expected 18"
+        return 1
+      IO.println s!"  recursion vk: {Address.blake3 backend.system.vkBytes}"
+      (← IO.getStdout).flush
+      pure <| Aiur.sp1CompressAggregateRoot backend.system.vkBytes
+        (outerClaimBytes outerClaim) wrapper.proof recursionParameters.fri
+        mode output onchainOutput
+    | .mathlib20260903 => do
+      IO.println "  multi-stark: 2892243e674f9a0b3aca9004a8d00c79a23beec1"
+      IO.println "  recursion vk: be6f790a7a978336ab513cb77c9e208a606df72f9167e4a264778da641749768"
+      (← IO.getStdout).flush
+      pure <| Aiur.sp1CompressMathlib20260903 wrapper.proof mode output onchainOutput
+  match result with
+  | .ok () =>
+    IO.println s!"ok: SP1 {mode} accepted aggregate root {rootAddress} \
+under protocol {protocol.label}"
+    return 0
+  | .error error =>
+    IO.eprintln s!"error: SP1 root compression failed: {error}"
+    return 1
+
+end Ix.Cli.CompressRootCmd
+
+open Ix.Cli.CompressRootCmd in
+def compressRootCmd : Cli.Cmd := `[Cli|
+  "compress-root" VIA runCompressRootCmd;
+  "Compress one closed ix_aggr root through SP1 to a final SNARK (build with IX_SP1=1)"
+
+  FLAGS:
+    "mode" : String;           "SP1 stage: execute | core | compressed | groth16 | plonk (default: groth16)."
+    "protocol" : String;       "Verifier protocol: current | mathlib-2026-09-03 (default: current)."
+    "output" : String;         "Save the verified SP1 SDK proof container at this path."
+    "onchain-output" : String; "For groth16/plonk, save the raw onchain proof bytes at this path."
+    "allow-open-root";         "Allow a root retaining assumptions for execute-only guest profiling; never permits proof generation."
+
+  ARGS:
+    ...root : String; "Exactly one 32-byte store address of a persisted aggregate root."
+]
+
+end

Ix/Cli/VerifyCmd.lean

@@ -149,7 +149,7 @@ def auditAggregateConstants (env : Ixon.Env) (statement : Aggr.CheckEnvTrees) :
 
 /-- Build the two deterministic systems whose identities are committed by an
 aggregate root: the IxVM vk and the single-entrypoint recursion vk. -/
-private def buildAggregateBackend
+def buildAggregateBackend
     (recursionParameters : MultiStark.RecursionParameters) :
     IO (Except String AggregateBackend) := do
   let ixvmCompiled ← match IxVM.ixVM with

Main.lean

@@ -11,6 +11,7 @@ import Ix.Cli.ValidateLeanCmd
 import Ix.Cli.ClaimCmd
 import Ix.Cli.CatalogCmd
 import Ix.Cli.CompileCmd
+import Ix.Cli.CompressRootCmd
 import Ix.Cli.DecompileCmd
 import Ix.Cli.DiffCmd
 import Ix.Cli.IngressCmd
@@ -52,6 +53,7 @@ def ixCmd : Cli.Cmd := `[Cli|
     treeCmd;
     profileCmd;
     proveCmd;
+    compressRootCmd;
     shardCmd;
     codegenCmd;
     verifyCmd;

README.md

@@ -339,6 +339,39 @@ the [SP1 docs](https://docs.succinct.xyz/docs/sp1/getting-started/install).
    with progressive backoff. It is a pass-through no-op when `SP1_PROVER` is not
    `cuda`.
 
+#### Compressing an Aiur aggregate root
+
+`ix compress-root` verifies a closed Stage 2 Aiur-FRI root inside a dedicated
+SP1 guest and can run SP1's recursion tail through a Groth16 or Plonk proof.
+Build the connector explicitly, then name the root object already present in
+the Ix store:
+
+```console
+IX_SP1=1 lake build ix
+lake exe ix compress-root ROOT_ADDRESS --mode execute
+WITHOUT_VK_VERIFICATION=1 lake exe ix compress-root ROOT_ADDRESS --mode groth16 \
+  --output root.sp1 --onchain-output root.groth16
+```
+
+The default `--protocol current` deterministically rebuilds the current
+`ix_aggr` verifying key and checks the proof natively before entering SP1.
+Modes are `execute`, `core`, `compressed`, `groth16`, and `plonk`.
+
+The fully audited Mathlib root produced on 2026-09-03 predates the current
+Multi-STARK wire protocol. It has a deliberately separate compatibility guest:
+
+```console
+lake exe ix compress-root \
+  c2fdce660eb66899efa303b41d4ca1611a62a688ef20684fdc327739d38bd67f \
+  --protocol mathlib-2026-09-03 --mode execute
+```
+
+That protocol accepts only the dated wrapper address, closed claim, proof
+digest, Aiur verifying key, and FRI parameters recorded in
+`Tests/Fixtures/Aggregate/mathlib-2026-09-03/PROVENANCE.md`. It is never an
+automatic fallback: omitting `--protocol` continues to use—and reject an old
+proof under—the current verifier.
+
 ### Proving under Zisk
 
 The Ix kernel typechecker also has a Zisk guest at `zisk/guest/` driven by a

Tests/Aggr.lean

@@ -5,6 +5,7 @@ public import Ix.Aggr
 public import Ix.Claim
 public import Ix.AssumptionTree
 public import Ix.Cli.AggregateCmd
+public import Ix.Cli.CompressRootCmd
 public import Tests.MultiStark
 
 /-!
@@ -531,6 +532,39 @@ def smokeSuite : IO UInt32 := do
       shapeWeightsBounded,
     test "driver specs use uniform aggregate claims and cache version 2"
       uniformDriverClaims,
+    test "final compression accepts a closed CheckEnv root"
+      ((Ix.Cli.CompressRootCmd.validateBundledClaim
+        (.checkEnv a none) "groth16" false).isOk),
+    test "final compression rejects a root retaining assumptions"
+      (!(Ix.Cli.CompressRootCmd.validateBundledClaim
+        (.checkEnv a (some b)) "groth16" false).isOk),
+    test "execute profiling requires an explicit open-root opt-in"
+      (!(Ix.Cli.CompressRootCmd.validateBundledClaim
+        (.checkEnv a (some b)) "execute" false).isOk),
+    test "execute profiling may opt into an open root"
+      ((Ix.Cli.CompressRootCmd.validateBundledClaim
+        (.checkEnv a (some b)) "execute" true).isOk),
+    test "open-root opt-in cannot be used by a proof-producing mode"
+      (!(Ix.Cli.CompressRootCmd.validateBundledClaim
+        (.checkEnv a none) "groth16" true).isOk),
+    test "final compression rejects non-CheckEnv claims"
+      (!(Ix.Cli.CompressRootCmd.validateBundledClaim
+        (.check a none) "execute" false).isOk),
+    test "historical compression protocol is selected explicitly"
+      ((Ix.Cli.CompressRootCmd.parseProtocol "mathlib-2026-09-03").isOk),
+    test "unknown compression protocols are rejected"
+      (!(Ix.Cli.CompressRootCmd.parseProtocol "legacy-ish").isOk),
+    test "historical protocol accepts its exact dated root and claim"
+      ((Ix.Cli.CompressRootCmd.validateProtocolRoot .mathlib20260903
+        Ix.Cli.CompressRootCmd.mathlib20260903AggregateAddress
+        (.checkEnv Ix.Cli.CompressRootCmd.mathlib20260903RootAddress none)).isOk),
+    test "historical protocol rejects another wrapper address"
+      (!(Ix.Cli.CompressRootCmd.validateProtocolRoot .mathlib20260903 a
+        (.checkEnv Ix.Cli.CompressRootCmd.mathlib20260903RootAddress none)).isOk),
+    test "historical protocol rejects another bundled claim"
+      (!(Ix.Cli.CompressRootCmd.validateProtocolRoot .mathlib20260903
+        Ix.Cli.CompressRootCmd.mathlib20260903AggregateAddress
+        (.checkEnv a none)).isOk),
     expectOk "wrap of an IxVM child accepts" wrapIxvm,
     expectOk "wrap of a self child accepts" wrapSelf,
     expectOk "pair (IxVM, IxVM) accepts" pairII,

Tests/AggrSemantics.lean

@@ -92,7 +92,8 @@ environment and 52.5 MB manifest are identified in the adjacent provenance
 record rather than checked in. This proof predates the a8aab731 protocol bump:
 the gate re-hashes and decodes the exact wrapper, pins its unconditional root
 claim, and ensures the current backend rejects it at that protocol boundary
-instead of accidentally accepting an incompatible proof. -/
+instead of accidentally accepting an incompatible proof. The separately
+selected SP1 compatibility guest is tested by the connector package. -/
 private def stage2FixturePinnedAndFenced : IO Bool := do
   try
     unless (← stage2FixturePath.pathExists) do
@@ -132,7 +133,7 @@ private def stage2FixturePinnedAndFenced : IO Bool := do
         args := #[s!"HOME={home}", exe.toString, "verify", "--aggregate",
           stage2FixtureAddressHex] }
       if out.exitCode == 0 then
-        IO.eprintln "obsolete Stage 2 fixture unexpectedly verified under the current protocol"
+        IO.eprintln "historical Stage 2 fixture unexpectedly verified under the current protocol"
         return false
       unless out.stderr.contains "InvalidProofShape" ||
           out.stdout.contains "InvalidProofShape" do
@@ -762,7 +763,7 @@ def semanticSuite : IO UInt32 := do
       shardPrepPreservesSemantics,
     test "verified aggregate proof audit certifies every fixture constant"
       aggregateProofAuditsEveryConstant,
-    test "dated Mathlib Stage 2 proof is pinned and fenced at its protocol boundary"
+    test "dated Mathlib Stage 2 proof is pinned and rejected by the current protocol"
       productionStage2FixturePinnedAndFenced,
     test "aggregate constant audit rejects an omitted environment constant"
       missingConstantRejected,