Skip to content

Commit c88df18

Browse files
samuelburnhamsamuelburnham
authored
feat: Add SP1 and Zisk kernel proving backends (#411)
* feat: Cargo workspace + SP1/Zisk proving backends Convert the crate to a Cargo workspace with subcrates and add the SP1 and Zisk kernel proving backends. Make aiur::vk_codec::aiur_system_to_bytes public so the FFI layer (crates/ffi/src/aiur/protocol.rs) can serialize the verifying key. * feat: manifest-driven sharding and bisection-tree aggregation Port the kernel-sharding profiler and partitioner into the workspace and build the proving pipeline on top of it: - manifest-driven sharding for the Zisk host (drops --topo/stats scaffolding) - budget-driven shard count from a per-shard cycle cap, recalibrated cycles-per-heartbeat (208k->215k), and auto-sizing from machine RAM - emit the bisection tree and carry it in the .ixes manifest - tree-aligned aggregation with in-circuit assumption discharge - cross-run proof reuse on the shard-plan path (drops the legacy reuse path) - store-aware planning: partition only novel work, resolve the rest by reuse * fix: kernel proving fixes, formatting, and cleanup - add NatSuccMode::Stuck cache to prove ByteArray.utf8DecodeChar?_utf8EncodeChar_append - cargo fmt and clippy fixes in the shard examples * chore: SP1 blake3 fork, CI, and cleanup - publish the blake3 precompile fork, fix the SP1 guest build, and document proving - add CI * fix: clippy in vk_codec, document Zisk sharding, scope CI execute - vk_codec: drop the always-Ok `Result` wrapper from `to_bytes` (clippy `unnecessary_wraps`); callers updated. - README: document the Zisk shard-proving path — profile → shard → prove via `--shard-plan`, and the resumable proof store (`--store-dir`/`--no-reuse`/`--require-closed`). - ci: scope the riscv-zkvm-execute job to `--only-const myReflEq` so it certifies one constant (Init deps become Claim assumptions) instead of typechecking all of Init, which never finished. * feat: out-of-circuit profiler + bin-packing shard planner `ix profile`: record every kernel-work counter on each run (heartbeats, subst-node visits, whnf/def-eq calls, nat-arith limb-work) plus the delta-unfold graph into a `.ixprof` sidecar, and print a cargo-zisk-style cost breakdown with a predicted Zisk leaf cycles/RAM estimate. Counter instrumentation lives in subst/def_eq/tc/whnf; the model coefficients are defined once in `shard.rs` and shared with the planner. `ix shard`: ingest the `.ixprof` and partition with no kernel re-run. The default cap path bin-packs to a per-shard cycle (hence prover-RAM) cap instead of balancing into a fixed count — the fewest shards that each stay under the cap, each packed as full as the dependency structure allows. A fine min-cut pre-partition supplies a cut-coherent block order so dependency overlap packs into the same shard (paid once, not re-ingressed per shard); the cap test counts that cross-ingress exactly. `--shards N` keeps balanced min-cut bisection for manual control; `--max-ram` defaults to detected system RAM at RAM_USABLE_FRAC headroom. `ix shard` also reports total shards, total predicted cycles, and a prove-time estimate from the measured leaf model (54 s + 158 s·Bsteps per shard). `--parallelism N` divides the wall-clock for an N-prover setup; sharded proving is sequential today, so the default is 1. Default sidecar names mirror the env base name: `init.ixe` → `init.ixprof` → `init.ixes`. Remove the kernel example binaries: all functionality is reachable via the `ix profile`/`ix shard` CLI or the public `shard.rs` functions, so the examples (and their `env_logger` dev-dep) are dropped. Also folds in the in-progress SP1/Zisk host `--constant`/`--skip-deps` flag unification and the Zisk cycle cost-model doc. The ~10-min zkVM execute CI moves out of the per-PR path into a push-to-main `riscv-bench.yml` (fixture compile + SP1/Zisk execute), using the matching `--constant --skip-deps`.
1 parent 0f8eef5 commit c88df18

181 files changed

Lines changed: 26370 additions & 2513 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/riscv-bench.yml‎

Lines changed: 124 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,124 @@
1+
name: RISC-V bench
2+
3+
# zkVM execute is ~10+ min (toolchain installs + host builds + emulation), so it
4+
# is kept off the per-PR path: this workflow runs only on pushes to main (and on
5+
# manual dispatch). It compiles the `minimal.ixe` fixture, then executes the
6+
# kernel typecheck of one constant in the SP1 and Zisk VMs — in parallel jobs.
7+
on:
8+
push:
9+
branches: main
10+
workflow_dispatch:
11+
12+
permissions:
13+
contents: read
14+
15+
concurrency:
16+
group: ${{ github.workflow }}-${{ github.ref }}
17+
cancel-in-progress: true
18+
19+
jobs:
20+
# Compile a tiny env once (ix is already built here) and hand it to the zkVM
21+
# execute jobs via artifact, so those jobs stay Lean-free.
22+
compile-fixture:
23+
name: Compile zkVM fixture (minimal.ixe)
24+
runs-on: warp-ubuntu-latest-x64-16x
25+
steps:
26+
- uses: actions/checkout@v6
27+
- uses: actions-rust-lang/setup-rust-toolchain@v1
28+
- uses: leanprover/lean-action@v1
29+
with:
30+
build-args: "--wfail -v"
31+
- name: Compile zkVM test fixture (minimal.ixe)
32+
run: lake exe ix compile Tests/MinimalDefs.lean --out minimal.ixe
33+
- uses: actions/upload-artifact@v4
34+
with:
35+
name: minimal-ixe
36+
path: minimal.ixe
37+
if-no-files-found: error
38+
39+
# Execute the kernel typecheck of the `minimal.ixe` fixture natively (no Nix,
40+
# no proof, no GPU). SP1 and Zisk run as independent jobs so they parallelize;
41+
# each installs only its own toolchain via sp1up / ziskup (prebuilt binaries)
42+
# and downloads the shared fixture. minimal.ixe carries the full Init closure,
43+
# so we scope execution with `--constant myReflEq --skip-deps`: that
44+
# subject-only-typechecks just the named constant, trusting its Init
45+
# dependencies as Claim assumptions, instead of typechecking all of Init (which
46+
# never finishes in the emulator). Each host bails non-zero on any typecheck
47+
# failure; we also assert the `failures: 0` line.
48+
#
49+
# The apt list is the shared superset both backends need: the ZisK book's full
50+
# Ubuntu list (its prebuilt cargo-zisk and proofman's C++ link OpenMPI, OpenMP,
51+
# GMP, nlohmann-json, nasm, secp256k1, …) plus pkg-config + libssl-dev for
52+
# SP1's host crates (openssl/bindgen). The Nix shells provided all this; a bare
53+
# runner doesn't. Must precede the toolchain install (it runs cargo-zisk).
54+
sp1-execute:
55+
name: SP1 zkVM Execute
56+
needs: compile-fixture
57+
runs-on: warp-ubuntu-latest-x64-16x
58+
steps:
59+
- uses: actions/checkout@v6
60+
- uses: actions-rust-lang/setup-rust-toolchain@v1
61+
with:
62+
cache-workspaces: sp1
63+
- name: Install system build deps
64+
run: |
65+
sudo apt-get update
66+
sudo apt-get install -y \
67+
xz-utils jq curl build-essential qemu-system libomp-dev libgmp-dev \
68+
nlohmann-json3-dev protobuf-compiler uuid-dev libgrpc++-dev \
69+
libsecp256k1-dev libsodium-dev libpqxx-dev nasm libopenmpi-dev \
70+
openmpi-bin openmpi-common libclang-dev clang gcc-riscv64-unknown-elf \
71+
pkg-config libssl-dev
72+
- uses: actions/download-artifact@v4
73+
with:
74+
name: minimal-ixe
75+
- name: Install SP1 toolchain (sp1up, latest)
76+
run: |
77+
curl -L https://sp1up.succinct.xyz | bash
78+
~/.sp1/bin/sp1up
79+
echo "$HOME/.sp1/bin" >> "$GITHUB_PATH"
80+
# The precompile-aware SP1 runner-binary is auto-built from the fork git
81+
# dep by `sp1-core-executor-runner`'s build script — no manual override.
82+
- name: SP1 — execute minimal.ixe (assert failures == 0)
83+
run: |
84+
cd sp1
85+
cargo run --bin sp1-host -- --execute --ixe ../minimal.ixe --constant myReflEq --skip-deps | tee only.txt
86+
grep -qE "failures: 0\b" only.txt
87+
88+
zisk-execute:
89+
name: Zisk zkVM Execute
90+
needs: compile-fixture
91+
runs-on: warp-ubuntu-latest-x64-16x
92+
steps:
93+
- uses: actions/checkout@v6
94+
- uses: actions-rust-lang/setup-rust-toolchain@v1
95+
with:
96+
cache-workspaces: zisk
97+
- name: Install system build deps
98+
run: |
99+
sudo apt-get update
100+
sudo apt-get install -y \
101+
xz-utils jq curl build-essential qemu-system libomp-dev libgmp-dev \
102+
nlohmann-json3-dev protobuf-compiler uuid-dev libgrpc++-dev \
103+
libsecp256k1-dev libsodium-dev libpqxx-dev nasm libopenmpi-dev \
104+
openmpi-bin openmpi-common libclang-dev clang gcc-riscv64-unknown-elf \
105+
pkg-config libssl-dev
106+
- uses: actions/download-artifact@v4
107+
with:
108+
name: minimal-ixe
109+
- name: Install Zisk toolchain (ziskup, latest)
110+
# `--cpu` picks the CPU build (no GPU on the runner) and `--nokey` skips
111+
# the proving/verify keys — together they avoid ziskup's interactive
112+
# /dev/tty prompts, and execute needs no keys. `--prefix $HOME/.zisk`
113+
# pins the install where cargo-zisk's ZiskPaths fallback looks (the
114+
# runner sets XDG_CONFIG_HOME, which would otherwise relocate it).
115+
run: |
116+
curl -L https://raw.githubusercontent.com/0xPolygonHermez/zisk/main/ziskup/install.sh \
117+
| bash -s -- --cpu --nokey -y --prefix "$HOME/.zisk"
118+
echo "$HOME/.zisk/bin" >> "$GITHUB_PATH"
119+
- name: Zisk — execute minimal.ixe (assert failures == 0)
120+
run: |
121+
cd zisk
122+
ulimit -l unlimited 2>/dev/null || true
123+
cargo run --bin zisk-host -- --execute --ixe ../minimal.ixe --constant myReflEq --skip-deps | tee only.txt
124+
grep -qE "failures: 0\b" only.txt

‎.gitignore‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
**/.lake
33

44
# Rust
5-
/target
5+
**/target
66

77
# Nix
88
result*

‎Benchmarks/Compile/CompileInit.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
import Init

‎Benchmarks/Compile/README.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ Test libraries for the Ix compiler
1010

1111
First ensure the Lean version used to build Ix matches the `Benchmarks/Compile/lean-toolchain` version (check against `ix --version`). Then run
1212

13-
`ix compile --path /path/to/Compile<Lib>.lean` # replace `<Lib>` with `InitStd`, `Lean`, `Mathlib`, or `FLT`
13+
`ix compile /path/to/Compile<Lib>.lean` # replace `<Lib>` with `Init`, `InitStd`, `Lean`, `Mathlib`, or `FLT`
1414

1515
> [!NOTE]
1616
> Compiling Mathlib and FLT currently requires a multi-core CPU and >64 GB RAM.

‎Benchmarks/Compile/lakefile.toml‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,9 @@ name = "Compile"
22
version = "0.1.0"
33
defaultTargets = ["CompileInitStd"]
44

5+
[[lean_lib]]
6+
name = "CompileInit"
7+
58
[[lean_lib]]
69
name = "CompileInitStd"
710

‎Benchmarks/CompileFC/README.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,4 +16,4 @@ This project shadows the `formal-conjectures` project's Lean version, which is n
1616

1717
First ensure the Lean version used to build Ix matches the `Benchmarks/CompileFC/lean-toolchain` version (check against `ix --version`). Then run
1818

19-
`ix compile --path /path/to/CompileFC.lean`
19+
`ix compile /path/to/CompileFC.lean`

‎Cargo.lock‎

Lines changed: 106 additions & 27 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

0 commit comments

Comments
 (0)