Matthieu Sozeau
email: matthieu.sozeau@inria.fr

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Proof assistants have become invaluable tools in the hands of mathematicians, computer scientists and proof engineers that aim to build certified theories, software, systems and hardware, as evidenced by successful, large formalization projects ranging from famously hard mathematical results ( [START_REF] Gonthier | A Machine-Checked Proof of the Odd Order Theorem[END_REF], [START_REF] Thomas | A formal proof of the Kepler conjecture[END_REF]) to realistic compilers ( [START_REF] Leroy | Formal certification of a compiler back-end, or: programming a compiler with a proof assistant[END_REF], [START_REF] Kiam Tan | The verified CakeML compiler backend[END_REF]), program logics ( [START_REF] Jung | Safe systems programming in Rust[END_REF][START_REF] Appel | Program Logics -for Certified Compilers[END_REF]), operating systems ( [START_REF] Klein | seL4: formal verification of an OS kernel[END_REF][START_REF] Gu | CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels[END_REF]) and even hardware design ([2, 36, 14]). Ultimately, however, all these formalizations rely on a Trusted Theory Base (TTB), that consists of the mathematical foundations of the proof-assistant -most often a variant of Higher-Order Logic, Set Theory or Type Theory-and a Trusted Code Base (TCB): its actual implementation in a general purpose programming language. To obtain the highest guarantees on the proof assistants results, one should in principle also verify the consistency of the foundations, usually by building models in a Trusted Theory (Zermelo-Fraenkel Set Theory being the most common one), the adequacy of the implementation with this theory, and the correct compilation of this implementation.

Goals of the project

The theory behind Coq's calculus, the Polymorphic Cumulative Calculus of (Co-)Inductive Constructions (PCUIC), is rather well-studied and well-tested now: most important fragments have accepted consistency proofs and no inconsistency was found in the rules that have been implemented in the last 30 years. That is, until a new axiom like Univalence breaks implicit assumptions in the calculus as happened recently for the guard checking algorithm. More worryingly, blatant inconsistencies (accepted proofs of False), are reported at least once a year, due to bugs in the implementation 1 . The source of these bugs falls generally under the category of programming errors and unforeseen interactions between subsystems. Coq is indeed a complex piece of software resulting from 37 years of research and development, incorporating many features in a single system. Its architecture was last revised in the V7 series (1999)(2000)(2001)(2002)(2003)(2004) by Jean-Christophe Filliâtre [START_REF] Filliâtre | A Coq retrospective, at the heart of Coq architecture, the genesis of version 7.0[END_REF][START_REF] Filliâtre | Design of a proof assistant: Coq version 7[END_REF], following the de Bruijn criterion. It means that COQ does have a well-delimited, trustable proof-checking kernel, so these errors are not to be attributed to bad design in general. Rather, the problem is that this "small" kernel already comprises around 20kLoC of complex OCAML code + around 10kLoC of C code implementing a virtual machine for conversion. The system also relies on the whole OCaml compiler when used with the native_compute tactic for fast computation/conversion. To be fair (and grateful!), one should note that we never had to blame OCaml for a miscompilation resulting in an inconsistency. In conclusion, to avoid these errors, we should rather apply program verification to COQ's implementation. This is a slightly different endeavor than the above works. Indeed, mechanized or not, the aforementionned proofs are concerned with idealized versions of the calculus that do not correspond to the actual implementation of PCUIC in OCaml, nor do they have any bearing on its compiled version, a priori. The METACOQ 2 project's goal is to bridge the gap between the model theoretic justification of the theory and the actual implementation of the COQ kernel. To do so, we need to answer the following questions in a formal, concrete way:

• What calculus is implemented by Coq exactly?

• Which meta-theoretical properties hold on the implementation?

To answer these questions, we develop a specification of COQ's type theory ( §2), a COQ definition of a type-checker and conversion procedure that corresponds to the current COQ implementation, and verify both the sanity of the specification and correctness and completeness of the implementation.

Plan of the article. To verify the sanity of the specification we develop the meta-theory ( §3) of the PCUIC calculus and show that it enjoys type preservation ( §3.2.2) and principality ( §3.2.4) of types, along with the expected confluence of reduction ( §3.2.3) and proof that conversion is a congruence. We can then construct a corresponding type checker ( §4) that is shown correct and complete with respect to the specification. Finally, to be able to execute this type-checker on large examples, we can extract it to OCaml and compare it to the type-checker implemented in COQ. Ideally, this last step should also be verified: we present a verified erasure procedure ( §5) that takes a COQ environment and definition and produces a program in an (untyped) weak call-by-value λ -calculus extended with a dummy constructor (λ ). We prove that erasure preserves observations of values, starting from a well-typed closed term. In combination with the CERTICOQ compiler [START_REF] Anand | CertiCoq: A verified compiler for Coq[END_REF] from λ to C-light and the COMPCERT [START_REF] Gallium | The CompCert project. Compilers You Can Formally Trust[END_REF] compiler from C-light to assembly, this will provide an end-to-end verified implementation of COQ's kernel. We discuss the remaining hurdles to realize this and further extensions in section 6.

Attribution

The results surveyed in this article are due to METACOQ team as a whole: Abhishek Anand, Dannil Annenkov, Simon Boulier, Cyril Cohen, Yannick Forster, Meven Lennon-Bertrand, Gregory Malecha, Jakob Botsch Nielsen, Matthieu Sozeau, Nicolas Tabareau and Théo Winterhalter.

