Add additional check for ccreghot (#506)

* Add additional check for `ccreghot`

---------

Co-authored-by: William DeMeo <williamdemeo@gmail.com>

Author: WhatisRT

CHANGELOG.md

@@ -36,6 +36,9 @@
 - Check `proposal ≡ nothing` if action not `ChangePParams` or `TreasuryWdrl`
 - Implement proper vote counting for SPOs
 - Check a DRep exists before delegating to it.
+- Prevent older Plutus versions in transaction with Conway features
+- Allow reference scripts and inputs to be used with Plutus V1
+- Add sanity checks for delegating hot credentials
 
 ### V0.9
 

src/Ledger/Certs.lagda

@@ -57,10 +57,10 @@ data DCert : Type where
   ccreghot    : Credential → Maybe Credential → DCert
 \end{code}
 \begin{code}[hide]
-  -- The `reg` cert is deprecated in Conway, but it's still present in this era 
-  -- for backwards compatibility. This has been added to the spec to make 
+  -- The `reg` cert is deprecated in Conway, but it's still present in this era
+  -- for backwards compatibility. This has been added to the spec to make
   -- conformance testing work properly. We don't talk about this certificate
-  -- in the pdf because it has been deprecated and we want to discourage people 
+  -- in the pdf because it has been deprecated and we want to discourage people
   -- from using it.
   reg         : Credential → Coin → DCert
 \end{code}
@@ -76,10 +76,10 @@ cwitness (deregdrep c _)     = just c
 cwitness (ccreghot c _)      = just c
 \end{code}
 \begin{code}[hide]
--- The implementation requires the `reg` cert to be witnessed only if the 
--- deposit is set. There didn't use to be a field for the deposit, but that was 
--- added in the Conway era to make it easier to determine, just by looking at 
--- the transaction, how much deposit was paid for that certificate. 
+-- The implementation requires the `reg` cert to be witnessed only if the
+-- deposit is set. There didn't use to be a field for the deposit, but that was
+-- added in the Conway era to make it easier to determine, just by looking at
+-- the transaction, how much deposit was paid for that certificate.
 cwitness (reg _ zero)        = nothing
 cwitness (reg c (suc _))     = just c
 \end{code}
@@ -94,14 +94,15 @@ cwitness (reg c (suc _))     = just c
 record CertEnv : Type where
 \end{code}
 \begin{code}[hide]
-  constructor ⟦_,_,_,_⟧ᶜ
+  constructor ⟦_,_,_,_,_⟧ᶜ
   field
 \end{code}
 \begin{code}
     epoch     : Epoch
     pp        : PParams
     votes     : List GovVote
     wdrls     : RwdAddr ⇀ Coin
+    coldCreds : ℙ Credential
 
 record DState : Type where
 \end{code}
@@ -207,6 +208,7 @@ private variable
   stᵈ stᵈ' : DState
   stᵍ stᵍ' : GState
   stᵖ stᵖ' : PState
+  cc : ℙ Credential
 \end{code}
 
 \subsection{Removal of Pointer Addresses, Genesis Delegations and MIR Certificates}
@@ -270,10 +272,9 @@ constitutional committee.
     hot credential is more conveniently accessed.  If the hot credential
     is compromised, it can be changed using the cold credential.}
   We check that the cold key did not previously
-  resign from the committee. Note that we intentionally do not check
-  if the cold key is actually part of the committee; if it isn't, then
-  the corresponding hot key does not carry any voting power. By allowing
-  this, a newly elected member of the constitutional committee can
+  resign from the committee. We allow this delegation for any cold
+  credential that is either part of \EnactState or is is a proposal.
+  This allows a newly elected member of the constitutional committee to
   immediately delegate their vote to a hot key and use it to vote. Since
   votes are counted after previous actions have been enacted, this allows
   constitutional committee members to act without a delay of one epoch.
