-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathToken.etiml
224 lines (198 loc) · 10.7 KB
/
Token.etiml
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
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
pragma etiml ^0.1
structure Pervasive = struct
fun addBy b a = a + b
fun subBy b a = a - b
fun orBy b a = a || b
(* fun waste_time () = 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 *)
(* fun for_ ['a] {m1 m2: Time} {m1' m2' start : Nat} {eend : Nat | start <= eend} (start : nat {start}, eend : nat {eend}, init : 'a, f : forall {i : Nat | start <= i /\ i < eend} using (m1, m1'), nat {i} * 'a -- m2, m2' --> 'a) return 'a using (m1+m2+3281.0)*$(eend-start)+3970.0, (m1'+m2'+52*32)*(eend-start)+50*32 = *)
(* lets *)
(* fun loop {i : Nat | start <= i /\ i <= eend} (i : nat {i}, acc : 'a) (* using (m1+m2) * $(eend-i), (m1'+m2') * (eend-i) *) = *)
(* ifi i #>= eend then (* waste_time (); *) acc *)
(* else *)
(* %loop (i #+ #1, %f (i, acc)) using (m1+m2+3281.0) * $(eend-i)+1651.0, (m1'+m2'+52*32) * (eend-i)+16*32 *)
(* end *)
(* in *)
(* %loop (start, init) *)
(* end *)
fun require b = if b then (* waste_time (); *)() else (throw using _) end
end
interface tokenRecipient = sig
public fun receiveApproval (_from : address, _value : uint256, _token : address, _extraData : bytes)
end
contract TokenERC20 = struct
(* Public variables of the token *)
public state name : vector uint256
public state symbol : vector uint256
(* public val decimals = #18 *)
public val decimals = #0
(* 18 decimals is the strongly suggested default, avoid changing it *)
public state totalSupply : cell uint256
(* This creates an array with all balances *)
public state balanceOf : map address uint256
public state allowance : map address (map address uint256)
(* This generates a public event on the blockchain that will notify clients *)
event Transfer(indexed from : address, indexed to : address, value : uint256)
(* This notifies clients about the amount burnt *)
event Burn(indexed from : address, value : uint256)
(* (* PW: here is a limitation of TiML: it can't parametrize on states. MicroTiML actually supports it (for continuations), so TiML should support it too. *) *)
(* fun for_name ['a] {m1 m2: Time} {m1' m2' start : Nat} {eend : Nat | start <= eend} (start : nat {start}, eend : nat {eend}, init : 'a, f : forall {j : Nat | start <= j /\ j < eend} using (m1, m1'), funtype pre {name : j} post {name : j+1} nat {j} * 'a -- m2, m2' --> 'a) pre {name : start} post {name : eend} return 'a (* using (m1+m2+3281.0)*$(eend-start)+3970.0, (m1'+m2'+52)*(eend-start)+50 *) = *)
(* lets *)
(* fun loop {i : Nat | start <= i /\ i <= eend} (i : nat {i}, acc : 'a) pre {name : i} post {name : eend} (* using (m1+m2) * $(eend-i), (m1'+m2') * (eend-i) *) = *)
(* ifi i #>= eend then (* waste_time (); *)acc asc_state {name : eend} *)
(* else *)
(* @loop {i+1} (i #+ #1, @f {i} (i, acc)) using (m1+m2+3281.0) * $(eend-i)+1651.0, (m1'+m2'+52*32) * (eend-i)+16*32 *)
(* end *)
(* in *)
(* %loop (start, init) *)
(* end *)
(* fun copy_name {old len : Nat} (s : array uint256 {len}) pre {name : old} post {name : len} = *)
(* vector_clear name; *)
(* %for_name (#0, array_len s, (), fn {i | 0 <= i /\ i < len} (i : nat {i}, ()) pre {name : i} post {name : i+1} => *)
(* push_back (name, array_get(s, i)) *)
(* ) *)
(* fun for_symbol ['a] {m1 m2: Time} {m1' m2' start : Nat} {eend : Nat | start <= eend} (start : nat {start}, eend : nat {eend}, init : 'a, f : forall {j : Nat | start <= j /\ j < eend} using (m1, m1'), funtype pre {symbol : j} post {symbol : j+1} nat {j} * 'a -- m2, m2' --> 'a) pre {symbol : start} post {symbol : eend} return 'a using (m1+m2+3281.0)*$(eend-start)+3970.0, (m1'+m2'+52*32)*(eend-start)+50*32 = *)
(* lets *)
(* fun loop {i : Nat | start <= i /\ i <= eend} (i : nat {i}, acc : 'a) pre {symbol : i} post {symbol : eend} (* using (m1+m2) * $(eend-i), (m1'+m2') * (eend-i) *) = *)
(* ifi i #>= eend then (* waste_time (); *)acc asc_state {symbol : eend} *)
(* else *)
(* @loop {i+1} (i #+ #1, @f {i} (i, acc)) using (m1+m2+3281.0) * $(eend-i)+1651.0, (m1'+m2'+52*32) * (eend-i)+16*32 *)
(* end *)
(* in *)
(* %loop (start, init) *)
(* end *)
(* fun copy_symbol {old len : Nat} (s : array uint256 {len}) pre {symbol : old} post {symbol : len} = *)
(* vector_clear symbol; *)
(* %for_symbol (#0, array_len s, (), fn {i | 0 <= i /\ i < len} (i : nat {i}, ()) pre {symbol : i} post {symbol : i+1} => *)
(* push_back (symbol, array_get(s, i)) *)
(* ) *)
(**
* Constructor function
*
* Initializes contract with initial supply tokens to the creator of the contract
*)
public fun constructor {old1 old2 len1 len2 : Nat} (
initialSupply : uint256,
tokenName : array uint256 {len1},
tokenSymbol : array uint256 {len2}
) (* pre {name : old1, symbol : old2} post {name : len1, symbol : len2} *) =
totalSupply ::= initialSupply * ((10 #** decimals) using _); (* Update total supply with the decimal amount *)
set balanceOf[msg.sender] !!totalSupply (* Give the creator all initial tokens *)
(* %copy_name tokenName; (* Set the name for display purposes *) *)
(* %copy_symbol tokenSymbol (* Set the symbol for display purposes *) *)
(** *)
(* * Internal transfer, only can be called by this contract *)
(* *)
internal fun _transfer (_from : address, _to : address, _value : uint) using _ =
(* Prevent transfer to 0x0 address. Use burn() instead *)
require(1=1);
require(_to <> 0x0);
(* Check if the sender has enough *)
require(balanceOf[_from] >= _value);
(* Check for overflows *)
require(balanceOf[_to] + _value > balanceOf[_to]);
(* Save this for an assertion in the future *)
let previousBalances = balanceOf[_from] + balanceOf[_to];
(* Subtract from the sender *)
modify balanceOf[_from] -= _value;
(* Add the same to the recipient *)
modify balanceOf[_to] += _value;
(* emit Transfer(_from, _to, _value); *)
(* Asserts are used to use static analysis to find bugs in your code. They should never fail *)
require(balanceOf[_from] + balanceOf[_to] = previousBalances)
(* (* (* assert2(balanceOf[_from] + balanceOf[_to] = previousBalances) *) *) *)
(* assert2(1=1) *)
(* * Transfer tokens *)
(* * *)
(* * Send `_value` tokens to `_to` from your account *)
(* * *)
(* * @param _to The address of the recipient *)
(* * @param _value the amount to send *)
public fun transfer (_to : address, _value : uint256) =
_transfer(msg.sender, _to, _value)
(* ; (_to, _value, msg.sender, balanceOf[msg.sender], balanceOf[_to]) *)
(* * Transfer tokens from other address *)
(* * *)
(* * Send `_value` tokens to `_to` on behalf of `_from` *)
(* * *)
(* * @param _from The address of the sender *)
(* * @param _to The address of the recipient *)
(* * @param _value the amount to send *)
public fun transferFrom (_from : address, _to : address, _value : uint256) =
require(_value <= allowance[_from][msg.sender]); (* Check allowance *)
modify allowance[_from][msg.sender] -= _value;
_transfer(_from, _to, _value);
true
(* (_from, _to, _value, msg.sender, allowance[_from][msg.sender], balanceOf[_from], balanceOf[_to]) *)
(* * Set allowance for other address *)
(* * *)
(* * Allows `_spender` to spend no more than `_value` tokens on your behalf *)
(* * *)
(* * @param _spender The address authorized to spend *)
(* * @param _value the max amount they can spend *)
public fun approve (_spender : address, _value : uint256) =
set allowance[msg.sender][_spender] _value;
true
(* (msg.sender, _spender, _value, allowance[msg.sender][_spender]) *)
(** *)
(* * Set allowance for other address and notify *)
(* * *)
(* * Allows `_spender` to spend no more than `_value` tokens on your behalf, and then ping the contract about it *)
(* * *)
(* * @param _spender The address authorized to spend *)
(* * @param _value the max amount they can spend *)
(* * @param _extraData some extra information to send to the approved contract *)
(* *)
public fun approveAndCall (_spender : address, _value : uint256(* , _extraData : bytes *)) =
let spender = attach _spender tokenRecipient;
if approve(_spender, _value) then
call spender receiveApproval(msg.sender, _value, this, _extraData);
true
else false end
(* ; (msg.sender, _spender, _value, allowance[msg.sender][_spender]) *)
(** *)
(* * Destroy tokens *)
(* * *)
(* * Remove `_value` tokens from the system irreversibly *)
(* * *)
(* * @param _value the amount of money to burn *)
(* *)
public fun burn (_value : uint256) =
require(balanceOf[msg.sender] >= _value); (* Check if the sender has enough *)
modify balanceOf[msg.sender] -= _value; (* Subtract from the sender *)
modify totalSupply -= _value; (* Updates totalSupply *)
(* emit Burn(msg.sender, _value); *)
true
(* (msg.sender, _value, balanceOf[msg.sender], !!totalSupply) *)
(** *)
(* * Destroy tokens from other account *)
(* * *)
(* * Remove `_value` tokens from the system irreversibly on behalf of `_from`. *)
(* * *)
(* * @param _from the address of the sender *)
(* * @param _value the amount of money to burn *)
(* *)
public fun burnFrom (_from : address, _value : uint256) =
require(balanceOf[_from] >= _value); (* Check if the targeted balance is enough *)
require(_value <= allowance[_from][msg.sender]); (* Check allowance *)
modify balanceOf[_from] -= _value; (* Subtract from the targeted balance *)
modify allowance[_from][msg.sender] -= _value; (* Subtract from the sender's allowance *)
modify totalSupply -= _value; (* Update totalSupply *)
(* emit Burn(_from, _value); *)
true
(* (msg.sender, _from, _value, balanceOf[_from], !!totalSupply, allowance[_from][msg.sender]) *)
val () = %constructor (0xa0, {}, {})
(* val _ = transfer (0x246, 0x80) *)
(* val () = set allowance[0x246][0x8888] 0x50 *)
(* val _ = transferFrom (0x246, 0x123, 0x20) *)
(* val _ = burnFrom (0x246, 0x20) *)
(* val _ = approve (0x123, 0x80) *)
(* val _ = burn 0x20 *)
(* val _ = approveAndCall (0x123, 0x80) *)
(* val () = dispatch {transfer = transfer, *)
(* transferFrom = transferFrom, *)
(* approve = approve, *)
(* approveAndCall = approveAndCall, *)
(* burn = burn, *)
(* burnFrom = burnFrom, *)
(* } *)
end