Lars Brünjes Polina Vinogradova - Plutus: Writing Reliable Smart Contracts

Dr. Lars Brnjesholds a Ph. D. in Pure Mathematics from the University of Regensburg(Germany) and has been a postdoc at the universities of Cambridge (UK) and Regensburg.After working as a Software Architect for ten years, he joined IOHK in 2016. As Director ofEducation for IOHK he gives talks and delivers trainings and Haskell courses all over the world,but is also involved in IOHK research projects.

Dr. Polina Vinogradovaholds a Ph. D. in Computer Science from the University of Ottawa.Her Ph. D. research consisted of the formalization of category-theoretic proofs,definitions and examples related to the study of abstract computation.She obtained her Masters degree in Mathematics, also from the University of Ottawa,with the focus of her thesis being the study of abstract computation usingCategory theory, in particular, Turing categories.

The authors thank Niamh Ahern, Michael Peyton Jones, Alejandro Garcia and the IOHK Plutus Team,without whose hard work and dedication this book would not have been possible.

2019 Input Output HK Limited.

The 'Plutus: Writing Reliable Smart Contracts' eBook is the property of Input Output HK Limited. All content and materials havebeen produced by Input Output HK Limited and can be reused in accordance with the Apache 2.0 license.The exercises and code samples included in this book are examples and are usedas learning aids. The source files for this eBook are stored in thePlutus GitHub repository and are covered by our open source license agreement.

This book teaches you how to write reliable smart contracts with Plutus, thenew general purpose language developed by IOHK for smart contracts on the blockchain.

This book aims to educate beginner Haskell developers in the fundamentals ofPlutus. It is the first book written about Plutus and uses real life samples tohelp anchor the application of this new and exciting smart contract language totangible use cases. This book will be continuously updated with the latest codeto ensure that the content is current and up to speed with the latest version ofPlutus.A general understanding of smart contracts would be useful to learn about andwork with Plutus, but is not essential for starting out. For general functionalprogrammers with blockchain domain knowledge, we recommend that you read aboutand understand the basics of Haskell programming prior to reading this book.

Come and explore the world of Plutus and learn our new language throughreal life scenarios and sample code snippets!

In order to become proficient with all things Plutus, it isinevitable that you must first acquire a solid understanding of howaccounting is done on the Cardano platform.

We traditionally think of money transfers as being between two bank accounts,or perhaps internet addresses in the case of digital currency. The Cardano platform,like a number of other cryptocurrency platforms such as Bitcoin, uses insteadan accounting approach known as UTXO-style. A full formal description ofthis type of accounting can be found as part of the Cardano ledgerformal specification, see .

UTXO-style accounting documents the flow of money not from account to account,but rather from transaction to transaction. Each transaction has inputs(where the money being spent is coming from), and outputs(where this money is going). Note that the body of a transaction may alsocontain other data, as we will see later when we examine the extendedUTXO model in the chapter.

Consider the data flow graph below, . The black lines represent unspent outputsof transactions, and the red lines represent these outputs being used as inputsto subsequent transactions. The vertical unlabelled box represents a singletransaction having several inputs and several outputs. The blue certificatesdenote remaining unspent outputs in our illustration.Note that here, at the start of the data flow graph, Alice has 100 Ada inunspent outputs from before the start time of this graph -this money comes from one or more transactions outside the scope of this picture.We abstract this with a single box (labelled with her name and the 100 Ada).This box has two black (output) lines coming out of it, with the total valueof these outputs adding up to 100 Ada):

Now, Bob has 10 Ada from previous unspent outputs. He spends them as follows:

This new transaction we illustrate here has two inputs, 42 from Alice, and 10from Bob. This transaction has two outputs, 2 Ada to Bob, and 50 to Charlie.We also see that Charlie has 52 Ada from a previously unspent output, fora total of 102 Ada he can spend in future transactions. Bob is left withonly one output of 2 Ada, and Alice, a total of 58 Ada in unspent outputsfrom other transactions.

The above model is strictly showing the flow of currency between severalparticipants. In this simplified version, the transactions illustrated are notpaying fees, etc.Even in this somewhat simplified model, we see that an output must always be spentin full. That is, a record of an unspent output cannot be modified (this wouldbe account-based bookkeeping), only used entirely. In order to maintainthe ledger bookkeeping integrity, the new transaction must have all the unspent outputs (totalingthe correct amount of all the unspent outputs) that are being used up by it. In theexample above, our new transaction removes (i.e. uses as inputs) unspent outputs of value42 from Alice and 10 from Bob, for a total of 52 Ada. We must then have52 Ada of outputs from this transaction (2 to Bob and 50 to Charlie).Note here that Bob had both an unspent output used by this transaction andan unspent output produced by this transaction. That is, he got, so to say,change (of 2 Ada) from this transaction. Since there is no true way to spendpart of an output, this is how UTXO accounting deals with partial spending -by adding a "change" output.

Notice here that this style of accounting makes it convenient, if not intuitive,to distribute the flow of cash from several contributors to several recipients byhaving it flow into a common pot, i.e. the transaction, before being sent tothe intended payees.This is, in a very general sense, the goal of smart contracts.Let us explore what is going on during the processing of a UTXO transaction event more formally.For the basic transactionmodel we discuss here, refer to .

Before we examine the structure of transactions, let us look at how book keepingis done on the ledger. The record on the ledger thatcontains this information is called a UTXO, short of Unspent Transaction Outputsand denoted UTXO in the figure.This record is a finite map, where the key is a pair of transaction ID andan index,