Merge origin/master into llm-recording-and-analysis

Brings in #73, which landed web fact-parity work overlapping this branch:
selector-tagged ax handles, aria-disabled in `enabled`, shadow-DOM traversal
and a `scrollable`/`editable` dump, plus a third folio property and two new
testTags on HomeScreen.

Six files conflicted. The option-carrying ones took the union of both sides'
fields, so `--label-source` and `--exit-on-violation` both reach the pipeline.
In web-runtime.ts both sides changed how an element is described: master gave
`elementHandle` a selector to tag handles with, this branch gave it raw
attribute names and a field hint. Both survive, and `enabled` now answers
through master's isEnabled while `editable` stays.

Claude-Session: https://claude.ai/code/session_01A5KmftdEJ49A9z5mF5ESrX

docs/development/ci.md

@@ -0,0 +1,161 @@
+---
+title: CI
+---
+
+# CI
+
+`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
+neither is a merge gate.
+
+## folio
+
+Actions -> folio -> Run workflow. Inputs pick the legs (`all`, `android`, `ios`,
+`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, with that leg's pinned
+numbers:
+
+```
+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 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.
+
+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.
+
+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 |
+| no trace at all, on exit 0 or 2 | red: the run recorded nothing, so there is no verdict to read |
+| 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
+visit, and the property convicts on arithmetic it cannot attribute: an early
+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, because it convicts in four
+runs out of five rather than five. The leg asserts that the run stayed healthy
+and reached the transaction screen, and reports the conviction it usually gets as
+a bonus. A gate that fails one run in five would be useless here: its failure
+message, "the double-submit bug was NOT found", is indistinguishable from the
+regression the gate exists to catch.
+
+It used to be two runs in five. The android backend now waits out a route
+cross-fade before it snapshots, the way the ios companion and the chrome driver
+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
+cross-origin isolation. Served without them the app loads a blank canvas and
+every step observes an empty accessibility tree.
+
+The seeds are calibrated, not guessed. On an M-series mac, web seed 3 convicts at
+step 185-187 and ios seed 7 at step 97-101, each 3 runs out of 3 and each with a
+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 200 steps: its conviction lands at step 178, so a
+shorter budget would never see the bonus. A full run costs about five minutes.
+
+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
+`simctl uninstall` before each repeat or the numbers drift.
+
+The ios leg passes `--clear-data=false`, because the job installs a fresh build
+immediately before the run and a freshly installed app is already clear state.
+The in-run reinstall is worth avoiding: `simctl uninstall` + `install` followed
+straight away by the XCTest runner's own launch fails with `app.folio is unknown
+to FrontBoard` maybe half the time. That used to hang the run outright; the
+launch RPC is bounded now, so it fails in about 90 seconds with a real error
+instead, but a failing leg is still a failing leg. The job timeouts are the
+backstop if it happens anyway.
+
+Only one sanderling run may drive a given simulator at a time. The driver takes
+an advisory lock on the target's UDID and a second run is refused with the lock
+path in the message, because two runs interleaving app lifecycle leave the first
+run's automation session bound to a bundle the simulator no longer knows.
+
+## replay-ui
+
+Actions -> replay-ui -> Run workflow. This one is dogfooding: it records a trace
+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`.
+
+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
+
+Both workflows upload their run directories as artifacts, and write the step
+count, seed and violations to the job summary. To replay a failure:
+
+```
+gh run download <run-id> -n folio-android
+sanderling replay <the downloaded runs directory>
+```
+
+That is the same UI the replay-ui workflow fuzzes. Open the step the summary
+named, and the Violations tab shows the witness: the property, the reason, and
+the extractor values at the step that caused it.
+
+## When a device leg flakes
+
+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 "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. A leg failing with "a predicate threw" is
+a different problem entirely and no seed will fix it.

docs/development/design-principles.md

@@ -51,3 +51,25 @@ There is exactly one authoring surface: the TypeScript spec. There is no separat
 
 This is intentional. A test harness with two authoring languages (YAML plus code, JSON plus code) splits concerns in a way that always drifts. Something works in one surface and not the other, and debugging requires holding both in your head.
 
