docs: correct the snippets and numbers that drifted from the code

docs/development/ci.md

@@ -4,9 +4,9 @@ title: CI
 
 # CI
 
-`ci.yml` runs on every pull request: it builds, unit-tests, and drives two small
-web fixtures through headless Chrome. It never runs sanderling against a real
-app.
+`ci.yml` runs on every pull request: it builds, unit-tests, and drives three
+small web fixtures through headless Chrome (`test/browser/testdata`). It never
+runs sanderling against a real app.
 
 Two other workflows do, and both are `workflow_dispatch` only. They boot devices,
 build apps and take minutes, which is not what you want on every push, and
@@ -15,33 +15,51 @@ neither is a merge gate.
 ## folio
 
 Actions -> folio -> Run workflow. Inputs pick the legs (`all`, `android`, `ios`,
-`web`), and override the seed, the wall-clock budget, and the step budget; `0`
-means "use the calibrated value in the workflow".
+`web`), and override the seed, the step budget and the wall-clock budget. Seed
+and step budget take `0` to mean "use the calibrated value in the workflow"; the
+wall-clock budget has no such sentinel and is passed through as written, so
+every leg gets whatever you type there.
 
 Each leg builds `examples/folio` for its platform, builds the CLI with only the
 tags that platform needs (`make sanderling-android` and friends), and runs
 `examples/folio/sanderling/spec.ts` through `.github/scripts/folio-run.sh`. That
