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

Module Counter_mismatch.
  Record record : Set := Build {
    account : Tx_rollup_l2_address.t;
    expected : int64;
    provided : int64;
  }.
  Definition with_account account (r : record) :=
    Build account r.(expected) r.(provided).
  Definition with_expected expected (r : record) :=
    Build r.(account) expected r.(provided).
  Definition with_provided provided (r : record) :=
    Build r.(account) r.(expected) provided.
End Counter_mismatch.
Definition Counter_mismatch := Counter_mismatch.record.

Module Maximum_withdraws_per_message_exceeded.
  Record record : Set := Build {
    current : int;
    maximum : int;
  }.
  Definition with_current current (r : record) :=
    Build current r.(maximum).
  Definition with_maximum maximum (r : record) :=
    Build r.(current) maximum.
End Maximum_withdraws_per_message_exceeded.
Definition Maximum_withdraws_per_message_exceeded :=
  Maximum_withdraws_per_message_exceeded.record.

Init function; without side-effects in Coq

Definition init_module : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch
      "tx_rollup_operation_counter_mismatch" "Operation counter mismatch"
      "A transaction rollup operation has been submitted with an incorrect counter"
      None
      (Data_encoding.obj3
        (Data_encoding.req None None "account" Tx_rollup_l2_address.encoding)
        (Data_encoding.req None None "expected" Data_encoding.int64_value)
        (Data_encoding.req None None "provided" Data_encoding.int64_value))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Counter_mismatch" then
            let '{|
              Counter_mismatch.account := account;
                Counter_mismatch.expected := expected;
                Counter_mismatch.provided := provided
                |} := cast Counter_mismatch payload in
            Some (account, expected, provided)
          else None
        end)
      (fun (function_parameter : Tx_rollup_l2_address.t × int64 × int64) ⇒
        let '(account, expected, provided) := function_parameter in
        Build_extensible "Counter_mismatch" Counter_mismatch
          {| Counter_mismatch.account := account;
            Counter_mismatch.expected := expected;
            Counter_mismatch.provided := provided; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "tx_rollup_incorrect_aggregated_signature"
      "Incorrect aggregated signature" "The aggregated signature is incorrect"
      None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Incorrect_aggregated_signature" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Incorrect_aggregated_signature" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch
      "tx_rollup_unknown_metadata" "Unknown metadata"
      "A public key index was provided but the account information for this index is not present in the context."
      None
      (Data_encoding.obj1
        (Data_encoding.req None None "idx" Data_encoding.int32_value))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Unallocated_metadata" then
            let i_value := cast int32 payload in
            Some i_value
          else None
        end)
      (fun (i_value : int32) ⇒
        Build_extensible "Unallocated_metadata" int32 i_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "tx_rollup_invalid_transaction" "Invalid transaction"
      "The signer signed multiple operations in the same transaction. He must gather all the contents in a single operation"
      None
      (Data_encoding.obj1
        (Data_encoding.req None None "pk"
          Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Multiple_operations_for_signer" then
            let idx := cast Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) payload in
            Some idx
          else None
        end)
      (fun (idx : Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t)) ⇒
        Build_extensible "Multiple_operations_for_signer"
          Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) idx) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "tx_rollup_invalid_transaction_encoding" "Invalid transaction encoding"
      "The transaction could not be decoded from bytes" None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Invalid_transaction_encoding" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Invalid_transaction_encoding" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "tx_rollup_invalid_batch_encoding" "Invalid batch encoding"
      "The batch could not be decoded from bytes" None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Invalid_batch_encoding" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Invalid_batch_encoding" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "tx_rollup_unexpectedly_indexed_ticket"
      "Unexpected indexed ticket in deposit or transfer"
      "Tickets in layer2-to-layer1 transfers must be referenced by value." None
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Unexpectedly_indexed_ticket" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Unexpectedly_indexed_ticket" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_missing_ticket"
      "Attempted to withdraw from a ticket missing in the rollup"
      "A withdrawal must reference a ticket that already exists in the rollup."
      None
      (Data_encoding.obj1
        (Data_encoding.req None None "ticket_hash"
          Alpha_context.Ticket_hash.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Missing_ticket" then
            let ticket_hash := cast Alpha_context.Ticket_hash.t payload in
            Some ticket_hash
          else None
        end)
      (fun (ticket_hash : Alpha_context.Ticket_hash.t) ⇒
        Build_extensible "Missing_ticket" Alpha_context.Ticket_hash.t
          ticket_hash) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_unknown_address"
      "Attempted to sign a transfer with an unknown address"
      "The address must exist in the context when signing a transfer with it."
      None
      (Data_encoding.obj1
        (Data_encoding.req None None "address" Tx_rollup_l2_address.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Unknown_address" then
            let addr := cast Tx_rollup_l2_address.t payload in
            Some addr
          else None
        end)
      (fun (addr : Tx_rollup_l2_address.t) ⇒
        Build_extensible "Unknown_address" Tx_rollup_l2_address.t addr) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_invalid_self_transfer" "Attempted to transfer ticket to self"
      "The index for the destination is the same as the sender" None
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Invalid_self_transfer" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Invalid_self_transfer" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "tx_rollup_invalid_zero_transfer" "Attempted to transfer zero ticket"
      "A transfer's amount must be greater than zero." None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Invalid_zero_transfer" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Invalid_zero_transfer" unit tt) in
  Error_monad.register_error_kind Error_monad.Permanent
    "tx_rollup_maximum_withdraws_per_message_exceeded"
    "Maximum tx-rollup withdraws per message exceeded"
    "The maximum number of withdraws allowed per tx-rollup message exceeded"
    None
    (Data_encoding.obj2
      (Data_encoding.req None None "current" Data_encoding.int31)
      (Data_encoding.req None None "limit" Data_encoding.int31))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload ⇒
        if String.eqb tag "Maximum_withdraws_per_message_exceeded" then
          let '{|
            Maximum_withdraws_per_message_exceeded.current := current;
              Maximum_withdraws_per_message_exceeded.maximum := maximum
              |} := cast Maximum_withdraws_per_message_exceeded payload in
          Some (current, maximum)
        else None
      end)
    (fun (function_parameter : int × int) ⇒
      let '(current, maximum) := function_parameter in
      Build_extensible "Maximum_withdraws_per_message_exceeded"
        Maximum_withdraws_per_message_exceeded
        {| Maximum_withdraws_per_message_exceeded.current := current;
          Maximum_withdraws_per_message_exceeded.maximum := maximum; |}).

