IntersectMBO · williamdemeo · Nov 18, 2025 · Nov 17, 2025 · Nov 17, 2025
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -4,6 +4,7 @@
 
 ### WIP
 
+- Change `RwdAddr` to `RewardAddress`
 - Do not count pool deposits a second time when reregistering pools
 - Allow reregistration of pools in the POOL transition relation
 - Implement the fPoolParams field of PState as in the Shelley specification

diff --git a/build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Foreign/API.hs b/build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Foreign/API.hs
@@ -6,7 +6,7 @@ module MAlonzo.Code.Ledger.Foreign.API
 import MAlonzo.Code.Ledger.Prelude.Foreign.HSTypes                   as X
   (HSSet(..), HSMap(..), ComputationResult(..), Rational(..))
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Address           as X
-  (Credential(..), BaseAddr(..), BootstrapAddr(..), RwdAddr(..), Addr, HSVKey (..))
+  (Credential(..), BaseAddr(..), BootstrapAddr(..), RewardAddress(..), Addr, HSVKey (..))
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.PParams           as X
   (DrepThresholds(..), PoolThresholds(..), Acnt(..), PParams(..), PParamsUpdate(..))
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Transaction       as X

diff --git a/build-tools/static/latex/macros.sty b/build-tools/static/latex/macros.sty
@@ -351,7 +351,7 @@ Scale=0.80 %% Alternatives: Scale=MatchUppercase, Scale=MatchLowercase
 \newcommand{\RTC}{\AgdaFunction{ReflexiveTransitiveClosure}}
 \newcommand{\RTCI}{\AgdaOperator{\AgdaBound{\AgdaUnderscore{}⊢\AgdaUnderscore{}⇀⟦\AgdaUnderscore{}⟧*\AgdaUnderscore{}}}}
 \newcommand{\RTCB}{\AgdaOperator{\AgdaBound{\AgdaUnderscore{}⊢\AgdaUnderscore{}⇀⟦\AgdaUnderscore{}⟧\AgdaUnderscore{}}}}
-\newcommand{\RwdAddrToCoinMap}{\AgdaRecord{RwdAddr}~\AgdaFunction{⇀}~\AgdaFunction{Coin}}
+\newcommand{\RwdAddrToCoinMap}{\AgdaRecord{RewardAddress}~\AgdaFunction{⇀}~\AgdaFunction{Coin}}
 
 \newcommand{\ScriptHash}{\AgdaFunction{ScriptHash}}
 \newcommand{\ScriptPurpose}{\AgdaDatatype{ScriptPurpose}}

diff --git a/build-tools/static/md/mkdocs/includes/links.md b/build-tools/static/md/mkdocs/includes/links.md
@@ -1,3 +1,4 @@
+[Abstract Type for Parameter Updates]: Ledger.Conway.Specification.PParams.md#sec:abstract-type-for-parameter-updates
 [Agda documentation]: https://agda.readthedocs.io/en/
 [Agda record types]: https://agda.readthedocs.io/en/stable/language/record-types.html
 [Agda Wiki]: https://wiki.portal.chalmers.se/agda/pmwiki.php

diff --git a/src/Ledger/Conway/Conformance/Certs.agda b/src/Ledger/Conway/Conformance/Certs.agda
@@ -15,7 +15,7 @@ open Certs public
   hiding (DState; GState; CertState; HasCast-DState; HasCast-GState; HasCast-CertState;
           _⊢_⇀⦇_,DELEG⦈_; _⊢_⇀⦇_,GOVCERT⦈_;
           _⊢_⇀⦇_,CERT⦈_; _⊢_⇀⦇_,PRE-CERT⦈_; _⊢_⇀⦇_,POST-CERT⦈_; _⊢_⇀⦇_,CERTS⦈_; ⟦_,_,_⟧ᵈ)
-open RwdAddr
+open RewardAddress
 
 record DState : Type where
   constructor ⟦_,_,_,_⟧ᵈ

diff --git a/src/Ledger/Conway/Conformance/Certs/Properties.agda b/src/Ledger/Conway/Conformance/Certs/Properties.agda
@@ -166,14 +166,14 @@ instance
         open GState (CertState.gState cs); open DState (CertState.dState cs)
         refresh = mapPartial (isGovVoterDRep ∘ voter) (fromList votes)
         refreshedDReps  = mapValueRestricted (const (CertEnv.epoch ce + drepActivity)) dreps refresh
