Secure compilation of rich smart contracts on poor UTXO blockchains

BY KEYHUNTER 05.03.2025
Secure compilation of rich smart contracts on poor UTXO blockchains

Most blockchain platforms from Ethereum onwards render smart contracts as stateful reactive objects that update their state and transfer crypto-assets in response to transactions. A drawback of this design is that when users submit a transaction, they cannot predict in which state it will be executed. This exposes them to transaction-ordering attacks, a widespread class of attacks where adversaries with the power to construct blocks of transactions can extract value from smart contracts (the so-called MEV attacks). The UTXO model is an alternative blockchain design that thwarts these attacks by requiring new transactions to spend past ones: since transactions have unique identifiers, reordering attacks are ineffective. Currently, the blockchains following the UTXO model either provide contracts with limited expressiveness (Bitcoin), or require complex run-time environments (Cardano). We present ILLUML, an Intermediate-Level Language for the UTXO Model. ILLUML can express real-world smart contracts, e.g. those found in Decentralized Finance. We define a compiler from ILLUML to a bare-bone UTXO blockchain with loop-free scripts. Our compilation target only requires minimal extensions to Bitcoin Script: in particular, we exploit covenants, a mechanism for preserving scripts along chains of transactions. We prove the security of our compiler: namely, any attack targeting the compiled contract is also observable at the ILLUML level. Hence, the compiler does not introduce new vulnerabilities that were not already present in the source ILLUML contract. We evaluate the practicality of ILLUML as a compilation target for higher-level languages. To this purpose, we implement a compiler from a contract language inspired by Solidity to ILLUML, and we apply it to a benchmark or real-world smart contracts.

Index Terms—Blockchain, smart contracts, UTXO model

  1. Introduction

Smart contracts are agreements between mutually untrusted parties that are enforceable by a computer program, without the need of a trusted intermediary. Currently, most implementations of smart contracts are based on permissionless blockchains, where the conjunction with crypto-assets has given rise to new applications, like decentralized finance (DeFi) [1] and decentralized autonomous organizations (DAOs) [2], that overall control nearly 90 billion dollars worth of assets today [3].

Two main smart contracts models have emerged so far. In the account-based model, contracts are reactive objects that live on the blockchain and process user transactions by updating their state and transferring crypto-assets among users [4]. In the UTXO model, instead, contracts, their state, and the ownership of assets are encoded within transactions: when a new transaction is published in the blockchain, it replaces (“spends”) an old transaction, effectively updating the contract state and the assets ownership. The UTXO model was first proposed by Bitcoin, where the idea of blockchain-based contracts originated in 2012. The account-based model was later introduced in 2015 by Ethereum, where contracts were popularized. Most blockchain platforms today follow the account-based model: besides Ethereum, also other mainstream blockchains such as Solana, Avalanche, Hedera, Algorand and Tezos are account-based (albeit with differences, sometimes notable, from case to case).

Account-based vs. UTXO blockchains. In the account-based model, contracts can be seen as objects with a state accessible and modifiable by methods, as in object-oriented programming. For instance, to withdraw 10 token units from a Bank contract, a user A sends a transaction $\text{withdraw}(10)$ to Bank, which will react by updating its state and A’s wallet. Programming contracts in the UTXO model requires instead a paradigm shift from the common object-oriented style [5]. Indeed, a UTXO transaction does not directly represent a contract action: rather, it encodes a transfer of crypto-assets from its inputs to its outputs. Transaction outputs specify the assets they control, the contract state, and the conditions under which the assets can be transferred again. Transaction inputs are references to unspent outputs of previous transactions, and provide the values that make their spending conditions true. The blockchain state is given by the set of Unspent Transaction Outputs (UTXO). A transaction can spend one or more of outputs in the UTXO set, specifying them as its inputs: this effectively removes these outputs from the blockchain state, and creates new ones. The new outputs update the state of the contracts, and redistribute the assets according to their spending conditions. These conditions are specified in a scripting language, the expressiveness of which is reflected on that of contracts. For instance, in the banking use case above, the state of the Bank contract could be scattered among a set of outputs. To withdraw, A must send a transaction which spends one or more of these outputs, and whose output has a spending condition that can be satisfied only by A (e.g., a signature verification against A’s public key). In addition, the Bank state in the new output must be a correct update of the old state (e.g., in the new state A’s account must have 10 tokens less than in the old state). Programming contracts in this model is more complex than in the account-based model, since the links to familiar programming abstractions are weaker.

Despite this additional complexity, the UTXO model has a series of advantages over the account-based model. A first problem of account-based stateful platforms like Ethereum is to undermine the concurrent execution of transactions. Namely, a multi-core blockchain node cannot simply execute transactions in parallel, since they may perform conflicting accesses to shared parts of the state, possibly leading to an inconsistent state [6]. In such platforms, there is no efficient way to detect when transactions can be safely parallelized: in general, determining the accessed parts of the state requires to fully execute them. In the UTXO model, instead, it is easy to detect when transactions are parallelizable: just check if they spend disjoint outputs, which can be done efficiently [7].

Another problem of the account-based model is that a user sending a transaction to the blockchain network cannot accurately predict the state in which it will be executed. This has several negative consequences, such as the unpredictability of transaction fees and the susceptibility to maximal extractable value (MEV) attacks [8]–[10]. Fees are a common incentive mechanism for the blockchain network to execute transactions and a defence against denial-of-service attacks. To be accepted, a transaction must pay a fee which is proportional to the computational resources needed to validate it. The actual amount of these resources heavily depends on the initial state where the transaction is performed: so, to be sure that their transactions are accepted, users specify a maximum fee they are willing to pay. Besides forcing users to over-approximate fees, this also opens to attacks where the adversary front-runs transactions so that they are executed in a state where the paid fee is insufficient: the consequence is that users pay the fee even for rejected transactions that do not update the contract state according to their intention. With MEV attacks instead, the adversary colludes with malicious blockchain nodes to propose blocks where the ordering of transactions is profitable for the adversary (to the detriment of users). These attacks are very common in account-based blockchains (targeting in particular DeFi contracts), and are estimated to be worth more than USD 1 billion [11] so far.

The UTXO model naturally mitigates these attacks. Indeed, when a user sends a transaction ( T ) to the blockchain network, they know exactly in which state it will be executed, since this state is completely determined by ( T )’s inputs. Therefore, if an adversary ( M ) front-runs ( T ) with their transaction ( T_M ), the transaction ( T ) will be rejected by the blockchain network, since some of its inputs are spent by ( T_M ). If the user still desires to perform the action in the new state, they must resend ( T ), updating its inputs (and therefore, specifying the new state where the action is executed). This thwarts both the fees exhaustion attacks and the MEV attacks described before.

UTXO designs: Bitcoin vs. Cardano. Currently, the two main UTXO blockchains are Bitcoin and Cardano. These platforms follow radically different design choices in the structure of transactions and in the scripting languages to specify their spending conditions. These differences deeply affect the expressiveness of their contracts and the complexity of their runtime environments. On the one hand, Bitcoin has a minimal scripting language, featuring only basic arithmetic and logical operations, conditionals, hashes, and (limited) signature verification [12]. This imposes a stringent limit on the expressiveness of contracts in Bitcoin: contracts requiring unbounded computational steps, or transfers of tokens different than native crypto-currency, cannot be expressed [13]. Neglecting the lack of expressiveness, the design choice of keeping the scripting language minimal has some positive aspects: besides limiting the attack surface and simplifying the overall design (e.g., no gas mechanism is needed), it facilitates the formal verification of contracts. On the other side of the spectrum, Cardano’s scripting language is an untyped lambda-calculus [14], which makes Cardano scripts, and in turn contracts, Turing-complete. This increase in expressiveness comes at a cost, in that the static verification of general contract properties is undecidable. Furthermore, since Cardano’s scripts feature unbounded iteration, a gas mechanism is needed to abort time-consuming computations and suitably reward blockchain nodes for validating transactions. Although the gas needed to execute a transaction is statically known (unlike in account-based blockchains, where it depends on the actual state where the transaction is executed), still it would be safer to avoid the gas mechanism altogether. For instance, a misalignment of the gas incentives led to DoS attack on Ethereum [15]. Another drawback of Bitcoin, Cardano, and UTXO blockchains in general, is that, due to the absence of explicit state, writing stateful contracts is more difficult than in account-based blockchains [5].

