improvements

src/Ledger/Conway/Specification/Certs.lagda.md

@@ -67,9 +67,6 @@ instance
 CCHotKeys : Type
 CCHotKeys = Credential ⇀ Maybe Credential
 
-DReps : Type
-DReps = Credential ⇀ Epoch
-
 PoolEnv : Type
 PoolEnv = PParams
 
@@ -94,9 +91,6 @@ StakeDelegs = Credential ⇀ KeyHash
 record HasCCHotKeys {a} (A : Type a) : Type a where
   field CCHotKeysOf : A → CCHotKeys
 
-record HasDReps {a} (A : Type a) : Type a where
-  field DRepsOf : A → DReps
-
 record HasPools {a} (A : Type a) : Type a where
   field PoolsOf : A → Pools
 
@@ -113,7 +107,6 @@ record HasStakeDelegs {a} (A : Type a) : Type a where
   field StakeDelegsOf : A -> StakeDelegs
 
 open HasCCHotKeys ⦃...⦄ public
-open HasDReps ⦃...⦄ public
 open HasPools ⦃...⦄ public
 open HasRetiring ⦃...⦄ public
 open HasRewards ⦃...⦄ public
@@ -126,14 +119,6 @@ open HasStakeDelegs ⦃...⦄ public
 ## Delegation Definitions
 
 
-An "active" `DRep`{.AgdaInductiveConstructor} is one whose expiry epoch is not less than the current epoch.
-
-```agda
-opaque
-  activeDReps : {A : Type} ⦃ _ : HasDReps A ⦄ → Epoch → A → ℙ Credential
-  activeDReps currentEpoch s = dom (filterᵐ (λ (_ , e) → currentEpoch ≤ e) (DRepsOf s))
-```
-
 ```agda
 data DCert : Type where
   delegate    : Credential → Maybe VDeleg → Maybe KeyHash → Coin → DCert

src/Ledger/Conway/Specification/Epoch.lagda.md

@@ -462,11 +462,11 @@ module VDelegDelegatedStake
   (dState       : DState)
   where
 
-  activeDReps' : ℙ Credential
-  activeDReps' = activeDReps currentEpoch gState
+  activeDReps : ℙ Credential
+  activeDReps = dom (DRepsOf gState ∣ currentEpoch ≤Expiry)
 
   activeVDelegs : ℙ VDeleg
-  activeVDelegs = mapˢ vDelegCredential activeDReps' ∪ ❴ vDelegNoConfidence ❵ ∪ ❴ vDelegAbstain ❵
+  activeVDelegs = mapˢ vDelegCredential activeDReps ∪ ❴ vDelegNoConfidence ❵ ∪ ❴ vDelegAbstain ❵
 
   -- compute the stake for a credential
   stakePerCredential : Credential → Coin

src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.lagda.md

@@ -198,9 +198,9 @@ module AcceptedByDRep-≈ {Γ Γ' : RatifyEnv} (Γ≈Γ' : RatifyEnv- Γ ≈ Γ'
   castVotes = refl
 
   opaque
-    unfolding activeDReps
+    unfolding DRepsOf_∣_≤Expiry
 
-    activeDReps-≡ᵉ : abdr.activeDReps' ≡ᵉ abdr'.activeDReps'
+    activeDReps-≡ᵉ : abdr.activeDReps ≡ᵉ abdr'.activeDReps
     activeDReps-≡ᵉ with Γ≈Γ'.currentEpoch
     ... | refl = dom-cong $
       begin
@@ -513,8 +513,8 @@ module VDelegDelegatedStake-≈
   module vds' = VDelegDelegatedStake currentEpoch utxoSt govSt gState' dState
 
   opaque
-    unfolding activeDReps
-    activeDReps-≡ᵉ : vds.activeDReps' ≡ᵉ vds'.activeDReps'
+    unfolding DRepsOf_∣_≤Expiry
+    activeDReps-≡ᵉ : vds.activeDReps ≡ᵉ vds'.activeDReps
     activeDReps-≡ᵉ = dom-cong $
       begin
         filterᵐ (λ (_ , e) → currentEpoch ≤ e) gState.dreps ˢ

src/Ledger/Conway/Specification/Epoch/Properties/NoPropSameDReps.lagda.md

@@ -34,7 +34,7 @@ then the set of `activeDReps`{.AgdaField} of `es`{.AgdaBound} in
 ```agda
 prop≡∅⇒activeDReps-const : Epoch → NewEpochState → Type
 prop≡∅⇒activeDReps-const e es =
