Votes in the state must be by registered entities

src/Ledger/Conway/Conformance/Gov.agda

@@ -3,16 +3,16 @@
 open import Ledger.Types.GovStructure
 open import Ledger.Transaction using (TransactionStructure)
 
-module Ledger.Conway.Conformance.Gov (txs : _) (open TransactionStructure txs using (govStructure)) where
-open GovStructure govStructure hiding (epoch)
+module Ledger.Conway.Conformance.Gov (txs : _) (open TransactionStructure txs hiding (epoch)) where
 
 open import Ledger.Prelude hiding (any?; Any; all?; All; Rel; lookup; ∈-filter)
 
 open import Axiom.Set.Properties th using (∃-sublist-⇔)
 
-open import Ledger.GovernanceActions govStructure hiding (yes; no)
+open import Ledger.GovernanceActions govStructure using (Vote)
 open import Ledger.Enact govStructure
 open import Ledger.Conway.Conformance.Ratify txs hiding (vote)
+open import Ledger.Conway.Conformance.Certs govStructure
 
 open import Data.List.Ext using (subpermutations; sublists)
 open import Data.List.Ext.Properties2
@@ -32,21 +32,15 @@ GovState : Type
 GovState = List (GovActionID × GovActionState)
 
 record GovEnv : Type where
-
-  constructor ⟦_,_,_,_,_⟧ᵍ
+  constructor ⟦_,_,_,_,_,_⟧ᵍ
   field
 
     txid        : TxId
     epoch       : Epoch
     pparams     : PParams
     ppolicy     : Maybe ScriptHash
     enactState  : EnactState
-
-data
-
-  _⊢_⇀⦇_,GOV'⦈_  : GovEnv × ℕ → GovState → GovVote ⊎ GovProposal → GovState → Type
-
-_⊢_⇀⦇_,GOV⦈_     : GovEnv → GovState → List (GovVote ⊎ GovProposal) → GovState → Type
+    certState   : CertState
 
 private variable
   Γ : GovEnv
@@ -62,6 +56,9 @@ private variable
   k : ℕ
   p : Maybe ScriptHash
 
+open GState
+open PState
+
 govActionPriority : GovAction → ℕ
 govActionPriority NoConfidence             = 0
 govActionPriority (UpdateCommittee _ _ _)  = 1
@@ -74,13 +71,13 @@ govActionPriority Info                     = 6
 _∼_ : ℕ → ℕ → Type
 n ∼ m = (n ≡ m) ⊎ (n ≡ 0 × m ≡ 1) ⊎ (n ≡ 1 × m ≡ 0)
 
-_≈_ : GovAction → GovAction → Type
-a ≈ a' = (govActionPriority a) ∼ (govActionPriority a')
+_≈ᵍ_ : GovAction → GovAction → Type
+a ≈ᵍ a' = (govActionPriority a) ∼ (govActionPriority a')
 
 _∼?_ : (n m : ℕ) → Dec (n ∼ m)
 n ∼? m = n ≟ m ⊎-dec (n ≟ 0 ×-dec m ≟ 1) ⊎-dec (n ≟ 1 ×-dec m ≟ 0)
 
-_≈?_ : (a a' : GovAction) → Dec (a ≈ a')
+_≈?_ : (a a' : GovAction) → Dec (a ≈ᵍ a')
 a ≈? a' = (govActionPriority a) ∼? (govActionPriority a')
 
 
@@ -91,11 +88,6 @@ insertGovAction ((gaID₀ , gaSt₀) ∷ gaPrs) (gaID₁ , gaSt₁)
      then (gaID₀ , gaSt₀) ∷ insertGovAction gaPrs (gaID₁ , gaSt₁)
      else (gaID₁ , gaSt₁) ∷ (gaID₀ , gaSt₀) ∷ gaPrs
 
