Merge pull request #1619 from input-output-hk/origin/andre/plutus-spe…

…c-changes

Various changes and additions requested by Polina

goguen/formal-spec/frontmatter.tex

@@ -24,6 +24,7 @@
 
 \author{
    Polina Vinogradova \\ {\small \texttt{[email protected]}} \\
+   Andre Knispel \\ {\small \texttt{[email protected]}} \\
    }
 
 \date{}

goguen/formal-spec/goguen-changes.tex

@@ -40,7 +40,8 @@
 \DeliverableResponsible{Formal Methods Team}
 %\EditorName{Jared Corduan, \IOHK}
 \Authors{
-   Polina Vinogradova \quad \texttt{[email protected]}
+   Polina Vinogradova \quad \texttt{[email protected]} \\
+   Andre Knispel \quad \texttt{[email protected]}
 }
 %\DueDate{15$^{\textrm{th}}$ October 2019}
 %\SubmissionDate{8th October 2019}{2019/10/08}
@@ -162,7 +163,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}}
@@ -182,7 +183,7 @@
 \newcommand{\MSig}{\type{MSig}}
 \newcommand{\Credential}{\type{Credential}}
 \newcommand{\CurrencyId}{\type{CurrencyId}}
-\newcommand{\Token}{\type{Token}}
+\newcommand{\AssetID}{\type{AssetID}}
 \newcommand{\Quantity}{\type{Quantity}}
 \newcommand{\QuantityPM}{\type{Quantity}^{\pm}}
 \newcommand{\ValuePM}{\type{Value}^{\pm}}
@@ -353,4 +354,8 @@
 \bibliographystyle{plainnat}
 \bibliography{references}
 
+\begin{appendix}
+  \include{properties}
+\end{appendix}
+
 \end{document}

goguen/formal-spec/properties.tex

@@ -0,0 +1,24 @@
+\section{Properties of the Goguen Ledger}
+\label{sec:properties}
+
+This section collects properties that the ledger described previously
+is expected to satisfy.
+
+\begin{itemize}
+\item Any token with the $\PolicyID$ of Ada is an Ada token, i.e. it
+  also has the $\AssetID$ of Ada.
+\item The general accounting property holds with any transaction,
+  whether it is fully processed or just paying fees. In particular,
+  this implies that the total amount of Ada in the system is constant.
+\item If a transaction is accepted and marked as paying fees only
+  (i.e. $\fun{txvaltag}\, tx \in \Yes$), then the only change to the ledger
+  when processing the transaction is that the inputs marked for paying
+  fees are moved to the fee pot.
+\item If a Shelley transaction is accepted, it is fully processed.
+\item If a transaction extends the UTxO, all its scripts validate, and
+  if it has a script that does not validate, it cannot extend the
+  UTxO.
+\item A valid transaction that does not forge tokens satisfies the
+  accounting property of the Shelley ledger where the type $\Coin$ is
+  replaced by $\Value$.
+\end{itemize}

goguen/formal-spec/transactions.tex

@@ -14,13 +14,13 @@ \section{Transactions}
 except for the following changes and additions:
 
 \begin{itemize}
-  \item $\ScriptHash$ is the type of hashes
+  \item $\PolicyID$ is the type of hashes
   of Plutus and MSig scripts (and any other scripts added in the future)
 
   \item $\RdmrsHash$ is the type of hashes of the indexed redeemer structure
   included in the transaction (details about this structure below)
 
-  \item $\Token,~\Quantity$ are types
+  \item $\AssetID,~\Quantity$ are types
   related to native multicurrency on the ledger.
 
   \item  $\ScriptMSig$ is the native multisignature scripts already supported.
@@ -58,10 +58,10 @@ \section{Transactions}
   \item $\Value$ is the multicurrency type used to represent
   both fungible and non fungible tokens. The key of this finite map type is
   the hash of the monetary policy script for tokens of this currency.
-  This hash is referred to as the ID of the currency. Within a single
-  currency, there may be tokens with different token identifiers
-  (of type $\Token$). Tokens with different currency IDs
-  or different token identifiers are not fungible with each other.
+  This hash is referred to as the $\PolicyID$ of the currency. Within a single
+  currency, tokens belong to an $\AssetID$, which is assigned at the creation
+  the token and can be controlled by monetary policy script. Tokens with different
+  $\PolicyID$s or different $\AssetID$s are not fungible with each other.
   See the note below for a discussion of Ada representation.
 
   \item $\IsFee$ is a tag that indicates when an input has been marked
