Cardano Updates

* Remove DepositsChange

Calculate deposit changes from CertState and certificates in the tx

---------

Co-authored-by: William DeMeo <[email protected]>

UTxOEnv now carries the pre-batch CertState directly rather than a
precomputed DepositsChange, so the LEDGER computational instance no
longer needs separate environments for the valid and invalid cases.
The two old builders (utxoΓ-valid : CertState → CertState → UTxOEnv,
utxoΓ-invalid : UTxOEnv) collapse into a single

   utxoΓ : UTxOEnv
   utxoΓ = ⟦ slot , pparams , treasury , utxo₀ , certState
           , allScripts , RewardsOf certState ⟧

with certState (= the pre-batch state) used in both the LEDGER-V and
LEDGER-I cases.  This resolves the [NotInScope] error from
calculateDepositsChange (which no longer exists) and removes the
vestigial CertState → CertState arguments to utxoΓ-valid that were
unused after the refactor.

The completeness side gets one small additional change: the implicit
argument order in the LEDGER-V destructuring is reorganised to match
the constructor's declared order
   {utxoState₁ , govSt₁ , certSt₁ , certSt₂ , govSt₂ , utxoSt₂}
so the subsequent computeSubledgers / computeEntities / computeGov /
computeUtxow pattern matches against the right intermediate states.

Also adds a "Design Note: Cert-State Threading and Deposit Accounting"
subsection to Utxo.lagda.md explaining the rationale for the
refactor.  Key points:

+  The UTXO rule has been promoted from a consumer of CertState data
   to a secondary executor of certificate accounting:
   updateCertDeposit recomputes the deposit evolution that the
   CERT/ENTITIES rules also produce as part of their operational
   semantics.
+  The same certificate-deposit logic now exists in two places --
   inside the DELEG/POOL/GOVCERT sub-rules of CERT, and inside
   updateCertDeposit in Utxo.lagda.md.
+  Any drift between the two is a soundness problem, since it would
   admit transactions whose UTxO-side balance equation accepts but
   whose actual CertState evolution doesn't balance.  The note states
   the consistency obligation as a lemma to be discharged alongside
   LEDGER-pov.

UTxOEnv now carries the pre-batch CertState directly rather than a
precomputed DepositsChange, so the LEDGER computational instance no
longer needs separate environments for the valid and invalid cases.
The two old builders (utxoΓ-valid : CertState → CertState → UTxOEnv,
utxoΓ-invalid : UTxOEnv) collapse into a single

   utxoΓ : UTxOEnv
   utxoΓ = ⟦ slot , pparams , treasury , utxo₀ , certState
           , allScripts , RewardsOf certState ⟧

with certState (= the pre-batch state) used in both the LEDGER-V and
LEDGER-I cases.  This resolves the [NotInScope] error from
calculateDepositsChange (which no longer exists) and removes the
vestigial CertState → CertState arguments to utxoΓ-valid that were
unused after the refactor.

The completeness side gets one small additional change: the implicit
argument order in the LEDGER-V destructuring is reorganised to match
the constructor's declared order
   {utxoState₁ , govSt₁ , certSt₁ , certSt₂ , govSt₂ , utxoSt₂}
so the subsequent computeSubledgers / computeEntities / computeGov /
computeUtxow pattern matches against the right intermediate states.

Also adds a "Design Note: Cert-State Threading and Deposit Accounting"
subsection to Utxo.lagda.md explaining the rationale for the
refactor.  Key points:

+  The UTXO rule has been promoted from a consumer of CertState data
   to a secondary executor of certificate accounting:
   updateCertDeposit recomputes the deposit evolution that the
   CERT/ENTITIES rules also produce as part of their operational
   semantics.
+  The same certificate-deposit logic now exists in two places --
   inside the DELEG/POOL/GOVCERT sub-rules of CERT, and inside
   updateCertDeposit in Utxo.lagda.md.
+  Any drift between the two is a soundness problem, since it would
   admit transactions whose UTxO-side balance equation accepts but
   whose actual CertState evolution doesn't balance.  The note states
   the consistency obligation as a lemma to be discharged alongside
   LEDGER-pov.

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.