diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 15:08:16 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 15:08:16 +0100 |
| commit | d5bbfed2c8a0a208cf365abb1df249c9d91ff8e4 (patch) | |
| tree | a45099b41d9e67247f22cf216bff10b9e3b9b2d4 /backend/CSE3analysisproof.v | |
| parent | 11dc19dc169d99a944abb4144ea67eb4fc03f883 (diff) | |
| download | compcert-kvx-d5bbfed2c8a0a208cf365abb1df249c9d91ff8e4.tar.gz compcert-kvx-d5bbfed2c8a0a208cf365abb1df249c9d91ff8e4.zip | |
oper1
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index a1e57eb5..5eff5e08 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -552,4 +552,18 @@ Section SOUNDNESS. rewrite PSet.gaddo in CONTAINS by congruence. apply (kill_reg_sound rel rs m dst v REL i eq); auto. Qed. + + Hint Resolve oper2_sound : cse3. + + Theorem oper1_sound: + forall no dst sop args rel rs m v, + sem_rel rel rs m -> + sem_rhs sop args rs m v -> + sem_rel (oper1 (ctx := ctx) no dst sop args rel) (rs # dst <- v) m. + Proof. + intros. + unfold oper1. + destruct in_dec; auto with cse3. + Qed. + End SOUNDNESS. |