@@ -166,14 +166,15 @@ \section{Transactions}
   %
   \begin{equation*}
     \begin{array}{r@{~\in~}lr}
-      \var{h} &\ScriptHash & \text{ script hash}\\
+      \var{polid} &\PolicyID & \text{hash of policy scripts}\\
       \var{hdv} &\RdmrsHash & \text{hash of the indexed redeemers structure}\\
-      \var{tok} & \Token & \text{token identifier}\\
+      \var{assetid} & \AssetID & \text{asset identifier}\\
       \var{quan} & \Quantity & \text{quantity of a token}\\
       \var{msig} & \ScriptMSig & \text{Multisig scripts} \\
       \var{plc} & \ScriptPlutus & \text{Plutus scripts of initial Plutus version} \\
       \var{yes} & \Yes & \text{tag type for yes} \\
       \var{no} & \Nope & \text{tag type for no} \\
+      \var{dat} & \Data & \text{the $\Data$ type} \\
     \end{array}
   \end{equation*}
   %
@@ -188,11 +189,6 @@ \section{Transactions}
     \begin{array}{r@{~\in~}l@{\qquad=\qquad}lr}
       \var{scr} & \Script & \ScriptPlutus \uniondistinct \ScriptMSig \\
       \var{isv} & \IsValidating & \Yes \uniondistinct \Nope \\
-      \var{dat}
-      & \Data
-      & \mathbb{N}\uniondistinct\mathbb{H}\uniondistinct(\mathbb{N}\times\seqof{\Data})
-        \uniondistinct\seqof{\Data}\uniondistinct\seqof{\Data \times \Data}
-%      & \text{the $\Data$ type}\\
     \end{array}
   \end{equation*}
 %
@@ -201,7 +197,7 @@ \section{Transactions}
   \begin{equation*}
     \begin{array}{r@{~\in~}l@{\qquad=\qquad}lr}
       \var{val} & \Value
-      & \ScriptHash \mapsto (\Token \mapsto \Quantity)
+      & \PolicyID \mapsto (\AssetID \mapsto \Quantity)
 %      & \text{a collection of tokens}
       \\
       \var{isf}
@@ -269,18 +265,7 @@ \section{Transactions}
 \textbf{Data Representation.}
 The type $\Data$ is a Plutus type, however, there is a similar type in the
 ledger. We do not assume these are the same $\Data$, but we do assume there
-is structural equality between them. Often we must represent the empty type,
-$\Nothing$, as a term of type $\Data$. We use the notation defined in
-Figure \ref{fig:defs:todata} to do this.
-
-\begin{figure*}[htb]
-  \begin{align*}
-    \Nothing_d ~\in~& \Data \\
-    & \text{the Data representation of empty type} \\
-  \end{align*}
-  \caption{Empty Data Representation}
-  \label{fig:defs:todata}
-\end{figure*}
+is structural equality between them.
 
 \textbf{Witnessing.}
 In Figure \ref{fig:defs:utxo-shelley-2}, the type $\TxWitness$ contains everything
@@ -556,7 +541,7 @@ \section{Transactions}
 is an implementation detail, which we omit here.
 Note that it necessarily is equivalent to $\Value$, optimized
 for Ada-only cases, has a unique representation for the Ada token class,
-and does not allow tokens of the Ada currency to have a $\Token$ value
+and does not allow tokens of the Ada currency to have a $\AssetID$ value
 of anything other than $\mathsf{adaToken}$.
 In Figure \ref{fig:defs:functions-helper} are the following helper functions,
 
@@ -599,9 +584,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} \\
@@ -664,7 +649,7 @@ \section{Transactions}
   \emph{Abstract Script Validation Functions}
   %
   \begin{align*}
-     &\fun{hashScript} \in  ~\Script\to \ScriptHash \\
+     &\fun{hashScript} \in  ~\Script\to \PolicyID \\
      &\text{compute script hash} \\~\\
      &\fun{hashData} \in  ~\Data \to \DataHash \\
      &\text{compute hash of data} \\~\\

