1. Marlowe 3.0 tutorials

This document gives an overview of a set of Marlowe tutorials.

  1. Introducing Marlowe This tutorial gives an overview of the ideas behind Marlowe, as a domain-specific language embedded in Haskell. It also introduces commitments and timeouts, which are central to how Marlowe works in a blockchain context.

  2. A first example This tutorial introduces a simple financial contract in pseudocode, before explaining how it is modified to work in Marlowe, giving the first example of a Marlowe contract.

  3. The Marlowe model In this tutorial we look at our general approach to modelling contracts in Marlowe, and the context in which Marlowe contracts are executed: the Cardano blockchain. In doing this we also introduce some of the standard terminology that we will use in describing Marlowe.

  4. Marlowe step by step This tutorial explains the five ways of building contracts in Marlowe. Four of these – Pay, Let, If and When – build a complex contract from simpler contracts, and the fifth, Close, is a simple contract. In explaining these contracts we will also explain Marlowe values, observations and actions, which are used to supply external information and inputs to a running contract to control how it will evolve.

  5. Marlowe in Blockly Marlowe contracts can be built using the Blockly visual programming environment, as described in a series of videos making up this tutorial.

  6. The Marlowe data types This tutorial formally introduces Marlowe as a Haskell data type, as well as presenting the different types used by the model, and discussing a number of assumptions about the infrastructure in which contracts will be run.

  7. Embedded Marlowe This tutorial shows how to use some simple features of Haskell to write Marlowe contracts that are more readable, maintainable and reusable, by revisiting the escrow contract.

  8. Using Marlowe This tutorial shows you how to use Marlowe from within Haskell, and in particular shows how to exercise a contract using the semantics given earlier.

  9. The Marlowe Playground This tutorial introduces the Marlowe Playground, an online tool for creating embedded Marlowe contracts and interactively stepping through their execution.

  10. Potential problems with contracts This tutorial reviews how not to write Marlowe contracts, and what can go wrong when executing contracts even if they have been written correctly.

  11. Static analysis Marlowe contracts can be analysed without running them, and so, for instance, we can verify that a contract will always make the payments that it is required to, irrespective of the inputs that it receives. This tutoiral explains this, and how to run an analysis in the playground.

  12. ACTUS and Marlowe This tutorial gives an introduction to the general idea of the ACTUS taxonomy, plus examples implemented in Marlowe.

  13. Migrating to Marlowe 3.0 Here we explain how the current version of Marlowe is related to earlier versions, in particular version 1.3 and 2.0.

These tutorials address the current version of Marlowe, 3.0, which is implemented in the Marlowe Playground, and available here.

The version covered in the ISoLA paper, and supported in the original version of Meadow, is tagged as v1.3 and is available here.

2. Introducing Marlowe

This tutorial gives an overview of the ideas behind Marlowe, as a domain-specific language embedded in Haskell. It also introduces commitments and timeouts, which are central to how Marlowe works in a blockchain context.

2.1. Programming Languages and Domain-Specific Languages

The first computers were programmed in “machine code”. Each kind of system had a different code, and these codes were low-level and inexpressive: programs were long sequences of very simple instructions, incomprehensible to anyone who had not written them. Nowadays we are able to use higher-level languages like C, Java and Haskell to program systems. The same languages can be used on widely different machines, and the structure of the programs reflects what they do. On blockchain, their equivalents are languages like Plutus, Solidity and Simplicity. These higher-level languages are general purpose – they can be used to solve all sorts of different problems – but the solutions they express are still programs, and they still require programming skills to use them effectively.

In contrast, Marlowe is a domain-specific language (DSL) which is designed to be usable by someone who is expert in a particular field, rather than requiring programming skills to use it. In the case of Marlowe, the domain is the field of financial contracts.

Using a DSL has many advantages beyond its use by non-programmers:

  • We can ensure that certain sorts of bad programs cannot even be written, by designing those possibilities out of the language. By doing this we can aim to avoid some of the unanticipated exploits which have been a problem for existing blockchains.

  • We can also more easily check that programs have the properties that we want: for example, in the case of a Marlowe contract, we can make sure that the contract will never fail to make a payment that it should.

  • Because it is a DSL, we can build special-purpose tools to help people write programs in the language. In the case of Marlowe we can emulate how a contract will behave before it is run for real on the blockchain; this helps us to make sure that the contract we have written is doing what it is intended to.

Marlowe is also an embedded DSL, hosted in the Haskell programming language. While it is possible to use “pure” Marlowe if we wish, being embedded in a general-purpose language allows contract writers to selectively exploit features of Haskell in writing Marlowe contracts, making them easier to read, supporting re-use and so forth.

2.2. Marlowe in a nutshell

Marlowe is modelled on financial contract DSLs popularised in the last decade or so by academics and enterprises such as LexiFi, which provides contract software in the financial sector. In developing Marlowe, we have adapted these languages to work on blockchain. Marlowe is implemented on the Cardano blockchain, but could equally well be implemented on Ethereum or other blockchain platforms; in this respect it is “platform agnostic” just like modern programming languages like Java and C++. The Marlowe Playground online emulator tool allows you to experiment with, develop, simulate and analyse Marlowe contracts in your web browser, without having to install any software.

What does a Marlowe contract look like? It is built by combining a small number of building blocks that describe making a payment, making an observation of something in the “real world”, waiting until a certain condition becomes true, and so on.

2.3. Timeouts, deposits and commitments

Where we differ from non-blockchain approaches is in how we make sure that the contract is followed. This means not only that the instructions of the contract are not disobeyed – “nothing bad happens” – but also that the participants participate and don’t walk away early, leaving money locked up in the contract forever: “good things actually happen”. We do this using timeouts.

A contract can ask a participant to make a deposit of some funds, but obviously the contract cannot actually force a participant to make a deposit. Instead, the contract can wait for a period of time for the participant to commit to the contract: when that period of time expires, the contract moves on to follow some alternative instructions. This prevents a participant stopping a contract by not taking part, thus making sure that “things happen”.

All the constructs of Marlowe that require user participation – including user deposits and user choices – are protected by timeouts. Because of this, it is easy to see that the commitment made by a participant to a contract is finite: we can predict when the contract will have nothing left to do – when it can be closed – at this point any unspent funds left in the contract are refunded to participants, and the contract stops, or terminates. So, any funds put into the contract by a participant can’t be locked up forever: at this point the commitment effectively ends.

What is more, it is easy for us to read off from the contract when it will terminate, we call this the lifetime of the contract: all participants will therefore be able to find out this lifetime before taking part in the contract,

In our model, a running contract cannot force a deposit or a choice to happen: all it can do is to request a deposit or choice from a participant. In other words, for these actions it cannot “push”, but it can “pull”. On the other hand, it can make payments automatically, so some aspects of a Marlowe contract can “push” to make some things happen, e.g. ensuring that a payment is made to a participant by constructing an appropriate transaction output.

2.4. Marlowe in action

We are working on a production release of Marlowe on the Cardano blockchain early in 2020. From today, you are able to explore Marlowe for yourself, either by downloading it and using the Haskell implementation directly, or by using the online Marlowe Playground simulation tool; these are both covered in subsequent tutorials. These will also cover the details of Marlowe, introduce a series of examples, look deeper into the tools for Marlowe.

In the next six months we will be polishing the language design itself and developing a set of templates for popular financial instruments. Because Marlowe is a DSL we can work out how Marlowe contracts will behave without running them: this means that we can provide valuable diagnostics to potential participants before they commit to a contract, using static analysis. We can also use logic tools to formally prove properties of Marlowe contracts, giving users the highest level of assurance that their contracts behave as intended.

2.5. Where to go to find out more

This tutorial covers the latest version of Marlowe, while all but the first of these links covers Marlowe 1.3, which is very close to Marlowe 3.0 in conception but which differs in a number of detailed ways.

3. A first example

This tutorial introduces a simple financial contract in pseudocode, before explaining how it is modified to work in Marlowe, giving the first example of a Marlowe contract.

3.1. A simple escrow contract

Escrow

Suppose that alice wants to buy a cat from bob, but neither of them trusts the other. Fortunately, they have a mutual friend carol whom they both trust to be neutral (but not enough to give her the money and act as an intermediary). They therefore agree on the following contract, written using simple functional pseudocode. This kind of contract is a simple example of escrow.

When aliceChoice
     (When bobChoice
           (If (aliceChosen `ValueEQ` bobChosen)
               agreement
               arbitrate))

The contract is described using the constructors of a Haskell data type. The outermost constructor When has two arguments: the first is an observation and the second is another contract. The intended meaning of this is that when the observation becomes true, the second contract is activated.

The second contract is itself another When – asking for a decision from bob – but inside that, there is a choice: If alice and bob agree on what to do, it is done; if not, carol is asked to arbitrate and make a decision.

