remains one admit

1 files changed, 46 insertions, 8 deletions

diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 3fbc9912..215f5c41 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -765,14 +765,52 @@ Proof.
         eapply external_call_sound; eauto with cse3.
         
   - (* Icond *)
-    econstructor. split.
-    + eapply exec_Icond with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption.
-      * TR_AT. reflexivity.
-      * rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial.
-        eassumption.
-      * reflexivity.
-    + econstructor; eauto.
-      destruct b; IND_STEP.
+    destruct (find_cond_in_fmap (ctx := (context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc cond args) as [bfound | ] eqn:FIND_COND.                                                                    
+    + econstructor; split.
+      * eapply exec_Inop; try eassumption.
+        TR_AT. unfold transf_instr. rewrite FIND_COND. reflexivity.
+      * replace bfound with b.
+        { econstructor; eauto.
+          admit.
+        }
+        unfold find_cond_in_fmap in FIND_COND.
+        change RB.t with (option RELATION.t) in REL.
+        change Regmap.get with PMap.get in REL.
+        destruct (@PMap.get (option RELATION.t) pc
+                            (@fst invariants analysis_hints (preanalysis tenv f))) as [rel | ] eqn:FIND_REL.
+        2: discriminate.
+        pose proof (is_condition_present_sound pc rel cond args rs m REL) as COND_PRESENT_TRUE.
+        pose proof (is_condition_present_sound pc rel (negate_condition cond) args rs m REL) as COND_PRESENT_FALSE.
+        rewrite eval_negate_condition in COND_PRESENT_FALSE.
+        destruct (is_condition_present pc rel cond args).
+        { rewrite COND_PRESENT_TRUE in H0 by trivial.
+          congruence.
+        }
+        destruct (is_condition_present pc rel (negate_condition cond) args).
+        { destruct (eval_condition cond rs ## args m) as [b0 | ].
+          2: discriminate.
+          inv H0.
+          cbn in COND_PRESENT_FALSE.
+          intuition.
+          inv H0.
+          inv FIND_COND.
+          destruct b; trivial; cbn in H2; discriminate.
+        }
+        rewrite <- subst_args_ok with (invariants := (fst (preanalysis tenv f))) (ctx := (context_from_hints (snd (preanalysis tenv f)))) (pc := pc) (sp:=sp) (m:=m) in COND_PRESENT_TRUE.
+        admit.
+        unfold fmap_sem.
+        change RB.t with (option RELATION.t).
+        rewrite FIND_REL.
+        exact REL.
+   + econstructor; split.        
+      * eapply exec_Icond with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption.
+        ** TR_AT. unfold transf_instr. rewrite FIND_COND.
+           reflexivity.
+        ** rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial.
+           eassumption.
+        ** reflexivity.
+     * econstructor; eauto.
+       destruct b; IND_STEP.
       
   - (* Ijumptable *)
     econstructor. split.