Eliminate checkScriptData from the formal spec

alonzo/formal-spec/utxo.tex

@@ -765,10 +765,6 @@ \subsection{Witnessing}
   paired with the hashes of corresponding the witnessing scripts.
   This function collects hashes of both phase-1 and phase-2 scripts.
 
-  \item $\fun{checkScriptData}$ returns $\True$ if, for the given script purpose,
-  whenever the script it points to is phase-2, the transaction contains an associated entry
-  in the indexed redeemers structure.
-
   \item $\fun{languages}$ returns the set of (phase-2) script languages
   of all the scripts included in the transaction
 \end{itemize}
@@ -801,10 +797,6 @@ \subsection{Witnessing}
     & \where \\
     & ~~~~~~~ \var{txb}~=~\txbody{tx}
     \nextdef
-    & \hspace{-1cm}\fun{checkScriptData} \in \Tx \to (\ScriptPurpose \times \ScriptHash) \to \Bool \\
-    & \hspace{-1cm}\fun{checkScriptData}~\var{tx}~(\var{sp},\var{h})~=~ \forall s, (h\mapsto s) \in \fun{txscripts}~(\fun{txwits}~tx),\\
-    & (s \in \ScriptPhTwo~\Rightarrow \fun{txrdmrs}~tx~sp \neq \{\}) \\
-    \nextdef
     & \hspace{-1cm}\fun{languages} \in \TxWitness \to \powerset{\Language} \\
     & \hspace{-1cm}\fun{languages}~\var{txw}~=~
       \{\fun{language}~s \mid s \in \range (\fun{txscripts}~{txw}) \cap \ScriptPhTwo\}
@@ -886,8 +878,8 @@ \subsection{Witnessing}
       \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 sph \in \fun{scriptsNeeded}~\var{utxo}~\var{tx},~ \fun{checkScriptData}~tx~sph} \\
-      \hldiff{\ \forall~(\var{ptr}\mapsto \wcard)~\in~\fun{txrdmrs}~tx, ~ \var{ptr}~\in~\{~\fun{rdptr}~txb~sp~
+      \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 \}}
       \\~\\