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

@@ -286,6 +286,16 @@ 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
+
 end Aiur
 
 end

Ix/Cli/CompressRootCmd.lean

@@ -0,0 +1,112 @@
+/-
+`ix compress-root ROOT_ADDRESS` turns one closed, persisted `ix_aggr` root
+into an SP1 proof and, by default, a final Groth16 SNARK.
+
+The command 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 SP1 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 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
+
+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 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
+
+  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!"Compressing aggregate root {rootAddress} with SP1 ({mode})"
+  IO.println s!"  bundled claim: {wrapper.claim}"
+  IO.println s!"  recursion vk: {Address.blake3 backend.system.vkBytes}"
+  (← IO.getStdout).flush
+  match Aiur.sp1CompressAggregateRoot backend.system.vkBytes
+      (outerClaimBytes outerClaim) wrapper.proof recursionParameters.fri
+      mode output onchainOutput with
+  | .ok () =>
+    IO.println s!"ok: SP1 {mode} accepted aggregate root {rootAddress}"
+    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)."
+    "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

@@ -96,7 +96,7 @@ structure ExpectedAggregate where
 
 /-- 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;

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,24 @@ 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),
     expectOk "wrap of an IxVM child accepts" wrapIxvm,
     expectOk "wrap of a self child accepts" wrapSelf,
     expectOk "pair (IxVM, IxVM) accepts" pairII,

crates/aiur/Cargo.toml

@@ -13,12 +13,13 @@ num-bigint = { workspace = true }
 rayon = { workspace = true }
 rustc-hash = { workspace = true }
 tracing = { workspace = true }
-tracing-texray = { workspace = true }
+tracing-texray = { workspace = true, optional = true }
 
 [features]
-default = []
+default = ["texray"]
 parallel = ["multi-stark/parallel"]
 cuda = ["multi-stark/cuda"]
+texray = ["dep:tracing-texray"]
 
 [lints]
 workspace = true

crates/aiur/src/synthesis.rs

@@ -313,6 +313,7 @@ impl AiurSystem {
     input: &[G],
     io_buffer: &mut IOBuffer,
   ) -> (Vec<G>, AiurProof) {
+    #[cfg(feature = "texray")]
     tracing_texray::examine_current();
 
     // Execute the Aiur bytecode.
@@ -393,6 +394,7 @@ impl AiurSystem {
       &mut IOBuffer,
     ) -> Result<(QueryRecord, Vec<G>), ExecError>,
   {
+    #[cfg(feature = "texray")]
     tracing_texray::examine_current();
     let _g = tracing::info_span!("aiur/execute_ixvm").entered();
     let (query_record, output) =
@@ -573,6 +575,23 @@ mod tests {
       ]
     );
     system.verify(&claim, &proof).expect("xor split outputs must verify");
+
+    // The terminal zkVM receives only the serialized verifier key, not the
+    // prover-side `AiurSystem`. Exercise that exact path against a real proof
+    // so codec round trips alone cannot mask a transcript/config mismatch.
+    let vk_bytes = crate::vk_codec::aiur_system_to_bytes(&system)
+      .expect("encode verifier key");
+    let vk = crate::vk_codec::AiurVerifyingKey::from_bytes(&vk_bytes)
+      .expect("decode verifier key");
+    assert_eq!(vk.to_bytes(), vk_bytes, "verifier key is canonical");
+    vk.verify(&claim, &proof).expect("decoded verifier key must verify");
+
+    let mut tampered_claim = claim.clone();
+    tampered_claim[2] += G::ONE;
+    assert!(
+      vk.verify(&tampered_claim, &proof).is_err(),
+      "decoded verifier key must bind the outer claim"
+    );
   }
 
   /// Hand-build a toplevel exercising the two migrated integration paths that

crates/aiur/src/vk_codec.rs

@@ -68,7 +68,7 @@ use multi_stark::{
   lookup::{Lookup, WidthBinding},
   p3_field::{PrimeCharacteristicRing, PrimeField64},
   system::{Circuit, System},
-  types::{Commitment, CommitmentParameters, FriParameters, Val},
+  types::{Commitment, CommitmentParameters, FriParameters, PcsError, Val},
 };
 
 use crate::synthesis::{AiurConfig, AiurSystem};
@@ -502,6 +502,51 @@ pub(crate) fn from_bytes(
   Ok((system, commitment_parameters, fri_parameters))
 }
 
+/// A verifier-only Aiur key decoded from [`aiur_system_to_bytes`].
+///
+/// This is the narrow surface used by zkVM guests: unlike [`AiurSystem`], it
+/// carries neither bytecode nor a prover key, but it can verify a serialized
+/// proof under the exact commitment and FRI parameters embedded in the key.
+pub struct AiurVerifyingKey {
+  system: System<AiurConfig>,
+  commitment_parameters: CommitmentParameters,
+  fri_parameters: FriParameters,
+}
+
+impl AiurVerifyingKey {
+  /// Decode a verifying key and require full input consumption.
+  pub fn from_bytes(bytes: &[u8]) -> Result<Self, String> {
+    from_bytes(bytes).map(|(system, commitment_parameters, fri_parameters)| {
+      Self { system, commitment_parameters, fri_parameters }
+    })
+  }
+
+  /// Re-encode to the canonical Aiur verifying-key wire format.
+  pub fn to_bytes(&self) -> Vec<u8> {
+    to_bytes(&self.system, self.commitment_parameters, self.fri_parameters)
+  }
+
+  pub const fn commitment_parameters(&self) -> CommitmentParameters {
+    self.commitment_parameters
+  }
+
+  pub const fn fri_parameters(&self) -> FriParameters {
+    self.fri_parameters
+  }
+
+  pub fn num_circuits(&self) -> usize {
+    self.system.circuits.len()
+  }
+
+  pub fn verify(
+    &self,
+    claim: &[Val],
+    proof: &crate::synthesis::AiurProof,
+  ) -> Result<(), multi_stark::verifier::VerificationError<PcsError>> {
+    self.system.verify(claim, proof)
+  }
+}
+
 #[cfg(test)]
 mod tests {
   use super::*;

crates/ffi/Cargo.toml

@@ -35,6 +35,10 @@ tracing = { workspace = true }
 tracing-subscriber = { workspace = true }
 tracing-texray = { workspace = true }
 
+# Optional SP1 terminal connector. The default build keeps a linkable error
+# stub; enabling this dependency builds the aggregate-verifier guest ELF.
+sp1-compress-host = { path = "../../sp1-compress/host", optional = true }
+
 # Iroh dependencies
 bytes = { version = "1.10.1", optional = true }
 tokio = { version = "1.44.1", optional = true }
@@ -51,6 +55,8 @@ parallel = ["aiur/parallel"]
 cuda = ["aiur/cuda"]
 test-ffi = []
 net = ["bytes", "tokio", "iroh", "iroh-base", "n0-error", "getrandom", "bincode", "serde"]
+sp1 = ["dep:sp1-compress-host"]
+sp1-cuda = ["sp1", "sp1-compress-host/cuda"]
 
 [lints]
 workspace = true