utxo.tex

\section{UTxO}
\label{sec:utxo}

\begin{figure*}[htb]
  \emph{Functions}
  %
  \begin{align*}
    & \fun{isTwoPhaseScriptAddress} : \Tx \to \Addr \to \Bool \\
    & \fun{isTwoPhaseScriptAddress}~tx~a = \\
      &\quad\begin{cases}
        \True  & a \in \AddrScr \land \fun{validatorHash}~a \mapsto s \in \fun{txscripts} (\fun{txwits}~tx) \land s \in \ScriptPhTwo \\
        \False & \text{otherwise}
      \end{cases}
                 \nextdef
    & \fun{totExUnits} : \Tx \to \ExUnits \\
    & \fun{totExUnits}~\var{tx} = \sum_{r \in \fun{txrdmrs}~tx} \fun{exunits}~r
    \nextdef
    & \fun{feesOK} : \PParams \to \Tx \to \UTxO \to \Bool  \\
    & \fun{feesOK}~\var{pp}~tx~utxo~= \\
    &~~      \minfee{pp}~{tx} \leq \txfee{txb} \wedge (\fun{txrdmrs}~tx \neq \emptyset \Rightarrow \\
    &~~~~~~(\forall (a, \wcard, \wcard) \in \fun{range}~(\fun{collateral}~{txb} \restrictdom \var{utxo}), a \in \AddrVKey) \\
    &~~~~~~\wedge~ \fun{isAdaOnly}~\var{balance} \\
    &~~~~~~\wedge~ \var{balance}*100 \geq \txfee{txb} * (\fun{collateralPercent}~pp) \\
    &~~~~~~\wedge~ \fun{collateral}~{tx} \neq \emptyset) \\
    &~~      \where \\
    & ~~~~~~~ \var{txb} = \txbody{tx} \\
    & ~~~~~~~ \var{balance} = \fun{ubalance}~(\fun{collateral}~{txb} \restrictdom \var{utxo})
    \nextdef
    & \fun{cbalance} : \UTxO \to \Coin \\
    & \fun{cbalance}~\var{utxo} =  \fun{valueToCoin}~(\fun{ubalance}~\var{utxo})
    \nextdef
    & \fun{txscriptfee} : \Prices \to \ExUnits \to \Coin \\
    & \fun{txscriptfee}~(pr_{mem}, pr_{steps})~ (\var{mem, steps})
    = \fun{ceiling}~(\var{pr_{mem}}*\var{mem} + \var{pr_{steps}}*\var{steps})
    \nextdef
    &\fun{minfee} : \PParams \to \Tx \to \Coin \\
    &\fun{minfee}~\var{pp}~\var{tx} = \\
    &~~(\fun{a}~\var{pp}) \cdot \fun{txSize}~\var{tx} + (\fun{b}~\var{pp}) +
    \hldiff{\fun{txscriptfee}~(\fun{prices}~{pp})~(\fun{totExunits}~(\fun{txbody}~{tx}))}
  \end{align*}
  \caption{Functions related to fees and collateral}
  \label{fig:functions:utxo}
\end{figure*}

We have added or changed several functions that deal with fees and collateral as shown in Figure \ref{fig:functions:utxo}.

\begin{itemize}
  \item $\fun{isTwoPhaseScriptAddress}$ is a predicate that checks
  whether an address is used as a script address with a phase-2
  script.
  \item $\fun{totExunits}$ calculates the total $\ExUnits$ in a transaction by summing
  the per-script units stored in the indexed redeemer structure
  \item The predicate $\fun{feesOK}$ checks whether the transaction is
  paying the necessary fees, and that it does it correctly. That is, it checks that:
  \begin{enumerate}[label=({\roman*})]
    \item the fee amount that the transaction states it is paying suffices to cover
    the minimum fee that the transaction is obligated to pay; and if the transaction uses phase-2 scripts, that
    \item the collateral inputs refer only to UTxOs with key-hash addresses;
    \item all the collateral inputs refer to UTxOs containing Ada only and no other kinds of token; and
    \item the collateral provided is sufficient to cover the percentage of the
    transaction fee amount specified by the protocol parameter $\fun{collateralPercent}$
    \item the set of collateral inputs is non-empty
  \end{enumerate}
  Note that checking that a transaction is carrying redeemers is the most simple way to
  check that it is carrying phase-2 scripts. A separate check is done in the rule prior to
  calling the $\fun{feesOK}$ function that ensure that this is the case.
  \item $\fun{txscriptfee}$ calculates the fee that a transaction must pay for script
  execution based on the amount of $\ExUnits$ it has budgeted, and the prices in the current protocol parameters
  for each component of $\ExUnits$. The prices are expressed as rational numbers,
  so we take the ceiling of the result of the calculation to get an integer-valued $\Coin$.
  \item The minimum fee calculation, $\fun{minfee}$, includes the script
  fees that the transaction is obligated to pay in order to run its scripts.
\end{itemize}

Note that when creating a transaction, the wallet is responsible for
determining the fees. Thus, it also has to execute the phase-2 scripts
and include the fees for their execution.

\subsection{Combining Scripts with Their Inputs}
\label{sec:scripts-inputs}

Figure~\ref{fig:functions:script1} shows the functions that are needed to
retrieve all the data that is relevant to Plutus script validation.
These include:

