Skip to content

Commit 61cb1bd

Browse files
samuelburnhamsamuelburnham
committed
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 7478fff commit 61cb1bd

25 files changed

Lines changed: 1539 additions & 1202 deletions

‎.github/workflows/ci.yml‎

Lines changed: 0 additions & 81 deletions
Original file line numberDiff line numberDiff line change
@@ -28,15 +28,6 @@ jobs:
2828
run: lake test -- --ignored aiur aiur-hashes ixvm multi-stark recursive-verifier
2929
- name: Check Lean versions match for Ix and compiler bench
3030
run: diff lean-toolchain Benchmarks/Compile/lean-toolchain
31-
# Compile a tiny env once (ix is already built here) and hand it to the
32-
# zkVM execute job via artifact, so that job stays Lean-free.
33-
- name: Compile zkVM test fixture (minimal.ixe)
34-
run: lake exe ix compile Tests/MinimalDefs.lean --out minimal.ixe
35-
- uses: actions/upload-artifact@v4
36-
with:
37-
name: minimal-ixe
38-
path: minimal.ixe
39-
if-no-files-found: error
4031

4132
rust-test:
4233
runs-on: ubuntu-latest
@@ -64,75 +55,3 @@ jobs:
6455
uses: EmbarkStudios/cargo-deny-action@v2
6556
with:
6657
rust-version: ${{ env.RUST_VERSION }}
67-
68-
# Execute the kernel typecheck of the `minimal.ixe` fixture in the SP1 and
69-
# Zisk VMs natively (no Nix): install the toolchains via sp1up / ziskup
70-
# (prebuilt binaries), build the hosts, and run `--execute` (no proof, no
71-
# GPU). The precompile-aware SP1 runner-binary is auto-built from the fork
72-
# git dep by `sp1-core-executor-runner`'s build script — no manual override
73-
# needed. Each host bails non-zero on any typecheck failure; we also assert
74-
# the `failures: 0` line and exercise the `--only-const` closure-sub-env path
75-
# (a constant present in the fixture) on both backends.
76-
riscv-zkvm-execute:
77-
name: RISC-V zkVM Execute
78-
needs: lean-test
79-
runs-on: warp-ubuntu-latest-x64-16x
80-
steps:
81-
- uses: actions/checkout@v6
82-
- uses: actions-rust-lang/setup-rust-toolchain@v1
83-
with:
84-
cache-workspaces: |
85-
sp1
86-
zisk
87-
# System deps for the zkVM backends. The first block is the ZisK book's
88-
# full Ubuntu list (its prebuilt cargo-zisk and proofman's C++ link these:
89-
# OpenMPI, OpenMP, GMP, nlohmann-json, nasm, secp256k1, …); pkg-config +
90-
# libssl-dev are for SP1's host crates (openssl/bindgen). The Nix shells
91-
# provided all this; a bare runner doesn't. Must precede the ziskup
92-
# install, which runs cargo-zisk to set up the toolchain.
93-
- name: Install system build deps
94-
run: |
95-
sudo apt-get update
96-
sudo apt-get install -y \
97-
xz-utils jq curl build-essential qemu-system libomp-dev libgmp-dev \
98-
nlohmann-json3-dev protobuf-compiler uuid-dev libgrpc++-dev \
99-
libsecp256k1-dev libsodium-dev libpqxx-dev nasm libopenmpi-dev \
100-
openmpi-bin openmpi-common libclang-dev clang gcc-riscv64-unknown-elf \
101-
pkg-config libssl-dev
102-
- uses: actions/download-artifact@v4
103-
with:
104-
name: minimal-ixe
105-
- name: Install SP1 toolchain (sp1up, latest)
106-
run: |
107-
curl -L https://sp1up.succinct.xyz | bash
108-
~/.sp1/bin/sp1up
109-
echo "$HOME/.sp1/bin" >> "$GITHUB_PATH"
110-
- name: Install Zisk toolchain (ziskup, latest)
111-
# `--cpu` picks the CPU build (no GPU on the runner) and `--nokey` skips
112-
# the proving/verify keys — together they avoid ziskup's interactive
113-
# /dev/tty prompts, and execute needs no keys. `--prefix $HOME/.zisk`
114-
# pins the install where cargo-zisk's ZiskPaths fallback looks (the
115-
# runner sets XDG_CONFIG_HOME, which would otherwise relocate it).
116-
run: |
117-
curl -L https://raw.githubusercontent.com/0xPolygonHermez/zisk/main/ziskup/install.sh \
118-
| bash -s -- --cpu --nokey -y --prefix "$HOME/.zisk"
119-
echo "$HOME/.zisk/bin" >> "$GITHUB_PATH"
120-
# `download-artifact` drops minimal.ixe in the repo root; both hosts run
121-
# from their workspace dir, so the env is `../minimal.ixe`. Debug builds
122-
# (no `--release`) keep host compile time down. minimal.ixe carries the
123-
# full Init closure (the three MinimalDefs constants plus everything the
124-
# implicit prelude import pulls in), so we scope execution with
125-
# `--only-const myReflEq`: that typechecks just the one constant and
126-
# leaves its Init dependencies as Claim assumptions, instead of
127-
# typechecking all of Init (which never finishes in the emulator).
128-
- name: SP1 — execute minimal.ixe (assert failures == 0)
129-
run: |
130-
cd sp1
131-
cargo run --bin sp1-host -- --execute --ixe ../minimal.ixe --only-const myReflEq | tee only.txt
132-
grep -qE "failures: 0\b" only.txt
133-
- name: Zisk — execute minimal.ixe (assert failures == 0)
134-
run: |
135-
cd zisk
136-
ulimit -l unlimited 2>/dev/null || true
137-
cargo run --bin zisk-host -- --execute --ixe ../minimal.ixe --only-const myReflEq | tee only.txt
138-
grep -qE "failures: 0\b" only.txt

‎.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

0 commit comments

Comments
 (0)