Add deposits in CERT

Author: carlostome

src/Ledger/Dijkstra/Specification/Certs.lagda.md

@@ -73,12 +73,6 @@ data DCert : Type where
   regdrep     : Credential → Coin → Anchor → DCert
   deregdrep   : Credential → Coin → DCert
   ccreghot    : Credential → Maybe Credential → DCert
-  -- The `reg` cert is deprecated in Conway, but it's still present in this era
-  -- for backwards compatibility. This has been added to the spec to make
-  -- conformance testing work properly. We don't talk about this certificate
-  -- in the docs because it has been deprecated and we want to discourage people
-  -- from using it.
-  reg         : Credential → Coin → DCert
 
 cwitness : DCert → Maybe Credential
 cwitness (delegate c _ _ _)  = just c
@@ -89,14 +83,6 @@ cwitness (regdrep c _ _)     = just c
 cwitness (deregdrep c _)     = just c
 cwitness (ccreghot c _)      = just c
 
--- The implementation requires the `reg` cert to be witnessed only if the
--- deposit is set. There didn't use to be a field for the deposit, but that was
--- added in the Conway era to make it easier to determine, just by looking at
--- the transaction, how much deposit was paid for that certificate.
-cwitness (reg _ zero)        = nothing
-cwitness (reg c (suc _))     = just c
-
-
 -- Certification Types
 record CertEnv : Type where
   field
@@ -112,18 +98,21 @@ record DState : Type where
     voteDelegs   : VoteDelegs
     stakeDelegs  : StakeDelegs
     rewards      : Rewards
+    deposits     : Deposits
 
 record PState : Type where
   field
     pools     : Pools
     fPools    : Pools
     retiring  : KeyHash ⇀ Epoch
+    deposits  : Deposits
 
 record GState : Type where
   constructor ⟦_,_⟧ᵛ
   field
     dreps      : DReps
     ccHotKeys  : Credential ⇀ Maybe Credential
+    deposits   : Deposits
 
 record CertState : Type where
   constructor ⟦_,_,_⟧ᶜˢ
@@ -139,9 +128,6 @@ record DelegEnv : Type where
     delegatees    : ℙ Credential
 ```
 
-
-
-
 <!--
 ```agda
 record HasDeposits {a} (A : Type a) : Type a where
@@ -265,6 +251,7 @@ private variable
   pools fPools           : Pools
   retiring               : Retiring
   wdrls                  : Withdrawals
+  deposits deposits'     : Deposits
 
   an          : Anchor
   Γ           : CertEnv
@@ -314,19 +301,12 @@ data _⊢_⇀⦇_,DELEG⦈_ : DelegEnv → DState → DCert → DState → Type
             fromList ( nothing ∷ just vDelegAbstain ∷ just vDelegNoConfidence ∷ [] )
     ∙ mkh ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵
       ────────────────────────────────
-      ⟦ pp , pools , delegatees ⟧ ⊢ ⟦ vDelegs , sDelegs , rwds ⟧ ⇀⦇ delegate c mvd mkh d ,DELEG⦈ ⟦ insertIfJust c mvd vDelegs , insertIfJust c mkh sDelegs , rwds ∪ˡ ❴ c , 0 ❵ ⟧
+      ⟦ pp , pools , delegatees ⟧ ⊢ ⟦ vDelegs , sDelegs , rwds , deposits ⟧ ⇀⦇ delegate c mvd mkh d ,DELEG⦈ ⟦ insertIfJust c mvd vDelegs , insertIfJust c mkh sDelegs , rwds ∪ˡ ❴ c , 0 ❵ , deposits ∪⁺ ❴ CredentialDeposit c , d ❵ ⟧
 
   DELEG-dereg :
     ∙ (c , 0) ∈ rwds
       ────────────────────────────────
-      ⟦ pp , pools , delegatees ⟧ ⊢ ⟦ vDelegs , sDelegs , rwds ⟧ ⇀⦇ dereg c md ,DELEG⦈ ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧
-
-  DELEG-reg :
-    ∙ c ∉ dom rwds
-    ∙ d ≡ pp .keyDeposit ⊎ d ≡ 0
-      ────────────────────────────────
-      ⟦ pp , pools , delegatees ⟧ ⊢ ⟦ vDelegs , sDelegs , rwds ⟧ ⇀⦇ reg c d ,DELEG⦈ ⟦ vDelegs , sDelegs , rwds ∪ˡ ❴ c , 0 ❵ ⟧
-
+      ⟦ pp , pools , delegatees ⟧ ⊢ ⟦ vDelegs , sDelegs , rwds , deposits ⟧ ⇀⦇ dereg c md ,DELEG⦈ ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ , deposits ∣ ❴ CredentialDeposit c ❵ ᶜ ⟧
 
 
 isPoolRegistered : Pools -> KeyHash -> Maybe StakePoolParams
@@ -335,32 +315,45 @@ isPoolRegistered ps kh = lookupᵐ? ps kh
 -- Auxiliary POOL transition system --
 data _⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Type where
 
-  POOL-regpool :
-    let
-      fPool' =
-        if isPoolRegistered pools kh
-          then ❴ kh , poolParams ❵ ∪ˡ fPools
-          else fPools
-     in
+  POOL-reg :
+    ∙ Is-just (isPoolRegistered pools kh)
     ────────────────────────────────
     pp ⊢ ⟦ pools
          , fPools
          , retiring
+         , deposits
          ⟧ ⇀⦇ regpool kh poolParams ,POOL⦈ ⟦
            pools ∪ˡ ❴ kh , poolParams ❵
