MetaRocq: a verified metatheory for the Rocq prover

What the project is

MetaRocq is a project formalizing Rocq in Rocq and providing tools for manipulating Rocq terms and developing certified plugins, meaning translations, compilers or tactics, in Rocq.

That sentence contains three things, and the third is the reason the first two exist. A certified plugin is one whose correctness rests on a proof rather than on inspection: a tactic that manipulates the prover's terms, a translation from one calculus to another, or a compiler that emits code, each one checked against a specification before you trust it.

The way this project gets there is by first doing the boring work properly. The prover has a type system, and the rules of that system are written down somewhere in the implementation. A metatheory is the study of those rules: whether typing is preserved by reduction, whether the system is confluent, whether every term has a smallest type, whether a well-typed program cannot go wrong. If you write a plugin that manipulates terms, those theorems are the contract you are working against, and if they are only informally true, your plugin is built on sand.

So the project's structure follows from that. It contains a metatheory, and then the things that the metatheory makes possible.

The organisation is worth noting. At the centre is a quoting library, and the project is a single repository that extends it with additional features, each extension in a dedicated folder. There is a dependency graph published as an image, and the readme suggests it may be useful for navigating the project, which is what you say about a codebase of about three hundred thousand lines of the prover's own language and thirty thousand lines of the implementation language.

Those two numbers are the scale of the thing, and they are the first thing a reader should absorb. This is not a library that wraps the prover; it is a research-scale reimplementation of the parts of the prover that a plugin author needs, with the mathematics done first and the code second.

The distribution model is the prover's own package system, with a separate package for each component, and the readme points at installation and documentation documents in the repository rather than duplicating them. The channel is a chat server, and there is a badge for opening the project in an editor, which for a project whose artifacts are source files in a proof assistant is the sensible default.

The quoting library, and why quoting comes first

The central component is a quoting library, and the readme's description of it is short enough to state in full: it takes terms and constructs a representation of their syntax tree as an inductive data type, and the representation is based on the kernel's term representation.

That last clause is the design decision. A plugin that wants to inspect a term could work with the prover's own internal representation, or with a copy of it, or with its own simplified model. Working with the kernel's representation means the thing a plugin inspects is the thing the kernel checks, which is the only way a quoting-based tool can be trusted to see the same term the type checker will see.

The library exposes that representation through a small set of commands. There is a command to test the quotation of a term, one to quote a definition under a name, and one to quote a definition recursively, which follows the definitions the term depends on. And there is a tactic that quotes a term and hands the result to a continuation.

That last shape, a term and a continuation, is the interface a tactic author actually works with, and the fact that the library provides it rather than only a value is the difference between a quotation library and a quotation facility.

Around that core the readme lists four more capabilities, and together they are the API a plugin needs.

There is reification of the environment structures, covering constant and inductive declarations along with their universe structures. In other words, you can ask not just what a term is but what the constants and the inductive types in scope are, and at which universe levels. That is what you need to write a tactic that adds a new declaration.

There is denotation of terms and global declarations, which is the reverse direction: given a term you have built, get back the thing the prover will treat as that term.

There is a monad for querying the environment, manipulating global declarations, calling the type checker, and inserting them into the global environment, in the style of the metaprogramming tactic system. And monadic programs of that shape are run by a command. This is the layer that turns a quotation library into a development environment: the monad is where the read, check and insert operations live.

And then there is a formalization of the typing rules, reflecting the ones of the prover, and the readme is precise about its scope: it covers all of the prover except eta-expansion and template polymorphism. Naming the exceptions is a good sign, because a formalisation that quietly omits something is worse than one that admits it.

A cleaned-up calculus, and what has been proved about it

The second major component is a formalisation of the term language, and the readme gives it the full name of the Polymorphic Cumulative Calculus of Inductive Constructions, with the shorter name used in the directory. It is a cleaned up version of the prover's term language and its type system, and it is shown equivalent to the prover's own.

So the approach is: take the real system, rewrite it so that the rules are easier to reason about, prove that the rewrite preserves the meaning, and then work with the clean version. That is a standard technique and it is the reason the component exists at all, because the prover's own type system is large enough that proving things about it directly is painful.

