Skip to main content

🍃 Time.v


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
  : 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
    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.