Some formula fixes

2 files changed, 14 insertions, 14 deletions

diff --git a/proof.tex b/proof.tex
index 4f58746..63200c1 100644
--- a/proof.tex
+++ b/proof.tex
@@ -29,7 +29,7 @@ The main correctness theorem is analogous to that stated in \compcert{}~\cite{le
 \begin{theorem}
   For any safe behaviour $B$, whenever the translation from $C$ succeeds and produces Verilog $V$, then $V$ has behaviour $B$ only if $C$ has behaviour $B$.
   \begin{equation*}
-    \forall C, V, B \in \texttt{Safe},\, \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land V \Downarrow B \implies C \Downarrow B.
+    \forall\ C\ V\ B, B \in \texttt{Safe} \land \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land V \Downarrow B \implies C \Downarrow B.
   \end{equation*}
 \end{theorem}
 
@@ -47,7 +47,7 @@ As HTL is quite far removed from 3AC, this first translation is the most involve
 \begin{lemma}[Forward simulation from 3AC to HTL]\label{lemma:htl}
   We write \texttt{tr\_htl} for the translation from 3AC to HTL.
   \begin{equation*}
-    \forall c, h, B \in \texttt{Safe}, \yhfunction{tr\_htl} (c) = \yhconstant{OK} (h) \land c \Downarrow B \implies h \Downarrow B.
+    \forall\ c\ h\ B, B \in \texttt{Safe} \land \yhfunction{tr\_htl} (c) = \yhconstant{OK} (h) \land c \Downarrow B \implies h \Downarrow B.
   \end{equation*}
 \end{lemma}
 
@@ -58,12 +58,12 @@ We prove this lemma by first establishing a specification of the translation fun
 %To simplify the proof, instead of using the translation algorithm as an assumption, as was done in Lemma~\ref{lemma:htl}, a specification of the translation can be constructed instead which contains all the properties that are needed to prove the correctness.  For example, for the translation from 3AC to HTL, 
 The specification for the translation of 3AC instructions into HTL data-path and control logic can be defined by the following predicate:
 \begin{equation*}
-  \yhfunction{spec\_instr } \mathit{fin }\ \mathit{ret }\ \sigma\ \mathit{stk }\ i\ \mathit{data }\ \mathit{control}
+  \yhfunction{spec\_instr}\ \mathit{fin}\ \mathit{ret}\ \sigma\ \mathit{stk}\ i\ \mathit{data}\ \mathit{control}
 \end{equation*}
 
 \noindent Here, the $\mathit{control}$ and $\mathit{data}$ parameters are the statements that the current 3AC instruction $i$ should translate to. The other parameters are the special registers defined in Section~\ref{sec:verilog:integrating}. An example of a rule describing the translation of an arithmetic/logical operation from 3AC is the following:
 \begin{equation*}
-  \inferrule[Iop]{\yhfunction{tr\_op } \mathit{op }\ \vec{a} = \yhconstant{OK } e}{\yhfunction{spec\_instr } \mathit{fin }\ \mathit{ret }\ \sigma\ \mathit{stk }\ (\yhconstant{Iop } \mathit{op }\ \vec{a}\ d\ n)\ (d\ \yhkeyword{<=}\ e)\ (\sigma\ \yhkeyword{<=}\ n)}
+  \inferrule[Iop]{\yhfunction{tr\_op}\ \mathit{op}\ \vec{a} = \yhconstant{OK}\ e}{\yhfunction{spec\_instr}\ \mathit{fin}\ \mathit{ret}\ \sigma\ \mathit{stk}\ (\yhconstant{Iop}\ \mathit{op}\ \vec{a}\ d\ n)\ (d\ \yhkeyword{<=}\ e)\ (\sigma\ \yhkeyword{<=}\ n)}
 \end{equation*}
 
 \noindent Assuming that the translation of the operator $\mathit{op}$ with operands $\vec{a}$ is successful and results in expression $e$, the rule describes how the destination register $d$ is updated to $e$ via a non-blocking assignment in the data path, and how the program counter $\sigma$ is updated to point to the next CFG node $n$ via another non-blocking assignment in the control logic.
@@ -73,7 +73,7 @@ In the following lemma, $\yhfunction{spec\_htl}$ is the top-level specification
 \begin{lemma}\label{lemma:specification}
   If a 3AC program $c$ is translated correctly to an HTL program $h$, then the specification of the translation holds.
   \begin{equation*}
-    \forall\ c\ h,\ \yhfunction{tr\_htl} (c) = \yhconstant{OK}(h) \implies \yhfunction{spec\_htl}\ c\ h.
+    \forall\ c\ h, \yhfunction{tr\_htl} (c) = \yhconstant{OK}(h) \implies \yhfunction{spec\_htl}\ c\ h.
   \end{equation*}
 \end{lemma}
 
@@ -110,9 +110,9 @@ We can now define the simulation diagram for the translation. The 3AC state can
     \begin{tikzpicture}
       \begin{scope}
         \node[circle] (s1) at (0,1.5) {$R, M, \mathit{pc}$};
-        \node[circle] (r1) at (7.2,1.5) {$\Gamma_{r}, \Gamma_{a}$};
+        \node[circle] (r1) at (8.5,1.5) {$\Gamma_{r}, \Gamma_{a}$};
         \node[circle] (s2) at (0,0) {$R', M', \mathit{pc}'$};
-        \node[circle] (r2) at (7.2,0) {$\Gamma_{r}', \Gamma_{a}'$};
+        \node[circle] (r2) at (8.5,0) {$\Gamma_{r}', \Gamma_{a}'$};
         %\node at (6.8,0.75) {+};
         \draw (s1) -- node[above] {$\mathcal{I} \land (R \le \Gamma_{r}) \land (M \le \Gamma_{a}) \land (\mathit{pc} = \Gamma_{r}[\sigma])$} ++ (r1);
         \draw[-{Latex}] ($(s1.south) + (0,0.4)$) -- ($(s2.north) - (0,0.4)$);
diff --git a/verilog.tex b/verilog.tex
index b8c0907..015d462 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -56,7 +56,7 @@ which modifies one array element using blocking assignment and then a second usi
 To reason about circuits that execute on the negative edge of the clock (such as our RAM interface described in Section~\ref{sec:algorithm:optimisation:ram}),  support for negative-edge-triggered \alwaysblock{}s was added to the semantics. This is shown in the modifications of the \textsc{Module} rule shown below:
 
 \begin{equation*}
-  \inferrule[Module]{(\Gamma, \epsilon, \vec{m})\ \downarrow_{\text{module}^{+}} (\Gamma', \Delta') \\ (\Gamma'\ //\ \Delta', \epsilon, \vec{m}) \downarrow_{\text{module}^{-}} (\Gamma'', \Delta'')}{(\Gamma, \yhkeyword{module } \yhconstant{main} \yhkeyword{(...);}\ \vec{m}\ \yhkeyword{endmodule}) \downarrow_{\text{program}} (\Gamma''\ //\ \Delta'')}
+  \inferrule[Module]{(\Gamma, \epsilon, \vec{m})\ \downarrow_{\text{module}^{+}} (\Gamma', \Delta') \\ (\Gamma'\ //\ \Delta', \epsilon, \vec{m}) \downarrow_{\text{module}^{-}} (\Gamma'', \Delta'')}{(\Gamma, \yhkeyword{module}\ \yhconstant{main} \yhkeyword{(...);}\ \vec{m}\ \yhkeyword{endmodule}) \downarrow_{\text{program}} (\Gamma''\ //\ \Delta'')}
 \end{equation*}
 
 The main execution of the module $\downarrow_{\text{module}}$ is split into $\downarrow_{\text{module}^{+}}$ and $\downarrow_{\text{module}^{-}}$, which are rules that only execute \alwaysblock{}s triggered at the positive and at the negative edge respectively. The positive-edge-triggered \alwaysblock{}s are processed in the same way as in the original \textsc{Module} rule. The output maps $\Gamma'$ and $\Delta'$ are then merged and passed as the blocking assignments map into the negative edge execution, so that all the blocking and nonblocking assignments are present.  Finally, all the negative-edge-triggered \alwaysblock{}s are processed and merged to give the final state.
@@ -74,13 +74,13 @@ The main execution of the module $\downarrow_{\text{module}}$ is split into $\do
   \centering
   \begin{minipage}{1.0\linewidth}
     \begin{gather*}
-      \inferrule[Step]{\Gamma_r[\mathit{rst}] = 0 \\ \Gamma_r[\mathit{fin}] = 0 \\ (m, (\Gamma_r, \Gamma_a))\ \downarrow_{\text{program}} (\Gamma_r', \Gamma_a')}{\yhconstant{State } \mathit{sf }\ m\ \ \Gamma_r[\sigma]\ \ \Gamma_r\ \Gamma_a \longrightarrow \yhconstant{State } \mathit{sf }\ m\ \ \Gamma_r'[\sigma]\ \ \Gamma_r'\ \Gamma_a'}\\
+      \inferrule[Step]{\Gamma_r[\mathit{rst}] = 0 \\ \Gamma_r[\mathit{fin}] = 0 \\ (m, (\Gamma_r, \Gamma_a))\ \downarrow_{\text{program}} (\Gamma_r', \Gamma_a')}{\yhconstant{State}\ \mathit{sf}\ m\ \ \Gamma_r[\sigma]\ \ \Gamma_r\ \Gamma_a \longrightarrow \yhconstant{State}\ \mathit{sf}\ m\ \ \Gamma_r'[\sigma]\ \ \Gamma_r'\ \Gamma_a'}\\
       %
-      \inferrule[Finish]{\Gamma_r[\mathit{fin}] = 1}{\yhconstant{State } \mathit{sf }\ m\ \sigma\ \Gamma_r\ \Gamma_a \longrightarrow \yhconstant{Returnstate } \mathit{sf }\ \Gamma_r[ \mathit{ret}]}\\
+      \inferrule[Finish]{\Gamma_r[\mathit{fin}] = 1}{\yhconstant{State}\ \mathit{sf}\ m\ \sigma\ \Gamma_r\ \Gamma_a \longrightarrow \yhconstant{Returnstate}\ \mathit{sf}\ \Gamma_r[ \mathit{ret}]}\\
       %
-      \inferrule[Call]{ }{\yhconstant{Callstate } \mathit{sf }\ m\ \vec{r} \longrightarrow \yhconstant{State } \mathit{sf }\ m\ n\ ((\yhfunction{init\_params}\ \vec{r}\ a)[\sigma \mapsto n, \mathit{fin} \mapsto 0, \mathit{rst} \mapsto 0])\ \epsilon}\\
+      \inferrule[Call]{ }{\yhconstant{Callstate}\ \mathit{sf}\ m\ \vec{r} \longrightarrow \yhconstant{State}\ \mathit{sf}\ m\ n\ ((\yhfunction{init\_params}\ \vec{r}\ a)[\sigma \mapsto n, \mathit{fin} \mapsto 0, \mathit{rst} \mapsto 0])\ \epsilon}\\
       %
-      \inferrule[Return]{ }{\yhconstant{Returnstate } (\yhconstant{Stackframe } r\ m\ \mathit{pc }\ \Gamma_r\ \Gamma_a :: \mathit{sf})\ v \longrightarrow \yhconstant{State } \mathit{sf }\ m\ \mathit{pc }\ (\Gamma_{r} [ \sigma \mapsto \mathit{pc}, r \mapsto v ])\ \Gamma_{a}}
+      \inferrule[Return]{ }{\yhconstant{Returnstate}\ (\yhconstant{Stackframe}\ r\ m\ \mathit{pc}\ \Gamma_r\ \Gamma_a :: \mathit{sf})\ v \longrightarrow \yhconstant{State}\ \mathit{sf}\ m\ \mathit{pc}\ (\Gamma_{r} [ \sigma \mapsto \mathit{pc}, r \mapsto v ])\ \Gamma_{a}}
     \end{gather*}
   \end{minipage}
   \caption{Top-level small-step semantics for Verilog modules in \compcert{}'s computational framework.}%
@@ -113,8 +113,8 @@ Note that there is no step from \texttt{State} to \texttt{Callstate}; this is be
 Therefore, in addition to the rules shown in Fig.~\ref{fig:inference_module}, an initial state and final state need to be defined:
 
 \begin{gather*}
-  \inferrule[Initial]{\yhfunction{is\_internal}\ (P.\texttt{main})}{\yhfunction{initial\_state}\ (\yhconstant{Callstate } []\ (P.\texttt{main})\ [])}\qquad
-  \inferrule[Final]{ }{\yhfunction{final\_state}\ (\yhconstant{Returnstate } []\ n)\ n}
+  \inferrule[Initial]{\yhfunction{is\_internal}\ P.\texttt{main}}{\yhfunction{initial\_state}\ (\yhconstant{Callstate}\ []\ P.\texttt{main}\ [])}\qquad
+  \inferrule[Final]{ }{\yhfunction{final\_state}\ (\yhconstant{Returnstate}\ []\ n)\ n}
 \end{gather*}
 
 \noindent where the initial state is the \texttt{Callstate} with an empty stack frame and no arguments for the \texttt{main} function of program $P$, where this \texttt{main} function needs to be in the current translation unit.  The final state results in the program output of value $n$ when reaching a \texttt{Returnstate} with an empty stack frame.