Add additional check for ccreghot

CHANGELOG.md

@@ -20,6 +20,9 @@
 - Add `curTreasury` field to transactions
 - Compute the voting stake distribution
 - Add deposit amount to `dereg` certificate
+- 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

@@ -78,7 +78,7 @@ cwitness (ccreghot c _)      = c
 record CertEnv : Type where
 \end{code}
 \begin{code}[hide]
-  constructor ⟦_,_,_,_,_⟧ᶜ
+  constructor ⟦_,_,_,_,_,_⟧ᶜ
   field
 \end{code}
 \begin{code}
@@ -87,6 +87,7 @@ record CertEnv : Type where
     votes     : List GovVote
     wdrls     : RwdAddr ⇀ Coin
     deposits  : Deposits
+    coldCreds : ℙ Credential
 
 record DState : Type where
 \end{code}
@@ -188,6 +189,7 @@ private variable
   stakeDelegs : Credential ⇀ KeyHash
   rewards : Credential ⇀ Coin
   deps : Deposits
+  cc : ℙ Credential
 \end{code}
 
 \subsection{Removal of Pointer Addresses, Genesis Delegations and MIR Certificates}
@@ -239,10 +241,9 @@ constitutional committee.
 \item \GOVCERTderegdrep deregisters a DRep.
 \item \GOVCERTccreghot registers a hot credential for constitutional
   committee members. 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.
@@ -352,7 +353,7 @@ data _⊢_⇀⦇_,GOVCERT⦈_ where
   GOVCERT-regdrep : let open PParams pp in
     ∙ (d ≡ drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps)
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , deps ⟧ᶜ ⊢  ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ regdrep c d an ,GOVCERT⦈
+      ⟦ e , pp , vs , wdrls , deps , cc ⟧ᶜ ⊢  ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ regdrep c d an ,GOVCERT⦈
                                   ⟦ ❴ c , e + drepActivity ❵ ∪ˡ dReps , ccKeys ⟧ᵛ
 
   GOVCERT-deregdrep :
@@ -362,8 +363,9 @@ data _⊢_⇀⦇_,GOVCERT⦈_ where
 
   GOVCERT-ccreghot :
     ∙ (c , nothing) ∉ ccKeys
+    ∙ c ∈ cc
       ────────────────────────────────
-      Γ ⊢ ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ ccreghot c mc ,GOVCERT⦈ ⟦ dReps , ❴ c , mc ❵ ∪ˡ ccKeys ⟧ᵛ
+      ⟦ e , pp , vs , wdrls , deps , cc ⟧ᶜ ⊢ ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ ccreghot c mc ,GOVCERT⦈ ⟦ dReps , ❴ c , mc ❵ ∪ˡ ccKeys ⟧ᵛ
 \end{code}
 \end{AgdaSuppressSpace}
 \caption{Auxiliary GOVCERT transition system}
@@ -393,12 +395,12 @@ data _⊢_⇀⦇_,CERT⦈_ where
   CERT-deleg :
     ∙ ⟦ pp , PState.pools stᵖ , deps ⟧ᵈᵉ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , deps ⟧ᶜ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ' , stᵖ , stᵍ ⟧ᶜˢ
+      ⟦ e , pp , vs , wdrls , deps , cc ⟧ᶜ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ' , stᵖ , stᵍ ⟧ᶜˢ
 
   CERT-pool :
     ∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , deps ⟧ᶜ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ' , stᵍ ⟧ᶜˢ
+      ⟦ e , pp , vs , wdrls , deps , cc ⟧ᶜ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ' , stᵍ ⟧ᶜˢ
 
   CERT-vdel :
     ∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
@@ -421,7 +423,7 @@ data _⊢_⇀⦇_,CERTBASE⦈_ where
     ∙ wdrlCreds ⊆ dom voteDelegs
     ∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , deps ⟧ᶜ ⊢ ⟦
