11institutetext: University of Padova 22institutetext: University of Bologna –
Inria FOCUS 33institutetext: University of Bologna – European University
Institute

# Pacta sunt servanda: legal contracts in _Stipula_

Silvia Crafa 11 Cosimo Laneve 22 Giovanni Sartor 33

###### Abstract

There is a growing interest in running legal contracts on digital systems, at
the same time, it is important to understand to what extent software contracts
may capture legal content. We then undertake a foundational study of legal
contracts and we distill four main features: agreement, permissions,
violations and obligations. We therefore design _Stipula_ , a domain specific
language that assists lawyers in programming legal contracts through specific
patterns. The language is based on a small set of abstractions that correspond
to common patterns in legal contracts, and that are amenable to be executed
either on centralized or on distributed systems. _Stipula_ comes with a formal
semantics and an observational equivalence, that provide for a clear account
of the contracts’ behaviour. The expressive power of the language is
illustrated by a set of examples that correspond to template contracts that
are often used in practice.

##  1 Introduction

A legal contract is “an agreement which is intended to give rise to a binding
legal relationship or to have some other legal effect” [23]. The parties are
in principle free to determine the content of their contracts (_party
autonomy/freedom of contract_): the law recognizes their intention to achieve
the agreed outcomes and secures the enforcement of such outcomes (_legally
binding effect_). A contract produces the intended effects, declared by the
parties, only if it is legally valid: the law may deny validity to certain
clauses (_e.g._ excessive interests rate) and/or may establish additional
effects that were not stated by the parties (_e.g._ consumer’s power to
withdraw from an online sale, warranties, etc.). The intervention of the law
is particularly significant when the contractor (usually the weaker party,
such as the worker in an employment contract or the consumer in an online
purchase) agrees without having awareness of all clauses in the contract, nor
having the ability to negotiate them, due to the existing unbalance of power.

The assimilation of software contracts to legally binding contracts, or rather
the double nature of digital contracts as computational mechanisms and as
legal contracts, raises both legal and technological issues. Blockchain-based
smart contracts have been advocated for digitally encoding legal contracts, so
that the execution and enforcement of contractual conditions may occur
automatically, without human intervention. However, we will mostly refer to
_software contracts_ as “digital legal contracts”, stressing the fact that
most of the benefits of digitally encoding legal contracts come from the
precise definition and automatic execution of a piece of programmable
software, not necessarily operating over a blockchain.

In this paper, after discussing the main issues raised by the literature, we
propose a technology that may contribute to addressing them. The overall aim
is to facilitate the transparency of software contracts, as well as the
mapping of computational operations into legal-institutional outcomes, thus
limiting or mitigating the problems concerning the implementation of software
contracts and preventing disputes between the parties.

Specifically, we put forward _Stipula_ , a new domain specific language for
the creation of software legal contracts. _Stipula_ is pivoted on a small
number of abstractions that are useful to capture the distinctive elements of
legal contracts, that is _permissions_ , _prohibitions_ , _obligations_ ,
fungible and non fungible _assets_ exchanges, risk (viz.  _alea_), _escrows_
and _securities_. All these normative elements are expressed by a strictly
regimented behaviour in legal contracts: permissions and empowerments
correspond to the possibility of performing an action at a certain stage,
prohibitions correspond to the interdiction of doing an action, while
obligations are recast into commitments that are checked at a specific time
limit. Moreover, the set of normative elements changes over time according to
the actions have been done (or not). To model these changes, _Stipula_ commits
to a _state-aware programming_ style, inspired by the state machine pattern
widely used in the programming language practice. This technique allows one to
enforce the intended behaviour by prohibiting, for instance, the invocation of
a function before another specific function is called.

A second distinctive feature of _Stipula_ is the _event_ primitive, a
programming abstraction that is used to issue an obligation and schedule a
future statement that automatically executes a corresponding penalty, if the
obligation is not met. This allows one to implement legal obligations and
commitments in terms of the future execution of a (state-aware) computation at
a specific point in time.

A third peculiarity of _Stipula_ is the _agreement operator_ , which marks
that the contract’s parties have reached a consensus on the contractual
arrangement they want to create. In legal contracts, this phase corresponds to
the subscription of the contract, where there are parties that are going to
set the contractual conditions and others that accept them. Technically, the
operation is a multiparty synchronization, which may be implemented by ad-hoc
protocols in many kinds of distributed systems.

The fourth key feature regards _assets_ , which are first-class linear
concepts in _Stipula_. In particular, _Stipula_ has an explicit, and thus
conscious, management of linear resources, such as currency-like values and
tokens. The transfer of such resources must preserve the total supply: the
sender of the asset must always relinquish the control of the transferred
asset. These assets are necessary in legal contracts: currency is required for
payment but also for escrows, and tokens, both fungible and non-fungible, are
useful to model securities and provide a digital handle on a physical good
(possibly equipped with and IoT mechanism). The design choice of explicitly
marking asset movements with an ad hoc syntax in _Stipula_ promotes a safer,
asset-aware, programming discipline that reduces the risk of the so-called
double spending, the accidental loss or the locked-in assets. This is
particularly useful for legal contracts running over a blockchain, where many
kinds of assets and tokens are pervasive in the most successful blockchain
applications and their induced economy. Therefore, _Stipula_ uses a simple and
powerful core of primitives that support the writing of digital legal
contracts even by non ICT experts.

In Section 2 we give an interdisciplinary discussion about smart legal
contracts, focusing on the interlace between the digital and legal elements
required by the digitalization of juridical acts. The syntax of _Stipula_ is
formally defined in Section 3 where a simple example – the Bike-Rental
contract – is used to describe the concepts. _Stipula_ semantics is defined in
Section 4, sticking to an operational approach that specifies the runtime
behaviour of legal contracts by means of transitions. In Section 5, following
a standard technique in concurrency theory [20], we develop an observational
equivalence that provides for an equational theory of smart legal contracts.
The equivalence is based on a notion of _bisimulation_ that equates contracts
differing for hidden elements, such as names of states, and singles out
conditions for identifying contracts that send two assets in different order.
The study of the implementation of the distinctive elements of _Stipula_ ,
namely agreements, assets and events, either on a blockchain system, using a
Solidity-like target language, or not, is undertaken in Section 6. The
specification in _Stipula_ of a set of archetypal acts, ranging from renting
to (digital) licenses and to bets, is reported in Section 7

We end our contribution by discussing the related work in Section 8 and
delivering our final remarks in Section 9.

##  2 Smart Legal contracts

A substantial debate has taken place on whether the parties’ decision to
execute a smart contract having certain computational effects may count as
legal contract establishing corresponding legal effect, _e.g._ [13, 17, 19,
21]. A simple answer to this question comes from the principle of “ _freedom
of form_ ” in contracts, which is shared by modern legal systems: _parties are
free to express their agreement using the language and medium they prefer,
including a programming language_. Therefore, by this principle, smart
contracts may count as legal contracts.

However, the problem is whether smart contracts preserve the essential
elements of legal ones. In this respect, a legal contract is meant to bring
about the _institutional effects_ intended by the parties, that is
establishing new obligations, rights, powers and liabilities between them or
to transfer rights (such as rights to property) from one party to the other.
These institutional effects are guaranteed by the possibility of activating
judicial enforcements. That is, each party may start a lawsuit if he believes
that the other party has failed to comply with the contract. In this case, the
judge will have to interpret the contract, ascertain the facts of the case,
and determine whether there has indeed been a contractual violation.
Accordingly, the defaulting party may be enjoined to comply or pay damages.
Whether and to what extent we may consider that a smart contract produces
judicially enforceable legal effects is more debatable, given that smart
contract modify especially in absence of international technical standards and
transnational legal frameworks.

We recognise that no easy and comprehensive solution is yet at hand for the
issue we have just mentioned. However, we believe that it can be at least
mitigated if a strict, and understandable mapping is established between
executable instructions and institutional-normative effects. To this aim, we
observe that the lifecycle of a legal contract goes through a number of
phases: (_a_) formation and negotiation, (_b_) contract storage/notarizing,
(_c_) performance, enforcement and monitoring, (_d_) possible modification
(_e_) dispute resolution, and (_f_) termination. Software-based solutions can
be valuable in all these phases, additionally, the specific features of
blockchain-based implementations make them convenient in some of them. For
example, the negotiation of contractual conditions could benefit from
software-mediated interactions, but might require a degree of privacy that
conflicts with that of a public blockchain, which naturally runs on
transnational infrastructures, thus crossing several, possibly different,
legal systems and jurisdictions (_c.f._ General Data Protection Regulation is
valid only in Europe). Similarly the dispute resolution can take advantage of
online services with flexible interfaces, since it can hardly be fully
programmed nor ported on-chain. Exceptional behaviors, such as mutual or
unilateral dissent, contract termination or contract modifications matching a
change in the parties’ will, are also very problematic and require a flexible
programming style that admits suitable patterns to amend the behaviour of a
running software.

On the other hand, software-based solutions, possibly based on the blockchain,
are perfectly suited to phases (_b_) and (_c_). Both the content of the legal
contract and the expression of agreement of the parties can be digitally
notarized, and code can be used to express the contractual clauses and
automatically enforce them through the runtime execution. Additionally,
encoding legal contracts as software has the advantage of enabling the usage
of verification (formal) methods to ensure the correctness of the software
execution.

Nevertheless, if smart contracts are legally binding, then it is necessary to
ensure that the parties are fully aware of the computational effects of their
code. Only in this case, there may be a genuine agreement over the content of
the contract. Thus transparency and some degree of readability by contractors
that have no or little computer expertise becomes a key requirement. Relating
to this point, we acknowledge that similar problems also exist in natural
language contracts, which are usually signed without the parties being aware
of all of their clauses and judicial enforcement being too costly or complex
to be practicable. Usually, when concluding online purchases of goods or
services, most consumers just click the “accept” button, without even trying
to read the clauses (which are often lengthy and full of legal jargon).

We believe that _Stipula_ provides some important advantages as a language for
specifying smart legal contracts. Its primitives are concise and abstract
enough to be easily accessible to lawyers. Its formal operational semantics
promises that the execution of contracts does not lead to unexpected
behaviours and is amenable to automatic verification. To mention a distinctive
feature of _Stipula_ , the agreement primitive helps to deal with some legal
issues, since it clearly identifies the moment when (some) legal effects are
triggered and the parties who are involved. For instance, the set of parties
involved in the agreement might include an Authority that is charged to
monitor contextual constraints, such as obligations of diligent storage and
care, or the obligations of using goods only as intended, taking care of
litigations and dispute resolution. Moreover, untrusted players involved in a
bet contract can rely on the agreement to explicitly define the data source
providing the outcome of the aleatory value associated to the bet.

##  3 The _Stipula_ language

⬇ F $::=$ _ $|$ @Q $\texttt{A}:$ f($\overline{\tt z}$)[$\overline{\tt y}$]
(B){ S W }$\,\Rightarrow\,$@$\texttt{Q}^{\prime}\;$ F S $::=$ _ $|$ E
$\rightarrow$ x S $|$ E $\multimap$ h,h′ S $|$ E $\rightarrow$ A S $|$ E
$\multimap$ h,A S $|$ (B){ S } S W $::=$ _ $|$ E$\,\gg\,$@Q { S
}$\,\Rightarrow\,$@$\texttt{Q}^{\prime}\;\;$ W E $::=$ now $|$ Real $|$ String
$|$ B $|$ X $|$ E op E B $::=$ true $|$ false $|$ E rop E $|$ B
$\mathbin{\binampersand}\mathbin{\binampersand}$ B $|$ B || B $|$ ~B
---
Table 1:  Syntax of _Stipula_.

_Stipula_ features a minimal set of primitives that are primary in legal
contracts, such as agreements, field updates, conditional behaviour, timed
events, value and asset transfer, functions and states like Finite State
Machines (FSMs).

We use countable sets of: _contract names_ , ranged over by C, $\mbox{{\tt
C}}^{\prime}$, $\cdots$; names of externally owned accounts, called  _parties_
, ranged over by $A$, $A^{\prime}$, $\cdots$; _function names_ ranged over f,
g, $\cdots$. Parties represent the users involved in the contract, _i.e._
authenticated users in centralized systems (or addresses in blockchain
systems). _Assets_ and generic contract’s _fields_ are syntactically set apart
since they have different semantics. Then we assume a countable set of _asset
names_ , ranged over by h, $\texttt{h}^{\prime}$, $\cdots$, and a set of
_field names_ , ranged over x, $\texttt{x}^{\prime}$, $\cdots$. We reserve z,
z′, y, y′, for function parameters and $\texttt{A},\texttt{A}^{\prime},\cdots$
for parameters that are parties. Finally, we will use Q,
$\texttt{Q}^{\prime}$, $\cdots$, to range over contract states. To simplify
the syntax, we often use the vector notation ${\overline{x}}$ to denote
possibly empty sequences of elements. A smart legal contract in _Stipula_ is
written

⬇

stipula C {

assets ${\overline{\tt h}}$

fields $\overline{\tt x}$

agreement($\overline{\tt A}$)(${\overline{\tt x}^{\prime}}$){ //
$\overline{\tt x}^{\prime}\subseteq{\overline{\tt x}}$

$\overline{{\tt A}_{1}}$ : $\overline{\tt x}_{1}$

$\cdots$

$\overline{{\tt A}_{n}}$ : $\overline{\tt x}_{n}$ // $\bigcup_{i\in
1..n}\overline{{\tt A}_{i}}\subseteq\overline{{\tt A}}\qquad\bigcup_{i\in
1..n}\overline{{\tt x}_{i}}\subseteq\overline{{\tt
x}^{\prime}}\qquad\bigcap_{i\in 1..n}\overline{{\tt x}_{i}}=\varnothing$

} $\Rightarrow$ @Q

