Merge PR #18630: coqchk: check const_relevance

Reviewed-by: ppedrot
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

checker/checker.ml

@@ -309,6 +309,9 @@ let explain_exn = function
   | CheckInductive.InductiveMismatch (mind,field) ->
     hov 0 (MutInd.print mind ++ str ": field " ++ str field ++ str " is incorrect.")
 
+  | Mod_checking.BadConstant (cst, why) ->
+    hov 0 (Constant.print cst ++ spc() ++ why)
+
   | Assert_failure (s,b,e) ->
       hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
                (if s = "" then mt ()

checker/mod_checking.ml

@@ -31,6 +31,8 @@ let register_opacified_constant env opac kn cb =
   in
   Cmap.add kn wo_body opac
 
+exception BadConstant of Constant.t * Pp.t
+
 let check_constant_declaration env opac kn cb opacify =
   Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ Constant.print kn);
   let env = CheckFlags.set_local_flags cb.const_typing_flags env in
@@ -47,7 +49,9 @@ let check_constant_declaration env opac kn cb opacify =
       true, env
   in
   let ty = cb.const_type in
-  let _ = infer_type env ty in
+  let jty = infer_type env ty in
+  if not (Sorts.relevance_equal cb.const_relevance (Sorts.relevance_of_sort jty.utj_type))
+  then raise Pp.(BadConstant (kn, str "incorrect const_relevance"));
   let body, env = match cb.const_body with
     | Undef _ | Primitive _ -> None, env
     | Def c -> Some c, env

checker/mod_checking.mli

@@ -11,3 +11,5 @@
 val set_indirect_accessor : (Opaqueproof.opaque -> Constr.t * unit Opaqueproof.delayed_universes) -> unit
 
 val check_module : Environ.env -> Names.Cset.t Names.Cmap.t -> Names.ModPath.t -> Declarations.module_body -> Names.Cset.t Names.Cmap.t
+
+exception BadConstant of Names.Constant.t * Pp.t

dev/doc/critical-bugs.md

@@ -21,6 +21,7 @@ This file recollects knowledge about critical bugs found in Coq since version 8.
       - [de Bruijn indice bug in checking guard of nested cofixpoints](#de-bruijn-indice-bug-in-checking-guard-of-nested-cofixpoints)
       - [de Bruijn indice bug in computing allowed elimination principle](#de-bruijn-indice-bug-in-computing-allowed-elimination-principle)
       - [bug in Prop<=Set conversion which made Set identifiable with Prop, preventing a proof-irrelevant interpretation of Prop](#bug-in-propset-conversion-which-made-set-identifiable-with-prop-preventing-a-proof-irrelevant-interpretation-of-prop)
+      - [incorrect abstraction of sort variables in relevance marks on opaque constants](#incorrect-abstraction-of-sort-variables-in-relevance-marks-on-opaque-constants)
     - [Module system](#module-system)
       - [missing universe constraints in typing "with" clause of a module type](#missing-universe-constraints-in-typing-with-clause-of-a-module-type)
       - [universe constraints for module subtyping not stored in vo files](#universe-constraints-for-module-subtyping-not-stored-in-vo-files)
@@ -216,6 +217,19 @@ This file recollects knowledge about critical bugs found in Coq since version 8.
 - GH issue number: none?
 - risk: ?
 
+#### incorrect abstraction of sort variables in relevance marks on opaque constants
+
+and lack of checking of relevance marks on constants in coqchk
+
+- component: sort polymorphism / proof irrelevance
+- introduced: V8.10 for the coqchk bug, V8.19 for the coqc bug
+- impacted released versions: V8.19.0
+- impacted coqchk: versions: V8.10-V8.19.0
+- fixed in: V8.19.1, V8.20
+- found by: Gaëtan Gilbert
+- exploit / GH issue: [#18629](https://github.com/coq/coq/issues/18629)
+- risk: low (requires specific plugin code unlikely to be found in non malicious plugin)
+
 ### Module system
 
 #### missing universe constraints in typing "with" clause of a module type