Skip to content

The CertiRocq pipeline

Jump to bottom Edit New page
Wolfgang Meier edited this page Mar 19, 2026 · 6 revisions

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

  1. Reification (Gallina -> PCUIC)
    We reify a Gallina program to its Gallina PCUIC AST using MetaRocq's reification facility.
    Status: ✅ The (quite simple) quoting function is in the TCB. The translation to PCUIC is verified.
    This is documented in the MetaRocq papers.

  2. Erasure (PCUIC -> λbox)
    We erase types and proofs using MetaRocq's verified erasure. Status: ✅ Verified
    This is documented in Matthieu Sozeau's habilitation thesis.

  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 CertiRocq. 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
  1. WebAssembly code generation (λΑΝF^C -> Wasm)
    Compiles λΑΝF^C to Wasm. Implementation and proof are inspired by the C-backend and described in [CPP'25].(https://dl.acm.org/doi/10.1145/3703595.3705879)
    Status: ✅ Verified
Add a custom footer

Clone this wiki locally