-addVote : GovState → GovActionID → Voter → Vote → GovState
-addVote s aid voter v = map modifyVotes s
-  where modifyVotes = λ (gid , s') → gid , record s'
-          { votes = if gid ≡ aid then insert (votes s') voter v else votes s'}
-
 mkGovStatePair : Epoch → GovActionID → RwdAddr → (a : GovAction) → NeedsHash a
                  → GovActionID × GovActionState
 mkGovStatePair e aid addr a prev = (aid , record
@@ -106,11 +98,29 @@ addAction : GovState
           → GovState
 addAction s e aid addr a prev = insertGovAction s (mkGovStatePair e aid addr a prev)
 
-validHFAction : GovProposal → GovState → EnactState → Type
-validHFAction (record { action = TriggerHF v ; prevAction = prev }) s e =
-  (let (v' , aid) = EnactState.pv e in aid ≡ prev × pvCanFollow v' v)
-  ⊎ ∃₂[ x , v' ] (prev , x) ∈ fromList s × x .action ≡ TriggerHF v' × pvCanFollow v' v
-validHFAction _ _ _ = ⊤
+opaque
+  addVote : GovState → GovActionID → Voter → Vote → GovState
+  addVote s aid voter v = map modifyVotes s
+    where modifyVotes : GovActionID × GovActionState → GovActionID × GovActionState
+          modifyVotes = λ (gid , s') → gid , record s'
+            { votes = if gid ≡ aid then insert (votes s') voter v else votes s'}
+
+  isRegistered : GovEnv → Voter → Type
+  isRegistered ⟦ _ , _ , _ , _ , _ , ⟦ _ , pState , gState ⟧ᶜˢ ⟧ᵍ (r , c) = case r of λ where
+    CC    → just c ∈ range (gState .ccHotKeys)
+    DRep  → c ∈ dom (gState .dreps)
+    SPO   → c ∈ mapˢ KeyHashObj (dom (pState .pools))
+
+  validHFAction : GovProposal → GovState → EnactState → Type
+  validHFAction (record { action = TriggerHF v ; prevAction = prev }) s e =
+    (let (v' , aid) = EnactState.pv e in aid ≡ prev × pvCanFollow v' v)
+    ⊎ ∃₂[ x , v' ] (prev , x) ∈ fromList s × x .action ≡ TriggerHF v' × pvCanFollow v' v
+  validHFAction _ _ _ = ⊤
+
+data
+  _⊢_⇀⦇_,GOV'⦈_  : GovEnv × ℕ → GovState → GovVote ⊎ GovProposal → GovState → Type
+
+_⊢_⇀⦇_,GOV⦈_   : GovEnv → GovState → List (GovVote ⊎ GovProposal) → GovState → Type
 
 -- Convert list of (GovActionID,GovActionState)-pairs to list of GovActionID pairs.
 getAidPairsList : GovState → List (GovActionID × GovActionID)
@@ -147,7 +157,7 @@ hasParentE e aid a = case getHashES e a of
 hasParent : EnactState → GovState → (a : GovAction) → NeedsHash a → Type
 hasParent e s a aid with getHash aid
 ... | just aid' = hasParentE e aid' a
-                  ⊎ Any (λ (gid , gas) → gid ≡ aid' × action gas ≈ a) s
+                  ⊎ Any (λ (gid , gas) → gid ≡ aid' × action gas ≈ᵍ a) s
 ... | nothing = ⊤
 
 open Equivalence
@@ -236,6 +246,7 @@ data _⊢_⇀⦇_,GOV'⦈_ where
     in
     ∙ (aid , ast) ∈ fromList s
     ∙ canVote pparams (action ast) (proj₁ voter)
+    ∙ isRegistered Γ voter
       ───────────────────────────────────────
       (Γ , k) ⊢ s ⇀⦇ inj₁ vote ,GOV'⦈ addVote s aid voter v
 

src/Ledger/Conway/Conformance/Gov/Properties.agda

@@ -75,6 +75,9 @@ private
   hasPrev record { action = (TreasuryWdrl _) }        v = no λ ()
   hasPrev record { action = Info }                    v = no λ ()
 
+opaque
+  unfolding validHFAction isRegistered
+
   instance
     validHFAction? : ∀ {p s e} → validHFAction p s e ⁇
     validHFAction? {record { action = NoConfidence }} = Dec-⊤
@@ -93,6 +96,11 @@ private
     validHFAction? {record { action = TreasuryWdrl _ }} = Dec-⊤
     validHFAction? {record { action = Info }} = Dec-⊤
 
+  isRegistered? : ∀ Γ v → Dec (isRegistered Γ v)
+  isRegistered? _ (CC   , _) = ¿ _ ∈ _ ¿
+  isRegistered? _ (DRep , _) = ¿ _ ∈ _ ¿
+  isRegistered? _ (SPO  , _) = ¿ _ ∈ _ ¿
+
 instance
   Computational-GOV' : Computational _⊢_⇀⦇_,GOV'⦈_ String
   Computational-GOV' = record {Go} where
@@ -103,15 +111,18 @@ instance
       module GoVote sig where
         open GovVote sig
 
-        computeProof = case lookupActionId pparams (proj₁ voter) gid s of λ where
-            (yes p) → case Any↔ .from p of λ where
-              (_ , mem , refl , cV) → success (_ , GOV-Vote (∈-fromList .to mem , cV))
-            (no ¬p)  → failure (genErrors ¬p)
+        computeProof = case lookupActionId pparams (proj₁ voter) gid s ,′ isRegistered? (proj₁ Γ) voter of λ where
+            (yes p , yes p') → case Any↔ .from p of λ where
+              (_ , mem , refl , cV) → success (_ , GOV-Vote (∈-fromList .to mem , cV , p'))
+            (yes _ , no ¬p) → failure (genErrors ¬p)
+            (no ¬p , _)     → failure (genErrors ¬p)
 
         completeness : ∀ s' → Γ ⊢ s ⇀⦇ inj₁ sig ,GOV'⦈ s' → map proj₁ computeProof ≡ success s'
-        completeness s' (GOV-Vote (mem , cV)) with lookupActionId pparams (proj₁ voter) gid s
-        ... | no ¬p = ⊥-elim (¬p (Any↔ .to (_ , ∈-fromList .from mem , refl , cV)))
-        ... | yes p with Any↔ .from p
+        completeness s' (GOV-Vote (mem , cV , reg))
+          with lookupActionId pparams (proj₁ voter) gid s | isRegistered? (proj₁ Γ) voter
+        ... | no ¬p | _ = ⊥-elim (¬p (Any↔ .to (_ , ∈-fromList .from mem , refl , cV)))
+        ... | yes _ | no ¬p = ⊥-elim $ ¬p reg
+        ... | yes p | yes p' with Any↔ .from p
         ... | (_ , mem , refl , cV) = refl
 
       module GoProp prop where

src/Ledger/Conway/Conformance/Ledger.agda

@@ -19,6 +19,8 @@ open import Ledger.Conway.Conformance.Utxow txs abs
 open import Ledger.Conway.Conformance.Certs govStructure
 
 open Tx
+open GState
+open GovActionState
 
 record LEnv : Type where
 
@@ -44,6 +46,17 @@ txgov : TxBody → List (GovVote ⊎ GovProposal)
 txgov txb = map inj₂ txprop ++ map inj₁ txvote
   where open TxBody txb
 
+isUnregisteredDRep : CertState → Voter → Type
+isUnregisteredDRep ⟦ _ , _ , gState ⟧ᶜˢ (r , c) = r ≡ DRep × c ∉ dom (gState .dreps)
+
+removeOrphanDRepVotes : CertState → GovActionState → GovActionState
+removeOrphanDRepVotes certState gas = record gas { votes = votes′ }
+  where
+    votes′ = filterKeys (¬_ ∘ isUnregisteredDRep certState) (votes gas)
+
+_|ᵒ_ : GovState → CertState → GovState
+govSt |ᵒ certState = L.map (map₂ (removeOrphanDRepVotes certState)) govSt
+
 private variable
   Γ : LEnv
   s s' s'' : LState
@@ -70,7 +83,7 @@ data
     ∙  isValid tx ≡ true
     ∙  record { LEnv Γ } ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'
     ∙  ⟦ epoch slot , pparams , txvote , txwdrls ⟧ᶜ ⊢ certState ⇀⦇ txcerts ,CERTS⦈ certState'
-    ∙  ⟦ txid , epoch slot , pparams , ppolicy , enactState ⟧ᵍ ⊢ govSt ⇀⦇ txgov txb ,GOV⦈ govSt'
+    ∙  ⟦ txid , epoch slot , pparams , ppolicy , enactState , certState' ⟧ᵍ ⊢ govSt |ᵒ certState' ⇀⦇ txgov txb ,GOV⦈ govSt'
        ────────────────────────────────
        Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ ⟦ utxoSt'' , govSt' , certState' ⟧ˡ