Update on Overleaf.

1 files changed, 3 insertions, 0 deletions

diff --git a/proof.tex b/proof.tex
index 86ad1f9..eb39834 100644
--- a/proof.tex
+++ b/proof.tex
@@ -15,6 +15,7 @@ However, this forward simulation might still allow for wrong behaviour of the ta
 \end{equation*}
 
 To prove this statement, we therefore have to prove that the Verilog semantics are deterministic and that the forward simulation between the C and the Verilog holds as well.
+\JW{Hm, I'm a little confused. Which theorem is the actual `correctness' theorem? Looks like we could combine the two theorems into something like \[\forall C, V, B \notin \texttt{Wrong},\, \yhfunction{HLS} (C) = \yhconstant{OK} (V) \implies (V \Downarrow_{s} B ~\text{iff}~ C \Downarrow B)\] Is that the theorem you actually want?}
 
 \subsection{Forward Simulation}
 
@@ -94,6 +95,8 @@ The Verilog semantics that are used are deterministic, as the order of operation
 
 \subsection{Coq Mechanisation}
 
+\JW{Would be nice to include a few high-level metrics here. How many person-years of effort was the proof (very roughly)? How many lines of Coq? How many files, how many lemmas? How long does it take for the Coq proof to execute?}
+
 \subsection{Proving \texttt{Oshrximm} correct}
 
 % Mention that this optimisation is not performed sometimes (clang -03).