FA1.2 Approvable Ledger, formal verification by Nomadic Labs

Introduction

Overview

We’d like to describe a recent verification effort at Nomadic Labs, namely:

• A formalisation in Coq of the FA1.2 standard;
• verification in Coq of the formal correctness of three FA1.2 smart contracts with respect to this formalisation; and
• a description of what we learned from our effort, and of the changes and updates made to the standard and the implementations, following our checks.

Background, precise links, and definitions of technical terms¹ follow below. Here are the Coq files:

• The GitLab Merge Request of the verification effort (also the corresponding GitLab branch).
• A snapshot of this GitLab branch on Software Heritage. All relevant code links in this blog post will point here.
• The FA1.2 interface
• The FA1.2 specification
• Per-contract proof file for the camlCase implementation
• Per-contract proof file for the Edukera implementation
• Per-contract proof file for the Dexter 2 implementation

Background: ledgers as smart contracts

Most blockchains have a native token. Tezos has tez; Bitcoin has bitcoin; and Ethereum has ether. These tokens can be used to store value, just like fiat currency.² Tezos has no other primitive tokens — but it has smart contracts, which gives flexibility to create further tokens and more generally to store value in novel ways.

In fact, Tezos can express any token you can imagine: just code a smart contract to keep a ledger of who owns your token and how much, and invoke your contract on the Tezos blockchain. Et voilà: you have a new token on the Tezos blockchain, whose ownership is represented as a ledger state in your smart contract, along with whatever other functionalities you imagined and implemented — e.g. to convert between ledger entries and USD, like USDtz.

However, to do this in a scalable and uniform manner, we need interoperability standards to which such smart contracts can adhere. Enter the FA1.2 standard:

The FA1.2 standard

What FA1.2 is

The FA1.2 standard is a standard for smart contracts implementing token ledgers on the Tezos blockchain.³ The FA1.2 standard is a plain English document (i.e. not code, but a description of what code should do), officially registered as Tezos Improvement Proposal (TZIP) number 7.⁴

An FA1.2-compliant smart contract implements a ledger that maps owners to account balances (just like a bank ledger maps account owners to account balances), and offers entrypoints (described below) to get balances, approve transfers,⁵ and so forth, satisfying certain properties as stated in the standard.

For the rest of this blog post, we may write FA1.2 contract as shorthand for “a smart contract that satisfies the FA1.2 standard”.

Entrypoints of an FA1.2 smart contract

An FA1.2-compliant smart contract has (at least) the following five entrypoints:

1. %transfer expects a from account, a to account, and an amount of tokens to be transferred, and updates the ledger accordingly.
2. %approve expects an owner, a spender, and a new allowance for the spender, and updates the approvals accordingly.
3. %getBalance expects an owner and returns (via a callback) the owner’s balance.
4. %getAllowance expects an owner, a spender, and returns (via a callback) the approved allowance for the spender.
5. %getTotalSupply returns (again via a callback) the total sum of all balances in the ledger.

The list above is non-exclusive: an FA1.2 contract can include other entrypoints — e.g. for burning and minting tokens, or managing an administrator — but it’s the entrypoints listed above that gives a smart contract the property of being “an FA1.2 smart contract”.

We will call the last three entrypoints — %getBalance, %getAllowance, and %getTotalSupply — view entrypoints; in OOP we might call them getter methods. The view entrypoints will become particularly interesting later on in this post, because thanks to our verification work we discovered an ambiguity in their specification.

Examples of FA1.2 contracts

Examples of live FA1.2 contracts include:

1. ETHtz, a token wrapping Ether (ETH) (dapp)
2. The USD-pegged stablecoin USDtz (dapp)
3. Wrapped Bitcoin tzBTC (dapp)
4. A liquidity ledger that is part of the Dexter 2 system.

A word on Dexters 1 and 2: Dexter is a smart contract to enable trade between tez — the Tezos blockchain’s native token — and any FA1.2 token. In the current, live version of Dexter (call it Dexter 1 in this blog post⁶) the liquidity ledger is integrated in the main contract in a manner that does not conform to FA1.2. Dexter 2 is a forthcoming replacement of Dexter 1 which includes various improvements, including a modular internal architecture which includes a distinct, FA1.2-compliant, liquidity ledger. Dexter 2’s liquidity ledger is the contract that has been verified in this work.

