🕶️ Blinded_public_key_hash.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Path_encoding.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "Blinded public key hash" in
let title := "A blinded public key hash" in
let b58check_prefix :=
String.String "001" (String.String "002" ("1" ++ String.String "223" ""))
in
let size_value :=
Some Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.size_value) in
{|
Blake2B.PrefixedName.name := name;
Blake2B.PrefixedName.title := title;
Blake2B.PrefixedName.size_value := size_value;
Blake2B.PrefixedName.b58check_prefix := b58check_prefix
|}).
Module Index.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Path_encoding.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "Blinded public key hash" in
let title := "A blinded public key hash" in
let b58check_prefix :=
String.String "001" (String.String "002" ("1" ++ String.String "223" ""))
in
let size_value :=
Some Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.size_value) in
{|
Blake2B.PrefixedName.name := name;
Blake2B.PrefixedName.title := title;
Blake2B.PrefixedName.size_value := size_value;
Blake2B.PrefixedName.b58check_prefix := b58check_prefix
|}).
Module Index.
Inclusion of the module [H]
Definition t := H.(S.HASH.t).
Definition name := H.(S.HASH.name).
Definition title := H.(S.HASH.title).
Definition pp := H.(S.HASH.pp).
Definition pp_short := H.(S.HASH.pp_short).
Definition op_eq := H.(S.HASH.op_eq).
Definition op_ltgt := H.(S.HASH.op_ltgt).
Definition op_lt := H.(S.HASH.op_lt).
Definition op_lteq := H.(S.HASH.op_lteq).
Definition op_gteq := H.(S.HASH.op_gteq).
Definition op_gt := H.(S.HASH.op_gt).
Definition compare := H.(S.HASH.compare).
Definition equal := H.(S.HASH.equal).
Definition max := H.(S.HASH.max).
Definition min := H.(S.HASH.min).
Definition hash_bytes := H.(S.HASH.hash_bytes).
Definition hash_string := H.(S.HASH.hash_string).
Definition zero := H.(S.HASH.zero).
Definition size_value := H.(S.HASH.size_value).
Definition to_bytes := H.(S.HASH.to_bytes).
Definition of_bytes_opt := H.(S.HASH.of_bytes_opt).
Definition of_bytes_exn := H.(S.HASH.of_bytes_exn).
Definition to_b58check := H.(S.HASH.to_b58check).
Definition to_short_b58check := H.(S.HASH.to_short_b58check).
Definition of_b58check_exn := H.(S.HASH.of_b58check_exn).
Definition of_b58check_opt := H.(S.HASH.of_b58check_opt).
Definition b58check_encoding := H.(S.HASH.b58check_encoding).
Definition encoding := H.(S.HASH.encoding).
Definition rpc_arg := H.(S.HASH.rpc_arg).
Definition Map := H.(S.HASH.Map).
Definition Path_encoding_Make_hex_include :=
Path_encoding.Make_hex
{|
Path_encoding.ENCODING.to_bytes := H.(S.HASH.to_bytes);
Path_encoding.ENCODING.of_bytes_opt := H.(S.HASH.of_bytes_opt)
|}.
Definition name := H.(S.HASH.name).
Definition title := H.(S.HASH.title).
Definition pp := H.(S.HASH.pp).
Definition pp_short := H.(S.HASH.pp_short).
Definition op_eq := H.(S.HASH.op_eq).
Definition op_ltgt := H.(S.HASH.op_ltgt).
Definition op_lt := H.(S.HASH.op_lt).
Definition op_lteq := H.(S.HASH.op_lteq).
Definition op_gteq := H.(S.HASH.op_gteq).
Definition op_gt := H.(S.HASH.op_gt).
Definition compare := H.(S.HASH.compare).
Definition equal := H.(S.HASH.equal).
Definition max := H.(S.HASH.max).
Definition min := H.(S.HASH.min).
Definition hash_bytes := H.(S.HASH.hash_bytes).
Definition hash_string := H.(S.HASH.hash_string).
Definition zero := H.(S.HASH.zero).
Definition size_value := H.(S.HASH.size_value).
Definition to_bytes := H.(S.HASH.to_bytes).
Definition of_bytes_opt := H.(S.HASH.of_bytes_opt).
Definition of_bytes_exn := H.(S.HASH.of_bytes_exn).
Definition to_b58check := H.(S.HASH.to_b58check).
Definition to_short_b58check := H.(S.HASH.to_short_b58check).
Definition of_b58check_exn := H.(S.HASH.of_b58check_exn).
Definition of_b58check_opt := H.(S.HASH.of_b58check_opt).
Definition b58check_encoding := H.(S.HASH.b58check_encoding).
Definition encoding := H.(S.HASH.encoding).
Definition rpc_arg := H.(S.HASH.rpc_arg).
Definition Map := H.(S.HASH.Map).
Definition Path_encoding_Make_hex_include :=
Path_encoding.Make_hex
{|
Path_encoding.ENCODING.to_bytes := H.(S.HASH.to_bytes);
Path_encoding.ENCODING.of_bytes_opt := H.(S.HASH.of_bytes_opt)
|}.
Inclusion of the module [Path_encoding_Make_hex_include]
Definition to_path :=
Path_encoding_Make_hex_include.(Path_encoding.S.to_path).
Definition of_path :=
Path_encoding_Make_hex_include.(Path_encoding.S.of_path).
Definition path_length :=
Path_encoding_Make_hex_include.(Path_encoding.S.path_length).
(* Index *)
Definition module :=
{|
Storage_description.INDEX.to_path := to_path;
Storage_description.INDEX.of_path := of_path;
Storage_description.INDEX.path_length := path_length;
Storage_description.INDEX.rpc_arg := rpc_arg;
Storage_description.INDEX.encoding := encoding;
Storage_description.INDEX.compare := compare
|}.
End Index.
Definition Index : Storage_description.INDEX (t := H.(S.HASH.t)) :=
Index.module.
Path_encoding_Make_hex_include.(Path_encoding.S.to_path).
Definition of_path :=
Path_encoding_Make_hex_include.(Path_encoding.S.of_path).
Definition path_length :=
Path_encoding_Make_hex_include.(Path_encoding.S.path_length).
(* Index *)
Definition module :=
{|
Storage_description.INDEX.to_path := to_path;
Storage_description.INDEX.of_path := of_path;
Storage_description.INDEX.path_length := path_length;
Storage_description.INDEX.rpc_arg := rpc_arg;
Storage_description.INDEX.encoding := encoding;
Storage_description.INDEX.compare := compare
|}.
End Index.
Definition Index : Storage_description.INDEX (t := H.(S.HASH.t)) :=
Index.module.
Inclusion of the module [H]
Definition t := H.(S.HASH.t).
Definition name := H.(S.HASH.name).
Definition title := H.(S.HASH.title).
Definition pp := H.(S.HASH.pp).
Definition pp_short := H.(S.HASH.pp_short).
Definition op_eq := H.(S.HASH.op_eq).
Definition op_ltgt := H.(S.HASH.op_ltgt).
Definition op_lt := H.(S.HASH.op_lt).
Definition op_lteq := H.(S.HASH.op_lteq).
Definition op_gteq := H.(S.HASH.op_gteq).
Definition op_gt := H.(S.HASH.op_gt).
Definition compare := H.(S.HASH.compare).
Definition equal := H.(S.HASH.equal).
Definition max := H.(S.HASH.max).
Definition min := H.(S.HASH.min).
Definition hash_bytes := H.(S.HASH.hash_bytes).
Definition hash_string := H.(S.HASH.hash_string).
Definition zero := H.(S.HASH.zero).
Definition size_value := H.(S.HASH.size_value).
Definition to_bytes := H.(S.HASH.to_bytes).
Definition of_bytes_opt := H.(S.HASH.of_bytes_opt).
Definition of_bytes_exn := H.(S.HASH.of_bytes_exn).
Definition to_b58check := H.(S.HASH.to_b58check).
Definition to_short_b58check := H.(S.HASH.to_short_b58check).
Definition of_b58check_exn := H.(S.HASH.of_b58check_exn).
Definition of_b58check_opt := H.(S.HASH.of_b58check_opt).
Definition b58check_encoding := H.(S.HASH.b58check_encoding).
Definition encoding := H.(S.HASH.encoding).
Definition rpc_arg := H.(S.HASH.rpc_arg).
Definition Map := H.(S.HASH.Map).
Definition name := H.(S.HASH.name).
Definition title := H.(S.HASH.title).
Definition pp := H.(S.HASH.pp).
Definition pp_short := H.(S.HASH.pp_short).
Definition op_eq := H.(S.HASH.op_eq).
Definition op_ltgt := H.(S.HASH.op_ltgt).
Definition op_lt := H.(S.HASH.op_lt).
Definition op_lteq := H.(S.HASH.op_lteq).
Definition op_gteq := H.(S.HASH.op_gteq).
Definition op_gt := H.(S.HASH.op_gt).
Definition compare := H.(S.HASH.compare).
Definition equal := H.(S.HASH.equal).
Definition max := H.(S.HASH.max).
Definition min := H.(S.HASH.min).
Definition hash_bytes := H.(S.HASH.hash_bytes).
Definition hash_string := H.(S.HASH.hash_string).
Definition zero := H.(S.HASH.zero).
Definition size_value := H.(S.HASH.size_value).
Definition to_bytes := H.(S.HASH.to_bytes).
Definition of_bytes_opt := H.(S.HASH.of_bytes_opt).
Definition of_bytes_exn := H.(S.HASH.of_bytes_exn).
Definition to_b58check := H.(S.HASH.to_b58check).
Definition to_short_b58check := H.(S.HASH.to_short_b58check).
Definition of_b58check_exn := H.(S.HASH.of_b58check_exn).
Definition of_b58check_opt := H.(S.HASH.of_b58check_opt).
Definition b58check_encoding := H.(S.HASH.b58check_encoding).
Definition encoding := H.(S.HASH.encoding).
Definition rpc_arg := H.(S.HASH.rpc_arg).
Definition Map := H.(S.HASH.Map).
Init function; without side-effects in Coq
Definition init_module : unit :=
Base58.check_encoded_prefix b58check_encoding "btz1" 37.
Definition of_ed25519_pkh
(activation_code : bytes)
(pkh : Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t)) : t :=
hash_bytes (Some activation_code)
[ Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.to_bytes) pkh ].
Definition activation_code : Set := bytes.
Definition activation_code_size : int :=
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.size_value).
Definition activation_code_encoding : Data_encoding.encoding Bytes.t :=
Data_encoding.Fixed.bytes_value activation_code_size.
Definition activation_code_of_hex (h_value : string) : option bytes :=
if (String.length h_value) ≠i (activation_code_size ×i 2) then
None
else
Hex.to_bytes (Hex.Hex h_value).
Base58.check_encoded_prefix b58check_encoding "btz1" 37.
Definition of_ed25519_pkh
(activation_code : bytes)
(pkh : Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t)) : t :=
hash_bytes (Some activation_code)
[ Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.to_bytes) pkh ].
Definition activation_code : Set := bytes.
Definition activation_code_size : int :=
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.size_value).
Definition activation_code_encoding : Data_encoding.encoding Bytes.t :=
Data_encoding.Fixed.bytes_value activation_code_size.
Definition activation_code_of_hex (h_value : string) : option bytes :=
if (String.length h_value) ≠i (activation_code_size ×i 2) then
None
else
Hex.to_bytes (Hex.Hex h_value).