\begin{itemize}
\item $\mathsf{EI}$ is a global constant needed to compute the current system time.
\item $\mathsf{SysSt}$ is another global constant needed to compute the system time.
\item $\UTCTime$ is the system time (UTC time zone)
\item
  $\ScriptPurpose$ is a sum type of all parts of a transaction that may
  require a script witness to validate. Note that this contains the data
  (eg. a certificate $c \in \fun{txcerts}~{txb}$,
  or a transaction input $tin \in \fun{txcerts}~{txb}$) of the item being validated,
  not just a tag indicating the type.
\item
  $\fun{indexof}$ is a helper function that finds the index of a given certificate, value, input, or
  withdrawal in a list, finite map, or set of such objects. The implementation is not given
  directly, but we give a high-level description of how it relies on the underlying ordering.
  For each of these, it computes the index as follows :
  \begin{itemize}
    \item certificates in the $\DCert$ list are indexed in the order in which they arranged
    in the (full, unfiltered) list of certificates inside the transaction
    \item the index of a reward account $\var{ract}$ in the reward withdrawals map is
    the index of $\var{ract}$ as a key in the (unfiltered) map. The keys of the $\Wdrl$
    map are arranged in the order defined on the $\RewardAcnt$ type, which is a lexicographical
    (abbrv. lex) order
    on the pair of the $\Network$ and the $\Credential$.
    \item the set of inputs is an ordered set (according to the order defined on
    the type $\TxIn$) - this also is the order in which the elements of the set are
    indexed (lex order on the pair of $\TxId$ and $\Ix$). All inputs of a transaction
    are included in the set being indexed (not just the ones that point to a Plutus script UTxO)
    \item the set of policy IDs is ordered according to the order defined on $\PolicyID$ (lex).
    The index of a $\PolicyID$ in this set of policy IDs is computed according to this order.
    Note that at the use site, the set of policy IDs passed to $\fun{indexof}$ is
    the (unfiltered) domain of the $\Value$ map in the $\fun{mint}$ field of the transaction.
  \end{itemize}
  Note that in all the orderings above, long and short lex are one in the same, since
  for each of the ordered types, all the terms of that type have the same length.
\item
  $\fun{indexedRdmrs}$ indexes the pair of a redeemer and an $\ExUnits$ value
  for a given script by its script purpose (eg. the input, or certificate, etc.),
  and $\Nothing$ if no associated data is found.
  It uses the script purpose to generate the $\RdmrPtr$ key,
  then find the corresponding entry in the redeemer structure.
  \item $\fun{rdptr}$ builds a redeemer pointer from a script purpose by
  setting the tag according to the type of the script purpose, and the index
  according to the placement of script purpose inside its container (ie. by using $\fun{indexof}$)
\end{itemize}


\begin{figure}[htb]
  \emph{Global Constants}
  %
  \begin{equation*}
    \begin{array}{r@{~\in~}l@{}lr}
      \mathsf{EI}
      & \EpochInfo
      & \text{Alonzo epoch info} \\
      \mathsf{SysSt}
      & \SystemStart
      & \text{System start time}
    \end{array}
  \end{equation*}
  \emph{Abstract Types}
  %
  \begin{equation*}
    \begin{array}{r@{~\in~}l@{}lr}
      \var{tm}
      & \UTCTime
      & \text{System time}
    \end{array}
  \end{equation*}
  %
  \emph{Derived types}
  %
  \begin{equation*}
    \begin{array}{r@{~\in~}l@{\qquad=\qquad}lr}
      \var{sp}
      & \ScriptPurpose
      & \PolicyID \uniondistinct \TxIn \uniondistinct \AddrRWD \uniondistinct \DCert
%      & \text{item the script is validated for}
    \end{array}
  \end{equation*}
  %
  \emph{Abstract functions}
  \begin{align*}
    &\fun{indexOf} : \DCert \to \seqof{\DCert} \to \Ix^?\\
    &\fun{indexOf} : \AddrRWD \to \Wdrl \to \Ix^?\\
    &\fun{indexOf} : \TxIn \to \powerset{\TxIn} \to \Ix^?\\
    &\fun{indexOf} : \PolicyID \to \powerset{\PolicyID} \to \Ix^?
  \end{align*}
  %
  \emph{Indexing functions}
  \begin{align*}
    &\fun{indexedRdmrs} : \Tx \to \ScriptPurpose \to (\Redeemer~\times~\ExUnits)^?\\
    &\fun{indexedRdmrs}~tx~sp =
      \begin{cases}
        r        & (\fun{rdptr}~txb~sp)~ \mapsto r \in \fun{txrdmrs}~(\fun{txwits}~{tx}) \} \\
        \Nothing & \text{otherwise}
      \end{cases} \\
    & ~~\where \\
    & ~~\quad \var{txb} = \txbody{tx}
    \nextdef
    &\fun{rdptr} :\TxBody~\to~\ScriptPurpose~ \to~ \RdmrPtr^? \\
    &\fun{rdptr}~txb~sp~ =
      \begin{cases}
        (\mathsf{Cert},\fun{indexOf}~\var{sp}~(\fun{txcerts}~{txb}))   & \var{sp} \in \DCert \\
        (\mathsf{Rewrd},\fun{indexOf}~\var{sp}~(\fun{txwdrls}~{txb}))   & \var{sp} \in \AddrRWD \\
        (\mathsf{Mint},\fun{indexOf}~\var{sp}~(\dom (\fun{mint}~{txb})))    & \var{sp} \in \PolicyID \\
        (\mathsf{Spend},\fun{indexOf}~\var{sp}~(\fun{txinputs}~{txb})) & \var{sp} \in \TxIn
      \end{cases}
  \end{align*}
  \caption{Indexing script and data objects}
  \label{fig:functions:script1}
\end{figure}


