GuardCert

GuardCert is a Rocq framework for proving guarded program transformations correct and for composing them into verified whole-program compilation with CompCert.

Many optimizations are only valid under a precondition that a compiler cannot decide statically: loop tiling of a C loop nest with runtime bounds is correct only if the bounds stay in a range where the transformed index arithmetic does not overflow and every array access stays in bounds. GuardCert installs such an optimization as a guarded replacement of the original code region:

run a generated check G (it may read the program state and write private temporaries)
if G accepts then
    run the optimized candidate, then restore the variables the rest of the program can observe
else
    run the original code

and proves that the resulting whole program refines the original one. The check, the candidate and the restoration code are generated and proved by verified Rocq code; external tools (here the Pluto scheduler) only propose schedules, tile sizes and parameter ranges, and every proposal is checked.

This repository contains the framework, its instantiation for CompCert's Clight language, a polyhedral loop-optimization instance built on the verified validators and code generator of PolCert, two extracted whole-program compilers, and three end-to-end examples.

What is proved

The development is organized in layers:

1. Language-independent kernel (prototype/interface/GuardInterface.v, theories/AbstractGuard.v, theories/SemanticFacts.v). A host language provides commands, checks and a selection construct select G yes no with its execution law. A guard certificate states that the check is safe on a domain of entry states, always produces a result, and, when it accepts, establishes the optimization's premise together with a relation between the original entry state and the checked state (refusal has no meaning other than "use the original code"). A conditional certificate (or its preservation counterpart) states that the candidate is correct from accepted states and the fallback from refused states. guardify_refinement, guardify_preservation and guardify_program_refinement combine them into the correctness of select G candidate fallback and of a program that contains it. These theorems use no axioms.

2. Condition services (theories/, adapters/compcert-memory/). Executable checks with soundness proofs: capture of loop bounds read from memory, interval profiles for runtime parameters, array-footprint (in-bounds) checks, machine-word range checks for generated index arithmetic, and the corresponding read permissions in CompCert's memory model.

3. Clight host and installation (theories/Clight*.v, prototype/interface/Clight*.v, prototype/interface/DirectRegionInstallation.v). Regions are selected in the actual Clight program; the host checks names, scopes and control flow at the region, proves that private temporaries are fresh, restores the public exit state (loop counters and scalars that the rest of the program can read) and lifts the local result to a forward simulation of the whole Clight program.

4. Polyhedral optimization instance (adapters/compcert-memory/, theories/PolCert*.v). A loop region over double-precision arrays is decoded into PolCert's polyhedral model; a schedule and tiling proposed by Pluto is checked with PolCert's verified validators (affine scheduling, tiling and band validators), PolCert's verified code generator produces the candidate loop, which is lowered to Clight with checked machine-word arithmetic. The generated check captures the runtime parameters and verifies the conditions that the candidate's proof needs.

5. Complete compilation. Each compiler entry is composed with CompCert's front end and back end. The two entries used by the examples have the theorems

   DirectDoubleContextCompiler.compile_selected_direct_double_context_program_correct :
     forall chosen private_count phase lower upper program target,
     mayReturn (compile_selected_direct_double_context_program
                  chosen private_count phase lower upper program) (OK target) ->
     backward_simulation (Csem.semantics program) (Asm.semantics target).
   
   DirectParametricDoubleBandCleanupCompiler.compile_selected_direct_parametric_double_band_cleanup_program_correct :
     forall chosen private_count phase budget lower upper program target,
     mayReturn (compile_selected_direct_parametric_double_band_cleanup_program
                  chosen private_count phase budget lower upper program) (OK target) ->
     backward_simulation (Csem.semantics program) (Asm.semantics target).

   program is the CompCert C program (Csyntax) and target the generated x86-64 assembly program. The arguments chosen (selected regions), private_count (a budget of fresh names), phase (the scheduler interface), budget and lower/upper (proposed parameter profile) are untrusted inputs: the theorem holds for all of them. mayReturn is PolCert's semantics of computations that call untrusted oracles: the theorem holds for every result the computation may return. This is the same kind of statement as CompCert's own Compiler.transf_c_program_correct.

Trusted base and assumptions

