From 6e8e6d51fee334023647d44b66a12e7167be8e70 Mon Sep 17 00:00:00 2001 From: PJ Date: Sat, 15 Aug 2026 22:55:09 +0530 Subject: [PATCH 1/4] 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 | 31 +++++++--- .../folio-submit-balance-predicate.test.ts | 61 +++++++++++++++++++ pkg/spec/test/folio-transition-frame.test.ts | 20 +++++- 3 files changed, 103 insertions(+), 9 deletions(-) diff --git a/examples/folio/sanderling/predicates.ts b/examples/folio/sanderling/predicates.ts index 27bee6d..a4b0445 100644 --- a/examples/folio/sanderling/predicates.ts +++ b/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; } diff --git a/pkg/spec/test/folio-submit-balance-predicate.test.ts b/pkg/spec/test/folio-submit-balance-predicate.test.ts index 280f18a..4daff32 100644 --- a/pkg/spec/test/folio-submit-balance-predicate.test.ts +++ b/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 diff --git a/pkg/spec/test/folio-transition-frame.test.ts b/pkg/spec/test/folio-transition-frame.test.ts index 64bcbf3..a886650 100644 --- a/pkg/spec/test/folio-transition-frame.test.ts +++ b/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, ); }); From 21a020de74d082d9f9335c177ac33fbfb8e8eac6 Mon Sep 17 00:00:00 2001 From: PJ Date: Sat, 15 Aug 2026 22:55:13 +0530 Subject: [PATCH 2/4] docs(folio): say what property 2 demands now that it is a bound --- examples/folio/sanderling/spec.ts | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/examples/folio/sanderling/spec.ts b/examples/folio/sanderling/spec.ts index 260e291..0881aae 100644 --- a/examples/folio/sanderling/spec.ts +++ b/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({ From 4027aa1e4489c24852d2d0e964a019792082394e Mon Sep 17 00:00:00 2001 From: PJ Date: Sat, 15 Aug 2026 23:02:37 +0530 Subject: [PATCH 3/4] test(folio): pin that a commit stays in the window until Home reads it The interaction that keeps a stale Home card list from ever banking counts the budget has already forgotten: a submit lands on the ledger, so the reading that resets the window is a whole action later and the submit is still in it. Characterization, not a regression: no code changed and it cannot go red first. --- .../test/folio-home-card-readings.test.ts | 43 +++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/pkg/spec/test/folio-home-card-readings.test.ts b/pkg/spec/test/folio-home-card-readings.test.ts index c76babe..876ab67 100644 --- a/pkg/spec/test/folio-home-card-readings.test.ts +++ b/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, + ); +}); From 8ad68b278fa4a07a78671b4c90b07af6abcf4bdd Mon Sep 17 00:00:00 2001 From: PJ Date: Sat, 15 Aug 2026 23:02:42 +0530 Subject: [PATCH 4/4] docs(folio): record why a banked card reading can be trusted as current The freshness rule rests on the app popping one entry back to the ledger, not on anything the frame carries, so the assumption and the measurements behind it belong next to it. --- examples/folio/sanderling/predicates.ts | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/examples/folio/sanderling/predicates.ts b/examples/folio/sanderling/predicates.ts index a4b0445..3411450 100644 --- a/examples/folio/sanderling/predicates.ts +++ b/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 { value: T | null; carrier: T | null;