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

Prove `LEDGER-pov` for the Dijkstra LEDGER rule: getCoin s ≡ getCoin s',
where getCoin (LedgerState) sums UTxO coin, the rewards balance, the three
cert-deposit pots, and the gov-action deposits.  Typechecks under --safe
with no postulates or holes.

Top-down plan: the supporting Certs / UTxO / Gov facts are module
parameters of `Ledger.Properties.PoV`, forming the frozen contract for the
follow-up PRs (#1186 utxo/utxow, #1210 certs, and a future Gov PoV).

New modules:
- Ledger/Properties/PoV: LEDGER-pov.  The LEDGER-V case is a single
  LedgerState-level equational chain; direct-deposit value cancels between
  the UTxO and CertState sides, gov-deposit growth is matched against the
  produced-side govProposalsDeposits, and `bat'` converts the closed-form
  batch balance (#1186 shape) to the chain's two-level posPart/negPart
  deposit form via the batch-cert-deposits-bridge (#1210 shape) and
  net-arith.
- Entities/Properties/PoV: ENTITIES-pov and SUBENTITIES-pov, the
  value-flow equations for the post-#1256 tx-signal rules.  NetworkId and
  domain facts come from the rules' own premises; the no-truncation bound
  (withdrawal amount ≤ input-state balance) is an explicit hypothesis —
  the phantom-withdrawal gap flagged in the #1256 review, provided at the
  LEDGER level by the ENTITIES/SUBENTITIES-wdrls-bounded parameters.
- Entities/Properties/ApplyToRewardsPoV: applyWithdrawals-pov and
  applyDirectDeposits-pov fold lemmas.

Spec changes:
- Ledger: getCoin (LedgerState) gains a coinFromGovDeposit summand
  (gov-action deposits live in GovActionState.deposit, not
  GState.deposits, yet the UTXO batch balance charges
  govProposalsDeposits on the produced side).
- Certs: getCoin (CertState) is now total (rewards + deposit pots), with
  coinFromRewards / coinFromDeposits projections.
- Prelude: era-independent sum lemmas (+-interleave, sum-map-+).

Squash of the pre-rebase branch (13 WIP commits, head f677e1b), rebased
onto master and adapted to #1250 (explicit cert deposits, closed-form
newCertDeposits/refundCertDeposits), #1253/#1256 (EntitiesEnv,
SUBENTITIES, tx-signal ENTITIES), #1262 (legacyMode threading), and
#1263/#1265 (UTXOW premise changes).  Master absorbed this branch's
deposit sign-swap fix in #1250, so it is no longer part of the diff.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Author: williamdemeo

CHANGELOG.md

@@ -4,6 +4,18 @@
 
 ### WIP
 
+- Prove preservation of value for the `LEDGER` rule (`LEDGER-pov`, #1187), in new module
+  `Ledger.Properties.PoV`.  Supporting modules: `Entities.Properties.PoV`
+  (`ENTITIES-pov`, `SUBENTITIES-pov`) and `Entities.Properties.ApplyToRewardsPoV`
+  (`applyWithdrawals-pov`, `applyDirectDeposits-pov`).  The supporting UTxO, Certs, and
+  Gov facts are module parameters, to be discharged by #1186, #1210, and a future
+  `Gov.Properties.PoV`.
+- Count governance-action deposits in `getCoin LedgerState` via a new
+  `coinFromGovDeposit : GovState → Coin` (sum of `GovActionState.deposit`).  These
+  deposits live in `GovActionState.deposit`, not `GState.deposits`, so the three
+  `CertState` deposit pots alone do not account for them.
+- Make `getCoin` on `CertState` total (rewards balance plus the three deposit pots) and
+  add the `coinFromRewards`/`coinFromDeposits` projections in `Certs`.
 - 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.

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

@@ -362,11 +362,27 @@ module _ (pp : PParams) where
       addRefundCertDeposit acc _               = acc
 ```
 
+The two coin-bearing components of a `CertState`{.AgdaRecord} are the rewards
+(account) balances and the three deposit pots.  `coinFromRewards`{.AgdaFunction} and
+`coinFromDeposits`{.AgdaFunction} project their totals; `getCoin`{.AgdaFunction} on a
+`CertState`{.AgdaRecord} is their sum, so preservation-of-value statements can be
+phrased at the `CertState`{.AgdaRecord} level.
+
+```agda
+coinFromRewards : CertState → Coin
+coinFromRewards = rewardsBalance ∘ DStateOf
+
+coinFromDeposits : CertState → Coin
+coinFromDeposits cs =
+  getCoin (DepositsOf (DStateOf cs)) + getCoin (DepositsOf (PStateOf cs)) + getCoin (DepositsOf (GStateOf cs))
+```
+
 <!--
 ```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
 ```