Merge pull request #2353 from input-output-hk/polina/formal-fix

 Formal spec update

alonzo/formal-spec/alonzo-changes.tex

@@ -180,14 +180,14 @@
 \newcommand{\ScriptPlutus}{\type{Script}_{plc}}
 \newcommand{\PlutusVI}{\type{PlutusV1}}
 \newcommand{\PlutusVII}{\type{PlutusV2}}
-\newcommand{\ScriptNative}{\type{Script^{native}}}
-\newcommand{\ScriptNonNative}{\type{Script^{non-native}}}
+\newcommand{\ScriptPhOne}{\type{Script^{ph1}}}
+\newcommand{\ScriptPhTwo}{\type{Script^{ph2}}}
 \newcommand{\ScriptV}{\type{Script_{v}}}
 \newcommand{\ScriptPurpose}{\type{ScriptPurpose}}
 \newcommand{\Rdmrs}{\type{Rdmrs}}
 \newcommand{\DorR}{\type{DorR}}
 \newcommand{\ValidationData}{\type{ValidationData}}
-\newcommand{\IsValidating}{\type{IsValidating}}
+\newcommand{\IsValid}{\type{IsValid}}
 \newcommand{\HashUnsData}{\type{HashUnsData}}
 \newcommand{\True}{\mathsf{True}}
 \newcommand{\False}{\mathsf{False}}
@@ -220,6 +220,7 @@
 \newcommand{\SKey}{\type{SKey}}
 \newcommand{\SKeyEv}{\type{SKey_{ev}}}
 \newcommand{\KeyHash}{\type{KeyHash}}
+\newcommand{\RewardAcnt}{\type{RewardAcnt}}
 \newcommand{\KeyHashGen}{\type{KeyHash_G}}
 \newcommand{\KeyPair}{\type{KeyPair}}
 \newcommand{\KeyPairEv}{\type{KeyPair_{ev}}}
@@ -378,7 +379,7 @@
 
 \include{txinfo}
 
-\include{constants}
+%\include{constants}
 
 
 \addcontentsline{toc}{section}{References}

alonzo/formal-spec/introduction.tex

@@ -3,14 +3,14 @@ \section{Introduction}
 \TODO{Please run a spell checker over the final document}
 
 This document describes the extensions to the multi-asset formal ledger specification~\cite{shelley_ma_spec} that are
-required for the support of non-native scripts, in particular Plutus Core. This underpins future Plutus development: there should be minimal changes to these ledger rules to support future non-native languages.
+required for the support of phase two scripts, in particular Plutus Core. This underpins future Plutus development: there should be minimal changes to these ledger rules to support future phase-2 languages (eg. upcoming versions of Plutus).
 %
 The two major extensions that are described here are:
 
 \begin{inparaenum}
 \item
 the introduction
-of \emph{non-native} scripts, i.e. scripts that are not evaluated internally by the ledger; and
+of \emph{phase-2} scripts, i.e. scripts that are not evaluated internally by the ledger; and
 \item
   additions to the Shelley-era UTxO (unspent transaction output) model that are needed to support Plutus
   constructs (the ``extended UTxO'' model).
@@ -21,22 +21,22 @@ \section{Introduction}
 As with the multi-asset formal specification, these rules will be implemented in the form of an executable ledger specification that will then be
 integrated with the Cardano node.
 
-\subsection{Non-Native Scripts}
+\subsection{Phase Two Scripts}
 
 The Shelley formal specification introduced the concept of ``multi-signature'' scripts.
-\emph{Native scripts}, such as these, are captured entirely by the ledger rules.
+\emph{Phase one scripts}, such as these, are captured entirely by the ledger rules.
 Execution costs can therefore be easily assessed \emph{before} they are processed by the implementation,
 and any fees can be calculated directly within the ledger rule implementation,
 based on e.g. the size of the transaction that includes the script.
 
-In contrast, \emph{non-native} scripts can perform arbitrary
+In contrast, \emph{phase-2} scripts can perform arbitrary
 (and, in principle, Turing-complete) computations.
