The CertiCoq pipeline

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

1. Reification ( -> 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 -> L2
   L2 is a slight variation of λbox.
   Status: Proof pending

4. Fully-applied constructors (L3 -> L3) Eta expands constructor applications so that constructors are fully applied and removes type parameters.
   Status: Proof pending

5. Eta-expand branches (L3 -> L3)
   Ensures that expressions in the arms of pattern-matching construct are lambdas.
   Status: Verified

6. Let-bind environment (L3 -> L4)
   Let-binds the environment of at the beginning of the program.
   Status: Verified

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

8. 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
   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.

9. 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. (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 pending