

































\section{Introduction}
\label{sec:introduction}


dApps enable multiple parties
sharing state
to jointly execute functionality
according to a predefined agreement. The main component is the 
smart contract -- the predefined agreement -- 
that regulates the interaction between 
the dApp's clients. Client--contract interactions can be logically described by
state machines~\cite{SergeyNJ0TH19,MavridouL18,MavridouLSD19,SuvorovU19}
specifying
which party
is allowed to do what and when.

dApps can operate without centralized trusted intermediaries by
relying on a blockchain and its consensus protocol. To this end, a contract is deployed to and executed on the blockchain, which guarantees its correct execution; clients that run outside of the blockchain can interact with the contract via transactions.
A key feature of dApps is that they can directly link application logic with transfer of monetary assets.
This enables a wide range of correctness/security-sensitive
business applications, e.g., for cryptocurrencies, crowdfunding, \changed{and} public offerings,\!\footnote{
  700\,K to 2.7\,M contracts have been deployed
  per month between July 2020 and June 2021~\cite{google-cloud-big-query-contracts-per-month}
  on the Ethereum blockchain -- the most popular dApps platform~\cite{dapp-q2-2020-report}.
  %
  %
  %
  %
  %
  %
  %
  %
  %
  Some dApps manage tremendous amounts of assets, e.g.,
  Uniswap \cite{uniswap-info} -- the largest Ethereum trading platform
  had a daily trading volume of 0.5\,B\,--\,1.5\,B~USD in June 2021.}
and make them, at the same time, an attractive target for attackers.
\changed{The latter is aggrevated by the fact that contracts can be called by any client in the network,}
including malicious ones that try to force the contract to deviate
from the intended behavior~\cite{daoExploit}. 
These issues demand programming models
that ensure the correctness and security of dApps by-design, especially 
\changed{given the fact that contract code cannot be updated after deployment.}

\changed{We address correctness and security of the client--contract interaction of dApps
by enforcing the execution order of contract code.}
Deviations from the intended
interaction protocols due to implementation errors
and/or malicious attacks are indeed a critical threat 
(besides issues with arithmetic or buffer overflows, etc.).
\changed{In recent years, there have been several large attacks exploiting flawed program flow control in smart contracts.
Most famously, attackers managed to steal around 50\,M~USD~\cite{daoExploitAnalysis,daoExploit} from a decentralized autonomous organization, the DAO.
In two attacks on the Parity multi-signature wallet, attackers stole respectively froze cryptocurrencies worth 30\,M~USD~\cite{parityBug} respectively 150\,M~USD~\cite{parity2}.}

\subparagraph{Programming dApps.} 
The design space of dApp programming languages can be structured along two dimensions -- similar to other multi-party applications -- based on: 
(1)~how the involved parties (contract and clients) are defined, 
and (2)~how the correctness of their interactions is ensured.

There are two choices for (1): a \emph{local} versus a \emph{global model}. 
In a \emph{local model}, parties are defined each in a
separate \emph{local} program and their interactions are encoded
via 
send and receive effects. 
In contrast, in a \emph{global model}, parties are defined within one shared program 
and interactions are
encoded via combined send-and-receive operations with no effects visible to the outside world.
The local model is followed by actor systems~\cite{Agha:1986:AMC:7929} 
or by approaches stemming from process 
calculi \cite{10.1145/359576.359585};
the global model
by tierless~\cite{Queinnec00,
  Cooper:2006:LWP:1777707.1777724, Choi:2019, ChoiC19, Fowler:2019, Serrano:2006,
  Serrano:2016, Radanne:2016, Weisenburger:2018}
and choreographic~\cite{
  HondaMBCY11, MontesiGZ14, giallorenzo2020choreographies} languages.
  %



The local model requires an explicitly specified protocol
for governing the inter-process send-receive relations
to ensure that every send effect has a corresponding receive effect 
in an interacting -- separately defined -- process.
In contrast, with a global model, there is no need to 
separately specify such a protocol.
All parties run the same program
in lock-step, where
a single send-and-receive operation
performs a send when executed by one party and
a receive on the other party.
Due to this encapsulation of the communication effects,
there is no non-local information to track --  
the program's control flow defines the correct interaction
and a standard System-F-style type system is sufficient. 

Approaches to dApp programming --
industrial or research ones --
follow a local model,
thus rely on 
explicitly specifying the client--contract interaction protocol.
Moreover, the contract and clients are implemented in different languages,
hence, developers have to master two technology stacks.
The dominating approach 
in industry uses
Solidity~\cite{ethereumPopularity} for the contract and
JavaScript for clients.
Solidity relies on developers expressing the protocol 
using assertions in the contract code, which are checked at 
run time~\cite{solidity-best-practises}. 
Failing to correctly introduce assertions 
may give parties illegal access 
to monetary values to the detriment of others~\cite{10.1145/3274694.3274743,10.1145/2976749.2978309}.
In research, contract languages~\cite{DasBHP19,
Coblenz17, SchransED18, Schrans19, Coblenz19, Coblenz20, psamathe,
BlackshearCDGMNPQRSZZ19}
have been proposed that rely on advanced type systems such as
session types, type states, and linear types.
There, processes are typed by the protocol
(of side-effects such as sending and receiving)
that they follow on evaluation,
and non-compliant processes are rejected by the type-checker.

The global model has not been explored for dApp programming. 
This is unfortunate given
the potential to get by with a standard typing discipline and 
to avoid intricacies and potential mismatches of a two-language stack.
Our work fills this gap by proposing
\textsf{Prisma}\xspace{} -- the first language that
features a \emph{global programming model} for Ethereum dApps.
While we focus on the Ethereum blockchain, we believe our techniques to be applicable to other smart contract platforms.

\subparagraph{\textsf{Prisma}\xspace.}
\textsf{Prisma}\xspace enables interleaving contract and client logic within the same program 
and adopts a \emph{direct style (DS)} notation for encoding
send-and-receive operations akin to languages with baked-in support for asynchronous interactions,
e.g., via async/await \cite{DBLP:conf/ecoop/BiermanRMMT12,scala-async}.
DS addresses several shortcomings with the currently dominant encoding
of the protocol's \emph{finite state machines (FSM)}
as one method per transition~\cite{ethereumPopularity, Coblenz17, SchransED18, Schrans19, Coblenz19, Coblenz20}.

First, \changed{FSM style} 
  corresponds to a control-flow graph of basic blocks, which
  is low-level and more suited to be written by a compiler than by a human 
  -- \textsf{Prisma}\xspace leaves it to the compiler to map down high-level declarative 
  DS to low-level \changed{FSM style}.
More importantly, ensuring safety in \changed{FSM style}  
  requires a form of dependent types,
  as the type of an action depends on the current state.
Second, with \changed{FSM style}, the
contract is a passive entity whose execution 
is driven by clients. The DS encoding, in contrast, 
allows the contract to actively ask clients for input.
The latter style naturally fits an execution model
where a dominant acting role controls
the execution and diverts control to other parties
when their input is needed, which matches well the 
dApp setting. 

Overall, \textsf{Prisma}\xspace relieves the developer from the responsibility of
correctly managing distributed, asynchronous program flows and 
the heterogeneous technology stack.
Instead, the burden is put on the compiler, which distributes the program flow 
by means of selective continuation-passing-style (CPS) translation
and defunctionalisation and inserts guards against malicious client interactions.
\changed{
We needed to develop a CPS translation for the code that runs on
the Ethereum Virtual Machine (EVM) since the EVM has no built-in support
for concurrency primitives to suspend execution and resume later,
which could be used to implement asynchronous communication.
While CPS translations are well-known, we cannot use them out-of-the-box
because the control flow is interwoven with distribution in our case.
Given that CPS translations reify control flows into values,
a CPS translation that does not take distribution into account
would allow malicious clients to force the contract to deviate from the intended control flow
by passing a spoofed value to the contract.
Thus, it is imperative to prove correctness of our \emph{distributed CPS translation}
and ensure control-flow integrity of the contract.
}
We formally define the compilation steps and prove them sound and, by doing so, 
eliminate the risk of programmers implementing
unsafe interactions that can potentially be exploited. 






\section{\textsf{Prisma}\xspace in a Nutshell}
\label{sec:the-language}

We present \textsf{Prisma}\xspace by the example of a TicTacToe game, demonstrating
that client and contract are written in a single language,
where protocols are expressed by control flow (instead of relying on advanced typing disciplines)
and enforced by the compiler.

\subparagraph{\changed{Example}.}
TicTacToe is a two-player game over a $3\times3$ board in which
players take turns in writing their sign into one of the free fields until all fields
are occupied, or one player wins by owning three fields in any row, column, or diagonal.
The main transaction of a TicTacToe dApp is \lstinline!move(x,y)!
used by a player to occupy field \lstinline!(x,y)!.
A \lstinline!move(x,y)!  is valid if it is the sender's turn and \lstinline!(x,y)! is empty.
Before the game, players deposit their stakes, and after the game, the stakes are paid to the winner.

\input{paper/graphs/prismaFigures.tex}

Fig.~\ref{fig:funding-diagram} depicts possible control flows
with transitions labeled by client actions that trigger them.
Black arrows depict intended control flows.
The dApp starts in the funding state
where both parties deposit  stakes via \textit{Fund$(c)$}.
Next,
  parties execute \textit{Move$(x,y)$}
  until one party wins or the game ends in a draw.
Finally, any party can invoke a payout of the stakes via \textit{Payout$()$}.\footnote{
  We omit handling timeouts on funding and execution for brevity.
  %
  %
}
Red dashed arrows illustrate the effects of a mismanaged control flow:
a malicious player could trigger a premature payout 
preventing the counterpart to get financial gains.







\section{Compilation and its Correctness}
\label{sec:formalization}


\textsf{Prisma}\xspace is compiled to Solidity and Scala.
\changed{
An important part of our compiler is CPS translation.
Using a standard CPS translation alone, however, is not sufficient
because the control flow is intertwined with distribution.
We need to consider that, while malicious clients cannot change the code executed by the contract,
they can run different code on the client side than what was assigned to them.
Therefore, clients can pass unintended continuations to the contract.
To ensure the correctness of our compiler,
we formalize a selective CPS translation, defunctionalisation toghether
with the process of guarding against unintendend jumps.
Assuming the worst case, i.e.,
all clients are malicious and replace their code completely
executing arbitrary code instead,
we prove guarding contract code is sufficent to guarantee
that behavior of the contract execution is preserved by compilation.
}
The compilation process is key in hiding the complexity of enforcing distributed program flow from the developer
-- hence, correctness is critical.


