Governance Actions

This section defines several concepts and types used to represent governance actions.

{-# OPTIONS --safe #-}

open import Ledger.Dijkstra.Specification.Gov.Base

module Ledger.Dijkstra.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.Core.Specification.ProtocolVersion

Roles and Actions

There are three governance roles and actors of role are identified by a type of credential. A governance action is one of the seven types.

data GovRole : Type where
  CC DRep SPO : GovRole

GovRoleCredential : GovRole → Type
GovRoleCredential CC   = Credential
GovRoleCredential DRep = Credential
GovRoleCredential SPO  = KeyHash

data GovActionType : Type where
  NoConfidence        : GovActionType
  UpdateCommittee     : GovActionType
  NewConstitution     : GovActionType
  TriggerHardFork     : GovActionType
  ChangePParams       : GovActionType
  TreasuryWithdrawal  : GovActionType
  Info                : GovActionType

GovActionData : GovActionType → Type
GovActionData NoConfidence        = ⊤
GovActionData UpdateCommittee     = (Credential ⇀ Epoch) × ℙ Credential × ℚ
GovActionData NewConstitution     = DocHash × Maybe ScriptHash
GovActionData TriggerHardFork     = ProtVer
GovActionData ChangePParams       = PParamsUpdate
GovActionData TreasuryWithdrawal  = Withdrawals
GovActionData Info                = ⊤

record GovAction : Type where
  constructor ⟦_,_⟧ᵍᵃ
  field
    gaType : GovActionType
    gaData : GovActionData gaType

open GovAction public

-- Governance actions are uniquely identified by a `GovActionID`.
GovActionID : Type
GovActionID  = TxId × ℕ

data Vote : Type where
  yes no abstain  : Vote

record GovVoter : Type where
  constructor ⟦_,_⟧ᵍᵛ
  field
    gvRole       : GovRole
    gvCredential : GovRoleCredential gvRole

record Anchor : Type where
  -- context about why a vote was cast in a certain manner
  field
    url   : String
    hash  : DocHash -- abstract but instantiated with 32-bit hash type

record GovVote : Type where
  field
    gid         : GovActionID
    voter       : GovVoter
    vote        : Vote
    anchor      : Maybe Anchor

record GovVotes : Type where
  -- collects votes cast by members of each of the governance roles
  field
    gvCC   : Credential ⇀ Vote
    gvDRep : Credential ⇀ Vote
    gvSPO  : KeyHash ⇀ Vote

-- Vote Delegation
data VDeleg : Type where
  vDelegCredential   : Credential → VDeleg
  vDelegAbstain      : VDeleg
  vDelegNoConfidence : VDeleg

VoteDelegs : Type
VoteDelegs   = Credential ⇀ VDeleg

-- Hash Protection
NeedsHash : GovActionType → Type
NeedsHash NoConfidence        = GovActionID
NeedsHash UpdateCommittee     = GovActionID
NeedsHash NewConstitution     = GovActionID
NeedsHash TriggerHardFork     = GovActionID
NeedsHash ChangePParams       = GovActionID
NeedsHash TreasuryWithdrawal  = ⊤
NeedsHash Info                = ⊤

HashProtected : Type → Type
HashProtected A = A × GovActionID

Policy : Type
Policy = Maybe ScriptHash

record GovProposal : Type where
  field
    action      : GovAction
    prevAction  : NeedsHash (gaType action)  -- pointer to previous action
    policy      : Policy                     -- pointer to optional proposal policy
    deposit     : Coin                       -- to be returned to returnAddr
    returnAddr  : RewardAddress              -- reward address;  dep returned here when prop is removed
    anchor      : Anchor                     -- placeholder for further information about the proposal


-- state of an individual governance action
record GovActionState : Type where
  field
    votes       : GovVotes
    returnAddr  : RewardAddress
    expiresIn   : Epoch
    action      : GovAction
    prevAction  : NeedsHash (gaType action)

-- Governance Helper Functions
isGovVoterDRep : GovVoter → Maybe Credential
isGovVoterDRep $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{4169}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4176}{\htmlId{4176}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = just c
isGovVoterDRep _ = nothing

govVoterCredential : GovVoter → Credential
govVoterCredential $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{4283}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4290}{\htmlId{4290}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix}$ = c
govVoterCredential $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{4322}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4329}{\htmlId{4329}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix}$ = c
govVoterCredential $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{4361}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4368}{\htmlId{4368}{\htmlClass{Bound}{\text{kh}}}}\, \end{pmatrix}$ = KeyHashObj kh

proposedCC : GovAction → ℙ Credential
proposedCC $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1087}{\htmlId{4443}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{4461}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4462}{\htmlId{4462}{\htmlClass{Bound}{\text{x}}}}\, , \,\htmlId{4466}{\htmlClass{Symbol}{\text{\_}}}\, , \,\htmlId{4470}{\htmlClass{Symbol}{\text{\_)}}}\, \end{pmatrix}$ = dom x
proposedCC _ = ∅

