Gov

{-# OPTIONS --safe #-}

open import Ledger.Conway.Abstract
open import Ledger.Prelude
open import Ledger.Conway.Transaction using (TransactionStructure)

module Ledger.Conway.Conformance.Gov
  (txs : _) (open TransactionStructure txs hiding (epoch))
  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
  where

open import Axiom.Set.Properties th using (∃-sublist-⇔)

open import Ledger.Conway.Enact govStructure
open import Ledger.Conway.Ledger txs abs

open import Ledger.Conway.Conformance.Certs govStructure
open import Ledger.Conway.Conformance.Equivalence.Certs txs abs
open import Ledger.Conway.Conformance.Equivalence.Convert

open import Ledger.Conway.Gov txs using (GovState) public
import Ledger.Conway.Gov txs as L

record GovEnv : Type where
  field
    txid        : TxId
    epoch       : Epoch
    pparams     : PParams
    ppolicy     : Maybe ScriptHash
    enactState  : EnactState
    certState   : CertState
    rewardCreds : ℙ Credential

instance
  unquoteDecl HasCast-GovEnv = derive-HasCast
    [ (quote GovEnv , HasCast-GovEnv) ]

_⊢_⇀⦇_,GOVS⦈_ : GovEnv → GovState → List (GovVote ⊎ GovProposal) → GovState → Type
Γ ⊢ govSt ⇀⦇ gvps ,GOVS⦈ govSt'
  = $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Gov.html#785}{\htmlId{1195}{\htmlClass{Function}{\text{txid}}}}\, \\ \,\href{Ledger.Conway.Conformance.Gov.html#808}{\htmlId{1202}{\htmlClass{Function}{\text{epoch}}}}\, \\ \,\href{Ledger.Conway.Conformance.Gov.html#832}{\htmlId{1210}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Conway.Conformance.Gov.html#858}{\htmlId{1220}{\htmlClass{Function}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Conway.Conformance.Gov.html#893}{\htmlId{1230}{\htmlClass{Function}{\text{enactState}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Convert.html#460}{\htmlId{1243}{\htmlClass{Function}{\text{conv}}}}\, \,\href{Ledger.Conway.Conformance.Gov.html#922}{\htmlId{1248}{\htmlClass{Function}{\text{certState}}}}\, \\
  \,\href{Ledger.Conway.Conformance.Gov.html#950}{\htmlId{1262}{\htmlClass{Function}{\text{rewardCreds}}}}\, \end{pmatrix}$ L.⊢ rmOrphanDRepVotes (conv certState) govSt  ⇀⦇ gvps ,GOVS⦈ govSt'
  where open GovEnv Γ