Skip to main content

🐆 Tx_rollup_commitment_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.Proto_alpha.Environment.
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)
      |}.

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_1Option.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)
      |}.

Inclusion of the module [Path_encoding_Make_hex_include]
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 "commitment "
        (CamlinternalFormatBasics.Alpha
          (CamlinternalFormatBasics.String_literal " : messages = "
            (CamlinternalFormatBasics.Alpha
              (CamlinternalFormatBasics.String_literal " predecessor "
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.String_literal
                    " for inbox with merkle root "
                    (CamlinternalFormatBasics.Alpha
                      CamlinternalFormatBasics.End_of_format))))))))
      "commitment %a : messages = %a predecessor %a for inbox with merkle root %a")
    Tx_rollup_level_repr.pp t_value.(template.level) pp_messages
    t_value.(template.messages) (Format.pp_print_option 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.String_literal ", root: "
                    (CamlinternalFormatBasics.Alpha
                      (CamlinternalFormatBasics.String_literal
                        ", last_result_message_hash: "
                        (CamlinternalFormatBasics.Alpha
                          CamlinternalFormatBasics.End_of_format))))))
              "count: %d, root: %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
      ((let arg :=
        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; |})
        in
      fun (eta :
        Data_encoding.encoding
          (int × Merkle_hash.H.(S.HASH.t) × Tx_rollup_message_result_hash_repr.t))
        ⇒ arg None eta)
        (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 : int := 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) : option Hash.t :=
    match function_parameter with
    | cons key_value []
      Option.bind (Hex.to_bytes (Hex.Hex key_value))
        (Data_encoding.Binary.of_bytes_opt Hash.encoding)
    | _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.