Refactoring the Management of Native Tokens in the Tezos Economic Protocol

Before the Ithaca protocol proposal, native protocol token¹ (tez) movements and associated balance updates could be difficult to follow in the Octez source code for developers and maintainers. For example, crediting or debiting a contract, or creating the corresponding balance updates, often happened at distant locations in the code, with a sometimes non-trivial control flow in between those operations. With Ithaca, we have refactored the code to centralize token movements (e.g. transactions, fees payments, rewards, …) in a dedicated module, so that:

1. Token transfers are more explicit and uniform, and associated balance updates are exhaustive.
2. It is easier to assess properties related to token movements, such as preserving the invariant circulating tokens = minted tokens - burned tokens. Here, the term circulating tokens refers to all tokens frozen or held by user and smart contracts.

To achieve this, we aimed for an implementation of token transfers that is correct-by-construction in the following senses:

• Tokens are either minted and deposited into an account, moved from one account to another, or withdrawn from an account and burned; and
• Balance updates found in block metadata give a complete and exact account of all tokens minted, moved or burned.

The first property ensures that the total amount of tokens in circulation is equal to the difference between the amount of tokens minted and the amount of tokens burned. Continuously ensuring theses properties while the protocol evolves can be particularly tedious when the implementation does not use an explicit notion of token transfer from one token holder to another. The second property allows anyone to audit all token movements that happen when a block has been applied, just by looking at the balance updates in the block’s metadata.

Token management in Hangzhou

In protocol Hangzhou, token transfers are implemented in a few steps consisting of debiting a sender of tokens, crediting a receiver of tokens and constructing balance updates to report the movement. Even though those steps are semantically very close to each other, they are intermixed with other instructions and hence can be distant within the source code. For example, a transfer from an implicit account to another is implemented as follows:

...
Contract.spend ctxt sender amount >>=? fun ctxt ->
(match Contract.is_implicit receiver with
| None -> return (ctxt, [], false)
| Some _ -> (
    Contract.allocated ctxt receiver >>=? function
    | true -> return (ctxt, [], false)
    | false ->
        Lwt.return
          ( Fees.origination_burn ctxt >|? fun (ctxt, origination_burn) ->
            ( ctxt,
              [
                Receipt.
                  ( Contract payer,
                    Debited origination_burn,
                    Block_application );
              ],
              true ) )))
>>=? fun (ctxt, maybe_burn_balance_update, allocated_receiver_contract) ->
Contract.credit ctxt receiver amount >>=? fun ctxt ->
...

This implementation makes it difficult to ensure that the tokens have been accurately transferred from the sender to the receiver. Indeed, to ensure this, it is also necessary to be certain that the function calls between the transfer steps do not modify the balance of the accounts concerned. Moreover, the balance updates corresponding to debiting the sender and crediting the receiver are done much later after many other instructions. Furthermore, between debiting the sender and crediting the receiver, a balance update is created to reflect the fact that tokens have been burned to pay the origination cost. However, the call to Fees.origination_burn does not involve tokens and only involves the accounting of the consumed storage space. Here the balance update is created in anticipation of tokens being burned at some other location in the code when the following instruction is executed: Fees.burn_storage_fees ctxt ~storage_limit ~payer:.... Consequently it is more difficult to verify that all balance updates found in block metadata faithfully reflect token movements that have occurred.

Token management in Ithaca

In protocol Ithaca token management explicitly consists of three possible operations:

• Mint tokens and deposit them into an account
• Transfer tokens from one account to another
• Withdraw tokens from an account and burn them

A new module named Token provides functions to perform these operations, and to obtain the balance of an account. Here, the term account must be understood in a broader sense than in implicit or originated accounts. For instance, to freeze the deposits of a delegate, deposited funds are withdrawn from the delegate’s implicit account and its balance of frozen tokens is increased. To make that type of token management operation fit the pattern of a transfer from one account to another, the frozen deposits of a delegate must be viewed as a kind of account from the point of view of the Token module. Hence, the notion of account needs to be generalized.

A lightweight generalization of accounts

We want to make the notion of a transfer from one account to another more explicit, while minimizing the amount of rewritten code, and hence reducing the risk of introducing bugs. Hence, the notion of account is generalized in a lightweight fashion. There are three kinds of accounts: source accounts, container accounts, and sink accounts.

Source accounts are debited whenever new tokens are minted, and designate fictitious accounts with a virtually infinite balance from which tokens can be withdrawn. For example, `Nonce_revelation_rewards is the source account of tokens minted to reward delegates for revealing their nonces, and `Liquidity_baking_subsidies is the source account of tokens minted to subsidize the liquidity baking CPMM contract.

Container accounts are regular (user and smart contract) accounts, or convenience accounts that hold tokens temporarily (e.g. when parts of a delegate’s funds are frozen). These accounts have a finite capacity (of a fixed-size integer) and a balance that is increased or decreased whenever they are credited or debited. The function Token.balance allows to read the balance of a container account. For example, the account (`Contract c) represents an implicit or originated account c, and the account (`Frozen_deposits d) represents the account of the frozen deposits of the delegate d.

Sink accounts are credited whenever tokens are burned, and designate fictitious accounts virtually able to receive an unlimited number of tokens. For example, the sink account `Storage_fees is the receiver of storage fees burned for consuming storage space on the chain, and the sink account `Double_signing_punishments is the receiver of tokens burned as punishment for a delegate that has double baked or double endorsed.

