Merge branch 'folio-spec-attribution' into trial-merge

examples/folio/sanderling/predicates.ts

@@ -106,6 +106,21 @@ export function readHomeTotalBalance(args: {
 //
 // 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.
+//
+// A non-empty list is trusted as current, and that rests on the app's shape
+// rather than on anything in the frame. `fresh` also resets the submit window,
+// so a card list drawn before the store caught up with a commit would bank
+// stale counts, start the next window empty, and leave the rise arriving with
+// no budget to cover it: a healthy app convicted of a double submit. Folio
+// cannot serve that frame. AddTransactionViewModel.submit pops ONE entry, so a
+// commit lands back on the ledger it came from and the first Home reading is a
+// whole action and settle later. Two pops do reach Home, but two pops means two
+// Submit events, which is the double submit itself, and a verdict there is
+// late rather than wrong. Measured over four recorded android runs: 51
+// commit-capable single taps landed on the ledger or the transaction screen and
+// none on Home, 49 of 49 commits already showed their new balance in the frame
+// read at the same step, and no rise ever arrived against an empty budget in
+// 1303 steps. A submit that navigated straight to Home would reopen this.
 export interface HomeCardReading<T> {
   value: T | null;
   carrier: T | null;
@@ -678,12 +693,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 +754,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 +769,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;
 }

examples/folio/sanderling/spec.ts

@@ -258,10 +258,15 @@ const newAccountBalanceIsZero = always(
   ),
 );
 
-// Property 2: a tap on TxnSubmit must move the total balance by exactly the
-// typed amount. A double-submit lands two transactions, so the balance shifts
-// by twice the typed amount and the check fires. The route gate inside the
+// Property 2: a tap on TxnSubmit cannot move the total balance by more than the
+// typed amount. A double-submit lands two transactions, so the balance shifts by
+// twice the typed amount and the check fires. The route gate inside the
 // predicate skips off-Home landings where totalBalance.current is the carrier.
+//
+// The name is the property's, and the gate keys on it, so it stays; what it
+// demands is the bound, for the reason submitChangesBalanceByTypedAmount gives:
+// a total that has not re-rendered yet has not moved, and an equality convicts a
+// healthy app for a frame that has not caught up.
 const submitMovesBalanceByTypedAmount = always(
   next(() =>
     submitChangesBalanceByTypedAmount({

pkg/spec/test/folio-home-card-readings.test.ts

@@ -107,6 +107,7 @@ function run(steps: { route: string | null; cards: CardReading[]; lastAction: un
 
 const idle = { kind: "Tap", on: "testTag:AccountCard" };
 const doubleSubmit = { kind: "DoubleTap", on: "testTag:AddTransactionScreen > testTag:TxnSubmit" };
+const submit = { kind: "Tap", on: "testTag:AddTransactionScreen > testTag:TxnSubmit" };
 
 test("an un-laid-out Home no longer kills the counting invariant", () => {
   const trace = run([
@@ -157,3 +158,45 @@ test("an un-laid-out Home does not close the counting window", () => {
     true,
   );
 });
+
+// What keeps a healthy submit from ever arriving as a rise nobody paid for. The
+// reading banked here also resets the submit window, so a Home card list drawn
+// before the store caught up with a commit would bank stale counts, start the
+// next window empty, and leave the rise turning up with no budget to cover it.
+// The app cannot put that frame in front of the spec: submit() pops one entry,
+// so a commit lands back on the ledger it came from and the first Home reading
+// is a whole action later, with the submit still in the window when the rise
+// does show up.
+test("a submit landing on the ledger is still in the window when Home reads it", () => {
+  const trace = run([
+    { route: "home", cards: [card("Checking", 0, "3")], lastAction: idle },
+    { route: "ledger", cards: [], lastAction: submit },
+    { route: "home", cards: [card("Checking", 5000, "4")], lastAction: idle },
+  ]);
+  assert.equal(trace[2]?.submits, 1);
+  assert.equal(
+    committedTransactionsExceedSubmits({
+      countsBefore: trace[1]?.counts ?? null,
+      countsAfter: trace[2]?.counts ?? null,
+      submitsInWindow: trace[2]?.submits ?? 0,
+    }),
+    false,
+  );
+});
+
+test("and a double submit down that same path still convicts", () => {
+  const trace = run([
+    { route: "home", cards: [card("Checking", 0, "3")], lastAction: idle },
+    { route: "ledger", cards: [], lastAction: doubleSubmit },
+    { route: "home", cards: [card("Checking", 10000, "5")], lastAction: idle },
+  ]);
+  assert.equal(trace[2]?.submits, 1);
+  assert.equal(
+    committedTransactionsExceedSubmits({
+      countsBefore: trace[1]?.counts ?? null,
+      countsAfter: trace[2]?.counts ?? null,
+      submitsInWindow: trace[2]?.submits ?? 0,
+    }),
+    true,
+  );
+});

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,
   );
 });