-
Notifications
You must be signed in to change notification settings - Fork 23
/
Model.v
103 lines (82 loc) · 3.08 KB
/
Model.v
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
(*
This file is part of the verified smart contract project of SECBIT Labs.
Copyright 2018 SECBIT Labs
This program is free software: you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public License
as published by the Free Software Foundation, either version 3 of
the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public License
along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
Require Export LibEx.
Require Export Lists.List.
Require Export ZArith.
Require Export Integers.
Require Export String.
Require Export Types.
Require Export Mapping.
Require Export AbsModel.
(*
The state of an fixed-supply ERC20 token contract.
contract FixedSupplyToken is ERC20Interface, Owned {
string public symbol;
string public name;
uint8 public decimals;
uint public _totalSupply;
mapping(address => uint) balances;
mapping(address => mapping(address => uint)) allowed;
...
}
*)
Record state : Type :=
mk_st {
st_symbol: string;
st_name: string;
st_decimals: uint8;
st_totalSupply: uint256;
st_balances: a2v;
st_allowed: aa2v;
}.
Inductive event : Type :=
(* ERC20 events *)
| ev_Transfer (a: address) (from: address) (to: address) (v: value): event
| ev_Approval (a: address) (owner: address) (spender: address) (v: value): event
| ev_EIP20 (a: address) (_initialAmount: uint256) (_tokenName: string)
(_decimalUnits: uint8) (_tokenSymbol: string) : event
(* Return event that models the return value *)
| ev_return (A: Type) (ret: A) : event
| ev_revert (this: address)
.
Definition eventlist := TEventList event.
Definition env := TEnv.
Definition contract := TContract state.
(* Method call *)
Inductive mcall : Type :=
| mc_EIP20 (ia: uint256) (name: string) (dec: uint8) (sym: string) : mcall
| mc_fallback: mcall
| mc_balanceOf (owner: address): mcall
| mc_transfer (to: address) (v: value): mcall
| mc_transferFrom (from: address) (to: address) (v: value): mcall
| mc_approve (spender: address) (v: value): mcall
| mc_allowance (owner: address) (spender: value): mcall
.
(* Message, with a simplication that args are embedded in `m_func`,
instead of calldata *)
Definition message := TMessage mcall.
(* Assume parameters of message calls are in valid ranges. *)
Axiom ctor_totalSupply_inrange:
forall ia name dec sym msg,
msg = mc_EIP20 ia name dec sym -> 0 <= ia /\ ia <= MAX_UINT256.
Axiom transfer_value_inrange:
forall to v msg,
msg = mc_transfer to v -> 0 <= v /\ v <= MAX_UINT256.
Axiom transferFrom_value_inrange:
forall from to v msg,
msg = mc_transferFrom from to v -> 0 <= v /\ v <= MAX_UINT256.
Axiom approve_value_inrange:
forall spender v msg,
msg = mc_approve spender v -> 0 <= v /\ v <= MAX_UINT256.