Our research question is whether one can find a balance between the two approaches which also overcomes their usability issues. More specifically, ours is a quest for a contract language and a UTXO model such that:

  • the expressiveness of contracts is enough for real-world use cases (contracts are Turing-complete);
  • executing contracts requires a simple blockchain design (individual transaction scripts are not Turing-complete, and no gas mechanism is required);
  • it can serve as a compilation target of developer-friendly higher-level contract languages.

Contributions. We address this research question by proposing an expressive intermediate-level contract language that compiles into transactions executable by a bare-bone UTXO blockchain (with no gas mechanism). The key insight is to scatter the execution of complex contract actions across multiple UTXO transactions. Even if each of these transactions contains only simple (loop-free) scripts, the overall chain of transactions can encompass complex (possibly recursive) behaviours.

We summarize our main contributions as follows:

  • Illum, an Intermediate Level Language for UTXO blockchains. Illum is a Turing-complete clause language with primitives to exchange crypto-assets. We evaluate Illum on a few use cases, including gambling games, auctions and Ponzi schemes (Section 2).
  • a compiler from Illum to UTXO transactions. The scripting language used in these transactions is Bitcoin Script extended with covenants, operators to constrain the output scripts of the redeeming transactions [16]. This is a lightweight mechanism, which can be implemented with minimal overhead on the runtime of UTXO blockchains [17], [18].

• a proof of the security of the ILLUM compiler. Namely, we prove that, even in the presence of adversaries, with overwhelming probability there is a step-by-step correspondence between the execution of an ILLUM contract and that of the chain of transactions resulting from its compilation. Our security result essentially establishes Robust Trace Property Preservation [19], [20], ensuring that each computational trace (involving any computational adversary) has a symbolic counterpart (involving a suitable symbolic adversary). Its proof is quite complex, as it matches every possible contract action in ILLUM (more than 20 cases) with some action at the blockchain level.

• a prototype implementation of a compiler from a Solidity-like high-level contract language to ILLUM. We illustrate our compilation technique in Section 7.

• an evaluation of the practicality of our approach, based on a benchmark of common smart contracts that we implement in the high-level language and then translate to ILLUM with our prototype compiler. Overall, our evaluation shows that it is feasible to reconcile the UTXO model with the familiar procedural programming style supported by Solidity, effectively making UTXO contracts more usable in practice.

Because of space constraints, we refer to a technical report for the proofs [21], and to a github repository¹ for the code of the prototype compiler and of the benchmark.

  1. Overview

In this section we overview our approach, discussing its main features and results. Here we will mostly focus on intuition, leveraging on examples and postponing the full technical development to later sections.

2.1. An intermediate contract language

ILLUM is a clause-based process calculus that can serve as an intermediate contract language and compiles to a bare-bone UTXO model. ILLUM contracts are sets of clauses, each having a defining equation of the form:

[ X(\text{In}; \text{Ex}) = {vT \text{ if } p}C ]

Here, ( X ) is the clause name, ( \text{In} ) and ( \text{Ex} ) are sequences of formal parameters (respectively, internal and external), ( {vT \text{ if } p} ) is the funding precondition (namely: “( v ) units of tokens ( T ) are available and the condition ( p ) is true”), and ( C ) is a process encoding the clause behaviour. We provide some intuition about these constructs with an example.

Example: a “double or nothing” game. We specify a gambling game between two players ( A ) and ( B ) as follows:

[ \begin{align*} \text{Init}(\cdot) &= {0} \text{ (call } \text{Play}_A(1); \text{ call } \text{Play}_B(1)} \ \text{Play}_A(v; \cdot) &= {vT} \text{ (call } \text{Play}_B(2v; \cdot) \ &\quad + \text{afterRel5 : send } (vT \rightarrow A)} \ \text{Play}_B(v; \cdot) &= {vT} \text{ (call } \text{Play}_A(2v; \cdot) \ &\quad + \text{afterRel5 : send } (vT \rightarrow B)} \end{align*} ]

Here, we have not used external parameters, and we have omitted writing if ( \text{true} ) in the funding precondition.

To start the game, participants can invoke the Init clause. Since it has no funding precondition, this does not require paying tokens upfront. After that, the contract gives two options: either calling \text{Play}_A or \text{Play}_B. Choosing either option requires the player to satisfy its funding precondition: here, both clauses require paying ( v = 1 ) tokens ( T ), since the internal parameter ( v ) is set to 1 by the caller \text{Init}. Now, assume that \text{Play}_A was chosen. The clause offers two new options: either calling \text{Play}_B with a doubled internal parameter ( v ), or sending ( v ) units of ( T ) to player ( A ) after 5 time units. The first option requires to pay other ( v = 1 ) tokens to the contract, so that its new balance satisfies the funding precondition of \text{Play}_B. After that, both players can take turns doubling the contract balance, until one of them fails to do so within 5 time units. When this happens, the other player can redeem the whole contract balance, ending the game.

In the game seen so far, the contract balance is fully determined by the contract itself, with players having no choice in regard to how many tokens they can add. External parameters allow us to make the game more interesting, letting players arbitrarily raise the bet as long as it is greater than the double of the previous balance:

[ \begin{align*} \text{Play}_A(v; \cdot) &= {wT \text{ if } w > 2v} \text{ (call } \text{Play}_B(w; \cdot) \ &\quad + \text{afterRel5 : send } (wT \rightarrow A)} \ \text{Play}_B(\bar{w}; \cdot) &= {\bar{w}T \text{ if } \bar{w} > 2\bar{w}} \text{ (call } \text{Play}_A(\bar{w}; \cdot) \ &\quad + \text{afterRel5 : send } (\bar{w}T \rightarrow B)} \end{align*} ]

For instance, assume that \text{Play}_A(v; \cdot) is active when ( v ) is determined by the process, while the external parameter ( w =? ) is chosen by the player, provided that it respects the funding precondition of \text{Play}_B, namely ( w > 2\bar{w} ). This means that the player must pay enough tokens to make the contract balance reach ( 2w ) tokens, doubling the previous balance ( w ).

More on ILLUM clauses. Generalising from the previous examples, processes ( C ) are choices ( D_1 + \cdots + D_k ) among one or more branches. Branches have two forms:

• \text{send} \ (v_1T_1 \rightarrow A_1) \cdots (v_nT_n \rightarrow A_n). This branch sends ( v_i ) tokens of type ( T_i ) to participant ( A_i ) (for all ( i )). The needed funds are taken from the process balance and from the contributing participants.

• call ( \langle X_1(\cdot);? \rangle \cdots \langle X_n(\cdot);? \rangle ). This branch invokes the clauses ( X_i ) in parallel, with the actual internal parameters given by the expressions ( E_i ). The external parameters ? represent values chosen by participants. The call operation is enabled when the funding preconditions of every ( X_i ) are satisfied. Like in the previous case, the needed funds are taken from the process balance, and from additional funds possibly sent by participants.

