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

Require TezosOfOCaml.Proto_alpha.Script_timestamp.

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

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

Lemma compare_is_valid :
  Compare.Valid.t (fun _ ⇒ True) id Script_timestamp.compare.
Proof.
  apply (Compare.equality (
    let proj '(Script_timestamp.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.to_zint t) →
  Script_timestamp.of_string
    (Script_timestamp.to_string t) = Some t.
  intros.
  unfold Script_timestamp.of_string, Script_timestamp.to_string.
  destruct_all Script_timestamp.t; simpl in ×.
  rewrite Z.to_int64_eq by lia.
  unfold Time.of_seconds, Time.to_seconds,
    Script_timestamp.of_int64, Z.of_int64.
  rewrite Option.catch_no_errors.
  rewrite Time.of_notation_to_notation_eq; lia.
Qed.

to_string and of_string are inverse

Lemma to_string_of_string_is_inverse : ∀ t s,
  Int64.Valid.t (Script_timestamp.to_zint t)→
  Script_timestamp.of_string s = Some t →
  Script_timestamp.to_string t = s.
Proof.
  autounfold with script_timestamp_repr.
  intros t s HInt H.
  destruct t as [t].
  rewrite Option.catch_no_errors.
  rewrite Z.to_int64_eq by lia.
  destruct Time.of_notation eqn:H_notation_eq.
  { pose proof (Time.of_notation_some_implies _ _ H_notation_eq) as H_inv.
    hauto lq: on.
  }
  { rewrite Option.catch_no_errors in H.
    inversion H.
    apply Time.to_notation_of_string_eq.
  }
Qed.

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