Module indexes.
  Record record : Set := Build {
    address_indexes :
      list (Tx_rollup_l2_address.t × Tx_rollup_l2_address.Indexable.index);
    ticket_indexes :
      list
        (Alpha_context.Ticket_hash.t ×
          Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.index));
  }.
  Definition with_address_indexes address_indexes (r : record) :=
    Build address_indexes r.(ticket_indexes).
  Definition with_ticket_indexes ticket_indexes (r : record) :=
    Build r.(address_indexes) ticket_indexes.
End indexes.
Definition indexes := indexes.record.

Definition encoding_indexes : Data_encoding.t indexes :=
  Data_encoding.conv
    (fun (function_parameter : indexes) ⇒
      let '{|
        indexes.address_indexes := address_indexes;
          indexes.ticket_indexes := ticket_indexes
          |} := function_parameter in
      (address_indexes, ticket_indexes))
    (fun (function_parameter :
      list (Tx_rollup_l2_address.t × Tx_rollup_l2_address.Indexable.index) ×
        list
          (Alpha_context.Ticket_hash.t ×
            Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.index)))
      ⇒
      let '(address_indexes, ticket_indexes) := function_parameter in
      {| indexes.address_indexes := address_indexes;
        indexes.ticket_indexes := ticket_indexes; |}) None
    (Data_encoding.obj2
      (Data_encoding.req None None "address_indexes"
        (Data_encoding.list_value None
          (Data_encoding.tup2 Tx_rollup_l2_address.encoding
            Tx_rollup_l2_address.Indexable.index_encoding)))
      (Data_encoding.req None None "ticket_indexes"
        (Data_encoding.list_value None
          (Data_encoding.tup2 Alpha_context.Ticket_hash.encoding
            Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.index_encoding))))).

Module Message_result.

Records for the constructor parameters

  Module ConstructorRecords_transaction_result.
    Module transaction_result.
      Module Transaction_failure.
        Record record {index reason : Set} : Set := Build {
          index : index;
          reason : reason;
        }.
        Arguments record : clear implicits.
        Definition with_index {t_index t_reason} index
          (r : record t_index t_reason) :=
          Build t_index t_reason index r.(reason).
        Definition with_reason {t_index t_reason} reason
          (r : record t_index t_reason) :=
          Build t_index t_reason r.(index) reason.
      End Transaction_failure.
      Definition Transaction_failure_skeleton := Transaction_failure.record.
    End transaction_result.
  End ConstructorRecords_transaction_result.
  Import ConstructorRecords_transaction_result.

  Reserved Notation "'transaction_result.Transaction_failure".

  Inductive transaction_result : Set :=
  | Transaction_success : transaction_result
  | Transaction_failure :
    'transaction_result.Transaction_failure → transaction_result
  
  where "'transaction_result.Transaction_failure" :=
    (transaction_result.Transaction_failure_skeleton int Error_monad._error).

  Module transaction_result.
    Include ConstructorRecords_transaction_result.transaction_result.
    Definition Transaction_failure := 'transaction_result.Transaction_failure.
  End transaction_result.

  Inductive deposit_result : Set :=
  | Deposit_success : indexes → deposit_result
  | Deposit_failure : Error_monad._error → deposit_result.

  Definition encoding_transaction_result
    : Data_encoding.encoding transaction_result :=
    Data_encoding.union None
      [
        let kind_value := "transaction_success" in
        Data_encoding.case_value kind_value None (Data_encoding.Tag 0)
          (Data_encoding.constant kind_value)
          (fun (function_parameter : transaction_result) ⇒
            match function_parameter with
            | Transaction_success ⇒ Some tt
            | _ ⇒ None
            end)
          (fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Transaction_success);
        let kind_value := "transaction_failure" in
        Data_encoding.case_value kind_value None (Data_encoding.Tag 1)
          (Data_encoding.obj1
            (Data_encoding.req None None kind_value
              (Data_encoding.obj2
                (Data_encoding.req None None "transaction_index"
                  Data_encoding.int31)
                (Data_encoding.req None None "reason"
                  Error_monad.error_encoding))))
          (fun (function_parameter : transaction_result) ⇒
            match function_parameter with
            |
              Transaction_failure {|
                transaction_result.Transaction_failure.index := index_value;
                  transaction_result.Transaction_failure.reason
                    :=
                    reason_value
                  |} ⇒ Some (index_value, reason_value)
            | _ ⇒ None
            end)
          (fun (function_parameter : int × Error_monad._error) ⇒
            let '(index_value, reason_value) := function_parameter in
            Transaction_failure
              {|
                transaction_result.Transaction_failure.index :=
                  index_value;
                transaction_result.Transaction_failure.reason :=
                  reason_value; |})
      ].

  Definition encoding_deposit_result : Data_encoding.encoding deposit_result :=
    Data_encoding.union None
      [
        let kind_value := "deposit_success" in
        Data_encoding.case_value kind_value None (Data_encoding.Tag 0)
          (Data_encoding.obj1
            (Data_encoding.req None None kind_value encoding_indexes))
          (fun (function_parameter : deposit_result) ⇒
            match function_parameter with
            | Deposit_success indexes_value ⇒ Some indexes_value
            | _ ⇒ None
            end)
          (fun (indexes_value : indexes) ⇒ Deposit_success indexes_value);
        let kind_value := "deposit_failure" in
        Data_encoding.case_value kind_value None (Data_encoding.Tag 1)
          (Data_encoding.obj1
            (Data_encoding.req None None kind_value
              (Data_encoding.obj1
                (Data_encoding.req None None "reason"
                  Error_monad.error_encoding))))
          (fun (function_parameter : deposit_result) ⇒
            match function_parameter with
            | Deposit_failure reason_value ⇒ Some reason_value
            | _ ⇒ None
            end)
          (fun (reason_value : Error_monad._error) ⇒
            Deposit_failure reason_value)
      ].

  Module Batch_V1.

