From d4249c7350e6525b0ebc9fbf978d61487b55add1 Mon Sep 17 00:00:00 2001 From: whatisRT Date: Mon, 18 Nov 2024 14:22:50 +0100 Subject: [PATCH] Add a proper `EnterpriseAddr` type --- src/Ledger/Address.lagda | 49 ++++++++++++------- src/Ledger/Conway/Conformance/Utxo.agda | 2 +- .../Conway/Foreign/HSLedger/Address.agda | 3 ++ src/Ledger/Utxo.lagda | 2 +- src/ScriptVerification/HelloWorld.agda | 4 +- src/ScriptVerification/Lib.agda | 2 +- src/ScriptVerification/SucceedIfNumber.agda | 6 +-- 7 files changed, 43 insertions(+), 25 deletions(-) diff --git a/src/Ledger/Address.lagda b/src/Ledger/Address.lagda index db5b5e549..7193d867e 100644 --- a/src/Ledger/Address.lagda +++ b/src/Ledger/Address.lagda @@ -6,6 +6,7 @@ open import Ledger.Prelude open import Tactic.Derive.DecEq open import Tactic.Derive.Show +import Data.Sum.Relation.Unary.All as Sum module Ledger.Address ( \end{code} @@ -59,7 +60,11 @@ data isScript : Credential → Type where record BaseAddr : Type where field net : Network pay : Credential - stake : Maybe Credential + stake : Credential + +record EnterpriseAddr : Type where + field net : Network + pay : Credential record BootstrapAddr : Type where field net : Network @@ -71,18 +76,21 @@ record RwdAddr : Type where stake : Credential \end{code} \begin{code}[hide] -open BaseAddr; open BootstrapAddr; open BaseAddr; open BootstrapAddr +open BaseAddr; open EnterpriseAddr; open BootstrapAddr +open BootstrapAddr using (attrsSize) public \end{code} \begin{code} -VKeyBaseAddr = Σ[ addr ∈ BaseAddr ] isVKey (addr .pay) -VKeyBootstrapAddr = Σ[ addr ∈ BootstrapAddr ] isVKey (addr .pay) -ScriptBaseAddr = Σ[ addr ∈ BaseAddr ] isScript (addr .pay) -ScriptBootstrapAddr = Σ[ addr ∈ BootstrapAddr ] isScript (addr .pay) +VKeyBaseAddr = Σ[ addr ∈ BaseAddr ] isVKey (addr .pay) +VKeyEnterpriseAddr = Σ[ addr ∈ EnterpriseAddr ] isVKey (addr .pay) +VKeyBootstrapAddr = Σ[ addr ∈ BootstrapAddr ] isVKey (addr .pay) +ScriptBaseAddr = Σ[ addr ∈ BaseAddr ] isScript (addr .pay) +ScriptEnterpriseAddr = Σ[ addr ∈ EnterpriseAddr ] isScript (addr .pay) +ScriptBootstrapAddr = Σ[ addr ∈ BootstrapAddr ] isScript (addr .pay) -Addr = BaseAddr ⊎ BootstrapAddr -VKeyAddr = VKeyBaseAddr ⊎ VKeyBootstrapAddr -ScriptAddr = ScriptBaseAddr ⊎ ScriptBootstrapAddr +Addr = BaseAddr ⊎ EnterpriseAddr ⊎ BootstrapAddr +VKeyAddr = VKeyBaseAddr ⊎ VKeyEnterpriseAddr ⊎ VKeyBootstrapAddr +ScriptAddr = ScriptBaseAddr ⊎ ScriptEnterpriseAddr ⊎ ScriptBootstrapAddr \end{code} \\ \emph{Helper functions} @@ -104,13 +112,15 @@ isScriptRwdAddr = isScript ∘ RwdAddr.stake \end{figure*} \begin{code}[hide] payCred (inj₁ record {pay = pay}) = pay -payCred (inj₂ record {pay = pay}) = pay +payCred (inj₂ (inj₁ record {pay = pay})) = pay +payCred (inj₂ (inj₂ record {pay = pay})) = pay -stakeCred (inj₁ record {stake = stake}) = stake +stakeCred (inj₁ record {stake = stake}) = just stake stakeCred (inj₂ _) = nothing netId (inj₁ record {net = net}) = net -netId (inj₂ record {net = net}) = net +netId (inj₂ (inj₁ record {net = net})) = net +netId (inj₂ (inj₂ record {net = net})) = net data isBootstrapAddr : Addr → Set where IsBootstrapAddr : ∀ a → isBootstrapAddr (inj₂ a) @@ -120,6 +130,9 @@ instance isBootstrapAddr? {inj₁ _} = ⁇ no λ () isBootstrapAddr? {inj₂ a} = ⁇ yes (IsBootstrapAddr a) +if_isBootstrapAddr_ : Addr → (BootstrapAddr → Set) → Set +if a isBootstrapAddr P = Sum.All (const ⊤) (Sum.All (const ⊤) P) a + instance unquoteDecl DecEq-Credential = derive-DecEq ((quote Credential , DecEq-Credential) ∷ []) @@ -141,13 +154,15 @@ _ = isScriptRwdAddr ⁇¹ ∋ it getScriptHash : ∀ a → isScriptAddr a → ScriptHash getScriptHash (inj₁ _) (SHisScript sh) = sh -getScriptHash (inj₂ _) (SHisScript sh) = sh +getScriptHash (inj₂ (inj₁ _)) (SHisScript sh) = sh +getScriptHash (inj₂ (inj₂ _)) (SHisScript sh) = sh instance abstract - unquoteDecl DecEq-BaseAddr DecEq-BootstrapAddr DecEq-RwdAddr = derive-DecEq - ( (quote BaseAddr , DecEq-BaseAddr) - ∷ (quote BootstrapAddr , DecEq-BootstrapAddr) - ∷ (quote RwdAddr , DecEq-RwdAddr) + unquoteDecl DecEq-BaseAddr DecEq-EnterpriseAddr DecEq-BootstrapAddr DecEq-RwdAddr = derive-DecEq + ( (quote BaseAddr , DecEq-BaseAddr) + ∷ (quote EnterpriseAddr , DecEq-EnterpriseAddr) + ∷ (quote BootstrapAddr , DecEq-BootstrapAddr) + ∷ (quote RwdAddr , DecEq-RwdAddr) ∷ [] ) module _ ⦃ _ : Show Network ⦄ ⦃ _ : Show KeyHash ⦄ ⦃ _ : Show ScriptHash ⦄ where diff --git a/src/Ledger/Conway/Conformance/Utxo.agda b/src/Ledger/Conway/Conformance/Utxo.agda index 1470791f1..8da2fff06 100644 --- a/src/Ledger/Conway/Conformance/Utxo.agda +++ b/src/Ledger/Conway/Conformance/Utxo.agda @@ -280,7 +280,7 @@ data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type ∙ ∀[ (_ , txout) ∈ txoutsʰ .proj₁ ] serSize (getValueʰ txout) ≤ maxValSize pp ∙ ∀[ (a , _) ∈ range txoutsʰ ] - Sum.All (const ⊤) (λ a → a .BootstrapAddr.attrsSize ≤ 64) a + if a isBootstrapAddr (λ a → a .attrsSize ≤ 64) ∙ ∀[ (a , _) ∈ range txoutsʰ ] netId a ≡ NetworkId ∙ ∀[ a ∈ dom txwdrls ] a .RwdAddr.net ≡ NetworkId ∙ txNetworkId ≡? NetworkId diff --git a/src/Ledger/Conway/Foreign/HSLedger/Address.agda b/src/Ledger/Conway/Foreign/HSLedger/Address.agda index e0b0ff879..266b2b043 100644 --- a/src/Ledger/Conway/Foreign/HSLedger/Address.agda +++ b/src/Ledger/Conway/Foreign/HSLedger/Address.agda @@ -9,6 +9,9 @@ instance HsTy-BaseAddr = autoHsType BaseAddr ⊣ fieldPrefix "base" Conv-BaseAddr = autoConvert BaseAddr + HsTy-EnterpriseAddr = autoHsType EnterpriseAddr ⊣ fieldPrefix "enterprise" + Conv-EnterpriseAddr = autoConvert EnterpriseAddr + HsTy-BootstrapAddr = autoHsType BootstrapAddr ⊣ fieldPrefix "boot" Conv-BootstrapAddr = autoConvert BootstrapAddr diff --git a/src/Ledger/Utxo.lagda b/src/Ledger/Utxo.lagda index 777a4dd8b..4b5d95a9e 100644 --- a/src/Ledger/Utxo.lagda +++ b/src/Ledger/Utxo.lagda @@ -531,7 +531,7 @@ data _⊢_⇀⦇_,UTXO⦈_ where ∙ ∀[ (_ , txout) ∈ txoutsʰ .proj₁ ] serSize (getValueʰ txout) ≤ maxValSize pp ∙ ∀[ (a , _) ∈ range txoutsʰ ] - Sum.All (const ⊤) (λ a → a .BootstrapAddr.attrsSize ≤ 64) a + if a isBootstrapAddr (λ a → a .attrsSize ≤ 64) ∙ ∀[ (a , _) ∈ range txoutsʰ ] netId a ≡ NetworkId ∙ ∀[ a ∈ dom txwdrls ] a .RwdAddr.net ≡ NetworkId ∙ txNetworkId ≡? NetworkId diff --git a/src/ScriptVerification/HelloWorld.agda b/src/ScriptVerification/HelloWorld.agda index 3669e905e..6be00ce52 100644 --- a/src/ScriptVerification/HelloWorld.agda +++ b/src/ScriptVerification/HelloWorld.agda @@ -35,7 +35,7 @@ initEnv = createEnv 0 initTxOut : TxOut initTxOut = inj₁ (record { net = 0 ; pay = ScriptObj 777 ; - stake = just (ScriptObj 777) }) + stake = ScriptObj 777 }) , 10 , nothing , nothing script : TxIn × TxOut @@ -52,7 +52,7 @@ succeedTx = record { body = record ∷ (5 , ((inj₁ (record { net = 0 ; pay = KeyHashObj 5 ; - stake = just (KeyHashObj 5) })) + stake = KeyHashObj 5 })) , (1000000000000 - 10000000000) , nothing , nothing)) ∷ []) ; txfee = 10000000000 diff --git a/src/ScriptVerification/Lib.agda b/src/ScriptVerification/Lib.agda index a81467104..7b79bea51 100644 --- a/src/ScriptVerification/Lib.agda +++ b/src/ScriptVerification/Lib.agda @@ -81,7 +81,7 @@ createUTxO : (index : ℕ) → Maybe (D ⊎ DataHash) → TxIn × TxOut createUTxO index wallet value d = (index , index) - , (inj₁ (record { net = 0 ; pay = KeyHashObj wallet ; stake = just (KeyHashObj wallet) }) + , (inj₁ (record { net = 0 ; pay = KeyHashObj wallet ; stake = KeyHashObj wallet }) , value , d , nothing) createInitUtxoState : (wallets : ℕ) diff --git a/src/ScriptVerification/SucceedIfNumber.agda b/src/ScriptVerification/SucceedIfNumber.agda index 2d1d821d9..476ce3531 100644 --- a/src/ScriptVerification/SucceedIfNumber.agda +++ b/src/ScriptVerification/SucceedIfNumber.agda @@ -44,14 +44,14 @@ initEnv = createEnv 0 initTxOut : TxOut initTxOut = inj₁ (record { net = 0 ; pay = ScriptObj 777 ; - stake = just (ScriptObj 777) }) + stake = ScriptObj 777 }) , 10 , just (inj₂ 99) , nothing -- initTxOut for script without datum reference initTxOut' : TxOut initTxOut' = inj₁ (record { net = 0 ; pay = ScriptObj 888 ; - stake = just (ScriptObj 888) }) + stake = ScriptObj 888 }) , 10 , nothing , nothing scriptDatum : TxIn × TxOut @@ -74,7 +74,7 @@ succeedTx = record { body = record ∷ (5 , ((inj₁ (record { net = 0 ; pay = KeyHashObj 5 ; - stake = just (KeyHashObj 5) })) + stake = KeyHashObj 5 })) , (1000000000000 - 10000000000) , nothing , nothing)) ∷ []) ; txfee = 10000000000