🍃 Time.v
Proofs
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.
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.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.