Remove redundancy in section hypotheses of kernel entries.

We only do it for entries and not declarations because the upper layers
rely on the kernel being able to quickly tell that a definition is improperly
used inside a section. Typically, tactics can mess with the named context
and thus make the use of section definitions illegal. This cannot happen in
the kernel but we cannot remove it due to the code dependency.

Probably fixing a soundness bug reachable via ML code only. We were doing
fancy things w.r.t. computation of the transitive closure of the the variables,
in particular lack of proper sanitization of the kernel input.

11 files changed, 39 insertions, 49 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 0951b07d49..b88a2e6194 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -161,7 +161,7 @@ type 'opaque result = {
   cook_universes : universes;
   cook_relevance : Sorts.relevance;
   cook_inline : inline;
-  cook_context : Constr.named_context option;
+  cook_context : Id.Set.t option;
 }
 
 let expmod_constr_subst cache modlist subst c =
@@ -242,11 +242,7 @@ let cook_constant { from = cb; info } =
     OpaqueDef (Opaqueproof.discharge_direct_opaque info o)
   | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked")
   in
-  let const_hyps =
-    Context.Named.fold_outside (fun decl hyps ->
-      List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl')))
-		  hyps)
-      hyps0 ~init:cb.const_hyps in
+  let const_hyps = Id.Set.diff (Context.Named.to_vars cb.const_hyps) (Context.Named.to_vars hyps0) in
   let typ = abstract_constant_type (expmod cb.const_type) hyps in
   {
     cook_body = body;
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 671cdf51fe..83a8b9edfc 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -23,7 +23,7 @@ type 'opaque result = {
   cook_universes : universes;
   cook_relevance : Sorts.relevance;
   cook_inline : inline;
-  cook_context : Constr.named_context option;
+  cook_context : Names.Id.Set.t option;
 }
 
 val cook_constant : recipe -> Opaqueproof.opaque result
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 47e2f72b0e..1e6bc14935 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -61,7 +61,7 @@ type mutual_inductive_entry = {
 type definition_entry = {
   const_entry_body : constr;
   (* List of section variables *)
-  const_entry_secctx : Constr.named_context option;
+  const_entry_secctx : Id.Set.t option;
   (* State id on which the completion of type checking is reported *)
   const_entry_feedback : Stateid.t option;
   const_entry_type : types option;
@@ -70,7 +70,7 @@ type definition_entry = {
 
 type section_def_entry = {
   secdef_body : constr;
-  secdef_secctx : Constr.named_context option;
+  secdef_secctx : Id.Set.t option;
   secdef_feedback : Stateid.t option;
   secdef_type : types option;
 }
@@ -78,7 +78,7 @@ type section_def_entry = {
 type 'a opaque_entry = {
   opaque_entry_body   : 'a;
   (* List of section variables *)
-  opaque_entry_secctx : Constr.named_context;
+  opaque_entry_secctx : Id.Set.t;
   (* State id on which the completion of type checking is reported *)
   opaque_entry_feedback : Stateid.t option;
   opaque_entry_type        : types;
@@ -88,7 +88,7 @@ type 'a opaque_entry = {
 type inline = int option (* inlining level, None for no inlining *)
 
 type parameter_entry = 
-    Constr.named_context option * types in_universes_entry * inline
+    Id.Set.t option * types in_universes_entry * inline
 
 type primitive_entry = {
   prim_entry_type : types option;
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 4268f0a602..1069d9a62c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -733,7 +733,7 @@ let constant_entry_of_side_effect eff =
   if Declareops.is_opaque cb then
   OpaqueEff {
     opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
-    opaque_entry_secctx = cb.const_hyps;
+    opaque_entry_secctx = Context.Named.to_vars cb.const_hyps;
     opaque_entry_feedback = None;
     opaque_entry_type = cb.const_type;
     opaque_entry_universes = univs;
@@ -741,7 +741,7 @@ let constant_entry_of_side_effect eff =
   else
   DefinitionEff {
     const_entry_body = p;
-    const_entry_secctx = Some cb.const_hyps;
+    const_entry_secctx = Some (Context.Named.to_vars cb.const_hyps);
     const_entry_feedback = None;
     const_entry_type = Some cb.const_type;
     const_entry_universes = univs;
diff --git a/kernel/section.ml b/kernel/section.ml
index 4a9b222798..babd9fe7a1 100644
--- a/kernel/section.ml
+++ b/kernel/section.ml
@@ -146,19 +146,11 @@ let empty_segment = {
   abstr_uctx = AUContext.empty;
 }
 
-let extract_hyps sec vars hyps =
-  (* FIXME: this code is fishy. It is supposed to check that declared section
-     variables are an ordered subset of the ambient ones, but it doesn't check
-     e.g. uniqueness of naming nor convertibility of the section data. *)
-  let rec aux ids hyps = match ids, hyps with
-  | id :: ids, decl :: hyps when Names.Id.equal id (NamedDecl.get_id decl) ->
-    decl :: aux ids hyps
-  | _ :: ids, hyps ->
-    aux ids hyps
-  | [], _ -> []
-  in
-  let ids = List.map NamedDecl.get_id @@ List.firstn sec.sec_context vars in
-  aux ids hyps
+let extract_hyps sec vars used =
+  (* Keep the section-local segment of variables *)
+  let vars = List.firstn sec.sec_context vars in
+  (* Only keep the part that is used by the declaration *)
+  List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) used) vars
 
 let section_segment_of_entry vars e hyps sections =
   (* [vars] are the named hypotheses, [hyps] the subset that is declared by the
@@ -180,12 +172,14 @@ let section_segment_of_entry vars e hyps sections =
 let segment_of_constant env con s =
   let body = Environ.lookup_constant con env in
   let vars = Environ.named_context env in
-  section_segment_of_entry vars (SecDefinition con) body.Declarations.const_hyps s
+  let used = Context.Named.to_vars body.Declarations.const_hyps in
+  section_segment_of_entry vars (SecDefinition con) used s
 
 let segment_of_inductive env mind s =
   let mib = Environ.lookup_mind mind env in
   let vars = Environ.named_context env in
-  section_segment_of_entry vars (SecInductive mind) mib.Declarations.mind_hyps s
+  let used = Context.Named.to_vars mib.Declarations.mind_hyps in
+  section_segment_of_entry vars (SecInductive mind) used s
 
 let instance_from_variable_context =
   List.rev %> List.filter NamedDecl.is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index b65e62ba30..f70b2960cf 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -221,9 +221,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
 let build_constant_declaration env result =
   let open Cooking in
   let typ = result.cook_type in
-  let check declared inferred =
-    let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in
-    let inferred_set, declared_set = mk_set inferred, mk_set declared in
+  let check declared_set inferred_set =
     if not (Id.Set.subset inferred_set declared_set) then
       let l = Id.Set.elements (Id.Set.diff inferred_set declared_set) in
       let n = List.length l in
@@ -239,11 +237,6 @@ let build_constant_declaration env result =
          str "Proof using " ++ declared_vars ++ fnl () ++
          str "to" ++ fnl () ++
          str "Proof using " ++ inferred_vars) in
-  let sort l =
-    List.filter (fun decl ->
-      let id = NamedDecl.get_id decl in
-      List.exists (NamedDecl.get_id %> Names.Id.equal id) l)
-    (named_context env) in
   (* We try to postpone the computation of used section variables *)
   let hyps, def =
     let context_ids = List.map NamedDecl.get_id (named_context env) in
@@ -252,7 +245,7 @@ let build_constant_declaration env result =
     | None ->
       if List.is_empty context_ids then
         (* Empty section context: no need to check *)
-        [], def
+        Id.Set.empty, def
       else
         (* No declared section vars, and non-empty section context:
            we must look at the body NOW, if any *)
@@ -264,16 +257,19 @@ let build_constant_declaration env result =
           (* Opaque definitions always come with their section variables *)
           assert false
         in
-        keep_hyps env (Id.Set.union ids_typ ids_def), def
+        Environ.really_needed env (Id.Set.union ids_typ ids_def), def
     | Some declared ->
+      let needed = Environ.really_needed env declared in
+      (* Transitive closure ensured by the upper layers *)
+      let () = assert (Id.Set.equal needed declared) in
         (* We use the declared set and chain a check of correctness *)
-        sort declared,
+        declared,
         match def with
         | Undef _ | Primitive _ as x -> x (* nothing to check *)
         | Def cs as x ->
             let ids_typ = global_vars_set env typ in
             let ids_def = global_vars_set env (Mod_subst.force_constr cs) in
-            let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in
+            let inferred = Environ.really_needed env (Id.Set.union ids_typ ids_def) in
             check declared inferred;
             x
         | OpaqueDef lc -> (* In this case we can postpone the check *)
@@ -281,12 +277,13 @@ let build_constant_declaration env result =
           let kont c =
             let ids_typ = global_vars_set env typ in
             let ids_def = global_vars_set env c in
-            let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in
+            let inferred = Environ.really_needed env (Id.Set.union ids_typ ids_def) in
             check declared inferred
           in
           OpaqueDef (iter kont lc)
   in
   let univs = result.cook_universes in
+  let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in
   let tps = 
     let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in
     Option.map Cemitcodes.from_val res
@@ -317,7 +314,10 @@ let translate_recipe env _kn r =
   let univs = result.cook_universes in
   let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs result.cook_body in
   let tps = Option.map Cemitcodes.from_val res in
-  { const_hyps = Option.get result.cook_context;
+  let hyps = Option.get result.cook_context in
+  (* Trust the set of section hypotheses generated by Cooking *)
+  let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in
+  { const_hyps = hyps;
     const_body = result.cook_body;
     const_type = result.cook_type;
     const_body_code = tps;
diff --git a/tactics/declare.ml b/tactics/declare.ml
index e418240d3a..b6a0d9f39a 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -72,7 +72,7 @@ type constant_obj = {
 type 'a proof_entry = {
   proof_entry_body   : 'a Entries.const_entry_body;
   (* List of section variables *)
-  proof_entry_secctx : Constr.named_context option;
+  proof_entry_secctx : Id.Set.t option;
   (* State id on which the completion of type checking is reported *)
   proof_entry_feedback : Stateid.t option;
   proof_entry_type        : Constr.types option;
@@ -228,7 +228,7 @@ let cast_opaque_proof_entry e =
         ids_typ, vars
     in
     let () = if Aux_file.recording () then record_aux env hyp_typ hyp_def in
-    keep_hyps env (Id.Set.union hyp_typ hyp_def)
+    Environ.really_needed env (Id.Set.union hyp_typ hyp_def)
   | Some hyps -> hyps
   in
   {
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 4cb876cecb..da66a2713c 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -23,7 +23,7 @@ open Entries
 type 'a proof_entry = {
   proof_entry_body   : 'a Entries.const_entry_body;
   (* List of section variables *)
-  proof_entry_secctx : Constr.named_context option;
+  proof_entry_secctx : Id.Set.t option;
   (* State id on which the completion of type checking is reported *)
   proof_entry_feedback : Stateid.t option;
   proof_entry_type        : Constr.types option;
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index a2929e45cd..b723922642 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -36,7 +36,7 @@ type opacity_flag = Opaque | Transparent
 
 type t =
   { endline_tactic : Genarg.glob_generic_argument option
-  ; section_vars : Constr.named_context option
+  ; section_vars : Id.Set.t option
   ; proof : Proof.t
   ; udecl: UState.universe_decl
   (** Initial universe declarations *)
@@ -128,7 +128,7 @@ let set_used_variables ps l =
   if not (Option.is_empty ps.section_vars) then
     CErrors.user_err Pp.(str "Used section variables can be declared only once");
   (* EJGA: This is always empty thus we should modify the type *)
-  (ctx, []), { ps with section_vars = Some ctx}
+  (ctx, []), { ps with section_vars = Some (Context.Named.to_vars ctx) }
 
 let get_open_goals ps =
   let Proof.{ goals; stack; shelf } = Proof.data ps.proof in
diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli
index d15e23c2cc..b9d1b37a11 100644
--- a/tactics/proof_global.mli
+++ b/tactics/proof_global.mli
@@ -17,7 +17,7 @@ type t
 (* Should be moved into a proper view *)
 val get_proof : t -> Proof.t
 val get_proof_name : t -> Names.Id.t
-val get_used_variables : t -> Constr.named_context option
+val get_used_variables : t -> Names.Id.Set.t option
 
 (** Get the universe declaration associated to the current proof. *)
 val get_universe_decl : t -> UState.universe_decl
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 42d1a1f3fc..c7a588d2b4 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -359,7 +359,7 @@ let save_lemma_admitted ~(lemma : t) : unit =
         let env = Global.env () in
         let ids_typ = Environ.global_vars_set env typ in
         let ids_def = Environ.global_vars_set env pproof in
-        Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
+        Some (Environ.really_needed env (Id.Set.union ids_typ ids_def))
       | _ -> None in
   let universes = Proof_global.get_initial_euctx lemma.proof in
   let ctx = UState.check_univ_decl ~poly universes udecl in