diff --git a/examples/folio/sanderling/predicates.ts b/examples/folio/sanderling/predicates.ts index 27bee6d..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; @@ -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; } 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({ 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, + ); +}); 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, ); });