Furthermore, two FA1.2 contracts exist that are not themselves live on the blockchain but which exist as code made freely available and open-source for anyone to build on and deploy:

1. an FA1.2 contract by camlCase written in Morley, and
2. an FA1.2 contract by Edukera written in Archetype (see also pretty-printed code).

So several FA1.2-compliant ledgers exist for the Tezos blockchain:

• ledgers in ETHtz, USDtz, and tzBTC;
• an internal ledger used by the Dexter 2 smart contract; and
• a pair of general-purpose ledger implementations, one by camlCase and one by Edukera.

This makes sense, because keeping a ledger is a basic functionality.

Two important questions

Two questions now arise:

1. Are the ledgers above correctly implemented: does the implementation comply with the FA1.2 standard?

   The technical term for this is (formal) correctness. Just because an implementation says

   “I am a smart contract implementing an FA1.2-compliant token ledger”

   does not mean it is one. The implementation might contain an error.

2. Is the FA1.2 standard itself correct and unambiguous?

   Just because a standard says

   “I am a standard”

   does not mean that it is one. The FA1.2 standard is a plain English document. This could contain an error, ambiguity, or omission.

We should answer

• Question 2 (correctness of the standard) before
• Question 1 (correctness of an implementation with respect to a formalisation of that standard),

since we should check that a standard makes sense before we formalise it and check that an implementation is formally correct with respect to this formalisation!⁷

The FA1.2 standard formalised

Formalising “FA1.2 standard” as “FA1.2 interface” + “FA1.2 spec”

To answer Question 2 above, we at Nomadic Labs wrote some code in the Coq proof assistant, as follows:

1. The FA1.2 interface.

   This asserts internal (intensional) structure which the smart contract must support, along with axioms on its behaviour.

   An FA1.2-compliant smart contract may support other internal structure too. And why is a file regarding intensional behaviour called an interface? Because it provides an abstract interface to the implementation’s storage and parameter types; see a note below.

2. The FA1.2 specification.

   This specifies how FA1.2 entrypoints interact with the internal structure of the FA1.2 interface. An FA1.2-compliant smart contract may contain more entrypoints than those specified in the FA1.2 standard.

3. There is also an FA12 verification file, which collects lemmas proved purely from the interface and specification files. More on this later.

So: we translated the English FA1.2 standard into a pair of Coq file and some corollaries — the first concerning intensional structure, the second concerning extensional behaviour, and the third collecting their consequences when put together — and we can write the following informal equation:

We now discuss the components on the right-hand side of this equation, in more detail.

We start with the FA1.2 interface, which is as discussed a collection of Coq module types that does two things: provide an abstract interface of an FA1.2 implementation’s storage and parameter types; and impose axiomatic requirements on its behaviour.

We discuss each in turn:

The FA1.2 interface (functions)

The FA1.2 interface posits the following getters and setters over an FA1.2 implementation’s storage:

1. a function getBalance to return an owner’s balance, or return zero if the owner does not have a balance in the ledger (getBalance is a totalising wrapper around an underlying partial function getBalanceOpt);⁸
2. a function getAllowance to return an owner’s allowance for a spender, or zero if the spender is not recorded as having an allowance with the owner (again, this is a wrapper for an underlying getAllowanceOpt);
3. a function setBalance and a function setAllowance to modify the corresponding data; and
4. a function getTotalSupply to obtain the total sum of all tokens in the ledger.

Here that is again as Coq code:

getBalance      : data storage_ty -> data address -> data nat (** is wrapper for ... **)
getBalanceOpt   : data storage_ty -> data address -> data (option nat)
getAllowance    : data storage_ty -> data address -> data address -> data nat
getAllowanceOpt : data storage_ty -> data address -> data address -> data (option nat)
setBalance      : data storage_ty -> data address -> data nat -> data storage_ty
setAllowance    : data storage_ty -> data address -> data address -> 
                                  data nat -> data storage_ty
getTotalSupply  : data storage_ty -> data nat

For experts: data above is a wrapper that turns a Michelson type into a Coq type. To be more precise, it is a Coq function that translates an underlying Mi-Cho-Coq representation of Michelson types, to a type data in Coq.

