Paolo Giarrusso (Jul 28 2021 at 04:45): Paolo Giarrusso (Jul 28 2021 at 04:45):Here's a hypothetical: Suppose I might be interested in the ANSSI Coq guidelines (https://www.ssi.gouv.fr/uploads/2014/11/anssi-requirements-on-the-use-of-coq-in-the-context-of-common-criteria-evaluations-v1.0-en.pdf), yet I also wanted to use SProp; the latter is an experimental feature (https://coq.github.io/doc/master/refman/addendum/sprop.html), something that ANSSI strongly discourages:
Developers Rule 3.10. Developers shall not use features explicitly flagged as experimental in the Coq user manual
How concerned should I be? The manual implies that upper layers do not support it maturely, but what about the kernel? ANSSI does not distinguish between "experimental kernel support" and "experimental support", but potentially it should, especially given its emphasis on coqchk.
What about definitional UIP? Do we know, for instance, whether it affects consistency of other axioms? It is listed by coqchk as an axiom.
Gregory Malecha (Jul 28 2021 at 12:12):@Yves Bertot might have some insights on this
Bas Spitters (Jul 28 2021 at 12:52):SProp is part of the type theory, and hence part of the kernel, isn't it.
As it is still experimental, ANSSI seems to want to avoid it. I think for good reasons.
@Gaëtan Gilbert is the expert on SProp
Yves Bertot (Jul 28 2021 at 12:54):I believe the intention of the ANSSI is to be very conservative here. In a security evaluation process, we are not sure that the evaluators will be very competent in the Coq system, so they will take very seriously what the Coq developers describe as safe or experimental. If at some point the Coq developers want SProp to be considered as part of the robust, tested Coq ecosystem, they will need to change how this feature is documented.
On the specific point of SProp and definitional UIP, I believe the expert is @Gaëtan Gilbert. If you think that these features are essential for some formal proof to become economically viable, then we need to have discuss the question among Coq developers to see if this can be marked as safe.
Paolo Giarrusso (Jul 28 2021 at 13:06):We are using Iris extensively, and the Iris/stdpp developers (more or less the same people) are considering using to strengthen their theory https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/309, @Yves Bertot .
Ralf Jung (Jul 28 2021 at 13:11):indeed, we'd like to use SProp (but not definitional UIP) to make data structures defines via sigma types unify better (by making the proof part of the sigma type an SProp)
Ralf Jung (Jul 28 2021 at 13:11):Cc @Robbert Krebbers
Paolo Giarrusso (Jul 28 2021 at 13:28):It makes perfect sense that ANSSI delegates the safety question to Coq developers and their assessment. Both ANSSI and other users might benefit from a coqc —safe flag encoding that choice, tho of course the choice is complex. For instance, coqchk’s “Closed under the global context” is a conservative approximation today — but it does not flag uses of SProp, only of Definitional UIP.
Paolo Giarrusso (Jul 28 2021 at 13:29):(Probably time to point out that I might technically be in a conflict of interest in this discussion.)
Ralf Jung (Jul 28 2021 at 13:35):also given that SProp is available on current Coq without any flag or settings, I have to assume Iris is already using several other experimental Coq features without even realizing that they are experimental
Ralf Jung (Jul 28 2021 at 13:35):if this is a serious distinction, it should be treated more like unstable features in Rust: they should be unavailable unless one opts-in to them
Ralf Jung (Jul 28 2021 at 13:36):anyway we'll defer merging that MR until after Robbert's vacation. if we don't hear back from BedRock about this in the next 4 weeks we'll assume it's okay to merge. ;)
Gregory Malecha (Jul 28 2021 at 13:37):Thanks @Ralf Jung
Robbert Krebbers (Jul 28 2021 at 13:37):(Also what makes a feature experimental? SProp has a paper that describes its theory, but that cannot be said of the module system...)
Paolo Giarrusso (Jul 28 2021 at 13:38):That paper exists for modules! There’s >= 2 PhD theses
Paolo Giarrusso (Jul 28 2021 at 13:39):… there’s also a distinction between “experimental and affects safety” (kernel SProp support), “experimental but does not” (make vos, SProp support by tactics, …)
Ralf Jung (Jul 28 2021 at 13:40):however, making our data structures behave better wrt unification is also something that users request, so I currently still think we should land this in a few weeks -- but let's see if any new evidence comes up :)
Robbert Krebbers (Jul 28 2021 at 13:41):Which theses are that? They do not seem to be cited at https://coq.inria.fr/distrib/current/refman/language/core/modules.html
Paolo Giarrusso (Jul 28 2021 at 13:44):Good question! What I found was the work by Jacek Chrząszcz on modules (https://doi.org/10.1007/10930755_18, https://doi.org/10.1007/978-3-540-24849-1_9 and their thesis, which cites a previous one as foundation)
Paolo Giarrusso (Jul 28 2021 at 13:44): Paolo Giarrusso (Jul 28 2021 at 13:46):and Jacek Chrząszcz is acknowledged in https://coq.inria.fr/distrib/current/refman/history.html (for Coq V7) — https://coq.inria.fr/distrib/current/refman/changes.html#id759 implies that V8.0's system is an evolution not a rewrite
Paolo Giarrusso (Jul 28 2021 at 13:51):(however, I just found them, and it's not yet clear how many extensions are beyond those papers)
Robbert Krebbers (Jul 28 2021 at 13:55):It would be great if the refman could document that. That is, if it could refer to the relevant theses and papers (in this case, Jacek's thesis), and says how it compares to the current implementation.
Anyway, I think this might not be the right place for this discussion.
Théo Zimmermann (Jul 28 2021 at 13:55):Following the discussions with ANSSI about experimental features, there was a PR opened by @Maxime Dénès clarifying this info (what is experimental) in the refman: https://github.com/coq/coq/pull/10582. But it was never finished and was recently marked as stale. I think that Bedrock is part of the Coq Consortium, so @Gregory Malecha feel free to contact the consortium engineers to put this back on top of the agenda. There should probably be a discussion among Coq developers on what should be considered experimental (or unsafe) as of today, but this discussion didn't happen yet AFAICT.
Paolo Giarrusso (Jul 28 2021 at 14:05):(for the modules side discussion I filed https://github.com/coq/coq/issues/14717 so we can redirect the OT)
Ralf Jung (Jul 28 2021 at 14:07):@Théo Zimmermann I think just putting this in the refman is not enough, if the distinction is so important it needs to be put into code IMO
Ralf Jung (Jul 28 2021 at 14:08):Ralf Jung said:
also given that
SPropis available on current Coq without any flag or settings, I have to assume Iris is already using several other experimental Coq features without even realizing that they are experimental
in fact as Robbert notes we are using Ltac2, which is experimental
Paolo Giarrusso (Jul 28 2021 at 14:09):I'd rather hope that Ltac2 use should not be a concern for ANSSI — at least, it should not affect soundness if coqchk passes (?)
Gregory Malecha (Jul 28 2021 at 14:10):i think it is important to distinguish between logically (soundness) experimental and just unstable from an API point of view
Théo Zimmermann (Jul 28 2021 at 14:10):Ralf Jung said:
Théo Zimmermann I think just putting this in the refman is not enough, if the distinction is so important it needs to be put into code IMO
Actually I agree. I'm just stating the current situation.
Gregory Malecha (Jul 28 2021 at 14:11):e.g. it seems ok (but in bad taste) to use mangled names because changing the mangling algorithm will not affect soundness.
Gaëtan Gilbert (Jul 28 2021 at 14:49):sprop is not experimental over soundness issues, rather it has completeness issues both in the kernel (https://github.com/coq/coq/issues/14015) and in inference (the "bad relevance mark" problem, some tactics may do silly things like set used to (https://github.com/coq/coq/issues/14609))
definitional uip implies uip and so is inconsistent with some axioms like univalence
coq + sprop + definitional uip is approximately equiconsistent with coq - sprop + axiomatic uip and that one other axiom you need to translate to extentional type theory
(-indices-matter takes effect over definitional uip so somehow it wouldn't be a problem for hott even if we enabled it by default )
(it won't be enabled by default, because we're pretty sure it makes conversion undecidable and the way we know to implement it has known nontermination)
Hugo Herbelin (Jul 28 2021 at 21:17):(it won't be enabled by default, because we're pretty sure it makes conversion undecidable and the way we know to implement it has known nontermination)
It seems that - indices-matter would apply also to prevent the known examples of non-termination (A = B for A and B types would need a squash to be put in SProp, preventing UIP to be definitional afaiu).
Yves Bertot (Jul 29 2021 at 06:58):Thanks @Gaëtan Gilbert, this information is invaluable. We need to find a way to make this available as documentation, and a way to help users make sure that they are sitting on the right side of the fence with respect to stable and safe features.
Bas Spitters (Aug 02 2021 at 08:34):@Gaëtan Gilbert I believe your thesis is the main reference for this, isn't it?
Your paper only does sMLTT, not full pCUIC, IIRC.
I have a copy of your thesis of course, but I could not find it online. Maybe you can post a precise link to the result here, including a precise description of what has been proved about consistency, normalization, VM, native_compute, ...
Gaëtan Gilbert (Aug 02 2021 at 11:37):does anyone do full pcuic?
Paolo Giarrusso (Aug 02 2021 at 14:22):at least http://arxiv.org/abs/1710.03912 does for consistency
Gaëtan Gilbert (Aug 02 2021 at 14:28):does that count as "full"? (no inductives in Prop, eliminators instead of fixpoints, etc)
Bas Spitters (Aug 02 2021 at 14:39):We should as a community at some point.
Regarding the present discussion, we can have the same standards for SProp as for the rest of Coq, I guess.
Last updated: Oct 03 2023 at 04:02 UTC