From e4c7ff447ad30832c42ee51f0fe7e1cf62d2eee9 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 5 Feb 2020 17:34:03 +0100 Subject: wellformed_reg_kill_mem --- backend/CSE2proof.v | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) (limited to 'backend/CSE2proof.v') diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 4d503f90..0d369e7a 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -321,7 +321,8 @@ Proof. rewrite PTree.gro by congruence. apply Hrel; trivial. Qed. - +Local Hint Resolve wellformed_reg_kill_reg : wellformed. + Lemma wellformed_mem_kill_mem: forall rel, (wellformed_mem rel) -> (wellformed_mem (kill_mem rel)). @@ -343,6 +344,21 @@ Proof. Qed. Local Hint Resolve wellformed_mem_kill_mem : wellformed. +Lemma wellformed_reg_kill_mem: + forall rel, + (wellformed_reg rel) -> (wellformed_reg (kill_mem rel)). +Proof. + unfold wellformed_reg, kill_mem. + simpl. + intros rel Hrel. + intros i j sv KILLMEM KILLABLE. + apply Hrel with (sv := sv); trivial. + rewrite PTree.gremove_t in KILLMEM. + destruct ((mem_used rel) ! i) in KILLMEM. + discriminate. + assumption. +Qed. + Lemma wellformed_mem_move: forall r dst rel, (wellformed_mem rel) -> (wellformed_mem (move r dst rel)). -- cgit