apply_cond1_sound

1 files changed, 30 insertions, 0 deletions

diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index 8cc009cc..75dae91a 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -1288,6 +1288,36 @@ Section SOUNDNESS.
 
   Hint Resolve external_call_sound : cse3.
 
+
+  Definition sem_rel_b (rel : RB.t) (rs : regset) (m : mem) :=
+    match rel with
+    | None => False
+    | Some rel => sem_rel rel rs m
+    end.
+  
+  Lemma apply_cond1_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_b (apply_cond1 (ctx:=ctx) pc cond args rel) rs m).
+  Proof.
+    intros.
+    unfold apply_cond1.
+    destruct eq_find as [eq_id | ] eqn:FIND; cbn.
+    2: assumption.
+    destruct PSet.contains eqn:CONTAINS.
+    {
+      pose proof (eq_find_sound pc (Cond (negate_condition cond) args) eq_id FIND) as FIND_SOUND.
+      unfold sem_rel in REL.
+      pose proof (REL eq_id (Cond (negate_condition cond) args) CONTAINS FIND_SOUND) as REL_id.
+      cbn in REL_id.
+      rewrite eval_negate_condition in REL_id.
+      rewrite COND in REL_id.
+      discriminate.
+    }
+    exact REL.
+  Qed.
+        
   (*
   Section INDUCTIVENESS.
     Variable fn : RTL.function.