Skip to content

ChangePPGroup

Theorem: PParam updates have non-empty groups

{-# OPTIONS --safe #-}

open import Ledger.Conway.Specification.Gov.Base

module Ledger.Conway.Specification.Gov.Properties.ChangePPGroup
  (gs : GovStructure) (open GovStructure gs)
  where

open import Ledger.Prelude
open import Ledger.Conway.Specification.Gov.Actions gs hiding (yes; no)
open import Ledger.Conway.Specification.Gov gs
open import Data.List.Relation.Unary.Any using (here; there)

private
  GOVS' = _⊢_⇀⟦_⟧ᵢ*'_ {_⊢_⇀⟦_⟧ᵇ_ = IdSTS} {_⊢_⇀⦇_,GOV⦈_}

Informally.

Let p : ``GovProposal be a governance proposal whose action is a ChangePParams action carrying the parameter update pu : ``PParamsUpdate. If the GOV rule accepts p, then the set updateGroupspu is nonempty.1

Formally.

ChangePPHasGroup :
  {Γ     : GovEnv}
  {k     : ℕ}
  {s s'  : GovState}
  {p     : GovProposal}
  {pu    : PParamsUpdate}
  → (Γ , k) ⊢ s ⇀⦇ inj₂ p ,GOV⦈ s'
  → GovActionOf p ≡ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2652}{\htmlId{1242}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Properties.ChangePPGroup.html#1162}{\htmlId{1258}{\htmlClass{Bound}{\text{pu}}}}\, \end{pmatrix}$
  → updateGroups pu ≢ ∅

Proof.

A proposal signal can only be consumed by GOV-Propose, whose first premise is actionWellFormeda for the proposed action a. Substituting the hypothesis a ≡ ⟦ ChangePParams , pu ⟧ᵍᵃ makes that premise reduce to ppdWellFormedpu, whose first component is the claim.

ChangePPHasGroup (GOV-Propose (awf , _)) eq = subst actionWellFormed eq awf .proj₁

Lifting to GOVS

The same holds for every proposal in a list of signals accepted by GOVS, the reflexive transitive closure of GOV that processes the governance signals of a single transaction.

The lift is an induction on the derivation: the step that consumes inj₂p is a GOV step, to which the previous result applies, and every other step is handled by the induction hypothesis. The induction runs over GOVS', the general indexed closure _⊢_⇀⟦_⟧ᵢ*'_ of GOV, since the index advances along the trace.

ChangePPHasGroupᵢ :
  {Γ     : GovEnv}
  {k     : ℕ}
  {s s'  : GovState}
  {sigs  : List (GovVote ⊎ GovProposal)}
  {p     : GovProposal}
  {pu    : PParamsUpdate}
  → GOVS' (Γ , k) s sigs s'
  → inj₂ p ∈ˡ sigs
  → GovActionOf p ≡ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2652}{\htmlId{2654}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Properties.ChangePPGroup.html#2562}{\htmlId{2670}{\htmlClass{Bound}{\text{pu}}}}\, \end{pmatrix}$
  → updateGroups pu ≢ ∅
ChangePPHasGroupᵢ (BS-base _) ()
ChangePPHasGroupᵢ (BS-ind st _) (here refl) eq = ChangePPHasGroup st eq
ChangePPHasGroupᵢ (BS-ind _ rest) (there mem) eq = ChangePPHasGroupᵢ rest mem eq

GOVS is that closure at index 0, so the statement for GOVS is an instance of the above.

GOVS-ChangePPHasGroup :
  {Γ     : GovEnv}
  {s s'  : GovState}
  {sigs  : List (GovVote ⊎ GovProposal)}
  {p     : GovProposal}
  {pu    : PParamsUpdate}
  → Γ ⊢ s ⇀⦇ sigs ,GOVS⦈ s'
  → inj₂ p ∈ˡ sigs
  → GovActionOf p ≡ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2652}{\htmlId{3249}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Properties.ChangePPGroup.html#3157}{\htmlId{3265}{\htmlClass{Bound}{\text{pu}}}}\, \end{pmatrix}$
  → updateGroups pu ≢ ∅
GOVS-ChangePPHasGroup = ChangePPHasGroupᵢ

  1. The GOV premise cannot be dropped. Nothing stops a transaction body from listing a degenerate proposal whose update touches no parameter group; what rules such a proposal out is the premise actionWellFormed of the GOV-Propose rule. So the property is about proposals the ledger accepts, not proposals a transaction merely mentions. ↩