moved rewards check to LEDGER

Author: Soupstraw

src/Ledger/Certs.lagda

@@ -466,15 +466,14 @@ data _⊢_⇀⦇_,CERTBASE⦈_ where
         wdrlCreds        = mapˢ stake (dom wdrls)
         validVoteDelegs  = voteDelegs ∣^ (  mapˢ (credVoter DRep) (dom dReps)
                                         ∪ fromList (noConfidenceRep ∷ abstainRep ∷ []) )
+        rewards'         = constMap wdrlCreds 0 ∪ˡ rewards
     in
-    ∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
-      ────────────────────────────────
       ⟦ e , pp , vs , wdrls , cc ⟧ ⊢
         ⟦ ⟦ voteDelegs , stakeDelegs , rewards ⟧
         , stᵖ
         , ⟦ dReps , ccHotKeys ⟧
         ⟧ ⇀⦇ _ ,CERTBASE⦈
-        ⟦ ⟦ validVoteDelegs , stakeDelegs , constMap wdrlCreds 0 ∪ˡ rewards ⟧
+        ⟦ ⟦ validVoteDelegs , stakeDelegs , rewards' ⟧
         , stᵖ
         , ⟦ refreshedDReps , ccHotKeys ⟧
         ⟧

src/Ledger/Conway/Conformance/Certs.agda

@@ -200,20 +200,19 @@ data _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → T
 data _⊢_⇀⦇_,CERTBASE⦈_ : CertEnv → CertState → ⊤ → CertState → Type where
   CERT-base :
     let open PParams pp
-        refresh         = mapPartial getDRepVote (fromList vs)
-        refreshedDReps  = mapValueRestricted (const (e + drepActivity)) dReps refresh
-        wdrlCreds       = mapˢ stake (dom wdrls)
+        refresh          = mapPartial getDRepVote (fromList vs)
+        refreshedDReps   = mapValueRestricted (const (e + drepActivity)) dReps refresh
+        wdrlCreds        = mapˢ stake (dom wdrls)
         validVoteDelegs  = voteDelegs ∣^ (mapˢ (credVoter DRep) (dom dReps) ∪ fromList (noConfidenceRep ∷ abstainRep ∷ []))
+        rewards'         = constMap wdrlCreds 0 ∪ˡ rewards
     in
-    ∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
-      ────────────────────────────────
       ⟦ e , pp , vs , wdrls , cc ⟧ ⊢
       ⟦ ⟦ voteDelegs , stakeDelegs , rewards , ddep ⟧
       , stᵖ
       , ⟦ dReps , ccHotKeys , gdep ⟧
       ⟧
       ⇀⦇ _ ,CERTBASE⦈
-      ⟦ ⟦ validVoteDelegs , stakeDelegs , constMap wdrlCreds 0 ∪ˡ rewards , ddep ⟧
+      ⟦ ⟦ validVoteDelegs , stakeDelegs , rewards' , ddep ⟧
       , stᵖ
       , ⟦ refreshedDReps , ccHotKeys , gdep ⟧
       ⟧

src/Ledger/Conway/Conformance/Certs/Properties.agda

@@ -194,13 +194,8 @@ instance
 
     goal : ComputationResult String
            (∃-syntax (_⊢_⇀⦇_,CERTBASE⦈_ ⟦ CertEnv.epoch ce , pp , votes , wdrls , _ ⟧ st sig))
-    goal = case ¿ mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) ⊆ rewards ˢ ¿ of λ where
-      (yes p) → success (-, CERT-base (p {_}))
-      (no ¬p) → failure (genErrors ¬p)
-  Computational-CERTBASE .completeness ce st _ st' (CERT-base p) with
-    ¿ mapˢ (map₁ RwdAddr.stake) (CertEnv.wdrls ce ˢ) ⊆ (st .CertState.dState .DState.rewards) ˢ ¿
-  ... | yes _ = refl
-  ... | no ¬q = ⊥-elim (¬q p)
+    goal = success (-, CERT-base)
+  Computational-CERTBASE .completeness ce st _ st' CERT-base = refl
 
 Computational-CERTS : Computational _⊢_⇀⦇_,CERTS⦈_ String
 Computational-CERTS = it

