{-# OPTIONS --safe #-} open import Data.Nat.Properties using (+-0-monoid) open import Data.Rational using (ℚ) open import Ledger.Prelude open import Ledger.Conway.Specification.Gov.Base module Ledger.Conway.Specification.Enact (gs : _) (open GovStructure gs) where open import Ledger.Conway.Specification.Gov.Actions gs 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 record HasEnactState {a} (A : Type a) : Type a where field EnactStateOf : A → EnactState open HasEnactState ⦃...⦄ public instance HasPParams-EnactState : HasPParams EnactState HasPParams-EnactState .PParamsOf = proj₁ ∘ EnactState.pparams HasccMaxTermLength-EnactState : HasCCMaxTermLength EnactState HasccMaxTermLength-EnactState .CCMaxTermLengthOf = PParams.ccMaxTermLength ∘ PParamsOf HasWithdrawals-EnactState : HasWithdrawals EnactState HasWithdrawals-EnactState .WithdrawalsOf = EnactState.withdrawals unquoteDecl HasCast-EnactEnv = derive-HasCast [ (quote EnactEnv , HasCast-EnactEnv) ] open EnactState 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 data _⊢_⇀⦇_,ENACT⦈_ : EnactEnv → EnactState → GovAction → EnactState → Type private variable s : EnactState up : PParamsUpdate new : Credential ⇀ Epoch rem : ℙ Credential q : ℚ dh : DocHash sh : Maybe ScriptHash v : ProtVer wdrl : Withdrawals t : Treasury gid : GovActionID e : Epoch instance _ = +-0-monoid open PParams using (ccMaxTermLength) open EnactState using (cc) data _⊢_⇀⦇_,ENACT⦈_ where Enact-NoConf : ─────────────────────────────────────── $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#2586}{\htmlId{2804}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2571}{\htmlId{2810}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2606}{\htmlId{2814}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#997}{\htmlId{2827}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\htmlId{2842}{\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#2586}{\htmlId{3121}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2571}{\htmlId{3127}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2606}{\htmlId{3131}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1035}{\htmlId{3144}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{3162}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Enact.html#2441}{\htmlId{3163}{\htmlClass{Generalizable}{\text{new}}}}\, , \,\href{Ledger.Conway.Specification.Enact.html#2468}{\htmlId{3169}{\htmlClass{Generalizable}{\text{rem}}}}\, , \,\href{Ledger.Conway.Specification.Enact.html#2489}{\htmlId{3175}{\htmlClass{Generalizable}{\text{q}}}}\,\,\htmlId{3176}{\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#2586}{\htmlId{3322}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2571}{\htmlId{3328}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2606}{\htmlId{3332}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1073}{\htmlId{3345}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{3363}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Enact.html#2497}{\htmlId{3364}{\htmlClass{Generalizable}{\text{dh}}}}\, , \,\href{Ledger.Conway.Specification.Enact.html#2512}{\htmlId{3369}{\htmlClass{Generalizable}{\text{sh}}}}\,\,\htmlId{3371}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ,ENACT⦈ record s { constitution = (dh , sh) , gid } Enact-HF : ─────────────────────────────────────── $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#2586}{\htmlId{3493}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2571}{\htmlId{3499}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2606}{\htmlId{3503}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1111}{\htmlId{3516}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2536}{\htmlId{3534}{\htmlClass{Generalizable}{\text{v}}}}\, \end{pmatrix}$ ,ENACT⦈ record s { pv = v , gid } Enact-PParams : ─────────────────────────────────────── $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#2586}{\htmlId{3643}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2571}{\htmlId{3649}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2606}{\htmlId{3653}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1149}{\htmlId{3666}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2420}{\htmlId{3682}{\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#2586}{\htmlId{3896}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2571}{\htmlId{3902}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2606}{\htmlId{3906}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1187}{\htmlId{3919}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2550}{\htmlId{3940}{\htmlClass{Generalizable}{\text{wdrl}}}}\, \end{pmatrix}$ ,ENACT⦈ record s { withdrawals = newWdrls } Enact-Info : ─────────────────────────────────────── $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#2586}{\htmlId{4059}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2571}{\htmlId{4065}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2606}{\htmlId{4069}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1225}{\htmlId{4082}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\htmlId{4089}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ ,ENACT⦈ s