Branches can be decorated with time constraints and authorizations. Time constraints enable a branch only after a certain time has passed. They can be absolute (after ( t ): ( D )), making the branch ( D ) enabled since a certain time ( t ), or relative (afterRel ( \delta : D )), making ( D ) enabled after a delay ( \delta ) since the previous contract step. Authorizations (( A : D )) enable a branch only when ( A ) has provided their authorization. Note that multiple authorizations are possible (e.g., ( A : B : D )). In this case, all the

¹. https://github.com/bitbart/illum-lang/

involved participants must agree on the chosen branch. Furthermore, if the branch is a call, then they must also agree on the values of the external parameters. Effectively, all the external parameters are chosen by the authorizers.

To stipulate a contract, participants spawn an instance of a clause, providing the funds required by its funding precondition $v \mathcal{T}$. Note that $v \mathcal{T}$ can be a sequence $v_1 \mathcal{T}_1 \cdots v_n \mathcal{T}_n$, meaning that $v_i$ units of each token $\mathcal{T}_i$ are required. Doing so activates the clause, running its process, which can in turn spawn instances of other clauses via call, transferring the control to them. Spawning multiple instances of clauses is possible by exploiting the inherent parallelism of the UTXO model. We take advantage of this parallelism in the following example.

Exploiting parallelism. We specify a “Ponzi” scheme contract as follows:

$$ P(v; A) = { v \mathcal{T} } \text{ call } \langle S(2v; A); |P(2v; ?)\rangle|P(2v; ?) } $$

$$S(v, A) = { v \mathcal{T} } \text{ send } \langle v \mathcal{T} \rightarrow A \rangle$$

The clause $P$ takes an integer $v$ as an internal parameter, and a participant $A$ as an external parameter (denoting the owner). The funding precondition requires $v$ units of $\mathcal{T}$. The clause $P$ calls $S$ along with two copies of itself (each one doubling the internal parameter $v$) (note that they are before the “;”).

When $P(v; A)$ is active, to continue the contract we need to satisfy the preconditions of all called clauses, which require $6v \mathcal{T}$ overall. Since the contract balance is $v \mathcal{T}$, participants must provide $5v \mathcal{T}$. In practice, the owner $A$ will need to convince two participants $B$ and $C$ to provide $2.5v \mathcal{T}$ each, in exchange for setting themselves as owners in the newly spawned copies of $P$. When the call is performed, the former owner $A$ receives $2v \mathcal{T}$. If $B$ and $C$ later manage to enrol two other participants in the scheme, they will receive $4v \mathcal{T}$, gaining $4v \mathcal{T} – 2.5v \mathcal{T} = 1.5v \mathcal{T}$. Note that if $C$ does not find new participants, but $B$ does, $B$ can still continue its process, since each copy of $P$ executes independently. We remark that $B$ and $C$ are not known when $A$ is enrolled: this is why we need to use external parameters.

Upon compilation, parallel active contracts can be concurrently executed by UTXO blockchain nodes by exploiting their internal parallelism. This would not be possible with a traditional stateful account-based implementation, where a single contract would process all transactions.

2.2. The UTXO model

ILLUM contracts can be executed on a bare-bone UTXO blockchain, with no Turing-complete scripting language and no gas mechanism. Basically, a UTXO model similar to Bitcoin’s is enough, with the addition of custom tokens and covenants [16]–[18].

A transaction $\mathcal{T}$ in this UTXO model is a tuple with the following fields, similarly to Bitcoin:

  • out is a sequence of transaction outputs, i.e. triples of the form $(\arg, \scr, \val)$, where $\arg$ is a sequence of values (which we use to encode the contract state), $\scr$ is the script specifying the spending condition, and $\val$ encodes the tokens held by the output $(\mathcal{T})$.
  • in is a sequence of transaction inputs, referring to the transaction outputs which are going to be spent by $\mathcal{T}$. An input $(\mathcal{T}’, i)$ refers to the $i$-th output of a previous transaction $\mathcal{T}’$.
  • wit is a sequence of witnesses (sequences of values), passed as parameters to the scripts of input transactions. More precisely, if $\mathsf{in}(j) = (\mathcal{T}’, i)$, then $\mathsf{wit}(j)$ is the witness passed to the script $\mathcal{T}’.\mathsf{out}(i).\mathsf{scr}$.

As a simple example, we display below a transaction $\mathcal{T}_1$ containing a single output, which holds 1T and can be redeemed by any transaction carrying a signature of $A$ in its wit field (referred to by $\mathsf{rtx}.\mathsf{wit}$).

$\mathcal{T}_1$
$\mathsf{in}(1): { \mathcal{T}_1, 1 }$
$\mathsf{wit}(1): { \mathsf{sig}_A(\mathcal{T}_2) }$
$\mathsf{out}(1): { \arg: pk_A, }$
$\mathsf{scr}: \mathsf{versig}(\mathsf{ctxo}.\mathsf{arg}_1, \mathsf{rtx}.\mathsf{wit})$
$\mathsf{val}: 1T$

In order to redeem the tokens held in a transaction output $\mathcal{T}’.\mathsf{out}(j)$, a transaction $\mathcal{T}”$ must have the spending condition $\mathcal{T}’.\mathsf{out}(j).\mathsf{scr}$. This script can access the fields of $\mathcal{T}$ and $\mathcal{T}”$, perform basic arithmetic, logical and cryptographic operations (hasing, signature verification of the redeeming transaction), and enforce time constraints. Covenant operators allow the script in $\mathcal{T}$ to constrain the scripts in $\mathcal{T}”$. The covenant $\mathsf{verscr}((\sigma, n))$ mandates the $n$-th output of $\mathcal{T}”$ to have a script equal to $\sigma$. The covenant $\mathsf{verrec}(n)$ requires the $n$-th output of $\mathcal{T}”$ to have the same script of $\mathcal{T}.\mathsf{out}(j)$, the one currently being checked.

As an example, consider the following transaction redeeming the (only output) of $\mathcal{T}_1$:

$\mathcal{T}_2$
$\mathsf{in}(1): { \mathcal{T}_1, 1 }$
$\mathsf{wit}(1): { \mathsf{sig}_B(\mathcal{T}_2) }$
$\mathsf{out}(1): { \arg: pk_B, }$
$\mathsf{scr}: \mathsf{versig}(\mathsf{ctxo}.\mathsf{arg}_1, \mathsf{rtx}.\mathsf{wit})$
$\mathsf{val}: 1T$

The transaction $\mathcal{T}_2$ can redeem its input, since it carries a witness (a signature of $A$) that satisfies the script $\mathcal{T}_1.\mathsf{out}(1).\mathsf{scr}$. Furthermore the assets in $\mathcal{T}_2$’s output do not exceed those in its inputs. The spending condition of $\mathcal{T}_2$ is given by the argument (containing $A$’s public key $pk_A$), and the script $\mathsf{scr}$. The script is a conjunction of three conditions:

  • the wit of the redeeming transaction must contain a transaction signature, to be verified against the public key stored in the 1st element of the arg sequence of the current transaction output (denoted by $\mathsf{ctxo}.\mathsf{arg}_1$). In $\mathcal{T}_2$, this is just $pk_A$.
  • the 1st output of the redeeming transaction must have 1T value (here $\mathsf{rtxo}(i)$ is the $i$-th output of the redeeming transaction).
  • the 1st script of the redeeming transaction must be equal to the current one. This is enforced using the covenant $\mathsf{verrec}(1)$.

This transaction actually implements a sort of Non-Fungible Token (NFT). To transfer the NFT to $B$, $A$ spends $\mathcal{T}_2$ with a redeeming transaction $\mathcal{T}_3$, writing her signature in the wit field of $\mathcal{T}_3$, and setting the arg field to $B$’s public key $pk_B$. Note that the script and the balance are preserved along transactions thanks to the covenant.

2.3. The ILLUM compiler

