feat: add complete Flock Stage 3 compression for aggregate roots

Cargo.toml

@@ -9,11 +9,12 @@ members = [
   "crates/ixvm-codegen",
   "crates/ixon",
   "crates/kernel",
+  "crates/terminal",
 ]
-# `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"]
+# `zisk/`, `sp1/`, `sp1-compress/`, and `flock-stage3/` are isolated Cargo
+# workspaces with heavyweight or specialized toolchains; keep normal host
+# workspace operations from picking them up.
+exclude = ["zisk", "sp1", "sp1-compress", "flock-stage3", "multi-stark"]
 resolver = "2"
 
 [profile.dev]
@@ -40,13 +41,15 @@ ix-common = { path = "crates/common" }
 ix-compile = { path = "crates/compile" }
 ixon = { path = "crates/ixon" }
 ix-kernel = { path = "crates/kernel" }
+ix-terminal = { path = "crates/terminal" }
 
 # lean-ffi tree (lean-ffi crate + factored-out bignat sub-crate)
 bignat = { git = "https://github.com/argumentcomputer/lean-ffi.git", rev = "93c7e52952ae94546be08313f4ff3922984c84d5" }
 lean-ffi = { git = "https://github.com/argumentcomputer/lean-ffi.git", rev = "93c7e52952ae94546be08313f4ff3922984c84d5" }
 
 # External shared deps
 anyhow = "1"
+bincode = { version = "2.0.1", features = ["serde"] }
 blake3 = "1.8.4"
 dashmap = "6.1.0"
 hashbrown = "0.15"

Ix/Aiur/Protocol.lean

@@ -296,6 +296,15 @@ descriptive error while remaining linkable. -/
 opaque sp1CompressAggregateRoot : @& ByteArray → @& ByteArray → @& ByteArray →
   @& FriParameters → @& String → @& String → @& String → Except String Unit
 
+/-- Compile/evaluate (`preflight`) or prove (`prove`) the complete no-RISC-V
+Flock Stage 3 relation for one Aiur aggregate root. `prove` requires an output
+path and atomically installs the verified `Stage3ArtifactV1`. Without the Cargo
+`flock` feature this binding returns a descriptive error while remaining
+linkable. -/
+@[extern "rs_flock_stage3_aggregate_root"]
+opaque flockStage3AggregateRoot : @& ByteArray → @& ByteArray → @& ByteArray →
+  @& FriParameters → @& String → @& String → Except String Unit
+
 end Aiur
 
 end

Ix/Cli/CompressRootCmd.lean

@@ -24,17 +24,46 @@ 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
 
+/-- Canonical terminal-backend transport reconstructed from a persisted
+aggregate wrapper. SP1 and Flock share this adapter so they cannot drift on the
+recursion key, outer claim, proof bytes, or FRI parameters. -/
+structure AggregateRootInputs where
+  rootAddress : Address
+  bundledClaim : Ix.Claim
+  verifyingKey : ByteArray
+  outerClaim : ByteArray
+  proof : ByteArray
+  fri : Aiur.FriParameters
+
+def prepareAggregateRootInputs (rootHex : String) : IO (Except String AggregateRootInputs) := do
+  let some rootAddress := Address.fromString rootHex
+    | return .error s!"aggregate root: expected 64-char hex (32-byte address), \
+        got {rootHex.length}-char {rootHex}"
+  let wrapper ← match Ixon.Proof.de (← StoreIO.toIO (Store.read rootAddress)) with
+    | .ok wrapper => pure wrapper
+    | .error error =>
+      return .error s!"aggregate wrapper {rootAddress} does not decode: {error}"
+  let recursionParameters := MultiStark.defaultRecursionParameters
+  let backend ← match ← Ix.Cli.VerifyCmd.buildAggregateBackend recursionParameters with
+    | .ok backend => pure backend
+    | .error error => return .error error
+  let outerClaim := Ix.Cli.AggregateCmd.aggregateOuterClaim
+    backend.allowed backend.aggrIdx wrapper.claim
+  if outerClaim.size != 18 then
+    return .error s!"internal ix_aggr claim width is {outerClaim.size}, expected 18"
+  return .ok {
+    rootAddress
+    bundledClaim := wrapper.claim
+    verifyingKey := backend.system.vkBytes
+    outerClaim := outerClaimBytes outerClaim
+    proof := wrapper.proof
+    fri := recursionParameters.fri
+  }
+
 /-- 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. -/
@@ -58,35 +87,22 @@ def runCompressRootCmd (p : Cli.Parsed) : IO UInt32 := do
   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
+  let inputs ← match ← prepareAggregateRootInputs rootHex with
+    | .ok inputs => pure inputs
+    | .error error => IO.eprintln s!"error: {error}"; return 1
+  match validateBundledClaim inputs.bundledClaim 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.println s!"Compressing aggregate root {inputs.rootAddress} with SP1 ({mode})"
+  IO.println s!"  bundled claim: {inputs.bundledClaim}"
+  IO.println s!"  recursion vk: {Address.blake3 inputs.verifyingKey}"
   (← IO.getStdout).flush
-  match Aiur.sp1CompressAggregateRoot backend.system.vkBytes
-      (outerClaimBytes outerClaim) wrapper.proof recursionParameters.fri
+  match Aiur.sp1CompressAggregateRoot inputs.verifyingKey
+      inputs.outerClaim inputs.proof inputs.fri
       mode output onchainOutput with
   | .ok () =>
-    IO.println s!"ok: SP1 {mode} accepted aggregate root {rootAddress}"
+    IO.println s!"ok: SP1 {mode} accepted aggregate root {inputs.rootAddress}"
     return 0
   | .error error =>
     IO.eprintln s!"error: SP1 root compression failed: {error}"