Copy changes to the Goguen spec to Shelley-MC

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{}

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}}

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} \\~\\

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,20 +45,21 @@ \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.
 
   \item $\Value$ is the multicurrency type used to represent
   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} \\

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,18 +233,18 @@ \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}
       \\
       ~
       \\
       \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},\\