ci(folio): a thrown predicate is not a conviction

exit 2 means the run recorded a violation, and a predicate that throws
is recorded as one too. so was newAccountBalanceIsZero, an unrelated
property in the same spec. the gate read the exit code and went green
with detection dead.

.github/scripts/folio-run.sh

@@ -3,12 +3,13 @@
 # exit code the job expects. Kept out of the workflow YAML so it can be run by
 # hand, which is how it was calibrated:
 #
-#   SEED=3 MAX_STEPS=240 .github/scripts/folio-run.sh android
+#   SEED=9 MAX_STEPS=200 .github/scripts/folio-run.sh android
 #
-# web and ios expect exit 2: folio's double-submit bug is still there, and a run
+# web and ios expect a conviction: folio's double-submit bug is still there, and
-# that no longer finds it is a regression in the fuzzer, not a pass. android is a
+# a run that no longer finds it is a regression in the fuzzer, not a pass. The
-# health gate instead, because a run there is not a function of its seed; see
+# exit code alone does not say that much, so this script reads the trace: see
-# docs/development/ci.md.
+# GATED_PROPERTIES below. android is a health gate instead, because it convicts
+# in four runs out of five rather than five; see docs/development/ci.md.
 set -uo pipefail
 
 platform="${1:?usage: folio-run.sh android|ios|web}"
@@ -86,31 +87,95 @@ esac
 code=$?
 
 run_dir="$(ls -d "$output"/*/ 2>/dev/null | tail -1)"
+trace="${run_dir:-.}/trace.jsonl"
 steps=0
-[ -n "$run_dir" ] && steps=$(wc -l < "$run_dir/trace.jsonl" | tr -d ' ')
+[ -f "$trace" ] && steps=$(wc -l < "$trace" | tr -d ' ')
-violated=$(grep -ho '"violations":\[[^]]*\]' "$run_dir/trace.jsonl" 2>/dev/null | head -1)
+
+# The two properties that state folio's double-submit. Anything else the spec
+# proves false is a different finding, and this leg has nothing to say about it.
+GATED_PROPERTIES="submitMovesBalanceByTypedAmount,submitCommitsOneTransactionPerAction"
+
+# Exit 2 means "the run recorded a violation", and that is NOT the same as "the
+# run convicted folio". A predicate that THROWS is recorded as a violation too,
+# with is_error set and the thrown text as its reason, and it reaches exit 2 by
+# the identical path. So does a violation of newAccountBalanceIsZero, a real but
+# unrelated property in the same spec, which one android seed produces. Reading
+# the exit code alone leaves the gate green with detection dead.
+#
+# So sort the trace's violations three ways, by name and by is_error:
+#   line 1  convictions: a gated property that was proved false
+#   line 2  thrown: a predicate that blew up, with the reason it gave
+#   line 3  other: a real violation of some property this leg does not gate on
+classified=$(TRACE="$trace" GATED="$GATED_PROPERTIES" python3 - <<'PY'
+import json, os
+
+gated = set(os.environ["GATED"].split(","))
+convictions, thrown, other = [], [], []
+try:
+    lines = open(os.environ["TRACE"], encoding="utf-8", errors="replace")
+except OSError:
+    lines = []
+for line in lines:
+    try:
+        step = json.loads(line)
+    except ValueError:
+        continue
+    witnesses = step.get("witnesses") or {}
+    for name in step.get("violations") or []:
+        witness = witnesses.get(name) or {}
+        if witness.get("is_error"):
+            reason = " ".join(str(witness.get("reason") or "").split())
+            thrown.append("%s: %s" % (name, reason) if reason else name)
+        elif name in gated:
+            convictions.append(name)
+        else:
+            other.append(name)
+for names in (convictions, thrown, other):
+    print(", ".join(names))
+PY
+)
+convicted=$(printf '%s\n' "$classified" | sed -n '1p')
+thrown=$(printf '%s\n' "$classified" | sed -n '2p')
+other=$(printf '%s\n' "$classified" | sed -n '3p')
 
 {
   echo "### folio on $platform"
   echo
   echo "- seed \`$seed\`, budget $max_steps steps / $duration"
   echo "- $steps steps recorded, exit $code"
-  [ -n "$violated" ] && echo "- $violated"
+  [ -n "$convicted" ] && echo "- convicted on: $convicted"
+  [ -n "$other" ] && echo "- also violated: $other"
+  [ -n "$thrown" ] && echo "- **a predicate threw**: $thrown"
 } >> "$summary"
 
+# A thrown predicate fails every leg, android included. It is not evidence about
+# folio: the property that threw is violated from that step on whatever the app
+# does, and --exit-on-violation ends the run there, so nothing past it was
+# checked. Reporting that as a conviction, or as android's bonus, is the hole
+# this check exists to close.
+if [ -n "$thrown" ]; then
+  echo "folio/$platform: a predicate threw, so exit $code is not a verdict about folio: $thrown" >&2
+  echo "folio/$platform: fix the spec (examples/folio/sanderling/) and run again" >&2
+  exit 1
+fi
+
 if [ "$platform" = "android" ]; then
-  # A health gate, not a conviction gate. The android hierarchy dump can show
+  # A health gate, not a conviction gate: android convicts in four runs out of
-  # two screens mid-transition, and such a step applies no action, so the same
+  # five, and a gate that fails the fifth would report a regression it had not
-  # seed walks a different trajectory each run and the bug turns up in about two
+  # found. Reaching the transaction screen is what this leg proves: the app
-  # runs in five. Demanding a conviction would cry wolf more often than it would
+  # built, installed, launched and drove.
-  # catch the regression it exists to catch. Reaching the transaction screen is
-  # what this leg proves: the app built, installed, launched and drove.
   case "$code" in
     0) ;;
-    2) echo "folio/android: found the submit bug in $steps steps (a bonus, not required)" ;;
+    2)
+      if [ -n "$convicted" ]; then
+        echo "folio/android: found the submit bug in $steps steps (a bonus, not required)"
+      else
+        echo "folio/android: violated $other, which is not the double-submit; judging health only"
+      fi
+      ;;
     *) echo "folio/android: the harness failed with exit $code" >&2; exit "$code" ;;
   esac
-  if ! grep -q '"AddTransactionScreen"' "$run_dir/trace.jsonl"; then
+  if ! grep -q '"AddTransactionScreen"' "$trace" 2>/dev/null; then
     echo "folio/android: the run never reached AddTransactionScreen, so it never got past login" >&2
     exit 1
   fi
@@ -119,7 +184,18 @@ if [ "$platform" = "android" ]; then
 fi
 
 case "$code" in
-  2) echo "folio/$platform: found the submit bug in $steps steps"; exit 0 ;;
+  2)
-  0) echo "folio/$platform: the run finished clean; the double-submit bug was NOT found in $steps steps (seed $seed)" >&2; exit 1 ;;
+    if [ -z "$convicted" ]; then
+      echo "folio/$platform: exit 2, but the violation was ${other:-nothing this trace records}, not the double-submit this leg gates on" >&2
+      exit 1
+    fi
+    echo "folio/$platform: found the submit bug in $steps steps ($convicted)"
+    exit 0
+    ;;
+  0)
+    echo "folio/$platform: the run finished clean; the double-submit bug was NOT found in $steps steps (seed $seed)" >&2
+    echo "folio/$platform: the spec ran without throwing, so this is the fuzzer no longer reaching the bug, not a broken spec" >&2
+    exit 1
+    ;;
   *) echo "folio/$platform: the harness failed with exit $code" >&2; exit "$code" ;;
 esac