@@ -389,18 +390,19 @@ data _⊢_⇀⦇_,GOVCERT⦈_ where
   GOVCERT-regdrep : ∀ {pp} → let open PParams pp in
     ∙ (d ≡ drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps)
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls ⟧ᶜ ⊢  ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ regdrep c d an ,GOVCERT⦈
+      ⟦ e , pp , vs , wdrls , cc ⟧ᶜ ⊢  ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ regdrep c d an ,GOVCERT⦈
                                   ⟦ ❴ c , e + drepActivity ❵ ∪ˡ dReps , ccKeys ⟧ᵛ
 
   GOVCERT-deregdrep :
     ∙ c ∈ dom dReps
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls ⟧ᶜ ⊢ ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ deregdrep c d ,GOVCERT⦈ ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys ⟧ᵛ
+      ⟦ e , pp , vs , wdrls , cc ⟧ᶜ ⊢ ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ deregdrep c d ,GOVCERT⦈ ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys ⟧ᵛ
 
   GOVCERT-ccreghot :
     ∙ (c , nothing) ∉ ccKeys
+    ∙ c ∈ cc
       ────────────────────────────────
-      Γ ⊢ ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ ccreghot c mc ,GOVCERT⦈ ⟦ dReps , ❴ c , mc ❵ ∪ˡ ccKeys ⟧ᵛ
+      ⟦ e , pp , vs , wdrls , cc ⟧ᶜ ⊢ ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ ccreghot c mc ,GOVCERT⦈ ⟦ dReps , ❴ c , mc ❵ ∪ˡ ccKeys ⟧ᵛ
 \end{code}
 \end{AgdaSuppressSpace}
 \caption{Auxiliary GOVCERT transition system}
@@ -430,12 +432,12 @@ data _⊢_⇀⦇_,CERT⦈_ where
   CERT-deleg :
     ∙ ⟦ pp , PState.pools stᵖ , dom (GState.dreps stᵍ) ⟧ᵈᵉ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls ⟧ᶜ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ' , stᵖ , stᵍ ⟧ᶜˢ
+      ⟦ e , pp , vs , wdrls , cc ⟧ᶜ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ' , stᵖ , stᵍ ⟧ᶜˢ
 
   CERT-pool :
     ∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls ⟧ᶜ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ' , stᵍ ⟧ᶜˢ
+      ⟦ e , pp , vs , wdrls , cc ⟧ᶜ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ' , stᵍ ⟧ᶜˢ
 
   CERT-vdel :
     ∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
@@ -460,7 +462,7 @@ data _⊢_⇀⦇_,CERTBASE⦈_ where
     ∙ filter isKeyHash wdrlCreds ⊆ dom voteDelegs
     ∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls ⟧ᶜ ⊢
+      ⟦ e , pp , vs , wdrls , cc ⟧ᶜ ⊢
         ⟦ ⟦ voteDelegs , stakeDelegs , rewards ⟧ᵈ
         , stᵖ
         , ⟦ dReps , ccHotKeys ⟧ᵛ

src/Ledger/Certs/Properties.agda

@@ -43,12 +43,11 @@ instance
     _ → failure "Unexpected certificate in DELEG"
   Computational-DELEG .completeness ⟦ pp , pools , delegatees ⟧ᵈᵉ ⟦ _ , _ , rwds ⟧ᵈ (delegate c mv mc d)
     s' (DELEG-delegate p) rewrite dec-yes (¿ (c ∉ dom rwds → d ≡ pp .PParams.keyDeposit)
-                                           × (c ∈ dom rwds → d ≡ 0)
-                                           × mv ∈ mapˢ (just ∘ credVoter DRep) delegatees ∪
-                                               fromList ( nothing ∷ just abstainRep ∷ just noConfidenceRep ∷ [] )
-                                           × mc ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵
+                                × (c ∈ dom rwds → d ≡ 0)
+                                × mv ∈ mapˢ (just ∘ credVoter DRep) delegatees ∪ fromList ( nothing ∷ just abstainRep ∷ just noConfidenceRep ∷ [] )
+                                × mc ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵
                                            ¿) p .proj₂ = refl
-  Computational-DELEG .completeness ⟦ _ , _ , _ ⟧ᵈᵉ ⟦ _ , _ , rwds ⟧ᵈ (dereg c d) _ (DELEG-dereg p)
+  Computational-DELEG .completeness ⟦ _ , _ , deps ⟧ᵈᵉ ⟦ _ , _ , rwds ⟧ᵈ (dereg c d) _ (DELEG-dereg p)
     rewrite dec-yes (¿ (c , 0) ∈ rwds ¿) p .proj₂ = refl
   Computational-DELEG .completeness ⟦ pp , _ , _ ⟧ᵈᵉ ⟦ _ , _ , rwds ⟧ᵈ (reg c d) _ (DELEG-reg p)
     rewrite dec-yes (¿ c ∉ dom rwds × (d ≡ pp .PParams.keyDeposit ⊎ d ≡ 0) ¿) p .proj₂ = refl
