From c0e8d5c0ea52cfb0773ce881e6029f1879b1c7cf Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 3 Oct 2019 11:04:51 +0200
Subject: 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.
---
 kernel/section.ml | 24 +++++++++---------------
 1 file changed, 9 insertions(+), 15 deletions(-)

(limited to 'kernel/section.ml')

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
-- 
cgit v1.2.3