feat(dijkstra): add UTXO and UTXOW preservation-of-value modules

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

Author: williamdemeo

src/Ledger/Dijkstra/Specification/Utxo/Properties/Base.lagda.md

@@ -0,0 +1,80 @@
+---
+source_branch: 1123-cip-159-11-prove-pov-and-invariants
+source_path: src/Ledger/Dijkstra/Specification/Utxo/Properties/Base.lagda.md
+---
+
+# UTXO Properties: Base lemmas (Dijkstra era)
+
+This module collects era-independent helper lemmas used by
+`Utxo.Properties.PoV`{.AgdaModule}.  It currently contains:
+
++  `∙-homo-Coin`{.AgdaFunction}: the `coin` monoid-homomorphism's `_∙_` property.
++  `newTxid⇒disj`{.AgdaFunction}: freshness of `TxIdOf tx` in an existing
+   `utxo` implies `disjoint'`{.AgdaFunction} of `dom utxo`{.AgdaFunction} and
+   `dom (outs tx)`{.AgdaFunction}.
++  `outs-disjoint`{.AgdaFunction}: the specialisation used by
+   `Utxo.Properties.PoV`{.AgdaModule}.
+
+**Not yet ported from Conway**: the `balance`{.AgdaFunction}-arithmetic lemmas
+(`balance-cong`{.AgdaFunction}, `balance-cong-coin`{.AgdaFunction},
+`balance-∪`{.AgdaFunction}, `split-balance`{.AgdaFunction}).  Conway's versions
+rely on `indexedSumᵐ-cong`{.AgdaFunction} over a finite map of hashed TxOuts;
+Dijkstra's `balance`{.AgdaFunction} is defined as `∑ˢ[ v ← valuesOfUTxO utxo ] v`
+(a sum over a `ℙ Value`{.AgdaFunction}), so the Conway proofs don't apply
+verbatim.  Porting them requires the set-theoretic cong lemmas from
+`abstract-set-theory.FiniteSetTheory`{.AgdaModule}; for now, `balance-∪`{.AgdaFunction}
+and `split-balance`{.AgdaFunction} remain as module parameters to
+`Utxo.Properties.PoV`{.AgdaModule}.
+
+<!--
+```agda
+{-# OPTIONS --safe #-}
+
+open import Ledger.Dijkstra.Specification.Abstract    using (AbstractFunctions)
+open import Ledger.Dijkstra.Specification.Transaction
+
+module Ledger.Dijkstra.Specification.Utxo.Properties.Base
+  (txs : _) (open TransactionStructure txs)
+  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
+  where
+
+open import Prelude; open Equivalence
+open import Ledger.Prelude hiding (≤-trans; ≤-antisym; All); open Properties
+open import Ledger.Dijkstra.Specification.Utxo txs abs
+
+open import Algebra.Morphism using (module MonoidMorphisms; IsMagmaHomomorphism)
+
+open MonoidMorphisms.IsMonoidHomomorphism
+
+private variable
+  ℓ : TxLevel
+```
+-->
+
+## `∙-homo-Coin`
+
+```agda
+∙-homo-Coin : ∀ (x y : Value) → coin (x + y) ≡ coin x + coin y
+∙-homo-Coin = IsMagmaHomomorphism.homo (isMagmaHomomorphism coinIsMonoidHomomorphism)
+```
+
+## Freshness ⇒ disjointness
+
+```agda
+module _ (tx : Tx ℓ) (let open Tx tx; open TxBody txBody)
+         {utxo : UTxO} where
+
+  newTxid⇒disj : TxIdOf tx ∉ mapˢ proj₁ (dom utxo)
+               → disjoint' (dom utxo) (dom (outs tx))
+  newTxid⇒disj id∉utxo =
+    disjoint⇒disjoint' λ h h' → id∉utxo $ to ∈-map
+      (-, (case from ∈-map h' of λ where
+            (_ , refl , h'') → case from ∈-map h'' of λ where (_ , refl , _) → refl) , h)
+
+  -- Specialisation used by Utxo.Properties.PoV:
+  -- freshness ⇒ (utxo ∣ SpendInputs ᶜ) and outs are disjoint.
+  outs-disjoint : TxIdOf tx ∉ mapˢ proj₁ (dom utxo)
+                → disjoint (dom (utxo ∣ SpendInputsOf tx ᶜ)) (dom (outs tx))
+  outs-disjoint fresh =
+    λ h₁ h₂ → ∉-∅ $ proj₁ (newTxid⇒disj fresh) $ to ∈-∩ (res-comp-domᵐ h₁ , h₂)
+```