$$ % symbols of linear logic \newcommand{\lolli}{\multimap} \newcommand{\tensor}{\otimes} \newcommand{\with}{\mathbin{\&}} \newcommand{\paar}{\mathbin{\dnasrepma}} \newcommand{\one}{\mathbf{1}} \newcommand{\zero}{\mathbf{0}} \newcommand{\bang}{{!}} \newcommand{\whynot}{{?}} % \oplus, \top, \bot % \newcommand{\bilolli}{\multimapboth} % in txfonts % \newcommand{\lif}{\multimapinv} % in txfonts \newcommand{\bilolli}{\mathrel{\raisebox{1pt}{\ensuremath{\scriptstyle\circ}}{\!\lolli}}} \newcommand{\lif}{\mathrel{\raisebox{1pt}{\ensuremath{\scriptstyle\circ}}{\!-}}} \newcommand{\aff}{{@}} \newcommand{\multi}[1]{\underset{#1}{\Large\tensor}} \newcommand{\gmulti}[1]{\underset{#1}{\Large\tensor^g}} $$

Introduction

As a demonstration of specification in Linear Logic, we demonstrate the specification of an ERC20 token, with the commonly understood token transfer semantics as found in ds-token.

Semantics

We refer to an arbitrary token as a gem. An arbitrary token with some holder \(Holder\) is written as \(GEM(Holder)\).

We introduce a convenient notation for holding multiple gems:

\[ \multi{N}GEM(O) = \underbrace{GEM(O) \tensor ... \tensor GEM(O)}_N \]

Our token has a notion of 'allowance'. If there exists an 'allowance' token, \(Allowance(Src, Sender)\), then the \(Sender\) is allowed to transfer one gem from \(Src\) to any other entity. Multiple allowance tokens are denoted as for multiple gems.

Our token has a notion of of ownership. If there exists a \(GemOwner(Sender)\) token then the \(Sender\) is able to perform some extra token operations.

Our persistent context contains a \(MSG(sender)\) resource, which relates to msg.sender in the EVM (Solidity) model.

Specification

TODO: need a tensor in front of multi

Send gems from the \(sender\) to \(Dst\):

\[\begin{array}{ll} transfer(Dst, Wad) := & \multi{Wad} GEM(sender) \\ & \lolli \\ & \multi{Wad} GEM(Dst) \end{array}\]

Increase the allowance of \(Guy\):

\[\begin{array}{ll} approve(Guy, Wad) := & 1 \\ & \lolli \\ & \multi{Wad} Allowance(sender, Guy) \end{array}\]

Transfer gems on behalf of another entity:

\[\begin{array}{ll} transferFrom(Src, Dst, Wad) := & \multi{Wad} GEM(Src) \\ & \multi{Wad} Allowance(Src, sender) \\ & \lolli \\ & \multi{Wad} GEM(Dst) \end{array}\]

Create new gems:

\[\begin{array}{ll} mint(Wad) := & GemOwner(sender) \\ & \lolli \\ & \multi{Wad} GEM(sender) \\ & \tensor GemOwner(sender) \end{array}\]

Destroy gems:

\[\begin{array}{ll} burn(Wad) := & GemOwner(sender) \\ & \multi{Wad} GEM(sender) \\ & \lolli \\ & GemOwner(sender) \end{array}\]

Add an owner:

\[\begin{array}{ll} rely(Guy) := & GemOwner(sender) \\ & \lolli \\ & GemOwner(Guy) \\ & GemOwner(sender) \end{array}\]

Remove an owner:

\[\begin{array}{ll} deny(Guy) := & GemOwner(sender) \\ & GemOwner(Guy) \\ & \lolli \\ & GemOwner(sender) \end{array}\]

Limitations

Note that we have not defined the read-only operations balanceOf, totalSupply and allowance. It is not possible to define these within the logic as this requires knowledge of the global state, something that is only possible on a meta-logical level.

We can do things like define counters that track these quantities, for example define a resource \(GEM_T(GemTotalSupply)\) and then redefine mint:

\[\begin{array}{ll} mint'(Wad) := & GemOwner(sender) \\ & \tensor GEM_T(TotalSupply) \\ & \lolli \\ & \multi{Wad} GEM(sender) \\ & \tensor GemOwner(sender) \\ & \tensor GEM_T(TotalSupply + Wad) \end{array}\]

Similarly we could have a notion of a wallet, where the Guy has a balance of Wad: \(GEM(Guy, Wad)\). balanceOf can easily be pattern matched.

In the latter case we run into a problem: is this wallet unique? To create a new wallet we have to be aware of the global state, to check if one exists already.