Formal properties
See presentation article:
Deploy a Verified Implementation of FA1.2 Contract · Digital Assets on Tezos

Declarations

The contract declares two assets:

ledger asset

1
asset ledger identified by holder to big_map {
2
holder : address;
3
tokens : nat = 0;
4
} initialized by {
5
{ holder = caller; tokens = totalsupply }
6
}
Copied!
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

1
asset allowance identified by addr_owner addr_spender to big_map {
2
addr_owner : address;
3
addr_spender : address;
4
amount : nat;
5
}
Copied!
The allowance asset stores the amount of tokens that can be spent by addr_spender on the behalf of addr_owner.

Contract invariant

1
ledger.sum(tokens) = totalsupply
Copied!
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:
1
entry %transfer (%from : address, %to : address, value : nat) {
2
require {
3
r1 otherwise "NotEnoughBalance" : ledger[%from].tokens >= value;
4
}
5
effect {
6
if caller <> %from then (
7
var current = allowance[(%from, caller)].amount;
8
dofailif(current < value, ("NotEnoughAllowance", ((value, current))));
9
allowance.update((%from, caller), { amount -= value });
10
);
11
ledger.update(%from, { tokens -= value });
12
ledger.addupdate(%to, { tokens += value });
13
}
14
}
Copied!

1/ Effect on ledger

1.1/ Effect on %from token holder

1
%from <> %to ->
2
let some before_ledger_from = before.ledger[%from] in
3
let some after_ledger_from = ledger[%from] in
4
after_ledger_from = { before_ledger_from with
5
tokens = abs (before_ledger_from.tokens - value)
6
}
7
otherwise false
8
otherwise false
Copied!
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

1
%from <> %to ->
2
let some after_ledger_to = ledger[%to] in
3
let some before_ledger_to = before.ledger[%to] in
4
after_ledger_to = { before_ledger_to with
5
tokens = (before_ledger_to.tokens + value)
6
}
7
otherwise
8
after_ledger_to = { holder = %to; tokens = value }
9
otherwise false
Copied!
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

1
%from = %to -> ledger = before.ledger
Copied!
No effect on ledger when %from is equal to %to.

1.4/ Unchanged ledger records

1
forall tokenholder in ledger,
2
tokenholder.holder <> %from ->
3
tokenholder.holder <> %to ->
4
before.ledger[tokenholder.holder] = some(tokenholder)
Copied!
Tokenholders other than %from and %to, are not modified nor added to ledger.

1.5/ Removed ledger records

1
removed.ledger.isempty()
Copied!
No record is removed from ledger.

1.6/ Added ledger records

1
let some before_to = before.ledger[%to] in
2
added.ledger.isempty()
3
otherwise
4
added.ledger = [ { holder = %to; tokens = value } ]
Copied!
The added record in 'ledger', if any, is the %to record.

2/ Effect on allowance

2.1/ Effect on (%from,caller) allowance record

1
caller <> %from ->
2
let some before_from_caller = before.allowance[(%from,caller)] in
3
let some after_from_caller = allowance[(%from,caller)] in
4
before_from_caller.amount > value ->
5
after_from_caller = { before_from_caller with
6
amount = abs (before_from_caller.amount - value)
7
}
8
otherwise false
9
otherwise true
Copied!
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

1
caller = %from -> allowance = before.allowance
Copied!
No effect on allowance when caller is equal to %from.

2.2/ Unchanged allowance records

1
forall a in allowance,
2
a.addr_owner <> %from and a.addr_spender <> caller ->
3
before.allowance[(a.addr_owner,a.addr_spender)] = some(a)
Copied!
Allowed amounts other than those associated to %from and caller are identical.

2.3/ Added and removed allowance records

1
removed.allowance.isempty() and added.allowance.isempty()
Copied!
No allowance record is added or removed.

3/ Explicit fail

3.1/ Not Enough Balance

