[Dijkstra] CIP-159-10: Apply direct deposits in POST-CERT (#1122)

Per @carlostome's review of #1161, move CIP-159 direct-deposit
application out of the LEDGER/SUBLEDGER orchestration rules and into
the POST-CERT sub-rule of CERTS, alongside the existing voteDelegs
filtering.

CertEnv gains a sixth field, directDeposits, populated by LEDGER-V
(DirectDepositsOf tx) and SUBLEDGER-V (DirectDepositsOf stx) when
constructing each CERTS invocation's environment.  POST-CERT (CERT-post)
gains a premise dom directDeposits ⊆ dom rewards and updates its
post-state's rewards to rewards ∪⁺ directDeposits.

SUBLEDGER-V and LEDGER-V revert to threading-only: certStateWithDDeps,
the certStateFinal let-binding, and the dom-check premises are removed.
Computational instances are updated correspondingly.

Per-transaction semantics are preserved (POST-CERT runs at the end of
each transaction's CERTS invocation).  Phantom-asset prevention via
NoPhantomWithdrawals is unaffected (accountBalances is fixed at the
pre-batch snapshot).  depositsChange remains orthogonal
(applyDirectDeposits touches rewards only; calculateDepositsChange
reads deposits only).

Direct-deposit documentation moves from Ledger.lagda.md to the POST-CERT
section of Certs.lagda.md.

Author: williamdemeo

src/Ledger/Dijkstra/Foreign/Certs.lagda.md

@@ -59,11 +59,12 @@ instance
 
 record CertEnv' : Type where
   field
-    epoch     : Epoch
-    pp        : PParams
-    votes     : List GovVote'
-    wdrls     : RewardAddress ⇀ Coin
-    coldCreds : ℙ Credential
+    epoch          : Epoch
+    pp             : PParams
+    votes          : List GovVote'
+    wdrls          : RewardAddress ⇀ Coin
+    coldCreds      : ℙ Credential
+    directDeposits : DirectDeposits
 
 instance
   HsTy-CertEnv' = autoHsType CertEnv'
@@ -74,8 +75,8 @@ instance
 
   mkCertEnv' : Convertible CertEnv CertEnv'
   mkCertEnv' = λ where
-    .to   ce → let module ce = CertEnv ce in record { epoch = ce.epoch ; pp = ce.pp ; votes = to ce.votes ; wdrls = ce.wdrls ; coldCreds = ce.coldCreds }
-    .from ce → let module ce = CertEnv' ce in record { epoch = ce.epoch ; pp = ce.pp ; votes = from ce.votes ; wdrls = ce.wdrls ; coldCreds = ce.coldCreds }
+    .to   ce → let module ce = CertEnv ce in record { epoch = ce.epoch ; pp = ce.pp ; votes = to ce.votes ; wdrls = ce.wdrls ; coldCreds = ce.coldCreds ; directDeposits = ce.directDeposits }
+    .from ce → let module ce = CertEnv' ce in record { epoch = ce.epoch ; pp = ce.pp ; votes = from ce.votes ; wdrls = ce.wdrls ; coldCreds = ce.coldCreds ; directDeposits = ce.directDeposits }
 
   HsTy-CertEnv = MkHsType CertEnv (HsType CertEnv')
   Conv-CertEnv = mkCertEnv' ⨾ Conv-CertEnv'

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

@@ -85,11 +85,12 @@ cwitness (ccreghot c _)      = just c
 -- Certification Types
 record CertEnv : Type where
   field
-    epoch     : Epoch
-    pp        : PParams
-    votes     : List GovVote
-    wdrls     : Withdrawals
-    coldCreds : ℙ Credential
+    epoch           : Epoch
+    pp              : PParams
+    votes           : List GovVote
+    wdrls           : Withdrawals
+    coldCreds       : ℙ Credential
+    directDeposits  : DirectDeposits
 
 record DState : Type where
   constructor ⟦_,_,_,_⟧ᵈ
@@ -255,6 +256,7 @@ private variable
   pools fPools           : Pools
   retiring               : Retiring
   wdrls                  : Withdrawals
+  dd                     : DirectDeposits
   A                      : Type
   deposits deposits'     : A ⇀ Coin
 
@@ -290,8 +292,9 @@ applyDirectDeposits : DirectDeposits → DState → DState
 applyDirectDeposits dd ds = record ds { rewards = RewardsOf ds ∪⁺ dd }
 ```
 
-The `LEDGER`{.AgdaDatatype} rule will call `applyDirectDeposits`{.AgdaFunction} to
-credit direct deposits to account balances as part of processing a transaction batch.
+The `POST-CERT`{.AgdaDatatype} rule calls `applyDirectDeposits`{.AgdaFunction} to
+credit each transaction's direct deposits to its account balances after certificate
+processing.  See *Direct Deposit Application (CIP-159)* below for details.
 
 ```agda
 applyWithdrawals : Withdrawals → Rewards → Rewards
@@ -407,32 +410,32 @@ data _⊢_⇀⦇_,GOVCERT⦈_ : CertEnv → GState → DCert → GState → Type
   GOVCERT-regdrep :
     ∙ (d ≡ pp .drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps)
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ dReps , ccKeys , deposits ⟧ ⇀⦇ regdrep c d an ,GOVCERT⦈ ⟦ ❴ c , e + pp .drepActivity ❵ ∪ˡ dReps , ccKeys , deposits ∪⁺ ❴ c , d ❵ ⟧
+      ⟦ e , pp , vs , wdrls , cc , dd ⟧ ⊢ ⟦ dReps , ccKeys , deposits ⟧ ⇀⦇ regdrep c d an ,GOVCERT⦈ ⟦ ❴ c , e + pp .drepActivity ❵ ∪ˡ dReps , ccKeys , deposits ∪⁺ ❴ c , d ❵ ⟧
 
   GOVCERT-deregdrep :
     ∙ c ∈ dom dReps
     ∙ (c , d) ∈ deposits
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ dReps , ccKeys , deposits ⟧ ⇀⦇ deregdrep c d ,GOVCERT⦈ ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys , deposits ∣ ❴ c ❵ ᶜ ⟧
+      ⟦ e , pp , vs , wdrls , cc , dd ⟧ ⊢ ⟦ dReps , ccKeys , deposits ⟧ ⇀⦇ deregdrep c d ,GOVCERT⦈ ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys , deposits ∣ ❴ c ❵ ᶜ ⟧
 
   GOVCERT-ccreghot :
     ∙ (c , nothing) ∉ ccKeys
     ∙ c ∈ cc
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ dReps , ccKeys , deposits ⟧ ⇀⦇ ccreghot c mc ,GOVCERT⦈ ⟦ dReps , ❴ c , mc ❵ ∪ˡ ccKeys , deposits ⟧
+      ⟦ e , pp , vs , wdrls , cc , dd ⟧ ⊢ ⟦ dReps , ccKeys , deposits ⟧ ⇀⦇ ccreghot c mc ,GOVCERT⦈ ⟦ dReps , ❴ c , mc ❵ ∪ˡ ccKeys , deposits ⟧
 
 -- CERT Transition System --
 data _⊢_⇀⦇_,CERT⦈_  : CertEnv → CertState → DCert → CertState → Type where
 
   CERT-deleg :
     ∙ ⟦ pp , PState.pools stᵖ , dom (GState.dreps stᵍ) ⟧ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ' , stᵖ , stᵍ ⟧
+      ⟦ e , pp , vs , wdrls , cc , dd ⟧ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ' , stᵖ , stᵍ ⟧
 
   CERT-pool :
     ∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ' , stᵍ ⟧
+      ⟦ e , pp , vs , wdrls , cc , dd ⟧ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ' , stᵍ ⟧
 
   CERT-gov :
     ∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
@@ -473,7 +476,7 @@ data _⊢_⇀⦇_,PRE-CERT⦈_ : CertEnv → CertState → ⊤ → CertState →
     ∙ wdrlCreds ⊆ dom rewards
     ∙ ∀[ (addr , amt) ∈ wdrls ˢ ] amt ≤ maybe id 0 (lookupᵐ? rewards (stake addr))
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards , deposits ⟧ , stᵖ , ⟦ dReps , ccHotKeys , deposits' ⟧ ⟧ ⇀⦇ _ ,PRE-CERT⦈ ⟦ ⟦ voteDelegs , stakeDelegs , applyWithdrawals wdrls rewards , deposits ⟧ , stᵖ , ⟦ refreshedDReps , ccHotKeys , deposits' ⟧ ⟧
+      ⟦ e , pp , vs , wdrls , cc , dd ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards , deposits ⟧ , stᵖ , ⟦ dReps , ccHotKeys , deposits' ⟧ ⟧ ⇀⦇ _ ,PRE-CERT⦈ ⟦ ⟦ voteDelegs , stakeDelegs , applyWithdrawals wdrls rewards , deposits ⟧ , stᵖ , ⟦ refreshedDReps , ccHotKeys , deposits' ⟧ ⟧
 ```
 
 **TODO**: Version restriction (deferred).  CIP-159 specifies that partial withdrawals are
@@ -484,14 +487,55 @@ follow-up issue.
 
 ## POST-CERT Transition Rule
 
+### Direct Deposit Application (CIP-159)
+
+The `POST-CERT`{.AgdaDatatype} rule applies CIP-159 direct deposits to the
+threaded `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}.
+
+The premise `dom directDeposits ⊆ dom rewards` 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 check is
+performed against the post-`CERT`{.AgdaDatatype} `rewards`{.AgdaField} of the
+*same* transaction, so deregistrations performed by *prior* sub-transactions in
+the same batch are correctly accounted for: a sub-transaction whose deposit
+targets a credential deregistered earlier in the batch will fail this premise.
+
+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} module by the
+`NoPhantomWithdrawals`{.AgdaFunction} predicate, which bounds *batch-wide*
+withdrawal totals (per reward address) by the `accountBalances`{.AgdaField} field
+of `UTxOEnv`{.AgdaRecord} / `SubUTxOEnv`{.AgdaRecord} — the *pre-batch* snapshot
+`RewardsOf certState₀`{.AgdaBound}.  Because `accountBalances`{.AgdaField} is
+fixed at the pre-batch value and never updated by direct deposit application,
+the phantom-asset prohibition holds regardless of the per-transaction
+`rewards`{.AgdaField} updates done by `POST-CERT`{.AgdaDatatype}.
+
+
 ```agda
 data _⊢_⇀⦇_,POST-CERT⦈_ : CertEnv → CertState → ⊤ → CertState → Type where
 
   CERT-post :
     let activeVDelegs = mapˢ vDelegCredential (dom (DRepsOf stᵍ))
                          ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ [])
     in
-      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards , deposits ⟧ , stᵖ , stᵍ ⟧ ⇀⦇ _ ,POST-CERT⦈ ⟦ ⟦ voteDelegs ∣^ activeVDelegs , stakeDelegs , rewards , deposits ⟧ , stᵖ , stᵍ ⟧
+    ∙ dom dd ⊆ dom rewards
+      ────────────────────────────────
+      ⟦ e , pp , vs , wdrls , cc , dd ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards , deposits ⟧ , stᵖ , stᵍ ⟧ ⇀⦇ _ ,POST-CERT⦈ ⟦ ⟦ voteDelegs ∣^ activeVDelegs , stakeDelegs , rewards ∪⁺ dd , deposits ⟧ , stᵖ , stᵍ ⟧
+
 
 
 -- CERTS Transition System --

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

@@ -90,10 +90,10 @@ instance
   Computational-POOL .completeness _ stᵖ (regpool c _) _ (POOL-reg p)
     with ¿ Is-just (lookupᵐ? (PoolsOf stᵖ) c) ¿
   ... | yes p' = ⊥-elim (¬Is-just↔Is-nothing _ .from p p')
-  ... | no ¬p = refl
+  ... | no _ = refl
   Computational-POOL .completeness _ stᵖ (regpool c _) _ (POOL-rereg p)
     with ¿ Is-just (lookupᵐ? (PoolsOf stᵖ) c) ¿
-  ... | yes p = refl
+  ... | yes _ = refl
   ... | no ¬p = ⊥-elim (¬p p)
   Computational-POOL .completeness _ _ (retirepool _ _) _ POOL-retirepool = refl
 
@@ -147,7 +147,7 @@ instance
     dCert@(regpool c poolParams) cs' (CERT-pool h)
     with computeProof (CertEnv.pp ce) (CertState.pState cs) dCert
     | completeness _ _ _ _ h
-  ... | success x | refl = refl
+  ... | success _ | refl = refl
   Computational-CERT .completeness ce cs
     dCert@(retirepool c e) cs' (CERT-pool h)
     with completeness _ _ _ _ h
@@ -182,14 +182,22 @@ instance
         p .proj₂ = refl
 
   Computational-POST-CERT : Computational _⊢_⇀⦇_,POST-CERT⦈_ String
-  Computational-POST-CERT .computeProof ce cs tt = success ( cs' , CERT-post)
+  Computational-POST-CERT .computeProof ce cs tt with ¿ dom (CertEnv.directDeposits ce) ⊆ dom (RewardsOf cs) ¿
+  ... | (no ¬p) = failure (genErrors ¬p)
+  ... | (yes p) = success (cs' , CERT-post p)
     where
       validVoteDelegs : VoteDelegs
       validVoteDelegs = VoteDelegsOf cs ∣^ (mapˢ vDelegCredential (dom (DRepsOf cs)) ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ []) )
+
+      newRewards : Rewards
+      newRewards = RewardsOf cs ∪⁺ CertEnv.directDeposits ce
+
       cs' : CertState
-      cs' = ⟦ ⟦ validVoteDelegs , _ , _ ⟧ , PStateOf cs , GStateOf cs ⟧
+      cs' = ⟦ ⟦ validVoteDelegs , StakeDelegsOf cs , newRewards , DepositsOf (DStateOf cs) ⟧ , PStateOf cs , GStateOf cs ⟧
 
-  Computational-POST-CERT .completeness ce cs _ cs' CERT-post = refl
+  Computational-POST-CERT .completeness ce cs _ cs' (CERT-post p) with ¿ dom (CertEnv.directDeposits ce) ⊆ dom (RewardsOf cs) ¿
+  ... | yes _ = refl
+  ... | no ¬p = ⊥-elim (¬p p)
 
 Computational-CERTS : Computational _⊢_⇀⦇_,CERTS⦈_ String
 Computational-CERTS = it