adopt improvements from PR #1169

Author: williamdemeo

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

@@ -141,6 +141,14 @@ record HasDepositsChange {a} (A : Type a) : Type a where
   field DepositsChangeOf : A → DepositsChange
 open HasDepositsChange ⦃...⦄ public
 
+record HasDepositsChangeTop {a} (A : Type a) : Type a where
+  field DepositsChangeTopOf : A → ℤ
+open HasDepositsChangeTop ⦃...⦄ public
+
+record HasDepositsChangeSub {a} (A : Type a) : Type a where
+  field DepositsChangeSubOf : A → ℤ
+open HasDepositsChangeSub ⦃...⦄ public
+
 record HasScriptPool {a} (A : Type a) : Type a where
   field ScriptPoolOf : A → ℙ Script
 open HasScriptPool ⦃...⦄ public
@@ -209,6 +217,18 @@ instance
   HasDonations-UTxOState : HasDonations UTxOState
   HasDonations-UTxOState .DonationsOf = UTxOState.donations
 
+  HasDepositsChangeTop-DepositsChange : HasDepositsChangeTop DepositsChange
+  HasDepositsChangeTop-DepositsChange .DepositsChangeTopOf = DepositsChange.depositsChangeTop
+
+  HasDepositsChangeSub-DepositsChange : HasDepositsChangeSub DepositsChange
+  HasDepositsChangeSub-DepositsChange .DepositsChangeSubOf = DepositsChange.depositsChangeSub
+
+  HasDepositsChangeTop-UTxOEnv : HasDepositsChangeTop UTxOEnv
+  HasDepositsChangeTop-UTxOEnv .DepositsChangeTopOf = DepositsChangeTopOf ∘ DepositsChangeOf
+
+  HasDepositsChangeSub-UTxOEnv : HasDepositsChangeSub UTxOEnv
+  HasDepositsChangeSub-UTxOEnv .DepositsChangeSubOf = DepositsChangeSubOf ∘ DepositsChangeOf
+
   unquoteDecl HasCast-DepositsChange
               HasCast-UTxOEnv
               HasCast-SubUTxOEnv
@@ -256,6 +276,9 @@ minfee pp txTop utxo = pp .a * (SizeOf txTop) + pp .b
 instance
   HasCoin-UTxO : HasCoin UTxO
   HasCoin-UTxO .getCoin = cbalance
+
+  HasCoin-UTxOState : HasCoin UTxOState
+  HasCoin-UTxOState .getCoin s = getCoin (UTxOOf s) + FeesOf s + DonationsOf s
 ```
 -->
 
@@ -300,6 +323,16 @@ collateralCheck pp txTop utxo =
   × coin (balance (utxo ∣ CollateralInputsOf txTop)) * 100 ≥ (TxFeesOf txTop) * pp .collateralPercentage
   × (CollateralInputsOf txTop) ≢ ∅
 
+producedTx : Tx ℓ → Value
+producedTx tx = balance (outs tx)
+                + inject (DonationsOf tx)
+                + inject (getCoin (DirectDepositsOf tx))
+
+consumedTx : Tx ℓ → UTxO → Value
+consumedTx tx utxo = balance (utxo ∣ SpendInputsOf tx)
+                     + MintedValueOf tx
+                     + inject (getCoin (WithdrawalsOf tx))
+
 module _ (depositsChange : DepositsChange) where
 
   open DepositsChange depositsChange
@@ -316,11 +349,6 @@ module _ (depositsChange : DepositsChange) where
   depositRefundsTop : Coin
   depositRefundsTop = negPart depositsChangeTop
 
-  consumedTx : Tx ℓ → UTxO → Value
-  consumedTx tx utxo = balance (utxo ∣ SpendInputsOf tx)
-                       + MintedValueOf tx
-                       + inject (getCoin (WithdrawalsOf tx))
-
   consumed : TopLevelTx → UTxO → Value
   consumed txTop utxo = consumedTx txTop utxo
                         + inject depositRefundsTop
@@ -337,11 +365,6 @@ In the preservation-of-value equation, direct deposits appear on the
 the transaction and that amount is deposited into accounts.
 
 ```agda
-  producedTx : Tx ℓ → Value
-  producedTx tx = balance (outs tx)
-                  + inject (DonationsOf tx)
-                  + inject (getCoin (DirectDepositsOf tx))
-
   produced : TopLevelTx → Value
   produced txTop = producedTx txTop
                    + inject (TxFeesOf txTop)