From 1ca812beed29753639bf75f8ad58f2164c610c74 Mon Sep 17 00:00:00 2001 From: PJ Date: Sat, 15 Aug 2026 22:48:27 +0530 Subject: [PATCH 1/4] docs(skills): add a property patterns catalogue skill --- skills/sanderling-property-patterns/SKILL.md | 340 +++++++++++++++++++ 1 file changed, 340 insertions(+) create mode 100644 skills/sanderling-property-patterns/SKILL.md diff --git a/skills/sanderling-property-patterns/SKILL.md b/skills/sanderling-property-patterns/SKILL.md new file mode 100644 index 0000000..32c2300 --- /dev/null +++ b/skills/sanderling-property-patterns/SKILL.md @@ -0,0 +1,340 @@ +--- +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 panels on screen at once.** 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 panel 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], + [25, defaultActions], +); +``` + +## 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. + +Both of these must hold at a step where exactly one submit is in the window: + +```ts +// sound: no more moved than that one submit could account for +Math.abs(currTotalBalance - prevTotalBalance) <= typedAmount +// tempting: it moved by exactly what I typed +Math.abs(currTotalBalance - prevTotalBalance) === typedAmount +``` + +The equality catches the same bug, a double submit moving the balance by twice +the typed amount, and it also convicts an app that behaved: a commit still in +flight when the reading was taken, a submit the app refused, a tap that never +landed. Each of those is a legitimate way for the balance not to have moved, and +under an equality each one obliges you to write a guard for it. You will miss +one. Under a bound none of them are violations in the first place, because the +app doing less than you expected is not the bug you are hunting. + +`submitChangesBalanceByTypedAmount` in `examples/folio/sanderling/predicates.ts` +is written as the equality, and you can read its guard stack as the price of +that choice: a route gate, a confirmed-dispatch gate, a window gate, a +typed-amount-is-parseable gate, two null gates and three +`Number.isSafeInteger` gates, all before the comparison. + +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 +const submitCommitsOneTransactionPerAction = always( + next(() => + !committedTransactionsExceedSubmits({ + countsBefore: homeTxnCounts.previous ?? null, + countsAfter: homeTxnCounts.current, + submitsInWindow: submitsSinceCounts.current, + }), + ), +); +``` + +Reach for this whenever the effect is countable, because it beats the amount +version on every axis. 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. In folio it is the property that does most of the detecting. + +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 actions on one side of the bound +without accumulating evidence on the other. Measured on a real 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 actions. 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 fix is to read the fact somewhere the run visits often, and to weight the +actions that return there. A bound whose budget always exceeds its evidence is a +property you can delete. + +**The window must not be spent on actions that provably could not cause the +effect.** Folio's transaction submit button is declared +`enabled = state.amount.isNotBlank()` (`AddTransactionScreen.kt`), so a tap on +it with an empty amount field commits nothing and must not consume budget. +Counting those taps was over half the window on real runs: 35 taps against a +real budget of 16, and 42 against 17. `countSubmitsInWindow` in +`predicates.ts` still counts them, which is why that number is worth checking +before you trust a green run of this property. + +Establishing that an action could not have had an effect is app knowledge, not +something the runner can tell you. Here the field's own text at the moment of +the tap settles it, and the spec already reads it as +`txnAmountField.previous?.text`. `element.enabled` is on every +`AccessibilityElement` for the general case, though whether your platform +populates it honestly is something to verify on a real tree rather than assume. + +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`, and substring +matching is looser still. + +**What the runner could not promise.** `state.lastAction` distinguishes three +things and collapsing 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 can find out whether it + landed, because an RPC deadline can fire after the tap arrived + +The rule follows the shape of the property. An action of unknown fate 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 must +decline on it, which is the same reason shape 2 prefers bounds: a property +demanding the effect of an action that may never have run convicts the app of +the runner's own uncertainty. + +Note the one event that removes an action from a window without removing its +effect: when the app leaves the foreground the runner relaunches it and drops +the pending `lastAction`, while any effect that action already committed to +persisted storage survives the restart. A carrier you hold across steps in a +module-level variable does not know a restart happened either. If a property +compares readings across an interval that a relaunch can sit inside, that is the +gap to think about. + +**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. 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. From 2394c29d10ddec079b66115211903797de88de0e Mon Sep 17 00:00:00 2001 From: PJ Date: Sat, 15 Aug 2026 22:51:16 +0530 Subject: [PATCH 2/4] docs(skills): add a spec authoring skill covers hooks, extractors, selectors, properties, actions and the order to write them in, with a complete sample spec that typechecks against the real export surface. --- skills/sanderling-spec-authoring/SKILL.md | 353 ++++++++++++++++++++++ 1 file changed, 353 insertions(+) create mode 100644 skills/sanderling-spec-authoring/SKILL.md 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. From 7068b03ffc33534946008edd2417002cf425f85c Mon Sep 17 00:00:00 2001 From: PJ Date: Sat, 15 Aug 2026 22:55:56 +0530 Subject: [PATCH 3/4] docs(skills): ground the property patterns catalogue in the merged specs --- skills/sanderling-property-patterns/SKILL.md | 226 +++++++++++++------ 1 file changed, 153 insertions(+), 73 deletions(-) diff --git a/skills/sanderling-property-patterns/SKILL.md b/skills/sanderling-property-patterns/SKILL.md index 32c2300..183170c 100644 --- a/skills/sanderling-property-patterns/SKILL.md +++ b/skills/sanderling-property-patterns/SKILL.md @@ -63,12 +63,12 @@ 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 panels on screen at once.** This +**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 panel into view its own weight. +brings the second reading into view its own weight. ```ts const switchATab = actions(() => { @@ -78,10 +78,26 @@ const switchATab = actions(() => { 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 @@ -90,28 +106,41 @@ 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. -Both of these must hold at a step where exactly one submit is in the window: +`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: no more moved than that one submit could account for -Math.abs(currTotalBalance - prevTotalBalance) <= typedAmount -// tempting: it moved by exactly what I typed +// 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 ``` -The equality catches the same bug, a double submit moving the balance by twice -the typed amount, and it also convicts an app that behaved: a commit still in -flight when the reading was taken, a submit the app refused, a tap that never -landed. Each of those is a legitimate way for the balance not to have moved, and -under an equality each one obliges you to write a guard for it. You will miss -one. Under a bound none of them are violations in the first place, because the -app doing less than you expected is not the bug you are hunting. +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. -`submitChangesBalanceByTypedAmount` in `examples/folio/sanderling/predicates.ts` -is written as the equality, and you can read its guard stack as the price of -that choice: a route gate, a confirmed-dispatch gate, a window gate, a -typed-amount-is-parseable gate, two null gates and three -`Number.isSafeInteger` gates, all before the comparison. +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 @@ -123,54 +152,80 @@ bound. The same bound, stated in counts. One action must not produce two effects. ```ts -const submitCommitsOneTransactionPerAction = always( - next(() => - !committedTransactionsExceedSubmits({ - countsBefore: homeTxnCounts.previous ?? null, - countsAfter: homeTxnCounts.current, - submitsInWindow: submitsSinceCounts.current, - }), - ), -); +!committedTransactionsExceedSubmits({ + countsBefore: homeTxnCounts.previous ?? null, + countsAfter: homeTxnCounts.current, + submitsInWindow: submitsSinceCounts.current, +}) ``` -Reach for this whenever the effect is countable, because it beats the amount -version on every axis. 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. In folio it is the property that does most of the detecting. +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 actions on one side of the bound -without accumulating evidence on the other. Measured on a real 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 actions. 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. +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 fix is to read the fact somewhere the run visits often, and to weight the -actions that return there. A bound whose budget always exceeds its evidence is a -property you can delete. +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.** Folio's transaction submit button is declared -`enabled = state.amount.isNotBlank()` (`AddTransactionScreen.kt`), so a tap on -it with an empty amount field commits nothing and must not consume budget. -Counting those taps was over half the window on real runs: 35 taps against a -real budget of 16, and 42 against 17. `countSubmitsInWindow` in -`predicates.ts` still counts them, which is why that number is worth checking -before you trust a green run of this property. +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. Here the field's own text at the moment of -the tap settles it, and the spec already reads it as -`txnAmountField.previous?.text`. `element.enabled` is on every -`AccessibilityElement` for the general case, though whether your platform -populates it honestly is something to verify on a real tree rather than assume. +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 @@ -299,31 +354,55 @@ 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`, and substring -matching is looser still. +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` distinguishes three -things and collapsing them is unsound: +**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` means no action ran +- `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 -The rule follows the shape of the property. An action of unknown fate 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 must -decline on it, which is the same reason shape 2 prefers bounds: a property -demanding the effect of an action that may never have run convicts the app of -the runner's own uncertainty. +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. -Note the one event that removes an action from a window without removing its -effect: when the app leaves the foreground the runner relaunches it and drops -the pending `lastAction`, while any effect that action already committed to -persisted storage survives the restart. A carrier you hold across steps in a -module-level variable does not know a restart happened either. If a property -compares readings across an interval that a relaunch can sit inside, that is the -gap to think about. +`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.** @@ -333,8 +412,9 @@ gap to think about. 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. A property -you have only ever seen go red is a property you have half tested. +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. From d79fb3f2d66d4a8004843a03ae78992abe6f79cc Mon Sep 17 00:00:00 2001 From: PJ Date: Sat, 15 Aug 2026 22:56:28 +0530 Subject: [PATCH 4/4] docs(skills): name the selector keys that still substring match --- skills/sanderling-spec-review/SKILL.md | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) 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.