Add deposits in CERT

Author: carlostome

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

@@ -31,16 +31,6 @@ record StakePoolParams : Type where
     pledge          : Coin
     rewardAccount   : Credential
 
--- Deposit Types
-data DepositPurpose : Type where
-  CredentialDeposit  : Credential   → DepositPurpose
-  PoolDeposit        : KeyHash      → DepositPurpose
-  DRepDeposit        : Credential   → DepositPurpose
-  GovActionDeposit   : GovActionID  → DepositPurpose
-
-Deposits : Type
-Deposits = DepositPurpose ⇀ Coin
-
 -- Miscellaneous Type Aliases
 
 CCHotKeys : Type
@@ -73,12 +63,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 +73,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 +88,21 @@ record DState : Type where
     voteDelegs   : VoteDelegs
     stakeDelegs  : StakeDelegs
     rewards      : Rewards
+    deposits     : Credential ⇀ Coin
 
 record PState : Type where
   field
     pools     : Pools
     fPools    : Pools
     retiring  : KeyHash ⇀ Epoch
+    deposits  : KeyHash ⇀ Coin
 
 record GState : Type where
   constructor ⟦_,_⟧ᵛ
   field
     dreps      : DReps
     ccHotKeys  : Credential ⇀ Maybe Credential
+    deposits   : Credential ⇀ Coin
 
 record CertState : Type where
   constructor ⟦_,_,_⟧ᶜˢ
@@ -139,19 +118,12 @@ record DelegEnv : Type where
     delegatees    : ℙ Credential
 ```
 
-
-
-
 <!--
 ```agda
-record HasDeposits {a} (A : Type a) : Type a where
-  field DepositsOf : A → Deposits
+record HasDeposits (A : Type) {K : Type} : Type where
+  field DepositsOf : A → K ⇀ Coin
 open HasDeposits ⦃...⦄ public
 
-instance
-  unquoteDecl DecEq-DepositPurpose = derive-DecEq
-    ((quote DepositPurpose , DecEq-DepositPurpose) ∷ [])
-
 record HasCCHotKeys {a} (A : Type a) : Type a where
   field CCHotKeysOf : A → CCHotKeys
 open HasCCHotKeys ⦃...⦄ public
@@ -208,9 +180,15 @@ instance
   HasRewards-DState : HasRewards DState
   HasRewards-DState .RewardsOf = DState.rewards
 
+  HasDeposits-DState : HasDeposits DState
+  HasDeposits-DState .DepositsOf = DState.deposits
+
   HasPools-PState : HasPools PState
   HasPools-PState .PoolsOf = PState.pools
 
+  HasDeposits-PState : HasDeposits PState
+  HasDeposits-PState .DepositsOf = PState.deposits
+
   HasRetiring-PState : HasRetiring PState
   HasRetiring-PState .RetiringOf = PState.retiring
 
@@ -220,6 +198,9 @@ instance
   HasCCHotKeys-GState : HasCCHotKeys GState
   HasCCHotKeys-GState .CCHotKeysOf = GState.ccHotKeys
 
+  HasDeposits-GState : HasDeposits GState
+  HasDeposits-GState .DepositsOf = GState.deposits
+
   HasDState-CertState : HasDState CertState
   HasDState-CertState .DStateOf = CertState.dState
 
@@ -265,6 +246,8 @@ private variable
   pools fPools           : Pools
   retiring               : Retiring
   wdrls                  : Withdrawals
+  A                      : Type
+  deposits deposits'     : A ⇀ Coin
 
   an          : Anchor
   Γ           : CertEnv
@@ -314,19 +297,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 ∪⁺ ❴ 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 ∣ ❴ c ❵ ᶜ ⟧
 
 
 isPoolRegistered : Pools -> KeyHash -> Maybe StakePoolParams
@@ -335,32 +311,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 ∪ˡ ❴ 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 +359,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 ∪⁺ ❴ 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 ∣ ❴ 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 +385,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 +405,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 +416,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 --

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

@@ -165,6 +165,20 @@ rmOrphanDRepVotes cs govSt = L.map (map₂ go) govSt
 allColdCreds : GovState → EnactState → ℙ Credential
 allColdCreds govSt es =
   ccCreds (es .cc) ∪ concatMapˢ (λ (_ , st) → proposedCC (GovActionOf st)) (fromList govSt)
