Properties
{-# 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#1877}{\htmlId{660}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\htmlId{682}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ → success (_ , Enact-NoConf)
$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1915}{\htmlId{737}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{759}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Enact.Properties.html#760}{\htmlId{760}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Conway.Specification.Enact.Properties.html#766}{\htmlId{766}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Conway.Specification.Enact.Properties.html#772}{\htmlId{772}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{773}{\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#1953}{\htmlId{1094}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{1116}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ → success (-, Enact-NewConst)
$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1991}{\htmlId{1172}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\htmlId{1194}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ → success (-, Enact-HF)
$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2029}{\htmlId{1244}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\htmlId{1266}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ → success (-, Enact-PParams)
$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2105}{\htmlId{1321}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\htmlId{1343}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ → success (-, Enact-Info)
$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2067}{\htmlId{1395}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.Properties.html#1417}{\htmlId{1417}{\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{1718}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#1877}{\htmlId{1719}{\htmlClass{DottedPattern InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\htmlId{1741}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ | Enact-NoConf = refl
... | $\begin{pmatrix} \,\htmlId{1795}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#1915}{\htmlId{1796}{\htmlClass{DottedPattern InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{1818}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Enact.Properties.html#1819}{\htmlId{1819}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Conway.Specification.Enact.Properties.html#1825}{\htmlId{1825}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Conway.Specification.Enact.Properties.html#1831}{\htmlId{1831}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{1832}{\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{2062}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#1953}{\htmlId{2063}{\htmlClass{DottedPattern InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{2085}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ | Enact-NewConst = refl
... | $\begin{pmatrix} \,\htmlId{2139}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#1991}{\htmlId{2140}{\htmlClass{DottedPattern InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\htmlId{2162}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ | Enact-HF = refl
... | $\begin{pmatrix} \,\htmlId{2216}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#2029}{\htmlId{2217}{\htmlClass{DottedPattern InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\htmlId{2239}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ | Enact-PParams = refl
... | $\begin{pmatrix} \,\htmlId{2293}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#2105}{\htmlId{2294}{\htmlClass{DottedPattern InductiveConstructor}{\text{Info}}}}\, \\ \,\htmlId{2316}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ | Enact-Info = refl
... | $\begin{pmatrix} \,\htmlId{2370}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#2067}{\htmlId{2371}{\htmlClass{DottedPattern InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.Properties.html#2393}{\htmlId{2393}{\htmlClass{Bound}{\text{wdrl}}}}\, \end{pmatrix}$ | Enact-Wdrl p
rewrite dec-yes (¿ ∑[ x ← s .withdrawals ∪⁺ wdrl ] x ≤ EnactEnv.treasury Γᵉ ¿) p .proj₂
= refl