🐆 Tx_rollup_l2_apply.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_apply.
Require TezosOfOCaml.Environment.V8.Proofs.Error_monad.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_l2_address.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_l2_batch.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_l2_context_sig.
Module indexes.
Module Valid.
Import Proto_alpha.Tx_rollup_l2_apply.indexes.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_apply.
Require TezosOfOCaml.Environment.V8.Proofs.Error_monad.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_l2_address.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_l2_batch.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_l2_context_sig.
Module indexes.
Module Valid.
Import Proto_alpha.Tx_rollup_l2_apply.indexes.
Validity predicate for the type [indexes].
Record t (x : Tx_rollup_l2_apply.indexes) : Prop := {
address_indexes :
List.Forall
(fun '(_, index) ⇒
Tx_rollup_l2_context_sig.address_index.Valid.t index
)
x.(address_indexes);
ticket_indexes :
List.Forall
(fun '(_, index) ⇒
Tx_rollup_l2_context_sig.ticket_index.Valid.t index
)
x.(ticket_indexes);
}.
End Valid.
End indexes.
address_indexes :
List.Forall
(fun '(_, index) ⇒
Tx_rollup_l2_context_sig.address_index.Valid.t index
)
x.(address_indexes);
ticket_indexes :
List.Forall
(fun '(_, index) ⇒
Tx_rollup_l2_context_sig.ticket_index.Valid.t index
)
x.(ticket_indexes);
}.
End Valid.
End indexes.
The encoding [encoding_indexes] is valid.
Lemma encoding_indexes_is_valid :
Data_encoding.Valid.t indexes.Valid.t Tx_rollup_l2_apply.encoding_indexes.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros [] []; simpl in ×.
repeat split; trivial;
eapply List.Forall_impl;
try match goal with
| H : _ |- _ ⇒ apply H
end;
intros; Tactics.destruct_pairs.
{ easy. }
{ step; simpl in *; try easy.
repeat split; lia.
}
Qed.
#[global] Hint Resolve encoding_indexes_is_valid : Data_encoding_db.
Module Message_result.
Import Proto_alpha.Tx_rollup_l2_apply.Message_result.
Module transaction_result.
Module Valid.
Data_encoding.Valid.t indexes.Valid.t Tx_rollup_l2_apply.encoding_indexes.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros [] []; simpl in ×.
repeat split; trivial;
eapply List.Forall_impl;
try match goal with
| H : _ |- _ ⇒ apply H
end;
intros; Tactics.destruct_pairs.
{ easy. }
{ step; simpl in *; try easy.
repeat split; lia.
}
Qed.
#[global] Hint Resolve encoding_indexes_is_valid : Data_encoding_db.
Module Message_result.
Import Proto_alpha.Tx_rollup_l2_apply.Message_result.
Module transaction_result.
Module Valid.
Validity predicate [transaction_result].
Definition t (x : transaction_result) : Prop :=
match x with
| Transaction_success ⇒ True
| Transaction_failure {|
transaction_result.Transaction_failure.index := index;
|} ⇒
Pervasives.Int31.Valid.t index
end.
End Valid.
End transaction_result.
Module deposit_result.
Module Valid.
match x with
| Transaction_success ⇒ True
| Transaction_failure {|
transaction_result.Transaction_failure.index := index;
|} ⇒
Pervasives.Int31.Valid.t index
end.
End Valid.
End transaction_result.
Module deposit_result.
Module Valid.
Validity predicate [deposit_result].
Definition t (x : deposit_result) : Prop :=
match x with
| Deposit_success indexes ⇒ indexes.Valid.t indexes
| Deposit_failure _ ⇒ True
end.
End Valid.
End deposit_result.
match x with
| Deposit_success indexes ⇒ indexes.Valid.t indexes
| Deposit_failure _ ⇒ True
end.
End Valid.
End deposit_result.
The encoding [encoding_transaction_result] is valid.
Lemma encoding_transaction_result_is_valid :
Data_encoding.Valid.t transaction_result.Valid.t
encoding_transaction_result.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_transaction_result_is_valid
: Data_encoding_db.
Data_encoding.Valid.t transaction_result.Valid.t
encoding_transaction_result.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_transaction_result_is_valid
: Data_encoding_db.
The encoding [encoding_deposit_result] is valid.
Lemma encoding_deposit_result_is_valid :
Data_encoding.Valid.t deposit_result.Valid.t encoding_deposit_result.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_deposit_result_is_valid : Data_encoding_db.
Module Batch_V1.
Module Valid.
Data_encoding.Valid.t deposit_result.Valid.t encoding_deposit_result.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_deposit_result_is_valid : Data_encoding_db.
Module Batch_V1.
Module Valid.
Validity predicate for [t].
Definition t (x : Batch_V1.t) : Prop :=
match x with
| Batch_V1.Batch_result {|
Batch_V1.t.Batch_result.results := results;
Batch_V1.t.Batch_result.indexes := indexes;
|} ⇒
List.Forall
(fun '(transaction, result) ⇒
Tx_rollup_l2_batch.V1.transaction.Valid.t transaction ∧
transaction_result.Valid.t result
)
results ∧
indexes.Valid.t indexes
end.
End Valid.
End Batch_V1.
End Message_result.
match x with
| Batch_V1.Batch_result {|
Batch_V1.t.Batch_result.results := results;
Batch_V1.t.Batch_result.indexes := indexes;
|} ⇒
List.Forall
(fun '(transaction, result) ⇒
Tx_rollup_l2_batch.V1.transaction.Valid.t transaction ∧
transaction_result.Valid.t result
)
results ∧
indexes.Valid.t indexes
end.
End Valid.
End Batch_V1.
End Message_result.