Records for the constructor parameters

    Module ConstructorRecords_t.
      Module t.
        Module Batch_result.
          Record record {results indexes : Set} : Set := Build {
            results : results;
            indexes : indexes;
          }.
          Arguments record : clear implicits.
          Definition with_results {t_results t_indexes} results
            (r : record t_results t_indexes) :=
            Build t_results t_indexes results r.(indexes).
          Definition with_indexes {t_results t_indexes} indexes
            (r : record t_results t_indexes) :=
            Build t_results t_indexes r.(results) indexes.
        End Batch_result.
        Definition Batch_result_skeleton := Batch_result.record.
      End t.
    End ConstructorRecords_t.
    Import ConstructorRecords_t.

    Reserved Notation "'t.Batch_result".

    Inductive t : Set :=
    | Batch_result : 't.Batch_result → t
    
    where "'t.Batch_result" :=
      (t.Batch_result_skeleton
        (list (Tx_rollup_l2_batch.V1.transaction × transaction_result)) indexes).

    Module t.
      Include ConstructorRecords_t.t.
      Definition Batch_result := 't.Batch_result.
    End t.

    Definition encoding : Data_encoding.encoding t :=
      Data_encoding.conv
        (fun (function_parameter : t) ⇒
          let
            'Batch_result {|
              t.Batch_result.results := results;
                t.Batch_result.indexes := indexes_value
                |} := function_parameter in
          (results, indexes_value))
        (fun (function_parameter :
          list (Tx_rollup_l2_batch.V1.transaction × transaction_result) ×
            indexes) ⇒
          let '(results, indexes_value) := function_parameter in
          Batch_result
            {| t.Batch_result.results := results;
              t.Batch_result.indexes := indexes_value; |}) None
        (Data_encoding.obj2
          (Data_encoding.req None None "results"
            (Data_encoding.list_value None
              (Data_encoding.tup2
                (Data_encoding.Compact.make
                  (Some (Variant.Build "Uint8" unit tt))
                  Tx_rollup_l2_batch.V1.compact_transaction_signer_index)
                encoding_transaction_result)))
          (Data_encoding.req None None "allocated_indexes" encoding_indexes)).

    (* Batch_V1 *)
    Definition module :=
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}.
  End Batch_V1.
  Definition Batch_V1 := Batch_V1.module.

  Inductive message_result : Set :=
  | Deposit_result : deposit_result → message_result
  | Batch_V1_result : Batch_V1.(Storage_sigs.VALUE.t) → message_result.

  Definition message_result_encoding : Data_encoding.encoding message_result :=
    Data_encoding.union None
      [
        let kind_value := "deposit_result" in
        Data_encoding.case_value kind_value None (Data_encoding.Tag 0)
          (Data_encoding.obj1
            (Data_encoding.req None None kind_value
              encoding_deposit_result))
          (fun (function_parameter : message_result) ⇒
            match function_parameter with
            | Deposit_result result_value ⇒ Some result_value
            | _ ⇒ None
            end)
          (fun (result_value : deposit_result) ⇒
            Deposit_result result_value);
        let kind_value := "batch_v1_result" in
        Data_encoding.case_value kind_value None (Data_encoding.Tag 1)
          (Data_encoding.obj1
            (Data_encoding.req None None kind_value
              Batch_V1.(Storage_sigs.VALUE.encoding)))
          (fun (function_parameter : message_result) ⇒
            match function_parameter with
            | Batch_V1_result result_value ⇒ Some result_value
            | _ ⇒ None
            end)
          (fun (result_value : Batch_V1.(Storage_sigs.VALUE.t)) ⇒
            Batch_V1_result result_value)
      ].

  Definition t : Set :=
    message_result × list Alpha_context.Tx_rollup_withdraw.t.

  Definition encoding
    : Data_encoding.encoding
      (message_result × list Alpha_context.Tx_rollup_withdraw.t) :=
    Data_encoding.tup2 message_result_encoding
      (Data_encoding.list_value None Alpha_context.Tx_rollup_withdraw.encoding).
End Message_result.

Module parameters.
  Record record : Set := Build {
    tx_rollup_max_withdrawals_per_batch : int;
  }.
  Definition with_tx_rollup_max_withdrawals_per_batch
    tx_rollup_max_withdrawals_per_batch (r : record) :=
    Build tx_rollup_max_withdrawals_per_batch.
End parameters.
Definition parameters := parameters.record.

Module BATCH_V1.
  Record signature {ctxt_type : Set} {m : Set → Set} : Set := {
    ctxt_type := ctxt_type;
    m := m;
    apply_batch :
      ctxt_type → parameters → Tx_rollup_l2_batch.V1.t →
      m
        (ctxt_type × Message_result.Batch_V1.(Storage_sigs.VALUE.t) ×
          list Alpha_context.Tx_rollup_withdraw.t);
    check_signature :
      ctxt_type → Tx_rollup_l2_batch.V1.t →
      m (ctxt_type × indexes × Tx_rollup_l2_batch.V1.t);
  }.
End BATCH_V1.
Definition BATCH_V1 := @BATCH_V1.signature.
Arguments BATCH_V1 {_ _}.

Module S.
  Record signature {ctxt_type : Set} {m : Set → Set} : Set := {
    ctxt_type := ctxt_type;
    m := m;
    Batch_V1 : BATCH_V1 (ctxt_type := ctxt_type) (m := fun (a : Set) ⇒ m a);
    

[apply_deposit ctxt deposit] credits a quantity of tickets to a layer2 address in [ctxt].

This function can fail if the [deposit.amount] is not strictly-positive.

If the [deposit] causes an error, then a withdrawal returning the funds to the deposit's sender is returned.

    apply_deposit :
      ctxt_type → Alpha_context.Tx_rollup_message.deposit →
      m
        (ctxt_type × Message_result.deposit_result ×
          option Alpha_context.Tx_rollup_withdraw.t);
    

[apply_message ctxt parameters message] interprets the [message] in the [ctxt].

That is,

{ul {li Deposit tickets if the message is a deposit. } {li Decodes the batch and interprets it for the correct batch version. }}

The function can fail with {!Invalid_batch_encoding} if it's not able to decode the batch.

The function can also return errors from subsequent functions, see {!apply_deposit} and batch interpretations for various versions.

The list of withdrawals in the message result followed the ordering of the contents in the message.

    apply_message :
      ctxt_type → parameters → Alpha_context.Tx_rollup_message.t →
      m (ctxt_type × Message_result.t);
  }.
End S.
Definition S := @S.signature.
Arguments S {_ _}.

