Add UTXOW preconditions

Author: carlostome

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

@@ -1,4 +1,4 @@
----
+--
 source_branch: master
 source_path: src/Ledger/Dijkstra/Specification/Ledger.lagda
 ---
@@ -197,15 +197,15 @@ data _⊢_⇀⦇_,SUBLEDGER⦈_ : SubLedgerEnv → LState → SubLevelTx → LSt
 ```agda
     in
       ∙ isTopLevelValid ≡ true
-      ∙ ⟦ slot , pp , treasury ⟧  ⊢ utxoState ⇀⦇ stx ,SUBUTXOW⦈ utxoState'
+      ∙ ⟦ slot , pp , treasury , {!!} ⟧  ⊢ utxoState ⇀⦇ stx ,SUBUTXOW⦈ utxoState'
       ∙ ⟦ epoch slot , pp , txGovVotes , txWithdrawals , allColdCreds govState enactState ⟧ ⊢ certState ⇀⦇ txCerts ,CERTS⦈ certState'
       ∙ ⟦ txId , epoch slot , pp , ppolicy , enactState , certState' , dom (RewardsOf certState) ⟧ ⊢ {- rmOrphanDRepVotes certState' -} govState ⇀⦇ txgov txb ,GOVS⦈ govState'
       ────────────────────────────────
       ⟦ slot , ppolicy , pp , enactState , treasury , isTopLevelValid ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState' , govState' , certState' ⟧
 
   SUBLEDGER-I :
       ∙ isTopLevelValid ≡ false
-      ∙ ⟦ slot , pp , treasury ⟧ ⊢ utxoState ⇀⦇ stx ,SUBUTXOW⦈ utxoState
+      ∙ ⟦ slot , pp , treasury , {!!} ⟧ ⊢ utxoState ⇀⦇ stx ,SUBUTXOW⦈ utxoState
       ────────────────────────────────
       ⟦ slot , ppolicy , pp , enactState , treasury , isTopLevelValid ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState , govState , certState ⟧
 
@@ -237,7 +237,7 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LState → TopLevelTx → LState 
     in
       ∙ isValid tx ≡ true
       ∙ ⟦ slot , ppolicy , pp , enactState , treasury , isValid tx ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ txSubTransactions ,SUBLEDGERS⦈ ⟦ utxoState' , govState' , certState' ⟧
-      ∙ ⟦ slot , pp , treasury ⟧  ⊢ utxoState' ⇀⦇ tx ,UTXOW⦈ utxoState''
+      ∙ ⟦ slot , pp , treasury , {!!} ⟧  ⊢ utxoState' ⇀⦇ tx ,UTXOW⦈ utxoState''
       ∙ ⟦ epoch slot , pp , txGovVotes , txWithdrawals , allColdCreds govState enactState ⟧ ⊢ certState' ⇀⦇ txCerts ,CERTS⦈ certState''
       ∙ ⟦ txId , epoch slot , pp , ppolicy , enactState , certState' , dom (RewardsOf certState) ⟧ ⊢ {- rmOrphanDRepVotes certState' -} govState ⇀⦇ txgov txb ,GOVS⦈ govState'
       ────────────────────────────────
@@ -255,7 +255,7 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LState → TopLevelTx → LState 
     in
       ∙ isValid tx ≡ false
       ∙ ⟦ slot , ppolicy , pp , enactState , treasury , isValid tx ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ txSubTransactions  ,SUBLEDGERS⦈ ⟦ utxoState , govState , certState ⟧
-      ∙ ⟦ slot , pp , treasury ⟧ ⊢ utxoState ⇀⦇ tx ,UTXOW⦈ utxoState'
+      ∙ ⟦ slot , pp , treasury , {!!} ⟧ ⊢ utxoState ⇀⦇ tx ,UTXOW⦈ utxoState'
       ────────────────────────────────
       ⟦ slot , ppolicy , pp , enactState , treasury ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ tx ,LEDGER⦈ ⟦ utxoState' , govState , certState ⟧
 ```

src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md

