🇿 Zk_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.Zk_rollup_scalar.
Module Address.
Definition prefix : string := "epx1".
Definition encoded_size : int := 37.
Definition decoded_prefix : string :=
String.String "001" (String.String "023" (String.String "224" "}")).
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "Zk_rollup_hash" in
let title := "A zk rollup address" in
let b58check_prefix := decoded_prefix in
let size_value := Some 20 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.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.Zk_rollup_scalar.
Module Address.
Definition prefix : string := "epx1".
Definition encoded_size : int := 37.
Definition decoded_prefix : string :=
String.String "001" (String.String "023" (String.String "224" "}")).
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "Zk_rollup_hash" in
let title := "A zk rollup address" in
let b58check_prefix := decoded_prefix in
let size_value := Some 20 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_module1 : unit :=
Base58.check_encoded_prefix b58check_encoding prefix encoded_size.
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)
|}.
Base58.check_encoded_prefix b58check_encoding prefix encoded_size.
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).
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).
Init function; without side-effects in Coq
Definition init_module2 : unit :=
let msg := "Error while generating rollup address" in
Error_monad.register_error_kind Error_monad.Permanent
"rollup.error_zk_rollup_address_generation" msg msg
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") msg))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Error_zk_rollup_address_generation" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Error_zk_rollup_address_generation" unit tt).
Definition from_nonce (nonce_value : Origination_nonce.t) : M? t :=
(fun (function_parameter : option bytes) ⇒
match function_parameter with
| None ⇒
Error_monad.error_value
(Build_extensible "Error_zk_rollup_address_generation" unit tt)
| Some nonce_value ⇒ return? (hash_bytes None [ nonce_value ])
end)
(Data_encoding.Binary.to_bytes_opt None Origination_nonce.encoding
nonce_value).
Definition of_b58data (function_parameter : Base58.data)
: option H.(S.HASH.t) :=
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Data" then
let h_value := cast H.(S.HASH.t) payload in
Some h_value
else None
end.
End Address.
Definition t : Set := Address.t.
Definition to_scalar (x_value : Address.t) : Zk_rollup_scalar.t :=
Zk_rollup_scalar.of_bits
(Data_encoding.Binary.to_string_exn None Address.encoding x_value).
let msg := "Error while generating rollup address" in
Error_monad.register_error_kind Error_monad.Permanent
"rollup.error_zk_rollup_address_generation" msg msg
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") msg))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Error_zk_rollup_address_generation" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Error_zk_rollup_address_generation" unit tt).
Definition from_nonce (nonce_value : Origination_nonce.t) : M? t :=
(fun (function_parameter : option bytes) ⇒
match function_parameter with
| None ⇒
Error_monad.error_value
(Build_extensible "Error_zk_rollup_address_generation" unit tt)
| Some nonce_value ⇒ return? (hash_bytes None [ nonce_value ])
end)
(Data_encoding.Binary.to_bytes_opt None Origination_nonce.encoding
nonce_value).
Definition of_b58data (function_parameter : Base58.data)
: option H.(S.HASH.t) :=
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Data" then
let h_value := cast H.(S.HASH.t) payload in
Some h_value
else None
end.
End Address.
Definition t : Set := Address.t.
Definition to_scalar (x_value : Address.t) : Zk_rollup_scalar.t :=
Zk_rollup_scalar.of_bits
(Data_encoding.Binary.to_string_exn None Address.encoding x_value).
Records for the constructor parameters
Module ConstructorRecords_pending_list.
Module pending_list.
Module Empty.
Record record {next_index : Set} : Set := Build {
next_index : next_index;
}.
Arguments record : clear implicits.
Definition with_next_index {t_next_index} next_index
(r : record t_next_index) :=
Build t_next_index next_index.
End Empty.
Definition Empty_skeleton := Empty.record.
Module Pending.
Record record {next_index length : Set} : Set := Build {
next_index : next_index;
length : length;
}.
Arguments record : clear implicits.
Definition with_next_index {t_next_index t_length} next_index
(r : record t_next_index t_length) :=
Build t_next_index t_length next_index r.(length).
Definition with_length {t_next_index t_length} length
(r : record t_next_index t_length) :=
Build t_next_index t_length r.(next_index) length.
End Pending.
Definition Pending_skeleton := Pending.record.
End pending_list.
End ConstructorRecords_pending_list.
Import ConstructorRecords_pending_list.
Reserved Notation "'pending_list.Empty".
Reserved Notation "'pending_list.Pending".
Inductive pending_list : Set :=
| Empty : 'pending_list.Empty → pending_list
| Pending : 'pending_list.Pending → pending_list
where "'pending_list.Empty" := (pending_list.Empty_skeleton int64)
and "'pending_list.Pending" := (pending_list.Pending_skeleton int64 int).
Module pending_list.
Include ConstructorRecords_pending_list.pending_list.
Definition Empty := 'pending_list.Empty.
Definition Pending := 'pending_list.Pending.
End pending_list.
Definition pending_list_encoding : Data_encoding.t pending_list :=
let '(empty_tag, pending_tag) := (0, 1) in
let empty_encoding :=
Data_encoding.obj1
(Data_encoding.req None None "next_index"
(Data_encoding.Compact.make (Some (Variant.Build "Uint8" unit tt))
Data_encoding.Compact.int64_value)) in
let pending_encoding :=
Data_encoding.obj2
(Data_encoding.req None None "next_index"
(Data_encoding.Compact.make (Some (Variant.Build "Uint8" unit tt))
Data_encoding.Compact.int64_value))
(Data_encoding.req None None "length" Data_encoding.uint16) in
Data_encoding.matching None
(fun (function_parameter : pending_list) ⇒
match function_parameter with
| Empty {| pending_list.Empty.next_index := next_index |} ⇒
Data_encoding.matched None empty_tag empty_encoding next_index
|
Pending {|
pending_list.Pending.next_index := next_index;
pending_list.Pending.length := length
|} ⇒
Data_encoding.matched None pending_tag pending_encoding
(next_index, length)
end)
[
Data_encoding.case_value "Empty" None (Data_encoding.Tag empty_tag)
empty_encoding
(fun (function_parameter : pending_list) ⇒
match function_parameter with
| Empty {| pending_list.Empty.next_index := next_index |} ⇒
Some next_index
| _ ⇒ None
end)
(fun (next_index : int64) ⇒
Empty {| pending_list.Empty.next_index := next_index; |});
Data_encoding.case_value "Pending" None (Data_encoding.Tag pending_tag)
pending_encoding
(fun (function_parameter : pending_list) ⇒
match function_parameter with
|
Pending {|
pending_list.Pending.next_index := next_index;
pending_list.Pending.length := length
|} ⇒ Some (next_index, length)
| _ ⇒ None
end)
(fun (function_parameter : int64 × int) ⇒
let '(next_index, length) := function_parameter in
Pending
{| pending_list.Pending.next_index := next_index;
pending_list.Pending.length := length; |})
].
Module Index.
Definition t : Set := t.
Definition path_length : M? int := return? 1.
Definition to_path (c_value : Address.t) (l_value : list string)
: list string :=
let raw_key :=
Data_encoding.Binary.to_bytes_exn None Address.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 Address.t) :=
match function_parameter with
| cons key_value [] ⇒
return?
(Option.bind (Hex.to_bytes (Hex.Hex key_value))
(Data_encoding.Binary.of_bytes_opt Address.encoding))
| _ ⇒ return? None
end.
Definition rpc_arg : RPC_arg.t Address.t := Address.rpc_arg.
Definition encoding : Data_encoding.t Address.t := Address.encoding.
Definition compare : Address.t → Address.t → int := Address.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.
Definition in_memory_size (function_parameter : t) : Saturation_repr.t :=
let '_ := function_parameter in
Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
(Cache_memory_helpers.string_size_gen Address.size_value).
Module pending_list.
Module Empty.
Record record {next_index : Set} : Set := Build {
next_index : next_index;
}.
Arguments record : clear implicits.
Definition with_next_index {t_next_index} next_index
(r : record t_next_index) :=
Build t_next_index next_index.
End Empty.
Definition Empty_skeleton := Empty.record.
Module Pending.
Record record {next_index length : Set} : Set := Build {
next_index : next_index;
length : length;
}.
Arguments record : clear implicits.
Definition with_next_index {t_next_index t_length} next_index
(r : record t_next_index t_length) :=
Build t_next_index t_length next_index r.(length).
Definition with_length {t_next_index t_length} length
(r : record t_next_index t_length) :=
Build t_next_index t_length r.(next_index) length.
End Pending.
Definition Pending_skeleton := Pending.record.
End pending_list.
End ConstructorRecords_pending_list.
Import ConstructorRecords_pending_list.
Reserved Notation "'pending_list.Empty".
Reserved Notation "'pending_list.Pending".
Inductive pending_list : Set :=
| Empty : 'pending_list.Empty → pending_list
| Pending : 'pending_list.Pending → pending_list
where "'pending_list.Empty" := (pending_list.Empty_skeleton int64)
and "'pending_list.Pending" := (pending_list.Pending_skeleton int64 int).
Module pending_list.
Include ConstructorRecords_pending_list.pending_list.
Definition Empty := 'pending_list.Empty.
Definition Pending := 'pending_list.Pending.
End pending_list.
Definition pending_list_encoding : Data_encoding.t pending_list :=
let '(empty_tag, pending_tag) := (0, 1) in
let empty_encoding :=
Data_encoding.obj1
(Data_encoding.req None None "next_index"
(Data_encoding.Compact.make (Some (Variant.Build "Uint8" unit tt))
Data_encoding.Compact.int64_value)) in
let pending_encoding :=
Data_encoding.obj2
(Data_encoding.req None None "next_index"
(Data_encoding.Compact.make (Some (Variant.Build "Uint8" unit tt))
Data_encoding.Compact.int64_value))
(Data_encoding.req None None "length" Data_encoding.uint16) in
Data_encoding.matching None
(fun (function_parameter : pending_list) ⇒
match function_parameter with
| Empty {| pending_list.Empty.next_index := next_index |} ⇒
Data_encoding.matched None empty_tag empty_encoding next_index
|
Pending {|
pending_list.Pending.next_index := next_index;
pending_list.Pending.length := length
|} ⇒
Data_encoding.matched None pending_tag pending_encoding
(next_index, length)
end)
[
Data_encoding.case_value "Empty" None (Data_encoding.Tag empty_tag)
empty_encoding
(fun (function_parameter : pending_list) ⇒
match function_parameter with
| Empty {| pending_list.Empty.next_index := next_index |} ⇒
Some next_index
| _ ⇒ None
end)
(fun (next_index : int64) ⇒
Empty {| pending_list.Empty.next_index := next_index; |});
Data_encoding.case_value "Pending" None (Data_encoding.Tag pending_tag)
pending_encoding
(fun (function_parameter : pending_list) ⇒
match function_parameter with
|
Pending {|
pending_list.Pending.next_index := next_index;
pending_list.Pending.length := length
|} ⇒ Some (next_index, length)
| _ ⇒ None
end)
(fun (function_parameter : int64 × int) ⇒
let '(next_index, length) := function_parameter in
Pending
{| pending_list.Pending.next_index := next_index;
pending_list.Pending.length := length; |})
].
Module Index.
Definition t : Set := t.
Definition path_length : M? int := return? 1.
Definition to_path (c_value : Address.t) (l_value : list string)
: list string :=
let raw_key :=
Data_encoding.Binary.to_bytes_exn None Address.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 Address.t) :=
match function_parameter with
| cons key_value [] ⇒
return?
(Option.bind (Hex.to_bytes (Hex.Hex key_value))
(Data_encoding.Binary.of_bytes_opt Address.encoding))
| _ ⇒ return? None
end.
Definition rpc_arg : RPC_arg.t Address.t := Address.rpc_arg.
Definition encoding : Data_encoding.t Address.t := Address.encoding.
Definition compare : Address.t → Address.t → int := Address.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.
Definition in_memory_size (function_parameter : t) : Saturation_repr.t :=
let '_ := function_parameter in
Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
(Cache_memory_helpers.string_size_gen Address.size_value).