ProofCompiler

Certificate translation through compilation and optimization — ICFEM 2009 research prototype.

ProofCompiler translates Coq proof certificates alongside annotated programs: from a small C-like source language to RTL, then through compiler optimizations. This repository preserves the historical INRIA/MOBIUS prototype and an experimental port to Rocq 9.3.0 and OCaml 5.5.2.

Five historical examples produce certificates accepted by the Rocq kernel and independently checked with coqchk. The matrix experiment has been rerun functionally; its certificate sizes are not an exact numerical reproduction of the 2009 results. Quicksort remains incomplete. This is research software, not a complete C compiler or a proof of correctness of the compiler itself.

Scientific origin

The software was developed at INRIA within the MOBIUS project. Sylvain Heraud, coauthor of the software and paper, supplied the recovered archive and confirmed its historical public distribution under the GPL. The original distribution infrastructure is no longer available. ARCHIVE.md distinguishes this contributor testimony from independently verified records. The precise SVN revision and its identity with the snapshot used for the paper are unknown. No upstream version-control history has been reconstructed.

Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, César Kunz, and Anne Pacalet. Implementing a Direct Method for Certificate Translation. In Formal Methods and Software Engineering, ICFEM 2009, Lecture Notes in Computer Science 5885, pp. 541–560. Springer, 2009. DOI: 10.1007/978-3-642-10373-5_28. Publisher's record.

This preservation and porting effort is not an official continuation of INRIA or MOBIUS, and does not imply endorsement by the institutions or all paper coauthors.

Branches and historical reference

Reference	Purpose	Status
main	Selected historical source archive, provenance, licenses and manifests	Frozen archive; not maintained; historical Coq 8.2pl1 build unvalidated
modern-rocq	Rocq 9.3.0 / OCaml 5.5.2 adaptations, checked examples and reproduction instruments	Experimental port; only the documented environment and cases are qualified
archive-import	Initial import of 450 historical files	Preserved archival tag; predates restoration of the linking helper

The fourth archival commit restores the unchanged historical helper, bringing the retained selection on main to 451 files. Modern adaptations are subsequent commits on modern-rocq; they do not rewrite the archival commits or tag. The original README, source/test reference files and .oracle files remain available. Historical tests and oracles have not been regenerated to fit the port.

Compiler and certificate pipeline

1. Parse and type-check .src programs with contracts, assertions and loop invariants.
2. Generate source verification conditions using weakest-precondition and strongest-postcondition machinery; discharge them with supplied Coq proof scripts.
3. Compile the program to an RTL control-flow representation and generate RTL obligations.
4. Transform the source certificates into RTL certificates, retaining their logical dependencies. The implementation supports constant propagation, common subexpression elimination (CSE), branch elimination and dead-code elimination.
5. Construct analysis certificates where needed, combine them with program certificates, and translate the combined proofs through optimization.
6. Check the resulting terms against their obligations in Rocq; export the qualified certificates for checking in a separate coqchk process.

The modern port uses the actual historical compiler and translation routines, with adapted Rocq APIs and explicitly recorded proof-script compatibility changes. It does not replace transformed certificates with independent proofs of the optimized programs. The coverage report records which transformations change obligations and use their input certificates.

Build and reproduce

Use modern-rocq, with Rocq 9.3.0 built with OCaml 5.5.2, on the tested macOS arm64/Homebrew environment. The scripts use /opt/homebrew/bin and GMP under /opt/homebrew/opt/gmp/lib, plus Python 3, findlib and the installed Rocq OCaml packages. Other versions and platforms have not been qualified. There is no automatic dependency installation or historical makefile execution.

From the repository root, validate the build, check_index, independent proof checking, negative logical tests, oracles and integrity:

PROOFCOMPILER_BUILD_DIR="$PWD/_build-modern/base-validation" sh modern/validate.sh

Run the full historical example suite in another fresh directory:

PROOFCOMPILER_BUILD_DIR="$PWD/_build-modern/extended-validation" sh modern/validate_extended.sh

The extended suite currently exits with status 1: Quicksort is incomplete, and matrix has a partial oracle comparison. Inspect its result matrix and logs; a zero process status alone is never taken as proof validation.

Rebuild and measure the matrix certificates, including Quicksort diagnostics:

python3 modern/experiments/reproduce.py --build-dir _build-modern/matrix-reproduction

Use a new directory name for each extended suite or experimental run. The experimental recipe checks the known partial results explicitly; its successful completion does not mean that Quicksort passes or that the 2009 sizes match. See README-MODERN.md for prerequisites, outputs and targeted commands, and BUILD-HISTORICAL.md for the separate, unvalidated Coq 8.2pl1 reconstruction instructions.

Validated examples

