{-# OPTIONS --safe #-}

open import Ledger.Conway.Specification.Gov.Base

module Ledger.Conway.Specification.Enact.Properties.Computational (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#997}{\htmlId{568}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,        \\ \,\htmlId{590}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (_ , Enact-NoConf)
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1035}{\htmlId{645}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\,     \\ \,\htmlId{667}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Enact.Properties.Computational.html#668}{\htmlId{668}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Conway.Specification.Enact.Properties.Computational.html#674}{\htmlId{674}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Conway.Specification.Enact.Properties.Computational.html#680}{\htmlId{680}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{681}{\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#1073}{\htmlId{1002}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\,     \\ \,\htmlId{1024}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (-, Enact-NewConst)
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1111}{\htmlId{1080}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,     \\ \,\htmlId{1102}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (-, Enact-HF)
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1149}{\htmlId{1152}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,       \\ \,\htmlId{1174}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (-, Enact-PParams)
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1225}{\htmlId{1229}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,                \\ \,\htmlId{1251}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (-, Enact-Info)
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1187}{\htmlId{1303}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\href{Ledger.Conway.Specification.Enact.Properties.Computational.html#1325}{\htmlId{1325}{\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{1626}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#997}{\htmlId{1627}{\htmlClass{DottedPattern InductiveConstructor}{\text{NoConfidence}}}}\,        \\ \,\htmlId{1649}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-NoConf   = refl
  ... | $\begin{pmatrix} \,\htmlId{1703}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#1035}{\htmlId{1704}{\htmlClass{DottedPattern InductiveConstructor}{\text{UpdateCommittee}}}}\,     \\ \,\htmlId{1726}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Enact.Properties.Computational.html#1727}{\htmlId{1727}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Conway.Specification.Enact.Properties.Computational.html#1733}{\htmlId{1733}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Conway.Specification.Enact.Properties.Computational.html#1739}{\htmlId{1739}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{1740}{\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{1970}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#1073}{\htmlId{1971}{\htmlClass{DottedPattern InductiveConstructor}{\text{NewConstitution}}}}\,     \\ \,\htmlId{1993}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-NewConst = refl
  ... | $\begin{pmatrix} \,\htmlId{2047}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#1111}{\htmlId{2048}{\htmlClass{DottedPattern InductiveConstructor}{\text{TriggerHardFork}}}}\,     \\ \,\htmlId{2070}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-HF       = refl
  ... | $\begin{pmatrix} \,\htmlId{2124}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#1149}{\htmlId{2125}{\htmlClass{DottedPattern InductiveConstructor}{\text{ChangePParams}}}}\,       \\ \,\htmlId{2147}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-PParams  = refl
  ... | $\begin{pmatrix} \,\htmlId{2201}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#1225}{\htmlId{2202}{\htmlClass{DottedPattern InductiveConstructor}{\text{Info}}}}\,                \\ \,\htmlId{2224}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-Info     = refl
  ... | $\begin{pmatrix} \,\htmlId{2278}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#1187}{\htmlId{2279}{\htmlClass{DottedPattern InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\href{Ledger.Conway.Specification.Enact.Properties.Computational.html#2301}{\htmlId{2301}{\htmlClass{Bound}{\text{wdrl}}}}\,            \end{pmatrix}$ | Enact-Wdrl p
    rewrite dec-yes (¿ ∑[ x ← s .withdrawals ∪⁺ wdrl ] x ≤ EnactEnv.treasury Γᵉ ¿) p .proj₂
    = refl