\subsection{Plutus Script Validation}
Figure~\ref{fig:defs:functions-valid} shows the abstract functions that are used for script validation.
In this figure, the function $\fun{txInfo}$, which creates a summary of the transaction
and ledger state as a $\TxInfo$, is defined in Section \ref{sec:txinfo}, as is the $\TxInfo$
type itself.
The function $\fun{valContext}$, also defined in \ref{sec:txinfo}, constructs the
validation context from the $\TxInfo$ summary.

\begin{itemize}
\item $\fun{epochInfoSlotToUTCTime}$ translates a slot number to system time if possible.
This translation is implemented by the consensus algorithm (not the ledger), and requires
two additional parameters to do this. Note that this does not depend on the clock of the node.

If it is not possible to do this translation, $\Nothing$ is returned.
The reason it may not be possible to translate is that the slot number
is too far in the future for the system to accurately
predict the exact time to which it refers.

\item
  $\fun{runPLCScript}$ validates Plutus scripts. It takes the following
  arguments:
  \begin{itemize}
  \item A cost model, that is used to calculate the $\ExUnits$ that are needed for script execution;
  \item A script to execute;
  \item the execution unit budget; and
  \item A list of terms of type $\Data$ that will be passed to the script.
  \end{itemize}
  It outputs the validation result.
  Note that script execution stops if the full budget has been spent before validation is complete.
  It is left abstract because it is implemented as part of the phase-1 script interpreter, not the ledger.
  The interpreter called depends on the language of the script.
\end{itemize}


\textbf{Slot to time translation.}
One of the inputs to scripts is the transaction validity interval (recall here that
they do not actually see the current slot number). The length of a
slot may change in a future era. In this case, for a script written in a previous
era, if we were to pass the transaction validity interval expressed as slot numbers,
we get that

\begin{itemize}
  \item the script logic is expressed in terms of slot numbers
  which likely assume the slot length of the era in which it was created
  \item the slot numbers in the validity interval of the transaction are used
  assuming slot length of the current era
\end{itemize}

Therefore, the slot numbers inside the contract and the slot numbers in the transaction
map differently onto points in time. The ledger does not have access to data (or conversion functions)
that is needed to convert transaction validity interval slots numbers to slots numbers
that correspond to the contracts world view. To address this, we decided to pass
phase-2 contracts (in all languages and all eras) the system time instead of slot numbers.
The conversion function is implemented by consensus (see~\cite{cardano_consensus}),
which has the information to do this correctly for

