OIP-6 Invariant testing for OUSD

It would be good to have through invariant testing for the OUSD token contract.

Here's an initial draft.

Transfers

• The receiving account's balance after a transfer must increase by exactly the amount transferred. (We may not be able to do this)
• The sending account's balance after a transfer must decrease by exactly the amount transferred. (We may not be able to do this)
• The receiving account's balance after a transfer must increase by at least the amount transferred.
• The receiving account's balance after a transfer must not increase by more than the amount transferred + rounding error.
• The sending account's balance after a transfer must decrease by no more than amount transferred.
• The sending account's balance after a transfer must decrease by no less than the amount transferred minus rounding error.
• An account should be always to successfully call transfer with its balance.
• An account never be able to successfully call transfer for an amount greater than their balance.
• A transfer to the same account should not change that account's balance
• Outside of an allowance, sender cannot decrease other users’ balances
• Transfers to the zero account revert

Change Supply

• After a changeSupply, the total supply should exactly match the target total supply. (This is needed to ensure successive rebases are correct).
• The total supply may be greater than the sum of account balances. (The difference will go into future rebases)
• Non-rebasing supply should not be larger than total supply
• global rebasingCreditsPerToken should never not increase

Accounting

• Account balance should remain the same after opting in (May not be able to meet)
• Account balance should not increase when opting in. (Ok to lose rounding funds doing this)
• Account balance should remain the same after opting out
• Account balance should remain the same when a smart contract auto converts
• After rebasing change, total Supply should remain the same
• Non-rebasing credits should be correct (needs clear definition)
• An account balance should not be larger than total supply
• An account balance should not be larger than non-rebasing supply
• An accounts credits / credits per token should not be greater than the total supply

Balance Of

• The balanceOf function should never revert
• The rebasing credits per token ratio must greater than zero

Vault Connection Mint/Burn

• Minting 0 tokens should not affect account balance
• Minting tokens should always increase the account balance by at least amount
• Minting tokens should not increase the account balance by more than rounding error above amount
• Burning 0 tokens should not affect account balance
• A burn of an account balance must result in a zero balance
• You should always be able to burn an account's balance
• Burning tokens must decrease the balance by at least amount.

Misc

• An account should not be able to increase their balance more than rounding error outside of transfers in or rebasing.

Start by locating the OUSD token contract and the listed entry points: transfer, changeSupply, opt-in/out, balanceOf, and vault mint/burn operations. Turn the draft requirements into executable invariants, resolving the items marked as uncertain or needing definitions, and finish when the invariant suite covers the agreed behaviors.