@@ -65,60 +64,60 @@ instance
   Computational-POOL .completeness _ _ (retirepool _ _) _ POOL-retirepool = refl
 
   Computational-GOVCERT : Computational _⊢_⇀⦇_,GOVCERT⦈_ String
-  Computational-GOVCERT .computeProof ⟦ _ , pp , _ , _ ⟧ᶜ ⟦ dReps , _ ⟧ᵛ (regdrep c d _) =
+  Computational-GOVCERT .computeProof ⟦ _ , pp , _ , _ , _ ⟧ᶜ ⟦ dReps , _ ⟧ᵛ (regdrep c d _) =
     let open PParams pp in
     case ¿ (d ≡ drepDeposit × c ∉ dom dReps)
          ⊎ (d ≡ 0 × c ∈ dom dReps) ¿ of λ where
       (yes p) → success (-, GOVCERT-regdrep p)
       (no ¬p) → failure (genErrors ¬p)
-  Computational-GOVCERT .computeProof ⟦ _ , _ , _ , _ ⟧ᶜ ⟦ dReps , _ ⟧ᵛ (deregdrep c d) =
-    case ¿ c ∈ dom dReps ¿ of λ where
+  Computational-GOVCERT .computeProof _ ⟦ dReps , _ ⟧ᵛ (deregdrep c _) =
+    case c ∈? dom dReps of λ where
       (yes p) → success (-, GOVCERT-deregdrep p)
       (no ¬p)  → failure (genErrors ¬p)
-  Computational-GOVCERT .computeProof _ ⟦ _ , ccKeys ⟧ᵛ (ccreghot c _) =
-    case ¬? ((c , nothing) ∈? (ccKeys ˢ)) of λ where
+  Computational-GOVCERT .computeProof ⟦ _ , _ , _ , _ , cc ⟧ᶜ ⟦ _ , ccKeys ⟧ᵛ (ccreghot c _) =
+    case ¿ ((c , nothing) ∉ ccKeys ˢ) × c ∈ cc ¿ of λ where
       (yes p) → success (-, GOVCERT-ccreghot p)
       (no ¬p) → failure (genErrors ¬p)
   Computational-GOVCERT .computeProof _ _ _ = failure "Unexpected certificate in GOVCERT"
-  Computational-GOVCERT .completeness ⟦ _ , pp , _ , _ ⟧ᶜ ⟦ dReps , _ ⟧ᵛ
+  Computational-GOVCERT .completeness ⟦ _ , pp , _ , _ , _ ⟧ᶜ ⟦ dReps , _ ⟧ᵛ
     (regdrep c d _) _ (GOVCERT-regdrep p)
     rewrite dec-yes
       ¿ (let open PParams pp in
         (d ≡ drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps))
       ¿ p .proj₂ = refl
-  Computational-GOVCERT .completeness ⟦ _ , _ , _ , _ ⟧ᶜ ⟦ dReps , _ ⟧ᵛ
-    (deregdrep c d) _ (GOVCERT-deregdrep p)
-    rewrite dec-yes (¿ c ∈ dom dReps ¿) p .proj₂ = refl
-  Computational-GOVCERT .completeness _ ⟦ _ , ccKeys ⟧ᵛ
-    (ccreghot c _) _ (GOVCERT-ccreghot ¬p)
-    rewrite dec-no ((c , nothing) ∈? (ccKeys ˢ)) ¬p = refl
+  Computational-GOVCERT .completeness _ ⟦ dReps , _ ⟧ᵛ
+    (deregdrep c _) _ (GOVCERT-deregdrep p)
+    rewrite dec-yes (c ∈? dom dReps) p .proj₂ = refl
+  Computational-GOVCERT .completeness ⟦ _ , _ , _ , _ , cc ⟧ᶜ ⟦ _ , ccKeys ⟧ᵛ
+    (ccreghot c _) _ (GOVCERT-ccreghot p)
+    rewrite dec-yes (¿ (((c , nothing) ∉ ccKeys ˢ) × c ∈ cc) ¿) p .proj₂ = refl
 
   Computational-CERT : Computational _⊢_⇀⦇_,CERT⦈_ String
