[Dijkstra] CIP-159-11: Prove preservation of value and invariant properties for CIP-159

# Description

**Depends on**: Issues #1116, #1117, #1120, #1122

This issue tracks the preservation-of-value (PoV) and invariant work for CIP-159 in the Dijkstra-era formal ledger specification. The work has been split into three sibling sub-issues, each closed by its own PR; this issue serves as the umbrella tracker.

CIP-159 changes the value flow in the ledger by introducing direct deposits (value flowing from UTxO world to account balances) and partial withdrawals (value flowing from accounts to UTxO world in potentially smaller amounts). These changes affect the PoV proofs and introduce new invariants that need to be stated and proved.

## Split into sub-issues

| Sub-issue | Scope | PR |
|-----------|-------|----|
| #1185 | Certs PoV (`CERTS-pov`, `CERT-pov`, `PRE-CERT-pov`, `applyWithdrawals-pov`) | TBD |
| #1186 | UTxO and UTxOW PoV (`UTXO-V-mechanical`, `batch-balance-coin`, `UTXOW⇒UTXO`) | TBD |
| #1187 | LEDGER PoV (top-level `LEDGER-pov` theorem) | TBD |

## Architecture context

The Dijkstra PoV proof structure differs from Conway in several important ways.

1. **`UTxOState` has 3 fields** (`utxo`, `fees`, `donations`) — deposits are tracked in `CertState`, not `UTxOState`. So `getCoin UTxOState` = `getCoin utxo + fees + donations`.

2. **`LedgerState` total value** is `getCoin utxoSt + getCoin certState + coinFromDeposits certState`, where `getCoin certState` is the rewards/account balance total and `coinFromDeposits certState` accumulates the protocol-level deposits across `DState`/`PState`/`GState`.

3. **The `consumed ≡ produced` equation** is a conjunct in `UTXO-Premises` (not an inline premise). It uses `consumedBatch`/`producedBatch` parameterized by `DepositsChange`, and there is a separate legacy-mode check (`consumed ≡ produced` for the top-level alone).

4. **`UTXOS` is trivial** (`⊤ → ⊤`) — it only checks script evaluation. State modification happens in `UTXO-valid`/`UTXO-invalid`.

