Restate #1233 as a CERTS invariant after the removal of POST-CERT

Master removed the POST-CERT rule; delegated voting stake is now dropped by
GOVCERT at the moment a DRep is deregistered.  POST-CERT used to corestrict
voteDelegs to the active VDelegs at the end of every batch, which is what made
the property an unconditional postcondition of CERTS and its proof a one-liner.
That sweep is gone, so an arbitrary input state may already violate the
containment and nothing in a CERTS step would repair it.

Restate the property as a genuine CERTS invariant and prove it:

    CERTS-voteDelegsVDeleg : LedgerInvariant _|-_->(_,CERTS)_ voteDelegsVDeleg

The containment is now maintained incrementally by the two rules that could
break it.  DELEG-delegate may install only a VDeleg that is already active for
the current delegatees, and GOVCERT-deregdrep, the one rule that shrinks the
registered DReps, deletes every delegation to the credential it deregisters in
the same step.  The remaining rules either leave both fields alone or only grow
the DRep domain, for which activeVDelegs is monotone.

The proof establishes invariance for DELEG, GOVCERT, CERT and PRE-CERT, then
lifts the CERT lemma along RTC-preserves-inv.  In Axiom.Set.Map.Extra, drop
cores-range-|_ (nothing corestricts any more) and add what the new proof needs:
coex-|-in, for reading a pair back out of a complement corestriction, and
dom-cup-l-supset-r with its corollaries dom-insert-supset and
dom-mapValueRestricted-supset, for the two left-biased unions that refresh and
extend the DReps.  Each takes the map whose keys are preserved explicitly, since
it sits under proj1 and unification cannot recover it.

Also restate the prose entry in Conway/Specification/Properties.lagda.md and
restore the changelog line dropped in an earlier rebase.

AI-assisted development: Claude Opus 5 (Anthropic)

Author: williamdemeo

src-lib-exts/abstract-set-theory/Axiom/Set/Map/Extra.agda

@@ -705,14 +705,37 @@ module _  {A B : Type}
 
 -- Corestriction
 
--- Corestricting a map to a set `X` of values confines its range to `X`.
--- Indeed, `(m ∣^ X) ˢ` is `m ˢ` filtered by the predicate `(_∈ X) ∘ proj₂`, so every
--- pair surviving the filter carries a proof that its value belongs to `X`.
+-- Corestricting a map away from a set `X` of values: `(m ∣^ X ᶜ) ˢ` is `m ˢ` filtered
+-- by `(_∉ X) ∘ proj₂`, so every surviving pair is a pair of `m` whose value avoids `X`.
 -- The map `m` is an explicit argument because it cannot be recovered by unification:
