Add statistics

1 files changed, 23 insertions, 0 deletions

diff --git a/proof.tex b/proof.tex
index 4d617b5..f0c3564 100644
--- a/proof.tex
+++ b/proof.tex
@@ -105,6 +105,29 @@ The Verilog semantics that are used are deterministic, as the order of operation
 
 \subsection{Coq Mechanisation}
 
+\begin{table*}
+  \centering
+  \begin{tabular}{p{4cm}p{1cm}p{1cm}p{1cm}p{1.5cm}p{1cm}}
+    \toprule
+    & \textbf{Coq Code} & \textbf{OCaml Code} & \textbf{Specifi\-cations} & \textbf{Theorems \& Proofs} & \textbf{Total}\\
+    \midrule
+    {\footnotesize Data structures and libraries} & 274 & - & - & 654 & 928\\
+    {\footnotesize Integer, values} & 2 & 8 & 10 & &\\
+    {\footnotesize HTL semantics} & 1048 & 8093 & 9141 & &\\
+    {\footnotesize HTL generation} & 2 & 8 & 10 & &\\
+    {\footnotesize Verilog semantics} & 2 & 8 & 10 & &\\
+    {\footnotesize Verilog generation} & 2 & 8 & 10 & &\\
+    {\footnotesize Top-level driver, pretty printers} & & & & &\\
+    \midrule
+    \textbf{Total} & & & & &\\
+    \bottomrule
+  \end{tabular}
+  \caption{Statistics about the proof.}
+  \label{tab:proof_statistics}
+\end{table*}
+
+The Coq mechanisation 
+
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "main"