Verified Extraction from Rocq to PIR

Abstract

Plutus Core is a λ-calculus-based target language for the validator logic of smart contracts on the Cardano blockchain. In this thesis, we cover the development of a verified extraction pipeline from Rocq to Plutus Core, by defining and verifying part of the missing translation from MetaRocq’s verified extraction to λT□ , MetaRocq’s language of typed erased terms, to Plutus’ Intermediate Language, PIR, which can then be certified by the PlutusCert project. Our pipeline allows users to write verified methods as Gallina programs in the Rocq prover and then safely extract them to PIR programs. We currently support translation for a subset of Gallina consisting of the simply typed λ-calculus with global definitions.