Refactor deposits; add IsValidFlag typeclass; Use typeclasses for field accesors

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
@@ -98,21 +88,21 @@ record DState : Type where
     voteDelegs   : VoteDelegs
     stakeDelegs  : StakeDelegs
     rewards      : Rewards
-    deposits     : Deposits
+    deposits     : Credential ⇀ Coin
 
 record PState : Type where
   field
     pools     : Pools
     fPools    : Pools
     retiring  : KeyHash ⇀ Epoch
-    deposits  : Deposits
+    deposits  : KeyHash ⇀ Coin
 
 record GState : Type where
   constructor ⟦_,_⟧ᵛ
   field
     dreps      : DReps
     ccHotKeys  : Credential ⇀ Maybe Credential
-    deposits   : Deposits
+    deposits   : Credential ⇀ Coin
 
 record CertState : Type where
   constructor ⟦_,_,_⟧ᶜˢ
@@ -130,14 +120,10 @@ record DelegEnv : Type where
 
 <!--
 ```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
@@ -194,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
 
@@ -206,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
 
@@ -251,7 +246,8 @@ private variable
   pools fPools           : Pools
   retiring               : Retiring
   wdrls                  : Withdrawals
-  deposits deposits'     : Deposits
+  A                      : Type
+  deposits deposits'     : A ⇀ Coin
 
   an          : Anchor
   Γ           : CertEnv
@@ -301,12 +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 , deposits ⟧ ⇀⦇ delegate c mvd mkh d ,DELEG⦈ ⟦ insertIfJust c mvd vDelegs , insertIfJust c mkh sDelegs , rwds ∪ˡ ❴ c , 0 ❵ , deposits ∪⁺ ❴ CredentialDeposit c , d ❵ ⟧
+      ⟦ 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 , deposits ⟧ ⇀⦇ dereg c md ,DELEG⦈ ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ , deposits ∣ ❴ CredentialDeposit c ❵ ᶜ ⟧
+      ⟦ pp , pools , delegatees ⟧ ⊢ ⟦ vDelegs , sDelegs , rwds , deposits ⟧ ⇀⦇ dereg c md ,DELEG⦈ ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ , deposits ∣ ❴ c ❵ ᶜ ⟧
 
 
 isPoolRegistered : Pools -> KeyHash -> Maybe StakePoolParams
@@ -326,7 +322,7 @@ data _⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Type wh
            pools ∪ˡ ❴ kh , poolParams ❵
          , fPools
          , retiring
-         , deposits ∪⁺ ❴ PoolDeposit kh , pp .poolDeposit ❵
+         , deposits ∪ˡ ❴ kh , pp .poolDeposit ❵
          ⟧
 
   POOL-rereg :
@@ -363,12 +359,12 @@ 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 , deposits ⟧ ⇀⦇ regdrep c d an ,GOVCERT⦈ ⟦ ❴ c , e + pp .drepActivity ❵ ∪ˡ dReps , ccKeys , deposits ∪⁺ ❴ DRepDeposit c , d ❵ ⟧
+      ⟦ 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 , deposits ⟧ ⇀⦇ deregdrep c d ,GOVCERT⦈ ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys , deposits ∣ ❴ DRepDeposit c ❵ ᶜ ⟧
+      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ dReps , ccKeys , deposits ⟧ ⇀⦇ deregdrep c d ,GOVCERT⦈ ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys , deposits ∣ ❴ c ❵ ᶜ ⟧
 
   GOVCERT-ccreghot :
     ∙ (c , nothing) ∉ ccKeys

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
 

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

@@ -36,6 +36,17 @@ open import Ledger.Dijkstra.Specification.Script.Validation txs abs
 
 ```agda
 record UTxOEnv : Type where
+  field
+    slot             : Slot
+    pparams          : PParams
+    treasury         : Treasury
+    utxo₀            : UTxO
+    isTopLevelValid  : Bool
+    depositsChange   : ℤ
+    globalScripts    : ℙ P1Script × ℙ P2Script
+    globalData       : DataHash ⇀ Datum
+
+record SubUTxOEnv : Type where
   field
     slot             : Slot
     pparams          : PParams
@@ -54,7 +65,6 @@ record UTxOState : Type where
   field
     utxo       : UTxO
     fees       : Fees
