blob: 92affd0773c180fe86d8c810a44de214887fe7d8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
+++
title = "Equation lemma proof"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a8e2"]
forwardlinks = ["3a8g"]
zettelid = "3a8e3"
+++
The equation lemma is proven by defining a constant property over the
semantics, and proving that correct. This is proven in two parts:
1. Prove the property using the initial entry point of the control flow
graph.
2. Prove the property for an arbitrary point, assuming that the
property holds for the previous value in the control flow graph.
This therefore results in a kind of induction over the semantics
themselves, and then allows one to use the property anywhere in the
semantics preservation proof.
This can be used to prove the equation lemma, because the proof of
preservation of the registers can be proven that way, but it can also be
used for other proofs, such as proving the CompCertGSA ([\#3a8g])
generation correct.
[\#3a8g]: /zettel/3a8g
|
