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}
@@ -327,6 +333,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⦈
+        ⟦ vDelegs , sDelegs , rwds ∪ˡ ❴ c , 0 ❵ ⟧ᵈ
+\end{code}
 \end{AgdaSuppressSpace}
 \caption{Auxiliary DELEG transition system}
 \label{fig:sts:aux-cert-deleg}

src/Ledger/Certs/Properties.agda

@@ -35,6 +35,11 @@ instance
     (dereg c d) → case ¿ (c , 0) ∈ rwds ¿ of λ where
       (yes p) → success (-, DELEG-dereg p)
       (no ¬p) → failure (genErrors ¬p)
+    (reg c d) → case ¿ c ∉ dom rwds
+                     × d ≡ pp .PParams.keyDeposit
+                     ¿ of λ where
+      (yes p) → success (-, DELEG-reg p)
+      (no ¬p) → failure (genErrors ¬p)
     _ → 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)
@@ -45,6 +50,8 @@ instance
                                            ¿) p .proj₂ = refl
   Computational-DELEG .completeness ⟦ _ , _ , _ ⟧ᵈᵉ ⟦ _ , _ , 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 ¿) p .proj₂ = refl
 
   Computational-POOL : Computational _⊢_⇀⦇_,POOL⦈_ String
   Computational-POOL .computeProof _ ⟦ pools , _ ⟧ᵖ (regpool c _) =
@@ -99,6 +106,10 @@ instance
     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ᵍ ⟧ᶜˢ
+    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ᵍ ⟧ᶜˢ
     dCert@(dereg c _) ⟦ stᵈ' , stᵖ , stᵍ ⟧ᶜˢ (CERT-deleg h)
     with computeProof ⟦ pp , PState.pools stᵖ , dom (GState.dreps stᵍ) ⟧ᵈᵉ stᵈ dCert | completeness _ _ _ _ h
@@ -186,7 +197,7 @@ module _  {Γ : CertEnv}
               → Γ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ' , stᵖ' , stᵍ' ⟧ᶜˢ
               → getCoin ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ≡ getCoin ⟦ stᵈ' , stᵖ' , stᵍ' ⟧ᶜˢ
   CERT-pov (CERT-deleg (DELEG-delegate {rwds = rwds} _)) = sym (∪ˡsingleton0≡ rwds)
-
+  CERT-pov (CERT-deleg (DELEG-reg {rwds = rwds} _)) = sym (∪ˡsingleton0≡ rwds)
   CERT-pov {stᵖ = stᵖ} {stᵖ'} {stᵍ} {stᵍ'}
     (CERT-deleg (DELEG-dereg {c = c} {rwds} {vDelegs = vDelegs}{sDelegs} x)) = begin
     getCoin ⟦ ⟦ vDelegs , sDelegs , rwds ⟧ᵈ , stᵖ , stᵍ ⟧ᶜˢ

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/Ledger/Properties.agda

@@ -319,9 +319,11 @@ module SetoidProperties (tx : Tx) (Γ : LEnv) (s : LState) where
   filterCR (regdrep _ _ _)     deps = filter-pres-≡ᵉ (dom-cong (resᵐ-∅ᶜ {M = deps}))
   filterCR (retirepool _ _)    deps = filter-pres-≡ᵉ (dom-cong (resᵐ-∅ᶜ {M = deps}))
   filterCR (ccreghot _ _)      deps = filter-pres-≡ᵉ (dom-cong (resᵐ-∅ᶜ {M = deps}))
+  filterCR (reg _ _)           deps = filter-pres-≡ᵉ (dom-cong (resᵐ-∅ᶜ {M = deps}))
 
   filterCD : (c : DCert) (deps : Deposits) → filterˢ isGADeposit (dom (certDeposit c pp ˢ)) ≡ᵉ ∅
   filterCD (delegate _ _ _ _)  deps = filter-∅ λ _ → CredDepIsNotGADep ∘ from ∈-singleton ∘ dom-single→single
+  filterCD (reg _ _)           deps = filter-∅ λ _ → CredDepIsNotGADep ∘ from ∈-singleton ∘ dom-single→single
   filterCD (regpool _ _)       deps = filter-∅ λ _ → PoolDepIsNotGADep ∘ from ∈-singleton ∘ dom-single→single
   filterCD (regdrep _ _ _)     deps = filter-∅ λ _ → DRepDepIsNotGADep ∘ from ∈-singleton ∘ dom-single→single
   filterCD (dereg _ _)         deps = ≡ᵉ.trans (filter-pres-≡ᵉ dom∅) $ filter-∅ λ _ a∈ _ → ∉-∅ a∈
@@ -342,6 +344,16 @@ module SetoidProperties (tx : Tx) (Γ : LEnv) (s : LState) where
     where
       cd = certDeposit dcert pp
       filter0 = filterCD dcert deps
