Skip to content

Commit

Permalink
Add a proper EnterpriseAddr type
Browse files Browse the repository at this point in the history
  • Loading branch information
@WhatisRT
WhatisRT committed Nov 18, 2024
1 parent 0158b1c commit d4249c7
Show file tree
Hide file tree
Showing 7 changed files with 43 additions and 25 deletions.
49 changes: 32 additions & 17 deletions src/Ledger/Address.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down Expand Up @@ -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
Expand All @@ -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}
Expand All @@ -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)
Expand All @@ -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) ∷ [])

Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/Ledger/Conway/Conformance/Utxo.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 3 additions & 0 deletions src/Ledger/Conway/Foreign/HSLedger/Address.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion src/Ledger/Utxo.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions src/ScriptVerification/HelloWorld.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/ScriptVerification/Lib.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 : ℕ)
Expand Down
6 changes: 3 additions & 3 deletions src/ScriptVerification/SucceedIfNumber.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down

0 comments on commit d4249c7

Please sign in to comment.