1 files changed, 29 insertions, 0 deletions
diff --git a/content/zettel/3c3i1.md b/content/zettel/3c3i1.md
new file mode 100644
index 0000000..284b63b
--- /dev/null
+++ b/content/zettel/3c3i1.md
@@ -0,0 +1,29 @@
++++
+title = "Repeated application of a translation pass in CompCert"
+date = "2022-10-04"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3c3i"]
+forwardlinks = []
+zettelid = "3c3i1"
++++
+
+Currently it's true that if-conversion is quite tricky to prove, because
+the recursive nature of the translation is quite complicated. However,
+if one limits the translation to just modifying parts of the code in a
+non-recursive way, then the proof becomes simpler. At every point one
+only has to reason about two possibilities, either the current point has
+been converted, meaning another block that exists in the graph has been
+chosen and has been inlined, or the current block has not changed at
+all.
+
+Once one has defined a translation like that, one can just repeat it
+multiple times with different rewrites to get any kind of
+transformations one wants. To prove the correctness of the multiple
+applications one should be able to prove that the `match_prog` property
+holds for any reflexive and transitive closure. In addition to that, an
+instance of the linker type class also needs to be implemented to show
+that separate compilation is still supported as well, however that
+should also just work because the `match_prog` property is very similar
+to other `match_prog` properties.