stake field of BaseAddr should be optional

This closes issue #606.
IntersectMBO · Nov 12, 2024 · 8efbcad · 8efbcad
1 parent bb05c86
commit 8efbcad
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 8 deletions.
diff --git a/src/Ledger/Address.lagda b/src/Ledger/Address.lagda
@@ -59,7 +59,7 @@ data isScript : Credential → Type where
 record BaseAddr : Type where
   field net    : Network
         pay    : Credential
-        stake  : Credential
+        stake  : Maybe Credential
 
 record BootstrapAddr : Type where
   field net        : Network
@@ -106,7 +106,7 @@ isScriptRwdAddr  = isScript ∘ RwdAddr.stake
 payCred (inj₁ record {pay = pay}) = pay
 payCred (inj₂ record {pay = pay}) = pay
 
-stakeCred (inj₁ record {stake = stake}) = just stake
+stakeCred (inj₁ record {stake = stake}) = stake
 stakeCred (inj₂ _) = nothing
 
 netId (inj₁ record {net = net}) = net

diff --git 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 = ScriptObj 777 })
+                           stake = just (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 = KeyHashObj 5 }))
+                                                                    stake = just (KeyHashObj 5) }))
                                                  , (1000000000000 - 10000000000) , nothing , nothing))
                                                ∷ [])
                          ; txfee = 10000000000

diff --git 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 = KeyHashObj wallet })
+                                , (inj₁ (record { net = 0 ; pay = KeyHashObj wallet ; stake = just (KeyHashObj wallet) })
                                   , value , d , nothing)
 
 createInitUtxoState : (wallets : ℕ)

diff --git 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 = ScriptObj 777 })
+                           stake = just (ScriptObj 777) })
                            , 10 , just (inj₂ 99) , nothing
 
 -- initTxOut for script without datum reference
 initTxOut' : TxOut
 initTxOut' = inj₁ (record { net = 0 ;
                            pay = ScriptObj 888 ;
-                           stake = ScriptObj 888 })
+                           stake = just (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 = KeyHashObj 5 }))
+                                                                     stake = just (KeyHashObj 5) }))
                                                   , (1000000000000 - 10000000000) , nothing , nothing))
                                                 ∷ [])
                          ; txfee = 10000000000