standards-build: the proof gate turned a verified proof into a failure #599

Merged

dcharlot merged 2 commits from ci/proof-gate-sigpipe into main 2026-11-03 15:17:18 -05:00

Conversation 0 Commits 2 Files changed 1 +8 -3

2026-11-03

Transaction Science

standards-build: the plan job decided what to build from the longest queue ...

`plan` is the job every other leg of this workflow declares in `needs` -- it
runs `scripts/standards-touched.py` and emits the matrix. It ran on
`linux-arm64`, which is the label the fleet cannot spare: measured while this
was queued, `linux-arm64` was 282 runs deep and `linux` was idle on a 20-core
host. So the small job that decides what to build waited behind the heavy jobs
it was deciding about, and every leg of the build waited on it.

It is pure Python over a git diff and needs no particular architecture, so it
moves to `linux`.

This is one line of the same fix #598 applies to all 55 path gates in the
repository, taken here because the proof-gate fix in this pull request cannot
land without it: that fix unblocks every branch whose proofs leg currently
turns a verified proof into a failure, and it was itself sitting behind the
queue it needs to clear. #598 remains the general change; the two diffs are
identical on this line and merge as one.

Co-Authored-By: Claude Opus 5 <[email protected]>

0efe3e6569

• View at this point in history

2026-11-03 06:40:53 -05:00

Transaction Science

standards-build: the proof gate turned a verified proof into a failure ...

The gate read:

    echo "$out" | grep -q '^VERIFICATION:- SUCCESSFUL' || { ...; exit 1; }

under `set -o pipefail`. `grep -q` exits at its first match, `echo` then dies of
SIGPIPE (141), and pipefail promotes that to the pipeline's status -- so **a
found match becomes a failure**. Whether it bites is a race on how much of
`$out` fits the pipe buffer, which makes it a function of the harness's output
size, not of the proof.

Caught live on #598, whose branch does not carry this fix:

    == widening_a_set_can_only_lower_its_cap ==
     ** 0 of 336 failed (1 unreachable)
     ** 4 of 4 cover properties satisfied
    VERIFICATION:- SUCCESSFUL
    widening_a_set_can_only_lower_its_cap did not verify

The proof verified and the gate said it did not. The 15-property harness
immediately above it passed in the same run, which is the size dependence
showing itself directly.

It was previously measured at about 1 in 20 against a 191 KB output, and that
rate is now known to be the wrong way to describe it: at 336 properties it is
not intermittent, it is reliable. So this is a gate that became *less* reliable
as the thing it guards grew -- the failure mode a proof gate can least afford,
because its output reads as "the proof broke".

A here-string has no writer to kill. The same change is also carried inside the
Rust 1.99.1 pull request; it is split out here because that one cannot land
quickly, and every proofs run until it does is subject to this.

Co-Authored-By: Claude Opus 5 <[email protected]>

4fbef95bc3

• View at this point in history

2026-11-03 03:40:09 -05:00