-script is plain bash so you can reproduce a job locally:
+script is plain bash so you can reproduce a job locally, with that leg's pinned
+numbers:
 
 ```
-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 the bug.** Folio double-submits a transaction when the
 submit button is double-tapped, and two properties catch it:
-`submitMovesBalanceByTypedAmount`, which needs the balance to move by exactly
-twice the typed amount, and `submitCommitsOneTransactionPerAction`, which needs
-more transactions committed than there were submit actions. The runs pass
-`--exit-on-violation`, so:
+`submitMovesBalanceByTypedAmount`, which demands the total balance move by
+exactly the amount typed, and `submitCommitsOneTransactionPerAction`, which
+demands no more transactions committed over a window than there were submit
+actions in it. A double tap is one action committing two transactions, so it
+breaks both.
 
-| exit | meaning | job |
-|---|---|---|
-| 2 | the run found a violation | green |
-| 0 | the run finished clean | red: the fuzzer stopped finding a bug that is still there |
-| 1 | something went wrong | red: the harness broke |
+The runs pass `--exit-on-violation`, which exits 2 when the run recorded a
+violation and 1 when something went wrong. Telling those apart is the whole
+point of the exit code: a job that only knew "non-zero" could not tell a working
+fuzzer from a broken emulator.
 
-Distinguishing 0 from 1 is the whole point of the exit code: a job that only
-knew "non-zero" could not tell a working fuzzer from a broken emulator.
+Exit 2 on its own is not a conviction, though, so the script reads the trace
+before it decides:
+
+| what the trace says | job |
+|---|---|
+| a violation of one of the two properties above, with no `is_error` on its witness | green |
+| a violation whose witness carries `is_error` | red: a predicate threw, and a thrown predicate is recorded as a violation like any other |
+| a violation of any other property (`newAccountBalanceIsZero` fires on one android seed) | red: a real finding, but not the one this leg gates on |
+| no violation and exit 0 | red: the fuzzer stopped finding a bug that is still there |
+| exit 1, or any other code | red: the harness broke, and the code propagates |
+
+The first two rows are why the check is worth the code it takes. A `TypeError`
+in `predicates.ts` and a fuzzer that no longer reaches the bug both used to
+print "found the submit bug" and exit 0, and they need opposite responses: one
+is a spec to fix, the other is a seed to recalibrate. A thrown predicate fails
+android as well, where a conviction is otherwise only a bonus, because a spec
+that stopped running is not evidence about the app.
 
 The balance property only judges a window holding exactly one submit action.
 Without that rule the recorded delta covers every transaction since the last Home
@@ -111,9 +129,11 @@ from `test/browser/testdata/throwing` (violations and uncaught exceptions, so
 every panel has something to render), serves it with `sanderling replay`, and
 fuzzes that UI with `replay-ui/sanderling/spec.ts`.
 
-Every property there is a cross-panel agreement - two panels deriving the same
-fact by different paths have to say the same thing - so it holds for any trace
-and needs no recalibrating when the fixture changes. Any violation fails the job.
+Six of the seven properties there are cross-panel agreements - two panels
+deriving the same fact by different paths have to say the same thing - so they
+hold for any trace and need no recalibrating when the fixture changes. The
+seventh is the stock `noUncaughtExceptions`, which asks nothing of the panels
+and only fails if the UI throws. Any violation fails the job.
 
 ## Reading a failure
 
@@ -133,7 +153,8 @@ the extractor values at the step that caused it.
 
 Expecting a violation from a single seed is timing-sensitive, most of all on an
 emulator. Calibration reduces that; it does not remove it. If a platform starts
-failing across repeated dispatches with exit 0, do not raise the step budget
-blindly - run a seed sweep with the campaign tool
+failing across repeated dispatches with "the double-submit bug was NOT found",
+do not raise the step budget blindly - run a seed sweep with the campaign tool
 (`cmd/internal-tools/campaign`), which exists for exactly this, and pin a seed
-that finds the bug with room to spare.
+that finds the bug with room to spare. A leg failing with "a predicate threw" is
+a different problem entirely and no seed will fix it.

docs/manual/case-study.md

@@ -33,6 +33,7 @@ const submitMovesBalanceByTypedAmount = always(
     const action = lastAction.current;
     if (action?.kind !== "Tap" && action?.kind !== "DoubleTap") return true;
     if (!JSON.stringify(action.on ?? "").includes("TxnSubmit")) return true;
+    if (submitsInWindow.current !== 1) return true;
     const typed = parseTypedAmount(txnAmountField.previous?.text);
     if (typed === 0) return true;
     const before = totalBalance.previous;
@@ -44,38 +45,83 @@ const submitMovesBalanceByTypedAmount = always(
 
 `always` checks the formula at every step; `next` lets it compare the step before a submit to the step after. The guards narrow it to the one transition that matters, a submit that lands back on home, and the last line states the rule: the balance moved by exactly the typed amount. Double-submit moves it by twice that, and the formula is false.
 
-The null guard is not defensive clutter, it is the difference between a property and a false alarm. Read a balance you could not parse as `0` and the comparison becomes `0 - 0 === typed`, which is false at every healthy submit. A reading you do not have is not evidence, so the property declines to judge. The real spec guards the same way against a balance too large for exact integer arithmetic.
+The window guard is the difference between a property and a false conviction. `totalBalance.previous` is the last total we read, not the total as of the last transaction, so the two numbers being compared can straddle any number of commits: a real run produced a delta of 13000 against a typed 19600, because the window held a double-submit's two 19600 debits and an unrelated 26200 credit. A delta like that is not evidence about the amount typed into any one submit. Exactly one submit action in the window still catches the bug, because the double tap is a single action.
+
+The null guard is not defensive clutter either. Read a balance you could not parse as `0` and the comparison becomes `0 - 0 === typed`, which is false at every healthy submit. A reading you do not have is not evidence, so the property declines to judge. The real spec guards the same way against a balance too large for exact integer arithmetic.
 
 The values it reads come from extractors, which pull state out of the UI tree once per step:
 
 ```ts
-const route = extract<string | null>("route", s => {
-  if (s.ax.find({ testTag: "AddTransactionScreen" })) return "add-transaction";
-  if (s.ax.find({ testTag: "HomeScreen" })) return "home";
-  // ...other screens
-  return null;
-});
+const SCREENS = {
+  login: "LoginScreen",
+  "add-account": "AddAccountScreen",
+  "add-transaction": "AddTransactionScreen",
+  ledger: "LedgerScreen",
+  home: "HomeScreen",
+} as const;
+type Route = keyof typeof SCREENS;
 
