Skip to content

Commit

Permalink
Yield Delegation / Rebasing Token Rewrite (#2298)
Browse files Browse the repository at this point in the history
* initial second implementation of rebasing to another account

* update to core functionality

* add gas fucntion

* simplify execute

* simplify mint and burn

* initial version of Daniel's yield delegation implementation

* prettier and linter fixes

* Add slots to OUSD contract to align with existing deployments

* Generated new OUSD contract diagrams

* Added deploy scripts for OToken upgrades

* Generated new OUSD storage diagram

* some minor bug fixes

* Prettier and fix spelling in comments

* Unit test fixes

* fix initialise function sigature and visibility of functions

* fix some tests

* add explanation for the alternativeCreditsPerToken check

* prettier

* reintroduce the original check

* explicitly call rebaseOpt out if the yield delegating account hasn't opted out already

* add one more test

* add Readme of the token contract logic

* force account to be rebasing on yield delegation

* add explicit whitelist of allowed states when delegating yield

* add more defensive checks where isNonRebasingAccount can not mistankingly be used to return true for yield delegation sources

* remove increase/decrease allowance

* Update docs with invarients

* Use safecast for any downcasting (#2306)

* use safecasts for any downcasting

* use safecast when downcasting from int256. Also fix tests

* prettier

* clean up implementation

* More invarients around outer functions

* Format invarients

* further simplify the code when handling different rebase states

* remove nonreentrant modifiers from the toke code as they are not needed

* allow empty conracts to rebaseOptIn without auto migration

* Transfer unit tests for new token implementation (#2310)

* remove nonreentrant modifiers from the toke code as they are not needed

* add setup for all account types

* check all relevant contract initial states

* add test between any possible contract accounts

* prettier

* add some documentation and prettier

* More invarients

* Correct total supply docs

* Transfer unit tests for new token implementation (#2310)

* remove nonreentrant modifiers from the toke code as they are not needed

* add setup for all account types

* check all relevant contract initial states

* add test between any possible contract accounts

* prettier

* add some documentation and prettier

* fix test

* remove redundant state checks

* remove overwriting the same value to alternativeCreditsPerToken

* add non zero checks in delegation functions

* correct error

* correct some contract view modifiers

* add a readable error message when allowance is exceeded

* reducing 2 functions to 1

* deprecate isUpgraded

* rename totalSupply

* improve initialisation checks

* remove gas optimisation that would also allow for errorneously large transfers

* remove underflow checks

* simplify code check for rebaseOptIn and add a test for it

* remove comments

* move the balance and credits query above the rebaseState changes

* use _adjustGlobals function to adjust globals in yield delegation

* futher simplify the undelegateYield function

* unify the variable names

* add comment

* a couple of more places to utilise the _adjustGlobals function

* no need this being a separate variable

* undo bug introduction

* wrong use of msg.sender bug fix

* function doesn't need to return any values

* simplify

* improve syntax

* add events for yield delegation

* remove var init

* fix deploy file

* add tests to catch possible incorrect rebaseOptIn / rebaseOptOut attributions

* simplify changeSupply code

* add storage slot gap

* Comments update

* Comments spelling update

* correct comments

* unify variable names

* make credits calculation based of off balance for higher accuracy (in context of rounding errors)

* minor gas optimisation

* correct storage slot amount so it totals to 200

* Improve rebasing supply accuracy V2 (#2314)

* accurate balance accounting v2 for nonRebasingSupply calculation

* prettier

* correct comment

* minor gas optimisation

* gas optimisation

* better naming

* add a test where multiple rebaseOptIn/OptOut calls do not result in increasing account balance

* add a check for zero address with governanceRebaseOptIn tx

* Update on rebasing

* add a check for zero address with governanceRebaseOptIn tx

* make an exception for balance exact non rebasing accounts (StdNonRebasing, YieldDelegationSource)

* add test for the 1e27 cpt token exception

* add a test to for creditsBalanceOf and creditsBalanceOfHighres

* add nonRebasingCreditsPerToken to the test

* add auto migration test and revert test for rebaseOptOut

* prettier

* add tests for missing requires in yield delegation

* simplify code

* revert to the previous implementation of the deprecated function

* add OETH upgrade deployment file

* change license to Business Source License

* prettier

* on changeSupply round up in the favour of the protocol

* round down when calculating credits from balances

* Revert "round down when calculating credits from balances"

This reverts commit dc854bc.

* fix typos (#2323)

* gas optimisation (#2322)

* add missing natspec (#2321)

* L-02 Missing Docstrings (#2319)

* add missing natspec

* corrections to code comments

* Correct globals storage

* Only empty accounts can rebaseOptIn if already rebasing

* gas optimisation

* remove extra new line

* optimise gas when setting alternativeCreditsPerToken (#2325)

* Certora Formal Verification for OUSD (#2329)

* Add OUSD spec files and running scripts

* Small updates to running scripts.

* Add invariants to SumOfBalances spec.

* Fix certora spec. Starting with an invalid state would result in an invalid state

---------

Co-authored-by: Nicholas Addison <[email protected]>
Co-authored-by: Daniel Von Fange <[email protected]>
Co-authored-by: Roy-Certora <[email protected]>
  • Loading branch information
4 people authored Jan 8, 2025
1 parent a29405f commit c38136a
Show file tree
Hide file tree
Showing 37 changed files with 3,060 additions and 806 deletions.
3 changes: 3 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -84,3 +84,6 @@ fork-coverage
unit-coverage

.VSCodeCounter

# Certora #
.certora_internal
16 changes: 16 additions & 0 deletions certora/confs/OUSD_accounting.conf
Original file line number Diff line number Diff line change
@@ -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",
}
18 changes: 18 additions & 0 deletions certora/confs/OUSD_balances.conf
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
{
"files": [
"contracts/contracts/token/OUSD.sol"
],
"msg": "OUSD Balances invariants",
"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/BalanceInvariants.spec",
"server": "production"
}
17 changes: 17 additions & 0 deletions certora/confs/OUSD_other.conf
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
{
"files": [
"contracts/contracts/token/OUSD.sol"
],
"msg": "OUSD other invariants",
"packages": [
"@openzeppelin/contracts=contracts/lib/openzeppelin/contracts",
],
"process": "emv",
"prover_args": [
"-mediumTimeout 40",
],
"smt_timeout":"1000",
"solc": "solc8.28",
"verify": "OUSD:certora/specs/OUSD/OtherInvariants.spec",
"server": "production"
}
19 changes: 19 additions & 0 deletions certora/confs/OUSD_sumOfBalances.conf
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
{
"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",
"-s [z3:lia2,z3:arith1,yices:def]",
],
"multi_assert_check":true,
"smt_timeout":"1000",
"solc": "solc8.28",
"verify": "OUSD:certora/specs/OUSD/SumOfBalances.spec",
"server": "production"
}
4 changes: 4 additions & 0 deletions certora/run.sh
Original file line number Diff line number Diff line change
@@ -0,0 +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
158 changes: 158 additions & 0 deletions certora/specs/OUSD/AccountInvariants.spec
Original file line number Diff line number Diff line change
@@ -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);
}
Loading

0 comments on commit c38136a

Please sign in to comment.