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.

examples/folio/sanderling/predicates.ts

@@ -1,3 +1,38 @@
+// 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;
+}
+
 // Reads the Home screen's own TOTAL BALANCE node and advances the carrier the
 // spec holds between Home visits.
 //
@@ -8,8 +43,9 @@
 //
 // Three cases, and the difference between the reported value and the carrier is
 // the whole point:
-//   - off Home there is nothing to read, so the last total we actually read is
-//     reported and carried on unchanged;
+//   - 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
@@ -24,17 +60,58 @@ export interface HomeTotalReading {
 }
 
 export function readHomeTotalBalance(args: {
-  onHome: boolean;
+  route: string | null;
   totalText: string | undefined;
   previousCarrier: number | null;
 }): HomeTotalReading {
-  const { onHome, totalText, previousCarrier } = args;
-  if (!onHome) return { value: previousCarrier, carrier: previousCarrier, fresh: false };
+  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
@@ -42,11 +119,14 @@ export function readHomeTotalBalance(args: {
 export function isTxnSubmitTap(
   lastAction: { kind?: string; on?: string | object } | null,
 ): 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("TxnSubmit");
+  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
@@ -154,6 +234,84 @@ export function cardTxnCountDigits(args: {
   return source?.match(TRAILING_TXN_COUNT)?.[1];
 }
 
+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 {
+  digits: string | 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.
+export function homeTxnCountsOf(cards: readonly CardReading[]): Record<string, string> | null {
+  const counts: Record<string, string> = {};
+  for (const card of cards) {
+    if (card.name !== "" && card.digits !== undefined) counts[card.name] = card.digits;
+  }
+  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

examples/folio/sanderling/spec.ts

@@ -11,7 +11,7 @@ import {
   weighted,
   whenRoute,
 } from "@sanderling/spec";
-import type { State } from "@sanderling/spec";
+import type { AccessibilityElement, State } from "@sanderling/spec";
 import { defaultActions, doubleTaps } from "@sanderling/spec/defaults";
 import {
   cardAccountName,
@@ -19,40 +19,76 @@ import {
   cardTxnCountDigits,
   committedTransactionsExceedSubmits,
   countSubmitsInWindow,
+  createdAccountHasNonZeroBalance,
+  homeAccountsOf,
+  homeTxnCountsOf,
   parseDollarCents,
   parseTypedAmount,
+  readHomeCards,
   readHomeTotalBalance,
+  routeOfFrame,
   submitChangesBalanceByTypedAmount,
 } from "./predicates";
+import type { Account, CardReading } from "./predicates";
 
-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;
-}
+// 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;
 
-// 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;
-});
+// 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.
+const routeOf = (s: State): Route | null =>
+  routeOfFrame<Route>(SCREENS, tag => s.ax.find({ testTag: tag }) != null);
 
-// Account cards on Home: identity comes from AccountName, balance from
-// AccountBalance. Web exposes neither child (the card is one merged node
-// there), so both readings go through predicates.ts, which falls back to
-// parsing the card's own text.
-const accounts = extract<Account[]>("accounts", s =>
-  s.ax.findAll([{ testTag: "HomeScreen" }, { testTag: "AccountCard" }]).map(card => ({
-    name: cardAccountName({ childText: card.find({ testTag: "AccountName" })?.text, cardText: card.text }),
+// 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;
+
+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 = (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 })),
-  })));
+      cardBalanceText({
+        childText: card.find({ testTag: "AccountBalance" })?.text,
+        cardText: card.text,
+      })),
+    digits: cardTxnCountDigits({
+      childText: card.find({ testTag: "AccountTxnCount" })?.text,
+      cardText: card.text,
+    }),
+  }));
 
 // 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
@@ -60,14 +96,12 @@ const accounts = extract<Account[]>("accounts", 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-read Home total so `previous` and `current` stay on the same scale.
-const homeTotalText = (s: State) =>
-  s.ax.find([{ testTag: "HomeScreen" }, { testTag: "TotalBalance" }])?.text;
-const onHome = (s: State) => s.ax.find({ testTag: "HomeScreen" }) != null;
+const homeTotalText = (s: State) => on("home", "TotalBalance")(s)?.text;
 
 let lastHomeTotal: number | null = null;
 const totalBalance = extract<number | null>("totalBalance", s => {
   const reading = readHomeTotalBalance({
-    onHome: onHome(s),
+    route: routeOf(s),
     totalText: homeTotalText(s),
     previousCarrier: lastHomeTotal,
   });
@@ -82,7 +116,7 @@ const totalBalance = extract<number | null>("totalBalance", s => {
 let submitsSinceHomeTotal = 0;
 const submitsInWindow = extract("submitsInWindow", s => {
   const fresh = readHomeTotalBalance({
-    onHome: onHome(s),
+    route: routeOf(s),
     totalText: homeTotalText(s),
     previousCarrier: null,
   }).fresh;
@@ -95,67 +129,81 @@ const submitsInWindow = extract("submitsInWindow", s => {
   return window.reported;
 });
 
-// Transactions committed per account, read off the Home cards. Carried across
-// off-Home steps exactly like totalBalance, and for the same reason: the pair
-// the property compares has to be two Home readings, not a Home reading and
-// whatever happened to be on screen. A card whose count is unreadable is left
-// out of the map rather than guessed at; the predicate treats a missing account
-// as no evidence.
+// 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, string> | null = null;
 const homeTxnCounts = extract<Record<string, string> | null>("homeTxnCounts", s => {
-  if (!onHome(s)) return lastHomeTxnCounts;
-  const counts: Record<string, string> = {};
-  for (const card of s.ax.findAll([{ testTag: "HomeScreen" }, { testTag: "AccountCard" }])) {
-    const name = cardAccountName({
-      childText: card.find({ testTag: "AccountName" })?.text,
-      cardText: card.text,
-    });
-    const digits = cardTxnCountDigits({
-      childText: card.find({ testTag: "AccountTxnCount" })?.text,
-      cardText: card.text,
-    });
-    if (name !== "" && digits !== undefined) counts[name] = digits;
-  }
-  lastHomeTxnCounts = counts;
-  return counts;
+  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 === null || 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
@@ -185,7 +233,7 @@ const submitCommitsOneTransactionPerAction = always(
     !committedTransactionsExceedSubmits({
       countsBefore: homeTxnCounts.previous ?? null,
       countsAfter: homeTxnCounts.current,
-      submitsInWindow: submitsInWindow.current,
+      submitsInWindow: submitsSinceCounts.current,
     }),
   ),
 );