diff --git a/src/Ledger/Dijkstra/Specification/Entities.lagda.md b/src/Ledger/Dijkstra/Specification/Entities.lagda.md
index 65bdbdab3..3c51cf181 100644
--- a/src/Ledger/Dijkstra/Specification/Entities.lagda.md
+++ b/src/Ledger/Dijkstra/Specification/Entities.lagda.md
@@ -9,16 +9,14 @@ source_path: src/Ledger/Dijkstra/Specification/Entities.lagda.md
 ```agda
 {-# OPTIONS --safe #-}
 
-open import Ledger.Dijkstra.Specification.Gov.Base using (GovStructure)
+open import Ledger.Dijkstra.Specification.Transaction using (TransactionStructure)
 
 module Ledger.Dijkstra.Specification.Entities
-  (gs : GovStructure) (open GovStructure gs) where
+  (txs : TransactionStructure) (open TransactionStructure txs) where
 
 open import Ledger.Prelude renaming (filterˢ to filter)
 open import Ledger.Prelude.Numeric.UnitInterval
-open import Ledger.Dijkstra.Specification.Gov.Actions gs hiding (yes; no)
-open import Ledger.Dijkstra.Specification.Account gs
-open import Ledger.Dijkstra.Specification.Certs gs
+open import Ledger.Dijkstra.Specification.Certs govStructure
 open RewardAddress
 open PParams
 ```
@@ -29,19 +27,25 @@ open PParams
 ```agda
 record EntitiesEnv : Type where
   field
-    epoch           : Epoch
-    pp              : PParams
-    votes           : List GovVote
-    coldCredentials : ℙ Credential
-    withdrawals     : Withdrawals
-    directDeposits  : DirectDeposits
+    epoch                   : Epoch
+    pp                      : PParams
+    coldCredentials         : ℙ Credential
+    legacyMode              : Bool
+    rewards₀                : Rewards
 
+record SubEntitiesEnv : Type where
+  field
+    epoch                   : Epoch
+    pp                      : PParams
+    coldCredentials         : ℙ Credential
+    rewards₀                : Rewards
 ```
 
 <!--
 ```agda
-unquoteDecl HasCast-EntitiesEnv = derive-HasCast
-  [ (quote EntitiesEnv , HasCast-EntitiesEnv) ]
+unquoteDecl HasCast-EntitiesEnv HasCast-SubEntitiesEnv = derive-HasCast
+  ( (quote SubEntitiesEnv , HasCast-SubEntitiesEnv) ∷
+  [ (quote EntitiesEnv , HasCast-EntitiesEnv) ])
 
 instance
   EntitiesEnv-HasEpoch : HasEpoch EntitiesEnv
@@ -87,92 +91,119 @@ applyWithdrawals = applyToRewards _∸_
 
 # `ENTITIES`{.AgdaDatatype} Transition System
 
-In Dijkstra, the `ENTITIES`{.AgdaDatatype} rule replaces pre-Dijkstra
-`CERTS`{.AgdaDatatype} rule. This rule processes withdrawals,
-certificates and direct deposits.
+In Dijkstra, the new `ENTITIES`{.AgdaDatatype} rule subsumes the
+pre-Dijkstra `CERTS`{.AgdaDatatype} rule. This rule in addition to
+processing certificates via `CERTS`{.AgdaDatatype}, processes
+withdrawals, direct deposits, and account balance intervals.
+
+CIP-159 introduces two new fields to transactions: `directDeposits`
+and `balanceIntervals`. Direct deposits represent value that flows
+from the transaction into account addresses. Balance intervals enable
+transactions to assert predicates about account balances.
 
-## Withdrawal Processing
+## Withdrawals 
 
 The `ENTITIES`{.AgdaDatatype} rule applies withdrawals, via
 `applyWithdrawals`{.AgdaFunction} before certificate evaluation.  In
-the Dijkstra era, CIP-159 extends the withdrawal semantics from an
-"all-or-nothing" model (where the withdrawn amount must equal the full
-account balance) to a "partial withdrawal" model (where any amount up
-to the full balance may be withdrawn).
-
-Premise (1) ensures that each withdrawal targets a registered
-account and that the withdrawal amount does not exceed the account's
-current balance.
-
-The phantom-asset prohibition of CIP-159 — that withdrawals in one
-sub-transaction may not draw from deposits made by an earlier
-sub-transaction in the same batch — is enforced separately in the
-`Utxo`{.AgdaModule} (see [Phantom Asset
-Prevention](Ledger.Dijkstra.Specification.Utxo.md#subsubsec:phantom-asset-prevention)).
-
-## Direct Deposit Application (CIP-159)
-
-The `ENTITIES`{.AgdaDatatype} rule applies CIP-159 direct deposits to the
-`CertState`{.AgdaRecord} after all individual `CERT`{.AgdaDatatype} steps
-for the transaction have run, alongside its existing `voteDelegs`{.AgdaField}
-filtering. Specifically:
-
-+  `voteDelegs`{.AgdaField} is restricted to credentials that delegate to a
-   currently-registered `DRep`{.AgdaInductiveConstructor} (or to the abstain /
-   no-confidence pseudo-DReps).
-+  `rewards`{.AgdaField} is augmented by `directDeposits`{.AgdaField} via
-   `∪⁺`{.AgdaFunction} (union with addition) — equivalently,
-   `applyDirectDeposits directDeposits` is applied to the threaded
-   `DState`{.AgdaRecord}.
-
-Premise (2) ensures that `applyDirectDeposits`{.AgdaFunction} does not
-silently re-introduce a credential into `rewards`{.AgdaField} that was
-deregistered earlier in the same transaction's `CERT`{.AgdaDatatype}
-steps (and is therefore no longer present in `voteDelegs`{.AgdaField},
-`stakeDelegs`{.AgdaField}, or `deposits`{.AgdaField}), which would
-produce an inconsistent `DState`{.AgdaRecord}.
+the Dijkstra era, withdrawals can be partial, unless in legacy mode.
+
+## Direct Deposits
+
+The `ENTITIES`{.AgdaDatatype} rule applies direct deposits to the
+`CertState`{.AgdaRecord} after  `CERTS`{.AgdaDatatype}.
 
 <!--
 ```agda
 open GovVote using (voter)
 
 private variable