@@ -129,12 +129,12 @@ credsNeededMinusCollateral txb = a ∪ b ∪ c ∪ d ∪ e
   e = mapPartial (λ p → if PolicyOf p then (λ {sh} → just (Propose  p , ScriptObj sh)) else nothing)
                  (fromList (GovProposalsOf txb))
 
-credsNeeded : (ℓ : TxLevel) → UTxO → (TxBody ℓ) → ℙ (ScriptPurpose × Credential)
-credsNeeded TxLevelTop utxo txb = credsNeededMinusCollateral txb
+credsNeeded : {ℓ : TxLevel} → UTxO → (TxBody ℓ) → ℙ (ScriptPurpose × Credential)
+credsNeeded {TxLevelTop} utxo txb = credsNeededMinusCollateral txb
   ∪ mapˢ (λ (i , o) → (Spend  i , payCred (proj₁ o))) ((utxo ∣ (txIns ∪ collateralInputs)) ˢ)
   where open TxBody txb
 
-credsNeeded TxLevelSub utxo txb = credsNeededMinusCollateral txb
+credsNeeded {TxLevelSub} utxo txb = credsNeededMinusCollateral txb
   ∪ mapˢ (λ (i , o) → (Spend  i , payCred (proj₁ o))) ((utxo ∣ txIns) ˢ)
   where open TxBody txb
 

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

@@ -397,6 +397,11 @@ This section collects some unimportant but useful helper and accessor functions.
   txinsScript : ℙ TxIn → UTxO → ℙ TxIn
   txinsScript txins utxo = txins ∩ dom (proj₁ (scriptOuts utxo))
 
+  txOutToScript : TxOut → Maybe Script
+  txOutToScript (_ , _ , _ , s) = s
+
+```
+
   refScripts : Tx txLevel → UTxO → List Script
   refScripts tx utxo =
     mapMaybe (proj₂ ∘ proj₂ ∘ proj₂) $ setToList (range (utxo ∣ (txIns ∪ refInputs)))
@@ -406,6 +411,7 @@ This section collects some unimportant but useful helper and accessor functions.
   txscripts tx utxo = scripts (tx .txWitnesses) ∪ fromList (refScripts tx utxo)
     where open Tx; open TxWitnesses
 
+<<<<<<< HEAD
   lookupScriptHash : ScriptHash → Tx txLevel → UTxO → Maybe Script
   lookupScriptHash sh tx utxo =
     if sh ∈ mapˢ proj₁ (m ˢ) then
@@ -414,6 +420,17 @@ This section collects some unimportant but useful helper and accessor functions.
       nothing
     where m = setToMap (mapˢ < hash , id > (txscripts tx utxo))
 
+=======
+  lookupScriptHash : ScriptHash → Tx txLevel → UTxO → UTxO → Maybe Script
+  lookupScriptHash sh tx utxoSpend₀ utxoRefView = lookupHash sh (txscripts tx utxoSpend₀ utxoRefView)
+
+  -- TODO: implement the actual evolving `utxoRefView` (issue #1006)
+
+```
+
+<!--
+```agda
+>>>>>>> fc70f5e8 (Add UTXOW preconditions)
   getSubTxScripts : SubLevelTx → ℙ (TxId × ScriptHash)
   getSubTxScripts subtx = mapˢ (λ hash → (TxIdOf subtx , hash)) (ScriptHashes subtx)
     where
@@ -428,6 +445,10 @@ This section collects some unimportant but useful helper and accessor functions.
   getTxScripts {TxLevelTop} =
     concatMapˢ getSubTxScripts ∘ fromList ∘ TxBody.txSubTransactions ∘ TxBodyOf
 ```
+<<<<<<< HEAD
+=======
+-->
+>>>>>>> fc70f5e8 (Add UTXOW preconditions)
 
 CIP-0118 models "required top-level guards" as a list of requirements coming
 from subtransaction bodies. The list can contain duplicates, and later logic

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

@@ -38,9 +38,12 @@ 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
+    globalRefInputsScripts : ℙ Script
+    globalData             : DataHash ⇀ Datum
 
 record UTxOState : Type where
   field
