Added HSPlutusScript

Author: Soupstraw

src/Ledger/Conway/Conformance/Script.agda

@@ -24,18 +24,28 @@ module Ledger.Conway.Conformance.Script
 
 open Ledger.Script crypto es
 
-record HashedTimelock : Type where
+record HSTimelock : Type where
   field
     timelock : Timelock
     storedHash : ScriptHash
 
 instance
-  Hashable-HashedTimelock : Hashable HashedTimelock ScriptHash
-  Hashable-HashedTimelock .hash = HashedTimelock.storedHash
+  Hashable-HSTimelock : Hashable HSTimelock ScriptHash
+  Hashable-HSTimelock .hash = HSTimelock.storedHash
 
-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 scriptHash : ScriptHash
+        serSize    : ℕ
+
+instance
+  Hashable-HSPlutusScript : Hashable HSPlutusScript ScriptHash
+  Hashable-HSPlutusScript .hash = HSPlutusScript.scriptHash
 
 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/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) → hash x
+        (inj₂ x) → hash 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/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