Skip to main content

πŸƒΒ V7_modules.v

Environment

Gitlab

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.Variant.

Module Type Pervasives_signature.
  Parameter raise : βˆ€ {a : Set}, extensible_type β†’ a.

  Parameter raise_notrace : βˆ€ {a : Set}, extensible_type β†’ a.

  Parameter invalid_arg : βˆ€ {a : Set}, string β†’ a.

  Parameter failwith : βˆ€ {a : Set}, string β†’ a.

  Parameter not : bool β†’ bool.

  Parameter op_andand : bool β†’ bool β†’ bool.

  Parameter op_pipepipe : bool β†’ bool β†’ bool.

  Parameter __LOC__ : string.

  Parameter __FILE__ : string.

  Parameter __LINE__ : int.

  Parameter __MODULE__ : string.

  Parameter __POS__ : string Γ— int Γ— int Γ— int.

  Parameter __LOC_OF__ : βˆ€ {a : Set}, a β†’ string Γ— a.

  Parameter __LINE_OF__ : βˆ€ {a : Set}, a β†’ int Γ— a.

  Parameter __POS_OF__ : βˆ€ {a : Set}, a β†’ (string Γ— int Γ— int Γ— int) Γ— a.

  Parameter op_pipegt : βˆ€ {a b : Set}, a β†’ (a β†’ b) β†’ b.

  Parameter op_atat : βˆ€ {a b : Set}, (a β†’ b) β†’ a β†’ b.

  Parameter op_tildeminus : int β†’ int.

  Parameter op_tildeplus : int β†’ int.

  Parameter succ : int β†’ int.

  Parameter pred : int β†’ int.

  Parameter op_plus : int β†’ int β†’ int.

  Parameter op_minus : int β†’ int β†’ int.

  Parameter op_star : int β†’ int β†’ int.

  Parameter op_div : int β†’ int β†’ int.

  Parameter _mod : int β†’ int β†’ int.

  Parameter abs : int β†’ int.

  Parameter max_int : int.

  Parameter min_int : int.

  Parameter land : int β†’ int β†’ int.

  Parameter lor : int β†’ int β†’ int.

  Parameter lxor : int β†’ int β†’ int.

  Parameter lnot : int β†’ int.

  Parameter lsl : int β†’ int β†’ int.

  Parameter lsr : int β†’ int β†’ int.

  Parameter asr : int β†’ int β†’ int.

  Parameter op_caret : string β†’ string β†’ string.

  Parameter int_of_char : ascii β†’ int.

  Parameter char_of_int : int β†’ ascii.

  Parameter ignore : βˆ€ {a : Set}, a β†’ unit.

  Parameter string_of_bool : bool β†’ string.

  Parameter bool_of_string_opt : string β†’ option bool.

  Parameter string_of_int : int β†’ string.

  Parameter int_of_string_opt : string β†’ option int.

  Parameter fst : βˆ€ {a b : Set}, a Γ— b β†’ a.

  Parameter snd : βˆ€ {a b : Set}, a Γ— b β†’ b.

  Parameter op_at : βˆ€ {a : Set}, list a β†’ list a β†’ list a.

  Module ref.
    Record record {a : Set} : Set := Build {
      contents : a;
    }.
    Arguments record : clear implicits.
    Definition with_contents {t_a} contents (r : record t_a) :=
      Build t_a contents.
  End ref.
  Definition ref := ref.record.

  Parameter ref_value : βˆ€ {a : Set}, a β†’ ref a.

  Parameter op_exclamation : βˆ€ {a : Set}, ref a β†’ a.

  Parameter op_coloneq : βˆ€ {a : Set}, ref a β†’ a β†’ unit.

  Parameter incr : ref int β†’ unit.

  Parameter decr : ref int β†’ unit.

  Inductive result (a b : Set) : Set :=
  | Ok : a β†’ result a b
  | Error : b β†’ result a b.

  Arguments Ok {_ _}.
  Arguments Error {_ _}.

  Definition format6 (a b c d e f : Set) : Set :=
    CamlinternalFormatBasics.format6 a b c d e f.

  Definition format4 (a b c d : Set) : Set := format6 a b c c c d.

  Definition format (a b c : Set) : Set := format4 a b c c.

  Parameter string_of_format : βˆ€ {a b c d e f : Set},
    format6 a b c d e f β†’ string.

  Parameter format_of_string : βˆ€ {a b c d e f : Set},
    format6 a b c d e f β†’ format6 a b c d e f.

  Parameter op_caretcaret : βˆ€ {a b c d e f g h : Set},
    format6 a b c d e f β†’ format6 f b c e g h β†’ format6 a b c d g h.
End Pervasives_signature.
Require Export TezosOfOCaml.Environment.V7.Pervasives.
Module Pervasives_check : Pervasives_signature := Pervasives.

Module Type Either_signature.
  Inductive t (a b : Set) : Set :=
  | Left : a β†’ t a b
  | Right : b β†’ t a b.

  Arguments Left {_ _}.
  Arguments Right {_ _}.

  Parameter equal : βˆ€ {a b : Set},
    (a β†’ a β†’ bool) β†’ (b β†’ b β†’ bool) β†’ t a b β†’ t a b β†’ bool.

  Parameter compare : βˆ€ {a b : Set},
    (a β†’ a β†’ int) β†’ (b β†’ b β†’ int) β†’ t a b β†’ t a b β†’ int.
End Either_signature.
Require Export TezosOfOCaml.Environment.V7.Either.
Module Either_check : Either_signature := Either.

Module Type String_signature.
  Parameter length : string β†’ int.

  Parameter get : string β†’ int β†’ ascii.

  Parameter make : int β†’ ascii β†’ string.

  Parameter init_value : int β†’ (int β†’ ascii) β†’ string.

  Parameter sub : string β†’ int β†’ int β†’ string.

  Parameter blit : string β†’ int β†’ bytes β†’ int β†’ int β†’ unit.

  Parameter concat : string β†’ list string β†’ string.

  Parameter iter : (ascii β†’ unit) β†’ string β†’ unit.

  Parameter iteri : (int β†’ ascii β†’ unit) β†’ string β†’ unit.

  Parameter map : (ascii β†’ ascii) β†’ string β†’ string.

  Parameter mapi : (int β†’ ascii β†’ ascii) β†’ string β†’ string.

  Parameter trim : string β†’ string.

  Parameter escaped : string β†’ string.

  Parameter index_opt : string β†’ ascii β†’ option int.

  Parameter rindex_opt : string β†’ ascii β†’ option int.

  Parameter index_from_opt : string β†’ int β†’ ascii β†’ option int.

  Parameter rindex_from_opt : string β†’ int β†’ ascii β†’ option int.

  Parameter contains : string β†’ ascii β†’ bool.

  Parameter contains_from : string β†’ int β†’ ascii β†’ bool.

  Parameter rcontains_from : string β†’ int β†’ ascii β†’ bool.

  Parameter uppercase_ascii : string β†’ string.

  Parameter lowercase_ascii : string β†’ string.

  Parameter capitalize_ascii : string β†’ string.

  Parameter uncapitalize_ascii : string β†’ string.

  Definition t : Set := string.

  Parameter compare : t β†’ t β†’ int.

  Parameter equal : t β†’ t β†’ bool.

  Parameter split_on_char : ascii β†’ string β†’ list string.
End String_signature.
Require Export TezosOfOCaml.Environment.V7.String.
Module String_check : String_signature := String.

Module Type Char_signature.
  Parameter code : ascii β†’ int.

  Parameter chr : int β†’ ascii.

  Parameter escaped : ascii β†’ string.

  Parameter lowercase_ascii : ascii β†’ ascii.

  Parameter uppercase_ascii : ascii β†’ ascii.

  Definition t : Set := ascii.

  Parameter compare : t β†’ t β†’ int.

  Parameter equal : t β†’ t β†’ bool.
End Char_signature.
Require Export TezosOfOCaml.Environment.V7.Char.
Module Char_check : Char_signature := Char.

Module Type Bytes_signature.
  Parameter length : bytes β†’ int.

  Parameter get : bytes β†’ int β†’ ascii.

  Parameter set : bytes β†’ int β†’ ascii β†’ unit.

  Parameter make : int β†’ ascii β†’ bytes.

  Parameter init_value : int β†’ (int β†’ ascii) β†’ bytes.

  Parameter empty : bytes.

  Parameter copy : bytes β†’ bytes.

  Parameter of_string : string β†’ bytes.

  Parameter to_string : bytes β†’ string.

  Parameter sub : bytes β†’ int β†’ int β†’ bytes.

  Parameter sub_string : bytes β†’ int β†’ int β†’ string.

  Parameter extend : bytes β†’ int β†’ int β†’ bytes.

  Parameter fill : bytes β†’ int β†’ int β†’ ascii β†’ unit.

  Parameter blit : bytes β†’ int β†’ bytes β†’ int β†’ int β†’ unit.

  Parameter blit_string : string β†’ int β†’ bytes β†’ int β†’ int β†’ unit.

  Parameter concat : bytes β†’ list bytes β†’ bytes.

  Parameter cat : bytes β†’ bytes β†’ bytes.

  Parameter iter : (ascii β†’ unit) β†’ bytes β†’ unit.

  Parameter iteri : (int β†’ ascii β†’ unit) β†’ bytes β†’ unit.

  Parameter map : (ascii β†’ ascii) β†’ bytes β†’ bytes.

  Parameter mapi : (int β†’ ascii β†’ ascii) β†’ bytes β†’ bytes.

  Parameter trim : bytes β†’ bytes.

  Parameter escaped : bytes β†’ bytes.

  Parameter index_opt : bytes β†’ ascii β†’ option int.

  Parameter rindex_opt : bytes β†’ ascii β†’ option int.

  Parameter index_from_opt : bytes β†’ int β†’ ascii β†’ option int.

  Parameter rindex_from_opt : bytes β†’ int β†’ ascii β†’ option int.

  Parameter contains : bytes β†’ ascii β†’ bool.

  Parameter contains_from : bytes β†’ int β†’ ascii β†’ bool.

  Parameter rcontains_from : bytes β†’ int β†’ ascii β†’ bool.

  Parameter uppercase_ascii : bytes β†’ bytes.

  Parameter lowercase_ascii : bytes β†’ bytes.

  Parameter capitalize_ascii : bytes β†’ bytes.

  Parameter uncapitalize_ascii : bytes β†’ bytes.

  Definition t : Set := bytes.

  Parameter compare : t β†’ t β†’ int.

  Parameter equal : t β†’ t β†’ bool.
End Bytes_signature.
Require Export TezosOfOCaml.Environment.V7.Bytes.
Module Bytes_check : Bytes_signature := Bytes.

Module Type Int32_signature.
  Parameter zero : int32.

  Parameter one : int32.

  Parameter minus_one : int32.

  Parameter neg : int32 β†’ int32.

  Parameter add : int32 β†’ int32 β†’ int32.

  Parameter sub : int32 β†’ int32 β†’ int32.

  Parameter mul : int32 β†’ int32 β†’ int32.

  Parameter div : int32 β†’ int32 β†’ int32.

  Parameter rem : int32 β†’ int32 β†’ int32.

  Parameter succ : int32 β†’ int32.

  Parameter pred : int32 β†’ int32.

  Parameter abs : int32 β†’ int32.

  Parameter max_int : int32.

  Parameter min_int : int32.

  Parameter logand : int32 β†’ int32 β†’ int32.

  Parameter logor : int32 β†’ int32 β†’ int32.

  Parameter logxor : int32 β†’ int32 β†’ int32.

  Parameter lognot : int32 β†’ int32.

  Parameter shift_left : int32 β†’ int β†’ int32.

  Parameter shift_right : int32 β†’ int β†’ int32.

  Parameter shift_right_logical : int32 β†’ int β†’ int32.

  Parameter of_int : int β†’ int32.

  Parameter to_int : int32 β†’ int.

  Parameter of_string_opt : string β†’ option int32.

  Parameter to_string : int32 β†’ string.

  Definition t : Set := int32.

  Parameter compare : t β†’ t β†’ int.

  Parameter equal : t β†’ t β†’ bool.
End Int32_signature.
Require Export TezosOfOCaml.Environment.V7.Int32.
Module Int32_check : Int32_signature := Int32.

Module Type Int64_signature.
  Parameter zero : int64.

  Parameter one : int64.

  Parameter minus_one : int64.

  Parameter neg : int64 β†’ int64.

  Parameter add : int64 β†’ int64 β†’ int64.

  Parameter sub : int64 β†’ int64 β†’ int64.

  Parameter mul : int64 β†’ int64 β†’ int64.

  Parameter div : int64 β†’ int64 β†’ int64.

  Parameter rem : int64 β†’ int64 β†’ int64.

  Parameter succ : int64 β†’ int64.

  Parameter pred : int64 β†’ int64.

  Parameter abs : int64 β†’ int64.

  Parameter max_int : int64.

  Parameter min_int : int64.

  Parameter logand : int64 β†’ int64 β†’ int64.

  Parameter logor : int64 β†’ int64 β†’ int64.

  Parameter logxor : int64 β†’ int64 β†’ int64.

  Parameter lognot : int64 β†’ int64.

  Parameter shift_left : int64 β†’ int β†’ int64.

  Parameter shift_right : int64 β†’ int β†’ int64.

  Parameter shift_right_logical : int64 β†’ int β†’ int64.

  Parameter of_int : int β†’ int64.

  Parameter to_int : int64 β†’ int.

  Parameter of_int32 : int32 β†’ int64.

  Parameter to_int32 : int64 β†’ int32.

  Parameter of_string_opt : string β†’ option int64.

  Parameter to_string : int64 β†’ string.

  Definition t : Set := int64.

  Parameter compare : t β†’ t β†’ int.

  Parameter equal : t β†’ t β†’ bool.
End Int64_signature.
Require Export TezosOfOCaml.Environment.V7.Int64.
Module Int64_check : Int64_signature := Int64.

Module Type Format_signature.
  Parameter formatter : Set.

  Parameter pp_open_box : formatter β†’ int β†’ unit.

  Parameter pp_close_box : formatter β†’ unit β†’ unit.

  Parameter pp_open_hbox : formatter β†’ unit β†’ unit.

  Parameter pp_open_vbox : formatter β†’ int β†’ unit.

  Parameter pp_open_hvbox : formatter β†’ int β†’ unit.

  Parameter pp_open_hovbox : formatter β†’ int β†’ unit.

  Parameter pp_print_string : formatter β†’ string β†’ unit.

  Parameter pp_print_as : formatter β†’ int β†’ string β†’ unit.

  Parameter pp_print_int : formatter β†’ int β†’ unit.

  Parameter pp_print_char : formatter β†’ ascii β†’ unit.

  Parameter pp_print_bool : formatter β†’ bool β†’ unit.

  Parameter pp_print_space : formatter β†’ unit β†’ unit.

  Parameter pp_print_cut : formatter β†’ unit β†’ unit.

  Parameter pp_print_break : formatter β†’ int β†’ int β†’ unit.

  Parameter pp_print_custom_break :
    formatter β†’ string Γ— int Γ— string β†’ string Γ— int Γ— string β†’ unit.

  Parameter pp_force_newline : formatter β†’ unit β†’ unit.

  Parameter pp_print_if_newline : formatter β†’ unit β†’ unit.

  Parameter pp_print_flush : formatter β†’ unit β†’ unit.

  Parameter pp_print_newline : formatter β†’ unit β†’ unit.

  Parameter pp_set_margin : formatter β†’ int β†’ unit.

  Parameter pp_get_margin : formatter β†’ unit β†’ int.

  Parameter pp_set_max_indent : formatter β†’ int β†’ unit.

  Parameter pp_get_max_indent : formatter β†’ unit β†’ int.

  Parameter pp_set_max_boxes : formatter β†’ int β†’ unit.

  Parameter pp_get_max_boxes : formatter β†’ unit β†’ int.

  Parameter pp_over_max_boxes : formatter β†’ unit β†’ bool.

  Parameter pp_open_tbox : formatter β†’ unit β†’ unit.

  Parameter pp_close_tbox : formatter β†’ unit β†’ unit.

  Parameter pp_set_tab : formatter β†’ unit β†’ unit.

  Parameter pp_print_tab : formatter β†’ unit β†’ unit.

  Parameter pp_print_tbreak : formatter β†’ int β†’ int β†’ unit.

  Parameter pp_set_ellipsis_text : formatter β†’ string β†’ unit.

  Parameter pp_get_ellipsis_text : formatter β†’ unit β†’ string.

  Parameter pp_print_list : βˆ€ {a : Set},
    option (formatter β†’ unit β†’ unit) β†’ (formatter β†’ a β†’ unit) β†’
    formatter β†’ list a β†’ unit.

  Parameter pp_print_text : formatter β†’ string β†’ unit.

  Parameter pp_print_option : βˆ€ {a : Set},
    option (formatter β†’ unit β†’ unit) β†’ (formatter β†’ a β†’ unit) β†’
    formatter β†’ option a β†’ unit.

  Parameter pp_print_result : βˆ€ {a e : Set},
    (formatter β†’ a β†’ unit) β†’ (formatter β†’ e β†’ unit) β†’ formatter β†’
    Pervasives.result a e β†’ unit.

  Parameter fprintf : βˆ€ {a : Set},
    formatter β†’ Pervasives.format a formatter unit β†’ a.

  Parameter sprintf : βˆ€ {a : Set}, Pervasives.format a unit string β†’ a.

  Parameter asprintf : βˆ€ {a : Set},
    Pervasives.format4 a formatter unit string β†’ a.

  Parameter dprintf : βˆ€ {a : Set},
    Pervasives.format4 a formatter unit (formatter β†’ unit) β†’ a.

  Parameter ifprintf : βˆ€ {a : Set},
    formatter β†’ Pervasives.format a formatter unit β†’ a.

  Parameter kfprintf : βˆ€ {a b : Set},
    (formatter β†’ a) β†’ formatter β†’ Pervasives.format4 b formatter unit a β†’ b.

  Parameter kdprintf : βˆ€ {a b : Set},
    ((formatter β†’ unit) β†’ a) β†’ Pervasives.format4 b formatter unit a β†’ b.

  Parameter ikfprintf : βˆ€ {a b : Set},
    (formatter β†’ a) β†’ formatter β†’ Pervasives.format4 b formatter unit a β†’ b.

  Parameter ksprintf : βˆ€ {a b : Set},
    (string β†’ a) β†’ Pervasives.format4 b unit string a β†’ b.

  Parameter kasprintf : βˆ€ {a b : Set},
    (string β†’ a) β†’ Pervasives.format4 b formatter unit a β†’ b.
End Format_signature.
Require Export TezosOfOCaml.Environment.V7.Format.
Module Format_check : Format_signature := Format.

Module Type Logging_signature.
  Inductive level : Set :=
  | Debug : level
  | Info : level
  | Notice : level
  | Warning : level
  | Error : level
  | Fatal : level.

  Parameter log : βˆ€ {a : Set},
    level β†’ Pervasives.format4 a Format.formatter unit unit β†’ a.

  Parameter log_string : level β†’ string β†’ unit.
End Logging_signature.
Require Export TezosOfOCaml.Environment.V7.Logging.
Module Logging_check : Logging_signature := Logging.

Module Type Hex_signature.
  Inductive t : Set :=
  | Hex : string β†’ t.

  Parameter of_char : ascii β†’ ascii Γ— ascii.

  Parameter to_char : ascii β†’ ascii β†’ option ascii.

  Parameter of_string : option (list ascii) β†’ string β†’ t.

  Parameter to_string : t β†’ option string.

  Parameter of_bytes : option (list ascii) β†’ bytes β†’ t.

  Parameter to_bytes : t β†’ option bytes.

  Parameter hexdump_s : option bool β†’ option bool β†’ t β†’ string.

  Parameter pp : Format.formatter β†’ t β†’ unit.

  Parameter show : t β†’ string.
End Hex_signature.
Require Export TezosOfOCaml.Environment.V7.Hex.
Module Hex_check : Hex_signature := Hex.

Module Type Z_signature.
  Parameter t : Set.

  Parameter zero : t.

  Parameter one : t.

  Parameter minus_one : t.

  Parameter of_int : int β†’ t.

  Parameter of_int32 : int32 β†’ t.

  Parameter of_int64 : int64 β†’ t.

  Parameter of_string : string β†’ t.

  Parameter of_substring : string β†’ int β†’ int β†’ t.

  Parameter of_string_base : int β†’ string β†’ t.

  Parameter of_substring_base : int β†’ string β†’ int β†’ int β†’ t.

  Parameter succ : t β†’ t.

  Parameter pred : t β†’ t.

  Parameter abs : t β†’ t.

  Parameter neg : t β†’ t.

  Parameter add : t β†’ t β†’ t.

  Parameter sub : t β†’ t β†’ t.

  Parameter mul : t β†’ t β†’ t.

  Parameter div : t β†’ t β†’ t.

  Parameter rem : t β†’ t β†’ t.

  Parameter div_rem : t β†’ t β†’ t Γ— t.

  Parameter cdiv : t β†’ t β†’ t.

  Parameter fdiv : t β†’ t β†’ t.

  Parameter ediv_rem : t β†’ t β†’ t Γ— t.

  Parameter ediv : t β†’ t β†’ t.

  Parameter erem : t β†’ t β†’ t.

  Parameter divexact : t β†’ t β†’ t.

  Parameter divisible : t β†’ t β†’ bool.

  Parameter congruent : t β†’ t β†’ t β†’ bool.

  Parameter logand : t β†’ t β†’ t.

  Parameter logor : t β†’ t β†’ t.

  Parameter logxor : t β†’ t β†’ t.

  Parameter lognot : t β†’ t.

  Parameter shift_left : t β†’ int β†’ t.

  Parameter shift_right : t β†’ int β†’ t.

  Parameter shift_right_trunc : t β†’ int β†’ t.

  Parameter numbits : t β†’ int.

  Parameter trailing_zeros : t β†’ int.

  Parameter testbit : t β†’ int β†’ bool.

  Parameter popcount : t β†’ int.

  Parameter hamdist : t β†’ t β†’ int.

  Parameter to_int : t β†’ int.

  Parameter to_int32 : t β†’ int32.

  Parameter to_int64 : t β†’ int64.

  Parameter to_string : t β†’ string.

  Parameter format : string β†’ t β†’ string.

  Parameter fits_int : t β†’ bool.

  Parameter fits_int32 : t β†’ bool.

  Parameter fits_int64 : t β†’ bool.

  Parameter pp_print : Format.formatter β†’ t β†’ unit.

  Parameter compare : t β†’ t β†’ int.

  Parameter equal : t β†’ t β†’ bool.

  Parameter leq : t β†’ t β†’ bool.

  Parameter geq : t β†’ t β†’ bool.

  Parameter lt : t β†’ t β†’ bool.

  Parameter gt : t β†’ t β†’ bool.

  Parameter sign : t β†’ int.

  Parameter min : t β†’ t β†’ t.

  Parameter max : t β†’ t β†’ t.

  Parameter is_even : t β†’ bool.

  Parameter is_odd : t β†’ bool.

  Parameter pow : t β†’ int β†’ t.

  Parameter sqrt : t β†’ t.

  Parameter sqrt_rem : t β†’ t Γ— t.

  Parameter root_value : t β†’ int β†’ t.

  Parameter rootrem : t β†’ int β†’ t Γ— t.

  Parameter perfect_power : t β†’ bool.

  Parameter perfect_square : t β†’ bool.

  Parameter log2 : t β†’ int.

  Parameter log2up : t β†’ int.

  Parameter size_value : t β†’ int.

  Parameter extract : t β†’ int β†’ int β†’ t.

  Parameter signed_extract : t β†’ int β†’ int β†’ t.

  Parameter to_bits : t β†’ string.

  Parameter of_bits : string β†’ t.
End Z_signature.
Require Export TezosOfOCaml.Environment.V7.Z.
Module Z_check : Z_signature := Z.

Module Type Q_signature.
  Module t.
    Record record : Set := Build {
      num : Z.t;
      den : Z.t;
    }.
    Definition with_num num (r : record) :=
      Build num r.(den).
    Definition with_den den (r : record) :=
      Build r.(num) den.
  End t.
  Definition t := t.record.

  Parameter make : Z.t β†’ Z.t β†’ t.

  Parameter zero : t.

  Parameter one : t.

  Parameter minus_one : t.

  Parameter inf : t.

  Parameter minus_inf : t.

  Parameter undef : t.

  Parameter of_bigint : Z.t β†’ t.

  Parameter of_int : int β†’ t.

  Parameter of_int32 : int32 β†’ t.

  Parameter of_int64 : int64 β†’ t.

  Parameter of_ints : int β†’ int β†’ t.

  Parameter of_string : string β†’ t.

  Parameter num : t β†’ Z.t.

  Parameter den : t β†’ Z.t.

  Inductive kind : Set :=
  | ZERO : kind
  | INF : kind
  | MINF : kind
  | UNDEF : kind
  | NZERO : kind.

  Parameter classify : t β†’ kind.

  Parameter is_real : t β†’ bool.

  Parameter sign : t β†’ int.

  Parameter compare : t β†’ t β†’ int.

  Parameter equal : t β†’ t β†’ bool.

  Parameter min : t β†’ t β†’ t.

  Parameter max : t β†’ t β†’ t.

  Parameter leq : t β†’ t β†’ bool.

  Parameter geq : t β†’ t β†’ bool.

  Parameter lt : t β†’ t β†’ bool.

  Parameter gt : t β†’ t β†’ bool.

  Parameter to_bigint : t β†’ Z.t.

  Parameter to_int : t β†’ int.

  Parameter to_int32 : t β†’ int32.

  Parameter to_int64 : t β†’ int64.

  Parameter to_string : t β†’ string.

  Parameter neg : t β†’ t.

  Parameter abs : t β†’ t.

  Parameter add : t β†’ t β†’ t.

  Parameter sub : t β†’ t β†’ t.

  Parameter mul : t β†’ t β†’ t.

  Parameter inv : t β†’ t.

  Parameter div : t β†’ t β†’ t.

  Parameter mul_2exp : t β†’ int β†’ t.

  Parameter div_2exp : t β†’ int β†’ t.

  Parameter pp_print : Format.formatter β†’ t β†’ unit.

  Parameter op_tildeminus : t β†’ t.

  Parameter op_tildeplus : t β†’ t.

  Parameter op_plus : t β†’ t β†’ t.

  Parameter op_minus : t β†’ t β†’ t.

  Parameter op_star : t β†’ t β†’ t.

  Parameter op_div : t β†’ t β†’ t.

  Parameter lsl : t β†’ int β†’ t.

  Parameter asr : t β†’ int β†’ t.

  Parameter op_tildedollar : int β†’ t.

  Parameter op_divdiv : int β†’ int β†’ t.

  Parameter op_tildedollardollar : Z.t β†’ t.

  Parameter op_divdivdiv : Z.t β†’ Z.t β†’ t.

  Parameter op_eq : t β†’ t β†’ bool.

  Parameter op_lt : t β†’ t β†’ bool.

  Parameter op_gt : t β†’ t β†’ bool.

  Parameter op_lteq : t β†’ t β†’ bool.

  Parameter op_gteq : t β†’ t β†’ bool.

  Parameter op_ltgt : t β†’ t β†’ bool.
End Q_signature.
Require Export TezosOfOCaml.Environment.V7.Q.
Module Q_check : Q_signature := Q.

Module Type Lwt_signature.
  Parameter t : βˆ€ (a : Set), Set.

  Parameter _return : βˆ€ {a : Set}, a β†’ t a.

  Parameter bind : βˆ€ {a b : Set}, t a β†’ (a β†’ t b) β†’ t b.

  Parameter map : βˆ€ {a b : Set}, (a β†’ b) β†’ t a β†’ t b.

  Parameter return_unit : t unit.

  Parameter return_none : βˆ€ {A : Set}, t (option A).

  Parameter return_nil : βˆ€ {A : Set}, t (list A).

  Parameter return_true : t bool.

  Parameter return_false : t bool.

  Parameter return_some : βˆ€ {a : Set}, a β†’ t (option a).

  Parameter return_ok : βˆ€ {B a : Set}, a β†’ t (Pervasives.result a B).

  Parameter return_error : βˆ€ {B e : Set}, e β†’ t (Pervasives.result B e).
End Lwt_signature.
(* We do not implement the Lwt module, as it is the identity monad for us since
   the protocol code is sequential and interactions with the store can be
   implemented in a purely functional way. *)


