Various changes and additions requested by Polina

goguen/formal-spec/frontmatter.tex

@@ -24,6 +24,7 @@
 
 \author{
    Polina Vinogradova \\ {\small \texttt{polina.vinogradova@iohk.io}} \\
+   Andre Knispel \\ {\small \texttt{andre.knispel@iohk.io}} \\
    }
 
 \date{}

goguen/formal-spec/goguen-changes.tex

@@ -40,7 +40,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}
@@ -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,21 @@
+\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 The general accounting property holds with any transaction,
+  whether it is fully processed or not. 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
@@ -90,6 +90,8 @@ \section{Transactions}
   option will additionally allow users to write their own programmatic solutions
   to choosing for-fees inputs.
 
+  \item $\TxId$ is always computed from values of type $\Tx$, never from $\ShelleyTx$ or $\GoguenTx$.
+
   \item $\UTxOIn$ is the type of the keys in the UTxO finite map. In Goguen, it is
   the same as the type as the basic UTxO keys in Shelley, but we have changed the name
   to make the distinction between a transaction input type and UTxO keys.
@@ -166,14 +168,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 +191,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 +199,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 +267,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 +543,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 +586,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 +651,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

@@ -41,7 +41,8 @@ \subsection{UTxO Transitions}
 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*}
@@ -149,7 +150,7 @@ \subsection{Value Operations and Partial Order.}
 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$
+as a total map that maps to the trivial element $\epsilon \in \AssetID \to \Quantity$
 almost everywhere except for a several currency IDs that appear in $\dom~v$.
 
 This way, when adding two terms of type value, $\{ cid1 \mapsto tkns1\}$ and
@@ -270,7 +271,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 +740,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 +811,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 +836,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 +950,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{valueSize}~(\fun{getValue}~txout) * \fun{minUTxOValue} pp \\~
       \\
       \fun{txsize}~{tx}\leq\fun{maxTxSize}~\var{pp} \\
       \fun{txexunits}~{txb} \leq \fun{maxTxExUnits}~{pp}
@@ -1041,14 +1042,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 +1099,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 +1129,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 +1148,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