Skip to content

Commit

Permalink
comments
Browse files Browse the repository at this point in the history
  • Loading branch information
@polinavino
polinavino committed Sep 27, 2021
1 parent 53bc6d6 commit 9f9db83
Showing 1 changed file with 118 additions and 94 deletions.
212 changes: 118 additions & 94 deletions alonzo/formal-spec/txinfo.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,20 +3,20 @@ \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, together with the script purpose for which the script
$\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 term
into into a $\Data$ term.
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 info
$\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 as a term of a type defined in the Plutus
library. The $\fun{txInfo}$ function builds this representation.
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
Expand All @@ -26,12 +26,12 @@ \section{TxInfo Construction}
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}.
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$ term which encodes both the summary of the transaction and ledger information
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}
Expand All @@ -42,7 +42,7 @@ \section{TxInfo Construction}
&\text{Plutus Script Context}
\nextdef
&\fun{P.toData} \in \type{P.T} \to \Data \\
&\text{Constructs a Data term from a Plutus term of type P.T}
&\text{Constructs a Data element from a Plutus-library-type element of type P.T}
\end{align*}
\emph{Ledger Functions}
%
Expand All @@ -61,15 +61,17 @@ \section{TxInfo Construction}
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$. All terms made up of untranslatable
terms also translate 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$
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$.

We denote a term $t$ of a ledger type $\type{LT}$ that has been translated to the
corresponding Plutus type by $t_P$.
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.
Expand All @@ -87,85 +89,107 @@ \section{TxInfo Construction}
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 scripts and $\Data$
terms therein are constructed with constructors of terms of these types, themselves
applied to correctly typed terms. Functions that perfom these checks are
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]
\begin{align*}
& \emph{Hash Types} \\
& \ScriptHash & \type{P.ValidatorHash} \\
& \KeyHash & \type{P.PubKeyHash} \\
& \DataHash & \type{P.DatumHash} \\
& \TxId & \type{P.TxId} \\
~\\
& \emph{Transaction Input, ie. Output Reference} \\
& \TxIn & \type{P.TxOutRef} \\
~\\
& \emph{Credential Types} \\
& \Ptr & \type{P.StakingPtr} \\
& \Credential & \type{P.Credential} \\
& \Credential & \type{P.StakingHash} \\
& \StakeCredential & \type{P.StakingCredential} \\
~\\
& \emph{Credentials and Withdrawals} \\
& \Wdrl & \type{P.StakingCredential} \times \Integer \\
& \PolicyID & \type{P.CurrencySymbol} \\
& \AssetName & \type{P.TokenName} \\
~\\
& \emph{Certificate Types} \\
& \DCert & \type{P.DCert} \\
& \DCertRegKey & \type{P.DCertDelegRegKey} \\
& \DCertDeRegKey & \type{P.DCertDelegDeRegKey} \\
& \DCertDeleg & \type{P.DCertDelegDelegate} \\
& \DCertRetirePool & \type{P.DCertPoolRetire} \\
~\\
& \emph{Data-dropping Certificate Types} \\
& \DCertGen & \type{P.DCertGenesis} \\
& \DCertMir & \type{P.DCertMir} \\
\end{align*}
\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]
\begin{align*}
& \emph{Script Purpose Types} \\
& \mathsf{Cert} & \type{P.Certifying} \\
& \mathsf{Rwrd} & \type{P.Rewarding} \\
& \mathsf{Mint} & \type{P.Minting} \\
& \mathsf{Spend} & \type{P.Spending} \\
~\\
& \emph{Execution Budget Types} \\
& \Integer & \type{P.ExCPU} \\
& \Integer & \type{P.ExMemory}\\
& \ExUnits & \type{P.ExBudget} \\
~\\
\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{$\uparrow$ Realized inputs (built by $\fun{txInfoIn}$)} \\
& ~~~~ \times \seqof{\type{P.TxOut^?}} \\
& ~~~~ \text{$\uparrow$ outputs} \\ %\type{P.txInfoOutputs}
& ~~~~ \times \type{P.Value} \\
& ~~~~ \text{$\uparrow$ fee, built by applying $\fun{transValue}\circ\fun{inject}$ to the $\Coin$ fee} \\ %= transValue (inject @(Mary.Value (Crypto era)) fee), \type{P.txInfoFee}
& ~~~~ \times \type{P.Value} \\
& ~~~~ \text{$\uparrow$ mint field, built from the mint $\Value$ by $\fun{transValue}$} \\ % = transValue forge, \type{P.txInfoMint}
& ~~~~ \times \seqof{\type{P.DCert}} \\
& ~~~~ \text{$\uparrow$ list of certificates} \\ %= foldr (\c ans \to transDCert c : ans) [] (certs' tbody), \type{P.txInfoDCert}
& ~~~~ \times (\type{P.StakingCredential} \times \Integer) \\
& ~~~~ \text{$\uparrow$ the $\Wdrl$s, reward withdrawal pairs of credential and reward amount} \\ % = Map.toList (transWdrl (wdrls' tbody)), \type{P.txInfoWdrl}
& ~~~~ \times \type{P.POSIXTimeRange} \\
& ~~~~ \text{$\uparrow$ transaction validity POSIX time range (built by $\fun{transVITime}$)} \\ % = timeRange, \type{P.txInfoValidRange}
& ~~~~ \times \seqof{\type{P.PubKeyHash}} \\
& ~~~~\text{$\uparrow$ hashes of keys whose signature are required} \\ % = map transKeyHash (Set.toList (reqSignerHashes' tbody)), \type{P.txInfoSignatories}
& ~~~~ \times \seqof{(\DataHash \times \Data)} \\
& ~~~~ \text{$\uparrow$ 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{$\uparrow$ list of pairs of datum hashes and their datum preimages}
& ~~~~ \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}
Expand All @@ -175,13 +199,13 @@ \section{TxInfo Construction}
\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)
\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 ~\} \\
& \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
Expand All @@ -191,7 +215,7 @@ \section{TxInfo Construction}
\nextdef
& \fun{txInfoIn} \in \UTxO \to \TxIn \to \type{P.TxInInfo} \\
& \fun{txInfoIn}~ utxo~ txin = \begin{cases}
(\var{txin}_P, \var{txout}_P) & \text{when $(\var{txin}\mapsto\var{txout})\in\var{utxo}$} \\
(\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}
Expand All @@ -215,17 +239,17 @@ \section{TxInfo Construction}
\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 \\
& \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 term 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$}
& \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*}
Expand Down

0 comments on commit 9f9db83

Please sign in to comment.