Adding Invariants¶
Process¶
- define invariant in plain language and formal condition.
- map invariant to concrete state variables and transitions.
- add enforcement checks in conformance and/or formal tools.
- add negative test proving invariant catches violation.
Candidate Invariants¶
- user reward claims never exceed user reward bucket
- principal claim never exceeds covered principal remainder
- receipt id cannot be processed twice for same scope
- stale/quarantined observations cannot enable running claims
High-Value Invariants¶
Start with properties that protect funds or governance: no consumed intent can be reused, no unregistered vault can pass deposit readiness, no queued upgrade can execute before readyAt, no stale observation can enable normal claims, no receipt source id can be counted twice, and settlement must preserve principal-first ordering.
Evidence Standard¶
An invariant is not covered until the test command, seed or proof configuration, source commit, and output are archived. Link the evidence back to the handbook page that states the invariant.
Evidence Model¶
| Field | Requirement |
|---|---|
| Purpose | procedure for adding new properties safely. |
| Expected location | test and spec directories. |
| Current local evidence status | Evidence required unless the named artifact is present in this repository or the Solidity source snapshot and has been inspected in the current run. |
| What it proves | review discipline for new invariants. |
| What it does not prove | that old invariants are sufficient after source changes. |
| How to regenerate | Run the documented tool from a clean environment, archive command, commit/source hash, config, stdout/stderr, and result files. |
| Production requirement | Results must be tied to the exact source manifest lock, compiler version, dependency lock, and deployment artifact under review. |
| Owner responsible | Protocol engineering owns source/test correctness; security review owns independent challenge; governance owns accepting residual risk. |
| Failure meaning | A failure blocks release, launch, upgrade, or operation until root cause is fixed or explicitly accepted with documented risk. |
Review Notes¶
Do not write “pass” for Invariant additions without current evidence. If evidence is missing, stale, or tied to a different source snapshot, write Evidence required and keep the gap visible in the release or operations checklist.