-
Notifications
You must be signed in to change notification settings - Fork 3
/
Model.csp
182 lines (161 loc) · 7.07 KB
/
Model.csp
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
//@@Curve Compound Pool Deposit@@
// Pool tokens: USDC, DAI; cCrv, cUSDC, cDAI
// Key protocols: Curve, Compound; Maker
#include "C:\Users\User\Desktop\Compound.csp";
#include "C:\Users\User\Desktop\Curve_cPool.csp";
// Accounts indexes
#define user 0;
#define curveDeposit 1;
#define compCUSDC 2;
#define curveSwap 3;
#define compBorrower 4;
#define exchanger 5;
#define compUser 6;
// Token indexes
#define USDC 0;
#define DAI 1;
#define cUSDC 0;
#define cDAI 1;
// Supplementary functions and values
IncreaseBlockNum() = blockMined{currentBlockNumber = currentBlockNumber + 1;} -> Skip;
// Compound Protocol
// Minting/removing cTokens; borrowing tokens from Compound
//var compSupplied = 200;
var redeemAmt;
var initAmt;
var compProfit;
Compound_Depositor(compSupplied) = tau{initAmt = USDC_balances[compUser];} ->
tx(USDC_approveF,compUser,[compCUSDC, compSupplied, 0, 0]);
tx(mintF,compUser,[compSupplied,0,0,0]);
tau{redeemAmt = cUSDC_accountTokens[compUser];} ->
tx(redeemF, compUser, [redeemAmt,0,0,0]);
tau{compProfit = USDC_balances[compUser] - initAmt;} -> Skip;
var borrowedAmount;
var returnedAmount;
Compound_Borrower() = tau{borrowedAmount = USDC_balances[compCUSDC];} -> // the borrowerAmount causes over-utilization
tx(borrowF, compBorrower, [borrowedAmount,0,0,0]);
tau{returnedAmount = borrowedAmount * 2;} ->
tx(USDC_approveF, compBorrower, [compCUSDC, returnedAmount, 0, 0]);
tx(repayF, compBorrower, [returnedAmount,0,0,0]);
// Curve Protocol Depositor and Exchanger
//var suppliedTokens = [10000, 0];
var suppliedTokens = 10000;
var minMintTokens = 8000;
var add; var remove;
Curve_Depositor() = tx(USDC_approveF, user, [curveDeposit, suppliedTokens,0,0]);
tx(add_liquidity, user, [suppliedTokens,minMintTokens,0,0]);
tau{add = cCrv_balances[user]; remove = add * 5 / 10;} ->
tx(cCrv_approveF, user, [curveDeposit,add,0,0]);
tx(remove_liquidity, user, [add,0,0,0]);
var minSwap;
Curve_Exchanger(i) = Curve_Exchanger_USDC(i) <> Curve_Exchanger_DAI(i);
Curve_Exchanger_USDC(i) = tau{minSwap = 1;} ->
(tx(cUSDC_approveF, exchanger, [curveSwap,i,0,0]);
tx(exchange, exchanger, [USDC,DAI,i,minSwap]));
Curve_Exchanger_DAI(i) = tau{minSwap = 1;} ->
(tx(cDAI_approveF, exchanger, [curveSwap,i,0,0]);
tx(exchange, exchanger,[DAI,USDC,i,minSwap]));
System() = Curve_Depositor() ||| Compound_Depositor(5000) ||| Compound_Borrower() ||| IncreaseBlockNum() ||| Curve_Exchanger(90000000);
Reverting() = atomic {
tau{swapBalances = pre_swapBalances;
exchangeRates = pre_exchangeRates;
cCrv_balances = pre_cCrv_balances;
cCrv_allowed = cCrv_allowed;
cCrv_totalSupply = pre_cCrv_totalSupply;
USDC_balances = pre_USDC_balances;
USDC_allowed = pre_USDC_allowed;
DAI_balances = pre_DAI_balances;
DAI_allowed = pre_DAI_allowed;
cUSDC_accountTokens = pre_cUSDC_accountTokens;
cUSDC_allowed = pre_cUSDC_allowed;
cDAI_accountTokens = pre_cDAI_accountTokens;
cDAI_allowed = pre_cDAI_allowed;
cUSDC_totalSupply = pre_cUSDC_totalSupply;
cDAI_totalSupply = pre_cDAI_totalSupply;
accountBorrows = pre_accountBorrows;
totalBorrows = pre_totalBorrows;
totalReserves = pre_totalReserves;
totalCash = pre_totalCash;
borrowRate = pre_borrowRate;
borrowIndex = pre_borrowIndex;
currentBlockNumber = pre_currentBlockNumber;
cCrv_sum = call(sum,cCrv_balances);
cUSDC_sum = call(sum,cUSDC_accountTokens);
cDAI_sum = call(sum,cDAI_accountTokens);
USDC_sum = call(sum,USDC_balances);
DAI_sum = call(sum,DAI_balances);
} -> STATE_REVERTED -> Skip
};
tx(function,sender,params) = atomic {
tau{pre_swapBalances = swapBalances;
pre_exchangeRates = exchangeRates;
pre_cCrv_balances = cCrv_balances;
pre_cCrv_allowed = cCrv_allowed;
pre_cCrv_totalSupply = cCrv_totalSupply;
pre_USDC_balances = USDC_balances;
pre_USDC_allowed = USDC_allowed;
pre_DAI_balances = DAI_balances;
pre_DAI_allowed = DAI_allowed;
pre_cUSDC_accountTokens = cUSDC_accountTokens;
pre_cUSDC_allowed = cUSDC_allowed;
pre_cDAI_accountTokens = cDAI_accountTokens;
pre_cDAI_allowed = cDAI_allowed;
pre_cUSDC_totalSupply = cUSDC_totalSupply;
pre_cDAI_totalSupply = cDAI_totalSupply;
pre_accountBorrows = accountBorrows;
pre_totalBorrows = totalBorrows;
pre_totalReserves = totalReserves;
pre_totalCash = totalCash;
pre_borrowRate = borrowRate;
pre_borrowIndex = borrowIndex;
pre_currentBlockNumber = currentBlockNumber;
} ->
case {
function == add_liquidity: Curve_addLiquidity(params[0], params[1], sender)
function == remove_liquidity: Curve_remove_liquidity_one_coin(params[0], params[1], sender)
function == borrowF: cUSDC_borrow(params[0], sender)
function == mintF: cUSDC_mint(params[0], sender)
function == repayF: cUSDC_repayBorrow(params[0], sender)
function == redeemF: cUSDC_redeem(params[0], sender)
function == USDC_approveF: USDC_approve(params[0], params[1], sender)
function == cCrv_approveF: cCrv_approve(params[0], params[1], sender)
function == cUSDC_approveF: cUSDC_approve(params[0], params[1], sender)
function == cDAI_approveF: cDAI_approve(params[0], params[1], sender)
function == exchange: Curve_swap_exchange(params[0], params[1], params[2], params[3], sender)
default: Skip
}
};
// Properties
#assert System() deadlockfree;
#define positiveUnderlying suppliedTokens > 0;
#define positiveMintedCrv cCrv_mintAmount > 0;
#define positiveMintedComp mintTokens > 0;
#define cCrv_balanceInv cCrv_sum == cCrv_totalSupply;
#define DAI_balanceInv DAI_sum == DAI_totalSupply;
#define USDC_balanceInv USDC_sum == USDC_totalSupply;
#define cDAI_balanceInv cDAI_sum == cDAI_totalSupply;
#define cUSDC_balanceInv cUSDC_sum == cUSDC_totalSupply;
#define smallLoss loss <= suppliedTokens / 10;
#define incrExchange prevExchangeRate <= newExchangeRate;
#define nonnegativeProfit compProfit >= 0;
#define negativeProfit compProfit < 0;
#define positiveLoss loss > 0;
#define negativeLoss loss < 0;
#assert System() |=[] (AddLiquidity -> []smallLoss);
#assert System() |=[](positiveUnderlying -> <>(positiveMintedComp && positiveMintedCrv));
#assert System() |=[] (cCrv_balanceInv && DAI_balanceInv && USDC_balanceInv && cDAI_balanceInv && cUSDC_balanceInv);
#assert System() |=[] cCrv_balanceInv;
#assert System() |=[] incrExchange;
#assert System() |=[] (Mint.cUSDC -> []nonnegativeProfit);
#assert System() reaches nonnegativeProfit with min(compProfit);
#assert System() reaches nonnegativeProfit with max(compProfit);
#assert System() reaches negativeProfit with min(compProfit);
#assert System() reaches positiveLoss with max(loss);
#assert System() reaches positiveLoss with min(loss);
#assert System() reaches negativeLoss with max(loss);
#assert System() reaches negativeLoss with min(loss);
#assert ERC20_Approve() refines Test_Approve();
#assert Test_Approve() refines ERC20_Approve();
// An example of an ERC20 token standard conformance checking
ERC20_Approve() = approval.0.1.200 -> Skip;
Test_Approve() = USDC_approve(1,200,0) [] cUSDC_approve(1,200,0) [] DAI_approve(1,200,0) [] cDAI_approve(1,200,0) [] cCrv_approve(1,200,0);