[Conway] Property: ChangePParams proposals have a non-empty update group (#1234)

build-tools/static/mkdocs/includes/links.md

@@ -61,9 +61,11 @@
 [Introduction]: Ledger.Introduction.md
 [LEDGER]: Ledger.Conway.Specification.Ledger.md#ledger-transition-system
 [Ledger.Properties]: Ledger.Conway.Specification.Ledger.Properties.md
+[Ledger.Properties.ChangePPGroup]: Ledger.Conway.Specification.Ledger.Properties.ChangePPGroup.md
 [Ledger.Properties.GovDepsMatch]: Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch.md
 [Ledger.Properties.PoV]: Ledger.Conway.Specification.Ledger.Properties.PoV.md
 [LEDGERS]: Ledger.Conway.Specification.Ledger.md#ledgers-transition-system
+[Ledger-ChangePPHasGroup]: Ledger.Conway.Specification.Ledger.Properties.ChangePPGroup.md#thm:LEDGER-ChangePPGroup
 [LEDGER-GovDepsMatch]: Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch.md#lem:LedgerGovDepsMatch
 [Ledger-LastVoteApplied]: Ledger.Conway.Specification.Ledger.Properties.LastVoteApplied.md
 [LEDGER-PoV]: Ledger.Conway.Specification.Ledger.Properties.PoV.md#thm:LEDGER-PoV

build-tools/static/mkdocs/mkdocs.yml

@@ -160,6 +160,7 @@ nav:
       - Properties: Ledger.Conway.Specification.Ledger.Properties.md
       - Properties/:
         - Base: Ledger.Conway.Specification.Ledger.Properties.Base.md
+        - ChangePPGroup: Ledger.Conway.Specification.Ledger.Properties.ChangePPGroup.md
         - Computational: Ledger.Conway.Specification.Ledger.Properties.Computational.md
         - GovDepsMatch: Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch.md
         - PoV: Ledger.Conway.Specification.Ledger.Properties.PoV.md

src/Ledger/Conway/Specification/Gov/Properties/ChangePPGroup.lagda.md

@@ -3,44 +3,114 @@ source_branch: master
 source_path: src/Ledger/Conway/Specification/Gov/Properties/ChangePPGroup.lagda.md
 ---
 
-## Claim: <span class="AgdaRecord">PParam</span> updates have non-empty groups {#clm:ChangePPGroup}
+## Theorem: <span class="AgdaRecord">PParam</span> updates have non-empty groups {#clm:ChangePPGroup}
 
 <!--
 ```agda
 
 {-# OPTIONS --safe #-}
 
-open import Ledger.Conway.Specification.Transaction
+open import Ledger.Conway.Specification.Gov.Base
 
 module Ledger.Conway.Specification.Gov.Properties.ChangePPGroup
-  (txs : _) (open TransactionStructure txs)
+  (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)
 
-instance
-  _ : IsSet TxBody GovProposal
-  _ = record { toSet = fromList ∘ TxBody.txGovProposals }
+private
+  GOVS' = _⊢_⇀⟦_⟧ᵢ*'_ {_⊢_⇀⟦_⟧ᵇ_ = IdSTS} {_⊢_⇀⦇_,GOV⦈_}
 ```
 -->
 
 *Informally*.
 
-Let `p`{.AgdaBound} : `GovProposal`{.AgdaRecord} be a governance proposal and suppose the
-`GovActionType`{.AgdaDatatype} of `p`{.AgdaBound} `.action`{.AgdaField} is `ChangePParams`{.AgdaInductiveConstructor}.
-If the data field of `p`{.AgdaBound}—that is
-`pu`{.AgdaBound} = `p`{.AgdaBound} `.action`{.AgdaField} `.gaData`{.AgdaField}—is
-denoted by `pu`{.AgdaBound} (for "parameter update"), then the set
-`updateGroups`{.AgdaField} `pu`{.AgdaBound} is nonempty.
-
+Let `p : ``GovProposal`{.AgdaRecord} be a governance proposal whose
+`action`{.AgdaField} is a `ChangePParams`{.AgdaInductiveConstructor} action carrying
+the parameter update `pu : ``PParamsUpdate`{.AgdaField}.  If the `GOV`{.AgdaDatatype}
+rule accepts `p`, then the set `updateGroups`{.AgdaField}` pu` is nonempty.[^1]
 
 *Formally*.
 
 ```agda
-ChangePPHasGroup : {tx : Tx} {p : GovProposal} (pu : PParamsUpdate)
-  → p ∈ Tx.body tx → p .GovProposal.action ≡ ⟦ ChangePParams , pu ⟧ᵍᵃ
-  → Type
-ChangePPHasGroup pu _ _ = updateGroups pu ≢ ∅
+ChangePPHasGroup :
+  {Γ     : GovEnv}
+  {k     : ℕ}
+  {s s'  : GovState}
+  {p     : GovProposal}
+  {pu    : PParamsUpdate}
+  → (Γ , k) ⊢ s ⇀⦇ inj₂ p ,GOV⦈ s'
+  → GovActionOf p ≡ ⟦ ChangePParams , pu ⟧ᵍᵃ
+  → updateGroups pu ≢ ∅
+```
+
+*Proof*.
+
+A proposal signal can only be consumed by `GOV-Propose`{.AgdaInductiveConstructor},
+whose first premise is `actionWellFormed`{.AgdaFunction}` a` for the proposed action
+`a`.  Substituting the hypothesis `a ≡ ⟦ ChangePParams , pu ⟧ᵍᵃ` makes that
+premise reduce to `ppdWellFormed`{.AgdaFunction}` pu`, whose first component is the
+claim.
+
+```agda
+ChangePPHasGroup (GOV-Propose (awf , _)) eq = subst actionWellFormed eq awf .proj₁
+```
+
+### Lifting to <span class="AgdaFunction">GOVS</span>
+
+The same holds for every proposal in a list of signals accepted by
+`GOVS`{.AgdaFunction}, the reflexive transitive closure of `GOV`{.AgdaDatatype} that
+processes the governance signals of a single transaction.
+
+The lift is an induction on the derivation: the step that consumes
+`inj₂`{.AgdaInductiveConstructor}` p` is a `GOV`{.AgdaDatatype} step, to which the
+previous result applies, and every other step is handled by the induction hypothesis.
+The induction runs over `GOVS'`{.AgdaFunction}, the general indexed closure
+`_⊢_⇀⟦_⟧ᵢ*'_`{.AgdaDatatype} of `GOV`{.AgdaDatatype}, since the index advances along
+the trace.
+
+```agda
+ChangePPHasGroupᵢ :
+  {Γ     : GovEnv}
+  {k     : ℕ}
+  {s s'  : GovState}
+  {sigs  : List (GovVote ⊎ GovProposal)}
+  {p     : GovProposal}
+  {pu    : PParamsUpdate}
+  → GOVS' (Γ , k) s sigs s'
+  → inj₂ p ∈ˡ sigs
+  → GovActionOf p ≡ ⟦ ChangePParams , pu ⟧ᵍᵃ
+  → 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
 ```
 
-*Proof*. (coming soon)
+`GOVS`{.AgdaFunction} is that closure at index `0`, so the statement for
+`GOVS`{.AgdaFunction} is an instance of the above.
+
+```agda
+GOVS-ChangePPHasGroup :
+  {Γ     : GovEnv}
+  {s s'  : GovState}
+  {sigs  : List (GovVote ⊎ GovProposal)}
+  {p     : GovProposal}
+  {pu    : PParamsUpdate}
+  → Γ ⊢ s ⇀⦇ sigs ,GOVS⦈ s'
+  → inj₂ p ∈ˡ sigs
+  → GovActionOf p ≡ ⟦ ChangePParams , pu ⟧ᵍᵃ
+  → updateGroups pu ≢ ∅
+GOVS-ChangePPHasGroup = ChangePPHasGroupᵢ
+```
+
+---
+
+[^1]: The `GOV`{.AgdaDatatype} 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`{.AgdaFunction} of the `GOV-Propose`{.AgdaInductiveConstructor}
+      rule.  So the property is about proposals the ledger *accepts*, not proposals a
+      transaction merely mentions.

src/Ledger/Conway/Specification/Ledger/Properties.lagda.md

@@ -9,6 +9,7 @@ source_path: src/Ledger/Conway/Specification/Ledger/Properties.lagda.md
 module Ledger.Conway.Specification.Ledger.Properties where
 
 open import Ledger.Conway.Specification.Ledger.Properties.Base
+open import Ledger.Conway.Specification.Ledger.Properties.ChangePPGroup
 open import Ledger.Conway.Specification.Ledger.Properties.Computational
 open import Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch
 open import Ledger.Conway.Specification.Ledger.Properties.LastVoteApplied

src/Ledger/Conway/Specification/Ledger/Properties/ChangePPGroup.lagda.md

@@ -0,0 +1,76 @@
+---
+source_branch: master
+source_path: src/Ledger/Conway/Specification/Ledger/Properties/ChangePPGroup.lagda.md
+---
+
+## Theorem: <span class="AgdaRecord">PParam</span> updates have non-empty groups at the LEDGER level {#thm:LEDGER-ChangePPGroup}
+
+<!--
+```agda
+{-# 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`{.AgdaFunction} property to the
+`LEDGER`{.AgdaDatatype} rule as the following claim:
+
+If `p : ``GovProposal`{.AgdaRecord} is a governance proposal carried by the
+transaction `tx` and the `action`{.AgdaField} of `p` is a
+`ChangePParams`{.AgdaInductiveConstructor} with parameter update
+`pu : ``PParamsUpdate`{.AgdaField}, then the set `updateGroups`{.AgdaField}` pu` is
+nonempty.
+
+The transaction must be valid.  An invalid transaction takes the
+`LEDGER-I`{.AgdaInductiveConstructor} rule, which never runs `GOVS`{.AgdaFunction},
+so its proposals are not checked for well-formedness.  (They are also not recorded in
+the governance state.)
+
+*Formally*.
+
+```agda
+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 ≡ ⟦ ChangePParams , pu ⟧ᵍᵃ
+  → updateGroups pu ≢ ∅
+```
+
+*Proof*.
+
+The `LEDGER-V`{.AgdaInductiveConstructor} rule feeds `txgov`{.AgdaFunction}
+`txb = map inj₂ txGovProposals ++ map inj₁ txGovVotes` to
+`GOVS`{.AgdaFunction}, so a proposal of the transaction occurs in that signal list,
+and `GOVS-ChangePPHasGroup`{.AgdaFunction} applies.
+
+```agda
+LEDGER-ChangePPHasGroup refl (LEDGER-V⋯ _ _ _ govs) p∈ eq =
+  GOVS-ChangePPHasGroup govs
+    (∈-++⁺ˡ (∈-map⁺ inj₂ (Equivalence.from ∈-fromList p∈))) eq
+LEDGER-ChangePPHasGroup refl (LEDGER-I⋯ () _) _ _
+```

src/Ledger/Conway/Specification/Properties.lagda.md

@@ -109,13 +109,16 @@ proposals in `tx`{.AgdaBound}.
 
 ### Other Miscellaneous Properties
 
-+  **Claim** [Gov-ChangePPHasGroup][]. PParam updates have non-empty groups.
++  **Theorem** [Gov-ChangePPHasGroup][] and [Ledger-ChangePPHasGroup][].
+   PParam updates have non-empty groups.
 
    Let `p`{.AgdaBound} : `GovProposal`{.AgdaRecord} be a governance proposal and
    suppose the `GovActionType`{.AgdaDatatype} of `p`{.AgdaBound}
    `.action`{.AgdaField} is `ChangePParams`{.AgdaInductiveConstructor}.  Moreover,
-   suppose `pu`{.AgdaBound} is the data field of `p`{.AgdaBound}. Then the
-   set `updateGroups`{.AgdaField} `pu`{.AgdaBound} is nonempty.
+   suppose `pu`{.AgdaBound} is the data field of `p`{.AgdaBound}.  If the
+   `GOV`{.AgdaDatatype} rule accepts `p`{.AgdaBound}, then the set
+   `updateGroups`{.AgdaField} `pu`{.AgdaBound} is nonempty.  The same holds for every
+   proposal of a valid transaction accepted by the `LEDGER`{.AgdaDatatype} rule.
 
 
 +  **Theorem** [Gov-LastVoteApplied][] and [Ledger-LastVoteApplied][].