-  GovStateOf es ≡ [] → activeDReps e es ≡ᵉ activeDReps (sucᵉ e) es
+  GovStateOf es ≡ [] → dom (DRepsOf es ∣ e ≤Expiry) ≡ᵉ dom (DRepsOf es ∣ (sucᵉ e) ≤Expiry)
 ```
 
 *Proof*. (coming soon)

src/Ledger/Conway/Specification/Gov/Actions.lagda.md

@@ -11,15 +11,16 @@ This section defines several concepts and types used to represent governance act
 ```agda
 {-# OPTIONS --safe #-}
 
+open import Ledger.Conway.Specification.Gov.Base
+
+module Ledger.Conway.Specification.Gov.Actions (gs : _) (open GovStructure gs) where
+
 open import Data.Nat.Properties using (+-0-monoid)
 open import Data.Rational using (ℚ; 0ℚ; 1ℚ)
 
 open import Tactic.Derive.Show
 
 open import Ledger.Prelude as P hiding (yes; no)
-open import Ledger.Conway.Specification.Gov.Base
-
-module Ledger.Conway.Specification.Gov.Actions (gs : _) (open GovStructure gs) where
 ```
 -->
 
@@ -441,3 +442,22 @@ proposedCC ⟦ UpdateCommittee , (x , _ , _) ⟧ᵍᵃ = dom x
 proposedCC _ = ∅
 ```
 
+An "active" `DRep`{.AgdaInductiveConstructor} is one whose expiry epoch is not less than the current epoch.
+
+```agda
+DReps : Type
+DReps = Credential ⇀ Epoch
+```
+
+<!--
+```agda
+record HasDReps {a} (A : Type a) : Type a where
+  field DRepsOf : A → DReps
+open HasDReps ⦃...⦄ public
+opaque
+```
+-->
+```agda
+  DRepsOf_∣_≤Expiry : {A : Type} ⦃ _ : HasDReps A ⦄ → A → Epoch → DReps
+  DRepsOf a ∣ e ≤Expiry = filterᵐ (λ (_ , expEpoch) → e ≤ expEpoch) (DRepsOf a)
+```

src/Ledger/Conway/Specification/Ratify.lagda.md

@@ -412,8 +412,8 @@ module AcceptedByDRep (Γ : RatifyEnv)
 -->
 
 ```agda
-  activeDReps' : ℙ Credential
-  activeDReps' = activeDReps currentEpoch Γ
+  activeDReps : ℙ Credential
+  activeDReps = dom (DRepsOf Γ ∣ currentEpoch ≤Expiry)
 
   castVotes : VDeleg ⇀ Vote
   castVotes = mapKeys vDelegCredential gvDRep
@@ -424,7 +424,7 @@ module AcceptedByDRep (Γ : RatifyEnv)
       _            → ❴ vDelegAbstain , Vote.abstain ❵ ∪ˡ ❴ vDelegNoConfidence , Vote.no  ❵
 
   defaultDRepCredentialVotes : VDeleg ⇀ Vote
-  defaultDRepCredentialVotes = constMap (mapˢ vDelegCredential activeDReps') Vote.no
+  defaultDRepCredentialVotes = constMap (mapˢ vDelegCredential activeDReps) Vote.no
 
   actualVotes : VDeleg ⇀ Vote
   actualVotes  = castVotes ∪ˡ defaultDRepCredentialVotes