Skip to content

refactor activeDReps to avoid duplication #971

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

Open
wants to merge 5 commits into
base: master
Choose a base branch
from
Open

refactor activeDReps to avoid duplication #971

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
d91b7ce
initial refactor of `activeDReps`
williamdemeo Oct 30, 2025
110c1bd
fix opacity and remove another `activeDReps` def
williamdemeo Oct 30, 2025
fa4f4ad
Merge branch 'master' into 970-dry-activedreps
williamdemeo Oct 31, 2025
aa64872
improvements
williamdemeo Oct 31, 2025
e9811b0
minor improvements
williamdemeo Oct 31, 2025
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
3 changes: 0 additions & 3 deletions src/Ledger/Conway/Conformance/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,9 +48,6 @@ getRewards = DState.rewards ∘ CertState.dState ∘ LState.certState ∘ getLSt
allDReps : NewEpochState → DReps
allDReps = GState.dreps ∘ CertState.gState ∘ LState.certState ∘ getLState

activeDReps : Epoch → NewEpochState → ℙ Credential
activeDReps currentEpoch s = dom (filterᵐ (λ (_ , e) → currentEpoch ≤ e) (allDReps s))

getGovState : NewEpochState → GovState
getGovState = LState.govSt ∘ getLState

Expand Down
8 changes: 1 addition & 7 deletions src/Ledger/Conway/Specification/Certs.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,9 +67,6 @@ instance
CCHotKeys : Type
CCHotKeys = Credential ⇀ Maybe Credential

DReps : Type
DReps = Credential ⇀ Epoch

PoolEnv : Type
PoolEnv = PParams

Expand All @@ -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

Expand All @@ -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
Expand All @@ -125,6 +118,7 @@ open HasStakeDelegs ⦃...⦄ public

## Delegation Definitions


