diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 56 |
1 files changed, 41 insertions, 15 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d1631e8cb0..1f97497d60 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -249,8 +249,36 @@ let check_engagement env expected_impredicative_set = (** {6 Stm machinery } *) +module Certificate : +sig + type t + + val make : safe_environment -> t + + (** Checks whether [dst] is a valid extension of [src] *) + val check : src:t -> dst:t -> bool +end = +struct + +type t = { + certif_struc : Declarations.structure_body; +} + +let make senv = { + certif_struc = senv.revstruct; +} + +let is_suffix l suf = match l with +| [] -> false +| _ :: l -> l == suf + +let check ~src ~dst = + is_suffix dst.certif_struc src.certif_struc + +end + type side_effect = { - from_env : Declarations.structure_body CEphemeron.key; + seff_certif : Certificate.t CEphemeron.key; seff_constant : Constant.t; seff_body : Constr.t Declarations.constant_body; } @@ -609,7 +637,7 @@ let inline_side_effects env body side_eff = let filter e = let cb = (e.seff_constant, e.seff_body) in if Environ.mem_constant e.seff_constant env then None - else Some (cb, e.from_env) + else Some (cb, e.seff_certif) in (* CAVEAT: we assure that most recent effects come first *) let side_eff = List.map_filter filter (SideEffects.repr side_eff) in @@ -678,21 +706,18 @@ let inline_private_constants env ((body, ctx), side_eff) = let ctx' = Univ.ContextSet.union ctx ctx' in (body, ctx') -let is_suffix l suf = match l with -| [] -> false -| _ :: l -> l == suf - (* Given the list of signatures of side effects, checks if they match. * I.e. if they are ordered descendants of the current revstruct. Returns the number of effects that can be trusted. *) -let check_signatures curmb sl = +let check_signatures senv sl = + let curmb = Certificate.make senv in let is_direct_ancestor accu mb = match accu with | None -> None | Some curmb -> try let mb = CEphemeron.get mb in - if is_suffix mb curmb + if Certificate.check ~src:curmb ~dst:mb then Some mb else None with CEphemeron.InvalidKey -> None in @@ -759,13 +784,14 @@ let translate_direct_opaque env kn ce = let () = assert (is_empty_private u) in { cb with const_body = OpaqueDef c } -let export_side_effects mb env eff = +let export_side_effects senv eff = + let env = senv.env in let not_exists e = not (Environ.mem_constant e.seff_constant env) in let aux (acc,sl) e = if not (not_exists e) then acc, sl - else e :: acc, e.from_env :: sl in + else e :: acc, e.seff_certif :: sl in let seff, signatures = List.fold_left aux ([],[]) (SideEffects.repr eff) in - let trusted = check_signatures mb signatures in + let trusted = check_signatures senv signatures in let push_seff env eff = let { seff_constant = kn; seff_body = cb ; _ } = eff in let env = Environ.add_constant kn (lift_constant cb) env in @@ -803,7 +829,7 @@ let push_opaque_proof pf senv = senv, o let export_private_constants eff senv = - let exported = export_side_effects senv.revstruct senv.env eff in + let exported = export_side_effects senv eff in let map senv (kn, c) = match c.const_body with | OpaqueDef p -> let local = empty_private c.const_universes in @@ -825,7 +851,7 @@ let add_constant l decl senv = | OpaqueEntry ce -> let handle env body eff = let body, uctx, signatures = inline_side_effects env body eff in - let trusted = check_signatures senv.revstruct signatures in + let trusted = check_signatures senv signatures in let trusted = if trusted then List.length signatures else 0 in body, uctx, trusted in @@ -888,9 +914,9 @@ let add_private_constant l decl senv : (Constant.t * private_constants) * safe_e in let senv = add_constant_aux senv (kn, dcb) in let eff = - let from_env = CEphemeron.create senv.revstruct in + let from_env = CEphemeron.create (Certificate.make senv) in let eff = { - from_env = from_env; + seff_certif = from_env; seff_constant = kn; seff_body = cb; } in |