@@ -102,10 +105,17 @@ data _⊢_⇀⦇_,SUBUTXO⦈_ : UTxOEnv → UTxOState → SubLevelTx → UTxOSta
 data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv → UTxOState → TopLevelTx → UTxOState → Type where
 
   UTXO :
+<<<<<<< HEAD
     let txb    = Tx.txBody tx
         subTxs = TxBody.txSubTransactions txb
     in
     ∙ requiredTopLevelGuardsSatisfied tx subTxs
+=======
+    ∙ SpendInputsOf tx ≢ ∅
+    ∙ SpendInputsOf tx ⊆ dom (UTxOOf Γ)                           -- (1)
+    ∙ ReferenceInputsOf tx ⊆ dom (UTxOOf s)
+    ∙ requiredTopLevelGuardsSatisfied tx (SubTransactionsOf tx)   -- (2)
+>>>>>>> fc70f5e8 (Add UTXOW preconditions)
     ∙ Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ s'
       ────────────────────────────────
       Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'

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

@@ -3,12 +3,7 @@ source_branch: master
 source_path: src/Ledger/Dijkstra/Specification/Utxow.lagda.md
 ---
 
-# UTxOW (Dijkstra skeleton)
-
-This is a **minimal skeleton** of the Dijkstra-era witnessing layer.
-
-It currently acts as a wrapper around `UTXO`, mirroring Conway's shape, but without
-committing to full witnessing checks yet.
+# UTxOW
 
 <!--
 ```agda
@@ -24,30 +19,133 @@ 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
   stx : SubLevelTx
 ```
 -->
 
