Skip to content

The CertiCoq pipeline

Matthieu Sozeau edited this page Oct 11, 2022 · 11 revisions

This page explains briefly the CertiCoq pipeline and its verification status.

  1. Reification (Gallina -> PCUIC)
    We reify a Gallina program to its Gallina AST using MetaCoq's reification facility.

  2. Erasure (PCUIC -> λbox)
    We erase types and proofs using MetaCoq's verified erasure.

  3. λbox -> λboxMut
    λboxMut is a slight variation of λbox using mutual inductive types instead of nested inductive types.
    Status: Verified

  4. Let-bind environment (λboxMut -> λboxLocal)
    Let-binds the environment at the beginning of the program.
    Status: Verified

  5. ANF translation (λboxLocal -> λΑΝF)
    Converts λboxLocal to λANF, the core intermediate representation of CertiCoq. By default we use direct-style translation, but
    Status of CPS translation: Verified
    Status of direct translation: Proof underway

  6. ANF pipeline (λΑΝF -> λΑΝF^C)
    The λΑΝF pipeline consists on 13 passes built from of 7 distinct transformations:
    Inlining, Shrinking, Uncurrying, Lambda lifting, Closure conversion, Hoisting, Dead parameter elimination
    The code is compiled to λΑΝF^C, a subset of the ANF language that has no nested functions and as such it has flat-scoping and no closures (closures are explicitly introduced by means of closure conversion).
    Status: Verified
    Each of the phases are verified. The λΑΝF comes with an end-to-end compositional compiler correctness theorem. (Top-level theorems).
    The implementation and proof is documented in Zoe Paraskevopoulou's thesis.

  7. C-code generation (λΑΝF^C -> Clight)
    Compiles λΑΝF^C to C-code. Currently there are two code-generation procedures:

  • The old code generator, that can only handle CPS code. This phase is documented in Olivier Savary Bélanger's thesis
    Status: Proof underway
  • The new code generator, that handles the full fragment of λΑΝF^C.
    Status: Proof underway