Fix TODOs in the formal spec

IntersectMBO · Jun 24, 2019 · 0815e32 · 0815e32
1 parent 08159b5
commit 0815e32
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 12 deletions.
diff --git a/shelley/chain-and-ledger/formal-spec/chain.tex b/shelley/chain-and-ledger/formal-spec/chain.tex
@@ -708,8 +708,8 @@ \subsection{Block Header Transition}
         \var{nes}'
       }
       \\~\\
-      (\wcard,~\wcard,~\var{b_{prev}},~\wcard,~\var{es},~\var{ru},~\wcard,~\wcard)\leteq\var{nes}
-      % TODO: is es = (_ _ _ pp) ?
+      (\wcard,~\wcard,~\var{b_{prev}},~\wcard,~\var{es},~\var{ru},~\wcard,~\wcard)\leteq\var{nes} \\
+      (\wcard,~\wcard,~\wcard,~\var{es})\leteq \var{es}
       \\
       {
         \left(
@@ -853,7 +853,7 @@ \subsection{Verifiable Random Function}
       & ~~~~\where \\
       & ~~~~~~~~~~\var{hk} \leteq \hashKey{(\bvkcold bhb)} \\
       & ~~~~~~~~~~\var{ss} \leteq \slotToSeed{(\bslot{bhb})} \\
-      % TODO : is vk = bvkcold bhb ?
+      & ~~~~~~~~~~\var{vk} \leteq \fun{bvkcold}~\var{bhb} \\
   \end{align*}
   \label{fig:vrf-checks}
 \end{figure}
@@ -1383,8 +1383,7 @@ \subsection{Chain Transition}
               \eta_c' \\
         \end{array}\right)}
       } \\~\\~\\
-      \var{ls'}\leteq\fun{setIssueNumbers}~\var{ls}~\var{cs} \\ % TODO should
-                                % this be cs' ?
+      \var{ls'}\leteq\fun{setIssueNumbers}~\var{ls}~\var{cs'} \\
       {
         {\left(\begin{array}{c}
               \dom{osched} \\

diff --git a/shelley/chain-and-ledger/formal-spec/epoch.tex b/shelley/chain-and-ledger/formal-spec/epoch.tex
@@ -900,8 +900,6 @@ \subsection{Complete Epoch Boundary Transition}
       \\~\\~\\
       \var{(\wcard,~\wcard,~\wcard,~(\var{pup},~\wcard,~\wcard,~\wcard))}\leteq\var{utxoSt'}\\
       \var{pp_{new}}\leteq\fun{votedValue_{PParams}}~\var{pup}\\
-      % TODO: I think this isn't the right type, `pup` is PPUpdate which is not
-      % a complete set of `PParams`.
       {
         \begin{array}{l}
           \var{pp_{new}}\\

diff --git a/shelley/chain-and-ledger/formal-spec/update.tex b/shelley/chain-and-ledger/formal-spec/update.tex
@@ -244,7 +244,7 @@ \section{Updates}
       &
       \dom{\var{aup}}\subseteq\dom{\var{dms}}
       \\
-      \var{aup'}\leteq\var{aup_s}\unionoverrideRight\var{aup} % TODO: not needed here?
+      \var{aup'}\leteq\var{aup_s}\unionoverrideRight\var{aup}
       &
       \var{fav}\leteq\fun{votedValue_{Applications}}~\var{aup'}
       \\
@@ -327,8 +327,7 @@ \section{Updates}
   \begin{equation}\label{eq:update}
     \inference[Update]
     {
-      (\var{pup},~\var{aup})\leteq\var{up} % TODO: duplicate of state names in
-                                           % signal
+      (\var{pup_{u}},~\var{aup_{u}})\leteq\var{up}
       \\~\\
       {
         \left(
@@ -340,7 +339,7 @@ \section{Updates}
       }
       \vdash
       \left(\var{pup}\right)
-      \trans{\hyperref[fig:rules:pp-update]{ppup}}{\var{pup}}
+      \trans{\hyperref[fig:rules:pp-update]{ppup}}{\var{pup_{u}}}
       \left(\var{pup'}\right)
       &
       {
@@ -361,7 +360,7 @@ \section{Updates}
           \end{array}
         \right)
       }
-      \trans{\hyperref[fig:rules:av-update]{avup}}{\var{aup}}
+      \trans{\hyperref[fig:rules:av-update]{avup}}{\var{aup_{u}}}
       {
         \left(
           \begin{array}{r}