Ledger.Conway.Specification.Gov

{-# 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 : Voter
  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 , record
  { votes = ∅ ; 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 → Voter → Vote → GovState
  addVote s aid voter v = map modifyVotes s
    where modifyVotes : GovActionID × GovActionState → GovActionID × GovActionState
          modifyVotes = λ (gid , s') → gid , record s'
            { votes = if gid ≡ aid then insert (votes s') voter v else votes s'}

  isRegistered : GovEnv → Voter → Type
  isRegistered Γ (r , c) = case r of


    λ where


      CC    → just c ∈ range (gState .ccHotKeys)
      DRep  → c ∈ dom (gState .dreps)
      SPO   → c ∈ mapˢ KeyHashObj (dom (pState .pools))
        where
          open CertState (GovEnv.certState Γ) using (gState; pState)

  validHFAction : GovProposal → GovState → EnactState → Type
  validHFAction (record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#923}{\htmlId{7151}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#7169}{\htmlId{7169}{\htmlClass{Bound}{\text{v}}}}\, \end{pmatrix}$ ; prevAction = prev }) s e =
    (let (v' , aid) = EnactState.pv e in aid ≡ prev × pvCanFollow v' v)
    ⊎ ∃₂[ x , v' ] (prev , x) ∈ fromList s × x .action ≡ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#923}{\htmlId{7335}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#7290}{\htmlId{7353}{\htmlClass{Bound}{\text{v'}}}}\, \end{pmatrix}$ × pvCanFollow v' v
  validHFAction _ _ _ = ⊤


data


  _⊢_⇀⦇_,GOV⦈_  : GovEnv × ℕ → GovState → GovVote ⊎ GovProposal → GovState → Type


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


-- 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#961}{\htmlId{13149}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\htmlId{13165}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ =
  p ≡ ppolicy
actionValid rewardCreds p ppolicy epoch $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#999}{\htmlId{13229}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\href{Ledger.Conway.Specification.Gov.html#13251}{\htmlId{13251}{\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#847}{\htmlId{13358}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{13376}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.html#13377}{\htmlId{13377}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Conway.Specification.Gov.html#13383}{\htmlId{13383}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Conway.Specification.Gov.html#13389}{\htmlId{13389}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{13390}{\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#961}{\htmlId{13583}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#13599}{\htmlId{13599}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ = ppdWellFormed x
actionWellFormed $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#999}{\htmlId{13642}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\href{Ledger.Conway.Specification.Gov.html#13664}{\htmlId{13664}{\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#809}{\htmlId{13904}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,    \\ \,\htmlId{13922}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#847}{\htmlId{13954}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{13972}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#885}{\htmlId{14004}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{14022}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#923}{\htmlId{14054}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,       \\ \,\htmlId{14078}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#961}{\htmlId{14110}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,   \\ \,\htmlId{14128}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#999}{\htmlId{14160}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,    \\ \,\htmlId{14184}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1037}{\htmlId{14216}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,            \\ \,\htmlId{14234}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it

actionWellFormed? : ∀ {a} → actionWellFormed a ⁇
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#809}{\htmlId{14317}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,    \\ \,\htmlId{14335}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#847}{\htmlId{14368}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{14386}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#885}{\htmlId{14419}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{14437}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#923}{\htmlId{14470}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,       \\ \,\htmlId{14494}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#961}{\htmlId{14527}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,   \\ \,\htmlId{14545}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#999}{\htmlId{14578}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,    \\ \,\htmlId{14602}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1037}{\htmlId{14635}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,            \\ \,\htmlId{14653}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it


open GovEnv
open PParams hiding (a)

variable
  machr : Maybe Anchor
  achr : Anchor
  ast  : GovActionState


data _⊢_⇀⦇_,GOV⦈_ where


  GOV-Vote :
    ∙ (aid , ast) ∈ fromList s
    ∙ canVote (PParamsOf Γ) (action ast) (proj₁ voter)
    ∙ isRegistered Γ voter
    ∙ ¬ expired (Γ .epoch) ast
      ───────────────────────────────────────
      (Γ , k) ⊢ s ⇀⦇ inj₁ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.html#2335}{\htmlId{15035}{\htmlClass{Generalizable}{\text{aid}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#2355}{\htmlId{15041}{\htmlClass{Generalizable}{\text{voter}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#2388}{\htmlId{15049}{\htmlClass{Generalizable}{\text{v}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#14715}{\htmlId{15053}{\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⦈_ = ReflexiveTransitiveClosureᵢ {sts = _⊢_⇀⦇_,GOV⦈_}