[Dijkstra] CIP-159-11c: Prove LEDGER preservation of value (#1187)

CHANGELOG.md

@@ -4,9 +4,18 @@
 
 ### WIP
 
+- Fix preservation-of-value soundness bug in `Utxo`: deposit terms were on the wrong
+  sides of the batch-balance equation. New deposits (`newCertDeposits`,
+  `govProposalsDeposits`) now appear on the *produced* side and refunds
+  (`refundCertDeposits`) on the *consumed* side, matching the trusted Conway
+  convention. The previous (swapped) placement let a transaction create value.
+- Count governance-action deposits in `getCoin LedgerState` via a new
+  `coinFromGovDeposit : GovState → Coin` (sum of `GovActionState.deposit`). Post-#1214
+  these deposits live in `GovActionState.deposit`, not `GState.deposits`, so
+  `coinFromDeposits` alone no longer accounts for them.
 - Move cert-deposit helpers from `Utxo` to `Certs`.
 - Fix `updateCertDeposits`: use `foldl` (CERTS is head-first).
-- Add `HasCoin-UTxOState` and `HasCoin-LedgerState` instances; the latter sums UTxO total, rewards balance, and all three deposit fields.
+- Add `HasCoin-UTxOState` and `HasCoin-LedgerState` instances; the latter sums UTxO total, rewards balance, the three `CertState` deposit fields (`coinFromDeposits`), and governance-action deposits (`coinFromGovDeposit`).
 - Apply per-transaction direct deposits to `CertState` after each `CERTS` step in `SUBLEDGER-V` and `LEDGER-V` (CIP-159).
 - Forbid CIP-159 fields (`txDirectDeposits`, `txBalanceIntervals`) in legacy mode via explicit `UTXOW-legacy` premises.
 - Allow partial withdrawals in `PRE-CERT` rule; define `applyWithdrawals` and `_≤ᵐ_` (CIP-159).

src/Ledger/Dijkstra/Specification.lagda.md

@@ -69,6 +69,7 @@ import Ledger.Dijkstra.Specification.Enact.Properties
 import Ledger.Dijkstra.Specification.Entities
 import Ledger.Dijkstra.Specification.Entities.Properties
 ```
+
 ## <span class="AgdaModule">Epoch</span>
 
 ```agda

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

@@ -33,6 +33,15 @@ DirectDeposits : Type
 DirectDeposits = RewardAddress ⇀ Coin
 ```
 
+<!--
+```agda
+record HasDirectDeposits {a} (A : Type a) : Type a where
+  field DirectDepositsOf : A → DirectDeposits
+open HasDirectDeposits ⦃...⦄ public
+```
+-->
+
+
 ## Balance Intervals {#sec:balance-intervals}
 
 [CIP 159][] allows a transaction to assert that an account's balance falls within a

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

@@ -192,6 +192,9 @@ instance
   HasWithdrawals-CertEnv : HasWithdrawals CertEnv
   HasWithdrawals-CertEnv .WithdrawalsOf = CertEnv.wdrls
 
+  HasDirectDeposits-CertEnv : HasDirectDeposits CertEnv
+  HasDirectDeposits-CertEnv .DirectDepositsOf = CertEnv.directDeposits
+
   HasVoteDelegs-DState : HasVoteDelegs DState
   HasVoteDelegs-DState .VoteDelegsOf = DState.voteDelegs
 
@@ -353,6 +356,9 @@ doesn't balance.
 coinFromDeposits : CertState → Coin
 coinFromDeposits cs = coinFromDepositTriple (depositTripleOf cs)
 
+coinFromRewards : CertState → Coin
+coinFromRewards = rewardsBalance ∘ DStateOf
+
 module _ (pp : PParams) (certState : CertState) where
 
   updateCertDeposits : List DCert → CertState
@@ -373,7 +379,8 @@ module _ (pp : PParams) (certState : CertState) where
 ```agda
 instance
   HasCoin-CertState : HasCoin CertState
-  HasCoin-CertState .getCoin = rewardsBalance ∘ DStateOf
+  -- Total coin held in a CertState: the rewards balance plus the deposit pots.
+  HasCoin-CertState .getCoin = λ cs → coinFromRewards cs + coinFromDeposits cs
 
   unquoteDecl DecEq-StakePoolParams = derive-DecEq
     ((quote StakePoolParams , DecEq-StakePoolParams) ∷ [])

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

@@ -13,5 +13,7 @@ module Ledger.Dijkstra.Specification.Entities.Properties where
 -->
 
 ```agda
+open import Ledger.Dijkstra.Specification.Entities.Properties.ApplyToRewardsPoV
 open import Ledger.Dijkstra.Specification.Entities.Properties.Computational
+open import Ledger.Dijkstra.Specification.Entities.Properties.PoV
 ```