🚗 Migration_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.

Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Receipt_repr.

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

Module origination_result.
  Module Valid.
    Import Proto_alpha.Migration_repr.origination_result.

Validity predicate for [origination_result].

    Record t (x : Migration_repr.origination_result) : Prop := {
      balance_updates :
        Receipt_repr.balance_updates.Valid.t x.(balance_updates);
    }.
  End Valid.
End origination_result.

The encoding [origination_result_list_encoding] is valid.

Lemma origination_result_list_encoding_is_valid :
  Data_encoding.Valid.t (List.Forall origination_result.Valid.t)
    Migration_repr.origination_result_list_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  intros l H.
  eapply List.Forall_impl; try apply H.
  sauto l: on.
Qed.
#[global] Hint Resolve origination_result_list_encoding_is_valid :
  Data_encoding_db.