Skip to main content

⛽ Gas_comparable_input_size.v

Proofs

See code, See simulations, Gitlab , OCaml

The simulation [dep_size_of_comparable_value] is valid.
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.