diff options
-rw-r--r-- | src/hls/Abstr.v | 11 | ||||
-rw-r--r-- | src/hls/GiblePargenproof.v | 376 |
2 files changed, 344 insertions, 43 deletions
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index 5ce7c0a..f67627d 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -1500,3 +1500,14 @@ Proof. unfold forest_preds, set_forest_p, get_forest_p'. rewrite PTree.gss; auto. Qed. + +Lemma forest_pred_gss2 : + forall (f : forest) r p, + (forest_preds (f #p r <- p)) ! r = Some p. +Proof. intros. unfold set_forest_p. simpl. now rewrite PTree.gss. Qed. + +Lemma forest_pred_gso2 : + forall (f : forest) r w p, + r <> w -> + (forest_preds (f #p w <- p)) ! r = (forest_preds f) ! r. +Proof. intros. unfold set_forest_p. simpl. now rewrite PTree.gso by auto. Qed. diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index 8c3d77f..e531fd3 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -66,6 +66,12 @@ Definition evaluable {A} (ctx: @ctx A) p := exists b, sem_pexpr ctx p b. Definition all_evaluable {A B} (ctx: @ctx A) f_p (l: predicated B) := forall p y, NE.In (p, y) l -> evaluable ctx (from_pred_op f_p p). +Definition pred_forest_evaluable {A} (ctx: @ctx A) (ps: PTree.t pred_pexpr) := + forall i p, ps ! i = Some p -> evaluable ctx p. + +Definition forest_evaluable {A} (ctx: @ctx A) (f: forest) := + pred_forest_evaluable ctx f.(forest_preds). + Lemma all_evaluable_cons : forall A B pr ctx b a, all_evaluable ctx pr (NE.cons a b) -> @@ -85,6 +91,16 @@ Proof. eapply H. constructor; eauto. Qed. +Lemma all_evaluable_cons3 : + forall A B pr ctx b p a, + all_evaluable ctx pr b -> + evaluable ctx (from_pred_op pr p) -> + @all_evaluable A B ctx pr (NE.cons (p, a) b). +Proof. + unfold all_evaluable; intros. inv H1. inv H3. inv H1. auto. + eauto. +Qed. + Lemma all_evaluable_singleton : forall A B pr ctx b p, @all_evaluable A B ctx pr (NE.singleton (p, b)) -> @@ -93,6 +109,29 @@ Proof. unfold all_evaluable; intros. eapply H. constructor. Qed. +Lemma get_forest_p_evaluable : + forall A (ctx: @ctx A) f r, + forest_evaluable ctx f -> + evaluable ctx (f #p r). +Proof. + intros. unfold "#p", get_forest_p'. + destruct_match. unfold forest_evaluable in *. + unfold pred_forest_evaluable in *. eauto. + unfold evaluable. eexists. constructor. constructor. +Qed. + +Lemma set_forest_p_evaluable : + forall A (ctx: @ctx A) f r p, + forest_evaluable ctx f -> + evaluable ctx p -> + forest_evaluable ctx (f #p r <- p). +Proof. + unfold forest_evaluable, pred_forest_evaluable; intros. + destruct (peq i r); subst. + - rewrite forest_pred_gss2 in H1. now inv H1. + - rewrite forest_pred_gso2 in H1 by auto; eauto. +Qed. + Inductive state_lessdef : instr_state -> instr_state -> Prop := state_lessdef_intro : forall rs1 rs2 ps1 ps2 m1, @@ -769,12 +808,6 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. | nil => Enil end. - Lemma sem_pred_expr_merge : - forall G (ctx: @Abstr.ctx G) args ps l, - Forall2 (sem_pred_expr ps sem_ident ctx) args l -> - sem_pred_expr ps sem_ident ctx (merge args) (to_elist l). - Proof. Admitted. - Lemma sem_val_list_elist : forall G (ctx: @Abstr.ctx G) l j, sem_val_list ctx (to_elist l) j -> @@ -872,11 +905,17 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. Lemma sem_pred_expr_seq_app : forall G A B (f: predicated (A -> B)) - ps (ctx: @ctx G) l f_ l_, + ps (ctx: @ctx G) l f_ l_ + (EVALUABLE: all_evaluable ctx ps l), sem_pred_expr ps sem_ident ctx l l_ -> sem_pred_expr ps sem_ident ctx f f_ -> sem_pred_expr ps sem_ident ctx (seq_app f l) (f_ l_). - Proof. Admitted. + Proof. + unfold seq_app; intros. + remember (fun x : (A -> B) * A => fst x (snd x)) as app. + replace (f_ l_) with (app (f_, l_)) by (rewrite Heqapp; auto). + eapply sem_pred_expr_predicated_map. eapply sem_pred_expr_predicated_prod; auto. + Qed. Lemma sem_pred_expr_map : forall A B C (ctx: @ctx A) ps (f: B -> C) y v, @@ -917,7 +956,8 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. Lemma sem_pred_expr_seq_app_val : forall G A B V (s: @Abstr.ctx G -> B -> V -> Prop) (f: predicated (A -> B)) - ps ctx l v f_ l_, + ps ctx l v f_ l_ + (EVALUABLE: all_evaluable ctx ps l), sem_pred_expr ps sem_ident ctx l l_ -> sem_pred_expr ps sem_ident ctx f f_ -> s ctx (f_ l_) v -> @@ -1038,6 +1078,15 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. cbn. f_equal. eauto. Qed. + Lemma sem_pred_expr_merge : + forall G (ctx: @Abstr.ctx G) ps l args, + Forall2 (sem_pred_expr ps sem_ident ctx) args l -> + sem_pred_expr ps sem_ident ctx (merge args) (to_elist l). + Proof. + induction l; intros. + - inv H. cbn; repeat constructor. + - inv H. cbn. unfold merge. Admitted. + Lemma sem_pred_expr_merge2 : forall A (ctx: @ctx A) pr l l', sem_pred_expr pr sem_ident ctx (merge l) l' -> @@ -1125,38 +1174,267 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. cbn; constructor; auto. Qed. +Lemma evaluable_and_true : + forall G (ctx: @ctx G) ps p, + evaluable ctx (from_pred_op ps p) -> + evaluable ctx (from_pred_op ps (p ∧ T)). +Proof. + intros. unfold evaluable in *. inv H. exists (x && true). cbn. + constructor; auto. constructor. +Qed. + +Lemma NEin_map : + forall A B p y (f: A -> B) a, + NE.In (p, y) (predicated_map f a) -> + exists x, NE.In (p, x) a /\ y = f x. +Proof. + induction a; intros. + - inv H. destruct a. econstructor. split; eauto. constructor. + - inv H. inv H1. inv H. destruct a. cbn in *. econstructor; econstructor; eauto. + constructor; tauto. + specialize (IHa H). inv IHa. inv H0. + econstructor; econstructor; eauto. constructor; tauto. +Qed. + +Lemma NEin_map2 : + forall A B (f: A -> B) a p y, + NE.In (p, y) a -> + NE.In (p, f y) (predicated_map f a). +Proof. + induction a; crush. + inv H. constructor. + inv H. inv H1. + - constructor; auto. + - constructor; eauto. +Qed. + +Lemma all_evaluable_predicated_map : + forall A B G (ctx: @ctx G) ps (f: A -> B) p, + all_evaluable ctx ps p -> + all_evaluable ctx ps (predicated_map f p). +Proof. + induction p. + - unfold all_evaluable; intros. + exploit NEin_map; eauto; intros. inv H1. inv H2. + eapply H; eauto. + - intros. cbn. + eapply all_evaluable_cons3. eapply IHp. eapply all_evaluable_cons; eauto. + cbn. destruct a. cbn in *. eapply all_evaluable_cons2; eauto. +Qed. + +Lemma all_evaluable_predicated_map2 : + forall A B G (ctx: @ctx G) ps (f: A -> B) p, + all_evaluable ctx ps (predicated_map f p) -> + all_evaluable ctx ps p. +Proof. + induction p. + - unfold all_evaluable in *; intros. + eapply H. eapply NEin_map2; eauto. + - intros. cbn. destruct a. + cbn in H. pose proof H. eapply all_evaluable_cons in H; eauto. + eapply all_evaluable_cons2 in H0; eauto. + unfold all_evaluable. specialize (IHp H). + unfold all_evaluable in IHp. + intros. inv H1. inv H3. inv H1; eauto. + specialize (IHp _ _ H1). eauto. +Qed. + +Lemma all_evaluable_map_and : + forall A B G (ctx: @ctx G) ps (a: NE.non_empty ((pred_op * A) * (pred_op * B))), + (forall p1 x p2 y, + NE.In ((p1, x), (p2, y)) a -> + evaluable ctx (from_pred_op ps p1) + /\ evaluable ctx (from_pred_op ps p2)) -> + all_evaluable ctx ps (NE.map (fun x => match x with ((a, b), (c, d)) => (Pand a c, (b, d)) end) a). +Proof. + induction a. + - intros. cbn. repeat destruct_match. inv Heqp. + unfold all_evaluable; intros. inv H0. + unfold evaluable. + exploit H. constructor. + intros [Ha Hb]. inv Ha. inv Hb. + exists (x && x0). constructor; auto. + - intros. unfold all_evaluable; cbn; intros. inv H0. inv H2. + + repeat destruct_match. inv Heqp0. inv H0. + specialize (H p2 a1 p3 b ltac:(constructor; eauto)). + inv H. inv H0. inv H1. exists (x && x0). + constructor; eauto. + + eapply IHa; intros. eapply H. econstructor. right. eauto. + eauto. +Qed. + +Lemma all_evaluable_map_add : + forall A B G (ctx: @ctx G) ps (a: pred_op * A) (b: predicated B) p1 x p2 y, + evaluable ctx (from_pred_op ps (fst a)) -> + all_evaluable ctx ps b -> + NE.In (p1, x, (p2, y)) (NE.map (fun x : pred_op * B => (a, x)) b) -> + evaluable ctx (from_pred_op ps p1) /\ evaluable ctx (from_pred_op ps p2). +Proof. + induction b; intros. + - cbn in *. inv H1. unfold all_evaluable in *. specialize (H0 _ _ ltac:(constructor)). + auto. + - cbn in *. inv H1. inv H3. + + inv H1. unfold all_evaluable in H0. specialize (H0 _ _ ltac:(constructor; eauto)); auto. + + eapply all_evaluable_cons in H0. specialize (IHb _ _ _ _ H H0 H1). auto. +Qed. + +Lemma NEin_NEapp5 : + forall A (a: A) x y, + NE.In a (NE.app x y) -> + NE.In a x \/ NE.In a y. +Proof. + induction x; crush. + - inv H. inv H1. left. constructor. tauto. + - inv H. inv H1. left. constructor; tauto. + exploit IHx; eauto; intros. inv H0. + left. constructor; tauto. tauto. +Qed. + +Lemma all_evaluable_non_empty_prod : + forall A B G (ctx: @ctx G) ps p1 x p2 y (a: predicated A) (b: predicated B), + all_evaluable ctx ps a -> + all_evaluable ctx ps b -> + NE.In ((p1, x), (p2, y)) (NE.non_empty_prod a b) -> + evaluable ctx (from_pred_op ps p1) + /\ evaluable ctx (from_pred_op ps p2). +Proof. + induction a; intros. + - cbn in *. eapply all_evaluable_map_add; eauto. destruct a; cbn in *. eapply H; constructor. + - cbn in *. eapply NEin_NEapp5 in H1. inv H1. eapply all_evaluable_map_add; eauto. + destruct a; cbn in *. eapply all_evaluable_cons2; eauto. + eapply all_evaluable_cons in H. eauto. +Qed. + +Lemma all_evaluable_predicated_prod : + forall A B G (ctx: @ctx G) ps (a: predicated A) (b: predicated B), + all_evaluable ctx ps a -> + all_evaluable ctx ps b -> + all_evaluable ctx ps (predicated_prod a b). +Proof. + intros. unfold all_evaluable; intros. + unfold predicated_prod in *. exploit all_evaluable_map_and; eauto. + intros. eapply all_evaluable_non_empty_prod. 3: { eauto. } + eauto. eauto. +Qed. + +Lemma cons_pred_expr_evaluable : + forall G (ctx: @ctx G) ps a b, + all_evaluable ctx ps a -> + all_evaluable ctx ps b -> + all_evaluable ctx ps (cons_pred_expr a b). +Proof. + unfold cons_pred_expr; intros. + apply all_evaluable_predicated_map. + now apply all_evaluable_predicated_prod. +Qed. + +Lemma fold_right_all_evaluable : + forall G (ctx: @ctx G) ps n, + Forall (all_evaluable ctx ps) (NE.to_list n) -> + all_evaluable ctx ps (NE.fold_right cons_pred_expr (NE.singleton (T, Enil)) n). +Proof. + induction n; cbn in *; intros. + - unfold cons_pred_expr. eapply all_evaluable_predicated_map. eapply all_evaluable_predicated_prod. + inv H. auto. unfold all_evaluable; intros. inv H0. exists true. constructor. + - inv H. specialize (IHn H3). now eapply cons_pred_expr_evaluable. +Qed. + +Lemma evaluable_negate : + forall G (ctx: @ctx G) p, + evaluable ctx p -> + evaluable ctx (¬ p). +Proof. + induction p; intros. + - destruct p. cbn in *. inv H. + exists (negb x). constructor. inv H0. + rewrite negb_if. now rewrite negb_involutive. + - repeat econstructor. + - repeat econstructor. + - cbn. exploit IHp1. inv H. inv H0. econstructor. eauto. + intros. exploit IHp2. inv H. inv H1. econstructor. eauto. + intros. inv H0. inv H1. econstructor. econstructor; eauto. + - cbn. exploit IHp1. inv H. inv H0. econstructor. eauto. + intros. exploit IHp2. inv H. inv H1. econstructor. eauto. + intros. inv H0. inv H1. econstructor. econstructor; eauto. +Qed. + +Lemma predicated_evaluable : + forall G (ctx: @ctx G) ps (p: pred_op), + pred_forest_evaluable ctx ps -> + evaluable ctx (from_pred_op ps p). +Proof. + unfold pred_forest_evaluable; intros. induction p; intros; cbn. + - repeat destruct_match; subst; unfold get_forest_p'. + destruct_match. eapply H; eauto. econstructor. constructor. constructor. + eapply evaluable_negate. + destruct_match. eapply H; eauto. econstructor. constructor. constructor. + - repeat econstructor. + - repeat econstructor. + - inv IHp1. inv IHp2. econstructor. constructor; eauto. + - inv IHp1. inv IHp2. econstructor. constructor; eauto. +Qed. + +Lemma predicated_evaluable_all : + forall A G (ctx: @ctx G) ps (p: predicated A), + pred_forest_evaluable ctx ps -> + all_evaluable ctx ps p. +Proof. + unfold all_evaluable; intros. + eapply predicated_evaluable. eauto. +Qed. + +Lemma merge_all_evaluable : + forall G (ctx: @ctx G) ps, + pred_forest_evaluable ctx ps -> + forall f args, + all_evaluable ctx ps (merge (list_translation args f)). +Proof. + intros. eapply predicated_evaluable_all. eauto. +Qed. + +(*| +Here we can finally assume that everything in the forest is evaluable, which +will allow us to prove that translating the list of register accesses will also +all be evaluable. +|*) + Lemma sem_update_Iop : - forall A op rs args m v f ps ctx, + forall A op rs args m v f ps ctx + (EVALF: forest_evaluable ctx f), Op.eval_operation (ctx_ge ctx) (ctx_sp ctx) op rs ## args (is_mem (ctx_is ctx)) = Some v -> sem ctx f ((mk_instr_state rs ps m), None) -> @sem_pred_expr A _ _ (forest_preds f) sem_value ctx (seq_app (pred_ret (Eop op)) (merge (list_translation args f))) v. Proof. - intros * EVAL SEM. + intros * EVALF EVAL SEM. exploit sem_pred_expr_list_translation; try eassumption. intro H; inversion_clear H as [x [HS HV]]. eapply sem_pred_expr_seq_app_val. + - eapply merge_all_evaluable; eauto. - cbn in *; eapply sem_pred_expr_merge; eauto. - apply sem_pred_expr_pred_ret. - econstructor; [eauto|]; auto. Qed. Lemma sem_update_Iload : - forall A rs args m v f ps ctx addr a0 chunk, + forall A rs args m v f ps ctx addr a0 chunk + (EVALF: forest_evaluable ctx f), Op.eval_addressing (ctx_ge ctx) (ctx_sp ctx) addr rs ## args = Some a0 -> Mem.loadv chunk m a0 = Some v -> sem ctx f ((mk_instr_state rs ps m), None) -> @sem_pred_expr A _ _ (forest_preds f) sem_value ctx (seq_app (seq_app (pred_ret (Eload chunk addr)) (merge (list_translation args f))) (f #r Mem)) v. Proof. - intros * EVAL MEM SEM. + intros * EVALF EVAL MEM SEM. exploit sem_pred_expr_list_translation; try eassumption. intro H; inversion_clear H as [x [HS HV]]. inversion SEM as [? ? ? ? ? ? REG PRED HMEM EXIT]; subst. exploit sem_pred_expr_ident2; [eapply HMEM|]. intros H; inversion_clear H as [x' [HS' HV']]. eapply sem_pred_expr_seq_app_val; eauto. + { eapply predicated_evaluable_all; eauto. } { eapply sem_pred_expr_seq_app; eauto. + - eapply predicated_evaluable_all; eauto. - eapply sem_pred_expr_merge; eauto. - apply sem_pred_expr_pred_ret. } @@ -1308,7 +1586,8 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. Proof. intros. destruct p; cbn; inv H; auto. Qed. Lemma sem_update_Istore : - forall A rs args m v f ps ctx addr a0 chunk m' v', + forall A rs args m v f ps ctx addr a0 chunk m' v' + (EVALF: forest_evaluable ctx f), Op.eval_addressing (ctx_ge ctx) (ctx_sp ctx) addr rs ## args = Some a0 -> Mem.storev chunk m a0 v' = Some m' -> sem_value ctx v v' -> @@ -1316,24 +1595,26 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. @sem_pred_expr A _ _ (forest_preds f) sem_mem ctx (seq_app (seq_app (pred_ret (Estore v chunk addr)) (merge (list_translation args f))) (f #r Mem)) m'. - Proof. Admitted. - (* intros * EVAL MEM SEM. *) - (* exploit sem_pred_expr_list_translation; try eassumption. *) - (* intro H; inversion_clear H as [x [HS HV]]. *) - (* inversion SEM as [? ? ? ? ? ? REG PRED HMEM EXIT]; subst. *) - (* exploit sem_pred_expr_ident2; [eapply HMEM|]. *) - (* intros H; inversion_clear H as [x' [HS' HV']]. *) - (* eapply sem_pred_expr_seq_app; eauto. *) - (* { eapply sem_pred_expr_seq_app; eauto. *) - (* - eapply sem_pred_expr_merge; eauto. *) - (* - apply sem_pred_expr_pred_ret. *) - (* - constructor. *) - (* } *) - (* econstructor; eauto. *) - (* Qed. *) + Proof. + intros * EVALF EVAL STOREV SEMVAL SEM. + exploit sem_merge_list; try eassumption. + intro MERGE. exploit sem_pred_expr_ident2; eauto. + intro TMP; inversion_clear TMP as [x [HS HV]]. + inversion_clear SEM as [? ? ? ? ? ? REG PRED HMEM EXIT]. + exploit sem_pred_expr_ident2; [eapply HMEM|]. + intros TMP; inversion_clear TMP as [x' [HS' HV']]. + eapply sem_pred_expr_ident. + eapply sem_pred_expr_seq_app; eauto. + eapply predicated_evaluable_all; eauto. + eapply sem_pred_expr_seq_app; eauto. + eapply predicated_evaluable_all; eauto. + eapply sem_pred_expr_pred_ret. + econstructor; eauto. + Qed. Lemma sem_update_Iop_top: - forall A f p p' f' rs m pr op res args p0 v state, + forall A f p p' f' rs m pr op res args p0 v state + (EVALF: forest_evaluable state f), Op.eval_operation (ctx_ge state) (ctx_sp state) op rs ## args m = Some v -> truthy pr p0 -> valid_mem (is_mem (ctx_is state)) m -> @@ -1342,7 +1623,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. eval_predf pr p = true -> @sem A state f' (mk_instr_state (rs # res <- v) pr m, None). Proof. - intros * EVAL_OP TRUTHY VALID SEM UPD EVAL_PRED. + intros * EVALF EVAL_OP TRUTHY VALID SEM UPD EVAL_PRED. pose proof SEM as SEM2. inversion UPD as [PRUNE]. unfold Option.bind in PRUNE. destr. inversion_clear PRUNE. @@ -1370,7 +1651,8 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. Qed. Lemma sem_update_Iload_top: - forall A f p p' f' rs m pr res args p0 v state addr a chunk, + forall A f p p' f' rs m pr res args p0 v state addr a chunk + (EVALF: forest_evaluable state f), Op.eval_addressing (ctx_ge state) (ctx_sp state) addr rs ## args = Some a -> Mem.loadv chunk m a = Some v -> truthy pr p0 -> @@ -1380,7 +1662,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. eval_predf pr p = true -> @sem A state f' (mk_instr_state (rs # res <- v) pr m, None). Proof. - intros * EVAL_OP LOAD TRUTHY VALID SEM UPD EVAL_PRED. + intros * EVALF EVAL_OP LOAD TRUTHY VALID SEM UPD EVAL_PRED. pose proof SEM as SEM2. inversion UPD as [PRUNE]. unfold Option.bind in PRUNE. destr. inversion_clear PRUNE. @@ -1420,7 +1702,8 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. Qed. Lemma sem_update_Istore_top: - forall A f p p' f' rs m pr res args p0 state addr a chunk m', + forall A f p p' f' rs m pr res args p0 state addr a chunk m' + (EVALF: forest_evaluable state f), Op.eval_addressing (ctx_ge state) (ctx_sp state) addr rs ## args = Some a -> Mem.storev chunk m a rs !! res = Some m' -> truthy pr p0 -> @@ -1430,7 +1713,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. eval_predf pr p = true -> @sem A state f' (mk_instr_state rs pr m', None). Proof. - intros * EVAL_OP STORE TRUTHY VALID SEM UPD EVAL_PRED. + intros * EVALF EVAL_OP STORE TRUTHY VALID SEM UPD EVAL_PRED. pose proof SEM as SEM2. inversion UPD as [PRUNE]. unfold Option.bind in PRUNE. destr. inversion_clear PRUNE. @@ -1443,22 +1726,29 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. rewrite forest_reg_gss. exploit sem_pred_expr_ident2; [exact MEM|]; intro HSEM_; inversion_clear HSEM_ as [x [HSEM1 HSEM2]]. - inv REG. specialize (H res). apply exists_sem_pred in H. inversion_clear H as [r' [HNE HVAL]]. + inv REG. specialize (H res). + pose proof H as HRES. + eapply sem_pred_expr_ident2 in HRES. + inversion_clear HRES as [r2 [HRES1 HRES2]]. + apply exists_sem_pred in H. inversion_clear H as [r' [HNE HVAL]]. + exploit sem_merge_list. eauto. instantiate (2 := args). intro HSPE. eapply sem_pred_expr_ident2 in HSPE. + inversion_clear HSPE as [l_ [HSPE1 HSPE2]]. eapply sem_pred_expr_prune_predicated; eauto. eapply sem_pred_expr_app_predicated. - eapply sem_pred_expr_seq_app_val; [solve [eauto]| |]. - eapply sem_pred_expr_seq_app. admit. + eapply sem_pred_expr_seq_app_val; [solve [eapply predicated_evaluable_all; eauto]|solve [eauto]| |]. + eapply sem_pred_expr_seq_app; [solve [eapply predicated_evaluable_all; eauto]|solve [eauto]|]. eapply sem_pred_expr_flap2. - eapply sem_pred_expr_seq_app. admit. + eapply sem_pred_expr_seq_app; [solve [eapply predicated_evaluable_all; eauto]|solve [eauto]|]. eapply sem_pred_expr_pred_ret. econstructor. eauto. 3: { eauto. } - eauto. admit. eauto. inv PRED. eauto. + eauto. auto. eauto. inv PRED. eauto. rewrite eval_predf_Pand. rewrite EVAL_PRED. rewrite truthy_dflt. auto. auto. + auto. - Admitted. + Qed. Lemma sem_update_instr : - forall f i' i'' a sp p i p' f', + forall f i' i'' a sp p i p' f' + (EVALF: forest_evaluable (mk_ctx i sp ge) f), step_instr ge sp (Iexec i') a (Iexec i'') -> valid_mem (is_mem i) (is_mem i') -> sem (mk_ctx i sp ge) f (i', None) -> @@ -1466,7 +1756,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. eval_predf (is_ps i') p = true -> sem (mk_ctx i sp ge) f' (i'', None). Proof. - inversion 1; subst; clear H; intros VALID SEM UPD EVAL_PRED; pose proof SEM as SEM2. + inversion 2; subst; clear H; intros VALID SEM UPD EVAL_PRED; pose proof SEM as SEM2. - inv UPD; auto. - eauto using sem_update_Iop_top. - eauto using sem_update_Iload_top. |