Cardano Updates

The GetDRepDelegations patch history note is better suited to
commit message than an inline comment that will lack context over time.

The SRPs were removed and are now obtained directly from CHaP.

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

Babbage is old enough to be removed per era rotation policy.
Route Babbage transactions to unsupportedEra, keeping only
Conway and Dijkstra as active evaluation eras.

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

Remove babbageToConway and babbageToDijkstra translation paths,
keeping only sameEra and conwayToDijkstra as suggested in review.

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

Align with the two-letter era alias convention used throughout
the codebase (Sh, Al, Ba, Cn). Also qualify Cardano.Ledger.Core
as Ledger.Core for clarity.

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

Add encodePParams, encodeUtxo, encodeGovActionState, and govProposals
to Dijkstra.hs. Replace all unsafeCoerce in Query.hs with these
proper Dijkstra-era encoders.

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

Add ~400 lines of Dijkstra-era encoding functions (encodeTxOut,
encodeNativeScript, encodeDelegCert, encodeScriptPurpose, etc.)
so PredicateFailure.hs can use them instead of unsafeCoercing
through Conway encoders.

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

Add encodeMempoolFailure for Dijkstra era and two new predicate
failures (PointerAddressInCollateralReturn, SpendingOutputFromSubTransaction)
rather than unsafeCoercing through Conway's encodeLedgerFailure.

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

Use upgradeTxOut and fmap upgrade for BabbageTxOut and UTxO
Dijkstra era translations instead of unsafeCoerce.

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

Update test generators, specs, and orphan instances to include
Dijkstra era patterns. Add Dijkstra entry to deserialization failure
test data. Fix BootstrapVote voter schema to use ExtendedVerificationKey.
Update all test vector JSON files for the new era.

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

Add ShelleyBasedEraDijkstra and QueryIfCurrentDijkstra pattern matches
across all encoding, decoding, query, and predicate failure modules.
Introduce Ogmios.Data.Json.Dijkstra with CBOR bridge functions for
type conversion between the nominally distinct Dijkstra and Conway
ledger types. Update era indices, codec configs, and the Prelude era
list. Adapt Rewards module to new ledger API types (NonZero,
ChainAccountState, StakeWithDelegation). Re-enable GetDRepDelegations
query now that NodeToClientV_23 is available in cardano-node 11.0.1.

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

Update cabal.project constraints, index-state, and dependency bounds
for cardano-node 11.0.1 (ouroboros-consensus 3.0.1, cardano-ledger-conway
>= 1.22.1). Update Dockerfile, CI workflows, and JSON schemas to
reference the new node version and include the Dijkstra era.

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.

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

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