package archetype

  1. Overview
  2. Docs
module M = Model
val gArchetypeDir : string
val gArchetypeLib : string
val gArchetypeColl : string
val gArchetypeSum : string
val gArchetypeList : string
val gArchetypeTrace : string
val mk_id : string -> string
val mk_ac_id : string -> string
val mk_ac_added_id : string -> string
val mk_ac_rmed_id : string -> string
val gs : string
val mk_ac : string -> ('a, 'b, string) Mlwtree.abstract_term
val mk_ac_old : string -> ((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, 'd, 'e) Mlwtree.abstract_term
val mk_ac_added : string -> ('a, 'b, string) Mlwtree.abstract_term
val mk_ac_old_added : string -> ((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, 'd, 'e) Mlwtree.abstract_term
val mk_ac_rmed : string -> ('a, 'b, string) Mlwtree.abstract_term
val mk_ac_old_rmed : string -> ((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, 'd, 'e) Mlwtree.abstract_term
val mk_ac_sv : string -> string -> ('a, 'b, string) Mlwtree.abstract_term
type change =
  1. | CAdd of Mlwtree.ident
  2. | CRm of Mlwtree.ident
  3. | CUpdate of Mlwtree.ident
  4. | CTransfer of Mlwtree.ident
  5. | CGet of Mlwtree.ident
  6. | CIterate of Mlwtree.ident
  7. | CCall of Mlwtree.ident
val mk_change_term : change -> (('a, 'b, string) Mlwtree.abstract_term, 'c, 'd) Mlwtree.abstract_term
val mk_trace : change -> Mlwtree.loc_term
val mk_const_fields : Ident.ident Location.loced Archetype__Model.model_gen -> (('a, 'b, string) Mlwtree.abstract_term, string Mlwtree.abstract_type, string) Mlwtree.abstract_field list
val mk_sum_clone_id : string -> string -> string
val mk_sum_clone : 'a -> string -> string -> string -> ('b, 'c, string) Mlwtree.abstract_decl
val mk_keys_eq_axiom : Mlwtree.ident -> Mlwtree.ident -> Mlwtree.typ -> Mlwtree.decl
val mk_partition_axiom : Mlwtree.ident -> Mlwtree.ident -> 'a -> Mlwtree.ident -> Mlwtree.typ -> Mlwtree.decl
val mk_select_test : (('a, 'b, string) Mlwtree.abstract_term, 'b, string) Mlwtree.abstract_term as 'a -> (('a, 'b, string) Mlwtree.abstract_term, 'b, string) Mlwtree.abstract_term
val extract_args : M.lident M.mterm_gen -> (M.mterm * string * 'a Mlwtree.abstract_type) list
val get_select_id : M.model -> Ident.ident -> M.mterm -> int
val mk_select_name : M.model -> Ident.ident -> M.mterm -> string
val wdl : 'a list -> 'a Mlwtree.with_loc list
val deloc : 'a Mlwtree.with_loc list -> 'a list
val zip : 'a list -> 'a list -> 'a list -> 'a list -> 'a list
val cap : string Mlwtree.with_loc -> string Mlwtree.with_loc
val map_lident : M.lident -> Mlwtree.loc_ident
val map_lidents : M.lident list -> Mlwtree.loc_ident list
val type_to_init : Mlwtree.loc_typ -> Mlwtree.loc_term
val map_btype : M.btyp -> 'a Mlwtree.abstract_type
val map_mtype : M.type_ -> Mlwtree.loc_typ
val map_term : M.mterm -> Mlwtree.loc_term
val map_record_term : 'a -> M.mterm -> Mlwtree.loc_term
val is_local_invariant : 'a -> Ident.ident -> M.lident M.mterm_gen -> bool
val adds_asset : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> M.lident M.mterm_gen -> bool
val is_only_security : M.security_predicate -> bool
val map_action_to_change : M.action_description -> change
val mk_spec_invariant : [< `Loop | `Storage ] -> M.security_item -> (Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list
val mk_invariant : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident Location.loced -> [> `Loop | `Preasset of Mlwtree.ident | `Precoll of Mlwtree.ident | `Prelist of Mlwtree.ident | `Storage ] -> Mlwtree.loc_term -> Mlwtree.loc_term
val mk_pre_list : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Mlwtree.ident -> Mlwtree.loc_term -> Mlwtree.loc_term
val mk_pre_coll : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Mlwtree.ident -> Mlwtree.loc_term -> Mlwtree.loc_term
val mk_pre_asset : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Mlwtree.ident -> Mlwtree.loc_term -> Mlwtree.loc_term
val mk_loop_invariant : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Mlwtree.loc_term -> Mlwtree.loc_term
val mk_eq_extensionality : 'a -> M.record -> Mlwtree.loc_decl
val record_to_clone : Ident.ident Location.loced Archetype__Model.model_gen -> M.info_asset -> ('a, 'b, Ident.ident Mlwtree.with_loc) Mlwtree.abstract_decl
val get_record : 'a -> ('b, 'c, 'a) Mlwtree.abstract_decl list -> ('b, 'c, 'a) Mlwtree.abstract_decl
val get_record_name : ('a, 'b, 'c) Mlwtree.abstract_decl -> 'c
type logical_mod =
  1. | Nomod
  2. | Added
  3. | Removed
type logical_context = {
  1. old : bool;
  2. lmod : logical_mod;
}
val init_ctx : logical_context
val map_mterm : Ident.ident Location.loced Archetype__Model.model_gen -> logical_context -> M.mterm -> Mlwtree.loc_term
val mk_api_precond : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> [> `Loop | `Preasset of Mlwtree.ident | `Precoll of Mlwtree.ident | `Prelist of Mlwtree.ident | `Storage ] -> (Mlwtree.term, Ident.ident) Mlwtree.abstract_formula list
val mk_key_found_cond : [< `Curr | `Old ] -> string -> ((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term -> (((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term, 'e, string) Mlwtree.abstract_term
val mk_not_found_cond : [< `Curr | `Old ] -> string -> ((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term -> ((((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term, 'e, string) Mlwtree.abstract_term, 'f, 'g) Mlwtree.abstract_term
val mk_get_field_from_pos : string -> string -> (((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, 'd, 'e) Mlwtree.abstract_term, string Mlwtree.abstract_type, string) Mlwtree.abstract_decl
val mk_get_asset : string -> string -> string Mlwtree.abstract_type -> ((((((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term, 'e, string) Mlwtree.abstract_term, 'f, string) Mlwtree.abstract_term, 'g Mlwtree.abstract_type, string) Mlwtree.abstract_term, string Mlwtree.abstract_type, string) Mlwtree.abstract_decl
val mk_set_asset_precond : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Mlwtree.ident -> (Mlwtree.term, Ident.ident) Mlwtree.abstract_formula list
val mk_contains : string -> 'a Mlwtree.abstract_type -> (((('b, 'c, string) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term, 'e Mlwtree.abstract_type, string) Mlwtree.abstract_term, 'a Mlwtree.abstract_type, string) Mlwtree.abstract_decl
val mk_unshallow : string -> string Mlwtree.abstract_type -> ((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, string Mlwtree.abstract_type, string) Mlwtree.abstract_decl
val mk_add_asset_precond : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Mlwtree.ident -> (Mlwtree.term, Ident.ident) Mlwtree.abstract_formula list
val mk_listtocoll_precond : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Mlwtree.ident -> (Mlwtree.term, Ident.ident) Mlwtree.abstract_formula list
val gen_field_getter : 'a -> 'b -> (('c, 'd, 'e) Mlwtree.abstract_term, 'f Mlwtree.abstract_type, 'a) Mlwtree.abstract_decl
val gen_field_getters : ('a, 'b, 'c) Mlwtree.abstract_decl -> (('d, 'e, 'f) Mlwtree.abstract_term, 'g Mlwtree.abstract_type, 'c) Mlwtree.abstract_decl list
val mk_add_asset : Ident.ident Location.loced Archetype__Model.model_gen -> Mlwtree.ident -> Mlwtree.ident -> Mlwtree.decl
val mk_rm_asset : Ident.ident Location.loced Archetype__Model.model_gen -> Mlwtree.ident -> Mlwtree.ident -> Mlwtree.decl
val mk_add_partition_field : Ident.ident Location.loced Archetype__Model.model_gen -> Mlwtree.ident -> Mlwtree.ident -> Mlwtree.ident -> Mlwtree.ident -> Mlwtree.ident -> Mlwtree.decl
val mk_rm_partition_field : Ident.ident Location.loced Archetype__Model.model_gen -> Mlwtree.ident -> Mlwtree.ident -> Mlwtree.ident -> Mlwtree.ident -> Mlwtree.ident -> Mlwtree.decl
val fold_exns : M.lident M.mterm_gen -> Mlwtree.term list
val is_fail : M.mterm -> bool
val flatten_if_fail : Ident.ident Location.loced Archetype__Model.model_gen -> M.mterm -> Mlwtree.loc_term
val mk_require : string -> int -> 'a -> ('a, string Mlwtree.with_loc) Mlwtree.abstract_formula
val mk_requires : Ident.ident Location.loced Archetype__Model.model_gen -> string -> Ident.ident Location.loced Archetype__Model.specification_gen option -> (Mlwtree.loc_term, string Mlwtree.with_loc) Mlwtree.abstract_formula list
val is_src : M.source -> ('a * 'b M.function_struct_gen * 'c) -> bool
val mk_entry_require : Ident.ident Location.loced Archetype__Model.model_gen -> string list -> (Mlwtree.loc_term, string Mlwtree.with_loc) Mlwtree.abstract_formula list
val mk_endo_functions : Ident.ident Location.loced Archetype__Model.model_gen -> (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl list
val mk_exo_functions : Ident.ident Location.loced Archetype__Model.model_gen -> (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl list
val rm_fail_exn : Mlwtree.loc_term list -> Mlwtree.loc_term list
val to_whyml : M.model -> Mlwtree.mlw_tree
OCaml

Innovation. Community. Security.