data arguments passed as list

IntersectMBO · Jan 6, 2020 · b9579db · b9579db
1 parent 23b59e0
commit b9579db
Showing 1 changed file with 4 additions and 5 deletions.
diff --git a/shelley/chain-and-ledger/formal-spec/transactions.tex b/shelley/chain-and-ledger/formal-spec/transactions.tex
@@ -253,7 +253,7 @@ \section{Transactions}
       \fun{getDataHash} & \TxOut \to \HashDat & \text{data script hash} \\
       \fun{forged} & \Tx \to \Value & \text{value forged by tx}\\
       \fun{txexunits} & \Tx \to \ExUnits & \text{portion of fee allocated for scripts}\\
-      \fun{hashPP} & \Tx \to \HashPP^? & \text{hash of the protocol params}\\
+      \fun{hashPP} & \Tx \to \HashPP^? & \text{hash of the Plutus params}\\
       \fun{txvaltag} & \Tx \to \IsValidating & \text{transaction validation tag}\\
       \fun{txvlds} & \Tx \to \Vlds & \text{validator scripts}\\
       \fun{txdats} & \Tx \to (\HashDat \mapsto \Data) & \text{data scripts}\\
@@ -327,21 +327,20 @@ \section{Transactions}
     \ExUnits \to (\IsValidating \times \ExUnits) \\
     & \text{resource-restricted validation of a multi-sig script} \\~\\
     & \fun{valPLCupTo} \in \CostMod \to\ScriptPlutus\to
-    (\Data \times \Data \times \Data \times
-    \ExUnits) \to (\IsValidating \times \ExUnits) \\
+    (\seqof{\Data} \times \ExUnits) \to (\IsValidating \times \ExUnits) \\
     & \text{resource-restricted validation of a Plutus script}
   \end{align*}
   %
   \emph{Notation}
   %
   \begin{align*}
     \llbracket \var{script_v} \rrbracket_{\var{cm},\var{exunits}}(\var{dataval},~\var{rdmr},~\var{ptx})
-    &=& \fun{valPLCupTo} ~{cm}~\var{script_v}~(\var{dataval},~\var{rdmr},~\var{ptx},~
+    &=& \fun{valPLCupTo} ~{cm}~\var{script_v}~((\var{dataval};~\var{rdmr};~\var{ptx};\epsilon),~
     \var{exunits})
     \nextdef
     \llbracket \var{script_v} \rrbracket_{\var{cm},\var{exunits}} \var{ptx}
     &=& \begin{cases}
-    \fun{valPLCupTo} ~\var{cm}~\var{script_v} ~ \var{\Nothing}~\var{\Nothing}~\var{ptx}~
+    \fun{valPLCupTo} ~\var{cm}~\var{script_v} ~(\var{ptx};\epsilon)~
     \var{exunits} ~& \text{if}~\var{script_v} \in \ScriptPlutus \\
     \fun{valMSIGupTo} ~\var{cm}~\var{script_v} ~\var{ptx}~
     \var{exunits} & \text{if}~\var{script_v} \in \ScriptMSig