ERC20
The one and only
The standard may be found at this address:
erc20.arl
1
archetype erc20
2
3
constant name : string = "mytoken"
4
5
constant total : int = 1000
6
with {
7
i0: total > 0
8
}
9
10
asset allowance {
11
allowed : address;
12
amount : int;
13
} with {
14
i2 : amount > 0;
15
}
16
17
asset tokenHolder identified by holder {
18
holder : address;
19
tokens : int;
20
allowances : allowance collection;
21
} with {
22
i1: tokens >= 0;
23
i3: allowances.sum(the.amount) <= tokens;
24
} initialized by [
25
{ holder = caller; tokens = total; allowances = [] }
26
]
27
28
action dotransfer (dest : pkey of tokenHolder, value : int) {
29
30
specification {
31
p1 : before.tokenHolder.sum(tokens) = tokenHolder.sum(tokens);
32
p2 : let some th = tokenHolder.get(dest) in
33
let some bth = before.tokenHolder.get(dest) in
34
th.tokens = bth.tokens + value
35
otherwise true
36
otherwise true;
37
p3 : let some thc = tokenHolder.get(caller) in
38
let some bthc = before.tokenHolder.get(caller) in
39
thc.tokens = bthc.tokens - value
40
otherwise true
41
otherwise true;
42
p4 : let some th = tokenHolder.get(dest) in
43
forall t in tokenHolder,
44
forall bt in before.tokenHolder,
45
t.holder <> th.holder ->
46
t.holder <> caller ->
47
t.tokens = bt.tokens
48
otherwise true;
49
}
50
51
failif {
52
f0 : value < 0;
53
f1 : tokenHolder.get(caller).tokens < value
54
}
55
56
effect {
57
tokenHolder.update( tokenHolder.get(dest).holder, { tokens += value });
58
tokenHolder.update( caller, { tokens -= value })
59
}
60
}
Copied!
Last modified 1mo ago
Export as PDF
Copy link
Edit on GitHub