ERC20

Search…
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!
Formal properties
ICO
Last modified 1mo ago
Export as PDF
Copy link
Edit on GitHub