plutus-cert

Translation certification of Plutus compiler passes in Coq.

Status

Work in progress

Reading

• Translation Certification for Smart Contracts (Krijnen, J.O.G, Chakravarty, M.M., Keller, G. and Swierstra, W., FLOPS 2022): Translation relations for certifying Plutus compilations
• Verified Compiler Optimisations (Joris Dral, 2022 MSc thesis): Using step-indexed logical relations for verifying translation relations
• Automatically Deriving Checkers for Compilation Verification (Bart Remmers, 2023 MSc thesis): Generating decision procedures for translation relations

Setup (Nix)

Run nix develop.

Setup (Nix + coq-lsp + vs-code)

1. Run nix develop in a shell.
2. Run code in that same shell
3. Run which coq-lsp
4. Enter this path in vscode coq-lsp plugin settings.