\begin{itemize}
  \item all slots prior to the current slot
  \item a number of slots after the current slot (this number is determined by
  the consensus's forecast window)
\end{itemize}

Note that because of this potential slot length change issue, Plutus scripts will
not receive any information in terms of slot numbers (no phase-1 scripts, no
validity intervals as slots, and not the current slot). Phase-1 timelock scripts
continue to operate on validity interval data expressed as slot numbers, and are
therefore vulnerable to the consequences of changing the slot length.

\textbf{Validation context construction.}
  As additional phase-2 scripting languages become supported in the future, scripts of different
  languages may expect different (or differently structured) transaction and ledger data summary.
  The $\fun{txInfo}$ function will be implemented differently
  for each new language. So, the construction is
  dependent on both the language of the script being validated and the ledger/transaction structure
  of the current era.

  In order to ensure that running scripts of all script languages is supported indefinitely across
  future eras, the $\fun{txInfo}$ function must be total.
  Recall here that while \emph{running} all scripts must be supported across
  all future ledger changes,
  it is not a requirement that every script must \emph{validate} within the context of some transaction.

  The $\fun{txInfo}$ output is computed once for the whole transaction. The output of the function
  $\fun{valContext}$ is computed separately for each script purpose.
  The script purpose is passed to it
  to allow the script to reference itself via its hash, and to be aware of what it is validating.

\textbf{Know your contract arguments.}
  A Plutus validator script may receive either a list of three terms of type $\Data$, in case it validates the spending of script outputs
  or two terms (redeemer and context, with no datum), for all other uses.
  Script authors must keep this in mind when writing scripts, since the ledger call to the interpreter is oblivious to what
  arguments are required.

  The following is a summary of what arguments are required for what scripts:
  \begin{itemize}
    \item Datum objects are required for all output-locking phase-2 scripts. That is, a
    phase-2 script-locked output that does not include a datum hash is unspendable.
    \item Non-output locking scripts do not expect datum objects - that is, it is not possible to pass
    a datum to a script used for another purpose (certificate, etc.).
    \item Redeemers are required for all phase-2 scripts.
  \end{itemize}

   If a transaction carrying a Plutus script is missing any inputs required
   to run a script, we have specified this to be a phase 1
   ledger failure, and the script is never run (even if its code does not look at
   the missing input). The reason for this approach is that
   not passing all inputs results in a script never actually getting run,
   rather than running and failing.

\begin{figure*}[htb]
  \emph{Abstract Script Validation Functions}
  %
  \begin{align*}
     &\fun{epochInfoSlotToUTCTime} : \EpochInfo \to \SystemStart \to \Slot \to \UTCTime^? \\
     &\text{Translate slot number to system time or fail} \\~\\
     &\fun{runPLCScript} : \CostMod \to \ScriptPlutus \to \ExUnits \to \seqof{\Data} \to
     \IsValid \\
     &\text{Validate a Plutus script, taking resource limits into account}
  \end{align*}
  %
  \emph{Notation}
  %
  \begin{align*}
    \llbracket \var{script_v} \rrbracket_{\var{cm},\var{eu}}~\var{d}
    &=& \fun{runPLCScript}~{cm} ~\var{script_v}~\var{eu}~\var{d}
  \end{align*}
  \caption{Script Validation, cont.}
  \label{fig:defs:functions-valid}
\end{figure*}

Figure \ref{fig:functions:script2} contains the functions used to
match scripts with their corresponding inputs and pass them to the
evaluator.

\begin{itemize}
  \item $\fun{getDatum}$ looks for a datum associated with a given script purpose. Note that
  only an $\TxIn$-type script purpose can result in finding an associated datum hash.
  If no datum is found, an empty list is returned. A list containing the found datum
  is returned otherwise.

  \item $\fun{collectTwoPhaseScriptInputs}$ builds a list of scripts, paired with their
  inputs. Specifically, each tuple in the list contains :

  \begin{itemize}
  \item the script, only if it is a phase-2 one;

  \item a list of the following script arguments, in this order:

  \begin{itemize}
    \item the hash of the required datum, if any (returned by the $\fun{getDatum}$ function,
    wrapped in a list type instead of a $\Data^?$ type).

    \item a redeemer, returned as the first term of the pair by the $\fun{indexedRdmrs}$ function.
    and an $\ExUnits$ amount. We are assuming this value is not $\Nothing$ here
    because that must have already been checked by the UTXOW rule.

    \item the validation context, built by the $\fun{valContext}$ function using
    the transaction summary built by $\fun{txInfo}$, together with the current item being validated;
  \end{itemize}

  \item an $\ExUnits$ amount, which is the second term of the pair returned by the $\fun{indexedRdmrs}$ function.

  \item the cost model for $\PlutusVI$, specified in the protocol parameters
  \end{itemize}

  \item $\fun{evalScripts}$ evaluates a whole list of scripts. For $\PlutusVI$ scripts,
  it evaluates them paired with all their
  inputs by calling the phase-2 script validator function, $\fun{runPLCScript}$ (see
  \ref{sec:txinfo} for details).
  For phase-1 (timelock) scripts, it calls $\fun{evalTimelock}$. This case
  is unused though, as
  the list of scripts and inputs that gets passed to the this function is constructed
  to contain only Plutus scripts. So, phase-1 scripts do not get evaluated twice.
\end{itemize}

Note that no ``checks'' are performed within these functions (though they may be,
in the implementation).
Missing validators, missing inputs, incorrect hashes, the wrong type of script etc,
are caught during the application of the UTXOW rule (before these functions are ever applied).

\begin{figure}[htb]
  \begin{align*}
    & \fun{getDatum} : \Tx \to \UTxO \to \ScriptPurpose \to \seqof{\Datum} \\
    & \fun{getDatum}~{tx}~{utxo}~{sp} = 
      \begin{cases}
        [\var{d}] & \var{sp} \mapsto (\_, \_, h_d) \in \var{utxo}, \var{h_d}\mapsto \var{d} \in \fun{txdats}~(\fun{txwits}~tx) \\
        \epsilon  & \text{otherwise}
      \end{cases}
    \nextdef
    & \fun{collectTwoPhaseScriptInputs} : \EpochInfo \to \SystemStart \to \PParams \to \Tx \to \UTxO \to \\
    & ~~~~ \seqof{(\Script \times \seqof{\Data} \times \ExUnits \times \CostMod)} \\
    & \fun{collectTwoPhaseScriptInputs} ~\var{ei}~\var{sysSt}~\var{pp}~\var{tx}~ \var{utxo}  =  \\
    & ~~\fun{toList} \{ (\var{script}, (\fun{getDatum}~tx~utxo~sp ; \var{rdmr};\fun{valContext}~\var{txinfo}~\var{sp}), \var{eu}, \var{cm}) \mid \\
    & ~~~~(\var{sp}, \var{scriptHash}) \in \fun{scriptsNeeded}~{utxo}~{(\txbody{tx})}, \\
    & ~~~~\var{scriptHash}\mapsto \var{script}\in \fun{txscripts}~(\fun{txwits}~tx), \\
    & ~~~~(\var{rdmr}, \var{eu}) := \fun{indexedRdmrs}~tx~sp, \\
    & ~~~~\fun{language}~{script} \mapsto \var{cm} \in \fun{costmdls}~{pp}, \\
    & ~~~~\var{script} \in \ScriptPhTwo \} \\
    & \where \\
    & ~~~~~~~ \var{txinfo} = \fun{txInfo}~\var{ei}~\var{sysSt}~(\fun{language}~{script})~{pp}~\var{utxo}~\var{tx}
    \nextdef
    & \fun{evalScripts} : \Tx \times \seqof{(\Script \times \seqof{\Data} \times \ExUnits \times \CostMod)} \to \IsValid \\
    & \fun{evalScripts}~\var{tx}~\epsilon = \True \\
    & \fun{evalScripts}~\var{tx}~((\var{sc}, \var{d}, \var{eu}, \var{cm});\Gamma) = \\
      & \begin{cases}
        \llbracket sc \rrbracket_{cm,\var{eu}} d \land \fun{evalScripts}~\var{tx}~\Gamma & \var{sc}\in\ScriptPlutus \\
        \fun{evalTimelock}~\var{tx}~\var{sc} \land \fun{evalScripts}~\var{tx}~\Gamma & \var{sc}\in\ScriptPhOne
      \end{cases}
  \end{align*}
  \caption{Scripts and their arguments}
  \label{fig:functions:script2}
\end{figure}

\subsection{Two-Phase Transaction Validation for Phase-2 Scripts}
\label{sec:two-phase}

Transactions are validated in two phases:
the first phase consists of every aspect of transaction validation apart from executing the phase-2 scripts; and
the second phase involves actually executing those scripts.
This ensures that users pay for the computational resources that are needed to validate phase-2 scripts, even
if script validation fails. %
In order to handle script execution, an additional transition system is used, called UTXOS.
It performs the appropriate UTxO state changes, based on the
value of the $\IsValid$ tag, which it checks using the $\fun{evalScripts}$ function.

In general, there is no way to check \emph{a-priori} that the budget that has been supplied is sufficient for the transaction.
This can only be done by actually running the scripts. From the perspective of the ledger, there is no difference
between a script that exhausts the $\ExUnits$ budget during validation, and one that fails to validate.

\textbf{Transaction integrity and charging for failing scripts.}
If a transaction contains a failing script, the only change to the ledger that is made
is that the collateral is collected into the fee pot. It is important to note here
that it can be the case that the only signatures on a transaction are those
of the keys for the collateral UTxOs (but this must include at least one signature).

The implication of this is that the collateral key owners may be the only
users that attest to the integrity of the data in the body of the transaction. These
same key owners, however, are also the only users who stand to lose money if the
transaction is modified in some way that results in phase-2 failure.
Transactions with the same body will necessarily have the same outcome of phase-2
script validation (we give the details in the deterministic script validation property, \ref{prop:fixed-inputs}).
Therefore, signing the body ensures any modification to any part of a transaction (including
witnesses, etc.) or update to the ledger state that affect the transaction's validity will result in a phase-1 failure,
and no collateral collected. The implication of this is that
the collateral-locking keys have full control over the outcome of phase-2 validation.


\textbf{The $\IsValid$ Tag. }
It is always in the interest of the slot leader to have the new block validate,
and for it to contain only valid transactions. This motivates the
slot leader to:

\begin{enumerate}
  \item Correctly apply the $\IsValid$ tag;
  \item Include all transactions that validate within the block,
  \textit{even when there is a 2nd phase script validation failure};
  \item Exclude any transactions that are phase-1 invalid
\end{enumerate}

One important reason for adding the validation tag
to a transaction is that re-applying blocks will not require repeat
execution of scripts in the transactions inside a block, which would increase execution costs.
In fact, when replaying
blocks, all the witnessing information can be thrown away.

\subsection{The UTXOS transition system}
\label{sec:utxo-state-trans}

We have defined a separate transition system, UTXOS, to represent the two distinct
UTxO state changes: i) when all the scripts in a transaction validate; and
ii) when at least one fails to validate. Its transition types
are identical to the UTXO transition (Figure
\ref{fig:ts-types:utxo-scripts}).

