1 files changed, 64 insertions, 0 deletions
diff --git a/content/zettel/3a5c1.md b/content/zettel/3a5c1.md
new file mode 100644
index 0000000..857e31d
--- /dev/null
+++ b/content/zettel/3a5c1.md
@@ -0,0 +1,64 @@
++++
+title = "Mutliple to one step simulation"
+date = "2022-04-24"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3a5c"]
+forwardlinks = ["3c3h1", "1b6", "3c3", "3a5c1a"]
+zettelid = "3a5c1"
++++
+
+This has been implemented in CompCert-KVX ([\#3c3h1]) \[1\] (Figure 12).
+
+The main problem that is often encountered is that you want to do
+multiple steps in the source language, and only one step in the output
+language. One example of this is when adding basic blocks ([\#1b6]) to
+the target language. In this case, one will often define the execution
+of the basic block using big-step semantics, as otherwise there would
+not be a great benefit of using these semantics. These semantics are
+useful for proving scheduling ([\#3c3]), for example. However, this
+means that the semantics are not in a one to one correspondence anymore.
+
+The traditional way to prove a forward simulation between a source and a
+target language is by using a simulation in lock-step, where one step in
+the input corresponds to one step in the output. However, a
+generalisation of this is to allow for the fact that one step in the
+input could match one or more steps in the output semantics. This is
+directly supported by the small step semantics framework inside of
+CompCert. Finally, another generalisation is that one step in the input
+could correspond to zero or more steps in the output. This comes with
+the limitation that one has to show that the semantics will not get
+stuck, meaning there is some constantly decreasing metric when one is
+not performing a step.
+
+However, none of these things directly solve the issue of having to
+perform multiple step in the input to be able to even do one step in the
+output. To do this, one will have to abuse the star simulation (zero or
+more steps), but keep track of the previous steps that one has already
+performed to be able to reconstruct the proof from the start of the
+output step to the end of the output step. This can be done by always
+performing a `star_refl` step (don't perform a step), but still create a
+way to match states until one reaches the end of the output step.
+
+<div id="refs" class="references csl-bib-body" markdown="1">
+
+<div id="ref-six22_formal_verif_super_sched" class="csl-entry"
+markdown="1">
+
+<span class="csl-left-margin">\[1\]
+</span><span class="csl-right-inline">C. Six, L. Gourdin, S. Boulmé, D.
+Monniaux, J. Fasse, and N. Nardino, “Formally verified superblock
+scheduling,” in *Proceedings of the 11th ACM SIGPLAN international
+conference on certified programs and proofs*, in CPP 2022. Philadelphia,
+PA, USA: Association for Computing Machinery, 2022, pp. 40–54. doi:
+[10.1145/3497775.3503679].</span>
+
+</div>
+
+</div>
+
+  [\#3c3h1]: /zettel/3c3h1
+  [\#1b6]: /zettel/1b6
+  [\#3c3]: /zettel/3c3
+  [10.1145/3497775.3503679]: https://doi.org/10.1145/3497775.3503679