{-# OPTIONS --safe #-}

open import Ledger.Conway.Specification.Gov.Base
open import Ledger.Conway.Specification.Transaction using (TransactionStructure)

module Ledger.Conway.Specification.Gov (txs : _) (open TransactionStructure txs hiding (epoch)) where

open import Ledger.Prelude hiding (any?; Any; all?; All; Rel; lookup; ∈-filter)

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

open import Ledger.Conway.Specification.Gov.Actions govStructure using (Vote)
open import Ledger.Conway.Specification.Enact govStructure
open import Ledger.Conway.Specification.Ratify txs hiding (vote)
open import Ledger.Conway.Specification.Certs govStructure

open import stdlib.Data.List.Subpermutations using (subpermutations; sublists)
open import stdlib.Data.List.Subpermutations.Properties
open import Data.List.Membership.Propositional.Properties using (Any↔; ∈-filter⁻; ∈-filter⁺)
open import Data.List.Relation.Binary.Subset.Propositional using () renaming (_⊆_ to _⊆ˡ_)
open import Data.List.Relation.Unary.All using (all?; All)
open import Data.List.Relation.Unary.Any using (any?; Any)
open import Data.List.Relation.Unary.Unique.DecPropositional using (unique?)
open import Data.List.Relation.Unary.Unique.Propositional using (Unique)
open import Relation.Nullary.Decidable using () renaming (map to map-Dec)
open import Function.Properties.Equivalence using () renaming (sym to sym-Equiv)
open import Function.Related.Propositional using (↔⇒)

open GovActionState


GovState : Type
GovState = List (GovActionID × GovActionState)


record HasGovState {a} (A : Type a) : Type a where
  field GovStateOf : A  GovState
open HasGovState ⦃...⦄ public


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


instance
  HasPParams-GovEnv : HasPParams GovEnv
  HasPParams-GovEnv .PParamsOf = GovEnv.pparams

  HasEnactState-GovEnv : HasEnactState GovEnv
  HasEnactState-GovEnv .EnactStateOf = GovEnv.enactState

  HasCertState-GovEnv : HasCertState GovEnv
  HasCertState-GovEnv .CertStateOf = GovEnv.certState

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

private variable
  Γ      : GovEnv
  s s'   : GovState
  aid    : GovActionID
  voter  : GovVoter
  vote   : GovVote
  v      : Vote
  d      : Coin
  addr   : RwdAddr
  a      : GovAction
  prev   : NeedsHash (gaType a)
  k      : 
  p      : Maybe ScriptHash

open GState
open PState


govActionPriority : GovActionType  
govActionPriority NoConfidence        = 0
govActionPriority UpdateCommittee     = 1
govActionPriority NewConstitution     = 2
govActionPriority TriggerHardFork     = 3
govActionPriority ChangePParams       = 4
govActionPriority TreasuryWithdrawal  = 5
govActionPriority Info                = 6

Overlap : GovActionType  GovActionType  Type
Overlap NoConfidence     UpdateCommittee  = 
Overlap UpdateCommittee  NoConfidence     = 
Overlap a                a'               = a  a'


-- TODO: cleanup this
Overlap? : (a a' : GovActionType)  Dec (Overlap a a')
Overlap? NoConfidence    UpdateCommittee  = Dec-⊤ .dec
Overlap? UpdateCommittee NoConfidence     = Dec-⊤ .dec
Overlap? NoConfidence NoConfidence = yes refl
Overlap? NoConfidence NewConstitution = no  ())
Overlap? NoConfidence TriggerHardFork = no  ())
Overlap? NoConfidence ChangePParams = no  ())
Overlap? NoConfidence TreasuryWithdrawal = no  ())
Overlap? NoConfidence Info = no  ())
Overlap? UpdateCommittee UpdateCommittee = yes refl
Overlap? UpdateCommittee NewConstitution = no  ())
Overlap? UpdateCommittee TriggerHardFork = no  ())
Overlap? UpdateCommittee ChangePParams = no  ())
Overlap? UpdateCommittee TreasuryWithdrawal = no  ())
Overlap? UpdateCommittee Info = no  ())
Overlap? NewConstitution NoConfidence = no  ())
Overlap? NewConstitution UpdateCommittee = no  ())
Overlap? NewConstitution NewConstitution = yes refl
Overlap? NewConstitution TriggerHardFork = no  ())
Overlap? NewConstitution ChangePParams = no  ())
Overlap? NewConstitution TreasuryWithdrawal = no  ())
Overlap? NewConstitution Info = no  ())
Overlap? TriggerHardFork NoConfidence = no  ())
Overlap? TriggerHardFork UpdateCommittee = no  ())
Overlap? TriggerHardFork NewConstitution = no  ())
Overlap? TriggerHardFork TriggerHardFork = yes refl
Overlap? TriggerHardFork ChangePParams = no  ())
Overlap? TriggerHardFork TreasuryWithdrawal = no  ())
Overlap? TriggerHardFork Info = no  ())
Overlap? ChangePParams NoConfidence = no  ())
Overlap? ChangePParams UpdateCommittee = no  ())
Overlap? ChangePParams NewConstitution = no  ())
Overlap? ChangePParams TriggerHardFork = no  ())
Overlap? ChangePParams ChangePParams = yes refl
Overlap? ChangePParams TreasuryWithdrawal = no  ())
Overlap? ChangePParams Info = no  ())
Overlap? TreasuryWithdrawal NoConfidence = no  ())
Overlap? TreasuryWithdrawal UpdateCommittee = no  ())
Overlap? TreasuryWithdrawal NewConstitution = no  ())
Overlap? TreasuryWithdrawal TriggerHardFork = no  ())
Overlap? TreasuryWithdrawal ChangePParams = no  ())
Overlap? TreasuryWithdrawal TreasuryWithdrawal = yes refl
Overlap? TreasuryWithdrawal Info = no  ())
Overlap? Info NoConfidence = no  ())
Overlap? Info UpdateCommittee = no  ())
Overlap? Info NewConstitution = no  ())
Overlap? Info TriggerHardFork = no  ())
Overlap? Info ChangePParams = no  ())
Overlap? Info TreasuryWithdrawal = no  ())
Overlap? Info Info = yes refl


