VoteDelegsVDeleg
Theorem: voteDelegs values point at registered DReps¶
Informally.
A CertState has a DState, a PState,
and a GState. The DState contains a field
voteDelegs, a map sending the Credential of a
delegator to the VDeleg that receives its voting stake. The
GState contains a field dreps whose domain is the set
of registered DReps.
VDeleg has three constructors:
vDelegCredential, which takes the
Credential of a DRep, and the two constants
vDelegAbstain and
vDelegNoConfidence. Call a VDeleg
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 step introduces a
vote delegation that is inactive for the registered DReps: if
every value of voteDelegs 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 may only install a VDeleg
that is already active, and GOVCERT-deregdrep, which
shrinks the set of registered DReps, simultaneously deletes every
delegation to the credential it deregisters.
Formally.
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.
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.
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 grows with the set of credentials, and
the two constants are active for every set.
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 preserves the property).
The delegatee set is fixed throughout, so this is a statement about
voteDelegs alone. The premise of
DELEG-delegate says precisely that the installed
VDeleg is active; DELEG-dereg only
removes entries, and DELEG-reg leaves
voteDelegs alone.
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
DELEG-vDelegsIn : ∀ {pp : PParams} {pools : Pools} → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg.html#5090}{\htmlId{5126}{\htmlClass{Bound}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg.html#5105}{\htmlId{5131}{\htmlClass{Bound}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg.html#803}{\htmlId{5139}{\htmlClass{Generalizable}{\text{D}}}}\, \end{pmatrix}$ ⊢ 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 preserves the property).
GOVCERT-regdrep only grows the domain of
dreps, so activeVDelegs only grows;
GOVCERT-ccreghot touches neither field. In the
GOVCERT-deregdrep case a value v of the
resulting map comes from the incoming map and, by the corestriction, differs from
vDelegCredential c. If v
is one of the two constants it stays active; otherwise v is
vDelegCredential c' for some registered
c', and c' ≢ c, so
c' is still registered after the deregistration.
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 and PRE-CERT preserve the property).
CERT-pool touches neither field, and
CERT-pre leaves voteDelegs alone while
refreshing dreps with a left-biased union that keeps every key.
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 step is a PRE-CERT step followed by a
trace of CERT steps, so the theorem follows by lifting the two
lemmas along the reflexive-transitive closure.
CERTS-voteDelegsVDeleg (run (pre , trace)) = RTC-preserves-inv CERT-voteDelegsVDeleg trace ∘ PRE-CERT-voteDelegsVDeleg pre