5. **Direct deposits are applied per-transaction** (as of #1161). The helper `certStateWithDDeps tx cs = record cs { dState = applyDirectDeposits (DirectDepositsOf tx) (DStateOf cs) }` is invoked once per transaction in the batch — once for each sub-transaction inside `SUBLEDGER-V`, plus once for the top-level transaction inside `LEDGER-V`. Because `applyDirectDeposits` only modifies `rewards`, applying it per-transaction is *equivalent* to aggregating all direct deposits via `∪⁺` and applying the sum at the end.

6. **The Conway `LEDGER-PoV` proof** decomposes into `UTXOpov` and `CERTS-pov` with the key equation `getCoin utxoSt + getCoin certState ≡ getCoin utxoSt' + getCoin certState'`. The proof hinges on `CERTS-pov`: `getCoin s₁ ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ)`. CIP-159 changes both sides: `CERTS-pov` retains its statement but is reproved using `applyWithdrawals-pov` (since `PRE-CERT` now subtracts withdrawal amounts rather than zeroing the entries), and the LEDGER-level decomposition acquires a new "direct deposit" term that appears on both the produced side of `consumedBatch ≡ producedBatch` and on the CertState side via the `certStateWithDDeps` step, so that the two cancel in the total.

## Properties to state and prove

### 1. LEDGER preservation of value (updated)

The total value in the system is preserved across a `LEDGER` transition. With CIP-159, the total includes account balances, and value can transfer between the UTxO side and the account-balance side via direct deposits.

```agda
-- Total system value:
-- Dijkstra UTxOState has 3 fields (no deposits), so:
-- getCoin utxoSt = cbalance utxo + fees + donations
-- CertState getCoin counts only rewards (account balances).
-- coinFromDeposits accounts for DState, PState, GState protocol-level deposits.
HasCoin-LedgerState : HasCoin LedgerState
HasCoin-LedgerState .getCoin s =
getCoin (UTxOStateOf s) -- cbalance + fees + donations
+ getCoin (CertStateOf s) -- rewards
+ coinFromDeposits (CertStateOf s) -- DState+PState+GState deposits
```

**Claim.** `getCoin s ≡ getCoin s'` when `Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s'`.

The proof must account for the following.

+ Direct deposits move value from `producedBatch` (UTxO side, via the new `DirectDepositsOf` term included in each `producedTx`) to `CertState` (via `certStateWithDDeps`, which calls `applyDirectDeposits` on the post-`CERTS` `DState`). These cancel in the total.
+ Partial withdrawals move value from account balances (`CertState`) to `consumedBatch` (UTxO side, via `WithdrawalsOf`). The amount withdrawn appears on both sides: subtracted from `getCoin certState` and added to `getCoin utxoSt`.
+ The `DepositsChange` threading (computed from `CertState` diffs via `calculateDepositsChange`) is orthogonal — it tracks registration deposits (DState/PState/GState `deposits` fields), not direct deposits (DState `rewards` field).

This is the scope of sub-issue #1187.

### 2. Batch-wide PoV (updated)

The `consumedBatch ≡ producedBatch` equation in `UTXO-Premises` includes direct deposits on the produced side.

```agda
consumedBatch (DepositsChangeOf Γ) txTop (UTxOOf Γ) ≡ producedBatch (DepositsChangeOf Γ) txTop
```

Where `producedBatch` sums `producedTx` over the batch, and each `producedTx` includes `inject (getCoin (DirectDepositsOf tx))`. The `consumedBatch` side includes `inject (getCoin (WithdrawalsOf tx))` for each transaction. The coin projection of this equation is proved as `batch-balance-coin` and threaded into the LEDGER-level proof.

This is part of the scope of sub-issue #1186.

### 3. Direct-deposit registration invariant

**Claim.** If a `LEDGER` transition succeeds, then the credentials receiving direct deposits in any transaction (top-level or sub-transaction) are registered in the *post-`CERTS`* `CertState` of that same transaction.

```agda
dom (DirectDepositsOf tx) ⊆ dom (RewardsOf certState₂) -- top-level
dom (DirectDepositsOf stx) ⊆ dom (RewardsOf certState₁) -- per sub-transaction
```

This follows from the phase-1 preconditions in `LEDGER-V` (top-level) and `SUBLEDGER-V` (sub-transactions). The check is performed against the post-`CERTS` state of *the same* transaction, so deregistrations performed by *prior* sub-transactions in the batch are correctly accounted for: a sub-transaction whose deposit targets a credential deregistered by an earlier sub-transaction will fail its own premise.

### 4. Phantom asset invariant

**Claim.** For any batch, the total withdrawn amount from any credential does not exceed the *pre-batch* balance of that credential.

```agda
∀ c . totalWithdrawn c txTop ≤ lookupOr 0 c (RewardsOf (DStateOf certState₀))
```

This is directly enforced by the `NoPhantomWithdrawals` conjunct in `UTXO-Premises` (issue #1120) and is provable from the `LEDGER` rule premises. The bound is against the `accountBalances` field of `UTxOEnv`, which is fixed at `RewardsOf certState₀` (the pre-batch snapshot) and never updated mid-batch — so direct deposits applied earlier in the batch do not inflate the balance available to later withdrawals.

### 5. Non-negative account balance invariant

**Claim.** Account balances remain non-negative after a `LEDGER` transition.

```agda
∀ c . lookupOr 0 c (RewardsOf (DStateOf certStateFinal)) ≥ 0
```

This follows from: pre-batch balances are non-negative (inductive hypothesis from `Rewards = Credential ⇀ Coin`, where `Coin = ℕ`); withdrawals are bounded by pre-batch balances (phantom-asset prevention, #1120); and direct deposits are non-negative (`Coin` values are natural numbers). In Dijkstra, since `Rewards = Credential ⇀ Coin` and `Coin = ℕ`, non-negativity is trivially guaranteed by the type system. The real content of this invariant is that the subtraction performed by `applyWithdrawals` in `PRE-CERT` does not underflow, which is ensured by the phantom-asset prevention bound (and is what `applyWithdrawals-pov` actually proves).

### 6. Balance-interval satisfaction (soundness)

**Claim.** If a `LEDGER` transition succeeds and a transaction specifies balance intervals, those intervals were satisfied by the pre-batch account balances.

This is trivially an invariant since it is a conjunct in `UTXO-Premises`/`SUBUTXO-Premises`, but stating it explicitly documents the intended semantics.

### 7. CERTS preservation of value (updated for partial withdrawals)

The Conway `CERTS-pov` proves

```agda
getCoin s₁ ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ)
```

assuming full withdrawals: the withdrawn amount equals the account balance for each withdrawn credential. With partial withdrawals, the equation still holds — `getCoin (WithdrawalsOf Γ)` is the *actual amount withdrawn* (the value specified in the transaction), not the full balance — but the proof structure is different.

The key change is in `PRE-CERT`: instead of `constMap wdrlCreds 0 ∪ˡ rewards` (which zeros out withdrawn credentials), the new rule applies `applyWithdrawals wdrls rewards`, which subtracts each withdrawal amount. The `PRE-CERT-pov` lemma is reproved using a new `applyWithdrawals-pov` lemma based on fold induction rather than map decomposition.

This is the scope of sub-issue #1185.

### 8. SUBLEDGER / SUBLEDGERS preservation of value

**Claim.** The `SUBLEDGERS` transition relates the pre-batch `LedgerState` to the post-`SUBLEDGERS` `LedgerState` by accounting for sub-transaction withdrawals (consumed-side) and per-sub-transaction direct deposits (produced-side, applied via `certStateWithDDeps`).

This is needed as a lemma for the batch-wide LEDGER-PoV. The `SUBLEDGER-V` case processes `SUBUTXOW`, `CERTS`, and `GOVS` for each sub-transaction, then applies that sub-transaction's direct deposits to its post-`CERTS` `CertState`. The composite `SUBLEDGERS-pov` lemma combines `CERTS-pov` per sub-transaction with the equational reasoning that tracks the running `CertState` through the chain.

This is part of the scope of sub-issue #1187 (LEDGER PoV).

## Proof strategy summary

The Dijkstra LEDGER-PoV proof follows the Conway template with the following differences.

1. **Decompose** `getCoin s ≡ getCoin s'` into `getCoin utxoSt + getCoin certState + coinFromDeposits certState ≡ getCoin utxoSt' + getCoin certStateFinal + coinFromDeposits certState'`.
2. **Account for direct deposits**. In `LEDGER-V`, `certStateFinal = certStateWithDDeps tx certState₂`, so `getCoin certStateFinal = getCoin certState₂ + getCoin (DirectDepositsOf tx)`. Sub-transaction direct deposits are similarly accumulated through the `SUBLEDGERS` chain.
3. **Use the batch PoV equation** (`consumedBatch ≡ producedBatch` from `UTXO-Premises`), which includes direct deposits on the produced side and withdrawals on the consumed side, summed across the entire batch.
4. **Use `CERTS-pov`** (updated for partial withdrawals) to relate `getCoin certState₁` to `getCoin certState₂` plus the top-level withdrawal total; combine with the per-sub-transaction `CERTS-pov` invocations across `SUBLEDGERS`.
5. **Show cancellation**. Direct deposit amounts appear in `producedBatch` (UTxO side) and in `getCoin certStateFinal` (CertState side), so they cancel in the total.
6. **Posiive/negative deposit accounting**. The `coinFromDeposits` term changes by `DepositsChangeTop + DepositsChangeSub` (signed), and the `consumedBatch ≡ producedBatch` equation includes corresponding `posPart` / `negPart` summands that cancel via the `posNeg-deposits` identity.

The main new challenge versus Conway is step 2: the per-transaction `applyDirectDeposits` step creates a value transfer between the two "pots" (UTxOState and CertState) that must be tracked through the proof. Per-transaction application makes the proof slightly easier than batch-wide application would have, because each transaction's direct-deposit total appears next to its own `producedTx` term in `producedBatch`.

## Acceptance criteria

- [ ] `HasCoin-LedgerState` defined for Dijkstra's `LedgerState` (already exists in `Ledger.lagda.md`).
- [ ] LEDGER-PoV stated with direct deposits included in the value accounting.
- [ ] Batch-wide PoV (`consumedBatch ≡ producedBatch`) verified against updated definitions.
- [ ] CERTS-pov updated for partial withdrawals.
- [ ] Non-negative account balance invariant stated.
- [ ] Phantom asset invariant stated.
- [ ] At least the key properties (LEDGER-PoV, non-negative balances) are proved, or stated as `Claim` with a clear proof sketch.
- [ ] All property modules compile with `--safe`.

Detailed acceptance criteria for each sub-component are in the corresponding sub-issue.

## Design notes

+ Some properties may initially be stated as `Claim` (unproved) and proved later. The priority is to state them correctly so they serve as regression tests as the formalization evolves.
+ The non-negative balance invariant is crucial for the soundness of the phantom-asset prevention: if balances could go negative (via underflow), the withdrawal bound check would be unsound. Since `Coin = ℕ`, the type system prevents negative balances, but the invariant that `applyWithdrawals` does not violate the `Rewards` map structure is still worth stating — and is exactly what `applyWithdrawals-pov` proves.
+ The Dijkstra UTxO PoV proof differs from Conway because deposits are not in `UTxOState`. The `DepositsChange` threading through `UTxOEnv` is used in `consumed`/`produced` but does not affect the UTxO state transition directly — it only appears in the PoV equation.
+ The Conway `LEDGER-I` PoV proof uses `cong (_+ rewardsBalance dState)` because `certState` is unchanged. The same pattern applies in Dijkstra: direct deposits are not applied in the invalid case (no `certStateWithDDeps` step in `LEDGER-I`).

## References

+ Conway PoV proofs: `Ledger.Conway.Specification.Ledger.Properties.PoV`, `Ledger.Conway.Specification.Utxo.Properties.PoV`, `Ledger.Conway.Specification.Certs.Properties.PoV`.
+ Existing Dijkstra properties: `Ledger.Dijkstra.Specification.Utxo.Properties`, `Ledger.Dijkstra.Specification.Certs.Properties`.
+ `UTXO-Premises` in `src/Ledger/Dijkstra/Specification/Utxo.lagda.md`.
+ `LEDGER-V` / `LEDGER-I` in `src/Ledger/Dijkstra/Specification/Ledger.lagda.md`.
+ `calculateDepositsChange`, `certStateWithDDeps`, and `applyDirectDeposits` (from #1115 and #1122).