src/Ledger/Conway/Conformance/Equivalence/Certs.agda

@@ -153,7 +153,7 @@ instance
                  → L.Deposits × L.Deposits
                    ⊢ Γ L.⊢ s ⇀⦇ _ ,CERTBASE⦈ s' ⭆ⁱ λ deposits _ →
                      Γ C.⊢ (deposits ⊢conv s) ⇀⦇ _ ,CERTBASE⦈ (deposits ⊢conv s')
-  CERTBASEToConf .convⁱ deposits (L.CERT-base h) = C.CERT-base h
+  CERTBASEToConf .convⁱ deposits L.CERT-base = C.CERT-base
 
   DELEGToConf : ∀ {Γ s dcert dcerts s'}
                   (open L.DelegEnv Γ renaming (pparams to pp))
@@ -235,7 +235,7 @@ instance
   CERTBASEFromConf : ∀ {Γ s s'}
                    → Γ C.⊢ s ⇀⦇ _ ,CERTBASE⦈ s' ⭆
                      Γ L.⊢ (conv s) ⇀⦇ _ ,CERTBASE⦈ (conv s')
-  CERTBASEFromConf .convⁱ _ (C.CERT-base h) = L.CERT-base h
+  CERTBASEFromConf .convⁱ _ C.CERT-base = L.CERT-base
 
   CERTS'FromConf : ∀ {Γ s dcerts s'}
                  → ReflexiveTransitiveClosure {sts = C._⊢_⇀⦇_,CERT⦈_} Γ s dcerts s' ⭆

src/Ledger/Conway/Conformance/Ledger.agda

@@ -39,7 +39,7 @@ private variable
   s s' s'' : LState
   utxoSt' : UTxOState
   govSt' : GovState
-  certState' : CertState
+  certState' certState'' : CertState
   tx : Tx
 
 open UTxOState
@@ -52,18 +52,23 @@ data
 
   LEDGER-V :
     let open LState s; txb = tx .body; open TxBody txb; open LEnv Γ
-        open CertState certState; open DState dState
         utxoSt'' = record utxoSt' { deposits = updateDeposits pparams txb (deposits utxoSt') }
         wdrlCreds   = mapˢ RwdAddr.stake (dom txwdrls)
+        voteDelegs = certState .CertState.dState .DState.voteDelegs
+        rewards = certState .CertState.dState .DState.rewards
+        rewards' = constMap wdrlCreds 0 ∪ˡ rewards
+        dState = certState .CertState.dState
+        dState' = record dState { rewards = rewards' }
+        certState' = record certState { dState = dState' }
      in
     ∙  isValid tx ≡ true
     ∙  record { LEnv Γ } ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'
-    ∙  ⟦ epoch slot , pparams , txvote , txwdrls , allColdCreds govSt enactState ⟧ ⊢ certState ⇀⦇ txcerts ,CERTS⦈ certState'
+    ∙  ⟦ epoch slot , pparams , txvote , txwdrls , allColdCreds govSt enactState ⟧ ⊢ certState' ⇀⦇ txcerts ,CERTS⦈ certState''
     ∙  filterˢ isKeyHash wdrlCreds ⊆ dom voteDelegs
-    ∙  ⟦ txid , epoch slot , pparams , ppolicy , enactState ,  certState' , dom
-    rewards ⟧ ⊢ govSt ⇀⦇ txgov txb ,GOVS⦈ govSt'
+    ∙  ⟦ txid , epoch slot , pparams , ppolicy , enactState ,  certState'' , dom rewards ⟧ ⊢ govSt ⇀⦇ txgov txb ,GOVS⦈ govSt'
+    ∙  wdrlCreds ⊆ dom rewards
        ────────────────────────────────
