Use literal overloading for epochs (#387)

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}

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

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ˢ }

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

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ᶜ

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