Files
sanderling/docs/manual/spec-language.md
T
pj 11f72a722a follow-ups from the pr #73 review (#77)
* ci(folio): run gradle on jdk 21 for the metro plugin

the metro gradle plugin folio builds with publishes org.gradle.jvm.version 21
and java 21 class files, so every leg failed at the folio build on a 17
runtime. local builds pass on jdk 25, which is why only ci saw it.

* fix(build): clean pkg/spec/dist, not the dead spec-api path

* chore: point stale spec-api comments at pkg/spec

* fix(spec): publish src so an installed package carries the runtime entries

* fix(testrun): alias the installed spec package so one module graph loads

* fix(spec): export Direction, ScrollAction and LongPressAction from the entry

* docs(spec): cut the package readme to a description and doc links

* docs: say how the cli and spec package versions relate

* fix(verifier): report whether the last action was confirmed applied

Both hosts get applied: true when the runner saw the dispatch succeed and
applied: null when it could not, so an unconfirmed action stops arriving at
the spec as no action at all.

* fix(runner): an apply error leaves the action's fate unknown, not undone

A deadline that fires after the tap was dispatched leaves the effect
committed. Reporting nil made the spec see an effect with no action to cause
it, which is how the counting property convicts a healthy app.

* fix(release): stage the sidecar jar at the renamed embed path

* test(replay-ui): trace fixtures for the vacuity counts

one real green run, one run that rendered nothing, one that judges every property at least once.

* ci(replay-ui): count the steps each property judged

the exit code says no property returned false; it does not say any property was ever evaluated. this reads the trace and reports judged vs declined per property, and fails when the step page never rendered.

* test(replay-ui): cover the summary script from make test

* ci(replay-ui): summarise through the vacuity script

* docs(ci): explain the replay-ui judged/declined counts

* fix(verifier): encode element-valued extractors into the trace

An ax element exports with its find/findAll host functions attached, and
json.Marshal refuses the whole value over them: json: unsupported type:
func(goja.FunctionCall) goja.Value. The encoding failed, curr stayed nil,
and the goja hosts (ios, android) recorded null for every element-valued
extractor in both the per-step diff and the violation witness.

Apply the web host's sanitize rule before marshaling, so one rule encodes
an element on both hosts.

* test(verifier): pin element encoding to one rule on both hosts

* test(runner): assert an element reaches trace.jsonl and its witness

* feat(spec): give state.lastAction an applied field

Three states, not two: no action is a null lastAction, applied: true is an
action the runner confirmed, applied: null is one it dispatched and never
learned the fate of.

* fix(folio): do not attribute an effect to an unconfirmed action

submitChangesBalanceByTypedAmount and createdAccountHasNonZeroBalance both
convict by pinning an effect on the last action, so both decline unless the
runner saw it applied. The fixtures now say which fate they mean.

* test(folio): an unconfirmed submit belongs in the window

The count is an upper bound on the submits a window holds, so the tap that may
have landed counts and committedTransactionsExceedSubmits has nothing to
convict on.

* test(runner): a tap that lands under a failed apply is not a double submit

Drives the real folio counting predicates through the runner against a device
that commits the tap and then times out. The double-submit case is the control:
without it a green proves only that the property never fired.

* test(verifier): pin the three lastAction states on both hosts

The web page is handed the same applied field the goja object exposes, so a
property cannot read one thing on native and another on web.

* docs(spec-language): document the three lastAction states
2026-08-15 15:51:33 +05:30

14 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 & { applied: true | null }) | 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 and on any step that dispatched nothing
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

lastAction.applied is true when the runner saw the dispatch succeed and null when the apply call failed with the action possibly already delivered: an RPC deadline can fire after the tap reached the app, and nothing can find out afterwards. So there are three states, not two. state.lastAction === null means no action ran; applied === null means one ran whose fate is unknown. A property that attributes an effect to the action ("this submit must move the balance by the typed amount") has to decline unless applied is true, or a timeout convicts a healthy app. A property that counts what the app COULD have done should include it: an unconfirmed submit belongs in an upper bound on how many submits a window holds.

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

  • id maps to the Android resource-id (e.g., com.example:id/button). The id:<value> selector matches by suffix after :id/, so id:button matches com.example:id/button.
  • desc maps to content-desc.
  • class is the Java view class name (e.g., android.widget.TextView).
  • attrs contains raw UIAutomator attributes: package, scrollable, checkable, etc.

iOS

  • id maps to the accessibilityIdentifier set via .accessibilityIdentifier in SwiftUI/UIKit.
  • desc maps to accessibilityText, which the iOS sidecar builds by merging accessibilityLabel and the element's value (e.g., "Close, icon description"). The desc:<value> selector handles this by also matching when the description starts with <value>, .
  • class is the XCUITest element type (e.g., XCUIElementTypeButton).
  • attrs contains raw XCUITest attributes: title, placeholderValue, hasFocus, etc.

Web (Chrome)

  • id maps to the HTML id attribute.
  • desc is derived from aria-label, alt, or title.
  • class is the lowercase HTML tag name (e.g., button, input).
  • attrs contains 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)