adopt improvements from PR #1169

Author: williamdemeo

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

@@ -142,6 +142,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
@@ -210,6 +218,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
@@ -257,6 +277,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
 ```
 -->
 
@@ -301,6 +324,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
@@ -317,11 +350,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
@@ -338,11 +366,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)

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

@@ -51,8 +51,8 @@ derivation as their final premise.  We factor out an extractor:
 UTXOW⇒UTXO : ∀ {Γ : UTxOEnv} {s s' : UTxOState} {tx : TopLevelTx}
   → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' → ∃[ legacyMode ] ((Γ , legacyMode) ⊢ s ⇀⦇ tx ,UTXO⦈ s')
 
-UTXOW⇒UTXO (UTXOW-normal-⋯ _ _ _ _ _ _ _ _ _ _ utxo) = false , utxo
-UTXOW⇒UTXO (UTXOW-legacy-⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ utxo) = true , utxo
+UTXOW⇒UTXO (UTXOW-normal-⋯ _ _ _ _ _ _ _ _ _ _ _ utxo) = false , utxo
+UTXOW⇒UTXO (UTXOW-legacy-⋯ _ _ _ _ _ _ _ _ _ _ _ utxo) = true , utxo
 ```
 
 ## `UTXOW-I-getCoin`: collateral collection preserves `getCoin`