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

TxInfo chapter #2494

Merged
merged 1 commit into from
Oct 12, 2021
Merged

TxInfo chapter #2494

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
4 changes: 2 additions & 2 deletions eras/alonzo/formal-spec/alonzo-changes.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -195,6 +195,7 @@
\newcommand{\Tag}{\type{Tag}}
\newcommand{\Credential}{\type{Credential}}
\newcommand{\AssetID}{\type{AssetID}}
\newcommand{\Integer}{\type{Integer}}

%% Adding witnesses
\newcommand{\AssetName}{\type{AssetName}}
Expand Down Expand Up @@ -380,8 +381,6 @@

\include{value-size}

\include{txinfo}

%\include{constants}


Expand All @@ -390,6 +389,7 @@
\bibliography{references}

\begin{appendix}
\include{txinfo}
\include{properties}
\end{appendix}

Expand Down
17 changes: 7 additions & 10 deletions eras/alonzo/formal-spec/properties.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -155,7 +155,7 @@ \section{Formal Properties}
\begin{proof}
With the same argument as previously, we only need to discuss the
equivalent claim for the $\mathsf{UTXOS}$ transition. Under these
assumptions, $\var{sLst} := \fun{collectTwoPhaseScriptInputs}$ is an empty
assumptions, $\var{sLst}$ is an empty
list. Thus $\fun{evalScripts}~sLst = \True$, and the transition rule
had to be $\mathsf{Scripts{-}Yes}$.
\end{proof}
Expand Down Expand Up @@ -274,7 +274,7 @@ \section{Formal Properties}
The following holds :
\[\fun{txValTag}~tx ~=~ \fun{evalScripts}~{tx}~{sLst} \]
where
\[ \var{sLst} \leteq \fun{collectTwoPhaseScriptInputs} ~\field_{pp}(s)~\var{tx}~ \Utxo(s) \]
\[ \var{sLst} \leteq \fun{collectTwoPhaseScriptInputs}~\mathsf{EI}~\mathsf{SysSt} ~\field_{pp}(s)~\var{tx}~ \Utxo(s) \]
\end{lemma}
\begin{proof}
Inspecting the $\mathsf{Scripts{-}Yes}$ and the $\mathsf{Scripts{-}No}$ rules of the $\mathsf{UTXOS}$ transition,
Expand Down Expand Up @@ -363,9 +363,6 @@ \section{Formal Properties}
also true in an implementation. In particular, the interpreter does not
obtain any system randomness, etc.

\item We assume that constructing the validation context from $\TxInfo$ and
the $\ScriptPurpose$ by $\fun{valContext}$ is deterministic.

\item We do not need to check here that the hashes that are the keys of the
$\fun{txscripts}$ and $\fun{txdats}$ fields match the computed hashes of the scripts and
datum objects they index. This is because these hashes must be computed as part of
Expand Down Expand Up @@ -413,9 +410,9 @@ \section{Formal Properties}

The following holds :

\[\fun{toSet}~(\fun{collectTwoPhaseScriptInputs} ~\field_{pp}(s)~\var{tx}~ \Utxo(s))\]
\[\fun{toSet}~(\fun{collectTwoPhaseScriptInputs}~\mathsf{EI}~\mathsf{SysSt} ~\field_{pp}(s)~\var{tx}~ \Utxo(s))\]
\[ = \]
\[\fun{toSet}~(\fun{collectTwoPhaseScriptInputs} ~\field_{pp}(u)~\var{tx'}~ \Utxo(u))\]
\[\fun{toSet}~(\fun{collectTwoPhaseScriptInputs}~\mathsf{EI}~\mathsf{SysSt} ~\field_{pp}(u)~\var{tx'}~ \Utxo(u))\]

\end{lemma}
\begin{proof}
Expand Down Expand Up @@ -501,7 +498,7 @@ \section{Formal Properties}
will not match.

\item $\fun{valContext}$ and $\fun{txInfo}$ :
The $\fun{valContext}$ function is assumed deterministic.
The $\fun{valContext}$ function is defined in \ref{sec:txinfo} and is pure.
All fields of the $\TxInfo$
structure, with the exceptions listed below,
are straightforward translations of the corresponding transaction body fields (see \ref{sec:txinfo}) that
Expand Down Expand Up @@ -557,9 +554,9 @@ \section{Formal Properties}
\end{equation*}
The following holds :

\[\fun{evalScripts}~{tx}~ (\fun{collectTwoPhaseScriptInputs} ~\field_{pp}(s)~\var{tx}~ \Utxo(s))\]
\[\fun{evalScripts}~{tx}~ (\fun{collectTwoPhaseScriptInputs}~\mathsf{EI}~\mathsf{SysSt} ~\field_{pp}(s)~\var{tx}~ \Utxo(s))\]
\[ = \]
\[\fun{evalScripts}~{tx'}~ (\fun{collectTwoPhaseScriptInputs} ~\field_{pp}(u)~\var{tx'}~ \Utxo(u))\]
\[\fun{evalScripts}~{tx'}~ (\fun{collectTwoPhaseScriptInputs}~\mathsf{EI}~\mathsf{SysSt} ~\field_{pp}(u)~\var{tx'}~ \Utxo(u))\]

\end{corollary}

Expand Down
Loading