Skip to main content

πŸƒΒ S.v

Environment

Gitlab

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require TezosOfOCaml.Environment.Structs.V0.Base58.
Require TezosOfOCaml.Environment.Structs.V0.Bytes.
Require TezosOfOCaml.Environment.Structs.V0.Data_encoding.
Require TezosOfOCaml.Environment.Structs.V0.Error_monad.
Require TezosOfOCaml.Environment.Structs.V0.Format.
Require TezosOfOCaml.Environment.Structs.V0.Pervasives.
Require TezosOfOCaml.Environment.Structs.V0.RPC_arg.
Require TezosOfOCaml.Environment.Structs.V0.Seq.
Import Error_monad.Notations.

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 :
      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;
    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;
  }.
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;
    size_in_memory : int;
    of_z : Z.t β†’ t;
    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 := {
    t := t;
    size_in_memory : int;
    size_in_bytes : int;
    Scalar : FIELD (t := Scalar_t);
    check_bytes : Bytes.t β†’ bool;
    of_bytes_opt : Bytes.t β†’ option t;
    to_bytes : t β†’ Bytes.t;
    zero : t;
    one : t;
    add : t β†’ t β†’ t;
    double : t β†’ t;
    negate : t β†’ t;
    eq_value : t β†’ t β†’ bool;
    mul : t β†’ Scalar.(FIELD.t) β†’ t;
  }.
End CURVE.
Definition CURVE := @CURVE.signature.
Arguments CURVE {_ _}.

Module PVSS_ELEMENT.
  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;
    (* extensible_type_definition `Base58.data` *)
    b58check_encoding : Base58.encoding t;
    encoding : Data_encoding.t t;
    rpc_arg : RPC_arg.t t;
  }.
End PVSS_ELEMENT.
Definition PVSS_ELEMENT := @PVSS_ELEMENT.signature.
Arguments PVSS_ELEMENT {_}.

Module PVSS_PUBLIC_KEY.
  Record signature {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;
    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;
  }.
End PVSS_PUBLIC_KEY.
Definition PVSS_PUBLIC_KEY := @PVSS_PUBLIC_KEY.signature.
Arguments PVSS_PUBLIC_KEY {_}.

Module PVSS_SECRET_KEY.
  Record signature {public_key t : Set} : Set := {
    public_key := public_key;
    t := t;
    encoding : Data_encoding.t t;
    rpc_arg : RPC_arg.t t;
    to_public_key : t β†’ public_key;
  }.
End PVSS_SECRET_KEY.
Definition PVSS_SECRET_KEY := @PVSS_SECRET_KEY.signature.
Arguments PVSS_SECRET_KEY {_ _}.

Module PVSS.
  Record signature
    {proof Clear_share_t Commitment_t Encrypted_share_t Public_key_t
      Secret_key_t : Set} : Set := {
    proof := proof;
    Clear_share : PVSS_ELEMENT (t := Clear_share_t);
    Commitment : PVSS_ELEMENT (t := Commitment_t);
    Encrypted_share : PVSS_ELEMENT (t := Encrypted_share_t);
    Public_key : PVSS_PUBLIC_KEY (t := Public_key_t);
    Secret_key :
      PVSS_SECRET_KEY (public_key := Public_key.(PVSS_PUBLIC_KEY.t))
        (t := Secret_key_t);
    proof_encoding : Data_encoding.t proof;
    check_dealer_proof :
      list Encrypted_share.(PVSS_ELEMENT.t) β†’
      list Commitment.(PVSS_ELEMENT.t) β†’ proof β†’
      list Public_key.(PVSS_PUBLIC_KEY.t) β†’ bool;
    check_revealed_share :
      Encrypted_share.(PVSS_ELEMENT.t) β†’ Clear_share.(PVSS_ELEMENT.t) β†’
      Public_key.(PVSS_PUBLIC_KEY.t) β†’ proof β†’ bool;
    reconstruct :
      list Clear_share.(PVSS_ELEMENT.t) β†’ list int β†’
      Public_key.(PVSS_PUBLIC_KEY.t);
  }.
End PVSS.
Definition PVSS := @PVSS.signature.
Arguments PVSS {_ _ _ _ _ _}.