Module Make.
  Class FArgs {Context_t : Set} {Context_m : Set → Set} := {
    Context :
      Tx_rollup_l2_context_sig.CONTEXT (t := Context_t) (m := Context_m);
  }.
  Arguments Build_FArgs {_ _}.

  Definition ctxt_type `{FArgs} : Set :=
    Context.(Tx_rollup_l2_context_sig.CONTEXT.t).

  Definition index_value `{FArgs} {A B C : Set}
    (get_or_associate_index :
      A → B →
      Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
        (A × Tx_rollup_l2_context_sig.created_existed × Indexable.index B))
    (add_index : C → B × Indexable.index B → C) (ctxt : A) (indexes_value : C)
    (indexable : Indexable.t B)
    : Context.(Tx_rollup_l2_context_sig.CONTEXT.m) (A × C × Indexable.index B) :=
    match Indexable.destruct indexable with
    | Either.Right v_value ⇒
      Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letplus)
        (get_or_associate_index ctxt v_value)
        (fun function_parameter ⇒
          let '(ctxt, created, idx) := function_parameter in
          match created with
          | Tx_rollup_l2_context_sig.Existed ⇒ (ctxt, indexes_value, idx)
          | Tx_rollup_l2_context_sig.Created ⇒
            (ctxt, (add_index indexes_value (v_value, idx)), idx)
          end)
    | Either.Left i_value ⇒
      Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
        (ctxt, indexes_value, i_value)
    end.

  Definition address_index `{FArgs}
    (ctxt : Context.(Tx_rollup_l2_context_sig.CONTEXT.t))
    (indexes_value : indexes) (indexable : Indexable.t Tx_rollup_l2_address.t)
    : Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
      (Context.(Tx_rollup_l2_context_sig.CONTEXT.t) × indexes ×
        Indexable.index Tx_rollup_l2_address.t) :=
    let get_or_associate_index :=
      Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_index).(Tx_rollup_l2_context_sig.INDEX.get_or_associate_index)
      in
    let add_index
      (indexes_value : indexes)
      (x_value : Tx_rollup_l2_address.t × Tx_rollup_l2_address.Indexable.index)
      : indexes :=
      indexes.with_address_indexes
        (cons x_value indexes_value.(indexes.address_indexes)) indexes_value in
    index_value get_or_associate_index add_index ctxt indexes_value indexable.

  Definition ticket_index `{FArgs}
    (ctxt : Context.(Tx_rollup_l2_context_sig.CONTEXT.t))
    (indexes_value : indexes)
    (indexable : Indexable.t Alpha_context.Ticket_hash.t)
    : Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
      (Context.(Tx_rollup_l2_context_sig.CONTEXT.t) × indexes ×
        Indexable.index Alpha_context.Ticket_hash.t) :=
    let get_or_associate_index :=
      Context.(Tx_rollup_l2_context_sig.CONTEXT.Ticket_index).(Tx_rollup_l2_context_sig.INDEX.get_or_associate_index)
      in
    let add_index
      (indexes_value : indexes)
      (x_value :
        Alpha_context.Ticket_hash.t ×
          Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.index))
      : indexes :=
      indexes.with_ticket_indexes
        (cons x_value indexes_value.(indexes.ticket_indexes)) indexes_value in
    index_value get_or_associate_index add_index ctxt indexes_value indexable.

  Definition address_of_signer_index `{FArgs}
    (idx : Tx_rollup_l2_batch.Signer_indexable.(Indexable.INDEXABLE.index))
    : Tx_rollup_l2_address.Indexable.index :=
    Indexable.index_exn (Indexable.to_int32 idx).

  Definition signer_of_address_index `{FArgs}
    (idx : Tx_rollup_l2_address.Indexable.index)
    : Tx_rollup_l2_batch.Signer_indexable.(Indexable.INDEXABLE.index) :=
    Indexable.index_exn (Indexable.to_int32 idx).

  Definition empty_indexes `{FArgs} : indexes :=
    {| indexes.address_indexes := nil; indexes.ticket_indexes := nil; |}.

  Definition assert_non_zero_quantity `{FArgs} (qty : Tx_rollup_l2_qty.t)
    : Context.(Tx_rollup_l2_context_sig.CONTEXT.m) unit :=
    Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail_when)
      (Tx_rollup_l2_qty.op_eq qty Tx_rollup_l2_qty.zero)
      (Build_extensible "Invalid_zero_transfer" unit tt).

[get_metadata ctxt idx] returns the metadata associated to [idx] in [ctxt]. It must have an associated metadata in the context, otherwise, something went wrong in {!check_signature}.

  Definition get_metadata `{FArgs}
    (ctxt : ctxt_type) (idx : Tx_rollup_l2_context_sig.address_index)
    : Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
      Tx_rollup_l2_context_sig.metadata :=
    Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
      (Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_metadata).(Tx_rollup_l2_context_sig.ADDRESS_METADATA.get)
        ctxt idx)
      (fun metadata ⇒
        match metadata with
        | None ⇒
          Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail)
            (Build_extensible "Unallocated_metadata" int32
              (Indexable.to_int32 idx))
        | Some metadata ⇒
          Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
            metadata
        end).

[get_metadata_signer] gets the metadata for a signer using {!get_metadata}. It transforms a signer index to an address one.

  Definition get_metadata_signer `{FArgs}
    (ctxt : ctxt_type)
    (signer_idx :
      Tx_rollup_l2_batch.Signer_indexable.(Indexable.INDEXABLE.index))
    : Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
      Tx_rollup_l2_context_sig.metadata :=
    get_metadata ctxt (address_of_signer_index signer_idx).

[transfers ctxt source_idx destination_idx tidx amount] transfers [amount] from [source_idx] to [destination_idx] of [tidx].

  Definition transfer `{FArgs}
    (ctxt : Context.(Tx_rollup_l2_context_sig.CONTEXT.t))
    (source_idx : Indexable.index Tx_rollup_l2_address.address)
    (destination_idx : Indexable.index Tx_rollup_l2_address.address)
    (tidx : Tx_rollup_l2_context_sig.ticket_index) (amount : Tx_rollup_l2_qty.t)
    : Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
      Context.(Tx_rollup_l2_context_sig.CONTEXT.t) :=
    Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
      (Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail_unless)
        ((Indexable.compare_indexes source_idx destination_idx) ≠i 0)
        (Build_extensible "Invalid_self_transfer" unit tt))
      (fun function_parameter ⇒
        let '_ := function_parameter in
        Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
          (assert_non_zero_quantity amount)
          (fun function_parameter ⇒
            let '_ := function_parameter in
            Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
              (Context.(Tx_rollup_l2_context_sig.CONTEXT.Ticket_ledger).(Tx_rollup_l2_context_sig.TICKET_LEDGER.spend)
                ctxt tidx source_idx amount)
              (fun ctxt ⇒
                Context.(Tx_rollup_l2_context_sig.CONTEXT.Ticket_ledger).(Tx_rollup_l2_context_sig.TICKET_LEDGER.credit)
                  ctxt tidx destination_idx amount))).

[deposit ctxt aidx tidx amount] credits [amount] of [tidx] to [aidx]. They are deposited from the layer1 and created in the layer2 context, but, we only handle the creation part (i.e. in the layer2) in this module.

  Definition deposit `{FArgs}
    (ctxt : Context.(Tx_rollup_l2_context_sig.CONTEXT.t))
    (aidx : Tx_rollup_l2_context_sig.address_index)
    (tidx : Tx_rollup_l2_context_sig.ticket_index) (amount : Tx_rollup_l2_qty.t)
    : Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
      Context.(Tx_rollup_l2_context_sig.CONTEXT.t) :=
    Context.(Tx_rollup_l2_context_sig.CONTEXT.Ticket_ledger).(Tx_rollup_l2_context_sig.TICKET_LEDGER.credit)
      ctxt tidx aidx amount.

  Module Batch_V1.

