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

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

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

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

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

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

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

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