val first (e: epoch) : timestamp
val first (e: epoch) : timestamp
let first (e: epoch): timestamp
  = { e; c = 0 }
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
/
prims.fst.checked FStar.Pervasives.fsti.checked
Zeta.Time.fsti
e: Zeta.Time.epoch -> Zeta.Time.timestamp
Zeta.Time.epoch Zeta.Time.Mktimestamp Zeta.Time.timestamp
let first (e: epoch) : timestamp =
  
{ e = e; c = 0 }