Skip to content

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)

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#800}{\htmlId{4115}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4122}{\htmlId{4122}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = just c
isGovVoterDRep _ = nothing

govVoterCredential : GovVoter → Credential
govVoterCredential $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#797}{\htmlId{4229}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4236}{\htmlId{4236}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix}$ = c
govVoterCredential $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#800}{\htmlId{4268}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4275}{\htmlId{4275}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix}$ = c
govVoterCredential $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#805}{\htmlId{4307}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4314}{\htmlId{4314}{\htmlClass{Bound}{\text{kh}}}}\, \end{pmatrix}$ = KeyHashObj kh

proposedCC : GovAction → ℙ Credential
proposedCC $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1033}{\htmlId{4389}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{4407}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4408}{\htmlId{4408}{\htmlClass{Bound}{\text{x}}}}\, , \,\htmlId{4412}{\htmlClass{Symbol}{\text{\_}}}\, , \,\htmlId{4416}{\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#797}{\htmlId{8129}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8136}{\htmlId{8136}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#797}{\htmlId{8144}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8151}{\htmlId{8151}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}$
    with c ≟ c'
  ... | P.yes p = P.yes (cong $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#797}{\htmlId{8206}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8188}{\htmlId{8215}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{8216}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{8220}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8224}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8226}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8231}{\htmlId{8231}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{8234}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8236}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8241}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{8244}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8246}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{8251}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8231}{\htmlId{8253}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8256}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{8260}{\htmlClass{Symbol}{\text{})}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8073}{\htmlId{8265}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8280}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8281}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#797}{\htmlId{8287}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8294}{\htmlId{8294}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#800}{\htmlId{8302}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8309}{\htmlId{8309}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8316}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8318}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8323}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8325}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8073}{\htmlId{8330}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8345}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8346}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#797}{\htmlId{8352}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8359}{\htmlId{8359}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#805}{\htmlId{8367}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8374}{\htmlId{8374}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8381}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8383}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8388}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8390}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8073}{\htmlId{8395}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8410}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8411}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#800}{\htmlId{8417}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8424}{\htmlId{8424}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#797}{\htmlId{8432}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8439}{\htmlId{8439}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8446}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8448}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8453}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8455}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8073}{\htmlId{8460}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8475}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8476}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#800}{\htmlId{8482}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8489}{\htmlId{8489}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#800}{\htmlId{8497}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8504}{\htmlId{8504}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}
    \,\htmlId{8515}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8489}{\htmlId{8520}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{8522}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8504}{\htmlId{8524}{\htmlClass{Bound}{\text{c'}}}}\,
  \,\htmlId{8529}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8533}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8535}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8541}{\htmlId{8541}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{8543}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8545}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{8551}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{8552}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#800}{\htmlId{8559}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8541}{\htmlId{8570}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{8571}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{8575}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8579}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8581}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8586}{\htmlId{8586}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{8589}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8591}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8596}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{8599}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8601}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{8606}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8586}{\htmlId{8608}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8611}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{8615}{\htmlClass{Symbol}{\text{})}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8073}{\htmlId{8620}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8635}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8636}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#800}{\htmlId{8642}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8649}{\htmlId{8649}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#805}{\htmlId{8657}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8664}{\htmlId{8664}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8671}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8673}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8678}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8680}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8073}{\htmlId{8685}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8700}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8701}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#805}{\htmlId{8707}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8714}{\htmlId{8714}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#797}{\htmlId{8722}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8729}{\htmlId{8729}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8736}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8738}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8743}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8745}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8073}{\htmlId{8750}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8765}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8766}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#805}{\htmlId{8772}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8779}{\htmlId{8779}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#800}{\htmlId{8787}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8794}{\htmlId{8794}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8801}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8803}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8808}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8810}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8073}{\htmlId{8815}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8830}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8831}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#805}{\htmlId{8837}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8844}{\htmlId{8844}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#805}{\htmlId{8852}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8859}{\htmlId{8859}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}
    \,\htmlId{8870}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8844}{\htmlId{8875}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{8877}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8859}{\htmlId{8879}{\htmlClass{Bound}{\text{c'}}}}\,
  \,\htmlId{8884}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8888}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8890}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8896}{\htmlId{8896}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{8898}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8900}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{8906}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{8907}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#805}{\htmlId{8914}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8896}{\htmlId{8924}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{8925}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{8929}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8933}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8935}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8940}{\htmlId{8940}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{8943}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8945}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8950}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{8953}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8955}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{8960}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8940}{\htmlId{8962}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8965}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{8969}{\htmlClass{Symbol}{\text{})}}}\,

  \,\htmlId{8975}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8987}{\htmlId{8987}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\, \,\htmlId{9003}{\htmlClass{Symbol}{\text{=}}}\, \,\href{stdlib-classes.Class.HasCast.Derive.html#2690}{\htmlId{9005}{\htmlClass{Function}{\text{derive-HasCast}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{9020}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{9022}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{9023}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#2282}{\htmlId{9029}{\htmlClass{Record}{\text{GovVote}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8987}{\htmlId{9039}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\,\,\htmlId{9054}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{9056}{\htmlClass{Function Operator}{\text{]}}}}\,
  \,\htmlId{9060}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9072}{\htmlId{9072}{\htmlClass{Function}{\text{Show-VDeleg}}}}\, \,\htmlId{9084}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.Derive.Show.html#2038}{\htmlId{9086}{\htmlClass{Function}{\text{derive-Show}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{9098}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{9100}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{9101}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#2643}{\htmlId{9107}{\htmlClass{Datatype}{\text{VDeleg}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9072}{\htmlId{9116}{\htmlClass{Function}{\text{Show-VDeleg}}}}\,\,\htmlId{9127}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{9129}{\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)