\begin{itemize}[leftmargin=*]
\item We present the core calculus (\changed{Section}~\ref{subsec:syntax}) $\textsf{MiniPrisma}\xspace_*$  -- 
a hybrid language that includes elements of both the source ($\textsf{MiniPrisma}\xspace_s$)
and the compilation target ($\textsf{MiniPrisma}\xspace_t$), while abstracting over details of both Scala and Solidity. 
We define a hybrid language because
the source and the target share many constructs -- the hybrid language
allows us to focus on how the differences are compiled.

\item We model the compiler
as a sequence of steps that transform $\textsf{MiniPrisma}\xspace_*$ programs 
via several intermediate representations.

\item We define $\textsf{MiniPrisma}\xspace_*$ semantics as a reduction relation over 
configurations consisting of traces of evaluation events and expressions being evaluated.
We distinguish between a good semantics, which evaluates the program in the usual way, 
and a bad semantics, which models attackers by ignoring client instructions and producing 
arbitrary values that are sent to the contract.

\item We prove 
\changed{secure compilation} by showing that the \changed{observable} behavior of the programs 
before and after compilation is equivalent. We capture the observable program 
behavior by the trace of events generated during program evaluation (as guided by the semantic definition) 
and show trace equivalence of programs before and after compilation.
\end{itemize}

\changed{
In more concrete terms, the last point guarantees
the integrity for the control flow of the contract
in the presence of malicious clients.
Note that compiler correctness in a traditional sense (i.e., preservation of the semantics through compilation) is not sufficient in the presence of malicious attackers that can tamper with parts of the code.
}

\changed{
More specifically,
the compiler preserves control flow by inserting additional guards in places where the basic blocks of the program have been separated and distributed onto different computers by the CPS translation.
This ensures that the control flow among the parties is guaranteed not to change after compilation.
In particular, we consider that malicious attackers may tamper with certain parts of the code (the client code).
Therefore the guards have to be placed on the contract side.
Our guarantees hold despite clients tampering with the code.
}

\changed{
For example, in the source code of the TicTacToe game (Section~\ref{sec:the-language}),
it is immediately visible that the players take alternating turns.
Yet, the compiled code is separated and distributed into small chunks of code.
Parties execute a chunk and then wait for other parties,
which will decide on a move that influences where, when, and how to proceed execution.
Our proof shows
that we still ensure that control flow of the contract of the original program
even under attack.
}

\begin{figure}
	\figurehead
	\centering
	%
	\input{notes/syntax.tex}
	\caption{$\textsf{MiniPrisma}\xspace_*$ syntax.}
	\label{fig:syntax}
\end{figure}

\subsection{Syntax}
\label{subsec:syntax}

The syntax of $\textsf{MiniPrisma}\xspace_*$ (Fig.~\ref{fig:syntax}),
has three kinds of identifiers $id$, $\iden$, $\syniden$,
from unspecified sets of distinct names.
Pure identifiers $id$ are for function arguments and let bindings;
mutable variables $\iden$ are for heap variable assignment and access.
In the target program, mutable variables $\syniden$ ($\ensuremath{\operatorname{\mathsf{who}}}, \ensuremath{\operatorname{\mathsf{state}}}, \ensuremath{\operatorname{\mathsf{clfn}}}, \ensuremath{\operatorname{\mathsf{cofn}}}$)
generated by the compiler can also appear.
We call compiler-generated identifiers \emph{synthetic}.
Normal identifiers are separated from synthetic ones to distinguish
compiler generated and developer code.
Definitions $\decl$ and definitions for synthetic identifiers $\syndecl$
are semicolon-separated lists of declarations that
assign values to variables and annotate either the contract or the client location.
\changed{Each program} $P$ consists of definitions $\decl$ and synthetic definitions $\syndecl$
followed by the main contract expression $\mainexp$.
Program $P$ corresponds to a single \textsf{Prisma}\xspace split class,
$\decl$ and $\syndecl$ to methods and generated methods,
and $\mainexp$ to a constructor containing the initialisation of its class members
(such as the body of \lstinline!init!, Fig.~\ref{fig:portable-class}).

Constants $c$ are unsigned 256\,bit integer literals and built-in operators.
$\textsf{MiniPrisma}\xspace_*$ supports tuples introduced by nesting pairs ($::$)
and eliminated by pattern matching.
Tuples allow multiple values to cross tiers in a single message.
Values $v$ are constants, value pairs, and lambdas.
Patterns $x$ are constants, pattern pairs, and variables.
Expressions $\subexp$ are constants, expression pairs, lambdas, variables,
  variable accesses/assignments, bindings and function applications.

Main expressions $\mainexp$ may further contain remote client expressions, 
embedding client code into contract code and waiting for its result.
The source client expression ${\downarrow}_s(e,~()\to e)$
can be answered by any client whose address fulfills the predicate specified as first argument.
$\downarrow_s$ corresponds to direct-style remote access via \lstinline!awaitCl! in \textsf{Prisma}\xspace.
We use the syntax form ${\downarrow}_t(c,~()\to e)$
to model the execution of code $e$ on the specified client $c$.
$\downarrow_t$ has no correspondence in the source syntax.
Our compilation first splits the predicate from the source client expressions
into a separate access control guard.
Then, it eliminates client expressions, 
turning the contract into a passive entity that 
stops and waits for client input.

We now map the hybrid language $\textsf{MiniPrisma}\xspace_*$ to 
the source and target languages, $\textsf{MiniPrisma}\xspace_s$ and $\textsf{MiniPrisma}\xspace_t$.
$\textsf{MiniPrisma}\xspace_s$ has all expressions of $\textsf{MiniPrisma}\xspace_*$,
except those that contain $\ensuremath{\,\operatorname{\mathsf{\gg\hspace{-2pt}=}}\,}$ (bind), $\ensuremath{\operatorname{\mathsf{trmp}}}$ (trampoline), $\mathsf{Done}$, $\mathsf{More}$, $\downarrow_t$,
or synthetic identifiers $j$.
$\textsf{MiniPrisma}\xspace_t$ has all expressions of $\textsf{MiniPrisma}\xspace_*$
except those that contain $\downarrow_s, \downarrow_t, \ensuremath{\,\operatorname{\mathsf{\gg\hspace{-2pt}=}}\,}$.
$\ensuremath{\,\operatorname{\mathsf{\gg\hspace{-2pt}=}}\,}$ and $\downarrow_t$ may neither appear in source nor target programs;
the former is only an intermediate compiler construct,
the latter is used
to track of the current evaluating location. %


\begin{figure}
  \figurehead
  \centering
  %
  \input{notes/def_fv_sugar_match.tex}
  \caption{Syntactic sugar.}
  \label{fig:sugar}
\end{figure}

\subparagraph{Syntactic sugar.}
In Fig.~\ref{fig:sugar}, we define some syntactic sugar to improve readability.
We use infix binary operators and tuple syntax for nested pairs ending in the unit value $()$;
we elide the let expression head for let bindings matching $()$,
$\ensuremath{\operatorname{\mathsf{assert}}}(x)$ is a let binding matching true;
we use monadic syntax for let bindings of effectful expressions; 
 $\ensuremath{\operatorname{\mathsf{if\,let}}\,} x = \mainexp \ensuremath{\operatorname{\,\mathsf{then}}\,} \subexp \ensuremath{\operatorname{\,\mathsf{else}}\,} \subexp$
is the application of the built-in $\ensuremath{\operatorname{\mathsf{try}}}$ function.


\subparagraph{Events and configurations.}
In Fig.~\ref{fig:syntax2}, we define left-to-right
evaluation contexts $E$~\cite{FelleisenH92};
and compilation frames $F$~\cite{Pitts00},
such that every expression decomposes into a frame-redex pair $F~\subexp$ or is an atom $\Finv$.
Events $\trace$ and $\syntrace$ are lists that capture
the observable side-effects of evaluating expressions.
They are either
(a)~state changes
  $\ensuremath{\mathsf{wr}}(c,\iden,v)$ and $\ensuremath{\mathsf{wr}}(c,\syniden,v)$,
  from the initial definitions or variable assignment,
  where $\iden$ and $\syniden$ are the variable being assigned, $c$ the location,
  and $v$ the assigned value, 
  or
(b)~client-to-contract communication $\ensuremath{\mathsf{msg}}(c,v)$,
  where $c$ is the address of the client and $v$ the sent value. 
Configurations $C = \trace;\syntrace;c \mainexp$, represent a particular execution state,
where $\trace$ (and $\syntrace$) are
traces of normal (and synthetic) events produced by the evaluation,
$c$ is the evaluating location, and $\mainexp$ is the expression under evaluation.

\begin{figure}
  \figurehead
  \centering
  \input{notes/syntax2.tex}
  \caption{Frames, Events and configurations.}
  \label{fig:syntax2}
  %
\end{figure}

\subparagraph{Initialization.}
Initialization in Fig.~\ref{fig:initialisation} generates the initial program configuration,
which
models the decentralized application with a single contract and multiple clients.
We model a fixed set of clients $A$ interacting with a contract.
The initialization of a program 
$\decl;\syndecl;\mainexp$
to a configuration 
$\trace;\syntrace;0;\mainexp$
  leaves the expression $\mainexp$ untouched
  and generates a
  %
  list of events
  -- one write event for each normal and synthetic 
  %
  definition.
Location 0 represents the contract.

\begin{figure}
	\figurehead
	\centering
  $\begin{array}{lll}
  init_A(\decl;\syndecl;\mainexp)
    &=& init_A(\decl;\syndecl);~0;~\mainexp \\
  init_A(\decl;\syndecl)
    &=& ( wr(0,\iden,v)    ~|~ \forall ~ (\ensuremath{\mathsf{@co\,this.}} \iden=v)    \in \decl ) \\
    & & ( wr(0,\syniden,v) ~|~ \forall ~ (\ensuremath{\mathsf{@co\,this.}} \syniden=v) \in \syndecl ) \\
    & & ( wr(c,\iden,v)    ~|~ \forall ~ (\ensuremath{\mathsf{@cl\,this.}} \iden=v)    \in \decl,~~ c \in A ) \\
    & & ( wr(c,\syniden,v) ~|~ \forall ~ (\ensuremath{\mathsf{@cl\,this.}} \syniden=v) \in \syndecl,~~ c \in A )
  \end{array}$
  \caption{Initialization.}
  \label{fig:initialisation}
