🐆 Tx_rollup_commitment_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.Merkle_list.
Require TezosOfOCaml.Proto_alpha.Path_encoding.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_level_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_result_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_prefixes.
Module Hash.
Definition commitment_hash : string :=
Tx_rollup_prefixes.commitment_hash.(Tx_rollup_prefixes.t.b58check_prefix).
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "Commitment_hash" in
let title := "A commitment ID" in
let b58check_prefix := commitment_hash in
let size_value :=
Some Tx_rollup_prefixes.commitment_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.Merkle_list.
Require TezosOfOCaml.Proto_alpha.Path_encoding.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_level_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_result_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_prefixes.
Module Hash.
Definition commitment_hash : string :=
Tx_rollup_prefixes.commitment_hash.(Tx_rollup_prefixes.t.b58check_prefix).
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "Commitment_hash" in
let title := "A commitment ID" in
let b58check_prefix := commitment_hash in
let size_value :=
Some Tx_rollup_prefixes.commitment_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 init_module_repr : unit :=
Tx_rollup_prefixes.check_encoding Tx_rollup_prefixes.commitment_hash
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)
|}.
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 init_module_repr : unit :=
Tx_rollup_prefixes.check_encoding Tx_rollup_prefixes.commitment_hash
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).
Definition rpc_arg : RPC_arg.arg t :=
let construct := Data_encoding.Binary.to_string_exn None encoding in
let destruct (str : string) : Pervasives.result t string :=
(fun x_1 ⇒ Option.value_e x_1 "Failed to decode commitment")
(Data_encoding.Binary.of_string_opt encoding str) in
RPC_arg.make (Some "A tx_rollup commitment.") "tx_rollup_commitment"
destruct construct tt.
End Hash.
Module Merkle_hash.
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "Message_result_list_hash" in
let title := "A merklised message result list hash" in
let b58check_prefix :=
Tx_rollup_prefixes.message_result_list_hash.(Tx_rollup_prefixes.t.b58check_prefix)
in
let size_value :=
Some
Tx_rollup_prefixes.message_result_list_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
|}).
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 rpc_arg : RPC_arg.arg t :=
let construct := Data_encoding.Binary.to_string_exn None encoding in
let destruct (str : string) : Pervasives.result t string :=
(fun x_1 ⇒ Option.value_e x_1 "Failed to decode commitment")
(Data_encoding.Binary.of_string_opt encoding str) in
RPC_arg.make (Some "A tx_rollup commitment.") "tx_rollup_commitment"
destruct construct tt.
End Hash.
Module Merkle_hash.
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "Message_result_list_hash" in
let title := "A merklised message result list hash" in
let b58check_prefix :=
Tx_rollup_prefixes.message_result_list_hash.(Tx_rollup_prefixes.t.b58check_prefix)
in
let size_value :=
Some
Tx_rollup_prefixes.message_result_list_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 _Set := H.(S.HASH._Set).
Definition Map := H.(S.HASH.Map).
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 _Set := H.(S.HASH._Set).
Definition Map := H.(S.HASH.Map).
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_module_repr : unit :=
Tx_rollup_prefixes.check_encoding
Tx_rollup_prefixes.message_result_list_hash b58check_encoding.
End Merkle_hash.
Definition Merkle :=
Merkle_list.Make
{|
Merkle_list.S_El.to_bytes := Tx_rollup_message_result_hash_repr.to_bytes
|}
{|
S.HASH.name := Merkle_hash.name;
S.HASH.title := Merkle_hash.title;
S.HASH.pp := Merkle_hash.pp;
S.HASH.pp_short := Merkle_hash.pp_short;
S.HASH.op_eq := Merkle_hash.op_eq;
S.HASH.op_ltgt := Merkle_hash.op_ltgt;
S.HASH.op_lt := Merkle_hash.op_lt;
S.HASH.op_lteq := Merkle_hash.op_lteq;
S.HASH.op_gteq := Merkle_hash.op_gteq;
S.HASH.op_gt := Merkle_hash.op_gt;
S.HASH.compare := Merkle_hash.compare;
S.HASH.equal := Merkle_hash.equal;
S.HASH.max := Merkle_hash.max;
S.HASH.min := Merkle_hash.min;
S.HASH.hash_bytes := Merkle_hash.hash_bytes;
S.HASH.hash_string := Merkle_hash.hash_string;
S.HASH.zero := Merkle_hash.zero;
S.HASH.size_value := Merkle_hash.size_value;
S.HASH.to_bytes := Merkle_hash.to_bytes;
S.HASH.of_bytes_opt := Merkle_hash.of_bytes_opt;
S.HASH.of_bytes_exn := Merkle_hash.of_bytes_exn;
S.HASH.to_b58check := Merkle_hash.to_b58check;
S.HASH.to_short_b58check := Merkle_hash.to_short_b58check;
S.HASH.of_b58check_exn := Merkle_hash.of_b58check_exn;
S.HASH.of_b58check_opt := Merkle_hash.of_b58check_opt;
S.HASH.b58check_encoding := Merkle_hash.b58check_encoding;
S.HASH.encoding := Merkle_hash.encoding;
S.HASH.rpc_arg := Merkle_hash.rpc_arg;
S.HASH._Set := Merkle_hash._Set;
S.HASH.Map := Merkle_hash.Map
|}.
Module template.
Record record {a : Set} : Set := Build {
level : Tx_rollup_level_repr.t;
messages : a;
predecessor : option Hash.t;
inbox_merkle_root : Tx_rollup_inbox_repr.Merkle.root;
}.
Arguments record : clear implicits.
Definition with_level {t_a} level (r : record t_a) :=
Build t_a level r.(messages) r.(predecessor) r.(inbox_merkle_root).
Definition with_messages {t_a} messages (r : record t_a) :=
Build t_a r.(level) messages r.(predecessor) r.(inbox_merkle_root).
Definition with_predecessor {t_a} predecessor (r : record t_a) :=
Build t_a r.(level) r.(messages) predecessor r.(inbox_merkle_root).
Definition with_inbox_merkle_root {t_a} inbox_merkle_root (r : record t_a) :=
Build t_a r.(level) r.(messages) r.(predecessor) inbox_merkle_root.
End template.
Definition template := template.record.
Definition map_template {A B : Set} (f_value : A → B) (x_value : template A)
: template B :=
{| template.level := x_value.(template.level);
template.messages := f_value x_value.(template.messages);
template.predecessor := x_value.(template.predecessor);
template.inbox_merkle_root := x_value.(template.inbox_merkle_root); |}.
Definition pp_template {a : Set}
(pp_messages : Format.formatter → a → unit) (fmt : Format.formatter)
(t_value : template a) : unit :=
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Level: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "Messages: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "Predecessor: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal
"Inbox merkle root: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format)))))))))))
"Level: %a@,Messages: %a@,Predecessor: %a@,Inbox merkle root: %a")
Tx_rollup_level_repr.pp t_value.(template.level) pp_messages
t_value.(template.messages)
(Format.pp_print_option
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.pp_print_string fmt "None")) Hash.pp)
t_value.(template.predecessor) Tx_rollup_inbox_repr.Merkle.pp_root
t_value.(template.inbox_merkle_root).
Definition encoding_template {A : Set} (encoding : Data_encoding.encoding A)
: Data_encoding.encoding (template A) :=
Data_encoding.conv
(fun (function_parameter : template A) ⇒
let '{|
template.level := level;
template.messages := messages;
template.predecessor := predecessor;
template.inbox_merkle_root := inbox_merkle_root
|} := function_parameter in
(level, messages, predecessor, inbox_merkle_root))
(fun (function_parameter :
Tx_rollup_level_repr.t × A × option Hash.t ×
Tx_rollup_inbox_repr.Merkle.root) ⇒
let '(level, messages, predecessor, inbox_merkle_root) :=
function_parameter in
{| template.level := level; template.messages := messages;
template.predecessor := predecessor;
template.inbox_merkle_root := inbox_merkle_root; |}) None
(Data_encoding.obj4
(Data_encoding.req None None "level" Tx_rollup_level_repr.encoding)
(Data_encoding.req None None "messages" encoding)
(Data_encoding.req None None "predecessor"
(Data_encoding.option_value Hash.encoding))
(Data_encoding.req None None "inbox_merkle_root"
Tx_rollup_inbox_repr.Merkle.root_encoding)).
Module Compact.
Module excerpt.
Record record : Set := Build {
count : int;
root : Merkle_hash.H.(S.HASH.t);
last_result_message_hash : Tx_rollup_message_result_hash_repr.t;
}.
Definition with_count count (r : record) :=
Build count r.(root) r.(last_result_message_hash).
Definition with_root root (r : record) :=
Build r.(count) root r.(last_result_message_hash).
Definition with_last_result_message_hash last_result_message_hash
(r : record) :=
Build r.(count) r.(root) last_result_message_hash.
End excerpt.
Definition excerpt := excerpt.record.
Definition t : Set := template excerpt.
Definition pp : Format.formatter → template excerpt → unit :=
pp_template
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : excerpt) ⇒
let '{|
excerpt.count := count;
excerpt.root := root_value;
excerpt.last_result_message_hash := last_result_message_hash
|} := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Count: "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal
" Merkle root hash: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal
"Last result message hash: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))))))
"Count: %d@, Merkle root hash: %a@,Last result message hash: %a")
count Merkle_hash.pp root_value
Tx_rollup_message_result_hash_repr.pp last_result_message_hash).
Definition encoding : Data_encoding.encoding (template excerpt) :=
encoding_template
(Data_encoding.conv
(fun (function_parameter : excerpt) ⇒
let '{|
excerpt.count := count;
excerpt.root := root_value;
excerpt.last_result_message_hash := last_result_message_hash
|} := function_parameter in
(count, root_value, last_result_message_hash))
(fun (function_parameter :
int × Merkle_hash.H.(S.HASH.t) × Tx_rollup_message_result_hash_repr.t)
⇒
let '(count, root_value, last_result_message_hash) :=
function_parameter in
{| excerpt.count := count; excerpt.root := root_value;
excerpt.last_result_message_hash := last_result_message_hash; |})
None
(Data_encoding.obj3
(Data_encoding.req None None "count" Data_encoding.int31)
(Data_encoding.req None None "root" Merkle_hash.encoding)
(Data_encoding.req None None "last_message_result_hash"
Tx_rollup_message_result_hash_repr.encoding))).
Definition hash_value (t_value : template excerpt) : Hash.t :=
let bytes_value := Data_encoding.Binary.to_bytes_exn None encoding t_value
in
Hash.hash_bytes None [ bytes_value ].
End Compact.
Module Full.
Definition t : Set := template (list Tx_rollup_message_result_hash_repr.t).
Definition pp
: Format.formatter →
template (list Tx_rollup_message_result_hash_repr.t) → unit :=
pp_template
(Format.pp_print_list None Tx_rollup_message_result_hash_repr.pp).
Definition encoding : Data_encoding.t t :=
encoding_template
(Data_encoding.list_value None Tx_rollup_message_result_hash_repr.encoding).
Definition compact
(full_value : template (list Tx_rollup_message_result_hash_repr.t))
: template Compact.excerpt :=
map_template
(fun (list_value : list Tx_rollup_message_result_hash_repr.t) ⇒
let root_value := Merkle.(Merkle_list.T.compute) list_value in
(fun (function_parameter : int × Tx_rollup_message_result_hash_repr.t)
⇒
let '(count, last_result_message_hash) := function_parameter in
{| Compact.excerpt.count := count; Compact.excerpt.root := root_value;
Compact.excerpt.last_result_message_hash :=
last_result_message_hash; |})
(List.fold_left
(fun (function_parameter :
int × Tx_rollup_message_result_hash_repr.t) ⇒
let '(acc_value, _) := function_parameter in
fun (m_value : Tx_rollup_message_result_hash_repr.t) ⇒
((acc_value +i 1), m_value))
(0, Tx_rollup_message_result_hash_repr.zero) list_value)) full_value.
End Full.
Module Index.
Definition t : Set := Hash.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 Hash.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 Hash.encoding))
| _ ⇒ return? None
end.
Definition rpc_arg : RPC_arg.arg Hash.t := Hash.rpc_arg.
Definition encoding : Data_encoding.t Hash.t := Hash.encoding.
Definition compare : Hash.t → Hash.t → int := Hash.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 Submitted_commitment.
Module t.
Record record : Set := Build {
commitment : Compact.t;
commitment_hash : Hash.t;
committer : Signature.public_key_hash;
submitted_at : Raw_level_repr.t;
finalized_at : option Raw_level_repr.t;
}.
Definition with_commitment commitment (r : record) :=
Build commitment r.(commitment_hash) r.(committer) r.(submitted_at)
r.(finalized_at).
Definition with_commitment_hash commitment_hash (r : record) :=
Build r.(commitment) commitment_hash r.(committer) r.(submitted_at)
r.(finalized_at).
Definition with_committer committer (r : record) :=
Build r.(commitment) r.(commitment_hash) committer r.(submitted_at)
r.(finalized_at).
Definition with_submitted_at submitted_at (r : record) :=
Build r.(commitment) r.(commitment_hash) r.(committer) submitted_at
r.(finalized_at).
Definition with_finalized_at finalized_at (r : record) :=
Build r.(commitment) r.(commitment_hash) r.(committer) r.(submitted_at)
finalized_at.
End t.
Definition t := t.record.
Definition encoding : Data_encoding.encoding t :=
let compact := Compact.encoding in
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.commitment := commitment;
t.commitment_hash := commitment_hash;
t.committer := committer;
t.submitted_at := submitted_at;
t.finalized_at := finalized_at
|} := function_parameter in
(commitment, commitment_hash, committer, submitted_at, finalized_at))
(fun (function_parameter :
Compact.t × Hash.t × Signature.public_key_hash × Raw_level_repr.t ×
option Raw_level_repr.t) ⇒
let
'(commitment, commitment_hash, committer, submitted_at, finalized_at) :=
function_parameter in
{| t.commitment := commitment; t.commitment_hash := commitment_hash;
t.committer := committer; t.submitted_at := submitted_at;
t.finalized_at := finalized_at; |}) None
(Data_encoding.obj5 (Data_encoding.req None None "commitment" compact)
(Data_encoding.req None None "commitment_hash" Hash.encoding)
(Data_encoding.req None None "committer"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "submitted_at" Raw_level_repr.encoding)
(Data_encoding.opt None None "finalized_at" Raw_level_repr.encoding)).
(* Submitted_commitment *)
Definition module :=
{|
Storage_sigs.VALUE.encoding := encoding
|}.
End Submitted_commitment.
Definition Submitted_commitment := Submitted_commitment.module.
Tx_rollup_prefixes.check_encoding
Tx_rollup_prefixes.message_result_list_hash b58check_encoding.
End Merkle_hash.
Definition Merkle :=
Merkle_list.Make
{|
Merkle_list.S_El.to_bytes := Tx_rollup_message_result_hash_repr.to_bytes
|}
{|
S.HASH.name := Merkle_hash.name;
S.HASH.title := Merkle_hash.title;
S.HASH.pp := Merkle_hash.pp;
S.HASH.pp_short := Merkle_hash.pp_short;
S.HASH.op_eq := Merkle_hash.op_eq;
S.HASH.op_ltgt := Merkle_hash.op_ltgt;
S.HASH.op_lt := Merkle_hash.op_lt;
S.HASH.op_lteq := Merkle_hash.op_lteq;
S.HASH.op_gteq := Merkle_hash.op_gteq;
S.HASH.op_gt := Merkle_hash.op_gt;
S.HASH.compare := Merkle_hash.compare;
S.HASH.equal := Merkle_hash.equal;
S.HASH.max := Merkle_hash.max;
S.HASH.min := Merkle_hash.min;
S.HASH.hash_bytes := Merkle_hash.hash_bytes;
S.HASH.hash_string := Merkle_hash.hash_string;
S.HASH.zero := Merkle_hash.zero;
S.HASH.size_value := Merkle_hash.size_value;
S.HASH.to_bytes := Merkle_hash.to_bytes;
S.HASH.of_bytes_opt := Merkle_hash.of_bytes_opt;
S.HASH.of_bytes_exn := Merkle_hash.of_bytes_exn;
S.HASH.to_b58check := Merkle_hash.to_b58check;
S.HASH.to_short_b58check := Merkle_hash.to_short_b58check;
S.HASH.of_b58check_exn := Merkle_hash.of_b58check_exn;
S.HASH.of_b58check_opt := Merkle_hash.of_b58check_opt;
S.HASH.b58check_encoding := Merkle_hash.b58check_encoding;
S.HASH.encoding := Merkle_hash.encoding;
S.HASH.rpc_arg := Merkle_hash.rpc_arg;
S.HASH._Set := Merkle_hash._Set;
S.HASH.Map := Merkle_hash.Map
|}.
Module template.
Record record {a : Set} : Set := Build {
level : Tx_rollup_level_repr.t;
messages : a;
predecessor : option Hash.t;
inbox_merkle_root : Tx_rollup_inbox_repr.Merkle.root;
}.
Arguments record : clear implicits.
Definition with_level {t_a} level (r : record t_a) :=
Build t_a level r.(messages) r.(predecessor) r.(inbox_merkle_root).
Definition with_messages {t_a} messages (r : record t_a) :=
Build t_a r.(level) messages r.(predecessor) r.(inbox_merkle_root).
Definition with_predecessor {t_a} predecessor (r : record t_a) :=
Build t_a r.(level) r.(messages) predecessor r.(inbox_merkle_root).
Definition with_inbox_merkle_root {t_a} inbox_merkle_root (r : record t_a) :=
Build t_a r.(level) r.(messages) r.(predecessor) inbox_merkle_root.
End template.
Definition template := template.record.
Definition map_template {A B : Set} (f_value : A → B) (x_value : template A)
: template B :=
{| template.level := x_value.(template.level);
template.messages := f_value x_value.(template.messages);
template.predecessor := x_value.(template.predecessor);
template.inbox_merkle_root := x_value.(template.inbox_merkle_root); |}.
Definition pp_template {a : Set}
(pp_messages : Format.formatter → a → unit) (fmt : Format.formatter)
(t_value : template a) : unit :=
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Level: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "Messages: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal "Predecessor: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal
"Inbox merkle root: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format)))))))))))
"Level: %a@,Messages: %a@,Predecessor: %a@,Inbox merkle root: %a")
Tx_rollup_level_repr.pp t_value.(template.level) pp_messages
t_value.(template.messages)
(Format.pp_print_option
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.pp_print_string fmt "None")) Hash.pp)
t_value.(template.predecessor) Tx_rollup_inbox_repr.Merkle.pp_root
t_value.(template.inbox_merkle_root).
Definition encoding_template {A : Set} (encoding : Data_encoding.encoding A)
: Data_encoding.encoding (template A) :=
Data_encoding.conv
(fun (function_parameter : template A) ⇒
let '{|
template.level := level;
template.messages := messages;
template.predecessor := predecessor;
template.inbox_merkle_root := inbox_merkle_root
|} := function_parameter in
(level, messages, predecessor, inbox_merkle_root))
(fun (function_parameter :
Tx_rollup_level_repr.t × A × option Hash.t ×
Tx_rollup_inbox_repr.Merkle.root) ⇒
let '(level, messages, predecessor, inbox_merkle_root) :=
function_parameter in
{| template.level := level; template.messages := messages;
template.predecessor := predecessor;
template.inbox_merkle_root := inbox_merkle_root; |}) None
(Data_encoding.obj4
(Data_encoding.req None None "level" Tx_rollup_level_repr.encoding)
(Data_encoding.req None None "messages" encoding)
(Data_encoding.req None None "predecessor"
(Data_encoding.option_value Hash.encoding))
(Data_encoding.req None None "inbox_merkle_root"
Tx_rollup_inbox_repr.Merkle.root_encoding)).
Module Compact.
Module excerpt.
Record record : Set := Build {
count : int;
root : Merkle_hash.H.(S.HASH.t);
last_result_message_hash : Tx_rollup_message_result_hash_repr.t;
}.
Definition with_count count (r : record) :=
Build count r.(root) r.(last_result_message_hash).
Definition with_root root (r : record) :=
Build r.(count) root r.(last_result_message_hash).
Definition with_last_result_message_hash last_result_message_hash
(r : record) :=
Build r.(count) r.(root) last_result_message_hash.
End excerpt.
Definition excerpt := excerpt.record.
Definition t : Set := template excerpt.
Definition pp : Format.formatter → template excerpt → unit :=
pp_template
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : excerpt) ⇒
let '{|
excerpt.count := count;
excerpt.root := root_value;
excerpt.last_result_message_hash := last_result_message_hash
|} := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Count: "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal
" Merkle root hash: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@," 0 0)
(CamlinternalFormatBasics.String_literal
"Last result message hash: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))))))
"Count: %d@, Merkle root hash: %a@,Last result message hash: %a")
count Merkle_hash.pp root_value
Tx_rollup_message_result_hash_repr.pp last_result_message_hash).
Definition encoding : Data_encoding.encoding (template excerpt) :=
encoding_template
(Data_encoding.conv
(fun (function_parameter : excerpt) ⇒
let '{|
excerpt.count := count;
excerpt.root := root_value;
excerpt.last_result_message_hash := last_result_message_hash
|} := function_parameter in
(count, root_value, last_result_message_hash))
(fun (function_parameter :
int × Merkle_hash.H.(S.HASH.t) × Tx_rollup_message_result_hash_repr.t)
⇒
let '(count, root_value, last_result_message_hash) :=
function_parameter in
{| excerpt.count := count; excerpt.root := root_value;
excerpt.last_result_message_hash := last_result_message_hash; |})
None
(Data_encoding.obj3
(Data_encoding.req None None "count" Data_encoding.int31)
(Data_encoding.req None None "root" Merkle_hash.encoding)
(Data_encoding.req None None "last_message_result_hash"
Tx_rollup_message_result_hash_repr.encoding))).
Definition hash_value (t_value : template excerpt) : Hash.t :=
let bytes_value := Data_encoding.Binary.to_bytes_exn None encoding t_value
in
Hash.hash_bytes None [ bytes_value ].
End Compact.
Module Full.
Definition t : Set := template (list Tx_rollup_message_result_hash_repr.t).
Definition pp
: Format.formatter →
template (list Tx_rollup_message_result_hash_repr.t) → unit :=
pp_template
(Format.pp_print_list None Tx_rollup_message_result_hash_repr.pp).
Definition encoding : Data_encoding.t t :=
encoding_template
(Data_encoding.list_value None Tx_rollup_message_result_hash_repr.encoding).
Definition compact
(full_value : template (list Tx_rollup_message_result_hash_repr.t))
: template Compact.excerpt :=
map_template
(fun (list_value : list Tx_rollup_message_result_hash_repr.t) ⇒
let root_value := Merkle.(Merkle_list.T.compute) list_value in
(fun (function_parameter : int × Tx_rollup_message_result_hash_repr.t)
⇒
let '(count, last_result_message_hash) := function_parameter in
{| Compact.excerpt.count := count; Compact.excerpt.root := root_value;
Compact.excerpt.last_result_message_hash :=
last_result_message_hash; |})
(List.fold_left
(fun (function_parameter :
int × Tx_rollup_message_result_hash_repr.t) ⇒
let '(acc_value, _) := function_parameter in
fun (m_value : Tx_rollup_message_result_hash_repr.t) ⇒
((acc_value +i 1), m_value))
(0, Tx_rollup_message_result_hash_repr.zero) list_value)) full_value.
End Full.
Module Index.
Definition t : Set := Hash.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 Hash.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 Hash.encoding))
| _ ⇒ return? None
end.
Definition rpc_arg : RPC_arg.arg Hash.t := Hash.rpc_arg.
Definition encoding : Data_encoding.t Hash.t := Hash.encoding.
Definition compare : Hash.t → Hash.t → int := Hash.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 Submitted_commitment.
Module t.
Record record : Set := Build {
commitment : Compact.t;
commitment_hash : Hash.t;
committer : Signature.public_key_hash;
submitted_at : Raw_level_repr.t;
finalized_at : option Raw_level_repr.t;
}.
Definition with_commitment commitment (r : record) :=
Build commitment r.(commitment_hash) r.(committer) r.(submitted_at)
r.(finalized_at).
Definition with_commitment_hash commitment_hash (r : record) :=
Build r.(commitment) commitment_hash r.(committer) r.(submitted_at)
r.(finalized_at).
Definition with_committer committer (r : record) :=
Build r.(commitment) r.(commitment_hash) committer r.(submitted_at)
r.(finalized_at).
Definition with_submitted_at submitted_at (r : record) :=
Build r.(commitment) r.(commitment_hash) r.(committer) submitted_at
r.(finalized_at).
Definition with_finalized_at finalized_at (r : record) :=
Build r.(commitment) r.(commitment_hash) r.(committer) r.(submitted_at)
finalized_at.
End t.
Definition t := t.record.
Definition encoding : Data_encoding.encoding t :=
let compact := Compact.encoding in
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.commitment := commitment;
t.commitment_hash := commitment_hash;
t.committer := committer;
t.submitted_at := submitted_at;
t.finalized_at := finalized_at
|} := function_parameter in
(commitment, commitment_hash, committer, submitted_at, finalized_at))
(fun (function_parameter :
Compact.t × Hash.t × Signature.public_key_hash × Raw_level_repr.t ×
option Raw_level_repr.t) ⇒
let
'(commitment, commitment_hash, committer, submitted_at, finalized_at) :=
function_parameter in
{| t.commitment := commitment; t.commitment_hash := commitment_hash;
t.committer := committer; t.submitted_at := submitted_at;
t.finalized_at := finalized_at; |}) None
(Data_encoding.obj5 (Data_encoding.req None None "commitment" compact)
(Data_encoding.req None None "commitment_hash" Hash.encoding)
(Data_encoding.req None None "committer"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "submitted_at" Raw_level_repr.encoding)
(Data_encoding.opt None None "finalized_at" Raw_level_repr.encoding)).
(* Submitted_commitment *)
Definition module :=
{|
Storage_sigs.VALUE.encoding := encoding
|}.
End Submitted_commitment.
Definition Submitted_commitment := Submitted_commitment.module.