-
Notifications
You must be signed in to change notification settings - Fork 13
/
Epoch.agda
84 lines (63 loc) · 2.37 KB
/
Epoch.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
{-# OPTIONS --safe #-}
module Ledger.Types.Epoch where
open import Ledger.Prelude hiding (compare; Rel)
open import Agda.Builtin.FromNat
open import Algebra using (Semiring)
open import Relation.Binary
open import Data.Nat.Properties using (+-*-semiring)
record EpochStructure : Set₁ where
field Slotʳ : Semiring 0ℓ 0ℓ
Epoch : Set; ⦃ DecEq-Epoch ⦄ : DecEq Epoch
Slot = Semiring.Carrier Slotʳ
field ⦃ DecPo-Slot ⦄ : HasDecPartialOrder≡ {A = Slot}
⦃ DecEq-Slot ⦄ : DecEq Slot
epoch : Slot → Epoch
firstSlot : Epoch → Slot
StabilityWindow : Slot
sucᵉ : Epoch → Epoch
-- preorders and partial orders
instance
preoEpoch : HasPreorder
preoEpoch = hasPreorderFromStrictPartialOrder {_<_ = _<_ on firstSlot}
record
{ isEquivalence = isEquivalence
; irrefl = λ where refl → <-irrefl {A = Slot} refl
; trans = <-trans {A = Slot}
; <-resp-≈ = (λ where refl → id) , (λ where refl → id)
}
_ = _<_ {A = Slot} ⁇² ∋ it
_ = _≤_ {A = Slot} ⁇² ∋ it
_ = _<_ {A = Epoch} ⁇² ∋ it
_ = _≤_ {A = Epoch} ⁇² ∋ it
-- addition
open Semiring Slotʳ renaming (_+_ to _+ˢ_)
ℕtoEpoch : ℕ → Epoch
ℕtoEpoch zero = epoch 0#
ℕtoEpoch (suc n) = sucᵉ (ℕtoEpoch n)
_+ᵉ_ : ℕ → Epoch → Epoch
zero +ᵉ e = e
suc n +ᵉ e = sucᵉ (n +ᵉ e)
instance
addSlot : HasAdd Slot
addSlot ._+_ = _+ˢ_
addEpoch : HasAdd Epoch
addEpoch ._+_ e e' = epoch (firstSlot e + firstSlot e')
Number-Epoch : Number Epoch
Number-Epoch .Number.Constraint _ = ⊤
Number-Epoch .Number.fromNat x = ℕtoEpoch x
record GlobalConstants : Set₁ where
field Network : Set; ⦃ DecEq-Netw ⦄ : DecEq Network
SlotsPerEpochᶜ : ℕ; ⦃ NonZero-SlotsPerEpochᶜ ⦄ : NonZero SlotsPerEpochᶜ
StabilityWindowᶜ : ℕ
Quorum : ℕ
NetworkId : Network
ℕEpochStructure : EpochStructure
ℕEpochStructure = λ where
.Slotʳ → +-*-semiring
.Epoch → ℕ
.epoch slot → slot / SlotsPerEpochᶜ
.firstSlot e → e * SlotsPerEpochᶜ
.StabilityWindow → StabilityWindowᶜ
.sucᵉ → suc
where open EpochStructure
open GlobalConstants using (ℕEpochStructure) public