[Dijkstra] CIP-159-10: Apply batch-wide direct deposits in LEDGER rule (#1122)

After all sub-rule transitions (`SUBLEDGERS`, `CERTS`, `GOVS`, `UTXOW`),
apply batch-wide direct deposits to the final CertState via
`applyDirectDeposits` and `allDirectDeposits`.

`Ledger.lagda.md`:
+  Update `LEDGER-V` output: compute `certStateFinal` by applying
   `allDirectDeposits` to `certState₂`, use `certStateFinal` in the
   output `LedgerState` and in `rmOrphanDRepVotes`;
+  `LEDGER-I` unchanged (invalid batches don't apply deposits);
+  Document direct deposit application ordering and phantom asset
   prevention rationale.

`Ledger/Properties/Computational.lagda.md`:
+  Update `computeProof` valid branch to compute `certStateFinal` and use
   it in the output `LedgerState`.

Author: williamdemeo

CHANGELOG.md

@@ -4,8 +4,9 @@
 
 ### WIP
 
+- Apply batch-wide direct deposits to `CertState` in `LEDGER-V` output (CIP-159).
 - Forbid CIP-159 fields (`txDirectDeposits`, `txBalanceIntervals`) in legacy mode via explicit `UTXOW-legacy` premises.
-- Allow partial withdrawals in `PRE-CERT` rule; define `applyWithdrawals` and `_≤ᵐ_` (CIP-159).
+- Allow partial withdrawals in `PRE-CERT` rule; define `applyWithdrawals` (CIP-159).
 - Extend `TxInfo` with `txDirectDeposits` and `txBalanceIntervals` fields (CIP-159).
 - Remove `allBalanceIntervals` batch-level aggregation helper; balance interval
   assertions will be checked per-(sub)transaction in `UTXO`/`SUBUTXO` rules (see #1117).

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

@@ -305,8 +305,31 @@ data _⊢_⇀⦇_,SUBLEDGER⦈_ : SubLedgerEnv → LedgerState → SubLevelTx 
 
 _⊢_⇀⦇_,SUBLEDGERS⦈_ : SubLedgerEnv → LedgerState → List SubLevelTx → LedgerState → Type
 _⊢_⇀⦇_,SUBLEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,SUBLEDGER⦈_}
+```
+
+**Direct Deposit Application (CIP-159)**.  After all sub-rule transitions
+(`SUBLEDGERS`{.AgdaDatatype}, `CERTS`{.AgdaDatatype}, `GOVS`{.AgdaDatatype},
+`UTXOW`{.AgdaDatatype}), batch-wide direct deposits are applied to the final
+`CertState`{.AgdaRecord}.  The function `applyDirectDeposits`{.AgdaFunction} (from
+the `Certs`{.AgdaModule} module) adds deposit amounts to account balances via `∪⁺`,
+and `allDirectDeposits`{.AgdaFunction} (from the `Transaction`{.AgdaModule} module)
+aggregates direct deposits across the top-level transaction and all sub-transactions.
+
+Direct deposits are applied *after* withdrawal processing (in `CERTS`{.AgdaDatatype})
+to ensure that withdrawals are checked against pre-batch balances.  This prevents
+phantom asset attacks where a deposit from one sub-transaction inflates the balance
+available for withdrawal by another sub-transaction in the same batch.
+
+`depositsChange`{.AgdaFunction} is computed from `certStateᵢ` (`i ∈ {0,1,2}`)
+(not `certStateFinal`) since it represents net deposit change across the batch
+(not direct deposit value transfers) and reflects registration/deregistration.
 
+`rmOrphanDRepVotes` uses `certStateFinal` (not `certState₂`) so it sees
+the post-deposit `DRep` state.  (In practice, `applyDirectDeposits`{.AgdaFunction}
+only modifies rewards, so `rmOrphanDRepVotes` would produce the same result either
+way, but using `certStateFinal` is semantically correct.)
 
+```agda
 data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LedgerState → TopLevelTx → LedgerState → Type where
 
   LEDGER-V :
@@ -321,15 +344,17 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LedgerState → TopLevelTx → Ledg
 
          depositsChange : DepositsChange
          depositsChange = calculateDepositsChange certState₀ certState₁ certState₂
+
+         certStateFinal : CertState
+         certStateFinal = record certState₂ { dState = applyDirectDeposits (allDirectDeposits tx) (DStateOf certState₂) }
     in
       ∙ IsValidFlagOf tx ≡ true
       ∙ ⟦ 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 , RewardsOf certState₀ ⟧ ⊢ utxoState₁ ⇀⦇ tx ,UTXOW⦈ utxoState₂
         ────────────────────────────────
-        ⟦ slot , ppolicy , pp , enactState , treasury ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ tx ,LEDGER⦈ ⟦ utxoState₂ , rmOrphanDRepVotes certState₂ govState₂ , certState₂ ⟧
-
+        ⟦ slot , ppolicy , pp , enactState , treasury ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ tx ,LEDGER⦈ ⟦ utxoState₂ , rmOrphanDRepVotes certStateFinal govState₂ , certStateFinal ⟧
 
   LEDGER-I :
     let  utxo₀ : UTxO

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

@@ -330,9 +330,10 @@ instance
                       -- UTXOW must run from the post-SUBLEDGERS UTxOState (utxoSt₁)
                       computeUtxow utxoΓ utxoSt₁ txTop >>= λ where
                         (utxoSt₂ , utxoStep) →
-                          let finalGov = rmOrphanDRepVotes certSt₂ govSt₂
+                          let certStateFinal = record certSt₂ { dState = applyDirectDeposits (allDirectDeposits txTop) (DStateOf certSt₂) }
+                              finalGov = rmOrphanDRepVotes certStateFinal govSt₂
                           in
-                          success ( ⟦ utxoSt₂ , finalGov , certSt₂ ⟧ˡ
+                          success ( ⟦ utxoSt₂ , finalGov , certStateFinal ⟧ˡ
                                   , LEDGER-V (isV , subStep , certStep , govStep , utxoStep))
 
         (no ¬isV) →