Skip to content

The CertiRocq plugin

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

The CertiRocq plugin provides commands to compile Gallina programs to Clight, to register external functions realized in C, and to compile and run the generated C code. It uses the extracted sources of CertiRocq to OCaml.

The CertiRocq plugin can be loaded with:

From CertiRocq.Plugin Require Import CertiRocq.

For usage information type:

CertiRocq -help.

Compiling Gallina to C

CertiRocq Compile <options> <definition>.

This command (recursively) compiles a Gallina definition to a C program. The relevant environment dependencies are compiled as well. The command will generate two files: filename.c and filename.h: The generated C code and the corresponding header file.

By default, the filename will be the fully qualified name of the definition to be compiled.

The command options are:

  • -file "filename": Specifies the filename of the generated C files.

  • -ext "suff": Specifies a suffix to be appended to the filename.

  • -cps: Compiles the program to continuation-passing style. The default is direct-style compilation. Note that CPS is generally less efficient and it will result in around 2x overhead.

  • -time: Prints timing info for each compilation phase.

  • -O N, where N=0 or N=1: N=1 (default) will enable the λΑΝF transformation lambda-lifting that will try to allocate closure environments is registers. N=0 disables lambda lifting.

  • -time_anf: print timing info for each phase of the λANF pipeline.

  • -args N : Maximum number of (user) arguments in the generated C code. The default is N=5. The rest of the arguments are passed using a global array.

Note that compiling code that contains computationally relevant axioms will fail, unless user specifies C functions that realize the axiom. (next section).

Extracting constants to C functions

CertiRocq supports mapping Gallina constants (including axioms) to specific C functions.

CertiRocq Compile <options> <definitions>
  Extract Constants [ constant1 => "c_function1" (with tinfo)?,
                      ... , 
                      constantN => "c_functionN" ]
  Include [ "file1.h", "/foo/bar.h" as absolute, ..., "fileM.h" as library, "file_C.h" "file_rocq.h" as library ].

The above command will map and specify which Gallina constants are compiled to which functions and the files that contain the function declarations (that will be included in the generated C code). The optional with tinfo annotation is necessary when the C code needs to use the garbage collector's interface, e.g. when it allocates. By default the includes are used as is when compiling the C code, so they are #included in quotes and should be in the same directory as the generated code. The as absolute qualifier passes the absolute path while the as library qualifier expects the file to be in CertiRocq's runtime directory (usually `rocq c -where`/user-contrib/CertiRocq/Plugin/runtime). When both "file_C.h" and "file_rocq.h" are given with the as library qualifier, the first is used for all the commands below except for CertiRocq Eval which allows to dynamically link the code to Rocq, in which case file_rocq.h and file_rocq.c can use OCaml's FFI to call back Rocq APIs.

An N-ary Gallina function should be implemented with an N-ary C function unless it allocates, in case it gets an additional first argument of type thread_info* (defined in gc_stack.h or gc.h). Note that in Gallina the constant is still a first-class function that can be handled as an ordinary function (e.g., partial application).

A 0-ary Gallina definition should be implemented with a 0-ary C function.