One of our main contributions is a compiler from ILLUM contracts to UTXO transactions. Intuitively, we encode active clauses into transaction outputs, where the ( \text{val} ) field records the contract balance, ( \text{scr} ) enforces the contract logic, and ( \text{arg} ) records the contract state.

The ( \text{arg} ) field of a transaction output encoding an active clause will have one entry for each actual parameter, and the following additional entries: ( \text{name} ) to represent the clause name, ( \text{branch} ) to represent the index of the executed branch, and ( \text{nonce} ) to keep the behaviour faithful to the ILLUM semantics. The ( \text{scr} ) field of all transactions outputs resulting from the compilation of an ILLUM contract is the same, and it is preserved along chains of transactions by using the ( \text{verrec} ) covenant.

Here we illustrate the compilation of an auction contract focussing on the construction of the script.

An auction contract. The contract (Figure 1) consists of three clauses: ( \text{Init} ) that takes no parameters and initialises the auction with a starting bid of 0 tokens; ( \text{Bid} ) that allows a ( \text{Bidder} ) to raise the ( \text{oldBid} ) to a ( \text{newBid} ); and ( \text{Pay} ) which transfers tokens to a participant. The contract flows as follows. After the initialisation, a participant can call the clause ( \text{Bid} ) to start the auction, setting themselves as the highest bidder. Then, we must execute one of the two branches of ( \text{Bid} ). The first branch raises the bid, setting the values of ( \text{newBid} ) and ( \text{Bidder} ) through external parameters, and refunds the previous bidder. The second branch closes the auction, transferring the tokens to the hardcoded ( \text{Owner} ). Since the first branch of ( \text{Bid} ) recursively calls the clause ( \text{Bid} ) itself, it can only be taken if the funding precondition is satisfied, which means that the new bid must be greater than the previous one. On the other hand, the second branch of ( \text{Bid} ) can only be executed by the owner after a deadline of 1000 time units. By choosing this branch the owner closes the auction, and receives the highest bid.

Compiling the contract, we obtain the following script:

[ \text{scr}\text{Auction} := \begin{cases} \text{idx} = 1 & \text{if } \langle \text{ctxo}.\text{name} = \text{Init} \rangle \text{ then scr}\text{Init} \text{ else } \ \text{idx} = 1 & \text{if } \langle \text{ctxo}.\text{name} = \text{Bid} \rangle \text{ then scr}\text{Bid} \text{ else } \ \text{idx} = 1 & \text{if } \langle \text{ctxo}.\text{name} = \text{Pay} \rangle \text{ then scr}\text{Pay} \text{ else false} \end{cases} ]

The condition ( \text{idx} = 1 ) checks that this output is redeemed by an input at position 1. This is needed to thwart attacks where a transaction spends two contracts at once, effectively cancelling one of them. The rest of the script is a switch among the possible clauses, where ( \text{ctxo}.\text{name} ) denotes the ( \text{name} ) item of the ( \text{arg} ) field in the current transaction output. For brevity here we only illustrate the most interesting case, i.e. ( \text{scr}_\text{Bid} ). Recall that the ( \text{Bid} ) process is a choice between two branches. Consequently, the associated script has the following form:

[ \text{scr}\text{Bid} := \begin{cases} \text{if BranchCond1 then scr}\text{Branch1} & \text{else if BranchCond2 then scr}_\text{Branch2} & \text{else false} \end{cases} ]

The first branch calls two clauses, i.e. ( \text{Bid} ) and ( \text{Pay} ):

[ \text{call} \langle \text{Bid}⟨\text{newBid},?⟩,? \rangle ∥ \text{Pay}⟨\text{newBid},\text{Bidder}⟩ ]

Consistently, ( \text{BranchCond1} ) checks that the redeeming transaction ( \text{rtx} ) has exactly two outputs: this is the goal of the condition ( \text{outlen}(\text{rtx}) = 2 ) below. Furthermore, ( \text{BranchCond1} ) checks that the chosen branch is indeed the first one: this is done by requiring that both outputs in the redeeming transaction ( \text{rtxo}(1) \text{ and } \text{rtxo}(2) ) have the argument ( \text{branch} ) set to 1.

[ \text{BranchCond1} := \text{outlen}(\text{rtx}) = 2 \text{ and } \text{rtxo}(1).\text{branch} = 1 \text{ and } \text{rtxo}(2).\text{branch} = 1 ]

The second branch instead performs a send operation with exactly one recipient, so we check that the redeeming transaction has exactly one output, which has its ( \text{branch} ) argument set to 2.

[ \text{BranchCond2} := \text{outlen}(\text{rtx}) = 1 \text{ and } \text{rtxo}(1).\text{branch} = 2 ]

The script ( \text{scr}_\text{Branch1} ) verifies that the two outputs of the redeeming transaction encode, respectively, the clauses ( \text{Bid} ) and ( \text{Pay} ). The part corresponding to ( \text{Bid} ) is:

[ \text{rtxo}(1).\text{name} = \text{Bid} \text{ and } \text{verrec}(1) \text{ and } |\text{rtxo}(1).\text{arg}| = 6 \text{ and } \text{rtxo}(1).\text{oldBid} = \text{ctxo}.\text{newBid} \text{ and } \text{rtxo}(1).\text{val} = \text{rtxo}(1).\text{newBid} \text{ and } \text{rtxo}(1).\text{newBid} > \text{rtxo}(1).\text{oldBid} \text{ and } \text{rtxo}(1).\text{Bidder} \neq \text{Null} \text{ and } \cdots ]

The script performs the following checks on the redeeming transaction: (i) the clause name in the first output is indeed ( \text{Bid} ); (ii) the script is preserved (via the ( \text{verrec} ) covenant); (iii) the number of arguments is correct (3 arguments for ( \text{newBid} ), ( \text{oldBid} ) and ( \text{Bidder} ), and 3 arguments for ( \text{name} ), ( \text{branch} ) and ( \text{nonce} )); (iv) the value of the ( \text{oldBid} ) of the redeeming transaction is set to the ( \text{newBid} ) of the current transaction, coherently with the passing of parameters in the ( \text{Bid} ) clause; (v) the amount of tokens of type ( T ) transferred to the redeeming transaction is the one specified in the funding precondition; (vi) the guard in the funding precondition is satisfied.

The part of the script corresponding to ( \text{Pay} ) is obtained in the same way:

[ \cdots \text{rtxo}(2).\text{name} = \text{Pay} \text{ and } \text{verrec}(2) \text{ and } |\text{rtxo}(2).\text{arg}| = 5 \text{ and } \text{rtxo}(2).A = \text{ctxo}.\text{Bidder} \text{ and } \text{rtxo}(2).v = \text{ctxo}.\text{newBid} \text{ and } \text{rtxo}(2).\text{val} = \text{ctxo}.\text{newBid} \cdot T ]

The script scrBranch2 encodes the send operation in Figure 1, enforcing the authorization of Owner and the absolute time constraint of 1000 time units:

absAfter 1000 : versig(Owner, rtx.wit(1)) and verscr(vctx.owner, rtx.wit(1)), 1) and
|rtxo(1).arg| = 3 and
rtxo(1).owner = Owner and
rtxo(1).val = ctxo.newBid T

The script performs the following checks on the redeeming transaction: (i) absAfter forces the redeeming transaction to be published at a time greater than 1000; (ii) the first versig checks the presence of Owner‘s signature in the witness of the redeeming transaction; (iii) the only output of the redeeming transaction has 3 arguments (owner, branch, and nonce), and a script that accepts any transaction signed by the owner (this is enforced by the verscr covenant). This effectively transfers the ownership of the tokens to Owner. The details of our compilation technique are in Section 4.

2.4. Security of the ILLUM compiler

