From b58d8b709234833244744990b7ec47d92ac34556 Mon Sep 17 00:00:00 2001 From: Polina Vinogradova Date: Tue, 28 Sep 2021 13:03:25 -0400 Subject: [PATCH] Add txinfo appendix rebase comments Small changes to formatting comments Streamlining & cleanup ei sysSt global constants time translate --- eras/alonzo/formal-spec/alonzo-changes.tex | 4 +- eras/alonzo/formal-spec/properties.tex | 17 +- eras/alonzo/formal-spec/txinfo.tex | 313 ++++++++++++++++++++- eras/alonzo/formal-spec/utxo.tex | 80 ++---- 4 files changed, 351 insertions(+), 63 deletions(-) diff --git a/eras/alonzo/formal-spec/alonzo-changes.tex b/eras/alonzo/formal-spec/alonzo-changes.tex index e00a2beb83..de1965f30c 100644 --- a/eras/alonzo/formal-spec/alonzo-changes.tex +++ b/eras/alonzo/formal-spec/alonzo-changes.tex @@ -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}} @@ -380,8 +381,6 @@ \include{value-size} -\include{txinfo} - %\include{constants} @@ -390,6 +389,7 @@ \bibliography{references} \begin{appendix} + \include{txinfo} \include{properties} \end{appendix} diff --git a/eras/alonzo/formal-spec/properties.tex b/eras/alonzo/formal-spec/properties.tex index 106cd57b5e..cf853f1012 100644 --- a/eras/alonzo/formal-spec/properties.tex +++ b/eras/alonzo/formal-spec/properties.tex @@ -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} @@ -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, @@ -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 @@ -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} @@ -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 @@ -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} diff --git a/eras/alonzo/formal-spec/txinfo.tex b/eras/alonzo/formal-spec/txinfo.tex index 7c1d0d7c0e..3a266cef78 100644 --- a/eras/alonzo/formal-spec/txinfo.tex +++ b/eras/alonzo/formal-spec/txinfo.tex @@ -3,5 +3,314 @@ \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. + +\subsection{Type Translations} + +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}. + +\textbf{Notation. } +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. + +If $\type{LT}$ is a ledger type, and $\type{P.LT}$ is the corresponding Plutus type to +which elements of $\type{LT}$ must be translated, we denote the +translation function by: + +\[ \fun{toPlutusType_{LT}} : \type{LT} \to \type{P.LT} \] + +As a shorthand, we always write $t_P$ for $\fun{toPlutusType}_{LT}~t$, if $t$ is of type $\type{LT}$. + +In many cases this function is simply the identity function, and all +the cases in which it is not the identity will be described below. + +\textbf{Untranslatable Types. } +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$. + +\textbf{Certificates. } +Translating certain kinds of certificates drops the data in the +certificates, in particular, the $\DCertGen$ and $\DCertMir$ ones. +The $\DCertRegPool$ pool registration certificate has a non-identity translation function, +$\fun{transPoolCert}$. + +\textbf{Time Translation.} +Functions needed to implement conversion of a slot number to POSIX time are +given in Figure \ref{fig:time-funcs}. + +\textbf{Pointer Address Resolution. } +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. + +\textbf{Well-Formed Scripts and Data. } +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}{l@{~~~}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}{l@{~~~}l} + \TxIn & \type{P.TxOutRef} \\ + \end{array} + \end{equation*} + \emph{Credential Types} \\ + \begin{equation*} + \begin{array}{l@{~~~}l} + \Ptr & \type{P.StakingPtr} \\ + \Credential & \type{P.Credential} \\ + \Credential & \type{P.StakingHash} \\ + \StakeCredential & \type{P.StakingCredential} \\ + \end{array} + \end{equation*} + \emph{Value Types} \\ + \begin{equation*} + \begin{array}{l@{~~~}l} + \Wdrl & \type{P.StakingCredential} \times \Integer \\ + \PolicyID & \type{P.CurrencySymbol} \\ + \AssetName & \type{P.TokenName} \\ + \Coin & \Integer \\ + \Quantity & \Integer \\ + \end{array} + \end{equation*} + \emph{Certificate Types} \\ + \begin{equation*} + \begin{array}{l@{~~~}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 Types} \\ + \begin{equation*} + \begin{array}{l@{~~~}l} + \RewardAcnt & \type{P.StakingHash} \\ + \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}{l@{~~~}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}{l@{~~~}l} + \Integer & \type{P.ExCPU} \\ + \Integer & \type{P.ExMemory}\\ + \ExUnits & \type{P.ExBudget} \\ + \end{array} + \end{equation*} + \emph{TxInfo} \\ + \begin{align*} + & \TxInfo = \\ + & ~~~~ \seqof{\type{P.TxInInfo^?}} % & \text{inputs} \\ %\type{P.txInfoInputs} & + & \text{realized inputs} \\ + & ~~~~ \times \seqof{\type{P.TxOut^?}} + & \text{outputs} \\ %\type{P.txInfoOutputs} + & ~~~~ \times \type{P.Value} + & \text{fee} \\ %= transValue (inject @(Mary.Value (Crypto era)) fee), \type{P.txInfoFee} + & ~~~~ \times \type{P.Value} + & \text{mint field} \\ % = 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} \\ % = Map.toList (transWdrl (wdrls' tbody)), \type{P.txInfoWdrl} + & ~~~~ \times \type{P.POSIXTimeRange} + & \text{validity interval in POSIX time} \\ % = timeRange, \type{P.txInfoValidRange} + & ~~~~ \times \seqof{\type{P.PubKeyHash}} + & \text{key hashes of required signatures} \\ % = map transKeyHash (Set.toList (reqSignerHashes' tbody)), \type{P.txInfoSignatories} + & ~~~~ \times \seqof{(\DataHash \times \Data)} + & \text{list of datums and their hashes} \\ % = 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] + \emph{Abstract Types} + \begin{equation*} + \begin{array}{r@{~\in~}l@{\quad\quad\quad\quad}r} + \var{scs} & \type{Seconds} & \text{time in seconds} + \end{array} + \end{equation*} + % + \emph{Abstract Conversion Functions} + \begin{align*} + & \fun{utcTimeToPOSIXSeconds} \UTCTime \to \type{Seconds} \\ + & \text{Convert UTC Time to seconds} + \end{align*} + % + \emph{Rounding Functions} + \begin{align*} + & \fun{truncate} \type{Fraction} \to \Integer \\ + & \text{Round a fractional value to the nearest integer} + \end{align*} + % + \emph{Slot to Time Conversion} + \begin{align*} + & \fun{slotToPOSIXTime} \in \PParams \to \EpochInfo \to \SystemStart \to \Slot \to \type{P.POSIXTime} \\ + & \fun{slotToPOSIXTime}~pp~ei~sysS~vs~=~\\ + & ~~~~\fun{truncate}~ ((\fun{utcTimeToPOSIXSeconds}~(\fun{epochInfoSlotToUTCTime}~pp~ei~sysS~vs))~*~1000) \\ + & \text{Translate validity interval to a POSIX time range} + \end{align*} + \caption{Types and Functions Used in Time Conversion} + \label{fig:time-funcs} +\end{figure*} + +\begin{figure*}[htb] + \emph{Conversion Functions} + \begin{align*} + & \fun{toPlutusType}_{\Addr} \in \Addr \to \type{P.Address} \\ + & \fun{toPlutusType}_{\Addr} ~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{toPlutusType}_{\Value} \in \Value \to \type{P.Value} \\ + & \fun{toPlutusType}_{\Value}~ (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_P) ~\} \\ + & \text{Value translation} + \nextdef + & \fun{toPlutusType}_{\TxOut} \in \TxOut \to \type{P.TxOut} \\ + & \fun{toPlutusType}_{\TxOut}~ (a, v, h) = (a_P, v_P, h_P) \\ + & \text{Output translation} + \nextdef + & \fun{toPlutusType}_{\DCert} \in \DCert \to \type{P.DCert} \\ + & \fun{toPlutusType}_{\DCert}~\var{c} = \begin{cases} + (\fun{poolId}~\var{c},~\fun{poolVrf}~\var{c}) & \text{if } \var{c}\in \DCertRegPool \\ + c_P & \text{otherwise} + \end{cases} \\ + & \text{Certificate translation} + \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} \\ + \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) = \bigwedge_{d\in ds} \type{validPlutusdata}~d \\ + & \fun{validPlutusdata}~ (\type{P.Map}~ ds) = \bigwedge_{(x,y)\in ds} \type{validPlutusdata}~x \wedge \type{validPlutusdata}~y \\ + & \fun{validPlutusdata} ~(\type{P.List}~ ds) = \bigwedge_{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*} + +\subsection{Building Transaction Summary} + +The functions in Figure \ref{fig:txinfo-funcs} are needed to build a $\Data$ summary of a transaction. +The function $\type{P.toData}$ converts a Plutus-library element +into a $\Data$ element. + +\textbf{The $\fun{txInfo}$ Function.} +$\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. The $\EpochInfo$ and $\SystemStart$ + arguments are needed for translating slot numbers to POSIX time. + + 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}. + +\textbf{The $\fun{valContext}$ Function.} + $\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 Functions} + % + \begin{align*} + &\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 \EpochInfo \to \SystemStart \to \UTxO \to \Tx \to \TxInfo \\ + &\fun{txInfo}~ pp~ ei~ sysS~ utxo~tx = \\ + & ~~~~ (\{~(\var{txin}_P, \var{txout}_P) \mid \var{txin}\in \fun{txinputs}~tx,~(\var{txin}\mapsto\var{txout})\in\var{utxo}~\}, \\ + & ~~~~ \{~\var{tout}_P\mid\var{tout}\in\fun{txouts}~{tx}~\} , \\ + & ~~~~ (\fun{inject}~(\fun{txfee}~{tx}))_P, \\ + & ~~~~ (\fun{mint}~{tx})_P , \\ + & ~~~~ [~ c_P \mid c \in \fun{txcerts}~{tx} ~] , \\ + & ~~~~ \{~(s_P,~c_P)\mid s\mapsto c \in \fun{txwdrls}~{tx}~\} , \\ + & ~~~~ \fun{transVITime} ~pp ~ei~ sysS~ (\fun{txvldt}~tx) , \\ + & ~~~~ \{~k_P\mid k \in \dom \fun{txwitsVKey}~{tx}~\} , \\ + & ~~~~ \{~(h_P,~d_P)\mid h\mapsto d \in \fun{txdats}~{tx}~\} , \\ + & ~~~~ (\fun{txid}~{tx})_P) \\ + &\text{Summarizes transaction data} + \nextdef + &\fun{valContext} \in \type{P.TxInfo} \to \ScriptPurpose \to \Data \\ + &\fun{valContext}~\var{txinfo}~\var{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} diff --git a/eras/alonzo/formal-spec/utxo.tex b/eras/alonzo/formal-spec/utxo.tex index 436e00a47d..575c3a7bca 100644 --- a/eras/alonzo/formal-spec/utxo.tex +++ b/eras/alonzo/formal-spec/utxo.tex @@ -84,11 +84,9 @@ \subsection{Combining Scripts with Their Inputs} 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 $\EpochInfo$ is a consensus-level parameter needed to compute the system time. Within -the Alonzo era, this is constant, with value $\mathsf{epochInfo}$ -\item $\SystemStart$ is another consensus-level parameter needed to compute the system time. Within -the Alonzo era, this is also constant, with value $\mathsf{systemTime}$ \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 @@ -97,7 +95,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 @@ -131,19 +130,25 @@ \subsection{Combining Scripts with Their Inputs} \begin{figure}[htb] - \emph{Abstract types and constants of these types} + \emph{Global Constants} % \begin{equation*} \begin{array}{r@{~\in~}l@{}lr} - \var{tm} - & \UTCTime - & \text{System time (variable)} \\ - \mathsf{epochInfo} + \mathsf{EI} & \EpochInfo - & \text{Epoch info (constant within Alonzo)} \\ - \mathsf{systemTime} + & \text{Alonzo epoch info} \\ + \mathsf{SysSt} & \SystemStart - & \text{System start time (constant within Alonzo)} + & \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*} % @@ -193,6 +198,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. @@ -204,23 +214,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: @@ -313,22 +306,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} @@ -338,7 +320,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} @@ -403,9 +385,9 @@ \subsection{Plutus Script Validation} \epsilon & \text{otherwise} \end{cases} \nextdef - & \fun{collectTwoPhaseScriptInputs} \in \PParams \to \Tx \to \UTxO \to \\ + & \fun{collectTwoPhaseScriptInputs} \in \EpochInfo \to \SystemStart \to \PParams \to \Tx \to \UTxO \to \\ & ~~~~ \seqof{(\Script \times \seqof{\Data} \times \ExUnits \times \CostMod)} \\ - & \fun{collectTwoPhaseScriptInputs} ~\var{pp}~\var{tx}~ \var{utxo} ~=~ \\ + & \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), \\ @@ -413,7 +395,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}~\var{ei}~\var{sysSt}~(\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 \\ @@ -531,7 +513,7 @@ \subsection{The UTXOS transition system} \inference[Scripts-Yes] { \var{txb}\leteq\txbody{tx} & - \var{sLst} := \fun{collectTwoPhaseScriptInputs}~\var{pp}~\var{tx}~\var{utxo} + \var{sLst} := \fun{collectTwoPhaseScriptInputs}~\mathsf{EI}~\mathsf{SysSt}~\var{pp}~\var{tx}~\var{utxo} \\ ~ \\ @@ -582,7 +564,7 @@ \subsection{The UTXOS transition system} \inference[Scripts-No] { \var{txb}\leteq\txbody{tx} & - \var{sLst} := \fun{collectTwoPhaseScriptInputs}~\var{pp}~\var{tx}~\var{utxo} + \var{sLst} := \fun{collectTwoPhaseScriptInputs}~\mathsf{EI}~\mathsf{SysSt}~\var{pp}~\var{tx}~\var{utxo} \\ ~ \\ @@ -663,7 +645,7 @@ \subsection{The UTXOS transition system} \var{txb}\leteq\txbody{tx} & \fun{ininterval}~\var{slot}~(\fun{txvldt}~{tx}) & \hldiff{\var{(\wcard, i_f)}\leteq\fun{txvldt}~{tx}} \\~\\ - \hldiff{\Nothing \notin \{\fun{txrdmrs}~\var{tx}, i_f\} ~\Rightarrow~ \fun{epochInfoSlotToUTCTime}~\mathsf{epochInfo}~\mathsf{systemTime}~i_f \neq \Nothing} \\ + \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}