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.

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

Address audit comments and introduce protocol parameters #1938

Merged
merged 2 commits into from
Oct 28, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
23 changes: 14 additions & 9 deletions shelley-ma/formal-spec/chain.tex
Original file line number Diff line number Diff line change
Expand Up @@ -54,25 +54,30 @@ \section{Blockchain layer}
In Figure~\ref{fig:functions:to-ma}, we give the functions that will be used
to transition from a Shelley chain state into a chain state that provides multi-asset support.
The only part of the state that is affected by the transition is the UTxO. For ease of
reading, we use different notation here to define the UTxO update, and specify
explicitly only the change to the UTxO, implying that every other part of the
state is unaffected.
reading, we keep the function $\fun{updateChainStateUTxO}$ abstract, which simply transforms the
UTxO that is nested deeply inside the chain state with the provided function.

%%
%% Figure - Shelley to MA Transition
%%
\begin{figure}[htb]
%
\emph{Abstract function}
%
\begin{align*}
& \fun{updateChainStateUTxO} \in (\ShelleyUTxO \to \UTxO) \to \ShelleyChainState \to \ChainState \\
& \text{update the UTxO in a Shelley chain state}
\end{align*}
%
\emph{Chain state update}
%
\begin{align*}
& \fun{mkUTxO} ~\in~ \ShelleyUTxO \to \UTxO \\
& \fun{mkUTxO}~\var{utxo} ~=~ \{~ \var{txin} \mapsto (a,\fun{coinToValue}~c) ~\vert~
\var{txin} \mapsto \var{(a,c)}\in ~\var{utxo}~\} \\
& \text{make UTxO with MA}
\var{txin} \mapsto \var{(a,c)}\in ~\var{utxo}~\}
\nextdef
& \fun{toMA} \in ~ \ShelleyChainState \to \ChainState \\
& \fun{toMA}~cs = cs' \\
& \where \\
& ~~~~ cs'_{utxo} = \fun{mkUTxO}~\var{utxo} \\
& \text{transform Shelley chain state to a MA-supporting state}
& \fun{toMA}~cs = \fun{updateChainStateUTxO}~\fun{mkUTxO}
\end{align*}
\caption{Shelley to Multi-Asset Chain State Transtition}
\label{fig:functions:to-ma}
Expand Down
2 changes: 1 addition & 1 deletion shelley-ma/formal-spec/epoch.tex
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ \section{Rewards and the Epoch Boundary}
& \where \\
& ~~~~ (~\var{rewards},~\var{delegations},~\var{ptrs},~\wcard,~\wcard,~\wcard)
= \var{dstate} \\
& ~~~~ (~\var{poolParams}~\wcard,~\wcard) = \var{pstate} \\
& ~~~~ (~\var{poolParams},~\wcard,~\wcard) = \var{pstate} \\
& ~~~~ \var{stakeRelation} = \left(
\left(\fun{stakeCred_b}^{-1}\cup\left(\fun{addrPtr}\circ\var{ptr}\right)^{-1}\right)
\circ\left(\hldiff{\fun{utxoAda}}~{\var{utxo}}\right)
Expand Down
7 changes: 3 additions & 4 deletions shelley-ma/formal-spec/mps-language.tex
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,9 @@ \section{Script Constructors and Evaluation}
\begin{align*}
\fun{validateScript} & \in\Script\to
\powerset{\KeyHash}\to\TxBody\to\Bool \\
\fun{validateScript} & ~s~\var{vhks}~\var{txb}
~\var{txb}~\var{utxo} =
\fun{validateScript} & ~s~\var{vhks}~\var{txb}~=
\begin{cases}
\fun{evalMultiSigScript}~s~vhks & \text{if}~s \in\ScriptMSig \\
\fun{evalMultiSigScript}~s~vhks & \text{if}~s \in\ScriptNI \\
\fun{evalFPS}~s~\var{vhks} ~txb & \text{if}~s \in\ScriptMPS \\
\mathsf{False} & \text{otherwise}
\end{cases}
Expand All @@ -21,7 +20,7 @@ \section{Script Constructors and Evaluation}
We have updated the
$\fun{validateScripts}$ function, to allow for the validation of both the
multi-signature scripts and forging policy scripts, calling the appropriate
evaluator for each type of script, see~\ref{fig:functions-validate}.
evaluator for each type of script, see Figure~\ref{fig:functions-validate}.

\begin{note}
This appendix will change if we change anything about the language, it will go
Expand Down
31 changes: 31 additions & 0 deletions shelley-ma/formal-spec/protocol-parameters.tex
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
\section{Protocol Parameters}

In Shelley, the size of a UTxO entry was bounded from above, which
will not be the case anymore. The protocol parameter
$\var{minUTxOValue}$ was used to prevent an attack on the UTxO size,
but as there is no upper bound on the memory usage of a UTxO entry
anymore, this parameter will be retired in favor of two new
parameters, $\var{adaPerUTxOByte}$ and $\var{outputSizeConstants}$.


\begin{figure*}[htb]
\emph{Protocol Parameters}
%
\begin{equation*}
\begin{array}{r@{~\in~}lr}
\var{adaPerUTxOByte} \mapsto \nonnegReals & \PParams & \text{conversion factor for UTxO storage space}\\
\var{outputSizeConstants} \mapsto \Z \times \Z \times \Z & \PParams & \text{constants for outputSize}
\end{array}
\end{equation*}
%
\emph{Accessor Functions}
%
\begin{center}
\fun{adaPerUTxOByte},
\fun{outputSizeConstants}
\end{center}
%
\caption{Definitions Used in Protocol Parameters}
\label{fig:defs:protocol-parameters}
\end{figure*}

4 changes: 3 additions & 1 deletion shelley-ma/formal-spec/shelley-ma.tex
Original file line number Diff line number Diff line change
Expand Up @@ -178,7 +178,8 @@
\newcommand{\RdmrsHash}{\type{RdmrsHash}}
\newcommand{\Script}{\type{Script}}
\newcommand{\ScriptPlutus}{\type{Script}_{plc}}
\newcommand{\ScriptMPS}{\type{Script}_{fps}}
\newcommand{\ScriptNI}{\type{Script^{native}_{v1}}}
\newcommand{\ScriptMPS}{\type{Script^{native}_{v2}}}
\newcommand{\ScriptMSig}{\type{Script}_{msig}}
\newcommand{\ScriptV}{\type{Script_{v}}}
\newcommand{\Datum}{\type{Datum}}
Expand Down Expand Up @@ -359,6 +360,7 @@
\include{introduction}
\include{notation}
\include{value}
\include{protocol-parameters}
\include{transactions}

\include{utxo}
Expand Down
15 changes: 8 additions & 7 deletions shelley-ma/formal-spec/transactions.tex
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,8 @@
%
\begin{equation*}
\begin{array}{r@{~\in~}l@{\qquad=\qquad}lr}
\var{s_{fps}} & \ScriptMPS & \text{extended script language}
\\
\var{s_{v1}} & \ScriptNI & \ScriptMSig \\
\var{s_{v2}} & \ScriptMPS & \text{extended script language}
\end{array}
\end{equation*}
%
Expand All @@ -15,7 +15,7 @@
\begin{array}{r@{~\in~}l@{\qquad=\qquad}lr}
\var{txout} & \TxOut & \Addr \times \hldiff{\Value} \\
% & \text{tx outputs}
\var{s} & \Script & \hldiff{\ScriptMSig \uniondistinct \ScriptMPS}
\var{s} & \Script & \hldiff{\ScriptNI \uniondistinct \ScriptMPS}
% & \text{scripts}
\\
\end{array}
Expand All @@ -31,9 +31,9 @@
& \times~ \seqof{\DCert} & \fun{txcerts}& \text{certificates}\\
& \times ~\hldiff{\Value} & \hldiff{\fun{forge}} &\text{value forged}\\
& \times ~\Coin & \fun{txfee} &\text{non-script fee}\\
& \times ~\hldiff{\Slot^? \times \Slot^?} & \fun{txvldt} & \text{validity interval}\\
& \times ~\hldiff{\Slot^? \times \Slot^?} & \hldiff{\fun{txvldt}} & \text{validity interval}\\
& \times~ \Wdrl & \fun{txwdrls} &\text{reward withdrawals}\\
& \times ~\Update & \fun{txUpdates} & \text{update proposals}\\
& \times ~\Update^? & \fun{txUpdates} & \text{update proposals}\\
& \times ~\MetaDataHash^? & \fun{txMDhash} & \text{metadata hash}
\end{array}
\end{equation*}
Expand Down Expand Up @@ -66,13 +66,14 @@ \subsection*{New Output Type}

\subsection*{New Script Type}

The type $\Script$ has been extended to include a new scripting language,
The multi-signature scripting language has been renamed to $\ScriptNI$ and
the type $\Script$ has been extended to include a new scripting language,
$\ScriptMPS$. The two types of scripts which make up the $\Script$ type are both
native, meaning
that they are evaluated by the ledger directly. We specify the evaluation
function for the additional script type in section~\ref{sec:mps-lang}.

Both types of scripts can be used in the exact same way, which means, for this
Both types of scripts can be used for the same purposes, which means, for this
spec, as

\begin{itemize}
Expand Down
14 changes: 3 additions & 11 deletions shelley-ma/formal-spec/utxo.tex
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,7 @@ \subsection*{The UTXO Transition Rule}
\item The transaction is not forging any Ada.

\item The $\Value$ of each output is constrained from below by a
$\Value$ that contains the product of $\var{minUTxOValue}$ and the
$\Value$ that contains the product of $\var{adaPerUTxOByte}$ and the
estimated size of the output as Ada, and zero otherwise. Note that
this implies that no quantity appearing in that output can be
negative.
Expand Down Expand Up @@ -155,10 +155,10 @@ \subsection*{The UTXO Transition Rule}
\\
~
\\
\hldiff{\mathsf{adaPolicy}~\notin \supp{\fun{forge}~tx}} \\
\hldiff{\mathsf{adaPolicy}~\notin \supp{\fun{forge}~txb}} \\
~\\
\hldiff{\forall txout \in \txouts{txb},} \\
\hldiff{txout \geq \fun{coinToValue}(\fun{outputSize}~{txout} * \fun{minUTxOValue}~pp)} \\~
\hldiff{txout \geq \fun{coinToValue}(\fun{outputSize}~{txout} * \fun{adaPerUTxOByte}~pp)} \\~
\\
\forall (\wcard\mapsto (a,~\wcard)) \in \txouts{txb}, \fun{netId}~a =\NetworkId
\\
Expand Down Expand Up @@ -241,11 +241,3 @@ \subsection*{Witnessing}
(forging, output-locking, etc.).
All scripts are run in the same way, with $\fun{validateScript}$ being responsible
for calling the evaluator appropriate for the specific type of script.

\begin{note}
The cost model for the new script type is non-existent, the bigger scripts
cost more only because they increase the size of the transaction.

This could be a problem with arbitrary ORs! Checking lots of things before
concluding the script fails could be bad
\end{note}
8 changes: 5 additions & 3 deletions shelley-ma/formal-spec/value-size.tex
Original file line number Diff line number Diff line change
Expand Up @@ -18,10 +18,12 @@ \section{Output Size}

\begin{figure*}[h]
\begin{align*}
& \fun{outputSize} \in \TxOut \to \MemoryEstimate \\
& \fun{outputSize} ~\var{out} = k_0 + k_1 * |\{ (\var{pid}, \var{aid}) : \var{v}~\var{pid}~\var{aid} \neq 0
& \fun{outputSize} \in \PParams \to \TxOut \to \MemoryEstimate \\
& \fun{outputSize}~{pp}~\var{out} = k_0 + k_1 * |\{ (\var{pid}, \var{aid}) : \var{v}~\var{pid}~\var{aid} \neq 0
\land (\var{pid}, \var{aid}) \neq (\mathsf{adaPolicy}, \mathsf{adaName}) \}| \\
& \phantom{\fun{outputSize} ~\var{out} = k_0} + k_2 * |\{ \var{pid} : \exists aid : v~pid~aid \neq 0 \}|
& \phantom{\fun{outputSize}~{pp}~\var{out} = k_0} + k_2 * |\{ \var{pid} : \exists aid : v~pid~aid \neq 0 \}| \\
& ~~\where \\
& ~~~~~~(k_0, k_1, k_2) = \fun{outputSizeConstants}~{pp}
\end{align*}
\caption{Value Size}
\label{fig:test}
Expand Down
4 changes: 3 additions & 1 deletion shelley-ma/formal-spec/value.tex
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ \section{Coin and Multi-Asset Tokens}
%
\begin{align*}
\mathsf{adaPolicy} \in& ~\PolicyID & \text{Ada Policy ID} \\
\mathsf{adaName} \in& ~\AssetName & \text{Ada Asset Name} \\
\mathsf{adaName} \in& ~\AssetName & \text{Ada Asset Name}
\end{align*}
\emph{Helper Functions}
%
Expand Down Expand Up @@ -86,6 +86,8 @@ \subsection*{Representing Multi-asset Types and Values}
\emph{token bundles}.

\item $\mathsf{adaPolicy}$ and $\mathsf{adaName}$ are the $\PolicyID$ and $\AssetName$ of Ada respectively.
It is not possible to forge any token with the $\PolicyID$ $\mathsf{adaPolicy}$, which means that every
token in the UTxO belonging to $\mathsf{adaPolicy}$ will have $\AssetName$ $\mathsf{adaName}$.

\item $\fun{coinToValue}$ and $\fun{valueToCoin}$ convert between the two types,
by taking a $\Coin$ to a $\Value$ that only contains Ada, and extracting the amount of Ada from a $\Value$ respectively.
Expand Down