In fact, we can allow for the option of bob making the first choice, rather than alice, and so in general When offers a list of cases,[1] each with an action and a corresponding contract that is triggered when that action happens:

  When [ Case aliceChoice
              (When [ Case bobChoice
                          (If (aliceChosen `ValueEQ` bobChosen)
                             agreement
                             arbitrate) ],
        Case bobChoice
              (When [ Case aliceChoice
                          (If (aliceChosen `ValueEQ` bobChosen)
                              agreement
                              arbitrate) ]
       ]

In this contract, either Alice or Bob can make the first choice; the other then makes a choice. If they agree, then that is done; if not, Carol arbitrates.

Exercise

Think about executing this contract in practice. Suppose that Alice has already committed some money to the contract. What will happen if Bob chooses not to participate any further?

We have assumed that Alice has already committed her payment, but suppose that we want to design a contract to ensure that: what would we need to do to?

3.2. Escrow in Marlowe

Marlowe contracts incorporate extra constructs to ensure that they progress properly. Each time we see a When, we need to provide two additional things:

  • a timeout after which the contract will progress, and

  • the continuation contract to which it progresses.

3.3. Adding timeouts

First, let us examine how to modify what we have written to take care of the case that the condition of the When never becomes true. So, we add timeout and continuation values to each When occurring in the contract.

  When [ Case aliceChoice
              (When [ Case bobChoice
                          (If (aliceChosen `ValueEQ` bobChosen)
                             agreement
                             arbitrate) ]
                    60            -- ADDED
                    arbitrate),   -- ADDED
        Case bobChoice
              (When [ Case aliceChoice
                          (If (aliceChosen `ValueEQ` bobChosen)
                              agreement
                              arbitrate) ]
                    60            -- ADDED
                    arbitrate)    -- ADDED
        ]
        40            -- ADDED
        Close        -- ADDED

The outermost When calls for the first choice to be made by Alice or Bob: if neither of them has made a choice by time 40, the contract is closed and all the funds in the contract are refunded.

Close is typically the last step in every “path” through a Marlowe contract, and its effect is to refund the money in the contract to the participants; we will describe this in more detail in a later tutorial. In this particular case, refund will happen after 40 slots.

Looking at the inner constructs, if a choice has been made, then we wait for a second one. If that is not forthcoming by slot 60, then Carol is called upon to arbitrate.[2]

3.4. Adding commitments

Next, we should look at how cash is committed as the first step of the contract.

 When [Case (Deposit "alice" "alice" ada price)   -- ADDED
  (When [ Case aliceChoice
              (When [ Case bobChoice
                          (If (aliceChosen `ValueEQ` bobChosen)
                             agreement
                             arbitrate) ]
                    60
                    arbitrate),
        Case bobChoice
              (When [ Case aliceChoice
                          (If (aliceChosen `ValueEQ` bobChosen)
                              agreement
                              arbitrate) ]
                    60
                    arbitrate)
        ]
        40
        Close)
    ]
    10                                       -- ADDED
    Close                                   -- ADDED

A deposit of price is requested from "alice": if it is given, then it is held in an account, also called "alice". Accounts like this exist for the life of the contract only; each account belongs to a single contract.

There is a timeout of 10 slots on making the deposit; if that is reached without a deposit being made, the contract is closed and all the money already in the contract is refunded. In this case, that is simply the end of the contract.

3.5. Definitions

We will see later that parts of this contract description, such as arbitrate, agreement, and price, use the Haskell embedding of Marlowe DSL to give some shorthand definitions. We also use overloaded strings to make some descriptions – e.g. of accounts – more concise.

These are discussed in more detail when we look at embedded Marlowe.

Exercise

Comment on the choice of timeout values, and look at alternatives.

For example, what would happen if the timeout of 40 on the When were to be replaced by 60, and vice versa? Would it be sensible to have the same timeout, of 100 say, on each When? If not, why not?

This example has shown many of the ingredients of the Marlowe contract language; in the next tutorial we will present the complete language.

3.6. Notes

  • While accounts names need to be provided manually in the example here, these could be generated by users’ wallets in a version of Marlowe deployed on a blockchain.

4. The Marlowe model

Marlowe is designed to support the execution of financial contracts on blockchain, and specifically to work on Cardano. Contracts are built by putting together a small number of constructs that in combination can be used to describe many different kinds of financial contract.

Before we describe those constructs, we need to look at our general approach to modelling contracts in Marlowe, and the context in which Marlowe contracts are executed, the Cardano blockchain. In doing this we also introduce some of the terminology that we will use, indicating definitions by italics.

4.1. Contracts

Contracts in Marlowe run on a blockchain, but need to interact with the off-chain world. The parties to the contract, whom we also call the participants, can engage in various actions: they can be asked to deposit money, or to make a choice between various alternatives. A notification of an external value (also called an oracle value), such as the current price of a particular commodity, is the other possible form of input.[3]

Running a contract will also produce external effects, by making payments to parties in the contract.

Accounts

The Marlowe model allows for a contract to control money in a number of disjoint accounts: this allows for more explicit control of how the money flows in the contract. Each account is owned by a particular party to the contract, and that party receives a refund of any remaining funds in the account when the contract is closed.[4] These accounts are local, in that they only exist as during the execution of the contract, and during that time they are only accessible by parties to the contract.

Steps and states

Marlowe contracts describe a series of steps, typically by describing the first step, together with another (sub-) contract that describes what to do next. For example, the contract Pay a p t v cont says “make a payment of value v of token t to the party p from the account a, and then follow the contract cont”. We call cont the continuation of the contract.

In executing a contract we need to keep track of the current contract: after making a step in the example above, the current contract is the continuation, cont. We also have to keep track of some other information, such as how much is held in each account: we call this information the state: this potentially changes at each step too. A step can also see an action taking place, such as money being deposited, or an effect being produced, e.g. a payment.

4.2. Blockchain

While Marlowe is designed to work with blockchains in general,[5] some details of how it interacts with the blockchain are relevant when describing the semantics and implementation of Marlowe.

A UTxO-based blockchain is a chain of blocks, each of which contains a collection of transactions. Each transaction has a set of inputs and outputs, and the blockchain is built by linking unspent transaction outputs (UTxO) to the inputs of a new transaction. At most one block can be generated in each slot, which are 20 seconds long.

The mechanisms by which these blocks are generated, and by whom, are not relevant here, but contracts will be expressed in terms of slot numbers, counting from the starting (“genesis”) block of the blockchain.

UTxO and wallets

Value on the blockchain resides in the UTxO, which are protected cryptographically by a private key held by the owner. These keys can be used to redeem the output, and so to use them as inputs to new transactions, which can be seen as spending the value in the inputs. Users typically keep track of their private keys, and the values attached to them, in a cryptographically-secure wallet.

It is through their wallets that users are able to interact with smart contracts - including Marlowe contracts – running on the blockchain. Deposits are made from users’ wallets, and payments received by them. Note, however, that these are definitely off chain actions that need to be controlled by code running in the user’s wallet: they cannot be made to happen by the Marlowe contract itself.

Value

In previous examples, whenever a Value was required, we have exclusively used Ada. This makes a lot of sense, seeing as Ada is the fundamental currency supported by Cardano.

Plutus offers a more general concept of value, though, supporting custom fungible, non-fungible, and mixed tokens

What is a Value in Plutus?

newtype Value = Value
    {getValue :: Map CurrencySymbol (Map TokenName Integer)}

The types CurrencySymbol and TokenName are both simple wrappers around ByteString.

This notion of value encompasses Ada, fungible tokens (think currencies), non-fungible tokens (a custom token that is not interchangeable with other tokens), and more exotic mixed cases:

  • Ada has the empty bytestring as CurrencySymbol and TokenName.

  • A fungible token is represented by a CurrencySymbol for which there is exactly one TokenSymbol which can have an arbitrary non-negative integer quantity (of which Ada is a special case).

  • A class of non-fungible tokens is a CurrencySymbol with several TokenNames, each of which has a quantity of one. Each of these names corresponds to one unique non-fungible token.

  • Mixed tokens are those with several TokenNames and quantities greater than one.

Cardano and Plutus provide a simple way to introduce a new currency by forging it using monetary policy scripts. This effectively embedds Ethereum ERC-20/ERC-721 standards as primitive values in Cardano.

4.3. Executing a Marlowe contract

Executing a Marlowe contract on Cardano blockchain means constraining user-generated transactions according to the contract’s logic. If a contract expects a deposit of 100 Ada from Alice, only such a transaction will succed, anything else will be rejected.

A transaction contains an ordered list of inputs. Marlowe interpreter is executed during transaction validation. First, it evaluates the contract step by step until it cannot be changed any further without processing any input, a condition that we call being quiescent. At this stage we progress through When with passed timeouts, If, Let, Pay, and Close constructs without consuming any inputs.

The first input is then processed, and then the contract is single stepped again until quiescence, and this process is repeated until all the inputs are processed. At each step the current contact and the state will change, some input may be processed, and payments made.

Such a transaction, as shown in the diagram below, is added to the blockchain. What we do next is to describe in detail what Marlowe contracts look like, and how they are evaluated step by step.

Building a transaction

transaction

5. Marlowe step by step

Marlowe has five ways of building contracts. Four of these – Pay, Let, If and When – build a complex contract from simpler contracts, and the fifth, Close, is a simple contract. At each step of execution, as well as returning a new state and continuation contract, it is possible that effects – payments – and warnings can be generated too.

In explaining these contracts we will also explain Marlowe values, observations and actions, which are used to supply external information and inputs to a running contract to control how it will evolve.

5.1. Pay

A payment contract Pay a p t v cont will make a payment of value v of token t from the account a to a payee p, which will be one of the contract participants or another account in the contract. Warnings will be generated if the value v is negative, or if there is not enough in the account to make the payment in full (even if there are positive balances of other tokens in the account). In that case a partial payment (of all the money available) is made. The continuation contract is the one given in the contract: cont.

5.2. Close

A contract Close provides for the contract to be closed (or terminated). The only action that is performs is to provide refunds to the owners of accounts that contain a positive balance. This is performed one account per step, but all accounts will be refunded in a single transaction.

Before discussing other forms of contracts, we need to describe values, observations and actions.

5.3. Values, observations and actions

Values include some quantities that change with time, including “the current slot number”,[6] “the current balance of some token in an account”, and any choices that have already been made; we call these volatile values. Values can also be combined using addition, subtraction and negation.

Observations are Boolean values derived by comparing values, and can be combined using the standard Boolean operators. It is also possible to observe whether any choice has been made (for a particular identified choice).

Observations will have a value at every step of execution. On the other hand, actions happen at particular points during execution. As noted earlier, actions can be

  • depositing money,

  • making a choice between various alternatives, or

  • notifying an external or oracle value, such as the current price of a particular commodity.

5.4. If

The conditional If obs cont1 cont2 will continue as cont1 or cont2, depending on the Boolean value of the observation obs when this construct is executed.

5.5. When

This is the most complex constructor for contracts, with the form When cases timeout cont. It is a contract that is triggered on actions, which may or may not happen at any particular slot: what happens when various actions happen is described by the cases in the contract.

In the contract When cases timeout cont, the list cases contains a collection of cases. Each case has the form Case ac co where ac is an action and co a continuation (another contract). When a particular action, e.g. ac, happens, the state is updated accordingly and the contract will continue as the corresponding continuation co.

In order to make sure that the contract makes progress eventually, the contract When cases timeout cont will continue as cont once the timeout, a slot number, is reached.

5.6. Let

A let contract Let id val cont allows a contract to name a value using an identifier. In this case, the expression val is evaluated, and stored with the name id. The contract then continues as cont.

As well as allowing us to use abbreviations, this mechanism also means that we can capture and save volatile values that might be changing with time, e.g. the current price of oil, or the current slot number, at a particular point in the execution of the contract, to be used later on in contract execution.

6. Marlowe in Blockly

So far in these tutorials we have concentrated on building contracts in the textual version of Marlowe, embedded in Haskell, Marlowe contracts can also be built using the Blockly visual programming environment, as described in this series of videos.

7. The Marlowe data types

This tutorial formally introduces Marlowe as a Haskell data type, as well as presenting the different types used by the model, and discussing a number of assumptions about the infrastructure in which contracts will be run. The code that we describe here comes from the Haskell modules Semantics.hs and Util.hs.

7.1. Marlowe

The Marlowe domain-specific language (DSL) is modelled as a collection of algebraic types in Haskell, with contracts being given by the Contract type:

data Contract = Close
              | Pay AccountId Payee Token Value Contract
              | If Observation Contract Contract
              | When [Case] Timeout Contract
              | Let ValueId Value Contract
              | Assert Observation Contract

We saw in the previous tutorial what these contracts do. In the rest of this tutorial we will dig a bit deeper into the Haskell types that are used to represent the various components of the contracts, including accounts, values, observations, and actions. We will also look at types that relate to the execution of contracts, including inputs, states, the environment.

7.2. Basic components

In modelling basic parts of Marlowe we use a combination of Haskell data types, that define new types, and type synonyms that give a new name to an existing type.[7]

A Marlowe Account holds amounts of multiple currencies and/or fungible and non-fungible tokens. A concrete amount is indexed by a Token, which is a pair of CurrencySymbol and TokenName. You can think of an Account as a Map Token Integer, where

data Token = Token CurrencySymbol TokenName

Cardano’s Ada token is Token adaSymbol adaToken. But you are free to create your own currencies and tokens.

Tokens of a currency can represent roles in a contract, e.g "buyer" and "seller". Think of a legal contract in the sense of "hereafter referred to as the Performer/Vendor/Artist/Consultant". This way we can decouple the notion of ownership of a contract role, and make it tradable. So you can sell your loan or buy a share of a role in some contract.

tradeRoles = CurrencySymbol "TradeRoles"
buyer = TokenName "buyer"
seller = TokenName "seller"
account = fromList[(Token tradeRoles buyer, 1), (ada 1000)]

Here account holds a buyer token of currency "TradeRoles", and 1000 Ada.

A Party is represented as either a public key hash or a role name.

data Party  = PK PubKeyHash | Role TokenName

In order to progress a Marlowe contract, a party must provide an evidence. For PK party that would be a valid signature of a transaction signed by a private key of a public key that hashes to party’s PubKeyHash, similarly to Bitcoin’s Pay to Public Key Hash mechanism. For a Role party the evidence is spending a role token within the same transaction, usually to the same owner.

So, Role parties will look like (Role "alice"), (Role "bob") and so on. However, Haskell allows us to present and read in these values more concisely (by declaring a custom instance of Show and using overloaded strings) so that these can be input and read as "alice", "bob" etc.

Slot numbers and amounts of money are treated in a similar way; with the same show/overload approach they will appear in contracts as numbers:

data Slot    = Slot Integer
type Timeout = Slot

Accounts have a number NumAccount and an owner, who is a Party to the contract.

type NumAccount = Integer
data AccountId  = AccountId NumAccount Party

and an example would be AccountId 0 "alice". Note that "alice" is the owner here in the sense that she will be refunded any money in the account when the contract terminates.

Because in many contracts, each party will own at most one account, we can use overloaded strings to allow us to abbreviate this account – account number 0 for any owner – by the name of its owner: in this case "alice".

A payment can be made to one of the parties to the contract, or to one of the accounts of the contract, and this is reflected in the definition

data Payee = Account AccountId
           | Party Party

Choices – of integers – are identified by ChoiceId which combines a name for the choice with the Party who had made the choice:

type ChoiceName = Text
data ChoiceId   = ChoiceId ChoiceName Party
type ChosenNum  = Integer

Values, as defined using Let are also identified by integers.[8]

data ValueId    = ValueId Integer

7.3. Values, observations and actions

Building on the basic types, we can describe three higher-level components of contracts: a type of values, on top of that a type of observations, and also a type of actions, which trigger particular cases. First, looking at Value we have

data Value = AvailableMoney AccountId Token
           | Constant Integer
           | NegValue Value
           | AddValue Value Value
           | SubValue Value Value
           | MulValue Value Value
           | Scale Rational Value
           | ChoiceValue ChoiceId
           | SlotIntervalStart
           | SlotIntervalEnd
           | UseValue ValueId
           | Cond Observation Value Value

The different kinds of values – all of which are Integer – are pretty much self explanatory, but for completeness we have

  • Lookup of the value in an account AvailableMoney, made in a choice ChoiceValue and in an identifier that has already been defined UseValue.

  • Arithmetic constants and operators.

  • Scale multiplies a Value by a rational constant, say, 2/3, and rounds the result using 'half even' aka 'banking' rounding. So, 14/10 rounds to 1, both 15/10 and 25/10 rounds to 2.

  • The start and end of the current slot interval; see below for further discussion of this.

  • Cond represents if-expressions, that is - first argument to Cond is a condition (Observation) to check, second is a Value to take when condition is satisfied and the last one is a Value for unsatisfied condition; for example: (Cond FalseObs (Constant 1) (Constant 2)) is equivalent to (Constant 2)

  • Assert does not have any effect on the state of the contract, but it issues a warning when the Observation is false. It can be used to ensure that a property holds in any given point of the contract, since static analysis will fail if any execution causes an Assert to be false.

Next we have observations

data Observation = AndObs Observation Observation
                 | OrObs Observation Observation
                 | NotObs Observation
                 | ChoseSomething ChoiceId
                 | ValueGE Value Value
                 | ValueGT Value Value
                 | ValueLT Value Value
                 | ValueLE Value Value
                 | ValueEQ Value Value
                 | TrueObs
                 | FalseObs

These are really self-explanatory: we can compare values for (in)equality and ordering, and combine observations using the Boolean connectives. The only other construct ChoseSomething indicates whether any choice has been made for a given ChoiceId.

Cases and actions are given by these types:

data Case = Case Action Contract

data Action = Deposit AccountId Party Token Value
            | Choice ChoiceId [Bound]
            | Notify Observation

data Bound = Bound Integer Integer

Three kinds of action are possible:

  • A Deposit n p t v makes a deposit of value v of token t into account number n belonging to party p.

  • A choice is made for a particular id with a list of bounds on the values that are acceptable. For example, [Bound 0 0, Bound 3 5] offers the choice of one of 0, 3, 4 and 5.

  • The contract is notified that a particular observation be made. Typically this would be done by one of the parties, or one of their wallets acting automatically.

This completes our discussion of the types that make up Marlowe contracts.

7.4. Dynamic data

As we noted earlier, the semantics of Marlowe consist in building transactions, like this:

transaction A transaction is built from a series of steps, some of which consume an input value, and others produce effects, or payments. In describing this we explained that a transaction modified a contract (to its continuation) and the state, but more precisely we have a function

computeTransaction :: TransactionInput -> State -> Contract -> TransactionOutput

where the types are defined like this:

data TransactionInput = TransactionInput
    { txInterval :: SlotInterval
    , txInputs   :: [Input] }

data TransactionOutput =
    TransactionOutput
        { txOutWarnings :: [ReduceWarning]
        , txOutPayments :: [Payment]
        , txOutState    :: State
        , txOutContract :: Contract }
    | Error TransactionError

The notation used here adds field names to the arguments of the constructors, giving selectors for the data as well as making in clearer the purpose of each field.

The TransactionInput type has two components: the SlotInterval in which it can validly be added to the blockchain, and an ordered sequence of Input values to be processed in that transaction.

A TransactionOutput value has four components: the last two are the updated State and Contract, while the second gives a ordered sequence of Payments produced by the transaction. The first component contains a list of any warnings produced by processing the transaction.

7.5. Slot ranges

This is part of the architecture of Cardano/Plutus, which acknowledges that it is not possible to predict precisely in which slot a particular transaction will be processed. Transactions are therefore given a slot interval in which they are expected to be processed, and this carries over to Marlowe: each step of a Marlowe contract is processed in the context of a range of slots.

data Slot         = Slot Integer
data SlotInterval = SlotInterval Slot Slot

ivFrom, ivTo :: SlotInterval -> Slot
ivFrom (SlotInterval from _) = from
ivTo   (SlotInterval _ to)   = to

How does this affect the processing of a Marlowe contract? Each step is processed relative to a slot interval, and the current slot value needs to lie within that interval.

The endpoints of the interval are accessible as the values SlotIntervalStart and SlotIntervalEnd, and these can be used in observations. Timeouts need to be processed unambiguously, so that all values in the slot interval have to either have exceeded the timeout for it to take effect, or fall before the timeout, for normal execution to take effect. In other words, the timeout value needs to either be less or equal than SlotIntervalStart (in order for the timeout to take effect) or be strictly greater than SlotIntervalEnd (for normal execution to take place).

Notes

The model makes a number of assumptions about the blockchain infrastructure in which it is run.

  • It is assumed that cryptographic functions and operations are provided by a layer external to Marlowe, and so they need not be modelled explicitly.

  • We assume that time is “coarse grained” and measured by block or slot number, so that, in particular, timeouts are delimited using block/slot numbers.

  • Making a deposit is not something that a contract can perform; rather, it can request that a deposit is made, but that then has to be established externally: hence the input of (a collection of) deposits for each transaction.

  • The model manages the refund of funds back to the owner of a particular account when a contract reaches the point of Close.

8. Embedded Marlowe

In this tutorial we go back to the escrow example, and show how we can use the embedding of Marlowe in Haskell to make more readable, modular and reusable descriptions of Marlowe contracts.

8.1. A simple escrow contract, revisited.

Escrow

Recall that we developed this Marlowe contract in our earlier tutorial.

While we presented it there as a “monolothic” contract, we can use Haskell definitions to make it more readable. To start with, we can separate the initial commitment from the inner working part of the contract:

contract :: Contract
contract = When [Case (Deposit "alice" "alice" ada price) inner]
                10
                Close

inner :: Contract
inner =
  When [ Case aliceChoice
              (When [ Case bobChoice
                          (If (aliceChosen `ValueEQ` bobChosen)
                             agreement
                             arbitrate) ]
                    60
                    arbitrate),
        Case bobChoice
              (When [ Case aliceChoice
                          (If (aliceChosen `ValueEQ` bobChosen)
                              agreement
                              arbitrate) ]
                    60
                    arbitrate)
        ]
        40
        Close

Many of the terms here are themselves defined within Haskell. Principally, we have the two contracts that deal with what happens when there is agreement between Alice and Bob, and if not, how Carol should arbitrate between them:

agreement :: Contract
agreement =
  If
    (aliceChosen `ValueEQ` (Constant 0))
    (Pay "alice" (Party "bob") ada price Close)
    Close

arbitrate :: Contract
arbitrate =
  When  [ Case carolClose Close,
          Case carolPay (Pay "alice" (Party "bob") ada price Close) ]
        100
        Close

Within these contracts we are also using simple abbreviations such as

price :: Value
price = Constant 450

which indicates the price of the cat, and so the value of the money under escrow.

We can also describe the choices made by Alice and Bob, noting that we’re also asked for a default value defValue just in case the choices have not been made.

aliceChosen, bobChosen :: Value

aliceChosen = ChoiceValue (ChoiceId choiceName "alice")
bobChosen   = ChoiceValue (ChoiceId choiceName "bob")

defValue = Constant 42

choiceName :: ChoiceName
choiceName = "choice"

In describing choices we can give sensible names to the numeric values:

pay,refund,both :: [Bound]

pay    = [Bound 0 0]
refund = [Bound 1 1]
both   = [Bound 0 1]

and define new functions (or “templates”) for ourselves. In this case we define

choice :: Party -> [Bound] -> Action

choice party bounds =
  Choice (ChoiceId choiceName party) bounds

as a way of making the expression of choices somewhat simpler and more readable:

alicePay, aliceRefund, aliceChoice :: Action
alicePay    = choice "alice" pay
aliceRefund = choice "alice" refund
aliceChoice = choice "alice" both

Given all these definitions, we are able to write the contract at the start of this section in a way that makes its intention clear. Writing in ``pure'' Marlowe, or by expanding out these definitions, we would have this contract instead:

When [
  (Case
     (Deposit
        (AccountId 0 "alice") "alice" ada
        (Constant 450))
     (When [
           (Case
              (Choice
                 (ChoiceId "choice" "alice") [
                 (Bound 0 1)])
              (When [
                 (Case
                    (Choice
                       (ChoiceId "choice" "bob") [
                       (Bound 0 1)])
                    (If
                       (ValueEQ
                          (ChoiceValue
                             (ChoiceId "choice" "alice"))
                          (ChoiceValue
                             (ChoiceId "choice" "bob")))
                       (If
                          (ValueEQ
                             (ChoiceValue
                                (ChoiceId "choice" "alice"))
                             (Constant 0))
                          (Pay
                             (AccountId 0 "alice")
                             (Party "bob") ada
                             (Constant 450) Close) Close)
                       (When [
                             (Case
                                (Choice
                                   (ChoiceId "choice" "carol") [
                                   (Bound 1 1)]) Close)
                             ,
                             (Case
                                (Choice
                                   (ChoiceId "choice" "carol") [
                                   (Bound 0 0)])
                                (Pay
                                   (AccountId 0 "alice")
                                   (Party "bob") ada
                                   (Constant 450) Close))] 100 Close)))] 60
                 (When [
                       (Case
                          (Choice
                             (ChoiceId "choice" "carol") [
                             (Bound 1 1)]) Close)
                       ,
                       (Case
                          (Choice
                             (ChoiceId "choice" "carol") [
                             (Bound 0 0)])
                          (Pay
                             (AccountId 0 "alice")
                             (Party "bob") ada
                             (Constant 450) Close))] 100 Close)))
           ,
           (Case
              (Choice
                 (ChoiceId "choice" "bob") [
                 (Bound 0 1)])
              ... similarly to the "alice" case above ...

Exercises

What other abbreviations could you add to the contract at the top of the page?

Can you spot any functions that you could define to make the contract shorter, or more modular?

This example has shown how embedding in Haskell gives us a more expressive language, simply by reusing some of the basic features of Haskell, namely definitions of constants and functions. In the next tutorial you will learn about how to exercise Marlowe contracts in ghci.

Note
  • This contracts is contained in the modules EscrowSimpleV2.hs

  • The expanded version comes from the Marlowe Playground, which supports expansion of embedded definitions into pure Marlowe..

9. Using Marlowe

This tutorial shows you how to use Marlowe from within Haskell, and in particular shows how to exercise a contract using the semantics given earlier.

9.1. Marlowe in Haskell

This tutorial works in version 3.0 of Marlowe which can be found in the master branch of the repository:

git clone https://github.com/input-output-hk/marlowe.git
cd marlowe

9.2. Stepping through contracts

As we saw earlier the semantics of a single transaction are defined by the function

computeTransaction :: TransactionInput -> State -> Contract -> TransactionOutput

where the types are defined like this:

data TransactionInput = TransactionInput
    { txInterval :: SlotInterval
    , txInputs   :: [Input] }

data TransactionOutput =
    TransactionOutput
        { txOutWarnings :: [ReduceWarning]
        , txOutPayments :: [Payment]
        , txOutState    :: State
        , txOutContract :: Contract }
    | Error TransactionError

and States are defined like this, with a helper function to define an initially empty state:

data State = State { accounts :: Map AccountId Money
                   , choices  :: Map ChoiceId ChosenNum
                   , boundValues :: Map ValueId Integer
                   , minSlot :: Slot }

emptyState :: Slot -> State
emptyState sn = State { accounts = Map.empty
                      , choices = Map.empty
                      , boundValues = Map.empty
                      , minSlot = sn }

We can use the facilities of ghci to step through a contract one transaction at a time, and, here, we will do that with the embedded escrow contract contained in EscrowSimmpleV2.hs.

To single step, you can work in ghci like this, using the facility to make local bindings:

Prelude> :set -XOverloadedStrings
Prelude> :l Language/Marlowe/Examples/EscrowSimpleV2.hs
 ...
*Lang...V2> let (TransactionOutput txWarn1 txPay1 state1 con1) = computeTransaction (TransactionInput (0, 0) [IDeposit "alice" "alice" ada 450]) (emptyState 0) contract

In doing this we have pattern matched the output of an application of computeTransaction, which takes three inputs: the second is an initial state (at slot number 0) and the third is the initial escrow contract. The first is a TransactionInput which contains a SlotInterval – here SlotInterval 0 0 – and a deposit of 450 Lovelace from "alice" into her account "alice" namely IDeposit "alice" "alice" ada 450.

If you want to try this for yourself in ghci, you can copy and paste from the code examples: they are in horizontally scrolling windows.

The output is matched with TransactionOutput txWarn1 txPay1 state1 con1 so that we can examine the various components separately:

*Lang...V2> txWarn1
[]
*Lang...V2> txPay1
[]
*Lang...V2> state1
State {accounts = fromList [((AccountId 0 "alice", ada), 450)], choices = fromList [], boundValues = fromList [], minSlot = 0}
*Lang...V2> con1
When [Case (Choice (ChoiceId "choice" "alice") [Bound 0 1])
 ...

This shows that the transaction generates no warnings or payments, but updates the state to show the balance in the account "alice", and updates the contract, ready to receive a choice from Alice or Bob.

In the next state the contract is waiting for input, and if both Alice and Bob agree to make a payment to Bob by choosing 0, then a payment to Bob is generated. This is verified through this interaction in GHCI:

*Lang...V2> let (TransactionOutput txWarn2 txPay2 state2 con2) = computeTransaction (TransactionInput (SlotInterval 0 0) [IChoice (ChoiceId "choice" "alice") 0, IChoice (ChoiceId "choice" "bob") 0]) state1 con1
*Lang...V2> txPay2
[Payment "bob" ada 450]
*Lang...V2> con2
Close
*Lang...V2> state2
State {accounts = fromList [], choices = fromList [(ChoiceId "choice" "alice",0),(ChoiceId "choice" "bob",0)], boundValues = fromList [], minSlot = 0}

An alternative way of doing this is to add these definitions to a working file, e.g. Build.hs, where these definitions will be preserved. Indeed, it would be very sensible to include some of the definitions used above in such a file.

9.3. Alternative routes through the contract

The local bindings are lost each time a :load or :l command is performed, so doing that allows us to re-use some earlier commands. An alternative execution of the contract is given by

  • First step: Alice deposits money as in the earlier example.

  • Second step: Alice and Bob select different options. This can be done like this:

*Lang...V2> let (TransactionOutput txWarn2 txPay2 state2 con2) = computeTransaction (TransactionInput (SlotInterval 0 0) [IChoice (ChoiceId "choice" "alice") 0, IChoice (ChoiceId "choice" "bob") 1]) state1 con1
*Lang...V2> con2
When [Case (Choice (ChoiceId "choice" "carol") [Bound 1 1]) Close, Case (Choice (ChoiceId "choice" "carol") [Bound 0 0]) (Pay (AccountId 0 "alice") (Party "bob") ada (Constant 450) Close)] 100 Close
*Lang...V2> state2
State {accounts = fromList [((AccountId 0 "alice", ada), 450)], choices = fromList [(ChoiceId "choice" "alice",0),(ChoiceId "choice" "bob",1)], boundValues = fromList [] , minSlot = 0}

This shows that we’re now in a contract where the choice is up to Carol, and that there is still the 450 Lovelace in the "alice" account.

  • Third step: Carol makes a choice. If she chooses 0, payment to Bob is made. If she chooses 1, Alice is refunded. Let’s do that now:

*Lang...V2> let (TransactionOutput txWarn3 txPay3 state3 con3) = computeTransaction  (TransactionInput (SlotInterval 0 0) [IChoice (ChoiceId "choice" "carol") 1]) state2 con2
*Lang...V2> txPay3
[Payment "alice" ada 450]
*Lang...V2> con3
Close
*Lang...V2> state3
State {accounts = fromList [], choices = fromList [(ChoiceId "choice" "alice",0), (ChoiceId "choice" "bob",1),(ChoiceId "choice" "carol",1)], boundValues = fromList [], minSlot = 0}

So now the contract is ready to Close, and so to refund any remaining money, but it is clear from state3 that there are no accounts containing non-zero balances, and so the contract is terminated.

Why is single stepping useful? It is the equivalent of debugging, and we are able to see the internal state of the contract at each stage, the contract continuation, i.e. what remains to be executed, and the actions produced at each step.

Exercise

Explore some other ways of engaging with the contract - What happens when Bob and Alice choose to refund the money to Alice? - What happens if Bob and Alice disagree, but Carol sides with Bob?

9.4. There must be an easier way!

Yes, there is!

We look next at our tool, the Marlowe Playground, that will capitalise on the fact that we are working in a DSL to automate picking the right inputs and allow users to interact with contracts.

10. The Marlowe Playground

This tutorial gives an overview of the Marlowe Playground, an online tool that allows users to create, to analyse, to interact with and to simulate the operation of embedded Marlowe contracts. It is available at https://alpha.marlowe.iohkdev.io.

10.1. Introducing the Marlowe Playground

For Marlowe to be usable in practice, users need to be able to understand how contracts will behave once deployed to the blockchain, but without doing the deployment. We can do that by simulating their behaviour off-chain, interactively stepping through the evaluation of a contract in the browser-based tool, the Marlowe Playground, a web tool that supports the interactive construction, revision, and simulation of smart-contracts written in Marlowe.

The playground has three top-level tabs,

  • The Haskell Editor

  • The Simulator

  • Blockly, the visual editor

and we look at these three in turn now.

We use bold type for buttons and other components in what follows.

10.2. The Haskell Editor: developing embedded contracts

The editor supports the development of Marlowe contracts, described in Haskell. We can use Haskell to make contract definitions more readable by using Haskell definitions for sub-components, abbreviations, and simple template functions. The Haskell editor tab is shown in the following image.

The Haskell editor

The figure shows that the tool is in the Haskell editor pane (number 1 in the diagram). The tool contains a number of example contracts, and in this case we are looking at the “escrow” contract (number 2). To describe a Marlowe contract in the editor, we have to define a top-level value contract of type Contract (number 3); it is this value that is converted to pure Marlowe with the Compile button (number 4), and which we can Send to simulator with the eponymous button (number 5).

10.3. Simulating Marlowe contracts

The second tab in the Marlowe Playground allows users to simulate Marlowe contracts transaction by transaction. Typically these are contracts developed in the Haskell editor or within Blockly, but they can also be entered and modified in the editor pane here too.

The Simulation tab

The simulation tab is selected on the left-hand side of the screen (number 1 in the figure). At the foot of this side of the screen, and on all tabs, is a link to the online tutorial for Marlowe (number 2). The pane also contains a number of example contracts, and these are selected above the main editor window (number 3).

Contracts in the simulator can be transferred to the Blockly visual editor (button number 4), and if you have a GitHub account, it’s also possible to save contracts that you develop as GitHub gists (number 5). To do this, log into your account using the Log in button at the top right of the screen. You will then see buttons to allow you to Publish or save contracts as gists, and to Load contracts from GitHub.

The tile at the foot of the window (number 6) gives information about the current contract and its state. The tab shown here will give information about the state of execution of the Marlowe contract, including the values held in the various accounts of the contract, choices and payments made, the current block number and so on. Other tabs give access to static analysis and its results, as well as other warnings and errors.

In simulating a contract there are two stages

  • Inputs are chosen, and form part of

  • Transactions that aggregate a number of inputs and payments.

Inputs are chosen (number 7) from the inputs that are relevant at the particular point of the contract. By relevant here we mean that these are the (only) inputs that will make the contract progress at this stage. In other words, input choice is "intelligent". An input is added to the transaction that is being built by selecting the + button (number 7).

Once the relevant inputs have been chosen, and these appear here in the box (number 8), the transaction can be added to the chain by selecting Apply. But other controls are available here too:

  • Next block will advance the current block number.

  • Undo will undo the last action made in the simulator. This means that we can explore a contract interactively, making some moves, undoing some of them, and then proceeding in a different direction.

  • Reset will reset the contract and its state back to their initial values: the full contract and an empty state.

In the bottom right-hand corner (number 9) is a box for contextual help information.

10.4. Building contracts with Blockly

The playground provides a mechanism for creating and viewing contracts in a visual form, rather than in text. This is given by the third tab in the playground.

The Blockly tab

The Blockly tab is indicated on the left-hand side (number 1). In the main part of the window, a contract is shown (number 2). Contracts built using the visual editor can be transferred to the simulator with the To code button (number 3), and visual elements for all the different Marlowe types are selected below that (number 4). If Contract is selected then we see

Contracts in the Blockly tab

where we can see visual versions of the five different kinds of contract (number 1). These can be selected and moved to the main part of the window, and be snapped together to form a contract.

10.5. Performing a simulation

Moving back to the simulation tab, and selecting the Escrow contract we see

Simulation step 1

Here we focus on the input composer, which at each stage shows only those inputs that will make the contract progress. In this case we require Alice to deposit 450 Ada. We can do that with the + button next to this input. After doing that we see

Simulation step 2

with the input as part of the transaction to perform. We can then add this transaction to the blockchain by selecting Apply, but note that we can also use the other controls to Undo the last step (here to move the input out of the transaction), to Reset to the initial state, or to move to the Next block.

Assuming that we do select Apply we then see at the foot of the screen that the deposit has taken place

Simulation step 3

and this remains in view if we add Alice’s and Bob’s choices to the transaction. Note also the the current state of the contract is shown in the main part of the window, and indeed we are waiting at this stage for choices from Alice and Bob.

If Alice and Bob make different choices, and we apply the transaction we then see

Simulation step 4

and at this point in the evolution of the contract we are awaiting a choice from Carol to arbitrate the outcome.

10.6. Analysing a contract

The static analysis of a contract is performed by selecting the Static analysis tab in the pane at the foot of the page.

Static analysis

Clicking the Analyse button results in the current contract in the current state being analysed. The result is either to say that the contract passed all the tests, or to explain how it fails, and giving the sequence of transactions that lead to the error. As an exercise try this with the Escrow contract, changing the initial deposit from Alice to something smaller than 450 Ada.

Exercise

Use the Marlowe Playground to interact with the escrow contract in the various scenarios discussed earlier, in the tutorial on using Marlowe.

Explore making some changes to the contract, and interactions with those modified contracts.

Exercise

Use the Marlowe Playground to explore the other contracts presented in there: the deposit incentive contract, and the crowd-funding example.

11. Potential problems with contracts

The Marlowe language is designed to have as few as possible pitfalls and gotchas, so that contracts can be written intuitively, avoiding any surprises. Nevertheless, it is impossible by design to exclude all contracts that should not be written, without making Marlowe much harder to use. Moreover, even when a contract is well written, it is still possible for its users to interact with it in invalid ways, by issuing invalid transactions.

In all cases, when these unintended effects happen, Marlowe is designed to behave in the most intuitive and conservative way possible. However, it is worth being aware of these potential problems, and review how Marlowe behaves in these situations. That is the subject of this tutorial.

11.1. Warnings

Marlowe warnings are indications that a contract is written wrongly. A well-written contract should never issue a warning, no matter how the users interact with it. Ideally, we would like to forbid contracts that can issue warnings from being ever written, but that would require Marlowe contracts to be dependently-typed, and writing expressions that are dependently-typed is much more cumbersome.

Instead, Marlowe allows contracts that issue warning to be written, and we provide static analysis tools that let contract developers check whether a particular contract can possibly issue warnings. Additionally, we provide fall-back behaviours for when a contract produces a warning, despite our advice. We provide fall-back behaviours because we acknowledge that analysing big contracts can be very computationally expensive, and because mistakes can be made. We want badly written contracts to fail in the most harmless way possible, that is conservatively.

Non-positive payments

When a contract is supposed to pay an amount of money that is less than one unit of a currency or token, it will issue a NonPositivePay warning, and it will not transfer any money.

Negative payments should be implemented as either positive deposits (when paying a participant), or positive payments in the opposite direction (when paying between accounts).

Non-positive deposits

When a contract is supposed to expect an amount of money that is less than one unit of a currency of token, it will still wait for a IDeposit transaction, but that transaction does not need to transfer any money into the contract and no money is transferred to the participant that issues the transaction. Once this ‘fake’ deposit is successful, the contract will issue a NonPositiveDeposit warning.

Negative deposits should always be implemented as positive payments.

Partial payment

When a contract is supposed to pay an amount of money that is larger than the amount of money that there is in the source account, it will just transfer whatever is available in that account, even if there is enough money in all the accounts of the contract, and it will issue a PartialPay warning.

Partial payments should be avoided because a contract that never produces a partial payment is an explicit contract. Explicit contracts reassure their users that they will be enforceable, and that wherever in the contract it says a payment is going to happen it will indeed happen.

Let shadowing (not covered by static analysis)

When a contract reaches a Let construct that re-defines a value with an identifier that was already defined by an outer Let, the contract will issue a Shadowing warning, and it will override the previous definition.

Shadowing is a bad programming practice because it leads to confusion. Using the same identifier for more than one thing can mislead developers or users into thinking that one usage of Use is going to be evaluated to one amount while it is actually going to be evaluated to some other different amount.

11.2. Bad smells

There are some other ‘bad smells’ that indicate that a contract has probably been poorly designed.

These contracts are valid, in the sense that they will not necessarily cause any warnings, and they do what they say that they do, but they have characteristics that suggest that either the contract developer was not fully aware of the consequences of the contract, or that the developer purposefully wrote the contract in a way that was confusing for the reader.

Undefined Let usage (should be a warning)

When a Use construct uses an identifier that has not been defined yet, it will evaluate to the default value of 0. No warning will be issued but, again, this is a bad practice because it can be misleading. (Constant 0) should be used instead since it makes explicit the amount in question.

Unreachable parts of a contract

This is the main bad smell in Marlowe contracts. If part of the contract is unreachable, why would it have been included in the first place?

This bad smell takes a number of shapes.

Sub-Contract is not reachable

For example:

    If FalseObs contract1 contract2

The previous contract is equivalent to contract2. In general you should never use FalseObs, and you should only use TrueObs as the root observation of a Case construct.

Observation is always short-cut

For example:

    OrObs TrueObs observation1

The previous observation is equivalent to observation1. Again, you should only use TrueObs as the root observation of a Case construct.

When branch is unreachable

For example:

    When [ Case (Notify TrueObs) contract1
         , Case (Notify TrueObs) contract2 ]
         10
         contract3

contract2 is unreachable, the whole Case could be removed from the contract and the behaviour would be the same.

Nested non-increasing timeouts

For example:

    When []
         10
         When [ Case (Notify TrueObs)
                     contract1 ]
              10
              contract2

contract1 is unreachable: after block 10, the contract will directly evolve into contract2. The inner When does not make any difference to the contract.

11.3. Usability issues

Even if a contract avoids warnings, and has no unreachable code, it may still allow malicious users to force other users into undesirable situations that were not originally intended by developer of the contract.

Bad timing of When constructs

Consider the following contract:

    When [Case (Choice (ChoiceId "choice1" (Role "alice")) [Bound 0 10])
               (When [Case (Choice (ChoiceId "choice2" (Role "bob")) [Bound 0 10])
                           Close
                     ]
                10
                (Pay (AccountId 1 (Role "bob")) (Party (Role "alice"))
                     ada
                     (Constant 10)
                     Close
                )
            )
         ]
         10
         Close

There is nothing wrong in principle with this contract, but if (Role "alice") makes her choice on block 9, it will be virtually impossible for bob to make his choice on time and get the refund of the money in his account (AccountId 1 (Role "bob")). Unless, this is part of a game and that is an intended effect, this is likely an unfair contract for (Role "bob").

In general, it is a good practice to ensure that When constructs have increasing timeouts, and that the increase between timeouts is reasonable for the different parties to issue and get their transactions accepted by the blockchain. There are many reasons why the participation of a party may be delayed: an energy supply failure, a sudden peak in the number of pending transactions in the blockchain, network attacks, etc. So it is important to allow plenty of time, and to be generous with timeouts and with increases in timeouts.

11.4. Errors

Finally, even if a contract is perfectly written. Users may use it incorrectly, and we call those incorrect usages errors.

In all cases, whenever a transaction causes an error, the transaction will have no effect on the Contract or on its State. In fact, the wallet of a user will know in advance whether a transaction is going to produce an error, because transactions are deterministic, so users should never need to send an erroneous transaction to the blockchain.

Ambiguous interval

When a transaction reaches a timeout, its slot interval must be unambiguous about whether the timeout has passed or not. For example, if the top-most When of a contract has timeout 10 and a transaction with slot interval [6, 14] is issued, the transaction will cause an AmbiguousSlotIntervalError error, because it is impossible to know whether the timeout has passed just by looking at the transaction. To avoid this, the transaction must be split into two separate transactions:

  1. One with slot interval [6, 9].

  2. Another one with slot interval [10, 14].

Apply no-match

If a transaction does not provide the inputs that are expected by the Contract, then the contract will issue a NoMatchError error, and the whole transaction will be discarded.

Useless transaction

If a transaction does not have any effect on the Contract or State, it will result on a UselessTransaction error, and the whole transaction will be discarded. The reason why we discard useless transactions is that they open the door to Denial of Service (DoS) attacks, because a potential attacker could flood the contract with unnecessary transactions and prevent necessary transactions to make it into the blockchain.

12. Static analysis

One distinctive feature of Marlowe – probably its most distinctive feature – is that we can analyse contracts, and deduce properties of them, without running them.

We can check, in advance of running a contract, these properties:

  • Partial payments: i.e. payments when there was not enough money in account.

  • Non positive deposits: under which the contract asks for a value which is negtive or zero.

  • Non positive payments: payments of 0 or a negative amount.

  • Shadowing of Lets , where two Lets set the same identifier in the same execution path.

In the rest of this tutorial we will focus on the first of these, which is the worst kind of error. It is in this case that a payment fails, because there is not enough money in the contract (or more strictly in the account) to make a complete payment.

12.1. An example

Let us look at this example, in Blockly

An example contract in Blockly

and in pure Marlowe

An example contract in Marlowe

The contract first requires a deposit from Alice of 1 Lovelace, and then asks Bob to make a choice (called bool) of 0 or 1. The contract then pays this choice plus one to Bob from Alice’s account.

So, we can see that while the contract works OK when Bob chooses 0, there won’t be enough in the contract to pay him if he chooses 1. Our analysis, which is built into the SIMULATION tab in the Marlowe Playground, can diagnose this:

Failed analysis

This shows that the error occurs when

  • Alice has made the deposit, and

  • Bob has chosen the value 1.

and that the error generated is a TransactionPartialPay: in this case Bob only receives a payment of 1 instead of 2.

If we modify the contract so that Alice makes an initial deposit of 2, then the analysis will succeed:

Successful analysis

12.2. Under the hood

Just to re-iterate: the effect of this analysis is to check every possible execution path through the contract, using a symbolic version of the contract. This gets passed to the Z3 SMT solver, which is a state-of-the-art automated system for deciding whether logic formulas are satisfable.

If the analysis is not successful, i.e. if there is a way of making the contract fail a payment, then the system will also give an example of how it can go wrong, and present that to the user. Users can then fix the problem, and check it again.

12.3. Next steps

In the next few months we will look at how to present the results of our analysis in a more "user friendly" way, as well as broadening out the scope of our work.

Exercise

Use the analysis button in the Marlowe Playground to analyse some of the contracts that you have already written. If the analysis fails, can you see why, and correct the contracts so that they do not fail.

13. ACTUS and Marlowe

This tutorial gives an introduction to the general idea of the ACTUS standards for the algorithmic representation of financial contracts, plus examples implemented in Marlowe.

13.1. ACTUS

The ACTUS Financial Research Foundation https://www.actusfrf.org has created a standard for financial contracts, categorised by means of a taxonomy and described in a detailed technical specification.

The ACTUS standards build on the understanding that financial contracts are legal agreements between two (or more) counterparties on the exchange of future cash flows. Historically, such legal agreements are described in natural language leading to ambiguity and artificial diversity. As a response, the ACTUS standards define financial contracts by means of a set of contractual terms and deterministic functions mapping these terms onto future payment obligations. Thereby, it is possible to describe the vast majority of financial instruments through a set of little more than 30 Contract Types or modular templates, respectively.

The ACTUS specifications provide a breadth of exercises for implementation in Marlowe, and we illustrate an approach to this in the following example.

13.2. Simple Zero Coupon Bond Example

A zero-coupon bond is a debt security that does not pay interest (a coupon) but is issued at a discount, rendering profit at maturity when the bond is redeemed for its full face value.

For example, an investor can buy a bond that costs 1000 Lovelace with 15% discount. She pays 850 Lovelace to the bond issuer before start time, here 10.

Later, after maturity date, time 20 here, the investor can exchange the bond for its full notional, i.e. 1000 Lovelace.

When [
  (Case
     (Deposit
        (AccountId 0 "investor")
        "investor" ada
        (Constant 850))
     (Pay
        (AccountId 0 "investor")
        (Party "issuer") ada
        (Constant 850)
        (When [
           (Case
              (Deposit
                 (AccountId 0 "investor")
                 "issuer" ada
                 (Constant 1000))
              (Pay
                 (AccountId 0 "investor")
                 (Party "investor") ada
                 (Constant 1000)
                 Close))
            ]
            20
            Close)))
     ]
     10
     Close

This contract has a significant drawback. Once the investor has deposited the 850 Lovelace, it will be immediately paid to the issuer (if the investor does not invest in time, the contract ends). After that, two outcomes are possible

  • the issuer deposits 1000 Lovelace in the investor's account, and that is then immediately paid to the investor in full;

  • if the investor doesn’t make the deposit, then the contract is closed and all the money in the contract is refunded, but there is no money in the contract at this point, so the investor loses her money.

How can we avoid this problem of the issuer defaulting?

There are at least two ways to solve this: we could ask the issuer to deposit the full amount before the contract begins, but that would defeat the object of issuing the bond in the first place. More realistically, we could ask a third party to be a guarantor of the deal.

Exercise

Give a variant of the zeroCouponBond contract in which it is necessary for the issuer to put the full value of the up before the bond is issued.

Exercise

Give a variant of the zeroCouponBond contract which also includes a guarantor who puts up the full payment up before the bond is issued, and who will pay that counterparty if the issuer defaults; if the issuer does make the payment in time, then the guarantor should recover their money.

13.3. Guaranteed Coupon Bond Example

This more complex bond involves an investor who deposits 1000 Lovelace, which is immediately paid to the issuer. The issuer then has to pay as interest 10 Lovelace every 10 slots. On maturity the investor should receive back the interest plus the full value of the bond.

couponBondFor3Month12Percent =
    -- investor deposits 1000 Lovelace
    When [ Case (Deposit "investor" "investor" ada (Constant 1000))
        -- and pays it to the issuer
        (Pay "investor" (Party "issuer") ada (Constant 1000)
            -- after 10 slots expect to receive 10 Lovelace interest
            (When [ Case (Deposit "investor" "issuer" ada (Constant 10))
                -- and pay it to the investor
                (Pay "investor" (Party "investor" ) ada (Constant 10)
                    -- same for 2nd 10 slots
                    (When [ Case (Deposit "investor" "issuer" ada (Constant 10))
                        (Pay "investor" (Party "investor" ) ada (Constant 10)
                            -- after maturity date investor
                            -- expects to receive notional + interest payment
                            (When [ Case (Deposit "investor" "issuer" ada (Constant 1010))
                                (Pay "investor" (Party "investor" ) ada (Constant 1010) Close)]
                            (Slot 40)
                            Close))]
                    (Slot 30)
                    Close))]
            (Slot 20)
            Close))]
    (Slot 10)
    Close

Exercise

Give a variant of the zcouponBondFor3Month12Percent contract which also includes a guarantor who puts up the full payment up before the bond is issued, and who will pay that counterparty if the issuer defaults; if the issuer does make the payment in time, then the guarantor should recover their money.

IOHK plans to implement the full ACTUS standard using Marlowe and Plutus over the coming year.

14. Migrating to Marlowe 3.0

This tutorial explains how Marlowe 3.0 differs from earlier versions of the language, versions 1.3 and 2.0.

14.1. Remove Both

We do not include a Both construct in Marlowe 3.0, which makes all contracts sequential.

Since in none of the versions of Marlowe was there communication among the branches of Both, the only extra functionality provided by Both in practice was the ability to wait for several money deposits at the same time.

We take care of this functionality by updating the When construct. Instead of having different branches wait for different inputs, we move to a completely sequential and synchronous model, where we can wait for one of several possible inputs at the same time (as in select).

The reason we removed this construct is that sequential programs are easier to analyse and easier to reason about, since there is no need for synchronisation and no opportunity for race conditions.

14.2. Include accounts

In earlier versions of Marlowe each commitment has its own timeout. This means that money deposited in a contract is not fungible, because it can be distinguished by its timeout. To achieve fungibility we have removed timeouts from individual constructs, and have a single timeout for all commitments. This contract lifetime is straightforward to infer from the timeouts in the contract.

We do, however, include accounts to organise the money deposited into the contract. This makes it more transparent how money flows within the contract, and in particular identifies to whom money is refunded when the contract terminates.

Each account is identifier by a pair of a number (account number) and a participant; the participant indicates who will get the money in the account by default when Close is reached.

The reason we chose to include accounts is that without them we found that we were essentially keeping track of the accounts manually. Additionally, in every leaf of the AST, we found ourselves calculating how much we must return to every participant, cluttering the tree with repetitious “boilerplate”. Thus, having money organised in accounts can make contracts easier to reason about and less prone to error.

Note that we can provide full fungibility by using a single account. We only need to write the appropriate Pay commands in the leaves of the contract. If all the money is paid to participants, then Close has no effect.[9]

Discussion: Implicit vs Explicit Accounts

Many of the use cases for accounts – and all those that we can identify for ACTUS contracts – have one account per participant, and one participant per account (the “1-1 model”). This raises the question of whether we should give an implicit treatment of accounts, with each participant owning one account.

On the other hand, there are a variety of plausible scenarios for accounts which do not conform to the 1-1 model.

Examples where multiple participants use an account.

  • Alice owns an account to which she commits money for Bob to spend (think of Alice as Bob’s employer). Bob is able to spend up to the limit in the account, but after the commitment times out, Alice recovers anything remaining.

  • Alice owns an account to which she commits money for Bob and Carol to spend (think of Alice as Bob’s and Carol’s employer). They are able to spend (jointly) up to the limit in the account, but after the commitment times out, Alice recovers anything remaining.

  • On the other hand, they could each be given a separate account from which to spend: that would enforce individual limits as well as an aggregate limit.

  • If Bob [and Carol] want to spend money they can also add money to the account, but they should realise that anything unused will be refunded to Alice.

Examples of multiple accounts for one person:

  • Examples of underwriting would fit here. A person underwrites first-level risk, and second-level risk using different accounts. Only when the first level underwriting of all participants is spent will second level spending occur.

14.3. Close replaces Null / Pay

Since all contracts are sequential now, we can easily tell when a contract terminates, i.e: when only Null is left. We use this opportunity to close the contract and to refund any money remaining in the accounts; for this reason we have renamed Null to Close (aiding comprehensibility).

As noted earlier, there is no longer any explicit timeout in the accounts, since all contracts will eventually reduce to Close. In fact, we can statically and efficiently calculate an upper bound for when this will happen, making this aspect of Marlowe analysable.

14.4. Pay

Pay is now immediate, and it has a single continuation, and fewer parameters.[10] It allows payments from an account to a participant or to another account. We discarded PayAll, since it can be emulated as a finite series of Pay. In fact, we can define payAll as a Haskell function (see zeroCouponBond example).

It is a consequence of removing the Both construct, that it is now unequivocal which Pay goes first: they are all sequential, thus aiding analysis. With the Both construct we could potentially have Pays happen in any order (since both sides of Both are supposed to run concurrently).

14.5. Multi-clause When

We have modified When to include a set of possible actions that can be input while When waits. We call this approach “One of Many”, because it accepts one action out of potentially many allowed actions. When remains as follows:

When [Case] Timeout Contract

where When will either wait for Timeout and continue as Contract, or continue as specified in one of the Cases, whichever happens first. Case is defined as:

data Case = Case Action Contract

and Action as:

data Action = Deposit AccountId Party Token Value
            | Choice ChoiceId [Bound]
            | Notify Observation

A Case clause will be activated only if the corresponding Action is produced, and it will continue as Contract. In case of two Actions matching, the first one in the list will be executed.

Three kinds of actions are supported:

  • Deposit represents a deposit of money into an account; this was originally called Commit.

  • Choice represents a choice made by a participant from within a set of Integer values (specified by the list of Bounds).

  • Notify will wait for a Notify action issued when the Observation is true. We call it Notify in order to make it clear that we cannot just wait for Observations, but that someone must trigger the contract in a moment when an Observation is true.

We have discarded adding observations to Deposit and Choice since it would not be obvious whether the Observation would be evaluated before or after applying the action.

In addition to explicit cases in When, we must remember that the timeout branch is also a case, and it also needs to be triggered (similarly to Notify).[11] [12]

14.6. Observations and Values

We have discarded Observations and Values that can be expressed by combining others: like the general AvailableMoney (for the whole contract), or like DepositedMoneyBy, that remembers the amount of money deposited by a participant, since the contract can be restructured to observe that, and supporting would require additional information in the state (simplicity).

We have retained the ChoseSomething observation, even though, in the proposed semantics, every occurrence of ChoseSomething can be evaluated statically and efficiently by examining its context.

For example, in the following contract we can see that the first occurrence of ChoseSomething will evaluate to True, and the second one to False:

When [ Case (Choice (ChoiceId 1 Alice) [(1,1)])
            (If (ChoseSomething (ChoiceId 1 Alice))
                Close
                Close)
     , Case (Choice (ChoiceId 2 Bob) [(2,2)])
            (If (ChoseSomething (ChoiceId 1 Alice))
                Close
                Close)]
     0
     Close

Nevertheless, we have chosen to keep the construct for two reasons:

  • It allows for code reusability (convenience). For example, in the previous contract, we could define chosen1:

  let chosen1 = If (ChoseSomething (ChoiceId 1 1))
                   Close
                   Close
  in
  When [ Case (Choice (ChoiceId 1 1) [(1,1)])
              chosen1
       , Case (Choice (ChoiceId 2 2) [(2,2)])
              chosen1]
       0
       Close

But this would not be possible if we did not have the construct ChoseSomething, since the value to which it reduces depends on the context.

  • It may no longer be the case that occurrences of the construct can be evaluated statically if we extend the When construct to support “many of many” inputs.

14.7. Inclusion of SlotIntervals

The EUTxO specification provides validation scripts with slot-intervals instead of with slot numbers. This is to promote determinism in validation scripts. Nevertheless, we have kept the timeout of When (the only timeout) as a slot number. The way we deal with slot-intervals is by requiring that the interval of a transaction does not include any timeout over which the semantics has to make a choice. For example: if a timeout is 10, a transaction with interval 5-15 will fail with AmbiguousSlotInterval. Participants would have to issue a transaction with interval 5-9 or 10-15 (or both).

Nevertheless, for Values, we provide the two constructs SlotIntervalStart and SlotIntervalEnd. An alternative to consider would be to modify the semantics so that Values are non-deterministic, that way we could include a CurrentSlot construct and just invalidate transactions that are ambiguous, but this would complicate the semantics and make them less predictable.


1. Lists in Marlowe are included in square brackets, as in [2,3,4].
2. Again, we will describe how arbitrate and agreement work in a later tutorial.
3. We can think of oracles as another kind of party to the contract; under this view notifications become the choices made by that party.
4. A fully “fungible” model is supported by a contract with a single account, and with explicit allocation of any remaining funds on contract termination.
5. Indeed, Marlowe could be modified to run off blockchain, or to work on a permissioned blockchain, too.
6. The presentation here is a simplification of the concrete implementation, in which transactions are associated with a slot interval during which it is valid to add them to the blockchain.The reason for this is that in general it is difficult to predict the precise slot in which a transaction will be accepted for inclusion on the blockchain; it is therefore more robust to specify an interval in which the transaction should be accepted. The view presented here is a simplification in that effectively we consider only intervals of length one. So, a Marlowe contract is able to access the upper and lower bounds on the current slot interval, rather than the specific current slot value. Executing a contract can, in some circumstances, lead to an “ambiguous slot interval error”, but we do not cover that any further here.
7. In fact we used newtype declarations rather than data types because they are more efficiently implemented.
8. This may be modified in the future to allow values to be named by strings.
9. We can potentially provide a way of statically analysing the contract to check whether there can possibly be any money left in any account when Close is reached.
10. This means that payments now obey a “push” model rather than a “pull” model.
11. Nevertheless, triggering the contract for processing timeouts is not urgent as it is with Notify, because while Observations can alternate between True and False, timeouts can only happen once and, independently of whether they have been observed by the contract or not, they cannot be reversed.
12. Indeed, an explicit Case can no longer be issued after the timeout, even if the timeout has not been observed by the contract, since the timeout is checked before the Inputs. However, a participant may want to trigger a timeout in cases where no other Inputs are needed, in order to trigger one or more payments, for example. In the current implementation of the semantics that would be done by issuing a transaction with an empty list of Inputs.