Add preconditions to UTXOW

Author: carlostome

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

@@ -38,9 +38,11 @@ open import Ledger.Dijkstra.Specification.Script.Validation txs abs
 ```agda
 record UTxOEnv : Type where
   field
-    slot      : Slot
-    pparams   : PParams
-    treasury  : Treasury
+    slot             : Slot
+    pparams          : PParams
+    treasury         : Treasury
+    utxo₀            : UTxO
+    refInputsScripts : ℙ Script
 
 record UTxOState : Type where
   field

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

@@ -24,22 +24,53 @@ module Ledger.Dijkstra.Specification.Utxow
   where
 
 open import Ledger.Dijkstra.Specification.Utxo txs abs
+open import Ledger.Dijkstra.Specification.Script.Validation txs abs
 
 private variable
+  ℓ : TxLevel
   Γ  : UTxOEnv
   s s' : UTxOState
-  tx : TopLevelTx
+  tx : Tx ℓ
 ```
 -->
 
 ```agda
-data _⊢_⇀⦇_,UTXOW⦈_ : UTxOEnv → UTxOState → TopLevelTx → UTxOState → Type where
+data _⊢_⇀⦇_,UTXOW⦈_ : UTxOEnv → UTxOState → Tx ℓ → UTxOState → Type where
 
-  UTXOW-inductive :
-    ∙ Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'
+  UTXOW :
+    let
+         open Tx tx
+         open TxBody txBody
+         open TxWitnesses txWitnesses
+
+         utxo₀               = Γ .UTxOEnv.utxo₀
+         utxo                = s .UTxOState.utxo
+         witsKeyHashes       = mapˢ hash (dom vKeySigs)
+         neededScriptHashes  = mapPartial (isScriptObj  ∘ proj₂) (credsNeeded utxo₀ txBody)
+         neededVKeyHashes    = mapPartial (isKeyHashObj ∘ proj₂) (credsNeeded utxo₀ txBody)
+         -- txdatsHashes        = mapˢ hash txdats
+         -- inputsDataHashes    = mapPartial (λ txout →  if txOutToP2Script utxo tx txout
+         --                                              then txOutToDataHash txout
+         --                                              else nothing) (range (utxo ∣ txIns))
+         -- refInputsDataHashes = mapPartial txOutToDataHash (range (utxo ∣ refInputs))
+         -- outputsDataHashes   = mapPartial txOutToDataHash (range txOuts)
+         p1Scripts       = mapPartial toP1Script
+           ( scripts                             -- (1) scripts from witnesses
+             ∪ mapPartial txOutScript
+                 ( range (utxo₀ ∣ txIns)         -- (2) scripts from transaction inputs
+                   ∪ range (utxo ∣ refInputs)    -- (3) scripts from reference inputs
+                 )
+             ∪ Γ .UTxOEnv.refInputsScripts       -- (4) scripts from all reference inputs
+           )
+    in
+    ∙  ∀[ (vk , σ) ∈ vKeySigs ] isSigned vk (txidBytes txId) σ
+    ∙  ∀[ s ∈ p1Scripts ] (hash s ∈ neededScriptHashes → validP1Script witsKeyHashes txVldt s)
+    ∙  neededVKeyHashes ⊆ witsKeyHashes
+    -- ∙  inputsDataHashes ⊆ txdatsHashes
+    -- ∙  txdatsHashes ⊆ inputsDataHashes ∪ outputsDataHashes ∪ refInputsDataHashes
+    -- ∙  languages tx utxo ⊆ allowedLanguages tx utxo
+    -- ∙  txADhash ≡ map hash txAD
+    -- ∙  Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'
       ────────────────────────────────
       Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s'
 ```
-
-This file intentionally contains **no** additional premises yet.  As Dijkstra witnessing
-evolves, this is where signature / script / datum / language constraints can be added.