Add caption above the table

1 files changed, 3 insertions, 4 deletions

diff --git a/proof.tex b/proof.tex
index 0d6d4b1..6446c9b 100644
--- a/proof.tex
+++ b/proof.tex
@@ -216,8 +216,9 @@ The final lemma we need is that the Verilog we generate is deterministic. This r
 
 \subsection{Coq Mechanisation}
 
-\begin{table*}
+\begin{table}
   \centering
+  \caption{Statistics about the numbers of lines of code in the proof and implementation of \vericert{}.}\label{tab:proof_statistics}
   \begin{tabular}{lrrrrr}
     \toprule
     & \textbf{Coq code} & \multicolumn{1}{p{1cm}}{\raggedleft\textbf{OCaml code}} & \textbf{Spec} & \multicolumn{1}{p{2cm}}{\raggedleft\textbf{Theorems \& Proofs}} & \textbf{Total}\\
@@ -234,9 +235,7 @@ The final lemma we need is that the Verilog we generate is deterministic. This r
     \textbf{Total}                      & 1721 & 775 & 693  & 8355 & 11544 \\
     \bottomrule
   \end{tabular}
-  \caption{Statistics about the numbers of lines of code in the proof and implementation of \vericert{}.}
-  \label{tab:proof_statistics}
-\end{table*}
+\end{table}
 
 The lines of code for the implementation and proof of \vericert{} can be found in Table~\ref{tab:proof_statistics}.  Overall, it took about 1.5 person-years to build \vericert{} -- about three person-months on implementation and 15 person-months on proofs.  The largest proof is the correctness proof for the HTL generation, which required equivalence proofs between all integer operations supported by \compcert{} and those supported in hardware.  From the 3069 lines of proof code in the HTL generation, 1189 are for the correctness proof of just the load and store instructions.  These were tedious to prove correct because of the substantial difference between the memory models used, and the need to prove properties such as stores outside of the allocated memory being undefined, so that a finite array could be used. In addition to that, since pointers in HTL and Verilog are represented as integers, whereas there is a separate `pointer' value in the \compcert{} semantics, it was painful to reason about them and many new theorems had to be proven about integers and pointers in \vericert{}.  Moreover, the second-largest proof of the correct RAM generation includes many proofs about the extensional equality of array operations, such as merging arrays with different assignments.  As the negative edge implies two merges take place every clock cycle, the proofs about the equality of the arrays becomes more tedious as well.