Fix

1 files changed, 0 insertions, 4 deletions

diff --git a/proof.tex b/proof.tex
index bc1d95f..6749482 100644
--- a/proof.tex
+++ b/proof.tex
@@ -168,10 +168,6 @@ The HTL-to-Verilog simulation is conceptually simple, as the only transformation
   %The proof of the translation from maps to case-statements follows by induction over the list of elements in the map and the fact that each key will be unique.  In addition to that, the statement that is currently being evaluated is guaranteed by the correctness of the list of elements to be in that list.  The latter fact therefore eliminates the base case, as an empty list does not contain the element we know is in the list.  The other two cases follow by the fact that either the key is equal to the evaluated value of the case expression, or it isn't.  In the first case we can then evaluate the statement and get the state after the case expression, as the uniqueness of the key tells us that the key cannot show up in the list anymore.  In the other case we can just apply the inductive hypothesis and remove the current case from the case statement, as it did not match.
 \end{proof}
 
-One problem with our representation of the state as an actual register is that we have to make sure that the state does not overflow.  Currently, the state register always has 32 bits, meaning the maximum number of states supported is $2^{32}$.
-%This means that during the translation we have to check that each state can fit into an integer. 
-\vericert{} will error out if there are more than this many nodes in the 3AC, thus satisfying the correctness theorem vacuously.
-
 \subsection{Deterministic Semantics}\label{sec:proof:deterministic}
 
 %Finally, to obtain the backward simulation that we want, it has to be shown that if we generate hardware with a specific behaviour, that it is the only possible program with that behaviour.  This only has to be performed for the final intermediate language, which is Verilog, so that the backward simulation holds for the whole chain from Clight to Verilog.