Add abstract functions and types for handling time

Author: facundominguez

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

@@ -129,6 +129,14 @@ instance
         (inj₁ x) → HSTimelock.tlScriptSize x
         (inj₂ x) → HSPlutusScript.psScriptSize x
     ; valContext = λ _ _ → zero
+    ; UTCTime = ℕ
+    ; POSIXTimeRange = ⊤
+    ; EpochInfo = ⊤
+    ; SystemStart = ⊤
+    ; EI = tt
+    ; SysSt = tt
+    ; epochInfoSlotToUTCTime = λ _ _ _ → nothing
+    ; transVITime = λ _ _ _ → tt
     }
 
 open import Ledger.Core.Specification.Address Network KeyHash ScriptHash using () public

src/Ledger/Conway/Specification/Abstract.lagda.md

@@ -28,12 +28,22 @@ record indexOf : Type where
     indexOfVote           : GovVoter       → List GovVoter     → Maybe Ix
     indexOfProposal       : GovProposal    → List GovProposal  → Maybe Ix
 
-record AbstractFunctions : Type where
-  field txscriptfee  : Prices → ExUnits → Coin
+ValidityInterval = Maybe Slot × Maybe Slot
+
+record AbstractFunctions : Type₁ where
+  field UTCTime      : Type
+        POSIXTimeRange : Type
+        EpochInfo    : Type
+        SystemStart  : Type
+        EI           : EpochInfo
+        SysSt        : SystemStart
+        txscriptfee  : Prices → ExUnits → Coin
         serSize      : Value → MemoryEstimate
         indexOfImp   : indexOf
         runPLCScript : CostModel → P2Script → ExUnits → List Data → Bool
         scriptSize   : Script → ℕ
         valContext   : TxInfo → ScriptPurpose → Data
         getLanguageView : PParams → Language → LangDepView
+        epochInfoSlotToUTCTime : EpochInfo → SystemStart → Slot → Maybe UTCTime
+        transVITime : EpochInfo → SystemStart → ValidityInterval → POSIXTimeRange
 ```

src/Test/AbstractImplementation.agda

@@ -10,7 +10,7 @@ module Test.AbstractImplementation
   (valContext' : TxInfo → ScriptPurpose → D)
   where
 
-open import Ledger.Prelude using (nothing; _,_)
+open import Ledger.Prelude using (nothing; _,_; ℕ; ⊤; tt; id)
 
 open import Test.LedgerImplementation T D
   renaming (SVTransactionStructure to SVTransactionStructure')
@@ -34,4 +34,12 @@ SVAbstractFunctions = record
   ; runPLCScript = λ { x (sh , script) x₂ x₃ → script x₃ }
   ; scriptSize = λ _ → 0
   ; valContext = valContext'
+  ; UTCTime = ℕ
+  ; POSIXTimeRange = ⊤
+  ; EpochInfo = ⊤
+  ; SystemStart = ⊤
+  ; EI = tt
+  ; SysSt = tt
+  ; epochInfoSlotToUTCTime = λ _ _ _ → nothing
+  ; transVITime = λ _ _ _ → tt
   }