ERC20

Fungible token on Ethereum

The standard description may be found at this address:

erc20.arl
erc20.arl
archetype erc20
constant total : nat = 1_000_000_000_000_000
variable onetoken : nat = 1_000_000
asset allowance identified by owner spender {
owner : address;
spender : address;
amount : nat;
}
asset tokenHolder identified by holder {
holder : address;
tokens : nat = 0;
} initialized by {
{ holder = caller; tokens = total }
}
entry dotransfer (dest : pkey<tokenHolder>, value : nat) {
require {
d0 : tokenHolder[caller].tokens >= value
}
effect {
tokenHolder.addupdate( dest, { tokens += value });
tokenHolder.update( caller, { tokens -= value })
}
}
entry approve(ispender : address, value : nat) {
require {
d1 : tokenHolder[caller].tokens >= value;
}
effect {
allowance.addupdate((caller, ispender), { amount = value });
}
}
entry transferFrom(from_ : address, to_ : address, value : nat) {
require {
(* d1: allowance.contains(from_); *)
d3: allowance[(from_,caller)].amount >= value;
d4: tokenHolder[from_].tokens >= value
}
effect {
(* update allowance *)
allowance.update((from_,caller), { amount -= value });
(* update token *)
tokenHolder.addupdate(to_, { tokens += value });
tokenHolder.update(from_, { tokens -= value });
}
}
Edit on GitHub