IxVM: native execution pipeline by arthurpaulino · Pull Request #463 · argumentcomputer/ix

arthurpaulino · 2026-07-01T11:19:05Z

Codegen the IxVM Aiur kernel to Rust, run witness/prove Rust-side against a Rust-owned env, and wire the fast path through every ix check / ix prove entry point.

Wall time on shard 26 of the 64-way init.ixes partition: 1029 s → 62 s (~16× end-to-end).

What's here

Eight commits, roughly grouped:

Codegen kernel

Aiur Bytecode → Rust codegen pass. Walks the compiled IxVM Bytecode.Toplevel and emits one fn aiur_fn_N(...) per Aiur function into crates/ix/src/aiur_ixvm.rs (~4.8 MB, 743 fns). Same QueryRecord shape as the interpreter — proof-verification compatible.
Value-returning byte ops in the codegen output. Eliminates the Vec<G> scratch buffer per byte op (~245 sites) via per-op helpers (bytes2_xor_value, bytes2_add_value, etc.) that bump the byte-chip queries and return the gadget output directly. Also dead-folds unconstrained || false / !unconstrained && !false and uses an unchecked array copy on Call cache hits.

Rust-owned witness + env

Port IxVM.ClaimHarness.buildShardCheckEnvWitness to Rust. Parallel closure walk (rayon + DashSet) + parallel byte→G conversion. Eliminates the per-byte boxing into Aiur.G that dominated per-shard wall time.
Wire the Rust witness fast path through per-claim check/prove and both benchmarks. Adds FFIs for check_addr / prove_addr / shard_prove, plus bytes-blob variants for the compiled-Lean-env code path.
EnvHandle: Rust-owned ixon::Env exposed to Lean as an opaque handle. Collapses six per-call FFIs into four *_with_env FFIs + two constructors (fromIxe / fromBytes). The env is parsed exactly once per CLI invocation; every per-target FFI call reuses the same handle. Prove FFIs return claim_bytes so Lean deserializes the wire claim instead of recomputing it.

CI + ergonomics

