Enactment

{-# OPTIONS --safe #-}

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

open import Ledger.Prelude
open import Ledger.Conway.Specification.Gov.Base

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

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

Auxiliary Types and Functions

This section contains some definitions required to define the ENACT transition system. EnactEnv is the environment and EnactState the state of ENACT, which enacts a governance action. All governance actions except TreasuryWithdrawal and Info modify EnactState permanently, which of course can have further consequences. TreasuryWithdrawal accumulates withdrawal temporarily in the withdrawals field of EnactState, but this information is applied and reset in EPOCH (see EPOCH Transition System). Also, enacting these governance actions is the only way of modifying EnactState.

Note that all other fields of EnactState also contain a GovActionID since they are HashProtected.

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

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

Type of the ENACT transition system

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

private variable
  s : EnactState
  up : PParamsUpdate
  new : Credential ⇀ Epoch
  rem : ℙ Credential
  q : ℚ
  dh : DocHash
  sh : Maybe ScriptHash
  v : ProtVer
  wdrl : Withdrawals
  t : Treasury
  gid : GovActionID
  e : Epoch

instance
  _ = +-0-monoid

The ENACT Transition System

This section defines the rules of the ENACT transition system. Usually no preconditions are checked and the state is simply updated (including the GovActionID for the hash protection scheme, if required). The exceptions are UpdateCommittee and TreasuryWithdrawal:

• UpdateCommittee requires that maximum terms are respected, and

• TreasuryWithdrawal requires that the treasury is able to cover the sum of all withdrawals (old and new).

open PParams using (ccMaxTermLength)
open EnactState using (cc)
data _⊢_⇀⦇_,ENACT⦈_ where

  Enact-NoConf :
    ───────────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#3869}{\htmlId{4818}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3854}{\htmlId{4824}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3889}{\htmlId{4828}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2446}{\htmlId{4841}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\htmlId{4856}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ ,ENACT⦈ record s { cc = nothing , gid }

  Enact-UpdComm : let old      = maybe proj₁ ∅ (s .cc .proj₁)
                      maxTerm  = CCMaxTermLengthOf s +ᵉ e
                  in
    ∀[ term ∈ range new ] term ≤ maxTerm
    ───────────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#3869}{\htmlId{5135}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3854}{\htmlId{5141}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3889}{\htmlId{5145}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2484}{\htmlId{5158}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{5176}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Enact.html#3724}{\htmlId{5177}{\htmlClass{Generalizable}{\text{new}}}}\, , \,\href{Ledger.Conway.Specification.Enact.html#3751}{\htmlId{5183}{\htmlClass{Generalizable}{\text{rem}}}}\, , \,\href{Ledger.Conway.Specification.Enact.html#3772}{\htmlId{5189}{\htmlClass{Generalizable}{\text{q}}}}\,\,\htmlId{5190}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ,ENACT⦈
      record s { cc = just ((new ∪ˡ old) ∣ rem ᶜ , q) , gid }

  Enact-NewConst :
    ───────────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#3869}{\htmlId{5336}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3854}{\htmlId{5342}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3889}{\htmlId{5346}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2522}{\htmlId{5359}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{5377}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Enact.html#3780}{\htmlId{5378}{\htmlClass{Generalizable}{\text{dh}}}}\, , \,\href{Ledger.Conway.Specification.Enact.html#3795}{\htmlId{5383}{\htmlClass{Generalizable}{\text{sh}}}}\,\,\htmlId{5385}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ,ENACT⦈ record s { constitution = (dh , sh) , gid }

  Enact-HF :
    ───────────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#3869}{\htmlId{5507}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3854}{\htmlId{5513}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3889}{\htmlId{5517}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2560}{\htmlId{5530}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3819}{\htmlId{5548}{\htmlClass{Generalizable}{\text{v}}}}\, \end{pmatrix}$ ,ENACT⦈ record s { pv = v , gid }

  Enact-PParams :
    ───────────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#3869}{\htmlId{5657}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3854}{\htmlId{5663}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3889}{\htmlId{5667}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2598}{\htmlId{5680}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3703}{\htmlId{5696}{\htmlClass{Generalizable}{\text{up}}}}\, \end{pmatrix}$ ,ENACT⦈
      record s { pparams = applyUpdate (PParamsOf s) up , gid }

  Enact-Wdrl : let newWdrls = s .withdrawals ∪⁺ wdrl in
    ∑[ x ← newWdrls ] x ≤ t
    ───────────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#3869}{\htmlId{5910}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3854}{\htmlId{5916}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3889}{\htmlId{5920}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2636}{\htmlId{5933}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3833}{\htmlId{5954}{\htmlClass{Generalizable}{\text{wdrl}}}}\, \end{pmatrix}$ ,ENACT⦈ record s { withdrawals = newWdrls }

  Enact-Info :
    ───────────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Enact.html#3869}{\htmlId{6073}{\htmlClass{Generalizable}{\text{gid}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3854}{\htmlId{6079}{\htmlClass{Generalizable}{\text{t}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#3889}{\htmlId{6083}{\htmlClass{Generalizable}{\text{e}}}}\, \end{pmatrix}$ ⊢ s ⇀⦇ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2674}{\htmlId{6096}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\htmlId{6103}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ ,ENACT⦈ s