Skip to main content

🍃 S.v

Environment

See proofs, Gitlab , OCaml

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

Require Proto_alpha.Environment.Base58.
Require Proto_alpha.Environment.Bytes.
Require Proto_alpha.Environment.Data_encoding.
Require Proto_alpha.Environment.Error_monad.
Require Proto_alpha.Environment.Format.
Require Proto_alpha.Environment.Pervasives.
Require Proto_alpha.Environment.RPC_arg.
Require Proto_alpha.Environment.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 :
       {_error a : Set},
      (key a Pervasives.result unit (list _error)) t a
      Pervasives.result unit (list _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 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 {_ _ _ _ _ _}.