Link to the formal development This article is best read online, as links in the text point to the formal development definition, which are generally too large to include in the presentation.

Syntax and Semantics

The METACOQ project initially started as an extension of Gregory Malecha's TEMPLATE-COQ plugin, developed during his PhD on efficient and extensible reflection in dependent type theory [START_REF] Michael | Extensible Proof Engineering in Intensional Type Theory[END_REF]. TEMPLATE-COQ provided a reification of COQ's term and environment structures in COQ itself, i.e. COQ Inductive datatype declarations that model the syntax of terms and global declarations of definitions and inductive types, as close as possible to the OCAML definitions used in COQ's kernel. In addition, it implemented in an OCAML COQ plugin the meta-definitions of quoting and unquoting of terms between the two representations, similarly to AGDA's reflection mechanism. The syntax of terms is given in figure 1. It corresponds closely to COQ's internal syntax, handling local variables (tRel, with a de Bruijn index), free named variables (tVar), existential variables (tEvar), sorts (tSort), the type-cast construct (tCast), dependent products, lambda-abstraction, let-ins and n-ary application (tApp), application of global references: constants, inductives, and constructors, a dependent case analysis construct (tCase, see 3.5 for more details) and primitive projections (tProj), fixpoints and co-fixpoints and finally, primitive integers and floating-point values (a recent [START_REF] Bertholon | Primitive Floats in Coq[END_REF] addition to COQ).

The Template Monad

On top of these syntactic objects, one can define an API much like COQ's OCaml API to interact with the kernel of COQ: adding and looking up global definitions, calling the type-checker or higher-level primitives like proof-search for specific type-class instances. In [START_REF] Sozeau | The MetaCoq Project[END_REF], we show how this can be organized by defining a general TemplateMonad type-class that describes the structure of programs interacting with COQ's kernel. We need a monadic abstraction to encapsulate the handling of the global state of the COQ system that is being manipulated: updates to the global environment but also the obligation handling machinery of PROGRAM [START_REF] Sozeau | Subset Coercions in Coq[END_REF]. An interpreter for actions in this monad (e.g. adding a new definition with a given name and proof term) is meta-programmed in OCAML, using continuations to handle the interactive aspect of execution and maintaining coherence of the system state, similarly to the proof engine monad of the MTAC2 [START_REF] Kaiser | Mtac2: typed tactics for backward reasoning in Coq[END_REF] tactic language.

Using this monad, one can meta-program plugins in COQ that take input from the user, ask for user to provide definitions or proofs of particular types and update the environment from computed definitions. This can be used to define user-extensible translations [44, §4], or to derive lenses for a record definition [44, §5]. The TemplateMonad has a variant that also allows extraction of the monadic programs so they can be run efficiently in OCAML, putting it on par with the development of plugins for COQ directly in OCAML. METACOQ plugins deriving parametricity theorems [44, §4.3.1] and induction principles and subterm relations from inductive definitions [START_REF] Ullrich | Generating induction principles and subterm relations for inductive types using MetaCoq[END_REF] can be defined this way, opening the possibility to verify their implementations. For parametricity for example, one can show that there is a procedure to construct from any well-typed term from COQ a proof that the parametricity predicate derived from its type holds on the term. As shown by Pédrot and Tabareau in [START_REF] Pédrot | The fire triangle: how to mix substitution, dependent elimination, and effects[END_REF], this can in turn be used to build internal syntactic models of richer, effectful type theories.

In the rest of this article, we will review how we built certified foundations needed for such efforts, that is the typing specification and the type inference algorithm used to check well-typedness.

Typing, Reduction and Conversion

The calculus at the basis of COQ is the Polymorphic Cumulative Calculus of (Co-)Inductive Constructions (PCUIC). PCUIC is a general dependently-typed programming language, with pattern-matching and (co-)recursive definitions, universe polymorphic global declarations (constants or inductive types). Its origin is the Calculus of Constructions of Coquand and Huet [START_REF] Coquand | The Calculus of Constructions[END_REF] with β η-conversion, extended by the (Co-)Inductive type definition scheme of Paulin-Mohring [START_REF] Paulin-Mohring | Inductive Definitions in the System Coq -Rules and Properties[END_REF], guarded (co-)fixpoint definitions [START_REF] Giménez | Structural Recursive Definitions in Type Theory[END_REF], universe polymorphism [START_REF] Sozeau | Universe Polymorphism in Coq[END_REF] and cumulative inductive types [START_REF] Timany | Cumulative Inductive Types In Coq[END_REF]. The latest additions to the core calculus are a definitionally proof-irrelevant sort SProp and the addition of primitive types [START_REF] Armand | Extending Coq with Imperative Features and Its Application to SAT Verification[END_REF]. While they are supported in the syntax, they are not yet supported by our specification.

The sort system includes an infinite hierarchy of predicative universes Type@{i} (i ∈ N) and an impredicative sort Prop. We consider Set to be a synonym for Type@{0}, hence its interpretation is always predicative 3 . A specificity of COQ is the treatment of Prop and in particular the singleton elimination rule that allows to eliminate propositional content into computational content, if it is trivial (a proof of absurdity, an equality, conjunction or accessibility proof): we will see in the section on erasure [START_REF] Appel | Program Logics -for Certified Compilers[END_REF] how that is justified from the computational standpoint.

Conversion, Cumulativity

