🕰️ Time_repr.v
Proofs
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Int64.Valid.t (x -Z y) → Time_repr.op_minus x y = x -Z y.
Proof.
intro; apply Int64.normalize_identity; auto.
Qed.