docs: a bound still needs the relaunch guard, and eventually does convict

internal/ltl/formula.go

@@ -84,8 +84,9 @@ type NextFormula struct {
 }
 
 // EventuallyFormula obliges its inner formula to hold at some step within the
-// given bound. An unbounded eventually never triggers a violation within a
+// given bound. An unbounded eventually that never fires is violated when the
-// finite run.
+// run ends, with the reason "eventually never satisfied", so an eventually over
+// a state the run may not reach is red on every run that does not reach it.
 //
 // When Duration is non-zero and Deadline is the zero time, the evaluator
 // resolves the absolute deadline on first reduction using the observation

skills/sanderling-property-patterns/SKILL.md

@@ -393,11 +393,19 @@ 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
 it**. So a bound counts it and a property demanding an effect has to decline on
 it. That is why `committedAmountExceedsOneSubmit`, which only bounds how far the
-balance could have moved, needs no `confirmedApplied` guard and no
+balance could have moved, needs no `confirmedApplied` guard, while
-`acrossRelaunch` guard, while `createdAccountHasNonZeroBalance`, which demands
+`createdAccountHasNonZeroBalance`, which demands that a card appear, does.
-that a card appear, needs both. Demanding the effect of an action that may never
+Demanding the effect of an action that may never have run convicts the app of
-have run, or that a restart may have swallowed, convicts the app of the runner's
+the runner's own uncertainty.
-own uncertainty.
+
+A relaunch is not symmetric with that, and folio is a good illustration of why a
+bound can still need the guard. `SqlLedgerStore` starts its flows on
+`stateIn(Eagerly, emptyList())` and Home composes the total unconditionally, so
+a restarted app draws `$0.00` until sqlite answers. That is not a commit the
+restart swallowed, it is a reading of the wrong process, and its size is
+arbitrary. A bound cannot absorb it, so the balance properties keep
+`acrossRelaunch` even though they are bounds. Work out what a restart does to
+the reading, not just to the effect.
 
 `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