Add governance action deposit vote delegation (#101)

src/Ledger/Chain.lagda

@@ -9,6 +9,8 @@ module Ledger.Chain (txs : TransactionStructure) where
 
 open import Ledger.Prelude
 
+open import Algebra
+
 open TransactionStructure txs
 open import Ledger.PParams epochStructure
 open import Ledger.NewPP txs
@@ -41,6 +43,9 @@ record ChainState : Set where
 record Block : Set where
   field ts   : List Tx
         slot : Slot
+
+instance
+  _ = +-0-monoid
 \end{code}
 \caption{Definitions for the NEWEPOCH and CHAIN transition systems}
 \end{figure*}
@@ -55,6 +60,7 @@ private variable
   e : Epoch
   es' : EnactState
   newTally : TallyState
+  rwds : RwdAddr ↛ Coin
 
 -- The NEWEPOCH rule is actually multiple rules in one for the sake of simplicity:
 -- it also does what EPOCH used to do in previous eras
@@ -71,13 +77,15 @@ data _⊢_⇀⦇_,NEWEPOCH⦈_ : NewEpochEnv → NewEpochState → Epoch → New
       pup = PPUpdateState.pup ppup
       acnt' = record acnt { treasury = Acnt.treasury acnt + UTxOState.fees utxoSt }
       retired = retiring ⁻¹ e
-      certState' = record certState { pState = record pState { pools = pools ∣ retired ᶜ ; retiring = retiring ∣ retired ᶜ } }
+      certState' = record certState {
+        pState = record pState { pools = pools ∣ retired ᶜ ; retiring = retiring ∣ retired ᶜ };
+        dState = record dState { rewards = DState.rewards dState ∪⁺ rwds } }
       ls' = record ls { tally = newTally ; utxoSt = record utxoSt { fees = 0 } ; certState = certState' }
     in
     e ≡ sucᵉ lastEpoch
     → record { currentEpoch = e ; ccHotKeys = VState.ccHotKeys vState ; NewEpochEnv Γ }
-                    ⊢                               ⟦ es  , [] ⟧ʳ
-                    ⇀⦇ setToList (tally ˢ) ,RATIFY⦈ ⟦ es' , setToList (newTally ˢ) ⟧ʳ
+                    ⊢                               ⟦ es  , [] , ∅ᵐ ⟧ʳ
+                    ⇀⦇ setToList (tally ˢ) ,RATIFY⦈ ⟦ es' , setToList (newTally ˢ) , rwds ⟧ʳ
     -- TODO: remove keys that aren't in the CC from the hot key map
     ────────────────────────────────
     Γ ⊢ nes ⇀⦇ e ,NEWEPOCH⦈ ⟦ e , acnt' , ls' , es' ⟧ⁿᵉ

src/Ledger/Deleg.lagda

@@ -46,11 +46,12 @@ DelegEnv  = PParams
 PoolEnv   = PParams
 
 record DState : Set where
-  constructor ⟦_,_⟧ᵈ
+  constructor ⟦_,_,_⟧ᵈ
   field voteDelegs      : Credential ↛ VDeleg
   --    ^ stake credential to DRep credential
         stakeDelegs     : Credential ↛ Credential
   --    ^ stake credential to pool credential
+        rewards         : RwdAddr ↛ Coin
 
 record PState : Set where
   constructor ⟦_,_⟧ᵖ
@@ -77,6 +78,7 @@ private variable
   sDelegs : Credential ↛ Credential
   retiring retiring' : Credential ↛ Epoch
   ccKeys : KeyHash ↛ Maybe KeyHash
+  rwds : RwdAddr ↛ Coin
   dCert : DCert
   c c' : Credential
   mc : Maybe Credential
@@ -115,8 +117,8 @@ data _⊢_⇀⦇_,DELEG⦈_ : DelegEnv → DState → DCert → DState → Set w
   DELEG-delegate :
     d ≡ requiredVDelegDeposit pp mv ⊔ requiredDeposit pp mc
     ────────────────────────────────
-    pp ⊢ ⟦ vDelegs , sDelegs ⟧ᵈ ⇀⦇ delegate c mv mc d ,DELEG⦈
-         ⟦ insertIfPresent c mv vDelegs , insertIfPresent c mc sDelegs ⟧ᵈ
+    pp ⊢ ⟦ vDelegs , sDelegs , rwds ⟧ᵈ ⇀⦇ delegate c mv mc d ,DELEG⦈
+         ⟦ insertIfPresent c mv vDelegs , insertIfPresent c mc sDelegs ,rwds ⟧ᵈ
 
 data _⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Set where
   POOL-regpool : let open PParams pp ; open PoolParams poolParams in