Module Type Data_encoding_signature.
  Inductive json : Set :=
  | Bool : bool β†’ json
  | Null : json
  | O : list (string Γ— json) β†’ json
  | Float : float β†’ json
  | String : string β†’ json
  | A : list json β†’ json.

  Inductive tag_size : Set :=
  | Uint16 : tag_size
  | Uint8 : tag_size.

  Parameter json_schema : Set.

  Parameter t : βˆ€ (a : Set), Set.

  Definition encoding (a : Set) : Set := t a.

  Parameter classify : βˆ€ {a : Set}, encoding a β†’ Variant.t.

  Parameter null : encoding unit.

  Parameter empty : encoding unit.

  Parameter unit_value : encoding unit.

  Parameter constant : string β†’ encoding unit.

  Parameter int8 : encoding int.

  Parameter uint8 : encoding int.

  Parameter int16 : encoding int.

  Parameter uint16 : encoding int.

  Parameter int31 : encoding int.

  Parameter int32_value : encoding int32.

  Parameter int64_value : encoding int64.

  Parameter ranged_int : int β†’ int β†’ encoding int.

  Parameter z_value : encoding Z.t.

  Parameter n_value : encoding Z.t.

  Parameter bool_value : encoding bool.

  Parameter string_value : encoding string.

  Parameter bytes_value : encoding Bytes.t.

  Parameter option_value : βˆ€ {a : Set}, encoding a β†’ encoding (option a).

  Parameter result_value : βˆ€ {a b : Set},
    encoding a β†’ encoding b β†’ encoding (Pervasives.result a b).

  Parameter list_value : βˆ€ {a : Set},
    option int β†’ encoding a β†’ encoding (list a).

  Parameter conv : βˆ€ {a b : Set},
    (a β†’ b) β†’ (b β†’ a) β†’ option json_schema β†’ encoding b β†’ encoding a.

  Parameter conv_with_guard : βˆ€ {a b : Set},
    (a β†’ b) β†’ (b β†’ Pervasives.result a string) β†’ option json_schema β†’
    encoding b β†’ encoding a.

  Parameter with_decoding_guard : βˆ€ {a : Set},
    (a β†’ Pervasives.result unit string) β†’ encoding a β†’ encoding a.

  Parameter assoc : βˆ€ {a : Set},
    encoding a β†’ encoding (list (string Γ— a)).

  Parameter field : βˆ€ (a : Set), Set.

  Parameter req : βˆ€ {t : Set},
    option string β†’ option string β†’ string β†’ encoding t β†’ field t.

  Parameter opt : βˆ€ {t : Set},
    option string β†’ option string β†’ string β†’ encoding t β†’ field (option t).

  Parameter varopt : βˆ€ {t : Set},
    option string β†’ option string β†’ string β†’ encoding t β†’ field (option t).

  Parameter dft : βˆ€ {t : Set},
    option string β†’ option string β†’ string β†’ encoding t β†’ t β†’ field t.

  Parameter obj1 : βˆ€ {f1 : Set}, field f1 β†’ encoding f1.

  Parameter obj2 : βˆ€ {f1 f2 : Set},
    field f1 β†’ field f2 β†’ encoding (f1 Γ— f2).

  Parameter obj3 : βˆ€ {f1 f2 f3 : Set},
    field f1 β†’ field f2 β†’ field f3 β†’ encoding (f1 Γ— f2 Γ— f3).

  Parameter obj4 : βˆ€ {f1 f2 f3 f4 : Set},
    field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ encoding (f1 Γ— f2 Γ— f3 Γ— f4).

  Parameter obj5 : βˆ€ {f1 f2 f3 f4 f5 : Set},
    field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’
    encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5).

  Parameter obj6 : βˆ€ {f1 f2 f3 f4 f5 f6 : Set},
    field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
    encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6).

  Parameter obj7 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 : Set},
    field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
    field f7 β†’ encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7).

  Parameter obj8 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 f8 : Set},
    field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
    field f7 β†’ field f8 β†’ encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8).

  Parameter obj9 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
    field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
    field f7 β†’ field f8 β†’ field f9 β†’
    encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8 Γ— f9).

  Parameter obj10 : βˆ€ {f1 f10 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
    field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
    field f7 β†’ field f8 β†’ field f9 β†’ field f10 β†’
    encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8 Γ— f9 Γ— f10).

  Parameter merge_objs : βˆ€ {o1 o2 : Set},
    encoding o1 β†’ encoding o2 β†’ encoding (o1 Γ— o2).

  Parameter tup1 : βˆ€ {f1 : Set}, encoding f1 β†’ encoding f1.

  Parameter tup2 : βˆ€ {f1 f2 : Set},
    encoding f1 β†’ encoding f2 β†’ encoding (f1 Γ— f2).

  Parameter tup3 : βˆ€ {f1 f2 f3 : Set},
    encoding f1 β†’ encoding f2 β†’ encoding f3 β†’ encoding (f1 Γ— f2 Γ— f3).

  Parameter tup4 : βˆ€ {f1 f2 f3 f4 : Set},
    encoding f1 β†’ encoding f2 β†’ encoding f3 β†’ encoding f4 β†’
    encoding (f1 Γ— f2 Γ— f3 Γ— f4).

  Parameter tup5 : βˆ€ {f1 f2 f3 f4 f5 : Set},
    encoding f1 β†’ encoding f2 β†’ encoding f3 β†’ encoding f4 β†’ encoding f5 β†’
    encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5).

  Parameter tup6 : βˆ€ {f1 f2 f3 f4 f5 f6 : Set},
    encoding f1 β†’ encoding f2 β†’ encoding f3 β†’ encoding f4 β†’ encoding f5 β†’
    encoding f6 β†’ encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6).

  Parameter tup7 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 : Set},
    encoding f1 β†’ encoding f2 β†’ encoding f3 β†’ encoding f4 β†’ encoding f5 β†’
    encoding f6 β†’ encoding f7 β†’ encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7).

  Parameter tup8 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 f8 : Set},
    encoding f1 β†’ encoding f2 β†’ encoding f3 β†’ encoding f4 β†’ encoding f5 β†’
    encoding f6 β†’ encoding f7 β†’ encoding f8 β†’
    encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8).

  Parameter tup9 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
    encoding f1 β†’ encoding f2 β†’ encoding f3 β†’ encoding f4 β†’ encoding f5 β†’
    encoding f6 β†’ encoding f7 β†’ encoding f8 β†’ encoding f9 β†’
    encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8 Γ— f9).

  Parameter tup10 : βˆ€ {f1 f10 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
    encoding f1 β†’ encoding f2 β†’ encoding f3 β†’ encoding f4 β†’ encoding f5 β†’
    encoding f6 β†’ encoding f7 β†’ encoding f8 β†’ encoding f9 β†’ encoding f10 β†’
    encoding (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8 Γ— f9 Γ— f10).

  Parameter merge_tups : βˆ€ {a1 a2 : Set},
    encoding a1 β†’ encoding a2 β†’ encoding (a1 Γ— a2).

  Parameter case : βˆ€ (t : Set), Set.

  Inductive case_tag : Set :=
  | Tag : int β†’ case_tag
  | Json_only : case_tag.

  Parameter match_result : Set.

  Definition matching_function (a : Set) : Set := a β†’ match_result.

  Parameter matched : βˆ€ {a : Set},
    option Variant.t β†’ int β†’ encoding a β†’ a β†’ match_result.

  Parameter case_value : βˆ€ {a t : Set},
    string β†’ option string β†’ case_tag β†’ encoding a β†’ (t β†’ option a) β†’
    (a β†’ t) β†’ case t.

  Parameter matching : βˆ€ {t : Set},
    option Variant.t β†’ matching_function t β†’ list (case t) β†’ encoding t.

  Parameter union : βˆ€ {t : Set},
    option Variant.t β†’ list (case t) β†’ encoding t.

  Parameter string_enum : βˆ€ {a : Set}, list (string Γ— a) β†’ encoding a.

  Module Fixed.
    Parameter string_value : int β†’ encoding string.

    Parameter bytes_value : int β†’ encoding bytes.

    Parameter add_padding : βˆ€ {a : Set}, encoding a β†’ int β†’ encoding a.

    Parameter list_value : βˆ€ {a : Set},
      int β†’ encoding a β†’ encoding (list a).

    Parameter array_value : βˆ€ {a : Set},
      int β†’ encoding a β†’ encoding (array a).
  End Fixed.

  Module _Variable.
    Parameter string_value : encoding string.

    Parameter bytes_value : encoding bytes.

    Parameter array_value : βˆ€ {a : Set},
      option int β†’ encoding a β†’ encoding (array a).

    Parameter list_value : βˆ€ {a : Set},
      option int β†’ encoding a β†’ encoding (list a).
  End _Variable.

  Module Bounded.
    Parameter string_value : int β†’ encoding string.

    Parameter bytes_value : int β†’ encoding bytes.
  End Bounded.

  Parameter dynamic_size : βˆ€ {a : Set},
    option Variant.t β†’ encoding a β†’ encoding a.

  Parameter check_size : βˆ€ {a : Set}, int β†’ encoding a β†’ encoding a.

  Parameter splitted : βˆ€ {a : Set}, encoding a β†’ encoding a β†’ encoding a.

  Parameter mu : βˆ€ {a : Set},
    string β†’ option string β†’ option string β†’ (encoding a β†’ encoding a) β†’
    encoding a.

  Parameter def : βˆ€ {t : Set},
    string β†’ option string β†’ option string β†’ encoding t β†’ encoding t.

  Parameter lazy_t : βˆ€ (a : Set), Set.

  Parameter lazy_encoding : βˆ€ {a : Set}, encoding a β†’ encoding (lazy_t a).

  Parameter force_decode : βˆ€ {a : Set}, lazy_t a β†’ option a.

  Parameter force_bytes : βˆ€ {a : Set}, lazy_t a β†’ bytes.

  Parameter make_lazy : βˆ€ {a : Set}, encoding a β†’ a β†’ lazy_t a.

  Parameter apply_lazy : βˆ€ {a b : Set},
    (a β†’ b) β†’ (bytes β†’ b) β†’ (b β†’ b β†’ b) β†’ lazy_t a β†’ b.

  Module Compact.
    Parameter t : βˆ€ (a : Set), Set.

    Parameter make : βˆ€ {a : Set}, option Variant.t β†’ t a β†’ encoding a.

    Parameter tag_bit_count : βˆ€ {a : Set}, t a β†’ int.

    Parameter void : Set.

    Parameter void_value : t void.

    Parameter refute : βˆ€ {a : Set}, void β†’ a.

    Parameter unit_value : t unit.

    Parameter bool_value : t bool.

    Parameter payload : βˆ€ {a : Set}, encoding a β†’ t a.

    Parameter option_value : βˆ€ {a : Set}, t a β†’ t (option a).

    Parameter conv : βˆ€ {a b : Set},
      option (encoding a) β†’ (a β†’ b) β†’ (b β†’ a) β†’ t b β†’ t a.

    Parameter tup1 : βˆ€ {a : Set}, t a β†’ t a.

    Parameter tup2 : βˆ€ {a b : Set}, t a β†’ t b β†’ t (a Γ— b).

    Parameter tup3 : βˆ€ {a b c : Set}, t a β†’ t b β†’ t c β†’ t (a Γ— b Γ— c).

    Parameter tup4 : βˆ€ {a b c d : Set},
      t a β†’ t b β†’ t c β†’ t d β†’ t (a Γ— b Γ— c Γ— d).

    Parameter tup5 : βˆ€ {f1 f2 f3 f4 f5 : Set},
      t f1 β†’ t f2 β†’ t f3 β†’ t f4 β†’ t f5 β†’ t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5).

    Parameter tup6 : βˆ€ {f1 f2 f3 f4 f5 f6 : Set},
      t f1 β†’ t f2 β†’ t f3 β†’ t f4 β†’ t f5 β†’ t f6 β†’
      t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6).

    Parameter tup7 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 : Set},
      t f1 β†’ t f2 β†’ t f3 β†’ t f4 β†’ t f5 β†’ t f6 β†’ t f7 β†’
      t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7).

    Parameter tup8 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 f8 : Set},
      t f1 β†’ t f2 β†’ t f3 β†’ t f4 β†’ t f5 β†’ t f6 β†’ t f7 β†’ t f8 β†’
      t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8).

    Parameter tup9 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
      t f1 β†’ t f2 β†’ t f3 β†’ t f4 β†’ t f5 β†’ t f6 β†’ t f7 β†’ t f8 β†’ t f9 β†’
      t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8 Γ— f9).

    Parameter tup10 : βˆ€ {f1 f10 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
      t f1 β†’ t f2 β†’ t f3 β†’ t f4 β†’ t f5 β†’ t f6 β†’ t f7 β†’ t f8 β†’ t f9 β†’
      t f10 β†’ t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8 Γ— f9 Γ— f10).

    Parameter field : βˆ€ (a : Set), Set.

    Parameter req : βˆ€ {a : Set}, string β†’ t a β†’ field a.

    Parameter opt : βˆ€ {a : Set}, string β†’ t a β†’ field (option a).

    Parameter obj1 : βˆ€ {a : Set}, field a β†’ t a.

    Parameter obj2 : βˆ€ {a b : Set}, field a β†’ field b β†’ t (a Γ— b).

    Parameter obj3 : βˆ€ {a b c : Set},
      field a β†’ field b β†’ field c β†’ t (a Γ— b Γ— c).

    Parameter obj4 : βˆ€ {a b c d : Set},
      field a β†’ field b β†’ field c β†’ field d β†’ t (a Γ— b Γ— c Γ— d).

    Parameter obj5 : βˆ€ {f1 f2 f3 f4 f5 : Set},
      field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’
      t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5).

    Parameter obj6 : βˆ€ {f1 f2 f3 f4 f5 f6 : Set},
      field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
      t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6).

    Parameter obj7 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 : Set},
      field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
      field f7 β†’ t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7).

    Parameter obj8 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 f8 : Set},
      field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
      field f7 β†’ field f8 β†’ t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8).

    Parameter obj9 : βˆ€ {f1 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
      field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
      field f7 β†’ field f8 β†’ field f9 β†’
      t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8 Γ— f9).

    Parameter obj10 : βˆ€ {f1 f10 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
      field f1 β†’ field f2 β†’ field f3 β†’ field f4 β†’ field f5 β†’ field f6 β†’
      field f7 β†’ field f8 β†’ field f9 β†’ field f10 β†’
      t (f1 Γ— f2 Γ— f3 Γ— f4 Γ— f5 Γ— f6 Γ— f7 Γ— f8 Γ— f9 Γ— f10).

    Parameter int32_value : t int32.

    Parameter int64_value : t int64.

    Parameter list_value : βˆ€ {a : Set}, int β†’ encoding a β†’ t (list a).

    Parameter case : βˆ€ (a : Set), Set.

    Parameter case_value : βˆ€ {a b : Set},
      string β†’ option string β†’ t b β†’ (a β†’ option b) β†’ (b β†’ a) β†’ case a.

    Parameter union : βˆ€ {a : Set},
      option int β†’ option int β†’ list (case a) β†’ t a.

    Parameter void_case : βˆ€ {a : Set}, string β†’ case a.

    Parameter or_int32 : βˆ€ {a : Set},
      string β†’ string β†’ option string β†’ encoding a β†’ t (Either.t int32 a).

    Module Custom.
      Definition tag : Set := int.

      Parameter join_tags : list (tag Γ— int) β†’ tag.

      Module S.
        Record signature {input layout : Set} : Set := {
          
The type of [input] this module allows to encode.
          input := input;
          
The various ways to efficiently encode [input].
          layout := layout;
          
The list of layouts available to encode [input].
          layouts : list layout;
          
The number of bits necessary to distinguish between the various layouts.
          tag_len : int;
          
[tag layout] computes the tag of {!Data_encoding.union} to be used to encode values classified as [layout].
{b Warning:} It is expected that [tag layout < 2^tag_len - 1].
          tag : layout β†’ tag;
          
[partial_encoding layout] returns the encoding to use for values classified as [layout].
This encoding can be partial in the sense that it may fail (it will raise an [Invalid_argument]) for some values of [x]. However, it is expected that [partial_encoding (classify x) x] will always succeed.
          partial_encoding : layout β†’ encoding input;
          
[classify x] returns the layout to be used to encode [x].
          classify : input β†’ layout;
          
The encoding to use when targeting a JSON output.
          json_encoding : encoding input;
        }.
      End S.
      Definition S := @S.signature.
      Arguments S {_ _}.

      Parameter make : βˆ€ {a : Set},
        {layout : Set @ S (input := a) (layout := layout)} β†’ t a.
    End Custom.
  End Compact.

  Definition compact (a : Set) : Set := Compact.t a.

  Parameter json_value : encoding json.

  Parameter json_schema_value : encoding json_schema.

  Module Json.
    Parameter schema : βˆ€ {a : Set},
      option string β†’ encoding a β†’ json_schema.

    Parameter construct : βˆ€ {t : Set},
      option Variant.t β†’ encoding t β†’ t β†’ json.

    Parameter destruct : βˆ€ {t : Set},
      option bool β†’ encoding t β†’ json β†’ t.

    Reserved Notation "'path".

    Inductive path_item : Set :=
    | Index : int β†’ path_item
    | Field : string β†’ path_item
    | Next : path_item
    | Star : path_item
    
    where "'path" := (list path_item).

    Definition path := 'path.

    Parameter print_error :
      option (Format.formatter β†’ extensible_type β†’ unit) β†’
      Format.formatter β†’ extensible_type β†’ unit.

    Parameter cannot_destruct : βˆ€ {a b : Set},
      Pervasives.format4 a Format.formatter unit b β†’ a.

    Parameter wrap_error : βˆ€ {a b : Set}, (a β†’ b) β†’ a β†’ b.

    Parameter pp : Format.formatter β†’ json β†’ unit.
  End Json.

  Module Binary.
    Parameter length : βˆ€ {a : Set}, encoding a β†’ a β†’ int.

    Parameter fixed_length : βˆ€ {a : Set}, encoding a β†’ option int.

    Parameter maximum_length : βˆ€ {a : Set}, encoding a β†’ option int.

    Parameter of_bytes_opt : βˆ€ {a : Set}, encoding a β†’ bytes β†’ option a.

    Parameter of_string_opt : βˆ€ {a : Set},
      encoding a β†’ string β†’ option a.

    Parameter to_bytes_opt : βˆ€ {a : Set},
      option int β†’ encoding a β†’ a β†’ option bytes.

    Parameter to_bytes_exn : βˆ€ {a : Set},
      option int β†’ encoding a β†’ a β†’ bytes.

    Parameter to_string_opt : βˆ€ {a : Set},
      option int β†’ encoding a β†’ a β†’ option string.

    Parameter to_string_exn : βˆ€ {a : Set},
      option int β†’ encoding a β†’ a β†’ string.
  End Binary.
End Data_encoding_signature.
Require Export TezosOfOCaml.Environment.V7.Data_encoding.
Module Data_encoding_check : Data_encoding_signature := Data_encoding.

Module Type Raw_hashes_signature.
  Parameter blake2b : bytes β†’ bytes.

  Parameter sha256 : bytes β†’ bytes.

  Parameter sha512 : bytes β†’ bytes.

  Parameter keccak256 : bytes β†’ bytes.

  Parameter sha3_256 : bytes β†’ bytes.

  Parameter sha3_512 : bytes β†’ bytes.
End Raw_hashes_signature.
Require Export TezosOfOCaml.Environment.V7.Raw_hashes.
Module Raw_hashes_check : Raw_hashes_signature := Raw_hashes.

Module Type Compare_signature.
  Module COMPARABLE.
    Record signature {t : Set} : Set := {
      t := t;
      compare : t β†’ t β†’ int;
    }.
  End COMPARABLE.
  Definition COMPARABLE := @COMPARABLE.signature.
  Arguments COMPARABLE {_}.

  Module S.
    Record signature {t : Set} : Set := {
      t := t;
      
[x = y] iff [compare x y = 0]
      op_eq : t β†’ t β†’ bool;
      
[x <> y] iff [compare x y <> 0]
      op_ltgt : t β†’ t β†’ bool;
      
[x < y] iff [compare x y < 0]
      op_lt : t β†’ t β†’ bool;
      
[x <= y] iff [compare x y <= 0]
      op_lteq : t β†’ t β†’ bool;
      
[x >= y] iff [compare x y >= 0]
      op_gteq : t β†’ t β†’ bool;
      
[x > y] iff [compare x y > 0]
      op_gt : t β†’ t β†’ bool;
      
[compare] an alias for the functor parameter's [compare] function
      compare : t β†’ t β†’ int;
      
[equal x y] iff [compare x y = 0]
      equal : t β†’ t β†’ bool;
      
[max x y] is [x] if [x >= y] otherwise it is [y]
      max : t β†’ t β†’ t;
      
[min x y] is [x] if [x <= y] otherwise it is [y]
      min : t β†’ t β†’ t;
    }.
  End S.
  Definition S := @S.signature.
  Arguments S {_}.

  Parameter Make :
    βˆ€ {P_t : Set},
    βˆ€ (P : COMPARABLE (t := P_t)), S (t := P.(COMPARABLE.t)).

  Parameter Char : S (t := ascii).

  Parameter Bool : S (t := bool).

  Module Int.
    Definition t : Set := int.

    Parameter op_eq : int β†’ int β†’ bool.

    Parameter op_ltgt : int β†’ int β†’ bool.

    Parameter op_lt : int β†’ int β†’ bool.

    Parameter op_gt : int β†’ int β†’ bool.

    Parameter op_lteq : int β†’ int β†’ bool.

    Parameter op_gteq : int β†’ int β†’ bool.

    Parameter compare : int β†’ int β†’ int.

    Parameter max : int β†’ int β†’ int.

    Parameter min : int β†’ int β†’ int.

    Parameter equal : int β†’ int β†’ bool.
  End Int.

  Parameter Int32 : S (t := int32).

  Parameter Uint32 : S (t := int32).

  Parameter Int64 : S (t := int64).

  Parameter Uint64 : S (t := int64).

  Parameter String : S (t := string).

  Parameter Bytes : S (t := bytes).

  Parameter Z : S (t := Z.t).

  Parameter Q : S (t := Q.t).

  Parameter List :
    βˆ€ {P_t : Set},
    βˆ€ (P : COMPARABLE (t := P_t)), S (t := list P.(COMPARABLE.t)).

  Parameter Option :
    βˆ€ {P_t : Set},
    βˆ€ (P : COMPARABLE (t := P_t)), S (t := option P.(COMPARABLE.t)).

  Parameter Result :
    βˆ€ {Ok_t Error_t : Set},
    βˆ€ (Ok : COMPARABLE (t := Ok_t)),
    βˆ€ (Error : COMPARABLE (t := Error_t)),
    S (t := Pervasives.result Ok.(COMPARABLE.t) Error.(COMPARABLE.t)).

  Module List_length_with.
    Parameter op_eq : βˆ€ {a : Set}, list a β†’ int β†’ bool.

    Parameter op_ltgt : βˆ€ {a : Set}, list a β†’ int β†’ bool.

    Parameter op_lt : βˆ€ {a : Set}, list a β†’ int β†’ bool.

    Parameter op_lteq : βˆ€ {a : Set}, list a β†’ int β†’ bool.

    Parameter op_gteq : βˆ€ {a : Set}, list a β†’ int β†’ bool.

    Parameter op_gt : βˆ€ {a : Set}, list a β†’ int β†’ bool.

    Parameter compare : βˆ€ {a : Set}, list a β†’ int β†’ int.

    Parameter equal : βˆ€ {a : Set}, list a β†’ int β†’ bool.
  End List_length_with.

  Module List_lengths.
    Parameter op_eq : βˆ€ {a b : Set}, list a β†’ list b β†’ bool.

    Parameter op_ltgt : βˆ€ {a b : Set}, list a β†’ list b β†’ bool.

    Parameter op_lt : βˆ€ {a b : Set}, list a β†’ list b β†’ bool.

    Parameter op_lteq : βˆ€ {a b : Set}, list a β†’ list b β†’ bool.

    Parameter op_gteq : βˆ€ {a b : Set}, list a β†’ list b β†’ bool.

    Parameter op_gt : βˆ€ {a b : Set}, list a β†’ list b β†’ bool.

    Parameter compare : βˆ€ {a b : Set}, list a β†’ list b β†’ int.

    Parameter equal : βˆ€ {a b : Set}, list a β†’ list b β†’ bool.
  End List_lengths.

  Parameter or_else : int β†’ (unit β†’ int) β†’ int.
End Compare_signature.
Require Export TezosOfOCaml.Environment.V7.Compare.
Module Compare_check : Compare_signature := Compare.

Module Type Time_signature.
  Parameter t : Set.

  Parameter Included_S : Compare.S (t := t).

  Definition op_eq : t β†’ t β†’ bool := Included_S.(Compare.S.op_eq).

  Definition op_ltgt : t β†’ t β†’ bool := Included_S.(Compare.S.op_ltgt).

  Definition op_lt : t β†’ t β†’ bool := Included_S.(Compare.S.op_lt).

  Definition op_lteq : t β†’ t β†’ bool := Included_S.(Compare.S.op_lteq).

  Definition op_gteq : t β†’ t β†’ bool := Included_S.(Compare.S.op_gteq).

  Definition op_gt : t β†’ t β†’ bool := Included_S.(Compare.S.op_gt).

  Definition compare : t β†’ t β†’ int := Included_S.(Compare.S.compare).

  Definition equal : t β†’ t β†’ bool := Included_S.(Compare.S.equal).

  Definition max : t β†’ t β†’ t := Included_S.(Compare.S.max).

  Definition min : t β†’ t β†’ t := Included_S.(Compare.S.min).

  Parameter add : t β†’ int64 β†’ t.

  Parameter diff_value : t β†’ t β†’ int64.

  Parameter of_seconds : int64 β†’ t.

  Parameter to_seconds : t β†’ int64.

  Parameter of_notation : string β†’ option t.

  Parameter of_notation_exn : string β†’ t.

  Parameter to_notation : t β†’ string.

  Parameter encoding : Data_encoding.t t.

  Parameter rfc_encoding : Data_encoding.t t.

  Parameter pp_hum : Format.formatter β†’ t β†’ unit.
End Time_signature.
Require Export TezosOfOCaml.Environment.V7.Time.
Module Time_check : Time_signature := Time.

Module Type TzEndian_signature.
  Parameter get_int32 : bytes β†’ int β†’ int32.

  Parameter get_int32_string : string β†’ int β†’ int32.

  Parameter set_int32 : bytes β†’ int β†’ int32 β†’ unit.

  Parameter set_int8 : bytes β†’ int β†’ int β†’ unit.

  Parameter get_int8 : bytes β†’ int β†’ int.

  Parameter get_int8_string : string β†’ int β†’ int.

  Parameter set_int16 : bytes β†’ int β†’ int β†’ unit.

  Parameter get_int16 : bytes β†’ int β†’ int.

  Parameter get_int16_string : string β†’ int β†’ int.

  Parameter set_int64 : bytes β†’ int β†’ int64 β†’ unit.

  Parameter get_int64 : bytes β†’ int β†’ int64.

  Parameter get_int64_string : string β†’ int β†’ int64.

  Parameter get_uint8 : bytes β†’ int β†’ int.

  Parameter get_uint8_string : string β†’ int β†’ int.

  Parameter set_uint8 : bytes β†’ int β†’ int β†’ unit.

  Parameter get_uint16 : bytes β†’ int β†’ int.

  Parameter get_uint16_string : string β†’ int β†’ int.

  Parameter set_uint16 : bytes β†’ int β†’ int β†’ unit.
End TzEndian_signature.
Require Export TezosOfOCaml.Environment.V7.TzEndian.
Module TzEndian_check : TzEndian_signature := TzEndian.

Module Type Bits_signature.
  Parameter numbits : int β†’ int.
End Bits_signature.
Require Export TezosOfOCaml.Environment.V7.Bits.
Module Bits_check : Bits_signature := Bits.

Module Type Equality_witness_signature.
  Inductive eq : Set :=
  | Refl : eq.

  Parameter t : βˆ€ (a : Set), Set.

  Parameter make : βˆ€ {a : Set}, unit β†’ t a.

  Parameter eq_value : βˆ€ {a b : Set}, t a β†’ t b β†’ option eq.

  Parameter hash_value : βˆ€ {a : Set}, t a β†’ int.
End Equality_witness_signature.
Require Export TezosOfOCaml.Environment.V7.Equality_witness.
Module Equality_witness_check : Equality_witness_signature := Equality_witness.

Module Type FallbackArray_signature.
  Parameter t : βˆ€ (a : Set), Set.

  Parameter make : βˆ€ {a : Set}, int β†’ a β†’ t a.

  Parameter of_list : βˆ€ {a b : Set}, b β†’ (a β†’ b) β†’ list a β†’ t b.

  Parameter fallback : βˆ€ {a : Set}, t a β†’ a.

  Parameter length : βˆ€ {a : Set}, t a β†’ int.

  Parameter get : βˆ€ {a : Set}, t a β†’ int β†’ a.

  Parameter set : βˆ€ {a : Set}, t a β†’ int β†’ a β†’ unit.

  Parameter iter : βˆ€ {a : Set}, (a β†’ unit) β†’ t a β†’ unit.

  Parameter map : βˆ€ {a b : Set}, (a β†’ b) β†’ t a β†’ t b.

  Parameter fold : βˆ€ {a b : Set}, (b β†’ a β†’ b) β†’ t a β†’ b β†’ b.

  Parameter fold_map : βˆ€ {a b c : Set},
    (b β†’ a β†’ b Γ— c) β†’ t a β†’ b β†’ c β†’ b Γ— t c.
End FallbackArray_signature.
Require Export TezosOfOCaml.Environment.V7.FallbackArray.
Module FallbackArray_check : FallbackArray_signature := FallbackArray.

Module Type Error_monad_signature.
  Inductive error_category : Set :=
  | Outdated : error_category
  | Permanent : error_category
  | Temporary : error_category
  | Branch : error_category.

  Definition _error := extensible_type.

  Parameter error_encoding : Data_encoding.t _error.

  Parameter pp : Format.formatter β†’ _error β†’ unit.

  Parameter register_error_kind : βˆ€ {err : Set},
    error_category β†’ string β†’ string β†’ string β†’
    option (Format.formatter β†’ err β†’ unit) β†’ Data_encoding.t err β†’
    (_error β†’ option err) β†’ (err β†’ _error) β†’ unit.

  Parameter json_of_error : _error β†’ Data_encoding.json.

  Parameter error_of_json : Data_encoding.json β†’ _error.

  Module error_info.
    Record record : Set := Build {
      category : error_category;
      id : string;
      title : string;
      description : string;
      schema : Data_encoding.json_schema;
    }.
    Definition with_category category (r : record) :=
      Build category r.(id) r.(title) r.(description) r.(schema).
    Definition with_id id (r : record) :=
      Build r.(category) id r.(title) r.(description) r.(schema).
    Definition with_title title (r : record) :=
      Build r.(category) r.(id) title r.(description) r.(schema).
    Definition with_description description (r : record) :=
      Build r.(category) r.(id) r.(title) description r.(schema).
    Definition with_schema schema (r : record) :=
      Build r.(category) r.(id) r.(title) r.(description) schema.
  End error_info.
  Definition error_info := error_info.record.

  Parameter pp_info : Format.formatter β†’ error_info β†’ unit.

  Parameter get_registered_errors : unit β†’ list error_info.

  Parameter trace : βˆ€ (err : Set), Set.

  Definition tzresult (a : Set) : Set := Pervasives.result a (trace _error).

  Parameter make_trace_encoding : βˆ€ {_error : Set},
    Data_encoding.t _error β†’ Data_encoding.t (trace _error).

  Parameter trace_encoding : Data_encoding.t (trace _error).

  Parameter pp_trace : Format.formatter β†’ trace _error β†’ unit.

  Parameter result_encoding : βˆ€ {a : Set},
    Data_encoding.t a β†’ Data_encoding.t (tzresult a).

  Parameter ok : βˆ€ {a trace : Set}, a β†’ Pervasives.result a trace.

  Parameter _return : βˆ€ {a trace : Set}, a β†’ Pervasives.result a trace.

  Parameter return_unit : βˆ€ {trace : Set}, Pervasives.result unit trace.

  Parameter return_none : βˆ€ {a trace : Set},
    Pervasives.result (option a) trace.

  Parameter return_some : βˆ€ {a trace : Set},
    a β†’ Pervasives.result (option a) trace.

  Parameter return_nil : βˆ€ {a trace : Set},
    Pervasives.result (list a) trace.

  Parameter return_true : βˆ€ {trace : Set}, Pervasives.result bool trace.

  Parameter return_false : βˆ€ {trace : Set}, Pervasives.result bool trace.

  Parameter error_value : βˆ€ {a err : Set},
    err β†’ Pervasives.result a (trace err).

  Parameter trace_of_error : βˆ€ {err : Set}, err β†’ trace err.

  Parameter fail : βˆ€ {a err : Set}, err β†’ Pervasives.result a (trace err).

  Parameter op_gtgteq : βˆ€ {a b : Set}, a β†’ (a β†’ b) β†’ b.

  Parameter op_gtpipeeq : βˆ€ {a b : Set}, a β†’ (a β†’ b) β†’ b.

  Parameter op_gtgtquestion : βˆ€ {a b trace : Set},
    Pervasives.result a trace β†’ (a β†’ Pervasives.result b trace) β†’
    Pervasives.result b trace.

  Parameter op_gtpipequestion : βˆ€ {a b trace : Set},
    Pervasives.result a trace β†’ (a β†’ b) β†’ Pervasives.result b trace.

  Parameter op_gtgteqquestion : βˆ€ {a b trace : Set},
    Pervasives.result a trace β†’ (a β†’ Pervasives.result b trace) β†’
    Pervasives.result b trace.

  Parameter op_gtpipeeqquestion : βˆ€ {a b trace : Set},
    Pervasives.result a trace β†’ (a β†’ b) β†’ Pervasives.result b trace.

  Parameter op_gtgtquestioneq : βˆ€ {a b trace : Set},
    Pervasives.result a trace β†’ (a β†’ Pervasives.result b trace) β†’
    Pervasives.result b trace.

  Parameter op_gtpipequestioneq : βˆ€ {a b trace : Set},
    Pervasives.result a trace β†’ (a β†’ b) β†’ Pervasives.result b trace.

  Parameter record_trace : βˆ€ {a err : Set},
    err β†’ Pervasives.result a (trace err) β†’ Pervasives.result a (trace err).

  Parameter trace_value : βˆ€ {b err : Set},
    err β†’ Pervasives.result b (trace err) β†’ Pervasives.result b (trace err).

  Parameter record_trace_eval : βˆ€ {a err : Set},
    (unit β†’ err) β†’ Pervasives.result a (trace err) β†’
    Pervasives.result a (trace err).

  Parameter trace_eval : βˆ€ {b err : Set},
    (unit β†’ err) β†’ Pervasives.result b (trace err) β†’
    Pervasives.result b (trace err).

  Parameter error_unless : βˆ€ {err : Set},
    bool β†’ err β†’ Pervasives.result unit (trace err).

  Parameter error_when : βˆ€ {err : Set},
    bool β†’ err β†’ Pervasives.result unit (trace err).

  Parameter fail_unless : βˆ€ {err : Set},
    bool β†’ err β†’ Pervasives.result unit (trace err).

  Parameter fail_when : βˆ€ {err : Set},
    bool β†’ err β†’ Pervasives.result unit (trace err).

  Parameter unless : βˆ€ {trace : Set},
    bool β†’ (unit β†’ Pervasives.result unit trace) β†’
    Pervasives.result unit trace.

  Parameter when_ : βˆ€ {trace : Set},
    bool β†’ (unit β†’ Pervasives.result unit trace) β†’
    Pervasives.result unit trace.

  Parameter dont_wait : βˆ€ {trace : Set},
    (extensible_type β†’ unit) β†’ (trace β†’ unit) β†’
    (unit β†’ Pervasives.result unit trace) β†’ unit.

  Parameter catch : βˆ€ {a : Set},
    option (extensible_type β†’ bool) β†’ (unit β†’ a) β†’ tzresult a.

  Parameter catch_f : βˆ€ {a : Set},
    option (extensible_type β†’ bool) β†’ (unit β†’ a) β†’
    (extensible_type β†’ _error) β†’ tzresult a.

  Parameter catch_s : βˆ€ {a : Set},
    option (extensible_type β†’ bool) β†’ (unit β†’ a) β†’ tzresult a.

  Parameter join_e : βˆ€ {err : Set},
    list (Pervasives.result unit (trace err)) β†’
    Pervasives.result unit (trace err).

  Parameter all_e : βˆ€ {a err : Set},
    list (Pervasives.result a (trace err)) β†’
    Pervasives.result (list a) (trace err).

  Parameter both_e : βˆ€ {a b err : Set},
    Pervasives.result a (trace err) β†’ Pervasives.result b (trace err) β†’
    Pervasives.result (a Γ— b) (trace err).

  Parameter shell_tztrace : Set.

  Definition shell_tzresult (a : Set) : Set :=
    Pervasives.result a shell_tztrace.

  Module Lwt_syntax.
    Parameter _return : βˆ€ {a : Set}, a β†’ a.

    Parameter return_none : βˆ€ {A : Set}, option A.

    Parameter return_nil : βˆ€ {A : Set}, list A.

    Parameter return_true : bool.

    Parameter return_false : bool.

    Parameter return_some : βˆ€ {a : Set}, a β†’ option a.

    Parameter return_ok : βˆ€ {B a : Set}, a β†’ Pervasives.result a B.

    Parameter return_error : βˆ€ {B e : Set}, e β†’ Pervasives.result B e.

    Parameter return_ok_unit : βˆ€ {e : Set}, Pervasives.result unit e.

    Parameter return_ok_true : βˆ€ {e : Set}, Pervasives.result bool e.

    Parameter return_ok_false : βˆ€ {e : Set}, Pervasives.result bool e.

    Parameter return_ok_none : βˆ€ {a e : Set},
      Pervasives.result (option a) e.

    Parameter return_ok_nil : βˆ€ {a e : Set}, Pervasives.result (list a) e.

    Parameter op_letstar : βˆ€ {a b : Set}, a β†’ (a β†’ b) β†’ b.

    Parameter op_andstar : βˆ€ {a b : Set}, a β†’ b β†’ a Γ— b.

    Parameter op_letplus : βˆ€ {a b : Set}, a β†’ (a β†’ b) β†’ b.

    Parameter op_andplus : βˆ€ {a b : Set}, a β†’ b β†’ a Γ— b.

    Parameter join : list unit β†’ unit.

    Parameter all : βˆ€ {a : Set}, list a β†’ list a.

    Parameter both : βˆ€ {a b : Set}, a β†’ b β†’ a Γ— b.
  End Lwt_syntax.

  Module Option_syntax.
    Parameter _return : βˆ€ {a : Set}, a β†’ option a.

    Parameter fail : βˆ€ {a : Set}, option a.

    Parameter return_unit : option unit.

    Parameter return_nil : βˆ€ {a : Set}, option (list a).

    Parameter return_true : option bool.

    Parameter return_false : option bool.

    Parameter op_letstar : βˆ€ {a b : Set},
      option a β†’ (a β†’ option b) β†’ option b.

    Parameter op_andstar : βˆ€ {a b : Set},
      option a β†’ option b β†’ option (a Γ— b).

    Parameter op_letplus : βˆ€ {a b : Set}, option a β†’ (a β†’ b) β†’ option b.

    Parameter op_andplus : βˆ€ {a b : Set},
      option a β†’ option b β†’ option (a Γ— b).

    Parameter both : βˆ€ {a b : Set}, option a β†’ option b β†’ option (a Γ— b).
  End Option_syntax.

  Module Result_syntax.
    Parameter _return : βˆ€ {a e : Set}, a β†’ Pervasives.result a e.

    Parameter return_unit : βˆ€ {e : Set}, Pervasives.result unit e.

    Parameter return_none : βˆ€ {a e : Set}, Pervasives.result (option a) e.

    Parameter return_some : βˆ€ {a e : Set},
      a β†’ Pervasives.result (option a) e.

    Parameter return_nil : βˆ€ {a e : Set}, Pervasives.result (list a) e.

    Parameter return_true : βˆ€ {e : Set}, Pervasives.result bool e.

    Parameter return_false : βˆ€ {e : Set}, Pervasives.result bool e.

    Parameter fail : βˆ€ {a e : Set}, e β†’ Pervasives.result a e.

    Parameter op_letstar : βˆ€ {a b e : Set},
      Pervasives.result a e β†’ (a β†’ Pervasives.result b e) β†’
      Pervasives.result b e.

    Parameter op_letplus : βˆ€ {a b e : Set},
      Pervasives.result a e β†’ (a β†’ b) β†’ Pervasives.result b e.

    Parameter join : βˆ€ {e : Set},
      list (Pervasives.result unit e) β†’ Pervasives.result unit (list e).

    Parameter all : βˆ€ {a e : Set},
      list (Pervasives.result a e) β†’ Pervasives.result (list a) (list e).

    Parameter both : βˆ€ {a b e : Set},
      Pervasives.result a e β†’ Pervasives.result b e β†’
      Pervasives.result (a Γ— b) (list e).
  End Result_syntax.

  Module Lwt_result_syntax.
    Parameter _return : βˆ€ {a e : Set}, a β†’ Pervasives.result a e.

    Parameter return_unit : βˆ€ {e : Set}, Pervasives.result unit e.

    Parameter return_none : βˆ€ {a e : Set}, Pervasives.result (option a) e.

    Parameter return_some : βˆ€ {a e : Set},
      a β†’ Pervasives.result (option a) e.

    Parameter return_nil : βˆ€ {a e : Set}, Pervasives.result (list a) e.

    Parameter return_true : βˆ€ {e : Set}, Pervasives.result bool e.

    Parameter return_false : βˆ€ {e : Set}, Pervasives.result bool e.

    Parameter fail : βˆ€ {a e : Set}, e β†’ Pervasives.result a e.

    Parameter op_letstar : βˆ€ {a b e : Set},
      Pervasives.result a e β†’ (a β†’ Pervasives.result b e) β†’
      Pervasives.result b e.

    Parameter op_letplus : βˆ€ {a b e : Set},
      Pervasives.result a e β†’ (a β†’ b) β†’ Pervasives.result b e.

    Parameter lwt_map_error : βˆ€ {a e f : Set},
      (e β†’ f) β†’ Pervasives.result a e β†’ Pervasives.result a f.

    Parameter op_letstarexclamation : βˆ€ {a b : Set}, a β†’ (a β†’ b) β†’ b.

    Parameter op_letstarquestion : βˆ€ {a b e : Set},
      Pervasives.result a e β†’ (a β†’ Pervasives.result b e) β†’
      Pervasives.result b e.

    Parameter join : βˆ€ {e : Set},
      list (Pervasives.result unit e) β†’ Pervasives.result unit (list e).

    Parameter all : βˆ€ {a e : Set},
      list (Pervasives.result a e) β†’ Pervasives.result (list a) (list e).

    Parameter both : βˆ€ {a b e : Set},
      Pervasives.result a e β†’ Pervasives.result b e β†’
      Pervasives.result (a Γ— b) (list e).
  End Lwt_result_syntax.

  Module Lwt_option_syntax.
    Parameter _return : βˆ€ {a : Set}, a β†’ option a.

    Parameter return_unit : option unit.

    Parameter return_nil : βˆ€ {a : Set}, option (list a).

    Parameter return_true : option bool.

    Parameter return_false : option bool.

    Parameter fail : βˆ€ {a : Set}, option a.

    Parameter op_letstar : βˆ€ {a b : Set},
      option a β†’ (a β†’ option b) β†’ option b.

    Parameter op_andstar : βˆ€ {a b : Set},
      option a β†’ option b β†’ option (a Γ— b).

    Parameter op_letplus : βˆ€ {a b : Set}, option a β†’ (a β†’ b) β†’ option b.

    Parameter op_andplus : βˆ€ {a b : Set},
      option a β†’ option b β†’ option (a Γ— b).

    Parameter op_letstarexclamation : βˆ€ {a b : Set}, a β†’ (a β†’ b) β†’ b.

    Parameter op_letstarquestion : βˆ€ {a b : Set},
      option a β†’ (a β†’ option b) β†’ option b.

    Parameter both : βˆ€ {a b : Set}, option a β†’ option b β†’ option (a Γ— b).
  End Lwt_option_syntax.

  Module Tzresult_syntax.
    Parameter _return : βˆ€ {_error a : Set},
      a β†’ Pervasives.result a _error.

    Parameter return_unit : βˆ€ {_error : Set},
      Pervasives.result unit _error.

    Parameter return_none : βˆ€ {_error a : Set},
      Pervasives.result (option a) _error.

    Parameter return_some : βˆ€ {_error a : Set},
      a β†’ Pervasives.result (option a) _error.

    Parameter return_nil : βˆ€ {_error a : Set},
      Pervasives.result (list a) _error.

    Parameter return_true : βˆ€ {_error : Set},
      Pervasives.result bool _error.

    Parameter return_false : βˆ€ {_error : Set},
      Pervasives.result bool _error.

    Parameter fail : βˆ€ {_error a : Set},
      _error β†’ Pervasives.result a (trace _error).

    Parameter op_letstar : βˆ€ {a b e : Set},
      Pervasives.result a e β†’ (a β†’ Pervasives.result b e) β†’
      Pervasives.result b e.

    Parameter op_andstar : βˆ€ {a b e : Set},
      Pervasives.result a (trace e) β†’ Pervasives.result b (trace e) β†’
      Pervasives.result (a Γ— b) (trace e).

    Parameter op_letplus : βˆ€ {a b e : Set},
      Pervasives.result a e β†’ (a β†’ b) β†’ Pervasives.result b e.

    Parameter op_andplus : βˆ€ {a b e : Set},
      Pervasives.result a (trace e) β†’ Pervasives.result b (trace e) β†’
      Pervasives.result (a Γ— b) (trace e).

    Parameter join : βˆ€ {_error : Set},
      list (Pervasives.result unit (trace _error)) β†’
      Pervasives.result unit (trace _error).

    Parameter all : βˆ€ {_error a : Set},
      list (Pervasives.result a (trace _error)) β†’
      Pervasives.result (list a) (trace _error).

    Parameter both : βˆ€ {_error a b : Set},
      Pervasives.result a (trace _error) β†’
      Pervasives.result b (trace _error) β†’
      Pervasives.result (a Γ— b) (trace _error).
  End Tzresult_syntax.

  Module Lwt_tzresult_syntax.
    Parameter _return : βˆ€ {_error a : Set},
      a β†’ Pervasives.result a _error.

    Parameter return_unit : βˆ€ {_error : Set},
      Pervasives.result unit _error.

    Parameter return_none : βˆ€ {_error a : Set},
      Pervasives.result (option a) _error.

    Parameter return_some : βˆ€ {_error a : Set},
      a β†’ Pervasives.result (option a) _error.

    Parameter return_nil : βˆ€ {_error a : Set},
      Pervasives.result (list a) _error.

    Parameter return_true : βˆ€ {_error : Set},
      Pervasives.result bool _error.

    Parameter return_false : βˆ€ {_error : Set},
      Pervasives.result bool _error.

    Parameter fail : βˆ€ {_error a : Set},
      _error β†’ Pervasives.result a (trace _error).

    Parameter op_letstar : βˆ€ {a b e : Set},
      Pervasives.result a e β†’ (a β†’ Pervasives.result b e) β†’
      Pervasives.result b e.

    Parameter op_andstar : βˆ€ {a b e : Set},
      Pervasives.result a (trace e) β†’ Pervasives.result b (trace e) β†’
      Pervasives.result (a Γ— b) (trace e).

    Parameter op_letplus : βˆ€ {a b e : Set},
      Pervasives.result a e β†’ (a β†’ b) β†’ Pervasives.result b e.

    Parameter op_andplus : βˆ€ {a b e : Set},
      Pervasives.result a (trace e) β†’ Pervasives.result b (trace e) β†’
      Pervasives.result (a Γ— b) (trace e).

    Parameter op_letstarexclamation : βˆ€ {a b : Set}, a β†’ (a β†’ b) β†’ b.

    Parameter op_letstarquestion : βˆ€ {a b e : Set},
      Pervasives.result a e β†’ (a β†’ Pervasives.result b e) β†’
      Pervasives.result b e.

    Parameter join : βˆ€ {_error : Set},
      list (Pervasives.result unit (trace _error)) β†’
      Pervasives.result unit (trace _error).

    Parameter all : βˆ€ {_error a : Set},
      list (Pervasives.result a (trace _error)) β†’
      Pervasives.result (list a) (trace _error).

    Parameter both : βˆ€ {_error a b : Set},
      Pervasives.result a (trace _error) β†’
      Pervasives.result b (trace _error) β†’
      Pervasives.result (a Γ— b) (trace _error).
  End Lwt_tzresult_syntax.
End Error_monad_signature.
Require Export TezosOfOCaml.Environment.V7.Error_monad.
Module Error_monad_check : Error_monad_signature := Error_monad.

Export Error_monad.Notations.

Module Type Seq_signature.
  Reserved Notation "'t".

  Inductive node (a : Set) : Set :=
  | Nil : node a
  | Cons : a β†’ 't a β†’ node a
  
  where "'t" := (fun (t_a : Set) β‡’ unit β†’ node t_a).

  Definition t := 't.

  Arguments Nil {_}.
  Arguments Cons {_}.

  Parameter empty : βˆ€ {a : Set}, t a.

  Parameter _return : βˆ€ {a : Set}, a β†’ t a.

  Parameter cons_value : βˆ€ {a : Set}, a β†’ t a β†’ t a.

  Parameter append : βˆ€ {a : Set}, t a β†’ t a β†’ t a.

  Parameter map : βˆ€ {a b : Set}, (a β†’ b) β†’ t a β†’ t b.

  Parameter filter : βˆ€ {a : Set}, (a β†’ bool) β†’ t a β†’ t a.

  Parameter filter_map : βˆ€ {a b : Set}, (a β†’ option b) β†’ t a β†’ t b.

  Parameter flat_map : βˆ€ {a b : Set}, (a β†’ t b) β†’ t a β†’ t b.

  Parameter fold_left : βˆ€ {a b : Set}, (a β†’ b β†’ a) β†’ a β†’ t b β†’ a.

  Parameter iter : βˆ€ {a : Set}, (a β†’ unit) β†’ t a β†’ unit.

  Parameter unfold : βˆ€ {a b : Set}, (b β†’ option (a Γ— b)) β†’ b β†’ t a.

  Parameter first : βˆ€ {a : Set}, t a β†’ option a.

  Parameter fold_left_e : βˆ€ {a b trace : Set},
    (a β†’ b β†’ Pervasives.result a trace) β†’ a β†’ t b β†’
    Pervasives.result a trace.

  Parameter fold_left_s : βˆ€ {a b : Set}, (a β†’ b β†’ a) β†’ a β†’ t b β†’ a.

  Parameter fold_left_es : βˆ€ {a b trace : Set},
    (a β†’ b β†’ Pervasives.result a trace) β†’ a β†’ t b β†’
    Pervasives.result a trace.

  Parameter iter_e : βˆ€ {a trace : Set},
    (a β†’ Pervasives.result unit trace) β†’ t a β†’ Pervasives.result unit trace.

  Parameter iter_s : βˆ€ {a : Set}, (a β†’ unit) β†’ t a β†’ unit.

  Parameter iter_es : βˆ€ {a trace : Set},
    (a β†’ Pervasives.result unit trace) β†’ t a β†’ Pervasives.result unit trace.

  Parameter iter_ep : βˆ€ {a : Set}, (a β†’ M? unit) β†’ t a β†’ M? unit.

  Parameter iter_p : βˆ€ {a : Set}, (a β†’ unit) β†’ t a β†’ unit.
End Seq_signature.
Require Export TezosOfOCaml.Environment.V7.Seq.
Module Seq_check : Seq_signature := Seq.

Module Type List_signature.
  Definition t (a : Set) : Set := list a.

  Parameter nil : βˆ€ {a : Set}, list a.

  Parameter nil_e : βˆ€ {a trace : Set}, Pervasives.result (list a) trace.

  Parameter nil_s : βˆ€ {a : Set}, list a.

  Parameter nil_es : βˆ€ {a trace : Set}, Pervasives.result (list a) trace.

  Parameter cons_value : βˆ€ {a : Set}, a β†’ list a β†’ list a.

  Parameter is_empty : βˆ€ {a : Set}, list a β†’ bool.

  Parameter hd : βˆ€ {a : Set}, list a β†’ option a.

  Parameter tl : βˆ€ {a : Set}, list a β†’ option (list a).

  Parameter nth : βˆ€ {a : Set}, list a β†’ int β†’ option a.

  Parameter nth_opt : βˆ€ {a : Set}, list a β†’ int β†’ option a.

  Parameter last : βˆ€ {a : Set}, a β†’ list a β†’ a.

  Parameter last_opt : βˆ€ {a : Set}, list a β†’ option a.

  Parameter find : βˆ€ {a : Set}, (a β†’ bool) β†’ list a β†’ option a.

  Parameter find_opt : βˆ€ {a : Set}, (a β†’ bool) β†’ list a β†’ option a.

  Parameter find_map : βˆ€ {a b : Set},
    (a β†’ option b) β†’ list a β†’ option b.

  Parameter mem : βˆ€ {a : Set}, (a β†’ a β†’ bool) β†’ a β†’ list a β†’ bool.

  Parameter assoc : βˆ€ {a b : Set},
    (a β†’ a β†’ bool) β†’ a β†’ list (a Γ— b) β†’ option b.

  Parameter assoc_opt : βˆ€ {a b : Set},
    (a β†’ a β†’ bool) β†’ a β†’ list (a Γ— b) β†’ option b.

  Parameter assq : βˆ€ {a b : Set}, a β†’ list (a Γ— b) β†’ option b.

  Parameter assq_opt : βˆ€ {a b : Set}, a β†’ list (a Γ— b) β†’ option b.

  Parameter mem_assoc : βˆ€ {a b : Set},
    (a β†’ a β†’ bool) β†’ a β†’ list (a Γ— b) β†’ bool.

  Parameter mem_assq : βˆ€ {a b : Set}, a β†’ list (a Γ— b) β†’ bool.

  Parameter remove_assoc : βˆ€ {a b : Set},
    (a β†’ a β†’ bool) β†’ a β†’ list (a Γ— b) β†’ list (a Γ— b).

  Parameter remove_assq : βˆ€ {a b : Set}, a β†’ list (a Γ— b) β†’ list (a Γ— b).

  Parameter init_value : βˆ€ {a trace : Set},
    trace β†’ int β†’ (int β†’ a) β†’ Pervasives.result (list a) trace.

  Parameter length : βˆ€ {a : Set}, list a β†’ int.

  Parameter rev : βˆ€ {a : Set}, list a β†’ list a.

  Parameter concat : βˆ€ {a : Set}, list (list a) β†’ list a.

  Parameter append : βˆ€ {a : Set}, list a β†’ list a β†’ list a.

  Parameter rev_append : βˆ€ {a : Set}, list a β†’ list a β†’ list a.

  Parameter flatten : βˆ€ {a : Set}, list (list a) β†’ list a.

  Parameter combine : βˆ€ {a b trace : Set},
    trace β†’ list a β†’ list b β†’ Pervasives.result (list (a Γ— b)) trace.

  Parameter rev_combine : βˆ€ {a b trace : Set},
    trace β†’ list a β†’ list b β†’ Pervasives.result (list (a Γ— b)) trace.

  Parameter split : βˆ€ {a b : Set}, list (a Γ— b) β†’ list a Γ— list b.

  Parameter iter2 : βˆ€ {a b trace : Set},
    trace β†’ (a β†’ b β†’ unit) β†’ list a β†’ list b β†’
    Pervasives.result unit trace.

  Parameter map2 : βˆ€ {a b c trace : Set},
    trace β†’ (a β†’ b β†’ c) β†’ list a β†’ list b β†’
    Pervasives.result (list c) trace.

  Parameter rev_map2 : βˆ€ {a b c trace : Set},
    trace β†’ (a β†’ b β†’ c) β†’ list a β†’ list b β†’
    Pervasives.result (list c) trace.

  Parameter fold_left2 : βˆ€ {a b c trace : Set},
    trace β†’ (a β†’ b β†’ c β†’ a) β†’ a β†’ list b β†’ list c β†’
    Pervasives.result a trace.

  Parameter fold_right2 : βˆ€ {a b c trace : Set},
    trace β†’ (a β†’ b β†’ c β†’ c) β†’ list a β†’ list b β†’ c β†’
    Pervasives.result c trace.

  Parameter for_all2 : βˆ€ {a b trace : Set},
    trace β†’ (a β†’ b β†’ bool) β†’ list a β†’ list b β†’
    Pervasives.result bool trace.

  Parameter _exists2 : βˆ€ {a b trace : Set},
    trace β†’ (a β†’ b β†’ bool) β†’ list a β†’ list b β†’
    Pervasives.result bool trace.

  Parameter init_e : βˆ€ {a trace : Set},
    trace β†’ int β†’ (int β†’ Pervasives.result a trace) β†’
    Pervasives.result (list a) trace.

  Parameter init_s : βˆ€ {a trace : Set},
    trace β†’ int β†’ (int β†’ a) β†’ Pervasives.result (list a) trace.

  Parameter init_es : βˆ€ {a trace : Set},
    trace β†’ int β†’ (int β†’ Pervasives.result a trace) β†’
    Pervasives.result (list a) trace.

  Parameter init_p : βˆ€ {a trace : Set},
    trace β†’ int β†’ (int β†’ a) β†’ Pervasives.result (list a) trace.

  Parameter find_e : βˆ€ {a trace : Set},
    (a β†’ Pervasives.result bool trace) β†’ list a β†’
    Pervasives.result (option a) trace.

  Parameter find_s : βˆ€ {a : Set}, (a β†’ bool) β†’ list a β†’ option a.

  Parameter find_es : βˆ€ {a trace : Set},
    (a β†’ Pervasives.result bool trace) β†’ list a β†’
    Pervasives.result (option a) trace.

  Parameter find_map_e : βˆ€ {a b trace : Set},
    (a β†’ Pervasives.result (option b) trace) β†’ list a β†’
    Pervasives.result (option b) trace.

  Parameter find_map_s : βˆ€ {a b : Set},
    (a β†’ option b) β†’ list a β†’ option b.

  Parameter find_map_es : βˆ€ {a b trace : Set},
    (a β†’ Pervasives.result (option b) trace) β†’ list a β†’
    Pervasives.result (option b) trace.

  Parameter filter : βˆ€ {a : Set}, (a β†’ bool) β†’ list a β†’ list a.

  Parameter filteri : βˆ€ {a : Set}, (int β†’ a β†’ bool) β†’ list a β†’ list a.

  Parameter find_all : βˆ€ {a : Set}, (a β†’ bool) β†’ list a β†’ list a.

  Parameter rev_filter : βˆ€ {a : Set}, (a β†’ bool) β†’ list a β†’ list a.

  Parameter rev_filteri : βˆ€ {a : Set},
    (int β†’ a β†’ bool) β†’ list a β†’ list a.

  Parameter rev_filter_some : βˆ€ {a : Set}, list (option a) β†’ list a.

  Parameter filter_some : βˆ€ {a : Set}, list (option a) β†’ list a.

  Parameter rev_filter_ok : βˆ€ {a b : Set},
    list (Pervasives.result a b) β†’ list a.

  Parameter filter_ok : βˆ€ {a b : Set},
    list (Pervasives.result a b) β†’ list a.

  Parameter rev_filter_error : βˆ€ {a b : Set},
    list (Pervasives.result a b) β†’ list b.

  Parameter filter_error : βˆ€ {a b : Set},
    list (Pervasives.result a b) β†’ list b.

  Parameter rev_filter_left : βˆ€ {a b : Set}, list (Either.t a b) β†’ list a.

  Parameter filter_left : βˆ€ {a b : Set}, list (Either.t a b) β†’ list a.

  Parameter rev_filter_right : βˆ€ {a b : Set},
    list (Either.t a b) β†’ list b.

  Parameter filter_right : βˆ€ {a b : Set}, list (Either.t a b) β†’ list b.

  Parameter rev_filter_e : βˆ€ {a trace : Set},
    (a β†’ Pervasives.result bool trace) β†’ list a β†’
    Pervasives.result (list a) trace.

  Parameter filter_e : βˆ€ {a trace : Set},
    (a β†’ Pervasives.result bool trace) β†’ list a β†’
    Pervasives.result (list a) trace.

  Parameter rev_filter_s : βˆ€ {a : Set}, (a β†’ bool) β†’ list a β†’ list a.

  Parameter filter_s : βˆ€ {a : Set}, (a β†’ bool) β†’ list a β†’ list a.

  Parameter rev_filter_es : βˆ€ {a trace : Set},
    (a β†’ Pervasives.result bool trace) β†’ list a β†’
    Pervasives.result (list a) trace.

  Parameter filter_es : βˆ€ {a trace : Set},
    (a β†’ Pervasives.result bool trace) β†’ list a β†’
    Pervasives.result (list a) trace.

  Parameter rev_filteri_e : βˆ€ {a trace : Set},
    (int β†’ a β†’ Pervasives.result bool trace) β†’ list a β†’
    Pervasives.result (list a) trace.

  Parameter filteri_e : βˆ€ {a trace : Set},
    (int β†’ a β†’ Pervasives.result bool trace) β†’ list a β†’
    Pervasives.result (list a) trace.

  Parameter rev_filteri_s : βˆ€ {a : Set},
    (int β†’ a β†’ bool) β†’ list a β†’ list a.

  Parameter filteri_s : βˆ€ {a : Set},
    (int β†’ a β†’ bool) β†’ list a β†’ list a.

  Parameter rev_filteri_es : βˆ€ {a trace : Set},
    (int β†’ a β†’ Pervasives.result bool trace) β†’ list a β†’
    Pervasives.result (list a) trace.

  Parameter filteri_es : βˆ€ {a trace : Set},
    (int β†’ a β†’ Pervasives.result bool trace) β†’ list a β†’
    Pervasives.result (list a) trace.

  Parameter rev_partition : βˆ€ {a : Set},
    (a β†’ bool) β†’ list a β†’ list a Γ— list a.

  Parameter partition : βˆ€ {a : Set},
    (a β†’ bool) β†’ list a β†’ list a Γ— list a.

  Parameter rev_partition_map : βˆ€ {a b c : Set},
    (a β†’ Either.t b c) β†’ list a β†’ list b Γ— list c.

  Parameter partition_map : βˆ€ {a b c : Set},
    (a β†’ Either.t b c) β†’ list a β†’ list b Γ— list c.

  Parameter rev_partition_result : βˆ€ {a b : Set},
    list (Pervasives.result a b) β†’ list a Γ— list b.

  Parameter partition_result : βˆ€ {a b : Set},
    list (Pervasives.result a b) β†’ list a Γ— list b.

  Parameter rev_partition_either : βˆ€ {a b : Set},
    list (Either.t a b) β†’ list a Γ— list b.

  Parameter partition_either : βˆ€ {a b : Set},
    list (Either.t a b) β†’ list a Γ— list b.

  Parameter rev_partition_e : βˆ€ {a trace : Set},
    (a β†’ Pervasives.result bool trace) β†’ list a β†’
    Pervasives.result (list a Γ— list a) trace.

  Parameter partition_e : βˆ€ {a trace : Set},
    (a β†’ Pervasives.result bool trace) β†’ list a β†’
    Pervasives.result (list a Γ— list a) trace.

  Parameter rev_partition_s : βˆ€ {a : Set},
    (a β†’ bool) β†’ list a β†’ list a Γ— list a.

  Parameter partition_s : βˆ€ {a : Set},
    (a β†’ bool) β†’ list a β†’ list a Γ— list a.

  Parameter rev_partition_es : βˆ€ {a trace : Set},
    (a β†’ Pervasives.result bool trace) β†’ list a β†’
    Pervasives.result (list a Γ— list a) trace.

  Parameter partition_es : βˆ€ {a trace : Set},
    (a β†’ Pervasives.result bool trace) β†’ list a β†’
    Pervasives.result (list a Γ— list a) trace.

  Parameter partition_p : βˆ€ {a : Set},
    (a β†’ bool) β†’ list a β†’ list a Γ— list a.

  Parameter rev_partition_map_e : βˆ€ {a b c trace : Set},
    (a β†’ Pervasives.result (Either.t b c) trace) β†’ list a β†’
    Pervasives.result (list b Γ— list c) trace.

  Parameter partition_map_e : βˆ€ {a b c trace : Set},
    (a β†’ Pervasives.result (Either.t b c) trace) β†’ list a β†’
    Pervasives.result (list b Γ— list c) trace.

  Parameter rev_partition_map_s : βˆ€ {a b c : Set},
    (a β†’ Either.t b c) β†’ list a β†’ list b Γ— list c.

  Parameter partition_map_s : βˆ€ {a b c : Set},
    (a β†’ Either.t b c) β†’ list a β†’ list b Γ— list c.

  Parameter rev_partition_map_es : βˆ€ {a b c trace : Set},
    (a β†’ Pervasives.result (Either.t b c) trace) β†’ list a β†’
    Pervasives.result (list b Γ— list c) trace.

  Parameter partition_map_es : βˆ€ {a b c trace : Set},
    (a β†’ Pervasives.result (Either.t b c) trace) β†’ list a β†’
    Pervasives.result (list b Γ— list c) trace.

  Parameter iter : βˆ€ {a : Set}, (a β†’ unit) β†’ list a β†’ unit.

  Parameter iter_e : βˆ€ {a trace : Set},
    (a β†’ Pervasives.result unit trace) β†’ list a β†’
    Pervasives.result unit trace.

  Parameter iter_s : βˆ€ {a : Set}, (a β†’ unit) β†’ list a β†’ unit.

  Parameter iter_es : βˆ€ {a trace : Set},
    (a β†’ Pervasives.result unit trace) β†’ list a β†’
    Pervasives.result unit trace.

  Parameter iter_p : βˆ€ {a : Set}, (a β†’ unit) β†’ list a β†’ unit.

  Parameter iteri : βˆ€ {a : Set}, (int β†’ a β†’ unit) β†’ list a β†’ unit.

  Parameter iteri_e : βˆ€ {a trace : Set},
    (int β†’ a β†’ Pervasives.result unit trace) β†’ list a β†’
    Pervasives.result unit trace.

  Parameter iteri_s : βˆ€ {a : Set}, (int β†’ a β†’ unit) β†’ list a β†’ unit.

  Parameter iteri_es : βˆ€ {a trace : Set},
    (int β†’ a β†’ Pervasives.result unit trace) β†’ list a β†’
    Pervasives.result unit trace.

  Parameter iteri_p : βˆ€ {a : Set}, (int β†’ a β†’ unit) β†’ list a β†’ unit.

  Parameter map : βˆ€ {a b : Set}, (a β†’ b) β†’ list a β†’ list b.

  Parameter map_e : βˆ€ {a b trace : Set},
    (a β†’ Pervasives.result b trace) β†’ list a β†’
    Pervasives.result (list b) trace.

  Parameter map_s : βˆ€ {a b : Set}, (a β†’ b) β†’ list a β†’ list b.

  Parameter map_es : βˆ€ {a b trace : Set},
    (a β†’ Pervasives.result b trace) β†’ list a β†’
    Pervasives.result (list b) trace.

  Parameter map_p : βˆ€ {a b : Set}, (a β†’ b) β†’ list a β†’ list b.

  Parameter mapi : βˆ€ {a b : Set}, (int β†’ a β†’ b) β†’ list a β†’ list b.

  Parameter mapi_e : βˆ€ {a b trace : Set},
    (int β†’ a β†’ Pervasives.result b trace) β†’ list a β†’
    Pervasives.result (list b) trace.

  Parameter mapi_s : βˆ€ {a b : Set}, (int β†’ a β†’ b) β†’ list a β†’ list b.

  Parameter mapi_es : βˆ€ {a b trace : Set},
    (int β†’ a β†’ Pervasives.result b trace) β†’ list a β†’
    Pervasives.result (list b) trace.

  Parameter mapi_p : βˆ€ {a b : Set}, (int β†’ a β†’ b) β†’ list a β†’ list b.

  Parameter rev_map : βˆ€ {a b : Set}, (a β†’ b) β†’ list a β†’ list b.

  Parameter rev_mapi : βˆ€ {a b : Set}, (int β†’ a β†’ b) β†’ list a β†’ list b.

  Parameter rev_map_e : βˆ€ {a b trace : Set},
    (a β†’ Pervasives.result b trace) β†’ list a β†’
    Pervasives.result (list b) trace.

  Parameter rev_map_s : βˆ€ {a b : Set}, (a β†’ b) β†’ list a β†’ list b.

  Parameter rev_map_es : βˆ€ {a b trace : Set},
    (a β†’ Pervasives.result b trace) β†’ list a β†’
    Pervasives.result (list b) trace.

  Parameter rev_map_p : βˆ€ {a b : Set}, (a β†’ b) β†’ list a β†’ list b.

  Parameter rev_mapi_e : βˆ€ {a b trace : Set},
    (int β†’ a β†’ Pervasives.result b trace) β†’ list a β†’
    Pervasives.result (list b) trace.

  Parameter rev_mapi_s : βˆ€ {a b : Set},
    (int β†’ a β†’ b) β†’ list a β†’ list b.

  Parameter rev_mapi_es : βˆ€ {a b trace : Set},
    (int β†’ a β†’ Pervasives.result b trace) β†’ list a β†’
    Pervasives.result (list b) trace.

  Parameter rev_mapi_p : βˆ€ {a b : Set},
    (int β†’ a β†’ b) β†’ list a β†’ list b.

  Parameter rev_filter_map : βˆ€ {a b : Set},
    (a β†’ option b) β†’ list a β†’ list b.

  Parameter rev_filter_map_e : βˆ€ {a b trace : Set},
    (a β†’ Pervasives.result (option b) trace) β†’ list a β†’
    Pervasives.result (list b) trace.

  Parameter filter_map_e : βˆ€ {a b trace : Set},
    (a β†’ Pervasives.result (option b) trace) β†’ list a β†’
    Pervasives.result (list b) trace.

  Parameter rev_filter_map_s : βˆ€ {a b : Set},
    (a β†’ option b) β†’ list a β†’ list b.

  Parameter filter_map : βˆ€ {a b : Set},
    (a β†’ option b) β†’ list a β†’ list b.

  Parameter filter_map_s : βˆ€ {a b : Set},
    (a β†’ option b) β†’ list a β†’ list b.

  Parameter rev_filter_map_es : βˆ€ {a b trace : Set},
    (a β†’ Pervasives.result (option b) trace) β†’ list a β†’
    Pervasives.result (list b) trace.

  Parameter filter_map_es : βˆ€ {a b trace : Set},
    (a β†’ Pervasives.result (option b) trace) β†’ list a β†’
    Pervasives.result (list b) trace.

  Parameter filter_map_p : βˆ€ {a b : Set},
    (a β†’ option b) β†’ list a β†’ list b.

  Parameter concat_map : βˆ€ {a b : Set}, (a β†’ list b) β†’ list a β†’ list b.

  Parameter concat_map_s : βˆ€ {a b : Set},
    (a β†’ list b) β†’ list a β†’ list b.

  Parameter concat_map_e : βˆ€ {_error a b : Set},
    (a β†’ Pervasives.result (list b) _error) β†’ list a β†’
    Pervasives.result (list b) _error.

  Parameter concat_map_es : βˆ€ {_error a b : Set},
    (a β†’ Pervasives.result (list b) _error) β†’ list a β†’
    Pervasives.result (list b) _error.

  Parameter concat_map_p : βˆ€ {a b : Set},
    (a β†’ list b) β†’ list a β†’ list b.

  Parameter fold_left : βˆ€ {a b : Set}, (a β†’ b β†’ a) β†’ a β†’ list b β†’ a.

  Parameter fold_left_e : βˆ€ {a b trace : Set},
    (a β†’ b β†’ Pervasives.result a trace) β†’ a β†’ list b β†’
    Pervasives.result a trace.

  Parameter fold_left_s : βˆ€ {a b : Set}, (a β†’ b β†’ a) β†’ a β†’ list b β†’ a.

  Parameter fold_left_es : βˆ€ {a b trace : Set},
    (a β†’ b β†’ Pervasives.result a trace) β†’ a β†’ list b β†’
    Pervasives.result a trace.

  Parameter fold_left_map : βˆ€ {a b c : Set},
    (a β†’ b β†’ a Γ— c) β†’ a β†’ list b β†’ a Γ— list c.

  Parameter fold_left_map_e : βˆ€ {a b c trace : Set},
    (a β†’ b β†’ Pervasives.result (a Γ— c) trace) β†’ a β†’ list b β†’
    Pervasives.result (a Γ— list c) trace.

  Parameter fold_left_map_s : βˆ€ {a b c : Set},
    (a β†’ b β†’ a Γ— c) β†’ a β†’ list b β†’ a Γ— list c.

  Parameter fold_left_map_es : βˆ€ {a b c trace : Set},
    (a β†’ b β†’ Pervasives.result (a Γ— c) trace) β†’ a β†’ list b β†’
    Pervasives.result (a Γ— list c) trace.

  Parameter fold_left_i : βˆ€ {a b : Set},
    (int β†’ a β†’ b β†’ a) β†’ a β†’ list b β†’ a.

  Parameter fold_left_i_e : βˆ€ {a b trace : Set},
    (int β†’ a β†’ b β†’ Pervasives.result a trace) β†’ a β†’ list b β†’
    Pervasives.result a trace.

  Parameter fold_left_i_s : βˆ€ {a b : Set},
    (int β†’ a β†’ b β†’ a) β†’ a β†’ list b β†’ a.

  Parameter fold_left_i_es : βˆ€ {a b trace : Set},
    (int β†’ a β†’ b β†’ Pervasives.result a trace) β†’ a β†’ list b β†’
    Pervasives.result a trace.

  Parameter fold_right : βˆ€ {a b : Set}, (a β†’ b β†’ b) β†’ list a β†’ b β†’ b.

  Parameter fold_right_e : βˆ€ {a b trace : Set},
    (a β†’ b β†’ Pervasives.result b trace) β†’ list a β†’ b β†’
    Pervasives.result b trace.

  Parameter fold_right_s : βˆ€ {a b : Set},
    (a β†’ b β†’ b) β†’ list a β†’ b β†’ b.

  Parameter fold_right_es : βˆ€ {a b trace : Set},
    (a β†’ b β†’ Pervasives.result b trace) β†’ list a β†’ b β†’
    Pervasives.result b trace.

  Parameter iter2_e : βˆ€ {a b trace : Set},
    trace β†’ (a β†’ b β†’ Pervasives.result unit trace) β†’ list a β†’ list b β†’
    Pervasives.result unit trace.

  Parameter iter2_s : βˆ€ {a b trace : Set},
    trace β†’ (a β†’ b β†’ unit) β†’ list a β†’ list b β†’
    Pervasives.result unit trace.

  Parameter iter2_es : βˆ€ {a b trace : Set},
    trace β†’ (a β†’ b β†’ Pervasives.result unit trace) β†’ list a β†’ list b β†’
    Pervasives.result unit trace.

  Parameter map2_e : βˆ€ {a b c trace : Set},
    trace β†’ (a β†’ b β†’ Pervasives.result c trace) β†’ list a β†’ list b β†’
    Pervasives.result (list c) trace.

  Parameter map2_s : βˆ€ {a b c trace : Set},
    trace β†’ (a β†’ b β†’ c) β†’ list a β†’ list b β†’
    Pervasives.result (list c) trace.

  Parameter map2_es : βˆ€ {a b c trace : Set},
    trace β†’ (a β†’ b β†’ Pervasives.result c trace) β†’ list a β†’ list b β†’
    Pervasives.result (list c) trace.

  Parameter rev_map2_e : βˆ€ {a b c trace : Set},
    trace β†’ (a β†’ b β†’ Pervasives.result c trace) β†’ list a β†’ list b β†’
    Pervasives.result (list c) trace.

  Parameter rev_map2_s : βˆ€ {a b c trace : Set},
    trace β†’ (a β†’ b β†’ c) β†’ list a β†’ list b β†’
    Pervasives.result (list c) trace.

  Parameter rev_map2_es : βˆ€ {a b c trace : Set},
    trace β†’ (a β†’ b β†’ Pervasives.result c trace) β†’ list a β†’ list b β†’
    Pervasives.result (list c) trace.

  Parameter fold_left2_e : βˆ€ {a b c trace : Set},
    trace β†’ (a β†’ b β†’ c β†’ Pervasives.result a trace) β†’ a β†’ list b β†’
    list c β†’ Pervasives.result a trace.

  Parameter fold_left2_s : βˆ€ {a b c trace : Set},
    trace β†’ (a β†’ b β†’ c β†’ a) β†’ a β†’ list b β†’ list c β†’
    Pervasives.result a trace.

  Parameter fold_left2_es : βˆ€ {a b c trace : Set},
    trace β†’ (a β†’ b β†’ c β†’ Pervasives.result a trace) β†’ a β†’ list b β†’
    list c β†’ Pervasives.result a trace.

  Parameter fold_right2_e : βˆ€ {a b c trace : Set},
    trace β†’ (a β†’ b β†’ c β†’ Pervasives.result c trace) β†’ list a β†’ list b β†’
    c β†’ Pervasives.result c trace.

  Parameter fold_right2_s : βˆ€ {a b c trace : Set},
    trace β†’ (a β†’ b β†’ c β†’ c) β†’ list a β†’ list b β†’ c β†’
    Pervasives.result c trace.

  Parameter fold_right2_es : βˆ€ {a b c trace : Set},
    trace β†’ (a β†’ b β†’ c β†’ Pervasives.result c trace) β†’ list a β†’ list b β†’
    c β†’ Pervasives.result c trace.

  Parameter for_all : βˆ€ {a : Set}, (a β†’ bool) β†’ list a β†’ bool.

  Parameter for_all_e : βˆ€ {a trace : Set},
    (a β†’ Pervasives.result bool trace) β†’ list a β†’
    Pervasives.result bool trace.

  Parameter for_all_s : βˆ€ {a : Set}, (a β†’ bool) β†’ list a β†’ bool.

  Parameter for_all_es : βˆ€ {a trace : Set},
    (a β†’ Pervasives.result bool trace) β†’ list a β†’
    Pervasives.result bool trace.

  Parameter for_all_p : βˆ€ {a : Set}, (a β†’ bool) β†’ list a β†’ bool.

  Parameter _exists : βˆ€ {a : Set}, (a β†’ bool) β†’ list a β†’ bool.

  Parameter exists_e : βˆ€ {a trace : Set},
    (a β†’ Pervasives.result bool trace) β†’ list a β†’
    Pervasives.result bool trace.

  Parameter exists_s : βˆ€ {a : Set}, (a β†’ bool) β†’ list a β†’ bool.

  Parameter exists_es : βˆ€ {a trace : Set},
    (a β†’ Pervasives.result bool trace) β†’ list a β†’
    Pervasives.result bool trace.

  Parameter exists_p : βˆ€ {a : Set}, (a β†’ bool) β†’ list a β†’ bool.

  Parameter for_all2_e : βˆ€ {a b trace : Set},
    trace β†’ (a β†’ b β†’ Pervasives.result bool trace) β†’ list a β†’ list b β†’
    Pervasives.result bool trace.

  Parameter for_all2_s : βˆ€ {a b trace : Set},
    trace β†’ (a β†’ b β†’ bool) β†’ list a β†’ list b β†’
    Pervasives.result bool trace.

  Parameter for_all2_es : βˆ€ {a b trace : Set},
    trace β†’ (a β†’ b β†’ Pervasives.result bool trace) β†’ list a β†’ list b β†’
    Pervasives.result bool trace.

  Parameter exists2_e : βˆ€ {a b trace : Set},
    trace β†’ (a β†’ b β†’ Pervasives.result bool trace) β†’ list a β†’ list b β†’
    Pervasives.result bool trace.

  Parameter exists2_s : βˆ€ {a b trace : Set},
    trace β†’ (a β†’ b β†’ bool) β†’ list a β†’ list b β†’
    Pervasives.result bool trace.

  Parameter exists2_es : βˆ€ {a b trace : Set},
    trace β†’ (a β†’ b β†’ Pervasives.result bool trace) β†’ list a β†’ list b β†’
    Pervasives.result bool trace.

  Parameter combine_drop : βˆ€ {a b : Set}, list a β†’ list b β†’ list (a Γ— b).

  Parameter combine_with_leftovers : βˆ€ {a b : Set},
    list a β†’ list b β†’ list (a Γ— b) Γ— option (Either.t (list a) (list b)).

  Parameter product : βˆ€ {a b : Set}, list a β†’ list b β†’ list (a Γ— b).

  Parameter compare : βˆ€ {a : Set},
    (a β†’ a β†’ int) β†’ list a β†’ list a β†’ int.

  Parameter compare_lengths : βˆ€ {a b : Set}, list a β†’ list b β†’ int.

  Parameter compare_length_with : βˆ€ {a : Set}, list a β†’ int β†’ int.

  Parameter equal : βˆ€ {a : Set},
    (a β†’ a β†’ bool) β†’ list a β†’ list a β†’ bool.

  Parameter sort : βˆ€ {a : Set}, (a β†’ a β†’ int) β†’ list a β†’ list a.

  Parameter stable_sort : βˆ€ {a : Set}, (a β†’ a β†’ int) β†’ list a β†’ list a.

  Parameter fast_sort : βˆ€ {a : Set}, (a β†’ a β†’ int) β†’ list a β†’ list a.

  Parameter sort_uniq : βˆ€ {a : Set}, (a β†’ a β†’ int) β†’ list a β†’ list a.

  Parameter to_seq : βˆ€ {a : Set}, list a β†’ Seq.t a.

  Parameter of_seq : βˆ€ {a : Set}, Seq.t a β†’ list a.

  Parameter init_ep : βˆ€ {_error a : Set},
    _error β†’ int β†’ (int β†’ M? a) β†’ M? (list a).

  Parameter filter_ep : βˆ€ {a : Set},
    (a β†’ M? bool) β†’ list a β†’ M? (list a).

  Parameter partition_ep : βˆ€ {a : Set},
    (a β†’ M? bool) β†’ list a β†’ M? (list a Γ— list a).

  Parameter partition_map_ep : βˆ€ {a b c : Set},
    (a β†’ M? (Either.t b c)) β†’ list a β†’ M? (list b Γ— list c).

  Parameter iter_ep : βˆ€ {a : Set}, (a β†’ M? unit) β†’ list a β†’ M? unit.

  Parameter iteri_ep : βˆ€ {a : Set},
    (int β†’ a β†’ M? unit) β†’ list a β†’ M? unit.

  Parameter map_ep : βˆ€ {a b : Set}, (a β†’ M? b) β†’ list a β†’ M? (list b).

  Parameter mapi_ep : βˆ€ {a b : Set},
    (int β†’ a β†’ M? b) β†’ list a β†’ M? (list b).

  Parameter rev_map_ep : βˆ€ {a b : Set},
    (a β†’ M? b) β†’ list a β†’ M? (list b).

  Parameter rev_mapi_ep : βˆ€ {a b : Set},
    (int β†’ a β†’ M? b) β†’ list a β†’ M? (list b).

  Parameter filter_map_ep : βˆ€ {a b : Set},
    (a β†’ M? (option b)) β†’ list a β†’ M? (list b).

  Parameter concat_map_ep : βˆ€ {a b : Set},
    (a β†’ M? (list b)) β†’ list a β†’ M? (list b).

  Parameter for_all_ep : βˆ€ {a : Set}, (a β†’ M? bool) β†’ list a β†’ M? bool.

  Parameter exists_ep : βˆ€ {a : Set}, (a β†’ M? bool) β†’ list a β†’ M? bool.
End List_signature.
Require Export TezosOfOCaml.Environment.V7.List.
Module List_check : List_signature := List.

Module Type Array_signature.
  Definition t (a : Set) : Set := array a.

  Parameter concat : βˆ€ {a : Set}, list (t a) β†’ t a.

  Parameter length : βˆ€ {a : Set}, t a β†’ int.

  Parameter to_list : βˆ€ {a : Set}, t a β†’ list a.

  Parameter get : Variant.t.

  Parameter unsafe_get : Variant.t.

  Parameter set : Variant.t.

  Parameter unsafe_set : Variant.t.

  Parameter to_seq : Variant.t.

  Parameter to_seqi : Variant.t.

  Parameter make : Variant.t.

  Parameter create : Variant.t.

  Parameter make_matrix : Variant.t.

  Parameter create_float : Variant.t.

  Parameter make_float : Variant.t.

  Parameter sub : Variant.t.

  Parameter fill : Variant.t.

  Parameter blit : Variant.t.

  Parameter iter2 : Variant.t.

  Parameter map2 : Variant.t.

  Parameter combine : Variant.t.

  Parameter sort : Variant.t.

  Parameter stable_sort : Variant.t.

  Parameter fast_sort : Variant.t.

  Module Floatarray.

  End Floatarray.
End Array_signature.
Require Export TezosOfOCaml.Environment.V7.Array.
Module Array_check : Array_signature := Array.

Module Type _Set_signature.
  Module S.
    Record signature {elt t : Set} : Set := {
      elt := elt;
      t := t;
      empty : t;
      is_empty : t β†’ bool;
      mem : elt β†’ t β†’ bool;
      add : elt β†’ t β†’ t;
      singleton : elt β†’ t;
      remove : elt β†’ t β†’ t;
      union : t β†’ t β†’ t;
      inter : t β†’ t β†’ t;
      disjoint : t β†’ t β†’ bool;
      diff_value : t β†’ t β†’ t;
      compare : t β†’ t β†’ int;
      equal : t β†’ t β†’ bool;
      subset : t β†’ t β†’ bool;
      iter : (elt β†’ unit) β†’ t β†’ unit;
      iter_e :
        βˆ€ {trace : Set},
        (elt β†’ Pervasives.result unit trace) β†’ t β†’
        Pervasives.result unit trace;
      iter_s : (elt β†’ unit) β†’ t β†’ unit;
      iter_p : (elt β†’ unit) β†’ t β†’ unit;
      iter_es :
        βˆ€ {trace : Set},
        (elt β†’ Pervasives.result unit trace) β†’ t β†’
        Pervasives.result unit trace;
      map : (elt β†’ elt) β†’ t β†’ t;
      fold : βˆ€ {a : Set}, (elt β†’ a β†’ a) β†’ t β†’ a β†’ a;
      fold_e :
        βˆ€ {a trace : Set},
        (elt β†’ a β†’ Pervasives.result a trace) β†’ t β†’ a β†’
        Pervasives.result a trace;
      fold_s : βˆ€ {a : Set}, (elt β†’ a β†’ a) β†’ t β†’ a β†’ a;
      fold_es :
        βˆ€ {a trace : Set},
        (elt β†’ a β†’ Pervasives.result a trace) β†’ t β†’ a β†’
        Pervasives.result a trace;
      for_all : (elt β†’ bool) β†’ t β†’ bool;
      _exists : (elt β†’ bool) β†’ t β†’ bool;
      filter : (elt β†’ bool) β†’ t β†’ t;
      filter_map : (elt β†’ option elt) β†’ t β†’ t;
      partition : (elt β†’ bool) β†’ t β†’ t Γ— t;
      cardinal : t β†’ int;
      elements : t β†’ list elt;
      min_elt : t β†’ option elt;
      min_elt_opt : t β†’ option elt;
      max_elt : t β†’ option elt;
      max_elt_opt : t β†’ option elt;
      choose : t β†’ option elt;
      choose_opt : t β†’ option elt;
      split : elt β†’ t β†’ t Γ— bool Γ— t;
      find : elt β†’ t β†’ option elt;
      find_opt : elt β†’ t β†’ option elt;
      find_first : (elt β†’ bool) β†’ t β†’ option elt;
      find_first_opt : (elt β†’ bool) β†’ t β†’ option elt;
      find_last : (elt β†’ bool) β†’ t β†’ option elt;
      find_last_opt : (elt β†’ bool) β†’ t β†’ option elt;
      of_list : list elt β†’ t;
      to_seq_from : elt β†’ t β†’ Seq.t elt;
      to_seq : t β†’ Seq.t elt;
      to_rev_seq : t β†’ Seq.t elt;
      add_seq : Seq.t elt β†’ t β†’ t;
      of_seq : Seq.t elt β†’ t;
      iter_ep : (elt β†’ M? unit) β†’ t β†’ M? unit;
    }.
  End S.
  Definition S := @S.signature.
  Arguments S {_ _}.

  Parameter Make_t :
    βˆ€ {Ord_t : Set} (Ord : Compare.COMPARABLE (t := Ord_t)), Set.

  Parameter Make :
    βˆ€ {Ord_t : Set},
    βˆ€ (Ord : Compare.COMPARABLE (t := Ord_t)),
    S (elt := Ord.(Compare.COMPARABLE.t)) (t := Make_t Ord).
End _Set_signature.
Require Export TezosOfOCaml.Environment.V7._Set.
Module _Set_check : _Set_signature := _Set.

Module Type Map_signature.
  Module S.
    Record signature {key : Set} {t : Set β†’ Set} : Set := {
      key := key;
      t := t;
      empty : βˆ€ {a : Set}, t a;
      is_empty : βˆ€ {a : Set}, t a β†’ bool;
      mem : βˆ€ {a : Set}, key β†’ t a β†’ bool;
      add : βˆ€ {a : Set}, key β†’ a β†’ t a β†’ t a;
      update : βˆ€ {a : Set}, key β†’ (option a β†’ option a) β†’ t a β†’ t a;
      singleton : βˆ€ {a : Set}, key β†’ a β†’ t a;
      remove : βˆ€ {a : Set}, key β†’ t a β†’ t a;
      merge :
        βˆ€ {a b c : Set},
        (key β†’ option a β†’ option b β†’ option c) β†’ t a β†’ t b β†’ t c;
      union :
        βˆ€ {a : Set}, (key β†’ a β†’ a β†’ option a) β†’ t a β†’ t a β†’ t a;
      compare : βˆ€ {a : Set}, (a β†’ a β†’ int) β†’ t a β†’ t a β†’ int;
      equal : βˆ€ {a : Set}, (a β†’ a β†’ bool) β†’ t a β†’ t a β†’ bool;
      iter : βˆ€ {a : Set}, (key β†’ a β†’ unit) β†’ t a β†’ unit;
      
[iter_e f m] applies [f] to the bindings of [m] one by one in an unspecified order. If all the applications result in [Ok ()], then the result of the iteration is [Ok ()]. If any of the applications results in [Error e] then the iteration stops and the result of the iteration is [Error e].
      iter_e :
        βˆ€ {a trace : Set},
        (key β†’ a β†’ Pervasives.result unit trace) β†’ t a β†’
        Pervasives.result unit trace;
      iter_s : βˆ€ {a : Set}, (key β†’ a β†’ unit) β†’ t a β†’ unit;
      iter_p : βˆ€ {a : Set}, (key β†’ a β†’ unit) β†’ t a β†’ unit;
      
[iter_es f m] applies [f] to the bindings of [m] in an unspecified order, one after the other as the promises resolve. If all the applications result in [Ok ()], then the result of the iteration is [Ok ()]. If any of the applications results in [Error e] then the iteration stops and the result of the iteration is [Error e].
      iter_es :
        βˆ€ {a trace : Set},
        (key β†’ a β†’ Pervasives.result unit trace) β†’ t a β†’
        Pervasives.result unit trace;
      fold : βˆ€ {a b : Set}, (key β†’ a β†’ b β†’ b) β†’ t a β†’ b β†’ b;
      
[fold_e f m init] is [f k1 d1 init >>? fun acc -> f k2 d2 acc >>? fun acc -> …] where [kN] is the key bound to [dN] in [m].
      fold_e :
        βˆ€ {a b trace : Set},
        (key β†’ a β†’ b β†’ Pervasives.result b trace) β†’ t a β†’ b β†’
        Pervasives.result b trace;
      fold_s : βˆ€ {a b : Set}, (key β†’ a β†’ b β†’ b) β†’ t a β†’ b β†’ b;
      
[fold_es f m init] is [f k1 d1 init >>=? fun acc -> f k2 d2 acc >>=? fun acc -> …] where [kN] is the key bound to [dN] in [m].
      fold_es :
        βˆ€ {a b trace : Set},
        (key β†’ a β†’ b β†’ Pervasives.result b trace) β†’ t a β†’ b β†’
        Pervasives.result b trace;
      for_all : βˆ€ {a : Set}, (key β†’ a β†’ bool) β†’ t a β†’ bool;
      _exists : βˆ€ {a : Set}, (key β†’ a β†’ bool) β†’ t a β†’ bool;
      filter : βˆ€ {a : Set}, (key β†’ a β†’ bool) β†’ t a β†’ t a;
      filter_map : βˆ€ {a b : Set}, (key β†’ a β†’ option b) β†’ t a β†’ t b;
      partition : βˆ€ {a : Set}, (key β†’ a β†’ bool) β†’ t a β†’ t a Γ— t a;
      cardinal : βˆ€ {a : Set}, t a β†’ int;
      bindings : βˆ€ {a : Set}, t a β†’ list (key Γ— a);
      min_binding : βˆ€ {a : Set}, t a β†’ option (key Γ— a);
      min_binding_opt : βˆ€ {a : Set}, t a β†’ option (key Γ— a);
      max_binding : βˆ€ {a : Set}, t a β†’ option (key Γ— a);
      max_binding_opt : βˆ€ {a : Set}, t a β†’ option (key Γ— a);
      choose : βˆ€ {a : Set}, t a β†’ option (key Γ— a);
      choose_opt : βˆ€ {a : Set}, t a β†’ option (key Γ— a);
      split : βˆ€ {a : Set}, key β†’ t a β†’ t a Γ— option a Γ— t a;
      find : βˆ€ {a : Set}, key β†’ t a β†’ option a;
      find_opt : βˆ€ {a : Set}, key β†’ t a β†’ option a;
      find_first : βˆ€ {a : Set}, (key β†’ bool) β†’ t a β†’ option (key Γ— a);
      find_first_opt :
        βˆ€ {a : Set}, (key β†’ bool) β†’ t a β†’ option (key Γ— a);
      find_last : βˆ€ {a : Set}, (key β†’ bool) β†’ t a β†’ option (key Γ— a);
      find_last_opt :
        βˆ€ {a : Set}, (key β†’ bool) β†’ t a β†’ option (key Γ— a);
      map : βˆ€ {a b : Set}, (a β†’ b) β†’ t a β†’ t b;
      mapi : βˆ€ {a b : Set}, (key β†’ a β†’ b) β†’ t a β†’ t b;
      to_seq : βˆ€ {a : Set}, t a β†’ Seq.t (key Γ— a);
      to_rev_seq : βˆ€ {a : Set}, t a β†’ Seq.t (key Γ— a);
      to_seq_from : βˆ€ {a : Set}, key β†’ t a β†’ Seq.t (key Γ— a);
      add_seq : βˆ€ {a : Set}, Seq.t (key Γ— a) β†’ t a β†’ t a;
      of_seq : βˆ€ {a : Set}, Seq.t (key Γ— a) β†’ t a;
      iter_ep :
    βˆ€ {a _error: Set},
    (key β†’ a β†’ Pervasives.result unit (Error_monad.trace _error)) β†’
    t a β†’
    Pervasives.result unit (Error_monad.trace _error);

    }.
  End S.
  Definition S := @S.signature.
  Arguments S {_ _}.

  Parameter Make_t :
    βˆ€ {Ord_t : Set} (Ord : Compare.COMPARABLE (t := Ord_t)), Set β†’ Set.

  Parameter Make :
    βˆ€ {Ord_t : Set},
    βˆ€ (Ord : Compare.COMPARABLE (t := Ord_t)),
    S (key := Ord.(Compare.COMPARABLE.t)) (t := Make_t Ord).
End Map_signature.
Require Export TezosOfOCaml.Environment.V7.Map.
Module Map_check : Map_signature := Map.

Module Type Option_signature.
  Definition t (a : Set) : Set := option a.

  Parameter none : βˆ€ {a : Set}, option a.

  Parameter none_e : βˆ€ {a trace : Set}, Pervasives.result (option a) trace.

  Parameter none_s : βˆ€ {a : Set}, option a.

  Parameter none_es : βˆ€ {a trace : Set},
    Pervasives.result (option a) trace.

  Parameter some : βˆ€ {a : Set}, a β†’ option a.

  Parameter some_unit : option unit.

  Parameter some_nil : βˆ€ {a : Set}, option (list a).

  Parameter some_e : βˆ€ {a trace : Set},
    a β†’ Pervasives.result (option a) trace.

  Parameter some_s : βˆ€ {a : Set}, a β†’ option a.

  Parameter some_es : βˆ€ {a trace : Set},
    a β†’ Pervasives.result (option a) trace.

  Parameter value_value : βˆ€ {a : Set}, option a β†’ a β†’ a.

  Parameter value_e : βˆ€ {a trace : Set},
    option a β†’ trace β†’ Pervasives.result a trace.

  Parameter value_f : βˆ€ {a : Set}, option a β†’ (unit β†’ a) β†’ a.

  Parameter value_fe : βˆ€ {a trace : Set},
    option a β†’ (unit β†’ trace) β†’ Pervasives.result a trace.

  Parameter bind : βˆ€ {a b : Set}, option a β†’ (a β†’ option b) β†’ option b.

  Parameter join : βˆ€ {a : Set}, option (option a) β†’ option a.

  Parameter either : βˆ€ {a : Set}, option a β†’ option a β†’ option a.

  Parameter map : βˆ€ {a b : Set}, (a β†’ b) β†’ option a β†’ option b.

  Parameter map_s : βˆ€ {a b : Set}, (a β†’ b) β†’ option a β†’ option b.

  Parameter map_e : βˆ€ {a b trace : Set},
    (a β†’ Pervasives.result b trace) β†’ option a β†’
    Pervasives.result (option b) trace.

  Parameter map_es : βˆ€ {a b trace : Set},
    (a β†’ Pervasives.result b trace) β†’ option a β†’
    Pervasives.result (option b) trace.

  Parameter fold : βˆ€ {a b : Set}, a β†’ (b β†’ a) β†’ option b β†’ a.

  Parameter fold_s : βˆ€ {a b : Set}, a β†’ (b β†’ a) β†’ option b β†’ a.

  Parameter fold_f : βˆ€ {a b : Set},
    (unit β†’ a) β†’ (b β†’ a) β†’ option b β†’ a.

  Parameter iter : βˆ€ {a : Set}, (a β†’ unit) β†’ option a β†’ unit.

  Parameter iter_s : βˆ€ {a : Set}, (a β†’ unit) β†’ option a β†’ unit.

  Parameter iter_e : βˆ€ {a trace : Set},
    (a β†’ Pervasives.result unit trace) β†’ option a β†’
    Pervasives.result unit trace.

  Parameter iter_es : βˆ€ {a trace : Set},
    (a β†’ Pervasives.result unit trace) β†’ option a β†’
    Pervasives.result unit trace.

  Parameter is_none : βˆ€ {a : Set}, option a β†’ bool.

  Parameter is_some : βˆ€ {a : Set}, option a β†’ bool.

  Parameter equal : βˆ€ {a : Set},
    (a β†’ a β†’ bool) β†’ option a β†’ option a β†’ bool.

  Parameter compare : βˆ€ {a : Set},
    (a β†’ a β†’ int) β†’ option a β†’ option a β†’ int.

  Parameter to_result : βˆ€ {a trace : Set},
    trace β†’ option a β†’ Pervasives.result a trace.

  Parameter of_result : βˆ€ {a e : Set}, Pervasives.result a e β†’ option a.

  Parameter to_list : βˆ€ {a : Set}, option a β†’ list a.

  Parameter to_seq : βˆ€ {a : Set}, option a β†’ Seq.t a.

  Parameter catch : βˆ€ {a : Set},
    option (extensible_type β†’ bool) β†’ (unit β†’ a) β†’ option a.

  Parameter catch_s : βˆ€ {a : Set},
    option (extensible_type β†’ bool) β†’ (unit β†’ a) β†’ option a.
End Option_signature.
Require Export TezosOfOCaml.Environment.V7.Option.
Module Option_check : Option_signature := Option.

Module Type Result_signature.
  Definition t (a e : Set) : Set := Pervasives.result a e.

  Parameter ok : βˆ€ {a e : Set}, a β†’ Pervasives.result a e.

  Parameter ok_s : βˆ€ {a e : Set}, a β†’ Pervasives.result a e.

  Parameter error_value : βˆ€ {a e : Set}, e β†’ Pervasives.result a e.

  Parameter error_s : βˆ€ {a e : Set}, e β†’ Pervasives.result a e.

  Parameter _return : βˆ€ {a e : Set}, a β†’ Pervasives.result a e.

  Parameter return_unit : βˆ€ {e : Set}, Pervasives.result unit e.

  Parameter return_none : βˆ€ {a e : Set}, Pervasives.result (option a) e.

  Parameter return_some : βˆ€ {a e : Set},
    a β†’ Pervasives.result (option a) e.

  Parameter return_nil : βˆ€ {a e : Set}, Pervasives.result (list a) e.

  Parameter return_true : βˆ€ {e : Set}, Pervasives.result bool e.

  Parameter return_false : βˆ€ {e : Set}, Pervasives.result bool e.

  Parameter value_value : βˆ€ {a e : Set}, Pervasives.result a e β†’ a β†’ a.

  Parameter value_f : βˆ€ {a e : Set},
    Pervasives.result a e β†’ (unit β†’ a) β†’ a.

  Parameter bind : βˆ€ {a b e : Set},
    Pervasives.result a e β†’ (a β†’ Pervasives.result b e) β†’
    Pervasives.result b e.

  Parameter bind_s : βˆ€ {a b e : Set},
    Pervasives.result a e β†’ (a β†’ Pervasives.result b e) β†’
    Pervasives.result b e.

  Parameter bind_error : βˆ€ {a e f : Set},
    Pervasives.result a e β†’ (e β†’ Pervasives.result a f) β†’
    Pervasives.result a f.

  Parameter bind_error_s : βˆ€ {a e f : Set},
    Pervasives.result a e β†’ (e β†’ Pervasives.result a f) β†’
    Pervasives.result a f.

  Parameter join : βˆ€ {a e : Set},
    Pervasives.result (Pervasives.result a e) e β†’ Pervasives.result a e.

  Parameter map : βˆ€ {a b e : Set},
    (a β†’ b) β†’ Pervasives.result a e β†’ Pervasives.result b e.

  Parameter map_e : βˆ€ {a b e : Set},
    (a β†’ Pervasives.result b e) β†’ Pervasives.result a e β†’
    Pervasives.result b e.

  Parameter map_s : βˆ€ {a b e : Set},
    (a β†’ b) β†’ Pervasives.result a e β†’ Pervasives.result b e.

  Parameter map_es : βˆ€ {a b e : Set},
    (a β†’ Pervasives.result b e) β†’ Pervasives.result a e β†’
    Pervasives.result b e.

  Parameter map_error : βˆ€ {a e f : Set},
    (e β†’ f) β†’ Pervasives.result a e β†’ Pervasives.result a f.

  Parameter map_error_e : βˆ€ {a e f : Set},
    (e β†’ Pervasives.result a f) β†’ Pervasives.result a e β†’
    Pervasives.result a f.

  Parameter map_error_s : βˆ€ {a e f : Set},
    (e β†’ f) β†’ Pervasives.result a e β†’ Pervasives.result a f.

  Parameter map_error_es : βˆ€ {a e f : Set},
    (e β†’ Pervasives.result a f) β†’ Pervasives.result a e β†’
    Pervasives.result a f.

  Parameter fold : βˆ€ {a c e : Set},
    (a β†’ c) β†’ (e β†’ c) β†’ Pervasives.result a e β†’ c.

  Parameter iter : βˆ€ {a e : Set},
    (a β†’ unit) β†’ Pervasives.result a e β†’ unit.

  Parameter iter_s : βˆ€ {a e : Set},
    (a β†’ unit) β†’ Pervasives.result a e β†’ unit.

  Parameter iter_error : βˆ€ {a e : Set},
    (e β†’ unit) β†’ Pervasives.result a e β†’ unit.

  Parameter iter_error_s : βˆ€ {a e : Set},
    (e β†’ unit) β†’ Pervasives.result a e β†’ unit.

  Parameter is_ok : βˆ€ {a e : Set}, Pervasives.result a e β†’ bool.

  Parameter is_error : βˆ€ {a e : Set}, Pervasives.result a e β†’ bool.

  Parameter equal : βˆ€ {a e : Set},
    (a β†’ a β†’ bool) β†’ (e β†’ e β†’ bool) β†’ Pervasives.result a e β†’
    Pervasives.result a e β†’ bool.

  Parameter compare : βˆ€ {a e : Set},
    (a β†’ a β†’ int) β†’ (e β†’ e β†’ int) β†’ Pervasives.result a e β†’
    Pervasives.result a e β†’ int.

  Parameter to_option : βˆ€ {a e : Set}, Pervasives.result a e β†’ option a.

  Parameter of_option : βˆ€ {a e : Set},
    e β†’ option a β†’ Pervasives.result a e.

  Parameter to_list : βˆ€ {a e : Set}, Pervasives.result a e β†’ list a.

  Parameter to_seq : βˆ€ {a e : Set}, Pervasives.result a e β†’ Seq.t a.

  Parameter catch : βˆ€ {a : Set},
    option (extensible_type β†’ bool) β†’ (unit β†’ a) β†’
    Pervasives.result a extensible_type.

  Parameter catch_f : βˆ€ {_error a : Set},
    option (extensible_type β†’ bool) β†’ (unit β†’ a) β†’
    (extensible_type β†’ _error) β†’ Pervasives.result a _error.

  Parameter catch_s : βˆ€ {a : Set},
    option (extensible_type β†’ bool) β†’ (unit β†’ a) β†’
    Pervasives.result a extensible_type.
End Result_signature.
Require Export TezosOfOCaml.Environment.V7.Result.
Module Result_check : Result_signature := Result.

Module Type RPC_arg_signature.
  Parameter t : βˆ€ (a : Set), Set.

  Definition arg (a : Set) : Set := t a.

  Parameter make : βˆ€ {a : Set},
    option string β†’ string β†’ (string β†’ Pervasives.result a string) β†’
    (a β†’ string) β†’ unit β†’ arg a.

  Module descr.
    Record record : Set := Build {
      name : string;
      descr : option string;
    }.
    Definition with_name name (r : record) :=
      Build name r.(descr).
    Definition with_descr descr (r : record) :=
      Build r.(name) descr.
  End descr.
  Definition descr := descr.record.

  Parameter descr_value : βˆ€ {a : Set}, arg a β†’ descr.

  Parameter bool_value : arg bool.

  Parameter int_value : arg int.

  Parameter uint : arg int.

  Parameter int32_value : arg int32.

  Parameter uint31 : arg int32.

  Parameter int64_value : arg int64.

  Parameter uint63 : arg int64.

  Parameter string_value : arg string.

  Parameter like : βˆ€ {a : Set}, arg a β†’ option string β†’ string β†’ arg a.

  Inductive eq (a : Set) : Set :=
  | Eq : eq a.

  Arguments Eq {_}.

  Parameter eq_value : βˆ€ {a b : Set}, arg a β†’ arg b β†’ option (eq a).
End RPC_arg_signature.
Require Export TezosOfOCaml.Environment.V7.RPC_arg.
Module RPC_arg_check : RPC_arg_signature := RPC_arg.

Module Type RPC_path_signature.
  Parameter t : βˆ€ (prefix params : Set), Set.

  Definition path (prefix params : Set) : Set := t prefix params.

  Definition context (prefix : Set) : Set := path prefix prefix.

  Parameter root_value : context unit.

  Parameter open_root : βˆ€ {a : Set}, context a.

  Parameter add_suffix : βˆ€ {params prefix : Set},
    path prefix params β†’ string β†’ path prefix params.

  Parameter op_div : βˆ€ {params prefix : Set},
    path prefix params β†’ string β†’ path prefix params.

  Parameter add_arg : βˆ€ {a params prefix : Set},
    path prefix params β†’ RPC_arg.t a β†’ path prefix (params Γ— a).

  Parameter op_divcolon : βˆ€ {a params prefix : Set},
    path prefix params β†’ RPC_arg.t a β†’ path prefix (params Γ— a).

  Parameter add_final_args : βˆ€ {a params prefix : Set},
    path prefix params β†’ RPC_arg.t a β†’ path prefix (params Γ— list a).

  Parameter op_divcolonstar : βˆ€ {a params prefix : Set},
    path prefix params β†’ RPC_arg.t a β†’ path prefix (params Γ— list a).
End RPC_path_signature.
Require Export TezosOfOCaml.Environment.V7.RPC_path.
Module RPC_path_check : RPC_path_signature := RPC_path.

Module Type RPC_query_signature.
  Parameter t : βˆ€ (a : Set), Set.

  Definition query (a : Set) : Set := t a.

  Parameter empty : query unit.

  Parameter field : βˆ€ (a b : Set), Set.

  Parameter field_value : βˆ€ {a b : Set},
    option string β†’ string β†’ RPC_arg.t a β†’ a β†’ (b β†’ a) β†’ field b a.

  Parameter opt_field : βˆ€ {a b : Set},
    option string β†’ string β†’ RPC_arg.t a β†’ (b β†’ option a) β†’
    field b (option a).

  Parameter flag : βˆ€ {b : Set},
    option string β†’ string β†’ (b β†’ bool) β†’ field b bool.

  Parameter multi_field : βˆ€ {a b : Set},
    option string β†’ string β†’ RPC_arg.t a β†’ (b β†’ list a) β†’ field b (list a).

  Parameter open_query : βˆ€ (a b c : Set), Set.

  Parameter query_value : βˆ€ {a b : Set}, b β†’ open_query a b b.

  Parameter op_pipeplus : βˆ€ {a b c d : Set},
    open_query a b (c β†’ d) β†’ field a c β†’ open_query a b d.

  Parameter seal : βˆ€ {a b : Set}, open_query a b a β†’ t a.

  Definition untyped : Set := list (string Γ— string).

  Parameter parse : βˆ€ {a : Set}, query a β†’ untyped β†’ a.
End RPC_query_signature.
Require Export TezosOfOCaml.Environment.V7.RPC_query.
Module RPC_query_check : RPC_query_signature := RPC_query.

Module Type RPC_service_signature.
  Inductive meth : Set :=
  | PUT : meth
  | GET : meth
  | DELETE : meth
  | POST : meth
  | PATCH : meth.

  Parameter t : βˆ€ (prefix params query input output : Set), Set.

  Definition service (prefix params query input output : Set) : Set :=
    t prefix params query input output.

  Parameter get_service : βˆ€ {output params prefix query : Set},
    option string β†’ RPC_query.t query β†’ Data_encoding.t output β†’
    RPC_path.t prefix params β†’ service prefix params query unit output.

  Parameter post_service : βˆ€ {input output params prefix query : Set},
    option string β†’ RPC_query.t query β†’ Data_encoding.t input β†’
    Data_encoding.t output β†’ RPC_path.t prefix params β†’
    service prefix params query input output.

  Parameter delete_service : βˆ€ {output params prefix query : Set},
    option string β†’ RPC_query.t query β†’ Data_encoding.t output β†’
    RPC_path.t prefix params β†’ service prefix params query unit output.

  Parameter patch_service : βˆ€ {input output params prefix query : Set},
    option string β†’ RPC_query.t query β†’ Data_encoding.t input β†’
    Data_encoding.t output β†’ RPC_path.t prefix params β†’
    service prefix params query input output.

  Parameter put_service : βˆ€ {input output params prefix query : Set},
    option string β†’ RPC_query.t query β†’ Data_encoding.t input β†’
    Data_encoding.t output β†’ RPC_path.t prefix params β†’
    service prefix params query input output.
End RPC_service_signature.
Require Export TezosOfOCaml.Environment.V7.RPC_service.
Module RPC_service_check : RPC_service_signature := RPC_service.

Module Type RPC_answer_signature.
  Module stream.
    Record record {next shutdown : Set} : Set := Build {
      next : next;
      shutdown : shutdown;
    }.
    Arguments record : clear implicits.
    Definition with_next {t_next t_shutdown} next
      (r : record t_next t_shutdown) :=
      Build t_next t_shutdown next r.(shutdown).
    Definition with_shutdown {t_next t_shutdown} shutdown
      (r : record t_next t_shutdown) :=
      Build t_next t_shutdown r.(next) shutdown.
  End stream.
  Definition stream_skeleton := stream.record.

  Reserved Notation "'stream".

  Inductive t (o : Set) : Set :=
  | OkStream : 'stream o β†’ t o
  | Unauthorized : option (list Error_monad._error) β†’ t o
  | OkChunk : o β†’ t o
  | Error : option (list Error_monad._error) β†’ t o
  | Ok : o β†’ t o
  | Not_found : option (list Error_monad._error) β†’ t o
  | Forbidden : option (list Error_monad._error) β†’ t o
  | Created : option string β†’ t o
  | Conflict : option (list Error_monad._error) β†’ t o
  | No_content : t o
  
  where "'stream" :=
    (fun (t_a : Set) β‡’ stream_skeleton (unit β†’ option t_a) (unit β†’ unit)).

  Definition stream := 'stream.

  Arguments OkStream {_}.
  Arguments Unauthorized {_}.
  Arguments OkChunk {_}.
  Arguments Error {_}.
  Arguments Ok {_}.
  Arguments Not_found {_}.
  Arguments Forbidden {_}.
  Arguments Created {_}.
  Arguments Conflict {_}.
  Arguments No_content {_}.

  Parameter _return : βˆ€ {o : Set}, o β†’ t o.

  Parameter return_chunked : βˆ€ {o : Set}, o β†’ t o.

  Parameter return_stream : βˆ€ {o : Set}, stream o β†’ t o.

  Parameter not_found : βˆ€ {o : Set}, t o.

  Parameter fail : βˆ€ {a : Set}, list Error_monad._error β†’ t a.
End RPC_answer_signature.
Require Export TezosOfOCaml.Environment.V7.RPC_answer.
Module RPC_answer_check : RPC_answer_signature := RPC_answer.

Module Type RPC_directory_signature.
  Parameter t : βˆ€ (prefix : Set), Set.

  Definition directory (prefix : Set) : Set := t prefix.

  Parameter empty : βˆ€ {prefix : Set}, directory prefix.

  Parameter map : βˆ€ {a b : Set}, (a β†’ b) β†’ directory b β†’ directory a.

  Parameter prefix : βˆ€ {p pr : Set},
    RPC_path.path pr p β†’ directory p β†’ directory pr.

  Parameter merge : βˆ€ {a : Set},
    option Variant.t β†’ directory a β†’ directory a β†’ directory a.

  Inductive step : Set :=
  | Static : string β†’ step
  | Dynamic : RPC_arg.descr β†’ step
  | DynamicTail : RPC_arg.descr β†’ step.

  Inductive conflict : Set :=
  | CService : RPC_service.meth β†’ conflict
  | CDir : conflict
  | CBuilder : conflict
  | CDynDescr : string β†’ string β†’ conflict
  | CTail : conflict
  | CTypes : RPC_arg.descr β†’ RPC_arg.descr β†’ conflict
  | CType : RPC_arg.descr β†’ list string β†’ conflict.

  Parameter register : βˆ€ {input output params prefix query : Set},
    bool β†’ directory prefix β†’
    RPC_service.t prefix params query input output β†’
    (params β†’ query β†’ input β†’ Error_monad.tzresult output) β†’
    directory prefix.

  Parameter opt_register : βˆ€ {input output params prefix query : Set},
    bool β†’ directory prefix β†’
    RPC_service.t prefix params query input output β†’
    (params β†’ query β†’ input β†’ Error_monad.tzresult (option output)) β†’
    directory prefix.

  Parameter gen_register : βˆ€ {input output params prefix query : Set},
    directory prefix β†’ RPC_service.t prefix params query input output β†’
    (params β†’ query β†’ input β†’ Variant.t) β†’ directory prefix.

  Parameter lwt_register : βˆ€ {input output params prefix query : Set},
    bool β†’ directory prefix β†’
    RPC_service.t prefix params query input output β†’
    (params β†’ query β†’ input β†’ output) β†’ directory prefix.

  Parameter register0 : βˆ€ {i o q : Set},
    bool β†’ directory unit β†’ RPC_service.t unit unit q i o β†’
    (q β†’ i β†’ Error_monad.tzresult o) β†’ directory unit.

  Parameter register1 : βˆ€ {a i o prefix q : Set},
    bool β†’ directory prefix β†’ RPC_service.t prefix (unit Γ— a) q i o β†’
    (a β†’ q β†’ i β†’ Error_monad.tzresult o) β†’ directory prefix.

  Parameter register2 : βˆ€ {a b i o prefix q : Set},
    bool β†’ directory prefix β†’ RPC_service.t prefix ((unit Γ— a) Γ— b) q i o β†’
    (a β†’ b β†’ q β†’ i β†’ Error_monad.tzresult o) β†’ directory prefix.

  Parameter register3 : βˆ€ {a b c i o prefix q : Set},
    bool β†’ directory prefix β†’
    RPC_service.t prefix (((unit Γ— a) Γ— b) Γ— c) q i o β†’
    (a β†’ b β†’ c β†’ q β†’ i β†’ Error_monad.tzresult o) β†’ directory prefix.

  Parameter register4 : βˆ€ {a b c d i o prefix q : Set},
    bool β†’ directory prefix β†’
    RPC_service.t prefix ((((unit Γ— a) Γ— b) Γ— c) Γ— d) q i o β†’
    (a β†’ b β†’ c β†’ d β†’ q β†’ i β†’ Error_monad.tzresult o) β†’ directory prefix.

  Parameter register5 : βˆ€ {a b c d e i o prefix q : Set},
    bool β†’ directory prefix β†’
    RPC_service.t prefix (((((unit Γ— a) Γ— b) Γ— c) Γ— d) Γ— e) q i o β†’
    (a β†’ b β†’ c β†’ d β†’ e β†’ q β†’ i β†’ Error_monad.tzresult o) β†’
    directory prefix.

  Parameter opt_register0 : βˆ€ {i o q : Set},
    bool β†’ directory unit β†’ RPC_service.t unit unit q i o β†’
    (q β†’ i β†’ Error_monad.tzresult (option o)) β†’ directory unit.

  Parameter opt_register1 : βˆ€ {a i o prefix q : Set},
    bool β†’ directory prefix β†’ RPC_service.t prefix (unit Γ— a) q i o β†’
    (a β†’ q β†’ i β†’ Error_monad.tzresult (option o)) β†’ directory prefix.

  Parameter opt_register2 : βˆ€ {a b i o prefix q : Set},
    bool β†’ directory prefix β†’ RPC_service.t prefix ((unit Γ— a) Γ— b) q i o β†’
    (a β†’ b β†’ q β†’ i β†’ Error_monad.tzresult (option o)) β†’ directory prefix.

  Parameter opt_register3 : βˆ€ {a b c i o prefix q : Set},
    bool β†’ directory prefix β†’
    RPC_service.t prefix (((unit Γ— a) Γ— b) Γ— c) q i o β†’
    (a β†’ b β†’ c β†’ q β†’ i β†’ Error_monad.tzresult (option o)) β†’
    directory prefix.

  Parameter opt_register4 : βˆ€ {a b c d i o prefix q : Set},
    bool β†’ directory prefix β†’
    RPC_service.t prefix ((((unit Γ— a) Γ— b) Γ— c) Γ— d) q i o β†’
    (a β†’ b β†’ c β†’ d β†’ q β†’ i β†’ Error_monad.tzresult (option o)) β†’
    directory prefix.

  Parameter opt_register5 : βˆ€ {a b c d e i o prefix q : Set},
    bool β†’ directory prefix β†’
    RPC_service.t prefix (((((unit Γ— a) Γ— b) Γ— c) Γ— d) Γ— e) q i o β†’
    (a β†’ b β†’ c β†’ d β†’ e β†’ q β†’ i β†’ Error_monad.tzresult (option o)) β†’
    directory prefix.

  Parameter gen_register0 : βˆ€ {i o q : Set},
    directory unit β†’ RPC_service.t unit unit q i o β†’ (q β†’ i β†’ Variant.t) β†’
    directory unit.

  Parameter gen_register1 : βˆ€ {a i o prefix q : Set},
    directory prefix β†’ RPC_service.t prefix (unit Γ— a) q i o β†’
    (a β†’ q β†’ i β†’ Variant.t) β†’ directory prefix.

  Parameter gen_register2 : βˆ€ {a b i o prefix q : Set},
    directory prefix β†’ RPC_service.t prefix ((unit Γ— a) Γ— b) q i o β†’
    (a β†’ b β†’ q β†’ i β†’ Variant.t) β†’ directory prefix.

  Parameter gen_register3 : βˆ€ {a b c i o prefix q : Set},
    directory prefix β†’ RPC_service.t prefix (((unit Γ— a) Γ— b) Γ— c) q i o β†’
    (a β†’ b β†’ c β†’ q β†’ i β†’ Variant.t) β†’ directory prefix.

  Parameter gen_register4 : βˆ€ {a b c d i o prefix q : Set},
    directory prefix β†’
    RPC_service.t prefix ((((unit Γ— a) Γ— b) Γ— c) Γ— d) q i o β†’
    (a β†’ b β†’ c β†’ d β†’ q β†’ i β†’ Variant.t) β†’ directory prefix.

  Parameter gen_register5 : βˆ€ {a b c d e i o prefix q : Set},
    directory prefix β†’
    RPC_service.t prefix (((((unit Γ— a) Γ— b) Γ— c) Γ— d) Γ— e) q i o β†’
    (a β†’ b β†’ c β†’ d β†’ e β†’ q β†’ i β†’ Variant.t) β†’ directory prefix.

  Parameter lwt_register0 : βˆ€ {i o q : Set},
    bool β†’ directory unit β†’ RPC_service.t unit unit q i o β†’ (q β†’ i β†’ o) β†’
    directory unit.

  Parameter lwt_register1 : βˆ€ {a i o prefix q : Set},
    bool β†’ directory prefix β†’ RPC_service.t prefix (unit Γ— a) q i o β†’
    (a β†’ q β†’ i β†’ o) β†’ directory prefix.

  Parameter lwt_register2 : βˆ€ {a b i o prefix q : Set},
    bool β†’ directory prefix β†’ RPC_service.t prefix ((unit Γ— a) Γ— b) q i o β†’
    (a β†’ b β†’ q β†’ i β†’ o) β†’ directory prefix.

  Parameter lwt_register3 : βˆ€ {a b c i o prefix q : Set},
    bool β†’ directory prefix β†’
    RPC_service.t prefix (((unit Γ— a) Γ— b) Γ— c) q i o β†’
    (a β†’ b β†’ c β†’ q β†’ i β†’ o) β†’ directory prefix.

  Parameter lwt_register4 : βˆ€ {a b c d i o prefix q : Set},
    bool β†’ directory prefix β†’
    RPC_service.t prefix ((((unit Γ— a) Γ— b) Γ— c) Γ— d) q i o β†’
    (a β†’ b β†’ c β†’ d β†’ q β†’ i β†’ o) β†’ directory prefix.

  Parameter lwt_register5 : βˆ€ {a b c d e i o prefix q : Set},
    bool β†’ directory prefix β†’
    RPC_service.t prefix (((((unit Γ— a) Γ— b) Γ— c) Γ— d) Γ— e) q i o β†’
    (a β†’ b β†’ c β†’ d β†’ e β†’ q β†’ i β†’ o) β†’ directory prefix.

  Parameter register_dynamic_directory : βˆ€ {a prefix : Set},
    option string β†’ directory prefix β†’ RPC_path.t prefix a β†’
    (a β†’ directory a) β†’ directory prefix.
End RPC_directory_signature.
Require Export TezosOfOCaml.Environment.V7.RPC_directory.
Module RPC_directory_check : RPC_directory_signature := RPC_directory.

Module Type Base58_signature.
  Parameter encoding : βˆ€ (a : Set), Set.

  Parameter simple_decode : βˆ€ {a : Set}, encoding a β†’ string β†’ option a.

  Parameter simple_encode : βˆ€ {a : Set}, encoding a β†’ a β†’ string.

  Definition data := extensible_type.

  Parameter register_encoding : βˆ€ {a : Set},
    string β†’ int β†’ (a β†’ string) β†’ (string β†’ option a) β†’ (a β†’ data) β†’
    encoding a.

  Parameter check_encoded_prefix : βˆ€ {a : Set},
    encoding a β†’ string β†’ int β†’ unit.

  Parameter decode : string β†’ option data.
End Base58_signature.
Require Export TezosOfOCaml.Environment.V7.Base58.
Module Base58_check : Base58_signature := Base58.

Module Type S_signature.
  Module T.
    Record signature {t : Set} : Set := {
      t := t;
      op_eq : t β†’ t β†’ bool;
      op_ltgt : t β†’ t β†’ bool;
      op_lt : t β†’ t β†’ bool;
      op_lteq : t β†’ t β†’ bool;
      op_gteq : t β†’ t β†’ bool;
      op_gt : t β†’ t β†’ bool;
      compare : t β†’ t β†’ int;
      equal : t β†’ t β†’ bool;
      max : t β†’ t β†’ t;
      min : t β†’ t β†’ t;
      pp : Format.formatter β†’ t β†’ unit;
      encoding : Data_encoding.t t;
      to_bytes : t β†’ bytes;
      of_bytes : bytes β†’ option t;
    }.
  End T.
  Definition T := @T.signature.
  Arguments T {_}.

  Module HASHABLE.
    Record signature {t hash : Set} : Set := {
      t := t;
      op_eq : t β†’ t β†’ bool;
      op_ltgt : t β†’ t β†’ bool;
      op_lt : t β†’ t β†’ bool;
      op_lteq : t β†’ t β†’ bool;
      op_gteq : t β†’ t β†’ bool;
      op_gt : t β†’ t β†’ bool;
      compare : t β†’ t β†’ int;
      equal : t β†’ t β†’ bool;
      max : t β†’ t β†’ t;
      min : t β†’ t β†’ t;
      pp : Format.formatter β†’ t β†’ unit;
      encoding : Data_encoding.t t;
      to_bytes : t β†’ bytes;
      of_bytes : bytes β†’ option t;
      hash := hash;
      hash_value : t β†’ hash;
      hash_raw : bytes β†’ hash;
    }.
  End HASHABLE.
  Definition HASHABLE := @HASHABLE.signature.
  Arguments HASHABLE {_ _}.

  Module MINIMAL_HASH.
    Record signature {t : Set} : Set := {
      t := t;
      name : string;
      title : string;
      pp : Format.formatter β†’ t β†’ unit;
      pp_short : Format.formatter β†’ t β†’ unit;
      op_eq : t β†’ t β†’ bool;
      op_ltgt : t β†’ t β†’ bool;
      op_lt : t β†’ t β†’ bool;
      op_lteq : t β†’ t β†’ bool;
      op_gteq : t β†’ t β†’ bool;
      op_gt : t β†’ t β†’ bool;
      compare : t β†’ t β†’ int;
      equal : t β†’ t β†’ bool;
      max : t β†’ t β†’ t;
      min : t β†’ t β†’ t;
      hash_bytes : option bytes β†’ list bytes β†’ t;
      hash_string : option string β†’ list string β†’ t;
      zero : t;
    }.
  End MINIMAL_HASH.
  Definition MINIMAL_HASH := @MINIMAL_HASH.signature.
  Arguments MINIMAL_HASH {_}.

  Module RAW_DATA.
    Record signature {t : Set} : Set := {
      t := t;
      size_value : int;
      to_bytes : t β†’ bytes;
      of_bytes_opt : bytes β†’ option t;
      of_bytes_exn : bytes β†’ t;
    }.
  End RAW_DATA.
  Definition RAW_DATA := @RAW_DATA.signature.
  Arguments RAW_DATA {_}.

  Module B58_DATA.
    Record signature {t : Set} : Set := {
      t := t;
      to_b58check : t β†’ string;
      to_short_b58check : t β†’ string;
      of_b58check_exn : string β†’ t;
      of_b58check_opt : string β†’ option t;
      b58check_encoding : Base58.encoding t;
    }.
  End B58_DATA.
  Definition B58_DATA := @B58_DATA.signature.
  Arguments B58_DATA {_}.

  Module ENCODER.
    Record signature {t : Set} : Set := {
      t := t;
      encoding : Data_encoding.t t;
      rpc_arg : RPC_arg.t t;
    }.
  End ENCODER.
  Definition ENCODER := @ENCODER.signature.
  Arguments ENCODER {_}.

  Module INDEXES_SET.
    Record signature {elt t : Set} : Set := {
      elt := elt;
      t := t;
      empty : t;
      is_empty : t β†’ bool;
      mem : elt β†’ t β†’ bool;
      add : elt β†’ t β†’ t;
      singleton : elt β†’ t;
      remove : elt β†’ t β†’ t;
      union : t β†’ t β†’ t;
      inter : t β†’ t β†’ t;
      disjoint : t β†’ t β†’ bool;
      diff_value : t β†’ t β†’ t;
      compare : t β†’ t β†’ int;
      equal : t β†’ t β†’ bool;
      subset : t β†’ t β†’ bool;
      iter : (elt β†’ unit) β†’ t β†’ unit;
      iter_e :
        βˆ€ {trace : Set},
        (elt β†’ Pervasives.result unit trace) β†’ t β†’
        Pervasives.result unit trace;
      iter_s : (elt β†’ unit) β†’ t β†’ unit;
      iter_p : (elt β†’ unit) β†’ t β†’ unit;
      iter_es :
        βˆ€ {trace : Set},
        (elt β†’ Pervasives.result unit trace) β†’ t β†’
        Pervasives.result unit trace;
      map : (elt β†’ elt) β†’ t β†’ t;
      fold : βˆ€ {a : Set}, (elt β†’ a β†’ a) β†’ t β†’ a β†’ a;
      fold_e :
        βˆ€ {a trace : Set},
        (elt β†’ a β†’ Pervasives.result a trace) β†’ t β†’ a β†’
        Pervasives.result a trace;
      fold_s : βˆ€ {a : Set}, (elt β†’ a β†’ a) β†’ t β†’ a β†’ a;
      fold_es :
        βˆ€ {a trace : Set},
        (elt β†’ a β†’ Pervasives.result a trace) β†’ t β†’ a β†’
        Pervasives.result a trace;
      for_all : (elt β†’ bool) β†’ t β†’ bool;
      _exists : (elt β†’ bool) β†’ t β†’ bool;
      filter : (elt β†’ bool) β†’ t β†’ t;
      filter_map : (elt β†’ option elt) β†’ t β†’ t;
      partition : (elt β†’ bool) β†’ t β†’ t Γ— t;
      cardinal : t β†’ int;
      elements : t β†’ list elt;
      min_elt : t β†’ option elt;
      min_elt_opt : t β†’ option elt;
      max_elt : t β†’ option elt;
      max_elt_opt : t β†’ option elt;
      choose : t β†’ option elt;
      choose_opt : t β†’ option elt;
      split : elt β†’ t β†’ t Γ— bool Γ— t;
      find : elt β†’ t β†’ option elt;
      find_opt : elt β†’ t β†’ option elt;
      find_first : (elt β†’ bool) β†’ t β†’ option elt;
      find_first_opt : (elt β†’ bool) β†’ t β†’ option elt;
      find_last : (elt β†’ bool) β†’ t β†’ option elt;
      find_last_opt : (elt β†’ bool) β†’ t β†’ option elt;
      of_list : list elt β†’ t;
      to_seq_from : elt β†’ t β†’ Seq.t elt;
      to_seq : t β†’ Seq.t elt;
      to_rev_seq : t β†’ Seq.t elt;
      add_seq : Seq.t elt β†’ t β†’ t;
      of_seq : Seq.t elt β†’ t;
      iter_ep : (elt β†’ M? unit) β†’ t β†’ M? unit;
      random_elt : t β†’ elt;
      encoding : Data_encoding.t t;
    }.
  End INDEXES_SET.
  Definition INDEXES_SET := @INDEXES_SET.signature.
  Arguments INDEXES_SET {_ _}.

  Module INDEXES_MAP.
    Record signature {key : Set} {t : Set β†’ Set} : Set := {
      key := key;
      t := t;
      empty : βˆ€ {a : Set}, t a;
      is_empty : βˆ€ {a : Set}, t a β†’ bool;
      mem : βˆ€ {a : Set}, key β†’ t a β†’ bool;
      add : βˆ€ {a : Set}, key β†’ a β†’ t a β†’ t a;
      update : βˆ€ {a : Set}, key β†’ (option a β†’ option a) β†’ t a β†’ t a;
      singleton : βˆ€ {a : Set}, key β†’ a β†’ t a;
      remove : βˆ€ {a : Set}, key β†’ t a β†’ t a;
      merge :
        βˆ€ {a b c : Set},
        (key β†’ option a β†’ option b β†’ option c) β†’ t a β†’ t b β†’ t c;
      union :
        βˆ€ {a : Set}, (key β†’ a β†’ a β†’ option a) β†’ t a β†’ t a β†’ t a;
      compare : βˆ€ {a : Set}, (a β†’ a β†’ int) β†’ t a β†’ t a β†’ int;
      equal : βˆ€ {a : Set}, (a β†’ a β†’ bool) β†’ t a β†’ t a β†’ bool;
      iter : βˆ€ {a : Set}, (key β†’ a β†’ unit) β†’ t a β†’ unit;
      iter_e :
        βˆ€ {a trace : Set},
        (key β†’ a β†’ Pervasives.result unit trace) β†’ t a β†’
        Pervasives.result unit trace;
      iter_s : βˆ€ {a : Set}, (key β†’ a β†’ unit) β†’ t a β†’ unit;
      iter_p : βˆ€ {a : Set}, (key β†’ a β†’ unit) β†’ t a β†’ unit;
      iter_es :
        βˆ€ {a trace : Set},
        (key β†’ a β†’ Pervasives.result unit trace) β†’ t a β†’
        Pervasives.result unit trace;
      fold : βˆ€ {a b : Set}, (key β†’ a β†’ b β†’ b) β†’ t a β†’ b β†’ b;
      fold_e :
        βˆ€ {a b trace : Set},
        (key β†’ a β†’ b β†’ Pervasives.result b trace) β†’ t a β†’ b β†’
        Pervasives.result b trace;
      fold_s : βˆ€ {a b : Set}, (key β†’ a β†’ b β†’ b) β†’ t a β†’ b β†’ b;
      fold_es :
        βˆ€ {a b trace : Set},
        (key β†’ a β†’ b β†’ Pervasives.result b trace) β†’ t a β†’ b β†’
        Pervasives.result b trace;
      for_all : βˆ€ {a : Set}, (key β†’ a β†’ bool) β†’ t a β†’ bool;
      _exists : βˆ€ {a : Set}, (key β†’ a β†’ bool) β†’ t a β†’ bool;
      filter : βˆ€ {a : Set}, (key β†’ a β†’ bool) β†’ t a β†’ t a;
      filter_map : βˆ€ {a b : Set}, (key β†’ a β†’ option b) β†’ t a β†’ t b;
      partition : βˆ€ {a : Set}, (key β†’ a β†’ bool) β†’ t a β†’ t a Γ— t a;
      cardinal : βˆ€ {a : Set}, t a β†’ int;
      bindings : βˆ€ {a : Set}, t a β†’ list (key Γ— a);
      min_binding : βˆ€ {a : Set}, t a β†’ option (key Γ— a);
      min_binding_opt : βˆ€ {a : Set}, t a β†’ option (key Γ— a);
      max_binding : βˆ€ {a : Set}, t a β†’ option (key Γ— a);
      max_binding_opt : βˆ€ {a : Set}, t a β†’ option (key Γ— a);
      choose : βˆ€ {a : Set}, t a β†’ option (key Γ— a);
      choose_opt : βˆ€ {a : Set}, t a β†’ option (key Γ— a);
      split : βˆ€ {a : Set}, key β†’ t a β†’ t a Γ— option a Γ— t a;
      find : βˆ€ {a : Set}, key β†’ t a β†’ option a;
      find_opt : βˆ€ {a : Set}, key β†’ t a β†’ option a;
      find_first : βˆ€ {a : Set}, (key β†’ bool) β†’ t a β†’ option (key Γ— a);
      find_first_opt :
        βˆ€ {a : Set}, (key β†’ bool) β†’ t a β†’ option (key Γ— a);
      find_last : βˆ€ {a : Set}, (key β†’ bool) β†’ t a β†’ option (key Γ— a);
      find_last_opt :
        βˆ€ {a : Set}, (key β†’ bool) β†’ t a β†’ option (key Γ— a);
      map : βˆ€ {a b : Set}, (a β†’ b) β†’ t a β†’ t b;
      mapi : βˆ€ {a b : Set}, (key β†’ a β†’ b) β†’ t a β†’ t b;
      to_seq : βˆ€ {a : Set}, t a β†’ Seq.t (key Γ— a);
      to_rev_seq : βˆ€ {a : Set}, t a β†’ Seq.t (key Γ— a);
      to_seq_from : βˆ€ {a : Set}, key β†’ t a β†’ Seq.t (key Γ— a);
      add_seq : βˆ€ {a : Set}, Seq.t (key Γ— a) β†’ t a β†’ t a;
      of_seq : βˆ€ {a : Set}, Seq.t (key Γ— a) β†’ t a;
      iter_ep :
    βˆ€ {a _error: Set},
    (key β†’ a β†’ Pervasives.result unit (Error_monad.trace _error)) β†’
    t a β†’
    Pervasives.result unit (Error_monad.trace _error);

      encoding : βˆ€ {a : Set}, Data_encoding.t a β†’ Data_encoding.t (t a);
    }.
  End INDEXES_MAP.
  Definition INDEXES_MAP := @INDEXES_MAP.signature.
  Arguments INDEXES_MAP {_ _}.

  Module INDEXES.
    Record signature {t Set_t : Set} {Map_t : Set β†’ Set} : Set := {
      t := t;
      _Set : INDEXES_SET (elt := t) (t := Set_t);
      Map : INDEXES_MAP (key := t) (t := Map_t);
    }.
  End INDEXES.
  Definition INDEXES := @INDEXES.signature.
  Arguments INDEXES {_ _ _}.

  Module HASH.
    Record signature {t Set_t : Set} {Map_t : Set β†’ Set} : Set := {
      t := t;
      name : string;
      title : string;
      pp : Format.formatter β†’ t β†’ unit;
      pp_short : Format.formatter β†’ t β†’ unit;
      op_eq : t β†’ t β†’ bool;
      op_ltgt : t β†’ t β†’ bool;
      op_lt : t β†’ t β†’ bool;
      op_lteq : t β†’ t β†’ bool;
      op_gteq : t β†’ t β†’ bool;
      op_gt : t β†’ t β†’ bool;
      compare : t β†’ t β†’ int;
      equal : t β†’ t β†’ bool;
      max : t β†’ t β†’ t;
      min : t β†’ t β†’ t;
      hash_bytes : option bytes β†’ list bytes β†’ t;
      hash_string : option string β†’ list string β†’ t;
      zero : t;
      size_value : int;
      to_bytes : t β†’ bytes;
      of_bytes_opt : bytes β†’ option t;
      of_bytes_exn : bytes β†’ t;
      to_b58check : t β†’ string;
      to_short_b58check : t β†’ string;
      of_b58check_exn : string β†’ t;
      of_b58check_opt : string β†’ option t;
      (* extensible_type_definition `Base58.data` *)
      b58check_encoding : Base58.encoding t;
      encoding : Data_encoding.t t;
      rpc_arg : RPC_arg.t t;
      _Set : INDEXES_SET (elt := t) (t := Set_t);
      Map : INDEXES_MAP (key := t) (t := Map_t);
    }.
  End HASH.
  Definition HASH := @HASH.signature.
  Arguments HASH {_ _ _}.

  Module MERKLE_TREE.
    Record signature {elt t Set_t : Set} {Map_t : Set β†’ Set} {path : Set} : Set
      := {
      elt := elt;
      t := t;
      name : string;
      title : string;
      pp : Format.formatter β†’ t β†’ unit;
      pp_short : Format.formatter β†’ t β†’ unit;
      op_eq : t β†’ t β†’ bool;
      op_ltgt : t β†’ t β†’ bool;
      op_lt : t β†’ t β†’ bool;
      op_lteq : t β†’ t β†’ bool;
      op_gteq : t β†’ t β†’ bool;
      op_gt : t β†’ t β†’ bool;
      compare : t β†’ t β†’ int;
      equal : t β†’ t β†’ bool;
      max : t β†’ t β†’ t;
      min : t β†’ t β†’ t;
      hash_bytes : option bytes β†’ list bytes β†’ t;
      hash_string : option string β†’ list string β†’ t;
      zero : t;
      size_value : int;
      to_bytes : t β†’ bytes;
      of_bytes_opt : bytes β†’ option t;
      of_bytes_exn : bytes β†’ t;
      to_b58check : t β†’ string;
      to_short_b58check : t β†’ string;
      of_b58check_exn : string β†’ t;
      of_b58check_opt : string β†’ option t;
      (* extensible_type_definition `Base58.data` *)
      b58check_encoding : Base58.encoding t;
      encoding : Data_encoding.t t;
      rpc_arg : RPC_arg.t t;
      _Set : INDEXES_SET (elt := t) (t := Set_t);
      Map : INDEXES_MAP (key := t) (t := Map_t);
      compute : list elt β†’ t;
      empty : t;
      path := path;
      compute_path : list elt β†’ int β†’ path;
      check_path : path β†’ elt β†’ t Γ— int;
      path_encoding : Data_encoding.t path;
    }.
  End MERKLE_TREE.
  Definition MERKLE_TREE := @MERKLE_TREE.signature.
  Arguments MERKLE_TREE {_ _ _ _ _}.

  Module SIGNATURE_PUBLIC_KEY_HASH.
    Record signature {t Set_t : Set} {Map_t : Set β†’ Set} : Set := {
      t := t;
      pp : Format.formatter β†’ t β†’ unit;
      pp_short : Format.formatter β†’ t β†’ unit;
      op_eq : t β†’ t β†’ bool;
      op_ltgt : t β†’ t β†’ bool;
      op_lt : t β†’ t β†’ bool;
      op_lteq : t β†’ t β†’ bool;
      op_gteq : t β†’ t β†’ bool;
      op_gt : t β†’ t β†’ bool;
      compare : t β†’ t β†’ int;
      equal : t β†’ t β†’ bool;
      max : t β†’ t β†’ t;
      min : t β†’ t β†’ t;
      size_value : int;
      to_bytes : t β†’ bytes;
      of_bytes_opt : bytes β†’ option t;
      of_bytes_exn : bytes β†’ t;
      to_b58check : t β†’ string;
      to_short_b58check : t β†’ string;
      of_b58check_exn : string β†’ t;
      of_b58check_opt : string β†’ option t;
      (* extensible_type_definition `Base58.data` *)
      b58check_encoding : Base58.encoding t;
      encoding : Data_encoding.t t;
      rpc_arg : RPC_arg.t t;
      _Set : INDEXES_SET (elt := t) (t := Set_t);
      Map : INDEXES_MAP (key := t) (t := Map_t);
      zero : t;
    }.
  End SIGNATURE_PUBLIC_KEY_HASH.
  Definition SIGNATURE_PUBLIC_KEY_HASH := @SIGNATURE_PUBLIC_KEY_HASH.signature.
  Arguments SIGNATURE_PUBLIC_KEY_HASH {_ _ _}.

  Module SIGNATURE_PUBLIC_KEY.
    Record signature {t public_key_hash_t : Set} : Set := {
      t := t;
      pp : Format.formatter β†’ t β†’ unit;
      op_eq : t β†’ t β†’ bool;
      op_ltgt : t β†’ t β†’ bool;
      op_lt : t β†’ t β†’ bool;
      op_lteq : t β†’ t β†’ bool;
      op_gteq : t β†’ t β†’ bool;
      op_gt : t β†’ t β†’ bool;
      compare : t β†’ t β†’ int;
      equal : t β†’ t β†’ bool;
      max : t β†’ t β†’ t;
      min : t β†’ t β†’ t;
      to_b58check : t β†’ string;
      to_short_b58check : t β†’ string;
      of_b58check_exn : string β†’ t;
      of_b58check_opt : string β†’ option t;
      (* extensible_type_definition `Base58.data` *)
      b58check_encoding : Base58.encoding t;
      encoding : Data_encoding.t t;
      rpc_arg : RPC_arg.t t;
      public_key_hash_t := public_key_hash_t;
      hash_value : t β†’ public_key_hash_t;
      size_value : t β†’ int;
      of_bytes_without_validation : bytes β†’ option t;
    }.
  End SIGNATURE_PUBLIC_KEY.
  Definition SIGNATURE_PUBLIC_KEY := @SIGNATURE_PUBLIC_KEY.signature.
  Arguments SIGNATURE_PUBLIC_KEY {_ _}.

  Module SIGNATURE.
    Record signature {Public_key_hash_t Public_key_hash_Set_t : Set}
      {Public_key_hash_Map_t : Set β†’ Set} {Public_key_t t watermark : Set}
      : Set := {
      Public_key_hash :
        SIGNATURE_PUBLIC_KEY_HASH (t := Public_key_hash_t)
          (Set_t := Public_key_hash_Set_t) (Map_t := Public_key_hash_Map_t);
      Public_key :
        SIGNATURE_PUBLIC_KEY (t := Public_key_t)
          (public_key_hash_t := Public_key_hash.(SIGNATURE_PUBLIC_KEY_HASH.t));
      t := t;
      pp : Format.formatter β†’ t β†’ unit;
      size_value : int;
      to_bytes : t β†’ bytes;
      of_bytes_opt : bytes β†’ option t;
      of_bytes_exn : bytes β†’ t;
      op_eq : t β†’ t β†’ bool;
      op_ltgt : t β†’ t β†’ bool;
      op_lt : t β†’ t β†’ bool;
      op_lteq : t β†’ t β†’ bool;
      op_gteq : t β†’ t β†’ bool;
      op_gt : t β†’ t β†’ bool;
      compare : t β†’ t β†’ int;
      equal : t β†’ t β†’ bool;
      max : t β†’ t β†’ t;
      min : t β†’ t β†’ t;
      to_b58check : t β†’ string;
      to_short_b58check : t β†’ string;
      of_b58check_exn : string β†’ t;
      of_b58check_opt : string β†’ option t;
      (* extensible_type_definition `Base58.data` *)
      b58check_encoding : Base58.encoding t;
      encoding : Data_encoding.t t;
      rpc_arg : RPC_arg.t t;
      zero : t;
      watermark := watermark;
      
Check a signature
      check :
        option watermark β†’ Public_key.(SIGNATURE_PUBLIC_KEY.t) β†’ t β†’ bytes β†’
        bool;
    }.
  End SIGNATURE.
  Definition SIGNATURE := @SIGNATURE.signature.
  Arguments SIGNATURE {_ _ _ _ _ _}.

  Module AGGREGATE_SIGNATURE.
    Record signature {Public_key_hash_t Public_key_hash_Set_t : Set}
      {Public_key_hash_Map_t : Set β†’ Set} {Public_key_t t watermark : Set}
      : Set := {
      Public_key_hash :
        SIGNATURE_PUBLIC_KEY_HASH (t := Public_key_hash_t)
          (Set_t := Public_key_hash_Set_t) (Map_t := Public_key_hash_Map_t);
      Public_key :
        SIGNATURE_PUBLIC_KEY (t := Public_key_t)
          (public_key_hash_t := Public_key_hash.(SIGNATURE_PUBLIC_KEY_HASH.t));
      t := t;
      pp : Format.formatter β†’ t β†’ unit;
      size_value : int;
      to_bytes : t β†’ bytes;
      of_bytes_opt : bytes β†’ option t;
      of_bytes_exn : bytes β†’ t;
      op_eq : t β†’ t β†’ bool;
      op_ltgt : t β†’ t β†’ bool;
      op_lt : t β†’ t β†’ bool;
      op_lteq : t β†’ t β†’ bool;
      op_gteq : t β†’ t β†’ bool;
      op_gt : t β†’ t β†’ bool;
      compare : t β†’ t β†’ int;
      equal : t β†’ t β†’ bool;
      max : t β†’ t β†’ t;
      min : t β†’ t β†’ t;
      to_b58check : t β†’ string;
      to_short_b58check : t β†’ string;
      of_b58check_exn : string β†’ t;
      of_b58check_opt : string β†’ option t;
      (* extensible_type_definition `Base58.data` *)
      b58check_encoding : Base58.encoding t;
      encoding : Data_encoding.t t;
      rpc_arg : RPC_arg.t t;
      zero : t;
      watermark := watermark;
      check :
        option watermark β†’ Public_key.(SIGNATURE_PUBLIC_KEY.t) β†’ t β†’ bytes β†’
        bool;
      aggregate_check :
        list (Public_key.(SIGNATURE_PUBLIC_KEY.t) Γ— option watermark Γ— bytes) β†’
        t β†’ bool;
      aggregate_signature_opt : list t β†’ option t;
    }.
  End AGGREGATE_SIGNATURE.
  Definition AGGREGATE_SIGNATURE := @AGGREGATE_SIGNATURE.signature.
  Arguments AGGREGATE_SIGNATURE {_ _ _ _ _ _}.

  Module FIELD.
    Record signature {t : Set} : Set := {
      t := t;
      
The order of the finite field
      order : Z.t;
      
Minimal number of bytes required to encode a value of the field.
      size_in_bytes : int;
      
[check_bytes bs] returns [true] if [bs] is a correct byte representation of a field element
      check_bytes : Bytes.t β†’ bool;
      
The neutral element for the addition
      zero : t;
      
The neutral element for the multiplication
      one : t;
      
[add a b] returns [a + b mod order]
      add : t β†’ t β†’ t;
      
[mul a b] returns [a * b mod order]
      mul : t β†’ t β†’ t;
      
[eq a b] returns [true] if [a = b mod order], else [false]
      eq_value : t β†’ t β†’ bool;
      
[negate x] returns [-x mod order]. Equivalently, [negate x] returns the unique [y] such that [x + y mod order = 0]
      negate : t β†’ t;
      
[inverse_opt x] returns [x^-1] if [x] is not [0] as an option, else [None]
      inverse_opt : t β†’ option t;
      
[pow x n] returns [x^n]
      pow : t β†’ Z.t β†’ t;
      
From a predefined bytes representation, construct a value t. It is not required that to_bytes [(Option.get (of_bytes_opt t)) = t]. By default, little endian encoding is used and the given element is modulo the prime order
      of_bytes_opt : Bytes.t β†’ option t;
      
Convert the value t to a bytes representation which can be used for hashing for instance. It is not required that [to_bytes (Option.get (of_bytes_opt t)) = t]. By default, little endian encoding is used, and length of the resulting bytes may vary depending on the order.
      to_bytes : t β†’ Bytes.t;
    }.
  End FIELD.
  Definition FIELD := @FIELD.signature.
  Arguments FIELD {_}.

  Module PRIME_FIELD.
    Record signature {t : Set} : Set := {
      t := t;
      order : Z.t;
      size_in_bytes : int;
      check_bytes : Bytes.t β†’ bool;
      zero : t;
      one : t;
      add : t β†’ t β†’ t;
      mul : t β†’ t β†’ t;
      eq_value : t β†’ t β†’ bool;
      negate : t β†’ t;
      inverse_opt : t β†’ option t;
      pow : t β†’ Z.t β†’ t;
      of_bytes_opt : Bytes.t β†’ option t;
      to_bytes : t β†’ Bytes.t;
      
Actual number of bytes allocated for a value of type t
      size_in_memory : int;
      
[of_z x] builds an element t from the Zarith element [x]. [mod order] is applied if [x >= order] or [x < 0].
      of_z : Z.t β†’ t;
      
[to_z x] builds a Zarith element, using the decimal representation. Arithmetic on the result can be done using the modular functions on integers
      to_z : t β†’ Z.t;
    }.
  End PRIME_FIELD.
  Definition PRIME_FIELD := @PRIME_FIELD.signature.
  Arguments PRIME_FIELD {_}.

  Module CURVE.
    Record signature {t Scalar_t : Set} : Set := {
      
The type of the element in the elliptic curve
      t := t;
      
Actual number of bytes allocated for a value of type t
      size_in_memory : int;
      
The size of a point representation, in bytes
      size_in_bytes : int;
      Scalar : FIELD (t := Scalar_t);
      
Check if a point, represented as a byte array, is on the curve *
      check_bytes : Bytes.t β†’ bool;
      
Attempt to construct a point from a byte array
      of_bytes_opt : Bytes.t β†’ option t;
      
Return a representation in bytes
      to_bytes : t β†’ Bytes.t;
      
Zero of the elliptic curve
      zero : t;
      
A fixed generator of the elliptic curve
      one : t;
      
Return the addition of two element
      add : t β†’ t β†’ t;
      
Double the element
      double : t β†’ t;
      
Return the opposite of the element
      negate : t β†’ t;
      
Return [true] if the two elements are algebraically the same
      eq_value : t β†’ t β†’ bool;
      
Multiply an element by a scalar
      mul : t β†’ Scalar.(FIELD.t) β†’ t;
    }.
  End CURVE.
  Definition CURVE := @CURVE.signature.
  Arguments CURVE {_ _}.
End S_signature.
Require Export TezosOfOCaml.Environment.V7.S.
Module S_check : S_signature := S.

Module Type Blake2B_signature.
  Module Name.
    Record signature : Set := {
      name : string;
      title : string;
      size_value : option int;
    }.
  End Name.
  Definition Name := Name.signature.

  Module PrefixedName.
    Record signature : Set := {
      name : string;
      title : string;
      size_value : option int;
      b58check_prefix : string;
    }.
  End PrefixedName.
  Definition PrefixedName := PrefixedName.signature.

  Parameter Make_minimal_t : βˆ€ (Name : Name), Set.

  Parameter Make_minimal :
    βˆ€ (Name : Name), S.MINIMAL_HASH (t := Make_minimal_t Name).

  Module Register.
    Record signature : Set := {
      register_encoding :
        βˆ€ {a : Set},
        string β†’ int β†’ (a β†’ string) β†’ (string β†’ option a) β†’
        (a β†’ Base58.data) β†’ Base58.encoding a;
    }.
  End Register.
  Definition Register := Register.signature.

  Parameter Make_t : βˆ€ (Register : Register) (Name : PrefixedName), Set.

  Parameter Make_Set_t :
    βˆ€ (Register : Register) (Name : PrefixedName), Set.

  Parameter Make_Map_t :
    βˆ€ (Register : Register) (Name : PrefixedName), Set β†’ Set.

  Parameter Make :
    βˆ€ (Register : Register),
    βˆ€ (Name : PrefixedName),
    S.HASH (t := Make_t Register Name) (Set_t := Make_Set_t Register Name)
      (Map_t := Make_Map_t Register Name).
End Blake2B_signature.
Require Export TezosOfOCaml.Environment.V7.Blake2B.
Module Blake2B_check : Blake2B_signature := Blake2B.

Module Type Bls_signature.
  Parameter Included_AGGREGATE_SIGNATURE_Public_key_hash_t : Set.

  Parameter Included_AGGREGATE_SIGNATURE_Public_key_hash_Set_t : Set.

  Parameter Included_AGGREGATE_SIGNATURE_Public_key_hash_Map_t : Set β†’ Set.

  Parameter Included_AGGREGATE_SIGNATURE_Public_key_t : Set.

  Parameter Included_AGGREGATE_SIGNATURE_t : Set.

  Parameter Included_AGGREGATE_SIGNATURE :
    S.AGGREGATE_SIGNATURE
      (Public_key_hash_t := Included_AGGREGATE_SIGNATURE_Public_key_hash_t)
      (Public_key_hash_Set_t :=
        Included_AGGREGATE_SIGNATURE_Public_key_hash_Set_t)
      (Public_key_hash_Map_t :=
        Included_AGGREGATE_SIGNATURE_Public_key_hash_Map_t)
      (Public_key_t := Included_AGGREGATE_SIGNATURE_Public_key_t)
      (t := Included_AGGREGATE_SIGNATURE_t) (watermark := bytes).

  Definition Public_key_hash :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.Public_key_hash).

  Definition Public_key :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.Public_key).

  Definition t := Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.t).

  Definition pp : Format.formatter β†’ t β†’ unit :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.pp).

  Definition size_value : int :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.size_value).

  Definition to_bytes : t β†’ bytes :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.to_bytes).

  Definition of_bytes_opt : bytes β†’ option t :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.of_bytes_opt).

  Definition of_bytes_exn : bytes β†’ t :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.of_bytes_exn).

  Definition op_eq : t β†’ t β†’ bool :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.op_eq).

  Definition op_ltgt : t β†’ t β†’ bool :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.op_ltgt).

  Definition op_lt : t β†’ t β†’ bool :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.op_lt).

  Definition op_lteq : t β†’ t β†’ bool :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.op_lteq).

  Definition op_gteq : t β†’ t β†’ bool :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.op_gteq).

  Definition op_gt : t β†’ t β†’ bool :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.op_gt).

  Definition compare : t β†’ t β†’ int :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.compare).

  Definition equal : t β†’ t β†’ bool :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.equal).

  Definition max : t β†’ t β†’ t :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.max).

  Definition min : t β†’ t β†’ t :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.min).

  Definition to_b58check : t β†’ string :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.to_b58check).

  Definition to_short_b58check : t β†’ string :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.to_short_b58check).

  Definition of_b58check_exn : string β†’ t :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.of_b58check_exn).

  Definition of_b58check_opt : string β†’ option t :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.of_b58check_opt).

  Definition b58check_encoding : Base58.encoding t :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.b58check_encoding).

  Definition encoding : Data_encoding.t t :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.encoding).

  Definition rpc_arg : RPC_arg.t t :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.rpc_arg).

  Definition zero : t :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.zero).

  Definition check :
    option bytes β†’ Public_key.(S.SIGNATURE_PUBLIC_KEY.t) β†’ t β†’ bytes β†’ bool
    := Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.check).

  Definition aggregate_check :
    list (Public_key.(S.SIGNATURE_PUBLIC_KEY.t) Γ— option bytes Γ— bytes) β†’ t β†’
    bool :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.aggregate_check).

  Definition aggregate_signature_opt : list t β†’ option t :=
    Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.aggregate_signature_opt).

  Module Primitive.
    Parameter Fr_t : Set.

    Parameter Fr : S.PRIME_FIELD (t := Fr_t).

    Parameter G1_t : Set.

    Parameter G1 : S.CURVE (t := G1_t) (Scalar_t := Fr.(S.PRIME_FIELD.t)).

    Parameter G2_t : Set.

    Parameter G2 : S.CURVE (t := G2_t) (Scalar_t := Fr.(S.PRIME_FIELD.t)).

    Parameter pairing_check : list (G1.(S.CURVE.t) Γ— G2.(S.CURVE.t)) β†’ bool.
  End Primitive.