ix codegen --check. CI-facing flag that compares the emitted Rust source against the on-disk file and exits 1 on drift. Wired into lean-test. Warm ~2 s.
ix check --interp {source|bytecode}. Single flag with two modes. bytecode bypasses the codegen kernel via the generic Aiur bytecode interpreter — no ix codegen + cargo build cycle when iterating on Ix/IxVM/*.lean. source reaches the Aiur source interpreter for its richer per-step diagnostics.

Coverage

Every ix check / ix prove shape now routes through the native pipeline:

Command	Path
`ix check NAME --ixe`	`checkAddrWithEnv` (codegen kernel)
`ix check NAME` (no `--ixe`)	`checkAddrWithEnv` + `EnvHandle.fromBytes`
`ix check --claim hex --ixe`	`checkAddrWithEnv` for `check addr none`
`ix check --ixes --shard K`	`shardCheckWithEnv`
`ix check --ixes`	`shardCheckWithEnv` × all shards, shared env
`ix prove NAME --ixe`	`proveAddrWithEnv`
`ix prove --ixes --shard K`	`shardProveWithEnv`
`ix prove --ixes`	`shardProveWithEnv` × all shards
`Benchmarks/Typecheck` Phase 1 + 2	shared `EnvHandle` across execute + prove

Fallbacks:

--interp source — Aiur source interpreter (richer errors). Target.leanW materialised Lean-side.
--interp bytecode — generic bytecode interpreter, skips codegen/rebuild cycle.
--claim <hex> for non-check addr none variants (eval / reveal / contains / checkEnv-with-asm) — Lean witness builder.

FFI surface

Six new FFIs replace the ten single-use ones deleted along the way:

// Constructorsrs_aiur_env_handle_from_ixe(path) -> LeanExternal<EnvHandle>
rs_aiur_env_handle_from_bytes(bytes) -> LeanExternal<EnvHandle>
// Check (returns output + ioBuffer + queryCounts)rs_aiur_toplevel_check_addr_with_env(toplevel, fun_idx, handle, addr_bytes, use_bytecode)
rs_aiur_toplevel_shard_check_with_env (toplevel, fun_idx, handle, owned_blob, use_bytecode)// Prove (returns claim_bytes + proof + ioBuffer)
rs_aiur_system_prove_addr_with_env (system, fri, fun_idx, handle, addr_bytes)
rs_aiur_system_shard_prove_with_env (system, fri, fun_idx, handle, owned_blob)

Measurements

Shard 26 of the 64-way init.ixes partition (blake3 / defeq / Nat-heavy):

Variant	Wall	Speedup
Baseline (Lean witness + bytecode interp)	1029 s	1.0×
Lean witness + codegen kernel	1015 s	1.01×
Rust witness (serial) + codegen kernel	101 s	10 ×
Rust witness (parallel) + codegen kernel	80 s	12.9×
+ value-helper byte ops	64 s	16.1×
+ `EnvHandle` (env parsed once)	62 s	16.6×

FFT cost 107_006_963_281 on every variant — bit-identical QueryRecord traces across all backends.

Sanity across three entry points (warm):

Command	Wall	FFT (G)
`ix check Nat.add_comm` (compiled env, `EnvHandle.fromBytes`)	2.4 s	23_603_449
`ix check --ixe init.ixe Nat.add_comm`	3.1 s	23_603_449
`ix check Std.Time.Week.Offset.ofMilliseconds` (codegen)	9.3 s	12_430_516_949
`ix check --interp bytecode Std.Time.Week.Offset.ofMilliseconds`	14.6 s	12_430_516_949
`ix check --interp source Eq`	6.3 s	(`Eq: ()`)

New crate

crates/ix/ (ix) — IxVM-specific glue. Depends on aiur, common, ixon.

aiur_ixvm.rs — codegen'd kernel (regenerated by ix codegen).
aiur_ixvm_runner.rs — thin execute_ixvm wrapper that routes through execute_generated.
aiur_ixvm_witness.rs — Rust witness builders (build_claim_check_witness, build_shard_check_env_witness) with parallel closure walk + byte-to-G conversion.
env_handle.rs — EnvHandle wrapping ixon::Env with anon_hints populated.

CI

lean-test now runs lake exe ix codegen --check (exits 1 if crates/ix/src/aiur_ixvm.rs doesn't match what the emitter would produce). Prevents merging stale generated kernels that drift from the Bytecode → Rust pass.

Notes for reviewers

crates/ix/src/aiur_ixvm.rs is generated. Ignore the diff; regeneration is deterministic and CI-gated.
The --interp source path still requires a Lean-side ClaimWitness. forEachClaim takes a forceLeanWitness : Bool and materialises one via mkWitness when the source interpreter is selected.
EnvHandle keeps the mmap alive across per-target calls: Env::get_anon_mmap returns per-constant Arc<Mmap> windows, and the handle owns the Env; Lean's reference-counted LeanExternal<EnvHandle> drives the drop.
The prove-path executor is injected as a closure from ffi into aiur::AiurSystem::prove_ixvm so aiur doesn't need to depend on ix (which depends on aiur).

Adds a new Aiur pipeline stage that translates `Bytecode.Toplevel` into a Rust source module, one `fn aiur_fn_N` per Aiur function. The generated code mirrors `src/aiur/execute.rs`'s QueryRecord side effects exactly: same `function_queries.insert` timing, same cache-hit multiplicity bumps, same memory-queries insertion order, same `bytes{1,2}_queries` updates, same IO sequencing. Per-witness trace hashes match the interpreter byte-for-byte on every const tested (`Nat.add_comm`, `Vector.append`, `Std.Time.Week.Offset.ofMilliseconds`). * `Ix/Aiur/Stages/Codegen.lean`: structured Rust IR (`RustExpr` / `RustStmt` / `RustItem` / `MatchArm` / labeled blocks) plus a formatter. Codegen is a structural walk over the Bytecode AST, no string templating. `EmitM = StateM EmitState` threads `(nextVal, nextLabel)` so per-ValIdx Rust locals and per-MC labels are fresh. * Aiur's `map: Vec<G>` is gone in the generated kernel: every ValIdx becomes a Rust local `__v_{i}: G`. Match-arm bodies snapshot `nextVal` on entry so per-arm allocations don't leak to siblings. `MatchContinue` / `Yield` use labeled-block + `break 'label [G; OUT_SIZE]` to bubble yielded values out and rebind them at outer scope. * Deep Aiur recursion uses `stacker::maybe_grow(64 KiB, 4 MiB, …)` at the top of every generated fn, so the native call stack grows on demand rather than pre-reserving a giant thread stack. Verified against shard 24 of the 64-way `init.ixes` partition, which SEGFAULTs without it. * `ix codegen`: new CLI command. Compiles the IxVM Aiur source, walks the bytecode, writes the generated Rust to a fixed path (`src/ix/aiur_ixvm.rs`). The output path is hard-coded; no override. * `src/ix/aiur_ixvm.rs`: the generated kernel, 743 `aiur_fn_*` + `execute_generated` dispatch. Auto-regenerated; do not edit. `#![cfg_attr(rustfmt, rustfmt::skip)]` + a broad `#![allow(unused_*, non_snake_case, clippy::all)]` since the layout is for the compiler, not humans. * `src/ix/aiur_ixvm_runner.rs`: `execute_ixvm(toplevel, fun_idx, args, io_buffer) -> Result<(QueryRecord, Vec<G>), ExecError>`. Same return shape as `Toplevel::execute`, but routes through `execute_generated`. * `src/aiur/synthesis.rs`: `AiurSystem::prove_ixvm(...)` — same shape as `prove`, but the execute step calls `execute_ixvm`. Verification-compatible (proofs from one path verify under the other). * `src/aiur/execute.rs`: helpers exposed for the codegen'd kernel (`bytes{1,2}_execute` → `pub(crate)`, `unconstrained_big_uint_div_mod_helper` extracted, `CodegenBytes{1,2}{Op,}` aliases re-exported, `QueryRecord::new` → `pub(crate)`, `ExecError::InvalidFunIdx` added). * `src/ffi/aiur/protocol.rs`: two new FFI exports — `rs_aiur_toplevel_execute_ixvm` and `rs_aiur_system_prove_ixvm`. Same wire format as the existing `_execute` / `prove` exports. * `Ix/Aiur/Semantics/BytecodeFfi.lean`: `Bytecode.Toplevel.executeIxVM` — mirror of `execute`. * `Ix/Aiur/Protocol.lean`: `AiurSystem.proveIxVM`. * `Ix/Cli/CheckCmd.lean`: `runCompiled` now dispatches through `executeIxVM`. The Rust bytecode interpreter is no longer reachable from `ix check` (the Lean-side `--interp` fallback stays for richer error diagnostics). * `Ix/Cli/ProveCmd.lean`: `proveOne` uses `proveIxVM`. * `Cargo.toml`: `stacker = "0.1"`. For witnesses where execute is the dominant work (single-const checks via `ix check 'X'`), the codegen'd kernel is ~1.6× faster than the bytecode interpreter end-to-end (measured on `Nat.add_comm`, `Vector.append`, `Std.Time.Week.Offset.ofMilliseconds`). Tiny consts are within ~10% (stacker probe overhead amortises). Peak RSS is within a few MB of the interpreter — stacker grows the stack on demand, no giant upfront reservation. For shard-driven `ix check --shard K` runs the speedup is invisible: per-shard wall time is dominated (~92%) by `buildShardCheckEnvWitness` in Lean, NOT by the kernel execute (~8%). Cutting witness construction is the next lever. `Nat.add_comm` proof produced via `proveIxVM` verifies under the existing `AiurSystem::verify`. End-to-end: lake exe ix prove 'Nat.add_comm' → proof addr 0d0ab0f9… lake exe ix verify 0d0ab0f9… → ok

Replaces `IxVM.ClaimHarness.buildShardCheckEnvWitness` (Lean side, ~92% of shard wall time on heavy partitions) with a Rust port that builds the `aiur::execute::IOBuffer` directly, without per-byte boxing into Lean `Aiur.G` values. The two hot phases run on rayon: * Closure walk: each owned addr's transitive `Constant.refs` + projection-block traversal runs on its own thread; results are deduped through a `dashmap::DashSet`. * Byte-to-G conversion: per-const `(key, data)` tuples are built in parallel chunks of 256; final IOBuffer assembly (channel arena append + key→`IOKeyInfo` map insert) runs serially because the arena index is monotonic. * `src/ix/aiur_ixvm_witness.rs` (new): `build_shard_check_env_witness` produces `(claim, claim_digest_input, io_buffer)` ready to feed to `execute_ixvm`. Mirrors the 6-channel layout documented in `Ix/IxVM/ClaimHarness.lean` (claim / asm tree / const bytes / Defn hint / blob discriminator / blob raw bytes). * `src/ffi/aiur/protocol.rs`: new FFI `rs_aiur_toplevel_shard_check_ixvm` bundles witness build + `execute_ixvm` into one cross-language trip. Returns the same `(output, ioBuffer, queryCounts)` shape as `rs_aiur_toplevel_execute_ixvm`, so the Lean shim stays drop-in compatible. * `Ix/Aiur/Semantics/BytecodeFfi.lean`: `Bytecode.Toplevel.shardCheckIxVM` wraps the FFI. * `Ix/Cli/CheckCmd.lean`: shard-mode `ix check` (`--ixe + --ixes`) now dispatches through `runShardOwnedNative` → `shardCheckIxVM`, bypassing the Lean witness builder. Single- shard and whole-partition paths share the fast route; the legacy `runShardCheckManifest` / `runShardCheckAll` callbacks stay live for `--interp` only. Shard 26 of the 64-way `init.ixes` partition, on the same host: | Variant | total | speedup | | --- | --: | --: | | Lean witness + bytecode-interp (baseline)| 1029 s | 1.0× | | Lean witness + codegen kernel | 1015 s | 1.01× | | Rust witness (serial) + codegen | 101 s | 9.95× | | Rust witness (parallel) + codegen | 80 s | 12.9× | The serial Rust witness collapses the 935 s of Lean per-byte boxing into ~23 s; rayon hides that 23 s under the codegen-kernel execute (~78 s) so witness build effectively becomes free at the shard level. FFT cost matches the bytecode interpreter exactly (107_006_963_281), so the QueryRecord layout is bit-identical across all four variants. * Closure walk uses single-source BFS with the global visited set shared via `DashSet::contains` checks before pushing to the per-thread stack — avoids redundant work without a per-owned union step. * Per-channel ordering: each chunk's partial `ChannelEntries` feeds the serial fold in iteration order, so channel arena contents match the Lean side's exactly. Test still relies on trace-hash parity from the earlier codegen commit, which exercised the same path through the bytecode interpreter and the codegen kernel. * Coverage check is currently skipped on the IxVM-native whole-partition path (`runShardManifestAllNative`); legacy `runShardCheckAll` still does it for `--interp`. Re-enable separately if needed.

plumbing, unchecked cache-hit array copy Three targeted cuts to the generated kernel (`src/ix/aiur_ixvm.rs`); all preserve QueryRecord parity (shard 26 FFT cost unchanged at 107_006_963_281). Every `U8*` op previously emitted a `Vec<G>` scratch (~245 sites): let __b2_out: [G; 1] = { let mut __scratch: Vec<G> = vec![__v_i, __v_j]; if unconstrained { __scratch.extend(vec![Bytes2::xor(...)]); } else { bytes2_execute(0, 1, &Bytes2Op::Xor, &mut __scratch, record); } let __arr: [G; 1] = __scratch[2..].try_into().unwrap(); __arr }; Net cost: a 2-element `vec![]` alloc + a `__scratch.extend(vec![..])` (another small alloc inside `Bytes2::execute`'s returned Vec) + a slice→array `try_into().unwrap()`. Added per-op `bytes{1,2}_*_value(args..., record) -> G | (G,G) | (G,G,G) | [G; 8]` in `src/aiur/execute.rs` — each bumps the corresponding `bytes{1,2}_queries.bump_*` and returns the gadget output by value. The pure (`Bytes{1,2}::*`) helpers stay the unconstrained shortcut. Codegen now emits: let __v_n: G = if unconstrained { Bytes2::xor(&__v_i, &__v_j) } else { bytes2_xor_value(__v_i, __v_j, record) }; Zero `Vec<G>` allocation per byte op. `U8Add`/`U8Sub` also gain because `bytes2_add_value` runs the `Bytes2::add` gadget once (returning the full `(low, carry)`) instead of the interpreter's two `Bytes2::add` calls (one for the carry, one for the low push). To make `bump_*` callable from `execute.rs`, all `Bytes1Queries` / `Bytes2Queries::bump_*` methods are now `pub(crate)`. No behaviour change. The `Op::Call` cache-check emitted `unconstrained || OP_UN` and `!unconstrained && !OP_UN` even when the static `OP_UN` was `false`, which is the common case. Codegen now emits the folded shape directly: let __cu = unconstrained; // was: unconstrained || false if !unconstrained { *result.multiplicity += G::ONE; } // was: !unconstrained && !false When `OP_UN == true`, the callee always runs unconstrained AND the multiplicity bump is always suppressed; codegen folds to `let __cu = true;` and elides the bump branch entirely. LLVM was already folding these, so this is mostly source-cleanliness and a small frontend win. The cache-hit branch read `result.output` (an `&[G]`) and converted it back to `[G; OUT_N]` via `.try_into().unwrap()`. The length is statically `OUT_N` — we control the producer (the matching `aiur_fn_{callee}::Ctrl::Return` inserts an `[G; OUT_N]`-typed array into the same slot). The runtime bounds-check + Result discharge is dead work. Codegen now emits: let __ret: [G; OUT_N] = unsafe { *(result.output.as_ptr() as *const [G; OUT_N]) }; Sound: same-fn slot, fixed `OUT_N`, no aliasing. | Variant | mean | | --- | --: | | Rust witness (parallel) + codegen | 80 s | | + value-helper byte ops (#1) | 64 s | | + folded `__cu` + unsafe cache copy (#2+#3) | 62 s | The bulk of the win is #1 (#1 alone: ~−18%). #2+#3 are a further ~3% — mostly noise / Rust-frontend cleanup since LLVM already folds the constant `false` ops. * `src/aiur/execute.rs`: 12 value-returning byte helpers added (`bytes1_bit_decompose_value`, `bytes1_shift_left_value`, `bytes1_shift_right_value`, `bytes2_{xor,and,or,less_than,mul, chain_rotr7,chain_rotr4,add,sub}_value`). * `src/aiur/gadgets/bytes1.rs`, `src/aiur/gadgets/bytes2.rs`: all `bump_*` upgraded to `pub(crate)` so the value helpers can call them. * `Ix/Aiur/Stages/Codegen.lean`: `emitU8Bytes1` / `emitU8Bytes2` / `emitU8Add` / `emitU8Sub` rewritten to call the per-op value helpers — no scratch Vec, no slice→array conversion. `emitCall` constant-folds `opUn = false` and emits the unsafe cache-hit copy. Prelude imports updated to bring the new helpers into scope. * `src/ix/aiur_ixvm.rs`: regenerated. 245 `Vec<G>` scratch sites → 11 (only `unconstrainedBigUintDivMod`'s scratch left); 3324 `unconstrained || false` → 0; 3000+ `result.output.try_into() .unwrap()` → 0. * `Ix/Cli/CheckCmd.lean`: incidental cleanup of probe-only timing prints in `runShardOwnedNative` (added during measurement, no longer needed).

Per-claim mode (a `Claim.check addr none`) builds a closure rooted at the target address. That closure can be the whole environment when the target is a heavily-shared root constant. The Lean witness builder paid per-byte boxing into `Aiur.G` for every byte in that closure — the same cost we already eliminated for shard mode. # Surface Five new FFIs, all bundling witness build + execute_ixvm (and STARK prove where applicable) into one cross-language trip so the `IOBuffer` never crosses the boundary mid-pipeline: * `rs_aiur_toplevel_check_addr_ixvm` — `Bytecode.Toplevel.checkAddrIxVM (toplevel) (funIdx) (ixePath) (addrBytes)`: per-claim check; builds witness for `Claim.check addr none` via `build_claim_check_witness`, runs `execute_ixvm`. Same return shape as `shardCheckIxVM`. * `rs_aiur_toplevel_check_env_bytes_ixvm` — same as above but takes the env as a serialized byte blob (`Ixon.serEnv`) instead of a `.ixe` path. Used by the compiled-Lean-env code path (`ix check NAME` without `--ixe`), where the env is built in Lean memory. * `rs_aiur_system_prove_addr_ixvm` — `AiurSystem.proveAddrIxVM (...)`: per-claim prove (witness + execute + STARK prove all in Rust). * `rs_aiur_system_prove_env_bytes_ixvm` — bytes-blob counterpart. * `rs_aiur_system_shard_prove_ixvm` — `AiurSystem.shardProveIxVM (...)`: per-shard prove end-to-end in Rust. `build_claim_check_witness` lives next to `build_shard_check_env_witness` in `src/ix/aiur_ixvm_witness.rs` and uses the same parallel closure walk + parallel byte→G conversion. The bytes-blob FFIs additionally harvest `anon_hints` from each `Def` named entry after `Env::get` — `Env::get` (full form, used by the bytes-blob path) doesn't populate `env.anon_hints` the way `Env::get_anon` does, but the kernel's `verify_claim` reads ch 3 (Defn reducibility hints) so the hints must end up in the env. This mirrors the harvest pass already inside `get_anon` at `src/ix/ixon/serialize.rs:1683`. # Wiring `Ix.Cli.CheckCmd.WitnessSource`: a three-arm discriminated union threaded through `forEachClaim` (the shared check/prove driver): * `.native ixePath addr` — `.ixe`-backed env, Rust mmap. * `.nativeBytes envBytes addr` — Lean-memory env serialized to bytes, Rust decodes via `Env::get`. * `.lean witness` — pre-built `ClaimWitness` (fallback). `runCompiled` and `proveOne` dispatch on the source. # Coverage | Command | Path | |---------------------------------------|-----------------------------------------------| | `ix check NAME --ixe` | **`checkAddrIxVM`** (new) | | `ix check NAME` (no `--ixe`) | **`checkEnvBytesIxVM`** (new) | | `ix check --claim hex --ixe` | `checkAddrIxVM` for `check addr none` | | `ix check --ixes --shard K` | `shardCheckIxVM` (existed) | | `ix check --ixes` | `shardCheckIxVM` (existed) | | `ix prove NAME --ixe` | **`proveAddrIxVM`** (new) | | `ix prove NAME` (no `--ixe`) | **`proveEnvBytesIxVM`** (new) | | `ix prove --ixes --shard K` | **`shardProveIxVM`** (new) | | `ix prove --ixes` | **`shardProveIxVM`** loop (new) | | `Benchmarks/Typecheck.lean` Phase 1 | `checkAddrIxVM` / `executeIxVM` | | `Benchmarks/Typecheck.lean` Phase 2 | `proveAddrIxVM` / `proveIxVM` | | `Benchmarks/IxVM.lean` | `proveIxVM` (was `prove`) | `--interp` route is preserved: it materialises any `WitnessSource` back into a `ClaimWitness` before driving the Aiur source interpreter. `--claim <hex>` over non-`check addr none` variants (`eval` / `reveal` / `contains` / `checkEnv-with-asm`) still uses the Lean witness builder. # Sanity * `ix check Nat.add_comm --ixe init.ixe` (warm): 3.1 s wall, FFT = 23_603_449. * `ix check Nat.add_comm` (compiled env via bytes blob, warm): 2.4 s wall, FFT = 23_603_449. # Known overheads (tracked for a follow-up redesign) * **Per-claim env re-parse on `--ixe + many names`**: each FFI call re-runs `Env::get_anon_mmap` on the same path. Mathlib-scale iteration pays the lazy-index build N times instead of once. * **`--interp + .nativeBytes` round-trip**: Lean serializes the compiled env then `materialise` deserializes it back, just to feed `runInterp`. * **`runShardProveNative` claim reconstruct**: redoes the closure walk + canonical `AssumptionTree` build Lean-side after `shardProveIxVM` already computed the same claim internally. A future `EnvHandle`-based API would close all three: build the env once into a Rust-owned handle, pass the handle to every per-claim/per-shard FFI, and have prove FFIs return the serialized claim bytes.

Before: every per-claim and per-shard FFI re-parsed the Ixon env (`Env::get_anon_mmap` per call). On `--ixe + many names` / all-shards prove, this is the dominant overhead for iteration-heavy workflows — O(num_consts) lazy-index build × N targets. After: the env lives once per CLI invocation in a Rust-owned `EnvHandle`. Lean holds an opaque `Aiur.EnvHandle` reference and threads `@& EnvHandle` through every per-target FFI call. The env is parsed exactly once at handle construction; downstream calls share it. # Surface Five new FFIs collapse the previous six per-call variants (`checkAddrIxVM`, `checkEnvBytesIxVM`, `shardCheckIxVM`, `proveAddrIxVM`, `proveEnvBytesIxVM`, `shardProveIxVM` — all deleted): * `rs_aiur_env_handle_from_ixe(path) → LeanExternal<EnvHandle>`: mmap-load via `Env::get_anon_mmap`. Anon parser already harvests `anon_hints`; no post-pass. * `rs_aiur_env_handle_from_bytes(blob) → LeanExternal<EnvHandle>`: decode `Ixon.serEnv`-shape blob via `Env::get` + harvest `anon_hints` from each `Def` named entry. Used by the compiled-Lean-env path. * `rs_aiur_toplevel_check_addr_with_env(toplevel, fun_idx, handle, addr_bytes)`: per-claim check. Reuses handle's parsed env. * `rs_aiur_toplevel_shard_check_with_env(toplevel, fun_idx, handle, owned_blob)`: per-shard check. * `rs_aiur_system_prove_addr_with_env(system, fri, fun_idx, handle, addr_bytes) → (claim_bytes, proof, ioBuffer)`: per-claim prove. Rust serializes the reconstructed `Ix.Claim` via `ixon::Claim::put` so Lean can deserialize via `Ixon.runGet Ix.Claim.get` directly — no closure walk + canonical `AssumptionTree` recomputation Lean-side. * `rs_aiur_system_shard_prove_with_env(system, fri, fun_idx, handle, owned_blob) → (claim_bytes, proof, ioBuffer)`: per-shard prove. # Lean * `Aiur.EnvHandle` opaque type with `fromIxe` / `fromBytes`. * `Aiur.Bytecode.Toplevel.checkAddrWithEnv` / `shardCheckWithEnv`, `Aiur.AiurSystem.proveAddrWithEnv` / `shardProveWithEnv`. * `Ix.Cli.CheckCmd.Target` replaces `WitnessSource`: ```lean inductive Target where | addr (a : Address) -- Claim.check addr none | shard (owned : Array Address) -- Claim.checkEnv | leanW (w : ClaimWitness) -- --interp, --claim non-check ``` `runCompiled` / `proveOne` take `(envHandle?, target)`. The envHandle is `none` only for `.leanW` (`--interp` legacy path). * `runShardOwnedNative` and the manifest-driver helpers take the envHandle as a parameter. Single-shard mode builds it once; all-shards mode reuses the same handle across every shard's FFI call (eliminates per-shard re-mmap). * `runShardProveNative` deserializes the wire claim bytes via `Ixon.runGet Ix.Claim.get` instead of re-running `shardCheckEnvClaim`. # Benchmarks `Benchmarks/Typecheck.lean` builds the envHandle once before Phase 1, reuses it across Phase 1 (execute) + Phase 2 (prove). Both phases now go through `checkAddrWithEnv` / `proveAddrWithEnv` on the full-closure path. `--subject-only` still uses Lean `buildVerifyConst` + `executeIxVM` / `proveIxVM` (witnesses intentionally small there). # New crate `crates/ix/src/env_handle.rs` — the `EnvHandle` struct + constructors live in the existing `ix` crate next to the witness builder and codegen runner. # Sanity * Multi-target check (warm): `ix check --ixe init.ixe Nat.add_comm Nat.add` → 3.3 s wall, single envHandle shared across both targets. * Shard 26 check (warm): `ix check --ixe init.ixe --ixes init.ixes --shard 26` → ~78 s wall, FFT = 107_006_963_281 (parity preserved). # Coverage | Command | Path | |--------------------------------------|-----------------------------------| | `ix check NAME --ixe` | `checkAddrWithEnv` | | `ix check NAME` (no `--ixe`) | `checkAddrWithEnv` + fromBytes | | `ix check --claim hex --ixe` | `checkAddrWithEnv` for check-none | | `ix check --ixes --shard K` | `shardCheckWithEnv` | | `ix check --ixes` | `shardCheckWithEnv` × all shards | | `ix prove NAME --ixe` | `proveAddrWithEnv` | | `ix prove --ixes --shard K` | `shardProveWithEnv` | | `ix prove --ixes` | `shardProveWithEnv` × all shards | | `Benchmarks/Typecheck` Phase 1+2 | `checkAddrWithEnv` / `proveAddrWithEnv` | Only `--interp` and `--claim hex` over a non-`check addr none` persisted claim still build a Lean `ClaimWitness`; both go via the `.leanW` target arm.

`ix codegen --check` compares the emitted Rust source against the on-disk `crates/ix/src/aiur_ixvm.rs` and exits 0 if identical, 1 otherwise. No write side effect. ~2 s warm; fast enough to gate on every PR. Wired into the `lean-test` CI job so a forgotten regen on a kernel-touching PR fails CI instead of merging stale generated code that drifts from the Bytecode → Rust emitter.

Two interpreter modes behind a single `--interp` flag: * `--interp source`: Aiur source interpreter (`Aiur.runFunction` over the source-level `Decls`). Richer per-step error diagnostics. * `--interp bytecode`: generic Aiur bytecode interpreter (`Bytecode.Toplevel.execute`, `rs_aiur_toplevel_execute` route). Skips the `ix codegen` + `cargo build --release` cycle needed after editing `Ix/IxVM/*.lean` — the bytecode is rebuilt Lean-side at exe load. Slower per-check than the codegen kernel; ideal for tight iteration on the IxVM source. * omit the flag entirely for the native codegen kernel (default). Invalid values (e.g. `--interp foo`) fail fast with a clear error. # Plumbing The `check_addr_with_env` and `shard_check_with_env` FFIs take a `use_bytecode: bool` and dispatch via a shared `dispatch_execute` helper. `--interp bytecode` sets it to `true`. The `.leanW` arm of `runCompiled` also picks between `Bytecode.Toplevel.execute` and `executeIxVM` based on the same flag. The `--interp source` path requires a Lean `ClaimWitness`. The existing driver had switched to `.addr`/`.shard` targets against the Rust-owned `EnvHandle`; source-interp had no way to materialise those. `forEachClaim` now takes a `forceLeanWitness : Bool` — when true, it builds a Lean witness for every target (via `mkWitness` / `loadIxonEnv` for the compiled-Lean-env path) and passes `.leanW` so `runInterp` can consume it directly. # Sanity * `ix check Std.Time.Week.Offset.ofMilliseconds` (warm): 9.3 s wall, FFT = 12_430_516_949 (codegen kernel). * `ix check --interp bytecode Std.Time.Week.Offset.ofMilliseconds` (warm): 14.6 s wall, FFT = 12_430_516_949 (bytecode interp). * `ix check --interp source Eq` (warm): 6.3 s wall, output `Eq: ()`. * `ix check --interp garbage Nat.add_comm`: exits 1 with clear error.

Aligns the ap/codegen-ixvm-native stack with main's KLevel pointer port (b84a500) and re-lands clippy-clean under the workspace lint set: - Regen crates/ix/src/aiur_ixvm.rs from Aiur source (KLevel = &KLevelNode changes the generated fn shapes; ~26k lines net churn). - Extend the generated file's #![allow(...)] header (via Ix/Aiur/Stages/Codegen.lean) with clippy::ptr_as_ptr, clippy::match_same_arms, and clippy::large_types_passed_by_value — three lints the codegen's straight-line style trips deterministically on every regen and that clippy::all doesn't cover. - rustfmt reflow in crates/aiur/src/execute.rs and a handful of ix / ffi files that CI now enforces via the ap/aiur-aux-recursor-parity toolchain. - Fix 4 real clippy warnings uncovered under the workspace lint set: * env_handle.rs: clone-on-Copy → deref (ReducibilityHints is Copy). * aiur_ixvm_witness.rs: collapse if-let-if, drop needless continue, slice::from_ref instead of &[x.clone()]. * aiur_ixvm_runner.rs: keep execute_ixvm's Vec<G> arg (required by AiurSystem::prove_ixvm's fn-pointer bound) + local #[allow( clippy::needless_pass_by_value)] with a comment explaining why. * ffi/aiur/protocol.rs: unqualify aiur::G/IOBuffer/QueryRecord after the workspace lint added unused_qualifications; is_multiple_of() over % 0. Verified: cargo clippy --workspace --all-targets --all-features --D warnings clean; lake test -- --ignored ixvm passes.

samuelburnham

Claude review

1. Default `ix check --ixes` dropped the coverage check

runShardManifestAllNative (Ix/Cli/CheckCmd.lean:477) never calls shardsCover; the docstring says "skips the coverage check; trust the user". At the merge base, the all-shards route
went unconditionally through runShardCheckAll, which gates on shardsCover first.

Since the .ixes manifest is an untrusted input reconciled against the env by silent intersection (ownedConstsForBlocks, CheckCmd.lean:387), a stale/truncated/buggy manifest now makes
ix check --ixes exit 0 while some env constants are never checked by any shard. The most likely trigger is the mundane one: edit a definition, rebuild the .ixe (content addressing gives
the edited cone new addresses), forget to re-run ix shard — and the constants that go unchecked are exactly the ones just edited. shardsCover's own docstring calls coverage "the whole
soundness condition for the check case", so exit 0 silently stops meaning "the environment typechecks".

Both ixonEnv and shards are already in scope from loadEnvAndShards, so the fix is the same one line runShardCheckAll uses (CheckCmd.lean:558):

if !(← shardsCover ixonEnv shards) then return 1

(Skipping it on the single-shard --shard K path is fine/consistent with before; it's the all-shards "full verdict" mode that needs it.)

2. `ix check --ixe … --claim <hex> --interp source` regressed

The claimHex arm of forEachClaim (CheckCmd.lean:229-234) maps .check addr none to Target.addr unconditionally, ignoring forceLeanWitness — unlike the two name-based arms right
below it (:243, :261), which consult the flag. Under --interp source, runOne then rejects .addr with "--interp requires a Lean witness; addr/shard targets unreachable here" — so
re-checking a persisted check addr none claim under the source interpreter always fails (with a message claiming the path is unreachable). At the merge base this combination worked (the
claimHex arm always built a Lean witness). Fix is to mirror the sibling arms:

| .check addr none =>
if forceLeanWitness thenlet witness ← IO.ofExcept <|
IxVM.ClaimHarness.buildClaimWitness ixonEnv claim trees
pure (.leanW witness)
else pure (.addr addr)

Ironically only the common claim shape breaks — the exotic variants fall through to .leanW and interpret fine. And this is exactly the debug path someone reaches for when the fast path
gives them a failure.

3. Witness IOBuffer layout is nondeterministic across runs

closure_from_set (crates/ix/src/aiur_ixvm_witness.rs:119) collects the closure via DashSet::new() (std RandomState, fresh seed per process), and that ordering feeds arena idx
assignment in add_entries_parallel. Those idx/len values are committed as auxiliary trace columns (trace.rs, Op::IOGetInfo), so proof bytes can differ run-to-run and never
byte-match a Lean-built witness's layout. The QueryRecord itself is insulated (all io_get_info call sites consume idx/len locally — so the bit-identical-trace claim in the PR
description survives), and soundness is unaffected; this is about reproducible proofs and future Lean-vs-Rust differential testing.

The fix is nearly free: build_shard_check_env_witness already computes a sorted closure_vec but then passes the unsorted set to add_entries_parallel; build_claim_check_witness
doesn't sort at all. Sorting both makes the layout canonical.

Worth addressing (this PR or follow-up)

4. No in-tree parity test

The whole design rests on "generated kernel ≡ interpreter on the QueryRecord", but there's no test or CI step that runs both paths on a fixture and diffs the records (no #[test] under
crates/ix/). One record-equality test on a small workload would turn the parity invariant from reviewed-by-hand into checked-by-CI.

samuelburnham

Stamping to unblock pending CI

samuelburnham · 2026-07-02T22:08:56Z

It's a bit unclear what this crate is for based on the name, maybe it could be renamed to ix-codegen?

…rity + rename ix crate to ixvm-codegen Four review fixes on the codegen-ixvm-native stack. - **Coverage gate on \`--ixes\` (all-shards, native path).** \`runShardManifestAllNative\` now calls \`shardsCover\` before running any shard, matching the pre-refactor \`runShardCheckAll\` behavior. Without this, a stale/truncated \`.ixes\` manifest makes \`ix check --ixes\` exit 0 while some env constants are never checked by any shard — the mundane trigger being: edit a definition, rebuild the \`.ixe\`, forget to re-run \`ix shard\`, and the constants that go unchecked are exactly the ones just edited. Single-shard \`--shard K\` path is unchanged (consistent with pre-refactor). \`shardsCover\` moved above \`runShardManifestAllNative\` to satisfy forward-decl ordering. - **\`ix check --ixe … --claim <hex> --interp source\` regression.** The \`claimHex\` arm in \`forEachClaim\` ignored \`forceLeanWitness\` and always mapped \`.check addr none\` claims to \`Target.addr\`. Under \`--interp source\`, \`runInterp\` then rejects \`.addr\` with "\`--interp requires a Lean witness; addr/shard targets unreachable here\`". Now mirrors the sibling name-based arms and routes through the Lean witness path when \`forceLeanWitness\` is on. Only bit the common claim shape. - **Codegen ↔ bytecode parity CI test.** New \`runParityCase\` + \`parityCases\` in \`Tests/Ix/IxVM.lean\` wire every constant already listed in \`kernelCheckEntries\` plus \`kernel_unit_tests\` through BOTH \`Toplevel.execute\` (bytecode) and \`Toplevel.executeIxVM\` (codegen'd Rust), and diff the returned \`(output, IOBuffer, QueryCounts)\` triples. Turns "generated kernel ≡ interpreter on QueryRecord" from reviewed-by-hand into checked-by-CI. 129 assertions run per suite invocation (43 constants × output + IOBuffer + QueryCount), all pass on this branch head. - **Rename \`crates/ix\` → \`crates/ixvm-codegen\`.** The old \`ix\` crate held only the codegen'd IxVM kernel + its runner + witness helpers. \`ix-kernel\` is the hand-written Rust ix typechecker; \`ix-common\` / \`ix-compile\` are Ix-level infrastructure. \`ixvm-codegen\` cleanly names what this crate holds. Path updates: workspace \`members\` and \`workspace.dependencies\`, ffi crate dep + \`use\` sites, Lean \`codegenOutPath\` in \`Ix/Cli/CodegenCmd.lean\`, doc reference in \`Ix/Aiur/Semantics/BytecodeFfi.lean\`. \`ix codegen\` now writes to \`crates/ixvm-codegen/src/aiur_ixvm.rs\`. Verified: \`cargo check --workspace\` + \`lake test -- --ignored ixvm\` both exit 0 post-rename; parity + pinned FFT tests all pass.

Post-rename, ixvm-codegen pulls stacker → psm → ar_archive_writer (a build-time transitive). ar_archive_writer is licensed under the LLVM-exception variant of Apache-2.0 (standard for LLVM tooling; no additional runtime obligation for downstream users), which isn't on the workspace allow list. Add a per-crate exception scoped to ar_archive_writer so we don't blanket-allow the license family across the tree.

The op (added with the native execution pipeline, #463) pushes two values onto the value map during execution — the quotient/remainder list-head pointers — and the constraint generator allocates two auxiliary columns for them, but the trace populator treated it as a no-op. Every ValIdx and witness column after the first big-Nat division in a block was therefore off by two, and trace population panicked with "index out of bounds" at trace.rs:308 — the exit-134 failures on every big-Nat-heavy prove in the bench-main aiur job (List.mergeSort, String.split, the SInt instRxcHasSize_eq family, Multiset.sort, …). Reproducible in seconds with any Nat-division user, e.g. `bench-typecheck --consts Nat.repr`. The trace arm now mirrors the execute arm: recompute (q, r) with num_bigint and resolve the head pointers execution already recorded in memory[10] via a read-only twin of build_klimbs_u64, pushing both as map entries + auxiliary columns. Verified: Nat.repr proves end-to-end (panicked before); `lake test -- --ignored aiur ixvm` passes; clippy clean.

* fix(zisk): drop --max-witness-stored flag, use Zisk's default cap Lowering the witness cap below Zisk's built-in default (10) was measured to have a negligible effect on host RAM and prove time for the kernel typecheck workload, so the CLI override (which defaulted to 5) is removed and the prover uses EmbeddedOpts::default(). Drop the now-stale flag mentions and per-RAM tuning guidance from the README, the cost-model doc, and the shard.rs model comments. * feat(ci): CSV-driven !benchmark + Zisk/SP1/native benchmarks Rebased onto main (post #411 + #459) and integrated with the renamed bench-main.yml and reworked bencher-track interface. - Benchmarks/Vectors.csv: single shared source of truth (71 library constants from Init/Std/Mathlib/Lean). Consumed by Aiur (bench-typecheck --manifest), the zkVM hosts, and shell. - bench-pr.yml: `!benchmark [aiur] [zisk] [sp1|all] [execute|prove]` over the curated set, posting a main-vs-PR table; main results cached by base SHA. Hardened: comment body from env (no injection), allowlisted env parsing. - .github/scripts/{bench.py,run.sh}: parse/manifest/compare/comment, and the compile-.ixe + backend driver (cycles/execute-time/throughput/peak-rss, plus shards/max-shard-cycles for sharded runs). - .github/actions/install-{sp1,zisk}: shared zkVM toolchain + deps install, used by bench-pr.yml, bench-main.yml, and riscv-bench.yml. - bench-main.yml: add zkvm-execute (Zisk/SP1 cycle counts + time/RAM) and native-check (native parallel `ix check --anon` throughput) jobs, using the new bencher-track workload/thresholds interface. - bench-typecheck: add --constant / --skip-deps (align with the zkVM hosts; --skip-deps replaces --subject-only) and --execute-only (fast execute path). * test(ci): trigger bench-pr.yml on pull_request (TEMPORARY) issue_comment workflows only run from the default branch, so the `!benchmark` path can't be exercised on a PR branch. Add a pull_request trigger (base/head from the PR payload; empty comment → parser defaults) to test pre-merge. Revert before merge — delete the `pull_request:` trigger; the dual base/head resolution and `|| pull_request.number` fallbacks are harmless to keep. * feat(ci): default to ~11 primary constants The full curated set (~60 InitStd) is too slow to run on every !benchmark and on the bencher prove/zkVM jobs. Add a `primary` column to Vectors.csv marking 11 constants spanning shape (nat/list/array/int/string/vector/multiset, defs + proofs) and the cheap→heavy cost range (incl. 3 shard targets), and make it the default: - bench.py manifest --primary; parse honors BENCH_FULL (run the full set). - bench-pr.yml: !benchmark defaults to the primary subset; BENCH_FULL=1 runs the whole curated set. - bench-main.yml: prove + zkvm-execute derive constants from `manifest --primary` (replacing the hardcoded lists), so all backends bench the same set from the one source of truth. The tier filter keeps prove on the cheap primaries (heavy ones would OOM a single-shard prove); execute/native get the heavy ones for scale. * feat(ci): native backend on !benchmark + bencher parity/cleanup Bring both surfaces (!benchmark PR comment and bencher.dev) to parity across all four backends and remove the test scaffolding. - Native kernel on !benchmark: add a `native` backend (whole-env `ix check --anon`, the parallel out-of-circuit kernel) — bench.py backend/runner/metrics, a run.sh `native` branch, and a GNU-time install for native PR cells. `all` now fans out aiur/zisk/sp1/native. - run.sh: single-source the Aiur path through a per-constant bench-typecheck loop (per-constant peak-rss), add a per-constant `timeout` to the zkVM execute path (heavy primaries can't hang a job), and accept the env arg case-insensitively (bencher reuses the cached InitStd.ixe; bench-pr compiles initStd.ixe). - bench-main.yml: the prove and native-check jobs now drive run.sh too (dedup with the PR path); zkvm-execute gains the Mathlib env to match prove/native. - bench-thresholds-reset.yml: register the zisk / sp1 / native-check workloads. - bench-pr.yml: drop the temporary pull_request trigger (keep the harmless dual-SHA / number fallbacks). - docs/benchmarking.md: document the two surfaces, backends, Vectors.csv, the !benchmark grammar, and the bencher workloads / threshold resets. * feat(ci): Aiur proves all primaries that fit 128GB; native checks primaries too - Aiur prove now covers the whole primary subset: bench.py exempts --primary from the prove cheap-tier cap, and run.sh proves each constant whose Aiur fft-cost fits the prover RAM ceiling (AIUR_PROVE_MAX_FFT, ~128 GB at 2.34 GB per billion fft) and execute-only's the rest — so heavy primaries (only Vector.extract_append at ~145 GB) still report execute metrics instead of being dropped. BENCH_FULL prove stays capped at the cheap tier so it doesn't balloon. - native now reports two views per env: the whole env (`ix check --anon`, keyed by env) and a per-primary subject check (`ix check --consts`, keyed by constant) — apples-to-apples with the zkVM --skip-deps execute. Wired into both the native-check bencher job and the !benchmark native backend. - run.sh: fix a stream-corruption bug — tool stdout and ::warning::/::notice:: now go to logs/stderr so only JSON reaches the per-constant `jq -s` merge. * feat(ci): texray per-phase drill-down + child-process-aware peak RAM Route every backend's peak-rss and per-phase timings through tracing-texray: - peak-rss now comes from the fork's process-tree sampler, so Zisk's ASM microservices' memory (tens of GB in separate PIDs) is captured — a bare /proc/self/status read of the host missed it. Verified on real execute runs: sp1 ~9GB, zisk ~49GB peak. - zisk/sp1 hosts and bench-typecheck self-report cycles/time/throughput/ peak-rss via --json, retiring run.sh's grep/awk/time parsing. They also emit per-phase span timings via --texray-json; native check-rs reports peak-rss as a 6th ##check## field. - run.sh folds span timings into a per-constant `phases` object; bench.py renders a collapsible per-phase drill-down in the !benchmark comparison, and bench-main.yml tracks phase: measures on bencher. tracing-texray is pinned to the argumentcomputer/tracing-texray json-ram branch (rev 15ae57c), which adds the process-tree RSS sampler + JSON sink. * refactor(ci): rename backend native→ooc; suffix bencher workloads with -check - Backend `native` is renamed to `ooc` (out-of-circuit) throughout: the BACKENDS tuple in bench.py, the run.sh case arm, the `native-check` job in bench-main.yml (now `ooc-check`), the `\!benchmark` grammar in bench-pr.yml, and docs/benchmarking.md. - Bencher workload names carry an explicit `-check` suffix so the tracked identity is self-describing: `aiur-check`, `zisk-check`, `sp1-check`, `ooc-check` (was `aiur`, `zisk`, `sp1`, `native-check`). Reset workflow tokens (options / valid / accepted / error text), tag-reference comments, and the bencher-track action's docstring updated to match. - Clarify the `\!benchmark` grammar: `([aiur] [zisk] [sp1] [ooc] | all)` — `all` is an alternative to the whole backend list, not just to `ooc`. * refactor(ci): bencher-first !benchmark, unified --consts CLI, RAM harness **bench.py !benchmark surface** - `fetch-main`: queries bencher.dev's public reports API for `branch=main` at the base SHA, filters results by `--names`, and reshapes into the neutral `{ "<name>": { "<metric>": v } }` shape. Replaces the actions/cache layer; bench-pr.yml falls back to a local base run only when bencher hasn't ingested the base SHA yet. TODO left for non-main base branches. - Mode is fixed per backend (`aiur=prove`, others=`execute`); the optional bare `execute` token in `!benchmark` flips aiur to `--execute-only`. Grammar drops `[execute|prove]` and `BENCH_GPU`; zkVM prove paths removed. - Single runner `warp-ubuntu-latest-x64-32x` for every cell; testbeds unified to `<backend>-check-x64-32x`; `MAIN_TESTBEDS` maps (backend, mode) to the slug. - `compare` renders the OOM sentinel `{"oom": true}` as `OOM` cells + `n/a` Δ%. Regression/improvement flags fire on every metric column (previously only the first); summary counts distinct constants; worst names constant + metric. `_human` is unit-aware: bytes → GiB/MiB, seconds → µs/ms/s/m, counts → K/M/B/T. - Sub-span (per-constant phase) drill-down removed with a TODO; `run.sh`'s `merge_phases` and `bench-main.yml`'s `phase:` flattening still populate the neutral JSON for later reinstatement. **CLI unification** (bench-typecheck, zisk-host, sp1-host) - Dropped `--constant`; added `--consts <n1,n2,…>` (comma-list, clap `value_delimiter` on the Rust hosts) and `--consts-file <path>`. Multi-const runs loop the single-const path per name, accumulating one entry per name via a merge-safe `write_json_entry`. - Dropped `--texray-json <path>` and `--no-texray`. `--texray` (bool) alone toggles the tracing-texray subscriber; combined with `--json <path>`, span timings auto-write to `<json>.spans`. - Inline `#[cfg(test)] mod cli_tests` in each Rust host covers value-delimiter parsing, `--consts` `requires`, and `collect_consts` union/dedup. **Vectors.csv** - Removed `aiur_fft`, `zisk_cycles` (measurements live in bencher, never here). Rows can now omit trailing zero fields; parser tolerates 3+ cols. - Primary set curated: renamed `Vector.extract_append` → `Vector.extract_append._proof_1` (kept as shard_target); promoted `Vector.append` and `Nat.sub_le_of_le_add` to primary; added the un- shardable Init constants from the Zisk cost-model doc's canonical 12 (`Char.ofOrdinal_le_of_le`, `Array.extract_append._proof_1_1`, the `SInt.Int{8,16,32,64}.instRxcHasSize_eq` family with the case corrected), plus `ByteArray.utf8DecodeChar?_utf8EncodeChar_append`, `String.append`, `IxVMPrim.nat_pow_big`, and `Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual`. Trimmed obvious duplicates (`Array.qsort`, `Int.ediv`, `List.dropLast`, `List.range`, `UInt32.toNat`, `Std.Time.Month.Offset.ofNat`). **RAM harness** (run.sh, aiur prove) - Tier gate removed. Every constant attempts a full prove. - `watch_ram_kill` samples `ps -eo pid,ppid,rss` every ~3 s and SIGKILLs the tree if it exceeds `AIUR_PROVE_MAX_RSS_GB` (default 120 GB — 8 GB headroom under 128 GB). Killed constants record `{"oom": true}` for the compare table. **Misc** - `install-zisk`'s description now correctly says the proving key is installed (`client.setup()` loads const-trees before execute too). - `bencher-track`'s workload description enumerates all options. - `zisk/Cargo.toml`'s patch example uses `/path/to/…`, not `/home/ubuntu`. - `docs/zisk-cycle-cost-model.md` finding #4 disambiguates "not-shardable" (mutual blocks only) from "not full-closure-single-leaf provable" (the canonical 12). - `riscv-bench.yml` still on the temporary `sb/ci-benchmarks` push trigger; drop before merge. * feat(ci): compile as a !benchmark backend; full-closure zkVM parity; threshold + doc cleanup **`compile` as a !benchmark backend** - bench.py: `DEFAULT_MODE["compile"]="compile"`, `MAIN_TESTBEDS[("compile","compile")]="ix-compile-x64-32x"`, `METRICS[("compile","compile")]=["compile-time","throughput","file-size", "constants"]`. `cmd_manifest` short-circuits on `--backend compile`: writes a one-line names.txt with the CamelCase env slug (`InitStd` / `Lean` / `Mathlib` / `FLT`) and skips the CSV. New `--backend` arg on manifest. - run.sh: setup step teed to `$compile_log` for every backend; `compile` ignores REUSE_IXE (needs a fresh compile to measure) and parses `##benchmark## <elapsed_ms> <bytes> <constants>` into the neutral `{ "<CamelCase>": {"compile-time","file-size","constants","throughput"} }` shape. Compile job on main (`bench-main.yml` testbed `ix-compile-x64-32x`) is the same run bencher already stores. - bench-pr.yml: `!benchmark ([aiur] [zisk] [sp1] [ooc] [compile] | all)`; manifest step passes `--backend "$BACKEND"`. **zkVM parity with ooc (drop `--skip-deps`)** - run.sh zisk/sp1 branch: `--consts <c>` without `--skip-deps` so the check is directly comparable to `ooc`'s `ix check-rs --consts <c>` (also full-closure). Comparing subject-only zkVM against full-closure ooc mixed in-circuit-vs-out-of-circuit overhead with scope; both are now full-closure, so the delta isolates just the overhead. **Threshold semantics for deterministic-but-directional measures** - bench-main.yml zkvm-execute (now zkvm-typecheck): `cycles`, `shards`, `max-shard-cycles` change from pinned `0/0` to `upper 0 / lower _`. These are deterministic (no noise) but a real guest / packer improvement legitimately drops them; the old pin flagged wins as regressions. `constants` (definitional count) stays `0/0`. **docs/benchmarking.md — stale content swept** - Removed the "design-level skips post a note explaining why" paragraph (that machinery was already removed). - Replaced the `cheap → prove / heavy → execute-only` fallback description with the RAM-watchdog reality (attempts prove for every primary; OOMs go through as `{"oom": true}` sentinels rendered `OOM`). - Backends table adds `compile`; drops metrics `aiur` doesn't actually emit. - "Constant set": ~20 primaries in ~68 total (was ~11 in ~60); notes tier is informational-only now, rows may omit trailing zeros, and `compile` short-circuits the CSV. - Per-measure threshold breakdown replaces the incorrect "Deterministic measures … are pinned exactly" claim. - "Not yet covered" now lists three real TODOs (zkVM prove, per-constant phase drill-down, non-main base branches) with pointers to the in-code TODO markers. **Code comment audit** — every touched comment/docstring re-read; stale references to `--skip-deps` parity, tier-based fallback, sub-span drill-down, and cache-hit rendering all updated to match implementation. * feat(ci): annotate compare table cells with ratio (1.5x faster/slower) Δ% is easier to interpret at scale when paired with a ratio — e.g. `-33.3% (1.50x faster)` for a big prove-time drop; `+15.2% (1.15x slower)` for a real execute-time regression. Only shown when the factor is >= 1.05x (roughly ±5% in either direction) so sub-noise deltas don't get `(1.02x slower)` clutter next to `+1.1%`. Cell format cascades cleanly: `{Δ%} [(1.NN× {slower|faster})] [emoji]`. * fix(ci): review fixes — full-closure check-rs, OOM/polarity/caching, dedup Fixes from the branch-wide review, plus build-once caching and a dedup pass. **check-rs full-closure mode (new kernel FFI)** - `rs_kernel_check_anon_consts`: resolve displayed names via the env's `named` map (the zkVM hosts' resolution), then anon-check the seeds' FULL dependency closures via the existing `closure_addrs` + `build_anon_work` primitives — no sub-env serialization. `skip_deps` restricts to subject-only. `index_anon_work` extracted so the whole-env and filtered paths share the result-slot indexing. - `ix check-rs --anon --consts <names>` now runs that (full-closure default, `--skip-deps` opt-out — the hosts' CLI shape); meta-mode seeded checks are unchanged (subject-only, bisect flows intact). run.sh's ooc per-constant view uses it, so ooc-vs-zkVM deltas genuinely isolate in-circuit overhead (both sides now full-closure anon; previously ooc was subject-only meta). **OOM sentinel end-to-end** - run.sh merges `oom: true` INTO already-measured Phase-1 metrics (was: overwrite); compare renders OOM only for the missing metrics. - `bench.py bmf` (one neutral→BMF converter replacing four hand-copied jq/awk pipelines in bench-main.yml) strips the boolean sentinel — one OOM row no longer fails the whole bencher upload. This also covers the zkVM execute path, which gained its own RAM watchdog + sentinel. - Watchdog: setsid + process-group kill (reaches all descendants); kernel OOM beating the 3 s sampler (exit 137, no marker) labels OOM instead of silently dropping; per-constant wall-clock timeouts (AIUR_PROVE_TIMEOUT 50m / AIUR_EXECUTE_TIMEOUT 25m); $out re-merged per constant so a job-level kill keeps completed rows. **compare correctness** - throughput is higher-is-better: flags/worst/ratio direction-aware (HIGHER_IS_BETTER + _badness). - Ratio wording follows metric kind: times faster/slower, bytes larger/smaller, counts more/fewer. - `execute-peak-rss`: Phase-1 RSS high-water sampled at the Phase 1/2 boundary in bench-typecheck (both modes) and adopted by the zkVM hosts' execute JSON — one name for "execute-phase peak" on every backend; bare `peak-rss` reserved for prove-phase peaks. aiur-execute compares it apples-to-apples against prove-run baselines (raw peak-rss would dwarf it). - One-side-empty tables get a loud note (e.g. CLI-incompatible base). - Tidy JSON: bench-typecheck emits decimal `JsonNumber`s (`jsonRound`) instead of Float's full binary repr. **fetch-main robustness** - Retry with backoff + newest-first pagination (base SHA beyond page one no longer forces a permanent fallback). - Exit codes honored by bench-pr.yml: 3 (transient) → local fallback; 2 (BACKEND_TABLE / bench-main drift) fails the cell loudly. - ooc whole-env row keyed CamelCase on both sides (benv_cc table in run.sh, ENV_CC in bench.py) and admitted past the --names filter. **build-once + caching (bench-pr.yml)** - New build job: ix + bench-typecheck built once per head SHA (they embed the IxVM kernel/prover), cached as `bench-bins-<sha>`; cells restore into .bins/pr instead of per-cell Lean builds. Re-running \!benchmark on the same commit skips the build. - Base fallback restores bench-main's own `bench-bins-`/`bench-ixe-` caches (toolchain cmp + mathlib-oleans guard) before paying for a from-scratch base build. PR-side .ixe cached across cells. - Cache keys renamed `aiur-bench-bins-`/`aiur-ixe-` → `bench-bins-`/`bench-ixe-` (they serve every backend). - run.sh resolves tools in-tree first, then PATH (`resolve_bin`). **dedup** - bench.py: DEFAULT_MODE + METRICS + MAIN_TESTBEDS collapsed into one BACKEND_TABLE (mode / testbed / per-mode metrics). - bench-main's compile job routes through run.sh's compile backend + bmf — the `##benchmark##` line is parsed in exactly one place (run.sh gains `flt` in its env table for the FLT matrix cell). - `Ix.Cli.ConstsFile`: one names-file/comma-list parser (inline-`#` comments, dedup) shared by check-rs meta+anon, bench-typecheck, and `ix compile --exclude-file` — closes the whole-line-vs-inline comment drift across the five previous copies. **hosts** - clap `requires = "consts"` dropped from --json/--skip-deps (rejected valid --consts-file-only runs); validated in main after collect_consts. zisk's multi-`--ixe` guard now covers --consts-file. **misc** - Vectors.csv / docs tier semantics corrected (manifest-only consumer); stale prove-fallback comments fixed; tracing-texray bumped to bd4faa08; push-to-main workflows drop their concurrency groups (every merged commit must be benchmarked; a later merge must never cancel one). Verified: cargo check -p ix-ffi, lake build ix / bench-typecheck, live runs of the new check-rs mode against a 480 MB Init/Std env (closure = 34 items / 42 targets for Nat.add_comm; --skip-deps = 1; missing names error loudly), bmf/parse/compare dry-runs, YAML + bash -n + AST checks. zisk/sp1 host crates compile-verified in CI only (local sandbox lacks the pil2-proofman C++ toolchain). * ci: convert riscv-bench into a zkVM host build+test gate (no proving key) bench-main.yml's zkvm-execute job now runs real executions of both hosts on every main push, but tolerates per-constant failures by design (dropped rows, OOM sentinels) — it never turns red on a breakage. This workflow becomes the red-X signal instead, kept cheap: - Build-only + unit tests: `cargo build --release --bin <host>` plus `cargo test --release --bin <host>`, which covers the clap surface run.sh drives (--consts comma-splitting, --consts-file union/dedup, shard-plan conflicts). No execution, so no fixture compile job, no minimal.ixe artifact, no memlock prlimit. - install-zisk gains a `proving-key` input (default true): the key is loaded at runtime by `client.setup()`, never at build time, so the build gate skips the ~3 GB download + const-tree regeneration. - Renamed "RISC-V bench" → "zkVM host build" (it no longer benchmarks). - The TEMPORARY sb/ci-benchmarks push trigger (from the mid-branch test commit) reverts to main-only here; the tip commit is its sole carrier. The runtime/typecheck smoke signal (executing myReflEq and asserting failures == 0) is retired: that coverage now lives in zkvm-execute's real runs, at the cost of being warnings-not-red-X. * fix(ci): pre-build proofman-starks-lib-c to serialize the shared make zisk-host pulls zisk-sdk as both a dependency and a build-dependency, so cargo compiles proofman-starks-lib-c as two units whose build scripts can run concurrently — and both run `make` inside the SHARED ~/.cargo/git/checkouts/pil2-proofman-* source tree (not OUT_DIR). On a cold runner the Makefile stamp is absent, so both units take the `make clean` + `make -j` path and race: one unit's clean deletes build/ while the other's g++ is mid-compile, dying with "opening dependency file ….d: No such file or directory" (g++ writes .d files at the END of compilation, so the dir vanished underneath it). Warm runners never hit it — the stamp short-circuits the clean — which is why the race only surfaced on this branch's cold cache (lockfile change → new rust-cache key). install-zisk now builds the sys crate solo first: its build script runs once, `make` completes, the stamp lands; both units of the subsequent parallel build then skip the clean and their `make -j` is a no-op. Same total work, just ordered. The proper fix is an flock around the make in pil2-proofman's build.rs — worth an upstream PR. * fix(ci): resolve run.sh tool binaries lazily at their use sites `resolve_bin ix` ran unconditionally at startup, but bench-main's zkvm-execute job legitimately has no `ix` anywhere: it restores only the `.ixe` cache (REUSE_IXE=1 skips the compile step) and builds its zkVM host via cargo — before the resolve_bin refactor that job never touched `ix` at all, so the eager check regressed it with "ix not found (in-tree or PATH)". Resolve per use site instead: the compile step and the ooc branch resolve `ix`, the aiur branch resolves `bench-typecheck`, and the zkVM branch needs neither. * fix(ci): classify alloc-abort proves as OOM, sweep Zisk shm, fix vector names Three fixes for the failing bench-main runs: - run.sh: a heavy prove can die of memory without tripping the watchdog or the kernel OOM killer — one huge trace allocation fails and the runtime aborts (SIGABRT, exit 134) with an allocator message. looks_like_oom() folds that third case into the OOM classification so those constants get an OOM row instead of being dropped. Non-OOM failures now log the first lines of the tool output so drops are diagnosable from the job log. - run.sh: after a watchdog group-kill, the Zisk host never runs its Drop-time cleanup of /dev/shm/ZISK_* segments (multi-GB; the MT output segment alone starts at 6 GB), so the next host launch fails creating its own segments before Zisk's startup stale-pid sweep runs — exactly one dropped constant after every OOM kill (the alternating OOM/exit-1 pattern in the zisk-execute logs). Sweep the debris between constants. - Vectors.csv: IxVMPrim.nat_pow_big removed (kernel primitive, never present in compiled envs); Vector.extract_append._proof_1 → ._proof_2 and Array.extract_append._proof_1_1 → Array.extract_append (proof-term names are toolchain-dependent; both replacements verified against a freshly compiled initStd.ixe and measured heavy: fft-cost 23.4e9 / 40.1e9). * ci: move the zkVM host build gate into ci.yml; comment out the sp1 benchmarks riscv-bench.yml's two jobs (build + unit-test the Zisk/SP1 hosts, no execution, no proving key) are cheap enough (~5 min with warm caches) to gate every PR commit, and ci.yml already has exactly the triggers and per-ref cancellation they need — so they move there and the standalone workflow goes away. sp1 benchmarks are commented out for now — the execute run is too slow: the sp1 cell of bench-main's zkvm-execute matrix and bench-pr's Install SP1 step. Uncomment both to re-enable. The \!benchmark backend-subset selection is unchanged. * fix(aiur): populate trace rows for UnconstrainedBigUintDivMod The op (added with the native execution pipeline, #463) pushes two values onto the value map during execution — the quotient/remainder list-head pointers — and the constraint generator allocates two auxiliary columns for them, but the trace populator treated it as a no-op. Every ValIdx and witness column after the first big-Nat division in a block was therefore off by two, and trace population panicked with "index out of bounds" at trace.rs:308 — the exit-134 failures on every big-Nat-heavy prove in the bench-main aiur job (List.mergeSort, String.split, the SInt instRxcHasSize_eq family, Multiset.sort, …). Reproducible in seconds with any Nat-division user, e.g. `bench-typecheck --consts Nat.repr`. The trace arm now mirrors the execute arm: recompute (q, r) with num_bigint and resolve the head pointers execution already recorded in memory[10] via a read-only twin of build_klimbs_u64, pushing both as map entries + auxiliary columns. Verified: Nat.repr proves end-to-end (panicked before); `lake test -- --ignored aiur ixvm` passes; clippy clean. * feat(bench): track Aiur proof-size and verify-time Prover changes can trade prove speed against proof size or verification cost, so Phase 2 now serializes each fresh proof (proof-size, bytes) and verifies it (verify-time; a verification failure is reported loudly and drops only that measure). The full-closure path rebuilds the Array-G claim from proveAddrWithEnv's serialized claim bytes — verify_claim's input is the 32-G blake3 digest of those bytes, the same recipe as `ix verify`. Both measures flow through the neutral JSON into the PR compare table (bench.py aiur prove metrics + byte/second unit mapping) and onto bencher (verify-time 10% upper, proof-size 5% upper). Measured: Nat.add_comm proves in 1.63s, verifies in 0.19s, 33.4 MB proof. * feat(ci): env-sharded zisk execute via ix profile → ix shard manifests The constants that OOM as single full-closure leaves (extract_append proofs, the instRxcHasSize_eq family, …) are only measurable under env sharding — their checks fit in one manifest shard each, with deps checked in other shards (docs/zisk-cycle-cost-model.md, finding 4). Wire the existing offline partitioner into CI instead of any per-constant sharding: - compile job: after the compile benchmark, `ix profile <Env>.ixe` → `ix shard --max-ram 120` for InitStd/Mathlib; the `.ixes` manifest is cached next to the `.ixe` (every restore of that key lists the same paths — actions/cache versions entries by path list). - zisk-host: `--shard-plan --execute --json` now writes one env-level row — total cycles, shards, max-shard-cycles, execute-time, throughput, execute-peak-rss, and a per-shard `shard-cycles` breakdown — keyed by the new `--json-name` (default: manifest stem). - run.sh: the zkVM guest-run dance (setsid + RAM watchdog + OOM classification + shm sweep + merge) is factored into one `zkvm_run` helper; when a `.ixes` sits next to the `.ixe` (bench-main only — the \!benchmark PR path has none) the zisk branch appends the env-sharded run after the per-constant loop. - bench.py bmf: nested-object flattening generalized — `phases` → `phase:` as before, any other dict (e.g. `shard-cycles`) → `<key>:` — so per-shard cycles land on bencher as un-thresholded measures while the thresholded aggregates (cycles, shards, max-shard-cycles) do the alerting. zkvm job timeout 60 → 150 min: the whole-env run (own 60m cap inside run.sh) rides on top of the per-constant loop. * feat(ci): fill partial bencher misses from a targeted base run fetch-main previously treated main.json as all-or-nothing: any name bencher lacked at the base SHA (typically constants the PR itself adds to Vectors.csv) silently rendered n/a. It now writes the uncovered subset to --missing-out and still exits 0; bench-pr runs the base checkout on JUST those names and merges under bencher's rows (bencher wins overlaps — it is the canonical main side), so a brand-new constant gets a real main-vs-PR delta on its first \!benchmark. The full-set base fallback (exit 3, SHA not ingested) is unchanged. * feat(ci): PR side cuts its own zisk shard manifest A PR can change the kernel's cost profile, so the env-sharded zisk run must not inherit main's partition. run.sh now cuts the manifest in-place (ix profile → ix shard) whenever one isn't already sitting next to the .ixe — the profiler counts heartbeats rather than wall time, so an unchanged tree re-partitions deterministically and per-shard comparisons stay meaningful. bench-main's compile-job manifest keeps pre-empting the generation on the main side; the \!benchmark PR side profiles its own tree (manifest cached per head SHA under bench-pr-ixes-*). The base fallback reuses bench-main's cached manifest and pays the env-sharded run only on a full bencher miss — a partial miss means bencher already holds main's env row (ZISK_ENV_SHARD=0 skips it). bench-pr benchmark timeout 120 → 180 min for the zisk cell's worst case (per-constant loop + profile + the env execute's own 60m cap). * feat(ci): per-shard execute-time and peak RAM in the zisk env row The shard breakdown carried cycles only. Each shard now also records its guest execute time (SDK-reported) and its RAM high-water — the texray sampler's peak is reset before every shard, so the windows are independent and the env row's execute-peak-rss becomes their max (the run's execution-phase high-water; setup RAM no longer counted). Uploaded as shard-time:<k> / shard-peak-rss:<k> alongside shard-cycles:<k>, all un-thresholded like phase:. No prove-side equivalent yet: zisk proving isn't wired up in CI at all (needs a GPU runner), so there is no prove-time for any zisk row. * feat(ix): compile --consts seed selection + `ix shard extract` subcommand Two ways to get a closure-only `.ixe` for one constant: - `ix compile <file.lean> --consts <n1,n2,…>` (+ --consts-file): seed the compile by exact constant name instead of the whole import env, with transitive deps via the existing collectDeps — same names vocabulary as `ix check --consts`. Mutually exclusive with --module. - `ix shard extract <env.ixe> --consts <n1,n2,…> --out <sub.ixe>`: the sharding pipeline's scoping step — cut the closure out of an EXISTING env without recompiling from source. The output carries the closure's genuine constant bytes, blobs, and reducibility hints (build_sub_env, now shared via sub_env_of), plus a name→address entry per closure constant so `--consts`-style tools still resolve. Metadata is dropped (real ConstantMeta references name addresses throughout its tree and would need the full hash-consed name index) — extracted envs serve the anon pipeline; meta-mode tools need the source env. A mutual-block member extracts its whole block. Verified against a fresh initStd.ixe: both forms produce envs whose bench-typecheck fft-cost is bit-identical to the full-env run (content addressing at work), and extract → ix profile → ix shard composes cleanly (Int8.instRxcHasSize_eq: 2.1 MB closure env, 16.08e9 steps → 11 shards at the 120 GiB cap). * feat(ci): closure-sharded zisk execute for heavy primaries Replaces the whole-env sharded run (wrong scope: all of InitStd is 1.94e12 steps / 1263 shards, and its biggest atomic block is INFEASIBLE under the cap) with per-constant closure sharding through the canonical pipeline. For each heavy-tier primary, run.sh runs `ix shard extract` (closure-only env, no recompile) → `ix profile` → `ix shard --max-ram 120`, then one `zisk-host --shard-plan --execute` run executes the shards sequentially — the constant's row carries totals plus the per-shard shard-{cycles,time,peak-rss}:<k> breakdown, uploaded to bencher like every other measure. Cheap primaries keep the single-leaf --consts run. - run.sh: cut_closure_shards (also exposed as the `cutshards` backend so bench-main's compile job pre-cuts through the same code path) + heavy-tier dispatch in the zisk loop (ZISK_HEAVY_NAMES). A constant whose partition still can't fit (atomic mutual block over the cap) OOMs under the RAM watchdog: honest OOM row, remaining shards skipped, loop proceeds to the next constant. Cutting failures fall back to the single-leaf run. - bench.py manifest --heavy-out: the selected heavy-tier names, from Vectors.csv's tier column. - bench-main: the compile job pre-cuts zkshards-<Bench>/ next to the fresh .ixe (it has ix + the toolchain; the zkvm job stays Lean-free) and ships it to the zkvm job in the sha-keyed bench-ixe-* cache entry. - bench-pr: the PR side cuts its own artifacts fresh every run (cheap — seconds per closure — and a PR can change the cost profile; profiling counts heartbeats, so an unchanged tree re-partitions deterministically); the base fallback reuses bench-main's pre-cut dir. * feat(bench): reject typecheck failures loudly — fail fast, ❌ row, red job A constant the kernel rejects is a correctness regression, not a benchmark datum. End to end: - zisk-host: every sharded loop (shard-plan execute + prove, whole-env execute + leaf prove) bails on the FIRST failing shard via the shared reject_failures helper — mirroring the OOM kill, which also cancels the constant's remaining shards — instead of accumulating failures across the full manifest. sp1 and the single-leaf paths already bailed immediately. - run.sh: a zkVM failure whose log carries the host's "kernel typecheck produced" abort records the neutral `{"failed": true}` sentinel (an ::error:: annotation, not a silent drop); ooc does the same when ##check## reports failures. bench-typecheck marks Phase-1 check errors failed and skips them in Phase 2. Failure warnings now print the log's head AND tail (the host's abort lands at the end of a mid-manifest log). - bench.py compare: `failed` renders ❌ cells (outranking OOM) plus a bold "FAILED TO TYPECHECK on the <side> side" note under the table; bmf strips the sentinel so rejected rows never reach bencher. - workflows: prove/zkvm/ooc jobs (bench-main) and the benchmark cell (bench-pr) exit nonzero when the neutral JSON carries a failed row — AFTER the clean rows upload / the table posts, so the red X lands on the commit/PR without losing the report. * test(ci): trigger bench-main on branch pushes (TEMPORARY) Drop this commit before merging. The zkVM build gate needs no branch trigger — it lives in ci.yml now and runs on pull_request. * feat(bench): ix bench orchestrator + neutral row contract; retire run.sh/bench.py One orchestrator, `ix bench`, now runs every benchmark cell locally and in CI, over a single tool contract with no output scraping: - crates/bench (ix-bench) + Ix/Benchmark/Neutral.lean: the neutral rows contract — { name: { status: ok|rejected|oom, ...metrics } }, flushed per name, with typed exit codes (0 ok / 2 usage / 3 kernel rejection). Hosts' duplicated helpers (write_json_entry, collect_consts, peak_rss_bytes) move here. - zisk-host/sp1-host: rejection writes the row (status: rejected) and exits 3 instead of an error string the harness had to grep. - ix check-rs --json: whole-env row, or per-name independently-timed closure rows (env loaded once) via an optional json path on the existing rs_kernel_check_anon_consts extern; ##check## markers removed. The triplicated env-load/name-resolution prefix in the FFI is now one loader. - ix compile --json: compile row; ##benchmark## marker removed. The displayed-name fallback no longer rescans the env per missing name. - bench-typecheck: status rows + exit 3; per-constant RSS windows (sampler reset per name) via a new texray reset binding. - ix bench run/compare/bmf/fetch-main/comment/matrix (Lean): manifest from Vectors.csv, spawn under .github/scripts/watchdog.sh (TERM→grace→KILL tree-RSS sidecar), resume loop marking a killed constant's row oom and continuing, zisk heavy-tier closure sharding, empty-rows-is-red gate, local baselines under .bench/ so a bare rerun compares against the previous run. compare renders the same Markdown table locally and in CI; bmf drops non-ok rows so rejected/OOM constants never reach bencher; fetch-main keeps the newest report at a SHA (was oldest-wins). - Benchmarks/bench-config.json: single registry (env slugs/modules, backends, testbeds, modes). Workflow matrices are generated from it (ix bench matrix), the \!benchmark parser reads it, thresholds-reset derives its workload lists from it. - Workflows: every measurement step is one `ix bench run` + `ix bench bmf`; the four copy-pasted jq typecheck gates are gone (exit codes redden the step); run.sh deleted; bench.py reduced to the pre-build comment parser. bench-pr's base side runs only the names bencher lacked (--names-file). - No per-constant timeouts: job-level timeout-minutes is the only clock. zisk-host/sp1-host compile is validated by ci.yml's zkvm build gates (their toolchains aren't available locally). * test(ci): TEMPORARY triggers to exercise the bench workflows from this branch Revert before merge (every hunk is marked TEMPORARY): - bench-main.yml runs on pushes to sb/ci-benchmarks, not just main. - bench-pr.yml also runs on pull_request (head-ref gated to this branch): a push to the branch's open PR fires `synchronize`, whose payload carries the base/head SHAs and PR number that issue_comment needs an action to look up. pull_request runs use a fixed cheap command (`\!benchmark ooc compile`) so every push exercises fetch-main → run → compare → comment end to end and posts the table on the PR. * refactor(bench): drop the "neutral" vocabulary for the results format "Neutral" described what the format isn't (backend-specific) rather than what it is. The shared per-constant results file is now just the "benchmark results JSON" / "results rows", and the Lean module moves accordingly: Ix/Benchmark/Neutral.lean → Ix/Benchmark/Results.lean (namespace Ix.Benchmark.Results). Comments, CLI help text, and docs updated to match; no behavioral change. * fix(ci): isolate the App token from PR-derived code in bench-pr CodeQL flagged the comment job (untrusted checkout TOCTOU + untrusted code execution in a privileged issue_comment workflow): it checked out the PR head and ran the PR-built `ix bench comment` in the same job that later mints the GitHub App token, so a malicious commit — including one force-pushed after the \!benchmark authorization — could hijack the job and reach the token. Split it: an unprivileged `assemble` job (contents: read, no secrets) checks out the PR and runs `ix bench comment`, uploading the finished body as an artifact; the `comment` job keeps the token but now performs no checkout and runs no repo-derived code — artifact download, token mint, post. Untrusted checkouts in the build/benchmark/assemble jobs also stop persisting the workflow token in .git. * fix(ci): passthrough-env step failed on every cell (heredoc terminator) The step interpolated the passthrough lines into a quoted heredoc inside a YAML block scalar: the indentation put the PTENV terminator off column 0, so bash never found it, swallowed the stray lines, and the loop's final [ -n ] test made the step exit 1 — on every cell, since the passthrough is usually empty. Deliver the lines via an env var and filter blanks with sed (exit 0 either way). This also removes inline ${{ }} interpolation from the script body. * feat(bench): announce each constant before its execute/prove A watchdog kill or OOM mid-prove left no way to tell which constant was in flight — bench-typecheck printed a constant's line only after it finished. Both phases now print a flushed `[i/N] proving <name> (fft-cost=…)` line first, so the crash site is always named in the log (and matches the row `ix bench run` marks oom). * fix(bench): don't relabel deterministic tool failures as per-constant OOM The first \!benchmark run on the transition PR rendered every main-side ooc row as OOM: bencher had no base data, the fallback ran main's ix — which predates --json — and each spawn died instantly with a usage error. The resume loop read every death as a kill of the in-flight constant, poisoning all 18 names one spawn at a time. Only a killed tool (exit ≥ 128: watchdog TERM/KILL or the kernel OOM killer) now implicates the in-flight constant; any other nonzero exit is deterministic and aborts the remaining names loudly. compare gains the matching one-side-empty note ("main produced no results — often a CLI-incompatible base binary") instead of a silent all-n/a column. * refactor(bench): one-line side-failure notes in the compare table The two-sentence diagnosis repeated per failing cell was noise; the workflow logs carry the why. * feat(bench): track peak RSS on the compile cell Every other backend reports its RAM high-water; compile didn't only because the old marker line never carried one. Window the tree-RSS sampler around the serialize step (the loaded Lean env stays in the baseline — RSS is absolute) and add peak-rss to the compile metrics. * refactor(bench): render file-size as env-size in the compare table The JSON key / bencher measure slug stays file-size (renaming would orphan its threshold and history; bencher plots it as "Environment Size") — only the table column label changes. * refactor(bench): cutshards backend → `ix bench shard` subcommand It measures nothing and emits no rows, so modeling it as a backend forced a dummy registry entry (enabled: false, no testbed) into bench-config.json. As a sibling of `run` the pseudo-entry disappears and the name reads as what it does. * feat(bench): execute-side throughput + surface both Aiur RAM peaks The execute and prove RAM high-waters were already measured in separate sampler windows (execute-peak-rss before any proving allocations, peak-rss per prove), but the prove table only displayed the prove peak — execute-peak-rss now joins the prove-mode columns. bench-typecheck also records execute-throughput (closure constants/sec over Phase 1, the witness-generation analog of the proving throughput), rendered higher-is-better like its prove-side counterpart. * refactor(bench): drop the compile mode - the compile backend runs as execute Three mode tokens for two real behaviors: only aiur distinguishes prove/execute, so a third mode existing solely to label the compile backend's single behavior was registry noise. Its metrics key and default_mode move to execute; cell labels/baselines become compile-<env>-execute. * refactor(bench): rename the prove-phase peak to prove-peak-rss With execute-peak-rss now beside it in the prove table, a bare peak-rss was ambiguous. The rename covers everywhere the value is a prove-phase high-water: bench-typecheck rows, both zkVM hosts' prove paths, and the aiur prove columns. ooc and compile keep plain peak-rss — their single phase leaves nothing to disambiguate. Fresh bencher measure; the old peak-rss series on the aiur testbed is orphaned (pipeline is new, no meaningful history lost). * refactor(bench): bare peak-rss everywhere, phases separated by testbed Revert the prove-peak-rss/execute-peak-rss/execute-throughput naming: metric names stay simple and phase scoping moves to the storage layer. The aiur backend's two modes become two cells on their own bencher testbeds (aiur-execute-* / aiur-prove-*, replacing aiur-check-*): an execute row carries the Phase-1 peak-rss and constants/sec throughput, a prove row the prover's peak and constants/prove-sec — shared names, no collision, because the modes never share a row or a testbed. bench-main gains the aiur execute cell (mode joins the matrix); bench-config testbeds may now be per-mode objects (fetch-main and the thresholds-reset jq handle both shapes). zisk/sp1 rows return to bare peak-rss, and throughput's cross-backend unit reuse stays as is. Also: integer columns render with thousands separators (105,492). * feat(bench): aiur execute-only is local-only; CI uploads the prove run The prove run simulates the real workload and measures Phase 1 (execute-time, fft-cost) inside the same process en route, so a separate CI execute cell added runtime without adding signal. bench-main's aiur job is back to a single prove cell per env (testbed/workload aiur-prove); the standalone-execute testbed and per-mode testbed objects are gone (config testbeds are plain strings again); the \!benchmark `execute` token is removed from the grammar. `ix bench run --backend aiur --mode execute` remains as a fast local dev loop with .bench/ baselines — it just never reaches bencher or the PR comment. * feat(bench): restore the \!benchmark execute token `\!benchmark aiur execute` runs the Phase-1-only cell on a PR again. PR cells never upload to bencher, so the only correctness wrinkle is the main side: bencher stores each backend's DEFAULT mode only, and the shared measure names (peak-rss, throughput) mean that mode's phase — fetch-main now exits 3 for any non-default mode, so an execute cell's main side is always measured fresh on the base checkout instead of misreading prove-phase numbers as execute-phase ones. * feat(bench): bench-main runs aiur execute and prove as separate cells Both modes upload to their own testbeds (aiur-execute-* / aiur-prove-*), so a \!benchmark aiur cell of either kind always finds a cached main-side baseline on bencher — no base-checkout fallback for the execute mode (the previous non-default-mode guard in fetch-main is gone; per-mode testbed objects return to the config, and the thresholds-reset jq handles both shapes again). Costs one extra Phase-1 run per env per main push; measure names stay bare, phase-scoped by the cell. * fix(ci): concise matrix job names Without an explicit name, GitHub appends every matrix value to the job title — the PR benchmark cell showed backend, env, slug, mode, runner, AND the label (which alone is the cell id). Name the matrix jobs from their cell coordinates: <backend>-<env>[-<mode>]. * refactor(bench): aiur testbeds keep the subject word — aiur-check-{prove,execute} The suite's testbeds name what they measure (zisk-check, ooc-check); aiur-prove/aiur-execute dropped the subject. Both cells benchmark the kernel typecheck — prove/execute are modes of it — so the testbeds are now aiur-check-prove-x64-32x / aiur-check-execute-x64-32x (workloads aiur-check-prove / aiur-check-execute). History migration (before the next push of this branch): rename bencher testbed aiur-typecheck-x64-32x -> aiur-check-prove-x64-32x, and copy the reset tag: bencher-thresholds-reset-aiur -> the same commit tagged as bencher-thresholds-reset-aiur-check-prove. * refactor(bench): drop the BENCH_TIER PR knob; render peak-rss as peak-ram BENCH_TIER was a four-hop plumbing chain (parse → output → env → --tier) whose default is a no-op: the tier column's real consumers — zisk's heavy-shard routing and the prove --full cheap default — read Vectors.csv inside `ix bench run`, which keeps --tier for local use. An unknown BENCH_TIER= line in a comment now just falls off the allowlist. Vectors.csv's header also catches up with the ix bench era. peak-rss renders as peak-ram in compare tables (display only, like env-size — the bencher measure slug is unchanged). * refactor(bench): one env spelling — InitStd everywhere Collapse the env-key/slug pair (initStd/InitStd) inherited from run.sh's benv/benv_cc split. The TitleCase name is now the single identifier: the registry key, the \!benchmark token (matched case-insensitively), the `ix bench run --env` value, the `<env>.ixe` filename, the zkshards-<env> dir, the cache-key suffix, the cell label, and the env-keyed bencher benchmark name. The registry drops the slug field, matrix cells drop the slug member, EnvInfo loses its slug, and Vectors.csv's env column is TitleCase. Cache paths change spelling but keys are SHA-scoped, so no migration. * fix(bench): satisfy clippy without allows cast_precision_loss on the per-name throughput: convert the closure count through u32 (exact in f64) instead of a raw usize cast. The exit-code constants become u8 — ExitCode::from is their only numeric consumer, which also drops the hosts' `as u8` casts. * feat(bench): print throughput + peak RAM on bench-typecheck's log lines The rows always carried them; the per-constant console lines only showed constants/fft-cost/execute (and the prove line omitted its peak), so a reader scanning the CI log saw neither. * refactor(bench): shared instrumentation for aiur execute metrics Supersedes the ad-hoc per-line arithmetic from the previous commit: - The standalone execute FFI entries (dispatch_execute / rs_aiur_toplevel_execute_ixvm) now carry the same aiur/execute_ixvm span the prove pipeline emits, so Phase-1 duration and RAM Δ/peak stream through the one texray channel — and land in <json>.spans — instead of being computed per benchmark. - bench-typecheck installs the texray subscriber before Phase 1 (bare --texray previously deferred it to the prove phase). - The per-constant console line formats throughput via the benchmark framework's Throughput.formatRate; the hand-rolled rate and GiB math is gone. * feat(bench): one process per constant; span timings become phase:* measures Per-constant backends (aiur, zkVM) now spawn one tool process per constant, like the original run.sh granularity: a kill costs exactly that constant (row marked oom, keeping whatever the tool flushed) and the resume loop's first-missing-row inference is deleted. The payoff is span attribution for free — each spawn truncates <out>.spans at startup, so after it exits the file IS that constant's window; ix bench run folds it into the row as flat phase: fields (aiur tracing spans and the zkVM hosts' record_manual entries alike, no tool changes). The flat keys pass through bmf untouched as independent bencher measures (witness gen, stage commits, quotient, ... each get a trend line) and come back from fetch-main in the same shape; compare renders them as a collapsible per-constant drill-down after the main table. bench-typecheck switches from whole-file rewrites to the shared merge-style row writes (Results.writeEntry) so per-constant processes can share one results file. ooc keeps its single multi-name process: the check-rs rows mode already attributes per name with the env loaded once, and out-of-circuit checks don't approach the RAM ceiling. * feat(bench): nest each constant's phase table in its own drop-down One collapsed drill-down per cell, one collapsible entry per constant inside it — 17 constants no longer expand into one wall of tables. * feat(bench): per-constant phase drop-downs directly under the main table The main table keeps every constant's high-level row; each constant with phase data gets its own top-level collapsed mini-table, opened individually — no outer wrapper to expand first. * fix(bench): verified review findings — panic strategy, gate completeness, atomic rows 1. zisk host workspace drops panic="abort": with it, every deterministic panic (e.g. a missing .ixe expect) exits SIGABRT=134, which runPerConstant reads as an OOM kill — a broken host became a green cell of all-oom rows with an empty upload. Unwinding panics exit 101 and hit the loud abort path; SIGABRT stays reserved for real allocation-failure OOMs. (sp1-host already unwound; guests keep their own profiles in their excluded workspaces.) 2. The gate now checks COMPLETENESS, not just emptiness: every selected name (plus the env-keyed row for ooc/compile) owes exactly one row, so an aborted loop, a killed ooc batch, or a dropped whole-env check exits 1 instead of shipping a quietly partial green cell. 3. Row writes are atomic (temp + rename) on both sides — Lean writeEntry (markOom/mergeSpans now route through it) and Rust write_json_entry. A KILL mid-write previously truncated the shared accumulator, which the tolerant readers silently reset to {}, losing every prior row. 4. A watchdog kill during teardown (row already carries the mode's completion metric, e.g. prove-time — the prover releasing tens of GB right after the final write) no longer relabels the finished row oom and out of the upload. Plus dead nested-phases vocabulary: bmf's phases special case, the row-shape docs, and the stale drill-down bullet all catch up with the flat phase: keys. * chore(zisk): drop the panic-strategy comment * fix(ci): create-github-app-token deprecated app-id in favor of client-id The input accepts the numeric App ID as well (the JWT issuer claim takes either), so the TOKEN_APP_ID secret is unchanged. * refactor(bench): registry as Lean code — bench-config.json and bench.py deleted The JSON registry existed to share env/backend data across three runtimes: ix bench (Lean), the pre-build Python comment parser, and the thresholds-reset jq. Eliminate the other two consumers and the file has no reason to exist: - The registry is now typed Lean data (envSpecs/backendSpecs in Ix/Cli/BenchCmd.lean) — one language, one owner, and the getObjVal? chains in run/shard/compare/fetch-main/matrix collapse into struct lookups. The --config flags disappear. - \!benchmark parsing moves into `ix bench parse` (COMMENT_BODY → GITHUB_OUTPUT, same allowlist grammar), run at the end of bench-pr's build job right after the ix binary exists; the setup job keeps only the authorization gate and SHA resolution, and the matrix/config outputs move to the build job. The last Python is gone. - bencher-thresholds-reset keeps static workload lists with a sync note pointing at backendSpecs — it runs on cheap runners with no built ix, and its dispatch options were already forced static by GitHub. * refactor(bench): local-first CLI — parse previews, comment becomes report The ix bench surface should be generic CLI infra that CI merely calls, not CI infra that happens to be a CLI: - `parse` takes the command via --comment (a local dry-run preview of which cells a \!benchmark schedules), falling back to the COMMENT_BODY env var; the Actions-format machine outputs are written only when $GITHUB_OUTPUT is set instead of spilling to stdout. - `comment` → `report`: assemble per-cell tables into one Markdown report, readable locally with zero flags; the commit/logs links only render when the PR workflow passes --head/--repo-url/--run-id, and --out is optional (always printed). * refactor(bench): group the CI adapters under ix bench ci parse and matrix exist for the workflows; the top-level listing now reads as the local tools plus one clearly-labeled ci namespace. * docs(bench): full accuracy pass on the benchmarking docs - gate guarantee stated correctly: every selected name owes a row (not just non-empty), so a partial cell can't be green - bench-pr shape caught up with the parse move (setup only authorizes and resolves SHAs; build ends with ix bench ci parse) and the assemble/comment privilege split - watchdog section covers the teardown-kill exception and the single-process ooc/compile cells - grammar adds the sp1 token and enumerates the passthrough allowlist - local usage gains a single-constant aiur walkthrough and the fetch-main flow for comparing a local run against main's bencher data - README benchmark section links here instead of just the bencher plots * refactor(bench): CI data out of the generic registry benchRunner was a runs-on matrix field only ix bench ci parse consumes — it moves next to the ci adapters as ciRunner. The 120 GB default ceiling was really "the CI runner's 128 GB minus headroom" posing as a universal constant; defaultCeilingGb now derives from the machine's own RAM (/proc/meminfo MemTotal minus 8 GiB, floor 8, conservative 16 when unreadable), so CI lands where it always did and a workstation gets a ceiling that actually protects it. * fix(bench): baselines move to the framework's .lake/benches root .bench/ duplicated an existing convention: Ix.Benchmark already writes all benchmark output under BENCH_OUTPUT_DIR (default .lake/benches). ix bench saveBaseline and compare now share that root — one output convention, and baselines stop polluting git status. * fix(bench): watchdog must never lose the race to the runner The bitblast prove OOM took the whole job down ("The operation was canceled"): tree-RSS was 7 GB past the 120 GB ceiling before the 3s sampler saw it, and the fixed 10s TERM grace let the prover keep allocating until the VM thrashed, the runner agent missed its heartbeat, and GitHub canceled the job before any kill landed. - sample every 1s instead of 3s (the breach is seen ~GBs earlier) - the grace only continues while the tree is BELOW the ceiling: still at/above it after TERM means still allocating -> KILL immediately. Rows are flushed as tools go, so nothing of value needs the grace. - default ceiling headroom widens to MemTotal minus 12 GiB (the 128 GiB runner lands at 116): it must absorb ~two sampling periods of allocation past the ceiling plus the OS and runner agent. Verified live: a 2 GB allocation under a 1 GB ceiling gets TERM'd and exits 143 within a second. * fix(ci): derive the benched-env gate from the registry The compile job's shard-cut and cache-save conditionals hand-copied 'InitStd || Mathlib'; a step now asks the in-job ix (ci matrix --kind envs) whether matrix.env is benched, so adding a benched env is a registry-only change. * fix(bench): per-shard data uploads as benchmarks, not one measure per index toBmf flattened nested shard breakdowns to shard-cycles:0, shard-cycles:1, ... — a new bencher MEASURE per shard index, spamming the measure list with dozens of dynamically-named entries. Multiplicity belongs in the benchmark-name dimension: each shard now uploads as <name>/shard-<idx> sharing the parent row's measure slugs (cycles, execute-time, peak-rss). The rows JSON keeps its nested shape; only the bencher projection changes. * fix(ci): threshold the compile cell's peak-rss peak-rss joined the compile metrics but never its thresholds list, so bencher warned 'No Threshold found' and the measure could never alert. Same 10% upper bound as the other cells' peak-rss. * fix(bench): enforce the RAM ceiling with RLIMIT_DATA, sampler as backstop The aiur prove OOM still took the runner down: tree-RSS was 13 GB past the ceiling at the FIRST sample after the breach — the prover's commit phases allocate multiple GB/s across 32 threads, faster than any sampling cadence can react. Sampling-based kills fundamentally lose that race; by the time the sampler sees the spike the VM is thrashing and GitHub cancels the job before the TERM lands. watchdog.sh now sets RLIMIT_DATA to the ceiling on the spawned command: the allocation that would cross the line fails inside the process, and Rust's handle_alloc_error / Lean's OOM panic abort on the spot (SIGABRT = 134 ≥ 128 → oom row) with zero overshoot. The tree-RSS sampler stays as the backstop for what a per-process limit can't see: the sum across Zisk's ASM microservice tree. Verified: a 2 GB allocation under a 1 GB ceiling now fails in-process instantly (no TERM path), normal commands unaffected. * fix(bench): never upload an empty BMF report A cell whose rows all end oom/rejected — or that failed before producing rows — left bmf writing {} and the \!cancelled() upload step sending it to bencher, which rejects it as 'No benchmarks found'. bmf now exits 1 when zero benchmarks survive the non-ok filter, and the bencher-track steps gate on the bmf step's outcome as well as \!cancelled(): clean rows still upload past an exit-3 run, but an empty report skips the upload instead of failing it. * fix(bench): absolute watchdog path; exec failure is not an OOM The zisk cell's empty bencher upload traced to a broken spawn, not a benchmark: the hosts run with the zisk/ workspace as cwd, where the repo-relative ./.github/scripts/watchdog.sh fails to exec. Lean reports that as exit 255, which runPerConstant read as a kill — both constants got fake oom rows, the completeness gate saw every row present and passed, and bmf stripped the non-ok rows down to {}. The watchdog path is now resolved to an absolute path before any spawn, and exit 255 (never a signal death; our kills are 134/137/143) aborts the cell loudly instead of minting oom rows. * fix(ci): say where the main side actually came from in the table title The fetch-main exit-3 case wrote the literal 'source=ran', rendering as 'main from: ran'. All three cases now name the source and base SHA: 'bencher @ <sha7>', 'bencher @ <sha7> + base run (N new)', or 'base run @ <sha7> (not on bencher)'. * fix(bench): only annotate the mode for multi-mode backends in the summary 'ooc=execute compile=execute' implied a choice that doesn't exist; single-mode backends now print bare, aiur keeps aiur=prove/execute. * fix(bench): drop the mode from single-mode cells' table titles Same rule as the config summary: 'compile · InitStd · execute' names a mode nobody chose; aiur keeps its prove/execute segment. * fix(bench): fixed 120 GB default ceiling; RLIMIT_DATA stays everywhere The Mathlib compile hit the MemTotal-derived 111 GB ceiling with room to spare in physical RAM: RLIMIT_DATA caps virtual data mappings, and Lean's allocator reserves well beyond true RSS, so the derived value was too tight for the biggest legitimate workload. Rather than per-backend enforcement modes, keep one simple rule: the rlimit works, set it to a flat 120 GB (what the sampler ceiling always was) and let --ceiling-gb override on smaller machines. * feat(bench): cgroup memory.max as the watchdog's primary enforcement The kernel primitive both prior layers approximated: memory.max caps the tree's RESIDENT memory and (with memory.oom.group) OOM-kills the whole group atomically at the ceiling, exiting 137 — no sampling race for the prover's GB/s bursts, no virtual-memory false trips for Lean's allocator slack (only actual pages are charged), and Zisk's ASM microservices sum into the same budget. Used when cgroup v2 and passwordless sudo are available (the CI runners); otherwise the RLIMIT_DATA + tree-RSS-sampler fallback remains for local runs, with a log line naming the active mode. * feat(bench): cgroup-only watchdog — no fallback, fail loudly The RLIMIT_DATA + tree-RSS-sampler fallback is gone: a run whose ceiling cannot be enforced is not a benchmark run. watchdog.sh now requires cgroup v2 + passwordless sudo and exits 2 with a plain reason otherwise; ix bench run likewise hard-fails when the watchdog script is missing instead of running unguarded. The sampler machinery (tree_pids/tree_rss_kb/TERM-grace loop) is deleted with it. * fix(bench): sampler-only watchdog with adaptive cadence Revert the cgroup mode (and the earlier RLIMIT_DATA layer): back to the plain tree-RSS sampler, sudo-free and identical everywhere. The burst problem is handled by cadence instead of a kernel cap: sampling drops from ~1s to 0.2s once the tree is within 20 GB of the ceiling (100 GB at the default 120), and the post-TERM grace re-checks every 0.2s, KILLing immediately while the tree is still at the ceiling. Worst-case overshoot shrinks from GB-per-second x seconds to x ~0.4s. ix bench run still hard-fails when the watchdog script is missing — an unenforced ceiling is not a benchmark run. * fix(bench): restore the RAM-derived default ceiling The flat 120 was a leftover from the RLIMIT_DATA era (a VA cap needed fixed slack above RSS); for the sampler it protects nothing on machines with less RAM and leaves ~3 GB of headroom on the 123 GiB runner. Back to MemTotal minus 12 GiB (runner: 111; 64 GiB workstation: 52), which the adaptive fast-cadence zone sits under wherever the run happens. * refactor(bench): zkvm testbeds gain the mode suffix (zisk-check-execute) Same lesson aiur taught: shared measure names (peak-rss, throughput) mean that mode's phase, so a future zisk/sp1 prove mode needs its own testbed — and an unsuffixed zisk-check silently meaning "execute only" is the asymmetry we just cleaned up for aiur. Renaming now rides the merge's existing bencher migration (console rename + reset-all) instead of paying a second cycle later. The zkvm job derives testbed/workload from the cell's mode, so a prove cell would land on zisk-check-prove-x64-32x with no workflow edits. * feat(ci): bench-pr prepare stage — compile ea…

arthurpaulino · 2026-07-01T11:19:05Z