1
fails with (msg : string) :
2
let some after_ledger_from = ledger[%from] in
3
msg = "NotEnoughBalance" and
4
after_ledger_from.tokens < value
5
otherwise true
Copied!
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

1
fails with (msg : string * (nat * nat)) :
2
let some after_allowance_from_caller = allowance[(%from,caller)] in
3
msg = ("NotEnoughAllowance", (value, after_allowance_from_caller.amount)) and
4
caller <> %from and
5
after_allowance_from_caller.amount < value
6
otherwise false
Copied!
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

1
length (operations) = 0
Copied!
No operation generated.

approve

Archetype implementation:
1
entry approve(spender : address, value : nat) {
2
var k = (caller, spender);
3
if allowance.contains(k) then (
4
var previous = allowance[k].amount;
5
dofailif(previous > 0 and value > 0, (("UnsafeAllowanceChange", previous)));
6
);
7
allowance.addupdate( k, { amount = value });
8
}
Copied!

1/ Effect on ledger

1
ledger = before.ledger
Copied!
No effect on ledger.

2/ Effect on allowance

2.1/ Effect on (caller,spender) allowance record

1
let some after_allowance_caller_spender = allowance[(caller,spender)] in
2
let some before_allowance_caller_spender = before.allowance[(caller,spender)] in
3
after_allowance_caller_spender = { before_allowance_caller_spender with
4
amount = value
5
}
6
otherwise
7
after_allowance_caller_spender = {
8
addr_owner = caller;
9
addr_spender = spender;
10
amount = value
11
}
12
otherwise false
Copied!
Allowed amount of tokens spendable by spender on the behalf of caller is set to value.

2.2/ Unchanged allowance records

1
forall a in allowance,
2
(a.addr_owner, a.addr_spender) <> (caller, spender) ->
3
before.allowance[(a.addr_owner, a.addr_spender)] = some(a)
Copied!
Other allowed amounts than the allowed amount of tokens spendable by spender on the behalf of caller, are unchanged.

2.3/ Added allowance records

1
let some allowance_caller_spender = before.allowance[(caller, spender)] in
2
added.allowance.isempty()
3
otherwise
4
added.allowance = [ { addr_owner = caller; addr_spender = spender; amount = value } ]
Copied!
The added allowance record, if any, is the caller and spender one.

2.4/ Removed allowance records

1
removed.allowance.isempty()
Copied!
No record is removed from allowance.

3/ Explicit fail

1
fails with (msg : (string * nat)) :
2
let some allowance_caller_spender = allowance[(caller,spender)] in
3
msg = ("UnsafeAllowanceChange", allowance_caller_spender.amount) and
4
value > 0 and
5
allowance_caller_spender.amount > 0
6
otherwise false
Copied!
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

1
length (operations) = 0
Copied!
No operation generated.

getAllowance

Archetype implementation:
1
getter getAllowance (owner : address, spender : address) : nat {
2
return (allowance[(owner, spender)].amount)
3
}
Copied!

1/ Effect on ledger

1
ledger = before.ledger
Copied!
No effect on ledger.

2/ Effect on allowance

1
allowance = before.allowance
Copied!
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

1
length (operations) = 1
Copied!
Creates one callback operation.

getBalance

Archetype implementation:
1
getter getBalance (owner : address) : nat {
2
return (ledger[owner].tokens)
3
}
Copied!

1/ Effect on ledger

1
ledger = before.ledger
Copied!
No effect on ledger.

2/ Effect on allowance

1
allowance = before.allowance
Copied!
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

1
length (operations) = 1
Copied!
Creates one callback operation.

getTotalSupply

Archetype implementation:
1
getter getTotalSupply () : nat {
2
return totalsupply
3
}
Copied!

1/ Effect on ledger

1
ledger = before.ledger
Copied!
No effect on ledger.

2/ Effect on allowance

1
allowance = before.allowance
Copied!
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

1
length (operations) = 1
Copied!
Creates one callback operation.
Last modified 1yr ago