F

}

where C identifies the contract; its body contains assets and fields (without
any typed information: _Stipula_ is type-free), the _agreement code_ , where
$\bigcup_{i\in 1..n}\overline{{\tt x}_{i}}$ is a partition of $\overline{{\tt
x}^{\prime}}$ while the sequences of parties $\overline{{\tt A}_{i}}$ are
subsets of the full list $\overline{\tt A}$ of parties involved in the
contract C. Finally, F is a sequence of functions, written according to the
syntax given in Table 1.

The definition of _who_ is going to participate to the contract and _what_ are
the terms of the contract in an explicit abstraction – the _agreement_ – is
another distinctive feature of _Stipula_. Technically, the agreement is the
_constructor_ of the contract, that specifies the parameters $\overline{\tt
x^{\prime}}$, i.e., the terms of the contract, and the set $\overline{\tt A}$
of involved parties. Moreover, the code specifies who must agree on the
initial value of contract’s fields and the initial state of the contract.
Observe that no asset can be set during the agreement. It is assumed that
fields, assets and parties’ names do not contain duplicates.

The dichotomy between assets and fields is a key design choice of _Stipula_.
Indeed, the relevance of first-class resources, _i.e._ linear values that
cannot be copied nor dismissed, is widely acknowledged in several programming
languages (such as Rust or the smart contract languages Move [12] and Nomos
[11]) to support a safer asset-aware contract programming. Legal contracts
also manage assets, such as money and tokens granting a digital access to
(possibly physical) goods or services. Henceforth the decision to
syntactically highlight the differences between operations on values and on
assets.

Functions F and their bodies are written according to the syntax in Table 1.
The function’s syntax highlights the constraint that only the party A can
invoke the function f, and only when the contract is in state Q. Function’s
parameters are split in two lists: the _formal parameters_ $\overline{\tt z}$
in brackets and the _asset parameters_ $\overline{\tt y}$ in square brackets.
The _precondition_ (B) is a predicate on parameters of the functions and
fields and assets of the contract that constrains the execution of the body of
f. Finally the _body_ {S W} $\Rightarrow$ @Q′ specifies the _statement part_
S, the _event part_ W, and the state $\texttt{Q}^{\prime}$ of the contract
when the function execution terminates. Function’s parameters are assumed
without duplicates, and empty lists of (asset) parameters are shortened by
omitting empty parenthesis. Additionally we assume that function parameters
$\overline{\tt z}$ and $\overline{\tt y}$ do not occur in W to enforce that it
is correctly executed outside the scope of the function.

_Statements_ S include the empty statement -- and different types of
assignments, followed by a continuation. Assignments use the two symbols
$\multimap$ and $\rightarrow$ to differentiate updates of assets and of
fields, respectively. The syntax of the two operators is taken from [11].
Assignments can be either _local_ , that is referring to local fields or local
assets, denoted by E $\rightarrow$ x and E $\multimap$ h,h′, respectively, or
they can be _remote_ , denoted by E $\rightarrow$ A and E $\multimap$ h,A,
defining the sending of a value and an asset, respectively, to the address A.
Asset assignments are ternary operations: the meaning of E $\multimap$ h,h′ is
that the value of E is subtracted to the asset h and added to the asset h′ –
_resources stored in assets can be moved but cannot be destroyed_. The
operational semantics will ensure that asset assignments can at most drain an
asset, preventing assets with negative values. In the rest of the paper we
will always abbreviate assignments such as h $\multimap$ h,h′ and h
$\multimap$ h,A′ (which are very usual, indeed) into h $\multimap$ h′ and h
$\multimap$ A′, respectively. Statements also include _conditionals_ (B){ S }
S′ that executes S if the predicate B is true and continues as S′.

_Events_ W are sequences of _timed continuations_ that schedule some code for
future execution. More precisely, the term E $\gg$ @Q {S} $\Rightarrow$ @Q′
schedules an execution that is triggered at a time $\mathbb{t}$ that is the
value of E. When triggered, the continuation S will be executed only if the
contract’s state is Q. At the end of the execution of S, the contract transits
to Q′. That is, in _Stipula_ , the programming abstractions of FSMs are used
to schedule the future execution of a (state-aware) computation at a specific
point in time. We will show that this notion of events is pivotal in the
encoding of legal obligations and commitments.

_Expressions_ E can be Real (written with the fixed-point notation), String
(written between “"”), names of assets, fields and parameters, generically
ranged over by X. Expressions also include boolean values and boolean
expressions B. The keyword now, expressed as a real, stores the present time
(when the code is executed). We will range over constant _values_ with the
names $u,v,\cdots$; they also include asset constants like tokens. We will be
a little liberal with values and operations, generically denoted by E op E:
they include standard arithmetic operations and operations on tokens, _e.g._
use_once(token) generates a usage-code providing a single access to the
service or the good associated to the token asset. The operation $\mathbb{t}$
\+ n sums n seconds to the time value $\mathbb{t}$. _Boolean expressions_ B
are the standard ones, where the operations rop are the relational operations
(==, >=, etc.) The set of names occurring in E will be noted by $\mbox{{\em
fv}}(\mbox{\tt E})$.

A _Stipula_ program $\mathcal{P}$ is a sequence of smart legal contracts
definitions. The contracts are inactive as long as no group of addresses has
interest to run them, by invoking the agreement code. We remark that in
_Stipula_ the code of a contract cannot invoke another contract: we postpone
to future work the study of language extensions allowing cross references
between legal contracts using inheritance and composition. Therefore, at the
moment, since legal contracts are independent, there is no loss of generality
in considering a program to be composed by a single smart legal contract
definition.

#### Example

Consider the following simple contract for renting bikes:

⬇

1stipula Bike_Rental {

2 assets wallet

3 fields cost, rent_time, use_code

4

5 agreement (Lender, Borrower)(cost, rent_time) {

6 Lender, Borrower : cost, rent_time

7 } $\Rightarrow$ @Inactive

8

9 @Inactive Lender : offer (z) {

10 z $\rightarrow$ use_code

11 } $\Rightarrow$ @Proposal

12

13 @Proposal Borrower : accept [y]

14 (y == cost) {

15 y $\multimap$ wallet

16 use_code $\rightarrow$ Borrower

17 now + rent_time $\gg$

18 @Using { //end-of-time usage

19 "End_Reached" $\rightarrow$ Borrower

20 wallet $\multimap$ Lender

21 } $\Rightarrow$ @End

22 } $\Rightarrow$ @Using

23

24 @Using Borrower : end {

25 wallet $\multimap$ Lender

26 } $\Rightarrow$ @End

27}

Listing 1: The rent for free contract

The agreement code specifies that there are two parties – the Lender and
Borrower – and that the Lender sets the values for the time of usage
(rent_time) and the cost, while the Borrower has to agree on such values. Then
Lender sends a use-code that is stored in the contract (in the use_code field)
and is not accessible to Borrower till he pays for the usage. The transition
from Inactive to Proposal at the end of the offer function enables the
Borrower to pay for the usage – function accept – that takes in input an asset
y and moves it into wallet with y $\multimap$ wallet at line 15 (this is a
shortening for wallet $\multimap$ wallet, Borrower). Then the contract sends
the use-code to the borrower (line 16), which now can use the bike till the
time limit. This constraint is expressed by the event in lines 17-21. We have
two remarks: first, the payment is not made to Lender but the asset is stored
in the contract (in wallet); second, the event will be triggered when the time
expires. In this case a message to Borrower is sent, the payment is
transferred to Lender, which will change bike’s use code so that the bike will
be locked at the next Borrower’s stop. The function end can be invoked by
Borrower to terminate the renting before time expires. The legal issues
involved in a rent contract will be discussed in Section 7.

##  4 Semantics

The meaning of _Stipula_ primitives is defined in an operational way by means
of a transition relation. Let $\mbox{{\tt
C}}(\Phi\mathrel{,}\ell\mathrel{,}\Sigma\mathrel{,}\Psi)$ be a _runtime
contract_ where

  * •

C is the contract name;

  * •

$\Phi$ is the current state of the contract: it is either -- (for no state)
or a contract state Q;

  * •

$\ell$ is a mapping from fields and assets to values;

  * •

$\Sigma$ is a possible residual of a function body or of an event handler,
_i.e._ $\Sigma$ is either -- or a term $\texttt{S}\
\texttt{W}\Rightarrow\texttt{@}\texttt{Q}$;

  * •

$\Psi$ is a (possibly empty) multiset of _pending events_ that have been
already scheduled for future execution but not yet triggered. We let $\Psi$ be
-- when there are no pending events, otherwise
$\Psi=\texttt{W}_{1}~{}|~{}\ldots~{}|~{}\texttt{W}_{n}$ such that each Wi is a
single event expression (not a sequence), and its _time guard_ is an
expression that has already been evaluated into a time value $\mathbb{t}_{i}$.

Runtime contracts are ranged over by $\mathbb{C}$, $\mathbb{C}^{\prime}$,
$\cdots$. A _configuration_ , ranged over by $\mathbb{S}$,
$\mathbb{S}^{\prime}$, $\cdots$, is a pair
$\mathbb{C}{\mathrel{\mbox{\tt,}}}\mathbb{t}$, where $\mathbb{t}$ is a global
clock. As anticipated, there is no loss of generality in considering programs
made of a single running contract; a remark about the extension to
configurations containing several contracts is reported at the end of the
section.

The transition relation of a _Stipula_ program $\mathcal{P}$ is
$\mathbb{S}\mathrel{\stackrel{{\scriptstyle\mu}}{{\longrightarrow}}}_{\mathcal{P}}\mathbb{S}^{\prime}$,
where

$\mu\quad::=\quad\\_\quad|\quad(\overline{A},\,{\overline{A}_{1}}:\overline{v}_{1},\cdots,{\overline{A}_{n}}:\overline{v}_{n})\quad|\quad
A:\texttt{f}(\overline{u})[\overline{v}]\quad|\quad v\rightarrow A\quad|\quad
v\multimap A$

that is the label $\mu$ is either empty, or denotes an initial agreement, or a
function call, or a value send, or an asset transfer. In the following we will
always omit the index $\mathcal{P}$ because it is considered implicit. The
formal definition of
$\mathbb{S}\mathrel{\stackrel{{\scriptstyle\mu}}{{\longrightarrow}}}\mathbb{S}^{\prime}$
is given in Table 2, using the following auxiliary predicates and functions:

  * •

$\llbracket\texttt{E}\rrbracket_{\ell}$ is a function that returns the value
of E in the memory $\ell$. We omit the definition.

  * •

$\llbracket\texttt{W}\rrbracket_{\ell}$ is the multiset of scheduled events
obtained from the sequence W by replacing every time expression by its value
in the time guards. That is
$\llbracket\mbox{\raisebox{-2.58334pt}{{\tt-\\!\\!\\!-}}}\rrbracket_{\ell}=\mbox{\raisebox{-2.58334pt}{{\tt-\\!\\!\\!-}}}$
and
$\llbracket\texttt{E}\gg\texttt{@}\texttt{Q}\\{\texttt{S}\\}\Rightarrow\texttt{@}\texttt{Q}^{\prime}\
\
\texttt{W}^{\prime}\rrbracket_{\ell}=\llbracket\texttt{E}\rrbracket_{\ell}\gg\texttt{@}\texttt{Q}\\{\texttt{S}\\}\Rightarrow\texttt{@}\texttt{Q}^{\prime}~{}|~{}\llbracket\texttt{W}^{\prime}\rrbracket_{\ell}$.

  * •

Let $\Psi$ be a multiset of pending events, and $\mathbb{t}$ a time value,
then the predicate $\Psi\mathrel{\mbox{\tt,}}\mathbb{t}\mathrel{\nrightarrow}$
is _true_ whenever
$\Psi=\mathbb{t}_{1}\gg\texttt{@}\texttt{Q}_{1}\\{\texttt{S}_{1}\\}\Rightarrow\texttt{@}\texttt{Q}_{1}^{\prime}~{}|~{}\cdots~{}|~{}\mathbb{t}_{n}\gg\texttt{@}\texttt{Q}_{n}\\{\texttt{S}_{1}\\}\Rightarrow\texttt{@}\texttt{Q}_{n}^{\prime}$
and, for every $1\leq i\leq n$, $\mathbb{t}_{i}\neq\mathbb{t}$, _false_
otherwise.

$\begin{array}[]{c}\begin{array}[]{l}\mbox{\tiny[{\sc Agree}]}\\\
\frac{{}^{\textstyle\begin{array}[]{c}\texttt{agreement(}\overline{\tt
A}\texttt{)(}\overline{\tt x}\texttt{)\\{ }\overline{\tt A}_{1}:\overline{\tt
x}_{1}\ \cdots\ \overline{\tt A}_{n}:\overline{\tt x}_{n}\
\\}\Rightarrow\texttt{@}\texttt{Q}\ \in\;\mbox{{\tt
C}}\end{array}}}{{}_{\textstyle\mbox{{\tt
C}}(\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}}\mathrel{,}\emptyset\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}}\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}})\mathrel{\mbox{\tt,}}\mathbb{t}\mathrel{\stackrel{{\scriptstyle(\overline{A},\,{\overline{A}_{i}}{:}\overline{v}_{i}\
^{i=1...n})}}{{\longrightarrow}}}\mbox{{\tt
C}}(\texttt{Q}\mathrel{,}[{\overline{\tt
A}}\mapsto{\overline{A}},\overline{\tt x}_{i}~{}\mapsto~{}\overline{v}_{i}\
^{i=1...n}]\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}}\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}})\mathrel{\mbox{\tt,}}\mathbb{t}}}\end{array}\\\\[8.5359pt]
\begin{array}[]{l}\mbox{\tiny[{\sc Function}]}\\\
\frac{{}^{\textstyle\begin{array}[]{c}\texttt{@}\texttt{Q}~{}\texttt{A}~{}\texttt{:~{}f(}\overline{\mbox{{\tt
z}}}\texttt{)[}\overline{\mbox{{\tt y}}}\texttt{] (B) \\{ S~{}W
\\}}\Rightarrow\texttt{@}\texttt{Q}^{\prime}\in\mbox{{\tt C}}\\\
\Psi\mathrel{\mbox{\tt,}}\mathbb{t}\mathrel{\nrightarrow}\\\
\ell(\texttt{A})=A\quad\ell^{\prime}=\ell[\overline{\mbox{{\tt
z}}}\mapsto\overline{u},\overline{\mbox{{\tt
y}}}\mapsto\overline{v}]\quad\llbracket\texttt{B}\rrbracket_{\ell^{\prime}}={\it
true}\end{array}}}{{}_{\textstyle\mbox{{\tt
C}}(\texttt{Q}\mathrel{,}\ell\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}}\mathrel{,}\Psi)\mathrel{\mbox{\tt,}}\mathbb{t}\mathrel{\stackrel{{\scriptstyle
A:\texttt{f}(\overline{u})[\overline{v}]}}{{\longrightarrow}}}\mbox{{\tt
C}}(\texttt{Q};\ell^{\prime}\mathrel{,}\texttt{S}\,\texttt{W}\Rightarrow\texttt{@}\texttt{Q}^{\prime}\mathrel{,}\Psi)\mathrel{\mbox{\tt,}}\mathbb{t}}}\end{array}\quad\begin{array}[]{l}\mbox{\tiny[{\sc
State Change}]}\\\
\frac{{}^{\textstyle\llbracket\texttt{W}\\{^{\mathbb{t}}/_{\texttt{now}}\\}\rrbracket_{\ell}=\Psi^{\prime}}}{{}_{\textstyle\mbox{{\tt
C}}(\texttt{Q}\mathrel{,}\ell\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}}\,\texttt{W}\Rightarrow\texttt{@}\texttt{Q}^{\prime}\mathrel{,}\Psi)\mathrel{\mbox{\tt,}}\mathbb{t}\mathrel{\stackrel{{\scriptstyle}}{{\longrightarrow}}}\mbox{{\tt
C}}(\texttt{Q}^{\prime}\mathrel{,}\ell\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}}\mathrel{,}\Psi^{\prime}~{}|~{}\Psi)\mathrel{\mbox{\tt,}}\mathbb{t}}}\end{array}\par\\\\[28.45274pt]
\begin{array}[]{l}\mbox{\tiny[{\sc Event Match}]}\\\
\frac{{}^{\textstyle\begin{array}[]{c}\Psi=\mathbb{t}\gg\texttt{@}\texttt{Q}~{}\\{~{}\texttt{S}~{}\\}\Rightarrow\texttt{@}\texttt{Q}^{\prime}~{}|~{}\Psi^{\prime}\end{array}}}{{}_{\textstyle\mbox{{\tt
C}}(\texttt{Q}\mathrel{,}\ell\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}}\mathrel{,}\Psi)\mathrel{\mbox{\tt,}}\mathbb{t}\mathrel{\stackrel{{\scriptstyle}}{{\longrightarrow}}}\mbox{{\tt
C}}(\texttt{Q}\mathrel{,}\ell\mathrel{,}\texttt{S}\Rightarrow\texttt{@}\texttt{Q}^{\prime}\mathrel{,}\Psi^{\prime})\mathrel{\mbox{\tt,}}\mathbb{t}}}\end{array}\qquad\begin{array}[]{l}\mbox{\tiny[{\sc
Tick}]}\\\
\frac{{}^{\textstyle\Psi\mathrel{\mbox{\tt,}}\mathbb{t}\mathrel{\nrightarrow}}}{{}_{\textstyle\mbox{{\tt
C}}(\texttt{Q}\mathrel{,}\ell\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}}\mathrel{,}\Psi)\mathrel{\mbox{\tt,}}\mathbb{t}\mathrel{\stackrel{{\scriptstyle}}{{\longrightarrow}}}\mbox{{\tt
C}}(\texttt{Q}\mathrel{,}\ell\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}}\mathrel{,}\Psi)\mathrel{\mbox{\tt,}}\mathbb{t}+1}}\end{array}\\\
\\\ \begin{array}[]{l}\mbox{\tiny[{\sc Value\\_Send}]}\\\
\frac{{}^{\textstyle\llbracket\texttt{E}\rrbracket_{\ell}=v\quad\ell(\texttt{A})=A}}{{}_{\textstyle\mbox{{\tt
C}}(\texttt{Q}\mathrel{,}\ell\mathrel{,}\texttt{E}\rightarrow\texttt{A}~{}\Sigma\mathrel{,}\Psi)\mathrel{\stackrel{{\scriptstyle
v\rightarrow A}}{{\longrightarrow}}}\mbox{{\tt
C}}(\texttt{Q}\mathrel{,}\ell\mathrel{,}\Sigma\mathrel{,}\Psi)}}\end{array}\quad\begin{array}[]{l}\mbox{\tiny[{\sc
Asset\\_Send}]}\\\
\frac{{}^{\textstyle\llbracket\texttt{E}\rrbracket_{\ell}=v\quad\ell(\texttt{h})\geq
v\quad\ell(\texttt{A})=A}}{{}_{\textstyle\mbox{{\tt
C}}(\texttt{Q}\mathrel{,}\ell\mathrel{,}\texttt{E}\multimap\texttt{h,}\texttt{A}~{}\Sigma\mathrel{,}\Psi)\mathrel{\stackrel{{\scriptstyle
v\multimap A}}{{\longrightarrow}}}\mbox{{\tt
C}}(\texttt{Q}\mathrel{,}\ell[\texttt{h}\mapsto\ell(\texttt{h})-v]\mathrel{,}\Sigma\mathrel{,}\Psi)}}\end{array}\\\\[17.07182pt]
\begin{array}[]{l}\mbox{\tiny[{\sc Field\\_Update}]}\\\
\frac{{}^{\textstyle\llbracket\texttt{E}\rrbracket_{\ell}=v}}{{}_{\textstyle\mbox{{\tt
C}}(\texttt{Q}\mathrel{,}\ell\mathrel{,}\texttt{E}\rightarrow\texttt{x}~{}\Sigma\mathrel{,}\Psi)\mathrel{\stackrel{{\scriptstyle}}{{\longrightarrow}}}\mbox{{\tt
C}}(\texttt{Q}\mathrel{,}\ell[\texttt{x}\mapsto
v]\mathrel{,}\Sigma\mathrel{,}\Psi)}}\end{array}\quad\begin{array}[]{l}\mbox{\tiny[{\sc
Asset\\_Update}]}\\\
\frac{{}^{\textstyle\llbracket\texttt{E}\rrbracket_{\ell}=v\qquad\ell(\texttt{h})\geq
v}}{{}_{\textstyle\begin{array}[]{l}\mbox{{\tt
C}}(\texttt{Q}\mathrel{,}\ell\mathrel{,}\texttt{E}\multimap\texttt{h,h}^{\prime}~{}\Sigma\mathrel{,}\Psi)\\\
\qquad\mathrel{\stackrel{{\scriptstyle}}{{\longrightarrow}}}\mbox{{\tt
C}}(\texttt{Q}\mathrel{,}\ell[\texttt{h}\mapsto\ell(\texttt{h})-v,\texttt{h}^{\prime}\mapsto\ell(\texttt{h}^{\prime})+v]\mathrel{,}\Sigma\mathrel{,}\Psi)\end{array}}}\end{array}\\\\[17.07182pt]
\begin{array}[]{l}\mbox{\tiny[{\sc Cond\\_true}]}\\\
\frac{{}^{\textstyle\llbracket\texttt{B}\rrbracket_{\ell}={\it
true}}}{{}_{\textstyle\mbox{{\tt
C}}(\texttt{Q}\mathrel{,}(\texttt{B})\\{\texttt{S}\\}~{}\Sigma\mathrel{,}\Psi)\mathrel{\stackrel{{\scriptstyle}}{{\longrightarrow}}}\mbox{{\tt
C}}(\texttt{Q}\mathrel{,}\ell\mathrel{,}\texttt{S}~{}\Sigma\mathrel{,}\Psi)}}\end{array}\qquad\begin{array}[]{l}\mbox{\tiny[{\sc
Cond\\_false}]}\\\
\frac{{}^{\textstyle\llbracket\texttt{B}\rrbracket_{\ell}={\it
false}}}{{}_{\textstyle\mbox{{\tt
C}}(\texttt{Q}\mathrel{,}(\texttt{B})\\{\texttt{S}\\}~{}\Sigma\mathrel{,}\Psi)\mathrel{\stackrel{{\scriptstyle}}{{\longrightarrow}}}\mbox{{\tt
C}}(\texttt{Q}\mathrel{,}\ell\mathrel{,}\Sigma\mathrel{,}\Psi)}}\end{array}\\\
\\\ \end{array}$ Table 2:  The transition relation of _Stipula_

