Enactment¶
Auxiliary Types and Functions¶
This section contains some definitions required to define the
ENACT
transition system. EnactEnv
is the environment
and EnactState
the state of ENACT
, which enacts a
governance action. All governance actions except
TreasuryWithdrawal
and
Info
modify EnactState
permanently,
which of course can have further consequences.
TreasuryWithdrawal
accumulates withdrawal temporarily in
the withdrawals
field of EnactState
, but this information
is applied and reset in EPOCH
(see EPOCH Transition System).
Also, enacting these governance actions is the only way of modifying
EnactState
.
Note that all other fields of EnactState
also contain a
GovActionID
since they are HashProtected
.
record EnactEnv : Type where field gid : GovActionID treasury : Treasury epoch : Epoch record EnactState : Type where field cc : HashProtected (Maybe ((Credential ⇀ Epoch) × ℚ)) constitution : HashProtected (DocHash × Maybe ScriptHash) pv : HashProtected ProtVer pparams : HashProtected PParams withdrawals : Withdrawals
ccCreds : HashProtected (Maybe ((Credential ⇀ Epoch) × ℚ)) → ℙ Credential ccCreds (just x , _) = dom (x .proj₁) ccCreds (nothing , _) = ∅ getHash : ∀ {a} → NeedsHash a → Maybe GovActionID getHash {NoConfidence} h = just h getHash {UpdateCommittee} h = just h getHash {NewConstitution} h = just h getHash {TriggerHardFork} h = just h getHash {ChangePParams} h = just h getHash {TreasuryWithdrawal} _ = nothing getHash {Info} _ = nothing getHashES : EnactState → GovActionType → Maybe GovActionID getHashES es NoConfidence = just (es .cc .proj₂) getHashES es (UpdateCommittee) = just (es .cc .proj₂) getHashES es (NewConstitution) = just (es .constitution .proj₂) getHashES es (TriggerHardFork) = just (es .pv .proj₂) getHashES es (ChangePParams) = just (es .pparams .proj₂) getHashES es (TreasuryWithdrawal) = nothing getHashES es Info = nothing
Type of the ENACT transition system
data _⊢_⇀⦇_,ENACT⦈_ : EnactEnv → EnactState → GovAction → EnactState → Type
ENACT Transition System¶
This section defines the rules of the ENACT
transition system.
Usually no preconditions are checked and the state is simply updated (including the
GovActionID
for the hash protection scheme, if
required). The exceptions are UpdateCommittee
and
TreasuryWithdrawal
:
-
UpdateCommittee
requires that maximum terms are respected, and -
TreasuryWithdrawal
requires that the treasury is able to cover the sum of all withdrawals (old and new).
Enact-NoConf : ─────────────────────────────────────── $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#3864}{\htmlId{4801}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3849}{\htmlId{4807}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3884}{\htmlId{4811}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1877}{\htmlId{4824}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\htmlId{4839}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ ,ENACT⦈ record s { cc = nothing , gid } Enact-UpdComm : let old = maybe proj₁ ∅ (s .cc .proj₁) maxTerm = CCMaxTermLengthOf s +ᵉ e in ∀[ term ∈ range new ] term ≤ maxTerm ─────────────────────────────────────── $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#3864}{\htmlId{5118}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3849}{\htmlId{5124}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3884}{\htmlId{5128}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1915}{\htmlId{5141}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{5159}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Enact.html#3719}{\htmlId{5160}{\htmlClass{Generalizable}{\text{new}}}}\, , \,\href{Ledger.Conway.Specification.Enact.html#3746}{\htmlId{5166}{\htmlClass{Generalizable}{\text{rem}}}}\, , \,\href{Ledger.Conway.Specification.Enact.html#3767}{\htmlId{5172}{\htmlClass{Generalizable}{\text{q}}}}\,\,\htmlId{5173}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ,ENACT⦈ record s { cc = just ((new ∪ˡ old) ∣ rem ᶜ , q) , gid } Enact-NewConst : ─────────────────────────────────────── $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#3864}{\htmlId{5319}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3849}{\htmlId{5325}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3884}{\htmlId{5329}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1953}{\htmlId{5342}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{5360}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Enact.html#3775}{\htmlId{5361}{\htmlClass{Generalizable}{\text{dh}}}}\, , \,\href{Ledger.Conway.Specification.Enact.html#3790}{\htmlId{5366}{\htmlClass{Generalizable}{\text{sh}}}}\,\,\htmlId{5368}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ,ENACT⦈ record s { constitution = (dh , sh) , gid } Enact-HF : ─────────────────────────────────────── $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#3864}{\htmlId{5490}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3849}{\htmlId{5496}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3884}{\htmlId{5500}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1991}{\htmlId{5513}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3814}{\htmlId{5531}{\htmlClass{Generalizable}{\text{v}}}}\, \end{pmatrix}$ ,ENACT⦈ record s { pv = v , gid } Enact-PParams : ─────────────────────────────────────── $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#3864}{\htmlId{5640}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3849}{\htmlId{5646}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3884}{\htmlId{5650}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2029}{\htmlId{5663}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3698}{\htmlId{5679}{\htmlClass{Generalizable}{\text{up}}}}\, \end{pmatrix}$ ,ENACT⦈ record s { pparams = applyUpdate (PParamsOf s) up , gid } Enact-Wdrl : let newWdrls = s .withdrawals ∪⁺ wdrl in ∑[ x ← newWdrls ] x ≤ t ─────────────────────────────────────── $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#3864}{\htmlId{5893}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3849}{\htmlId{5899}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3884}{\htmlId{5903}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2067}{\htmlId{5916}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3828}{\htmlId{5937}{\htmlClass{Generalizable}{\text{wdrl}}}}\, \end{pmatrix}$ ,ENACT⦈ record s { withdrawals = newWdrls } Enact-Info : ─────────────────────────────────────── $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#3864}{\htmlId{6056}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3849}{\htmlId{6062}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3884}{\htmlId{6066}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2105}{\htmlId{6079}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\htmlId{6086}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ ,ENACT⦈ s