feat(folio-web): judge one commit per submit over a home-card window

Replaces totalBalanceMatchesAccounts and balanceMatchesTransactionDelta,
which compared two consecutive steps on one screen and so could not see a
double submission that lands across a navigation.

examples/folio-web/sanderling/spec.ts

@@ -3,6 +3,7 @@ import {
   Tap,
   actions,
   always,
+  doubleTaps,
   eventually,
   extract,
   llm,
@@ -13,11 +14,20 @@ import {
   waitOnce,
   weighted,
 } from "@sanderling/spec";
+import type { State } from "@sanderling/spec";
 import { noUncaughtExceptions } from "@sanderling/spec/defaults/properties";
+import {
+  committedTransactionsExceedSubmits,
+  countSubmitsInWindow,
+  homeTxnCountsOf,
+  readHomeCards,
+} from "./predicates";
 
 // Page-presence checks via stable element ids.
+const isHomeFrame = (s: State) => !!s.ax.find({ id: "add-account" });
+
 const onLoginPage = extract((s) => !!s.ax.find({ id: "email" })).named("onLoginPage");
-const onHomePage = extract((s) => !!s.ax.find({ id: "add-account" })).named("onHomePage");
+const onHomePage = extract(isHomeFrame).named("onHomePage");
 const onAddAccountPage = extract((s) => !!s.ax.find({ id: "account-name" })).named("onAddAccountPage");
 const onLedgerPage = extract((s) => !!s.ax.find({ id: "ledger" })).named("onLedgerPage");
 const onAddTxnPage = extract((s) => !!s.ax.find({ id: "txn-amount" })).named("onAddTxnPage");
@@ -42,10 +52,13 @@ function readCents(value: string | undefined): number {
   return isNaN(parsed) ? 0 : parsed;
 }
 
-const totalBalance = extract((s) => {
-  const el = s.ax.find({ id: "total-balance" });
-  return readCents(el?.attrs?.["data-cents"]);
-}).named("totalBalance");
+// A count of 0 is a real reading and a missing one is not, so this cannot fall
+// back to readCents.
+function readCount(value: string | undefined): number | undefined {
+  if (value === undefined) return undefined;
+  const parsed = parseInt(value, 10);
+  return Number.isSafeInteger(parsed) ? parsed : undefined;
+}
 
 // Account cards expose `data-account-id` + `data-balance` so the spec reads
 // structured data without parsing aria-label.
@@ -62,10 +75,46 @@ const ledgerTxnCount = extract((s) => {
   return readCents(el?.attrs?.["data-txn-count"]);
 }).named("ledgerTxnCount");
 
-const ledgerBalance = extract((s) => {
-  const el = s.ax.find({ id: "ledger-balance" });
-  return readCents(el?.attrs?.["data-cents"]);
-}).named("ledgerBalance");
+// Transactions committed per account, off Home's own cards, carried across
+// off-Home steps: the pair a property compares has to be two Home readings, not
+// a Home reading and whatever happened to be on screen. See readHomeCards.
+const homeCardReadings = (s: State) =>
+  s.ax.findAll({ "data-testid": "account-card" }).map((el) => ({
+    accountId: el.attrs?.["data-account-id"] ?? "",
+    count: readCount(el.attrs?.["data-txn-count"]),
+  }));
+
+let lastHomeTxnCounts: Record<string, number> | null = null;
+const homeTxnCounts = extract((s) => {
+  const reading = readHomeCards({
+    onHome: isHomeFrame(s),
+    reading: homeTxnCountsOf(homeCardReadings(s)),
+    previousCarrier: lastHomeTxnCounts,
+  });
+  lastHomeTxnCounts = reading.carrier;
+  return reading.value;
+}).named("homeTxnCounts");
+
+// Submit actions inside the window `homeTxnCounts.previous` and
+// `homeTxnCounts.current` span. Recomputed rather than shared with the
+// extractor above because extractor getters may not read one another; both
+// derive freshness from the same reading, so they reset on the same step.
+let submitsSinceHomeCards = 0;
+const submitsSinceCounts = extract((s) => {
+  const fresh = readHomeCards({
+    onHome: isHomeFrame(s),
+    reading: homeTxnCountsOf(homeCardReadings(s)),
+    previousCarrier: null,
+  }).fresh;
+  const counted = countSubmitsInWindow({
+    previousCount: submitsSinceHomeCards,
+    lastAction: s.lastAction,
+    amountText: s.ax.find({ id: "txn-amount" })?.attrs?.["value"],
+    fresh,
+  });
+  submitsSinceHomeCards = counted.next;
+  return counted.reported;
+}).named("submitsSinceCounts");
 
 // UI element handles.
 const emailField = extract((s) => s.ax.find({ id: "email" })).named("emailField");
@@ -97,25 +146,27 @@ const loggedOutReachesLogin = always(
   ),
 );
 
-const totalBalanceMatchesAccounts = always(() => {
-  if (!onHomePage.current) return true;
-  const cards = accountCards.current;
-  if (cards.length === 0) return true;
-  const sum = cards.reduce((acc, c) => acc + c.balance, 0);
-  return sum === totalBalance.current;
-});
-
-const balanceMatchesTransactionDelta = always(
-  now(() => onLedgerPage.current && ledgerTxnCount.current > 0).implies(
-    next(() => {
-      if (!onLedgerPage.current) return true;
-      const prevCount = ledgerTxnCount.previous ?? 0;
-      const curCount = ledgerTxnCount.current;
-      if (curCount !== prevCount + 1) return true;
-      const prevBal = ledgerBalance.previous ?? 0;
-      const curBal = ledgerBalance.current;
-      return curBal !== prevBal;
-    }),
+// One action commits at most one transaction, measured over the window between
+// two Home card readings rather than over a single step transition.
+//
+// The window is what makes it work. A commit always routes through
+// /transactions/new and pops back to the ledger it came from, so the fuzzer can
+// add transactions all day without Home being redrawn: any rule phrased over
+// two consecutive steps on one screen never gets a pair to judge. This one
+// stays sound however wide the gap between two Home readings gets, because the
+// submit count is taken over exactly the same interval as the two counts it
+// compares.
+//
+// `next` because the first step of a run has no previous reading to compare
+// against.
+const submitCommitsOneTransactionPerAction = always(
+  next(
+    () =>
+      !committedTransactionsExceedSubmits({
+        countsBefore: homeTxnCounts.previous ?? null,
+        countsAfter: homeTxnCounts.current,
+        submitsInWindow: submitsSinceCounts.current,
+      }),
   ),
 );
 
@@ -136,8 +187,7 @@ const someTransactionExists = eventually(
 export const properties = {
   loggedInLeavesLogin,
   loggedOutReachesLogin,
-  totalBalanceMatchesAccounts,
-  balanceMatchesTransactionDelta,
+  submitCommitsOneTransactionPerAction,
   loginReachable,
   accountCreationReachable,
   someTransactionExists,
@@ -276,6 +326,10 @@ const logoutAction = actions(() => {
 // so the seeded picker draws from the edge-case corpus and the model writes its
 // own text. It holds the 8 weight those two leaves shared, so every other
 // branch keeps the share it had.
+//
+// `doubleTaps` gets explicit weight because rapid double-submission is a
+// failure mode these forms must be idempotent under, and no other branch
+// provokes it: every authored leaf taps once.
 export const actionsRoot = weighted(
   [30, loginHelper],
   [2, adversarialLogin],
@@ -292,6 +346,7 @@ export const actionsRoot = weighted(
   [1, logoutAction],
   [4, taps],
   [8, typing],
+  [5, doubleTaps],
   [2, waitOnce],
 );