ci: dispatch workflows for folio and the replay ui (#73)

* feat(runner): stop the step loop at the first violation on request

* feat(testrun): report violations as a typed error under exit-on-violation

* feat(cli): add --exit-on-violation and exit 2 when it fires

* docs(cli): document --exit-on-violation, --max-steps, and exit codes

* fix(web): enumerate and query across shadow roots in both producers

* test(chrome): compare both producers on a shadow-dom parity page

* test(browser): drive a canvas-under-shadow-root fixture end to end

* fix(web): select the focused field inside a shadow root before typing

* fix(web): report the pathname as the screen when there is no hash route

* fix(web): settle on dom quiescence instead of returning at body ready

* feat(replay-ui): add data-testid hooks the dogfood spec drives

* feat(replay-ui): add the dogfood spec sanderling runs against the replay ui

* fix(replay-ui): scope the screenshot property to the named state panel

* chore(make): add per-platform sanderling build targets

* ci: add dispatch workflows for folio and the replay ui

* docs: describe the dispatch workflows and how to read a failure

* ci(folio): give the ios leg its jdk, android sdk, just, and a clean app start

* refactor(web): use max for the settle budget

* ci: pin calibrated seeds, skip the flaky ios reinstall, bound every job

* ci: authenticate and pin the buf setup step

the anonymous release download hit the shared runner ip rate limit and
failed the job with 'socket hang up' after three retries.

* docs: record that canvas apps need a dom proxy to be text-fuzzable

* fix(ios): bound lifecycle rpcs and claim the target device

a launch the simulator rejects sent the xctest session into a recovery
chain that answered minutes late or never, and the rpc had no deadline,
so the run hung with no trace and no error. also take a per-udid flock:
a second run's reinstall lands under the first's live automation session
and wedges it.

* docs(ci): correct the ios hang wording and note the device lock

* refactor(verifier): derive the lastAction shape from one field list

both hosts must show a spec the same lastAction. one ordered list now
feeds the goja object and the json the web host installs, so they
cannot drift.

* fix(web): install lastAction in the page before extractors read it

state.lastAction was hardcoded null on web, so every property reading it
was silently vacuous: a correct property passed without ever firing.

* fix(web): carry element identity on actions and fix findAll on paths

an action's target was coordinates only, so a property matching on which
element was acted upon could never fire. ax.findAll([a,b]) also returned
nothing on web.

* fix(chrome): wait out a route transition before sampling facts

the tree stays byte-identical and quiet across a cross-fade, so both the
quiet timer and the unchanged-tree escape called it settled mid-flight
and extractors read two screens at once.

* fix: bound the pre-run app launch

launch happens before the runner starts, so --duration never covered it
and a wedged driver hung with no trace and no error.

* fix(folio): read balances from merged cards and treat unreadable as unknown

compose for web merges the whole accountcard subtree, so the balance
child never exists there and every card parsed as 0. the property then
compared 0 to 0 and fired on any submit, which is a false positive
generator. unknown is now null and null is vacuously true.

* test(folio): cover merged-card parsing and unknown balances

* ci(folio): make web an expect-the-bug leg

the web runtime can observe the double submit now, so the health gate
understates it. seed 1 finds it at step 109, 3 runs out of 3.

* docs(ci): explain why a submit tap landing on home is the bug

* fix(ios): read a StaticText's label as its text

AXValue was the only source for text, but a StaticText carries its
string in AXLabel, so nothing on screen had .text on ios: a spec reading
it saw everything on android and nothing here.

* docs(ci): correct the calibrated step ranges

* fix(folio): stop convicting on arithmetic float64 cannot hold

past 2^53 cents the gap between representable values is 128, so a real
1600-cent move reads back as something else and the equality is false
for a healthy submit as readily as a double one. also match parseCents:
a sign or an oversized amount is rejected, not read as an amount.

* test(folio): pin the safe-integer guard and its boundary

* docs: stop teaching the zero-default that caused a false alarm

* docs: write down the silent-vacuity failure modes

* feat(folio): tag the home total and the card transaction count

the total was the only untagged node on the screen, so the spec had to
sum cards and a clipped card broke the sum.

* fix(folio): read the app's own total and refuse contaminated windows

summing cards went null when one was clipped, and the null poisoned the
carrier for the rest of the run. the balance window also spanned every
transaction since the last home visit, so the property convicted on
deltas it could not attribute: the old web witness was 3.16x the typed
amount, not 2x.

* test(folio): pin the window rules and the count invariant

* fix(folio): never read a frame that shows two screens

android dumps a cross-fade with both screens in the tree. the route said
add-transaction while an unscoped find said home, so the oracle took a
half-rendered total as fresh and convicted on a tap that committed
nothing. one function now decides the route and returns null when the
frame is ambiguous.

* test(folio): cover transition frames, card readings and creation

* fix(folio): only disambiguate counts that came from merged text

the equal-length digit rule exists because web merges the card and an
account named -1 makes '12' ambiguous. a dedicated count node has
nothing to disambiguate, so applying it there threw away real evidence.

* ci(folio): pin the recalibrated seeds and drop android to a health gate

web 3 and ios 7 convict 3 runs out of 3 with an exactly 2x witness.
android convicts 2 in 5 because the same seed does not walk the same
trajectory there, so it proves the app runs instead.

* docs(ci): describe the two properties and why android cannot convict

* fix(android): wait out a route cross-fade before snapshotting

the dump could hold two screens at once, and the runner refuses to act
on such a tree, so a quarter of android steps applied no action and the
count varied per run: the same seed never walked the same trajectory.
the ios companion and the chrome driver already do this.

* ci(folio): let the android leg run far enough to see its conviction

* docs: only the repo owner merges

* ci(folio): a thrown predicate is not a conviction

exit 2 means the run recorded a violation, and a predicate that throws
is recorded as one too. so was newAccountBalanceIsZero, an unrelated
property in the same spec. the gate read the exit code and went green
with detection dead.

* ci: install idb-companion from its tap and stop interpolating inputs

idb-companion is not in homebrew-core, so the ios leg died before it
built anything. replay-ui expanded dispatch inputs into the shell.

* docs: correct the snippets and numbers that drifted from the code

* test(sidecar): pin that a slow read counts toward the stability streak

* fix(web): read the page's extractors only on steps that count

the page advances the spec's carriers when it evaluates, but the runner
applied the result only on non-transitional steps. a discarded step
moved the window forward anyway, so the next accepted pair bracketed two
transactions while counting one submit, and convicted a healthy app.
extractor errors now fail the run instead of leaving goja's values in
current against v8's in previous.

* fix(chrome): anchor the transition deadline when the dom goes quiet

it was anchored at script start, so a page that churned past the window
reached the check already expired and returned mid cross-fade. the
driver now publishes the idle timeout it needs, since the caller's 1s
could never spend the 800ms window.

* fix(web): fail on a partial extractor override

same mixed-producer hazard as the install error: some extractors hold
the page's value and the rest hold goja's, and a property comparing
across that split fires on a healthy app.

* docs: six of seven, the seventh is the stock property

* fix(folio): drop a name two cards answer to

homeTxnCountsOf keyed on the account name and let the last card win, so
two accounts the fuzzer named the same collapsed into one entry. a
reading that saw one Travel card and a later one that saw both then
subtracted two different accounts' counts, and
submitCommitsOneTransactionPerAction convicted a healthy app of
double-submitting. it is a gated property in folio-run.sh, so that reads
as "found the submit bug" over a card scrolling into view.

same rule createdAccountHasNonZeroBalance already applies: a name
nothing can attribute is no evidence. counted over every card, since an
unreadable twin spoils the identity too.

* perf(folio): read each frame once

every extractor asked routeOf, and routeOf does five ax.find calls. on
web each find walks the document and every shadow root beneath it, so
the spec cost 110 tree walks a step; homeCards was parsed four times
over. now 5 and once.

keyed on the identity of the state object because both hosts build a new
one per step and hand that one object to every getter, so it cannot
outlive its frame. holding the reference is what keeps that true rather
than likely.

* fix(web): keep an undefined reading's index through JSON

json has no undefined, so an extractor whose getter returned one had its
whole index dropped by JSON.stringify. that index then kept goja's
dump-derived value while its neighbours held the page's, and a property
comparing previous to current across the split fires on a healthy app.
folio has nine on(route, tag) extractors, so this was most extractors on
most steps.

each reading is wrapped in a {value} envelope: the drop now happens
inside the entry, and an absent value means the getter returned
undefined, which is what the goja host records for the same getter. a
json null would instead claim it returned null and x.current ===
undefined would answer differently on the two hosts.

* feat(verifier): report the registered extractor count

the web path needs it to check the page sent one reading per extractor.

* fix(runner): fail when the page reports fewer readings than extractors

the comment here already claimed a partial override was fatal. it was
not: the skipped check only catches indices outside the extractor list,
so a page reporting values for some extractors and not others left the
rest holding goja's reading of the dump with nothing said.

* test(browser): drive an undefined reading through the whole web path

four layers carry it: the page's envelope, the driver's unwrap, the
runner's count check and the verifier's decode. each has a unit test and
only a run proves they compose. goes red both ways, decoding an absent
value as null and dropping the envelope.

* fix(web): offer the aria roles a user activates

only role=button was in the tappable set, so link, checkbox, radio,
switch, tab, option, the menuitems and treeitem were invisible to the
enumeration however plain the control looked. the replay ui builds its
step rows as <li role="option">, and the spec dogfooding it had to
hand-write an action to reach them because no default verb could see a
single row.

both producers build the set from the same role list, since the parity
test compares them element by element.

* test(browser): tap a role-based control end to end

every control on the page is an <li role="option">, the shape the
replay ui gives its step rows, and the spec carries no action of its
own: the property firing is the evidence the default enumeration offered
a tap on one.

* fix(web): read aria-disabled as disabled

the enabled fact came off the disabled property, which only real form
controls have. it reads undefined on the role-based controls the
tappable set now covers, so every one of them looked enabled however
plainly it was marked otherwise, and the fuzzer would spend actions on
inert ones.

both producers answer the same two ways, and the parity fixture carries
a disabled row so the comparison covers it: reverting one side alone
names the element and the fact.

* docs(replay-ui): the enumeration reaches step rows now

the comment said role="option" is not in the tappable selector set,
which stopped being true a few commits ago. selectAStep stays, for the
reason the tab weight below it stays: one row among the page's clickable
elements is a thin chance, and both step-facing properties go vacuous on
a run that never selects one.

* test(runner): bound the last-action test by steps, not wall clock

100ms of wall clock against an assertion that two steps ran fatals under
load with "the web path never installed it", which reads as a
regression. every sibling test in the package uses a long duration and
MaxSteps.

* ci: run the kotlin tests in make test

RouteTransitionTest and the stability poll cover the android settle and
nothing in ci ran them. :sidecar:test needs no android sdk, checked by
running it with ANDROID_HOME pointed at nothing.

* fix(sidecar): measure the stability streak as observed quiet

parameterising pollUntilStable also moved the clock to the start of the
read that opened a run of identical snapshots, so a read's own duration
counted as quiet. the pre-existing caller polls a real uiautomator dump:
at 400ms a read, 750ms of required quiet became 250ms of observed quiet
and the poll settled in two reads instead of four.

the parameters stay, the semantics go back.

* test(sidecar): pin the transition cap by driving it

it asserted 1500 >= 700 + 300, two constants, which can only fail if
someone edits a constant. it now drives awaitSettledTree against a fade
that lands after 700ms and asserts it hands back the settled tree before
the cap. cut the cap to 1000 and it goes red.

* ci: pin buf-setup-action to a commit

it takes a token now, so a floating tag is a token handed to whatever
that tag moves to. note v1 there is a branch, not a tag, so the ref
lookup that resolves it is matching-refs/heads/v1.

* ci: declare least-privilege permissions

none of the three declared any, so each got the repository default.
release.yml and docs.yml already do this. all three only check out,
build, test and upload artifacts.

* ci: fail fast when a server never comes up

the readiness loops fell through silently after 30 tries, so a server
that never started surfaced as an opaque driver failure minutes later.
each now says what did not answer and on which port.

* ci(folio): a missing trace is not a verdict

with no trace the android gate ran its grep against ./trace.jsonl and
reported "never reached AddTransactionScreen, so it never got past
login", which is not what happened. the web and ios branches had the
same misdiagnosis on exit 0.

same class, one line up: the classifier's own failure was swallowed, so
with the evidence reader dead the gate printed a healthy run and exited
0.

* ci(replay-ui): skip a run directory with no trace

the summarise step is if: always(), and under github's bash -eo pipefail
an unmatched glob stays literal, the redirect fails, pipefail carries it
into the assignment and -e kills the step. so a failed fuzz run went red
twice, once for the real reason.

examples/folio/app/shared/src/commonMain/kotlin/app/folio/feature/home/HomeScreen.kt

@@ -72,7 +72,12 @@ fun HomeScreen(state: HomeUiState, onEvent: (HomeEvent) -> Unit) {
             Row(verticalAlignment = Alignment.Bottom) {
                 Column {
                     Text("TOTAL BALANCE", style = Type.label, color = t.textMuted)
-                    Text(formatCents(total), style = Type.balance, color = t.text)
+                    Text(
+                        formatCents(total),
+                        style = Type.balance,
+                        color = t.text,
+                        modifier = Modifier.testTag("TotalBalance"),
+                    )
                 }
                 Box(Modifier.weight(1f))
                 Text(
@@ -153,7 +158,12 @@ private fun AccountCard(
                 overflow = TextOverflow.Ellipsis,
                 modifier = Modifier.testTag("AccountName"),
             )
-            Text(txnLabel, style = Type.caption, color = t.textMuted)
+            Text(
+                txnLabel,
+                style = Type.caption,
+                color = t.textMuted,
+                modifier = Modifier.testTag("AccountTxnCount"),
+            )
         }
         Text(
             formatCents(balance),

examples/folio/sanderling/predicates.ts

@@ -1,62 +1,505 @@
-// Computes the Home-screen total balance from the visible AccountCard balances.
-// When no Home cards are visible (Ledger, AddTransaction, etc.) the carrier
-// value is returned so the property compares apples to apples across screen
-// transitions. The Ledger LedgerBalance is intentionally ignored because it is
-// a single-account number on a different scale than the Home multi-account sum.
-export function computeHomeTotalBalance(args: {
-  cardBalanceTexts: (string | undefined)[];
-  previousCarrier: number;
-}): number {
-  const { cardBalanceTexts, previousCarrier } = args;
-  if (cardBalanceTexts.length === 0) return previousCarrier;
-  return cardBalanceTexts.reduce((sum, text) => sum + parseDollarCents(text), 0);
+// The screen a frame shows, or null when it does not show exactly one.
+//
+// `present` answers whether a screen's marker node is in the accessibility
+// tree. Android puts two markers there constantly: its 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, occasionally three at once.
+// iOS produced none in 2558 steps and web one in 560, so this is not a rule
+// invented for a hypothetical.
+//
+// Such a frame is a navigation transition, and it is evidence about neither
+// screen. Ranking the markers and taking the first is what convicted folio's
+// spec in 11 android runs: `route` answered add-transaction off the screen
+// being torn down while a separate unscoped find answered "on Home" off the one
+// being built, so a half-rendered Home counted as a fresh balance reading and
+// reset the submit window under a tap that had not landed yet. Every reading
+// below takes the route as its only input, so there is no second answer left
+// for it to disagree with.
+//
+// The engine already draws this line: a transitional tree yields no builtin
+// targets at all (see targets() in internal/verifier), so a spec that keeps
+// picking one of the two screens is the only thing still handing out
+// coordinates from an animation.
+export function routeOfFrame<R extends string>(
+  screens: Record<R, string>,
+  present: (tag: string) => boolean,
+): R | null {
+  let shown: R | null = null;
+  for (const route of Object.keys(screens) as R[]) {
+    if (!present(screens[route])) continue;
+    if (shown !== null) return null;
+    shown = route;
+  }
+  return shown;
 }
 
-// Parses formatCents output like "$5.00", "-$1,234.56", "+$0.50" back to integer cents.
-function parseDollarCents(text: string | undefined): number {
-  if (!text) return 0;
-  const sign = text.startsWith("-") ? -1 : 1;
-  const digits = text.replace(/[^0-9]/g, "");
-  return digits ? sign * parseInt(digits, 10) : 0;
+// A reading taken once per frame, keyed on the identity of the state object the
+// reading came off.
+//
+// Both hosts build a NEW state object per step and hand that one object to
+// every extractor: goja's PushSnapshot builds it through stateObject
+// (internal/verifier/worker.go), the web runtime's evaluateExtractors through
+// buildState (pkg/spec/src/web-runtime.ts). So the object IS the frame, and a
+// value cached against it cannot outlive the frame it was read on. Holding the
+// reference is what keeps that true rather than merely likely: the cached state
+// cannot be collected, so no later step's state can be the same object.
+//
+// Worth having because these readings walk the whole tree. On web every
+// `find` is a querySelectorAll across the document and each shadow root
+// beneath it, and the spec takes a dozen of them per step off one frame.
+export function oncePerFrame<S extends object, T>(read: (frame: S) => T): (frame: S) => T {
+  let last: { frame: S; value: T } | null = null;
+  return frame => {
+    if (last === null || last.frame !== frame) last = { frame, value: read(frame) };
+    return last.value;
+  };
+}
+
+// Reads the Home screen's own TOTAL BALANCE node and advances the carrier the
+// spec holds between Home visits.
+//
+// The app computes that number over ALL accounts, so it does not care which
+// account cards happen to be laid out inside the viewport. Summing the visible
+// AccountCard balances did: a card clipped at the bottom edge exposes no
+// AccountBalance child, and a partial sum looks exactly like money moving.
+//
+// Three cases, and the difference between the reported value and the carrier is
+// the whole point:
+//   - anywhere but Home there is nothing to read, so the last total we actually
+//     read is reported and carried on unchanged. A transition frame is one of
+//     those places: its route is null, which is not "home";
+//   - on Home with an unreadable total the reading is UNKNOWN, so null is
+//     reported (the property treats null as vacuous) while the carrier keeps
+//     the last value we did read. Writing null into the carrier is what used to
+//     poison every later step: off-Home steps hand the carrier back, so one
+//     unreadable Home turned the property vacuous for the rest of the run;
+//   - on Home with a readable total, that total is both the reading and the new
+//     carrier, and `fresh` says the comparison window closes here.
+export interface HomeTotalReading {
+  value: number | null;
+  carrier: number | null;
+  fresh: boolean;
+}
+
+export function readHomeTotalBalance(args: {
+  route: string | null;
+  totalText: string | undefined;
+  previousCarrier: number | null;
+}): HomeTotalReading {
+  const { route, totalText, previousCarrier } = args;
+  if (route !== "home") return { value: previousCarrier, carrier: previousCarrier, fresh: false };
+  const total = parseDollarCents(totalText);
+  if (total === null) return { value: null, carrier: previousCarrier, fresh: false };
+  return { value: total, carrier: total, fresh: true };
+}
+
+// The same reading, taken off Home's account cards instead of its total, for
+// the readings the spec carries between Home visits (the account list and the
+// per-account transaction counts).
+//
+// The empty reading is the whole point. Android renders Home's own node a frame
+// or two before its list, so `findAll` over the cards comes back empty while the
+// screen is already claiming to be Home. That is UNKNOWN, not "no accounts":
+// writing it into the carrier is the poisoning readHomeTotalBalance was already
+// fixed for. It killed the counting invariant outright on android, where
+// counts_prev was {} at every evaluation point of all 17 runs measured.
+//
+// Callers pass null for a reading they could not take, so an empty list and an
+// empty map are one case here rather than two.
+export interface HomeCardReading<T> {
+  value: T | null;
+  carrier: T | null;
+  fresh: boolean;
+}
+
+export function readHomeCards<T>(args: {
+  route: string | null;
+  reading: T | null;
+  previousCarrier: T | null;
+}): HomeCardReading<T> {
+  const { route, reading, previousCarrier } = args;
+  if (route !== "home") return { value: previousCarrier, carrier: previousCarrier, fresh: false };
+  if (reading === null) return { value: null, carrier: previousCarrier, fresh: false };
+  return { value: reading, carrier: reading, fresh: true };
+}
+
+function isTapOn(
+  lastAction: { kind?: string; on?: string | object } | null,
+  target: string,
+): boolean {
+  if (lastAction == null) return false;
+  if (lastAction.kind !== "Tap" && lastAction.kind !== "DoubleTap") return false;
+  const on = lastAction.on;
+  const onString = typeof on === "string" ? on : on != null ? JSON.stringify(on) : "";
+  return onString.includes(target);
+}
+
+// Is this the action that commits a transaction? Nothing else in Folio reaches
+// Repository.createTransaction: AddTransactionViewModel.submit() is the only
+// caller, AddTransactionEvent.Submit is the only thing that runs it, and the
+// TxnSubmit button's onClick is the only thing that sends that event.
+export function isTxnSubmitTap(
+  lastAction: { kind?: string; on?: string | object } | null,
+): boolean {
+  return isTapOn(lastAction, "TxnSubmit");
+}
+
+// Likewise the only action that creates an account.
+export function isAddAccountSubmitTap(
+  lastAction: { kind?: string; on?: string | object } | null,
+): boolean {
+  return isTapOn(lastAction, "AddAccountSubmit");
+}
+
+// Counts the submit actions inside the window the balance property compares
+// over: from the last Home total we read to this step, inclusive of this step's
+// action.
+//
+// Counting ACTIONS rather than transactions is deliberate. A double-tap is one
+// action that commits two transactions, which is precisely the bug, so a rule
+// phrased in transactions could not tell the bug apart from two healthy
+// submits. A rule phrased in actions can: one action in the window means the
+// whole balance delta belongs to that action, and comparing it against the
+// amount typed for it is fair.
+//
+// The reset lands on `fresh`, the same event that advances the carrier, so the
+// count always describes exactly the interval the two compared totals span.
+export function countSubmitsInWindow(args: {
+  previousCount: number;
+  lastAction: { kind?: string; on?: string | object } | null;
+  fresh: boolean;
+}): { reported: number; next: number } {
+  const { previousCount, lastAction, fresh } = args;
+  const reported = previousCount + (isTxnSubmitTap(lastAction) ? 1 : 0);
+  return { reported, next: fresh ? 0 : reported };
+}
+
+// Parses formatCents output like "$5.00", "-$1,234.56", "+$0.50" back to
+// integer cents. Anything that is not a complete amount is null, not 0: a
+// balance we could not read is unknown, and reading it as zero silently moves
+// the Home total.
+export function parseDollarCents(text: string | undefined): number | null {
+  if (!text) return null;
+  const match = text.trim().match(/^([-+]?)\$?(\d{1,3}(?:,\d{3})*|\d+)\.(\d{2})$/);
+  if (!match) return null;
+  const [, sign, dollars, cents] = match;
+  if (dollars === undefined || cents === undefined) return null;
+  return (sign === "-" ? -1 : 1) * (parseInt(dollars.replace(/,/g, ""), 10) * 100 + parseInt(cents, 10));
+}
+
+// Compose Multiplatform for Web merges an AccountCard's whole subtree into one
+// accessibility node: the AccountName and AccountBalance children that Android
+// and iOS expose do not exist there, and the card's own text is
+// initials + name + "N transaction(s)" + balance run together with no
+// separator, e.g. "INInvestments12 transactions$2,589.00". The two helpers
+// below prefer the structured child and only parse the merged text when the
+// platform did not give us one.
+
+// The balance is the amount at the very END of the card text. Anchoring there
+// is the whole trick: digit-scraping the merged string would swallow the "12"
+// of "12 transactions" into the amount.
+const TRAILING_BALANCE = /[-+]?\$[\d,]+\.\d{2}\s*$/;
+
+// The transaction-count label sits between the name and the balance. The group
+// captures the digit run so the count can be read from the same match.
+const TRAILING_TXN_COUNT = /(\d+)\s*transactions?\s*$/;
+
+export function cardBalanceText(args: {
+  childText: string | undefined;
+  cardText: string | undefined;
+}): string | undefined {
+  const { childText, cardText } = args;
+  if (childText) return childText;
+  const match = cardText?.match(TRAILING_BALANCE);
+  return match ? match[0].trim() : undefined;
+}
+
+// The result is an identity key, not a display name: off web it is the
+// AccountName text, on web it is whatever the merged card text leaves in front
+// of the count label, initials and all ("T2Travel" for "Travel 2024"). Its only
+// consumer compares it for set membership. Keep it stable, not pretty: the
+// count label always starts at the first digit of the run before it, so the
+// key does not move as an account's transaction count grows.
+export function cardAccountName(args: {
+  childText: string | undefined;
+  cardText: string | undefined;
+}): string {
+  const { childText, cardText } = args;
+  if (childText) return childText;
+  if (!cardText) return "";
+  const head = cardText.replace(TRAILING_BALANCE, "");
+  const label = head.match(TRAILING_TXN_COUNT);
+  if (!label || label.index === undefined) return head.trim();
+  return head.slice(0, label.index).trim();
+}
+
+// One card's transaction count, in the strongest form its SOURCE supports. The
+// two forms are the whole reason this is not just a number:
+//
+//   - a NUMBER when the count came from the card's own AccountTxnCount node.
+//     That node's text is the count label and nothing else, so its digits are
+//     the count and subtracting two readings is exact arithmetic;
+//   - the digit RUN as TEXT when the count had to be recovered from merged card
+//     text. Web merges the AccountCard subtree into one node, and an account
+//     whose name ends in digits runs them into the count: the account named
+//     "-1" holding 2 transactions merges to "-1-12 transactions", whose maximal
+//     digit run reads 12. That prefix is fixed for a given account, so two
+//     readings whose runs are the SAME LENGTH still differ by exactly the true
+//     difference (19 to 120 is impossible; 19 to 110 is a length change), while
+//     two of different lengths do not: 9 to 10 reads as 19 to 110, a delta of
+//     91 out of a delta of 1. Keeping the run as text is what lets
+//     committedTransactionsExceedSubmits see the length change and drop the
+//     pair instead of convicting on it.
+//
+// Carrying the distinction is what keeps that length rule where it belongs.
+// There is no name in front of a dedicated node's digits for it to protect
+// against, so applied there it buys nothing and throws away real evidence every
+// time an account crosses a decade: of the three android seed-9 runs that
+// finished without convicting, two had dropped a window on this rule, one
+// reading 7 against 12 and the other 4 against 10.
+//
+// This is a fact about the reading, not about the platform. A platform that
+// starts exposing the node gets exact counts by exposing it, and one that stops
+// falls back to the text rule on the same step it stops.
+export type TxnCount = number | string;
+
+export function cardTxnCount(args: {
+  childText: string | undefined;
+  cardText: string | undefined;
+}): TxnCount | undefined {
+  const { childText, cardText } = args;
+  const source = childText ?? cardText?.replace(TRAILING_BALANCE, "");
+  const digits = source?.match(TRAILING_TXN_COUNT)?.[1];
+  if (digits === undefined) return undefined;
+  return childText === undefined ? digits : parseInt(digits, 10);
+}
+
+export interface Account {
+  // Identity key, not a display name: on web it carries the card's initials.
+  name: string;
+  // null when the card's balance could not be read at all (see cardBalanceText).
+  balance: number | null;
+}
+
+// One Home card, already parsed by the three helpers above.
+export interface CardReading extends Account {
+  count: TxnCount | undefined;
+}
+
+// The two readings Home's card list yields, each null when there is nothing in
+// it to read. Both feed readHomeCards, which is where null stops the carrier
+// from being overwritten.
+//
+// An account list is empty for two reasons a frame cannot tell apart: the app
+// has no accounts, or it has not drawn them yet. Calling both unknown costs one
+// detection, the very first account of a run, and buys back every card that
+// arrived late.
+export function homeAccountsOf(cards: readonly CardReading[]): Account[] | null {
+  if (cards.length === 0) return null;
+  return cards.map(({ name, balance }) => ({ name, balance }));
+}
+
+// A card whose name or count is unreadable is left out rather than guessed at;
+// committedTransactionsExceedSubmits treats a missing account as no evidence.
+// Every card being unreadable leaves nothing to compare, which is unknown.
+//
+// A name carried by more than one card is left out for the same reason, the
+// rule createdAccountHasNonZeroBalance applies with `matches.length === 1`:
+// nothing here can say which of them a count came from. Folio accepts the same
+// account name twice and Home lists whatever fits the viewport, so a reading
+// that saw one Travel card and a later one that saw two would otherwise
+// subtract two DIFFERENT accounts' counts and convict a healthy app of
+// double-submitting. The twin does not have to be readable to spoil the
+// identity, so duplicates are counted over every card, not just the usable
+// ones. Dropping a card can only ever cost a detection.
+export function homeTxnCountsOf(cards: readonly CardReading[]): Record<string, TxnCount> | null {
+  const cardsPerName = new Map<string, number>();
+  for (const card of cards) cardsPerName.set(card.name, (cardsPerName.get(card.name) ?? 0) + 1);
+  const counts: Record<string, TxnCount> = {};
+  for (const card of cards) {
+    if (card.name === "" || card.count === undefined) continue;
+    if (cardsPerName.get(card.name) !== 1) continue;
+    counts[card.name] = card.count;
+  }
+  return Object.keys(counts).length === 0 ? null : counts;
+}
+
+// Did the account the fuzzer just created come into existence holding money?
+//
+// "Appeared in the visible set" is not "was created". Home lists the accounts
+// that fit the viewport, so an existing account arrives in a later reading
+// whenever the list scrolls, whenever a card that was clipped becomes laid out,
+// and (before the route fix) whenever the earlier reading came off a
+// half-rendered Home mid-transition. All three read as a brand new account, and
+// the last two convicted this property on android over a Travel account holding
+// $24,112.00 and a Savings account holding $429,585.00.
+//
+// The one appearance that IS attributable to a creation is the account the
+// fuzzer asked for: the name it typed into AddAccountScreen, judged on the step
+// where that screen's submit landed on Home. Everything else that shows up is a
+// card that came into view, and this property has nothing to say about it.
+//
+// Returns true only for a violation it can attribute. Unattributable is not the
+// same as fine, and both come back false here.
+export function createdAccountHasNonZeroBalance(args: {
+  route: string | null;
+  lastAction: { kind?: string; on?: string | object } | null;
+  typedName: string | undefined;
+  before: Account[] | null;
+  after: Account[] | null;
+}): boolean {
+  const { route, lastAction, before, after } = args;
+  if (route !== "home") return false;
+  if (!isAddAccountSubmitTap(lastAction)) return false;
+  if (before === null || after === null) return false;
+  const typed = (args.typedName ?? "").trim();
+  if (typed === "") return false;
+  // Web merges the card into one node whose text opens with the avatar
+  // initials, so the identity key is "INInvestments" where android and iOS give
+  // "Investments"; endsWith covers both. Two cards answering to the same typed
+  // name (a second "Travel", or a card the tree exposed twice) leave the
+  // appearance unattributable, so nothing is judged.
+  const matches = after.filter(account => account.name.endsWith(typed));
+  const created = matches.length === 1 ? matches[0] : undefined;
+  if (created === undefined) return false;
+  if (before.some(account => account.name === created.name)) return false;
+  return created.balance !== null && created.balance !== 0;
+}
+
+// Every accepted submit commits exactly one transaction, so over any window the
+// number of transactions committed cannot exceed the number of submit actions
+// taken. A double-submit is one action committing two, which is the only way to
+// break it. Rejected submits (parseCents refuses the amount) commit nothing, so
+// the normal case sits comfortably under the bound.
+//
+// Only accounts present in BOTH readings are counted, and only upward movement.
+// A card that scrolled out of the viewport, or one whose count could not be
+// read, simply drops out of the sum. That makes the result a LOWER BOUND on the
+// transactions committed, and a lower bound that already exceeds the submit
+// count is still a real violation. Missing cards can cost a detection; they
+// cannot manufacture one.
+//
+// Transactions are never deleted (Ledger.sq has no DELETE for them), so a
+// per-account count only ever rises; the max(0, ...) is defensive, not load
+// bearing.
+export function committedTransactionsExceedSubmits(args: {
+  countsBefore: Record<string, TxnCount> | null;
+  countsAfter: Record<string, TxnCount> | null;
+  submitsInWindow: number;
+}): boolean {
+  const { countsBefore, countsAfter, submitsInWindow } = args;
+  if (countsBefore === null || countsAfter === null) return false;
+  if (!Number.isSafeInteger(submitsInWindow)) return false;
+  let committed = 0;
+  for (const name of Object.keys(countsAfter)) {
+    const before = countsBefore[name];
+    const after = countsAfter[name];
+    if (before === undefined || after === undefined) continue;
+    const rise = countRise(before, after);
+    if (rise !== null && rise > 0) committed += rise;
+  }
+  return committed > submitsInWindow;
+}
+
+// How far one account's count rose between two readings, or null when the pair
+// is not comparable. Not comparable is not zero: the account drops out of the
+// sum entirely, which can only cost a detection.
+function countRise(before: TxnCount, after: TxnCount): number | null {
+  if (typeof before === "number" && typeof after === "number") {
+    if (!Number.isSafeInteger(before) || !Number.isSafeInteger(after)) return null;
+    return after - before;
+  }
+  // Recovered from merged card text, where the run may carry an account-name
+  // prefix, so only equal-length runs subtract to the true difference: see
+  // TxnCount. A pair whose two readings came from different sources is one
+  // neither rule can vouch for, and it is dropped with them.
+  if (typeof before !== "string" || typeof after !== "string") return null;
+  if (before.length !== after.length) return null;
+  const from = parseInt(before, 10);
+  const to = parseInt(after, 10);
+  if (!Number.isSafeInteger(from) || !Number.isSafeInteger(to)) return null;
+  return to - from;
 }
 
 // Parses raw user input in the transaction amount field into integer cents.
-// Mirrors the Folio app's parseCents: whole numbers like "50" become 5000
-// cents, decimals like "5.50" become 550, more than 2 decimals or non-numeric
-// input return 0. Leading +/- signs are tolerated and treated as positive.
+// Mirrors the Folio app's parseCents (app/shared/.../util/Format.kt): whole
+// numbers like "50" become 5000 cents, decimals like "5.50" become 550, more
+// than 2 decimals or non-numeric input return 0. A sign is NOT tolerated,
+// because parseCents does not tolerate one either: it rejects "-50" outright,
+// so the app creates no transaction, and reading the field as a real amount
+// would make the property demand a balance move that never happened.
+//
+// 0 also means "an amount this reading cannot represent". parseCents returns
+// null once the whole part no longer fits a Kotlin Long, and its cents fit a
+// Long where ours are float64 doubles, exact only to Number.MAX_SAFE_INTEGER.
+// Past that the digits we compute are not the digits the app applied, so the
+// reading is unknown rather than large, and 0 routes it to the property's
+// vacuous branch.
 export function parseTypedAmount(text: string | undefined | null): number {
   if (!text) return 0;
-  let trimmed = text.trim().replace(/,/g, "");
-  if (trimmed.startsWith("+") || trimmed.startsWith("-")) trimmed = trimmed.slice(1);
+  const trimmed = text.trim().replace(/,/g, "");
   if (!/^\d+(\.\d{1,2})?$/.test(trimmed)) return 0;
   const dot = trimmed.indexOf(".");
   const whole = dot < 0 ? trimmed : trimmed.slice(0, dot);
   const frac = dot < 0 ? "" : trimmed.slice(dot + 1);
   const fracPadded = (frac + "00").slice(0, 2);
-  return parseInt(whole, 10) * 100 + parseInt(fracPadded, 10);
+  const cents = parseInt(whole, 10) * 100 + parseInt(fracPadded, 10);
+  return Number.isSafeInteger(cents) ? cents : 0;
 }
 
 // When the last action is a tap (or double-tap) on the transaction Submit
 // button, the absolute change in total balance must equal the amount the
 // user typed. A double-submit lands two transactions and shifts the balance
 // by 2x the typed amount, tripping this check. The route gate skips steps
-// whose landing screen is not Home: totalBalance is only freshly computed
-// from visible AccountCards on Home, so off-Home comparisons would read a
-// stale carrier value and false-fire.
+// whose landing screen is not Home: totalBalance is only freshly read from
+// Home's own TOTAL BALANCE node, so off-Home comparisons would read a stale
+// carrier value and false-fire.
+//
+// submitsInWindow is what keeps the comparison honest. prevTotalBalance is the
+// last total we READ, not the total as of the previous transaction, so the two
+// compared numbers can straddle any number of commits: a real run produced a
+// 13000 delta against a typed 19600 because the window held a double-submit's
+// two 19600 debits AND an unrelated 26200 credit. A delta like that is not
+// evidence about the amount typed into any one submit, so anything other than
+// exactly one submit action in the window is vacuous. Exactly one still catches
+// the bug: the double-tap is a single action.
 export function submitChangesBalanceByTypedAmount(args: {
   route: string | null;
   lastAction: { kind?: string; on?: string | object } | null;
+  submitsInWindow: number;
   typedAmount: number;
-  prevTotalBalance: number;
-  currTotalBalance: number;
+  prevTotalBalance: number | null;
+  currTotalBalance: number | null;
 }): boolean {
-  const { route, lastAction, typedAmount, prevTotalBalance, currTotalBalance } = args;
+  const { route, lastAction, submitsInWindow, typedAmount } = args;
+  const { prevTotalBalance, currTotalBalance } = args;
+
   if (route !== "home") return true;
-  if (lastAction == null) return true;
-  if (lastAction.kind !== "Tap" && lastAction.kind !== "DoubleTap") return true;
-  const on = lastAction.on;
-  const onString = typeof on === "string" ? on : on != null ? JSON.stringify(on) : "";
-  if (!onString.includes("TxnSubmit")) return true;
+  if (!isTxnSubmitTap(lastAction)) return true;
+  if (submitsInWindow !== 1) return true;
   if (typedAmount === 0) return true;
+  // An unknown total on either side is not evidence of anything. Comparing one
+  // would turn every unreadable Home into a violation.
+  if (prevTotalBalance === null || currTotalBalance === null) return true;
+  // Same rule for a total we cannot hold exactly. These are integer cents in
+  // float64, exact only up to Number.MAX_SAFE_INTEGER. The app caps a
+  // transaction at whatever fits a Kotlin Long, so a balance of ~1e18 cents is
+  // one accepted amount away, and up there the gap between representable
+  // values is 128 cents: a real 1600-cent move reads back as something else
+  // entirely. The equality below is then false for a healthy single submit
+  // exactly as readily as for a double one, and a check that cannot pass is not
+  // a check that failed.
+  //
+  // The three guarded quantities are the ones that lose precision on their own:
+  // each balance, because the number parsed out of the card text stops being
+  // the number the card shows, and the typed amount, because parseTypedAmount
+  // multiplies by 100. Their difference needs no guard of its own: IEEE
+  // subtraction of two exact integers is correctly rounded, so if the real
+  // difference equals a safe typedAmount it is itself safe and comes out exact,
+  // and if it does not, it cannot round INTO a safe typedAmount either. Adding
+  // a magnitude check there would only silence honest mismatches.
+  if (!Number.isSafeInteger(prevTotalBalance)) return true;
+  if (!Number.isSafeInteger(currTotalBalance)) return true;
+  if (!Number.isSafeInteger(typedAmount)) return true;
   return Math.abs(currTotalBalance - prevTotalBalance) === typedAmount;
 }

examples/folio/sanderling/spec.ts

@@ -11,91 +11,203 @@ import {
   weighted,
   whenRoute,
 } from "@sanderling/spec";
+import type { AccessibilityElement, State } from "@sanderling/spec";
 import { defaultActions, doubleTaps } from "@sanderling/spec/defaults";
 import {
-  computeHomeTotalBalance,
+  cardAccountName,
+  cardBalanceText,
+  cardTxnCount,
+  committedTransactionsExceedSubmits,
+  countSubmitsInWindow,
+  createdAccountHasNonZeroBalance,
+  homeAccountsOf,
+  homeTxnCountsOf,
+  oncePerFrame,
+  parseDollarCents,
   parseTypedAmount,
+  readHomeCards,
+  readHomeTotalBalance,
+  routeOfFrame,
   submitChangesBalanceByTypedAmount,
 } from "./predicates";
+import type { Account, CardReading, TxnCount } from "./predicates";
 
-interface Account {
-  name: string;
-  balance: number;
-}
+// Screen markers, and the route each one names. Detection is by testTag
+// (resource-id on Android, accessibilityIdentifier on iOS).
+const SCREENS = {
+  login: "LoginScreen",
+  "add-account": "AddAccountScreen",
+  "add-transaction": "AddTransactionScreen",
+  ledger: "LedgerScreen",
+  home: "HomeScreen",
+} as const;
+type Route = keyof typeof SCREENS;
 
-// Parses formatCents output like "$5.00", "-$1,234.56", "+$0.50" back to integer cents.
-function parseDollarCents(text: string | undefined): number {
-  if (!text) return 0;
-  const sign = text.startsWith("-") ? -1 : 1;
-  const digits = text.replace(/[^0-9]/g, "");
-  return digits ? sign * parseInt(digits, 10) : 0;
-}
+// The screen this frame shows, or null when it does not show exactly one: see
+// routeOfFrame, which owns that rule and the reason for it. Everything below
+// takes its answer from here, so no two readings can disagree about which
+// screen the app is on. Every extractor asks, so the answer is read once per
+// frame: see oncePerFrame for why that stays fresh.
+const routeOf = oncePerFrame(
+  (s: State): Route | null =>
+    routeOfFrame<Route>(SCREENS, tag => s.ax.find({ testTag: tag }) != null),
+);
 
-// Route detection via testTag (resource-id on Android, accessibilityIdentifier on iOS)
-const loggedIn = extract("loggedIn", s => s.ax.find({ testTag: "LoginScreen" }) == null);
-const route = extract<string | null>("route", s => {
-  if (s.ax.find({ testTag: "LoginScreen" })) return "login";
-  if (s.ax.find({ testTag: "AddAccountScreen" })) return "add-account";
-  if (s.ax.find({ testTag: "AddTransactionScreen" })) return "add-transaction";
-  if (s.ax.find({ testTag: "LedgerScreen" })) return "ledger";
-  if (s.ax.find({ testTag: "HomeScreen" })) return "home";
-  return null;
-});
+// An element is a reading, and a target, only when the route says we are on its
+// screen. Scoping a find to the screen's own node is not enough on a transition
+// frame: both screens are in the tree, so the one the app has already left
+// still resolves and the tap goes to whatever now occupies those pixels.
+const on =
+  (route: Route, tag: string) =>
+  (s: State): AccessibilityElement | undefined =>
+    routeOf(s) === route ? s.ax.find([{ testTag: SCREENS[route] }, { testTag: tag }]) : undefined;
 
-// Account cards on Home: identity is the AccountName text; balance comes from AccountBalance.
-const accounts = extract<Account[]>("accounts", s =>
-  s.ax.findAll([{ testTag: "HomeScreen" }, { testTag: "AccountCard" }]).map(card => ({
-    name: card.find({ testTag: "AccountName" })?.text ?? "",
-    balance: parseDollarCents(card.find({ testTag: "AccountBalance" })?.text),
+const allOn =
+  (route: Route, tag: string) =>
+  (s: State): AccessibilityElement[] =>
+    routeOf(s) === route ? s.ax.findAll([{ testTag: SCREENS[route] }, { testTag: tag }]) : [];
+
+const loggedIn = extract("loggedIn", s => routeOf(s) !== "login");
+const route = extract<Route | null>("route", routeOf);
+
+// One parse of Home's account cards. Identity comes from AccountName, balance
+// from AccountBalance, the transaction count from AccountTxnCount. Web exposes
+// none of those children (the card is one merged node there), so every reading
+// goes through predicates.ts, which falls back to parsing the card's own text.
+//
+// Everything that comes off the card list shares this parse so the readings
+// cannot disagree with each other about what was on screen.
+const homeCards = oncePerFrame((s: State): CardReading[] =>
+  allOn("home", "AccountCard")(s).map(card => ({
+    name: cardAccountName({
+      childText: card.find({ testTag: "AccountName" })?.text,
+      cardText: card.text,
+    }),
+    balance: parseDollarCents(
+      cardBalanceText({
+        childText: card.find({ testTag: "AccountBalance" })?.text,
+        cardText: card.text,
+      })),
+    count: cardTxnCount({
+      childText: card.find({ testTag: "AccountTxnCount" })?.text,
+      cardText: card.text,
+    }),
   })));
 
-// Total balance: sum of AccountCard balances visible on Home. The carrier
-// deliberately tracks only the Home multi-account total. Ledger's
+// Total balance: Home's own TOTAL BALANCE node, which the app computes over
+// every account rather than over the cards that happen to be laid out inside
+// the viewport. The carrier deliberately tracks only that Home total. Ledger's
 // LedgerBalance is a single-account number on a different scale and would
 // corrupt cross-screen comparisons if mixed in. Off-Home steps carry forward
-// the last-seen Home sum so `previous` and `current` stay on the same scale.
-let lastHomeTotal = 0;
-const totalBalance = extract("totalBalance", s => {
-  const cards = s.ax.findAll([{ testTag: "HomeScreen" }, { testTag: "AccountCard" }]);
-  const cardBalanceTexts = cards.map(c => c.find({ testTag: "AccountBalance" })?.text);
-  lastHomeTotal = computeHomeTotalBalance({ cardBalanceTexts, previousCarrier: lastHomeTotal });
-  return lastHomeTotal;
+// the last-read Home total so `previous` and `current` stay on the same scale.
+const homeTotalText = (s: State) => on("home", "TotalBalance")(s)?.text;
+
+let lastHomeTotal: number | null = null;
+const totalBalance = extract<number | null>("totalBalance", s => {
+  const reading = readHomeTotalBalance({
+    route: routeOf(s),
+    totalText: homeTotalText(s),
+    previousCarrier: lastHomeTotal,
+  });
+  lastHomeTotal = reading.carrier;
+  return reading.value;
+});
+
+// Submit actions inside the window `totalBalance.previous` and
+// `totalBalance.current` span. Recomputed rather than shared with the extractor
+// above because extractor getters may not read one another; both derive
+// freshness from the same reading, so they reset on the same step.
+let submitsSinceHomeTotal = 0;
+const submitsInWindow = extract("submitsInWindow", s => {
+  const fresh = readHomeTotalBalance({
+    route: routeOf(s),
+    totalText: homeTotalText(s),
+    previousCarrier: null,
+  }).fresh;
+  const window = countSubmitsInWindow({
+    previousCount: submitsSinceHomeTotal,
+    lastAction: s.lastAction,
+    fresh,
+  });
+  submitsSinceHomeTotal = window.next;
+  return window.reported;
+});
+
+// The account list, carried across off-Home steps exactly like totalBalance and
+// for the same reason: the pair a property compares has to be two Home
+// readings, not a Home reading and whatever happened to be on screen.
+let lastHomeAccounts: Account[] | null = null;
+const accounts = extract<Account[] | null>("accounts", s => {
+  const reading = readHomeCards({
+    route: routeOf(s),
+    reading: homeAccountsOf(homeCards(s)),
+    previousCarrier: lastHomeAccounts,
+  });
+  lastHomeAccounts = reading.carrier;
+  return reading.value;
+});
+
+// Transactions committed per account, same carrier rule.
+let lastHomeTxnCounts: Record<string, TxnCount> | null = null;
+const homeTxnCounts = extract<Record<string, TxnCount> | null>("homeTxnCounts", s => {
+  const reading = readHomeCards({
+    route: routeOf(s),
+    reading: homeTxnCountsOf(homeCards(s)),
+    previousCarrier: lastHomeTxnCounts,
+  });
+  lastHomeTxnCounts = reading.carrier;
+  return reading.value;
+});
+
+// The counting invariant gets its own window because its carrier advances on a
+// different event than the total's: a Home frame can render the footer total
+// while its card list is still empty. Sharing submitsInWindow would let the
+// count reset without the counts pair moving, and a window whose submit count
+// is smaller than the interval its two readings span is a false conviction
+// waiting to happen.
+let submitsSinceHomeCards = 0;
+const submitsSinceCounts = extract("submitsSinceCounts", s => {
+  const fresh = readHomeCards({
+    route: routeOf(s),
+    reading: homeTxnCountsOf(homeCards(s)),
+    previousCarrier: null,
+  }).fresh;
+  const window = countSubmitsInWindow({
+    previousCount: submitsSinceHomeCards,
+    lastAction: s.lastAction,
+    fresh,
+  });
+  submitsSinceHomeCards = window.next;
+  return window.reported;
 });
 
 const lastAction = extract("lastAction", s => s.lastAction);
 
-const loginEmailField = extract("loginEmailField", s =>
-  s.ax.find([{ testTag: "LoginScreen" }, { testTag: "LoginEmail" }]));
-const loginPasswordField = extract("loginPasswordField", s =>
-  s.ax.find([{ testTag: "LoginScreen" }, { testTag: "LoginPassword" }]));
-const loginSubmit = extract("loginSubmit", s =>
-  s.ax.find([{ testTag: "LoginScreen" }, { testTag: "LoginSubmit" }]));
-const addAccountButton = extract("addAccountButton", s =>
-  s.ax.find([{ testTag: "HomeScreen" }, { testTag: "AddAccountButton" }]));
-const accountNameField = extract("accountNameField", s =>
-  s.ax.find([{ testTag: "AddAccountScreen" }, { testTag: "AccountNameField" }]));
-const addAccountSubmit = extract("addAccountSubmit", s =>
-  s.ax.find([{ testTag: "AddAccountScreen" }, { testTag: "AddAccountSubmit" }]));
-const addTxnButton = extract("addTxnButton", s =>
-  s.ax.find([{ testTag: "LedgerScreen" }, { testTag: "AddTransactionButton" }]));
-const txnAmountField = extract("txnAmountField", s =>
-  s.ax.find([{ testTag: "AddTransactionScreen" }, { testTag: "TxnAmountField" }]));
-const txnSubmit = extract("txnSubmit", s =>
-  s.ax.find([{ testTag: "AddTransactionScreen" }, { testTag: "TxnSubmit" }]));
-const accountCards = extract("accountCards", s =>
-  s.ax.findAll([{ testTag: "HomeScreen" }, { testTag: "AccountCard" }]));
+const loginEmailField = extract("loginEmailField", on("login", "LoginEmail"));
+const loginPasswordField = extract("loginPasswordField", on("login", "LoginPassword"));
+const loginSubmit = extract("loginSubmit", on("login", "LoginSubmit"));
+const addAccountButton = extract("addAccountButton", on("home", "AddAccountButton"));
+const accountNameField = extract("accountNameField", on("add-account", "AccountNameField"));
+const addAccountSubmit = extract("addAccountSubmit", on("add-account", "AddAccountSubmit"));
+const addTxnButton = extract("addTxnButton", on("ledger", "AddTransactionButton"));
+const txnAmountField = extract("txnAmountField", on("add-transaction", "TxnAmountField"));
+const txnSubmit = extract("txnSubmit", on("add-transaction", "TxnSubmit"));
+const accountCards = extract("accountCards", allOn("home", "AccountCard"));
 
-// Property 1: every newly-appearing account starts with balance === 0.
-// Identity is by visible name. Guard against navigation transitions where
-// accounts vanish from the visible tree.
+// Property 1: an account starts life holding nothing. The account it judges is
+// the one the fuzzer just created, on the step that creation landed on Home:
+// a card that merely turns up in a later reading is a card that came into view,
+// not an account that came into existence. See createdAccountHasNonZeroBalance.
 const newAccountBalanceIsZero = always(
-  next(() => {
-    const prev = accounts.previous ?? [];
-    const curr = accounts.current;
-    if (prev.length === 0 || curr.length === 0) return true;
-    const prevNames = new Set(prev.map(a => a.name));
-    return curr.filter(a => !prevNames.has(a.name)).every(a => a.balance === 0);
-  })
+  next(() =>
+    !createdAccountHasNonZeroBalance({
+      route: route.current,
+      lastAction: lastAction.current,
+      typedName: accountNameField.previous?.text,
+      before: accounts.previous ?? null,
+      after: accounts.current,
+    }),
+  ),
 );
 
 // Property 2: a tap on TxnSubmit must move the total balance by exactly the
@@ -107,13 +219,29 @@ const submitMovesBalanceByTypedAmount = always(
     submitChangesBalanceByTypedAmount({
       route: route.current,
       lastAction: lastAction.current,
+      submitsInWindow: submitsInWindow.current,
       typedAmount: parseTypedAmount(txnAmountField.previous?.text),
-      prevTotalBalance: totalBalance.previous ?? 0,
+      prevTotalBalance: totalBalance.previous ?? null,
       currTotalBalance: totalBalance.current,
     }),
   ),
 );
 
+// Property 3: one submit action commits at most one transaction. Counting
+// actions against transactions needs no amounts and no float arithmetic, and it
+// stays sound however wide the window between two Home readings gets, because
+// both sides of the comparison accumulate over the same window. It is the
+// double-submit stated directly: one tap, two rows.
+const submitCommitsOneTransactionPerAction = always(
+  next(() =>
+    !committedTransactionsExceedSubmits({
+      countsBefore: homeTxnCounts.previous ?? null,
+      countsAfter: homeTxnCounts.current,
+      submitsInWindow: submitsSinceCounts.current,
+    }),
+  ),
+);
+
 const DEMO_EMAIL = "[email protected]";
 const DEMO_PASSWORD = "ledger123";
 
@@ -171,6 +299,7 @@ const addTxn = whenRoute(route, ["home", "ledger", "add-transaction"], () => {
 export const properties = {
   newAccountBalanceIsZero,
   submitMovesBalanceByTypedAmount,
+  submitCommitsOneTransactionPerAction,
 };
 
 export const setup = login;