From d31de3b247ac0f752c1e694b3414d079120b4a3e Mon Sep 17 00:00:00 2001 From: PJ Date: Fri, 14 Aug 2026 16:33:11 +0530 Subject: [PATCH] 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 | 178 +++++++++++++++++-- examples/folio/sanderling/spec.ts | 218 +++++++++++++++--------- 2 files changed, 301 insertions(+), 95 deletions(-) diff --git a/examples/folio/sanderling/predicates.ts b/examples/folio/sanderling/predicates.ts index 52cf62c..2b22c19 100644 --- a/examples/folio/sanderling/predicates.ts +++ b/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( + screens: Record, + 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 { + value: T | null; + carrier: T | null; + fresh: boolean; +} + +export function readHomeCards(args: { + route: string | null; + reading: T | null; + previousCarrier: T | null; +}): HomeCardReading { + 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 | null { + const counts: Record = {}; + 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 diff --git a/examples/folio/sanderling/spec.ts b/examples/folio/sanderling/spec.ts index a60dd6f..fed37f4 100644 --- a/examples/folio/sanderling/spec.ts +++ b/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("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(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("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", 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("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("totalBalance", s => { const reading = readHomeTotalBalance({ - onHome: onHome(s), + route: routeOf(s), totalText: homeTotalText(s), previousCarrier: lastHomeTotal, }); @@ -82,7 +116,7 @@ const totalBalance = extract("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("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 | null = null; const homeTxnCounts = extract | null>("homeTxnCounts", s => { - if (!onHome(s)) return lastHomeTxnCounts; - const counts: Record = {}; - 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, }), ), );