diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-14 21:56:30 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-14 21:56:30 +0200 |
| commit | 7c6ce18466ed1de58a0f99c785c777d63a9a6149 (patch) | |
| tree | c1afac8e4b12fc833b4da838abbd38eca3f98be0 /backend/CSE3analysisproof.v | |
| parent | 1050bb788994cd6944770bf754230f4c90d9442b (diff) | |
| download | compcert-kvx-7c6ce18466ed1de58a0f99c785c777d63a9a6149.tar.gz compcert-kvx-7c6ce18466ed1de58a0f99c785c777d63a9a6149.zip | |
a bit of progress
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index f4e3672d..0ddaa527 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -745,6 +745,25 @@ Section SOUNDNESS. Hint Resolve oper1_sound : cse3. + Lemma rel_idem_replace: + forall rel rs r m, + sem_rel rel rs m -> + sem_rel rel rs # r <- (rs # r) m. + Proof. + intros until m. + intro REL. + unfold sem_rel, sem_eq, sem_rhs in *. + intros. + specialize REL with (i:=i) (eq0:=eq). + rewrite Regmap.gsident. + replace ((rs # r <- (rs # r)) ## (eq_args eq)) with + (rs ## (eq_args eq)). + { apply REL; auto. } + apply list_map_exten. + intros. + apply Regmap.gsident. + Qed. + Lemma move_sound : forall no : node, forall rel : RELATION.t, @@ -756,6 +775,10 @@ Section SOUNDNESS. unfold move. intros until m. intro REL. + destruct (peq src dst). + { subst dst. + apply rel_idem_replace; auto. + } pose proof (eq_find_sound no {| eq_lhs := dst; eq_op := SOp Omove; eq_args := src :: nil |}) as EQ_FIND_SOUND. destruct eq_find. - intros i eq CONTAINS. |