What has been proved about this calculus is the list in the readme, and it is a long one, and it is the heart of the project.

There is weakening for global declarations, and weakening and substitution for local contexts, which are the basic structural rules. There is confluence of reduction, using a notion of parallel reduction, which is the statement that the order in which you reduce does not matter. There is context cumulativity and conversion, and the validity of typing. There is subject reduction, with a stated exclusion for case and cofix reduction. There is principality, that every typeable term has a smallest type, which is the property a bidirectional presentation depends on.

There is a bidirectional presentation of the system, an equivalent presentation that enforces the directionality of the typing rules, and strengthening follows from it. There are the elimination restrictions, which ensure that singleton elimination from the proposition sort to the type sort is only allowed on singleton inductives in the proposition sort. There is canonicity, that the weak head normal form of a term of inductive type is a constructor application. There is consistency under the assumption of strong normalization. And there is weak call-by-value standardization, that normal forms of first-order inductive terms can be found by weak call-by-value evaluation.

Two things are worth noticing about that list. The first is that the metatheory is not one theorem but a foundation: a verified type checker needs subject reduction and canonicity, an erasure pipeline needs the typing rules to know what to erase, and a plugin framework needs principality to know that adding a declaration preserves meaning.

The second is the exclusions, which appear twice. Subject reduction excludes case and cofix reduction, and consistency is under the assumption of strong normalization. Neither is an oversight; both are the standard boundary of what is provable without assuming the system terminates. A proof assistant whose own termination is not proved can have a metatheory that is conditional on termination, and saying so explicitly is what makes the rest of the work usable rather than merely impressive.

The safe checker, and what verified buys you

The third component is an implementation of a fuel-free and verified reduction machine, conversion checker and type checker for the calculus. The readme also says it relies on a postulate of strong normalization of the reduction relation on well-typed terms, and that the checker is shown to be correct and complete with respect to the calculus specification.

Correct and complete is a strong pair of claims, and they are the right ones to make about a type checker. Correct means the checker accepts everything that should be accepted. Complete means it accepts nothing that should not be. A checker that is correct but incomplete is unsound in the direction of rejecting good programs, which is safe but useless. A checker that is complete but incorrect is unsound in the dangerous direction, and it is the case that a plugin author has to be most afraid of.

The word fuel-free matters too. A fuel-based checker is one that is given a budget and stops when it runs out, which is a practical engineering choice for a type checker that must terminate on a term that does. Fuel-free here means the machine does not need a budget, because the strong normalization postulate guarantees it terminates on well-typed input. The postulate is doing real work: it is the assumption that lets the implementation be simple and the proof be short.

The extracted checker is available in the prover as a new vernacular command, and the readme gives the exact form and the module to import first.

MetaRocq SafeCheck <term>

And then it gives you the comparison you would want. There is a second command that runs the prover's own type checker, so that you can see roughly how the times compare.

MetaRocq RocqCheck <term>

That pairing is a nice piece of engineering communication. A verified checker that is ten times slower than the built-in one is a curiosity; a verified checker that is comparable in speed is something you can actually deploy. The readme invites you to compare rather than asserting a number, which is the honest way to present a performance claim you have not measured in every configuration.

There is also a verified and efficient re-typing procedure, in a separate module, and the readme notes it is useful in tactics. Re-typing is what a tactic does when it builds a term and needs to know its type without a full re-check, and a verified fast path for it is exactly the piece a plugin author needs and cannot easily build themselves.

Erasure, and the plugin architecture

The fourth component is erasure: a procedure to an untyped lambda calculus that accomplishes the same thing as the type and proof erasure phase of the prover's own extraction plugin. The extracted safe erasure is available as another vernacular command.

MetaRocq Erase <term>

Erasure is the step that turns a proof-carrying program into a program, by removing the types and the proofs. It is where the theory meets the practice: a verified erasure procedure is a guarantee that the code you extract does not depend on anything that was erased, which is the property that makes extraction usable for real programs rather than for demonstrations.