goguen/formal-spec/utxo.tex

@@ -35,13 +35,20 @@ \subsection{UTxO Transitions}
   and non-script transaction inputs.
 \end{itemize}
 
+Because the $\Tx$ type is a sum of $\ShelleyTx$ and $\GoguenTx$, and
+there was a way of computing an ID from a Shelley transaction, there
+is potential for confusion how the ID of a transaction is
+computed. Here, $\TxId$ is always computed from values of type $\Tx$,
+never from $\ShelleyTx$ or $\GoguenTx$.
+
 Note that when submitting a transaction, the wallet is responsible for
 determining the total price of the
 validation of all the Plutus scripts in a transaction
 by running the script itself to see how much resources it takes and doing the
 fee calculation using the cost model in protocol parameters. It is then
 also responsible for adding enough inputs to the transaction to cover the
-fees required.
+fees required. In the implementation of the wallet this is handled
+automatically by default, so this generates no overhead for users.
 
 \begin{figure}[htb]
   \begin{align*}
@@ -140,33 +147,32 @@ \subsection{UTxO Transitions}
   to the deposit pot.
   This calculation now also takes the current slot number as an argument, which is
   needed to construct the correct UTxO outputs.
+
+  \item For calculating the minimum size of an output, we need the
+  function $\fun{scaledValueSize}$ that computes the size of a
+  $\Value$. It is defined as the size of the serialization of the
+  $\Value$, in analogy to $\fun{txSize}$.
 \end{itemize}
 
 \subsection{Value Operations and Partial Order.}
 \label{sec:value-ops}
-Note that
-the $\fun{consumed}$ and $\fun{produced}$ values are compared as $\Value$.
-The type $\Value$ has a partial order defined on it in (see~\cite{plutus_eutxo}).
-The idea of this partial order, as well as operations like addition and subtraction
-of terms of the $\Value$ type, is that a term $v \in \Value$ can be treated
-as a total map that maps to the trivial element $\epsilon \in \Token \to \Quantity$
-almost everywhere except for a several currency IDs that appear in $\dom~v$.
+Some of the UTxO update and precondition functions now operate on the $\Value$
+type instead of $\Coin$ (sometimes on a combination of $\Value$ and $\Coin$).
+To make this precise, we must define basic operations on $\Value$, which
+include, most notably, addition and $\leq$ comparison.
 
-This way, when adding two terms of type value, $\{ cid1 \mapsto tkns1\}$ and
-$\{ cid2 \mapsto tkns2\}$, the result is
-\[ \{ cid1 \mapsto (tkns1 + \epsilon), cid2 \mapsto (\epsilon + tkns2)\} \]
+Because the absence of a token in a $\Value$ has the same semantics as
+the token being present with an amount of $0$, we regard two elements of
+type $\Value$ as the same if they only differ by some tokens with
+amount $0$. This means that we can equivalently regard values as total
+maps that map all except a finite amount of its inputs to $0$.
 
-which simplifies to
+This way, when adding two partial maps, $m_1$ and $m_2$, $m_1 + m_2$ is defined
+by $(m_1 + m_2)~\var{pid}~\var{aid} := (m_1~\var{pid}~\var{aid}) + (m_2~\var{pid}~\var{aid})$.
 
-\[ \{ cid1 \mapsto tkns1, cid2 \mapsto tkns2\} \]
+Similarly, if we compare two maps, we compare them as follows:
 
-This definition of addition is also defined in Section~\ref{sec:notation-shelley}.
-Similarly, if we compare these two tokens, we compare them as follows
-(element-wise, with $\epsilon$ as the value associated to any currency ID
-not present in on of the values),
-
-\[ (\{ cid1 \mapsto tkns1\}~\leq~\{ cid2 \mapsto tkns2\}) \Leftrightarrow \\
-   (tkns1 \leq \epsilon~\wedge~ \epsilon \leq tkns2) \]
+\[ m_1 \leq m_2 \Leftrightarrow \forall~\var{pid}~\var{aid}, m_1~\var{pid}~\var{aid} \leq m_2~\var{pid}~\var{aid} \]
 
 \begin{figure}[htb]
   \emph{Helper Functions}
