Skip to content

Commit

Permalink
rebase
Browse files Browse the repository at this point in the history
  • Loading branch information
@polinavino
polinavino committed Sep 28, 2021
1 parent c6c4be1 commit bdf74e2
Show file tree
Hide file tree
Showing 3 changed files with 264 additions and 34 deletions.
1 change: 1 addition & 0 deletions eras/alonzo/formal-spec/alonzo-changes.tex
View file
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
255 changes: 253 additions & 2 deletions eras/alonzo/formal-spec/txinfo.tex
View file
Expand Up @@ -3,5 +3,256 @@ \section{TxInfo Construction}

This section specifies exactly what parts of the transaction and ledger
state are used by the $\fun{txInfo}$ function to construct the
$\TxInfo$ term that gets passed as an
argument to the Plutus interpreter.
$\TxInfo$ element that, together with the script purpose for which the script
is being run, gets passed as a $\Data$ argument to the Plutus interpreter.

The functions in Figure \ref{fig:txinfo-funcs} are needed to build a $\Data$ summary of a transaction.
In this Section we use the notation $\type{P.PlutusType}$ for the Plutus type
$\type{PlutusType}$ (specified in the Plutus library) to distinguish it from ledger types.
The type $\type{P.ScriptContext}$ represents
the script context. The function $\type{P.toData}$ converts a Plutus-library element
into a $\Data$ element.

$\fun{txInfo}$ summarizes all the necessary transaction and chain state information
that needs to be passed to the script interpreter. Below, we specify how to
represent relevant transaction data in terms of a Plutus
library-defined type. The $\fun{txInfo}$ function builds this representation.

The $\Language$ argument
is required because different languages have different expectations of the
format and contents of the $\TxInfo$ summary.

Note that $\fun{txInfo}$ has a $\UTxO$ argument. Even though the full ledger UTxO
is passed to it, we define this function in such a way that the only
entries in the ledger UTxO map that a Plutus script
actually sees via the argument $\fun{txInfo}$ builds are the ones corresponding to the transaction
inputs (ie. its realized inputs). This is done in order to maintain the locality of
evaluation. For details, see the deterministic script evaluation property~\ref{prop:fixed-inputs}.

$\fun{valContext}$ constructs the \emph{validation context}, also referred to as the
script context. A validation context is
a $\Data$ element which encodes both the summary of the transaction and ledger information
(this is supplied by the $\fun{txInfo}$ summarization function), and the script purpose.

\begin{figure}
\emph{Plutus Library Types and Functions}
%
\begin{align*}
&\type{P.ScriptContext} ~=~ \type{P.TxInfo} \times \type{P.ScriptPurpose} \\
&\text{Plutus Script Context}
\nextdef
&\fun{P.toData} \in \type{P.T} \to \Data \\
&\text{Constructs a Data element from a Plutus-library-type element of type P.T}
\end{align*}
\emph{Ledger Functions}
%
\begin{align*}
&\fun{txInfo} \in \Language \to \PParams \to \UTxO \to \Tx \to \TxInfo \\
&\text{Summarizes transaction data}
\nextdef
&\fun{valContext} \in \type{P.TxInfo} \to \ScriptPurpose \to \Data \\
&\fun{valContext}~txinfo~sp = \fun{P.toData}~(txinfo,~sp_{P})
&\text{Pairs transaction data with a script purpose}
\end{align*}
\caption{Transaction Summarization Functions}
\label{fig:txinfo-funcs}
\end{figure}

We give the Plutus types corresponding to the ledger counterparts in Figures \ref{fig:txinfo-types}
and \ref{fig:txinfo-types-two}. Details for types that have non-identity translation
functions between ledger and Plutus types are in Figure \ref{fig:txinfo-translations}.
The non-identity translation functions are specified in the comments of the $\TxInfo$ type
definition.

Certain types, such as the bootstrap address type, cannot be passed to scripts, and
are therefore translated as $\Nothing$. Any type that cannot be fully translated
as a Plutus-library type is also translated to $\Nothing$.
For example, since a bootstrap address $a \in \AddrBS$
is not translatable, neither is $a\in\Addr$, and $(a,\wcard,\wcard) \in \TxOut$
also translates to $\Nothing$.

If $t$ is a term of type $LT$, then we denote the translated term of type $P.LT$ by $t_P$.

Translating certain kinds of certificates drops the data in the
certificates, in particular, the $\DCertGen$ and $\DCertMir$ ones.

The constant returned by $\fun{slotToPOSIXTime}$,

\[\type{ResolutionConstant}\]

Is the maximum possible value of a POSIX time interval. This will be adjusted in
future eras to reflect the time being translated.

