Added HSPlutusScript, changed refScriptsSize

src/Ledger/Conway/Conformance/Script.agda

@@ -24,18 +24,29 @@ module Ledger.Conway.Conformance.Script
 
 open Ledger.Script crypto es
 
-record HashedTimelock : Type where
+record HSTimelock : Type where
   field
-    timelock : Timelock
-    storedHash : ScriptHash
+    timelock     : Timelock
+    tlScriptHash : ScriptHash
+    tlScriptSize : ℕ
 
 instance
-  Hashable-HashedTimelock : Hashable HashedTimelock ScriptHash
-  Hashable-HashedTimelock .hash = HashedTimelock.storedHash
+  Hashable-HSTimelock : Hashable HSTimelock ScriptHash
+  Hashable-HSTimelock .hash = HSTimelock.tlScriptHash
 
-unquoteDecl DecEq-HashedTimelock = derive-DecEq ((quote HashedTimelock , DecEq-HashedTimelock) ∷ [])
+unquoteDecl DecEq-HSTimelock = derive-DecEq ((quote HSTimelock , DecEq-HSTimelock) ∷ [])
+
+record HSPlutusScript : Type where
+  constructor MkHSPlutusScript
+  field psScriptHash : ScriptHash
+        psScriptSize : ℕ
+
+instance
+  Hashable-HSPlutusScript : Hashable HSPlutusScript ScriptHash
+  Hashable-HSPlutusScript .hash = HSPlutusScript.psScriptHash
 
 P1ScriptStructure-HTL : P1ScriptStructure
 P1ScriptStructure-HTL = record
-  { P1Script = HashedTimelock
-  ; validP1Script = λ x y → evalTimelock x y ∘ HashedTimelock.timelock }
+  { P1Script = HSTimelock
+  ; validP1Script = λ x y → evalTimelock x y ∘ HSTimelock.timelock }
+

src/Ledger/Conway/Conformance/Utxow.agda

@@ -35,7 +35,7 @@ data _⊢_⇀⦇_,UTXOW⦈_ where
         witsKeyHashes     = mapˢ hash (dom vkSigs)
         witsScriptHashes  = mapˢ hash scripts
         inputHashes       = L.getInputHashes tx utxo
-        refScriptHashes   = mapˢ hash (refScripts tx utxo)
+        refScriptHashes   = fromList $ map hash (refScripts tx utxo)
         neededHashes      = L.scriptsNeeded utxo txb
         txdatsHashes      = dom txdats
         allOutHashes      = L.getDataHashes (range txouts)

src/Ledger/Conway/Foreign/HSLedger/Core.agda

@@ -79,7 +79,6 @@ module Implementation where
   toData : ∀ {A : Type} → A → Data
   toData _ = 0
 
-  PlutusScript = ℕ × ⊤
   ExUnits      = ℕ × ℕ
   ExUnit-CommutativeMonoid = CommutativeMonoid 0ℓ 0ℓ ExUnits ∋ (Conversion.fromBundle record
     { Carrier = ExUnits
@@ -94,9 +93,6 @@ module Implementation where
   instance
     Show-ExUnits : Show ExUnits
     Show-ExUnits = Show-×
-
-    Hashable-PlutusScript : Hashable PlutusScript ℕ
-    Hashable-PlutusScript .hash (h , _) = h
 
   CostModel    = ⊤
   Language     = ⊤

src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda

@@ -50,6 +50,7 @@ instance
       HSP2ScriptStructure = record
         { Implementation
         ; validPlutusScript = λ _ _ _ _ → ⊤
+        ; PlutusScript = HSPlutusScript
         }
 
 open import Ledger.PParams it it it hiding (Acnt; DrepThresholds; PoolThresholds)
@@ -120,7 +121,9 @@ instance
       ; indexOfProposal = λ _ _ → nothing
       }
     ; runPLCScript = λ _ _ _ _ → false
-    ; scriptSize = λ _ → 0
+    ; scriptSize = λ where 
+        (inj₁ x) → HSTimelock.tlScriptSize x
+        (inj₂ x) → HSPlutusScript.psScriptSize x
     }
 
 open import Ledger.Address Network KeyHash ScriptHash using () public

src/Ledger/Conway/Foreign/HSLedger/Transaction.agda