@@ -213,6 +219,9 @@ \subsection{Value Operations and Partial Order.}
     &~~\ubalance{(\outs{slot}~{txb})}  + \fun{coinToValue}(\txfee{txb} \\
     &~~+ \deposits{pp}{stpools}~{(\txcerts{txb})})\\
     & \text{value produced} \\
+    \nextdef
+    & \fun{scaledValueSize} \in \Value \to \N \\
+    & \fun{scaledValueSize}~\var{val} = \fun{valueSize}~\var{val} / \fun{valueSize}~(\fun{coinToValue}~1) \\
   \end{align*}
   \caption{Functions used in UTxO rules}
   \label{fig:functions:utxo}
@@ -270,7 +279,7 @@ \subsection{Putting Together Plutus Scripts and Their Inputs}
   %
   \emph{Helper functions}
   \begin{align*}
-    &\fun{indexedScripts} \in \GoguenTx \to (\ScriptHash \mapsto \Script) \\
+    &\fun{indexedScripts} \in \GoguenTx \to (\PolicyID \mapsto \Script) \\
     & \text{make a finite map of hash-indexed scripts} \\
     &\fun{indexedScripts}~{tx} ~=~ \{ h \mapsto s ~\vert~ \fun{hashScript}~{s}~=~h,
      s\in~\fun{txscripts}~(\fun{txwits}~{tx})\}
@@ -739,11 +748,11 @@ \subsection{Updating the UTxO State}
   \emph{State transitions}
   \begin{equation*}
     \_ \vdash
-    \var{\_} \trans{utxos}{\_} \var{\_}
+    \var{\_} \trans{utxo, utxos}{\_} \var{\_}
     \subseteq \powerset (\UTxOEnv \times \UTxOState \times \GoguenTx \times \UTxOState)
   \end{equation*}
   %
-  \caption{UTxO state update types}
+  \caption{UTxO and UTxO script state update types}
   \label{fig:ts-types:utxo-scripts}
 \end{figure}
 
@@ -810,10 +819,8 @@ \subsection{Updating the UTxO State}
     \\~\\
     \var{refunded} \leteq \keyRefunds{pp}{stkCreds}~{txb}
     \\
-    \var{decayed} \leteq \decayedTx{pp}{stkCreds}~{txb}
-    \\
     \var{depositChange} \leteq
