/
structs.spec
181 lines (153 loc) · 6.56 KB
/
structs.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
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
/**
* @title Structs Example
*
* This is an example reasoning about structs.
* The spec contains examples for:
* 1. Referencing a struct and its fields.
* 2. method block including methods passing structs as arguments and returning structs.
* 3. method block entry for a default getter.
* 4. method block entry returning a struct as a tuple.
* 5. structs in cvl functions - passing and returning.
* 6. struct as a parameter of preserved function.
*/
using Bank as bank; // bank is the same as currentContract.
methods {
/// Definition of a user-defined solidity method returning a struct
function getCustomer(address a) external returns(BankAccountRecord.Customer) envfree;
/// Definition of a function with struct as an argument
function addCustomer(BankAccountRecord.Customer) external envfree;
function balanceOf(address) external returns(uint) envfree;
function balanceOfAccount(address, uint) external returns(uint) envfree;
function totalSupply() external returns(uint) envfree;
function getNumberOfAccounts(address) external returns (uint256) envfree;
function isCustomer(address) external returns (bool) envfree;
}
/**
Comparison of full structs is not supported. Each field should be compared instead.
Here only the id field is compared because arrays (accounts field) cannot be compared.
*/
function integrityOfCustomerInsertion(BankAccountRecord.Customer c1) returns bool {
addCustomer(c1);
BankAccountRecord.Customer c = getCustomer(c1.id);
return (c.id == c1.id);
}
/**
Calling a solidity method returning a struct.
@param a - customer's address
@param accountId - account number
*/
function getAccount(address a, uint256 accountInd) returns BankAccountRecord.BankAccount {
BankAccountRecord.Customer c = bank.getCustomer(a);
return c.accounts[accountInd];
}
/// returning a struct as a tuple.
function getAccountNumberAndBalance(address a, uint256 accountInd) returns (uint256, uint256) {
env e;
BankAccountRecord.Customer c = getCustomer(a);
BankAccountRecord.BankAccount account = getAccount(e.msg.sender, accountInd);
return (account.accountNumber, account.accountBalance) ;
}
/**
You can define rule parameters of a user defined type.
*/
rule correctCustomerInsertion(BankAccountRecord.Customer c1){
bool correct = integrityOfCustomerInsertion(c1);
assert (correct, "Bad customer insertion");
}
/// Example for assigning to a tuple.
rule updateOfBlacklist() {
env e;
address user;
address user1;
uint256 account;
uint256 account1;
uint256 ind = addToBlackList(e, user, account);
user1 = currentContract.blackList[ind].id;
account1 = currentContract.blackList[ind].account;
assert (user == user1 && account == account1, "Customer in black list is not the one added.");
}
/// Example for struct parameter and nested struct member reference
rule witnessForIntegrityOfTransferFromCustomerAccount(BankAccountRecord.Customer c) {
env e;
uint256 accountNum;
address to;
uint256 toAccount;
require c.accounts[accountNum].accountBalance > 0;
transfer(e, to, assert_uint256(c.accounts[accountNum].accountBalance/2), accountNum, toAccount);
satisfy c.accounts[accountNum].accountBalance < balanceOfAccount(to, toAccount);
}
/// Assignment to a struct.
/// The term getCustomer(a).id is not supported yet.
rule integrityOfCustomerKeyRule(address a, method f) {
env e;
calldataarg args;
BankAccountRecord.Customer c = getCustomer(a);
require c.id == a || c.id == 0;
f(e,args);
assert c.id == a || c.id == 0;
}
/// Represent the sum of all accounts of all users
/// sum _customers[a].accounts[i].accountBalance
persistent ghost mathint sumBalances {
init_state axiom sumBalances == 0;
}
/// Mirror on a struct _customers[a].accounts[i].accountBalance
persistent ghost mapping(address => mapping(uint256 => uint256)) accountBalanceMirror {
init_state axiom forall address a. forall uint256 i. accountBalanceMirror[a][i] == 0;
}
/// Number of accounts per user
ghost mapping(address => uint256) numOfAccounts {
// assumption: it's infeasible to grow the list to these many elements.
axiom forall address a. numOfAccounts[a] < max_uint256;
init_state axiom forall address a. numOfAccounts[a] == 0;
}
/// Store hook to synchronize numOfAccounts with the length of the customers[KEY address a].accounts array.
hook Sstore _customers[KEY address user].accounts.length uint256 newLength {
if (newLength > numOfAccounts[user])
require accountBalanceMirror[user][require_uint256(newLength-1)] == 0 ;
numOfAccounts[user] = newLength;
}
/**
An internal step check to verify that our ghost works as expected, it should mirror the number of accounts.
Once the sload is defined, this invariant becomes a tautology
*/
invariant checkNumOfAccounts(address user)
numOfAccounts[user] == bank.getNumberOfAccounts(user);
/// This Sload is required in order to eliminate adding unintializaed account balance to sumBalances.
hook Sload uint256 length _customers[KEY address user].accounts.length {
require numOfAccounts[user] == length;
}
/// hook on a complex data structure, a mapping to a struct with a dynamic array
hook Sstore _customers[KEY address a].accounts[INDEX uint256 i].accountBalance uint256 new_value (uint old_value) {
require old_value == accountBalanceMirror[a][i]; // Need this inorder to sync on insert of new element
sumBalances = sumBalances + new_value - old_value ;
accountBalanceMirror[a][i] = new_value;
}
/// Sload on a struct field.
hook Sload uint256 value _customers[KEY address a].accounts[INDEX uint256 i].accountBalance {
// when balance load, safely assume it is less than the sum of all values
require to_mathint(value) <= sumBalances;
require to_mathint(i) <= to_mathint(numOfAccounts[a]-1);
}
/// Non-customers have no account.
invariant emptyAccount(address user)
!isCustomer(user) => (
getNumberOfAccounts(user) == 0 &&
(forall uint256 i. accountBalanceMirror[user][i] == 0 )) ;
/// struct as a parameter of preserved function.
invariant totalSupplyEqSumBalances()
to_mathint(totalSupply()) == sumBalances
{
preserved addCustomer(BankAccountRecord.Customer c)
{
requireInvariant emptyAccount(c.id);
}
}
/// Comparing nativeBalances of current contract.
invariant solvency()
totalSupply() <= nativeBalances[currentContract] {
// safely assume that Bank doesn't call itself
preserved with (env e){
require e.msg.sender != currentContract;
}
}