feat: Add ix decompile CLI, fix Rust decompile perf and tests#490

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

Merged
samuelburnham merged 3 commits into from
Jul 14, 2026
Merged

feat: Add ix decompile CLI, fix Rust decompile perf and tests #490

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
1064f84
perf: Fix ignored-test fallout from #484 and bound decompile/validate…
samuelburnham Jul 13, 2026
41a1876
feat: Add `ix decompile` and its benchmark backend
samuelburnham Jul 13, 2026
ba9a104
test: Cover Rust decompile over the serialized roundtrip
samuelburnham Jul 13, 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
82 changes: 81 additions & 1 deletion .github/workflows/bench-main.yml
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -16,7 +16,10 @@ name: Benchmark main
# 4. ooc-check — restore that `.ixe` and run the out-of-circuit Rust kernel
# (the same kernel, out-of-circuit and parallel — far faster)
# over the whole env, tracking throughput.
# 5. aiur-recursive — the aiur-recursive toy
# 5. decompile — restore that `.ixe` and decompile it back to Lean constants
# (the inverse of step 1); tracks decompile-time /
# throughput / peak-rss.
# 6. aiur-recursive — the aiur-recursive toy
# (bench-recursive-verifier):
# prove fixed tiny statements, run the in-circuit
# multi-stark verifier over each proof, then prove THAT
Expand DownExpand Up@@ -617,3 +620,80 @@ jobs:
--threshold-measure peak-rss --threshold-test percentage
--threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
--threshold-lower-boundary _

