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

dcharlot commented 2026-11-03 07:39:15 -05:00

Owner

Copy link

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]

🤖 Generated with Claude Code

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]> 🤖 Generated with [Claude Code](https://claude.com/claude-code)

dcharlot added 1 commit 2026-11-03 07:39:15 -05:00

wai-formal-verification: two proof shards that had outgrown where they ran ... 8f0080d4ed

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]>

dcharlot added 1 commit 2026-11-03 11:20:46 -05:00

wai-formal-verification: the Kani cache would have overwritten the second macOS host's install ... ebe9985a82

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]>

dcharlot merged commit d1cb7a289b into main 2026-11-03 14:38:55 -05:00

dcharlot referenced this pull request from a commit 2026-11-03 14:38:56 -05:00

Merge pull request 'wai-formal-verification: two proof shards that had outgrown where they ran' (#602) from ci/proof-shards-to-96 into main

dcharlot referenced this pull request 2026-11-03 15:21:06 -05:00

CI: the gate that decides whether a workflow runs was queued behind the work it gates #603

dcharlot referenced this pull request 2026-11-03 15:21:26 -05:00

CI: the gate that decides whether a workflow runs was queued behind the work it gates #598

Sign in to join this conversation.

Reviewers

No reviewers

Labels

Clear labels

No items

No labels

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

1 participant

Notifications

Subscribe

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference

Transaction-Science/open-standards!602

No description provided.