feat(folio-web): predicates for counting commits against submit actions

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<T> {
+  value: T | null;
+  carrier: T | null;
+  fresh: boolean;
+}
+
+export function readHomeCards<T>(args: {
+  onHome: boolean;
+  reading: T | null;
+  previousCarrier: T | null;
+}): HomeReading<T> {
+  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<string, number> | null {
+  const counts: Record<string, number> = {};
+  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<string, number> | null;
+  countsAfter: Record<string, number> | 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;
+}

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<string, number> | null = null;
+  let previousCounts: Record<string, number> | 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]);
+});