-    in case ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs
-              × mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) ⊆ rewards ˢ ¿ of λ where
+    in case ¿ filterˢ isKeyHash (mapˢ RewardAddress.stake (dom wdrls)) ⊆ dom voteDelegs
+              × mapˢ (map₁ RewardAddress.stake) (wdrls ˢ) ⊆ rewards ˢ ¿ of λ where
       (yes p) → success (-, CERT-pre p)
       (no ¬p) → failure (genErrors ¬p)
   Computational-PRE-CERT .completeness ce st _ st' (CERT-pre p)
     rewrite let dState = CertState.dState st; open DState dState in
-      dec-yes ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom (CertEnv.wdrls ce))) ⊆ dom voteDelegs
-                × mapˢ (map₁ RwdAddr.stake) (CertEnv.wdrls ce ˢ) ⊆ rewards ˢ ¿
+      dec-yes ¿ filterˢ isKeyHash (mapˢ RewardAddress.stake (dom (CertEnv.wdrls ce))) ⊆ dom voteDelegs
+                × mapˢ (map₁ RewardAddress.stake) (CertEnv.wdrls ce ˢ) ⊆ rewards ˢ ¿
         p .proj₂ = refl
 
   -- POST-CERT has no premises, so computing always succeeds

diff --git a/src/Ledger/Conway/Conformance/Epoch.agda b/src/Ledger/Conway/Conformance/Epoch.agda
@@ -27,7 +27,7 @@ open import Ledger.Conway.Conformance.Utxo txs abs
 open import Ledger.Conway.Conformance.Certs govStructure
 open import Ledger.Conway.Conformance.Rewards txs abs
 open import Ledger.Conway.Specification.Epoch txs abs
-  using (getStakeCred; getOrphans; mkStakeDistrs; toRwdAddr) public
+  using (getStakeCred; getOrphans; mkStakeDistrs; toRewardAddress) public
 import Ledger.Conway.Specification.Epoch txs abs as EpochSpec
 
 record EpochState : Type where
@@ -158,14 +158,14 @@ data _⊢_⇀⦇_,EPOCH⦈_ : ⊤ → EpochState → Epoch → EpochState → Ty
 
       govSt' = filter (λ x → ¿ proj₁ x ∉ mapˢ proj₁ removed' ¿) govSt
 
-      removedGovActions : ℙ (RwdAddr × DepositPurpose × Coin)
+      removedGovActions : ℙ (RewardAddress × DepositPurpose × Coin)
       removedGovActions =
         flip concatMapˢ removed' λ (gaid , gaSt) →
           mapˢ
             (returnAddr gaSt ,_)
             ((utxoSt .deposits ∣ ❴ GovActionDeposit gaid ❵) ˢ)
 
-      govActionReturns : RwdAddr ⇀ Coin
+      govActionReturns : RewardAddress ⇀ Coin
       govActionReturns =
         aggregate₊ (mapˢ (λ (a , _ , d) → a , d) removedGovActions ᶠˢ)
 
@@ -174,7 +174,7 @@ data _⊢_⇀⦇_,EPOCH⦈_ : ⊤ → EpochState → Epoch → EpochState → Ty
 
       retired    = (pState .retiring) ⁻¹ e
       payout     = govActionReturns ∪⁺ trWithdrawals
-      refunds    = pullbackMap payout toRwdAddr (dom (dState .rewards))
+      refunds    = pullbackMap payout toRewardAddress (dom (dState .rewards))
       unclaimed  = getCoin payout - getCoin refunds
       vDeposits  = gState .deposits
 

diff --git a/src/Ledger/Conway/Foreign/HSLedger/Address.agda b/src/Ledger/Conway/Foreign/HSLedger/Address.agda
@@ -15,8 +15,8 @@ instance
   HsTy-BootstrapAddr = autoHsType BootstrapAddr ⊣ fieldPrefix "boot"
   Conv-BootstrapAddr = autoConvert BootstrapAddr
 
-  HsTy-RwdAddr = autoHsType RwdAddr ⊣ fieldPrefix "rwd"
-  Conv-RwdAddr = autoConvert RwdAddr
+  HsTy-RewardAddress = autoHsType RewardAddress ⊣ fieldPrefix "rwd"
+  Conv-RewardAddress = autoConvert RewardAddress
 
 unquoteDecl = do
   hsTypeAlias Addr
