Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Replace SVAL with a function #1905

Merged
merged 2 commits into from
Oct 28, 2020
Merged

Replace SVAL with a function #1905

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
007e96f
Replace the SVAL rule with a function
WhatisRT Oct 26, 2020
58c0e9c
Fix evalScripts
WhatisRT Oct 27, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
242 changes: 13 additions & 229 deletions goguen/formal-spec/utxo.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -395,10 +395,7 @@ \subsection{Two-Phase Transaction Validation for Non-Native Scripts}
and applies the state changes that are computed by the UTXOS transition.
\\
\textbf{(UTXOS):} & Performs the appropriate UTxO state changes, based on the
value of the $\IsValidating$ tag, which it checks using the SVAL transition.
\\
\textbf{(SVAL):} & Runs the scripts, verifying that the $\IsValidating$ tag
is applied correctly.
value of the $\IsValidating$ tag, which it checks using the $\fun{evalScripts}$ function.
\end{tabular}

In general, there is no way to check that the budget that has been supplied is sufficient for the transaction,
Expand All @@ -409,102 +406,13 @@ \subsection{Two-Phase Transaction Validation for Non-Native Scripts}
If a transaction contains an invalid script, the only change to the ledger
as a result of applying this transaction is the fees.

Two-phase validation requires a new transition system
(see Figure \ref{fig:ts-types:utxos}) to sequentially run
scripts and to track spent execution units as part of its state
($\var{remExU}$). The signal here is a sequence of pairs of a validator
script and the corresponding input data.

Note that there is one state variable in the SVAL transition system. The reason
for this is that in the second, script-running validation phase, we separate
the UTxO state update from sequentially running scripts. This transition
system is strictly for running the scripts, and a transition of this type
will be used by another rule to perform the correct UTxO update.

Running scripts sequentially
to verify that they all validate in the allotted $\ExUnits$ budget only requires
the amount of remaining $\ExUnits$ to be included in the state, and nothing else.
In the environment, we need the protocol parameters and the
transaction being validated. All other data needed
to run the scripts comes from the signal.

\begin{figure}[htb]
\emph{Validation environment}
\begin{equation*}
\ValEnv =
\left(
\begin{array}{r@{~\in~}lr}
\var{pp} & \PParams & \text{protocol parameters}\\
\var{tx} & \GoguenTx & \text{transaction being processed} \\
\end{array}
\right)
\end{equation*}
%
\emph{Validation state}
\begin{equation*}
\ValState =
\left(
\begin{array}{r@{~\in~}lr}
\var{remExU} & \ExUnits & \text{exunits remaining to spend on validation} \\
\end{array}
\right)
\end{equation*}
%
\emph{Script transitions}
\begin{equation*}
\_ \vdash
\var{\_} \trans{sval}{\_} \var{\_}
\subseteq \powerset (\ValEnv \times \ValState \times \seqof{(\ScriptPlutus\times\seqof{\Data}\times\CostMod)} \times \ValState)
\end{equation*}
%
\caption{UTxO script validation types}
\label{fig:ts-types:utxos}
\end{figure}

The rules for the second-phase script validation SVAL are given in
Figure~\ref{fig:rules:utxo-scrval}. Again, no UTxO state update
is done in this rule. Its purpose is to verify that the
validation tag ($\fun{txvaltag}$) is applied correctly by the creater of
the block. It does this by running all the scripts.

Note that following the Shelley ledger specification approach, every function
that we define and use in the preconditions or calculations that are used in the ledger rules is
necessarily total.
In this way, all the errors (validation failures) that we encounter always come from
rule applications, i.e. a precondition of a rule is not met.
We mention this here because the SVAL rule looks as if it could be
simply a function. However, we want the incorrect application of the
validation tag to be an error, so this must be an error that comes form
an unmet precondition of a rule.

There are three transition rules.
The first rule, $\mathsf{Scripts\mbox{-}Val}$, applies when:

\begin{enumerate}
\item There
are no scripts left to validate in the signal list (i.e. this is the base case of
induction when all the scripts have validated) -- note that there could be $\ExUnits$ left over; and
\item The validation tag is applied correctly (it is $\True$).
\end{enumerate}

The $\mathsf{Scripts\mbox{-}Stop}$ rule applies when:

\begin{enumerate}
\item The current script-input pair does not validate;
(either because the transaction ran out of $\ExUnits$ or for any other reason); and
\item The validation tag is correct ($\False$ in this case).
\end{enumerate}

These first two rules require no state change.
The $\mathsf{Scripts\mbox{-}Ind}$ rule applies when:

\begin{enumerate}
\item The current script being validated has been validated;
\item There is a non-negative fee which remains to pay for validating
the rest of the scripts in the list; and
\item Transition rules apply for the rest of the list (without the current script).
\end{enumerate}

The only state change in this rule is of the variable $\var{remExU}$.
It is decreased by subtracting the cost of the execution of the
current script from its current value.
Expand Down Expand Up @@ -542,117 +450,17 @@ \subsection{Two-Phase Transaction Validation for Non-Native Scripts}
result in different validation outcomes running the same script on the same
arguments.