+
+calculateDepositsChange : CertState → CertState → ℤ
+calculateDepositsChange certState certState' = initialCoin - finalCoin
+  where
+    initialCoin : ℕ
+    initialCoin = getCoin (DepositsOf (DStateOf certState))
+                  + getCoin (DepositsOf (PStateOf certState))
+                  + getCoin (DepositsOf (GStateOf certState))
+
+    finalCoin : ℕ
+    finalCoin = getCoin (DepositsOf (DStateOf certState'))
+                + getCoin (DepositsOf (PStateOf certState'))
+                + getCoin (DepositsOf (GStateOf certState'))
+
 ```
 
 -- ## <span class="AgdaDatatype">LEDGER</span> Transition System
@@ -178,6 +192,7 @@ private variable
   utxo₀                 : UTxO
   govState govState'    : GovState
   certState certState'  : CertState
+  depositsChange        : ℤ
   stx                   : SubLevelTx
   slot                  : Slot
   ppolicy               : Maybe ScriptHash
@@ -246,12 +261,15 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LState → TopLevelTx → LState 
 
          allData : DataHash ⇀ Datum
          allData = setToMap (mapˢ < hash , id > (getAllData tx utxo₀))
+
+         depositsChange : ℤ
+         depositsChange = calculateDepositsChange certState certState''
     in
-      ∙ Tx.isValid tx ≡ true
-      ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , Tx.isValid tx , allScripts , allData ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState' , govState' , certState' ⟧
-      ∙ ⟦ slot , pp , treasury , utxo₀ , Tx.isValid tx , allScripts , allData ⟧  ⊢ utxoState' ⇀⦇ tx ,UTXOW⦈ utxoState''
+      ∙ IsValidFlagOf tx ≡ true
+      ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , IsValidFlagOf tx , allScripts , allData ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState' , govState' , certState' ⟧
       ∙ ⟦ epoch slot , pp , ListOfGovVotesOf tx , WithdrawalsOf tx , allColdCreds govState enactState ⟧ ⊢ certState' ⇀⦇ DCertsOf tx ,CERTS⦈ certState''
       ∙ ⟦ TxIdOf tx , epoch slot , pp , ppolicy , enactState , certState' , dom (RewardsOf certState) ⟧ ⊢ rmOrphanDRepVotes certState' govState ⇀⦇ GovProposals+Votes tx ,GOVS⦈ govState'
+      ∙ ⟦ slot , pp , treasury , utxo₀ , IsValidFlagOf tx , depositsChange , allScripts , allData ⟧  ⊢ utxoState' ⇀⦇ tx ,UTXOW⦈ utxoState''
       ────────────────────────────────
       ⟦ slot , ppolicy , pp , enactState , treasury ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ tx ,LEDGER⦈ ⟦ utxoState'' , govState'' , certState'' ⟧
 
@@ -264,23 +282,14 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LState → TopLevelTx → LState 
          allData : DataHash ⇀ Datum
          allData = setToMap (mapˢ < hash , id > (getAllData tx utxo₀))
     in
-      ∙ Tx.isValid tx ≡ false
-      ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , Tx.isValid tx , allScripts , allData ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ SubTransactionsOf tx  ,SUBLEDGERS⦈ ⟦ utxoState , govState , certState ⟧
-      ∙ ⟦ slot , pp , treasury , utxo₀ , Tx.isValid tx , allScripts , allData ⟧ ⊢ utxoState ⇀⦇ tx ,UTXOW⦈ utxoState'
+      ∙ IsValidFlagOf tx ≡ false
+      ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , IsValidFlagOf tx , allScripts , allData ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ SubTransactionsOf tx  ,SUBLEDGERS⦈ ⟦ utxoState , govState , certState ⟧
+      ∙ ⟦ slot , pp , treasury , utxo₀ , IsValidFlagOf tx , 0ℤ , allScripts , allData ⟧ ⊢ utxoState ⇀⦇ tx ,UTXOW⦈ utxoState'
       ────────────────────────────────
       ⟦ slot , ppolicy , pp , enactState , treasury ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ tx ,LEDGER⦈ ⟦ utxoState' , govState , certState ⟧
 ```
 
--- <!--
--- ```agda
--- pattern LEDGER-V⋯ w x y z = LEDGER-V (w , x , y , z)
--- pattern LEDGER-I⋯ y z     = LEDGER-I (y , z)
--- ```
--- -->
-
--- ## <span class="AgdaDatatype">LEDGERS</span> Transition System
-
--- ```agda
--- _⊢_⇀⦇_,LEDGERS⦈_ : LEnv → LState → List Tx → LState → Type
--- _⊢_⇀⦇_,LEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,LEDGER⦈_}
--- ```
+```agda
+_⊢_⇀⦇_,LEDGERS⦈_ : LedgerEnv → LState → List TopLevelTx → LState → Type
+_⊢_⇀⦇_,LEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,LEDGER⦈_}
+```

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

@@ -372,13 +372,20 @@ could be either of them.
     field TxOutsOf : A → Ix ⇀ TxOut
   open HasTxOuts ⦃...⦄ public
 
+  record HasIsValidFlag {a} (A : Type a) : Type a where
+    field IsValidFlagOf : A → Bool
+  open HasIsValidFlag ⦃...⦄ public
+
   instance
     HasTxBody-Tx : HasTxBody (Tx txLevel)
     HasTxBody-Tx .TxBodyOf = Tx.txBody
 
     HasTxWitnesses-Tx : HasTxWitnesses (Tx txLevel)
     HasTxWitnesses-Tx .TxWitnessesOf = Tx.txWitnesses
 
+    HasIsValidFlag-Tx : HasIsValidFlag TopLevelTx
+    HasIsValidFlag-Tx .IsValidFlagOf = Tx.isValid
+
     HasRedeemers-TxWitnesses : HasRedeemers (TxWitnesses txLevel)
     HasRedeemers-TxWitnesses .RedeemersOf = TxWitnesses.txRedeemers