🎯 Destination_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.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_repr.
Inductive t : Set :=
| Contract : Contract_repr.t → t
| Tx_rollup : Tx_rollup_repr.t → t
| Sc_rollup : Sc_rollup_repr.t → t
| Zk_rollup : Zk_rollup_repr.t → t.
Definition Compare_Make_include :=
Compare.Make
(let t : Set := t in
let compare (l1 : t) (l2 : t) : int :=
match (l1, l2) with
| (Contract k1, Contract k2) ⇒ Contract_repr.compare k1 k2
| (Tx_rollup k1, Tx_rollup k2) ⇒ Tx_rollup_repr.compare k1 k2
| (Sc_rollup k1, Sc_rollup k2) ⇒ Sc_rollup_repr.Address.compare k1 k2
| (Zk_rollup k1, Zk_rollup k2) ⇒ Zk_rollup_repr.Address.compare k1 k2
| (Contract _, _) ⇒ (-1)
| (_, Contract _) ⇒ 1
| (Tx_rollup _, _) ⇒ (-1)
| (_, Tx_rollup _) ⇒ 1
| (Sc_rollup _, _) ⇒ (-1)
| (_, Sc_rollup _) ⇒ 1
end in
{|
Compare.COMPARABLE.compare := compare
|}).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_repr.
Inductive t : Set :=
| Contract : Contract_repr.t → t
| Tx_rollup : Tx_rollup_repr.t → t
| Sc_rollup : Sc_rollup_repr.t → t
| Zk_rollup : Zk_rollup_repr.t → t.
Definition Compare_Make_include :=
Compare.Make
(let t : Set := t in
let compare (l1 : t) (l2 : t) : int :=
match (l1, l2) with
| (Contract k1, Contract k2) ⇒ Contract_repr.compare k1 k2
| (Tx_rollup k1, Tx_rollup k2) ⇒ Tx_rollup_repr.compare k1 k2
| (Sc_rollup k1, Sc_rollup k2) ⇒ Sc_rollup_repr.Address.compare k1 k2
| (Zk_rollup k1, Zk_rollup k2) ⇒ Zk_rollup_repr.Address.compare k1 k2
| (Contract _, _) ⇒ (-1)
| (_, Contract _) ⇒ 1
| (Tx_rollup _, _) ⇒ (-1)
| (_, Tx_rollup _) ⇒ 1
| (Sc_rollup _, _) ⇒ (-1)
| (_, Sc_rollup _) ⇒ 1
end in
{|
Compare.COMPARABLE.compare := 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 to_b58check (function_parameter : t) : string :=
match function_parameter with
| Contract k_value ⇒ Contract_repr.to_b58check k_value
| Tx_rollup k_value ⇒ Tx_rollup_repr.to_b58check k_value
| Sc_rollup k_value ⇒ Sc_rollup_repr.Address.to_b58check k_value
| Zk_rollup k_value ⇒ Zk_rollup_repr.Address.to_b58check k_value
end.
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 to_b58check (function_parameter : t) : string :=
match function_parameter with
| Contract k_value ⇒ Contract_repr.to_b58check k_value
| Tx_rollup k_value ⇒ Tx_rollup_repr.to_b58check k_value
| Sc_rollup k_value ⇒ Sc_rollup_repr.Address.to_b58check k_value
| Zk_rollup k_value ⇒ Zk_rollup_repr.Address.to_b58check k_value
end.
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
Error_monad.register_error_kind Error_monad.Permanent
"destination_repr.invalid_b58check" "Destination decoding failed"
"Failed to read a valid destination from a b58check_encoding data" None
(Data_encoding.obj1
(Data_encoding.req None None "input" Data_encoding.string_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_destination_b58check" then
let x_value := cast string payload in
Some x_value
else None
end)
(fun (x_value : string) ⇒
Build_extensible "Invalid_destination_b58check" string x_value).
Definition of_b58data (data : Base58.data) : option t :=
let decode_on_none {A B : Set}
(decode : Base58.data → option A) (wrap : A → B)
(function_parameter : option B) : option B :=
match function_parameter with
| Some x_value ⇒ Some x_value
| None ⇒ Option.map wrap (decode data)
end in
decode_on_none Zk_rollup_repr.Address.of_b58data
(fun (z_value : Zk_rollup_repr.Address.t) ⇒ Zk_rollup z_value)
(decode_on_none Sc_rollup_repr.Address.of_b58data
(fun (s_value : Sc_rollup_repr.Address.t) ⇒ Sc_rollup s_value)
(decode_on_none Tx_rollup_repr.of_b58data
(fun (t_value : Tx_rollup_repr.t) ⇒ Tx_rollup t_value)
(decode_on_none Contract_repr.of_b58data
(fun (c_value : Contract_repr.t) ⇒ Contract c_value) None))).
Definition of_b58check_opt (s_value : string) : option t :=
Option.bind (Base58.decode s_value) of_b58data.
Definition of_b58check (s_value : string) : M? t :=
match of_b58check_opt s_value with
| None ⇒
Error_monad.error_value
(Build_extensible "Invalid_destination_b58check" string s_value)
| Some dest ⇒ Pervasives.Ok dest
end.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.def "transaction_destination"
(Some "A destination of a transaction")
(Some
"A destination notation compatible with the contract notation as given to an RPC or inside scripts. Can be a base58 implicit contract hash, a base58 originated contract hash, a base58 originated transaction rollup, or a base58 originated smart-contract rollup.")
(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 destination notation."
CamlinternalFormatBasics.End_of_format)
"Invalid destination notation.")
end) None Data_encoding.string_value)
(Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
(Pervasives.op_at
(Contract_repr.cases
(fun (function_parameter : t) ⇒
match function_parameter with
| Contract x_value ⇒ Some x_value
| _ ⇒ None
end) (fun (x_value : Contract_repr.t) ⇒ Contract x_value))
[
Data_encoding.case_value "Tx_rollup" None (Data_encoding.Tag 2)
(Data_encoding.Fixed.add_padding Tx_rollup_repr.encoding 1)
(fun (function_parameter : t) ⇒
match function_parameter with
| Tx_rollup k_value ⇒ Some k_value
| _ ⇒ None
end)
(fun (k_value : Tx_rollup_repr.t) ⇒ Tx_rollup k_value);
Data_encoding.case_value "Sc_rollup" None (Data_encoding.Tag 3)
(Data_encoding.Fixed.add_padding
Sc_rollup_repr.Address.encoding 1)
(fun (function_parameter : t) ⇒
match function_parameter with
| Sc_rollup k_value ⇒ Some k_value
| _ ⇒ None
end)
(fun (k_value : Sc_rollup_repr.Address.t) ⇒
Sc_rollup k_value);
Data_encoding.case_value "Zk_rollup" None (Data_encoding.Tag 4)
(Data_encoding.Fixed.add_padding
Zk_rollup_repr.Address.encoding 1)
(fun (function_parameter : t) ⇒
match function_parameter with
| Zk_rollup k_value ⇒ Some k_value
| _ ⇒ None
end)
(fun (k_value : Zk_rollup_repr.Address.t) ⇒
Zk_rollup k_value)
]))).
Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
match function_parameter with
| Contract k_value ⇒ Contract_repr.pp fmt k_value
| Tx_rollup k_value ⇒ Tx_rollup_repr.pp fmt k_value
| Sc_rollup k_value ⇒ Sc_rollup_repr.pp fmt k_value
| Zk_rollup k_value ⇒ Zk_rollup_repr.Address.pp fmt k_value
end.
Definition in_memory_size (function_parameter : t) : Saturation_repr.t :=
match function_parameter with
| Contract k_value ⇒
Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
(Contract_repr.in_memory_size k_value)
| Tx_rollup k_value ⇒
Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
(Tx_rollup_repr.in_memory_size k_value)
| Sc_rollup k_value ⇒
Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
(Sc_rollup_repr.in_memory_size k_value)
| Zk_rollup k_value ⇒
Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
(Zk_rollup_repr.in_memory_size k_value)
end.
Error_monad.register_error_kind Error_monad.Permanent
"destination_repr.invalid_b58check" "Destination decoding failed"
"Failed to read a valid destination from a b58check_encoding data" None
(Data_encoding.obj1
(Data_encoding.req None None "input" Data_encoding.string_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_destination_b58check" then
let x_value := cast string payload in
Some x_value
else None
end)
(fun (x_value : string) ⇒
Build_extensible "Invalid_destination_b58check" string x_value).
Definition of_b58data (data : Base58.data) : option t :=
let decode_on_none {A B : Set}
(decode : Base58.data → option A) (wrap : A → B)
(function_parameter : option B) : option B :=
match function_parameter with
| Some x_value ⇒ Some x_value
| None ⇒ Option.map wrap (decode data)
end in
decode_on_none Zk_rollup_repr.Address.of_b58data
(fun (z_value : Zk_rollup_repr.Address.t) ⇒ Zk_rollup z_value)
(decode_on_none Sc_rollup_repr.Address.of_b58data
(fun (s_value : Sc_rollup_repr.Address.t) ⇒ Sc_rollup s_value)
(decode_on_none Tx_rollup_repr.of_b58data
(fun (t_value : Tx_rollup_repr.t) ⇒ Tx_rollup t_value)
(decode_on_none Contract_repr.of_b58data
(fun (c_value : Contract_repr.t) ⇒ Contract c_value) None))).
Definition of_b58check_opt (s_value : string) : option t :=
Option.bind (Base58.decode s_value) of_b58data.
Definition of_b58check (s_value : string) : M? t :=
match of_b58check_opt s_value with
| None ⇒
Error_monad.error_value
(Build_extensible "Invalid_destination_b58check" string s_value)
| Some dest ⇒ Pervasives.Ok dest
end.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.def "transaction_destination"
(Some "A destination of a transaction")
(Some
"A destination notation compatible with the contract notation as given to an RPC or inside scripts. Can be a base58 implicit contract hash, a base58 originated contract hash, a base58 originated transaction rollup, or a base58 originated smart-contract rollup.")
(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 destination notation."
CamlinternalFormatBasics.End_of_format)
"Invalid destination notation.")
end) None Data_encoding.string_value)
(Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
(Pervasives.op_at
(Contract_repr.cases
(fun (function_parameter : t) ⇒
match function_parameter with
| Contract x_value ⇒ Some x_value
| _ ⇒ None
end) (fun (x_value : Contract_repr.t) ⇒ Contract x_value))
[
Data_encoding.case_value "Tx_rollup" None (Data_encoding.Tag 2)
(Data_encoding.Fixed.add_padding Tx_rollup_repr.encoding 1)
(fun (function_parameter : t) ⇒
match function_parameter with
| Tx_rollup k_value ⇒ Some k_value
| _ ⇒ None
end)
(fun (k_value : Tx_rollup_repr.t) ⇒ Tx_rollup k_value);
Data_encoding.case_value "Sc_rollup" None (Data_encoding.Tag 3)
(Data_encoding.Fixed.add_padding
Sc_rollup_repr.Address.encoding 1)
(fun (function_parameter : t) ⇒
match function_parameter with
| Sc_rollup k_value ⇒ Some k_value
| _ ⇒ None
end)
(fun (k_value : Sc_rollup_repr.Address.t) ⇒
Sc_rollup k_value);
Data_encoding.case_value "Zk_rollup" None (Data_encoding.Tag 4)
(Data_encoding.Fixed.add_padding
Zk_rollup_repr.Address.encoding 1)
(fun (function_parameter : t) ⇒
match function_parameter with
| Zk_rollup k_value ⇒ Some k_value
| _ ⇒ None
end)
(fun (k_value : Zk_rollup_repr.Address.t) ⇒
Zk_rollup k_value)
]))).
Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
match function_parameter with
| Contract k_value ⇒ Contract_repr.pp fmt k_value
| Tx_rollup k_value ⇒ Tx_rollup_repr.pp fmt k_value
| Sc_rollup k_value ⇒ Sc_rollup_repr.pp fmt k_value
| Zk_rollup k_value ⇒ Zk_rollup_repr.Address.pp fmt k_value
end.
Definition in_memory_size (function_parameter : t) : Saturation_repr.t :=
match function_parameter with
| Contract k_value ⇒
Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
(Contract_repr.in_memory_size k_value)
| Tx_rollup k_value ⇒
Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
(Tx_rollup_repr.in_memory_size k_value)
| Sc_rollup k_value ⇒
Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
(Sc_rollup_repr.in_memory_size k_value)
| Zk_rollup k_value ⇒
Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
(Zk_rollup_repr.in_memory_size k_value)
end.