Infrastructure · Verification
ClosureConservationCheck
Check that a conserved quantity balances over every holder, as an equality, not as a lower bound on the holders being watched
Definition
Mechanism
A test of a conserved quantity, as in Conservation, names the closure, meaning every holder of the quantity, including system accounts, fee pools, stock or funds in transit, and rounding remainders, and asserts that the opening balance plus inflows across the boundary equals the outflows plus the closing balance, within a stated rounding bound. A one-sided check, such as asserting that each user gets back at least what they put in, is reported as a bound, not as conservation. The equality constrains totals only: a transfer between two holders inside the closure passes it, even to the wrong holder. The check is itself tested by injecting an unbalanced change, such as a movement recorded on one side only or a balance left out of the sum, as in DetectorSelfTest.
Invariants
- The closure is named, and every holder in it is included in the check.
- Conservation is asserted as opening balance plus inflows equals outflows plus closing balance, within a stated rounding bound; a one-sided bound is reported as a bound.
- The check is shown to fail when an unbalanced change is injected.
Risks
Failure modes
Watched-holder bound
only the visible holders, such as customer accounts, are checked, so quantity created for them, or lost from a system account, goes unseen.
Open closure
a holder of the quantity, such as a fee pool or an account that collects rounding remainders, is left out.
Rounding slack
the tolerance is wide enough to absorb a real leak.
Misallocation read as conservation
a transfer to the wrong holder passes, since the equality constrains totals only.
Relationships
Builds on
References
Physics
An invariant quantity preserved under a closed system's transformations — a substrate law
Test the detectors that guard a process, so their silence is not mistaken for health
Nothing in this library builds on this pattern yet.