Skip to main content

🚗 Migration_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.Environment.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Receipt_repr.

Require TezosOfOCaml.Proto_alpha.Migration_repr.
Import Migration_repr.origination_result.

Module Valid.
  Definition t (ors : list Migration_repr.origination_result) : Prop :=
    List.Forall
      (fun orReceipt_repr.Balance_updates.Valid.t
                or.(balance_updates)) ors.
End Valid.

Lemma origination_result_list_encoding_is_valid :
  Data_encoding.Valid.t Valid.t Migration_repr.origination_result_list_encoding.
  Data_encoding.Valid.data_encoding_auto.
  hauto l: on use: Forall_forall.
Qed.
#[global] Hint Resolve origination_result_list_encoding_is_valid : Data_encoding_db.