Merge branch 'spec-authoring-skills' into trial-merge

2026-10-02 19:17:10 +00:00 · 2026-08-15 23:04:37 +05:30
commit 17f0a020fa
@@ -16,7 +16,8 @@ Run a spec against an app for a fixed duration.
 |---|---|---|
 | `--spec` | required | Path to the TypeScript spec. |
 | `--bundle-id` | required | Target app bundle ID (Android: applicationId). |
-| `--launcher-activity` | resolved | Optional `<pkg>/<activity>` to launch. Overrides default resolution. |
+| `--device` | optional (android) | Android device serial, as `adb devices` reports it. Required when more than one device is attached. |
 | `--android-app-path` | optional (android) | Path to the APK. Clear-state reinstalls from it instead of running `pm clear`. |
 | `--platform` | `android` | Target platform: `android`, `ios`, or `web`. |
 | `--avd` | optional (android) | Android AVD name to boot if no device is connected. Required only when no device is connected and multiple AVDs exist. |
 | `--ios-device` | optional (ios) | iOS target: a simulator name/UDID to boot, or a connected device's name, UDID, or CoreDevice id. |
@@ -24,6 +25,7 @@ Run a spec against an app for a fixed duration.
 | `--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`. |
 | `--arm` | optional | Experiment label recorded in the run's metadata. Used by the campaign tool to tell one sweep cell from another. |
 | `--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. |
@@ -13,7 +13,7 @@ A run is not a unit test. The closer picture is: boot a fuzzer for an hour and s
 ```
 sanderling test --spec spec.ts --bundle-id com.example.app --duration 30m
  │
-  ├── launch the app under test (pass --clear-data to wipe app data first)
+  ├── launch the app under test (wipes app data first unless --clear-data=false)
  ├── boot the sidecar (or connect to Chrome on web)
  ├── bundle the spec, load it into the JS runtime
  │
@@ -63,4 +63,6 @@ A run ends when:
 - `--duration` elapses, or
 - the process is interrupted (Ctrl+C).
