standards-build: the proof gate turned a verified proof into a failure #599
Loading…
Reference in a new issue
No description provided.
Delete branch "ci/proof-gate-sigpipe"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
standards-build: the proof gate turned a verified proof into a failure
The gate read:
under
set -o pipefail.grep -qexits at its first match,echothen dies ofSIGPIPE (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
$outfits the pipe buffer, which makes it a function of the harness's outputsize, not of the proof.
Caught live on #598, whose branch does not carry this fix:
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]
🤖 Generated with Claude Code
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]>