Skip to content

Commit

Permalink
Merge pull request #2543 from input-output-hk/andre/alonzo-audit
Browse files Browse the repository at this point in the history 
Alonzo spec fixes
  • Loading branch information
@nc6
nc6 authored Nov 12, 2021
2 parents 3c74bc2 + 539fdae commit ff4bff0
Show file tree
Hide file tree
Showing 6 changed files with 137 additions and 157 deletions.
3 changes: 1 addition & 2 deletions eras/alonzo/formal-spec/alonzo-changes.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -379,8 +379,6 @@

\include{chain}

\include{value-size}

%\include{constants}


Expand All @@ -390,6 +388,7 @@

\begin{appendix}
\include{txinfo}
\include{value-size}
\include{properties}
\end{appendix}

Expand Down
24 changes: 12 additions & 12 deletions eras/alonzo/formal-spec/chain.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -117,35 +117,35 @@ \subsection{Block Body Transition}
\end{figure}

We have also defined a function that transforms the Shelley ledger state into
the corresponding Goguen one, see Figure~\ref{fig:functions:to-shelley}. We
refer to the Shelley-era protocol parameter type as $\ShelleyPParams$, and the corresponding Goguen
the corresponding Alonzo one, see Figure~\ref{fig:functions:to-shelley}. We
refer to the Shelley-era protocol parameter type as $\ShelleyPParams$, and the corresponding Alonzo
type as $\PParams$. We use the notation $\var{chainstate}_{x}$ to represent
variable $x$ in the chain state. We do not specify the variables that
remain unchanged during the transition.

