pj/sanderling
1
0 Fork 0
mirror of https://github.com/priyanshujain/sanderling.git synced 2026-10-02 11:07:10 +00:00
Code Issues Packages Projects Releases Wiki Activity

Merge branch 'spec-authoring-skills' into skills-setup-and-triage

Browse Source
This commit is contained in:
pj committed 2026-08-15 22:58:07 +05:30
2 parents a51c8cb742 221c9a91b5
commit ffc857f58f
3 files changed
+781 -3
Download Patch File Download Diff File Expand all files Collapse all files

No files matched your search

skills/sanderling-property-patterns/SKILL.md
+420
View File
@@ -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.
skills/sanderling-spec-authoring/SKILL.md
+353
View File
@@ -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.
skills/sanderling-spec-review/SKILL.md
+8 -3
View File
@@ -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.