Peregrine: a middle-end for code generation from proof assistants

The code generation capabilities of proof assistants like Rocq [22], Agda [1], and Lean [6] allow programs whose properties have been verified in the proof assistant to be extracted to industrial programming languages. This process must be trusted to produce extracted programs with the specified behaviour, unless it is entirely formally verified, such as in HOL4, which uses proof generation for generated code and the verified CakeML compiler [17, 21]. However, implementing and verifying an extraction pipeline remains an arduous task which is not feasible to repeat for every choice of proof assistant and target language one may desire to use.

The Peregrine Project aims to simplify this process by providing a unified middle-end for code generation, suitable for use with multiple proof assistants and target languages. Our approach is built around λ□, an intermediate stage in Rocq’s extraction to OCaml [15], and its existing formalization as part of the MetaRocq project [19]. As novel contributions, we add Agda and Lean frontends, which produce λ□ code from their respective source language, and a backend translating λ□ into CakeML. Furthermore, we use MetaRocq’s verified erasure [20] as a Rocq frontend and integrate several existing Rocq extraction pipelines as Peregrine backends for OCaml, C, WebAssembly, Rust and Elm.

We have successfully used Peregrine to extract useful computational artifacts from an Agda specification of a blockchain consensus protocol. We believe that comparing the performance of programs extracted via Peregrine with various proof assistants and target languages can yield useful insights in the near term. In the long run, we hope to verify all Peregrine frontends and backends and obtain end-to-end correctness theorems for extracted code.