\begin{figure}[htb]
  \emph{State transitions}
  \begin{equation*}
    \_ \vdash
    \var{\_} \trans{utxos}{\_} \var{\_}
    \subseteq \powerset (\UTxOEnv \times \UTxOState \times \Tx \times \UTxOState)
  \end{equation*}
  %
  \caption{UTxO script state update types}
  \label{fig:ts-types:utxo-scripts}
\end{figure}

There are two rules, corresponding to the two possible state changes of the
UTxO state in the UTXOS transition system (Figure~\ref{fig:rules:utxo-state-upd}).
%
In both cases, the $\fun{evalScripts}$ function is called upon to verify that the $\IsValid$
tag has been applied correctly. The function $\fun{collectTwoPhaseScriptInputs}$ is used to build
the input list $\var{sLst}$ for the $\fun{evalScripts}$ function.
%
The first rule
applies when the validation tag is $\True$.
In this case, the states of the UTxO, fee
  and deposit pots, and updates are updated exactly as in the current Shelley
  ledger spec.
%
  The second rule
  applies when the validation tag is $\False$.
  In this case, the UTxO state changes as follows:

  \begin{enumerate}
    \item All the
    UTxO entries corresponding to the collateral inputs are removed;

    \item The sum total of the value of the collateral UTxO entries
    is added to the fee pot.
  \end{enumerate}


