Mechanised meta theory for Plutus Core

Plutus Core is the language Plutus programs are compiled into. It is based on System F omega with iso-recursive types.

Meta theory is theory about the theory. It seeks to answer the questions of whether the language and its semantics are correct rather than whether a particular program is correct. To mechanize it is to get a proof assistant tool to check your proofs for you. This gives a much higher degree of assurance.

This repository contains a formalisation of Plutus Core in Agda. Agda is both a dependently typed functional programming language and a proof assistant. It is particularly suited to formalising programming languages. Agda programs can be compiled to Haskell and can make use of Haskell libraries.

• Intrinsically typed representation of the syntax (of Plutus Core);
• Intrinsically typed representation of the reduction semantics;
• Formal Proofs of progress and (type) preservation;
• Evaluator that can be run inside Agda;
• Correspondence to untyped syntax;
• Correspondence to untyped (reduction) semantics;
• Published paper.

• An extrinsically typed evaluator that can be compiled to Haskell;
• Typechecker + compilation to Haskell;
• Automated building under CI;
• Automated testing of evaluation under CI;
• Automated testing of typechecking under CI.
• Automatic geneneration of programs to test using NEAT
• Published paper.

• Intrinsically typed EC reduction;
• Intrinsically typed CK machine;
• Intrinsically typed CEK machine;
• Correspondence between structural reduction and EC reduction;
• Correspondence between CK executation and reduction (in EC style);
• Correspondence between CK executation and CEK execution;
• Soundness of typechecking;
• Completeness of typechecking;
• Intrinsic evaluation, compiled to Haskell.
• Published paper.

• Untyped CEK machine;
• Testing typed CEK against untyped CEK;
• Correspondence between typed and untyped CEK;
• Untyped CEK compiled to production quality Haskell;
• Published paper.

plutus-metatheory is a module inside plutus, so the instructions are the same as for other plutus components, see the top-level README.

You can execute the plc-agda command like this:

$ cabal run plc-agda

To run the tests you can execute:

$ cabal test plutus-metatheory

To build the documentation as a static site:

$ agda --html --html-highlight=auto --html-dir=html src/index.lagda.md
$ jekyll build -s html -d html/_site

• The formalisation currently covers the full language of Plutus Core: System F omega with (deep) iso-recursive types, and builtin-types for integers and bytestrings, reduction, CK and CEK semantics and type checking. Progress and preservation have been shown to hold for the small-step operational semantics.

• The Agda formalisation contains an executable plc-agda which makes use of the parser and pretty printer from plutus-core in conjunction with an interpreter written in Agda. It has the same interface as plc. It supports evaluation using various reduction strategies and type checking.

See the site generated from the Literate Agda for an explanation of the structure of the formalisation and links to the code.