From 6a2797ace635cddfea3a3835661a19eccc3f4ad2 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 12 Sep 2021 20:16:09 +0100
Subject: Add some tiny changes and upgrades to the proof section

---
 proof.tex | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'proof.tex')

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}
-- 
cgit 

