Revised infrastructure for lazy loading of opaque proofs

 Get rid of the LightenLibrary hack : no more last-minute
 collect of opaque terms and Obj.magic tricks. Instead, we
 make coqc accumulate the opaque terms as soon as constant_bodies
 are created outside sections. In these cases, the opaque
 terms are placed in a special table, and some (DirPath.t * int)
 are used as indexes in constant_body. In an interactive session,
 the local opaque terms stay directly stored in the constant_body.

 The structure of .vo file stays similar : magic number, regular
 library structure, digest of the first part, array of opaque terms.
 In addition, we now have a final checksum for checking the
 integrity of the whole .vo file. The other difference is that
 lazy_constr aren't changed into int indexes in .vo files, but are
 now coded as (substitution list * DirPath.t * int). In particular
 this approach allows to refer to opaque terms from another
 library. This (and accumulating substitutions in lazy_constr)
 seems to greatly help decreasing the size of opaque tables :
 -20% of vo size on the standard library :-). The compilation times
 are slightly better, but that can be statistic noise.

 The -force-load-proofs isn't active anymore : it behaves now
 just like -lazy-load-proofs. The -dont-load-proofs mode has
 slightly changed : opaque terms aren't seen as axioms anymore,
 but accessing their bodies will raise an error.

 Btw, API change : Declareops.body_of_constant now produces directly
 a constr option instead of a constr_substituted option

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16382 85f007b7-540e-0410-9357-904b9bb8a0f7

checker/check.ml

@@ -40,7 +40,7 @@ type compilation_unit_name = DirPath.t
 
 type library_disk = {
   md_name : compilation_unit_name;
-  md_compiled : Safe_typing.LightenLibrary.lightened_compiled_library;
+  md_compiled : Safe_typing.compiled_library;
   md_objects : library_objects;
   md_deps : (compilation_unit_name * Digest.t) array;
   md_imports : compilation_unit_name array }
@@ -56,6 +56,7 @@ type library_t = {
   library_name : compilation_unit_name;
   library_filename : CUnix.physical_path;
   library_compiled : Safe_typing.compiled_library;
+  library_opaques : Term.constr array;
   library_deps : (compilation_unit_name * Digest.t) array;
   library_digest : Digest.t }
 
@@ -91,6 +92,19 @@ let library_full_filename dir = (find_library dir).library_filename
 let register_loaded_library m =
   libraries_table := LibraryMap.add m.library_name m !libraries_table
 
+(* Map from library names to table of opaque terms *)
+let opaque_tables = ref LibraryMap.empty
+
+let access_opaque_table dp i =
+  let t =
+    try LibraryMap.find dp !opaque_tables
+    with Not_found -> assert false
+  in
+  assert (i < Array.length t);
+  t.(i)
+
+let _ = Declarations.indirect_opaque_access := access_opaque_table
+
 let check_one_lib admit (dir,m) =
   let file = m.library_filename in
   let md = m.library_compiled in
@@ -105,7 +119,7 @@ let check_one_lib admit (dir,m) =
   else
     (Flags.if_verbose ppnl
       (str "Checking library: " ++ pr_dirpath dir);
-      Safe_typing.import file md dig);
+      Safe_typing.import file md m.library_opaques dig);
   Flags.if_verbose pp (fnl());
   pp_flush ();
   register_loaded_library m
@@ -280,7 +294,8 @@ let with_magic_number_check f a =
 let mk_library md f table digest = {
   library_name = md.md_name;
   library_filename = f;
-  library_compiled = Safe_typing.LightenLibrary.load table md.md_compiled;
+  library_compiled = md.md_compiled;
+  library_opaques = table;
   library_deps = md.md_deps;
   library_digest = digest }
 
@@ -298,16 +313,24 @@ let intern_from_file (dir, f) =
     try
       let ch = with_magic_number_check raw_intern_library f in
       let (md:library_disk) = System.marshal_in f ch in
-      let digest = System.marshal_in f ch in
-      let table = (System.marshal_in f ch : Safe_typing.LightenLibrary.table) in
-      close_in ch;
+      let (digest:Digest.t) = System.marshal_in f ch in
+      let (table:Term.constr array) = System.marshal_in f ch in
+      (* Verification of the final checksum *)
+      let pos = pos_in ch in
+      let (checksum:Digest.t) = System.marshal_in f ch in
+      let () = close_in ch in
+      let ch = open_in f in
+      if not (String.equal (Digest.channel ch pos) checksum) then
+        errorlabstrm "intern_from_file" (str "Checksum mismatch");
+      let () = close_in ch in
       if dir <> md.md_name then
