Cannot register and deregister same stake credential

src/Axiom/Set/Rel.agda

@@ -99,6 +99,9 @@ module _ {x : A} {y : B} where
     dom-single→single : a ∈ dom ❴ x , y ❵ → a ∈ ❴ x ❵
     dom-single→single = to ∈-singleton ∘ from ∈-dom-singleton-pair
 
+    ∈-dom-single≡ : a ∈ dom ❴ x , y ❵ → a ≡ x
+    ∈-dom-single≡ = (from ∈-singleton) ∘ dom-single→single
+
     single→dom-single : a ∈ ❴ x ❵ → a ∈ dom ❴ x , y ❵
     single→dom-single = to ∈-dom-singleton-pair ∘ from ∈-singleton
 

src/Ledger/Certs.lagda

@@ -300,9 +300,12 @@ data
 \begin{code}
   _⊢_⇀⦇_,CERTBASE⦈_  : CertEnv → CertState → ⊤ → CertState → Type
 \end{code}
+\begin{code}[hide]
+module _ where
+\end{code}
 \begin{code}
-_⊢_⇀⦇_,CERTS⦈_     : CertEnv → CertState → List DCert → CertState → Type
-_⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ _⊢_⇀⦇_,CERTBASE⦈_ _⊢_⇀⦇_,CERT⦈_
+  _⊢_⇀⦇_,CERTS⦈_     : CertEnv → CertState → List DCert → CertState → Type
+  _⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ _⊢_⇀⦇_,CERTBASE⦈_ _⊢_⇀⦇_,CERT⦈_
 \end{code}
 \end{AgdaSuppressSpace}
 \caption{Types for the transition systems relating to certificates}
@@ -439,11 +442,7 @@ data _⊢_⇀⦇_,CERTBASE⦈_ where
     ∙ filterˢ isKeyHash wdrlCreds ⊆ dom voteDelegs
     ∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , deps ⟧ᶜ ⊢ ⟦
-        ⟦ voteDelegs , stakeDelegs , rewards ⟧ᵈ , stᵖ , ⟦ dreps , ccHotKeys ⟧ᵛ ⟧ᶜˢ ⇀⦇ _ ,CERTBASE⦈ ⟦
-        ⟦ voteDelegs , stakeDelegs , constMap wdrlCreds 0 ∪ˡ rewards ⟧ᵈ
-        , stᵖ
-        , ⟦ refreshedDReps , ccHotKeys ⟧ᵛ ⟧ᶜˢ
+      ⟦ e , pp , vs , wdrls , deps ⟧ᶜ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards ⟧ᵈ , stᵖ , ⟦ dreps , ccHotKeys ⟧ᵛ ⟧ᶜˢ ⇀⦇ _ ,CERTBASE⦈ ⟦ ⟦ voteDelegs , stakeDelegs , constMap wdrlCreds 0 ∪ˡ rewards ⟧ᵈ , stᵖ , ⟦ refreshedDReps , ccHotKeys ⟧ᵛ ⟧ᶜˢ
 \end{code}
 \end{AgdaSuppressSpace}
 \caption{CERTS rules}

src/Ledger/Conway/Conformance/Certs.agda

@@ -90,20 +90,19 @@ record DelegEnv : Type where
 
 GovCertEnv  = CertEnv
 
-certDeposit : DCert → PParams → DepositPurpose ⇀ Coin
+certDeposit : DCert → PParams → Deposits
 certDeposit (delegate c _ _ v) _   = ❴ CredentialDeposit c , v ❵
 certDeposit (regdrep c v _)    _   = ❴ DRepDeposit c , v ❵
 certDeposit _                  _   = ∅
 -- handled in the Utxo module:
 -- certDeposit (regpool kh _)     pp  = ❴ PoolDeposit kh , pp .poolDeposit ❵
 
 certRefund : DCert → ℙ DepositPurpose
-certRefund (dereg c _)    = ❴ CredentialDeposit c ❵
+certRefund (dereg c _)      = ❴ CredentialDeposit c ❵
 certRefund (deregdrep c _)  = ❴ DRepDeposit c ❵
-certRefund _              = ∅
+certRefund _                = ∅
 
