From 4fbef95bc32830709b2505539e566e51b6bb6b27 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Mon, 2 Nov 2026 07:56:37 -0500 Subject: [PATCH 1/2] 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 --- .github/workflows/standards-build.yml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/.github/workflows/standards-build.yml b/.github/workflows/standards-build.yml index 771cbf05b..4d3b8eef1 100644 --- a/.github/workflows/standards-build.yml +++ b/.github/workflows/standards-build.yml @@ -406,7 +406,12 @@ jobs: echo "== $h ==" out="$(cargo kani -p joulespec-core --harness "$h" 2>&1)" echo "$out" | grep -E '^ \*\* |^VERIFICATION' - echo "$out" | grep -q '^VERIFICATION:- SUCCESSFUL' \ + # A here-string, not `echo | grep -q`: grep -q exits at the first + # match, echo then dies of SIGPIPE (141), and `set -o pipefail` + # turns a match into a failure. It is a race on how much of $out + # fits the pipe buffer, so it passed while this harness reported 15 + # properties and failed at 336. + grep -q '^VERIFICATION:- SUCCESSFUL' <<<"$out" \ || { echo "$h did not verify"; exit 1; } # "N of M cover properties satisfied". Both numbers are read with # their own expression rather than by splitting one capture, so @@ -434,7 +439,7 @@ jobs: echo "mutation applied: the scale is now computed in 64 bits" out="$(cargo kani -p joulespec-core --harness the_ratio_rule_is_total_over_every_input 2>&1 || true)" echo "$out" | grep -E '^ \*\* |^VERIFICATION' - echo "$out" | grep -q '^VERIFICATION:- FAILED' \ + grep -q '^VERIFICATION:- FAILED' <<<"$out" \ || { echo "the prover did not refute an overflowing ratio rule"; exit 1; } # The NVML backends sit behind features no workspace member enables -- 2.54.0 (Apple Git-157) From 0efe3e65690c2bbd754ce89217a108e586863fbe Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Tue, 3 Nov 2026 06:40:53 -0500 Subject: [PATCH 2/2] 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 --- .github/workflows/standards-build.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/standards-build.yml b/.github/workflows/standards-build.yml index 4d3b8eef1..4464ab7ed 100644 --- a/.github/workflows/standards-build.yml +++ b/.github/workflows/standards-build.yml @@ -70,7 +70,7 @@ jobs: # matrix is the entries it selects. plan: name: which workspaces this change touches - runs-on: linux-arm64 + runs-on: linux outputs: include: ${{ steps.plan.outputs.include }} any: ${{ steps.plan.outputs.any }} -- 2.54.0 (Apple Git-157)