Add Safe(C) in first paragraph

1 files changed, 2 insertions, 2 deletions

diff --git a/proof.tex b/proof.tex
index 550fdd6..63f8225 100644
--- a/proof.tex
+++ b/proof.tex
@@ -18,7 +18,7 @@ Together, these differences mean that translating 3AC directly to Verilog is inf
 
 \subsection{Formulating the Correctness Theorem}
 
-The main correctness theorem is analogous to that stated in \compcert{}~\cite{leroy09_formal_verif_realis_compil}: for all Clight source programs $C$, if the translation to the target Verilog code succeeds, and $C$ has a safe observable behaviour $B$ when executed, then the target Verilog code will have the same behaviour $B$. Here, a `safe' execution is one that either converges or diverges, but does not `go wrong'. If the program does admit some wrong behaviour (such as undefined behaviour in C), the correctness theorem does not apply. A safe behaviour, then, is either a final state (in the case of convergence) or divergent. In \compcert{}, a behaviour is also associated with a trace of I/O events, but since external function calls are not supported in \vericert{}, this trace will always be empty.
+The main correctness theorem is analogous to that stated in \compcert{}~\cite{leroy09_formal_verif_realis_compil}: for all Clight source programs $C$, if the translation to the target Verilog code succeeds, $\mathit{Safe}(C)$ holds and the target Verilog has behaviour $B$ when simulated, then the Clight source program will have the same behaviour $B$. $\mathit{Safe}(C)$ means all observable behaviours of $C$ are safe, which can be defined as $\forall B,\ C \Downarrow B \implies B \in \texttt{Safe}$.  A behaviour is in \texttt{Safe} if it is either a final state (in the case of convergence) or divergent, but it cannot `go wrong', meaning the source program must not contain undefined behaviour. In \compcert{}, a behaviour is also associated with a trace of I/O events, but since external function calls are not supported in \vericert{}, this trace will always be empty.
 
 %This correctness theorem is also appropriate for HLS, as HLS is often used as a part of a larger hardware design that is connected together using a hardware description language like Verilog.  This means that HLS designs are normally triggered multiple times and results are returned each time when the computation terminates, which is the property that the correctness theorem states.
 
@@ -27,7 +27,7 @@ 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}
-  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,\ C \Downarrow B \implies B \in \texttt{Safe}$) 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 then $V$ has behaviour $B$ only if $C$ has behaviour $B$.
   \begin{equation*}
     \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*}