1 files changed, 25 insertions, 0 deletions
diff --git a/content/zettel/3c3b1.md b/content/zettel/3c3b1.md
new file mode 100644
index 0000000..f4f8ce2
--- /dev/null
+++ b/content/zettel/3c3b1.md
@@ -0,0 +1,25 @@
++++
+title = "Matching states in RTLBlock and RTLPar"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3c3b"]
+forwardlinks = ["3c3b2"]
+zettelid = "3c3b1"
++++
+
+One issue is how to match states from the translation from RTLBlock to
+RTLPar. Even though the translation is quite straightforward, matching
+the states is still quite tricky because of issues with missing
+intentional equality between memories and registers.
+
+To match states, we therefore have to ensure that the RTLPar memory is
+*extended* from the RTLBlock memory, so that all loads and stores still
+result in the same values. In addition to that we need to check that the
+register file is *less defined* than the RTLBlock register file.
+Finally, stack frames also need to match, which also only have to be
+*less defined*.
+
+Finally, we also need to assert that the function was translated using
+the translation function that ensures that all the basic blocks succeed
+in the validation.