Rule [Agree] in Table 2 establishes the agreement of the parties involved in
the contract. This operation is a multiparty synchronization, where some
parties, namely $\overline{A}_{i}$, agree on the initial values
$\overline{v}_{i}$ of the contract’s fields $\overline{\texttt{{x${}_{i}$}}}$,
for $i\in 1,..n$. The resulting configuration moves the contract to the
initial state Q and initializes the values of the parties parameters
$\overline{\tt A}$ and the contract’s fields $\overline{\tt x}$. We recall the
syntactic conditions of the agreement term, given in the previous section:
$(i)$ the sequence $\overline{\tt x}$ is a subset of the contract’s fields,
$(ii)$ $\bigcup_{i\in 1..n}\overline{{\tt x}_{i}}$ is a partition of
$\overline{{\tt x}}$ and $(iii)$ the sequences of parties $\overline{{\tt
A}_{i}}$ are subsets of the full list $\overline{\tt A}$.

Rule [Function] defines function invocations; the label specifies the address
$A$ performing the invocation and the function name f with the actual
parameters. The transition may occur provided (_i_) the contract is the state
Q that admits invocations of f from $A$ and (_ii_) the contract is _idle_ ,
_i.e._ the contract has no statement to execute – _c.f._ the left-hand side
runtime contract – (_iii_) the precondition B is satisfied, and no event can
be triggered – _c.f._ the premise
$\Psi\mathrel{\mbox{\tt,}}\mathbb{t}\mathrel{\nrightarrow}$. In particular,
this last constraint expresses that events _have precedence_ on possible
function invocations. For example, if a payment deadline is reached and, at
the same time, the payment arrives, it will be refused in favour of the event
managing the deadline.

Rule [State Change] says that a contract changes state when the statements
execution terminates and the sequence of events W is added to the multiset of
pending events, up to the evaluations of their time expressions, _i.e._ the
occurrences of the identifier now are replaced by the current value of the
clock.

Rule [Event Match] specifies that event handlers may run provided there is no
statement to perform in the runtime contract, and the time guard of the event
has exactly the value of the global clock $\mathbb{t}$. Observe that the
timeouts of the events are evaluated in an eager way when the event is
scheduled – _c.f._ rule [State Change] – not when the event handler is
triggered. Moreover, the state change performed at the end of the execution of
the event handler is carried over again by the rule [State Change], with an
empty sequence W.

Rule [Tick] models the elapsing of time. This happens when the contract has no
statement to perform and no event can be triggered. Intuitively, the
implementation of _Stipula_ on top of a blockchain will bind the global clock
to the timestamp of the current block. Therefore a sequence of semantic
transitions performed in the same unit of time will correspond to a set of
transactions inserted into the same block to be appended to the blockchain.

It is worth to notice that the foregoing rules imply that the complete
execution of a function call does not affect the global time. This admits the
paradoxical phenomenon that an endless sequence of function invocations does
not make time elapse. While this is possible in theory, it is not in practice,
since blocks can only include a finite number of transactions. Additionally,
all the legal contracts we have analyzed are finite state, each state admits a
single function invocation, and function invocations update the state in a
noncircular way, thus preventing infinite sequence of function calls. An
alternative choice would be to adjust the semantics so to increment the clock
every time a maximal number of functions has been evaluated, thus forcing each
block to contain at most a limited number of function invocations. We have
preferred to stick to the simpler semantics.

Table 2 defines transitions due to the execution of statements. All these
transitions are local to the runtime contract and time does not change.
Therefore, for simplicity, we always omit the clock. We only discuss
[Asset_Send] and [Asset_Update] because the other rules are standard. Rule
[Asset_Send] returns part of an asset h to the party $A$. This part, named
$v$, is removed from the asset, _c.f._ the memory of the right-hand side
runtime contract in the conclusion. In a similar way, [Asset_Update] moves a
part $v$ of an asset h to an asset $\texttt{h}^{\prime}$. For this reason, the
final memory becomes
$\ell[\texttt{h}\mapsto\ell(\texttt{h})-v,\texttt{h}^{\prime}\mapsto\ell(\texttt{h}^{\prime})+v]$.
We observe that assets, representing physical entities (coins, houses, goods,
etc.) are never destroyed. The condition $\ell(\texttt{h})\geq v$ in the
premises ensures that assets can never become negative.

The semantics of _Stipula_ does not consider runtime errors, for instance an
attempt to drain too much value from an asset results in a stuck
configuration. We postpone to future work a precise account of runtime
failures and contract errors, since it requires a deep interdisciplinary
analysis of the legal issues involved in the execution of the exceptional
cases.

