From bba943019b73609c59d7980bb79a02bd26f727e5 Mon Sep 17 00:00:00 2001 From: Andre Knispel Date: Thu, 18 Apr 2024 15:26:23 +0200 Subject: [PATCH] Use literal overloading for epochs (#387) --- src/Ledger/Epoch.lagda | 8 +++++--- src/Ledger/Epoch/Properties.agda | 6 ++++-- src/Ledger/PPUp.lagda | 10 ++++------ src/Ledger/PPUp/Properties.agda | 10 +++++----- src/Ledger/Types/Epoch.agda | 5 +++++ src/Prelude.agda | 5 +++++ 6 files changed, 28 insertions(+), 16 deletions(-) diff --git a/src/Ledger/Epoch.lagda b/src/Ledger/Epoch.lagda index 46242d5d..104f0b76 100644 --- a/src/Ledger/Epoch.lagda +++ b/src/Ledger/Epoch.lagda @@ -6,6 +6,8 @@ open import Data.Nat.Properties using (+-0-monoid; +-0-commutativeMonoid) open import Data.List using (filter) +open import Agda.Builtin.FromNat + open import Ledger.Prelude open import Ledger.Abstract open import Ledger.Transaction @@ -100,7 +102,7 @@ its results, i.e: certState' = ⟦ record dState { rewards = rewards ∪⁺ refunds } , ⟦ pools ∣ retired ᶜ , retiring ∣ retired ᶜ ⟧ᵖ - , ⟦ if null govSt' then mapValues sucᵉ dreps else dreps + , ⟦ if null govSt' then mapValues (1 +_) dreps else dreps , ccHotKeys ∣ ccCreds (es .EnactState.cc) ⟧ᵛ ⟧ᶜˢ utxoSt' = ⟦ utxo , 0 , deposits ∣ mapˢ (proj₁ ∘ proj₂) removedGovActions ᶜ , 0 ⟧ᵘ @@ -132,13 +134,13 @@ data \end{code} \begin{code} NEWEPOCH-New : - e ≡ sucᵉ lastEpoch + e ≡ lastEpoch + 1 → Γ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps' ──────────────────────────────── Γ ⊢ ⟦ lastEpoch , eps ⟧ⁿᵉ ⇀⦇ e ,NEWEPOCH⦈ ⟦ e , eps' ⟧ⁿᵉ NEWEPOCH-Not-New : - e ≢ sucᵉ lastEpoch + e ≢ lastEpoch + 1 ──────────────────────────────── Γ ⊢ ⟦ lastEpoch , eps ⟧ⁿᵉ ⇀⦇ e ,NEWEPOCH⦈ ⟦ lastEpoch , eps ⟧ⁿᵉ \end{code} diff --git a/src/Ledger/Epoch/Properties.agda b/src/Ledger/Epoch/Properties.agda index 6f68fa69..2aaf1622 100644 --- a/src/Ledger/Epoch/Properties.agda +++ b/src/Ledger/Epoch/Properties.agda @@ -4,6 +4,8 @@ open import Ledger.Prelude open import Ledger.Transaction open import Ledger.Abstract +open import Agda.Builtin.FromNat + module Ledger.Epoch.Properties (txs : _) (open TransactionStructure txs) (abs : AbstractFunctions txs) (open AbstractFunctions abs) @@ -52,12 +54,12 @@ module _ {Γ : NewEpochEnv} {nes : NewEpochState} {e : Epoch} where open NewEpochState nes NEWEPOCH-total : ∃[ nes' ] Γ ⊢ nes ⇀⦇ e ,NEWEPOCH⦈ nes' - NEWEPOCH-total with e ≟ sucᵉ lastEpoch + NEWEPOCH-total with e ≟ lastEpoch + 1 ... | yes p = ⟦ e , proj₁ EPOCH-total' ⟧ⁿᵉ , NEWEPOCH-New p (EPOCH-total' .proj₂) ... | no ¬p = -, NEWEPOCH-Not-New ¬p NEWEPOCH-complete : ∀ nes' → Γ ⊢ nes ⇀⦇ e ,NEWEPOCH⦈ nes' → proj₁ NEWEPOCH-total ≡ nes' - NEWEPOCH-complete nes' h with e ≟ sucᵉ lastEpoch | h + NEWEPOCH-complete nes' h with e ≟ lastEpoch + 1 | h ... | yes p | NEWEPOCH-New x x₁ rewrite EPOCH-complete' _ x₁ = refl ... | yes p | NEWEPOCH-Not-New x = ⊥-elim $ x p ... | no ¬p | NEWEPOCH-New x x₁ = ⊥-elim $ ¬p x diff --git a/src/Ledger/PPUp.lagda b/src/Ledger/PPUp.lagda index 1e5b9881..f8c8e328 100644 --- a/src/Ledger/PPUp.lagda +++ b/src/Ledger/PPUp.lagda @@ -6,7 +6,7 @@ open import Agda.Builtin.FromNat open import Algebra; open import Algebra.Literals import Data.Product.Properties as × -import Data.Nat as ℕ; import Data.Nat.Properties as ℕ; import Data.Nat.Literals as ℕ +import Data.Nat as ℕ; import Data.Nat.Properties as ℕ open import Ledger.Prelude hiding (_*_) open import Ledger.Transaction @@ -17,8 +17,6 @@ open Semiring Slotʳ using (_*_) open Semiring-Lit Slotʳ private variable m n : ℕ - -instance _ = ℕ.number \end{code} \begin{figure*}[h] \begin{code} @@ -71,7 +69,7 @@ data _⊢_⇀⦇_,PPUP⦈_ : PPUpdateEnv → PPUpdateState → Maybe Update → PPUpdateCurrent : let open PPUpdateEnv Γ in dom pup ⊆ dom genDelegs → All (isViableUpdate pparams) (range pup) - → slot + (2 * StabilityWindow) < firstSlot (sucᵉ (epoch slot)) + → slot + 2 * StabilityWindow < firstSlot (epoch slot + 1) → epoch slot ≡ e ──────────────────────────────── Γ ⊢ record { pup = pupˢ ; fpup = fpupˢ } ⇀⦇ just (pup , e) ,PPUP⦈ @@ -80,8 +78,8 @@ data _⊢_⇀⦇_,PPUP⦈_ : PPUpdateEnv → PPUpdateState → Maybe Update → PPUpdateFuture : let open PPUpdateEnv Γ in dom pup ⊆ dom genDelegs → All (isViableUpdate pparams) (range pup) - → firstSlot (sucᵉ (epoch slot)) ≤ slot + (2 * StabilityWindow) - → sucᵉ (epoch slot) ≡ e + → firstSlot (epoch slot + 1) ≤ slot + 2 * StabilityWindow + → epoch slot + 1 ≡ e ──────────────────────────────── Γ ⊢ record { pup = pupˢ ; fpup = fpupˢ } ⇀⦇ just (pup , e) ,PPUP⦈ record { pup = pupˢ ; fpup = pup ∪ˡ fpupˢ } diff --git a/src/Ledger/PPUp/Properties.agda b/src/Ledger/PPUp/Properties.agda index fb9d0c23..f388e468 100644 --- a/src/Ledger/PPUp/Properties.agda +++ b/src/Ledger/PPUp/Properties.agda @@ -1,6 +1,6 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (_+_; _*_) +open import Ledger.Prelude hiding (_*_) open Computational ⦃...⦄; open HasDecPartialOrder ⦃...⦄ open import Ledger.Transaction @@ -11,22 +11,22 @@ open import Ledger.PPUp txs private -- Ring literals open import Agda.Builtin.FromNat - open import Algebra; open Semiring Slotʳ hiding (refl) + open import Algebra; open Semiring Slotʳ using (_*_) open import Algebra.Literals; open Semiring-Lit Slotʳ Current-Property : PPUpdateEnv → Update → Set Current-Property Γ (pup , e) = let open PPUpdateEnv Γ in dom pup ⊆ dom genDelegs × All (isViableUpdate pparams) (range pup) - × (slot + (2 * StabilityWindow)) < firstSlot (sucᵉ (epoch slot)) + × slot + 2 * StabilityWindow < firstSlot (epoch slot + 1) × epoch slot ≡ e Future-Property : PPUpdateEnv → Update → Set Future-Property Γ (pup , e) = let open PPUpdateEnv Γ in dom pup ⊆ dom genDelegs × All (isViableUpdate pparams) (range pup) - × firstSlot (sucᵉ (epoch slot)) ≤ (slot + (2 * StabilityWindow)) - × sucᵉ (epoch slot) ≡ e + × firstSlot (epoch slot + 1) ≤ slot + 2 * StabilityWindow + × epoch slot + 1 ≡ e instance Computational-PPUP : Computational _⊢_⇀⦇_,PPUP⦈_ String diff --git a/src/Ledger/Types/Epoch.agda b/src/Ledger/Types/Epoch.agda index 6c0f3f7f..0cc4804f 100644 --- a/src/Ledger/Types/Epoch.agda +++ b/src/Ledger/Types/Epoch.agda @@ -4,6 +4,7 @@ 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) @@ -58,6 +59,10 @@ record EpochStructure : Set₁ where 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ᶜ diff --git a/src/Prelude.agda b/src/Prelude.agda index 2c4eb3ac..d87b6b59 100644 --- a/src/Prelude.agda +++ b/src/Prelude.agda @@ -70,3 +70,8 @@ open import Class.Show public infix 2 ∃₂-syntax syntax ∃₂-syntax (λ x y → C) = ∃₂[ x , y ] C + +-- Instance for number literals, not enabled by default +import Data.Nat.Literals as ℕ + +instance Number-ℕ = ℕ.number