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


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

govVoterCredential : GovVoter → Credential
govVoterCredential $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#373}{\htmlId{3805}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#3812}{\htmlId{3812}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix}$ = c
govVoterCredential $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#376}{\htmlId{3844}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#3851}{\htmlId{3851}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix}$ = c
govVoterCredential $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#381}{\htmlId{3883}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#3890}{\htmlId{3890}{\htmlClass{Bound}{\text{kh}}}}\, \end{pmatrix}$ = KeyHashObj kh

proposedCC : GovAction → ℙ Credential
proposedCC $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#609}{\htmlId{3965}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{3983}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#3984}{\htmlId{3984}{\htmlClass{Bound}{\text{x}}}}\, , \,\htmlId{3988}{\htmlClass{Symbol}{\text{\_}}}\, , \,\htmlId{3992}{\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#373}{\htmlId{7689}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7696}{\htmlId{7696}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#373}{\htmlId{7704}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7711}{\htmlId{7711}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}$
    with c ≟ c'
  ... | P.yes p = P.yes (cong $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#373}{\htmlId{7766}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7748}{\htmlId{7775}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{7776}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{7780}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{7784}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{7786}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7791}{\htmlId{7791}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{7794}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{7796}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{7801}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{7804}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{7806}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{7811}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7791}{\htmlId{7813}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{7816}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{7820}{\htmlClass{Symbol}{\text{})}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7633}{\htmlId{7825}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{7840}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7841}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#373}{\htmlId{7847}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7854}{\htmlId{7854}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#376}{\htmlId{7862}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7869}{\htmlId{7869}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{7876}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{7878}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{7883}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{7885}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7633}{\htmlId{7890}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{7905}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7906}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#373}{\htmlId{7912}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7919}{\htmlId{7919}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#381}{\htmlId{7927}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7934}{\htmlId{7934}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{7941}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{7943}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{7948}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{7950}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7633}{\htmlId{7955}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{7970}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7971}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#376}{\htmlId{7977}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7984}{\htmlId{7984}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#373}{\htmlId{7992}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7999}{\htmlId{7999}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8006}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8008}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8013}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8015}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7633}{\htmlId{8020}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8035}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8036}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#376}{\htmlId{8042}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8049}{\htmlId{8049}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#376}{\htmlId{8057}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8064}{\htmlId{8064}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}
    \,\htmlId{8075}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8049}{\htmlId{8080}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{8082}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8064}{\htmlId{8084}{\htmlClass{Bound}{\text{c'}}}}\,
  \,\htmlId{8089}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8093}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8095}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8101}{\htmlId{8101}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{8103}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8105}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{8111}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{8112}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#376}{\htmlId{8119}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8101}{\htmlId{8130}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{8131}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{8135}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8139}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8141}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8146}{\htmlId{8146}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{8149}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8151}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8156}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{8159}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8161}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{8166}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8146}{\htmlId{8168}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8171}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{8175}{\htmlClass{Symbol}{\text{})}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7633}{\htmlId{8180}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8195}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8196}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#376}{\htmlId{8202}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8209}{\htmlId{8209}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#381}{\htmlId{8217}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8224}{\htmlId{8224}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8231}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8233}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8238}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8240}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7633}{\htmlId{8245}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8260}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8261}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#381}{\htmlId{8267}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8274}{\htmlId{8274}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#373}{\htmlId{8282}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8289}{\htmlId{8289}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8296}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8298}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8303}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8305}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7633}{\htmlId{8310}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8325}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8326}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#381}{\htmlId{8332}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8339}{\htmlId{8339}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#376}{\htmlId{8347}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8354}{\htmlId{8354}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8361}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8363}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8368}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8370}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7633}{\htmlId{8375}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8390}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8391}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#381}{\htmlId{8397}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8404}{\htmlId{8404}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#381}{\htmlId{8412}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8419}{\htmlId{8419}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}
    \,\htmlId{8430}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8404}{\htmlId{8435}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{8437}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8419}{\htmlId{8439}{\htmlClass{Bound}{\text{c'}}}}\,
  \,\htmlId{8444}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8448}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8450}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8456}{\htmlId{8456}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{8458}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8460}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{8466}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{8467}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#381}{\htmlId{8474}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8456}{\htmlId{8484}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{8485}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{8489}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8493}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8495}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8500}{\htmlId{8500}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{8503}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8505}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8510}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{8513}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8515}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{8520}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8500}{\htmlId{8522}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8525}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{8529}{\htmlClass{Symbol}{\text{})}}}\,

  \,\htmlId{8535}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8547}{\htmlId{8547}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\, \,\htmlId{8563}{\htmlClass{Symbol}{\text{=}}}\, \,\href{stdlib-classes.Class.HasCast.Derive.html#2690}{\htmlId{8565}{\htmlClass{Function}{\text{derive-HasCast}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{8580}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{8582}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{8583}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1858}{\htmlId{8589}{\htmlClass{Record}{\text{GovVote}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8547}{\htmlId{8599}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\,\,\htmlId{8614}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{8616}{\htmlClass{Function Operator}{\text{]}}}}\,
  \,\htmlId{8620}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8632}{\htmlId{8632}{\htmlClass{Function}{\text{Show-VDeleg}}}}\, \,\htmlId{8644}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.Derive.Show.html#2038}{\htmlId{8646}{\htmlClass{Function}{\text{derive-Show}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{8658}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{8660}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{8661}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#2219}{\htmlId{8667}{\htmlClass{Datatype}{\text{VDeleg}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8632}{\htmlId{8676}{\htmlClass{Function}{\text{Show-VDeleg}}}}\,\,\htmlId{8687}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{8689}{\htmlClass{Function Operator}{\text{]}}}}\,


\,\htmlId{8693}{\htmlClass{Comment}{\text{-- return the DReps of A that expire in epoch e or later}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8750}{\htmlId{8750}{\htmlClass{Function}{\text{activeInEpoch}}}}\, \,\htmlId{8764}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Core.Specification.Epoch.html#646}{\htmlId{8766}{\htmlClass{Function}{\text{Epoch}}}}\, \,\htmlId{8772}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Core.Specification.Address.html#259}{\htmlId{8774}{\htmlClass{Datatype}{\text{Credential}}}}\, \,\href{Data.Product.Base.html#1618}{\htmlId{8785}{\htmlClass{Function Operator}{\text{×}}}}\, \,\href{Ledger.Core.Specification.Epoch.html#646}{\htmlId{8787}{\htmlClass{Function}{\text{Epoch}}}}\, \,\htmlId{8793}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Primitive.html#388}{\htmlId{8795}{\htmlClass{Primitive}{\text{Type}}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8750}{\htmlId{8800}{\htmlClass{Function}{\text{activeInEpoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8814}{\htmlId{8814}{\htmlClass{Bound}{\text{e}}}}\, \,\htmlId{8816}{\htmlClass{Symbol}{\text{(\_}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8821}{\htmlId{8821}{\htmlClass{Bound}{\text{expEpoch}}}}\,\,\htmlId{8829}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{8831}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8814}{\htmlId{8833}{\htmlClass{Bound}{\text{e}}}}\, \,\href{Class.HasOrder.Core.html#613}{\htmlId{8835}{\htmlClass{Field Operator}{\text{≤}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8821}{\htmlId{8837}{\htmlClass{Bound}{\text{expEpoch}}}}\,

\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8847}{\htmlId{8847}{\htmlClass{Function}{\text{activeDRepsOf}}}}\, \,\htmlId{8861}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{8863}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8864}{\htmlId{8864}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{8866}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Agda.Primitive.html#388}{\htmlId{8868}{\htmlClass{Primitive}{\text{Type}}}}\,\,\htmlId{8872}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{8874}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8876}{\htmlId{8876}{\htmlClass{Bound}{\text{\_}}}}\, \,\htmlId{8878}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4878}{\htmlId{8880}{\htmlClass{Record}{\text{HasDReps}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8864}{\htmlId{8889}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{8891}{\htmlClass{Symbol}{\text{⦄}}}\, \,\htmlId{8893}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8864}{\htmlId{8895}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{8897}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Core.Specification.Epoch.html#646}{\htmlId{8899}{\htmlClass{Function}{\text{Epoch}}}}\, \,\htmlId{8905}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4025}{\htmlId{8907}{\htmlClass{Function}{\text{DReps}}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8847}{\htmlId{8913}{\htmlClass{Function}{\text{activeDRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8927}{\htmlId{8927}{\htmlClass{Bound}{\text{a}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8929}{\htmlId{8929}{\htmlClass{Bound}{\text{e}}}}\, \,\htmlId{8931}{\htmlClass{Symbol}{\text{=}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#4102}{\htmlId{8933}{\htmlClass{Function}{\text{filterᵐ}}}}\, \,\htmlId{8941}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8750}{\htmlId{8942}{\htmlClass{Function}{\text{activeInEpoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8929}{\htmlId{8956}{\htmlClass{Bound}{\text{e}}}}\,\,\htmlId{8957}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{8959}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4927}{\htmlId{8960}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8927}{\htmlId{8968}{\htmlClass{Bound}{\text{a}}}}\,\,\htmlId{8969}{\htmlClass{Symbol}{\text{)}}}\,