WIP -- [Dijkstra] CIP-159-11b: Prove UTxO and UTxOW preservation of value (#1186)

[williamdemeo]

[!WARNING]

🔖 Resume here — session hand-off 2026-06-16 (dependency provider; NOT yet on Entities refactor)

Top-down reorder: this PR provides the UTxO/UTxOW-PoV facts that discharge #1203's UTxO-side module parameters. Complete it AFTER #1203's skeleton fixes the exact statements needed (prove only those).

⚠️ Not updated for the Entities refactor (#1201). Still based on the pre-Entities branch 1185-dijkstra-certs-pov; last touched 2026-05-20; CI predates the current formal-ledger-agda job.

To finish:

1. Port onto the Entities refactor (Add ENTITIES rule #1201) and rebase onto current master (bd56c87); retarget base to master.
2. Discharge deferred params balance-∪, split-balance, outs-disjoint (last is local via the already-proved newTxid⇒disj).
3. Fill the UTXO-pov {!!} to match the statement WIP -- [Dijkstra] CIP-159-11c: Prove LEDGER preservation of value (#1187) #1203 actually consumes.
4. Re-run CI (now includes the Agda typecheck) and confirm green.

---

Description

Closes #1186.

This PR adds the preservation-of-value (PoV) building blocks for the Dijkstra UTXO and UTXOW rules. These are the UTxO-side ingredients consumed by the LEDGER-level proof in sub-issue #1187; this PR does not itself prove a complete UTXO-pov theorem (that statement's exact shape depends on how LEDGER-pov threads sub-transaction state).

This PR is the second of three replacing the original PR #1169, which has been split along module-tree boundaries. It contains only the Utxo/Properties and Utxow/Properties sub-trees. It targets the branch of PR #<new-A> (Certs PoV) so that CI sees the full PoV chain in order; once #<new-A> merges, this PR will be retargeted to master.

---

Modules

Module	Purpose	Status
Utxo.Properties.Base	∙-homo-Coin, newTxid⇒disj, outs-disjoint, coin-∑ˡ	Proved
Utxo.Properties.PoV	UTXO-level PoV building blocks	Mostly proved
Utxow.Properties.PoV	UTXOW⇒UTXO extractor + delegated wrappers	Proved

---

What's proved

The Dijkstra UTXO PoV proof decomposes into two orthogonal pieces, matching the batch structure of the rule.

Mechanical state change

UTXO-I-getCoin (invalid case: collateral collection preserves getCoin) and UTXO-V-mechanical (valid case: additive rearrangement relating getCoin s₀ to getCoin s₁ via split-balance + balance-∪). Both proved.

Batch coin balance

batch-balance-coin — the coin projection of the consumedBatch ≡ producedBatch premise (premise p₇ of the UTXO rule) — proved via a three-layer structure.

1. Per-transaction (coin-producedTx, coin-consumedTx). Unfold producedTx / consumedTx and peel coin through each + inject _ layer using ∙-homo-Coin + coin∘inject≗id. The consumed version uses coin (MintedValueOf t) ≡ 0 (UTXO premise p₆ for top-level, SUBUTXO premise for sub-transactions) to cancel the mint term.

2. Sum over sub-transactions (coin-∑-producedTx-sub, coin-∑-consumedTx-sub). Push coin through the ∑ˡ-indexed sum using the new coin-∑ˡ lemma (a four-line monoid-homomorphism induction in Utxo.Properties.Base), then apply the per-transaction equations pointwise. The consumed version threads noMintingSubTxs tx through the sub-tx list induction.

3. Batch level (coin-of-consumedBatch, coin-of-producedBatch). Peel the outer + inject _ layers, substitute Layer 1 for the top-level summand and Layer 2 for the sub-transaction sum, and finish with a small associative-commutative shuffle using a swap-right helper.

UTXOW-level

UTXOW-I-getCoin, UTXOW-V-mechanical, UTXOW-batch-balance-coin, and utxow-pov-invalid are thin wrappers. Both UTXOW-normal and UTXOW-legacy embed a UTXO derivation as their final premise, so a single UTXOW⇒UTXO extractor reduces every statement to its UTXO-level counterpart.

Combined UTXO-pov statement

The combined UTXO-pov theorem is stated but left as a placeholder ({!!}) — its exact form depends on how the consumer (LEDGER-pov, sub-issue #<C>) threads sub-transaction state. All three of its building blocks (UTXO-I-getCoin, UTXO-V-mechanical, batch-balance-coin) are already proved.

---

Outstanding proof obligations

balance-∪ and split-balance are taken as module parameters of Utxo.Properties.PoV. The Conway versions of these lemmas rely on indexedSumᵐ-cong over a finite map of hashed TxOuts; Dijkstra defines balance as ∑ˢ over a ℙ Value, so the Conway proofs do not apply verbatim. Porting them requires the set-theoretic cong lemmas from abstract-set-theory.FiniteSetTheory and is era-independent enough to be tracked as its own follow-up.

outs-disjoint is also taken as a module parameter; once newTxid⇒disj (already proved in Utxo.Properties.Base) is combined with the appropriate UTxO disjointness reasoning, this can be discharged locally.

---

Design notes

λ {u}{u'} → η-wrapping

Passing balance-∪ directly to UTXOW-PoV triggers Agda to eta-expand the {u u' : UTxO} implicits through UTxO's Σ _ left-unique record structure, leaving the left-unique field as an unresolved meta. Binding {u}{u'} as pattern variables in an outer lambda makes them concrete bound values and sidesteps the eta-expansion. This pattern is used at the UTXOW⇒UTXO instantiation site.

Why no per-step "before/after" theorem at the UTXO level

Unlike Conway, the mechanical state change alone (for the valid case) does not suffice to prove a local getCoin s₀ ≡ getCoin s₁ equation, because

• utxoSt₀ passed to the UTXO rule at the LEDGER level is the post-SUBLEDGERS state, not the pre-batch state, so in general UTxOOf utxoSt₀ ≢ UTxOOf Γ; and
• the batch balance equation relates UTxOOf Γ (the pre-batch snapshot) to quantities summed over the entire batch, not just the top-level tx.

Consequently, deriving a full value-preservation statement for the UTXO rule alone requires threading information about the preceding SUBLEDGERS step — work that is done in LEDGER-pov (sub-issue #<C>), not here.

---

Checklist

• Commit sequence broadly makes sense and commits have useful messages
• Any semantic changes to the specifications are documented in CHANGELOG.md
• Code is formatted according to CONTRIBUTING.md
• Self-reviewed the diff