refactor(folio): name the balance property for the bound it asserts

it stopped being an equality and became |delta| <= typed, so the old name
demanded more than the property does. renamed with the ci gate's
GATED_PROPERTIES in the same commit so the gate never sees a name it does
not know.
This commit is contained in:
pj committed 2026-08-15 23:04:15 +05:30
1 parent 6a7764eac7
commit 112d347432
8 files changed
+57 -57

No files matched your search

+1 -1
View File
@@ -32,7 +32,7 @@ SEED=9 MAX_STEPS=200 .github/scripts/folio-run.sh android
**web and ios expect the bug.** Folio double-submits a transaction when the
submit button is double-tapped, and two properties catch it:
`submitMovesBalanceByTypedAmount`, which demands the total balance move by
`submitMovesBalanceByAtMostTypedAmount`, which demands the total balance move by
exactly the amount typed, and `submitCommitsOneTransactionPerAction`, which
demands no more transactions committed over a window than there were submit
actions in it. A double tap is one action committing two transactions, so it
+2 -2
View File
@@ -27,7 +27,7 @@ You do not script the double tap. You state the invariant and let sanderling fin
The amount the user types must equal the amount the balance moves:
```ts
const submitMovesBalanceByTypedAmount = always(
const submitMovesBalanceByAtMostTypedAmount = always(
next(() => {
if (route.current !== "home") return true;
const action = lastAction.current;
@@ -179,7 +179,7 @@ That is the whole input. Three invariants, a way in, and a weighted sense of whe
## What the run does
sanderling launches Folio, logs in, and starts exploring. Most steps are unremarkable: open an account, add a transaction, watch the balance move by exactly what was typed, `submitMovesBalanceByTypedAmount` holds.
sanderling launches Folio, logs in, and starts exploring. Most steps are unremarkable: open an account, add a transaction, watch the balance move by exactly what was typed, `submitMovesBalanceByAtMostTypedAmount` holds.
Then a step lands two taps on submit before the first save settles. Two transactions post. The balance jumps by twice the typed amount. At that step the formula evaluates false and the run records a violation: the step, the screenshot, the offending action, and the residual formula that failed.