🐆 Tx_rollup_message_result_hash_repr.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.Tx_rollup_message_result_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_prefixes.
Definition message_result_hash : string :=
Tx_rollup_prefixes.message_result_hash.(Tx_rollup_prefixes.t.b58check_prefix).
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "Message_result_hash" in
let title := "A message result hash" in
let b58check_prefix := message_result_hash in
let size_value :=
Some
Tx_rollup_prefixes.message_result_hash.(Tx_rollup_prefixes.t.hash_size)
in
{|
Blake2B.PrefixedName.name := name;
Blake2B.PrefixedName.title := title;
Blake2B.PrefixedName.size_value := size_value;
Blake2B.PrefixedName.b58check_prefix := b58check_prefix
|}).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Path_encoding.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_result_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_prefixes.
Definition message_result_hash : string :=
Tx_rollup_prefixes.message_result_hash.(Tx_rollup_prefixes.t.b58check_prefix).
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "Message_result_hash" in
let title := "A message result hash" in
let b58check_prefix := message_result_hash in
let size_value :=
Some
Tx_rollup_prefixes.message_result_hash.(Tx_rollup_prefixes.t.hash_size)
in
{|
Blake2B.PrefixedName.name := name;
Blake2B.PrefixedName.title := title;
Blake2B.PrefixedName.size_value := size_value;
Blake2B.PrefixedName.b58check_prefix := b58check_prefix
|}).
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 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 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).
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).
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
Tx_rollup_prefixes.check_encoding Tx_rollup_prefixes.message_result_hash
b58check_encoding.
Definition hash_uncarbonated (result_value : Tx_rollup_message_result_repr.t)
: H.(S.HASH.t) :=
let bytes_value :=
Data_encoding.Binary.to_bytes_exn None
Tx_rollup_message_result_repr.encoding result_value in
H.(S.HASH.hash_bytes) None [ bytes_value ].
Definition init_value : H.(S.HASH.t) :=
hash_uncarbonated Tx_rollup_message_result_repr.init_value.
Tx_rollup_prefixes.check_encoding Tx_rollup_prefixes.message_result_hash
b58check_encoding.
Definition hash_uncarbonated (result_value : Tx_rollup_message_result_repr.t)
: H.(S.HASH.t) :=
let bytes_value :=
Data_encoding.Binary.to_bytes_exn None
Tx_rollup_message_result_repr.encoding result_value in
H.(S.HASH.hash_bytes) None [ bytes_value ].
Definition init_value : H.(S.HASH.t) :=
hash_uncarbonated Tx_rollup_message_result_repr.init_value.