Skip to main content

🐆 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.Proto_alpha.Environment.
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 :=
  (let arg :=
    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; |}) in
  fun (eta :
    Data_encoding.encoding
      (Signature.public_key_hash × Tx_rollup_l2_address.Indexable.value ×
        Ticket_hash_repr.t × Tx_rollup_l2_qty.t)) ⇒ arg None eta)
    (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)).

Definition batch_encoding : Data_encoding.encoding string :=
  let json_value :=
    Data_encoding.conv Bytes.of_string Bytes.to_string None
      Data_encoding.bytes_value in
  Data_encoding.splitted json_value Data_encoding.string_value.

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" batch_encoding))
        (fun (function_parameter : t) ⇒
          match function_parameter with
          | Batch batchSome 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 depositSome deposit
          | _None
          end) (fun (deposit : deposit) ⇒ Deposit deposit)
    ].

Axiom pp : Format.formatter t unit.

Definition size_value (function_parameter : t) : int :=
  match function_parameter with
  | Batch batchString.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.