[Dijkstra] CIP-159-10: Apply batch-wide direct deposits in LEDGER rule (#1122)

[williamdemeo]

Description

This PR closes Issue #1122.

NOTE FOR REVIEWER. This PR depends on #1160 (UTxO rules; Issue #1117) which added accountBalances threading. The heavy lifting was already done in that PR; this PR merely adds the direct deposit application step to the LEDGER rule, so the target branch is that of PR #1160 (1117-cip-159-05-update-utxo-for-dir-deps-bal-intervals).

---

Changes

src/Ledger/Dijkstra/Specification/Ledger.lagda.md:

• Updated LEDGER-V output. After all sub-rule transitions, batch-wide direct deposits are applied to the final CertState:

  certStateFinal = record certState₂
    { dState = applyDirectDeposits (allDirectDeposits tx) (DStateOf certState₂) }

  The output LedgerState uses certStateFinal instead of certState₂, and rmOrphanDRepVotes receives certStateFinal so it sees the post-deposit state.

• LEDGER-I unchanged since invalid batches (IsValidFlagOf tx ≡ false) do not apply direct deposits, consistent with existing collateral collection semantics.

• New documentation. Explains the application ordering and the phantom asset prevention rationale.

src/Ledger/Dijkstra/Specification/Ledger/Properties/Computational.lagda.md:

• Updated computeProof (valid branch). Computes certStateFinal and uses it in the output LedgerState. The invalid branch is unchanged.

• completeness (valid branch) Requires no changes — both computeProof and the LEDGER-V conclusion compute the same certStateFinal term, so refl holds.

---

Design Notes

• Batch-level, not per-sub-transaction. Direct deposits are applied once after all transitions, not interleaved with sub-transaction processing. CIP-159 explicitly forbids per-sub-transaction application to prevent phantom asset attacks (where a deposit from one subtransaction inflates the balance available for withdrawal by another subtransaction).

• Applied after CERTS. Withdrawals in CERTS are checked against pre-batch balances (via accountBalances in UTxOEnv). Applying deposits after ensures withdrawals can't access freshly deposited funds within the same batch.

• depositsChange uses certState₂, not certStateFinal. The deposit change computation reflects registration/deregistration deposit changes only — not direct deposit value transfers. This is correct because direct deposits are not gov proposal deposits.

• rmOrphanDRepVotes uses certStateFinal. Semantically correct (it should see the final DRep state), though in practice applyDirectDeposits only modifies rewards, not voteDelegs or dreps, so the result is the same either way.

• allDirectDeposits and applyDirectDeposits are pre-existing. allDirectDeposits (in Transaction.lagda.md) aggregates direct deposits across the batch using ∪⁺. applyDirectDeposits (in Certs.lagda.md) applies them to a DState via ∪⁺.

---

Acceptance criteria checklist

• accountBalances field in UTxOEnv/SubUTxOEnv/SubLedgerEnv (done in [Dijkstra] CIP-159-05: Update UTxO rules for direct deposits and balance intervals #1117)
• LEDGER-V populates accountBalances from certState₀ (done in [Dijkstra] CIP-159-05: Update UTxO rules for direct deposits and balance intervals #1117)
• Batch-wide direct deposits applied in LEDGER-V output
• LEDGER-I does NOT apply direct deposits
• Application ordering correct (after CERTS, before output)
• computeProof updated for new output
• Module compiles with --safe

---

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

[Copilot]

Pull request overview

Note

Copilot was unable to run its full agentic suite in this review.

Applies CIP-159 batch-wide direct deposits at the end of a valid LEDGER transition by updating the final CertState (and ensuring the computational proof produces the same final state).

Changes:

• Update LEDGER-V to apply applyDirectDeposits (allDirectDeposits tx) to the final CertState and use that state for rmOrphanDRepVotes and the output LedgerState.
• Update computeProof (valid branch) to construct/use the same post-deposit CertState.
• Add documentation and a CHANGELOG entry describing ordering rationale and phantom-asset prevention.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 2 comments.

File	Description
src/Ledger/Dijkstra/Specification/Ledger.lagda.md	Applies batch-wide direct deposits in LEDGER-V output and documents the ordering/rationale.
src/Ledger/Dijkstra/Specification/Ledger/Properties/Computational.lagda.md	Aligns computeProof output with the updated LEDGER-V post-deposit CertState.
CHANGELOG.md	Notes the behavioral/spec change for CIP-159 direct deposits in LEDGER-V.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.