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