diff --git a/skills/sanderling-property-patterns/SKILL.md b/skills/sanderling-property-patterns/SKILL.md new file mode 100644 index 0000000..183170c --- /dev/null +++ b/skills/sanderling-property-patterns/SKILL.md @@ -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. diff --git a/skills/sanderling-spec-authoring/SKILL.md b/skills/sanderling-spec-authoring/SKILL.md new file mode 100644 index 0000000..a8c34b8 --- /dev/null +++ b/skills/sanderling-spec-authoring/SKILL.md @@ -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. diff --git a/skills/sanderling-spec-review/SKILL.md b/skills/sanderling-spec-review/SKILL.md index 743d01a..4bef943 100644 --- a/skills/sanderling-spec-review/SKILL.md +++ b/skills/sanderling-spec-review/SKILL.md @@ -84,9 +84,14 @@ 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`. Substring -matching is looser still: `{id: "Sub"}` matching `AddAccountSubmit` is not a -match, it is a coincidence. +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.