# Proposal for strengthening ticket handling in the Tezos Protocol

**Status:** APPROVED
**Authors:** Hans Hoglund, Joel Bjornson, Derek Sorensen
**Target Protocol:** J
**Summary:** Add runtime checking of ticket ownership, with no change to semantics and on-chain ticket representation.
**Previous proposal:** https://hackmd.io/Gc2GZGV-QSuqHtzj2vvlsQ?view

## Background

### Motivation

Tickets provide a first-class notion of ownership in the Tezos Protocol. In order to support use cases such as FTs, NFTs and permissions systems, tickets must satisfy strong ownership invariants.

Though the current Protocol is believed to rule out invalid uses of tickets, we do not have certainty that it does. We therefore propose a simple mechanism to detect invalid ticket uses. The aim is not to *rule these events out in advance*, but to *detect them and signal an error* if they do.

### Ticket semantics

We are not proposing any changes to ticket semantics, but here is a brief overview of the current state:

Tickets have *value semantics*. Tickets that have the same creator, value and amount can not be distinguished.

A contract can create any number of tickets with `TICKET`. The creator and value fields are immutable, and can not be changed by `SPLIT_TICKET` and `JOIN_TICKET`. The only way for a contract to retrieve a ticket it has not created itself, is to have it *transfered* from another contract, via `CREATE_CONTRACT` or `TRANSFER_TOKENS`.

#### Token types

We can think of a pair of a creator (a contract address) and a value (a packable value) as a *type of token*. For example `(Alice, "red")`, `(Alice, "blue")` and `(Bob, "red")` are all distinct *token types*. Token types are not the same as Michelson types. For example `(Alice, False)` is a token type, and corresponding tickets have the (Michelson) type `ticket bool`.

Possessing (in storage or on stack) a ticket `(creator, value, n)` implies ownership of `n` tokens of token-type `(owner, value)`. For example, possession of the ticket `(Alice, "red", 5)` implies ownership of 5 `(Alice, "red")` tokens.

> Note: When we refer to *tokens* in this document, we mean the kind of tokens implied by tickets, not native tokens or smart-contract encoded tokens.

### Guarantees from the type system

The Michelson type system aims to prevent falsification and bad ownership change, using the Duplicable attribute.

Basic types such as `nat` are Duplicable. Tickets are not Duplicable by design.

