diff options
Diffstat (limited to 'src/hls/GiblePargenproofBackward.v')
-rw-r--r-- | src/hls/GiblePargenproofBackward.v | 152 |
1 files changed, 138 insertions, 14 deletions
diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v index 7b68475..718eb66 100644 --- a/src/hls/GiblePargenproofBackward.v +++ b/src/hls/GiblePargenproofBackward.v @@ -33,6 +33,7 @@ Require Import vericert.hls.GiblePargenproofEquiv. Require Import vericert.hls.GiblePargen. Require Import vericert.hls.Predicate. Require Import vericert.hls.Abstr. +Require Import vericert.hls.AbstrSemIdent. Require Import vericert.common.Monad. Require Import Optionmonad. @@ -49,6 +50,8 @@ Module Import OptionExtra := MonadExtra(Option). Definition state_lessdef := GiblePargenproofEquiv.match_states. +(* Set Nested Proofs Allowed. *) + (*| =================================== GiblePar to Abstr Translation Proof @@ -113,17 +116,46 @@ Definition evaluable_pred_list {G} ctx pr l := In p l -> @evaluable_pred_expr 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') -> *) +(* sem (mk_ctx i0 sp ge) f (i, cf) -> *) +(* evaluable_pred_expr (mk_ctx i0 sp ge) pr (f' #r (Reg dst)) -> *) +(* state_lessdef i ti -> *) +(* exists i', sem (mk_ctx i0 sp ge) f' (i', cf). *) +(* Proof. *) +(* intros. cbn in H. unfold Option.bind in H. destr. inv H. *) +(* destruct ti. econstructor. econstructor. *) +(* unfold evaluable_pred_expr in H1. Admitted. *) + Lemma evaluable_pred_expr_exists : - forall sp pr f i0 exit_p exit_p' f' cf i ti p op args dst, + forall sp pr f i0 exit_p exit_p' f' i ti p op args dst, + (forall x, sem_pexpr (mk_ctx i0 sp ge) (get_forest_p' x f'.(forest_preds)) (pr !! x)) -> + eval_predf pr exit_p = true -> update (exit_p, f) (RBop p op args dst) = Some (exit_p', f') -> - sem (mk_ctx i0 sp ge) f (i, cf) -> - evaluable_pred_expr (mk_ctx i0 sp ge) pr (f' #r (Reg dst)) -> + 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) (RBop p op args dst) (Iexec ti'). Proof. - intros. cbn in H. unfold Option.bind in H. destr. inv H. - destruct ti. econstructor. econstructor. - unfold evaluable_pred_expr in H1. Admitted. + intros * HPRED HEVAL **. cbn -[seq_app] in H. unfold Option.bind in H. destr. inv H. + destruct ti. + 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. + assert (eval_predf pr (dfltp p ∧ exit_p') = true) by admit. + exploit sem_pred_expr_app_predicated2; eauto; intros. + exploit sem_pred_expr_seq_app_val2; eauto; simplify. + unfold pred_ret in *. inv H4. inv H12. + destruct i. exploit sem_merge_list; eauto; intros. + instantiate (1 := args) in H4. + eapply sem_pred_expr_ident2 in H4. simplify. + exploit sem_pred_expr_ident_det. eapply H5. eapply H4. + intros. subst. exploit sem_pred_expr_ident. eapply H5. eapply H8. + intros. + + econstructor. econstructor. + Admitted. Lemma remember_expr_in : forall x l f a, @@ -148,6 +180,100 @@ Proof. auto using remember_expr_in. 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) -> + ~ In f #r (Reg x) (remember_expr f l a) -> + f #r (Reg x) = f_mid #r (Reg x). +Proof. + intros; destruct a; cbn in *; + unfold Option.bind in H; repeat destr; inv H; try easy. + - assert (~ (f #r (Reg r) = f #r (Reg x)) /\ ~ (In f #r (Reg x) l)) by tauto. + inv H. destruct (resource_eq (Reg r) (Reg x)); + try (rewrite e in *; contradiction). + now rewrite forest_reg_gso by auto. + - assert (~ (f #r (Reg r) = f #r (Reg x)) /\ ~ (In f #r (Reg x) l)) by tauto. + inv H. destruct (resource_eq (Reg r) (Reg x)); + try (rewrite e in *; contradiction). + now rewrite forest_reg_gso by auto. + - destruct (resource_eq Mem (Reg x)); try discriminate. + now rewrite forest_reg_gso by auto. +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 x, In (f #r (Reg x)) l' \/ f #r (Reg x) = f' #r (Reg x). +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 x0 as ((p_mid & f_mid) & l_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. + destruct (in_dec pred_expr_eqb (f #r (Reg x)) (remember_expr f l a)); + eauto using in_mfold_left_abstr. + inv H1; eapply not_remembered_in_forest 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') -> + 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)). +Proof. + intros. + pose proof H as Y. apply in_forest_or_remembered with (x := x) in Y. + inv Y; eauto. + inv H0. inv H5. rewrite H2. + 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 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') -> + 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') -> + 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. +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, sem (mk_ctx i0 sp ge) f (i, None) -> @@ -178,15 +304,13 @@ Proof. by admit; destruct H as (pred & op & args & dst & EQ); subst a. exploit evaluable_pred_expr_exists; eauto. - unfold evaluable_pred_list in Y0. - instantiate (1 := forest_preds f'). - apply Y0 in YI. auto. - (* provable using evaluability in list *) intros [t step]. - - assert (exists ti_mid, sem {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} - f_mid (ti_mid, None)) by admit. + (* I have the pred already from sem. *) + admit. admit. admit. intros [t step]. + (* unfold evaluable_pred_list in Y0. *) + (* instantiate (1 := forest_preds f'). *) + (* eapply in_forest_evaluable; eauto. *) + (* (* provable using evaluability in list *) intros [t step]. *) - destruct H as (ti_mid & Hsem2). exploit IHinstrs. 2: { eapply Y. } eauto. auto. eauto. reflexivity. intros (ti_mid' & Hseq & Hstate). assert (state_lessdef ti_mid t) by admit. |