🍬 Script_timestamp_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.Environment.Proofs.Int64.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Option.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Time.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Z.

Require TezosOfOCaml.Proto_alpha.Script_timestamp_repr.

#[global] Hint Unfold
  Script_timestamp_repr.of_int64
  Script_timestamp_repr.diff_value
  Script_timestamp_repr.sub_delta
  Script_timestamp_repr.add_delta
  Script_timestamp_repr.to_zint
  Script_timestamp_repr.of_zint
  : tezos_z.

#[local] Hint Unfold
  Script_timestamp_repr.of_string
  Script_timestamp_repr.to_string
  Script_timestamp_repr.of_int64
  Script_timestamp_repr.to_num_str
  Script_timestamp_repr.to_notation
  Script_timestamp_repr.to_zint
  Time_repr.of_notation
  Time_repr.to_seconds
  Time_repr.to_notation
  of_seconds
  of_int64
  to_int64
  : script_timestamp_repr.

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

of_string (to_string t) preserves t

Lemma of_string_to_string_is_inverse : ∀ t,
  Int64.Valid.t (Script_timestamp_repr.to_zint t) →
  Script_timestamp_repr.of_string
    (Script_timestamp_repr.to_string t) = Some t.
  intros.
  autounfold with script_timestamp_repr in ×.
  destruct t as [t].
  rewrite Int64.normalize_identity; [|easy].
  destruct (Option.catch None (fun _ : unit ⇒ to_notation t)) eqn:?.
  { apply Option.catch_some_eq in Heqo. rewrite Heqo.
    now rewrite Time.of_notation_to_notation_eq. }
  { now rewrite Time.of_notation_to_string_eq. }
Qed.

to_string and of_string are inverse

Lemma to_string_of_string_is_inverse : ∀ t s,
  Int64.Valid.t (Script_timestamp_repr.to_zint t)→
  Script_timestamp_repr.of_string s = Some t →
  Script_timestamp_repr.to_string t = s.
  autounfold with script_timestamp_repr.
  intros t s HInt H.
  destruct t as [t].
  destruct (of_notation s) eqn:Eq_of_notation in H.
  { destruct Option.catch eqn:Eq_catch.
    { apply Time.of_notation_some_implies in Eq_of_notation.
      injection H. intros H1. rewrite H1 in Eq_of_notation.
      clear H H1. apply Option.catch_some_eq in Eq_catch.
      rewrite Int64.normalize_identity in Eq_catch; [|easy].
      now rewrite Eq_catch. }
    { apply Time.of_notation_some_implies. hauto l: on. } }
  { apply Option.catch_some_eq in H.
    destruct Option.catch eqn:Eq_catch.
    { apply Option.catch_some_eq in Eq_catch.
      rewrite Int64.normalize_identity in Eq_catch; [|easy].
      injection H as H.
      rewrite H in Eq_catch.
      now rewrite Time.to_notation_of_string_eq in Eq_catch. }
    { injection H as H. rewrite H.
      now rewrite Z.to_string_of_string_eq. } }
Qed.

Lemma encoding_is_valid :
  Data_encoding.Valid.t (fun _ ⇒ True) Script_timestamp_repr.encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.