From 28742bbae49e836b40e9ae53e02b4a1fa0802422 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Joosep=20J=C3=A4=C3=A4ger?= Date: Thu, 21 Nov 2024 17:11:11 +0200 Subject: [PATCH] Added `reg` cert --- src/Ledger/Certs.lagda | 31 ++++++++++++++++++------ src/Ledger/Conway/Conformance/Certs.agda | 1 + src/Ledger/ScriptValidation.agda | 4 +++ src/Ledger/Utxo.lagda | 5 ++++ src/Ledger/Utxow.lagda | 2 +- 5 files changed, 34 insertions(+), 9 deletions(-) diff --git a/src/Ledger/Certs.lagda b/src/Ledger/Certs.lagda index dca153797..8e9942eab 100644 --- a/src/Ledger/Certs.lagda +++ b/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} diff --git a/src/Ledger/Conway/Conformance/Certs.agda b/src/Ledger/Conway/Conformance/Certs.agda index 38d502316..21fd358d7 100644 --- a/src/Ledger/Conway/Conformance/Certs.agda +++ b/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 ❵ ᶜ diff --git a/src/Ledger/ScriptValidation.agda b/src/Ledger/ScriptValidation.agda index 8db1df934..77d0ffe6b 100644 --- a/src/Ledger/ScriptValidation.agda +++ b/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 diff --git a/src/Ledger/Utxo.lagda b/src/Ledger/Utxo.lagda index 777a4dd8b..791f727be 100644 --- a/src/Ledger/Utxo.lagda +++ b/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) diff --git a/src/Ledger/Utxow.lagda b/src/Ledger/Utxow.lagda index dcc508945..6bad8ce4f 100644 --- a/src/Ledger/Utxow.lagda +++ b/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