notes and script stuff

shelley/chain-and-ledger/formal-spec/ledger-spec.tex

@@ -62,6 +62,7 @@
 \newcommand{\Rnn}{\ensuremath{\mathbb{R}^{\geq 0}}}
 \newcommand{\Tx}{\type{Tx}}
 \newcommand{\TxBody}{\type{TxBody}}
+\newcommand{\UnsignedData}{\type{UnsignedData}}
 \newcommand{\VldSR}{\type{VldSR}}
 \newcommand{\VldOut}{\type{VldOut}}
 \newcommand{\Vlds}{\type{Vlds}}
@@ -96,7 +97,6 @@
 \newcommand{\Applications}{\type{Applications}}
 \newcommand{\AVUpdate}{\type{AVUpdate}}
 \newcommand{\Update}{\type{Update}}
-
 \newcommand{\DCert}{\type{DCert}}
 \newcommand{\DCertRegKey}{\type{DCert_{regkey}}}
 \newcommand{\DCertDeRegKey}{\type{DCert_{deregkey}}}
@@ -112,7 +112,6 @@
 \newcommand{\ValEnv}{\type{ValEnv}}
 \newcommand{\ValState}{\type{ValState}}
 \newcommand{\ScrInData}{\type{ScrInData}}
-
 \newcommand{\AddrRWD}{\type{Addr_{rwd}}}
 \newcommand{\AddrB}{\type{Addr_{base}}}
 \newcommand{\AddrP}{\type{Addr_{ptr}}}
@@ -156,6 +155,7 @@
 \newcommand{\HashPP}{\type{HashPP}}
 \newcommand{\Script}{\type{Script}}
 \newcommand{\ScriptPlutus}{\type{Script}_{plc}}
+\newcommand{\ScrPLC}{\type{ScrPLC}}
 \newcommand{\ScriptMSig}{\type{Script}_{msig}}
 \newcommand{\ScriptV}{\type{Script_{v}}}
 \newcommand{\DatVal}{\type{DatVal}}

shelley/chain-and-ledger/formal-spec/protocol-parameters.tex

@@ -29,6 +29,17 @@ \section{Protocol Parameters}
 \item $\ExUnits$ abstract units of resources for script execution
 \end{itemize}
 
+\begin{note}
+  If we want a record of when Plutus versions were introduced, we want to keep
+  the $\var{minPlutusVer}$ as a map $\PlutusVer \mapsto \Slot$.
+  The $\var{maxPlutusVer}$ should go into $\var{avs}$. I think both
+  $\ProtVer$ and the $\var{avs}$ application versions should go into the
+  Plutus-specific hash. Do we need a separate data type for the Plutus-relevant
+  protocol parameters (and then add the aforementioned two parameters too),
+  or should this be a selector function instead, returning the tuple of
+  useful parameters?
+\end{note}
+
 We also added several protocol parameters and accessor functions.
 
 

shelley/chain-and-ledger/formal-spec/transactions.tex

@@ -14,7 +14,10 @@ \section{Transactions}
   values are used instead of booleans for clarity.
 
   \item $\ScriptPlutus$ and $\ScriptMSig$ are two types of scripts this spec
