.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:
@@ -178,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: |