🐆 Tx_rollup_l2_batch.v

Proofs

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_batch.

Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_l2_qty.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_l2_context_sig.

Module V1.
  Import Proto_alpha.Tx_rollup_l2_batch.V1.

  Module operation_content.
    Import Proto_alpha.Tx_rollup_l2_batch.V1.operation_content.

    Module Withdraw.
      Module Valid.
        Import Proto_alpha.Tx_rollup_l2_batch.V1.operation_content.Withdraw.

Validity predicate for the payload of the contructor [Withdraw].

        Record t (x : Withdraw) : Prop := {
          qty : Tx_rollup_l2_qty.Valid.t x.(qty);
        }.
      End Valid.
    End Withdraw.

    Module Transfer.
      Module Valid.
        Import Proto_alpha.Tx_rollup_l2_batch.V1.operation_content.Transfer.

Validity predicate for the payload of the contructor [Transfer].

        Record t (x : Transfer) : Prop := {
          destination :
            Tx_rollup_l2_context_sig.address_index.Valid.t x.(destination);
          ticket_hash :
            Tx_rollup_l2_context_sig.ticket_index.Valid.t x.(ticket_hash);
          qty : Tx_rollup_l2_qty.Valid.t x.(qty);
        }.
      End Valid.
    End Transfer.

    Module Valid.

Validity predicate for the type [t].

      Definition t (x : operation_content) : Prop :=
        match x with
        | Tx_rollup_l2_batch.V1.Withdraw x ⇒ Withdraw.Valid.t x
        | Tx_rollup_l2_batch.V1.Transfer x ⇒ Transfer.Valid.t x
        end.
    End Valid.
  End operation_content.

  Module operation.
    Module Valid.
      Import Proto_alpha.Tx_rollup_l2_batch.V1.operation.

Validity predicate for [operation].

      Record t (x : operation) : Prop := {
        signer : Indexable.Index.Valid.t x.(signer);
        counter : Int64.Valid.t x.(counter);
        contents : List.Forall operation_content.Valid.t x.(contents);
      }.
    End Valid.
  End operation.

  Module transaction.
    Module Valid.

Validity predicate for the type [transaction].

      Definition t (x : transaction) : Prop :=
        List.Forall operation.Valid.t x.
    End Valid.
  End transaction.

  Module Valid.
    Import Proto_alpha.Tx_rollup_l2_batch.V1.t.

Validity predicate for the type [t].

    Record t (x : t) : Prop := {
      contents : List.Forall transaction.Valid.t x.(contents);
    }.
  End Valid.
End V1.