From 40c39e93b9337f001c02c5131d862537afbe7edf Mon Sep 17 00:00:00 2001 From: PJ Date: Sun, 16 Aug 2026 01:09:56 +0530 Subject: [PATCH 1/7] fix(folio): the bound carries no unconfirmed-submit guard deleting confirmedApplied here broke 0 of 355 tests: under a bound a submit that may not have landed moves the balance by 0, which the bound already permits, so the guard could only ever drop the double commit it exists to catch. the relaunch guard stays for a reason the bound does not cover, and both tests now assert a verdict that changes when their guard does. --- examples/folio/sanderling/predicates.ts | 20 +++++++---- .../folio-submit-balance-predicate.test.ts | 34 +++++++++++-------- 2 files changed, 32 insertions(+), 22 deletions(-) diff --git a/examples/folio/sanderling/predicates.ts b/examples/folio/sanderling/predicates.ts index 37415e3..473e096 100644 --- a/examples/folio/sanderling/predicates.ts +++ b/examples/folio/sanderling/predicates.ts @@ -736,13 +736,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/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, ); From 969f58b329924d30e1a6409748092004f5aa47be Mon Sep 17 00:00:00 2001 From: PJ Date: Sun, 16 Aug 2026 01:10:49 +0530 Subject: [PATCH 2/7] test(folio): judge the conjunct on the landings a real run produces three of the 18 frames the recorded ios run drove it down, each with the second commit the bound is there to catch. neutering the comparison reddens it: a second commit on 357900 went unjudged. --- pkg/spec/test/folio-ledger-window.test.ts | 31 +++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/pkg/spec/test/folio-ledger-window.test.ts b/pkg/spec/test/folio-ledger-window.test.ts index 49bf8e5..5f47229 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. From a275bf766c0c3e67a4b63ed762051e3fa408a888 Mon Sep 17 00:00:00 2001 From: PJ Date: Sun, 16 Aug 2026 01:12:09 +0530 Subject: [PATCH 3/7] test(folio): the walk drives the composition the spec runs countSubmitsInWindow never saw an amountText here, so every walk test counted submits the app must have refused. with the field passed, a refused submit no longer buys a later double tap an alibi: without it the window reads 3, not 1. --- pkg/spec/test/folio-ledger-window.test.ts | 39 ++++++++++++++++++++--- 1 file changed, 34 insertions(+), 5 deletions(-) diff --git a/pkg/spec/test/folio-ledger-window.test.ts b/pkg/spec/test/folio-ledger-window.test.ts index 5f47229..a0fa6ae 100644 --- a/pkg/spec/test/folio-ledger-window.test.ts +++ b/pkg/spec/test/folio-ledger-window.test.ts @@ -317,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; @@ -342,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; @@ -389,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 }, From e6e71f9ba0e3353514be2252243261e55cd10938 Mon Sep 17 00:00:00 2001 From: PJ Date: Sun, 16 Aug 2026 01:12:32 +0530 Subject: [PATCH 4/7] docs(folio): say which double submit the conjunct can see, and which it cannot the home landing is the counting invariant's, three of three in the recorded ios run; this one gets the interleaving whose second pop is cancelled. it is still the only judge on the 18 ledger landings that run produced. --- examples/folio/sanderling/predicates.ts | 42 +++++++++++++++++-------- 1 file changed, 29 insertions(+), 13 deletions(-) diff --git a/examples/folio/sanderling/predicates.ts b/examples/folio/sanderling/predicates.ts index 473e096..8a0dbfd 100644 --- a/examples/folio/sanderling/predicates.ts +++ b/examples/folio/sanderling/predicates.ts @@ -602,20 +602,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 them, had nowhere else to be caught: Home's total was read once 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 From dfa36606593c0b963974ebd174cf165e8eba0c1e Mon Sep 17 00:00:00 2001 From: PJ Date: Sun, 16 Aug 2026 01:12:51 +0530 Subject: [PATCH 5/7] docs(folio): the narrow window is not where the detection comes from the double taps land on home, so the counting form convicts them; what turned 0 convictions into 4 on the recorded ios run is submitCouldCommit, which drops the windows at those three steps from 5/4/7 to 2/1/2. --- examples/folio/sanderling/spec.ts | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) 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( () => From a3ed4608da149a07f97c9141ac48cd51109645b0 Mon Sep 17 00:00:00 2001 From: PJ Date: Sun, 16 Aug 2026 01:14:26 +0530 Subject: [PATCH 6/7] fix(folio): an amount over the app's cap spends no window budget the corpus reaches TxnSubmit with 999999999999999999999, AMOUNT_REGEX takes it and AddTransactionViewModel refuses it against MAX_TRANSACTION_AMOUNT_CENTS, so counting it was budget a double submit could hide behind. --- examples/folio/sanderling/predicates.ts | 16 +++++++++++---- pkg/spec/test/folio-submit-window.test.ts | 25 +++++++++++++++++++++-- 2 files changed, 35 insertions(+), 6 deletions(-) diff --git a/examples/folio/sanderling/predicates.ts b/examples/folio/sanderling/predicates.ts index 8a0dbfd..21f1b7e 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 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, From 32d78bfc0bdada58cc438c96c950e700d659c754 Mon Sep 17 00:00:00 2001 From: PJ Date: Sun, 16 Aug 2026 01:15:30 +0530 Subject: [PATCH 7/7] docs(folio): say which form judged one step, not which node was read once --- examples/folio/sanderling/predicates.ts | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/folio/sanderling/predicates.ts b/examples/folio/sanderling/predicates.ts index 21f1b7e..b0a07fe 100644 --- a/examples/folio/sanderling/predicates.ts +++ b/examples/folio/sanderling/predicates.ts @@ -633,8 +633,8 @@ export function committedTransactionsExceedSubmits(args: { // 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 them, had nowhere else to be caught: Home's total was read once in the -// whole run. +// 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.