Plutus and IOHK

Philip Wadler

We apply the zipper construct of Huet to prove correct an optimiser for a simply-typed lambda calculus with force and delay. The work here is used as the basis for a certifying optimising compiler for the Plutus smart contract language on the Cardano blockchain.

The paper is an executable literate Agda script, and its source may be found in the file

Dedicated to Olivier Danvy on the occasion of his 64th birthday.

The Cardano blockchain is the first to use proof of stake, offers native support for multiple currencies and is evolving toward a distributed governance model. It supports smart contracts through Plutus, a language based on System F𝜔 with recursion. About half a dozen languages compile into Plutus, the first of which is Plinth (formerly Plutus Tx)— a language that reuses a subset of the Haskell syntax, and has been in commercial use since 2021.

Our journey building Plinth has been unconventional in a number of ways. First, Plinth programs are written in a subset of Haskell, using standard Haskell syntax and types, which brings a number of advantages. Second, compilation is primarily handled by a GHC plugin, one of the most intricate we are aware of. Third, while some compiler optimizations mirror those in Haskell, others diverge significantly to meet on-chain execution constraints. Fourth, Plutus programs run on an instrumented CEK machine with a formal specification in Agda. This report reflects on our design choices, outlining effective practices, challenges, and key takeaways, with an emphasis on recent advances in the language, compiler, and runtime.

Good news for researchers in formal verification: smart contracts regularly suffer exploits such as the DAO bug, which lost the equivalent of 60 million USD on Ethereum. This makes a strong case for applying formal methods to guarantee essential properties.

Which properties would we like to prove? Most previous studies focus on contract-specific properties that do not generalize to a wide class of smart contracts. There is currently no commonly agreed upon list of properties to use as a starting point in writing a formal specification.

We propose three properties that we believe are relevant to all smart contracts: Validity, Liquidity, and Fidelity. Focusing on the concrete case of the Cardano platform, we show how these properties stop exploits similar to the DAO bug, as well as preventing other common issues such as the locking of funds and double satisfaction.

We model an account simulation, a multi-signature wallet, and an order book decentralized exchange, as example smart contract specifications using state transition systems in the Agda proof assistant. We formalize the above properties and prove they hold for the models. The models are then separately proven to be functionally equivalent to a validator implementation in Agda, which is translated to Haskell using agda2hs. The Haskell code can then be compiled and put on the Cardano blockchain directly. We use the Cardano Node Emulator to run property-based tests and confirm that our validator works correctly.

Lambda calculi are often used as intermediate representations for compilers. However, they require extensions to handle higherlevel features of programming languages. In this paper we show how to construct an IR based on System Fμω which supports recursive functions and datatypes, and describe how to compile it to System Fμω. Our IR was developed for commercial use at the IOHK company, where it is used as part of a compilation pipeline for smart contracts running on a blockchain.

System F, also known as the polymorphic λ-calculus, is a typed λ-calculus independently discovered by the logician Jean-Yves Girard and the computer scientist John Reynolds. We consider Fωμ, which adds higher-order kinds and iso-recursive types. We present the first complete, intrinsically typed, executable, formalisation of System Fωμ that we are aware of. The work is motivated by verifying the core language of a smart contract system based on System Fωμ. The paper is a literate Agda script.

Philip Wadler,