\begin{figure}[htb]
  \begin{equation}
    \inference[Scripts-Yes]
    {
    \var{txb}\leteq\txbody{tx} &
    \var{sLst} := \fun{collectTwoPhaseScriptInputs}~\mathsf{EI}~\mathsf{SysSt}~\var{pp}~\var{tx}~\var{utxo}
    \\~\\
    {
      \begin{array}{r}
        \var{slot} \\
        \var{pp} \\
        \var{genDelegs} \\
      \end{array}
    }
    \vdash \var{pup} \trans{\hyperref[fig:rules:update]{ppup}}{\fun{txup}~\var{tx}} \var{pup'}
    \\~\\
    \var{refunded} \leteq \keyRefunds{pp}{txb}
    \\
    \var{depositChange} \leteq
      \fun{totalDeposits}~{pp}~\var{poolParams}~(\txcerts{txb})~-~\var{refunded}
    \\~\\
    \fun{isValid}~\var{tx} = \fun{evalScripts}~\var{tx}~\var{sLst} = \True
    }
    {
    \begin{array}{l}
      \var{slot}\\
      \var{pp}\\
      \var{poolParams}\\
      \var{genDelegs}\\
    \end{array}
      \vdash
      \left(
      \begin{array}{r}
        \var{utxo} \\
        \var{deposits} \\
        \var{fees} \\
        \var{pup} \\
      \end{array}
      \right)
      \trans{utxos}{tx}
      \left(
      \begin{array}{r}
        \varUpdate{\var{(\txins{txb} \subtractdom \var{utxo}) \cup \outs{txb}}}  \\
        \varUpdate{\var{deposits} + \var{depositChange}} \\
        \varUpdate{\var{fees} + \txfee{txb}} \\
        \varUpdate{\var{pup'}} \\
      \end{array}
      \right) \\
    }
  \end{equation}
  \begin{equation}
    \inference[Scripts-No]
    {
    \var{txb}\leteq\txbody{tx} &
    \var{sLst} := \fun{collectTwoPhaseScriptInputs}~\mathsf{EI}~\mathsf{SysSt}~\var{pp}~\var{tx}~\var{utxo}
    \\
    ~
    \\
    \fun{isValid}~\var{tx} = \fun{evalScripts}~\var{tx}~\var{sLst} = \False
    }
    {
    \begin{array}{l}
      \var{slot}\\
      \var{pp}\\
      \var{poolParams}\\
      \var{genDelegs}\\
    \end{array}
      \vdash
      \left(
      \begin{array}{r}
        \var{utxo} \\
        \var{deposits} \\
        \var{fees} \\
        \var{pup} \\
      \end{array}
      \right)
      \trans{utxos}{tx}
      \left(
      \begin{array}{r}
        \varUpdate{\var{\fun{collateral}~{txb} \subtractdom \var{utxo}}}  \\
        \var{deposits} \\
        \varUpdate{\var{fees} + \fun{cbalance}~(\fun{collateral}~{txb}\restrictdom \var{utxo})} \\
        \var{pup} \\
      \end{array}
      \right)
    }
  \end{equation}
  \caption{State update rules}
  \label{fig:rules:utxo-state-upd}
\end{figure}

Figure \ref{fig:rules:utxo-shelley} shows the $\type{UTxO-inductive}$
transition rule for the UTXO transition type.
This rule has the following changes:

\begin{enumerate}
  \item The transaction pays fees and supplies collateral Ada correctly, as defined above;

  \item The end of the transaction validity interval is translatable into
  system time (ie. within the consensus's forecast window). This is checked
  by $\fun{epochInfoSlotToUTCTime}$, which returns $\Nothing$ if the end slot is outside.
  Note that we do not need to check that the start slot can be converted to
  time, because all pasts slots can be converted into time correctly.

  \item $\fun{coinsPerUTxOWord}$ is now a protocol parameter explicitly, the
  $\fun{utxoEntrySize}$ calculation is defined differently than for ShelleyMA
  (see Section~\ref{sec:value-size})

  \item $\fun{maxValSize}$ is now also a protocol parameter (not a constant).
  It represents a size (in bytes) of the total transaction
  size that the size of a $\Value$ in an output can be. Otherwise, this check is
  the same as in ShelleyMA.

  \item The network ID field in the transaction body must match the
  network ID constant

 \item The execution unit budget for a transaction is within the maximum
  permitted number of units for a transaction;

  \item The number of maximum allowed collateral inputs is not exceeded

  \item The UTXOS state transition is valid (this is the transition that runs the
  phase-2 scripts)
\end{enumerate}

The resulting state transition is defined entirely by the application of the
UTXOS rule.

\begin{figure}[htb]
  \begin{equation}\label{eq:utxo-inductive-shelley}
    \inference[UTxO-inductive]
    {
      \var{txb}\leteq\txbody{tx} &
      \fun{ininterval}~\var{slot}~(\fun{txvldt}~{txb}) &
      \hldiff{\var{(\wcard, i_f)}\leteq\fun{txvldt}~{tx}} \\~\\
      \hldiff{\Nothing \notin \{\fun{txrdmrs}~\var{tx}, i_f\} \Rightarrow \fun{epochInfoSlotToUTCTime}~\mathsf{EI}~\mathsf{SysSt}~i_f \neq \Nothing} \\
      \txins{txb} \neq \emptyset
      & \hldiff{\fun{feesOK}~pp~tx~utxo}
      & \txins{txb}~\cup~\fun{collateral}~{txb}~ \subseteq~ \dom \var{utxo}
      \\
      \consumed{pp}{utxo}{txb} = \produced{pp}{poolParams}~{txb}
      \\~\\
      \mathsf{adaID}\notin \supp {\fun{mint}~tx} \\~\\
      \forall txout \in \txouts{txb}, \\
      \fun{getValue}~txout \geq \fun{inject}~(\hldiff{\fun{utxoEntrySize}~{txout} * \fun{coinsPerUTxOWord}~pp)} \\~
      \\
      \forall txout \in \txouts{txb},\\
      \fun{serSize}~(\fun{getValue}~txout) \leq \hldiff{\fun{maxValSize}~pp} \\~
      \\
      \forall (\wcard\mapsto (a,~\wcard)) \in \txouts{txb}, a \in \AddrBS \Rightarrow \fun{bootstrapAttrsSize}~a \leq 64 \\
      \forall (\wcard\mapsto (a,~\wcard)) \in \txouts{txb}, \fun{netId}~a = \NetworkId
      \\
      \forall (a\mapsto\wcard) \in \txwdrls{txb}, \fun{netId}~a = \NetworkId \\
      \hldiff{(\fun{txnetworkid}~\var{txb} = \NetworkId) \vee (\fun{txnetworkid}~\var{txb} = \Nothing)}
      \\~\\
      \fun{txsize}~{tx}\leq\fun{maxTxSize}~\var{pp} \\~\\
      \hldiff{\fun{totExunits}~{tx} \leq \fun{maxTxExUnits}~{pp}} &  \hldiff{\| \fun{collateral}~{tx} \| \leq \fun{maxCollateralInputs}~{pp}}
      \\
      ~
      \\
      \hldiff{{
        \begin{array}{c}
          \var{slot}\\
          \var{pp}\\
          \var{poolParams}\\
          \var{genDelegs}\\
        \end{array}
      }
      \vdash
      {
        \left(
          \begin{array}{r}
            \var{utxo} \\
            \var{deposits} \\
            \var{fees} \\
            \var{pup}\\
          \end{array}
        \right)
      }
      \trans{utxos}{\var{tx}}
      {
        \left(
          \begin{array}{r}
            \var{utxo'} \\
            \var{deposits'} \\
            \var{fees'} \\
            \var{pup'}\\
          \end{array}
        \right)
      }
    }}
    {
      \begin{array}{l}
        \var{slot}\\
        \var{pp}\\
        \var{poolParams}\\
        \var{genDelegs}\\
      \end{array}
      \vdash
      \left(
      \begin{array}{r}
        \var{utxo} \\
        \var{deposits} \\
        \var{fees} \\
        \var{pup}\\
      \end{array}
      \right)
      \trans{utxo}{tx}
      \left(
      \begin{array}{r}
        \varUpdate{\var{utxo'}}  \\
        \varUpdate{\var{deposits'}} \\
        \varUpdate{\var{fees'}} \\
        \varUpdate{\var{pup'}}\\
      \end{array}
      \right)
    }
  \end{equation}
  \caption{UTxO inference rules}
  \label{fig:rules:utxo-shelley}
\end{figure}

\subsection{Witnessing}
\label{sec:wits}

Because of two-phase transaction validation, phase-2 script validation is not part of phase one of transaction witnessing
(it is done in phase 2, once the rest of the transaction is validated).
However, phase-1 script validation does remain part of transaction witnessing.
When witnessing a transaction in phase one, we therefore need to validate only the phase-1 scripts.

We construct the following helper functions :

\begin{itemize}
  \item $\fun{witsVKeyNeeded}$ is a Shelley function adjusted to include
  keys that are specified in the $\fun{reqSignerHashes}$ field of the transaction,
  as well as keys locking the UTxOs to which the collateral inputs of the transaction point.

  \item $\fun{scriptsNeeded}$ assembles the all the $\ScriptPurpose$ terms
  for validation of every transaction action that requires script validation,
  paired with the hashes of corresponding the witnessing scripts.
  This function collects hashes of both phase-1 and phase-2 scripts.

  \item $\fun{languages}$ returns the set of (phase-2) script languages
  of all the scripts included in the transaction
\end{itemize}

\begin{figure}[htb]
  \begin{align*}
    & \hspace{-0.8cm}\fun{witsVKeyNeeded} : \UTxO \to \Tx \to (\KeyHashGen\mapsto\VKey) \to
      \powerset{\KeyHash} \\
    &  \hspace{-0.8cm}\fun{witsVKeyNeeded}~\var{utxo}~\var{tx}~\var{genDelegs} = \\
    & ~~\{ \fun{paymentHK}~a \mid i \mapsto (a, \wcard) \in \var{utxo},~i\in\fun{txinsVKey}~{tx} \cup \hldiff{\fun{collateral}~{tx}} \} \\
    \cup & ~~
           \{\fun{stakeCred_r}~a\mid a\mapsto \wcard \in \AddrRWDVKey
      \restrictdom \txwdrls{tx}\}\\
    \cup & ~~(\AddrVKey \cap \fun{certWitsNeeded}~{tx}) \\
    \cup & ~~\fun{propWits}~(\fun{txup}~\var{tx})~\var{genDelegs} \\
    \cup & ~~\bigcup_{\substack{c \in \txcerts{tx} \\ ~c \in\DCertRegPool}} \fun{poolOwners}~{c} \\
    \cup & ~~\hldiff{\fun{reqSignerHashes}~\var{tx}}
    \nextdef
    & \hspace{-1cm}\fun{scriptsNeeded} : \UTxO \to \TxBody \to \powerset (\ScriptPurpose \times \ScriptHash) \\
    & \hspace{-1cm}\fun{scriptsNeeded}~\var{utxo}~\var{txb} = \\
    & ~~\{ (\var{i}, \fun{validatorHash}~a) \mid i\in\fun{txinsScript}~{(\fun{txins~\var{txb}})}~{utxo}, i \mapsto (a, \wcard, \wcard) \in \var{utxo} \} \\
    \cup & ~~\{ (\var{a}, \fun{stakeCred_{r}}~\var{a}) \mid a \in \dom (\AddrRWDScr
           \restrictdom \fun{txwdrls}~\var{txb}) \} \\
    \cup & ~~\{ (\var{cert}, \var{c}) \mid \var{cert} \in (\DCertDeleg \cup \DCertDeRegKey)\cap\fun{txcerts}~txb, \\
    & ~~~~~~\var{c} \in \cwitness{cert} \cap \AddrScr\} \\
      \cup & ~~\{ (\var{pid}, \var{pid}) \mid \var{pid} \in \supp~(\fun{mint}~\var{txb}) \}
    \nextdef
    & \hspace{-1cm}\fun{languages} : \TxWitness \to \powerset{\Language} \\
    & \hspace{-1cm}\fun{languages}~\var{txw} = 
      \{\fun{language}~s \mid s \in \range (\fun{txscripts}~{txw}) \cap \ScriptPhTwo\}
  \end{align*}
  \caption{UTXOW helper functions}
  \label{fig:functions-witnesses}
\end{figure}

We have made the following changes and additions to the UTXOW preconditions:

\begin{itemize}

\item All the phase-1 scripts in the transaction validate;

\item The transaction contains exactly those scripts that are required for witnessing and no
additional ones;

    \item The datums included in the witnesses contain all the datums required for
    validating in phase 2. That is,
    datums for all output-locking phase-2 scripts for the payment credentials of the addresses of the
    UTxOs the transaction is spending must have attached datum objects. This check will also fail if
    the datum hash fields of such UTxOs are $\Nothing$, as $\Nothing$ is not a
    hash of a datum (and therefore is not a key of the $\DataHash$-indexed map).

    \item The only datums included in a transaction have hashes that are either in a UTxO
    corresponding to a transaction input, or in a transaction output. The
    output datums are for communication only, and are therefore optional, hence
    the use of subset equality. No additional
    datums are permitted.

    \item For every item that needs to be validated by a phase-2 script, and that
    phase-2 script is present, the transaction contains
      an entry in the indexed redeemer structure (ie. the execution units and redeemer for it are specified).
      Note here that if the full script is not present, we cannot tell from the hash
      that the script is phase-2, and therefore requires a redeemer;

    \item Each redeemer pointer in the indexed redeemer structure corresponds to
    a pointer constructed using $\fun{rdptr}$ from some script purpose of a phase-2
    script of the transaction.
    This ensures that there are no additional entries present in the structure
    (ie. those that are not required for validation of any script);

    \item The signatures of the keys whose hashes are specified in the
    $\fun{reqSignerHashes}$ field in a transaction
    have all indeed signed it;

    \item
    The hash of the subset of protocol parameter values and witnessing data that have been included in the
    transaction body is the same as
    the hash of the witness data and the subset of protocol parameters that are currently contained in the ledger;
\end{itemize}

If these conditions are all satisfied, then the resulting UTxO state change is fully determined
by the UTXO transition (the application of which is also part of the conditions).

\begin{figure}[htb]
  \emph{State transitions}
  \begin{equation*}
    \_ \vdash
    \var{\_} \trans{utxow}{\_} \var{\_}
    \subseteq \powerset (\UTxOEnv \times \UTxOState \times \Tx \times \UTxOState)
  \end{equation*}
  %
  \caption{UTxO with witnesses state update types}
  \label{fig:ts-types:utxo-witness}
\end{figure}

\begin{figure}
  \begin{equation}
    \label{eq:utxo-witness-inductive-alonzo}
    \inference[UTxO-witG]
    {
      \var{txb}\leteq\txbody{tx} &
      \var{txw}\leteq\fun{txwits}~{tx} \\
      (utxo, \wcard, \wcard, \wcard) \leteq \var{utxoSt} \\
      \var{witsKeyHashes} \leteq \{\fun{hashKey}~\var{vk} \vert \var{vk} \in
      \dom (\txwitsVKey{txw}) \}\\
      \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{\{ h \mid (\_, h) \in \fun{scriptsNeeded}~\var{utxo}~txb\} = \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}~{tx}\}}
      \\~\\
      \hldiff{\ \dom (\fun{txrdmrs}~tx)  = \{~\fun{rdptr}~txb~sp~
       \vert~ (sp,h) \in \fun{scriptsNeeded}~\var{utxo}~(\txbody{tx}), } \\
      \hldiff{h\mapsto s \in \fun{txscripts}~{txw}, s \in \ScriptPhTwo \}}
      \\~\\
      \var{txbodyHash}\leteq\fun{hash}~(\txbody{tx}) \\
      \forall \var{vk} \mapsto \sigma \in \txwitsVKey{tx},
      \mathcal{V}_{\var{vk}}{\serialised{txbodyHash}}_{\sigma} \\
      \fun{witsVKeyNeeded}~{utxo}~{tx}~{genDelegs} \subseteq witsKeyHashes
      \\~\\
      genSig \leteq
      \left\{
        \fun{hashKey}~gkey \vert gkey \in\dom{genDelegs}
      \right\}
      \cap
      \var{witsKeyHashes}
      \\
      \left\{
        c\in\txcerts{txb}~\cap\DCertMir
      \right\} \neq\emptyset \implies \vert genSig\vert \geq \Quorum
      \\~\\
      \var{adh}\leteq\fun{txADhash}~\var{txb}
      &
      \var{ad}\leteq\fun{auxiliaryData}~\var{tx}
      \\
      (\var{adh}=\Nothing \land \var{ad}=\Nothing)
      \lor
      (\var{adh}=\fun{hashAD}~\var{ad})
      \\~\\
      \hldiff{\fun{languages}~{txw} \subseteq \dom(\fun{costmdls}~tx)} \\
      \hldiff{\fun{scriptIntegrityHash}~{txb} = 
        \fun{hashScriptIntegrity}~\var{pp}~(\fun{languages}~{txw})~(\fun{txrdmrs}~{txw})~(\fun{txdats}~{txw})}
      \\~\\
      {
        \begin{array}{r}
          \var{slot}\\
          \var{pp}\\
          \var{poolParams}\\
          \var{genDelegs}\\
        \end{array}
      }
      \vdash \var{utxoSt} \trans{\hyperref[fig:rules:utxo-shelley]{utxo}}{tx}
      \var{utxoSt'}\\
    }
    {
      \begin{array}{r}
        \var{slot}\\
        \var{pp}\\
        \var{poolParams}\\
        \var{genDelegs}\\
      \end{array}
      \vdash \var{utxoSt} \trans{utxow}{tx} \varUpdate{\var{utxoSt'}}
    }
  \end{equation}
  \caption{UTxO with witnesses inference rules for Tx}
  \label{fig:rules:utxow-alonzo}
\end{figure}