ERC20

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