Invariants
| Invariant | Statement |
|---|---|
| No Dual State | At the boundary of the auction window — T−1s, T, T+1s — the contract must be in exactly one of open or closing. Never both. |
| Cap Enforcement | e_i ≤ A_max for every address, in every round, with no implementation path that allocates above the cap even transiently. |
| Fill Conservation | Σ e_i = V_target and Σ token_i = tokenPool exactly, after largest-remainder correction. |
| Non-Negative Refund | refund_i = z_i − e_i ≥ 0 for every address, always. |
| Entry-Conversion Integrity | A failed conversion into USDG at deposit time must not be credited to the user's z_i. The deposit simply does not enter the auction. |
| Proof Integrity | A tampered proof, a proof against a stale root, a replayed claim, and a re-entrant claim call must all fail deterministically. |
| Failure Atomicity | MONEY and SEATS failures both resolve to e_i = 0 for all i with no LP creation. There is no partial-success state between "cleared" and "fully refunded." |
Regression Requirements
Beyond the invariants, the implementation must pass a randomized fuzz suite:
| Runs | 10,000+ |
randomized |
| Addresses per run | 1 – 120 |
synthetic |
| Deposit sizes | random |
across the full range |
| Tolerated failures | 0 |
exactly zero, not "within tolerance" |
The counted incidence of each of the following must be exactly zero: negative refunds, over-cap allocations, over-principal allocations, and any conservation violation.
Why zero, not a tolerance
Conservation in this mechanism is an integer identity, not a floating-point approximation. A single unit of drift means the largest-remainder procedure is wrong, and drift compounds across rounds.