ChangePPGroup

{-# OPTIONS --safe #-}

open import Ledger.Conway.Specification.Abstract
open import Ledger.Conway.Specification.Transaction

module Ledger.Conway.Specification.Gov.Properties.ChangePPGroup
  (txs : _) (open TransactionStructure txs)
  where

open import Ledger.Prelude

instance
  _ : IsSet TxBody GovProposal
  _ = record { toSet = fromList ∘ TxBody.txprop }

Claim (PParam updates have non-empty groups).

Informally.

Let p : GovProposal be a governance proposal and suppose the GovActionType of p .action is ChangePParams. If the data field of p—that is pu = p .action .gaData—is denoted by pu (for "parameter update"), then the set updateGroups pu is nonempty.

Formally.

ChangePPHasGroup : {tx : Tx} {p : GovProposal} (pu : PParamsUpdate)
  → p ∈ Tx.body tx → p .GovProposal.action ≡ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1616}{\htmlId{1049}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Properties.ChangePPGroup.html#982}{\htmlId{1065}{\htmlClass{Bound}{\text{pu}}}}\, \end{pmatrix}$
  → Type
ChangePPHasGroup pu _ _ = updateGroups pu ≢ ∅

Proof. (coming soon)