Duplicability of containers [depends on what they contain]([src/proto_alpha/lib_protocol/script_ir_translator.ml](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/script_ir_translator.ml#L996)). `list T` is Duplicable iff T is Duplicable, and so on. In Haskell we would write:

instance Duplicable a => Duplicable (List a)
instance Duplicable v => Duplicable (BigMap k v)
...

The `DUP` operation is forbidden on non-Duplicable values. This is checked statically (at Michelson type-checking time). This guarantees that a ticket cannot be sent to some other contract and, at the same time, remain in the sender's storage.

### Guarantees from runtime checks

Most guarantees about ticket ownership come from the Michelson type system and calling convention. There are also a few runtime checks:

- `operation` is a Duplicable type for legacy reasons. However, at most one out of two operations resulting from a DUP call can be used, or execution will fail.
- Implicit accounts are prevented from sending ticket-containing types to contracts.

These mechanisms prevent tickets from being serialized (and copied) or forged by instantiating them as storage when originating a new contract.

### Confidence

We are interested in ruling out invariants such as:

- Contracts forging tickets.
- Implicit accounts forging tickets.
- Accidental duplication of tickets.

Although the current implementation of tickets is believed to rule these out, as described above, this has not been formally proven.

Furthermore, changes to the Protocol codebase such as extending Michelson with new instructions may introduce new vulnerabilities.

## Proposal

We propose to decorate the Protocol with a optional *token validation* layer, which tracks balances per contract and token type. The only purpose of the validation layer is to reject invalid operations. In addition to rejecting the block containing the invalid transaction, validation errors can be logged and automatically reported to Protocol developers. **Token validation failure should always be treated as a Protocol bug**.

Compared with [our previous proposal](https://hackmd.io/Gc2GZGV-QSuqHtzj2vvlsQ?view), this does not change the representation of tickets. It only adds an extra layer of protection to detect invalid operations.

### Ticket-balance table

The validation layer consists of:
- A new storage table `Balance`
- Functions to update the `Balance` table and fail on invalid states

The storage table has the following layout, mapping *ticket creator*, *content* and *current owner* to an amount. In other words, it gives the current balance for a given *contract* and *token type*. The table is sparse: a missing row means a balance of zero.

| Creator x Content x Owner | Amount |
|---------------------------|-----------|
| (KT789, "T1", KT789) | 1 |
| (KT789, "T1", KT123) | 5 |
| (KT700, Unit, KT800) | 7 |
| ... | ... |

To ensure fast lookups, the content should be a type supporting hashing and equality. Because ticket content is always comparable, either these exist or they can be implemented (or the underlying Merkle hash could be used).

The Michelson ticket instructions are **not** impacted and do not perform any additional side effects. Instead, validation is performed in pre and post-execution steps.

### An example

Below is an example of how to account for tickets in a contract call to $K_1$.

#### Pre-execution

All $K_1$'s tickets exist in either:

- The *incoming* arguments passed to $K_1$, which we call $I$.
- $K_1$'s storage. We call the number of tokens in the storage $S_1$.

digraph {
  compound=true
  rankdir=TB

  graph [ fontname="Source Sans Pro", fontsize=20 ];
  node [ fontname="Source Sans Pro", fontsize=18];
  edge [ fontname="Source Sans Pro", fontsize=12 ];


   {
     concentrate=false
    ts [label="K1's Tickets"] [shape=box]
    i [label="Parameters (I)"] [shape=box]
    s [label="Storage (S1)"] [shape=box]
    lz [label="Lazy"] [shape=box]
    ss [label="Strict"] [shape=box]
    ts -> s
    ts -> i
    s -> ss
    s -> lz
    label="Pre-execution"
  }
}

We trust that the balance table has been updated to reflect the accounting of these tickets in a previous post-execution step. We refer to the balance table projection for $K_1$ as $B_1$.

The balance, $B_1$, for some token before execution is:

$$
B_1 = S_1 + I
$$

For example, assume $K_1$ receives one $Alice^{Blue}$ token in parameters, and has four of them in storage, along with one $Bob^{Red}$ and one $K_1^{Yellow}$. We have:

| Token type | $S_1$ | $I$ | $B_1$ |
|----------------|-------|--------|------:|
| $Alice^{Blue}$ | 4 | 1 | 5 |
| $Bob^{Red}$ | 1 | 0 | 1 |
| $K_1^{Yellow}$ | 1 | 0 | 1 |

#### Execution

Michelson is executed, producing operations and *new storage*. This has no effect on the balance table.

#### Post-execution

After executing contract $K_1$, tickets may exist in $K_1$'s storage as well as in emitted operations:

digraph {
  compound=true
  rankdir=TB

  graph [ fontname="Source Sans Pro", fontsize=20 ];
  node [ fontname="Source Sans Pro", fontsize=18];
  edge [ fontname="Source Sans Pro", fontsize=12 ];


   {
     concentrate=false
    ts [label="Tickets After"] [shape=box]
    os [label="Operations (outgoing)"] [shape=box]
    s [label="Storage (S2)"] [shape=box]
    lz [label="Lazy"] [shape=box]
    ss [label="Strict"] [shape=box]
    ts -> s
    ts -> os
    s -> ss
    s -> lz
    label="Pre-execution"
  }
}

All $K_1$s tickets (except for any tickets in parameters in calls to $K_1$) now only exist in $K_1$'s storage. We perform a diff, $\Delta$, on the old and new balances for a token type:

$$
\Delta = B_2 - B_1 = S_2 - B_1 = S_2 - S_1 - I
$$

:::info
Calculating $(\Delta = S_2 - S_1 - I)$ naively may be expensive and we we would like to avoid performing a strict traversal over both storage values. See the [implementation section](#Implementation) below for details.
:::

The diff may tell us that $K_1$ has withdrawn two $Alice^{Blue}$ and one $Bob^{Red}$ from the store, and deposited one $K_1^{Yellow}$.

The new balance $B_2$ is equivalent to what the amount put back into $K_1$'s storage $S_2$.

| Token type | $B_1$ | $I$ | $S_1$ | $S_2$ | $\Delta$
|----------------|-------|-------|-------|-----------|-------:|
| $Alice^{Blue}$ | 5 | 1 | 4 | 2 | -3 |
| $Bob^{Red}$ | 1 | 0 | 1 | 0 | -1 |
| $K_1^{Yellow}$ | 0 | 0 | 0 | 1 | 1 |

We now verify that for each row, either:

1. Balance did not increase ($\Delta <= 0$), or
2. This token type is of the shape $(K_1, \_)$, that is $K_1$ created tokens in its own namespace.

Assuming no errors, the balance table for $K_1$ can be updated according to the new balances.

We then proceed to update balance for recipients.

The diff table above implies a *spending budget* for each token type, not created by $K_1$. The budget for tickets created by $K_1$ is unlimited as $K_1$ could have minted any number of them.

Formally, for some set of minted tokens $t_{mt}$, outgoing tokens $I_o$ must satisfy:

$$
I_o <= B_1 - B_2 + I_{mt}
$$

If $I_o$ is smaller than the RHS then at least one ticket was *dropped*.

We compute $I_o$ by a strict deep traversal of the Michelson operations (rejecting duplicated operations), finding all *outgoing* tickets from the operations parameters in either `CREATE_CONTRACT` or `TRANSFER_TOKEN`, resulting in a table such as:

| Token | Recipient | Amount |
|----------------|------------------|-------------------:|
| $Alice^{Blue}$ | $K_2$ | 1 |
| $Alice^{Blue}$ | $K_3$ | 2 |
| $K_1^{Green}$ | $K_2$ | 10 |

First, we validate that the total outgoing amounts of each ticket type does not exceed the *spending budget*. If the budget is exceeded — implying that a ticket has **somehow** been forged — an error is thrown and the transaction fails.

In the case above, we have 3 outgoing units of $Alice^{Blue}$ tickets. This is compatible with the budget. We also have 10 units of $K_1^{Green}$ to $K_2$ which is fine, as $K_1$ tickets don't have any spending budget.

The balance table can now be updated for the $K_2$ and $K_3$ contracts. The projection of the transfer table for each recipient contract becomes incoming tokens $I$ in the next post-execution phase.

#### Summary

The call to contract $K_1$:

- Transferred 3 units of $Alice^{Blue}$ to other contracts.
- Created 1 unit of $K_1^{Yellow}$ and saved in the storage.
- Created and transferred 10 units of $K_1^{Green}$ to another contract.
- Dropped 1 unit of $Bob^{Red}$.

#### Implementation

Any value, $S$, representing the number of tokens in the storage can be split into *strict* and a *lazy* parts, so that:

$$
S = S^{strict} + S^{lazy}
$$

The strict part consists of tickets in any non-lazy data structure (such as `pair` and `list`), while the `lazy` part is the number of tickets in lazy structures, or more specifically `big-map`s.

Expanding the definitions for $B_1$ above using the strict and lazy partitioning scheme gives:

$$
\begin{align}
B_1 &= S_1 + I = S_{1}^{strict} + S_1^{lazy} + I \implies \\
S_1^{lazy} &= B_1 - S_{1}^{strict} - I
\end{align}
$$

We can also expand the definition for the new balance, $B2$:

$$
\begin{align}
B_2 = S_2 = S_2^{strict} + S_2^{lazy}
\end{align}
$$

When executing a Michelson script, we're also give a *lazy-diff* value that represents changes to the lazy part of the storage. Introducing a term $S_{\delta}^{lazy}$ for the part of the diff that concerns tickets with ticket count $S$, implies:

$$
S_2^{lazy} = S_1^{lazy} + S_{\delta}^{lazy}
$$

After plugging in the equation for $S_1^{lazy}$:

$$
S_2^{lazy} = (B_1 - S_1^{strict} - I) + S_{\delta}^{lazy}
$$

We thus have the following formula for $B_2$:

$$
B_2 = B_1 + S_2^{strict} + S_{\delta}^{lazy} - S_{1}^{strict} - I
$$

Or:

$$
B_2 = B_1 + \Delta
$$

Where:

$$
\Delta = S_2^{strict} - S_{1}^{strict} + S_{\delta}^{lazy} - I
$$

So, in order to calculate the new balance $B_2$ and $\Delta$ for some token, we need:

- $B_1$ — balance before the execution of the contract.
- $S_1^{strict}$ — the amount of tokens in the strict part of the old storage.
- $S_2^{strict}$ — the amount of tokens in the strict part of the new storage.
- $S_{\delta}^{lazy}$ — the amount of tokens *added/removed* to the lazy part of the storage.
- $I$ — the amount of tokens contained in the incoming arguments.

#### Tickets inside lazy structures (big-maps)

The scenarios for which we need to traverse both the strict and the lazy
parts of a data-structure are:

1) Tickets contained a big-map in the incoming parameters.
2) Tickets contained in a big-map in some outgoing parameters to `TRANSFER_TOKEN` operation.
3) Tickets contained in a big-map in the new storage of a `CREATE_CONTRACT` operation.

Note that if a big-map does not contain tickets, it will never be traversed.

Additional scenarios for when values of big-maps are traversed:

4) When a big map containing tickets changes ownership—by being sent as parameter from a contract to another or to the storage of a new contract.
6) A big-map containing tickets is dropped.
7) A big-map containing tickets is moved within the storage.

