not yet the transfer functions that record predicates

1 files changed, 54 insertions, 7 deletions

diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 215f5c41..7af62b95 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -771,7 +771,28 @@ Proof.
         TR_AT. unfold transf_instr. rewrite FIND_COND. reflexivity.
       * replace bfound with b.
         { econstructor; eauto.
-          admit.
+          assert (is_inductive_allstep (ctx:= (context_from_hints (snd (preanalysis tenv f)))) f tenv (fst  (preanalysis tenv f))) as IND by
+        (apply checked_is_inductive_allstep;
+         eapply transf_function_invariants_inductive; eassumption).
+         unfold is_inductive_allstep, is_inductive_step, apply_instr' in IND.
+         specialize IND with (pc:=pc) (pc':= if b then ifso else ifnot) (instr:= (Icond cond args ifso ifnot predb)).
+         cbn in IND.
+         rewrite H in IND.
+         assert (RB.ge (fst (preanalysis tenv f)) # (if b then ifso else ifnot)
+          match (fst (preanalysis tenv f)) # pc with
+          | Some x => apply_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc tenv (Icond cond args ifso ifnot predb) x
+          | None => None
+          end) as INDUCTIVE by (destruct b; intuition).
+         clear IND.
+
+         change node with positive.
+
+         destruct ((fst (preanalysis tenv f)) # pc).
+         2: exfalso; exact REL.
+         
+         destruct ((fst (preanalysis tenv f)) # (if b then ifso else ifnot)).
+          - eapply rel_ge. exact INDUCTIVE. exact REL.
+          - cbn in INDUCTIVE. exfalso. exact INDUCTIVE.
         }
         unfold find_cond_in_fmap in FIND_COND.
         change RB.t with (option RELATION.t) in REL.
@@ -796,12 +817,38 @@ Proof.
           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.
+        clear COND_PRESENT_TRUE COND_PRESENT_FALSE.
+        pose proof (is_condition_present_sound pc rel cond (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) rs m REL) as COND_PRESENT_TRUE.
+        pose proof (is_condition_present_sound pc rel (negate_condition cond) (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) rs m REL) as COND_PRESENT_FALSE.
+        rewrite eval_negate_condition in COND_PRESENT_FALSE.
+        
+        destruct is_condition_present.
+        { rewrite subst_args_ok with (sp:=sp) (m:=m) in COND_PRESENT_TRUE.
+          { rewrite COND_PRESENT_TRUE in H0 by trivial.
+            congruence.
+          }
+          unfold fmap_sem.
+          change RB.t with (option RELATION.t).
+          rewrite FIND_REL.
+          exact REL.
+        }
+        destruct is_condition_present.
+        { rewrite subst_args_ok with (sp:=sp) (m:=m) in COND_PRESENT_FALSE.
+          { 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.
+          }
+          unfold fmap_sem.
+          change RB.t with (option RELATION.t).
+          rewrite FIND_REL.
+          exact REL.          
+        }
+        discriminate.
    + 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.