Understanding the Coq kernel

Using Coq
1

Dear Coq community,
I would like to start a discourse on the Coq kernel/checker, as in terms of logic it is probably the primary source of reliability of the tool, one of its distinguishing features and the one piece that I can find less public information about.

Apologies for verbosity, I tried to make every first sentence of each numbered item summarize the goal of the item it refers to.
I hope people of the community will further integrate or contribute to the following questions:

  1. [Progression] Has the kernel/checker always been the same (say for a long time) or is it continuously evolving release after release?
    If the latter holds then:
    (A) How fast does the kernel evolve (compared to releases)?
    (B) Do the revisions of the kernel undergo any meta-theoretical check over changes (e.g. that the implementation continues to implement CIC - or the underlying variant of CIC, when a implementation or meta-theoretical change occurs)? To be concrete with an example, it appears from the Credits section of the Coq reference manual [1] that version 8.9 of the kernel allows mutually recursive records, what level of trust is it built to make sure this addition does not break the kernel logical consistency?

  2. [Documentation] Is there any place where information about the kernel implementation and its metatheory can be found?
    Of course one could look into the kernel [2] or checker [3] implementations themselves, but I was rather wondering if the notorious “few pages metatheory” underlying Gallina syntax was otherwise available in written form as a complement - with, e.g., the corresponding proofs of safety, normalization, substitution lemmas, etc.
    I know about Barras’ Coq in Coq [4], but that seems to be dealing only with CoC (plus I expect that the extracted kernel would not be able to deal with Gallina proof terms of today’s version of Coq).
    Someone cited Coq’Art in the past (e.g. see the thread in [5]) but I do not know how complete is the treatment of that book with respect to implementation details - I do not have access to Springer.
    Also [6] seems to be related but how close is it to the Coq kernel implementation?
    From [7]: “Gallina includes several useful features that must be considered as extensions to CIC. The important metatheorems about CIC have not been extended to the full breadth of the features that go beyond the formalized language, but most Coq users do not seem to lose much sleep over this omission”.

  3. [Diversity] Is there only one implementation of the kernel/checker or are there more (e.g. cooked up using different programming languages, or preferring slower, more reliable versions vs. faster, optimized versions for fast QED)?
    For example, in Lean there seem to be 3 officially available proof checkers [8], written in C++, Haskell and Scala (although 1 kernel for computing the terms [9]).

  4. [Implementability] What would it take for people external to the Coq development team to implement a new kernel/checker from scratch?
    Would it be just a matter of implementing CIC or would there be something more (e.g. dealing with Coq-specific constructs that are not part of CIC but are part of Gallina).
    In [6] there are some details for how to build a small kernel for Matita, but I am not too confident that the information contained there are either to the point or enough for a complete implementation (e.g. dealing with modules for one thing).
    This point is also related to that of [Documentation], above, and that of [Serializability], below.

  5. [Serializability] Can Gallina terms generated by Coq be serialized in some tool-independent format, so that external tools can manipulate them?
    A post on SerAPI recently came out [10] but I do not know whether there are any plans to make this or similar formats/APIs standard.
    Lean seems to have such a feature [11].

  6. [Minimality] Are there ways to use smaller parts of the small kernel to check the proofs generated by Coq (e.g. restricting the kernel to only deal with the CoC part, or using a subkernel with only one universe)?
    The only approximation to this that I found (in [12]) seems to allow this partially using the options -norec and -admit of the coqchk command (although I do not think it is to the point). Also compilation to .vio files seems to go in this direction but that just seems to remove opaque definitions.

    It appears from e.g. [13] that efficiency reasons lead the developers to some larger-than-needed implementation of the Coq kernel, so I guess it would it be fair to imagine that less efficient implementations could lead to smaller kernels (I think of small in terms of code complexity, rather than kLOC). I am also wondering about how small a reliable kernel can be in order to be trusted (this is closely related to the point of [Documentation] above, if reviews of the kernel by external people are expected).

  7. [Kernel vs. Checker] I am a bit confused about the separation of the Coq kernel and Coq proof checker.
    Command coqchk seems to work on object .vo files, for which “non-logical information is not checked [by coqchk]” [12]. Also, from the answer in [14] it seems that some information in lost while serializing to .vo files ("[…] there are many objects that are not serializable […]" and “[…] the checker inputs all the library information, but ignores quite a few datatypes.”)
    So the question is: Is there any loss in using (and linking) .vo files (as opposed to relying on a “whole-program” compilation)?
    And does coqchk actually use the same core code as QED does (or are these two checks performed by separate pieces of OCaml code)?