The arguments and the results of the C functions must fit into machine integers (default 64 bits). Opaque datatypes realized in C must be either pointers outside the CertiRocq heap or have a 64-bit unboxed representation with the least significant bit set to 1 (for compatibility with CertiRocq's garbage collector).

For modular registration of extracted constants, use the CertiRocq Register command:

CertiRocq Register 
  [ constant1 => "c_function1", 
    ... , 
    constantN => "c_functionN" ]
  Include [ "file1.h", ... , "fileM.h" ].

The effects of CertiRocq Register commands can be accumulated to register FFI functions, and are taken into account in subsequent calls to the CertiRocq Compile commands.

If you are writing foreign functions in C, you will want to generate glue code. The command that generates glue code is CertiRocq Generate Glue:

CertiRocq Generate Glue -file "glue" [ bool, nat, option ].

The code generated through this command is described in more detail in a separate page.

Default FFI implementations

When loading CertiRocq.CertiRocq, one gets FFI implementations for primitive integer (CertiRocq.PrimInt63) and floating point (CertiRocq.PrimFloats) operations along with an interface for calling Rocq back CertiRocq.RocqMsgFFI. This module provides the following functions that are realized by calling back Rocq:

Axiom (msg_info : string -> unit).
Axiom (msg_notice : string -> unit).
Axiom (msg_debug : string -> unit).
Axiom (user_error : string -> unit).

These send message to the various channels available in Rocq's IDEs (info, notices, debug) or raise an error.

Compiling the generated C code

Once the C files are generated they can be compiled with an ordinary C compiler (like GCC or Clang) or the CompCert verified compiler. The generated C files must be linked with the garbage collector.

This is currently done manually:

  • The files gc_stack.c (or gc.c if -cps is used), gc.h, values.h must be included (and .o files linked) from the RUNTIME_PATH directory which one can define as:
RUNTIME_PATH=`rocq c -where`/user-contrib/CertiRocq/Plugin/runtime/

The recommended compilation command is then:

gcc -o <file> -Wno-everything -O2 -fomit-frame-pointer -I ${RUNTIME_PATH} -L ${RUNTIME_PATH} ${RUNTIME_LIBS} filename.c glue.c <other_files>

where filename.c is the generated C code, glue.c is the generated glue code, and ${RUNTIME_LIBS} is the CertiRocq runtime including the garbage collector implementation and FFI bindings.

There are a few options for ${RUNTIME_LIBS}:

  • It must include gc_stack.o when using the ANF pipeline or gc.o when using the CPS pipeline.
  • If the code is expected to be linked to Rocq afterwards, use rocq_ffi.o to bind the rocq_msg_* functions with Rocq's code. Otherwise use rocq_c_ffi.o to bind those to functions that print to standard output and standard error, or exit the program after printing a message on user_error.
  • If the code is using primitive integers or floats, it must include prim_int63.o and prim_floats.o respectively.

Hence the standard setting to build a standalone executable is:

RUNTIME_LIBS = gc_stack.o rocq_c_ffi.o prim_int63.o prim_floats.o

Compiling and running programs

The CertiRocq Eval command provides an all-in-one command that produces C files, compiles them with gcc (preferably) or clang-11, dynamically loads the code and runs it, finally reifying the result to a Rocq term. In this case the libs are:

RUNTIME_LIBS = gc_stack.o rocq_ffi.o prim_int63.o prim_floats.o

The certirocq_eval c k tactic compiles and evaluates c and passes the reified result to the ltac continuation function k (usually of the form ltac:(fun c_value => ...). Beware that at Qed time, Rocq cannot call back the compiler, any conversion between c and c_value that is necessary for typechecking will be performed by the standard conversion algorithm of Rocq.

Compiling and running standalone programs

The CertiRocq Run command provides an all-in-one command that produces C files, compiles them with gcc (preferably) or clang-11, and runs them, redirecting standard output to Rocq's info channel and standard error to Rocq's warnings channel. The generated program can also be run standalone outside of Rocq in this case. The libraries in this case are:

RUNTIME_LIBS = gc_stack.o rocq_c_ffi.o prim_int63.o prim_floats.o

Printing λANF

The CertiRocq plugin allows to emit λANF, the core intermediate representation of CertiRocq.

CertiRocq Show IR <options> <definition>.

CertiRocq Show IR <options> <definition> 
  Extract Constants [ constant1 => "c_function1", 
                      ... , 
                      constantN => "c_functionN" ].

Note that the program is printed after compilation through the λANF pipeline, and it is closure-converted and hoisted (i.e., all functions are defined at the top-level, just as a C program).

Compiling Gallina to Wasm

CertiRocq Compile Wasm <options> <definition>.

This command produces a single WebAssembly binary that can be run with any modern Wasm runtime. The compilation uses the same pipeline as the C backend - up until the λANF layer, so the relevant options are supported (see above).

The generated binary adheres to the 1.0 standard of WebAssembly, but may additionally use Tail-Call instructions. (The Tail-Call proposal is part of the Wasm 3.0 standard and supported by the major engines.) How to run such a Wasm binary is described here.

Add a custom footer

Clone this wiki locally