Thread rewards0 from Ledger

Author: carlostome

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

@@ -33,12 +33,20 @@ record EntitiesEnv : Type where
     coldCredentials         : ℙ Credential
     legacyMode              : Bool
     rewards₀                : Rewards
+
+record SubEntitiesEnv : Type where
+  field
+    epoch                   : Epoch
+    pp                      : PParams
+    coldCredentials         : ℙ Credential
+    rewards₀                : Rewards
 ```
 
 <!--
 ```agda
-unquoteDecl HasCast-EntitiesEnv = derive-HasCast
-  [ (quote EntitiesEnv , HasCast-EntitiesEnv) ]
+unquoteDecl HasCast-EntitiesEnv HasCast-SubEntitiesEnv = derive-HasCast
+  ( (quote SubEntitiesEnv , HasCast-SubEntitiesEnv) ∷
+  [ (quote EntitiesEnv , HasCast-EntitiesEnv) ])
 
 instance
   EntitiesEnv-HasEpoch : HasEpoch EntitiesEnv
@@ -117,16 +125,12 @@ private variable
   stakeDelegs stakeDelegs' : StakeDelegs
   ccHotKeys : CCHotKeys
   voteDelegs voteDelegs' : VoteDelegs
-  withdrawals : Withdrawals
-  directDeposits : DirectDeposits
-  accountBalanceIntervals : AccountBalanceIntervals
   rewards₀ : Rewards
   depositsᵍ depositsᵈ depositsᵈ' : Credential ⇀ Coin
   legacyMode : Bool
 
   dCerts : List DCert
   e : Epoch
-  votes : List GovVote
   pp : PParams
   cc : ℙ Credential
 
@@ -136,16 +140,17 @@ private variable
 -->
 
 ```agda
-data _⊢_⇀⦇_,SUBENTITIES⦈_ : EntitiesEnv → CertState → SubLevelTx → CertState → Type where
+data _⊢_⇀⦇_,SUBENTITIES⦈_ : SubEntitiesEnv → CertState → SubLevelTx → CertState → Type where
 
   SUBENTITIES :
-    let refresh         = mapPartial (isGovVoterDRep ∘ voter) (fromList votes)
+    let refresh         = mapPartial (isGovVoterDRep ∘ voter) (fromList (ListOfGovVotesOf txSub))
         refreshedDReps  = mapValueRestricted (const (e + pp .drepActivity)) dReps refresh
         activeVDelegs   = mapˢ vDelegCredential (dom (DRepsOf gState'))
                                ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ [])
 
         withdrawals               = WithdrawalsOf txSub
         withdrawalsCredentials    = mapˢ stake (dom withdrawals)
+        accountBalanceIntervals   = BalanceIntervalsOf txSub
         directDeposits            = DirectDepositsOf txSub
         directDepositsCredentials = mapˢ stake (dom directDeposits)
     in
@@ -162,21 +167,22 @@ data _⊢_⇀⦇_,SUBENTITIES⦈_ : EntitiesEnv → CertState → SubLevelTx →
     ∙ ∀[ a ∈ dom directDeposits ] NetworkIdOf a ≡ NetworkId
     ∙ directDepositsCredentials ⊆ dom rewards'
       ────────────────────────────────
-      ⟦ e , pp , cc , legacyMode , rewards₀ ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards , depositsᵈ ⟧ , pState , ⟦ dReps , ccHotKeys , depositsᵍ ⟧ ⟧ ⇀⦇ txSub ,SUBENTITIES⦈ ⟦ ⟦ voteDelegs' ∣^ activeVDelegs , stakeDelegs' , applyDirectDeposits directDeposits rewards' , depositsᵈ' ⟧ , pState' , gState' ⟧
+      ⟦ e , pp , cc , rewards₀ ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards , depositsᵈ ⟧ , pState , ⟦ dReps , ccHotKeys , depositsᵍ ⟧ ⟧ ⇀⦇ txSub ,SUBENTITIES⦈ ⟦ ⟦ voteDelegs' ∣^ activeVDelegs , stakeDelegs' , applyDirectDeposits directDeposits rewards' , depositsᵈ' ⟧ , pState' , gState' ⟧
 ```
 
 ```agda
 data _⊢_⇀⦇_,ENTITIES⦈_ : EntitiesEnv → CertState → TopLevelTx → CertState → Type where
 
   ENTITIES :
-    let refresh         = mapPartial (isGovVoterDRep ∘ voter) (fromList votes)
+    let refresh         = mapPartial (isGovVoterDRep ∘ voter) (fromList (ListOfGovVotesOf txTop))
         refreshedDReps  = mapValueRestricted (const (e + pp .drepActivity)) dReps refresh
         activeVDelegs   = mapˢ vDelegCredential (dom (DRepsOf gState'))
                                ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ [])
 
         withdrawalsSubTxs          = foldl (λ acc txSub → acc ∪⁺ WithdrawalsOf txSub) ∅ (SubTransactionsOf txTop)
         withdrawals                = WithdrawalsOf txTop
         withdrawalsCredentials     = mapˢ stake (dom withdrawals)
+        accountBalanceIntervals    = BalanceIntervalsOf txSub
         directDeposits             = DirectDepositsOf txTop
         directDepositsCredentials  = mapˢ stake (dom directDeposits)
     in

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

@@ -28,7 +28,7 @@ open import Ledger.Dijkstra.Specification.Gov govStructure
 open import Ledger.Dijkstra.Specification.Utxo txs abs
 open import Ledger.Dijkstra.Specification.Utxow txs abs
 open import Ledger.Dijkstra.Specification.Certs govStructure
-open import Ledger.Dijkstra.Specification.Entities govStructure
+open import Ledger.Dijkstra.Specification.Entities txs
 
 open EnactState using (cc)
 ```
