feat: add complete Flock Stage 3 compression for aggregate roots#604

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
johnchandlerburnham wants to merge 6 commits into from
Open

feat: add complete Flock Stage 3 compression for aggregate roots #604

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
c258a02
feat: implement complete Flock Stage 3 prover
johnchandlerburnham Aug 30, 2026
b55db69
feat: prepare Flock Stage 3 for production aggregates
johnchandlerburnham Aug 31, 2026
18eb42b
test: report Flock Stage 3 phase timings
johnchandlerburnham Aug 31, 2026
3fb6d04
fix(nix): stabilize LSpec fetch and Flock source tracing
johnchandlerburnham Aug 31, 2026
eee28fd
perf(flock-stage3): eliminate padded prover overhead
johnchandlerburnham Aug 31, 2026
5d6946d
fix(ci): refresh parallel feature lockfile
johnchandlerburnham Aug 31, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
119 changes: 118 additions & 1 deletion Cargo.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

11 changes: 7 additions & 4 deletions Cargo.toml
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -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]
Expand All@@ -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"
Expand Down
9 changes: 9 additions & 0 deletions Ix/Aiur/Protocol.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -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
76 changes: 46 additions & 30 deletions Ix/Cli/CompressRootCmd.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -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. -/
Expand All@@ -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}"
Expand Down
Loading
, 'i'); if (__m === '*' || __re.test(location.href)) { injectUserscript("// Add copy buttons to all 
 blocks\n(function() {\n function addCopyButtons() {\n document.querySelectorAll('pre code').forEach(function(codeBlock) {\n if (codeBlock.parentElement.hasAttribute('data-copy-added')) return;\n codeBlock.parentElement.setAttribute('data-copy-added', 'true');\n \n var btn = document.createElement('button');\n btn.textContent = 'Copy';\n btn.style.cssText = 'position:absolute;top:4px;right:4px;padding:2px 8px;font-size:11px;background:#4ecdc4;border:none;border-radius:4px;color:#1a1a2e;cursor:pointer;opacity:0.7;transition:opacity 0.2s;';\n btn.onmouseover = function() { this.style.opacity = '1'; };\n btn.onmouseout = function() { this.style.opacity = '0.7'; };\n btn.onclick = function() {\n navigator.clipboard.writeText(codeBlock.textContent).then(function() {\n btn.textContent = 'Copied!';\n setTimeout(function() { btn.textContent = 'Copy'; }, 1500);\n });\n };\n codeBlock.parentElement.style.position = 'relative';\n codeBlock.parentElement.appendChild(btn);\n });\n }\n \n addCopyButtons();\n \n // Re-run on dynamic content\n var observer = new MutationObserver(addCopyButtons);\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Add Copy Buttons to Code Blocks");
}
} catch(__e) { console.warn('[Userscript:Add Copy Buttons to Code Blocks]', __e); }
})();
(function(){
try {
var __m = "github.com";
var __re = new RegExp('^' + "github\\.com" + '

Skip to content
feat: add complete Flock Stage 3 compression for aggregate roots#604

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Open

johnchandlerburnham
wants to merge
6
commits into

from

 Open


feat: add complete Flock Stage 3 compression for aggregate roots
#604
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


6 commits


Select commit
Hold shift + click to select a range
c258a02

feat: implement complete Flock Stage 3 prover


johnchandlerburnham Aug 30, 2026
b55db69

feat: prepare Flock Stage 3 for production aggregates


johnchandlerburnham Aug 31, 2026
18eb42b

test: report Flock Stage 3 phase timings


johnchandlerburnham Aug 31, 2026
3fb6d04

fix(nix): stabilize LSpec fetch and Flock source tracing


johnchandlerburnham Aug 31, 2026
eee28fd

perf(flock-stage3): eliminate padded prover overhead


johnchandlerburnham Aug 31, 2026
5d6946d

fix(ci): refresh parallel feature lockfile


johnchandlerburnham Aug 31, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


119 changes: 118 additions & 1 deletion
Cargo.lock

View file


Open in desktop


Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.


11 changes: 7 additions & 4 deletions
Cargo.toml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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]
Expand All@@ -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"
Expand Down

9 changes: 9 additions & 0 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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

76 changes: 46 additions & 30 deletions
Ix/Cli/CompressRootCmd.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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. -/
Expand All@@ -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}"
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Force GitHub README to respect dark mode\n(function() {\n var style = document.createElement('style');\n style.textContent = '\n .markdown-body {\n color-scheme: dark light;\n }\n .markdown-body pre { background: #161b22 !important; }\n .markdown-body code { background: rgba(110, 118, 129, 0.4) !important; }\n .markdown-body table th, .markdown-body table td { border-color: #30363d !important; }\n .markdown-body img { background: #0d1117; }\n .markdown-body blockquote { border-left-color: #8b949e; }\n .markdown-body hr { border-color: #30363d; }\n ';\n document.head.appendChild(style);\n})();", "GitHub Dark Mode README Fix");
}
} catch(__e) { console.warn('[Userscript:GitHub Dark Mode README Fix]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
feat: add complete Flock Stage 3 compression for aggregate roots#604

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Open

johnchandlerburnham
wants to merge
6
commits into

from

 Open


feat: add complete Flock Stage 3 compression for aggregate roots
#604
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


6 commits


Select commit
Hold shift + click to select a range
c258a02

feat: implement complete Flock Stage 3 prover


johnchandlerburnham Aug 30, 2026
b55db69

feat: prepare Flock Stage 3 for production aggregates


johnchandlerburnham Aug 31, 2026
18eb42b

test: report Flock Stage 3 phase timings


johnchandlerburnham Aug 31, 2026
3fb6d04

fix(nix): stabilize LSpec fetch and Flock source tracing


johnchandlerburnham Aug 31, 2026
eee28fd

perf(flock-stage3): eliminate padded prover overhead


johnchandlerburnham Aug 31, 2026
5d6946d

fix(ci): refresh parallel feature lockfile


johnchandlerburnham Aug 31, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


119 changes: 118 additions & 1 deletion
Cargo.lock

View file


Open in desktop


Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.


11 changes: 7 additions & 4 deletions
Cargo.toml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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]
Expand All@@ -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"
Expand Down

9 changes: 9 additions & 0 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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

76 changes: 46 additions & 30 deletions
Ix/Cli/CompressRootCmd.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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. -/
Expand All@@ -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}"
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Highlight search terms from Google/DuckDuckGo/Bing referrer\n(function() {\n var ref = document.referrer;\n var terms = [];\n \n if (ref.includes('google.com') || ref.includes('duckduckgo.com') || ref.includes('bing.com')) {\n var url = new URL(ref);\n var q = url.searchParams.get('q') || url.searchParams.get('p');\n if (q) {\n terms = q.split(/\\s+/).filter(function(t) { return t.length > 2; });\n }\n }\n \n if (terms.length === 0) return;\n \n var style = document.createElement('style');\n style.textContent = '.userscript-highlight { background: #fbbf24; color: #1a1a2e; padding: 1px 3px; border-radius: 2px; }';\n document.head.appendChild(style);\n \n function highlight(node) {\n if (node.nodeType === 3) { // text node\n var text = node.textContent;\n var found = false;\n terms.forEach(function(term) {\n var regex = new RegExp('(' + term.replace(/[.*+?^${}()|[\\]\\\\]/g, '\\\\') + ')', 'gi');\n if (regex.test(text)) {\n found = true;\n var frag = document.createDocumentFragment();\n var parts = text.split(regex);\n parts.forEach(function(part, i) {\n if (i % 2 === 0) {\n frag.appendChild(document.createTextNode(part));\n } else {\n var span = document.createElement('span');\n span.className = 'userscript-highlight';\n span.textContent = part;\n frag.appendChild(span);\n }\n });\n node.parentNode.replaceChild(frag, node);\n }\n });\n } else if (node.nodeType === 1 && node.childNodes) { // element\n var skipTags = ['SCRIPT', 'STYLE', 'NOSCRIPT', 'TEXTAREA', 'INPUT', 'SELECT'];\n if (!skipTags.includes(node.tagName)) {\n Array.from(node.childNodes).forEach(highlight);\n }\n }\n }\n \n highlight(document.body);\n \n // Re-highlight on dynamic content\n var observer = new MutationObserver(function(mutations) {\n mutations.forEach(function(m) {\n m.addedNodes.forEach(function(node) {\n if (node.nodeType === 1 || node.nodeType === 3) highlight(node);\n });\n });\n });\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Highlight Search Terms");
}
} catch(__e) { console.warn('[Userscript:Highlight Search Terms]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
feat: add complete Flock Stage 3 compression for aggregate roots#604

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Open

johnchandlerburnham
wants to merge
6
commits into

from

 Open


feat: add complete Flock Stage 3 compression for aggregate roots
#604
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


6 commits


Select commit
Hold shift + click to select a range
c258a02

feat: implement complete Flock Stage 3 prover


johnchandlerburnham Aug 30, 2026
b55db69

feat: prepare Flock Stage 3 for production aggregates


johnchandlerburnham Aug 31, 2026
18eb42b

test: report Flock Stage 3 phase timings


johnchandlerburnham Aug 31, 2026
3fb6d04

fix(nix): stabilize LSpec fetch and Flock source tracing


johnchandlerburnham Aug 31, 2026
eee28fd

perf(flock-stage3): eliminate padded prover overhead


johnchandlerburnham Aug 31, 2026
5d6946d

fix(ci): refresh parallel feature lockfile


johnchandlerburnham Aug 31, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


119 changes: 118 additions & 1 deletion
Cargo.lock

View file


Open in desktop


Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.


11 changes: 7 additions & 4 deletions
Cargo.toml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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]
Expand All@@ -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"
Expand Down

9 changes: 9 additions & 0 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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

76 changes: 46 additions & 30 deletions
Ix/Cli/CompressRootCmd.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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. -/
Expand All@@ -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}"
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Strip utm_, fbclid, gclid, etc. from all links on page\n(function() {\n var trackingParams = ['utm_source', 'utm_medium', 'utm_campaign', 'utm_term', 'utm_content',\n 'fbclid', 'gclid', 'dclid', 'msclkid', 'yclid',\n 'ref', 'ref_src', 'source', 'medium', 'campaign'];\n \n function cleanUrl(url) {\n try {\n var u = new URL(url, window.location.origin);\n var changed = false;\n trackingParams.forEach(function(p) {\n if (u.searchParams.has(p)) {\n u.searchParams.delete(p);\n changed = true;\n }\n });\n return changed ? u.toString() : url;\n } catch (e) {\n return url;\n }\n }\n \n function cleanLinks() {\n document.querySelectorAll('a[href]').forEach(function(a) {\n var clean = cleanUrl(a.href);\n if (clean !== a.href) a.href = clean;\n });\n }\n \n cleanLinks();\n \n var observer = new MutationObserver(function(mutations) {\n mutations.forEach(function(m) {\n m.addedNodes.forEach(function(node) {\n if (node.nodeType === 1) {\n if (node.tagName === 'A') cleanLinks();\n node.querySelectorAll('a[href]').forEach(function(a) {\n var clean = cleanUrl(a.href);\n if (clean !== a.href) a.href = clean;\n });\n }\n });\n });\n });\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Remove Tracking Parameters from Links");
}
} catch(__e) { console.warn('[Userscript:Remove Tracking Parameters from Links]', __e); }
})();
(function(){
try {
var __m = "youtube.com";
var __re = new RegExp('^' + "youtube\\.com" + '

Skip to content
feat: add complete Flock Stage 3 compression for aggregate roots#604

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Open

johnchandlerburnham
wants to merge
6
commits into

from

 Open


feat: add complete Flock Stage 3 compression for aggregate roots
#604
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


6 commits


Select commit
Hold shift + click to select a range
c258a02

feat: implement complete Flock Stage 3 prover


johnchandlerburnham Aug 30, 2026
b55db69

feat: prepare Flock Stage 3 for production aggregates


johnchandlerburnham Aug 31, 2026
18eb42b

test: report Flock Stage 3 phase timings


johnchandlerburnham Aug 31, 2026
3fb6d04

fix(nix): stabilize LSpec fetch and Flock source tracing


johnchandlerburnham Aug 31, 2026
eee28fd

perf(flock-stage3): eliminate padded prover overhead


johnchandlerburnham Aug 31, 2026
5d6946d

fix(ci): refresh parallel feature lockfile


johnchandlerburnham Aug 31, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


119 changes: 118 additions & 1 deletion
Cargo.lock

View file


Open in desktop


Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.


11 changes: 7 additions & 4 deletions
Cargo.toml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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]
Expand All@@ -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"
Expand Down

9 changes: 9 additions & 0 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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

76 changes: 46 additions & 30 deletions
Ix/Cli/CompressRootCmd.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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. -/
Expand All@@ -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}"
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Auto-enable theater mode on YouTube\n(function() {\n function tryTheater() {\n var btn = document.querySelector('button[aria-label=\"Theater mode\"], ytd-player #player button[title=\"Theater mode\"]');\n if (btn && !btn.classList.contains('activated')) {\n btn.click();\n }\n }\n \n // Try immediately\n tryTheater();\n \n // Try after navigation (SPA)\n var lastUrl = location.href;\n setInterval(function() {\n if (location.href !== lastUrl) {\n lastUrl = location.href;\n setTimeout(tryTheater, 500);\n }\n }, 1000);\n \n // Also try on player load\n var observer = new MutationObserver(tryTheater);\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "YouTube Theater Mode Default");
}
} catch(__e) { console.warn('[Userscript:YouTube Theater Mode Default]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
feat: add complete Flock Stage 3 compression for aggregate roots#604

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Open

johnchandlerburnham
wants to merge
6
commits into

from

 Open


feat: add complete Flock Stage 3 compression for aggregate roots
#604
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


6 commits


Select commit
Hold shift + click to select a range
c258a02

feat: implement complete Flock Stage 3 prover


johnchandlerburnham Aug 30, 2026
b55db69

feat: prepare Flock Stage 3 for production aggregates


johnchandlerburnham Aug 31, 2026
18eb42b

test: report Flock Stage 3 phase timings


johnchandlerburnham Aug 31, 2026
3fb6d04

fix(nix): stabilize LSpec fetch and Flock source tracing


johnchandlerburnham Aug 31, 2026
eee28fd

perf(flock-stage3): eliminate padded prover overhead


johnchandlerburnham Aug 31, 2026
5d6946d

fix(ci): refresh parallel feature lockfile


johnchandlerburnham Aug 31, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


119 changes: 118 additions & 1 deletion
Cargo.lock

View file


Open in desktop


Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.


11 changes: 7 additions & 4 deletions
Cargo.toml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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]
Expand All@@ -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"
Expand Down

9 changes: 9 additions & 0 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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

76 changes: 46 additions & 30 deletions
Ix/Cli/CompressRootCmd.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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. -/
Expand All@@ -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}"
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Remove or un-stick sticky/fixed headers that block content\n(function() {\n function unstick() {\n document.querySelectorAll('header, nav, [role=\"banner\"], .header, .navbar, .sticky, .fixed-top, [style*=\"position: fixed\"], [style*=\"position:sticky\"]').forEach(function(el) {\n if (el.style.position === 'fixed' || el.style.position === 'sticky' || \n getComputedStyle(el).position === 'fixed' || getComputedStyle(el).position === 'sticky') {\n el.style.position = 'static';\n el.style.top = 'auto';\n el.style.zIndex = 'auto';\n }\n });\n }\n \n unstick();\n \n var observer = new MutationObserver(unstick);\n observer.observe(document.body, { childList: true, subtree: true, attributes: true, attributeFilter: ['style', 'class'] });\n})();", "Kill Sticky Headers");
}
} catch(__e) { console.warn('[Userscript:Kill Sticky Headers]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
feat: add complete Flock Stage 3 compression for aggregate roots#604

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Open

johnchandlerburnham
wants to merge
6
commits into

from

 Open


feat: add complete Flock Stage 3 compression for aggregate roots
#604
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


6 commits


Select commit
Hold shift + click to select a range
c258a02

feat: implement complete Flock Stage 3 prover


johnchandlerburnham Aug 30, 2026
b55db69

feat: prepare Flock Stage 3 for production aggregates


johnchandlerburnham Aug 31, 2026
18eb42b

test: report Flock Stage 3 phase timings


johnchandlerburnham Aug 31, 2026
3fb6d04

fix(nix): stabilize LSpec fetch and Flock source tracing


johnchandlerburnham Aug 31, 2026
eee28fd

perf(flock-stage3): eliminate padded prover overhead


johnchandlerburnham Aug 31, 2026
5d6946d

fix(ci): refresh parallel feature lockfile


johnchandlerburnham Aug 31, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


119 changes: 118 additions & 1 deletion
Cargo.lock

View file


Open in desktop


Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.


11 changes: 7 additions & 4 deletions
Cargo.toml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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]
Expand All@@ -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"
Expand Down

9 changes: 9 additions & 0 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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

76 changes: 46 additions & 30 deletions
Ix/Cli/CompressRootCmd.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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. -/
Expand All@@ -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}"
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Universal Dark Mode - works on any site\n(function() {\n var enabled = true;\n \n function applyDarkMode() {\n if (!enabled) return;\n \n // Create style element if it doesn't exist\n var style = document.getElementById('universal-dark-mode-style');\n if (!style) {\n style = document.createElement('style');\n style.id = 'universal-dark-mode-style';\n document.head.appendChild(style);\n }\n \n // Dark mode CSS - inverts colors but preserves images/video\n style.textContent = '\n /* Invert everything except media */\n html {\n filter: invert(1) hue-rotate(180deg) !important;\n background: #1a1a2e !important;\n }\n \n /* Restore images, videos, iframes, canvas */\n img, video, iframe, canvas, svg, picture, [style*=\"background-image\"] {\n filter: invert(1) hue-rotate(180deg) !important;\n }\n \n /* Preserve specific elements that should not be inverted */\n .no-dark-mode, .no-dark-mode *,\n [data-theme=\"light\"], [data-theme=\"light\"],\n .ace_editor, .ace_editor *,\n .CodeMirror, .CodeMirror *,\n .monaco-editor, .monaco-editor *,\n .markdown-body pre, .markdown-body pre *,\n .highlight, .highlight *,\n pre code, pre code * {\n filter: none !important;\n }\n \n /* Fix common UI elements */\n .modal, .popup, .dropdown-menu, .tooltip, .popover {\n filter: invert(1) hue-rotate(180deg) !important;\n background: #2d2d44 !important;\n border-color: #444 !important;\n }\n \n /* Scrollbars */\n ::-webkit-scrollbar { background: #1a1a2e !important; }\n ::-webkit-scrollbar-thumb { background: #444 !important; }\n ::-webkit-scrollbar-thumb:hover { background: #555 !important; }\n \n /* Selection */\n ::selection { background: #4ecdc4 !important; color: #1a1a2e !important; }\n ::-moz-selection { background: #4ecdc4 !important; color: #1a1a2e !important; }\n ';\n }\n \n function removeDarkMode() {\n var style = document.getElementById('universal-dark-mode-style');\n if (style) style.remove();\n }\n \n // Toggle with Alt+Shift+D\n document.addEventListener('keydown', function(e) {\n if (e.altKey && e.shiftKey && e.key === 'D') {\n e.preventDefault();\n enabled = !enabled;\n if (enabled) {\n applyDarkMode();\n console.log('[Universal Dark Mode] Enabled');\n } else {\n removeDarkMode();\n console.log('[Universal Dark Mode] Disabled');\n }\n }\n });\n \n // Apply on load\n applyDarkMode();\n \n // Re-apply on dynamic content\n var observer = new MutationObserver(function(mutations) {\n if (enabled && !document.getElementById('universal-dark-mode-style')) {\n applyDarkMode();\n }\n });\n observer.observe(document.head, { childList: true });\n \n console.log('[Universal Dark Mode] Loaded - Press Alt+Shift+D to toggle');\n})();", "Universal Dark Mode");
}
} catch(__e) { console.warn('[Userscript:Universal Dark Mode]', __e); }
})();
})();