-      (\deposits{pp}~{stpools}~{\txcerts{txb}}) - (\var{refunded} + \var{decayed})
+      (\deposits{pp}~{stpools}~{(\txcerts{txb})}) - \var{refunded}
     }
     {
     \begin{array}{l}
@@ -837,7 +844,7 @@ \subsection{Updating the UTxO State}
       \begin{array}{r}
         \varUpdate{\var{(\txins{txb} \subtractdom \var{utxo}) \cup \outs{slot}~{txb}}}  \\
         \varUpdate{\var{deposits} + \var{depositChange}} \\
-        \varUpdate{\var{fees} + \txfee{txb} + \var{decayed}} \\
+        \varUpdate{\var{fees} + \txfee{txb}} \\
         \varUpdate{\var{ups'}} \\
       \end{array}
       \right) \\
@@ -951,6 +958,8 @@ \subsection{Updating the UTxO State}
       \\
       \mathsf{adaID}~\notin \dom~{\fun{forge}~tx} \\
       \forall txout \in \txouts{txb}, ~ \fun{getValue}~txout  ~\geq ~ 0 \\~
+      \forall txout \in \txouts{txb}, ~ \fun{getCoin}~txout ~\geq \\
+      \fun{scaledValueSize}~(\fun{getValue}~txout) * \fun{minUTxOValue}~pp \\~
       \\
       \fun{txsize}~{tx}\leq\fun{maxTxSize}~\var{pp} \\
       \fun{txexunits}~{txb} \leq \fun{maxTxExUnits}~{pp}
@@ -1041,14 +1050,14 @@ \subsection{Witnessing}
 \begin{figure}[htb]
   \begin{align*}
       & \hspace{-1cm}\fun{scriptsNeeded} \in \UTxO \to \GoguenTx \to
-        \ScriptHash\\
+        \PolicyID\\
       & \hspace{-1cm}\text{items that need script validation and corresponding script hashes} \\
       &  \hspace{-1cm}\fun{scriptsNeeded}~\var{utxo}~\var{tx} = \\
       & ~~\{ \fun{validatorHash}~(\fun{getAddr}~{txout}) \mid i \mapsto \var{txout} \in \var{utxo},\\
       & ~~~~~i\in\fun{txinsScript}~{(\fun{txinputs}~\var{txb})}~{utxo}\} \\
       \cup & ~~\{ \var{a} \mid a \mapsto c \in \fun{txwdrls}~\var{txb}),
          a\in \AddrRWDScr \} \\
-        \cup & ~~\ScriptHash \cap \fun{certWitsNeeded}~{txb} \\
+        \cup & ~~\PolicyID \cap \fun{certWitsNeeded}~{txb} \\
         \cup & ~~\{ cid \mid cid \mapsto \var{tkns}~\in~\fun{forge}~{txb} \} \\
       & \where \\
       & ~~~~~~~ \var{txb}~=~\txbody{tx} \\
@@ -1098,13 +1107,24 @@ \subsection{Witnessing}
 If these conditions are all satisfied, the resulting UTxO state change is fully determined
 by the UTXO transition (the application of which is also part of the conditions).
 
+\begin{figure}[htb]
+  \emph{State transitions}
+  \begin{equation*}
+    \_ \vdash
+    \var{\_} \trans{utxow}{\_} \var{\_}
+    \subseteq \powerset (\UTxOEnv \times \UTxOState \times \Tx \times \UTxOState)
+  \end{equation*}
+  %
+  \caption{UTxO with witnesses state update types}
+  \label{fig:ts-types:utxo-scripts}
+\end{figure}
+
 \begin{figure}
   \begin{equation}
     \label{eq:utxo-witness-inductive-goguen}
     \inference[UTxO-witG]
     {
       \var{tx}~\leteq~\fun{toGoguenTx}~{tx}_o \\~\\
-      \var{h}_{txo}~\leteq~\fun{hash}~{tx}_o &
       \var{txb}\leteq\txbody{tx} &
       \var{txw}\leteq\fun{txwits}~{tx} &
       \var{tx}~\in~\GoguenTx \\
@@ -1117,7 +1137,7 @@ \subsection{Witnessing}
       \forall h \in ~\fun{scriptsNeeded}~\var{utxo}~\var{tx}, ~h\mapsto s~\in~\fun{indexedScripts}~{tx},\\
        s \in \ScriptPlutus~\Leftrightarrow ~\fun{findRdmr}~{tx}~{c}\neq \emptyset
       \\~\\
-      \forall \var{cert}~\in~\fun{txcerts}~{txb}, \fun{regCred}~{cert}\in \ScriptHash \Leftrightarrow
+      \forall \var{cert}~\in~\fun{txcerts}~{txb}, \fun{regCred}~{cert}\in \PolicyID \Leftrightarrow
       \var{cert} \in~ \DCertDeRegKey \\~\\
       \forall~\var{txin}\in\fun{txinputs}~{txb},
       \var{txin} \mapsto \var{(\wcard,\wcard,h_d)} \in \var{utxo},
@@ -1136,7 +1156,7 @@ \subsection{Witnessing}
       \fun{hash}~(\fun{txrdmrs}~\var{txw})~ =~  \fun{rdmrsHash}~{txb} \\
       \\~\\
       \forall \var{vk} \mapsto \sigma \in \txwitsVKey{txw},
-      \mathcal{V}_{\var{vk}}{\serialised{\var{h}_{tx}}}_{\sigma} \\
+      \mathcal{V}_{\var{vk}}{\serialised{tx_{o}}}_{\sigma} \\
       \fun{witsVKeyNeeded}~{utxo}~{tx}~{genDelegs} \subseteq \var{witsKeyHashes}
       \\~\\
       genSig \leteq

shelley-mc/formal-spec/frontmatter.tex

@@ -17,6 +17,7 @@
 
 \author{
    Polina Vinogradova \\ {\small \texttt{[email protected]}} \\
+   Andre Knispel \\ {\small \texttt{[email protected]}} \\
    }
 
 \date{}