make audit runs Print Assumptions on the two compiler theorems, on the kernel theorems and, for comparison, on CompCert's transf_c_program_correct, and checks the result against the classified list in scripts/assumptions.json. The kernel theorems are closed. The two compiler theorems use 42 assumptions:

• the 35 assumptions of CompCert's own correctness theorem: standard logical axioms (classical logic, functional extensionality, proof irrelevance, the axioms of the classical real numbers of the Rocq standard library), the semantics of external functions and inline assembly, and CompCert's OCaml-implemented heuristics and options (register allocation, inlining, selection heuristics, printers);
• 7 parameters of PolCert's polyhedral library (VPL): the untrusted polyhedral backend PedraQBackend (t, top, isEmpty, add, pr) and two printing functions of CoqAddOn. They are realized by the extraction directives in scripts/build_compiler.py and OCaml code in adapters/compcert-memory/native/. The theorems are proved for an arbitrary implementation of these parameters (VPL's backend returns certificates that verified code interprets); the OCaml realization is only trusted to respect their types and PolCert's model of computations with oracles.

In addition, as for CompCert itself, the following are trusted:

• the Rocq kernel, extraction to OCaml, and the OCaml compiler and runtime;
• the extraction directives in scripts/build_compiler.py, which map the VPL parameters above and VPL's printing and debugging helpers to OCaml, and replace PolCert's untrusted topological sort (whose result is checked by verified code) by an OCaml implementation;
• the part of the compiler before the theorem's starting point: the C preprocessor (GCC), CompCert's parser and elaborator, and GuardCert's pragma frontend (prototype/annotated-polyhedral/native/GuardScopFrontend.ml). The frontend wraps each #pragma scop region in a labeled block; with the default settings it also folds references to const integer objects in file-scope initializers and flattens variable-length array parameters, as GCC accepts them (neither applies to the examples). Further rewrites are available only through explicit environment variables and are not used here. The theorem is about the Csyntax program that results;
• the assembler and linker (GCC), and CompCert's printing of assembly code.

Untrusted, with every output checked: Pluto, the OCaml code that reads Pluto's output and proposes tiling witnesses and parameter profiles (adapters/compcert-memory/native/GuardDirectDouble*.ml), the region selection and the Fourier-Motzkin and emptiness oracles.

Scope

This is a research prototype. In particular:

• The optimization instance handles affine loop nests over global double-precision arrays (static double arrays of fixed extent; separate global arrays cannot alias), with long long loop counters and loop bounds given by literals or by integer global variables. It runs on x86-64 Linux. Single-precision (float) kernels, pointers to arrays, function parameters as loop bounds and general aliasing are not supported in this release.
• Runtime parameters are supported through a finite interval profile [lower, upper] chosen at compile time (environment variables GUARDCERT_TREE_LOWER/GUARDCERT_TREE_UPPER) together with the array extents: the generated check accepts only parameter values for which the candidate's machine-word and footprint conditions hold; all other values run the original code. The check is a sufficient condition, not the weakest one.
• If a region cannot be decoded, validated or installed, the compiler leaves it unchanged; this is a compile-time refusal, not a runtime fallback.
• No performance claim is made. The guarded program can be slower than the same program compiled without the optimization (it is in the Jacobi examples): the schedule is Pluto's, and the check, the generated loop bounds and the restoration of the public exit state have a cost.

Examples

Three complete C programs in examples/ are compiled by the verified compilers. Each program reads its loop bounds from the command line into global variables, so they are runtime parameters; the marked region is a benchmark kernel (see the adaptations below). make -C examples (or python3 examples/run.py --paths NAME) compiles each program with GCC (-O0, reference), with the GuardCert compiler with optimization proposals disabled (plain), and with the example's optimization policy (guarded); it checks that the guarded replacement was installed (the guarded Clight differs from the plain Clight), runs the three executables on each input, compares their complete output (a hash of every array element), and observes with two GDB hardware watchpoints whether the guarded executable runs the candidate or the original loop (after the initialization, the original loop writes two chosen array cells in an order that the candidate does not follow).

matmul: dense matrix multiplication

