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#1476}{\htmlId{562}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\htmlId{577}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$                → success (_ , Enact-NoConf)
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1511}{\htmlId{633}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ (\,\href{Ledger.Conway.Specification.Enact.Properties.html#652}{\htmlId{652}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Conway.Specification.Enact.Properties.html#658}{\htmlId{658}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Conway.Specification.Enact.Properties.html#664}{\htmlId{664}{\htmlClass{Bound}{\text{q}}}}\,) \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#1546}{\htmlId{986}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{1004}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ → success (-, Enact-NewConst)
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1581}{\htmlId{1046}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\,       \\ \,\htmlId{1064}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ → success (-, Enact-HF)
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1616}{\htmlId{1100}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,   \\ \,\htmlId{1118}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ → success (-, Enact-PParams)
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1686}{\htmlId{1159}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,            \\ \,\htmlId{1177}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ → success (-, Enact-Info) 
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1651}{\htmlId{1216}{\htmlClass{InductiveConstructor}{\text{TreasuryWdrl}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.Properties.html#1231}{\htmlId{1231}{\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{1543}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#1476}{\htmlId{1544}{\htmlClass{DottedPattern InductiveConstructor}{\text{NoConfidence}}}}\,    \\ \,\htmlId{1562}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-NoConf   = refl
  ... | $\begin{pmatrix} \,\htmlId{1616}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#1511}{\htmlId{1617}{\htmlClass{DottedPattern InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ (\,\href{Ledger.Conway.Specification.Enact.Properties.html#1636}{\htmlId{1636}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Conway.Specification.Enact.Properties.html#1642}{\htmlId{1642}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Conway.Specification.Enact.Properties.html#1648}{\htmlId{1648}{\htmlClass{Bound}{\text{q}}}}\,) \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{1879}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#1546}{\htmlId{1880}{\htmlClass{DottedPattern InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{1898}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ | Enact-NewConst = refl
  ... | $\begin{pmatrix} \,\htmlId{1938}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#1581}{\htmlId{1939}{\htmlClass{DottedPattern InductiveConstructor}{\text{TriggerHF}}}}\,       \\ \,\htmlId{1957}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ | Enact-HF       = refl
  ... | $\begin{pmatrix} \,\htmlId{1997}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#1616}{\htmlId{1998}{\htmlClass{DottedPattern InductiveConstructor}{\text{ChangePParams}}}}\,   \\ \,\htmlId{2016}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ | Enact-PParams  = refl
  ... | $\begin{pmatrix} \,\htmlId{2056}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#1686}{\htmlId{2057}{\htmlClass{DottedPattern InductiveConstructor}{\text{Info}}}}\,            \\ \,\htmlId{2075}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ | Enact-Info     = refl
  ... | $\begin{pmatrix} \,\htmlId{2115}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#1651}{\htmlId{2116}{\htmlClass{DottedPattern InductiveConstructor}{\text{TreasuryWdrl}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.Properties.html#2131}{\htmlId{2131}{\htmlClass{Bound}{\text{wdrl}}}}\, \end{pmatrix}$ | Enact-Wdrl p
    rewrite dec-yes (¿ ∑[ x ← s .withdrawals ∪⁺ wdrl ] x ≤ EnactEnv.treasury Γᵉ ¿) p .proj₂
    = refl