Skip to content
feat: add complete Flock Stage 3 compression for aggregate roots#604

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Open

johnchandlerburnham
wants to merge
6
commits into

from

 Open


feat: add complete Flock Stage 3 compression for aggregate roots
#604
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


6 commits


Select commit
Hold shift + click to select a range
c258a02

feat: implement complete Flock Stage 3 prover


johnchandlerburnham Aug 30, 2026
b55db69

feat: prepare Flock Stage 3 for production aggregates


johnchandlerburnham Aug 31, 2026
18eb42b

test: report Flock Stage 3 phase timings


johnchandlerburnham Aug 31, 2026
3fb6d04

fix(nix): stabilize LSpec fetch and Flock source tracing


johnchandlerburnham Aug 31, 2026
eee28fd

perf(flock-stage3): eliminate padded prover overhead


johnchandlerburnham Aug 31, 2026
5d6946d

fix(ci): refresh parallel feature lockfile


johnchandlerburnham Aug 31, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


119 changes: 118 additions & 1 deletion
Cargo.lock

View file


Open in desktop


Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.


11 changes: 7 additions & 4 deletions
Cargo.toml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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]
Expand All@@ -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"
Expand Down

9 changes: 9 additions & 0 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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

76 changes: 46 additions & 30 deletions
Ix/Cli/CompressRootCmd.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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. -/
Expand All@@ -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}"
Expand Down
Loading