• Source: examples/matmul/matmul.c. The region is a C rendering of the kernel of the PolCert benchmark matmul (tests/polopt-generated/inputs/matmul.loop) in which every array index is offset by 2: C[i+2][j+2] = beta*C[i+2][j+2] + alpha*A[i+2][k+2]*B[k+2][j+2] over 0 <= i < M, 0 <= j < N, 0 <= k < K. M, N, K are long long globals set from the command line (at most 513); the arrays are 520 x 520.
• Compiler: build/compiler/context-int/ccomp (DirectDoubleContextCompiler.compile_selected_direct_double_context_program).
• Optimization target: Pluto's affine schedule tiled by 32 x 32 x 32, without intra-tile reordering; parameter profile [0, 512].
• Generated guard: read M and, only where the original loop would read them, N and K; accept if each is in [0, 512] (the array extent 520 already covers this profile). On acceptance the tiled candidate runs and the exit values of i, j, k are restored; otherwise the original loop runs.

Input M N K	Observed path	Output equal to GCC and to the plain build	State hash
128 96 160	candidate	yes	40633ddcf2a51b8b
512 512 64	candidate	yes	1e45b4656c866cb7
513 96 32	original loop (guard refuses, M > 512)	yes	70f0f414f269c132
0 0 0	no write (empty iteration space)	yes	b1240f765b145b6c

jacobi-1d: one-dimensional Jacobi stencil

• Source: examples/jacobi-1d/jacobi1d.c. The region is a C rendering of the kernel of the PolCert benchmark jacobi-1d-imper (tests/polopt-regression/inputs/jacobi-1d-imper.loop) in which the indices of a are offset by 1: per time step t < T, b[i] = 0.33333*(a[i-1]+a[i]+a[i+1]) for 2 <= i < N-1, then a[j] = b[j] for 2 <= j < N-1. T and N are long long globals set from the command line (T at most 1048576, N at most 4096); the arrays have 4099 and 4097 elements.
• Compiler: build/compiler/band-parametric-cleanup-int/ccomp (DirectParametricDoubleBandCleanupCompiler.compile_selected_direct_parametric_double_band_cleanup_program): PolCert's band (time-tiling) validator and code generator with runtime parameters, followed by a proved simplification of the generated loops.
• Optimization target: Pluto's diamond tiling with tile size 32; parameter profile [0, 1048575].
• Generated guard: read T and, if the time loop runs, N; accept if both are in [0, 1048575] and the accesses of the candidate stay inside both arrays (N + 1 <= 4099 whenever the space loop runs). On acceptance the candidate runs and the exit values of t, i, j are restored; otherwise the original loop runs.

Input T N	Observed path	Output equal to GCC and to the plain build	State hash
4096 4096	candidate	yes	cce5f07e88c670fd
64 128	candidate	yes	8c680048eba44291
8192 4096	candidate	yes	edbeb1e76909fd19
1048576 16	original loop (guard refuses, T > 1048575)	yes	63447ec98fbac4a4
0 64	no write (empty iteration space)	yes	2b1d7dbf2ba821a6

jacobi-2d: two-dimensional Jacobi stencil

• Source: examples/jacobi-2d/jacobi2d.c. The region is the kernel of the Pluto/PolCert benchmark jacobi-2d-imper, unchanged; T (at most 1048576) and N (at most 2000) are long long globals set from the command line; both arrays are 2000 x 2000 and, unlike in the benchmark, both are initialized.
• Compiler and optimization target: as for jacobi-1d (same compiler binary, diamond tiling, profile [0, 1048575]). The same proved compiler entry handles the additional loop dimension without new proofs.

Input T N	Observed path	Output equal to GCC and to the plain build	State hash
64 2000	candidate	yes	b8e87ea3941515e1
32 64	candidate	yes	9b8ab1be17a788ef
1048576 16	original loop (guard refuses, T > 1048575)	yes	2e841f7eff7b912c
0 64	no write (empty iteration space)	yes	be5d2244cc730379

For each program, the whole-program result is the theorem of the compiler entry above applied to that program: the compiled assembly program is a backward simulation of the Csem semantics of the C program. The tables report test runs, not additional proofs; the runner writes the details, including the generated Clight (*.light.c) and the scheduler's input and output files, to build/examples/<name>/. In these runs the guarded programs were not faster than the plain ones (the Jacobi candidates were slower); see Scope.

