From fa3bd7cf4caf43b9e29e3aed834af19aa7a3c794 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 21 May 2023 17:37:54 +0100 Subject: Finish abstr_seq_reverse_correct_fold --- src/hls/Gible.v | 11 ++++ src/hls/GiblePargenproofBackward.v | 122 ++++++++++++++++++++++++++----------- src/hls/GibleSeq.v | 18 ++++++ 3 files changed, 116 insertions(+), 35 deletions(-) (limited to 'src/hls') diff --git a/src/hls/Gible.v b/src/hls/Gible.v index b7959be..d7b0e66 100644 --- a/src/hls/Gible.v +++ b/src/hls/Gible.v @@ -440,6 +440,17 @@ Proof. repeat constructor; inv H; erewrite eval_predf_pr_equiv; eauto. Qed. +Lemma step_exists_Iterm: + forall sp i instr ti cf, + step_instr sp (Iexec i) instr (Iterm i cf) -> + state_equiv i ti -> + step_instr sp (Iexec ti) instr (Iterm ti cf). +Proof. + inversion_clear 1; subst; intros. + econstructor. + inv H. eapply truthy_match_state; eauto. +Qed. + End RELABSTR. (*| diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v index f3fdacd..b4b4145 100644 --- a/src/hls/GiblePargenproofBackward.v +++ b/src/hls/GiblePargenproofBackward.v @@ -113,6 +113,19 @@ Definition update' (s: pred_op * forest * list pred_expr * list pred_expr) (i: i 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). +Lemma equiv_update: + forall i p f l lm p' f' l' lm', + mfold_left update' i (Some (p, f, l, lm)) = Some (p', f', l', lm') -> + mfold_left update i (Some (p, f)) = Some (p', f'). +Proof. + induction i; cbn -[update] in *; intros. + - inv H; auto. + - exploit OptionExtra.mfold_left_Some; eauto; + intros [[[[p_mid f_mid] l_mid] lm_mid] HB]. + unfold Option.bind2, Option.ret in HB; repeat destr. inv Heqp1. + eapply IHi; eauto. +Qed. + Definition gather_predicates (preds : PTree.t unit) (i : instr): option (PTree.t unit) := match i with | RBop (Some p) _ _ _ @@ -459,6 +472,17 @@ Proof. erewrite <- eval_predf_pr_equiv; eauto. Qed. +Lemma evaluable_pred_expr_exists_RBexit3 : + forall i p cf f p_exit p_exit' f', + eval_predf (is_ps i) (dfltp p) = true -> + update (p_exit, f) (RBexit p cf) = Some (p_exit', f') -> + eval_predf (is_ps i) p_exit' = false. +Proof. + intros. cbn in *. unfold Option.bind in *. destr. inv H0. + rewrite eval_predf_simplify. rewrite eval_predf_Pand. + rewrite eval_predf_negate. rewrite H. auto. +Qed. + Lemma remember_expr_in : forall x l f a, In x l -> In x (remember_expr f l a). @@ -618,13 +642,11 @@ Lemma abstr_seq_revers_correct_fold_sem_pexpr : 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' lm lm', + forall G instrs p f l p' f' l' i0 sp ge 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 -> - sem_predset (@mk_ctx G i0 sp ge) f' ps' -> - ps !! pred = ps' !! pred. + sem_predset (@mk_ctx G i0 sp ge) f' ps' -> + exists ps, sem_predset (mk_ctx i0 sp ge) f ps. Proof. Admitted. Definition all_preds_in f preds := @@ -694,9 +716,19 @@ Lemma state_lessdef_state_equiv : forall x y, state_lessdef x y <-> state_equiv x y. Proof. split; intros; inv H; constructor; auto. Qed. +Lemma abstr_seq_reverse_correct_fold_false : + forall sp instrs i0 i ti cf f' l p p' l' f lm lm', + eval_predf (is_ps i) p = false -> + sem (mk_ctx i0 sp ge) f (i, Some cf) -> + mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> + sem (mk_ctx i0 sp ge) f' (i, Some cf) -> + state_lessdef i ti -> + SeqBB.step ge sp (Iexec ti) instrs (Iterm ti cf). +Proof. Admitted. + (* [[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 preds preds' lm lm', + forall sp instrs i0 i i' ti cf f' l p p' l' f preds preds' lm lm' ps', valid_mem (is_mem i0) (is_mem i) -> all_preds_in f preds -> eval_predf (is_ps i) p = true -> @@ -705,13 +737,14 @@ Lemma abstr_seq_reverse_correct_fold : 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_predset (mk_ctx i0 sp ge) f' ps' -> 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 YALL YEVAL Y3 Y YGATHER Y0 YEVALUABLE Y1 Y2. + induction instrs; intros * YVALID YALL YEVAL Y3 Y YGATHER Y0 YEVALUABLE YSEM_FINAL 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 |}) @@ -753,7 +786,7 @@ Proof. eapply sem_update_valid_mem; eauto. eapply gather_predicates_in_forest; eauto. eapply eval_predf_update_true; eauto. - eauto. eauto. eauto. eauto. eauto. symmetry. + eauto. eauto. eauto. eauto. eauto. eauto. symmetry. eapply state_lessdef_state_equiv; eauto. intros [ti' [YHH HLD]]. exists ti'; split; eauto. econstructor; eauto. @@ -777,7 +810,7 @@ Proof. eapply sem_update_valid_mem; eauto. eapply gather_predicates_in_forest; eauto. eapply eval_predf_update_true; eauto. - eauto. eauto. eauto. eauto. eauto. symmetry. + eauto. eauto. eauto. eauto. eauto. eauto. symmetry. eapply state_lessdef_state_equiv; eauto. intros [ti' [YHH HLD]]. exists ti'; split; eauto. econstructor; eauto. @@ -787,7 +820,7 @@ Proof. 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. @@ -801,13 +834,14 @@ Proof. eapply sem_update_valid_mem; eauto. eapply gather_predicates_in_forest; eauto. eapply eval_predf_update_true; eauto. - eauto. eauto. eauto. eauto. eauto. symmetry. + 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_RBsetpred; eauto. admit. + + exploit abstr_seq_revers_correct_fold_sem_pexpr_eval; eauto; intros [ps_mid HPRED2]. + exploit evaluable_pred_expr_exists_RBsetpred; eauto. intros [ti_mid HSTEP]. - + pose proof Y3 as YH. pose proof HSTEP as YHSTEP. pose proof Y2 as Y2SPLIT; inv Y2SPLIT. @@ -821,33 +855,50 @@ Proof. eapply sem_update_valid_mem; eauto. eapply gather_predicates_in_forest; eauto. eapply eval_predf_update_true; eauto. - eauto. eauto. eauto. eauto. eauto. symmetry. + eauto. eauto. eauto. eauto. eauto. eauto. symmetry. eapply state_lessdef_state_equiv; eauto. intros [ti' [YHH HLD]]. exists ti'; split; eauto. econstructor; eauto. + case_eq (eval_predf (is_ps i) (dfltp o)); intros. - * admit. + * exploit evaluable_pred_expr_exists_RBexit2; eauto; intros HSTEP. + instantiate (1:=c) in HSTEP. + instantiate (1:=sp) in HSTEP. + exploit evaluable_pred_expr_exists_RBexit3. eauto. eauto. intros. + pose proof (state_lessdef_state_equiv i ti). inv H1. + specialize (H2 Y2). + pose proof (step_exists_Iterm ge sp ti _ i _ HSTEP + ltac:(symmetry; assumption)). + exploit sem_update_instr_term; eauto; intros. inv H4. + exploit abstr_fold_falsy; auto. eauto. eapply equiv_update; eauto. cbn. auto. + intros. eapply sem_det in Y1; eauto. inv Y1. inv H7. + exploit abstr_seq_reverse_correct_fold_false. + eapply H6. eapply H5. eauto. eauto. eauto. intros. + 2: { reflexivity. } + exploit GibleSeq.step_exists. eapply H7. transitivity i. symmetry. + eapply state_lessdef_state_equiv; auto. eauto. simplify. + exists ti; split; auto. constructor. auto. transitivity i. symmetry; auto. + auto. * exploit evaluable_pred_expr_exists_RBexit; eauto; intros HSTEP. - instantiate (1:=cf) in HSTEP. instantiate (1:=sp) in HSTEP. + instantiate (1:=c) in HSTEP. instantiate (1:=sp) in 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 H2. - exploit sem_update_instr. auto. eauto. eauto. eauto. eapply Heqo. 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. - reflexivity. eauto. 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. - -Admitted. + 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 H2. + exploit sem_update_instr. auto. eauto. eauto. eauto. eapply Heqo. 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. + cbn. inv H4. + reflexivity. + eapply gather_predicates_in_forest; eauto. + eapply eval_predf_update_true; eauto. + eauto. eauto. eauto. eauto. eauto. eauto. symmetry. + eapply state_lessdef_state_equiv; eauto. + intros [ti' [YHH HLD]]. + exists ti'; split; eauto. econstructor; eauto. +Qed. Lemma sem_empty : forall G (ctx: @Abstr.ctx G), @@ -871,10 +922,11 @@ Proof. Qed. Lemma abstr_seq_reverse_correct: - forall sp x i i' ti cf x' l lm, + forall sp x i i' ti cf x' l lm ps', abstract_sequence' x = Some (x', l, lm) -> evaluable_pred_list (mk_ctx i sp ge) x'.(forest_preds) l -> evaluable_pred_list_m (mk_ctx i sp ge) x'.(forest_preds) lm -> + sem_predset {| ctx_is := i; ctx_sp := sp; ctx_ge := ge |} x' ps' -> 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) diff --git a/src/hls/GibleSeq.v b/src/hls/GibleSeq.v index e99c860..c9d7ab2 100644 --- a/src/hls/GibleSeq.v +++ b/src/hls/GibleSeq.v @@ -314,3 +314,21 @@ Lemma step_instr_unchanged_state : forall A (ge: Genv.t A unit) sp r st st' cf, step_instr ge sp (Iexec st) r (Iterm st' cf) -> st = st'. Proof. intros. inv H; auto. Qed. + +Lemma step_exists: + forall A (ge: Genv.t A unit) sp instrs i i' ti cf, + SeqBB.step ge sp (Iexec i) instrs (Iterm i' cf) -> + state_equiv i ti -> + exists ti', + SeqBB.step ge sp (Iexec ti) instrs (Iterm ti' cf) + /\ state_equiv i' ti'. +Proof. + induction instrs. + - intros. inv H. + - intros. inv H. + + exploit (@step_exists A); eauto; simplify. + exploit IHinstrs; eauto; simplify. + eexists; split. econstructor; eauto. auto. + + inversion H4; subst. eexists. constructor. + constructor. eapply step_exists_Iterm; eauto. auto. +Qed. -- cgit