Add time translation functions

src/Ledger/Conway/Conformance/Equivalence/Utxo.agda

@@ -52,7 +52,7 @@ module _ {Γ s tx s'} where
   utxoSDeposits (C.Scripts-No  _) = deposits
 
   utxoDeposits : Γ C.⊢ s ⇀⦇ tx ,UTXO⦈ s' → L.Deposits
-  utxoDeposits (C.UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ h) = utxoSDeposits h
+  utxoDeposits (C.UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ h) = utxoSDeposits h
 
   utxowDeposits : Γ C.⊢ s ⇀⦇ tx ,UTXOW⦈ s' → L.Deposits
   utxowDeposits (C.UTXOW-inductive⋯ _ _ _ _ _ _ _ _ _ _ h) = utxoDeposits h
@@ -79,8 +79,8 @@ instance
   -- deposits don't change! Why are they even part of the UTxOState?
   -- In conformance the update happens in GOVCERT (under CERT).
   UTXOToConf : ∀ {Γ s tx s'} → Γ L.⊢ s ⇀⦇ tx ,UTXO⦈ s' ⭆ Γ C.⊢ s ⇀⦇ tx ,UTXO⦈ (withDepositsFrom s s')
-  UTXOToConf {s = s} {tx = tx} .convⁱ _ (L.UTXO-inductive (a , b , c , d , e , f , g , r , h , i , j , k , l , m , n , o , p , utxo)) =
-    C.UTXO-inductive (a , b , c , d , e , f , g , r , h , i , j , k , l , m , n , o , p , conv utxo)
+  UTXOToConf {s = s} {tx = tx} .convⁱ _ (L.UTXO-inductive (a , b , c , d , e , f , g , r , h , i , j , k , l , m , n , o , p , q , utxo)) =
+    C.UTXO-inductive (a , b , c , d , e , f , g , r , h , i , j , k , l , m , n , o , p , q , conv utxo)
 
   UTXOFromConf : ∀ {Γ s tx s'}
                    (let open L.UTxOEnv Γ using () renaming (pparams to pp)
@@ -90,8 +90,8 @@ instance
                → (isValid tx ≡ false ⊎ L.ValidCertDeposits pp deposits txCerts)
                  ⊢ Γ C.⊢ s ⇀⦇ tx ,UTXO⦈ s' ⭆ⁱ λ _ h →
                    Γ L.⊢ s ⇀⦇ tx ,UTXO⦈ (setDeposits (utxoDeposits h) s')
-  UTXOFromConf {s = s} {tx = tx} .convⁱ validCerts (C.UTXO-inductive (a , b , c , d , e , f , g , r , h , i , j , k , l , m , n , o , p , utxo)) =
-    L.UTXO-inductive (a , b , c , d , e , f , g , r , h , i , j , k , l , m , n , o , p , (validCerts ⊢conv utxo))
+  UTXOFromConf {s = s} {tx = tx} .convⁱ validCerts (C.UTXO-inductive (a , b , c , d , e , f , g , r , h , i , j , k , l , m , n , o , p , q , utxo)) =
+    L.UTXO-inductive (a , b , c , d , e , f , g , r , h , i , j , k , l , m , n , o , p , q , (validCerts ⊢conv utxo))
 
   UTXOWToConf : ∀ {Γ s tx s'} → Γ L.⊢ s ⇀⦇ tx ,UTXOW⦈ s' ⭆ Γ C.⊢ s ⇀⦇ tx ,UTXOW⦈ (withDepositsFrom s s')
   UTXOWToConf .convⁱ _ (L.UTXOW-inductive⋯ a b c d e f g h i j utxo) =

src/Ledger/Conway/Conformance/Utxo.agda

@@ -91,6 +91,10 @@ data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type
     ∙ txIns ∩ refInputs ≡ ∅                  ∙ L.inInterval slot txVldt
     ∙ L.minfee pp utxo tx ≤ txFee            ∙ (txrdmrs ˢ ≢ ∅ → L.collateralCheck pp tx utxo)
     ∙ consumed pp s txb ≡ produced pp s txb  ∙ coin mint ≡ 0
+    ∙ (¬ (∅ᵐ ≡ᵐ txrdmrs) × nothing ≢ proj₁ txVldt →
+         (do s ← proj₁ txVldt
+             epochInfoSlotToUTCTime EI SysSt s) ≢ nothing
+      )
     ∙ txsize ≤ maxTxSize pp
     ∙ L.refScriptsSize utxo tx ≤ pp .maxRefScriptSizePerTx
 
@@ -108,6 +112,6 @@ data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type
       ────────────────────────────────
       Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'
 
-pattern UTXO-inductive⋯ tx Γ s x y z w k l m c v j n o p q r t u h
-      = UTXO-inductive {tx}{Γ}{s} (x , y , z , w , k , l , m , c , v , j , n , o , p , q , r , t , u , h)
+pattern UTXO-inductive⋯ tx Γ s x y z w k l m c v j n o p q r t u a h
+      = UTXO-inductive {tx}{Γ}{s} (x , y , z , w , k , l , m , c , v , j , n , o , p , q , r , t , u , a , h)
 unquoteDecl UTXO-premises = genPremises UTXO-premises (quote UTXO-inductive)

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 = λ _ _ _ → just 0
+    ; transVITime = λ _ _ _ → tt
     }
 
 open import Ledger.Core.Specification.Address Network KeyHash ScriptHash using () public

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

@@ -28,12 +28,40 @@ 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
+```
+
+In the Alonzo specification [VK21,](#alonzo-ledger-spec),
+`transVITime`{.AgdaFunction} is implemented in terms of operations coming from
+the plutus library. We defer bringing these operations to Agda until we actually
+need them by defining `transVITime`{.AgdaFunction} as abstract.
+
+```agda
+record AbstractFunctions : Type₁ where
+  field UTCTime      : Type
+        ⦃ DecEq-UTCTime ⦄ : DecEq UTCTime
+        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
+
+        -- Translates a ValidityInterval, which is expressed in slots, to a
+        -- POSIXTimeRange, expressed in terms of POSIXTime.
+        transVITime : EpochInfo → SystemStart → ValidityInterval → POSIXTimeRange
 ```
+
+## References {#references .unnumbered}
+
+**\[VK21\]** <span id="alonzo-ledger-spec"
+label="alonzo-ledger-spec"></span> Polina Vinogradova and Andre Knispel.
+*A Formal Specification of the Cardano Ledger integrating Plutus Core*.
+2021.

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

@@ -539,6 +539,10 @@ data _⊢_⇀⦇_,UTXO⦈_ where
     ∙ txIns ∩ refInputs ≡ ∅                  ∙ inInterval slot txVldt
     ∙ minfee pp utxo tx ≤ txFee              ∙ (txrdmrs ˢ ≢ ∅ → collateralCheck pp tx utxo)
     ∙ consumed pp s txb ≡ produced pp s txb  ∙ coin mint ≡ 0
+    ∙ (¬ (∅ᵐ ≡ᵐ txrdmrs) × nothing ≢ proj₁ txVldt →
+         (do s ← proj₁ txVldt
+             epochInfoSlotToUTCTime EI SysSt s) ≢ nothing
+      )
     ∙ txsize ≤ maxTxSize pp
     ∙ refScriptsSize utxo tx ≤ pp .maxRefScriptSizePerTx
     ∙ ∀[ (_ , txout) ∈ ∣ txOutsʰ ∣ ]
@@ -558,8 +562,8 @@ data _⊢_⇀⦇_,UTXO⦈_ where
 
 <!--
 ```agda
-pattern UTXO-inductive⋯ tx Γ s x y z w k l m c v j n o p q r t u h
-  = UTXO-inductive {Γ = Γ} {s = s} {tx = tx} (x , y , z , w , k , l , m , c , v , j , n , o , p , q , r , t , u , h)
+pattern UTXO-inductive⋯ tx Γ s x y z w k l m c d v j n o p q r t u h
+  = UTXO-inductive {Γ = Γ} {s = s} {tx = tx} (x , y , z , w , k , l , m , c , d , v , j , n , o , p , q , r , t , u , h)
 unquoteDecl UTXO-premises = genPremises UTXO-premises (quote UTXO-inductive)
 ```
 -->

src/Ledger/Conway/Specification/Utxo/Properties/Computational.lagda.md

@@ -117,16 +117,16 @@ instance
                                       (inj₂ _) → "something else broke"
 
         computeProofH : Dec H → ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s')
-        computeProofH (yes (x , y , z , e , k , l , m , c , v , j , n , o , p , q , r , t , u)) =
-            map₂′ (UTXO-inductive⋯ _ _ _ x y z e k l m c v j n o p q r t u) <$> computeProof' Γ s tx
+        computeProofH (yes (x , y , z , e , k , l , m , c , d , v , j , n , o , p , q , r , t , u)) =
+            map₂′ (UTXO-inductive⋯ _ _ _ x y z e k l m c d v j n o p q r t u) <$> computeProof' Γ s tx
         computeProofH (no ¬p) = failure $ genErr ¬p
 
         computeProof : ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s')
         computeProof = computeProofH H?
 
         completeness : ∀ s' → Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s' → map proj₁ computeProof ≡ success s'
-        completeness s' (UTXO-inductive⋯ _ _ _ x y z w k l m c v j n o p q r t u h) with H?
-        ... | no ¬p = ⊥-elim $ ¬p (x , y , z , w , k , l , m , c , v , j , n , o , p , q , r , t , u)
+        completeness s' (UTXO-inductive⋯ _ _ _ x y z w k l m c d v j n o p q r t u h) with H?
+        ... | no ¬p = ⊥-elim $ ¬p (x , y , z , w , k , l , m , c , d , v , j , n , o , p , q , r , t , u)
         ... | yes _ with computeProof' Γ s tx | completeness' _ _ _ _ h
         ... | success _ | refl = refl
 

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; just; _,_; ℕ; ⊤; 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 = λ _ _ _ → just 0
+  ; transVITime = λ _ _ _ → tt
   }