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{1815}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,        \\ \,\htmlId{1837}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (_ , Enact-NoConf)
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1087}{\htmlId{1892}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\,     \\ \,\htmlId{1914}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#1915}{\htmlId{1915}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#1921}{\htmlId{1921}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#1927}{\htmlId{1927}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{1928}{\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{2249}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\,     \\ \,\htmlId{2271}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (-, Enact-NewConst)
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1163}{\htmlId{2327}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,     \\ \,\htmlId{2349}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (-, Enact-HF)
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1201}{\htmlId{2399}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,       \\ \,\htmlId{2421}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (-, Enact-PParams)
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1277}{\htmlId{2476}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,                \\ \,\htmlId{2498}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ → success (-, Enact-Info)
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1239}{\htmlId{2550}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#2572}{\htmlId{2572}{\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{2874}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1049}{\htmlId{2875}{\htmlClass{DottedPattern InductiveConstructor}{\text{NoConfidence}}}}\,        \\ \,\htmlId{2897}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-NoConf    = refl
  ... | $\begin{pmatrix} \,\htmlId{2952}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1087}{\htmlId{2953}{\htmlClass{DottedPattern InductiveConstructor}{\text{UpdateCommittee}}}}\,     \\ \,\htmlId{2975}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#2976}{\htmlId{2976}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#2982}{\htmlId{2982}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#2988}{\htmlId{2988}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{2989}{\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{3219}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1125}{\htmlId{3220}{\htmlClass{DottedPattern InductiveConstructor}{\text{NewConstitution}}}}\,     \\ \,\htmlId{3242}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-NewConst  = refl
  ... | $\begin{pmatrix} \,\htmlId{3297}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1163}{\htmlId{3298}{\htmlClass{DottedPattern InductiveConstructor}{\text{TriggerHardFork}}}}\,     \\ \,\htmlId{3320}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-HF        = refl
  ... | $\begin{pmatrix} \,\htmlId{3375}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1201}{\htmlId{3376}{\htmlClass{DottedPattern InductiveConstructor}{\text{ChangePParams}}}}\,       \\ \,\htmlId{3398}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-PParams   = refl
  ... | $\begin{pmatrix} \,\htmlId{3453}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1277}{\htmlId{3454}{\htmlClass{DottedPattern InductiveConstructor}{\text{Info}}}}\,                \\ \,\htmlId{3476}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ | Enact-Info      = refl
  ... | $\begin{pmatrix} \,\htmlId{3531}{\htmlClass{DottedPattern Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1239}{\htmlId{3532}{\htmlClass{DottedPattern InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\href{Ledger.Dijkstra.Specification.Enact.Properties.Computational.html#3554}{\htmlId{3554}{\htmlClass{Bound}{\text{wdrl}}}}\,            \end{pmatrix}$ | Enact-Wdrl p
    rewrite dec-yes (¿ ∑[ x ← s .withdrawals ∪⁺ wdrl ] x ≤ EnactEnv.treasury Γᵉ ¿) p .proj₂
    = refl