Reference
Trading invariants
These conditions are required at every successful external state transition. Reverting calls leave the prior state unchanged. Protocol-wide invariants are catalogued separately in Protocol invariants.
Pair custody
- The pair's Yes balance is greater than or equal to its stored Yes reserve.
- The pair's No balance is greater than or equal to its stored No reserve.
- The pair's Invalid balance is exactly zero.
- An LP withdrawal cannot claim more Yes or No shares than the pair owns. Withdrawal amounts are proportional to synchronized reserves and the liquidity burned.
Unsolicited Yes or No donations can make a balance greater than its stored reserve. Before reserve-dependent mutations, the pair synchronizes stored reserves upward to those effective balances. Invalid shares are never a trading asset and cannot be donated through an accepted ERC-1155 callback.
Router custody
Every successful router operation ends with the same Invalid, Yes, and No balances with which that operation began. This deliberately preserves any pre-existing balances while preventing the operation from accumulating new share residue.
Swaps
- For every successful exact-input or exact-output swap,
k_after ≥ k_before, wherekis the synchronized effective Yes reserve multiplied by the synchronized effective No reserve. - An exact-output swap delivers exactly the requested output amount.
- An exact-output swap never charges more than the caller's
maxAmountIn.
The product comparison starts from effective reserves so a donation cannot be mistaken for swap-created growth.
Lifecycle
- Once the question has ended, the question has resolved, or the universe has forked, initialization, liquidity addition, and both swap forms revert permanently.
- While fork continuation is pending or the SecurityPool is not operational, the same operations also revert for as long as that state lasts.
- Proportional liquidity removal has no lifecycle guard, so LP tokens never become trapped.