Add premise on epochInfoSlotToUTCTime to UTXO rule

Author: facundominguez

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/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ʰ ∣ ]