Fix weird alignment issues

2 files changed, 14 insertions, 15 deletions

diff --git a/chapters/hls.tex b/chapters/hls.tex
index b4f75d6..7e1f79e 100644
--- a/chapters/hls.tex
+++ b/chapters/hls.tex
@@ -804,7 +804,7 @@ because Vericert (currently) only supports types represented by 32 bits.
 \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]
+\startformula \startmathalignment[n=1]
   \NC\text{\sc Step }\ \frac{\startmatrix[n=1]
     \NC \Gamma_r[\mathit{rst}] = 0 \qquad \Gamma_r[\mathit{fin}] = 0 \NR
     \NC(m, (\Gamma_r, \Gamma_a))\ \downarrow_{\text{program}} (\Gamma_r', \Gamma_a') \NR
@@ -828,7 +828,7 @@ because Vericert (currently) only supports types represented by 32 bits.
     \NC\longrightarrow \text{\tt State}\ \mathit{sf}\ m\ \mathit{pc}\ (\Gamma_{r} [ \sigma \mapsto
       \mathit{pc}, r \mapsto v ])\ \Gamma_{a}\NR
     \stopmatrix}\NR
-\stopalign \stopformula
+\stopmathalignment \stopformula
 \stopplacefigure
 
 The CompCert computation model defines a set of states through which execution passes. In this
@@ -879,11 +879,11 @@ execution; likewise, the {\sc Return} rule is only matched for the final return
 function. Therefore, in addition to the rules shown in \in{Figure}[fig:inference_module], an initial
 state and final state need to be defined:
 
-\placeformula\startformula \startalign[n=1]
+\placeformula\startformula\startmathalignment[n=1]
   \NC\text{\sc Initial }\ \frac{\text{\tt is\_internal}\ P.\text{\tt main}}{\text{\tt initial\_state}\
     (\text{\tt Callstate}\ []\ P.\text{\tt main}\ [])}\NR
   \NC\text{\sc Final }\ \frac{}{\text{\tt final\_state}\ (\text{\tt Returnstate}\ []\ n)\ n}\NR
-\stopalign \stopformula
+\stopmathalignment\stopformula
 
 \noindent where the initial state is the \type{Callstate} with an empty stack frame and no arguments
 for the \type{main} function of program $P$, where this \type{main} function needs to be in the
@@ -1046,10 +1046,10 @@ Whenever the translation from $C$ succeeds and produces Verilog $V$, and all obs
 of $C$ are safe, then $V$ has behaviour $B$ only if $C$ has behaviour $B$.
 
 \placeformula\startformula
-  \startalign[n=1,align={1:right}]
+  \startmathalignment[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
+  \stopmathalignment
 \stopformula
 
 Why is this correctness theorem also the right one for HLS? It could be argued that hardware
@@ -1204,7 +1204,7 @@ matching state.
 
 \startplacefigure[reference={fig:htl_ram_spec},title={Specification for the memory implementation in
     HTL, where $r$ is the RAM, which is then implemented by equivalent Verilog code.}]
-  \startformula \startalign[n=1]
+  \startformula \startmathalignment[n=1]
   \NC \text{\sc Idle}\ \frac{\Gamma_{\rm r}[\mathit{r.en}] = \Gamma_{\rm r}[\mathit{r.u_{en}}]}{((\Gamma_{\rm r}, \Gamma_{\rm a}), \Delta, r) \downarrow_{\text{ram}} \Delta}\NR
 %
   \NC \text{\sc Load}\ \frac{\Gamma_{\rm r}[\mathit{r.en}] \ne \Gamma_{\rm
@@ -1221,7 +1221,7 @@ matching state.
       \mathit{r.u\_en}], \NR
 \NC \Delta_{\rm a}[\mathit{r.mem} \mapsto (\Gamma_{\rm a}[
         \mathit{r.mem}])[\mathit{r.addr} \mapsto \mathit{r.d_{in}}]]\NR\stopmatrix\right) } \NR