-  rewards₀ rewards₁ : Rewards
+  txTop : TopLevelTx
+  txSub : SubLevelTx
+  rewards rewards' : Rewards
   dReps : DReps
-  stakeDelegs stakeDelegs₀ stakeDelegs₁ : StakeDelegs
+  stakeDelegs stakeDelegs' : StakeDelegs
   ccHotKeys : CCHotKeys
-  voteDelegs₀ voteDelegs₁ : VoteDelegs
-  wdrls : Withdrawals
-  dd : DirectDeposits
-  depositsᵍ depositsᵈ₀ depositsᵈ₁ : Credential ⇀ Coin
+  voteDelegs voteDelegs' : VoteDelegs
+  rewards₀ : Rewards
+  depositsᵍ depositsᵈ depositsᵈ' : Credential ⇀ Coin
+  legacyMode : Bool
 
-  dCerts : List DCert
   e : Epoch
-  vs : List GovVote
   pp : PParams
   cc : ℙ Credential
 
-  gState₁ : GState
-  pState₀ pState₁ : PState
+  gState' : GState
+  pState pState' : PState
 ```
 -->
 
 ```agda
-data _⊢_⇀⦇_,ENTITIES⦈_ : EntitiesEnv → CertState → List DCert → CertState → Type where
+data _⊢_⇀⦇_,SUBENTITIES⦈_ : SubEntitiesEnv → CertState → SubLevelTx → CertState → Type where
+
+  SUBENTITIES :
+    let refresh         = mapPartial (isGovVoterDRep ∘ voter) (fromList (ListOfGovVotesOf txSub))
+        refreshedDReps  = mapValueRestricted (const (e + pp .drepActivity)) dReps refresh
+        activeVDelegs   = mapˢ vDelegCredential (dom (DRepsOf gState'))
+                               ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ [])
+
+        withdrawals               = WithdrawalsOf txSub
+        withdrawalsCredentials    = mapˢ stake (dom withdrawals)
+        accountBalanceIntervals   = BalanceIntervalsOf txSub
+        directDeposits            = DirectDepositsOf txSub
+        directDepositsCredentials = mapˢ stake (dom directDeposits)
+    in
+    ∙ ∀[ a ∈ dom withdrawals ] NetworkIdOf a ≡ NetworkId
+    ∙ withdrawalsCredentials ⊆ dom rewards₀
+    ∙ withdrawalsCredentials ⊆ dom rewards
+
+    ∙ dom accountBalanceIntervals ⊆ dom rewards
+    ∙ ∀[ (c , interval) ∈ accountBalanceIntervals ˢ ]
+        (InBalanceInterval (maybe id 0 (lookupᵐ? rewards c)) interval)
+
+    ∙ ⟦ e , pp , cc ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , applyWithdrawals withdrawals rewards , depositsᵈ ⟧ , pState , ⟦ refreshedDReps , ccHotKeys , depositsᵍ ⟧ ⟧ ⇀⦇ DCertsOf txSub  ,CERTS⦈ ⟦ ⟦ voteDelegs' , stakeDelegs' , rewards' , depositsᵈ' ⟧ , pState' , gState' ⟧
+
+    ∙ ∀[ a ∈ dom directDeposits ] NetworkIdOf a ≡ NetworkId
+    ∙ directDepositsCredentials ⊆ dom rewards'
+      ────────────────────────────────
+      ⟦ e , pp , cc , rewards₀ ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards , depositsᵈ ⟧ , pState , ⟦ dReps , ccHotKeys , depositsᵍ ⟧ ⟧ ⇀⦇ txSub ,SUBENTITIES⦈ ⟦ ⟦ voteDelegs' ∣^ activeVDelegs , stakeDelegs' , applyDirectDeposits directDeposits rewards' , depositsᵈ' ⟧ , pState' , gState' ⟧
+```
+
+```agda
+data _⊢_⇀⦇_,ENTITIES⦈_ : EntitiesEnv → CertState → TopLevelTx → CertState → Type where
 
   ENTITIES :
-    let refresh         = mapPartial (isGovVoterDRep ∘ voter) (fromList vs)
+    let refresh         = mapPartial (isGovVoterDRep ∘ voter) (fromList (ListOfGovVotesOf txTop))
         refreshedDReps  = mapValueRestricted (const (e + pp .drepActivity)) dReps refresh
-        wdrlCreds       = mapˢ stake (dom wdrls)
-        ddCreds         = mapˢ stake (dom dd)
-        activeVDelegs   = mapˢ vDelegCredential (dom (DRepsOf gState₁))
+        activeVDelegs   = mapˢ vDelegCredential (dom (DRepsOf gState'))
                                ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ [])
+
+        withdrawalsSubTxs          = foldl (λ acc txSub → acc ∪⁺ WithdrawalsOf txSub) ∅ (SubTransactionsOf txTop)
+        withdrawals                = WithdrawalsOf txTop
+        withdrawalsCredentials     = mapˢ stake (dom withdrawals)
+        accountBalanceIntervals    = BalanceIntervalsOf txTop
+        directDeposits             = DirectDepositsOf txTop
+        directDepositsCredentials  = mapˢ stake (dom directDeposits)
     in
-    ∙ filter isKeyHash wdrlCreds ⊆ dom voteDelegs₀
-    ∙ wdrlCreds ⊆ dom rewards₀
-    ∙ ∀[ (addr , amt) ∈ wdrls ˢ ] amt ≤ maybe id 0 (lookupᵐ? rewards₀ (stake addr)) -- (1)
-    ∙ ⟦ e , pp , cc ⟧ ⊢ ⟦ ⟦ voteDelegs₀ , stakeDelegs₀ , applyWithdrawals wdrls rewards₀ , depositsᵈ₀ ⟧ , pState₀ , ⟦ refreshedDReps , ccHotKeys , depositsᵍ ⟧ ⟧ ⇀⦇ dCerts  ,CERTS⦈ ⟦ ⟦ voteDelegs₁ , stakeDelegs₁ , rewards₁ , depositsᵈ₁ ⟧ , pState₁ , gState₁ ⟧
-    ∙ ddCreds ⊆ dom rewards₁ -- (2)
+
+    ∙ ∀[ a ∈ dom withdrawals ] NetworkIdOf a ≡ NetworkId
+    ∙ withdrawalsCredentials ⊆ dom rewards
+
+    ∙ (legacyMode ≡ true →
+        ∙ ∀[ (addr , amt) ∈ withdrawals ˢ ] amt ≡ maybe id 0 (lookupᵐ? rewards (stake addr))
+        ∙ ∀[ (addr , amt) ∈ withdrawalsSubTxs ˢ ] amt ≤ maybe id 0 (lookupᵐ? rewards₀ (stake addr)))
+
+    ∙ (legacyMode ≡ false →
+        ∙ withdrawalsCredentials ⊆ dom rewards₀
+        ∙ ∀[ (addr , amt) ∈ (withdrawalsSubTxs ∪⁺ withdrawals) ˢ ] amt ≤ maybe id 0 (lookupᵐ? rewards₀ (stake addr)))
+
+    ∙ dom accountBalanceIntervals ⊆ dom rewards
+    ∙ ∀[ (c , interval) ∈ accountBalanceIntervals ˢ ]
+        (InBalanceInterval (maybe id 0 (lookupᵐ? rewards c)) interval)
+
+    ∙ ⟦ e , pp , cc ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , applyWithdrawals withdrawals rewards , depositsᵈ ⟧ , pState , ⟦ refreshedDReps , ccHotKeys , depositsᵍ ⟧ ⟧ ⇀⦇ DCertsOf txTop  ,CERTS⦈ ⟦ ⟦ voteDelegs' , stakeDelegs' , rewards' , depositsᵈ' ⟧ , pState' , gState' ⟧
+
+    ∙ ∀[ a ∈ dom directDeposits ] NetworkIdOf a ≡ NetworkId
+    ∙ directDepositsCredentials ⊆ dom rewards'
       ────────────────────────────────
-      ⟦ e , pp , vs , cc , wdrls , dd ⟧ ⊢ ⟦ ⟦ voteDelegs₀ , stakeDelegs₀ , rewards₀ , depositsᵈ₀ ⟧ , pState₀ , ⟦ dReps , ccHotKeys , depositsᵍ ⟧ ⟧ ⇀⦇ dCerts ,ENTITIES⦈ ⟦ ⟦ voteDelegs₁ ∣^ activeVDelegs , stakeDelegs₁ , applyDirectDeposits dd rewards₁ , depositsᵈ₁ ⟧ , pState₁ , gState₁ ⟧
+      ⟦ e , pp , cc , legacyMode , rewards₀ ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards , depositsᵈ ⟧ , pState , ⟦ dReps , ccHotKeys , depositsᵍ ⟧ ⟧ ⇀⦇ txTop ,ENTITIES⦈ ⟦ ⟦ voteDelegs' ∣^ activeVDelegs , stakeDelegs' , applyDirectDeposits directDeposits rewards' , depositsᵈ' ⟧ , pState' , gState' ⟧
 ```
diff --git a/src/Ledger/Dijkstra/Specification/Entities/Properties/Computational.lagda.md b/src/Ledger/Dijkstra/Specification/Entities/Properties/Computational.lagda.md
index 18fd10cd7..db81d681b 100644
--- a/src/Ledger/Dijkstra/Specification/Entities/Properties/Computational.lagda.md
+++ b/src/Ledger/Dijkstra/Specification/Entities/Properties/Computational.lagda.md
@@ -6,15 +6,14 @@ source_path: src/Ledger/Dijkstra/Specification/Entitities/Properties/Computation
 ```agda
 {-# OPTIONS --safe #-}
 
-open import Ledger.Dijkstra.Specification.Gov.Base using (GovStructure)
+open import Ledger.Dijkstra.Specification.Transaction using (TransactionStructure)
 
 module Ledger.Dijkstra.Specification.Entities.Properties.Computational
-  (govStructure : GovStructure) where
+  (txs : TransactionStructure) (open TransactionStructure txs) where
 
 open import Ledger.Prelude
-open import Ledger.Dijkstra.Specification.Gov.Actions govStructure hiding (yes; no)
 open import Ledger.Dijkstra.Specification.Certs govStructure
-open import Ledger.Dijkstra.Specification.Entities govStructure
+open import Ledger.Dijkstra.Specification.Entities txs
 open import Ledger.Dijkstra.Specification.Gov govStructure
 
 open import Ledger.Dijkstra.Specification.Certs.Properties.Computational govStructure
@@ -23,7 +22,6 @@ open import stdlib-meta.Tactic.GenError using (genErrors)
 import Data.Maybe.Relation.Unary.Any as M
 import Data.Maybe.Relation.Unary.All as M
 
-open GovStructure govStructure
 open RewardAddress
 
 open GovVote
@@ -31,46 +29,143 @@ open GovVote
 module Computational-CERTS = Computational Computational-CERTS
 
 instance
+  Computational-SUBENTITIES : Computational _⊢_⇀⦇_,SUBENTITIES⦈_ String
+  Computational-SUBENTITIES = record {go}
+    where
+      module go (Γ : SubEntitiesEnv) (s₀ : CertState) (txSub : SubLevelTx)
+                (let module Γ = SubEntitiesEnv Γ
+                     refresh         = mapPartial (isGovVoterDRep ∘ voter) (fromList (ListOfGovVotesOf txSub))
+                     refreshedDReps  = mapValueRestricted (const (Γ.epoch  + Γ.pp .PParams.drepActivity)) (DRepsOf s₀) refresh
+
+                     withdrawals               = WithdrawalsOf txSub
+                     withdrawalsCredentials    = mapˢ stake (dom withdrawals)
+                     accountBalanceIntervals   = BalanceIntervalsOf txSub
+                     directDeposits            = DirectDepositsOf txSub
+                     directDepositsCredentials = mapˢ stake (dom directDeposits)
+
+                ) where
+
+        s₁ : CertState
+        s₁ = ⟦ ⟦ VoteDelegsOf s₀ , StakeDelegsOf s₀ , applyWithdrawals withdrawals (RewardsOf s₀) , DepositsOf (DStateOf s₀) ⟧
+               , PStateOf s₀
+               , ⟦ refreshedDReps
+                 , CCHotKeysOf s₀
+                 , DepositsOf (GStateOf s₀) ⟧ ⟧
+
+        computeProof : ComputationResult String (∃-syntax (_⊢_⇀⦇_,SUBENTITIES⦈_ Γ s₀ txSub))
+        computeProof with ¿
+            ∙ ∀[ a ∈ dom withdrawals ] NetworkIdOf a ≡ NetworkId
+            ∙ withdrawalsCredentials ⊆ dom Γ.rewards₀
+            ∙ withdrawalsCredentials ⊆ dom (RewardsOf s₀)
+
+            ∙ dom accountBalanceIntervals ⊆ dom (RewardsOf s₀)
+            ∙ ∀[ (c , interval) ∈ accountBalanceIntervals ˢ ]
+                (InBalanceInterval (maybe id 0 (lookupᵐ? (RewardsOf s₀) c)) interval)
+
+            ∙ ∀[ a ∈ dom directDeposits ] NetworkIdOf a ≡ NetworkId
+          ¿ | Computational-CERTS.computeProof ⟦ Γ.epoch , Γ.pp , Γ.coldCredentials ⟧ s₁ (DCertsOf txSub)
+        ... | no ¬p | _ = failure ""
+        ... | yes _ | failure e = failure e
+        ... | yes (p₁ , p₂ , p₃ , p₄ , p₅ , p₆) | success (s₂ , p)
+          with ¿ directDepositsCredentials ⊆ dom (RewardsOf s₂) ¿
+        ... | no ¬p = failure ""
+        ... | yes p₇ = success (-, (SUBENTITIES (p₁ , p₂ , p₃ , p₄ , p₅ , p , p₆ , p₇)))
+
+        completeness : ∀ (s' : CertState) → Γ ⊢ s₀ ⇀⦇ txSub ,SUBENTITIES⦈ s' → map proj₁ computeProof ≡ success s'
+        completeness s' (SUBENTITIES (p₁ , p₂ , p₃ , p₄ , p₅ , p , p₆ , p₇))
+          with ¿
+            ∙ ∀[ a ∈ dom withdrawals ] NetworkIdOf a ≡ NetworkId
+            ∙ withdrawalsCredentials ⊆ dom Γ.rewards₀
+            ∙ withdrawalsCredentials ⊆ dom (RewardsOf s₀)
+
+            ∙ dom accountBalanceIntervals ⊆ dom (RewardsOf s₀)
+            ∙ ∀[ (c , interval) ∈ accountBalanceIntervals ˢ ]
+                (InBalanceInterval (maybe id 0 (lookupᵐ? (RewardsOf s₀) c)) interval)
+
+            ∙ ∀[ a ∈ dom directDeposits ] NetworkIdOf a ≡ NetworkId
+          ¿ | Computational-CERTS.computeProof ⟦ Γ.epoch , Γ.pp , Γ.coldCredentials ⟧ s₁ (DCertsOf txSub) | Computational-CERTS.completeness _ _ _ _ p
+        ... | no ¬p | _ | p' = ⊥-elim (¬p (p₁ , p₂ , p₃ , p₄ , p₅ , p₆))
+        ... | yes _ | failure e | ()
+        ... | yes (p₁ , p₂ , p₃ , p₄ , p₅ , p₆) | success (s₂ , p) | refl
+          with ¿ directDepositsCredentials ⊆ dom (RewardsOf s₂) ¿
+        ... | no ¬p  = ⊥-elim (¬p p₇)
+        ... | yes _ = refl
+
   Computational-ENTITIES : Computational _⊢_⇀⦇_,ENTITIES⦈_ String
   Computational-ENTITIES = record {go}
     where
-      module go (Γ : EntitiesEnv) (s₀ : CertState) (dCerts : List DCert)
+      module go (Γ : EntitiesEnv) (s₀ : CertState) (txTop : TopLevelTx)
                 (let module Γ = EntitiesEnv Γ
-                     refresh  = mapPartial (isGovVoterDRep ∘ voter) (fromList Γ.votes)
+                     refresh         = mapPartial (isGovVoterDRep ∘ voter) (fromList (ListOfGovVotesOf txTop))
                      refreshedDReps  = mapValueRestricted (const (Γ.epoch  + Γ.pp .PParams.drepActivity)) (DRepsOf s₀) refresh
-                     wdrlCreds       = mapˢ stake (dom Γ.withdrawals)
-                     ddCreds         = mapˢ stake (dom Γ.directDeposits)
+
+                     withdrawalsSubTxs          = foldl (λ acc txSub → acc ∪⁺ WithdrawalsOf txSub) ∅ (SubTransactionsOf txTop)
+                     withdrawals               = WithdrawalsOf txTop
+                     withdrawalsCredentials    = mapˢ stake (dom withdrawals)
+                     accountBalanceIntervals   = BalanceIntervalsOf txTop
+                     directDeposits            = DirectDepositsOf txTop
+                     directDepositsCredentials = mapˢ stake (dom directDeposits)
+
                 ) where
         
         s₁ : CertState
-        s₁ = ⟦ ⟦ VoteDelegsOf s₀ , StakeDelegsOf s₀ , applyWithdrawals Γ.withdrawals (RewardsOf s₀) , DepositsOf (DStateOf s₀) ⟧
+        s₁ = ⟦ ⟦ VoteDelegsOf s₀ , StakeDelegsOf s₀ , applyWithdrawals withdrawals (RewardsOf s₀) , DepositsOf (DStateOf s₀) ⟧
                , PStateOf s₀
                , ⟦ refreshedDReps
                  , CCHotKeysOf s₀
                  , DepositsOf (GStateOf s₀) ⟧ ⟧
 
-        computeProof : ComputationResult String (∃-syntax (_⊢_⇀⦇_,ENTITIES⦈_ Γ s₀ dCerts))
-        computeProof with ¿ filterˢ isKeyHash wdrlCreds ⊆ dom (VoteDelegsOf s₀)
-                          × wdrlCreds ⊆ dom (RewardsOf s₀)
-                          × (∀[ (addr , amt) ∈ Γ.withdrawals ˢ ] amt ≤ maybe id 0 (lookupᵐ? (RewardsOf s₀) (stake addr)))
-                          ¿ | Computational-CERTS.computeProof ⟦ EpochOf Γ , PParamsOf Γ , ColdCredentialsOf Γ ⟧ s₁ dCerts
+        computeProof : ComputationResult String (∃-syntax (_⊢_⇀⦇_,ENTITIES⦈_ Γ s₀ txTop))
+        computeProof with ¿
+            ∙ ∀[ a ∈ dom withdrawals ] NetworkIdOf a ≡ NetworkId
+            ∙ withdrawalsCredentials ⊆ dom (RewardsOf s₀)
+
+            ∙ (Γ.legacyMode ≡ true →
+                ∙ ∀[ (addr , amt) ∈ withdrawals ˢ ] amt ≡ maybe id 0 (lookupᵐ? (RewardsOf s₀) (stake addr))
+                ∙ ∀[ (addr , amt) ∈ withdrawalsSubTxs ˢ ] amt ≤ maybe id 0 (lookupᵐ? Γ.rewards₀ (stake addr)))
+
+            ∙ (Γ.legacyMode ≡ false →
+                ∙ withdrawalsCredentials ⊆ dom Γ.rewards₀
+                ∙ ∀[ (addr , amt) ∈ (withdrawalsSubTxs ∪⁺ withdrawals) ˢ ] amt ≤ maybe id 0 (lookupᵐ? Γ.rewards₀ (stake addr)))
+
+            ∙ dom accountBalanceIntervals ⊆ dom (RewardsOf s₀)
+            ∙ ∀[ (c , interval) ∈ accountBalanceIntervals ˢ ]
+                (InBalanceInterval (maybe id 0 (lookupᵐ? (RewardsOf s₀) c)) interval)
+
+            ∙ ∀[ a ∈ dom directDeposits ] NetworkIdOf a ≡ NetworkId
+          ¿ | Computational-CERTS.computeProof ⟦ Γ.epoch , Γ.pp , Γ.coldCredentials ⟧ s₁ (DCertsOf txTop)
         ... | no ¬p | _ = failure ""
         ... | yes _ | failure e = failure e
-        ... | yes (p₁ , p₂ , p₃) | success (s₂ , p)
-          with ¿ ddCreds ⊆ dom (RewardsOf s₂) ¿
+        ... | yes (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇) | success (s₂ , p)
+          with ¿
+            ∙ directDepositsCredentials ⊆ dom (RewardsOf s₂) ¿
         ... | no ¬p = failure ""
-        ... | yes p₄ = success (-, (ENTITIES (p₁ , p₂ , p₃ , p , p₄)))
+        ... | yes p₈ = success (-, (ENTITIES (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p , p₇ , p₈)))
     
-        completeness : ∀ (s' : CertState) → Γ ⊢ s₀ ⇀⦇ dCerts ,ENTITIES⦈ s' → map proj₁ computeProof ≡ success s'
-        completeness s' (ENTITIES (p₁ , p₂ , p₃ , p , p₄))
-          with ¿ filterˢ isKeyHash wdrlCreds ⊆ dom (VoteDelegsOf s₀)
-               × wdrlCreds ⊆ dom (RewardsOf s₀)
-               × (∀[ (addr , amt) ∈ Γ.withdrawals ˢ ] amt ≤ maybe id 0 (lookupᵐ? (RewardsOf s₀) (stake addr)))
-               ¿ | Computational-CERTS.computeProof ⟦ EpochOf Γ , PParamsOf Γ , ColdCredentialsOf Γ ⟧ s₁ dCerts | Computational-CERTS.completeness _ _ _ _ p
-        ... | no ¬p | _ | p' = ⊥-elim (¬p (p₁ , p₂ , p₃))
+        completeness : ∀ (s' : CertState) → Γ ⊢ s₀ ⇀⦇ txTop ,ENTITIES⦈ s' → map proj₁ computeProof ≡ success s'
+        completeness s' (ENTITIES (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p , p₇ , p₈))
+          with ¿
+            ∙ ∀[ a ∈ dom withdrawals ] NetworkIdOf a ≡ NetworkId
+            ∙ withdrawalsCredentials ⊆ dom (RewardsOf s₀)
+
+            ∙ (Γ.legacyMode ≡ true →
+                ∙ ∀[ (addr , amt) ∈ withdrawals ˢ ] amt ≡ maybe id 0 (lookupᵐ? (RewardsOf s₀) (stake addr))
+                ∙ ∀[ (addr , amt) ∈ withdrawalsSubTxs ˢ ] amt ≤ maybe id 0 (lookupᵐ? Γ.rewards₀ (stake addr)))
+
+            ∙ (Γ.legacyMode ≡ false →
+                ∙ withdrawalsCredentials ⊆ dom Γ.rewards₀
+                ∙ ∀[ (addr , amt) ∈ (withdrawalsSubTxs ∪⁺ withdrawals) ˢ ] amt ≤ maybe id 0 (lookupᵐ? Γ.rewards₀ (stake addr)))
+
+            ∙ dom accountBalanceIntervals ⊆ dom (RewardsOf s₀)
+            ∙ ∀[ (c , interval) ∈ accountBalanceIntervals ˢ ]
+                (InBalanceInterval (maybe id 0 (lookupᵐ? (RewardsOf s₀) c)) interval)
+
+            ∙ ∀[ a ∈ dom directDeposits ] NetworkIdOf a ≡ NetworkId
+          ¿ | Computational-CERTS.computeProof ⟦ Γ.epoch , Γ.pp , Γ.coldCredentials ⟧ s₁ (DCertsOf txTop) | Computational-CERTS.completeness _ _ _ _ p
+        ... | no ¬p | _ | p' = ⊥-elim (¬p (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇))
         ... | yes _ | failure e | ()
-        ... | yes (p₁ , p₂ , p₃) | success (s₂ , p) | refl
-          with ¿ ddCreds ⊆ dom (RewardsOf s₂) ¿ 
-        ... | no ¬p  = ⊥-elim (¬p p₄)
-        ... | yes p₄ = refl
+        ... | yes (p₁ , p₂ , p₃ , p₄ , p₅ , p₆) | success (s₂ , p) | refl
+          with ¿ directDepositsCredentials ⊆ dom (RewardsOf s₂) ¿
+        ... | no ¬p  = ⊥-elim (¬p p₈)
+        ... | yes _ = refl
 ```
diff --git a/src/Ledger/Dijkstra/Specification/Ledger.lagda.md b/src/Ledger/Dijkstra/Specification/Ledger.lagda.md
index 9bbf84a08..33ba3722f 100644
--- a/src/Ledger/Dijkstra/Specification/Ledger.lagda.md
+++ b/src/Ledger/Dijkstra/Specification/Ledger.lagda.md
@@ -28,7 +28,7 @@ open import Ledger.Dijkstra.Specification.Gov govStructure
 open import Ledger.Dijkstra.Specification.Utxo txs abs
 open import Ledger.Dijkstra.Specification.Utxow txs abs
 open import Ledger.Dijkstra.Specification.Certs govStructure
-open import Ledger.Dijkstra.Specification.Entities govStructure
+open import Ledger.Dijkstra.Specification.Entities txs
 
 open EnactState using (cc)
 ```
@@ -45,7 +45,7 @@ record SubLedgerEnv : Type where
     enactState       : EnactState
     treasury         : Treasury
     utxo₀            : UTxO
-    certState        : CertState
+    rewards₀         : Rewards
     allScripts       : ℙ Script
     isTopLevelValid  : Bool
 
@@ -211,6 +211,7 @@ private variable
   treasury                          : Treasury
   isTopLevelValid                   : Bool
   allScripts                        : ℙ Script
+  rewards₀                          : Rewards
 ```
 -->
 
@@ -278,16 +279,16 @@ data _⊢_⇀⦇_,SUBLEDGER⦈_ : SubLedgerEnv → LedgerState → SubLevelTx 
   SUBLEDGER-V :
       ∙ isTopLevelValid ≡ true
       ∙ ⟦ slot , pp , treasury , utxo₀ , certState , allScripts , isTopLevelValid ⟧ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₁
-      ∙ ⟦ epoch slot , pp , ListOfGovVotesOf stx , allColdCreds govState₀ enactState , WithdrawalsOf stx , DirectDepositsOf stx ⟧ ⊢ certState₀ ⇀⦇ DCertsOf stx ,ENTITIES⦈ certState₁
+      ∙ ⟦ epoch slot , pp , allColdCreds govState₀ enactState , rewards₀ ⟧ ⊢ certState₀ ⇀⦇ stx ,SUBENTITIES⦈ certState₁
       ∙ ⟦ TxIdOf stx , epoch slot , pp , ppolicy , enactState , certState₁ , dom (RewardsOf certState₁) ⟧ ⊢ govState₀ ⇀⦇ GovProposals+Votes stx ,GOVS⦈ govState₁
         ────────────────────────────────
-        ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , certState , allScripts , isTopLevelValid ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧
+        ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , rewards₀ , allScripts , isTopLevelValid ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧
 
   SUBLEDGER-I :
       ∙ isTopLevelValid ≡ false
       ∙ ⟦ slot , pp , treasury , utxo₀ , certState , allScripts , isTopLevelValid  ⟧ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₀
         ────────────────────────────────
-        ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , certState , allScripts , isTopLevelValid ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧
+        ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , rewards₀ , allScripts , isTopLevelValid ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧
 
 _⊢_⇀⦇_,SUBLEDGERS⦈_ : SubLedgerEnv → LedgerState → List SubLevelTx → LedgerState → Type
 _⊢_⇀⦇_,SUBLEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,SUBLEDGER⦈_}
@@ -299,12 +300,15 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LedgerState → TopLevelTx → Ledg
     let  utxo₀ : UTxO
          utxo₀ = UTxOOf utxoState₀
 
+         rewards₀ : Rewards
+         rewards₀ = RewardsOf certState₀
+
          allScripts : ℙ Script
          allScripts = getAllScripts tx utxo₀
     in
       ∙ IsValidFlagOf tx ≡ true
-      ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , certState₀ , allScripts , IsValidFlagOf tx ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧
-      ∙ ⟦ epoch slot , pp , ListOfGovVotesOf tx , allColdCreds govState₁ enactState , WithdrawalsOf tx , DirectDepositsOf tx ⟧ ⊢ certState₁ ⇀⦇ DCertsOf tx ,ENTITIES⦈ certState₂
+      ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , rewards₀ , allScripts , IsValidFlagOf tx ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧
+      ∙ ⟦ epoch slot , pp , allColdCreds govState₁ enactState , true , rewards₀ ⟧ ⊢ certState₁ ⇀⦇ tx ,ENTITIES⦈ certState₂
       ∙ ⟦ TxIdOf tx , epoch slot , pp , ppolicy , enactState , certState₂ , dom (RewardsOf certState₂) ⟧ ⊢ govState₁ ⇀⦇ GovProposals+Votes tx ,GOVS⦈ govState₂
       ∙ ⟦ slot , pp , treasury , utxo₀ , certState₀ , allScripts ⟧ ⊢ utxoState₁ ⇀⦇ tx ,UTXOW⦈ utxoState₂
         ────────────────────────────────
@@ -314,11 +318,14 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LedgerState → TopLevelTx → Ledg
     let  utxo₀ : UTxO
          utxo₀ = UTxOOf utxoState₀
 
+         rewards₀ : Rewards
+         rewards₀ = RewardsOf certState₀
+
          allScripts : ℙ Script
          allScripts = getAllScripts tx utxo₀
     in
       ∙ IsValidFlagOf tx ≡ false
-      ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , certState₀ , allScripts , IsValidFlagOf tx ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧
+      ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , rewards₀ , allScripts , IsValidFlagOf tx ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧
       ∙ ⟦ slot , pp , treasury , utxo₀ , certState₀ , allScripts ⟧ ⊢ utxoState₀ ⇀⦇ tx ,UTXOW⦈ utxoState₁
         ────────────────────────────────
         ⟦ slot , ppolicy , pp , enactState , treasury ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ tx ,LEDGER⦈ ⟦ utxoState₁ , govState₀ , certState₀ ⟧
diff --git a/src/Ledger/Dijkstra/Specification/Utxo.lagda.md b/src/Ledger/Dijkstra/Specification/Utxo.lagda.md
index 77d2334fe..7a48065b6 100644
--- a/src/Ledger/Dijkstra/Specification/Utxo.lagda.md
+++ b/src/Ledger/Dijkstra/Specification/Utxo.lagda.md
@@ -345,43 +345,6 @@ the transaction and that amount is deposited into accounts.
                             + ∑ˡ[ stx ← SubTransactionsOf txTop ] (producedTx stx)
 ```
 
-## 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.
-
-In the preservation-of-value equation, direct deposits appear on the
-*produced* side: value leaves the UTxO and enters account balances.  The
-`getCoin (DirectDepositsOf tx)` term, appearing in the definition of
-`producedTx`{.AgdaFunction}, sums the ADA of all direct deposits in
-the transaction.
-
-### Phantom Asset Prevention {#subsubsec:phantom-asset-prevention}
-
-```agda
-NoPhantomWithdrawals : Rewards → TopLevelTx → Type
-NoPhantomWithdrawals preBalances txTop =
-  ∀[ (addr , amt) ∈ allWithdrawals txTop ˢ ]
-    amt ≤ maybe id 0 (lookupᵐ? preBalances (RewardAddress.stake addr))
-```
-
-**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.
-
-**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
 
 ### Phase-2 Validation
@@ -558,14 +521,8 @@ data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv × Bool → UTxOState → TopLevelTx → UT
     ∙ ∀[ (_ , o) ∈ ∣ TxOutsOf txTop ∣ ] (serializedSize (txOutToValue o) ≤ maxValSize (PParamsOf Γ))
     ∙ ∀[ (a , _) ∈ range (TxOutsOf txTop) ] (Sum.All (const ⊤) (λ a → AttrSizeOf a ≤ maxBootstrapAddrSize)) a
     ∙ ∀[ (a , _) ∈ range (TxOutsOf txTop) ] (netId a ≡ NetworkId)
-    ∙ ∀[ a ∈ dom (WithdrawalsOf txTop)] NetworkIdOf a ≡ NetworkId
-    ∙ ∀[ a ∈ dom (DirectDepositsOf txTop)] (NetworkIdOf a ≡ NetworkId)
     ∙ MaybeNetworkIdOf txTop ~ just NetworkId
     ∙ CurrentTreasuryOf txTop  ~ just (TreasuryOf Γ)
-    ∙ mapˢ stake (dom (DirectDepositsOf txTop)) ⊆ dom (RewardsOf Γ)
-    ∙ dom (BalanceIntervalsOf txTop) ⊆ dom (RewardsOf Γ)
-    ∙ ∀[ (c , interval) ∈ BalanceIntervalsOf txTop ˢ ]
-        (InBalanceInterval (maybe id 0 (lookupᵐ? (RewardsOf Γ) c)) interval)
     ∙ Γ ⊢ _ ⇀⦇ txTop ,UTXOS⦈ _
       ────────────────────────────────
     let