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_trace_entry : Ident.ident Location.loced Archetype__Model.model_gen -> (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl Mlwtree.with_loc
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 mk_select_body : Mlwtree.ident -> (('a, Mlwtree.typ, Mlwtree.ident) Mlwtree.abstract_term, Mlwtree.typ, Mlwtree.ident) Mlwtree.abstract_term as 'a -> Mlwtree.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 -> [> `Axiom | `Axiom2 | `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_axiom_invariant : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Mlwtree.loc_term -> Mlwtree.loc_term
val mk_axiom2_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 -> string -> Ident.ident -> [> `Axiom | `Axiom2 | `Loop | `Preasset of Mlwtree.ident | `Precoll of Mlwtree.ident | `Prelist of Mlwtree.ident | `Storage ] -> (Mlwtree.term, string) 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 -> string -> Ident.ident -> Mlwtree.ident -> (Mlwtree.term, string) 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 -> string -> Ident.ident -> Mlwtree.ident -> (Mlwtree.term, string) Mlwtree.abstract_formula list
val mk_listtocoll_precond : Ident.ident Location.loced Archetype__Model.model_gen -> string -> Ident.ident -> Mlwtree.ident -> (Mlwtree.term, string) Mlwtree.abstract_formula list
val mk_listtocoll : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> (Mlwtree.term, Ident.ident Mlwtree.abstract_type, string) Mlwtree.abstract_decl
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.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct