WIP

src/Ledger/Foreign/HSLedger/Address.agda

@@ -2,6 +2,10 @@ module Ledger.Foreign.HSLedger.Address where
 
 open import Ledger.Foreign.HSLedger.BaseTypes
 
+{-# FOREIGN GHC
+  import qualified MAlonzo.Code.Ledger.Foreign.HSTypes
+#-}
+
 instance
   HsTy-Credential = autoHsType Credential
   Conv-Credential = autoConvert Credential
@@ -17,3 +21,4 @@ instance
 
 unquoteDecl = do
   hsTypeAlias Addr
+  hsTypeAlias Wdrl

src/Ledger/Foreign/HSLedger/Core.agda

@@ -56,7 +56,7 @@ module Implementation where
   toData : ∀ {A : Type} → A → Data
   toData _ = tt
 
-  PlutusScript = ⊤
+  PlutusScript = ScriptHash
   ExUnits      = ℕ × ℕ
   ExUnit-CommutativeMonoid = IsCommutativeMonoid' 0ℓ 0ℓ ExUnits ∋ (toCommMonoid' record
     { Carrier = ExUnits
@@ -132,12 +132,9 @@ instance
     { hashRespectsUnion = hashRespectsUnion
     ; ps = HSP2ScriptStructure }
     where
-    postulate
-      instance Hashable-Timelock : Hashable Timelock ℕ
-
-      hashRespectsUnion : ∀ {A B ℍ}
-        → Hashable A ℍ → Hashable B ℍ
-        → Hashable (A ⊎ B) ℍ
+    hashRespectsUnion : {A B Hash : Type} → Hashable A Hash → Hashable B Hash → Hashable (A ⊎ B) Hash
+    hashRespectsUnion record { hash = hash₁ } record { hash = hash₂ } =
+      record { hash = λ where (inj₁ x) → hash₁ x; (inj₂ y) → hash₂ y }
 
     HSP2ScriptStructure : PlutusStructure
     HSP2ScriptStructure = record
@@ -217,3 +214,14 @@ instance
     }
 
 open import Ledger.Address Network KeyHash ScriptHash using () public
+
+-- * Aliases
+unquoteDecl = do
+  hsTypeAlias Coin
+  hsTypeAlias ExUnits
+  hsTypeAlias Data
+  hsTypeAlias Redeemer
+  hsTypeAlias AuxiliaryData
+  hsTypeAlias Epoch
+  hsTypeAlias ScriptHash
+  hsTypeAlias GovActionID

src/Ledger/Foreign/HSLedger/Gov.agda

@@ -110,6 +110,10 @@ instance
   HsTy-GovActionState = MkHsType GovActionState (HsType GovActionState')
   Conv-GovActionState = mkGovActionState' ⨾ Conv-GovActionState'
 
+unquoteDecl = do
+  hsTypeAlias Voter
+  hsTypeAlias GovState
+
 -- Computational function
 
 gov-step : HsType (GovEnv → GovState → List (GovVote ⊎ GovProposal) → ComputationResult String GovState)

src/Ledger/Foreign/HSLedger/Ledger.agda

@@ -14,7 +14,10 @@ open import Ledger.Ledger.Properties it it
 
 instance
   -- These are "duplicate" because of the duplicate STSs
-  HsTy-GState' = autoHsType GState ⊣ withConstructor "MkGState"
+  HsTy-GState' = autoHsType GState
+    ⊣ withName "GState'"
+    • withConstructor "MkGState'"
+    • fieldPrefix "gs'"
   Conv-GState' = autoConvert GState
 
   HsTy-DState' = autoHsType DState ⊣ withConstructor "MkDState"

src/Ledger/Foreign/HSLedger/Transaction.agda

@@ -17,6 +17,9 @@ instance
   {-# TERMINATING #-}
   Conv-Timelock = autoConvert Timelock
 
+  HsTy-HashedTimelock = autoHsType HashedTimelock ⊣ withConstructor "MkHashedTimelock"
+  Conv-HashedTimelock = autoConvert HashedTimelock
+
   HsTy-TxWitnessess = autoHsType TxWitnesses ⊣ withConstructor "MkTxWitnesses"
   Conv-TxWitnessess = autoConvert TxWitnesses
 
@@ -37,3 +40,4 @@ unquoteDecl = do
   hsTypeAlias DataHash ⊣ withName "DataHash"
   hsTypeAlias Value
   hsTypeAlias TxOut
+  hsTypeAlias RdmrPtr

src/Ledger/Gov.lagda

@@ -365,3 +365,4 @@ and some conditions depending on the type of the action:
   epoch are allowed, and candidates cannot be added and removed at the same time;
 \item and we check the validity of hard-fork actions via \validHFAction.
 \end{itemize}
+

src/Ledger/Script.lagda

@@ -152,15 +152,25 @@ instance
         (RequireTimeExpire a) → mapDec evalTEx evalTEx˘ dec
         (RequireMOf m xs)     → mapDec evalMOf evalMOf˘ (MOf-go? m xs)
 
-P1ScriptStructure-TL : ⦃ Hashable Timelock ScriptHash ⦄ → P1ScriptStructure
+record HashedTimelock : Type where
+  field
+    script : Timelock
+    h : ScriptHash
+
+unquoteDecl DecEq-HashedTimelock = derive-DecEq ((quote HashedTimelock , DecEq-HashedTimelock) ∷ [])
+instance
+  Hashable-HashedTimelock : Hashable HashedTimelock ScriptHash
+  Hashable-HashedTimelock = record { hash = HashedTimelock.h }
+
+P1ScriptStructure-TL : P1ScriptStructure
 P1ScriptStructure-TL = record
-  { P1Script = Timelock
-  ; validP1Script = evalTimelock }
+  { P1Script = HashedTimelock
+  ; validP1Script = λ kh I tl → evalTimelock kh I (tl .HashedTimelock.script)
+  }
 
 record ScriptStructure : Type₁ where
   field hashRespectsUnion :
           {A B Hash : Type} → Hashable A Hash → Hashable B Hash → Hashable (A ⊎ B) Hash
-        ⦃ Hash-Timelock ⦄ : Hashable Timelock ScriptHash
 
   p1s : P1ScriptStructure
   p1s = P1ScriptStructure-TL

src/Ledger/ScriptValidation.agda

@@ -180,5 +180,5 @@ open Tx
 evalScripts : Tx → List (Script × List Data × ExUnits × CostModel) → Bool
 evalScripts tx [] = true
 evalScripts tx ((inj₁ tl , d , eu , cm) ∷ Γ) =
-  ¿ evalTimelock (reqSigHash (body tx)) (txvldt (body tx)) tl ¿ᵇ ∧ evalScripts tx Γ
+  ¿ evalTimelock (reqSigHash (body tx)) (txvldt (body tx)) (tl .HashedTimelock.script) ¿ᵇ ∧ evalScripts tx Γ
 evalScripts tx ((inj₂ ps , d , eu , cm) ∷ Γ) = ⟦ ps ⟧, cm , eu , d ∧ evalScripts tx Γ

src/Ledger/hs-src/Lib.hs

@@ -4,14 +4,17 @@ module Lib
   ) where
 
 import MAlonzo.Code.Ledger.Foreign.HSTypes              as X
-  (HSSet(..), HSMap(..), ComputationResult(..))
+  (HSSet(..), HSMap(..), ComputationResult(..), Rational(..))
 import MAlonzo.Code.Ledger.Foreign.HSLedger.Address     as X
   (Credential(..), BaseAddr(..), BootstrapAddr(..), RwdAddr(..), Addr)
 import MAlonzo.Code.Ledger.Foreign.HSLedger.PParams     as X
   (DrepThresholds(..), PoolThresholds(..), Acnt(..), PParams(..), PParamsUpdate(..))
 import MAlonzo.Code.Ledger.Foreign.HSLedger.Transaction as X
-  ( Tag(..), Timelock(..), TxWitnesses(..), TxBody(..), Tx(..), TxId, Ix, TxIn, P1Script, P2Script
-  , Script, Datum, DataHash, Value, TxOut)
+  ( Tag(..), Timelock(..), TxWitnesses(..), TxBody(..)
+  , Tx(..), TxId, Ix, TxIn, P1Script, P2Script, Script
+  , Datum, DataHash, Value, TxOut, HashedTimelock(..)
+  , RdmrPtr
+  )
 import MAlonzo.Code.Ledger.Foreign.HSLedger.Cert        as X
   (certStep', certsStep')
 import MAlonzo.Code.Ledger.Foreign.HSLedger.Chain       as X
@@ -27,10 +30,14 @@ import MAlonzo.Code.Ledger.Foreign.HSLedger.Gov         as X
   ( GovRole(..), Anchor(..), VDeleg(..), Vote(..), GovVote(..), GovEnv(..), GovProposal(..)
   , GovActionState(..), govStep)
 import MAlonzo.Code.Ledger.Foreign.HSLedger.Ledger      as X
-  (LEnv(..), LState(..), ledgerStep, CertState(..), DState(..))
+  ( LEnv(..), LState(..), ledgerStep, CertState(..), DState(..)
+  , GState'(..))
 import MAlonzo.Code.Ledger.Foreign.HSLedger.NewEpoch    as X
   (NewEpochState(..), newEpochStep, HsRewardUpdate(..))
 import MAlonzo.Code.Ledger.Foreign.HSLedger.Ratify      as X
   (StakeDistrs(..), RatifyEnv(..), RatifyState(..), ratifyStep)
 import MAlonzo.Code.Ledger.Foreign.HSLedger.Utxo        as X
   (UTxOEnv(..), UTxOState(..), UTxO, utxoStep, utxowStep)
+import MAlonzo.Code.Ledger.Foreign.HSLedger.Core        as X
+  ( Coin, ExUnits, Redeemer, AuxiliaryData, Epoch
+  , ScriptHash, GovActionID)

src/ScriptVerification/LedgerImplementation.agda

@@ -123,17 +123,12 @@ instance _ = SVCrypto
 
 open import Ledger.Script it it
 
-
-
 SVScriptStructure : ScriptStructure
 SVScriptStructure = record
   { hashRespectsUnion = hashRespectsUnion
-  ; ps = SVP2ScriptStructure }
+  ; ps = SVP2ScriptStructure
+  }
   where
-
-    instance Hashable-Timelock : Hashable Timelock ℕ
-             Hashable-Timelock = record { hash = λ x → 0 }
-
     instance Hashable-PlutusScript : Hashable Implementation.PlutusScript ℕ
              Hashable-PlutusScript = record { hash = λ x → proj₁ x }