-         , fPool'
-         , retiring ∣  ❴ kh ❵ ᶜ
+         , fPools
+         , retiring
+         , deposits ∪⁺ ❴ PoolDeposit kh , pp .poolDeposit ❵
+         ⟧
+
+  POOL-rereg :
+    ∙ Is-nothing (isPoolRegistered pools kh)
+    ────────────────────────────────
+    pp ⊢ ⟦ pools
+         , fPools
+         , retiring
+         , deposits
+         ⟧ ⇀⦇ regpool kh poolParams ,POOL⦈ ⟦
+           pools
+         , ❴ kh , poolParams ❵ ∪ˡ fPools
+         , retiring ∣ ❴ kh ❵ ᶜ
+         , deposits
          ⟧
 
   POOL-retirepool :
     ────────────────────────────────
     pp ⊢ ⟦ pools
          , fPools
          , retiring
+         , deposits
          ⟧ ⇀⦇ retirepool kh e ,POOL⦈ ⟦
            pools
          , fPools
          , ❴ kh , e ❵ ∪ˡ retiring
+         , deposits
          ⟧
 
 
@@ -370,18 +363,18 @@ data _⊢_⇀⦇_,GOVCERT⦈_ : CertEnv → GState → DCert → GState → Type
   GOVCERT-regdrep :
     ∙ (d ≡ pp .drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps)
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ dReps , ccKeys ⟧ ⇀⦇ regdrep c d an ,GOVCERT⦈ ⟦ ❴ c , e + pp .drepActivity ❵ ∪ˡ dReps , ccKeys ⟧
+      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ dReps , ccKeys , deposits ⟧ ⇀⦇ regdrep c d an ,GOVCERT⦈ ⟦ ❴ c , e + pp .drepActivity ❵ ∪ˡ dReps , ccKeys , deposits ∪⁺ ❴ DRepDeposit c , d ❵ ⟧
 
   GOVCERT-deregdrep :
     ∙ c ∈ dom dReps
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ dReps , ccKeys ⟧ ⇀⦇ deregdrep c d ,GOVCERT⦈ ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys ⟧
+      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ dReps , ccKeys , deposits ⟧ ⇀⦇ deregdrep c d ,GOVCERT⦈ ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys , deposits ∣ ❴ DRepDeposit c ❵ ᶜ ⟧
 
   GOVCERT-ccreghot :
     ∙ (c , nothing) ∉ ccKeys
     ∙ c ∈ cc
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ dReps , ccKeys ⟧ ⇀⦇ ccreghot c mc ,GOVCERT⦈ ⟦ dReps , ❴ c , mc ❵ ∪ˡ ccKeys ⟧
+      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ dReps , ccKeys , deposits ⟧ ⇀⦇ ccreghot c mc ,GOVCERT⦈ ⟦ dReps , ❴ c , mc ❵ ∪ˡ ccKeys , deposits ⟧
 
 -- CERT Transition System --
 data _⊢_⇀⦇_,CERT⦈_  : CertEnv → CertState → DCert → CertState → Type where
@@ -396,7 +389,7 @@ data _⊢_⇀⦇_,CERT⦈_  : CertEnv → CertState → DCert → CertState →
       ────────────────────────────────
       ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ' , stᵍ ⟧
 
-  CERT-vdel :
+  CERT-gov :
     ∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
       ────────────────────────────────
       Γ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ , stᵍ' ⟧
@@ -416,7 +409,7 @@ data _⊢_⇀⦇_,PRE-CERT⦈_ : CertEnv → CertState → ⊤ → CertState →
     ∙ filter isKeyHash wdrlCreds ⊆ dom voteDelegs
     ∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards ⟧ , stᵖ , ⟦ dReps , ccHotKeys ⟧ ⟧ ⇀⦇ _ ,PRE-CERT⦈ ⟦ ⟦ voteDelegs , stakeDelegs , constMap wdrlCreds 0 ∪ˡ rewards ⟧ , stᵖ , ⟦ refreshedDReps , ccHotKeys ⟧ ⟧
+      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards , deposits ⟧ , stᵖ , ⟦ dReps , ccHotKeys , deposits' ⟧ ⟧ ⇀⦇ _ ,PRE-CERT⦈ ⟦ ⟦ voteDelegs , stakeDelegs , constMap wdrlCreds 0 ∪ˡ rewards , deposits ⟧ , stᵖ , ⟦ refreshedDReps , ccHotKeys , deposits' ⟧ ⟧
 
 
 -- POST-CERT Transition Rule --
@@ -427,7 +420,7 @@ data _⊢_⇀⦇_,POST-CERT⦈_ : CertEnv → CertState → ⊤ → CertState 
     let activeVDelegs = mapˢ vDelegCredential (dom (DRepsOf stᵍ))
                          ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ [])
     in
-      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards ⟧ , stᵖ , stᵍ ⟧ ⇀⦇ _ ,POST-CERT⦈ ⟦ ⟦ voteDelegs ∣^ activeVDelegs , stakeDelegs , rewards ⟧ , stᵖ , stᵍ ⟧
+      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards , deposits ⟧ , stᵖ , stᵍ ⟧ ⇀⦇ _ ,POST-CERT⦈ ⟦ ⟦ voteDelegs ∣^ activeVDelegs , stakeDelegs , rewards , deposits ⟧ , stᵖ , stᵍ ⟧
 
 
 -- CERTS Transition System --