In dependent type theory, conversion and typing are usually intertwined, through the conversion rule which states that a term of type T can be seen as a term of type U for any (well-formed) typed U convertible to T . PCUIC is presented in the style of Pure Type Systems, where this conversion relation is untyped and can be defined independently on raw terms as the reflexive, symmetric and transitive closure of one-step reduction. We hence first define a reduction relation as an inductive predicate that includes all reduction rules of PCUIC: β for application, ι for cases, ζ for let-ins, fix and cofix, delta for constants and congruence rules allowing to apply reductions under any context (under lambdas, dependent products, etc). We take its closure with an additional twist: rather than a strict reflexivity rule, we define an α-equivalence relation that ignores the name annotations of binders (they are included in the core syntax for printing purposes only). Moreover, this relation is parameterized by a relation on universes to implement syntactic cumulativity of universes and inductive types. Indeed in COQ's theory we have: i ≤ j Type@{i} ≤ Type@{ j} A similar rule applies to cumulative inductive types. We call this relation α-cumulativity when instantiated with the large inequality of universes, in which case it is only a preorder. In case we instantiate it with equality of universes, we recover the usual α-conversion relation, which is an equivalence.

Two terms are hence in the cumulativity relation if they can be linked by reductions or expansions up-to α-cumulativity.

Typing