+  noGACerts (dcert@(reg _ _) ∷ cs) deps = begin
+    filterˢ isGADeposit (dom (updateCertDeposits pp cs (deps ∪⁺ cd))) ≈⟨ noGACerts cs _ ⟩
+    filterˢ isGADeposit (dom (deps ∪⁺ cd)) ≈⟨ filter-pres-≡ᵉ dom∪⁺≡∪dom ⟩
+    filterˢ isGADeposit (dom deps ∪ dom (cd ˢ )) ≈⟨ filter-hom-∪ ⟩
+    filterˢ isGADeposit (dom deps) ∪ filterˢ isGADeposit (dom (cd ˢ)) ≈⟨ ∪-cong ≡ᵉ.refl $ filterCD dcert deps ⟩
+    filterˢ isGADeposit (dom deps) ∪ ∅ ≈⟨ ∪-identityʳ $ filterˢ isGADeposit (dom deps) ⟩
+    filterˢ isGADeposit (dom deps) ∎
+    where
+      cd = certDeposit dcert pp
+      filter0 = filterCD dcert deps
   noGACerts (dcert@(regpool _ _) ∷ cs) deps = begin
     filterˢ isGADeposit (dom (updateCertDeposits pp cs (deps ∪⁺ cd))) ≈⟨ noGACerts cs _ ⟩
     filterˢ isGADeposit (dom (deps ∪⁺ cd)) ≈⟨ filter-pres-≡ᵉ dom∪⁺≡∪dom ⟩

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

@@ -222,6 +222,7 @@ instance
 \begin{code}
 certDeposit : DCert → PParams → Deposits
 certDeposit (delegate c _ _ v) _   = ❴ CredentialDeposit c , v ❵
+certDeposit (reg c _)          pp  = ❴ CredentialDeposit c , pp .keyDeposit ❵
 certDeposit (regpool kh _)     pp  = ❴ PoolDeposit kh , pp .poolDeposit ❵
 certDeposit (regdrep c v _)    _   = ❴ DRepDeposit c , v ❵
 certDeposit _                  _   = ∅
@@ -245,6 +246,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 +277,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)
@@ -288,6 +294,12 @@ instance
 
 updateCertDeposits  : PParams → List DCert → Deposits → Deposits
 updateCertDeposits pp [] deposits = deposits
+\end{code}
+\begin{code}[hide]
+updateCertDeposits pp (reg c v ∷ certs) deposits
+  = updateCertDeposits pp certs (deposits ∪⁺ certDeposit (reg c v) pp)
+\end{code}
+\begin{code}
 updateCertDeposits pp (delegate c vd khs v ∷ certs) deposits
   = updateCertDeposits pp certs (deposits ∪⁺ certDeposit (delegate c vd khs v) pp)
 updateCertDeposits pp (regpool kh p ∷ certs) deposits

src/Ledger/Utxo/Properties.lagda

@@ -662,25 +662,27 @@ module _ -- ASSUMPTION --
           ∎
         where open Prelude.≡-Reasoning
 
-  ≤certDeps  :  (certs : List DCert)
-                {d : DepositPurpose ⇀ Coin} {(dp , c) : DepositPurpose × Coin}
+  ≤certDeps  :  {d : DepositPurpose ⇀ Coin} {(dp , c) : DepositPurpose × Coin}
              →  getCoin d ≤ getCoin (d ∪⁺ ❴ (dp , c) ❵)
 
-  ≤certDeps certs {d} = begin
+  ≤certDeps {d} = begin
     getCoin d                      ≤⟨ m≤m+n (getCoin d) _ ⟩
     getCoin d + _                  ≡⟨ sym ∪⁺singleton≡ ⟩
     getCoin (d ∪⁺ ❴ _ ❵)           ∎
     where open ≤-Reasoning
 
+
   ≤updateCertDeps : (cs : List DCert) {pp : PParams} {deposits :  DepositPurpose ⇀ Coin}
     → noRefundCert cs
     → getCoin deposits ≤ getCoin (updateCertDeposits pp cs deposits)
   ≤updateCertDeps [] nrf = ≤-reflexive refl
+  ≤updateCertDeps (reg c v ∷ cs) {pp} {deposits} (_ All.∷ nrf) =
+    ≤-trans ≤certDeps (≤updateCertDeps cs {pp} {deposits ∪⁺ ❴ CredentialDeposit c , pp .PParams.keyDeposit ❵} nrf)
   ≤updateCertDeps (delegate c _ _ v ∷ cs) {pp} {deposits} (_ All.∷ nrf) =
-    ≤-trans (≤certDeps cs) (≤updateCertDeps cs {pp} {deposits ∪⁺ ❴ CredentialDeposit c , v ❵} nrf)
-  ≤updateCertDeps (regpool _ _ ∷ cs)       (_ All.∷ nrf) = ≤-trans (≤certDeps cs) (≤updateCertDeps cs nrf)
+    ≤-trans ≤certDeps (≤updateCertDeps cs {pp} {deposits ∪⁺ ❴ CredentialDeposit c , v ❵} nrf)
+  ≤updateCertDeps (regpool _ _ ∷ cs)       (_ All.∷ nrf) = ≤-trans ≤certDeps (≤updateCertDeps cs nrf)
   ≤updateCertDeps (retirepool _ _ ∷ cs)    (_ All.∷ nrf) = ≤updateCertDeps cs nrf
-  ≤updateCertDeps (regdrep _ _ _ ∷ cs)     (_ All.∷ nrf) = ≤-trans (≤certDeps cs) (≤updateCertDeps cs nrf)
+  ≤updateCertDeps (regdrep _ _ _ ∷ cs)     (_ All.∷ nrf) = ≤-trans ≤certDeps (≤updateCertDeps cs nrf)
   ≤updateCertDeps (ccreghot _ _ ∷ cs)      (_ All.∷ nrf) = ≤updateCertDeps cs nrf
 
   -- Main Theorem: General Minimum Spending Condition --

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