-updateCertDeposit  : PParams → DCert → (DepositPurpose ⇀ Coin)
-                   → DepositPurpose ⇀ Coin
+updateCertDeposit  : PParams → DCert → Deposits → Deposits
 updateCertDeposit pp cert deposits
   = (deposits ∪⁺ certDeposit cert pp) ∣ certRefund cert ᶜ
 

src/Ledger/Epoch.lagda

@@ -122,23 +122,10 @@ open GovActionState using (returnAddr)
 \begin{NoConway}
 \begin{code}
 applyRUpd : RewardUpdate → EpochState → EpochState
-applyRUpd ⟦ Δt , Δr , Δf , rs ⟧ʳᵘ
-  ⟦ ⟦ treasury , reserves ⟧ᵃ
-  , ss
-  , ⟦ ⟦ utxo , fees , deposits , donations ⟧ᵘ
-    , govSt
-    , ⟦ ⟦ voteDelegs , stakeDelegs , rewards ⟧ᵈ , pState , gState ⟧ᶜˢ ⟧ˡ
-  , es
-  , fut
-  ⟧ᵉ' =
-  ⟦ ⟦ posPart (ℤ.+ treasury ℤ.+ Δt ℤ.+ ℤ.+ unregRU')
-    , posPart (ℤ.+ reserves ℤ.+ Δr) ⟧ᵃ
-  , ss
-  , ⟦ ⟦ utxo , posPart (ℤ.+ fees ℤ.+ Δf) , deposits , donations ⟧ᵘ
-    , govSt
-    , ⟦ ⟦ voteDelegs , stakeDelegs , rewards ∪⁺ regRU ⟧ᵈ , pState , gState ⟧ᶜˢ ⟧ˡ
-  , es
-  , fut ⟧ᵉ'
+applyRUpd
+  ⟦ Δt , Δr , Δf , rs ⟧ʳᵘ
+  ⟦ ⟦ treasury , reserves ⟧ᵃ , ss , ⟦ ⟦ utxo , fees , deposits , donations ⟧ᵘ , govSt , ⟦ ⟦ voteDelegs , stakeDelegs , rewards ⟧ᵈ , pState , gState ⟧ᶜˢ ⟧ˡ , es , fut ⟧ᵉ' =
+  ⟦ ⟦ posPart (ℤ.+ treasury ℤ.+ Δt ℤ.+ ℤ.+ unregRU') , posPart (ℤ.+ reserves ℤ.+ Δr) ⟧ᵃ , ss , ⟦ ⟦ utxo , posPart (ℤ.+ fees ℤ.+ Δf) , deposits , donations ⟧ᵘ , govSt , ⟦ ⟦ voteDelegs , stakeDelegs , rewards ∪⁺ regRU ⟧ᵈ , pState , gState ⟧ᶜˢ ⟧ˡ , es , fut ⟧ᵉ'
   where
     regRU     = rs ∣ dom rewards
     unregRU   = rs ∣ dom rewards ᶜ
@@ -246,11 +233,7 @@ its results by carrying out each of the following tasks.
 
       govSt' = filter (λ x → ¿ proj₁ x ∉ mapˢ proj₁ removed' ¿) govSt
 
-      certState' =
-        ⟦ record dState { rewards = dState .rewards ∪⁺ refunds }
-        , ⟦ (pState .pools) ∣ retired ᶜ , (pState .retiring) ∣ retired ᶜ ⟧ᵖ
-        , ⟦ if null govSt' then mapValues (1 +_) (gState .dreps) else (gState .dreps)
-          , (gState .ccHotKeys) ∣ ccCreds (es .cc) ⟧ᵛ ⟧ᶜˢ
+      certState' = ⟦ record dState { rewards = dState .rewards ∪⁺ refunds } , ⟦ (pState .pools) ∣ retired ᶜ , (pState .retiring) ∣ retired ᶜ ⟧ᵖ , ⟦ if null govSt' then mapValues (1 +_) (gState .dreps) else (gState .dreps) , (gState .ccHotKeys) ∣ ccCreds (es .cc) ⟧ᵛ ⟧ᶜˢ
 
       utxoSt' = ⟦ utxoSt .utxo , utxoSt .fees , utxoSt .deposits ∣ mapˢ (proj₁ ∘ proj₂) removedGovActions ᶜ , 0 ⟧ᵘ