The typing relation of PCUIC is a fairly standard inductively defined relation that mostly corresponds to usual "on paper" treatments (e.g. COQ's reference manual [START_REF]The Coq Proof Assistant[END_REF]):

Touring the MetaCoq project

All_local_env (lift_typing typing Σ) Γ → nth_error Γ n = Some decl → Σ ; Γ tRel n : lift 0 (S n) decl.(decl_type) | type_Sort l : All_local_env (lift_typing typing Σ) Γ → LevelSet.In l (global_ext_levels Σ) → Σ ; Γ tSort l : tSort (super l) | type_Prod na A B s1 s2 : Σ ; Γ A : tSort s1 → Σ ; Γ , na : a A B : tSort s2 → Σ ; Γ tProd na A B : tSort (sort_of_product s1 s2) | type_Lambda na A t s1 B : Σ ; Γ A : tSort s1 → Σ ; Γ , na : a A t : B → Σ ; Γ tLambda na A t : tProd na A B | type_LetIn na b B t s1 A : Σ ; Γ B : tSort s1 → Σ ; Γ b : B → Σ ; Γ , na := b : d B t : A → Σ ; Γ tLetIn na b B t : tLetIn na b B A | type_App t na A B u : Σ ; Γ t : tProd na A B → Σ ; Γ u : A → Σ ; Γ tApp t u : B{0 := u} | type_Cumul t A B : Σ ; Γ t : A → (isWfArity typing Σ Γ B + {s & Σ ; Γ B : tSort s}) → Σ ; Γ A ≤ B → Σ ; Γ t : B | ..

. (* remaining definitions for constants, inductive and coinductive types *)

where Σ ; Γ t : T := (typing Σ Γ t T).

Inductive cumul

(Σ : global_env_ext) (Γ : context) : term → term → Type := | cumul_refl t u : leq_term (global_ext_constraints Σ) t u → Σ ; Γ t ≤ u | cumul_red_l t u v : fst Σ ; Γ t v → Σ ; Γ v ≤ u → Σ ; Γ t ≤ u | cumul_red_r t u v : Σ ; Γ t ≤ v → fst Σ ; Γ u v → Σ ; Γ t ≤ u where Σ ; Γ t ≤ u := (cumul Σ Γ t u).
Definition leq_term ϕ t u := eq_term_upto_univ (eq_universe ϕ) (leq_universe ϕ) t u. Σ

; Γ u : A → Σ ; Γ tApp t u : B{0 := u} | type_Cumul t A B : Σ ; Γ t : A → (isWfArity typing Σ Γ B + {s & Σ ; Γ B : tSort s}) → Σ ; Γ A ≤ B → Σ ; Γ t : B | ..

. (* remaining definitions for constants, inductive and coinductive types *)

where Σ ; Γ t : T := (typing Σ Γ t T).

Inductive cumul

(Σ : global_env_ext) (Γ : context) : term → term → Type := | cumul_refl t u : leq_term (global_ext_constraints Σ) t u → Σ ; Γ t ≤ u | cumul_red_l t u v : fst Σ ; Γ t v → Σ ; Γ v ≤ u → Σ ; Γ t ≤ u | cumul_red_r t u v : Σ ; Γ t ≤ v → fst Σ ; Γ u v → Σ ; Γ t ≤ u where Σ ; Γ t ≤ u := (cumul Σ Γ t u).
Definition leq_term ϕ t u := eq_term_upto_univ (eq_universe ϕ) (leq_universe ϕ) t u. The typing judgement is a predicate taking as parameters the global context extended with a universe declaration, a local context of assumptions and two terms corresponding to the subject and type of the typing rules. Derivations are defined in the Type sort to allow for easy inductions on the size of derivations. The typing rules are explained in detail in [44, §2] and [START_REF] Sozeau | Coq Coq Correct! Verifying Typechecking and Erasure for Coq, in Coq[END_REF][ §2.2]. The typing rules are syntax-directed, i.e. there is one rule per head constructor of term, except for the cumulativity rule which can apply anywhere in a derivation. Note that we use a standard de Bruijn encoding for local variables, along with lifting and parallel substitution operations. As can be seen from the definition of figure 1, we used a nested datatype definition (list term, list (branch term)), hence some care must be taken to define recursive definitions and user-friendly induction principles on terms and derivations, lifting a predicate on terms to lists in the appropriate way. This is done by defining first a size measure on terms and then using well-founded induction on sizes of terms and derivations to derive easy to use induction principles.

Global environments Typing extends straightforwardly to local and global contexts. We formalize in particular which invariants should hold on the definition of inductive types, including strict positivity and the invariants enjoyed by cumulative inductive types. This is one point where we depart from the pen-and-paper treatments: indeed in [START_REF] Timany | Cumulative Inductive Types In Coq[END_REF], the theory that is studied is an idealization of COQ's implementation where equality is a judgement and inductive declarations do not carry parameters. In contrast, the implementation cannot rely on typing conditions to decide the cumulativity judgement and subtyping is rather defined on two different instances of the same inductive type, e..g list@{Set} nat and list@{i} nat. We hence had to retro-engineer, from COQ's OCAML code, a proper treatment of cumulative inductive types. We'll see in section 3.5 that this was a non-trivial endeavor.

Translation from Template to PCUIC

The tApp constructor represents n-ary application of a term f to a list of arguments args. This follows rather closely COQ's implementation, where the application node takes an array of arguments, for an even more compact representation of applications. Immediate access to the head of applications is an important optimization in practice, but this representation, while memory-efficient, imposes a hidden invariant on the term representation: the term f should not itself be an application, and the list of arguments should also always be non-empty. The application typing rule is likewise complicated as we have to consider application to a spine of arguments, rather than a single argument.

In COQ's kernel, this is handled by making the term type abstract and using smart constructors to enforce these invariants. Replicating this in COQ is tedious, as we have to either:

• work everywhere with an abstract/subset type of terms, precluding the use of primitive fixpoint and case-analysis

• or work with the raw syntax and add well-formedness preconditions everywhere

Our solution is to interface with COQ using the raw Template term syntax, keeping close to the implementation. To avoid dealing with well-formedness assumptions, we define a translation from this syntax to the PCUIC term syntax where application is a binary constructor. We define similar reduction and typing judgments on the simplified syntax and show the equivalence of the two systems Template and PCUIC. This crucially relies on well-founded induction on the size of derivations to "reassociate" between binary applications and n-ary ones. The metatheory hereafter is developed on the more prooffriendly PCUIC syntax, but its theorems also apply to the original system. We simplify the PCUIC syntax further by removing the tCast constructor and translating it by an application of the identity function: this is observationally equivalent. The cast syntax in COQ is solely used to mark a place where a specific conversion algorithm should be used to convert the inferred type of a term with a specified expected type. This is used to call vm compoute or native compute to perform the cumulativity check, rather than COQ's standard "call-by-need" conversion algorithm. As we do not formalize these fast conversion checks, this is not a loss. Note also that this has no bearing on the typeability of the term, in theory. Only in practice performing conversion with the default algorithm might be infeasible.

Metatheory

Now armed with the definition of typing and reduction in PCUIC, we can start proving the usual metatheoretical results of dependent type theories. We first derive the theory of our binding structures: the usual lemmas about de Bruijn operations of lifting and substitution are proven easily.

Digression on binding

Unfortunately, at the time we started the project (circa 2017), the Autosubst framework [START_REF] Schäfer | Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions[END_REF] could not be used to automatically derive this theory for us, due to the use of nested lists. We however learned from their work [START_REF] Stark | Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions[END_REF] and developed the more expressive σ -calculus, defined from operations of renaming (for a renaming N → N) and instantiation (for a function N → term), which provide a more proof-friendly interface to reason on the de Bruijn representation. We show that COQ's kernel functions of lifting and substitution (carrying just the number of crossed binders) are simulated with specific renaming and instantiation operations. Both variants are still of interest: it would be out of the question to use the σ -calculus operations which build closures while traversing terms in COQ's implementation. However the structured nature of the σ -calculus and its amenability to automation, having a decidable equational theory [START_REF] Stark | Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions[END_REF], is a clear advantage in practice.

One example where this shines is the treatment of (dependent) let-bindings in the calculus. Dependent let-bindings are an entirely different beast than ML-like let-bindings which can be simulated with abstraction and application. In particular, three rules of reduction can apply on local definitions:

Γ let x := t in b b[t/x] ζ Γ let x := t in b let x := t in b when Γ, x := t b b cong-let-body Γ, x := t, ∆ x ↑ |∆|+1 (t) δ
Here ↑ n (t) represents the shifting of indices of the free variables of t by n, and b[t/x] the usual capture-avoiding substitution. The first rule is usual let-reduction, the second is a congruence rule allowing to reduce under a let and the last allows to expand a local definition from the context. In the course of the metatheoretical development we must prove lemmas that allow to "squeeze" or smash the let-bindings in a context. This results in a reduced context with no let-bindings anymore and a corresponding substitution that mixes the properly substituted bodies corresponding to the removed letbindings and regular variables, to apply to terms in the original context. This involves interchanging δ , Touring the MetaCoq project zeta and cong-let-body rules combined with the proper liftings and substitutions. This kind of reasoning appears in particular as soon as we want to invert an application judgment as let-bindings can appear anywhere in the type of the functional argument. Using σ -calculus reasoning and building the right abstractions tremendously helped simplify the proofs which would otherwise easily become indecipherable algebraic rewritings with the low level indices in liftings and substitutions.

Properties

Structural Properties

The usual Weakening and Substitution theorems can be proven straightforwardly by induction on the derivations. We use a beefed-up eliminator that automatically lifts the typing property we want to prove to well-formedness of the global environment, which also contains typing derivations. Likewise, we always prove properties simulataneously on well-formed local contexts and type derivations, so our theorems provide a conjunction of properties. When we moved to the σ -calculus represenation, we factorized these proofs by first stating renaming and instantiation lemmas, from which weakening and substitution follow as corrolaries. We also verify that typing is invariant by alpha-conversion, so name annotations on binders are indeed irrelevant.

Type Preservation

Proving subject reduction (a.k.a. type preservation) for dependent type theories can be rather difficult in a setting where definitional equality is typed, as it usually requires a logical relation argument/model construction, see e.g. [START_REF] Abel | Decidability of conversion for type theory in type theory[END_REF]. However, the syntactic theory is relatively well-understood for PTS: one can first independently prove context conversion/cumulativity and injectivity of Π-types (i.e. Πx : A.B ≡ Πx : A .B → A ≡ A ∧ B ≡ B ), to prove type preservation in the application case. Similarly, we have injectivity of inductive type applications, up-to the cumulativity relation on universes.

However, two other difficulties arise for PCUIC. First, we are considering a realistic type theory, will full-blown inductive family declarations, with a distinction between parameters and indices (that can contain let-bindings), and cumulative, universe polymorphic inductive types. To our knowledge, nobody ever attempted to formalize the proof at this level of detail before, even on paper. There is a good reason for that: the level of complexity is very high. Showing that the dependent case analysis reduction rule is sound mixes features such as let-bindings, the de Bruijn representation of binding adding various liftings and substitutions and the usual indigestible nesting of quantifications on indices in the typing rules of inductive types, constructors and branches. This is also ample reason to verify the code: many critical bugs a propos let-binding and inductive types were reported over the years. To tame this complexity, we tried to modularize the proof and provide the most abstract inversion lemmas on typing of inductive values and match constructs.

Second, COQ's theory is known to be broken regarding positive co-inductive types and subject reduction. We hence parameterize the proof: subject reduction holds only on judgments where no dependent case analysis is performed on co-inductive types. Negative co-inductive types implemented with primitive projections however can be show to enjoy subject reduction without restriction.

Confluence

To support inversion lemmas such as Π-type injectivity, we need to show that reduction is confluent. From this proof, it follows that the abstract, undirected conversion relation T ≡ U is equivalent to reduc-tion of the two sides to terms T and U that are in the syntactic α-cumulativity relation. We extend here Takahashi's refinement [START_REF] Takahashi | Parallel Reductions in lambda-Calculus[END_REF] of Tait/Martin-Löf's seminal proof of confluence for λ -calculus. The basic idea of the confluence proof is to consider parallel reduction instead of one-step reduction and prove the following triangle lemma:

C C Correct! Verification of Type Checking and Erasure for C , in C 8:13 traversal (see Figure 7). The fact that it is optimal is expressed by the following triangle property (for readability, we express the following two properties using commutative diagrams).

T 2.2 (T ).

For every term t and context Γ, we have Γ, t ρ(Γ), ρ(t) and for every ∆, u such that Γ, t ∆, u, the following triangle commutes

Γ, t * ∆, u * 4 ρ(Γ), ρ(t)
Parallel reduction is con uent because it is con uent in exactly one step, by using Theorem 2.2 twice.

C 2.2.1 (C P R

). Parallel reduction is con uent.

Γ, t o { # / ∆, u # . ∆ , u o { ρ(Γ), ρ(t)
Context Conversion (PCUIC: ContextConversion). One can go "out" of parallel-reduction back to the traditional transitive closure of 1-step reduction by forgetting the target contexts (PCUIC: Con uence). Due to the action at a distance nature of let-in de niens reduction, we cannot get full context conversion from the substitution lemma. We prove only after con uence that for two contexts Γ and ∆, if red 1 _ctx Γ ∆ and red 1 Γ t u then there exists a common reduct of t and u using the re exive-transitive closure of red 1 ∆.

From this, we de ne a notion of reductions of contexts and derive a con uence lemma for it: convertible contexts have a common reduct. Finally, this allows us to show that cumulativity and typing are preserved by conversion. Although we did not prove it, we believe our formalisation is generic enough to prove an additional strenghtening lemma w.r.t. cumulativity.

Subject Reduction & Principality.

Type preservation depends on a validity lemma of typing (PCUIC: Validity), and the usual inversion properties of the system (PCUIC: Inversion). Validity for this calculus is complicated by the fact that not all types have types: algebraic universes cannot be typed. This shows up in the second premise of the cumulativity rule ( gure 2). Therefore, we suppose the following properties on the metatheory.

Conjecture subject_reduction

: ∀ (Σ : global_env_ext) Γ t u T, wf Σ → Σ ; Γ t : T → red Σ Γ t u → Σ ; Γ u : T.
Note that due to subtyping, the "natural" type of t might be smaller. The general property of cumulativity we assume is:

Conjecture principal_typing {Γ u A B} : Σ ; Γ u : A → Σ ; Γ u : B → C, Σ ; Γ C ≤ A × Σ ; Γ C ≤ B × Σ ; Γ u : C.
This property together with subject reduction is essential to derive strong enough principles of reasoning on typing derivations up-to reduction (e.g., for sorts for the erasure procedure §4), or to get preservation of typing by conversions, as necessary in the veri ed conversion checker ( §3). The ρ function here is an "optimal" reduction function that reduces simultaneously all parallel redexes in a term or context. The fact that we need to consider contexts is due to let-bindings again: in one step of ρ, we might reduce a local definition to an abstraction, expand it in function position of an application and reduce the produced beta-redex. Using the triangle property twice, it is trivial to derive the diamond lemma and hence confluence for parallel reduction. By inclusion of one step reduction in parallel reduction, and parallel reduction in the transitive closure of one-step reduction (the "squashing" lemma), reduction is also confluent. This last part of reasoning is done abstractly, but accounting for the generalization to reduction in pairs of a context and a term. It then suffices to show commutation lemmas for reduction and α-cumulativity to show the equivalence of reduction up-to α-cumulativity and the undirected cumulativity relation. Confluence is crucial to show transitivity of the directed version.

Using this characterization of cumulativity, we can easily show that it is a congruence and that it enjoys expected inversion lemmas: if two Π-types are convertible, then they both reduce to Π-types that are in the α-cumulativity relation, so their domains are convertible and their codomains are in the cumulativity relation. Similarly, Π-types cannot be convertible to sorts or inductive types: there is no confusion between distinct type constructors.

Principality

As PCUIC is based on the notion of cumulativity rather than mere conversion, type uniqueness does not hold in the system. However, the refined property of principality does: for any context Γ and well-typed term t, there is a unique type T such that any other typing of t, Γ t : U we have T ≤ U. This property is essential for deciding type-checking: to check Γ t : U, it suffices to infer the principal type of t and check cumulativity. Principal typing is also used by the erasure procedure to take sound decisions based on the principal type of a given term.

Strengthening

The last expected structural property of the system is strengthening (a.k.a. thinning), which can be stated as:

Γ, x : A, ∆ t : T → x / ∈ FV(∆) ∪ FV(t) ∪ FV(T ) → Γ, ∆ t : T
This property ensures that typing is not influenced by unused variables, and is at the basis of the clear tactic of COQ, a quite essential building block in proof scripts. Unfortunately, this property cannot be proven by a simple induction on the typing derivation: the free-floating conversion rule allows to go through types mentioning the variables to clear, even if they do not appear in the term and type in the conclusion of the whole derivation.

Touring the MetaCoq project

Bidirectional Type Checking To The Rescue

This unfortunate situation can be resolved by reifying the principality property and type checking strategy as a bidirectional typing inductive definition. This variant of typing explicitly keeps track of the information flow in typing rules. In practice it separates the syntax-directed rules in a synthesis (a.k.a. inference) judgment (the term position is an input, while the type is an output) from the non-directed ones as checking rules (both positions are input). In [START_REF] Lennon-Bertrand | Complete Bidirectional Typing for the Calculus of Inductive Constructions[END_REF], Meven Lennon-Bertrand develops a bidirectional variant for PCUIC, show equivalent to the orignal PCUIC, in which strengthening and principality become trivial to derive.

The crux of these argument is that bidrectional typing derivations are "canonical" for a given term, and move uses of the conversion rule to the top of the derivation, where they are strictly necessary. In addition, multiple cumulativity rules get "compressed" into a single change-of-phase rule, relying on transitivity of cumulativity. In a bidirectional synthesis derivation, if a variable does not appear in the term position, then it cannot appear in the inferred type. Simultaneously, in a checking derivation, if a variable does not appear in the term and type, then it cannot appear in these positions in any of the subderivations.

Case In Point

This detour through bidirectional typechecking is not accidental. In [START_REF] Sozeau | Coq Coq Correct! Verifying Typechecking and Erasure for Coq, in Coq[END_REF], we only proved the soundness of a typechecking algorithm for PCUIC ( §4). It is in the course of formalizing the completeness of the type-checker ( §4) that we discovered a problem in the typing rules of COQ. The problem appears in the dependent case analysis construct match. The gist of the typing rule was to typecheck the scrutinee at some unspecified inductive type X@{ u} p i, where u is a universe instance, p the parameters and i the indices of the inductive family. The match construct also takes an elimination predicate, expected to be of type:

Π(

-----→ x : I@[ v]), X@{ v} p x → Type

Looking at this type, we would extract the universe instance v and parameters p of the inductive X assumption. The typing rule checked that the universe instance of the scrutinee u was convertible to v, rather than only in the cumulativity relation according to the subtyping rules for cumulative inductive types. It also compared the parameters p and p for convertibility, by first lifting p in a context extended with the -----→ x : I@[ v] bindings, but these two instances did not necessarily live in the same type! These mistakes lead to a loss of subject reduction, if cumulativity is used to lower the universes of the scrutinee, making the whole pattern-matching untypeable 4 . The problem appeared immediately while trying to prove completeness of type-checking, at the stage of designing the bidirectional typing rules: the flow of information was unclear and led us to the bug. We also realized that, to justify the comparison of the parameters, we would need to verify that x / ∈ FV( p ) and apply strengthening, which as we have just seen is not directly provable on undirected typing rules. This motivated us to push for a change in the term representation of match in COQ 5 that solves both problems at once, by storing at the match node the universe instance and parameters that define the eliminator, and doing a sound cumulativity test of the infered type of the scrutinee and the (reconstructed) expected type of the eliminator. We are currently finishing to update the whole METACOQ development to handle this change of representation6 .

A Type-Checker for PCUIC 4.1 Cumulativity

In [45, §3], we present a sound type-checker for PCUIC. To implement type-checking, we had to first develop a reasonably efficient reduction machine and algorithms to decide cumulativity. There are three separate algorithms at play to implement the cumulativity test.

Universes in COQ are floating variables subject to constraints [START_REF] Herbelin | Type Inference with Algebraic Universes in the Calculus of Inductive Constructions[END_REF], not directly natural numbers. To ensure consistency, one hence needs to verify that the constraints always have a valuation in the natural numbers. This boils down to deciding the (in-)equational theory of the tropical algebra (N, max, +k, ≤). We develop a longest-simple-paths algorithm to check consistency of universe constraints: the valuation of each variable can be read off as the weight of its longest simple path from the source (Type@{0}). This is a naïve model and implementation of the state-of-the-art algorithm implemented in COQ, which derives from an incremental cycle detection algorithm [START_REF] Michael | A New Approach to Incremental Cycle Detection and Related Problems[END_REF] and whose formal verification is a work-inprogress [START_REF] Guéneau | Formal Proof and Analysis of an Incremental Cycle Detection Algorithm[END_REF]. Our specification is more expressive than COQ's current implementation, as it is able to handle arbitrary +k ≤ +k constraints between universe expressions, avoiding to distinguish so-called algebraic universes and implement costly universe refreshing operations when building terms. We hope to integrate this generalization back in COQ's implementation. Using this consistency check, it is easy to define α-cumulativity by structural recursion on terms.

Reduction We implement a weak-head reduction stack machine that can efficiently find the weakhead normal form of a term. To define this function, we must assume an axiom of strong normalization, which implies that reduction is well-founded on well-typed terms. This is the only axiom used in the development.

Conversion COQ uses a smart, mostly call-by-name, conversion algorithm, that uses performancecritical heuristics to decide which constants to unfold and when. COQ's algorithm does not naïvely reduce both terms to normal form to compare them, but rather incrementally reduces them to whnfs (without δ -reduction), compare their heads and recursively calls itself. When faced with the same defined constant on both sides, it first tries to unify their arguments before resorting to unfolding, resulting in faster successes but also potentially costly backtracking.

The main difficulty in the development of the conversion algorithm is that its termination and correctness are intertwined, so it is developed as a dependently-typed program that takes well-typed terms as arguments (ensuring termination of recursive calls assuming SN) and returns a proof of their convertibility (or non-convertibility). In other words it is proven sound and complete by construction. The design of the termination measure also involves a delicate construction of a dependent lexicographic ordering on terms in a stack due to Théo Winterhalter [START_REF] Winterhalter | Formalisation and Meta-Theory of Type Theory[END_REF].

Type Checking

On top of conversion, implementing a type inference algorithm is straightforward: it is a simple structurally recursive function that takes well-formed global and local contexts and a raw term. It simply checks if the rule determined by the head of the term can apply. Figure 3 shows the type and beginning of the inference algorithm.

Touring the MetaCoq project Again, the function is strongly typed: its result lives in the typing result monad, which is an exception monad, returning (ret) a sigma-type of an inferred type A and a "squashed" proof that the term has this type or failing with type error (raise). As all our derivations are in Type by default, we use explicit squashing into Prop when writing programs manipulating terms:

The elimination rules for propositional inductives ensures that our programs cannot make computational choices based on the shape of the squashed derivations, and that extraction will remove these arguments. The extracted version of infer hence only takes a context (assumed to be well-formed) and a term and returns an error or an infered type, just like in COQ's implementation.

Using the bidirectional presentation of the system, we can simplify the correctness and completeness proof in [START_REF] Sozeau | Coq Coq Correct! Verifying Typechecking and Erasure for Coq, in Coq[END_REF] as the algorithm really follows the same structure as bidirectional derivations. Typechecking is simply defined as type inference followed by a conversion test, as usual.

Verifying Global Environments

Once the type-checker for terms is defined, we can lift it to verify global environment declarations. For constants and axioms, this is straightforward. However, declarations of inductive types are more complex and require to first define a sound context cumulativity test, a strict positivity check and to turn the universe constraints into a graph structure. This is again done using a monad EnvCheck:

Given a global environment Σ, this produces either an error or a pair of a graph and a proof that the universe graph models the constraints in Σ and a (squashed) proof that the environment is well-formed.

Erasure from PCUIC to λ -calculus

The type-checker can be extracted to OCAML and run on reasonably large programs. For example it can be used to successfully check the prelude of the HoTT library [START_REF] Bauer | The HoTT library: a formalization of homotopy type theory in Coq[END_REF], including a large proof that adjoint equivalences can be promoted to homotopy equivalences. However, our first attempt to extraction was unsuccessful: we had to change the COQ definitions so that OCAML could typecheck the generated code, as we hit a limitation of the extraction mechanism in presence of dependently-typed variadic functions. The obvious next step was hence to verify the erasure procedure itself! In [45, §4], we present a sound erasure procedure from PCUIC to untyped, call-by-value λ -calculus. This corresponds to the first part of COQ's extraction mechanism [START_REF] Letouzey | A New Extraction for Coq[END_REF], which additionally tries to maintain simple types corresponding to the original program. Erausre is performed by a single traversal of the term, expected to be well-typed. It checks if the given subterm is a type (its type is a sort Prop or Type) or if it is a proof of a proposition (its type P has sort Prop), in which case it returns a dummy term, and otherwise proceeds recursively, copying the structure of the original term. The result of erasure hence contains no type information anymore, and all propositional content is replaced with .

We can prove the following correctness statement on this procedure:

Our correctness theorem shows that if we have a well-typed term t and t erases to t , then if t reduces to a value v using weak-cbv reduction, then the erased term t also reduces to an observationally equivalent value v . The extraction pre precondition enforces that the environment is well-formed. The proof follows Letouzey's original pen-and-paper proof closely [START_REF] Letouzey | Programmation fonctionnelle certifiée: l'extraction de programmes dans l'assistant Coq[END_REF]. Since [START_REF] Sozeau | Coq Coq Correct! Verifying Typechecking and Erasure for Coq, in Coq[END_REF], we proved two additional verified passes of optimization on the erased term and environment:

• We remove from Σ the definitions that are not used for evaluation, pruning the environment from useless declarations that are no longer needed for the computation.

• We remove dummy pattern-matchings on terms, that should always trivially reduce to their single branch.

The end result of erasure is an untyped term that contains only the raw computational content of the original definition. It can be further compiled with the CERTICOQ compiler and COMPCERT to produce certified assembly code from COQ definitions.

Going further

We have presented the whole METACOQ project, which spans from the reification of COQ terms down to the erasure of well-typed terms to untyped λ -calculs. The whole project weights about 100kLoC of OCAML and COQ code, and is still under active development. We think this is a convincing example that we can move from a Trusted Code Base consisting of COQ's unverified kernel down to a Trusted Theory Base that consists of the formalized typing rules of PCUIC and its axiom of Strong Normalization.

The METACOQ (and CERTICOQ) projects are both ongoing work subject to limitations, we summarize here the current state of affairs.

Limitations

While PCUIC models a large part of COQ's implementation, it still misses a few impotant features of the theory:

• The η-conversion rule is not supported in our formalization, preventing us to check most of the standard library. Dealing with η rules in an untyped conversion setting is a notoriously hard

Figure 1 :

 1 Figure 1: Term syntax

8 : 6

 86 Ma hieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter Inductive typing (Σ : global_env_ext) (Γ : context) : term → term → Type := | type_Rel n decl :

Fig. 2 .

 2 Fig. 2. Excerpt of typing rules

Fig. 2 .

 2 Fig. 2. Excerpt of typing rules

Figure 2 :

 2 Figure 2: Type signature and notation for typing

  Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 8. Publication date: January 2020.

Figure 3 :

 3 Figure 3: Type inference function excerpt

https://github.com/coq/coq/blob/master/dev/doc/critical-bugs

https://metacoq.github.io

COQ supports an -impredicative-set flag to switch to an impredicative interpretation, but it is seldom used today

https://github.com/coq/coq/issues/13495

CEP 34 by Hugo Herbelin, Coq PR 13563 by Pierre-Marie Pédrot, integrated in Coq 8.14

https://github.com/MetaCoq/metacoq/pull/534

Bibliography

References

Touring the MetaCoq project issue. We are however hopeful that we found a solution to this problem by quotienting definitional equality with η-reduction, and hope to present this result soon.

• Similarly, we do not handle the new SProp sort of COQ. Our methodology for η-conversion should however also apply for this case.

• We do not formalize yet the guard-checking of fixpoint and co-fixpoint definitions, relying instead on oracles. Our strong normalization assumption hence includes an assumption of correctness of the guard checkers. We are currently working on integrating a definition of the guard checking algorithm and verifying its basic metatheory (invariance by renaming, substitution, etc.).

• We did not consider the module system of COQ, which is mostly orthogonal to the core typing algorithm but represents a significant share of COQ's kernel implementation, we leave this to future work.

• We leave out the so-called "template"-polymorphism feature of COQ, which is a somewhat fragile (i.e. prone to bugs), non-modular alternative to cumulative inductive types. This prevents us from checking most of the COQ standard library today as it makes intensive use of this feature. We are working with the COQ development team to move the standard library to universe polymorphism to sidestep this issue.

Conclusion and Perspectives

There are many directions in which we consider to extend the project:

• On the specification side we would like to link our typing judgment to the "Coq en Coq" formalization of Barras [START_REF] Barras | Semantical Investigations in Intuitionistic Set Theory and Type Theories with Inductive Families[END_REF], which provides the Strong Normalization proof we are assuming, for a slightly different variant of the calculus. This formalization is based on a sized-typing discipling for inductive types, which will require to show an equivalence with PCUIC's guardness checker, or an update of PCUIC to handle sized typing altogether.

• Proving that the theory is equivalent to a variant where conversion is typed, i.e. definitional equality is a judgment would also make our theory closer to categorical models of type theory, e.g., Categories with Families. This can build on recent results in this direction by Siles and Herbelin [START_REF] Siles | Pure Type System conversion is always typable[END_REF], updating them to handle cumulativity.

• In addition to the parametricity translation that we would like to prove correct, many syntactic models of type theory, extending it with side-effects [START_REF] Pédrot | An effectful way to eliminate addiction to dependence[END_REF] or forcing [START_REF] Jaber | The Definitional Side of the Forcing[END_REF] have recently been developed. METACOQ is the right setting to mechanize these results.

• We have concentrated our verification efforts on the core type-checking algorithm of COQ, but higher-level components like unification, elaboration and the proof engine would also benefit from formal treatment. We hope to tackle these components in the future.

• Finally, on the user side, we are still at the beginning of the exploration of the meta-programming features of METACOQ. It could be used to justify for example the foundations of the MTAC 2 language [START_REF] Kaiser | Mtac2: typed tactics for backward reasoning in Coq[END_REF], to turn the typed tactic language into a definitional extension of COQ's theory.