From 8f0080d4ed6f476c9b1d9f578207018d94b355b7 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Tue, 3 Nov 2026 07:38:57 -0500 Subject: [PATCH 1/2] wai-formal-verification: two proof shards that had outgrown where they ran A model checker that runs out of time has refuted nothing and proved nothing. It is the one failure mode a proof gate must not reach by accident, and this workflow reached it: `kani (isqrt512)` failed after **1 h 59 m 46 s** against its own 120-minute budget, on a `linux` runner with 15 GiB shared by two jobs. The workflow already recorded this failure for a sibling shard, in the comment above its own matrix: the rans64 totality proof (k26) peaks near 28 GiB, CBMC ran out of memory on `linux`, and it was given a shard of its own on `macos`. What that comment then claimed -- "every other shard has run to completion on the linux runner" -- is what `isqrt512` has now falsified. The same box, the same cause, a different symptom: an allocation error the first time, a timeout the second. And the destination of the first move has since become the fleet's most contended host. `macos` is served by a Mac Studio carrying two CI labels, an inference server and a 30-process simulation sweep, measured at **load 185 on 32 cores**. A 28 GiB harness and a two-hour budget are precisely the workloads that die first there. Both shards move to `macos-proofs`: a 28-core, 96 GB Mac Studio measured at load ~6, with a runner of capacity 1 so a harness never shares the machine. The label is deliberately narrow, and that is the point. That host has the Command Line Tools but no full Xcode, no Metal compiler, no node, no Playwright browsers and no Java. Several hosts already answer the general `macos` label with different provisioning, which is how a missing tool arrives as what looks like a code failure. `macos-proofs` promises only what the box has -- rustup, git, curl, cores and memory -- and these shards install their own prover and cache it. Also moved, one line: this workflow's `does this change touch it` gate, from `linux-arm64` to `linux`. Every job here declares that gate in `needs`, so on `linux-arm64` it waits behind the queue it is rationing -- which would have left this change unable to verify itself. #598 makes the same move for all 55 gates; the two diffs are identical on this line. What this does not claim: that the proofs are faster, or that the timeout was a proof problem. Nothing about the harnesses changed. They are being given a machine where the measured budget is the one they were written against. Co-Authored-By: Claude Opus 5 --- .github/workflows/wai-formal-verification.yml | 34 ++++++++++++++----- 1 file changed, 26 insertions(+), 8 deletions(-) diff --git a/.github/workflows/wai-formal-verification.yml b/.github/workflows/wai-formal-verification.yml index 957e23457..89ff750e6 100644 --- a/.github/workflows/wai-formal-verification.yml +++ b/.github/workflows/wai-formal-verification.yml @@ -95,7 +95,7 @@ jobs: # `true` (scripts/pr-touches-paths.py). relevant: name: does this change touch it - runs-on: linux-arm64 + runs-on: linux outputs: run: ${{ steps.gate.outputs.run }} steps: @@ -144,19 +144,37 @@ jobs: # isqrt harnesses and the longest stage harnesses have shards of their own. # Harnesses gated by cfg(kani_open) are not compiled here. # - # Each shard runs where its memory fits. The rans64 totality proof (k26) peaks at - # about 28 GiB of resident memory and takes about 690 s of verification (measured - # with /usr/bin/time -l on a 256 GB host); the linux runner has 15 GiB, shared by - # two jobs, and CBMC ran out of memory there. It has a shard of its own on the - # macos runner. Every other shard has run to completion on the linux runner. + # Each shard runs where its memory fits, and two of them no longer fit the + # general runners. + # + # The rans64 totality proof (k26) peaks at about 28 GiB of resident memory and + # takes about 690 s of verification (measured with /usr/bin/time -l on a 256 GB + # host). The `linux` runners have 15 GiB shared by two jobs, and CBMC ran out of + # memory there, so it was moved to `macos` -- which is a host carrying two CI + # labels, an inference server and a simulation sweep, and was measured at load + # 185 on 32 cores. + # + # `isqrt512` then began failing on `linux` the same way, but as a timeout rather + # than an allocation error: 1 h 59 m 46 s against this job's 120-minute budget. A + # model checker that runs out of time has refuted nothing and proved nothing, so + # it is the one failure mode a proof gate must not reach by accident. + # + # Both now run on `macos-proofs`: a 28-core, 96 GB Mac Studio at load ~6, with a + # runner of capacity 1 so a harness never shares the box with another. The label + # is deliberately narrow -- that host has the Command Line Tools but no full + # Xcode, Metal, node, browsers or Java, so it must not answer the general `macos` + # label, where a missing tool reads as a code failure. It has rustup, and these + # shards install their own prover. + # + # Every other shard has run to completion on the linux runners. matrix: include: - { shard: integer-core, os: linux, harness: "rans:: int_entropy:: int_transform:: wai_video_policy:: staged_predict:: staged_wir1_arith::" } - { shard: arith, os: linux, harness: "proofs::arith::k01 proofs::arith::k03 proofs::arith::k13_isqrt_u128 proofs::arith::k17 proofs::arith::k32 proofs::limb::" } - - { shard: isqrt512, os: linux, harness: "proofs::arith::k13_isqrt_i512 proofs::arith::k13_isqrt_ceil_i512" } + - { shard: isqrt512, os: macos-proofs, harness: "proofs::arith::k13_isqrt_i512 proofs::arith::k13_isqrt_ceil_i512" } - { shard: stage, os: linux, harness: "proofs::stage::k23 proofs::stage::k27 proofs::stage::k28 proofs::stage::k29_residual_step_32bit_identity_registered proofs::stage::k30 proofs::stage::e11 proofs::stage::e12" } - { shard: stage-long, os: linux, harness: "proofs::stage::k29_residual_step_32bit_identity_every_range" } - - { shard: rans64-t2, os: macos, harness: "proofs::stage::k26" } + - { shard: rans64-t2, os: macos-proofs, harness: "proofs::stage::k26" } - { shard: sound, os: linux, harness: "proofs::sound::" } - { shard: plan, os: linux, harness: "proofs::plan::" } steps: -- 2.54.0 (Apple Git-157) From ebe9985a826bc91fbd11b575244013d3b2aee25e Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Tue, 3 Nov 2026 11:20:39 -0500 Subject: [PATCH 2/2] wai-formal-verification: the Kani cache would have overwritten the second macOS host's install The move to `macos-proofs` left a condition behind. `Cache Kani toolchain` was skipped by `matrix.os != 'macos'`, and the comment above it gives the reason: those runners execute on the host, so `~` is the host's own home, where Kani is already installed, and a restore writes over a live install. `macos-proofs` is a second such host, and `!= 'macos'` is false for it, so the step would have run there -- and `runner.os` is `macOS` on both, so the two hosts would also have been sharing one cache key, each saving its own install over the other's. The test is now a prefix, `!startsWith(matrix.os, 'macos')`, which is what the comment always meant. Kani 0.67.0 is installed on that host: `cargo-kani 0.67.0`, with `~/.kani/kani-0.67.0/bin/kani-driver`, `bin/cbmc` and `toolchain/bin/rustc` all present, which is exactly the three-way test the `Install Kani` step skips on. So the shards find a prover and do not fetch one. Two things this run will also test that the last one could not, because it never reached a step: the proofs host's own provisioning, and whether these harnesses fit its 96 GB. Co-Authored-By: Claude Opus 5 --- .github/workflows/wai-formal-verification.yml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/.github/workflows/wai-formal-verification.yml b/.github/workflows/wai-formal-verification.yml index 89ff750e6..ab7f99bd3 100644 --- a/.github/workflows/wai-formal-verification.yml +++ b/.github/workflows/wai-formal-verification.yml @@ -196,11 +196,14 @@ jobs: echo "$HOME/.cargo/bin" >> "$GITHUB_PATH" # Kani ships its own pinned nightly and a CBMC build; both are slow to - # fetch, so they are cached on the verifier version. Not on macOS: that - # runner's home is the host's own, where Kani is installed, and a restore - # would write over a live install. + # fetch, so they are cached on the verifier version. Not on either macOS + # label: those runners execute on the host, so `~` is the host's own home, + # where Kani is installed, and a restore would write over a live install. + # The test is a prefix, not `!= 'macos'`, because `macos-proofs` is a second + # such host -- and `runner.os` is `macOS` for both, so one key would also + # have them overwriting each other's. - name: Cache Kani toolchain - if: matrix.os != 'macos' + if: ${{ !startsWith(matrix.os, 'macos') }} uses: actions/cache@v4 with: path: | -- 2.54.0 (Apple Git-157)