🐆 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.
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.
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.
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.
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.
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.
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].