End Bls_signature.
Require Export TezosOfOCaml.Environment.V7.Bls.
Module Bls_check : Bls_signature := Bls.

Module Type Ed25519_signature.
  Parameter Included_SIGNATURE_Public_key_hash_t : Set.

  Parameter Included_SIGNATURE_Public_key_hash_Set_t : Set.

  Parameter Included_SIGNATURE_Public_key_hash_Map_t : Set β†’ Set.

  Parameter Included_SIGNATURE_Public_key_t : Set.

  Parameter Included_SIGNATURE_t : Set.

  Parameter Included_SIGNATURE :
    S.SIGNATURE (Public_key_hash_t := Included_SIGNATURE_Public_key_hash_t)
      (Public_key_hash_Set_t := Included_SIGNATURE_Public_key_hash_Set_t)
      (Public_key_hash_Map_t := Included_SIGNATURE_Public_key_hash_Map_t)
      (Public_key_t := Included_SIGNATURE_Public_key_t)
      (t := Included_SIGNATURE_t) (watermark := bytes).

  Definition Public_key_hash :=
    Included_SIGNATURE.(S.SIGNATURE.Public_key_hash).

  Definition Public_key := Included_SIGNATURE.(S.SIGNATURE.Public_key).

  Definition t := Included_SIGNATURE.(S.SIGNATURE.t).

  Definition pp : Format.formatter β†’ t β†’ unit :=
    Included_SIGNATURE.(S.SIGNATURE.pp).

  Definition size_value : int := Included_SIGNATURE.(S.SIGNATURE.size_value).

  Definition to_bytes : t β†’ bytes := Included_SIGNATURE.(S.SIGNATURE.to_bytes).

  Definition of_bytes_opt : bytes β†’ option t :=
    Included_SIGNATURE.(S.SIGNATURE.of_bytes_opt).

  Definition of_bytes_exn : bytes β†’ t :=
    Included_SIGNATURE.(S.SIGNATURE.of_bytes_exn).

  Definition op_eq : t β†’ t β†’ bool := Included_SIGNATURE.(S.SIGNATURE.op_eq).

  Definition op_ltgt : t β†’ t β†’ bool :=
    Included_SIGNATURE.(S.SIGNATURE.op_ltgt).

  Definition op_lt : t β†’ t β†’ bool := Included_SIGNATURE.(S.SIGNATURE.op_lt).

  Definition op_lteq : t β†’ t β†’ bool :=
    Included_SIGNATURE.(S.SIGNATURE.op_lteq).

  Definition op_gteq : t β†’ t β†’ bool :=
    Included_SIGNATURE.(S.SIGNATURE.op_gteq).

  Definition op_gt : t β†’ t β†’ bool := Included_SIGNATURE.(S.SIGNATURE.op_gt).

  Definition compare : t β†’ t β†’ int :=
    Included_SIGNATURE.(S.SIGNATURE.compare).

  Definition equal : t β†’ t β†’ bool := Included_SIGNATURE.(S.SIGNATURE.equal).

  Definition max : t β†’ t β†’ t := Included_SIGNATURE.(S.SIGNATURE.max).

  Definition min : t β†’ t β†’ t := Included_SIGNATURE.(S.SIGNATURE.min).

  Definition to_b58check : t β†’ string :=
    Included_SIGNATURE.(S.SIGNATURE.to_b58check).

  Definition to_short_b58check : t β†’ string :=
    Included_SIGNATURE.(S.SIGNATURE.to_short_b58check).

  Definition of_b58check_exn : string β†’ t :=
    Included_SIGNATURE.(S.SIGNATURE.of_b58check_exn).

  Definition of_b58check_opt : string β†’ option t :=
    Included_SIGNATURE.(S.SIGNATURE.of_b58check_opt).

  Definition b58check_encoding : Base58.encoding t :=
    Included_SIGNATURE.(S.SIGNATURE.b58check_encoding).

  Definition encoding : Data_encoding.t t :=
    Included_SIGNATURE.(S.SIGNATURE.encoding).

  Definition rpc_arg : RPC_arg.t t := Included_SIGNATURE.(S.SIGNATURE.rpc_arg).

  Definition zero : t := Included_SIGNATURE.(S.SIGNATURE.zero).

  Definition check :
    option bytes β†’ Public_key.(S.SIGNATURE_PUBLIC_KEY.t) β†’ t β†’ bytes β†’ bool
    := Included_SIGNATURE.(S.SIGNATURE.check).
