Compiler certification

[ana-pantilie]

Introduction

We want to certify the PIR to UPLC compiler. Part of the motivation behind this feature is:

• a better guarantee that the end user's high level code behaves the same as the low level code they upload and is run on the chain
• we want to ensure that proofs of properties of the high level code also translate to the low level code

Jacco has worked on a couple of papers presenting his incremental approach to verification. See https://github.com/jaccokrijnen/plutus-cert/tree/master, https://iohk.io/en/research/library/papers/translation-certification-for-smart-contracts-scp/. His implementation is done in Coq.

Our approach

The idea is to certify that the optimisations done by the compiler on the input code produces code which is equivalent in some way. A part of the work is defining this equivalence.

Based on Jacco's ideas, we will first formalise the optimisations as translation relations between two ASTs. This provides a syntactic specification which will be proven in some language which we need to agree on. The next step is to define the equivalence relation and prove that holds for the two ASTs as well.

The implementation therefore, for each compiler optimisation, expects a before-AST and an after-AST and finds and checks a proof that the two ASTs are equivalent in both the syntatic sense and the semantic sense.

Preliminary phase

Our goal during the preliminary phase is to gather the requirements for a POC.

Action items:

• Understand how the Coq decision procedure approach works #5894
• Investigate implementing the proof generation in Isabelle #5895
• Discuss with Agda experts and with Jacco: https://docs.google.com/document/d/1Go-TMLgFS7Qq5yTCMTx47YrzDmfGanlokAq2iLnSDgo/edit?usp=sharing https://docs.google.com/document/d/1QouC1mZSfkt6hUcYtsTFbjY4qxCPRhAFJm0uZgw3Inc/edit?usp=sharing

Proof of concept

We have decided on the following:

• the language to implement the certification component is Agda
• we will focus on UPLC
• we will select a simple UPLC optimisation from https://github.com/IntersectMBO/plutus/tree/master/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform, probably CaseOfCase

Action items:

• Agda translation relation for CaseOfCase UPLC phase #5916
• Build certifier infrastructure and integrate with compiler #5941
• Agda decision procedure for CaseOfCase translations #5944
• Add simplifier tags in UPLC simplifier #6540
• Find a way to serialise Agda proof terms #6424
• https://github.com/IntersectMBO/plutus-private/issues/74
• Explore possibilities for Semantic Equivalence proof

Making the certifier production-ready

• https://github.com/IntersectMBO/plutus-private/issues/1200
• https://github.com/IntersectMBO/plutus-private/issues/1210
• https://github.com/IntersectMBO/plutus-private/issues/1212
• https://github.com/IntersectMBO/plutus-private/issues/1221
• https://github.com/IntersectMBO/plutus-private/issues/1223
• https://github.com/IntersectMBO/plutus-private/issues/1222
• https://github.com/IntersectMBO/plutus-private/issues/1224