\end{figure}

\subsection{Compilation}

The compiler eliminates language features
not supported by the compilation target
one by one, lowering the abstraction level from
  (1)~\emph{direct style communication (DS)} -- which needs language support for !-notation~\cite{idris-bang-notation} --
  through the intermediate representations of
  (2)~\emph{monadic normal form (MNF)} -- which needs support for do-notation~\cite{haskell-do-notation} -- and
  (3)~\emph{continuation-passing style (CPS)} -- which needs higher-order functions -- to
  (4)~explicitly encoding \emph{finite state machines (FSM)} -- for which first-order functions suffice.
In the following, we provide an intuition for the compiler steps
and subsequently their formal definitions.

First, the compilation steps $\mnfe$ and $\assoc$ transform DS remote communication ${\downarrow}\subexp$ 
to variable bindings ($x \gets \subexp$)
and nested let bindings are flattened such that a program is prefixed by a sequence of let expressions.
Second, step $\guarde$ generates access control guards around client expressions
to enforce correct execution even when clients behave maliciously.
Third, step $\dtle$ transforms previously generated let bindings for remote communication
($x \gets \subexp_1\ensuremath{;\;} \mainexp_2$) 
to monadic bindings $\subexp_1 \ensuremath{\,\operatorname{\mathsf{\gg\hspace{-2pt}=}}\,} x \to \mainexp_2$.
Fourth, step $\defun$ transforms functions into data structures that
can be sent over the network and are interpreted by a function (i.e., an FSM) 
on the other side.
Compared to standard defunctionalization, we handle two more issues.
First, we defunctionalize the built-in higher-order operator ($\ensuremath{\,\operatorname{\mathsf{\gg\hspace{-2pt}=}}\,}$) 
by wrapping the program expression into a call to a trampoline $\ensuremath{\operatorname{\mathsf{trmp}}}(...)$
  and transforming the bind operator ($... \ensuremath{\,\operatorname{\mathsf{\gg\hspace{-2pt}=}}\,} x \to ...$)
  to the $(\mathsf{More}, ..., ...)$ data structure;
 the trampoline repeatedly interprets the argument of $\mathsf{More}$ 
 %
  until it returns $\mathsf{Done}$ instead of $\mathsf{More}$ signaling the program's result.
  %
  %
Second, we keep contract and client functions separate
by generating separate synthesized interpreter functions, called $\mathsf{cofn}$ and $\mathsf{clfn}$,
  thereby splitting the code into the parts specific to contract and client.

\subparagraph{MNF transformation (Fig.~\ref{fig:mnf}).}
The $\mnfp$ function wraps the main expression $\mainexp$ into a call to the trampoline
with the pair $(\text{Done}, \mainexp)$ -- signaling the final result -- as argument.
Then, $\mnfe$ transforms expressions recursively,
binding sub-expressions to variables,
resulting in a program prefixed by a sequence of let bindings.
As recursive calls to $\mnfe$ may return chains of let bindings,
we apply $\assoc$ to produce a flat chain of let bindings.
Given a let binding, whose sub-expressions are in MNF,
associativity recursively flattens the expression,
by moving nested let bindings to the front,
($ ...~(...~\mainexp_0;~\mainexp_1);~\mainexp_2 = ...~\mainexp_0;~(...~\mainexp_0;~\mainexp_2) $),
creating a single MNF expression
(i.e., $\assoc$ is composition for MNF terms).

\begin{figure}
  \figurehead
  \centering
  %
  \input{notes/def_mnf.tex}
  \caption{Monadic normal form transformation.}
  \label{fig:mnf}
  %
\end{figure}

\begin{figure}
  \figurehead
  \centering
  %
  \input{notes/def_guard.tex}
  \caption{Guarding.}
  \label{fig:guard}
\end{figure}


\subparagraph{Guarding (Fig.~\ref{fig:guard}).}
We insert access-control guards
for remote communication expressions $\gets_s$ to enforce
(i)~the execution order of contract code after running the client expression and
(ii)~that the correct client invokes the contract continuation.
The transformation sets the synthetic variable $\mathsf{state}$ to a unique value before the client expression,
and stores the predicate to designate valid clients in the synthetic variable $\mathsf{who}$.
After the client expression, the generated code asserts that the contract is in the same state,
and checks that the sender fulfills the predicate.
The assertion trivially holds in the sequential execution of the source language,
but after more compilation steps the client will be responsible
for calling the correct continuation on the contract.
Since client code is untrusted, the contract needs to ensure
that only the correct client can invoke only the correct continuation.

\begin{figure}
  \figurehead
  \centering
  \input{notes/def_cps.tex}
  \caption{Continuation-passing style transformation.}
  \label{fig:rotation}
\end{figure}

\begin{figure}
  \figurehead
  \centering
  \input{notes/def_defun.tex}
  \caption{Defunctionalization.}
  \label{fig:defunctionalisation}
\end{figure}

\subparagraph{CPS transformation (Fig.~\ref{fig:rotation}).}
The  $\dtle$ transformation turns the
chains of let bindings produced by $\mnfe$ into
  CPS.
  The chain contains three cases
of syntax forms:
(1)~monadic binding ($x \gets ...\ensuremath{;\;} \mainexp_1$),
(2)~let binding ($ x = \subexp_0\ensuremath{;\;} \mainexp_1$),
or (3)~final expression.
For (1), $\dtle$ replaces the monadic binding with an explicit call to the bind operator ($... \ensuremath{\,\operatorname{\mathsf{\gg\hspace{-2pt}=}}\,} (x \to cps(\mainexp_1))$).
For (2) and (3), $\dtle$ recurses into the tail of the chain.
This resembles do-notation desugaring (e.g., in Haskell).


\subparagraph{Defunctionalization (Fig.~\ref{fig:defunctionalisation}).}
The $\defun$ function
transforms the chains of let bindings and bind operators produced by $\dtle$,
which contains three cases of syntax forms:
(1)~a bind operator ($\subexp_1 \ensuremath{\,\operatorname{\mathsf{\gg\hspace{-2pt}=}}\,} \subexp_2$),
or (2)~a let binding ($ x = \subexp_1\ensuremath{;\;} \subexp_2$),
or (3)~the final expression.
For (1), 
$\subexp_1$ and $\subexp_2$ are replaced by data structures
that contain values for the free variables in $\subexp_1$ and $\subexp_2$
and are tagged with a fresh ID.
The body of the expression is lifted to top-level synthetic definitions.
For this, $\defun$ modifies the synthetic definitions $b$
by extracting the body $\subexp_{1,alt}$ of the synthetic $\ensuremath{\operatorname{\mathsf{clfn}}}$ definition
and the body $\subexp_{2,alt}$ of $\ensuremath{\operatorname{\mathsf{cofn}}}$,
and by adding an additional conditional clause to these definitions.
The added clause answers to requests for a given ID with evaluating the original expression.
For (2) and (3), $\defun$ recurses into the expressions.

After defunctionalization, lambdas
$x \to \subexp_0$ are lifted and assigned a top-level identifier $id_0$
and lambda applications, $id_0(\subexp_1)$,
are replaced with calls to a synthesized interpreter 
function $\text{\textsf{fn}}(id_0, \subexp_1)$.
The latter branches on the identifier
and executes the code that was lifted out of the original function.



\subparagraph{Compiling.}
The $\mathit{comp}$ function composes the compiler steps after $\mathit{mnf}$:

\vspace{-1.1em}
\[ \begin{array}{ll}
\mathit{comp} &~=~ \defun ~\circ~ \dtle ~\circ~ \guarde \\
\mathit{comp}' &~=~ \defunOuter ~\circ~ \dtlp ~\circ~ \guardp
\end{array} \]



\subsection{Semantics}

We model the semantics as a reduction relation
over configurations $\trace;\syntrace;c;\mainexp \to \trace';\syntrace';c';\mainexp'$.
Location $c=0$ denotes contract execution, otherwise 
execution of client of address $c$.
We distinguish good ($\textcolor{blue}{\to_g}$)
and  bad ($\textcolor{red}{\to_b}$) evaluations
(Fig.~\ref{fig:dynamic-semantics} and~\ref{fig:dynamic-semantics2});
shared rules are in black, without subscript ($\to$).

\textit{Attacker model.}
Attackers can control an arbitrary number of clients
and make them send arbitrary messages.
Hence, the bad semantics can answer a request to a client
with an arbitrary message from an arbitrary $id$.
We use evaluation with bad semantics to show that our compiler enforces access control against malicious clients.

Good evaluations of client expressions in the source language (\textcolor{blue}{\textsc{Rgs}})
  and calls to the trampoline in the target language (\textcolor{blue}{\textsc{Rgt}})
  reduce to a client that fulfils
  the given predicate. We require that predicates evaluate purely.
  %
  Hence, $p$ and $q$ 
  %
  do not change in the
  evaluation.
On the other hand,
  bad evaluation of client expressions in the source language (\textcolor{red}{\text{Rbs}})
  and of calls to the trampoline in the target (\textcolor{red}{\textsc{Rbt}})
  ignore the predicate, choosing an arbitrary client.
The trampoline ends, when it reaches $\mathsf{Done}$ (\textsc{Rt}).
Further, after chosing a client to evaluate,
  the good evaluation (\textcolor{blue}{\textsc{Rg}}) continues to reduce the client expression to a value,
while the bad evaluation (\textcolor{red}{\textsc{Rb}}) replaces the expression $\subexp$
   with a (manipulated) arbitrary value $v'$.
Both evaluations (\textcolor{blue}{\textsc{Rg}}, 
\textcolor{red}{\textsc{Rb}}) emit the message event $\ensuremath{\mathsf{msg}}(c,v)$ and an assignment to the special variable $\mathsf{sender}$,
  when a client expressions is reduced to a value $v$, to record the client--contract interaction.


\begin{figure}
  \figurehead
  \centering
  %
  \input{notes/def_match.tex}
  \caption{Pattern matching.}
  \label{fig:pattern-matching}
\end{figure}

\begin{figure}
  \figurehead
  \centering
  \input{notes/dynamic_semantics.txt.tex}
  \caption{Evaluation (1/2).}
  \label{fig:dynamic-semantics}
  %