Note that

• the functions getBalance, getAllowance, setBalance, setAllowance, and getTotalSupply might be present in the smart contract’s source code as explicit internal functions — e.g. one way to write an FA1.2-compliant smart contract is to use a smart contracts language that is a functional language and allows us to actually write these functions — but also
• these functions might be implicitly definable from the basic datatypes of the implementation, but not explicitly represented as such — e.g. perhaps the smart contract is written in a low-level language that simply does not have functions.

Part of the power of the interface is that it makes this distinction not matter so much: in the rest of the verification we can operate as if getBalance exists, even if it’s only implicit.

The FA1.2 interface (axioms)

The FA1.2 interface also imposes axioms on the getters and setters above. For example:

Example axiom 1

setBalance to amount, followed by getBalance, should return the amount. In Coq:

Parameter getBalance_setBalance_eq : forall sto owner amount,
      getBalance (setBalance sto owner amount) owner = amount. 

Example axiom 2

Setting a balance of one owner must leave the balances of other owners unchanged:

Parameter getBalance_setBalance_neq : forall sto owner owner' amount,
  owner <> owner' ->
  getBalance (setBalance sto owner amount) owner' =
  getBalance sto owner'.

For experts: Example axioms 1 and 2 state that the ledger is an abstract array.

Example axiom 3

Setting an allowance for an owner and a spender must have no impact on anyone’s balance values:

Parameter getAllowance_setAllowance_eq : forall sto owner spender amount,
  getAllowance (setAllowance sto owner spender amount) owner spender =
    amount.

Summary

So: the FA1.2 interface is Coq code, not English. Like the FA1.2 standard from which it derives, the FA1.2 interface abstracts away from smart contract implementation details to allow us to carry out aspects of the verification once and for all, in an implementation-independent manner.

With this in hand, we can conveniently state the FA1.2 specification:

The FA1.2 specification

The FA1.2 specification specifies how smart contract entrypoints should invoke functions specified in the FA1.2 interface — in other words, it specifies the effect of executing FA1.2 entrypoints in terms of the abstract view of the contract given by the interface.

Excerpts from here and here:

(** Entry point: ep_getBalance *)
    Definition ep_getBalance
               (p : data parameter_ep_getBalance_ty)
               (sto : data storage_ty)
               (ret_ops :  data (list operation))
               (ret_sto :  data storage_ty) :=
      let '(owner, callback) := p in
      let balance := getBalance sto owner in
      let op := transfer_tokens env nat balance (amount env) callback in
      ret_sto = sto /\ ret_ops = [op].

Here, we specify in ep_getBalance that the behavior of the %getBalance entrypoint is equivalent to retrieving the balance of the owner (using the getBalance getter provided by the interface) and sending it to callback, through the emission of a transfer operation.

The specification looks like code but it’s not: it specifies required entrypoints and their parameters and behaviour, but treats them as opaque structures, the internal composition of which we do not examine.

Three FA1.2 smart contract implementions verified

Having written the FA1.2 interface and specification just discussed, we verified formal correctness with respect to them, of three FA1.2 smart contract implementations:

1. an FA1.2 contract by camlCase,
2. an FA1.2 contract by Edukera (pretty-printed code), and
3. the Dexter 2 FA1.2 implementation.

Edukera had already checked their implementation using a different methodology. Both the contract and its specification are written in the Archetype language and converted by the Archetype compiler into a collection of proof obligations. These proof obligations are subsequently solved using the verification platform Why3 by means of SMT solvers.

Nevertheless, we decided to carry out the verification of the Edukera contract in Coq to put our approach to the test: if the two verification efforts yield the same result, namely a formal proof of correctness, we have a basis for comparison; if not, we investigate any discrepancies.

Examples of implementational differences

The three implementations maintain internal storage differently:

Map of approved balances / ledger of balances

In the Edukera and Dexter 2 implementations, the map of approved allowances across owners is stored separately from the ledger of balances. The Edukera storage is

storage (pair (big_map %allowance (pair address address) nat)
              (big_map %ledger address nat))

and the Dexter 2 storage is

storage (pair (big_map %tokens address nat)
              (pair (big_map %allowances (pair (address %owner) (address %spender)) nat)
        (pair (address %admin) (nat %total_supply))))