diff --git a/src/Ledger/Conway/Foreign/HSLedger/Certs.agda b/src/Ledger/Conway/Foreign/HSLedger/Certs.agda
@@ -38,7 +38,7 @@ record CertEnv' : Type where
     epoch     : Epoch
     pp        : PParams
     votes     : List GovVote'
-    wdrls     : RwdAddr ⇀ Coin
+    wdrls     : RewardAddress ⇀ Coin
     coldCreds : ℙ Credential
 
 instance

diff --git a/src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda b/src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda
@@ -116,12 +116,12 @@ instance
     ; txscriptfee = λ tt y → 0
     ; serSize     = λ v → 0
     ; indexOfImp  = record
-      { indexOfDCert    = λ _ _ → nothing
-      ; indexOfRwdAddr  = λ _ _ → nothing
-      ; indexOfTxIn     = λ _ _ → nothing
-      ; indexOfPolicyId = λ _ _ → nothing
-      ; indexOfVote     = λ _ _ → nothing
-      ; indexOfProposal = λ _ _ → nothing
+      { indexOfDCert          = λ _ _ → nothing
+      ; indexOfRewardAddress  = λ _ _ → nothing
+      ; indexOfTxIn           = λ _ _ → nothing
+      ; indexOfPolicyId       = λ _ _ → nothing
+      ; indexOfVote           = λ _ _ → nothing
+      ; indexOfProposal       = λ _ _ → nothing
       }
     ; runPLCScript = λ _ _ _ _ → false
     ; scriptSize = λ where 

diff --git a/src/Ledger/Conway/Foreign/HSLedger/Gov.agda b/src/Ledger/Conway/Foreign/HSLedger/Gov.agda
@@ -55,13 +55,13 @@ record GovProposal' : Type where
     prevAction  : GovActionID       -- NeedsHash action
     policy      : Maybe ScriptHash
     deposit     : Coin
-    returnAddr  : RwdAddr
+    returnAddr  : RewardAddress
     anchor      : Anchor
 
 record GovActionState' : Type where
   field
     votes       : GovVotes
-    returnAddr  : RwdAddr
+    returnAddr  : RewardAddress
     expiresIn   : Epoch
     action      : GovAction'
     prevAction  : GovActionID       -- NeedsHash action

diff --git a/src/Ledger/Conway/Foreign/HSLedger/Gov/Actions.agda b/src/Ledger/Conway/Foreign/HSLedger/Gov/Actions.agda
@@ -18,7 +18,7 @@ data GovAction' : Type where
   NewConstitution     : DocHash → Maybe ScriptHash               →  GovAction'
   TriggerHardFork     : ProtVer                                  →  GovAction'
   ChangePParams       : PParamsUpdate                            →  GovAction'
-  TreasuryWithdrawal  : (RwdAddr ⇀ Treasury)                     →  GovAction'
+  TreasuryWithdrawal  : (RewardAddress ⇀ Treasury)               →  GovAction'
   Info                :                                             GovAction'
 
 instance

diff --git a/src/Ledger/Conway/Specification/Abstract.lagda.md b/src/Ledger/Conway/Specification/Abstract.lagda.md
@@ -17,12 +17,12 @@ open import Ledger.Conway.Specification.Script.ScriptPurpose txs
 
 record indexOf : Type where
   field
-    indexOfDCert    : DCert → List DCert → Maybe Ix
-    indexOfRwdAddr  : RwdAddr → Withdrawals → Maybe Ix
-    indexOfTxIn     : TxIn → ℙ TxIn → Maybe Ix
-    indexOfPolicyId : ScriptHash → ℙ ScriptHash → Maybe Ix
-    indexOfVote     : GovVoter → List GovVoter → Maybe Ix
-    indexOfProposal : GovProposal → List GovProposal → Maybe Ix
+    indexOfDCert          : DCert          → List DCert        → Maybe Ix
+    indexOfRewardAddress  : RewardAddress  → Withdrawals       → Maybe Ix
+    indexOfTxIn           : TxIn           → ℙ TxIn            → Maybe Ix
+    indexOfPolicyId       : ScriptHash     → ℙ ScriptHash      → Maybe Ix
+    indexOfVote           : GovVoter       → List GovVoter     → Maybe Ix
+    indexOfProposal       : GovProposal    → List GovProposal  → Maybe Ix
 
 record AbstractFunctions : Type where
   field txscriptfee  : Prices → ExUnits → Coin

diff --git a/src/Ledger/Conway/Specification/Certs.lagda.md b/src/Ledger/Conway/Specification/Certs.lagda.md
@@ -16,7 +16,7 @@ open import Ledger.Prelude.Numeric.UnitInterval
 module Ledger.Conway.Specification.Certs (gs : _) (open GovStructure gs) where
 
 open import Ledger.Conway.Specification.Gov.Actions gs hiding (yes; no)
-open RwdAddr
+open RewardAddress
 open PParams
 ```
 -->

diff --git a/src/Ledger/Conway/Specification/Certs/Properties/Computational.lagda.md b/src/Ledger/Conway/Specification/Certs/Properties/Computational.lagda.md
@@ -150,14 +150,14 @@ instance
         open GState (gState cs); open DState (dState cs)
         refresh = mapPartial (isGovVoterDRep ∘ voter) (fromList votes)
         refreshedDReps  = mapValueRestricted (const (CertEnv.epoch ce + drepActivity)) dreps refresh
-    in case ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs
-              × mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) ⊆ rewards ˢ ¿ of λ where
+    in case ¿ filterˢ isKeyHash (mapˢ RewardAddress.stake (dom wdrls)) ⊆ dom voteDelegs
+              × mapˢ (map₁ RewardAddress.stake) (wdrls ˢ) ⊆ rewards ˢ ¿ of λ where
       (yes p) → success (-, CERT-pre p)
       (no ¬p) → failure (genErrors ¬p)
   Computational-PRE-CERT .completeness ce st _ st' (CERT-pre p)
     rewrite let dState = CertState.dState st; open DState dState in
-      dec-yes ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom (CertEnv.wdrls ce))) ⊆ dom voteDelegs
-                × mapˢ (map₁ RwdAddr.stake) (CertEnv.wdrls ce ˢ) ⊆ rewards ˢ ¿
+      dec-yes ¿ filterˢ isKeyHash (mapˢ RewardAddress.stake (dom (CertEnv.wdrls ce))) ⊆ dom voteDelegs
+                × mapˢ (map₁ RewardAddress.stake) (CertEnv.wdrls ce ˢ) ⊆ rewards ˢ ¿
         p .proj₂ = refl
 
   -- POST-CERT has no premises, so computing always succeeds

diff --git a/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md b/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md
@@ -118,7 +118,7 @@ some `dcert`{.AgdaBound} : `DCert`{.AgdaDatatype}. Then,
 
   injOn : (wdls : Withdrawals)
           → ∀[ a ∈ dom (wdls ˢ) ] NetworkIdOf a ≡ NetworkId
-          → InjectiveOn (dom (wdls ˢ)) RwdAddr.stake
+          → InjectiveOn (dom (wdls ˢ)) RewardAddress.stake
   injOn _ h {record { stake = stakex }} {record { stake = stakey }} x∈ y∈ refl =
     cong (λ u → record { net = u ; stake = stakex }) (trans (h x∈) (sym (h y∈)))
 
@@ -169,8 +169,8 @@ value of the withdrawals in `Γ`{.AgdaBound}.  In other terms,
         open DState (dState cs )
         open DState (dState cs') renaming (rewards to rewards')
         module ≡ᵉ       = IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
-        wdrlsCC         = mapˢ (map₁ RwdAddr.stake) (wdrls ˢ)
-        zeroMap         = constMap (mapˢ RwdAddr.stake (dom wdrls)) 0
+        wdrlsCC         = mapˢ (map₁ RewardAddress.stake) (wdrls ˢ)
+        zeroMap         = constMap (mapˢ RewardAddress.stake (dom wdrls)) 0
         rwds-∪ˡ-decomp  = (rewards ∣ dom wdrlsCC ᶜ) ∪ˡ (rewards ∣ dom wdrlsCC)
       in
         begin

diff --git a/src/Ledger/Conway/Specification/Epoch.lagda.md b/src/Ledger/Conway/Specification/Epoch.lagda.md
@@ -185,8 +185,8 @@ instance
     ( (quote EpochState     , HasCast-EpochState)
     ∷ [ (quote NewEpochState  , HasCast-NewEpochState)])
 
-toRwdAddr : Credential → RwdAddr
-toRwdAddr x = record { net = NetworkId ; stake = x }
+toRewardAddress : Credential → RewardAddress
+toRewardAddress x = record { net = NetworkId ; stake = x }
 
 getStakeCred : TxOut → Maybe Credential
 getStakeCred (a , _ , _ , _) = stakeCred a
@@ -405,7 +405,7 @@ for voting purposes.
 
 <!--
 ```agda
-open RwdAddr using (stake)
+open RewardAddress using (stake)
 opaque
 ```
 -->
@@ -444,7 +444,7 @@ stake to `SPOs`{.AgdaInductiveConstructor}.  This function is used both in the
      where
        open UTxOState utxoSt
 
-       govSt' : ℙ (GovActionID × RwdAddr)
+       govSt' : ℙ (GovActionID × RewardAddress)
        govSt' = mapˢ (map₂ returnAddr) (fromList govSt)
 ```
 
@@ -612,7 +612,7 @@ getOrphans es govSt = proj₁ $ iterate step ([] , govSt) (length govSt)
 record Governance-Update : Type where
   constructor GovernanceUpdate
   field
-    removedGovActions : ℙ (RwdAddr × DepositPurpose × Coin)
+    removedGovActions : ℙ (RewardAddress × DepositPurpose × Coin)
     govSt'            : GovState
 
 module GovernanceUpdate (ls : LState)
@@ -635,7 +635,7 @@ module GovernanceUpdate (ls : LState)
   removed' : ℙ (GovActionID × GovActionState)
   removed' = removed ∪ orphans
 
-  removedGovActions : ℙ (RwdAddr × DepositPurpose × Coin)
+  removedGovActions : ℙ (RewardAddress × DepositPurpose × Coin)
   removedGovActions =
     flip concatMapˢ removed' λ (gaid , gaSt) →
       mapˢ
@@ -707,16 +707,16 @@ module Post-POOLREAPUpdate (es : EnactState)
 -->
 ```agda
   opaque
-    govActionReturns : RwdAddr ⇀ Coin
+    govActionReturns : RewardAddress ⇀ Coin
     govActionReturns =
       aggregate₊ (mapˢ (λ (a , _ , d) → a , d) removedGovActions ᶠˢ)
 
-    payout : RwdAddr ⇀ Coin
+    payout : RewardAddress ⇀ Coin
     payout = govActionReturns ∪⁺ WithdrawalsOf es
 
   opaque
     refunds : Credential ⇀ Coin
-    refunds = pullbackMap payout toRwdAddr (dom (RewardsOf dState'))
+    refunds = pullbackMap payout toRewardAddress (dom (RewardsOf dState'))
 
   dState'' : DState
   dState'' = ⟦ VoteDelegsOf dState' , StakeDelegsOf dState' , RewardsOf dState' ∪⁺ refunds ⟧

diff --git a/src/Ledger/Conway/Specification/Gov.lagda.md b/src/Ledger/Conway/Specification/Gov.lagda.md
@@ -98,7 +98,7 @@ private variable
   vote   : GovVote
   v      : Vote
   d      : Coin
-  addr   : RwdAddr
+  addr   : RewardAddress
   a      : GovAction
   prev   : NeedsHash (gaType a)
   k      : ℕ
@@ -208,7 +208,7 @@ insertGovAction ((gaID₀ , gaSt₀) ∷ gaPrs) (gaID₁ , gaSt₁)
      then (gaID₀ , gaSt₀) ∷ insertGovAction gaPrs (gaID₁ , gaSt₁)
      else (gaID₁ , gaSt₁) ∷ (gaID₀ , gaSt₀) ∷ gaPrs
 
-mkGovStatePair :  Epoch → GovActionID → RwdAddr → (a : GovAction) → NeedsHash (a .gaType)
+mkGovStatePair :  Epoch → GovActionID → RewardAddress → (a : GovAction) → NeedsHash (a .gaType)
                   → GovActionID × GovActionState
 mkGovStatePair e aid addr a prev = (aid , gas)
   where
@@ -220,7 +220,7 @@ mkGovStatePair e aid addr a prev = (aid , gas)
                 ; prevAction = prev
                 }
 
-addAction :  GovState → Epoch → GovActionID → RwdAddr
+addAction :  GovState → Epoch → GovActionID → RewardAddress
              → (a : GovAction) → NeedsHash (a .gaType)
              → GovState
 addAction s e aid addr a prev = insertGovAction s (mkGovStatePair e aid addr a prev)
@@ -410,25 +410,24 @@ maxAllEnactable e = maxsublists⊧P (allEnactable? e)
 
 ## Validity and Wellformedness Predicates {#validity-and-wellformedness-predicates}
 
-This section defines predicates used in the `GOVPropose`{.AgdaInductiveConstructor} case
-of the GOV rule to ensure that a governance action is valid and well-formed.
+This section defines two predicates used in the `GOVPropose`{.AgdaInductiveConstructor} case
+of the GOV rule to ensure that a governance action is valid and well-formed.  To make
+sense of these predicates, one must understand how we represent and construct a
+governance action. This is explained in the
+[Governance Actions Section](Ledger.Conway.Specification.Gov.Actions.md#sec:actions).
 
 ```agda
 actionValid : ℙ Credential → Maybe ScriptHash → Maybe ScriptHash → Epoch → GovAction → Type
-actionValid rewardCreds p ppolicy epoch ⟦ ChangePParams , _ ⟧ᵍᵃ =
-  p ≡ ppolicy
-actionValid rewardCreds p ppolicy epoch ⟦ TreasuryWithdrawal  , x ⟧ᵍᵃ =
-  p ≡ ppolicy × mapˢ RwdAddr.stake (dom x) ⊆ rewardCreds
-actionValid rewardCreds p ppolicy epoch ⟦ UpdateCommittee , (new , rem , q) ⟧ᵍᵃ =
-  p ≡ nothing × (∀[ e ∈ range new ]  epoch < e) × (dom new ∩ rem ≡ᵉ ∅)
-actionValid rewardCreds p ppolicy epoch _ =
-  p ≡ nothing
+actionValid _ p ppolicy _ ⟦ ChangePParams , _ ⟧ᵍᵃ = p ≡ ppolicy
+actionValid rwdCreds p ppolicy _ ⟦ TreasuryWithdrawal , wdrls ⟧ᵍᵃ = p ≡ ppolicy × mapˢ CredentialOf (dom wdrls) ⊆ rwdCreds
+actionValid _ p _ epoch ⟦ UpdateCommittee , (new , rem , q) ⟧ᵍᵃ = p ≡ nothing × (∀[ e ∈ range new ] epoch < e) × dom new ∩ rem ≡ᵉ ∅
+actionValid _ p _ _ _ = p ≡ nothing
 
 actionWellFormed : GovAction → Type
-actionWellFormed ⟦ ChangePParams , x ⟧ᵍᵃ = ppdWellFormed x
-actionWellFormed ⟦ TreasuryWithdrawal  , x ⟧ᵍᵃ =
-  (∀[ a ∈ dom x ] NetworkIdOf a ≡ NetworkId) × (∃[ v ∈ range x ] ¬ (v ≡ 0))
-actionWellFormed _                 = ⊤
+actionWellFormed ⟦ ChangePParams , ppup ⟧ᵍᵃ = ppdWellFormed ppup
+actionWellFormed ⟦ TreasuryWithdrawal , wdrls ⟧ᵍᵃ =  (∀[ a ∈ dom wdrls ] NetworkIdOf a ≡ NetworkId)
+                                                     × ∃[ v ∈ range wdrls ] ¬ (v ≡ 0)
+actionWellFormed _ = ⊤
 ```
 
 +  `actionValid`{.AgdaFunction} ensures that the proposed action is valid
@@ -442,17 +441,20 @@ actionWellFormed _                 = ⊤
        registered;
 
     -  an `UpdateCommittee`{.AgdaInductiveConstructor} action is valid if
-       credentials of proposed candidates have not expired, and the action
+       credentials of proposed candidates have not expired and the action
        does not propose to both add and remove the same candidate.
 
 +  `actionWellFormed`{.AgdaFunction} ensures that the proposed action is
-    well-formed:
+    well-formed; there are two cases:
 
-   -  a `ChangePParams`{.AgdaInductiveConstructor} action must preserves well-formedness of the protocol parameters;
+   -  a `ChangePParams`{.AgdaInductiveConstructor} action is well-formed if the
+      `PParamUpdate`{.AgdaField}, `ppup`{.AgdaBound}, preserves well-formedness of the
+      protocol parameters, as expressed by the `ppdWellFormed`{.AgdaFunction}
+      predicate (see [Abstract Type for Parameter Updates][]).
 
    -  a `TreasuryWithdrawal`{.AgdaInductiveConstructor} action is well-formed if the
-      network ID is correct and there is at least one non-zero withdrawal amount in
-      the given `RwdAddrToCoinMap`{.AgdaRecord} map.
+      network ID is correct and the `Withdrawals`{.AgdaDatatype} map,
+      `wdrls`{.AgdaBound}, includes at least one non-zero withdrawal amount.
 
 
 <!--