package archetype

  1. Overview
  2. Docs
module M = Model
type error_desc =
  1. | NotSupported of string
  2. | TODONotTranslated of string
val pp_error_desc : Stdlib.Format.formatter -> error_desc -> unit
type error = Location.t * error_desc
val emit_error : (Location.t * error_desc) -> unit
val dl : 'a -> 'a Mlwtree.with_loc
val gArchetypeDir : string
val gArchetypeLib : string
val gArchetypeField : string
val gArchetypeView : string
val gArchetypeColl : string
val gArchetypeAgg : string
val gArchetypeSum : string
val gArchetypeSort : string
val gArchetypeTrace : string
val gArchetypeSet : string
val gArchetypeList : string
val gOperations : string
val gListAs : string
val gFieldAs : string
val gViewAs : string
val mk_module_name : string -> string
val mk_id : string -> string
val mk_param_value : string -> string
val mk_ac_id : string -> string
val mk_ac_added_id : string -> string
val mk_ac_rmed_id : string -> string
val mk_ac_unmvd_id : string -> string
val mk_aggregate_id : string -> string
val gs : string
val gsinit : string
val gsarg : string
val mk_ac_st : string -> string -> ('a, 'b, string) Mlwtree.abstract_term
val mk_ac_old_st : 'a -> string -> ((('b, 'c, 'd) Mlwtree.abstract_term, 'e, string) Mlwtree.abstract_term, 'f, 'g) Mlwtree.abstract_term
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_st : string -> string -> ('a, 'b, string) Mlwtree.abstract_term
val mk_ac_old_added_st : 'a -> string -> ((('b, 'c, 'd) Mlwtree.abstract_term, 'e, string) Mlwtree.abstract_term, 'f, 'g) 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_st : string -> string -> ('a, 'b, string) Mlwtree.abstract_term
val mk_ac_old_rmed_st : 'a -> string -> ((('b, 'c, 'd) Mlwtree.abstract_term, 'e, string) Mlwtree.abstract_term, 'f, 'g) 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_field_id : string -> string
val mk_view_id : string -> string
val mk_use_euclidean_div : Ident.ident Location.loced Archetype__Model.model_gen -> (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl list
val mk_use_min_max : Ident.ident Location.loced Archetype__Model.model_gen -> (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl list
val map_lident : M.lident -> Mlwtree.loc_ident
val map_btype : M.btyp -> ('a, 'b) Mlwtree.abstract_type
val get_type_idx : M.type_ -> M.type_ list -> int
val mk_map_name : Ident.ident Location.loced Archetype__Model.model_gen -> M.type_ -> string
val mk_set_name : Ident.ident Location.loced Archetype__Model.model_gen -> M.type_ -> string
val mk_list_name : Ident.ident Location.loced Archetype__Model.model_gen -> M.type_ -> string
val map_mtype : Ident.ident Location.loced Archetype__Model.model_gen -> M.type_ -> Mlwtree.loc_typ
val mk_list_name_from_mlwtype : Ident.ident Location.loced Archetype__Model.model_gen -> Mlwtree.typ -> string
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
type trace_id_type =
  1. | Asset
  2. | Entry
  3. | Field
val trace_value_type_to_string : trace_id_type -> string
val mk_trace_id : trace_id_type -> string -> string
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, (string, 'c) Mlwtree.abstract_type) Mlwtree.abstract_type, string) Mlwtree.abstract_field list
val mk_sum_clone_id : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Ident.ident Location.loced Archetype__Model.mterm_gen -> string
val mk_sum_clone_from_id : string -> int -> string
val mk_get_sum_value_id : string -> int -> string
val mk_get_sum_value_from_pos_id : string -> int -> string
val mk_sum : string -> int -> 'a -> 'b -> ('c, 'd, string) Mlwtree.abstract_term
val mk_sum_from_col : string -> int -> 'a -> ('b, 'c, string) Mlwtree.abstract_term
val mk_sum_clone : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> string -> M.type_ -> Ident.ident Location.loced Archetype__Model.mterm_gen -> ('a, (Ident.ident, Mlwtree.typ) Mlwtree.abstract_type, string) Mlwtree.abstract_decl
val mk_partition_axiom : Mlwtree.ident -> Mlwtree.ident -> 'a -> Mlwtree.ident -> Mlwtree.typ -> Mlwtree.decl
val sort_kind_to_string : M.sort_kind -> string
val mk_cmp_function_id : string -> (string * M.sort_kind) list -> string
val mk_cmp_function : Ident.ident Location.loced Archetype__Model.model_gen -> Mlwtree.ident -> (Ident.ident * M.sort_kind) list -> (Mlwtree.term, Mlwtree.typ, Mlwtree.ident) Mlwtree.abstract_decl
val mk_sort_clone_id : string -> (string * M.sort_kind) list -> string
val mk_sort_clone : 'a -> string -> (string * M.sort_kind) list -> ('b, (string, 'c) Mlwtree.abstract_type, string) Mlwtree.abstract_decl
type filter =
  1. | Select
  2. | Removeif
val mk_afun_test : ((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term as 'a, 'b, string) Mlwtree.abstract_term -> ((('a, 'b, string) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term, 'e, string) Mlwtree.abstract_term
val acc_has_id : 'a -> ('b * 'c * 'd) list -> bool
val extract_args : M.lident M.mterm_gen -> (M.mterm * string * ('a, 'b) Mlwtree.abstract_type) list
val mk_filter_name : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Ident.ident Location.loced Archetype__Model.mterm_gen -> filter -> string
val mk_select_name : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Ident.ident Location.loced Archetype__Model.mterm_gen -> string
val mk_removeif_name : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Ident.ident Location.loced Archetype__Model.mterm_gen -> string
val mk_filter_predicate : filter -> Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Ident.ident Location.loced Archetype__Model.mterm_gen -> ((('a, ('c, 'd) Mlwtree.abstract_type, string) Mlwtree.abstract_term as 'b, ('c, 'd) Mlwtree.abstract_type, string) Mlwtree.abstract_term as 'a, ('c, 'd) Mlwtree.abstract_type, string) Mlwtree.abstract_term -> (string * M.type_) list -> (((('b, ('c, 'd) Mlwtree.abstract_type, string) Mlwtree.abstract_term, ('c, 'd) Mlwtree.abstract_type, string) Mlwtree.abstract_term, ('c, 'd) Mlwtree.abstract_type, string) Mlwtree.abstract_term, Mlwtree.typ, string) Mlwtree.abstract_decl
val get_definition_body : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> M.lident M.mterm_gen option
val get_predicate_body : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> M.lident M.mterm_gen option
val is_predicate : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> bool
val extract_def_args : Ident.ident Location.loced Archetype__Model.model_gen -> M.lident M.mterm_gen -> (('a, 'b, Ident.ident) Mlwtree.abstract_term * Ident.ident * Mlwtree.loc_typ) list
val get_def_params : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> ('a, 'b, Ident.ident) Mlwtree.abstract_term list
val get_pred_params : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> ('a, 'b, Ident.ident) Mlwtree.abstract_term list
val wdl : 'a list -> 'a0 Mlwtree.with_loc list
val deloc : 'a Mlwtree.with_loc list -> 'b list
val zip : 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i list
val cap : string Mlwtree.with_loc -> string Mlwtree.with_loc
val mk_map_clone : string -> 'a -> 'b -> ('c, 'd, string Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_set_clone : string -> 'a -> ('b, 'c, string Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_list_clone : string -> 'a -> ('b, 'c, string Mlwtree.with_loc) Mlwtree.abstract_decl
val map_record_fields : Ident.ident Location.loced Archetype__Model.model_gen -> M.record_field list -> (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_field list
val map_lidents : M.lident list -> Mlwtree.loc_ident list
val type_to_init : Ident.ident Location.loced Archetype__Model.model_gen -> Mlwtree.loc_typ -> 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.entry_description -> change
val map_security_pred : [< `Loop | `Storage ] -> M.security_predicate -> ((('a, ('b, 'c) Mlwtree.abstract_type, Ident.ident) Mlwtree.abstract_term as 'a, ('b, 'c) Mlwtree.abstract_type, Ident.ident) Mlwtree.abstract_term, 'd, 'e) Mlwtree.abstract_term
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_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_enums : Ident.ident Location.loced Archetype__Model.model_gen -> M.asset -> (Mlwtree.loc_term, Mlwtree.loc_typ, string Mlwtree.with_loc) Mlwtree.abstract_decl list
val get_fail_idx : Ident.ident Location.loced Archetype__Model.model_gen -> M.type_ -> int
val mk_field : Ident.ident Location.loced Archetype__Model.model_gen -> M.asset -> ('a, Mlwtree.loc_typ, string Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_view : Ident.ident Location.loced Archetype__Model.model_gen -> M.asset -> ('a, Mlwtree.loc_typ, string Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_set_field_id : string -> string
val get_record : 'a -> ('b, 'c, 'd) Mlwtree.abstract_decl list -> ('e, 'f, 'g) Mlwtree.abstract_decl
val get_record_name : ('a, 'b, 'c) Mlwtree.abstract_decl -> 'd
val mk_lbl_before : string option -> string
val mk_inv_lbl : string option -> string -> string
val mk_storage_loop_inv : string option -> Mlwtree.ident -> Mlwtree.ident -> (Mlwtree.loc_term, string Mlwtree.with_loc) Mlwtree.abstract_formula
val is_identical : Tools.String.t -> M.effect list -> bool
val mk_vars_loop_invariants : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident option -> string option -> Mlwtree.ident -> Ident.ident Location.loced Archetype__Model.mterm_gen -> (Mlwtree.loc_term, string Mlwtree.with_loc) Mlwtree.abstract_formula list
type mode =
  1. | Inv
  2. | Logic
  3. | Exec
  4. | Def
type logical_context = {
  1. lctx : mode;
  2. entry_id : Mlwtree.ident option;
  3. locals : Mlwtree.ident list;
  4. loop_id : Mlwtree.ident option;
  5. fun_ : bool;
  6. fails : bool;
}
val init_ctx : logical_context
val mk_sid : logical_context -> string
val is_coll_field : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> bool
val is_exec_divergent : ('a, 'b) M.mterm_node -> bool
val get_tuple_size : M.ntype -> int
val cp_storage : string -> (('a, 'b, string) Mlwtree.abstract_term, 'c, 'd) Mlwtree.abstract_term
val is_partition : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Ident.ident -> bool
val mk_storage_id : logical_context -> string
val mk_coll_term : string -> logical_context -> (M.temp * M.delta) -> ((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, 'd, Ident.ident) Mlwtree.abstract_term
val mk_loc_coll_term : string -> logical_context -> (M.temp * M.delta) -> Mlwtree.loc_term
val mk_lc_term : string -> logical_context -> Mlwtree.loc_term
val mk_temp_delta : 'a M.container_kind_gen -> M.temp * M.delta
val map_mterm : Ident.ident Location.loced Archetype__Model.model_gen -> logical_context -> M.mterm -> Mlwtree.loc_term
val mk_filter_args : Ident.ident Location.loced Archetype__Model.model_gen -> logical_context -> (Mlwtree.ident * M.type_) list -> M.lident M.mterm_gen -> Mlwtree.loc_term list
val mk_asset_key_value : Ident.ident Location.loced Archetype__Model.model_gen -> logical_context -> Ident.ident -> M.lident M.mterm_gen -> Mlwtree.loc_term
val map_asset_values : Ident.ident Location.loced Archetype__Model.model_gen -> M.asset_item list -> (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_field list
val map_init_mterm : Ident.ident Location.loced Archetype__Model.model_gen -> logical_context -> M.mterm -> Mlwtree.loc_term
val mk_asset_invariants : Ident.ident Location.loced Archetype__Model.model_gen -> logical_context -> (Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list
val mk_contract_invariants : Ident.ident Location.loced Archetype__Model.model_gen -> logical_context -> (Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list
val mk_variable_invariants : Ident.ident Location.loced Archetype__Model.model_gen -> logical_context -> (Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list
val mk_security_invariants : M.model -> 'a -> (Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list
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, ('f, 'g) Mlwtree.abstract_type, 'h) 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_type, 'h) Mlwtree.abstract_term
val mk_get_sum_value_from_pos : string -> int -> ((('a, 'c, string) Mlwtree.abstract_term as 'b, 'c, string) Mlwtree.abstract_term as 'a, 'c, string) Mlwtree.abstract_term -> ((((('b, 'c, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, (string, 'd) Mlwtree.abstract_type, string) Mlwtree.abstract_decl
val mk_get_sum_value : string -> int -> ((('a, 'c, string) Mlwtree.abstract_term as 'b, 'c, string) Mlwtree.abstract_term as 'a, 'c, string) Mlwtree.abstract_term -> ((('b, 'c, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, (string, 'd) Mlwtree.abstract_type, string) Mlwtree.abstract_decl
val mk_storage_api_before_storage : M.model -> 'a -> (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl list
val fold_fails : Ident.ident Location.loced Archetype__Model.model_gen -> logical_context -> M.lident M.mterm_gen -> (Mlwtree.loc_ident option * Mlwtree.loc_term) list
val fold_exns : Ident.ident Location.loced Archetype__Model.model_gen -> 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 -> logical_context -> M.mterm -> Mlwtree.loc_term
val mk_delta_requires : Ident.ident Location.loced Archetype__Model.model_gen -> (Mlwtree.loc_term, string Mlwtree.with_loc) Mlwtree.abstract_formula list
val mk_preconds : Ident.ident Location.loced Archetype__Model.model_gen -> M.argument list -> M.lident M.mterm_gen -> (Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list
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_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
type desc_container =
  1. | Dset of M.type_
  2. | Dlist of M.type_
  3. | Dmap of M.type_
  4. | Dasset of M.asset
  5. | Denum of M.enum
  6. | Drecord of M.record
val show_desc_container : desc_container -> Ppx_deriving_runtime.string
val pp_desc_container : Stdlib.Format.formatter -> desc_container -> unit
val cmp_desc_container : desc_container -> desc_container -> bool
val to_whyml : M.model -> Mlwtree.mlw_tree