-        errorlabstrm "load_physical_library"
+        errorlabstrm "intern_from_file"
           (name_clash_message dir md.md_name f);
       Flags.if_verbose ppnl (str" done]");
       md,table,digest
     with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in
   depgraph := LibraryMap.add md.md_name md.md_deps !depgraph;
+  opaque_tables := LibraryMap.add md.md_name table !opaque_tables;
   mk_library md f table digest
 
 let get_deps (dir, f) =

checker/declarations.ml

@@ -480,24 +480,34 @@ let subst_substituted s r =
 
 let force_constr = force subst_mps
 
+let from_val c = ref (LSval c)
+
 type constr_substituted = constr substituted
 
 let val_cstr_subst = val_substituted val_constr
 
 let subst_constr_subst = subst_substituted
 
-(** Beware! In .vo files, lazy_constr are stored as integers
-   used as indexes for a separate table. The actual lazy_constr is restored
-   later, by [Safe_typing.LightenLibrary.load]. This allows us
-   to use here a different definition of lazy_constr than coqtop:
-   since the checker will inspect all proofs parts, even opaque
-   ones, no need to use Lazy.t here *)
+(* Nota : in coqtop, the [lazy_constr] type also have a [Direct]
+   constructor, but it shouldn't occur inside a .vo, so we ignore it *)
+
+type lazy_constr =
+  | Indirect of substitution list * DirPath.t * int
+(* | Direct of constr_substituted *)
+
+let subst_lazy_constr sub = function
+  | Indirect (l,dp,i) -> Indirect (sub::l,dp,i)
+
+let indirect_opaque_access =
+  ref ((fun dp i -> assert false) : DirPath.t -> int -> constr)
+
+let force_lazy_constr = function
+  | Indirect (l,dp,i) ->
+    let c = !indirect_opaque_access dp i in
+    force_constr (List.fold_right subst_constr_subst l (from_val c))
 
-type lazy_constr = constr_substituted
-let subst_lazy_constr = subst_substituted
-let force_lazy_constr = force_constr
-let lazy_constr_from_val c = c
-let val_lazy_constr = val_cstr_subst
+let val_lazy_constr =
+  val_sum "lazy_constr" 0 [|[|val_list val_subst;val_dp;val_int|]|]
 
 (** Inlining level of parameters at functor applications.
     This is ignored by the checker. *)
@@ -532,8 +542,8 @@ type constant_body = {
 
 let body_of_constant cb = match cb.const_body with
   | Undef _ -> None
-  | Def c -> Some c
-  | OpaqueDef c -> Some c
+  | Def c -> Some (force_constr c)
+  | OpaqueDef c -> Some (force_lazy_constr c)
 
 let constant_has_body cb = match cb.const_body with
   | Undef _ -> false

checker/declarations.mli

@@ -30,16 +30,9 @@ type constr_substituted
 val force_constr : constr_substituted -> constr
 val from_val : constr -> constr_substituted
 
-(** Beware! In .vo files, lazy_constr are stored as integers
-   used as indexes for a separate table. The actual lazy_constr is restored
-   later, by [Safe_typing.LightenLibrary.load]. This allows us
-   to use here a different definition of lazy_constr than coqtop:
-   since the checker will inspect all proofs parts, even opaque
-   ones, no need to use Lazy.t here *)
-
 type lazy_constr
-val force_lazy_constr : lazy_constr -> constr
-val lazy_constr_from_val : constr_substituted -> lazy_constr
+
+val indirect_opaque_access : (DirPath.t -> int -> constr) ref
 
 (** Inlining level of parameters at functor applications.
     This is ignored by the checker. *)
@@ -63,7 +56,7 @@ type constant_body = {
     const_native_name : native_name ref;
     const_inline_code : bool }
 
-val body_of_constant : constant_body -> constr_substituted option
+val body_of_constant : constant_body -> constr option
 val constant_has_body : constant_body -> bool
 val is_opaque : constant_body -> bool
 

checker/mod_checking.ml

@@ -35,7 +35,7 @@ let check_constant_declaration env kn cb =
         let _ = infer_type envty ty in
         (match body_of_constant cb with
           | Some bd ->
-              let j = infer env' (force_constr bd) in
+              let j = infer env' bd in
               conv_leq envty j ty
           | None -> ())
     | PolymorphicArity(ctxt,par) ->

checker/safe_typing.ml

@@ -59,117 +59,19 @@ let check_imports f caller env needed =
   in
   Array.iter check needed
 
+type nativecode_symb_array
 
 type compiled_library =
     DirPath.t *
     module_body *
     (DirPath.t * Digest.t) array *
-    engagement option
-
- (* Store the body of modules' opaque constants inside a table.  
-
-    This module is used during the serialization and deserialization
-    of vo files. 
-
-    By adding an indirection to the opaque constant definitions, we
-    gain the ability not to load them. As these constant definitions
-    are usually big terms, we save a deserialization time as well as
-    some memory space. *)
-module LightenLibrary : sig
-  type table 
-  type lightened_compiled_library 
-  val load : table -> lightened_compiled_library -> compiled_library
-end = struct
-
-  (* The table is implemented as an array of [constr_substituted].
-     Keys are hence integers. To avoid changing the [compiled_library]
-     type, we brutally encode integers into [lazy_constr]. This isn't
-     pretty, but shouldn't be dangerous since the produced structure
-     [lightened_compiled_library] is abstract and only meant for writing
-     to .vo via Marshal (which doesn't care about types).
-  *)
-  type table = constr_substituted array
-  let key_of_lazy_constr (c:lazy_constr) = (Obj.magic c : int)
-
-  (* To avoid any future misuse of the lightened library that could 
-     interpret encoded keys as real [constr_substituted], we hide 
-     these kind of values behind an abstract datatype. *)
-  type lightened_compiled_library = compiled_library
-
-  (* Map a [compiled_library] to another one by just updating 
-     the opaque term [t] to [on_opaque_const_body t]. *)
-  let traverse_library on_opaque_const_body =
-    let rec traverse_module mb =
-      match mb.mod_expr with 
-	  None -> 
-	    { mb with
-		mod_expr = None;
-		mod_type = traverse_modexpr mb.mod_type;
-	    }
-	| Some impl when impl == mb.mod_type-> 
-	    let mtb =  traverse_modexpr mb.mod_type in 
-	      { mb with
-		  mod_expr = Some mtb;
-		  mod_type = mtb;
-	      }    
-	| Some impl -> 
-	    { mb with
-		mod_expr = Option.map traverse_modexpr mb.mod_expr;
-		mod_type = traverse_modexpr mb.mod_type;
-	    }    
-    and traverse_struct struc =
-      let traverse_body (l,body) = (l,match body with
-	| (SFBconst cb) when is_opaque cb ->
-	  SFBconst {cb with const_body = on_opaque_const_body cb.const_body}
-	| (SFBconst _ | SFBmind _ ) as x -> 
-	  x
-	| SFBmodule m -> 
-	  SFBmodule (traverse_module m)
-	| SFBmodtype m -> 
-	  SFBmodtype ({m with typ_expr = traverse_modexpr m.typ_expr}))
-      in
-      List.map traverse_body struc
-
-    and traverse_modexpr = function
-      | SEBfunctor (mbid,mty,mexpr) ->
-	SEBfunctor (mbid,
-		    ({mty with
-		      typ_expr = traverse_modexpr mty.typ_expr}),
-		    traverse_modexpr mexpr)
-      | SEBident mp as x -> x
-      | SEBstruct (struc) ->
-	SEBstruct  (traverse_struct struc)
-      | SEBapply (mexpr,marg,u) ->
-	SEBapply (traverse_modexpr mexpr,traverse_modexpr marg,u)
-      | SEBwith (seb,wdcl) ->
-	SEBwith (traverse_modexpr seb,wdcl)
-    in
-    fun (dp,mb,depends,s) -> (dp,traverse_module mb,depends,s) 
-
-  (* Loading is also a traversing that decodes the embedded keys that
-     are inside the [lightened_library]. If the [load_proof] flag is
-     set, we lookup inside the table to graft the
-     [constr_substituted]. Otherwise, we set the [const_body] field
-     to [None]. 
-  *)
-  let load table lightened_library =
-    let decode_key = function
-      | Undef _ | Def _ -> assert false
-      | OpaqueDef k ->
-          let k = key_of_lazy_constr k in
-	  let body =
-	    try table.(k)
-	    with _ -> error "Error while retrieving an opaque body"
-	  in
-	  OpaqueDef (lazy_constr_from_val body)
-    in
-    traverse_library decode_key lightened_library
-
-end
+    engagement option *
+    nativecode_symb_array
 
 open Validate
 let val_deps = val_array (val_tuple ~name:"dep"[|val_dp;no_val|])
-let val_vo = val_tuple ~name:"vo" [|val_dp;val_module;val_deps;val_opt val_eng|]
+let val_vo = val_tuple ~name:"vo"
+  [|val_dp;val_module;val_deps;val_opt val_eng; no_val|]
 
 (* This function should append a certificate to the .vo file.
    The digest must be part of the certicate to rule out attackers
@@ -180,8 +82,9 @@ let stamp_library file digest = ()
 
 (* When the module is checked, digests do not need to match, but a
    warning is issued in case of mismatch *)
-let import file (dp,mb,depends,engmt as vo) digest =
+let import file (dp,mb,depends,engmt,_ as vo) table digest =
   Validate.apply !Flags.debug val_vo vo;
+  Validate.apply !Flags.debug (val_array Term.val_constr) table;
   Flags.if_verbose ppnl (str "*** vo structure validated ***"); pp_flush ();
   let env = !genv in
   check_imports msg_warning dp env depends;
@@ -193,7 +96,7 @@ let import file (dp,mb,depends,engmt as vo) digest =
   full_add_module dp mb digest
 
 (* When the module is admitted, digests *must* match *)
-let unsafe_import file (dp,mb,depends,engmt as vo) digest =
+let unsafe_import file (dp,mb,depends,engmt,_ as vo) digest =
   if !Flags.debug then ignore vo; (*Validate.apply !Flags.debug val_vo vo;*)
   let env = !genv in
   check_imports (errorlabstrm"unsafe_import") dp env depends;

checker/safe_typing.mli

@@ -19,22 +19,6 @@ type compiled_library
 
 val set_engagement : Declarations.engagement -> unit
 val import         :
-  CUnix.physical_path -> compiled_library -> Digest.t -> unit
+  CUnix.physical_path -> compiled_library -> constr array -> Digest.t -> unit
 val unsafe_import  :
   CUnix.physical_path -> compiled_library -> Digest.t -> unit
-
-(** Store the body of modules' opaque constants inside a table. 
-
-    This module is used during the serialization and deserialization
-    of vo files. 
-*)
-module LightenLibrary :
-sig
-  type table 
-  type lightened_compiled_library 
-
-  (** [load table lcl] builds a compiled library from a
-      lightened library [lcl] by remplacing every index by its related
-      opaque terms inside [table]. *)
-  val load : table -> lightened_compiled_library -> compiled_library
-end

doc/refman/RefMan-com.tex

@@ -219,25 +219,19 @@ \subsection{By command line options\index{Options of the command line}
 
 \item[{\tt -dont-load-proofs}]\ 
 
-  Warning: this is an unsafe mode.
-  Instead of loading in memory the proofs of opaque theorems, they are
-  treated as axioms. This results in smaller memory requirement and
-  faster compilation, but the behavior of the system might slightly change
-  (for instance during module subtyping), and some features won't be
-  available (for example {\tt Print Assumptions}).
+  In this mode, it is an error to access the body of opaque theorems
+  (for example via {\tt Print} or {\tt Print Assumptions}).
 
 \item[{\tt -lazy-load-proofs}]\
 
   This is the default behavior. Proofs of opaque theorems aren't
   loaded immediately in memory, but only when necessary, for instance
   during some module subtyping or {\tt Print Assumptions}. This should be
-  almost as fast and efficient as {\tt -dont-load-proofs}, with none
-  of its drawbacks.
+  almost as fast and efficient as {\tt -dont-load-proofs}.
 
 \item[{\tt -force-load-proofs}]\
 
-  Proofs of opaque theorems are loaded in memory as soon as the
-  corresponding {\tt Require} is done. This used to be Coq's default behavior.
+  Deprecated, now the same as {\tt -lazy-load-proofs}.
 
 \item[{\tt -no-hash-consing}] \mbox{}