End Ed25519_signature.
Require Export TezosOfOCaml.Environment.V7.Ed25519.
Module Ed25519_check : Ed25519_signature := Ed25519.

Module Type Secp256k1_signature.
  Parameter Included_SIGNATURE_Public_key_hash_t : Set.

  Parameter Included_SIGNATURE_Public_key_hash_Set_t : Set.

  Parameter Included_SIGNATURE_Public_key_hash_Map_t : Set β†’ Set.

  Parameter Included_SIGNATURE_Public_key_t : Set.

  Parameter Included_SIGNATURE_t : Set.

  Parameter Included_SIGNATURE :
    S.SIGNATURE (Public_key_hash_t := Included_SIGNATURE_Public_key_hash_t)
      (Public_key_hash_Set_t := Included_SIGNATURE_Public_key_hash_Set_t)
      (Public_key_hash_Map_t := Included_SIGNATURE_Public_key_hash_Map_t)
      (Public_key_t := Included_SIGNATURE_Public_key_t)
      (t := Included_SIGNATURE_t) (watermark := bytes).

  Definition Public_key_hash :=
    Included_SIGNATURE.(S.SIGNATURE.Public_key_hash).

  Definition Public_key := Included_SIGNATURE.(S.SIGNATURE.Public_key).

  Definition t := Included_SIGNATURE.(S.SIGNATURE.t).

  Definition pp : Format.formatter β†’ t β†’ unit :=
    Included_SIGNATURE.(S.SIGNATURE.pp).

  Definition size_value : int := Included_SIGNATURE.(S.SIGNATURE.size_value).

  Definition to_bytes : t β†’ bytes := Included_SIGNATURE.(S.SIGNATURE.to_bytes).

  Definition of_bytes_opt : bytes β†’ option t :=
    Included_SIGNATURE.(S.SIGNATURE.of_bytes_opt).

  Definition of_bytes_exn : bytes β†’ t :=
    Included_SIGNATURE.(S.SIGNATURE.of_bytes_exn).

  Definition op_eq : t β†’ t β†’ bool := Included_SIGNATURE.(S.SIGNATURE.op_eq).

  Definition op_ltgt : t β†’ t β†’ bool :=
    Included_SIGNATURE.(S.SIGNATURE.op_ltgt).

  Definition op_lt : t β†’ t β†’ bool := Included_SIGNATURE.(S.SIGNATURE.op_lt).

  Definition op_lteq : t β†’ t β†’ bool :=
    Included_SIGNATURE.(S.SIGNATURE.op_lteq).

  Definition op_gteq : t β†’ t β†’ bool :=
    Included_SIGNATURE.(S.SIGNATURE.op_gteq).

  Definition op_gt : t β†’ t β†’ bool := Included_SIGNATURE.(S.SIGNATURE.op_gt).

  Definition compare : t β†’ t β†’ int :=
    Included_SIGNATURE.(S.SIGNATURE.compare).

  Definition equal : t β†’ t β†’ bool := Included_SIGNATURE.(S.SIGNATURE.equal).

  Definition max : t β†’ t β†’ t := Included_SIGNATURE.(S.SIGNATURE.max).

  Definition min : t β†’ t β†’ t := Included_SIGNATURE.(S.SIGNATURE.min).

  Definition to_b58check : t β†’ string :=
    Included_SIGNATURE.(S.SIGNATURE.to_b58check).

  Definition to_short_b58check : t β†’ string :=
    Included_SIGNATURE.(S.SIGNATURE.to_short_b58check).

  Definition of_b58check_exn : string β†’ t :=
    Included_SIGNATURE.(S.SIGNATURE.of_b58check_exn).

  Definition of_b58check_opt : string β†’ option t :=
    Included_SIGNATURE.(S.SIGNATURE.of_b58check_opt).

  Definition b58check_encoding : Base58.encoding t :=
    Included_SIGNATURE.(S.SIGNATURE.b58check_encoding).

  Definition encoding : Data_encoding.t t :=
    Included_SIGNATURE.(S.SIGNATURE.encoding).

  Definition rpc_arg : RPC_arg.t t := Included_SIGNATURE.(S.SIGNATURE.rpc_arg).

  Definition zero : t := Included_SIGNATURE.(S.SIGNATURE.zero).

  Definition check :
    option bytes β†’ Public_key.(S.SIGNATURE_PUBLIC_KEY.t) β†’ t β†’ bytes β†’ bool
    := Included_SIGNATURE.(S.SIGNATURE.check).
