Cardano Updates

Also switch from package memory to package ram.

Replaces console.log with silent error handling to prevent leaking error details
to stdout in production. Matches the error handling pattern used in JWT.verify().

Signed-off-by: A-Chronicle <[email protected]>

- Use numeric underscore: 21600 -> 21_600
- Remove redundant lambda and void: \i -> void . insertTx $ bigTx i -> insertTx . bigTx

Introduces a new package providing authenticated v2 envelope wrapping
for Byron HD wallet extended private keys.

Key design:
- C layer handles ed25519 key generation, public-key derivation, signing,
  and BIP32 child derivation; it stores and operates on plaintext key
  material only
- Haskell layer owns all encryption: Argon2id key derivation
  (128 MiB, t=3, p=4) and XChaCha20-Poly1305 AEAD wrapping with a
  freshly randomized salt and nonce per write
- CBOR-encoded versioned envelope with explicit associated data binding
  format version, KDF parameters, cipher, payload shape, public key,
  and chain code — preventing silent swaps without detection
- Fail-closed public API: passphrase-using operations return Either and
  reject wrong passphrases at authentication time
- Test helpers for fast-KDF and deterministic randomness modes keep the
  test suite sub-second without touching production paths
- Benchmark suite covers create, validate, sign, and change-passphrase
  under production Argon2id parameters

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

Add preservation-of-value property modules for the Dijkstra era,
adapted from the Conway PoV proof structure for CIP-159 (partial
withdrawals and direct deposits).

New modules:
- Certs.Properties.PoVLemmas: CERT-pov, POST-CERT-pov, sts-pov,
  PRE-CERT-pov (adapted for applyWithdrawals subtraction semantics)
- Certs.Properties.PoV: CERTS-pov top-level theorem
- Certs.Properties.ApplyWithdrawalsPov: Key new lemma showing
  applyWithdrawals decreases rewardsBalance by exactly getCoin wdrls
- Ledger.Properties.PoV: HasCoin instances, LEDGER-pov statement
  with proof sketch for direct deposit cancellation

Design notes:
- PRE-CERT-pov delegates to applyWithdrawals-pov (fold induction)
  instead of Conway's constMap/res-decomp/sumConstZero chain
- LEDGER-pov identifies the applyDirectDeposits cancellation as the
  main new proof obligation vs Conway
- applyWithdrawals-pov is structured as three layers: single-step
  (applyOne-pov), fold induction (foldl-applyOne-pov), top-level

Status: Skeleton with holes; does not yet fully typecheck.

There were unresolved proof obligations from Conway.