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

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.

State and partially prove the Dijkstra LEDGER preservation-of-value
theorem with the corrected HasCoin-LedgerState that includes deposits.

- LEDGER-I (invalid case): Fully proved via utxow-pov-invalid.
- LEDGER-V (valid case): Equational chain with holes, to be filled.

The HasCoin-LedgerState total is:
  getCoin utxoSt + rewardsBalance(certState) + coinFromDeposits(certState)

Key insight: SUBLEDGERS-pov cannot be proved independently because
individual SUBUTXO rules have no balance premise — only the batch-level
consumedBatch ≡ producedBatch constrains the total. The LEDGER-V proof
must reason about the entire step at once.

After all sub-rule transitions (`SUBLEDGERS`, `CERTS`, `GOVS`, `UTXOW`),
apply batch-wide direct deposits to the final CertState via
`applyDirectDeposits` and `allDirectDeposits`.

`Ledger.lagda.md`:
+  Update `LEDGER-V` output: compute `certStateFinal` by applying
   `allDirectDeposits` to `certState₂`, use `certStateFinal` in the
   output `LedgerState` and in `rmOrphanDRepVotes`;
+  `LEDGER-I` unchanged (invalid batches don't apply deposits);
+  Document direct deposit application ordering and phantom asset
   prevention rationale.

`Ledger/Properties/Computational.lagda.md`:
+  Update `computeProof` valid branch to compute `certStateFinal` and use
   it in the output `LedgerState`.

Complete the LEDGER preservation-of-value proof structure for Dijkstra.

- LEDGER-I: Fully proved via utxow-pov-invalid.
- LEDGER-V: Complete equational chain with no holes or unresolved metas.
  Decomposes into:
  - step-i: combined CERTS accounting (sub + top level)
  - arithmetic-1, arithmetic-2: ℕ rearrangements
  - step-iii-iv: batch UTxO + deposit accounting (assumption)
  - step-ii: applyDirectDeposits cancellation (assumption)

New sub-lemma proved:
- SUBLEDGERS-certs-pov: induction on ReflexiveTransitiveClosure showing
  rewardsBalance decreases by exactly the sum of sub-withdrawal amounts.
  Dispatches SUBLEDGER-I (impossible when isTopLevelValid ≡ true) and
  SUBLEDGER-V (uses sub-level CERTS-pov with NetworkId extracted from
  SUBUTXOW → SUBUTXO premises).

Remaining assumptions (module parameters):
- batch-utxo-accounting: consumedBatch ≡ producedBatch coin projection
  combined with mechanical UTxO tracking and deposit accounting
- applyDirectDeposits-rewardsBalance: gc-hom (∪⁺ distributes getCoin)
- utxow-pov-invalid: collateral collection preserves getCoin utxoSt
- ∪ˡ-res-lookup-preserve, sum-map-proj₂≡getCoin, setToList-Unique

Proves by induction on the SUBLEDGERS transition that the UTxO-state
coin total at the start of a sub-tx batch plus all outs + donations
equals the UTxO coin total at the end plus all consumed spend inputs
(compared against the batch-start snapshot `utxo₀`):

```agda
getCoin (UTxOStateOf s₀) + Σ (cbalance (outs stx) + DonationsOf stx)
≡ getCoin (UTxOStateOf s₁) + Σ cbalance (utxo₀ ∣ SpendInputsOf stx)
```

Base case (`BS-base Id-nop`): both sides reduce to `x + 0`, so `refl`.
Inductive case: `SUBLEDGER-I` is impossible under `isTopLevelValid ≡
true`; `SUBLEDGER-V` combines the per-step SUBUTXOW balance with the
IH via an eight-step +-commutative-monoid rearrangement.

Introduces `subutxow-step-coin` as a new module parameter:

```agda
getCoin s₀ + cbalance (outs stx) + DonationsOf stx
≡ getCoin s₁ + cbalance (UTxOOf Γ ∣ SpendInputsOf stx)
```

+  Rationale for keeping this as a parameter at the SUBLEDGERS level:
   proving it locally requires, beyond `balance-∪` and `split-balance`,
   two batch-wide invariants:

   1. the running UTxO agrees with `utxo₀` on every sub-tx's spend
      inputs, and
   2. freshness of each sub-tx's TxId relative to the running UTxO

   neither of which is a local SUBUTXO premise; both follow from
   batch-wide disjointness exposed by the outer UTXO rule and will be
   discharged in a follow-up PR dedicated to general Dijkstra PoV
   infrastructure.

Statement parallels the existing `SUBLEDGERS-certs-pov`, uses
`SubLedgerEnv.utxo₀ Γ` uniformly on the RHS (matching the shape of
`batch-balance-coin`), and is the key lemma needed to derive
`batch-utxo-accounting` internally in the next step of this PR.

Replace the two `coin-of-consumedBatch` / `coin-of-producedBatch` module
parameters of `Utxo/Properties/PoV` with direct proofs.  The proofs are
organised as three layers:

+  Layer 1 — single-transaction coin equations

   `coin-producedTx : coin (producedTx t) ≡ cbalance (outs t) + DonationsOf t + getCoin (DirectDepositsOf t)`

   `coin-consumedTx : coin (MintedValueOf t) ≡ 0 → coin (consumedTx t utxo₀) ≡ cbalance (utxo₀ ∣ SpendInputsOf t) + getCoin (WithdrawalsOf t)`

   Each is a direct unfolding: repeated `∙-homo-Coin` to distribute `coin`
   across `+`, followed by `coin∘inject≗id` to strip each `inject`.  The
   consumed version additionally uses `coin (MintedValueOf t) ≡ 0` to cancel
   the mint term (from UTXO premise p₆ / SUBUTXO premise).

+  Layer 2 — sum-over-sub-transactions coin equations

   `coin-∑-producedTx-sub` : pushes `coin` through the `∑ˡ`-indexed sum over
   `SubTransactionsOf tx` using the new `coin-∑ˡ` lemma (from
   `Utxo/Properties/Base`), then applies Layer 1 pointwise by list induction.

   `coin-∑-consumedTx-sub` : same shape, threading a `noMintingSubTxs tx`
   hypothesis (`∀ stx → stx ∈ˡ SubTransactionsOf tx → coin (MintedValueOf stx) ≡ 0`)
   through the induction so each element's Layer-1 application has its
   `noMint` premise available.

+  Layer 3 — the two batch-level coin equations

   `coin-of-consumedBatch` and `coin-of-producedBatch`: unfold the outer
   `+ inject _` / `+ ∑ˡ _` structure of `consumedBatch` / `producedBatch` by
   repeated `∙-homo-Coin` and `coin∘inject≗id`, substitute the Layer-1
   top-level equation for the top-level summand, and substitute the Layer-2
   equation for the sub-transaction sum.

   The produced-side proof ends with a small associative-commutative shuffle
   (`reshape-top`) that reorders the top-level fields from
   `(outs + Donations + DirectDeposits) + TxFees` to the stated
   `outs + TxFees + Donations + DirectDeposits`.  The shuffle uses the same
   `swap-right` helper already used in `UTXO-V-mechanical`.

+  Supporting change

   Adds a small helper alias `noMintingSubTxs` at the top of the file to keep
   the sub-level mint-conservation hypothesis readable in the theorem
   statements.

All proofs typecheck under `--safe`.  The `UTXO-pov` placeholder remains;
this commit delivers the coin-balance infrastructure that the eventual
full proof (and the LEDGER-pov's `BatchUtxoAccounting` consumer) will
depend on.

CIP-159 changes the transaction balancing rules and introduces Phase-1
balance interval validation.  This commit updates the UTxO transition
system accordingly.

`Utxo.lagda.md`:
+  Add accountBalances : Rewards field to UTxOEnv and SubUTxOEnv for
   pre-batch account balance lookups;
+  Add HasAccountBalances type class and instances;
+  Update producedTx to include direct deposit amounts on the produced
   side of the preservation-of-value equation;
+  Add direct deposit registration premise to UTXO and SUBUTXO
   (`dom DirectDepositsOf ⊆ dom AccountBalancesOf`);
+  Add balance interval validation premise to UTXO and SUBUTXO
   (∀ (c,interval) ∈ BalanceIntervalsOf, InBalanceInterval using
   pre-batch account balances).

`Utxo/Properties/Computational.lagda.md`:
+  Update Computational-UTXO for new premise tuple arity (19+h → 21+h)

`Ledger.lagda.md`:
+  Add accountBalances field to SubLedgerEnv;
+  Populate accountBalances in SUBLEDGER-V, SUBLEDGER-I, LEDGER-V,
   LEDGER-I using RewardsOf certState₀ (pre-batch balances).

Add the applyWithdrawals preservation-of-value proof machinery and
prove several lemmas that were previously assumed as module parameters
in Conway.

New proofs in Ledger.Prelude (previously Conway module parameters):
- indexedSumᵛ'-∪: getCoin distributes over disjoint ∪ˡ
- sumConstZero: getCoin (constMap X 0) ≡ 0
- getCoin-cong: indexedSum' proj₂ respects set equality
- res-decomp: (m ∪ˡ m') ≡ᵉ (m ∪ˡ (m' ∣ dom m ᶜ))
- getCoin-singleton, ≡ᵉ-getCoin, ∪ˡsingleton∈dom, ∪ˡsingleton∉dom,
  ∪ˡsingleton0≡: singleton map getCoin lemmas
- indexedSumL-proj₂-zero: sum of zero-valued entries is zero
- setToList-∈: opaque bridge from list membership to set membership

New module Certs.Properties.ApplyWithdrawalsPoV:
- applyOne-pov: single withdrawal step decreases getCoin by amt
- foldl-applyOne-pov: fold induction with Unique invariant
- applyWithdrawals-pov: top-level lemma for PRE-CERT-pov
- ∪ˡ-res-dom-preserve: ∪ˡ with complement restriction preserves
  domain membership for other credentials

Remaining assumptions (deferred to agda-sets library):
- ∪ˡ-res-lookup-preserve: lookupᵐ? stability under ∪ˡ for other keys
- sum-map-proj₂≡getCoin: relates list-level sum to indexedSumᵛ'
- setToList-Unique: credential uniqueness of withdrawal list
- ≡ᵉ-getCoinˢ: getCoin invariance under injective key renaming

Each transaction's `txDirectDeposits` are now applied to the threaded
`CertState` immediately after that transaction's `CERTS` step, replacing
the batch-wide application introduced earlier on this branch.

  * `SUBLEDGER-V` applies `DirectDepositsOf stx` to `certState₁` after
    `CERTS` and emits the result.
  * `LEDGER-V` still applies the top-level transaction's deposits to
    `certState₂` after the top-level `CERTS`, but the premise now bounds
    `dom (DirectDepositsOf tx)` rather than the batch aggregate
    `dom (allDirectDeposits tx)`.
  * `certStateWithDDeps` is generalised to
    `∀ {ℓ} → Tx ℓ → CertState → CertState` so both rules can invoke it
    with the local `DirectDepositsOf`.

The original draft of this branch argued that batch-wide application
made CIP-159's phantom-asset prohibition manifest in the rule
structure.  Per-transaction application is equally safe: the prohibition
is enforced separately by `NoPhantomWithdrawals` in the `Utxo` module,
which bounds batch-wide withdrawal totals against the `accountBalances`
field of `UTxOEnv`/`SubUTxOEnv` — fixed at the pre-batch snapshot
`RewardsOf certState₀` regardless of when (or how) deposits are applied
to the threaded `CertState`.  Per-transaction application also mirrors
the Haskell ledger executor's sequential per-transaction processing,
which simplifies the conformance proof and avoids a structural gap
between the spec and the implementation.

A direct-deposit registration premise is added to each rule to prevent
`applyDirectDeposits` from silently re-introducing a credential into
`rewards` after deregistration earlier in the same transaction:

  * `SUBLEDGER-V` requires
    `dom (DirectDepositsOf stx) ⊆ dom (RewardsOf certState₁)`.
  * `LEDGER-V` requires
    `dom (DirectDepositsOf tx)  ⊆ dom (RewardsOf certState₂)`.

The check is local to each transaction's post-`CERTS` state, so a
sub-transaction whose deposit targets a credential deregistered by an
earlier sub-transaction in the same batch will fail the premise.

`Computational-SUBLEDGER` and `Computational-LEDGER` are updated to
dispatch on these decidable premises in `computeProof` and
`completeness`.  `depositsChange` is unaffected: it reads only the
protocol-deposit fields of `DState`/`PState`/`GState`, which
`applyDirectDeposits` does not touch.

Refs: #1122

Each transaction's `txDirectDeposits` are now applied to the threaded
`CertState` immediately after that transaction's `CERTS` step, replacing
the batch-wide application introduced earlier on this branch.

  * `SUBLEDGER-V` applies `DirectDepositsOf stx` to `certState₁` after
    `CERTS` and emits the result.
  * `LEDGER-V` still applies the top-level transaction's deposits to
    `certState₂` after the top-level `CERTS`, but the premise now bounds
    `dom (DirectDepositsOf tx)` rather than the batch aggregate
    `dom (allDirectDeposits tx)`.
  * `certStateWithDDeps` is generalised to
    `∀ {ℓ} → Tx ℓ → CertState → CertState` so both rules can invoke it
    with the local `DirectDepositsOf`.

The original draft of this branch argued that batch-wide application
made CIP-159's phantom-asset prohibition manifest in the rule
structure.  Per-transaction application is equally safe: the prohibition
is enforced separately by `NoPhantomWithdrawals` in the `Utxo` module,
which bounds batch-wide withdrawal totals against the `accountBalances`
field of `UTxOEnv`/`SubUTxOEnv` — fixed at the pre-batch snapshot
`RewardsOf certState₀` regardless of when (or how) deposits are applied
to the threaded `CertState`.  Per-transaction application also mirrors
the Haskell ledger executor's sequential per-transaction processing,
which simplifies the conformance proof and avoids a structural gap
between the spec and the implementation.

A direct-deposit registration premise is added to each rule to prevent
`applyDirectDeposits` from silently re-introducing a credential into
`rewards` after deregistration earlier in the same transaction:

  * `SUBLEDGER-V` requires
    `dom (DirectDepositsOf stx) ⊆ dom (RewardsOf certState₁)`.
  * `LEDGER-V` requires
    `dom (DirectDepositsOf tx)  ⊆ dom (RewardsOf certState₂)`.

The check is local to each transaction's post-`CERTS` state, so a
sub-transaction whose deposit targets a credential deregistered by an
earlier sub-transaction in the same batch will fail the premise.

`Computational-SUBLEDGER` and `Computational-LEDGER` are updated to
dispatch on these decidable premises in `computeProof` and
`completeness`.  `depositsChange` is unaffected: it reads only the
protocol-deposit fields of `DState`/`PState`/`GState`, which
`applyDirectDeposits` does not touch.

Refs: #1122

After all sub-rule transitions (`SUBLEDGERS`, `CERTS`, `GOVS`, `UTXOW`),
apply batch-wide direct deposits to the final CertState via
`applyDirectDeposits` and `allDirectDeposits`.

`Ledger.lagda.md`:
+  Update `LEDGER-V` output: compute `certStateFinal` by applying
   `allDirectDeposits` to `certState₂`, use `certStateFinal` in the
   output `LedgerState` and in `rmOrphanDRepVotes`;
+  `LEDGER-I` unchanged (invalid batches don't apply deposits);
+  Document direct deposit application ordering and phantom asset
   prevention rationale.

`Ledger/Properties/Computational.lagda.md`:
+  Update `computeProof` valid branch to compute `certStateFinal` and use
   it in the output `LedgerState`.
+  Clean up redundant code.

`applyDirectDeposits` uses `∪⁺` (union-with-addition) on the `rewards`
map, so a credential not present in `RewardsOf certState₂` is added as a
new entry rather than rejected.  The pre-existing SUBUTXO/UTXO premise
`dom (DirectDepositsOf tx) ⊆ dom (AccountBalancesOf Γ)` only checks
against the pre-batch balances `RewardsOf certState₀`, so it does not
catch the case where a credential is registered pre-batch, deregistered
during `CERTS`, and direct-deposited to in the same batch.  Without the
new premise, the resulting `certStateFinal` is internally inconsistent:
the credential has a positive `rewards` entry but no corresponding
`voteDelegs`, `stakeDelegs`, or `deposits` entry — effectively re-
registering the credential without a key deposit.

Add the phase-1 premise

    dom (allDirectDeposits tx) ⊆ dom (RewardsOf certState₂)

to `LEDGER-V` to rule this out.  Filtering `allDirectDeposits tx` by
`dom (RewardsOf certState₂)` would be an alternative, but it would
silently destroy user funds when a deposit and a deregistration race in
the same batch.  The premise is symmetric to (and complements) the
existing pre-batch SUBUTXO/UTXO check.

Update `Ledger/Properties/Computational.lagda.md` for the new premise,
and pass `UTxOStateOf s₁` explicitly to `computeUtxow` in the LEDGER
valid branch (the previous `_` resolved by chained unification through
the LEDGER-V constructor, which was fragile and obscured intent).

TODO: fix `Ledger/Properties/Computational.lagda.md`; it's choking on
the new premise.

Nixpkgs expects to drop support for intel macs in 26.11.

* Add Dijkstra Foreign modules

* NativeScripts; add DecEq-Network as an explicit parameter to avoid agda bug

for bug report see https://github.com/agda/agda/issues/8532