```agda
data DCert : Type where
delegate : Credential → Maybe VDeleg → Maybe KeyHash → Coin → DCert
Expand Down
3 changes: 3 additions & 0 deletions src/Ledger/Conway/Specification/Enact.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,6 +84,9 @@ ccCreds : HashProtected (Maybe ((Credential ⇀ Epoch) × ℚ)) → ℙ Credenti
ccCreds (just x , _) = dom (x .proj₁)
ccCreds (nothing , _) = ∅

ℚof? : HashProtected (Maybe ((Credential ⇀ Epoch) × ℚ)) → Maybe ℚ
ℚof? cc' = proj₂ <$> (proj₁ cc')

getHash : ∀ {a} → NeedsHash a → Maybe GovActionID
getHash {NoConfidence} h = just h
getHash {UpdateCommittee} h = just h
Expand Down
18 changes: 4 additions & 14 deletions src/Ledger/Conway/Specification/Epoch.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
activeDReps = dom (DRepsOf gState ∣ currentEpoch ≤Expiry)

-- active vote delegations
activeVDelegs : ℙ VDeleg
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
```
<!--
Expand Down
66 changes: 35 additions & 31 deletions src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -197,26 +197,28 @@ module AcceptedByDRep-≈ {Γ Γ' : RatifyEnv} (Γ≈Γ' : RatifyEnv- Γ ≈ Γ'
castVotes : abdr.castVotes ≡ abdr'.castVotes
castVotes = refl

activeDReps : abdr.activeDReps ≡ᵉ abdr'.activeDReps
activeDReps with Γ≈Γ'.currentEpoch
... | refl = dom-cong $
begin
filterᵐ (λ (_ , e) → Γ.currentEpoch ≤ e) Γ.dreps ˢ
≈⟨ filterᵐ-idem {m = Γ.dreps} ⟨
filterᵐ (λ (_ , e) → Γ.currentEpoch ≤ e) (filterᵐ (λ (_ , e) → Γ.currentEpoch ≤ e) Γ.dreps) ˢ
≈⟨ filter-cong Γ≈Γ'.dreps ⟩
filterᵐ (λ (_ , e) → Γ'.currentEpoch ≤ e) (filterᵐ (λ (_ , e) → Γ'.currentEpoch ≤ e) Γ'.dreps) ˢ
≈⟨ filterᵐ-idem {m = Γ'.dreps} ⟩
filterᵐ (λ (_ , e) → Γ'.currentEpoch ≤ e) Γ'.dreps ˢ
∎
where
open import Relation.Binary.Reasoning.Setoid ≡ᵉ-Setoid
opaque
unfolding DRepsOf_∣_≤Expiry

activeDReps-≡ᵉ : abdr.activeDReps ≡ᵉ abdr'.activeDReps
activeDReps-≡ᵉ with Γ≈Γ'.currentEpoch
... | refl = dom-cong $
begin
filterᵐ (λ (_ , e) → Γ.currentEpoch ≤ e) Γ.dreps ˢ
≈⟨ filterᵐ-idem {m = Γ.dreps} ⟨
filterᵐ (λ (_ , e) → Γ.currentEpoch ≤ e) (filterᵐ (λ (_ , e) → Γ.currentEpoch ≤ e) Γ.dreps) ˢ
≈⟨ filter-cong Γ≈Γ'.dreps ⟩
filterᵐ (λ (_ , e) → Γ'.currentEpoch ≤ e) (filterᵐ (λ (_ , e) → Γ'.currentEpoch ≤ e) Γ'.dreps) ˢ
≈⟨ filterᵐ-idem {m = Γ'.dreps} ⟩
filterᵐ (λ (_ , e) → Γ'.currentEpoch ≤ e) Γ'.dreps ˢ
∎
where open import Relation.Binary.Reasoning.Setoid ≡ᵉ-Setoid

predeterminedDRepVotes : abdr.predeterminedDRepVotes ≡ abdr'.predeterminedDRepVotes
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}
Expand Down Expand Up @@ -251,8 +253,8 @@ module AcceptedByDRep-≈ {Γ Γ' : RatifyEnv} (Γ≈Γ' : RatifyEnv- Γ ≈ Γ'
(StakeDistrs-_≈_.stakeDistrVDeleg Γ≈Γ'.stakeDistrs)
(dom-cong (coresᵐ-cong {m = abdr.actualVotes} {m' = abdr'.actualVotes} actualVotes ≡ᵉ-isEquivalence.refl)))
where
open import Relation.Binary.Structures _≡ᵉ_
module ≡ᵉ-isEquivalence = IsEquivalence ≡ᵉ-isEquivalence
open import Relation.Binary.Structures _≡ᵉ_
module ≡ᵉ-isEquivalence = IsEquivalence ≡ᵉ-isEquivalence

accepted-→ : abdr.accepted → abdr'.accepted
accepted-→ x =
Expand Down Expand Up @@ -510,22 +512,24 @@ 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 $
begin
filterᵐ (λ (_ , e) → currentEpoch ≤ e) gState.dreps ˢ
≈⟨ filterᵐ-idem {m = gState.dreps} ⟨
filterᵐ (λ (_ , e) → currentEpoch ≤ e) (filterᵐ (λ (_ , e) → currentEpoch ≤ e) gState.dreps) ˢ
≈⟨ filter-cong gState≈gState'.dreps ⟩
filterᵐ (λ (_ , e) → currentEpoch ≤ e) (filterᵐ (λ (_ , e) → currentEpoch ≤ e) gState'.dreps) ˢ
≈⟨ filterᵐ-idem {m = gState'.dreps} ⟩
filterᵐ (λ (_ , e) → currentEpoch ≤ e) gState'.dreps ˢ
∎
where
open import Relation.Binary.Reasoning.Setoid ≡ᵉ-Setoid
opaque
unfolding DRepsOf_∣_≤Expiry
activeDReps-≡ᵉ : vds.activeDReps ≡ᵉ vds'.activeDReps
activeDReps-≡ᵉ = dom-cong $
begin
filterᵐ (λ (_ , e) → currentEpoch ≤ e) gState.dreps ˢ
≈⟨ filterᵐ-idem {m = gState.dreps} ⟨
filterᵐ (λ (_ , e) → currentEpoch ≤ e) (filterᵐ (λ (_ , e) → currentEpoch ≤ e) gState.dreps) ˢ
≈⟨ filter-cong gState≈gState'.dreps ⟩
filterᵐ (λ (_ , e) → currentEpoch ≤ e) (filterᵐ (λ (_ , e) → currentEpoch ≤ e) gState'.dreps) ˢ
≈⟨ filterᵐ-idem {m = gState'.dreps} ⟩
filterᵐ (λ (_ , e) → currentEpoch ≤ e) gState'.dreps ˢ
∎
where
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
Expand Down
3 changes: 2 additions & 1 deletion src/Ledger/Conway/Specification/Epoch/Properties/NoPropSameDReps.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ module Ledger.Conway.Specification.Epoch.Properties.NoPropSameDReps
(abs : AbstractFunctions txs) (open AbstractFunctions abs)
where

open import Ledger.Conway.Specification.Certs govStructure
open import Ledger.Conway.Specification.Epoch txs abs
open import Ledger.Conway.Specification.Gov txs
open import Ledger.Prelude
Expand All @@ -33,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)
31 changes: 28 additions & 3 deletions src/Ledger/Conway/Specification/Gov/Actions.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
```
-->

Expand Down Expand Up @@ -441,3 +442,27 @@ proposedCC ⟦ UpdateCommittee , (x , _ , _) ⟧ᵍᵃ = dom x
proposedCC _ = ∅
```

```agda
DReps : Type
DReps = Credential ⇀ Epoch
```

<!--
```agda
record HasDReps {a} (A : Type a) : Type a where
field DRepsOf : A → DReps
open HasDReps ⦃...⦄ public

opaque
```
-->

The following function takes a type `A`{.AgdaDatatype} with an associated set of
`DReps`{.AgdaDatatype}, and an epoch `e`{.AgdaBound}, and returns the
`DReps`{.AgdaDatatype} of `A`{.AgdaDatatype} that expire in epoch `e`{.AgdaBound} or
later.

```agda
DRepsOf_∣_≤Expiry : {A : Type} ⦃ _ : HasDReps A ⦄ → A → Epoch → DReps
DRepsOf a ∣ e ≤Expiry = filterᵐ (λ (_ , expEpoch) → e ≤ expEpoch) (DRepsOf a)
Comment on lines +466 to +467
Copy link
Collaborator

@carlostome carlostome Nov 3, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I find confusing that the naming of this function uses a composite of names from other functions. By this I mean:

  1. DRepsOf
  2. |
  3. ≤

Copy link
Collaborator

@WhatisRT WhatisRT Nov 4, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

How about activeDRepsOf?

```
9 changes: 0 additions & 9 deletions src/Ledger/Conway/Specification/Properties.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 }
Expand Down
28 changes: 14 additions & 14 deletions src/Ledger/Conway/Specification/Ratify.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,14 +10,15 @@ source_path: src/Ledger/Conway/Specification/Ratify.lagda.md

{-# OPTIONS --safe #-}

open import Ledger.Conway.Specification.Transaction hiding (Vote)

module Ledger.Conway.Specification.Ratify (txs : _) (open TransactionStructure txs) where

import Data.Integer as ℤ
open import Data.Rational as ℚ using (ℚ; 0ℚ; _⊔_)
open import Data.Nat.Properties hiding (_≟_; _≤?_)

open import Ledger.Prelude hiding (_∧_; _∨_; _⊔_) renaming (filterᵐ to filter; ∣_∣ to _↓)
open import Ledger.Conway.Specification.Transaction hiding (Vote)

module Ledger.Conway.Specification.Ratify (txs : _) (open TransactionStructure txs) where

open import Ledger.Conway.Specification.Certs govStructure
open import Ledger.Conway.Specification.Enact govStructure
Expand Down Expand Up @@ -314,8 +315,8 @@ module AcceptedByCC (currentEpoch : Epoch)
```
<!--
```agda
open EnactState eSt using (cc; pparams)
open PParams (proj₁ pparams)
open EnactState eSt using (cc)
open PParams (PParamsOf eSt)
open GovActionState gaSt
open GovVotes votes using (gvCC)
```
Expand Down Expand Up @@ -345,7 +346,7 @@ module AcceptedByCC (currentEpoch : Epoch)
else constMap (dom m) Vote.no

mT : Maybe ℚ
mT = threshold (proj₁ pparams) (proj₂ <$> (proj₁ cc)) action CC
mT = threshold (PParamsOf eSt) (ℚof? cc) action CC

t : ℚ
t = maybe id 0ℚ mT
Expand Down Expand Up @@ -402,9 +403,8 @@ module AcceptedByDRep (Γ : RatifyEnv)
```
<!--
```agda
open EnactState eSt using (cc; pparams)
open RatifyEnv Γ using (currentEpoch; dreps; stakeDistrs)
open PParams (proj₁ pparams)
open EnactState eSt using (cc)
open RatifyEnv Γ using (currentEpoch; stakeDistrs)
open StakeDistrs stakeDistrs
open GovActionState gaSt
open GovVotes votes using (gvDRep)
Expand All @@ -416,7 +416,7 @@ module AcceptedByDRep (Γ : RatifyEnv)
castVotes = mapKeys vDelegCredential gvDRep

activeDReps : ℙ Credential
activeDReps = dom (filter (λ (_ , e) → currentEpoch ≤ e) dreps)
activeDReps = dom (DRepsOf Γ ∣ currentEpoch ≤Expiry)

predeterminedDRepVotes : VDeleg ⇀ Vote
predeterminedDRepVotes = case gaType action of λ where
Expand All @@ -428,10 +428,10 @@ module AcceptedByDRep (Γ : RatifyEnv)

actualVotes : VDeleg ⇀ Vote
actualVotes = castVotes ∪ˡ defaultDRepCredentialVotes
∪ˡ predeterminedDRepVotes
∪ˡ predeterminedDRepVotes

t : ℚ
t = maybe id 0ℚ (threshold (proj₁ pparams) (proj₂ <$> (proj₁ cc)) action DRep)
t = maybe id 0ℚ (threshold (PParamsOf eSt) (ℚof? cc) action DRep)

acceptedStake totalStake : Coin
acceptedStake = ∑[ x ← stakeDistrVDeleg ∣ actualVotes ⁻¹ Vote.yes ] x
Expand Down Expand Up @@ -523,7 +523,7 @@ module AcceptedBySPO (delegatees : VoteDelegs)

<!--
```agda
open EnactState eSt using (cc; pparams)
open EnactState eSt using (cc)
open GovActionState gaSt
open GovVotes votes using (gvSPO)
```
Expand All @@ -547,7 +547,7 @@ module AcceptedBySPO (delegatees : VoteDelegs)
actualVotes = castVotes ∪ˡ mapFromFun defaultVote (dom stakeDistrPools)

t : ℚ
t = maybe id 0ℚ (threshold (proj₁ pparams) (proj₂ <$> (proj₁ cc)) action SPO)
t = maybe id 0ℚ (threshold (PParamsOf eSt) (ℚof? cc) action SPO)

acceptedStake totalStake : Coin
acceptedStake = ∑[ x ← stakeDistrPools ∣ actualVotes ⁻¹ Vote.yes ] x
Expand Down