Cardano Updates

Bumps [github.com/blinklabs-io/gouroboros](https://github.com/blinklabs-io/gouroboros) from 0.182.0 to 0.183.0.
- [Release notes](https://github.com/blinklabs-io/gouroboros/releases)
- [Changelog](https://github.com/blinklabs-io/gouroboros/blob/main/RELEASE_NOTES.md)
- [Commits](https://github.com/blinklabs-io/gouroboros/compare/v0.182.0...v0.183.0)

---
updated-dependencies:
- dependency-name: github.com/blinklabs-io/gouroboros
  dependency-version: 0.183.0
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <[email protected]>

Bumps [github.com/blinklabs-io/cardano-models](https://github.com/blinklabs-io/cardano-models) from 0.7.1 to 0.7.2.
- [Release notes](https://github.com/blinklabs-io/cardano-models/releases)
- [Commits](https://github.com/blinklabs-io/cardano-models/compare/v0.7.1...v0.7.2)

---
updated-dependencies:
- dependency-name: github.com/blinklabs-io/cardano-models
  dependency-version: 0.7.2
  dependency-type: direct:production
  update-type: version-update:semver-patch
...

Signed-off-by: dependabot[bot] <[email protected]>

Bumps [github.com/dgraph-io/badger/v4](https://github.com/dgraph-io/badger) from 4.9.1 to 4.9.2.
- [Release notes](https://github.com/dgraph-io/badger/releases)
- [Changelog](https://github.com/dgraph-io/badger/blob/main/CHANGELOG.md)
- [Commits](https://github.com/dgraph-io/badger/compare/v4.9.1...v4.9.2)

---
updated-dependencies:
- dependency-name: github.com/dgraph-io/badger/v4
  dependency-version: 4.9.2
  dependency-type: direct:production
  update-type: version-update:semver-patch
...

Signed-off-by: dependabot[bot] <[email protected]>

New modules under src/Ledger/Dijkstra/Specification/Certs/Properties/:
+  PoVLemmas.lagda.md  (CERT-level)
+  PoV.lagda.md        (CERTS-level)

PoVLemmas exports:
+  CERT-pov: preservation of value at one CERT step
+  CERT-pots-≡ᵐᵗ: per-step ≡ᵐ-componentwise triple bridge
+  CERT-coinFromDeposits-step: per-step coin bridge (derived)
+  Triple machinery: pots, coinFromDeposits-pots,
   updateCertDeposit-list, pots-updateCertDeposits
+  PoolDepositsAligned, Is-just-isPoolRegistered⇒∈-dom

PoV exports a bundled Certs-PoV module parameterised by
indexedSumᵛ'-∪ and PoolDepositsAligned-CERT, providing:
+  CERTS-pov: preservation across the closure
+  CERTS-Deposits-Bridge.CERTS-coinFromDeposits-updateCertDeposits:
   the closed-form coin bridge consumed by LEDGER-pov

The triple-form per-step bridge from the previous Ledger-PoV branch
required a deferred propositional equation m ∪ˡ ❴ k , v ❵ ≡ m
(when k ∈ dom m). This PR drops that parameter, using instead the
upstream ≡ᵐ-componentwise singleton-∈-∪ˡ plumbed through the closed
form via ∪⁺-cong-r, ∪ˡ-cong, restrict-cong, and collapsed to a coin
equality via ≡ᵉ-getCoin.

Refs #1185

Adds the per-step and RTC-induction bridging lemmas that prove the actual `CertState` produced by a `CERTS` chain has the same three deposit pots (and hence the same `coinFromDeposits`) as the closed-form `updateCertDeposits` applied to the initial state and the cert list.  This is the cert-deposit half of the `LEDGER-pov` chain; combined with the `posNeg-deposits` cancellation identity, it closes the deposit-accounting equation against the UTXO batch-balance equation.

New proofs (PR branch):

+  `CERT-deposits-updateCertDeposit` in `Certs.Properties.PoVLemmas`.  Per-step, case-split on the `CERT` rule's eight `DCert` constructors; `refl` in seven cases, `POOL-rereg` discharged via the pool-deposit alignment invariant.

+  `CERTS-deposits-updateCertDeposits` in `Certs.Properties.PoV`.  RTC induction mirroring `CERTS-pov`.  Factored through `updateCertDeposit-list`, a pure pot-only `foldl` that is the rule-intrinsic counterpart of `updateCertDeposits`; the bridge `pots-updateCertDeposits` handles the inheritance of non-deposit `CertState` fields.

+  `CERTS-coinFromDeposits-updateCertDeposits`.  Coin projection of the main lemma, immediately usable by `LEDGER-pov`.

Both bridging lemmas are parameterised over (a) two deferred set/map facts (`∪ˡ-singleton-mem-≡`, `Is-just-isPoolRegistered⇒∈-dom`) to be discharged from the standard library; and (b) the pool-deposit alignment invariant `PoolDepositsAligned` plus, for the RTC sibling, its `CERT`-step preservation lemma — both follow by inspection of the `POOL` sub-rules.

Master-touching changes

+  **Bug fix in `updateCertDeposits`**.  Was setting `DState.deposits` to `depositsᵍ` (the `GState` delta) instead of `depositsᵈ`.  The `depositsᵈ` name was bound by destructuring but otherwise unused — almost certainly an unintended typo.

+  **Bug fix in `updateCertDeposits`**.  Was using `foldr`, processing certs right-to-left.  The `CERTS` rule processes certs left-to-right (via `BS-ind`'s head-first decomposition).  For non-commutative cert sequences this is unsound: e.g. `[delegate c keyDeposit, dereg c (just keyDeposit)]` for a fresh credential should end with `c ∉ deposits` per `CERTS`, but `foldr` (which processes the `dereg` on the fresh state first as a no-op, then the `delegate`) ends with `c ∈ deposits`.  Switched to `foldl`.  Conway's `updateCertDeposits` is recursive left-to-right (equivalent to `foldl`); Dijkstra's own `applyToRewards` uses `foldl`.

+  **Refactor**.  Extracted `updateCertDepositsStep` as a named function from `updateCertDeposits`' inner lambda, so that downstream proofs can state and use its per-step pots equation.

+  **Hoist**.  Moved `updateCertDeposit`, `updateCertDeposits`, `coinFromDeposits`, `depositsChange`, `newCertDeposits`, `refundCertDeposits` from `Utxo.lagda.md` to `Certs.lagda.md`.  These depend only on `Certs`-level definitions (`PParams`, `DCert`, `CertState`); the previous location forced any proof referencing them to take the larger `TransactionStructure` / `AbstractFunctions` parameter set, blocking placement of the bridging lemmas in `Certs.Properties.PoV{,Lemmas}`.  `govProposalsDeposits` remains in `Utxo.lagda.md` (depends on `GovProposal`).

PR-branch-only changes:

+  `Ledger.lagda.md`. Replaced the local `coinFromDeposit` (singular) with the hoisted `coinFromDeposits` (plural).  `HasCoin-LedgerState` has three summands: `getCoin(UTxOState) + rewardsBalance(DState) + coinFromDeposits(CertState)`.  Gov-action deposits are stored in `GState.deposits` (keyed by `returnAddr`'s stake credential) and are therefore already counted by the third summand.

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.<...>.

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.

+  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.

Signed-off-by: jeluard <[email protected]>

Signed-off-by: yHSJ <[email protected]>

Signed-off-by: Jonathan Lim <[email protected]>

Store path: /nix/store/ff91csiwpspvqahaach56ahq86lf53vd-combined-docs

The info banner sat inside the genesis() function body, so it fired once per `wb genesis <op>` dispatch