diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-04 17:23:41 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-04 17:23:41 +0100 |
commit | b55e522ca286bbe96be3ce5fc05c984b2a4a130a (patch) | |
tree | 96abdce0ce13a2bf567a75bb0fcb40d27917c7a6 /backend/CSE2proof.v | |
parent | e88c7fa00a5174ecf897b3cb59b7adee818a1788 (diff) | |
download | compcert-kvx-b55e522ca286bbe96be3ce5fc05c984b2a4a130a.tar.gz compcert-kvx-b55e522ca286bbe96be3ce5fc05c984b2a4a130a.zip |
invariant guaranteed
Diffstat (limited to 'backend/CSE2proof.v')
-rw-r--r-- | backend/CSE2proof.v | 56 |
1 files changed, 53 insertions, 3 deletions
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. |