From 3d966bbaec1d6d7f3bc195442bca95509e5043bc Mon Sep 17 00:00:00 2001 From: Roy-Certora Date: Wed, 18 Dec 2024 09:41:03 +0200 Subject: [PATCH 1/3] Add OUSD spec files and running scripts --- .gitignore | 3 + certora/confs/OUSD_accounting.conf | 16 ++ certora/confs/OUSD_balances.conf | 16 ++ certora/confs/OUSD_other.conf | 16 ++ certora/confs/OUSD_sumOfBalances.conf | 18 ++ certora/run.sh | 3 + certora/specs/OUSD/AccountInvariants.spec | 158 +++++++++++ certora/specs/OUSD/BalanceInvariants.spec | 183 +++++++++++++ certora/specs/OUSD/OtherInvariants.spec | 306 ++++++++++++++++++++++ certora/specs/OUSD/SumOfBalances.spec | 195 ++++++++++++++ certora/specs/OUSD/common.spec | 92 +++++++ 11 files changed, 1006 insertions(+) create mode 100644 certora/confs/OUSD_accounting.conf create mode 100644 certora/confs/OUSD_balances.conf create mode 100644 certora/confs/OUSD_other.conf create mode 100644 certora/confs/OUSD_sumOfBalances.conf create mode 100644 certora/run.sh create mode 100644 certora/specs/OUSD/AccountInvariants.spec create mode 100644 certora/specs/OUSD/BalanceInvariants.spec create mode 100644 certora/specs/OUSD/OtherInvariants.spec create mode 100644 certora/specs/OUSD/SumOfBalances.spec create mode 100644 certora/specs/OUSD/common.spec diff --git a/.gitignore b/.gitignore index bfc271b61d..05a805c264 100644 --- a/.gitignore +++ b/.gitignore @@ -84,3 +84,6 @@ fork-coverage unit-coverage .VSCodeCounter + +# Certora # +.certora_internal diff --git a/certora/confs/OUSD_accounting.conf b/certora/confs/OUSD_accounting.conf new file mode 100644 index 0000000000..7bdc7cf7ed --- /dev/null +++ b/certora/confs/OUSD_accounting.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "contracts/contracts/token/OUSD.sol" + ], + "msg": "OUSD Accounting invariants", + "packages": [ + "@openzeppelin/contracts=contracts/lib/openzeppelin/contracts", + ], + "process": "emv", + "prover_args": [ + + ], + "solc": "solc8.28", + "verify": "OUSD:certora/specs/OUSD/AccountInvariants.spec", + "server": "production", +} \ No newline at end of file diff --git a/certora/confs/OUSD_balances.conf b/certora/confs/OUSD_balances.conf new file mode 100644 index 0000000000..74c3b610c0 --- /dev/null +++ b/certora/confs/OUSD_balances.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "contracts/contracts/token/OUSD.sol" + ], + "msg": "OUSD Balances invariants", + "packages": [ + "@openzeppelin/contracts=contracts/lib/openzeppelin/contracts", + ], + "process": "emv", + "prover_args": [ + + ], + "solc": "solc8.28", + "verify": "OUSD:certora/specs/OUSD/BalanceInvariants.spec", + "server": "production" +} \ No newline at end of file diff --git a/certora/confs/OUSD_other.conf b/certora/confs/OUSD_other.conf new file mode 100644 index 0000000000..8abded891d --- /dev/null +++ b/certora/confs/OUSD_other.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "contracts/contracts/token/OUSD.sol" + ], + "msg": "OUSD other invariants", + "packages": [ + "@openzeppelin/contracts=contracts/lib/openzeppelin/contracts", + ], + "process": "emv", + "prover_args": [ + + ], + "solc": "solc8.28", + "verify": "OUSD:certora/specs/OUSD/OtherInvariants.spec", + "server": "production" +} \ No newline at end of file diff --git a/certora/confs/OUSD_sumOfBalances.conf b/certora/confs/OUSD_sumOfBalances.conf new file mode 100644 index 0000000000..d0bc8568f4 --- /dev/null +++ b/certora/confs/OUSD_sumOfBalances.conf @@ -0,0 +1,18 @@ +{ + "files": [ + "contracts/contracts/token/OUSD.sol" + ], + "msg": "OUSD Sum of balances rules", + "packages": [ + "@openzeppelin/contracts=contracts/lib/openzeppelin/contracts", + ], + "process": "emv", + "prover_args": [ + "-mediumTimeout 40", + ], + "multi_assert_check":true, + "smt_timeout":"1000", + "solc": "solc8.28", + "verify": "OUSD:certora/specs/OUSD/SumOfBalances.spec", + "server": "production" +} \ No newline at end of file diff --git a/certora/run.sh b/certora/run.sh new file mode 100644 index 0000000000..6c52eab517 --- /dev/null +++ b/certora/run.sh @@ -0,0 +1,3 @@ +certoraRun certora/confs/OUSD_balances.conf +certoraRun certora/confs/OUSD_other.conf +certoraRun certora/confs/OUSD_sumOfBalances.conf diff --git a/certora/specs/OUSD/AccountInvariants.spec b/certora/specs/OUSD/AccountInvariants.spec new file mode 100644 index 0000000000..1de654903e --- /dev/null +++ b/certora/specs/OUSD/AccountInvariants.spec @@ -0,0 +1,158 @@ +import "./common.spec"; + +function allAccountValidState() { + requireInvariant DelegationAccountsCorrelation(); + requireInvariant DelegationValidRebaseState(); + requireInvariant stdNonRebasingDoesntYield(); + requireInvariant alternativeCreditsPerTokenIsOneOrZeroOnly(); + requireInvariant yieldDelegationSourceHasNonZeroYeildTo(); + requireInvariant yieldDelegationTargetHasNonZeroYeildFrom(); + requireInvariant yieldToOfZeroIsZero(); + requireInvariant yieldFromOfZeroIsZero(); + requireInvariant cantYieldToSelf(); + requireInvariant cantYieldFromSelf(); + requireInvariant zeroAlternativeCreditsPerTokenStates(); + requireInvariant nonZeroAlternativeCreditsPerTokenStates(); +} + +/// @title Any non zero valued YieldTo points to an account that has a YieldFrom pointing back to the starting account and vice versa. +/// @property Account Invariants +invariant DelegationAccountsCorrelation() + forall address account. + (OUSD.yieldTo[account] != 0 => (OUSD.yieldFrom[OUSD.yieldTo[account]] == account)) + && + (OUSD.yieldFrom[account] != 0 => (OUSD.yieldTo[OUSD.yieldFrom[account]] == account)) + { + preserved with (env e) { + requireInvariant DelegationValidRebaseState(); + requireInvariant yieldToOfZeroIsZero(); + requireInvariant yieldFromOfZeroIsZero(); + } + } + +/// @title Any non zero valued YieldTo points to an account Iff that account is in YieldDelegationSource state and +/// Any non zero valued YieldFrom points to an account Iff that account is in YieldDelegationTarget state. +/// @property Account Invariants +invariant DelegationValidRebaseState() + forall address account. + (OUSD.yieldTo[account] != 0 <=> OUSD.rebaseState[account] == YieldDelegationSource()) + && + (OUSD.yieldFrom[account] != 0 <=> OUSD.rebaseState[account] == YieldDelegationTarget()) + { + preserved with (env e) { + requireInvariant DelegationAccountsCorrelation(); + requireInvariant yieldToOfZeroIsZero(); + requireInvariant yieldFromOfZeroIsZero(); + } + } + +/// @title Any account with a zero value in alternativeCreditsPerToken has a rebaseState that is one of (NotSet, StdRebasing, or YieldDelegationTarget) +/// @property Account Invariants +invariant zeroAlternativeCreditsPerTokenStates() + forall address account . OUSD.alternativeCreditsPerToken[account] == 0 <=> (OUSD.rebaseState[account] == NotSet() || + OUSD.rebaseState[account] == StdRebasing() || + OUSD.rebaseState[account] == YieldDelegationTarget()) + { + preserved { + requireInvariant yieldToOfZeroIsZero(); + requireInvariant yieldFromOfZeroIsZero(); + requireInvariant DelegationAccountsCorrelation(); + requireInvariant DelegationValidRebaseState(); + } + } + +/// @title Any account with value of 1e18 in alternativeCreditsPerToken has a rebaseState that is one of (StdNonRebasing, YieldDelegationSource) +/// @property Account Invariants +invariant nonZeroAlternativeCreditsPerTokenStates() + forall address account . OUSD.alternativeCreditsPerToken[account] != 0 <=> (OUSD.rebaseState[account] == StdNonRebasing() || + OUSD.rebaseState[account] == YieldDelegationSource()) + { + preserved undelegateYield(address _account) with (env e) { + requireInvariant yieldToOfZeroIsZero(); + requireInvariant yieldFromOfZeroIsZero(); + requireInvariant DelegationAccountsCorrelation(); + requireInvariant DelegationValidRebaseState(); + } + } + +/// @title The result of balanceOf of any account in StdNonRebasing state equals the account's credit-balance. +/// @property Balance Invariants +invariant stdNonRebasingBalanceEqCreditBalances(address account) + OUSD.rebaseState[account] == StdNonRebasing() => OUSD.balanceOf(account) == OUSD.creditBalances[account] + { + preserved { + requireInvariant yieldToOfZeroIsZero(); + requireInvariant yieldFromOfZeroIsZero(); + requireInvariant DelegationAccountsCorrelation(); + requireInvariant DelegationValidRebaseState(); + requireInvariant nonZeroAlternativeCreditsPerTokenStates(); + requireInvariant stdNonRebasingDoesntYield(); + requireInvariant alternativeCreditsPerTokenIsOneOrZeroOnly(); + } + } + +/// @title Any account in StdNonRebasing state doesn't yield to no account. +/// @property Account Invariants +invariant stdNonRebasingDoesntYield() + forall address account . OUSD.rebaseState[account] == StdNonRebasing() => OUSD.yieldTo[account] == 0 + { + preserved { + requireInvariant yieldToOfZeroIsZero(); + requireInvariant yieldFromOfZeroIsZero(); + requireInvariant DelegationAccountsCorrelation(); + requireInvariant DelegationValidRebaseState(); + } + } + +/// @title alternativeCreditsPerToken can only be set to 0 or 1e18, no other values +/// @property Account Invariants +invariant alternativeCreditsPerTokenIsOneOrZeroOnly() + forall address account . OUSD.alternativeCreditsPerToken[account] == 0 || OUSD.alternativeCreditsPerToken[account] == e18(); + +/// @title Any account with rebaseState = YieldDelegationSource has a nonZero yieldTo +/// @property Account Invariants +invariant yieldDelegationSourceHasNonZeroYeildTo() + forall address account . OUSD.rebaseState[account] == YieldDelegationSource() => OUSD.yieldTo[account] != 0; + +/// @title Any account with rebaseState = YieldDelegationTarget has a nonZero yieldFrom +/// @property Account Invariants +invariant yieldDelegationTargetHasNonZeroYeildFrom() + forall address account . OUSD.rebaseState[account] == YieldDelegationTarget() => OUSD.yieldFrom[account] != 0; + +// Helper Invariants +/// @title yieldTo of zero is zero +/// @property Account Invariants +invariant yieldToOfZeroIsZero() + yieldTo(0) == 0; + +/// @title yieldFrom of zero is zero +/// @property Account Invariants +invariant yieldFromOfZeroIsZero() + yieldFrom(0) == 0; + +/// @title yieldTo of an account can't be the same as the account +/// @property Account Invariants +invariant cantYieldToSelf() + forall address account . OUSD.yieldTo[account] != 0 => OUSD.yieldTo[account] != account; + +/// @title yieldFrom of an account can't be the same as the account +/// @property Account Invariants +invariant cantYieldFromSelf() + forall address account . OUSD.yieldFrom[account] != 0 => OUSD.yieldFrom[account] != account; + +/// @title Only delegation changes the different effective identity. +/// @property Account Invariants +rule onlyDelegationChangesPairingState(address accountA, address accountB, method f) +filtered{f -> !f.isView} +{ + bool different_before = differentAccounts(accountA, accountB); + env e; + calldataarg args; + f(e, args); + bool different_after = differentAccounts(accountA, accountB); + + if(delegateMethods(f)) { + satisfy different_before != different_after; + } + assert different_before != different_after => delegateMethods(f); +} diff --git a/certora/specs/OUSD/BalanceInvariants.spec b/certora/specs/OUSD/BalanceInvariants.spec new file mode 100644 index 0000000000..56f25375da --- /dev/null +++ b/certora/specs/OUSD/BalanceInvariants.spec @@ -0,0 +1,183 @@ +import "./common.spec"; +import "./AccountInvariants.spec"; + +// holds the credits sum of all accounts in stdNonRebasing state. +ghost mathint sumAllNonRebasingBalances { + init_state axiom sumAllNonRebasingBalances == 0; +} + +// holds the credits sum of all accounts in one of the following states: NotSet, StdRebasing, and YieldDelegationTarget. +ghost mathint sumAllRebasingBalances { + init_state axiom sumAllRebasingBalances == 0; +} + +ghost mapping(address => uint256) creditBalancesMirror { + init_state axiom forall address account . creditBalancesMirror[account] == 0; +} + +ghost mapping(address => OUSD.RebaseOptions) rebaseStateMirror { + init_state axiom forall address account . rebaseStateMirror[account] == NotSet(); +} + +hook Sload uint256 creditBalance creditBalances[KEY address account] { + require creditBalance == creditBalancesMirror[account]; +} + +hook Sload OUSD.RebaseOptions rebaseOption rebaseState[KEY address account] { + require rebaseOption == rebaseStateMirror[account]; +} + +// rebaseState is always updated before updateing the credits balance (when it is updated) so the best way to keep track of credit balance per state +// is to add the changes when the credits are updated with consideration to the current account rebasing state. +hook Sstore creditBalances[KEY address account] uint256 new_creditBalance (uint256 old_creditBalance) { + require old_creditBalance == creditBalancesMirror[account]; + if (rebaseStateMirror[account] == StdNonRebasing()) { + sumAllNonRebasingBalances = sumAllNonRebasingBalances - old_creditBalance + new_creditBalance; + } else if (rebaseStateMirror[account] != YieldDelegationSource()) { + sumAllRebasingBalances = sumAllRebasingBalances - old_creditBalance + new_creditBalance; + } + creditBalancesMirror[account] = new_creditBalance; +} + +hook Sstore rebaseState[KEY address account] OUSD.RebaseOptions new_rebaseOption (OUSD.RebaseOptions old_rebaseOption) { + require old_rebaseOption == rebaseStateMirror[account]; + // transitioning out of StdNonRebasing state - substract balance from sumAllNonRebasing + if(old_rebaseOption == StdNonRebasing() && new_rebaseOption != StdNonRebasing()) { + sumAllNonRebasingBalances = sumAllNonRebasingBalances - creditBalancesMirror[account]; + // transitioning into StdNonRebasing state - add balance to sumAllNonRebasing + } else if (old_rebaseOption != StdNonRebasing() && new_rebaseOption == StdNonRebasing()) { + sumAllNonRebasingBalances = sumAllNonRebasingBalances + creditBalancesMirror[account]; + } + // transitioning into rebasing state - add balance to sumAllRebasing + if (!isRebasing(old_rebaseOption) && isRebasing(new_rebaseOption)) { + sumAllRebasingBalances = sumAllRebasingBalances + creditBalancesMirror[account]; + } + // transitioning out of rebasing state - subtract balance from sumAllRebasing + else if (isRebasing(old_rebaseOption) && !isRebasing(new_rebaseOption)) { + sumAllRebasingBalances = sumAllRebasingBalances - creditBalancesMirror[account]; + } + + rebaseStateMirror[account] = new_rebaseOption; +} + +/// @title The sum of all RebaseOptions.StdNonRebasing accounts equals the nonRebasingSupply. +/// @property Balance Invariants +invariant sumAllNonRebasingBalancesEqNonRebasingSupply() + sumAllNonRebasingBalances == nonRebasingSupply() + { + preserved { + initTotalSupply(); + allAccountValidState(); + require OUSD.rebasingCreditsPerToken_ >= e18(); + } + } + +/// @title The sum of the credits in all NotSet, StdRebasing, and YieldDelegationTarget accounts equal the rebasingCredits. +/// @property Balance Invariants +invariant sumAllRebasingCreditsEqRebasingCredits() + sumAllRebasingBalances == rebasingCreditsHighres() + { + preserved { + initTotalSupply(); + allAccountValidState(); + require OUSD.rebasingCreditsPerToken_ >= e18(); + } + } + +/// @title Ensure correlation between the sum of the credits in all NotSet, StdRebasing, and YieldDelegationTarget accounts match +/// the rebasingCredits allowing for a bounded rounding error calculated as `rebasingCreditsPerToken / 1e18` for both rebaseOptIn and governanceRebaseOptIn. +/// @property Balance Invariants +rule sumAllRebasingCreditsAndTotalRebasingCreditsCorelation(method f) + filtered{f -> f.selector == sig:rebaseOptIn().selector || + f.selector == sig:governanceRebaseOptIn(address).selector} + { + env e; + calldataarg args; + + initTotalSupply(); + allAccountValidState(); + require OUSD.rebasingCreditsPerToken_ >= e18(); + + require sumAllRebasingBalances == rebasingCreditsHighres(); + + f(e, args); + + assert EqualUpTo(sumAllRebasingBalances, rebasingCreditsHighres(), BALANCE_ROUNDING_ERROR(OUSD.rebasingCreditsPerToken_)); +} + +/// @title Verify that the total supply remains within the maximum allowable limit. +/// @property Balance Invariants +invariant totalSupplyLessThanMaxSupply() + OUSD.totalSupply() <= max_uint128 + { + preserved { + initTotalSupply(); + allAccountValidState(); + require OUSD.rebasingCreditsPerToken_ >= e18(); + requireInvariant sumAllNonRebasingBalancesEqNonRebasingSupply(); + require isInitialized(); + } + } + +/// @title Verify that the total balance of delegator and delegatee remains unchanged after yield delegation. +/// @property Balance Invariants +rule delegateYieldPreservesSumOfBalances(address from, address to, address other) { + env e; + initTotalSupply(); + allAccountValidState(); + require OUSD.rebasingCreditsPerToken_ >= e18(); + require other != from; + require other != to; + + uint256 fromBalancePre = OUSD.balanceOf(from); + uint256 toBalancePre = OUSD.balanceOf(to); + uint256 otherBalancePre = OUSD.balanceOf(other); + uint256 totalSupplyPre = OUSD.totalSupply(); + + mathint sumBalancesPre = fromBalancePre + toBalancePre; + + delegateYield(e, from, to); + + uint256 fromBalancePost = OUSD.balanceOf(from); + uint256 toBalancePost = OUSD.balanceOf(to); + uint256 otherBalancePost = OUSD.balanceOf(other); + uint256 totalSupplyPost = OUSD.totalSupply(); + + mathint sumBalancesPost = fromBalancePost + toBalancePost; + + assert sumBalancesPre == sumBalancesPost; + assert otherBalancePre == otherBalancePost; + assert totalSupplyPre == totalSupplyPost; +} + +/// @title Verify that the total balance of delegator and delegatee remains unchanged after undelegation. +/// @property Balance Invariants +rule undelegateYieldPreservesSumOfBalances(address from, address other) { + env e; + initTotalSupply(); + allAccountValidState(); + require OUSD.rebasingCreditsPerToken_ >= e18(); + address yieldedTo = OUSD.yieldTo[from]; + require other != from; + require other != yieldedTo; + + uint256 fromBalancePre = OUSD.balanceOf(from); + uint256 toBalancePre = OUSD.balanceOf(yieldedTo); + uint256 otherBalancePre = OUSD.balanceOf(other); + uint256 totalSupplyPre = OUSD.totalSupply(); + + mathint sunBalancesPre = fromBalancePre + toBalancePre; + + undelegateYield(e, from); + + uint256 fromBalancePost = OUSD.balanceOf(from); + uint256 toBalancePost = OUSD.balanceOf(yieldedTo); + uint256 otherBalancePost = OUSD.balanceOf(other); + uint256 totalSupplyPost = OUSD.totalSupply(); + + mathint sunBalancesPost = fromBalancePost + toBalancePost; + + assert sunBalancesPost == sunBalancesPre; + assert otherBalancePre == otherBalancePost; + assert totalSupplyPre == totalSupplyPost; +} diff --git a/certora/specs/OUSD/OtherInvariants.spec b/certora/specs/OUSD/OtherInvariants.spec new file mode 100644 index 0000000000..675f2e71c7 --- /dev/null +++ b/certora/specs/OUSD/OtherInvariants.spec @@ -0,0 +1,306 @@ +import "./common.spec"; +import "./AccountInvariants.spec"; + +/// @title Verify account balance integrity based on rebase state +// Ensures balances are correctly calculated for Yield Delegation Targets, Standard Rebasing, +// Non-Rebasing, and undefined (NotSet) states to maintain consistency in OUSD accounting. +/// @property Balance Integrities +rule balanceOfIntegrity(address account) { + env e; + initTotalSupply(); + allAccountValidState(); + require OUSD.rebasingCreditsPerToken_ >= e18(); + + OUSD.RebaseOptions accountState = OUSD.rebaseState[account]; + + address delegator = OUSD.yieldFrom[account]; + uint256 balance = balanceOf(account); + uint256 delegatorBalance = balanceOf(delegator); + + mathint baseBalance = (OUSD.creditBalances[account] * e18()) / OUSD.rebasingCreditsPerToken_; + + if (accountState == YieldDelegationTarget()) { + assert balance + delegatorBalance == baseBalance; + } else if (accountState == NotSet() || accountState == StdRebasing()) { + assert balance == baseBalance; + } else if (accountState == StdNonRebasing()) { + assert balance == OUSD.creditBalances[account]; + } + assert true; +} + +/// @title After a non-reverting call to rebaseOptIn() the alternativeCreditsPerToken[account] == 0 and does not result in a change in account balance. +/// @property Balance Integrities +rule rebaseOptInIntegrity() { + env e; + address account = e.msg.sender; + initTotalSupply(); + allAccountValidState(); + require OUSD.rebasingCreditsPerToken_ >= e18(); + + uint256 balancePre = OUSD.balanceOf(account); + + OUSD.rebaseOptIn(e); + + uint256 balancePost = OUSD.balanceOf(account); + + assert OUSD.alternativeCreditsPerToken[account] == 0; + assert balancePre == balancePost; +} + +/// @title After a non-reverting call to governanceRebaseOptIn() the alternativeCreditsPerToken[account] == 0 and does not result in a change in account balance. +/// @property Balance Integrities +rule governanceRebaseOptInIntegrity(address account) { + env e; + initTotalSupply(); + allAccountValidState(); + require OUSD.rebasingCreditsPerToken_ >= e18(); + + uint256 balancePre = OUSD.balanceOf(account); + + OUSD.governanceRebaseOptIn(e, account); + + uint256 balancePost = OUSD.balanceOf(account); + + assert OUSD.alternativeCreditsPerToken[account] == 0; + assert balancePre == balancePost; +} + +/// @title After a non-reverting call to rebaseOptOut() the alternativeCreditsPerToken[account] == 1e18 and does not result in a change in account balance. +/// @property Balance Integrities +rule rebaseOptOutIntegrity() { + env e; + address account = e.msg.sender; + initTotalSupply(); + allAccountValidState(); + + uint256 balancePre = OUSD.balanceOf(account); + + OUSD.rebaseOptOut(e); + + uint256 balancePost = OUSD.balanceOf(account); + + assert OUSD.alternativeCreditsPerToken[account] == e18(); + assert balancePre == balancePost; +} + +/// @title Only transfer, transferFrom, mint, burn, and changeSupply result in a change in any account's balance. +/// @property Balance Integrities +rule whoCanChangeBalance(method f, address account) { + env e; + calldataarg args; + initTotalSupply(); + allAccountValidState(); + require OUSD.rebasingCreditsPerToken_ >= e18(); + require isInitialized(); + + uint256 balancePre = OUSD.balanceOf(account); + + f(e, args); + + uint256 balancePost = OUSD.balanceOf(account); + + assert balancePre != balancePost => whoCanChangeBalance(f); +} + +/// @title A successful mint() call by the vault results in the target account's balance increasing by the amount specified. +/// @property Balance Integrities +rule mintIntegrity(address account, uint256 amount) { + env e; + initTotalSupply(); + allAccountValidState(); + require OUSD.rebasingCreditsPerToken_ >= e18(); + + uint256 balancePre = OUSD.balanceOf(account); + + mint(e, account, amount); + + uint256 balancePost = OUSD.balanceOf(account); + + assert balancePost == balancePre + amount; +} + +/// @title A successful burn() call by the vault results in the target account's balance decreasing by the amount specified. +/// @property Balance Integrities +rule burnIntegrity(address account, uint256 amount) { + env e; + initTotalSupply(); + allAccountValidState(); + require OUSD.rebasingCreditsPerToken_ >= e18(); + + uint256 balancePre = OUSD.balanceOf(account); + + burn(e, account, amount); + + uint256 balancePost = OUSD.balanceOf(account); + + assert balancePost == balancePre - amount; +} + +/// @title After a call to changeSupply() then nonRebasingCredits + (rebasingCredits / rebasingCreditsPer) <= totalSupply and the new totalSupply match what was passed into the call. +/// @property Balance Integrities +rule changeSupplyIntegrity(uint256 newTotalSupply) { + env e; + initTotalSupply(); + allAccountValidState(); + require OUSD.rebasingCreditsPerToken_ >= e18(); + require newTotalSupply >= OUSD.totalSupply(); + + OUSD.changeSupply(e, newTotalSupply); + + assert OUSD.totalSupply() == newTotalSupply; + assert (nonRebasingSupply() + (rebasingCreditsHighres() / OUSD.rebasingCreditsPerToken_)) <= OUSD.totalSupply(); +} + +/// @title Only transfers, mints, and burns change the balance of StdNonRebasing and YieldDelegationSource accounts. +/// @property Balance Integrities +rule whoCanChangeNonRebasingBalance(method f, address account) { + env e; + calldataarg args; + initTotalSupply(); + allAccountValidState(); + require OUSD.rebasingCreditsPerToken_ >= e18(); + require isInitialized(); + + uint256 balancePre = OUSD.balanceOf(account); + + f(e, args); + + uint256 balancePost = OUSD.balanceOf(account); + OUSD.RebaseOptions statePost = OUSD.rebaseState[account]; + + assert balancePre != balancePost && (statePost == StdNonRebasing() || statePost == YieldDelegationSource()) => + f.selector == sig:transfer(address, uint256) .selector || + f.selector == sig:transferFrom(address, address, uint256).selector || + f.selector == sig:mint(address, uint256).selector || + f.selector == sig:burn(address, uint256).selector; +} + +/// @title Recipient and sender (msg.sender) account balances should increase and decrease respectively by the amount after a transfer operation +// Account balance should not change after a transfer operation if the recipient is the sender. +/// @property Balance Integrities +rule transferIntegrityTo(address account, uint256 amount) { + env e; + require sufficientResolution(); + allAccountValidState(); + initTotalSupply(); + + uint256 toBalanceBefore = balanceOf(account); + uint256 fromBalanceBefore = balanceOf(e.msg.sender); + + transfer(e, account, amount); + + uint256 toBalanceAfter = balanceOf(account); + uint256 fromBalanceAfter = balanceOf(e.msg.sender); + + assert account != e.msg.sender => toBalanceAfter - toBalanceBefore == amount; + assert account != e.msg.sender => fromBalanceBefore - fromBalanceAfter == amount; + assert account == e.msg.sender => toBalanceBefore == toBalanceAfter; +} + +/// @title Transfer doesn't change the balance of a third party. +/// @property Balance Integrities +rule transferThirdParty(address account) { + env e; + address to; + uint256 amount; + + uint256 otherBalanceBefore = balanceOf(account); + require sufficientResolution(); + + // requiring proved invariants + allAccountValidState(); + initTotalSupply(); + + transfer(e, to, amount); + uint256 otherUserBalanceAfter = balanceOf(account); + + assert (e.msg.sender != account && to != account) => otherBalanceBefore == otherUserBalanceAfter; +} + +/// @title Account balance should be increased by the amount minted. +/// @property Balance Integrities +rule mintIntegrityTo(address account, uint256 amount) { + env e; + uint256 balanceBefore = balanceOf(account); + + // assumption for the known rounding error that goes like ~ 10^18 / rebasingCreditsPerToken_ + require sufficientResolution(); + + // requiring proved invariants + allAccountValidState(); + initTotalSupply(); + + mint(e, account, amount); + + uint256 balanceAfter = balanceOf(account); + + assert balanceAfter - balanceBefore == amount; +} + +/// @title Any third-party account balance should not change after a mint operation. +/// @property Balance Integrities +rule mintIntegrityThirdParty(address account) { + env e; + address to; + uint256 amount; + + uint256 otherBalanceBefore = balanceOf(account); + + // assumption for the known rounding error that goes like ~ 10^18 / rebasingCreditsPerToken_ + require sufficientResolution(); + + // requiring proved invariants + allAccountValidState(); + initTotalSupply(); + + mint(e, to, amount); + + uint256 otherBalanceAfter = balanceOf(account); + + assert to != account => otherBalanceBefore == otherBalanceAfter; +} + +/// @title Account balance should be decreased by the amount burned. +/// @property Balance Integrities +rule burnIntegrityTo(address account, uint256 amount) { + env e; + + uint256 balanceBefore = balanceOf(account); + + // assumption for the known rounding error that goes like ~ 10^18 / rebasingCreditsPerToken_ + require sufficientResolution(); + + // requiring proved invariants + allAccountValidState(); + initTotalSupply(); + + burn(e, account, amount); + + uint256 balanceAfter = balanceOf(account); + + assert balanceBefore - balanceAfter == amount; +} + +/// @title Any third-party account balance should not change after a burn operation. +/// @property Balance Integrities +rule burnIntegrityThirdParty(address account) { + env e; + address to; + uint256 amount; + + uint256 otherBalanceBefore = balanceOf(account); + + // assumption for the known rounding error that goes like ~ 10^18 / rebasingCreditsPerToken_ + require sufficientResolution(); + + // requiring proved invariants + allAccountValidState(); + initTotalSupply(); + + burn(e, to, amount); + + uint256 otherBalanceAfter = balanceOf(account); + + assert to != account => otherBalanceBefore == otherBalanceAfter; +} diff --git a/certora/specs/OUSD/SumOfBalances.spec b/certora/specs/OUSD/SumOfBalances.spec new file mode 100644 index 0000000000..13f3098bb1 --- /dev/null +++ b/certora/specs/OUSD/SumOfBalances.spec @@ -0,0 +1,195 @@ +import "BalanceInvariants.spec"; + +definition whoChangesMultipleBalances(method f) returns bool = + f.selector == sig:initialize(address,uint256).selector || + f.selector == sig:changeSupply(uint256).selector; + +definition whoChangesSingleBalance(method f) returns bool = + !delegateMethods(f) && + !transferMethods(f) && + !whoChangesMultipleBalances(f); + +/// This function is symmetric with respect to exchange of user <-> yieldFrom[user] and user <-> yieldTo[user]. +function effectiveBalance(address user) returns mathint { + if (rebaseState(user) == YieldDelegationTarget()) { + return balanceOf(user) + balanceOf(OUSD.yieldFrom[user]); + } else if (rebaseState(user) == YieldDelegationSource()) { + return balanceOf(user) + balanceOf(OUSD.yieldTo[user]); + } else { + return to_mathint(balanceOf(user)); + } +} + +/// @title Auxiliary rule: the effective balance is the same for the same effective account. +rule effectiveBalanceIsEquivalentForSameAccounts(address accountA, address accountB) { + require OUSD.rebasingCreditsPerToken_ >= e18(); + allAccountValidState(); + + assert !differentAccounts(accountA, accountB) => effectiveBalance(accountA) == effectiveBalance(accountB); +} + +/// @title Both transfer methods must preserve the sum of balances. +/// The total supply and any balance of a third party cannot change. +/// @property Balance Invariants +rule transferPreservesSumOfBalances(address accountA, address accountB, method f) +filtered{f -> transferMethods(f)} +{ + //require OUSD.rebasingCreditsPerToken_ >= e18(); + /// Under-approximation : otherwise timesout. + require OUSD.rebasingCreditsPerToken_ == 1001*e18()/1000; + allAccountValidState(); + initTotalSupply(); + /// Third party (different user). + address other; + require differentAccounts(other, accountA); + require differentAccounts(other, accountB); + + mathint balanceA_pre = effectiveBalance(accountA); + mathint balanceB_pre = effectiveBalance(accountB); + mathint sumOfBalances_pre = differentAccounts(accountA, accountB) ? balanceA_pre + balanceB_pre : balanceA_pre; + mathint balanceO_pre = effectiveBalance(other); + mathint totalSupply_pre = totalSupply(); + env e; + if(f.selector == sig:transfer(address,uint256).selector) { + require e.msg.sender == accountA; + transfer(e, accountB, _); + } else if(f.selector == sig:transferFrom(address,address,uint256).selector) { + transferFrom(e, accountA, accountB, _); + } else { + assert false; + } + mathint balanceA_post = effectiveBalance(accountA); + mathint balanceB_post = effectiveBalance(accountB); + mathint sumOfBalances_post = differentAccounts(accountA, accountB) ? balanceA_post + balanceB_post : balanceA_post; + mathint balanceO_post = effectiveBalance(other); + mathint totalSupply_post = totalSupply(); + + assert differentAccounts(other, accountA), "The third party cannot change its identity status after transfer"; + assert differentAccounts(other, accountB), "The third party cannot change its identity status after transfer"; + assert sumOfBalances_pre == sumOfBalances_post, "The sum of balances must be conserved"; + assert balanceO_pre == balanceO_post, "The balance of a third party cannot change after transfer"; + assert totalSupply_pre == totalSupply_post, "The total supply is invariant to transfer operations"; +} + +/// @title The sum of balances of any two accounts cannot surpass the total supply. +/// @property Balance Invariants +rule sumOfTwoAccountsBalancesLETotalSupply(address accountA, address accountB, method f) +filtered{f -> !f.isView && !whoChangesMultipleBalances(f) && !delegateMethods(f) && !transferMethods(f)} +{ + require OUSD.rebasingCreditsPerToken_ >= e18(); + allAccountValidState(); + initTotalSupply(); + + address other; + require threeDifferentAccounts(accountA, accountB, other); + + mathint balanceA_pre = effectiveBalance(accountA); + mathint balanceB_pre = effectiveBalance(accountB); + mathint sumOfBalances_pre = balanceA_pre + balanceB_pre; + mathint totalSupply_pre = totalSupply(); + env e; + calldataarg args; + f(e, args); + mathint balanceA_post = effectiveBalance(accountA); + mathint balanceB_post = effectiveBalance(accountB); + mathint sumOfBalances_post = balanceA_post + balanceB_post; + mathint totalSupply_post = totalSupply(); + + /// Assume that only accountA and accountB balances change. + require balanceA_pre != balanceA_post && balanceB_pre != balanceB_post; + + assert sumOfBalances_pre <= totalSupply_pre => sumOfBalances_post <= totalSupply_post; +} + +/// @title The sum of all rebasing account balances cannot surpass the total supply after calling for changeSupply. +/// @property Balance Invariants +rule changeSupplyPreservesSumOFRebasingLesEqTotalSupply(uint256 amount) { + env e; + require OUSD.rebasingCreditsPerToken_ >= e18(); + allAccountValidState(); + initTotalSupply(); + require amount >= totalSupply(); + requireInvariant sumAllNonRebasingBalancesEqNonRebasingSupply(); + requireInvariant sumAllRebasingCreditsEqRebasingCredits(); + requireInvariant totalSupplyLessThanMaxSupply(); + + require sumAllRebasingBalances * e18() / OUSD.rebasingCreditsPerToken_ <= totalSupply(); + + changeSupply(e, amount); + + assert sumAllRebasingBalances * e18() / OUSD.rebasingCreditsPerToken_ <= totalSupply(); +} + +/// @title Which methods change the balance of a single account. +rule onlySingleAccountBalanceChange(address accountA, address accountB, method f) +filtered{f -> !f.isView && whoChangesSingleBalance(f)} +{ + require OUSD.rebasingCreditsPerToken_ >= e18(); + allAccountValidState(); + initTotalSupply(); + /// Require different accounts before + require differentAccounts(accountA, accountB); + /// Probe balances before + mathint balanceA_pre = effectiveBalance(accountA); + mathint balanceB_pre = effectiveBalance(accountB); + /// Call an arbitrary function. + env e; + calldataarg args; + f(e, args); + /// Require different accounts after + require differentAccounts(accountA, accountB); + /// Probe balances after + mathint balanceA_post = effectiveBalance(accountA); + mathint balanceB_post = effectiveBalance(accountB); + + assert balanceA_pre != balanceA_post => balanceB_pre == balanceB_post; +} + +/// @title Which methods change the balance of only two accounts. +rule onlyTwoAccountsBalancesChange(address accountA, address accountB, address accountC, method f) +filtered{f -> !f.isView && !whoChangesMultipleBalances(f) && !delegateMethods(f)} +{ + require OUSD.rebasingCreditsPerToken_ >= e18(); + allAccountValidState(); + initTotalSupply(); + /// Require different accounts before + require threeDifferentAccounts(accountA, accountB, accountC); + /// Probe balances before + mathint balanceA_pre = effectiveBalance(accountA); + mathint balanceB_pre = effectiveBalance(accountB); + mathint balanceC_pre = effectiveBalance(accountC); + /// Call an arbitrary function. + env e; + calldataarg args; + f(e, args); + /// Probe balances after + mathint balanceA_post = effectiveBalance(accountA); + mathint balanceB_post = effectiveBalance(accountB); + mathint balanceC_post = effectiveBalance(accountC); + + /// Assert different accounts after + assert threeDifferentAccounts(accountA, accountB, accountC); + assert balanceA_pre != balanceA_post && balanceB_pre != balanceB_post => balanceC_post == balanceC_pre; +} + +/// @title If two accounts become paired / unpaired, then their sum of balances is preserved, and the total supply is unchanged. +rule pairingPreservesSumOfBalances(address accountA, address accountB, method f) +filtered{f -> !f.isView} +{ + require OUSD.rebasingCreditsPerToken_ == e18(); + allAccountValidState(); + initTotalSupply(); + + bool different_before = differentAccounts(accountA, accountB); + mathint sumOfBalances_pre = balanceOf(accountA) + balanceOf(accountB); + mathint totalSupply_pre = totalSupply(); + env e; + calldataarg args; + f(e, args); + bool different_after = differentAccounts(accountA, accountB); + mathint sumOfBalances_post = balanceOf(accountA) + balanceOf(accountB); + mathint totalSupply_post = totalSupply(); + + assert different_before != different_after => sumOfBalances_post == sumOfBalances_pre; + assert different_before != different_after => totalSupply_pre == totalSupply_post; +} diff --git a/certora/specs/OUSD/common.spec b/certora/specs/OUSD/common.spec new file mode 100644 index 0000000000..0a6caa3007 --- /dev/null +++ b/certora/specs/OUSD/common.spec @@ -0,0 +1,92 @@ +using OUSD as OUSD; + +methods { + function OUSD.yieldTo(address) external returns (address) envfree; + function OUSD.yieldFrom(address) external returns (address) envfree; + function OUSD.totalSupply() external returns (uint256) envfree; + function OUSD.rebasingCreditsPerTokenHighres() external returns (uint256) envfree; + function OUSD.rebasingCreditsPerToken() external returns (uint256) envfree; + function OUSD.rebasingCreditsHighres() external returns (uint256) envfree; + function OUSD.rebasingCredits() external returns (uint256) envfree; + function OUSD.balanceOf(address) external returns (uint256) envfree; + function OUSD.creditsBalanceOf(address) external returns (uint256,uint256) envfree; + function OUSD.creditsBalanceOfHighres(address) external returns (uint256,uint256,bool) envfree; + function OUSD.nonRebasingCreditsPerToken(address) external returns (uint256) envfree; + function OUSD.transfer(address,uint256) external returns (bool); + function OUSD.transferFrom(address,address,uint256) external returns (bool); + function OUSD.allowance(address,address) external returns (uint256) envfree; + function OUSD.approve(address,uint256) external returns (bool); + function OUSD.mint(address,uint256) external; + function OUSD.burn(address,uint256) external; + function OUSD.governanceRebaseOptIn(address) external; + function OUSD.rebaseOptIn() external; + function OUSD.rebaseOptOut() external; + function OUSD.changeSupply(uint256) external; + function OUSD.delegateYield(address, address) external; + function OUSD.undelegateYield(address) external; + function rebaseState(address) external returns (OUSD.RebaseOptions) envfree; + function nonRebasingSupply() external returns (uint256) envfree; +} + +definition e18() returns uint256 = 1000000000000000000; // definition for 1e18 + +definition MIN_TOTAL_SUPPLY() returns mathint = 10^16; + +// RebaseOptions state definitions +definition NotSet() returns OUSD.RebaseOptions = OUSD.RebaseOptions.NotSet; +definition StdRebasing() returns OUSD.RebaseOptions = OUSD.RebaseOptions.StdRebasing; +definition StdNonRebasing() returns OUSD.RebaseOptions = OUSD.RebaseOptions.StdNonRebasing; +definition YieldDelegationTarget() returns OUSD.RebaseOptions = OUSD.RebaseOptions.YieldDelegationTarget; +definition YieldDelegationSource() returns OUSD.RebaseOptions = OUSD.RebaseOptions.YieldDelegationSource; + +function initTotalSupply() { require totalSupply() >= MIN_TOTAL_SUPPLY(); } + +definition sufficientResolution() returns bool = rebasingCreditsPerToken() >= e18(); + +definition EqualUpTo(mathint A, mathint B, mathint TOL) returns bool = + A > B ? A - B <= TOL : B - A <= TOL; + +definition BALANCES_TOL() returns mathint = 2; + +// p = rebasingCreditsPerToken_ +definition BALANCE_ERROR(uint256 p) returns mathint = e18() / p; + +definition BALANCE_ROUNDING_ERROR(uint256 p) returns mathint = p / e18(); + +definition isInitialized() returns bool = OUSD.vaultAddress != 0; + +definition whoCanChangeBalance(method f) returns bool = + f.selector == sig:transfer(address, uint256).selector || + f.selector == sig:transferFrom(address, address, uint256).selector || + f.selector == sig:mint(address, uint256).selector || + f.selector == sig:burn(address, uint256).selector || + f.selector == sig:changeSupply(uint256).selector || + false; + +definition isRebasing(OUSD.RebaseOptions state) returns bool = + state == NotSet() || + state == StdRebasing() || + state == YieldDelegationTarget() || + false; + +definition differentAccounts(address accountA, address accountB) returns bool = + /// Account have different identities + (accountA != accountB) && + /// The yield target of accountA is not accountB + (OUSD.rebaseState[accountA] == YieldDelegationSource() => OUSD.yieldTo[accountA] != accountB) && + /// The yield source of accountA is not accountB + (OUSD.rebaseState[accountA] == YieldDelegationTarget() => OUSD.yieldFrom[accountA] != accountB); + +definition threeDifferentAccounts(address accountA, address accountB, address accountC) returns bool = + differentAccounts(accountA, accountB) && + differentAccounts(accountA, accountC) && + differentAccounts(accountB, accountC); + +definition transferMethods(method f) returns bool = + f.selector == sig:transfer(address,uint256).selector || + f.selector == sig:transferFrom(address,address,uint256).selector; + +definition delegateMethods(method f) returns bool = + f.selector == sig:undelegateYield(address).selector || + f.selector == sig:delegateYield(address,address).selector; + \ No newline at end of file From e579d5b81476ed9dea4f45ce7f87b56e170ce844 Mon Sep 17 00:00:00 2001 From: Roy-Certora Date: Wed, 18 Dec 2024 10:03:11 +0200 Subject: [PATCH 2/3] Small updates to running scripts. --- certora/confs/OUSD_balances.conf | 4 +++- certora/confs/OUSD_other.conf | 3 ++- certora/run.sh | 1 + 3 files changed, 6 insertions(+), 2 deletions(-) diff --git a/certora/confs/OUSD_balances.conf b/certora/confs/OUSD_balances.conf index 74c3b610c0..2198f7d8a8 100644 --- a/certora/confs/OUSD_balances.conf +++ b/certora/confs/OUSD_balances.conf @@ -8,8 +8,10 @@ ], "process": "emv", "prover_args": [ - + "-mediumTimeout 50", ], + "multi_assert_check":true, + "smt_timeout":"1000", "solc": "solc8.28", "verify": "OUSD:certora/specs/OUSD/BalanceInvariants.spec", "server": "production" diff --git a/certora/confs/OUSD_other.conf b/certora/confs/OUSD_other.conf index 8abded891d..cc28a77c16 100644 --- a/certora/confs/OUSD_other.conf +++ b/certora/confs/OUSD_other.conf @@ -8,8 +8,9 @@ ], "process": "emv", "prover_args": [ - + "-mediumTimeout 40", ], + "smt_timeout":"1000", "solc": "solc8.28", "verify": "OUSD:certora/specs/OUSD/OtherInvariants.spec", "server": "production" diff --git a/certora/run.sh b/certora/run.sh index 6c52eab517..c6c57a4140 100644 --- a/certora/run.sh +++ b/certora/run.sh @@ -1,3 +1,4 @@ +certoraRun certora/confs/OUSD_accounting.conf certoraRun certora/confs/OUSD_balances.conf certoraRun certora/confs/OUSD_other.conf certoraRun certora/confs/OUSD_sumOfBalances.conf From 8afe596fc36081567d307f79e545f5d5b146bba3 Mon Sep 17 00:00:00 2001 From: Roy-Certora Date: Wed, 18 Dec 2024 13:42:06 +0200 Subject: [PATCH 3/3] Add invariants to SumOfBalances spec. --- certora/confs/OUSD_balances.conf | 2 +- certora/confs/OUSD_sumOfBalances.conf | 1 + certora/specs/OUSD/OtherInvariants.spec | 6 ++++++ certora/specs/OUSD/SumOfBalances.spec | 2 +- 4 files changed, 9 insertions(+), 2 deletions(-) diff --git a/certora/confs/OUSD_balances.conf b/certora/confs/OUSD_balances.conf index 2198f7d8a8..c1c8d283f7 100644 --- a/certora/confs/OUSD_balances.conf +++ b/certora/confs/OUSD_balances.conf @@ -8,7 +8,7 @@ ], "process": "emv", "prover_args": [ - "-mediumTimeout 50", + "-mediumTimeout 40", ], "multi_assert_check":true, "smt_timeout":"1000", diff --git a/certora/confs/OUSD_sumOfBalances.conf b/certora/confs/OUSD_sumOfBalances.conf index d0bc8568f4..34d9d30c47 100644 --- a/certora/confs/OUSD_sumOfBalances.conf +++ b/certora/confs/OUSD_sumOfBalances.conf @@ -9,6 +9,7 @@ "process": "emv", "prover_args": [ "-mediumTimeout 40", + "-s [z3:lia2,z3:arith1,yices:def]", ], "multi_assert_check":true, "smt_timeout":"1000", diff --git a/certora/specs/OUSD/OtherInvariants.spec b/certora/specs/OUSD/OtherInvariants.spec index 675f2e71c7..de3ebdaf11 100644 --- a/certora/specs/OUSD/OtherInvariants.spec +++ b/certora/specs/OUSD/OtherInvariants.spec @@ -1,5 +1,9 @@ import "./common.spec"; import "./AccountInvariants.spec"; +import "./BalanceInvariants.spec"; + +use invariant sumAllNonRebasingBalancesEqNonRebasingSupply; +use invariant sumAllRebasingCreditsEqRebasingCredits; /// @title Verify account balance integrity based on rebase state // Ensures balances are correctly calculated for Yield Delegation Targets, Standard Rebasing, @@ -143,6 +147,8 @@ rule changeSupplyIntegrity(uint256 newTotalSupply) { env e; initTotalSupply(); allAccountValidState(); + requireInvariant sumAllNonRebasingBalancesEqNonRebasingSupply(); + requireInvariant sumAllRebasingCreditsEqRebasingCredits(); require OUSD.rebasingCreditsPerToken_ >= e18(); require newTotalSupply >= OUSD.totalSupply(); diff --git a/certora/specs/OUSD/SumOfBalances.spec b/certora/specs/OUSD/SumOfBalances.spec index 13f3098bb1..cf08a24b63 100644 --- a/certora/specs/OUSD/SumOfBalances.spec +++ b/certora/specs/OUSD/SumOfBalances.spec @@ -176,7 +176,7 @@ filtered{f -> !f.isView && !whoChangesMultipleBalances(f) && !delegateMethods(f) rule pairingPreservesSumOfBalances(address accountA, address accountB, method f) filtered{f -> !f.isView} { - require OUSD.rebasingCreditsPerToken_ == e18(); + require OUSD.rebasingCreditsPerToken_ >= e18(); allAccountValidState(); initTotalSupply();