Our main technical result is the security of the compiler establishing a strict correspondence between actions at the ILLUM level and those at the blockchain level. This ensures that any contract behaviour that is observable at the blockchain level is also observable in the semantics of ILLUM. In particular, any attack that may happen at the blockchain level can be detected by inspecting the symbolic semantics of ILLUM contracts. This is a fundamental step towards static analysis tools for the verification of security properties of contracts in the UTXO model.

Here we outline how this result is proved in Sections 5 and 6. We start by defining the adversary model, both at the symbolic level of ILLUM and at the computational level of the blockchain. The adversary is modelled as a PPTIME algorithm that schedules the actions chosen by participants, possibly interleaving them with adversarial actions. The bridge between the symbolic and the computational level is given through a coherence relation, which associates symbolic actions (e.g., a call action) with their computational counterparts (e.g., a transaction). The definition of this coherence relation is quite gruelling, as it must consider all possible actions, which amount to 20 cases: this complexity of course reflects on the proofs. As a first sanity check, we show in Lemma 1 that the coherence relation precisely characterizes the exchange of assets: namely, the asset ownership is consistent between symbolic and computational executions whenever they are coherent. Our main security result (Theorem 2) guarantees that any computational execution is coherent with some symbolic execution, up-to a negligible error probability. Together with Lemma 1, it proves that computational exchanges of assets, including those mediated by contracts, are always mirrored at the symbolic level.

3. The ILLUM intermediate language

We now refine the description of ILLUM given in Section 2, by providing its syntax and semantics. Because of space constraints, we omit some technicalities, relying on examples and intuitions: see [21] for full details.

Syntax.

We assume a set Part of participants, (ranged over by A, B, ⋯, and by a dummy participant Null). Contracts and deposits are denoted by the lowercase letters x, y, ⋯, while clauses will have names X, Y, ⋯. Clause parameters will be denoted by Ii and Ex, while the actual values substituted to those parameters will be denoted by T, and Ex. Arithmetic expressions (integer constants and parameters, basic operations, hashes) are denoted by E, while participant expressions (constants and parameters) are denoted by Ni. The value of parameters and expressions can also be key-value mappings. The domain of a mapping can be chosen to be either the integers or the participants. The codomain can be chosen similarly. If M is a mapping expression, we denote with M[⋯] the access to one of its values, and with M[⋯ → ⋯] the update of one of its associations. Sequences are denoted in bold, with x = x_1 · · · x_n.

We remark that the precise set of data types that can be used in parameters and expressions is not fundamental to the design of ILLUM. Indeed, our design can be easily adapted to different data types by suitably altering the syntax and semantics of expressions. To support compilation to the UTXO model, we simply require that the underlying blockchain scripting language supports the same data types and operations. We assume that data types include at least integers and participants, since their role is crucial to ILLUM constructs. Key-value mappings, instead, are not as crucial, and could be removed if not supported by the underlying blockchain, at the expense of reducing the usability of ILLUM. Throughout the paper, we mostly showcase examples that use only the fundamental data types (integers and participants). Notably, the ILLUM compiler handles all these contracts without requiring mappings to be supported by the compilation target. In Section 7 we will also exploit mappings to discuss more complex contracts.

Definition 1 (Clauses). A clause is defined by an equation

[ x(\text{In}_i; \text{Ex}_j) = {E[T] \text{ if } p} C ]

where {E[T] if p} is the funding precondition, and C is a process. The clause takes two sequences of parameters In and Ex. Parameters can be of any type (integers, participants, or mappings). These types are always clear from the context, hence omitted. We require that all the parameter names in E, p, and C are present in In, Ex.

When X is invoked, the calling process provides the actual internal parameters, while the participants who are performing the call choose the actual external ones. The funding precondition {vT if p} encodes the requirements for the invocation of X. Namely, the sequence vT = v_1T_1 · · · v_nT_n, asks the participants to transfer v_i tokens of type T_i to the process C (for all i). Moreover, p is a boolean condition on the parameters that must hold. We write {vT} for {vT if true}.

Definition 2 (Processes). Processes have the following

syntax: [ C ::= \sum_{i \in I} D_i \quad \text{process} ] [ D ::= \text{branch} ] [ \text{call} \ldots \parallel \langle X_i ; \text{In}_i ; ? \rangle \parallel \ldots ] [ \text{send} \ldots \parallel \langle E_i ; T_i \rightarrow N_i \rangle \parallel \ldots ] [ N : D ] [ \text{after} \ E : D \quad \text{wait for} \ N \quad \text{authorization} ] [ \text{afterRel} E : D \quad \text{wait until} \ E ] [ \text{call} \ldots \parallel \text{Ex} \parallel \ldots \quad \text{after activation} ]

where we assume that: (i) each clause name ( X ) has a unique defining equation ( X(\text{In} ; \text{Ex}) = { \text{ET} \text{ if } p } C ); (ii) the sequence ( \text{In} ) of actual parameters passed to a called clause ( X_i ) matches, in length and typing, the sequence ( \text{In} ) of formal (internal) parameters; (iii) the order of decorations is immaterial.

A clause ( X(\ldots) ) together with two correctly typed sequences of actual parameters ( \text{In} ) and ( \text{Ex} ) is said to be an instantiated clause, and denoted by ( X(\text{In} ; \text{Ex}) ).

Semantics. The execution of contracts is modelled as a transition relation between configurations, that are abstract representations of the blockchain state. In a configuration, tokens can be stored in deposits and active contracts.

A deposit ( \langle A, v T \rangle ) represents ( v ) units of token ( T ) owned by ( A ). It is uniquely identified by the name ( x ), and can only be spent upon ( A )’s authorization. A term ( \langle C, v T \rangle ) is an active contract, where ( x ) is the unique identifier, ( t ) is the activation time, and ( v T ) is the balance, which can only be transferred according to the contract logic specified by ( C ).

Besides the terms used to store tokens, in a configuration we also have advertisements and authorizations.

Advertisement terms are used by a participant to propose one of the following actions:

  • The activation of a new contract. This is done by advertising ( \Phi = [X; z; (x, j)] ), which specifies the instantiated clause ( X(\text{In} ; \text{Ex}) ) and a nonempty list ( z ) of deposit names that will be spent to fund the contract. The index ( h ) is just a nonce used to differentiate between two otherwise identical advertisements.
  • The continuation of an active contract. This is done by advertising ( \Phi = [D ; z; (x, j)] ). The list ( z ) specifies the deposits that will be spent for the continuation and added to the balance of ( x ). The index ( h ) is again a nonce. The term ( D ) is an advertised branch, constructed by taking ( D ), the ( j )-th branch of ( x ), and instantiating the question marks ( ? ) appearing in a call with the actual values ( \text{Ex} ).

Authorization terms are used by participants to enable the spending of deposits and to enable the execution of a contract branch decorated by ( A ). Authorizations have the form ( A[\chi] ), where ( A ) is the authorizing participant, and ( \chi ) denotes the authorized action. We see here two cases of authorization terms, relegating the others to Appendix A:

  • ( A[z \triangleright \Phi] ) authorises the spending of a deposit ( z ) owned by ( A ) that appears in the advertisement ( \Phi ).
  • ( A[x \triangleright \Phi] ) authorises the continuation of the ( j )-th branch of a contract ( x ), as advertised by ( \Phi = [A ; D ; z; (x, j)] ).

Definition 3 (Configurations). A configuration ( \Gamma ) is a term ( \Gamma \mid t ), where ( t \in \mathbb{N} ) denotes the time, and the pre-configuration ( \tilde{\Gamma} ) has the following syntax:

[ \tilde{\Gamma} ::= \langle C, v T \rangle \quad \text{active contract} \ \langle A, v T \rangle \quad \text{deposit} \ \Phi \quad \text{advertisement} \ A[\chi] \quad \text{authorization} \ (\tilde{\Gamma} \mid \tilde{\Gamma}) \quad \text{parallel composition} ]

