adding txinsScript function

IntersectMBO · Jul 27, 2023 · 76e2f0f · 76e2f0f
1 parent db84b14
commit 76e2f0f
Show file tree

Hide file tree

Showing 3 changed files with 25 additions and 3 deletions.
diff --git a/src/Ledger/ScriptValidation.agda b/src/Ledger/ScriptValidation.agda
@@ -107,9 +107,16 @@ txInfo l pp utxo tx = record
   where
     txb = body tx
 
+-- Figure 11
+scriptsNeeded : UTxO → TxBody → ℙ (ScriptPurpose × ScriptHash)
+scriptsNeeded utxo txb with txins txb
+... | ans = {!!}
+
 collectPhaseTwoScriptInputs : PParams → Tx
                                       → UTxO
                                       → List (Script × List Data × ExUnits × CostModel)
-collectPhaseTwoScriptInputs pp tx utxo with getDatum tx utxo {!!}
-... | ans = {!!}
+collectPhaseTwoScriptInputs pp tx utxo = {!scriptsNeeded!}
+
 
+{- with getDatum tx utxo {!!}
+... | ans = {!!} -}
diff --git a/src/Ledger/Transaction.lagda b/src/Ledger/Transaction.lagda
@@ -136,6 +136,7 @@ the transaction body are:
           wits    : TxWitnesses
           isValid : Bool
           txAD    : Maybe AuxiliaryData
+
 \end{code}
 \emph{Abstract functions}
 \begin{code}
@@ -152,6 +153,20 @@ the transaction body are:
 
   txinsVKey : ℙ TxIn → UTxO → ℙ TxIn
   txinsVKey txins utxo = txins ∩ dom ((utxo ↾' to-sp (isVKeyAddr? ∘ proj₁)) ˢ)
+
+  open import Relation.Nullary.Decidable using (⌊_⌋)
+
+  isScriptAddrUTxO : TxIn × TxOut → Bool
+  isScriptAddrUTxO (fst , addr , snd) = ⌊ isScriptAddr? addr ⌋
+
+  isScriptAddrUTxOProp : specProperty λ x → isScriptAddrUTxO x ≡ true
+  isScriptAddrUTxOProp = to-sp (λ x → isScriptAddrUTxO x ≟ true)
+
+  scriptOuts : UTxO → UTxO
+  scriptOuts utxo = filterᵐ (sp-∘ isScriptAddrUTxOProp λ z → z) utxo
+
+  txinsScript : ℙ TxIn → UTxO → ℙ TxIn
+  txinsScript txins utxo = txins ∩ dom (proj₁ (scriptOuts utxo))
 \end{code}
 \end{figure*}
 \begin{code}[hide]

diff --git a/src/Ledger/Utxo.lagda b/src/Ledger/Utxo.lagda
@@ -346,7 +346,7 @@ data _⊢_⇀⦇_,UTXO⦈_ where
 \begin{code}[hide]
 -- TODO: This can't be moved into Properties because it breaks. Move
 -- this once this is fixed.
---unquoteDecl Computational-UTXO = deriveComputational (quote _⊢_⇀⦇_,UTXO⦈_) Computational-UTXO
+-- unquoteDecl Computational-UTXO = deriveComputational (quote _⊢_⇀⦇_,UTXO⦈_) Computational-UTXO
 \end{code}
 \caption{UTXO inference rules}
 \label{fig:rules:utxo-shelley}