ERC20

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 });
  }
}