The initial configuration of a _Stipula_ program $\mathcal{P}$ made of a
single contract C is $\mbox{{\tt
C}}(\mbox{\raisebox{-2.58334pt}{{\tt-\\!\\!\\!-}}}\mathrel{,}\varnothing\mathrel{,}\mbox{\raisebox{-2.58334pt}{{\tt-\\!\\!\\!-}}}\mathrel{,}\mbox{\raisebox{-2.58334pt}{{\tt-\\!\\!\\!-}}})\mathrel{\mbox{\tt,}}\mathbb{t}$.
The contract is _inactive_ as long as no group of addresses has interest to
run it, _c.f._ rule [Agree]. The global clock can be any value, because it
corresponds to the absolute time, defined by the timestamp of the current
block in the blockchain system.

#### Example

Possible initial transitions of the Bike_Rental contract in Example 3 are
reported in Table 3. We assume that the actual names of parties are the same
as the formal names (therefore we omit the mappings in the memories). Let be
$\mu_{0}=((\mathit{Alice,Bob}),(\mathit{Alice,Bob}):(36000,2))$, _i.e._ Alice
and Bob agree about renting a bike for 2 euro for 1 hour – the time is
measured in seconds. Let also be
$\ell=[\texttt{Lender}\mapsto\mathit{Alice},\texttt{Borrower}\mapsto\mathit{Bob},\texttt{cost}\mapsto
2,\texttt{time\\_limit}\mapsto 3600]$, and
$\ell^{\prime}=\ell[z\mapsto\mbox{{\tt 123}},\mbox{{\tt
use\\_code}}\mapsto\mbox{{\tt 123}}]$ and S W be the body of the function
accept.

$\mbox{{\tt
Bike\\_Rental}}(\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}}\mathrel{,}\emptyset\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}}\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}})\mathrel{\mbox{\tt,}}\texttt{0}$

$\begin{array}[]{r@{\\!}clr}&\mathrel{\stackrel{{\scriptstyle\mu_{0}}}{{\longrightarrow}}}&\mbox{{\tt
Bike\\_Rental}}(\texttt{Inactive}\mathrel{,}\ell\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}}\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}})\mathrel{\mbox{\tt,}}\texttt{0}&\mbox{{\small{\sc[Agree]}}}\\\
&\mathrel{\stackrel{{\scriptstyle}}{{\longrightarrow}}}&\mbox{{\tt
Bike\\_Rental}}(\texttt{Inactive}\mathrel{,}\ell\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}}\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}})\mathrel{\mbox{\tt,}}\texttt{1}&\mbox{{\small{\sc[Tick]}}}\\\
&\mathrel{\stackrel{{\scriptstyle\mathit{Alice}\texttt{:offer(123)}}}{{\longrightarrow}}}&\mbox{{\tt
Bike\\_Rental}}(\texttt{Inactive}\mathrel{,}\ell[z\mapsto\mbox{\tt
123}]\mathrel{,}z\rightarrow\mbox{{\tt
use\\_code}}\Rightarrow\mbox{{\tt@Proposal}}\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}})\mathrel{\mbox{\tt,}}\texttt{1}&\mbox{{\small{\sc[Function]}}}\\\
&\mathrel{\stackrel{{\scriptstyle}}{{\longrightarrow}}}&\mbox{{\tt
Bike\\_Rental}}(\texttt{Inactive}\mathrel{,}\ell^{\prime}\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}}\Rightarrow\mbox{{\tt@Proposal}}\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}})\mathrel{\mbox{\tt,}}\texttt{1}&\mbox{{\small{\sc[Field\\_Update]}}}\\\
&\mathrel{\stackrel{{\scriptstyle}}{{\longrightarrow}}}&\mbox{{\tt
Bike\\_Rental}}(\texttt{Proposal}\mathrel{,}\ell^{\prime}\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}}\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}})\mathrel{\mbox{\tt,}}\texttt{1}&\mbox{{\small{\sc[State\\_Change]}}}\\\
&\mathrel{\stackrel{{\scriptstyle}}{{\longrightarrow}}}&\mbox{{\tt
Bike\\_Rental}}(\texttt{Proposal}\mathrel{,}\ell^{\prime}\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}}\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}})\mathrel{\mbox{\tt,}}\texttt{2}&\mbox{{\small{\sc[Tick]}}}\\\
&\mathrel{\stackrel{{\scriptstyle}}{{\longrightarrow}}}&\mbox{{\tt
Bike\\_Rental}}(\texttt{Proposal}\mathrel{,}\ell^{\prime}\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}}\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}})\mathrel{\mbox{\tt,}}\texttt{3}&\mbox{{\small{\sc[Tick]}}}\\\
&\mathrel{\stackrel{{\scriptstyle\mathit{Bob}\texttt{:accept[2]}}}{{\longrightarrow}}}&\mbox{{\tt
Bike\\_Rental}}(\texttt{Proposal}\mathrel{,}\ell^{\prime}[y\mapsto\mbox{{\tt
2}}]\mathrel{,}\texttt{S
W}\Rightarrow\mbox{{\tt@End}}\mathrel{,}\mbox{\raisebox{-2.32501pt}{{\tt-\\!\\!\\!-}}})\mathrel{\mbox{\tt,}}\texttt{3}&\mbox{{\small{\sc[Function]}}}\end{array}$

Table 3:  Initial transitions of Bike_Rental

To sum up, a legal contract behaves as follows:

  1. 1.

the first action is always an agreement, which moves the contract to an idle
state;

  2. 2.

in an idle state, fire any ready event with a matching state. If there is one,
execute its handler until the end, which is an idle state;

  3. 3.

if there is no event to be triggered in an idle state, _either_ tick _or_ call
any permitted function (_i.e._ with matching state and preconditions). A
function invocation amounts to execute its body until the end, which is again
an idle state.

Therefore, we observe that _Stipula_ has three sources of nondeterminism:
(_i_) the order of the execution of ready event handlers, (_ii_) the order of
the calls of permitted functions, and (_iii_) the delay of permitted function
calls to a later time (thus, possibly, after other event handlers). For
example, the contract C with two functions @Q A:f{--}$\Rightarrow$@Q and @Q
A′:g{--}$\Rightarrow$@Q behaves as either $\mathrel{\stackrel{{\scriptstyle
A\texttt{:f}}}{{\longrightarrow}}}\mathrel{\stackrel{{\scriptstyle}}{{\longrightarrow}}}_{n}\mathrel{\stackrel{{\scriptstyle
A^{\prime}\texttt{:g}}}{{\longrightarrow}}}$ or
$\mathrel{\stackrel{{\scriptstyle
A^{\prime}\texttt{:g}}}{{\longrightarrow}}}\mathrel{\stackrel{{\scriptstyle}}{{\longrightarrow}}}_{n}\mathrel{\stackrel{{\scriptstyle
A\texttt{:f}}}{{\longrightarrow}}}$, where
$\mathrel{\stackrel{{\scriptstyle}}{{\longrightarrow}}}_{n}$ are transitions
that make the time elapse (rule [Tick]). As another example, consider a
contract $\mbox{{\tt C}}^{\prime}$ with a function @Q A:f {-- now $\gg$
@Q′{ "hello"$\rightarrow$A }$\Rightarrow$@Q′ }$\Rightarrow$@Q and a function
@Q A′:g {--}$\Rightarrow$@Q′. Then it may behave as either
$\mathrel{\stackrel{{\scriptstyle
A\texttt{:f}}}{{\longrightarrow}}}\mathrel{\stackrel{{\scriptstyle
A^{\prime}\texttt{:g}}}{{\longrightarrow}}}\mathrel{\stackrel{{\scriptstyle\texttt{''hello''}\rightarrow\texttt{A}}}{{\longrightarrow}}}$
or as $\mathrel{\stackrel{{\scriptstyle
A\texttt{:f}}}{{\longrightarrow}}}\mathrel{\stackrel{{\scriptstyle}}{{\longrightarrow}}}_{n}\mathrel{\stackrel{{\scriptstyle
A^{\prime}\texttt{:g}}}{{\longrightarrow}}}$, after which the action
$\mathrel{\stackrel{{\scriptstyle\texttt{''hello''}\rightarrow
A}}{{\longrightarrow}}}$ is disabled, or as $\mathrel{\stackrel{{\scriptstyle
A^{\prime}\texttt{:g}}}{{\longrightarrow}}}$, which precludes the call of f.

#### Remark.

The semantics of _Stipula_ may be easily extended to configurations with
several smart legal contracts. It is sufficient to consider configurations as
consisting of sets of runtime contracts and to change the rule [Tick]. To
illustrate the general case, let $\mathbb{C}=\mbox{{\tt
C}}_{1}(\Phi_{1}\mathrel{,}\ell_{1}\mathrel{,}\Sigma_{1}\mathrel{,}\Psi_{1}),\cdots,\mbox{{\tt
C}}_{n}(\Phi_{n}\mathrel{,}\ell_{n}\mathrel{,}\Sigma_{n}\mathrel{,}\Psi_{n})$.
We define $\mathtt{Events}(\mathbb{C})\stackrel{{\scriptstyle\textsf{\tiny
def}}}{{=}}\Psi_{1}~{}|~{}\cdots~{}|~{}\Psi_{n}$. The new rule [Tick] becomes

$\begin{array}[]{l}\mbox{\tiny[{\sc Tick+}]}\\\
\frac{{}^{\textstyle\mathtt{Events}(\mathbb{C})\mathrel{\mbox{\tt,}}\mathbb{t}\mathrel{\nrightarrow}}}{{}_{\textstyle\mathbb{C}\mathrel{\mbox{\tt,}}\mathbb{t}\mathrel{\stackrel{{\scriptstyle}}{{\longrightarrow}}}\mathbb{C}\mathrel{\mbox{\tt,}}\mathbb{t}+1}}\end{array}$

##  5 _Stipula_ laws and Equational Theory

The operational semantics of Tables 2 and 2 is too intensional because it
defines the behaviour of a legal contract without showing any evidence of the
differences between contracts. Nevertheless, it is the base for defining a
more appropriate, extensional semantics using a standard technique based on
observations [20]. According to this technique, two contracts cannot be
separated if a party using them cannot distinguish one from the other. Said
otherwise, a party can differentiate two contracts if he can _observe
different interactions_. It turns out that defining the observations is a
critical point of the overall technique, because it allows to fine-tune the
discriminating power of the extensional semantics. The appropriate
observations for smart legal contracts match the design principles of
_Stipula_ : let $A$ be a party, then

  * •

$A$ should observe the _agreement_ that he is going to sign, because
stipulating a different agreement may be unsatisfactory; therefore we envisage
the observation $(A:\overline{v})$, that observes the exact set of values
$\overline{v}$ the party $A$ agreed about.

  * •

$A$ should also observe the _permission_ or the _prohibition_ to invoke a
functionality at a given time $\mathbb{t}$, _i.e._ whether
$A:\texttt{f}(\overline{v})[\overline{w}]$ is possible at $\mathbb{t}$ or not;

  * •

$A$ should finally observe whether at $\mathbb{t}$ he can _receive_ a value or
an asset, _i.e._ whether $v\rightarrow A$ or $v\multimap A$ are possible at
$\mathbb{t}$ or not.

The ordering of invocations and receives can be safely overlooked, as long as
they belong to the same block of transactions, that is they are executed at
the same global time. Notice also that the above observations allow a party to
observe contract’s _obligations_. Indeed, by shifting the observation at a
specific point in time, one can observe the effects of executing the event
that encodes a legal commitment, such as the issue of a sanction or the
impossibility to do further actions. On the other hand, the foregoing notion
of observations abstracts away from the names of the contract’s assets and
internal states.

We will use the following notations:

  * •

Let be
$\alpha_{1}=(\overline{A},\,{\overline{A}_{1}}{:}\overline{v}_{1}\cdots{\overline{A}_{n}}{:}\overline{v}_{n})$
and
$\alpha_{2}=(\overline{B},\,{\overline{B}_{1}}{:}\overline{w}_{1}\cdots{\overline{B}_{n}}{:}\overline{w}_{n})$
then we write $\alpha_{1}\sim\alpha_{2}$ if $\overline{A}$ and $\overline{B}$
are equal up to reordering of sequences, and similarly for
${\overline{A}_{i}}:\overline{v}_{i}$ and $\overline{B}_{j}:\overline{v}_{i}$.

  * •

Let be
$\mathrel{\stackrel{{\scriptstyle\mu}}{{\Longrightarrow}}}\;\stackrel{{\scriptstyle\textsf{\tiny
def}}}{{=}}\;\mathrel{\stackrel{{\scriptstyle}}{{\Longrightarrow}}}\mathrel{\stackrel{{\scriptstyle\mu}}{{\longrightarrow}}}\mathrel{\stackrel{{\scriptstyle}}{{\Longrightarrow}}}$,
where $\mathrel{\stackrel{{\scriptstyle}}{{\Longrightarrow}}}$ stands for any
number of $\mathrel{\stackrel{{\scriptstyle}}{{\longrightarrow}}}$
transitions, possibly zero.

The following definition of legal contract equivalence compares the observable
behavior of contracts. It is defined over configurations, so to appropriately
shift the time of the contract’s observations. The equivalence is defined as a
suitable bisimulation game that is consistent with the idea that in blockchain
systems the interactions are batched in blocks of transactions.

######  Definition 1 (Legal Bisimulation)

A symmetric relation $\mathcal{R}$ is a legal bisimulation between two
configurations at time $\mathbb{t}$, written
$\mathbb{C}_{1}{\mathrel{\mbox{\tt,}}}\mathbb{t}\ \ \mathcal{R}\ \
\mathbb{C}_{2}{\mathrel{\mbox{\tt,}}}\mathbb{t}$, whenever

  1. 1.