We assume that: (i) the parallel composition is associative and commutative; (ii) all parallel terms are distinct; (iii) names are unique; (iv) all expressions occurring in active contracts are reduced to constants (integers or names).

An example. In Section 2 we have discussed the intuition behind the language semantics. Here we refine this intuition by precisely illustrating the evolution of the configuration during the execution of a simple contract. This example shows the semantics of the main language constructs, and the role of advertisements and authorizations terms.

[ X(a; b) = { b T \text{ if } b > a } \quad \text{Wait}(b) \ \text{Wait}(b) = \text{afterRel} 10 : \text{send} (b T \rightarrow A) \

  • B : \text{call} X(b; ?) ]

The first branch allows ( A ) to withdraw the whole balance after 10 time units since the contract activation. The second branch allows ( B ) to temporarily prevent ( A ) from withdrawing: this requires ( B ) to restart the contract with an increased balance. We start from the initial configuration:

[ \Gamma_0 = \langle C, 1 T \rangle z_1 | \langle B, 2 T \rangle z_2 | \langle B, 3 T \rangle z_3 | t ]

Participant ( C ) starts by advertising ( \Phi_0 = [X(0; 1) ; z_1] ), then authorizes the use of their deposit ( z_1 ) in the stipulation, and finally stipulates the contract, reaching configuration ( \Gamma_1 ):

[ \Gamma_0 \rightarrow \Gamma_0 \mid \Phi_0 \rightarrow \Gamma_0 \mid \Phi_0 | C[z_1 \triangleright \Phi_0] \ \rightarrow \langle \text{Wait}(1), 1 T \rangle z_2 | \langle B, 2 T \rangle z_2 | \langle B, 3 T \rangle z_3 | t = \Gamma_1 ]

From ( \Gamma_1 ) there are multiple possible continuations. For instance, ( B ) can choose to execute the second branch of ( \text{Wait} ). To do so, ( B ) first produces the advertisement ( \Phi_1 = [B : \text{call} X(1; 3) ; z_2 ; (x, 2)] ). Then, ( B ) gives two authorizations: one to satisfy the decoration ( B : \ldots ) in the second branch of ( \text{Wait} ), and another one to allow the spending of ( z_2 ). With these, the configuration can evolve as follows:

[ \Gamma_1 \rightarrow \Gamma_1 \mid \Phi_1 \rightarrow \Gamma_1 \mid \Phi_1 \mid B[x \triangleright \Phi_1] \ \rightarrow \Gamma_1 \mid \Phi_1 | B[x \triangleright \Phi_1] | B[z_2 \triangleright \Phi_1] \ \rightarrow \langle \text{Wait}(3), 3 T \rangle z_2 | \langle B, 3 T \rangle z_3 | t = \Gamma_2 ]

( B ) can again choose the second branch, this time spending ( z_2 ) to fund its execution. Otherwise, if ( B ) lets the time pass, ( A ) can advertise the continuation:

[ \Phi_2 = [\text{afterRel} 10 : \text{send} (3 T \rightarrow A) ; (x’, 1)] h ]

and then withdraw the contract balance:

[ \Gamma_2 \rightarrow \langle \text{Wait}(3), 3T \rangle^{l_T}{x_r} \mid \langle B, 3T \rangle{z_3} \mid t + 10 = \Gamma_3 \ \rightarrow \Gamma_3 \mid \Phi_2 \rightarrow \langle A, 3T \rangle^{l_T}{x_2} \mid \langle B, 3T \rangle{z_3} \mid t + 10 ]

The semantics of ILLUM has a set of rules for reducing contracts, and another set for deposits (see Appendix A).

Turing-completeness. ILLUM is Turing-complete: indeed, we can simulate in ILLUM any counter machine [22], a well-known Turing-complete computational model. The proof is similar to that in [23]: we simulate any counter machine by storing each counter in the arguments of recursive clauses. Incrementing and decrementing the counters is simply done by specifying the new values of the arguments inside the call. Conditional jumps are simulated as choices, also exploiting clause preconditions. This construction does not exploit key-value mappings: it is only based on the assumption that integers are unbounded, as usual. Notice that, despite its Turing-completeness, ILLUM can be compiled down to a “poor” UTXO blockchain, i.e. one with non-Turing-complete scripts. This is accomplished by spreading the execution of a compiled contract across multiple transactions, each with its own loop-free script. Note that our key-value mappings just feature operators to lookup a single key and to update a single association: in this way, even with maps, UTXO scripts can be run in nearly constant-time. This makes the gas mechanism unnecessary.

4. Compiling ILLUM to UTXO scripts

The compilation target of ILLUM is a UTXO blockchain that is close to Bitcoin, with minimal extensions in the structure of transactions and in the scripting language to overcome its expressiveness limitations.

Scripting language. We consider a scripting language that extends Bitcoin Script with covenants, borrowing from [16] (see [21] for its syntax and semantics). Here we recap some operators that are used by our compiler. First, \texttt{ctxo.f} denotes the field ( f ) of the current transaction output that is being spent. Similarly, \texttt{rtxo(e).f} denotes the field ( f ) of the ( e )-th output of the redeeming transaction. Then, we have the covenants: \texttt{verscr}(\texttt{scr}, n) checks that the ( n )-th output script of the redeeming transaction is equal to \texttt{scr}, while \texttt{verrec}(n) checks that the ( n )-th output script of the redeeming transaction is equal to the one of the output being spent. The operators \texttt{inidx} and \texttt{rtxw} denote, respectively, the position of the redeeming input among the ones of the redeeming transaction, and the witness associated to it. To improve readability, we will use names instead of indices when referring to arguments in the \texttt{arg} sequence (e.g., we write \texttt{ctxo.owner} for \texttt{ctxo.arg.1}).

While constructing a contract script we will need to replace the parameters ( \texttt{ln}_i ) and ( \texttt{Ex}_i ) appearing in an expression ( E ) with the respective arguments \texttt{ctxo.ln}_i and \texttt{ctxo.Ex}_i. To simplify the notation, we denote this substitution with \texttt{ctxo.E}. For instance, if the contract contains a term ( t \cdot \cdots \cdot t = \texttt{ln}_1 + \texttt{Ex}_3 + 3 ), we will write \texttt{ctxo.t} instead of \texttt{ctxo.ln}_1 + \texttt{ctxo.Ex}_3 + 3. Similarly, whenever an expression uses the arguments of a redeeming transaction’s output, we denote it as \texttt{rtxo(j).E}.

Representing deposits. We represent a deposit ( \langle A, vT \rangle ) in an ILLUM configuration as a transaction output with value ( vT ), argument \texttt{owner} set to ( A ), and the script:

[ \text{versig}(\texttt{ctxo.owner}, \texttt{rtxw.1}) ]

allowing ( A ) to spend the funds by providing her signature.

How the compiler works. Representing an active contract ( \langle C, vT \rangle ) at the blockchain level is more complex: we need to consider the clause ( X(\texttt{ln}_i; \texttt{Ex}_j) ) from which it originated. The output representing ( x ) has a value ( vT ), and its arguments are the following: \texttt{name} for the clause name ( X ), for the actual parameters \texttt{ln}_i and \texttt{Ex}_j, and two technical arguments \texttt{nonce} and \texttt{branch}. The output script of a contract is preserved along executions: we detail its construction in the next paragraphs, refining and generalising the intuitions given in Section 2 (the full technical details are in [21]).

