Skip to main content

🐆 Tx_rollup_l2_batch.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.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Indexable.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_address.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_context_sig.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_qty.

Definition tag_size : Variant.t := Variant.Build "Uint8" unit tt.

Inductive signer : Set :=
| Bls_pk : Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) signer
| L2_addr : Tx_rollup_l2_address.t signer.

Definition Signer_indexable :=
  Indexable.Make
    (let t : Set := signer in
    let pp (fmt : Format.formatter) (function_parameter : signer) : unit :=
      match function_parameter with
      | Bls_pk _Format.pp_print_string fmt "<bls_signature>"
      | L2_addr addrTx_rollup_l2_address.pp fmt addr
      end in
    let compare (x_value : signer) (y_value : signer) : int :=
      match (x_value, y_value) with
      | (Bls_pk pk1, Bls_pk pk2)
        Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.compare) pk1 pk2
      | (L2_addr addr1, L2_addr addr2)
        Tx_rollup_l2_address.compare addr1 addr2
      | (L2_addr _, Bls_pk _) ⇒ (-1)
      | (Bls_pk _, L2_addr _) ⇒ 1
      end in
    let encoding :=
      Data_encoding.union None
        [
          Data_encoding.case_value "bls_pk" None (Data_encoding.Tag 0)
            Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding)
            (fun (function_parameter : signer) ⇒
              match function_parameter with
              | Bls_pk pkSome pk
              | _None
              end)
            (fun (pk : Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t)) ⇒
              Bls_pk pk);
          Data_encoding.case_value "l2_addr" None (Data_encoding.Tag 1)
            Tx_rollup_l2_address.encoding
            (fun (function_parameter : signer) ⇒
              match function_parameter with
              | L2_addr addrSome addr
              | _None
              end)
            (fun (addr : Tx_rollup_l2_address.t) ⇒ L2_addr addr)
        ] in
    {|
      Indexable.VALUE.encoding := encoding;
      Indexable.VALUE.compare := compare;
      Indexable.VALUE.pp := pp
    |}).

