From ba20b8ec6b452ef2266c5249b3986c0bc712a428 Mon Sep 17 00:00:00 2001 From: whatisRT Date: Mon, 26 Jul 2021 17:19:23 +0200 Subject: [PATCH] Remove duplicate check for required scripts in UTXOW --- alonzo/formal-spec/utxo.tex | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/alonzo/formal-spec/utxo.tex b/alonzo/formal-spec/utxo.tex index a07183ce6a..1270aca148 100644 --- a/alonzo/formal-spec/utxo.tex +++ b/alonzo/formal-spec/utxo.tex @@ -874,11 +874,10 @@ \subsection{Witnessing} \hldiff{\var{inputHashes}\leteq \{ h \mid (\_ \mapsto (a, \_, h)) \in \txins{txb} \restrictdom \var{utxo}, \fun{isTwoPhaseScriptAddress}~{tx}~{a}\}} \\~\\ \hldiff{\forall \var{s} \in \range (\fun{txscripts}~{txw}) \cap \ScriptPhOne, \fun{validateScript}~\var{s}~\var{tx}}\\~\\ - \hldiff{\{ s \mid (\_, s) \in \fun{scriptsNeeded}~\var{utxo}~\var{tx}\} = \dom (\fun{txscripts}~{txw})} \\~\\ + \hldiff{\{ h \mid (\_, h) \in \fun{scriptsNeeded}~\var{utxo}~\var{tx}\} = \dom (\fun{txscripts}~{txw})} \\~\\ \hldiff{\var{inputHashes} \subseteq \dom (\fun{txdats}~{txw})} \\~\\ \hldiff{\dom (\fun{txdats}~{txw}) \subseteq \var{inputHashes} \cup \{h~\mid~ (\wcard, \wcard, h)\in\fun{txouts}\}} \\~\\ - \hldiff{\forall (\_, h) \in \fun{scriptsNeeded}~\var{utxo}~\var{tx},~h \in \dom (\fun{txscripts}~(\fun{txwits}~tx))} \\ \hldiff{\ \dom (\fun{txrdmrs}~tx) ~=~\{~\fun{rdptr}~txb~sp~ \vert~ (sp,h)~\in~\fun{scriptsNeeded}~\var{utxo}~\var{tx}, } \\ \hldiff{h\mapsto s~\in~\fun{txscripts}~{txw}, s~\in~\ScriptPhTwo \}}