docs(skills): both shipped balance forms are bounds now

This commit is contained in:
pj committed 2026-08-16 01:06:49 +05:30
1 parent 4d14e9ca54
commit ef7466e61e
1 file changed
+36 -33
+36 -33
View File
@@ -106,34 +106,34 @@ climbed), state a bound on it rather than a prediction of it.
**Prefer an upper bound to an equality.** This is the single most valuable **Prefer an upper bound to an equality.** This is the single most valuable
sentence in this file. sentence in this file.
`examples/folio/sanderling/predicates.ts` states one rule about one app both Folio shipped one of these both ways and the equality lost, so the two are worth
ways, so the two are worth reading side by side. Each line is the last line of reading side by side. Each line is the last line of a predicate in
its predicate, after the guards, at a step where exactly one submit sits in the `examples/folio/sanderling/predicates.ts`, after the guards, at a step where
window: exactly one submit sits in the window:
```ts ```ts
// sound, committedAmountExceedsOneSubmit: the violation is moving by MORE // what folio's total-balance property demanded, until 6e8e6d5
// than the one submit in this window could account for
Math.abs(currAccountBalance - prevAccountBalance) > typedAmount
// tempting, submitChangesBalanceByTypedAmount: it moved by exactly what I typed
Math.abs(currTotalBalance - prevTotalBalance) === typedAmount Math.abs(currTotalBalance - prevTotalBalance) === typedAmount
// what it demands now
Math.abs(currTotalBalance - prevTotalBalance) <= typedAmount
// and the same bound stated as the violation, over the account's own balance
Math.abs(currAccountBalance - prevAccountBalance) > typedAmount
``` ```
Both catch the bug, because a double submit moves the balance by twice the typed All three catch the bug, because a double submit moves the balance by twice the
amount. Only the second also convicts an app that behaved. A balance that has typed amount and twice x exceeds x. Only the equality also convicts an app that
not moved is a commit still in flight (folio's `createTransaction` runs in a behaved. A balance that has not moved is a commit still in flight (folio's
coroutine), a submit the app rejected, or a tap that never landed, and none of `createTransaction` runs in a coroutine, and Home's total re-renders on the
those is evidence of anything. store's own schedule), a submit the app rejected, or a tap that never landed,
and none of those is evidence of anything.
The asymmetry is the point. Moving by more than one submit's worth is not The asymmetry is the point. Moving by more than one submit's worth is not
something a correct app can do, so the bound needs no case for any of the three. something a correct app can do, so the bound needs no case for any of the three.
The equality needs a case for each, and every one you forget is a false The equality needs a case for each, and every one you forget is a false
conviction. Compare the two guard stacks and the price is exactly legible: the conviction. Two of those cases are facts the runner cannot promise you (see
equality declines on `confirmedApplied` and on `acrossRelaunch`, and the bound below): an action it could not confirm was applied, and an action it had to
carries neither, because a submit that may not have landed and a restart that relaunch the app after. Both leave the balance under the bound and both break an
may have eaten the commit both leave the balance under the bound anyway. Those equality, so a bound counts them and an equality has to decline on them.
are the two facts the runner cannot promise (see below), and needing to guard
against both is a cost of the equality, not of the app.
You do give something up, so make the trade deliberately. A bound cannot see a You do give something up, so make the trade deliberately. A bound cannot see a
balance that moved by *less* than the typed amount, and for a ledger that is a balance that moved by *less* than the typed amount, and for a ledger that is a
@@ -344,8 +344,10 @@ without throwing once.
**Absence is unknown, never a default.** Extractors return null when the element **Absence is unknown, never a default.** Extractors return null when the element
is not there, and a property handed null declines. `0`, `""` and `[]` are the is not there, and a property handed null declines. `0`, `""` and `[]` are the
values that turn a property into one that fires on healthy runs: folio's values that turn a property into one that fires on healthy runs: folio's
balances once parsed as `0` on web, so the check became `|0 - 0| === typed` and balances once parsed as `0` on web, so the check, an equality at the time,
was false at every healthy submit. An empty list has the same problem in the became `|0 - 0| === typed` and was false at every healthy submit. Under today's
bound the same `0` reads as `|0 - 0| <= typed` and passes at every submit
instead, which is the same defect wearing green. An empty list has the same problem in the
other direction, and it is worse because it looks reasonable. Android renders other direction, and it is worse because it looks reasonable. Android renders
Home's own node a frame or two before its list, so `findAll` over the cards Home's own node a frame or two before its list, so `findAll` over the cards
comes back empty while the screen already claims to be Home. That is unknown, comes back empty while the screen already claims to be Home. That is unknown,
@@ -388,23 +390,24 @@ of its states is unsound:
One rule covers the last two, and it is the rule that decides shape 2 for you. One rule covers the last two, and it is the rule that decides shape 2 for you.
An action the runner cannot fully vouch for **still counts toward a bound on An action the runner cannot fully vouch for **still counts toward a bound on
what the app could have done**, and it **never licenses attributing an effect to what the app could have done**, and it **never licenses attributing an effect to
it**. So a bound counts it and an equality has to decline on it. That is why it**. So a bound counts it and a property demanding an effect has to decline on
`committedAmountExceedsOneSubmit` needs no `confirmedApplied` guard and no it. That is why `committedAmountExceedsOneSubmit`, which only bounds how far the
`acrossRelaunch` guard while `submitChangesBalanceByTypedAmount` needs both: a balance could have moved, needs no `confirmedApplied` guard and no
property demanding the effect of an action that may never have run, or that a `acrossRelaunch` guard, while `createdAccountHasNonZeroBalance`, which demands
restart may have swallowed, convicts the app of the runner's own uncertainty. that a card appear, needs both. Demanding the effect of an action that may never
have run, or that a restart may have swallowed, convicts the app of the runner's
own uncertainty.
`relaunched` is the same shape of fact as `applied`, applied to app state rather `relaunched` is the same shape of fact as `applied`, applied to app state rather
than to dispatch. The action itself did happen. What nobody can promise across than to dispatch. The action itself did happen. What nobody can promise across
it is that the process ran continuously, that the commit survived, or that the it is that the process ran continuously, that the commit survived, or that the
screen is showing the same slice of the same list it was. So a property assuming screen is showing the same slice of the same list it was. So a property assuming
continuous state declines, via `acrossRelaunch(lastAction)`, and folio uses it continuous state declines, via `acrossRelaunch(lastAction)`.
in three places: `createdAccountHasNonZeroBalance` declines because Home redraws `createdAccountHasNonZeroBalance` declines because Home redraws from the top and
from the top and the card carrying the typed name may be an older account laid the card carrying the typed name may be an older account laid out where the new
out where the new one used to be, the equality property declines because it one used to be. `countSubmitsInWindow` uses the same call to **stop trusting its
demands an effect, and `countSubmitsInWindow` uses it to **stop trusting its own own refusal evidence**, since a relaunch is the one thing that can put a form
refusal evidence**, since a relaunch is the one thing that can put a form state state on screen other than the one the tap read.
on screen other than the one the tap read.
Both fields are `true | null` rather than booleans, and that is deliberate: only Both fields are `true | null` rather than booleans, and that is deliberate: only
the positive report is a fact the runner can vouch for, so `null` is "not the positive report is a fact the runner can vouch for, so `null` is "not