Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
williamdemeo wants to merge 2 commits into
base: 1117-cip-159-05-update-utxo-for-dir-deps-bal-intervals
Choose a base branch
from
Open

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0c5d520
[Dijkstra] CIP-159-05: Update UTxO rules for direct deposits and bala…
williamdemeo Apr 11, 2026
95e47c8
[Dijkstra] CIP-159-08: Phantom asset attack prevention (#1120)
williamdemeo Apr 12, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 14 additions & 8 deletions src/Ledger/Dijkstra/Specification/Ledger.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,7 @@ record SubLedgerEnv : Type where
isTopLevelValid : Bool
allScripts : ℙ Script
allData : DataHash ⇀ Datum
accountBalances : Rewards

record LedgerEnv : Type where
field
Expand Down Expand Up @@ -79,6 +80,10 @@ instance

HasTreasury-SubLedgerEnv : HasTreasury SubLedgerEnv
HasTreasury-SubLedgerEnv .TreasuryOf = SubLedgerEnv.treasury

HasAccountBalances-SubLedgerEnv : HasAccountBalances SubLedgerEnv
HasAccountBalances-SubLedgerEnv .AccountBalancesOf = SubLedgerEnv.accountBalances

```
-->
```agda
Expand Down Expand Up @@ -215,6 +220,7 @@ private variable
isTopLevelValid : Bool
allScripts : ℙ Script
allData : DataHash ⇀ Datum
accountBalances : Rewards
```
-->

Expand Down Expand Up @@ -285,17 +291,17 @@ data _⊢_⇀⦇_,SUBLEDGER⦈_ : SubLedgerEnv → LedgerState → SubLevelTx

SUBLEDGER-V :
∙ isTopLevelValid ≡ true
∙ ⟦ slot , pp , treasury , utxo₀ , isTopLevelValid , allScripts , allData ⟧ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₁
∙ ⟦ slot , pp , treasury , utxo₀ , isTopLevelValid , allScripts , allData , accountBalances ⟧ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₁
∙ ⟦ epoch slot , pp , ListOfGovVotesOf stx , WithdrawalsOf stx , allColdCreds govState₀ enactState ⟧ ⊢ certState₀ ⇀⦇ DCertsOf stx ,CERTS⦈ certState₁
∙ ⟦ TxIdOf stx , epoch slot , pp , ppolicy , enactState , certState₁ , dom (RewardsOf certState₁) ⟧ ⊢ govState₀ ⇀⦇ GovProposals+Votes stx ,GOVS⦈ govState₁
────────────────────────────────
⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , isTopLevelValid , allScripts , allData ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧
⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , isTopLevelValid , allScripts , allData , accountBalances ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧

SUBLEDGER-I :
∙ isTopLevelValid ≡ false
∙ ⟦ slot , pp , treasury , utxo₀ , isTopLevelValid , allScripts , allData ⟧ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₀
∙ ⟦ slot , pp , treasury , utxo₀ , isTopLevelValid , allScripts , allData , accountBalances ⟧ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₀
────────────────────────────────
⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , isTopLevelValid , allScripts , allData ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧
⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , isTopLevelValid , allScripts , allData , accountBalances ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧

_⊢_⇀⦇_,SUBLEDGERS⦈_ : SubLedgerEnv → LedgerState → List SubLevelTx → LedgerState → Type
_⊢_⇀⦇_,SUBLEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,SUBLEDGER⦈_}
Expand All @@ -317,10 +323,10 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LedgerState → TopLevelTx → Ledg
depositsChange = calculateDepositsChange certState₀ certState₁ certState₂
in
∙ IsValidFlagOf tx ≡ true
∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , IsValidFlagOf tx , allScripts , allData ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧
∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , IsValidFlagOf tx , allScripts , allData , RewardsOf certState₀ ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧
∙ ⟦ epoch slot , pp , ListOfGovVotesOf tx , WithdrawalsOf tx , allColdCreds govState₁ enactState ⟧ ⊢ certState₁ ⇀⦇ DCertsOf tx ,CERTS⦈ certState₂
∙ ⟦ TxIdOf tx , epoch slot , pp , ppolicy , enactState , certState₂ , dom (RewardsOf certState₂) ⟧ ⊢ govState₁ ⇀⦇ GovProposals+Votes tx ,GOVS⦈ govState₂
∙ ⟦ slot , pp , treasury , utxo₀ , depositsChange , allScripts , allData ⟧ ⊢ utxoState₁ ⇀⦇ tx ,UTXOW⦈ utxoState₂
∙ ⟦ slot , pp , treasury , utxo₀ , depositsChange , allScripts , allData , RewardsOf certState₀ ⟧ ⊢ utxoState₁ ⇀⦇ tx ,UTXOW⦈ utxoState₂
────────────────────────────────
⟦ slot , ppolicy , pp , enactState , treasury ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ tx ,LEDGER⦈ ⟦ utxoState₂ , rmOrphanDRepVotes certState₂ govState₂ , certState₂ ⟧

Expand All @@ -336,8 +342,8 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LedgerState → TopLevelTx → Ledg
allData = setToMap (mapˢ < hash , id > (getAllData tx))
in
∙ IsValidFlagOf tx ≡ false
∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , IsValidFlagOf tx , allScripts , allData ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧
∙ ⟦ slot , pp , treasury , utxo₀ , ⟦ 0ℤ , 0ℤ ⟧ , allScripts , allData ⟧ ⊢ utxoState₀ ⇀⦇ tx ,UTXOW⦈ utxoState₁
∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , IsValidFlagOf tx , allScripts , allData , RewardsOf certState₀ ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧
∙ ⟦ slot , pp , treasury , utxo₀ , ⟦ 0ℤ , 0ℤ ⟧ , allScripts , allData , RewardsOf certState₀ ⟧ ⊢ utxoState₀ ⇀⦇ tx ,UTXOW⦈ utxoState₁
────────────────────────────────
⟦ slot , ppolicy , pp , enactState , treasury ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ tx ,LEDGER⦈ ⟦ utxoState₁ , govState₀ , certState₀ ⟧

Expand Down
14 changes: 9 additions & 5 deletions src/Ledger/Dijkstra/Specification/Ledger/Properties/Computational.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -92,7 +92,7 @@ instance

-- Helper env constructors (avoid `let ... in with ...` parse issues)
subUtxoΓ : SubLedgerEnv → SubUTxOEnv
subUtxoΓ Γ = ⟦ slot , pparams , treasury , utxo₀ , isTopLevelValid , allScripts , allData ⟧
subUtxoΓ Γ = ⟦ slot , pparams , treasury , utxo₀ , isTopLevelValid , allScripts , allData , accountBalances ⟧
where open SubLedgerEnv Γ

certΓ : SubLedgerEnv → LedgerState → SubLevelTx → CertEnv
Expand All @@ -117,7 +117,7 @@ instance
let open SubLedgerEnv Γ
open LedgerState s
subUtxoΓ : SubUTxOEnv
subUtxoΓ = ⟦ slot , pparams , treasury , utxo₀ , isTopLevelValid , allScripts , allData ⟧
subUtxoΓ = ⟦ slot , pparams , treasury , utxo₀ , isTopLevelValid , allScripts , allData , accountBalances ⟧
certΓ : CertEnv
certΓ = ⟦ epoch slot , pparams , ListOfGovVotesOf stx , WithdrawalsOf stx
, allColdCreds govSt enactState ⟧
Expand All @@ -140,7 +140,7 @@ instance
isI : isTopLevelValid ≡ false
isI = ¬-not ¬isV
subUtxoΓ : SubUTxOEnv
subUtxoΓ = ⟦ slot , pparams , treasury , utxo₀ , isTopLevelValid , allScripts , allData ⟧
subUtxoΓ = ⟦ slot , pparams , treasury , utxo₀ , isTopLevelValid , allScripts , allData , accountBalances ⟧
in case computeSubutxow subUtxoΓ utxoSt stx of λ where
(failure e) → failure e
(success (utxoSt' , utxoStep)) →
Expand Down Expand Up @@ -229,6 +229,7 @@ instance
, IsValidFlagOf tx
, allScriptsOf tx s
, allDataOf tx s
, RewardsOf (CertStateOf s)
⟧

certΓOf : LedgerEnv → TopLevelTx → GovState → CertEnv
Expand Down Expand Up @@ -261,6 +262,7 @@ instance
, depositsChange
, allScriptsOf tx s
, allDataOf tx s
, RewardsOf (CertStateOf s)
⟧

utxoΓ-invalid : LedgerEnv → LedgerState → TopLevelTx → UTxOEnv
Expand All @@ -272,6 +274,7 @@ instance
, ⟦ 0ℤ , 0ℤ ⟧
, allScriptsOf tx s
, allDataOf tx s
, RewardsOf (CertStateOf s)
⟧
```
-->
Expand All @@ -294,7 +297,8 @@ instance
allData = setToMap (mapˢ < hash , id > (getAllData txTop))
subΓ : SubLedgerEnv
subΓ = ⟦ slot , ppolicy , pparams , enactState , treasury
, utxo₀ , IsValidFlagOf txTop , allScripts , allData ⟧
, utxo₀ , IsValidFlagOf txTop , allScripts , allData
, RewardsOf certState ⟧
in
case IsValidFlagOf txTop ≟ true of λ where
(yes isV) →
Expand All @@ -321,7 +325,7 @@ instance
depositsChange : DepositsChange
depositsChange = calculateDepositsChange certState₀ certState₁ certSt₂
utxoΓ : UTxOEnv
utxoΓ = ⟦ slot , pparams , treasury , utxo₀ , depositsChange , allScripts , allData ⟧
utxoΓ = ⟦ slot , pparams , treasury , utxo₀ , depositsChange , allScripts , allData , RewardsOf certState ⟧
in
-- UTXOW must run from the post-SUBLEDGERS UTxOState (utxoSt₁)
computeUtxow utxoΓ utxoSt₁ txTop >>= λ where
Expand Down
8 changes: 8 additions & 0 deletions src/Ledger/Dijkstra/Specification/Transaction.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -709,6 +709,14 @@ allowed to inspect utxo for its inputs.
foldl (λ acc txSub → acc ∪⁺ DirectDepositsOf txSub)
(DirectDepositsOf txTop)
(SubTransactionsOf txTop)

-- Batch-wide withdrawal aggregation: sums withdrawal amounts for the same reward
-- address across the top-level transaction and all sub-transactions.
allWithdrawals : TopLevelTx → Withdrawals
allWithdrawals txTop =
foldl (λ acc txSub → acc ∪⁺ WithdrawalsOf txSub)
(WithdrawalsOf txTop)
(SubTransactionsOf txTop)
```


Expand Down
72 changes: 66 additions & 6 deletions src/Ledger/Dijkstra/Specification/Utxo.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -83,6 +83,7 @@ record UTxOEnv : Type where
depositsChange : DepositsChange
allScripts : ℙ Script
allData : DataHash ⇀ Datum
accountBalances : Rewards

record SubUTxOEnv : Type where
field
Expand All @@ -93,6 +94,7 @@ record SubUTxOEnv : Type where
isTopLevelValid : Bool
allScripts : ℙ Script
allData : DataHash ⇀ Datum
accountBalances : Rewards
```

The `UTxOEnv`{.AgdaRecord} carries
Expand Down Expand Up @@ -150,6 +152,10 @@ record HasDataPool {a} (A : Type a) : Type a where
field DataPoolOf : A → DataHash ⇀ Datum
open HasDataPool ⦃...⦄ public

record HasAccountBalances {a} (A : Type a) : Type a where
field AccountBalancesOf : A → Rewards
open HasAccountBalances ⦃...⦄ public

record HasSlot {a} (A : Type a) : Type a where
field SlotOf : A → Slot
open HasSlot ⦃...⦄ public
Expand All @@ -176,6 +182,9 @@ instance
HasDataPool-UTxOEnv : HasDataPool UTxOEnv
HasDataPool-UTxOEnv .DataPoolOf = UTxOEnv.allData

HasAccountBalances-UTxOEnv : HasAccountBalances UTxOEnv
HasAccountBalances-UTxOEnv .AccountBalancesOf = UTxOEnv.accountBalances

HasSlot-SubUTxOEnv : HasSlot SubUTxOEnv
HasSlot-SubUTxOEnv .SlotOf = SubUTxOEnv.slot

Expand All @@ -197,6 +206,9 @@ instance
HasDataPool-SubUTxOEnv : HasDataPool SubUTxOEnv
HasDataPool-SubUTxOEnv .DataPoolOf = SubUTxOEnv.allData

HasAccountBalances-SubUTxOEnv : HasAccountBalances SubUTxOEnv
HasAccountBalances-SubUTxOEnv .AccountBalancesOf = SubUTxOEnv.accountBalances

HasUTxO-UTxOState : HasUTxO UTxOState
HasUTxO-UTxOState .UTxOOf = UTxOState.utxo

Expand Down Expand Up @@ -296,9 +308,7 @@ collateralCheck pp txTop utxo =
× isAdaOnly (balance (utxo ∣ CollateralInputsOf txTop))
× coin (balance (utxo ∣ CollateralInputsOf txTop)) * 100 ≥ (TxFeesOf txTop) * pp .collateralPercentage
× (CollateralInputsOf txTop) ≢ ∅
```

```agda
module _ (depositsChange : DepositsChange) where

open DepositsChange depositsChange
Expand Down Expand Up @@ -328,9 +338,10 @@ module _ (depositsChange : DepositsChange) where
consumedBatch txTop utxo = consumed txTop utxo
+ ∑ˡ[ stx ← SubTransactionsOf txTop ] (consumedTx stx utxo)
+ inject depositRefundsSub

producedTx : Tx ℓ → Value
producedTx tx = balance (outs tx) + inject (DonationsOf tx)
producedTx tx = balance (outs tx)
+ inject (DonationsOf tx)
+ inject (getCoin (DirectDepositsOf tx))

produced : TopLevelTx → Value
produced txTop = producedTx txTop
Expand All @@ -343,6 +354,42 @@ module _ (depositsChange : DepositsChange) where
+ inject newDepositsSub
```

## CIP-159 Notes

### Preservation of Value

CIP-159 introduces two new fields to transactions: `directDeposits` and
`balanceIntervals`. Direct deposits represent value that flows from the transaction
into account addresses.
Comment on lines +362 to +363
Copy link
Copy Markdown
Collaborator

@carlostome carlostome Apr 20, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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


In the preservation-of-value equation, direct deposits appear on the
*produced* side: value leaves the UTxO and enters account balances. The
Comment on lines +363 to +366
Copy link

Copilot AI Apr 14, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copilot uses AI. Check for mistakes.
`getCoin (DirectDepositsOf tx)` term, appearing in the definition of
`producedTx`{.AgdaFunction}, sums the ADA of all direct deposits in
the transaction.

### Phantom Asset Prevention

```agda
NoPhantomWithdrawals : Rewards → TopLevelTx → Type
NoPhantomWithdrawals preBalances txTop =
∀[ (addr , amt) ∈ allWithdrawals txTop ˢ ]
amt ≤ maybe id 0 (lookupᵐ? preBalances (RewardAddress.stake addr))
Comment on lines +374 to +377
Copy link

Copilot AI Apr 14, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 uses AI. Check for mistakes.
```

**The Problem**. CIP-159 identifies a "phantom asset" attack when nested
transactions combine direct deposits and withdrawals to the same account within a
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.
Comment on lines +382 to +384
Copy link
Copy Markdown
Collaborator

@carlostome carlostome Apr 20, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Copy Markdown
Member Author

@williamdemeo williamdemeo Apr 22, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


**The Solution**. Withdrawals across the entire batch are bounded by the
**pre-batch** account balances. The `NoPhantomWithdrawals`{.AgdaFunction} predicate
checks that the total withdrawal for each reward address (aggregated via
`allWithdrawals`{.AgdaFunction}) does not exceed the pre-batch balance of the
corresponding credential. This mirrors the spend-side safety principle where
spending inputs must come from the pre-batch UTxO snapshot (`utxo₀`{.AgdaField}).


## The <span class="AgdaDatatype">UTXOS</span> Transition System

Expand Down Expand Up @@ -433,6 +480,12 @@ The [CIP][1] states:
words, spending inputs across all top- and sub-level transactions
are disjoint.

4. Direct deposit targets must be registered accounts (their credentials
must appear in `dom accountBalances`).

5. Each balance interval assertion must hold against the pre-batch account
balances; this is a Phase-1 validity condition.

```agda
data _⊢_⇀⦇_,SUBUTXO⦈_ : SubUTxOEnv → UTxOState → SubLevelTx → UTxOState → Type where

Expand All @@ -455,6 +508,9 @@ data _⊢_⇀⦇_,SUBUTXO⦈_ : SubUTxOEnv → UTxOState → SubLevelTx → UTxO
∙ ∀[ a ∈ dom (WithdrawalsOf txSub)] (NetworkIdOf a ≡ NetworkId)
∙ MaybeNetworkIdOf txSub ~ just NetworkId
∙ CurrentTreasuryOf txSub ~ just (TreasuryOf Γ)
∙ dom (DirectDepositsOf txSub) ⊆ dom (AccountBalancesOf Γ)
∙ ∀[ (c , interval) ∈ BalanceIntervalsOf txSub ˢ ]
InBalanceInterval (maybe id 0 (lookupᵐ? (AccountBalancesOf Γ) c)) interval
────────────────────────────────
let
s₁ = if IsTopLevelValidFlagOf Γ
Expand Down Expand Up @@ -514,6 +570,10 @@ data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv × Bool → UTxOState → TopLevelTx → UT
∙ ∀[ a ∈ dom (WithdrawalsOf txTop)] NetworkIdOf a ≡ NetworkId
∙ MaybeNetworkIdOf txTop ~ just NetworkId
∙ CurrentTreasuryOf txTop ~ just (TreasuryOf Γ)
∙ dom (DirectDepositsOf txTop) ⊆ dom (AccountBalancesOf Γ)
∙ NoPhantomWithdrawals (AccountBalancesOf Γ) txTop
∙ ∀[ (c , interval) ∈ BalanceIntervalsOf txTop ˢ ]
InBalanceInterval (maybe id 0 (lookupᵐ? (AccountBalancesOf Γ) c)) interval
∙ Γ ⊢ _ ⇀⦇ txTop ,UTXOS⦈ _
────────────────────────────────
let
Expand All @@ -526,8 +586,8 @@ data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv × Bool → UTxOState → TopLevelTx → UT
<!--
```agda
unquoteDecl UTXO-premises = genPremises UTXO-premises (quote UTXO)
pattern UTXO-⋯ p₀ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉ p₁₀ p₁₁ p₁₂ p₁₃ p₁₄ p₁₅ p₁₆ p₁₇ p₁₈ h
= UTXO (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈ , h)
pattern UTXO-⋯ p₀ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉ p₁₀ p₁₁ p₁₂ p₁₃ p₁₄ p₁₅ p₁₆ p₁₇ p₁₈ p₁₉ p₂₀ p₂₁ h
= UTXO (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈ , p₁₉ , p₂₀ , p₂₁ , h)
```
-->

Expand Down
Loading
Loading