[operation_with_signer_index ctxt indexes op] takes an operation and performs multiple get/sets on the context to return an operation where the signer is replaced by its index.

It performs on the [ctxt]: {ul {li If the signer is an index, we read the public key from the [ctxt].} {li If the signer is a public key, we associate a new index to it in the [ctxt]. The public key is also added to the metadata if not already present.}}

{b Note:} If the context already contains all the required information, we only read from it.

    Definition operation_with_signer_index `{FArgs}
      (ctxt : ctxt_type) (indexes_value : indexes)
      (op : Tx_rollup_l2_batch.V1.operation)
      : Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
        (ctxt_type × indexes × Tx_rollup_l2_batch.V1.operation ×
          Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t)) :=
      Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
        match Indexable.destruct op.(Tx_rollup_l2_batch.V1.operation.signer)
          with
        | Either.Left signer_index ⇒
          let address_index := address_of_signer_index signer_index in
          Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
            (get_metadata ctxt address_index)
            (fun metadata ⇒
              let pk := metadata.(Tx_rollup_l2_context_sig.metadata.public_key)
                in
              Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
                (ctxt, indexes_value, pk, address_index))
        | Either.Right (Tx_rollup_l2_batch.Bls_pk signer_pk) ⇒
          let addr :=
            Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value) signer_pk in
          Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
            (Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_index).(Tx_rollup_l2_context_sig.INDEX.get_or_associate_index)
              ctxt addr)
            (fun function_parameter ⇒
              let '(ctxt, created, idx) := function_parameter in
              match created with
              | Tx_rollup_l2_context_sig.Existed ⇒
                Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
                  (Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
                    (Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_metadata).(Tx_rollup_l2_context_sig.ADDRESS_METADATA.get)
                      ctxt idx)
                    (fun metadata ⇒
                      match metadata with
                      | Some _ ⇒
                        Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
                          ctxt
                      | None ⇒
                        Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_metadata).(Tx_rollup_l2_context_sig.ADDRESS_METADATA.init_with_public_key)
                          ctxt idx signer_pk
                      end))
                  (fun ctxt ⇒
                    Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
                      (ctxt, indexes_value, signer_pk, idx))
              | Tx_rollup_l2_context_sig.Created ⇒
                let indexes_value :=
                  indexes.with_address_indexes
                    (cons (addr, idx) indexes_value.(indexes.address_indexes))
                    indexes_value in
                Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
                  (Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_metadata).(Tx_rollup_l2_context_sig.ADDRESS_METADATA.init_with_public_key)
                    ctxt idx signer_pk)
                  (fun ctxt ⇒
                    Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
                      (ctxt, indexes_value, signer_pk, idx))
              end)
        | Either.Right (Tx_rollup_l2_batch.L2_addr signer_addr) ⇒
          Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
            (Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_index).(Tx_rollup_l2_context_sig.INDEX.get)
              ctxt signer_addr)
            (fun idx ⇒
              match idx with
              | None ⇒
                Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail)
                  (Build_extensible "Unknown_address" Tx_rollup_l2_address.t
                    signer_addr)
              | Some idx ⇒
                Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
                  (get_metadata ctxt idx)
                  (fun metadata ⇒
                    Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
                      (ctxt, indexes_value,
                        metadata.(Tx_rollup_l2_context_sig.metadata.public_key),
                        idx))
              end)
        end
        (fun function_parameter ⇒
          let '(ctxt, indexes_value, pk, idx) := function_parameter in
          let op :=
            Tx_rollup_l2_batch.V1.operation.with_signer
              (signer_of_address_index idx) op in
          Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
            (ctxt, indexes_value, op, pk)).

[check_transaction ctxt indexes transmitted transaction] performs an *active* check of an operation. We consider this as an *active* check because the function is likely to write in the [ctxt], since it replaces the signer's public key (if provided) by its index in {!operation_with_signer_index}.

Outside of the active preprocessing, we check that a signer signs at most one operation in the [transaction].

It also associates the signer to the bytes representation of a transaction in [transmitted], which is used to check the aggregated signature.

    Definition check_transaction `{FArgs}
      (ctxt : ctxt_type) (indexes_value : indexes)
      (transmitted : list (Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) × bytes))
      (transaction : Tx_rollup_l2_batch.V1.transaction)
      : Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
        (ctxt_type × indexes ×
          list (Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) × bytes) ×
          list Tx_rollup_l2_batch.V1.operation) :=
      Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
        match
          Data_encoding.Binary.to_bytes_opt None
            (Data_encoding.Compact.make (Some (Variant.Build "Uint8" unit tt))
              Tx_rollup_l2_batch.V1.compact_transaction) transaction with
        | Some buf ⇒
          Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
            buf
        | None ⇒
          Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail)
            (Build_extensible "Invalid_transaction_encoding" unit tt)
        end
        (fun buf ⇒
          Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
            (Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.list_fold_left_m)
              (fun (function_parameter :
                ctxt_type × indexes ×
                  list (Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) × bytes) ×
                  list Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) ×
                  list Tx_rollup_l2_batch.V1.operation) ⇒
                let '(ctxt, indexes_value, transmitted, signers, ops) :=
                  function_parameter in
                fun (op : Tx_rollup_l2_batch.V1.operation) ⇒
                  Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
                    (operation_with_signer_index ctxt indexes_value op)
                    (fun function_parameter ⇒
                      let '(ctxt, indexes_value, op, pk) := function_parameter
                        in
                      if
                        List.mem Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.equal)
                          pk signers
                      then
                        Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail)
                          (Build_extensible "Multiple_operations_for_signer"
                            Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) pk)
                      else
                        Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
                          (ctxt, indexes_value, (cons (pk, buf) transmitted),
                            (cons pk signers), (cons op ops))))
              (ctxt, indexes_value, transmitted, nil, nil) transaction)
            (fun function_parameter ⇒
              let '(ctxt, indexes_value, transmitted, _, rev_ops) :=
                function_parameter in
              Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
                (ctxt, indexes_value, transmitted, (List.rev rev_ops)))).

    Definition check_signature `{FArgs}
      (ctxt : ctxt_type) (function_parameter : Tx_rollup_l2_batch.V1.t)
      : Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
        (ctxt_type × indexes × Tx_rollup_l2_batch.V1.t) :=
      let
        '{|
          Tx_rollup_l2_batch.V1.t.contents := transactions;
            Tx_rollup_l2_batch.V1.t.aggregated_signature := aggregated_signature
            |} as batch := function_parameter in
      Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
        (Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.list_fold_left_m)
          (fun (function_parameter :
            ctxt_type × indexes ×
              list (Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) × bytes) ×
              list Tx_rollup_l2_batch.V1.transaction) ⇒
            let '(ctxt, indexes_value, transmitted, new_transactions) :=
              function_parameter in
            fun (transaction : Tx_rollup_l2_batch.V1.transaction) ⇒
              Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
                (check_transaction ctxt indexes_value transmitted transaction)
                (fun function_parameter ⇒
                  let '(ctxt, indexes_value, transmitted, transaction) :=
                    function_parameter in
                  Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
                    (ctxt, indexes_value, transmitted,
                      (cons transaction new_transactions))))
          (ctxt, empty_indexes, nil, nil) transactions)
        (fun function_parameter ⇒
          let '(ctxt, indexes_value, transmitted, rev_new_transactions) :=
            function_parameter in
          Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
            (Context.(Tx_rollup_l2_context_sig.CONTEXT.bls_verify) transmitted
              aggregated_signature)
            (fun b_value ⇒
              Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
                (Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail_unless)
                  b_value
                  (Build_extensible "Incorrect_aggregated_signature" unit tt))
                (fun function_parameter ⇒
                  let '_ := function_parameter in
                  let batch :=
                    Tx_rollup_l2_batch.V1.t.with_contents
                      (List.rev rev_new_transactions) batch in
                  Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
                    (ctxt, indexes_value, batch)))).

[apply_operation_content ctxt source content] performs the transfer on the [ctxt]. The validity of the transfer is checked in the context itself, e.g. for an invalid balance.

It returns the potential created indexes:

{ul {li The destination address index.} {li The ticket exchanged index.}}

    Definition apply_operation_content `{FArgs}
      (ctxt : ctxt_type) (indexes_value : indexes)
      (source_idx :
        Tx_rollup_l2_batch.Signer_indexable.(Indexable.INDEXABLE.index))
      (op_content : Tx_rollup_l2_batch.V1.operation_content)
      : Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
        (ctxt_type × indexes × option Alpha_context.Tx_rollup_withdraw.t) :=
      match op_content with
      |
        Tx_rollup_l2_batch.V1.Withdraw {|
          Tx_rollup_l2_batch.V1.operation_content.Withdraw.destination := claimer;
            Tx_rollup_l2_batch.V1.operation_content.Withdraw.ticket_hash :=
              ticket_hash;
            Tx_rollup_l2_batch.V1.operation_content.Withdraw.qty := amount
            |} ⇒
        Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
          (Context.(Tx_rollup_l2_context_sig.CONTEXT.Ticket_index).(Tx_rollup_l2_context_sig.INDEX.get)
            ctxt ticket_hash)
          (fun tidx_opt ⇒
            Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstarquestion)
              (Option.value_e tidx_opt
                (Build_extensible "Missing_ticket" Alpha_context.Ticket_hash.t
                  ticket_hash))
              (fun tidx ⇒
                let source_idx := address_of_signer_index source_idx in
                Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
                  (assert_non_zero_quantity amount)
                  (fun function_parameter ⇒
                    let '_ := function_parameter in
                    Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
                      (Context.(Tx_rollup_l2_context_sig.CONTEXT.Ticket_ledger).(Tx_rollup_l2_context_sig.TICKET_LEDGER.spend)
                        ctxt tidx source_idx amount)
                      (fun ctxt ⇒
                        let withdrawal :=
                          {|
                            Alpha_context.Tx_rollup_withdraw.order.claimer :=
                              claimer;
                            Alpha_context.Tx_rollup_withdraw.order.ticket_hash
                              := ticket_hash;
                            Alpha_context.Tx_rollup_withdraw.order.amount :=
                              amount; |} in
                        Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
                          (ctxt, indexes_value, (Some withdrawal))))))
      |
        Tx_rollup_l2_batch.V1.Transfer {|
          Tx_rollup_l2_batch.V1.operation_content.Transfer.destination := destination;
            Tx_rollup_l2_batch.V1.operation_content.Transfer.ticket_hash :=
              ticket_hash;
            Tx_rollup_l2_batch.V1.operation_content.Transfer.qty := qty
            |} ⇒
        Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
          (address_index ctxt indexes_value destination)
          (fun function_parameter ⇒
            let '(ctxt, indexes_value, dest_idx) := function_parameter in
            Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
              (ticket_index ctxt indexes_value ticket_hash)
              (fun function_parameter ⇒
                let '(ctxt, indexes_value, tidx) := function_parameter in
                let source_idx := address_of_signer_index source_idx in
                Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
                  (transfer ctxt source_idx dest_idx tidx qty)
                  (fun ctxt ⇒
                    Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
                      (ctxt, indexes_value, None))))
      end.