DReps : Type
DReps = Credential ⇀ Epoch

record HasGovActionType (A : Type) : Type where
  field GovActionTypeOf : A → GovActionType
open HasGovActionType ⦃...⦄ public

record HasVoteDelegs {a} (A : Type a) : Type a where
  field VoteDelegsOf : A → VoteDelegs
open HasVoteDelegs ⦃...⦄ public

record HasGovAction (A : Type) : Type where
  field GovActionOf : A → GovAction
open HasGovAction ⦃...⦄ public

record HasGovVoter {a} (A : Type a) : Type a where
  field GovVoterOf : A → GovVoter
open HasGovVoter ⦃...⦄ public

record HasGovVotes {a} (A : Type a) : Type a where
  field GovVotesOf : A → GovVotes
open HasGovVotes ⦃...⦄ public

record HasVote {a} (A : Type a) : Type a where
  field VoteOf : A → Vote
open HasVote ⦃...⦄ public

record HasPolicy {a} (A : Type a) : Type a where
  field PolicyOf : A → Policy
open HasPolicy ⦃...⦄ public

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

record HasAnchor {a} (A : Type a) : Type a where
  field AnchorOf : A → Anchor
open HasAnchor ⦃...⦄ public

record HasDeposit {a} (A : Type a) : Type a where
  field DepositOf : A → Coin
open HasDeposit ⦃...⦄ public

