-
Notifications
You must be signed in to change notification settings - Fork 19
/
EIP20Token.v
178 lines (152 loc) · 6.83 KB
/
EIP20Token.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
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
(** * EIP20 Token Implementation *)
(**
This file contains an implementation of the EIP 20 Token Specification (https://eips.ethereum.org/EIPS/eip-20).
The implementation is essentially a port of
https://github.com/ConsenSys/Tokens/blob/fdf687c69d998266a95f15216b1955a4965a0a6d/contracts/eip20/EIP20.sol
*)
From Coq Require Import ZArith_base.
From Coq Require Import List. Import ListNotations.
From ConCert.Execution Require Import Monad.
From ConCert.Execution Require Import ResultMonad.
From ConCert.Execution Require Import Serializable.
From ConCert.Execution Require Import Blockchain.
From ConCert.Execution Require Import Containers.
From ConCert.Execution Require Import ContractCommon.
From ConCert.Utils Require Import Extras.
From ConCert.Utils Require Import RecordUpdate.
(** * Contract types *)
Section EIP20Token.
Context {BaseTypes : ChainBase}.
Set Nonrecursive Elimination Schemes.
Definition TokenValue := N.
Open Scope N_scope.
Open Scope bool.
Inductive Msg :=
| transfer : Address -> TokenValue -> Msg
| transfer_from : Address -> Address -> TokenValue -> Msg
| approve : Address -> TokenValue -> Msg.
Record State :=
build_state {
total_supply : TokenValue;
balances : AddressMap.AddrMap TokenValue;
allowances : AddressMap.AddrMap (AddressMap.AddrMap TokenValue)
}.
Record Setup :=
build_setup {
owner : Address;
init_amount : TokenValue;
}.
Definition Error : Type := nat.
Definition default_error : Error := 1%nat.
(* begin hide *)
MetaCoq Run (make_setters State).
MetaCoq Run (make_setters Setup).
Section Serialization.
Global Instance setup_serializable : Serializable Setup :=
Derive Serializable Setup_rect <build_setup>.
Global Instance msg_serializable : Serializable Msg :=
Derive Serializable Msg_rect <transfer, transfer_from, approve>.
Global Instance state_serializable : Serializable State :=
Derive Serializable State_rect <build_state>.
End Serialization.
(* end hide *)
Definition error {T : Type} : result T Error :=
Err default_error.
(** * Contract functions *)
(** ** init *)
(** Initialize contract storage *)
Definition init (chain : Chain)
(ctx : ContractCallContext)
(setup : Setup)
: result State Error :=
Ok {| total_supply := setup.(init_amount);
balances := AddressMap.add setup.(owner)
setup.(init_amount)
AddressMap.empty;
allowances := AddressMap.empty
|}.
Definition increment_balance (m : AddressMap.AddrMap TokenValue)
(addr : Address)
(inc : TokenValue)
: AddressMap.AddrMap TokenValue :=
match AddressMap.find addr m with
| Some old => AddressMap.add addr (old + inc) m
| None => AddressMap.add addr inc m
end.
(** ** transfer *)
(** Transfers [amount] tokens, if [from] has enough tokens to transfer *)
Definition try_transfer (from : Address)
(to : Address)
(amount : TokenValue)
(state : State)
: result State Error :=
let from_balance := with_default 0 (AddressMap.find from state.(balances)) in
if from_balance <? amount
then error
else let new_balances := AddressMap.add from (from_balance - amount) state.(balances) in
let new_balances := increment_balance new_balances to amount in
Ok (state<|balances := new_balances|>).
(** ** transfer_from *)
(** The delegate tries to transfer [amount] tokens from [from] to [to].
Succeeds if [from] has indeed allowed the delegate to spend at least [amount] tokens on its behalf. *)
Definition try_transfer_from (delegate : Address)
(from : Address)
(to : Address)
(amount : TokenValue)
(state : State)
: result State Error :=
do from_allowances_map <- result_of_option (AddressMap.find from state.(allowances)) default_error ;
do delegate_allowance <- result_of_option (AddressMap.find delegate from_allowances_map) default_error ;
let from_balance := with_default 0 (AddressMap.find from state.(balances)) in
if (delegate_allowance <? amount) || (from_balance <? amount)
then error
else let new_allowances := AddressMap.add delegate (delegate_allowance - amount) from_allowances_map in
let new_balances := AddressMap.add from (from_balance - amount) state.(balances) in
let new_balances := increment_balance new_balances to amount in
Ok (state<|balances := new_balances|><|allowances ::= AddressMap.add from new_allowances|>).
(** ** approve *)
(** The caller approves the delegate to transfer up to [amount] tokens on behalf of the caller *)
Definition try_approve (caller : Address)
(delegate : Address)
(amount : TokenValue)
(state : State)
: result State Error :=
match AddressMap.find caller state.(allowances) with
| Some caller_allowances =>
Ok (state<|allowances ::= AddressMap.add caller (AddressMap.add delegate amount caller_allowances)|>)
| None =>
Ok (state<|allowances ::= AddressMap.add caller (AddressMap.add delegate amount AddressMap.empty)|>)
end.
(** ** receive *)
(** Contract entrypoint function *)
Open Scope Z_scope.
Definition receive (chain : Chain)
(ctx : ContractCallContext)
(state : State)
(maybe_msg : option Msg)
: result (State * list ActionBody) Error :=
let sender := ctx.(ctx_from) in
(** Only allow calls with no money attached *)
if ctx.(ctx_amount) >? 0
then error
else
match maybe_msg with
| Some (transfer to amount) =>
without_actions (try_transfer sender to amount state)
| Some (transfer_from from to amount) =>
without_actions (try_transfer_from sender from to amount state)
| Some (approve delegate amount) =>
without_actions (try_approve sender delegate amount state)
(** transfer actions to this contract are not allowed *)
| None => error
end.
Close Scope Z_scope.
Definition contract : Contract Setup Msg State Error :=
build_contract init receive.
(* sum of all balances in the token state *)
Definition sum_balances (state : EIP20Token.State) :=
sumN (fun '(k, v) => v) (FMap.elements (balances state)).
Definition get_allowance state from delegate :=
with_default 0 (FMap.find delegate (with_default
(@FMap.empty (FMap Address TokenValue) _) (FMap.find from (allowances state)))).
End EIP20Token.