1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Pp
open Util
open Names
open Declarations
open Environ
open Mod_checking
(************************************************************************)
(*
* Global environment
*)
let genv = ref empty_env
let reset () = genv := empty_env
let get_env () = !genv
let set_engagement c =
genv := set_engagement c !genv
(* full_add_module adds module with universes and constraints *)
let full_add_module dp mb digest =
let env = !genv in
let env = add_constraints mb.mod_constraints env in
let env = Modops.add_module mb env in
genv := add_digest env dp digest
(* Check that the engagement expected by a library matches the initial one *)
let check_engagement env c =
match engagement env, c with
| Some ImpredicativeSet, Some ImpredicativeSet -> ()
| _, None -> ()
| _, Some ImpredicativeSet ->
error "Needs option -impredicative-set"
(* Libraries = Compiled modules *)
let report_clash f caller dir =
let msg =
str "compiled library " ++ str(string_of_dirpath caller) ++
spc() ++ str "makes inconsistent assumptions over library" ++ spc() ++
str(string_of_dirpath dir) ++ fnl() in
f msg
let check_imports f caller env needed =
let check (dp,stamp) =
try
let actual_stamp = lookup_digest env dp in
if stamp <> actual_stamp then report_clash f caller dp
with Not_found ->
error ("Reference to unknown module " ^ (string_of_dirpath dp))
in
List.iter check needed
type compiled_library =
dir_path *
module_body *
(dir_path * Digest.t) list *
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 lighten_compiled_library
val save : compiled_library -> lighten_compiled_library * table
val load : load_proof:bool -> (unit -> table) -> lighten_compiled_library -> compiled_library
end = struct
(* The table is implemented as an array of [constr_substituted].
Thus, its keys are integers which can be easily embedded inside
[constr_substituted]. This way the [compiled_library] type does
not have to be changed. *)
type table = constr_substituted array
(* 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 lighten_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 lighten_module mb =
{ mb with
mod_expr = None;
mod_type = lighten_modexpr mb.mod_type;
}
and lighten_struct struc =
let lighten_body (l,body) = (l,match body with
| SFBconst ({const_opaque=true} as x) ->
SFBconst {x with const_body = on_opaque_const_body x.const_body }
| (SFBconst _ | SFBmind _ ) as x ->
x
| SFBmodule m ->
SFBmodule (lighten_module m)
| SFBmodtype m ->
SFBmodtype ({m with typ_expr = lighten_modexpr m.typ_expr}))
in
List.map lighten_body struc
and lighten_modexpr = function
| SEBfunctor (mbid,mty,mexpr) ->
SEBfunctor (mbid,
({mty with
typ_expr = lighten_modexpr mty.typ_expr}),
lighten_modexpr mexpr)
| SEBident mp as x -> x
| SEBstruct (struc) ->
SEBstruct (lighten_struct struc)
| SEBapply (mexpr,marg,u) ->
SEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u)
| SEBwith (seb,wdcl) ->
SEBwith (lighten_modexpr seb,wdcl)
in
fun (dp,mb,depends,s) -> (dp,lighten_module mb,depends,s)
(* To disburden a library from opaque definitions, we simply
traverse it and add an indirection between the module body
and its reference to a [const_body]. *)
let save library =
let ((insert : constr_substituted -> constr_substituted),
(get_table : unit -> table)) =
(* We use an integer as a key inside the table. *)
let counter = ref 0 in
(* ... but it is wrap inside a [constr_substituted]. *)
let key_as_constr key = Declarations.from_val (Term.Rel key) in
(* During the traversal, the table is implemented by a list
to get constant time insertion. *)
let opaque_definitions = ref [] in
((* Insert inside the table. *)
(fun opaque_definition ->
incr counter;
opaque_definitions := opaque_definition :: !opaque_definitions;
key_as_constr !counter),
(* Get the final table representation. *)
(fun () -> Array.of_list (List.rev !opaque_definitions)))
in
let encode_const_body : constr_substituted option -> constr_substituted option = function
| None -> None
| Some ct -> Some (insert ct)
in
let lightened_library = traverse_library encode_const_body library in
(lightened_library, get_table ())
(* Loading is also a traversing that decode 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 ~load_proof (get_table : unit -> table) lightened_library =
let decode_key : constr_substituted option -> constr_substituted option =
if load_proof then
let table = get_table () in
function Some cterm ->
Some (table.(
try
match Declarations.force_constr cterm with
| Term.Rel key -> key
| _ -> assert false
with _ -> assert false
))
| _ -> None
else
fun _ -> None
in
traverse_library decode_key lightened_library
end
open Validate
let val_deps = val_list (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|]
(* This function should append a certificate to the .vo file.
The digest must be part of the certicate to rule out attackers
that could change the .vo file between the time it was read and
the time the stamp is written.
For the moment, .vo are not signed. *)
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 =
Validate.apply !Flags.debug val_vo vo;
Flags.if_verbose msgnl (str "*** vo structure validated ***");
let env = !genv in
check_imports msg_warning dp env depends;
check_engagement env engmt;
check_module (add_constraints mb.mod_constraints env) mb.mod_mp mb;
stamp_library file digest;
(* We drop proofs once checked *)
(* let mb = lighten_module mb in*)
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 =
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;
check_engagement env engmt;
(* We drop proofs once checked *)
(* let mb = lighten_module mb in*)
full_add_module dp mb digest
|
