fix(folio): bound the total-balance move instead of demanding it exactly

The write finishes before AddTransactionViewModel navigates, but nothing
establishes that Home's total has re-rendered before the frame is read, and
an equality convicts a healthy app for a total one frame behind. A delta of
zero is exactly the shape nine of the eleven measured android false
convictions had. 2x still exceeds x, so all four recorded convictions
survive, checked against the traces.

The trade is real: a balance that moves by LESS than the amount typed is no
longer judged anywhere in this spec.

examples/folio/sanderling/predicates.ts

@@ -678,12 +678,27 @@ export function parseTypedAmount(text: string | undefined | null): number {
 }
 
 // When the last action is a tap (or double-tap) on the transaction Submit
-// button, the absolute change in total balance must equal the amount the
-// user typed. A double-submit lands two transactions and shifts the balance
-// by 2x the typed amount, tripping this check. The route gate skips steps
-// whose landing screen is not Home: totalBalance is only freshly read from
-// Home's own TOTAL BALANCE node, so off-Home comparisons would read a stale
-// carrier value and false-fire.
+// button, the absolute change in total balance cannot EXCEED 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 read from Home's own
+// TOTAL BALANCE node, so off-Home comparisons would read a stale carrier value
+// and false-fire.
+//
+// A bound rather than the equality this used to be, and the same bound
+// committedAmountExceedsOneSubmit applies to the account's own balance. The
+// write finishes before AddTransactionViewModel navigates, but nothing
+// establishes that Home's total has re-rendered before the frame is read: the
+// store's flow re-emits on its own schedule. A total that has not caught up has
+// not moved at all, and an equality convicts a healthy app for it.
+//
+// The cost is real and is not covered anywhere else in this spec: a balance
+// that moves by LESS than the amount typed, a transaction silently dropped or
+// committed for the wrong amount, is a bug this no longer judges. It cannot be
+// told apart from a total one frame behind, and a check that fires on both is
+// evidence about neither. What it keeps is the bug it exists for: every one of
+// the four recorded android convictions is a 6400 move against 3200 typed, and
+// 2x still exceeds x.
 //
 // 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
@@ -724,7 +739,7 @@ export function submitChangesBalanceByTypedAmount(args: {
   // transaction at whatever fits a Kotlin Long, so a balance of ~1e18 cents is
   // one accepted amount away, and up there the gap between representable
   // values is 128 cents: a real 1600-cent move reads back as something else
-  // entirely. The equality below is then false for a healthy single submit
+  // entirely. The comparison below is then false for a healthy single submit
   // exactly as readily as for a double one, and a check that cannot pass is not
   // a check that failed.
   //
@@ -739,5 +754,5 @@ export function submitChangesBalanceByTypedAmount(args: {
   if (!Number.isSafeInteger(prevTotalBalance)) return true;
   if (!Number.isSafeInteger(currTotalBalance)) return true;
   if (!Number.isSafeInteger(typedAmount)) return true;
-  return Math.abs(currTotalBalance - prevTotalBalance) === typedAmount;
+  return Math.abs(currTotalBalance - prevTotalBalance) <= typedAmount;
 }

pkg/spec/test/folio-submit-balance-predicate.test.ts

@@ -521,6 +521,67 @@ test("a submit the runner could not confirm demands no balance move", () => {
   );
 });
 
+// The write finishes before AddTransactionViewModel navigates, but nothing
+// establishes that Home's total has re-rendered by the time the frame is read:
+// the store's flow re-emits on its own schedule and the destination composes off
+// whatever value it has. A total that has not caught up has not moved at all,
+// and an equality reads that as the app having ignored the amount.
+test("a commit the Home total has not caught up with is not a violation", () => {
+  assert.equal(
+    submitChangesBalanceByTypedAmount({
+      route: "home",
+      lastAction: { kind: "Tap", on: submitOn, applied: true },
+      submitsInWindow: 1,
+      typedAmount: 19600,
+      prevTotalBalance: 220900,
+      currTotalBalance: 220900,
+    }),
+    true,
+  );
+});
+
+// What the bound gives up, and it is a real bug class: an app that moves the
+// balance by LESS than the amount typed. Nothing in this spec judges that any
+// more. It cannot be told apart from a total that has not caught up, and a check
+// that fires on both is not evidence about either.
+test("an under-move is no longer judged, which is the trade", () => {
+  assert.equal(
+    submitChangesBalanceByTypedAmount({
+      route: "home",
+      lastAction: { kind: "Tap", on: submitOn, applied: true },
+      submitsInWindow: 1,
+      typedAmount: 19600,
+      prevTotalBalance: 0,
+      currTotalBalance: 10000,
+    }),
+    true,
+  );
+});
+
+// The witness measured on four recorded android runs, all four of which convict
+// here and nowhere else: the double tap moved the total by 6400 against 3200
+// typed. The bound has to keep every one of them.
+test("the measured double submit still fires under the bound", () => {
+  for (const [prev, curr] of [
+    [17952800, 17959200],
+    [19796100, 19802500],
+    [200000032904800, 200000032911200],
+  ]) {
+    assert.equal(
+      submitChangesBalanceByTypedAmount({
+        route: "home",
+        lastAction: { kind: "DoubleTap", on: submitOn, applied: true },
+        submitsInWindow: 1,
+        typedAmount: 3200,
+        prevTotalBalance: prev ?? null,
+        currTotalBalance: curr ?? null,
+      }),
+      false,
+      `the double submit at ${prev} -> ${curr} stopped firing`,
+    );
+  }
+});
+
 // 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

pkg/spec/test/folio-transition-frame.test.ts

@@ -131,7 +131,11 @@ test("the measured android transition chain no longer convicts at delta 0", () =
   );
 
   // What the reset bought the old spec: the same landing, judged against a
-  // window of one and a total the transition frame had already banked.
+  // window of one and a total the transition frame had already banked. It
+  // convicted on a delta of zero, and that shape cannot convict any more even
+  // with the window reset back to one, because the property is a bound rather
+  // than an equality. A balance that did not move is under any typed amount,
+  // whether nothing was submitted or the total has not caught up yet.
   assert.equal(
     submitChangesBalanceByTypedAmount({
       route: "home",
@@ -141,6 +145,20 @@ test("the measured android transition chain no longer convicts at delta 0", () =
       prevTotalBalance: 8691100,
       currTotalBalance: 8691100,
     }),
+    true,
+  );
+
+  // The double tap it was always meant to catch is untouched by that: two
+  // 33900 debits against one action still exceed the amount typed for it.
+  assert.equal(
+    submitChangesBalanceByTypedAmount({
+      route: "home",
+      lastAction: { ...phantomSubmit, kind: "DoubleTap" },
+      submitsInWindow: 1,
+      typedAmount: 33900,
+      prevTotalBalance: 8691100,
+      currTotalBalance: 8691100 - 67800,
+    }),
     false,
   );
 });