Skip to main content

🐆 Tx_rollup_l2_apply.v

Proofs

See code, Gitlab , OCaml

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.

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.

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.
Validity predicate [transaction_result].
      Definition t (x : transaction_result) : Prop :=
        match x with
        | Transaction_successTrue
        | 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 indexesindexes.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.

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