if
$\mathbb{C}_{1}{\mathrel{\mbox{\tt,}}}\mathbb{t}\mathrel{\stackrel{{\scriptstyle\alpha}}{{\Longrightarrow}}}\mathbb{C}_{1}^{\prime}{\mathrel{\mbox{\tt,}}}\mathbb{t}$
then
$\mathbb{C}_{2}{\mathrel{\mbox{\tt,}}}\mathbb{t}\mathrel{\stackrel{{\scriptstyle\alpha^{\prime}}}{{\Longrightarrow}}}\mathbb{C}_{2}^{\prime}{\mathrel{\mbox{\tt,}}}\mathbb{t}$
for some $\alpha^{\prime}$ such that $\alpha\sim\alpha^{\prime}$ and
$\mathbb{C}_{1}^{\prime}{\mathrel{\mbox{\tt,}}}\mathbb{t}\ \ \mathcal{R}\ \
\mathbb{C}_{2}^{\prime},\mathbb{t}$;

  2. 2.

if
$\mathbb{C}_{1}{\mathrel{\mbox{\tt,}}}\mathbb{t}\mathrel{\stackrel{{\scriptstyle\mu_{1}}}{{\Longrightarrow}}}\cdots\mathrel{\stackrel{{\scriptstyle\mu_{n}}}{{\Longrightarrow}}}\mathbb{C}_{1}^{\prime},\mathbb{t}\mathrel{\stackrel{{\scriptstyle}}{{\longrightarrow}}}\mathbb{C}_{1}^{\prime},\mathbb{t}+1$
then there exist $\mu_{1}^{\prime}\cdots\mu_{n}^{\prime}$ that is a
permutation of $\mu_{1}\cdots\mu_{n}$ such that
$\mathbb{C}_{2}{\mathrel{\mbox{\tt,}}}\mathbb{t}\mathrel{\stackrel{{\scriptstyle\mu_{1}^{\prime}}}{{\Longrightarrow}}}\cdots\mathrel{\stackrel{{\scriptstyle\mu_{n}^{\prime}}}{{\Longrightarrow}}}\mathbb{C}_{2}^{\prime}{\mathrel{\mbox{\tt,}}}\mathbb{t}\mathrel{\stackrel{{\scriptstyle}}{{\longrightarrow}}}\mathbb{C}_{2}^{\prime}{\mathrel{\mbox{\tt,}}}\mathbb{t}+1$
and $\mathbb{C}_{1}^{\prime}{\mathrel{\mbox{\tt,}}}\mathbb{t}+1\ \mathcal{R}\
\mathbb{C}_{2}^{\prime}{\mathrel{\mbox{\tt,}}}\mathbb{t}+1$.

Let $\simeq$ be the largest legal bisimulation, called _bisimilarity_. When
the initial configurations of contracts C and $\mbox{{\tt C}}^{\prime}$ are
bisimilar, we simply write $\mbox{{\tt C}}\simeq\mbox{{\tt C}}^{\prime}$.

Being a symmetric relation, a legal bisimulation compares both contracts’
permissions and prohibitions: if C permits an action (_i.e._ exhibits an
observation), then $\mbox{{\tt C}}^{\prime}$ must permit the same action, and
if C prohibits an action (_i.e._ does not exhibit a function call or an
external communication), then also $\mbox{{\tt C}}^{\prime}$ must not exhibit
the corresponding observation. Moreover, the bisimulation game enforces a
_transfer property_ , that is it shifts the time of observation to the future,
so to capture and compare the changes of permissions/prohibitions and the
(future) obligations. Observe that the equivalence abstracts away the ordering
of the observations within the same time clock, since in a blockchain there is
no strong notion of ordering between the transactions contained in the same
block. Nevertheless, specific orderings of function invocations are important
in _Stipula_ contracts and the equivalence cannot overlook essential
precedence constraints. For instance, the requirement that a function
delivering a service can only be invoked after another specific function, say
a payment. This is indeed the case for the legal bisimulation. To explain,
consider the contract C with two functions @Q A:f{--}$\Rightarrow$@Q and @Q
A′:g{--}$\Rightarrow$@Q and the contract $\mbox{{\tt C}}^{\prime}$ with two
functions @Q A:f{--}$\Rightarrow$@Q′ and @Q′ A′:g{--}$\Rightarrow$@Q. In
C the functions can be called in any order, while in $\mbox{{\tt C}}^{\prime}$
the function g can be invoked only after f. Accordingly, $\mbox{{\tt
C}}\not\simeq\mbox{{\tt C}}^{\prime}$ since there is a runtime configuration
of C that exhibits the observation $\mathrel{\stackrel{{\scriptstyle
A^{\prime}:{\rm g}}}{{\Longrightarrow}}}$, while it is not the case for the
contract $\mbox{{\tt C}}^{\prime}$, since at any time it can only exhibit
$\mathrel{\stackrel{{\scriptstyle A:{\rm
f}}}{{\Longrightarrow}}}\mathrel{\stackrel{{\scriptstyle A^{\prime}:{\rm
g}}}{{\Longrightarrow}}}$.

The following theorem highlights the property that the internal state of the
contract is abstracted away by the extensional semantics, which only observes
the external contract’s behavior. The proof is omitted because it is standard.

######  Theorem 5.1 (Internal refactoring)

Let C and $\mbox{{\tt C}}^{\prime}$ be two contracts that are equal up-to a
bijective renaming of states. Then $\mbox{{\tt C}}\simeq\mbox{{\tt
C}}^{\prime}$. Similarly, for bijective renaming of assets, fields and
contract names.

The theorem could be extended to contracts equal up-to the number of
contract’s fields and assets, as long as their external behavior is the same.
We keep for future work a precise formalization of the internal refactoring
allowed by the observational equivalence.

Bisimilarity is also independent from _future_ clock values. This allows us to
garbage-collect events that cannot be triggered anymore because the time for
their scheduling is already elapsed.

######  Theorem 5.2 (Time shift)

  1. 1.

If
$\mathbb{C}{\mathrel{\mbox{\tt,}}}\mathbb{t}\simeq\mathbb{C}^{\prime}{\mathrel{\mbox{\tt,}}}\mathbb{t}$
and $\mathbb{t}\leq\mathbb{t}^{\prime}$, then
$\mathbb{C}{\mathrel{\mbox{\tt,}}}\mathbb{t}^{\prime}\simeq\mathbb{C}^{\prime}{\mathrel{\mbox{\tt,}}}\mathbb{t}^{\prime}$.

  2. 2.

If $\mathbb{t}<\mathbb{t}^{\prime}$ then $\mbox{{\tt
C}}(\texttt{Q}\mathrel{,}\ell\mathrel{,}\Sigma\mathrel{,}\Psi~{}|~{}\mathbb{t}\gg\texttt{@}\texttt{Q}~{}\\{~{}\texttt{S}~{}\\}\Rightarrow\texttt{@}\texttt{Q}^{\prime})\,{\mathrel{\mbox{\tt,}}}\,\mathbb{t}^{\prime}\
\simeq\ \mbox{{\tt
C}}(\texttt{Q}\mathrel{,}\ell\mathrel{,}\Sigma\mathrel{,}\Psi)\,{\mathrel{\mbox{\tt,}}}\,\mathbb{t}^{\prime}$.

We finally put forward a set of algebraic laws that formalize the fact that
the ordering of remote communications can be safely overlooked, as long as
they belong to the same transaction. The laws are defined over statements,
therefore, let $\mbox{{\tt C}}[~{}]$ be a _context_ , that is a contract that
contains an hole where a statement may occur. We write
$\texttt{S}\simeq\texttt{S}^{\prime}$ if, for every context $\mbox{{\tt
C}}[~{}]$, $\mbox{{\tt C}}[\texttt{S}]\simeq\mbox{{\tt
C}}[\texttt{S}^{\prime}]$.

###### Theorem 5.3

The following non-interference laws hold in _Stipula_ (whenever they are
applicable, we assume $\texttt{x}\notin\mbox{{\em fv}}(\texttt{E}^{\prime})$
and $\texttt{x}^{\prime}\notin\mbox{{\em fv}}(\texttt{E})$ and
$\texttt{h}\notin\mbox{{\em fv}}(\texttt{E}^{\prime})$ and
$\texttt{h}^{\prime}\notin\mbox{{\em fv}}(\texttt{E}^{\prime})$ and
$\texttt{h}^{\prime\prime}\notin\mbox{{\em fv}}(\texttt{E})$ and
$\texttt{h}^{\prime\prime\prime}\notin\mbox{{\em fv}}(\texttt{E})$):

$\begin{array}[]{@{\hspace{-.0cm}}r@{\quad}c@{\quad}l@{\quad}l}\texttt{E}\rightarrow\texttt{A}\;\;\texttt{E}^{\prime}\rightarrow\texttt{A}^{\prime}&\simeq&\texttt{E}^{\prime}\rightarrow\texttt{A}^{\prime}\;\;\texttt{E}\rightarrow\texttt{A}&\\\
\texttt{E}\rightarrow\texttt{x}\;\;\texttt{E}^{\prime}\rightarrow\texttt{A}&\simeq&\texttt{E}^{\prime}\rightarrow\texttt{A}\;\;\texttt{E}\rightarrow
x&\\\ \texttt{E}\rightarrow\texttt{x}\;\;\texttt{E}^{\prime}\rightarrow
x^{\prime}&\simeq&\texttt{E}^{\prime}\rightarrow\texttt{x}^{\prime}\;\;\texttt{E}\rightarrow\texttt{x}&\\\
\texttt{E}\multimap\texttt{h},\texttt{A}\;\;\texttt{E}^{\prime}\rightarrow\texttt{A}^{\prime}&\simeq&\texttt{E}^{\prime}\rightarrow\texttt{A}^{\prime}\;\;\texttt{E}\multimap\texttt{h},\texttt{A}&\\\
\texttt{E}\multimap\texttt{h},\texttt{A}\;\;\texttt{E}^{\prime}\rightarrow\texttt{x}^{\prime}&\simeq&\texttt{E}^{\prime}\rightarrow\texttt{x}^{\prime}\;\;\texttt{E}\multimap\texttt{h},\texttt{A}&\\\
\texttt{E}\multimap\texttt{h},\texttt{h}^{\prime}\;\;\texttt{E}^{\prime}\rightarrow\texttt{A}&\simeq&\texttt{E}^{\prime}\rightarrow\texttt{A}\;\;\texttt{E}\multimap\texttt{h},\texttt{h}^{\prime}&\\\
\texttt{E}\multimap\texttt{h},\texttt{h}^{\prime}\;\;\texttt{E}^{\prime}\rightarrow\texttt{x}^{\prime}&\simeq&\texttt{E}^{\prime}\rightarrow\texttt{x}^{\prime}\;\;\texttt{E}\multimap\texttt{h},\texttt{h}^{\prime}&\\\
\texttt{E}\multimap\texttt{h},\texttt{A}\;\;\texttt{E}^{\prime}\multimap\texttt{h}^{\prime\prime},\texttt{A}^{\prime}&\simeq&\texttt{E}^{\prime}\multimap\texttt{h}^{\prime\prime},\texttt{A}^{\prime}\;\;\texttt{E}\multimap\texttt{h},\texttt{A}&\\\
\texttt{E}\multimap\texttt{h},\texttt{A}\;\;\texttt{E}^{\prime}\multimap\texttt{h}^{\prime\prime},\texttt{h}^{\prime\prime\prime}&\simeq&\texttt{E}^{\prime}\multimap\texttt{h}^{\prime\prime},\texttt{h}^{\prime\prime\prime}\;\;\texttt{E}\multimap\texttt{h},\texttt{A}&\\\
\texttt{E}\multimap\texttt{h},\texttt{h}^{\prime}\;\;\texttt{E}^{\prime}\multimap\texttt{h}^{\prime\prime},\texttt{h}^{\prime\prime\prime}&\simeq&\texttt{E}^{\prime}\multimap\texttt{h}^{\prime\prime},\texttt{h}^{\prime\prime\prime}\;\;\texttt{E}\multimap\texttt{h},\texttt{h}^{\prime}&\end{array}$

###### Proof

We prove the first equality. Let be
$\texttt{S}_{1}=\texttt{E}\rightarrow\texttt{A}\;\;\texttt{E}^{\prime}\rightarrow\texttt{A}^{\prime}$
and
$\texttt{S}_{2}=\texttt{E}^{\prime}\rightarrow\texttt{A}^{\prime}\;\;\texttt{E}\rightarrow\texttt{A}$,
and let be $\mbox{{\tt C}}_{1}=\mbox{{\tt C}}[\texttt{S}_{1}]$ and $\mbox{{\tt
C}}_{2}=\mbox{{\tt C}}[\texttt{S}_{2}]$, then we need to prove that
$\mbox{{\tt
C}}_{1}(\mbox{\raisebox{-2.58334pt}{{\tt-\\!\\!\\!-}}},\varnothing,\mbox{\raisebox{-2.58334pt}{{\tt-\\!\\!\\!-}}},\mbox{\raisebox{-2.58334pt}{{\tt-\\!\\!\\!-}}}){\mathrel{\mbox{\tt,}}}\mathbb{t}\simeq\mbox{{\tt
C}}_{2}(\mbox{\raisebox{-2.58334pt}{{\tt-\\!\\!\\!-}}},\varnothing,\mbox{\raisebox{-2.58334pt}{{\tt-\\!\\!\\!-}}},\mbox{\raisebox{-2.58334pt}{{\tt-\\!\\!\\!-}}}){\mathrel{\mbox{\tt,}}}\mathbb{t}$.
Let also $\mathbb{C}_{i}=\mbox{{\tt
C}}_{i}(\Phi,\ell,\mbox{\raisebox{-2.58334pt}{{\tt-\\!\\!\\!-}}},\Psi[\texttt{S}_{i}])$,
with $i=1,2$, be the runtime contract where the statement $\texttt{S}_{i}$
occurs within a number of handlers of future events. We demonstrate that the
symmetric closure of the following relation is a legal bisimulation:

$\begin{array}[]{l}\\{\,\bigl{(}\mbox{{\tt
C}}_{1}(\mbox{\raisebox{-2.58334pt}{{\tt-\\!\\!\\!-}}},\varnothing,\mbox{\raisebox{-2.58334pt}{{\tt-\\!\\!\\!-}}},\mbox{\raisebox{-2.58334pt}{{\tt-\\!\\!\\!-}}}){\mathrel{\mbox{\tt,}}}\mathbb{t}\
,\ \mbox{{\tt
C}}_{2}(\mbox{\raisebox{-2.58334pt}{{\tt-\\!\\!\\!-}}},\varnothing,\mbox{\raisebox{-2.58334pt}{{\tt-\\!\\!\\!-}}},\mbox{\raisebox{-2.58334pt}{{\tt-\\!\\!\\!-}}}){\mathrel{\mbox{\tt,}}}\mathbb{t}\bigr{)}\,\\}\\\\[5.69054pt]
\cup\,\\{\,\bigl{(}\mbox{{\tt
C}}_{1}(\texttt{Q},\ell,\mbox{\raisebox{-2.58334pt}{{\tt-\\!\\!\\!-}}},\Psi[\texttt{S}_{1}]){\mathrel{\mbox{\tt,}}}\mathbb{t}^{\prime}\
,\ \mbox{{\tt
C}}_{2}(\texttt{Q},\ell,\mbox{\raisebox{-2.58334pt}{{\tt-\\!\\!\\!-}}},\Psi[\texttt{S}_{2}]){\mathrel{\mbox{\tt,}}}\mathbb{t}^{\prime}\bigr{)}\quad\;|~{}\;\text{for
every }\texttt{Q},\ell,\Psi[~{}],\mathbb{t}^{\prime}\;\\}\end{array}$

Indeed, notice that the statement
$\texttt{E}\rightarrow\texttt{A}\;\;\texttt{E}^{\prime}\rightarrow\texttt{A}^{\prime}$
can only contribute to the behavior of C with a couple of transitions during
the evaluation of the body of a function or the evaluation of an event
handler. Therefore the statement must be completely executed with the same
time clock, possibly a number $k$ of times due to the multiple function calls
and event handlers that are executed during the same time clock.

Formally, if
$\mathbb{C}_{1},\mathbb{t}^{\prime}\mathrel{\stackrel{{\scriptstyle\mu_{1}}}{{\Longrightarrow}}}\cdots\mathrel{\stackrel{{\scriptstyle\mu_{n}}}{{\Longrightarrow}}}\mathbb{C}_{1}^{\prime},\mathbb{t}^{\prime}\mathrel{\stackrel{{\scriptstyle}}{{\longrightarrow}}}\mathbb{C}_{1}^{\prime},\mathbb{t}^{\prime}+1$,
then the sequence $\mu_{1}\cdots\mu_{n}$ contains $k$ occurrences of the pair
$v\rightarrow\texttt{A},v^{\prime}\rightarrow\texttt{A}^{\prime}$. Similarly,
there exist $\mu^{\prime}_{1}\cdots\mu^{\prime}_{n}$ and a configuration
$\mathbb{C}_{2}^{\prime},\mathbb{t}^{\prime}$ such that
$\mathbb{C}_{2},\mathbb{t}^{\prime}\mathrel{\stackrel{{\scriptstyle\mu^{\prime}_{1}}}{{\Longrightarrow}}}\cdots\mathrel{\stackrel{{\scriptstyle\mu^{\prime}_{n}}}{{\Longrightarrow}}}\mathbb{C}_{2}^{\prime},\mathbb{t}^{\prime}\mathrel{\stackrel{{\scriptstyle}}{{\longrightarrow}}}\mathbb{C}_{2}^{\prime},\mathbb{t}^{\prime}+1$,
where the sequence $\mu^{\prime}_{1}\cdots\mu^{\prime}_{n}$ is identical to
$\mu_{1}\cdots\mu_{n}$ but for the $k$ occurrences of the pair
$v\rightarrow\texttt{A},v^{\prime}\rightarrow\texttt{A}^{\prime}$ that has
been swapped into
$v^{\prime}\rightarrow\texttt{A}^{\prime},v\rightarrow\texttt{A}$. The
argument also holds in the converse direction.

##  6 Towards a distributed implementation

The definition of _Stipula_ is implementation-agnostic, that is it can be
either executed as a centralized application or it can be run on top of a
distributed system, such as a blockchain. Implementing _Stipula_ in terms of
smart contracts, _e.g._ Solidity, would bring in the advantages of a public
and decentralized blockchain platform. These include the benefits coming form
the fact that several governments have recently recognised that smart
contracts and, more generally, programs operating over distributed ledgers,
have legal value [6, 4, 2]. However, _Stipula_ ’s contracts are more general
and encompass smart contracts: they provide benefits in terms of automatic
execution and enforcement of contractual conditions, traceability, and outcome
certainty even without using a blockchain. In particular, running a legal
contract over a secured centralized system allows for more efficiency, energy
save, additional privacy. Moreover, a controlled level of intermediation can
better monitor the contract enforcement, dealing with disputes between
contract’s parties and carring out judicial enforcements. Finally, the
intrinsic open nature of legal contracts is another challenge for smart
contracts, that can hardly deal with the off-chain world: external data enter
the blockchain only through oracles, which are problematic in many senses, and
the dynamic change of behaviours conflicts with the rigidity of smart
contracts definition. Time is another big issue in blockchains.

While we are currently prototyping _Stipula_ on a centralized system, we think
that a distributed implementation on a blockchain system is interesting. Below
we discuss the issues of prototyping _Stipula_ , either on top of a
centralized system or a distributed system like a (public) blockchain.

#### Functions and States.

_Stipula_ contracts are very close to class definitions, therefore sticking to
an object-oriented target language as Java or Solidity would ease the
prototyping effort. In this context, the state-aware programming is also well
developed. In particular, several smart contract languages widely use the
state machine pattern (_c.f._ Solidity [1] and Obsidian [3]).

#### Parties.

The implementation of _Stipula_ must carefully handle digital identities,
ensuring that a contract’s function is actually invoked by the correct caller.
In blockchain implementation this corresponds to the _externally owned
accounts_ , but the pseudoanonimity provided by _public_ blockchains might be
a limitation, since legal contract’s parties must have a trusted identity,
especially in the case of authorities, which must be bound to parties that are
trusted intermediaries.

#### Agreements.

The agreement code is technically a _join synchronization_ that expresses a
consensus between the parties to start the contract with particular values of
the (non-linear) fields. This construct can be implemented by resorting to a
barrier-like protocol, where each party Ai may call, in whatever order, a
specific function to propose the values he agrees on, and the barrier
eventually checks the consistency of the proposed values before moving the
contract to the initial state. The following snippet of Solidity-like code (a
similar code can be written also in Java RMI) corresponds to the agreement
code (see Section 3), where we assume that the fields of the contract are x1,
$\cdots$, xk with types T1,$\cdots$,Tk, respectively. We also assume that
$\overline{{\tt A}_{i}}:\overline{{\tt x}_{i}}$ is defined as ${{\tt
A}_{i}}^{1},\cdots,{{\tt A}_{i}}^{s\\_i}:{{\tt x}_{i}}^{1},\cdots,{{\tt
x}_{i}}^{s\\_i^{\prime}}$.

⬇

address A1, ... , An ;

T1 x1; ... ; Tk xk ;

enum State {Nothing, Q}

State state = State.Nothing ;

int counter = 1 ;

T${{}_{i}}^{1}$ aux${}_{i}\\_$x${{}_{i}}^{1}$;...;
T${{}_{i}}^{r\\_i^{\prime}}$ aux${}_{i}\\_$x${{}_{i}}^{r\\_i^{\prime}}$; // 1
$\leq i\leq$ n

bool use$\\_$oncei = true ; // 1 $\leq i\leq$ n

function set$\\_$oki(T${{}_{i}}^{1}$ z${{}_{i}}^{1}$,...,T${{}_{i}}^{r\\_i}$
z${{}_{i}}^{r\\_i}$,T${{}_{i}}^{r\\_i+1}$
z${{}_{i}}^{r\\_i+1}$,...,T${{}_{i}}^{r\\_i+r\\_i^{\prime}}$
z${{}_{i}}^{r\\_i+r\\_i^{\prime}}$){ // 1 $\leq i\leq$ n

if (sender == Ai $\mathbin{\binampersand}\mathbin{\binampersand}$
use$\\_$oncei){

use$\\_$oncei = false ;

x${{}_{i}}^{1}$ = z${{}_{i}}^{1}$ ; ... ; x${{}_{i}}^{r\\_i}$ =
z${{}_{i}}^{r\\_i}$ ;

aux${}_{i}\\_$x1 = z${{}_{i}}^{r\\_i+1}$;...;
aux${}_{i}\\_$x${}_{r_{i}^{\prime}}$ = z${{}_{i}}^{r\\_i+r\\_i^{\prime}}$;

if (counter == n){

if ($\bigwedge_{1\leq\texttt{i}\leq
n}$(aux${}_{i}\\_$x${{}_{i}}^{1}$==x${{}_{i}}^{1}$
$\mathbin{\binampersand}\mathbin{\binampersand}$...$\mathbin{\binampersand}\mathbin{\binampersand}$
aux${}_{i}\\_$x${{}_{i}}^{r\\_i^{\prime}}$==x${{}_{i}}^{r\\_i^{\prime}}$))

state = State.Q ;

else throw error;

} else counter = counter + 1 ;

} else throw error;

}

Each function set_oki can be called only once by the party Ai, with two lists
of parameters: the first $r_{i}$ values are used to set the contract’s fields
x${{}_{i}}^{1}$, $\cdots$, x${{}_{i}}^{r\\_i}$. The last $r_{i}^{\prime}$
values are recorded into the auxiliary fields
aux${}_{i}\\_$x${{}_{i}}^{r\\_i+1}$, $\cdots$,
aux${}_{i}\\_$x${{}_{i}}^{r\\_i+r\\_i^{\prime}}$, to express that Ai agrees
with anyone setting the contract’s fields x${{}_{i}}^{r\\_i+1}$, $\cdots$,
x${{}_{i}}^{r\\_i+r\\_i^{\prime}}$. When all the parties have done the
agreement, _i.e._ counter is equal to n, a check on the consistency of
aux${}_{i}\\_$x${{}_{i}}^{j}$ is performed and, in case it succeeds, the
contract becomes active moving to the state Q. The snippet also shows that
contract’s states can be easily mapped to enumerations, as usual in the
Solidity State Machine pattern.

There is a discrepancy between the above code and the semantics of the
agreement in Table 2. While the agreement has a transactional nature (it may
occur as a whole or not), the above Solidity protocol takes time, _i.e._ it is
performed in several blocks and, in any block, a failure may occur. In this
case, there is a backtrack to the _initial state of the block_ and not to the
initial state of the protocol, as it happens in _Stipula_. This means that the
error management should take care of removing partial values stored in the
fields of the contract. Nevertheless, another source of discrepancy seems more
awkward: the gas consumption. In fact, the successful termination of the
agreement as well as the failed one have a cost in Ethereum, while it is not
the case. To bridge this gap, we should design agreements with fees payed by
parties that are used for the consensus. We have not yet studied these
details, which are postponed to future work.

#### Assets.

Assets are linear resources that cannot be duplicated or leaked: when a
resource value is assigned, the location previously holding the value is
emptied. Modern programming languages, $e.g.,$ Rust and Move, have already
recognized the relevance of having linear resources as first-class entities,
because they can significantly simplify programming and the effort required
for verification. _Stipula_ features a simple abstraction to manage assets,
which is used to represent both currency and indivisible tokens. To implement
these assets on top of a blockchain, we can resort to the popular token
standards on Ethereum (ERC-20 for virtual currency and ERC-721 for non
fungible tokens[14]). Alternatively, we can rely on the Move language, whose
designers have featured programmable linear resources by constraining them to
adhere to ad-hoc rules specified by its declaring module [8, 12]. Using a
pseudo-code inspired to Move, we might define (divisible) assets h and h′ as
resources of type H, so that the operations
$\texttt{E}\multimap\texttt{h},\texttt{h}^{\prime}$ and
$\texttt{E}\multimap\texttt{h},\texttt{A}$ may be encoded by h.move(E,h′) and
h.withdraw(E,A), according to the definitions below:

     resource H {
         T amount ;
    ΨΨ
         function move(T x, H h) {
              (x <= amount){ h = h + x ; amount = amount - x ; }
         }ΨΨ
         function withdraw(T x, address A) {
              (x <= amount){ A.send(x) ; amount = amount - x ; }
         }
         constructor(T x){ amount = x ; }
     }

#### Events.

Events correspond to scheduling a computation for future execution. While this
is a common feature of concurrent programming (many mainstream languages
provide primitives for _futures_ and _callbacks_), it is more difficult to
implement events in the context of blockchain. There are two reasons:

  1. 1.

in blockchains, the time flows according to the block insertion. Therefore, if
the event should be scheduled in one minute and the next block is inserted in
ten minutes, there is a delay that must be pondered;

  2. 2.

blockchains do not admit the record of statements that have to be performed
afterwards in a future transaction.

As regards the second issue, the standard technique adopted in Ethereum to
circumvent this limitation is based on the Solidity’s _event_ construct and
off-chain _oracle_ services. To explain, the _Stipula_ event E$\,\gg\,$ @Q { S
}$\,\Rightarrow\,$ @Q′ emitted by a function foo can be mapped to the Solidity
code:

⬇

event R(uint time, address lc) ;

function call_back_R() external {

if (state == State.Q) { S ; state = State.Q’; }

}

