Cardano Updates

Introduce three new modules implementing the UTXO-level building blocks
of the Dijkstra-era preservation-of-value proof (towards closing #1123 /
CIP-159-11):

+  `Utxo/Properties/Base.lagda.md`
   Era-independent helper lemmas: `∙-homo-Coin`, `newTxid⇒disj`,
   `outs-disjoint`.  Intentionally minimal for now — the Conway Base
   proofs of `balance-cong`, `balance-∪`, and `split-balance` do not
   port verbatim because Dijkstra defines `balance` as `∑ˢ` over a set
   of Values rather than as `indexedSumᵐ` over a map of hashed TxOuts.
   Tracking issue filed for the proper port.

+  `Utxo/Properties/PoV.lagda.md`
   The Dijkstra UTXO preservation-of-value proof is split into two
   orthogonal pieces:

   -  Mechanical state change (`UTXO-I-getCoin`, `UTXO-V-mechanical`):
      relates `getCoin s₀` to `getCoin s₁` from the UTxOState transition
      alone, using `split-balance` and `balance-∪`.  Proved.

   -  Batch coin balance (`batch-balance-coin`): the coin projection of
      the `consumedBatch ≡ producedBatch` premise (premise p₇ of the
      UTXO rule).  Proved from the two module parameters
      `coin-of-consumedBatch` and `coin-of-producedBatch`, which are
      themselves left as assumptions for now (see PoV follow-up work).

   The combined `UTXO-pov` theorem is stated but left as a placeholder
   (`?`); its exact form depends on how `LEDGER-pov`'s
   `BatchUtxoAccounting` consumer threads sub-transaction state.

+  `Utxow/Properties/PoV.lagda.md`
   UTXOW-level wrappers that extract the UTXO derivation from either
   `UTXOW-normal` or `UTXOW-legacy` (via a shared `UTXOW⇒UTXO`
   extractor) and delegate to the UTXO-level lemmas.  Provides
   `utxow-pov-invalid` in the exact shape required as a module
   parameter by `Ledger/Properties/PoV.lagda.md`.

Proof-internal notes:

+  `balance-∪` and `split-balance` are currently module parameters
   to `Utxo/Properties/PoV` pending the port of Conway Base's balance
   arithmetic to Dijkstra (see tracking issue).

+  The 7-term +-commutative-monoid shuffle in `UTXO-V-mechanical` is
   proved by hand using a `swap-right` helper; this could later be
   replaced by a call to a commutative-monoid solver.

+  All three modules typecheck under `--safe`.

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

Add confirmed tx throughput to proto-devnet dashboard