End Secp256k1_signature.
Require Export TezosOfOCaml.Environment.V7.Secp256k1.
Module Secp256k1_check : Secp256k1_signature := Secp256k1.

Module Type P256_signature.
  Parameter Included_SIGNATURE_Public_key_hash_t : Set.

  Parameter Included_SIGNATURE_Public_key_hash_Set_t : Set.

  Parameter Included_SIGNATURE_Public_key_hash_Map_t : Set β†’ Set.

  Parameter Included_SIGNATURE_Public_key_t : Set.

  Parameter Included_SIGNATURE_t : Set.

  Parameter Included_SIGNATURE :
    S.SIGNATURE (Public_key_hash_t := Included_SIGNATURE_Public_key_hash_t)
      (Public_key_hash_Set_t := Included_SIGNATURE_Public_key_hash_Set_t)
      (Public_key_hash_Map_t := Included_SIGNATURE_Public_key_hash_Map_t)
      (Public_key_t := Included_SIGNATURE_Public_key_t)
      (t := Included_SIGNATURE_t) (watermark := bytes).

  Definition Public_key_hash :=
    Included_SIGNATURE.(S.SIGNATURE.Public_key_hash).

  Definition Public_key := Included_SIGNATURE.(S.SIGNATURE.Public_key).

  Definition t := Included_SIGNATURE.(S.SIGNATURE.t).

  Definition pp : Format.formatter β†’ t β†’ unit :=
    Included_SIGNATURE.(S.SIGNATURE.pp).

  Definition size_value : int := Included_SIGNATURE.(S.SIGNATURE.size_value).

  Definition to_bytes : t β†’ bytes := Included_SIGNATURE.(S.SIGNATURE.to_bytes).

  Definition of_bytes_opt : bytes β†’ option t :=
    Included_SIGNATURE.(S.SIGNATURE.of_bytes_opt).

  Definition of_bytes_exn : bytes β†’ t :=
    Included_SIGNATURE.(S.SIGNATURE.of_bytes_exn).

  Definition op_eq : t β†’ t β†’ bool := Included_SIGNATURE.(S.SIGNATURE.op_eq).

  Definition op_ltgt : t β†’ t β†’ bool :=
    Included_SIGNATURE.(S.SIGNATURE.op_ltgt).

  Definition op_lt : t β†’ t β†’ bool := Included_SIGNATURE.(S.SIGNATURE.op_lt).

  Definition op_lteq : t β†’ t β†’ bool :=
    Included_SIGNATURE.(S.SIGNATURE.op_lteq).

  Definition op_gteq : t β†’ t β†’ bool :=
    Included_SIGNATURE.(S.SIGNATURE.op_gteq).

  Definition op_gt : t β†’ t β†’ bool := Included_SIGNATURE.(S.SIGNATURE.op_gt).

  Definition compare : t β†’ t β†’ int :=
    Included_SIGNATURE.(S.SIGNATURE.compare).

  Definition equal : t β†’ t β†’ bool := Included_SIGNATURE.(S.SIGNATURE.equal).

  Definition max : t β†’ t β†’ t := Included_SIGNATURE.(S.SIGNATURE.max).

  Definition min : t β†’ t β†’ t := Included_SIGNATURE.(S.SIGNATURE.min).

  Definition to_b58check : t β†’ string :=
    Included_SIGNATURE.(S.SIGNATURE.to_b58check).

  Definition to_short_b58check : t β†’ string :=
    Included_SIGNATURE.(S.SIGNATURE.to_short_b58check).

  Definition of_b58check_exn : string β†’ t :=
    Included_SIGNATURE.(S.SIGNATURE.of_b58check_exn).

  Definition of_b58check_opt : string β†’ option t :=
    Included_SIGNATURE.(S.SIGNATURE.of_b58check_opt).

  Definition b58check_encoding : Base58.encoding t :=
    Included_SIGNATURE.(S.SIGNATURE.b58check_encoding).

  Definition encoding : Data_encoding.t t :=
    Included_SIGNATURE.(S.SIGNATURE.encoding).

  Definition rpc_arg : RPC_arg.t t := Included_SIGNATURE.(S.SIGNATURE.rpc_arg).

  Definition zero : t := Included_SIGNATURE.(S.SIGNATURE.zero).

  Definition check :
    option bytes β†’ Public_key.(S.SIGNATURE_PUBLIC_KEY.t) β†’ t β†’ bytes β†’ bool
    := Included_SIGNATURE.(S.SIGNATURE.check).