-We require transactions that use non-native scripts
+We require transactions that use phase-2 scripts
 to have a budget in terms of a number of abstract $\ExUnits$.
 This budget gives a quantitative bound on resource usage in terms of a number of specific metrics, including memory usage or abstract execution steps.
 The budget is then used as part of the transaction fee calculation.
 
-Every non-native scripting language
+Every phase-2 scripting language
 converts the calculated execution cost into a number of $\ExUnits$ using a cost model,
 $\CostMod$, which depends on the language and is provided as a protocol parameter.
 This allows execution costs (and so transaction fees) to be varied without requiring a major protocol version change (``hard fork'').
@@ -73,24 +73,24 @@ \subsection{Non-Native Scripts}
   though the collected fees are different in the two cases.
 \end{itemize}
 
-Another important point to make about both native and non-native scripts on Cardano is that
+Another important point to make about both phase one and two scripts on Cardano is that
 running scripts in all languages will be supported indefinitely whenever possible.
 Making it impossible to run a script in a particular scripting language
 makes UTxO entries locked by that script unspendable.
 
-We use the terms Plutus, $\PlutusVI$, and ``non-native scripting language'' in this specification
+We use the terms Plutus, $\PlutusVI$, and ``phase two scripting language'' in this specification
 somewhat interchangably. The reason for this is that while we intend for the infrastructure
 set up in this document to be somewhat language-agnostic (in particular,
 able to support multiple versions of Plutus), it only gives all the details for
-the first and (currenly only) non-native script language, $\PlutusVI$,
+the first and (currenly only) phase-2 script language, $\PlutusVI$,
 the introduction of which represents the
 start of the Alonzo era.
 
 
 \subsection{Extended UTxO}
 
 The specification of the extended UTxO model follows the description that was given in~\cite{chakravarty2020extended}.
-All transaction outputs that are locked by non-native scripts must include the hash of an additional ``datum''. The actual datum needs to be supplied by the transaction spending that output, and can be used to encode state, for example.
+All transaction outputs that are locked by phase-2 scripts must include the hash of an additional ``datum''. The actual datum needs to be supplied by the transaction spending that output, and can be used to encode state, for example.
 While this datum could instead have been stored directly in the UTxO, our choice of storing it in the transaction body improves space efficiency in the implementation by reducing the UTxO storage requirements. The datum is passed to a script that validates that the output is spent correctly.
 
 All transactions also need to supply a \emph{redeemer} for all items that are validated by a script. This is an additional piece of data that is passed to the script, and that could be considered as a form of user-input to the script. Note that the same script could be used for multiple different purposes in the same transaction, so in general it might be necessary to include more than one redeemer per script.

alonzo/formal-spec/ledger.tex

@@ -3,7 +3,7 @@ \section{Ledger State Transition}
 
 Figure~\ref{fig:rules:ledger} separates the case where all the scripts
 in a transaction successfully validate from the case where there is one or more that does not.
-These two cases are distinguished by the use of the $\IsValidating$ tag.
+These two cases are distinguished by the use of the $\IsValid$ tag.
 %
 Besides collateral collection, no side effects should occur when processing a
 transaction that contains a script that does not validate. That is, no
@@ -16,7 +16,7 @@ \section{Ledger State Transition}
     \label{eq:ledger}
     \inference[ledger-V]
     {
-      \fun{isValidating}~{tx} = \True \\~\\
+      \fun{isValid}~{tx} = \True \\~\\
       {
         \begin{array}{c}
           \var{slot} \\
@@ -74,7 +74,7 @@ \section{Ledger State Transition}
     \label{eq:ledger}
     \inference[ledger-NV]
     {
-      \fun{isValidating}~{tx} = \False \\~\\
+      \fun{isValid}~{tx} = \False \\~\\
       (\var{dstate}, \var{pstate}) \leteq \var{dpstate} \\
       (\_, \_, \_, \_, \_, \var{genDelegs}, \_) \leteq \var{dstate} \\
       (\var{poolParams}, \_, \_) \leteq \var{pstate} \\