+      ⟦ e , pp , vs , wdrls , deps , cc ⟧ᶜ ⊢ ⟦
         ⟦ voteDelegs , stakeDelegs , rewards ⟧ᵈ , stᵖ , ⟦ dreps , ccHotKeys ⟧ᵛ ⟧ᶜˢ ⇀⦇ _ ,CERTBASE⦈ ⟦
         ⟦ voteDelegs , stakeDelegs , constMap wdrlCreds 0 ∪ˡ rewards ⟧ᵈ
         , stᵖ

src/Ledger/Certs/Properties.agda

@@ -48,7 +48,7 @@ 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
@@ -58,12 +58,12 @@ instance
     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
@@ -72,32 +72,32 @@ instance
   Computational-GOVCERT .completeness _ ⟦ dReps , _ ⟧ᵛ
     (deregdrep c) _ (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 ⟦ _ , _ , _ , _ , _ , 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 , _ , deps ⟧ᶜ) ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ dCert
+  Computational-CERT .computeProof Γ@(⟦ e , pp , vs , _ , deps , _ ⟧ᶜ) ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ dCert
     with computeProof ⟦ pp , PState.pools stᵖ , deps ⟧ᵈᵉ 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 , deps ⟧ᶜ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ
+  Computational-CERT .completeness ⟦ _ , pp , _ , wdrls , deps , _ ⟧ᶜ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ
     dCert@(delegate c mv mc d) ⟦ stᵈ' , stᵖ , stᵍ ⟧ᶜˢ (CERT-deleg h)
     with computeProof ⟦ pp , PState.pools stᵖ , deps ⟧ᵈᵉ stᵈ dCert | completeness _ _ _ _ h
   ... | success _ | refl = refl
-  Computational-CERT .completeness ⟦ _ , pp , _ , wdrls , deps ⟧ᶜ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ
+  Computational-CERT .completeness ⟦ _ , pp , _ , wdrls , deps , _ ⟧ᶜ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ
     dCert@(dereg c _) ⟦ stᵈ' , stᵖ , stᵍ ⟧ᶜˢ (CERT-deleg h)
     with computeProof ⟦ pp , PState.pools stᵖ , deps ⟧ᵈᵉ 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
@@ -116,14 +116,14 @@ 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)
         wdrlCreds = mapˢ RwdAddr.stake (dom wdrls)
     in case ¿ wdrlCreds ⊆ 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 ¿ mapˢ RwdAddr.stake (dom wdrls) ⊆ dom voteDelegs × mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) ⊆ rewards ˢ ¿
         p .proj₂ = refl

src/Ledger/Enact.lagda

@@ -55,6 +55,11 @@ record EnactState : Type where
     pv            : HashProtected ProtVer
     pparams       : HashProtected PParams
     withdrawals   : RwdAddr ⇀ Coin
+\end{code}
+\begin{code}[hide]
+open EnactState
+\end{code}
+\begin{code}
 
 ccCreds : HashProtected (Maybe ((Credential ⇀ Epoch) × ℚ)) → ℙ Credential
 ccCreds (just x   , _)  = dom (x .proj₁)
@@ -69,8 +74,6 @@ getHash {ChangePParams _}        h = just h
 getHash {TreasuryWdrl _}         _ = nothing
 getHash {Info}                   _ = nothing
 
-open EnactState
-
 getHashES : EnactState → GovAction → Maybe GovActionID
 getHashES es NoConfidence             = just $ es .cc .proj₂
 getHashES es (UpdateCommittee _ _ _)  = just $ es .cc .proj₂

src/Ledger/Foreign/LedgerTypes.agda

@@ -580,18 +580,20 @@ data DepositPurpose : Type where
   data DepositPurpose (CredentialDeposit | PoolDeposit | DRepDeposit | GovActionDeposit) #-}
 
 record CertEnv : Type where
