Some more fixes of the proof section

1 files changed, 9 insertions, 9 deletions

diff --git a/proof.tex b/proof.tex
index 6a44ed6..1a91d4e 100644
--- a/proof.tex
+++ b/proof.tex
@@ -1,4 +1,4 @@
-\section{Proof}\label{sec:proof}
+\section{Semantics Preservation Proof of Translation}\label{sec:proof}
 
 Now that the Verilog semantics have been adapted to the CompCert model, we are in a position to formally prove the correctness of our C-to-Verilog compilation.  This section describes the main correctness theorem that was proven and the main ideas behind the proof. The full Coq proof is available in auxiliary material.
 
@@ -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, B \in \texttt{Safe} \land \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land V \Downarrow B \implies C \Downarrow B.
+    \forall C, V, B \in \texttt{Safe},\quad \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, B \in \texttt{Safe} \land \yhfunction{tr\_htl} (c) = \yhconstant{OK} (h) \land c \Downarrow B \implies h \Downarrow B.
+    \forall c, h, B \in \texttt{Safe},\quad \yhfunction{tr\_htl} (c) = \yhconstant{OK} (h) \land c \Downarrow B \implies h \Downarrow B.
   \end{equation*}
 \end{lemma}
 
@@ -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,\quad \yhfunction{tr\_htl} (c) = \yhconstant{OK}(h) \implies \yhfunction{spec\_htl}\ c\ h.
   \end{equation*}
 \end{lemma}
 
@@ -171,7 +171,7 @@ The other invariants and assumptions for defining two matching states in HTL are
   Given an HTL program, the forward simulation relation should hold after inserting the RAM and wiring the load, store and control signals.
 
   \begin{align*}
-    &\forall\ h\ B, B \in \texttt{Safe} \land \yhfunction{tr\_ram}(h) = h' \land h \Downarrow B \implies h' \Downarrow B.
+    \forall h, B \in \texttt{Safe},\quad \yhfunction{tr\_ram}(h) = h' \land h \Downarrow B \implies h' \Downarrow B.
   \end{align*}
 \end{lemma}
 
@@ -183,7 +183,7 @@ The HTL-to-Verilog simulation is conceptually simple, as the only transformation
 \begin{lemma}[Forward simulation from HTL to Verilog]\label{lemma:verilog}
   We write $\yhfunction{tr\_verilog}$ for the translation from HTL to Verilog. (Note that this translation cannot fail, so we do not need the \yhconstant{OK} constructor here.)
   \begin{align*}
-    &\forall\ h\ V\ B, B \in \texttt{Safe} \land \yhfunction{tr\_verilog} (h) = V \land h \Downarrow B \implies V \Downarrow B.
+    \forall h, V, B \in \texttt{Safe},\quad \yhfunction{tr\_verilog} (h) = V \land h \Downarrow B \implies V \Downarrow B.
   \end{align*}
 \end{lemma}
 
@@ -193,16 +193,16 @@ The HTL-to-Verilog simulation is conceptually simple, as the only transformation
   %The proof of the translation from maps to case-statements follows by induction over the list of elements in the map and the fact that each key will be unique.  In addition to that, the statement that is currently being evaluated is guaranteed by the correctness of the list of elements to be in that list.  The latter fact therefore eliminates the base case, as an empty list does not contain the element we know is in the list.  The other two cases follow by the fact that either the key is equal to the evaluated value of the case expression, or it isn't.  In the first case we can then evaluate the statement and get the state after the case expression, as the uniqueness of the key tells us that the key cannot show up in the list anymore.  In the other case we can just apply the inductive hypothesis and remove the current case from the case statement, as it did not match.
 \end{proof}
 
-\subsection{Deterministic Semantics}\label{sec:proof:deterministic}
+\subsection{Deterministic Verilog Semantics}\label{sec:proof:deterministic}
 
 %Finally, to obtain the backward simulation that we want, it has to be shown that if we generate hardware with a specific behaviour, that it is the only possible program with that behaviour.  This only has to be performed for the final intermediate language, which is Verilog, so that the backward simulation holds for the whole chain from Clight to Verilog.
-The final lemma we need is that the Verilog we generate is deterministic. This result allows us to replace the forwards simulation we have proved with the backwards simulation we desire.
+The final lemma we need is that the Verilog semantics is deterministic. This result allows us to replace the forwards simulation we have proved with the backwards simulation we desire.
 
 \begin{lemma}\label{lemma:deterministic}
   If a Verilog program $V$ admits both behaviours $B_1$ and $B_2$, then $B_1$ and $B_2$ must be the same.
 
   \begin{equation*}
-    \forall\ V\ B_{1}\ B_{2}, V \Downarrow B_{1} \land V \Downarrow B_{2} \implies B_{1} = B_{2}.
+    \forall V, B_{1}, B_{2},\quad V \Downarrow B_{1} \land V \Downarrow B_{2} \implies B_{1} = B_{2}.
   \end{equation*}
 \end{lemma}