🍬 Script_int_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.Script_int_repr.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Compare.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.

#[global] Hint Unfold
  Script_int_repr.zero
  Script_int_repr.zero_n
  Script_int_repr.one_n
  Script_int_repr.of_int
  Script_int_repr.of_int32
  Script_int_repr.of_int64
  Script_int_repr.of_zint
  Script_int_repr.to_int
  Script_int_repr.to_int64
  Script_int_repr.to_zint
  Script_int_repr.add
  Script_int_repr.sub
  Script_int_repr.mul
  Script_int_repr.ediv
  Script_int_repr.add_n
  Script_int_repr.succ_n
  Script_int_repr.mul_n
  Script_int_repr.ediv_n
  Script_int_repr.abs
  Script_int_repr.neg
  Script_int_repr.int_value
  : tezos_z.

Module N.
  Module Valid.
    Definition t x : Prop :=
      0 ≤ let 'Script_int_repr.Num_tag n_value := x in n_value.
  End Valid.
End N.

Lemma compare_is_valid :
  Compare.Valid.t (fun _ ⇒ True) id Script_int_repr.compare.
Proof.
  apply (Compare.equality (
    let proj '(Script_int_repr.Num_tag z) := z in
    Compare.projection proj Z.compare
  )); [sauto lq: on|].
  eapply Compare.implies.
  { eapply Compare.projection_is_valid.
    apply Compare.z_is_valid.
  }
  all: sauto.
Qed.

Lemma z_encoding_is_valid :
  Data_encoding.Valid.t (fun _ ⇒ True) Script_int_repr.z_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve z_encoding_is_valid : Data_encoding_db.

Lemma n_encoding_is_valid :
  Data_encoding.Valid.t N.Valid.t Script_int_repr.n_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve n_encoding_is_valid : Data_encoding_db.