In contrast, the camlCase implementation maintains one big map mapping an owner to a pair whose first component is the owner’s balance and the second component is a map of the owner’s approved allowances:

storage (pair (big_map %accounts address
                                 (pair (nat :balance)
                                       (map :approvals address
                                                       nat)))
              (nat %fields));

(In the code above, %fields corresponds to the total supply.)

Thus, the Edukera and Dexter 2 contracts admit an account that is absent from the ledger — not even with a zero balance — yet has approved spenders in the map of allowances.

In the camlCase contract this cannot happen as there is no global map of allowances separate from the ledger; instead, each owner maintains its own map of allowances.

Additional entrypoints

Contracts providing functionalities beyond the FA1.2 standard may have additional fields in their storage. For instance, the Dexter 2 contract has a field called %admin for an administrator account.

Admin is the only account allowed to burn and/or mint tokens in Dexter 2, using an additional %mintOrBurn entrypoint. The Edukera and camlCase implementations have no entrypoints aside from those specified in the FA1.2 interface.

Guarantees provided by formal correctness

Correctness with respect to the FA1.2 interface and specification ensures that certain things are guaranteed, regardless of any implementational differences. For example:

Sum of balances is unchanged

If an implementation is correct, then regardless of

• the specific form of storage, or
• whether or not there are any additional entrypoints,

each of the five FA1.2 entrypoints must leave the total sum of balances unchanged.⁹

This is in a file fa12_verification, which consists of a number of useful lemmas and a culminating Theorem sumOfAllBalances_constant.

This theorem is checked once-and-for-all, purely from an assumption that the smart contract is FA1.2-compliant — no need to re-run the proof for each implementation; no need even to look at the implementation code (once we have proved that it is FA1.2-compliant).

Storage Validity

The FA1.2 standard states (in English) that the %getTotalSupply entrypoint must return the total sum of all tokens in the ledger.¹⁰

The FA1.2 interface posits a function getTotalSupply : data storage_ty -> data nat, and the FA1.2 specification requires that that the value returned by the FA1.2 %getTotalSupply entrypoint is equal to the value we get by calling getTotalSupply directly (in other words: the specification insists that the %getTotalSupply entrypoint is equivalent to calling the getTotalSupply function directly on the storage).

However this in itself does not guarantee that the getTotalSupply function actually returns the sum of all tokens. This must be checked on a per-implementation basis, as we now discuss.

The FA1.2 interface defines a storageValid predicate —

Definition storageValid sto :=
    getTotalSupply sto = sumOfAllBalances sto.

But in an implementation we are unlikely to see this summation directly implemented in code, since it is impractical to recompute the total sum of all balances every time the %getTotalSupply entrypoint is invoked —- depending on the implementation language, the data structures may not even permit this iteration (i.e. not foldable), so that the language abstractions might make such a sum impossible to even express (e.g. big map).

Thus, the total supply is stored as a separate field in the storage and updated as tokens are burned or minted. The camlCase and Dexter 2 implementations do this. The Edukera implementation does too but since it provides no options for burning or minting tokens, it just sets total supply to a large constant number: constant totalsupply : nat = 10_000_000.

Now to prove formal correctness we must prove that storageValid is indeed valid:

• camlCase
• Edukera
• Dexter 2

The proofs of these properties are quite long, and this is where some real work has to happen: we have to actually read the implementation and prove in Coq that storageValid — the equality between the value returned by %getTotalSupply and the total sum of all tokens — is maintained as a dynamic invariant preserved by all of the contract’s entrypoints. This includes entrypoints that are not required by the FA1.2 standard, e.g. entrypoints for minting and burning tokens, if any.

In practice, most of the work was already done by the sumOfAllBalances_constant theorem previously discussed. Of the three contracts we considered only the the Dexter 2 contract has an additional entrypoint. Yes this is handled using bespoke reasoning, but even so this reasoning mostly just calls generic lemmas from the fa12_verification file which we mentioned above.

All entrypoints are present

The FA1.2 parameter identifies the entrypoint to be invoked and provides the arguments to go along with the specified entrypoint. The abstract FA1.2 interface requires an implementation to provide a method

