🍃 S.v
Environment
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 {_ _ _ _ _ _}.
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 {_ _ _ _ _ _}.