[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
deposit sign-swap fix in #1250, so it is no longer part of the diff.

AI-assistend development: 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/Entities/Properties/ApplyToRewardsPoV.lagda.md

@@ -290,7 +290,7 @@ holds.
 ```
 -->
 
-#### `applyWithdrawals-pov`
+#### <span class="AgdaFunction">applyWithdrawals-pov</span>
 
 ```agda
   applyWithdrawals-pov : (wdrls : Withdrawals) (rwds : Rewards)
@@ -329,7 +329,7 @@ holds.
 
 ### Direct-deposit preservation of value
 
-#### `applyOne-pov-add` (one direct-deposit step increases `getCoin` by `amt`)
+#### <span class="AgdaFunction">applyOne-pov-add</span> (one direct-deposit step increases `getCoin` by `amt`)
 
 For addition, no `amt ≤ bal` premise is needed (the operation is total),
 and the per-step equation is `getCoin (...) ≡ getCoin acc + amt`
@@ -360,7 +360,7 @@ balance.
 ```
 -->
 
-#### `foldl-applyOne-pov-add` (fold induction, no `Unique` needed)
+#### <span class="AgdaFunction">foldl-applyOne-pov-add</span> (fold induction, no `Unique` needed)
 
 Unlike the withdrawal version, the additive fold induction needs only
 domain preservation; the `Unique`{.AgdaDatatype} witness drops out.
@@ -405,7 +405,7 @@ the same credential simply accumulates additions correctly.
 ```
 -->
 
-#### `applyDirectDeposits-pov`
+#### <span class="AgdaFunction">applyDirectDeposits-pov</span>
 
 Note the slimmed-down signature relative to `applyWithdrawals-pov`: no
 `NetworkId`{.AgdaFunction} premise (none is needed), no

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

@@ -126,7 +126,7 @@ module ENTITIES-PoV
   open ApplyToRewards-PoV ∪ˡ-lookup-preserve sum-map-proj₂≡getCoin setToList-Unique public
 ```
 
-## Rewards flow
+### Rewards flow
 
 **Informally**.  Let `s`{.AgdaBound}, `s'`{.AgdaBound} be `CertStates`{.AgdaRecord}
 related by `SUBENTITIES`{.AgdaDatatype} with signal `txSub`{.AgdaBound}, and suppose
@@ -227,7 +227,7 @@ hypothesis; in normal mode the rule bounds withdrawals only against the pre-batc
     aw = applyWithdrawals (WithdrawalsOf txTop) r₀
 ```
 
-## Deposit flow
+### Deposit flow
 
 Outside the inner CERTS run, a `SUBENTITIES`{.AgdaDatatype}/`ENTITIES`{.AgdaDatatype}
 step touches only the rewards map (withdrawals and direct deposits), and the DRep
@@ -282,7 +282,7 @@ preservation of `PoolDepositsRegistered`{.AgdaFunction}, and the
     CERTS-new-thread certsStep
 ```
 
-## Full value flow
+### Full value flow
 
 Adding the two flows gives preservation of value for the full `CertState`{.AgdaRecord}
 coin (recall `getCoin`{.AgdaFunction} on a `CertState`{.AgdaRecord} is