🐆 Tx_rollup_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.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Origination_nonce.
Require TezosOfOCaml.Proto_alpha.Path_encoding.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_prefixes.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Origination_nonce.
Require TezosOfOCaml.Proto_alpha.Path_encoding.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_prefixes.
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
Error_monad.register_error_kind Error_monad.Permanent
"rollup.invalid_tx_rollup_notation" "Invalid tx rollup notation"
"A malformed tx rollup notation was given to an RPC or in a script."
(Some
(fun (ppf : Format.formatter) ⇒
fun (x_value : string) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid tx rollup notation "
(CamlinternalFormatBasics.Caml_string
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))
"Invalid tx rollup notation %S") x_value))
(Data_encoding.obj1
(Data_encoding.req None None "notation" Data_encoding.string_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_rollup_notation" then
let loc_value := cast string payload in
Some loc_value
else None
end)
(fun (loc_value : string) ⇒
Build_extensible "Invalid_rollup_notation" string loc_value).
Module Hash.
Definition rollup_hash : string :=
Tx_rollup_prefixes.rollup_address.(Tx_rollup_prefixes.t.b58check_prefix).
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "Rollup_hash" in
let title := "A rollup ID" in
let b58check_prefix := rollup_hash in
let size_value :=
Some Tx_rollup_prefixes.rollup_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
|}).
Error_monad.register_error_kind Error_monad.Permanent
"rollup.invalid_tx_rollup_notation" "Invalid tx rollup notation"
"A malformed tx rollup notation was given to an RPC or in a script."
(Some
(fun (ppf : Format.formatter) ⇒
fun (x_value : string) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid tx rollup notation "
(CamlinternalFormatBasics.Caml_string
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))
"Invalid tx rollup notation %S") x_value))
(Data_encoding.obj1
(Data_encoding.req None None "notation" Data_encoding.string_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_rollup_notation" then
let loc_value := cast string payload in
Some loc_value
else None
end)
(fun (loc_value : string) ⇒
Build_extensible "Invalid_rollup_notation" string loc_value).
Module Hash.
Definition rollup_hash : string :=
Tx_rollup_prefixes.rollup_address.(Tx_rollup_prefixes.t.b58check_prefix).
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "Rollup_hash" in
let title := "A rollup ID" in
let b58check_prefix := rollup_hash in
let size_value :=
Some Tx_rollup_prefixes.rollup_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 [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 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).
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
Tx_rollup_prefixes.check_encoding Tx_rollup_prefixes.rollup_address
b58check_encoding.
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)
|}.
Tx_rollup_prefixes.check_encoding Tx_rollup_prefixes.rollup_address
b58check_encoding.
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).
End Hash.
Definition t : Set := Hash.t.
Definition Compare_impl :=
Compare.Make
(let t : Set := t in
let compare (r1 : Hash.t) (r2 : Hash.t) : int :=
Hash.compare r1 r2 in
{|
Compare.COMPARABLE.compare := compare
|}).
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).
End Hash.
Definition t : Set := Hash.t.
Definition Compare_impl :=
Compare.Make
(let t : Set := t in
let compare (r1 : Hash.t) (r2 : Hash.t) : int :=
Hash.compare r1 r2 in
{|
Compare.COMPARABLE.compare := compare
|}).
Inclusion of the module [Compare_impl]
Definition op_eq := Compare_impl.(Compare.S.op_eq).
Definition op_ltgt := Compare_impl.(Compare.S.op_ltgt).
Definition op_lt := Compare_impl.(Compare.S.op_lt).
Definition op_lteq := Compare_impl.(Compare.S.op_lteq).
Definition op_gteq := Compare_impl.(Compare.S.op_gteq).
Definition op_gt := Compare_impl.(Compare.S.op_gt).
Definition compare := Compare_impl.(Compare.S.compare).
Definition equal := Compare_impl.(Compare.S.equal).
Definition max := Compare_impl.(Compare.S.max).
Definition min := Compare_impl.(Compare.S.min).
Definition in_memory_size {A : Set} (function_parameter : A)
: Saturation_repr.t :=
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.rollup_address.(Tx_rollup_prefixes.t.hash_size)).
Definition to_b58check (rollup : Hash.t) : string := Hash.to_b58check rollup.
Definition of_b58data (function_parameter : Base58.data) : option Hash.t :=
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Data" then
let hash_value := cast Hash.t payload in
Some hash_value
else None
end.
Definition of_b58check_opt (s_value : string) : option Hash.t :=
Option.bind (Base58.decode s_value) of_b58data.
Definition of_b58check (s_value : string) : M? Hash.t :=
match of_b58check_opt s_value with
| Some hash_value ⇒ return? hash_value
| _ ⇒
Error_monad.error_value
(Build_extensible "Invalid_rollup_notation" string s_value)
end.
Definition pp (ppf : Format.formatter) (hash_value : Hash.t) : unit :=
Hash.pp ppf hash_value.
Definition encoding : Data_encoding.encoding Hash.t :=
Data_encoding.def "tx_rollup_id" (Some "A tx rollup handle")
(Some
"A tx rollup notation as given to an RPC or inside scripts, is a base58 tx rollup hash")
(Data_encoding.splitted
(Data_encoding.conv to_b58check
(fun (s_value : string) ⇒
match of_b58check s_value with
| Pervasives.Ok s_value ⇒ s_value
| Pervasives.Error _ ⇒
Data_encoding.Json.cannot_destruct
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid tx rollup notation."
CamlinternalFormatBasics.End_of_format)
"Invalid tx rollup notation.")
end) None Data_encoding.string_value) Hash.encoding).
Definition originated_tx_rollup (nonce_value : Origination_nonce.t) : Hash.t :=
let data :=
Data_encoding.Binary.to_bytes_exn None Origination_nonce.encoding
nonce_value in
Hash.hash_bytes None [ data ].
Definition rpc_arg : RPC_arg.arg Hash.t :=
let construct := to_b58check in
let destruct (hash_value : string) : Pervasives.result Hash.t string :=
Result.map_error
(fun (function_parameter : Error_monad.trace Error_monad._error) ⇒
let '_ := function_parameter in
"Cannot parse tx rollup id") (of_b58check hash_value) in
RPC_arg.make (Some "A tx rollup identifier encoded in b58check.")
"tx_rollup_id" destruct construct tt.
Module Index.
Definition t : Set := t.
Definition path_length : M? int := return? 1.
Definition to_path (c_value : Hash.t) (l_value : list string) : list string :=
let raw_key := Data_encoding.Binary.to_bytes_exn None encoding c_value in
let 'Hex.Hex key_value := Hex.of_bytes None raw_key in
cons key_value l_value.
Definition of_path (function_parameter : list string) : M? (option Hash.t) :=
match function_parameter with
| cons key_value [] ⇒
return?
(Option.bind (Hex.to_bytes (Hex.Hex key_value))
(Data_encoding.Binary.of_bytes_opt encoding))
| _ ⇒ return? None
end.
Definition rpc_arg : RPC_arg.arg Hash.t := rpc_arg.
Definition encoding : Data_encoding.encoding Hash.t := encoding.
Definition compare : t → t → int := compare.
(* Index *)
Definition module :=
{|
Storage_description.INDEX.path_length := path_length;
Storage_description.INDEX.to_path := to_path;
Storage_description.INDEX.of_path := of_path;
Storage_description.INDEX.rpc_arg := rpc_arg;
Storage_description.INDEX.encoding := encoding;
Storage_description.INDEX.compare := compare
|}.
End Index.
Definition Index := Index.module.
Module Cmp.
Definition t : Set := t.
Definition compare : t → t → int := compare.
(* Cmp *)
Definition module :=
{|
Compare.COMPARABLE.compare := compare
|}.
End Cmp.
Definition Cmp := Cmp.module.
Definition _Set := _Set.Make Cmp.
Definition Map := Map.Make Cmp.
Definition op_ltgt := Compare_impl.(Compare.S.op_ltgt).
Definition op_lt := Compare_impl.(Compare.S.op_lt).
Definition op_lteq := Compare_impl.(Compare.S.op_lteq).
Definition op_gteq := Compare_impl.(Compare.S.op_gteq).
Definition op_gt := Compare_impl.(Compare.S.op_gt).
Definition compare := Compare_impl.(Compare.S.compare).
Definition equal := Compare_impl.(Compare.S.equal).
Definition max := Compare_impl.(Compare.S.max).
Definition min := Compare_impl.(Compare.S.min).
Definition in_memory_size {A : Set} (function_parameter : A)
: Saturation_repr.t :=
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.rollup_address.(Tx_rollup_prefixes.t.hash_size)).
Definition to_b58check (rollup : Hash.t) : string := Hash.to_b58check rollup.
Definition of_b58data (function_parameter : Base58.data) : option Hash.t :=
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Data" then
let hash_value := cast Hash.t payload in
Some hash_value
else None
end.
Definition of_b58check_opt (s_value : string) : option Hash.t :=
Option.bind (Base58.decode s_value) of_b58data.
Definition of_b58check (s_value : string) : M? Hash.t :=
match of_b58check_opt s_value with
| Some hash_value ⇒ return? hash_value
| _ ⇒
Error_monad.error_value
(Build_extensible "Invalid_rollup_notation" string s_value)
end.
Definition pp (ppf : Format.formatter) (hash_value : Hash.t) : unit :=
Hash.pp ppf hash_value.
Definition encoding : Data_encoding.encoding Hash.t :=
Data_encoding.def "tx_rollup_id" (Some "A tx rollup handle")
(Some
"A tx rollup notation as given to an RPC or inside scripts, is a base58 tx rollup hash")
(Data_encoding.splitted
(Data_encoding.conv to_b58check
(fun (s_value : string) ⇒
match of_b58check s_value with
| Pervasives.Ok s_value ⇒ s_value
| Pervasives.Error _ ⇒
Data_encoding.Json.cannot_destruct
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid tx rollup notation."
CamlinternalFormatBasics.End_of_format)
"Invalid tx rollup notation.")
end) None Data_encoding.string_value) Hash.encoding).
Definition originated_tx_rollup (nonce_value : Origination_nonce.t) : Hash.t :=
let data :=
Data_encoding.Binary.to_bytes_exn None Origination_nonce.encoding
nonce_value in
Hash.hash_bytes None [ data ].
Definition rpc_arg : RPC_arg.arg Hash.t :=
let construct := to_b58check in
let destruct (hash_value : string) : Pervasives.result Hash.t string :=
Result.map_error
(fun (function_parameter : Error_monad.trace Error_monad._error) ⇒
let '_ := function_parameter in
"Cannot parse tx rollup id") (of_b58check hash_value) in
RPC_arg.make (Some "A tx rollup identifier encoded in b58check.")
"tx_rollup_id" destruct construct tt.
Module Index.
Definition t : Set := t.
Definition path_length : M? int := return? 1.
Definition to_path (c_value : Hash.t) (l_value : list string) : list string :=
let raw_key := Data_encoding.Binary.to_bytes_exn None encoding c_value in
let 'Hex.Hex key_value := Hex.of_bytes None raw_key in
cons key_value l_value.
Definition of_path (function_parameter : list string) : M? (option Hash.t) :=
match function_parameter with
| cons key_value [] ⇒
return?
(Option.bind (Hex.to_bytes (Hex.Hex key_value))
(Data_encoding.Binary.of_bytes_opt encoding))
| _ ⇒ return? None
end.
Definition rpc_arg : RPC_arg.arg Hash.t := rpc_arg.
Definition encoding : Data_encoding.encoding Hash.t := encoding.
Definition compare : t → t → int := compare.
(* Index *)
Definition module :=
{|
Storage_description.INDEX.path_length := path_length;
Storage_description.INDEX.to_path := to_path;
Storage_description.INDEX.of_path := of_path;
Storage_description.INDEX.rpc_arg := rpc_arg;
Storage_description.INDEX.encoding := encoding;
Storage_description.INDEX.compare := compare
|}.
End Index.
Definition Index := Index.module.
Module Cmp.
Definition t : Set := t.
Definition compare : t → t → int := compare.
(* Cmp *)
Definition module :=
{|
Compare.COMPARABLE.compare := compare
|}.
End Cmp.
Definition Cmp := Cmp.module.
Definition _Set := _Set.Make Cmp.
Definition Map := Map.Make Cmp.