Skip to content

ENACT: Computational

This module proves that the ENACT transition rule is computational.

{-# 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#1049}{\htmlId{1849}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,        \\ \,\htmlId{1871}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (_ , Enact-NoConf)
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1087}{\htmlId{1926}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\,     \\ \,\htmlId{1948}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#1949}{\htmlId{1949}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#1955}{\htmlId{1955}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#1961}{\htmlId{1961}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{1962}{\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#1125}{\htmlId{2283}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\,     \\ \,\htmlId{2305}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (-, Enact-NewConst)
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1163}{\htmlId{2361}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,     \\ \,\htmlId{2383}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (-, Enact-HF)
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1201}{\htmlId{2433}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,       \\ \,\htmlId{2455}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (-, Enact-PParams)
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1277}{\htmlId{2510}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,                \\ \,\htmlId{2532}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (-, Enact-Info)
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1239}{\htmlId{2584}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#2606}{\htmlId{2606}{\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{2908}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1049}{\htmlId{2909}{\htmlClass{DottedPattern InductiveConstructor}{\text{NoConfidence}}}}\,        \\ \,\htmlId{2931}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-NoConf    = refl
  ... | $\begin{pmatrix} \,\htmlId{2986}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1087}{\htmlId{2987}{\htmlClass{DottedPattern InductiveConstructor}{\text{UpdateCommittee}}}}\,     \\ \,\htmlId{3009}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#3010}{\htmlId{3010}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#3016}{\htmlId{3016}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#3022}{\htmlId{3022}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{3023}{\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{3253}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1125}{\htmlId{3254}{\htmlClass{DottedPattern InductiveConstructor}{\text{NewConstitution}}}}\,     \\ \,\htmlId{3276}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-NewConst  = refl
  ... | $\begin{pmatrix} \,\htmlId{3331}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1163}{\htmlId{3332}{\htmlClass{DottedPattern InductiveConstructor}{\text{TriggerHardFork}}}}\,     \\ \,\htmlId{3354}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-HF        = refl
  ... | $\begin{pmatrix} \,\htmlId{3409}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1201}{\htmlId{3410}{\htmlClass{DottedPattern InductiveConstructor}{\text{ChangePParams}}}}\,       \\ \,\htmlId{3432}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-PParams   = refl
  ... | $\begin{pmatrix} \,\htmlId{3487}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1277}{\htmlId{3488}{\htmlClass{DottedPattern InductiveConstructor}{\text{Info}}}}\,                \\ \,\htmlId{3510}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-Info      = refl
  ... | $\begin{pmatrix} \,\htmlId{3565}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1239}{\htmlId{3566}{\htmlClass{DottedPattern InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#3588}{\htmlId{3588}{\htmlClass{Bound}{\text{wdrl}}}}\,            \end{pmatrix}$ | Enact-Wdrl p
    rewrite dec-yes (¿ ∑[ x ← s .withdrawals ∪⁺ wdrl ] x ≤ EnactEnv.treasury Γᵉ ¿) p .proj₂
    = refl