Added reg cert

src/Ledger/Certs.lagda

@@ -56,16 +56,22 @@ data DCert : Type where
   deregdrep   : Credential → Coin → DCert
   ccreghot    : Credential → Maybe Credential → DCert
 \end{code}
+\begin{code}[hide]
+  reg         : Credential → Coin → DCert
+\end{code}
 \begin{NoConway}
 \begin{code}
-cwitness : DCert → Credential
-cwitness (delegate c _ _ _)  = c
-cwitness (dereg c _)         = c
-cwitness (regpool kh _)      = KeyHashObj kh
-cwitness (retirepool kh _)   = KeyHashObj kh
-cwitness (regdrep c _ _)     = c
-cwitness (deregdrep c _)     = c
-cwitness (ccreghot c _)      = c
+cwitness : DCert → Maybe Credential
+cwitness (delegate c _ _ _)  = just c
+cwitness (dereg c _)         = just c
+cwitness (regpool kh _)      = just $ KeyHashObj kh
+cwitness (retirepool kh _)   = just $ KeyHashObj kh
+cwitness (regdrep c _ _)     = just c
+cwitness (deregdrep c _)     = just c
+cwitness (ccreghot c _)      = just c
+\end{code}
+\begin{code}[hide]
+cwitness (reg _ _)           = nothing
 \end{code}
 \end{NoConway}
 \end{AgdaMultiCode}
@@ -328,6 +334,15 @@ data _⊢_⇀⦇_,DELEG⦈_ where
       ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢  ⟦ vDelegs , sDelegs , rwds ⟧ᵈ ⇀⦇ dereg c d ,DELEG⦈
                           ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧ᵈ
 \end{code}
+\begin{code}[hide]
+  DELEG-reg : let open PParams pp in
+    ∙ c ∉ dom rwds
+    ∙ d ≡ keyDeposit
+      ────────────────────────────────
+      ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢
+        ⟦ vDelegs , sDelegs , rwds ⟧ᵈ ⇀⦇ reg c d ,DELEG⦈
+        ⟦ insertIfJust c mv vDelegs , insertIfJust c mkh sDelegs , rwds ∪ˡ ❴ c , 0 ❵ ⟧ᵈ
+\end{code}
 \end{AgdaSuppressSpace}
 \caption{Auxiliary DELEG transition system}
 \label{fig:sts:aux-cert-deleg}

src/Ledger/Conway/Conformance/Certs.agda

@@ -54,6 +54,7 @@ certRefund _                = ∅
 
 updateCertDeposit  : PParams → DCert → Deposits → Deposits
 updateCertDeposit pp (delegate c _ _ v) deposits = deposits ∪⁺ ❴ CredentialDeposit c , v ❵
+updateCertDeposit pp (reg c _)          deposits = deposits ∪⁺ ❴ CredentialDeposit c , pp .PParams.keyDeposit ❵
 updateCertDeposit pp (regdrep c v _)    deposits = deposits ∪⁺ ❴ DRepDeposit c , v ❵
 updateCertDeposit pp (dereg c _)        deposits = deposits ∣ ❴ CredentialDeposit c ❵ ᶜ
 updateCertDeposit pp (deregdrep c _)    deposits = deposits ∣ ❴ DRepDeposit c ❵ ᶜ

src/Ledger/ScriptValidation.agda

@@ -78,6 +78,7 @@ txInfo l pp utxo tx = record
   } where open Tx tx; open TxBody body
 
 data DelegateOrDeReg : DCert → Type where instance
+  reg       : ∀ {x y} →     DelegateOrDeReg (reg x y)
   delegate  : ∀ {x y z w} → DelegateOrDeReg (delegate x y z w)
   dereg     : ∀ {x y} →     DelegateOrDeReg (dereg x y)
   regdrep   : ∀ {x y z} →   DelegateOrDeReg (regdrep x y z)
@@ -87,6 +88,7 @@ instance
   Dec-DelegateOrDeReg : DelegateOrDeReg ⁇¹
   Dec-DelegateOrDeReg {dc} .dec with dc
   ... | delegate _ _ _ _ = yes it
+  ... | reg _ _          = yes it
   ... | dereg _ _        = yes it
   ... | regdrep _ _ _    = yes it
   ... | deregdrep _ _    = yes it
@@ -125,6 +127,8 @@ certScripts d with ¿ DelegateOrDeReg d ¿
 ... | no ¬p = nothing
 certScripts c@(delegate  (KeyHashObj x) _ _ _) | yes p = nothing
 certScripts c@(delegate  (ScriptObj  y) _ _ _) | yes p = just (Cert c , y)
+certScripts c@(reg       (KeyHashObj x) _)     | yes p = nothing
+certScripts c@(reg       (ScriptObj  y) _)     | yes p = just (Cert c , y)
 certScripts c@(dereg     (KeyHashObj x) _)     | yes p = nothing
 certScripts c@(dereg     (ScriptObj  y) _)     | yes p = just (Cert c , y)
 certScripts c@(regdrep   (KeyHashObj x) _ _)   | yes p = nothing

src/Ledger/Utxo.lagda

@@ -245,6 +245,9 @@ data ValidCertDeposits (pp : PParams) (deps : Deposits) : List DCert → Set
   regdrep    : ∀ {c v a certs}
              → ValidCertDeposits pp (deps ∪⁺ ❴ DRepDeposit c , v ❵) certs
              → ValidCertDeposits pp deps (regdrep c v a ∷ certs)
+  reg        : ∀ {c v certs}
+             → ValidCertDeposits pp (deps ∪⁺ ❴ CredentialDeposit c , v ❵) certs
+             → ValidCertDeposits pp deps (reg c v ∷ certs)
   dereg      : ∀ {c d certs}
              → (CredentialDeposit c , d) ∈ deps
              → ValidCertDeposits pp (deps ∣ ❴ CredentialDeposit c ❵ ᶜ) certs
@@ -273,6 +276,8 @@ private
     mapDec retirepool (λ where (retirepool p) → p) (validCertDeposits? _ _)
   validCertDeposits? deps (ccreghot _ _ ∷ certs) =
     mapDec ccreghot (λ where (ccreghot p) → p) (validCertDeposits? _ _)
+  validCertDeposits? deps (reg _ _ ∷ certs) =
+    mapDec reg (λ where (reg p) → p) (validCertDeposits? _ _)
   validCertDeposits? deps (dereg c d ∷ certs) with ¿ (CredentialDeposit c , d) ∈ deps ¿
   ... | yes p = mapDec (dereg p)  (λ where (dereg _ d) → d) (validCertDeposits? _ _)
   ... | no ¬p = no (λ where (dereg p _) → ¬p p)

src/Ledger/Utxow.lagda

@@ -101,7 +101,7 @@ credsNeeded : UTxO → TxBody → ℙ (ScriptPurpose × Credential)
 credsNeeded utxo txb
   =  mapˢ (λ (i , o)  → (Spend  i , payCred (proj₁ o))) ((utxo ∣ txins) ˢ)
   ∪  mapˢ (λ a        → (Rwrd   a , stake a)) (dom (txwdrls .proj₁))
-  ∪  mapˢ (λ c        → (Cert   c , cwitness c)) (fromList txcerts)
+  ∪  mapPartial (λ c  → (Cert   c ,_) <$> cwitness c) (fromList txcerts)
   ∪  mapˢ (λ x        → (Mint   x , ScriptObj x)) (policies mint)
   ∪  mapˢ (λ v        → (Vote   v , proj₂ v)) (fromList (map voter txvote))
   ∪  mapPartial (λ p  → case  p .policy of