extract_fa12_ep : data parameter_ty -> data (option fa12_parameter_ty)

that maps an entrypoint of the implementation to a corresponding entrypoint in the FA1.2 standard. It is partial (the “option” in option fa12_parameter_ty) because the implementation may have additional entrypoints that do not correspond to any FA1.2 entrypoint.

We then require that each FA1.2 entrypoint has a corresponding entrypoint in the implementation — and hence that the implementation is indeed an implementation of FA1.2:

Parameter ep_transfer_required : forall (q : data parameter_ep_transfer_ty),
  exists p, extract_fa12_ep p = Some (inl (inl q)).

Parameter ep_approve_required : forall (q : data parameter_ep_approve_ty),
  exists p, extract_fa12_ep p = Some (inl (inr q)).

Parameter ep_getAllowance_required : forall (q : data parameter_ep_getAllowance_ty),
  exists p, extract_fa12_ep p = Some (inr (inl q)).

Parameter ep_getBalance_required : forall (q : data parameter_ep_getBalance_ty),
  exists p, extract_fa12_ep p = Some (inr (inr (inl q))).

Parameter ep_getTotalSupply_required : forall (q : data parameter_ep_getTotalSupply_ty),
  exists p, extract_fa12_ep p = Some (inr (inr (inr q))).

The %approve entrypoint is correct

The specification for the %approve entrypoint guarantees that the storage returned by the contract is obtained from the initial storage by calling setAllowance with the owner, spender, and amount arguments accompanying the call to %approve.

Here’s the Coq code:

(** Entry point: ep_approve *)
Definition ep_approve
           (p : data parameter_ep_approve_ty)
           (sto : data storage_ty)
           (ret_ops : data (list operation))
           (ret_sto : data storage_ty) :=
  let '(spender, new_allowance) := p in
  (sender = spender /\ ret_sto = sto) \/
  let current_allowance := getAllowance sto sender spender in
  (current_allowance = 0%N \/ new_allowance = 0%N) /\
  ret_sto = setAllowance sto sender spender new_allowance.

Underspecification

The FA1.2 standard is underspecified by design. For example:

• The standard imposes no restriction on the operations returned by the %transfer and %approve entrypoints — since e.g. a contract may need to invoke calls to another contract to access the contents of its ledger, if these are stored remotely.
• A contract may contain entrypoints other than those mentioned in the standard (e.g. to mint and burn tokens).

Just because such details are not fully specified in FA1.2 does not mean we can ignore them in our verification effort! We saw one instance of this above: an obviously necessary requirement that every entrypoint must preserve storage validity — even if the entrypoint is not mentioned in the FA1.2 standard. Thus, the FA1.2 standard requires (explicitly or implicitly) some invariants which may apply to all of an implementation, even if — especially if — that implementation has extra bells and whistles.¹¹

So for each particular implementation, we formulate an additional specification file describing in more detail relevant behaviour of the implementation’s entrypoints:

• camlCase per-implementation file
• Edukera per-implementation file
• Dexter 2 per-implementation file

For example: all three specification files above include a further requirement ret_ops = nil that the %transfer and %approve entrypoints return no operations.¹²

For example: in the camlCase and Edukera specification files, we require the %getBalance entrypoint to fail if the owner does not have a balance in the ledger; the Dexter 2 specification file must succeed even in this case and return zero.¹³

Each such contract-tailored FA1.2 specification is designed in such a way that it:

1. implies the general FA1.2 specification, and
2. fully describes the behavior of the given contract.

The latter point implies that for each entrypoint, the returned storage and the list of operations are uniquely identified by the initial environment and storage, and the entrypoint parameter.¹⁴

As mentioned earlier, we can carry out some important verification once and for all, without recourse to a contract-tailored specification file. For instance, we can prove that in any contract satisfying the general FA1.2 specification, the total sum of all tokens remains unchanged by any of the five entrypoints. For the view entrypoints this is of course trivial; establishing this for the %approve and (especially) %transfer entrypoints requires some amount of effort that would otherwise have to be carried out for each implementation separately. The axioms we imposed earlier as part of the abstract FA1.2 interface are key here.

In contrast, the Edukera Why3 verification features similar invariants, but as one-off proof obligations; e.g., the following formal property is part of the %transfer entrypoint specification:

