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/CSE2proof.v | 56 ++++++++++++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 53 insertions(+), 3 deletions(-)

(limited to 'backend/CSE2proof.v')

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