|
| 1 | +# Invariant Tests |
| 2 | + |
| 3 | +[TOC] |
| 4 | + |
| 5 | +This document describes the **stateful invariant suite** in [`test/invariant/`](../../test/invariant/) — what each invariant asserts, why it matters, how the handlers are built, and how the suite was verified to actually catch bugs. |
| 6 | + |
| 7 | +Invariant tests differ from the unit and fuzz tests elsewhere in `test/`: instead of exercising a fixed call sequence, Foundry drives a **handler** contract with long, randomly-ordered sequences of calls and re-checks every `invariant_*` function after each step. They are the right tool for the two **stateful (operation) rules**, whose storage evolves across calls. |
| 8 | + |
| 9 | +Validation rules are read-only and hold no per-transfer state, so they have nothing to conserve across a call sequence — they are covered by unit and fuzz tests instead. |
| 10 | + |
| 11 | +--- |
| 12 | + |
| 13 | +## 1. Running the suite |
| 14 | + |
| 15 | +```bash |
| 16 | +forge test --match-path "test/invariant/*" # the invariant suite only |
| 17 | +forge test --match-contract ConditionalTransferInvariants |
| 18 | +forge test --match-contract MintAllowanceInvariants |
| 19 | +forge test # everything, invariants included |
| 20 | +``` |
| 21 | + |
| 22 | +Configuration lives in `foundry.toml`: |
| 23 | + |
| 24 | +```toml |
| 25 | +[invariant] |
| 26 | +runs = 64 # independent random sequences |
| 27 | +depth = 128 # calls per sequence |
| 28 | +fail_on_revert = true # a reverting handler call fails the run |
| 29 | +``` |
| 30 | + |
| 31 | +`runs × depth` ⇒ **8 192 handler calls per invariant**. `fail_on_revert = true` is deliberate: the handlers are written to only ever make calls the rule will accept, so **any** revert means the handler (or the rule) is wrong, and we want to know. The suite currently reports **0 reverts**. |
| 32 | + |
| 33 | +--- |
| 34 | + |
| 35 | +## 2. Architecture — the handler pattern |
| 36 | + |
| 37 | +Foundry cannot usefully fuzz a rule directly: `approveTransfer` needs `OPERATOR_ROLE`, `transferred` may only be called by the bound entity, and random inputs would mostly revert. So each rule gets a **handler** that: |
| 38 | + |
| 39 | +1. **Holds the required roles and is itself the bound entity.** The handler is passed to `bindToken(address(handler))` and granted the operator role, so `msg.sender` inside the rule is the handler and every call is authorized. |
| 40 | +2. **Bounds the inputs.** A small actor set (3 addresses) and a small value range make the fuzzer *collide* on the same keys repeatedly, which is what actually exercises the accounting. |
| 41 | +3. **Skips calls that would revert** (e.g. cancelling a non-existent approval), so `fail_on_revert = true` stays meaningful. |
| 42 | +4. **Maintains ghost variables** — an independent, off-chain-style mirror of what the rule's state *should* be. The invariant then compares the rule against the ghost. |
| 43 | + |
| 44 | +``` |
| 45 | + ┌──────────────────────┐ randomly-ordered calls ┌──────────────────┐ |
| 46 | + │ Foundry invariant │ ──────────────────────────▶ │ Handler │ |
| 47 | + │ fuzzer │ │ (bound entity, │ |
| 48 | + └──────────────────────┘ │ role holder) │ |
| 49 | + │ └────────┬─────────┘ |
| 50 | + │ after every call real call │ ghost update |
| 51 | + ▼ ▼ |
| 52 | + ┌──────────────────────┐ ┌────────┐ ┌────────────┐ |
| 53 | + │ invariant_*() │ compares ─────────────▶│ Rule │ │ ghosts │ |
| 54 | + └──────────────────────┘ └────────┘ └────────────┘ |
| 55 | +``` |
| 56 | + |
| 57 | +`targetSelector` restricts the fuzzer to the handler's own action functions. Without it, Foundry would also call the public functions the handler inherits from forge-std's `Test`, wasting the call budget. |
| 58 | + |
| 59 | +| File | Role | |
| 60 | +|---|---| |
| 61 | +| [`test/invariant/ConditionalTransferHandler.sol`](../../test/invariant/ConditionalTransferHandler.sol) | Drives `RuleConditionalTransferLight`'s approval state machine | |
| 62 | +| [`test/invariant/MintAllowanceHandler.sol`](../../test/invariant/MintAllowanceHandler.sol) | Drives `RuleMintAllowance`'s quota accounting | |
| 63 | +| [`test/invariant/RuleInvariants.t.sol`](../../test/invariant/RuleInvariants.t.sol) | The two invariant test contracts and their `setUp` | |
| 64 | + |
| 65 | +--- |
| 66 | + |
| 67 | +## 3. The invariants |
| 68 | + |
| 69 | +### 3.1 `RuleConditionalTransferLight` — approval conservation |
| 70 | + |
| 71 | +Handler actions: `approve` · `cancel` · `execute` · `executeMintOrBurn`. |
| 72 | +Ghosts: `totalApproved`, `totalCancelled`, `totalExecuted`, `mintBurnCalls`. |
| 73 | + |
| 74 | +#### `invariant_approvalConservation` |
| 75 | + |
| 76 | +``` |
| 77 | +totalApproved − totalCancelled − totalExecuted == Σ approvalCounts |
| 78 | +``` |
| 79 | + |
| 80 | +Every approval ever recorded is, at any moment, in exactly one of three states: **still outstanding**, **cancelled**, or **consumed by a transfer**. The equality says approvals are neither **double-spent** (one `approveTransfer` consumed twice) nor **lost** (an approval that vanishes without being cancelled or used). |
| 81 | + |
| 82 | +The invariant additionally asserts `totalApproved >= totalCancelled + totalExecuted`, which fails loudly if the rule ever lets more approvals be consumed than were recorded — i.e. an underflow of `approvalCounts` (`INV-5`). |
| 83 | + |
| 84 | +#### `invariant_noApprovalExceedsTotalRecorded` |
| 85 | + |
| 86 | +``` |
| 87 | +Σ approvalCounts ≤ totalApproved |
| 88 | +``` |
| 89 | + |
| 90 | +A weaker but independent bound: no tuple can ever hold more outstanding approvals than were granted in total. It catches a class of bug (spurious increments) that conservation alone could mask if a matching spurious decrement existed. |
| 91 | + |
| 92 | +#### Emergent property — mint/burn never consume an approval |
| 93 | + |
| 94 | +The handler calls `executeMintOrBurn`, firing `transferred(address(0), to, v)` and `transferred(from, address(0), v)`, but **deliberately does not** count these in `totalExecuted`. If a mint or burn ever consumed an approval, `Σ approvalCounts` would drop while `totalExecuted` stayed put, and `invariant_approvalConservation` would break. |
| 95 | + |
| 96 | +So the mint/burn exemption is proved by the conservation invariant itself — no separate test needed. |
| 97 | + |
| 98 | +### 3.2 `RuleMintAllowance` — exact quota accounting |
| 99 | + |
| 100 | +Handler actions: `setAllowance` · `increase` · `decrease` · `mint` · `regularTransfer`. |
| 101 | +Ghosts: `ghostAllowance[minter]` (a full mirror), `totalCredited`, `totalMinted`. |
| 102 | + |
| 103 | +#### `invariant_allowanceMatchesGhost` |
| 104 | + |
| 105 | +``` |
| 106 | +for every minter m: rule.mintAllowance(m) == ghostAllowance[m] |
| 107 | +``` |
| 108 | + |
| 109 | +The strongest of the four. The handler recomputes the expected allowance independently after every accepted operation, so this asserts the rule's arithmetic is **exactly** right after *any* interleaving of set / increase / decrease / mint. It subsumes "never underflows" and "monotonically non-increasing across mints" (`INV-7`). |
| 110 | + |
| 111 | +#### `invariant_mintedNeverExceedsCredited` |
| 112 | + |
| 113 | +``` |
| 114 | +Σ minted ≤ Σ credited |
| 115 | +``` |
| 116 | + |
| 117 | +A cumulative safety bound independent of the mirror: across the whole run, minters can never mint more in total than was ever granted to them, regardless of how quotas were reset or adjusted along the way. |
| 118 | + |
| 119 | +#### Emergent property — non-mint transfers never touch a quota |
| 120 | + |
| 121 | +The handler calls `regularTransfer` (a `transferred(spender, from ≠ 0, to, v)` call) and **deliberately leaves the ghost unchanged**. If the rule ever deducted quota on a non-mint path, the mirror would diverge and `invariant_allowanceMatchesGhost` would fail. |
| 122 | + |
| 123 | +--- |
| 124 | + |
| 125 | +## 4. Negative controls — proving the suite can fail |
| 126 | + |
| 127 | +An invariant suite that cannot fail is worthless. Both invariants were **mutation-tested**: a real bug was injected into the rule, the suite was run, and the failure was confirmed. The mutations were then reverted. |
| 128 | + |
| 129 | +| Mutation | Injected bug | Result | |
| 130 | +|---|---|---| |
| 131 | +| `RuleConditionalTransferLightApprovalBase._transferred` — remove `approvalCounts[hash] = count - 1` | Approval **double-spend**: one approval can be consumed forever | ❌ `invariant_approvalConservation` fails: `approval accounting drifted: 0 != 1` | |
| 132 | +| `RuleMintAllowanceBase._transferredFrom` — `current - value` → `current - value + 1` | **Off-by-one** quota deduction: minters slowly gain free quota | ❌ `invariant_allowanceMatchesGhost` fails: `mint allowance drifted from expected: 1938542 != 1938541` | |
| 133 | + |
| 134 | +Re-run these yourself before trusting a change to either rule: if you mutate the accounting and the suite still passes, the suite has regressed. |
| 135 | + |
| 136 | +--- |
| 137 | + |
| 138 | +## 5. Coverage map |
| 139 | + |
| 140 | +Invariant IDs refer to [`THREAT_MODEL.md`](../../THREAT_MODEL.md) §8; verification status is tracked in [`RESULT.md`](../../RESULT.md). |
| 141 | + |
| 142 | +| Invariant (threat model) | Property | Covered by | |
| 143 | +|---|---|---| |
| 144 | +| `INV-5` | `approvalCounts` never underflows; one approval ⇒ one transfer | `invariant_approvalConservation`, `invariant_noApprovalExceedsTotalRecorded` | |
| 145 | +| `INV-7` | `mintAllowance` non-increasing across mints, never underflows, `Σ minted ≤ Σ granted` | `invariant_allowanceMatchesGhost`, `invariant_mintedNeverExceedsCredited` | |
| 146 | +| `INV-12` (partial) | Mint/burn handled explicitly, never falling into the transfer path | Emergent from both suites (see §3.1, §3.2) | |
| 147 | + |
| 148 | +**Not covered by invariants (by design):** |
| 149 | + |
| 150 | +- `INV-1`, `INV-2`, `INV-3`, `INV-9` — properties of *stateless* view functions; unit and fuzz tests are the right tool (`test/ThreatModel/ThreatModelTests.t.sol`). |
| 151 | +- `INV-6` (`_transferHash` injectivity) — a pure function; covered by `testFuzz_HASH1_ApprovalBucketsAreDistinct`. |
| 152 | +- `INV-4`, `INV-11` (access control) — covered by the per-rule access-control suites. |
| 153 | +- `INV-10` (ERC-2771 binding identity) — currently holds by static reasoning; a live regression test is the open item **I-10a** in [`RULE_IMPROVEMENT.md`](../../RULE_IMPROVEMENT.md). |
| 154 | + |
| 155 | +--- |
| 156 | + |
| 157 | +## 6. Adding a new invariant |
| 158 | + |
| 159 | +1. Add the action to the relevant handler. **Guard it** so it can only make calls the rule accepts (`fail_on_revert = true` will otherwise fail the run). |
| 160 | +2. Update the ghost state *after* the rule call, in the same function. If the rule call reverts, the whole handler call reverts and the ghost rolls back with it — which is what keeps the mirror consistent. |
| 161 | +3. Register the new selector in the `targetSelector(...)` array in `RuleInvariants.t.sol`, otherwise it will never be fuzzed. |
| 162 | +4. Add the `invariant_*` function, with a message argument on each assertion so a failure is legible. |
| 163 | +5. **Mutation-test it.** Inject the bug it is supposed to catch and confirm it fails. |
| 164 | + |
| 165 | +If you add a new stateful rule, it needs its own handler; validation rules do not. |
0 commit comments