* fix(ltl): give every thunk a construction identity Two distinct unnamed predicates both described as "Thunk(...)", so obligation collapse merged their residuals and could drop a live violation. Identity is assigned at construction and the fields are unexported, so a thunk cannot be built without one. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(ltl): reduce a thrown-predicate residual instead of panicking The verifier substitutes an ErrorFormula for the residual of a property whose predicate threw, and that residual is fed back in on the next step. reduce had no case for it, so the run crashed. It re-reports the same failure now. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(ltl): make a bounded always the dual of a bounded eventually G<=n(f) and not F<=n(not f) disagreed on traces where the inner was still pending when the window closed, so nnf's negation normal form was not semantics preserving. Both sides now range over the observations at which their inner can definitely resolve: the eventually keeps a pending inner as a disjunct, and the always discharges vacuously at window close. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(ltl): arm a one-shot root once per run A root that carries its own horizon is one obligation for the whole run, not one per observation. Re-instantiating a top-level eventually monitored G F<=n(p) instead of F<=n(p) and left one live obligation per step behind; a bounded always restarted its window every step and never closed. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(verifier): stop wrapping a top-level eventually in always `eventually(p).within(300, "seconds")` as a property meant "within 300 seconds of every step", which spawned an obligation per step with its own resolved deadline. A 553-step run carried 553 of them and serialized a 75 KB residual. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(ltl): serialize the resolved deadline of a bounded window Two obligations spawned at different steps from one duration-bounded formula differ only in the deadline the evaluator resolved for them, so they serialized identically and the trace erased a distinction the evaluator makes. The authored window stays in amount/unit; the resolved deadline rides alongside. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(verifier): split a witness's origin step from its detection step A deferred obligation spans two steps: the one that armed it and the one whose reduction failed. They were conflated under one index, so the extractor snapshot (which is the detecting step's state) was reported against the origin step. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(runner): record a witness's detection step in the trace Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * feat(replay-ui): show the step a violation was detected at The witness evidence is the detecting step's state, so say which step that is and let a reader jump to it. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(verifier): record the extractor state the predicates actually read On the web path extractor bodies are evaluated in V8 and injected here, but only the goja value was replaced. The trace diff and the violation witness therefore described a state no property ever saw. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * refactor(spec): one candidate producer over one target-eligibility rule Both hosts routed verbs themselves and both policies enumerated their own actions, and all four drifted. Web sent `swipes` to scrollable containers only, so swipe-to-dismiss on a list row was reachable on native and unreachable on web; the model policy folded gestures its own way and could not reach what the seeded picker drew. A host now reports facts about every element and never decides which verb may act on it: targets.ts acceptsTarget owns that for both. pick.ts builtinCandidates is the single enumeration, and the model policy reads it through __sanderlingEnumerateBuiltin__ instead of reimplementing it in Go. Gesture verbs change with it: scrolls stay vertical over scrollable containers, swipes go free-form in all four directions from any element with real bounds. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(runner): name a builtin scroll by its drag origin A builtin gesture carries endpoints and no selector, so every scroll rendered as "Scroll down " in the prompt's recent-action memory and two scrollable regions were indistinguishable. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(chrome): clear storage over cdp instead of scripting an opaque origin Launch runs while the tab is still on about:blank, whose opaque origin denies storage access, so localStorage.clear() threw SecurityError and every web run died at launch. Storage.clearDataForOrigin needs no navigation. The exception helper lands here because "Uncaught" is what hid this for so long. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(chrome): enable the swiftshader webgl fallback Headless Chrome runs with --disable-gpu, and without this flag it refuses the software WebGL backend: getContext returns null, so a canvas-rendered app paints nothing and every screenshot is identical black. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * fix(web): resolve testTag through data-testid or id Compose Multiplatform emits its testTag into the element id, which the native table already accepts via the resource-id alias. The two web selector tables were the only place that rejected it. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * test(spec): type-check the spec api as part of make test The fake runtime in api.test.ts did not return a chainable handle from extract, so the file had not type-checked since named() was added. Wiring the check into make test stops it drifting again. Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J * docs(manual): one-shot eventually and the gesture verbs Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J
13 KiB
title
| title |
|---|
| Spec language reference |
Spec language reference
Lookup reference for everything importable from @sanderling/spec. For a worked example, read the case study first.
Module structure
A spec is a TypeScript module evaluated by the Go runner each step. It exports properties and actionsRoot, plus an optional setup and generator:
import { ... } from "@sanderling/spec";
export const properties = { ... };
export const actionsRoot = weighted(...);
export const setup = login; // optional
export const generator = llm(...); // optional, see below
setup is an ActionGenerator the runner consults before actionsRoot each step. While it returns actions, they run; when it returns an empty list, the runner falls through to actionsRoot. Use it for preconditions like login and onboarding. If the app later regresses across the precondition (a logout mid-run), setup re-engages on its own.
State
Every extractor callback receives a State:
interface State {
ax: AccessibilityTree;
snapshots: Record<string, unknown>;
lastAction: Action | null;
logs: readonly LogEntry[];
exceptions: readonly ExceptionRecord[];
time: number; // ms since run start
}
| Field | Description |
|---|---|
ax |
Live UI hierarchy for this step |
snapshots |
Key-value data pushed by the app SDK (empty if SDK not integrated) |
lastAction |
The action dispatched in the previous step, or null on the first step |
logs |
Log entries collected since the previous step |
exceptions |
Uncaught exceptions or Sanderling.reportError() calls since the previous step |
time |
Milliseconds elapsed since the run started |
Selectors
Selectors are passed to ax.find(), ax.findAll(), and element-scoped .find() / .findAll().
String selectors
| Form | Matches |
|---|---|
id:<value> |
Exact match on resource-id, or element whose resource-id ends with :id/<value> (Android) |
text:<value> |
Substring match on text content |
desc:<value> |
Exact match on accessibility description; also matches when description starts with <value>, (iOS merged labels) |
descPrefix:<prefix> |
Starts-with match on accessibility description |
<attr>:<value> |
Substring match on any raw attribute by name |
Boolean attributes ("true" / "false") use exact match rather than substring.
Object selectors
Pass an object to apply multiple attribute filters with AND semantics:
s.ax.find({ accessibilityText: "LoginScreen" })
s.ax.find({ testTag: "AccountCard", clickable: true })
Every key-value pair must match. Substring and boolean rules apply per attribute.
Known attribute names are typed; you get autocomplete on testTag, text, content-desc, the boolean states (clickable, enabled, focused, checked, selected), and the cross-platform aliases (identifier, accessibilityIdentifier, accessibilityText, accessibilityLabel, label, resource-id, class, elementType, package, placeholderValue, hintText). Boolean state attributes accept a native true / false. Other attribute keys still type-check as a string-valued fallback so raw driver attributes remain reachable.
Path selectors
An array of object selectors matches a path: each segment is matched within the subtree of the previous match. Arrays work on the tree root and on element-scoped .find/.findAll.
s.ax.find([{ testTag: "LoginScreen" }, { testTag: "LoginEmail" }])
s.ax.findAll([{ testTag: "HomeScreen" }, { testTag: "AccountCard" }])
String selectors chain the same way with >, but only on the tree root (ax.find, ax.findAll):
s.ax.find("id:HomeScreen > descPrefix:account_card:")
s.ax.find("id:LedgerScreen > desc:ledger_balance_display")
Cross-platform aliases
These key aliases are resolved automatically so selectors work across platforms without changes:
| Write this | Also checks |
|---|---|
content-desc |
accessibilityText |
accessibilityText |
content-desc |
label |
accessibilityText |
accessibilityLabel |
accessibilityText |
identifier |
resource-id |
accessibilityIdentifier |
resource-id |
AccessibilityElement fields
Fields available on every element returned by find / findAll:
| Field | Type | Description |
|---|---|---|
id |
string |
resource-id (Android) or accessibility identifier (iOS) |
text |
string |
Visible text content |
desc |
string |
Accessibility description (content-desc / accessibilityText) |
class |
string |
View class (Android), element type (iOS), or HTML tag (web) |
clickable |
boolean |
Element is interactive |
enabled |
boolean |
Element is enabled |
checked |
boolean |
Checkbox or toggle state |
focused |
boolean |
Element has input focus |
selected |
boolean |
Selection state |
bounds |
{ left, top, right, bottom } |
Bounding box in device pixels |
x |
number |
Center X (derived from bounds) |
y |
number |
Center Y (derived from bounds) |
attrs |
Record<string, string> |
All raw attributes from the driver |
Platform notes
Android
idmaps to the Android resource-id (e.g.,com.example:id/button). Theid:<value>selector matches by suffix after:id/, soid:buttonmatchescom.example:id/button.descmaps tocontent-desc.classis the Java view class name (e.g.,android.widget.TextView).attrscontains raw UIAutomator attributes:package,scrollable,checkable, etc.
iOS
idmaps to theaccessibilityIdentifierset via.accessibilityIdentifierin SwiftUI/UIKit.descmaps toaccessibilityText, which the iOS sidecar builds by mergingaccessibilityLabeland the element's value (e.g.,"Close, icon description"). Thedesc:<value>selector handles this by also matching when the description starts with<value>,.classis the XCUITest element type (e.g.,XCUIElementTypeButton).attrscontains raw XCUITest attributes:title,placeholderValue,hasFocus, etc.
Web (Chrome)
idmaps to the HTMLidattribute.descis derived fromaria-label,alt, ortitle.classis the lowercase HTML tag name (e.g.,button,input).attrscontains all HTML attributes available to CDP.
KMP (Kotlin Multiplatform)
KMP apps are tested identically to native apps. An Android KMP build uses the Android driver; an iOS KMP build uses the iOS driver. There is no separate KMP driver. The accessibility tree structure reflects the target platform, so the same selector portability rules apply.
Extractors
const loggedIn = extract((s) => !!s.ax.find("id:home-tab-bar"));
const route = extract("route", (s) => ...); // named form
loggedIn.current // T - value from the current step
loggedIn.previous // T | undefined - value from the previous step, undefined on first step
Extractors are evaluated before properties and action generators. Use .previous to detect transitions between steps. Named extractors appear by name in the replay UI and trace.
LTL operators
| Function | Meaning |
|---|---|
always(f) |
f must hold at every step |
eventually(f).within(n, unit) |
f must hold at some step within n "milliseconds", "seconds", or "steps" |
now(f) |
f evaluated at the current step (for use inside always/next bodies) |
next(f) |
f evaluated at the step immediately after the current one |
A property that is an eventually at the top level is one goal for the whole run: it is armed at the first step and discharged for good the first time it holds. Written inside always(...) the same formula is armed again at every step, which asks for the window to be met from every step in the run.
Formula combinators - available on every Formula:
| Method | Meaning |
|---|---|
.implies(other) |
If this holds, other must also hold |
.and(other) |
Both must hold |
.or(other) |
At least one must hold |
.not() |
Negation |
Actions
Constructors
Tap({ on: element | string })
DoubleTap({ on: element | string })
LongPress({ on: element | string })
InputText({ into: element | string, text: string })
Swipe({ from: element | Point, to: element | Point, durationMillis?: number })
Scroll({ direction: "up" | "down" | "left" | "right", in?: element | string })
PressKey({ key: Key })
Wait({ durationMillis: number })
Key values: "back", "home", "enter", "tab", "up", "down", "left", "right".
On web, "back" maps to Backspace and "home" is not supported. All other keys work on all platforms.
Built-in generators
| Generator | Behaviour |
|---|---|
taps |
Random tap on a clickable element |
doubleTaps |
Random double tap on a clickable element |
longPresses |
Random long press on a clickable element |
typing |
Types a value from the edge-case corpus into a random editable field |
scrolls |
Scrolls a random scrollable container up or down |
swipes |
Random up, down, left, or right swipe from any visible element |
waitOnce |
Idles one step |
pressKeys |
Presses a random supported key |
scrolls anchors on a scrollable container and moves its content up or down. It never
scrolls sideways, because every scrollable container on screen gets a candidate and a
sideways pair doubles that list for little return; write Scroll({ in, direction }) when
you need one.
swipes is a free drag of 200 to 600 px from any element with real bounds, in any of the
four directions. The sideways ones are what reach swipe-to-dismiss and swipe-to-delete on
a list row.
actions(generator)
Wraps a callback that returns Action[]. The callback runs each step the generator is eligible.
const doLogin = actions(() => {
if (loggedIn.current) return [];
const submit = loginSubmit.current;
return submit ? [Tap({ on: submit })] : [];
});
weighted(...entries)
Assembles a weighted tree. Each entry is [weight, generator]. Weights are relative within the tree.
export const actionsRoot = weighted(
[50, doLogin],
[10, taps],
[2, swipes],
);
whenRoute(routeExtractor, routes, body)
Builds a generator that runs body only when the extractor's current value is in routes (a string or array of strings). Returns an empty list otherwise.
const addTxn = whenRoute(route, ["home", "ledger", "add-transaction"], () => {
...
return [Tap({ on: btn })];
});
Samplers
Every sampler has .generate(). Draws are seeded by the run's PRNG, so a run replays identically from its seed.
| Sampler | Produces |
|---|---|
from(items) |
An item from a fixed list |
integers().between(min, max) |
An integer in the range |
strings().length(min, max).alpha() |
A random string; .alpha() restricts to letters |
emails().domain("example.com") |
A random email address |
edgeCaseText() |
A value from the adversarial input corpus (empty and whitespace strings, emoji, numeric boundary values, very long strings, injection payloads) |
const names = from(["Checking", "Savings", "Travel"]);
const amounts = integers().between(1, 500);
// inside an actions() callback:
InputText({ into: nameField, text: names.generate() })
InputText({ into: amountField, text: String(amounts.generate()) })
LLM generator
By default the run's PRNG picks each action. --generator llm swaps out the picker for a vision model and nothing else: same spec, same actionsRoot, same weights, same actions. Add the export and pick a model.
export const generator = llm({
model: "gpt-5.4-nano",
instructions: "Folio is a personal-finance ledger app. The home screen lists accounts with balances; you can open an account and add transactions.",
});
Set OPENROUTER_API_KEY or OPENAI_API_KEY (OpenRouter wins if both are set). With a plain OpenAI key, drop the vendor prefix from the model id. The model needs image input and strict json_schema structured output.
Each step it gets a screenshot plus a numbered list of the concrete actions your tree yields right now, each tagged with its weight, and picks one number. That list is the seeded picker's own candidate enumeration, so both modes explore the same action space and only the choice differs. instructions are appended to the prompt: say what the app is, not how to test it; the model works that part out. Everything else is unchanged. Setup actions still run first, typing still falls back to the edge-case corpus when the model supplies no text, and the trace records the reasoning, the chosen number, and source: "llm" so the replay UI can show why each pick happened.
It is one model call per step, so keep --duration modest.
Defaults
import { defaultActions, doubleTaps } from "@sanderling/spec/defaults";
import { noUncaughtExceptions, noLogcatErrors } from "@sanderling/spec/defaults/properties";
defaultActions is a ready-made weighted tree of the built-in generators: taps and typing at weight 100, scrolls 50, swipes 25, double taps 10. Use it as a baseline pool or as one entry in your own tree.
| Property | Fails when |
|---|---|
noUncaughtExceptions |
An uncaught exception or Sanderling.reportError() call is captured |
noLogcatErrors |
Logcat emits any error-level (E) lines since the previous step (Android only; holds elsewhere) |