insertGovAction : GovState  GovActionID × GovActionState  GovState
insertGovAction [] gaPr = [ gaPr ]
insertGovAction ((gaID₀ , gaSt₀)  gaPrs) (gaID₁ , gaSt₁)
  =  if govActionPriority (action gaSt₀ .gaType)  govActionPriority (action gaSt₁ .gaType)
     then (gaID₀ , gaSt₀)  insertGovAction gaPrs (gaID₁ , gaSt₁)
     else (gaID₁ , gaSt₁)  (gaID₀ , gaSt₀)  gaPrs

mkGovStatePair :  Epoch  GovActionID  RwdAddr  (a : GovAction)  NeedsHash (a .gaType)
                   GovActionID × GovActionState
mkGovStatePair e aid addr a prev = (aid , gas)
  where
  gas : GovActionState
  gas = record  { votes = record { gvCC =  ; gvDRep =  ; gvSPO =  }
                ; returnAddr = addr
                ; expiresIn = e
                ; action = a
                ; prevAction = prev
                }

addAction :  GovState  Epoch  GovActionID  RwdAddr
              (a : GovAction)  NeedsHash (a .gaType)
              GovState
addAction s e aid addr a prev = insertGovAction s (mkGovStatePair e aid addr a prev)


opaque


  addVote : GovState  GovActionID  GovVoter  Vote  GovState
  addVote gSt aid voter v = map modifyVotes gSt
    where
    modifyVotes : GovActionID × GovActionState  GovActionID × GovActionState
    modifyVotes (gid , gaSt) = gid , (if gid  aid then record gaSt { votes = votes' voter } else gaSt)
      where
      open GovVotes (votes gaSt)
      votes' : GovVoter  GovVotes
      votes' $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#368}{\htmlId{7034}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#7039}{\htmlId{7039}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = record { gvCC = insert gvCC c v ; gvDRep = gvDRep ; gvSPO = gvSPO }
      votes' $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#371}{\htmlId{7130}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#7137}{\htmlId{7137}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = record { gvCC = gvCC ; gvDRep = insert gvDRep c v ; gvSPO = gvSPO }
      votes' $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#376}{\htmlId{7228}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#7234}{\htmlId{7234}{\htmlClass{Bound}{\text{kh}}}}\, \end{pmatrix}$ = record { gvCC = gvCC ; gvDRep = gvDRep ; gvSPO = insert gvSPO kh v }

  isRegistered : GovEnv  GovVoter  Type
  isRegistered Γ v = case v of
    λ where
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#368}{\htmlId{7406}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Specification.Gov.html#7413}{\htmlId{7413}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix}$  just c  range (CCHotKeysOf (CertStateOf Γ))
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#371}{\htmlId{7475}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#7482}{\htmlId{7482}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix}$  c  dom (DRepsOf (CertStateOf Γ))
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#376}{\htmlId{7533}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  \\ \,\href{Ledger.Conway.Specification.Gov.html#7540}{\htmlId{7540}{\htmlClass{Bound}{\text{kh}}}}\, \end{pmatrix}$  kh  dom (PoolsOf (CertStateOf Γ))

  validHFAction : GovProposal  GovState  EnactState  Type
  validHFAction (record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1111}{\htmlId{7683}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#7701}{\htmlId{7701}{\htmlClass{Bound}{\text{v}}}}\, \end{pmatrix}$ ; prevAction = prev }) s e =
    (aid'  prev × pvCanFollow ver v)  ∃₂[ x , v' ]  (prev , x)  fromList s
                                                      × x .action  $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1111}{\htmlId{7884}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#7784}{\htmlId{7902}{\htmlClass{Bound}{\text{v'}}}}\, \end{pmatrix}$
                                                      × pvCanFollow v' v
    where
      ver : ProtVer
      ver = EnactState.pv e .proj₁
      aid' : GovActionID
      aid' = EnactState.pv e .proj₂

  validHFAction _ _ _ = 


-- Convert list of (GovActionID,GovActionState)-pairs to list of GovActionID pairs.
getAidPairsList : GovState  List (GovActionID × GovActionID)
getAidPairsList aid×states =
  mapMaybe  (aid , aState)  (aid ,_) <$> getHash (prevAction aState)) $ aid×states

-- A list of GovActionID pairs connects the first GovActionID to the second.
_connects_to_ : List (GovActionID × GovActionID)  GovActionID  GovActionID  Type
[] connects aidNew to aidOld = aidNew  aidOld
((aid , aidPrev)  s) connects aidNew to aidOld  =
  aid  aidNew × s connects aidPrev to aidOld  s connects aidNew to aidOld


enactable  : EnactState  List (GovActionID × GovActionID)
            GovActionID × GovActionState  Type
enactable e aidPairs = λ (aidNew , as)  case getHashES e (action as .gaType) of
  λ where
   nothing         
   (just aidOld)   ∃[ t ]  fromList t  fromList aidPairs
                            × Unique t × t connects aidNew to aidOld

allEnactable : EnactState  GovState  Type
allEnactable e aid×states = All (enactable e (getAidPairsList aid×states)) aid×states

hasParentE : EnactState  GovActionID  GovActionType  Type
hasParentE e aid gaTy = case getHashES e gaTy of
  λ where
    nothing     
    (just id)   id  aid

hasParent : EnactState  GovState  (gaTy : GovActionType)  NeedsHash gaTy  Type
hasParent e s gaTy aid = case getHash aid of
  λ where
    nothing       
    (just aid')   hasParentE e aid' gaTy
                    Any  (gid , gas)  gid  aid' × Overlap (GovActionTypeOf gas) gaTy) s


open Equivalence

hasParentE? :  e aid a  Dec (hasParentE e aid a)
hasParentE? e aid gaTy with getHashES e gaTy
... | nothing   = yes _
... | (just id) = id  aid

hasParent? :  e s a aid  Dec (hasParent e s a aid)
hasParent? e s gaTy aid with getHash aid
... | just aid' = hasParentE? e aid' gaTy
                  ⊎-dec any?  (gid , gas)  gid  aid' ×-dec Overlap? (GovActionTypeOf gas) gaTy) s
... | nothing = yes _

-- newtype to make the instance resolution work
data hasParent' : EnactState  GovState  (gaTy : GovActionType)  NeedsHash gaTy  Type where
  HasParent' :  {x y z w}  hasParent x y z w  hasParent' x y z w

instance
  hasParent?' :  {x y z w}  hasParent' x y z w 
  hasParent?' =  map′ HasParent'  where (HasParent' x)  x) (hasParent? _ _ _ _)

[_connects_to_?] :  l aidNew aidOld  Dec (l connects aidNew to aidOld)
[ [] connects aidNew to aidOld ?] = aidNew  aidOld

[ (aid , aidPrev)  s connects aidNew to aidOld ?] =
  ((aid  aidNew) ×-dec [ s connects aidPrev to aidOld ?]) ⊎-dec [ s connects aidNew to aidOld ?]

any?-connecting-subperm :  {u} {v}   L  Dec (Any l  Unique l × l connects u to v) (subpermutations L))
any?-connecting-subperm {u} {v} L = any?  l  unique? _≟_ l ×-dec [ l connects u to v ?]) (subpermutations L)

∃?-connecting-subperm :  {u} {v}   L  Dec (∃[ l ] l ∈ˡ subpermutations L × Unique l × l connects u to v)
∃?-connecting-subperm L = map-Dec (sym-Equiv (↔⇒ Any↔)) (any?-connecting-subperm L)

∃?-connecting-subset :  {u} {v}   L  Dec (∃[ l ] l ⊆ˡ L × Unique l × l connects u to v)
∃?-connecting-subset L = map-Dec (sym-Equiv ∃uniqueSubset⇔∃uniqueSubperm) (∃?-connecting-subperm L)

enactable? :  eState aidPairs aidNew×st  Dec (enactable eState aidPairs aidNew×st)
enactable? eState aidPairs (aidNew , as) with getHashES eState (GovActionTypeOf as)
... | nothing = yes tt
... | just aidOld = map-Dec (sym-Equiv ∃-sublist-⇔) (∃?-connecting-subset aidPairs)

allEnactable? :  eState aid×states  Dec (allEnactable eState aid×states)
allEnactable? eState aid×states =
  all?  aid×st  enactable? eState (getAidPairsList aid×states) aid×st) aid×states

-- newtype to make the instance resolution work
data allEnactable' : EnactState  GovState  Type where
  AllEnactable' :  {x y}  allEnactable x y  allEnactable' x y

instance
  allEnactable?' :  {x y}  allEnactable' x y 
  allEnactable?' =  map′ AllEnactable'  where (AllEnactable' x)  x) (allEnactable? _ _)

-- `maxAllEnactable` returns a list `ls` of sublists of the given
-- list (`aid×states : List (GovActionID × GovActionState)`) such that
--    (i) each sublist `l ∈ ls` satisfies `allEnactable e l` and
--   (ii) each sublist `l ∈ ls` is of maximal length among sublists of `aid×states` satisfying `allEnactable`.
maxAllEnactable : EnactState  GovState  List GovState
maxAllEnactable e = maxsublists⊧P (allEnactable? e)

-- Every sublist returned by `maxAllEnactable` satisfies (i).
∈-maxAllEnactable→allEnactable :  {e} {aid×states} l
   l ∈ˡ maxAllEnactable e aid×states  allEnactable e l
∈-maxAllEnactable→allEnactable {e} {aid×states} l l∈ =
  proj₂ (∈-filter⁻ (allEnactable? e) {l} {sublists aid×states}
          (proj₁ (∈-filter⁻  l  length l  maxlen (sublists⊧P (allEnactable? e) aid×states)) l∈)))

-- Every sublist returned by `maxAllEnactable` satisfies (ii).
∈-maxAllEnactable→maxLength :  {e aid×states l l'}
                               l ∈ˡ sublists aid×states  allEnactable e l
                               l' ∈ˡ maxAllEnactable e aid×states
                               length l  length l'
∈-maxAllEnactable→maxLength {e} {aid×states} {l} {l'} l∈ el l'∈ =
  let ls = sublists⊧P (allEnactable? e) aid×states in
    subst (length l ≤_)
          (sym (proj₂ (∈-filter⁻  l  length l  maxlen ls) {xs = ls} l'∈)))
          (∈-maxlen-≤ l (∈-filter⁺ (allEnactable? e) l∈ el))


actionValid :  Credential  Maybe ScriptHash  Maybe ScriptHash  Epoch  GovAction  Type
actionValid rewardCreds p ppolicy epoch $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1149}{\htmlId{13691}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\htmlId{13707}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ =
  p  ppolicy
actionValid rewardCreds p ppolicy epoch $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1187}{\htmlId{13771}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\href{Ledger.Conway.Specification.Gov.html#13793}{\htmlId{13793}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ =
  p  ppolicy × mapˢ RwdAddr.stake (dom x)  rewardCreds
actionValid rewardCreds p ppolicy epoch $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1035}{\htmlId{13900}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{13918}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.html#13919}{\htmlId{13919}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Conway.Specification.Gov.html#13925}{\htmlId{13925}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Conway.Specification.Gov.html#13931}{\htmlId{13931}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{13932}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ =
  p  nothing × (∀[ e  range new ]  epoch < e) × (dom new  rem ≡ᵉ )
actionValid rewardCreds p ppolicy epoch _ =
  p  nothing

actionWellFormed : GovAction  Type
actionWellFormed $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1149}{\htmlId{14125}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#14141}{\htmlId{14141}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ = ppdWellFormed x
actionWellFormed $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1187}{\htmlId{14184}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\href{Ledger.Conway.Specification.Gov.html#14206}{\htmlId{14206}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ =
  (∀[ a  dom x ] NetworkIdOf a  NetworkId) × (∃[ v  range x ] ¬ (v  0))
actionWellFormed _                 = 


actionValid? :  {rewardCreds p ppolicy epoch a}  actionValid rewardCreds p ppolicy epoch a 
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#997}{\htmlId{14446}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,        \\ \,\htmlId{14468}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1035}{\htmlId{14500}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\,     \\ \,\htmlId{14522}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1073}{\htmlId{14554}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\,     \\ \,\htmlId{14576}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1111}{\htmlId{14608}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,     \\ \,\htmlId{14630}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1149}{\htmlId{14662}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,       \\ \,\htmlId{14684}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1187}{\htmlId{14716}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\htmlId{14738}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1225}{\htmlId{14770}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,                \\ \,\htmlId{14792}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it

actionWellFormed? :  {a}  actionWellFormed a 
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#997}{\htmlId{14875}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,        \\ \,\htmlId{14897}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1035}{\htmlId{14930}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\,     \\ \,\htmlId{14952}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1073}{\htmlId{14985}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\,     \\ \,\htmlId{15007}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1111}{\htmlId{15040}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,     \\ \,\htmlId{15062}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1149}{\htmlId{15095}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,       \\ \,\htmlId{15117}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1187}{\htmlId{15150}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\htmlId{15172}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1225}{\htmlId{15205}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,                \\ \,\htmlId{15227}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it

open GovEnv
open PParams hiding (a)
open GovVoter

variable
  machr : Maybe Anchor
  achr : Anchor
  ast  : GovActionState


data _⊢_⇀⦇_,GOV⦈_ : GovEnv ×   GovState  GovVote  GovProposal  GovState  Type where

  GOV-Vote :
     (aid , ast)  fromList s
     canVote (PParamsOf Γ) (action ast) (gvRole voter)
     isRegistered Γ voter
     ¬ expired (Γ .epoch) ast
      ───────────────────────────────────────
      (Γ , k)  s ⇀⦇ inj₁ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.html#2339}{\htmlId{15688}{\htmlClass{Generalizable}{\text{aid}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#2362}{\htmlId{15694}{\htmlClass{Generalizable}{\text{voter}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#2401}{\htmlId{15702}{\htmlClass{Generalizable}{\text{v}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#15302}{\htmlId{15706}{\htmlClass{Generalizable}{\text{machr}}}}\, \end{pmatrix}$ ,GOV⦈ addVote s aid voter v

  GOV-Propose :
    let pp           = PParamsOf Γ
        e            = Γ .epoch
        enactState   = EnactStateOf Γ
        rewardCreds  = Γ .rewardCreds
        prop         = record { returnAddr = addr ; action = a ; anchor = achr
                              ; policy = p ; deposit = d ; prevAction = prev }
    in
     actionWellFormed a
     actionValid rewardCreds p (Γ .ppolicy) e a
     d  pp .govActionDeposit
     validHFAction prop s enactState
     hasParent enactState s (GovActionTypeOf a) prev
     NetworkIdOf addr  NetworkId
     CredentialOf addr  rewardCreds
      ───────────────────────────────────────
      (Γ , k)  s ⇀⦇ inj₂ prop ,GOV⦈ addAction s (pp .govActionLifetime +ᵉ e)
                                                 (Γ .txid , k) addr a prev



_⊢_⇀⦇_,GOVS⦈_ : GovEnv  GovState  List (GovVote  GovProposal)  GovState  Type


_⊢_⇀⦇_,GOVS⦈_ = ReflexiveTransitiveClosureᵢ {sts = _⊢_⇀⦇_,GOV⦈_}