From 4ac969bb3f0ad020e6d31c98bd14c2017d68d6b5 Mon Sep 17 00:00:00 2001
From: PJ <ipriyanshujain@gmail.com>
Date: Sat, 15 Aug 2026 20:49:38 +0530
Subject: [PATCH 1/8] fix(folio): attribute a created account by its whole key,
 not a suffix

createdAccountHasNonZeroBalance matched the created card with endsWith, so
an older account whose name ends with the typed one ("Emergency Fund" for a
typed "Fund") was judged instead whenever the new card was clipped out of
the reading. Build both keys the card can carry, the plain name and web's
initials + name, and compare them whole.
---
 examples/folio/sanderling/predicates.ts | 37 ++++++++--
 pkg/spec/test/folio-new-account.test.ts | 94 +++++++++++++++++++++++--
 2 files changed, 122 insertions(+), 9 deletions(-)

diff --git a/examples/folio/sanderling/predicates.ts b/examples/folio/sanderling/predicates.ts
index ab93c60..4d99389 100644
--- a/examples/folio/sanderling/predicates.ts
+++ b/examples/folio/sanderling/predicates.ts
@@ -259,6 +259,24 @@ export function cardAccountName(args: {
   return head.slice(0, label.index).trim();
 }
 
+// The avatar text that opens a merged card's identity key, mirroring Folio's
+// initialsOf (app/shared/.../util/Format.kt).
+//
+// A mirror because the alternative is a suffix test, and a suffix test cannot
+// say which card a name belongs to. Drift can only cost a detection: the result
+// is compared whole against a card's key, so initials that stop matching the
+// app match no card rather than the wrong one.
+export function initialsOf(name: string): string {
+  // Java's \s, which is what Kotlin's Regex("\\s+") compiles to. JS's \s also
+  // matches the unicode spaces, and would split names the app keeps whole.
+  const parts = name.trim().split(/[ \t\n\v\f\r]+/).filter(part => part !== "");
+  const first = parts[0];
+  const last = parts[parts.length - 1];
+  if (first === undefined || last === undefined) return "?";
+  if (parts.length === 1) return first.slice(0, 2).toUpperCase();
+  return (first.slice(0, 1) + last.slice(0, 1)).toUpperCase();
+}
+
 // 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:
 //
@@ -386,10 +404,21 @@ export function createdAccountHasNonZeroBalance(args: {
   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));
+  // "Investments". Both forms are built from the name that was typed and
+  // compared whole. A suffix test covered both too, and it also let any OTHER
+  // account ending in those letters answer for the created one: type "Fund"
+  // next to an existing "Emergency Fund", have the new card clipped out of the
+  // reading the way Home clips any card, and the old account is convicted for
+  // money it has held all along. It cost detections as well, because a typed
+  // name that two cards end with is judged as unattributable rather than as the
+  // one card that carries it.
+  //
+  // Two cards answering to one key stay unattributable: Accounts.name is UNIQUE
+  // and Repository.createAccount rejects a name already taken, so that pair is
+  // a card the tree exposed twice, or two names the merged key cannot tell
+  // apart.
+  const mergedKey = initialsOf(typed) + typed;
+  const matches = after.filter(account => account.name === typed || account.name === mergedKey);
   const created = matches.length === 1 ? matches[0] : undefined;
   if (created === undefined) return false;
   if (before.some(account => account.name === created.name)) return false;
diff --git a/pkg/spec/test/folio-new-account.test.ts b/pkg/spec/test/folio-new-account.test.ts
index d5ee3ab..8c9950c 100644
--- a/pkg/spec/test/folio-new-account.test.ts
+++ b/pkg/spec/test/folio-new-account.test.ts
@@ -1,7 +1,10 @@
 import assert from "node:assert/strict";
 import { test } from "node:test";
 
-import { createdAccountHasNonZeroBalance } from "../../../examples/folio/sanderling/predicates.ts";
+import {
+  createdAccountHasNonZeroBalance,
+  initialsOf,
+} from "../../../examples/folio/sanderling/predicates.ts";
 
 const created = {
   kind: "Tap",
@@ -209,9 +212,90 @@ test("the merged web key still matches the name that was typed", () => {
   );
 });
 
-// Two cards answering to one typed name leave the appearance unattributable:
-// the fuzzer creates duplicates from a five-name list, and the tree has been
-// seen exposing the same card twice on a transition frame.
+// The avatar the merged web key opens with, hand-computed off Format.kt rather
+// than off the mirror, because a mirror checked against itself checks nothing.
+// A single word gives its first two characters, several give the first letter
+// of the first and of the last, and an empty name gives "?".
+test("the initials a merged key opens with are the app's", () => {
+  const named: [string, string][] = [
+    ["CH", "Checking"],
+    ["SA", "Savings"],
+    ["TR", "Travel"],
+    ["EF", "Emergency Fund"],
+    ["IN", "Investments"],
+    ["FU", "Fund"],
+    ["T2", "Travel 2024"],
+    ["A", "a"],
+    ["X9", "x9"],
+    ["-1", "-1"],
+    ["?", ""],
+    ["?", "   "],
+  ];
+  for (const [initials, name] of named) {
+    assert.equal(initialsOf(name), initials, `initials for ${JSON.stringify(name)}`);
+  }
+});
+
+// The attribution used to be a suffix test, and a suffix test hands the verdict
+// to whichever OTHER account happens to end with the typed name. Home lists
+// what fits the viewport, so the card that was just created is clipped out of
+// the reading exactly as easily as any other, and the older account left in it
+// is then judged for money it has held all along.
+test("an older account whose name ends with the typed one is not the created one", () => {
+  assert.equal(
+    createdAccountHasNonZeroBalance({
+      route: "home",
+      lastAction: created,
+      typedName: "Fund",
+      before: [account("Checking", 0)],
+      after: [account("Checking", 0), account("Emergency Fund", 461012300)],
+    }),
+    false,
+  );
+});
+
+test("the merged web key is matched whole too, not by its ending", () => {
+  assert.equal(
+    createdAccountHasNonZeroBalance({
+      route: "home",
+      lastAction: created,
+      typedName: "Fund",
+      before: [account("CHChecking", 0)],
+      after: [account("CHChecking", 0), account("EFEmergency Fund", 461012300)],
+    }),
+    false,
+  );
+});
+
+// The card that was actually asked for is still judged, standing next to the
+// account that merely ends with its name.
+test("the created card is judged beside an account whose name ends with it", () => {
+  assert.equal(
+    createdAccountHasNonZeroBalance({
+      route: "home",
+      lastAction: created,
+      typedName: "Fund",
+      before: [account("Emergency Fund", 461012300)],
+      after: [account("Emergency Fund", 461012300), account("Fund", 5000)],
+    }),
+    true,
+  );
+  assert.equal(
+    createdAccountHasNonZeroBalance({
+      route: "home",
+      lastAction: created,
+      typedName: "Fund",
+      before: [account("EFEmergency Fund", 461012300)],
+      after: [account("EFEmergency Fund", 461012300), account("FUFund", 5000)],
+    }),
+    true,
+  );
+});
+
+// Two cards answering to one typed name leave the appearance unattributable.
+// Accounts.name is UNIQUE and Repository.createAccount rejects a name already
+// taken, so the pair is one card the tree exposed twice on a transition frame,
+// or two names the merged web key cannot tell apart.
 test("two cards matching the typed name are not attributable to the creation", () => {
   assert.equal(
     createdAccountHasNonZeroBalance({
@@ -219,7 +303,7 @@ test("two cards matching the typed name are not attributable to the creation", (
       lastAction: created,
       typedName: "Travel",
       before: [account("Checking", 0)],
-      after: [account("Checking", 0), account("Travel", 5000), account("MyTravel", 900)],
+      after: [account("Checking", 0), account("Travel", 5000), account("Travel", 900)],
     }),
     false,
   );

From 2d789d7d17a40c7080841be7e7b1a3f9e0e8bc68 Mon Sep 17 00:00:00 2001
From: PJ <ipriyanshujain@gmail.com>
Date: Sat, 15 Aug 2026 21:03:07 +0530
Subject: [PATCH 2/8] feat(folio): judge a submit against the account's own
 balance

The counting invariant can only close its window on Home, and the iOS run
in #78 went 117 steps between two Home readings: 37 submits against a rise
of 15 transactions is no evidence about the double tap sitting inside it.
The ledger and the add-transaction screen both show the account's own
balance, and an accepted submit pops back to the ledger, so a window
bounded by those readings holds one action.

The bound is an upper one: a balance that has not moved is a commit still
in flight, a rejected submit or a tap that never landed, and none of those
is a violation. Moving by more than the one submit in the window typed is.
---
 examples/folio/sanderling/predicates.ts   | 102 +++++
 pkg/spec/test/folio-ledger-window.test.ts | 441 ++++++++++++++++++++++
 2 files changed, 543 insertions(+)
 create mode 100644 pkg/spec/test/folio-ledger-window.test.ts

diff --git a/examples/folio/sanderling/predicates.ts b/examples/folio/sanderling/predicates.ts
index 4d99389..82fbfc9 100644
--- a/examples/folio/sanderling/predicates.ts
+++ b/examples/folio/sanderling/predicates.ts
@@ -123,6 +123,51 @@ export function readHomeCards<T>(args: {
   return { value: reading, carrier: reading, fresh: true };
 }
 
+// The balance of the ONE account the ledger and the add-transaction screen are
+// showing, and the window it closes.
+//
+// It exists because the Home readings above close their window only when the
+// walk goes back to Home, and a walk inside the transaction flow does not: a
+// submit pops back to the ledger it came from, so the fuzzer can add
+// transactions all day without Home ever being redrawn. The iOS run in #78 went
+// 117 steps between two Home readings and accumulated 37 submits against a rise
+// of 15 transactions, which is no evidence about any single action. Both
+// screens here carry the account's own balance (LedgerBalance,
+// TxnCurrentBalance), so the window between two readings holds one action.
+//
+// WHICH account is never asked, because inside a run of these two routes it
+// cannot change. Route.Ledger is pushed only by tapping a card on Home,
+// Route.AddTransaction only by the ledger's own button for its own account, and
+// an accepted submit pops back to that same ledger. Reaching another account's
+// ledger means passing through Home, and one action reads one frame, so a frame
+// that is neither of these two routes always sits in between. Dropping the
+// carrier on every such frame, transition frames included, is what makes the
+// two compared numbers two readings of one account.
+export interface AccountBalanceReading {
+  value: number | null;
+  carrier: number | null;
+  fresh: boolean;
+}
+
+function showsOneAccount(route: string | null): boolean {
+  return route === "ledger" || route === "add-transaction";
+}
+
+export function readAccountBalance(args: {
+  route: string | null;
+  balanceText: string | undefined;
+  previousCarrier: number | null;
+}): AccountBalanceReading {
+  const { route, balanceText, previousCarrier } = args;
+  if (!showsOneAccount(route)) return { value: null, carrier: null, fresh: false };
+  const balance = parseAccountBalance(balanceText);
+  // Unreadable is unknown, not a new value: the balance node scrolls off the
+  // viewport like anything else. The account still cannot have changed, so the
+  // last number we read is carried across and the window stays open.
+  if (balance === null) return { value: previousCarrier, carrier: previousCarrier, fresh: false };
+  return { value: balance, carrier: balance, fresh: true };
+}
+
 // state.lastAction as the two hosts build it (internal/verifier/marshal.go
 // lastActionFields), read defensively: every field is what a Go struct decided
 // to emit, not something this file can trust a compile-time shape for.
@@ -240,6 +285,15 @@ export function cardBalanceText(args: {
   return match ? match[0].trim() : undefined;
 }
 
+// One account's own balance, off the node whose whole text it is: bare on the
+// ledger ("$196.00"), labelled in the add-transaction header
+// ("Balance: $196.00"). Anchored at the end for the same reason as above, so
+// the label cannot be read as part of the amount.
+export function parseAccountBalance(text: string | undefined): number | null {
+  const match = text?.match(TRAILING_BALANCE);
+  return match ? parseDollarCents(match[0].trim()) : null;
+}
+
 // 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
@@ -460,6 +514,54 @@ export function committedTransactionsExceedSubmits(args: {
   return committed > submitsInWindow;
 }
 
+// The same rule as above, measured in money over the account's own window: one
+// submit action can commit one transaction, so the account's balance cannot
+// move by more than the amount that submit typed.
+//
+// An UPPER BOUND, not the equality submitChangesBalanceByTypedAmount uses, and
+// that is what makes a one-action window safe. A balance that has not moved is
+// a commit still in flight (createTransaction runs in a coroutine), a submit
+// the app rejected, or a tap that never landed, and none of those is evidence
+// of anything; an equality would convict all three. Moving by MORE than one
+// submit's worth is not something a correct app can do: only createTransaction
+// moves this number, only a TxnSubmit tap reaches it, and the window holds
+// exactly one such tap. A double tap is one action committing two transactions,
+// so it moves the balance by twice what was typed and lands here.
+//
+// A submit the runner could not confirm needs no case of its own for the same
+// reason: if it never landed the balance did not move, which is under the
+// bound. countSubmitsInWindow counts it either way, so it cannot smuggle a
+// second commit into a window that looks like one.
+//
+// typedAmount is the amount the app parsed for THIS submit (parseTypedAmount
+// mirrors parseCents), so every rejected amount and every amount too large to
+// hold exactly arrives here as 0 and is vacuous.
+//
+// The float guards are the ones submitChangesBalanceByTypedAmount explains:
+// each balance and the typed amount lose precision on their own past
+// Number.MAX_SAFE_INTEGER. Their difference needs none, because a difference
+// that is really within a safe typedAmount is itself safe and comes out exact.
+export function committedAmountExceedsOneSubmit(args: {
+  route: string | null;
+  lastAction: ObservedAction | null;
+  submitsInWindow: number;
+  typedAmount: number;
+  prevAccountBalance: number | null;
+  currAccountBalance: number | null;
+}): boolean {
+  const { route, lastAction, submitsInWindow, typedAmount } = args;
+  const { prevAccountBalance, currAccountBalance } = args;
+  if (!showsOneAccount(route)) return false;
+  if (!isTxnSubmitTap(lastAction)) return false;
+  if (submitsInWindow !== 1) return false;
+  if (typedAmount <= 0) return false;
+  if (prevAccountBalance === null || currAccountBalance === null) return false;
+  if (!Number.isSafeInteger(prevAccountBalance)) return false;
+  if (!Number.isSafeInteger(currAccountBalance)) return false;
+  if (!Number.isSafeInteger(typedAmount)) return false;
+  return Math.abs(currAccountBalance - prevAccountBalance) > typedAmount;
+}
+
 // 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.
diff --git a/pkg/spec/test/folio-ledger-window.test.ts b/pkg/spec/test/folio-ledger-window.test.ts
new file mode 100644
index 0000000..49bf8e5
--- /dev/null
+++ b/pkg/spec/test/folio-ledger-window.test.ts
@@ -0,0 +1,441 @@
+import assert from "node:assert/strict";
+import { test } from "node:test";
+
+import {
+  committedAmountExceedsOneSubmit,
+  committedTransactionsExceedSubmits,
+  countSubmitsInWindow,
+  homeTxnCountsOf,
+  parseAccountBalance,
+  parseTypedAmount,
+  readAccountBalance,
+  readHomeCards,
+} from "../../../examples/folio/sanderling/predicates.ts";
+import type {
+  ObservedAction,
+  TxnCount,
+} from "../../../examples/folio/sanderling/predicates.ts";
+
+// The per-account balance the ledger and the add-transaction screen both show.
+// Its window closes on every frame of the transaction flow, where the Home
+// total's closes only when the walk goes back to Home: the iOS run in #78 went
+// 117 steps between two Home readings and accumulated 37 submits against a rise
+// of 15, so the double tap at step 32 sat in a window far too wide to judge.
+
+const submit: ObservedAction = {
+  kind: "Tap",
+  on: "testTag:AddTransactionScreen > testTag:TxnSubmit",
+  applied: true,
+};
+const doubleSubmit: ObservedAction = { ...submit, kind: "DoubleTap" };
+const openLedger: ObservedAction = {
+  kind: "Tap",
+  on: "testTag:HomeScreen > testTag:AccountCard",
+  applied: true,
+};
+const openAddTxn: ObservedAction = {
+  kind: "Tap",
+  on: "testTag:LedgerScreen > testTag:AddTransactionButton",
+  applied: true,
+};
+const typeAmount: ObservedAction = {
+  kind: "InputText",
+  on: "testTag:AddTransactionScreen > testTag:TxnAmountField",
+  applied: true,
+};
+const goBack: ObservedAction = { kind: "Tap", on: "testTag:BackButton", applied: true };
+
+test("the ledger writes the balance bare and the add-transaction header labels it", () => {
+  assert.equal(parseAccountBalance("$196.00"), 19600);
+  assert.equal(parseAccountBalance("Balance: $196.00"), 19600);
+  assert.equal(parseAccountBalance("-$1,234.56"), -123456);
+  assert.equal(parseAccountBalance("Balance: -$1,234.56"), -123456);
+  assert.equal(parseAccountBalance("$0.00"), 0);
+});
+
+test("a balance that is not a complete amount is unknown, not zero", () => {
+  assert.equal(parseAccountBalance(undefined), null);
+  assert.equal(parseAccountBalance(""), null);
+  assert.equal(parseAccountBalance("Balance:"), null);
+  assert.equal(parseAccountBalance("$1,23.00"), null);
+});
+
+// Which account these numbers belong to is never asked, because inside a run of
+// these two routes it cannot change: Route.Ledger is pushed only by tapping a
+// card on Home, Route.AddTransaction only by the ledger's own button for its
+// own account, and an accepted submit pops back to that same ledger. Reaching
+// another account means passing through Home, so every frame that is not one of
+// the two routes drops the carrier.
+test("a frame off the account's own screens drops the carrier", () => {
+  for (const route of ["home", "login", "add-account", null]) {
+    assert.deepEqual(
+      readAccountBalance({ route, balanceText: "$196.00", previousCarrier: 10000 }),
+      { value: null, carrier: null, fresh: false },
+      `route ${route} kept a carrier that may belong to another account`,
+    );
+  }
+});
+
+test("a readable balance on either of the two screens closes the window", () => {
+  assert.deepEqual(
+    readAccountBalance({ route: "ledger", balanceText: "$196.00", previousCarrier: 10000 }),
+    { value: 19600, carrier: 19600, fresh: true },
+  );
+  assert.deepEqual(
+    readAccountBalance({
+      route: "add-transaction",
+      balanceText: "Balance: $196.00",
+      previousCarrier: 10000,
+    }),
+    { value: 19600, carrier: 19600, fresh: true },
+  );
+});
+
+// The balance node scrolled out of the viewport is unknown, not a new value.
+// The account still cannot have changed, so the carrier survives and the window
+// stays open across the frame.
+test("an unreadable balance keeps the carrier and does not close the window", () => {
+  assert.deepEqual(
+    readAccountBalance({ route: "ledger", balanceText: undefined, previousCarrier: 10000 }),
+    { value: 10000, carrier: 10000, fresh: false },
+  );
+});
+
+test("a double submit moves the account balance by twice what was typed", () => {
+  assert.equal(
+    committedAmountExceedsOneSubmit({
+      route: "ledger",
+      lastAction: doubleSubmit,
+      submitsInWindow: 1,
+      typedAmount: 19600,
+      prevAccountBalance: 10000,
+      currAccountBalance: 49200,
+    }),
+    true,
+  );
+});
+
+test("a double-submitted debit is caught by the same bound", () => {
+  assert.equal(
+    committedAmountExceedsOneSubmit({
+      route: "ledger",
+      lastAction: doubleSubmit,
+      submitsInWindow: 1,
+      typedAmount: 19600,
+      prevAccountBalance: 10000,
+      currAccountBalance: -29200,
+    }),
+    true,
+  );
+});
+
+test("one submit moving the balance by exactly the typed amount is the app working", () => {
+  for (const after of [29600, -9600]) {
+    assert.equal(
+      committedAmountExceedsOneSubmit({
+        route: "ledger",
+        lastAction: submit,
+        submitsInWindow: 1,
+        typedAmount: 19600,
+        prevAccountBalance: 10000,
+        currAccountBalance: after,
+      }),
+      false,
+    );
+  }
+});
+
+// A balance that has not moved is a commit still in flight (createTransaction
+// runs in a coroutine), a submit the app rejected, or a tap that never landed.
+// None of those is evidence, and an equality would convict all three.
+test("a balance that has not moved yet is not evidence", () => {
+  assert.equal(
+    committedAmountExceedsOneSubmit({
+      route: "ledger",
+      lastAction: submit,
+      submitsInWindow: 1,
+      typedAmount: 19600,
+      prevAccountBalance: 10000,
+      currAccountBalance: 10000,
+    }),
+    false,
+  );
+});
+
+test("a window holding anything other than one submit is not attributable", () => {
+  for (const submitsInWindow of [0, 2, 37]) {
+    assert.equal(
+      committedAmountExceedsOneSubmit({
+        route: "ledger",
+        lastAction: submit,
+        submitsInWindow,
+        typedAmount: 19600,
+        prevAccountBalance: 10000,
+        currAccountBalance: 49200,
+      }),
+      false,
+    );
+  }
+});
+
+test("an amount this reading cannot represent is vacuous, not a violation", () => {
+  assert.equal(
+    committedAmountExceedsOneSubmit({
+      route: "ledger",
+      lastAction: submit,
+      submitsInWindow: 1,
+      typedAmount: parseTypedAmount("not an amount"),
+      prevAccountBalance: 10000,
+      currAccountBalance: 49200,
+    }),
+    false,
+  );
+  assert.equal(
+    committedAmountExceedsOneSubmit({
+      route: "ledger",
+      lastAction: submit,
+      submitsInWindow: 1,
+      typedAmount: Number.MAX_SAFE_INTEGER + 2,
+      prevAccountBalance: 10000,
+      currAccountBalance: 49200,
+    }),
+    false,
+  );
+});
+
+test("a balance too large to hold exactly is not compared", () => {
+  assert.equal(
+    committedAmountExceedsOneSubmit({
+      route: "ledger",
+      lastAction: submit,
+      submitsInWindow: 1,
+      typedAmount: 19600,
+      prevAccountBalance: Number.MAX_SAFE_INTEGER + 2,
+      currAccountBalance: 0,
+    }),
+    false,
+  );
+  assert.equal(
+    committedAmountExceedsOneSubmit({
+      route: "ledger",
+      lastAction: submit,
+      submitsInWindow: 1,
+      typedAmount: 19600,
+      prevAccountBalance: 0,
+      currAccountBalance: Number.MAX_SAFE_INTEGER + 2,
+    }),
+    false,
+  );
+});
+
+test("an unknown balance on either side is not evidence", () => {
+  assert.equal(
+    committedAmountExceedsOneSubmit({
+      route: "ledger",
+      lastAction: submit,
+      submitsInWindow: 1,
+      typedAmount: 19600,
+      prevAccountBalance: null,
+      currAccountBalance: 49200,
+    }),
+    false,
+  );
+  assert.equal(
+    committedAmountExceedsOneSubmit({
+      route: "ledger",
+      lastAction: submit,
+      submitsInWindow: 1,
+      typedAmount: 19600,
+      prevAccountBalance: 10000,
+      currAccountBalance: null,
+    }),
+    false,
+  );
+});
+
+test("a step whose action was not a submit attributes nothing", () => {
+  for (const lastAction of [openLedger, openAddTxn, typeAmount, goBack, null]) {
+    assert.equal(
+      committedAmountExceedsOneSubmit({
+        route: "ledger",
+        lastAction,
+        submitsInWindow: 1,
+        typedAmount: 19600,
+        prevAccountBalance: 10000,
+        currAccountBalance: 49200,
+      }),
+      false,
+    );
+  }
+});
+
+test("Home shows every account's money, so it is not this comparison's scale", () => {
+  for (const route of ["home", "login", "add-account", null]) {
+    assert.equal(
+      committedAmountExceedsOneSubmit({
+        route,
+        lastAction: doubleSubmit,
+        submitsInWindow: 1,
+        typedAmount: 19600,
+        prevAccountBalance: 10000,
+        currAccountBalance: 49200,
+      }),
+      false,
+    );
+  }
+});
+
+// A step of the walk: the frame it landed on, the balance node that frame
+// carried, what was in the amount field the step before, and the action that
+// got there. Driven through the same carrier and window the spec holds.
+interface Frame {
+  route: string | null;
+  balanceText?: string;
+  typed?: string;
+  lastAction: ObservedAction | null;
+}
+
+function walk(frames: readonly Frame[]) {
+  let carrier: number | null = null;
+  let submits = 0;
+  const verdicts: { violated: boolean; balance: number | null; submits: number }[] = [];
+  let previous: number | null = null;
+  let typedBefore = "";
+  for (const frame of frames) {
+    const reading = readAccountBalance({
+      route: frame.route,
+      balanceText: frame.balanceText,
+      previousCarrier: carrier,
+    });
+    carrier = reading.carrier;
+    const window = countSubmitsInWindow({
+      previousCount: submits,
+      lastAction: frame.lastAction,
+      fresh: reading.fresh,
+    });
+    submits = window.next;
+    verdicts.push({
+      violated: committedAmountExceedsOneSubmit({
+        route: frame.route,
+        lastAction: frame.lastAction,
+        submitsInWindow: window.reported,
+        typedAmount: parseTypedAmount(typedBefore),
+        prevAccountBalance: previous,
+        currAccountBalance: reading.value,
+      }),
+      balance: reading.value,
+      submits: window.reported,
+    });
+    previous = reading.value;
+    typedBefore = frame.typed ?? "";
+  }
+  return verdicts;
+}
+
+// The trajectory of #78: open an account, open the transaction form, type,
+// double tap. Not one frame of it is Home, so the Home readings the counting
+// invariant compares never advance and it has nothing to say about any of it.
+// This is what a 117-step stretch of that run looked like, and it is why the
+// double tap at step 32 went unconvicted.
+test("the Home window cannot judge a walk that never goes Home", () => {
+  const cards = [{ name: "Checking", balance: 10000, count: 3 as TxnCount }];
+  let carrier: Record<string, TxnCount> | null = homeTxnCountsOf(cards);
+  let submits = 0;
+  for (const lastAction of [openLedger, openAddTxn, typeAmount, doubleSubmit]) {
+    const reading = readHomeCards({ route: "ledger", reading: null, previousCarrier: carrier });
+    const previous = carrier;
+    carrier = reading.carrier;
+    const window = countSubmitsInWindow({ previousCount: submits, lastAction, fresh: reading.fresh });
+    submits = window.next;
+    assert.equal(
+      committedTransactionsExceedSubmits({
+        countsBefore: previous,
+        countsAfter: reading.value,
+        submitsInWindow: window.reported,
+      }),
+      false,
+    );
+  }
+});
+
+// The same trajectory, judged where the app actually is. The frame the double
+// tap lands on is the account's own ledger, so the window that closes there
+// holds exactly the one action.
+test("the double tap is convicted on the frame it lands on", () => {
+  const verdicts = walk([
+    { route: "ledger", balanceText: "$100.00", lastAction: openLedger },
+    { route: "add-transaction", balanceText: "Balance: $100.00", lastAction: openAddTxn },
+    { route: "add-transaction", balanceText: "Balance: $100.00", typed: "196", lastAction: typeAmount },
+    { route: "ledger", balanceText: "$492.00", lastAction: doubleSubmit },
+  ]);
+  assert.deepEqual(
+    verdicts.map(v => v.violated),
+    [false, false, false, true],
+  );
+  assert.equal(verdicts[3]?.submits, 1);
+});
+
+test("the same walk with one transaction committed is silent throughout", () => {
+  const verdicts = walk([
+    { route: "ledger", balanceText: "$100.00", lastAction: openLedger },
+    { route: "add-transaction", balanceText: "Balance: $100.00", lastAction: openAddTxn },
+    { route: "add-transaction", balanceText: "Balance: $100.00", typed: "196", lastAction: typeAmount },
+    { route: "ledger", balanceText: "$296.00", lastAction: submit },
+    { route: "add-transaction", balanceText: "Balance: $296.00", lastAction: openAddTxn },
+    { route: "add-transaction", balanceText: "Balance: $296.00", typed: "50", lastAction: typeAmount },
+    { route: "ledger", balanceText: "$346.00", lastAction: submit },
+  ]);
+  assert.deepEqual(
+    verdicts.map(v => v.violated),
+    [false, false, false, false, false, false, false],
+  );
+});
+
+// The reading a healthy app must survive: transactions arriving between two
+// readings that the window can no longer attribute to one action. The balance
+// node is off the viewport for a stretch, so the two numbers the property would
+// compare straddle two commits, and the balance moves by 296.00 against a typed
+// 50.00. Two submits in the window is not one, so there is nothing to judge.
+test("transactions arriving between two readings do not convict a healthy app", () => {
+  const verdicts = walk([
+    { route: "ledger", balanceText: "$100.00", lastAction: openLedger },
+    { route: "add-transaction", lastAction: openAddTxn },
+    { route: "add-transaction", typed: "196", lastAction: typeAmount },
+    { route: "ledger", lastAction: submit },
+    { route: "add-transaction", lastAction: openAddTxn },
+    { route: "add-transaction", typed: "100", lastAction: typeAmount },
+    { route: "ledger", balanceText: "$396.00", lastAction: submit },
+  ]);
+  assert.deepEqual(
+    verdicts.map(v => v.violated),
+    [false, false, false, false, false, false, false],
+  );
+  assert.equal(verdicts[6]?.submits, 2);
+  assert.equal(verdicts[6]?.balance, 39600);
+});
+
+// Attribution across accounts, which is the whole reason the carrier is dropped
+// rather than carried. A $500.00 account is left behind for an empty one whose
+// screens have not drawn their balance yet, and the submit into the new account
+// lands with exactly one submit in the window: every gate this property has is
+// open, and only the dropped carrier keeps it quiet. Carrying $500.00 across
+// that frame reads as 30400 committed against 19600 typed, on an app that did
+// nothing wrong.
+test("a ledger opened for another account never inherits the old balance", () => {
+  for (const between of ["home", null]) {
+    const verdicts = walk([
+      { route: "ledger", balanceText: "$500.00", lastAction: openAddTxn },
+      { route: between, lastAction: goBack },
+      { route: "ledger", lastAction: openLedger },
+      { route: "add-transaction", typed: "196", lastAction: openAddTxn },
+      { route: "ledger", balanceText: "$196.00", lastAction: submit },
+    ]);
+    assert.deepEqual(
+      verdicts.map(v => v.violated),
+      [false, false, false, false, false],
+      `an account switch through ${between} was compared across accounts`,
+    );
+    assert.equal(verdicts[4]?.submits, 1);
+    assert.equal(verdicts[4]?.balance, 19600);
+  }
+});

From 0e096c00b374f58ee8d1aa695567629cadd10fdb Mon Sep 17 00:00:00 2001
From: PJ <ipriyanshujain@gmail.com>
Date: Sat, 15 Aug 2026 21:04:39 +0530
Subject: [PATCH 3/8] feat(folio): close the submit window on the account's own
 screens

submitCommitsOneTransactionPerAction now states its rule over two windows:
the Home counts it already compared, and the account balance the ledger and
the add-transaction screen redraw on nearly every frame of the transaction
flow. Same rule, and the second window is usually one action wide.
---
 examples/folio/sanderling/spec.ts | 68 ++++++++++++++++++++++++++++---
 1 file changed, 62 insertions(+), 6 deletions(-)

diff --git a/examples/folio/sanderling/spec.ts b/examples/folio/sanderling/spec.ts
index a403d51..4555255 100644
--- a/examples/folio/sanderling/spec.ts
+++ b/examples/folio/sanderling/spec.ts
@@ -17,6 +17,7 @@ import {
   cardAccountName,
   cardBalanceText,
   cardTxnCount,
+  committedAmountExceedsOneSubmit,
   committedTransactionsExceedSubmits,
   countSubmitsInWindow,
   createdAccountHasNonZeroBalance,
@@ -25,6 +26,7 @@ import {
   oncePerFrame,
   parseDollarCents,
   parseTypedAmount,
+  readAccountBalance,
   readHomeCards,
   readHomeTotalBalance,
   routeOfFrame,
@@ -181,6 +183,44 @@ const submitsSinceCounts = extract("submitsSinceCounts", s => {
   return window.reported;
 });
 
+// The account's own balance, off whichever of its two screens is up. The routes
+// are exclusive, so at most one of these resolves and the reading is always one
+// account's number. Its carrier is dropped on every other route, which is what
+// keeps two readings from spanning two accounts: see readAccountBalance.
+const accountBalanceText = (s: State) =>
+  on("ledger", "LedgerBalance")(s)?.text ?? on("add-transaction", "TxnCurrentBalance")(s)?.text;
+
+let lastAccountBalance: number | null = null;
+const accountBalance = extract<number | null>("accountBalance", s => {
+  const reading = readAccountBalance({
+    route: routeOf(s),
+    balanceText: accountBalanceText(s),
+    previousCarrier: lastAccountBalance,
+  });
+  lastAccountBalance = reading.carrier;
+  return reading.value;
+});
+
+// A third window, for the same reason the counting invariant has its own: it
+// closes on this reading's freshness, which is a different event again. The
+// transaction flow redraws this balance on nearly every frame, so this window
+// is the narrow one, usually a single action wide.
+let submitsSinceAccountBalance = 0;
+const submitsSinceBalance = extract("submitsSinceAccountBalance", s => {
+  const fresh = readAccountBalance({
+    route: routeOf(s),
+    balanceText: accountBalanceText(s),
+    previousCarrier: null,
+  }).fresh;
+  const window = countSubmitsInWindow({
+    previousCount: submitsSinceAccountBalance,
+    lastAction: s.lastAction,
+    fresh,
+  });
+  submitsSinceAccountBalance = window.next;
+  return window.reported;
+});
+
 const lastAction = extract("lastAction", s => s.lastAction);
 
 const loginEmailField = extract("loginEmailField", on("login", "LoginEmail"));
@@ -232,13 +272,29 @@ const submitMovesBalanceByTypedAmount = always(
 // 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.
+//
+// One rule, two windows. The counting form can only compare two Home readings,
+// and a walk that stays inside the transaction flow gives it a window hundreds
+// of steps and dozens of submits wide, which is sound and says nothing. The
+// second form says the same thing in money about the one account whose screen
+// the walk is on, and that window is usually a single action, so it can still
+// tell one commit from two: see committedAmountExceedsOneSubmit.
 const submitCommitsOneTransactionPerAction = always(
-  next(() =>
-    !committedTransactionsExceedSubmits({
-      countsBefore: homeTxnCounts.previous ?? null,
-      countsAfter: homeTxnCounts.current,
-      submitsInWindow: submitsSinceCounts.current,
-    }),
+  next(
+    () =>
+      !committedTransactionsExceedSubmits({
+        countsBefore: homeTxnCounts.previous ?? null,
+        countsAfter: homeTxnCounts.current,
+        submitsInWindow: submitsSinceCounts.current,
+      }) &&
+      !committedAmountExceedsOneSubmit({
+        route: route.current,
+        lastAction: lastAction.current,
+        submitsInWindow: submitsSinceBalance.current,
+        typedAmount: parseTypedAmount(txnAmountField.previous?.text),
+        prevAccountBalance: accountBalance.previous ?? null,
+        currAccountBalance: accountBalance.current,
+      }),
   ),
 );
 

From 9770537aa6e9680724eb3b36300ed5f551a8db9d Mon Sep 17 00:00:00 2001
From: PJ <ipriyanshujain@gmail.com>
Date: Sat, 15 Aug 2026 21:11:30 +0530
Subject: [PATCH 4/8] fix(folio): decline the two demanding properties across a
 relaunch

The runner now keeps lastAction and marks it relaunched: true where it used
to report nothing at all, so the two properties that demand an effect judge
a step whose process may have died before the write landed.
submitChangesBalanceByTypedAmount and createdAccountHasNonZeroBalance both
decline there. The counting bound does not: a relaunch cannot manufacture a
transaction, and the submit is counted, so declining would throw away the
detection the runner fix restored.
---
 examples/folio/sanderling/predicates.ts       | 22 +++++++++++
 pkg/spec/test/folio-new-account.test.ts       | 34 +++++++++++++++++
 .../folio-submit-balance-predicate.test.ts    | 38 +++++++++++++++++++
 3 files changed, 94 insertions(+)

diff --git a/examples/folio/sanderling/predicates.ts b/examples/folio/sanderling/predicates.ts
index 82fbfc9..fe94ee5 100644
--- a/examples/folio/sanderling/predicates.ts
+++ b/examples/folio/sanderling/predicates.ts
@@ -181,6 +181,7 @@ export interface ObservedAction {
   kind?: string;
   on?: string | object;
   applied?: true | null;
+  relaunched?: true | null;
 }
 
 function isTapOn(lastAction: ObservedAction | null, target: string): boolean {
@@ -216,6 +217,19 @@ export function confirmedApplied(lastAction: ObservedAction | null): boolean {
   return lastAction != null && lastAction.applied === true;
 }
 
+// The runner reports this when its foreground guard had to relaunch the app
+// after the action. The action still happened, so it still counts toward how
+// many submits a window could hold; what nobody can promise across it is that
+// the process survived long enough to commit, or that Home is showing the same
+// slice of the account list it was.
+//
+// `true | null` for the same reason `applied` is: web and iOS cannot read the
+// foreground at all, so "no relaunch reported" is not "the app never
+// restarted", and only an explicit true licenses declining.
+export function acrossRelaunch(lastAction: ObservedAction | null): boolean {
+  return lastAction != null && lastAction.relaunched === true;
+}
+
 // 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.
@@ -453,6 +467,10 @@ export function createdAccountHasNonZeroBalance(args: {
   // card to: the card that turned up may be an older account of the same name
   // scrolling into view.
   if (!confirmedApplied(lastAction)) return false;
+  // A relaunch draws Home from the top again, so the card that carries the
+  // typed name may be an older account of that name laid out where the new one
+  // used to be, and the create may not have reached sqlite at all.
+  if (acrossRelaunch(lastAction)) return false;
   if (before === null || after === null) return false;
   const typed = (args.typedName ?? "").trim();
   if (typed === "") return false;
@@ -641,6 +659,10 @@ export function submitChangesBalanceByTypedAmount(args: {
   // runner could not confirm may have committed nothing, and a balance that
   // did not move is then exactly what a healthy app looks like.
   if (!confirmedApplied(lastAction)) return true;
+  // The runner restarted the app after this tap, so the process may have died
+  // between the commit and the sqlite write. A balance that did not move is
+  // then a healthy app, exactly as it is for a submit that may not have landed.
+  if (acrossRelaunch(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
diff --git a/pkg/spec/test/folio-new-account.test.ts b/pkg/spec/test/folio-new-account.test.ts
index 8c9950c..98845f8 100644
--- a/pkg/spec/test/folio-new-account.test.ts
+++ b/pkg/spec/test/folio-new-account.test.ts
@@ -322,6 +322,40 @@ test("a card that was already there is not a card that was just created", () =>
   );
 });
 
+// The runner's foreground guard restarted the app after the create. A fresh
+// launch draws Home from the top, so the visible set is whatever the new layout
+// fits rather than what was there a step ago, and "appeared in the reading" is
+// even less like "was created" than usual. The process may also have died
+// before the write landed, which makes the card that carries the typed name an
+// older account of that name coming into view.
+test("a create the runner relaunched across attributes nothing", () => {
+  assert.equal(
+    createdAccountHasNonZeroBalance({
+      route: "home",
+      lastAction: { ...created, relaunched: true },
+      typedName: "Travel",
+      before: [account("Checking", 0)],
+      after: [account("Checking", 0), account("Travel", 5000)],
+    }),
+    false,
+  );
+});
+
+test("no relaunch reported still judges the account that was created", () => {
+  for (const relaunched of [null, undefined]) {
+    assert.equal(
+      createdAccountHasNonZeroBalance({
+        route: "home",
+        lastAction: { ...created, relaunched },
+        typedName: "Travel",
+        before: [account("Checking", 0)],
+        after: [account("Checking", 0), account("Travel", 5000)],
+      }),
+      true,
+    );
+  }
+});
+
 // The apply call failed with the gesture possibly already delivered, so nobody
 // knows whether that account was created. The card carrying the typed name may
 // be an older one that scrolled into view, and attributing it to a creation
diff --git a/pkg/spec/test/folio-submit-balance-predicate.test.ts b/pkg/spec/test/folio-submit-balance-predicate.test.ts
index 672fb5b..280f18a 100644
--- a/pkg/spec/test/folio-submit-balance-predicate.test.ts
+++ b/pkg/spec/test/folio-submit-balance-predicate.test.ts
@@ -520,3 +520,41 @@ test("a submit the runner could not confirm demands no balance move", () => {
     true,
   );
 });
+
+// relaunched: true is the runner saying its foreground guard restarted the app
+// after this action. The tap landed, so the window still counts it, but nobody
+// can promise the process lived long enough for the write to reach sqlite. A
+// balance still sitting where it was is exactly what a healthy app looks like
+// across a relaunch, and demanding the typed amount of movement convicts it for
+// the runner's own restart.
+test("a submit the runner relaunched across demands no balance move", () => {
+  assert.equal(
+    submitChangesBalanceByTypedAmount({
+      route: "home",
+      lastAction: { kind: "Tap", on: submitOn, applied: true, relaunched: true },
+      submitsInWindow: 1,
+      typedAmount: 500,
+      prevTotalBalance: 1000,
+      currTotalBalance: 1000,
+    }),
+    true,
+  );
+});
+
+// The guard must not become a way of switching the property off. No relaunch
+// reported is the ordinary case, and web and iOS cannot report one at all.
+test("no relaunch reported still convicts a double submit", () => {
+  for (const relaunched of [null, undefined]) {
+    assert.equal(
+      submitChangesBalanceByTypedAmount({
+        route: "home",
+        lastAction: { kind: "DoubleTap", on: submitOn, applied: true, relaunched },
+        submitsInWindow: 1,
+        typedAmount: 500,
+        prevTotalBalance: 1000,
+        currTotalBalance: 2000,
+      }),
+      false,
+    );
+  }
+});

From 95e0ab8afa8de3949c2baa0c0953a20c26b460a3 Mon Sep 17 00:00:00 2001
From: PJ <ipriyanshujain@gmail.com>
Date: Sat, 15 Aug 2026 21:11:47 +0530
Subject: [PATCH 5/8] docs(folio): say why the merged card key cannot be made
 injective

Folio rejects a duplicate account name, so the twin the drop rule guards
against is two names the web key cannot tell apart, not two accounts
sharing a name. State what closing the rest would cost and what the tree
would have to carry to close it properly.
---
 examples/folio/sanderling/predicates.ts | 27 ++++++++++++++++++-------
 1 file changed, 20 insertions(+), 7 deletions(-)

diff --git a/examples/folio/sanderling/predicates.ts b/examples/folio/sanderling/predicates.ts
index fe94ee5..db36849 100644
--- a/examples/folio/sanderling/predicates.ts
+++ b/examples/folio/sanderling/predicates.ts
@@ -417,13 +417,26 @@ export function homeAccountsOf(cards: readonly CardReading[]): Account[] | null
 //
 // 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.
+// nothing here can say which of them a count came from. Two accounts never
+// share a NAME (Accounts.name is UNIQUE and Repository.createAccount rejects
+// one already taken, NOCASE), but they can share a KEY, because web's key is
+// the card text in front of the digit run, which is the name with any trailing
+// digits shaved off it: "Travel1" holding 25 transactions and "Travel12"
+// holding 6 both key to "TRTravel" and both read a three-digit run, so
+// subtracting one from the other subtracts two unrelated counting series. 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.
+//
+// What this cannot see is a twin that never shares a reading with its pair, and
+// Home lists only what fits the viewport. Nothing computed from the card text
+// can: the two cards' text is identical character for character ("TRTravel1"
+// followed by "25 transactions" and "TRTravel12" followed by "6 transactions"
+// are one string), so no key derived from it separates them. Refusing every run
+// that could hide a name's own digits would, at the price of the evidence web
+// convicts on today, whose measured witness is a count of 12 rising to 14.
+// Separating them needs something the tree does not carry: the account's id on
+// the card, or a separator in front of the count.
 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);

From ff7dde4be80fa97cab5e1ee34252ca5f1bc1d1c4 Mon Sep 17 00:00:00 2001
From: PJ <ipriyanshujain@gmail.com>
Date: Sat, 15 Aug 2026 21:12:28 +0530
Subject: [PATCH 6/8] test(folio): pin that two accounts can render the same
 card text

The proof behind the comment: "Travel1" holding 25 transactions and
"Travel12" holding 5 merge to the same string, so no identity key read off
a web card can tell them apart.
---
 pkg/spec/test/folio-account-card-parse.test.ts | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/pkg/spec/test/folio-account-card-parse.test.ts b/pkg/spec/test/folio-account-card-parse.test.ts
index 6b046b3..18230f3 100644
--- a/pkg/spec/test/folio-account-card-parse.test.ts
+++ b/pkg/spec/test/folio-account-card-parse.test.ts
@@ -65,6 +65,18 @@ test("name ending in digits does not leak into the balance", () => {
   assert.equal(balanceOf(card("20", "2024", 3, "-$1,234.56")), -123456);
 });
 
+// The limit of a key read off merged text, and the reason homeTxnCountsOf
+// guards the ambiguity rather than resolving it: two DIFFERENT accounts render
+// the same card, character for character. Names are unique (Accounts.name is
+// UNIQUE, checked NOCASE) but the count runs straight into a name that ends in
+// digits, so nothing computed from this string can say which account it is.
+test("two accounts can render one card, so no key off it can be injective", () => {
+  const travel1 = card("TR", "Travel1", 25, "$120.00");
+  const travel12 = card("TR", "Travel12", 5, "$120.00");
+  assert.equal(travel1, travel12);
+  assert.equal(cardAccountName({ childText: undefined, cardText: travel1 }), "TRTravel");
+});
+
 // The account key only has to be stable and per-account. newAccountBalanceIsZero
 // reads it as a set member: a key that drifted as an account's transaction
 // count grew would make an existing account look brand new, and the property

From 6b276253e858e541bef86bd79d496e4300b8aff5 Mon Sep 17 00:00:00 2001
From: PJ <ipriyanshujain@gmail.com>
Date: Sat, 15 Aug 2026 21:24:53 +0530
Subject: [PATCH 7/8] fix(folio): stop spending the submit budget on taps the
 app refused

The window is an upper bound on the transactions an interval could hold, and
a bound inflated by taps that commit nothing is a bound the app can never
exceed: #78 read a rise of 15 transactions against 37 submits. TxnSubmit is
clickable(enabled = amount.isNotBlank()) and parseCents refuses anything its
regex misses, so a tap whose landing frame shows a refused amount cannot have
committed. Over four recorded android runs that is 19, 11, 25 and 25 of 35,
26, 42 and 42 submit taps.

A relaunch is excepted: a fresh process draws an empty field whatever was
submitted.
---
 examples/folio/sanderling/predicates.ts   | 40 +++++++++-
 pkg/spec/test/folio-submit-window.test.ts | 90 +++++++++++++++++++++++
 2 files changed, 129 insertions(+), 1 deletion(-)

diff --git a/examples/folio/sanderling/predicates.ts b/examples/folio/sanderling/predicates.ts
index db36849..27bee6d 100644
--- a/examples/folio/sanderling/predicates.ts
+++ b/examples/folio/sanderling/predicates.ts
@@ -249,16 +249,54 @@ export function acrossRelaunch(lastAction: ObservedAction | null): boolean {
 // well have landed. Leaving it out is what convicted a healthy app:
 // committedTransactionsExceedSubmits saw a transaction rise of one against a
 // window of zero and called it a double submit.
+//
+// A submit the app must have refused does not count, for the mirror reason: it
+// cannot have committed anything, so the bound it would raise is slack the app
+// can hide a real double submit behind. See submitCouldCommit for what "must
+// have refused" is allowed to mean.
 export function countSubmitsInWindow(args: {
   previousCount: number;
   lastAction: ObservedAction | null;
+  amountText?: string;
   fresh: boolean;
 }): { reported: number; next: number } {
   const { previousCount, lastAction, fresh } = args;
-  const reported = previousCount + (isTxnSubmitTap(lastAction) ? 1 : 0);
+  // A relaunch is the one thing that can put a form state on screen other than
+  // the one the tap read, so the field it draws proves nothing about it.
+  const refused = !acrossRelaunch(lastAction) && !submitCouldCommit(args.amountText);
+  const reported = previousCount + (isTxnSubmitTap(lastAction) && !refused ? 1 : 0);
   return { reported, next: fresh ? 0 : reported };
 }
 
+// Could the app have committed anything for that submit? The amount field as
+// the LANDING frame shows it is the form state the tap read: the tap changes
+// nothing about it, and one action runs per step, so nothing else could have.
+// Off the transaction screen there is no field to read, and undefined is
+// unknown, which counts.
+//
+// False only where Folio's own code must have refused. parseCents takes
+// `^\d+(\.\d{1,2})?$` with commas stripped and refuses everything else, and
+// AddTransactionViewModel refuses a parsed zero on top of that. An empty field
+// never even reaches the parser: TxnSubmit is
+// clickable(enabled = amount.isNotBlank()), so the click does not fire.
+//
+// This is the difference between a bound and a useless one. The window is an
+// upper bound on the transactions the interval could hold, and a bound inflated
+// by taps that commit nothing is a bound the app can never exceed: the iOS run
+// in #78 read a rise of 15 transactions against a window of 37 submits and had
+// nothing to say. Measured over four recorded android runs, 19, 11, 25 and 25
+// of 35, 26, 42 and 42 submit taps landed with the amount field empty.
+//
+// An amount too large for a Kotlin Long is refused by the app too, and still
+// counts here: over-counting can only cost a detection, and the reading that
+// would have to prove the overflow is a float that cannot hold the number.
+export function submitCouldCommit(amountText: string | undefined): boolean {
+  if (amountText === undefined) return true;
+  const trimmed = amountText.trim().replace(/,/g, "");
+  if (!/^\d+(\.\d{1,2})?$/.test(trimmed)) return false;
+  return /[1-9]/.test(trimmed);
+}
+
 // 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
diff --git a/pkg/spec/test/folio-submit-window.test.ts b/pkg/spec/test/folio-submit-window.test.ts
index 6e19281..4774165 100644
--- a/pkg/spec/test/folio-submit-window.test.ts
+++ b/pkg/spec/test/folio-submit-window.test.ts
@@ -67,6 +67,96 @@ test("a second submit with no Home reading between them counts two", () => {
   );
 });
 
+// The window is a budget: an upper bound on the transactions the interval could
+// hold. A tap the app's own parser must have refused spends none of it, and on
+// android it does not even reach the parser, because TxnSubmit is
+// clickable(enabled = amount.isNotBlank()). Measured over four recorded android
+// runs, 19, 11, 25 and 25 of 35, 26, 42 and 42 submit taps landed on the
+// transaction screen with the amount field empty, so more than half the budget
+// was being spent on taps that cannot commit anything.
+test("a submit the app must have refused does not spend the window's budget", () => {
+  for (const amountText of ["", "   ", "0", "0.00", "00", "5.", "abc"]) {
+    assert.deepEqual(
+      countSubmitsInWindow({
+        previousCount: 0,
+        lastAction: { kind: "Tap", on: submitOn },
+        amountText,
+        fresh: false,
+      }),
+      { reported: 0, next: 0 },
+      `amount ${JSON.stringify(amountText)} was counted as a possible commit`,
+    );
+  }
+});
+
+// The field as the landing frame shows it, which is the form state the tap read:
+// nothing between the two changes it. Anywhere but the transaction screen there
+// is no field to read, and unknown has to count.
+test("an amount that could commit, or that nobody could read, spends the budget", () => {
+  for (const amountText of ["5", "0.01", "1,000", "999999999999999999999", undefined]) {
+    assert.deepEqual(
+      countSubmitsInWindow({
+        previousCount: 0,
+        lastAction: { kind: "Tap", on: submitOn },
+        amountText,
+        fresh: false,
+      }),
+      { reported: 1, next: 1 },
+      `amount ${JSON.stringify(amountText)} was dropped from the budget`,
+    );
+  }
+});
+
+// The one thing that can put a different form state on screen than the one the
+// tap read: the runner restarting the app, which the tap survives and the typed
+// amount does not. The field a fresh process draws is empty whatever was
+// submitted, so it proves nothing and the submit keeps its place in the budget.
+test("a submit across a relaunch spends the budget whatever the field shows", () => {
+  assert.deepEqual(
+    countSubmitsInWindow({
+      previousCount: 0,
+      lastAction: { kind: "Tap", on: submitOn, applied: true, relaunched: true },
+      amountText: "",
+      fresh: false,
+    }),
+    { reported: 1, next: 1 },
+  );
+});
+
+// What the budget costs the counting invariant, in the shape of the iOS run in
+// #78: a stretch of the walk that never went Home, most of it taps on a submit
+// button with nothing typed into the form, and one double tap that committed
+// twice. Counting the refused taps hands the app five transactions of slack it
+// never used, and two rows against six actions is no violation.
+test("refused submits used to hide a double submit behind their own budget", () => {
+  const frames = [
+    { amountText: "", lastAction: { kind: "Tap", on: submitOn } },
+    { amountText: "", lastAction: { kind: "Tap", on: submitOn } },
+    { amountText: "", lastAction: { kind: "Tap", on: submitOn } },
+    { amountText: "", lastAction: { kind: "Tap", on: submitOn } },
+    { amountText: "", lastAction: { kind: "Tap", on: submitOn } },
+    { amountText: undefined, lastAction: { kind: "DoubleTap", on: submitOn } },
+  ];
+  let budget = 0;
+  for (const frame of frames) {
+    budget = countSubmitsInWindow({
+      previousCount: budget,
+      lastAction: frame.lastAction,
+      amountText: frame.amountText,
+      fresh: false,
+    }).next;
+  }
+  assert.equal(budget, 1);
+  assert.equal(
+    committedTransactionsExceedSubmits({
+      countsBefore: { Checking: 3 },
+      countsAfter: { Checking: 5 },
+      submitsInWindow: budget,
+    }),
+    true,
+  );
+});
+
 // The two traces the freshness rule exists to tell apart, driven step by step
 // through the same pair of carriers the spec holds.
 function run(steps: { route: string | null; totalText?: string; lastAction: unknown }[]) {

From ae3c9fe0912b690f901e4116a4f5302901d322d8 Mon Sep 17 00:00:00 2001
From: PJ <ipriyanshujain@gmail.com>
Date: Sat, 15 Aug 2026 21:24:57 +0530
Subject: [PATCH 8/8] feat(folio): read the amount field into every submit
 window

Each of the three windows asks whether the tap could have committed, off the
field as the landing frame shows it.
---
 examples/folio/sanderling/spec.ts | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/examples/folio/sanderling/spec.ts b/examples/folio/sanderling/spec.ts
index 4555255..260e291 100644
--- a/examples/folio/sanderling/spec.ts
+++ b/examples/folio/sanderling/spec.ts
@@ -104,6 +104,11 @@ const homeCards = oncePerFrame((s: State): CardReading[] =>
 // the last-read Home total so `previous` and `current` stay on the same scale.
 const homeTotalText = (s: State) => on("home", "TotalBalance")(s)?.text;
 
+// The amount field as the frame a submit landed on shows it, which is the form
+// state that submit read. Every window below asks, because a submit the app
+// must have refused raises no bound: see submitCouldCommit.
+const txnAmountText = oncePerFrame((s: State) => on("add-transaction", "TxnAmountField")(s)?.text);
+
 let lastHomeTotal: number | null = null;
 const totalBalance = extract<number | null>("totalBalance", s => {
   const reading = readHomeTotalBalance({
@@ -129,6 +134,7 @@ const submitsInWindow = extract("submitsInWindow", s => {
   const window = countSubmitsInWindow({
     previousCount: submitsSinceHomeTotal,
     lastAction: s.lastAction,
+    amountText: txnAmountText(s),
     fresh,
   });
   submitsSinceHomeTotal = window.next;
@@ -177,6 +183,7 @@ const submitsSinceCounts = extract("submitsSinceCounts", s => {
   const window = countSubmitsInWindow({
     previousCount: submitsSinceHomeCards,
     lastAction: s.lastAction,
+    amountText: txnAmountText(s),
     fresh,
   });
   submitsSinceHomeCards = window.next;
@@ -215,6 +222,7 @@ const submitsSinceBalance = extract("submitsSinceAccountBalance", s => {
   const window = countSubmitsInWindow({
     previousCount: submitsSinceAccountBalance,
     lastAction: s.lastAction,
+    amountText: txnAmountText(s),
     fresh,
   });
   submitsSinceAccountBalance = window.next;