Cardano Updates

Add `-with-rtsopts=--optimistic-linking` to iserv-proxy's cabalProjectLocal so the RTS option is embedded in `main.c` at link time and processed with `RtsOptsAll` — bypassing the OPTION_UNSAFE gate that command-line `+RTS --optimistic-linking -RTS` is subject to. The wrapper scripts under `overlays/{linux-cross,mingw_w64}.nix` no longer need to pass it at invocation. Gated on `impl(ghc >=9.14)` since earlier RTS versions don't recognise the flag.

- Extract shared TxBody fields into encodeSharedTxBody
- Add encodeSubTx and encodeSubTxBody for Tx SubTx DijkstraEra
- Encode requiredTopLevelGuards in sub-transaction bodies
- Pass MetadataFormat through encodeTxBody for sub-tx metadata

Co-Authored-By: Claude <[email protected]>

- Replace downgradePParamsHKD with native encoder exposing real
  Dijkstra ref-script parameters (refScriptCostStride,
  refScriptCostMultiplier, maxRefScriptSizePerTx,
  maxRefScriptSizePerBlock)
- Wire up guards field via guardsTxBodyL replacing reqSignerHashesTxBodyL
- Wire up directDeposits and accountBalanceIntervals TxBody fields
- Fix DijkstraUnRegCert incorrectly mapped to ConwayRegCert
- Fix stale module comment referencing CBOR roundtrip

Co-Authored-By: Claude <[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.

Now that the file lives at
`src-lib-exts/abstract-set-theory/Axiom/Set/Map/Extra.lagda.md`:

+ Update the top-level module declaration to
  `module abstract-set-theory.Axiom.Set.Map.Extra (th : Theory) where`,
  matching the rest of the abstract-set-theory subtree.
+ Replace `open import Ledger.Prelude` with explicit imports from
  `abstract-set-theory.Prelude` and stdlib modules. `src-lib-exts/`
  cannot depend on `Ledger.Prelude` (upward dependency).
+ Inline the five-line `_≢ᵐ_` definition that previously lived in
  the standalone `Extra.agda`, and delete `Extra.agda`.
+ Convert the file to literate-markdown formatting with brief
  section prose; the module body is otherwise unchanged.
+ Update the single downstream caller
  (`Ledger.Conway.Conformance.Equivalence.Deposits`) to import from
  the new location.

Closes #1194

Co-authored-by: Copilot Autofix powered by AI <[email protected]>