Note that the $\Ptr$ addresses translated and passed to Plutus scripts are
not resolvable to their corresponding key or script staking credencials. This
is because doing a lookup in the resolution map, which part of the ledger state,
could break determinism.

During the transaction encoding and decoding process, a transaction is discarded if it is not
encoded correctly. This includes, in particular, a check that $\Script$ and $\Data$
elements contained in the transaction are well-formed. Functions that perfom these checks are
in Figure \ref{fig:data-script-check}. The $\fun{P.validateScript}$ function
is a Plutus-library function which checks whether a bytestring represents a
Plutus script.

\begin{figure*}[htb]
\emph{Hash Types} \\
\begin{equation*}
\begin{array}{r@{~~~}l}
\ScriptHash & \type{P.ValidatorHash} \\
\KeyHash & \type{P.PubKeyHash} \\
\DataHash & \type{P.DatumHash} \\
\TxId & \type{P.TxId} \\
\end{array}
\end{equation*}
\emph{Transaction Input, ie. Output Reference} \\
\begin{equation*}
\begin{array}{r@{~~~}l}
\TxIn & \type{P.TxOutRef} \\
\end{array}
\end{equation*}
\emph{Credential Types} \\
\begin{equation*}
\begin{array}{r@{~~~}l}
\Ptr & \type{P.StakingPtr} \\
\Credential & \type{P.Credential} \\
\Credential & \type{P.StakingHash} \\
\StakeCredential & \type{P.StakingCredential} \\
\end{array}
\end{equation*}
\emph{Credentials and Withdrawals} \\
\begin{equation*}
\begin{array}{r@{~~~}l}
\Wdrl & \type{P.StakingCredential} \times \Integer \\
\PolicyID & \type{P.CurrencySymbol} \\
\AssetName & \type{P.TokenName} \\
\end{array}
\end{equation*}
\emph{Certificate Types} \\
\begin{equation*}
\begin{array}{r@{~~~}l}
\DCert & \type{P.DCert} \\
\DCertRegKey & \type{P.DCertDelegRegKey} \\
\DCertDeRegKey & \type{P.DCertDelegDeRegKey} \\
\DCertDeleg & \type{P.DCertDelegDelegate} \\
\DCertRetirePool & \type{P.DCertPoolRetire} \\
\end{array}
\end{equation*}
\emph{Data-dropping Certificate Types} \\
\begin{equation*}
\begin{array}{r@{~~~}l}
\DCertGen & \type{P.DCertGenesis} \\
\DCertMir & \type{P.DCertMir} \\
\end{array}
\end{equation*}
\caption{TxInfo and Constituent Types}
\label{fig:txinfo-types}
\end{figure*}

