More proof changes

1 files changed, 4 insertions, 0 deletions

diff --git a/archive/proof.tex b/archive/proof.tex
index 9e962b7..6641c8d 100644
--- a/archive/proof.tex
+++ b/archive/proof.tex
@@ -1,3 +1,7 @@
+One example is the translation of instructions, where the translation function might contain many implementation specific details, such as in which order instructions are added to the data path or the control path, whereas the specification describes only describes which instructions were added.  The specification, \texttt{tr\_instr} can then be described as follows, where \textit{fin}, \textit{rtrn}, $\sigma$ and \textit{stk} are the registers for the finished signal, return value, current state and stack respectively, $i$ is the 3AC instruction being translated, and \textit{data} and \textit{control} are the data-flow and control logic map respectively.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 Firstly, as the input representation is a map, all the keys of the map will be unique, which will be translated to the matched expressions in the case statement.  In addition to that, the assumption is made that every possible evaluation of the state value will give a valid state, meaning the key will be present in the map.  Both of these observations mean that after the translation, for every possible value of the state, the case statement will be able to match an expression and enter the correct statement.  As each key is unique, if the state matches a case expression, then this also means that this is the only case expression that it could match, and it therefore has to be the correct case expression which contains the same statement as the map.
 
 However, the proof of uniqueness of the keys only works if the translation function is \emph{injective}, meaning that the function will result in distinct outputs for all possible inputs.  Otherwise, the proof of uniqueness of the keys for the input would not translate to a uniqueness of possible case expression matches in the output.  However, in our case the translation function is actually not injective, even though it might at first seem like it, because the state is stored as an integer, whereas the map is addressable by any positive number.  This means that if the positive number is greater than the maximum value that can be stored in the integer, the overflow would result in the wrong states being accessed.  To make the function injective, we therefore have to prove that the input positive number is never greater than $2^{32}-1$ so that the uniqueness property also holds for the output.