I am a non-expert with 100% trust in the Coq kernel, I am not proposing enhancements and neither am I trying to debunk Coq as a reliable system.
I just want to know more and start a discourse about the tool. I also have not read comprehensively all the works that I linked, so please apologize if I misread or misinterpreted something.

[1] https://coq.inria.fr/refman/credits.html
[2] https://github.com/coq/coq/tree/master/kernel
[3] https://github.com/coq/coq/tree/master/checker
[4] https://github.com/coq-contribs/coq-in-coq
[5] https://sympa.inria.fr/sympa/arc/coq-club/2013-05/msg00071.html
[6] A. Asperti, W. Ricciotti, C. Sacerdoti Coen, and E. Tassi. A compact kernel for the Calculus of Inductive Constructions. Sadhana, 34(1):71–144, 2009.
[7] http://adam.chlipala.net/cpdt/html/StackMachine.html
[8] https://github.com/leanprover/lean/blob/master/doc/faq.md
[9] https://github.com/leanprover/lean/tree/master/src/kernel
[10] jsCoq and SerAPI releases
[11] https://github.com/leanprover/lean/blob/master/doc/export_format.md
[12] https://coq.inria.fr/refman/practical-tools/coq-commands.html
[13] https://sympa.inria.fr/sympa/arc/coq-club/2013-09/msg00082.html
[14] https://stackoverflow.com/questions/48849091/how-is-a-vo-file-structured-so-that-coqchk-may-use-it

7 Likes
2

Very good points and summary; I cannot say a lot about it yet, but from the SerAPI point of view there are plans to provide some level of kernel access, that should help to some degree.

Also, the kernel evolves at a quite fast pace IMHO, so any description you make today of 8.10 won’t hold for key parts for 8.11.

2 Likes
3

You might be interested in the MetaCoq project, whose aim is to describe formally the Coq kernel:

The most complete description of the project and of its state is in this submitted article:

Do not hesitate to ask questions about it if you have some, I’ll try to answer.

3 Likes
4

We have been collecting papers on proof assistant checkers and kernels (and their certification as in MetaCoq) as part of our proof engineering bibliography. Below are some highlights not mentioned in preceding replies.

The best source for the general history of Coq and its kernel (up to 2004) is the foreword by Huet and Paulin-Mohring to the Coq’Art book. A recent take on the classic relative consistency proof of Coq’s foundations is that by Carneiro. See also a relevant Coq wiki page and a bibliography hosted on the wiki.

@techreport{Filliatre2000,
  author = "Jean-Christophe Filli\^atre",
  title = "Design of a proof assistant: {Coq} version 7",
  institution = "LRI, Universit\'e Paris Sud",
  type = "Research Report",
  number = 1369,
  month = oct,
  year = 2000,
  url = "http://www.lri.fr/~filliatr/ftp/publis/coqv7.ps.gz",
}

@InProceedings{Asperti2007,
author="Asperti, Andrea
and Coen, Claudio Sacerdoti
and Tassi, Enrico
and Zacchiroli, Stefano",
title="Crafting a Proof Assistant",
booktitle="Types for Proofs and Programs",
year="2007",
publisher="Springer",
pages="18--32",
isbn="978-3-540-74464-1",
doi="10.1007/978-3-540-74464-1_2",
}

@InProceedings{Harrison2006,
author="Harrison, John",
title="Towards Self-verification of {HOL Light}",
booktitle="Automated Reasoning",
year="2006",
publisher="Springer",
pages="177--191",
isbn="978-3-540-37188-5",
doi="10.1007/11814771_17",
}

@Article{Kumar2016,
author="Kumar, Ramana
and Arthan, Rob
and Myreen, Magnus O.
and Owens, Scott",
title="Self-Formalisation of Higher-Order Logic",
journal="Journal of Automated Reasoning",
year="2016",
month="Mar",
day="01",
volume="56",
number="3",
pages="221--259",
issn="1573-0670",
doi="10.1007/s10817-015-9357-x",
}

