[Conway] Property : voteDelegs range lies in VDelegs of registered DReps (#1233)

build-tools/static/mkdocs/docs/ledger-properties-dashboard.md

@@ -20,14 +20,15 @@ _Generated by `build-tools/scripts/property-tracking/scan_properties.py` from th
 
 | Era | proved | stated | planned | idea | total |
 | --- | ---: | ---: | ---: | ---: | ---: |
-| conway | 15 | 5 | 0 | 2 | 22 |
+| conway | 16 | 4 | 0 | 2 | 22 |
 | dijkstra | 0 | 0 | 0 | 15 | 15 |
 
 ### Conway
 
 | Status | Property | STS | Agda module | Issue(s) |
 | --- | --- | --- | --- | --- |
 | ✅ proved | CERT and CERTS preserve value | CERTS | [`Ledger.Conway.Specification.Certs.Properties.PoV`](Ledger.Conway.Specification.Certs.Properties.PoV.md) | [#1240](https://github.com/intersectmbo/formal-ledger-specifications/issues/1240) |
+| ✅ proved | voteDelegs range is contained in VDelegs built from its domain | CERTS | [`Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg`](Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg.md) | [#1233](https://github.com/intersectmbo/formal-ledger-specifications/issues/1233) |
 | ✅ proved | GA deposits are eventually refunded | CHAIN | [`Ledger.Conway.Specification.Chain.Properties.EventuallyRefunded`](Ledger.Conway.Specification.Chain.Properties.EventuallyRefunded.md) | [#414](https://github.com/intersectmbo/formal-ledger-specifications/issues/414) |
 | ✅ proved | govDepsMatch is a CHAIN invariant | CHAIN | [`Ledger.Conway.Specification.Chain.Properties.GovDepsMatch`](Ledger.Conway.Specification.Chain.Properties.GovDepsMatch.md) | [#1235](https://github.com/intersectmbo/formal-ledger-specifications/issues/1235) |
 | ✅ proved | EPOCH preserves the DReps equivalence (expired-DReps parametricity) | EPOCH | [`Ledger.Conway.Specification.Epoch.Properties.ExpiredDReps`](Ledger.Conway.Specification.Epoch.Properties.ExpiredDReps.md) | [#1241](https://github.com/intersectmbo/formal-ledger-specifications/issues/1241) |
@@ -42,7 +43,6 @@ _Generated by `build-tools/scripts/property-tracking/scan_properties.py` from th
 | ✅ proved | k proposals grow the GA deposit pot by k * govActionDeposit | UTXO | [`Ledger.Conway.Specification.Utxo.Properties.GenMinSpend`](Ledger.Conway.Specification.Utxo.Properties.GenMinSpend.md) | [#413](https://github.com/intersectmbo/formal-ledger-specifications/issues/413) |
 | ✅ proved | Coin consumed is at least the sum of GA deposits of the proposals | UTXO | [`Ledger.Conway.Specification.Utxo.Properties.MinSpend`](Ledger.Conway.Specification.Utxo.Properties.MinSpend.md) | [#1228](https://github.com/intersectmbo/formal-ledger-specifications/issues/1228) |
 | ✅ proved | UTXO preserves value | UTXO | [`Ledger.Conway.Specification.Utxo.Properties.PoV`](Ledger.Conway.Specification.Utxo.Properties.PoV.md) | [#1239](https://github.com/intersectmbo/formal-ledger-specifications/issues/1239) |
-| 🟡 stated | voteDelegs range is contained in VDelegs built from its domain | CERTS | [`Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg`](Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg.md) | [#1233](https://github.com/intersectmbo/formal-ledger-specifications/issues/1233) |
 | 🟡 stated | dom rewards = CredentialDeposit^-1 (dom deposits) is a CHAIN invariant | CHAIN | [`Ledger.Conway.Specification.Chain.Properties.CredDepsEqualDomRwds`](Ledger.Conway.Specification.Chain.Properties.CredDepsEqualDomRwds.md) | [#1230](https://github.com/intersectmbo/formal-ledger-specifications/issues/1230) |
 | 🟡 stated | EnactState only changes at an epoch boundary (new enact state => new epoch) | CHAIN | [`Ledger.Conway.Specification.Chain.Properties.EpochStep`](Ledger.Conway.Specification.Chain.Properties.EpochStep.md) | [#412](https://github.com/intersectmbo/formal-ledger-specifications/issues/412) |
 | 🟡 stated | Well-formedness of PParams is a CHAIN invariant | CHAIN | [`Ledger.Conway.Specification.Chain.Properties.PParamsWellFormed`](Ledger.Conway.Specification.Chain.Properties.PParamsWellFormed.md) | [#1231](https://github.com/intersectmbo/formal-ledger-specifications/issues/1231) |

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

@@ -703,6 +703,41 @@ module _  {A B : Type}
       lem-del-excluded m ¬p = filterᵐ-restrict m ⟨≈⟩ restrict-singleton-filterᵐ-false m ¬p
 
 
+-- Corestriction
+
+-- 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`).
+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
 
 -- Looking up a freshly inserted key returns the inserted value.

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

@@ -3,7 +3,7 @@ source_branch: master
 source_path: src/Ledger/Conway/Specification/Certs/Properties/VoteDelegsVDeleg.lagda.md
 ---
 
-## Claim: <span class="AgdaField">voteDelegs</span> field values are <span class="AgdaDatatype">VDelegs</span> constructed from their keys {#clm:VDelegsInRegDReps}
+## Theorem: <span class="AgdaField">voteDelegs</span> values point at registered <span class="AgdaFunction">DReps</span> {#clm:VDelegsInRegDReps}
 
 <!--
 ```agda
@@ -12,40 +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
+  stᵈ stᵈ'  : DState
+  certs     : List DCert
+  dCert     : DCert
+  D D'      : ℙ Credential
+  m         : VoteDelegs
+  v         : VDeleg
 ```
 -->
 
 *Informally*.
 
-A `CertState`{.AgdaRecord} has a `DState`{.AgdaDatatype}, a `PState`{.AgdaDatatype}, and a
-`GState`{.AgdaDatatype}.  The `DState`{.AgdaDatatype} contains a field
-`voteDelegs`{.AgdaField} which is a mapping from `Credential`{.AgdaDatatype} to
-`VDeleg`{.AgdaDatatype}.
+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} is a datatype with three constructors; the one of interest to
-us here is `vDelegCredential`{.AgdaInductiveConstructor}, which takes a `Credential`{.AgdaDatatype}.
+`VDeleg`{.AgdaDatatype} has three constructors:
+`vDelegCredential`{.AgdaInductiveConstructor}, which takes the
+`Credential`{.AgdaDatatype} of a `DRep`, and the two constants
+`vDelegAbstain`{.AgdaInductiveConstructor} and
+`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.
 
-Now suppose we have a collection `C`{.AgdaBound} of credentials—for instance, given
-`d`{.AgdaBound} : `DState`{.AgdaDatatype}, take `C`{.AgdaBound} to be the domain of
-the `voteDelegs`{.AgdaField} field of `d`{.AgdaBound}. We could then obtain a set of
-`VDelegs`{.AgdaDatatype} by applying `vDelegCredential`{.AgdaInductiveConstructor} to
-each element of `C`{.AgdaBound}.
+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.
 
-The present property asserts that the set of `VDelegs`{.AgdaDatatype} that results
-from the application of `vDelegCredential`{.AgdaInductiveConstructor} to the
-domain of the `voteDelegs`{.AgdaField} of `d`{.AgdaBound} contains the range
-of the `voteDelegs`{.AgdaField} of `d`{.AgdaBound}.
+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
-voteDelegsVDeleg :  DState → Type
-voteDelegsVDeleg d = range (VoteDelegsOf d) ⊆ mapˢ vDelegCredential (dom (VoteDelegsOf d))
+activeVDelegs : ℙ Credential → ℙ VDeleg
+activeVDelegs D =  mapˢ vDelegCredential D
+                   ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ [])
+
+voteDelegsVDeleg : CertState → Type
+voteDelegsVDeleg s = range (VoteDelegsOf s) ⊆ activeVDelegs (dom (DRepsOf s))
+
+CERTS-voteDelegsVDeleg : LedgerInvariant _⊢_⇀⦇_,CERTS⦈_ voteDelegsVDeleg
 ```
 
-*Proof*. (coming soon)
+*Proof*.
+
+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 (`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
+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 (`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-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
+```
+
+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 (pre , trace)) =
+  RTC-preserves-inv CERT-voteDelegsVDeleg trace ∘ PRE-CERT-voteDelegsVDeleg pre
+```

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

@@ -162,15 +162,22 @@ proposals in `tx`{.AgdaBound}.
    `activeDReps`{.AgdaField} of `es` in the next epoch.
 
 
-+  **Claim** [Certs-VoteDelegsVDeleg][].
-
-   Suppose we have a collection `C`{.AgdaBound} of credentials—for instance, given
-   `d`{.AgdaBound} : `DState`{.AgdaDatatype}, take `C`{.AgdaBound} to be the domain
-   of the `voteDelegs`{.AgdaField} field of `d`{.AgdaBound}.  Then the set of
-   `VDelegs`{.AgdaDatatype} that results from applying
-   `vDelegCredential`{.AgdaInductiveConstructor} to the domain of the
-   `voteDelegs`{.AgdaField} of `d`{.AgdaBound} contains the range of the
-   `voteDelegs`{.AgdaField} of `d`{.AgdaBound}.
++  **Theorem** [Certs-VoteDelegsVDeleg][]. Vote delegations point at registered
+   `DReps`{.AgdaFunction}.
+
+   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}.  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.
 
 ---