Governance
{-# OPTIONS --safe #-}
open import Ledger.Dijkstra.Specification.Gov.Base
module Ledger.Dijkstra.Specification.Gov (govStructure : GovStructure) where
open import Ledger.Prelude hiding (any?; Any; all?; All; Rel; lookup; ∈-filter)
open import Axiom.Set.Properties th using (∃-sublist-⇔)
open import Ledger.Core.Specification.ProtocolVersion
open import Ledger.Dijkstra.Specification.Gov.Actions govStructure hiding (yes; no)
open import Ledger.Dijkstra.Specification.Enact govStructure
open import Ledger.Dijkstra.Specification.Ratify govStructure
open import Ledger.Dijkstra.Specification.Certs govStructure
open import stdlib.Data.List.Subpermutations using (subpermutations; sublists)
open import stdlib.Data.List.Subpermutations.Properties
using (∃uniqueSubset⇔∃uniqueSubperm; maxsublists⊧P; maxlen; sublists⊧P; ∈-maxlen-≤)
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 EnactState using (cc)
open GovStructure govStructure
Governance Types and Functions
GovState : Type
GovState = List (GovActionID × GovActionState)
record GovEnv : Type where
field
txid : TxId
epoch : Epoch
pparams : PParams
ppolicy : Maybe ScriptHash
enactState : EnactState
certState : CertState
rewardCreds : ℙ Credential
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'
record HasGovState {a} (A : Type a) : Type a where
field GovStateOf : A → GovState
open HasGovState ⦃...⦄ public
record HasRewardCredentials {a} (A : Type a) : Type a where
field RewardCredentialsOf : A → ℙ Credential
open HasRewardCredentials ⦃...⦄ public
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
HasEpoch-GovEnv : HasEpoch GovEnv
HasEpoch-GovEnv .EpochOf = GovEnv.epoch
HasRewardCredentials-GovEnv : HasRewardCredentials GovEnv
HasRewardCredentials-GovEnv .RewardCredentialsOf = GovEnv.rewardCreds
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 : RewardAddress
a : GovAction
prev : NeedsHash (gaType a)
k : ℕ
p : Maybe ScriptHash
open GState
open PState
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 (GovActionTypeOf gaSt₀) ≤ govActionPriority (GovActionTypeOf gaSt₁)
then (gaID₀ , gaSt₀) ∷ insertGovAction gaPrs (gaID₁ , gaSt₁)
else (gaID₁ , gaSt₁) ∷ (gaID₀ , gaSt₀) ∷ gaPrs
mkGovStatePair
: Epoch
→ GovActionID
→ RewardAddress
→ (a : GovAction)
→ NeedsHash (a .gaType)
→ Coin
→ GovActionID × GovActionState
mkGovStatePair e aid addr a prev d = (aid , gas)
where
gas : GovActionState
gas = record { votes = record { gvCC = ∅ ; gvDRep = ∅ ; gvSPO = ∅ }
; returnAddr = addr
; expiresIn = e
; action = a
; prevAction = prev
; deposit = d
}
addAction
: GovState → Epoch → GovActionID → RewardAddress
→ (a : GovAction) → NeedsHash (a .gaType)
→ Coin
→ GovState
addAction s e aid addr a prev d = insertGovAction s (mkGovStatePair e aid addr a prev d)
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 (GovVotesOf gaSt)
votes' : GovVoter → GovVotes
votes' $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{7926}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.html#7931}{\htmlId{7931}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = record { gvCC = insert gvCC c v ; gvDRep = gvDRep ; gvSPO = gvSPO }
votes' $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{8022}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.html#8029}{\htmlId{8029}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = record { gvCC = gvCC ; gvDRep = insert gvDRep c v ; gvSPO = gvSPO }
votes' $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{8120}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.html#8126}{\htmlId{8126}{\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.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{8298}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.html#8305}{\htmlId{8305}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ → just c ∈ range (CCHotKeysOf (CertStateOf Γ) ∣ (ccCreds (cc (EnactStateOf Γ))))
$\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{8401}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.html#8408}{\htmlId{8408}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ → c ∈ dom (DRepsOf (CertStateOf Γ))
$\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{8459}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.html#8466}{\htmlId{8466}{\htmlClass{Bound}{\text{kh}}}}\, \end{pmatrix}$ → kh ∈ dom (PoolsOf (CertStateOf Γ))
validHFAction : GovProposal → GovState → EnactState → Type
validHFAction (record { action = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1163}{\htmlId{8609}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.html#8627}{\htmlId{8627}{\htmlClass{Bound}{\text{v}}}}\, \end{pmatrix}$ ; prevAction = prev }) s e =
(aid' ≡ prev × pvCanFollow v ver) ⊎ ∃₂[ x , v' ] (prev , x) ∈ fromList s
× GovActionState.action x ≡ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1163}{\htmlId{8824}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.html#8710}{\htmlId{8842}{\htmlClass{Bound}{\text{v'}}}}\, \end{pmatrix}$
× (if pvCanFollowMajor v' ver
then pvCanFollowMinor v v'
else pvCanFollow v v')
where
ver : ProtVer
ver = EnactState.pv e .proj₁
aid' : GovActionID
aid' = EnactState.pv e .proj₂
validHFAction _ _ _ = ⊤
getAidPairsList : GovState → List (GovActionID × GovActionID)
getAidPairsList aid×states =
mapMaybe (λ (aid , aState) → (aid ,_) <$> getHash (GovActionState.prevAction aState)) $ aid×states
_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 (GovActionTypeOf as) 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 _
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
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 : EnactState → GovState → List GovState
maxAllEnactable e = maxsublists⊧P (allEnactable? e)
∈-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∈)))
∈-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 _ p ppolicy _ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1201}{\htmlId{14998}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\htmlId{15014}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = p ≡ ppolicy
actionValid rwdCreds p ppolicy _ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1239}{\htmlId{15069}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.html#15090}{\htmlId{15090}{\htmlClass{Bound}{\text{wdrls}}}}\, \end{pmatrix}$ = p ≡ ppolicy × mapˢ CredentialOf (dom wdrls) ⊆ rwdCreds
actionValid _ p _ epoch $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1087}{\htmlId{15183}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{15201}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.html#15202}{\htmlId{15202}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.html#15208}{\htmlId{15208}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.html#15214}{\htmlId{15214}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{15215}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ = p ≡ nothing × (∀[ e ∈ range new ] epoch < e) × dom new ∩ rem ≡ᵉ ∅
actionValid _ p _ _ _ = p ≡ nothing
actionWellFormed : GovAction → Type
actionWellFormed $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1201}{\htmlId{15426}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.html#15442}{\htmlId{15442}{\htmlClass{Bound}{\text{ppup}}}}\, \end{pmatrix}$ = ppdWellFormed ppup
actionWellFormed $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1239}{\htmlId{15491}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.html#15512}{\htmlId{15512}{\htmlClass{Bound}{\text{wdrls}}}}\, \end{pmatrix}$ = (∀[ a ∈ dom wdrls ] NetworkIdOf a ≡ NetworkId)
× ∃[ v ∈ range wdrls ] ¬ (v ≡ 0)
actionWellFormed _ = ⊤
actionValid? : ∀ {rewardCreds p ppolicy epoch a} → actionValid rewardCreds p ppolicy epoch a ⁇
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1049}{\htmlId{15814}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\htmlId{15836}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1087}{\htmlId{15868}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{15890}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1125}{\htmlId{15922}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{15944}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1163}{\htmlId{15976}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\htmlId{15998}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1201}{\htmlId{16030}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\htmlId{16052}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1239}{\htmlId{16084}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\htmlId{16106}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1277}{\htmlId{16138}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\htmlId{16160}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? : ∀ {a} → actionWellFormed a ⁇
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1049}{\htmlId{16243}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\htmlId{16265}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1087}{\htmlId{16298}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{16320}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1125}{\htmlId{16353}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{16375}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1163}{\htmlId{16408}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\htmlId{16430}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1201}{\htmlId{16463}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\htmlId{16485}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1239}{\htmlId{16518}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\htmlId{16540}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1277}{\htmlId{16573}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\htmlId{16595}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
open GovEnv
open PParams hiding (a)
open GovVoter
variable
machr : Maybe Anchor
achr : Anchor
ast : GovActionState
The GOV Transition System
data _⊢_⇀⦇_,GOV⦈_ : GovEnv × ℕ → GovState → GovVote ⊎ GovProposal → GovState → Type where
GOV-Vote :
∙ (aid , ast) ∈ fromList s
∙ canVote (PParamsOf Γ) (GovActionOf ast) (gvRole voter)
∙ isRegistered Γ voter
∙ ¬ expired (Γ .epoch) ast
───────────────────────────────────────
(Γ , k) ⊢ s ⇀⦇ inj₁ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.html#3632}{\htmlId{17170}{\htmlClass{Generalizable}{\text{aid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.html#3655}{\htmlId{17176}{\htmlClass{Generalizable}{\text{voter}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.html#3694}{\htmlId{17184}{\htmlClass{Generalizable}{\text{v}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.html#16670}{\htmlId{17188}{\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
(pp. govActionDeposit)
_⊢_⇀⦇_,GOVS⦈_ : GovEnv → GovState → List (GovVote ⊎ GovProposal) → GovState → Type
_⊢_⇀⦇_,GOVS⦈_ = ReflexiveTransitiveClosureᵢ {sts = _⊢_⇀⦇_,GOV⦈_}