🐆 Tx_rollup_inbox_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.Tx_rollup_message_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_prefixes.
Module El.
Definition t : Set := Tx_rollup_message_hash_repr.t.
Definition to_bytes : Tx_rollup_message_hash_repr.t → bytes :=
Data_encoding.Binary.to_bytes_exn None Tx_rollup_message_hash_repr.encoding.
(* El *)
Definition module :=
{|
Merkle_list.S_El.to_bytes := to_bytes
|}.
End El.
Definition El := El.module.
Module Prefix.
Definition name : string := "Inbox_list_hash".
Definition title : string := "A merkle root hash for inboxes".
Definition b58check_prefix : string :=
Tx_rollup_prefixes.inbox_list_hash.(Tx_rollup_prefixes.t.b58check_prefix).
Definition size_value : option int :=
Some Tx_rollup_prefixes.inbox_list_hash.(Tx_rollup_prefixes.t.hash_size).
(* Prefix *)
Definition module :=
{|
Blake2B.PrefixedName.name := name;
Blake2B.PrefixedName.title := title;
Blake2B.PrefixedName.b58check_prefix := b58check_prefix;
Blake2B.PrefixedName.size_value := size_value
|}.
End Prefix.
Definition Prefix := Prefix.module.
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|} Prefix.
Definition Merkle_list := Merkle_list.Make El H.
Module Merkle.
Definition tree : Set := Merkle_list.(Merkle_list.T.t).
Definition root : Set := Merkle_list.(Merkle_list.T.h).
Definition path : Set := Merkle_list.(Merkle_list.T.path).
Definition empty : Merkle_list.(Merkle_list.T.t) :=
Merkle_list.(Merkle_list.T.nil).
Definition root_value
: Merkle_list.(Merkle_list.T.t) → Merkle_list.(Merkle_list.T.h) :=
Merkle_list.(Merkle_list.T.root_value).
Definition op_eq : H.(S.HASH.t) → H.(S.HASH.t) → bool := H.(S.HASH.op_eq).
Definition compare : H.(S.HASH.t) → H.(S.HASH.t) → int :=
H.(S.HASH.compare).
Definition root_encoding : Data_encoding.t H.(S.HASH.t) :=
H.(S.HASH.encoding).
Definition root_of_b58check_opt : string → option H.(S.HASH.t) :=
H.(S.HASH.of_b58check_opt).
Definition pp_root : Format.formatter → H.(S.HASH.t) → unit :=
H.(S.HASH.pp).
Definition path_encoding : Data_encoding.t Merkle_list.(Merkle_list.T.path) :=
Merkle_list.(Merkle_list.T.path_encoding).
Definition add_message
: Merkle_list.(Merkle_list.T.t) → Tx_rollup_message_hash_repr.t →
Merkle_list.(Merkle_list.T.t) := Merkle_list.(Merkle_list.T.snoc).
Definition tree_of_messages
: list Tx_rollup_message_hash_repr.t → Merkle_list.(Merkle_list.T.t) :=
List.fold_left Merkle_list.(Merkle_list.T.snoc)
Merkle_list.(Merkle_list.T.nil).
Definition compute_path
(messages : list Tx_rollup_message_hash_repr.t) (position : int)
: M? Merkle_list.(Merkle_list.T.path) :=
let tree_value := tree_of_messages messages in
Merkle_list.(Merkle_list.T.compute_path) tree_value position.
Definition check_path
: Merkle_list.(Merkle_list.T.path) → int →
Tx_rollup_message_hash_repr.t → Merkle_list.(Merkle_list.T.h) → M? bool :=
Merkle_list.(Merkle_list.T.check_path).
Definition path_depth : Merkle_list.(Merkle_list.T.path) → int :=
Merkle_list.(Merkle_list.T.path_depth).
Definition merklize_list (messages : list Tx_rollup_message_hash_repr.t)
: Merkle_list.(Merkle_list.T.h) :=
let tree_value := tree_of_messages messages in
root_value tree_value.
End Merkle.
Module t.
Record record : Set := Build {
inbox_length : int;
cumulated_size : int;
merkle_root : Merkle.root;
}.
Definition with_inbox_length inbox_length (r : record) :=
Build inbox_length r.(cumulated_size) r.(merkle_root).
Definition with_cumulated_size cumulated_size (r : record) :=
Build r.(inbox_length) cumulated_size r.(merkle_root).
Definition with_merkle_root merkle_root (r : record) :=
Build r.(inbox_length) r.(cumulated_size) merkle_root.
End t.
Definition t := t.record.
Definition op_eq (function_parameter : t) : t → bool :=
let '{|
t.inbox_length := inbox_length_left;
t.cumulated_size := cumulated_size_left;
t.merkle_root := merkle_root_left
|} := function_parameter in
fun (function_parameter : t) ⇒
let '{|
t.inbox_length := inbox_length_right;
t.cumulated_size := cumulated_size_right;
t.merkle_root := merkle_root_right
|} := function_parameter in
(inbox_length_left =i inbox_length_right) &&
((cumulated_size_left =i cumulated_size_right) &&
(Merkle.op_eq merkle_root_left merkle_root_right)).
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.inbox_length := inbox_length;
t.cumulated_size := cumulated_size;
t.merkle_root := merkle_root
|} := function_parameter in
(inbox_length, cumulated_size, merkle_root))
(fun (function_parameter : int × int × Merkle.root) ⇒
let '(inbox_length, cumulated_size, merkle_root) := function_parameter in
{| t.inbox_length := inbox_length; t.cumulated_size := cumulated_size;
t.merkle_root := merkle_root; |}) None
(Data_encoding.obj3
(Data_encoding.req None None "inbox_length" Data_encoding.int31)
(Data_encoding.req None None "cumulated_size" Data_encoding.int31)
(Data_encoding.req None None "merkle_root" Merkle.root_encoding)).
Definition empty : t :=
{| t.inbox_length := 0; t.cumulated_size := 0;
t.merkle_root := Merkle_list.(Merkle_list.T.empty); |}.
Definition size_value : Z.t :=
Z.of_int (Data_encoding.Binary.length encoding empty).
Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
let '{|
t.inbox_length := inbox_length;
t.cumulated_size := cumulated_size;
t.merkle_root := merkle_root
|} := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Inbox with length "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal ", size "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal ", merkle root "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))))
"Inbox with length %d, size %d, merkle root %a") inbox_length
cumulated_size Merkle.pp_root merkle_root.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Merkle_list.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_prefixes.
Module El.
Definition t : Set := Tx_rollup_message_hash_repr.t.
Definition to_bytes : Tx_rollup_message_hash_repr.t → bytes :=
Data_encoding.Binary.to_bytes_exn None Tx_rollup_message_hash_repr.encoding.
(* El *)
Definition module :=
{|
Merkle_list.S_El.to_bytes := to_bytes
|}.
End El.
Definition El := El.module.
Module Prefix.
Definition name : string := "Inbox_list_hash".
Definition title : string := "A merkle root hash for inboxes".
Definition b58check_prefix : string :=
Tx_rollup_prefixes.inbox_list_hash.(Tx_rollup_prefixes.t.b58check_prefix).
Definition size_value : option int :=
Some Tx_rollup_prefixes.inbox_list_hash.(Tx_rollup_prefixes.t.hash_size).
(* Prefix *)
Definition module :=
{|
Blake2B.PrefixedName.name := name;
Blake2B.PrefixedName.title := title;
Blake2B.PrefixedName.b58check_prefix := b58check_prefix;
Blake2B.PrefixedName.size_value := size_value
|}.
End Prefix.
Definition Prefix := Prefix.module.
Definition H :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|} Prefix.
Definition Merkle_list := Merkle_list.Make El H.
Module Merkle.
Definition tree : Set := Merkle_list.(Merkle_list.T.t).
Definition root : Set := Merkle_list.(Merkle_list.T.h).
Definition path : Set := Merkle_list.(Merkle_list.T.path).
Definition empty : Merkle_list.(Merkle_list.T.t) :=
Merkle_list.(Merkle_list.T.nil).
Definition root_value
: Merkle_list.(Merkle_list.T.t) → Merkle_list.(Merkle_list.T.h) :=
Merkle_list.(Merkle_list.T.root_value).
Definition op_eq : H.(S.HASH.t) → H.(S.HASH.t) → bool := H.(S.HASH.op_eq).
Definition compare : H.(S.HASH.t) → H.(S.HASH.t) → int :=
H.(S.HASH.compare).
Definition root_encoding : Data_encoding.t H.(S.HASH.t) :=
H.(S.HASH.encoding).
Definition root_of_b58check_opt : string → option H.(S.HASH.t) :=
H.(S.HASH.of_b58check_opt).
Definition pp_root : Format.formatter → H.(S.HASH.t) → unit :=
H.(S.HASH.pp).
Definition path_encoding : Data_encoding.t Merkle_list.(Merkle_list.T.path) :=
Merkle_list.(Merkle_list.T.path_encoding).
Definition add_message
: Merkle_list.(Merkle_list.T.t) → Tx_rollup_message_hash_repr.t →
Merkle_list.(Merkle_list.T.t) := Merkle_list.(Merkle_list.T.snoc).
Definition tree_of_messages
: list Tx_rollup_message_hash_repr.t → Merkle_list.(Merkle_list.T.t) :=
List.fold_left Merkle_list.(Merkle_list.T.snoc)
Merkle_list.(Merkle_list.T.nil).
Definition compute_path
(messages : list Tx_rollup_message_hash_repr.t) (position : int)
: M? Merkle_list.(Merkle_list.T.path) :=
let tree_value := tree_of_messages messages in
Merkle_list.(Merkle_list.T.compute_path) tree_value position.
Definition check_path
: Merkle_list.(Merkle_list.T.path) → int →
Tx_rollup_message_hash_repr.t → Merkle_list.(Merkle_list.T.h) → M? bool :=
Merkle_list.(Merkle_list.T.check_path).
Definition path_depth : Merkle_list.(Merkle_list.T.path) → int :=
Merkle_list.(Merkle_list.T.path_depth).
Definition merklize_list (messages : list Tx_rollup_message_hash_repr.t)
: Merkle_list.(Merkle_list.T.h) :=
let tree_value := tree_of_messages messages in
root_value tree_value.
End Merkle.
Module t.
Record record : Set := Build {
inbox_length : int;
cumulated_size : int;
merkle_root : Merkle.root;
}.
Definition with_inbox_length inbox_length (r : record) :=
Build inbox_length r.(cumulated_size) r.(merkle_root).
Definition with_cumulated_size cumulated_size (r : record) :=
Build r.(inbox_length) cumulated_size r.(merkle_root).
Definition with_merkle_root merkle_root (r : record) :=
Build r.(inbox_length) r.(cumulated_size) merkle_root.
End t.
Definition t := t.record.
Definition op_eq (function_parameter : t) : t → bool :=
let '{|
t.inbox_length := inbox_length_left;
t.cumulated_size := cumulated_size_left;
t.merkle_root := merkle_root_left
|} := function_parameter in
fun (function_parameter : t) ⇒
let '{|
t.inbox_length := inbox_length_right;
t.cumulated_size := cumulated_size_right;
t.merkle_root := merkle_root_right
|} := function_parameter in
(inbox_length_left =i inbox_length_right) &&
((cumulated_size_left =i cumulated_size_right) &&
(Merkle.op_eq merkle_root_left merkle_root_right)).
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.inbox_length := inbox_length;
t.cumulated_size := cumulated_size;
t.merkle_root := merkle_root
|} := function_parameter in
(inbox_length, cumulated_size, merkle_root))
(fun (function_parameter : int × int × Merkle.root) ⇒
let '(inbox_length, cumulated_size, merkle_root) := function_parameter in
{| t.inbox_length := inbox_length; t.cumulated_size := cumulated_size;
t.merkle_root := merkle_root; |}) None
(Data_encoding.obj3
(Data_encoding.req None None "inbox_length" Data_encoding.int31)
(Data_encoding.req None None "cumulated_size" Data_encoding.int31)
(Data_encoding.req None None "merkle_root" Merkle.root_encoding)).
Definition empty : t :=
{| t.inbox_length := 0; t.cumulated_size := 0;
t.merkle_root := Merkle_list.(Merkle_list.T.empty); |}.
Definition size_value : Z.t :=
Z.of_int (Data_encoding.Binary.length encoding empty).
Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
let '{|
t.inbox_length := inbox_length;
t.cumulated_size := cumulated_size;
t.merkle_root := merkle_root
|} := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Inbox with length "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal ", size "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal ", merkle root "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))))
"Inbox with length %d, size %d, merkle root %a") inbox_length
cumulated_size Merkle.pp_root merkle_root.