[check_counter ctxt signer counter] asserts that the provided [counter] is the successor of the one associated to the [signer] in the [ctxt].

    Definition check_counter `{FArgs}
      (ctxt : ctxt_type)
      (signer : Tx_rollup_l2_batch.Signer_indexable.(Indexable.INDEXABLE.t))
      (counter : int64) : Context.(Tx_rollup_l2_context_sig.CONTEXT.m) unit :=
      Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
        (get_metadata_signer ctxt signer)
        (fun metadata ⇒
          Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail_unless)
            (counter =i64
            (Int64.succ metadata.(Tx_rollup_l2_context_sig.metadata.counter)))
            (Build_extensible "Counter_mismatch" Counter_mismatch
              {|
                Counter_mismatch.account :=
                  Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value)
                    metadata.(Tx_rollup_l2_context_sig.metadata.public_key);
                Counter_mismatch.expected :=
                  Int64.succ
                    metadata.(Tx_rollup_l2_context_sig.metadata.counter);
                Counter_mismatch.provided := counter; |})).

[apply_operation ctxt indexes op] checks the counter validity for the [op.signer] with {!check_counter}, and then calls {!apply_operation_content} for each content in [op].

    Definition apply_operation `{FArgs}
      (ctxt : ctxt_type) (indexes_value : indexes)
      (function_parameter : Tx_rollup_l2_batch.V1.operation)
      : Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
        (ctxt_type × indexes × list Alpha_context.Tx_rollup_withdraw.t) :=
      let '{|
        Tx_rollup_l2_batch.V1.operation.signer := signer;
          Tx_rollup_l2_batch.V1.operation.counter := counter;
          Tx_rollup_l2_batch.V1.operation.contents := contents
          |} := function_parameter in
      Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
        (check_counter ctxt signer counter)
        (fun function_parameter ⇒
          let '_ := function_parameter in
          Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
            (Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.list_fold_left_m)
              (fun (function_parameter :
                ctxt_type × indexes × list Alpha_context.Tx_rollup_withdraw.t)
                ⇒
                let '(ctxt, indexes_value, withdrawals) := function_parameter in
                fun (content : Tx_rollup_l2_batch.V1.operation_content) ⇒
                  Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
                    (apply_operation_content ctxt indexes_value signer content)
                    (fun function_parameter ⇒
                      let '(ctxt, indexes_value, withdrawal_opt) :=
                        function_parameter in
                      Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
                        (ctxt, indexes_value,
                          (Pervasives.op_at (Option.to_list withdrawal_opt)
                            withdrawals)))) (ctxt, indexes_value, nil) contents)
            (fun function_parameter ⇒
              let '(ctxt, indexes_value, rev_withdrawals) := function_parameter
                in
              Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
                (ctxt, indexes_value, (List.rev rev_withdrawals)))).