Tokens can be transferred from a sender account (i.e. a source or container account) to a receiver account (i.e. a container or sink account). The type Token.container represents container accounts. The type Token.source represents accounts that can play the role of the sender in a transfer of tokens, and similarly, the type Token.sink represents accounts that can play the role of the receiver. Both Token.source and Token.sink contain Token.container since container accounts can be both sender and receiver of tokens. Those three types are wrappers that allow the Token module to dynamically dispatch the operations of crediting and debiting corresponding accounts to the right piece of code able to handle the operations.

Transferring tokens

The operations of token management can be performed by invoking the transfer or transfer_n functions of the Token module. A transfer of a given amount from a sender to a receiver simply consists in withdrawing that amount from the sender’s account and crediting the same amount to the receiver’s account. Hence:

• to mint an amount of tokens and deposit it into a receiver account, one transfers that amount from a source account to the receiver account
• to move tokens from one container account to another, one performs a transfer from the former (sender) account to the latter (receiver) account, and
• to burn an amount of tokens withdrawn from a given account, one performs a transfer from the sender account to a sink account.

Consider the following examples:

• Token.transfer ctxt (`Contract sender) (`Contract receiver) amount
• Token.transfer ctxt `Endorsing_rewards (`Contract d) rewards
• Token.transfer ctxt (`Frozen_deposits d) `Double_signing_punishments amount_to_burn.

The first example is the instruction invoked during a transaction operation from a sender contract to a receiver contract. Here the constructor `Contract allows to construct container accounts that can designate sender accounts as well as a receiver accounts. The implementation of the transfer functions is such that, by construction, transfers between container accounts leave the total amount of tokens in circulation unchanged. Also, those functions are the only locations where that property needs to hold.

The second and third examples correspond to the instructions invoked, respectively, to distribute endorsing rewards to a delegate d, and to punish a delegate d for double signing. Here Endorsing_rewards is a source account that cannot play the role of the receiver in a transfer, and Double_signing_punishments is a sink account that cannot play the role of the sender in a transfer. Using distinct types of accounts for different types of token transfers makes intent more explicit, more tractable and easier to verify. Tokens withdrawn from a source account are by definition minted, and tokens sent to sink accounts are by definition burned. When sticking to this transfer pattern, we can be sure that these are the only ways to respectively increase or decrease the amount of tokens in circulation. Since all token management operations now follow the transfer pattern, it is easy to list all locations in the protocol where token movements are involved just by running:

grep -R "Token.transfer" src/proto_alpha.

Balance updates

Whenever tokens are minted, moved, or burned, one or more accounts are debited, and another account is credited. This results into a sequence of balance updates reporting the amount of tokens debited from and credited to each of the accounts involved. In Ithaca, balance updates are exclusively generated by the transfer functions of the Token module. Therefore, by construction, they reflect exactly the token movements that have occurred. And it is now easier to assess that they are exhaustive and correct just by reviewing the implementation of the Token module.

In block metadata, the field balance_updates contains balance updates generated by the invocations of token transfer functions. Each invocation of those functions generates a list of balance updates starting with a series of debits, and ending with a credit matching those debits. Typically, this field contains a flat list resulting from the concatenation of one or more lists of balance updates. Consider for example the following flat list of balance updates:

  [ {"kind": "...", ..., "change": "-100", "origin": "block"},
    {"kind": "...", ..., "change": "100", "origin": "block"},
    {"kind": "...", ..., "change": "-125", "origin": "block"},
    {"kind": "...", ..., "change": "-75", "origin": "block"},
    {"kind": "...", ..., "change": "200", "origin": "block"} ]

This list reports that two transfers have occurred: 100 mutez are transferred from one account to another, and a total of 200 mutez are transferred from two accounts to a third. For a more complete description of the format for balance updates, see this page of the documentation.

Conclusions & Future Work

In Ithaca we have centralized the management of native protocol token movements in a dedicated module so that token transfers are correct by construction. Basically we have implemented some of the ideas mentioned here and here in a lightweight manner so as to minimize the risk of introducing bugs. The transfer pattern is now the only uniform means of minting, moving, or burning tokens in the Tezos protocol. By construction, balance updates in block metadata faithfully and exhaustively reflect all token transfers that have occurred when the block has been applied. To test this refactoring work, we have very much relied on our existing suite of unit and integration tests, and we have also written more unit tests to check the expected properties of the token transfer functions.

In some cases quite sensitive changes were necessary before we could apply the new transfer pattern to manage tokens, while preserving previous behavior. For instance, this was the case for the burning storage fees. Here it was important to preserve the validity of transactions where the sender’s balance is sufficient to pay the fees only when all internal transactions have been processed. To test such changes, we have back-ported them to previous protocols, and the chain has been replayed to ensure that the previous behavior has been preserved.

Our next work on the subject of token management will be to extend the Token module so that it also manages token delegations. The staking balance of a delegate can only be changed when token owners delegate or transfer their tokens, but updating staking balances is currently performed at various locations after each token transfer that affects staking balances. With the refactoring described above it will be possible to update the staking balance once and for all in the transfer functions of the Token module.