summaryrefslogtreecommitdiffstats
path: root/proof.tex
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-04-11 15:58:09 +0100
committerYann Herklotz <git@yannherklotz.com>2021-04-11 16:55:51 +0100
commitf1e4ebdba3c05e1c5d83eeb338c62fc3227b1a1a (patch)
tree096bb355bcbb3b465bd531cc793f7391e2c49d83 /proof.tex
parent9c107a5bd8330ca9b5b6bdadf715b2a48dda1489 (diff)
downloadoopsla21_fvhls-f1e4ebdba3c05e1c5d83eeb338c62fc3227b1a1a.tar.gz
oopsla21_fvhls-f1e4ebdba3c05e1c5d83eeb338c62fc3227b1a1a.zip
Add new results
Diffstat (limited to 'proof.tex')
-rw-r--r--proof.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/proof.tex b/proof.tex
index fe76db8..058969a 100644
--- a/proof.tex
+++ b/proof.tex
@@ -63,7 +63,7 @@ In the following lemma, $\yhfunction{spec\_htl}$ is the top-level specification
\subsubsection{From Specification to Simulation}
-To prove that the specification predicate implies the desired forward simulation, we must first define a relation that matches each 3AC state to an equivalent HTL state. This relation also captures the assumptions made about the 3AC code that we receive from \compcert{}.% so that these assumptions can be used to prove the translations correct.
+To prove that the specification predicate implies the desired forward simulation, we must first define a relation that matches each 3AC state to an equivalent HTL state. This relation also captures the assumptions made about the 3AC code that we receive from \compcert{}. % so that these assumptions can be used to prove the translations correct.
These assumptions then have to be proven to always hold assuming the HTL code was created by the translation algorithm. Some of the assumptions that need to be made about the 3AC and HTL code for a pair of states to match are:
\begin{itemize}