-  Computational-CERT .computeProof Γ@(⟦ e , pp , vs , _ ⟧ᶜ) ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ dCert
+  Computational-CERT .computeProof Γ@(⟦ e , pp , vs , _ , _ ⟧ᶜ) ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ dCert
     with computeProof ⟦ pp , PState.pools stᵖ , dom (GState.dreps stᵍ) ⟧ᵈᵉ stᵈ dCert
        | computeProof pp stᵖ dCert | computeProof Γ stᵍ dCert
   ... | success (_ , h) | _               | _               = success (-, CERT-deleg h)
   ... | failure _       | success (_ , h) | _               = success (-, CERT-pool h)
   ... | failure _       | failure _       | success (_ , h) = success (-, CERT-vdel h)
   ... | failure e₁      | failure e₂      | failure e₃      = failure $
     "DELEG: " <> e₁ <> "\nPOOL: " <> e₂ <> "\nVDEL: " <> e₃
-  Computational-CERT .completeness ⟦ _ , pp , _ , wdrls ⟧ᶜ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ
+  Computational-CERT .completeness ⟦ _ , pp , _ , wdrls , _ ⟧ᶜ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ
     dCert@(delegate c mv mc d) ⟦ stᵈ' , stᵖ , stᵍ ⟧ᶜˢ (CERT-deleg h)
     with computeProof ⟦ pp , PState.pools stᵖ , dom (GState.dreps stᵍ) ⟧ᵈᵉ stᵈ dCert | completeness _ _ _ _ h
   ... | success _ | refl = refl
-  Computational-CERT .completeness ⟦ _ , pp , _ , wdrls ⟧ᶜ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ
+  Computational-CERT .completeness ⟦ _ , pp , _ , wdrls , _ ⟧ᶜ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ
     dCert@(reg c d) ⟦ stᵈ' , stᵖ , stᵍ ⟧ᶜˢ (CERT-deleg h)
     with computeProof ⟦ pp , PState.pools stᵖ , dom (GState.dreps stᵍ) ⟧ᵈᵉ stᵈ dCert | completeness _ _ _ _ h
   ... | success _ | refl = refl
-  Computational-CERT .completeness ⟦ _ , pp , _ , wdrls ⟧ᶜ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ
+  Computational-CERT .completeness ⟦ _ , pp , _ , wdrls , _ ⟧ᶜ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ
     dCert@(dereg c _) ⟦ stᵈ' , stᵖ , stᵍ ⟧ᶜˢ (CERT-deleg h)
     with computeProof ⟦ pp , PState.pools stᵖ , dom (GState.dreps stᵍ) ⟧ᵈᵉ stᵈ dCert | completeness _ _ _ _ h
   ... | success _ | refl = refl
-  Computational-CERT .completeness ⟦ _ , pp , _ , _ ⟧ᶜ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ
+  Computational-CERT .completeness ⟦ _ , pp , _ , _ , _ ⟧ᶜ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ
     dCert@(regpool c poolParams) ⟦ stᵈ , stᵖ' , stᵍ ⟧ᶜˢ (CERT-pool h)
     with computeProof pp stᵖ dCert | completeness _ _ _ _ h
   ... | success _ | refl = refl
-  Computational-CERT .completeness ⟦ _ , pp , _ , _ ⟧ᶜ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ
+  Computational-CERT .completeness ⟦ _ , pp , _ , _ , _ ⟧ᶜ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ
     dCert@(retirepool c e) ⟦ stᵈ , stᵖ' , stᵍ ⟧ᶜˢ (CERT-pool h)
     with completeness _ _ _ _ h
   ... | refl = refl
@@ -137,15 +136,15 @@ instance
   ... | success _ | refl = refl
 
   Computational-CERTBASE : Computational _⊢_⇀⦇_,CERTBASE⦈_ String
-  Computational-CERTBASE .computeProof  ⟦ e , pp , vs , wdrls ⟧ᶜ st _ =
+  Computational-CERTBASE .computeProof ⟦ e , pp , vs , wdrls , _ ⟧ᶜ st _ =
     let open PParams pp; open CertState st; open GState gState; open DState dState
         refresh = mapPartial getDRepVote (fromList vs)
         refreshedDReps  = mapValueRestricted (const (e + drepActivity)) dreps refresh
     in case ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs
               × mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) ⊆ rewards ˢ ¿ of λ where
       (yes p) → success (-, CERT-base p)
       (no ¬p) → failure (genErrors ¬p)
