Prisma : A Tierless Language for Enforcing Contract-client Protocols in Decentralized Applications
Authors: 
David Richter, David Kretzler, Pascal Weisenburger, Guido Salvaneschi, Sebastian Faust, 
Mira MeziniAuthors Info & Claims
Article No.: 17, Pages 1 - 41
Abstract
Decentralized applications (dApps) consist of smart contracts that run on blockchains and clients that model collaborating parties. dApps are used to model financial and legal business functionality. Today, contracts and clients are written as separate programs—in different programming languages—communicating via send and receive operations. This makes distributed program flow awkward to express and reason about, increasing the potential for mismatches in the client-contract interface, which can be exploited by malicious clients, potentially leading to huge financial losses.
In this article, we present Prisma, a language for tierless decentralized applications, where the contract and its clients are defined in one unit and pairs of send and receive actions that “belong together” are encapsulated into a single direct-style operation, which is executed differently by sending and receiving parties. This enables expressing distributed program flow via standard control flow and renders mismatching communication impossible. We prove formally that our compiler preserves program behavior in presence of an attacker controlling the client code. We systematically compare Prisma with mainstream and advanced programming models for dApps and provide empirical evidence for its expressiveness and performance.
1 Introduction
dApps enable multiple parties sharing state to jointly execute functionality according to a predefined agreement. This predefined agreement is called a smart contract and regulates the interaction between the dApp’s clients. Such client–contract interactions can be logically described by state machines [63, 64, 85, 89] 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, and public offerings,1 and the same feature makes them an attractive target for attackers. The attack surface is wide, since 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 [49]. In recent years, there have been several large attacks exploiting flawed program flow control in smart contracts. Most famously, attackers managed to steal around 50M USD [9, 49] from a decentralized autonomous organization, the DAO. In two attacks on the Parity multi-signature wallet, attackers stole cryptocurrencies worth 30M USD [28] and froze 150M USD [73].
Programming dApps. In this article, we explore a programming model that ensures the correctness and security of the client–contract interaction of dApps by-design. Deviations from the intended interaction protocols due to implementation errors and/or malicious attacks are a critical threat (besides other issues such as arithmetic or buffer overflows, etc.) as demonstrated, e.g., by the DAO attack [9, 49] mentioned above.
dApps are multi-party applications. For such applications, there are two options for the programming model: a local and a global model. In a local model, parties are defined each in a separate local program, and their interactions are encoded via effectful send and receive instructions. Approaches that follow this model stem from process calculi [56] and include actor systems [19] and approaches using session types [42] and linear logic [90]. In contrast, in a global model, there is a single program shared by both parties and interactions are encoded via combined send-and-receive operations with no effects visible to the outside world. This model is represented by tierless [32, 38, 51, 75, 76, 86, 87, 91] and choreographic [53, 57, 67] languages. The local model requires an explicitly specified protocol to ensure that every send effect has a corresponding receive operation in an interacting—separately defined—process. 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 by the other party. Due to encapsulating communication effects, there is no non-local information to track—the program’s control flow defines the correct interaction and a simple type system is sufficient.
Current approaches to dApp programming—industrial or research ones—follow a local model, Contract and client are implemented in separate programs, thus safety relies 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 [66] for the contract and JavaScript for clients. Solidity relies on developers following best practices recommending to express the protocol as runtime assertions integrated into the contract code [13]. Failing to correctly introduce assertions may give parties illegal access to monetary values to the detriment of others [61, 68].
The currently dominant encoding style of the protocol as finite state machine (FSM) uses one contract-side function per FSM transition [34, 35, 36, 66, 81, 82]. While FSMs model a useful class of programs that can be efficiently verified, writing programs in such style directly has several shortcomings. First, an FSM corresponds to a control-flow graph of basic blocks, which is low-level and more suited as an internal compiler representation than as a front-end language for humans. Second, with the FSM style, the contract is a passive entity whose execution is driven by clients. This design puts the burden of enforcing the protocol on the programmers of the contract, as they have to explicitly consider in what state which messages are valid and reject all invalid messages from the clients. Otherwise, malicious clients would be able to force the contract to deviate from its intended behavior by sending messages that are invalid in the current state. Third, ensuring protocol compliance statically to guarantee safety requires advanced types, as the type of the next action depends on the current state.
In research, some smart contract languages [26, 34, 35, 36, 40, 69, 81, 82] have been proposed to overcome the FSM-style shortcomings. They 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, and non-compliant processes are rejected by the type-checker.
The global model has not been explored for dApp programming—which 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 Prisma —the first language that features a 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 as well.
Prisma . Prisma enables interleaving contract and client logic within the same program and adopts a 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 [25, 80]. Prisma leaves it to the compiler to map down high-level declarative DS to low-level FSM style. It avoids the need for advanced typing discipline and allows the contract to actively ask clients for input, promoting 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, Prisma relieves the developer from the responsibility of correctly managing distributed, asynchronous program flows and the heterogeneous technology stack. Instead, the burden is on the compiler, which distributes the program flow by means of selective continuation-passing-style (CPS) translation and defunctionalization, as well as inserts guards against malicious client interactions.
For this, 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, otherwise, to implement asynchronous communication. Given that CPS translations reify control flow, without proper guarding, malicious clients could force the contract to deviate from the intended flow by passing a spoofed value to the contract. Thus, it is imperative to prove that our distributed CPS translation ensures control-flow integrity of the contract, which we do on top of a formal definition of the compilation steps. The formally proven secure Prisma compiler eliminates the risk of programmers implementing unsafe interactions that can potentially be exploited.
Contributions. We make the following contributions:
(1)
We introduce Prisma, a global language for tierless dApps with direct-style client–contract interactions and explicit access control, implemented as an embedded DSL in Scala. Crucially, Prisma automatically enforces the correct program flow (Section 2).
(2)
A core calculus, MiniPrisma, which formalizes both Prisma and its compiler, as well as a proof that our compiler guarantees the preservation of control flow in presence of an attacker that controls the client code (Section 3).
(3)
Case studies that show Prisma can be used to implement common applications without prohibitive performance overhead (Section 5).
(4)
A comparison of Prisma with a session type and a type state smart contract programming language and the mainstream Solidity/JavaScript programming model (Section 6).
An extended abstract [78] and a software artifact [79] of this work was published at ECOOP’22; the implementation and case studies are also available at https://github.com/stg-tud/prisma
2 Prisma in A Nutshell
We present Prisma 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.
Example. TicTacToe is a two-player game over a \(3\times 3\) board. 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 Move(x,y) used by a player to occupy field (x,y). A Move(x,y) is valid if it is the sender’s turn and (x,y) is empty. Before the game, players deposit their stakes, and after the game, the stakes are paid to the winner.
Figure 1 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 Fund\((c)\). Next, parties execute 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 Payout\(()\).2 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.
Fig. 1.
Tierless dApps. Prisma is implemented as a DSL embedded into Scala, and Prisma programs are also valid Scala programs.3 Prisma interleaves contract and client logic within the same program. Annotations @co and @cl explicitly place declarations on the contract and on the client, respectively (cf. Table 1). A declaration marked as both @co and @cl has two copies. For security, code placed in one location cannot access definitions from the other—an attempt to do so yields a compile-time error. Developers can overrule this constraint to enable clients to read contract variables or call contract functions by combining @co with @cross. Combining @cl with @cross is not allowed—information can only flow from client to contract as part of a client–contract interaction protocol.
Table 1.
| Annotations | Description |
|---|---|
| @co | on contract |
| @cl | on clients |
| @co @cl | independent copies |
| on clients and contract | |
| @co @cross | on contract, but also |
| accessible by client | |
| @cl @cross | (illegal combination) |
There are three kinds of classes. Located classes are placed in one location (annotated with either @co or @cl); they cannot contain located members (annotated with either @co or @cl) and their instances cannot cross the client–contract boundary, e.g., be passed to or returned from @cross functions. Portable classes are annotated with both @co and @cl. Their instances can be passed to and returned from @cross functions; they must not contain mutable fields. Split classes have no location annotation; their instances live partly in both locations; they cannot be passed to or returned from @cross functions and their members must be located.
Prisma code is grouped into modules. While client declarations can use and be used from standard (non-Prisma) Scala code, contract declarations are not accessible from Scala and can only reference contract code from other Prisma modules (because contract/client code lives in different VMs).
For illustration, consider the TicTacToe dApp (Figure 2). The TicTacToeModule (Line 1)—modules are called object in Scala—contains a portable class UU (Line 3) and a split class TicTacToe (Line 5). Variables moves, winner, board (Lines 10, 11, 13) are placed on the contract and can be read by clients (@co @cross). The updateBoard function (Line 17) is placed on the client and updates client state (e.g., client’s UI). The move function (Line 15) is placed on the contract and changes the game state (move). move is not annotated with @cross, because @cross is intended for functions that do not change contract state and can be executed out-of-order without tampering with the client–contract interaction protocol. While Scala only has signed integers and signed longs literals, these are uncommon in Ethereum. Therefore, Prisma provides portable unsigned and signed integers for power-of-two bitsizes between \(2^3\) to \(2^8\), with common arithmetic operations, e.g., ''0''.u8 is an unsigned 8-bit integer of value 0 (Line 10).
Fig. 2.
Encoding client–contract protocols. In Prisma, a client-contract protocol is encoded as a split class containing dedicated awaitCl expressions for actively requesting and awaiting messages from specific clients and standard control-flow constructs. Hence, creating a new contract instance corresponds to creating a new instance of a protocol; once created, the contract instance actively triggers interactions with clients. The awaitCl expressions have the following syntax:
def awaitCl[T](who: Addr => Bool)(body: => (Ether, T)): T
They take two arguments. The first (who) is a predicate used by clients to decide whether it is their turn and by the contract to decide whether to accept a message from a client. This is unlike Solidity, where a function may be called by any party by default. By forcing developers to explicitly define access control, Prisma reduces the risk of human failure. The second argument (body) is the expression to be executed by the client. The client returns a pair of values to the contract: the amount of Ether and the message. The former can be accessed by the contract via the built-in expression value, the latter is returned by awaitCl. Besides receiving funds via awaitCl, a contract can also check its current balance (balance()) and transfer funds to an account (account.transfer(amount))).
Prisma ’s programming model is specifically designed to accommodate blockchain use cases. In contrast to other tierless models like client-server, we emphasize inversion of control such that the code is written as if the contract was the active driver of the protocol, while clients are passive and only react to requests by the contract. This enables to enforce the protocol on the contract side. For this reason, for example, we support the awaitCl construct on the active contract side, whereas there is no corresponding construct on the passive client side.
For illustration, consider the definition of init on the right-hand side of Figure 2, Line 28. It defines the protocol of TicTacToe as follows: From the beginning of init, the flow reaches awaitCl in Line 30 where the contract waits for clients to provide funding (by calling fund). Next, the contract continues until awaitCl in Line 33 and clients execute move (Line 21) until the game ends with a winner (winner != 0) or a draw (moves >= 9). At this point—awaitCl in Line 37—any party can request a payout and the contract executes to the end. The example illustrates how direct-style awaitCl expressions and the tierless model enable encoding multiparty protocols as standard control flow, with protocol phases corresponding to basic blocks between awaitCl expressions.
Compiling Prisma to Solidity. Abstractly, Prisma’s compiler takes a Prisma dApp program and splits it into two separate programs: a Scala client program and a Solidity contract program (Figure 3(a)). In more detail, the compiler (1) places all definitions according to their annotations and (2) splits contract methods that contain awaitCl expressions into a method that contains the code up to the awaitCl and a method that contains the continuation after the awaitCl (taking the result of the awaitCl as an argument). Once deployed, a contract is public and can be messaged by arbitrary clients—not exclusively the ones generated by Prisma —hence, we cannot assume that clients will actually execute the body passed to them by an awaitCl expression. To cope with malicious clients trying to tamper with the control flow of the contract, the compiler hardens contract code by generating code to enforce control flow integrity: storing the current phase before giving control to the client and rejecting methods invoked by wrong clients or in the wrong phase.
Fig. 3.
For illustration, the code generated from Figure 2 is schematically shown in Figures 3(b) and 3(c). The methods updateBoard, fund, move, and payout are annotated @cl and thus compiled into the client program (Figure 3(b)). The variables moves, winner, and board, and the method performMove, are annotated @co and thus compiled into the contract program (Figure 3(c)). Further, three new methods are generated on both the client and the contract—one for each awaitCl expression in init—corresponding to phases in the logical protocol (Figure 1). The Funding method of the client (Line 16) is generated from the body of the first awaitCl. Similarly, the Move method (Line 18) is generated from the second awaitCl and the Payout method (Line 20) from the third awaitCl. In the example, the generated methods are given meaningful names by capitalizing the single method called in the body of the awaitCl expressions from which they were generated. In the actual implementation, generated methods are simply enumerated. The code up to the first awaitCl (Line 30, Figure 2) is placed in the constructor of the generated contract, which ends by setting the active phase to Funding. The code between the first and the second awaitCl either loops back to the first awaitCl or continues to the second one (Line 33). The code is placed in the Fund method that requires the phase to be Funding and may change it to Exec if the loop condition fails. Similarly, the method Move is generated to contain the loop between the second and the third awaitCl (Line 37); and the method Payout contains the code from the third awaitCl to the end of init. Only the second awaitCl contains a (non-trivial) access control predicate, which results in an additional assertion in the body of Move (Line 46, Figure 3). Observe that the return types of the generated client methods are the argument types of the corresponding contract methods.
Compilation Techniques. While CPS is a key step in our translation pipeline, the example shows the final defunctionalized, trampolined code. The final output does not contain explicit continuations (i.e., a function that takes another function as an argument and calls that as its continuation). Instead, after defunctionalizing and trampolinizing the CPS translation, only one top-level function (Fund, Move, Payout) is callable at each phase, which is ensured by the require statement at the beginning of each function, and each function sets the next phase at the end. These functions play the role of the continuations.
Let us look at the correspondence between the original Prisma code (Figure 2) and the generated Solidity code (Figure 3(c)) from a higher-level perspective: To verify that the Prisma code matches the generated Solidity code, we proceed as follows:
First, we verify that the control flow of Figure 2 is accurately described by the automaton diagram in Figure 1. In particular, we observe that there are two loops in the automaton and there are also two while loops in the Prisma code. Further, there are three awaitCl expressions in the code, and there are three states in the automaton (plus a final state).
Second, we verify that the automaton in Figure 2 corresponds to the program flow of the Solidity code in Figure 3(c). In particular, we observe that there are four states in the automaton and there are four states in the Solidity code. Three of those have an associated function (T0 is Fund, T1 is Move, T2 is Payout), which are the only public functions that can be invoked in that state, thanks to the require statements. In the final state T3, no public function can be invoked. Furthermore, we can see that the automaton has two loops. It is possible to go from T0 either to T1 or stay in T0. This is represented in the Solidity code, by checking for the loop condition at the end of the function associated to T0, and then either changing the phase to T1, or doing nothing, which means staying in T0. Similarly, the loop in state T1 is encoded with an if at the end of the function to conditionally move to the next phase.
These two steps should illustrate how the control flow of the Prisma program—which is abstractly visualized by the automaton—is implemented and enforced by the generated Solidity program.
3 Compilation and Its Correctness
We informally introduce Prisma’s compilation process and our notion of correctness before formally specifying and proving the compiler correct.
3.1 High-level Overview of Prisma’s Secure Compilation
To implement the contract-client interaction, we CPS-translate Prisma code and execute continuations alternately between contract and client. A standard CPS translation is, however, not sufficient, because the control flow is distributed and we need to send function calls (i.e., the current continuation) over the network—or, more specifically, send the name and the arguments of the next function to execute. For this, we defunctionalize [77] the code to turn functions calls (which represent continuations) into data. This compilation process performs an inversion of control between the contract and the client. With Prisma’s contract–client communication in direct style, we can write dApps as if the contract was in control of the execution; Prisma allows the contract to request messages from clients and to process only responses that it requested.
After the compilation process, clients are in control of the execution because, in blockchains, contracts purely respond to messages from clients. As a result, dApps may become the target of malicious attacks. In our security model, we trust the contract to execute the code that we generate for it, whereas, we consider the client code untrusted, i.e., the client side can run arbitrary code. Crucially, it could pass unintended continuations to the contract to force the execution to continue in an arbitrary state. For example, in the source code of the TicTacToe game (Section 2), one needs to go through the game loop after funding and before payout. Yet, the compiled code is separated and distributed into small chunks. Parties execute a chunk and then wait for other parties to decide on a move that influences how to proceed with the execution. For this reason, the client could send a message at any time telling the contract to go into the payout phase. We need to guard the contract against such attempts to make it deviate from the protocol. Conceptually, if the client was able to force the execution to continue in an arbitrary state, then the control flow in the Prisma source would be violated. Execution would “jump” from one client expression to another one, skipping the code in between, which is not possible with the semantics of the source language.
Prisma’s compiler avoids such attacks and preserves control flow by inserting guards on the contract side. Guards are in places where the basic blocks of the program have been separated and distributed onto different hosts by CPS translation—to reject any improper continuations from clients. Guarding ensures the control flow integrity [18] of the contract in the presence of malicious clients by excluding any behavior of the compilation target that cannot be observed from the source. Informally, this is our notion of secure compilation, which we rigorously define and prove for Prisma’s compiler in this section. The compilation process is key in hiding the complexity of enforcing distributed control flow from the developer—hence, a formal proof of its correctness is critical.
To formalize the compiler, we specify a source and a target language. Figure 4 shows a schema of our compilation and the proof. The compiler (Figure 4, top) is a function that maps terms in the source language (\(Term_s\)) into terms in the target language (\(Term_t\)). A correct compiler preserves some properties of the code—depending on the notion of correctness. For example, typeability-preserving and semantics-preserving compilers have been extensively studied [71]. Because types are not the focus of this article, we omitted them from the figure. In the middle part of Figure 4, we show the evaluation of source and target to traces (\(eval_s\) and \(eval_t\), respectively)—and traditional compiler correctness as the equivalence between traces generated from the sources (\(Trace_s\)) and from the target (\(Trace_t\)). But compiler correctness4 in this traditional sense is not sufficient in the presence of malicious attackers that can tamper with parts of the code. Instead, we need to prove that Prisma is a secure abstraction, i.e., if security problems can arise on the target, then they must be visible in the Prisma source code, too, so developers do not need to look at target code to reason about potentially misbehaving clients. To this end, we define a hypothetical attacker model on the source code as the ability to only replace the body of a Prisma client expression and show that, with the contract part hardened with guards, the target attacker does not gain additional power over the hypothetical source attacker. Specifically, we define malicious semantics \(eval_{t,b}\) and \(eval_{s,b}\) for the target and the source language, respectively, and show that \(eval_{t,b} (compile~e) = compile (eval_{s,b}~e)\) (security property in Figure 4).
Fig. 4.
In the remainder of this section:
•
We present the core calculus (Section 3.2) \(\mathsf {MiniPrisma}\,_*\)—a hybrid language that includes elements of both the source (\(\mathsf {MiniPrisma}\,_s\)) and the compilation target (\(\mathsf {MiniPrisma}\,_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.
•
We model the compiler (Section 3.3) as a sequence of steps that transform \(\mathsf {MiniPrisma}\,_*\) programs via several intermediate representations.
•
We define \(\mathsf {MiniPrisma}\,_*\) semantics as a reduction relation over configurations consisting of traces of evaluation events and expressions being evaluated (Section 3.4). 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.
•
We prove secure compilation by showing that the observable behavior of the programs before and after compilation is equivalent (Section 3.5). 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.
3.2 Syntax
The syntax of \(\mathsf {MiniPrisma}\,_*\) (Figure 5) has three kinds of identifiers \(id\), \({i}\), \({j}\), from unspecified sets of distinct names. Pure identifiers \(id\) are for function arguments and let bindings; mutable variables \({i}\) are for heap variable assignment and access. In the target program, mutable variables \({j}\) (\({\mathsf {who}}, {\mathsf {state}}, {\mathsf {clfn}}, {\mathsf {cofn}}\)) generated by the compiler can also appear. We call compiler-generated identifiers synthetic. Normal identifiers are separated from synthetic ones to distinguish compiler generated and developer code. Definitions \({d}\) and definitions for synthetic identifiers \({b}\) are semicolon-separated lists of declarations that assign values to variables and annotate either the contract or the client location. Each program \(P\) consists of definitions \({d}\) and synthetic definitions \({b}\) followed by the main contract expression \({m}\). Program \(P\) corresponds to a single Prisma split class, \({d}\) and \({b}\) to methods and generated methods, and \({m}\) to a constructor containing the initialization of its class members (such as the body of init, Figure 2).
Fig. 5.
Constants \(c\) are unsigned 256 bit integer literals and built-in operators. \(\mathsf {MiniPrisma}\,_*\) 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 \({e}\) are constants, expression pairs, lambdas, variables, variable accesses/assignments, bindings, and function applications.
Main expressions \({m}\) may further contain remote client expressions, embedding client code into contract code and waiting for its result. The source client expression \({\mathsf {awaitCl}}_s(e,~()\rightarrow e)\) can be answered by any client whose address fulfills the predicate specified as first argument. \(\mathsf {awaitCl}_s\) corresponds to direct-style remote access via awaitCl in Prisma . We use the syntax form \({\mathsf {awaitCl}}_t(c,~()\rightarrow e)\) to model the execution of code \(e\) on the specified client \(c\). \(\mathsf {awaitCl}_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 \(\mathsf {MiniPrisma}\,_*\) to the source and target languages, \(\mathsf {MiniPrisma}\,_s\) and \(\mathsf {MiniPrisma}\,_t\). \(\mathsf {MiniPrisma}\,_s\) has all expressions of \(\mathsf {MiniPrisma}\,_*\), except those that contain \(\,{\mathsf {\gg \hspace{-2.0pt}=}}\,\) (bind), \({\mathsf {trmp}}\) (trampoline), \(\mathsf {Done}\), \(\mathsf {More}\), \(\mathsf {awaitCl}_t\), or synthetic identifiers \(j\). \(\mathsf {MiniPrisma}\,_t\) has all expressions of \(\mathsf {MiniPrisma}\,_*\) except those that contain \(\mathsf {awaitCl}_s, \mathsf {awaitCl}_t, \,{\mathsf {\gg \hspace{-2.0pt}=}}\,\).
\(\,{\mathsf {\gg \hspace{-2.0pt}=}}\,\) and \(\mathsf {awaitCl}_t\) may not appear neither in source nor target programs; the former is used only as an intermediate construction for the compiler, the latter only during evaluation to track the current location.
Syntactic sugar. In Figure 6, 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 \(()\), \({\mathsf {assert}}(x)\) is a let binding matching true; we use monadic syntax for let bindings of effectful expressions; \({\mathsf {if\,let}}\,x = {m}{\,\mathsf {then}}\,{e}{\,\mathsf {else}}\,{e}\) is the application of the built-in \({\mathsf {try}}\) function.
Fig. 6.
Events and configurations. In Figure 7, we define left-to-right evaluation contexts \(E\) [47]; and compilation frames \(F\) [74], such that every expression decomposes into a frame-redex pair \(F~{e}\) or is an atom \(a\). Events \({p}\) and \({q}\) are lists that capture the observable side-effects of evaluating expressions. They are either (a) state changes \(\mathsf {wr}(c,{i},v)\) and \(\mathsf {wr}(c,{j},v)\), from the initial definitions or variable assignment, where \({i}\) and \({j}\) are the variables being assigned, \(c\) the location, and \(v\) the assigned value, or (b) client-to-contract communication \(\mathsf {msg}(c,v)\), where \(c\) is the address of the client and \(v\) the sent value. Configurations \(C = {p};{q};c {m}\), represent a particular execution state, where \({p}\) (and \({q}\)) are traces of normal (and synthetic) events produced by the evaluation, \(c\) is the evaluating location, and \({m}\) is the expression under evaluation.
Fig. 7.
Initialization. Initialization in Figure 8 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 \({d};{b};{m}\) to a configuration \({p};{q};0;{m}\) leaves the expression \({m}\) untouched and generates a list of events —one write event for each normal and synthetic definition. Location 0 represents the contract.
Fig. 8.
3.3 Compilation
The compiler eliminates language features not supported by the compilation target one-by-one, lowering the abstraction level from (1) direct style communication (DS)—which needs language support for !-notation [5]—through the intermediate representations of (2) monadic normal form (MNF)—which needs support for do-notation [2]—and (3) continuation-passing style (CPS)—which needs higher-order functions—to (4) explicitly encoding 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 \({\mathit {mnf}}\) and \({\mathit {assoc}}\) transform DS remote communication \({\mathsf {awaitCl}_s}\) \((e, () \rightarrow {e})\) to variable bindings (\(id := {e}\)), and nested let bindings are flattened such that a program is prefixed by a sequence of let expressions. Second, step \({\mathit {guard}}\) generates access control guards around client expressions to enforce correct execution even when clients behave maliciously. Third, step \({\mathit {cps}}\) transforms previously generated let bindings for remote communication (\(x \leftarrow {e}_1;\;{m}_2\)) to monadic bindings \({e}_1 \,{\mathsf {\gg \hspace{-2.0pt}=}}\,x \rightarrow {m}_2\). Fourth, step \({\mathit {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 (\(\,{\mathsf {\gg \hspace{-2.0pt}=}}\,\)) by wrapping the program expression into a call to a trampoline \({\mathsf {trmp}}(...)\) and transforming the bind operator (\(... \,{\mathsf {\gg \hspace{-2.0pt}=}}\,x \rightarrow ...\)) 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.
MNF transformation (Figure 9). The \({\mathit {mnf^\prime }}\) function wraps the main expression \({m}\) into a call to the trampoline with the pair \((\text{Done}, {m})\)—signaling the final result—as argument. Then, \({\mathit {mnf}}\) transforms expressions recursively, binding sub-expressions to variables, resulting in a program prefixed by a sequence of let bindings. As recursive calls to \({\mathit {mnf}}\) may return chains of let bindings, we apply \({\mathit {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, (\(...~(...~{m}_0;~{m}_1);~{m}_2 = ...~{m}_0;~(...~{m}_0;~{m}_2)\)), creating a single MNF expression (i.e., \({\mathit {assoc}}\) is composition for MNF terms).
Fig. 9.
Guarding (Figure 10). We insert access control guards for remote communication expressions \(\leftarrow _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.
Fig. 10.
CPS transformation (Figure 11). The \({\mathit {cps}}\) transformation turns the chains of let bindings produced by \({\mathit {mnf}}\) into CPS. The chain contains three cases of syntax forms: (1) monadic binding (\(x \leftarrow ...;\;{m}_1\)), (2) let binding (\(x = {e}_0;\;{m}_1\)), or (3) final expression. For (1), \({\mathit {cps}}\) replaces the monadic binding with an explicit call to the bind operator (\(... \,{\mathsf {\gg \hspace{-2.0pt}=}}\,(x \rightarrow cps({m}_1))\)). For (2) and (3), \({\mathit {cps}}\) recurses into the tail of the chain. This resembles do-notation desugaring (e.g., in Haskell).
Fig. 11.
Defunctionalization (Figure 12). The \({\mathit {defun}}\) function transforms the chains of let bindings and bind operators produced by \({\mathit {cps}}\), which contains three cases of syntax forms: (1) a bind operator (\({e}_1 \,{\mathsf {\gg \hspace{-2.0pt}=}}\,{e}_2\)) or (2) a let binding (\(x = {e}_1;\;{e}_2\)) or (3) the final expression. For (1), \({e}_1\) and \({e}_2\) are replaced by data structures that contain values for the free variables in \({e}_1\) and \({e}_2\) and are tagged with a fresh ID. The body of the expression is lifted to top-level synthetic definitions. For this, \({\mathit {defun}}\) modifies the synthetic definitions \(b\) by extracting the body \({e}_{1,alt}\) of the synthetic \({\mathsf {clfn}}\) definition and the body \({e}_{2,alt}\) of \({\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), \({\mathit {defun}}\) recurses into the expressions.
Fig. 12.
After defunctionalization, lambdas \(x \rightarrow {e}_0\) are lifted and assigned a top-level identifier \(id_0\) and lambda applications, \(id_0({e}_1)\), are replaced with calls to a synthesized interpreter function \({\textsf {fn}}(id_0, {e}_1)\). The latter branches on the identifier and executes the code that was lifted out of the original function.
Compiling. The \(\mathit {comp}\) function composes the compiler steps (not including \(\mathit {mnf}\)). We also define the \(\mathit {comp^{\prime }}\) function, which jumps over the wrapping \(trmp\) expression and initializes the defunctionalization with an environment that contains the two functions \({\mathsf {cofn}}\) and \({\mathsf {clfn}}\), which assert false.
\begin{equation*} \begin{array}{ll} \mathit {comp} &~=~ {\mathit {defun}}~\circ ~ {\mathit {cps}}~\circ ~ {\mathit {guard}}\\ \mathit {comp}^{\prime } &~=~ {\mathit {defun^\prime }}~\circ ~ {\mathit {cps^\prime }}~\circ ~ {\mathit {guard^\prime }}\end{array} \end{equation*}
3.4 Semantics
We model the semantics as a reduction relation over configurations \({p};{q};c;{m}\rightarrow {p}^{\prime };{q}^{\prime };c^{\prime };{m}^{\prime }\). Location \(c=0\) denotes contract execution, otherwise execution of client of address \(c\). We distinguish good (\(\color{blue}{\rightarrow _g}\)) and bad (\(\color{red}{\rightarrow _b}\)) evaluations (Figures 13 and 14); shared rules are in black, without subscript (\(\rightarrow\)).
Fig. 13.
Fig. 14.
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 (Rgs) reduce to a client expression with a fixed client that fulfills the given predicate. We require that predicates evaluate purely. Hence, \({p}\) and \({q}\) do not change in the evaluation. However, bad evaluation of client expressions in the source language (Rbs) ignores the predicate, choosing an arbitrary client. Similarly, bad evaluation also chooses an arbitrary client for the evaluation of a trampoline in the target (Rtm), which does not specify a predicate. The trampoline ends when it reaches \(\mathsf {Done}\) (Rtd). Further, after choosing a client to evaluate, the good evaluation (Rg) continues to reduce the client expression to a value, while the bad evaluation (Rb) replaces the expression \({e}\) with a (manipulated) arbitrary value \(v^{\prime }\). Both evaluations (Rg, Rb) emit the message event \(\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.
Common Evaluation (Figure 14). Expressions are reduced under the evaluation context \(E\) on the current location (Re), assignment to variables is recorded in the trace (Rset\(^\circ\)), accessing a variable is answered by the most recent assignment to it from the trace in the current location (Rget\(^\circ\)). For synthetic variables, we use the synthetic store (Rget\(^\dagger\), Rset\(^\dagger\)). Binary operators are defined as unsigned 256 bit integer arithmetic; we only show the rule for addition (Rop). Further, we give rules for conditionals (Rt, Rf), let binding (Rlet), and function application (Rlam) using pattern matching.
Pattern matching (Figure 15). Matching \([x{⟾ }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 \({e}\), written \([id{\mapsto }v]~{e}\) (capture-avoiding substitution). Substitutions \(\sigma\) compose right-to-left \((\sigma \sigma ^{\prime }) x = \sigma (\sigma ^{\prime } x)\).
Fig. 15.
3.5 Secure Compilation
We prove that the observable behavior 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 \(\color{red}{\rightarrow _b^*}\).
Modelling Observable Behavior. The only source of observable nondeterminism in the bad semantics is the evaluation of \(\mathsf {awaitCl}_s\) and \(\mathsf {awaitCl}_t\). As clients’ decisions on message sending are influenced by the state of contract variables, tracking incoming client messages and state changes in the trace suffices to capture the observable program behavior. If the observable behavior is the same for the source and the compiled programs, then 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 \({p};{q};{m}\Downarrow\) be the trace set of the configuration \({p};{q};0;{m}\), e.g., the set of tuples of the final event sequence \({p}^{\prime }\) and value \(v\) of all reduction chains that start in \({p};{q};0;{m}\) and end in \({p}^{\prime };0;{q}^{\prime };v\). Our trace set definition does not include synthetic events \({q}^{\prime }\) 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~\color{red}{\Downarrow}\), be the union of the trace sets for each element:
\begin{equation*} {p};{q};{m}~\color{red}{\Downarrow} ~~=~ \lbrace ~ ({p}^{\prime },v) ~|~ ({p};{q};0;{m})~\color{red}{\rightarrow _b^*}~({p}^{\prime };{q}^{\prime };0;v) ~\rbrace \end{equation*}
\begin{equation*} T~\color{red}{\Downarrow} ~=~ \bigcup _{{p};{q};{m}\in T} ~ {p};{q};{m}~\color{red}{\Downarrow} . \end{equation*}
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:
\begin{equation*} (T~\color{red}{\approx} ~S)~~~\Leftrightarrow ~~~(T~\color{red}{\Downarrow} ~=~ S~\color{red}{\Downarrow}). \end{equation*}
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 \(\color{red}{\rightarrow _b^*}\) and the original program backward \(\color{red}{\leftarrow _b^*}\) until configurations converge.
Secure Compilation. Theorem 1 states our correctness property, which says that observable traces generated by the malicious evaluation of programs are preserved (\(\color{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.
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.\, \lbrace ~ init_A(comp^{\prime }(mnf^{\prime }((P)))) ~\rbrace ~\color{red}{\approx} ~\lbrace ~ init_A(P) ~\rbrace\).
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⟾ v]\). We formulate the necessary lemmas and sketch the proofs—the detailed proof is in Appendix C.
\(\lbrace \, {p};{q}; [x{⟾ }v]\,assoc({m}) \,\rbrace \approx \lbrace \, {p};{q}; [x{⟾ }v]\,{m}\,\rbrace\)
\(\lbrace \, {p};{q}; [x{⟾ }v]\,mnf({m}) \,\rbrace \approx \lbrace \, {p};{q}; [x{⟾ }v]\,{m}\,\rbrace\)
\(\lbrace \, init_C(mnf^{\prime }({d};{b}; {m})) \,\rbrace \approx \lbrace \, init_C({d};{b}; {m}) \,\rbrace\)
\(\lbrace \, [x{⟾ }v]\,init_A(comp({d};{b}; {\mathsf {trmp}}({m}))) \,\rbrace \approx \lbrace \, init_A({d};{b}; {\mathsf {trmp}}([x{⟾ }v]\,{m})) \,\rbrace\)
\(\lbrace \, [x{⟾ }v]\,init_A(comp^{\prime }({d};{b}; {\mathsf {trmp}}({m}))) \,\rbrace \approx \lbrace \, init_A({d};{b}; {\mathsf {trmp}}([x{⟾ }v]\,{m})) \,\rbrace\)
Proof sketch. Lemmas 1–5 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 (\({\rightarrow }^*\)) and the original program (\({\leftarrow }^*\)) 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 = {d};{b}; \mathsf {awaitCl}({e}_0, () \rightarrow {e}_1)\). The compiler transforms the remote communication \(\mathsf {awaitCl}_s\) into the use of a guard and a trampoline. The compiled program steps to the use of \(\mathsf {awaitCl}_t\), the source program to \(\mathsf {awaitCl}_s\). In the attacker relation \(\color{red}{\rightarrow _b}\), arbitrary clients can send arbitrary values with \(\mathsf {awaitCl}_t\), leading to additional traces compared to the ones permitted in the source program where communication is modeled by \(\mathsf {awaitCl}_s\). We observe that \(\mathsf {awaitCl}_s\) generates the trace elements \(\mathsf {msg}(c, \color{red}{v}), \mathsf {wr}(0, \mathrm{sender}, c)\) for all \(\color{red}{v}\) and that \(\mathsf {awaitCl}_t\) generates the trace elements \(\mathsf {msg}(\color{red}{c^{\prime }}, \color{red}{v}), \mathsf {wr}(0, \mathrm{sender}, \color{red}{c^{\prime }})\) for all \(\color{red}{v}, \color{red}{c^{\prime }}\), which differ for \(\color{red}{c^{\prime }} \ne c\).
Compilation adds an \(\mathsf {assert}\) expression (Figure 10) evaluated after receiving a value from a client. The \(\mathsf {assert}\) gets stuck for configurations that produce trace elements with \(\color{red}{c^{\prime }} \ne c\), removing the traces of such configurations from the trace set, leaving only the traces where \(\color{red}{c^{\prime }} = c\). Hence, the trace set before and after compilation is equal under attack.
4 Implementation
Prisma is embedded into Scala (the host language) with its features implemented as a source-to-source macro expansion.5
The backend generating Solidity code is well separated. One could disable the compilation step to Solidity in the compilation pipeline, e.g., to run distributed code on multiple JVMs instead. In this case, the “contract code” would be executed by one computer (the “server”), and other computers would run the “client code.”
The Scala runtime of Prisma contains the implementation of the serializable 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 runtime wraps web3j [6] (for invoking transactions and interacting with the blockchain in general), headlong [3] (for serialization/deserialization in the Ethereum-specific serialization format) as well as code to parse Solidity and Ethereum error messages and to translate them to Scala error messages.
5 Evaluation
We evaluate Prisma along two research questions:
RQ1
Does Prisma support the most common dApps scenarios?
RQ2
Do Prisma’s abstractions affect performance?
Case Studies and Expressiveness (1). Five classes of smart contract applications have been identified [24]: Financial, Wallet, Notary, Game, and Library. To answer 1, we implemented at least one case study per category in Prisma . We implemented an ERC-20 Token,6 a Crowdfunding, and an Escrowing dApp as representatives of financial dApps. We cover 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 notary contract enabling users to store arbitrary data, e.g., document hashes or images, together with a submission timestamp and the data owner. As games, we implemented TicTacToe (Section 2), Rock-Paper-Scissors, Hangman, and Chinese Checkers. Rock-Paper-Scissors makes use of timed commitments [20], 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 library-based development in Prisma by including a TicTacToe library to our case studies and another TicTacToe dApp that uses that library instead of deploying the logic itself.
We also implemented a state channel [44, 45, 65] for TicTacToe in Prisma, which is an example for the class of scalability solutions that have emerged more recently. State channels enable parties to move parts of their dApp to a non-blockchain consensus system, falling back to the blockchain in case of disputes, thereby making the dApps more efficient where possible.
Our case studies are between 1k and 7.5k 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 4k (5.5k, 1.5k, 7.5k) [16]. We further elaborate on the case studies including a comparison of the lines of code in Prisma compared to the equivalent lines in Solidity and Javascript in Appendix A. Our case studies demonstrate that Prisma supports most common dApps scenarios.
Performance of Prisma DApps (2). Performance on the Ethereum blockchain is usually measured in terms of an Ethereum-specific metric called gas. Each instruction of the EVM consumes gas that needs to be paid for by the users in form of transaction fees credited to the miner. We refer to the Ethereum yellow paper [1] for an overview of the gas consumption of the different EVM instructions. To answer 2, we implement our case studies in both Prisma 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 [93].
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. Prisma 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 Ganache (Core v2.13.2) on the latest supported hard fork (Muir Glacier). All contracts are compiled to EVM byte code with 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.
Results. Figure 16 shows the average gas consumption of contract deployment (Figure 16(a)) and interaction (Figure 16(c)) as well as the relative overhead of Prisma vs. Solidity/JS of deployment (Figure 16(b)) and interaction (Figure 16(d)). 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 Prisma is close to the one of Solidity/JS. Our compiler achieves a deployment overhead of maximally 6% (TicTacToe) or 86k gas (TicTacToe Channel). The interaction overhead is below 10% for all case studies, which at most amounts to 3.55k gas.7
Fig. 16.
Prisma ’s deployment overhead is mainly due to the automated flow control. To guarantee correct execution, Prisma 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 45k 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 Prisma ’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%, some contract invocations are far above, 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 (20k gas) than changing its value (5k gas) [93], 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.
Besides the gas-overhead, we also consider the time-overhead of Prisma. In Ethereum, the estimated confirmation time for transactions is 3–5 minutes (assuming no congestion), which makes the number of on-chain interactions dominate the total execution time. As Prisma preserves the number of on-chain interactions, we assess the time-overhead of Prisma, if any, to be negligible.
Note that, per se, it is not possible to achieve a better gas consumption in Prisma than in Solidity—every contract compiled from Prisma 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 overhead. We are confident that further engineering effort can eliminate the observed overhead.
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, which our compiler performs automatically, manually 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 article.
6 Discussion and Related Work
6.1 Smart Contract Languages for Enforcing Protocols
We compare Prisma to Solidity, Obsidian [34, 35, 36], and Nomos [40, 41]. We highlight these languages, as those also address the correctness of the client–contract interactions. Table 2 overviews the features of the surveyed languages for (a) the perspective of defining interacting parties, (b) the used encoding of the interaction effects, and (c) the method used to check the contract-client interaction protocol. Figures 3(c), 17, and 18 show code snippets in these languages, each encoding the TicTacToe state machine from Figure 1. All three languages focus solely on the contract and do not state how clients are developed, hence only contract code is shown.
Table 2.
| Language | Encoding | Perspective | Protocol |
|---|---|---|---|
| Solidity | FSM | Local | Assertions |
| Obsidian | FSM | Local | Type states |
| Nomos | MNF | Local | Session types |
| Prisma | DS | Global | Control flow |
Fig. 17.
Fig. 18.
All three approaches take a 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 c, sending and receiving is represented by explicit statements (x = recv c; ... and send c x; ...).
The approaches differ in the encoding style of communication effects. Solidity and Obsidian adopt an FSM-style encoding: Contract fields encode states, methods encode transitions. The contract in Figure 3(c) represents FSM states via the phase field with initial state Funding (Line 30). The Fund, Move, and Payout methods are transitions, e.g., Payout transitions the contract into the final state Closed (Line 51). 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 monadic normal form (MNF) via do-notation to order effects. While the implementation of TicTacToe in FSM style requires three methods(Fund, Move, Payout—one per transition), we only need two methods in MNF-style (funding, executing—one per state with multiple entry points) and a single method in DS-style (init). For instance, the sequence of states and transitions \(Executing \mathrel {{ \mathrel {\mathop {\longrightarrow }\limits ^{ { { Move(x, y)} }}}}} Finished \mathrel {{ \mathrel {\mathop {\longrightarrow }\limits ^{ {{ Payout()} }}}}} 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 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 runtime assertions to guard against invoking the methods in an incorrect order (e.g., require(phase==Finished) in Figure 3(c), Line 40). Unlike Solidity, which does not support statically checking protocol compliance, Nomos and Obsidian employ 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 runtime enforcement with static checks helps detecting cases that are guaranteed to fail at runtime ahead of time.
Obsidian. 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 Figure 17 is annotated with the state in which it can be called, e.g., Payout requires state Finished, and transitions to Closed (Line 7).
Nomos. Nomos employs session types. The session types Funding, Executing, Finished in Figure 18 encode the protocol. Receiving a message is represented by a function type, e.g., in the Funding state, we receive an integer int -> ... (Line 1). We respond by either repeating the funding (Funding) or continuing to the next state of the protocol (Executing). This is represented by internal choice +{ ... }, which takes multiple possible responses giving each of them a unique label (notenough and enough). Type 1 indicates the end of a protocol (Line 3). The contract processes funding (Line 4) and executing (Line 8) implement the protocol. The recv operation (Line 5) takes a session-typed channel of form T -> U, returns a value of type T, and changes the type of the channel to U. A session type for internal choice (+{ ... }) requires the program to select one of the offered labels (e.g., $$s.notenough in Line 6 and $$s.enough in Line 7), e.g., in the left and right branch of a conditional statement.
Type systems. We show excerpts of simplified typing rules for Nomos and Obsidian (Figure 19). 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 NomosS (and 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 ^{\prime }\). An expression \(e\) has type \(t\) in context \(\Delta\) and changes \(\Delta\) to \(\Delta ^{\prime }\). We can see that variables change their type on method invocation (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^{\prime }_i\). For Prisma, instead, a standard judgment \(\Gamma \vdash e:T\) suffices for communication. Variables do not change their type. \(\mathsf {awaitCl}(p)\lbrace b\rbrace\) has type \(T\) in context \(\Gamma\) if \(p\) is a predicate of \(Addr\) and \(b\) is a pair of \(Ether\) and \(T\):
Fig. 19.
Prisma . As shown in Table 2, Prisma occupies an unexplored point in the design space: global instead of local perspective on interacting parties, DS instead of FSM or MNF encoding of effects, and control flow instead of extra protocol for governing interactions.
Prisma takes a 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 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 control flow of interaction points in the program—the compiler can automatically generate access and control guards with correctness guarantees. Semantically, Prisma 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 callback hell [46] 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.8 Additionally, the developer has to implement getters for public variables with complex data types such as arrays.9 We provide some code measurements (lines of code and number of cross-tier control-flow calls) of our Prisma and Solidity/JS dApp case studies in Appendix B.
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.10 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 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.
6.2 Other Related Work
Smart contract languages. Harz and Knottenbelt [55] survey smart contract languages, Hu et al. [58] survey smart contract tools and systems, Wöhrer and Zdun [92] give an overview of design patterns in smart contracts. Brünjes and Gabbay [29] distinguish between imperative and functional smart contract programming. Imperative contracts are based on the account model; the most prominent language is Solidity [4]. Functional ones [30, 83, 84] are based on EUTxO (Extended Unspent Transaction Output) model [52]. State channels [31, 44, 45, 65] optimistically optimize contracts for the functional model. Prisma does not yet support compilation to state channels, but we plan to treat them as another kind of tier.
Smart contracts as state machines. Scilla [85] is an automata-based compiler for contracts. FSolidM [63] enables creating contracts via a graphical interface. VeriSolid [64] generates contracts from graphical models enriched with predicates based on computational tree logic. EFSM tools [89] generate contracts from state machines and linear temporal logic. Prisma avoids a separate specification but infers transactions and their order from the control flow of a multitier dApp.
Analysis tools. Durieux et al. [43] and Ferreira et al. [48] empirically validate languages and tools and relate design patterns to security vulnerabilities, extending the survey by Di Angelo and Salzer [21]. Our work is complementary, targeting the correctness of the distributed program flow. For vulnerabilities not related to program flow (e.g., front-running or bad randomness), developers (using Solidity/JavaScript or Prisma) can use the surveyed analysis tools.
Multitier languages. Multitier programming was pioneered by Hop [86, 87]. Modeling a persistent session in client–server applications with continuations was mentioned by Queinnec [75] and elaborated in Links [38, 51]. Eliom [76] supports bidirectional client–server communication for web applications. ScalaLoci [91] generalizes the multitier model to generic distributed architectures. Our work specializes it to the dApp domain and its specific properties. Giallorenzo et al. [54] establish interesting connections between multitier (subjective) and choreographic (objective) languages—two variants of the global model. Prisma adopts the subjective view, which naturally fits the dApp domain, where a dominant role (contract) controls the execution and diverts control to other parties (clients) to collect their input.
Mashic [60] is a compiler for a mashup between two JavaScript programs: the untrusted embedded (iframe) gadget(s) and the trustworthy hosting integrator program, which communicate via messages. The authors prove that the compiler guarantees integrity and confidentiality. More specifically, the gadget(s) cannot learn more than what the integrator sends and, analogously, the gadget’s influence is limited to the integrator’s interface. In Mashic, the two programs are separate and the compiler checks that they communicate only via specified messages. In contrast, in Prisma, client and contract code are mixed. Thus, in addition to checking that only the specified messages are used, we can also check the interaction protocol—expressed by the structure of the control flow of the program—and ensure that it is followed by the target program after compilation.
Swift’s [33] secure automatic partitioning approach uses information flow policies to derive placements. Based on the policies, a constraint solver with integer programming heuristically picks a placement such that network traffic is minimal and information flow integrity is preserved. In contrast, placements in Prisma are explicit to the developer. Further, in blockchain programming, every single instruction generated by the compiler potentially incurs high costs. Therefore, we demonstrated that our compiler generates inexpensive programs, whereas Swift does not consider the program’s execution cost.
Effectful programs and meta-programming. MNF and CSP are widely discussed as intermediate compiler forms [23, 37, 50, 59, 62]. F# computation expressions [72] support control-flow operators in monadic expressions. OCaml supports a monadic and applicative let [11]: more flexible than do-notation but still restricted to MNF. Idris’ !-notation [5] inspired the GHC proposal for monadic inline binding [10]. Scala supports effectful programs through coroutines [8], async/await [80], monadic inline binding [27], Dsl.scala [94], and a (deprecated) compiler plugin for CPS translation [7]. The dotty-cps-async macro [88] supports async/await and similar effects for the Dotty compiler.
7 Conclusion
We proposed Prisma, the first global language for dApps that features direct style communication. Compared to the state-of-the-art, Prisma (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 Prisma informally, define its formal semantics, formalize the compilation process, and prove it correct. We demonstrate Prisma ’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.
Footnotes
1
700k to 2.7M contracts have been deployed per month between July 2020 and June 2021 [15] on the Ethereum blockchain—the most popular dApps platform [39]. Some dApps manage tremendous amounts of assets, e.g., Uniswap [17]—the largest Ethereum trading platform—had a daily trading volume of 0.5 B–1.5 B USD in June 2021.
2
We omit handling timeouts on funding and execution for brevity.
3
In Scala val/var definitions are used for mutable/immutable fields and variables, def for methods, class for classes, and object for singletons. A case class is a class whose instances are compared by structure and not by reference.
4
Type and semantics preservation is not the focus of this article; we presume them for our compiler without a formal proof.
5
The implementation entails 21 Scala files, 3,412 lines of Scala source code (non-blank, non-comment) licensed under Apache 2.0 Open Source. The compiler phases are macros that recurse over the Scala AST: (a) the guarding phase, (b) the “simplifying” phase (including MNF translation, CPS translation of terms, defunctionalization), and (c) the translation phase of (a subset) of Scala expressions and types to a custom intermediate representation based on Scala case classes. The intermediate representation is translated to Solidity code and passed to the Solidity compiler (solc).
6
A study investigating all blocks mined until September 15, 2018 [70], found that 72.9 % of the high-activity contracts are token contracts compliant to ERC-20 or ERC-721, with an accumulated market capitalization of 12.7B USD.
7
Equals 0.59 USD based on gas price and exchange course of April 15, 2021.
8
Obsidian and Nomos do not provide any client design, so we can only compare to Solidity/JavaScript.
9
For simple data types, the getter is generated automatically.
10
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).
A Case Studies
This section describes the implemented case studies in detail. Bartoletti and Pompianu [24] identify five classes of smart contract applications: Financial, Notary, Game, Wallet, and Library. Our case studies include at least one application per category (Table 3). In addition, we consider scalability solutions.
Table 3.
| Category | Case study | Cross-tier calls | Prisma LoC | Solidity + JavaScript LoC |
|---|---|---|---|---|
| Financial | Token | 4 | 79 | 48 + 50 |
| Crowdfunding | 11 | 59 | 27 + 63 | |
| Escrow | 9 | 63 | 33 + 56 | |
| Wallet | Multi-signature wallet | 3 | 76 | 41 + 52 |
| Notary | General-purpose notary | 3 | 32 | 16 + 36 |
| Game | Rock Paper Scissors | 12 | 79 | 41 + 77 |
| TicTacToe | 5 | 61 | 31 + 52 | |
| Hangman | 15 | 119 | 86 + 83 | |
| Chinese Checkers | 4 | 167 | 141 + 47 | |
| Library | TicTacToe library | – | 167 | 141 + – |
| TicTacToe using library | 5 | 53 | 29 + 52 | |
| Scalability | TicTacToe channel | 9 | 177 | 56 + 177 |
Financial. These apps include digital tokens, crowdfunding, escrowing, advertisement, insurances, and sometimes Ponzi schemes. A study investigating all blocks mined until September 15th, 2018 [70], 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 Prisma 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 Prisma, which is the basic functionality of financial applications. Other financial use cases can be implemented in Prisma with similar techniques.
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 Prisma .
Games. We implemented TicTacToe (Section 2), Rock-Paper-Scissors, Hangman, and Chinese Checkers. Hangman evolves through multiple phases and hence benefits from the explicit control flow definition in Prisma 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 [20], 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, then 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.
Wallet. A wallet contract manages digital assets, i.e., cryptocurrencies and tokens, and offers additional features such as shared ownership or daily transaction limits. As of August 30, 2019, 3.9M of 17.9M (21%) deployed smart contracts have been different types of wallet contracts [22]. 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 runtime input, demonstrating calls among contracts in Prisma . 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 Prisma .
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 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 Prisma, 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.
Scalability solutions. State channels [44, 45, 65] 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 TicTacToe11 to demonstrate that Prisma supports state channels.
B Empirical Evaluation of Design Quality
In Section 6, we argued that with Prisma, (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 Prisma ’s design and do not require further evidence. Claim (c) has been formally proven in Section 3. It remains to investigate claim (e), i.e., in which extent Prisma reduces the amount of code and error-prone control-flow jumps.
To this end, we implemented all case studies with equivalent functionality in Prisma 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 Prisma and the Solidity implementations) 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 20). The results in Figure 20 show that case studies written in Prisma 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.
Fig. 20.
Second, we consider occurrences of explicit cross-tier control-flow calls in the Solidity/JavaScript dApps (cf. Table 3), which complicate control flow, compared to Prisma, 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, however, ensures that the control flow of the contract always continues in the line that passed the control flow to the client by invoking an awaitCl expression.
C Proofs
We provide the definition of \(\mathsf {comp}^{\prime }\) and \(\mathsf {comp}\) in Figure 21, the definition for the free variables for a given term \({\mathit {fv}}\) in Figure 22, and the detailed proofs for the theorem and the lemmas on the following pages.
Fig. 21.
Fig. 22.
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.,
\begin{equation*} \forall P. ~~~ \lbrace ~ init_A(comp^{\prime }(mnf^{\prime }((P)))) ~\rbrace \approx \cdots \approx \lbrace ~ init_A(P) ~\rbrace . \end{equation*}
\begin{equation*} \begin{array}{cl} \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad &~ init_A(comp^{\prime }(mnf^{\prime }(P)))\qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \\ \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad ~\overset{{\text{Lemma}\;\href{#thm4}{\text{3}}}}{\approx } &~ init_A(mnf^{\prime }(P))\qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \\ \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad ~\overset{{\text{Lemma}\;\href{#thm6}{\text{5}}}}{\approx } &~ init_A(P).\qquad \qquad \qquad \qquad \qquad \qquad \qquad \quad \\ \end{array} \end{equation*}
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 runtime.
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:
\begin{equation*} p;q;e \Downarrow ^n ~~=~ \lbrace ~ (p^{\prime },v) ~|~ (p;q;e) \rightarrow ^n (p^{\prime };q^{\prime };v) ~\rbrace ~~~~~~~~~~~~~~~~~~~~~~~~~ T \Downarrow ^n ~=~ \bigcup _{p;q;e \in T} ~ p;q;e \Downarrow ^n . \end{equation*}
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:
\begin{equation*} (T \approx ^n S) ~~~\Leftrightarrow ~~~ (T\Downarrow ^n ~\#_{\text{set}}~ S\Downarrow ^n), \end{equation*}
where \(\#_\text{set}\) is defined on trace sets as
\begin{equation*} T \#_{\text{set}} S ~~~\Leftrightarrow ~~~ (\forall t {\in } T.~ \exists s {\in } S.~~ t ~\#_{\text{trace}}~ s) \wedge (\forall s {\in } S.~ \exists t {\in } T.~~ t~ \#_{\text{trace}}~ s) \end{equation*}
and \(\#_\text{trace}\) on event traces as
\begin{equation*} \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}. \end{equation*}
\(assoc\) is 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 valid programs are closed terms, we show that \(assoc\) preserves the traceset of an open term \(e\) that is closed by substitution \([x⟾ v]\).
For all terms \({{e}}\), traces \({{p}}\), traces \({{q}}\), values \(v\), patterns \(x\),
\begin{equation*} \lbrace ~{{p}};{{q}};~[x{⟾ }v]~assoc({{e}})~\rbrace ~\approx ~ \cdots ~\approx ~ \lbrace ~{{p}};{{q}};~[x{⟾ }v]~{{e}}~\rbrace . \end{equation*}
By induction over term structure.
Case. \(~~~{{e}}~=~({\mathsf {let~}}x_1=({\mathsf {let~}}x_0={{e}}_0;~{{e}}_1);~{{e}}_2)\).
We know \(x_0~{\notin }~{\mathit {fv}}({{e}}_2)\), since \({{e}}_2\) is not in the scope of the \(x_0\) binding and that all identifiers are distinct, which can always be achieved by \(\alpha\)-renaming.
\begin{equation*} ~x_0~{\notin }~{\mathit {fv}}({{e}}_2) \end{equation*}
According to \(\approx\), we only consider terms that reduce to a value. Therefore, let \(\phi\) be the judgment that the term \({{e}}_0\) closed by \([x{⟾ }v]\) with trace \({{p}}\) evaluates to a value \(v_0\) producing trace \(p_0\).
\begin{equation*} ~\phi ~\equiv ~~~~({{p}};{{q}};~[x{⟾ }v]{{e}}_0~~~{\rightarrow }^*~~{{p}}~p_0;{{q}};~v_0) \end{equation*}
The lemma holds by the following chain of transitive relations. We evaluate the compiled program from top to bottom (\(~{\rightarrow }^*\)) and the original program from bottom to top (\(~{\leftarrow }^*\)) until configurations converge. The induction hypothesis (IH) allows the removal of \(assoc\) in redex position under traceset equality (\(\approx\)).
| \({\left\lbrace \begin{array}{l}{{p}};{{q}};~[x{⟾ }v]~assoc({{e}}) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; [x|=\gt v] assoc(e) \end{array}\right\rbrace }\right\rbrace\) | |
| \(\overset{\text{def.~}{{e}}}{=}\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~[x{⟾ }v]~assoc({\mathsf {let~}}x_1=({\mathsf {let~}}x_0={{e}}_0;~{{e}}_1);~{{e}}_2) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; [x|=\gt v] assoc(let x1=(let x0=e0; e1); e2) \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{\text{def.~}assoc}{=}\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~[x{⟾ }v]~assoc({\mathsf {let~}}x_0={{e}}_0;~assoc({\mathsf {let~}}x_1={{e}}_1;~{{e}}_2)) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; [x|=\gt v] assoc(let x0=e0; assoc(let x1=e1; e2)) \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{IH}{\approx }\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~[x{⟾ }v]~{\mathsf {let~}}x_0={{e}}_0;~assoc({\mathsf {let~}}x_1={{e}}_1;~{{e}}_2) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; [x|=\gt v] let x0=e0; assoc(let x1=e1; e2) \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{\text{def.~}{⟾ }}{=}\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~{\mathsf {let~}}x_0=[x{⟾ }v]~{{e}}_0;~[x{⟾ }v]~assoc({\mathsf {let~}}x_1={{e}}_1;~{{e}}_2) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; let x0=[x|=\gt v] e0; [x|=\gt v] assoc(let x1=e1; e2) \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{\phi }{~{\rightarrow }^*}\) | \({\left\lbrace \begin{array}{l}{{p}}~p_0;{{q}};~{\mathsf {let~}}x_0=v_0;~[x{⟾ }v]~assoc({\mathsf {let~}}x_1={{e}}_1;~{{e}}_2)~|~\forall ~v_0~p_0,~\phi \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p p0;q; let x0=v0; [x|=\gt v] assoc(let x1=e1; e2) | \forall v0 p0, \phi \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{{\rm R}{\rm\small{LET}}}{~{\rightarrow }}\) | \({\left\lbrace \begin{array}{l}{{p}}~p_0;{{q}};~[x_0{⟾ }v_0,~x{⟾ }v]~assoc({\mathsf {let~}}x_1={{e}}_1;~{{e}}_2)~|~\forall ~v_0~p_0,~\phi \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p p0;q; [x0|=\gt v0, x|=\gt v] assoc(let x1=e1; e2) | \forall v0 p0, \phi \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{IH}{\approx }\) | \({\left\lbrace \begin{array}{l}{{p}}~p_0;{{q}};~[x_0{⟾ }v_0,~x{⟾ }v]~{\mathsf {let~}}x_1={{e}}_1;~{{e}}_2~|~\forall ~v_0~p_0,~\phi \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p p0;q; [x0|=\gt v0, x|=\gt v] let x1=e1; e2 | \forall v0 p0, \phi \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{\text{def.~}{⟾ };~x_0~{\notin }~{\mathit {fv}}({{e}}_2)}{=}\) | \({\left\lbrace \begin{array}{l}{{p}}~p_0;{{q}};~{\mathsf {let~}}x_1=[x_0{⟾ }v_0,~x{⟾ }v]{{e}}_1;~[x{⟾ }v]{{e}}_2~|~\forall ~v_0~p_0,~\phi \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p p0;q; let x1=[x0|=\gt v0, x|=\gt v]e1; [x|=\gt v]e2 | \forall v0 p0, \phi \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{{\rm R}{\rm\small{LET}}}{~{\leftarrow }}\) | \({\left\lbrace \begin{array}{l}{{p}}~p_0;{{q}};~{\mathsf {let~}}x_1=({\mathsf {let~}}x_0=v_0;~[x{⟾ }v]{{e}}_1);~[x{⟾ }v]{{e}}_2~|~\forall ~v_0~p_0,~\phi \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p p0;q; let x1=(let x0=v0; [x|=\gt v]e1); [x|=\gt v]e2 | \forall v0 p0, \phi \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{\phi }{~{\leftarrow }^*}\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~{\mathsf {let~}}x_1=({\mathsf {let~}}x_0=[x{⟾ }v]{{e}}_0;~[x{⟾ }v]{{e}}_1);~[x{⟾ }v]{{e}}_2 \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; let x1=(let x0=[x|=\gt v]e0; [x|=\gt v]e1); [x|=\gt v]e2 \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{\text{def.~}{⟾ }}{=}\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~[x{⟾ }v]~{\mathsf {let~}}x_1=({\mathsf {let~}}x_0={{e}}_0;~{{e}}_1);~{{e}}_2 \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; [x|=\gt v] let x1=(let x0=e0; e1); e2 \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{\text{def.~}{{e}}}{=}\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~[x{⟾ }v]~{{e}} \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; [x|=\gt v] e \end{array}\right\rbrace }\right\rbrace\) |
Case. \(~~~{{e}}~\ne ~({\mathsf {let~}}x_1=({\mathsf {let~}}x_0={{e}}_0;~{{e}}_1);~{{e}}_2)\).
If \({{e}}\) is not of nested let form, then we simply apply the definition of \(assoc\).
| \({\left\lbrace \begin{array}{l}{{p}};{{q}};~[x{⟾ }v]~assoc({{e}}) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; [x|=\gt v] assoc(e) \end{array}\right\rbrace }\right\rbrace \qquad \qquad \qquad \qquad \qquad \qquad\) | |
| \(\overset{\text{def.~}assoc}{=}\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~[x{⟾ }v]~{{e}} \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; [x|=\gt v] e \end{array}\right\rbrace }\right\rbrace \qquad \qquad \qquad \qquad \qquad \qquad \qquad □\) |
\(mnf\) is 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 valid programs are closed terms, we show that \(mnf\) preserves the traceset of an open term \(e\) that is closed by substitution \([x⟾ v]\).
For all terms \({{e}}\), traces \({{p}}\), traces \({{q}}\), values \(v\), patterns \(x\),
\begin{equation*} \lbrace ~{{p}};{{q}};~[x{⟾ }v]~mnf({{e}})~\rbrace ~\approx ~ \cdots ~\approx ~ \lbrace ~{{p}};{{q}};~[x{⟾ }v]~{{e}}~\rbrace . \end{equation*}
By induction over term structure. Case. \({{e}}~=~{{e}}_0~{{e}}_1\).
According to \(\approx\), we only consider terms that reduce to a value. Therefore, let \(\phi _0\) be the judgment that the term \({{e}}_0\) closed by \([x{⟾ }v]\) with trace \({{p}}\) evaluates to a value \(v_0\) producing trace \(p_0\). Let \(\phi _1\) be the judgment that the term \({{e}}_1\) closed by \([x{⟾ }v]\) with trace \({{p}}~p_0\) evaluates to a value \(v_1\) producing trace \({{p}}~p_0~p_1\).
\begin{equation*} ~\phi _0~\equiv ~~~~({{p}};{{q}};~[x{⟾ }v]~{{e}}_0~~~{\rightarrow }^*~~{{p}}~p_0;{{q}};~v_0) \end{equation*}
\begin{equation*} ~\phi _1~\equiv ~~~~({{p}}~p_0;{{q}};~[x{⟾ }v]~{{e}}_1~~~{\rightarrow }^*~~{{p}}~p_0~p_1;{{q}};~v_1) \end{equation*}
Let \(id_0\) be the fresh identifier \(mnf\) produces.
\begin{equation*} ~id_0~{\mathsf {fresh}} \end{equation*}
The lemma holds by the following chain of transitive relations. We evaluate the compiled program from top to bottom (\(~{\rightarrow }^*\)) and the original program from bottom to top (\(~{\leftarrow }^*\)) until configurations converge. The IH allows the removal of \(mnf\) in redex position under traceset equality (\(\approx\)).
| \({\left\lbrace \begin{array}{l}{{p}};{{q}};~[x{⟾ }v]~mnf({{e}}) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; [x|=\gt v] mnf(e) \end{array}\right\rbrace }\right\rbrace\) | |
| \(\overset{\text{def.~}{{e}}}{=}\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~[x{⟾ }v]~mnf({{e}}_0~{{e}}_1) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; [x|=\gt v] mnf(e0 e1) \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{\text{def.~}mnf}{=}\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~[x{⟾ }v]~assoc({\mathsf {let~}}id_0=mnf({{e}}_0);~assoc({\mathsf {let~}}id_1=mnf({{e}}_1);~id_0~id_1)) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; [x|=\gt v] assoc(let id0=mnf(e0); assoc(let id1=mnf(e1); id0 id1)) \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{{\text{Lemma}\;\href{#thm2}{\text{1}}}}{\approx }\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~[x{⟾ }v]~{\mathsf {let~}}id_0=mnf({{e}}_0);~assoc({\mathsf {let~}}id_1=mnf({{e}}_1);~id_0~id_1) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; [x|=\gt v] let id0=mnf(e0); assoc(let id1=mnf(e1); id0 id1) \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{\text{def.~}{⟾ }}{=}\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~{\mathsf {let~}}id_0=[x{⟾ }v]~mnf({{e}}_0);~[x{⟾ }v]~assoc({\mathsf {let~}}id_1=mnf({{e}}_1);~id_0~id_1) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; let id0=[x|=\gt v] mnf(e0); [x|=\gt v] assoc(let id1=mnf(e1); id0 id1) \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{IH}{\approx }\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~{\mathsf {let~}}id_0=[x{⟾ }v]~{{e}}_0;~[x{⟾ }v]~assoc({\mathsf {let~}}id_1=mnf({{e}}_1);~id_0~id_1)) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; let id0=[x|=\gt v] e0; [x|=\gt v] assoc(let id1=mnf(e1); id0 id1)) \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{\phi _0}{~{\rightarrow }^*}\) | \({\left\lbrace \begin{array}{l}{{p}}~p_0;{{q}};~{\mathsf {let~}}id_0=v_0;~[x{⟾ }v]~assoc({\mathsf {let~}}id_1=mnf({{e}}_1);~id_0~id_1)~|~\forall ~v_0~p_0,~{\mathsf {if}}~\phi _0 \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p p0;q; let id0=v0; [x|=\gt v] assoc(let id1=mnf(e1); id0 id1) | \forall v0 p0, if \phi _0 \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{{\rm R}{\rm\small{LET}}}{~{\rightarrow }}\) | \({\left\lbrace \begin{array}{l}{{p}}~p_0;{{q}};~[id_0{⟾ }v_0,~x{⟾ }v]~assoc({\mathsf {let~}}id_1=mnf({{e}}_1);~id_0~id_1)~|~\forall ~v_0~p_0,~{\mathsf {if}}~\phi _0 \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p p0;q; [id0|-\gt v0, x|=\gt v] assoc(let id1=mnf(e1); id0 id1) | \forall v0 p0, if \phi _0 \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{\text{Lemma~}1}{\approx }\) | \({\left\lbrace \begin{array}{l}{{p}}~p_0;{{q}};~[id_0{⟾ }v_0,~x{⟾ }v]~{\mathsf {let~}}id_1=mnf({{e}}_1);~id_0~id_1~|~\forall ~v_0~p_0,~{\mathsf {if}}~\phi _0 \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p p0;q; [id0|-\gt v0, x|=\gt v] let id1=mnf(e1); id0 id1 | \forall v0 p0, if \phi _0 \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{\text{def.~}{⟾ }}{=}\) | \({\left\lbrace \begin{array}{l}{{p}}~p_0;{{q}};~{\mathsf {let~}}id_1=[id_0{⟾ }v_0,~x{⟾ }v]~mnf({{e}}_1);~v_0~id_1~|~\forall ~v_0~p_0,~{\mathsf {if}}~\phi _0 \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p p0;q; let id1=[id0|-\gt v0, x|=\gt v] mnf(e1); v0 id1 | \forall v0 p0, if \phi _0 \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{IH}{=}\) | \({\left\lbrace \begin{array}{l}{{p}}~p_0;{{q}};~{\mathsf {let~}}id_1=[id_0{⟾ }v_0,~x{⟾ }v]~{{e}}_1;~v_0~id_1~|~\forall ~v_0~p_0,~{\mathsf {if}}~\phi _0 \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p p0;q; let id1=[id0|-\gt v0, x|=\gt v] e1; v0 id1 | \forall v0 p0, if \phi _0 \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{id_0~{\mathsf {fresh}}}{=}\) | \({\left\lbrace \begin{array}{l}{{p}}~p_0;{{q}};~{\mathsf {let~}}id_1=[x{⟾ }v]~{{e}}_1;~v_0~id_1~|~\forall ~v_0~p_0,~{\mathsf {if}}~\phi _0 \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p p0;q; let id1=[x|=\gt v] e1; v0 id1 | \forall v0 p0, if \phi _0 \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{\phi _1}{~{\rightarrow }^*}\) | \({\left\lbrace \begin{array}{l}{{p}}~p_0~p_1;{{q}};~{\mathsf {let~}}id_1=v_1;~v_0~id_1~|~\forall ~v_0~v_1~p_0~p_1,~{\mathsf {if}}~\phi _0,~\phi _1 \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p p0 p1;q; let id1=v1; v0 id1 | \forall v0 v1 p0 p1, if \phi _0, \phi _1 \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{{\rm R}{\rm\small{LET}}}{~{\rightarrow }}\) | \({\left\lbrace \begin{array}{l}{{p}}~p_0~p_1;{{q}};~v_0~v_1~|~\forall ~v_0~v_1~p_0~p_1,~{\mathsf {if}}~\phi _0,~\phi _1 \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p p0 p1;q; v0 v1 | \forall v0 v1 p0 p1, if \phi _0, \phi _1 \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{\phi _1}{~{\leftarrow }^*}\) | \({\left\lbrace \begin{array}{l}{{p}}~p_0;{{q}};~v_0~[x{⟾ }v]~{{e}}_1~|~\forall ~v_0~p_0,~{\mathsf {if}}~\phi _0 \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p p0;q; v0 [x|=\gt v] e1 | \forall v0 p0, if \phi _0 \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{\phi _0}{~{\leftarrow }^*}\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~([x{⟾ }v]~{{e}}_0)~[x{⟾ }v]~{{e}}_1 \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; ([x|=\gt v] e0) [x|=\gt v] e1 \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{\text{def.~}{⟾ }}{=}\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~[x{⟾ }v]~{{e}}_0~{{e}}_1 \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; [x|=\gt v] e0 e1 \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{\text{def.~}{{e}}}{=}\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~[x{⟾ }v]~{{e}} \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; [x|=\gt v] e \end{array}\right\rbrace }\right\rbrace\) |
Case. \(~~{{e}}~=~{\mathsf {let~}}id_0={{e}}_0;~{{e}}_1\).
According to \(\approx\), we only consider terms that reduce to a value. Therefore, let \(\phi\) be the judgment that the term \({{e}}_0\) closed by \([x{⟾ }v]\) with trace \({{p}}\) evaluates to a value \(v_0\) producing trace \(p_0\).
\begin{equation*} ~\phi _0~\equiv ~~~~({{p}};{{q}};~[x{⟾ }v]~{{e}}_0~~~{\rightarrow }^*~~{{p}}~p_0;{{q}};~v_0) \end{equation*}
The lemma holds by the following chain of transitive relations. We evaluate the compiled program from top to bottom (\(~{\rightarrow }^*\)) and the original program from bottom to top (\(~{\leftarrow }^*\)) until configurations converge. The IH allows the removal of \(mnf\) in redex position under traceset equality (\(\approx\)).
| \({\left\lbrace \begin{array}{l}{{p}};{{q}};~[x{⟾ }v]~mnf({{e}}) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; [x|=\gt v] mnf(e) \end{array}\right\rbrace }\right\rbrace\) | |
| \(\overset{\text{def.~}{{e}}}{=}\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~[x{⟾ }v]~mnf({\mathsf {let~}}id_0=v_0;~{{e}}_1) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; [x|=\gt v] mnf(let id0=v0; e1) \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{\text{def.~}mnf}{=}\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~[x{⟾ }v]~assoc({\mathsf {let~}}id_0=mnf({{e}}_0);~mnf({{e}}_1)) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; [x|=\gt v] assoc(let id0=mnf(e0); mnf(e1)) \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{\text{Lemma~}1}{\approx }\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~[x{⟾ }v]~{\mathsf {let~}}id_0=mnf({{e}}_0);~mnf({{e}}_1) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; [x|=\gt v] let id0=mnf(e0); mnf(e1) \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{\text{def.~}{⟾ }}{=}\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~{\mathsf {let~}}id_0=[x{⟾ }v]~mnf({{e}}_0);~[x{⟾ }v]~mnf({{e}}_1) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; let id0=[x|=\gt v] mnf(e0); [x|=\gt v] mnf(e1) \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{IH}{\approx }\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~{\mathsf {let~}}id_0=[x{⟾ }v]~{{e}}_0;~[x{⟾ }v]~mnf({{e}}_1) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; let id0=[x|=\gt v] e0; [x|=\gt v] mnf(e1) \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{\phi _0}{~{\rightarrow }^*}\) | \({\left\lbrace \begin{array}{l}{{p}}~p_0;{{q}};~{\mathsf {let~}}id_0=v_0;~[x{⟾ }v]~mnf({{e}}_1)~|~\forall ~v_0~p_0,~{\mathsf {if}}~\phi _0 \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p p0;q; let id0=v0; [x|=\gt v] mnf(e1) | \forall v0 p0, if \phi _0 \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{{\rm R}{\rm\small{LET}}}{~{\rightarrow }}\) | \({\left\lbrace \begin{array}{l}{{p}}~p_0;{{q}};~[id_0{⟾ }v_0,~x{⟾ }v]~mnf({{e}}_1)~|~\forall ~v_0~p_0,~{\mathsf {if}}~\phi _0 \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p p0;q; [id0|-\gt v0, x|=\gt v] mnf(e1) | \forall v0 p0, if \phi _0 \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{IH}{\approx }\) | \({\left\lbrace \begin{array}{l}{{p}}~p_0;{{q}};~[id_0{⟾ }v_0,~x{⟾ }v]~{{e}}_1~|~\forall ~v_0~p_0,~{\mathsf {if}}~\phi _0 \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p p0;q; [id0|-\gt v0, x|=\gt v] e1 | \forall v0 p0, if \phi _0 \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{{\rm R}{\rm\small{LET}}}{~{\leftarrow }}\) | \({\left\lbrace \begin{array}{l}{{p}}~p_0;{{q}};~[x{⟾ }v]~{\mathsf {let~}}id_0=v_0;~{{e}}_1~|~\forall ~v_0~p_0,~{\mathsf {if}}~\phi _0 \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p p0;q; [x|=\gt v] let id0=v0; e1 | \forall v0 p0, if \phi _0 \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{\phi _0}{~{\leftarrow }^*}\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~[x{⟾ }v]~{\mathsf {let~}}id_0={{e}}_0;~{{e}}_1 \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; [x|=\gt v] let id0=e0; e1 \end{array}\right\rbrace }\right\rbrace\) |
| \(\overset{\text{def.~}{{e}}}{=}\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~[x{⟾ }v]~{{e}} \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; [x|=\gt v] e \end{array}\right\rbrace }\right\rbrace\) |
Case. \(\text{The~other~cases~of~${{e}}$~are~proved~analogously}\).\(□\)□
\(mnf^{\prime }\) is defined on programs. To evaluate a program, it is initialized with a set of clients \(A\). \(mnf^{\prime }\) preserves the traceset of (closed) programs \(P\) for any set of clients \(A\).
For all \(P\),
\begin{equation*} \lbrace ~init_A(mnf^{\prime }(P))~\rbrace ~\approx ~ \cdots ~\approx ~ \lbrace ~init_A(P)~\rbrace . \end{equation*}
By induction over term structure. Case. \(~~P~=~({{d}};{{b}};~{{e}}_0)\).
Initializing the definitions \({{d}};{{b}}\) with \(A\) produces the trace \({{p}}\) and the state \({{q}}\).
\begin{equation*} ~init_A({{d}};{{b}})~=~{{p}};{{q}} \end{equation*}
According to \(\approx\), we only consider terms that reduce to a value. Therefore, let \(\phi\) be the judgment that the term \({{e}}_0\) closed by \([x{⟾ }v]\) in trace \({{p}}\) produces a value \(v_0\) and trace \(p_0\).
\begin{equation*} ~\phi ~\equiv ~~~~({{p}};{{q}};~{{e}}_0~~~{\rightarrow }^*~~{{p}}~p_0;{{q}};~v_0) \end{equation*}
The lemma holds by the following chain of transitive relations. We evaluate the compiled program from top to bottom (\(~{\rightarrow }^*\)) and the original program from bottom to top (\(~{\leftarrow }^*\)) until configurations converge, using Lemma 2.
| \(\qquad \qquad \qquad \qquad \qquad\) | \({\left\lbrace \begin{array}{l}init_A(mnf^{\prime }(P)) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} init_A(mnf^{\prime }(P)) \end{array}\right\rbrace }\right\rbrace \qquad \qquad \qquad \qquad \qquad\) |
| \(\qquad \qquad \qquad \qquad \qquad \overset{\text{def.~}P}{=}\) | \({\left\lbrace \begin{array}{l}init_A(mnf^{\prime }({{d}};{{b}};~{{e}}_0)) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} init_A(mnf^{\prime }(d;b; e0)) \end{array}\right\rbrace }\right\rbrace \qquad \qquad \qquad \qquad \qquad\) |
| \(\qquad \qquad \qquad \qquad \qquad \overset{\text{def.~}mnf^{\prime }}{=}\) | \({\left\lbrace \begin{array}{l}init_A({{d}};{{b}};~{{\mathsf {trmp}}}(mnfe({\mathsf {Done}}({{e}}_0)))) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} init_A(d;b; tramp(mnfe(Done(e0)))) \end{array}\right\rbrace }\right\rbrace \qquad \qquad \qquad \qquad \qquad\) |
| \(\qquad \qquad \qquad \qquad \qquad \overset{\text{def.~}init_A}{=}\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~{{\mathsf {trmp}}}(mnfe({\mathsf {Done}}({{e}}_0))) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; tramp(mnfe(Done(e0))) \end{array}\right\rbrace }\right\rbrace \qquad \qquad \qquad \qquad \qquad\) |
| \(\qquad \qquad \qquad \qquad \qquad \overset{{\text{Lemma}\;\href{#thm3}{\text{2}}}}{\approx }\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~{{\mathsf {trmp}}}({\mathsf {Done}}({{e}}_0)) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; tramp(Done(e0)) \end{array}\right\rbrace }\right\rbrace \qquad \qquad \qquad \qquad \qquad\) |
| \(\qquad \qquad \qquad \qquad \qquad \overset{\phi }{~{\rightarrow }^*}\) | \({\left\lbrace \begin{array}{l}{{p}}~p_0;{{q}};~{{\mathsf {trmp}}}({\mathsf {Done}}(v_0))~|~\forall ~v_0~p_0,~{\mathsf {if}}~\phi \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p p0;q; tramp(Done(v0)) | \forall v0 p0, if \phi \end{array}\right\rbrace }\right\rbrace \qquad \qquad \qquad \qquad \qquad\) |
| \(\qquad \qquad \qquad \qquad \qquad \overset{{\rm R}{\rm\small{DONE}}}{~{\rightarrow }}\) | \({\left\lbrace \begin{array}{l}{{p}}~p_0;{{q}};~v_0~|~\forall ~v_0~p_0,~{\mathsf {if}}~\phi \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p p0;q; v0 | \forall v0 p0, if \phi \end{array}\right\rbrace }\right\rbrace \qquad \qquad \qquad \qquad \qquad\) |
| \(\qquad \qquad \qquad \qquad \qquad \overset{\phi }{~{\leftarrow }^*}\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~{{e}}_0 \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; e0 \end{array}\right\rbrace }\right\rbrace \qquad \qquad \qquad \qquad \qquad\) |
| \(\qquad \qquad \qquad \qquad \qquad \overset{\text{def.~}init_A}{=}\) | \({\left\lbrace \begin{array}{l}init_A({{d}};{{b}};~{{e}}_0) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} init_A(d;b; e0) \end{array}\right\rbrace }\right\rbrace \qquad \qquad \qquad \qquad \qquad\) |
| \(\qquad \qquad \qquad \qquad \qquad \overset{\text{def.~}P}{=}\) | \({\left\lbrace \begin{array}{l}init_A(P) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} init_A(P) \end{array}\right\rbrace }\right\rbrace \qquad \qquad \qquad \qquad \quad □\) |
\(comp\) is defined on programs. To evaluate a program, it is initialized with a set of clients \(A\). \(comp\) preserves the traceset of (closed) programs \(P\) for any set of clients \(A\).
For all definitions \({{b}}\), definitions \({{d}}\), terms \({{e}}\), values \(v\), patterns \(x\),
\begin{equation*} \lbrace ~[x{⟾ }v]~init_A(comp({{d}};{{b}};~{{\mathsf {trmp}}}({{e}})))~\rbrace ~\approx ~ \cdots ~\approx ~ \lbrace ~init_A({{d}};{{b}};~{{\mathsf {trmp}}}([x{⟾ }v]~{{e}}))~\rbrace . \end{equation*}
By induction over term structure. Case. \(~~~{{e}}~=~{\mathsf {let~}}x={\mathsf {awaitCl}}_s(({{e}}_0,~()~{\rightarrow }{{e}}_1));~{{e}}_2\).
\(comp\) expects the definitions \({{b}}\) to be of form:
\begin{equation*} {{b}}~=~\left(\begin{array}{l}~{\mathsf {@cl}}~\mathsf {this}.{\mathsf {clfn}}~=~id~{\rightarrow }~{{e}}_{1,alt};\\ ~{\mathsf {@co}}~\mathsf {this}.{\mathsf {cofn}}~=~id~{\rightarrow }~{{e}}_{2,alt};\\ ~b_{rest}\end{array}\right). \end{equation*}
\(comp\) is defined recursively and applied to the term \({{e}}_2\). Intuitively, \(comp\) transforms \({{e}}_2\) to \({{e}}_2^{\prime }\) and \({{b}}\) to \({{b}}^{\prime }\) by moving the part of \({{e}}_2\) that comes after the \({\mathsf {awaitCl}}_s\) call into the \({\mathsf {cofn}}\) definition inside \({{b}}\). The recursive call is given as follows:
\begin{equation*} ({{d}};{{b}}^{\prime };~{{\mathsf {trmp}}}({{e}}_2^{\prime }))~=~comp({{d}};{{b}};~{{\mathsf {trmp}}}({{e}}_2)) \end{equation*}
\begin{equation*} {{b}}^{\prime }~=~\left(\begin{array}{l}~{\mathsf {@cl}}~\mathsf {this}.{\mathsf {clfn}}~=~id~{\rightarrow }~{{e}}_{1,alt}^{\prime };\\ ~{\mathsf {@co}}~\mathsf {this}.{\mathsf {cofn}}~=~id~{\rightarrow }~{{e}}_{2,alt}^{\prime };\\ ~b_{rest}\end{array}\right). \end{equation*}
After the recursive call, \(comp\) moves the transformed \({{e}}_2^{\prime }\) into the \({\mathsf {cofn}}\) definition, resulting in \({{e}}^{\prime }\) and \({{b}}^{\prime \prime }\) with \({{e}}_{1,alt}^{\prime \prime }\) and \({{e}}_{2,alt}^{\prime \prime }\).
\begin{equation*} ~\phi ~\equiv ~~~~\big (~\lbrace ~{{d}};{{b}}^{\prime \prime };~{{\mathsf {trmp}}}({{e}}^{\prime })~\big \rbrace ~=~\big \lbrace ~comp({{d}};{{b}};~{{\mathsf {trmp}}}({{e}}))~\rbrace ~\big) \end{equation*}
\begin{equation*} {{b}}^{\prime \prime }~=~\left(\begin{array}{l}~{\mathsf {@cl}}~\mathsf {this}.{\mathsf {clfn}}~=~id~{\rightarrow }~{{e}}_{1,alt}^{\prime \prime };\\ ~{\mathsf {@co}}~\mathsf {this}.{\mathsf {cofn}}~=~id~{\rightarrow }~{{e}}_{2,alt}^{\prime \prime };\\ ~b_{rest}\end{array}\right) \end{equation*}
\begin{equation*} {{e}}_{1,alt}^{\prime \prime }~=~\left(\begin{array}{l}~{\mathsf {if}}~{\mathsf {let~}}(c~{\mathsf {::}}~{\mathit {fv}}(()~{\rightarrow }{{e}}_1))~=~id\\ ~{\mathsf {then}}~{{e}}_1\\ ~{\mathsf {else}}~{{e}}_{2,alt}^{\prime }\end{array}\right) \end{equation*}
\begin{equation*} {{e}}_{2,alt}^{\prime \prime }~=~\left(\begin{array}{l}~{\mathsf {if}}~{\mathsf {let~}}(c~{\mathsf {::}}~x~{\mathsf {::}}~{\mathit {fv}}(x~{\rightarrow }{{e}}_2^{\prime }))~=~id\\ ~{\mathsf {then}}~{\mathsf {assert}}(\mathsf {this}.{\mathsf {state}}~{\text{==}}~c~{{\&\&}}~\mathsf {this}.{\mathsf {sender}}~{\text{==}}~\mathsf {this}.{\mathsf {who}});\\ ~~~~~~~~~\mathsf {this}.{\mathsf {state}}~{\mathsf {:=}}~0;~{{e}}_2^{\prime }\\ ~{\mathsf {else}}~{{e}}_{2,alt}^{\prime }\end{array}\right) \end{equation*}
Let \({{p}};{{q}}\) be the trace and state produced by initializing \({{d}};{{b}}\) with \(A\), and \({{p}};{{q}}^{\prime }\) for initializing \({{d}};{{b}}^{\prime }\), and \({{p}};{{q}}^{\prime \prime }\) for initializing \({{d}};{{b}}^{\prime \prime }\).
\begin{equation*} init_A({{d}};{{b}})~~~=~{{p}};{{q}} \end{equation*}
\begin{equation*} init_A({{d}};{{b}}^{\prime })~~=~{{p}};{{q}}^{\prime } \end{equation*}
\begin{equation*} init_A({{d}};{{b}}^{\prime \prime })~=~{{p}};{{q}}^{\prime \prime } \end{equation*}
According to \(\approx\), we only consider terms that reduce to a value. Therefore, let \(\phi _0\) be the judgment that the term \({{e}}_0\) closed by \([x{⟾ }v]\) in trace \({{p}}\) produces a value \(v_0\) and trace \(p_1\).
\begin{equation*} \phi _0(q_\phi)~=~({{p}};q_\phi ;~[x{⟾ }v]~{{e}}_0~~{\rightarrow }~{{p}}~p_1;q_\phi ;~v_0) \end{equation*}
We define \(\phi _1\) based on \(\phi\):
\begin{equation*} ~~\phi \end{equation*}
\begin{equation*} = \end{equation*}
\begin{equation*} ~~\big \lbrace ~{{d}};{{b}}^{\prime \prime };~{{\mathsf {trmp}}}({{e}}^{\prime })~\big \rbrace ~=~\big \lbrace ~comp({{d}};{{b}};~{{\mathsf {trmp}}}({{e}}))~\big \rbrace \end{equation*}
\begin{equation*} ~{\rightarrow }~generalize~[x{⟾ }v]~init_A(...) \end{equation*}
\begin{equation*} ~~\big \lbrace ~[x{⟾ }v]~init_A({{d}};{{b}}^{\prime \prime };~{{\mathsf {trmp}}}({{e}}^{\prime }))~\big \rbrace ~=~\big \lbrace ~[x{⟾ }v]~init_A(comp({{d}};{{b}};~{{\mathsf {trmp}}}({{e}})))~\big \rbrace \end{equation*}
\begin{equation*} ~{\rightarrow }~(=~~{\rightarrow }~\approx) \end{equation*}
\begin{equation*} ~~\big \lbrace ~[x{⟾ }v]~init_A({{d}};{{b}}^{\prime \prime };~{{\mathsf {trmp}}}({{e}}^{\prime }))~\big \rbrace ~\approx ~\big \lbrace ~[x{⟾ }v]~init_A(comp({{d}};{{b}};~{{\mathsf {trmp}}}({{e}})))~\big \rbrace \end{equation*}
\begin{equation*} ~{\rightarrow }~IH \end{equation*}
\begin{equation*} ~~\big \lbrace ~[x{⟾ }v]~init_A({{d}};{{b}}^{\prime \prime };~{{\mathsf {trmp}}}({{e}}^{\prime }))~\big \rbrace ~\approx ~\big \lbrace ~init_A({{d}};{{b}};~{{\mathsf {trmp}}}([x{⟾ }v]~{{e}}))~\big \rbrace \end{equation*}
\begin{equation*} ~{\rightarrow }~\text{def.~}init_A \end{equation*}
\begin{equation*} ~~\big \lbrace ~{{p}};{{q}}^{\prime \prime };~{{\mathsf {trmp}}}([x{⟾ }v]~{{e}}^{\prime })~\big \rbrace ~\approx ~\big \lbrace ~{{p}};{{q}};~{{\mathsf {trmp}}}([x{⟾ }v]~{{e}})~\big \rbrace \end{equation*}
\begin{equation*} \equiv \end{equation*}
\begin{equation*} ~~\phi _1. \end{equation*}
The lemma holds by the following chain of transitive relations. We evaluate the compiled program from top to bottom (\(~{\rightarrow }^*\)) and the original program from bottom to top (\(~{\leftarrow }^*\)) until configurations converge.
Case. \(~~~{{e}}~=~x_0\).
Let \({{p}};{{q}}\) be the trace and state produced by initializing \({{d}};{{b}}\) with \(A\).
\begin{equation*} ~init_A({{d}};{{b}})~=~{{p}};{{q}} \end{equation*}
The traceset equality holds by definition of \(comp\) and \(init_A\).
| \({\left\lbrace \begin{array}{l}[x{⟾ }v]~init_A(comp({{d}};{{b}};~{{\mathsf {trmp}}}({{e}}))) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} [x|=\gt v] init_A(comp(d;b; tramp(e))) \end{array}\right\rbrace }\right\rbrace \qquad \qquad \qquad \qquad \qquad\) | |
| \(\qquad \qquad \qquad \qquad \qquad \overset{\text{def.~}{{e}}}{=}\) | \({\left\lbrace \begin{array}{l}[x{⟾ }v]~init_A(comp({{d}};{{b}};~{{\mathsf {trmp}}}(x_0))) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} [x|=\gt v] init_A(comp(d;b; tramp(x0))) \end{array}\right\rbrace }\right\rbrace \qquad \qquad \qquad \qquad \qquad\) |
| \(\qquad \qquad \qquad \qquad \qquad \overset{\text{def.~}comp}{=}\) | \({\left\lbrace \begin{array}{l}[x{⟾ }v]~init_A({{d}};{{b}};~comp({{\mathsf {trmp}}}(x_0))) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} [x|=\gt v] init_A(d;b; comp(tramp(x0))) \end{array}\right\rbrace }\right\rbrace \qquad \qquad \qquad \qquad \qquad\) |
| \(\qquad \qquad \qquad \qquad \qquad \overset{\text{def.~}init_A}{=}\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~[x{⟾ }v]~{{\mathsf {trmp}}}(x_0) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; [x|=\gt v] tramp(x0) \end{array}\right\rbrace }\right\rbrace \qquad \qquad \qquad \qquad \qquad\) |
| \(\qquad \qquad \qquad \qquad \qquad \overset{\text{def.~}{⟾ }}{=}\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~{{\mathsf {trmp}}}([x{⟾ }v]~x_0) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; tramp([x|=\gt v] x0) \end{array}\right\rbrace }\right\rbrace \qquad \qquad \qquad \qquad \qquad\) |
| \(\qquad \qquad \qquad \qquad \qquad \overset{\text{def.~}{{e}}}{=}\) | \({\left\lbrace \begin{array}{l}{{p}};{{q}};~{{\mathsf {trmp}}}([x{⟾ }v]~{{e}}) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} p;q; tramp([x|=\gt v] e) \end{array}\right\rbrace }\right\rbrace \qquad \qquad \qquad \qquad \qquad\) |
| \(\qquad \qquad \qquad \qquad \qquad \overset{\text{def.~}init_A}{=}\) | \({\left\lbrace \begin{array}{l}init_A({{d}};{{b}};~{{\mathsf {trmp}}}([x{⟾ }v]~{{e}})) \end{array}\right.}\) | \(\hspace{-15.0pt}\left.\vphantom{\left\lbrace \begin{array}{l} init_A(d;b; tramp([x|=\gt v] e)) \end{array}\right\rbrace }\right\rbrace \qquad \qquad \qquad \qquad \qquad □\) |
\(comp^{\prime }\) is defined on programs. To evaluate a program, it is initialized with a set of clients \(A\). \(comp^{\prime }\) preserves the traceset of (closed) programs \(P\) for any set of clients \(A\).
For all definitions \({{b}}\), definitions \({{d}}\), terms \({{e}}_0\),
\begin{equation*} \lbrace ~init_A(comp^{\prime }({{d}};{{b}};~{{\mathsf {trmp}}}({{e}}_0)))~\rbrace ~\approx ~ \cdots ~\approx ~ \lbrace ~init_A({{d}};{{b}}^{\prime };~{{\mathsf {trmp}}}({{e}}_0))~\rbrace . \end{equation*}
By induction over term structure. Case. \(~~P~=~({{d}};{{b}};~{{e}}_0)\).
Intuitively, \(comp^{\prime }\) prepends the definitions \({{b}}\) with initial definitions for \({\mathsf {clfn}}\) and \({\mathsf {cofn}}\) that only contain \({\mathsf {assert}}({\mathsf {false}})\), such that \(comp\) can be applied.
\begin{equation*} {{b}}^{\prime }~=~\left(\begin{array}{l}~{\mathsf {@cl}}~\mathsf {this}.{\mathsf {clfn}}~=~id~{\rightarrow }~{\mathsf {assert}}({\mathsf {false}});\\ ~{\mathsf {@co}}~\mathsf {this}.{\mathsf {cofn}}~=~id~{\rightarrow }~{\mathsf {assert}}({\mathsf {false}});\\ ~{{b}}\end{array}\right) \end{equation*}
The lemma holds by definition of \(comp^{\prime }\) and Lemma 4.
| \({\left\lbrace \begin{array}{l}init_A(comp^{\prime }({{d}};{{b}};~{{\mathsf {trmp}}}({{e}}_0))) \end{array}\right.}\) | \(\left.\vphantom{\left\lbrace \begin{array}{l} init_A(comp^{\prime }(d;b; tramp(e0))) \end{array}\right\rbrace }\right\rbrace \qquad \qquad \qquad \qquad \qquad \qquad\) | |
| \(\qquad \qquad \qquad \qquad \qquad \qquad \overset{\text{def.~}comp^{\prime }}{=}\) | \({\left\lbrace \begin{array}{l}init_A(comp({{d}};{{b}}^{\prime };~{{\mathsf {trmp}}}({{e}}_0)) \end{array}\right.}\) | \(\left.\vphantom{\left\lbrace \begin{array}{l} init_A(comp(d;b^{\prime }; tramp(e0)) \end{array}\right\rbrace }\right\rbrace \qquad \qquad \qquad \qquad \qquad \qquad\) |
| \(\qquad \qquad \qquad \qquad \qquad \qquad \overset{\text{Lemma~}4}{\approx }\) | \({\left\lbrace \begin{array}{l}init_A({{d}};{{b}}^{\prime };~{{\mathsf {trmp}}}({{e}}_0)) \end{array}\right.}\) | \(\left.\vphantom{\left\lbrace \begin{array}{l} init_A(d;b^{\prime }; tramp(e0)) \end{array}\right\rbrace }\right\rbrace \qquad \qquad \qquad \qquad \qquad \quad □\) |
Acknowledgment
Thanks to George Zakhour for feedback on the initial draft.
References
[1]
Gavin Wood. 2022. Ethereum Yellow Paper. Retrieved from https://ethereum.github.io/yellowpaper/paper.pdf
[2]
Simon Marlow. 2010. Haskell 2010: Language Report. Expressions. Do Expressions. Retrieved 14-11-2020 from https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-470003.14
[3]
Evan Saulpaugh. 2018. Headlong (GitHub Repository). Retrieved from https://github.com/esaulpaugh/headlong
[4]
Ethereum Foundation. 2015. Solidity Documentation. Retrieved 14-11-2020 from https://docs.soliditylang.org/en/v0.8.1/
[5]
Edwin Brady. 2007. The Idris Tutorial. Interfaces. Monads and do-notation. !-notation. Retrieved 14-11-2020 from http://docs.idris-lang.org/en/latest/tutorial/interfaces.html#notation
[6]
Web3 Labs. 2016. Web3j: Web3 Java Ethereum Ðapp API (GitHub Repository). Retrieved from https://github.com/web3j/web3j
[7]
Scala Development Team. 2013. Scala-continuations. The scala delimited continuations plugin and library. Retrieved from https://github.com/scala/scala-continuations
[8]
Aleksandar Prokopec. 2015. Scala coroutines. Retrieved from https://github.com/storm-enroute/coroutines
[9]
Phil Daian. 2016. Analysis of the DAO exploit. Retrieved 14-11-2020 from https://hackingdistributed.com/2016/06/18/analysis-of-the-dao-exploit/
[10]
Jon Purdy. 2017. Discussion on GHC Pre-Proposal: Add InlineBindings proposal. Retrieved 14-11-2020 from https://github.com/ghc-proposals/ghc-proposals/pull/64
[11]
Leo White. 2018. OCaml: Add “monadic” let operators. Retrieved from https://github.com/ocaml/ocaml/pull/1947
[12]
PolyCrypt GmbH. 2020. Perun Network. Retrieved from https://perun.network
[13]
Ethereum Foundation. 2015. Solidity Documentation - Common Patterns. Retrieved 14-11-2020 from https://docs.soliditylang.org/en/v0.7.4/common-patterns.html
[14]
State Channels contributors. 2020. State Channels. Retrieved from https://statechannels.org/
[15]
Google Inc. 2021. Google Cloud BigQuery: Contract deployment per month. Retrieved from https://console.cloud.google.com/bigquery
[16]
Google Inc. 2021. Google Cloud BigQuery: Contract size. Retrieved from https://console.cloud.google.com/bigquery
[17]
Uniswap Labs. 2021. Uniswap Info. Retrieved 07-07-2021 from https://v2.info.uniswap.org/home
[18]
Martín Abadi, Mihai Budiu, Úlfar Erlingsson, and Jay Ligatti. 2009. Control-flow integrity principles, implementations, and applications. ACM Trans. Inf. Syst. Secur. 13, 1 (2009), 4:1–4:40. DOI:DOI:
[19]
Gul Agha. 1986. Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge, MA.
[20]
Marcin Andrychowicz, Stefan Dziembowski, Daniel Malinowski, and Lukasz Mazurek. 2014. Secure multiparty computations on Bitcoin. In IEEE Symposium on Security and Privacy. IEEE Computer Society, 443–458. DOI:DOI:
[21]
Monika Di Angelo and Gernot Salzer. 2019. A survey of tools for analyzing Ethereum smart contracts. In IEEE International Conference on Decentralized Applications and Infrastructures. IEEE, 69–78. DOI:DOI:
[22]
Monika Di Angelo and Gernot Salzer. 2020. Wallet contracts on Ethereum. CoRR abs/2001.06909 (2020).
[23]
Andrew W. Appel. 1992. Compiling with Continuations. Cambridge University Press.
[24]
Massimo Bartoletti and Livio Pompianu. 2017. An empirical analysis of smart contracts: Platforms, applications, and design patterns. In International Conference on Financial Cryptography and Data Security. Springer, 494–509.
[25]
Gavin M. Bierman, Claudio V. Russo, Geoffrey Mainland, Erik Meijer, and Mads Torgersen. 2012. Pause ‘n’ play: Formalizing asynchronous C#. In 26th European Conference on Object-Oriented Programming(Lecture Notes in Computer Science, Vol. 7313), James Noble (Ed.). Springer, 233–257. DOI:DOI:
[26]
Sam Blackshear, Evan Cheng, D. Dill, Victor Gao, B. Maurer, T. Nowacki, Alistair Pott, S. Qadeer, Dario Russi, Stephane Sezer, Tim Zakian, and Run tian Zhou. 2019. Move: A language with programmable resources. https://developers.diem.com/papers/diem-move-a-language-with-programmable-resources/2019-06-18.pdf
[27]
Flavio W. Brasil and Sameer Brenn. 2017. Monadless - Syntactic Sugar for Monad Composition in Scala. Retrieved from https://github.com/monadless/monadless
[28]
Lorenz Breidenbach, Phil Daian, Ari Juels, and Emin Gün Sirer. 2016. An In-depth Look at the Parity Multisig Bug. Retrieved from hackingdistributed.com/2017/07/22/deep-dive-parity-bug/
[29]
Lars Brünjes and Murdoch James Gabbay. 2020. UTxO- vs account-based smart contract blockchain programming paradigms. In 9th International Symposium on Leveraging Applications of Formal Methods: Verification and Validation: Applications(Lecture Notes in Computer Science, Vol. 12478), Tiziana Margaria and Bernhard Steffen (Eds.). Springer, 73–88. DOI:DOI:
[30]
Manuel Chakravarty, Roman Kireev, Kenneth MacKenzie, Vanessa McHale, Jann Müller, Alexander Nemish, Chad Nester, Michael Peyton Jones, Simon Thompson, Rebecca Valentine, and Philip Wadler. 2019. Functional Blockchain Contracts. Retrieved from https://iohk.io/en/research/library/papers/functional-blockchain-contracts/
[31]
Manuel M. T. Chakravarty, Sandro Coretti, Matthias Fitzi, Peter Gazi, Philipp Kant, Aggelos Kiayias, and Alexander Russell. 2020. Hydra: Fast isomorphic state channels. IACR Cryptol. ePrint Arch. 2020 (2020), 299. Retrieved from https://eprint.iacr.org/2020/299
[32]
Kwanghoon Choi and Byeong-Mo Chang. 2019. A theory of RPC calculi for client–server model. J. Function. Program. 29 (2019). DOI:DOI:
[33]
Stephen Chong, Jed Liu, Andrew C. Myers, Xin Qi, K. Vikram, Lantian Zheng, and Xin Zheng. 2007. Secure web applications via automatic partitioning. In Symposium on Operating Systems Principles.
[34]
Michael J. Coblenz. 2017. Obsidian: A safer blockchain programming language. In 39th International Conference on Software Engineering, Sebastián Uchitel, Alessandro Orso, and Martin P. Robillard (Eds.). IEEE Computer Society, 97–99. DOI:DOI:
[35]
Michael J. Coblenz, Gauri Kambhatla, Paulette Koronkevich, Jenna L. Wise, Celeste Barnaby, Jonathan Aldrich, Joshua Sunshine, and Brad A. Myers. 2019. User-centered programming language design in the obsidian smart contract language. CoRR abs/1912.04719 (2019).
[36]
Michael J. Coblenz, Reed Oei, Tyler Etzel, Paulette Koronkevich, Miles Baker, Yannick Bloem, Brad A. Myers, Joshua Sunshine, and Jonathan Aldrich. 2019. Obsidian: Typestate and assets for safer blockchain programming. CoRR abs/1909.03523 (2019).
[37]
Youyou Cong, Leo Osvald, Grégory M. Essertel, and Tiark Rompf. 2019. Compiling with continuations, or without? Whatever. Proc. ACM Program. Lang. 3, ICFP (2019), 79:1–79:28. DOI:DOI:
[38]
Ezra Cooper, Sam Lindley, Philip Wadler, and Jeremy Yallop. 2007. Links: Web programming without tiers. In 5th International Conference on Formal Methods for Components and Objects (FMCO’06). Springer-Verlag, Berlin, 266–296. Retrieved from http://dl.acm.org/citation.cfm?id=1777707.1777724
[39]
Dapp.com. 2020. 2020 Q2 Dapp Market Report. Retrieved from https://www.dapp.com/article/q2-2020-dapp-market-report
[40]
Ankush Das, S. Balzer, J. Hoffmann, and F. Pfenning. 2019. Resource-aware session types for digital contracts. ArXiv abs/1902.06056 (2019).
[41]
Ankush Das, Jan Hoffmann, and Frank Pfenning. 2021. Nomos: A protocol-enforcing, asset-tracking, and gas-aware language for smart contracts. https://www.cs.cmu.edu/janh/assets/pdf/DasHP21.pdf
[42]
Mariangiola Dezani-Ciancaglini and Ugo de’Liguoro. 2009. Sessions and session types: An overview. In 6th International Workshop on Web Services and Formal Methods(Lecture Notes in Computer Science, Vol. 6194), Cosimo Laneve and Jianwen Su (Eds.). Springer, 1–28. DOI:DOI:
[43]
Thomas Durieux, João F. Ferreira, Rui Abreu, and Pedro Cruz. 2020. Empirical review of automated analysis tools on 47,587 Ethereum smart contracts. In 42nd International Conference on Software Engineering, Gregg Rothermel and Doo-Hwan Bae (Eds.). ACM, 530–541. DOI:DOI:
[44]
Stefan Dziembowski, Lisa Eckey, Sebastian Faust, Julia Hesse, and Kristina Hostáková. 2019. Multi-party virtual state channels. In 38th Annual International Conference on the Theory and Applications of Cryptographic Techniques: Advances in Cryptology(Lecture Notes in Computer Science, Vol. 11476), Yuval Ishai and Vincent Rijmen (Eds.). Springer, 625–656. DOI:DOI:
[45]
Stefan Dziembowski, Sebastian Faust, and Kristina Hostáková. 2018. General state channel networks. In ACM SIGSAC Conference on Computer and Communications Security, David Lie, Mohammad Mannan, Michael Backes, and XiaoFeng Wang (Eds.). ACM, 949–966. DOI:DOI:
[46]
Jonathan Edwards. 2009. Coherent reaction. In 24th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, Shail Arora and Gary T. Leavens (Eds.). ACM, 925–932. DOI:DOI:
[47]
Matthias Felleisen and Robert Hieb. 1992. The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci. 103, 2 (1992), 235–271. DOI:DOI:
[48]
João F. Ferreira, Pedro Cruz, Thomas Durieux, and Rui Abreu. 2020. SmartBugs: A framework to analyze solidity smart contracts. CoRR abs/2007.04771 (2020).
[49]
Klint Finley. 2016. A $50 million hack just showed that the DAO was all too human. Wired (62016).
[50]
Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. 1993. The essence of compiling with continuations. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’93), Robert Cartwright (Ed.). ACM, 237–247. DOI:DOI:
[51]
Simon Fowler, Sam Lindley, J. Garrett Morris, and Sára Decova. 2019. Exceptional asynchronous session types: Session types without tiers. Proc. ACM Program. Lang. 3, POPL, Article 28 (Jan.2019), 29 pages. DOI:DOI:
[52]
Murdoch James Gabbay. 2020. What is an EUTxO blockchain? CoRR abs/2007.12404 (2020).
[53]
Saverio Giallorenzo, Fabrizio Montesi, and Marco Peressotti. 2020. Choreographies as Objects. arxiv:2005.09520
[54]
Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti, David Richter, Guido Salvaneschi, and Pascal Weisenburger. 2021. Multiparty languages: The choreographic and multitier cases (pearl). In 35th European Conference on Object-Oriented Programming(LIPIcs, Vol. 194), Anders Møller and Manu Sridharan (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 22:1–22:27. DOI:DOI:
[55]
Dominik Harz and William J. Knottenbelt. 2018. Towards safer smart contracts: A survey of languages and verification methods. CoRR abs/1809.09805 (2018).
[56]
C. A. R. Hoare. 1978. Communicating sequential processes. Commun. ACM 21, 8 (Aug.1978), 666–677. DOI:DOI:
[57]
Kohei Honda, Aybek Mukhamedov, Gary Brown, Tzu-Chun Chen, and Nobuko Yoshida. 2011. Scribbling interactions with a formal foundation. In 7th International Conference on Distributed Computing and Internet Technology(Lecture Notes in Computer Science, Vol. 6536), Raja Natarajan and Adegboyega K. Ojo (Eds.). Springer, 55–75. DOI:DOI:
[58]
Bin Hu, Zongyang Zhang, Jianwei Liu, Yizhong Liu, Jiayuan Yin, Rongxing Lu, and Xiaodong Lin. 2020. A comprehensive survey on smart contract construction and execution: Paradigms, tools and systems. CoRR abs/2008.13413 (2020).
[59]
Andrew Kennedy. 2007. Compiling with continuations, continued. In 12th ACM SIGPLAN International Conference on Functional Programming, Ralf Hinze and Norman Ramsey (Eds.). ACM, 177–190. DOI:DOI:
[60]
Zhengqin Luo and Tamara Rezk. 2012. Mashic compiler: Mashup sandboxing based on inter-frame communication. In 25th IEEE Computer Security Foundations Symposium, Stephen Chong (Ed.). IEEE Computer Society, 157–170. DOI:DOI:
[61]
Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. 2016. Making smart contracts smarter. In ACM SIGSAC Conference on Computer and Communications Security (CCS’16). Association for Computing Machinery, New York, NY, 254–269. DOI:DOI:
[62]
Luke Maurer, Paul Downen, Zena M. Ariola, and Simon L. Peyton Jones. 2017. Compiling without continuations. In 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, Albert Cohen and Martin T. Vechev (Eds.). ACM, 482–494. DOI:DOI:
[63]
Anastasia Mavridou and Aron Laszka. 2018. Designing secure Ethereum smart contracts: A finite state machine based approach. In 22nd International Conference on Financial Cryptography and Data Security(Lecture Notes in Computer Science, Vol. 10957), Sarah Meiklejohn and Kazue Sako (Eds.). Springer, 523–540. DOI:DOI:
[64]
Anastasia Mavridou, Aron Laszka, Emmanouela Stachtiari, and Abhishek Dubey. 2019. VeriSolid: Correct-by-design smart contracts for Ethereum. In 23rd International Conference on Financial Cryptography and Data Security(Lecture Notes in Computer Science, Vol. 11598), Ian Goldberg and Tyler Moore (Eds.). Springer, 446–465. DOI:DOI:
[65]
Andrew Miller, Iddo Bentov, Surya Bakshi, Ranjit Kumaresan, and Patrick McCorry. 2019. Sprites and state channels: Payment networks that go faster than lightning. In 23rd International Conference on Financial Cryptography and Data Security(Lecture Notes in Computer Science, Vol. 11598), Ian Goldberg and Tyler Moore (Eds.). Springer, 508–526. DOI:DOI:
[66]
Mix. 2019. These Are the Top 10 Programming Languages in Blockchain. Retrieved from https://thenextweb.com/hardfork/2019/05/24/javascript-programming-java-cryptocurrency/
[67]
Fabrizio Montesi, Claudio Guidi, and Gianluigi Zavattaro. 2014. Service-oriented programming with Jolie. In Web Services Foundations, Athman Bouguettaya, Quan Z. Sheng, and Florian Daniel (Eds.). Springer, 81–107. DOI:DOI:
[68]
Ivica Nikolić, Aashish Kolluri, Ilya Sergey, Prateek Saxena, and Aquinas Hobor. 2018. Finding the greedy, prodigal, and suicidal contracts at scale. In 34th Annual Computer Security Applications Conference (ACSAC’18). Association for Computing Machinery, New York, NY, 653–663. DOI:DOI:
[69]
Reed Oei, Michael J. Coblenz, and Jonathan Aldrich. 2020. Psamathe: A DSL with flows for safe blockchain assets. CoRR abs/2010.04800 (2020).
[70]
Gustavo A. Oliva, Ahmed E. Hassan, and Zhen Ming Jack Jiang. 2020. An exploratory study of smart contracts in the Ethereum blockchain platform. Empir. Softw. Eng. 25, 3 (2020), 1864–1904. DOI:
[71]
Marco Patrignani, Amal Ahmed, and Dave Clarke. 2019. Formal approaches to secure compilation: A survey of fully abstract compilation and related work. ACM Comput. Surv. 51, 6 (2019), 125:1–125:36. DOI:DOI:
[72]
Tomas Petricek and Don Syme. 2014. The F# computation expression zoo. In International Symposium on Practical Aspects of Declarative Languages(Lecture Notes in Computer Science, Vol. 8324). Springer, 33–48.
[73]
Sergey Petrov. 2017. Another Parity Wallet Hack Explained. Retrieved from https://medium.com/@Pr0Ger/another-parity-wallet-hack-explained-847ca46a2e1c
[74]
Andrew M. Pitts. 2000. Operational semantics and program equivalence. In Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9–15, 2000, Advanced Lectures(Lecture Notes in Computer Science, Vol. 2395), Gilles Barthe, Peter Dybjer, Luís Pinto, and João Saraiva (Eds.). Springer, 378–412. DOI:DOI:
[75]
Christian Queinnec. 2000. The influence of browsers on evaluators or, continuations to program web servers. In 5th ACM SIGPLAN International Conference on Functional Programming (ICFP’00), Martin Odersky and Philip Wadler (Eds.). ACM, 23–33. DOI:DOI:
[76]
Gabriel Radanne, Jérôme Vouillon, and Vincent Balat. 2016. Eliom: A core ML language for tierless web programming. In 14th Asian Symposium on Programming Languages and Systems (APLAS’16), Atsushi Igarashi (Ed.). Springer-Verlag, Berlin, 377–397. DOI:DOI:
[77]
John C. Reynolds. 1972. Definitional interpreters for higher-order programming languages. In ACM Annual Conference (ACM’72).
[78]
David Richter, David Kretzler, Pascal Weisenburger, Guido Salvaneschi, Sebastian Faust, and Mira Mezini. 2022. Prisma: A tierless language for enforcing contract-client protocols in decentralized applications. In 36th European Conference on Object-Oriented Programming (ECOOP’22)(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 222), Karim Ali and Jan Vitek (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 35:1–35:4. DOI:DOI:
[79]
David Richter, David Kretzler, Pascal Weisenburger, Guido Salvaneschi, Sebastian Faust, and Mira Mezini. 2022. Prisma: A tierless language for enforcing contract-client protocols in decentralized applications (artifact). Dagstuhl Artifacts Ser. 8, 2 (2022), 16:1–16:3. DOI:DOI:
[80]
Scala Development Team. 2012. Scala-async. A Scala DSL to enable a direct style of coding when composing futures. https://github.com/scala/scala-async
[81]
Franklin Schrans, Susan Eisenbach, and Sophia Drossopoulou. 2018. Writing safe smart contracts in Flint. In 2nd International Conference on Art, Science, and Engineering of Programming, Stefan Marr and Jennifer B. Sartor (Eds.). ACM, 218–219. DOI:DOI:
[82]
Franklin Schrans, Daniel Hails, Alexander Harkness, Sophia Drossopoulou, and Susan Eisenbach. 2019. Flint for safer smart contracts. CoRR abs/1904.06534 (2019).
[83]
Pablo Lamela Seijas, Alexander Nemish, David Smith, and Simon Thompson. 2020. Marlowe: Implementing and analysing financial contracts on blockchain. In Workshop on Trusted Smart Contracts @ FC 2020, Tiziana Margaria and Bernhard Steffen (Eds.) Retrieved from https://iohk.io/en/research/library/papers/marloweimplementing-and-analysing-financial-contracts-on-blockchain/
[84]
Pablo Lamela Seijas and Simon J. Thompson. 2018. Marlowe: Financial contracts on blockchain. In 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Industrial Practice(Lecture Notes in Computer Science, Vol. 11247), Tiziana Margaria and Bernhard Steffen (Eds.). Springer, 356–375. DOI:DOI:
[85]
Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar, Anton Trunov, and Ken Chan Guan Hao. 2019. Safer smart contract programming with Scilla. PACMPL 3, OOPSLA (2019), 185:1–185:30. DOI:DOI:
[86]
Manuel Serrano, Erick Gallesio, and Florian Loitsch. 2006. Hop, a language for programming the Web 2.0. In 21st ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’06). ACM, New York, NY.
[87]
Manuel Serrano and Vincent Prunet. 2016. A glimpse of Hopjs. In 21st ACM SIGPLAN International Conference on Functional Programming (ICFP’16). ACM, New York, NY, 180–192. DOI:DOI:
[88]
Ruslan Shevchenko. 2020. dotty-cps-async. Retrieved from https://github.com/rssh/dotty-cps-async
[89]
Dmitrii Suvorov and Vladimir Ulyantsev. 2019. Smart contract design meets state machine synthesis: Case studies. CoRR abs/1906.02906 (2019).
[90]
Philip Wadler. 2012. Propositions as sessions. In ACM SIGPLAN International Conference on Functional Programming, Peter Thiemann and Robby Bruce Findler (Eds.). ACM, 273–286. DOI:DOI:
[91]
Pascal Weisenburger, Mirko Köhler, and Guido Salvaneschi. 2018. Distributed system development with ScalaLoci. Proc. ACM Program. Lang. 2, OOPSLA, Article 129 (Oct.2018), 30 pages. DOI:DOI:
[92]
Maximilian Wöhrer and Uwe Zdun. 2020. From domain-specific language to code: Smart contracts and the application of design patterns. IEEE Softw. 37, 4 (2020), 37–42. DOI:DOI:
[93]
Gavin Wood. 2014. Ethereum: A Secure Decentralised Generalised Transaction Ledger. Retrieved from https://ethereum.github.io/yellowpaper/paper.pdf
[94]
Bo Yang. 2016. Dsl.scala - A Framework to Create Embedded Domain-specific Languages in Scala. Retrieved from https://github.com/ThoughtWorksInc/Dsl.scala
Index Terms
- Prisma : A Tierless Language for Enforcing Contract-client Protocols in Decentralized Applications
Recommendations
Albert, An Intermediate Smart-Contract Language for the Tezos Blockchain
Financial Cryptography and Data SecurityAbstractTezos is a smart-contract blockchain. Tezos smart contracts are written in a low-level stack-based language called Michelson. In this article we present Albert, an intermediate language for Tezos smart contracts which abstracts Michelson stacks as ...
Type-directed language extension for effectful computations
SCALA '14: Proceedings of the Fifth Annual Scala WorkshopComputation types such as functors, applicative functors and monads have become common abstractions for modeling effectful computations in functional programming languages. They are often used together with special language extensions intended to ...
Designing language-oriented programming languages
OOPSLA '10: Proceedings of the ACM international conference companion on Object oriented programming systems languages and applications companionToday, language-oriented programming (LOP) is realized by using either language workbenches or internal DSLs, each with their own advantages and disadvantages. In this work, we design a host language for DSLs with language workbench features, thereby ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
September 2023
284 pages
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 23 September 2023
Online AM: 18 July 2023
Accepted: 10 May 2023
Revised: 06 February 2023
Received: 24 June 2022
Published in TOPLAS Volume 45, Issue 3
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
- German Federal Ministry of Education and Research BMBF iBlockchain
- German Research Foundation DFG
- Hessian Ministry of Higher Education, Research, Science and the Arts
- National Research Center for Applied Cybersecurity ATHENE
- Hessian LOEWE initiative LOEWE
- Swiss National Science Foundation SNSF
- University of St. Gallen unisig
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 1,031Total Downloads
- Downloads (Last 12 months)762
- Downloads (Last 6 weeks)53
Reflects downloads up to 13 Dec 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in