Home

Welcome to the CertiRocq wiki. The Wiki provides documentation for the CertiRocq compiler.

Contents

1. The CertiRocq Plugin
   Useful information about the usage of the CertiRocq plugin.
2. The bootstrapped CertiRocqC and CertiRocqChk Plugins
   Useful information about the bootstrapped plugins.
3. The CertiRocq Pipeline
   Information about the CertiRocq pipeline and its current verification status.
4. Glue Code and FFI
   Information about interfacing with the generated C code.
5. Memory Model and Garbage Collection
   Lightweight description of CertiRocq's memory representation and runtime.
6. When C code allocates on the Rocq heap
   How to write C functions that interface with Rocq functions
7. The WebAssembly backend