Let ( X_0 ) be the initial clause of a contract, and let ( X_1 \cdot \cdots \cdot X_n ) be the clauses that can be reached by recursively following every \texttt{call} operation that appears in ( X_0 )’s definition. We assume that ( X_i ) defines the process ( C_i ). We generate a script for the overall contract as follows. The script requires that the output must be redeemed from an input in the first position. Then, it performs a switch on the \texttt{name} argument to see which clause is currently encoded in the transaction output, and choose accordingly which script is going to be executed:

[ \text{scr} := \text{inidx} = 1 \quad \text{and} ]

[ \begin{align*} \text{if} \ (\text{ctxo.name} = X_0) & \ \text{then} \ \text{scr}{X_0} \ \text{else} \ & \quad \vdots \quad \vdots \ \text{if} \ (\text{ctxo.name} = X_n) & \ \text{then} \ \text{scr}{X_n} \ \text{else} \ \text{false} \end{align*} ]

To construct the script associated to a clause ( X ) in ( X_0 \cdot \cdots \cdot X_n ), we inspect its process ( C = D_1 + \cdots + D_m ), and associate an integer ( n_j ) with each ( D_j ) as follows: if ( D_j ) ends in a \texttt{call} then ( n_j ) is equal to the number of called clauses; otherwise, if ( D_j ) ends in a \texttt{send}, then ( n_j ) is equal to the number of participants receiving the funds. This ( n_j ) will be the number of outputs of a transaction that redeems the ( j )-th branch of ( C ). This transaction must also specify the value ( j ) in the \texttt{branch} argument of each of its outputs. To check these conditions, we use:

[ B_j := (\text{outlen(\texttt{rtx}))} = n_j \ \text{and} \ \text{rtxo(1).branch} = j \quad \text{and} \quad \cdots \quad \text{and} \ \text{rtxo(n_j).branch} = j ]

Then, we handle all the branches, with a conditional

[ (\text{scr}X := \text{if} \ B_1 \ \text{then} \ \text{scr}{D_1} \ \text{else} \ \vdots \quad \vdots \ \text{if} \ B_m \ \text{then} \ \text{scr}_{D_m} \ \text{else} \ \text{false}) ]

Each branch ( D ) in ( D_1 \cdot \cdots \cdot D_m ) is a sequence of decorations ended by a \texttt{call} or \texttt{send}. To construct ( \text{scr}_D ), we first focus on the decorations. If there is an authorization decoration, then the witnesses of the redeeming transaction requires a signature by the authorizing participant:

[ \text{scr}{A_1} \cdot \cdots \cdot \text{scr}{A_k} \cdot D : = \text{versig}(\texttt{ctxo.A_1}, \texttt{rtxw.1}) \quad \text{and} \quad \cdots ]

and \texttt{versig}(\texttt{ctxo.A_k}, \texttt{rtxw.k}) and \texttt{scr}_{D’}.

where ( D’ ) does not contain any authorization decoration. The “after” decorations are handled by the corresponding script operators absAfter/relAfter for absolute/relative timelocks:

[ \begin{align*} \text{scr}{\text{after} \cdot t} : D’ & := \text{absAfter ctxo} \cdot t : \text{scr}{D”} \ \text{scr}{\text{afterRel} \cdot \delta} : D’ & := \text{relAfter ctxo} \cdot \delta : \text{scr}{D”} \end{align*} ]

Finally, we describe the terminal parts of the script, i.e., send and call. First, we consider the case:

[ D” = \text{send} (v_1 T_1 \parallel \cdots \parallel v_n T_n \rightarrow A_n) ]

Here, we want each output of the redeeming transaction to encode a deposit of value ( v_i T_i ) owned by ( A_i ). We use the operator verscr to force the redeeming transaction to have the correct script, and ( \cdot | \cdot ) to check that it has exactly 3 arguments (corresponding to nonce, branch, and owner). The script also checks the output values and the owners:

[ \begin{align*} |\text{rtxo}(i)\text{.arg}| & = 3 \ \text{verscr}(\text{versig(ctxo} \cdot \text{owner}, \text{rtxo} \cdot \text{v}_i \cdot \text{T}_i), i) \text{ and} \ \text{rtxo}(i)\text{.owner} & = \text{ctxo} \cdot A_i \text{ and} \ \text{rtxo}(i)\text{.val} & = \text{ctxo} \cdot v_i T_i \text{ and} \ \end{align*} ]

The last case is that for a call:

[ D” = \text{call} (Y_1 (\text{In}_1; ?) \parallel \cdots \parallel Y_n (\text{In}_n; ?)) ]

Let ( Y_i(\text{In}_i; \text{Ex}_i) = {E_i T_i \text{ if } p_i} C_i ), where ( |\text{In}_i| = k_i ) and ( |\text{Ex}i| = h_i ). The script ( \text{scr}{\text{call} i} ) requires that the ( i )-th output of the redeeming transaction encodes the contract specified by ( Y_i(\text{In}_i; \text{Ex}_i) ), for some choice of the parameters ( \text{Ex}_i ). We use verrec to preserve the contract script, and then check that the output has the correct number of arguments. We also require that the ( \text{name} ) is ( Y_i ), and that the arguments ( \text{In}_i ) match the actual parameters.

Finally, we check the funding precondition:

[ \begin{align*} \text{scr}_{\text{call} i} := \text{verrec}(i) \text{ and } |\text{rtxo}(i)| & = 3 + k_i + h_i \text{ and} \ \text{rtxo}(i)\text{.name} & = Y_i \text{ and} \ \text{rtxo}(i)\text{.In}_i & = \text{ctxo} \cdot \text{In}_i \text{ and} \ \text{rtxo}(i)\text{.Ex}_i & = \text{ctxo} \cdot \text{Ex}_i \text{ and} \ \text{rtxo}(i)\text{.val} & = \text{rtxo}(i) E_i T_i \text{ and} \ \text{rtxo}(i)\text{.p}_i & = \text{rtxo}(i)\text{.p}_i \end{align*} ]

This must be done for all ( Y_1 \cdots Y_n ), obtaining:

[ \text{scr}{D”} := \text{scr}{\text{call} 1} \text{ and } \cdots \text{ and } \text{scr}_{\text{call} n} ]

Executing a compiled contract. The ILLUM compiler translates an ILLUM contract into a script. In this way, the compilation process creates a correspondence between active contracts and transaction outputs on the blockchain. We will formalise this coherence relation later when establishing the security of the compiler. For now, we just note that each execution step of an active ILLUM contract corresponds, in the blockchain, to a new transaction redeeming the previous output.

A hint about the correctness of the compiler. The script produced by the compiler imposes very stringent conditions on the redeeming transaction ( T ). In particular, its outputs are almost completely determined by the compiled script: the number of outputs and their assets are fixed; their script is determined either by verrec (in the call branches) or by verscr (in the send branches); the number of arguments is fixed, and the value of most of the arguments (which encode the contract state) is determined by the script. The only “free” fields in ( T ) are the arguments representing the external contract parameters, which are only subject to respect the funding precondition. This mirrors the ILLUM semantics, where participants can choose the actual external parameters at runtime. This “rigidity” is important in establishing the correctness of the ILLUM compiler: if a UTXO encodes an active contract ( \langle C, vT \rangle ), then any transaction that redeems it must behave in “agreement” with one of the branches of ( C ). The full details of the proof of correctness are presented in [21].

  1. Adversary model