+
+## 8. A property that cannot fail is worse than one that fails
+
+A spec fails loudly when it is wrong about the app. It fails silently when it is wrong about
+itself, and that is the failure this project has to design against.
+
+Two shapes recur. A property is *vacuously true* when a fact it reads is missing, so it never
+fires and every run is green: `state.lastAction` was hardcoded null on web, `ax.findAll` on a
+selector path returned nothing there, and no element on iOS carried `text` because the mapping
+only ever read `AXValue`. In each case a correct property proved nothing. A property is
+*degenerately false* when a missing fact is read as a value instead: folio's balances parsed as
+`0` on web, so the check became `|0 - 0| === typedAmount` and fired on every healthy submit.
+Both shapes look exactly like a working property from the outside.
+
+So an unreadable fact is unknown, never a default. Extractors return null rather than zero or
+empty string, and a property given an unknown declines to judge instead of convicting. The same
+rule covers arithmetic the representation cannot hold: integer cents in a float64 stop being
+exact past 2^53, and a comparison that cannot pass is not a comparison that failed.
+
+Which means a green run is evidence only if you can point at a step where the property actually
+fired, and a red one only if the witness holds real values. Read the witness, not the exit code.
+Every bug listed above was found that way, and each had already survived a run that looked fine.

docs/development/index.md

@@ -6,6 +6,7 @@ title: Development
 
 - [Design principles](./design-principles/)
 - [Architecture](./architecture/)
+- [CI](./ci/)
 - v0.1.0 scope: [milestone #1](https://github.com/priyanshujain/sanderling/milestone/1)
 
 ## Building the docs site locally

docs/manual/case-study.md

@@ -33,45 +33,95 @@ 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;
-    return Math.abs(totalBalance.current - (totalBalance.previous ?? 0)) === typed;
+    const before = totalBalance.previous;
+    if (before === null || totalBalance.current === null) return true;
+    return Math.abs(totalBalance.current - before) === typed;
   })
 );
 ```
 
 `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 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.
@@ -125,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
 

docs/manual/cli.md

@@ -22,11 +22,15 @@ Run a spec against an app for a fixed duration.
 | `--ios-device` | optional (ios) | iOS target: a simulator name/UDID to boot, or a connected device's name, UDID, or CoreDevice id. |
 | `--ios-app-path` | optional (ios) | Path to the `.app` bundle for clear-state reinstall (simulator via `simctl`, device via `devicectl`). |
 | `--duration` | `5m` | Total test duration (`30s`, `5m`, `2h`, `1d`). |
+| `--max-steps` | `0` | Stop after this many steps (`0` = no cap, the duration governs). A step budget is what makes two generators comparable. |
+| `--exit-on-violation` | `false` | Stop the run at the first property violation and exit `2`. |
 | `--seed` | `0` | PRNG seed. `0` uses a random seed and records it in `meta.json`. |
 | `--generator` | `seeded` | Who picks each action: `seeded` (the run's PRNG) or `llm` (a vision model). See [the LLM generator](../spec-language/#llm-generator). |
 | `--output` | `./runs` | Output directory for traces. |
 | `--clear-data` | `true` | Clear app data before launching so the run starts from a fresh install. Pass `--clear-data=false` to resume prior state. |
 
+Exit codes: `0` the run finished (violations, if any, are in the summary), `2` the run stopped on a violation under `--exit-on-violation`, `1` something went wrong. CI reads the difference between `2` and `1` to tell a found bug from a broken harness.
+
 ## `sanderling replay [run-or-runs-dir]`
 
 Serve a local web UI for browsing traces. The positional argument is optional and may point at either a runs directory (the parent of many runs) or a single run directory (auto-detected by the presence of `meta.json`). Defaults to `./runs`.
@@ -63,7 +67,5 @@ Print the CLI version.
 ## Flags coming in v0.1.0
 
 - `--permissions` to pre-set OS-level permissions (for example `--permissions location=allow,notifications=deny`).
-- `--max-steps` hard cap on step count.
-- `--exit-on-violation` stop the run on the first property violation.
 
 Tracked in the [v0.1.0 milestone](https://github.com/priyanshujain/sanderling/milestone/1).

docs/manual/introduction.md

@@ -80,6 +80,8 @@ The loop runs until the duration you set elapses. Every step is written to a tra
 
 Kotlin Multiplatform apps need nothing special: the Android build is tested through the Android driver and the iOS build through the iOS driver.
 
+Canvas-rendered web apps are the exception. On web, `InputText` types through the DevTools Protocol's `Input.insertText`, which needs a focused DOM element to deliver to, and a bare `<canvas>` is not one: the call produces no events at all and the app sees nothing typed. The driver cannot work around that, because there is no event target. Compose Multiplatform for Web is fine because it keeps a hidden `<input>` IME proxy in its shadow root, a real focusable element that receives the text. A canvas app that exposes no such element is tap-fuzzable but not text-fuzzable.
+
 ## Reading this manual
 
 - [Case study: Folio](../case-study/) follows sanderling finding a real bug in the example app, and shows how its spec is written.