@phdthesis{Kumar2015,
  author = "Ramana Kumar",
  title = "Self-compilation and self-verification",
  year = "2015",
  school = "University of Cambridge",
  url = "https://www.cl.cam.ac.uk/~rk436/thesis.pdf",
}

@Article{Davis2015,
author="Davis, Jared
and Myreen, Magnus O.",
title="The Reflective {Milawa} Theorem Prover is Sound (Down to the Machine Code that Runs it)",
journal="Journal of Automated Reasoning",
year="2015",
volume="55",
number="2",
pages="117--183",
issn="1573-0670",
doi="10.1007/s10817-015-9324-6",
}

@techreport{Pollack1997,
  title = "How to Believe a Machine-Checked Proof",
  author = "Robert Pollack",
  year = "1997",
  month = "July",
  number = "BRICS RS-97-18",
  institution = "Department of Computer Science, University of Aarhus",
  address = "Aarhus, Denmark",
  url = "http://www.brics.dk/RS/97/18/BRICS-RS-97-18.pdf",
}

@article{Adams2016b,
  author = "Mark Adams",
  title = "Proof Auditing Formalised Mathematics",
  journal = "Journal of Formalized Reasoning",
  volume = "9",
  number = "1",
  year = "2016",
  issn = "1972-5787",
  pages = "3--32",
  doi = "10.6092/issn.1972-5787/4576",
  url = "https://jfr.unibo.it/article/view/4576"
}

@InProceedings{Adams2016,
author="Adams, Mark",
editor="Blanchette, Jasmin Christian
and Merz, Stephan",
title="{HOL Zero's} Solutions for {Pollack-Inconsistency}",
booktitle="Interactive Theorem Proving",
year="2016",
publisher="Springer International Publishing",
address="Cham",
pages="20--35",
isbn="978-3-319-43144-4",
doi="10.1007/978-3-319-43144-4_2",
}

@article{Wiedijk2012,
title = "Pollack-inconsistency",
journal = "Electronic Notes in Theoretical Computer Science",
volume = "285",
pages = "85--100",
year = "2012",
note = "",
issn = "1571-0661",
doi = "10.1016/j.entcs.2012.06.008",
url = "http://www.sciencedirect.com/science/article/pii/S157106611200028X",
author = "Freek Wiedijk",
}

@InProceedings{Werner1997,
author="Werner, Benjamin",
title="Sets in types, types in sets",
booktitle="Theoretical Aspects of Computer Software",
year="1997",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="530--546",
isbn="978-3-540-69530-1",
doi="10.1007/BFb0014566",
}

@article{Barras2010,
  author = "Bruno Barras",
  title = "Sets in {Coq}, {Coq} in Sets",
  journal = "Journal of Formalized Reasoning",
  volume = "3",
  number = "1",
  year = "2010",
  issn = "1972-5787",
  pages = "29--48",
  doi = "10.6092/issn.1972-5787/1695",
  url = "https://jfr.unibo.it/article/view/1695",
}

@InProceedings{Anand2014,
author="Anand, Abhishek and Rahli, Vincent",
title="Towards a Formally Verified Proof Assistant",
booktitle="Interactive Theorem Proving",
year="2014",
publisher="Springer International Publishing",
address="Cham",
pages="27--44",
isbn="978-3-319-08970-6",
doi="10.1007/978-3-319-08970-6_3",
}

@article{Coquand1988,
title = "The calculus of constructions",
journal = "Information and Computation",
volume = "76",
number = "2",
pages = "95--120",
year = "1988",
issn = "0890-5401",
doi = "10.1016/0890-5401(88)90005-3",
url = "http://www.sciencedirect.com/science/article/pii/0890540188900053",
author = "Thierry Coquand and G{\'e}rard Huet"
}

@InProceedings{Coquand1990,
author="Coquand, Thierry
and Paulin-Mohring, Christine",
editor="Martin-L{\"o}f, Per
and Mints, Grigori",
title="Inductively defined types",
booktitle="COLOG-88",
year="1990",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="50--66",
isbn="978-3-540-46963-6",
doi="10.1007/3-540-52335-9_47",
}

@InProceedings{PaulinMohring1993,
author="Paulin-Mohring, Christine",
editor="Bezem, Marc
and Groote, Jan Friso",
title="Inductive definitions in the system {Coq} rules and properties",
booktitle="Typed Lambda Calculi and Applications",
year="1993",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="328--345",
isbn="978-3-540-47586-6",
doi="10.1007/BFb0037116"
}