Module V1.
Records for the constructor parameters
  Module ConstructorRecords_operation_content.
    Module operation_content.
      Module Withdraw.
        Record record {destination ticket_hash qty : Set} : Set := Build {
          destination : destination;
          ticket_hash : ticket_hash;
          qty : qty;
        }.
        Arguments record : clear implicits.
        Definition with_destination {t_destination t_ticket_hash t_qty}
          destination (r : record t_destination t_ticket_hash t_qty) :=
          Build t_destination t_ticket_hash t_qty destination r.(ticket_hash)
            r.(qty).
        Definition with_ticket_hash {t_destination t_ticket_hash t_qty}
          ticket_hash (r : record t_destination t_ticket_hash t_qty) :=
          Build t_destination t_ticket_hash t_qty r.(destination) ticket_hash
            r.(qty).
        Definition with_qty {t_destination t_ticket_hash t_qty} qty
          (r : record t_destination t_ticket_hash t_qty) :=
          Build t_destination t_ticket_hash t_qty r.(destination)
            r.(ticket_hash) qty.
      End Withdraw.
      Definition Withdraw_skeleton := Withdraw.record.

      Module Transfer.
        Record record {destination ticket_hash qty : Set} : Set := Build {
          destination : destination;
          ticket_hash : ticket_hash;
          qty : qty;
        }.
        Arguments record : clear implicits.
        Definition with_destination {t_destination t_ticket_hash t_qty}
          destination (r : record t_destination t_ticket_hash t_qty) :=
          Build t_destination t_ticket_hash t_qty destination r.(ticket_hash)
            r.(qty).
        Definition with_ticket_hash {t_destination t_ticket_hash t_qty}
          ticket_hash (r : record t_destination t_ticket_hash t_qty) :=
          Build t_destination t_ticket_hash t_qty r.(destination) ticket_hash
            r.(qty).
        Definition with_qty {t_destination t_ticket_hash t_qty} qty
          (r : record t_destination t_ticket_hash t_qty) :=
          Build t_destination t_ticket_hash t_qty r.(destination)
            r.(ticket_hash) qty.
      End Transfer.
      Definition Transfer_skeleton := Transfer.record.
    End operation_content.
  End ConstructorRecords_operation_content.
  Import ConstructorRecords_operation_content.

  Reserved Notation "'operation_content.Withdraw".
  Reserved Notation "'operation_content.Transfer".

  Inductive operation_content : Set :=
  | Withdraw : 'operation_content.Withdraw operation_content
  | Transfer : 'operation_content.Transfer operation_content
  
  where "'operation_content.Withdraw" :=
    (operation_content.Withdraw_skeleton Signature.public_key_hash
      Alpha_context.Ticket_hash.t Tx_rollup_l2_qty.t)
  and "'operation_content.Transfer" :=
    (operation_content.Transfer_skeleton Tx_rollup_l2_address.Indexable.t
      Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.t)
      Tx_rollup_l2_qty.t).

  Module operation_content.
    Include ConstructorRecords_operation_content.operation_content.
    Definition Withdraw := 'operation_content.Withdraw.
    Definition Transfer := 'operation_content.Transfer.
  End operation_content.

  Module operation.
    Record record : Set := Build {
      signer : Signer_indexable.(Indexable.INDEXABLE.t);
      counter : int64;
      contents : list operation_content;
    }.
    Definition with_signer signer (r : record) :=
      Build signer r.(counter) r.(contents).
    Definition with_counter counter (r : record) :=
      Build r.(signer) counter r.(contents).
    Definition with_contents contents (r : record) :=
      Build r.(signer) r.(counter) contents.
  End operation.
  Definition operation := operation.record.

  Definition transaction : Set := list operation.

  Definition signature : Set := Bls.t.

  Module t.
    Record record : Set := Build {
      contents : list transaction;
      aggregated_signature : signature;
    }.
    Definition with_contents contents (r : record) :=
      Build contents r.(aggregated_signature).
    Definition with_aggregated_signature aggregated_signature (r : record) :=
      Build r.(contents) aggregated_signature.
  End t.
  Definition t := t.record.

  Definition compact_operation_content
    : Data_encoding.Compact.t operation_content :=
    Data_encoding.Compact.union None None
      [
        Data_encoding.Compact.case_value "withdraw" None
          (Data_encoding.Compact.obj3
            (Data_encoding.Compact.req "destination"
              (Data_encoding.Compact.payload
                Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
            (Data_encoding.Compact.req "ticket_hash"
              (Data_encoding.Compact.payload
                Alpha_context.Ticket_hash.encoding))
            (Data_encoding.Compact.req "qty"
              Tx_rollup_l2_qty.compact_encoding))
          (fun (function_parameter : operation_content) ⇒
            match function_parameter with
            |
              Withdraw {|
                operation_content.Withdraw.destination := destination;
                  operation_content.Withdraw.ticket_hash :=
                    ticket_hash;
                  operation_content.Withdraw.qty := qty
                  |} ⇒ Some (destination, ticket_hash, qty)
            | _None
            end)
          (fun (function_parameter :
            Signature.public_key_hash × Alpha_context.Ticket_hash.t ×
              Tx_rollup_l2_qty.t) ⇒
            let '(destination, ticket_hash, qty) := function_parameter
              in
            Withdraw
              {|
                operation_content.Withdraw.destination :=
                  destination;
                operation_content.Withdraw.ticket_hash :=
                  ticket_hash;
                operation_content.Withdraw.qty := qty; |});
        Data_encoding.Compact.case_value "transfer" None
          (Data_encoding.Compact.obj3
            (Data_encoding.Compact.req "destination"
              (Indexable.compact Tx_rollup_l2_address.encoding))
            (Data_encoding.Compact.req "ticket_hash"
              Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.compact))
            (Data_encoding.Compact.req "qty"
              Tx_rollup_l2_qty.compact_encoding))
          (fun (function_parameter : operation_content) ⇒
            match function_parameter with
            |
              Transfer {|
                operation_content.Transfer.destination := destination;
                  operation_content.Transfer.ticket_hash :=
                    ticket_hash;
                  operation_content.Transfer.qty := qty
                  |} ⇒ Some (destination, ticket_hash, qty)
            | _None
            end)
          (fun (function_parameter :
            Indexable.t Tx_rollup_l2_address.t ×
              Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.either)
              × Tx_rollup_l2_qty.t) ⇒
            let '(destination, ticket_hash, qty) := function_parameter
              in
            Transfer
              {|
                operation_content.Transfer.destination :=
                  destination;
                operation_content.Transfer.ticket_hash :=
                  ticket_hash;
                operation_content.Transfer.qty := qty; |})
      ].

  Definition operation_content_encoding
    : Data_encoding.encoding operation_content :=
    Data_encoding.Compact.make (Some tag_size) compact_operation_content.

  Definition compact_operation_raw
    (encoding_signer :
      Data_encoding.Compact.t Signer_indexable.(Indexable.INDEXABLE.t))
    : Data_encoding.Compact.t operation :=
    Data_encoding.Compact.conv None
      (fun (function_parameter : operation) ⇒
        let '{|
          operation.signer := signer;
            operation.counter := counter;
            operation.contents := contents
            |} := function_parameter in
        (signer, counter, contents))
      (fun (function_parameter :
        Signer_indexable.(Indexable.INDEXABLE.t) × int64 ×
          list operation_content) ⇒
        let '(signer, counter, contents) := function_parameter in
        {| operation.signer := signer; operation.counter := counter;
          operation.contents := contents; |})
      (Data_encoding.Compact.obj3
        (Data_encoding.Compact.req "signer" encoding_signer)
        (Data_encoding.Compact.req "counter" Data_encoding.Compact.int64_value)
        (Data_encoding.Compact.req "contents"
          (Data_encoding.Compact.list_value 4 operation_content_encoding))).

  Definition operation_encoding_raw
    (encoding_signer :
      Data_encoding.Compact.t Signer_indexable.(Indexable.INDEXABLE.t))
    : Data_encoding.encoding operation :=
    Data_encoding.Compact.make (Some tag_size)
      (compact_operation_raw encoding_signer).

  Definition compact_transaction_raw
    (encoding_signer :
      Data_encoding.Compact.t Signer_indexable.(Indexable.INDEXABLE.t))
    : Data_encoding.Compact.t (list operation) :=
    Data_encoding.Compact.list_value 8 (operation_encoding_raw encoding_signer).

  Definition transaction_encoding_raw
    (encoding_signer :
      Data_encoding.Compact.t Signer_indexable.(Indexable.INDEXABLE.t))
    : Data_encoding.t transaction :=
    Data_encoding.Compact.make (Some tag_size)
      (compact_transaction_raw encoding_signer).

  Definition compact_signer_index
    : Data_encoding.Compact.t (Indexable.index signer) :=
    Data_encoding.Compact.conv None Indexable.to_int32 Indexable.index_exn
      Data_encoding.Compact.int32_value.

  Definition compact_signer_either
    : Data_encoding.Compact.t Signer_indexable.(Indexable.INDEXABLE.either) :=
    Signer_indexable.(Indexable.INDEXABLE.compact).

  Definition compact_operation : Data_encoding.Compact.t operation :=
    compact_operation_raw compact_signer_either.

  Definition compact_transaction_signer_index
    : Data_encoding.Compact.t (list operation) :=
    compact_transaction_raw compact_signer_index.

  Definition compact_transaction : Data_encoding.Compact.t (list operation) :=
    compact_transaction_raw compact_signer_either.

  Definition transaction_encoding : Data_encoding.t transaction :=
    transaction_encoding_raw compact_signer_either.

  Definition compact (bits : int) : Data_encoding.Compact.t t :=
    Data_encoding.Compact.conv None
      (fun (function_parameter : t) ⇒
        let '{|
          t.contents := contents;
            t.aggregated_signature := aggregated_signature
            |} := function_parameter in
        (aggregated_signature, contents))
      (fun (function_parameter : signature × list transaction) ⇒
        let '(aggregated_signature, contents) := function_parameter in
        {| t.contents := contents;
          t.aggregated_signature := aggregated_signature; |})
      (Data_encoding.Compact.obj2
        (Data_encoding.Compact.req "aggregated_signature"
          (Data_encoding.Compact.payload Bls.encoding))
        (Data_encoding.Compact.req "contents"
          (Data_encoding.Compact.list_value bits transaction_encoding))).
End V1.

Inductive t (signer content : Set) : Set :=
| V1 : V1.t t signer content.

Arguments V1 {_ _}.

We use two bits for the versioning of the layer-2 batches, which leaves six bits in the shared tag of compact encoding. We use these six bits to efficiently encode small lists.
To ensure backward compatibility, the value of the label [tag_bits] cannot be modified. To have more than 3 versions of the encoding, one would have to use the fourth case to wrap a new union.
{[ union ~tag_bits:2 ~inner_bits:6 [ case "V1" ...; case "V2" ...; case "V3" ...; case "V_next" ... (union [ case "V4" ... ; ... ]); ] ]}
Definition compact
  : Data_encoding.Compact.t (t Indexable.unknown Indexable.unknown) :=
  Data_encoding.Compact.union (Some 2) (Some 6)
    [
      Data_encoding.Compact.case_value "V1" None (V1.compact 6)
        (fun (function_parameter : t Indexable.unknown Indexable.unknown) ⇒
          let 'V1 x_value := function_parameter in
          Some x_value) (fun (x_value : V1.t) ⇒ V1 x_value)
    ].

An encoding for [t] that uses a specialized, space-efficient encoding for the list of transactions.