--- `_∣^_` goes through `⊆-map`, which mentions `m` only as `m ˢ` (i.e., `proj₁ m`).
-cores-range-⊆ : ∀ {A B : Type} ⦃ _ : DecEq B ⦄ (m : A ⇀ B) {X : ℙ B} → range (m ∣^ X) ⊆ X
-cores-range-⊆ m b∈range with Equivalence.from ∈-map b∈range
-... | _ , refl , ab∈cores = proj₁ (Equivalence.from ∈-filter ab∈cores)
+-- `_∣^_ᶜ` goes through `⊆-map`, which mentions `m` only as `m ˢ` (i.e., `proj₁ m`).
+coex-∈⁻ : {A B : Type} ⦃ _ : DecEq B ⦄ (m : A ⇀ B) {X : ℙ B} {a : A} {b : B}
+  → (a , b) ∈ (m ∣^ X ᶜ) ˢ → b ∉ X × (a , b) ∈ (m ˢ)
+coex-∈⁻ m = from ∈-filter
+
+
+-- A left-biased union never drops a key of its right operand.  A key that `m` also
+-- binds is taken from `m`; a key that `m` does not bind survives the filter that
+-- `_∪ˡ_` applies to `m'`.  Either way the key stays in the domain.
+dom-∪ˡ-⊇ʳ : {A B : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ B) → dom m' ⊆ dom (m ∪ˡ m')
+dom-∪ˡ-⊇ʳ m m' {a} a∈dom' with a ∈? dom m
+... | yes a∈dom =
+  to dom∈  ( from dom∈ a∈dom .proj₁
+           , Properties.∈-∪⁺ (inj₁ (from dom∈ a∈dom .proj₂)))
+... | no a∉dom =
+  to dom∈  ( from dom∈ a∈dom' .proj₁
+           , Properties.∈-∪⁺ (inj₂ (to ∈-filter (a∉dom , from dom∈ a∈dom' .proj₂))))
+
+-- Two consequences, phrased so that the map whose keys are preserved is the explicit
+-- argument: it is the one a caller can name, whereas the overriding map generally is
+-- not (it sits under `proj₁`, so unification cannot recover it from the goal).
+dom-insert-⊇ : {A B : Type} ⦃ _ : DecEq A ⦄ (m : A ⇀ B) {k : A} {v : B}
+  → dom m ⊆ dom (insert m k v)
+dom-insert-⊇ m {k} {v} = dom-∪ˡ-⊇ʳ ❴ k , v ❵ m
+
+dom-mapValueRestricted-⊇ : {A B : Type} ⦃ _ : DecEq A ⦄ (m : A ⇀ B)
+  {f : B → B} {X : ℙ A} → dom m ⊆ dom (mapValueRestricted f m X)
+dom-mapValueRestricted-⊇ m {f} {X} = dom-∪ˡ-⊇ʳ (mapValues f (m ∣ X)) m
 
 
 -- Map lemmas: lookup after insert

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

@@ -12,91 +12,204 @@ source_path: src/Ledger/Conway/Specification/Certs/Properties/VoteDelegsVDeleg.l
 
 open import Ledger.Conway.Specification.Gov.Base
 
-module Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg (gs : _) (open GovStructure gs) where
+module Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg
+  (gs : GovStructure) (open GovStructure gs)
+  where
 
 open import Ledger.Conway.Specification.Certs gs
 open import Ledger.Prelude
 open import Ledger.Conway.Specification.Gov.Actions gs
 
+open import Data.List.Relation.Unary.Any using (here; there)
+
 private variable
-  Γ      : CertEnv
-  s s'   : CertState
-  certs  : List DCert
+  Γ         : CertEnv
+  s s'      : CertState
+  stᵈ stᵈ'  : DState
+  certs     : List DCert
+  dCert     : DCert
+  D D'      : ℙ Credential
+  m         : VoteDelegs
+  v         : VDeleg
 ```
 -->
 
 *Informally*.
 
-A `CertState`{.AgdaRecord} has a `DState`{.AgdaRecord}, a `PState`{.AgdaRecord}, and a
-`GState`{.AgdaRecord}.  The `DState`{.AgdaRecord} contains a field
-`voteDelegs`{.AgdaField}, a map sending the `Credential`{.AgdaDatatype} of a delegator to
-the `VDeleg`{.AgdaDatatype} that receives its voting stake.  The `GState`{.AgdaRecord}
-contains a field `dreps`{.AgdaField} whose domain is the set of registered
-`DReps`{.AgdaFunction}.
+A `CertState`{.AgdaRecord} has a `DState`{.AgdaRecord}, a `PState`{.AgdaRecord},
+and a `GState`{.AgdaRecord}.  The `DState`{.AgdaRecord} contains a field
+`voteDelegs`{.AgdaField}, a map sending the `Credential`{.AgdaDatatype} of a
+delegator to the `VDeleg`{.AgdaDatatype} that receives its voting stake.  The
+`GState`{.AgdaRecord} contains a field `dreps`{.AgdaField} whose domain is the set
+of registered `DReps`{.AgdaFunction}.
 
 `VDeleg`{.AgdaDatatype} has three constructors:
 `vDelegCredential`{.AgdaInductiveConstructor}, which takes the
 `Credential`{.AgdaDatatype} of a `DRep`, and the two constants
 `vDelegAbstain`{.AgdaInductiveConstructor} and
-`vDelegNoConfidence`{.AgdaInductiveConstructor}.
+`vDelegNoConfidence`{.AgdaInductiveConstructor}.  Call a `VDeleg`{.AgdaDatatype}
+*active* for a set of credentials if it is one of those two constants or if it
+wraps a credential from that set.
+
+The property proved here asserts that no `CERTS`{.AgdaDatatype} step introduces a
+vote delegation that is inactive for the registered `DReps`{.AgdaFunction}: if
+every value of `voteDelegs`{.AgdaField} is active before the batch of
+certificates, then so is every value after it.
 
-Call a `VDeleg`{.AgdaDatatype} *active* in a state if it is one of those two constants or
-if it wraps the `Credential`{.AgdaDatatype} of a `DRep` registered in that state.  The
-present property asserts that a `CERTS`{.AgdaDatatype} step leaves no other kind of
-`VDeleg`{.AgdaDatatype} behind: every value of the `voteDelegs`{.AgdaField} map of the
-resulting state is active in that state.  Nothing is assumed about the initial state,
-because the `POST-CERT`{.AgdaDatatype} rule concluding every `CERTS`{.AgdaDatatype} step
-corestricts `voteDelegs`{.AgdaField} to exactly the set of active
-`VDelegs`{.AgdaDatatype}.
+The two rules that could break this maintain it themselves, in opposite ways.
+`DELEG-delegate`{.AgdaInductiveConstructor} may only install a `VDeleg`{.AgdaDatatype}
+that is already active, and `GOVCERT-deregdrep`{.AgdaInductiveConstructor}, which
+*shrinks* the set of registered `DReps`{.AgdaFunction}, simultaneously deletes every
+delegation to the credential it deregisters.
 
 *Formally*.
 
 ```agda
-activeVDelegs : CertState → ℙ VDeleg
-activeVDelegs s = mapˢ vDelegCredential (dom (DRepsOf s))
+activeVDelegs : ℙ Credential → ℙ VDeleg
+activeVDelegs D =  mapˢ vDelegCredential D
                    ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ [])
 
 voteDelegsVDeleg : CertState → Type
-voteDelegsVDeleg s = range (VoteDelegsOf s) ⊆ activeVDelegs s
+voteDelegsVDeleg s = range (VoteDelegsOf s) ⊆ activeVDelegs (dom (DRepsOf s))
 
-CERTS-voteDelegsVDeleg : Γ ⊢ s ⇀⦇ certs ,CERTS⦈ s' → voteDelegsVDeleg s'
+CERTS-voteDelegsVDeleg : LedgerInvariant _⊢_⇀⦇_,CERTS⦈_ voteDelegsVDeleg
 ```
 
 *Proof*.
 
-A `CERTS`{.AgdaDatatype} step consists of a `PRE-CERT`{.AgdaDatatype} step followed by a
-trace of `CERT`{.AgdaDatatype} steps that ends with a `POST-CERT`{.AgdaDatatype} step, so
-it suffices to establish the property at the end of such a trace.  We do so in two
-lemmas.
+It is convenient to read the property off one entry at a time, so we name the pointwise
+form and record that the two forms agree.
+
+```agda
+vDelegsIn : ℙ Credential → VoteDelegs → Type
+vDelegsIn D m = ∀ {c v} → (c , v) ∈ m → v ∈ activeVDelegs D
+
+⊆⇒vDelegsIn : (m : VoteDelegs) → range m ⊆ activeVDelegs D → vDelegsIn D m
+⊆⇒vDelegsIn _ h cv∈ = h (∈-map′ cv∈)
+
+vDelegsIn⇒⊆ : (m : VoteDelegs) → vDelegsIn D m → range m ⊆ activeVDelegs D
+vDelegsIn⇒⊆ _ h v∈range with Equivalence.from ∈-map v∈range
+... | _ , refl , cv∈ = h cv∈
+```
+
+The set of active `VDelegs`{.AgdaDatatype} grows with the set of credentials, and
+the two constants are active for every set.
+
+```agda
+activeVDelegs-mono : D ⊆ D' → activeVDelegs D ⊆ activeVDelegs D'
+activeVDelegs-mono D⊆D' v∈ with Equivalence.from ∈-∪ v∈
+... | inj₂ v∈consts = Equivalence.to ∈-∪ (inj₂ v∈consts)
+... | inj₁ v∈creds with Equivalence.from ∈-map v∈creds
+... | c , refl , c∈D =
+  Equivalence.to ∈-∪ (inj₁ (Equivalence.to ∈-map (c , refl , D⊆D' c∈D)))
+
+abstain∈active : vDelegAbstain ∈ activeVDelegs D
+abstain∈active = Equivalence.to ∈-∪ (inj₂ (Equivalence.to ∈-fromList (there (here refl))))
+
+noConfidence∈active : vDelegNoConfidence ∈ activeVDelegs D
+noConfidence∈active = Equivalence.to ∈-∪ (inj₂ (Equivalence.to ∈-fromList (here refl)))
+```
+
+**Lemma (`DELEG`{.AgdaDatatype} preserves the property)**.
+The delegatee set is fixed throughout, so this is a statement about
+`voteDelegs`{.AgdaField} alone.  The premise of
+`DELEG-delegate`{.AgdaInductiveConstructor} says precisely that the installed
+`VDeleg`{.AgdaDatatype} is active; `DELEG-dereg`{.AgdaInductiveConstructor} only
+removes entries, and `DELEG-reg`{.AgdaInductiveConstructor} leaves
+`voteDelegs`{.AgdaField} alone.
+
+```agda
+delegatee∈active :
+  just v ∈ mapˢ (just ∘ vDelegCredential) D
+           ∪ fromList (nothing ∷ just vDelegAbstain ∷ just vDelegNoConfidence ∷ [])
+  → v ∈ activeVDelegs D
+delegatee∈active mvd∈ with Equivalence.from ∈-∪ mvd∈
+... | inj₁ ∈creds with Equivalence.from ∈-map ∈creds
+... | c , refl , c∈D = Equivalence.to ∈-∪ (inj₁ (Equivalence.to ∈-map (c , refl , c∈D)))
+delegatee∈active mvd∈ | inj₂ ∈consts with Equivalence.from ∈-fromList ∈consts
+... | there (here refl)         = abstain∈active
+... | there (there (here refl)) = noConfidence∈active
+```
+
+```agda
+DELEG-vDelegsIn : ∀ {pp : PParams} {pools : Pools}
+  → ⟦ pp , pools , D ⟧ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
+  → vDelegsIn D (VoteDelegsOf stᵈ) → vDelegsIn D (VoteDelegsOf stᵈ')
+DELEG-vDelegsIn (DELEG-delegate {mvd = nothing} _) h = h
+DELEG-vDelegsIn (DELEG-delegate {mvd = just _} (_ , _ , mvd∈ , _)) h cv∈
+  with Properties.∈-∪⁻ cv∈
+... | inj₂ cv∈rest = h (proj₂ (Equivalence.from ∈-filter cv∈rest))
+... | inj₁ cv∈new  =
+  subst (_∈ activeVDelegs _)
+        (sym (cong proj₂ (Equivalence.from ∈-singleton cv∈new)))
+        (delegatee∈active mvd∈)
+DELEG-vDelegsIn (DELEG-dereg _) h cv∈ = h (ex-⊆ cv∈)
+DELEG-vDelegsIn (DELEG-reg _) h = h
+```
 
-**Lemma (`POST-CERT`{.AgdaDatatype} establishes the property).** The single constructor
-`CERT-post`{.AgdaInductiveConstructor} reveals the `voteDelegs`{.AgdaField} of its
-resulting state to be a corestriction `vd`{.AgdaBound} `∣^`{.AgdaOperator}
-`X`{.AgdaBound} of the incoming map `vd`{.AgdaBound}, and the range of a corestricted map
-is contained in the corestricting set (`cores-range-⊆`{.AgdaFunction}).  The set
-`X`{.AgdaBound} is read off the `GState`{.AgdaRecord}, which the rule leaves untouched, so
-`X`{.AgdaBound} is `activeVDelegs`{.AgdaFunction} of the resulting state.
+**Lemma (`GOVCERT`{.AgdaDatatype} preserves the property)**.
+`GOVCERT-regdrep`{.AgdaInductiveConstructor} only grows the domain of
+`dreps`{.AgdaField}, so `activeVDelegs`{.AgdaFunction} only grows;
+`GOVCERT-ccreghot`{.AgdaInductiveConstructor} touches neither field.  In the
+`GOVCERT-deregdrep`{.AgdaInductiveConstructor} case a value `v`{.AgdaBound} of the
+resulting map comes from the incoming map and, by the corestriction, differs from
+`vDelegCredential`{.AgdaInductiveConstructor} `c`{.AgdaBound}.  If `v`{.AgdaBound}
+is one of the two constants it stays active; otherwise `v`{.AgdaBound} is
+`vDelegCredential`{.AgdaInductiveConstructor} `c'`{.AgdaBound} for some registered
+`c'`{.AgdaBound}, and `c'`{.AgdaBound} `≢`{.AgdaFunction} `c`{.AgdaBound}, so
+`c'`{.AgdaBound} is still registered after the deregistration.
 
 ```agda
-POST-CERT-voteDelegsVDeleg : Γ ⊢ s ⇀⦇ _ ,POST-CERT⦈ s' → voteDelegsVDeleg s'
-POST-CERT-voteDelegsVDeleg (CERT-post {voteDelegs = vd}) = cores-range-⊆ vd
+GOVCERT-voteDelegsVDeleg : LedgerInvariant _⊢_⇀⦇_,GOVCERT⦈_ voteDelegsVDeleg
+GOVCERT-voteDelegsVDeleg (GOVCERT-regdrep {dReps = dReps} _) h =
+  activeVDelegs-mono (dom-insert-⊇ dReps) ∘ h
+GOVCERT-voteDelegsVDeleg (GOVCERT-ccreghot _) h = h
+GOVCERT-voteDelegsVDeleg (GOVCERT-deregdrep {c = c} {dReps = dReps} {vDelegs = vDelegs} _) h =
+  vDelegsIn⇒⊆ (vDelegs ∣^ ❴ vDelegCredential c ❵ ᶜ) λ cv∈ →
+    let v∉ , cv∈vd = coex-∈⁻ vDelegs cv∈ in
+    reinstate v∉ (⊆⇒vDelegsIn vDelegs h cv∈vd)
+  where
+  -- A delegation to `c'` survives the deregistration of `c` because `c' ≢ c`: were they
+  -- equal, `v` would be the very `vDelegCredential c` the corestriction ruled out.
+  keep : ∀ {v c'} → v ∉ ❴ vDelegCredential c ❵ → v ≡ vDelegCredential c'
+       → c' ∈ dom dReps → v ∈ activeVDelegs (dom (dReps ∣ ❴ c ❵ ᶜ))
+  keep {c' = c'} v∉ v≡ c'∈dom = Equivalence.to ∈-∪ (inj₁ (Equivalence.to ∈-map
+    ( c' , v≡
+    , ∈-resᶜ-dom⁺ ( (λ c'∈ → v∉ (Equivalence.to ∈-singleton (trans v≡
+                      (cong vDelegCredential (Equivalence.from ∈-singleton c'∈)))))
+                  , Equivalence.from dom∈ c'∈dom ) )))
+
+  reinstate : ∀ {v} → v ∉ ❴ vDelegCredential c ❵ → v ∈ activeVDelegs (dom dReps)
+            → v ∈ activeVDelegs (dom (dReps ∣ ❴ c ❵ ᶜ))
+  reinstate v∉ v∈ with Equivalence.from ∈-∪ v∈
+  ... | inj₂ v∈consts = Equivalence.to ∈-∪ (inj₂ v∈consts)
+  ... | inj₁ v∈creds  =
+    let c' , v≡ , c'∈dom = Equivalence.from ∈-map v∈creds in keep v∉ v≡ c'∈dom
 ```
 
-**Lemma (the property holds at the end of a `CERT`{.AgdaDatatype} trace).** Induct on the
-trace.  The intermediate `CERT`{.AgdaDatatype} steps are irrelevant: only the final state
-is constrained, and it is produced by the `POST-CERT`{.AgdaDatatype} step in the
-`run-[]`{.AgdaInductiveConstructor} case.
+**Lemma (`CERT`{.AgdaDatatype} and `PRE-CERT`{.AgdaDatatype} preserve the property)**.
+`CERT-pool`{.AgdaInductiveConstructor} touches neither field, and
+`CERT-pre`{.AgdaInductiveConstructor} leaves `voteDelegs`{.AgdaField} alone while
+refreshing `dreps`{.AgdaField} with a left-biased union that keeps every key.
 
 ```agda
-CERT-trace-voteDelegsVDeleg :
-  RunTraceAndThen _⊢_⇀⦇_,CERT⦈_ _⊢_⇀⦇_,POST-CERT⦈_ Γ s certs s' → voteDelegsVDeleg s'
-CERT-trace-voteDelegsVDeleg (run-[] post)    = POST-CERT-voteDelegsVDeleg post
-CERT-trace-voteDelegsVDeleg (run-∷ _ trace)  = CERT-trace-voteDelegsVDeleg trace
+CERT-voteDelegsVDeleg : LedgerInvariant _⊢_⇀⦇_,CERT⦈_ voteDelegsVDeleg
+CERT-voteDelegsVDeleg (CERT-deleg {stᵈ = stᵈ} {stᵈ' = stᵈ'} deleg) h =
+  vDelegsIn⇒⊆ (VoteDelegsOf stᵈ')
+              (DELEG-vDelegsIn deleg (⊆⇒vDelegsIn (VoteDelegsOf stᵈ) h))
+CERT-voteDelegsVDeleg (CERT-pool _) h = h
+CERT-voteDelegsVDeleg (CERT-vdel govcert) h = GOVCERT-voteDelegsVDeleg govcert h
+
+PRE-CERT-voteDelegsVDeleg : LedgerInvariant _⊢_⇀⦇_,PRE-CERT⦈_ voteDelegsVDeleg
+PRE-CERT-voteDelegsVDeleg (CERT-pre {dReps = dReps} _) h =
+  activeVDelegs-mono (dom-mapValueRestricted-⊇ dReps) ∘ h
 ```
 
-The theorem follows by inverting the `CERTS`{.AgdaDatatype} step and discarding its
-`PRE-CERT`{.AgdaDatatype} component.
+A `CERTS`{.AgdaDatatype} step is a `PRE-CERT`{.AgdaDatatype} step followed by a
+trace of `CERT`{.AgdaDatatype} steps, so the theorem follows by lifting the two
+lemmas along the reflexive-transitive closure.
 
 ```agda
-CERTS-voteDelegsVDeleg (run (_ , trace)) = CERT-trace-voteDelegsVDeleg trace
+CERTS-voteDelegsVDeleg (run (pre , trace)) =
+  RTC-preserves-inv CERT-voteDelegsVDeleg trace ∘ PRE-CERT-voteDelegsVDeleg pre
 ```

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

@@ -165,13 +165,19 @@ proposals in `tx`{.AgdaBound}.
 +  **Theorem** [Certs-VoteDelegsVDeleg][]. Vote delegations point at registered
    `DReps`{.AgdaFunction}.
 
-   Let `s`{.AgdaBound}, `s'`{.AgdaBound} be `CertStates`{.AgdaRecord} and
-   `certs`{.AgdaBound} a list of `DCerts`{.AgdaDatatype} such that `s`{.AgdaBound}
-   `⇀⦇`{.AgdaDatatype} `certs`{.AgdaBound} `,CERTS⦈`{.AgdaDatatype} `s'`{.AgdaBound}.
-   Then every value of the `voteDelegs`{.AgdaField} map of `s'`{.AgdaBound} either wraps
-   the `Credential`{.AgdaDatatype} of a `DRep` registered in `s'`{.AgdaBound}, or is
+   Say a `CertState`{.AgdaRecord} `s`{.AgdaBound} *delegates actively* when every value
+   of its `voteDelegs`{.AgdaField} map either wraps the `Credential`{.AgdaDatatype} of a
+   `DRep` registered in `s`{.AgdaBound}, or is
    `vDelegAbstain`{.AgdaInductiveConstructor}, or is
-   `vDelegNoConfidence`{.AgdaInductiveConstructor}.
+   `vDelegNoConfidence`{.AgdaInductiveConstructor}.  This is an invariant of the
+   `CERTS`{.AgdaDatatype} rule: if `s`{.AgdaBound} delegates actively and `s`{.AgdaBound}
+   `⇀⦇`{.AgdaDatatype} `certs`{.AgdaBound} `,CERTS⦈`{.AgdaDatatype} `s'`{.AgdaBound},
+   then `s'`{.AgdaBound} delegates actively.
+
+   Two rules keep it so.  `DELEG-delegate`{.AgdaInductiveConstructor} may install only a
+   delegation that is already active, and
+   `GOVCERT-deregdrep`{.AgdaInductiveConstructor}, the one rule that unregisters a
+   `DRep`, deletes every delegation to it in the same step.
 
 ---