Historical input	Qualified transformation	Source and translated certificates	Independent coqchk	Oracle comparison
check_index.src	Source → RTL, with index obligations	PASS	PASS	PASS
branch.src	Branch elimination and dead-code elimination	PASS	PASS	PASS
cnst_opt.src	Constant propagation	PASS	PASS	PASS
cse_opt.src	Common subexpression elimination	PASS	PASS	PASS
matrix.src	RTL, CSE analysis, merge and optimized certificates	PASS	PASS	PARTIAL

PASS refers to the precise checks and options in the coverage report, supplemented by the matrix measurement report for merge/native exports. Oracle checks distinguish presentation differences from comparison of instructions and obligation types. They do not require every generated file to be byte-identical to its historical printout. Negative controls reject open goals, suspended goals, unresolved evars, incorrect certificates and incompatible universes; an additional check rejects unresolved flexible universes.

Matrix experiment: modern and published sizes

Each cell is modern / published (2009), in syntax-tree node occurrences. Modern measurements use the actual proof terms in memory, before textual export.

Obligation	Source	RTL	Analysis	Merge	CSE
Pre	2477 / 2922	2385 / 2960	109 / 109	5874 / 7615	5874 / 7615
annot(l2)	6909 / 8746	6399 / 8272	138 / 138	17764 / 23276	17764 / 23276
annot(l4)	25113 / 33232	23989 / 32418	261 / 261	65951 / 86962	65951 / 86962
annot(l7)	67797 / 95195	64564 / 93907	229 / 229	128004 / 178012	187160 / 253575

The four Analysis values match. The other sixteen values are 15.23–31.25% lower. This is not evidence of an algorithmic improvement or exact reproduction. Modern arithmetic proofs, library bodies and Rocq term representations differ from Coq 8.2. The counter does not recursively unfold referenced constants; normalization occurs at specific translation stages. Source loop certificates are combinations of two proofs, following the archived compiler's routine. The original table-generation script and exact source revision remain unknown.

Reprinting and reimporting Gallina also changes some Merge/CSE term sizes while preserving validity, so those secondary measurements are reported separately. No scaling factor or counter adjustment was used. Consult the method and scientific assessment, absolute and relative differences, and machine-readable measurements and logs.

Scientific and technical limitations

• Quicksort is incomplete. Its first missing fragment exists under an older name and proves the current obligation unchanged. Two candidate fragments pass; four still fail. Three precondition fragments contain historical Admitted. The contract of partition also needs analysis for the permutation required by quick_rec. No complete Quicksort certificate is claimed.
• Matrix has a partial oracle. matrix_sp.cse.oracle ends inside node 32. Its complete prefix and the available obligation types are checked, but the full analysis graph cannot be compared with that truncated reference.
• Certificates depend on an abstract memory model. Historical Memory parameters and the actual transitive assumptions are reported. Kernel acceptance does not instantiate a concrete machine memory or establish termination. Matrix was run without -idx; it is not a memory-safety result.
• Historical alldiff is problematic. Its definition is contradictory on nonempty lists because it also requires each element to differ from itself. It is unchanged. It is absent from the transitive dependencies of the measured matrix certificates; this does not qualify every possible use in the compiler.
• The historical corpus contains incomplete proofs. Their presence is preserved for provenance, not presented as verification. Qualified runs reject missing certificates and unauthorized assumptions instead of admitting goals.
• Compatibility is deliberately narrow. Only Rocq 9.3.0 / OCaml 5.5.2 on the documented environment is tested. Some internal APIs and larger proof cases remain unqualified. Known external findlib warnings are retained.

See KNOWN-LIMITATIONS.md for details and the publication qualification for the final checks. Detailed technical reports are currently in French.

Citation, license and navigation

CITATION.cff gives the five-author paper as the preferred scientific citation. When citing an execution or this recovered software, also record the branch and exact Git commit, plus the environment and options used. The archival-preparation credit does not assert sole authorship of the historical implementation. No software DOI or public release date is invented.

The original GNU GPL v3 license text and existing notices are retained; 32 core historical source files explicitly permit version 3 or later. The third-party record documents the restored linking helper and five excluded optional documentation auxiliaries with unresolved file-specific terms. These exclusions affect historical documentation generation, not the modern compiler validation targets.

Location	Contents
src/	Compiler, Rocq adapter and proof libraries on this branch
tests/	Unchanged historical inputs, proof fragments and oracles
modern/proofs/	Explicitly documented compatibility copies of proof scripts
modern/experiments/	Nonintrusive measurement and diagnostic instruments
modern/	Validation scripts, reports and retained execution evidence
archival/	Original manifests, file selection and privacy review
ARCHIVE.md	Historical provenance, omissions and import record