Formal properties

See presentation article:
Deploy a Verified Implementation of FA1.2 Contract · Digital Assets on Tezos
## Introduction
assets.tqtezos.com
Declarations
The contract declares two assets:
ledger asset
asset ledger identified by holder to big_map {
  holder     : address;
  tokens     : nat = 0;
} initialized by {
  { holder = caller; tokens = totalsupply }
}
The ledger asset is the cap table: it holds the number of tokens for each token holder. totalsupply is the initial number of tokens held by the originator of the contract.
allowance asset
asset allowance identified by addr_owner addr_spender to big_map {
  addr_owner       : address;
  addr_spender     : address;
  amount           : nat;
}
The allowance asset stores the amount of tokens that can be spent by addr_spender on the behalf of addr_owner.
Contract invariant
ledger.sum(tokens) = totalsupply
No token is minted: the total number of tokens is equal to the initial totalsupply number of tokens, regardless of the state of the storage.
transfer
Archetype implementation:
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 });
  }
}
1/ Effect on ledger
1.1/ Effect on %from token holder
%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
When the %to address is different from the %from address, the number of tokens %to possesses is decread by value.
1.2/ Effect on %to token holder
%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
When the %to address is different from the %from address, the number of tokens %to possesses is increased by value when %to is already registered in the ledger, and set to value otherwise. Anyway, %to is registered in ledger.
1.3/ No effect on ledger
%from = %to -> ledger = before.ledger
No effect on ledger when %from is equal to %to.
1.4/ Unchanged ledger records
forall tokenholder in ledger,
tokenholder.holder <> %from ->
tokenholder.holder <> %to ->
before.ledger[tokenholder.holder] = some(tokenholder)
Tokenholders other than %from and %to, are not modified nor added to ledger.
1.5/ Removed ledger records
removed.ledger.isempty()
No record is removed from ledger.
1.6/ Added ledger records
let some before_to = before.ledger[%to] in
  added.ledger.isempty()
otherwise
  added.ledger = [ { holder = %to; tokens = value } ]
The added record in 'ledger', if any, is the %to record.
2/ Effect on allowance
2.1/ Effect on (%from,caller) allowance record
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
When caller is different from %from, the amount caller is authorised to spend on the behalf of %from is decreased by value if value is striclty greated than the authorized amount.
2.1/ No effect on allowance
caller = %from -> allowance = before.allowance
No effect on allowance when caller is equal to %from.
2.2/ Unchanged allowance records
forall a in allowance,
a.addr_owner <> %from and a.addr_spender <> caller ->
before.allowance[(a.addr_owner,a.addr_spender)] = some(a)
Allowed amounts other than those associated to %from and caller are identical.
2.3/ Added and removed allowance records
removed.allowance.isempty() and added.allowance.isempty()
No allowance record is added or removed.
3/ Explicit fail
3.1/ Not Enough Balance
fails with (msg : string) :
  let some after_ledger_from = ledger[%from] in
    msg = "NotEnoughBalance" and
    after_ledger_from.tokens < value
  otherwise true
When the entry fails with message "NotEnoughBalance", value is stricly greater than the number of tokens of %to. Cannot spend more than you own.
3.2/ Not Enough Allowance
fails 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
When the entry fails with message "NotEnoughAllowance", caller is different from %from and value is stricly greater than the allowed amount for %from and caller. A spender cannot spend more than allowed.
4/ Effect on operations
length (operations) = 0
No operation generated.
approve
Archetype implementation:
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 });
}
1/ Effect on ledger
ledger = before.ledger
No effect on ledger.
2/ Effect on allowance
2.1/ Effect on (caller,spender) allowance record
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
Allowed amount of tokens spendable by spender on the behalf of caller is set to value.
2.2/ Unchanged allowance records
forall a in allowance,
(a.addr_owner, a.addr_spender) <> (caller, spender) ->
before.allowance[(a.addr_owner, a.addr_spender)] = some(a)
Other allowed amounts than the allowed amount of tokens spendable by spender on the behalf of caller, are unchanged.
2.3/ Added allowance records
let some allowance_caller_spender = before.allowance[(caller, spender)] in
  added.allowance.isempty()
otherwise
  added.allowance = [ { addr_owner = caller; addr_spender = spender; amount = value } ]
The added allowance record, if any, is the caller and spender one.
2.4/ Removed allowance records
removed.allowance.isempty()
No record is removed from allowance.
3/ Explicit fail
fails 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
When the entry fails with message "UnsafeAllowanceChange", value is strictly greater than 0 and the allowed amount of tokens spendable by spender on the behalf of caller is not equal to zero.
Note that in that case, it may be set back to 0 by having spender call the transfer entry to transfer a number of tokens equal to the remaining allowed amount, from the approver address (ie caller above) to the approver address (ie to itself).
Indeed, according to properties 1.3 and 2.1 of the transfer entry, this has no effect on ledger and sets allowance record to 0.
4/ Effect on operations
length (operations) = 0
No operation generated.
getAllowance
Archetype implementation:
getter getAllowance (owner : address, spender : address) : nat {
  return (allowance[(owner, spender)].amount)
}
1/ Effect on ledger
ledger = before.ledger
No effect on ledger.
2/ Effect on allowance
allowance = before.allowance
No effect on allowance.
3/ Explicit fail
No explicit fail. The entry implicitely fails though if the provided callback is invalid.
4/ Effect on operations
length (operations) = 1
Creates one callback operation.
getBalance
Archetype implementation:
getter getBalance (owner : address) : nat {
  return (ledger[owner].tokens)
}
1/ Effect on ledger
ledger = before.ledger
No effect on ledger.
2/ Effect on allowance
allowance = before.allowance
No effect on allowance.
3/ Explicit fail
No explicit fail. The entry implicitely fails though if the provided callback is invalid.
4/ Effect on operations
length (operations) = 1
Creates one callback operation.
getTotalSupply
Archetype implementation:
getter getTotalSupply () : nat {
  return totalsupply
}
1/ Effect on ledger
ledger = before.ledger
No effect on ledger.
2/ Effect on allowance
allowance = before.allowance
No effect on allowance.
3/ Explicit fail
No explicit fail. The entry implicitely fails though if the provided callback is invalid.
4/ Effect on operations
length (operations) = 1
Creates one callback operation.
FA 1.2
ERC20
Last updated 3 weeks ago