🐆 Tx_rollup_l2_address.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Indexable.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_prefixes.
Definition Blake2B_Make_include :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "Tx_rollup_l2_address" in
let title :=
"The hash of a BLS public key used to identify a L2 ticket holders" in
let b58check_prefix :=
Tx_rollup_prefixes.l2_address.(Tx_rollup_prefixes.t.b58check_prefix) in
let size_value :=
Some Tx_rollup_prefixes.l2_address.(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.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Indexable.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_prefixes.
Definition Blake2B_Make_include :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "Tx_rollup_l2_address" in
let title :=
"The hash of a BLS public key used to identify a L2 ticket holders" in
let b58check_prefix :=
Tx_rollup_prefixes.l2_address.(Tx_rollup_prefixes.t.b58check_prefix) in
let size_value :=
Some Tx_rollup_prefixes.l2_address.(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 [Blake2B_Make_include]
Definition t := Blake2B_Make_include.(S.HASH.t).
Definition name := Blake2B_Make_include.(S.HASH.name).
Definition title := Blake2B_Make_include.(S.HASH.title).
Definition pp := Blake2B_Make_include.(S.HASH.pp).
Definition pp_short := Blake2B_Make_include.(S.HASH.pp_short).
(* Definition op_eq := Blake2B_Make_include.(S.HASH.op_eq).
Definition op_ltgt := Blake2B_Make_include.(S.HASH.op_ltgt).
Definition op_lt := Blake2B_Make_include.(S.HASH.op_lt).
Definition op_lteq := Blake2B_Make_include.(S.HASH.op_lteq).
Definition op_gteq := Blake2B_Make_include.(S.HASH.op_gteq).
Definition op_gt := Blake2B_Make_include.(S.HASH.op_gt).
Definition compare := Blake2B_Make_include.(S.HASH.compare).
Definition equal := Blake2B_Make_include.(S.HASH.equal).
Definition max := Blake2B_Make_include.(S.HASH.max).
Definition min := Blake2B_Make_include.(S.HASH.min). *)
Definition hash_bytes := Blake2B_Make_include.(S.HASH.hash_bytes).
Definition hash_string := Blake2B_Make_include.(S.HASH.hash_string).
Definition zero := Blake2B_Make_include.(S.HASH.zero).
(* Definition size_value := Blake2B_Make_include.(S.HASH.size_value). *)
Definition to_bytes := Blake2B_Make_include.(S.HASH.to_bytes).
Definition of_bytes_opt := Blake2B_Make_include.(S.HASH.of_bytes_opt).
Definition of_bytes_exn := Blake2B_Make_include.(S.HASH.of_bytes_exn).
Definition to_b58check := Blake2B_Make_include.(S.HASH.to_b58check).
Definition to_short_b58check := Blake2B_Make_include.(S.HASH.to_short_b58check).
Definition of_b58check_exn := Blake2B_Make_include.(S.HASH.of_b58check_exn).
Definition of_b58check_opt := Blake2B_Make_include.(S.HASH.of_b58check_opt).
Definition b58check_encoding := Blake2B_Make_include.(S.HASH.b58check_encoding).
Definition encoding := Blake2B_Make_include.(S.HASH.encoding).
Definition rpc_arg := Blake2B_Make_include.(S.HASH.rpc_arg).
Definition Compare_Make_include :=
Compare.Make
(let t : Set := t in
{|
Compare.COMPARABLE.compare := Blake2B_Make_include.(S.HASH.compare)
|}).
Definition name := Blake2B_Make_include.(S.HASH.name).
Definition title := Blake2B_Make_include.(S.HASH.title).
Definition pp := Blake2B_Make_include.(S.HASH.pp).
Definition pp_short := Blake2B_Make_include.(S.HASH.pp_short).
(* Definition op_eq := Blake2B_Make_include.(S.HASH.op_eq).
Definition op_ltgt := Blake2B_Make_include.(S.HASH.op_ltgt).
Definition op_lt := Blake2B_Make_include.(S.HASH.op_lt).
Definition op_lteq := Blake2B_Make_include.(S.HASH.op_lteq).
Definition op_gteq := Blake2B_Make_include.(S.HASH.op_gteq).
Definition op_gt := Blake2B_Make_include.(S.HASH.op_gt).
Definition compare := Blake2B_Make_include.(S.HASH.compare).
Definition equal := Blake2B_Make_include.(S.HASH.equal).
Definition max := Blake2B_Make_include.(S.HASH.max).
Definition min := Blake2B_Make_include.(S.HASH.min). *)
Definition hash_bytes := Blake2B_Make_include.(S.HASH.hash_bytes).
Definition hash_string := Blake2B_Make_include.(S.HASH.hash_string).
Definition zero := Blake2B_Make_include.(S.HASH.zero).
(* Definition size_value := Blake2B_Make_include.(S.HASH.size_value). *)
Definition to_bytes := Blake2B_Make_include.(S.HASH.to_bytes).
Definition of_bytes_opt := Blake2B_Make_include.(S.HASH.of_bytes_opt).
Definition of_bytes_exn := Blake2B_Make_include.(S.HASH.of_bytes_exn).
Definition to_b58check := Blake2B_Make_include.(S.HASH.to_b58check).
Definition to_short_b58check := Blake2B_Make_include.(S.HASH.to_short_b58check).
Definition of_b58check_exn := Blake2B_Make_include.(S.HASH.of_b58check_exn).
Definition of_b58check_opt := Blake2B_Make_include.(S.HASH.of_b58check_opt).
Definition b58check_encoding := Blake2B_Make_include.(S.HASH.b58check_encoding).
Definition encoding := Blake2B_Make_include.(S.HASH.encoding).
Definition rpc_arg := Blake2B_Make_include.(S.HASH.rpc_arg).
Definition Compare_Make_include :=
Compare.Make
(let t : Set := t in
{|
Compare.COMPARABLE.compare := Blake2B_Make_include.(S.HASH.compare)
|}).
Inclusion of the module [Compare_Make_include]
Definition op_eq := Compare_Make_include.(Compare.S.op_eq).
Definition op_ltgt := Compare_Make_include.(Compare.S.op_ltgt).
Definition op_lt := Compare_Make_include.(Compare.S.op_lt).
Definition op_lteq := Compare_Make_include.(Compare.S.op_lteq).
Definition op_gteq := Compare_Make_include.(Compare.S.op_gteq).
Definition op_gt := Compare_Make_include.(Compare.S.op_gt).
Definition compare := Compare_Make_include.(Compare.S.compare).
Definition equal := Compare_Make_include.(Compare.S.equal).
Definition max := Compare_Make_include.(Compare.S.max).
Definition min := Compare_Make_include.(Compare.S.min).
Definition address : Set := t.
Definition op_ltgt := Compare_Make_include.(Compare.S.op_ltgt).
Definition op_lt := Compare_Make_include.(Compare.S.op_lt).
Definition op_lteq := Compare_Make_include.(Compare.S.op_lteq).
Definition op_gteq := Compare_Make_include.(Compare.S.op_gteq).
Definition op_gt := Compare_Make_include.(Compare.S.op_gt).
Definition compare := Compare_Make_include.(Compare.S.compare).
Definition equal := Compare_Make_include.(Compare.S.equal).
Definition max := Compare_Make_include.(Compare.S.max).
Definition min := Compare_Make_include.(Compare.S.min).
Definition address : Set := t.
Init function; without side-effects in Coq
Definition init_module : unit :=
Tx_rollup_prefixes.check_encoding Tx_rollup_prefixes.l2_address
b58check_encoding.
Definition of_bls_pk (pk : Bls_signature.pk) : t :=
hash_bytes None [ Bls_signature.pk_to_bytes pk ].
Definition in_memory_size (function_parameter : t)
: Cache_memory_helpers.sint :=
let '_ := function_parameter in
Cache_memory_helpers.op_plusexclamation
(Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.header_size
Cache_memory_helpers.word_size)
(Cache_memory_helpers.string_size_gen
Tx_rollup_prefixes.l2_address.(Tx_rollup_prefixes.t.hash_size)).
Definition size_value {A : Set} (function_parameter : A) : int :=
let '_ := function_parameter in
Tx_rollup_prefixes.l2_address.(Tx_rollup_prefixes.t.hash_size).
Module Indexable.
Definition Indexable_Make_include :=
Indexable.Make
(let t : Set := t in
{|
Indexable.VALUE.encoding := encoding;
Indexable.VALUE.compare := compare;
Indexable.VALUE.pp := pp
|}).
Tx_rollup_prefixes.check_encoding Tx_rollup_prefixes.l2_address
b58check_encoding.
Definition of_bls_pk (pk : Bls_signature.pk) : t :=
hash_bytes None [ Bls_signature.pk_to_bytes pk ].
Definition in_memory_size (function_parameter : t)
: Cache_memory_helpers.sint :=
let '_ := function_parameter in
Cache_memory_helpers.op_plusexclamation
(Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.header_size
Cache_memory_helpers.word_size)
(Cache_memory_helpers.string_size_gen
Tx_rollup_prefixes.l2_address.(Tx_rollup_prefixes.t.hash_size)).
Definition size_value {A : Set} (function_parameter : A) : int :=
let '_ := function_parameter in
Tx_rollup_prefixes.l2_address.(Tx_rollup_prefixes.t.hash_size).
Module Indexable.
Definition Indexable_Make_include :=
Indexable.Make
(let t : Set := t in
{|
Indexable.VALUE.encoding := encoding;
Indexable.VALUE.compare := compare;
Indexable.VALUE.pp := pp
|}).
Inclusion of the module [Indexable_Make_include]
Definition t := Indexable_Make_include.(Indexable.INDEXABLE.t).
Definition index := Indexable_Make_include.(Indexable.INDEXABLE.index).
Definition value := Indexable_Make_include.(Indexable.INDEXABLE.value).
Definition either := Indexable_Make_include.(Indexable.INDEXABLE.either).
Definition value_value :=
Indexable_Make_include.(Indexable.INDEXABLE.value_value).
Definition index_value :=
Indexable_Make_include.(Indexable.INDEXABLE.index_value).
Definition index_exn :=
Indexable_Make_include.(Indexable.INDEXABLE.index_exn).
Definition compact := Indexable_Make_include.(Indexable.INDEXABLE.compact).
Definition encoding := Indexable_Make_include.(Indexable.INDEXABLE.encoding).
Definition index_encoding :=
Indexable_Make_include.(Indexable.INDEXABLE.index_encoding).
Definition value_encoding :=
Indexable_Make_include.(Indexable.INDEXABLE.value_encoding).
Definition compare :=
Indexable_Make_include.(Indexable.INDEXABLE.compare)
.
Definition compare_values :=
Indexable_Make_include.(Indexable.INDEXABLE.compare_values).
Definition compare_indexes :=
Indexable_Make_include.(Indexable.INDEXABLE.compare_indexes).
Definition pp {state : Set} :=
Indexable_Make_include.(Indexable.INDEXABLE.pp) .
Definition in_memory_size (x_value : Indexable.t)
: Cache_memory_helpers.sint :=
Indexable.in_memory_size in_memory_size x_value.
Definition size_value (x_value : Indexable.t) : int :=
Indexable.size_value size_value x_value.
End Indexable.
Definition index := Indexable_Make_include.(Indexable.INDEXABLE.index).
Definition value := Indexable_Make_include.(Indexable.INDEXABLE.value).
Definition either := Indexable_Make_include.(Indexable.INDEXABLE.either).
Definition value_value :=
Indexable_Make_include.(Indexable.INDEXABLE.value_value).
Definition index_value :=
Indexable_Make_include.(Indexable.INDEXABLE.index_value).
Definition index_exn :=
Indexable_Make_include.(Indexable.INDEXABLE.index_exn).
Definition compact := Indexable_Make_include.(Indexable.INDEXABLE.compact).
Definition encoding := Indexable_Make_include.(Indexable.INDEXABLE.encoding).
Definition index_encoding :=
Indexable_Make_include.(Indexable.INDEXABLE.index_encoding).
Definition value_encoding :=
Indexable_Make_include.(Indexable.INDEXABLE.value_encoding).
Definition compare :=
Indexable_Make_include.(Indexable.INDEXABLE.compare)
.
Definition compare_values :=
Indexable_Make_include.(Indexable.INDEXABLE.compare_values).
Definition compare_indexes :=
Indexable_Make_include.(Indexable.INDEXABLE.compare_indexes).
Definition pp {state : Set} :=
Indexable_Make_include.(Indexable.INDEXABLE.pp) .
Definition in_memory_size (x_value : Indexable.t)
: Cache_memory_helpers.sint :=
Indexable.in_memory_size in_memory_size x_value.
Definition size_value (x_value : Indexable.t) : int :=
Indexable.size_value size_value x_value.
End Indexable.