End P256_signature.
Require Export TezosOfOCaml.Environment.V7.P256.
Module P256_check : P256_signature := P256.

Module Type Chain_id_signature.
  Parameter Included_HASH_t : Set.

  Parameter Included_HASH_Set_t : Set.

  Parameter Included_HASH_Map_t : Set β†’ Set.

  Parameter Included_HASH :
    S.HASH (t := Included_HASH_t) (Set_t := Included_HASH_Set_t)
      (Map_t := Included_HASH_Map_t).

  Definition t := Included_HASH.(S.HASH.t).

  Definition name : string := Included_HASH.(S.HASH.name).

  Definition title : string := Included_HASH.(S.HASH.title).

  Definition pp : Format.formatter β†’ t β†’ unit := Included_HASH.(S.HASH.pp).

  Definition pp_short : Format.formatter β†’ t β†’ unit :=
    Included_HASH.(S.HASH.pp_short).

  Definition op_eq : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_eq).

  Definition op_ltgt : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_ltgt).

  Definition op_lt : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_lt).

  Definition op_lteq : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_lteq).

  Definition op_gteq : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_gteq).

  Definition op_gt : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_gt).

  Definition compare : t β†’ t β†’ int := Included_HASH.(S.HASH.compare).

  Definition equal : t β†’ t β†’ bool := Included_HASH.(S.HASH.equal).

  Definition max : t β†’ t β†’ t := Included_HASH.(S.HASH.max).

  Definition min : t β†’ t β†’ t := Included_HASH.(S.HASH.min).

  Definition hash_bytes : option bytes β†’ list bytes β†’ t :=
    Included_HASH.(S.HASH.hash_bytes).

  Definition hash_string : option string β†’ list string β†’ t :=
    Included_HASH.(S.HASH.hash_string).

  Definition zero : t := Included_HASH.(S.HASH.zero).

  Definition size_value : int := Included_HASH.(S.HASH.size_value).

  Definition to_bytes : t β†’ bytes := Included_HASH.(S.HASH.to_bytes).

  Definition of_bytes_opt : bytes β†’ option t :=
    Included_HASH.(S.HASH.of_bytes_opt).

  Definition of_bytes_exn : bytes β†’ t := Included_HASH.(S.HASH.of_bytes_exn).

  Definition to_b58check : t β†’ string := Included_HASH.(S.HASH.to_b58check).

  Definition to_short_b58check : t β†’ string :=
    Included_HASH.(S.HASH.to_short_b58check).

  Definition of_b58check_exn : string β†’ t :=
    Included_HASH.(S.HASH.of_b58check_exn).

  Definition of_b58check_opt : string β†’ option t :=
    Included_HASH.(S.HASH.of_b58check_opt).

  Definition b58check_encoding : Base58.encoding t :=
    Included_HASH.(S.HASH.b58check_encoding).

  Definition encoding : Data_encoding.t t := Included_HASH.(S.HASH.encoding).

  Definition rpc_arg : RPC_arg.t t := Included_HASH.(S.HASH.rpc_arg).

  Definition _Set := Included_HASH.(S.HASH._Set).

  Definition Map := Included_HASH.(S.HASH.Map).
End Chain_id_signature.
Require Export TezosOfOCaml.Environment.V7.Chain_id.
Module Chain_id_check : Chain_id_signature := Chain_id.

Module Type Signature_signature.
  Inductive public_key_hash : Set :=
  | Ed25519Hash :
    Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) β†’ public_key_hash
  | Secp256k1Hash :
    Secp256k1.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) β†’ public_key_hash
  | P256Hash :
    P256.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) β†’ public_key_hash.

  Inductive public_key : Set :=
  | Ed25519 : Ed25519.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) β†’ public_key
  | Secp256k1 : Secp256k1.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) β†’ public_key
  | P256 : P256.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) β†’ public_key.

  Inductive watermark : Set :=
  | Block_header : Chain_id.t β†’ watermark
  | Endorsement : Chain_id.t β†’ watermark
  | Generic_operation : watermark
  | Custom : bytes β†’ watermark.

  Parameter Included_SIGNATURE_Public_key_hash_Set_t : Set.

  Parameter Included_SIGNATURE_Public_key_hash_Map_t : Set β†’ Set.

  Parameter Included_SIGNATURE_t : Set.

  Parameter Included_SIGNATURE :
    S.SIGNATURE (Public_key_hash_t := public_key_hash)
      (Public_key_hash_Set_t := Included_SIGNATURE_Public_key_hash_Set_t)
      (Public_key_hash_Map_t := Included_SIGNATURE_Public_key_hash_Map_t)
      (Public_key_t := public_key) (t := Included_SIGNATURE_t)
      (watermark := watermark).

  Definition Public_key_hash :=
    Included_SIGNATURE.(S.SIGNATURE.Public_key_hash).

  Definition Public_key := Included_SIGNATURE.(S.SIGNATURE.Public_key).

  Definition t := Included_SIGNATURE.(S.SIGNATURE.t).

  Definition pp : Format.formatter β†’ t β†’ unit :=
    Included_SIGNATURE.(S.SIGNATURE.pp).

  Definition size_value : int := Included_SIGNATURE.(S.SIGNATURE.size_value).

  Definition to_bytes : t β†’ bytes := Included_SIGNATURE.(S.SIGNATURE.to_bytes).

  Definition of_bytes_opt : bytes β†’ option t :=
    Included_SIGNATURE.(S.SIGNATURE.of_bytes_opt).

  Definition of_bytes_exn : bytes β†’ t :=
    Included_SIGNATURE.(S.SIGNATURE.of_bytes_exn).

  Definition op_eq : t β†’ t β†’ bool := Included_SIGNATURE.(S.SIGNATURE.op_eq).

  Definition op_ltgt : t β†’ t β†’ bool :=
    Included_SIGNATURE.(S.SIGNATURE.op_ltgt).

  Definition op_lt : t β†’ t β†’ bool := Included_SIGNATURE.(S.SIGNATURE.op_lt).

  Definition op_lteq : t β†’ t β†’ bool :=
    Included_SIGNATURE.(S.SIGNATURE.op_lteq).

  Definition op_gteq : t β†’ t β†’ bool :=
    Included_SIGNATURE.(S.SIGNATURE.op_gteq).

  Definition op_gt : t β†’ t β†’ bool := Included_SIGNATURE.(S.SIGNATURE.op_gt).

  Definition compare : t β†’ t β†’ int :=
    Included_SIGNATURE.(S.SIGNATURE.compare).

  Definition equal : t β†’ t β†’ bool := Included_SIGNATURE.(S.SIGNATURE.equal).

  Definition max : t β†’ t β†’ t := Included_SIGNATURE.(S.SIGNATURE.max).

  Definition min : t β†’ t β†’ t := Included_SIGNATURE.(S.SIGNATURE.min).

  Definition to_b58check : t β†’ string :=
    Included_SIGNATURE.(S.SIGNATURE.to_b58check).

  Definition to_short_b58check : t β†’ string :=
    Included_SIGNATURE.(S.SIGNATURE.to_short_b58check).

  Definition of_b58check_exn : string β†’ t :=
    Included_SIGNATURE.(S.SIGNATURE.of_b58check_exn).

  Definition of_b58check_opt : string β†’ option t :=
    Included_SIGNATURE.(S.SIGNATURE.of_b58check_opt).

  Definition b58check_encoding : Base58.encoding t :=
    Included_SIGNATURE.(S.SIGNATURE.b58check_encoding).

  Definition encoding : Data_encoding.t t :=
    Included_SIGNATURE.(S.SIGNATURE.encoding).

  Definition rpc_arg : RPC_arg.t t := Included_SIGNATURE.(S.SIGNATURE.rpc_arg).

  Definition zero : t := Included_SIGNATURE.(S.SIGNATURE.zero).

  Definition check : option watermark β†’ public_key β†’ t β†’ bytes β†’ bool :=
    Included_SIGNATURE.(S.SIGNATURE.check).
End Signature_signature.
Require Export TezosOfOCaml.Environment.V7.Signature.
Module Signature_check : Signature_signature := Signature.

Module Type Block_hash_signature.
  Parameter Included_HASH_t : Set.

  Parameter Included_HASH_Set_t : Set.

  Parameter Included_HASH_Map_t : Set β†’ Set.

  Parameter Included_HASH :
    S.HASH (t := Included_HASH_t) (Set_t := Included_HASH_Set_t)
      (Map_t := Included_HASH_Map_t).

  Definition t := Included_HASH.(S.HASH.t).

  Definition name : string := Included_HASH.(S.HASH.name).

  Definition title : string := Included_HASH.(S.HASH.title).

  Definition pp : Format.formatter β†’ t β†’ unit := Included_HASH.(S.HASH.pp).

  Definition pp_short : Format.formatter β†’ t β†’ unit :=
    Included_HASH.(S.HASH.pp_short).

  Definition op_eq : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_eq).

  Definition op_ltgt : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_ltgt).

  Definition op_lt : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_lt).

  Definition op_lteq : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_lteq).

  Definition op_gteq : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_gteq).

  Definition op_gt : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_gt).

  Definition compare : t β†’ t β†’ int := Included_HASH.(S.HASH.compare).

  Definition equal : t β†’ t β†’ bool := Included_HASH.(S.HASH.equal).

  Definition max : t β†’ t β†’ t := Included_HASH.(S.HASH.max).

  Definition min : t β†’ t β†’ t := Included_HASH.(S.HASH.min).

  Definition hash_bytes : option bytes β†’ list bytes β†’ t :=
    Included_HASH.(S.HASH.hash_bytes).

  Definition hash_string : option string β†’ list string β†’ t :=
    Included_HASH.(S.HASH.hash_string).

  Definition zero : t := Included_HASH.(S.HASH.zero).

  Definition size_value : int := Included_HASH.(S.HASH.size_value).

  Definition to_bytes : t β†’ bytes := Included_HASH.(S.HASH.to_bytes).

  Definition of_bytes_opt : bytes β†’ option t :=
    Included_HASH.(S.HASH.of_bytes_opt).

  Definition of_bytes_exn : bytes β†’ t := Included_HASH.(S.HASH.of_bytes_exn).

  Definition to_b58check : t β†’ string := Included_HASH.(S.HASH.to_b58check).

  Definition to_short_b58check : t β†’ string :=
    Included_HASH.(S.HASH.to_short_b58check).

  Definition of_b58check_exn : string β†’ t :=
    Included_HASH.(S.HASH.of_b58check_exn).

  Definition of_b58check_opt : string β†’ option t :=
    Included_HASH.(S.HASH.of_b58check_opt).

  Definition b58check_encoding : Base58.encoding t :=
    Included_HASH.(S.HASH.b58check_encoding).

  Definition encoding : Data_encoding.t t := Included_HASH.(S.HASH.encoding).

  Definition rpc_arg : RPC_arg.t t := Included_HASH.(S.HASH.rpc_arg).

  Definition _Set := Included_HASH.(S.HASH._Set).

  Definition Map := Included_HASH.(S.HASH.Map).
End Block_hash_signature.
Require Export TezosOfOCaml.Environment.V7.Block_hash.
Module Block_hash_check : Block_hash_signature := Block_hash.

Module Type Operation_hash_signature.
  Parameter Included_HASH_t : Set.

  Parameter Included_HASH_Set_t : Set.

  Parameter Included_HASH_Map_t : Set β†’ Set.

  Parameter Included_HASH :
    S.HASH (t := Included_HASH_t) (Set_t := Included_HASH_Set_t)
      (Map_t := Included_HASH_Map_t).

  Definition t := Included_HASH.(S.HASH.t).

  Definition name : string := Included_HASH.(S.HASH.name).

  Definition title : string := Included_HASH.(S.HASH.title).

  Definition pp : Format.formatter β†’ t β†’ unit := Included_HASH.(S.HASH.pp).

  Definition pp_short : Format.formatter β†’ t β†’ unit :=
    Included_HASH.(S.HASH.pp_short).

  Definition op_eq : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_eq).

  Definition op_ltgt : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_ltgt).

  Definition op_lt : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_lt).

  Definition op_lteq : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_lteq).

  Definition op_gteq : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_gteq).

  Definition op_gt : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_gt).

  Definition compare : t β†’ t β†’ int := Included_HASH.(S.HASH.compare).

  Definition equal : t β†’ t β†’ bool := Included_HASH.(S.HASH.equal).

  Definition max : t β†’ t β†’ t := Included_HASH.(S.HASH.max).

  Definition min : t β†’ t β†’ t := Included_HASH.(S.HASH.min).

  Definition hash_bytes : option bytes β†’ list bytes β†’ t :=
    Included_HASH.(S.HASH.hash_bytes).

  Definition hash_string : option string β†’ list string β†’ t :=
    Included_HASH.(S.HASH.hash_string).

  Definition zero : t := Included_HASH.(S.HASH.zero).

  Definition size_value : int := Included_HASH.(S.HASH.size_value).

  Definition to_bytes : t β†’ bytes := Included_HASH.(S.HASH.to_bytes).

  Definition of_bytes_opt : bytes β†’ option t :=
    Included_HASH.(S.HASH.of_bytes_opt).

  Definition of_bytes_exn : bytes β†’ t := Included_HASH.(S.HASH.of_bytes_exn).

  Definition to_b58check : t β†’ string := Included_HASH.(S.HASH.to_b58check).

  Definition to_short_b58check : t β†’ string :=
    Included_HASH.(S.HASH.to_short_b58check).

  Definition of_b58check_exn : string β†’ t :=
    Included_HASH.(S.HASH.of_b58check_exn).

  Definition of_b58check_opt : string β†’ option t :=
    Included_HASH.(S.HASH.of_b58check_opt).

  Definition b58check_encoding : Base58.encoding t :=
    Included_HASH.(S.HASH.b58check_encoding).

  Definition encoding : Data_encoding.t t := Included_HASH.(S.HASH.encoding).

  Definition rpc_arg : RPC_arg.t t := Included_HASH.(S.HASH.rpc_arg).

  Definition _Set := Included_HASH.(S.HASH._Set).

  Definition Map := Included_HASH.(S.HASH.Map).
End Operation_hash_signature.
Require Export TezosOfOCaml.Environment.V7.Operation_hash.
Module Operation_hash_check : Operation_hash_signature := Operation_hash.

Module Type Operation_list_hash_signature.
  Parameter Included_MERKLE_TREE_t : Set.

  Parameter Included_MERKLE_TREE_Set_t : Set.

  Parameter Included_MERKLE_TREE_Map_t : Set β†’ Set.

  Parameter Included_MERKLE_TREE_path : Set.

  Parameter Included_MERKLE_TREE :
    S.MERKLE_TREE (elt := Operation_hash.t) (t := Included_MERKLE_TREE_t)
      (Set_t := Included_MERKLE_TREE_Set_t)
      (Map_t := Included_MERKLE_TREE_Map_t) (path := Included_MERKLE_TREE_path).

  Definition elt := Included_MERKLE_TREE.(S.MERKLE_TREE.elt).

  Definition t := Included_MERKLE_TREE.(S.MERKLE_TREE.t).

  Definition name : string := Included_MERKLE_TREE.(S.MERKLE_TREE.name).

  Definition title : string := Included_MERKLE_TREE.(S.MERKLE_TREE.title).

  Definition pp : Format.formatter β†’ t β†’ unit :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.pp).

  Definition pp_short : Format.formatter β†’ t β†’ unit :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.pp_short).

  Definition op_eq : t β†’ t β†’ bool :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.op_eq).

  Definition op_ltgt : t β†’ t β†’ bool :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.op_ltgt).

  Definition op_lt : t β†’ t β†’ bool :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.op_lt).

  Definition op_lteq : t β†’ t β†’ bool :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.op_lteq).

  Definition op_gteq : t β†’ t β†’ bool :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.op_gteq).

  Definition op_gt : t β†’ t β†’ bool :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.op_gt).

  Definition compare : t β†’ t β†’ int :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.compare).

  Definition equal : t β†’ t β†’ bool :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.equal).

  Definition max : t β†’ t β†’ t := Included_MERKLE_TREE.(S.MERKLE_TREE.max).

  Definition min : t β†’ t β†’ t := Included_MERKLE_TREE.(S.MERKLE_TREE.min).

  Definition hash_bytes : option bytes β†’ list bytes β†’ t :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.hash_bytes).

  Definition hash_string : option string β†’ list string β†’ t :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.hash_string).

  Definition zero : t := Included_MERKLE_TREE.(S.MERKLE_TREE.zero).

  Definition size_value : int :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.size_value).

  Definition to_bytes : t β†’ bytes :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.to_bytes).

  Definition of_bytes_opt : bytes β†’ option t :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.of_bytes_opt).

  Definition of_bytes_exn : bytes β†’ t :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.of_bytes_exn).

  Definition to_b58check : t β†’ string :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.to_b58check).

  Definition to_short_b58check : t β†’ string :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.to_short_b58check).

  Definition of_b58check_exn : string β†’ t :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.of_b58check_exn).

  Definition of_b58check_opt : string β†’ option t :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.of_b58check_opt).

  Definition b58check_encoding : Base58.encoding t :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.b58check_encoding).

  Definition encoding : Data_encoding.t t :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.encoding).

  Definition rpc_arg : RPC_arg.t t :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.rpc_arg).

  Definition _Set := Included_MERKLE_TREE.(S.MERKLE_TREE._Set).

  Definition Map := Included_MERKLE_TREE.(S.MERKLE_TREE.Map).

  Definition compute : list elt β†’ t :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.compute).

  Definition empty : t := Included_MERKLE_TREE.(S.MERKLE_TREE.empty).

  Definition path := Included_MERKLE_TREE.(S.MERKLE_TREE.path).

  Definition compute_path : list elt β†’ int β†’ path :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.compute_path).

  Definition check_path : path β†’ elt β†’ t Γ— int :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.check_path).

  Definition path_encoding : Data_encoding.t path :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.path_encoding).