@@ -180,23 +182,23 @@ open import Tactic.ReduceDec
 open import MyDebugOptions
 
 Computational-DELEG : Computational _⊢_⇀⦇_,DELEG⦈_
-Computational-DELEG .compute pp ⟦ vDelegs , sDelegs ⟧ᵈ (delegate c mv mc d) =
+Computational-DELEG .compute pp ⟦ vDelegs , sDelegs , rewards ⟧ᵈ (delegate c mv mc d) =
   ifᵈ d ≡ requiredVDelegDeposit pp mv ⊔ requiredDeposit pp mc
-    then just ⟦ insertIfPresent c mv vDelegs , insertIfPresent c mc sDelegs ⟧ᵈ
+    then just ⟦ insertIfPresent c mv vDelegs , insertIfPresent c mc sDelegs , rewards ⟧ᵈ
     else nothing
 Computational-DELEG .compute Γ s _ = nothing
-Computational-DELEG .≡-just⇔STS {pp} {⟦ s₁ , s₂ ⟧ᵈ} {cert} {s'} = mk⇔
-  (case cert return (λ c → compute Computational-DELEG pp ⟦ s₁ , s₂ ⟧ᵈ c ≡ just s' → pp ⊢ ⟦ s₁ , s₂ ⟧ᵈ ⇀⦇ c ,DELEG⦈ s') of λ where
+Computational-DELEG .≡-just⇔STS {pp} {⟦ s₁ , s₂ , rewards ⟧ᵈ} {cert} {s'} = mk⇔
+  (case cert return (λ c → compute Computational-DELEG pp ⟦ s₁ , s₂ , rewards ⟧ᵈ c ≡ just s' → pp ⊢ ⟦ s₁ , s₂ , rewards ⟧ᵈ ⇀⦇ c ,DELEG⦈ s') of λ where
     (delegate c mv mc d) h → case d ≟ requiredVDelegDeposit pp mv ⊔ requiredDeposit pp mc of λ where
-      (yes p) → subst _ (just-injective $ by-reduceDec h) (DELEG-delegate {mv = mv} {mc} {s₁} {s₂} {c} p)
+      (yes p) → subst _ (just-injective $ by-reduceDec h) (DELEG-delegate {mv = mv} {mc} {s₁} {s₂} {rewards} {c} p)
       (no ¬p) → case by-reduceDec h of λ ()
     (regpool x x₁) → λ ()
     (retirepool x x₁) → λ ()
-    (regdrep x x₁ _) → λ ()
+    (regdrep x x₁) → λ ()
     (deregdrep x) → λ ()
     (ccreghot x x₁) → λ ())
-  (λ where (DELEG-delegate {mv = mv} {mc} {vDelegs} {sDelegs} {c} h) → by-reduceDecInGoal
-             (refl {x = just ⟦ insertIfPresent c mv vDelegs , insertIfPresent c mc sDelegs ⟧ᵈ}))
+  (λ where (DELEG-delegate {mv = mv} {mc} {vDelegs} {sDelegs} {rwds} {c} h) → by-reduceDecInGoal
+             (refl {x = just ⟦ insertIfPresent c mv vDelegs , insertIfPresent c mc sDelegs , rewards ⟧ᵈ}))
 
 --Computational-CERTS : Computational _⊢_⇀⦇_,CERTS⦈_
 --Computational-CERTS .compute     = {!!}

src/Ledger/Ratify.lagda

@@ -27,6 +27,7 @@ _∧_ = _×_
 
 instance
   _ = +-0-commutativeMonoid
+  _ = +-0-monoid
 \end{code}
 \begin{figure*}[h]
 \begin{code}
@@ -39,9 +40,10 @@ record RatifyEnv : Set where
         ccHotKeys     : KeyHash ↛ Maybe KeyHash
 
 record RatifyState : Set where
-  constructor ⟦_,_⟧ʳ
-  field es      : EnactState
-        future  : List (GovActionID × GovActionState)
+  constructor ⟦_,_,_⟧ʳ
+  field es              : EnactState
+        future          : List (GovActionID × GovActionState)
+        depositReturns  : RwdAddr ↛ Coin
 \end{code}
 \caption{Types and functions for the RATIFY transition system}
 \end{figure*}
@@ -215,31 +217,32 @@ private variable
   upd : PParamsUpdate
   a : GovActionID × GovActionState
   f f' l : List (GovActionID × GovActionState)
+  rwds : RwdAddr ↛ Coin
 
 data _⊢_⇀⦇_,RATIFY'⦈_ : RatifyEnv → RatifyState → GovActionID × GovActionState → RatifyState → Set where
 \end{code}
 \begin{figure*}[h]
 \begin{code}
-  RATIFY-Accept : let open RatifyEnv Γ in
+  RATIFY-Accept : let open RatifyEnv Γ; open GovActionState (proj₂ a) in
     accepted Γ es (proj₂ a)
     → _ ⊢ es ⇀⦇ GovActionState.action (proj₂ a) ,ENACT⦈ es'
     ────────────────────────────────
-    Γ ⊢ ⟦ es , f ⟧ʳ ⇀⦇ a ,RATIFY'⦈ ⟦ es' , f ⟧ʳ
+    Γ ⊢ ⟦ es , f , rwds ⟧ʳ ⇀⦇ a ,RATIFY'⦈ ⟦ es' , f , rwds ∪⁺ ❴ returnAddr , deposit ❵ᵐ ⟧ʳ
 
   -- remove expired actions
   -- NOTE: don't have to remove actions that can never be accpted because of sufficient no votes
-  RATIFY-Reject : let open RatifyEnv Γ in
+  RATIFY-Reject : let open RatifyEnv Γ; open GovActionState (proj₂ a) in
     ¬ accepted Γ es (proj₂ a)
     → expired currentEpoch (proj₂ a)
     ────────────────────────────────
-    Γ ⊢ ⟦ es , f ⟧ʳ ⇀⦇ a ,RATIFY'⦈ ⟦ es , f ⟧ʳ
+    Γ ⊢ ⟦ es , f , rwds ⟧ʳ ⇀⦇ a ,RATIFY'⦈ ⟦ es , f , rwds ∪⁺ ❴ returnAddr , deposit ❵ᵐ ⟧ʳ
 
   -- continue voting in the next epoch
   RATIFY-Continue : let open RatifyEnv Γ in
     ¬ accepted Γ es (proj₂ a)
     → ¬ expired currentEpoch (proj₂ a)
     ────────────────────────────────
-    Γ ⊢ ⟦ es , f ⟧ʳ ⇀⦇ a ,RATIFY'⦈ ⟦ es , a ∷ f ⟧ʳ
+    Γ ⊢ ⟦ es , f , rwds ⟧ʳ ⇀⦇ a ,RATIFY'⦈ ⟦ es , a ∷ f , rwds ⟧ʳ
 
 _⊢_⇀⦇_,RATIFY⦈_ : RatifyEnv → RatifyState → List (GovActionID × GovActionState) → RatifyState → Set
 _⊢_⇀⦇_,RATIFY⦈_ = SS⇒BS (λ where (Γ , _) → Γ ⊢_⇀⦇_,RATIFY'⦈_)

src/Ledger/Utxo.lagda

@@ -94,6 +94,7 @@ data DepositPurpose : Set where
   CredentialDeposit  : DepositPurpose
   PoolDeposit        : DepositPurpose
   DRepDeposit        : DepositPurpose
+  GovActionDeposit   : DepositPurpose
 
 certDeposit : PParams → DCert → Maybe (DepositPurpose × Credential × Coin)
 certDeposit _  (delegate c _ _ v)  = just (CredentialDeposit , c , v)
@@ -114,6 +115,10 @@ certRefund _                               = nothing
 certRefundˢ : DCert → ℙ (DepositPurpose × Credential)
 certRefundˢ = partialToSet certRefund
 
+propDepositᵐ : GovProposal → (DepositPurpose × Credential) ↛ Coin
+propDepositᵐ record { deposit = d ; returnAddr = record { stake = c } }
+  = ❴ (GovActionDeposit , c) , d ❵ᵐ
+
 -- txDeposits : TxBody → (DepositPurpose × Credential) ↛ Coin
 -- txDeposits = foldr _∪⁺_ ∅ᵐ ∘ List.map certDepositᵐ ∘ txcerts
 
@@ -153,24 +158,36 @@ record UTxOState : Set where
         fees      : Coin
         deposits  : (DepositPurpose × Credential) ↛ Coin
 
-updateDeposits : PParams → List DCert → (DepositPurpose × Credential) ↛ Coin → (DepositPurpose × Credential) ↛ Coin
-updateDeposits _  []              deposits = deposits
-updateDeposits pp (cert ∷ certs)  deposits =
-  ((updateDeposits pp certs deposits) ∪⁺ certDepositᵐ pp cert) ∣ certRefundˢ cert ᶜ
+updateCertDeposits : PParams → List DCert → (DepositPurpose × Credential) ↛ Coin → (DepositPurpose × Credential) ↛ Coin
+updateCertDeposits _  []              deposits = deposits
+updateCertDeposits pp (cert ∷ certs)  deposits =
+  ((updateCertDeposits pp certs deposits) ∪⁺ certDepositᵐ pp cert) ∣ certRefundˢ cert ᶜ
+
+updateProposalDeposits : List GovProposal → (DepositPurpose × Credential) ↛ Coin → (DepositPurpose × Credential) ↛ Coin
+updateProposalDeposits [] deposits = deposits
+updateProposalDeposits (prop ∷ props) deposits = (updateProposalDeposits props deposits) ∪⁺ propDepositᵐ prop
+
+updateDeposits : PParams → TxBody → (DepositPurpose × Credential) ↛ Coin → (DepositPurpose × Credential) ↛ Coin
+updateDeposits pp txb = updateCertDeposits pp (txcerts txb) ∘ updateProposalDeposits (txprop txb)
 
-depositsChange : PParams → List DCert → (DepositPurpose × Credential) ↛ Coin → ℤ
-depositsChange pp certs deposits = getCoin (updateDeposits pp certs deposits) ⊖ getCoin deposits
+proposalDeposits : TxBody → ℕ
+proposalDeposits txb = sum $ List.map GovProposal.deposit (txprop txb)
+
+depositsChange : PParams → TxBody → (DepositPurpose × Credential) ↛ Coin → ℤ
+depositsChange pp txb deposits = getCoin (updateDeposits pp txb deposits) ⊖ getCoin deposits
 
 -- refundedDeposits : TxBody → ℙ (DepositPurpose × Credential)
 -- refundedDeposits = mapPartial certRefund ∘ fromList ∘ txcerts
 
 depositRefunds : PParams → UTxOState → TxBody → Coin
-depositRefunds pp st txb = negPart $ depositsChange pp (txcerts txb) deposits
+depositRefunds pp st txb = negPart $ depositsChange pp txb deposits
   where open UTxOState st
 
 newDeposits : PParams → UTxOState → TxBody → Coin
-newDeposits pp st txb = posPart $ depositsChange pp (txcerts txb) deposits
-  where open UTxOState st
+newDeposits pp st txb = certDeposits
+  where
+    open UTxOState st
+    certDeposits = posPart $ depositsChange pp txb deposits
 
 consumed : PParams → UTxOState → TxBody → Value
 consumed pp st txb = balance (UTxOState.utxo st ∣ txins txb)
@@ -270,8 +287,7 @@ data _⊢_⇀⦇_,UTXO⦈_ where
     Γ ⊢ s ⇀⦇ tx ,UTXO⦈
         ⟦ (utxo ∣ txins tx ᶜ) ∪ᵐˡ outs tx
         , fees + f
-        , updateDeposits pp (txcerts tx) deposits
-        ⟧ᵘ
+        , updateDeposits pp tx deposits ⟧ᵘ
 \end{code}
 \begin{code}[hide]
 -- TODO: This can't be moved into Properties because it breaks. Move

src/Ledger/Utxo/Properties.lagda

@@ -128,8 +128,8 @@ module DepositHelpers
 
   private
     dep = getCoin deposits
-    uDep = getCoin (updateDeposits pp (txcerts tx) deposits)
-    Δdep = depositsChange pp (txcerts tx) deposits
+    uDep = getCoin (updateDeposits pp tx deposits)
+    Δdep = depositsChange pp tx deposits
     ref = depositRefunds pp ⟦ utxo , fees , deposits ⟧ᵘ tx
     tot = newDeposits    pp ⟦ utxo , fees , deposits ⟧ᵘ tx