Cardano Updates

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

After direct-deposit application moved from LEDGER-V/SUBLEDGER-V into the
POST-CERT rule, the Certs preservation-of-value proofs needed to account for
the `getCoin (DirectDepositsOf Γ)` increase that POST-CERT now produces via
`rewards ∪⁺ directDeposits`.

Statement changes:
- POST-CERT-pov:  getCoin s ≡ getCoin s'
              →  getCoin s + getCoin (DirectDepositsOf Γ) ≡ getCoin s'
- sts-pov:        gains a `+ getCoin (DirectDepositsOf Γ)` term on the LHS
- CERTS-pov:      becomes the symmetric "consumed = produced" form
                  getCoin s₁ + getCoin (DirectDepositsOf Γ)
                  ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ)

Structural changes:
- POST-CERT-pov and sts-pov move into the parameterized `Certs-Pov-lemmas`
  sub-module (alongside PRE-CERT-pov), since they now require a fourth
  module parameter:
    indexedSumᵛ'-∪⁺ : ∀ (m m' : Rewards) → getCoin (m ∪⁺ m') ≡ getCoin m + getCoin m'
  This is the natural ∪⁺ analogue of the existing `indexedSumᵛ'-∪` lemma for
  `∪ˡ` on disjoint domains, but unconditional because `∪⁺` adds (rather than
  drops) values at shared keys.  TODO: upstream to agda-sets.
- `Certs-PoV` (in PoV.lagda.md) gains the same parameter and forwards it.

CERT-pov and PRE-CERT-pov are unchanged: the CERT and PRE-CERT rules did
not change in this refactor.

Closes part of #1185.

Following the merge of CIP-159 PR #1197 (DirectDeposits keyed by
RewardAddress; applyDirectDeposits and applyWithdrawals refactored
through a shared applyToRewards fold) and the agda-sets cleanup
PR #1196 (Conway Equivalence.Map utilities moved into Ledger.Prelude),
this commit updates the Dijkstra CERTS preservation-of-value proofs
to compile against the new APIs.

Main changes:

+  Rename `ApplyWithdrawals-PoV` sub-module to `ApplyToRewards-PoV`,
   since it now houses lemmas for both withdrawals and direct deposits.

+  Add `getCoin-∪ˡ-overwrite` bridge lemma: `getCoin (❴ c , v ❵ ∪ˡ acc)
   ≡ v + getCoin (acc ∣ ❴ c ❵ ᶜ)`.  Encapsulates the
   listing-vs-replacement reconciliation between the new `❴ k , v ❵ ∪ˡ
   acc` form (used by `applyToRewards`) and the equivalent
   complement-restricted form used by the existing decomposition
   reasoning.

+  Factor `split-by-lookup` as a top-level lemma decomposing
   `getCoin acc` along a known lookup result.  Used by both
   `applyOne-pov` (subtraction) and the new `applyOne-pov-add`
   (addition).

+  Add the additive parallel: `applyOne-pov-add`,
   `foldl-applyOne-pov-add`, and `applyDirectDeposits-pov`.  Mirrors
   the existing withdrawal chain, sharing `getCoin-∪ˡ-overwrite` and
   `split-by-lookup`.

+  Strengthen the `setToList-Unique` module parameter with a
   `NetworkId` premise on the map's domain (the assumption no longer
   conflates withdrawals-specifically with general
   `RewardAddress ⇀ Coin` maps).

+  Replace the `∪ˡ-res-lookup-preserve` module parameter (which
   carried a no-longer-needed complement restriction on the right
   operand) with `∪ˡ-lookup-preserve`, stated against the new
   `❴ c , v ❵ ∪ˡ m` form.

+  Add a small top-level helper `∈-dom⇒¬lookup-nothing` to discharge
   the defensive `nothing` case of `foldl-applyOne-pov-add`.

+  Update `POST-CERT-pov` to use the new
   `applyDirectDeposits-pov`; the proof is `sym
   (applyDirectDeposits-pov ...)`.  The CERT-post step's own
   `mapˢ stake (dom dd) ⊆ dom rewards` premise is extracted from the
   pattern rather than threaded as a separate parameter, since the
   pre-CERT* state's `dom rewards` is not preserved across `CERT`
   trace steps (in particular by `DELEG-dereg`).

+  Update `sts-pov` and `CERTS-pov` signatures accordingly: add the
   `DirectDeposits`-`NetworkId` premise, drop the
   membership-of-deposits premise.

The proofs now typecheck on top of master.

Update conformance tests

Bumps [idna](https://github.com/kjd/idna) from 3.11 to 3.15.
- [Release notes](https://github.com/kjd/idna/releases)
- [Changelog](https://github.com/kjd/idna/blob/master/HISTORY.md)
- [Commits](https://github.com/kjd/idna/compare/v3.11...v3.15)

---
updated-dependencies:
- dependency-name: idna
  dependency-version: '3.15'
  dependency-type: indirect
...

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

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

* meeting 134 merges

* add CIP-0177 confirmed after post meeting waiting period

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

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