diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-09 10:49:55 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-09 10:49:55 +0100 |
| commit | a54ea2bfba2ca35b968bbad36bd7e24e5da124c0 (patch) | |
| tree | 15710a9c1f471c0b1b501c5d51f73b36e5237b87 | |
| parent | 414c9f51fc8dcafe5a1deb873c682105ba554bb8 (diff) | |
| download | compcert-kvx-a54ea2bfba2ca35b968bbad36bd7e24e5da124c0.tar.gz compcert-kvx-a54ea2bfba2ca35b968bbad36bd7e24e5da124c0.zip | |
apply_cond0_sound
| -rw-r--r-- | backend/CSE3analysisproof.v | 26 |
1 files changed, 25 insertions, 1 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 75dae91a..a012771c 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -1317,7 +1317,31 @@ Section SOUNDNESS. } exact REL. Qed. - + + Lemma apply_cond0_sound : + forall pc cond args rel rs m + (COND : (eval_condition cond (rs ## args) m) = Some true) + (REL : (sem_rel rel rs m)), + (sem_rel (apply_cond0 (ctx:=ctx) pc cond args rel) rs m). + Proof. + intros. + unfold apply_cond0. + destruct eq_find as [eq_id | ] eqn:FIND; cbn. + 2: assumption. + pose proof (eq_find_sound pc (Cond cond args) eq_id FIND) as FIND_SOUND. + intros eq_id' eq' CONTAINS CATALOG. + destruct (peq eq_id eq_id'). + { subst eq_id'. + unfold sem_eq. + rewrite FIND_SOUND in CATALOG. + inv CATALOG. + assumption. + } + rewrite PSet.gaddo in CONTAINS by assumption. + unfold sem_rel in REL. + eapply REL; eassumption. + Qed. + (* Section INDUCTIVENESS. Variable fn : RTL.function. |