From c6fcc3d366c9a39fce73c1e5d20b7c0bdf515c86 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 12 Nov 2020 12:33:12 +0000
Subject: Add coq mechanisation

---
 proof.tex | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'proof.tex')

diff --git a/proof.tex b/proof.tex
index eb39834..061ea8d 100644
--- a/proof.tex
+++ b/proof.tex
@@ -118,6 +118,8 @@ x \div 2^y =
 
 The \compcert{} semantics for the \texttt{Oshrximm} instruction express it's operation exactly as shown in the equation above, even though in hardware the computation that would be performed would be different.  In \vericert{}, if the same operation would be implemented using Verilog operators, it is not guaranteed to be optimised correctly by the synthesis tools that convert the Verilog into a circuit.  To guarantee an output that does not include divides, we therefore have to express it in Verilog using shifts, and then prove that this representation is equivalent to the divide representation used in the \compcert{} semantics.  This proof discovered quite a few bugs in our initial implementation of optimisations, which rounded to $-\infty$ instead of 0.
 
+\subsection{Coq Mechanisation}
+
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "main"
-- 
cgit 

