diff --git a/examples/folio/sanderling/predicates.ts b/examples/folio/sanderling/predicates.ts index 37415e3..b0a07fe 100644 --- a/examples/folio/sanderling/predicates.ts +++ b/examples/folio/sanderling/predicates.ts @@ -283,6 +283,9 @@ export function countSubmitsInWindow(args: { return { reported, next: fresh ? 0 : reported }; } +// Folio's own cap, in cents (core/data/Repository.kt). +const MAX_TRANSACTION_AMOUNT_CENTS = 100_000_000; + // 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. @@ -302,14 +305,19 @@ export function countSubmitsInWindow(args: { // 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. +// An amount over Folio's cap is refused before any coroutine starts +// (MAX_TRANSACTION_AMOUNT_CENTS, checked in both AddTransactionViewModel.submit +// and Repository.createTransaction), and the fuzzer's corpus reaches the button +// with one: "999999999999999999999" passes AMOUNT_REGEX, so the field takes it. +// Float is precise enough to say which side of the cap an amount is on. The cap +// is 1e8, every integer cent up to 2^53 is exact, and an amount far enough above +// it to be inexact is far enough above it to be refused. 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); + if (!/[1-9]/.test(trimmed)) return false; + return Number(trimmed) * 100 <= MAX_TRANSACTION_AMOUNT_CENTS; } // Parses formatCents output like "$5.00", "-$1,234.56", "+$0.50" back to @@ -602,20 +610,36 @@ export function committedTransactionsExceedSubmits(args: { // 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 submitChangesBalanceByAtMostTypedAmount 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. +// An UPPER BOUND, the same one submitChangesBalanceByAtMostTypedAmount applies +// to Home's total, 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 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. +// What it can convict, and what it cannot. The double tap sends two Submit +// events, and where they land decides who judges them. Two commits and two pops +// reach Home, where this reads no balance at all and +// committedTransactionsExceedSubmits does the convicting: that is the shape the +// recorded iOS run at runs/folio-ios/20260815-102711 produced, three double taps +// out of three, all on Home. Two commits with the second pop cancelled by the +// first stop on the account's own ledger, and only this sees them. So this is +// not the check that fixed #78, and widening its route gate would not make it +// one: readAccountBalance drops the carrier off these two screens, so a Home +// landing has nothing to compare. +// +// It is not idle either. Over that same run it judged 18 of 240 steps against +// real readings, every one a submit landing back on the ledger with the balance +// moved by exactly what was typed. A commit for more than the amount typed, on +// any of those 18, had nowhere else to be caught: the total-balance form got +// past its own gates on one step in the whole run. +// +// A submit the runner could not confirm needs no case of its own: 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 @@ -736,13 +760,19 @@ export function submitChangesBalanceByAtMostTypedAmount(args: { if (route !== "home") return true; if (!isTxnSubmitTap(lastAction)) return true; - // The whole rule is that the delta belongs to THIS submit. A submit the - // 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. + // The two totals were read from two different processes. SqlLedgerStore + // starts each one on stateIn(Eagerly, emptyList()) and HomeScreen composes + // formatCents(total) off whatever the flow holds, so a restarted app draws + // $0.00 into TotalBalance until sqlite answers, and that number is as far + // from the last one as the accounts are rich. There is no submit anywhere + // that explains it. + // + // A submit the runner could not confirm needs no guard of its own: it may + // have committed nothing, and a balance that did not move is under any bound. + // countSubmitsInWindow counts it exactly like a confirmed one, so a total + // that moved by more than one typed amount is the same double commit either + // way. Under the equality this used to be, that case had to be excused; a + // guard for it here now only drops the convictions it exists to make. if (acrossRelaunch(lastAction)) return true; if (submitsInWindow !== 1) return true; if (typedAmount === 0) return true; diff --git a/examples/folio/sanderling/spec.ts b/examples/folio/sanderling/spec.ts index 2511a5a..4f7d952 100644 --- a/examples/folio/sanderling/spec.ts +++ b/examples/folio/sanderling/spec.ts @@ -286,12 +286,22 @@ const submitMovesBalanceByAtMostTypedAmount = always( // 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. +// One rule, two windows, and they judge different frames rather than the same +// frame twice. The counting form compares two Home readings, which is where a +// double tap lands: submit() pops one entry per commit, so two commits walk the +// stack back past the ledger to Home. What used to defeat it there was the +// width of the window, not the window's screen, and what fixed it is +// submitCouldCommit refusing to count submits the app cannot have accepted. +// Replaying the iOS run at runs/folio-ios/20260815-102711 through this file +// measures it: the three double taps sit in windows of 2, 1 and 2 submits with +// that rule and 5, 4 and 7 without, and the run convicts 4 times with it and 0 +// times without. +// +// 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. It judges +// the frames the counting form cannot see between two Home visits, and catches +// the double submit whose second pop never ran: see +// committedAmountExceedsOneSubmit. const submitCommitsOneTransactionPerAction = always( next( () => diff --git a/pkg/spec/test/folio-ledger-window.test.ts b/pkg/spec/test/folio-ledger-window.test.ts index 49bf8e5..a0fa6ae 100644 --- a/pkg/spec/test/folio-ledger-window.test.ts +++ b/pkg/spec/test/folio-ledger-window.test.ts @@ -145,6 +145,37 @@ test("one submit moving the balance by exactly the typed amount is the app worki } }); +// The frames this bound is actually driven down, replayed off the recorded iOS +// run at runs/folio-ios/20260815-102711 (seed 7, 240 steps). It judged 18 of +// them and fired on none: every one was a single Tap on TxnSubmit landing back +// on the account's own ledger with the balance moved by exactly what was typed, +// which is the app working. Three of those readings are below, with the same +// frame as it looks when the one action commits twice. +// +// A double tap is nowhere in that list, and the run took three of them: all +// three landed on Home, where this conjunct has no balance to read and +// committedTransactionsExceedSubmits convicted instead. What reaches here is +// the interleaving where the second commit's pop does not run. +test("the ledger landings a real run produces are judged, and a doubled one fires", () => { + for (const [prev, typed] of [ + [357900, 25100], + [455800, 7900], + [682500, 19300], + ]) { + const judge = (currAccountBalance: number) => + committedAmountExceedsOneSubmit({ + route: "ledger", + lastAction: submit, + submitsInWindow: 1, + typedAmount: typed!, + prevAccountBalance: prev!, + currAccountBalance, + }); + assert.equal(judge(prev! + typed!), false, `the recorded ${prev} -> ${prev! + typed!} was convicted`); + assert.equal(judge(prev! + 2 * typed!), true, `a second commit on ${prev} went unjudged`); + } +}); + // 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. @@ -286,8 +317,11 @@ test("Home shows every account's money, so it is not this comparison's scale", ( }); // 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. +// carried, the amount field as that frame shows it, and the action that got +// there. Driven through the same carrier and window the spec holds, `typed` +// included: the spec hands the landing frame's field to countSubmitsInWindow +// and the previous frame's to the property, and a walk that skips the first +// half drives a composition the spec never runs. interface Frame { route: string | null; balanceText?: string; @@ -311,6 +345,7 @@ function walk(frames: readonly Frame[]) { const window = countSubmitsInWindow({ previousCount: submits, lastAction: frame.lastAction, + amountText: frame.route === "add-transaction" ? (frame.typed ?? "") : undefined, fresh: reading.fresh, }); submits = window.next; @@ -358,9 +393,34 @@ test("the Home window cannot judge a walk that never goes Home", () => { } }); -// 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. +// The trajectory the recorded iOS run took to the frames this property judges, +// with the taps that reach TxnSubmit over an empty field: 40 of its 61 submit +// taps landed back on the transaction screen, and the field they read is the +// one the landing frame shows. Counting those as submits is what the run +// measures as the difference between 4 convictions and 0. Here the balance node +// is off the viewport while they happen, so nothing resets the window and the +// slack survives to the frame that matters. +test("submits the app must have refused do not buy a double tap an alibi", () => { + const verdicts = walk([ + { route: "ledger", balanceText: "$100.00", lastAction: openLedger }, + { route: "add-transaction", lastAction: openAddTxn }, + { route: "add-transaction", lastAction: submit }, + { route: "add-transaction", lastAction: submit }, + { route: "add-transaction", typed: "196", lastAction: typeAmount }, + { route: "ledger", balanceText: "$492.00", lastAction: doubleSubmit }, + ]); + assert.equal(verdicts[5]?.submits, 1); + assert.equal(verdicts[5]?.violated, true); +}); + +// The same trajectory, judged where the app actually is. The double tap sends +// two Submit events, and the frame it lands on says which of the two shapes +// they took: two commits and two pops reach Home, where the counting invariant +// judges them, and two commits with the second pop cancelled by the first stop +// on the account's own ledger, which is this one. The recorded iOS run took +// three double taps and all three landed on Home, so this frame is reasoned +// from the app's code (AddTransactionViewModel.submit commits inside +// viewModelScope, then pops) rather than measured. test("the double tap is convicted on the frame it lands on", () => { const verdicts = walk([ { route: "ledger", balanceText: "$100.00", lastAction: openLedger }, diff --git a/pkg/spec/test/folio-submit-balance-predicate.test.ts b/pkg/spec/test/folio-submit-balance-predicate.test.ts index 1617089..e2be9da 100644 --- a/pkg/spec/test/folio-submit-balance-predicate.test.ts +++ b/pkg/spec/test/folio-submit-balance-predicate.test.ts @@ -504,20 +504,23 @@ test("freshness boundary: a window with no submit in it is vacuous", () => { }); // applied: null is the runner saying it dispatched the tap and never learned -// whether it landed. A submit that committed nothing leaves the balance where -// it was, so demanding the typed amount of movement for it convicts an app that -// did exactly what it should have. -test("a submit the runner could not confirm demands no balance move", () => { +// whether it landed. Under the bound that buys the app nothing it did not +// already have: a submit that committed nothing leaves the balance where it +// was, and a balance that has not moved is under any bound. What the window +// still promises is that no OTHER submit action could have moved it, because +// countSubmitsInWindow counts an unconfirmed tap exactly like a confirmed one. +// So a move of twice the typed amount is the same double commit either way. +test("a submit the runner could not confirm is still held to the bound", () => { assert.equal( submitChangesBalanceByAtMostTypedAmount({ route: "home", - lastAction: { kind: "Tap", on: submitOn, applied: null }, + lastAction: { kind: "DoubleTap", on: submitOn, applied: null }, submitsInWindow: 1, typedAmount: 500, prevTotalBalance: 1000, - currTotalBalance: 1000, + currTotalBalance: 2000, }), - true, + false, ); }); @@ -583,20 +586,21 @@ test("the measured double submit still fires under the bound", () => { }); // 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", () => { +// after this action, so the two totals being compared were read from two +// different processes. SqlLedgerStore starts every one of them on +// stateIn(Eagerly, emptyList()) and HomeScreen composes formatCents(total) off +// whatever the flow holds, so the restarted app draws $0.00 into TotalBalance +// until sqlite answers. That reading is not a total this tap moved, and it is +// as far from the last one as the account is rich. +test("a total drawn by a restarted process is not compared with the old one", () => { assert.equal( submitChangesBalanceByAtMostTypedAmount({ route: "home", lastAction: { kind: "Tap", on: submitOn, applied: true, relaunched: true }, submitsInWindow: 1, typedAmount: 500, - prevTotalBalance: 1000, - currTotalBalance: 1000, + prevTotalBalance: 455800, + currTotalBalance: 0, }), true, ); diff --git a/pkg/spec/test/folio-submit-window.test.ts b/pkg/spec/test/folio-submit-window.test.ts index 4774165..6349113 100644 --- a/pkg/spec/test/folio-submit-window.test.ts +++ b/pkg/spec/test/folio-submit-window.test.ts @@ -89,11 +89,32 @@ test("a submit the app must have refused does not spend the window's budget", () } }); +// Folio caps a transaction at $1,000,000.00 (MAX_TRANSACTION_AMOUNT_CENTS, in +// core/data/Repository.kt), and AddTransactionViewModel.submit refuses anything +// over it before a coroutine starts. The fuzzer's corpus carries +// "999999999999999999999", AMOUNT_REGEX lets it into the field and it reaches +// the button, so this is a refusal the window used to pay for. +test("an amount over the app's cap cannot commit", () => { + for (const amountText of ["1000000.01", "1,000,001", "999999999999999999999"]) { + 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. +// is no field to read, and unknown has to count. The cap itself is an amount the +// app takes, so it counts too. 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]) { + for (const amountText of ["5", "0.01", "1,000", "1000000.00", "999999.99", undefined]) { assert.deepEqual( countSubmitsInWindow({ previousCount: 0,