Adaptations from the benchmark programs: the loop bounds are global variables read from the command line instead of compile-time constants, the arrays have the fixed extents given above, the programs print a hash of all array contents instead of the original output, and the matmul and jacobi-1d kernels use the index offsets described above. The jacobi-2d region is the benchmark's code, unchanged.

Building

Requirements: Linux on x86-64, GCC, GNU make, Python 3.9 or later, curl, git, patch, Docker (to build and run Pluto) and, for the path observation, GDB. No system OCaml or Rocq installation is needed.

make toolchain              # private opam switch in _toolchain/ (OCaml 4.14.1, Rocq 9.2.0, ...)
. _toolchain/env.sh
make JOBS=16 deps compcert  # CompCert 3.18 and the pinned, patched PolCert sources
make JOBS=16 proofs audit   # GuardCert proof closure and the assumption check
make JOBS=16 compilers      # build/compiler/<entry>/ccomp
sh scripts/build_pluto.sh   # untrusted scheduler, built in the PolCert image
make -C examples            # compile, run and compare the examples

make toolchain downloads opam 2.6.1 and, if no GMP development files are found, builds GMP 6.3.0 into the same directory; an existing opam switch with the versions listed in toolchain.lock.json can be used instead. All dependencies are fetched from their public sources at the revisions pinned in toolchain.lock.json, adapters/polcert-optimizer/source.lock.json and scripts/pluto.env, and are checked against recorded SHA-256 sums where the source is an archive or a file set. The opam packages are installed at the listed versions from the current opam repository; their own dependencies are resolved by opam at installation time.

Measured on an x86-64 server with 32 parallel jobs, starting from a fresh clone: the toolchain took 5 minutes, fetching and compiling CompCert and fetching PolCert 2 minutes, the GuardCert proof closure (441 GuardCert and 91 PolCert files) 17 minutes and the assumption check 1 minute, both compilers together 3 minutes, Pluto 4 minutes and the examples under 1 minute. The proof closure needs up to about 10 GB of memory for the largest files.

Pluto is built and run inside the Docker image hughshine/polcert, pinned by its digest in scripts/pluto.env. PolCert's own Dockerfile also uses images from the hughshine Docker Hub namespace.

To compile another program, mark the loop nest with #pragma scop and #pragma endscop and call the compiler like examples/run.py does, e.g.

GUARDCERT_PLUTO=$PWD/scripts/pluto.sh GUARDCERT_DIRECT_OUTPUT=$PWD/build/phases \
GUARDCERT_PHASE_KIND=tiled GUARDCERT_TILE_SIZES=32 GUARDCERT_PHASE_INTRATILE=0 \
GUARDCERT_TREE_LOWER=0 GUARDCERT_TREE_UPPER=512 GUARDCERT_DOUBLE_PRIVATE_COUNT=64 \
  build/compiler/context-int/ccomp -conf build/compiler/context-int/compcert.ini -S program.c
gcc program.s -o program

The GUARDCERT_* variables only configure untrusted proposals; the directory named by GUARDCERT_DIRECT_OUTPUT must exist and receives the scheduler's input and output files. Because scripts/pluto.sh runs Pluto in a container that mounts only this repository, run the compiler from a directory inside the repository and keep that output directory inside it as well.

Repository layout

Path	Contents
prototype/interface/	kernel interface (GuardInterface.v, GuardedRewrite.v), Clight region selection and installation, region factories, whole-program compiler entries
theories/	abstract guard and condition kernel, Clight host libraries, PolCert bridges and Loop-to-Clight lowering, CompCert composition
adapters/compcert-memory/	CompCert memory model services and the double-precision loop instance
adapters/compcert-memory/native/, prototype/annotated-polyhedral/native/	untrusted OCaml: proposals, oracles, pragma frontend
adapters/polcert/, adapters/polcert-optimizer/	PolCert pin and the patches applied to it (Rocq 9.2 port and extensions)
scripts/	toolchain bootstrap, dependency fetching, proof and compiler builds, assumption audit, Pluto build
pluto/	patch applied to Pluto
examples/	the three example programs, their configuration and the runner

License

GuardCert is distributed under the GNU Lesser General Public License, version 2.1; see LICENSE. NOTICE.md lists the third-party components, the files adapted from them and the licenses of the patches to PolCert, VPL and Pluto.