🕰️ Time_repr.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Time_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Int64.
Require TezosOfOCaml.Environment.V8.Proofs.Time.
Require TezosOfOCaml.Proto_alpha.Proofs.Period_repr.

[of_seconds_string] inverts [to_seconds_string]

Lemma of_seconds_string_to_seconds_string : ∀ t : Time_repr.t,
  Time_repr.of_seconds_string (Time_repr.to_seconds_string t) = Some t.
Proof.
  intro t.
  unfold Time_repr.to_seconds_string.
  unfold Time_repr.of_seconds_string.
  rewrite Int64.of_string_opt_to_string.
  reflexivity.
Qed.

[to_seconds_string] inverts [of_seconds_string]

Lemma to_seconds_string_of_seconds_string (str : string) :
  match Time_repr.of_seconds_string str with
  | Some t ⇒ Time_repr.to_seconds_string t = str
  | None ⇒ True
  end.
Proof.
  unfold Time_repr.of_seconds_string.
  pose proof (Int64.to_string_of_string_opt str) as pf.
  destruct (of_string_opt str); auto.
Qed.

[of_seconds_string] produces valid times

Lemma of_seconds_string_valid (str : string) :
  match Time_repr.of_seconds_string str with
  | Some t ⇒ Time.Valid.t t
  | None ⇒ True
  end.
Proof.
  unfold Time_repr.of_seconds_string.
  pose proof (Int64.of_string_opt_is_valid str) as pf.
  destruct (of_string_opt str); auto.
Qed.

[op_plusquestion] produces valid times

Lemma op_plusquestion_valid (x : Time.t) (y : Period_repr.period) :
  match Time_repr.op_plusquestion x y with
  | Pervasives.Ok t ⇒ Time.Valid.t t
  | Pervasives.Error _ ⇒ True
  end.
Proof.
  unfold Time_repr.op_plusquestion.
  destruct Time_repr.op_lt eqn:?; simpl; [lia|].
  destruct Time_repr.op_lt eqn:? in |- *; simpl; lia.
Qed.

[op_plusquestion] is the same as addition when [x +Z y] is valid

Lemma op_plusquestion_eq (x : Time.t) (y : Period_repr.period) :
  Int64.Valid.t (x +Z y) →
  match Time_repr.op_plusquestion x y with
  | Pervasives.Ok t ⇒ t = x +Z y
  | Pervasives.Error _ ⇒ True
  end.
Proof.
  intro Hv.
  destruct (Time_repr.op_plusquestion x y) eqn:Hres; auto.
  unfold Time_repr.op_plusquestion, of_seconds, Time_repr.op_lt,
    Time.add, Period_repr.to_seconds, "+i64" in Hres; simpl in Hres.
  destruct (x <? 0).
  { inversion Hres.
    apply Int64.normalize_identity; auto.
  }
  { destruct Z.ltb; inversion Hres.
    apply Int64.normalize_identity; auto.
  }
Qed.

[op_minusquestion] produces valid periods

Lemma op_minusquestion_valid (x y : Time.t) :
  match Time_repr.op_minusquestion x y with
  | Pervasives.Ok t ⇒ Period_repr.Valid.t t
  | Pervasives.Error _ ⇒ True
  end.
Proof.
  destruct (Time_repr.op_minusquestion x y) eqn:Hres; auto.
  unfold Time_repr.op_minusquestion, record_trace,
    Period_repr.of_seconds in Hres.
  simpl in Hres.
  unfold Period_repr.Internal.create, Period_repr.Internal.op_gteq,
    diff_value, Period_repr.Internal.zero in Hres.
  simpl in Hres.
  destruct (y -i64 x >=? 0) eqn:?; inversion Hres.
  lia.
Qed.

[op_minusquestion] is the same as subtraction when [x -Z y] is valid

Lemma op_minusquestion_eq (x y : Time.t) :
  Int64.Valid.t (y -Z x) →
  match Time_repr.op_minusquestion x y with
  | Pervasives.Ok t ⇒ t = y -Z x
  | Pervasives.Error _ ⇒ True
  end.
Proof.
  intro Hv.
  destruct (Time_repr.op_minusquestion x y) eqn:Hres; auto.
  unfold Time_repr.op_minusquestion, Period_repr.of_seconds,
    record_trace in Hres.
  simpl in Hres.
  unfold Period_repr.Internal.create, Period_repr.Internal.op_gteq,
    diff_value, Period_repr.Internal.zero in Hres.
  simpl in Hres.
  destruct (y -i64 x >=? 0); inversion Hres.
  lia.
Qed.

[op_minus] produces valid times

Lemma op_minus_valid (x : Time.t) (y : Period_repr.period) :
  Time.Valid.t (Time_repr.op_minus x y).
Proof.
  apply Int64.normalize_is_valid.
Qed.

[op_minus] is the same as subtraction when [x -Z y] is valid

Lemma op_minus_eq (x : Time.t) (y : Period_repr.period) :
  Int64.Valid.t (x -Z y) → Time_repr.op_minus x y = x -Z y.
Proof.
  intro; apply Int64.normalize_identity; auto.
Qed.