End Operation_list_hash_signature.
Require Export TezosOfOCaml.Environment.V7.Operation_list_hash.
Module Operation_list_hash_check : Operation_list_hash_signature := Operation_list_hash.

Module Type Operation_list_list_hash_signature.
  Parameter Included_MERKLE_TREE_t : Set.

  Parameter Included_MERKLE_TREE_Set_t : Set.

  Parameter Included_MERKLE_TREE_Map_t : Set β†’ Set.

  Parameter Included_MERKLE_TREE_path : Set.

  Parameter Included_MERKLE_TREE :
    S.MERKLE_TREE (elt := Operation_list_hash.t) (t := Included_MERKLE_TREE_t)
      (Set_t := Included_MERKLE_TREE_Set_t)
      (Map_t := Included_MERKLE_TREE_Map_t) (path := Included_MERKLE_TREE_path).

  Definition elt := Included_MERKLE_TREE.(S.MERKLE_TREE.elt).

  Definition t := Included_MERKLE_TREE.(S.MERKLE_TREE.t).

  Definition name : string := Included_MERKLE_TREE.(S.MERKLE_TREE.name).

  Definition title : string := Included_MERKLE_TREE.(S.MERKLE_TREE.title).

  Definition pp : Format.formatter β†’ t β†’ unit :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.pp).

  Definition pp_short : Format.formatter β†’ t β†’ unit :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.pp_short).

  Definition op_eq : t β†’ t β†’ bool :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.op_eq).

  Definition op_ltgt : t β†’ t β†’ bool :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.op_ltgt).

  Definition op_lt : t β†’ t β†’ bool :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.op_lt).

  Definition op_lteq : t β†’ t β†’ bool :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.op_lteq).

  Definition op_gteq : t β†’ t β†’ bool :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.op_gteq).

  Definition op_gt : t β†’ t β†’ bool :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.op_gt).

  Definition compare : t β†’ t β†’ int :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.compare).

  Definition equal : t β†’ t β†’ bool :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.equal).

  Definition max : t β†’ t β†’ t := Included_MERKLE_TREE.(S.MERKLE_TREE.max).

  Definition min : t β†’ t β†’ t := Included_MERKLE_TREE.(S.MERKLE_TREE.min).

  Definition hash_bytes : option bytes β†’ list bytes β†’ t :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.hash_bytes).

  Definition hash_string : option string β†’ list string β†’ t :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.hash_string).

  Definition zero : t := Included_MERKLE_TREE.(S.MERKLE_TREE.zero).

  Definition size_value : int :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.size_value).

  Definition to_bytes : t β†’ bytes :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.to_bytes).

  Definition of_bytes_opt : bytes β†’ option t :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.of_bytes_opt).

  Definition of_bytes_exn : bytes β†’ t :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.of_bytes_exn).

  Definition to_b58check : t β†’ string :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.to_b58check).

  Definition to_short_b58check : t β†’ string :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.to_short_b58check).

  Definition of_b58check_exn : string β†’ t :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.of_b58check_exn).

  Definition of_b58check_opt : string β†’ option t :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.of_b58check_opt).

  Definition b58check_encoding : Base58.encoding t :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.b58check_encoding).

  Definition encoding : Data_encoding.t t :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.encoding).

  Definition rpc_arg : RPC_arg.t t :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.rpc_arg).

  Definition _Set := Included_MERKLE_TREE.(S.MERKLE_TREE._Set).

  Definition Map := Included_MERKLE_TREE.(S.MERKLE_TREE.Map).

  Definition compute : list elt β†’ t :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.compute).

  Definition empty : t := Included_MERKLE_TREE.(S.MERKLE_TREE.empty).

  Definition path := Included_MERKLE_TREE.(S.MERKLE_TREE.path).

  Definition compute_path : list elt β†’ int β†’ path :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.compute_path).

  Definition check_path : path β†’ elt β†’ t Γ— int :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.check_path).

  Definition path_encoding : Data_encoding.t path :=
    Included_MERKLE_TREE.(S.MERKLE_TREE.path_encoding).
End Operation_list_list_hash_signature.
Require Export TezosOfOCaml.Environment.V7.Operation_list_list_hash.
Module Operation_list_list_hash_check : Operation_list_list_hash_signature := Operation_list_list_hash.

Module Type Protocol_hash_signature.
  Parameter Included_HASH_t : Set.

  Parameter Included_HASH_Set_t : Set.

  Parameter Included_HASH_Map_t : Set β†’ Set.

  Parameter Included_HASH :
    S.HASH (t := Included_HASH_t) (Set_t := Included_HASH_Set_t)
      (Map_t := Included_HASH_Map_t).

  Definition t := Included_HASH.(S.HASH.t).

  Definition name : string := Included_HASH.(S.HASH.name).

  Definition title : string := Included_HASH.(S.HASH.title).

  Definition pp : Format.formatter β†’ t β†’ unit := Included_HASH.(S.HASH.pp).

  Definition pp_short : Format.formatter β†’ t β†’ unit :=
    Included_HASH.(S.HASH.pp_short).

  Definition op_eq : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_eq).

  Definition op_ltgt : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_ltgt).

  Definition op_lt : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_lt).

  Definition op_lteq : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_lteq).

  Definition op_gteq : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_gteq).

  Definition op_gt : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_gt).

  Definition compare : t β†’ t β†’ int := Included_HASH.(S.HASH.compare).

  Definition equal : t β†’ t β†’ bool := Included_HASH.(S.HASH.equal).

  Definition max : t β†’ t β†’ t := Included_HASH.(S.HASH.max).

  Definition min : t β†’ t β†’ t := Included_HASH.(S.HASH.min).

  Definition hash_bytes : option bytes β†’ list bytes β†’ t :=
    Included_HASH.(S.HASH.hash_bytes).

  Definition hash_string : option string β†’ list string β†’ t :=
    Included_HASH.(S.HASH.hash_string).

  Definition zero : t := Included_HASH.(S.HASH.zero).

  Definition size_value : int := Included_HASH.(S.HASH.size_value).

  Definition to_bytes : t β†’ bytes := Included_HASH.(S.HASH.to_bytes).

  Definition of_bytes_opt : bytes β†’ option t :=
    Included_HASH.(S.HASH.of_bytes_opt).

  Definition of_bytes_exn : bytes β†’ t := Included_HASH.(S.HASH.of_bytes_exn).

  Definition to_b58check : t β†’ string := Included_HASH.(S.HASH.to_b58check).

  Definition to_short_b58check : t β†’ string :=
    Included_HASH.(S.HASH.to_short_b58check).

  Definition of_b58check_exn : string β†’ t :=
    Included_HASH.(S.HASH.of_b58check_exn).

  Definition of_b58check_opt : string β†’ option t :=
    Included_HASH.(S.HASH.of_b58check_opt).

  Definition b58check_encoding : Base58.encoding t :=
    Included_HASH.(S.HASH.b58check_encoding).

  Definition encoding : Data_encoding.t t := Included_HASH.(S.HASH.encoding).

  Definition rpc_arg : RPC_arg.t t := Included_HASH.(S.HASH.rpc_arg).

  Definition _Set := Included_HASH.(S.HASH._Set).

  Definition Map := Included_HASH.(S.HASH.Map).
End Protocol_hash_signature.
Require Export TezosOfOCaml.Environment.V7.Protocol_hash.
Module Protocol_hash_check : Protocol_hash_signature := Protocol_hash.

Module Type Context_hash_signature.
  Parameter Included_HASH_t : Set.

  Parameter Included_HASH_Set_t : Set.

  Parameter Included_HASH_Map_t : Set β†’ Set.

  Parameter Included_HASH :
    S.HASH (t := Included_HASH_t) (Set_t := Included_HASH_Set_t)
      (Map_t := Included_HASH_Map_t).

  Definition t := Included_HASH.(S.HASH.t).

  Definition name : string := Included_HASH.(S.HASH.name).

  Definition title : string := Included_HASH.(S.HASH.title).

  Definition pp : Format.formatter β†’ t β†’ unit := Included_HASH.(S.HASH.pp).

  Definition pp_short : Format.formatter β†’ t β†’ unit :=
    Included_HASH.(S.HASH.pp_short).

  Definition op_eq : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_eq).

  Definition op_ltgt : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_ltgt).

  Definition op_lt : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_lt).

  Definition op_lteq : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_lteq).

  Definition op_gteq : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_gteq).

  Definition op_gt : t β†’ t β†’ bool := Included_HASH.(S.HASH.op_gt).

  Definition compare : t β†’ t β†’ int := Included_HASH.(S.HASH.compare).

  Definition equal : t β†’ t β†’ bool := Included_HASH.(S.HASH.equal).

  Definition max : t β†’ t β†’ t := Included_HASH.(S.HASH.max).

  Definition min : t β†’ t β†’ t := Included_HASH.(S.HASH.min).

  Definition hash_bytes : option bytes β†’ list bytes β†’ t :=
    Included_HASH.(S.HASH.hash_bytes).

  Definition hash_string : option string β†’ list string β†’ t :=
    Included_HASH.(S.HASH.hash_string).

  Definition zero : t := Included_HASH.(S.HASH.zero).

  Definition size_value : int := Included_HASH.(S.HASH.size_value).

  Definition to_bytes : t β†’ bytes := Included_HASH.(S.HASH.to_bytes).

  Definition of_bytes_opt : bytes β†’ option t :=
    Included_HASH.(S.HASH.of_bytes_opt).

  Definition of_bytes_exn : bytes β†’ t := Included_HASH.(S.HASH.of_bytes_exn).

  Definition to_b58check : t β†’ string := Included_HASH.(S.HASH.to_b58check).

  Definition to_short_b58check : t β†’ string :=
    Included_HASH.(S.HASH.to_short_b58check).

  Definition of_b58check_exn : string β†’ t :=
    Included_HASH.(S.HASH.of_b58check_exn).

  Definition of_b58check_opt : string β†’ option t :=
    Included_HASH.(S.HASH.of_b58check_opt).

  Definition b58check_encoding : Base58.encoding t :=
    Included_HASH.(S.HASH.b58check_encoding).

  Definition encoding : Data_encoding.t t := Included_HASH.(S.HASH.encoding).

  Definition rpc_arg : RPC_arg.t t := Included_HASH.(S.HASH.rpc_arg).

  Definition _Set := Included_HASH.(S.HASH._Set).

  Definition Map := Included_HASH.(S.HASH.Map).

  Module Version.
    Definition t : Set := int.

    Parameter Included_S : Compare.S (t := t).

    Definition op_eq : t β†’ t β†’ bool := Included_S.(Compare.S.op_eq).

    Definition op_ltgt : t β†’ t β†’ bool := Included_S.(Compare.S.op_ltgt).

    Definition op_lt : t β†’ t β†’ bool := Included_S.(Compare.S.op_lt).

    Definition op_lteq : t β†’ t β†’ bool := Included_S.(Compare.S.op_lteq).

    Definition op_gteq : t β†’ t β†’ bool := Included_S.(Compare.S.op_gteq).

    Definition op_gt : t β†’ t β†’ bool := Included_S.(Compare.S.op_gt).

    Definition compare : t β†’ t β†’ int := Included_S.(Compare.S.compare).

    Definition equal : t β†’ t β†’ bool := Included_S.(Compare.S.equal).

    Definition max : t β†’ t β†’ t := Included_S.(Compare.S.max).

    Definition min : t β†’ t β†’ t := Included_S.(Compare.S.min).

    Parameter pp : Format.formatter β†’ t β†’ unit.

    Parameter encoding : Data_encoding.t t.

    Parameter of_int : int β†’ t.
  End Version.

  Definition version : Set := Version.t.
End Context_hash_signature.
Require Export TezosOfOCaml.Environment.V7.Context_hash.
Module Context_hash_check : Context_hash_signature := Context_hash.

Module Type Sapling_signature.
  Module Ciphertext.
    Parameter t : Set.

    Parameter encoding : Data_encoding.t t.

    Parameter get_memo_size : t β†’ int.
  End Ciphertext.

  Module Commitment.
    Parameter t : Set.

    Parameter encoding : Data_encoding.t t.

    Parameter valid_position : int64 β†’ bool.
  End Commitment.

  Module CV.
    Parameter t : Set.

    Parameter encoding : Data_encoding.t t.
  End CV.

  Module Hash.
    Parameter t : Set.

    Parameter compare : t β†’ t β†’ int.

    Parameter encoding : Data_encoding.t t.

    Parameter to_bytes : t β†’ Bytes.t.

    Parameter of_bytes_exn : Bytes.t β†’ t.

    Parameter uncommitted : int β†’ t.

    Parameter merkle_hash : int β†’ t β†’ t β†’ t.

    Parameter of_commitment : Commitment.t β†’ t.

    Parameter to_commitment : t β†’ Commitment.t.
  End Hash.

  Module Nullifier.
    Parameter t : Set.

    Parameter encoding : Data_encoding.t t.

    Parameter compare : t β†’ t β†’ int.
  End Nullifier.

  Module UTXO.
    Parameter rk : Set.

    Parameter spend_proof : Set.

    Parameter spend_sig : Set.

    Parameter output_proof : Set.

    Module input.
      Record record : Set := Build {
        cv : CV.t;
        nf : Nullifier.t;
        rk : rk;
        proof_i : spend_proof;
        signature : spend_sig;
      }.
      Definition with_cv cv (r : record) :=
        Build cv r.(nf) r.(rk) r.(proof_i) r.(signature).
      Definition with_nf nf (r : record) :=
        Build r.(cv) nf r.(rk) r.(proof_i) r.(signature).
      Definition with_rk rk (r : record) :=
        Build r.(cv) r.(nf) rk r.(proof_i) r.(signature).
      Definition with_proof_i proof_i (r : record) :=
        Build r.(cv) r.(nf) r.(rk) proof_i r.(signature).
      Definition with_signature signature (r : record) :=
        Build r.(cv) r.(nf) r.(rk) r.(proof_i) signature.
    End input.
    Definition input := input.record.

    Parameter input_encoding : Data_encoding.t input.

    Module output.
      Record record : Set := Build {
        cm : Commitment.t;
        proof_o : output_proof;
        ciphertext : Ciphertext.t;
      }.
      Definition with_cm cm (r : record) :=
        Build cm r.(proof_o) r.(ciphertext).
      Definition with_proof_o proof_o (r : record) :=
        Build r.(cm) proof_o r.(ciphertext).
      Definition with_ciphertext ciphertext (r : record) :=
        Build r.(cm) r.(proof_o) ciphertext.
    End output.
    Definition output := output.record.

    Parameter output_encoding : Data_encoding.t output.

    Parameter binding_sig : Set.

    Module transaction.
      Record record : Set := Build {
        inputs : list input;
        outputs : list output;
        binding_sig : binding_sig;
        balance : Int64.t;
        root : Hash.t;
        bound_data : string;
      }.
      Definition with_inputs inputs (r : record) :=
        Build inputs r.(outputs) r.(binding_sig) r.(balance) r.(root)
          r.(bound_data).
      Definition with_outputs outputs (r : record) :=
        Build r.(inputs) outputs r.(binding_sig) r.(balance) r.(root)
          r.(bound_data).
      Definition with_binding_sig binding_sig (r : record) :=
        Build r.(inputs) r.(outputs) binding_sig r.(balance) r.(root)
          r.(bound_data).
      Definition with_balance balance (r : record) :=
        Build r.(inputs) r.(outputs) r.(binding_sig) balance r.(root)
          r.(bound_data).
      Definition with_root root (r : record) :=
        Build r.(inputs) r.(outputs) r.(binding_sig) r.(balance) root
          r.(bound_data).
      Definition with_bound_data bound_data (r : record) :=
        Build r.(inputs) r.(outputs) r.(binding_sig) r.(balance) r.(root)
          bound_data.
    End transaction.
    Definition transaction := transaction.record.

    Parameter transaction_encoding : Data_encoding.t transaction.

    Parameter binding_sig_encoding : Data_encoding.t binding_sig.

    Module Legacy.
      Definition transaction_new : Set := transaction.

      Module transaction.
        Record record : Set := Build {
          inputs : list input;
          outputs : list output;
          binding_sig : binding_sig;
          balance : Int64.t;
          root : Hash.t;
        }.
        Definition with_inputs inputs (r : record) :=
          Build inputs r.(outputs) r.(binding_sig) r.(balance) r.(root).
        Definition with_outputs outputs (r : record) :=
          Build r.(inputs) outputs r.(binding_sig) r.(balance) r.(root).
        Definition with_binding_sig binding_sig (r : record) :=
          Build r.(inputs) r.(outputs) binding_sig r.(balance) r.(root).
        Definition with_balance balance (r : record) :=
          Build r.(inputs) r.(outputs) r.(binding_sig) balance r.(root).
        Definition with_root root (r : record) :=
          Build r.(inputs) r.(outputs) r.(binding_sig) r.(balance) root.
      End transaction.
      Definition transaction := transaction.record.

      Parameter transaction_encoding : Data_encoding.t transaction.

      Parameter cast : transaction β†’ transaction_new.
    End Legacy.
  End UTXO.

  Module Verification.
    Parameter t : Set.

    Parameter with_verification_ctx : βˆ€ {a : Set}, (t β†’ a) β†’ a.

    Parameter check_spend : t β†’ UTXO.input β†’ Hash.t β†’ string β†’ bool.

    Parameter check_output : t β†’ UTXO.output β†’ bool.

    Parameter final_check : t β†’ UTXO.transaction β†’ string β†’ bool.
  End Verification.
End Sapling_signature.
Require Export TezosOfOCaml.Environment.V7.Sapling.
Module Sapling_check : Sapling_signature := Sapling.

Module Type Timelock_signature.
  Parameter chest : Set.

  Parameter chest_encoding : Data_encoding.t chest.

  Parameter chest_key : Set.

  Parameter chest_key_encoding : Data_encoding.t chest_key.

  Inductive opening_result : Set :=
  | Correct : Bytes.t β†’ opening_result
  | Bogus_cipher : opening_result
  | Bogus_opening : opening_result.

  Parameter open_chest : chest β†’ chest_key β†’ int β†’ opening_result.

  Parameter get_plaintext_size : chest β†’ int.
End Timelock_signature.
Require Export TezosOfOCaml.Environment.V7.Timelock.
Module Timelock_check : Timelock_signature := Timelock.

Module Type Vdf_signature.
  Parameter form_size_bytes : int.

  Parameter discriminant_size_bytes : int.

  Parameter discriminant : Set.

  Parameter challenge : Set.

  Parameter result : Set.

  Parameter proof : Set.

  Definition difficulty : Set := Int64.t.

  Parameter discriminant_to_bytes : discriminant β†’ bytes.

  Parameter discriminant_of_bytes_opt : bytes β†’ option discriminant.

  Parameter challenge_to_bytes : challenge β†’ bytes.

  Parameter challenge_of_bytes_opt : bytes β†’ option challenge.

  Parameter result_to_bytes : result β†’ bytes.

  Parameter result_of_bytes_opt : bytes β†’ option result.

  Parameter proof_to_bytes : proof β†’ bytes.

  Parameter proof_of_bytes_opt : bytes β†’ option proof.

  Parameter generate_discriminant : option Bytes.t β†’ int β†’ discriminant.

  Parameter generate_challenge : discriminant β†’ Bytes.t β†’ challenge.

  Parameter prove : discriminant β†’ challenge β†’ difficulty β†’ result Γ— proof.

  Parameter verify :
    discriminant β†’ challenge β†’ difficulty β†’ result β†’ proof β†’ bool.
End Vdf_signature.
Require Export TezosOfOCaml.Environment.V7.Vdf.
Module Vdf_check : Vdf_signature := Vdf.

Module Type Micheline_signature.
  Definition annot : Set := list string.

  Inductive node (l p : Set) : Set :=
  | Int : l β†’ Z.t β†’ node l p
  | String : l β†’ string β†’ node l p
  | Bytes : l β†’ bytes β†’ node l p
  | Prim : l β†’ p β†’ list (node l p) β†’ annot β†’ node l p
  | Seq : l β†’ list (node l p) β†’ node l p.

  Arguments Int {_ _}.
  Arguments String {_ _}.
  Arguments Bytes {_ _}.
  Arguments Prim {_ _}.
  Arguments Seq {_ _}.

  Parameter canonical : βˆ€ (p : Set), Set.

  Parameter canonical_location : Set.

  Parameter dummy_location : canonical_location.

  Parameter root_value : βˆ€ {p : Set},
    canonical p β†’ node canonical_location p.

  Parameter canonical_location_encoding :
    Data_encoding.encoding canonical_location.

  Parameter canonical_encoding : βˆ€ {l : Set},
    string β†’ Data_encoding.encoding l β†’ Data_encoding.encoding (canonical l).

  Parameter location : βˆ€ {l p : Set}, node l p β†’ l.

  Parameter annotations : βˆ€ {l p : Set}, node l p β†’ list string.

  Parameter strip_locations : βˆ€ {A p : Set}, node A p β†’ canonical p.
End Micheline_signature.
Require Export TezosOfOCaml.Environment.V7.Micheline.
Module Micheline_check : Micheline_signature := Micheline.

Module Type Block_header_signature.
  Module shell_header.
    Record record : Set := Build {
      level : Int32.t;
      proto_level : int;
      predecessor : Block_hash.t;
      timestamp : Time.t;
      validation_passes : int;
      operations_hash : Operation_list_list_hash.t;
      fitness : list Bytes.t;
      context : Context_hash.t;
    }.
    Definition with_level level (r : record) :=
      Build level r.(proto_level) r.(predecessor) r.(timestamp)
        r.(validation_passes) r.(operations_hash) r.(fitness) r.(context).
    Definition with_proto_level proto_level (r : record) :=
      Build r.(level) proto_level r.(predecessor) r.(timestamp)
        r.(validation_passes) r.(operations_hash) r.(fitness) r.(context).
    Definition with_predecessor predecessor (r : record) :=
      Build r.(level) r.(proto_level) predecessor r.(timestamp)
        r.(validation_passes) r.(operations_hash) r.(fitness) r.(context).
    Definition with_timestamp timestamp (r : record) :=
      Build r.(level) r.(proto_level) r.(predecessor) timestamp
        r.(validation_passes) r.(operations_hash) r.(fitness) r.(context).
    Definition with_validation_passes validation_passes (r : record) :=
      Build r.(level) r.(proto_level) r.(predecessor) r.(timestamp)
        validation_passes r.(operations_hash) r.(fitness) r.(context).
    Definition with_operations_hash operations_hash (r : record) :=
      Build r.(level) r.(proto_level) r.(predecessor) r.(timestamp)
        r.(validation_passes) operations_hash r.(fitness) r.(context).
    Definition with_fitness fitness (r : record) :=
      Build r.(level) r.(proto_level) r.(predecessor) r.(timestamp)
        r.(validation_passes) r.(operations_hash) fitness r.(context).
    Definition with_context context (r : record) :=
      Build r.(level) r.(proto_level) r.(predecessor) r.(timestamp)
        r.(validation_passes) r.(operations_hash) r.(fitness) context.
  End shell_header.
  Definition shell_header := shell_header.record.

  Parameter shell_header_encoding : Data_encoding.t shell_header.

  Module t.
    Record record : Set := Build {
      shell : shell_header;
      protocol_data : bytes;
    }.
    Definition with_shell shell (r : record) :=
      Build shell r.(protocol_data).
    Definition with_protocol_data protocol_data (r : record) :=
      Build r.(shell) protocol_data.
  End t.
  Definition t := t.record.

  Parameter Included_HASHABLE : S.HASHABLE (t := t) (hash := Block_hash.t).

  Definition op_eq : t β†’ t β†’ bool := Included_HASHABLE.(S.HASHABLE.op_eq).

  Definition op_ltgt : t β†’ t β†’ bool := Included_HASHABLE.(S.HASHABLE.op_ltgt).

  Definition op_lt : t β†’ t β†’ bool := Included_HASHABLE.(S.HASHABLE.op_lt).

  Definition op_lteq : t β†’ t β†’ bool := Included_HASHABLE.(S.HASHABLE.op_lteq).

  Definition op_gteq : t β†’ t β†’ bool := Included_HASHABLE.(S.HASHABLE.op_gteq).

  Definition op_gt : t β†’ t β†’ bool := Included_HASHABLE.(S.HASHABLE.op_gt).

  Definition compare : t β†’ t β†’ int := Included_HASHABLE.(S.HASHABLE.compare).

  Definition equal : t β†’ t β†’ bool := Included_HASHABLE.(S.HASHABLE.equal).

  Definition max : t β†’ t β†’ t := Included_HASHABLE.(S.HASHABLE.max).

  Definition min : t β†’ t β†’ t := Included_HASHABLE.(S.HASHABLE.min).

  Definition pp : Format.formatter β†’ t β†’ unit :=
    Included_HASHABLE.(S.HASHABLE.pp).

  Definition encoding : Data_encoding.t t :=
    Included_HASHABLE.(S.HASHABLE.encoding).

  Definition to_bytes : t β†’ bytes := Included_HASHABLE.(S.HASHABLE.to_bytes).

  Definition of_bytes : bytes β†’ option t :=
    Included_HASHABLE.(S.HASHABLE.of_bytes).

  Definition hash_value : t β†’ Block_hash.t :=
    Included_HASHABLE.(S.HASHABLE.hash_value).

  Definition hash_raw : bytes β†’ Block_hash.t :=
    Included_HASHABLE.(S.HASHABLE.hash_raw).
End Block_header_signature.
Require Export TezosOfOCaml.Environment.V7.Block_header.
Module Block_header_check : Block_header_signature := Block_header.

Module Type Bounded_signature.
  Module BOUNDS.
    Record signature {ocaml_type : Set} : Set := {
      
[ocaml_type] is the type used for the internal representation of values within the bounded interval. This is the type that values in the interval are converted to and from. E.g., for an interval of 32-bit integers [ocaml_type = int32].
      ocaml_type := ocaml_type;
      
[min_value] represents the minimal value (included) reprensatable.
      min_value : ocaml_type;
      
[max_value] represents the maximal value (included) reprensatable.
      max_value : ocaml_type;
    }.
  End BOUNDS.
  Definition BOUNDS := @BOUNDS.signature.
  Arguments BOUNDS {_}.

  Module S.
    Record signature {t ocaml_type : Set} : Set := {
      
Internal representation of a bounded value.
      t := t;
      
Underlying OCaml representation for the bounded value.
      ocaml_type := ocaml_type;
      min_value : ocaml_type;
      max_value : ocaml_type;
      op_eq : t β†’ t β†’ bool;
      op_ltgt : t β†’ t β†’ bool;
      op_lt : t β†’ t β†’ bool;
      op_lteq : t β†’ t β†’ bool;
      op_gteq : t β†’ t β†’ bool;
      op_gt : t β†’ t β†’ bool;
      compare : t β†’ t β†’ int;
      equal : t β†’ t β†’ bool;
      max : t β†’ t β†’ t;
      min : t β†’ t β†’ t;
      
A (partial) encoding of the datatype. If the encoded value is out of bounds, an exception may be raised. See {!val:Data_encoding.conv_with_guard}.
      encoding : Data_encoding.t t;
      
A pretty-printer for values of type [t].
      pp : Format.formatter β†’ t β†’ unit;
      
[to_value t] is a projection to the OCaml representation of the bounded value [t].
      to_value : t β†’ ocaml_type;
      
[of_value ocaml_value] represents [ocaml_value] as a bounded value. Returns [None] if the value is outside of the bounds specified by {!val:min_value} and {!val:max_value}.
      of_value : ocaml_type β†’ option t;
    }.
  End S.
  Definition S := @S.signature.
  Arguments S {_ _}.

  Parameter Int64_t : βˆ€ (B : BOUNDS (ocaml_type := int64)), Set.

  Parameter Int64 :
    βˆ€ (B : BOUNDS (ocaml_type := int64)),
    S (t := Int64_t B) (ocaml_type := int64).

  Parameter Int32_t : βˆ€ (B : BOUNDS (ocaml_type := int32)), Set.

  Parameter Int32 :
    βˆ€ (B : BOUNDS (ocaml_type := int32)),
    S (t := Int32_t B) (ocaml_type := int32).

  Parameter Non_negative_int32_t : Set.

  Parameter Non_negative_int32 :
    S (t := Non_negative_int32_t) (ocaml_type := int32).

  Parameter Int31_t : βˆ€ (B : BOUNDS (ocaml_type := int)), Set.

  Parameter Int31 :
    βˆ€ (B : BOUNDS (ocaml_type := int)),
    S (t := Int31_t B) (ocaml_type := int).

  Parameter Int16_t : βˆ€ (B : BOUNDS (ocaml_type := int)), Set.

  Parameter Int16 :
    βˆ€ (B : BOUNDS (ocaml_type := int)),
    S (t := Int16_t B) (ocaml_type := int).

  Parameter Uint16_t : βˆ€ (B : BOUNDS (ocaml_type := int)), Set.

  Parameter Uint16 :
    βˆ€ (B : BOUNDS (ocaml_type := int)),
    S (t := Uint16_t B) (ocaml_type := int).

  Parameter Int8_t : βˆ€ (B : BOUNDS (ocaml_type := int)), Set.

  Parameter Int8 :
    βˆ€ (B : BOUNDS (ocaml_type := int)),
    S (t := Int8_t B) (ocaml_type := int).

  Parameter Uint8_t : βˆ€ (B : BOUNDS (ocaml_type := int)), Set.

  Parameter Uint8 :
    βˆ€ (B : BOUNDS (ocaml_type := int)),
    S (t := Uint8_t B) (ocaml_type := int).
End Bounded_signature.
Require Export TezosOfOCaml.Environment.V7.Bounded.
Module Bounded_check : Bounded_signature := Bounded.

Module Type Fitness_signature.
  Parameter Included_T : S.T (t := list bytes).

  Definition t := Included_T.(S.T.t).

  Definition op_eq : t β†’ t β†’ bool := Included_T.(S.T.op_eq).

  Definition op_ltgt : t β†’ t β†’ bool := Included_T.(S.T.op_ltgt).

  Definition op_lt : t β†’ t β†’ bool := Included_T.(S.T.op_lt).

  Definition op_lteq : t β†’ t β†’ bool := Included_T.(S.T.op_lteq).

  Definition op_gteq : t β†’ t β†’ bool := Included_T.(S.T.op_gteq).

  Definition op_gt : t β†’ t β†’ bool := Included_T.(S.T.op_gt).

  Definition compare : t β†’ t β†’ int := Included_T.(S.T.compare).

  Definition equal : t β†’ t β†’ bool := Included_T.(S.T.equal).

  Definition max : t β†’ t β†’ t := Included_T.(S.T.max).

  Definition min : t β†’ t β†’ t := Included_T.(S.T.min).

  Definition pp : Format.formatter β†’ t β†’ unit := Included_T.(S.T.pp).

  Definition encoding : Data_encoding.t t := Included_T.(S.T.encoding).

  Definition to_bytes : t β†’ bytes := Included_T.(S.T.to_bytes).

  Definition of_bytes : bytes β†’ option t := Included_T.(S.T.of_bytes).
End Fitness_signature.
Require Export TezosOfOCaml.Environment.V7.Fitness.
Module Fitness_check : Fitness_signature := Fitness.

Module Type Operation_signature.
  Module shell_header.
    Record record : Set := Build {
      branch : Block_hash.t;
    }.
    Definition with_branch branch (r : record) :=
      Build branch.
  End shell_header.
  Definition shell_header := shell_header.record.

  Parameter shell_header_encoding : Data_encoding.t shell_header.

  Module t.
    Record record : Set := Build {
      shell : shell_header;
      proto : bytes;
    }.
    Definition with_shell shell (r : record) :=
      Build shell r.(proto).
    Definition with_proto proto (r : record) :=
      Build r.(shell) proto.
  End t.
  Definition t := t.record.

  Parameter Included_HASHABLE : S.HASHABLE (t := t) (hash := Operation_hash.t).

  Definition op_eq : t β†’ t β†’ bool := Included_HASHABLE.(S.HASHABLE.op_eq).

  Definition op_ltgt : t β†’ t β†’ bool := Included_HASHABLE.(S.HASHABLE.op_ltgt).

  Definition op_lt : t β†’ t β†’ bool := Included_HASHABLE.(S.HASHABLE.op_lt).

  Definition op_lteq : t β†’ t β†’ bool := Included_HASHABLE.(S.HASHABLE.op_lteq).

  Definition op_gteq : t β†’ t β†’ bool := Included_HASHABLE.(S.HASHABLE.op_gteq).

  Definition op_gt : t β†’ t β†’ bool := Included_HASHABLE.(S.HASHABLE.op_gt).

  Definition compare : t β†’ t β†’ int := Included_HASHABLE.(S.HASHABLE.compare).

  Definition equal : t β†’ t β†’ bool := Included_HASHABLE.(S.HASHABLE.equal).

  Definition max : t β†’ t β†’ t := Included_HASHABLE.(S.HASHABLE.max).

  Definition min : t β†’ t β†’ t := Included_HASHABLE.(S.HASHABLE.min).

  Definition pp : Format.formatter β†’ t β†’ unit :=
    Included_HASHABLE.(S.HASHABLE.pp).

  Definition encoding : Data_encoding.t t :=
    Included_HASHABLE.(S.HASHABLE.encoding).

  Definition to_bytes : t β†’ bytes := Included_HASHABLE.(S.HASHABLE.to_bytes).

  Definition of_bytes : bytes β†’ option t :=
    Included_HASHABLE.(S.HASHABLE.of_bytes).

  Definition hash_value : t β†’ Operation_hash.t :=
    Included_HASHABLE.(S.HASHABLE.hash_value).

  Definition hash_raw : bytes β†’ Operation_hash.t :=
    Included_HASHABLE.(S.HASHABLE.hash_raw).
End Operation_signature.
Require Export TezosOfOCaml.Environment.V7.Operation.
Module Operation_check : Operation_signature := Operation.

