ci(folio): let the android leg run far enough to see its conviction

.github/workflows/folio.yml

@@ -10,9 +10,9 @@ name: folio
 # two are worth telling apart, which is why --exit-on-violation exits 2 and not
 # 1.
 #
-# android is a health gate. The same seed does not walk the same trajectory
+# android is a health gate. It convicts in four runs out of five, which is real
-# there, so the bug turns up in roughly two runs in five, and a conviction gate
+# evidence but not a gate: the fifth would report a regression it had not found.
-# would report a regression it had not found.
+# The budget is set so the conviction it usually gets is reported as a bonus.
 
 on:
   workflow_dispatch:
@@ -97,7 +97,7 @@ jobs:
           script: .github/scripts/folio-run.sh android
         env:
           SEED: ${{ inputs.seed != '0' && inputs.seed || '9' }}
-          MAX_STEPS: ${{ inputs.max-steps != '0' && inputs.max-steps || '120' }}
+          MAX_STEPS: ${{ inputs.max-steps != '0' && inputs.max-steps || '200' }}
           DURATION: ${{ inputs.duration }}
 
       - name: Upload the run

docs/development/ci.md

@@ -50,16 +50,27 @@ version of this gate went green on a witness whose delta was 3.16x the typed
 amount. Honest windows are rare, so the counting invariant carries most of the
 detection: it needs no amount and survives a wide window.
 
-**android is a health gate**, not a conviction gate. A run there is not a
+**android is a health gate**, not a conviction gate, because it convicts in four
-function of its seed. The hierarchy dump can show two screens at once during a
+runs out of five rather than five. The leg asserts that the run stayed healthy
-Compose cross-fade, such a step applies no action, and the count of those frames
+and reached the transaction screen, and reports the conviction it usually gets as
-varies run to run, so the same seed walks a different trajectory each time. The
+a bonus. A gate that fails one run in five would be useless here: its failure
-bug turns up in about two runs in five, which is not a gate: the failure message
+message, "the double-submit bug was NOT found", is indistinguishable from the
-"the double-submit bug was NOT found" would be indistinguishable from the
+regression the gate exists to catch.
-regression it exists to catch. The leg asserts instead that the run stayed
+
-healthy and reached the transaction screen, and reports a conviction as a bonus
+It used to be two runs in five. The android backend now waits out a route
-when it gets one. Fixing this means suppressing transitional frames in the
+cross-fade before it snapshots, the way the ios companion and the chrome driver
-android driver, the way the ios companion and the chrome driver already do.
+do, because a dump holding two screens at once makes the runner refuse to act on
+it and a quarter of android steps therefore applied no action at all. The number
+of those wasted steps varied run to run, so the same seed never walked the same
+trajectory. With the wait, four runs of one seed produced byte-identical decision
+sequences over 179 steps.
+
+The fifth diverged for the remaining reason: a route can settle before its
+content composes, so the tree holds one screen and almost nothing in it, and the
+fuzzer acts on a screen that is still filling in. That happened once in about a
+thousand steps. Catching it needs structural stability polling on every snapshot,
+which costs roughly 2.8s per mutating step and was removed for that reason, so it
+is the open item between android and a real conviction gate.
 
 The wasmJs app is served with `Cross-Origin-Opener-Policy` and
 `Cross-Origin-Embedder-Policy` headers, because its sqlite worker needs
@@ -72,9 +83,8 @@ delta of exactly twice the typed amount. Both run a 240-step budget. Keep them
 pinned: honest evidence is rare, and across 2261 ios steps only one submit tap
 landing on Home had a single-submit window.
 
-Android runs seed 9 over 120 steps, but as a health gate the seed is not load
+Android runs seed 9 over 200 steps: its conviction lands at step 178, so a
-bearing; the budget is, since a run that finds nothing walks the whole thing and
+shorter budget would never see the bonus. A full run costs about five minutes.
-costs seven minutes against ninety seconds for one that convicts.
 
 Repeating the ios leg by hand is not the same as running it in CI: with
 `--clear-data=false` a second local run inherits the first one's accounts, so