From dc2da35e2c101659879b39ca6e3397b47d35485c Mon Sep 17 00:00:00 2001 From: PJ Date: Mon, 17 Aug 2026 23:27:33 +0530 Subject: [PATCH] feat(folio-web): predicates for counting commits against submit actions --- examples/folio-web/sanderling/predicates.ts | 148 +++++++ .../test/folio-web-submit-counting.test.ts | 363 ++++++++++++++++++ 2 files changed, 511 insertions(+) create mode 100644 examples/folio-web/sanderling/predicates.ts create mode 100644 pkg/spec/test/folio-web-submit-counting.test.ts diff --git a/examples/folio-web/sanderling/predicates.ts b/examples/folio-web/sanderling/predicates.ts new file mode 100644 index 0000000..fcfa792 --- /dev/null +++ b/examples/folio-web/sanderling/predicates.ts @@ -0,0 +1,148 @@ +// A Home reading and the carrier it advances. +// +// A frame that is not Home, and a Home frame whose card list has not rendered, +// are the same case: nothing was read, so the last value we did read is +// reported and carried on unchanged. An empty list is equally "the app has no +// accounts" and "the app has not drawn them yet", and taking it as a reading is +// what would bank an empty window and leave the next rise arriving with no +// budget to cover it. +// +// `fresh` marks the one event that closes a comparison window, so it also +// resets the submit count taken over that window. +export interface HomeReading { + value: T | null; + carrier: T | null; + fresh: boolean; +} + +export function readHomeCards(args: { + onHome: boolean; + reading: T | null; + previousCarrier: T | null; +}): HomeReading { + const { onHome, reading, previousCarrier } = args; + if (!onHome || reading === null) { + return { value: previousCarrier, carrier: previousCarrier, fresh: false }; + } + return { value: reading, carrier: reading, fresh: true }; +} + +export interface CardReading { + accountId: string; + count: number | undefined; +} + +// Transactions committed per account, keyed by the account id the card carries. +// A card whose id or count is unreadable is left out rather than guessed at, +// and a reading with nothing left in it is unknown. +export function homeTxnCountsOf(cards: readonly CardReading[]): Record | null { + const counts: Record = {}; + for (const card of cards) { + if (card.accountId === "" || card.count === undefined) continue; + if (!Number.isSafeInteger(card.count)) continue; + counts[card.accountId] = card.count; + } + return Object.keys(counts).length === 0 ? null : counts; +} + +// state.lastAction as the runner builds it (internal/verifier/marshal.go +// lastActionFields), read defensively: every field is what a Go struct decided +// to emit, not something this file can trust a compile-time shape for. +export interface ObservedAction { + kind?: string; + on?: string | object; + applied?: true | null; +} + +// Is this the action that commits a transaction? Nothing else in the app +// reaches createTransaction: the add-transaction form's onSubmit is the only +// caller, and the txn-submit button is the only control that submits it. A +// double tap counts once, because it is one action. +export function isTxnSubmitTap(lastAction: ObservedAction | null): boolean { + if (lastAction == null) return false; + if (lastAction.kind !== "Tap" && lastAction.kind !== "DoubleTap") return false; + const on = lastAction.on; + const onText = typeof on === "string" ? on : on != null ? JSON.stringify(on) : ""; + return onText.includes("txn-submit"); +} + +// 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: one action runs +// per step and a tap changes no field, so nothing else could have. Off the +// transaction screen there is no field to read, and undefined is unknown, +// which counts. +// +// False only where the app's own code must have refused. This mirrors +// parseCents (src/format.ts) plus the handler's own `cents <= 0` rejection, and +// an empty field never reaches either: the submit button is disabled while the +// amount is blank, so no click fires at all. +// +// This is the difference between a bound and a useless one. The window is an +// upper bound on the transactions its interval could hold, and a bound inflated +// by taps that commit nothing is a bound a double submit hides behind: of 108 +// add-transaction frames in the recalibration run, 65 showed the amount field +// empty. +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; + const dot = trimmed.indexOf("."); + const whole = dot < 0 ? trimmed : trimmed.slice(0, dot); + const fraction = dot < 0 ? "" : trimmed.slice(dot + 1); + const cents = Number(whole) * 100 + Number((fraction + "00").slice(0, 2)); + return Number.isSafeInteger(cents) && cents > 0; +} + +// Counts the submit actions inside the window the counting property compares +// over: from the last Home reading we took to this step, inclusive of this +// step's action. +// +// Counting ACTIONS rather than transactions is the whole point. A double tap is +// one action that commits two transactions, which is precisely the defect, so a +// rule phrased in transactions could not tell it apart from two healthy +// submits. +// +// A submit whose dispatch the runner could not confirm counts, because this +// number is an upper bound and the tap may well have landed. +export function countSubmitsInWindow(args: { + previousCount: number; + lastAction: ObservedAction | null; + amountText: string | undefined; + fresh: boolean; +}): { reported: number; next: number } { + const { previousCount, lastAction, amountText, fresh } = args; + const counts = isTxnSubmitTap(lastAction) && submitCouldCommit(amountText); + const reported = previousCount + (counts ? 1 : 0); + return { reported, next: fresh ? 0 : reported }; +} + +// Every accepted submit commits exactly one transaction, so over any window the +// number of transactions committed cannot exceed the number of submit actions +// taken. A double submit is one action committing two, which is the only way to +// break it. Refused submits commit nothing and are not counted, so the healthy +// case sits at or under the bound rather than at it. +// +// Only accounts present in BOTH readings are counted, and only upward movement. +// A card that could not be read drops out of the sum, which makes the result a +// LOWER BOUND on the transactions committed; a lower bound that already exceeds +// the submit count is still a real violation. Missing cards can cost a +// detection, they cannot manufacture one. +// +// Transactions are never deleted, so a per-account count only ever rises. +export function committedTransactionsExceedSubmits(args: { + countsBefore: Record | null; + countsAfter: Record | null; + submitsInWindow: number; +}): boolean { + const { countsBefore, countsAfter, submitsInWindow } = args; + if (countsBefore === null || countsAfter === null) return false; + if (!Number.isSafeInteger(submitsInWindow)) return false; + let committed = 0; + for (const accountId of Object.keys(countsAfter)) { + const before = countsBefore[accountId]; + const after = countsAfter[accountId]; + if (before === undefined || after === undefined) continue; + if (after > before) committed += after - before; + } + return committed > submitsInWindow; +} diff --git a/pkg/spec/test/folio-web-submit-counting.test.ts b/pkg/spec/test/folio-web-submit-counting.test.ts new file mode 100644 index 0000000..b91427b --- /dev/null +++ b/pkg/spec/test/folio-web-submit-counting.test.ts @@ -0,0 +1,363 @@ +import assert from "node:assert/strict"; +import { test } from "node:test"; + +import { + committedTransactionsExceedSubmits, + countSubmitsInWindow, + homeTxnCountsOf, + isTxnSubmitTap, + readHomeCards, + submitCouldCommit, +} from "../../../examples/folio-web/sanderling/predicates.ts"; +import type { + CardReading, + ObservedAction, +} from "../../../examples/folio-web/sanderling/predicates.ts"; + +const CHECKING = "acct-checking"; +const SAVINGS = "acct-savings"; + +const submitTap = (): ObservedAction => ({ kind: "Tap", on: "id:txn-submit", applied: true }); +const submitDoubleTap = (): ObservedAction => ({ + kind: "DoubleTap", + on: "id:txn-submit", + applied: true, +}); +const otherTap = (on: string): ObservedAction => ({ kind: "Tap", on, applied: true }); + +test("a submit tap and a submit double tap are both one submit action", () => { + assert.equal(isTxnSubmitTap(submitTap()), true); + assert.equal(isTxnSubmitTap(submitDoubleTap()), true); +}); + +test("taps on other controls are not submits", () => { + assert.equal(isTxnSubmitTap(otherTap("id:add-txn")), false); + assert.equal(isTxnSubmitTap(otherTap("id:add-account-submit")), false); + assert.equal(isTxnSubmitTap({ kind: "InputText", on: "id:txn-amount" }), false); + assert.equal(isTxnSubmitTap(null), false); +}); + +// The disabled button and parseCents (src/format.ts) between them refuse these, +// so they raise no bound. Of 108 add-transaction frames in the recalibration +// run, 65 carried an empty amount field. +test("amounts the app must have refused do not count as submits", () => { + assert.equal(submitCouldCommit(""), false); + assert.equal(submitCouldCommit(" "), false); + assert.equal(submitCouldCommit("0"), false); + assert.equal(submitCouldCommit("0.00"), false); + assert.equal(submitCouldCommit("-5"), false); + assert.equal(submitCouldCommit("abc"), false); + assert.equal(submitCouldCommit("1.234"), false); + assert.equal(submitCouldCommit("999999999999999999999"), false); +}); + +test("amounts the app accepts count as submits", () => { + assert.equal(submitCouldCommit("1"), true); + assert.equal(submitCouldCommit("12.34"), true); + assert.equal(submitCouldCommit("0.01"), true); + assert.equal(submitCouldCommit("99999"), true); + assert.equal(submitCouldCommit("1,234"), true); +}); + +// Off the transaction screen there is no field to read, and unknown counts: +// the bound has to hold every submit the window could contain. +test("an unreadable amount counts, because the tap may have committed", () => { + assert.equal(submitCouldCommit(undefined), true); +}); + +const before = { [CHECKING]: 3, [SAVINGS]: 1 }; + +test("healthy window: three submits, three transactions", () => { + assert.equal( + committedTransactionsExceedSubmits({ + countsBefore: before, + countsAfter: { [CHECKING]: 5, [SAVINGS]: 2 }, + submitsInWindow: 3, + }), + false, + ); +}); + +test("refused submits commit nothing, which is under the bound", () => { + assert.equal( + committedTransactionsExceedSubmits({ + countsBefore: before, + countsAfter: before, + submitsInWindow: 4, + }), + false, + ); +}); + +// The defect, stated directly: one action, two rows. +test("double submit: one action commits two transactions", () => { + assert.equal( + committedTransactionsExceedSubmits({ + countsBefore: before, + countsAfter: { [CHECKING]: 5, [SAVINGS]: 1 }, + submitsInWindow: 1, + }), + true, + ); +}); + +test("boundary: committed equal to the submit count is not a violation", () => { + assert.equal( + committedTransactionsExceedSubmits({ + countsBefore: before, + countsAfter: { [CHECKING]: 4, [SAVINGS]: 1 }, + submitsInWindow: 1, + }), + false, + ); + assert.equal( + committedTransactionsExceedSubmits({ + countsBefore: before, + countsAfter: { [CHECKING]: 4, [SAVINGS]: 2 }, + submitsInWindow: 1, + }), + true, + ); +}); + +// Counting actions against transactions rather than gating on a one-submit +// window is what lets a wide window stay evidence. +test("wide window: five submits committing six transactions still fires", () => { + assert.equal( + committedTransactionsExceedSubmits({ + countsBefore: before, + countsAfter: { [CHECKING]: 8, [SAVINGS]: 4 }, + submitsInWindow: 5, + }), + true, + ); +}); + +// A card that could not be read drops out of the sum, so the result is a lower +// bound on what committed. Losing a card can cost a detection; it must never +// manufacture one. +test("an account missing from either reading is not counted", () => { + assert.equal( + committedTransactionsExceedSubmits({ + countsBefore: { [CHECKING]: 3, [SAVINGS]: 1 }, + countsAfter: { [CHECKING]: 3 }, + submitsInWindow: 0, + }), + false, + ); + assert.equal( + committedTransactionsExceedSubmits({ + countsBefore: { [CHECKING]: 3 }, + countsAfter: { [CHECKING]: 3, [SAVINGS]: 9 }, + submitsInWindow: 0, + }), + false, + ); +}); + +test("an unknown reading on either side is not evidence", () => { + assert.equal( + committedTransactionsExceedSubmits({ + countsBefore: null, + countsAfter: { [CHECKING]: 99 }, + submitsInWindow: 0, + }), + false, + ); + assert.equal( + committedTransactionsExceedSubmits({ + countsBefore: { [CHECKING]: 0 }, + countsAfter: null, + submitsInWindow: 0, + }), + false, + ); +}); + +test("a home frame whose cards have not rendered is unknown, not zero accounts", () => { + assert.equal(homeTxnCountsOf([]), null); + assert.equal(homeTxnCountsOf([{ accountId: CHECKING, count: undefined }]), null); + assert.deepEqual(homeTxnCountsOf([{ accountId: CHECKING, count: 0 }]), { [CHECKING]: 0 }); +}); + +test("a card with no readable id is left out rather than guessed at", () => { + assert.deepEqual( + homeTxnCountsOf([ + { accountId: "", count: 4 }, + { accountId: SAVINGS, count: 1 }, + ]), + { [SAVINGS]: 1 }, + ); +}); + +// One step of a run, as the spec sees it: whether this frame is Home, the cards +// on it, the action that landed on it, and the amount field it shows. +interface Frame { + onHome: boolean; + cards?: readonly CardReading[]; + lastAction?: ObservedAction; + amountText?: string; +} + +// Replays frames through the same three predicates the spec wires together, +// returning the verdict of submitCommitsOneTransactionPerAction at each step. +function replay(frames: readonly Frame[]): boolean[] { + let carrier: Record | null = null; + let previousCounts: Record | null = null; + let submits = 0; + return frames.map((frame) => { + const reading = readHomeCards({ + onHome: frame.onHome, + reading: frame.cards ? homeTxnCountsOf(frame.cards) : null, + previousCarrier: carrier, + }); + carrier = reading.carrier; + const counted = countSubmitsInWindow({ + previousCount: submits, + lastAction: frame.lastAction ?? null, + amountText: frame.amountText, + fresh: reading.fresh, + }); + submits = counted.next; + const violated = committedTransactionsExceedSubmits({ + countsBefore: previousCounts, + countsAfter: reading.value, + submitsInWindow: counted.reported, + }); + previousCounts = reading.value; + return violated; + }); +} + +const home = (count: number): Frame => ({ + onHome: true, + cards: [{ accountId: CHECKING, count }], +}); + +// The walk the fuzzer takes: Home, into the account, into the form, type, tap +// submit, back out, Home again. The two compared readings are eight steps +// apart and the property has to stay quiet the whole way. +const walkToSubmit: readonly Frame[] = [ + home(3), + { onHome: false, lastAction: otherTap("desc:Checking, $0.00") }, + { onHome: false, lastAction: otherTap("id:add-txn") }, + { onHome: false, lastAction: { kind: "InputText", on: "id:txn-amount" }, amountText: "12.34" }, +]; + +test("one submit committing one transaction is quiet across an eight-step window", () => { + const verdicts = replay([ + ...walkToSubmit, + { onHome: false, lastAction: submitTap(), amountText: "12.34" }, + { onHome: false, lastAction: otherTap("id:back") }, + { onHome: false, lastAction: otherTap("id:back") }, + home(4), + ]); + assert.deepEqual(verdicts, [false, false, false, false, false, false, false, false]); +}); + +// The planted defect: the same walk, one double tap, two rows. +test("a double tap committing two transactions fires at the next home reading", () => { + const verdicts = replay([ + ...walkToSubmit, + { onHome: false, lastAction: submitDoubleTap(), amountText: "12.34" }, + { onHome: false, lastAction: otherTap("id:back") }, + { onHome: false, lastAction: otherTap("id:back") }, + home(5), + ]); + assert.deepEqual(verdicts, [false, false, false, false, false, false, false, true]); +}); + +// A window can hold several submits and several visits to the form. Every +// transaction is accounted for by an action, so the bound holds. +test("many submits across a wide window stay under the bound", () => { + const verdicts = replay([ + home(3), + { onHome: false, lastAction: otherTap("desc:Checking, $0.00") }, + { onHome: false, lastAction: otherTap("id:add-txn") }, + { onHome: false, lastAction: submitTap(), amountText: "1" }, + { onHome: false, lastAction: otherTap("id:add-txn") }, + { onHome: false, lastAction: submitTap(), amountText: "250" }, + { onHome: false, lastAction: otherTap("id:add-txn") }, + { onHome: false, lastAction: submitTap(), amountText: "99999" }, + { onHome: false, lastAction: otherTap("id:back") }, + home(6), + ]); + assert.equal(verdicts.some((violated) => violated), false); +}); + +// The same wide window with one of the three taps doubled. The rise of four +// against a budget of three is what convicts. +test("a double tap hidden among healthy submits still fires", () => { + const verdicts = replay([ + home(3), + { onHome: false, lastAction: otherTap("desc:Checking, $0.00") }, + { onHome: false, lastAction: otherTap("id:add-txn") }, + { onHome: false, lastAction: submitTap(), amountText: "1" }, + { onHome: false, lastAction: otherTap("id:add-txn") }, + { onHome: false, lastAction: submitDoubleTap(), amountText: "250" }, + { onHome: false, lastAction: otherTap("id:add-txn") }, + { onHome: false, lastAction: submitTap(), amountText: "99999" }, + { onHome: false, lastAction: otherTap("id:back") }, + home(7), + ]); + assert.deepEqual(verdicts[9], true); +}); + +// Submits the app refused raise no bound, which is what keeps the window tight +// enough to convict. The same trace with the three empty-field taps counted +// would acquit a double submit. +test("taps on the disabled submit button do not pad the budget", () => { + const padded: readonly Frame[] = [ + home(3), + { onHome: false, lastAction: otherTap("desc:Checking, $0.00") }, + { onHome: false, lastAction: otherTap("id:add-txn") }, + { onHome: false, lastAction: submitTap(), amountText: "" }, + { onHome: false, lastAction: submitTap(), amountText: "" }, + { onHome: false, lastAction: submitTap(), amountText: "" }, + { onHome: false, lastAction: { kind: "InputText", on: "id:txn-amount" }, amountText: "1" }, + { onHome: false, lastAction: submitDoubleTap(), amountText: "1" }, + { onHome: false, lastAction: otherTap("id:back") }, + home(5), + ]; + assert.deepEqual(replay(padded)[9], true); +}); + +// A fresh Home reading closes one window and opens the next, so a submit +// already accounted for cannot be spent twice. +test("the submit budget resets on every home reading", () => { + const verdicts = replay([ + home(3), + { onHome: false, lastAction: otherTap("id:add-txn") }, + { onHome: false, lastAction: submitTap(), amountText: "1" }, + home(4), + { onHome: false, lastAction: otherTap("id:add-txn") }, + { onHome: false, lastAction: submitDoubleTap(), amountText: "1" }, + home(6), + ]); + assert.deepEqual(verdicts, [false, false, false, false, false, false, true]); +}); + +// A submit that lands back on Home belongs to the window that ends there, so +// the rise it caused is covered rather than convicted. +test("a submit whose landing frame is home is counted in that window", () => { + const verdicts = replay([ + home(3), + { onHome: false, lastAction: otherTap("id:add-txn") }, + { onHome: true, cards: [{ accountId: CHECKING, count: 4 }], lastAction: submitTap() }, + ]); + assert.deepEqual(verdicts, [false, false, false]); +}); + +// Home renders its own node before its card list, and an empty list is +// UNKNOWN, not "no accounts". Writing it into the carrier is what would leave +// the next real reading comparing against nothing. +test("a home frame with no cards yet neither convicts nor closes the window", () => { + const verdicts = replay([ + home(3), + { onHome: false, lastAction: otherTap("id:add-txn") }, + { onHome: false, lastAction: submitDoubleTap(), amountText: "1" }, + { onHome: true, cards: [] }, + home(5), + ]); + assert.deepEqual(verdicts, [false, false, false, false, true]); +});