ERC20
Fungible token on Ethereum
The standard description may be found at this address:
EIPs/eip-20.md at master · ethereum/EIPs
GitHub
erc20.arl
1
archetype erc20
2
3
constant total : nat = 1_000_000_000_000_000
4
variable onetoken : nat = 1_000_000
5
6
asset allowance identified by owner spender {
7
owner : address;
8
spender : address;
9
amount : nat;
10
}
11
12
asset tokenHolder identified by holder {
13
holder : address;
14
tokens : nat = 0;
15
} initialized by {
16
{ holder = caller; tokens = total }
17
}
18
19
entry dotransfer (dest : pkey<tokenHolder>, value : nat) {
20
require {
21
d0 : tokenHolder[caller].tokens >= value
22
}
23
effect {
24
tokenHolder.addupdate( dest, { tokens += value });
25
tokenHolder.update( caller, { tokens -= value })
26
}
27
}
28
29
entry approve(ispender : address, value : nat) {
30
require {
31
d1 : tokenHolder[caller].tokens >= value;
32
}
33
effect {
34
allowance.addupdate((caller, ispender), { amount = value });
35
}
36
}
37
38
entry transferFrom(from_ : address, to_ : address, value : nat) {
39
require {
40
(* d1: allowance.contains(from_); *)
41
d3: allowance[(from_,caller)].amount >= value;
42
d4: tokenHolder[from_].tokens >= value
43
}
44
effect {
45
(* update allowance *)
46
allowance.update((from_,caller), { amount -= value });
47
(* update token *)
48
tokenHolder.addupdate(to_, { tokens += value });
49
tokenHolder.update(from_, { tokens -= value });
50
}
51
}
Copied!
Last modified 1yr ago
Export as PDF
Copy link