Remove vote delegated stake when dreps are unregistered in a tx (Conway)

Author: carlostome

CHANGELOG.md

@@ -33,6 +33,7 @@
 
 ## Conway spec
 
+- Remove POST-CERT; delegated stake for voting is now removed by GOVCERT at the moment of deregistration
 - 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/Interface/ComputationalRelation.lagda.md

@@ -583,3 +583,27 @@ module _ {Init : C → S → ⊤ → S → Type} ⦃ _ : Computational Init Err
               | completeness {Err = Err} _ _ _ _ rtat
         ...   | success (t' , r) | refl = refl
 ```
+
+```agda
+module _ {Init : C → S → ⊤ → S → Type} ⦃ _ : Computational Init Err₂ ⦄ where
+  module _ {Step : C → S → Sig → S → Type} ⦃ _ : Computational Step Err₁ ⦄
+           ⦃ _ : InjectError Err₁ Err ⦄ ⦃ _ : InjectError Err₂ Err ⦄ where
+
+    instance
+      Computational-RunTraceAfter : Computational (RunTraceAfter Init Step) Err
+
+      Computational-RunTraceAfter .computeProof Γ s sigs
+        with computeProof {STS = Init} Γ s tt
+      ... | failure e = failure (injectError it e)
+      ... | success (s' , h)
+            with computeProof {STS = ReflexiveTransitiveClosure {sts = Step}} {Err = Err} Γ s' sigs
+      ...   | failure e = failure e
+      ...   | success (t , r) = success (t , run (h , r))
+
+      Computational-RunTraceAfter .completeness Γ s sigs t (run (init , rtc))
+        with computeProof {STS = Init} Γ s tt | completeness _ _ _ _ init
+      ... | success (s' , h) | refl
+            with computeProof {STS = ReflexiveTransitiveClosure {sts = Step}} {Err = Err} Γ s' sigs
+            | completeness {Err = Err} _ _ _ _ rtc
+      ...   | success (t' , r) | refl = refl
+```

src/Interface/STS.lagda.md

@@ -40,6 +40,9 @@ does—it processes a list of signals, transforming state.
    +  `RunTraceAfterAndThen`: run a given transition (`Init`), then run a transition
       (`Step`) for a each signal in a given list, then, once the list is empty, run a
       final (`Last`) transition.
+   +  `RunTraceAfter`: run a given transition (`Init`), then run a transition (`Step`)
+      for each signal in a given list. This is `RunTraceAfterAndThen` with a trivial
+      final transition, built on the reflexive-transitive closure of `Step`.
 
 ## High-level picture
 
@@ -142,6 +145,20 @@ ReflexiveTransitiveClosureᵢᵇ = _⊢_⇀⟦_⟧ᵢ*_
 ReflexiveTransitiveClosureᵇ = _⊢_⇀⟦_⟧*_
 ```
 
+### Running a Trace After an Initial Transition
+
+```agda
+data RunTraceAfter (Init : C → S → ⊤ → S → Type)
+                   (Step : C → S → Sig → S → Type) :
+  C → S → List Sig → S → Type where
+
+    run :
+        ∙ Init Γ s tt s'
+        ∙ ReflexiveTransitiveClosure {sts = Step} Γ s' sigs s''
+        ─────────────────────────────────────────────
+        RunTraceAfter Init Step Γ s sigs s''
+```
+
 ## Totality
 
 We say a single-step relation is **total** if every input has some output.

src/Ledger/Conway/Conformance/Certs.lagda.md

@@ -19,7 +19,7 @@ private module Certs = Ledger.Conway.Specification.Certs gs
 open Certs public
   hiding (DState; GState; CertState; HasCast-DState; HasCast-GState; HasCast-CertState;
           _⊢_⇀⦇_,DELEG⦈_; _⊢_⇀⦇_,GOVCERT⦈_;
-          _⊢_⇀⦇_,CERT⦈_; _⊢_⇀⦇_,PRE-CERT⦈_; _⊢_⇀⦇_,POST-CERT⦈_; _⊢_⇀⦇_,CERTS⦈_; ⟦_,_,_⟧ᵈ)
+          _⊢_⇀⦇_,CERT⦈_; _⊢_⇀⦇_,PRE-CERT⦈_; _⊢_⇀⦇_,CERTS⦈_; ⟦_,_,_⟧ᵈ)
 open RewardAddress
 
 record DState : Type where
@@ -105,6 +105,7 @@ private variable
   stᵈ stᵈ' : DState
   stᵍ stᵍ' : GState
   stᵖ stᵖ' : PState
+  stᶜ stᶜ' : CertState
 
 open GovVote
 
@@ -149,31 +150,31 @@ data _⊢_⇀⦇_,DELEG⦈_ where
         ⟦ vDelegs , sDelegs , rwds ∪ˡ ❴ c , 0 ❵
         , updateCertDeposit pp (reg c d) dep ⟧
 
-data _⊢_⇀⦇_,GOVCERT⦈_ : CertEnv → GState → DCert → GState → Type where
+data _⊢_⇀⦇_,GOVCERT⦈_ : CertEnv → CertState → DCert → CertState → Type where
   GOVCERT-regdrep : ∀ {pp} → let open PParams pp in
     ∙ (d ≡ drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps)
       ────────────────────────────────
       ⟦ e , pp , vs , wdrls , cc ⟧ ⊢
-      ⟦ dReps , ccKeys , dep ⟧
+      ⟦ stᵈ , stᵖ , ⟦ dReps , ccKeys , dep ⟧ ⟧
         ⇀⦇ regdrep c d an ,GOVCERT⦈
-      ⟦ ❴ c , e + drepActivity ❵ ∪ˡ dReps , ccKeys
-      , updateCertDeposit pp (regdrep c d an ) dep ⟧
+      ⟦ stᵈ , stᵖ , ⟦ ❴ c , e + drepActivity ❵ ∪ˡ dReps , ccKeys
+      , updateCertDeposit pp (regdrep c d an ) dep ⟧ ⟧
 
   GOVCERT-deregdrep :
     ∙ c ∈ dom dReps
     ∙ (DRepDeposit c , d) ∈ dep
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ dReps , ccKeys , dep ⟧
+      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ ⟦ vDelegs , sDelegs , rwds , ddep ⟧ᵈ , stᵖ , ⟦ dReps , ccKeys , dep ⟧ ⟧
           ⇀⦇ deregdrep c d ,GOVCERT⦈
-          ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys , updateCertDeposit pp (deregdrep c d) dep ⟧
+          ⟦ ⟦ vDelegs ∣^ ❴ vDelegCredential c ❵ ᶜ , sDelegs , rwds , ddep ⟧ᵈ , stᵖ , ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys , updateCertDeposit pp (deregdrep c d) dep ⟧ ⟧
 
   GOVCERT-ccreghot :
     ∙ (c , nothing) ∉ ccKeys
     ∙ c ∈ cc
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ dReps , ccKeys , dep ⟧
+      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ stᵈ , stᵖ , ⟦ dReps , ccKeys , dep ⟧ ⟧
           ⇀⦇ ccreghot c mc ,GOVCERT⦈
-          ⟦ dReps , ❴ c , mc ❵ ∪ˡ ccKeys , updateCertDeposit pp (ccreghot c mc) dep ⟧
+          ⟦ stᵈ , stᵖ , ⟦ dReps , ❴ c , mc ❵ ∪ˡ ccKeys , updateCertDeposit pp (ccreghot c mc) dep ⟧ ⟧
 
 data _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → Type where
   CERT-deleg :
@@ -187,9 +188,9 @@ data _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → T
       ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ' , stᵍ ⟧
 
   CERT-vdel :
-    ∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
+    ∙ Γ ⊢ stᶜ ⇀⦇ dCert ,GOVCERT⦈ stᶜ'
       ────────────────────────────────
-      Γ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ , stᵍ' ⟧
+      Γ ⊢ stᶜ ⇀⦇ dCert ,CERT⦈ stᶜ'
 
 data _⊢_⇀⦇_,PRE-CERT⦈_ : CertEnv → CertState → ⊤ → CertState → Type where
 
@@ -206,15 +207,6 @@ data _⊢_⇀⦇_,PRE-CERT⦈_ : CertEnv → CertState → ⊤ → CertState →
       ⇀⦇ _ ,PRE-CERT⦈
       ⟦ ⟦ voteDelegs , stakeDelegs , constMap wdrlCreds 0 ∪ˡ rewards , ddep ⟧ , stᵖ , ⟦ refreshedDReps , ccHotKeys , gdep ⟧ ⟧
 
-data _⊢_⇀⦇_,POST-CERT⦈_ : CertEnv → CertState → ⊤ → CertState → Type where
-
-  CERT-post :
-      ⟦ e , pp , vs , wdrls , cc ⟧
-      ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards , ddep ⟧ , stᵖ , stᵍ ⟧
-        ⇀⦇ _ ,POST-CERT⦈
-        ⟦ ⟦ voteDelegs ∣^ (mapˢ vDelegCredential (dom (GState.dreps stᵍ)) ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ []))
-          , stakeDelegs , rewards , ddep ⟧ , stᵖ , stᵍ ⟧
-
 _⊢_⇀⦇_,CERTS⦈_  : CertEnv → CertState  → List DCert  → CertState  → Type
-_⊢_⇀⦇_,CERTS⦈_ = RunTraceAfterAndThen _⊢_⇀⦇_,PRE-CERT⦈_ _⊢_⇀⦇_,CERT⦈_ _⊢_⇀⦇_,POST-CERT⦈_
+_⊢_⇀⦇_,CERTS⦈_ = RunTraceAfter _⊢_⇀⦇_,PRE-CERT⦈_ _⊢_⇀⦇_,CERT⦈_
 ```

src/Ledger/Conway/Conformance/Certs/Properties.lagda.md

@@ -84,41 +84,41 @@ instance
     rewrite dec-yes (¿ c ∉ dom (DState.rewards ds) × (d ≡ DelegEnv.pparams de .PParams.keyDeposit ⊎ d ≡ 0) ¿) p .proj₂ = refl
 
   Computational-GOVCERT : Computational _⊢_⇀⦇_,GOVCERT⦈_ String
-  Computational-GOVCERT .computeProof ce gs (regdrep c d _) =
-    let open CertEnv ce; open GState gs; open PParams pp in
-    case ¿ (d ≡ drepDeposit × c ∉ dom dreps)
-         ⊎ (d ≡ 0 × c ∈ dom dreps) ¿ of λ where
+  Computational-GOVCERT .computeProof ce cs (regdrep c d _) =
+    let open CertEnv ce; open PParams pp in
+    case ¿ (d ≡ drepDeposit × c ∉ dom (GState.dreps (CertState.gState cs)))
+         ⊎ (d ≡ 0 × c ∈ dom (GState.dreps (CertState.gState cs))) ¿ of λ where
       (yes p) → success (-, GOVCERT-regdrep p)
       (no ¬p) → failure (genErrors ¬p)
-  Computational-GOVCERT .computeProof ce gs (deregdrep c d) =
-    case ¿ c ∈ dom (GState.dreps gs) × (DRepDeposit c , d) ∈  (GState.deposits gs) ¿ of λ where
+  Computational-GOVCERT .computeProof ce cs (deregdrep c d) =
+    case ¿ c ∈ dom (GState.dreps (CertState.gState cs)) × (DRepDeposit c , d) ∈  (GState.deposits (CertState.gState cs)) ¿ of λ where
       (yes p) → success (-, GOVCERT-deregdrep p)
       (no ¬p)  → failure (genErrors ¬p)
-  Computational-GOVCERT .computeProof ce gs (ccreghot c _) =
-    let open CertEnv ce; open GState gs in
-    case ¿ ((c , nothing) ∉ ccHotKeys ˢ) × c ∈ coldCreds ¿ of λ where
+  Computational-GOVCERT .computeProof ce cs (ccreghot c _) =
+    let open CertEnv ce in
+    case ¿ ((c , nothing) ∉ GState.ccHotKeys (CertState.gState cs) ˢ) × c ∈ coldCreds ¿ of λ where
       (yes p) → success (-, GOVCERT-ccreghot p)
       (no ¬p) → failure (genErrors ¬p)
   Computational-GOVCERT .computeProof _ _ _ = failure "Unexpected certificate in GOVCERT"
-  Computational-GOVCERT .completeness ce gs
+  Computational-GOVCERT .completeness ce cs
     (regdrep c d _) _ (GOVCERT-regdrep p)
     rewrite dec-yes
       ¿ (let open CertEnv ce; open PParams pp in
-        (d ≡ drepDeposit × c ∉ dom (GState.dreps gs)) ⊎ (d ≡ 0 × c ∈ dom (GState.dreps gs)))
+        (d ≡ drepDeposit × c ∉ dom (GState.dreps (CertState.gState cs))) ⊎ (d ≡ 0 × c ∈ dom (GState.dreps (CertState.gState cs))))
       ¿ p .proj₂ = refl
-  Computational-GOVCERT .completeness _ gs
+  Computational-GOVCERT .completeness _ cs
     (deregdrep c d) _ (GOVCERT-deregdrep p)
-    rewrite dec-yes ¿ c ∈ dom (GState.dreps gs) × (DRepDeposit c , d) ∈ (GState.deposits gs) ¿ p .proj₂ = refl
-  Computational-GOVCERT .completeness ce gs
+    rewrite dec-yes ¿ c ∈ dom (GState.dreps (CertState.gState cs)) × (DRepDeposit c , d) ∈ (GState.deposits (CertState.gState cs)) ¿ p .proj₂ = refl
+  Computational-GOVCERT .completeness ce cs
     (ccreghot c _) _ (GOVCERT-ccreghot p)
-    rewrite dec-yes (¿ (((c , nothing) ∉ (GState.ccHotKeys gs) ˢ) × c ∈ CertEnv.coldCreds ce) ¿) p .proj₂ = refl
+    rewrite dec-yes (¿ (((c , nothing) ∉ (GState.ccHotKeys (CertState.gState cs)) ˢ) × c ∈ CertEnv.coldCreds ce) ¿) p .proj₂ = refl
 
   Computational-CERT : Computational _⊢_⇀⦇_,CERT⦈_ String
   Computational-CERT .computeProof ce cs dCert
     with computeProof ⟦ CertEnv.pp ce , PState.pools (CertState.pState cs) , dom (GState.dreps (CertState.gState cs)) ⟧
                       (CertState.dState cs) dCert
          | computeProof (CertEnv.pp ce) (CertState.pState cs) dCert
-         | computeProof ce (CertState.gState cs) dCert
+         | computeProof ce cs dCert
   ... | success (_ , h) | _               | _               = success (-, CERT-deleg h)
   ... | failure _       | success (_ , h) | _               = success (-, CERT-pool h)
   ... | failure _       | failure _       | success (_ , h) = success (-, CERT-vdel h)
@@ -151,18 +151,17 @@ instance
     with completeness _ _ _ _ h
   ... | refl = refl
   Computational-CERT .completeness Γ cs
-    dCert@(regdrep c d an)
-    cs' (CERT-vdel h)
-    with computeProof Γ (CertState.gState cs) dCert | completeness _ _ _ _ h
-  ... | success _ | refl = refl
+    (regdrep c d an) _ (CERT-vdel (GOVCERT-regdrep p))
+    rewrite dec-yes
+      ¿ (let open CertEnv Γ; open PParams pp in
+        (d ≡ drepDeposit × c ∉ dom (GState.dreps (CertState.gState cs))) ⊎ (d ≡ 0 × c ∈ dom (GState.dreps (CertState.gState cs))))
+      ¿ p .proj₂ = refl
   Computational-CERT .completeness Γ cs
-    dCert@(deregdrep c _) cs' (CERT-vdel h)
-    with computeProof Γ (CertState.gState cs) dCert | completeness _ _ _ _ h
-  ... | success _ | refl = refl
+    (deregdrep c d) _ (CERT-vdel (GOVCERT-deregdrep p))
+    rewrite dec-yes ¿ c ∈ dom (GState.dreps (CertState.gState cs)) × (DRepDeposit c , d) ∈ (GState.deposits (CertState.gState cs)) ¿ p .proj₂ = refl
   Computational-CERT .completeness Γ cs
-    dCert@(ccreghot c mkh) cs' (CERT-vdel h)
-    with computeProof Γ (CertState.gState cs) dCert | completeness _ _ _ _ h
-  ... | success _ | refl = refl
+    (ccreghot c _) _ (CERT-vdel (GOVCERT-ccreghot p))
+    rewrite dec-yes (¿ (((c , nothing) ∉ (GState.ccHotKeys (CertState.gState cs)) ˢ) × c ∈ CertEnv.coldCreds Γ) ¿) p .proj₂ = refl
 
 
   Computational-PRE-CERT : Computational _⊢_⇀⦇_,PRE-CERT⦈_ String
@@ -181,23 +180,6 @@ instance
                 × mapˢ (map₁ RewardAddress.stake) (CertEnv.wdrls ce ˢ) ⊆ rewards ˢ ¿
         p .proj₂ = refl
 
-  -- POST-CERT has no premises, so computing always succeeds
-  -- with the unique post-state and proof CERT-post.
-  Computational-POST-CERT : Computational _⊢_⇀⦇_,POST-CERT⦈_ String
-  Computational-POST-CERT .computeProof ce cs tt = success ( cs' , CERT-post)
-    where
-      dreps : DReps
-      dreps = GState.dreps (CertState.gState cs)
-      validVoteDelegs : VoteDelegs
-      validVoteDelegs = (DState.voteDelegs (CertState.dState cs)) ∣^ ( mapˢ vDelegCredential (dom dreps) ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ []) )
-      cs' : CertState
-      cs' = ⟦ ⟦ validVoteDelegs , _ , _ ⟧ , CertState.pState cs , CertState.gState cs ⟧
-
-  -- Completeness: the relational proof pins s' to exactly `post`,
-  -- and computeProof returns success at that same state; so refl.
-  Computational-POST-CERT .completeness ce cs _ cs' CERT-post = refl
-
-
 Computational-CERTS : Computational _⊢_⇀⦇_,CERTS⦈_ String
 Computational-CERTS = it
 ```