@@ -18,8 +18,11 @@ instance
   {-# TERMINATING #-}
   Conv-Timelock = autoConvert Timelock
 
-  HsTy-HashedTimelock = autoHsType HashedTimelock
-  Conv-HashedTimelock = autoConvert HashedTimelock
+  HsTy-HSTimelock = autoHsType HSTimelock
+  Conv-HSTimelock = autoConvert HSTimelock
+
+  HsTy-HSPlutusScript = autoHsType HSPlutusScript
+  Conv-HSPlutusScript = autoConvert HSPlutusScript
 
   HsTy-TxWitnessess = autoHsType TxWitnesses ⊣ withConstructor "MkTxWitnesses"
   Conv-TxWitnessess = autoConvert TxWitnesses

src/Ledger/Conway/Foreign/HSLedger/Utxo.agda

@@ -2,9 +2,11 @@
 
 module Ledger.Conway.Foreign.HSLedger.Utxo where
 
+open import Ledger.Prelude
+
 open import Ledger.Conway.Foreign.ExternalFunctions
 
-open import Data.String.Base renaming (_++_ to _+ˢ_) hiding (show; length)
+open import Data.String.Base renaming (_++_ to _+ˢ_) hiding (show; length; map; fromList)
 
 open import Ledger.Conway.Foreign.HSLedger.Core
 open import Ledger.Conway.Foreign.HSLedger.Address
@@ -65,6 +67,9 @@ module _ (ext : ExternalFunctions) where
           ("\tDeposits:    \t" +ˢ show (inject (L.newDeposits pparams (from st) body))) ∷
           ("\tFees:        \t" +ˢ show (inject txfee)) ∷
           ("\tTotal:       \t" +ˢ show (L.produced pparams (from st) body)) ∷
+          "" ∷
+          "Reference Scripts Info:" ∷
+          ("\tTotal size: \t" +ˢ show (L.refScriptsSize utxo (from tx))) ∷
           []
 
   {-# COMPILE GHC utxo-debug as utxoDebug #-}
@@ -77,7 +82,7 @@ module _ (ext : ExternalFunctions) where
         open UTxOEnv (from env)
         open TxWitnesses (coerce ⦃ TrustMe ⦄ wits)
         neededHashes = LW.scriptsNeeded utxo body
-        refScriptHashes = mapˢ 
+        refScriptHashes = fromList $ map
           hash 
           (refScripts (coerce ⦃ TrustMe ⦄ (from tx)) (coerce ⦃ TrustMe ⦄ utxo))
         witsScriptHashes  = mapˢ hash scripts

src/Ledger/Transaction.lagda

@@ -211,13 +211,13 @@ Ingredients of the transaction body introduced in the Conway era are the followi
   txinsScript : ℙ TxIn → UTxO → ℙ TxIn
   txinsScript txins utxo = txins ∩ dom (proj₁ (scriptOuts utxo))
 
-  refScripts : Tx → UTxO → ℙ Script
+  refScripts : Tx → UTxO → List Script
   refScripts tx utxo =
-    mapPartial (proj₂ ∘ proj₂ ∘ proj₂) (range (utxo ∣ (txins ∪ refInputs)))
+    mapMaybe (proj₂ ∘ proj₂ ∘ proj₂) $ setToList (range (utxo ∣ (txins ∪ refInputs)))
     where open Tx; open TxBody (tx .body)
 
   txscripts : Tx → UTxO → ℙ Script
-  txscripts tx utxo = scripts (tx .wits) ∪ refScripts tx utxo
+  txscripts tx utxo = scripts (tx .wits) ∪ fromList (refScripts tx utxo)
     where open Tx; open TxWitnesses
 
   lookupScriptHash : ScriptHash → Tx → UTxO → Maybe Script

src/Ledger/Utxo.lagda

@@ -206,7 +206,7 @@ module _ (let open Tx; open TxBody; open TxWitnesses) where opaque
 \end{NoConway}
 \begin{code}
   refScriptsSize : UTxO → Tx → ℕ
-  refScriptsSize utxo tx = ∑[ x ← mapValues scriptSize (setToHashMap (refScripts tx utxo)) ] x
+  refScriptsSize utxo tx = sum $ map scriptSize (refScripts tx utxo)
 
   minfee : PParams → UTxO → Tx → Coin
   minfee pp utxo tx  = pp .a * tx .body .txsize + pp .b

src/Ledger/Utxow.lagda

@@ -157,7 +157,7 @@ data _⊢_⇀⦇_,UTXOW⦈_ where
         witsKeyHashes     = mapˢ hash (dom vkSigs)
         witsScriptHashes  = mapˢ hash scripts
         inputHashes       = getInputHashes tx utxo
-        refScriptHashes   = mapˢ hash (refScripts tx utxo)
+        refScriptHashes   = fromList $ map hash (refScripts tx utxo)
         neededHashes      = scriptsNeeded utxo txb
         txdatsHashes      = dom txdats
         allOutHashes      = getDataHashes (range txouts)

src/Ledger/hs-src/Lib.hs

@@ -12,7 +12,7 @@ import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.PParams     as X
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Transaction as X
   ( Tag(..), Timelock(..), TxWitnesses(..), TxBody(..), Tx(..), TxId, Ix, TxIn, P1Script, P2Script
   , Script, Datum, DataHash, Value, TxOut, RdmrPtr, ScriptHash, AuxiliaryData, Wdrl
-  , HashedTimelock(..))
+  , HSTimelock (..), HSPlutusScript (..))
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Cert        as X
   (certStep, certsStep, CertState(..))
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Chain       as X