seven statements that hold after every transaction. each is checkable from public state.
| invariant | check |
|---|---|
| book after any mint or burn is greater than or equal to book before it | read book before and after any tx in the activity table |
| totalSupply <= q(E) with equality except for rounding down | compare totalSupply to q(position) computed here |
| totalSupply < K always | compare totalSupply to K |
| usedInBlock <= budget for the current block | read usedInBlock and budget from state |
| E is monotone non decreasing across the life of the contract | position in consecutive state reads never decreases |
| the contract's eth balance equals cistern exactly | compare the contract's eth balance on the explorer to cistern from state |
| no address holds any special role | search the verified source for owner, selfdestruct, delegatecall |