1 files changed, 36 insertions, 0 deletions
diff --git a/content/zettel/3a8e.md b/content/zettel/3a8e.md
new file mode 100644
index 0000000..4a1e710
--- /dev/null
+++ b/content/zettel/3a8e.md
@@ -0,0 +1,36 @@
++++
+title = "Equations on SSA"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3a8g5c", "3a8g5b", "3a8d"]
+forwardlinks = ["3a8f", "3a8e1"]
+zettelid = "3a8e"
++++
+
+There is also a notion of equations in CompCertSSA, which means that one
+can mathematically express the value that are stored in some registers.
+
+``` coq
+Lemma equation_lemma :
+  forall prog d op args x succ f m rs sp pc s,
+    wf_ssa_program prog ->
+    reachable prog (State s f sp pc rs m) ->
+    fn_code f d = Some (Iop op args x succ) ->
+    sdom f d pc ->
+    eval_operation sp op (rs##args) m = Some (rs#x).
+```
+
+Using the above Lemma, it is therefore possible to show that if
+operation at `d` is an assignment of an `Iop` instruction to `x`, then
+one can show that the evaluation of the operation with the arguments at
+the current register set will be equal to the value that is stored in
+the register set at `x`.
+
+**Question**: One question I have though, is can the args of the current
+register set not be different to the register set that was initially
+used to evaluate the initial `Iop` instruction?
+
+**Answer**: Actually, one possible answer to this is that the register
+already encode the index, so the args will actually be exactly the same
+that were used in the original evaluation of the `Iop` intruction.