Fix some of the maths

6 files changed, 33 insertions, 23 deletions

diff --git a/chapters/hls.tex b/chapters/hls.tex
index 1a5374c..6a86107 100644
--- a/chapters/hls.tex
+++ b/chapters/hls.tex
@@ -791,8 +791,9 @@ because Vericert (currently) only supports types represented by 32 bits.
 
 \subsection[sec:verilog:integrating]{Integrating the Verilog Semantics into CompCert's Model}
 
-\startplacefigure[title={Top-level semantics used in CompCert to initiate the first call to
-    \type{main} and well as return the final result of the \type{main} function.}]
+\startplacefigure[reference={fig:inference_module},title={Top-level semantics used in CompCert to
+    initiate the first call to \type{main} and well as return the final result of the \type{main}
+    function.}]
 \startformula \startalign[n=1]
   \NC\text{\sc Step }\ \frac{\startmatrix[n=1]
     \NC \Gamma_r[\mathit{rst}] = 0 \qquad \Gamma_r[\mathit{fin}] = 0 \NR
@@ -853,13 +854,13 @@ and $\mathit{ret}$ respectively.
 \desc{stack} The function stack can be modelled as a RAM block, which is implemented using an array
 in the module, and denoted as $\mathit{stk}$.
 
-\in{Figure}[fig:inference_module] shows the inference rules for moving
-between the computational states. The first, {\sc Step}, is the normal rule of execution. It defines
-one step in the \type{State} state, assuming that the module is not being reset, that the finish
-state has not been reached yet, that the current and next state are $v$ and $v'$, and that the
-module runs from state $\Gamma$ to $\Gamma'$ using the {\sc Step} rule. The {\sc Finish} rule
-returns the final value of running the module and is applied when the $\mathit{fin}$ register is
-set; the return value is then taken from the $\mathit{ret}$ register.
+\in{Figure}[fig:inference_module] shows the inference rules for moving between the computational
+states. The first, {\sc Step}, is the normal rule of execution. It defines one step in the
+\type{State} state, assuming that the module is not being reset, that the finish state has not been
+reached yet, that the current and next state are $v$ and $v'$, and that the module runs from state
+$\Gamma$ to $\Gamma'$ using the {\sc Step} rule. The {\sc Finish} rule returns the final value of
+running the module and is applied when the $\mathit{fin}$ register is set; the return value is then
+taken from the $\mathit{ret}$ register.
 
 Note that there is no step from \type{State} to \type{Callstate}; this is because function calls are
 not supported, and it is therefore impossible in our semantics ever to reach a \type{Callstate}
@@ -1014,16 +1015,17 @@ Verilog and CompCert's existing intermediate languages.
 
 Together, these differences mean that translating 3AC directly to Verilog is infeasible, as the
 differences in the semantics are too large. Instead, HTL, which was introduced in
-\in{Section}[sec:design], bridges the gap in the semantics between the two languages. HTL still
+\in{Section}[sec:hls:design], bridges the gap in the semantics between the two languages. HTL still
 consists of maps, like many of the other CompCert languages, but each state corresponds to a Verilog
 statement.
 
 \subsection[formulating-the-correctness-theorem]{Formulating the Correctness Theorem}
 
-The main correctness theorem is analogous to that stated in ~: 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 $C$ will have the same behaviour $B$.
-$\mathit{Safe}(C)$ means all observable behaviours of $C$ are safe, which can be defined as
+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 $C$ 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 \text{\tt Safe}$. A behaviour is in \type{Safe} if it is
 either a final state (in the case of convergence) or divergent, but it cannot \quote{go
   wrong}. (This means that the source program must not contain undefined behaviour.) In , a
@@ -1033,8 +1035,12 @@ supported in , this trace will always be empty.
 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$.
 
-\placeformula\startformula \forall C, V, B,\quad \text{\tt HLS} (C) = \text{\tt OK} (V) \land
-\mathit{Safe}(C) \implies (V \Downarrow B \implies C \Downarrow B). \stopformula
+\placeformula\startformula
+  \startalign[n=1,align={1:right}]
+    \NC \forall C, V, B,\quad \text{\tt HLS} (C) = \text{\tt OK} (V) \land \mathit{Safe}(C) \NR
+    \NC \implies (V \Downarrow B \implies C \Downarrow B). \NR
+  \stopalign
+\stopformula
 
 Why is this correctness theorem also the right one for HLS? It could be argued that hardware
 inherently runs forever and therefore does not produce a definitive final result. This would mean
@@ -1105,9 +1111,11 @@ instruction $i$ should translate to. The other parameters are the special regist
 Section~\goto{{[}sec:verilog:integrating{]}}[sec:verilog:integrating].  An example of a rule
 describing the translation of an arithmetic/logical operation from 3AC is the following:
 
-\startformula \text{\sc Iop}{\text{\tt tr\_op}\ \mathit{op}\ \vec{a} = \text{\tt OK}\ e}{\text{\tt
-    spec\_instr}\ \mathit{fin}\ \mathit{ret}\ \sigma\ \mathit{stk}\ (\text{\tt Iop}\ \mathit{op}\
-  \vec{a}\ d\ n)\ (d\ \text{\tt <=}\ e)\ (\sigma\ \text{\tt <=}\ n)} \stopformula
+\startformula
+  \text{\sc Iop}\ \frac{\text{\tt tr\_op}\ \mathit{op}\ \vec{a} = \text{\tt OK}\ e}{\text{\tt spec\_instr}\
+    \mathit{fin}\ \mathit{ret}\ \sigma\ \mathit{stk}\ (\text{\tt Iop}\ \mathit{op}\ \vec{a}\ d\ n)\
+    (d\ \text{\tt <=}\ e)\ (\sigma\ \text{\tt <=}\ n)}
+\stopformula
 
 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$
diff --git a/figures/timing-1.pdf b/figures/timing-1.pdf
index 8591313..24f8edd 100644
--- a/figures/timing-1.pdf
+++ b/figures/timing-1.pdf
diff --git a/figures/timing-2.pdf b/figures/timing-2.pdf
index 67b3a8e..36075c6 100644
--- a/figures/timing-2.pdf
+++ b/figures/timing-2.pdf
diff --git a/figures/timing-3.pdf b/figures/timing-3.pdf
index dd18ea9..68f4cf8 100644
--- a/figures/timing-3.pdf
+++ b/figures/timing-3.pdf
diff --git a/fonts_env.tex b/fonts_env.tex
index 157d4f3..313a2ea 100644
--- a/fonts_env.tex
+++ b/fonts_env.tex
@@ -18,10 +18,10 @@
 \definefallbackfamily[lsrfont][math][modern][range={uppercasescript,lowercasescript}]
 
 \starttypescript [lsrfont]
-  \definetypeface [lsrfont] [rm] [serif] [palatino]   [default]
-  \definetypeface [lsrfont] [ss] [sans]  [heros]      [default]
-  \definetypeface [lsrfont] [tt] [mono]  [modern]     [default]
-  \definetypeface [lsrfont] [mm] [math]  [eulernova]  [default]
+  \definetypeface [lsrfont] [rm] [serif] [palatino] [default]
+  \definetypeface [lsrfont] [ss] [sans]  [heros]    [default]
+  \definetypeface [lsrfont] [tt] [mono]  [modern]   [default]
+  \definetypeface [lsrfont] [mm] [math]  [palatino] [default]
 \stoptypescript
 
 \stopenvironment
diff --git a/lsr_env.tex b/lsr_env.tex
index 01a549b..5073992 100644
--- a/lsr_env.tex
+++ b/lsr_env.tex
@@ -21,6 +21,8 @@
     style=\rm,
 ]
 
+\placebookmarks[chapter,section,subsection]
+
 \usecolors[crayola]
 %\placebookmarks[chapter,section,subsection,subsubsection][chapter,section]
 %\setupinteractionscreen[option=bookmark]