\end{figure}

\subparagraph{Common Evaluation} (Fig.~\ref{fig:dynamic-semantics2}).
Expressions %
are reduced under the evaluation context $E$ on the current location (\textsc{Re}),
assignment to variables is recorded in the trace (\textsc{Rset$^\circ$}),
accessing 
a variable
  is answered by the most recent assignment to it from the trace
   in the current location (\textsc{Rget$^\circ$}).
For synthetic variables,
  we use the synthetic store (\textsc{Rget$^\dagger$}, \textsc{Rset$^\dagger$}).
Binary operators are defined as unsigned 256\,bit integer arithmetic;
  we only show the rule for addition (\textsc{Rop}).
Further, we give rules for
  conditionals (\textsc{Rt}, \textsc{Rf}),
  let binding (\textsc{Rlet}) and
  function application (\textsc{Rlam})
  using pattern matching.
  %

\begin{figure}
  \figurehead
  \centering
  \input{notes/dynamic_semantics2.txt.tex}
  \caption{Evaluation (2/2).}
  \label{fig:dynamic-semantics2}
  %
\end{figure}

\subparagraph{Pattern matching (Fig.~\ref{fig:pattern-matching}).}
Matching $[x{\Mapsto}v]$ is a partial function, 
matching patterns $x$ with values $v$,
  returning substitution of variables $id$ to values.
Matching is recursively defined over pairs; it
  matches constants to constants,
  identifiers to values by generating substitutions,
  and fails otherwise.
Substitutions $[id{\mapsto}v]$, in turn, can be applied to terms $\subexp$, written $[id{\mapsto}v]~\subexp$ (capture-avoiding substitution). Substitutions $\sigma$ compose right-to-left $(\sigma\sigma') x = \sigma (\sigma' x)$.



\subsection{\changed{Secure} Compilation}
We prove that the \changed{observable} behavior \changed{of the contract}
before and after compilation is equivalent.
We capture the observable behavior
by execution traces
and show that trace equivalence holds even when the program is attacked,
i.e., reduced by $\textcolor{red}{{} \to_b^* {}}$.

\subparagraph{\changed{Modelling Observable Behavior}.}
The only source of \changed{observable} nondeterminism in the bad semantics is
 the evaluation of $\downarrow_s$ and $\downarrow_t$.
As clients decisions on message sending
  are influenced by the state of contract variables, tracking
  incoming client messages
  and state changes \changed{in the trace}
  suffices to capture the observable program behavior.
If the observable behavior is the same for the source and the compiled programs,
they are indistinguishable.
Thus, behavior preservation
  amounts to trace equality on programs before and after compilation.
Further, it suffices to model 
  equality for non-stuck traces.
The evaluation gets stuck (program crash) on assertions that guard against
    deviations from the intended program flow.
The Ethereum Virtual Machine
  reverts contract calls that crash, i.e., state changes of crashed calls do not take effect, hence, 
  stuck traces are not observable.

Since bad evaluation is nondeterministic,
  we work with 
  not just programs, expressions and configurations, but
  program sets, expression sets, and configuration sets.
Let $\trace;\syntrace;\mainexp \Downarrow$ be the trace set of the configuration $\trace;\syntrace;0;\mainexp$, e.g.,
  the set of tuples of the final event-sequence $\trace'$ and value $v$
  of all reduction chains
  that start in $\trace;\syntrace;0;\mainexp$
  and end in $\trace';0;\syntrace';v$.
Our trace set definition does not include
synthetic events $\syntrace'$ of the final configuration.
Synthetic events are introduced through compilation; excluding them
  allows us to put source and target trace sets in relation.
Further, let the trace set of a configuration set $T~\textcolor{red}{\Downarrow}$,
  be the union of the trace sets for each element:

