JAR: JAM Axiomatic Reference

7.1. Timekeeping🔗

🔗def
Jar.newTimeslot [Jar.JamConfig] (h : Jar.Header) : Jar.Timeslot
Jar.newTimeslot [Jar.JamConfig]
  (h : Jar.Header) : Jar.Timeslot

τ' ≡ H_t. GP eq (28). The new timeslot is simply the block's timeslot.

🔗def
Jar.epochIndex [Jar.JamConfig] (t : Jar.Timeslot) : Nat
Jar.epochIndex [Jar.JamConfig]
  (t : Jar.Timeslot) : Nat

Epoch index: e = ⌊τ / E⌋. GP eq (34).

🔗def
Jar.epochSlot [Jar.JamConfig] (t : Jar.Timeslot) : Nat
Jar.epochSlot [Jar.JamConfig]
  (t : Jar.Timeslot) : Nat

Slot within epoch: m = τ mod E. GP eq (34).

🔗def
Jar.isEpochChange [Jar.JamConfig] (prior posterior : Jar.Timeslot) :
  Bool
Jar.isEpochChange [Jar.JamConfig]
  (prior posterior : Jar.Timeslot) : Bool

Whether the block crosses an epoch boundary.