\begin{figure}[htb]
\begin{equation}
\inference[Scripts-Val]
{
\fun{txvaltag}~\var{tx} = \True &
\var{remExU}~\geq~0
}
{
\begin{array}{l}
\var{pp}\\
\var{tx}\\
\end{array}
\vdash
\left(
\begin{array}{r}
\var{remExU}\\
\end{array}
\right)
\trans{sval}{\epsilon}
\left(
\begin{array}{r}
\var{remExU}\\
\end{array}
\right) \\
}
\end{equation}
\begin{equation}
\inference[Scripts-Stop]
{ \\~\\
(\var{isVal},\var{remExU'})~:=~ \llbracket sc \rrbracket_
{cm,\var{remExU}} dt \\
(sc, dt, cm) := s
\\
~
\\
\fun{txvaltag}~\var{tx} = \False &
(\var{remExU'}~<~0 ~ \lor ~ \var{isVal} = \False)
}
{
\begin{array}{l}
\var{pp}\\
\var{tx}\\
\end{array}
\vdash
\left(
\begin{array}{r}
\var{remExU}\\
\end{array}
\right)
\trans{sval}{\Gamma;s}
\left(
\begin{array}{r}
\var{remExU}\\
\end{array}
\right)
}
\end{equation}
\begin{equation}
\inference[Scripts-Ind]
{
{
\begin{array}{l}
\var{pp}\\
\var{tx}\\
\end{array}
}
\vdash
\left(
{
\begin{array}{r}
\var{remExU}\\
\end{array}
}
\right)
\trans{sval}{\Gamma}
\left(
{
\begin{array}{r}
\var{remExU'}\\
\end{array}
}
\right) \\
(\var{isVal},\var{remExU''})~:=~ \llbracket sc \rrbracket
_{cm,\var{remExU'}} dt \\
(sc, dt, cm) := s & \var{remExU''}~\geq~0
}
{
\begin{array}{l}
\var{pp}\\
\var{tx}\\
\end{array}
\vdash
\left(
\begin{array}{r}
\var{remExU}\\
\end{array}
\right)
\trans{sval}{\Gamma;s}
\left(
\begin{array}{r}
\varUpdate{remExU''}\\
\end{array}
\right)
}
\end{equation}
\caption{Script validation rules}
\label{fig:rules:utxo-scrval}
\begin{align*}
& \fun{evalScripts} \in \seqof{(\Script \times \seqof{\Data} \times \CostMod)} \to \ExUnits \to \Bool \\
& \fun{evalScripts}~\epsilon~\var{remExU}~=~\True \\
& \fun{evalScripts}~((\var{sc}, \var{d}, \var{cm});\Gamma)~\var{remExU}~=~
\var{isVal} \land \fun{evalScripts}~\Gamma~\var{remExU'} \\
& ~~\where \\
& ~~~~ (\var{isVal},\var{remExU'})~:=~ \llbracket sc \rrbracket_{cm,\var{remExU}} d
JaredCorduan marked this conversation as resolved.
Show resolved Hide resolved
\end{align*}
\end{figure}


\subsection{Updating the UTxO State}
\label{sec:utxo-state-trans}

Expand Down Expand Up @@ -706,24 +514,12 @@ \subsection{Updating the UTxO State}
\inference[Scripts-Yes]
{
\var{txb}\leteq\txbody{tx} &
\fun{txvaltag}~\var{tx} = \True
\var{sLst} := \fun{mkPLCLst}~\var{pp}~\var{tx}~\var{utxo}
\\
~
\\
\var{sLst} := \fun{mkPLCLst}~\var{pp}~\var{tx}~\var{utxo}
\fun{txvaltag}~\var{tx} = \fun{evalScripts}~\var{sLst}~(\fun{txexunits}~{tx}) = \True
\\~\\
{
\left(
\begin{array}{r}
\var{pp} \\
\var{tx} \\
\end{array}
\right)
}
\vdash
\var{\fun{txexunits}~{tx}}
\trans{sval}{sLst}\var{remExU}
\\~\\
{
\left(
\begin{array}{r}
Expand Down Expand Up @@ -772,23 +568,11 @@ \subsection{Updating the UTxO State}
\inference[Scripts-No]
{
\var{txb}\leteq\txbody{tx} &
\fun{txvaltag}~\var{tx} = \False
\var{sLst} := \fun{mkPLCLst}~\var{pp}~\var{tx}~\var{utxo}
\\
~
\\
\var{sLst} := \fun{mkPLCLst}~\var{pp}~\var{tx}~\var{utxo}
\\~\\
{
\left(
\begin{array}{r}
\var{pp} \\
\var{tx} \\
\end{array}
\right)
}
\vdash
\var{\fun{txexunits}~{tx}}
\trans{sval}{sLst}\var{remExU}
\fun{txvaltag}~\var{tx} = \fun{evalScripts}~\var{sLst}~(\fun{txexunits}~{tx}) = \False
}
{
\begin{array}{l}
Expand Down