From b55e522ca286bbe96be3ce5fc05c984b2a4a130a Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 4 Feb 2020 17:23:41 +0100
Subject: invariant guaranteed

---
 backend/CSE2.v      |  4 +++-
 backend/CSE2proof.v | 56 ++++++++++++++++++++++++++++++++++++++++++++++++++---
 2 files changed, 56 insertions(+), 4 deletions(-)

(limited to 'backend')

diff --git a/backend/CSE2.v b/backend/CSE2.v
index 2fc0c323..a818996b 100644
--- a/backend/CSE2.v
+++ b/backend/CSE2.v
@@ -268,6 +268,8 @@ Module ADD_BOTTOM(L : SEMILATTICE_WITHOUT_BOTTOM).
     - apply L.ge_refl.
       apply L.eq_refl.
   Qed.
+
+  Definition top := Some RELATION.top.
 End ADD_BOTTOM.
 
 Module RB := ADD_BOTTOM(RELATION).
@@ -441,7 +443,7 @@ Definition apply_instr' code (pc : node) (ro : RB.t) : RB.t :=
 
 Definition forward_map (f : RTL.function) := DS.fixpoint
   (RTL.fn_code f) RTL.successors_instr
-  (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top).
+  (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) RB.top.
 
 Definition forward_move_b (rb : RB.t) (x : reg) :=
   match rb with
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 15ce3ffb..351a4219 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -258,19 +258,69 @@ Proof.
 Qed.
 Local Hint Resolve wellformed_mem_load : wellformed.
 
-Definition wellformed_mem' (rb : RB.t) :=
+Definition wellformed_mem_rb (rb : RB.t) :=
   match rb with
   | None => True
   | Some r => wellformed_mem r
   end.
 
-Definition wellformed_apply_instr:
+Lemma wellformed_mem_apply_instr:
   forall instr rel,
     (wellformed_mem rel) ->
-    (wellformed_mem' (apply_instr instr rel)).
+    (wellformed_mem_rb (apply_instr instr rel)).
 Proof.
   destruct instr; simpl; auto with wellformed.
 Qed.
+Local Hint Resolve wellformed_mem_apply_instr : wellformed.
+
+Lemma wellformed_mem_rb_bot :
+  wellformed_mem_rb RB.bot.
+Proof.
+  simpl.
+  trivial.
+Qed.
+Local Hint Resolve wellformed_mem_rb_bot: wellformed.
+
+Lemma wellformed_mem_rb_top :
+  wellformed_mem_rb RB.top.
+Proof.
+  simpl.
+  auto with wellformed.
+Qed.
+Local Hint Resolve wellformed_mem_rb_top: wellformed.
+
+Lemma wellformed_mem_rb_apply_instr':
+  forall code pc rel,
+    (wellformed_mem_rb rel) ->
+    (wellformed_mem_rb (apply_instr' code pc rel)).
+Proof.
+  destruct rel; simpl; trivial.
+  intro.
+  destruct (code ! pc);
+  eauto with wellformed.
+Qed.
+Local Hint Resolve wellformed_mem_rb_apply_instr' : wellformed.
+
+Lemma wellformed_mem_rb_lub : forall a b,
+    (wellformed_mem_rb a) -> (wellformed_mem_rb b) -> (wellformed_mem_rb (RB.lub a b)).
+Proof.
+  destruct a; destruct b; simpl; auto with wellformed.
+Qed.
+Local Hint Resolve wellformed_mem_rb_lub: wellformed.
+
+Definition wellformed_mem_fmap fmap :=
+  forall i, wellformed_mem_rb (fmap !! i).
+
+Theorem wellformed_mem_forward_map : forall f,
+    forall fmap, (forward_map f) = Some fmap ->
+    wellformed_mem_fmap fmap.
+Proof.
+  intros.
+  unfold forward_map in *.
+  unfold wellformed_mem_fmap.
+  intro.
+  eapply DS.fixpoint_invariant with (ev := Some RELATION.top); eauto with wellformed.
+Qed.
 
 Local Transparent kill_reg.
 
-- 
cgit