Add some tiny changes and upgrades to the proof section

2 files changed, 5 insertions, 5 deletions

diff --git a/proof.tex b/proof.tex
index 2f78380..3499b4e 100644
--- a/proof.tex
+++ b/proof.tex
@@ -27,9 +27,9 @@ The main correctness theorem is analogous to that stated in \compcert{}~\cite{le
 %The following `backwards simulation' theorem describes the correctness theorem, where $\Downarrow$ stands for simulation and execution respectively.
 
 \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$.
+  Whenever the translation from $C$ succeeds and produces Verilog $V$, and all observable behaviours of $C$ are safe (i.e. $\mathit{Safe} (C)$ is defined as $\forall B,\ S \Downarrow B \implies B \in \texttt{Safe}$) then $V$ has behaviour $B$ only if $C$ has behaviour $B$.
   \begin{equation*}
-    \forall C, V, B \in \texttt{Safe},\quad \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land V \Downarrow B \implies C \Downarrow B.
+    \forall C, V, B,\quad \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land \mathit{Safe}(C) \implies (V \Downarrow B \implies C \Downarrow B).
   \end{equation*}
 \end{theorem}
 
@@ -45,7 +45,7 @@ The forward simulation from 3AC to HTL is stated in Lemma~\ref{lemma:htl} (Secti
 As HTL is quite far removed from 3AC, this first translation is the most involved and therefore requires a larger proof, because the translation from 3AC instructions to Verilog statements needs to be proven correct in this step.  In addition to that, the semantics of HTL are also quite different to the 3AC semantics. Instead of defining small-step semantics for each construct in Verilog, the semantics are defined over one clock cycle and mirror the semantics defined for Verilog.  Lemma~\ref{lemma:htl} shows the result that needs to be proven in this subsection.
 
 \begin{lemma}[Forward simulation from 3AC to HTL]\label{lemma:htl}
-  We write \texttt{tr\_htl} for the translation from 3AC to HTL.
+  We write \texttt{tr\_htl} for the translation from 3AC to HTL, assuming that all behaviour is safe.
   \begin{equation*}
     \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*}
@@ -104,7 +104,7 @@ We also define the following set $\mathcal{I}$ of invariants that must hold for
 We can now define the simulation diagram for the translation. The 3AC state can be represented by the tuple $(R,M,\mathit{pc})$, which captures the register file, memory, and program counter. The HTL state can be represented by the pair $(\Gamma_{r}, \Gamma_{a})$, which captures the states of all the registers and arrays in the module.  Finally, $\mathcal{I}$ stands for the other invariants that need to hold for the states to match.
 
 \begin{lemma}\label{lemma:simulation_diagram}
-  Given the 3AC state $(R,M,\mathit{pc})$ and the matching HTL state $(\Gamma_{r}, \Gamma_{a})$, assuming one step in the 3AC semantics produces state $(R',M',\mathit{pc}')$, there exist one or more steps in the HTL semantics that result in matching states $(\Gamma_{r}', \Gamma_{a}')$.  This is all under the assumption that the specification $\yhfunction{tr\_{htl}}$ holds for the translation.
+  Given the 3AC state $(R,M,\mathit{pc})$ and the matching HTL state $(\Gamma_{r}, \Gamma_{a})$, assuming one step in the 3AC semantics produces state $(R',M',\mathit{pc}')$, there exist one or more steps in the HTL semantics that result in matching states $(\Gamma_{r}', \Gamma_{a}')$.  This is all under the assumption that the specification $\yhfunction{spec\_{htl}}$ holds for the translation.
 
   \begin{center}
     \begin{tikzpicture}
diff --git a/verilog.tex b/verilog.tex
index 1e0b9ff..11087b0 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -92,7 +92,7 @@ The \compcert{} computation model defines a set of states through which executio
 \compcert{} executions pass through three main states:
 \begin{description}
   \item[\texttt{State} $\mathit{sf}$ $m$ $v$ $\Gamma_{r}$ $\Gamma_{a}$] The main state when executing a function, with stack frame $\mathit{sf}$, current module $m$, current state $v$ and variable states $\Gamma_{r}$ and $\Gamma_{a}$.
-  \item[\texttt{Callstate} $\mathit{sf}$ ${r}$] The state that is reached when a function is called, with the current stack frame $\mathit{sf}$, current module $m$ and arguments $\vec{r}$.
+  \item[\texttt{Callstate} $\mathit{sf}$ $m$ $\vec{r}$] The state that is reached when a function is called, with the current stack frame $\mathit{sf}$, current module $m$ and arguments $\vec{r}$.
   \item[\texttt{Returnstate} $\mathit{sf}$ $v$] The state that is reached when a function returns back to the caller, with stack frame $\mathit{sf}$ and return value $v$.
 \end{description}