diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/common/NonEmpty.v | 13 | ||||
-rw-r--r-- | src/hls/AbstrSemIdent.v | 20 | ||||
-rw-r--r-- | src/hls/GiblePargen.v | 10 | ||||
-rw-r--r-- | src/hls/GiblePargenproofBackward.v | 557 | ||||
-rw-r--r-- | src/hls/GiblePargenproofForward.v | 6 |
5 files changed, 506 insertions, 100 deletions
diff --git a/src/common/NonEmpty.v b/src/common/NonEmpty.v index 3aff11d..2c3ae94 100644 --- a/src/common/NonEmpty.v +++ b/src/common/NonEmpty.v @@ -292,3 +292,16 @@ Proof. inversion_clear H0 as [x0 [HN1 HN2]]. rewrite HN1 in H. inv H. cbn. f_equal. eauto. Qed. + +Lemma Forall_forall: + forall (A : Type) (P : A -> Prop) (l : non_empty A), Forall P l <-> (forall x : A, In x l -> P x). +Proof. + induction l. + - split; intros. + + inv H. inv H0. auto. + + constructor. specialize (H a). apply H. constructor. + - split; intros. + + inv H. inv H0. inv H1; eauto. eapply IHl in H4; eauto. + + constructor. eapply H. constructor; tauto. eapply IHl. + intros. eapply H. constructor; tauto. +Qed. diff --git a/src/hls/AbstrSemIdent.v b/src/hls/AbstrSemIdent.v index 36c3ffc..5c6b3eb 100644 --- a/src/hls/AbstrSemIdent.v +++ b/src/hls/AbstrSemIdent.v @@ -482,7 +482,7 @@ Lemma sem_pred_expr_flap : sem_pred_expr ps sem_ident ctx f f_ -> sem_pred_expr ps sem_ident ctx (flap f l) (f_ l). Proof. - induction f. unfold flap2; intros. inv H. inv H3. + induction f. unfold flap; intros. inv H. inv H3. constructor; eauto. constructor. intros. inv H. cbn. constructor; eauto. inv H5. constructor. @@ -501,6 +501,12 @@ Proof. eapply sem_pred_expr_cons_false; eauto. Qed. +Lemma sem_pred_expr_flap2_2 : + forall A B C (f: predicated (A -> B -> C)) ps l1 l2 x, + sem_pred_expr ps sem_ident ctx (flap2 f l1 l2) x -> + exists f_, sem_pred_expr ps sem_ident ctx f f_ /\ f_ l1 l2 = x. +Proof. Admitted. + Lemma sem_pred_expr_seq_app_val : forall A B V (s: @Abstr.ctx G -> B -> V -> Prop) (f: predicated (A -> B)) @@ -663,4 +669,16 @@ Proof. cbn; constructor; auto. Qed. +Lemma from_predicated_sem_pred_expr : + forall preds pe b, + sem_pred_expr preds sem_pred ctx pe b -> + sem_pexpr ctx (from_predicated true preds pe) b. +Proof. Admitted. + +Lemma from_predicated_sem_pred_expr2 : + forall preds pe b, + sem_pexpr ctx (from_predicated true preds pe) b -> + sem_pred_expr preds sem_pred ctx pe b. +Proof. Admitted. + End PROOF. diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index 08806aa..91b0450 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -279,16 +279,6 @@ Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest Some (new_p, f <-e pruned) end. -Definition remember_expr (f : forest) (lst: list pred_expr) (i : instr): list pred_expr := - match i with - | RBnop => lst - | RBop p op rl r => (f #r (Reg r)) :: lst - | RBload p chunk addr rl r => (f #r (Reg r)) :: lst - | RBstore p chunk addr rl r => (f #r Mem) :: lst - | RBsetpred p' c args p => lst - | RBexit p c => lst - end. - (*Compute match update (T, mk_forest (PTree.empty _) (PTree.empty _) (NE.singleton (T, EEbase))) (RBop None Op.Odiv (1::2::nil) 3) with | Some x => diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v index b6e79a1..911cd9b 100644 --- a/src/hls/GiblePargenproofBackward.v +++ b/src/hls/GiblePargenproofBackward.v @@ -89,13 +89,55 @@ Lemma sem_exists_execution : exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf). Proof. Admitted. *) -Definition update' (s: pred_op * forest * list pred_expr) (i: instr): option (pred_op * forest * list pred_expr) := - let '(p, f, l) := s in - Option.bind2 (fun p' f' => Option.ret (p', f', remember_expr f l i)) (update (p, f) i). +Definition remember_expr (f : forest) (lst: list pred_expr) (i : instr): list pred_expr := + match i with + | RBnop => lst + | RBop p op rl r => (f #r (Reg r)) :: lst + | RBload p chunk addr rl r => (f #r (Reg r)) :: lst + | RBstore p chunk addr rl r => lst + | RBsetpred p' c args p => lst + | RBexit p c => lst + end. -Definition abstract_sequence' (b : list instr) : option (forest * list pred_expr) := - Option.map (fun x => let '(_, y, z) := x in (y, z)) - (mfold_left update' b (Some (Ptrue, empty, nil))). +Definition remember_expr_m (f : forest) (lst: list pred_expr) (i : instr): list pred_expr := + match i with + | RBnop => lst + | RBop p op rl r => lst + | RBload p chunk addr rl r => lst + | RBstore p chunk addr rl r => (f #r Mem) :: lst + | RBsetpred p' c args p => lst + | RBexit p c => lst + end. + +Definition update' (s: pred_op * forest * list pred_expr * list pred_expr) (i: instr): option (pred_op * forest * list pred_expr * list pred_expr) := + let '(p, f, l, lm) := s in + Option.bind2 (fun p' f' => Option.ret (p', f', remember_expr f l i, remember_expr_m f lm i)) (update (p, f) i). + +Definition gather_predicates (preds : PTree.t unit) (i : instr): option (PTree.t unit) := + match i with + | RBop (Some p) _ _ _ + | RBload (Some p) _ _ _ _ + | RBstore (Some p) _ _ _ _ + | RBexit (Some p) _ => + Some (fold_right (fun x => PTree.set x tt) preds (predicate_use p)) + | RBsetpred p' c args p => + let preds' := match p' with + | Some p'' => fold_right (fun x => PTree.set x tt) preds (predicate_use p'') + | None => preds + end + in + match preds' ! p with + | Some _ => None + | None => Some preds' + end + | _ => Some preds + end. + +Definition abstract_sequence' (b : list instr) : option (forest * list pred_expr * list pred_expr) := + Option.bind (fun x => Option.bind (fun _ => Some x) + (mfold_left gather_predicates b (Some (PTree.empty _)))) + (Option.map (fun x => let '(_, y, z, zm) := x in (y, z, zm)) + (mfold_left update' b (Some (Ptrue, empty, nil, nil)))). Definition i_state (s: istate): instr_state := match s with @@ -110,14 +152,21 @@ Definition cf_state (s: istate): option cf_instr := end. Definition evaluable_pred_expr {G} (ctx: @Abstr.ctx G) pr p := - exists r, - sem_pred_expr pr sem_value ctx p r. + exists r, sem_pred_expr pr sem_value ctx p r. + +Definition evaluable_pred_expr_m {G} (ctx: @Abstr.ctx G) pr p := + exists r, sem_pred_expr pr sem_mem ctx p r. Definition evaluable_pred_list {G} ctx pr l := forall p, In p l -> @evaluable_pred_expr G ctx pr p. +Definition evaluable_pred_list_m {G} ctx pr l := + forall p, + In p l -> + @evaluable_pred_expr_m G ctx pr p. + (* Lemma evaluable_pred_expr_exists : *) (* forall sp pr f i0 exit_p exit_p' f' cf i ti p op args dst, *) (* update (exit_p, f) (RBop p op args dst) = Some (exit_p', f') -> *) @@ -130,7 +179,7 @@ Definition evaluable_pred_list {G} ctx pr l := (* destruct ti. econstructor. econstructor. *) (* unfold evaluable_pred_expr in H1. Admitted. *) -Lemma evaluable_pred_expr_exists : +Lemma evaluable_pred_expr_exists_RBop : forall sp f i0 exit_p exit_p' f' i ti p op args dst, eval_predf (is_ps i) exit_p = true -> valid_mem (is_mem i0) (is_mem i) -> @@ -186,6 +235,209 @@ Proof. now erewrite <- eval_predf_pr_equiv by exact H0. Qed. +Lemma evaluable_pred_expr_exists_RBload : + forall sp f i0 exit_p exit_p' f' i ti p chunk addr args dst, + eval_predf (is_ps i) exit_p = true -> + valid_mem (is_mem i0) (is_mem i) -> + update (exit_p, f) (RBload p chunk addr args dst) = Some (exit_p', f') -> + sem (mk_ctx i0 sp ge) f (i, None) -> + evaluable_pred_expr (mk_ctx i0 sp ge) f'.(forest_preds) (f' #r (Reg dst)) -> + state_lessdef i ti -> + exists ti', + step_instr ge sp (Iexec ti) (RBload p chunk addr args dst) (Iexec ti'). +Proof. + intros * HEVAL VALID_MEM **. cbn -[seq_app] in H. unfold Option.bind in H. destr. inv H. + assert (HPRED': sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f (is_ps i)) + by now inv H0. + inversion_clear HPRED' as [? ? ? HPRED]. + destruct ti as [is_trs is_tps is_tm]. + unfold evaluable_pred_expr in H1. destruct H1 as (r & Heval). + rewrite forest_reg_gss in Heval. + exploit sem_pred_expr_prune_predicated2; eauto; intros. + pose proof (truthy_dec (is_ps i) p) as YH. inversion_clear YH as [YH'|YH']. + - assert (eval_predf (is_ps i) (dfltp p ∧ exit_p') = true). + { pose proof (truthy_dflt _ _ YH'). rewrite eval_predf_Pand. + rewrite H1. now rewrite HEVAL. } + exploit sem_pred_expr_app_predicated2; eauto; intros. + exploit sem_pred_expr_seq_app_val2; eauto; simplify. + exploit sem_pred_expr_seq_app_val2; eauto; simplify. + unfold pred_ret in *. inv H6. inv H15. clear H13. inv H10. + destruct i as [is_rs_1 is_ps_1 is_m_1]. exploit sem_merge_list; eauto; intros. + instantiate (1 := args) in H6. + eapply sem_pred_expr_ident2 in H6. simplify. + exploit sem_pred_expr_ident_det. eapply H8. eapply H6. + intros. subst. inv H7. + eapply sem_val_list_det in H10; eauto; [|reflexivity]. subst. + cbn in *. inv H2. + econstructor. econstructor; eauto. + + erewrite <- match_states_list; eauto. + + inv H0. exploit sem_pred_expr_ident. eapply H5. eapply H15. intros. + eapply sem_pred_expr_det in H0. rewrite H0. eassumption. + reflexivity. eapply sem_mem_det. reflexivity. auto. + + inv H0. + assert (sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f (is_ps_1)) + by (now constructor). + pose proof (sem_predset_det _ _ ltac:(reflexivity) _ _ _ H0 H20). + assert (truthy is_ps_1 p). + { eapply truthy_match_state; eassumption. } + eapply truthy_match_state; eassumption. + - inv YH'. cbn -[seq_app] in H. + assert (eval_predf (is_ps i) (p0 ∧ exit_p') = false). + { rewrite eval_predf_Pand. now rewrite H1. } + eapply sem_pred_expr_app_predicated_false2 in H; eauto. + eexists. eapply exec_RB_falsy. constructor. auto. cbn. + assert (sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f (is_ps i)) + by (now constructor). + inv H0. pose proof (sem_predset_det _ _ ltac:(reflexivity) _ _ _ H4 H8). + inv H2. + erewrite <- eval_predf_pr_equiv by exact H16. + now erewrite <- eval_predf_pr_equiv by exact H0. +Qed. + +Lemma evaluable_pred_expr_exists_RBstore : + forall sp f i0 exit_p exit_p' f' i ti p chunk addr args src, + eval_predf (is_ps i) exit_p = true -> + valid_mem (is_mem i0) (is_mem i) -> + update (exit_p, f) (RBstore p chunk addr args src) = Some (exit_p', f') -> + sem (mk_ctx i0 sp ge) f (i, None) -> + evaluable_pred_expr_m (mk_ctx i0 sp ge) f'.(forest_preds) (f' #r Mem) -> + state_lessdef i ti -> + exists ti', + step_instr ge sp (Iexec ti) (RBstore p chunk addr args src) (Iexec ti'). +Proof. + intros * HEVAL VALID_MEM **. cbn -[seq_app] in H. unfold Option.bind in H. destr. inv H. + assert (HPRED': sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f (is_ps i)) + by now inv H0. + inversion_clear HPRED' as [? ? ? HPRED]. + destruct ti as [is_trs is_tps is_tm]. + unfold evaluable_pred_expr in H1. destruct H1 as (r & Heval). + rewrite forest_reg_gss in Heval. + exploit sem_pred_expr_prune_predicated2; eauto; intros. + pose proof (truthy_dec (is_ps i) p) as YH. inversion_clear YH as [YH'|YH']. + - assert (eval_predf (is_ps i) (dfltp p ∧ exit_p') = true). + { pose proof (truthy_dflt _ _ YH'). rewrite eval_predf_Pand. + rewrite H1. now rewrite HEVAL. } + exploit sem_pred_expr_app_predicated2; eauto; intros. + exploit sem_pred_expr_seq_app_val2; eauto; simplify. + exploit sem_pred_expr_seq_app_val2; eauto; simplify. + exploit sem_pred_expr_flap2_2; eauto; simplify. + exploit sem_pred_expr_seq_app_val2; eauto; simplify. + unfold pred_ret in *. inv H14. inv H11. inv H18. clear H16. inv H10. inv H7. + destruct i as [is_rs_1 is_ps_1 is_m_1]. exploit sem_merge_list; eauto; intros. + instantiate (1 := args) in H7. + eapply sem_pred_expr_ident2 in H7. simplify. + exploit sem_pred_expr_ident_det. eapply H8. eapply H7. + intros. subst. + eapply sem_val_list_det in H20; eauto; [|reflexivity]. subst. + cbn in *. inv H2. inv H0. inv H20. pose proof H0 as YH0. specialize (YH0 src). + exploit sem_pred_expr_ident. eapply H5. eauto. intros. + exploit sem_pred_expr_ident. eapply H12. eauto. intros. + eapply sem_pred_expr_det in H25; eauto; [|reflexivity|eapply sem_mem_det; reflexivity]. + eapply sem_pred_expr_det in YH0; eauto; [|reflexivity|eapply sem_value_det; reflexivity]. + subst. + econstructor. econstructor; eauto. + + erewrite <- match_states_list; eauto. + + rewrite <- H16. eassumption. + + assert (sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f (is_ps_1)) + by (now constructor). + pose proof (sem_predset_det _ _ ltac:(reflexivity) _ _ _ H24 H13). + assert (truthy is_ps_1 p). + { eapply truthy_match_state; eassumption. } + eapply truthy_match_state; eassumption. + - inv YH'. cbn -[seq_app] in H. + assert (eval_predf (is_ps i) (p0 ∧ exit_p') = false). + { rewrite eval_predf_Pand. now rewrite H1. } + eapply sem_pred_expr_app_predicated_false2 in H; eauto. + eexists. eapply exec_RB_falsy. constructor. auto. cbn. + assert (sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f (is_ps i)) + by (now constructor). + inv H0. pose proof (sem_predset_det _ _ ltac:(reflexivity) _ _ _ H4 H8). + inv H2. + erewrite <- eval_predf_pr_equiv by exact H16. + now erewrite <- eval_predf_pr_equiv by exact H0. +Qed. + +Lemma evaluable_pred_expr_exists_RBsetpred : + forall sp f i0 exit_p exit_p' f' i ti p c args src ps', + eval_predf (is_ps i) exit_p = true -> + valid_mem (is_mem i0) (is_mem i) -> + update (exit_p, f) (RBsetpred p c args src) = Some (exit_p', f') -> + sem (mk_ctx i0 sp ge) f (i, None) -> + sem_predset (mk_ctx i0 sp ge) f' ps' -> + state_lessdef i ti -> + exists ti', + step_instr ge sp (Iexec ti) (RBsetpred p c args src) (Iexec ti'). +Proof. + intros * HEVAL VALID_MEM **. cbn -[seq_app] in H. unfold Option.bind in H. destr. inv H. + assert (HPRED': sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f (is_ps i)) + by now inv H0. + inversion_clear HPRED' as [? ? ? HPRED]. + destruct ti as [is_trs is_tps is_tm]. destr. inv H4. inv H1. + pose proof H as YH. specialize (YH src). rewrite forest_pred_gss in YH. + inv YH; try inv H3. + + inv H1. inv H6. replace false with (negb true) in H4 by auto. + replace false with (negb true) in H8 by auto. + eapply sem_pexpr_negate2 in H4. eapply sem_pexpr_negate2 in H8. + destruct i. + exploit from_predicated_sem_pred_expr2; eauto; intros. + exploit sem_pred_expr_seq_app_val2. eapply HPRED. eauto. simplify. + inv H3. inv H15. clear H13. + exploit sem_merge_list; eauto; intros. instantiate (1:=args) in H3. + eapply sem_pred_expr_ident2 in H3; simplify. exploit sem_pred_expr_ident_det. + eapply H6. eauto. intros. subst. + intros. inv H10. eapply sem_val_list_det in H11; eauto. subst. + inv H2. + econstructor. econstructor. erewrite <- match_states_list; eauto. + erewrite <- storev_eval_condition; eauto. + assert (truthy is_ps p). + { destruct p. cbn in H4. constructor. + eapply sem_pexpr_forward_eval; eauto. constructor. + } + eapply truthy_match_state; eassumption. + reflexivity. + + inv H1. inv H6. inv H3. + * replace false with (negb true) in H1 by auto. eapply sem_pexpr_negate2 in H1. + eapply sem_pexpr_forward_eval in H1; eauto. rewrite eval_predf_negate in H1. + assert ((eval_predf (is_ps i) (dfltp p)) = false). + { replace false with (negb true) by auto. rewrite <- H1. now rewrite negb_involutive. } + econstructor. apply exec_RB_falsy. cbn. destruct p. constructor; auto. inv H2. + erewrite <- eval_predf_pr_equiv; eauto. now cbn in H3. + * replace false with (negb true) in H1 by auto. eapply sem_pexpr_negate2 in H1. + eapply sem_pexpr_forward_eval in H1; eauto. rewrite eval_predf_negate in H1. + now rewrite HEVAL in H1. + + inv H5. inv H3. + * inv H1. inv H5. + -- replace true with (negb false) in H1 by auto. eapply sem_pexpr_negate2 in H1. + eapply sem_pexpr_forward_eval in H1; eauto. + econstructor. apply exec_RB_falsy. cbn. destruct p. constructor; auto. inv H2. + erewrite <- eval_predf_pr_equiv; eauto. now cbn in H1. + -- replace true with (negb false) in H1 by auto. eapply sem_pexpr_negate2 in H1. + eapply sem_pexpr_forward_eval in H1; eauto. now rewrite HEVAL in H1. + * case_eq (eval_predf (is_ps i) (dfltp p)); intros. + -- eapply sem_pexpr_eval in H3; eauto. + destruct i. + exploit from_predicated_sem_pred_expr2; eauto; intros. + exploit sem_pred_expr_seq_app_val2. eapply HPRED. eauto. simplify. + inv H7. inv H15. clear H13. + exploit sem_merge_list; eauto; intros. instantiate (1:=args) in H7. + eapply sem_pred_expr_ident2 in H7; simplify. exploit sem_pred_expr_ident_det. + eapply H8. eauto. intros. subst. + inv H10. clear H8. eapply sem_val_list_det in H11; eauto. subst. + inv H2. + econstructor. econstructor. erewrite <- match_states_list; eauto. + erewrite <- storev_eval_condition; eauto. + assert (truthy is_ps p). + { destruct p. cbn in H4. constructor. + eapply sem_pexpr_forward_eval; eauto. + constructor. + } + eapply truthy_match_state; eassumption. + reflexivity. + -- econstructor. apply exec_RB_falsy. + destruct p. constructor. inv H2. erewrite <- eval_predf_pr_equiv; eauto. + easy. +Qed. + Lemma remember_expr_in : forall x l f a, In x l -> In x (remember_expr f l a). @@ -193,9 +445,16 @@ Proof. unfold remember_expr; destruct a; eauto using in_cons. Qed. +Lemma remember_expr_in_m : + forall x l f a, + In x l -> In x (remember_expr_m f l a). +Proof. + unfold remember_expr; destruct a; eauto using in_cons. +Qed. + Lemma in_mfold_left_abstr : - forall instrs p f l p' f' l' x, - mfold_left update' instrs (Some (p, f, l)) = Some (p', f', l') -> + forall instrs p f l p' f' l' x lm lm', + mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> In x l -> In x l'. Proof. induction instrs; intros. @@ -203,12 +462,28 @@ Proof. - cbn -[update] in *. pose proof H as Y. apply OptionExtra.mfold_left_Some in Y. inv Y. - rewrite H1 in H. destruct x0 as ((p_int & f_int) & l_int). + rewrite H1 in H. destruct x0 as (((p_int & f_int) & l_int) & lm_int). exploit IHinstrs; eauto. unfold Option.bind2, Option.ret in H1; repeat destr. inv H1. auto using remember_expr_in. Qed. +Lemma in_mfold_left_abstr_m : + forall instrs p f l p' f' l' x lm lm', + mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> + In x lm -> In x lm'. +Proof. + induction instrs; intros. + - cbn in *; now inv H. + - cbn -[update] in *. + pose proof H as Y. + apply OptionExtra.mfold_left_Some in Y. inv Y. + rewrite H1 in H. destruct x0 as (((p_int & f_int) & l_int) & lm_int). + exploit IHinstrs; eauto. + unfold Option.bind2, Option.ret in H1; repeat destr. inv H1. + auto using remember_expr_in_m. +Qed. + Lemma not_remembered_in_forest : forall a p f p_mid f_mid l x, update (p, f) a = Some (p_mid, f_mid) -> @@ -229,9 +504,23 @@ Proof. now rewrite forest_reg_gso by auto. Qed. +Lemma not_remembered_in_forest_m : + forall a p f p_mid f_mid l, + update (p, f) a = Some (p_mid, f_mid) -> + ~ In f #r Mem (remember_expr_m f l a) -> + f #r Mem = f_mid #r Mem. +Proof. + intros; destruct a; cbn in *; + unfold Option.bind in H; repeat destr; inv H; try easy. + - rewrite forest_reg_gso; auto. easy. + - rewrite forest_reg_gso; auto. easy. + - assert (~ (f #r Mem = f #r Mem) /\ ~ (In f #r Mem l)) by tauto. inv H. + contradiction. +Qed. + Lemma in_forest_or_remembered : - forall instrs p f l p' f' l', - mfold_left update' instrs (Some (p, f, l)) = Some (p', f', l') -> + forall instrs p f l p' f' l' lm lm', + mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> forall x, In (f #r (Reg x)) l' \/ f #r (Reg x) = f' #r (Reg x). Proof. induction instrs; try solve [crush]; []; intros. @@ -239,8 +528,8 @@ Proof. pose proof H as YX. apply OptionExtra.mfold_left_Some in YX. inv YX. rewrite H0 in H. - destruct x0 as ((p_mid & f_mid) & l_mid). - pose proof (IHinstrs _ _ _ _ _ _ H). + destruct x0 as (((p_mid & f_mid) & l_mid) & lm_mid). + pose proof (IHinstrs _ _ _ _ _ _ _ _ H). unfold Option.bind2, Option.ret in H0; cbn -[update] in H0; repeat destr. inv H0. specialize (H1 x). pose proof H as Y. @@ -250,9 +539,30 @@ Proof. rewrite n in *; tauto. Qed. +Lemma in_forest_or_remembered_m : + forall instrs p f l p' f' l' lm lm', + mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> + In (f #r Mem) lm' \/ f #r Mem = f' #r Mem. +Proof. + induction instrs; try solve [crush]; []; intros. + cbn -[update] in H. + pose proof H as YX. + apply OptionExtra.mfold_left_Some in YX. inv YX. + rewrite H0 in H. + destruct x as (((p_mid & f_mid) & l_mid) & lm_mid). + pose proof (IHinstrs _ _ _ _ _ _ _ _ H). + unfold Option.bind2, Option.ret in H0; cbn -[update] in H0; repeat destr. + inv H0. + pose proof H as Y. + destruct (in_dec pred_expr_eqb (f #r Mem) (remember_expr_m f lm a)); + eauto using in_mfold_left_abstr_m. + inv H1; eapply not_remembered_in_forest_m with (f_mid := f_mid) in n; eauto; + rewrite n in *; tauto. +Qed. + Lemma in_forest_evaluable : - forall G sp ge i' cf instrs p f l p' f' l' x i0, - mfold_left update' instrs (Some (p, f, l)) = Some (p', f', l') -> + forall G sp ge i' cf instrs p f l p' f' l' x i0 lm lm', + mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> sem (mk_ctx i0 sp ge) f' (i', cf) -> @evaluable_pred_list G (mk_ctx i0 sp ge) f'.(forest_preds) l' -> evaluable_pred_expr (mk_ctx i0 sp ge) f'.(forest_preds) (f #r (Reg x)). @@ -264,37 +574,31 @@ Proof. unfold evaluable_pred_expr. eauto. Qed. -Definition gather_predicates (preds : PTree.t unit) (i : instr): option (PTree.t unit) := - match i with - | RBop (Some p) _ _ _ - | RBload (Some p) _ _ _ _ - | RBstore (Some p) _ _ _ _ - | RBexit (Some p) _ => - Some (fold_right (fun x => PTree.set x tt) preds (predicate_use p)) - | RBsetpred p' c args p => - let preds' := match p' with - | Some p'' => fold_right (fun x => PTree.set x tt) preds (predicate_use p'') - | None => preds - end - in - match preds' ! p with - | Some _ => None - | None => Some preds' - end - | _ => Some preds - end. +Lemma in_forest_evaluable_m : + forall G sp ge i' cf instrs p f l p' f' l' i0 lm lm', + mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> + sem (mk_ctx i0 sp ge) f' (i', cf) -> + @evaluable_pred_list_m G (mk_ctx i0 sp ge) f'.(forest_preds) lm' -> + evaluable_pred_expr_m (mk_ctx i0 sp ge) f'.(forest_preds) (f #r Mem). +Proof. + intros. + pose proof H as Y. apply in_forest_or_remembered_m in Y. + inv Y; eauto. + inv H0. inv H5. rewrite H2. + unfold evaluable_pred_expr_m. eauto. +Qed. Lemma abstr_seq_revers_correct_fold_sem_pexpr : - forall instrs p f l p' f' l' preds preds', - mfold_left update' instrs (Some (p, f, l)) = Some (p', f', l') -> + forall instrs p f l p' f' l' preds preds' lm lm', + mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> mfold_left gather_predicates instrs (Some preds) = Some preds' -> forall pred, preds ! pred = Some tt -> f #p pred = f' #p pred. Proof. Admitted. Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval : - forall G instrs p f l p' f' l' i0 sp ge ps preds preds' ps', - mfold_left update' instrs (Some (p, f, l)) = Some (p', f', l') -> + forall G instrs p f l p' f' l' i0 sp ge ps preds preds' ps' lm lm', + mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> mfold_left gather_predicates instrs (Some preds) = Some preds' -> forall pred, preds ! pred = Some tt -> sem_predset (mk_ctx i0 sp ge) f ps -> @@ -302,9 +606,23 @@ Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval : ps !! pred = ps' !! pred. Proof. Admitted. +Definition all_preds_in f preds := + (forall x, NE.Forall (fun x => forall pred, PredIn pred (fst x) + -> PTree.get pred preds = Some tt) (f #r x)) + /\ NE.Forall (fun x => forall pred, PredIn pred (fst x) + -> PTree.get pred preds = Some tt) f.(forest_exit). + +Lemma gather_predicates_in_forest : + forall p i f p' f' preds preds', + update (p, f) i = Some (p', f') -> + gather_predicates preds i = Some preds' -> + all_preds_in f preds -> + all_preds_in f' preds'. +Proof. Admitted. + Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval3 : - forall A B G a_sem instrs p f l p' f' l' i0 sp ge preds preds' pe pe_val, - mfold_left update' instrs (Some (p, f, l)) = Some (p', f', l') -> + forall A B G a_sem instrs p f l p' f' l' i0 sp ge preds preds' pe pe_val lm lm', + mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> mfold_left gather_predicates instrs (Some preds) = Some preds' -> @sem_pred_expr G A B f'.(forest_preds) a_sem (mk_ctx i0 sp ge) pe pe_val -> NE.Forall (fun x => forall pred, PredIn pred (fst x) @@ -314,7 +632,7 @@ Proof. induction instrs; try solve [crush]; intros. cbn -[update] in *. exploit OptionExtra.mfold_left_Some. eapply H. - intros [[[p_mid f_mid] l_mid] HBind]. rewrite HBind in H. + intros [[[[p_mid f_mid] l_mid] lm_mid] HBind]. rewrite HBind in H. exploit OptionExtra.mfold_left_Some. eapply H0. intros [preds_mid HGather]. rewrite HGather in H0. exploit IHinstrs. eassumption. eassumption. eassumption. admit. @@ -324,8 +642,8 @@ Proof. (* intros [[p_val e_val] [HIN HSEM]]. *) Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval2 : - forall G instrs p f l p' f' l' i0 sp ge preds preds' pe, - mfold_left update' instrs (Some (p, f, l)) = Some (p', f', l') -> + forall G instrs p f l p' f' l' i0 sp ge preds preds' pe lm lm', + mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> mfold_left gather_predicates instrs (Some preds) = Some preds' -> @evaluable_pred_expr G (mk_ctx i0 sp ge) f'.(forest_preds) pe -> NE.Forall (fun x => forall pred, PredIn pred (fst x) @@ -337,21 +655,42 @@ Proof. eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3; eauto. Qed. +Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval4 : + forall G instrs p f l p' f' l' i0 sp ge preds preds' pe lm lm', + mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> + mfold_left gather_predicates instrs (Some preds) = Some preds' -> + @evaluable_pred_expr_m G (mk_ctx i0 sp ge) f'.(forest_preds) pe -> + NE.Forall (fun x => forall pred, PredIn pred (fst x) + -> PTree.get pred preds = Some tt) pe -> + evaluable_pred_expr_m (mk_ctx i0 sp ge) f.(forest_preds) pe. +Proof. + unfold evaluable_pred_expr in *. + intros. inv H1. exists x. + eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3; eauto. +Qed. + +Lemma state_lessdef_state_equiv : + forall x y, state_lessdef x y <-> state_equiv x y. +Proof. split; intros; inv H; constructor; auto. Qed. + (* [[id:5e6486bb-fda2-4558-aed8-243a9698de85]] *) Lemma abstr_seq_reverse_correct_fold : - forall sp instrs i0 i i' ti cf f' l p p' l' f, + forall sp instrs i0 i i' ti cf f' l p p' l' f preds preds' lm lm', valid_mem (is_mem i0) (is_mem i) -> + all_preds_in f preds -> eval_predf (is_ps i) p = true -> sem (mk_ctx i0 sp ge) f (i, None) -> - mfold_left update' instrs (Some (p, f, l)) = Some (p', f', l') -> + mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> + mfold_left gather_predicates instrs (Some preds) = Some preds' -> evaluable_pred_list (mk_ctx i0 sp ge) f'.(forest_preds) l' -> + evaluable_pred_list_m (mk_ctx i0 sp ge) f'.(forest_preds) lm' -> sem (mk_ctx i0 sp ge) f' (i', Some cf) -> state_lessdef i ti -> exists ti', SeqBB.step ge sp (Iexec ti) instrs (Iterm ti' cf) /\ state_lessdef i' ti'. Proof. - induction instrs; intros * YVALID YEVAL Y3 Y Y0 Y1 Y2. + induction instrs; intros * YVALID YALL YEVAL Y3 Y YGATHER Y0 YEVALUABLE Y1 Y2. - cbn in *. inv Y. assert (X: similar {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |}) @@ -360,36 +699,93 @@ Proof. - cbn -[update] in Y. pose proof Y as YX. apply OptionExtra.mfold_left_Some in YX. inv YX. + cbn in YGATHER. + pose proof YGATHER as YX. + apply OptionExtra.mfold_left_Some in YX. inv YX. rewrite H0 in YGATHER. + pose proof H0 as YGATHER_SINGLE. clear H0. rewrite H in Y. destruct x as ((p_mid & f_mid) & l_mid). unfold Option.bind2, Option.ret in H. repeat destr. inv H. - (* Assume we are in RBop for now*) - assert (exists pred op args dst, a = RBop pred op args dst) - by admit; destruct H as (pred & op & args & dst & EQ); subst a. - - exploit evaluable_pred_expr_exists; eauto. - eapply abstr_seq_revers_correct_fold_sem_pexpr_eval2; eauto. admit. admit. - admit. - - (* I have the pred already from sem. *) - intros [ti_mid HSTEP]. - (* unfold evaluable_pred_list in Y0. *) - (* instantiate (1 := forest_preds f'). *) - (* eapply in_forest_evaluable; eauto. *) - (* (* provable using evaluability in list *) intros [t step]. *) - - pose proof Y3 as YH. - pose proof HSTEP as YHSTEP. - pose proof Y2 as Y2SPLIT; inv Y2SPLIT. - eapply step_exists in YHSTEP. - 2: { symmetry. econstructor; try eassumption; auto. } - inv YHSTEP. inv H1. - exploit sem_update_instr. auto. eauto. eauto. eauto. eauto. auto. intros. - exploit IHinstrs. 3: { eauto. } admit. admit. eauto. admit. eauto. symmetry. - instantiate (1:=ti_mid). admit. intros [ti' [YHH HLD]]. - exists ti'; split; eauto. econstructor; eauto. + destruct a. + + cbn in Heqo. inv Heqo. cbn in YGATHER_SINGLE. inv YGATHER_SINGLE. + exploit IHinstrs; eauto; simplify. + exists x; split; auto. econstructor. constructor. auto. + + exploit evaluable_pred_expr_exists_RBop; eauto. + eapply abstr_seq_revers_correct_fold_sem_pexpr_eval2; eauto. + unfold evaluable_pred_list in Y0. eapply in_forest_evaluable; eauto. + eapply gather_predicates_in_forest in YALL; eauto. + unfold all_preds_in in YALL. inv YALL. eauto. + intros [ti_mid HSTEP]. + + pose proof Y3 as YH. + pose proof HSTEP as YHSTEP. + pose proof Y2 as Y2SPLIT; inv Y2SPLIT. + eapply step_exists in YHSTEP. + 2: { symmetry. econstructor; try eassumption; auto. } + inv YHSTEP. inv H1. + exploit sem_update_instr. auto. eauto. eauto. eauto. eauto. auto. intros. + exploit IHinstrs. 4: { eauto. } + cbn in YVALID. transitivity m'; auto. + replace m' with (is_mem {| is_rs := rs; Gible.is_ps := ps; Gible.is_mem := m' |}) by auto. + eapply sem_update_valid_mem; eauto. + eapply gather_predicates_in_forest; eauto. + eapply eval_predf_update_true; eauto. + eauto. eauto. eauto. eauto. eauto. symmetry. + eapply state_lessdef_state_equiv; eauto. + intros [ti' [YHH HLD]]. + exists ti'; split; eauto. econstructor; eauto. + + exploit evaluable_pred_expr_exists_RBload; eauto. + eapply abstr_seq_revers_correct_fold_sem_pexpr_eval2; eauto. + unfold evaluable_pred_list in Y0. eapply in_forest_evaluable; eauto. + eapply gather_predicates_in_forest in YALL; eauto. + unfold all_preds_in in YALL. inv YALL. eauto. + intros [ti_mid HSTEP]. + + pose proof Y3 as YH. + pose proof HSTEP as YHSTEP. + pose proof Y2 as Y2SPLIT; inv Y2SPLIT. + eapply step_exists in YHSTEP. + 2: { symmetry. econstructor; try eassumption; auto. } + inv YHSTEP. inv H1. + exploit sem_update_instr. auto. eauto. eauto. eauto. eauto. auto. intros. + exploit IHinstrs. 4: { eauto. } + cbn in YVALID. transitivity m'; auto. + replace m' with (is_mem {| is_rs := rs; Gible.is_ps := ps; Gible.is_mem := m' |}) by auto. + eapply sem_update_valid_mem; eauto. + eapply gather_predicates_in_forest; eauto. + eapply eval_predf_update_true; eauto. + eauto. eauto. eauto. eauto. eauto. symmetry. + eapply state_lessdef_state_equiv; eauto. + intros [ti' [YHH HLD]]. + exists ti'; split; eauto. econstructor; eauto. + + exploit evaluable_pred_expr_exists_RBstore; eauto. + eapply abstr_seq_revers_correct_fold_sem_pexpr_eval4; eauto. + unfold evaluable_pred_list in Y0. eapply in_forest_evaluable_m; eauto. + eapply gather_predicates_in_forest in YALL; eauto. + unfold all_preds_in in YALL. inv YALL. eauto. + intros [ti_mid HSTEP]. + + pose proof Y3 as YH. + pose proof HSTEP as YHSTEP. + pose proof Y2 as Y2SPLIT; inv Y2SPLIT. + eapply step_exists in YHSTEP. + 2: { symmetry. econstructor; try eassumption; auto. } + inv YHSTEP. inv H1. + exploit sem_update_instr. auto. eauto. eauto. eauto. eauto. auto. intros. + exploit IHinstrs. 4: { eauto. } + cbn in YVALID. transitivity m'; auto. + replace m' with (is_mem {| is_rs := rs; Gible.is_ps := ps; Gible.is_mem := m' |}) by auto. + eapply sem_update_valid_mem; eauto. + eapply gather_predicates_in_forest; eauto. + eapply eval_predf_update_true; eauto. + eauto. eauto. eauto. eauto. eauto. symmetry. + eapply state_lessdef_state_equiv; eauto. + intros [ti' [YHH HLD]]. + exists ti'; split; eauto. econstructor; eauto. + + admit. + + admit. Admitted. Lemma sem_empty : @@ -408,21 +804,16 @@ Qed. Lemma abstr_seq_reverse_correct: forall sp x i i' ti cf x' l, abstract_sequence' x = Some (x', l) -> - (forall p, In p l -> exists r, sem_pred_expr x'.(forest_preds) sem_value (mk_ctx i sp ge) p r) -> + evaluable_pred_list (mk_ctx i sp ge) x'.(forest_preds) l -> sem (mk_ctx i sp ge) x' (i', (Some cf)) -> state_lessdef i ti -> exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf) /\ state_lessdef i' ti'. Proof. -(* intros. exploit sem_exists_execution; eauto; simplify. - eauto using sem_equiv_execution. -Qed. *) intros. unfold abstract_sequence' in H. - unfold Option.map in H. repeat destr. inv H. - eapply abstr_seq_reverse_correct_fold. - 2: { eauto. } - all: eauto. - apply sem_empty. + unfold Option.map, Option.bind in H. repeat destr. inv H. inv Heqo. + eapply abstr_seq_reverse_correct_fold; + try eassumption; try reflexivity; apply sem_empty. Qed. (*| diff --git a/src/hls/GiblePargenproofForward.v b/src/hls/GiblePargenproofForward.v index bd18855..6411351 100644 --- a/src/hls/GiblePargenproofForward.v +++ b/src/hls/GiblePargenproofForward.v @@ -332,12 +332,6 @@ all be evaluable. predicated_not_inP pred (forest_exit f). Proof. Admitted. - Lemma from_predicated_sem_pred_expr : - forall A (ctx: @ctx A) preds pe b, - sem_pred_expr preds sem_pred ctx pe b -> - sem_pexpr ctx (from_predicated true preds pe) b. - Proof. Admitted. - Lemma sem_update_Isetpred: forall A (ctx: @ctx A) f pr p0 c args b rs m, valid_mem (ctx_mem ctx) m -> |