Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Improved performance when adding epochs #554

Merged
merged 2 commits into from
Aug 28, 2024
Merged

Improved performance when adding epochs #554

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
993b50b
Disabling committee updates for testing
Soupstraw Aug 27, 2024
b82584b
Disabling maxTerm check
Soupstraw Aug 27, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 5 additions & 3 deletions src/Ledger/GovernanceActions/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,9 @@ instance
NoConfidence → success (_ , Enact-NoConf)
(UpdateCommittee new rem q) →
case ¿ ∀[ term ∈ range new ]
term ≤ s .pparams .proj₁ .PParams.ccMaxTermLength +ᵉ e ¿ of λ where
(yes p) → success (-, Enact-NewComm p)
term ≤ s .pparams .proj₁ .PParams.ccMaxTermLength +ᵉ' e ¿ of λ where
(yes p) → success (-, Enact-NewComm
(subst (λ x → ∀[ term ∈ range new ] term ≤ x) (sym +ᵉ≡+ᵉ') p))
(no ¬p) → failure "ENACT failed at ∀[ term ∈ range new ] term ≤ (s .pparams .proj₁ .PParams.ccMaxTermLength +ᵉ e)"
(NewConstitution dh sh) → success (-, Enact-NewConst)
(TriggerHF v) → success (-, Enact-HF)
Expand All @@ -39,7 +40,8 @@ instance
... | .UpdateCommittee new rem q | Enact-NewComm p
rewrite dec-yes
(¿ ∀[ term ∈ range new ] term
≤ s .pparams .proj₁ .PParams.ccMaxTermLength +ᵉ e ¿) p .proj₂
≤ s .pparams .proj₁ .PParams.ccMaxTermLength +ᵉ' e ¿)
(subst (λ x → ∀[ term ∈ range new ] term ≤ x) +ᵉ≡+ᵉ' p) .proj₂
= refl
... | .NewConstitution dh sh | Enact-NewConst = refl
... | .TriggerHF v | Enact-HF = refl
Expand Down
20 changes: 16 additions & 4 deletions src/Ledger/Types/Epoch.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,10 @@ open import Algebra using (Semiring)
open import Relation.Binary
open import Data.Nat.Properties using (+-*-semiring)

additionVia : ∀{A : Set} → (A → A) → ℕ → A → A
additionVia sucFun zero r = r
additionVia sucFun (suc l) r = sucFun (additionVia sucFun l r)

record EpochStructure : Type₁ where
field Slotʳ : Semiring 0ℓ 0ℓ
Epoch : Type; ⦃ DecEq-Epoch ⦄ : DecEq Epoch; ⦃ Show-Epoch ⦄ : Show Epoch
Expand All @@ -23,6 +27,12 @@ record EpochStructure : Type₁ where
StabilityWindow : Slot
sucᵉ : Epoch → Epoch

_+ᵉ_ = additionVia sucᵉ

field
_+ᵉ'_ : ℕ → Epoch → Epoch
+ᵉ≡+ᵉ' : ∀ {a b} → a +ᵉ b ≡ a +ᵉ' b

-- preorders and partial orders

instance
Expand All @@ -48,10 +58,6 @@ record EpochStructure : Type₁ where
ℕ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 ._+_ = _+ˢ_
Expand All @@ -70,6 +76,10 @@ record GlobalConstants : Type₁ where
Quorum : ℕ
NetworkId : Network

ℕ+ᵉ≡+ᵉ' : ∀ {a b} → additionVia suc a b ≡ a + b
ℕ+ᵉ≡+ᵉ' {zero} {b} = refl
ℕ+ᵉ≡+ᵉ' {suc a} {b} = cong suc (ℕ+ᵉ≡+ᵉ' {a} {b})

ℕEpochStructure : EpochStructure
ℕEpochStructure = λ where
.Slotʳ → +-*-semiring
Expand All @@ -78,6 +88,8 @@ record GlobalConstants : Type₁ where
.firstSlot e → e * SlotsPerEpochᶜ
.StabilityWindow → StabilityWindowᶜ
.sucᵉ → suc
._+ᵉ'_ → _+_
.+ᵉ≡+ᵉ' {a} {b} → ℕ+ᵉ≡+ᵉ' {a} {b}

where open EpochStructure

Expand Down
Loading