The Coq mailing list

[Yannick Forster <yannick AT yforster.de>]

I'll try to give my view on the situation as a contributor to MetaCoq 
and co-author of Coq Coq Correct!, but others may want to chime in with 
a more detailed or different perspective.

>  > That seems unlikely, since the CIC is not strongly normalizing:
>
> The paper says <https://dl.acm.org/doi/epdf/10.1145/3371076>:
>
>     In practice, our formalisation assumes strong normalisation of the
>     reduction of CIC; and this even serves as the basis for the
>     implementation of algorithmic conversion, which is defined by
>     recursion on the strong normalisation assumption. We also assume
>     other properties of the metatheory3: subject reduction, validity,
>     strengthening, guard condition for inductive types and fixpoints and
>     proof-irrelevance. This is the only Achilles heel of our
>     formalisation, the correctness of the specification of the
>     metatheory: If the metatheory fulfills the well-known, assumed
>     properties, then there is no error in the implementation.
>
>
> Maybe we can get one of the authors to comment?

Indeed, the CIC *as currently implemented by the Coq kernel* is not 
strongly normalising. I think it is important to distinguish between the 
theory and its implementation here:

The CIC itself exists in various variants, usually without a detailed 
specification which fixpoints exactly are allowed. The Coq kernel 
implements one variant, where certain fixpoints are allowed, including 
the one mentioned by Cody which leads to a valid 
non-strongly-normalising term.

My stance here would be that the Coq kernel should better implement a 
variant of CIC which is strongly normalising, not the one it is 
currently implementing. There are reasons why the situation is at is is 
right now. One of these reasons is that specifications of Coq's guard 
condition are not very accessible, possibly even non-existent. It will 
require further discussion whether MetaCoq should weaken the assumptions 
or whether Coq should change the guard condition to implement a strongly 
normalising theory.

Compared to the sentence quoted by Jason, the Coq Coq Correct! / MetaCoq 
project has advanced and only relies on a strongly normalising 
meta-theory (subject reduction and validity are proved, the need for 
proof irrelevance was eliminated). Importantly, the proofs quantify over 
a strongly normalising guard condition, without specifying or 
implementing one.

That is, every strongly normalising variant of CIC is captured by 
MetaCoq. For all of the captured variants, the Coq Coq Correct project 
provides a verified type checker, which consequently only relies on the 
mentioned assumptions of the meta-theory.

> Does the Coq Coq Correct! project address the issues pertinent to this
> unsoundness bug? Last I checked they axiomatized the part that would
> have interacted with this guardedness condition:
> 
https://metacoq.github.io/metacoq/html/MetaCoq.PCUIC.PCUICTyping.html#ind_guard 

> 
<https://metacoq.github.io/metacoq/html/MetaCoq.PCUIC.PCUICTyping.html#ind_guard> 

> . This (and other "advanced" inductive extensions) is the part I find
> most dubious about Coq generally, so I really hope they get around to it
> at some point.

In the end, two approaches how MetaCoq can be used to tackle the problem 
seem reasonable to me:

1) Use the specification of CIC + a tbd specification of the guardedness 
checker for a (set-theoretic?) machine-checked consistency proof.

2) Show that CIC + a tbd specification of the guardedness checker can be 
reduced to CIC + a simpler tbd specification of the guardedness checker. 
For instance, one could hope that one can give a translation from CIC + 
complicated guard checker to CIC + very simple guard checker, e.g. only 
accepting recursors. Probably, that's way too optimistic, but there 
certainly is hope that MetaCoq will be able to serve as foundation for a 
very interesting future research project on the guard condition. But, 
unfortunately, we haven't got around to it yet :)

Best
Yannick



