[Dijkstra] CIP-159 MASTER PLAN: Formalize Account Address Enhancement

## Overview

This plan describes how to incorporate [CIP-159][] (Account Address Enhancement) into the Dijkstra-era Agda formal ledger specification. CIP-159 enables direct deposits into account (reward) addresses, partial withdrawals, and account balance intervals.

CIP-159 has two phases. **We only formalize the first (ADA-only) phase in Dijkstra**.

1. **ADA-only phase** (Dijkstra). Direct ADA deposits, partial withdrawals, account balance intervals.
2. **Multi-Asset phase** (future era). Native asset deposits/withdrawals, whitelist certificates, new protocol parameter `accountWhitelistCostPerByte`.

**For Dijkstra we only carry out the ADA-only phase** (Phase 1).

## Key Interactions with CIP-118 (Nested Transactions)

CIP-159 relies heavily on CIP-118. Older Plutus scripts (v1–v3) cannot see the new `direct_deposits` field, so the CIP isolates that field inside a sub-transaction while older scripts run in the top-level transaction. Similarly, partial withdrawals are only permitted inside sub-transactions when Plutus v1–v3 scripts are present.

Additionally, when sub-transactions both deposit into and withdraw from the same account, the CIP introduces a **phantom asset attack prevention** rule: withdrawals can only draw from the account balance as it existed *before* the batch began (i.e., deposits made by earlier sub-txs in the same batch are not available for later sub-tx withdrawals).

## Sub-Issues

| # | Issue | Summary | Depends on |
|---|-------|---------|------------|
| 01 | #1113 | Core types (`DirectDeposits`, `BalanceInterval`, `AccountBalanceIntervals`) | — |
| 02 | #1114 | Extend `TxBody` with `txDirectDeposits` and `txBalanceIntervals` fields | #1113 |
| 03 | #1115 | Extend `DState` to support account balances and direct deposits | #1113 |
| 04 | #1116 | Update certificate rules for partial withdrawals | #1113, #1115 |
| 05 | #1117 | Update UTxO rules for direct deposits and balance intervals | #1113, #1114, #1115 |
| 06 | #1118 | Extend `TxInfo` and script validation for CIP-159 fields | #1113, #1114 |
| 07 | #1119 | Version gating — restrict CIP-159 fields based on script language version | #1114 |
| 08 | #1120 | Phantom asset attack prevention for batched deposits/withdrawals | #1114, #1117, #1119 |
| 10 | #1122 | Update LEDGER rule to integrate direct deposits and thread account balances | #1114, #1115, #1117 |
| 11 | #1123 | Prove preservation of value and invariant properties for CIP-159 | #1116, #1117, #1120, #1122 |

## Dependency Graph

An arrow from A to B means B depends on A. For clarity, only the *primary* dependency edges are shown. The full dependency set for each issue is recorded in the table above.

```mermaid
graph TD
I1113["#1113 Core types"]
I1114["#1114 TxBody"]
I1115["#1115 DState"]
I1116["#1116 Certs"]
I1117["#1117 UTxO rules"]
I1118["#1118 TxInfo"]
I1119["#1119 Version gating"]
I1120["#1120 Phantom asset"]
I1122["#1122 LEDGER rule"]
I1123["#1123 Properties"]

I1113 --> I1114
I1113 --> I1115

I1114 --> I1118
I1114 --> I1119
I1114 --> I1117
I1115 --> I1116
I1115 --> I1117

I1117 --> I1120
I1119 --> I1120
I1117 --> I1122

I1116 --> I1123
I1120 --> I1123
I1122 --> I1123
```

## Dijkstra Era (ADA-only) Issues

- #1113 (partial: `Coin`-only `DirectDeposits`, `BalanceInterval` for `Coin`)
- #1114 (new `TxBody` fields)
- #1115 (extend `DState` rewards to support account balances)
- #1116 (partial: partial withdrawals only)
- #1117 (UTxO balancing w/ direct deposits, per-transaction bal interval phase-1 check in `UTXO`/`SUBUTXO`)
- #1118 (`TxInfo` extensions)
- #1119 (version gating)
- #1120 (phantom asset prevention)
- #1122 (LEDGER rule integration)
- #1123 (properties)

## Suggested Implementation Order

The dependency structure suggests the following implementation order for the Dijkstra era changes.

1. **#1113** — Core types (no dependencies; everything else builds on this).
2. **#1114, #1115** — `TxBody` extensions and `DState` changes (depend only on #1113; can be done in parallel).
3. **#1116, #1118, #1119** — Certificate rules, `TxInfo` extensions, and version gating (depend on the above; can be done in parallel).
4. **#1117** — UTxO rules (depends on #1113, #1114, #1115).
5. **#1120, #1122** — Phantom asset prevention and LEDGER rule (depend on #1117).
6. **#1123** — Properties (depends on nearly everything above).

[CIP-159]: https://github.com/cardano-foundation/CIPs/tree/master/CIP-0159