instance
  HasGovActionType-GovAction : HasGovActionType GovAction
  HasGovActionType-GovAction .GovActionTypeOf = GovAction.gaType

  HasCast-GovAction-Sigma : HasCast GovAction (Σ GovActionType GovActionData)
  HasCast-GovAction-Sigma .cast x = x .gaType , x .gaData

  HasCast-HashProtected : ∀ {A : Type} → HasCast (HashProtected A) A
  HasCast-HashProtected .cast = proj₁

  HasCast-HashProtected-MaybeScriptHash : HasCast (HashProtected (DocHash × Maybe ScriptHash)) (Maybe ScriptHash)
  HasCast-HashProtected-MaybeScriptHash .cast = proj₂ ∘ proj₁

  HasGovVoter-GovVote : HasGovVoter GovVote
  HasGovVoter-GovVote .GovVoterOf = GovVote.voter

  HasVote-GovVote : HasVote GovVote
  HasVote-GovVote .VoteOf = GovVote.vote

  HasPolicy-GovProposal : HasPolicy GovProposal
  HasPolicy-GovProposal .PolicyOf = GovProposal.policy

  HasAnchor-GovProposal : HasAnchor GovProposal
  HasAnchor-GovProposal .AnchorOf = GovProposal.anchor

  HasDeposit-GovProposal : HasDeposit GovProposal
  HasDeposit-GovProposal .DepositOf = GovProposal.deposit

  HasGovAction-GovProposal : HasGovAction GovProposal
  HasGovAction-GovProposal .GovActionOf = GovProposal.action

  HasGovAction-GovActionState : HasGovAction GovActionState
  HasGovAction-GovActionState .GovActionOf = GovActionState.action

  HasGovActionType-GovProposal : HasGovActionType GovProposal
  HasGovActionType-GovProposal .GovActionTypeOf = GovActionTypeOf ∘ GovActionOf

  HasGovActionType-GovActionState : HasGovActionType GovActionState
  HasGovActionType-GovActionState .GovActionTypeOf = GovActionTypeOf ∘ GovActionOf

  HasGovVotes-GovActionState : HasGovVotes GovActionState
  HasGovVotes-GovActionState .GovVotesOf = GovActionState.votes

  HasRewardAddress-GovActionState : HasRewardAddress GovActionState
  HasRewardAddress-GovActionState .RewardAddressOf = GovActionState.returnAddr

  HasRewardAddress-GovProposal : HasRewardAddress GovProposal
  HasRewardAddress-GovProposal .RewardAddressOf = GovProposal.returnAddr

  unquoteDecl Show-GovRole        = derive-Show [ (quote GovRole , Show-GovRole) ]
  unquoteDecl DecEq-GovActionType = derive-DecEq ((quote GovActionType , DecEq-GovActionType) ∷ [])
  unquoteDecl DecEq-GovRole       = derive-DecEq ((quote GovRole , DecEq-GovRole) ∷ [])
  unquoteDecl DecEq-Vote          = derive-DecEq ((quote Vote    , DecEq-Vote)    ∷ [])
  unquoteDecl DecEq-VDeleg        = derive-DecEq ((quote VDeleg  , DecEq-VDeleg)  ∷ [])

  DecEq-GovVoter : DecEq GovVoter
  DecEq-GovVoter ._≟_ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{8183}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8190}{\htmlId{8190}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{8198}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8205}{\htmlId{8205}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}$
    with c ≟ c'
  ... | P.yes p = P.yes (cong $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{8260}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8242}{\htmlId{8269}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{8270}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{8274}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8278}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8280}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8285}{\htmlId{8285}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{8288}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8290}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8295}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{8298}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8300}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{8305}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8285}{\htmlId{8307}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8310}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{8314}{\htmlClass{Symbol}{\text{})}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8127}{\htmlId{8319}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8334}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8335}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{8341}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8348}{\htmlId{8348}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{8356}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8363}{\htmlId{8363}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8370}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8372}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8377}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8379}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8127}{\htmlId{8384}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8399}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8400}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{8406}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8413}{\htmlId{8413}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{8421}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8428}{\htmlId{8428}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8435}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8437}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8442}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8444}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8127}{\htmlId{8449}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8464}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8465}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{8471}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8478}{\htmlId{8478}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{8486}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8493}{\htmlId{8493}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8500}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8502}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8507}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8509}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8127}{\htmlId{8514}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8529}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8530}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{8536}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8543}{\htmlId{8543}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{8551}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8558}{\htmlId{8558}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}
    \,\htmlId{8569}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8543}{\htmlId{8574}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{8576}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8558}{\htmlId{8578}{\htmlClass{Bound}{\text{c'}}}}\,
  \,\htmlId{8583}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8587}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8589}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8595}{\htmlId{8595}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{8597}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8599}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{8605}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{8606}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{8613}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8595}{\htmlId{8624}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{8625}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{8629}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8633}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8635}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8640}{\htmlId{8640}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{8643}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8645}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8650}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{8653}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8655}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{8660}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8640}{\htmlId{8662}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8665}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{8669}{\htmlClass{Symbol}{\text{})}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8127}{\htmlId{8674}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8689}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8690}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{8696}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8703}{\htmlId{8703}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{8711}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8718}{\htmlId{8718}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8725}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8727}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8732}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8734}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8127}{\htmlId{8739}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8754}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8755}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{8761}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8768}{\htmlId{8768}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{8776}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8783}{\htmlId{8783}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8790}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8792}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8797}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8799}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8127}{\htmlId{8804}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8819}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8820}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{8826}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8833}{\htmlId{8833}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{8841}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8848}{\htmlId{8848}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8855}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8857}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8862}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8864}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8127}{\htmlId{8869}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8884}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8885}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{8891}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8898}{\htmlId{8898}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{8906}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8913}{\htmlId{8913}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}
    \,\htmlId{8924}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8898}{\htmlId{8929}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{8931}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8913}{\htmlId{8933}{\htmlClass{Bound}{\text{c'}}}}\,
  \,\htmlId{8938}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8942}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8944}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8950}{\htmlId{8950}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{8952}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8954}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{8960}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{8961}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{8968}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8950}{\htmlId{8978}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{8979}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{8983}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8987}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8989}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8994}{\htmlId{8994}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{8997}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8999}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{9004}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{9007}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{9009}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{9014}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8994}{\htmlId{9016}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{9019}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{9023}{\htmlClass{Symbol}{\text{})}}}\,

  \,\htmlId{9029}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9041}{\htmlId{9041}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\, \,\htmlId{9057}{\htmlClass{Symbol}{\text{=}}}\, \,\href{stdlib-classes.Class.HasCast.Derive.html#2690}{\htmlId{9059}{\htmlClass{Function}{\text{derive-HasCast}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{9074}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{9076}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{9077}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#2336}{\htmlId{9083}{\htmlClass{Record}{\text{GovVote}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9041}{\htmlId{9093}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\,\,\htmlId{9108}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{9110}{\htmlClass{Function Operator}{\text{]}}}}\,
  \,\htmlId{9114}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9126}{\htmlId{9126}{\htmlClass{Function}{\text{Show-VDeleg}}}}\, \,\htmlId{9138}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.Derive.Show.html#2038}{\htmlId{9140}{\htmlClass{Function}{\text{derive-Show}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{9152}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{9154}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{9155}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#2697}{\htmlId{9161}{\htmlClass{Datatype}{\text{VDeleg}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9126}{\htmlId{9170}{\htmlClass{Function}{\text{Show-VDeleg}}}}\,\,\htmlId{9181}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{9183}{\htmlClass{Function Operator}{\text{]}}}}\,

-- return the DReps of A that expire in epoch e or later
activeInEpoch : Epoch → Credential × Epoch → Type
activeInEpoch e (_ , expEpoch) = e ≤ expEpoch

activeDRepsOf : {A : Type} ⦃ _ : HasDReps A ⦄ → A → Epoch → DReps
activeDRepsOf a e = filterᵐ (activeInEpoch e) (DRepsOf a)