[Dijkstra] CIP-159-01: core types

[williamdemeo]

Description

Closes #1113

CIP-159-01: Core types DirectDeposits, BalanceInterval, AccountBalanceIntervals

Summary

This PR introduces the shared domain types required by CIP-159 (Account Address Enhancement) in a new module Ledger.Dijkstra.Specification.Account. These types are used across Transaction, Certs, Utxo, and Script.Validation, so they are factored into their own module to avoid circular dependencies.

This covers Phase 1 (ADA-only). Phase 2 (multi-asset) upgrade paths are documented in the module as comments.

What's included

Definition	Type	Purpose
DirectDeposits	Credential ⇀ Coin	ADA deposits into account addresses within a transaction
BalanceInterval	Maybe Coin × Maybe Coin	Half-open interval [lo, hi) for balance assertions
AccountBalanceIntervals	Credential ⇀ BalanceInterval	Per-account balance interval assertions in a transaction
validBalanceInterval	BalanceInterval → Type	Well-formedness predicate requiring at least one bound
inBalanceInterval	Coin → BalanceInterval → Type	Membership predicate with Dec instance

Design decisions

• Maybe × Maybe representation for BalanceInterval: Follows the existing Maybe Slot × Maybe Slot convention used by validity intervals. A separate validBalanceInterval predicate excludes the (nothing, nothing) case rather than encoding it structurally, giving downstream rules flexibility in how they assert well-formedness.

• Half-open interval semantics: Unlike inInterval for slots (which uses closed [l, r] bounds), inBalanceInterval implements [lo, hi) as specified by CIP-159 (inclusive_lower_bound, exclusive_upper_bound). The upper bound check is suc c ≤ hi (i.e., c < hi).

• No explicit DecEq declarations: BalanceInterval inherits DecEq from DecEq-× and DecEq-Maybe in the prelude. DirectDeposits and AccountBalanceIntervals are type aliases over ⇀.

• Module parameterization: Parameterized by GovStructure (like Certs), giving access to Credential, Coin, etc.

Acceptance criteria checklist

• DirectDeposits type alias defined and available for import
• BalanceInterval and AccountBalanceIntervals types defined
• inBalanceInterval predicate defined with decidability (Dec)
• DecEq instances available where needed (inherited from prelude)
• 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

[carlostome]

Maybe note that "reward addresses" is pre-Dijkstra nomenclature, and that now these are called account addresses.

[carlostome]

A better approach will be to forbid by construction invalid balance intervals

[williamdemeo]

Yes, I thought of that (and Claude also suggested that as an alternative), but I thought it best to get it working with a simpler type, plus a predicate, first and then later upgrade to a richer type. Wdyt?