-  Computational-CERTBASE .completeness ⟦ e , pp , vs , wdrls ⟧ᶜ st _ st' (CERT-base p)
+  Computational-CERTBASE .completeness ⟦ e , pp , vs , wdrls , _ ⟧ᶜ st _ st' (CERT-base p)
     rewrite let dState = CertState.dState st; open DState dState in
       dec-yes ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs
                 × mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) ⊆ rewards ˢ ¿

src/Ledger/Conway/Conformance/Certs.agda

@@ -80,7 +80,7 @@ private variable
   d              : Coin
   c              : Credential
   mc             : Maybe Credential
-  delegatees     : ℙ Credential
+  delegatees cc  : ℙ Credential
   dCert          : DCert
   dep ddep gdep  : Deposits
   e              : Epoch
@@ -151,7 +151,7 @@ data _⊢_⇀⦇_,GOVCERT⦈_ : GovCertEnv → GState → DCert → GState → T
   GOVCERT-regdrep : ∀ {pp} → let open PParams pp in
     ∙ (d ≡ drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps)
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls ⟧ᶜ ⊢
+      ⟦ e , pp , vs , wdrls , cc ⟧ᶜ ⊢
       ⟦ dReps , ccKeys , dep ⟧ᵛ
         ⇀⦇ regdrep c d an ,GOVCERT⦈
       ⟦ ❴ c , e + drepActivity ❵ ∪ˡ dReps , ccKeys
@@ -161,27 +161,28 @@ data _⊢_⇀⦇_,GOVCERT⦈_ : GovCertEnv → GState → DCert → GState → T
     ∙ c ∈ dom dReps
     ∙ (DRepDeposit c , d) ∈ dep
       ────────────────────────────────
-      Γ ⊢ ⟦ dReps , ccKeys , dep ⟧ᵛ
+      ⟦ e , pp , vs , wdrls , cc ⟧ᶜ ⊢ ⟦ dReps , ccKeys , dep ⟧ᵛ
           ⇀⦇ deregdrep c d ,GOVCERT⦈
-          ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys , updateCertDeposit (CertEnv.pp Γ) (deregdrep c d) dep ⟧ᵛ
+          ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys , updateCertDeposit pp (deregdrep c d) dep ⟧ᵛ
 
   GOVCERT-ccreghot :
     ∙ (c , nothing) ∉ ccKeys
+    ∙ c ∈ cc
       ────────────────────────────────
-      Γ ⊢ ⟦ dReps , ccKeys , dep ⟧ᵛ
+      ⟦ e , pp , vs , wdrls , cc ⟧ᶜ ⊢ ⟦ dReps , ccKeys , dep ⟧ᵛ
           ⇀⦇ ccreghot c mc ,GOVCERT⦈
-          ⟦ dReps , ❴ c , mc ❵ ∪ˡ ccKeys , updateCertDeposit (CertEnv.pp Γ) (ccreghot c mc) dep ⟧ᵛ
+          ⟦ dReps , ❴ c , mc ❵ ∪ˡ ccKeys , updateCertDeposit pp (ccreghot c mc) dep ⟧ᵛ
 
 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 ⟧ᶜ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ' , stᵖ , stᵍ ⟧ᶜˢ
+      ⟦ e , pp , vs , wdrls , cc ⟧ᶜ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ' , stᵖ , stᵍ ⟧ᶜˢ
 
   CERT-pool :
     ∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls ⟧ᶜ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ' , stᵍ ⟧ᶜˢ
+      ⟦ e , pp , vs , wdrls , cc ⟧ᶜ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ' , stᵍ ⟧ᶜˢ
 
   CERT-vdel :
     ∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
@@ -199,7 +200,7 @@ data _⊢_⇀⦇_,CERTBASE⦈_ : CertEnv → CertState → ⊤ → CertState →
     ∙ filterˢ isKeyHash wdrlCreds ⊆ dom voteDelegs
     ∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls ⟧ᶜ ⊢
+      ⟦ e , pp , vs , wdrls , cc ⟧ᶜ ⊢
       ⟦ ⟦ voteDelegs , stakeDelegs , rewards , ddep ⟧ᵈ
       , stᵖ
       , ⟦ dReps , ccHotKeys , gdep ⟧ᵛ