forall tokenholder in ledger,
   tokenholder.holder <> %from ->
   tokenholder.holder <> %to ->
   before.ledger[tokenholder.holder] = some(tokenholder)

This states that if an account is neither the sender %from nor the recipient %to, then its ledger entry is untchanged by the %transfer entrypoint.

Problems detected, problems solved

Our verification revealed two discrepancies between how the three implementations above handled corner cases, which had not been explicitly addressed in the the FA1.2 standard — in other words, the implementations satisfied the FA1.2 standard but this standard was underspecified.

Discrepancy 1 resolved (making a transfer to yourself)

When the from and to accounts in the %transfer entrypoint coincide, the operation can be treated either

1. as a NOOP, or
2. as a regular transfer.

We noted that the camlCase contract implementation treats the operation as a NOOP; whereas the Edukera and Dexter 2 contract implementations treat the operation as a regular transfer.

There is a real logical difference between these two options. In the case of a NOOP, nothing changes at all. In the case of a regular transfer, the account balances don’t change but the spending allowance does, because it gets decremented by the amount transferred (from the contract to itself).

Following discussions:

• The FA1.2 standard was updated to eliminate this ambiguity by requiring that this corner case be treated as a regular transfer (GitLab issue).
• The camlCase implementation of the %transfer entrypoint was updated (GitLab issue).

Discrepancy 2 resolved (the view entrypoints)

Recall the view entrypoints %getBalance, %getAllowance, and %getTotalSupply mentioned above. The callback transactions are now required to forward to the callback all of the tez passed to the entrypoint (see the GitLab issue). The Edukera and the camlCase implementations were duly updated:

• The Edukera view entrypoints were updated (GitLab commit).
• The camlCase view entrypoints also needed slight adjustment (GitLab issue).
• The Dexter 2 implementation needed no change. The view entrypoints are hardcoded to send zero tez to the callback, and this is compliant since every Dexter 2 FA1.2 entrypoint is designed to fail if the number of tez passed to it is greater than zero.

Conclusions

The formal verification of an FA1.2 smart contract in Coq has the following components:

1. Checking correctness with respect to the abstract FA1.2 interface and specification.

   This includes instantiating concrete Coq types for the parameter and storage type parameters parameter_ty and storage_ty, providing methods for manipulating them, and proving that the axioms required by the interface are satisfied.

   (Here’s the relevant file for our first example of the camlCase contract.)

2. Formulating a contract-tailored FA1.2 specification for the implementation’s behaviour — including any additional entrypoints — together with a proof that the general FA1.2 specification is satisfied.

   The contract-tailored specification may reference additional data, operators, or behaviour that are not present in the FA1.2 standard: for instance, some contracts offer an option to pause some of the contract’s capabilities; if this flag is set, some (or even all) of the FA1.2 entrypoints might fail by default.

3. Verifying that the contract-tailored FA1.2 specification does indeed capture the behavior of the contract.

   Specifically: each of the FA1.2 entrypoints successfully returns an updated storage and a list of operations if and only if these satisfy the specification. We don’t need to establish both directions of the if-and-only-if explicitly. It suffices to prove:

   1. If an entrypoint successfully returns an updated storage and a list of operations, then these satisfy the specification.
   2. The specification uniquely identifies the return storage and the list of operations.
      
   3. If there exists a return storage and a list of operations that satisfy the specification, then the entrypoint succeeds (irrespective of the actual storage and list of operations returned).

   Here i is one direction of the equivalence, and i together with ii and iii implies the full equivalence. Proving ii and iii is often simpler than establishing the converse to i directly.

4. Verifying that all entry points (including any additional ones) preserve the validity of the storage.

   For entrypoints outside of FA1.2 this has to be established explicitly. For the FA1.2 entrypoints we already know that the sum of all tokens remains unchanged; hence we only need to show that the %getTotalSupply value remains the same. In case of the Dexter 2, Edukera, and camlCase implementations this was straightforward.

We will continue to improve and simplify the Coq code (and the Mi-Cho-Coq tool on which it depends), and future work includes:

1. An analogous treatment of the FA2 standard, an instance of which can be plugged into Dexter 2.
2. Adding native FA1.2 support to tezos-client.