On 29/12/2021 22:32, Jason Gross wrote:
>  > That seems unlikely, since the CIC is not strongly normalizing:
>
> The paper says <https://dl.acm.org/doi/epdf/10.1145/3371076>:
>
>     In practice, our formalisation assumes strong normalisation of the
>     reduction of CIC; and this even serves as the basis for the
>     implementation of algorithmic conversion, which is defined by
>     recursion on the strong normalisation assumption. We also assume
>     other properties of the metatheory3: subject reduction, validity,
>     strengthening, guard condition for inductive types and fixpoints and
>     proof-irrelevance. This is the only Achilles heel of our
>     formalisation, the correctness of the specification of the
>     metatheory: If the metatheory fulfills the well-known, assumed
>     properties, then there is no error in the implementation.
>
>
> Maybe we can get one of the authors to comment?
>
> Best,
> Jason
>
>
> On Wed, Dec 29, 2021 at 1:24 PM roux cody <cody.roux AT gmail.com 
> <mailto:cody.roux AT gmail.com>> wrote:
>
>
>
>     On Tue, Dec 28, 2021 at 9:59 PM Jason Gross <jasongross9 AT gmail.com
>     <mailto:jasongross9 AT gmail.com>> wrote:
>
>          > Would a hypothetical proof of consistency of the entire Coq
>         kernel as it currently exists be possible in principle
>
>         You may be interested in the Coq Coq Correct! project
>         <https://metacoq.github.io/coqcoqcorrect>, which re-implements a
>         significant fraction of Coq's kernel in Gallina (I think
>         everything except the .vo format, module types / functors,
>         universe polymorphism, and the VM and native reduction machines,
>         but don't quote me on this) and proves it correct relative to an
>         axiom stating strong normalization of CIC.
>
>
>
>     That seems unlikely, since the CIC is not strongly normalizing:
>
>     Fixpoint foo (n : nat) :=
>        let g := foo n in
>        0.
>
>     Eval compute in foo 2. (* stack overflow *)
>
>
>         Best,
>         Jason
>
>
>         On Tue, Dec 28, 2021 at 6:44 PM Abhishek Anand <aa755 AT pm.me
>         <mailto:aa755 AT pm.me>> wrote:
>
>
> >             I have a small side question regarding the wiki article.
> >             It contains a sentence:
> >
> >             > As a result, not all the legitimate functions that
> >             satisfy the current (unsound) guardedness checker will
> >             satisfy the new sized type based typechecker.
> >             My impression was that all the actual soundness holes in
> >             the guardedness checker were patched, so what unsoundness
> >             remains in the checker in recent versions of Coq? Would a
> >             hypothetical proof of consistency of the entire Coq kernel
> >             as it currently exists be possible in principle, or do we
> >             know that this is false without avoiding certain areas?
>
>             Yes, as far as I know, the guardedness checker was patched.
>             I fixed the article:
>             
> https://github.com/coq/coq/wiki/CoqTerminationDiscussion/_compare/8f9576e00875b77614eae47dbd5cbbbc86c7adfd...fd05a250486919dc8035174017acf65667f66967
>             
> <https://github.com/coq/coq/wiki/CoqTerminationDiscussion/_compare/8f9576e00875b77614eae47dbd5cbbbc86c7adfd...fd05a250486919dc8035174017acf65667f66967>
>
> >             Mario Carneiro
> >
> >             On Tue, Dec 28, 2021 at 3:34 PM public <aa755 AT pm.me
> >             <mailto:aa755 AT pm.me>> wrote:
> >
> >                 I wrote a wiki article about the last such incident I
> >                 remember.
> >                 https://github.com/coq/coq/wiki/CoqTerminationDiscussion
> >                 <https://github.com/coq/coq/wiki/CoqTerminationDiscussion>
> >                 (others have since contributed to the article)
> >
> >                 Regards,
> >                 Abhishek Anand
> >
> >
> >                 ‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐
> >
> >                 On Tuesday, December 28th, 2021 at 3:19 PM, Marco
> >                 Servetto <marco.servetto AT gmail.com
> >                 <mailto:marco.servetto AT gmail.com>> wrote:
> >
> >                 > Hi,
> >                 >
> >                 > I'm writing a little document talking about
> >                 soundness/unsoundesses in
> >                 >
> >                 > verification systems.
> >                 >
> >                 > I remember that there was a time we managed to prove
> >                 False in Coq, and
> >                 >
> >                 > the community came together effectively and promptly
> >                 to fix it, and
> >                 >
> >                 > all major proofs were unaffected by the fix. I also
> >                 remember members
> >                 >
> >                 > from other communities (Agda?) coming to give a hand.
> >                 >
> >                 > While I'm not a Coq genius, seeing the honesty and
> >                 the clear polite
> >                 >
> >                 > and direct action made by this community filled me
> >                 up with hope for
> >                 >
> >                 > the
> >                 >
> >                 > future.
> >                 >
> >                 > Do I remember correctly? Can someone help me to
> >                 summarise the event
> >                 >
> >                 > and provide some references? Do you have references
> >                 to other important
> >                 >
> >                 > tools that have been proved unsound and any
> >                 discussions about the
> >                 >
> >                 > response of their community?
> >                 >
> >                 > Marco.