Skip to content

Commit 07b3e70

Browse files
Roy-CertoraRoy-Certora
authored
Certora Formal Verification for OUSD (#2329)
* Add OUSD spec files and running scripts * Small updates to running scripts. * Add invariants to SumOfBalances spec.
1 parent c980607 commit 07b3e70

File tree

11 files changed

+1017
-0
lines changed

11 files changed

+1017
-0
lines changed

‎.gitignore‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -84,3 +84,6 @@ fork-coverage
8484
unit-coverage
8585

8686
.VSCodeCounter
87+
88+
# Certora #
89+
.certora_internal

‎certora/confs/OUSD_accounting.conf‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
{
2+
"files": [
3+
"contracts/contracts/token/OUSD.sol"
4+
],
5+
"msg": "OUSD Accounting invariants",
6+
"packages": [
7+
"@openzeppelin/contracts=contracts/lib/openzeppelin/contracts",
8+
],
9+
"process": "emv",
10+
"prover_args": [
11+
12+
],
13+
"solc": "solc8.28",
14+
"verify": "OUSD:certora/specs/OUSD/AccountInvariants.spec",
15+
"server": "production",
16+
}

‎certora/confs/OUSD_balances.conf‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
{
2+
"files": [
3+
"contracts/contracts/token/OUSD.sol"
4+
],
5+
"msg": "OUSD Balances invariants",
6+
"packages": [
7+
"@openzeppelin/contracts=contracts/lib/openzeppelin/contracts",
8+
],
9+
"process": "emv",
10+
"prover_args": [
11+
"-mediumTimeout 40",
12+
],
13+
"multi_assert_check":true,
14+
"smt_timeout":"1000",
15+
"solc": "solc8.28",
16+
"verify": "OUSD:certora/specs/OUSD/BalanceInvariants.spec",
17+
"server": "production"
18+
}

‎certora/confs/OUSD_other.conf‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
{
2+
"files": [
3+
"contracts/contracts/token/OUSD.sol"
4+
],
5+
"msg": "OUSD other invariants",
6+
"packages": [
7+
"@openzeppelin/contracts=contracts/lib/openzeppelin/contracts",
8+
],
9+
"process": "emv",
10+
"prover_args": [
11+
"-mediumTimeout 40",
12+
],
13+
"smt_timeout":"1000",
14+
"solc": "solc8.28",
15+
"verify": "OUSD:certora/specs/OUSD/OtherInvariants.spec",
16+
"server": "production"
17+
}

‎certora/confs/OUSD_sumOfBalances.conf‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
{
2+
"files": [
3+
"contracts/contracts/token/OUSD.sol"
4+
],
5+
"msg": "OUSD Sum of balances rules",
6+
"packages": [
7+
"@openzeppelin/contracts=contracts/lib/openzeppelin/contracts",
8+
],
9+
"process": "emv",
10+
"prover_args": [
11+
"-mediumTimeout 40",
12+
"-s [z3:lia2,z3:arith1,yices:def]",
13+
],
14+
"multi_assert_check":true,
15+
"smt_timeout":"1000",
16+
"solc": "solc8.28",
17+
"verify": "OUSD:certora/specs/OUSD/SumOfBalances.spec",
18+
"server": "production"
19+
}

‎certora/run.sh‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
certoraRun certora/confs/OUSD_accounting.conf
2+
certoraRun certora/confs/OUSD_balances.conf
3+
certoraRun certora/confs/OUSD_other.conf
4+
certoraRun certora/confs/OUSD_sumOfBalances.conf

‎certora/specs/OUSD/AccountInvariants.spec‎

Lines changed: 158 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,158 @@
1+
import "./common.spec";
2+
3+
function allAccountValidState() {
4+
requireInvariant DelegationAccountsCorrelation();
5+
requireInvariant DelegationValidRebaseState();
6+
requireInvariant stdNonRebasingDoesntYield();
7+
requireInvariant alternativeCreditsPerTokenIsOneOrZeroOnly();
8+
requireInvariant yieldDelegationSourceHasNonZeroYeildTo();
9+
requireInvariant yieldDelegationTargetHasNonZeroYeildFrom();
10+
requireInvariant yieldToOfZeroIsZero();
11+
requireInvariant yieldFromOfZeroIsZero();
12+
requireInvariant cantYieldToSelf();
13+
requireInvariant cantYieldFromSelf();
14+
requireInvariant zeroAlternativeCreditsPerTokenStates();
15+
requireInvariant nonZeroAlternativeCreditsPerTokenStates();
16+
}
17+
18+
/// @title Any non zero valued YieldTo points to an account that has a YieldFrom pointing back to the starting account and vice versa.
19+
/// @property Account Invariants
20+
invariant DelegationAccountsCorrelation()
21+
forall address account.
22+
(OUSD.yieldTo[account] != 0 => (OUSD.yieldFrom[OUSD.yieldTo[account]] == account))
23+
&&
24+
(OUSD.yieldFrom[account] != 0 => (OUSD.yieldTo[OUSD.yieldFrom[account]] == account))
25+
{
26+
preserved with (env e) {
27+
requireInvariant DelegationValidRebaseState();
28+
requireInvariant yieldToOfZeroIsZero();
29+
requireInvariant yieldFromOfZeroIsZero();
30+
}
31+
}
32+
33+
/// @title Any non zero valued YieldTo points to an account Iff that account is in YieldDelegationSource state and
34+
/// Any non zero valued YieldFrom points to an account Iff that account is in YieldDelegationTarget state.
35+
/// @property Account Invariants
36+
invariant DelegationValidRebaseState()
37+
forall address account.
38+
(OUSD.yieldTo[account] != 0 <=> OUSD.rebaseState[account] == YieldDelegationSource())
39+
&&
40+
(OUSD.yieldFrom[account] != 0 <=> OUSD.rebaseState[account] == YieldDelegationTarget())
41+
{
42+
preserved with (env e) {
43+
requireInvariant DelegationAccountsCorrelation();
44+
requireInvariant yieldToOfZeroIsZero();
45+
requireInvariant yieldFromOfZeroIsZero();
46+
}
47+
}
48+
49+
/// @title Any account with a zero value in alternativeCreditsPerToken has a rebaseState that is one of (NotSet, StdRebasing, or YieldDelegationTarget)
50+
/// @property Account Invariants
51+
invariant zeroAlternativeCreditsPerTokenStates()
52+
forall address account . OUSD.alternativeCreditsPerToken[account] == 0 <=> (OUSD.rebaseState[account] == NotSet() ||
53+
OUSD.rebaseState[account] == StdRebasing() ||
54+
OUSD.rebaseState[account] == YieldDelegationTarget())
55+
{
56+
preserved {
57+
requireInvariant yieldToOfZeroIsZero();
58+
requireInvariant yieldFromOfZeroIsZero();
59+
requireInvariant DelegationAccountsCorrelation();
60+
requireInvariant DelegationValidRebaseState();
61+
}
62+
}
63+
64+
/// @title Any account with value of 1e18 in alternativeCreditsPerToken has a rebaseState that is one of (StdNonRebasing, YieldDelegationSource)
65+
/// @property Account Invariants
66+
invariant nonZeroAlternativeCreditsPerTokenStates()
67+
forall address account . OUSD.alternativeCreditsPerToken[account] != 0 <=> (OUSD.rebaseState[account] == StdNonRebasing() ||
68+
OUSD.rebaseState[account] == YieldDelegationSource())
69+
{
70+
preserved undelegateYield(address _account) with (env e) {
71+
requireInvariant yieldToOfZeroIsZero();
72+
requireInvariant yieldFromOfZeroIsZero();
73+
requireInvariant DelegationAccountsCorrelation();
74+
requireInvariant DelegationValidRebaseState();
75+
}
76+
}
77+
78+
/// @title The result of balanceOf of any account in StdNonRebasing state equals the account's credit-balance.
79+
/// @property Balance Invariants
80+
invariant stdNonRebasingBalanceEqCreditBalances(address account)
81+
OUSD.rebaseState[account] == StdNonRebasing() => OUSD.balanceOf(account) == OUSD.creditBalances[account]
82+
{
83+
preserved {
84+
requireInvariant yieldToOfZeroIsZero();
85+
requireInvariant yieldFromOfZeroIsZero();
86+
requireInvariant DelegationAccountsCorrelation();
87+
requireInvariant DelegationValidRebaseState();
88+
requireInvariant nonZeroAlternativeCreditsPerTokenStates();
89+
requireInvariant stdNonRebasingDoesntYield();
90+
requireInvariant alternativeCreditsPerTokenIsOneOrZeroOnly();
91+
}
92+
}
93+
94+
/// @title Any account in StdNonRebasing state doesn't yield to no account.
95+
/// @property Account Invariants
96+
invariant stdNonRebasingDoesntYield()
97+
forall address account . OUSD.rebaseState[account] == StdNonRebasing() => OUSD.yieldTo[account] == 0
98+
{
99+
preserved {
100+
requireInvariant yieldToOfZeroIsZero();
101+
requireInvariant yieldFromOfZeroIsZero();
102+
requireInvariant DelegationAccountsCorrelation();
103+
requireInvariant DelegationValidRebaseState();
104+
}
105+
}
106+
107+
/// @title alternativeCreditsPerToken can only be set to 0 or 1e18, no other values
108+
/// @property Account Invariants
109+
invariant alternativeCreditsPerTokenIsOneOrZeroOnly()
110+
forall address account . OUSD.alternativeCreditsPerToken[account] == 0 || OUSD.alternativeCreditsPerToken[account] == e18();
111+
112+
/// @title Any account with rebaseState = YieldDelegationSource has a nonZero yieldTo
113+
/// @property Account Invariants
114+
invariant yieldDelegationSourceHasNonZeroYeildTo()
115+
forall address account . OUSD.rebaseState[account] == YieldDelegationSource() => OUSD.yieldTo[account] != 0;
116+
117+
/// @title Any account with rebaseState = YieldDelegationTarget has a nonZero yieldFrom
118+
/// @property Account Invariants
119+
invariant yieldDelegationTargetHasNonZeroYeildFrom()
120+
forall address account . OUSD.rebaseState[account] == YieldDelegationTarget() => OUSD.yieldFrom[account] != 0;
121+
122+
// Helper Invariants
123+
/// @title yieldTo of zero is zero
124+
/// @property Account Invariants
125+
invariant yieldToOfZeroIsZero()
126+
yieldTo(0) == 0;
127+
128+
/// @title yieldFrom of zero is zero
129+
/// @property Account Invariants
130+
invariant yieldFromOfZeroIsZero()
131+
yieldFrom(0) == 0;
132+
133+
/// @title yieldTo of an account can't be the same as the account
134+
/// @property Account Invariants
135+
invariant cantYieldToSelf()
136+
forall address account . OUSD.yieldTo[account] != 0 => OUSD.yieldTo[account] != account;
137+
138+
/// @title yieldFrom of an account can't be the same as the account
139+
/// @property Account Invariants
140+
invariant cantYieldFromSelf()
141+
forall address account . OUSD.yieldFrom[account] != 0 => OUSD.yieldFrom[account] != account;
142+
143+
/// @title Only delegation changes the different effective identity.
144+
/// @property Account Invariants
145+
rule onlyDelegationChangesPairingState(address accountA, address accountB, method f)
146+
filtered{f -> !f.isView}
147+
{
148+
bool different_before = differentAccounts(accountA, accountB);
149+
env e;
150+
calldataarg args;
151+
f(e, args);
152+
bool different_after = differentAccounts(accountA, accountB);
153+
154+
if(delegateMethods(f)) {
155+
satisfy different_before != different_after;
156+
}
157+
assert different_before != different_after => delegateMethods(f);
158+
}

0 commit comments

Comments
 (0)