@inbook{Coquand1990b,
  author = "Thierry Coquand",
  title = "Metamathematical investigations of a calculus of constructions",
  booktitle = "Logic and Computer Science",
  publisher = "Academic Press",
  year = "1990",
  pages = "91-122",
  editor = "P. Odifreddi",
  url = "http://www.cse.chalmers.se/~coquand/meta.pdf",
}
5

Very good questions. I hope the thread continue to receive answers as obviously no single answer to this will be sufficient.

Let me try to answer what I can but a big disclaimer is that I’m not a kernel expert at all:

It evolves a lot: Recent changes — Coq 8.19+alpha documentation

  • release 8.10 introduced the new sort SProp, primitive integers and a new unfolding heuristic in termination checking. The last one is not supposed to have any effect on the logical foundations. The primitive integers are primarily there for performance: technically, they add a new logical object, but this object could be simulated in the previous version of the logic. Finally, the SProp sort is really novel from the theoretical point of view and comes with an associated paper which justifies consistency relative to the previous theory: https://dl.acm.org/citation.cfm?id=3290316
  • release 8.9 introduced mutually recursive records as you noted. In theory, this expands the logical foundations, but records can be emulated using inductive types, so in practice, it does not change the expressive power. There could still be subtle bugs due to the implementation of reduction rules that could differ between inductive types and records…
  • release 8.8 restricted what is accepted in the kernel to recover a property that was lost (subject reduction)
  • release 8.7 introduced universe cumulativity for inductive types. There is a paper about it explaining why it is supposed to be consistent: https://pdfs.semanticscholar.org/78d3/c32c9db513fcf15368fd377e688bcd84d9e4.pdf
  • release 8.6 contained a much more efficient (and much more complex) cycle detection algorithm for checking the consistency of universe constraints: this does not change anything on the foundational level but it could have introduced bugs. This algorithm has recently been formalized http://gallium.inria.fr/~agueneau/publis/gueneau-jourdan-chargueraud-pottier-2019.pdf and the formally verified version has been integrated in Dune: Use a formally verified incremental cycle detection algorithm by Armael · Pull Request #1955 · ocaml/dune · GitHub. It is probably going to be integrated in Coq too, or at least in MetaCoq.

This is all without counting the many critical bug fixes (that for the most part were related to implementation problems).

Some developers have branches adding new stuff to the kernel (such as Inductive-Inductive) and some users are really pressing the developers to merge them, but they like to take their time to be sure of that it doesn’t introduce problems. On the other hand, there are already very complex stuff in the kernel, that have been there for a long time and that threaten its consistency (see also my answer here).

The CIC chapter of the reference manual should be the canonical reference: Typing rules — Coq 8.18.0 documentation. As you mentioned, there are also a lot of papers, none of which tries to be complete with what is actually implemented (and if they were doing that, they wouldn’t last before it became outdated).

The most promising effort (but a hard one) is the MetaCoq project that was mentioned above. There was an attempt at providing an alternative checker in Rust but it hasn’t seen much progress recently: GitHub - ppedrot/kravanenn: A set of tools for Coq written in Rust

Currently there is not nearly enough documentation of the vo format for someone external to the development team to implement a new kernel from scratch I think. And it would be a huge effort.

You can disable the VM and the native compute machinery, you can turn off several options related to universe polymorphism and to primitive projections (actually most are already off by default), and you can use the Coq checker, which defunctorialize the Coq code it is fed (which can lead to performance blow up in some cases). However, there currently is no generic mechanism for doing this.

What some researchers would like to do is to build the kernel in layers and to provide transformations that allow you to use one advanced feature without relying on its implementation in the kernel, but instead compiling it down to more basic stuff (at the price of lost of performance), like what the checker does with functors.

They use mostly the same code, but with some differences in the way some stuff is handled (such as functors). The checker loads object-files and does not need to know about plugins, nor about notations, etc.

Don’t worry. At the current time, it would be unfortunately very wrong to have 100% trust in the Coq kernel. However, that doesn’t make Coq unsafe for verification challenges (in non-adversarial contexts). The efforts going on towards a formally verified checker should help lift these limitations.

4 Likes
6

Not fully though due to definitional eta. I don’t know if mutual records add anything to solo records though.

1 Like