# Decompile — the inverse of compile. Restore the compile job's cached
# `.ixe` and decompile it back to Lean constants. One env-keyed row per
# benched env, mirroring the `compile` cell. A malformed decompile exits
# nonzero and reddens this step; deep roundtrip fidelity is gated by the
# canonical checks (`ix validate` / roundtrip tests), not measured here. No
# compiler or Lean toolchain build — `ix decompile` is a Rust FFI pass over
# the cached `.ixe`, so this reuses the staged `ix` binary like ooc-check.
decompile:
name: decompile-${{ matrix.bench }}
needs: [compile, plan]
runs-on: warp-ubuntu-latest-x64-32x
timeout-minutes: 60
strategy:
fail-fast: false
matrix:
bench: ${{ fromJson(needs.plan.outputs.bench-envs) }}
steps:
- uses: actions/checkout@v6
- uses: actions/cache/restore@v5
with:
path: ~/.local/bin
key: bench-bins-${{ github.sha }}
- run: echo "$HOME/.local/bin" >> $GITHUB_PATH
# Provision the toolchain so `ix` finds libleanshared (no package build).
- uses: leanprover/lean-action@v1
with:
auto-config: false
build: false
use-github-cache: false
# (The path list must match the compile job's save exactly.)
- uses: actions/cache/restore@v5
with:
path: |
${{ matrix.bench }}.ixe
zkshards-${{ matrix.bench }}
key: bench-ixe-${{ github.sha }}-${{ matrix.bench }}
fail-on-cache-miss: true
# A malformed decompile exits nonzero → red X here; a clean run's row
# uploads below.
- name: Run decompile benchmark
run: |
ix bench run --backend decompile --env ${{ matrix.bench }} --mode execute \
--ixe ${{ matrix.bench }}.ixe --out bench.json
# Upload whatever clean rows exist even when the run step reddened the
# job — bmf drops every non-ok (rejected/oom) row.
- name: Convert to Bencher Metric Format
id: bmf
if: ${{ !cancelled() }}
run: |
ix bench bmf --in bench.json --out bench-bmf.json
cat bench-bmf.json
# constants is deterministic → pinned (0/0); decompile-time / throughput
# / peak-rss are noisy wall-clock → percentage bounds. file-size (the
# input `.ixe`) duplicates the compile cell's, so it uploads for the
# row's completeness but rides no threshold here.
- uses: ./.github/actions/bencher-track
if: ${{ !cancelled() && steps.bmf.outcome == 'success' }}
with:
testbed: ix-decompile-x64-32x
workload: ix-decompile
file: bench-bmf.json
key: ${{ secrets.BENCHER_API_KEY }}
github-token: ${{ secrets.GITHUB_TOKEN }}
thresholds: |
--threshold-measure constants --threshold-test percentage
--threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0
--threshold-lower-boundary 0
--threshold-measure decompile-time --threshold-test percentage
--threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
--threshold-lower-boundary _
--threshold-measure throughput --threshold-test percentage
--threshold-max-sample-size __WINDOW__ --threshold-upper-boundary _
--threshold-lower-boundary 0.10
--threshold-measure peak-rss --threshold-test percentage
--threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
--threshold-lower-boundary _
12 changes: 7 additions & 5 deletions .github/workflows/bench-pr.yml
View file
Open in desktop
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
# `!benchmark` PR command: run the curated constant set (Benchmarks/Vectors.csv)
# through chosen prover backend(s) and post a main-vs-PR comparison table.
#
# !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [aiur-recursive] | all) [execute]
# !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [decompile] [aiur-recursive] | all) [execute]
# (sp1 is disabled in the registry (Ix/Cli/BenchCmd.lean) — the parser skips it
# with a note in the config summary)
# BENCH_ENVS=InitStd,Mathlib # which compiled envs (default InitStd; case-insensitive;
Expand All@@ -20,10 +20,12 @@
# Phase-1 columns `fft-cost` / `execute-time` measured en route; `zisk` /
# `sp1` / `ooc` run `execute`; `compile` runs `ix compile <env>.lean →
# <env>.ixe` (the same cell bench-main.yml uploads under testbed
# `ix-compile-*`); `aiur-recursive` runs the aiur-recursive toy
# (bench-recursive-verifier's fixed configs — env-independent, so it
# always schedules exactly one cell no matter what BENCH_ENVS says).
# The optional bare `execute` token flips `aiur` to
# `ix-compile-*`); `decompile` runs `ix decompile <env>.ixe` over the
# compile cell's fresh PR `.ixe` (testbed `ix-decompile-*`);
# `aiur-recursive` runs the aiur-recursive toy (bench-recursive-verifier's
# fixed configs — env-independent, so it always schedules exactly one cell
# no matter what BENCH_ENVS says). The optional bare `execute` token flips
# `aiur` to
# execute-only (Phase 1, skipping the prove); bench-main runs both aiur
# modes as separate cells on separate testbeds, so either kind of cell
# fetches a cached main-side baseline from bencher. (aiur's third mode,
Expand Down
8 changes: 4 additions & 4 deletions .github/workflows/bencher-thresholds-reset.yml
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -22,7 +22,7 @@ name: Bencher thresholds reset
# cancel by removing it before merge. Naming convention: one label per token,
# `bencher-thresholds-reset:<token>` where <token> is a workload (a backend
# testbed in Ix/Cli/BenchCmd.lean (backendSpecs) minus its runner-arch suffix:
# `ix-compile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `all` (the merge step expands an `all` label into every workload). Labeling
# requires Triage+, so PR authors from forks cannot self-queue a reset. The
# label shares the command/workflow name; the ref it moves is
Expand All@@ -44,7 +44,7 @@ on:
# GitHub requires literal choice options, so this list stays static:
# keep it (and the jobs' valid= lists below) in sync with the
# backend testbeds in Ix/Cli/BenchCmd.lean (backendSpecs).
options: [ix-compile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
sha:
description: "Commit to anchor to (default: HEAD)"
required: false
Expand DownExpand Up@@ -77,7 +77,7 @@ jobs:
# (backendSpecs) minus the runner-arch suffix. Static because this
# job runs on a cheap runner with no built `ix`; keep in sync when
# adding a backend.
valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ooc-check sp1-check-execute zisk-check-execute"
valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
if [ "$EVENT" = workflow_dispatch ]; then
# Reset the chosen workload(s) at the given commit; no PR scan.
sha="${INPUT_SHA:-$HEAD_SHA}"
Expand DownExpand Up@@ -133,7 +133,7 @@ jobs:
# which the merge job expands into every workload). Same static
# list as the reset job; keep both in sync with backendSpecs in
# Ix/Cli/BenchCmd.lean.
valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ooc-check sp1-check-execute zisk-check-execute"
valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
accepted="$valid all"
# Parse the workload token(s) after the command, lowercased.
workloads=$(printf '%s' "$BODY" \
Expand Down
23 changes: 22 additions & 1 deletion Ix/Cli/BenchCmd.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -185,6 +185,14 @@ def backendSpecs : List BackendSpec := [
{ name := "compile", defaultMode := "execute",
testbeds := [("execute", "ix-compile-x64-32x")],
metrics := [("execute", ["compile-time", "throughput", "peak-rss",
"file-size", "constants"])] },
-- The inverse of compile: decompiles the env's `.ixe` back to Lean
-- constants (roundtrip-verified). Env-keyed like compile, but a `.ixe`
-- CONSUMER — it reuses the compile cell's fresh `.ixe` rather than
-- producing one.
{ name := "decompile", defaultMode := "execute",
testbeds := [("execute", "ix-decompile-x64-32x")],
metrics := [("execute", ["decompile-time", "throughput", "peak-rss",
"file-size", "constants"])] }
]

Expand DownExpand Up@@ -492,6 +500,18 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do
if exit != 0 then
IO.eprintln s!"[bench] ix compile failed (exit {exit})"
return 1
| "decompile" =>
-- The inverse of compile: consume the env's `.ixe` (the compile cell's
-- fresh artifact) and decompile it back to Lean constants. Env-keyed row,
-- like compile. A malformed decompile exits nonzero and reddens the cell;
-- deep roundtrip fidelity is gated by the canonical roundtrip checks
-- (`ix validate` / the roundtrip tests), not measured here.
let ixe ← ensureIxe repo info ((p.flag? "ixe").map (·.as! String))
let ix ← resolveBin repo "ix"
let exit ← runGuarded watchdog ceilingGb ix
#["decompile", ixe, "--json", out, "--json-name", info.name]
if exit != 0 then
IO.eprintln s!"[bench] ix decompile failed (exit {exit})"
| "ooc" =>
let ixe ← ensureIxe repo info ((p.flag? "ixe").map (·.as! String))
let ix ← resolveBin repo "ix"
Expand DownExpand Up@@ -586,6 +606,7 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do
-- row too.
let expected := match backend with
| "compile" => #[info.name]
| "decompile" => #[info.name]
| "ooc" => #[info.name] ++ names
| "aiur-recursive" => (recursiveConfigs.map (·.1)).toArray
| _ => names
Expand DownExpand Up@@ -630,7 +651,7 @@ def benchRunCmd : Cli.Cmd := `[Cli|
"Run one benchmark cell (backend × env × mode), writing benchmark results JSON. Exits 0 on success (rows saved as the local baseline), 3 when the kernel rejected any constant, 1 when no rows were produced."

FLAGS:
backend : String; "aiur | zisk | sp1 | ooc | compile | aiur-recursive"
backend : String; "aiur | zisk | sp1 | ooc | compile | decompile | aiur-recursive"
env : String; "Benchmark env from the registry (default: InitStd)"
mode : String; "prove | execute | recursive (default: the backend's defaultMode)"
out : String; "Benchmark results JSON output path (default: bench.json)"
Expand Down
21 changes: 17 additions & 4 deletions Ix/Cli/BenchPlots.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -54,6 +54,9 @@ def plotTitle (workload measure : String) : String :=
| "ix-compile", "peak-rss" => "Ix Compile Peak RAM Usage"
| "ix-compile", "file-size" => "Ix Environment Size"
| "ix-compile", "constants" => "Ix Input Constants"
| "ix-decompile", "decompile-time" => "Ix Decompile Time"
| "ix-decompile", "throughput" => "Ix Decompile Throughput"
| "ix-decompile", "peak-rss" => "Ix Decompile Peak RAM Usage"
| "aiur-check-prove", "prove-time" => "Aiur Prove Time"
| "aiur-check-prove", "throughput" => "Aiur Prove Throughput"
| "aiur-check-prove", "peak-rss" => "Aiur Prove Peak RAM Usage"
Expand All@@ -78,10 +81,14 @@ def plotTitle (workload measure : String) : String :=
"Aiur FFT Cost" from the prove cell). Zisk `shards` is a PR-comment
column only ("Zisk Cycles" / max-shard-cycles carry the sharding
trend), and zisk `constants` charts on the cross-kernel overlay below
instead of alone. -/
instead of alone. `ix-decompile` reuses the compile cell's `.ixe`, so
its `file-size` / `constants` duplicate "Ix Environment Size" / "Ix
Input Constants" exactly — the decompile cell tracks only its own
decompile-time / throughput / peak-rss trends. -/
def plotSkips : List (String × String) :=
[("aiur-check-prove", "execute-time"), ("aiur-check-execute", "fft-cost"),
("zisk-check-execute", "shards"), ("zisk-check-execute", "constants")]
("zisk-check-execute", "shards"), ("zisk-check-execute", "constants"),
("ix-decompile", "file-size"), ("ix-decompile", "constants")]

/-- Canonical units per measure slug, asserted on every sync: bencher
auto-creates a measure with placeholder units ("Measure (units)") on
Expand All@@ -92,6 +99,7 @@ def unitsFor (slug : String) : Option String :=
if slug.startsWith "phase-" then some "seconds (s)" else
[("execute-peak-rss", "bytes (B)"),
("compile-time", "seconds (s)"),
("decompile-time", "seconds (s)"),
("execute-time", "seconds (s)"),
("prove-time", "seconds (s)"),
("verify-time", "seconds (s)"),
Expand All@@ -115,7 +123,7 @@ def unitsFor (slug : String) : Option String :=
/-- Dashboard group order (compile first, then aiur prove/execute, zisk,
ooc); unranked workloads (a future backend) sort last. -/
def workloadOrder : List String :=
["ix-compile", "aiur-check-prove", "aiur-check-execute",
["ix-compile", "ix-decompile", "aiur-check-prove", "aiur-check-execute",
"aiur-check-recursive", "aiur-recursive", "zisk-check-execute",
"ooc-check"]

Expand All@@ -127,7 +135,8 @@ structure PlotSpec where
/-- One spec per bench-main testbed: its measure slugs and the benchmark
row names uploaded there, mirroring the row emitters — compile keys
one row per env (benched or not: the compile matrix is deliberately
wider), ooc one whole-env row plus one full-closure row per primary,
wider), decompile one row per benched env (a `.ixe` consumer), ooc one
whole-env row plus one full-closure row per primary,
the per-constant backends one row per primary. Dynamic sub-rows
(`<name>/shard-N`) are left out: their multiplicity shifts with the
shard manifest, and the parent row carries the headline trend. -/
Expand All@@ -142,6 +151,10 @@ def plotSpecs (rows : Array BenchCmd.VectorRow) : Array PlotSpec := Id.run do
return (BenchCmd.envSpecs.map (·.name)).toArray
if b.name == "aiur-recursive" then
return (BenchCmd.recursiveConfigs.map (·.1)).toArray
-- decompile is env-keyed like compile but a `.ixe` consumer: one row
-- per benched env (it runs only where a benched `.ixe` exists).
if b.name == "decompile" then
return benched.toArray
let mut ns : Array String := #[]
for env in benched do
if b.name == "ooc" then ns := ns.push env
Expand Down
2 changes: 1 addition & 1 deletion Ix/Cli/BenchReport.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -43,7 +43,7 @@ def metricKind (metric : String) : String :=
then "bytes"
else if metric.startsWith "phase-" then "seconds"
else if ["execute-time", "prove-time", "verify-time", "check-time",
"compile-time"].contains metric then "seconds"
"compile-time", "decompile-time"].contains metric then "seconds"
else if ["fft-cost", "cycles", "steps", "max-shard-cycles",
"throughput"].contains metric then "count"
else if ["constants", "shards"].contains metric then "int"
Expand Down
83 changes: 83 additions & 0 deletions Ix/Cli/DecompileCmd.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
/-
`ix decompile <path.ixe>`: decompile a serialized `.ixe` environment back to
Lean constants — the inverse of `ix compile`. This is the decompile
benchmark's measured tool (env-keyed row, mirroring `ix compile --json`).

With `--json` the run records one env-keyed results row (decompile-time,
file-size, constants, throughput, peak-rss). A malformed decompile is a hard
error (nonzero exit → red cell). Deeper compile→decompile roundtrip fidelity
is gated by the canonical roundtrip checks (`ix validate` / the roundtrip
tests), which need the original Lean env a `.ixe` can't supply — so this
performance tool does not reproduce them.
-/
module
public import Cli
public import Ix.Common
public import Ix.TracingTexray
public import Ix.Benchmark.Results

public section

open System (FilePath)

namespace Ix.Cli.DecompileCmd

/-- Decompile a `.ixe` from disk, returning the decompiled constant
count. A malformed decompile throws (hard error). Implemented in
`crates/ffi/src/compile.rs::rs_decompile_env`. -/
@[extern "rs_decompile_env"]
opaque rsDecompileEnvFFI : @& String → IO Nat

def runDecompileCmd (p : Cli.Parsed) : IO UInt32 := do
let some pathArg := p.positionalArg? "path"
| p.printError "error: must specify <path> to a .ixe file"
return Ix.Benchmark.Results.exitUsage
let envPath := pathArg.as! String

-- Window the tree-RSS sampler around the decompile, mirroring
-- `ix compile --json` so the two rows share measurement
-- infrastructure and peak-rss semantics.
let benched := (p.flag? "json").isSome
if benched then
TracingTexray.startSampler
TracingTexray.resetPeakTreeRss

IO.println s!"Decompiling {envPath}"
let start ← IO.monoMsNow
let constants ← rsDecompileEnvFFI envPath
let elapsed := (← IO.monoMsNow) - start
IO.println s!"[decompile] {constants} constants in {elapsed.formatMs}"

if let some flag := p.flag? "json" then
let key := (p.flag? "json-name").map (·.as! String)
|>.getD ((FilePath.mk envPath).fileStem.getD "env")
let secs := elapsed.toFloat / 1000.0
let tput := if elapsed > 0
then constants.toFloat * 1000.0 / elapsed.toFloat else 0.0
let peakRss ← TracingTexray.peakTreeRssBytes
-- `file-size` is the INPUT `.ixe` the decompile consumed (the byte
-- counterpart to compile's output `.ixe`).
let size := (← (FilePath.mk envPath).metadata).byteSize.toNat
Ix.Benchmark.Results.writeRow (flag.as! String) key "ok"
[ ("decompile-time", Ix.Benchmark.Results.jsonRound 3 secs)
, ("file-size", Lean.toJson size)
, ("constants", Lean.toJson constants)
, ("throughput", Ix.Benchmark.Results.jsonRound 2 tput)
, ("peak-rss", Lean.toJson peakRss) ]

return 0

end Ix.Cli.DecompileCmd

open Ix.Cli.DecompileCmd in
def decompileCmd : Cli.Cmd := `[Cli|
decompile VIA runDecompileCmd;
"Decompile a serialized `.ixe` env back to Lean constants (inverse of `ix compile`). Measures the decompile pass; a malformed decompile exits nonzero. Deep roundtrip fidelity is gated by `ix validate` / the roundtrip tests."

FLAGS:
json : String; "Write the decompile's benchmark results row (decompile-time, file-size, constants, throughput, peak-rss) to this path, merging into any existing rows object."
"json-name" : String; "Row key for the --json row (default: the input `.ixe` file's stem)."

ARGS:
path : String; "Path to the serialized `.ixe` environment to decompile."
]
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 ix decompile CLI, fix Rust decompile perf and tests#490

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

 Merged

samuelburnham
merged 3 commits into

from

Jul 14, 2026
 Merged


feat: Add ix decompile CLI, fix Rust decompile perf and tests
#490
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


3 commits


Select commit
Hold shift + click to select a range
1064f84

perf: Fix ignored-test fallout from #484 and bound decompile/validate…


samuelburnham Jul 13, 2026
41a1876

feat: Add `ix decompile` and its benchmark backend


samuelburnham Jul 13, 2026
ba9a104

test: Cover Rust decompile over the serialized roundtrip


samuelburnham Jul 13, 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


82 changes: 81 additions & 1 deletion
.github/workflows/bench-main.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,7 +16,10 @@ name: Benchmark main
# 4. ooc-check — restore that `.ixe` and run the out-of-circuit Rust kernel
# (the same kernel, out-of-circuit and parallel — far faster)
# over the whole env, tracking throughput.
# 5. aiur-recursive — the aiur-recursive toy
# 5. decompile — restore that `.ixe` and decompile it back to Lean constants
# (the inverse of step 1); tracks decompile-time /
# throughput / peak-rss.
# 6. aiur-recursive — the aiur-recursive toy
# (bench-recursive-verifier):
# prove fixed tiny statements, run the in-circuit
# multi-stark verifier over each proof, then prove THAT
Expand DownExpand Up@@ -617,3 +620,80 @@ jobs:
 --threshold-measure peak-rss --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
 --threshold-lower-boundary _

 # Decompile — the inverse of compile. Restore the compile job's cached
 # `.ixe` and decompile it back to Lean constants. One env-keyed row per
 # benched env, mirroring the `compile` cell. A malformed decompile exits
 # nonzero and reddens this step; deep roundtrip fidelity is gated by the
 # canonical checks (`ix validate` / roundtrip tests), not measured here. No
 # compiler or Lean toolchain build — `ix decompile` is a Rust FFI pass over
 # the cached `.ixe`, so this reuses the staged `ix` binary like ooc-check.
 decompile:
 name: decompile-${{ matrix.bench }}
 needs: [compile, plan]
 runs-on: warp-ubuntu-latest-x64-32x
 timeout-minutes: 60
 strategy:
 fail-fast: false
 matrix:
 bench: ${{ fromJson(needs.plan.outputs.bench-envs) }}
 steps:
 - uses: actions/checkout@v6
 - uses: actions/cache/restore@v5
 with:
 path: ~/.local/bin
 key: bench-bins-${{ github.sha }}
 - run: echo "$HOME/.local/bin" >> $GITHUB_PATH
 # Provision the toolchain so `ix` finds libleanshared (no package build).
 - uses: leanprover/lean-action@v1
 with:
 auto-config: false
 build: false
 use-github-cache: false
 # (The path list must match the compile job's save exactly.)
 - uses: actions/cache/restore@v5
 with:
 path: |
 ${{ matrix.bench }}.ixe
 zkshards-${{ matrix.bench }}
 key: bench-ixe-${{ github.sha }}-${{ matrix.bench }}
 fail-on-cache-miss: true
 # A malformed decompile exits nonzero → red X here; a clean run's row
 # uploads below.
 - name: Run decompile benchmark
 run: |
 ix bench run --backend decompile --env ${{ matrix.bench }} --mode execute \
 --ixe ${{ matrix.bench }}.ixe --out bench.json
 # Upload whatever clean rows exist even when the run step reddened the
 # job — bmf drops every non-ok (rejected/oom) row.
 - name: Convert to Bencher Metric Format
 id: bmf
 if: ${{ !cancelled() }}
 run: |
 ix bench bmf --in bench.json --out bench-bmf.json
 cat bench-bmf.json
 # constants is deterministic → pinned (0/0); decompile-time / throughput
 # / peak-rss are noisy wall-clock → percentage bounds. file-size (the
 # input `.ixe`) duplicates the compile cell's, so it uploads for the
 # row's completeness but rides no threshold here.
 - uses: ./.github/actions/bencher-track
 if: ${{ !cancelled() && steps.bmf.outcome == 'success' }}
 with:
 testbed: ix-decompile-x64-32x
 workload: ix-decompile
 file: bench-bmf.json
 key: ${{ secrets.BENCHER_API_KEY }}
 github-token: ${{ secrets.GITHUB_TOKEN }}
 thresholds: |
 --threshold-measure constants --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0
 --threshold-lower-boundary 0
 --threshold-measure decompile-time --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
 --threshold-lower-boundary _
 --threshold-measure throughput --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary _
 --threshold-lower-boundary 0.10
 --threshold-measure peak-rss --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
 --threshold-lower-boundary _

12 changes: 7 additions & 5 deletions
.github/workflows/bench-pr.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
# `!benchmark` PR command: run the curated constant set (Benchmarks/Vectors.csv)
# through chosen prover backend(s) and post a main-vs-PR comparison table.
#
# !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [aiur-recursive] | all) [execute]
# !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [decompile] [aiur-recursive] | all) [execute]
# (sp1 is disabled in the registry (Ix/Cli/BenchCmd.lean) — the parser skips it
# with a note in the config summary)
# BENCH_ENVS=InitStd,Mathlib # which compiled envs (default InitStd; case-insensitive;
Expand All@@ -20,10 +20,12 @@
# Phase-1 columns `fft-cost` / `execute-time` measured en route; `zisk` /
# `sp1` / `ooc` run `execute`; `compile` runs `ix compile <env>.lean →
# <env>.ixe` (the same cell bench-main.yml uploads under testbed
# `ix-compile-*`); `aiur-recursive` runs the aiur-recursive toy
# (bench-recursive-verifier's fixed configs — env-independent, so it
# always schedules exactly one cell no matter what BENCH_ENVS says).
# The optional bare `execute` token flips `aiur` to
# `ix-compile-*`); `decompile` runs `ix decompile <env>.ixe` over the
# compile cell's fresh PR `.ixe` (testbed `ix-decompile-*`);
# `aiur-recursive` runs the aiur-recursive toy (bench-recursive-verifier's
# fixed configs — env-independent, so it always schedules exactly one cell
# no matter what BENCH_ENVS says). The optional bare `execute` token flips
# `aiur` to
# execute-only (Phase 1, skipping the prove); bench-main runs both aiur
# modes as separate cells on separate testbeds, so either kind of cell
# fetches a cached main-side baseline from bencher. (aiur's third mode,
Expand Down

8 changes: 4 additions & 4 deletions
.github/workflows/bencher-thresholds-reset.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -22,7 +22,7 @@ name: Bencher thresholds reset
# cancel by removing it before merge. Naming convention: one label per token,
# `bencher-thresholds-reset:<token>` where <token> is a workload (a backend
# testbed in Ix/Cli/BenchCmd.lean (backendSpecs) minus its runner-arch suffix:
# `ix-compile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `all` (the merge step expands an `all` label into every workload). Labeling
# requires Triage+, so PR authors from forks cannot self-queue a reset. The
# label shares the command/workflow name; the ref it moves is
Expand All@@ -44,7 +44,7 @@ on:
 # GitHub requires literal choice options, so this list stays static:
 # keep it (and the jobs' valid= lists below) in sync with the
 # backend testbeds in Ix/Cli/BenchCmd.lean (backendSpecs).
 options: [ix-compile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
 options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
 sha:
 description: "Commit to anchor to (default: HEAD)"
 required: false
Expand DownExpand Up@@ -77,7 +77,7 @@ jobs:
 # (backendSpecs) minus the runner-arch suffix. Static because this
 # job runs on a cheap runner with no built `ix`; keep in sync when
 # adding a backend.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 if [ "$EVENT" = workflow_dispatch ]; then
 # Reset the chosen workload(s) at the given commit; no PR scan.
 sha="${INPUT_SHA:-$HEAD_SHA}"
Expand DownExpand Up@@ -133,7 +133,7 @@ jobs:
 # which the merge job expands into every workload). Same static
 # list as the reset job; keep both in sync with backendSpecs in
 # Ix/Cli/BenchCmd.lean.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 accepted="$valid all"
 # Parse the workload token(s) after the command, lowercased.
 workloads=$(printf '%s' "$BODY" \
Expand Down

23 changes: 22 additions & 1 deletion
Ix/Cli/BenchCmd.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -185,6 +185,14 @@ def backendSpecs : List BackendSpec := [
 { name := "compile", defaultMode := "execute",
 testbeds := [("execute", "ix-compile-x64-32x")],
 metrics := [("execute", ["compile-time", "throughput", "peak-rss",
 "file-size", "constants"])] },
 -- The inverse of compile: decompiles the env's `.ixe` back to Lean
 -- constants (roundtrip-verified). Env-keyed like compile, but a `.ixe`
 -- CONSUMER — it reuses the compile cell's fresh `.ixe` rather than
 -- producing one.
 { name := "decompile", defaultMode := "execute",
 testbeds := [("execute", "ix-decompile-x64-32x")],
 metrics := [("execute", ["decompile-time", "throughput", "peak-rss",
 "file-size", "constants"])] }
]

Expand DownExpand Up@@ -492,6 +500,18 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do
 if exit != 0 then
 IO.eprintln s!"[bench] ix compile failed (exit {exit})"
 return 1
 | "decompile" =>
 -- The inverse of compile: consume the env's `.ixe` (the compile cell's
 -- fresh artifact) and decompile it back to Lean constants. Env-keyed row,
 -- like compile. A malformed decompile exits nonzero and reddens the cell;
 -- deep roundtrip fidelity is gated by the canonical roundtrip checks
 -- (`ix validate` / the roundtrip tests), not measured here.
 let ixe ← ensureIxe repo info ((p.flag? "ixe").map (·.as! String))
 let ix ← resolveBin repo "ix"
 let exit ← runGuarded watchdog ceilingGb ix
 #["decompile", ixe, "--json", out, "--json-name", info.name]
 if exit != 0 then
 IO.eprintln s!"[bench] ix decompile failed (exit {exit})"
 | "ooc" =>
 let ixe ← ensureIxe repo info ((p.flag? "ixe").map (·.as! String))
 let ix ← resolveBin repo "ix"
Expand DownExpand Up@@ -586,6 +606,7 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do
 -- row too.
 let expected := match backend with
 | "compile" => #[info.name]
 | "decompile" => #[info.name]
 | "ooc" => #[info.name] ++ names
 | "aiur-recursive" => (recursiveConfigs.map (·.1)).toArray
 | _ => names
Expand DownExpand Up@@ -630,7 +651,7 @@ def benchRunCmd : Cli.Cmd := `[Cli|
 "Run one benchmark cell (backend × env × mode), writing benchmark results JSON. Exits 0 on success (rows saved as the local baseline), 3 when the kernel rejected any constant, 1 when no rows were produced."

 FLAGS:
 backend : String; "aiur | zisk | sp1 | ooc | compile | aiur-recursive"
 backend : String; "aiur | zisk | sp1 | ooc | compile | decompile | aiur-recursive"
 env : String; "Benchmark env from the registry (default: InitStd)"
 mode : String; "prove | execute | recursive (default: the backend's defaultMode)"
 out : String; "Benchmark results JSON output path (default: bench.json)"
Expand Down

21 changes: 17 additions & 4 deletions
Ix/Cli/BenchPlots.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -54,6 +54,9 @@ def plotTitle (workload measure : String) : String :=
 | "ix-compile", "peak-rss" => "Ix Compile Peak RAM Usage"
 | "ix-compile", "file-size" => "Ix Environment Size"
 | "ix-compile", "constants" => "Ix Input Constants"
 | "ix-decompile", "decompile-time" => "Ix Decompile Time"
 | "ix-decompile", "throughput" => "Ix Decompile Throughput"
 | "ix-decompile", "peak-rss" => "Ix Decompile Peak RAM Usage"
 | "aiur-check-prove", "prove-time" => "Aiur Prove Time"
 | "aiur-check-prove", "throughput" => "Aiur Prove Throughput"
 | "aiur-check-prove", "peak-rss" => "Aiur Prove Peak RAM Usage"
Expand All@@ -78,10 +81,14 @@ def plotTitle (workload measure : String) : String :=
 "Aiur FFT Cost" from the prove cell). Zisk `shards` is a PR-comment
 column only ("Zisk Cycles" / max-shard-cycles carry the sharding
 trend), and zisk `constants` charts on the cross-kernel overlay below
 instead of alone. -/
 instead of alone. `ix-decompile` reuses the compile cell's `.ixe`, so
 its `file-size` / `constants` duplicate "Ix Environment Size" / "Ix
 Input Constants" exactly — the decompile cell tracks only its own
 decompile-time / throughput / peak-rss trends. -/
def plotSkips : List (String × String) :=
 [("aiur-check-prove", "execute-time"), ("aiur-check-execute", "fft-cost"),
 ("zisk-check-execute", "shards"), ("zisk-check-execute", "constants")]
 ("zisk-check-execute", "shards"), ("zisk-check-execute", "constants"),
 ("ix-decompile", "file-size"), ("ix-decompile", "constants")]

/-- Canonical units per measure slug, asserted on every sync: bencher
 auto-creates a measure with placeholder units ("Measure (units)") on
Expand All@@ -92,6 +99,7 @@ def unitsFor (slug : String) : Option String :=
 if slug.startsWith "phase-" then some "seconds (s)" else
 [("execute-peak-rss", "bytes (B)"),
 ("compile-time", "seconds (s)"),
 ("decompile-time", "seconds (s)"),
 ("execute-time", "seconds (s)"),
 ("prove-time", "seconds (s)"),
 ("verify-time", "seconds (s)"),
Expand All@@ -115,7 +123,7 @@ def unitsFor (slug : String) : Option String :=
/-- Dashboard group order (compile first, then aiur prove/execute, zisk,
 ooc); unranked workloads (a future backend) sort last. -/
def workloadOrder : List String :=
 ["ix-compile", "aiur-check-prove", "aiur-check-execute",
 ["ix-compile", "ix-decompile", "aiur-check-prove", "aiur-check-execute",
 "aiur-check-recursive", "aiur-recursive", "zisk-check-execute",
 "ooc-check"]

Expand All@@ -127,7 +135,8 @@ structure PlotSpec where
/-- One spec per bench-main testbed: its measure slugs and the benchmark
 row names uploaded there, mirroring the row emitters — compile keys
 one row per env (benched or not: the compile matrix is deliberately
 wider), ooc one whole-env row plus one full-closure row per primary,
 wider), decompile one row per benched env (a `.ixe` consumer), ooc one
 whole-env row plus one full-closure row per primary,
 the per-constant backends one row per primary. Dynamic sub-rows
 (`<name>/shard-N`) are left out: their multiplicity shifts with the
 shard manifest, and the parent row carries the headline trend. -/
Expand All@@ -142,6 +151,10 @@ def plotSpecs (rows : Array BenchCmd.VectorRow) : Array PlotSpec := Id.run do
 return (BenchCmd.envSpecs.map (·.name)).toArray
 if b.name == "aiur-recursive" then
 return (BenchCmd.recursiveConfigs.map (·.1)).toArray
 -- decompile is env-keyed like compile but a `.ixe` consumer: one row
 -- per benched env (it runs only where a benched `.ixe` exists).
 if b.name == "decompile" then
 return benched.toArray
 let mut ns : Array String := #[]
 for env in benched do
 if b.name == "ooc" then ns := ns.push env
Expand Down

2 changes: 1 addition & 1 deletion
Ix/Cli/BenchReport.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -43,7 +43,7 @@ def metricKind (metric : String) : String :=
 then "bytes"
 else if metric.startsWith "phase-" then "seconds"
 else if ["execute-time", "prove-time", "verify-time", "check-time",
 "compile-time"].contains metric then "seconds"
 "compile-time", "decompile-time"].contains metric then "seconds"
 else if ["fft-cost", "cycles", "steps", "max-shard-cycles",
 "throughput"].contains metric then "count"
 else if ["constants", "shards"].contains metric then "int"
Expand Down

83 changes: 83 additions & 0 deletions
Ix/Cli/DecompileCmd.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
/-
 `ix decompile <path.ixe>`: decompile a serialized `.ixe` environment back to
 Lean constants — the inverse of `ix compile`. This is the decompile
 benchmark's measured tool (env-keyed row, mirroring `ix compile --json`).

 With `--json` the run records one env-keyed results row (decompile-time,
 file-size, constants, throughput, peak-rss). A malformed decompile is a hard
 error (nonzero exit → red cell). Deeper compile→decompile roundtrip fidelity
 is gated by the canonical roundtrip checks (`ix validate` / the roundtrip
 tests), which need the original Lean env a `.ixe` can't supply — so this
 performance tool does not reproduce them.
-/
module
public import Cli
public import Ix.Common
public import Ix.TracingTexray
public import Ix.Benchmark.Results

public section

open System (FilePath)

namespace Ix.Cli.DecompileCmd

/-- Decompile a `.ixe` from disk, returning the decompiled constant
 count. A malformed decompile throws (hard error). Implemented in
 `crates/ffi/src/compile.rs::rs_decompile_env`. -/
@[extern "rs_decompile_env"]
opaque rsDecompileEnvFFI : @& String → IO Nat

def runDecompileCmd (p : Cli.Parsed) : IO UInt32 := do
 let some pathArg := p.positionalArg? "path"
 | p.printError "error: must specify <path> to a .ixe file"
 return Ix.Benchmark.Results.exitUsage
 let envPath := pathArg.as! String

 -- Window the tree-RSS sampler around the decompile, mirroring
 -- `ix compile --json` so the two rows share measurement
 -- infrastructure and peak-rss semantics.
 let benched := (p.flag? "json").isSome
 if benched then
 TracingTexray.startSampler
 TracingTexray.resetPeakTreeRss

 IO.println s!"Decompiling {envPath}"
 let start ← IO.monoMsNow
 let constants ← rsDecompileEnvFFI envPath
 let elapsed := (← IO.monoMsNow) - start
 IO.println s!"[decompile] {constants} constants in {elapsed.formatMs}"

 if let some flag := p.flag? "json" then
 let key := (p.flag? "json-name").map (·.as! String)
 |>.getD ((FilePath.mk envPath).fileStem.getD "env")
 let secs := elapsed.toFloat / 1000.0
 let tput := if elapsed > 0
 then constants.toFloat * 1000.0 / elapsed.toFloat else 0.0
 let peakRss ← TracingTexray.peakTreeRssBytes
 -- `file-size` is the INPUT `.ixe` the decompile consumed (the byte
 -- counterpart to compile's output `.ixe`).
 let size := (← (FilePath.mk envPath).metadata).byteSize.toNat
 Ix.Benchmark.Results.writeRow (flag.as! String) key "ok"
 [ ("decompile-time", Ix.Benchmark.Results.jsonRound 3 secs)
 , ("file-size", Lean.toJson size)
 , ("constants", Lean.toJson constants)
 , ("throughput", Ix.Benchmark.Results.jsonRound 2 tput)
 , ("peak-rss", Lean.toJson peakRss) ]

 return 0

end Ix.Cli.DecompileCmd

open Ix.Cli.DecompileCmd in
def decompileCmd : Cli.Cmd := `[Cli|
 decompile VIA runDecompileCmd;
 "Decompile a serialized `.ixe` env back to Lean constants (inverse of `ix compile`). Measures the decompile pass; a malformed decompile exits nonzero. Deep roundtrip fidelity is gated by `ix validate` / the roundtrip tests."

 FLAGS:
 json : String; "Write the decompile's benchmark results row (decompile-time, file-size, constants, throughput, peak-rss) to this path, merging into any existing rows object."
 "json-name" : String; "Row key for the --json row (default: the input `.ixe` file's stem)."

 ARGS:
 path : String; "Path to the serialized `.ixe` environment to decompile."
]
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 ix decompile CLI, fix Rust decompile perf and tests#490

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

 Merged

samuelburnham
merged 3 commits into

from

Jul 14, 2026
 Merged


feat: Add ix decompile CLI, fix Rust decompile perf and tests
#490
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


3 commits


Select commit
Hold shift + click to select a range
1064f84

perf: Fix ignored-test fallout from #484 and bound decompile/validate…


samuelburnham Jul 13, 2026
41a1876

feat: Add `ix decompile` and its benchmark backend


samuelburnham Jul 13, 2026
ba9a104

test: Cover Rust decompile over the serialized roundtrip


samuelburnham Jul 13, 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


82 changes: 81 additions & 1 deletion
.github/workflows/bench-main.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,7 +16,10 @@ name: Benchmark main
# 4. ooc-check — restore that `.ixe` and run the out-of-circuit Rust kernel
# (the same kernel, out-of-circuit and parallel — far faster)
# over the whole env, tracking throughput.
# 5. aiur-recursive — the aiur-recursive toy
# 5. decompile — restore that `.ixe` and decompile it back to Lean constants
# (the inverse of step 1); tracks decompile-time /
# throughput / peak-rss.
# 6. aiur-recursive — the aiur-recursive toy
# (bench-recursive-verifier):
# prove fixed tiny statements, run the in-circuit
# multi-stark verifier over each proof, then prove THAT
Expand DownExpand Up@@ -617,3 +620,80 @@ jobs:
 --threshold-measure peak-rss --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
 --threshold-lower-boundary _

 # Decompile — the inverse of compile. Restore the compile job's cached
 # `.ixe` and decompile it back to Lean constants. One env-keyed row per
 # benched env, mirroring the `compile` cell. A malformed decompile exits
 # nonzero and reddens this step; deep roundtrip fidelity is gated by the
 # canonical checks (`ix validate` / roundtrip tests), not measured here. No
 # compiler or Lean toolchain build — `ix decompile` is a Rust FFI pass over
 # the cached `.ixe`, so this reuses the staged `ix` binary like ooc-check.
 decompile:
 name: decompile-${{ matrix.bench }}
 needs: [compile, plan]
 runs-on: warp-ubuntu-latest-x64-32x
 timeout-minutes: 60
 strategy:
 fail-fast: false
 matrix:
 bench: ${{ fromJson(needs.plan.outputs.bench-envs) }}
 steps:
 - uses: actions/checkout@v6
 - uses: actions/cache/restore@v5
 with:
 path: ~/.local/bin
 key: bench-bins-${{ github.sha }}
 - run: echo "$HOME/.local/bin" >> $GITHUB_PATH
 # Provision the toolchain so `ix` finds libleanshared (no package build).
 - uses: leanprover/lean-action@v1
 with:
 auto-config: false
 build: false
 use-github-cache: false
 # (The path list must match the compile job's save exactly.)
 - uses: actions/cache/restore@v5
 with:
 path: |
 ${{ matrix.bench }}.ixe
 zkshards-${{ matrix.bench }}
 key: bench-ixe-${{ github.sha }}-${{ matrix.bench }}
 fail-on-cache-miss: true
 # A malformed decompile exits nonzero → red X here; a clean run's row
 # uploads below.
 - name: Run decompile benchmark
 run: |
 ix bench run --backend decompile --env ${{ matrix.bench }} --mode execute \
 --ixe ${{ matrix.bench }}.ixe --out bench.json
 # Upload whatever clean rows exist even when the run step reddened the
 # job — bmf drops every non-ok (rejected/oom) row.
 - name: Convert to Bencher Metric Format
 id: bmf
 if: ${{ !cancelled() }}
 run: |
 ix bench bmf --in bench.json --out bench-bmf.json
 cat bench-bmf.json
 # constants is deterministic → pinned (0/0); decompile-time / throughput
 # / peak-rss are noisy wall-clock → percentage bounds. file-size (the
 # input `.ixe`) duplicates the compile cell's, so it uploads for the
 # row's completeness but rides no threshold here.
 - uses: ./.github/actions/bencher-track
 if: ${{ !cancelled() && steps.bmf.outcome == 'success' }}
 with:
 testbed: ix-decompile-x64-32x
 workload: ix-decompile
 file: bench-bmf.json
 key: ${{ secrets.BENCHER_API_KEY }}
 github-token: ${{ secrets.GITHUB_TOKEN }}
 thresholds: |
 --threshold-measure constants --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0
 --threshold-lower-boundary 0
 --threshold-measure decompile-time --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
 --threshold-lower-boundary _
 --threshold-measure throughput --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary _
 --threshold-lower-boundary 0.10
 --threshold-measure peak-rss --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
 --threshold-lower-boundary _

12 changes: 7 additions & 5 deletions
.github/workflows/bench-pr.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
# `!benchmark` PR command: run the curated constant set (Benchmarks/Vectors.csv)
# through chosen prover backend(s) and post a main-vs-PR comparison table.
#
# !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [aiur-recursive] | all) [execute]
# !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [decompile] [aiur-recursive] | all) [execute]
# (sp1 is disabled in the registry (Ix/Cli/BenchCmd.lean) — the parser skips it
# with a note in the config summary)
# BENCH_ENVS=InitStd,Mathlib # which compiled envs (default InitStd; case-insensitive;
Expand All@@ -20,10 +20,12 @@
# Phase-1 columns `fft-cost` / `execute-time` measured en route; `zisk` /
# `sp1` / `ooc` run `execute`; `compile` runs `ix compile <env>.lean →
# <env>.ixe` (the same cell bench-main.yml uploads under testbed
# `ix-compile-*`); `aiur-recursive` runs the aiur-recursive toy
# (bench-recursive-verifier's fixed configs — env-independent, so it
# always schedules exactly one cell no matter what BENCH_ENVS says).
# The optional bare `execute` token flips `aiur` to
# `ix-compile-*`); `decompile` runs `ix decompile <env>.ixe` over the
# compile cell's fresh PR `.ixe` (testbed `ix-decompile-*`);
# `aiur-recursive` runs the aiur-recursive toy (bench-recursive-verifier's
# fixed configs — env-independent, so it always schedules exactly one cell
# no matter what BENCH_ENVS says). The optional bare `execute` token flips
# `aiur` to
# execute-only (Phase 1, skipping the prove); bench-main runs both aiur
# modes as separate cells on separate testbeds, so either kind of cell
# fetches a cached main-side baseline from bencher. (aiur's third mode,
Expand Down

8 changes: 4 additions & 4 deletions
.github/workflows/bencher-thresholds-reset.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -22,7 +22,7 @@ name: Bencher thresholds reset
# cancel by removing it before merge. Naming convention: one label per token,
# `bencher-thresholds-reset:<token>` where <token> is a workload (a backend
# testbed in Ix/Cli/BenchCmd.lean (backendSpecs) minus its runner-arch suffix:
# `ix-compile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `all` (the merge step expands an `all` label into every workload). Labeling
# requires Triage+, so PR authors from forks cannot self-queue a reset. The
# label shares the command/workflow name; the ref it moves is
Expand All@@ -44,7 +44,7 @@ on:
 # GitHub requires literal choice options, so this list stays static:
 # keep it (and the jobs' valid= lists below) in sync with the
 # backend testbeds in Ix/Cli/BenchCmd.lean (backendSpecs).
 options: [ix-compile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
 options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
 sha:
 description: "Commit to anchor to (default: HEAD)"
 required: false
Expand DownExpand Up@@ -77,7 +77,7 @@ jobs:
 # (backendSpecs) minus the runner-arch suffix. Static because this
 # job runs on a cheap runner with no built `ix`; keep in sync when
 # adding a backend.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 if [ "$EVENT" = workflow_dispatch ]; then
 # Reset the chosen workload(s) at the given commit; no PR scan.
 sha="${INPUT_SHA:-$HEAD_SHA}"
Expand DownExpand Up@@ -133,7 +133,7 @@ jobs:
 # which the merge job expands into every workload). Same static
 # list as the reset job; keep both in sync with backendSpecs in
 # Ix/Cli/BenchCmd.lean.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 accepted="$valid all"
 # Parse the workload token(s) after the command, lowercased.
 workloads=$(printf '%s' "$BODY" \
Expand Down

23 changes: 22 additions & 1 deletion
Ix/Cli/BenchCmd.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -185,6 +185,14 @@ def backendSpecs : List BackendSpec := [
 { name := "compile", defaultMode := "execute",
 testbeds := [("execute", "ix-compile-x64-32x")],
 metrics := [("execute", ["compile-time", "throughput", "peak-rss",
 "file-size", "constants"])] },
 -- The inverse of compile: decompiles the env's `.ixe` back to Lean
 -- constants (roundtrip-verified). Env-keyed like compile, but a `.ixe`
 -- CONSUMER — it reuses the compile cell's fresh `.ixe` rather than
 -- producing one.
 { name := "decompile", defaultMode := "execute",
 testbeds := [("execute", "ix-decompile-x64-32x")],
 metrics := [("execute", ["decompile-time", "throughput", "peak-rss",
 "file-size", "constants"])] }
]

Expand DownExpand Up@@ -492,6 +500,18 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do
 if exit != 0 then
 IO.eprintln s!"[bench] ix compile failed (exit {exit})"
 return 1
 | "decompile" =>
 -- The inverse of compile: consume the env's `.ixe` (the compile cell's
 -- fresh artifact) and decompile it back to Lean constants. Env-keyed row,
 -- like compile. A malformed decompile exits nonzero and reddens the cell;
 -- deep roundtrip fidelity is gated by the canonical roundtrip checks
 -- (`ix validate` / the roundtrip tests), not measured here.
 let ixe ← ensureIxe repo info ((p.flag? "ixe").map (·.as! String))
 let ix ← resolveBin repo "ix"
 let exit ← runGuarded watchdog ceilingGb ix
 #["decompile", ixe, "--json", out, "--json-name", info.name]
 if exit != 0 then
 IO.eprintln s!"[bench] ix decompile failed (exit {exit})"
 | "ooc" =>
 let ixe ← ensureIxe repo info ((p.flag? "ixe").map (·.as! String))
 let ix ← resolveBin repo "ix"
Expand DownExpand Up@@ -586,6 +606,7 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do
 -- row too.
 let expected := match backend with
 | "compile" => #[info.name]
 | "decompile" => #[info.name]
 | "ooc" => #[info.name] ++ names
 | "aiur-recursive" => (recursiveConfigs.map (·.1)).toArray
 | _ => names
Expand DownExpand Up@@ -630,7 +651,7 @@ def benchRunCmd : Cli.Cmd := `[Cli|
 "Run one benchmark cell (backend × env × mode), writing benchmark results JSON. Exits 0 on success (rows saved as the local baseline), 3 when the kernel rejected any constant, 1 when no rows were produced."

 FLAGS:
 backend : String; "aiur | zisk | sp1 | ooc | compile | aiur-recursive"
 backend : String; "aiur | zisk | sp1 | ooc | compile | decompile | aiur-recursive"
 env : String; "Benchmark env from the registry (default: InitStd)"
 mode : String; "prove | execute | recursive (default: the backend's defaultMode)"
 out : String; "Benchmark results JSON output path (default: bench.json)"
Expand Down

21 changes: 17 additions & 4 deletions
Ix/Cli/BenchPlots.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -54,6 +54,9 @@ def plotTitle (workload measure : String) : String :=
 | "ix-compile", "peak-rss" => "Ix Compile Peak RAM Usage"
 | "ix-compile", "file-size" => "Ix Environment Size"
 | "ix-compile", "constants" => "Ix Input Constants"
 | "ix-decompile", "decompile-time" => "Ix Decompile Time"
 | "ix-decompile", "throughput" => "Ix Decompile Throughput"
 | "ix-decompile", "peak-rss" => "Ix Decompile Peak RAM Usage"
 | "aiur-check-prove", "prove-time" => "Aiur Prove Time"
 | "aiur-check-prove", "throughput" => "Aiur Prove Throughput"
 | "aiur-check-prove", "peak-rss" => "Aiur Prove Peak RAM Usage"
Expand All@@ -78,10 +81,14 @@ def plotTitle (workload measure : String) : String :=
 "Aiur FFT Cost" from the prove cell). Zisk `shards` is a PR-comment
 column only ("Zisk Cycles" / max-shard-cycles carry the sharding
 trend), and zisk `constants` charts on the cross-kernel overlay below
 instead of alone. -/
 instead of alone. `ix-decompile` reuses the compile cell's `.ixe`, so
 its `file-size` / `constants` duplicate "Ix Environment Size" / "Ix
 Input Constants" exactly — the decompile cell tracks only its own
 decompile-time / throughput / peak-rss trends. -/
def plotSkips : List (String × String) :=
 [("aiur-check-prove", "execute-time"), ("aiur-check-execute", "fft-cost"),
 ("zisk-check-execute", "shards"), ("zisk-check-execute", "constants")]
 ("zisk-check-execute", "shards"), ("zisk-check-execute", "constants"),
 ("ix-decompile", "file-size"), ("ix-decompile", "constants")]

/-- Canonical units per measure slug, asserted on every sync: bencher
 auto-creates a measure with placeholder units ("Measure (units)") on
Expand All@@ -92,6 +99,7 @@ def unitsFor (slug : String) : Option String :=
 if slug.startsWith "phase-" then some "seconds (s)" else
 [("execute-peak-rss", "bytes (B)"),
 ("compile-time", "seconds (s)"),
 ("decompile-time", "seconds (s)"),
 ("execute-time", "seconds (s)"),
 ("prove-time", "seconds (s)"),
 ("verify-time", "seconds (s)"),
Expand All@@ -115,7 +123,7 @@ def unitsFor (slug : String) : Option String :=
/-- Dashboard group order (compile first, then aiur prove/execute, zisk,
 ooc); unranked workloads (a future backend) sort last. -/
def workloadOrder : List String :=
 ["ix-compile", "aiur-check-prove", "aiur-check-execute",
 ["ix-compile", "ix-decompile", "aiur-check-prove", "aiur-check-execute",
 "aiur-check-recursive", "aiur-recursive", "zisk-check-execute",
 "ooc-check"]

Expand All@@ -127,7 +135,8 @@ structure PlotSpec where
/-- One spec per bench-main testbed: its measure slugs and the benchmark
 row names uploaded there, mirroring the row emitters — compile keys
 one row per env (benched or not: the compile matrix is deliberately
 wider), ooc one whole-env row plus one full-closure row per primary,
 wider), decompile one row per benched env (a `.ixe` consumer), ooc one
 whole-env row plus one full-closure row per primary,
 the per-constant backends one row per primary. Dynamic sub-rows
 (`<name>/shard-N`) are left out: their multiplicity shifts with the
 shard manifest, and the parent row carries the headline trend. -/
Expand All@@ -142,6 +151,10 @@ def plotSpecs (rows : Array BenchCmd.VectorRow) : Array PlotSpec := Id.run do
 return (BenchCmd.envSpecs.map (·.name)).toArray
 if b.name == "aiur-recursive" then
 return (BenchCmd.recursiveConfigs.map (·.1)).toArray
 -- decompile is env-keyed like compile but a `.ixe` consumer: one row
 -- per benched env (it runs only where a benched `.ixe` exists).
 if b.name == "decompile" then
 return benched.toArray
 let mut ns : Array String := #[]
 for env in benched do
 if b.name == "ooc" then ns := ns.push env
Expand Down

2 changes: 1 addition & 1 deletion
Ix/Cli/BenchReport.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -43,7 +43,7 @@ def metricKind (metric : String) : String :=
 then "bytes"
 else if metric.startsWith "phase-" then "seconds"
 else if ["execute-time", "prove-time", "verify-time", "check-time",
 "compile-time"].contains metric then "seconds"
 "compile-time", "decompile-time"].contains metric then "seconds"
 else if ["fft-cost", "cycles", "steps", "max-shard-cycles",
 "throughput"].contains metric then "count"
 else if ["constants", "shards"].contains metric then "int"
Expand Down

83 changes: 83 additions & 0 deletions
Ix/Cli/DecompileCmd.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
/-
 `ix decompile <path.ixe>`: decompile a serialized `.ixe` environment back to
 Lean constants — the inverse of `ix compile`. This is the decompile
 benchmark's measured tool (env-keyed row, mirroring `ix compile --json`).

 With `--json` the run records one env-keyed results row (decompile-time,
 file-size, constants, throughput, peak-rss). A malformed decompile is a hard
 error (nonzero exit → red cell). Deeper compile→decompile roundtrip fidelity
 is gated by the canonical roundtrip checks (`ix validate` / the roundtrip
 tests), which need the original Lean env a `.ixe` can't supply — so this
 performance tool does not reproduce them.
-/
module
public import Cli
public import Ix.Common
public import Ix.TracingTexray
public import Ix.Benchmark.Results

public section

open System (FilePath)

namespace Ix.Cli.DecompileCmd

/-- Decompile a `.ixe` from disk, returning the decompiled constant
 count. A malformed decompile throws (hard error). Implemented in
 `crates/ffi/src/compile.rs::rs_decompile_env`. -/
@[extern "rs_decompile_env"]
opaque rsDecompileEnvFFI : @& String → IO Nat

def runDecompileCmd (p : Cli.Parsed) : IO UInt32 := do
 let some pathArg := p.positionalArg? "path"
 | p.printError "error: must specify <path> to a .ixe file"
 return Ix.Benchmark.Results.exitUsage
 let envPath := pathArg.as! String

 -- Window the tree-RSS sampler around the decompile, mirroring
 -- `ix compile --json` so the two rows share measurement
 -- infrastructure and peak-rss semantics.
 let benched := (p.flag? "json").isSome
 if benched then
 TracingTexray.startSampler
 TracingTexray.resetPeakTreeRss

 IO.println s!"Decompiling {envPath}"
 let start ← IO.monoMsNow
 let constants ← rsDecompileEnvFFI envPath
 let elapsed := (← IO.monoMsNow) - start
 IO.println s!"[decompile] {constants} constants in {elapsed.formatMs}"

 if let some flag := p.flag? "json" then
 let key := (p.flag? "json-name").map (·.as! String)
 |>.getD ((FilePath.mk envPath).fileStem.getD "env")
 let secs := elapsed.toFloat / 1000.0
 let tput := if elapsed > 0
 then constants.toFloat * 1000.0 / elapsed.toFloat else 0.0
 let peakRss ← TracingTexray.peakTreeRssBytes
 -- `file-size` is the INPUT `.ixe` the decompile consumed (the byte
 -- counterpart to compile's output `.ixe`).
 let size := (← (FilePath.mk envPath).metadata).byteSize.toNat
 Ix.Benchmark.Results.writeRow (flag.as! String) key "ok"
 [ ("decompile-time", Ix.Benchmark.Results.jsonRound 3 secs)
 , ("file-size", Lean.toJson size)
 , ("constants", Lean.toJson constants)
 , ("throughput", Ix.Benchmark.Results.jsonRound 2 tput)
 , ("peak-rss", Lean.toJson peakRss) ]

 return 0

end Ix.Cli.DecompileCmd

open Ix.Cli.DecompileCmd in
def decompileCmd : Cli.Cmd := `[Cli|
 decompile VIA runDecompileCmd;
 "Decompile a serialized `.ixe` env back to Lean constants (inverse of `ix compile`). Measures the decompile pass; a malformed decompile exits nonzero. Deep roundtrip fidelity is gated by `ix validate` / the roundtrip tests."

 FLAGS:
 json : String; "Write the decompile's benchmark results row (decompile-time, file-size, constants, throughput, peak-rss) to this path, merging into any existing rows object."
 "json-name" : String; "Row key for the --json row (default: the input `.ixe` file's stem)."

 ARGS:
 path : String; "Path to the serialized `.ixe` environment to decompile."
]
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 ix decompile CLI, fix Rust decompile perf and tests#490

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

 Merged

samuelburnham
merged 3 commits into

from

Jul 14, 2026
 Merged


feat: Add ix decompile CLI, fix Rust decompile perf and tests
#490
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


3 commits


Select commit
Hold shift + click to select a range
1064f84

perf: Fix ignored-test fallout from #484 and bound decompile/validate…


samuelburnham Jul 13, 2026
41a1876

feat: Add `ix decompile` and its benchmark backend


samuelburnham Jul 13, 2026
ba9a104

test: Cover Rust decompile over the serialized roundtrip


samuelburnham Jul 13, 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


82 changes: 81 additions & 1 deletion
.github/workflows/bench-main.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,7 +16,10 @@ name: Benchmark main
# 4. ooc-check — restore that `.ixe` and run the out-of-circuit Rust kernel
# (the same kernel, out-of-circuit and parallel — far faster)
# over the whole env, tracking throughput.
# 5. aiur-recursive — the aiur-recursive toy
# 5. decompile — restore that `.ixe` and decompile it back to Lean constants
# (the inverse of step 1); tracks decompile-time /
# throughput / peak-rss.
# 6. aiur-recursive — the aiur-recursive toy
# (bench-recursive-verifier):
# prove fixed tiny statements, run the in-circuit
# multi-stark verifier over each proof, then prove THAT
Expand DownExpand Up@@ -617,3 +620,80 @@ jobs:
 --threshold-measure peak-rss --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
 --threshold-lower-boundary _

 # Decompile — the inverse of compile. Restore the compile job's cached
 # `.ixe` and decompile it back to Lean constants. One env-keyed row per
 # benched env, mirroring the `compile` cell. A malformed decompile exits
 # nonzero and reddens this step; deep roundtrip fidelity is gated by the
 # canonical checks (`ix validate` / roundtrip tests), not measured here. No
 # compiler or Lean toolchain build — `ix decompile` is a Rust FFI pass over
 # the cached `.ixe`, so this reuses the staged `ix` binary like ooc-check.
 decompile:
 name: decompile-${{ matrix.bench }}
 needs: [compile, plan]
 runs-on: warp-ubuntu-latest-x64-32x
 timeout-minutes: 60
 strategy:
 fail-fast: false
 matrix:
 bench: ${{ fromJson(needs.plan.outputs.bench-envs) }}
 steps:
 - uses: actions/checkout@v6
 - uses: actions/cache/restore@v5
 with:
 path: ~/.local/bin
 key: bench-bins-${{ github.sha }}
 - run: echo "$HOME/.local/bin" >> $GITHUB_PATH
 # Provision the toolchain so `ix` finds libleanshared (no package build).
 - uses: leanprover/lean-action@v1
 with:
 auto-config: false
 build: false
 use-github-cache: false
 # (The path list must match the compile job's save exactly.)
 - uses: actions/cache/restore@v5
 with:
 path: |
 ${{ matrix.bench }}.ixe
 zkshards-${{ matrix.bench }}
 key: bench-ixe-${{ github.sha }}-${{ matrix.bench }}
 fail-on-cache-miss: true
 # A malformed decompile exits nonzero → red X here; a clean run's row
 # uploads below.
 - name: Run decompile benchmark
 run: |
 ix bench run --backend decompile --env ${{ matrix.bench }} --mode execute \
 --ixe ${{ matrix.bench }}.ixe --out bench.json
 # Upload whatever clean rows exist even when the run step reddened the
 # job — bmf drops every non-ok (rejected/oom) row.
 - name: Convert to Bencher Metric Format
 id: bmf
 if: ${{ !cancelled() }}
 run: |
 ix bench bmf --in bench.json --out bench-bmf.json
 cat bench-bmf.json
 # constants is deterministic → pinned (0/0); decompile-time / throughput
 # / peak-rss are noisy wall-clock → percentage bounds. file-size (the
 # input `.ixe`) duplicates the compile cell's, so it uploads for the
 # row's completeness but rides no threshold here.
 - uses: ./.github/actions/bencher-track
 if: ${{ !cancelled() && steps.bmf.outcome == 'success' }}
 with:
 testbed: ix-decompile-x64-32x
 workload: ix-decompile
 file: bench-bmf.json
 key: ${{ secrets.BENCHER_API_KEY }}
 github-token: ${{ secrets.GITHUB_TOKEN }}
 thresholds: |
 --threshold-measure constants --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0
 --threshold-lower-boundary 0
 --threshold-measure decompile-time --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
 --threshold-lower-boundary _
 --threshold-measure throughput --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary _
 --threshold-lower-boundary 0.10
 --threshold-measure peak-rss --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
 --threshold-lower-boundary _

12 changes: 7 additions & 5 deletions
.github/workflows/bench-pr.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
# `!benchmark` PR command: run the curated constant set (Benchmarks/Vectors.csv)
# through chosen prover backend(s) and post a main-vs-PR comparison table.
#
# !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [aiur-recursive] | all) [execute]
# !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [decompile] [aiur-recursive] | all) [execute]
# (sp1 is disabled in the registry (Ix/Cli/BenchCmd.lean) — the parser skips it
# with a note in the config summary)
# BENCH_ENVS=InitStd,Mathlib # which compiled envs (default InitStd; case-insensitive;
Expand All@@ -20,10 +20,12 @@
# Phase-1 columns `fft-cost` / `execute-time` measured en route; `zisk` /
# `sp1` / `ooc` run `execute`; `compile` runs `ix compile <env>.lean →
# <env>.ixe` (the same cell bench-main.yml uploads under testbed
# `ix-compile-*`); `aiur-recursive` runs the aiur-recursive toy
# (bench-recursive-verifier's fixed configs — env-independent, so it
# always schedules exactly one cell no matter what BENCH_ENVS says).
# The optional bare `execute` token flips `aiur` to
# `ix-compile-*`); `decompile` runs `ix decompile <env>.ixe` over the
# compile cell's fresh PR `.ixe` (testbed `ix-decompile-*`);
# `aiur-recursive` runs the aiur-recursive toy (bench-recursive-verifier's
# fixed configs — env-independent, so it always schedules exactly one cell
# no matter what BENCH_ENVS says). The optional bare `execute` token flips
# `aiur` to
# execute-only (Phase 1, skipping the prove); bench-main runs both aiur
# modes as separate cells on separate testbeds, so either kind of cell
# fetches a cached main-side baseline from bencher. (aiur's third mode,
Expand Down

8 changes: 4 additions & 4 deletions
.github/workflows/bencher-thresholds-reset.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -22,7 +22,7 @@ name: Bencher thresholds reset
# cancel by removing it before merge. Naming convention: one label per token,
# `bencher-thresholds-reset:<token>` where <token> is a workload (a backend
# testbed in Ix/Cli/BenchCmd.lean (backendSpecs) minus its runner-arch suffix:
# `ix-compile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `all` (the merge step expands an `all` label into every workload). Labeling
# requires Triage+, so PR authors from forks cannot self-queue a reset. The
# label shares the command/workflow name; the ref it moves is
Expand All@@ -44,7 +44,7 @@ on:
 # GitHub requires literal choice options, so this list stays static:
 # keep it (and the jobs' valid= lists below) in sync with the
 # backend testbeds in Ix/Cli/BenchCmd.lean (backendSpecs).
 options: [ix-compile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
 options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
 sha:
 description: "Commit to anchor to (default: HEAD)"
 required: false
Expand DownExpand Up@@ -77,7 +77,7 @@ jobs:
 # (backendSpecs) minus the runner-arch suffix. Static because this
 # job runs on a cheap runner with no built `ix`; keep in sync when
 # adding a backend.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 if [ "$EVENT" = workflow_dispatch ]; then
 # Reset the chosen workload(s) at the given commit; no PR scan.
 sha="${INPUT_SHA:-$HEAD_SHA}"
Expand DownExpand Up@@ -133,7 +133,7 @@ jobs:
 # which the merge job expands into every workload). Same static
 # list as the reset job; keep both in sync with backendSpecs in
 # Ix/Cli/BenchCmd.lean.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 accepted="$valid all"
 # Parse the workload token(s) after the command, lowercased.
 workloads=$(printf '%s' "$BODY" \
Expand Down

23 changes: 22 additions & 1 deletion
Ix/Cli/BenchCmd.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -185,6 +185,14 @@ def backendSpecs : List BackendSpec := [
 { name := "compile", defaultMode := "execute",
 testbeds := [("execute", "ix-compile-x64-32x")],
 metrics := [("execute", ["compile-time", "throughput", "peak-rss",
 "file-size", "constants"])] },
 -- The inverse of compile: decompiles the env's `.ixe` back to Lean
 -- constants (roundtrip-verified). Env-keyed like compile, but a `.ixe`
 -- CONSUMER — it reuses the compile cell's fresh `.ixe` rather than
 -- producing one.
 { name := "decompile", defaultMode := "execute",
 testbeds := [("execute", "ix-decompile-x64-32x")],
 metrics := [("execute", ["decompile-time", "throughput", "peak-rss",
 "file-size", "constants"])] }
]

Expand DownExpand Up@@ -492,6 +500,18 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do
 if exit != 0 then
 IO.eprintln s!"[bench] ix compile failed (exit {exit})"
 return 1
 | "decompile" =>
 -- The inverse of compile: consume the env's `.ixe` (the compile cell's
 -- fresh artifact) and decompile it back to Lean constants. Env-keyed row,
 -- like compile. A malformed decompile exits nonzero and reddens the cell;
 -- deep roundtrip fidelity is gated by the canonical roundtrip checks
 -- (`ix validate` / the roundtrip tests), not measured here.
 let ixe ← ensureIxe repo info ((p.flag? "ixe").map (·.as! String))
 let ix ← resolveBin repo "ix"
 let exit ← runGuarded watchdog ceilingGb ix
 #["decompile", ixe, "--json", out, "--json-name", info.name]
 if exit != 0 then
 IO.eprintln s!"[bench] ix decompile failed (exit {exit})"
 | "ooc" =>
 let ixe ← ensureIxe repo info ((p.flag? "ixe").map (·.as! String))
 let ix ← resolveBin repo "ix"
Expand DownExpand Up@@ -586,6 +606,7 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do
 -- row too.
 let expected := match backend with
 | "compile" => #[info.name]
 | "decompile" => #[info.name]
 | "ooc" => #[info.name] ++ names
 | "aiur-recursive" => (recursiveConfigs.map (·.1)).toArray
 | _ => names
Expand DownExpand Up@@ -630,7 +651,7 @@ def benchRunCmd : Cli.Cmd := `[Cli|
 "Run one benchmark cell (backend × env × mode), writing benchmark results JSON. Exits 0 on success (rows saved as the local baseline), 3 when the kernel rejected any constant, 1 when no rows were produced."

 FLAGS:
 backend : String; "aiur | zisk | sp1 | ooc | compile | aiur-recursive"
 backend : String; "aiur | zisk | sp1 | ooc | compile | decompile | aiur-recursive"
 env : String; "Benchmark env from the registry (default: InitStd)"
 mode : String; "prove | execute | recursive (default: the backend's defaultMode)"
 out : String; "Benchmark results JSON output path (default: bench.json)"
Expand Down

21 changes: 17 additions & 4 deletions
Ix/Cli/BenchPlots.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -54,6 +54,9 @@ def plotTitle (workload measure : String) : String :=
 | "ix-compile", "peak-rss" => "Ix Compile Peak RAM Usage"
 | "ix-compile", "file-size" => "Ix Environment Size"
 | "ix-compile", "constants" => "Ix Input Constants"
 | "ix-decompile", "decompile-time" => "Ix Decompile Time"
 | "ix-decompile", "throughput" => "Ix Decompile Throughput"
 | "ix-decompile", "peak-rss" => "Ix Decompile Peak RAM Usage"
 | "aiur-check-prove", "prove-time" => "Aiur Prove Time"
 | "aiur-check-prove", "throughput" => "Aiur Prove Throughput"
 | "aiur-check-prove", "peak-rss" => "Aiur Prove Peak RAM Usage"
Expand All@@ -78,10 +81,14 @@ def plotTitle (workload measure : String) : String :=
 "Aiur FFT Cost" from the prove cell). Zisk `shards` is a PR-comment
 column only ("Zisk Cycles" / max-shard-cycles carry the sharding
 trend), and zisk `constants` charts on the cross-kernel overlay below
 instead of alone. -/
 instead of alone. `ix-decompile` reuses the compile cell's `.ixe`, so
 its `file-size` / `constants` duplicate "Ix Environment Size" / "Ix
 Input Constants" exactly — the decompile cell tracks only its own
 decompile-time / throughput / peak-rss trends. -/
def plotSkips : List (String × String) :=
 [("aiur-check-prove", "execute-time"), ("aiur-check-execute", "fft-cost"),
 ("zisk-check-execute", "shards"), ("zisk-check-execute", "constants")]
 ("zisk-check-execute", "shards"), ("zisk-check-execute", "constants"),
 ("ix-decompile", "file-size"), ("ix-decompile", "constants")]

/-- Canonical units per measure slug, asserted on every sync: bencher
 auto-creates a measure with placeholder units ("Measure (units)") on
Expand All@@ -92,6 +99,7 @@ def unitsFor (slug : String) : Option String :=
 if slug.startsWith "phase-" then some "seconds (s)" else
 [("execute-peak-rss", "bytes (B)"),
 ("compile-time", "seconds (s)"),
 ("decompile-time", "seconds (s)"),
 ("execute-time", "seconds (s)"),
 ("prove-time", "seconds (s)"),
 ("verify-time", "seconds (s)"),
Expand All@@ -115,7 +123,7 @@ def unitsFor (slug : String) : Option String :=
/-- Dashboard group order (compile first, then aiur prove/execute, zisk,
 ooc); unranked workloads (a future backend) sort last. -/
def workloadOrder : List String :=
 ["ix-compile", "aiur-check-prove", "aiur-check-execute",
 ["ix-compile", "ix-decompile", "aiur-check-prove", "aiur-check-execute",
 "aiur-check-recursive", "aiur-recursive", "zisk-check-execute",
 "ooc-check"]

Expand All@@ -127,7 +135,8 @@ structure PlotSpec where
/-- One spec per bench-main testbed: its measure slugs and the benchmark
 row names uploaded there, mirroring the row emitters — compile keys
 one row per env (benched or not: the compile matrix is deliberately
 wider), ooc one whole-env row plus one full-closure row per primary,
 wider), decompile one row per benched env (a `.ixe` consumer), ooc one
 whole-env row plus one full-closure row per primary,
 the per-constant backends one row per primary. Dynamic sub-rows
 (`<name>/shard-N`) are left out: their multiplicity shifts with the
 shard manifest, and the parent row carries the headline trend. -/
Expand All@@ -142,6 +151,10 @@ def plotSpecs (rows : Array BenchCmd.VectorRow) : Array PlotSpec := Id.run do
 return (BenchCmd.envSpecs.map (·.name)).toArray
 if b.name == "aiur-recursive" then
 return (BenchCmd.recursiveConfigs.map (·.1)).toArray
 -- decompile is env-keyed like compile but a `.ixe` consumer: one row
 -- per benched env (it runs only where a benched `.ixe` exists).
 if b.name == "decompile" then
 return benched.toArray
 let mut ns : Array String := #[]
 for env in benched do
 if b.name == "ooc" then ns := ns.push env
Expand Down

2 changes: 1 addition & 1 deletion
Ix/Cli/BenchReport.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -43,7 +43,7 @@ def metricKind (metric : String) : String :=
 then "bytes"
 else if metric.startsWith "phase-" then "seconds"
 else if ["execute-time", "prove-time", "verify-time", "check-time",
 "compile-time"].contains metric then "seconds"
 "compile-time", "decompile-time"].contains metric then "seconds"
 else if ["fft-cost", "cycles", "steps", "max-shard-cycles",
 "throughput"].contains metric then "count"
 else if ["constants", "shards"].contains metric then "int"
Expand Down

83 changes: 83 additions & 0 deletions
Ix/Cli/DecompileCmd.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
/-
 `ix decompile <path.ixe>`: decompile a serialized `.ixe` environment back to
 Lean constants — the inverse of `ix compile`. This is the decompile
 benchmark's measured tool (env-keyed row, mirroring `ix compile --json`).

 With `--json` the run records one env-keyed results row (decompile-time,
 file-size, constants, throughput, peak-rss). A malformed decompile is a hard
 error (nonzero exit → red cell). Deeper compile→decompile roundtrip fidelity
 is gated by the canonical roundtrip checks (`ix validate` / the roundtrip
 tests), which need the original Lean env a `.ixe` can't supply — so this
 performance tool does not reproduce them.
-/
module
public import Cli
public import Ix.Common
public import Ix.TracingTexray
public import Ix.Benchmark.Results

public section

open System (FilePath)

namespace Ix.Cli.DecompileCmd

/-- Decompile a `.ixe` from disk, returning the decompiled constant
 count. A malformed decompile throws (hard error). Implemented in
 `crates/ffi/src/compile.rs::rs_decompile_env`. -/
@[extern "rs_decompile_env"]
opaque rsDecompileEnvFFI : @& String → IO Nat

def runDecompileCmd (p : Cli.Parsed) : IO UInt32 := do
 let some pathArg := p.positionalArg? "path"
 | p.printError "error: must specify <path> to a .ixe file"
 return Ix.Benchmark.Results.exitUsage
 let envPath := pathArg.as! String

 -- Window the tree-RSS sampler around the decompile, mirroring
 -- `ix compile --json` so the two rows share measurement
 -- infrastructure and peak-rss semantics.
 let benched := (p.flag? "json").isSome
 if benched then
 TracingTexray.startSampler
 TracingTexray.resetPeakTreeRss

 IO.println s!"Decompiling {envPath}"
 let start ← IO.monoMsNow
 let constants ← rsDecompileEnvFFI envPath
 let elapsed := (← IO.monoMsNow) - start
 IO.println s!"[decompile] {constants} constants in {elapsed.formatMs}"

 if let some flag := p.flag? "json" then
 let key := (p.flag? "json-name").map (·.as! String)
 |>.getD ((FilePath.mk envPath).fileStem.getD "env")
 let secs := elapsed.toFloat / 1000.0
 let tput := if elapsed > 0
 then constants.toFloat * 1000.0 / elapsed.toFloat else 0.0
 let peakRss ← TracingTexray.peakTreeRssBytes
 -- `file-size` is the INPUT `.ixe` the decompile consumed (the byte
 -- counterpart to compile's output `.ixe`).
 let size := (← (FilePath.mk envPath).metadata).byteSize.toNat
 Ix.Benchmark.Results.writeRow (flag.as! String) key "ok"
 [ ("decompile-time", Ix.Benchmark.Results.jsonRound 3 secs)
 , ("file-size", Lean.toJson size)
 , ("constants", Lean.toJson constants)
 , ("throughput", Ix.Benchmark.Results.jsonRound 2 tput)
 , ("peak-rss", Lean.toJson peakRss) ]

 return 0

end Ix.Cli.DecompileCmd

open Ix.Cli.DecompileCmd in
def decompileCmd : Cli.Cmd := `[Cli|
 decompile VIA runDecompileCmd;
 "Decompile a serialized `.ixe` env back to Lean constants (inverse of `ix compile`). Measures the decompile pass; a malformed decompile exits nonzero. Deep roundtrip fidelity is gated by `ix validate` / the roundtrip tests."

 FLAGS:
 json : String; "Write the decompile's benchmark results row (decompile-time, file-size, constants, throughput, peak-rss) to this path, merging into any existing rows object."
 "json-name" : String; "Row key for the --json row (default: the input `.ixe` file's stem)."

 ARGS:
 path : String; "Path to the serialized `.ixe` environment to decompile."
]
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 ix decompile CLI, fix Rust decompile perf and tests#490

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

 Merged

samuelburnham
merged 3 commits into

from

Jul 14, 2026
 Merged


feat: Add ix decompile CLI, fix Rust decompile perf and tests
#490
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


3 commits


Select commit
Hold shift + click to select a range
1064f84

perf: Fix ignored-test fallout from #484 and bound decompile/validate…


samuelburnham Jul 13, 2026
41a1876

feat: Add `ix decompile` and its benchmark backend


samuelburnham Jul 13, 2026
ba9a104

test: Cover Rust decompile over the serialized roundtrip


samuelburnham Jul 13, 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


82 changes: 81 additions & 1 deletion
.github/workflows/bench-main.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,7 +16,10 @@ name: Benchmark main
# 4. ooc-check — restore that `.ixe` and run the out-of-circuit Rust kernel
# (the same kernel, out-of-circuit and parallel — far faster)
# over the whole env, tracking throughput.
# 5. aiur-recursive — the aiur-recursive toy
# 5. decompile — restore that `.ixe` and decompile it back to Lean constants
# (the inverse of step 1); tracks decompile-time /
# throughput / peak-rss.
# 6. aiur-recursive — the aiur-recursive toy
# (bench-recursive-verifier):
# prove fixed tiny statements, run the in-circuit
# multi-stark verifier over each proof, then prove THAT
Expand DownExpand Up@@ -617,3 +620,80 @@ jobs:
 --threshold-measure peak-rss --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
 --threshold-lower-boundary _

 # Decompile — the inverse of compile. Restore the compile job's cached
 # `.ixe` and decompile it back to Lean constants. One env-keyed row per
 # benched env, mirroring the `compile` cell. A malformed decompile exits
 # nonzero and reddens this step; deep roundtrip fidelity is gated by the
 # canonical checks (`ix validate` / roundtrip tests), not measured here. No
 # compiler or Lean toolchain build — `ix decompile` is a Rust FFI pass over
 # the cached `.ixe`, so this reuses the staged `ix` binary like ooc-check.
 decompile:
 name: decompile-${{ matrix.bench }}
 needs: [compile, plan]
 runs-on: warp-ubuntu-latest-x64-32x
 timeout-minutes: 60
 strategy:
 fail-fast: false
 matrix:
 bench: ${{ fromJson(needs.plan.outputs.bench-envs) }}
 steps:
 - uses: actions/checkout@v6
 - uses: actions/cache/restore@v5
 with:
 path: ~/.local/bin
 key: bench-bins-${{ github.sha }}
 - run: echo "$HOME/.local/bin" >> $GITHUB_PATH
 # Provision the toolchain so `ix` finds libleanshared (no package build).
 - uses: leanprover/lean-action@v1
 with:
 auto-config: false
 build: false
 use-github-cache: false
 # (The path list must match the compile job's save exactly.)
 - uses: actions/cache/restore@v5
 with:
 path: |
 ${{ matrix.bench }}.ixe
 zkshards-${{ matrix.bench }}
 key: bench-ixe-${{ github.sha }}-${{ matrix.bench }}
 fail-on-cache-miss: true
 # A malformed decompile exits nonzero → red X here; a clean run's row
 # uploads below.
 - name: Run decompile benchmark
 run: |
 ix bench run --backend decompile --env ${{ matrix.bench }} --mode execute \
 --ixe ${{ matrix.bench }}.ixe --out bench.json
 # Upload whatever clean rows exist even when the run step reddened the
 # job — bmf drops every non-ok (rejected/oom) row.
 - name: Convert to Bencher Metric Format
 id: bmf
 if: ${{ !cancelled() }}
 run: |
 ix bench bmf --in bench.json --out bench-bmf.json
 cat bench-bmf.json
 # constants is deterministic → pinned (0/0); decompile-time / throughput
 # / peak-rss are noisy wall-clock → percentage bounds. file-size (the
 # input `.ixe`) duplicates the compile cell's, so it uploads for the
 # row's completeness but rides no threshold here.
 - uses: ./.github/actions/bencher-track
 if: ${{ !cancelled() && steps.bmf.outcome == 'success' }}
 with:
 testbed: ix-decompile-x64-32x
 workload: ix-decompile
 file: bench-bmf.json
 key: ${{ secrets.BENCHER_API_KEY }}
 github-token: ${{ secrets.GITHUB_TOKEN }}
 thresholds: |
 --threshold-measure constants --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0
 --threshold-lower-boundary 0
 --threshold-measure decompile-time --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
 --threshold-lower-boundary _
 --threshold-measure throughput --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary _
 --threshold-lower-boundary 0.10
 --threshold-measure peak-rss --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
 --threshold-lower-boundary _

12 changes: 7 additions & 5 deletions
.github/workflows/bench-pr.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
# `!benchmark` PR command: run the curated constant set (Benchmarks/Vectors.csv)
# through chosen prover backend(s) and post a main-vs-PR comparison table.
#
# !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [aiur-recursive] | all) [execute]
# !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [decompile] [aiur-recursive] | all) [execute]
# (sp1 is disabled in the registry (Ix/Cli/BenchCmd.lean) — the parser skips it
# with a note in the config summary)
# BENCH_ENVS=InitStd,Mathlib # which compiled envs (default InitStd; case-insensitive;
Expand All@@ -20,10 +20,12 @@
# Phase-1 columns `fft-cost` / `execute-time` measured en route; `zisk` /
# `sp1` / `ooc` run `execute`; `compile` runs `ix compile <env>.lean →
# <env>.ixe` (the same cell bench-main.yml uploads under testbed
# `ix-compile-*`); `aiur-recursive` runs the aiur-recursive toy
# (bench-recursive-verifier's fixed configs — env-independent, so it
# always schedules exactly one cell no matter what BENCH_ENVS says).
# The optional bare `execute` token flips `aiur` to
# `ix-compile-*`); `decompile` runs `ix decompile <env>.ixe` over the
# compile cell's fresh PR `.ixe` (testbed `ix-decompile-*`);
# `aiur-recursive` runs the aiur-recursive toy (bench-recursive-verifier's
# fixed configs — env-independent, so it always schedules exactly one cell
# no matter what BENCH_ENVS says). The optional bare `execute` token flips
# `aiur` to
# execute-only (Phase 1, skipping the prove); bench-main runs both aiur
# modes as separate cells on separate testbeds, so either kind of cell
# fetches a cached main-side baseline from bencher. (aiur's third mode,
Expand Down

8 changes: 4 additions & 4 deletions
.github/workflows/bencher-thresholds-reset.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -22,7 +22,7 @@ name: Bencher thresholds reset
# cancel by removing it before merge. Naming convention: one label per token,
# `bencher-thresholds-reset:<token>` where <token> is a workload (a backend
# testbed in Ix/Cli/BenchCmd.lean (backendSpecs) minus its runner-arch suffix:
# `ix-compile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `all` (the merge step expands an `all` label into every workload). Labeling
# requires Triage+, so PR authors from forks cannot self-queue a reset. The
# label shares the command/workflow name; the ref it moves is
Expand All@@ -44,7 +44,7 @@ on:
 # GitHub requires literal choice options, so this list stays static:
 # keep it (and the jobs' valid= lists below) in sync with the
 # backend testbeds in Ix/Cli/BenchCmd.lean (backendSpecs).
 options: [ix-compile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
 options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
 sha:
 description: "Commit to anchor to (default: HEAD)"
 required: false
Expand DownExpand Up@@ -77,7 +77,7 @@ jobs:
 # (backendSpecs) minus the runner-arch suffix. Static because this
 # job runs on a cheap runner with no built `ix`; keep in sync when
 # adding a backend.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 if [ "$EVENT" = workflow_dispatch ]; then
 # Reset the chosen workload(s) at the given commit; no PR scan.
 sha="${INPUT_SHA:-$HEAD_SHA}"
Expand DownExpand Up@@ -133,7 +133,7 @@ jobs:
 # which the merge job expands into every workload). Same static
 # list as the reset job; keep both in sync with backendSpecs in
 # Ix/Cli/BenchCmd.lean.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 accepted="$valid all"
 # Parse the workload token(s) after the command, lowercased.
 workloads=$(printf '%s' "$BODY" \
Expand Down

23 changes: 22 additions & 1 deletion
Ix/Cli/BenchCmd.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -185,6 +185,14 @@ def backendSpecs : List BackendSpec := [
 { name := "compile", defaultMode := "execute",
 testbeds := [("execute", "ix-compile-x64-32x")],
 metrics := [("execute", ["compile-time", "throughput", "peak-rss",
 "file-size", "constants"])] },
 -- The inverse of compile: decompiles the env's `.ixe` back to Lean
 -- constants (roundtrip-verified). Env-keyed like compile, but a `.ixe`
 -- CONSUMER — it reuses the compile cell's fresh `.ixe` rather than
 -- producing one.
 { name := "decompile", defaultMode := "execute",
 testbeds := [("execute", "ix-decompile-x64-32x")],
 metrics := [("execute", ["decompile-time", "throughput", "peak-rss",
 "file-size", "constants"])] }
]

Expand DownExpand Up@@ -492,6 +500,18 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do
 if exit != 0 then
 IO.eprintln s!"[bench] ix compile failed (exit {exit})"
 return 1
 | "decompile" =>
 -- The inverse of compile: consume the env's `.ixe` (the compile cell's
 -- fresh artifact) and decompile it back to Lean constants. Env-keyed row,
 -- like compile. A malformed decompile exits nonzero and reddens the cell;
 -- deep roundtrip fidelity is gated by the canonical roundtrip checks
 -- (`ix validate` / the roundtrip tests), not measured here.
 let ixe ← ensureIxe repo info ((p.flag? "ixe").map (·.as! String))
 let ix ← resolveBin repo "ix"
 let exit ← runGuarded watchdog ceilingGb ix
 #["decompile", ixe, "--json", out, "--json-name", info.name]
 if exit != 0 then
 IO.eprintln s!"[bench] ix decompile failed (exit {exit})"
 | "ooc" =>
 let ixe ← ensureIxe repo info ((p.flag? "ixe").map (·.as! String))
 let ix ← resolveBin repo "ix"
Expand DownExpand Up@@ -586,6 +606,7 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do
 -- row too.
 let expected := match backend with
 | "compile" => #[info.name]
 | "decompile" => #[info.name]
 | "ooc" => #[info.name] ++ names
 | "aiur-recursive" => (recursiveConfigs.map (·.1)).toArray
 | _ => names
Expand DownExpand Up@@ -630,7 +651,7 @@ def benchRunCmd : Cli.Cmd := `[Cli|
 "Run one benchmark cell (backend × env × mode), writing benchmark results JSON. Exits 0 on success (rows saved as the local baseline), 3 when the kernel rejected any constant, 1 when no rows were produced."

 FLAGS:
 backend : String; "aiur | zisk | sp1 | ooc | compile | aiur-recursive"
 backend : String; "aiur | zisk | sp1 | ooc | compile | decompile | aiur-recursive"
 env : String; "Benchmark env from the registry (default: InitStd)"
 mode : String; "prove | execute | recursive (default: the backend's defaultMode)"
 out : String; "Benchmark results JSON output path (default: bench.json)"
Expand Down

21 changes: 17 additions & 4 deletions
Ix/Cli/BenchPlots.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -54,6 +54,9 @@ def plotTitle (workload measure : String) : String :=
 | "ix-compile", "peak-rss" => "Ix Compile Peak RAM Usage"
 | "ix-compile", "file-size" => "Ix Environment Size"
 | "ix-compile", "constants" => "Ix Input Constants"
 | "ix-decompile", "decompile-time" => "Ix Decompile Time"
 | "ix-decompile", "throughput" => "Ix Decompile Throughput"
 | "ix-decompile", "peak-rss" => "Ix Decompile Peak RAM Usage"
 | "aiur-check-prove", "prove-time" => "Aiur Prove Time"
 | "aiur-check-prove", "throughput" => "Aiur Prove Throughput"
 | "aiur-check-prove", "peak-rss" => "Aiur Prove Peak RAM Usage"
Expand All@@ -78,10 +81,14 @@ def plotTitle (workload measure : String) : String :=
 "Aiur FFT Cost" from the prove cell). Zisk `shards` is a PR-comment
 column only ("Zisk Cycles" / max-shard-cycles carry the sharding
 trend), and zisk `constants` charts on the cross-kernel overlay below
 instead of alone. -/
 instead of alone. `ix-decompile` reuses the compile cell's `.ixe`, so
 its `file-size` / `constants` duplicate "Ix Environment Size" / "Ix
 Input Constants" exactly — the decompile cell tracks only its own
 decompile-time / throughput / peak-rss trends. -/
def plotSkips : List (String × String) :=
 [("aiur-check-prove", "execute-time"), ("aiur-check-execute", "fft-cost"),
 ("zisk-check-execute", "shards"), ("zisk-check-execute", "constants")]
 ("zisk-check-execute", "shards"), ("zisk-check-execute", "constants"),
 ("ix-decompile", "file-size"), ("ix-decompile", "constants")]

/-- Canonical units per measure slug, asserted on every sync: bencher
 auto-creates a measure with placeholder units ("Measure (units)") on
Expand All@@ -92,6 +99,7 @@ def unitsFor (slug : String) : Option String :=
 if slug.startsWith "phase-" then some "seconds (s)" else
 [("execute-peak-rss", "bytes (B)"),
 ("compile-time", "seconds (s)"),
 ("decompile-time", "seconds (s)"),
 ("execute-time", "seconds (s)"),
 ("prove-time", "seconds (s)"),
 ("verify-time", "seconds (s)"),
Expand All@@ -115,7 +123,7 @@ def unitsFor (slug : String) : Option String :=
/-- Dashboard group order (compile first, then aiur prove/execute, zisk,
 ooc); unranked workloads (a future backend) sort last. -/
def workloadOrder : List String :=
 ["ix-compile", "aiur-check-prove", "aiur-check-execute",
 ["ix-compile", "ix-decompile", "aiur-check-prove", "aiur-check-execute",
 "aiur-check-recursive", "aiur-recursive", "zisk-check-execute",
 "ooc-check"]

Expand All@@ -127,7 +135,8 @@ structure PlotSpec where
/-- One spec per bench-main testbed: its measure slugs and the benchmark
 row names uploaded there, mirroring the row emitters — compile keys
 one row per env (benched or not: the compile matrix is deliberately
 wider), ooc one whole-env row plus one full-closure row per primary,
 wider), decompile one row per benched env (a `.ixe` consumer), ooc one
 whole-env row plus one full-closure row per primary,
 the per-constant backends one row per primary. Dynamic sub-rows
 (`<name>/shard-N`) are left out: their multiplicity shifts with the
 shard manifest, and the parent row carries the headline trend. -/
Expand All@@ -142,6 +151,10 @@ def plotSpecs (rows : Array BenchCmd.VectorRow) : Array PlotSpec := Id.run do
 return (BenchCmd.envSpecs.map (·.name)).toArray
 if b.name == "aiur-recursive" then
 return (BenchCmd.recursiveConfigs.map (·.1)).toArray
 -- decompile is env-keyed like compile but a `.ixe` consumer: one row
 -- per benched env (it runs only where a benched `.ixe` exists).
 if b.name == "decompile" then
 return benched.toArray
 let mut ns : Array String := #[]
 for env in benched do
 if b.name == "ooc" then ns := ns.push env
Expand Down

2 changes: 1 addition & 1 deletion
Ix/Cli/BenchReport.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -43,7 +43,7 @@ def metricKind (metric : String) : String :=
 then "bytes"
 else if metric.startsWith "phase-" then "seconds"
 else if ["execute-time", "prove-time", "verify-time", "check-time",
 "compile-time"].contains metric then "seconds"
 "compile-time", "decompile-time"].contains metric then "seconds"
 else if ["fft-cost", "cycles", "steps", "max-shard-cycles",
 "throughput"].contains metric then "count"
 else if ["constants", "shards"].contains metric then "int"
Expand Down

83 changes: 83 additions & 0 deletions
Ix/Cli/DecompileCmd.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
/-
 `ix decompile <path.ixe>`: decompile a serialized `.ixe` environment back to
 Lean constants — the inverse of `ix compile`. This is the decompile
 benchmark's measured tool (env-keyed row, mirroring `ix compile --json`).

 With `--json` the run records one env-keyed results row (decompile-time,
 file-size, constants, throughput, peak-rss). A malformed decompile is a hard
 error (nonzero exit → red cell). Deeper compile→decompile roundtrip fidelity
 is gated by the canonical roundtrip checks (`ix validate` / the roundtrip
 tests), which need the original Lean env a `.ixe` can't supply — so this
 performance tool does not reproduce them.
-/
module
public import Cli
public import Ix.Common
public import Ix.TracingTexray
public import Ix.Benchmark.Results

public section

open System (FilePath)

namespace Ix.Cli.DecompileCmd

/-- Decompile a `.ixe` from disk, returning the decompiled constant
 count. A malformed decompile throws (hard error). Implemented in
 `crates/ffi/src/compile.rs::rs_decompile_env`. -/
@[extern "rs_decompile_env"]
opaque rsDecompileEnvFFI : @& String → IO Nat

def runDecompileCmd (p : Cli.Parsed) : IO UInt32 := do
 let some pathArg := p.positionalArg? "path"
 | p.printError "error: must specify <path> to a .ixe file"
 return Ix.Benchmark.Results.exitUsage
 let envPath := pathArg.as! String

 -- Window the tree-RSS sampler around the decompile, mirroring
 -- `ix compile --json` so the two rows share measurement
 -- infrastructure and peak-rss semantics.
 let benched := (p.flag? "json").isSome
 if benched then
 TracingTexray.startSampler
 TracingTexray.resetPeakTreeRss

 IO.println s!"Decompiling {envPath}"
 let start ← IO.monoMsNow
 let constants ← rsDecompileEnvFFI envPath
 let elapsed := (← IO.monoMsNow) - start
 IO.println s!"[decompile] {constants} constants in {elapsed.formatMs}"

 if let some flag := p.flag? "json" then
 let key := (p.flag? "json-name").map (·.as! String)
 |>.getD ((FilePath.mk envPath).fileStem.getD "env")
 let secs := elapsed.toFloat / 1000.0
 let tput := if elapsed > 0
 then constants.toFloat * 1000.0 / elapsed.toFloat else 0.0
 let peakRss ← TracingTexray.peakTreeRssBytes
 -- `file-size` is the INPUT `.ixe` the decompile consumed (the byte
 -- counterpart to compile's output `.ixe`).
 let size := (← (FilePath.mk envPath).metadata).byteSize.toNat
 Ix.Benchmark.Results.writeRow (flag.as! String) key "ok"
 [ ("decompile-time", Ix.Benchmark.Results.jsonRound 3 secs)
 , ("file-size", Lean.toJson size)
 , ("constants", Lean.toJson constants)
 , ("throughput", Ix.Benchmark.Results.jsonRound 2 tput)
 , ("peak-rss", Lean.toJson peakRss) ]

 return 0

end Ix.Cli.DecompileCmd

open Ix.Cli.DecompileCmd in
def decompileCmd : Cli.Cmd := `[Cli|
 decompile VIA runDecompileCmd;
 "Decompile a serialized `.ixe` env back to Lean constants (inverse of `ix compile`). Measures the decompile pass; a malformed decompile exits nonzero. Deep roundtrip fidelity is gated by `ix validate` / the roundtrip tests."

 FLAGS:
 json : String; "Write the decompile's benchmark results row (decompile-time, file-size, constants, throughput, peak-rss) to this path, merging into any existing rows object."
 "json-name" : String; "Row key for the --json row (default: the input `.ixe` file's stem)."

 ARGS:
 path : String; "Path to the serialized `.ixe` environment to decompile."
]
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 ix decompile CLI, fix Rust decompile perf and tests#490

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

 Merged

samuelburnham
merged 3 commits into

from

Jul 14, 2026
 Merged


feat: Add ix decompile CLI, fix Rust decompile perf and tests
#490
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


3 commits


Select commit
Hold shift + click to select a range
1064f84

perf: Fix ignored-test fallout from #484 and bound decompile/validate…


samuelburnham Jul 13, 2026
41a1876

feat: Add `ix decompile` and its benchmark backend


samuelburnham Jul 13, 2026
ba9a104

test: Cover Rust decompile over the serialized roundtrip


samuelburnham Jul 13, 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


82 changes: 81 additions & 1 deletion
.github/workflows/bench-main.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,7 +16,10 @@ name: Benchmark main
# 4. ooc-check — restore that `.ixe` and run the out-of-circuit Rust kernel
# (the same kernel, out-of-circuit and parallel — far faster)
# over the whole env, tracking throughput.
# 5. aiur-recursive — the aiur-recursive toy
# 5. decompile — restore that `.ixe` and decompile it back to Lean constants
# (the inverse of step 1); tracks decompile-time /
# throughput / peak-rss.
# 6. aiur-recursive — the aiur-recursive toy
# (bench-recursive-verifier):
# prove fixed tiny statements, run the in-circuit
# multi-stark verifier over each proof, then prove THAT
Expand DownExpand Up@@ -617,3 +620,80 @@ jobs:
 --threshold-measure peak-rss --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
 --threshold-lower-boundary _

 # Decompile — the inverse of compile. Restore the compile job's cached
 # `.ixe` and decompile it back to Lean constants. One env-keyed row per
 # benched env, mirroring the `compile` cell. A malformed decompile exits
 # nonzero and reddens this step; deep roundtrip fidelity is gated by the
 # canonical checks (`ix validate` / roundtrip tests), not measured here. No
 # compiler or Lean toolchain build — `ix decompile` is a Rust FFI pass over
 # the cached `.ixe`, so this reuses the staged `ix` binary like ooc-check.
 decompile:
 name: decompile-${{ matrix.bench }}
 needs: [compile, plan]
 runs-on: warp-ubuntu-latest-x64-32x
 timeout-minutes: 60
 strategy:
 fail-fast: false
 matrix:
 bench: ${{ fromJson(needs.plan.outputs.bench-envs) }}
 steps:
 - uses: actions/checkout@v6
 - uses: actions/cache/restore@v5
 with:
 path: ~/.local/bin
 key: bench-bins-${{ github.sha }}
 - run: echo "$HOME/.local/bin" >> $GITHUB_PATH
 # Provision the toolchain so `ix` finds libleanshared (no package build).
 - uses: leanprover/lean-action@v1
 with:
 auto-config: false
 build: false
 use-github-cache: false
 # (The path list must match the compile job's save exactly.)
 - uses: actions/cache/restore@v5
 with:
 path: |
 ${{ matrix.bench }}.ixe
 zkshards-${{ matrix.bench }}
 key: bench-ixe-${{ github.sha }}-${{ matrix.bench }}
 fail-on-cache-miss: true
 # A malformed decompile exits nonzero → red X here; a clean run's row
 # uploads below.
 - name: Run decompile benchmark
 run: |
 ix bench run --backend decompile --env ${{ matrix.bench }} --mode execute \
 --ixe ${{ matrix.bench }}.ixe --out bench.json
 # Upload whatever clean rows exist even when the run step reddened the
 # job — bmf drops every non-ok (rejected/oom) row.
 - name: Convert to Bencher Metric Format
 id: bmf
 if: ${{ !cancelled() }}
 run: |
 ix bench bmf --in bench.json --out bench-bmf.json
 cat bench-bmf.json
 # constants is deterministic → pinned (0/0); decompile-time / throughput
 # / peak-rss are noisy wall-clock → percentage bounds. file-size (the
 # input `.ixe`) duplicates the compile cell's, so it uploads for the
 # row's completeness but rides no threshold here.
 - uses: ./.github/actions/bencher-track
 if: ${{ !cancelled() && steps.bmf.outcome == 'success' }}
 with:
 testbed: ix-decompile-x64-32x
 workload: ix-decompile
 file: bench-bmf.json
 key: ${{ secrets.BENCHER_API_KEY }}
 github-token: ${{ secrets.GITHUB_TOKEN }}
 thresholds: |
 --threshold-measure constants --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0
 --threshold-lower-boundary 0
 --threshold-measure decompile-time --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
 --threshold-lower-boundary _
 --threshold-measure throughput --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary _
 --threshold-lower-boundary 0.10
 --threshold-measure peak-rss --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
 --threshold-lower-boundary _

12 changes: 7 additions & 5 deletions
.github/workflows/bench-pr.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
# `!benchmark` PR command: run the curated constant set (Benchmarks/Vectors.csv)
# through chosen prover backend(s) and post a main-vs-PR comparison table.
#
# !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [aiur-recursive] | all) [execute]
# !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [decompile] [aiur-recursive] | all) [execute]
# (sp1 is disabled in the registry (Ix/Cli/BenchCmd.lean) — the parser skips it
# with a note in the config summary)
# BENCH_ENVS=InitStd,Mathlib # which compiled envs (default InitStd; case-insensitive;
Expand All@@ -20,10 +20,12 @@
# Phase-1 columns `fft-cost` / `execute-time` measured en route; `zisk` /
# `sp1` / `ooc` run `execute`; `compile` runs `ix compile <env>.lean →
# <env>.ixe` (the same cell bench-main.yml uploads under testbed
# `ix-compile-*`); `aiur-recursive` runs the aiur-recursive toy
# (bench-recursive-verifier's fixed configs — env-independent, so it
# always schedules exactly one cell no matter what BENCH_ENVS says).
# The optional bare `execute` token flips `aiur` to
# `ix-compile-*`); `decompile` runs `ix decompile <env>.ixe` over the
# compile cell's fresh PR `.ixe` (testbed `ix-decompile-*`);
# `aiur-recursive` runs the aiur-recursive toy (bench-recursive-verifier's
# fixed configs — env-independent, so it always schedules exactly one cell
# no matter what BENCH_ENVS says). The optional bare `execute` token flips
# `aiur` to
# execute-only (Phase 1, skipping the prove); bench-main runs both aiur
# modes as separate cells on separate testbeds, so either kind of cell
# fetches a cached main-side baseline from bencher. (aiur's third mode,
Expand Down

8 changes: 4 additions & 4 deletions
.github/workflows/bencher-thresholds-reset.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -22,7 +22,7 @@ name: Bencher thresholds reset
# cancel by removing it before merge. Naming convention: one label per token,
# `bencher-thresholds-reset:<token>` where <token> is a workload (a backend
# testbed in Ix/Cli/BenchCmd.lean (backendSpecs) minus its runner-arch suffix:
# `ix-compile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `all` (the merge step expands an `all` label into every workload). Labeling
# requires Triage+, so PR authors from forks cannot self-queue a reset. The
# label shares the command/workflow name; the ref it moves is
Expand All@@ -44,7 +44,7 @@ on:
 # GitHub requires literal choice options, so this list stays static:
 # keep it (and the jobs' valid= lists below) in sync with the
 # backend testbeds in Ix/Cli/BenchCmd.lean (backendSpecs).
 options: [ix-compile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
 options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
 sha:
 description: "Commit to anchor to (default: HEAD)"
 required: false
Expand DownExpand Up@@ -77,7 +77,7 @@ jobs:
 # (backendSpecs) minus the runner-arch suffix. Static because this
 # job runs on a cheap runner with no built `ix`; keep in sync when
 # adding a backend.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 if [ "$EVENT" = workflow_dispatch ]; then
 # Reset the chosen workload(s) at the given commit; no PR scan.
 sha="${INPUT_SHA:-$HEAD_SHA}"
Expand DownExpand Up@@ -133,7 +133,7 @@ jobs:
 # which the merge job expands into every workload). Same static
 # list as the reset job; keep both in sync with backendSpecs in
 # Ix/Cli/BenchCmd.lean.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 accepted="$valid all"
 # Parse the workload token(s) after the command, lowercased.
 workloads=$(printf '%s' "$BODY" \
Expand Down

23 changes: 22 additions & 1 deletion
Ix/Cli/BenchCmd.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -185,6 +185,14 @@ def backendSpecs : List BackendSpec := [
 { name := "compile", defaultMode := "execute",
 testbeds := [("execute", "ix-compile-x64-32x")],
 metrics := [("execute", ["compile-time", "throughput", "peak-rss",
 "file-size", "constants"])] },
 -- The inverse of compile: decompiles the env's `.ixe` back to Lean
 -- constants (roundtrip-verified). Env-keyed like compile, but a `.ixe`
 -- CONSUMER — it reuses the compile cell's fresh `.ixe` rather than
 -- producing one.
 { name := "decompile", defaultMode := "execute",
 testbeds := [("execute", "ix-decompile-x64-32x")],
 metrics := [("execute", ["decompile-time", "throughput", "peak-rss",
 "file-size", "constants"])] }
]

Expand DownExpand Up@@ -492,6 +500,18 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do
 if exit != 0 then
 IO.eprintln s!"[bench] ix compile failed (exit {exit})"
 return 1
 | "decompile" =>
 -- The inverse of compile: consume the env's `.ixe` (the compile cell's
 -- fresh artifact) and decompile it back to Lean constants. Env-keyed row,
 -- like compile. A malformed decompile exits nonzero and reddens the cell;
 -- deep roundtrip fidelity is gated by the canonical roundtrip checks
 -- (`ix validate` / the roundtrip tests), not measured here.
 let ixe ← ensureIxe repo info ((p.flag? "ixe").map (·.as! String))
 let ix ← resolveBin repo "ix"
 let exit ← runGuarded watchdog ceilingGb ix
 #["decompile", ixe, "--json", out, "--json-name", info.name]
 if exit != 0 then
 IO.eprintln s!"[bench] ix decompile failed (exit {exit})"
 | "ooc" =>
 let ixe ← ensureIxe repo info ((p.flag? "ixe").map (·.as! String))
 let ix ← resolveBin repo "ix"
Expand DownExpand Up@@ -586,6 +606,7 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do
 -- row too.
 let expected := match backend with
 | "compile" => #[info.name]
 | "decompile" => #[info.name]
 | "ooc" => #[info.name] ++ names
 | "aiur-recursive" => (recursiveConfigs.map (·.1)).toArray
 | _ => names
Expand DownExpand Up@@ -630,7 +651,7 @@ def benchRunCmd : Cli.Cmd := `[Cli|
 "Run one benchmark cell (backend × env × mode), writing benchmark results JSON. Exits 0 on success (rows saved as the local baseline), 3 when the kernel rejected any constant, 1 when no rows were produced."

 FLAGS:
 backend : String; "aiur | zisk | sp1 | ooc | compile | aiur-recursive"
 backend : String; "aiur | zisk | sp1 | ooc | compile | decompile | aiur-recursive"
 env : String; "Benchmark env from the registry (default: InitStd)"
 mode : String; "prove | execute | recursive (default: the backend's defaultMode)"
 out : String; "Benchmark results JSON output path (default: bench.json)"
Expand Down

21 changes: 17 additions & 4 deletions
Ix/Cli/BenchPlots.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -54,6 +54,9 @@ def plotTitle (workload measure : String) : String :=
 | "ix-compile", "peak-rss" => "Ix Compile Peak RAM Usage"
 | "ix-compile", "file-size" => "Ix Environment Size"
 | "ix-compile", "constants" => "Ix Input Constants"
 | "ix-decompile", "decompile-time" => "Ix Decompile Time"
 | "ix-decompile", "throughput" => "Ix Decompile Throughput"
 | "ix-decompile", "peak-rss" => "Ix Decompile Peak RAM Usage"
 | "aiur-check-prove", "prove-time" => "Aiur Prove Time"
 | "aiur-check-prove", "throughput" => "Aiur Prove Throughput"
 | "aiur-check-prove", "peak-rss" => "Aiur Prove Peak RAM Usage"
Expand All@@ -78,10 +81,14 @@ def plotTitle (workload measure : String) : String :=
 "Aiur FFT Cost" from the prove cell). Zisk `shards` is a PR-comment
 column only ("Zisk Cycles" / max-shard-cycles carry the sharding
 trend), and zisk `constants` charts on the cross-kernel overlay below
 instead of alone. -/
 instead of alone. `ix-decompile` reuses the compile cell's `.ixe`, so
 its `file-size` / `constants` duplicate "Ix Environment Size" / "Ix
 Input Constants" exactly — the decompile cell tracks only its own
 decompile-time / throughput / peak-rss trends. -/
def plotSkips : List (String × String) :=
 [("aiur-check-prove", "execute-time"), ("aiur-check-execute", "fft-cost"),
 ("zisk-check-execute", "shards"), ("zisk-check-execute", "constants")]
 ("zisk-check-execute", "shards"), ("zisk-check-execute", "constants"),
 ("ix-decompile", "file-size"), ("ix-decompile", "constants")]

/-- Canonical units per measure slug, asserted on every sync: bencher
 auto-creates a measure with placeholder units ("Measure (units)") on
Expand All@@ -92,6 +99,7 @@ def unitsFor (slug : String) : Option String :=
 if slug.startsWith "phase-" then some "seconds (s)" else
 [("execute-peak-rss", "bytes (B)"),
 ("compile-time", "seconds (s)"),
 ("decompile-time", "seconds (s)"),
 ("execute-time", "seconds (s)"),
 ("prove-time", "seconds (s)"),
 ("verify-time", "seconds (s)"),
Expand All@@ -115,7 +123,7 @@ def unitsFor (slug : String) : Option String :=
/-- Dashboard group order (compile first, then aiur prove/execute, zisk,
 ooc); unranked workloads (a future backend) sort last. -/
def workloadOrder : List String :=
 ["ix-compile", "aiur-check-prove", "aiur-check-execute",
 ["ix-compile", "ix-decompile", "aiur-check-prove", "aiur-check-execute",
 "aiur-check-recursive", "aiur-recursive", "zisk-check-execute",
 "ooc-check"]

Expand All@@ -127,7 +135,8 @@ structure PlotSpec where
/-- One spec per bench-main testbed: its measure slugs and the benchmark
 row names uploaded there, mirroring the row emitters — compile keys
 one row per env (benched or not: the compile matrix is deliberately
 wider), ooc one whole-env row plus one full-closure row per primary,
 wider), decompile one row per benched env (a `.ixe` consumer), ooc one
 whole-env row plus one full-closure row per primary,
 the per-constant backends one row per primary. Dynamic sub-rows
 (`<name>/shard-N`) are left out: their multiplicity shifts with the
 shard manifest, and the parent row carries the headline trend. -/
Expand All@@ -142,6 +151,10 @@ def plotSpecs (rows : Array BenchCmd.VectorRow) : Array PlotSpec := Id.run do
 return (BenchCmd.envSpecs.map (·.name)).toArray
 if b.name == "aiur-recursive" then
 return (BenchCmd.recursiveConfigs.map (·.1)).toArray
 -- decompile is env-keyed like compile but a `.ixe` consumer: one row
 -- per benched env (it runs only where a benched `.ixe` exists).
 if b.name == "decompile" then
 return benched.toArray
 let mut ns : Array String := #[]
 for env in benched do
 if b.name == "ooc" then ns := ns.push env
Expand Down

2 changes: 1 addition & 1 deletion
Ix/Cli/BenchReport.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -43,7 +43,7 @@ def metricKind (metric : String) : String :=
 then "bytes"
 else if metric.startsWith "phase-" then "seconds"
 else if ["execute-time", "prove-time", "verify-time", "check-time",
 "compile-time"].contains metric then "seconds"
 "compile-time", "decompile-time"].contains metric then "seconds"
 else if ["fft-cost", "cycles", "steps", "max-shard-cycles",
 "throughput"].contains metric then "count"
 else if ["constants", "shards"].contains metric then "int"
Expand Down

83 changes: 83 additions & 0 deletions
Ix/Cli/DecompileCmd.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
/-
 `ix decompile <path.ixe>`: decompile a serialized `.ixe` environment back to
 Lean constants — the inverse of `ix compile`. This is the decompile
 benchmark's measured tool (env-keyed row, mirroring `ix compile --json`).

 With `--json` the run records one env-keyed results row (decompile-time,
 file-size, constants, throughput, peak-rss). A malformed decompile is a hard
 error (nonzero exit → red cell). Deeper compile→decompile roundtrip fidelity
 is gated by the canonical roundtrip checks (`ix validate` / the roundtrip
 tests), which need the original Lean env a `.ixe` can't supply — so this
 performance tool does not reproduce them.
-/
module
public import Cli
public import Ix.Common
public import Ix.TracingTexray
public import Ix.Benchmark.Results

public section

open System (FilePath)

namespace Ix.Cli.DecompileCmd

/-- Decompile a `.ixe` from disk, returning the decompiled constant
 count. A malformed decompile throws (hard error). Implemented in
 `crates/ffi/src/compile.rs::rs_decompile_env`. -/
@[extern "rs_decompile_env"]
opaque rsDecompileEnvFFI : @& String → IO Nat

def runDecompileCmd (p : Cli.Parsed) : IO UInt32 := do
 let some pathArg := p.positionalArg? "path"
 | p.printError "error: must specify <path> to a .ixe file"
 return Ix.Benchmark.Results.exitUsage
 let envPath := pathArg.as! String

 -- Window the tree-RSS sampler around the decompile, mirroring
 -- `ix compile --json` so the two rows share measurement
 -- infrastructure and peak-rss semantics.
 let benched := (p.flag? "json").isSome
 if benched then
 TracingTexray.startSampler
 TracingTexray.resetPeakTreeRss

 IO.println s!"Decompiling {envPath}"
 let start ← IO.monoMsNow
 let constants ← rsDecompileEnvFFI envPath
 let elapsed := (← IO.monoMsNow) - start
 IO.println s!"[decompile] {constants} constants in {elapsed.formatMs}"

 if let some flag := p.flag? "json" then
 let key := (p.flag? "json-name").map (·.as! String)
 |>.getD ((FilePath.mk envPath).fileStem.getD "env")
 let secs := elapsed.toFloat / 1000.0
 let tput := if elapsed > 0
 then constants.toFloat * 1000.0 / elapsed.toFloat else 0.0
 let peakRss ← TracingTexray.peakTreeRssBytes
 -- `file-size` is the INPUT `.ixe` the decompile consumed (the byte
 -- counterpart to compile's output `.ixe`).
 let size := (← (FilePath.mk envPath).metadata).byteSize.toNat
 Ix.Benchmark.Results.writeRow (flag.as! String) key "ok"
 [ ("decompile-time", Ix.Benchmark.Results.jsonRound 3 secs)
 , ("file-size", Lean.toJson size)
 , ("constants", Lean.toJson constants)
 , ("throughput", Ix.Benchmark.Results.jsonRound 2 tput)
 , ("peak-rss", Lean.toJson peakRss) ]

 return 0

end Ix.Cli.DecompileCmd

open Ix.Cli.DecompileCmd in
def decompileCmd : Cli.Cmd := `[Cli|
 decompile VIA runDecompileCmd;
 "Decompile a serialized `.ixe` env back to Lean constants (inverse of `ix compile`). Measures the decompile pass; a malformed decompile exits nonzero. Deep roundtrip fidelity is gated by `ix validate` / the roundtrip tests."

 FLAGS:
 json : String; "Write the decompile's benchmark results row (decompile-time, file-size, constants, throughput, peak-rss) to this path, merging into any existing rows object."
 "json-name" : String; "Row key for the --json row (default: the input `.ixe` file's stem)."

 ARGS:
 path : String; "Path to the serialized `.ixe` environment to decompile."
]
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 ix decompile CLI, fix Rust decompile perf and tests#490

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

 Merged

samuelburnham
merged 3 commits into

from

Jul 14, 2026
 Merged


feat: Add ix decompile CLI, fix Rust decompile perf and tests
#490
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


3 commits


Select commit
Hold shift + click to select a range
1064f84

perf: Fix ignored-test fallout from #484 and bound decompile/validate…


samuelburnham Jul 13, 2026
41a1876

feat: Add `ix decompile` and its benchmark backend


samuelburnham Jul 13, 2026
ba9a104

test: Cover Rust decompile over the serialized roundtrip


samuelburnham Jul 13, 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


82 changes: 81 additions & 1 deletion
.github/workflows/bench-main.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,7 +16,10 @@ name: Benchmark main
# 4. ooc-check — restore that `.ixe` and run the out-of-circuit Rust kernel
# (the same kernel, out-of-circuit and parallel — far faster)
# over the whole env, tracking throughput.
# 5. aiur-recursive — the aiur-recursive toy
# 5. decompile — restore that `.ixe` and decompile it back to Lean constants
# (the inverse of step 1); tracks decompile-time /
# throughput / peak-rss.
# 6. aiur-recursive — the aiur-recursive toy
# (bench-recursive-verifier):
# prove fixed tiny statements, run the in-circuit
# multi-stark verifier over each proof, then prove THAT
Expand DownExpand Up@@ -617,3 +620,80 @@ jobs:
 --threshold-measure peak-rss --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
 --threshold-lower-boundary _

 # Decompile — the inverse of compile. Restore the compile job's cached
 # `.ixe` and decompile it back to Lean constants. One env-keyed row per
 # benched env, mirroring the `compile` cell. A malformed decompile exits
 # nonzero and reddens this step; deep roundtrip fidelity is gated by the
 # canonical checks (`ix validate` / roundtrip tests), not measured here. No
 # compiler or Lean toolchain build — `ix decompile` is a Rust FFI pass over
 # the cached `.ixe`, so this reuses the staged `ix` binary like ooc-check.
 decompile:
 name: decompile-${{ matrix.bench }}
 needs: [compile, plan]
 runs-on: warp-ubuntu-latest-x64-32x
 timeout-minutes: 60
 strategy:
 fail-fast: false
 matrix:
 bench: ${{ fromJson(needs.plan.outputs.bench-envs) }}
 steps:
 - uses: actions/checkout@v6
 - uses: actions/cache/restore@v5
 with:
 path: ~/.local/bin
 key: bench-bins-${{ github.sha }}
 - run: echo "$HOME/.local/bin" >> $GITHUB_PATH
 # Provision the toolchain so `ix` finds libleanshared (no package build).
 - uses: leanprover/lean-action@v1
 with:
 auto-config: false
 build: false
 use-github-cache: false
 # (The path list must match the compile job's save exactly.)
 - uses: actions/cache/restore@v5
 with:
 path: |
 ${{ matrix.bench }}.ixe
 zkshards-${{ matrix.bench }}
 key: bench-ixe-${{ github.sha }}-${{ matrix.bench }}
 fail-on-cache-miss: true
 # A malformed decompile exits nonzero → red X here; a clean run's row
 # uploads below.
 - name: Run decompile benchmark
 run: |
 ix bench run --backend decompile --env ${{ matrix.bench }} --mode execute \
 --ixe ${{ matrix.bench }}.ixe --out bench.json
 # Upload whatever clean rows exist even when the run step reddened the
 # job — bmf drops every non-ok (rejected/oom) row.
 - name: Convert to Bencher Metric Format
 id: bmf
 if: ${{ !cancelled() }}
 run: |
 ix bench bmf --in bench.json --out bench-bmf.json
 cat bench-bmf.json
 # constants is deterministic → pinned (0/0); decompile-time / throughput
 # / peak-rss are noisy wall-clock → percentage bounds. file-size (the
 # input `.ixe`) duplicates the compile cell's, so it uploads for the
 # row's completeness but rides no threshold here.
 - uses: ./.github/actions/bencher-track
 if: ${{ !cancelled() && steps.bmf.outcome == 'success' }}
 with:
 testbed: ix-decompile-x64-32x
 workload: ix-decompile
 file: bench-bmf.json
 key: ${{ secrets.BENCHER_API_KEY }}
 github-token: ${{ secrets.GITHUB_TOKEN }}
 thresholds: |
 --threshold-measure constants --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0
 --threshold-lower-boundary 0
 --threshold-measure decompile-time --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
 --threshold-lower-boundary _
 --threshold-measure throughput --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary _
 --threshold-lower-boundary 0.10
 --threshold-measure peak-rss --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
 --threshold-lower-boundary _

12 changes: 7 additions & 5 deletions
.github/workflows/bench-pr.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
# `!benchmark` PR command: run the curated constant set (Benchmarks/Vectors.csv)
# through chosen prover backend(s) and post a main-vs-PR comparison table.
#
# !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [aiur-recursive] | all) [execute]
# !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [decompile] [aiur-recursive] | all) [execute]
# (sp1 is disabled in the registry (Ix/Cli/BenchCmd.lean) — the parser skips it
# with a note in the config summary)
# BENCH_ENVS=InitStd,Mathlib # which compiled envs (default InitStd; case-insensitive;
Expand All@@ -20,10 +20,12 @@
# Phase-1 columns `fft-cost` / `execute-time` measured en route; `zisk` /
# `sp1` / `ooc` run `execute`; `compile` runs `ix compile <env>.lean →
# <env>.ixe` (the same cell bench-main.yml uploads under testbed
# `ix-compile-*`); `aiur-recursive` runs the aiur-recursive toy
# (bench-recursive-verifier's fixed configs — env-independent, so it
# always schedules exactly one cell no matter what BENCH_ENVS says).
# The optional bare `execute` token flips `aiur` to
# `ix-compile-*`); `decompile` runs `ix decompile <env>.ixe` over the
# compile cell's fresh PR `.ixe` (testbed `ix-decompile-*`);
# `aiur-recursive` runs the aiur-recursive toy (bench-recursive-verifier's
# fixed configs — env-independent, so it always schedules exactly one cell
# no matter what BENCH_ENVS says). The optional bare `execute` token flips
# `aiur` to
# execute-only (Phase 1, skipping the prove); bench-main runs both aiur
# modes as separate cells on separate testbeds, so either kind of cell
# fetches a cached main-side baseline from bencher. (aiur's third mode,
Expand Down

8 changes: 4 additions & 4 deletions
.github/workflows/bencher-thresholds-reset.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -22,7 +22,7 @@ name: Bencher thresholds reset
# cancel by removing it before merge. Naming convention: one label per token,
# `bencher-thresholds-reset:<token>` where <token> is a workload (a backend
# testbed in Ix/Cli/BenchCmd.lean (backendSpecs) minus its runner-arch suffix:
# `ix-compile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `all` (the merge step expands an `all` label into every workload). Labeling
# requires Triage+, so PR authors from forks cannot self-queue a reset. The
# label shares the command/workflow name; the ref it moves is
Expand All@@ -44,7 +44,7 @@ on:
 # GitHub requires literal choice options, so this list stays static:
 # keep it (and the jobs' valid= lists below) in sync with the
 # backend testbeds in Ix/Cli/BenchCmd.lean (backendSpecs).
 options: [ix-compile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
 options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
 sha:
 description: "Commit to anchor to (default: HEAD)"
 required: false
Expand DownExpand Up@@ -77,7 +77,7 @@ jobs:
 # (backendSpecs) minus the runner-arch suffix. Static because this
 # job runs on a cheap runner with no built `ix`; keep in sync when
 # adding a backend.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 if [ "$EVENT" = workflow_dispatch ]; then
 # Reset the chosen workload(s) at the given commit; no PR scan.
 sha="${INPUT_SHA:-$HEAD_SHA}"
Expand DownExpand Up@@ -133,7 +133,7 @@ jobs:
 # which the merge job expands into every workload). Same static
 # list as the reset job; keep both in sync with backendSpecs in
 # Ix/Cli/BenchCmd.lean.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 accepted="$valid all"
 # Parse the workload token(s) after the command, lowercased.
 workloads=$(printf '%s' "$BODY" \
Expand Down

23 changes: 22 additions & 1 deletion
Ix/Cli/BenchCmd.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -185,6 +185,14 @@ def backendSpecs : List BackendSpec := [
 { name := "compile", defaultMode := "execute",
 testbeds := [("execute", "ix-compile-x64-32x")],
 metrics := [("execute", ["compile-time", "throughput", "peak-rss",
 "file-size", "constants"])] },
 -- The inverse of compile: decompiles the env's `.ixe` back to Lean
 -- constants (roundtrip-verified). Env-keyed like compile, but a `.ixe`
 -- CONSUMER — it reuses the compile cell's fresh `.ixe` rather than
 -- producing one.
 { name := "decompile", defaultMode := "execute",
 testbeds := [("execute", "ix-decompile-x64-32x")],
 metrics := [("execute", ["decompile-time", "throughput", "peak-rss",
 "file-size", "constants"])] }
]

Expand DownExpand Up@@ -492,6 +500,18 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do
 if exit != 0 then
 IO.eprintln s!"[bench] ix compile failed (exit {exit})"
 return 1
 | "decompile" =>
 -- The inverse of compile: consume the env's `.ixe` (the compile cell's
 -- fresh artifact) and decompile it back to Lean constants. Env-keyed row,
 -- like compile. A malformed decompile exits nonzero and reddens the cell;
 -- deep roundtrip fidelity is gated by the canonical roundtrip checks
 -- (`ix validate` / the roundtrip tests), not measured here.
 let ixe ← ensureIxe repo info ((p.flag? "ixe").map (·.as! String))
 let ix ← resolveBin repo "ix"
 let exit ← runGuarded watchdog ceilingGb ix
 #["decompile", ixe, "--json", out, "--json-name", info.name]
 if exit != 0 then
 IO.eprintln s!"[bench] ix decompile failed (exit {exit})"
 | "ooc" =>
 let ixe ← ensureIxe repo info ((p.flag? "ixe").map (·.as! String))
 let ix ← resolveBin repo "ix"
Expand DownExpand Up@@ -586,6 +606,7 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do
 -- row too.
 let expected := match backend with
 | "compile" => #[info.name]
 | "decompile" => #[info.name]
 | "ooc" => #[info.name] ++ names
 | "aiur-recursive" => (recursiveConfigs.map (·.1)).toArray
 | _ => names
Expand DownExpand Up@@ -630,7 +651,7 @@ def benchRunCmd : Cli.Cmd := `[Cli|
 "Run one benchmark cell (backend × env × mode), writing benchmark results JSON. Exits 0 on success (rows saved as the local baseline), 3 when the kernel rejected any constant, 1 when no rows were produced."

 FLAGS:
 backend : String; "aiur | zisk | sp1 | ooc | compile | aiur-recursive"
 backend : String; "aiur | zisk | sp1 | ooc | compile | decompile | aiur-recursive"
 env : String; "Benchmark env from the registry (default: InitStd)"
 mode : String; "prove | execute | recursive (default: the backend's defaultMode)"
 out : String; "Benchmark results JSON output path (default: bench.json)"
Expand Down

21 changes: 17 additions & 4 deletions
Ix/Cli/BenchPlots.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -54,6 +54,9 @@ def plotTitle (workload measure : String) : String :=
 | "ix-compile", "peak-rss" => "Ix Compile Peak RAM Usage"
 | "ix-compile", "file-size" => "Ix Environment Size"
 | "ix-compile", "constants" => "Ix Input Constants"
 | "ix-decompile", "decompile-time" => "Ix Decompile Time"
 | "ix-decompile", "throughput" => "Ix Decompile Throughput"
 | "ix-decompile", "peak-rss" => "Ix Decompile Peak RAM Usage"
 | "aiur-check-prove", "prove-time" => "Aiur Prove Time"
 | "aiur-check-prove", "throughput" => "Aiur Prove Throughput"
 | "aiur-check-prove", "peak-rss" => "Aiur Prove Peak RAM Usage"
Expand All@@ -78,10 +81,14 @@ def plotTitle (workload measure : String) : String :=
 "Aiur FFT Cost" from the prove cell). Zisk `shards` is a PR-comment
 column only ("Zisk Cycles" / max-shard-cycles carry the sharding
 trend), and zisk `constants` charts on the cross-kernel overlay below
 instead of alone. -/
 instead of alone. `ix-decompile` reuses the compile cell's `.ixe`, so
 its `file-size` / `constants` duplicate "Ix Environment Size" / "Ix
 Input Constants" exactly — the decompile cell tracks only its own
 decompile-time / throughput / peak-rss trends. -/
def plotSkips : List (String × String) :=
 [("aiur-check-prove", "execute-time"), ("aiur-check-execute", "fft-cost"),
 ("zisk-check-execute", "shards"), ("zisk-check-execute", "constants")]
 ("zisk-check-execute", "shards"), ("zisk-check-execute", "constants"),
 ("ix-decompile", "file-size"), ("ix-decompile", "constants")]

/-- Canonical units per measure slug, asserted on every sync: bencher
 auto-creates a measure with placeholder units ("Measure (units)") on
Expand All@@ -92,6 +99,7 @@ def unitsFor (slug : String) : Option String :=
 if slug.startsWith "phase-" then some "seconds (s)" else
 [("execute-peak-rss", "bytes (B)"),
 ("compile-time", "seconds (s)"),
 ("decompile-time", "seconds (s)"),
 ("execute-time", "seconds (s)"),
 ("prove-time", "seconds (s)"),
 ("verify-time", "seconds (s)"),
Expand All@@ -115,7 +123,7 @@ def unitsFor (slug : String) : Option String :=
/-- Dashboard group order (compile first, then aiur prove/execute, zisk,
 ooc); unranked workloads (a future backend) sort last. -/
def workloadOrder : List String :=
 ["ix-compile", "aiur-check-prove", "aiur-check-execute",
 ["ix-compile", "ix-decompile", "aiur-check-prove", "aiur-check-execute",
 "aiur-check-recursive", "aiur-recursive", "zisk-check-execute",
 "ooc-check"]

Expand All@@ -127,7 +135,8 @@ structure PlotSpec where
/-- One spec per bench-main testbed: its measure slugs and the benchmark
 row names uploaded there, mirroring the row emitters — compile keys
 one row per env (benched or not: the compile matrix is deliberately
 wider), ooc one whole-env row plus one full-closure row per primary,
 wider), decompile one row per benched env (a `.ixe` consumer), ooc one
 whole-env row plus one full-closure row per primary,
 the per-constant backends one row per primary. Dynamic sub-rows
 (`<name>/shard-N`) are left out: their multiplicity shifts with the
 shard manifest, and the parent row carries the headline trend. -/
Expand All@@ -142,6 +151,10 @@ def plotSpecs (rows : Array BenchCmd.VectorRow) : Array PlotSpec := Id.run do
 return (BenchCmd.envSpecs.map (·.name)).toArray
 if b.name == "aiur-recursive" then
 return (BenchCmd.recursiveConfigs.map (·.1)).toArray
 -- decompile is env-keyed like compile but a `.ixe` consumer: one row
 -- per benched env (it runs only where a benched `.ixe` exists).
 if b.name == "decompile" then
 return benched.toArray
 let mut ns : Array String := #[]
 for env in benched do
 if b.name == "ooc" then ns := ns.push env
Expand Down

2 changes: 1 addition & 1 deletion
Ix/Cli/BenchReport.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -43,7 +43,7 @@ def metricKind (metric : String) : String :=
 then "bytes"
 else if metric.startsWith "phase-" then "seconds"
 else if ["execute-time", "prove-time", "verify-time", "check-time",
 "compile-time"].contains metric then "seconds"
 "compile-time", "decompile-time"].contains metric then "seconds"
 else if ["fft-cost", "cycles", "steps", "max-shard-cycles",
 "throughput"].contains metric then "count"
 else if ["constants", "shards"].contains metric then "int"
Expand Down

83 changes: 83 additions & 0 deletions
Ix/Cli/DecompileCmd.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
/-
 `ix decompile <path.ixe>`: decompile a serialized `.ixe` environment back to
 Lean constants — the inverse of `ix compile`. This is the decompile
 benchmark's measured tool (env-keyed row, mirroring `ix compile --json`).

 With `--json` the run records one env-keyed results row (decompile-time,
 file-size, constants, throughput, peak-rss). A malformed decompile is a hard
 error (nonzero exit → red cell). Deeper compile→decompile roundtrip fidelity
 is gated by the canonical roundtrip checks (`ix validate` / the roundtrip
 tests), which need the original Lean env a `.ixe` can't supply — so this
 performance tool does not reproduce them.
-/
module
public import Cli
public import Ix.Common
public import Ix.TracingTexray
public import Ix.Benchmark.Results

public section

open System (FilePath)

namespace Ix.Cli.DecompileCmd

/-- Decompile a `.ixe` from disk, returning the decompiled constant
 count. A malformed decompile throws (hard error). Implemented in
 `crates/ffi/src/compile.rs::rs_decompile_env`. -/
@[extern "rs_decompile_env"]
opaque rsDecompileEnvFFI : @& String → IO Nat

def runDecompileCmd (p : Cli.Parsed) : IO UInt32 := do
 let some pathArg := p.positionalArg? "path"
 | p.printError "error: must specify <path> to a .ixe file"
 return Ix.Benchmark.Results.exitUsage
 let envPath := pathArg.as! String

 -- Window the tree-RSS sampler around the decompile, mirroring
 -- `ix compile --json` so the two rows share measurement
 -- infrastructure and peak-rss semantics.
 let benched := (p.flag? "json").isSome
 if benched then
 TracingTexray.startSampler
 TracingTexray.resetPeakTreeRss

 IO.println s!"Decompiling {envPath}"
 let start ← IO.monoMsNow
 let constants ← rsDecompileEnvFFI envPath
 let elapsed := (← IO.monoMsNow) - start
 IO.println s!"[decompile] {constants} constants in {elapsed.formatMs}"

 if let some flag := p.flag? "json" then
 let key := (p.flag? "json-name").map (·.as! String)
 |>.getD ((FilePath.mk envPath).fileStem.getD "env")
 let secs := elapsed.toFloat / 1000.0
 let tput := if elapsed > 0
 then constants.toFloat * 1000.0 / elapsed.toFloat else 0.0
 let peakRss ← TracingTexray.peakTreeRssBytes
 -- `file-size` is the INPUT `.ixe` the decompile consumed (the byte
 -- counterpart to compile's output `.ixe`).
 let size := (← (FilePath.mk envPath).metadata).byteSize.toNat
 Ix.Benchmark.Results.writeRow (flag.as! String) key "ok"
 [ ("decompile-time", Ix.Benchmark.Results.jsonRound 3 secs)
 , ("file-size", Lean.toJson size)
 , ("constants", Lean.toJson constants)
 , ("throughput", Ix.Benchmark.Results.jsonRound 2 tput)
 , ("peak-rss", Lean.toJson peakRss) ]

 return 0

end Ix.Cli.DecompileCmd

open Ix.Cli.DecompileCmd in
def decompileCmd : Cli.Cmd := `[Cli|
 decompile VIA runDecompileCmd;
 "Decompile a serialized `.ixe` env back to Lean constants (inverse of `ix compile`). Measures the decompile pass; a malformed decompile exits nonzero. Deep roundtrip fidelity is gated by `ix validate` / the roundtrip tests."

 FLAGS:
 json : String; "Write the decompile's benchmark results row (decompile-time, file-size, constants, throughput, peak-rss) to this path, merging into any existing rows object."
 "json-name" : String; "Row key for the --json row (default: the input `.ixe` file's stem)."

 ARGS:
 path : String; "Path to the serialized `.ixe` environment to decompile."
]
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 ix decompile CLI, fix Rust decompile perf and tests#490

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

 Merged

samuelburnham
merged 3 commits into

from

Jul 14, 2026
 Merged


feat: Add ix decompile CLI, fix Rust decompile perf and tests
#490
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


3 commits


Select commit
Hold shift + click to select a range
1064f84

perf: Fix ignored-test fallout from #484 and bound decompile/validate…


samuelburnham Jul 13, 2026
41a1876

feat: Add `ix decompile` and its benchmark backend


samuelburnham Jul 13, 2026
ba9a104

test: Cover Rust decompile over the serialized roundtrip


samuelburnham Jul 13, 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


82 changes: 81 additions & 1 deletion
.github/workflows/bench-main.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,7 +16,10 @@ name: Benchmark main
# 4. ooc-check — restore that `.ixe` and run the out-of-circuit Rust kernel
# (the same kernel, out-of-circuit and parallel — far faster)
# over the whole env, tracking throughput.
# 5. aiur-recursive — the aiur-recursive toy
# 5. decompile — restore that `.ixe` and decompile it back to Lean constants
# (the inverse of step 1); tracks decompile-time /
# throughput / peak-rss.
# 6. aiur-recursive — the aiur-recursive toy
# (bench-recursive-verifier):
# prove fixed tiny statements, run the in-circuit
# multi-stark verifier over each proof, then prove THAT
Expand DownExpand Up@@ -617,3 +620,80 @@ jobs:
 --threshold-measure peak-rss --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
 --threshold-lower-boundary _

 # Decompile — the inverse of compile. Restore the compile job's cached
 # `.ixe` and decompile it back to Lean constants. One env-keyed row per
 # benched env, mirroring the `compile` cell. A malformed decompile exits
 # nonzero and reddens this step; deep roundtrip fidelity is gated by the
 # canonical checks (`ix validate` / roundtrip tests), not measured here. No
 # compiler or Lean toolchain build — `ix decompile` is a Rust FFI pass over
 # the cached `.ixe`, so this reuses the staged `ix` binary like ooc-check.
 decompile:
 name: decompile-${{ matrix.bench }}
 needs: [compile, plan]
 runs-on: warp-ubuntu-latest-x64-32x
 timeout-minutes: 60
 strategy:
 fail-fast: false
 matrix:
 bench: ${{ fromJson(needs.plan.outputs.bench-envs) }}
 steps:
 - uses: actions/checkout@v6
 - uses: actions/cache/restore@v5
 with:
 path: ~/.local/bin
 key: bench-bins-${{ github.sha }}
 - run: echo "$HOME/.local/bin" >> $GITHUB_PATH
 # Provision the toolchain so `ix` finds libleanshared (no package build).
 - uses: leanprover/lean-action@v1
 with:
 auto-config: false
 build: false
 use-github-cache: false
 # (The path list must match the compile job's save exactly.)
 - uses: actions/cache/restore@v5
 with:
 path: |
 ${{ matrix.bench }}.ixe
 zkshards-${{ matrix.bench }}
 key: bench-ixe-${{ github.sha }}-${{ matrix.bench }}
 fail-on-cache-miss: true
 # A malformed decompile exits nonzero → red X here; a clean run's row
 # uploads below.
 - name: Run decompile benchmark
 run: |
 ix bench run --backend decompile --env ${{ matrix.bench }} --mode execute \
 --ixe ${{ matrix.bench }}.ixe --out bench.json
 # Upload whatever clean rows exist even when the run step reddened the
 # job — bmf drops every non-ok (rejected/oom) row.
 - name: Convert to Bencher Metric Format
 id: bmf
 if: ${{ !cancelled() }}
 run: |
 ix bench bmf --in bench.json --out bench-bmf.json
 cat bench-bmf.json
 # constants is deterministic → pinned (0/0); decompile-time / throughput
 # / peak-rss are noisy wall-clock → percentage bounds. file-size (the
 # input `.ixe`) duplicates the compile cell's, so it uploads for the
 # row's completeness but rides no threshold here.
 - uses: ./.github/actions/bencher-track
 if: ${{ !cancelled() && steps.bmf.outcome == 'success' }}
 with:
 testbed: ix-decompile-x64-32x
 workload: ix-decompile
 file: bench-bmf.json
 key: ${{ secrets.BENCHER_API_KEY }}
 github-token: ${{ secrets.GITHUB_TOKEN }}
 thresholds: |
 --threshold-measure constants --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0
 --threshold-lower-boundary 0
 --threshold-measure decompile-time --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
 --threshold-lower-boundary _
 --threshold-measure throughput --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary _
 --threshold-lower-boundary 0.10
 --threshold-measure peak-rss --threshold-test percentage
 --threshold-max-sample-size __WINDOW__ --threshold-upper-boundary 0.10
 --threshold-lower-boundary _

12 changes: 7 additions & 5 deletions
.github/workflows/bench-pr.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
# `!benchmark` PR command: run the curated constant set (Benchmarks/Vectors.csv)
# through chosen prover backend(s) and post a main-vs-PR comparison table.
#
# !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [aiur-recursive] | all) [execute]
# !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [decompile] [aiur-recursive] | all) [execute]
# (sp1 is disabled in the registry (Ix/Cli/BenchCmd.lean) — the parser skips it
# with a note in the config summary)
# BENCH_ENVS=InitStd,Mathlib # which compiled envs (default InitStd; case-insensitive;
Expand All@@ -20,10 +20,12 @@
# Phase-1 columns `fft-cost` / `execute-time` measured en route; `zisk` /
# `sp1` / `ooc` run `execute`; `compile` runs `ix compile <env>.lean →
# <env>.ixe` (the same cell bench-main.yml uploads under testbed
# `ix-compile-*`); `aiur-recursive` runs the aiur-recursive toy
# (bench-recursive-verifier's fixed configs — env-independent, so it
# always schedules exactly one cell no matter what BENCH_ENVS says).
# The optional bare `execute` token flips `aiur` to
# `ix-compile-*`); `decompile` runs `ix decompile <env>.ixe` over the
# compile cell's fresh PR `.ixe` (testbed `ix-decompile-*`);
# `aiur-recursive` runs the aiur-recursive toy (bench-recursive-verifier's
# fixed configs — env-independent, so it always schedules exactly one cell
# no matter what BENCH_ENVS says). The optional bare `execute` token flips
# `aiur` to
# execute-only (Phase 1, skipping the prove); bench-main runs both aiur
# modes as separate cells on separate testbeds, so either kind of cell
# fetches a cached main-side baseline from bencher. (aiur's third mode,
Expand Down

8 changes: 4 additions & 4 deletions
.github/workflows/bencher-thresholds-reset.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -22,7 +22,7 @@ name: Bencher thresholds reset
# cancel by removing it before merge. Naming convention: one label per token,
# `bencher-thresholds-reset:<token>` where <token> is a workload (a backend
# testbed in Ix/Cli/BenchCmd.lean (backendSpecs) minus its runner-arch suffix:
# `ix-compile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `all` (the merge step expands an `all` label into every workload). Labeling
# requires Triage+, so PR authors from forks cannot self-queue a reset. The
# label shares the command/workflow name; the ref it moves is
Expand All@@ -44,7 +44,7 @@ on:
 # GitHub requires literal choice options, so this list stays static:
 # keep it (and the jobs' valid= lists below) in sync with the
 # backend testbeds in Ix/Cli/BenchCmd.lean (backendSpecs).
 options: [ix-compile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
 options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
 sha:
 description: "Commit to anchor to (default: HEAD)"
 required: false
Expand DownExpand Up@@ -77,7 +77,7 @@ jobs:
 # (backendSpecs) minus the runner-arch suffix. Static because this
 # job runs on a cheap runner with no built `ix`; keep in sync when
 # adding a backend.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 if [ "$EVENT" = workflow_dispatch ]; then
 # Reset the chosen workload(s) at the given commit; no PR scan.
 sha="${INPUT_SHA:-$HEAD_SHA}"
Expand DownExpand Up@@ -133,7 +133,7 @@ jobs:
 # which the merge job expands into every workload). Same static
 # list as the reset job; keep both in sync with backendSpecs in
 # Ix/Cli/BenchCmd.lean.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 accepted="$valid all"
 # Parse the workload token(s) after the command, lowercased.
 workloads=$(printf '%s' "$BODY" \
Expand Down

23 changes: 22 additions & 1 deletion
Ix/Cli/BenchCmd.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -185,6 +185,14 @@ def backendSpecs : List BackendSpec := [
 { name := "compile", defaultMode := "execute",
 testbeds := [("execute", "ix-compile-x64-32x")],
 metrics := [("execute", ["compile-time", "throughput", "peak-rss",
 "file-size", "constants"])] },
 -- The inverse of compile: decompiles the env's `.ixe` back to Lean
 -- constants (roundtrip-verified). Env-keyed like compile, but a `.ixe`
 -- CONSUMER — it reuses the compile cell's fresh `.ixe` rather than
 -- producing one.
 { name := "decompile", defaultMode := "execute",
 testbeds := [("execute", "ix-decompile-x64-32x")],
 metrics := [("execute", ["decompile-time", "throughput", "peak-rss",
 "file-size", "constants"])] }
]

Expand DownExpand Up@@ -492,6 +500,18 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do
 if exit != 0 then
 IO.eprintln s!"[bench] ix compile failed (exit {exit})"
 return 1
 | "decompile" =>
 -- The inverse of compile: consume the env's `.ixe` (the compile cell's
 -- fresh artifact) and decompile it back to Lean constants. Env-keyed row,
 -- like compile. A malformed decompile exits nonzero and reddens the cell;
 -- deep roundtrip fidelity is gated by the canonical roundtrip checks
 -- (`ix validate` / the roundtrip tests), not measured here.
 let ixe ← ensureIxe repo info ((p.flag? "ixe").map (·.as! String))
 let ix ← resolveBin repo "ix"
 let exit ← runGuarded watchdog ceilingGb ix
 #["decompile", ixe, "--json", out, "--json-name", info.name]
 if exit != 0 then
 IO.eprintln s!"[bench] ix decompile failed (exit {exit})"
 | "ooc" =>
 let ixe ← ensureIxe repo info ((p.flag? "ixe").map (·.as! String))
 let ix ← resolveBin repo "ix"
Expand DownExpand Up@@ -586,6 +606,7 @@ def runBenchRunCmd (p : Cli.Parsed) : IO UInt32 := do
 -- row too.
 let expected := match backend with
 | "compile" => #[info.name]
 | "decompile" => #[info.name]
 | "ooc" => #[info.name] ++ names
 | "aiur-recursive" => (recursiveConfigs.map (·.1)).toArray
 | _ => names
Expand DownExpand Up@@ -630,7 +651,7 @@ def benchRunCmd : Cli.Cmd := `[Cli|
 "Run one benchmark cell (backend × env × mode), writing benchmark results JSON. Exits 0 on success (rows saved as the local baseline), 3 when the kernel rejected any constant, 1 when no rows were produced."

 FLAGS:
 backend : String; "aiur | zisk | sp1 | ooc | compile | aiur-recursive"
 backend : String; "aiur | zisk | sp1 | ooc | compile | decompile | aiur-recursive"
 env : String; "Benchmark env from the registry (default: InitStd)"
 mode : String; "prove | execute | recursive (default: the backend's defaultMode)"
 out : String; "Benchmark results JSON output path (default: bench.json)"
Expand Down

21 changes: 17 additions & 4 deletions
Ix/Cli/BenchPlots.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -54,6 +54,9 @@ def plotTitle (workload measure : String) : String :=
 | "ix-compile", "peak-rss" => "Ix Compile Peak RAM Usage"
 | "ix-compile", "file-size" => "Ix Environment Size"
 | "ix-compile", "constants" => "Ix Input Constants"
 | "ix-decompile", "decompile-time" => "Ix Decompile Time"
 | "ix-decompile", "throughput" => "Ix Decompile Throughput"
 | "ix-decompile", "peak-rss" => "Ix Decompile Peak RAM Usage"
 | "aiur-check-prove", "prove-time" => "Aiur Prove Time"
 | "aiur-check-prove", "throughput" => "Aiur Prove Throughput"
 | "aiur-check-prove", "peak-rss" => "Aiur Prove Peak RAM Usage"
Expand All@@ -78,10 +81,14 @@ def plotTitle (workload measure : String) : String :=
 "Aiur FFT Cost" from the prove cell). Zisk `shards` is a PR-comment
 column only ("Zisk Cycles" / max-shard-cycles carry the sharding
 trend), and zisk `constants` charts on the cross-kernel overlay below
 instead of alone. -/
 instead of alone. `ix-decompile` reuses the compile cell's `.ixe`, so
 its `file-size` / `constants` duplicate "Ix Environment Size" / "Ix
 Input Constants" exactly — the decompile cell tracks only its own
 decompile-time / throughput / peak-rss trends. -/
def plotSkips : List (String × String) :=
 [("aiur-check-prove", "execute-time"), ("aiur-check-execute", "fft-cost"),
 ("zisk-check-execute", "shards"), ("zisk-check-execute", "constants")]
 ("zisk-check-execute", "shards"), ("zisk-check-execute", "constants"),
 ("ix-decompile", "file-size"), ("ix-decompile", "constants")]

/-- Canonical units per measure slug, asserted on every sync: bencher
 auto-creates a measure with placeholder units ("Measure (units)") on
Expand All@@ -92,6 +99,7 @@ def unitsFor (slug : String) : Option String :=
 if slug.startsWith "phase-" then some "seconds (s)" else
 [("execute-peak-rss", "bytes (B)"),
 ("compile-time", "seconds (s)"),
 ("decompile-time", "seconds (s)"),
 ("execute-time", "seconds (s)"),
 ("prove-time", "seconds (s)"),
 ("verify-time", "seconds (s)"),
Expand All@@ -115,7 +123,7 @@ def unitsFor (slug : String) : Option String :=
/-- Dashboard group order (compile first, then aiur prove/execute, zisk,
 ooc); unranked workloads (a future backend) sort last. -/
def workloadOrder : List String :=
 ["ix-compile", "aiur-check-prove", "aiur-check-execute",
 ["ix-compile", "ix-decompile", "aiur-check-prove", "aiur-check-execute",
 "aiur-check-recursive", "aiur-recursive", "zisk-check-execute",
 "ooc-check"]

Expand All@@ -127,7 +135,8 @@ structure PlotSpec where
/-- One spec per bench-main testbed: its measure slugs and the benchmark
 row names uploaded there, mirroring the row emitters — compile keys
 one row per env (benched or not: the compile matrix is deliberately
 wider), ooc one whole-env row plus one full-closure row per primary,
 wider), decompile one row per benched env (a `.ixe` consumer), ooc one
 whole-env row plus one full-closure row per primary,
 the per-constant backends one row per primary. Dynamic sub-rows
 (`<name>/shard-N`) are left out: their multiplicity shifts with the
 shard manifest, and the parent row carries the headline trend. -/
Expand All@@ -142,6 +151,10 @@ def plotSpecs (rows : Array BenchCmd.VectorRow) : Array PlotSpec := Id.run do
 return (BenchCmd.envSpecs.map (·.name)).toArray
 if b.name == "aiur-recursive" then
 return (BenchCmd.recursiveConfigs.map (·.1)).toArray
 -- decompile is env-keyed like compile but a `.ixe` consumer: one row
 -- per benched env (it runs only where a benched `.ixe` exists).
 if b.name == "decompile" then
 return benched.toArray
 let mut ns : Array String := #[]
 for env in benched do
 if b.name == "ooc" then ns := ns.push env
Expand Down

2 changes: 1 addition & 1 deletion
Ix/Cli/BenchReport.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -43,7 +43,7 @@ def metricKind (metric : String) : String :=
 then "bytes"
 else if metric.startsWith "phase-" then "seconds"
 else if ["execute-time", "prove-time", "verify-time", "check-time",
 "compile-time"].contains metric then "seconds"
 "compile-time", "decompile-time"].contains metric then "seconds"
 else if ["fft-cost", "cycles", "steps", "max-shard-cycles",
 "throughput"].contains metric then "count"
 else if ["constants", "shards"].contains metric then "int"
Expand Down

83 changes: 83 additions & 0 deletions
Ix/Cli/DecompileCmd.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
/-
 `ix decompile <path.ixe>`: decompile a serialized `.ixe` environment back to
 Lean constants — the inverse of `ix compile`. This is the decompile
 benchmark's measured tool (env-keyed row, mirroring `ix compile --json`).

 With `--json` the run records one env-keyed results row (decompile-time,
 file-size, constants, throughput, peak-rss). A malformed decompile is a hard
 error (nonzero exit → red cell). Deeper compile→decompile roundtrip fidelity
 is gated by the canonical roundtrip checks (`ix validate` / the roundtrip
 tests), which need the original Lean env a `.ixe` can't supply — so this
 performance tool does not reproduce them.
-/
module
public import Cli
public import Ix.Common
public import Ix.TracingTexray
public import Ix.Benchmark.Results

public section

open System (FilePath)

namespace Ix.Cli.DecompileCmd

/-- Decompile a `.ixe` from disk, returning the decompiled constant
 count. A malformed decompile throws (hard error). Implemented in
 `crates/ffi/src/compile.rs::rs_decompile_env`. -/
@[extern "rs_decompile_env"]
opaque rsDecompileEnvFFI : @& String → IO Nat

def runDecompileCmd (p : Cli.Parsed) : IO UInt32 := do
 let some pathArg := p.positionalArg? "path"
 | p.printError "error: must specify <path> to a .ixe file"
 return Ix.Benchmark.Results.exitUsage
 let envPath := pathArg.as! String

 -- Window the tree-RSS sampler around the decompile, mirroring
 -- `ix compile --json` so the two rows share measurement
 -- infrastructure and peak-rss semantics.
 let benched := (p.flag? "json").isSome
 if benched then
 TracingTexray.startSampler
 TracingTexray.resetPeakTreeRss

 IO.println s!"Decompiling {envPath}"
 let start ← IO.monoMsNow
 let constants ← rsDecompileEnvFFI envPath
 let elapsed := (← IO.monoMsNow) - start
 IO.println s!"[decompile] {constants} constants in {elapsed.formatMs}"

 if let some flag := p.flag? "json" then
 let key := (p.flag? "json-name").map (·.as! String)
 |>.getD ((FilePath.mk envPath).fileStem.getD "env")
 let secs := elapsed.toFloat / 1000.0
 let tput := if elapsed > 0
 then constants.toFloat * 1000.0 / elapsed.toFloat else 0.0
 let peakRss ← TracingTexray.peakTreeRssBytes
 -- `file-size` is the INPUT `.ixe` the decompile consumed (the byte
 -- counterpart to compile's output `.ixe`).
 let size := (← (FilePath.mk envPath).metadata).byteSize.toNat
 Ix.Benchmark.Results.writeRow (flag.as! String) key "ok"
 [ ("decompile-time", Ix.Benchmark.Results.jsonRound 3 secs)
 , ("file-size", Lean.toJson size)
 , ("constants", Lean.toJson constants)
 , ("throughput", Ix.Benchmark.Results.jsonRound 2 tput)
 , ("peak-rss", Lean.toJson peakRss) ]

 return 0

end Ix.Cli.DecompileCmd

open Ix.Cli.DecompileCmd in
def decompileCmd : Cli.Cmd := `[Cli|
 decompile VIA runDecompileCmd;
 "Decompile a serialized `.ixe` env back to Lean constants (inverse of `ix compile`). Measures the decompile pass; a malformed decompile exits nonzero. Deep roundtrip fidelity is gated by `ix validate` / the roundtrip tests."

 FLAGS:
 json : String; "Write the decompile's benchmark results row (decompile-time, file-size, constants, throughput, peak-rss) to this path, merging into any existing rows object."
 "json-name" : String; "Row key for the --json row (default: the input `.ixe` file's stem)."

 ARGS:
 path : String; "Path to the serialized `.ixe` environment to decompile."
]
Loading