-  \stopalign \stopformula
+  \stopmathalignment \stopformula
 \stopplacefigure
 
 HTL can only represent a single state machine, so we must model the RAM abstractly to reason about
@@ -1300,7 +1300,6 @@ converted.
   \startformula
     \forall h, V, B \in \text{\tt Safe},\quad \text{\tt tr\_verilog} (h) = V \land h \Downarrow B
     \implies V \Downarrow B.
-
   \stopformula
 \stoplemma
 
diff --git a/chapters/scheduling.tex b/chapters/scheduling.tex
index 916812c..58528cd 100644
--- a/chapters/scheduling.tex
+++ b/chapters/scheduling.tex
@@ -291,13 +291,13 @@ next sections.
   \startfloatcombination[nx=2]
     \startplacefigure[reference={eq:standard},title={Syntax for instructions within a hyperblock.}]
       \startframedtext[frame=off,offset=none,width={0.45\textwidth}]
-      \startformula \startalign
+      \startformula\startmathalignment
 \NC i\ \ \eqdef \NC \ \ \text{\tt RBnop}                                                   \NR
 \NC                  \NC |\ \ \text{\tt RBop}\ p?\ \mathit{op}\ \vec{r}\ d                      \NR
 \NC                  \NC |\ \ \text{\tt RBload}\ p?\ \mathit{chunk}\ \mathit{addr}\ \vec{r}\ d  \NR
 \NC                  \NC |\ \ \text{\tt RBstore}\ p?\ \mathit{chunk}\ \mathit{addr}\ \vec{r}\ s \NR
 \NC                  \NC |\ \ \text{\tt RBsetpred}\ p?\ c\ \vec{r}\ d                           \NR
-\stopalign \stopformula
+\stopmathalignment\stopformula
 \stopframedtext
 
     \stopplacefigure
@@ -333,11 +333,11 @@ branch on a predicate an nests more control-flow instructions inside of it. This
 for if-conversion, when converting an already converted conditional statement, as depending on the
 predicate, a different control-flow instruction may be necessary.
 
-\placeformula[fig:hb_def]\startformula\startalign[align={1:left}]
+\placeformula[fig:hb_def]\startformula\startmathalignment[align={1:left}]
 \NC \blockbb \qquad \eqdef \qquad (\text{\tt slist}\ i) \times i_{\mathit{cf}} \NR \NC \parbb \qquad
 \eqdef \qquad (\text{\tt slist}\ (\text{\tt plist}\ (\text{\tt slist}\ i))) \times
 i_{\mathit{cf}}\NR
-\stopalign\stopformula
+\stopmathalignment\stopformula
 
 These instructions are use in \rtlblock\ as well as in \rtlpar. The main difference between these
 two languages is how these instructions are arranged within the hyperblock and the execution
@@ -539,7 +539,7 @@ predicated type and append the first predicated type to the second:
 
 \subsection[example-of-translation]{Example of translation}
 
-\placeformula[eq:4]\startformula\startalign[n=1,align={1:left}]
+\placeformula[eq:4]\startformula \startmathalignment[n=1,align={1:left}]
 \NC \text{\tt r1} =
 \startcases
   \NC \text{\tt r1}^{0} + \text{\tt r4}^{0} + \text{\tt r4}^{0}, \quad \NC \text{\tt p1} \NR
@@ -555,7 +555,7 @@ predicated type and append the first predicated type to the second:
   \NC \text{\tt !p2 \&\& p1}\NR
   \NC \text{\tt r3}^{0} \times \text{\tt r3}^{0},\quad \NC\text{\tt p2 \&\& p1}\NR
 \stopcases\NR
-\stopalign \stopformula
+\stopmathalignment \stopformula
 
 Using the example shown in \in{Figure}[fig:op_chain], the \rtlblock\ hyperblock shown in
 \in{Figure}{a}[fig:op_chain] is scheduled into the hyperblock \rtlpar\ shown in