initial refactor of activeDReps

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

@@ -125,6 +125,15 @@ 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

@@ -461,31 +461,21 @@ module VDelegDelegatedStake
   (gState       : GState)
   (dState       : DState)
   where
-```
-<!--
-```agda
-  open UTxOState utxoSt
-  open DState dState
-  open GState gState
-```
--->
-```agda
-  -- active DReps
-  activeDReps : ℙ Credential
-  activeDReps = dom (filterᵐ (λ (_ , e) → currentEpoch ≤ e) dreps)
 
-  -- active vote delegations
+  activeDReps' : ℙ Credential
+  activeDReps' = activeDReps currentEpoch gState
+
   activeVDelegs : ℙ VDeleg
-  activeVDelegs = mapˢ vDelegCredential activeDReps ∪ ❴ vDelegNoConfidence ❵ ∪ ❴ vDelegAbstain ❵
+  activeVDelegs = mapˢ vDelegCredential activeDReps' ∪ ❴ vDelegNoConfidence ❵ ∪ ❴ vDelegAbstain ❵
 
   -- compute the stake for a credential
   stakePerCredential : Credential → Coin
-  stakePerCredential c = cbalance (utxo ∣^' λ txout → getStakeCred txout ≡ just c)
+  stakePerCredential c = cbalance ((UTxOOf utxoSt) ∣^' λ txout → getStakeCred txout ≡ just c)
                          + fromMaybe 0 (lookupᵐ? (stakeFromGADeposits govSt utxoSt) c)
                          + fromMaybe 0 (lookupᵐ? (RewardsOf dState) c)
 
   calculate : VDeleg ⇀ Coin
-  calculate = mapFromFun (λ vd → ∑ˢ[ c ← voteDelegs ⁻¹ vd ] (stakePerCredential c))
+  calculate = mapFromFun (λ vd → ∑ˢ[ c ← (VoteDelegsOf dState) ⁻¹ vd ] (stakePerCredential c))
                          activeVDelegs
 ```
 <!--

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

@@ -197,8 +197,8 @@ module AcceptedByDRep-≈ {Γ Γ' : RatifyEnv} (Γ≈Γ' : RatifyEnv- Γ ≈ Γ'
   castVotes : abdr.castVotes ≡ abdr'.castVotes
   castVotes = refl
 
-  activeDReps : abdr.activeDReps ≡ᵉ abdr'.activeDReps
-  activeDReps with Γ≈Γ'.currentEpoch
+  activeDReps-≡ᵉ : abdr.activeDReps' ≡ᵉ abdr'.activeDReps'
+  activeDReps-≡ᵉ with Γ≈Γ'.currentEpoch
   ... | refl = dom-cong $
     begin
       filterᵐ (λ (_ , e) → Γ.currentEpoch ≤ e) Γ.dreps ˢ
@@ -216,7 +216,7 @@ module AcceptedByDRep-≈ {Γ Γ' : RatifyEnv} (Γ≈Γ' : RatifyEnv- Γ ≈ Γ'
   predeterminedDRepVotes = refl
 
   defaultDRepCredentialVotes : abdr.defaultDRepCredentialVotes ≡ᵐ abdr'.defaultDRepCredentialVotes
-  defaultDRepCredentialVotes = map-≡ᵉ (map-≡ᵉ activeDReps)
+  defaultDRepCredentialVotes = map-≡ᵉ (map-≡ᵉ activeDReps-≡ᵉ)
 
   actualVotes : abdr.actualVotes ≡ᵐ abdr'.actualVotes
   actualVotes = ∪ˡ-cong {m = abdr.castVotes} {m' = abdr.defaultDRepCredentialVotes ∪ˡ abdr.predeterminedDRepVotes}
@@ -510,8 +510,8 @@ module VDelegDelegatedStake-≈
   module vds  = VDelegDelegatedStake currentEpoch utxoSt govSt gState  dState
   module vds' = VDelegDelegatedStake currentEpoch utxoSt govSt gState' dState
 
-  activeDReps : vds.activeDReps ≡ᵉ vds'.activeDReps
-  activeDReps = dom-cong $
+  activeDReps-≡ᵉ : vds.activeDReps' ≡ᵉ vds'.activeDReps'
+  activeDReps-≡ᵉ = dom-cong $
     begin
       filterᵐ (λ (_ , e) → currentEpoch ≤ e) gState.dreps ˢ
         ≈⟨ filterᵐ-idem {m = gState.dreps} ⟨
@@ -525,7 +525,7 @@ module VDelegDelegatedStake-≈
       open import Relation.Binary.Reasoning.Setoid ≡ᵉ-Setoid
 
   activeVDelegs : vds.activeVDelegs ≡ᵉ vds'.activeVDelegs
-  activeVDelegs = ∪-cong (map-≡ᵉ activeDReps) ≡ᵉ-isEquivalence.refl
+  activeVDelegs = ∪-cong (map-≡ᵉ activeDReps-≡ᵉ) ≡ᵉ-isEquivalence.refl
     where
       open import Relation.Binary.Structures _≡ᵉ_
       module ≡ᵉ-isEquivalence = IsEquivalence ≡ᵉ-isEquivalence

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

@@ -74,16 +74,7 @@ instance
   isGADeposit? {PoolDeposit x} = ⁇ (no λ ())
   isGADeposit? {DRepDeposit x} = ⁇ (no λ ())
   isGADeposit? {GovActionDeposit x} = ⁇ (yes tt)
-```
--->
 
-```agda
-activeDReps : Epoch → NewEpochState → ℙ Credential
-activeDReps currentEpoch s = dom (filterᵐ (λ (_ , e) → currentEpoch ≤ e) (DRepsOf s))
-```
-
-<!--
-```agda
 instance
   _ : IsSet Block Tx
   _ = record { toSet = fromList ∘ Block.ts }

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

@@ -403,7 +403,7 @@ module AcceptedByDRep (Γ : RatifyEnv)
 <!--
 ```agda
   open EnactState eSt using (cc; pparams)
-  open RatifyEnv Γ using (currentEpoch; dreps; stakeDistrs)
+  open RatifyEnv Γ using (currentEpoch; stakeDistrs)
   open PParams (proj₁ pparams)
   open StakeDistrs stakeDistrs
   open GovActionState gaSt
@@ -412,19 +412,19 @@ module AcceptedByDRep (Γ : RatifyEnv)
 -->
 
 ```agda
+  activeDReps' : ℙ Credential
+  activeDReps' = activeDReps currentEpoch Γ
+
   castVotes : VDeleg ⇀ Vote
   castVotes = mapKeys vDelegCredential gvDRep
 
-  activeDReps : ℙ Credential
-  activeDReps = dom (filter (λ (_ , e) → currentEpoch ≤ e) dreps)
-
   predeterminedDRepVotes : VDeleg ⇀ Vote
   predeterminedDRepVotes = case gaType action of λ where
       NoConfidence → ❴ vDelegAbstain , Vote.abstain ❵ ∪ˡ ❴ vDelegNoConfidence , Vote.yes ❵
       _            → ❴ 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