Cardano Updates

Adds a new local state query that runs applyTx against the current
ledger state and returns the raw result. The provisional implementation
queries the full EpochState and runs applyTx client-side; this will be
replaced by a dedicated node-side consensus query.

Exposed from Cardano.Api.Query alongside other queries.

From https://github.com/IntersectMBO/cardano-base at 9a18592565cf15b900329095d699997b763b6bd3

The plaintext 64-byte ed25519 scalar is now held in sodium_malloc'd
memory (MLockedSizedBytes 64) throughout its lifetime:
- locked against swapping (mlock)
- never moved by the GC
- zeroed on release via mlsbFinalize

ScrubbedBytes (GC-heap, moveable, swappable) is no longer used for
any secret key material.  The wrapping key (Argon2id output) remains
in ScrubbedBytes for now.

All public crypto operations are now IO (Either XPrvError X).  The
unsafePerformIO facade is gone except for:
- the two global IORef initialisations (runtimeKdfParamsRef, randomModeRef)
- encryptedDerivePublic (pure EC math, no secret key involved)

Callers of encryptedKeyMaterial receive a MLockedSizedBytes 64 and
are responsible for calling mlsbFinalize when done with it.

Adds cardano-crypto-class to library build-depends.

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

Signed-off-by: Chris Gianelloni <[email protected]>