Fix layout and numbering of figures

4 files changed, 50 insertions, 30 deletions

diff --git a/.gitignore b/.gitignore
index 1dee67d..3a8cb0d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -302,3 +302,6 @@ TSWLatexianTemp*
 
 *.vimout
 *.tuc
+
+*.pgf
+*.pdf
diff --git a/Makefile b/Makefile
index 25f3414..55c4e4f 100644
--- a/Makefile
+++ b/Makefile
@@ -2,7 +2,13 @@
 
 all: main.pdf
 
+main.pdf: figures/timing-1.pdf figures/timing-2.pdf
+
+figures/%.pdf: figures/%.tex
+	latexmk -pdf -shell-escape $<
+	cp $(notdir $@) $@ || true
+
 # silent structure,structures,pages,resolvers,open source,close source,loading,modules
 %.pdf: %.tex
 	context --nonstopmode --silent='*' $<
-	mv $(notdir $@) $@
+	cp $(notdir $@) $@ || true
diff --git a/chapters/hls.tex b/chapters/hls.tex
index 1276450..ef75e78 100644
--- a/chapters/hls.tex
+++ b/chapters/hls.tex
@@ -84,8 +84,7 @@ chosen as the output language for Vericert because it is one of the most popular
 already exist a few formal semantics for it that could be used as a
 target~\cite{loow19_verif_compil_verif_proces, meredith10_veril}.  Bluespec, previously ruled out as
 a source language, is another possible target and there exists a formally verified translation to
-circuits using
-K\^{o}ika~\cite{bourgeat20_essen_blues}.
+circuits using Kôika~\cite{bourgeat20_essen_blues}.
 
 \paragraph{Choice of implementation language.} We chose Coq as the implementation language because
 of its mature support for code extraction; that is, its ability to generate OCaml programs directly
@@ -187,7 +186,7 @@ Vericert, this event is either a positive (rising) or a negative (falling) clock
 always-blocks triggering on the same event are executed in parallel. Always-blocks can also express
 control-flow using if-statements and case-statements.
 
-\startplacemarginfigure[reference={fig:tutorial:state_machine},location=top,title={Hello}]
+\startplacemarginfigure[reference={fig:tutorial:state_machine},title={Hello}]
   \startfloatcombination [nx=2, ny=1]
     \startplacesubfigure
       \startframedtext[width={0.9\textwidth},frame=off,offset=none,loffset=3cm,bodyfont=11pt]
@@ -248,7 +247,7 @@ will reset the value of \mono{tmp} and then set \mono{z} to the original value o
 nonblocking assignment does not change its value until the end of the clock cycle.  Finally, the
 last always-block will set the state to 0 again.
 
-\startplacemarginfigure[location=top,reference={fig:accumulator_c_rtl},title={Translating a simple
+\startplacemarginfigure[reference={fig:accumulator_c_rtl},title={Translating a simple
     program from C to Verilog.}]
   \startfloatcombination[nx=2,ny=1]
     \startplacefigure[number=no]
@@ -379,7 +378,7 @@ making it easier to prove optimisations like proper RAM insertion.
     split into a data-path and control logic for the next state calculation.  The Update block takes
     the current state, current values of all registers and at most one value stored in the RAM, and
     calculates a new value that can either be stored back in the RAM or in a
-    register.},reference={fig:accumulator_diagram},location=top]
+    register.},reference={fig:accumulator_diagram}]
 \definecolor[control][x=B3E2CD]
 \definecolor[data][x=FDCDAC]
 \starttikzpicture
