{-# OPTIONS --safe #-} open import Ledger.Conway.Specification.Gov.Base module Ledger.Conway.Specification.Enact.Properties (gs : _) (open GovStructure gs) where open import Ledger.Prelude open import Ledger.Conway.Specification.Gov.Actions gs hiding (yes; no) open import Ledger.Conway.Specification.Enact gs open EnactState open Computational ⦃...⦄ instance Computational-ENACT : Computational _⊢_⇀⦇_,ENACT⦈_ String Computational-ENACT .computeProof Γᵉ s = let open EnactEnv Γᵉ renaming (treasury to t; epoch to e) in λ where $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#809}{\htmlId{554}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\htmlId{576}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ → success (_ , Enact-NoConf) $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#847}{\htmlId{631}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{653}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Enact.Properties.html#654}{\htmlId{654}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Conway.Specification.Enact.Properties.html#660}{\htmlId{660}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Conway.Specification.Enact.Properties.html#666}{\htmlId{666}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{667}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ → case ¿ ∀[ term ∈ range new ] term ≤ CCMaxTermLengthOf s +ᵉ' e ¿ of λ where (yes p) → success (-, Enact-UpdComm (subst (λ x → ∀[ term ∈ range new ] term ≤ x) (sym +ᵉ≡+ᵉ') p)) (no ¬p) → failure "ENACT failed at ∀[ term ∈ range new ] term ≤ (CCMaxTermLengthOf s +ᵉ e)" $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#885}{\htmlId{988}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{1010}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ → success (-, Enact-NewConst) $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#923}{\htmlId{1066}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\htmlId{1088}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ → success (-, Enact-HF) $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#961}{\htmlId{1138}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\htmlId{1160}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ → success (-, Enact-PParams) $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1037}{\htmlId{1215}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\htmlId{1237}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ → success (-, Enact-Info) $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#999}{\htmlId{1289}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.Properties.html#1311}{\htmlId{1311}{\htmlClass{Bound}{\text{wdrl}}}}\, \end{pmatrix}$ → case ¿ ∑[ x ← s .withdrawals ∪⁺ wdrl ] x ≤ t ¿ of λ where (yes p) → success (-, Enact-Wdrl p) (no _) → failure "ENACT failed at ∑[ x ← (s .withdrawals ∪⁺ wdrl) ᶠᵐ ] x ≤ t" Computational-ENACT .completeness Γᵉ s action _ p with action | p ... | $\begin{pmatrix} \,\htmlId{1612}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#809}{\htmlId{1613}{\htmlClass{DottedPattern InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\htmlId{1635}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ | Enact-NoConf = refl ... | $\begin{pmatrix} \,\htmlId{1689}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#847}{\htmlId{1690}{\htmlClass{DottedPattern InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{1712}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Enact.Properties.html#1713}{\htmlId{1713}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Conway.Specification.Enact.Properties.html#1719}{\htmlId{1719}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Conway.Specification.Enact.Properties.html#1725}{\htmlId{1725}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{1726}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ | Enact-UpdComm p rewrite dec-yes (¿ ∀[ term ∈ range new ] term ≤ CCMaxTermLengthOf s +ᵉ' EnactEnv.epoch Γᵉ ¿) (subst (λ x → ∀[ term ∈ range new ] term ≤ x) +ᵉ≡+ᵉ' p) .proj₂ = refl ... | $\begin{pmatrix} \,\htmlId{1956}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#885}{\htmlId{1957}{\htmlClass{DottedPattern InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{1979}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ | Enact-NewConst = refl ... | $\begin{pmatrix} \,\htmlId{2033}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#923}{\htmlId{2034}{\htmlClass{DottedPattern InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\htmlId{2056}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ | Enact-HF = refl ... | $\begin{pmatrix} \,\htmlId{2110}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#961}{\htmlId{2111}{\htmlClass{DottedPattern InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\htmlId{2133}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ | Enact-PParams = refl ... | $\begin{pmatrix} \,\htmlId{2187}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#1037}{\htmlId{2188}{\htmlClass{DottedPattern InductiveConstructor}{\text{Info}}}}\, \\ \,\htmlId{2210}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ | Enact-Info = refl ... | $\begin{pmatrix} \,\htmlId{2264}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#999}{\htmlId{2265}{\htmlClass{DottedPattern InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.Properties.html#2287}{\htmlId{2287}{\htmlClass{Bound}{\text{wdrl}}}}\, \end{pmatrix}$ | Enact-Wdrl p rewrite dec-yes (¿ ∑[ x ← s .withdrawals ∪⁺ wdrl ] x ≤ EnactEnv.treasury Γᵉ ¿) p .proj₂ = refl