[apply_transaction ctxt indexes transaction] applies each operation in the [transaction]. It returns a {!transaction_result}, i.e. either every operation in the [transaction] succedeed and the [ctxt] is modified, or the [transaction] is a failure and the context is left untouched.

    Definition apply_transaction `{FArgs}
      (initial_ctxt : ctxt_type) (initial_indexes : indexes)
      (transaction : Tx_rollup_l2_batch.V1.transaction)
      : Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
        (ctxt_type × indexes × Message_result.transaction_result ×
          list Alpha_context.Tx_rollup_withdraw.t) :=
      let fix fold
        (params : ctxt_type × indexes × list Alpha_context.Tx_rollup_withdraw.t)
        (index_value : int) (ops : list Tx_rollup_l2_batch.V1.operation)
        : Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
          (ctxt_type × indexes × Message_result.transaction_result ×
            list Alpha_context.Tx_rollup_withdraw.t) :=
        let '(ctxt, prev_indexes, withdrawals) := params in
        match ops with
        | [] ⇒
          Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
            (ctxt, prev_indexes, Message_result.Transaction_success, withdrawals)
        | cons op rst ⇒
          Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
            (Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.catch)
              (apply_operation ctxt prev_indexes op)
              (fun (function_parameter :
                ctxt_type × indexes × list Alpha_context.Tx_rollup_withdraw.t)
                ⇒
                let '(ctxt, indexes_value, op_withdrawals) := function_parameter
                  in
                fold
                  (ctxt, indexes_value,
                    (Pervasives.op_at withdrawals op_withdrawals))
                  (index_value +i 1) rst)
              (fun (reason_value : Error_monad._error) ⇒
                Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
                  (initial_ctxt, initial_indexes,
                    (Message_result.Transaction_failure
                      {|
                        Message_result.transaction_result.Transaction_failure.index
                          := index_value;
                        Message_result.transaction_result.Transaction_failure.reason
                          := reason_value; |}), nil)))
            (fun function_parameter ⇒
              let '(ctxt, indexes_value, status, withdrawals) :=
                function_parameter in
              Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
                (ctxt, indexes_value, status, withdrawals))
        end in
      fold (initial_ctxt, initial_indexes, nil) 0 transaction.

[update_counters ctxt status transaction] updates the counters for the signers of operations in [transaction]. If the [transaction] failed because of a [Counter_mismatch] the counters are left untouched.

    Definition update_counters `{FArgs}
      (ctxt : Context.(Tx_rollup_l2_context_sig.CONTEXT.t))
      (status : Message_result.transaction_result)
      (transaction : list Tx_rollup_l2_batch.V1.operation)
      : Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
        Context.(Tx_rollup_l2_context_sig.CONTEXT.t) :=
      match status with
      |
        Message_result.Transaction_failure {|
          Message_result.transaction_result.Transaction_failure.reason := err
            |} ⇒
        match err with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Counter_mismatch" then
            let '_ := cast Counter_mismatch payload in
            Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
              ctxt
          else
            Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.list_fold_left_m)
              (fun (ctxt : Context.(Tx_rollup_l2_context_sig.CONTEXT.t)) ⇒
                fun (op : Tx_rollup_l2_batch.V1.operation) ⇒
                  Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_metadata).(Tx_rollup_l2_context_sig.ADDRESS_METADATA.incr_counter)
                    ctxt
                    (address_of_signer_index
                      op.(Tx_rollup_l2_batch.V1.operation.signer))) ctxt
              transaction
        end
      | Message_result.Transaction_success ⇒
        Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.list_fold_left_m)
          (fun (ctxt : Context.(Tx_rollup_l2_context_sig.CONTEXT.t)) ⇒
            fun (op : Tx_rollup_l2_batch.V1.operation) ⇒
              Context.(Tx_rollup_l2_context_sig.CONTEXT.Address_metadata).(Tx_rollup_l2_context_sig.ADDRESS_METADATA.incr_counter)
                ctxt
                (address_of_signer_index
                  op.(Tx_rollup_l2_batch.V1.operation.signer))) ctxt transaction
      end.

    Definition apply_batch `{FArgs}
      (ctxt : ctxt_type) (parameters : parameters)
      (batch : Tx_rollup_l2_batch.V1.t)
      : Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
        (ctxt_type × Message_result.Batch_V1.(Storage_sigs.VALUE.t) ×
          list Alpha_context.Tx_rollup_withdraw.t) :=
      Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
        (check_signature ctxt batch)
        (fun function_parameter ⇒
          let '(ctxt, indexes_value, batch) := function_parameter in
          let '{| Tx_rollup_l2_batch.V1.t.contents := contents |} := batch in
          Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
            (Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.list_fold_left_m)
              (fun (function_parameter :
                ctxt_type × indexes ×
                  list
                    (Tx_rollup_l2_batch.V1.transaction ×
                      Message_result.transaction_result) ×
                  list Alpha_context.Tx_rollup_withdraw.t) ⇒
                let '(prev_ctxt, prev_indexes, results, withdrawals) :=
                  function_parameter in
                fun (transaction : Tx_rollup_l2_batch.V1.transaction) ⇒
                  Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
                    (apply_transaction prev_ctxt prev_indexes transaction)
                    (fun function_parameter ⇒
                      let
                        '(new_ctxt, new_indexes, status, transaction_withdrawals) :=
                        function_parameter in
                      Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
                        (update_counters new_ctxt status transaction)
                        (fun new_ctxt ⇒
                          Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
                            (new_ctxt, new_indexes,
                              (cons (transaction, status) results),
                              (Pervasives.op_at withdrawals
                                transaction_withdrawals)))))
              (ctxt, indexes_value, nil, nil) contents)
            (fun function_parameter ⇒
              let '(ctxt, indexes_value, rev_results, withdrawals) :=
                function_parameter in
              let limit :=
                parameters.(parameters.tx_rollup_max_withdrawals_per_batch) in
              if Compare.List_length_with.op_gt withdrawals limit then
                Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail)
                  (Build_extensible "Maximum_withdraws_per_message_exceeded"
                    Maximum_withdraws_per_message_exceeded
                    {|
                      Maximum_withdraws_per_message_exceeded.current :=
                        List.length withdrawals;
                      Maximum_withdraws_per_message_exceeded.maximum := limit;
                      |})
              else
                let results := List.rev rev_results in
                Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
                  (ctxt,
                    (Message_result.Batch_V1.Batch_result
                      {|
                        Message_result.Batch_V1.t.Batch_result.results :=
                          results;
                        Message_result.Batch_V1.t.Batch_result.indexes :=
                          indexes_value; |}), withdrawals))).

    (* Batch_V1 *)
    Definition module `{FArgs} :=
      {|
        BATCH_V1.apply_batch := apply_batch;
        BATCH_V1.check_signature := check_signature
      |}.
  End Batch_V1.
  Definition Batch_V1 `{FArgs}
    : BATCH_V1 (ctxt_type := ctxt_type)
      (m := fun (a : Set) ⇒ Context.(Tx_rollup_l2_context_sig.CONTEXT.m) a) :=
    Batch_V1.module.

  Definition apply_deposit `{FArgs}
    (initial_ctxt : ctxt_type)
    (function_parameter : Alpha_context.Tx_rollup_message.deposit)
    : Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
      (ctxt_type × Message_result.deposit_result ×
        option Alpha_context.Tx_rollup_withdraw.t) :=
    let '{|
      Tx_rollup_message_repr.deposit.sender := sender;
        Tx_rollup_message_repr.deposit.destination := destination;
        Tx_rollup_message_repr.deposit.ticket_hash := ticket_hash;
        Tx_rollup_message_repr.deposit.amount := amount
        |} := function_parameter in
    let apply_deposit (function_parameter : unit)
      : Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
        (Context.(Tx_rollup_l2_context_sig.CONTEXT.t) × indexes) :=
      let '_ := function_parameter in
      Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
        (address_index initial_ctxt empty_indexes destination)
        (fun function_parameter ⇒
          let '(ctxt, indexes_value, aidx) := function_parameter in
          Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
            (ticket_index ctxt indexes_value (Indexable.value_value ticket_hash))
            (fun function_parameter ⇒
              let '(ctxt, indexes_value, tidx) := function_parameter in
              Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
                (deposit ctxt aidx tidx amount)
                (fun ctxt ⇒
                  Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
                    (ctxt, indexes_value)))) in
    Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.catch)
      (apply_deposit tt)
      (fun (function_parameter : ctxt_type × indexes) ⇒
        let '(ctxt, indexes_value) := function_parameter in
        Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
          (ctxt, (Message_result.Deposit_success indexes_value), None))
      (fun (reason_value : Error_monad._error) ⇒
        let withdrawal :=
          {| Alpha_context.Tx_rollup_withdraw.order.claimer := sender;
            Alpha_context.Tx_rollup_withdraw.order.ticket_hash := ticket_hash;
            Alpha_context.Tx_rollup_withdraw.order.amount := amount; |} in
        Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
          (initial_ctxt, (Message_result.Deposit_failure reason_value),
            (Some withdrawal))).

  Definition apply_message `{FArgs}
    (ctxt : ctxt_type) (parameters : parameters)
    (msg : Alpha_context.Tx_rollup_message.t)
    : Context.(Tx_rollup_l2_context_sig.CONTEXT.m)
      (ctxt_type × Message_result.t) :=
    match msg with
    | Alpha_context.Tx_rollup_message.Deposit deposit ⇒
      Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
        (apply_deposit ctxt deposit)
        (fun function_parameter ⇒
          let '(ctxt, result_value, withdrawl_opt) := function_parameter in
          Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
            (ctxt,
              ((Message_result.Deposit_result result_value),
                (Option.to_list withdrawl_opt))))
    | Alpha_context.Tx_rollup_message.Batch str ⇒
      let batch :=
        Data_encoding.Binary.of_string_opt Tx_rollup_l2_batch.encoding str in
      match batch with
      | Some (Tx_rollup_l2_batch.V1 batch) ⇒
        Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
          (Batch_V1.(BATCH_V1.apply_batch) ctxt parameters batch)
          (fun function_parameter ⇒
            let '(ctxt, result_value, withdrawals) := function_parameter in
            Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX._return)
              (ctxt,
                ((Message_result.Batch_V1_result result_value), withdrawals)))
      | None ⇒
        Context.(Tx_rollup_l2_context_sig.CONTEXT.Syntax).(Tx_rollup_l2_context_sig.SYNTAX.fail)
          (Build_extensible "Invalid_batch_encoding" unit tt)
      end
    end.

  (* Make *)
  Definition functor `{FArgs} :=
    {|
      S.Batch_V1 := Batch_V1;
      S.apply_deposit := apply_deposit;
      S.apply_message := apply_message
    |}.
End Make.
Definition Make {Context_t : Set} {Context_m : Set → Set}
  (Context : Tx_rollup_l2_context_sig.CONTEXT (t := Context_t) (m := Context_m))
  : S (ctxt_type := Context.(Tx_rollup_l2_context_sig.CONTEXT.t))
    (m := fun (a : Set) ⇒ Context.(Tx_rollup_l2_context_sig.CONTEXT.m) a) :=
  let '_ := Make.Build_FArgs Context in
  Make.functor.