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.

examples/folio/sanderling/predicates.ts

@@ -1,24 +1,75 @@
-// 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.
-// A single unreadable card makes the whole total null: a partial sum looks
-// exactly like money moving, and the balance property would fire on a healthy
-// step.
-export function computeHomeTotalBalance(args: {
-  cardBalanceTexts: (string | undefined)[];
+// 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:
+//   - off Home there is nothing to read, so the last total we actually read is
+//     reported and carried on unchanged;
+//   - 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: {
+  onHome: boolean;
+  totalText: string | undefined;
   previousCarrier: number | null;
-}): number | null {
-  const { cardBalanceTexts, previousCarrier } = args;
-  if (cardBalanceTexts.length === 0) return previousCarrier;
-  let sum = 0;
-  for (const text of cardBalanceTexts) {
-    const cents = parseDollarCents(text);
-    if (cents === null) return null;
-    sum += cents;
-  }
-  return sum;
+}): HomeTotalReading {
+  const { onHome, totalText, previousCarrier } = args;
+  if (!onHome) 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 };
+}
+
+// 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 {
+  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");
+}
+
+// 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
@@ -47,8 +98,9 @@ export function parseDollarCents(text: string | undefined): number | null {
 // of "12 transactions" into the amount.
 const TRAILING_BALANCE = /[-+]?\$[\d,]+\.\d{2}\s*$/;
 
-// The transaction-count label sits between the name and the balance.
-const TRAILING_TXN_COUNT = /\d+\s*transactions?\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;
@@ -79,6 +131,68 @@ export function cardAccountName(args: {
   return head.slice(0, label.index).trim();
 }
 
+// The digit run in front of a card's "transaction(s)" label, kept as TEXT.
+//
+// A string rather than a number because web merges the card 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). Two runs
+// of different lengths do not, and 9 to 10 would read as 19 to 110, a delta of
+// 91 out of a delta of 1. Keeping the run as text is what lets the predicate
+// see the length change and drop the pair instead of convicting on it.
+//
+// Android and iOS expose AccountTxnCount as its own node, where the run is just
+// the count and the length rule costs nothing but a window per decade.
+export function cardTxnCountDigits(args: {
+  childText: string | undefined;
+  cardText: string | undefined;
+}): string | undefined {
+  const { childText, cardText } = args;
+  const source = childText ?? cardText?.replace(TRAILING_BALANCE, "");
+  return source?.match(TRAILING_TXN_COUNT)?.[1];
+}
+
+// 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, string> | null;
+  countsAfter: Record<string, string> | 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;
+    // Different run lengths are not comparable: see cardTxnCountDigits.
+    if (before.length !== after.length) continue;
+    const from = parseInt(before, 10);
+    const to = parseInt(after, 10);
+    if (!Number.isSafeInteger(from) || !Number.isSafeInteger(to)) continue;
+    if (to > from) committed += to - from;
+  }
+  return committed > submitsInWindow;
+}
+
 // Parses raw user input in the transaction amount field into integer cents.
 // 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
@@ -109,23 +223,32 @@ export function parseTypedAmount(text: string | undefined | null): number {
 // 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 | 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.

examples/folio/sanderling/spec.ts

@@ -11,13 +11,17 @@ import {
   weighted,
   whenRoute,
 } from "@sanderling/spec";
+import type { State } from "@sanderling/spec";
 import { defaultActions, doubleTaps } from "@sanderling/spec/defaults";
 import {
   cardAccountName,
   cardBalanceText,
-  computeHomeTotalBalance,
+  cardTxnCountDigits,
+  committedTransactionsExceedSubmits,
+  countSubmitsInWindow,
   parseDollarCents,
   parseTypedAmount,
+  readHomeTotalBalance,
   submitChangesBalanceByTypedAmount,
 } from "./predicates";
 
@@ -50,18 +54,70 @@ const accounts = extract<Account[]>("accounts", s =>
       cardBalanceText({ childText: card.find({ testTag: "AccountBalance" })?.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: number | null = 0;
+// 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;
+
+let lastHomeTotal: number | null = null;
 const totalBalance = extract<number | null>("totalBalance", s => {
-  const cards = s.ax.findAll([{ testTag: "HomeScreen" }, { testTag: "AccountCard" }]);
-  const cardBalanceTexts = cards.map(c =>
-    cardBalanceText({ childText: c.find({ testTag: "AccountBalance" })?.text, cardText: c.text }));
-  lastHomeTotal = computeHomeTotalBalance({ cardBalanceTexts, previousCarrier: lastHomeTotal });
-  return lastHomeTotal;
+  const reading = readHomeTotalBalance({
+    onHome: onHome(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({
+    onHome: onHome(s),
+    totalText: homeTotalText(s),
+    previousCarrier: null,
+  }).fresh;
+  const window = countSubmitsInWindow({
+    previousCount: submitsSinceHomeTotal,
+    lastAction: s.lastAction,
+    fresh,
+  });
+  submitsSinceHomeTotal = window.next;
+  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.
+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 lastAction = extract("lastAction", s => s.lastAction);
@@ -111,6 +167,7 @@ const submitMovesBalanceByTypedAmount = always(
     submitChangesBalanceByTypedAmount({
       route: route.current,
       lastAction: lastAction.current,
+      submitsInWindow: submitsInWindow.current,
       typedAmount: parseTypedAmount(txnAmountField.previous?.text),
       prevTotalBalance: totalBalance.previous ?? null,
       currTotalBalance: totalBalance.current,
@@ -118,6 +175,21 @@ const submitMovesBalanceByTypedAmount = always(
   ),
 );
 
+// 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: submitsInWindow.current,
+    }),
+  ),
+);
+
 const DEMO_EMAIL = "[email protected]";
 const DEMO_PASSWORD = "ledger123";
 
@@ -175,6 +247,7 @@ const addTxn = whenRoute(route, ["home", "ledger", "add-transaction"], () => {
 export const properties = {
   newAccountBalanceIsZero,
   submitMovesBalanceByTypedAmount,
+  submitCommitsOneTransactionPerAction,
 };
 
 export const setup = login;