https://github.com/EasyCrypt/easycrypt
Tip revision: ab2599f60819d119abc0a6cdb043e5742260797d authored by Antoine Séré on 04 October 2022, 15:56:46 UTC
Issue after merge in compilation, ppx_deriving added to nix
Issue after merge in compilation, ppx_deriving added to nix
Tip revision: ab2599f
ecCoreFol.mli
(* -------------------------------------------------------------------- *)
open EcUtils
open EcBigInt
open EcPath
open EcMaps
open EcIdent
open EcTypes
open EcCoreModules
open EcMemory
(* -------------------------------------------------------------------- *)
val mhr : memory
val mleft : memory
val mright : memory
(* -------------------------------------------------------------------- *)
type quantif =
| Lforall
| Lexists
| Llambda
type hoarecmp = FHle | FHeq | FHge
type gty =
| GTty of (EcTypes.ty [@opaque])
| GTmodty of (module_type [@opaque])
| GTmem of (EcMemory.memtype [@opaque])
[@@deriving show]
and binding = ((EcIdent.t * gty) [@opaque])
[@@deriving show]
and bindings = (binding list [@opaque])
[@@deriving show]
and form = private {
f_node : f_node;
f_ty : ty;
f_fv : int EcIdent.Mid.t; (* local, memory, module ident *)
f_tag : int;
}
[@@deriving show]
and f_node =
| Fquant of (quantif [@opaque]) * (bindings [@opaque]) * form
| Fif of form * form * form
| Fmatch of form * form list * (ty [@opaque])
| Flet of (lpattern [@opaque]) * form * form
| Fint of (zint [@opaque])
| Flocal of (EcIdent.t [@opaque])
| Fpvar of (EcTypes.prog_var [@opaque]) * (memory [@opaque])
| Fglob of (EcPath.mpath [@opaque]) * (memory [@opaque])
| Fop of (EcPath.path [@opaque]) * (ty list [@opaque])
| Fapp of form * form list
| Ftuple of form list
| Fproj of form * int
| FhoareF of (sHoareF [@opaque]) (* $hr / $hr *)
| FhoareS of (sHoareS [@opaque])
| FcHoareF of (cHoareF [@opaque]) (* $hr / $hr *)
| FcHoareS of (cHoareS [@opaque])
| FbdHoareF of (bdHoareF [@opaque]) (* $hr / $hr *)
| FbdHoareS of (bdHoareS [@opaque])
| FequivF of (equivF [@opaque]) (* $left,$right / $left,$right *)
| FequivS of (equivS [@opaque])
| FeagerF of (eagerF [@opaque])
| Fcoe of (coe [@opaque])
| Fpr of (pr [@opaque]) (* hr *)
[@@deriving show]
and eagerF = {
eg_pr : (form [@opaque]);
eg_sl : (stmt [@opaque]); (* No local program variables *)
eg_fl : (EcPath.xpath [@opaque]);
eg_fr : (EcPath.xpath [@opaque]);
eg_sr : (stmt [@opaque]); (* No local program variables *)
eg_po : (form [@opaque])
}
[@@deriving show]
and equivF = {
ef_pr : (form [@opaque]);
ef_fl : (EcPath.xpath [@opaque]);
ef_fr : (EcPath.xpath [@opaque]);
ef_po : (form [@opaque]);
}
[@@deriving show]
and equivS = {
es_ml : (EcMemory.memenv [@opaque]);
es_mr : (EcMemory.memenv [@opaque]);
es_pr : (form [@opaque]);
es_sl : (stmt [@opaque]);
es_sr : (stmt [@opaque]);
es_po : (form [@opaque]); }
[@@deriving show]
and sHoareF = {
hf_pr : (form [@opaque]);
hf_f : (EcPath.xpath [@opaque]);
hf_po : (form [@opaque]);
}
[@@deriving show]
and sHoareS = {
hs_m : (EcMemory.memenv [@opaque]);
hs_pr : (form [@opaque]);
hs_s : (stmt [@opaque]);
hs_po : (form [@opaque]); }
[@@deriving show]
and cHoareF = {
chf_pr : (form [@opaque]);
chf_f : (EcPath.xpath [@opaque]);
chf_po : (form [@opaque]);
chf_co : (cost [@opaque]);
}
[@@deriving show]
and cHoareS = {
chs_m : (EcMemory.memenv [@opaque]);
chs_pr : (form [@opaque]);
chs_s : (stmt [@opaque]);
chs_po : (form [@opaque]);
chs_co : (cost [@opaque]); }
[@@deriving show]
and bdHoareF = {
bhf_pr : (form [@opaque]);
bhf_f : (EcPath.xpath [@opaque]);
bhf_po : (form [@opaque]);
bhf_cmp : (hoarecmp [@opaque]);
bhf_bd : (form [@opaque]);
}
[@@deriving show]
and bdHoareS = {
bhs_m : (EcMemory.memenv [@opaque]);
bhs_pr : (form [@opaque]);
bhs_s : (stmt [@opaque]);
bhs_po : (form [@opaque]);
bhs_cmp : (hoarecmp [@opaque]);
bhs_bd : (form [@opaque]);
}
[@@deriving show]
and coe = {
coe_pre : (form [@opaque]);
coe_mem : (EcMemory.memenv [@opaque]);
coe_e : (expr [@opaque]);
}
[@@deriving show]
and pr = {
pr_mem : (memory [@opaque]);
pr_fun : (EcPath.xpath [@opaque]);
pr_args : (form [@opaque]);
pr_event : (form [@opaque]);
}
[@@deriving show]
(* Invariant: keys of c_calls are functions of local modules,
with no arguments. *)
and cost = private {
c_self : (form [@opaque]); (* of type xint *)
c_calls : (call_bound EcPath.Mx.t [@opaque]);
}
[@@deriving show]
(* Call with cost at most [cb_cost], called at mist [cb_called].
[cb_cost] is here to properly handle substsitution when instantiating an
abstract module by a concrete one. *)
and call_bound = private {
cb_cost : (form [@opaque]);
cb_called : (form [@opaque]);
}
[@@deriving show]
and module_type = (form p_module_type [@opaque])
[@@deriving show]
type mod_restr = form p_mod_restr
(* -------------------------------------------------------------------- *)
val gtty : EcTypes.ty -> gty
val gtmodty : module_type -> gty
val gtmem : EcMemory.memtype -> gty
(* -------------------------------------------------------------------- *)
val as_gtty : gty -> EcTypes.ty
val as_modty : gty -> module_type
val as_mem : gty -> EcMemory.memtype
(* -------------------------------------------------------------------- *)
val gty_equal : gty -> gty -> bool
val gty_fv : gty -> int Mid.t
(* -------------------------------------------------------------------- *)
val mty_equal : module_type -> module_type -> bool
val mty_hash : module_type -> int
val mr_equal : mod_restr -> mod_restr -> bool
val mr_hash : mod_restr -> int
(* -------------------------------------------------------------------- *)
val f_equal : form -> form -> bool
val f_compare : form -> form -> int
val f_hash : form -> int
val f_fv : form -> int Mid.t
val f_ty : form -> EcTypes.ty
val f_ops : form -> Sp.t
module Mf : Map.S with type key = form
module Sf : Set.S with module M = Map.MakeBase(Mf)
module Hf : EHashtbl.S with type key = form
(* -------------------------------------------------------------------- *)
val mk_form : f_node -> EcTypes.ty -> form
val f_node : form -> f_node
(* -------------------------------------------------------------------- *)
(* not recursive *)
val f_map : (EcTypes.ty -> EcTypes.ty) -> (form -> form) -> form -> form
val f_iter : (form -> unit) -> form -> unit
val form_exists: (form -> bool) -> form -> bool
val form_forall: (form -> bool) -> form -> bool
(* -------------------------------------------------------------------- *)
val gty_as_ty : gty -> EcTypes.ty
val gty_as_mem : gty -> EcMemory.memtype
val gty_as_mod : gty -> module_type
val kind_of_gty: gty -> [`Form | `Mem | `Mod]
(* soft-constructors - common leaves *)
val f_local : EcIdent.t -> EcTypes.ty -> form
val f_pvar : EcTypes.prog_var -> EcTypes.ty -> memory -> form
val f_pvarg : EcTypes.ty -> memory -> form
val f_pvloc : variable -> memory -> form
val f_glob : mpath -> memory -> form
(* soft-constructors - common formulas constructors *)
val f_op : path -> EcTypes.ty list -> EcTypes.ty -> form
val f_app : form -> form list -> EcTypes.ty -> form
val f_tuple : form list -> form
val f_proj : form -> int -> EcTypes.ty -> form
val f_if : form -> form -> form -> form
val f_match : form -> form list -> EcTypes.ty -> form
val f_let : EcTypes.lpattern -> form -> form -> form
val f_let1 : EcIdent.t -> form -> form -> form
val f_quant : quantif -> bindings -> form -> form
val f_exists : bindings -> form -> form
val f_forall : bindings -> form -> form
val f_lambda : bindings -> form -> form
val f_forall_mems : (EcIdent.t * memtype) list -> form -> form
(* soft-constructors - hoare *)
val f_hoareF_r : sHoareF -> form
val f_hoareS_r : sHoareS -> form
val f_hoareF : form -> xpath -> form -> form
val f_hoareS : memenv -> form -> stmt -> form -> form
(* soft-constructors - cost hoare *)
val cost_r : form -> call_bound EcPath.Mx.t -> cost
val call_bound_r : form -> form -> call_bound
val f_cHoareF_r : cHoareF -> form
val f_cHoareS_r : cHoareS -> form
val f_cHoareF : form -> xpath -> form -> cost -> form
val f_cHoareS : memenv -> form -> stmt -> form -> cost -> form
(* soft-constructors - bd hoare *)
val hoarecmp_opp : hoarecmp -> hoarecmp
val f_bdHoareF_r : bdHoareF -> form
val f_bdHoareS_r : bdHoareS -> form
val f_bdHoareF : form -> xpath -> form -> hoarecmp -> form -> form
val f_bdHoareS : memenv -> form -> stmt -> form -> hoarecmp -> form -> form
(* soft-constructors - equiv *)
val f_equivS : memenv -> memenv -> form -> stmt -> stmt -> form -> form
val f_equivF : form -> xpath -> xpath -> form -> form
val f_equivS_r : equivS -> form
val f_equivF_r : equivF -> form
(* soft-constructors - eager *)
val f_eagerF_r : eagerF -> form
val f_eagerF : form -> stmt -> xpath -> xpath -> stmt -> form -> form
(* soft-constructors - Coe *)
val f_coe_r : coe -> form
val f_coe : form -> memenv -> expr -> form
(* soft-constructors - Pr *)
val f_pr_r : pr -> form
val f_pr : memory -> xpath -> form -> form -> form
(* soft-constructors - unit *)
val f_tt : form
(* soft-constructors - bool *)
val f_bool : bool -> form
val f_true : form
val f_false : form
(* soft-constructors - boolean operators *)
val fop_not : form
val fop_and : form
val fop_anda : form
val fop_or : form
val fop_ora : form
val fop_imp : form
val fop_iff : form
val fop_eq : EcTypes.ty -> form
val f_not : form -> form
val f_and : form -> form -> form
val f_ands : form list -> form
val f_anda : form -> form -> form
val f_andas : form list -> form
val f_or : form -> form -> form
val f_ors : form list -> form
val f_ora : form -> form -> form
val f_oras : form list -> form
val f_imp : form -> form -> form
val f_imps : form list -> form -> form
val f_iff : form -> form -> form
val f_eq : form -> form -> form
val f_eqs : form list -> form list -> form
(* soft-constructors - integers *)
val fop_int_opp : form
val fop_int_add : form
val fop_int_pow : form
val f_i0 : form
val f_i1 : form
val f_im1 : form
val f_int : zint -> form
val f_int_add : form -> form -> form
val f_int_sub : form -> form -> form
val f_int_opp : form -> form
val f_int_mul : form -> form -> form
val f_int_pow : form -> form -> form
val f_int_edivz : form -> form -> form
(* -------------------------------------------------------------------- *)
val f_is_inf : form -> form
val f_is_int : form -> form
val f_Inf : form
val f_N : form -> form
val f_xopp : form -> form
val f_xadd : form -> form -> form
val f_xmul : form -> form -> form
val f_xmuli : form -> form -> form
val f_xle : form -> form -> form
val f_xmax : form -> form -> form
val f_x0 : form
val f_x1 : form
(* -------------------------------------------------------------------- *)
module FSmart : sig
type a_local = EcIdent.t * ty
type a_pvar = prog_var * ty * memory
type a_quant = quantif * bindings * form
type a_if = form tuple3
type a_match = form * form list * ty
type a_let = lpattern * form * form
type a_op = path * ty list * ty
type a_tuple = form list
type a_app = form * form list * ty
type a_proj = form * ty
type a_glob = mpath * memory
val f_local : (form * a_local ) -> a_local -> form
val f_pvar : (form * a_pvar ) -> a_pvar -> form
val f_quant : (form * a_quant ) -> a_quant -> form
val f_if : (form * a_if ) -> a_if -> form
val f_match : (form * a_match ) -> a_match -> form
val f_let : (form * a_let ) -> a_let -> form
val f_op : (form * a_op ) -> a_op -> form
val f_tuple : (form * a_tuple ) -> a_tuple -> form
val f_app : (form * a_app ) -> a_app -> form
val f_proj : (form * a_proj ) -> a_proj -> int -> form
val f_glob : (form * a_glob ) -> a_glob -> form
val f_hoareF : (form * sHoareF ) -> sHoareF -> form
val f_hoareS : (form * sHoareS ) -> sHoareS -> form
val f_cHoareF : (form * cHoareF ) -> cHoareF -> form
val f_cHoareS : (form * cHoareS ) -> cHoareS -> form
val f_bdHoareF : (form * bdHoareF ) -> bdHoareF -> form
val f_bdHoareS : (form * bdHoareS ) -> bdHoareS -> form
val f_equivF : (form * equivF ) -> equivF -> form
val f_equivS : (form * equivS ) -> equivS -> form
val f_eagerF : (form * eagerF ) -> eagerF -> form
val f_coe : (form * coe ) -> coe -> form
val f_pr : (form * pr ) -> pr -> form
end
(* -------------------------------------------------------------------- *)
exception DestrError of string
val destr_error : string -> 'a
(* -------------------------------------------------------------------- *)
val destr_app1 : name:string -> (path -> bool) -> form -> form
val destr_app2 : name:string -> (path -> bool) -> form -> form * form
val destr_app1_eq : name:string -> path -> form -> form
val destr_app2_eq : name:string -> path -> form -> form * form
val destr_op : form -> EcPath.path * ty list
val destr_local : form -> EcIdent.t
val destr_pvar : form -> prog_var * memory
val destr_proj : form -> form * int
val destr_tuple : form -> form list
val destr_app : form -> form * form list
val destr_op_app : form -> (EcPath.path * ty list) * form list
val destr_not : form -> form
val destr_nots : form -> bool * form
val destr_and : form -> form * form
val destr_and3 : form -> form * form * form
val destr_and_r : form -> [`Sym | `Asym] * (form * form)
val destr_or : form -> form * form
val destr_or_r : form -> [`Sym | `Asym] * (form * form)
val destr_imp : form -> form * form
val destr_iff : form -> form * form
val destr_eq : form -> form * form
val destr_eq_or_iff : form -> form * form
val destr_let : form -> lpattern * form * form
val destr_let1 : form -> EcIdent.t * ty * form * form
val destr_forall1 : form -> EcIdent.t * gty * form
val destr_forall : form -> bindings * form
val decompose_forall: form -> bindings * form
val decompose_lambda: form -> bindings * form
val destr_lambda : form -> bindings * form
val destr_exists1 : form -> EcIdent.t * gty * form
val destr_exists : form -> bindings * form
val destr_equivF : form -> equivF
val destr_equivS : form -> equivS
val destr_eagerF : form -> eagerF
val destr_hoareF : form -> sHoareF
val destr_hoareS : form -> sHoareS
val destr_cHoareF : form -> cHoareF
val destr_cHoareS : form -> cHoareS
val destr_bdHoareF : form -> bdHoareF
val destr_bdHoareS : form -> bdHoareS
val destr_coe : form -> coe
val destr_pr : form -> pr
val destr_programS : [`Left | `Right] option -> form -> memenv * stmt
val destr_int : form -> zint
val destr_glob : form -> EcPath.mpath * memory
val destr_pvar : form -> EcTypes.prog_var * memory
(* -------------------------------------------------------------------- *)
val is_true : form -> bool
val is_false : form -> bool
val is_tuple : form -> bool
val is_not : form -> bool
val is_and : form -> bool
val is_or : form -> bool
val is_imp : form -> bool
val is_iff : form -> bool
val is_forall : form -> bool
val is_exists : form -> bool
val is_lambda : form -> bool
val is_let : form -> bool
val is_eq : form -> bool
val is_op : form -> bool
val is_local : form -> bool
val is_pvar : form -> bool
val is_proj : form -> bool
val is_equivF : form -> bool
val is_equivS : form -> bool
val is_eagerF : form -> bool
val is_hoareF : form -> bool
val is_hoareS : form -> bool
val is_cHoareF : form -> bool
val is_cHoareS : form -> bool
val is_bdHoareF : form -> bool
val is_bdHoareS : form -> bool
val is_coe : form -> bool
val is_pr : form -> bool
val is_eq_or_iff : form -> bool
(* -------------------------------------------------------------------- *)
val split_fun : form -> bindings * form
val split_args : form -> form * form list
(* -------------------------------------------------------------------- *)
val form_of_expr : EcMemory.memory -> EcTypes.expr -> form
(* -------------------------------------------------------------------- *)
exception CannotTranslate
val expr_of_form : EcMemory.memory -> form -> EcTypes.expr
(* -------------------------------------------------------------------- *)
(* A predicate on memory: λ mem. -> pred *)
type mem_pr = EcMemory.memory * form
(* -------------------------------------------------------------------- *)
type f_subst = private {
fs_freshen : bool; (* true means realloc local *)
fs_loc : form Mid.t;
fs_mem : EcIdent.t Mid.t;
fs_sty : ty_subst;
fs_ty : ty -> ty;
fs_opdef : (EcIdent.t list * expr) Mp.t;
fs_pddef : (EcIdent.t list * form) Mp.t;
fs_modtydef : path Mp.t;
fs_esloc : expr Mid.t;
fs_memtype : EcMemory.memtype option; (* Only substituted in Fcoe *)
fs_mempred : mem_pr Mid.t; (* For predicates over memories,
only substituted in Fcoe *)
}
(* -------------------------------------------------------------------- *)
module Fsubst : sig
val f_subst_id : f_subst
val is_subst_id : f_subst -> bool
val f_subst_init :
?freshen:bool
-> ?sty:ty_subst
-> ?opdef:(EcIdent.t list * expr) Mp.t
-> ?prdef:(EcIdent.t list * form) Mp.t
-> ?modtydef:path Mp.t
-> ?esloc:expr Mid.t
-> ?mt:EcMemory.memtype
-> ?mempred:(mem_pr Mid.t)
-> unit -> f_subst
val f_bind_local : f_subst -> EcIdent.t -> form -> f_subst
val f_bind_mem : f_subst -> EcIdent.t -> EcIdent.t -> f_subst
val f_bind_mod : f_subst -> EcIdent.t -> mpath -> f_subst
val f_bind_rename : f_subst -> EcIdent.t -> EcIdent.t -> ty -> f_subst
val f_subst : ?tx:(form -> form -> form) -> f_subst -> form -> form
val f_subst_local : EcIdent.t -> form -> form -> form
val f_subst_mem : EcIdent.t -> EcIdent.t -> form -> form
val f_subst_mod : EcIdent.t -> mpath -> form -> form
val uni_subst : (EcUid.uid -> ty option) -> f_subst
val uni : (EcUid.uid -> ty option) -> form -> form
val subst_tvar :
?es_loc:(EcTypes.expr EcIdent.Mid.t) ->
EcTypes.ty EcIdent.Mid.t ->
form -> form
val add_binding : f_subst -> binding -> f_subst * binding
val add_bindings : f_subst -> bindings -> f_subst * bindings
val subst_locals : form Mid.t -> form -> form
val subst_lpattern : f_subst -> lpattern -> f_subst * lpattern
val subst_xpath : f_subst -> xpath -> xpath
val subst_stmt : f_subst -> stmt -> stmt
val subst_e : f_subst -> expr -> expr
val subst_me : f_subst -> EcMemory.memenv -> EcMemory.memenv
val subst_m : f_subst -> EcIdent.t -> EcIdent.t
val subst_ty : f_subst -> ty -> ty
val subst_mty : f_subst -> module_type -> module_type
val subst_oi : f_subst -> form PreOI.t -> form PreOI.t
val subst_gty : f_subst -> gty -> gty
end
(* -------------------------------------------------------------------- *)
val can_subst : form -> bool
(* -------------------------------------------------------------------- *)
type core_op = [
| `True
| `False
| `Not
| `And of [`Asym | `Sym]
| `Or of [`Asym | `Sym]
| `Imp
| `Iff
| `Eq
]
val core_op_kind : path -> core_op option