Computational

{-# 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 ⦃...⦄

module _ {Γ : EnactEnv} {eSt : EnactState} {ga : GovAction} where

  -- TODO: Make this follow from computationalness or viceversa
  ENACT-deterministic : ∀ {eSt' eSt''}
                      → Γ ⊢ eSt ⇀⦇ ga ,ENACT⦈ eSt'
                      → Γ ⊢ eSt ⇀⦇ ga ,ENACT⦈ eSt''
                      → eSt' ≡ eSt''
  ENACT-deterministic Enact-NoConf Enact-NoConf = refl
  ENACT-deterministic (Enact-UpdComm _) (Enact-UpdComm _) = refl
  ENACT-deterministic Enact-NewConst Enact-NewConst = refl
  ENACT-deterministic Enact-HF Enact-HF = refl
  ENACT-deterministic Enact-PParams Enact-PParams = refl
  ENACT-deterministic (Enact-Wdrl _) (Enact-Wdrl _) = refl
  ENACT-deterministic Enact-Info Enact-Info = refl

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#2446}{\htmlId{1396}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,        \\ \,\htmlId{1418}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (_ , Enact-NoConf)
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2484}{\htmlId{1473}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\,     \\ \,\htmlId{1495}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Enact.Properties.Computational.html#1496}{\htmlId{1496}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Conway.Specification.Enact.Properties.Computational.html#1502}{\htmlId{1502}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Conway.Specification.Enact.Properties.Computational.html#1508}{\htmlId{1508}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{1509}{\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#2522}{\htmlId{1830}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\,     \\ \,\htmlId{1852}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (-, Enact-NewConst)
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2560}{\htmlId{1908}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,     \\ \,\htmlId{1930}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (-, Enact-HF)
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2598}{\htmlId{1980}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,       \\ \,\htmlId{2002}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (-, Enact-PParams)
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2674}{\htmlId{2057}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,                \\ \,\htmlId{2079}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (-, Enact-Info)
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2636}{\htmlId{2131}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\href{Ledger.Conway.Specification.Enact.Properties.Computational.html#2153}{\htmlId{2153}{\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{2454}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#2446}{\htmlId{2455}{\htmlClass{DottedPattern InductiveConstructor}{\text{NoConfidence}}}}\,        \\ \,\htmlId{2477}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-NoConf   = refl
  ... | $\begin{pmatrix} \,\htmlId{2531}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#2484}{\htmlId{2532}{\htmlClass{DottedPattern InductiveConstructor}{\text{UpdateCommittee}}}}\,     \\ \,\htmlId{2554}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Enact.Properties.Computational.html#2555}{\htmlId{2555}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Conway.Specification.Enact.Properties.Computational.html#2561}{\htmlId{2561}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Conway.Specification.Enact.Properties.Computational.html#2567}{\htmlId{2567}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{2568}{\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{2798}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#2522}{\htmlId{2799}{\htmlClass{DottedPattern InductiveConstructor}{\text{NewConstitution}}}}\,     \\ \,\htmlId{2821}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-NewConst = refl
  ... | $\begin{pmatrix} \,\htmlId{2875}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#2560}{\htmlId{2876}{\htmlClass{DottedPattern InductiveConstructor}{\text{TriggerHardFork}}}}\,     \\ \,\htmlId{2898}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-HF       = refl
  ... | $\begin{pmatrix} \,\htmlId{2952}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#2598}{\htmlId{2953}{\htmlClass{DottedPattern InductiveConstructor}{\text{ChangePParams}}}}\,       \\ \,\htmlId{2975}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-PParams  = refl
  ... | $\begin{pmatrix} \,\htmlId{3029}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#2674}{\htmlId{3030}{\htmlClass{DottedPattern InductiveConstructor}{\text{Info}}}}\,                \\ \,\htmlId{3052}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-Info     = refl
  ... | $\begin{pmatrix} \,\htmlId{3106}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#2636}{\htmlId{3107}{\htmlClass{DottedPattern InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\href{Ledger.Conway.Specification.Enact.Properties.Computational.html#3129}{\htmlId{3129}{\htmlClass{Bound}{\text{wdrl}}}}\,            \end{pmatrix}$ | Enact-Wdrl p
    rewrite dec-yes (¿ ∑[ x ← s .withdrawals ∪⁺ wdrl ] x ≤ EnactEnv.treasury Γᵉ ¿) p .proj₂
    = refl