val ts_geq : t1: Zeta.Time.timestamp -> t2: Zeta.Time.timestamp -> Prims.bool
let ts_geq (t1 t2: timestamp) =
  not (ts_lt t1 t2)
module Zeta.Time

(**
 * Time in zeta is two dimensional, consisting of (epoch, counter). All verifier threads have
 * internal clocks tracking time of this format and these clocks are used to associate
 * timestamps to "events" - state machine transitions - which ultimately are used to
 * characterize correctness.
 *)

(**
 * The first component of time in zeta. An epoch is the unit of verification in the sense
 * all events in an epoch are verified to be correct only after all threads transition
 * to the next epoch.
 *)
let epoch = nat

(**
 * A counter within an epoch.
 *)
let counter = nat

type timestamp = {
  e: epoch;
  c: counter;
}

(* next timestamp *)
let next (t: timestamp)
  = { e = t.e; c = t.c + 1 }

(* return the epoch of a timestamp *)
let epoch_of (t: timestamp)
  = t.e

(* first timestamp of an epoch *)
let first (e: epoch): timestamp
  = { e; c = 0 }

(* < relation of timestamps *)
let ts_lt (t1 t2: timestamp) =
  t1.e < t2.e || t1.e = t2.e && t1.c < t2.c
/
prims.fst.checked FStar.Pervasives.fsti.checked
Zeta.Time.fsti
t1: Zeta.Time.timestamp -> t2: Zeta.Time.timestamp -> Prims.bool
Zeta.Time.timestamp Prims.op_Negation Zeta.Time.ts_lt Prims.bool
let ts_geq (t1 t2: timestamp) =
  
not (ts_lt t1 t2)