From d5bbfed2c8a0a208cf365abb1df249c9d91ff8e4 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 10 Mar 2020 15:08:16 +0100
Subject: oper1

---
 backend/CSE3analysisproof.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'backend/CSE3analysisproof.v')

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.
-- 
cgit