fix(ci): fail folio when a gated property is not in the spec

Nothing tied GATED_PROPERTIES to the spec it gates. Renaming a property
left the classifier matching nothing: ios and web blamed the spec for
finding a different bug, and android silently reclassified a real
conviction as 'judging health only' and stayed green.

replay-ui-summary.sh already makes this check for its own list. The spec
path becomes SPEC-overridable the same way, so the check is testable.

.github/scripts/folio-run.sh

@@ -18,9 +18,49 @@ max_steps="${MAX_STEPS:-240}"
 duration="${DURATION:-20m}"
 sanderling="${SANDERLING:-./bin/sanderling}"
 output="runs/folio-$platform"
-spec="examples/folio/sanderling/spec.ts"
+spec="${SPEC:-examples/folio/sanderling/spec.ts}"
 summary="${GITHUB_STEP_SUMMARY:-/dev/null}"
 
+# 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="submitMovesBalanceByAtMostTypedAmount,submitCommitsOneTransactionPerAction"
+
+# A gate is only as good as these names, and nothing else ties them to the spec.
+# Rename a property there and the classification below matches nothing: ios and
+# web blame the spec for finding a different bug, and android reclassifies a
+# real conviction as "judging health only" and stays green. Checked before the
+# run so a rename costs seconds rather than the whole budget.
+SPEC="$spec" GATED="$GATED_PROPERTIES" SELF="$0" python3 - <<'PY' || exit 1
+import os, re, sys
+
+spec_path = os.environ["SPEC"]
+gated = [name for name in os.environ["GATED"].split(",") if name]
+try:
+    with open(spec_path, encoding="utf-8") as handle:
+        source = handle.read()
+except OSError as error:
+    sys.exit("folio: cannot read %s to check the gated properties still exist: %s"
+             % (spec_path, error))
+
+block = re.search(r"export\s+const\s+properties\s*=\s*\{(.*?)\}", source, re.S)
+if block is None:
+    sys.exit("folio: %s declares no `export const properties = {...}`, so the gated "
+             "properties cannot be checked against it" % spec_path)
+
+declared = set()
+for entry in re.sub(r"//[^\n]*", "", block.group(1)).split(","):
+    name = entry.split(":")[0].strip()
+    if re.fullmatch(r"[A-Za-z_$][A-Za-z0-9_$]*", name):
+        declared.add(name)
+
+missing = [name for name in gated if name not in declared]
+if missing:
+    sys.exit("folio: %s no longer declares %s, so this leg gates on a property that "
+             "cannot be violated and every real conviction would read as a different "
+             "finding. Update GATED_PROPERTIES in %s."
+             % (spec_path, ", ".join(missing), os.environ["SELF"]))
+PY
+
 folio_args=(--bundle-id app.folio)
 case "$platform" in
   android)
@@ -97,10 +137,6 @@ trace=""
 steps=0
 [ -f "$trace" ] && steps=$(wc -l < "$trace" | tr -d ' ')
 
-# 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="submitMovesBalanceByAtMostTypedAmount,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