{-# OPTIONS --safe #-}
open import Ledger.Dijkstra.Specification.Gov.Base
module Ledger.Dijkstra.Specification.Enact.Properties.Computational
  (gs : _) (open GovStructure gs) where

open import Ledger.Prelude
open import Ledger.Dijkstra.Specification.Gov.Actions gs hiding (yes; no)
open import Ledger.Dijkstra.Specification.Enact gs
open EnactState
open Computational ⦃...⦄

-- NOTE: The Dijkstra ENACT transition system has the same constructors as Conway
--       (Enact-NoConf, Enact-UpdComm, Enact-NewConst, Enact-HF, Enact-PParams,
--       Enact-Wdrl, Enact-Info).  This is a straight port of the Conway instance to
--       Dijkstra module paths.

module _ {Γ : EnactEnv} {eSt : EnactState} {ga : GovAction} where
  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.Dijkstra.Specification.Gov.Actions.html#625}{\htmlId{1533}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,        \\ \,\htmlId{1555}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (_ , Enact-NoConf)
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#663}{\htmlId{1610}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\,     \\ \,\htmlId{1632}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#1633}{\htmlId{1633}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#1639}{\htmlId{1639}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#1645}{\htmlId{1645}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{1646}{\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.Dijkstra.Specification.Gov.Actions.html#701}{\htmlId{1967}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\,     \\ \,\htmlId{1989}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (-, Enact-NewConst)
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#739}{\htmlId{2045}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,     \\ \,\htmlId{2067}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (-, Enact-HF)
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#777}{\htmlId{2117}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,       \\ \,\htmlId{2139}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (-, Enact-PParams)
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#853}{\htmlId{2194}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,                \\ \,\htmlId{2216}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (-, Enact-Info)
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#815}{\htmlId{2268}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#2290}{\htmlId{2290}{\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{2592}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#625}{\htmlId{2593}{\htmlClass{DottedPattern InductiveConstructor}{\text{NoConfidence}}}}\,        \\ \,\htmlId{2615}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-NoConf    = refl
  ... | $\begin{pmatrix} \,\htmlId{2670}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#663}{\htmlId{2671}{\htmlClass{DottedPattern InductiveConstructor}{\text{UpdateCommittee}}}}\,     \\ \,\htmlId{2693}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#2694}{\htmlId{2694}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#2700}{\htmlId{2700}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#2706}{\htmlId{2706}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{2707}{\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{2937}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#701}{\htmlId{2938}{\htmlClass{DottedPattern InductiveConstructor}{\text{NewConstitution}}}}\,     \\ \,\htmlId{2960}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-NewConst  = refl
  ... | $\begin{pmatrix} \,\htmlId{3015}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#739}{\htmlId{3016}{\htmlClass{DottedPattern InductiveConstructor}{\text{TriggerHardFork}}}}\,     \\ \,\htmlId{3038}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-HF        = refl
  ... | $\begin{pmatrix} \,\htmlId{3093}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#777}{\htmlId{3094}{\htmlClass{DottedPattern InductiveConstructor}{\text{ChangePParams}}}}\,       \\ \,\htmlId{3116}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-PParams   = refl
  ... | $\begin{pmatrix} \,\htmlId{3171}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#853}{\htmlId{3172}{\htmlClass{DottedPattern InductiveConstructor}{\text{Info}}}}\,                \\ \,\htmlId{3194}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-Info      = refl
  ... | $\begin{pmatrix} \,\htmlId{3249}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#815}{\htmlId{3250}{\htmlClass{DottedPattern InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#3272}{\htmlId{3272}{\htmlClass{Bound}{\text{wdrl}}}}\,            \end{pmatrix}$ | Enact-Wdrl p
    rewrite dec-yes (¿ ∑[ x ← s .withdrawals ∪⁺ wdrl ] x ≤ EnactEnv.treasury Γᵉ ¿) p .proj₂
    = refl