Enactment

{-# OPTIONS --safe #-}

open import Data.Nat.Properties using (+-0-monoid)
open import Data.Rational using (ℚ)

open import Ledger.Prelude
open import Ledger.Dijkstra.Specification.Gov.Base
open import Ledger.Core.Specification.ProtocolVersion

module Ledger.Dijkstra.Specification.Enact (gs : _) (open GovStructure gs) where

open import Ledger.Dijkstra.Specification.Gov.Actions gs

Auxiliary Types and Functions

record EnactEnv : Type where
  field
    gid       : GovActionID
    treasury  : Treasury
    epoch     : Epoch

-- EnactState is modified only by enacting governance action
-- All fields contain a GovActionID since they are hash-protected.
record EnactState : Type where
  field
    cc            : HashProtected (Maybe ((Credential ⇀ Epoch) × ℚ))
    constitution  : HashProtected (DocHash × Maybe ScriptHash)
    pv            : HashProtected ProtVer
    pparams       : HashProtected PParams
    withdrawals   : Withdrawals

record HasEnactState {a} (A : Type a) : Type a where
  field EnactStateOf : A → EnactState
open HasEnactState ⦃...⦄ public

instance
  HasPParams-EnactState : HasPParams EnactState
  HasPParams-EnactState .PParamsOf = proj₁ ∘ EnactState.pparams

  HasccMaxTermLength-EnactState : HasCCMaxTermLength EnactState
  HasccMaxTermLength-EnactState .CCMaxTermLengthOf = PParams.ccMaxTermLength ∘ PParamsOf

  HasWithdrawals-EnactState : HasWithdrawals EnactState
  HasWithdrawals-EnactState .WithdrawalsOf = EnactState.withdrawals

  unquoteDecl HasCast-EnactEnv = derive-HasCast
    [ (quote EnactEnv , HasCast-EnactEnv) ]

open EnactState

ccCreds : HashProtected (Maybe ((Credential ⇀ Epoch) × ℚ)) → ℙ Credential
ccCreds (just x   , _)  = dom (x .proj₁)
ccCreds (nothing  , _)  = ∅

getHash : ∀ {a} → NeedsHash a → Maybe GovActionID
getHash {NoConfidence}        h = just h
getHash {UpdateCommittee}     h = just h
getHash {NewConstitution}     h = just h
getHash {TriggerHardFork}     h = just h
getHash {ChangePParams}       h = just h
getHash {TreasuryWithdrawal}  _ = nothing
getHash {Info}                _ = nothing

getHashES : EnactState → GovActionType → Maybe GovActionID
getHashES es NoConfidence          = just (es .cc .proj₂)
getHashES es (UpdateCommittee)     = just (es .cc .proj₂)
getHashES es (NewConstitution)     = just (es .constitution .proj₂)
getHashES es (TriggerHardFork)     = just (es .pv .proj₂)
getHashES es (ChangePParams)       = just (es .pparams .proj₂)
getHashES es (TreasuryWithdrawal)  = nothing
getHashES es Info                  = nothing

private variable
  s        : EnactState
  up       : PParamsUpdate
  new      : Credential ⇀ Epoch
  removed  : ℙ Credential
  q        : ℚ
  dHash    : DocHash
  sHash    : Maybe ScriptHash
  protVer  : ProtVer
  wdrls    : Withdrawals
  t        : Treasury
  gid      : GovActionID
  ep       : Epoch

instance
  _ = +-0-monoid

The ENACT Transition System

data _⊢_⇀⦇_,ENACT⦈_ : EnactEnv → EnactState → GovAction → EnactState → Type where

  Enact-NoConf :
    ───────────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Enact.html#2988}{\htmlId{3291}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Enact.html#2966}{\htmlId{3297}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Enact.html#3013}{\htmlId{3301}{\htmlClass{Generalizable}{\text{ep}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1049}{\htmlId{3315}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\htmlId{3330}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ ,ENACT⦈ record s { cc = nothing , gid }

  Enact-UpdComm : let old      = maybe proj₁ ∅ (s .cc .proj₁)
                      maxTerm  = CCMaxTermLengthOf s +ᵉ ep
                  in
    ∀[ term ∈ range new ] term ≤ maxTerm
    ───────────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Enact.html#2988}{\htmlId{3610}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Enact.html#2966}{\htmlId{3616}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Enact.html#3013}{\htmlId{3620}{\htmlClass{Generalizable}{\text{ep}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1087}{\htmlId{3634}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{3652}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Enact.html#2796}{\htmlId{3653}{\htmlClass{Generalizable}{\text{new}}}}\, , \,\href{Ledger.Dijkstra.Specification.Enact.html#2828}{\htmlId{3659}{\htmlClass{Generalizable}{\text{removed}}}}\, , \,\href{Ledger.Dijkstra.Specification.Enact.html#2854}{\htmlId{3669}{\htmlClass{Generalizable}{\text{q}}}}\,\,\htmlId{3670}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ,ENACT⦈
      record s { cc = just ((new ∪ˡ old) ∣ removed ᶜ , q) , gid }

  Enact-NewConst :
    ───────────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Enact.html#2988}{\htmlId{3820}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Enact.html#2966}{\htmlId{3826}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Enact.html#3013}{\htmlId{3830}{\htmlClass{Generalizable}{\text{ep}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1125}{\htmlId{3844}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{3862}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Enact.html#2869}{\htmlId{3863}{\htmlClass{Generalizable}{\text{dHash}}}}\, , \,\href{Ledger.Dijkstra.Specification.Enact.html#2890}{\htmlId{3871}{\htmlClass{Generalizable}{\text{sHash}}}}\,\,\htmlId{3876}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ,ENACT⦈ record s { constitution = (dHash , sHash) , gid }

  Enact-HF :
    ───────────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Enact.html#2988}{\htmlId{4004}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Enact.html#2966}{\htmlId{4010}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Enact.html#3013}{\htmlId{4014}{\htmlClass{Generalizable}{\text{ep}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1163}{\htmlId{4028}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Enact.html#2920}{\htmlId{4046}{\htmlClass{Generalizable}{\text{protVer}}}}\, \end{pmatrix}$ ,ENACT⦈ record s { pv = protVer , gid }

  Enact-PParams :
    ───────────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Enact.html#2988}{\htmlId{4167}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Enact.html#2966}{\htmlId{4173}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Enact.html#3013}{\htmlId{4177}{\htmlClass{Generalizable}{\text{ep}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1201}{\htmlId{4191}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Enact.html#2769}{\htmlId{4207}{\htmlClass{Generalizable}{\text{up}}}}\, \end{pmatrix}$ ,ENACT⦈
      record s { pparams = applyUpdate (PParamsOf s) up , gid }

  Enact-Wdrl : let newWdrls = s .withdrawals ∪⁺ wdrls in
    ∑[ x ← newWdrls ] x ≤ t
    ───────────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Enact.html#2988}{\htmlId{4422}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Enact.html#2966}{\htmlId{4428}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Enact.html#3013}{\htmlId{4432}{\htmlClass{Generalizable}{\text{ep}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1239}{\htmlId{4446}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Enact.html#2941}{\htmlId{4467}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \end{pmatrix}$ ,ENACT⦈ record s { withdrawals = newWdrls }

  Enact-Info :
    ───────────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Enact.html#2988}{\htmlId{4587}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Enact.html#2966}{\htmlId{4593}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Enact.html#3013}{\htmlId{4597}{\htmlClass{Generalizable}{\text{ep}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1277}{\htmlId{4611}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\htmlId{4618}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ ,ENACT⦈ s