[Dijkstra] CIP-159-08 phantom asset attack prevention (#1120) by williamdemeo · Pull Request #1162 · IntersectMBO/formal-ledger-specifications

williamdemeo · 2026-04-12T03:44:15Z

Description

This PR closes Issue #1120.

NOTE FOR REVIEWER. This PR depends on #1117 (UTxO rules) for the accountBalances field in UTxOEnv. It does not depend on #1119 at the code level (no imports from Utxow), though #1119 is a logical prerequisite (version gating ensures CIP-159 fields can't appear in legacy mode).

Changes

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

New function. allWithdrawals : TopLevelTx → Withdrawals — aggregates withdrawal amounts across the top-level transaction and all sub-transactions using ∪⁺, mirroring the existing allDirectDeposits helper.

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

New predicate. NoPhantomWithdrawals : Rewards → TopLevelTx → Type — for each (addr, amt) in the batch-wide aggregated withdrawals, checks that amt ≤ lookupᵐ? preBalances (stake addr).
New UTXO premise. NoPhantomWithdrawals (AccountBalancesOf Γ) txTop added as a conjunct in the UTXO rule.
New documentation. Explains the phantom asset attack, the mitigation (pre-batch withdrawal bounds), and the analogy with spend-side safety (utxo₀ pattern).

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

Updated Computational-UTXO. Premise tuple grows from 21+h to 22+h.

Design Notes

Batch-wide check in UTXO, not per-sub-tx in SUBUTXO. The phantom asset check inspects all sub-transactions at once via allWithdrawals. SUBUTXO only sees one sub-transaction at a time and cannot enforce the batch-wide invariant.
allWithdrawals uses ∪⁺ (additive union). If the same reward address appears in multiple sub-transactions, amounts are summed. This correctly captures the total withdrawal pressure on each account.
Pre-batch balances via AccountBalancesOf Γ. The check uses the frozen pre-batch snapshot, not the running balance after earlier sub-transactions. This mirrors the utxo₀ pattern for spend-side safety.

Acceptance criteria checklist

NoPhantomWithdrawals predicate defined
allWithdrawals batch aggregation helper defined
New premise added to UTXO rule
Pre-batch account balances correctly used via AccountBalancesOf Γ
Check covers both top-level and sub-transaction withdrawals
Computational-UTXO updated for new premise
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.

This PR adds a CIP-159 “phantom asset” mitigation to the Dijkstra UTXO rule by bounding batch-wide withdrawals using pre-batch account balances, and updates the computational properties to match the new premise.

Changes:

Add allWithdrawals to aggregate withdrawals across a top-level tx and its sub-transactions using additive union (∪⁺).
Introduce NoPhantomWithdrawals and add it as a new premise to the UTXO rule (using AccountBalancesOf Γ as the frozen pre-batch snapshot).
Update Computational-UTXO premise packaging/unpacking to account for the additional predicate.

Reviewed changes

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

File	Description
src/Ledger/Dijkstra/Specification/Transaction.lagda.md	Adds `allWithdrawals` helper to compute batch-wide withdrawal totals used by the new safety check.
src/Ledger/Dijkstra/Specification/Utxo.lagda.md	Defines and documents `NoPhantomWithdrawals`, and threads it into the `UTXO` rule as a new premise.
src/Ledger/Dijkstra/Specification/Utxo/Properties/Computational.lagda.md	Updates the computational proof plumbing to include the new UTXO premise.

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

Copilot · 2026-04-14T03:07:35Z

+NoPhantomWithdrawals : Rewards → TopLevelTx → Type
+NoPhantomWithdrawals preBalances txTop =
+  ∀[ (addr , amt) ∈ allWithdrawals txTop ˢ ]
+    amt ≤ maybe id 0 (lookupᵐ? preBalances (RewardAddress.stake addr))


The expression maybe id 0 (lookupᵐ? ...) encodes an important defaulting policy (missing key ⇒ 0) but is fairly opaque and likely to be repeated (it already appears elsewhere in UTXO for balance-interval checks). Consider introducing a small helper (e.g., lookupᵐ?-default0 / lookup0) to centralize the semantics and improve readability, and then use it here.

Suggested change

NoPhantomWithdrawals : Rewards → TopLevelTx → Type

NoPhantomWithdrawals preBalances txTop =

∀[ (addr , amt) ∈ allWithdrawals txTop ˢ ]

amt ≤ maybe id 0 (lookupᵐ? preBalances (RewardAddress.stake addr))

lookup0 : Rewards → StakeCredential → Coin

lookup0 balances cred = maybe id 0 (lookupᵐ? balances cred)

NoPhantomWithdrawals : Rewards → TopLevelTx → Type

NoPhantomWithdrawals preBalances txTop =

∀[ (addr , amt) ∈ allWithdrawals txTop ˢ ]

amt ≤ lookup0 preBalances (RewardAddress.stake addr)

Copilot · 2026-04-14T03:07:36Z

+into account addresses.
+
+In the preservation-of-value equation, direct deposits appear on the
+*produced* side: value leaves the UTxO and enters account balances.  The


The text uses “account addresses”, but the formalization below is phrased in terms of reward addresses / stake credentials (e.g., withdrawals keyed by reward addresses and looked up via RewardAddress.stake). To avoid ambiguity for readers, it’d help to align terminology here (e.g., explicitly say “reward accounts (stake credentials)” if that’s what is meant, or define what “account address” refers to in this spec).

Suggested change

into account addresses.

In the preservation-of-value equation, direct deposits appear on the

*produced* side: value leaves the UTxO and enters account balances. The

into reward accounts (stake credentials).

In the preservation-of-value equation, direct deposits appear on the

*produced* side: value leaves the UTxO and enters reward-account balances. The

carlostome · 2026-04-20T13:44:40Z

+`balanceIntervals`.  Direct deposits represent value that flows from the transaction
+into account addresses.


I don't understand what "value that flows from the transaction into account addresses" means

carlostome · 2026-04-20T13:58:39Z

+single batch.  If a sub-transaction deposits ADA into an account and a later
+sub-transaction withdraws it, Plutus scripts may be tricked into believing native
+assets were minted.


I don't see how this is a problem from the POV of Plutus scripts. Already in nested transactions V4 scripts cannot assume transactions to be balanced since a sub-transaction might look like it pulls ADA out of thin air. I don't understand why in that case is not an issue but with direct deposits and withdrawals it is.

Instead of explaining this here, let's address this in a more prominent place where we cover not spending outputs created within the batch. And add examples. Make an issue for this.

…nce intervals (#1117) CIP-159 changes the transaction balancing rules and introduces Phase-1 balance interval validation. This commit updates the UTxO transition system accordingly. `Utxo.lagda.md`: + Add accountBalances : Rewards field to UTxOEnv and SubUTxOEnv for pre-batch account balance lookups; + Add HasAccountBalances type class and instances; + Update producedTx to include direct deposit amounts on the produced side of the preservation-of-value equation; + Add direct deposit registration premise to UTXO and SUBUTXO (`dom DirectDepositsOf ⊆ dom AccountBalancesOf`); + Add balance interval validation premise to UTXO and SUBUTXO (∀ (c,interval) ∈ BalanceIntervalsOf, InBalanceInterval using pre-batch account balances). `Utxo/Properties/Computational.lagda.md`: + Update Computational-UTXO for new premise tuple arity (19+h → 21+h) `Ledger.lagda.md`: + Add accountBalances field to SubLedgerEnv; + Populate accountBalances in SUBLEDGER-V, SUBLEDGER-I, LEDGER-V, LEDGER-I using RewardsOf certState₀ (pre-batch balances).

Add batch-wide withdrawal bound check to prevent phantom asset attacks when nested transactions combine deposits and withdrawals. `Transaction.lagda.md`: + Define allWithdrawals batch aggregation helper (mirrors allDirectDeposits) `Utxo.lagda.md`: + Define NoPhantomWithdrawals predicate using allWithdrawals + Add NoPhantomWithdrawals premise to UTXO rule + Document phantom asset attack and spend-side safety analogy `Utxo/Properties/Computational.lagda.md`: + Update Computational-UTXO for new premise tuple arity (21+h → 22+h)

williamdemeo linked an issue Apr 12, 2026 that may be closed by this pull request

[Dijkstra] CIP-159-08: Phantom asset attack prevention for batched deposits/withdrawals #1120

Open

7 tasks

williamdemeo changed the base branch from master to 1117-cip-159-05-update-utxo-for-dir-deps-bal-intervals April 12, 2026 03:44

williamdemeo self-assigned this Apr 12, 2026

williamdemeo changed the title ~~1120 cip 159 08 phantom asset attack prevention~~ [Dijkstra] CIP 159 08 phantom asset attack prevention (#1120) Apr 12, 2026

williamdemeo changed the title ~~[Dijkstra] CIP 159 08 phantom asset attack prevention (#1120)~~ [Dijkstra] CIP-159-08 phantom asset attack prevention (#1120) Apr 12, 2026

williamdemeo marked this pull request as ready for review April 12, 2026 03:49

williamdemeo requested a review from Copilot April 14, 2026 03:00

Copilot AI reviewed Apr 14, 2026

View reviewed changes

Copilot started reviewing on behalf of williamdemeo April 14, 2026 03:07 View session

williamdemeo mentioned this pull request Apr 14, 2026

[Dijkstra] CIP 159 Master PR bundle #1168

Open

4 tasks

williamdemeo added the CIP 159 Account Address Enhancement label Apr 16, 2026

carlostome reviewed Apr 20, 2026

View reviewed changes

williamdemeo force-pushed the 1117-cip-159-05-update-utxo-for-dir-deps-bal-intervals branch from 37f2bf6 to 33b565b Compare April 21, 2026 19:17

williamdemeo force-pushed the 1120-cip-159-08-phantom-asset-attack-prevention branch from 182388c to 8796ae6 Compare April 21, 2026 19:21

williamdemeo force-pushed the 1117-cip-159-05-update-utxo-for-dir-deps-bal-intervals branch from 33b565b to 0c5d520 Compare April 22, 2026 14:57

williamdemeo force-pushed the 1120-cip-159-08-phantom-asset-attack-prevention branch from 8796ae6 to 95e47c8 Compare April 22, 2026 15:01

williamdemeo mentioned this pull request Apr 22, 2026

[Dijkstra] document prohibiting within-batch withdrawals #1172

Open

williamdemeo force-pushed the 1117-cip-159-05-update-utxo-for-dir-deps-bal-intervals branch from 0c5d520 to 389d947 Compare April 24, 2026 00:47

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Dijkstra] CIP-159-08 phantom asset attack prevention (#1120)#1162

[Dijkstra] CIP-159-08 phantom asset attack prevention (#1120)#1162
williamdemeo wants to merge 2 commits into1117-cip-159-05-update-utxo-for-dir-deps-bal-intervalsfrom
1120-cip-159-08-phantom-asset-attack-prevention

williamdemeo commented Apr 12, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Apr 14, 2026

Uh oh!

Copilot AI Apr 14, 2026

Uh oh!

carlostome Apr 20, 2026

Uh oh!

carlostome Apr 20, 2026

Uh oh!

williamdemeo Apr 22, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

		`balanceIntervals`. Direct deposits represent value that flows from the transaction
		into account addresses.

Conversation

williamdemeo commented Apr 12, 2026

Description

Changes

Design Notes

Acceptance criteria checklist

Checklist

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Apr 14, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 14, 2026

Choose a reason for hiding this comment

Uh oh!

carlostome Apr 20, 2026

Choose a reason for hiding this comment

Uh oh!

carlostome Apr 20, 2026

Choose a reason for hiding this comment

Uh oh!

williamdemeo Apr 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

williamdemeo Apr 22, 2026 •

edited

Loading