All these scenarios require traversing the list of elements in the big-map
and hence is linear in the size. Given these constraints, putting tickets
in big-maps that are either moved or destroyed is not recommended.

### Other rejected scenarios

Let us now consider how various invalid scenarios are rejected by the token validation layer. We use the word **somehow** to refer to an unexpected bug in the Protocol (to be fixed and corrected when flagged by the token validation layer).

#### Contracts forging tickets

A contract **somehow** has on its stack a ticket implying ownership of a token it did not recieve or originate.

Any attempt to transfer or store this ticket will fail, because no corresponding record exists in the balance table.

#### Implicit account forging a ticket

A user **somehow** is allowed to originate a smart contract with a ticket in its storage type.

Any subsequent attempt to transfer this token will fail, because no corresponding entry exists in the balance table.

#### Accidental duplication

A contract **somehow** duplicates a ticket.

If the contract attempts to transfer both tickets, the first operation will succeed (and update the balance table), and the second one will fail as the balance is now too low.

## Pre-populating the balance table

Tickets created before adoption of this Protocol will not have corresponding entries in the balance table, so these have to be created retroactively.

We propose that migration to this Protocol traverses the state of all contracts by contracts whose storage type contains tickets (estimated to be <1% of mainnet contracts) adding entries corresponding to the tickets in their storage.

The implementation of this proposal will include evidence that this migration (stitch) completes in reasonable time on mainnet.

## Alternative approaches

### Formal verification

Instead of tracking token ownership via runtime validation, we could attempt to formally prove that the Protocol rules out the above failure cases for all possible ledger states. In order to prevent breakage on further protocol changes, the verification would have to be applied to future versions of the code base as well.

In practice this could mean:
- Running `coq-of-ocaml` applied to the current Protocol code base in the CI, or:
- Using `mi-cho-coq` and prove that it is equivalent to the current Protocol codebases.

Our proposal is lightweight in that it does not change protocol semantics, and does not rule out future attempts at verifying correctness (though a successful proof of correctness would render the checks suggested here unnecessary).

## Related work

- Document the exact semantics of tickets better.
- [Fix the documentation](https://gitlab.com/tezos/michelson-reference/-/issues/51) of Duplicable and other attributes.
- Add more regression tests to verify the behaviour of Michelson attributes (especially Duplicable).