-const totalBalance = extract("totalBalance", s =>
-  s.ax.findAll([{ testTag: "HomeScreen" }, { testTag: "AccountCard" }])
-    .reduce((sum, c) => sum + parseDollarCents(c.find({ testTag: "AccountBalance" })?.text), 0));
+// The screen this frame shows, or null when it does not show exactly one.
+// Android's hierarchy dump carries the outgoing and the incoming screen
+// together on better than one frame in five, and such a frame is a navigation
+// transition: evidence about neither screen. Ranking the markers and returning
+// the first one found is how a spec convicts itself on a half-drawn screen.
+const routeOf = (s: State): Route | null => {
+  let shown: Route | null = null;
+  for (const [name, tag] of Object.entries(SCREENS) as [Route, string][]) {
+    if (!s.ax.find({ testTag: tag })) continue;
+    if (shown !== null) return null;
+    shown = name;
+  }
+  return shown;
+};
+const route = extract<Route | null>("route", routeOf);
+
+// Home's own TOTAL BALANCE node, which the app computes over every account.
+// Summing the AccountCard balances reads only the cards laid out inside the
+// viewport, and a card clipped at the bottom edge looks exactly like money
+// moving. Off Home there is nothing to read, so the last total we did read is
+// carried forward and `previous` and `current` stay on the same scale.
+let lastHomeTotal: number | null = null;
+const totalBalance = extract<number | null>("totalBalance", s => {
+  if (routeOf(s) !== "home") return lastHomeTotal;
+  const total = parseDollarCents(
+    s.ax.find([{ testTag: "HomeScreen" }, { testTag: "TotalBalance" }])?.text);
+  if (total === null) return null; // unreadable is unknown; the carrier keeps its value
+  lastHomeTotal = total;
+  return total;
+});
 ```
 
-Every Folio screen and control carries a `testTag`. Compose exposes it as the resource-id on Android and the accessibility identifier on iOS, so one selector resolves on both. `extract` runs against the live tree each step; properties and actions read `.current` and `.previous`, never the raw state.
+Every Folio screen and control carries a `testTag`. Compose exposes it as the resource-id on Android and the accessibility identifier on iOS, so one selector resolves on both. `extract` runs against the live tree each step; properties and actions read `.current` and `.previous`, never the raw state. An extractor may not read another extractor's handle, which is why `totalBalance` calls `routeOf` rather than `route.current`.
 
-A second property states what new accounts must look like: a freshly created account starts at zero.
+A second property states what new accounts must look like: a freshly created account starts at zero. The work is in naming the account it judges.
 
 ```ts
 const newAccountBalanceIsZero = always(
   next(() => {
-    const before = new Set((accounts.previous ?? []).map(a => a.name));
-    return accounts.current
-      .filter(a => !before.has(a.name))
-      .every(a => a.balance === 0);
+    if (route.current !== "home") return true;
+    if (!isAddAccountSubmitTap(lastAction.current)) return true;
+    const typed = accountNameField.previous?.text?.trim();
+    const before = accounts.previous ?? null;
+    const after = accounts.current;
+    if (!typed || before === null || after === null) return true;
+    // The only card attributable to a creation is the one named what the fuzzer
+    // typed, on the step its submit landed. Anything else that turned up is a
+    // card that scrolled into view, not an account that came into existence.
+    const matches = after.filter(a => a.name.endsWith(typed));
+    if (matches.length !== 1) return true;
+    const created = matches[0];
+    if (before.some(a => a.name === created.name)) return true;
+    return created.balance === null || created.balance === 0;
   })
 );
 ```
 
+Diffing the two account lists and judging whatever is new is the version that reads better and does not work: Home lists the accounts that fit the viewport, so a card that scrolls in is indistinguishable from an account that was just created. That version convicted this property on android over a Travel account holding $24,112.00.
+
+A third property, `submitCommitsOneTransactionPerAction`, states the same bug without arithmetic: over any window, no more transactions may be committed than there were submit actions. It needs no amount and no float comparison, so it survives a window of any width, and it does most of the detecting in practice.
+
 ## Reaching the screens that matter
 
 A fuzzer that pokes at random never logs in, and never reaches a transaction form. The spec gives sanderling enough to drive the real flows, no more.
@@ -129,7 +175,7 @@ export const actionsRoot = weighted(
 );
 ```
 
-That is the whole input. Two invariants, a way in, and a weighted sense of where to spend time. Nothing here names the bug.
+That is the whole input. Three invariants, a way in, and a weighted sense of where to spend time. Nothing here names the bug.
 
 ## What the run does