addressing audit comments from April 11, 2019

IntersectMBO · Jun 28, 2019 · 4113e79 · 4113e79
1 parent 7133348
commit 4113e79
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 7 deletions.
diff --git a/shelley/chain-and-ledger/formal-spec/ledger-spec.tex b/shelley/chain-and-ledger/formal-spec/ledger-spec.tex
@@ -169,7 +169,6 @@
 \newcommand{\addrRw}[1]{\fun{addr_{rwd}}~ \var{#1}}
 \newcommand{\epoch}[1]{\fun{epoch}~\var{#1}}
 \newcommand{\kesPeriod}[1]{\fun{kesPeriod}~\var{#1}}
-\newcommand{\dcerts}[1]{\fun{dcerts}~ \var{#1}}
 \newcommand{\pps}[1]{\fun{pps}~ \var{#1}}
 
 %% UTxO witnesses

diff --git a/shelley/chain-and-ledger/formal-spec/ledger.tex b/shelley/chain-and-ledger/formal-spec/ledger.tex
@@ -71,7 +71,8 @@ \section{Ledger State Transition}
       \right)
       }
       \vdash
-      dpstate \trans{\hyperref[fig:rules:delegation-sequence]{delegs}}{\fun{dcerts}~\var{tx}} dpstate'
+      dpstate \trans{\hyperref[fig:rules:delegation-sequence]{delegs}}{
+                     \fun{txcerts}~\var{tx}} dpstate'
       \\~\\
       (\var{dstate}, \var{pstate}) \leteq \var{dpstate'} \\
       (\var{stkeys}, \_, \_, \_, \_, \var{dms}) \leteq \var{dstate} \\

diff --git a/shelley/chain-and-ledger/formal-spec/utxo.tex b/shelley/chain-and-ledger/formal-spec/utxo.tex
@@ -76,7 +76,7 @@ \subsection{UTxO Transitions}
 Moreover, when the property holds, value is only moved between transaction outputs,
 the reward accounts, the fee pot and the deposit pot.
 
-Note that the $\fun{consumed}$ function takes the registered stake pools ($\var{stpools}$)
+Note that the $\fun{produced}$ function takes the registered stake pools ($\var{stpools}$)
 as a parameter only in order to determine which pool registration certificates are
 new (and thus require a deposit) and which ones are updates.
 Registration will be discussed more in Section~\ref{sec:delegation-shelley}.
@@ -111,7 +111,7 @@ \subsection{UTxO Transitions}
     & \text{value produced} \\
     & \fun{produced}~\var{pp}~\var{stpools}~\var{tx} = \\
     &~~\ubalance{(\outs{tx})}
-    + \txfee{tx} + \deposits{pp}{stpools}~{(\dcerts{tx})}\\
+    + \txfee{tx} + \deposits{pp}{stpools}~{(\txcerts{tx})}\\
   \end{align*}
 
   \caption{Functions used in UTxO rules}
@@ -320,7 +320,7 @@ \subsection{UTxO Transitions}
       \var{decayed} \leteq \decayedTx{pp}{stkeys}~{tx}
       \\
       \var{depositChange} \leteq
-        (\deposits{pp}~{stpools}~{\fun{dcerts}~tx}) - (\var{refunded} + \var{decayed})
+        (\deposits{pp}~{stpools}~{\txcerts{tx}}) - (\var{refunded} + \var{decayed})
     }
     {
       \begin{array}{l}
@@ -472,7 +472,7 @@ \subsection{Deposits and Refunds}
       & \fun{keyRefunds} \in \PParams \to \StakeKeys \to \Tx \to \Coin
       & \text{key refunds for a transaction} \\
       & \keyRefunds{pp}{stkeys}{tx} =\\
-      & ~~~~~ \sum\limits_{\substack{c \in \fun{dcerts}~tx \\ c\in\DCertDeRegKey}}
+      & ~~~~~ \sum\limits_{\substack{c \in \txcerts{tx} \\ c\in\DCertDeRegKey}}
               \keyRefund{\dval}{d_{\min}}{\lambda}{stkeys}{(\txttl{tx})}{c}\\
       &
       \begin{array}{lr@{~=~}l}
@@ -512,7 +512,7 @@ \subsection{Deposits and Refunds}
       & \fun{decayedTx} \in \PParams \to \StakeKeys \to \Tx \to \Coin
       & \text{decayed deposit portions} \\
       & \decayedTx{pp}{stkeys}{tx} =\\
-      &   \sum\limits_{\substack{c \in \fun{dcerts}~tx \\ c \in\DCertDeRegKey}}
+      &   \sum\limits_{\substack{c \in \txcerts{tx} \\ c \in\DCertDeRegKey}}
           \decayedKey{pp}{stkeys}{(\txttl{tx})}{c}\\
   \end{align*}
   \caption{Functions used in Deposits - Decay}