@@ -783,7 +782,7 @@ because (currently) only supports types represented by 32 bits.
 
 \subsection[sec:verilog:integrating]{Integrating the Verilog Semantics into 's Model}
 
-\startplacemarginfigure[location=top]
+\startplacemarginfigure
 \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
@@ -904,11 +903,10 @@ Verilog and CompCert's existing intermediate languages.
 
 \startitemize
 \item
-  As already mentioned in Section~\goto{{[}sec:verilog:memory{]}}[sec:verilog:memory], because the
-  memory model in our Verilog semantics is finite and concrete, but the CompCert memory model is
-  more abstract and infinite with additional bounds, the equivalence of these models needs to be
-  proven.  Moreover, our memory is word-addressed for efficiency reasons, whereas CompCert's memory
-  is byte-addressed.
+  As already mentioned in \in{Section}[sec:verilog:memory], because the memory model in our Verilog
+  semantics is finite and concrete, but the CompCert memory model is more abstract and infinite with
+  additional bounds, the equivalence of these models needs to be proven.  Moreover, our memory is
+  word-addressed for efficiency reasons, whereas CompCert's memory is byte-addressed.
 \item
   Second, the Verilog semantics operates quite differently to the usual intermediate languages in
   CompCert. All the CompCert intermediate languages use a map from control-flow nodes to
@@ -922,9 +920,9 @@ 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
-Section~\goto{{[}sec:design{]}}[sec: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.
+\in{Section}[sec: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}
 
@@ -954,11 +952,10 @@ terminate with an answer. To start the execution of the hardware and to signal t
 that the inputs are ready, the $\mathit{rst}$ signal is set and unset. Then, once the result is
 ready, the $\mathit{fin}$ signal is set and the result value is placed in $\mathit{ret}$. These
 signals are also present in the semantics of execution shown in
-Fig.~\goto{{[}fig:inference_module{]}}[fig:inference_module]. The correctness theorem therefore also
-uses these signals, and the proof shows that once the $\mathit{fin}$ flag is set, the value in
-$\mathit{ret}$ is correct according to the semantics of Verilog and Clight. Note that the compiler
-is allowed to fail and not produce any output; the correctness theorem only applies when the
-translation succeeds.
+\in{Figure}[fig:inference_module]. The correctness theorem therefore also uses these signals, and
+the proof shows that once the $\mathit{fin}$ flag is set, the value in $\mathit{ret}$ is correct
+according to the semantics of Verilog and Clight. Note that the compiler is allowed to fail and not
+produce any output; the correctness theorem only applies when the translation succeeds.
 
 How can we prove this theorem? First, note that the theorem is a \quote{backwards simulation} result
 (every target behaviour must also be a source behaviour), following the terminology used in the
@@ -1197,10 +1194,9 @@ $B_1$ and $B_2$ must be the same.
 \stoplemma
 
 \startproof
- The Verilog semantics is deterministic because the order of operation of all the constructs is
- defined, so there is only one way to evaluate the module, and hence only one possible behaviour.
- This was proven for the small-step semantics shown in
- Fig.~\goto{{[}fig:inference_module{]}}[fig:inference_module].
+  The Verilog semantics is deterministic because the order of operation of all the constructs is
+  defined, so there is only one way to evaluate the module, and hence only one possible behaviour.
+  This was proven for the small-step semantics shown in \in{Figure}[fig:inference_module].
 \stopproof
 
 \subsection[coq-mechanisation]{Coq Mechanisation}
diff --git a/lsr_env.tex b/lsr_env.tex
index 0f6c356..bb83171 100644
--- a/lsr_env.tex
+++ b/lsr_env.tex
@@ -217,24 +217,39 @@
 %\writetolist[headers]{}{Chapter \hfill Title \hfill Page}
 
 % @see https://tex.stackexchange.com/a/243726
-\setupcaptions[table][location=top]
+\setupcaptions[table][location=top,default=top]
 
 % ==========================================================================
 % Figure
 % ==========================================================================
-\setupcaptions[figure][location={high,rightmargin},width=5cm,align={yes, tolerant},style=\rmx]
+\setupcaptions[figure][
+  location={high,rightmargin},
+  width=\rightmarginwidth,
+  align={yes, tolerant},
+  style=\rmx,
+]
+\setupfloat[figure][default=top,location=middle]
 
 \definefloat[subfigure][local=yes]
-\setupcaption[subfigure][numbercommand=\groupedcommand{(}{)},numberconversion=a,prefix=no,way=bytext]
+\setupcaption[subfigure][
+  numbercommand=\groupedcommand{(}{)},
+  numberconversion=a,
+  prefix=no,
+  way=bytext
+]
 \setuplabeltext[subfigure=]
 
 \newdimen\LeftMarginSize
 \LeftMarginSize=\dimexpr \backspace + \rightmarginwidth + \rightmargindistance \relax
 \newdimen\TextAreaSize
 \TextAreaSize=\dimexpr \textwidth + \rightmarginwidth + \rightmargindistance \relax
-\definefloat[marginfigure][textmarginfigures]
-\setupfloat[marginfigure][location={inner},width=\TextAreaSize,number=figure]
-\setupcaptions[marginfigure][leftmargin=\dimexpr \LeftMarginSize / 2 \relax]
+\definefloat[marginfigure][marginfigures][figure]
+\setupfloat[marginfigure][location=inner,default=top,width=\TextAreaSize]
+\setupcaptions[marginfigure][
+  leftmargin=\dimexpr \LeftMarginSize / 2 \relax,
+  location=bottom,
+  width=\textwidth,
+]
 \setuplabeltext[marginfigure=Figure~]
 
 %\definereferenceformat[sfig][left={\determineheadnumber[figure]\currentheadnumber.}]