+```agda
+languages : Tx ℓ → UTxO → ℙ Language
+languages tx utxo = ∅ -- TODO
+
+allowedLanguages : Tx ℓ → UTxO → ℙ Language
+allowedLanguages tx utxo = ∅ -- TODO
+```
+
 ```agda
 data _⊢_⇀⦇_,SUBUTXOW⦈_ : UTxOEnv → UTxOState → SubLevelTx → UTxOState → Type where
 
   SUBUTXOW :
+    let
+         open Tx tx
+         open TxBody txBody
+         open TxWitnesses txWitnesses
+         open UTxOEnv
+
+         utxo₀               = Γ .utxo₀
+         utxo                = s .UTxOState.utxo
+
+         witsKeyHashes       : ℙ KeyHash
+         witsKeyHashes       = mapˢ hash (dom vKeySigs)
+
+         allScripts : ℙ Script
+         allScripts =
+           ( scripts                             -- (1) scripts from witnesses
+             ∪ mapPartial txOutToScript
+                 ( range (utxo₀ ∣ txIns)         -- (2) scripts from transaction inputs
+                   ∪ range (utxo ∣ refInputs)    -- (3) scripts from reference inputs
+                 )
+             ∪ Γ .globalRefInputsScripts         -- (4) scripts from global reference inputs
+           )
+
+         p1Scripts : ℙ P1Script
+         p1Scripts = mapPartial toP1Script allScripts
+
+         p2Scripts : ℙ P2Script
+         p2Scripts = mapPartial toP2Script allScripts
+
+         neededScriptHashes  : ℙ ScriptHash
+         neededScriptHashes  = mapPartial (isScriptObj  ∘ proj₂) (credsNeeded utxo₀ txBody)
+
+         neededVKeyHashes : ℙ KeyHash
+         neededVKeyHashes = mapPartial (isKeyHashObj ∘ proj₂) (credsNeeded utxo₀ txBody)
+
+         neededDataHashes : ℙ DataHash
+         neededDataHashes = mapPartial (λ txOut@(a , _ , d , _) → do sh ← isScriptObj (payCred a)
+                                                                     _  ← lookupHash sh p2Scripts
+                                                                     d >>= isInj₂)
+                                       (range (utxo₀ ∣ txIns))
+
+    in
+    ∙  ∀[ (vk , σ) ∈ vKeySigs ] isSigned vk (txidBytes txId) σ
+    ∙  ∀[ s ∈ p1Scripts ] (hash s ∈ neededScriptHashes → validP1Script witsKeyHashes txVldt s)
+    ∙  neededVKeyHashes ⊆ witsKeyHashes
+    ∙  neededScriptHashes ⊆ mapˢ hash allScripts
+    ∙  neededDataHashes ⊆ dom (Γ .globalData)
+    ∙  languages tx utxo ⊆ allowedLanguages tx utxo
+    ∙  txADhash ≡ map hash txAuxData
     ∙ Γ ⊢ s ⇀⦇ stx ,SUBUTXO⦈ s'
       ────────────────────────────────
       Γ ⊢ s ⇀⦇ stx ,SUBUTXOW⦈ s'
 
 data _⊢_⇀⦇_,UTXOW⦈_ : UTxOEnv → UTxOState → TopLevelTx → UTxOState → Type where
 
   UTXOW :
-    ∙ Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'
+    let
+         open Tx tx
+         open TxBody txBody
+         open TxWitnesses txWitnesses
+         open UTxOEnv
+
+         utxo₀               = Γ .utxo₀
+         utxo                = s .UTxOState.utxo
+
+         witsKeyHashes       : ℙ KeyHash
+         witsKeyHashes       = mapˢ hash (dom vKeySigs)
+
+         allScripts : ℙ Script
+         allScripts =
+           ( scripts                             -- (1) scripts from witnesses
+             ∪ mapPartial txOutToScript
+                 ( range (utxo₀ ∣ txIns)         -- (2) scripts from transaction inputs
+                   ∪ range (utxo ∣ refInputs)    -- (3) scripts from reference inputs
+                 )
+             ∪ Γ .globalRefInputsScripts         -- (4) scripts from global reference inputs
+           )
+
+         p1Scripts : ℙ P1Script
+         p1Scripts = mapPartial toP1Script allScripts
+
+         p2Scripts : ℙ P2Script
+         p2Scripts = mapPartial toP2Script allScripts
+
+         neededScriptHashes  : ℙ ScriptHash
+         neededScriptHashes  = mapPartial (isScriptObj  ∘ proj₂) (credsNeeded utxo₀ txBody)
+
+         neededVKeyHashes : ℙ KeyHash
+         neededVKeyHashes = mapPartial (isKeyHashObj ∘ proj₂) (credsNeeded utxo₀ txBody)
+
+         neededDataHashes : ℙ DataHash
+         neededDataHashes = mapPartial (λ txOut@(a , _ , d , _) → do sh ← isScriptObj (payCred a)
+                                                                     _  ← lookupHash sh p2Scripts
+                                                                     d >>= isInj₂)
+                                       (range (utxo₀ ∣ txIns))
+
+    in
+    ∙  ∀[ (vk , σ) ∈ vKeySigs ] isSigned vk (txidBytes txId) σ
+    ∙  ∀[ s ∈ p1Scripts ] (hash s ∈ neededScriptHashes → validP1Script witsKeyHashes txVldt s)
+    ∙  neededVKeyHashes ⊆ witsKeyHashes
+    ∙  neededScriptHashes ⊆ mapˢ hash allScripts
+    ∙  neededDataHashes ⊆ dom (Γ .globalData)
+    ∙  languages tx utxo ⊆ allowedLanguages tx utxo
+    ∙  txADhash ≡ map hash txAuxData
+    ∙  Γ ⊢ 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.

src/Ledger/Prelude.lagda.md

@@ -86,4 +86,8 @@ module Filter where
   filter : ∀ {a} {p} {A : Type a} → (P : Pred A p) → ⦃ P ⁇¹ ⦄ → List A → List A
   filter P = Data.List.filter ¿ P ¿¹
 
+lookupHash : ∀ {T H : Type} ⦃ _ : DecEq H ⦄ ⦃ _ : Hashable T H ⦄ → H → ℙ T → Maybe T
+lookupHash h s =
+  if h ∈ mapˢ proj₁ (m ˢ) then just (lookupᵐ m h) else nothing
+  where m = setToMap (mapˢ < hash , id > s)
 ```