-    deposits   : Deposits
     donations  : Donations
 ```
 
@@ -64,23 +74,48 @@ record HasUTxOState {a} (A : Type a) : Type a where
   field UTxOStateOf : A → UTxOState
 open HasUTxOState ⦃...⦄ public
 
+record HasGlobalScripts {a} (A : Type a) : Type a where
+  field GlobalScriptsOf : A → ℙ P1Script × ℙ P2Script
+open HasGlobalScripts ⦃...⦄ public
+
+record HasGlobalData {a} (A : Type a) : Type a where
+  field GlobalDataOf : A → DataHash ⇀ Datum
+open HasGlobalData ⦃...⦄ public
+
 instance
   HasUTxO-UTxOEnv : HasUTxO UTxOEnv
   HasUTxO-UTxOEnv .UTxOOf = UTxOEnv.utxo₀
 
+  HasUTxO-SubUTxOEnv : HasUTxO SubUTxOEnv
+  HasUTxO-SubUTxOEnv .UTxOOf = SubUTxOEnv.utxo₀
+
+  HasGlobalScripts-UTxOEnv : HasGlobalScripts UTxOEnv
+  HasGlobalScripts-UTxOEnv .GlobalScriptsOf = UTxOEnv.globalScripts
+
+  HasGlobalScripts-SubUTxOEnv : HasGlobalScripts SubUTxOEnv
+  HasGlobalScripts-SubUTxOEnv .GlobalScriptsOf = SubUTxOEnv.globalScripts
+
+  HasGlobalData-UTxOEnv : HasGlobalData UTxOEnv
+  HasGlobalData-UTxOEnv .GlobalDataOf = UTxOEnv.globalData
+
+  HasGlobalData-SubUTxOEnv : HasGlobalData SubUTxOEnv
+  HasGlobalData-SubUTxOEnv .GlobalDataOf = SubUTxOEnv.globalData
+
   HasUTxO-UTxOState : HasUTxO UTxOState
   HasUTxO-UTxOState .UTxOOf = UTxOState.utxo
 
-  unquoteDecl HasCast-UTxOEnv HasCast-UTxOState = derive-HasCast
-    ( (quote UTxOEnv   , HasCast-UTxOEnv  ) ∷
-    [ (quote UTxOState , HasCast-UTxOState) ])
+  unquoteDecl HasCast-UTxOEnv HasCast-SubUTxOEnv HasCast-UTxOState = derive-HasCast
+    ( (quote UTxOEnv    , HasCast-UTxOEnv  ) ∷
+      (quote SubUTxOEnv , HasCast-SubUTxOEnv  ) ∷
+    [ (quote UTxOState  , HasCast-UTxOState) ])
 ```
 -->
 
 <!--
 ```agda
 private variable
-  Γ : UTxOEnv
+  A : Type
+  Γ : A
   s s' : UTxOState
   tx : TopLevelTx
   stx : SubLevelTx
@@ -120,7 +155,7 @@ This is achieved by the following precondition in the `UTXO`.{AgdaDatatype} and
 transaction (or partially applying any part of it).
 
 ```agda
-data _⊢_⇀⦇_,SUBUTXO⦈_ : UTxOEnv → UTxOState → SubLevelTx → UTxOState → Type where
+data _⊢_⇀⦇_,SUBUTXO⦈_ : SubUTxOEnv → UTxOState → SubLevelTx → UTxOState → Type where
 
   SUBUTXO :
 

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

@@ -23,7 +23,8 @@ open import Ledger.Dijkstra.Specification.Script.Validation txs abs
 
 private variable
   ℓ : TxLevel
-  Γ  : UTxOEnv
+  A  : Type
+  Γ  : A
   s s' : UTxOState
   tx : TopLevelTx
   stx : SubLevelTx
@@ -39,7 +40,7 @@ allowedLanguages tx utxo = ∅ -- TODO
 ```
 
 ```agda
-data _⊢_⇀⦇_,SUBUTXOW⦈_ : UTxOEnv → UTxOState → SubLevelTx → UTxOState → Type where
+data _⊢_⇀⦇_,SUBUTXOW⦈_ : SubUTxOEnv → UTxOState → SubLevelTx → UTxOState → Type where
 
   SUBUTXOW :
     let
@@ -48,17 +49,17 @@ data _⊢_⇀⦇_,SUBUTXOW⦈_ : UTxOEnv → UTxOState → SubLevelTx → UTxOSt
          open TxWitnesses txWitnesses
          open UTxOEnv
 
-         utxo₀               = Γ .utxo₀
-         utxo                = s .UTxOState.utxo
+         utxo₀               = UTxOOf Γ
+         utxo                = UTxOOf s
 
          witsKeyHashes       : ℙ KeyHash
          witsKeyHashes       = mapˢ hash (dom vKeySigs)
 
          p1Scripts : ℙ P1Script
-         p1Scripts = proj₁ (Γ .globalScripts)
+         p1Scripts = proj₁ (GlobalScriptsOf Γ)
 
          p2Scripts : ℙ P2Script
-         p2Scripts = proj₂ (Γ .globalScripts)
+         p2Scripts = proj₂ (GlobalScriptsOf Γ)
 
          neededScriptHashes  : ℙ ScriptHash
          neededScriptHashes  = mapPartial (isScriptObj  ∘ proj₂) (credsNeeded utxo₀ txBody)
@@ -77,12 +78,12 @@ data _⊢_⇀⦇_,SUBUTXOW⦈_ : UTxOEnv → UTxOState → SubLevelTx → UTxOSt
     ∙  ∀[ s ∈ p1Scripts ] (hash s ∈ neededScriptHashes → validP1Script witsKeyHashes txVldt s)
     ∙  neededVKeyHashes ⊆ witsKeyHashes
     ∙  neededScriptHashes ⊆ mapˢ hash p1Scripts ∪ mapˢ hash p2Scripts
-    ∙  neededDataHashes ⊆ dom (Γ .globalData)
+    ∙  neededDataHashes ⊆ dom (GlobalDataOf Γ)
     ∙  languages tx utxo ⊆ allowedLanguages tx utxo
     ∙  txADhash ≡ map hash txAuxData
-    ∙ Γ ⊢ s ⇀⦇ stx ,SUBUTXO⦈ s'
+    ∙  Γ ⊢ s ⇀⦇ stx ,SUBUTXO⦈ s'
       ────────────────────────────────
-      Γ ⊢ s ⇀⦇ stx ,SUBUTXOW⦈ s'
+       Γ ⊢ s ⇀⦇ stx ,SUBUTXOW⦈ s'
 
 data _⊢_⇀⦇_,UTXOW⦈_ : UTxOEnv → UTxOState → TopLevelTx → UTxOState → Type where
 

src/Ledger/Prelude.lagda.md

@@ -46,6 +46,7 @@ open import abstract-set-theory.FiniteSetTheory public
   renaming (_⊆_ to _⊆ˢ_)
 
 import Data.Integer as ℤ
+open import Data.Integer using (0ℤ) public
 import Data.Rational as ℚ
 open import Data.Rational using (ℚ)