diff --git a/shelley-mc/formal-spec/frontmatter.tex b/shelley-mc/formal-spec/frontmatter.tex index 7625c047a52..adcf4f30fbf 100644 --- a/shelley-mc/formal-spec/frontmatter.tex +++ b/shelley-mc/formal-spec/frontmatter.tex @@ -17,6 +17,7 @@ \author{ Polina Vinogradova \\ {\small \texttt{polina.vinogradova@iohk.io}} \\ + Andre Knispel \\ {\small \texttt{andre.knispel@iohk.io}} \\ } \date{} diff --git a/shelley-mc/formal-spec/mc-changes.tex b/shelley-mc/formal-spec/mc-changes.tex index fd21a0d4808..e4982dab0b3 100644 --- a/shelley-mc/formal-spec/mc-changes.tex +++ b/shelley-mc/formal-spec/mc-changes.tex @@ -41,7 +41,8 @@ \DeliverableResponsible{Formal Methods Team} %\EditorName{Jared Corduan, \IOHK} \Authors{ - Polina Vinogradova \quad \texttt{polina.vinogradova@iohk.io} + Polina Vinogradova \quad \texttt{polina.vinogradova@iohk.io} \\ + Andre Knispel \quad \texttt{andre.knispel@iohk.io} } %\DueDate{15$^{\textrm{th}}$ October 2019} %\SubmissionDate{8th October 2019}{2019/10/08} @@ -163,7 +164,7 @@ \newcommand{\MetaDataHash}{\type{MetaDataHash}} \newcommand{\MetaData}{\type{MetaData}} \newcommand{\DataHash}{\type{DataHash}} -\newcommand{\ScriptHash}{\type{ScriptHash}} +\newcommand{\PolicyID}{\type{PolicyID}} \newcommand{\PPHash}{\type{PPHash}} \newcommand{\RdmrsHash}{\type{RdmrsHash}} \newcommand{\Script}{\type{Script}} @@ -184,7 +185,7 @@ \newcommand{\MSig}{\type{MSig}} \newcommand{\Credential}{\type{Credential}} \newcommand{\CurrencyId}{\type{CurrencyId}} -\newcommand{\Token}{\type{Token}} +\newcommand{\AssetID}{\type{AssetID}} \newcommand{\CurrencyID}{\type{CurrencyID}} \newcommand{\Quantity}{\type{Quantity}} \newcommand{\QuantityPM}{\type{Quantity}^{\pm}} diff --git a/shelley-mc/formal-spec/mps-language.tex b/shelley-mc/formal-spec/mps-language.tex index f7da5a5df93..32dd207ce07 100644 --- a/shelley-mc/formal-spec/mps-language.tex +++ b/shelley-mc/formal-spec/mps-language.tex @@ -23,7 +23,7 @@ \section{MPS Language} \begin{figure*}[htb] \begin{align*} - & \fun{evalMPSScript} \in\ScriptMPS\to\ScriptHash\to\Slot\to\powerset\KeyHash \\ + & \fun{evalMPSScript} \in\ScriptMPS\to\PolicyID\to\Slot\to\powerset\KeyHash \\ &~~~~\to\TxBody\to\UTxO \to\Bool \\ & \text{UTxO is only for the outputs THIS tx is spending, not global UTxO, i.e.} \\ & \text{when called,}~\var{spentouts}~=~(\fun{txins}~\var{txb}) ~\restrictdom~\var{utxo} \\~\\ diff --git a/shelley-mc/formal-spec/transactions.tex b/shelley-mc/formal-spec/transactions.tex index 5d2899688cc..fb385aa5a47 100644 --- a/shelley-mc/formal-spec/transactions.tex +++ b/shelley-mc/formal-spec/transactions.tex @@ -18,7 +18,7 @@ \section{Transactions} the type scripting language, e.g. $\mathsf{nativeMSigTag}$ and $\mathsf{nativeMCTag}$ - \item $\CurrencyId$ is the identifier of a specific currency. The monetary + \item $\PolicyID$ is the identifier of a specific currency. The monetary policy of a currency with the ID $cid$ is given by the monetary policy script (MPS) $s$, such that $\fun{hashScript}~s~=~cid$. The script is called a monetary policy script because when run, it verifies that the tokens of a currency @@ -27,16 +27,16 @@ \section{Transactions} $\mathsf{True}$, and $\mathsf{False}$ otherwise. More on MPS below. - \item $\Token$ : for each currency ID $cid$, in the MC model, we can associate - some tokens with this currency. A term $t\in\Token$ is an identifier of a + \item $\AssetID$ : for each currency ID $cid$, in the MC model, we can associate + some tokens with this currency. A term $t\in\AssetID$ is an identifier of a kind of token in a given currency $cid$. Within the currency $cid$, - tokens of the same type (with the same identifier $t\in\Token$) are fungible + tokens of the same type (with the same identifier $t\in\AssetID$) are fungible with each other. That is, they are effectively the "same" token, in the same way that every Ada coin is indistinguishable from another Ada coin. Ada has the currency ID $\mathsf{adaID}$. The statement \textit{all of the tokens of this currency must be the same}, in a MC scheme, means that there is only one kind of term of - type $\Token$ associated + type $\AssetID$ associated with $\mathsf{adaID}$, and we call it $\mathsf{adaToken}$. See below for a more detailed discussion of Ada representation. @@ -45,7 +45,7 @@ \section{Transactions} These are not the same tokens and are not fungible with each other. \item $\Quantity$ is an integer type representing an amount. This type is used - specifically to represent an amount of a specific $\Token$. We associate + specifically to represent an amount of a specific $\AssetID$. We associate a term $q\in\Quantity$ with a specific token to keep track of how much of this token there is in a given value. @@ -53,12 +53,13 @@ \section{Transactions} all tokens, including Ada. The key of this finite map type is the hash of the monetary policy script for this currency. A value $v\in\Value$ is a finite map that assciates to each of its - currency ID keys a finite map $tkns\in\Token \mapsto \Quantity$, + currency ID keys a finite map $tkns\in\AssetID \mapsto \Quantity$, which represents all the tokens (of that particular currency) that are contained in $v$. - The map $tkns$ associates to each key $t\in\Token$ the quantity of tokens of - this kind (i.e. with this identifier). + The map $tkns$ associates to each key $t\in\AssetID$ the quantity of tokens of + this kind (i.e. with this identifier). Tokens are fungible with each other if + they belong to the same $\PolicyID$ and $\AssetID$. \item $\TxOut$ : The type of outputs carried by a transaction. This type is different from the Shelley $\TxOut$ type because it contains a $\Value$ @@ -92,14 +93,14 @@ \section{Transactions} \begin{array}{r@{~\in~}l@{\qquad=\qquad}lr} \var{lng} & \Language & \N \\ %\text{script language} - \var{cid} & \CurrencyId & \ScriptHash\\ + \var{pid} & \PolicyID & \PolicyID\\ % \text{currency ID}\\ - \var{tok} & \Token & \mathbb{H}\\ + \var{tok} & \AssetID & \mathbb{H}\\ % \text{token identifier}\\ \var{quan} & \Quantity & \Z \\ %\text{quantity of a token}\\ \var{val} & \Value - & \ScriptHash \mapsto (\Token \mapsto \Quantity) \\ + & \PolicyID \mapsto (\AssetID \mapsto \Quantity) \\ % & \text{a collection of tokens} \var{txout} & \TxOut @@ -166,7 +167,7 @@ \section{Transactions} \\~\\ \var{s_{mc}}\in\ScriptMPS & = & \type{JustMSig}~ \ScriptMSig\\ & \uniondistinct & - \type{MaxMinTimedTotal}~(\Token \mapsto (\Slot\times\Slot\times\Quantity\times\Quantity)) \\ + \type{MaxMinTimedTotal}~(\AssetID \mapsto (\Slot\times\Slot\times\Quantity\times\Quantity)) \\ & \uniondistinct& \type{RequireAll}~\powerset{\ScriptMPS} \end{array} @@ -211,7 +212,7 @@ \section{Transactions} \begin{figure*}[htb] \begin{align*} - \fun{validateScript} & \in\Script\to\ScriptHash\to\Slot\to + \fun{validateScript} & \in\Script\to\PolicyID\to\Slot\to \powerset{\KeyHash}\to\TxBody\to\UTxO\to\Bool \\ \fun{validateScript} & ~s~\var{cid}~\var{slot}~\var{vhks} ~\var{txb}~\var{spentouts} = @@ -345,9 +346,9 @@ \section{Transactions} \emph{Abstract Functions and Values} % \begin{align*} - \mathsf{adaID} \in& ~\ScriptHash + \mathsf{adaID} \in& ~\PolicyID & \text{Ada currency ID} \\ - \mathsf{adaToken} \in& ~\Token + \mathsf{adaToken} \in& ~\AssetID & \text{Ada Token} \\ \mathsf{co} \in& ~\Quantity \to \Coin & \text{type conversion} \\ diff --git a/shelley-mc/formal-spec/utxo.tex b/shelley-mc/formal-spec/utxo.tex index 00d9402e527..ed47ff476b6 100644 --- a/shelley-mc/formal-spec/utxo.tex +++ b/shelley-mc/formal-spec/utxo.tex @@ -51,7 +51,7 @@ \subsection{UTxO Transitions} $0$, and $\epsilon + \epsilon = \epsilon$. Note that this construction has to be iterated twice for the type $\Value$, as -addition on the type $\Token \mapsto \Quantity$ needs to be defined this way first. +addition on the type $\AssetID \mapsto \Quantity$ needs to be defined this way first. This definition of addition is also defined in Section~\ref{sec:notation-shelley}. @@ -78,8 +78,8 @@ \subsection{UTxO Transitions} calculation at the epoch boundary \item - The $\fun{ubalance}$ function calculates the (aggregated by currency ID and - Token) sum total of all the value in a given UTxO. + The $\fun{ubalance}$ function calculates the (aggregated by $\PolicyID$ and + $\AssetID$) sum total of all the value in a given UTxO. \item The $\fun{consumed}$ calculation is still the sum of the reward address value consumed, the values of the UTxO entries consumed, @@ -102,7 +102,7 @@ \subsection{UTxO Transitions} While the preservation of value is a single equality, it is really a comparison of token quantities aggregated by -$\Token$ and by $\CurrencyID$. In particular, ensuring that the produced +$\AssetID$ and by $\PolicyID$. In particular, ensuring that the produced amount equals the consumed amount also implies that the total quantity of Ada tokens is preserved. @@ -233,7 +233,9 @@ \subsection{UTxO Transitions} ~ \\ \mathsf{adaID}~\notin \dom~{\fun{forge}~tx} \\ - \forall txout \in \txouts{txb}, ~ \fun{getValue}~txout ~\geq ~ \epsilon \\~ + \forall txout \in \txouts{txb}, ~ \fun{getValue}~txout ~\geq ~ 0 \\~ + \forall txout \in \txouts{txb}, ~ \fun{getCoin}~txout ~\geq \\ + \fun{valueSize}~(\fun{getValue}~txout) * \fun{minUTxOValue} pp \\~ \\ \fun{txsize}~{tx}\leq\fun{maxTxSize}~\var{pp} \\ @@ -241,10 +243,8 @@ \subsection{UTxO Transitions} \\ \var{refunded} \leteq \keyRefunds{pp}{stkCreds}~{txb} \\ - \var{decayed} \leteq \decayedTx{pp}{stkCreds}~{txb} - \\ \var{depositChange} \leteq - \fun{totalDeposits}~{pp}{stpools}{(\txcerts{txb})} - (\var{refunded} + \var{decayed}) + \fun{totalDeposits}~{pp}{stpools}{\txcerts{txb}} - \var{refunded} } { \begin{array}{r} @@ -268,7 +268,7 @@ \subsection{UTxO Transitions} \begin{array}{r} \varUpdate{(\txins{txb} \subtractdom \var{utxo}) \cup \fun{outs}{txb}} \\ \varUpdate{\var{deposits} + \var{depositChange}} \\ - \varUpdate{\var{fees} + \txfee{txb} + \var{decayed}} \\ + \varUpdate{\var{fees} + \txfee{txb}} \\ \varUpdate{ups'}\\ \end{array} \right) @@ -301,7 +301,7 @@ \subsection{UTxO Transitions} \begin{figure}[htb] \begin{align*} & \hspace{-1cm}\fun{scriptsNeeded} \in \UTxO \to \Tx \to - \powerset{\ScriptHash} + \powerset{\PolicyID} & \text{required script hashes} \\ & \hspace{-1cm}\fun{scriptsNeeded}~\var{utxo}~\var{tx} = \\ & ~~\{ \fun{validatorHash}~a \mid i \mapsto (a, \wcard) \in \var{utxo},\\