FA 1.2

archetype fa12
​
constant totalsupply : nat = 10_000_000
​
asset allowance identified by addr_owner addr_spender to big_map {
  addr_owner       : address;
  addr_spender     : address;
  amount           : nat;
}
​
asset ledger identified by holder to big_map {
  holder     : address;
  tokens     : nat = 0;
} initialized by {
  { holder = caller; tokens = totalsupply }
}
​
entry %transfer (%from : address, %to : address, value : nat) {
  require {
    r1 otherwise "NotEnoughBalance" : ledger[%from].tokens >= value;
  }
  effect {
    if caller <> %from then (
      var current = allowance[(%from, caller)].amount;
      dofailif(current < value, ("NotEnoughAllowance", ((value, current))));
      allowance.update((%from, caller), { amount -=  value });
    );
    ledger.update(%from, { tokens -= value });
    ledger.addupdate(%to, { tokens += value });
  }
}
​
entry approve(spender : address, value : nat) {
  var k = (caller, spender);
  if allowance.contains(k) then (
    var previous = allowance[k].amount;
    dofailif(previous > 0 and value > 0, (("UnsafeAllowanceChange", previous)));
  );
  allowance.addupdate( k, { amount = value });
}
​
getter getAllowance (owner : address, spender : address) : nat {
  return (allowance[(owner, spender)].amount)
}
​
getter getBalance (owner : address) : nat {
  return (ledger[owner].tokens)
}
​
getter getTotalSupply () : nat {
  return totalsupply
}
​
///////////////////////////////////////////////////////////////////////////////
// SPECIFICATION
///////////////////////////////////////////////////////////////////////////////
​
specification {
  s1: ledger.sum(tokens) = totalsupply;
}
​
specification entry %transfer (%from : address, %to : address, value : nat) {
  fails {
    f0 with (msg : string) :
      let some after_ledger_from = ledger[%from] in
        msg = "NotEnoughBalance" and
        after_ledger_from.tokens < value
      otherwise true;
    f1 with (msg : string * (nat * nat)) :
      let some after_allowance_from_caller = allowance[(%from,caller)] in
        msg = ("NotEnoughAllowance", ((value, after_allowance_from_caller.amount))) and
        caller <> %from and
        after_allowance_from_caller.amount < value
      otherwise false;
  }
  // LEDGER ASSET
  postcondition transfer_p1 { // effect on %from nbtokens
    %from <> %to ->
    let some before_ledger_from = before.ledger[%from] in
    let some after_ledger_from  = ledger[%from] in
    after_ledger_from = { before_ledger_from with
      tokens = abs(before_ledger_from.tokens - value)
    }
    otherwise false otherwise false
  }
  postcondition transfer_p2 { // effect on %to nbtokens
    %from <> %to ->
    let some after_ledger_to = ledger[%to] in
    let some before_ledger_to = before.ledger[%to] in
      after_ledger_to = { before_ledger_to with
        tokens = before_ledger_to.tokens + value
      }
    otherwise
      after_ledger_to = { holder = %to; tokens = value }
    otherwise false // %to ledger asset exists after transfer
  }
  postcondition transfer_p3 {
    %from = %to -> ledger = before.ledger
  }
  postcondition transfer_p4 { // other ledger assets are unchanged
    forall tokenholder in ledger,
      tokenholder.holder <> %from ->
      tokenholder.holder <> %to ->
      let some before_th = before.ledger[tokenholder.holder] in
        tokenholder = before_th
      otherwise false // no other ledger is added
  }
  postcondition transfer_p5 { // no ledger asset is removed
    removed.ledger.isempty()
  }
  postcondition transfer_p6 { // number of added asset may be one
    let some before_to = before.ledger[%to] in
      added.ledger.isempty()
    otherwise
      added.ledger = [ { holder = %to; tokens = value } ]
  }
  // ALLOWANCE ASSET
  postcondition transfer_p7 { // effect on allowance
    caller <> %from ->
    let some before_from_caller = before.allowance[(%from,caller)] in
    let some after_from_caller = allowance[(%from,caller)] in
      before_from_caller.amount > value ->
      after_from_caller = { before_from_caller with
        amount = abs(before_from_caller.amount - value)
      }
    otherwise false
    otherwise true
  }
  postcondition transfer_p8 { // effect on allowance
    caller = %from -> allowance = before.allowance
  }
  postcondition transfer_p9 { // other allowance assets are unchanged
    forall a in allowance,
      a.addr_owner <> %from and a.addr_spender <> caller ->
      let some before_a = before.allowance[(a.addr_owner, a.addr_spender)] in
        a = before_a
      otherwise true
  }
  postcondition transfer_p10 { // no allowance is added or removed
    removed.allowance.isempty() and added.allowance.isempty()
  }
}
​
specification entry approve(spender : address, value : nat) {
  fails {
    f2 with (msg : (string * nat)) :
      let some allowance_caller_spender = allowance[(caller, spender)] in
        msg = ("UnsafeAllowanceChange", allowance_caller_spender.amount) and
        value > 0 and
        allowance_caller_spender.amount > 0
      otherwise false;
  }
  postcondition approve_p1 { // effect on allowance asset
    let some after_allowance_caller_spender = allowance[(caller,spender)] in
    let some before_allowance_caller_spender = before.allowance[(caller,spender)] in
      after_allowance_caller_spender = { before_allowance_caller_spender with
        amount = value
      }
    otherwise
      after_allowance_caller_spender = { addr_owner = caller; addr_spender = spender; amount = value }
    otherwise false
  }
​
  postcondition approve_p2 { // other allowance assets are unchanged
    forall a in allowance,
      (a.addr_owner, a.addr_spender) <> (caller, spender) ->
      let some before_a = before.allowance[(a.addr_owner, a.addr_spender)] in
        a = before_a
      otherwise false // no other allowance asset is added
  }
​
  postcondition approve_p3 { // added allowance
    let some allowance_caller_spender = before.allowance[(caller, spender)] in
      added.allowance.isempty()
    otherwise
      added.allowance = [ { addr_owner = caller; addr_spender = spender; amount = value } ]
  }
​
  postcondition approve_p4 { // no allowance asset is removed
    removed.allowance.isempty()
  }
​
  postcondition approve_p5 {
    ledger = before.ledger
  }
}
​
specification getter getAllowance (owner : address, spender : address) {
  postcondition getallowance_p1 { // creates one op
    length (operations) = 1
  }
  postcondition getallowance_p2 { // assets are unchanged
    ledger = before.ledger and allowance = before.allowance
  }
}
​
specification getter getBalance (owner : address) {
  postcondition getbalance_p1 { // creates one op
    length (operations) = 1
  }
  postcondition getbalance_p2 { // assets are unchanged
    ledger = before.ledger and allowance = before.allowance
  }
}
​
specification getter getTotalSupply () {
  postcondition gettotalsupply_p1 { // creates one op
    length (operations) = 1
  }
  postcondition gettotalsupply_p2 { // assets are unchanged
    ledger = before.ledger and allowance = before.allowance
  }
}
​