val counter : Type0
let counter = nat
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.
/
prims.fst.checked FStar.Pervasives.fsti.checked
Zeta.Time.fsti
Type0
Prims.nat
let counter =
  
nat