-  covers validation of
+  covers validation of. As a script type, the Plutus script is a pair of the
+  actual script and the version of the Plutus interpreter which was used to
+  make this script. Both of these pieces of data need to be passed to the
+  interpreter during script validation.
 
   \item $\IsFee$ is a tag that indicates when an input has been marked
   to be used for paying transaction fees ($\Yes$ for when it is for fees,
@@ -63,8 +66,8 @@ \section{Transactions}
       \var{curid} & \CurrencyId & \text{currency id}\\
       \var{tok} & \Token & \text{token identifier}\\
       \var{quan} & \Quantity & \text{quantity of a token}\\
-      \var{plc} & \ScriptPlutus & \text{Plutus scripts} \\
       \var{msig} & \ScriptMSig & \text{Multisig scripts} \\
+      \var{spl} & \ScrPLC & \text{Plutus scripts without the version number} \\
       \var{yes} & \Yes & \text{tag type for yes} \\
       \var{no} & \Nope & \text{tag type for no} \\
     \end{array}
@@ -73,6 +76,7 @@ \section{Transactions}
   %
   \begin{equation*}
     \begin{array}{r@{~\in~}l@{\qquad=\qquad}lr}
+      \var{plc} & \ScriptPlutus & \ScrPLC\times\PlutusVer & \text{Plutus scripts} \\
       \var{scr} & \Script & \ScriptPlutus \uniondistinct \ScriptMSig \\
       \var{isv} & \IsValidating & \Yes \uniondistinct \Nope \\
       \var{dat}
@@ -85,7 +89,6 @@ \section{Transactions}
   %
   \begin{equation*}
     \begin{array}{r@{~\in~}l@{\subset}lr}
-      \var{script_v}&\ScriptV & \Script & \text{validator script}\\
       \var{dataval}&\DatVal & \Data & \text{data script}\\
       \var{rdmr}&\Rdmr & \Data & \text{redeemer script}\\
     \end{array}
@@ -157,8 +160,14 @@ \section{Transactions}
 The types for passing to Plutus scripts are added in Figure \ref{fig:defs:utxo-pending}.
 There is current item $\CurItem$, which represents either the current input being
 spent, the current certificated being validated, or the current reward
-withdrawal. $\ScrInData$ is all the input data for a script. It is
-just validation data for MSIG, and data value, redeemer and validation data for PLC.
+withdrawal.
+
+\begin{note}
+Instead of the two possibilities for validator inputs, just $\ValidationData$ or
+the triple $(\ValidationData, \DatVal, \Rdmr)$, the input is now a list which
+either has one item in it or three. What is the correct input order to have
+it in?
+\end{note}
 
 
 \begin{figure*}[htb]
@@ -169,11 +178,6 @@ \section{Transactions}
       \var{cur}
       & \CurItem
       & \Nothing \uniondistinct \TxInTx \uniondistinct \Wdrl \uniondistinct \DCert
-      \\
-      \var{sid}
-      & \ScrInData
-      & \Data \uniondistinct
-        (\Data \times \Data \times \Data)
     \end{array}
   \end{equation*}
   \caption{Definitions used to make Validation Data}
@@ -196,7 +200,13 @@ \section{Transactions}
   \item $\TxBody$ also has the hash of the current protocol parameters
   (only the ones relevant to Plutus script validation), $\HashPP^?$,
   which is only obligatory to include when a transaction is carrying scripts
-  \item Not as part of the body, the transaction now also includes
+  \item $\UnsignedData$ is the part of the transaction that is outside the
+  (signed) body.
+  It contains all the data that does not need to be signed because either
+  this data is either
+  a) signatures, b) its hash is in the body or on-chain, c) it is a tag
+  added by the creator of the block, or d) it is other kinds of metadata
+  \item $\UnsignedData$ includes
   a finite map lookup $\Vlds$ to avoid having multiple
   copies of the validator (one for each input spending from that script).
   \item $\HashDat \mapsto \Data$ is a similar lookup for $\Data$.
@@ -232,12 +242,16 @@ \section{Transactions}
   %
   \begin{equation*}
     \begin{array}{r@{~\in~}l@{\qquad=\qquad}l}
-      \var{wit} & \TxWitness & (\VKey \mapsto \Sig)
+      \var{wit} & \TxWitness & \VKey \mapsto \Sig
+      \\
+      \var{unsignedData} ~\in~
+      & \UnsignedData ~=~
+      & \TxWitness \times \Vlds \times (\HashDat \mapsto \Data)
+            \times \IsValidating
       \\
       \var{tx}
       & \Tx
-      & \TxBody \times \TxWitness \times \Vlds \times (\HashDat \mapsto \Data)
-      \times \IsValidating
+      & \TxBody \times \UnsignedData
     \end{array}
   \end{equation*}
   %

shelley/chain-and-ledger/formal-spec/utxo.tex

@@ -122,7 +122,7 @@ \subsection{UTxO Transitions}
 
 \begin{figure}[htb]
   \begin{align*}