-  field epoch    : Epoch
-        pp       : PParams
-        votes    : List GovVote
-        wdrls    : HSMap RwdAddr Coin
-        deposits : HSMap DepositPurpose Coin
+  field epoch     : Epoch
+        pp        : PParams
+        votes     : List GovVote
+        wdrls     : HSMap RwdAddr Coin
+        deposits  : HSMap DepositPurpose Coin
+        coldCreds : List Credential
 {-# FOREIGN GHC
   data CertEnv = MkCertEnv
     { epoch      :: Epoch
     , pp         :: PParams
     , votes      :: [GovVote]
     , wdrls      :: HSMap RwdAddr Coin
     , ceDeposits :: HSMap DepositPurpose Coin
+    , coldCreds  :: [Credential]
     }
 #-}
 {-# COMPILE GHC CertEnv = data CertEnv (MkCertEnv) #-}

src/Ledger/GovernanceActions.lagda

@@ -233,6 +233,10 @@ instance
 getDRepVote : GovVote → Maybe Credential
 getDRepVote record { voter = (DRep , credential) }  = just credential
 getDRepVote _                                       = nothing
+
+proposedCC : GovAction → ℙ Credential
+proposedCC (UpdateCommittee x _ _) = dom x
+proposedCC _                       = ∅
 \end{code}
 \caption{Governance helper function}
 \end{figure*}

src/Ledger/Ledger.lagda

@@ -20,6 +20,8 @@ open import Ledger.Utxo txs abs
 open import Ledger.Utxow txs abs
 
 open Tx
+open GovActionState
+open EnactState using (cc)
 \end{code}
 
 The entire state transformation of the ledger state caused by a valid
@@ -56,6 +58,10 @@ record LState : Type where
 txgov : TxBody → List (GovVote ⊎ GovProposal)
 txgov txb = map inj₂ txprop ++ map inj₁ txvote
   where open TxBody txb
+
+allColdCreds : GovState → EnactState → ℙ Credential
+allColdCreds govSt es =
+  ccCreds (es .cc) ∪ concatMapˢ (λ (_ , st) → proposedCC (st .action)) (fromList govSt)
 \end{code}
 \end{AgdaMultiCode}
 \caption{Types and functions for the LEDGER transition system}
@@ -94,7 +100,7 @@ data
   LEDGER-V : let open LState s; txb = tx .body; open TxBody txb; open LEnv Γ in
     ∙  isValid tx ≡ true
     ∙  record { LEnv Γ } ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'
-    ∙  ⟦ epoch slot , pparams , txvote , txwdrls , deposits utxoSt ⟧ᶜ ⊢ certState ⇀⦇ txcerts ,CERTS⦈ certState'
+    ∙  ⟦ epoch slot , pparams , txvote , txwdrls , deposits utxoSt , allColdCreds govSt enactState ⟧ᶜ ⊢ certState ⇀⦇ txcerts ,CERTS⦈ certState'
     ∙  ⟦ txid , epoch slot , pparams , ppolicy , enactState ⟧ᵍ ⊢ govSt ⇀⦇ txgov txb ,GOV⦈ govSt'
        ────────────────────────────────
        Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ ⟦ utxoSt' , govSt' , certState' ⟧ˡ

src/Ledger/Ledger/Properties.agda

@@ -62,7 +62,7 @@ instance
       (tx : Tx)    (let open Tx tx renaming (body to txb); open TxBody txb)
       where
       utxoΓ = UTxOEnv ∋ record { LEnv Γ }
-      certΓ = CertEnv ∋ ⟦ epoch slot , pparams , txvote , txwdrls , UTxOState.deposits utxoSt ⟧ᶜ
+      certΓ = CertEnv ∋ ⟦ epoch slot , pparams , txvote , txwdrls , UTxOState.deposits utxoSt , _ ⟧ᶜ
       govΓ  = GovEnv  ∋ ⟦ txid , epoch slot , pparams , ppolicy , enactState ⟧ᵍ
 
       computeProof : ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s')