@@ -45,7 +45,7 @@ record SubLedgerEnv : Type where
     enactState       : EnactState
     treasury         : Treasury
     utxo₀            : UTxO
-    certState        : CertState
+    rewards₀         : Rewards
     allScripts       : ℙ Script
     isTopLevelValid  : Bool
 
@@ -211,6 +211,7 @@ private variable
   treasury                          : Treasury
   isTopLevelValid                   : Bool
   allScripts                        : ℙ Script
+  rewards₀                          : Rewards
 ```
 -->
 
@@ -278,16 +279,16 @@ data _⊢_⇀⦇_,SUBLEDGER⦈_ : SubLedgerEnv → LedgerState → SubLevelTx 
   SUBLEDGER-V :
       ∙ isTopLevelValid ≡ true
       ∙ ⟦ slot , pp , treasury , utxo₀ , certState , allScripts , isTopLevelValid ⟧ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₁
-      ∙ ⟦ epoch slot , pp , ListOfGovVotesOf stx , allColdCreds govState₀ enactState , WithdrawalsOf stx , DirectDepositsOf stx ⟧ ⊢ certState₀ ⇀⦇ DCertsOf stx ,ENTITIES⦈ certState₁
+      ∙ ⟦ epoch slot , pp , allColdCreds govState₀ enactState , rewards₀ ⟧ ⊢ certState₀ ⇀⦇ stx ,SUBENTITIES⦈ certState₁
       ∙ ⟦ TxIdOf stx , epoch slot , pp , ppolicy , enactState , certState₁ , dom (RewardsOf certState₁) ⟧ ⊢ govState₀ ⇀⦇ GovProposals+Votes stx ,GOVS⦈ govState₁
         ────────────────────────────────
-        ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , certState , allScripts , isTopLevelValid ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧
+        ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , rewards₀ , allScripts , isTopLevelValid ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧
 
   SUBLEDGER-I :
       ∙ isTopLevelValid ≡ false
       ∙ ⟦ slot , pp , treasury , utxo₀ , certState , allScripts , isTopLevelValid  ⟧ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₀
         ────────────────────────────────
-        ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , certState , allScripts , isTopLevelValid ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧
+        ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , rewards₀ , allScripts , isTopLevelValid ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧
 
 _⊢_⇀⦇_,SUBLEDGERS⦈_ : SubLedgerEnv → LedgerState → List SubLevelTx → LedgerState → Type
 _⊢_⇀⦇_,SUBLEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,SUBLEDGER⦈_}
@@ -299,12 +300,15 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LedgerState → TopLevelTx → Ledg
     let  utxo₀ : UTxO
          utxo₀ = UTxOOf utxoState₀
 
+         rewards₀ : Rewards
+         rewards₀ = RewardsOf certState₀
+
          allScripts : ℙ Script
          allScripts = getAllScripts tx utxo₀
     in
       ∙ IsValidFlagOf tx ≡ true
-      ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , certState₀ , allScripts , IsValidFlagOf tx ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧
-      ∙ ⟦ epoch slot , pp , ListOfGovVotesOf tx , allColdCreds govState₁ enactState , WithdrawalsOf tx , DirectDepositsOf tx ⟧ ⊢ certState₁ ⇀⦇ DCertsOf tx ,ENTITIES⦈ certState₂
+      ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , rewards₀ , allScripts , IsValidFlagOf tx ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧
+      ∙ ⟦ epoch slot , pp , allColdCreds govState₁ enactState , true , rewards₀ ⟧ ⊢ certState₁ ⇀⦇ tx ,ENTITIES⦈ certState₂
       ∙ ⟦ TxIdOf tx , epoch slot , pp , ppolicy , enactState , certState₂ , dom (RewardsOf certState₂) ⟧ ⊢ govState₁ ⇀⦇ GovProposals+Votes tx ,GOVS⦈ govState₂
       ∙ ⟦ slot , pp , treasury , utxo₀ , certState₀ , allScripts ⟧ ⊢ utxoState₁ ⇀⦇ tx ,UTXOW⦈ utxoState₂
         ────────────────────────────────
@@ -314,11 +318,14 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LedgerState → TopLevelTx → Ledg
     let  utxo₀ : UTxO
          utxo₀ = UTxOOf utxoState₀
 
+         rewards₀ : Rewards
+         rewards₀ = RewardsOf certState₀
+
          allScripts : ℙ Script
          allScripts = getAllScripts tx utxo₀
     in
       ∙ IsValidFlagOf tx ≡ false
-      ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , certState₀ , allScripts , IsValidFlagOf tx ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧
+      ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , rewards₀ , allScripts , IsValidFlagOf tx ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧
       ∙ ⟦ slot , pp , treasury , utxo₀ , certState₀ , allScripts ⟧ ⊢ utxoState₀ ⇀⦇ tx ,UTXOW⦈ utxoState₁
         ────────────────────────────────
         ⟦ slot , ppolicy , pp , enactState , treasury ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ tx ,LEDGER⦈ ⟦ utxoState₁ , govState₀ , certState₀ ⟧