function foo(T1 u1,..., Tn un){

...

emit R(E,address(this)) ;

}

The Solidity function foo emits an event named R carrying the time E and the
address of the issuing contract. Moreover, an external _DApp service_ – an
oracle – scans the blockchain looking for R events and calls the call_back_R
function of the contract at the appropriate time E. Other more complex and
safer protocols can be used. However a code external to the Ethereum
blockchain is always necessary in order to trigger the scheduled event
handler. A more satisfactory implementation of the _Stipula_ events might
adopt ideas taken from the implementation of timeouts in the Marlowe on top of
the Cardano blockchain, as discussed in Section 8.

To conclude the section, notice that, in this paper, we are overlooking issues
regarding errors and backtracks.

##  7 Expressivity of _Stipula_

_Stipula_ has been devised for writing legal contracts in a formal and
intelligible (to lawyers) way. In this section we analyze the expressivity of
_Stipula_ by writing the contracts for a set of archetypal acts, ranging from
renting to (digital) licenses and to bets. We conclude this analysis with a
table that summarizes the legal elements of the archetypal acts and the
programming abstractions that we have used to express them in _Stipula_.

###  7.1 The free rent contract

⬇

1stipula Free_Rent {

2

3 assets token

4 fields numBox, t_start, t_limit

5

6 agreement (Lender, Borrower)(t_start, t_limit) {

7 Lender , Borrower : t_start, t_limit

8 } $\Rightarrow$ @Inactive

9

10 @Inactive Lender : boxProposal (n)[t] {

11 t $\multimap$ token

12 n $\rightarrow$ numBox

13 now + t_start $\gg$ @Proposal {

14 token $\multimap$ Lender } $\Rightarrow$ @End

15 } $\Rightarrow$ @Proposal

16

17 @Proposal Borrower : boxUse {

18 (uses(token), numBox) $\rightarrow$ Borrower

19 now + t_limit $\gg$ @Using {

20 "Time_Limit_Reached" $\rightarrow$ Borrower

21 token $\multimap$ Lender

22 } $\Rightarrow$ @End

23 } $\Rightarrow$ @Using

24

25 @Using Borrower : returnBox {

26 token $\multimap$ Lender

27 } $\Rightarrow$ @End

28}

Listing 2: The rent for free contract

The free rent is the simplest kind of legal contract. It involves two parties,
the lender and the borrower, which initially agree about what good is rented,
what use should be made of it, the time limit (or in which case it must be
returned), the estimated of value and any defects in the good. Upon agreement,
the delivery of the good triggers the legal bond, that is the borrower has the
permission to use the good and the lender has the prohibition of preventing
him from doing so. Note that there is no transfer of ownership, but only the
right to use the good. The contract terminates either when the borrower
returns the good, or when the time limit is reached. Litigations could arise
when the borrower violates the obligations of diligent storage and care, the
obligations of using the good only as intended, and not granting the use to a
third party without the lender’s consent. In these cases the lender may demand
the immediate return of the object, in addition to compensation for the
damage. On the other hand, the borrower is entitled to compensation if the
good has defects that were known to the lender but that he did not initially
disclose.

The free rent contract puts forward the following points:

  * •

When a legal contract refers to a _physical_ good, the smart contract needs a
digital handle (an avatar) for that good. Many technological solutions, such
as smart locks of IoT devices, are actually available. In _Stipula_ we
abstract from the specific nature of such a digital handle, and we simply
represent it as an asset, which intuitively corresponds to a non fungible
token associated to the physical good.

  * •

The rent legal contract grants just the _usage_ of a good without the transfer
of ownership. Accordingly, while the communication of the token provides full
control of the associated physical good, we assume an operation uses(token)
(resp. use_once(token) or uses(token,A)) that generates a usage-code providing
access to the object associated to the token (resp. a usage-code only valid
(once) for the party A).

  * •

In a legal rent contract it is important to acknowledge the delivery of the
good, since this is the action that triggers the legal bonds. We rely on
assets and their _semantics_ to implement this feature.

The _Stipula_ code for the free rent of a locker is written in Listing 2. The
two parties agrees on the time limit for the locker usage (time_limit) and the
time limit to start the usage (time_start). Contract’s states allow one
sequence of actions: first Lender sends the number n of the locker and the
token t associated to n by calling box_proposal (line 10). This action moves
the contract to the temporary state Proposal and schedule the event in line
13. This event is essential to prevent the unique token associated to the
locker to be indefinitely locked-in in the smart contract when the borrower
never calls the boxUse function to finalize the delivery of the good. If
Borrower calls the function boxUse (line 16) within the timeout time_start,
then the number of the rented locker and the access code are returned. At the
same time, a second timeout is installed to check the time limit for the
locker usage, and the final state change to Using (line 21) vanishes the
timeout installed in line 13. This second event is needed to prevent a never
ending use of the locker. If time_limit is reached and the contract’s state is
still Using, then (lines 18-19) a message is sent to Borrower and the token is
sent back to Lender, which becomes again in full control of the locker and can
thus invalidate the access code held by the borrower. Otherwise, the rent
contract can terminate because the borrower explicitly returns the good before
the time limit. This is represented by a call of the function returnBox (line
23).

The smart legal contract of Listing 2 does not consider the compensations that
would be needed to deal with the disputes due to breaches of the contract,
such as the borrower’s diligent care during the locker’s usage. These
violations require off-chain monitoring and a dispute resolution mechanism.
The next example illustrates how this off-chain monitoring and enforcement can
be combined with the on-chain code.

###  7.2 The Digital Licensee contract

⬇

1stipula Licence {

2 assets token, balance

3 fields cost, t_start, t_limit

4

5 agreement (Licensor,Licensee,Authority)(cost, t_start, t_limit) {

6 Licensor, Licensee : cost, t_start, t_limit

7 } $\Rightarrow$ @Inactive

8

9 @Inactive Licensor : offerLicence [t] {

10 t $\multimap$ token

11 now + t_start $\gg$ @Proposal {

12 token $\multimap$ Licensor } $\Rightarrow$ @End

13 } $\Rightarrow$ @Proposal

14

15 @Proposal Licensee : activateLicence [b]

16 (b == cost){

17 b $\multimap$ balance

18 balance*0,1 $\multimap$ balance, Authority

19 uses(token,Licensee) $\rightarrow$ Licensee

20 now + t_limit $\gg$ @Trial {

21 balance $\multimap$ Licensee

22 token $\multimap$ Licensor

23 } $\Rightarrow$ @End

24 } $\Rightarrow$ @Trial

25

26 @Trial Licensee : buy {

27 balance $\multimap$ Licensor

28 token $\multimap$ Licensee

29 } $\Rightarrow$ @End

30

31 @Trial Authority : compensateLicensor {

32 balance $\multimap$ Licensor

33 token $\multimap$ Licensor

34 } $\Rightarrow$@End

35

36 @Trial Authority : compensateLicensee {

37 balance $\multimap$ Licensee

38 token $\multimap$ Licensor;

39 } $\Rightarrow$ @End

40}

Listing 3: The contract for a digital licence

Let us consider a contract corresponding to a licence to access a digital
service, like a software or an ebook: the digital service can be freely
accessed for a while, and can be permanently bought with an explicit
communication within the evaluation period (for a similar example, see [17]).
The licensing contractual clauses can be described as follows:

Article 1.

Licensor grants Licensee for a licence to evaluate the Product and fixes (_i_)
the _evaluation period_ and (_ii_) the _cost_ of the Product if Licensee will
bought it.

Article 2.

Licensee will pay the Product in advance; he will be reimbursed if the Product
will not be bought with an explicit communication within the evaluation
period. The refund will be the 90% of the cost because the 10% is payed to the
Authority (see Article 3).

Article 3.

Licensee must not publish the results of the evaluation during the evaluation
period and Licensor must reply within 10 hours to the queries of Licensee
related to the Product; this is supervised by Authority that may interrupt the
licence and reimburse either Licensor or Licensee according to whom breaches
this agreement.

Article 4.

This license will terminate automatically at the end of the evaluation period,
if the licensee does not buy the product.

Compared to the previous example, this contract involves payment and refund:
an amount of currency is escrowed, and two parts of it will be sent to
different parties, the Authority and either the Licensor or the Licensee.
_Stipula_ provides the general asset abstraction, together with a general
operation to move just a (positive) subset of the asset to a different owner.
This is exactly what is needed to deal with currency, therefore the _Stipula_
licence contract holds two different assets: an indivisible token providing an
handle to the digital service, and a balance that is a divisible asset
corresponding to the amount of currency kept in custody inside the smart
contract.

A further important feature of the contract is Article 3 that defines specific
constraints about the _off-chain_ behaviour of Licensor and Licensee. This
exemplifies the very general situations where contract’s violations cannot be
fully monitored by the on-chain software, such as the publication of a post in
a social network, or the leakage of a secret password, or the violation of the
obligation of diligent storage and care. In all these cases, it is required a
trusted third party, say an Authority, to supervise the disputes occurring
from the off-chain monitoring and to provide a trusted dispute resolution
mechanism. The code in Listing 3 illustrates the encoding of the off-chain
monitoring and enforcement mechanism with the on-chain smart contract code in
_Stipula_.

The agreement of Listing 3 involves three parties: Licensor, which fixes the
parameters of the contract, according to Article 1., Licensee, which
explicitly agrees, and Authority, which does not need to agree upon the
contracts’ parameters (_i.e._ the emptyset agreement noted --), but it is
important that it is involved in the agreement synchronization, because it
plays the role of the trusted third party that is entitled to call the
functions compen-sateLicensor and compensateLicensee.

In activateLicence, the caller, _i.e._ the Licensee, is required to send an
amount of assets equal to the fixed cost of the license. Notice the difference
between line 18 and line 19: the first one is the move of a fraction of asset
towards the authority, while the second is the simple communication to
Licensee of a personal usage code associated to the token. Once entered in the
Trial state, the contract can terminate in three ways: (_i_) the licensee
expresses its willingness to buy the licence by calling the function call
which grants him the full token, or (_ii_) the time limit for the free
evaluation period is reached, thus the scheduled event refunds the licensee
and gives the token back to the licensor, or (_iii_) during the evaluation
period a violation to Article 3 is identified and the authority pre-empts the
license by calling either the function compensateLicensor or
compensateLicensee. Observe that it is important that the code guarantees
that, in all the possible cases, the assets, both the token and the balance,
are not indefinitely locked-in the contract.

###  7.3 A bet contract

The bet contract is a simple example of a legal contract that contains an
element of randomness (_alea_), _i.e._ where the existence of the performances
or their extent depends on an event which is entirely independent of the will
of the parties. The main element of the contract is a future, aleatory event,
such as the winner of a football match, the delay of a flight, the future
value of a company’s stock.

A digital encoding of a bet contract requires that the parties explicitly
agree on the source of data that will determine the final value of the
aleatory event (the _Data Provider_), that is a specific online service, an
accredited institution, or any trusted third party. It is also important that
the digital contract provides precise time limits for accepting payments and
for providing the actual value of the aleatory event. Indeed there can be a
number of issues: the aleatory event does not happen, _e.g._ the football
match is cancelled, or the data provider fails to provide the required value,
_e.g._ the online service is down.

⬇

1stipula Alea {

2 assets bet1, bet2

3 fields alea_fact, val1, val2, data_source,

4 fee, amount, t_before, t_after

5

6 agreement(Better1,Better2,DataProvider)

7 (fee, data_source, t_before, t_after, alea_fact, amount){

8

9 DataProvider, Better1, Better2 : fee, data_source, t_after, alea_fact

10 Better1, Better2 : amount, t_before

11 } $\Rightarrow$ @Init

12

13 @Init Better1 : place_bet(x)[y]

14 (y == amount){

15 y $\multimap$ bet1

16 x $\rightarrow$ val1

17 t_before $\gg$ @First { bet1 $\multimap$ Better1 } $\Rightarrow$ @Fail

18 } $\Rightarrow$ @First

19

20 @First Better2: place_bet(x)[y]

21 (y == amount){

22 y $\multimap$ bet2

23 x $\rightarrow$ val2

24 t_after $\gg$ @Run {

25 bet1 $\multimap$ Better1

26 bet2 $\multimap$ Better2 } $\Rightarrow$ @Fail

27 } $\Rightarrow$ @Run

28

29 @Run DataProvider : data(x,z)[]

30 (x==alea_fact){

31 (z==val1){ // The winner is Better1

32 fee $\multimap$ bet2,DataProvider

33 bet2 $\multimap$ Better1

34 bet1 $\multimap$ Better1

35 }

36 (z==val2){ // The winner is Better2

37 fee $\multimap$ bet1,DataProvider

38 bet1 $\multimap$ Better2

39 bet2 $\multimap$ Better2

40 }

41 (z != val1 $\mathbin{\binampersand}\mathbin{\binampersand}$ z != val2){
//No winner

42 bet1 $\multimap$ DataProvider

43 bet2 $\multimap$ DataProvider

44 }

45 } $\Rightarrow$ @End

46}

Listing 4: The contract for a bet

The _Stipula_ code in Listing 4 corresponds to the case where Better1,
respectively Better2, places val1, respectively val2, a bet corresponding to
the agreed amount of currency, stored in the contract’s assets bet1 and bet2
respectively111For simplicity, this code requires Better1 to place its bet
before Better2, however it is easy to add similar function to let the two bets
be placed in any order.. Observe that both bets must be placed within an
(agreed) time limit t_before (line 17), to ensure that the legal bond is
established before the occurrence of the aleatory event. The second timeout,
scheduled in line 24, is used to ensure the contract termination even if the
DataProvider fails to provide the expected data, through the call of the
function data.

