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.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Author: williamdemeo

CHANGELOG.md

@@ -34,6 +34,7 @@
 ## Conway spec
 
 - Remove POST-CERT; delegated stake for voting is now removed by GOVCERT at the moment of deregistration
+- State and prove that `CERTS` preserves the property that every `voteDelegs` value is a `VDeleg` of a registered `DRep`, `vDelegAbstain`, or `vDelegNoConfidence` (see #1233)
 - Move `txIns ∩ refInputs ≡ ∅` precondition to `allowedLanguages` to allow non-disjoint tx and ref. inputs for Plutus V1-V2
 - Require collateral inputs to be present in the UTxO set in the UTXO rule
 - State and prove the claim that a voter's (last) vote in a block is applied to the governance action (see #417)

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

@@ -705,14 +705,38 @@ 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 = Equivalence.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 =
+  Equivalence.to dom∈ ( proj₁ (Equivalence.from dom∈ a∈dom)
+                      , Properties.∈-∪⁺ (inj₁ (proj₂ (Equivalence.from dom∈ a∈dom))) )
+... | no a∉dom =
+  Equivalence.to dom∈ ( proj₁ (Equivalence.from dom∈ a∈dom')
+                      , Properties.∈-∪⁺ (inj₂ (Equivalence.to ∈-filter
+                          (a∉dom , proj₂ (Equivalence.from dom∈ a∈dom')))) )
+
+-- 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

@@ -18,10 +18,17 @@ 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
 ```
 -->
 
@@ -40,63 +47,164 @@ contains a field `dreps`{.AgdaField} whose domain is the set of registered
 `vDelegAbstain`{.AgdaInductiveConstructor} and
 `vDelegNoConfidence`{.AgdaInductiveConstructor}.
 
-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}.
+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 present property 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 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

@@ -162,13 +162,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.
 
 ---