\vspace{-1.2em}
\[\trace;\syntrace;\mainexp~\textcolor{red}{\Downarrow} ~~=~ \{~ (\trace',v) ~|~ (\trace;\syntrace;0;\mainexp)~\textcolor{red}{\to_b^*}~(\trace';\syntrace';0;v) ~\} \]

\vspace{-1.2em}
\[ T~\textcolor{red}{\Downarrow} ~=~ \bigcup_{\trace;\syntrace;\mainexp \in T} ~ \trace;\syntrace;\mainexp~\textcolor{red}{\Downarrow}\]

We say that two configuration sets $T$ and $S$ are equivalent, denoted by $T \approx S$, iff
$T$ and $S$ have the same traces sets:

\vspace{-1.2em}
\[(T~\textcolor{red}{\approx}~S)  ~~~\Leftrightarrow~~~  (T~\textcolor{red}{\Downarrow} ~=~ S~\textcolor{red}{\Downarrow})\]

\vspace{-0.2em}
By this definition,
  two expressions that eventually evaluate to the same value with the same trace are related by trace equality.
We use this notion of trace equality to prove that a source program is trace-equal to its compiled version
  by evaluating the compiled program forward \textcolor{red}{$\to_b^*$}
  and the original program backward \textcolor{red}{$\gets_b^*$}
  until configurations converge.

\subparagraph{\changed{Secure Compilation}.}
Theorem~\ref{theorem:trace-equality} states our correctness property\changed{,
which says that observable traces generated the malicious evaluation of programs
are preserved ($\textcolor{red}{\approx}$) by compilation.
The malicious evaluation models
  that client code has been replaced with arbitrary code,
  while contract code is unchanged.
The preservation of observable traces implies
  the integrity %
  of the (unchanged) contract code.
Secure} compilation
guarantees that developers can write safe programs
in the source language without knowledge about the compilation
or the distributed execution of client/contract tiers.

\begin{globaltheorem}[\changed{Secure} Compilation]\label{theorem:trace-equality}\emph{
For each program $P$ over closed terms, the trace set of
the program under attack
equals the trace set of
the compiled program under attack:
$ \forall P.\, \{~ init_A(comp'(mnf'((P)))) ~\}~\textcolor{red}{\approx}~\{~ init_A(P) ~\} $.
}\end{globaltheorem}

We first show that trace equality holds for the different compiler steps.
Some compiler steps are defined as a recursive term-to-term transformation on open terms,
whereas traceset equality is defined by reducing terms to values, i.e., on closed terms.
Since all evaluable programs are closed terms,
we show that the compiler steps preserve the traceset of an open term $e$ that 
is closed by substitution $[x\Mapsto v]$. We formulate the necessary lemmas and sketch the proofs -- the detailed proof is in Appendix~\ref{appendix:proofs}.

{\small
\begin{globallemma}[assoc correct]\label{lemma:assoc}
$\{\, \trace;\syntrace; [x{\Mapsto}v]\,assoc(\mainexp) \,\} \approx \{\, \trace;\syntrace; [x{\Mapsto}v]\,\mainexp \,\}$
\end{globallemma}
\begin{globallemma}[mnf correct]\label{lemma:mnf}
$\{\, \trace;\syntrace; [x{\Mapsto}v]\,mnf(\mainexp) \,\} \approx \{\, \trace;\syntrace; [x{\Mapsto}v]\,\mainexp \,\}$
\end{globallemma}
\begin{globallemma}[mnf' correct]\label{lemma:mnf'}
$\{\, init_C(mnf'(\decl;\syndecl; \mainexp)) \,\} \approx \{\, init_C(\decl;\syndecl; \mainexp) \,\}$
\end{globallemma}
\begin{globallemma}[comp correct]\label{lemma:comp}
$\{\, [x{\Mapsto}v]\,init_A(comp(\decl;\syndecl; \ensuremath{\operatorname{\mathsf{trmp}}}(\mainexp))) \,\} \approx \{\, init_A(\decl;\syndecl; \ensuremath{\operatorname{\mathsf{trmp}}}([x{\Mapsto}v]\,\mainexp)) \,\}$
\end{globallemma}
\begin{globallemma}[comp' correct]\label{lemma:comp'}
$\{\, [x{\Mapsto}v]\,init_A(comp'(\decl;\syndecl; \ensuremath{\operatorname{\mathsf{trmp}}}(\mainexp))) \,\} \approx \{\, init_A(\decl;\syndecl; \ensuremath{\operatorname{\mathsf{trmp}}}([x{\Mapsto}v]\,\mainexp)) \,\}$
\end{globallemma}
}
\subparagraph{Proof sketch.}
Lemma~\ref{lemma:assoc}--\ref{lemma:comp'} hold by chain of transitive trace equality relations.
We show that a term is trace-equal to the same term after compilation,
  by evaluating the compiled program (${\to}^*$)
  and the original program (${\gets}^*$)
  until configurations converge.
In the inductive case,
  we can remove the current compiler step in redex position under traceset equality ($\approx$)
  since traces before and after applying the compiler step are equal by induction hypothesis.

An interesting case is the proof of $\mathit{comp}$ for $P = \decl;\syndecl; \downarrow(\subexp_0, () \to \subexp_1)$.
The compiler transforms the remote communication $\downarrow_s$
  into the use of a guard and a trampoline.
The compiled program steps to the use of $\downarrow_t$,
the source program to $\downarrow_s$.
In the attacker relation $\textcolor{red}{\to_b}$,
  arbitrary clients can send arbitrary values with $\downarrow_t$,
  leading to additional traces compared to the ones permitted in the source program.
  where communication is modeled by $\downarrow_s$.
We observe that $\downarrow_s$ generates the trace elements
$\ensuremath{\mathsf{msg}}(c, \textcolor{red}{v}), \ensuremath{\mathsf{wr}}(0, \mathrm{sender}, c)$ for all $\textcolor{red}{v}$
and that $\downarrow_t$ generates the trace elements
$\ensuremath{\mathsf{msg}}(\textcolor{red}{c'}, \textcolor{red}{v}), \ensuremath{\mathsf{wr}}(0, \mathrm{sender}, \textcolor{red}{c'})$
for all $\textcolor{red}{v}, \textcolor{red}{c'}$,
which differ for $\textcolor{red}{c'} \ne c$.

Compilation adds an $\mathsf{assert}$ expression (Fig.~\ref{fig:guard})
evaluated after receiving a value from a client.
The $\mathsf{assert}$ gets stuck for
configurations
that produce trace elements with $\textcolor{red}{c'} \ne c$,
removing the traces of such configurations from the
trace set,
leaving only the traces where $\textcolor{red}{c'} = c$.
Hence, the trace set before and after compilation is equal under attack.




\section{Implementation}

\changed{
\textsf{Prisma}\xspace is a language embedded into Scala as a host language.
\textsf{Prisma}\xspace's features are implemented as a source-to-source macro that transforms Scala code to Scala code.
The implementation entails 21 Scala files, 3\,412
lines of Scala source code (non-blank, non-comment) licensed under Apache 2.0 Open Source.
In addition to the source code of the compiler, we implemented several case studies in \textsf{Prisma}\xspace.
We further implemented the case studies in Solidity, and test runners in JavaScript for them.
A visual comparison of the LOC for the \textsf{Prisma}\xspace vs the Solidity case studies
can be found in Appendix~\ref{appendix:loc-evaluation}.
}

\changed{
\textsf{Prisma}\xspace{} contains implementation of the serialisable datatypes, portable between Scala and the EVM (fixed-size arrays, dynamic arrays, unsigned integers of length of powers of two up to 256 bit).
Our compiler implementation is based on Scala macros.
The compiler phases are macros recursing over the Scala AST:
namely the guarding phase,
and the ``simplifying'' phase (including MNF translation, CPS translation of terms, defunctionalisation)
and the translation of (a subset) of Scala expressions and types
to an custom intermediate representation based on Scala case classes.
The intermediate representation is translated to Solidity code,
and passed to the Solidity compiler (solc).
Our runtime wraps \lstinline!web3j!~\cite{web3j-github} (for invoking transactions and interacting with the blockchain in general)
and \lstinline!headlong!~\cite{headlong-github} (for serialisation/deserialisation in the Ethereum-specific serialisation format),
as well code to parse of Solidity and Ethereum error messages to translate them to Scala error messages.
}



\changed{
The backend to Solidity is well separated.
By disabling the compilation step to Solidity in the compilation pipeline,
we could also run distributed code on multiple JVMs instead, for example.
In this case, the "contract code" would be executed by a computer to serve as the "server", and other computers would run the "client code" to interact with the server.
}


\section{Evaluation}
\label{sec:discussion}

We evaluate \textsf{Prisma}\xspace along two research questions:

\begin{enumerate}[label=RQ\arabic*]
	\setlength{\itemindent}{2em}
	\item \label{rq-expressiveness} \emph{Does \textsf{Prisma}\xspace support the most common dApps scenarios?}
	%


	\item \label{rq-efficiency} \emph{Do \textsf{Prisma}\xspace's abstractions
        %
        affect performance?}
\end{enumerate}

\subparagraph{Case Studies and Expressiveness (\ref*{rq-expressiveness}).}
Five classes of smart contract
applications have been identified \cite{bartoletti2017empirical}: Financial, Wallet, Notary, Game, and Library.
To answer \ref{rq-expressiveness}, we implemented at least one 
case study per category in \textsf{Prisma}\xspace.
We implemented an ERC-20 Token,\!%
\footnote{A study investigating all blocks mined until Sep 15, 2018~\cite{oliva2020exploratory},
	found that 72.9\,\%
	with an accumulated market capitalization of 12.7\,B~USD.}
a Crowdfunding, and an Escrowing dApp as representatives of financial dApps.
We cover \emph{wallets}
by implementing a multi-signature wallet, a special type of wallet that provides a transaction voting mechanism by only executing transactions, which are signed by a fixed fraction of the set of owners.
We implemented a general-purpose \emph{notary} contract enabling
users to store arbitrary data, e.g., document hashes or images, together with a submission timestamp and the data owner.
As \emph{games}, we implemented TicTacToe (\changed{Section}~\ref{sec:the-language}),
Rock-Paper-Scissors, Hangman and Chinese Checkers.
Rock-Paper-Scissors makes use of timed commitments~\cite{DBLP:conf/sp/AndrychowiczDMM14},
i.e., all parties commit to a random seed share and open it
after all commitments have been posted.
The same technique can be used to generate randomness for dApps in a secure way.
To reduce expensive code deployment, developers outsource 
commonly used 
logic to library contracts.
We demonstrate \emph{library}-based development in \textsf{Prisma}\xspace by including a TicTacToe library
to our case studies and another 
TicTacToe dApp
which uses that library instead of deploying the logic itself.

We implemented a state channel~\cite{MBBKM19, DziembowskiFH18, DziembowskiEFHH19}
for TicTacToe in \textsf{Prisma}\xspace.
State channels are
\emph{scalability solutions} enabling parties to move their dApp
to a non-blockchain consensus system, falling-back
to the blockchain in case of disputes.

Our case studies are between 1\,K and 7.5\,K bytes which is a representative size: %
	Smart contracts are not built for large-scale applications
	since the gas model limits the maximal computation and storage volumes and
	causes huge fees for complex applications.
	The median (average, lower quantile, upper quantile) of the bytecode size of distinct contracts deployed at the time of writing is at 4\,K (5.5\,K, 1.5\,K, 7.5\,K)~\cite{google-cloud-big-query-contract-size}. %
We 
further elaborate on the case studies
in Appendix \ref{appendix:case-studies}.

\begin{figure*}
    \input{paper/graphs/deploymentCosts}
    \input{paper/graphs/deploymentOverhead}
    \input{paper/graphs/executionCosts}
    \input{paper/graphs/executionOverhead}
    \caption{
        The cost of abstraction. Gas overhead of contracts written with \textsf{Prisma}\xspace vs. Solidity. \\
        (The right plot displays minima, averages, maxima.)
    }
    \label{fig:gas-costs}
    \label{fig:gas-overhead}
    \vspace{-1em}
\end{figure*}

\subparagraph{Performance of Prisma DApps (\ref*{rq-efficiency}).}
\changed{Performance on the Ethereum blockchain is usually measured in terms of an Ethereum-specific metric called \textit{gas}.
Each instruction of the Ethereum Virtual Machine (EVM) consumes gas which needs to be paid for by the users in form of transaction fees credited to the miner.
We refer to the Ethereum yellow paper~\cite{ethereum-yellow-paper} for an overview of the gas consumption of the different EVM instructions.}
To answer \ref{rq-efficiency}, we implement 
our case studies in both \textsf{Prisma}\xspace and in Solidity/JavaScript
and compare their 
gas consumption.
Unlike prior work, 
we do not model a custom gas structure, but consider the real EVM gas costs \cite{wood2014ethereum}.

\emph{Experimental setup.}
We execute each case study on different inputs
to achieve different execution patterns that
cover all contract functions.
Each contract invocation that includes parameters with various sizes
(e.g., dynamic length arrays) is executed with a range of realistic inputs,
e.g., for Hangman, we consider several words (2 to 40 characters)
and different order of guesses, covering games in which the guesser wins
and those in which they lose.
\textsf{Prisma}\xspace and Solidity/JavaScript implementations are executed on the same inputs.

We perform the measurements on a local setup.
As the execution
in the Ethereum VM is deterministic,
a single measurement suffices.
We set up the local Ethereum blockchain with \textit{Ganache} (Core v2.13.2)
on the latest supported hard fork (Muir Glacier).
All contracts are compiled to EVM byte code with \textit{solc} (v0.8.1, optimized on 20 runs).
We differentiate contract deployment and contract interaction.
Deployment means uploading the contract to the blockchain and initializing its state,
which occurs just once per application instance.
A single instance typically involves several contract interactions,
i.e., transactions calling public contract functions.

\emph{Results.}
Fig.~\ref{fig:gas-costs} shows the average gas consumption of contract deployment (Fig.~\ref{fig:eval-deployment-cost}) and interaction (Fig.~\ref{fig:eval-execution-cost}) as well as the relative overhead of Prisma vs. Solidity/JS of deployment (Fig.~\ref{fig:eval-deployment-overhead}) and interaction (Fig.~\ref{fig:eval-execution-overhead}).
As the gas consumption of contract invocations depends heavily on the executed function,
the contract state, and the inputs, we provide the maximal, minimal and averaged overhead. 
The results show that the average gas consumption
of \textsf{Prisma}\xspace is close to the one of Solidity/JS.
Our compiler achieves a deployment overhead of maximally 6\,\%
The interaction overhead is below 10\,\%
which at most amounts to 3.55\,K gas.\!\footnote{equals 0.59~USD based on gas price and exchange course of April 15, 2021}


\textsf{Prisma}\xspace's deployment overhead is mainly due to the automated flow control.
To guarantee correct execution, \textsf{Prisma}\xspace manages a state variable
for dApps with more than one state.
The storage reserved for and the code deployed to maintain the state variable
cause a constant cost
of around 45\,K gas.
In Solidity, developers manually check whether flow control is needed
and, if so, may derive the state from existing
contract variables to avoid a state variable if possible.

The Token, Notary, Wallet and Library case studies do not require flow control:
each function can be called by any client at any time.
Hence, their overhead is small.
Escrow, Hangman and Rock-Paper-Scissors require a state variable, also in Solidity
-- which partially compensates the overhead of \textsf{Prisma}\xspace's automated flow control.
Crowdfunding, Chinese Checkers, TicTacToe (Library and Channel) do not require an explicit state variable in Solidity, as the state can be derived from the contract variables,
e.g., the number of moves.
Thus, these case studies have the largest deployment overhead.

While the average relative interaction overhead is constantly 
below 10\,\%
e.g., in Crowdfunding, TicTacToe Channel, and Rock-Paper-Scissors.
Yet, case studies with such spikes also involve interactions
that are executed within the same dApp
instance with a negative overhead and amortize the costs of more costly transactions.
These deviations are also mainly due to 
automated flow control.
In EVM, setting a zero variable to some non-zero value costs more
gas (20\,K gas) than changing its value (5\,K gas)~\cite{wood2014ethereum}, and setting the value to zero saves gas.
Occupying and releasing storage via the state variable can cost or
save gas in a different way than in traditional dApps
without an explicit state variable, leading to different (and even negative) overhead in different transactions.


As \textsf{Prisma}\xspace preserves the number of contract interactions, the on-chain execution time of dApps is not affected by our compiler. In Ethereum, the estimated confirmation time for transactions is 3-5~minutes (assuming no congestion), which makes on-chain execution dominate the total execution time. Thus, the overhead of \textsf{Prisma}\xspace,
if any, is negligible.

Note that per se it is not possible to achieve a better gas consumption in \textsf{Prisma}\xspace than in Solidity -- every contract compiled from \textsf{Prisma}\xspace can be implemented in Solidity.
Given the abstractions we offer beyond the traditional development approach,
and the sensibility of smart contracts
to small changes in instructions, we conclude that our abstractions come
with acceptable cost.
We are confident that further engineering effort can eliminate the observed overhead.

\emph{Threats to validity.}
The main threat
is that the manually written code may be optimized better or worse than the code generated by the compiler.
We mitigate this threat by applying all gas optimizations, our compiler performs automatically,
to the Solidity implementations.
An external threat is that changes in the gas pricing of Ethereum may affect our evaluation.
For reproducibility, we state the Ethereum version (hard fork), we used in the paper.

\begin{table}\figurehead\centering
  \caption{Related work.}\label{tab:related-work-style}
  \begin{tabular}{lllll}
    \toprule
    Language & Encoding & Perspective  & Protocol      \\
    \midrule
    Solidity & FSM      & Local        & Assertions    \\
    Obsidian & FSM      & Local        & Type states   \\
    Nomos    & MNF      & Local        & Session types \\
    \midrule
    \textsf{Prisma}\xspace & DS       & Global       & Control flow  \\
    \bottomrule
  \end{tabular}
  \vspace{-1.2em}
\end{table}



\section{Conclusion}
\label{sec:conclusion}

We proposed \textsf{Prisma}\xspace, the first global language for dApps that features direct style communication. 
Compared to the state of the art, \textsf{Prisma}\xspace (a)~enables the implementation of contract and client logic within the same development unit, rendering intricacies of the heterogeneous technology stack obsolete and avoiding boilerplate code, (b)~provides support for explicitly encoding the intended program flow and (c)~reduces the risk of human failures by enforcing the intended program flow and forcing developers to specify access control.

Unlike previous work that targeted challenges in the development of dApps with advanced typing disciplines 
e.g., session types, our model does not exhibit visible side effects
and  gets away with a standard System-F-style type system.
We describe the design and the main features of \textsf{Prisma}\xspace informally, define its formal semantics, formalize the compilation process and prove it correct.
We demonstrate \textsf{Prisma}\xspace's applicability via case studies and performance benchmarks.

We plan to generate state channels
-- to optimistically cost-optimize dApps --
similar to how we generate state machines from high-level logic.
Further, we believe that
our technique for deriving the communication protocol from direct-style control flow
generalizes beyond the domain of smart contracts and we will
explore its further applicability.


\section{Proofs}
\label{appendix:proofs}

\setcounter{globallemma}{0}
\setcounter{globaltheorem}{0}

We provide the definition of $\mathsf{comp}'$ and $\mathsf{comp}$ in Figure~\ref{fig:comp},
the definition for the free variables for a given term $\fv$ in Figure~\ref{fig:free-variables}
and the detailed proofs for the theorem and the lemmas on the following pages.

\vspace{3em}

\begin{figure}
$\begin{array}{llll}
comp'(\decl; \syndecl; \ensuremath{\operatorname{\mathsf{trmp}}}(\mainexp)) &~=~&
  \decl\ensuremath{;\;} \compilestep{coclfn}(\syndecl, id, \ensuremath{\operatorname{\mathsf{assert}}}(\ensuremath{\operatorname{\mathsf{false}}}), \ensuremath{\operatorname{\mathsf{assert}}}(\ensuremath{\operatorname{\mathsf{false}}}))\ensuremath{;\;} \ensuremath{\operatorname{\mathsf{trmp}}}(comp(\mainexp))\\
&& \begin{array}{ll} \text{where} & id \ensuremath{\operatorname{\mathsf{fresh}}} \end{array}\\[1em]

comp\left(\begin{array}{l}
  \decl; \compilestep{coclfn}(\syndecl, id,\\~~\subexp_{1,alt},\\~~\subexp_{2,alt});\\
  tmp \gets_s (() \to \subexp_1)\ensuremath{;\;} \subexp_2
\end{array}\right) &~=~& \left(\begin{array}{l}
  \decl; \compilestep{coclfn}(\syndecl, id,\\
  ~~\ensuremath{\operatorname{\mathsf{if\,let}}\,} (c :: \fv(() \to \subexp_1)) = id \ensuremath{\operatorname{\,\mathsf{then}}\,} \subexp_1 \ensuremath{\operatorname{\,\mathsf{else}}\,} \subexp_{1,alt}',\\
  ~~\ensuremath{\operatorname{\mathsf{if\,let}}\,} (c :: x :: \fv(x \to \subexp_2')) = id \ensuremath{\operatorname{\,\mathsf{then}}\,} \\
  ~~~~~~\ensuremath{\operatorname{\mathsf{assert}}}(\ensuremath{\mathsf{this}}.\ensuremath{\operatorname{\mathsf{state}}} == c \,\operatorname{\&\&}\, \ensuremath{\mathsf{this}}.\ensuremath{\operatorname{\mathsf{who}}}(\ensuremath{\mathsf{this}}.\ensuremath{\operatorname{\mathsf{sender}}}))\ensuremath{;\;} \\
  ~~~~~~\ensuremath{\mathsf{this}}.\ensuremath{\operatorname{\mathsf{state}}} := 0\ensuremath{;\;} \subexp_2' \\
  ~~\ensuremath{\operatorname{\,\mathsf{else}}\,}\\
  ~~~~~~ \subexp_{2,alt}');\\
  \ensuremath{\mathsf{this}}.\ensuremath{\operatorname{\mathsf{who}}} := \subexp_0\ensuremath{;\;} \ensuremath{\mathsf{this}}.\ensuremath{\operatorname{\mathsf{state}}} := c\ensuremath{;\;} \\
  (\mathsf{More},~ c :: \fv(() \to \subexp_1),~ c :: \fv(x \to \subexp_2'))
\end{array}\right)
\\[2.5em]
&& \begin{array}{ll}
     \text{where} & c \ensuremath{\operatorname{\mathsf{fresh}}}\\
     \text{and}   & \decl; \compilestep{coclfn}(\syndecl, id, \subexp_{1,alt}', \subexp_{2,alt}'); \subexp_2' =\\
                  & ~~ \defun[\decl; \compilestep{coclfn}(\syndecl, id, \subexp_{1,alt}, \subexp_{2,alt}); \subexp_2]\\
   \end{array}
\\

comp\left(\begin{array}{l}
  \decl; \compilestep{coclfn}(\syndecl, id, \subexp_{1,alt}, \subexp_{2,alt});\\
   x = \subexp_0; ~ \subexp_1
\end{array}\right) &~=~& \left(\begin{array}{l}
  \decl; \compilestep{coclfn}(\syndecl, id, \subexp_{1,alt}, \subexp_{2,alt});\\
   x = \subexp_0; ~ \defun(\subexp_1)
\end{array}\right)
\\

comp\left(\begin{array}{l}
  \decl; \compilestep{coclfn}(\syndecl, id, \subexp_{1,alt}, \subexp_{2,alt});\\
  \subexp
\end{array}\right) &~=~& \left(\begin{array}{l}
  \decl; \compilestep{coclfn}(\syndecl, id, \subexp_{1,alt}, \subexp_{2,alt});\\
  \subexp
\end{array}\right)
\\[2em]

\compilestep{coclfn}(\syndecl, id, \subexp_{1,alt}, \subexp_{2,alt}) &~=~&
  (\ensuremath{\mathsf{@cl\,this.}} \ensuremath{\operatorname{\mathsf{clfn}}} = id \to \subexp_{1,alt}); (\ensuremath{\mathsf{@co\,this.}} \ensuremath{\operatorname{\mathsf{cofn}}} = id \to \subexp_{2,alt}); b
\\
\end{array}$
\caption{$\mathsf{comp}'$ and $\mathsf{comp}$.}
\label{fig:comp}
\end{figure}

\vspace{3em}

\begin{figure}
  \input{notes/def_fv.tex}
  \caption{Free variables.}
  \label{fig:free-variables}
\end{figure}

\vspace{5em}

\clearpage{}


\begin{globaltheorem}[\changed{Secure Compilation}]\emph{
For all programs $P$ over closed terms, the trace set of evaluating the program under attack
equals the trace set of evaluating the compiled program under attack,
i.e.,
\[ \forall P. ~~~ \{~ init_A(comp'(mnf'((P)))) ~\} \approx ... \approx \{~ init_A(P) ~\}  \]
}\end{globaltheorem}

\begin{proof}
\[ \begin{array}{cl}
                                                   &~ init_A(comp'(mnf'(P)))\\
~\overset{\text{Lemma }\ref{lemma:mnf'}}{\approx}  &~ init_A(mnf'(P))\\
~\overset{\text{Lemma }\ref{lemma:comp'}}{\approx} &~ init_A(P)\\
\end{array} \]
\end{proof}

\subparagraph{Extensions}

For simplicity, our definition of initialization uses a fixed set of clients.
Yet, the malicious semantics does not actually depend on the fixed set of clients,
but instead models an attacker that is in control of all clients
with the capability of sending messages from any client, not bound to the fixed set.
Hence, it is straightforward to extend the proofs to the setting of a dynamic set of clients, e.g.,
clients joining and leaving at run time.

Further, our trace equality relation defines that all programs
in the relation eventually reduce to values, filtering out programs that loop or get stuck.
Below, we outline an approach to prove trace equality for looping or stuck programs
by showing that such programs loop with the same infinite trace
or get stuck at the same trace, respectively.
To this end, we track the number of steps done via a step-indexed trace equality relation:
\[ p;q;e \Downarrow^n ~~=~ \{~ (p',v) ~|~ (p;q;e) \to^n (p';q';v) ~\}
~~~~~~~~~~~~~~~~~~~~~~~~~
   T \Downarrow^n ~=~ \bigcup_{p;q;e \in T} ~ p;q;e \Downarrow^n      \]

With this definition, we can no longer use just equality of traces as the left and right program
may take a different number of steps to produce the same events.
Instead, we move from an equality relation to a relation stating non-disagreement, which says that
-- independently of how long we run either statement --
the traces will never be in disagreement:
\[ (T \approx^n S)  ~~~\Leftrightarrow~~~  (T\Downarrow^n ~\#_{\text{set}}~ S\Downarrow^n) \]

where $\#_\text{set}$ is defined on trace sets as
\[ T \#_{\text{set}} S  ~~~\Leftrightarrow~~~
(\forall t {\in} T.~ \exists s {\in} S.~~ t ~\#_{\text{trace}}~ s) \land
(\forall s {\in} S.~ \exists t {\in} T.~~ t~ \#_{\text{trace}}~ s) \]

and $\#_\text{trace}$ on event traces as
\[ \begin{array}{llllll}
(ev,   &())     &\#_{\text{trace}}& (ev,   &tail_2) &= true \\
(ev,   &tail_1) &\#_{\text{trace}}& (ev,   &())     &= true \\
(ev_1, &tail_1) &\#_{\text{trace}}& (ev_2, &tail_2) &= false \\
(ev,   &tail_1) &\#_{\text{trace}}& (ev,   &tail_2) &= tail_1 ~\#_{\text{trace}}~ tail_2 \\
\end{array}. \]


\clearpage{}\input{notes/lemma_assoc_preserves.txt.tex}
\clearpage{}\input{notes/lemma_mnfe_preserves.txt.tex}
\clearpage{}\input{notes/lemma_mnfp_preserves.txt.tex}
\clearpage{}\input{notes/lemma_dtle_preserves.txt.tex}
\clearpage{}\input{notes/lemma_dtlp_preserves.txt.tex}


\clearpage{}







\section{Discussion and Related Work}
\label{sec:background}

\subparagraph{Smart Contract Languages for Enforcing Protocols.}
We compare \textsf{Prisma}\xspace to Solidity,
Obsidian~\cite{Coblenz17, Coblenz19, Coblenz20}, and
Nomos~\cite{DasBHP19, Nomos21}.
We highlight these languages as those also address the 
correctness of the client--contract interactions.
Tab.~\ref{tab:related-work-style} overviews the features of the surveyed languages for
(a)~the \emph{perspective} of defining interacting parties,
(b)~the used \emph{encoding} of the interaction effects, 
and (c)~the method used to check the contract-client interaction \emph{protocol}.
Fig.~\ref{fig:solidity}, \ref{fig:type-states}, and~\ref{fig:session-types}
show code snippets in these languages,
each encoding the \emph{TicTacToe} state machine from Fig.~\ref{fig:funding-diagram}.
All three languages focus solely on the contract and do not state how clients are developed, 
hence only contract code is shown.

\begin{figure}[b]\figurehead
  \input{paper/listings/obsidian_ttt.tex}
  %
  \caption{Obsidian.}\label{fig:type-states}
  \vspace{-1em}
\end{figure}

\begin{figure}\figurehead
  \input{paper/listings/nomos_ttt.tex}
  %
  \caption{Nomos.}\label{fig:session-types}
\end{figure}

\begin{figure*}
    \begin{mathpar}
        \inferrule[NomosR]{
            \Psi;\Gamma,(y{:}A) \vdash P :: (c : B)
        }{
            \Psi;\Gamma \vdash (y {\gets} \mathsf{recv}~c;~P) :: (c : A \multimap B)
        }
        
        \inferrule[NomosS]{
            \Psi;\Gamma \vdash P :: (c : B)
        }{
            \Psi;\Gamma,(w{:}A) \vdash (\mathsf{send}~c~w;~P) :: (c : A \otimes B)
        }
        
        \inferrule[Obsidian]{
            (\mathsf{transaction}~T~m(\overline{t.(s \text{>>} s')~x}) \{ ... \}) \in \text{members}_{t_0}
        }{
            \Delta,\overline{e{:}t.s}
            \vdash
            e_0.m(\overline{e}) : T \dashv \Delta,\overline{e{:}t.s'}
        }
    \end{mathpar}
    \caption{Excerpts of simplified Nomos and Obsidian typing rules.}\label{fig:typing}
\end{figure*}

All three approaches take a \textbf{local perspective} on interacting parties:
Contract and clients are defined separately, and 
their interaction is encoded by explicit send and receive side effects.
In Solidity and Obsidian, receive corresponds to arguments and send to return values
of methods defined in the contract classes.
In Nomos, send and receive are expressed as procedures operating over a channel -- given a channel \lstinline!c!, sending and receiving is represented by explicit statements (\lstinline!x = recv c; ...! and \lstinline!send c x; ...!).


The approaches differ in the \textbf{encoding style}
of communication effects.
Solidity and Obsidian adopt an \emph{FSM-style encoding}:
Contract fields encode states, methods encode transitions.
The contract in Fig.~\ref{fig:solidity}
represents FSM states via the \lstinline!phase! field with initial state 
\lstinline!Funding! (Line~\ref{code:solidity-init-phase}).
The
\lstinline!Fund!, \lstinline!Move! and \lstinline!Payout! methods are transitions, e.g.,
\lstinline!Payout! transitions the contract into 
the final state  \lstinline!Closed! (Line~\ref{code:solidity-to-final-phase}).
The FSM-style encoding results in an implicitly-everywhere 
concurrent programming model, which is complex to reason about and unfitting for dApps
because the execution model of blockchains is inherently sequential -- all method invocations are brought into a world-wide total order.
Nomos adopts the \emph{monadic normal form~(MNF)}
via do-notation to order effects. 
While the implementation of TicTacToe  in \changed{FSM style} requires three methods(\lstinline!Fund!, \lstinline!Move!, \lstinline!Payout! -- one per transition), we only need two methods in MNF-style (\lstinline!funding!, \lstinline!executing! -- one per state with multiple entry points), and a single method in DS-style (\lstinline!init!).
For instance, the sequence of states and transitions
$Executing
\hspace{-0.35em}\raiseoperator{-0.13ex}{\closeoverset[0.43ex]{Move(x, y)}\longrightarrow}
Finished
\hspace{-0.35em}\raiseoperator{-0.13ex}{\closeoverset[0.43ex]{Payout()}\longrightarrow}
Closed$
in Nomos
can be written sequentially in do-notation
by inlining the last function which only has a single entry point.
Still, do-notation can be cumbersome
(e.g., funding and executing in Nomos are separate methods
that cannot be inlined since they have multiple entry points and model loops).



All three languages require an \textbf{explicit protocol}
for governing the 
send--receive interactions, to
ensure that every send effect has a corresponding receive effect 
in an interacting -- separately defined -- party.
In Solidity, developers express the protocol via 
run-time assertions to guard 
against invoking the methods
in an incorrect order
(e.g., \lstinline!require(phase==Finished)! in Fig.~\ref{fig:solidity}, Line~\ref{code:solidity-require-funding}).
Unlike Solidity, which does not support statically checking protocol compliance,
Nomos and Obsidian employ \emph{behavioral typing} for static checks.
Deployed contracts may interact with 
third-party, potentially manipulated clients.
Compile-time checking alone
cannot provide security guarantees.
Yet, 
complementing run-time enforcement with static checks 
helps detecting cases that are guaranteed to fail at run time ahead of time.







\emph{Obsidian}
employs typestates to increase safety of contract--client communication.
Contracts define a number of typestates; 
A method call can change the typestate of an object,
and calling a 
method on a receiver that is in the wrong typestate results in a typing error.
Each method in Fig.~\ref{fig:type-states}
is annotated with the state in which it can be called, e.g., \lstinline!Payout! 
requires state
\lstinline!Finished!,
and transitions to
\lstinline!Closed! (Line~\ref{code:obsidian-payout}).

\emph{Nomos} employs session types.
The session types \lstinline!Funding!, \lstinline!Executing!, \lstinline!Finished!
in Fig.~\ref{fig:session-types} encode the protocol.
Receiving a message is represented by a function type,
e.g., in the \lstinline!Funding! state,
we receive an integer \lstinline!int -> ...! (Line~\ref{code:nomos-type-funding}).
We respond by either repeating the funding (\lstinline!Funding!), or continuing
to the next state of the protocol (\lstinline!Executing!). This 
is represented by internal choice \lstinline!+{ ... }!
that takes multiple possible responses giving each of them a unique label (\lstinline!notenough! and \lstinline!enough!).
Type \lstinline!1! indicates the end of a protocol (Line~\ref{code:nomos-type-finished}).
The contract processes \lstinline!funding! (Line~\ref{code:nomos-process-funding}) and \lstinline!executing! (Line~\ref{code:nomos-process-executing}) implement the protocol.
The \lstinline!recv! operation (Line~\ref{code:nomos-receive}) takes a session-typed channel
of form \lstinline'T -> U', returns a value of type \lstinline!T!
and changes the type of the channel to \lstinline!U!.
A session type for internal choice (\lstinline!+{ ... }!),
requires the program to select
one of the offered labels (e.g., \lstinline!$$s.notenough! in Line~\ref{code:nomos-decision-notenough} and \lstinline!$$s.enough! in Line~\ref{code:nomos-decision-enough}),
e.g., in the left and right branch of a conditional statement.












\textit{Type systems.}
\label{sec:typing-comparison}
We show excerpts of simplified typing rules
for Nomos and Obsidian (Fig.~\ref{fig:typing}).
Nomos rules
have the form $\Psi;\Gamma \vdash P :: (c{:}A)$.
A process $P$ offers a channel $c$ of type $A$ with
values in context $\Psi$ and channels in $\Gamma$.
We can see that variables change their type to model the linearity of session types
in the \textsc{NomosS} (and \textsc{NomosR}) rule:
Sending (and receiving) changes the type of the channel $c$
from $A {\multimap} B$ to $B$
(and $A {\otimes} B$ to $B$).
Obsidian rules have the form $\Delta \vdash e{:}t \dashv \Delta'$.
An expression $e$ has type $t$ in context $\Delta$ and changes $\Delta$ to $\Delta'$.
We can see that variables change their type on method invocation (\textsc{Obsidian}):
A method $m$ in class $t_0$
with arguments $e_i$ of type $t_i$,
returning $T$\!,
changes the type state of the arguments from $s_i$ to $s'_i$.
For \textsf{Prisma}\xspace, instead, a standard judgement $\Gamma \vdash e:T$
suffices for communication.
Variables do not change their type.
$\mathsf{awaitCl}(p)\{b\}$ has type $T$ in context $\Gamma$
if $p$ is a predicate of $Addr$ and $b$ is a pair of $Ether$ and $T$:
\begin{mathpar}\centering
  \inferrule[Prisma]{
    \Gamma \vdash p:Addr \to Bool \and
    \Gamma \vdash b:Ether \times T
  }{
    \Gamma \vdash \mathsf{awaitCl} (p) \{ ~b~ \}:T
  }
\end{mathpar}







\subparagraph{\textsf{Prisma}\xspace.}
As shown in Tab.~\ref{tab:related-work-style}, \textsf{Prisma}\xspace occupies an unexplored point in the design space: 
\emph{global} instead of local perspective on interacting parties, \emph{direct style (DS)} instead of FSM or MNF 
encoding of effects, and \emph{control flow} instead of extra protocol for governing interactions.   

\textsf{Prisma}\xspace takes a \textbf{global perspective} on interacting parties.
The parties execute the same program,
where pairs of send and receive actions that ``belong together''
are encapsulated into a single \textbf{direct-style} operation, which
is executed differently by sending and receiving parties.
Hence, dApps are modeled
as sequences and loops of send-receive-instructions 
shared by interacting parties.
Due to the global direct style perspective, it is syntactically impossible to define parties 
with mismatching send and receive pairs.
Hence, a standard System-F-like type system suffices.
The interaction protocol follows directly from 
the sequential \textbf{control flow} of interaction points in the program -- the 
compiler can automatically generate access and control guards with correctness guarantees. 
Semantically, \textsf{Prisma}\xspace features a by-default-sequential programming model, 
intentionally making the sequential execution of methods explicit, 
including interaction effects. 

The global direct-style model also leads to improved
design of dApps:
No programmatic state management on the contract
and no so-called \textit{callback hell} \cite{Edwards09} on the client. 
The direct style is also superior to Nomos' MNF style. 
The tierless model avoids boilerplate:
Client code can directly access public contract variables, 
unlike JavaScript code, which has to access them via a function call that  
requires either an await expression or a callback;%
\footnote{Obsidian and Nomos do not provide any client design, so we can only compare to Solidity/JavaScript.}
additionally, the developer has to implement getters for 
public variables with complex data types such as arrays.\footnote{For simple data types the getter is generated automatically.}
We provide some code measurements (lines of code and number of cross-tier control-flow calls) 
of our \textsf{Prisma}\xspace and Solidity/JS dApp case studies
in Appendix~\ref{appendix:loc-evaluation}.

Finally, using one language for both the contract and the clients
naturally enables static type safety 
of values that cross the contract--client boundary:
an honest, non-compromized client cannot provide inconsistent input,
 %
 e.g., 
with wrong number of parameters or falsely encoded types.\footnote{Recall that in dApps checking cross-tier type-safety is not a security feature but a design-time safety feature (due to the open-world assumption of the execution model of public ledgers).}
In a setting with different language stacks,
it is not possible to statically detect type mismatches in the client--contract interaction;
e.g.,, Solidity has a type \textit{bytes} for byte arrays, which 
does not exist in JavaScript (commonly used to implement clients of a Solidity contract).
Client developers need to encode byte arrays using 
hexadecimal string representations starting with ``0x'', otherwise
they cannot be interpreted by the contract.


\section{Case studies}
\label{appendix:case-studies}

This section describes the implemented case studies in detail.
Bartoletti and Pompianu~\cite{bartoletti2017empirical} identify five classes of smart contract
applications: Financial, Notary, Game,  Wallet, and Library.
Our case studies include at least one application per category
(Table~\ref{tab:categories-and-x-tier-passes}). 
In addition, we consider scalability solutions.

\emph{Financial.}
These apps include digital tokens, crowdfunding, escrowing,
advertisement, insurances and sometimes Ponzi schemes. %
 A study investigating all blocks mined until September 15th, 2018~\cite{oliva2020exploratory}, 
 found that 72.9\,\% of the high-activity contracts are token contracts compliant to ERC-20 or ERC-721, 
 which have an accumulated market capitalization of US\,\$\,12.7 billion.
We have implemented a fungible \textsf{Prisma}\xspace token of the ERC-20 standard.
Further, we implemented crowdfunding and escrowing case studies.
These case studies demonstrate how to send and receive coins with \textsf{Prisma}\xspace, which is 
the basic functionality of financial applications.
Other financial use cases can be implemented in \textsf{Prisma}\xspace with similar techniques.

\emph{Notary.}
These contracts use the blockchain to store data immutably and persistently, e.g., to certify their ownership.
We implemented a general-purpose notary contract enabling 
users to store arbitrary data, e.g., document hashes or images, together with a submission timestamp and the data owner.
This case study demonstrates that Notaries are  expressible with \textsf{Prisma}\xspace.

\emph{Games.}
We implemented TicTacToe (Section~\ref{sec:the-language}),
Rock-Paper-Scissors, Hangman and Chinese Checkers.
Hangman evolves through multiple phases and hence benefits
from the explicit control flow definition in \textsf{Prisma}\xspace more than the other game case studies.
The game Chinese Checkers is more complex than the others, in regard to the number of parties, the game logic and the number of rounds, and hence, represents larger applications. 
Rock-Paper-Scissors illustrates how randomness for dApps is securely generated.
Every Ethereum transaction, including the executions of contracts, 
is deterministic -- all participants can validate the generation of new blocks.
Hence, secure randomness is negotiated among parties:
in this case, by making use of timed commitments~\cite{DBLP:conf/sp/AndrychowiczDMM14},
i.e., all parties commit to a random seed share and open it 
after all commitments have been posted.
The contract uses the sum of all seed shares as randomness.
If one party aborts prior to opening its commitment, it is penalized.
In Rock-Paper-Scissors both parties commit to their choice -- their random share -- and open it afterwards.
Other games of chance, e.g., gambling contracts, use the same technique.


\emph{Wallet.}
A wallet contract manages digital assets, i.e., cryptocurrencies and tokens, and offers additional features 
such as shared ownership or daily transaction limits.
At August 30, 2019, 3.9 M of 17.9 M (21\,\%) deployed smart contracts have been different types of wallet contracts \cite{DBLP:journals/corr/abs-2001-06909}.
Multi-signature wallets are a special type of wallet that provides a transaction voting mechanism by only executing transactions, which are signed by a fixed fraction of the set of owners.
Wallets transfer money and call other contracts in their users stead depending on run-time input, %
demonstrating calls among contracts in \textsf{Prisma}\xspace.
Further, a multi-signature wallet uses built-in features of the Ethereum VM for signature validation, i.e., data encoding, hash calculation, and signature verification, showing that these
features are supported in \textsf{Prisma}\xspace.

\emph{Libraries.}
As the cost of deploying a contract increases with the amount of code in Ethereum,
developers try to avoid code repetitions.
Contract inheritance does not help: child contracts simply copy the attributes 
and functions from the parent.
Yet, one can outsource commonly used logic to \emph{library contracts} 
that are deployed once and called by other contracts.
For example, the TicTacToe dApp and the TicTacToe channel in our case studies 
share some logic, e.g., to check the win condition.
To demonstrate libraries in \textsf{Prisma}\xspace, we include a TicTacToe library 
to our case studies and another on-chain executed TicTacToe dApp 
which uses such library instead of deploying the logic itself.
Libraries use a call instruction similar to wallets, although 
the call target is typically known at deployment and can be hard-coded.

\emph{Scalability solutions.}
State channels~\cite{MBBKM19, DziembowskiFH18, DziembowskiEFHH19} 
are scalability solutions, which enable a fixed group of parties to move their dApp 
to a non-blockchain consensus protocol: the execution falls-back 
to the blockchain in case of disputes.
Similar to multi-signature wallets, state channels use built-in signature validation.
We implemented a state channel for TicTacToe\footnote{A general solution is a much larger engineering effort and subject of industrial projects~\cite{perun-network, state-channels}}
to demonstrate that \textsf{Prisma}\xspace supports state channels.

\section{Empirical Evaluation of Design Quality}
\label{appendix:loc-evaluation}

\begin{figure}
	\figurehead
	\centering
	\caption{Categories and Cross-tier calls.}
	\label{tab:categories-and-x-tier-passes}
	\input{paper/graphs/crossTierPassesTable}
\end{figure}

\begin{figure}
	\figurehead
	\centering
	\input{paper/graphs/locComparison}
	\caption{LOC in Solidity/JavaScript and \textsf{Prisma}\xspace.}
	\label{fig:loc-comparison}
\end{figure}

In Section~\ref{sec:background}, we argued 
that with \textsf{Prisma}\xspace, 
(a) we provide communication safety with a standard system-F-like type-system,
(b) the program flow can be defined explicitly and is enforced automatically,
(c) dApp developers need to master a single technology that covers both tiers, 
(d) cross-tier type-safety can be checked at compile-time, 
and (e) the code is simpler and less verbose due to reduced boilerplate code for communication and less control flow jumps.
The claims (a), (c), and (d) are a direct consequence of \textsf{Prisma}\xspace's design and do not require further evidence.
Claim (c) has been formally proven in Section~\ref{sec:formalization}.
It remains to investigate claim (e), i.e., in which extent \textsf{Prisma}\xspace reduces the amount of code and error-prone control-flow jumps.


To this end, 
we implemented all case studies with equivalent functionality in \textsf{Prisma}\xspace and in Solidity/JavaScript.
The JavaScript client logic is in direct style using async/await -- 
the Solidity contract needs to be implemented as a finite-state-machine.
We keep the client logic of our case studies (in both, the \textsf{Prisma}\xspace and the Solidity implementation) as basic as possible, not to compare the client logic in Scala and in JavaScript but rather focus on the dApp semantics.
A complex client logic would shadow the interaction with the contract logic 
-- limited in size due to the gas semantics.


We start with comparing LOCs in the case studies (Figure~\ref{fig:loc-comparison}).
The results in Figure~\ref{fig:loc-comparison} show that case studies 
written in \textsf{Prisma}\xspace require only 55\,--\,89\,\% LOC compared to 
those implemented in Solidity/JavaScript.
One exception is the standalone library, which has no client code and hence does not directly 
profit from the tierless design.

Second, we consider occurrences of explicit cross-tier control-flow calls in the Solidity/JavaScript dApps (cf. Table~\ref{tab:categories-and-x-tier-passes}),
which complicate control flow,
compared to \textsf{Prisma}\xspace, where cross-tier access is seamless.
In the client implementations, 6\,--\,18\,\% of all lines trigger a contract interaction passing the control flow to the contract and waiting for the control flow to return.
From the contract code in finite-state-machine style, it is not directly apparent at which position the program flow continues, once passed back from clients to contract, i.e., which function is called by the clients next.
Direct-style code, on the other hand, ensures that the control flow of the contract always continues in the line that passed the control flow to the client by invoking an \lstinline!awaitCl! expression.