-    & \fun{mkScrLst} \to \PParams \to \Tx \to \UTxO \to \seqof{(\ScriptV,\ScrInData)} \\
+    & \fun{mkScrLst} \to \PParams \to \Tx \to \UTxO \to \seqof{(\ScriptV,\seqof{\Data})} \\
     & \text{a list of all validators and corresponding input data} \\
     & \fun{mkScrLst}  ~\var{pp}~\var{tx}~ \var{utxo} ~=~
     \fun{toList}~(\fun{allCertScrts}~\var{pp}~{utxo}~{tx} \cup \fun{allWDRLSScrts}~\var{pp}~{utxo}~{tx} \\
@@ -186,7 +186,7 @@ \subsection{UTxO Transitions}
 
 \begin{figure}[htb]
   \begin{align*}
-    & \fun{allCertScrts} \in \PParams \to \UTxO \to \Tx \to \powerset{(\ScriptV \times \ScrInData)} \\
+    & \fun{allCertScrts} \in \PParams \to \UTxO \to \Tx \to \powerset{(\ScriptV \times \seqof{\Data})} \\
     & \text{check that all certificate witnessing scripts in a tx validate} \\
     & \fun{allCertScrts}~{utxo}~{tx}~=~ \\
     & ~~\{ (\var{script_v},
@@ -196,7 +196,7 @@ \subsection{UTxO Transitions}
      \} \\
     %
     \nextdef
-    & \fun{allWDRLSScrts} \in \PParams \to \UTxO \to \Tx \to \powerset{(\ScriptV\times\ScrInData)} \\
+    & \fun{allWDRLSScrts} \in \PParams \to \UTxO \to \Tx \to \powerset{(\ScriptV\times\seqof{\Data})} \\
     & \text{check that all reward withdrawal locking scripts in a tx validate} \\
     & \fun{allWDRLSScrts}~{utxo}~{tx}~=~ \\
     & ~~\{ (\var{script_v},\fun{validationData}~\var{utxo}~\var{tx}~
@@ -205,7 +205,7 @@ \subsection{UTxO Transitions}
     & ~~\wcard\mapsto \var{script_v}\in \fun{validatorHash}~\var{a}\restrictdom\fun{txvlds}~{tx}\}
     \nextdef
     %
-    & \fun{forgedScrts} \in \PParams \to \UTxO \to \Tx \to \powerset{(\ScriptV\times\ScrInData)} \\
+    & \fun{forgedScrts} \in \PParams \to \UTxO \to \Tx \to \powerset{(\ScriptV\times\seqof{\Data})} \\
     & \text{check that all forging scripts in a tx validate} \\
     & \fun{forgedScrts}~{utxo}~{tx}~=~\\
     & ~~\{ (\var{script_v},
@@ -221,9 +221,9 @@ \subsection{UTxO Transitions}
 
 \begin{figure}[htb]
   \begin{align*}
-    & \fun{allInsScrts} \in \PParams \to \UTxO \to \Tx \to \powerset{(\ScriptV\times\ScrInData)} \\
+    & \fun{allInsScrts} \in \PParams \to \UTxO \to \Tx \to \powerset{(\ScriptV\times\seqof{\Data})} \\
     & \text{check that all UTxO entry locking scripts in a tx validate} \\
-    & \fun{allInsScrts}~{utxo}~{tx}~=~ \{ (\var{script_v}, (\var{dataval},\var{rdmr}, \\
+    & \fun{allInsScrts}~{utxo}~{tx}~=~ \{ (\var{script_v}; (\var{dataval};\var{rdmr}; \\
     & ~~ \fun{validationData}~\var{utxo}~\var{tx}~
       (txid,ix,\var{hash_r}))) ~\vert \\
     & ~~(txid,ix,\var{hash_r}) \in \fun{txinputs}~\var{tx}, \\
@@ -284,7 +284,7 @@ \subsection{UTxO Transitions}
   \begin{equation*}
     \_ \vdash
     \var{\_} \trans{utxos}{\_} \var{\_}
-    \subseteq \powerset (\ValEnv \times \ValState \times \seqof{\ScriptV\times\ScrInData} \times \ValState)
+    \subseteq \powerset (\ValEnv \times \ValState \times \seqof{(\ScriptV\times\seqof{\Data})} \times \ValState)
   \end{equation*}
   %
   \caption{UTxO script validation types}
@@ -604,7 +604,7 @@ \subsection{UTxO Transitions}
   has the full validator in the metadata
 
   \item for each currency ID in the forged value of a transaction, the transaction
-  has the full validator in the metadata 
+  has the full validator in the metadata
 
   \item the hash indexes of all validators are their correct hashes