{-# 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


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

govVoterCredential : GovVoter → Credential
govVoterCredential $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#427}{\htmlId{3859}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#3866}{\htmlId{3866}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix}$ = c
govVoterCredential $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#430}{\htmlId{3898}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#3905}{\htmlId{3905}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix}$ = c
govVoterCredential $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#435}{\htmlId{3937}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#3944}{\htmlId{3944}{\htmlClass{Bound}{\text{kh}}}}\, \end{pmatrix}$ = KeyHashObj kh

proposedCC : GovAction → ℙ Credential
proposedCC $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#663}{\htmlId{4019}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{4037}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4038}{\htmlId{4038}{\htmlClass{Bound}{\text{x}}}}\, , \,\htmlId{4042}{\htmlClass{Symbol}{\text{\_}}}\, , \,\htmlId{4046}{\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#427}{\htmlId{7743}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7750}{\htmlId{7750}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#427}{\htmlId{7758}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7765}{\htmlId{7765}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}$
    with c ≟ c'
  ... | P.yes p = P.yes (cong $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#427}{\htmlId{7820}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7802}{\htmlId{7829}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{7830}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{7834}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{7838}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{7840}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7845}{\htmlId{7845}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{7848}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{7850}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{7855}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{7858}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{7860}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{7865}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7845}{\htmlId{7867}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{7870}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{7874}{\htmlClass{Symbol}{\text{})}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7687}{\htmlId{7879}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{7894}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7895}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#427}{\htmlId{7901}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7908}{\htmlId{7908}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#430}{\htmlId{7916}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7923}{\htmlId{7923}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{7930}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{7932}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{7937}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{7939}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7687}{\htmlId{7944}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{7959}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7960}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#427}{\htmlId{7966}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7973}{\htmlId{7973}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#435}{\htmlId{7981}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7988}{\htmlId{7988}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{7995}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{7997}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8002}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8004}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7687}{\htmlId{8009}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8024}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8025}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#430}{\htmlId{8031}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8038}{\htmlId{8038}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#427}{\htmlId{8046}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8053}{\htmlId{8053}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8060}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8062}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8067}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8069}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7687}{\htmlId{8074}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8089}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8090}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#430}{\htmlId{8096}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8103}{\htmlId{8103}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#430}{\htmlId{8111}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8118}{\htmlId{8118}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}
    \,\htmlId{8129}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8103}{\htmlId{8134}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{8136}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8118}{\htmlId{8138}{\htmlClass{Bound}{\text{c'}}}}\,
  \,\htmlId{8143}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8147}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8149}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8155}{\htmlId{8155}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{8157}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8159}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{8165}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{8166}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#430}{\htmlId{8173}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8155}{\htmlId{8184}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{8185}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{8189}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8193}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8195}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8200}{\htmlId{8200}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{8203}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8205}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8210}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{8213}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8215}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{8220}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8200}{\htmlId{8222}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8225}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{8229}{\htmlClass{Symbol}{\text{})}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7687}{\htmlId{8234}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8249}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8250}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#430}{\htmlId{8256}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8263}{\htmlId{8263}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#435}{\htmlId{8271}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8278}{\htmlId{8278}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8285}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8287}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8292}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8294}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7687}{\htmlId{8299}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8314}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8315}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#435}{\htmlId{8321}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8328}{\htmlId{8328}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#427}{\htmlId{8336}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8343}{\htmlId{8343}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8350}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8352}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8357}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8359}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7687}{\htmlId{8364}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8379}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8380}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#435}{\htmlId{8386}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8393}{\htmlId{8393}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#430}{\htmlId{8401}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8408}{\htmlId{8408}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8415}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8417}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8422}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8424}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7687}{\htmlId{8429}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8444}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8445}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#435}{\htmlId{8451}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8458}{\htmlId{8458}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#435}{\htmlId{8466}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8473}{\htmlId{8473}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}
    \,\htmlId{8484}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8458}{\htmlId{8489}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{8491}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8473}{\htmlId{8493}{\htmlClass{Bound}{\text{c'}}}}\,
  \,\htmlId{8498}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8502}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8504}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8510}{\htmlId{8510}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{8512}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8514}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{8520}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{8521}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#435}{\htmlId{8528}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8510}{\htmlId{8538}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{8539}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{8543}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8547}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8549}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8554}{\htmlId{8554}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{8557}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8559}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8564}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{8567}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8569}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{8574}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8554}{\htmlId{8576}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8579}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{8583}{\htmlClass{Symbol}{\text{})}}}\,

  \,\htmlId{8589}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8601}{\htmlId{8601}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\, \,\htmlId{8617}{\htmlClass{Symbol}{\text{=}}}\, \,\href{stdlib-classes.Class.HasCast.Derive.html#2690}{\htmlId{8619}{\htmlClass{Function}{\text{derive-HasCast}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{8634}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{8636}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{8637}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1912}{\htmlId{8643}{\htmlClass{Record}{\text{GovVote}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8601}{\htmlId{8653}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\,\,\htmlId{8668}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{8670}{\htmlClass{Function Operator}{\text{]}}}}\,
  \,\htmlId{8674}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8686}{\htmlId{8686}{\htmlClass{Function}{\text{Show-VDeleg}}}}\, \,\htmlId{8698}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.Derive.Show.html#2038}{\htmlId{8700}{\htmlClass{Function}{\text{derive-Show}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{8712}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{8714}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{8715}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#2273}{\htmlId{8721}{\htmlClass{Datatype}{\text{VDeleg}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8686}{\htmlId{8730}{\htmlClass{Function}{\text{Show-VDeleg}}}}\,\,\htmlId{8741}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{8743}{\htmlClass{Function Operator}{\text{]}}}}\,


\,\htmlId{8747}{\htmlClass{Comment}{\text{-- return the DReps of A that expire in epoch e or later}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8804}{\htmlId{8804}{\htmlClass{Function}{\text{activeInEpoch}}}}\, \,\htmlId{8818}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Core.Specification.Epoch.html#646}{\htmlId{8820}{\htmlClass{Function}{\text{Epoch}}}}\, \,\htmlId{8826}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Core.Specification.Address.html#259}{\htmlId{8828}{\htmlClass{Datatype}{\text{Credential}}}}\, \,\href{Data.Product.Base.html#1618}{\htmlId{8839}{\htmlClass{Function Operator}{\text{×}}}}\, \,\href{Ledger.Core.Specification.Epoch.html#646}{\htmlId{8841}{\htmlClass{Function}{\text{Epoch}}}}\, \,\htmlId{8847}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Primitive.html#388}{\htmlId{8849}{\htmlClass{Primitive}{\text{Type}}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8804}{\htmlId{8854}{\htmlClass{Function}{\text{activeInEpoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8868}{\htmlId{8868}{\htmlClass{Bound}{\text{e}}}}\, \,\htmlId{8870}{\htmlClass{Symbol}{\text{(\_}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8875}{\htmlId{8875}{\htmlClass{Bound}{\text{expEpoch}}}}\,\,\htmlId{8883}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{8885}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8868}{\htmlId{8887}{\htmlClass{Bound}{\text{e}}}}\, \,\href{Class.HasOrder.Core.html#613}{\htmlId{8889}{\htmlClass{Field Operator}{\text{≤}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8875}{\htmlId{8891}{\htmlClass{Bound}{\text{expEpoch}}}}\,

\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8901}{\htmlId{8901}{\htmlClass{Function}{\text{activeDRepsOf}}}}\, \,\htmlId{8915}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{8917}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8918}{\htmlId{8918}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{8920}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Agda.Primitive.html#388}{\htmlId{8922}{\htmlClass{Primitive}{\text{Type}}}}\,\,\htmlId{8926}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{8928}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8930}{\htmlId{8930}{\htmlClass{Bound}{\text{\_}}}}\, \,\htmlId{8932}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4932}{\htmlId{8934}{\htmlClass{Record}{\text{HasDReps}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8918}{\htmlId{8943}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{8945}{\htmlClass{Symbol}{\text{⦄}}}\, \,\htmlId{8947}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8918}{\htmlId{8949}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{8951}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Core.Specification.Epoch.html#646}{\htmlId{8953}{\htmlClass{Function}{\text{Epoch}}}}\, \,\htmlId{8959}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4079}{\htmlId{8961}{\htmlClass{Function}{\text{DReps}}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8901}{\htmlId{8967}{\htmlClass{Function}{\text{activeDRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8981}{\htmlId{8981}{\htmlClass{Bound}{\text{a}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8983}{\htmlId{8983}{\htmlClass{Bound}{\text{e}}}}\, \,\htmlId{8985}{\htmlClass{Symbol}{\text{=}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#4102}{\htmlId{8987}{\htmlClass{Function}{\text{filterᵐ}}}}\, \,\htmlId{8995}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8804}{\htmlId{8996}{\htmlClass{Function}{\text{activeInEpoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8983}{\htmlId{9010}{\htmlClass{Bound}{\text{e}}}}\,\,\htmlId{9011}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{9013}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4981}{\htmlId{9014}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8981}{\htmlId{9022}{\htmlClass{Bound}{\text{a}}}}\,\,\htmlId{9023}{\htmlClass{Symbol}{\text{)}}}\,