-
Notifications
You must be signed in to change notification settings - Fork 40
/
ActiveCurrencies.spec
125 lines (115 loc) · 7 KB
/
ActiveCurrencies.spec
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
methods {
getNextSettleTime(address account) returns (uint40) envfree
getHasDebt(address account) returns (uint8) envfree
getAssetArrayLength(address account) returns (uint8) envfree
getBitmapCurrency(address account) returns (uint16) envfree
getActiveCurrencies(address account) returns (uint144) envfree
getAssetsBitmap(address account) returns (uint256) envfree
transfer(address,uint256) => NONDET
mul(int256,int256) => NONDET
div(int256,int256) => NONDET
}
/* Helper methods for active currencies */
definition getActiveMasked(address account, uint144 index) returns uint144 =
(getActiveCurrencies(account) >> (128 - index * 16)) & 0x00000000000000000000000000000000ffff;
definition getActiveUnmasked(address account, uint144 index) returns uint144 =
(getActiveCurrencies(account) >> (128 - index * 16)) & 0x000000000000000000000000000000003fff;
definition hasCurrencyMask(address account, uint144 index) returns bool =
(getActiveMasked(account, index) & 0x000000000000000000000000000000004000 == 0x000000000000000000000000000000004000);
definition hasValidMask(address account, uint144 index) returns bool =
(getActiveMasked(account, index) & 0x000000000000000000000000000000008000 == 0x000000000000000000000000000000008000) ||
(getActiveMasked(account, index) & 0x000000000000000000000000000000004000 == 0x000000000000000000000000000000004000) ||
(getActiveMasked(account, index) & 0x00000000000000000000000000000000c000 == 0x00000000000000000000000000000000c000);
definition MAX_CURRENCIES() returns uint256 = 0x3fff;
definition MAX_TIMESTAMP() returns uint256 = 2^32 - 1;
// Cannot have timestamps less than 90 days
definition MIN_TIMESTAMP() returns uint256 = 7776000;
/**
* If an account enables a bitmap portfolio it cannot strand assets behind such that the system
* becomes blind to them.
*/
rule enablingBitmapCannotLeaveBehindAssets(address account, uint16 currencyId) {
env e;
require currencyId <= MAX_CURRENCIES();
require e.block.timestamp >= MIN_TIMESTAMP();
require e.block.timestamp <= MAX_TIMESTAMP();
uint16 bitmapCurrencyId = getBitmapCurrency(account);
uint8 assetArrayLength = getAssetArrayLength(account);
uint256 assetsBitmap = getAssetsBitmap(account);
require bitmapCurrencyId != 0 => assetArrayLength == 0;
// Cannot set bitmap currency to 0 if it is already 0, will revert
require bitmapCurrencyId == 0 => currencyId > 0;
// Prevents invalid starting state
require bitmapCurrencyId == 0 => assetsBitmap == 0x0000000000000000000000000000000000000000000000000000000000000000;
enableBitmapForAccount@withrevert(e, account, currencyId, e.block.timestamp);
// In these cases the account has active assets or cash debts
assert (
assetArrayLength != 0 ||
assetsBitmap != 0x0000000000000000000000000000000000000000000000000000000000000000
) => lastReverted;
}
/**
* When a bitmap portfolio is active, it cannot ever have any assets in its array. If this occurs then
* there will be assets that are not accounted for during the free collateral check.
*/
invariant bitmapPortfoliosCannotHaveAssetArray(address account)
getBitmapCurrency(account) != 0 => getAssetArrayLength(account) == 0
/**
* If a bitmap currency is set then it cannot also be in active currencies or it will be considered a duplicate
*/
invariant bitmapCurrencyIsNotDuplicatedInActiveCurrencies(address account, uint144 i)
0 <= i && i < 9 && getActiveUnmasked(account, i) != 0 && hasCurrencyMask(account, i) =>
getActiveUnmasked(account, i) != getBitmapCurrency(account)
{
preserved with (env e) {
require getBitmapCurrency(account) <= MAX_CURRENCIES();
// no duplicates in active currencies
requireInvariant bitmapCurrencyIsNotDuplicatedInActiveCurrencies(account, 0);
requireInvariant bitmapCurrencyIsNotDuplicatedInActiveCurrencies(account, 1);
requireInvariant bitmapCurrencyIsNotDuplicatedInActiveCurrencies(account, 2);
requireInvariant bitmapCurrencyIsNotDuplicatedInActiveCurrencies(account, 3);
requireInvariant bitmapCurrencyIsNotDuplicatedInActiveCurrencies(account, 4);
requireInvariant bitmapCurrencyIsNotDuplicatedInActiveCurrencies(account, 5);
requireInvariant bitmapCurrencyIsNotDuplicatedInActiveCurrencies(account, 6);
requireInvariant bitmapCurrencyIsNotDuplicatedInActiveCurrencies(account, 7);
requireInvariant bitmapCurrencyIsNotDuplicatedInActiveCurrencies(account, 8);
requireInvariant activeCurrenciesAreNotDuplicatedAndSorted(account, 0, 1);
requireInvariant activeCurrenciesAreNotDuplicatedAndSorted(account, 1, 2);
requireInvariant activeCurrenciesAreNotDuplicatedAndSorted(account, 2, 3);
requireInvariant activeCurrenciesAreNotDuplicatedAndSorted(account, 3, 4);
requireInvariant activeCurrenciesAreNotDuplicatedAndSorted(account, 4, 5);
requireInvariant activeCurrenciesAreNotDuplicatedAndSorted(account, 5, 6);
requireInvariant activeCurrenciesAreNotDuplicatedAndSorted(account, 6, 7);
requireInvariant activeCurrenciesAreNotDuplicatedAndSorted(account, 7, 8);
}
}
/**
* Active currency flags are always sorted and cannot be double counted, if this occurs then there
* will be currencies that are double counted during the free collateral check.
*
* This check ensures that any two indexes of the active currencies byte vector are not duplicated
* and sorted properly.
*/
invariant activeCurrenciesAreNotDuplicatedAndSorted(address account, uint144 i, uint144 j)
(0 <= i && j == i + 1 && j < 9) =>
// If the current slot is zero then the next slot must also be zero
(
getActiveMasked(account, i) == 0 ? getActiveMasked(account, j) == 0 :
(
// The next slot may terminate
getActiveMasked(account, j) == 0 ||
// Or it may have a value which must be greater than the current value
(getActiveUnmasked(account, i) < getActiveUnmasked(account, j))
)
) {
preserved with (env e) {
requireInvariant activeCurrenciesAreNotDuplicatedAndSorted(account, 0, 1);
requireInvariant activeCurrenciesAreNotDuplicatedAndSorted(account, 1, 2);
requireInvariant activeCurrenciesAreNotDuplicatedAndSorted(account, 2, 3);
requireInvariant activeCurrenciesAreNotDuplicatedAndSorted(account, 3, 4);
requireInvariant activeCurrenciesAreNotDuplicatedAndSorted(account, 4, 5);
requireInvariant activeCurrenciesAreNotDuplicatedAndSorted(account, 5, 6);
requireInvariant activeCurrenciesAreNotDuplicatedAndSorted(account, 6, 7);
requireInvariant activeCurrenciesAreNotDuplicatedAndSorted(account, 7, 8);
}
}