🐆 Tx_rollup_message_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.V8.
Require TezosOfOCaml.Proto_alpha.Ticket_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_address.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_qty.

Module deposit.
  Record record : Set := Build {
    sender : Signature.public_key_hash;
    destination : Tx_rollup_l2_address.Indexable.value;
    ticket_hash : Ticket_hash_repr.t;
    amount : Tx_rollup_l2_qty.t;
  }.
  Definition with_sender sender (r : record) :=
    Build sender r.(destination) r.(ticket_hash) r.(amount).
  Definition with_destination destination (r : record) :=
    Build r.(sender) destination r.(ticket_hash) r.(amount).
  Definition with_ticket_hash ticket_hash (r : record) :=
    Build r.(sender) r.(destination) ticket_hash r.(amount).
  Definition with_amount amount (r : record) :=
    Build r.(sender) r.(destination) r.(ticket_hash) amount.
End deposit.
Definition deposit := deposit.record.

Definition deposit_encoding : Data_encoding.encoding deposit :=
  Data_encoding.conv
    (fun (function_parameter : deposit) ⇒
      let '{|
        deposit.sender := sender;
          deposit.destination := destination;
          deposit.ticket_hash := ticket_hash;
          deposit.amount := amount
          |} := function_parameter in
      (sender, destination, ticket_hash, amount))
    (fun (function_parameter :
      Signature.public_key_hash × Tx_rollup_l2_address.Indexable.value ×
        Ticket_hash_repr.t × Tx_rollup_l2_qty.t) ⇒
      let '(sender, destination, ticket_hash, amount) := function_parameter in
      {| deposit.sender := sender; deposit.destination := destination;
        deposit.ticket_hash := ticket_hash; deposit.amount := amount; |}) None
    (Data_encoding.obj4
      (Data_encoding.req None None "sender"
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
      (Data_encoding.req None None "destination"
        Tx_rollup_l2_address.Indexable.value_encoding)
      (Data_encoding.req None None "ticket_hash" Ticket_hash_repr.encoding)
      (Data_encoding.req None None "amount" Tx_rollup_l2_qty.encoding)).

Inductive t : Set :=
| Batch : string → t
| Deposit : deposit → t.

Definition encoding : Data_encoding.encoding t :=
  Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
    [
      Data_encoding.case_value "Batch" None (Data_encoding.Tag 0)
        (Data_encoding.obj1
          (Data_encoding.req None None "batch"
            (Data_encoding.string' None Data_encoding.Hex)))
        (fun (function_parameter : t) ⇒
          match function_parameter with
          | Batch batch ⇒ Some batch
          | _ ⇒ None
          end) (fun (batch : string) ⇒ Batch batch);
      Data_encoding.case_value "Deposit" None (Data_encoding.Tag 1)
        (Data_encoding.obj1
          (Data_encoding.req None None "deposit" deposit_encoding))
        (fun (function_parameter : t) ⇒
          match function_parameter with
          | Deposit deposit ⇒ Some deposit
          | _ ⇒ None
          end) (fun (deposit : deposit) ⇒ Deposit deposit)
    ].

Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
  match function_parameter with
  | Batch str ⇒
    let subsize := 10 in
    let '(str, ellipsis) :=
      if subsize <i (String.length str) then
        let substring := String.sub str 0 subsize in
        (substring, "...")
      else
        (str, "") in
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.Formatting_gen
          (CamlinternalFormatBasics.Open_box
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "<hov 2>"
                CamlinternalFormatBasics.End_of_format) "<hov 2>"))
          (CamlinternalFormatBasics.String_literal "Batch:"
            (CamlinternalFormatBasics.Formatting_lit
              (CamlinternalFormatBasics.Break "@ " 1 0)
              (CamlinternalFormatBasics.String
                CamlinternalFormatBasics.No_padding
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  (CamlinternalFormatBasics.Formatting_lit
                    CamlinternalFormatBasics.Close_box
                    CamlinternalFormatBasics.End_of_format))))))
        "@[<hov 2>Batch:@ %s%s@]") (Hex.show (Hex.of_string None str)) ellipsis
  |
    Deposit {|
      deposit.sender := sender;
        deposit.destination := destination;
        deposit.ticket_hash := ticket_hash;
        deposit.amount := amount
        |} ⇒
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.Formatting_gen
          (CamlinternalFormatBasics.Open_box
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "<hov 2>"
                CamlinternalFormatBasics.End_of_format) "<hov 2>"))
          (CamlinternalFormatBasics.String_literal "Deposit:"
            (CamlinternalFormatBasics.Formatting_lit
              (CamlinternalFormatBasics.Break "@ " 1 0)
              (CamlinternalFormatBasics.String_literal "sender="
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.Char_literal "," % char
                    (CamlinternalFormatBasics.Formatting_lit
                      (CamlinternalFormatBasics.Break "@ " 1 0)
                      (CamlinternalFormatBasics.String_literal "destination="
                        (CamlinternalFormatBasics.Alpha
                          (CamlinternalFormatBasics.Char_literal "," % char
                            (CamlinternalFormatBasics.Formatting_lit
                              (CamlinternalFormatBasics.Break "@ " 1 0)
                              (CamlinternalFormatBasics.String_literal
                                "ticket_hash="
                                (CamlinternalFormatBasics.Alpha
                                  (CamlinternalFormatBasics.Char_literal
                                    "," % char
                                    (CamlinternalFormatBasics.Formatting_lit
                                      (CamlinternalFormatBasics.Break "@ " 1 0)
                                      (CamlinternalFormatBasics.String_literal
                                        "amount:"
                                        (CamlinternalFormatBasics.Alpha
                                          (CamlinternalFormatBasics.Formatting_lit
                                            CamlinternalFormatBasics.Close_box
                                            CamlinternalFormatBasics.End_of_format))))))))))))))))))
        "@[<hov 2>Deposit:@ sender=%a,@ destination=%a,@ ticket_hash=%a,@ amount:%a@]")
      Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) sender
      Tx_rollup_l2_address.Indexable.pp destination Ticket_hash_repr.pp
      ticket_hash Tx_rollup_l2_qty.pp amount
  end.

Definition size_value (function_parameter : t) : int :=
  match function_parameter with
  | Batch batch ⇒ String.length batch
  |
    Deposit {|
      deposit.sender := _;
        deposit.destination := d_value;
        deposit.ticket_hash := _;
        deposit.amount := _
        |} ⇒
    let sender_size :=
      Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.size_value) in
    let destination_size := Tx_rollup_l2_address.Indexable.size_value d_value in
    let key_hash_size := 32 in
    let amount_size := 8 in
    ((sender_size +i destination_size) +i key_hash_size) +i amount_size
  end.