Merge branch 'conjunct-that-cannot-fire' into correctness-and-spec-skills

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;

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(
     () =>

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 },

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,
   );

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,