The semantics of ILLUM describes all actions that can be performed on contracts and deposits. For this reason the set of reachable configurations is very broad. In particular, it always contains the configuration obtained by donating all the deposits to a single participant. However, in a realistic scenario, this configuration would not be reached because participants would have no interest in authorizing the donations. To avoid considering these unrealistic executions, we need to restrict the semantics according to the behaviour of participants, which can decide whether to authorize or not any given action. To this aim, we introduce strategies, which are algorithms that model the participants’ behaviour, computing the actions chosen by a participant at each execution step. We assume a subset ( \text{Hon} ) of participants for whom the strategies are known. The strategies of these honest participants are instrumental in defining the adversary model. Namely, we see the adversary ( \text{Adv} ) as an entity that controls the scheduling of the actions chosen by honest participants, and possibly inserts their own actions. This is consistent with adversarial miners/validators in blockchains, who can read user transactions in the mempool, and produce blocks containing some of these transactions, suitably reordered and possibly interleaved with their own transactions. Intuitively, we model the adversary as a strategy that controls all participants outside of ( \text{Hon} ), can observe the actions outputted by the strategies of honest participants, and can decide to perform one of these actions or one of their own.

Symbolic runs. A symbolic run ( R^s ) is a sequence of configurations ( \Gamma_i ) connected by semantic actions ( \alpha_i ). The first configuration in the sequence only contains deposits, and has time ( t_0 = 0 ). We denote with ( \Gamma_0 \rightarrow \cdot \cdot \cdot \rightarrow \Gamma_n ) the last configuration of ( R^s ). A run is written as ( R^s = \Gamma_0 \rightarrow \alpha_0 \Gamma_1 \rightarrow \alpha_1 \Gamma_2 \rightarrow \cdot \cdot \cdot ).}

Symbolic strategy of honest participants. Each honest participant ( A ) has a strategy ( \Sigma_{A}^{s} ), i.e. a PPTIME algorithm that takes as input the symbolic run ( R^s ) and outputs the set of “choices” of ( A ), i.e. the ILLUM actions that ( A ) wants to perform. The strategy is subject to well-formedness.

constraints: (i) the actions in $\Sigma_A^c(R^c)$ must be enabled by the semantics in $\Gamma_R$; (ii) each authorization action in $\Sigma_A^c(R^c)$ must be of the form $A[\cdot \cdot \cdot \cdot \cdot]$ forbidding $A$ to impersonate another participant.

Symbolic adversarial strategy. Dishonest participants are controlled by the adversary $Adv$, who is also in charge of scheduling updates to the run. Their strategy $\Sigma_{Adv}$ is a PPTIME algorithm that takes as inputs the run $R^s$ and the sets of choices given by the honest participants’ strategies. The output of $\Sigma_{Adv}$ is a single LLLUM action $\lambda$ that will be used to update the run. $Adv$’s strategy is subject to the following constraints: (i) $\lambda$ must be enabled in $\Gamma_R$; (ii) if $\lambda$ is an authorization action by a honest $A$, then it must have been chosen by $A$; (iii) if $\lambda$ is a delay, then it must have been chosen by all honest participants. The second condition prevents $Adv$ from forging signatures, while the third condition ensures that $Adv$ cannot prevent honest participants from meeting deadlines.

Symbolic conformance. Since a strategy $\Sigma_A^c$ is probabilistic, we implicitly assume that it takes as input an infinite sequence of random bits $r_A$. Consider now a set of strategies $\Sigma^s$ including those of honest participants, $\Sigma_{Adv}^s$, and a random source $r$ from which the sequences $r_A$ are derived. We can uniquely determine a run $R^c$ by performing the actions outputted by $\Sigma_{Adv}^c$. Such a run is said to conform to $(\Sigma^s, r)$.

Computational runs. Above, we have defined an adversarial model at the symbolic level. We model adversaries at the computational level in a similar way, replacing symbolic actions with computational ones. A computational run $R^c$ is a sequence of actions $X$ in one of these forms:

  • $T$ appending transaction $T$ to the blockchain
  • $\delta$ performing a delay
  • $A \rightarrow s : m$ broadcasting of message $m$ from $A$

The first action in the run $R^c$ is an initial transaction that distributes tokens to participants, and it is followed by the broadcast of each participant’s public keys.

Computational strategies of honest participants. Each honest $A$ is associated with a computational strategy, i.e. a PPTIME algorithm $\Sigma_A^c$ that takes as input a computational run and outputs the set of choices of $A$. If $\Sigma_A^c(R^c)$ includes an action $X = T$, then $T$ must be consistent with $R^c$, essentially meaning that $T$ is a valid transaction in the blockchain state reached after the run $R^c$.

Computational adversarial strategy. Like in the symbolic case, the adversary is given scheduling power. The strategy $\Sigma_{Adv}^c$ takes as input the run $R^c$ and the actions chosen by honest participants, and outputs a single action that will be used to update $R^c$. As for honest participants, the adversary cannot output invalid transactions. Like in the symbolic case, $\Sigma_{Adv}^c$ is only allowed to output a delay if it has been chosen by all honest participants. We allow the adversary to impersonate any honest participants $A$. However, since $Adv$ does not know the random source $r_A$, and $\Sigma_{Adv}^c$ is PPTIME, $Adv$ will be, with overwhelming probability, unable to forge $A$’s signatures.

Computational conformance. Like in the symbolic case, a set of strategies $\Sigma^s$ and a random source $r$ can be used to uniquely determine a computational run $R^c$, that is said to conform to the pair $(\Sigma^s, r)$.

6. Security of the ILLUM compiler.

Symbolic and computational runs describe the evolution of contracts at two different level of abstraction: in Section 4 we have shown how transaction outputs encode ILLUM deposits and contracts. Formally this correspondence between runs is modelled as a relation, which we call coherence. Intuitively, coherence holds when the symbolic steps in $R^s$ and the computational steps in $R^c$ have the same effects on contracts and deposits.

Coherence. The coherence relation $R^s \sim_{txout} R^c$ is parameterized by a map $txout$ that relates the symbolic names of deposits and contracts to transaction outputs. Coherence is defined inductively, by exhaustively listing the possible actions of $R^s$. Here we present the most important cases, relegating the full definition to [21].

  • Advertising $\Phi$ in $R^s$ is matched by the broadcast of a message $m$ in $R^c$. The message $m$ encodes a transaction $T_\Phi$ representing the action advertised by $\Phi$. In particular, the script of $T_\Phi$’s outputs must be the one produced by the compiler. Note that $T_\Phi$ is not yet appended to the blockchain, but only broadcast.
  • Sending an authorization $A[\cdot \cdot \cdot \cdot \cdot ]$ in $R^c$ is matched by sending a message $m$ in $R^c$, containing a corresponding signature from $A$ on $T_\Phi$.
  • Initiating a contract in $R^c$ consumes the respective advertisement $\Phi$ and the required authorizations and deposits to insert a term $\langle C, vT_\Phi \rangle^v_1$ in the configuration. This is matched in $R^c$ by appending $T_\Phi$ to the blockchain. This uses the signatures that were broadcast together with the symbolic authorizations. Moreover, the map $txout$ is updated so that the new symbolic name $x$ is mapped to $T_\Phi$’s output.
  • Continuing a contract in $R^c$ is similar to the contract initiation described above, except that it may produce multiple deposits or contracts instead of a single one. Again, it is matched in $R^c$ by $T_\Phi$, where $\Phi$ is the continuation advertisement, and $txout$ is updated to map the new names to each output of $T_\Phi$.

The full definition also deals with deposit operations, delays, and transactions that spend inputs that are outside of the image of $txout$. The coherence relation is instrumental to establish correspondence results between the two models. Notably, Lemma 1 shows that the coherence relation precisely characterizes the exchange of assets.

Lemma 1. If $R^s \sim_{txout} R^c$ and $\langle A, vT \rangle_x$ is a deposit appearing in the last configuration $\Gamma_R$, then $txout(x)$ is an unspent output in $R^c$ and encodes the deposit $x$ (i.e. it has the structure presented in Section 4). Notably, this means that the token balance is preserved by $txout$.

Useful information for enthusiasts:

Contact me via Telegram: @ExploitDarlenePRO