-       Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ ⟦ utxoSt'' , govSt' , certState' ⟧
+       Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ ⟦ utxoSt'' , govSt' , certState'' ⟧
 
 
   LEDGER-I : let open LState s; txb = tx .body; open TxBody txb; open LEnv Γ in
@@ -72,8 +77,8 @@ data
        ────────────────────────────────
        Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ ⟦ utxoSt' , govSt , certState ⟧
 
-pattern LEDGER-V⋯ w x y z t = LEDGER-V (w , x , y , z , t)
-pattern LEDGER-I⋯ y z       = LEDGER-I (y , z)
+pattern LEDGER-V⋯ w x y z t u = LEDGER-V (w , x , y , z , t , u)
+pattern LEDGER-I⋯ y z         = LEDGER-I (y , z)
 
 _⊢_⇀⦇_,LEDGERS⦈_ : LEnv → LState → List Tx → LState → Type
 _⊢_⇀⦇_,LEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,LEDGER⦈_}

src/Ledger/Conway/Conformance/Ledger/Properties.agda

@@ -76,30 +76,46 @@ instance
       computeProof = case isValid ≟ true of λ where
         (yes p) → do
           (utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx
-          (certSt' , certStep) ← computeCerts certΓ certState txcerts
-          let wdrlCreds = mapˢ RwdAddr.stake (dom txwdrls)
-          wdrlsCheck ← case ¿ filterˢ isKeyHash wdrlCreds ⊆ dom (certState .CertState.dState .DState.voteDelegs) ¿ of λ where
+          let rewards = certState .CertState.dState .DState.rewards
+              wdrlCreds   = mapˢ RwdAddr.stake (dom txwdrls)
+              rewards' = constMap wdrlCreds 0 ∪ˡ rewards
+              dState = certState .CertState.dState
+              dState' = record dState { rewards = rewards' }
+              certState' = record certState { dState = dState' }
+          (certState'' , certStep) ← computeCerts certΓ certState' txcerts
+          wdrlsCheck ← case ¿ filterˢ isKeyHash wdrlCreds ⊆ dom (certState' .CertState.dState .DState.voteDelegs) ¿ of λ where
             (yes q) → success q
             (no ¬q) → failure (genErrors ¬q)
-          (govSt'  , govStep)  ← computeGov (govΓ certSt') (rmOrphanDRepVotes (conv certSt') govSt) (txgov txb)
-          success (_ , LEDGER-V⋯ p utxoStep certStep wdrlsCheck govStep)
+          (govSt'  , govStep)  ← computeGov (govΓ certState'') (rmOrphanDRepVotes (conv certState'') govSt) (txgov txb)
+          rwdsCheck ← case ¿ wdrlCreds ⊆ dom rewards ¿ of λ where
+            (yes q) → success q
+            (no ¬q) → failure (genErrors ¬q)
+          success (_ , LEDGER-V⋯ p utxoStep certStep wdrlsCheck govStep λ { x → rwdsCheck x })
         (no ¬p) → do
           (utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx
           success (_ , LEDGER-I⋯ (¬-not ¬p) utxoStep)
 
       completeness : ∀ s' → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' → (proj₁ <$> computeProof) ≡ success s'
-      completeness  ls' (LEDGER-V⋯ v utxoStep certStep u govStep)
+      completeness  ls' (LEDGER-V⋯ v utxoStep certStep u govStep t)
         with isValid ≟ true
       ... | no ¬v = contradiction v ¬v
       ... | yes refl
         with computeUtxow utxoΓ utxoSt tx | complete _ _ _ _ utxoStep
       ... | success (utxoSt' , _) | refl
-        with computeCerts certΓ certState txcerts | complete _ _ _ _ certStep
-      ... | success (certSt' , _) | refl
+        using rewards ← certState .CertState.dState .DState.rewards
+        using wdrlCreds ← mapˢ RwdAddr.stake (dom txwdrls)
+        using rewards' ← constMap wdrlCreds 0 ∪ˡ rewards
+        using dState ← certState .CertState.dState
+        using dState' ← record dState { rewards = rewards' }
+        using certState' ← record certState { dState = dState' }
+        with computeCerts certΓ certState' txcerts | complete _ _ _ _ certStep
+      ... | success (certState'' , _) | refl
         with dec-yes ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom txwdrls)) ⊆ dom (certState .CertState.dState .DState.voteDelegs) ¿ (λ { x → u x })
       ... | (_ , p)
-        with computeGov (govΓ certSt') (rmOrphanDRepVotes (conv certSt') govSt ) (txgov txb) | complete {STS = _⊢_⇀⦇_,GOVS⦈_} (govΓ certSt') _ _ _ govStep
-      ... | success (govSt' , _) | refl rewrite p = refl
+        with computeGov (govΓ certState'') (rmOrphanDRepVotes (conv certState'') govSt ) (txgov txb) | complete {STS = _⊢_⇀⦇_,GOVS⦈_} (govΓ certState'') _ _ _ govStep
+      ... | success (govSt' , _) | refl 
+        with dec-yes ¿ (mapˢ RwdAddr.stake (dom txwdrls)) ⊆ dom (certState .CertState.dState .DState.rewards) ¿ (λ {x → t x}) 
+      ... | (_ , q) rewrite p rewrite q = refl
       completeness ls' (LEDGER-I⋯ i utxoStep)
         with isValid ≟ true
       ... | yes refl = case i of λ ()

src/Ledger/Ledger.lagda

@@ -89,7 +89,7 @@ private variable
   s s' s'' : LState
   utxoSt utxoSt' : UTxOState
   govSt govSt' : GovState
-  certState certState' : CertState
+  certState certState' certState'' : CertState
   tx : Tx
   slot : Slot
   ppolicy : Maybe ScriptHash
@@ -110,13 +110,18 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LEnv → LState → Tx → LState → Type where
          open TxBody txb
 \end{code}
 \begin{code}
-         rewards     = certState .dState .rewards
+         rewards     = certState' .dState .rewards
          wdrlCreds   = mapˢ RwdAddr.stake (dom txwdrls)
+         rewards' = constMap wdrlCreds 0 ∪ˡ rewards
+         dState = certState .CertState.dState
+         dState' = record dState { rewards = rewards' }
+         certState' = record certState { dState = dState' }
+         voteDelegs = certState' .CertState.dState .voteDelegs
     in
     ∙ isValid tx ≡ true
     ∙ ⟦ slot , pp , treasury ⟧  ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'
-    ∙ ⟦ epoch slot , pp , txvote , txwdrls , allColdCreds govSt enactState ⟧ ⊢ certState ⇀⦇ txcerts ,CERTS⦈ certState'
-    ∙ filterˢ isKeyHash wdrlCreds ⊆ dom (certState .dState .voteDelegs)
+    ∙ ⟦ epoch slot , pp , txvote , txwdrls , allColdCreds govSt enactState ⟧ ⊢ certState' ⇀⦇ txcerts ,CERTS⦈ certState''
+    ∙ filterˢ isKeyHash wdrlCreds ⊆ dom voteDelegs
     ∙ ⟦ txid , epoch slot , pp , ppolicy , enactState , certState' , dom rewards ⟧ ⊢ rmOrphanDRepVotes certState' govSt ⇀⦇ txgov txb ,GOVS⦈ govSt'
       ────────────────────────────────
       ⟦ slot , ppolicy , pp , enactState , treasury ⟧ ⊢ ⟦ utxoSt , govSt , certState ⟧ ⇀⦇ tx ,LEDGER⦈ ⟦ utxoSt' , govSt' , certState' ⟧