[Dijkstra] CIP-159-05: Update UTxO for direct deposits and balance intervals (#1117)

[williamdemeo]

Description

This PR closes Issue #1117.

This PR updates the Dijkstra UTxO transition system for CIP-159 direct deposits and balance interval validation, as specified by CIP-159.

---

Changes

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

• Extended UTxOEnv and SubUTxOEnv. New accountBalances : Rewards field carrying the pre-batch account balances. Accompanied by a HasAccountBalances type class and instances for both environment types.

• Updated producedTx. Adds inject (getCoin (DirectDepositsOf tx)) to the produced side of the preservation-of-value equation. Direct deposits are value flowing from the transaction into account addresses.

• New UTXO premises.

  1. dom (DirectDepositsOf txTop) ⊆ dom (AccountBalancesOf Γ) — direct deposit targets must be registered accounts.
  2. ∀[ (c , interval) ∈ BalanceIntervalsOf txTop ˢ ] InBalanceInterval (maybe 0 id (lookupᵐ? (AccountBalancesOf Γ) c)) interval — Phase-1 balance interval validation against pre-batch balances.

• New SUBUTXO premises. Same two premises as UTXO, applied per-sub-transaction.

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

• Updated Computational-UTXO. Premise tuple grows from 19+h to 21+h. Both computeProof branches and both completeness branches updated.

• Computational-SUBUTXO. Uses the full tuple p without destructuring, so it adapts automatically via genPremises.

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

• Extended SubLedgerEnv. New accountBalances : Rewards field, with HasAccountBalances instance.

• Populated accountBalances at all construction sites. SUBLEDGER-V, SUBLEDGER-I, LEDGER-V, and LEDGER-I all pass RewardsOf certState₀ as the pre-batch account balances.

---

Design Notes

• Pre-batch account balances. Both UTxOEnv.accountBalances and SubUTxOEnv.accountBalances carry the same pre-batch snapshot (RewardsOf certState₀); this is consistent with CIP-159's design for local determinism: balance interval assertions are checked against the state before any sub-transaction in the batch modifies it, just as spending inputs are resolved against utxo₀.

• maybe id 0 (lookupᵐ? ...) for balance interval lookup. For unregistered credentials, the lookup returns nothing and maybe gives 0. An unregistered credential with effective balance 0 may legitimately satisfy ⟦0, ub ⦆ intervals; the separate registration premise (dom DirectDepositsOf ⊆ dom AccountBalancesOf) ensures deposit targets are known, but balance intervals don't require registration.

• Per-transaction, not batch-wide. Balance interval assertions are checked per-(sub)transaction, analogous to slot validity intervals; no batch-level aggregation of balance intervals is performed.

• Direct deposit registration per-transaction. Each (sub)transaction independently verifies that its direct deposit targets are registered, rather than checking batch-wide via allDirectDeposits.

• Ledger plumbing. The accountBalances field is populated immediately in this PR rather than deferred to [Dijkstra] CIP-159-10: Update LEDGER rule to integrate direct deposits and thread account balances #1122; keeps the code typecheckable and avoids using placeholders.

• UTXOS unchanged. The Dijkstra UTXOS rule is a trivial ⊤ → ⊤ transition checking only phase-2 script evaluation; no CIP-159 changes needed.

---

Acceptance criteria

• producedTx includes direct deposit amounts
• Balance interval validation premise added to UTXO rule
• Balance interval validation premise added to SUBUTXO rule
• InBalanceInterval predicate used correctly
• Registration precondition for direct deposit targets added
• UTxOEnv and SubUTxOEnv extended with accountBalances
• HasAccountBalances type class and instances defined
• UTXOS confirmed: no changes needed
• accountBalances populated in Ledger construction sites
• 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

Updates the Dijkstra UTxO and Ledger specifications to incorporate CIP-159 direct deposits into preservation-of-value and to add phase-1 validation for account balance interval assertions, threading pre-batch account balances through the relevant environments.

Changes:

• Extend UTxOEnv, SubUTxOEnv, and SubLedgerEnv with accountBalances : Rewards plus a HasAccountBalances accessor.
• Update the preservation-of-value accounting by adding direct deposits to producedTx.
• Add new UTXO/SUBUTXO premises enforcing (1) direct deposit target registration and (2) phase-1 InBalanceInterval checks against pre-batch balances, and propagate the new env field through computational/constructor plumbing.

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated no comments.

File	Description
src/Ledger/Dijkstra/Specification/Utxo.lagda.md	Adds accountBalances to UTxO environments, includes direct deposits in producedTx, and adds new UTXO/SUBUTXO premises for CIP-159 registration + balance interval validation.
src/Ledger/Dijkstra/Specification/Utxo/Properties/Computational.lagda.md	Updates the computational proof plumbing to account for the expanded UTXO premise tuple.
src/Ledger/Dijkstra/Specification/Ledger.lagda.md	Extends SubLedgerEnv with accountBalances and wires pre-batch balances into SUBLEDGER/LEDGER premises where environments are constructed.
src/Ledger/Dijkstra/Specification/Ledger/Properties/Computational.lagda.md	Threads pre-batch balances through computational environment constructors for SUBLEDGER/LEDGER.

---

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

[carlostome]

Nice work, LGTM!

I left a minor comment about spliting a precondition to make imho it somewhat more readable.

[carlostome]

In hindsight, maybe it'd be clearer (given the other precondition above) to add a separate precondition:

    ∙ dom (BalanceIntervalsOf txSub) ⊆ dom (AccountBalancesOf Γ)