ChangePPGroup

Theorem: PParam updates have non-empty groups at the LEDGER level

{-# OPTIONS --safe #-}

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

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

open import Ledger.Prelude
open import Ledger.Conway.Specification.Gov govStructure
open import Ledger.Conway.Specification.Gov.Properties.ChangePPGroup govStructure
open import Ledger.Conway.Specification.Ledger txs abs
open import Data.List.Membership.Propositional.Properties using (∈-++⁺ˡ; ∈-map⁺)

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

Informally.

This module lifts the GOVS-ChangePPHasGroup property to the LEDGER rule as the following claim:

If p : ``GovProposal is a governance proposal carried by the transaction tx and the action of p is a ChangePParams with parameter update pu : ``PParamsUpdate, then the set updateGroupspu is nonempty.

The transaction must be valid. An invalid transaction takes the LEDGER-I rule, which never runs GOVS, so its proposals are not checked for well-formedness. (They are also not recorded in the governance state.)

Formally.

LEDGER-ChangePPHasGroup :
  {Γ     : LEnv}
  {s s'  : LState}
  {tx    : Tx}
  {p     : GovProposal}
  {pu    : PParamsUpdate}
  → Tx.isValid tx ≡ true
  → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s'
  → p ∈ TxBodyOf tx
  → GovActionOf p ≡ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2652}{\htmlId{1920}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.Properties.ChangePPGroup.html#1802}{\htmlId{1936}{\htmlClass{Bound}{\text{pu}}}}\, \end{pmatrix}$
  → updateGroups pu ≢ ∅

Proof.

The LEDGER-V rule feeds txgov txb = map inj₂ txGovProposals ++ map inj₁ txGovVotes to GOVS, so a proposal of the transaction occurs in that signal list, and GOVS-ChangePPHasGroup applies.

LEDGER-ChangePPHasGroup refl (LEDGER-V⋯ _ _ _ govs) p∈ eq =
  GOVS-ChangePPHasGroup govs
    (∈-++⁺ˡ (∈-map⁺ inj₂ (Equivalence.from ∈-fromList p∈))) eq
LEDGER-ChangePPHasGroup refl (LEDGER-I⋯ () _) _ _