Module Type Context_signature.
  Inductive depth : Set :=
  | Ge : int β†’ depth
  | Lt : int β†’ depth
  | Eq : int β†’ depth
  | Le : int β†’ depth
  | Gt : int β†’ depth.

  Parameter config : Set.

  Parameter equal_config : config β†’ config β†’ bool.

  Module VIEW.
    Record signature {t key value tree : Set} : Set := {
      
The type for context views.
      t := t;
      
The type for context keys.
      key := key;
      
The type for context values.
      value := value;
      
The type for context trees.
      tree := tree;
      
[mem t k] is an Lwt promise that resolves to [true] iff [k] is bound to a value in [t].
      mem : t β†’ key β†’ bool;
      
[mem_tree t k] is like {!mem} but for trees.
      mem_tree : t β†’ key β†’ bool;
      
[find t k] is an Lwt promise that resolves to [Some v] if [k] is bound to the value [v] in [t] and [None] otherwise.
      find : t β†’ key β†’ option value;
      
[find_tree t k] is like {!find} but for trees.
      find_tree : t β†’ key β†’ option tree;
      
[list t key] is the list of files and sub-nodes stored under [k] in [t]. The result order is not specified but is stable.
[offset] and [length] are used for pagination.
      list_value : t β†’ option int β†’ option int β†’ key β†’ list (string Γ— tree);
      
[length t key] is an Lwt promise that resolves to the number of files and sub-nodes stored under [k] in [t].
It is equivalent to [list t k >|= List.length] but has a constant-time complexity.
      length : t β†’ key β†’ int;
      
[add t k v] is an Lwt promise that resolves to [c] such that: - [k] is bound to [v] in [c]; and [c] is similar to [t] otherwise.
If [k] was already bound in [t] to a value that is physically equal to [v], the result of the function is a promise that resolves to [t]. Otherwise, the previous binding of [k] in [t] disappears.
      add : t β†’ key β†’ value β†’ t;
      
[add_tree] is like {!add} but for trees.
      add_tree : t β†’ key β†’ tree β†’ t;
      
[remove t k v] is an Lwt promise that resolves to [c] such that: - [k] is unbound in [c]; and [c] is similar to [t] otherwise.
      remove : t β†’ key β†’ t;
      
[fold ?depth t root ~order ~init ~f] recursively folds over the trees and values of [t]. The [f] callbacks are called with a key relative to [root]. [f] is never called with an empty key for values; i.e., folding over a value is a no-op.
The depth is 0-indexed. If [depth] is set (by default it is not), then [f] is only called when the conditions described by the parameter is true: - [Eq d] folds over nodes and values of depth exactly [d]. [Lt d] folds over nodes and values of depth strictly less than [d]. [Le d] folds over nodes and values of depth less than or equal to [d]. [Gt d] folds over nodes and values of depth strictly more than [d]. [Ge d] folds over nodes and values of depth more than or equal to [d].
If [order] is [`Sorted] (the default), the elements are traversed in lexicographic order of their keys. For large nodes, it is memory-consuming, use [`Undefined] for a more memory efficient [fold].
      fold :
        βˆ€ {a : Set},
        option depth β†’ t β†’ key β†’ Variant.t β†’ a β†’ (key β†’ tree β†’ a β†’ a) β†’
        a;
      
[config t] is [t]'s hash configuration.
      config_value : t β†’ config;
    }.
  End VIEW.
  Definition VIEW := @VIEW.signature.
  Arguments VIEW {_ _ _ _}.

  Module Kind.
    Inductive t : Set :=
    | Tree : t
    | Value : t.
  End Kind.

  Module TREE.
    Record signature {t tree key value : Set} : Set := {
      
The type for context views.
      t := t;
      
The type for context trees.
      tree := tree;
      key := key;
      value := value;
      mem : tree β†’ key β†’ bool;
      mem_tree : tree β†’ key β†’ bool;
      find : tree β†’ key β†’ option value;
      find_tree : tree β†’ key β†’ option tree;
      list_value :
        tree β†’ option int β†’ option int β†’ key β†’ list (string Γ— tree);
      length : tree β†’ key β†’ int;
      add : tree β†’ key β†’ value β†’ tree;
      add_tree : tree β†’ key β†’ tree β†’ tree;
      remove : tree β†’ key β†’ tree;
      fold :
        βˆ€ {a : Set},
        option depth β†’ tree β†’ key β†’ Variant.t β†’ a β†’
        (key β†’ tree β†’ a β†’ a) β†’ a;
      config_value : tree β†’ config;
      
[empty _] is the empty tree.
      empty : t β†’ tree;
      
[is_empty t] is true iff [t] is [empty _].
      is_empty : tree β†’ bool;
      
[kind t] is [t]'s kind. It's either a tree node or a leaf value.
      kind_value : tree β†’ Kind.t;
      
[to_value t] is an Lwt promise that resolves to [Some v] if [t] is a leaf tree and [None] otherwise. It is equivalent to [find t ].
      to_value : tree β†’ option value;
      
[of_value _ v] is an Lwt promise that resolves to the leaf tree [v]. Is is equivalent to [add (empty _) v].
      of_value : t β†’ value β†’ tree;
      
[hash t] is [t]'s Merkle hash.
      hash_value : tree β†’ Context_hash.t;
      
[equal x y] is true iff [x] and [y] have the same Merkle hash.
      equal : tree β†’ tree β†’ bool;
      
[clear ?depth t] clears all caches in the tree [t] for subtrees with a depth higher than [depth]. If [depth] is not set, all of the subtrees are cleared.
      clear : option int β†’ tree β†’ unit;
    }.
  End TREE.
  Definition TREE := @TREE.signature.
  Arguments TREE {_ _ _ _}.

  Module Proof.
    Definition step : Set := string.

    Definition value : Set := bytes.

    Definition index : Set := int.

    Definition hash : Set := Context_hash.t.

    Module inode.
      Record record {a : Set} : Set := Build {
        length : int;
        proofs : list (index Γ— a);
      }.
      Arguments record : clear implicits.
      Definition with_length {t_a} length (r : record t_a) :=
        Build t_a length r.(proofs).
      Definition with_proofs {t_a} proofs (r : record t_a) :=
        Build t_a r.(length) proofs.
    End inode.
    Definition inode := inode.record.

    Module inode_extender.
      Record record {a : Set} : Set := Build {
        length : int;
        segment : list index;
        proof : a;
      }.
      Arguments record : clear implicits.
      Definition with_length {t_a} length (r : record t_a) :=
        Build t_a length r.(segment) r.(proof).
      Definition with_segment {t_a} segment (r : record t_a) :=
        Build t_a r.(length) segment r.(proof).
      Definition with_proof {t_a} proof (r : record t_a) :=
        Build t_a r.(length) r.(segment) proof.
    End inode_extender.
    Definition inode_extender := inode_extender.record.

    Inductive tree : Set :=
    | Value : value β†’ tree
    | Blinded_value : hash β†’ tree
    | Node : list (step Γ— tree) β†’ tree
    | Blinded_node : hash β†’ tree
    | Inode : inode inode_tree β†’ tree
    | Extender : inode_extender inode_tree β†’ tree
    
    with inode_tree : Set :=
    | Blinded_inode : hash β†’ inode_tree
    | Inode_values : list (step Γ— tree) β†’ inode_tree
    | Inode_tree : inode inode_tree β†’ inode_tree
    | Inode_extender : inode_extender inode_tree β†’ inode_tree.

    Inductive kinded_hash : Set :=
    | KNode : hash β†’ kinded_hash
    | KValue : hash β†’ kinded_hash.

    Module Stream.
      Inductive elt : Set :=
      | Value : value β†’ elt
      | Node : list (step Γ— kinded_hash) β†’ elt
      | Inode : inode hash β†’ elt
      | Inode_extender : inode_extender hash β†’ elt.

      Definition t : Set := Seq.t elt.
    End Stream.

    Definition stream : Set := Stream.t.

    Module t.
      Record record {a : Set} : Set := Build {
        version : int;
        before : kinded_hash;
        after : kinded_hash;
        state : a;
      }.
      Arguments record : clear implicits.
      Definition with_version {t_a} version (r : record t_a) :=
        Build t_a version r.(before) r.(after) r.(state).
      Definition with_before {t_a} before (r : record t_a) :=
        Build t_a r.(version) before r.(after) r.(state).
      Definition with_after {t_a} after (r : record t_a) :=
        Build t_a r.(version) r.(before) after r.(state).
      Definition with_state {t_a} state (r : record t_a) :=
        Build t_a r.(version) r.(before) r.(after) state.
    End t.
    Definition t := t.record.
  End Proof.

  Parameter Included_VIEW_t : Set.

  Parameter Included_VIEW_tree : Set.

  Parameter Included_VIEW :
    VIEW (t := Included_VIEW_t) (key := list string) (value := bytes)
      (tree := Included_VIEW_tree).

  Definition t := Included_VIEW.(VIEW.t).

  Definition key := Included_VIEW.(VIEW.key).

  Definition value := Included_VIEW.(VIEW.value).

  Definition tree := Included_VIEW.(VIEW.tree).

  Definition mem : t β†’ key β†’ bool := Included_VIEW.(VIEW.mem).

  Definition mem_tree : t β†’ key β†’ bool := Included_VIEW.(VIEW.mem_tree).

  Definition find : t β†’ key β†’ option value := Included_VIEW.(VIEW.find).

  Definition find_tree : t β†’ key β†’ option tree :=
    Included_VIEW.(VIEW.find_tree).

  Definition list_value :
    t β†’ option int β†’ option int β†’ key β†’ list (string Γ— tree) :=
    Included_VIEW.(VIEW.list_value).

  Definition length : t β†’ key β†’ int := Included_VIEW.(VIEW.length).

  Definition add : t β†’ key β†’ value β†’ t := Included_VIEW.(VIEW.add).

  Definition add_tree : t β†’ key β†’ tree β†’ t := Included_VIEW.(VIEW.add_tree).

  Definition remove : t β†’ key β†’ t := Included_VIEW.(VIEW.remove).

  Definition fold {a : Set} :
    option depth β†’ t β†’ key β†’ Variant.t β†’ a β†’ (key β†’ tree β†’ a β†’ a) β†’ a
    := Included_VIEW.(VIEW.fold).

  Definition config_value : t β†’ config := Included_VIEW.(VIEW.config_value).

  Parameter Tree : TREE (t := t) (tree := tree) (key := key) (value := value).

  Definition verifier (proof result : Set) : Set :=
    proof β†’ (tree β†’ tree Γ— result) β†’
    Pervasives.result (tree Γ— result) Variant.t.

  Definition tree_proof : Set := Proof.t Proof.tree.

  Parameter verify_tree_proof : βˆ€ {a : Set}, verifier tree_proof a.

  Definition stream_proof : Set := Proof.t Proof.stream.

  Parameter verify_stream_proof : βˆ€ {a : Set}, verifier stream_proof a.

  Module PROOF_ENCODING.
    Record signature : Set := {
      tree_proof_encoding : Data_encoding.t tree_proof;
      stream_proof_encoding : Data_encoding.t stream_proof;
    }.
  End PROOF_ENCODING.
  Definition PROOF_ENCODING := PROOF_ENCODING.signature.

  Module Proof_encoding.
    Module V1.
      Parameter Tree32 : PROOF_ENCODING.

      Parameter Tree2 : PROOF_ENCODING.
    End V1.

    Module V2.
      Parameter Tree32 : PROOF_ENCODING.

      Parameter Tree2 : PROOF_ENCODING.
    End V2.
  End Proof_encoding.

  Parameter complete : t β†’ string β†’ list string.

  Parameter get_hash_version : t β†’ Context_hash.Version.t.

  Parameter set_hash_version :
    t β†’ Context_hash.Version.t β†’ Error_monad.shell_tzresult t.

  Parameter cache_key : Set.

  Definition cache_value := extensible_type.

  Module CACHE.
    Record signature {t size index identifier key value : Set} : Set := {
      
Type for context view. A context contains a cache. A cache is made of subcaches. Each subcache has its own size limit. The limit of its subcache is called a layout and can be initialized via the [set_cache_layout] function.
      t := t;
      
Size for subcaches and values of the cache. Units are not specified and left to the economic protocol.
      size := size;
      
Index type to index caches.
      index := index;
      
Identifier type for keys.
      identifier := identifier;
      
A key uniquely identifies a cached [value] in some subcache.
      key := key;
      
Cached values inhabit an extensible type.
      value := value;
      
[key_of_identifier ~cache_index identifier] builds a key from the [cache_index] and the [identifier].
No check are made to ensure the validity of the index.
      key_of_identifier : index β†’ identifier β†’ key;
      
[identifier_of_key key] returns the identifier associated to the [key].
      identifier_of_key : key β†’ identifier;
      
[pp fmt cache] is a pretty printer for a [cache].
      pp : Format.formatter β†’ t β†’ unit;
      
[find ctxt k = Some v] if [v] is the value associated to [k] in in the cache where [k] is. Returns [None] if there is no such value in the cache of [k]. This function is in the Lwt monad because if the value has not been constructed, it is constructed on the fly.
      find : t β†’ key β†’ option value;
      
[set_cache_layout ctxt layout] sets the caches of [ctxt] to comply with given [layout]. If there was already a cache in [ctxt], it is erased by the new layout.
Otherwise, a fresh collection of empty caches is reconstructed from the new [layout]. Notice that cache [key]s are invalidated in that case, i.e., [get t k] will return [None].
      set_cache_layout : t β†’ list size β†’ t;
      
[update ctxt k (Some (e, size))] returns a cache where the value [e] of [size] is associated to key [k]. If [k] is already in the cache, the cache entry is updated.
[update ctxt k None] removes [k] from the cache.
      update : t β†’ key β†’ option (value Γ— size) β†’ t;
      
[sync ctxt ~cache_nonce] updates the context with the domain of the cache computed so far. Such function is expected to be called at the end of the validation of a block, when there is no more accesses to the cache.
[cache_nonce] identifies the block that introduced new cache entries. The nonce should identify uniquely the block which modifies this value. It cannot be the block hash for circularity reasons: The value of the nonce is stored onto the context and consequently influences the context hash of the very same block. Such nonce cannot be determined by the shell and its computation is delegated to the economic protocol.
      sync : t β†’ Bytes.t β†’ t;
      
[clear ctxt] removes all cache entries.
      clear : t β†’ t;
      
[list_keys ctxt ~cache_index] returns the list of cached keys in cache numbered [cache_index] along with their respective [size]. The returned list is sorted in terms of their age in the cache, the oldest coming first. If [cache_index] is invalid, then this function returns [None].
      list_keys : t β†’ index β†’ option (list (key Γ— size));
      
[key_rank index ctxt key] returns the number of cached value older than the given [key]; or, [None] if the [key] is not a cache key.
      key_rank : t β†’ key β†’ option int;
      
[future_cache_expectation ctxt ~time_in_blocks] returns [ctxt] except that the entries of the caches that are presumably too old to still be in the caches in [n_blocks] are removed.
This function is based on a heuristic. The context maintains the median of the number of removed entries: this number is multiplied by `n_blocks` to determine the entries that are likely to be removed in `n_blocks`.
      future_cache_expectation : t β†’ int β†’ t;
      
[cache_size ctxt ~cache_index] returns an overapproximation of the size of the cache. Returns [None] if [cache_index] is not a valid cache index.
      cache_size : t β†’ index β†’ option size;
      
[cache_size_limit ctxt ~cache_index] returns the maximal size of the cache indexed by [cache_index]. Returns [None] if [cache_index] is not a valid cache index.
      cache_size_limit : t β†’ index β†’ option size;
    }.
  End CACHE.
  Definition CACHE := @CACHE.signature.
  Arguments CACHE {_ _ _ _ _ _}.

  Parameter Cache :
    CACHE (t := t) (size := int) (index := int) (identifier := string)
      (key := cache_key) (value := cache_value).
End Context_signature.
Require Export TezosOfOCaml.Environment.V7.Context.
Module Context_check : Context_signature := Context.

Module Type Updater_signature.
  Module validation_result.
    Record record : Set := Build {
      context : Context.t;
      fitness : Fitness.t;
      message : option string;
      max_operations_ttl : int;
      last_allowed_fork_level : Int32.t;
    }.
    Definition with_context context (r : record) :=
      Build context r.(fitness) r.(message) r.(max_operations_ttl)
        r.(last_allowed_fork_level).
    Definition with_fitness fitness (r : record) :=
      Build r.(context) fitness r.(message) r.(max_operations_ttl)
        r.(last_allowed_fork_level).
    Definition with_message message (r : record) :=
      Build r.(context) r.(fitness) message r.(max_operations_ttl)
        r.(last_allowed_fork_level).
    Definition with_max_operations_ttl max_operations_ttl (r : record) :=
      Build r.(context) r.(fitness) r.(message) max_operations_ttl
        r.(last_allowed_fork_level).
    Definition with_last_allowed_fork_level last_allowed_fork_level
      (r : record) :=
      Build r.(context) r.(fitness) r.(message) r.(max_operations_ttl)
        last_allowed_fork_level.
  End validation_result.
  Definition validation_result := validation_result.record.

  Module quota.
    Record record : Set := Build {
      max_size : int;
      max_op : option int;
    }.
    Definition with_max_size max_size (r : record) :=
      Build max_size r.(max_op).
    Definition with_max_op max_op (r : record) :=
      Build r.(max_size) max_op.
  End quota.
  Definition quota := quota.record.

  Module rpc_context.
    Record record : Set := Build {
      block_hash : Block_hash.t;
      block_header : Block_header.shell_header;
      context : Context.t;
    }.
    Definition with_block_hash block_hash (r : record) :=
      Build block_hash r.(block_header) r.(context).
    Definition with_block_header block_header (r : record) :=
      Build r.(block_hash) block_header r.(context).
    Definition with_context context (r : record) :=
      Build r.(block_hash) r.(block_header) context.
  End rpc_context.
  Definition rpc_context := rpc_context.record.

  Module PROTOCOL.
    Record signature
      {block_header_data block_header block_header_metadata operation_data
        operation_receipt operation mode validation_state application_state
        Mempool_t Mempool_validation_info Mempool_keep_or_replace
        Mempool_operation_conflict Mempool_add_result Mempool_add_error
        Mempool_merge_error : Set} : Set := {
      
The maximum size of a block header in bytes.
      max_block_length : int;
      
The maximum size of an {!operation} in bytes. This value is bigger than the size of the bytes required for {!operation_data}, because this value accounts for the shell header.
      max_operation_data_length : int;
      
Operations quota for each validation pass. The length of the list denotes the number of validation passes.
      validation_passes : list quota;
      
The economic protocol-specific type of blocks.
      block_header_data := block_header_data;
      
Encoding for economic protocol-specific part of block headers.
A fully parsed block header.
      block_header := block_header;
      
Economic protocol-specific side information computed by the protocol during the validation of a block. Should not include information about the evaluation of operations which is handled separately by {!operation_metadata}. To be used as an execution trace by tools (client, indexer). Not necessary for validation.
      block_header_metadata := block_header_metadata;
      
Encoding for economic protocol-specific block metadata.
The economic protocol-specific type of operations.
      operation_data := operation_data;
      
Economic protocol-specific side information computed by the protocol during the validation of each operation, to be used conjointly with {!block_header_metadata}.
      operation_receipt := operation_receipt;
      
A fully parsed operation.
      operation := operation;
      
Encoding for economoic protocol-specific operation data.
Encoding for eonomic protocol-specific operation receipts.
Encoding that mixes an operation data and its receipt.
      operation_data_and_receipt_encoding :
        Data_encoding.t (operation_data Γ— operation_receipt);
      
[acceptable_pass op] gives the validation pass in which the input operation [op] can appear. For instance, it results in [Some 0] if [op] only belongs to the first pass. When [op] is ill-formed, [acceptable_pass op] returns [None].
      acceptable_pass : operation β†’ option int;
      
[compare_operations (oph1,op1) (oph2,op2)] defines a total ordering relation on valid operations.
The following requirements must be satisfied: [oph1] is the [Operation.hash.p1], [oph2] is [Operation.hash op2] and that [op1] and [op2] are valid in the same context.
[compare_operations (oph1,op1) (oph2,op2) = 0] happens only if [Operation_hash.compare oph1 oph2 = 0], meaning [op1 = op2] only when [op1] and [op2] are structurally identical.
Two operations of different validation_passes are compared in the reverse order of their [validation_pass]: the one with the smaller [validation_pass] is compared as being the greater.
When belonging to the same validation_pass, two operations comparison depends on their static parameters. An abstract weight is computed for each operation based on its static parameters. When two operations' weights are compared as equal, [compare_operation (oph1,op1) (oph2,op2)] is [Operation_hash.compare oph1 oph2].
[compare_operations] can be used as a [compare] component of an {!Stdlib.Map.OrderedType}, or any such collection which relies on a total comparison function.
      compare_operations :
        Operation_hash.t Γ— operation β†’ Operation_hash.t Γ— operation β†’ int;
      
The mode indicates the circumstances in which a block and/or operations are validated or applied, and contains specific information. It must be provided as an argument to [begin_validation] and [begin_application].
      mode := mode;
      
A functional state that is transmitted throughout the validation of a block (or during the lifetime of a mempool or RPC). It is created by [begin_validation] below, updated by [validate_operation], and required by [finalize_validation]. This state is immutable thus validator or baker implementations are allowed to pause, replay or backtrack throughout validation steps.
      validation_state := validation_state;
      
Similar to {!validation_state}, but for the application process.
      application_state := application_state;
      
[begin_validation predecessor_context chain_id mode ~predecessor] initializes the {!validation_state} for the validation process of an existing or new block.
[predecessor_context] and [predecessor] are the resulting context and shell header of the predecessor block. Exceptionally in {!Partial_validation} mode, they may instead come from any ancestor block that is more recent (i.e. has a greater level) than the current head's "last_allowed_fork_level".
[mode] specifies the circumstances of validation and also carries additional information: see {!mode}.
Note that for protocol versions <= K where [begin_validation] does not exist yet, this calls the old [begin_application] by necessity. However, in [Application] mode, this calls the old [begin_application] in [Partial_validation] mode in order to run more quickly. This preserves the behavior of [precheck] in [lib_validation/block_validation.ml] for old protocols. It does mean that the application of a validated block may fail in these protocols.
      begin_validation :
        Context.t β†’ Chain_id.t β†’ mode β†’ Block_header.shell_header β†’
        Error_monad.tzresult validation_state;
      
Validate an operation. If successful, return the updated {!validation_state}.
[check_signature] indicates whether the signature should be checked. It defaults to [true] because the signature needs to be correct for the operation to be valid. This argument exists for special cases where it is acceptable to bypass this check, e.g. if we know that the operation has already been successfully validated in another context.
      validate_operation :
        option bool β†’ validation_state β†’ Operation_hash.t β†’ operation β†’
        Error_monad.tzresult validation_state;
      
Run final and global checks on the block that must come after the validation of all its operations to establish its validity.
      finalize_validation : validation_state β†’ Error_monad.tzresult unit;
      
Initialize the {!application_state} for the application process of an existing or new block. See {!begin_validation} for details on the arguments.
In protocol versions > K, calling this function with the {!Partial_validation} mode returns an error.
      begin_application :
        Context.t β†’ Chain_id.t β†’ mode β†’ Block_header.shell_header β†’
        Error_monad.tzresult application_state;
      
Apply an operation. If successful, return the updated {!application_state} and the corresponding {!operation_receipt}.
This should be called for all operations in a block, after {!begin_application} and before {!finalize_application}. Moreover, the operation should have already been validated by {!validate_operation}.
      apply_operation :
        application_state β†’ Operation_hash.t β†’ operation β†’
        Error_monad.tzresult (application_state Γ— operation_receipt);
      
Finalize the context resulting from the application of the contents of the block.
If there is no protocol migration, i.e. if the block being applied is not the last block of the current economic protocol, then the resulting context can be used in the future as input for the validation and application of its successor blocks.
In {!Construction} mode, the [Block_header.shell_header option] argument must contain a value, which will be used to compute the [cache_nonce]. In other modes, it can as well be [None] since it will not be used.
      finalize_application :
        application_state β†’ option Block_header.shell_header β†’
        Error_monad.tzresult (validation_result Γ— block_header_metadata);
      
[rpc_services] provides the list of remote procedures exported by this protocol implementation.
      rpc_services : RPC_directory.t rpc_context;
      
[init chain_id ctxt hd] initializes the context, or upgrades the context after a protocol amendment. This function receives as arguments the [chain_id] of the current chain and the context [ctxt] resulting from the application of the block that triggered the amendment, as well as its header [hd]. This function should fail if the "protocol stitching", i.e., the transition from a valid previous protocol to the one being activated, has not been implemented.
      init_value :
        Chain_id.t β†’ Context.t β†’ Block_header.shell_header β†’
        Error_monad.tzresult validation_result;
      
[value_of_key chain_id predecessor_context predecessor_timestamp predecessor_level predecessor_fitness predecessor timestamp] returns a function to build one value of the cache from its key.
This function is used to restore all or part of the cache, for instance when booting a validator to preheat the cache, or when a reorganization happens. This function should never fail, returned errors are fatal.
The generated function is passed to [Context.Cache.load_caches] which will use it either immediately a cache-loading time or on-demand, when a given cached value is accessed.
      value_of_key :
        Chain_id.t β†’ Context.t β†’ Time.t β†’ Int32.t β†’ Fitness.t β†’
        Block_hash.t β†’ Time.t β†’
        Error_monad.tzresult
          (Context.cache_key β†’ Error_monad.tzresult Context.cache_value);
      
Mempool type. This immutable functional state keeps track of operations added to the mempool, and allows to detect conflicts between them and a new candidate operation.
      Mempool_t := Mempool_t;
      
Validation info type required to validate and add operations to a mempool.
Type of the function that may be provided in order to resolve a potential conflict when adding an operation to an existing mempool or when merging two mempools. This handler may be defined as a simple order relation over operations (e.g. prioritize the most profitable operations) or an arbitrary one (e.g. prioritize operations where the source is a specific manager).
Returning [`Keep] will leave the mempool unchanged and retain the [existing_operation] while returning [`Replace] will remove [existing_operation] and add [new_operation] instead.
      Mempool_conflict_handler :=
        Operation_hash.t Γ— operation β†’ Operation_hash.t Γ— operation β†’
        Mempool_keep_or_replace;
      Mempool_operation_conflict := Mempool_operation_conflict;
      
Return type when adding an operation to the mempool
      Mempool_add_result := Mempool_add_result;
      
Error type returned when adding an operation to the mempool fails.
      Mempool_add_error := Mempool_add_error;
      
Error type returned when the merge of two mempools fails.
      Mempool_merge_error := Mempool_merge_error;
      
Initialize a static [validation_info] and [mempool], required to validate and add operations, and an incremental and serializable {!mempool}.
      Mempool_init :
        Context.t β†’ Chain_id.t β†’ Block_hash.t β†’ Block_header.shell_header β†’
        Error_monad.tzresult (Mempool_validation_info Γ— Mempool_t);
      
Mempool encoding
      Mempool_encoding : Data_encoding.t Mempool_t;
      
Adds an operation to a [mempool] if and only if it is valid and does not conflict with previously added operation.
This function checks the validity of an operation and tries to add it to the mempool.
If a validation error is triggered, the result will be a [Validation_error]. If a conflict with a previous operation exists, the result will be [Add_conflict] is then checked. Important: no [Add_conflict] will be raised if a [conflict_handler] is provided (see [add_result]).
If no error is raised the operation is potentially added to the [mempool] depending on the [add_result] value.
      Mempool_add_operation :
        option bool β†’ option Mempool_conflict_handler β†’
        Mempool_validation_info β†’ Mempool_t β†’ Operation_hash.t Γ— operation β†’
        Pervasives.result (Mempool_t Γ— Mempool_add_result) Mempool_add_error;
      
[remove_operation mempool oph] removes the operation [oph] from the [mempool]. The [mempool] remains unchanged when [oph] is not present in the [mempool]
      Mempool_remove_operation : Mempool_t β†’ Operation_hash.t β†’ Mempool_t;
      
[merge ?conflict_handler mempool mempool'] merges [mempool'] {b into} [mempool].
Mempools may only be merged if they are compatible: i.e. both have been initialised with the same predecessor block. Otherwise, the [Incompatible_mempool] error is returned.
Conflicts between operations from the two mempools can occur. Similarly as [add_operation], a [Merge_conflict] error may be raised when no [conflict_handler] is provided.
[existing_operation] in [conflict_handler ~existing_operation ~new_operation] references operations present in [mempool] while [new_operation] will reference operations present in [mempool'].
      Mempool_merge :
        option Mempool_conflict_handler β†’ Mempool_t β†’ Mempool_t β†’
        Pervasives.result Mempool_t Mempool_merge_error;
      
[operations mempool] returns the map of operations present in [mempool].
      Mempool_operations :
        Mempool_t β†’ Operation_hash.Map.(S.INDEXES_MAP.t) operation;
    }.
  End PROTOCOL.
  Definition PROTOCOL := @PROTOCOL.signature.
  Arguments PROTOCOL {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _}.

  Parameter activate : Context.t β†’ Protocol_hash.t β†’ Context.t.
End Updater_signature.
Require Export TezosOfOCaml.Environment.V7.Updater.
Module Updater_check : Updater_signature := Updater.

Module Type RPC_context_signature.
  Definition t : Set := Updater.rpc_context.

  Module simple.
    Record record {pr : Set} : Set := Build {
      call_proto_service0 :
        βˆ€ {q i o : Set},
        RPC_service.t t t q i o β†’ pr β†’ q β†’ i β†’ Error_monad.shell_tzresult o;
      call_proto_service1 :
        βˆ€ {a q i o : Set},
        RPC_service.t t (t Γ— a) q i o β†’ pr β†’ a β†’ q β†’ i β†’
        Error_monad.shell_tzresult o;
      call_proto_service2 :
        βˆ€ {a b q i o : Set},
        RPC_service.t t ((t Γ— a) Γ— b) q i o β†’ pr β†’ a β†’ b β†’ q β†’ i β†’
        Error_monad.shell_tzresult o;
      call_proto_service3 :
        βˆ€ {a b c q i o : Set},
        RPC_service.t t (((t Γ— a) Γ— b) Γ— c) q i o β†’ pr β†’ a β†’ b β†’ c β†’ q β†’
        i β†’ Error_monad.shell_tzresult o;
    }.
    Arguments record : clear implicits.
  End simple.
  Definition simple := simple.record.

  Parameter make_call0 : βˆ€ {i o pr q : Set},
    RPC_service.t t t q i o β†’ simple pr β†’ pr β†’ q β†’ i β†’
    Error_monad.shell_tzresult o.

  Parameter make_call1 : βˆ€ {a i o pr q : Set},
    RPC_service.t t (t Γ— a) q i o β†’ simple pr β†’ pr β†’ a β†’ q β†’ i β†’
    Error_monad.shell_tzresult o.

  Parameter make_call2 : βˆ€ {a b i o pr q : Set},
    RPC_service.t t ((t Γ— a) Γ— b) q i o β†’ simple pr β†’ pr β†’ a β†’ b β†’ q β†’
    i β†’ Error_monad.shell_tzresult o.

  Parameter make_call3 : βˆ€ {a b c i o pr q : Set},
    RPC_service.t t (((t Γ— a) Γ— b) Γ— c) q i o β†’ simple pr β†’ pr β†’ a β†’ b β†’
    c β†’ q β†’ i β†’ Error_monad.shell_tzresult o.

  Parameter make_opt_call0 : βˆ€ {i o pr q : Set},
    RPC_service.t t t q i o β†’ simple pr β†’ pr β†’ q β†’ i β†’
    Error_monad.shell_tzresult (option o).

  Parameter make_opt_call1 : βˆ€ {a i o pr q : Set},
    RPC_service.t t (t Γ— a) q i o β†’ simple pr β†’ pr β†’ a β†’ q β†’ i β†’
    Error_monad.shell_tzresult (option o).

  Parameter make_opt_call2 : βˆ€ {a b i o pr q : Set},
    RPC_service.t t ((t Γ— a) Γ— b) q i o β†’ simple pr β†’ pr β†’ a β†’ b β†’ q β†’
    i β†’ Error_monad.shell_tzresult (option o).

  Parameter make_opt_call3 : βˆ€ {a b c i o pr q : Set},
    RPC_service.t t (((t Γ— a) Γ— b) Γ— c) q i o β†’ simple pr β†’ pr β†’ a β†’ b β†’
    c β†’ q β†’ i β†’ Error_monad.shell_tzresult (option o).
End RPC_context_signature.
Require Export TezosOfOCaml.Environment.V7.RPC_context.
Module RPC_context_check : RPC_context_signature := RPC_context.

Module Type Wasm_2_0_0_signature.
  Module input.
    Record record : Set := Build {
      inbox_level : Bounded.Non_negative_int32.(Bounded.S.t);
      message_counter : Z.t;
    }.
    Definition with_inbox_level inbox_level (r : record) :=
      Build inbox_level r.(message_counter).
    Definition with_message_counter message_counter (r : record) :=
      Build r.(inbox_level) message_counter.
  End input.
  Definition input := input.record.

  Module output.
    Record record : Set := Build {
      outbox_level : Bounded.Non_negative_int32.(Bounded.S.t);
      message_index : Z.t;
    }.
    Definition with_outbox_level outbox_level (r : record) :=
      Build outbox_level r.(message_index).
    Definition with_message_index message_index (r : record) :=
      Build r.(outbox_level) message_index.
  End output.
  Definition output := output.record.

  Inductive input_request : Set :=
  | No_input_required : input_request
  | Input_required : input_request.

  Module info.
    Record record : Set := Build {
      current_tick : Z.t;
      last_input_read : option input;
      input_request : input_request;
    }.
    Definition with_current_tick current_tick (r : record) :=
      Build current_tick r.(last_input_read) r.(input_request).
    Definition with_last_input_read last_input_read (r : record) :=
      Build r.(current_tick) last_input_read r.(input_request).
    Definition with_input_request input_request (r : record) :=
      Build r.(current_tick) r.(last_input_read) input_request.
  End info.
  Definition info := info.record.

  Module S.
    Record signature {tree : Set} : Set := {
      tree := tree;
      compute_step : tree β†’ tree;
      set_input_step : input β†’ string β†’ tree β†’ tree;
      get_output : output β†’ tree β†’ string;
      get_info : tree β†’ info;
    }.
  End S.
  Definition S := @S.signature.
  Arguments S {_}.

  Parameter Make :
    βˆ€ {Tree_t Tree_tree : Set},
    βˆ€ (Tree :
      Context.TREE (t := Tree_t) (tree := Tree_tree) (key := list string)
        (value := bytes)), S (tree := Tree.(Context.TREE.tree)).
End Wasm_2_0_0_signature.
Require Export TezosOfOCaml.Environment.V7.Wasm_2_0_0.
Module Wasm_2_0_0_check : Wasm_2_0_0_signature := Wasm_2_0_0.

Module Type Plonk_signature.
  Definition scalar : Set := Bls.Primitive.Fr.(S.PRIME_FIELD.t).

  Parameter public_parameters : Set.

  Parameter proof : Set.

  Parameter public_parameters_encoding : Data_encoding.t public_parameters.

  Parameter proof_encoding : Data_encoding.t proof.

  Parameter scalar_encoding : Data_encoding.t scalar.

  Parameter scalar_array_encoding : Data_encoding.t (array scalar).

  Parameter verify : public_parameters β†’ array scalar β†’ proof β†’ bool.

  Parameter verify_multi_circuits :
    public_parameters β†’ list (string Γ— list (array scalar)) β†’ proof β†’ bool.
End Plonk_signature.
Require Export TezosOfOCaml.Environment.V7.Plonk.
Module Plonk_check : Plonk_signature := Plonk.

Module Type Dal_signature.
  Parameter t : Set.

  Module parameters.
    Record record : Set := Build {
      redundancy_factor : int;
      page_size : int;
      slot_size : int;
      number_of_shards : int;
    }.
    Definition with_redundancy_factor redundancy_factor (r : record) :=
      Build redundancy_factor r.(page_size) r.(slot_size) r.(number_of_shards).
    Definition with_page_size page_size (r : record) :=
      Build r.(redundancy_factor) page_size r.(slot_size) r.(number_of_shards).
    Definition with_slot_size slot_size (r : record) :=
      Build r.(redundancy_factor) r.(page_size) slot_size r.(number_of_shards).
    Definition with_number_of_shards number_of_shards (r : record) :=
      Build r.(redundancy_factor) r.(page_size) r.(slot_size) number_of_shards.
  End parameters.
  Definition parameters := parameters.record.

  Parameter make : parameters β†’ Pervasives.result t Variant.t.

  Parameter commitment : Set.

  Module Commitment.
    Parameter encoding : Data_encoding.t commitment.

    Parameter to_b58check : commitment β†’ string.

    Parameter of_b58check_opt : string β†’ option commitment.

    Parameter zero : commitment.

    Parameter equal : commitment β†’ commitment β†’ bool.

    Parameter pp : Format.formatter β†’ commitment β†’ unit.
  End Commitment.

  Parameter commitment_proof : Set.

  Parameter commitment_proof_encoding : Data_encoding.t commitment_proof.

  Parameter verify_commitment : t β†’ commitment β†’ commitment_proof β†’ bool.

  Module page.
    Record record : Set := Build {
      index : int;
      content : bytes;
    }.
    Definition with_index index (r : record) :=
      Build index r.(content).
    Definition with_content content (r : record) :=
      Build r.(index) content.
  End page.
  Definition page := page.record.

  Parameter page_proof : Set.

  Parameter page_proof_encoding : Data_encoding.t page_proof.

  Parameter verify_page :
    t β†’ commitment β†’ page β†’ page_proof β†’ Result.t bool Variant.t.
End Dal_signature.
Require Export TezosOfOCaml.Environment.V7.Dal.
Module Dal_check : Dal_signature := Dal.