%%
%% Figure - Shelley to Goguen Transition
%% Figure - Shelley to Alonzo Transition
%%
\begin{figure}[htb]
\emph{Types and Constants}
%
\begin{align*}
& \NewParams ~=~ (\Language \mapsto \CostMod) \times \Prices \times \ExUnits \times \ExUnits \\
& \NewParams = (\Language \mapsto \CostMod) \times \Prices \times \ExUnits \times \ExUnits \\
& ~~~~~~~~ \times \N \times \Coin \times \N \times \N \\
& \text{the type of new parameters to add for Goguen}
& \text{the type of new parameters to add for Alonzo}
\nextdef
& \var{ivPP} ~\in~ \NewParams \\
& \text{the initial values for new Goguen parameters}
& \var{ivPP} \in \NewParams \\
& \text{the initial values for new Alonzo parameters}
\end{align*}
\emph{Shelley to Goguen Transition Functions}
\emph{Shelley to Alonzo Transition Functions}
%
\begin{align*}
& \fun{toGoguen} \in \ShelleyChainState \to \ChainState \\
& \fun{toGoguen}~\var{chainstate} =~\var{chainstate'} \\
& \fun{toAlonzo} : \ShelleyChainState \to \ChainState \\
& \fun{toAlonzo}~\var{chainstate} =~\var{chainstate'} \\
&~~\where \\
&~~~~\var{chainstate'}_{pparams}~=~(\var{pp}\cup \var{ivPP})~ - ~\var{minUTxOValue}\\
& \text{transform Shelley chain state to Goguen state}
& \text{transform Shelley chain state to Alonzo state}
\end{align*}
\caption{Shelley to Goguen State Transtition}
\caption{Shelley to Alonzo State Transtition}
\label{fig:functions:to-shelley}
\end{figure}
19 changes: 6 additions & 13 deletions eras/alonzo/formal-spec/introduction.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,21 +44,14 @@ \subsection{Phase Two Scripts}
distinct from the usual ``gas'' model in the following notable ways :

\begin{itemize}
\item The exact budget to run a script is expressed in terms of computational resources,
and included in the transaction data. This resource budget can be computed before submitting a transaction.
In contrast with the gas model, where the budget is expressed indirectly,
in terms of an upper bound on the fee the author is willing to pay for execution of the
\item The budget to run a script is expressed in terms of computational resources,
and included in the transaction data. The \emph{exact} resource budget required can
be computed before submitting a transaction, since script execution is deterministic.
See Section \ref{sec:determinism}.
In the gas model, the budget is expressed indirectly as an upper bound
on the fee the submitter is willing to pay for execution of the
contract (eg. their total available funds).

\item The exact total fee a transaction is paying is also specified in the transaction data.
For a transaction to be valid, this fee must cover the script-running resource budget at the current price,
as well as the size-based part of the required fee.
If the fee is not sufficient to cover the resource budget specified (eg. if the resource price increased),
the transaction is considered invalid and \emph{will not appear on the ledger (will not be included in a valid block)}.
No fees will be collected in this case.
This is in contrast with the gas model, where, if prices go up, a greater fee will be charged - up to
the maximum available funds, even if they are not sufficient to cover the cost of the execution of the contract.

\item The user specifies the UTxO entries containing funds sufficient to cover a percentage
(usually $100$ or more) of the total transaction fee.
These inputs are only collected \emph{in the case of script validation failure},
Expand Down
47 changes: 21 additions & 26 deletions eras/alonzo/formal-spec/protocol-parameters.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,27 +6,26 @@ \section{Language Versions and Cost Models}

\vspace{12pt}
\begin{tabular}{lp{5in}}
$\ExUnits$ &
$\ExUnits$ is made up of two integer values, representing abstract notions of the
relative memory usage and script execution steps respectively.
We give it the structure of a partially ordered monoid via its product structure,
i.e. addition and comparisons are defined point-wise.
\\
$\Prices$ &
$\Prices$ consists of two rational numbers that correspond to the components of $\ExUnits$:
the price per unit of memory and price per reduction step.
\\
$\CostMod$ &
$c\in\CostMod$ is the vector of coefficients that are used to compute
a value $exu\in\ExUnits$ given a vector of some resource primitives. The mapping is defined
concretely by the specific version of the Plutus interpreter that is associated with $\Language$.
A cost model is a vector of coefficients that are used to compute
the execution units required to execute a script. Its specifics depend on
specific versions of the Plutus interpreter it is used with.
We keep this type as abstract in the specification, see \cite{plutuscore} and \cite{plutustech}
for details.
\\
$\Language$ &
This represents phase-2 language types. Currently there is only $\PlutusVI$.
\\
$\Prices$ &
$\var{(pr_{mem}, pr_{steps})}\in \Prices$ consists of two rational numbers
that correspond to the components of $\ExUnits$:
$pr_{mem}$ is the price per unit of memory, and $pr_{steps}$ is the price per
reduction step. This is used to calculate the cost for a specific script execution.
\\
$\ExUnits$ &
$(mem, steps)\in \ExUnits$ is made up of two integer values.
These represent abstract notions of the relative memory usage and script execution steps,
respectively. We give it the structure of a partially ordered monoid via its product structure, i.e. addition and comparisons are defined point-wise.
\\
$\LangDepView$ &
A pair of two byte strings, where the first represents the serialized language tag (eg. the tag for $\PlutusVI$),
and the second, the protocol parameters that must be fixed (by the transaction) when carrying a phase-2 script
Expand Down Expand Up @@ -124,31 +123,27 @@ \subsection{Script Evaluation Cost Model and Prices}
\emph{Abstract types}
%
\begin{equation*}
\begin{array}{r@{~\in~}l@{\qquad\qquad\qquad}r}
\var{cm} & \CostMod & \text{Coefficients for the cost model}
\begin{array}{l@{\qquad\qquad\qquad}r}
\CostMod & \text{Coefficients for the cost model}
\end{array}
\end{equation*}
%
\emph{Derived types}
\begin{equation*}
\begin{array}{r@{~\in~}l@{\quad=\quad}l@{\qquad}r}
\var{lg}
& \Language
\begin{array}{l@{\quad=\quad}l@{\qquad}r}
\Language
& \{\PlutusVI, \dotsb\}
& \text{Script Language}
\\
\var{(pr_{mem}, pr_{steps})}
& \Prices
\Prices
& \mathsf{Rational} \times \mathsf{Rational}
& \text {Coefficients for $\ExUnits$ prices}
\\
\var{(mem, steps)}
& \ExUnits
\ExUnits
& \N \times \N
& \text{Abstract execution units}
\\
\var{ldv}
& \LangDepView
\LangDepView
& \ByteString~\times~\ByteString
& \text{Language Tag and PParams view}
\end{array}
Expand Down Expand Up @@ -195,7 +190,7 @@ \subsection{Script Evaluation Cost Model and Prices}
\emph{Helper Functions}
%
\begin{align*}
& \fun{getLanguageView} \in \PParams \to \Language \to \LangDepView \\
& \fun{getLanguageView} : \PParams \to \Language \to \LangDepView \\
& \fun{getLanguageView}~\var{pp}~\PlutusVI = (\fun{serialize}~\PlutusVI, ~ (\fun{serialize}~(\fun{costmdls}~{pp}~\{\PlutusVI\})))
\end{align*}
\caption{Definitions Used in Protocol Parameters}
Expand Down
93 changes: 43 additions & 50 deletions eras/alonzo/formal-spec/transactions.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -68,66 +68,59 @@ \section{Transactions}
\emph{Abstract types}
%
\begin{equation*}
\begin{array}{r@{~\in~}l@{\quad\quad\quad\quad}r}
\var{wph} &\ScriptIntegrityHash & \text{Script data hash}\\
\var{plc} & \ScriptPlutus & \text{Plutus core scripts} \\
\var{d} & \Data & \text{Generic script data}
\begin{array}{l@{\quad\quad\quad\quad}r}
\ScriptIntegrityHash & \text{Script data hash}\\
\ScriptPlutus & \text{Plutus core scripts} \\
\Data & \text{Generic script data}
\end{array}
\end{equation*}
%
\emph{Script types}
%
\begin{equation*}
\begin{array}{r@{~\in~}l@{\qquad=\qquad}lr}
\var{sc} & \ScriptPhTwo & \ScriptPlutus \\
\var{sc} & \Script & \ScriptPhOne \uniondistinct \ScriptPhTwo \\
\var{isv} & \IsValid & \Bool \\
\var{d} & \Datum & \Data \\
\var{r} & \Redeemer & \Data
\begin{array}{l@{\qquad=\qquad}lr}
\ScriptPhTwo & \ScriptPlutus \\
\Script & \ScriptPhOne \uniondistinct \ScriptPhTwo \\
\IsValid & \Bool \\
\Datum & \Data \\
\Redeemer & \Data
\end{array}
\end{equation*}
%
\emph{Derived types}
%
\begin{equation*}
\begin{array}{r@{~\in~}l@{\qquad=\qquad}lr}
\var{vi}
& \ValidityInterval
\begin{array}{l@{\qquad=\qquad}lr}
\ValidityInterval
& \Slot^? \times \Slot^?
% & \text{validity interval}
\\
\var{txout}
& \TxOut
\TxOut
& \Addr \times \Value \times \hldiff{\DataHash^?}
% & \text{transaction outputs in a transaction}
\\
\var{tag}
& \Tag
\Tag
& \{\mathsf{Spend},~\mathsf{Mint},~\mathsf{Cert},~\mathsf{Rewrd}\}
\\
\var{rdptr}
& \RdmrPtr
\RdmrPtr
& \Tag \times \Ix
% & \text{reverse pointer to thing dv is for}
\end{array}
\end{equation*}
%
\emph{Helper Functions}
%
\begin{align*}
\fun{language}& \in \Script \to \Language^?\\
\fun{hashData}& \in \Data \to \DataHash
\fun{language}& : \Script \to \Language^?\\
\fun{hashData}& : \Data \to \DataHash
\nextdef
\fun{getCoin}& \in \TxOut \to \Coin \\
\fun{getCoin}&~\hldiff{{(\_, \var{v}, \_)}} ~=~\fun{valueToCoin}~{v}
\fun{getCoin}& : \TxOut \to \Coin \\
\fun{getCoin}&~\hldiff{{(\_, \var{v}, \_)}} = \fun{valueToCoin}~{v}
\end{align*}
%
\begin{align*}
&\fun{hashScriptIntegrity} \in\PParams \to \powerset{\Language} \to (\RdmrPtr \mapsto \Redeemer \times \ExUnits) \\
&\fun{hashScriptIntegrity} : \PParams \to \powerset{\Language} \to (\RdmrPtr \mapsto \Redeemer \times \ExUnits) \\
&~~~~ \to (\DataHash \mapsto \Datum) \to \ScriptIntegrityHash^? \\
&\fun{hashScriptIntegrity}~{pp}~{langs}~{rdmrs}~{dats}~=~ \\
&\fun{hashScriptIntegrity}~{pp}~{langs}~{rdmrs}~{dats} = \\
&~~~~ \begin{cases}
\Nothing & rdmrs~=~\emptyset \land langs~=~\emptyset \land dats~=~\emptyset \\
\Nothing & rdmrs = \emptyset \land langs = \emptyset \land dats = \emptyset \\
\fun{hash} (rdmrs, dats, \{ \fun{getLanguageView}~pp~l \mid l \in langs \}) & \text{otherwise}
\end{cases}
\end{align*}
Expand All @@ -141,18 +134,18 @@ \section{Transactions}
%
\begin{equation*}
\begin{array}{r@{~~}l@{~~}l@{\qquad}l}
\var{wits} ~\in~ \TxWitness ~=~
\TxWitness =
& (\VKey \mapsto \Sig) & \fun{txwitsVKey} & \text{VKey signatures}\\
& \times ~(\ScriptHash \mapsto \Script) & \fun{txscripts} & \text{All scripts}\\
& \times~ \hldiff{(\DataHash \mapsto \Datum)} & \hldiff{\fun{txdats}} & \text{All datum objects}\\
& \times ~\hldiff{(\RdmrPtr \mapsto \Redeemer \times \ExUnits)}& \hldiff{\fun{txrdmrs}}& \text{Redeemers/budget}\\
& \times ~\hldiff{(\RdmrPtr \mapsto \Redeemer \times \ExUnits)}& \hldiff{\fun{txrdmrs}}& \text{Redeemers/budget}
\end{array}
\end{equation*}
%
\begin{equation*}
\begin{array}{r@{~~}l@{~~}l@{\qquad}l}
\var{txbody} ~\in~ \TxBody ~=~
& \powerset{\TxIn} & \fun{txinputs}& \text{Inputs}\\
\TxBody =
& \powerset{\TxIn} & \fun{txins}& \text{Inputs}\\
& \times ~\hldiff{\powerset{\TxIn}} & \hldiff{\fun{collateral}} & \text{Collateral inputs}\\
& \times ~(\Ix \mapsto \TxOut) & \fun{txouts}& \text{Outputs}\\
& \times~ \seqof{\DCert} & \fun{txcerts}& \text{Certificates}\\
Expand All @@ -170,7 +163,7 @@ \section{Transactions}
%
\begin{equation*}
\begin{array}{r@{~~}l@{~~}l@{\qquad}l}
\var{tx} ~\in~ \Tx ~=~
\Tx =
& \TxBody & \fun{txbody} & \text{Body}\\
& \times ~\TxWitness & \fun{txwits} & \text{Witnesses}\\
& \times ~\hldiff{\IsValid} & \hldiff{\fun{isValid}}&\text{Validation tag}\\
Expand Down Expand Up @@ -224,12 +217,14 @@ \subsection{Transactions}
that are collected (into the fee pot) to cover a percentage of
transaction fees (usually $100$ percent or more)
\emph{in case the transaction contains failing phase-2 scripts}. They are not collected otherwise.
The purpose of these is to cover the resource use costs incurred by block producers running not only
scripts that validate, but the failing one also. Only the inputs that are locked by VKeys can
be used for collateral, and they must only contain Ada.
The purpose of the collateral is to cover the resource use costs
incurred by block producers running scripts that do not validate.

Collateral inputs behave like regular inputs, except that they
must be VKey locked and can only contain Ada. See \ref{fig:functions:utxo}.

It is permitted to use the same inputs as both collateral and a regular inputs, as exactly
one set of inputs is ever collected : collateral ones in the case of script failure, and regular inputs
one set of inputs is ever collected: collateral ones in the case of script failure, and regular inputs
in the case when all scripts validate.

\item There is a new field called $\fun{reqSignerHashes}$ that is used to specify a set of hashes
Expand Down Expand Up @@ -261,18 +256,16 @@ \subsection{Transactions}
that are executed during the script execution phase validate.
The correctness of the tag is verified as part of the ledger rules, and the block is
deemed to be invalid if it is applied incorrectly.
If it is set to $\False$, then the block can be re-applied without script re-validation.
This tag cannot be signed, since it is applied by the block producer.
It can be used to re-apply blocks without script re-validation.
Since this tag is not part of the body, i.e. it is not signed, the block producer can
(and must) choose the correct value.
\item any auxiliary data.
\end{enumerate}

Note that unlike in Shelley or ShelleyMA eras, transactions inside blocks and transactions
a user submits are now of different types. A transaction inside a block is composed of
the user-submitted transaction paired with the $\IsValid$ tag, which is
added by the block producer. The user cannot
add their own tag because of how this tag is used in transaction validation, see
Section~\ref{sec:two-phase}.

\begin{note}
In the implementation the $\IsValid$ tag is part of a user-submitted
transaction, but it is ignored and re-computed by the block
producer.
\end{note}
\subsection{Additional Role of Signatures on TxBody}

The transaction body and the UTxO must uniquely determine all the data
Expand All @@ -287,14 +280,14 @@ \subsection{Additional Role of Signatures on TxBody}
certificates, minting policies, and reward addresses do not need to be signed.
The optional datum objects, however, could be stripped from the transaction without making
it invalid. The optional datums are stored in the same map the required ones, so,
for this reason, we do include all datum objects in the witness and PP hash calculation.
for this reason, we do include all datum objects in the script integrity hash calculation.
%
The hash of the indexed redeemer structure and the protocol parameters that are used by
script interpreters are included in the body of the transaction, as these are composed
by the transaction author rather than
fixed via a hash on the ledger. In the future, other parts of the ledger
state may also need to be included in this hash, if they are passed as
arguments to new script interpreter.
arguments to a new script interpreter.

\subsection{Data required for script validation.}
\label{sec:script-data}
Expand Down
Loading

0 comments on commit ff4bff0

Please sign in to comment.