🍃 Time.v

Proofs

See code, Gitlab

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.

#[global] Hint Unfold
    Time.op_eq
    Time.op_ltgt
    Time.op_lt
    Time.op_lteq
    Time.op_gteq
    Time.op_gt
    Time.compare
    Time.equal
    Time.max
    Time.min
    Time.add
    Time.diff_value
    Time.of_seconds
    Time.to_seconds
  : tezos_z.

Module Valid.
  Definition t (n : Time.t) : Prop :=
    Int64.min_int ≤ n ≤ Int64.max_int.
  #[global] Hint Unfold t : tezos_z.
End Valid.

Axiom of_notation_to_notation : ∀ time,
  let notation := Time.to_notation time in
  Time.of_notation notation =
  if String.equal notation "out_of_range" then
    None
  else
    Some time.

Axiom of_notation_to_notation_eq : ∀ t,
  Valid.t t →
  Time.of_notation (Time.to_notation t) = Some t.

Axiom of_notation_to_string_eq : ∀ t,
  Time.of_notation (Z.to_string t) = Some t.

Axiom to_notation_of_string_eq : ∀ s,
  Time.to_notation (Z.of_string s) = s.

Axiom of_notation_some_implies : ∀ s t,
  Time.of_notation s = Some t →
  Time.to_notation t = s ∧ Z.to_string t = s.

The encoding [internal_inbox_message_encoding] is valid.

Axiom encoding_is_valid : Data_encoding.Valid.t (fun _ ⇒ True) Time.encoding.

#[global] Hint Resolve encoding_is_valid : Data_encoding_db.