-Additional conditions (`--max-steps`, `--exit-on-violation`, hard crash handling) land in the [v0.1.0 milestone](https://github.com/priyanshujain/sanderling/milestone/1).
+- `--max-steps` is reached, or `--exit-on-violation` was passed and a property was violated.
 Hard crash handling lands in the [v0.1.0 milestone](https://github.com/priyanshujain/sanderling/milestone/1).
@@ -0,0 +1,15 @@
 # Skills for writing sanderling specs
 Agent skills for adopting sanderling: getting it running against your app, writing
 property specifications, reviewing them for the failure modes that make a spec
 look like it works when it does not, and reading a run honestly.
 Copy the ones you want into your agent's skills directory (`.claude/skills/` for
 Claude Code) or point your agent at this directory directly.
 Start with `sanderling-setup`, then `sanderling-spec-authoring`. Run
 `sanderling-spec-review` over anything before you trust it.
 The reasoning behind the rules these encode is in
 [docs/development/design-principles.md](../docs/development/design-principles.md),
 section 8 in particular.
@@ -0,0 +1,420 @@
 ---
 name: sanderling-property-patterns
 description: Decide what a sanderling spec should assert. A catalogue of property shapes that are sound (cross-panel agreement, bounds on an effect, counting actions against effects, input and navigation invariants), each with the tempting unsound version beside it. Use when starting a spec, when adding a property to one, or when a property keeps convicting an app that behaved.
 ---
 # Choosing what to assert
 You have sanderling driving your app and now you have to say what must be true.
 This is the hard part, and it fails in two directions: you freeze, or you write
 six properties none of which can ever be false.
 One rule orders everything below. **Soundness outranks detection.** A property
 that convicts more often and is sometimes wrong is strictly worse than one that
 convicts less and is never wrong, because a false conviction costs someone a day
 and then costs the whole suite its credibility. When a property cannot establish
 what it needs, it declines.
 Each shape below gives the sound form and the tempting form next to it, because
 the tempting one is usually what gets written first. The examples are from the
 two specs in this repo: `replay-ui/sanderling/spec.ts` (sanderling fuzzing its
 own trace browser) and `examples/folio/sanderling/spec.ts` with
 `examples/folio/sanderling/predicates.ts` (a KMP finance app).
 Once you have written properties, run `sanderling-spec-review` over them. It
 audits what this file helps you build.
 ## 1. Two parts of the UI derive the same fact and must agree
 Reach for this first, always. If your app shows the same number in two places,
 or shows a thing and a count of that thing, or renders a list and a selection
 into that list, you have a property and you do not have to think about windows,
 calibration, or attribution to write it.
 It is the strongest shape available. It holds on any run against any data, so
 nothing needs recalibrating when a fixture changes; it needs no reasoning about
 which action caused what; and an app that drifted on one of the two paths cannot
 satisfy it. It is the backbone of `replay-ui/sanderling/spec.ts`, which states it
 three times over: the toolbar's step count against the number of rows the list
 renders, the toolbar's step against the step the screenshot panel built its URL
 from, and the tab badge's violation count against the number of rows the
 violations panel shows.
 ```ts
 const stepCountMatchesTheList = always(() => {
  const current = toolbar.current;
  const rows = stepRows.current;
  if (!current || current.stepCount === null || rows.length === 0) return true;
  return current.stepCount === rows.length;
 });
 ```
 **What goes wrong: reading the second value off the wrong element.** Scope each
 reading to the panel you mean, by name, not by position in the tree.
 ```ts
 // tempting: the first screenshot on the page
 s.ax.find({ "data-testid": "screenshot" })
 // sound: the before panel's screenshot
 s.ax.find([{ "data-testid": "state-before" }, { "data-testid": "screenshot" }])
 ```
 Both versions pass most of the time. The fuzzer put the before panel on another
 tab, which left the after panel's image first on the page, and the first version
 fired against a UI that was behaving correctly.
 **What else goes wrong: never getting both readings onto one step.** This
 shape's failure mode is vacuity, not false conviction, which makes it quiet. An
 undirected run over replay-ui went 40 steps without switching a single tab out
 of roughly 15 clickable elements, leaving both tab-facing properties vacuously
 true. The fix is in the action tree, not the property: give the action that
 brings the second reading into view its own weight.
 ```ts
 const switchATab = actions(() => {
  const tabs = tabElements.current;
  return tabs.length === 0 ? [] : [Tap({ on: from(tabs).generate() })];
 });
 export const actionsRoot = weighted(
  [25, switchATab],
  [20, showAViolatingStepWithItsPanel],
  [25, defaultActions],
 );
 ```
 Weighting one half is usually not enough, and this is the part that surprises
 people. `badgeCountMatchesThePanel` needs a badge, which a tab strip renders
 only for a step that has a violation, and a panel to compare it against, which
 exists only while a particular tab is selected. Undirected actions put both on
 the same step 0 times in the 80 steps of replay-ui's first dogfood run. Aiming
 at the violating step alone just moved the misses to the other side: still 0
 judged. `showAViolatingStepWithItsPanel` in that spec aims at both halves in
 sequence, selecting a violating row and then opening a panel if none is up.
 It also opens the *after* panel deliberately, because the before panel's
 screenshot is what `screenshotShowsTheSelectedStep` reads, and covering it up
 would buy one property's evidence with another's. When two properties read the
 same screen, an action tree can starve one to feed the other, and nothing in the
 run output will say so.
 ## 2. An effect must not exceed what the actions could have caused
 When the app has an effect you can measure (money moved, rows added, a counter
 climbed), state a bound on it rather than a prediction of it.
 **Prefer an upper bound to an equality.** This is the single most valuable
 sentence in this file.
 `examples/folio/sanderling/predicates.ts` states one rule about one app both
 ways, so the two are worth reading side by side. Each line is the last line of
 its predicate, after the guards, at a step where exactly one submit sits in the
 window:
 ```ts
 // sound, committedAmountExceedsOneSubmit: the violation is moving by MORE
 // than the one submit in this window could account for
 Math.abs(currAccountBalance - prevAccountBalance) > typedAmount
 // tempting, submitChangesBalanceByTypedAmount: it moved by exactly what I typed
 Math.abs(currTotalBalance - prevTotalBalance) === typedAmount
 ```
 Both catch the bug, because a double submit moves the balance by twice the typed
 amount. Only the second also convicts an app that behaved. A balance that has
 not moved is a commit still in flight (folio's `createTransaction` runs in a
 coroutine), a submit the app rejected, or a tap that never landed, and none of
 those is evidence of anything.
 The asymmetry is the point. Moving by more than one submit's worth is not
 something a correct app can do, so the bound needs no case for any of the three.
 The equality needs a case for each, and every one you forget is a false
 conviction. Compare the two guard stacks and the price is exactly legible: the
 equality declines on `confirmedApplied` and on `acrossRelaunch`, and the bound
 carries neither, because a submit that may not have landed and a restart that
 may have eaten the commit both leave the balance under the bound anyway. Those
 are the two facts the runner cannot promise (see below), and needing to guard
 against both is a cost of the equality, not of the app.
 You do give something up, so make the trade deliberately. A bound cannot see a
 balance that moved by *less* than the typed amount, and for a ledger that is a
 real bug. The question to settle before giving it up is whether your readings are
 tight enough to tell "moved by less" from "has not finished moving yet". If they
 are not, the equality was never detecting that bug either; it was reporting it at
 random.
 The bound has one precondition, and it is the same one as shape 3: it bounds the
 effect by what the actions in the window could have caused, so the window has to
 count every action that could cause the effect. Miss one and the bound is not a
 bound.
 ## 3. Count the actions, not the amounts
 The same bound, stated in counts. One action must not produce two effects.
 ```ts
 !committedTransactionsExceedSubmits({
  countsBefore: homeTxnCounts.previous ?? null,
  countsAfter: homeTxnCounts.current,
  submitsInWindow: submitsSinceCounts.current,
 })
 ```
 Reach for this whenever the effect is countable. No arithmetic on values the UI
 formatted and you parsed back, no float precision to reason about, and it stays
 sound however wide the window between two readings gets, since both sides
 accumulate over the same window.
 It has exactly two failure modes and both are about the window. Neither makes it
 unsound. Both make it useless, quietly.
 **The window has to close often enough to attribute anything.** The window opens
 when you last read the fact and closes when you read it again, so a run that
 wanders away from that screen accumulates budget on one side of the bound
 without accumulating evidence on the other. Measured on a real iOS run: it went
 from step 19 to step 136 without returning to the screen the property reads,
 giving a transaction rise of 15 against a window of 37 submits. 15 is not more
 than 37, so nothing was reported. The same run also gave 4 against 7, 6 against
 13, and 1 against 1. Sound throughout, detected nothing.
 The obvious fix is to read the fact somewhere the run visits often. The better
 one, when the wide window is the app's own shape rather than an accident, is to
 **state the same rule a second time over a narrower window**, which is what
 folio's spec now does:
 ```ts
 const submitCommitsOneTransactionPerAction = always(
  next(
    () =>
      !committedTransactionsExceedSubmits({ /* Home's counts, wide window */ }) &&
      !committedAmountExceedsOneSubmit({ /* this account's balance, narrow window */ }),
  ),
 );
 ```
 The counting form can only close its window on a Home reading, and a walk that
 stays inside the transaction flow leaves it hundreds of steps and dozens of
 submits wide. The second conjunct says the same thing in money about the one
 account whose screen the walk is already on, and the transaction flow redraws
 that balance on nearly every frame, so its window is usually a single action
 wide, narrow enough to tell one commit from two. One rule, two windows, and the
 narrow one is where the detection actually comes from.
 That only works because the two readings are kept from spanning two accounts:
 `readAccountBalance` drops its carrier on every route that is not the ledger or
 the transaction screen, transition frames included. A narrow window buys nothing
 if the pair it compares straddles two different subjects.
 **The window must not be spent on actions that provably could not cause the
 effect.** A bound inflated by taps that commit nothing is a bound the app can
 never exceed, which is slack a real double submit hides behind. Folio's
 transaction submit is `clickable(enabled = amount.isNotBlank())`, so a tap with
 an empty field never fires at all, and the app's own `parseCents` refuses
 anything outside `^\d+(\.\d{1,2})?$` or parsing to zero. Measured over four
 recorded Android runs, 19, 11, 25 and 25 of 35, 26, 42 and 42 submit taps landed
 with the amount field empty, which is roughly half the budget in every one.
 `submitCouldCommit` in `predicates.ts` is that rule, and note how narrowly it is
 drawn. It returns false only where folio's own code **must** have refused, and
 returns true for anything it cannot rule out, including an undefined reading and
 an amount too large for the app to hold. Over-counting costs a detection;
 under-counting convicts a healthy app.
 Establishing that an action could not have had an effect is app knowledge, not
 something the runner can tell you, and it has to come from the frame the tap
 read. Folio reads the amount field on the landing frame, which is sound because
 the tap changes nothing about it and one action runs per step.
 `element.enabled` is on every `AccessibilityElement` for the general case,
 though whether your platform populates it honestly is worth checking on a real
 tree rather than assuming.
 The mirror of this rule matters just as much: an action whose effect you cannot
 rule out **must** be counted. Leaving out submits whose dispatch the runner
 could not confirm is what once convicted a healthy app here, when the property
 saw a transaction rise of one against a window of zero.
 ## 4. A value the user can reach must stay inside its legal range
 Anything the user can type, or a URL can carry, or a deep link can set, is
 attacker-controlled input to your app even when the attacker is a fuzzer. The
 property is that it stays legal, and it is cheap: one reading, no window, no
 attribution.
 ```ts
 const selectedStepIsInRange = always(() => {
  const current = toolbar.current;
  if (!current || current.step === null || current.stepCount === null) return true;
  return current.step >= 1 && current.step <= current.stepCount;
 });
 ```
 Two things make that sound. The bound comes from the app's own reading of how
 many steps the run has, not from a number you typed after looking at a fixture.
 And it asserts legality rather than a prediction:
 ```ts
 // tempting: I tapped next, so it must now be on step n + 1
 toolbar.current.step === (toolbar.previous?.step ?? 0) + 1
 ```
 which is false at the end of the run, false when the tap did not land, and false
 whenever the app is within its rights to clamp. Assert what must not happen.
 ## 5. State machine and navigation invariants
 Every screen with a selection, a mode, or a route has invariants that are true
 by construction and therefore worth stating, because "by construction" is
 exactly what breaks.
 **Exactly one, not at least one.** The looser version is the tempting one and it
 gives up the interesting half of the bug.
 ```ts
 const exactlyOneStepIsSelected = always(() => {
  const rows = stepRows.current;
  if (rows.length === 0) return true;
  return rows.filter((row) => row.active).length === 1;
 });
 ```
 Two selected rows is a stuck selection. Zero is the toolbar showing a step the
 list has no row for, which is what an off-by-one or a failed clamp looks like
 from the list's side, and `>= 1` would never see it.
 **A view change must not be a navigation.** Switching a tab, opening a menu or
 toggling a theme must leave the app where it was.
 ```ts
 const switchingTabsKeepsTheStep = always(
  next(() => {
    const previousTabs = activeTabs.previous;
    const previousToolbar = toolbar.previous;
    const currentToolbar = toolbar.current;
    if (previousTabs === undefined || previousTabs === activeTabs.current) return true;
    if (!previousToolbar || !currentToolbar) return true;
    return previousToolbar.step === currentToolbar.step;
  }),
 );
 ```
 Note the guard: it declines unless the tab strip actually changed. A property
 about an event must first establish that the event happened.
 The tempting unsound version of a navigation property is asserting the route you
 were hoping for, `route.current === "home"` after tapping submit. The app is
 within its rights to show a validation error and stay, and folio does exactly
 that for an amount of zero. State what must not happen, not what you wanted to.
 Deriving the route at all deserves care, and folio's `routeOfFrame` is the
 pattern: it returns the screen only when exactly one screen marker is in the
 tree, and null otherwise. Android's hierarchy dump carries the outgoing and the
 incoming screen together on 425 of 1879 steps measured across 17 runs, better
 than one frame in five. Such a frame is evidence about neither screen, and
 ranking the markers to pick one is how a spec convicts itself on an animation.
 ## 6. The ones you get for free
 ```ts
 import { noUncaughtExceptions, noLogcatErrors } from "@sanderling/spec/defaults";
 export const properties = { noUncaughtExceptions, /* yours */ };
 ```
 Export `noUncaughtExceptions` before you write anything of your own. It costs a
 line, it needs no app knowledge, and a fuzzer typing `'; DROP TABLE--` and a
 4096-character string into every field it finds will surface real breakage
 through it. `noLogcatErrors` is stricter and Android-only; it holds trivially
 elsewhere, so it is worth turning on once you know your app's log hygiene can
 support it.
 They do not substitute for the shapes above. An app can be thoroughly wrong
 about money without throwing once.
 ## The rules that cut across all of them
 **Absence is unknown, never a default.** Extractors return null when the element
 is not there, and a property handed null declines. `0`, `""` and `[]` are the
 values that turn a property into one that fires on healthy runs: folio's
 balances once parsed as `0` on web, so the check became `|0 - 0| === typed` and
 was false at every healthy submit. An empty list has the same problem in the
 other direction, and it is worse because it looks reasonable. Android renders
 Home's own node a frame or two before its list, so `findAll` over the cards
 comes back empty while the screen already claims to be Home. That is unknown,
 not "no accounts", and reading it as zero accounts killed folio's counting
 invariant outright: `countsBefore` was `{}` at every evaluation point of all 17
 runs measured.
 **Attribution needs injective keys.** If two distinct objects can produce the
 same identity key, a value silently jumps between unrelated series. Merged UI
 text is the usual culprit: web collapses an account card into a single node
 whose text runs the name into the count, so an account named `Travel1` with 25
 transactions and one named `Travel12` with 5 both render `TRTravel125
 transactions`. No function of that string can separate them. Where a key can
 collide, drop the reading rather than guess: `homeTxnCountsOf` leaves out any
 name carried by more than one card, because subtracting two different accounts'
 counts convicts a healthy app of double-submitting.
 **Match whole keys, not endings.** `endsWith` attribution judges an older
 account named `Emergency Fund` when the user typed `Fund`: have the new card
 clipped out of the reading, the way a list clips any card, and the old account
 is convicted for money it has held all along. Substring matching is looser
 still. Build every form of the key the platforms can produce and compare each
 one whole, which is what `createdAccountHasNonZeroBalance` does with
 `account.name === typed || account.name === initialsOf(typed) + typed`. Note
 that this bought detections as well as soundness: under the suffix test, a name
 that two cards ended with was thrown away as unattributable rather than matched
 to the one card that actually carried it.
 **What the runner could not promise.** `state.lastAction` is
 `Action & { applied: true | null; relaunched: true | null }`, and collapsing any
 of its states is unsound:
 - `null`, the whole field, means no action ran
 - `applied: true` means the runner saw the dispatch succeed
 - `applied: null` means it was dispatched and nobody can find out whether it
  landed, because an RPC deadline can fire after the tap arrived
 - `relaunched: true` means the runner had to bring the app back to the
  foreground after this action, so the two readings straddle a restart
 One rule covers the last two, and it is the rule that decides shape 2 for you.
 An action the runner cannot fully vouch for **still counts toward a bound on
 what the app could have done**, and it **never licenses attributing an effect to
 it**. So a bound counts it and an equality has to decline on it. That is why
 `committedAmountExceedsOneSubmit` needs no `confirmedApplied` guard and no
 `acrossRelaunch` guard while `submitChangesBalanceByTypedAmount` needs both: a
 property demanding the effect of an action that may never have run, or that a
 restart may have swallowed, convicts the app of the runner's own uncertainty.
 `relaunched` is the same shape of fact as `applied`, applied to app state rather
 than to dispatch. The action itself did happen. What nobody can promise across
 it is that the process ran continuously, that the commit survived, or that the
 screen is showing the same slice of the same list it was. So a property assuming
 continuous state declines, via `acrossRelaunch(lastAction)`, and folio uses it
 in three places: `createdAccountHasNonZeroBalance` declines because Home redraws
 from the top and the card carrying the typed name may be an older account laid
 out where the new one used to be, the equality property declines because it
 demands an effect, and `countSubmitsInWindow` uses it to **stop trusting its own
 refusal evidence**, since a relaunch is the one thing that can put a form state
 on screen other than the one the tap read.
 Both fields are `true | null` rather than booleans, and that is deliberate: only
 the positive report is a fact the runner can vouch for, so `null` is "not
 reported" rather than "did not happen". `relaunched` shows why it has to be that
 way. Web and iOS cannot read the foreground at all, so they never relaunch the
 app and equally cannot promise it never restarted, and a `false` there would be
 a claim nobody is in a position to make. Read the absence as a guarantee and you
 have made the same mistake as reading a missing value as zero, one level up.
 **Testing a property means both directions, every time.**
 - it fires on the bug it exists to catch
 - it stays silent on a run where the app behaved
 The second is the one people skip and the one that catches unsoundness. Build
 the fixture where the effect happens legitimately, at the boundary the property
 draws, and assert silence: the commit that is still settling, the submit the app
 refused, the card that scrolled into view rather than being created, the pair of
 readings taken either side of a relaunch. A property you have only ever seen go
 red is a property you have half tested.
 Then hand it to `sanderling-spec-review`, which will ask how many steps it
 actually judged on a real run.
@@ -0,0 +1,210 @@
 ---
 name: sanderling-run-triage
 description: Work out what a finished sanderling run actually proves. Use before trusting a green run, before filing the bug a red run seems to show, and any time the exit code is the only thing anyone has looked at.
 ---
 # Reading a run honestly
 A run produces one number that is easy to read and several that are worth
 reading. The easy one says whether a process finished. It does not say whether
 anything was checked, whether what was checked was your app, or whether the
 violation it reports is about the app at all.
 Work through the sections in order and report what you established and what you
 could not. "This run is not evidence, and here is the signal that says so" is a
 complete and useful answer.
 ## 1. The exit codes
 - **0** means the run completed. It does **not** mean no violations. Without
  `--exit-on-violation` a run that recorded violations still exits 0: measured
  on a ten step web run that recorded two, `run complete: 10 steps` and
  `2 violation record(s)`, exit code 0.
 - **2** means the run recorded a violation under `--exit-on-violation` and
  stopped there. The same ten step run with the flag exits 2 after four steps.
 - **1** means the harness broke. A bad target gives
  `error: launch app: page load error net::ERR_UNSAFE_PORT` and exit 1, and
  writes no run directory at all, because the trace is created after the launch
  succeeds.
 Anything other than 0 and 2 means the run did not complete, and a missing
 `trace.jsonl` under a 0 or a 2 means there is nothing to judge rather than
 nothing to report.
 Exit 2 is not a conviction. `.github/scripts/folio-run.sh` is the worked example
 worth reading in full: it exists because a thrown predicate reaches exit 2 by the
 identical path a real conviction does, and so does a violation of a real but
 unrelated property in the same spec. It sorts a trace's violations three ways,
 by name and by `is_error`: convictions of the properties the leg gates on,
 predicates that threw, and other real violations the leg has nothing to say
 about. Do the same sort by hand before you call a 2 a finding.
 ## 2. Reading a witness
 Witnesses live in `trace.jsonl`, one object per step under `witnesses`, keyed by
 property name. A real conviction and a real throw from the same run:
 ```json
 {"step": 4, "violations": ["countStaysUnderThree"],
 "witnesses": {"countStaysUnderThree": {
   "reason": "predicate false", "step": 4, "detected_step": 4,
   "extractors": {"count": 3}}}}
 {"step": 5, "violations": ["throwsOnceCountIsFour"],
 "witnesses": {"throwsOnceCountIsFour": {
   "reason": "Error: boom: no reading for this screen at <eval>:501:37(14)",
   "is_error": true, "step": 5, "detected_step": 5,
   "extractors": {"count": 4}}}}
 ```
 `step` is where the failed obligation was armed and `detected_step` is where the
 evaluation produced the violation; for a deferred obligation (a `next`, an
 `eventually`) they differ, and `extractors` is `detected_step`'s state, not
 `step`'s.
 The discipline is one sentence: open the witness and confirm those values could
 actually produce that verdict. An iOS witness read `typedAmount = 0`, and
 `submitChangesBalanceByTypedAmount` in `examples/folio/sanderling/predicates.ts`
 returns true at `typedAmount === 0` before it compares anything. So the trace
 appeared to show a conviction that could not have happened. The verdict was real
 and the artifact was lying, and until that was resolved neither the bug report
 nor the fix could be trusted.
 When a witness value looks impossible, suspect the reading before you suspect
 the property. Values reach a witness through the driver, and the driver can be
 wrong in ways the spec cannot see: erasing a text field used to leave characters
 behind, because a backspace only deletes to the left of the cursor and the
 runner taps the field's centre, and 7 of 19 measured `InputText` observations
 left residue that the spec then reasoned about as if it were the typed value.
 Two more things the witness tells you, if the spec extracts them. folio declares
 `extract("lastAction", s => s.lastAction)` precisely so they land in the trace:
 `applied: true` means the runner saw the dispatch succeed, `applied: null` means
 it was dispatched and nobody knows whether it landed, and `relaunched: true`
 means the app restarted between the two readings. A property attributing an
 effect to an action of unknown fate is unsound; see `sanderling-spec-review`.
 Finally, a property violates once. After it fires, its residual stays `false`
 (or `{"op": "error", ...}`) for every remaining step and it is never evaluated
 again. Measured across steps 4 to 10 of that run, `countStaysUnderThree` reads
 `{"op": "false"}` at every step after the first. So the violation count is a
 count of distinct properties, not of occurrences, and everything after a
 property's first violation is unchecked by that property.
 ## 3. A green run fails in two ways
 Either it checked nothing, or it checked and the fuzzer never reached the bug.
 These need opposite responses (fix the spec or the hooks; spend more budget or
 better actions) and the exit code distinguishes neither.
 The first is not a hypothetical. Against an empty page, six steps, exit 0, `no
 violations`, and `countNeverNegative` judged **0 of 6**: its extractor returned
 null every step, its guard short-circuited, and its residual read `{"op":
 "true"}` at every step, exactly as it reads when it compares real values.
 So count, per property, the steps where its guard passed and it compared
 something (**judged**) against the steps where it returned true without
 comparing anything (**declined**). `.github/scripts/replay-ui-summary.sh` does
 this for the replay-ui spec and prints a judged/declined table for exactly this
 reason. To do it by hand from a trace:
 - fold `extractor_changes` forward per step. Only extractors whose value changed
  are recorded, so a step with no entry for an extractor means unchanged, not
  absent. Measured: `{"count": {"prev": 0, "curr": 2}}` at one step and no
  `count` entry at the next.
 - skip steps carrying `skipped_verification` or `transitional`. They advance
  nothing.
 - apply each property's own guard to the folded values and count.
 That script also carries the honest warning about this technique: restating a
 property's guard outside the property is a second copy that can drift, so it
 checks that the trace's property names still match the ones it counts and that
 the spec still declares the extractors it reads, and it fails loudly when either
 moves.
 Do not try to read judged-versus-declined off `residuals`. `always(p)` residuals
 to `{"op": "true"}` whether `p` compared real values or short-circuited, so the
 two are indistinguishable there.
 ## 4. A red run fails in two ways
 Either a property was proved false about the app, or a predicate threw.
 `is_error` in the witness separates them and they mean opposite things.
 A conviction is a claim about the app. A throw is a claim about the spec, and it
 is worse than an unhelpful result: the property is violated from that step on
 whatever the app does, so it checks nothing for the rest of the run, and under
 `--exit-on-violation` the run ended there so nothing past it was checked by
 anything. The `reason` carries the JavaScript error and its location, which is
 usually enough to find it: `Error: boom: no reading for this screen at
 <eval>:501:37(14)`.
 The third case is a real violation of a property that is not the one you are
 asking about. It is a finding, and it is somebody's bug, but the run has nothing
 to say about the question you asked it. Name the property before you claim the
 result.
 ## 5. When a run is not evidence at all
 Some runs never got far enough for any of the above to matter, and every one of
 them exits 0 and reports no violations.
 **It never reached the app.** A launch flake left a fuzzer on the device
 launcher for 200 steps in 65 seconds, two nodes per snapshot, exit 0, no
 violations (issue #81). The check is that the app's own marker appears in the
 trace at all: the folio CI leg greps for `"AddTransactionScreen"` and fails the
 run when it is absent, which is more honest than any exit code it could read.
 The run's stdout also carries `app left foreground; relaunching` with the
 package it found instead.
 **The hierarchy is a handful of nodes.** `nodes=` in each step line is the
 cheapest signal there is. Measured: 6 on a four-element page, 2 on an empty one.
 A run whose `nodes` never leaves single digits is looking at a launcher, a
 crash screen, or a page that failed to boot.
 **It never left one screen.** `screen=` constant for the whole trace, or a
 `route` extractor that never changes value.
 **Steps far faster than the run's own median.** Take the per-step deltas from
 each step's `timestamp` and compare them against the run's median. A stretch of
 steps at a fraction of it is a driver that is not waiting for an app, because
 there is no app to wait for: 200 steps in 65 seconds is 325 ms a step, against
 seconds a step for a run that is driving something real.
 **It spent its budget on one action.** Count `next_action` by kind and selector.
 A run whose actions are one selector explored nothing, whatever its step count.
 None of these change the exit code. All of them change what the run proves,
 which is nothing.
 ## 6. `skipped_verification`, `transitional`, and the judged count
 The runner skips the verifier for a step whose hierarchy was still moving: an
 Android NavHost mid cross-fade after the retry budget, or a hierarchy fetch that
 failed or came back empty. Pushing such a tree would poison the previous/current
 extractor advance and make the next clean step convict a healthy app, so the
 step is recorded for replay and judged by nothing. `transitional` marks the
 tree; `skipped_verification` is set exactly when the verifier was skipped.
 The run says so itself:
 ```
 7 step(s) judged by nothing: the screen was still moving when it was read
 ```
 Subtract it. `run complete: 240 steps` with that line is a 233 step run for
 every purpose that matters, and `replay-ui-summary.sh` reports the pair as
 "N steps recorded, M verified" for the same reason. A run with many of these is
 telling you the driver could not get a clean read of your app, which is a
 finding about the setup and worth chasing rather than quietly accepting the
 smaller number.
 ## Reporting
 For any run, report: the exit code and whether `--exit-on-violation` was set;
 steps recorded against steps verified; per property, judged against declined;
 for every violation, its `is_error` and the witness values you actually opened;
 and which of the section 5 signals you checked. Name the step behind any claim.
 A run is evidence only for the properties that judged, and only for the app it
 was actually looking at. Everything else it produced is a log.
@@ -0,0 +1,260 @@
 ---
 name: sanderling-setup
 description: Get sanderling running against an app that is not folio. Use before writing a spec for a new app, when deciding what test hooks the app needs, and when a run will not start or starts and sees nothing.
 ---
 # Getting sanderling onto your app
 The goal of setup is not a run that finishes. It is a run whose output you can
 believe. Two things decide that, and both are usually treated as chores: the
 handles the app exposes, and the state the app starts in. Everything else here
 is plumbing.
 Every flag below is one the binary accepts. `sanderling test -h` is the
 authority, not this file and not the manual: the manual currently documents
 `--launcher-activity`, which the binary answers with `flag provided but not
 defined`. Check before you use a flag you have not seen work.
 ## 1. Install, then check the host
 The CLI installs from the release script, and the spec package from npm:
 ```sh
 curl -fsSL https://raw.githubusercontent.com/priyanshujain/sanderling/master/install.sh | bash
 npm install --save-dev @sanderling/spec
 ```
 Both come from the same release tag and the CLI bundles the package's TypeScript
 when it evaluates your spec, so they move together.
 `sanderling doctor` reports the host's readiness per platform and exits non-zero
 if anything is missing. On a Mac with no Android SDK it says:
 ```
 OK    adb on PATH
 FAIL  emulator on PATH or under ANDROID_HOME: not on PATH and ANDROID_HOME is unset
 OK    java 17+ on PATH
 FAIL  sidecar JAR is real (not placeholder): placeholder JAR embedded; run `make sidecar && make sanderling` to embed the real fat JAR
 error: 2 check(s) failed
 ```
 Scope it with `--platform web|android|ios|ios-device|all` (default `all`). Web
 needs a Chromium that launches headless. Android needs `adb`, an emulator on
 PATH or under `ANDROID_HOME`, Java 17 or newer, and the embedded sidecar JAR.
 iOS needs `xcrun` and `simctl`; `ios-device` adds `devicectl`, the macOS usbmuxd
 socket, a connected paired device, and App Store Connect signing credentials.
 Read the doctor's Android result as advisory rather than final: its emulator
 check today looks only at PATH, `ANDROID_HOME` and `ANDROID_SDK_ROOT`, while a
 run also searches `~/Library/Android/sdk`, `~/Android/Sdk` and the Homebrew
 command-line-tools paths. The run's own error names every location it tried, so
 that is the one to trust. In the other direction, a missing SDK can surface
 during a run as `sidecar health check: context deadline exceeded` about thirty
 seconds in, which names the symptom and not the cause (issue #69). If you see
 it, go back to `sanderling doctor --platform android` before believing anything
 about the sidecar.
 Two traps if you build from source rather than installing a release. A plain
 `go build ./cmd/sanderling` embeds a placeholder sidecar JAR, so every Android
 run stops at `sidecar: binary built without -tags withsidecar`; `make sanderling`
 (or `make sanderling-android`) embeds the real one. And `go run ./cmd/sanderling
 test` collapses the process exit code: a run that exits 2 comes back from
 `go run` as 1 with `exit status 2` printed. Use the built binary whenever the
 exit code matters, which is always in CI.
 ## 2. Point it at the app
 Android takes the applicationId, boots an AVD with `--avd`, and picks between
 attached devices with `--device <serial>` as `adb devices` prints it:
 ```sh
 sanderling test --spec spec.ts --bundle-id com.example.app --avd Pixel_7_API_34
 ```
 iOS takes `--platform ios` and `--ios-device`, which accepts a simulator name or
 UDID, or a connected device's name, UDID, or CoreDevice id. `--ios-app-path`
 points at the `.app` bundle and is what makes clear-state real; see section 4.
 Web takes a URL as the bundle id:
 ```sh
 sanderling test --spec spec.ts --platform web --bundle-id http://127.0.0.1:8799/index.html
 ```
 The web target has to genuinely load. A page that boots to a blank canvas still
 produces steps, still exits 0, and proves nothing: folio's own web leg needs
 COOP/COEP headers or its sqlite worker never starts, which is why
 `.github/scripts/folio-run.sh` serves the build itself instead of using a stock
 static server. Confirm the app rendered before you read anything else.
 ## 3. Test hooks are a prerequisite, not a polish step
 This is the part that decides whether a spec is possible at all. The header of
 `replay-ui/sanderling/spec.ts` states it as the lesson it is:
 > The hooks it drives (data-testid, data-step, ...) were added to the UI for
 > this spec. Needing them is the lesson: a UI with no stable handles is a UI
 > nothing can assert on, and that is as true for a person writing a test as it
 > is for a fuzzer.
 A fuzzer is not asking for anything a human test author does not need. It is
 only less able to squint at a screenshot and guess. Budget the hooks as part of
 adopting sanderling, before the spec, not after the first vacuous run.
 `testTag` is the portable name. `internal/hierarchy/hierarchy.go` aliases it to
 `resource-id`, `identifier` and `accessibilityIdentifier`, so one selector
 matches on every platform. What you have to add differs:
 **Compose on Android.** `Modifier.testTag("AddAccountSubmit")` alone does not
 reach the accessibility tree. The tree only carries it when a root composable
 sets `semantics { testTagsAsResourceId = true }`. folio does this once, at the
 app root, through an expect/actual bridge:
 `examples/folio/app/shared/src/androidMain/kotlin/app/folio/ui/TestTagBridge.android.kt`.
 Without it every `testTag` selector matches nothing, every property over it
 declines, and the run goes green having checked nothing.
 **Web.** `data-testid` is the hook. Every `data-*` attribute on the element
 reaches the spec under `attrs`, camel-cased the way `dataset` does it, so
 `data-step-count` reads as `attrs.stepCount`. That is how the replay-ui spec
 reads a panel's own claim about which step it is showing rather than re-deriving
 it. Hooks that carry a value, not just an identity, are what make cross-panel
 agreement properties possible.
 **iOS.** `accessibilityIdentifier`, set via `.accessibilityIdentifier` in
 SwiftUI or UIKit. Compose Multiplatform maps `testTag` to it for you.
 Two rules about the names themselves. A `testTag` selector falls through to a
 substring compare, so `{testTag: "Sub"}` matches `AddAccountSubmit`: make each
 hook a whole distinct name rather than a fragment of another. And give every
 screen a marker of its own, because a route extractor is what lets a property
 decline on the screens it has nothing to say about.
 The check that a hook exists is not that you added it. It is that you can point
 at a step in a real trace where a selector over it resolved to a value.
 `sanderling-spec-authoring` covers which hooks a spec needs and in what order to
 add them; this section is about what each platform requires before any of that
 reaches the tree.
 ## 4. A run must start from a known state
 `--clear-data` defaults to true and is the difference between a repeatable run
 and a measurement of your own leftovers. A second run that inherits the first
 one's accounts, cache and completed onboarding diverges at step 1: the seed
 reproduces nothing, the two runs' step counts are not comparable, and any number
 you quote from the pair is noise.
 What "clear" reaches depends on the platform, and in two cases it silently
 reaches less than you expect:
 - Android wipes app data through the sidecar. On OEM builds that deny
  `pm clear`, pass `--android-app-path <apk>` and it uninstalls and reinstalls
  instead.
 - iOS simulator without `--ios-app-path` resets the data container only and
  prints `clear-state requested without an app path: resetting the data
  container only`. With the path it does a full `simctl` uninstall and install.
  The container wipe is a real reset and folio's own iOS leg relies on it; the
  reinstall path is the one that races FrontBoard.
 - iOS on a physical device without `--ios-app-path` does not clear at all. It
  prints `clear-state on a physical device requires --ios-app-path for a
  reinstall; skipping (state not cleared)` and carries on. A device run left on
  the default flag inherits every previous run's data.
 - Web clears cookies and the target origin's storage. It cannot touch your
  backend. If your app's state lives on a server, reset it yourself between
  runs.
 `--clear-data=false` is a legitimate choice in one situation: you have just
 installed a fresh build, so the app is already in clear state and an in-run
 reinstall would only add a failure mode. Outside that, a run that resumes is a
 run you cannot repeat.
 ## 5. The device does not have to be local
 Android talks to whatever adb server the environment names.
 `ADB_SERVER_SOCKET=tcp:host:port` (or `tcp:port` for a server on this machine)
 is read first, then the older `ANDROID_ADB_SERVER_ADDRESS` and
 `ANDROID_ADB_SERVER_PORT` pair, then the loopback default. The CLI shells out to
 `adb` and inherits it; the JVM sidecar resolves the same variables when it
 attaches to a serial.
 Two things to get right. Pass `--device <serial>` exactly as the remote server
 reports it: with no serial the sidecar's target is a local `localhost:5555`, not
 your remote device. And a serial that already looks like `host:port` is dialled
 straight at adbd, bypassing any server, which is a different path with different
 failure modes. A value the sidecar cannot parse fails the run rather than
 falling back to loopback, and that is deliberate: emulator serials are numbered
 per server, so a quiet fallback would drive whatever this machine calls
 `emulator-5554` and report the results as the remote device's.
 ## 6. What a first run prints
 A ten step web run, in full:
 ```
 bundled spec: 16532 bytes (sha256=71375ed5bfc7)
 bundled web spec: 33131 bytes (sha256=779bae3c8fee)
 spec loaded into verifier
 trace dir: runs/20260815-172356
 running for 1m30s or 10 steps, whichever comes first (seed=7)
 step index=1 screen="/index.html" nodes=6
 ...
 step index=10 screen="/index.html" nodes=6
 elapsed: 1.715s
 run complete: 10 steps
 no violations.
 ```
 `nodes=` is the first number to read and the cheapest lie detector you have. On
 that page, four elements plus html and body gave `nodes=6`. The same command
 against an empty page gives `nodes=2` for every step, and still exits 0 with no
 violations. If `nodes` is a handful and never grows, the run is looking at
 something that is not your app.
 `screen=` is the route marker your spec's screen hooks produce. A run where it
 never changes never left one screen.
 The summary can carry a third line you should never skim past:
 ```
 7 step(s) judged by nothing: the screen was still moving when it was read
 ```
 Those steps were recorded but no property judged them, so the run's step count
 and its checked count are different numbers. `sanderling-run-triage` is about
 what to do with that.
 Set `--max-steps` whenever you intend to compare two runs: a step budget is what
 makes them comparable, since duration alone does not. `--seed` fixes the PRNG,
 and seed 0 draws a random one and records it in `meta.json`.
 ## 7. The run directory
 Each run writes `<output>/<UTC timestamp>/`, containing `meta.json`,
 `trace.jsonl`, and one PNG per step under `screenshots/`. `--output` defaults to
 `./runs`.
 `meta.json` is the run's identity: seed, spec path, bundled spec sha256,
 platform, bundle id, start and end times, generator, `max_steps`,
 `duration_millis`, host, and the `--arm` label if you set one. Two runs that
 differ in any of those are different runs and cannot be pooled.
 If the app never launched, there is no run directory at all: the launch error
 comes before the trace is created. `error: launch app: ...` with nothing under
 `./runs` means the run never began, which is a different thing from a run that
 began and found nothing.
 Open a run with `sanderling replay <dir>`, which accepts either the parent runs
 directory or a single run directory.
 ## Reporting
 Say what you actually ran and what came back: the `doctor` output you got rather
 than the one you expected, the exact `sanderling test` command, the step count
 and the `nodes=` figure from the first run, and for each hook you added, the step
 in a real trace where a selector over it resolved. Name what you could not
 establish, particularly any platform you did not run on.
 Setup is finished when a property can be written that could fail. Write it with
 `sanderling-spec-authoring`, review it with `sanderling-spec-review`, and read
 the run it produces with `sanderling-run-triage`.
@@ -0,0 +1,353 @@
 ---
 name: sanderling-spec-authoring
 description: Write a sanderling spec for an app: test hooks, extractors, selectors, properties, and an action tree that reaches the states the properties read. Use when adopting sanderling for a new app, when adding a property to an existing spec, and when a run is green because it never reached the state the property was written for.
 ---
 # Writing a sanderling spec
 A spec is a TypeScript module the runner evaluates once per step. It exports
 `properties` and `actionsRoot`, plus an optional `setup` and `generator`.
 Writing one is easy. Writing one that would catch a real bug is not, because a
 spec that checks nothing looks exactly like a spec that checks everything: both
 are a green run.
 So the order below is arranged around getting evidence early that each piece
 reads what you think it reads. When the spec is written, audit it with
 `sanderling-spec-review` before trusting a green run from it.
 ## Write it in this order
 Hooks, then extractors, then **one** property, then run it and read the witness,
 then everything else. Writing six properties before the first run is how people
 end up with six that cannot fire, and nothing in the output tells you which.
 ## Hooks first
 Your app needs stable handles or nothing can name what it is asserting on. The
 hooks the replay UI's spec drives (`data-testid`, `data-step`) were added to the
 UI for that spec, and its header says why: a UI with no stable handles is a UI
 nothing can assert on, and that is as true for a person writing a test as it is
 for a fuzzer.
 Put a hook on the screen or route markers, on every container you will scope a
 lookup to, and on every fact you will read. `testTag` is the portable one: it
 surfaces as resource-id on Android and accessibilityIdentifier on iOS, and on
 web it resolves to `data-testid` or `id`.
 ## Extractors
 `extract(name, fn)` reads one fact off `state.ax` per step. `.current` is this
 step's value, `.previous` the last step's, `undefined` on the first step.
 Name every one. The name is what you get back later: `extractor_changes` in
 `trace.jsonl` carries the prev/curr pair for each extractor whose value moved,
 and the witness recorded at a violation carries the extractor values behind it,
 by name. An unnamed extractor shows up as `extractor_3`, which tells you nothing
 at the point you most need to know what the property was looking at.
 The rule that decides whether the spec is worth anything:
 > **Return `null` when the element is absent. Never `0`, `""`, or `[]`.**
 An unreadable fact is unknown, and a default turns unknown into a claim. Both
 directions bite. Folio parsed a missing balance as `0` and its property became
 `Math.abs(0 - 0) === typedAmount`, false at every healthy submit. Read a missing
 panel's row count as `0` and the property says the cart is empty when the truth
 is that the cart is not on screen. Where the ambiguity is real, call it unknown:
 an empty `findAll` is both "no rows" and "not drawn yet", and folio treats it as
 unknown, which costs the very first account of a run and buys back every card
 that arrived late.
 Extractors run before properties and action generators, and they may not read
 each other. If two readings must come off one parse, put the parse in a helper
 both call: `examples/folio/sanderling/predicates.ts` does this with
 `oncePerFrame`, keyed on the state object, since both hosts build a new state
 object per step.
 ## Selectors
 `ax.find` and `ax.findAll` take a string (`"id:CartBadge"`), an object
 (`{id: "CartBadge"}`), or an array of objects for a path. Element handles carry
 their own `.find` / `.findAll` scoped to their subtree.
 The two forms resolve identically: an object key is matched by the same rule its
 string form uses, so `{id: "X"}` and `"id:X"` can never pick different elements.
 What differs is the rule per key. Measured against an Android dump holding
 `com.app:id/CartBadge`, whose content-desc is `Cart, 3 items`, alongside
 `AddAccountSubmit`:
 | Selector | Resolves to |
 |---|---|
 | `{id: "CartBadge"}` | the badge: `id` matches the whole resource-id, or the part after `:id/` |
 | `{id: "Sub"}` | nothing: `id` wants a whole name, not a fragment |
 | `{testTag: "CartBadge"}` | the badge: `testTag` reaches resource-id on Android and accessibilityIdentifier on iOS |
 | `{testTag: "Sub"}` | `AddAccountSubmit`, because every key outside the `id` / `desc` / `descPrefix` special cases is a **substring** match |
 | `{desc: "Cart"}` | the badge: `desc` takes the whole description, or an iOS merged label starting `Cart, ` |
 `testTag` is the portable key and the one to reach for, but name the element in
 full. A substring match on `Sub` is not a match, it is a coincidence, and it
 will one day pick a different control.
 A selector that matches nothing makes every property over it vacuous, and
 nothing anywhere reports that. This is why the selector you verify is the one
 you found a real value for in a witness, not the one that looked right when you
 wrote it.
 **Scope the lookup to a container instead of taking the first match on the
 page.** From `replay-ui/sanderling/spec.ts`: an earlier draft of
 `screenshotShowsTheSelectedStep` took the first screenshot on the page, the
 fuzzer put the "before" panel on another tab, which left the "after" panel's
 image first, and the property fired against a UI that was behaving correctly. It
 now reads `s.ax.find([{ "data-testid": "state-before" }, { "data-testid": "screenshot" }])`
 and is scoped to the panel it means.
 A screen marker is not enough scope on its own during a navigation. Android's
 hierarchy dump carries the outgoing and the incoming screen together on 425 of
 1879 steps measured across 17 runs, better than one frame in five, so a find
 scoped to a screen the app has already left still resolves. Decide the route once
 per frame, return `null` when more than one screen marker is present, and have
 every reading take its answer from there. `routeOfFrame` in folio's
 `predicates.ts` is that rule and carries the measurements.
 ## Properties
 `always(f)` requires `f` at every step. `next(f)` inside it compares this step
 to the next, which is how you state "this action had that effect". `now(f)`
 evaluates at the current step inside a formula body.
 `eventually(f).within(n, "steps" | "seconds" | "milliseconds")` requires `f`
 before the window closes; unbounded, it never fails a finite run. At the top
 level an `eventually` is one goal for the whole run, armed once and discharged
 for good the first time it holds; written inside `always` it re-arms at every
 step, which asks for the window to be met from everywhere. Every formula has
 `.implies`, `.and`, `.or`, `.not`.
 The stock properties are in `@sanderling/spec/defaults`. Put
 `noUncaughtExceptions` in every spec: it fails when the run captures an uncaught
 throwable or a `Sanderling.reportError` call, it needs no hooks and no
 calibration, and it is free. `noLogcatErrors` (also exported from
 `@sanderling/spec/defaults/properties`) fails on any error-level logcat line and
 is Android-only, holding vacuously elsewhere.
 ## What makes a good first property
 Prefer a **cross-panel agreement**: two parts of the UI that derive the same fact
 by different paths must say the same thing. The toolbar prints a step count and
 the list renders rows; a badge counts violation records and the panel counts the
 rows it can show for them. Those hold on any run, so they never need
 recalibrating against a fixture, and an app that gets the fact wrong in one of
 the two places cannot satisfy them however it was driven there.
 `replay-ui/sanderling/spec.ts` is six of these plus `noUncaughtExceptions`, and
 its header explains the choice.
 Contrast a property that needs the fuzzer to reach a specific state, like
 folio's "a submit moves the balance by exactly the amount typed". That is where
 the real bugs are, and it is the harder thing to keep honest: it needs an action
 tree that reaches the state, a window that closes often enough to bound what
 happened inside it, and attribution that cannot blame the wrong action. Folio's
 counting form went 117 steps between two readings on one iOS run and gathered 37
 submits against a rise of 15 transactions, which is perfectly sound and says
 nothing at all; the fix was to state the same rule over a number the app redraws
 on nearly every frame, so the window is usually one action wide. Write these
 second, and read `sanderling-spec-review` before you believe one.
 Whichever you write, name the input that makes it return false before you move
 on. If you cannot, it is decoration.
 ## Actions
 `actions(() => Action[])` returns the candidate actions for this step and the
 picker chooses one. The verbs are `Tap`, `DoubleTap`, `LongPress`, `InputText`,
 `Scroll`, `Swipe`, `PressKey`, and `Wait`. The built-in generators are `taps`,
 `doubleTaps`, `longPresses`, `typing`, `scrolls`, `swipes`, `pressKeys`, and
 `waitOnce`; `defaultActions` bundles them at taps and typing 100, scrolls 50,
 swipes 25, double taps 10.
 `weighted([n, generator], ...)` composes them with relative weights.
 `whenRoute(routeExtractor, routes, body)` runs `body` only on the named screens.
 The optional `setup` export runs before `actionsRoot` for as long as it returns
 actions, which is where login and onboarding belong; it re-engages on its own if
 the app logs itself out mid-run. Values come from `from(items)`,
 `integers().between(min, max)`, `strings().length(min, max).alpha()`,
 `emails().domain(host)`, and `edgeCaseText()`, all drawn from the run's seeded
 PRNG so a seed replays exactly.
 **The default enumeration explores, but reaching a specific interesting state
 usually needs a weighted action of your own.** With about 15 clickable elements
 on the replay UI's page, an undirected run went 40 steps without switching a
 single tab, which left both tab-facing properties vacuously true. Its badge
 agreement is worse: it needs two readings on one step, a badge, which only a
 step that has a violation renders, and a violations panel to compare it against.
 Undirected actions put both on the same step **0 times in the 80 steps of the
 first dogfood run**. The property was reachable in principle and judged nothing
 in practice, and aiming at the step alone just moved the misses to the other
 side, 0 judged either way. It took an action that selects a violating step and
 then opens a panel if none is up. Folio weights its transaction chain at 45 for
 the same reason: both balance properties observe that flow and nothing else
 reaches it.
 So for every property, name the action in the tree that puts everything it reads
 on screen at the same step. If there is none, add one, and give it enough weight
 that a short run gets there.
 ## Soundness outranks everything else here
 A property must never convict an app that behaved correctly. A property that
 convicts more often and is sometimes wrong is strictly worse than one that
 convicts less and is never wrong, because a false conviction costs someone a day
 and then costs the whole suite its credibility. **When in doubt, a property
 should decline to judge.**
 Declining costs at most a detection. Convicting a healthy app costs the spec.
 Concretely that means unknown stays `null`, a bound is preferred to an equality
 where the window can hold more than one cause, and a value carried across a
 screen change is dropped rather than compared.
 It also means reading `state.lastAction` for what it actually promises, which is
 three different things and not one:
 - `state.lastAction === null`: no action ran.
 - `applied: true`: the runner saw the dispatch succeed.
 - `applied: null`: it was dispatched and nobody knows whether it landed.
 The rule is short. **An action of unknown fate still counts toward bounds on
 what the app could have done, but it never licenses attributing an effect to
 it.** Leave it out of the bound and you convict a healthy app: folio saw a
 transaction rise of one against a window of zero submits and called it a double
 submit. Demand its effect and you convict the app of the runner's own
 uncertainty.
 `relaunched: true` says the runner had to bring the app back to the foreground
 after the action, so the two readings straddle a restart. The action still
 happened and still counts toward the bound, but nothing about state running
 continuously between the two readings survives it, and a property demanding that
 action's effect has to decline. Like `applied`, its null is "not reported", not
 "the app never restarted": web and iOS cannot read the foreground at all, so only
 an explicit `true` licenses declining.
 ## Run it, then read the witness
 **Write one property, run it, and read the witness before you write the second.**
 This is the step that gets skipped and it is the one that pays. A spec that has
 never had its readings confirmed against a real run looks exactly like a spec
 that has, right up until you find out that an extractor reads `null` on the
 platform you care about, or that a selector matches nothing, or that the value
 being compared is not the value you thought.
 ```sh
 sanderling test --spec spec.ts --bundle-id com.example.app --platform android --duration 2m
 sanderling replay
 ```
 Confirm two things before adding anything. First, that each extractor holds a
 real value at some step, by finding it in `extractor_changes` in `trace.jsonl`;
 the replay UI's hierarchy panel separately tells you whether the element your
 selector names is in the tree at all. Second, that the property actually
 compared values on some step rather than short-circuiting on its own guard. A
 green run is evidence only if you can point at a step where a property fired.
 Only then write the next property.
 Once a property is worth keeping, its logic is worth testing away from the
 device. Folio keeps its predicates in a plain module and unit-tests them in
 `pkg/spec/test/folio-*.test.ts`, run by `make test-spec-api`; the app's own
 Kotlin tests are `make test-folio`. Those files are the model for testing a
 property in isolation, including the direction people skip: a fixture where the
 effect happens legitimately, asserting that the predicate stays silent.
 ## A spec to adapt
 Complete and self-contained: a storefront whose header badge and cart panel both
 know how many things are in the cart.
 ```ts
 import { InputText, Tap, actions, always, extract, from, integers, weighted } from "@sanderling/spec";
 import { defaultActions, noUncaughtExceptions } from "@sanderling/spec/defaults";
 function wholeNumber(text: string | undefined): number | null {
  if (!text) return null;
  const parsed = Number(text.trim());
  return Number.isInteger(parsed) ? parsed : null;
 }
 // The header badge: the app's own count of what is in the cart.
 const badgeCount = extract("badgeCount", s =>
  wholeNumber(s.ax.find({ testTag: "CartBadge" })?.text));
 // The same fact by another path: the rows the cart panel renders. No panel is
 // null rather than 0, because nothing on screen is a fact we do not have, and
 // 0 would claim the cart is empty.
 const cartRowCount = extract("cartRowCount", s => {
  const panel = s.ax.find({ testTag: "CartPanel" });
  return panel ? panel.findAll({ testTag: "CartRow" }).length : null;
 });
 const checkoutEnabled = extract("checkoutEnabled", s => {
  const button = s.ax.find({ testTag: "CheckoutButton" });
  return button ? button.enabled === true : null;
 });
 // Two parts of the UI count the cart by different routes through the app's own
 // state, so they cannot disagree about how many things are in it.
 const badgeMatchesTheCart = always(() => {
  const badge = badgeCount.current;
  const rows = cartRowCount.current;
  if (badge === null || rows === null) return true;
  return badge === rows;
 });
 // Checkout is offered exactly when there is something to check out.
 const emptyCartCannotCheckOut = always(() => {
  const rows = cartRowCount.current;
  const enabled = checkoutEnabled.current;
  if (rows === null || enabled === null) return true;
  return rows > 0 || !enabled;
 });
 export const properties = {
  noUncaughtExceptions,
  badgeMatchesTheCart,
  emptyCartCannotCheckOut,
 };
 const productCards = extract("productCards", s => s.ax.findAll({ testTag: "ProductCard" }));
 const cartButton = extract("cartButton", s => s.ax.find({ testTag: "CartButton" }));
 const quantityField = extract("quantityField", s =>
  s.ax.find([{ testTag: "CartPanel" }, { testTag: "QuantityField" }]));
 const addAProduct = actions(() => {
  const cards = productCards.current;
  return cards.length === 0 ? [] : [Tap({ on: from(cards).generate() })];
 });
 const openTheCart = actions(() => {
  const button = cartButton.current;
  return button ? [Tap({ on: button })] : [];
 });
 const quantities = integers().between(1, 5);
 const changeAQuantity = actions(() => {
  const field = quantityField.current;
  return field ? [InputText({ into: field, text: String(quantities.generate()) })] : [];
 });
 // Both properties read the cart panel, so a run that never opens it judges
 // nothing. defaultActions carries the rest of the app.
 export const actionsRoot = weighted(
  [35, addAProduct],
  [25, openTheCart],
  [15, changeAQuantity],
  [25, defaultActions],
 );
 ```
 Both properties here decline whenever the panel is off screen, which is honest
 and also the thing to measure first: if `openTheCart` never wins the draw, they
 judge nothing, exactly like the replay UI's badge property did for 80 steps.
 The two real specs in the repo are the fuller references.
 `replay-ui/sanderling/spec.ts` is the cross-panel spec written the way this page
 recommends. `examples/folio/sanderling/spec.ts` with its `predicates.ts` is the
 harder kind, a spec that attributes effects to actions across screens, and every
 comment in it records a way it was once wrong. `docs/manual/spec-language.md` is
 the lookup reference for anything not covered here.
@@ -0,0 +1,149 @@
 ---
 name: sanderling-spec-review
 description: Review a sanderling spec for properties that cannot fail, cannot pass, or convict a healthy app. Use before trusting any spec, after any spec change, and whenever a run is green but you are not sure it checked anything.
 ---
 # Reviewing a sanderling spec
 A spec that is wrong does not look wrong. It looks like a passing run. Every
 failure below was found in a real spec that had been green for weeks, and each
 was caught by reading a witness rather than an exit code.
 Work through the checks in order. Report what you actually verified and what you
 could not; a review that says "I could not establish this" is worth more than one
 that implies coverage it did not check.
 ## 1. Can each property ever fail?
 For every property, find the input that makes it return false, and say what it is.
 If you cannot name one, the property is decoration.
 The common shape is a guard that short-circuits on absent elements:
 ```ts
 const badgeMatchesPanel = always(() => {
  const badges = violationBadges.current;
  const panels = panelCounts.current;
  if (badges.length === 0 || panels.length === 0) return true;  // declines
  return panels.every((c) => c === badges[0]);
 });
 ```
 That guard is correct in isolation: with nothing on screen there is nothing to
 disagree about. It is also how a property judges zero steps in an eighty step run
 and reports success. Measured on a real run, that exact property judged **0 of 80
 steps** while the job went green.
 So counting matters. For each property, count the steps where its guard passed
 and it actually compared values (**judged**) against the steps where it returned
 true without comparing anything (**declined**). A property that judged nothing
 proved nothing, whatever the exit code said.
 You can reconstruct this from a trace: fold `extractor_changes` forward per step
 to recover each extractor's value, then apply the property's own guard. Do not
 try to read it from `residuals`: `always(p)` residuals back to `{"op":"true"}`
 whether `p` compared real values or short-circuited, so the two are
 indistinguishable there.
 ## 2. Can each property ever pass?
 The mirror failure. A missing fact read as a value instead of as unknown turns a
 property into one that fires on every healthy run.
 ```ts
 // balances parse to 0 when the element is missing
 Math.abs(currBalance - prevBalance) === typedAmount   // 0 - 0 === typed, always
 ```
 Check every extractor: does it return `null` when the element is absent, or does
 it return `0`, `""`, or `[]`? An unreadable fact is unknown, never a default.
 ## 3. Would it convict an app that behaved correctly?
 This is the only unforgivable failure. A property that convicts more often and is
 sometimes wrong is strictly worse than one that convicts less and is never wrong,
 because a false conviction costs someone a day and then costs the whole suite its
 credibility.
 Test both directions for every property, always:
 - it fires on the bug it exists to catch
 - it stays silent on a run where the app behaved
 The second test is the one that matters and the one people skip. Build a fixture
 where the effect happens legitimately and assert silence.
 ## 4. Is the attribution sound?
 When a property blames an effect on an action, check it cannot blame the wrong one.
 **Identity keys must be injective.** If two distinct objects can produce the same
 key, a value can jump between unrelated series without anything noticing. Merged
 UI text is the usual culprit: an account named `Travel1` with 25 transactions and
 one named `Travel12` with 5 can both render `TRTravel125 transactions`. No
 function of that string can separate them.
 **Match whole keys, not endings or substrings.** `endsWith` attribution judges an
 older account named `Emergency Fund` when the user typed `Fund`.
 Selector matching has the same trap and it is easy to miss which keys carry it.
 `id`, `text`, `desc` and `descPrefix` resolve by their own rules, so `{id: "Sub"}`
 correctly matches nothing. Every other key, `testTag` included, falls through to a
 substring compare, so `{testTag: "Sub"}` matches `AddAccountSubmit`. That is not a
 match, it is a coincidence, and a property built on it judges whichever element
 happens to contain the fragment.
 **Drop the carrier when the screen changes.** A value carried across a route
 change is a value read from a screen that is no longer there.
 ## 5. Are the windows bounded?
 A property that compares two readings and counts actions between them is only as
 good as how often it closes the window.
 Real numbers from a real leg: a run went from step 19 to step 136 without
 returning to the screen the property read, so it saw a rise of 15 against a window
 of 37 actions. 15 is not more than 37, so nothing was reported, and the same run
 also gave 4 against 7, 6 against 13, and 1 against 1. The property was sound the
 whole time and detected nothing.
 Two fixes, and prefer the first:
 - **Close the window more often.** Read the fact somewhere the run visits often,
  not somewhere it visits rarely.
 - **Do not spend budget on actions that cannot have caused anything.** If the
  submit button is disabled when the field is empty, a tap on it committed
  nothing and must not count. That one change halved the window on a real spec.
 Prefer an **upper bound** to an equality. `|delta| > typedAmount` is sound where
 `|delta| === typedAmount` convicts a commit still in flight, a refused submit, and
 a tap that never landed.
 ## 6. Does every selector actually resolve?
 A selector that matches nothing makes every property over it vacuous, and nothing
 reports it. Verify by finding a step whose witness holds a real value for it, not
 by reading the selector and believing it.
 ## 7. Does the property know what the runner could not promise?
 `state.lastAction` distinguishes three things, and a property that collapses them
 is unsound:
 - `null` means no action ran
 - `applied: true` means the runner saw the dispatch succeed
 - `applied: null` means it was dispatched and nobody knows whether it landed
 An action of unknown fate still counts toward **bounds on what the app could have
 done**, and never licenses attributing an effect **to** it. `relaunched: true`
 says the app restarted between two readings, so a property assuming continuous
 state must decline.
 ## Reporting
 For each property give: can it fail, can it pass, does it convict a healthy app,
 how many steps it judged on a real run, and what you could not check. Name the
 step and the witness values behind any claim that a property works.
 A green run is evidence only if you can point at a step where a property actually
 fired. Read the witness, not the exit code.