01floor never decreases
For every reachable state transition, reserves/totalSupply after is greater than or equal to before. This is the whole product; everything else is downstream of it.
Invariants
What is proven, and what is merely intended
The properties below are the ones the invariant suite fuzzes against: swaps in both directions, exact-in and exact-out, partial and near-total redemptions, direct donations, floor defences, and time advanced across the decay boundary, in any order and any quantity.
02the hook holds nothing
The hook is a pass-through with no balance of its own. Its balance of every currency is zero at the end of every run.
03reserves match accounting
The vault's internal _reserves never exceeds the reserve asset it actually holds. Accounting never reads a token balance; a direct donation only counts once sync() sweeps it in, and sync() can only increase.
04no supply without a burn
totalSupply is non-increasing after initialize. There is no mint path, and every route out of the vault burns a proportional or greater share of supply first.
Why redemption is accretive
Redeeming k tokens at a price p per token raises the floor whenever p ≤ floor. The exit rate is fixed at 95 %, so:
floor' = R(S - 0.95k) / (S(S - k)) > R/S = floor for 0 < k < S
The 5 % retained is not a fee taken by anyone. It stays in the vault and accrues to everyone who did not exit.
The pawl
When the pool price falls below the floor, anyone can call the guard, which spends reserves to buy tokens back and burn them until price returns to the floor. Buying below the floor and burning cannot lower reserves/supply, so the defence is floor-neutral by construction. Spend is capped per block, and the price comes from the pool, never from an oracle.
Status
Pre-deployment. No contracts are live on any network, mainnet or testnet. Nothing has been audited. The deployment order is: Sepolia with a mock reserve, then a mainnet-fork dry run of the exact deploy script, then audit, then the mainnet factory, then a first token launched by the team with real capital before any external launch is enabled.