And the erasure pipeline includes verified optimisations, which the readme lists, and they are worth reading because they are the interesting part of the work. There is a transformation that removes lets in constructors, one that removes cases on propositional terms, one that switches to an unguarded fixpoint reduction rule, and one that transforms higher-order constructor applications into first-order blocks for easier translation to usual programming languages.

That last one is the tell. The point of erasure is to get to a language somebody else can compile, and the higher-order constructs of the proof language are exactly the ones that do not survive the trip. A verified transformation that flattens them is a transformation that is part of the specification rather than an afterthought in the backend, and the readme's phrase about easier translation is the honest way to say that the output is being shaped for the target.

The repository structure shows how the components relate. There is a directory for the quoting library, one for the calculus, one for the safe checker, one for erasure, one for the erasure plugin, one for the safe checker plugin, and separate ones for the quotation layer and for a shared utility and common package. The plugin directories are the ones that turn the verified components into commands the prover can run, and their existence is the reason the earlier two commands exist at all.

And there is a translations directory holding examples built on top of the whole stack, the first of which is a parametricity plugin. Parametricity is the property that says a program's behaviour is independent of the types it is instantiated at, and a parametricity plugin is the most demanding thing you can build with a metatheory, because it needs the metatheory to reason about types rather than only about terms. The readme lists it as an example, which means the project considers it within reach of its own machinery.

The build, the examples, and the release discipline

The build file is a conventional multi-project make file, and two of its targets are worth reading.

There is a configuration target that prints which configuration you are in, and it refuses to run if the configuration has not been set up, telling you to run the configuration script first. The build supports a local configuration, in which the library path is assembled from the working directory so that you are building against the checkout rather than against an installed copy, and it detects a Windows environment by looking for the path conversion command, because the path separator differs between the Windows and the Unix form of the same thing. That one conditional is the entire Windows support story of the build system, and it is the sort of detail that is invisible until it is wrong.

There is also a documentation target that builds the reference with a multi-index option, a table of contents, and a header and a footer taken from files in the repository, with the links to the prover's own standard library pointing at a specific version of the prover's documentation. Pinning that link to a version is a small thing that stops the generated documentation from quietly describing a different library than the one it was built against.

The examples directory is the best way to see what the project does, and its file names are a curriculum. There is a demo, a tour with a prelude that the tour itself depends on, an example that adds a constructor to an inductive type, one that writes a tactic about constructors, an automated theorem prover example, and one that checks typing correctness. The tour and its prelude are how the project teaches itself, and the fact that the tour has a separate prelude file means it is built the way a user would build their own project.

Around the top level there are the documents a large research project accumulates. There is a document for the documentation, one for installation, one describing how releases are made, one for outstanding work, and a separate document on typed equality, which is the kind of topic that gets its own document in a proof assistant because it is subtle enough that the answer is not obvious from the definitions. There is a script that checks the outstanding-work list, which is a small automation that keeps a to-do file honest.

And there is a Nix directory with a default expression, which is the modern way to make a project buildable by people who do not have the prover's toolchain installed and configured, and a directory containing the published dependency graph as an image.

The release history is the last thing, and it is the clearest statement of the project's relationship with the prover. The releases are named for the prover version they target, with a version of the project paired to a version of the prover, and there is a release for two consecutive prover versions. So the project is not released independently of the prover; it is released alongside it, which is the only sensible arrangement for something that reimplements part of it.

Editorial conclusion

MetaRocq fits somebody building a certified tactic, a certified translation, or a certified compiler inside a proof assistant, where the cost of an unsound metatheory is a proof that does not hold. It does not fit an application developer who simply wants to use the prover. Verify first which version of the prover you are on, since the releases are named for the prover release they target, that the features you need are outside the stated exceptions, because the typing formalisation explicitly leaves out eta-expansion and template polymorphism, and that the parts of the pipeline you rely on are the ones that were extracted and are stated to be correct and complete rather than the parts that are only proved correct.

Frequently asked questions

Official sources

1. License: MIT
2. MetaRocq/metarocq on GitHub
3. Project website
4. README
5. Releases