\begin{figure*}[htb]
\emph{Script Purpose Types} \\
\begin{equation*}
\begin{array}{r@{~~~}l}
\mathsf{Cert} & \type{P.Certifying} \\
\mathsf{Rwrd} & \type{P.Rewarding} \\
\mathsf{Mint} & \type{P.Minting} \\
\mathsf{Spend} & \type{P.Spending} \\
\end{array}
\end{equation*}
\emph{Execution Budget Types} \\
\begin{equation*}
\begin{array}{r@{~~~}l}
\Integer & \type{P.ExCPU} \\
\Integer & \type{P.ExMemory}\\
\ExUnits & \type{P.ExBudget} \\
\end{array}
\end{equation*}
\begin{align*}
& \emph{TxInfo} \\
& \TxInfo = \\
& ~~~~ \seqof{\type{P.TxInInfo^?}} % & \text{inputs} \\ %\type{P.txInfoInputs} &
& \text{realized inputs (built by $\fun{txInfoIn}$)} \\
& ~~~~ \times \seqof{\type{P.TxOut^?}}
& \text{outputs} \\ %\type{P.txInfoOutputs}
& ~~~~ \times \type{P.Value}
& \text{fee, translated by $\fun{transValue}\circ\fun{inject}$} \\ %= transValue (inject @(Mary.Value (Crypto era)) fee), \type{P.txInfoFee}
& ~~~~ \times \type{P.Value}
& \text{mint field, translated by $\fun{transValue}$} \\ % = transValue forge, \type{P.txInfoMint}
& ~~~~ \times \seqof{\type{P.DCert}}
& \text{list of certificates} \\ %= foldr (\c ans \to transDCert c : ans) [] (certs' tbody), \type{P.txInfoDCert}
& ~~~~ \times (\type{P.StakingCredential} \times \Integer)
& \text{reward withdrawal (credential and reward amount)} \\ % = Map.toList (transWdrl (wdrls' tbody)), \type{P.txInfoWdrl}
& ~~~~ \times \type{P.POSIXTimeRange}
& \text{validity POSIX time range, translated by $\fun{transVITime}$} \\ % = timeRange, \type{P.txInfoValidRange}
& ~~~~ \times \seqof{\type{P.PubKeyHash}}
& \text{hashes of keys whose signature are required} \\ % = map transKeyHash (Set.toList (reqSignerHashes' tbody)), \type{P.txInfoSignatories}
& ~~~~ \times \seqof{(\DataHash \times \Data)}
& \text{list of pairs of datum hashes and their datum preimages} \\ % = map transDataPair datpairs, \type{P.txInfoData}
& ~~~~ \times \type{P.TxId} % = (transSafeHash (hashAnnotated @(Crypto era) tbody)) \type{P.txInfoId}
& \text{transaction ID}
\end{align*}
\caption{TxInfo and Constituent Types}
\label{fig:txinfo-types-two}
\end{figure*}

\begin{figure*}[htb]
\begin{align*}
& \fun{transAddr} \in \Addr \to \type{P.Address} \\
& \fun{transAddr} ~a = \begin{cases}
\Nothing & \text{if}~a \in \AddrBS \\
(ob,~st) & \text{if}~a = (\wcard, ob_P, st_P)
\end{cases} \\
& \text{Address translation}
\nextdef
& \fun{transValue} \in \Value \to \type{P.Value} \\
& \fun{transValue}~ (c,~ mp) = \{~ pid_P\mapsto (aid_P \mapsto q_P) ~\mid~ pid \mapsto (aid \mapsto q) \in mp ~\} \\
& ~~~~\cup \{~\type{P.adaSymbol}\mapsto (\type{P.adaToken} \mapsto c) ~\} \\
& \text{Value translation}
\nextdef
& \fun{transDCert} \in \DCertRegPool \to \type{P.DCertPoolRegister} \\
& \fun{transDCert}~\var{pool} = (\fun{poolId}~\var{pool},~\fun{poolVrf}~\var{pool}) \\
& \text{Pool registration certificate translation}
\nextdef
& \fun{txInfoIn} \in \UTxO \to \TxIn \to \type{P.TxInInfo} \\
& \fun{txInfoIn}~ utxo~ txin = \begin{cases}
(\var{txin}_P, \var{txout}_P) & \text{if $(\var{txin}\mapsto\var{txout})\in\var{utxo}$} \\
\Nothing & \text{otherwise}
\end{cases} \\
& \text{Builds a Plutus realized input}
\nextdef
& \fun{transVITime} \in \PParams \to \EpochInfo \to \SystemStart \to \ValidityInterval \to \type{P.POSIXTimeRange} \\
& \fun{transVITime} ~pp ~ei~ sysS~ (vs,~ vf) = \\
& ~~~~ \begin{cases}
\type{P.always} & \text{if } vs = \Nothing ~\wedge~ vf = \Nothing \\
\type{P.to}~(\fun{slotToPOSIXTime}~pp~ei~sysS~vf) & \text{if } vs = \Nothing ~\wedge~ vf \neq \Nothing \\
\type{P.from}~(\fun{slotToPOSIXTime}~pp~ei~sysS~vs) & \text{if } vs \neq \Nothing ~\wedge~ vf = \Nothing \\
(\fun{slotToPOSIXTime}~pp~ei~sysS~vs,~\fun{slotToPOSIXTime}~pp~ei~sysS~vf) & \text{if } vs \neq \Nothing ~\wedge~ vf \neq \Nothing \\
\end{cases} \\
& ~~~~\where \\
& ~~~~~~~~\fun{slotToPOSIXTime}~pp~ei~sysS~vs~=~\type{ResolutionConstant} \\
& \text{Translate validity interval to a POSIX time range}
\end{align*}
\caption{TxInfo Constituent Type Translation Functions}
\label{fig:txinfo-translations}
\end{figure*}

\begin{figure*}[htb]
\begin{align*}
& \fun{validPlutusdata} \in \type{P.Data} \to \Bool \\
& \fun{validPlutusdata}~ (\type{P.Constr} ~\wcard ~ds) = \wedge_{d\in ds} (\type{validPlutusdata}~d) \\
& \fun{validPlutusdata}~ (\type{P.Map}~ ds) = \wedge_{(x,y)\in ds} ((\type{validPlutusdata}~x) \wedge (\type{validPlutusdata}~x)) \\
& \fun{validPlutusdata} ~(\type{P.List}~ ds) = \wedge_{d\in ds} (\type{validPlutusdata}~d) \\
& \fun{validPlutusdata}~ (\type{P.I}~ \wcard) = \True \\
& \fun{validPlutusdata}~ (\type{P.B}~ bs) = \fun{length} ~bs~ \leq~ 64 \\
& \text{Checks if a Data element is constructed correctly}
\nextdef
& \fun{validScript} \in \Script \to \Bool \\
& \fun{validScript} ~sc = \begin{cases}
\True & \text{if $sc \in \ScriptPhOne$} \\
\type{P.validateScript} ~sc & \text{if $sc \in \ScriptPhTwo$}
\end{cases} \\
& \text{Checks if a script is constructed correctly}
\end{align*}
\caption{Script and Data construction correctness checks}
\label{fig:data-script-check}
\end{figure*}
42 changes: 10 additions & 32 deletions eras/alonzo/formal-spec/utxo.tex
View file
Expand Up @@ -97,7 +97,8 @@ \subsection{Combining Scripts with Their Inputs}
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.
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
Expand Down Expand Up @@ -193,6 +194,11 @@ \subsection{Combining Scripts with Their Inputs}

\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.
Expand All @@ -204,23 +210,6 @@ \subsection{Plutus Script Validation}
is too far in the future for the system to accurately
predict the exact time to which it refers.

\item $\fun{txInfo}$ summarizes all the necessary transaction and chain state info
that needs to be passed to the script interpreter. The $\Language$ argument
is required because different languages have different expectations of the
format and contents of the $\TxInfo$ summary.

Note that $\fun{txInfo}$ has a $\UTxO$ argument. Even though the full ledger UTxO
is passed to it, we define this function in such a way that the only
entries in the ledger UTxO map that a Plutus script
actually sees via the argument $\fun{txInfo}$ builds are the ones corresponding to the transaction
inputs (ie. its realized inputs). This is done in order to maintain
deterministic evaluation. For details, see~\ref{sec:txinfo}

\item
$\fun{valContext}$ constructs the \emph{validation context}. A validation context is
a $\Data$ term which encodes both the summary of the transaction and ledger information
(this is supplied by the $\fun{txInfo}$ summarizing function), and the script purpose.

\item
$\fun{runPLCScript}$ validates Plutus scripts. It takes the following
arguments:
Expand Down Expand Up @@ -313,22 +302,11 @@ \subsection{Plutus Script Validation}
rather than running and failing.

\begin{figure*}[htb]
\emph{Abstract Script Validation Types}
%
\begin{equation*}
\begin{array}{r@{~\in~}l@{\quad\quad\quad\quad}r}
\var{txinfo} &\TxInfo & \text{Language-specific summary of transaction data}\\
\end{array}
\end{equation*}
\emph{Abstract Script Validation Functions}
%
\begin{align*}
&\fun{epochInfoSlotToUTCTime} \in \EpochInfo \to \SystemStart \to \Slot \to \UTCTime^? \\
&\text{Translate slot number to system time (via consensus) or fail} \\~\\
&\fun{txInfo} \in \Language \to \UTxO \to \Tx \to \TxInfo \\
&\text{Summarizes transaction data} \\~\\
&\fun{valContext} \in \TxInfo \to \ScriptPurpose \to \Data \\
&\text{Pairs transaction data with a script purpose} \\~\\
&\text{Translate slot number to system time or fail} \\~\\
&\fun{runPLCScript} \in \CostMod \to \ScriptPlutus \to \ExUnits \to \seqof{\Data} \to
\IsValid \\
&\text{Validate a Plutus script, taking resource limits into account}
Expand All @@ -338,7 +316,7 @@ \subsection{Plutus Script Validation}
%
\begin{align*}
\llbracket \var{script_v} \rrbracket_{\var{cm},\var{eu}}~\var{d}
&=& \fun{runPLCScript} ~\var{script_v}~\var{d}~\var{eu}~{cm}
&=& \fun{runPLCScript}~{cm} ~\var{script_v}~\var{eu}~\var{d}
\end{align*}
\caption{Script Validation, cont.}
\label{fig:defs:functions-valid}
Expand Down Expand Up @@ -413,7 +391,7 @@ \subsection{Plutus Script Validation}
& ~~~~\fun{language}~{script} \mapsto \var{cm} \in \fun{costmdls}~{pp}, \\
& ~~~~\var{script} \in \ScriptPhTwo \} \\
& \where \\
& ~~~~~~~ \var{txinfo}~=~\fun{txInfo}~(\fun{language}~{script})~\var{utxo}~\var{tx} \\
& ~~~~~~~ \var{txinfo}~=~\fun{txInfo}~(\fun{language}~{script})~{pp}~\var{utxo}~\var{tx} \\
\nextdef
& \fun{evalScripts} \in \Tx \times \seqof{(\Script \times \seqof{\Data} \times \ExUnits \times \CostMod)} \to \IsValid \\
& \fun{evalScripts}~\var{tx}~\epsilon = \True \\
Expand Down

0 comments on commit bdf74e2

Please sign in to comment.