Cardano Updates

Calculate deposit changes from CertState and certificates in the tx

Calculate deposit changes from CertState and certificates in the tx

For consistency with SUBUTXOW

Step 4 of the LEDGER preservation-of-value plan (#1187).  Chains the
three lemmas already proved in steps 2-3 over the single ENTITIES
constructor:

  applyWithdrawals-pov  on (wdrls, r₀)
  CERTS-pov             on the inner ⟦ ... ,CERTS⦈ premise
  applyDirectDeposits-pov on (dd, r₁)

The resulting equation is the value-flow statement for the whole rule:

  getCoin s + getCoin (DirectDepositsOf Γ)
    ≡ getCoin s' + getCoin (WithdrawalsOf Γ)

ENTITIES-pov takes the two per-batch NetworkId witnesses as separate
arguments, mirroring extract-netId's output in the old #1190 LEDGER-pov
proof.  These witnesses are produced at the call site by the
SUBUTXOW/UTXOW step and threaded into ENTITIES-pov from there.

The module ENTITIES-PoV inherits and re-exports the three set/map
parameters of ApplyToRewards-PoV (∪ˡ-lookup-preserve,
sum-map-proj₂≡getCoin, setToList-Unique), to be discharged in a
follow-up.

Also adds a top-level Entities.Properties module that re-exports the
two property submodules, matching the existing Certs.Properties
convention.

Step 3 of the LEDGER preservation-of-value plan (#1187).

These two lemmas describe the value flow through the per-transaction
withdrawal and direct-deposit handling that bracket the inner CERTS
step inside the new ENTITIES rule (#1201):

+  applyWithdrawals-pov: getCoin rwds ≡ getCoin (applyWithdrawals w r) + getCoin w
+  applyDirectDeposits-pov: getCoin (applyDirectDeposits d r) ≡ getCoin r + getCoin d

Both are proved by induction over setToList of the underlying
RewardAddress ⇀ Coin map, with a per-step lemma about applyOne (the
lambda body of applyToRewards) at each inductive step.

The withdrawal version requires the per-batch NetworkId witness and a
Unique-on-stake-projection invariant on the remaining fold list,
because truncating subtraction (_∸_) means an already-reduced balance
must never be revisited.  The direct-deposit version drops both --
addition is total and commutative, so a re-visit is harmless -- and
the resulting signature is correspondingly leaner.

The module ApplyToRewards-PoV is parameterised over three set/map
identities to be discharged in a follow-up:

+  ∪ˡ-lookup-preserve
+  sum-map-proj₂≡getCoin
+  setToList-Unique  (used only by applyWithdrawals-pov)

File location reflects the post-#1201 home of applyWithdrawals and
applyDirectDeposits: Entities.Specification.<...>, not
Certs.Specification.<...>.

+  Add singleton/union/sum lemmas to Ledger.Prelude

   Foundational identities used by the Dijkstra preservation-of-value
   proofs (#1187) and likely useful elsewhere.  All are stated at the
   generic `A ⇀ Coin` (or `List A`) level and are independent of any
   ledger-era rule.

   Added definitions:

   +  ≡ᵉ-getCoin, getCoin-cong, indexedSumᵛ'-∪, res-decomp: lift the
      abstract-set-theory equational machinery (≡ᵉ, indexedSum-cong,
      indexedSumᵐ-∪) to the `getCoin` interface.
   +  getCoin-singleton, ∪ˡsingleton∈dom, ∪ˡsingleton∉dom, ∪ˡsingleton0≡:
      left-biased union with a single-entry map, with the zero-valued
      specialisation that arises in DELEG-delegate / DELEG-dereg.
   +  sumConstZero, indexedSumL-proj₂-zero, setToList-∈: small list/set
      bookkeeping used by sumConstZero.
   +  sum-map-+, +-interleave: list-of-ℕ algebra that the eventual
      LEDGER-pov chain will use to interleave summands.
   +  dec-de-morgan: de Morgan rewrite for a decidable conjunction.

   No semantic change to any ledger rule.

+  Add Certs preservation-of-value lemmas for Dijkstra

   Step 2 of the LEDGER preservation-of-value plan (#1187).  In Dijkstra
   (post-#1201), CERTS is the plain reflexive-transitive closure of CERT,
   with withdrawal and direct-deposit handling having migrated to the
   surrounding ENTITIES rule.  Consequently the value-preservation
   statement for CERTS reduces to

      getCoin s ≡ getCoin s'

   This commit adds two new modules:

   +  Certs.Properties.PoVLemmas: the per-step lemma CERT-pov, with all
      four sub-rule cases (CERT-deleg DELEG-delegate, CERT-deleg
      DELEG-dereg, CERT-pool, CERT-gov).  The proofs use the
      singleton/union helpers now in Ledger.Prelude.
   +  Certs.Properties.PoV: the closure-level CERTS-pov, by induction on
      the reflexive-transitive closure using CERT-pov at each step.

   A one-line addition to Certs/Properties.lagda.md re-exports both new
   modules from the top-level Properties namespace.

   No parameterised wrapper modules.  Both lemmas are top-level
   definitions and threading-free for consumers.

Preliminary infrastructure for the LEDGER preservation-of-value proof (#1187).

LedgerState contains three coin-bearing components: the UTxO state (fees
and donations counted via the existing HasCoin-UTxOState instance), the
rewards balance in DState.rewards, and the three deposit pots (stake-key,
pool, DRep). The existing HasCoin-CertState instance only counts the
rewards balance; the deposit pots have to be added at the LedgerState
level for the LEDGER-pov equation to balance.

This commit:

+  Promotes coinFromDeposit from a where-bound helper inside
   calculateDepositsChange to a top-level definition, so the PoV proof
   (and any future consumer) can reference it directly.
+  Adds a HasCoin-LedgerState instance summing UTxO state coin, the
   rewards balance, and coinFromDeposit applied to the CertState.

No semantic change to LEDGER or any other rule.