LEDGER-V: forbid direct deposits to credentials deregistered in same batch

`applyDirectDeposits` uses `∪⁺` (union-with-addition) on the `rewards`
map, so a credential not present in `RewardsOf certState₂` is added as a
new entry rather than rejected.  The pre-existing SUBUTXO/UTXO premise
`dom (DirectDepositsOf tx) ⊆ dom (AccountBalancesOf Γ)` only checks
against the pre-batch balances `RewardsOf certState₀`, so it does not
catch the case where a credential is registered pre-batch, deregistered
during `CERTS`, and direct-deposited to in the same batch.  Without the
new premise, the resulting `certStateFinal` is internally inconsistent:
the credential has a positive `rewards` entry but no corresponding
`voteDelegs`, `stakeDelegs`, or `deposits` entry — effectively re-
registering the credential without a key deposit.

Add the phase-1 premise

    dom (allDirectDeposits tx) ⊆ dom (RewardsOf certState₂)

to `LEDGER-V` to rule this out.  Filtering `allDirectDeposits tx` by
`dom (RewardsOf certState₂)` would be an alternative, but it would
silently destroy user funds when a deposit and a deregistration race in
the same batch.  The premise is symmetric to (and complements) the
existing pre-batch SUBUTXO/UTXO check.

Update `Ledger/Properties/Computational.lagda.md` for the new premise,
and pass `UTxOStateOf s₁` explicitly to `computeUtxow` in the LEDGER
valid branch (the previous `_` resolved by chained unification through
the LEDGER-V constructor, which was fragile and obscured intent).

TODO: fix `Ledger/Properties/Computational.lagda.md`; it's choking on
the new premise.

Author: williamdemeo

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

@@ -329,6 +329,15 @@ the post-deposit `DRep` state.  (In practice, `applyDirectDeposits`{.AgdaFunctio
 only modifies rewards, so `rmOrphanDRepVotes` would produce the same result either
 way, but using `certStateFinal` is semantically correct.)
 
+**Deposits target post-batch registered accounts**.  `SUBUTXO`{.AgdaDatatype}
+and `UTXO`{.AgdaDatatype} check that direct-deposit targets are registered in the
+*pre-batch* balances, but they cannot account for deregistrations that occur during
+the batch.  Therefore, we add a new premise, `dom (allDirectDeposits tx) ⊆ dom (RewardsOf
+certState₂)`, to check that `applyDirectDeposits` does not silently re-introduce a
+deregistered credential into the `rewards` map without re-registering it via
+`voteDelegs`, `stakeDelegs`, or `deposits`, as that would result in an inconsistent
+`DState`.  The premise rules this out at phase 1.
+
 ### Design Rationale: Batch-wide Direct Deposit Application
 
 A natural alternative to applying direct deposits batch-wide (as above) is to
@@ -425,6 +434,7 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LedgerState → TopLevelTx → Ledg
       ∙ IsValidFlagOf tx ≡ true
       ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , IsValidFlagOf tx , allScripts , 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₂
+      ∙ dom (allDirectDeposits tx) ⊆ dom (RewardsOf certState₂)
       ∙ ⟦ TxIdOf tx , epoch slot , pp , ppolicy , enactState , certState₂ , dom (RewardsOf certState₂) ⟧ ⊢ govState₁ ⇀⦇ GovProposals+Votes tx ,GOVS⦈ govState₂
       ∙ ⟦ slot , pp , treasury , utxo₀ , depositsChange , allScripts , RewardsOf certState₀ ⟧ ⊢ utxoState₁ ⇀⦇ tx ,UTXOW⦈ utxoState₂
         ────────────────────────────────

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

@@ -224,10 +224,12 @@ instance
           (certSt₂ , certStep) → computeGov (govΓOf Γ txTop certSt₂) (GovStateOf s₁) (GovProposals+Votes txTop) >>= λ where
             (govSt₂ , govStep) →
               -- UTXOW must run from the post-SUBLEDGERS UTxOState ((UTxOState s₁))
-              computeUtxow (utxoΓ-valid Γ s txTop (CertStateOf s₁) certSt₂) _ txTop >>= λ where
-                (utxoSt₂ , utxoStep) →
-                  success ( ⟦ utxoSt₂ , rmOrphanDRepVotes (certStateWithDDeps txTop certSt₂) govSt₂ , certStateWithDDeps txTop certSt₂ ⟧ˡ
-                          , LEDGER-V (isV , subStep , certStep , govStep , utxoStep))
+              computeUtxow (utxoΓ-valid Γ s txTop (CertStateOf s₁) certSt₂) (UTxOStateOf s₁) txTop >>= λ where
+                (utxoSt₂ , utxoStep) → case ¿ dom (allDirectDeposits txTop) ⊆ dom (RewardsOf certSt₂) ¿ of λ where
+                  (yes h) →
+                    success ( ⟦ utxoSt₂ , rmOrphanDRepVotes (certStateWithDDeps txTop certSt₂) govSt₂ , certStateWithDDeps txTop certSt₂ ⟧ˡ
+                            , LEDGER-V (isV , subStep , certStep , h , govStep , utxoStep) )
+                  (no _)  → failure "direct deposit target was deregistered during this batch"
 
       (no ¬isV) → case computeSubledgers (subΓOf Γ s txTop) s (SubTransactionsOf txTop) of λ where
         (failure e) → failure e
@@ -252,7 +254,7 @@ instance
 ```agda
     completeness Γ s txTop s'
       (LEDGER-V {certState₁ = certSt₁} {certSt₂} {utxoState₁ = utxoSt₁} {govSt₁} {govSt₂} {utxoSt₂}
-        (isV , subStep , certStep , govStep , utxoStep))
+        (isV , subStep , certStep , h , govStep , utxoStep))
       with IsValidFlagOf txTop ≟ true
     ... | no ¬isV = contradiction isV ¬isV
     ... | yes refl
@@ -272,7 +274,11 @@ instance
       with computeUtxow (utxoΓ-valid Γ s txTop certSt₁ certSt₂) utxoSt₁ txTop
          | complete {STS = _⊢_⇀⦇_,UTXOW⦈_}
              (utxoΓ-valid Γ s txTop certSt₁ certSt₂) utxoSt₁ txTop utxoSt₂ utxoStep
-    ... | success (utxoSt₂ , _) | refl = refl
+    ... | success (utxoSt₂ , _) | refl
+      with ¿ dom (allDirectDeposits txTop) ⊆ dom (RewardsOf certSt₂) ¿
+    ... | yes _  = refl
+    ... | no ¬h  = ⊥-elim (¬h h)
+
 
     completeness Γ s txTop s' (LEDGER-I {utxoState₁ = utxoSt₁} (isI , subStep , utxoStep))
       with IsValidFlagOf txTop ≟ true