Skip to main content

🐆 Tx_rollup_message_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_repr.

Require Import TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Blake2B.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Int64.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.S.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Signature.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_l2_address.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_l2_qty.

Module Deposit.
  Module Valid.
    Import Tx_rollup_message_repr.deposit.

    Record t (p : Tx_rollup_message_repr.deposit) : Prop := {
      destination : Indexable.Value.Valid.t p.(destination);
      amount : Tx_rollup_l2_qty.Valid.t p.(amount);
    }.
  End Valid.
End Deposit.

Lemma deposit_encoding_is_valid : Data_encoding.Valid.t Deposit.Valid.t
  Tx_rollup_message_repr.deposit_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve deposit_encoding_is_valid : Data_encoding_db.

Lemma batch_encoding_is_valid : Data_encoding.Valid.t (fun _True)
  Tx_rollup_message_repr.batch_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve batch_encoding_is_valid : Data_encoding_db.

Module Valid.
  Definition t (x : Tx_rollup_message_repr.t) : Prop :=
    match x with
    | Tx_rollup_message_repr.Batch _True
    | Tx_rollup_message_repr.Deposit dDeposit.Valid.t d
    end.
End Valid.

Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t
  Tx_rollup_message_repr.encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.