-
Notifications
You must be signed in to change notification settings - Fork 20
/
ERC20.spec
91 lines (71 loc) · 3.02 KB
/
ERC20.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
/**
* # ERC20 Example
*
* This is an example specification for a generic ERC20 contract. It contains several
* simple rules verifying the integrity of the transfer function.
* To run, execute the following command in terminal:
*
* certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
*
* One of the rules here is badly phrased, and results in an erroneous fail.
* Understand the counter example provided by the Prover and then run the fixed
* spec:
*
* certoraRun ERC20.sol --verify ERC20:ERC20Fixed.spec --solc solc8.0
*/
// The methods block below gives various declarations regarding solidity methods.
methods
{
// When a function is not using the environment (e.g., `msg.sender`), it can be
// declared as `envfree`
function balanceOf(address) external returns (uint) envfree;
function allowance(address,address) external returns(uint) envfree;
function totalSupply() external returns (uint) envfree;
}
/** @title Transfer must move `amount` tokens from the caller's
* account to `recipient`
*/
rule transferSpec(address recipient, uint amount) {
env e;
// `mathint` is a type that represents an integer of any size
mathint balance_sender_before = balanceOf(e.msg.sender);
mathint balance_recip_before = balanceOf(recipient);
transfer(e, recipient, amount);
mathint balance_sender_after = balanceOf(e.msg.sender);
mathint balance_recip_after = balanceOf(recipient);
// Operations on mathints can never overflow nor underflow
assert balance_sender_after == balance_sender_before - amount,
"transfer must decrease sender's balance by amount";
assert balance_recip_after == balance_recip_before + amount,
"transfer must increase recipient's balance by amount";
}
/// @title Transfer must revert if the sender's balance is too small
rule transferReverts(address recipient, uint amount) {
env e;
require balanceOf(e.msg.sender) < amount;
transfer@withrevert(e, recipient, amount);
assert lastReverted,
"transfer(recipient,amount) must revert if sender's balance is less than `amount`";
}
/** @title Transfer must not revert unless
* - the sender doesn't have enough funds,
* - or the message value is nonzero,
* - or the recipient's balance would overflow,
* - or the message sender is 0,
* - or the recipient is 0
*/
rule transferDoesntRevert(address recipient, uint amount) {
env e;
require balanceOf(e.msg.sender) > amount;
require e.msg.value == 0; // No payment
// This requirement prevents overflow of recipient's balance.
// We convert `max_uint` to type `mathint` since:
// 1. a sum always returns type `mathint`, hence the left hand side is `mathint`,
// 2. `mathint` can only be compared to another `mathint`
require balanceOf(recipient) + amount < to_mathint(max_uint);
// Recall that `address(0)` is a special address that in general should not be used
require e.msg.sender != 0;
require recipient != 0;
transfer@withrevert(e, recipient, amount);
assert !lastReverted;
}