.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 }}
@@ -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