Add preliminary check that txIns exist in the UTxO prior to any changes

Author: carlostome

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

@@ -41,6 +41,7 @@ record UTxOEnv : Type where
     slot      : Slot
     pparams   : PParams
     treasury  : Treasury
+    utxo₀     : UTxO
 
 record UTxOState : Type where
   field
@@ -52,10 +53,19 @@ record UTxOState : Type where
 
 <!--
 ```agda
+open UTxOEnv
+open UTxOState
+-- open UTxOState
+
 private variable
   Γ : UTxOEnv
   s s' : UTxOState
   tx : TopLevelTx
+  -- utxo : UTxO
+  -- fees : Fees
+  -- donations : Donations
+  -- deposits : Deposits
+
 ```
 -->
 
@@ -73,20 +83,37 @@ data _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv → UTxOState → TopLevelTx → UTxOState
     Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ s
 ```
 
-## UTXO
+## The <span class="AgdaDatatype">UTXO</span> Transition System {#sec:the-utxo-transition-system}
+
+### New in Dijkstra
 
-(skeleton with the new phase-1 check)
+1. The set of spending inputs must exist in the UTxO _before_ applying the
+transaction (or partially applying any part of it). TODO: Add link to CIP once its finalized.
 
-This is the intended home of Dijkstra "phase-1 structural checks."
 
 ```agda
 data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv → UTxOState → TopLevelTx → UTxOState → Type where
 
-  UTXO-inductive :
-    let txb    = Tx.txBody tx
+  UTXO :
+    let
+```
+<!--
+```agda
+        open Tx tx renaming (txBody to txb)
+        open TxBody txb
+```
+-->
+```agda
         subTxs = TxBody.txSubTransactions txb
+        utxo₀  = Γ .utxo₀
+        utxo   = s .utxo
     in
+    ∙ txIns ≢ ∅
+    ∙ txIns ⊆ dom utxo₀ -- (1)
+    ∙ refInputs ⊆ dom utxo
+
     ∙ requiredTopLevelGuardsSatisfied tx subTxs
+
     ∙ Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ s'
       ────────────────────────────────
       Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'