Compared to the Digital Licence in Listing 3, the role of the DataProvider
here is less pivotal than that of the Authority. While it is expected that
Authority will play its part, DataProvider is much less than a peer of the
contract. It is sufficient that it is an independent party that is entitled to
call the contract’s function to supply the expected external data. The crucial
point of trust here is the data_source, not the DataProvider. In other terms,
since the parties involved in the agreement need not to trust each other, it
might happen that DataProvider supplies an incorrect value through the
function data. In this case, the betters can appeal against the data provider
since they agreed upon the data emitted by the data_source. As usual, any
dispute that might render the contract voidable or invalid, _e.g._ one better
knew the result of the match in advance, can be handled by adding to the code
of an authority party, according to the pattern illustrated in the Digital
Licence example.

###  7.4 Specification patterns in _Stipula_

The clauses of the foregoing legal acts have been specified in _Stipula_ by
means of patterns that, in our view, are common from the juridical point of
view. This is summarized in Table 4.

Example | Legal clauses | Smart Encoding in _Stipula_
---|---|---
Free rent | Permission and Prohibition |  States of the contract to allow or prevent the call of a function
| Obligation to return the good |  Event: timeout that triggers a repercussion
|  Access to a physical good without transfer of ownership |  (non fungible) Token: transfer only a usage code associated to the Token, i.e. operation uses(token,L)$\rightarrow$ L
|  Prohibition of preventing the usage | Token held in custody in the smart contract
Digital License |  Permission, Prohibition, and Obligation | States and Events
| Currency and escrow | (divisible) Asset
| Usage and purchase |  Token: either transfer only an associated, and personal, usage code, or transfer the token, i.e. uses(token,L)$\rightarrow$ L and token$\multimap$ L
|  Off-chain constraints and Authority for dispute resolution |  _Implicitly_ trusted party included in agreement
Bet | Commitment and Obligation | Event
| Aleatory value | Event: timeout to decide the effective value
| Authority that decides the value |  _Explicitly_ trusted party included in agreement
Table 4:  Legal clauses of the archetypal legal acts and their encodings in
_Stipula_

##  8 Related works

A number of projects have put forward legal markup languages, to wrap logic
and other contextual information around traditional legal prose, and providing
templates for common contracts. OpenLaw [24] also allows to reference
Ethereum-based smart contracts into legal agreements, and automatically
trigger them once the agreement is digitally signed by all parties. Signatures
by all relevant parties are stored on IPFS (the Inter-Planetary File System)
and the Ethereum blockchain. The Accord project [22] provides an open,
standardized format for smart legal contracts, consisting of natural language
and computable components. These contracts can then be interpreted by machines
and they do not necessarily operate on blockchains. These projects come with
sets of templates for standard legal contracts, that can be customized by
setting template’s parameters with appropriate values. In _Stipula_ , rather
than software templates, it is possible to define specific programming
patterns that can be used to encode the building blocks of legal contracts.
(see the Table 4). Lexon [15] uses context free grammars to define a
programming language syntax that is at the same time human readable and
automatically translated into, _e.g._ Solidity. Even if the high level Lexon
code is very close to natural language, there is no real control over the code
that is actually run: the semantics of the high level language is not defined,
thus the actual behaviour of the contract is that of the automatically
generated Solidity code, which might be much more subtle than that of the
(much simpler and more abstract) Lexon source. Compared to the Solidity code
of the Lexon examples in [16], the _Stipula_ version of the same contracts is
much clearer, thanks to primitives like agreement and asset movements. Thus,
directly coding in _Stipula_ appears to be safer than relying on the Lexon-
Solidity pair. Nevertheless, it should be not difficult to design an automatic
translation from Lexon to _Stipula_ so to not bind Lexon contracts to any
specific implementation.

Our work aims at conducing a foundational study of legal contracts, in order
to elicit a precisely defined set of building blocks that can be used to
describe, analyse and execute (thus enforce) legal agreements. This is similar
to what has been done in [18], which puts forward a set of combinators
expressing financial and insurance contracts, together with a denotational
semantics and algebraic properties that says what such contracts are worth.
These ideas have been implemented by the Marlowe and Findel languages [5, 7],
which are (small) domain specific language featuring constructs like
participants, tokens, currency and timeouts to wait until a certain condition
becomes true (similarly to _Stipula_).

In Marlowe the control logic is fully embedded in the contract, that can
always progress (and close) even without the participation of a non
collaborative party. In particular, to ensure progress, urgency and default
refund mechanism, Marlowe always impose timeouts, even for money commitments
and money retrieval authorizations. However, this _pull_ mechanism makes the
interaction logic indirect and complex, whereas in _Stipula_ it is always
clear who is the subject of each action and where the assets flow. Setting the
correct timeouts in Marlowe may also become difficult, while in _Stipula_
timeouts are optional (using events) and default mechanisms can be programmed
as escape clauses that can be triggered by the Authority calling corresponding
functions. Otherwise, in _Stipula_ , the finite lifetime of a contract may be
easily programmed by arranging its value during the agreement phase, and
issuing a corresponding event in the initial state.

Marlowe semantics is written in Haskell and is executed on the Cardano
blockchain, where the lifetime of a contract and timeouts are computed in
terms of slot numbers, that are measured by (Cardano’s) block number. Then the
language interpreter takes as additional input the current slot interval, and
the contract will continue as the timeout-continuation as soon as any valid
transaction is issued after the timeout’s slot number is reached. Thus, the
execution of a contract will involve multiple blocks, with multiple steps in
each block. Moreover, the time limit $T$ used as timeouts must be intended as
$[T-\Delta,T+\Delta]$, where $\Delta$ is a parameter of the implementation.
Similar ideas can be exploited to implement _Stipula_ ’s events on top of
blockchains.

Overall, we remark that legal contracts are more general and more expressive
than financial contracts. Accordingly, DSLs like Marlowe and Findel are built
around a fixed set of contract’s _combinators_ , that can be combined
according to suitable (algebraic) laws. Then they can be implemented using an
interpreter, that is a single program that handles any financial contract by
evaluating its (most external) combinator. The case of _Stipula_ is more
complex: agreement, assets, events, named states and named functions are
programming primitives rather than combinators. Therefore each _Stipula_
contract must be implemented, actually compiled, into a suitable running
software, e.g. a Java application or a Ethereum smart contract, and the
parties must collaborate by invoking the contract’s functions to make the
contract progress.

Finally, the class-based programming style of _Stipula_ is similar to that of
Solidity, but there are many differences between the two. Actually, _Stipula_
is much similar to Obsidian [10], which is based on state-oriented programming
and explicit management of linear assets, whose usability has been
experimentally assessed [9]. Obsidian has a type system that ensures the
correct manipulations of objects according to their current states and that
linearly typed assets are not accidentally lost. On the contrary, _Stipula_ is
untyped: the introduction of a type discipline is orthogonal and is postponed
to a later stage where we plan to investigate static analysis techniques
specifically suitable to the legal setting. As a cons, Obsidian has no
agreement nor event primitives, therefore the consensus about the contract’s
terms and the enforcing of legal obligations must be implemented in a much
more indirect way.

##  9 Conclusions

This paper presents a domain-specific language for defining legal contracts
that can be automatized on a blockchain system. _Stipula_ features a distilled
number of operations that enable the formalisation of the main elements of
juridical acts, such as permissions, prohibitions, and obligations. _Stipula_
is formal and we are proud of its semantics – the legal bisimulation – that
allows one to equate contracts that differ for clauses (events) that can never
be triggered or for the order of non-interfering communications. Furthermore,
the _Stipula_ semantics has also been used for sketching an implementation on
top of the Ethereum blockchain.

We believe that a range of legal arrangements can be adequately translated
into _Stipula_ , using simple patterns for the key elements of legal contracts
(see the archetypal examples in the Appendix). Nevertheless we acknowledge
that legal contracts cannot be fully replaced by _Stipula_ contracts, since
the formers thoroughly use the flexibility and generality of natural
languages, may appeal to complex and undetermined social-normative concepts
(such as fairness or good faith), may need to be revised as circumstances
change, may need intelligent enforcements in case on non-compliance, etc. It
is matter of (our) future research to deeply investigate these
interdisciplinary aspects and provide at lest partial solutions.

From the computer science point of view, a number of issues deserve to be
investigated in full detail: the extension of the language with operations for
failures, devising linear type systems that enforce the partial correctness of
_Stipula_ codes, the implementation of the language, the definition of a
(formal) translation in _Stipula_ of a high level language, such as Lexon or
part of it, in order to relieve lawyers from understanding computer science
jargons.

Overall, we are optimistic that future research on _Stipula_ can
satisfactorily address the above issues because its model is simple and
rigorous, which are, in our opinion, fundamental criteria for reasoning about
legal contracts and for understanding their basic principles. In our mind,
_Stipula_ is the backbone of a framework where addressing and studying other,
more complex features that are drawn from juridical acts.

## Acknowledgements

Giovanni Sartor has been supported by the H2020 European Research Council
(ERC) Project “CompuLaw” (G.A. 833647). Cosimo Laneve has been partly
supported by the H2020-MSCA-RISE project ID 778233 “Behavioural Application
Program Interfaces (BEHAPI)”. Silvia Crafa dedicates this work to Università
di Padova and its 800th academic year. We are grateful to the law student
Alessandro Parenti for his help in constructing the legal examples in Section
7.

## References

  * [1] Solidity Documentation: State Machine Common Pattern.  https://docs.soliditylang.org/en/v0.8.0/common-patterns.html\\#state-machine.
  * [2] Malta MDIA Act.  At https://mdia.gov.mt/wp-content/uploads/2018/10/MDIA.pdf, 2018\.
  * [3] Obsidian: A safer blockchain programming language.  Language Site at http://obsidian-lang.com/, 2018.
  * [4] Smart contract legislation and enforceability in Italy.  Gazzetta Ufficiale, Law of 11 febbraio 2019, n. 12, Art. 8 ter, at https://www.gazzettaufficiale.it/eli/id/2019/02/12/19G00017/sg, 2019\.
  * [5] Cardano Documentation.  https://docs.cardano.org/, 2020.
  * [6] Wyoming Regulation Act.  At https://www.wyoleg.gov/Legislation/2021/SF0038, 2021.
  * [7] Alex Biryukov, Dmitry Khovratovich, and Sergei Tikhomirov.  Findel: Secure derivative contracts for ethereum.  In Financial Cryptography and Data Security - FC 2017, volume 10323 of Lecture Notes in Computer Science, pages 453–467. Springer, 2017\.
  * [8] Sam Blackshear, David L. Dill, Shaz Qadeer, Clark W. Barrett, John C. Mitchell, Oded Padon, and Yoni Zohar.  Resources: A safe language abstraction for money.  CoRR, 2020.
  * [9] Michael J. Coblenz, Jonathan Aldrich, Brad A. Myers, and Joshua Sunshine.  Can advanced type systems be usable? an empirical study of ownership, assets, and typestate in obsidian.  Proc. ACM Program. Lang., 4(OOPSLA):132:1–132:28, 2020.
  * [10] Michael J. Coblenz, Reed Oei, Tyler Etzel, Paulette Koronkevich, Miles Baker, Yannick Bloem, Brad A. Myers, Joshua Sunshine, and Jonathan Aldrich.  Obsidian: Typestate and assets for safer blockchain programming.  ACM Trans. Program. Lang. Syst., 42(3):14:1–14:82, 2020.
  * [11] A. Das, S. Balzer, J. Hoffmann, F. Pfenning, and I. Santurkar.  Resource-aware session types for digital contracts.  In 2021 2021 IEEE 34th Computer Security Foundations Symposium (CSF), pages 111–126, Los Alamitos, CA, USA, jun 2021. IEEE Computer Society.
  * [12] Sam Blackshear et al.  Move: A language with programmable resources.  https://developers.diem.com/main/docs/move-paper, 2021.
  * [13] Giusella Finocchiaro and Chantal Bomprezzi.  A legal analysis of the use of blockchain technology for the formation of smart legal contracts.  MediaLaws, July 2020.
  * [14] Ethereum Foundation.  Token Standards.  https://ethereum.org/en/developers/docs/standards/tokens/, 2015-21.
  * [15] Lexon Foundation.  Lexon Home Page.  http://www.lexon.tech, 2019.
  * [16] Lexon Foundation.  Lexon Demo Editor.  http://demo.lexon.tech/apps/editor/, 2020.
  * [17] Guido Governatori, Florian Idelberger, Zoran Milosevic, Regis Riveret, Giovanni Sartor, and Xiwei Xu.  On legal contracts, imperative and declarative smart contracts, and blockchain systems.  Artificial Intelligence and Law, 26:377–409, 2018.
  * [18] Simon L. Peyton Jones, Jean-Marc Eber, and Julian Seward.  Composing contracts: an adventure in financial engineering, functional pearl.  In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP ’00), Montreal, Canada, September 18-21, 2000, pages 280–292. ACM, 2000.
  * [19] Giuliano Lemme.  Blockchain, smart contracts, privacy, o del nuovo manifestarsi della volontà contrattuale.  In Giuffrè Francis Lefebvre, editor, Privacy digitale, pages 293–323. Italy, 2019.
  * [20] Robin Milner.  Communication and concurrency.  PHI Series in computer science. Prentice Hall, 1989.
  * [21] Margaret Jane Radin.  The deformation of contract in the information society.  Oxford Journal of Legal Studies, 37, 2017.
  * [22] Open Source Contributors.  The Accord Project.  https://accordproject.org, 2018.
  * [23] Research Group on EC Private Law (Acquis Group) Study Group on a European Civil Code.  Principles, Definitions and Model Rules of European Private Law: Draft Common Frame of Reference (DCFR), Outline Edition.  Sellier, 2009.
  * [24] Aaron Wright, David Roon, and ConsenSys AG.  OpenLaw Web Site.  https://www.openlaw.io, 2019.