🐆 Tx_rollup_inbox_repr.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V7.
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.