⛽ Gas_comparable_input_size.v

Proofs

See code, See simulations, 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.Gas_comparable_input_size.

Require TezosOfOCaml.Proto_alpha.Simulations.Gas_comparable_input_size.
Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_family.

Validity predicate for [t].

Module Valid.
  Record t (l : Proto_alpha.Gas_comparable_input_size.t) : Prop := {
      pervasives_valid : Pervasives.Int.Valid.t l;
    }.
End Valid.

The encoding [encoding] is valid.

Lemma encoding_is_valid :
  Data_encoding.Valid.t Valid.t Gas_comparable_input_size.encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  intros; split.
  { apply Int64.of_int_is_valid; apply H. }
  { apply Int64.to_int_of_int; apply H. }
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

Module Micheline_size.

Validity predicate for [micheline_size].

  Module Valid.
    Import Gas_comparable_input_size.micheline_size.
    Record t (l : Gas_comparable_input_size.micheline_size) : Prop := {
        traversal : Pervasives.Int.Valid.t l.(traversal);
        int_bytes : Pervasives.Int.Valid.t l.(int_bytes);
        string_bytes : Pervasives.Int.Valid.t l.(string_bytes);
      }.
  End Valid.
End Micheline_size.

The encoding [micheline_size_encoding] is valid.

Lemma micheline_size_encoding_is_valid :
  Data_encoding.Valid.t Micheline_size.Valid.t
    Gas_comparable_input_size.micheline_size_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve micheline_size_encoding_is_valid : Data_encoding_db.