wai-formal-verification: two proof shards that had outgrown where they ran #602

Merged

dcharlot merged 2 commits from ci/proof-shards-to-96 into main 2026-11-03 14:38:55 -05:00

Conversation 0 Commits 2 Files changed 1 +33 -12

2026-11-03

Transaction Science

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 <[email protected]>

ebe9985a82

• View at this point in history

2026-11-03 11:20:39 -05:00

Transaction Science

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 <[email protected]>

8f0080d4ed

• View at this point in history

2026-11-03 07:38:57 -05:00