From 42ab7386b7d1a312712bf8dd4031c06fce5bc1ff Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 25 Sep 2023 22:00:58 +0200 Subject: Add incremental evaluability check --- debug/vericertTest.ml | 15 +- src/extraction/Extraction.v | 1 + src/hls/GiblePargen.v | 19 +- src/hls/GiblePargenproof.v | 400 +++++++++++++++++++++ src/hls/GiblePargenproofBackward.v | 690 ++++++++++++++++++++++++++++++++++++- src/hls/PrintAbstr.ml | 13 + 6 files changed, 1127 insertions(+), 11 deletions(-) diff --git a/debug/vericertTest.ml b/debug/vericertTest.ml index 48391db..87c9e60 100644 --- a/debug/vericertTest.ml +++ b/debug/vericertTest.ml @@ -26,7 +26,12 @@ let schedule_oracle l bb bbt = let (p2, m_expr_t) = p1 in let (bbt', reg_expr_t) = p2 in printf "F1:\n%a\n" PrintAbstr.print_forest bb'; - printf "F2:\n%a\n" PrintAbstr.print_forest bbt'; flush stdout; + printf "%a\n" PrintAbstr.print_evaluability_list reg_expr; + printf "%a\n" PrintAbstr.print_evaluability_list2 m_expr; + printf "F2:\n%a\n" PrintAbstr.print_forest bbt'; + printf "%a\n" PrintAbstr.print_evaluability_list reg_expr_t; + printf "%a\n" PrintAbstr.print_evaluability_list2 m_expr_t; + flush stdout; (&&) ((&&) ((&&) (if check l bb' bbt' then true else (Printf.printf "Failed 1\n"; false)) (empty_trees bb bbt)) (if (check_evaluability1 reg_expr reg_expr_t) then true else (Printf.printf "Failed 12\n"; false))) @@ -179,12 +184,12 @@ let () = seteq None 2 12 13; add None 2 1 4; mul (Some (Pand (plit false 1, plit false 2))) 3 1 1; - mul (Some (Pand (plit false 1, plit false 2))) 5 3 3; + mul (Some (Pand (plit false 1, plit false 2))) 3 3 3; goto (Some (Pand (plit false 1, plit false 2))) 10; mul (Some (Pand (plit false 1, plit true 2))) 3 1 4; goto (Some (Pand (plit false 1, plit true 2))) 10; add (Some (plit true 1)) 1 2 4; - mul (Some (Pand (plit true 1, plit false 2))) 5 3 3; + mul (Some (Pand (plit true 1, plit false 2))) 3 3 3; goto (Some (Pand (plit true 1, plit false 2))) 10; mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; goto (Some (Pand (plit true 1, plit true 2))) 10; @@ -197,8 +202,8 @@ let () = add (Some (plit true 1)) 1 2 4; mul (Some (Pand (plit false 1, plit true 2))) 3 1 4; mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; - mul (Some (Pand (plit false 1, plit false 2))) 5 3 3; - mul (Some (Pand (plit true 1, plit false 2))) 5 3 3; + mul (Some (Pand (plit false 1, plit false 2))) 3 3 3; + mul (Some (Pand (plit true 1, plit false 2))) 3 3 3; goto None 10; ] ] ] then Printf.printf "Passed 110\n" diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 0a83f02..f78b0bd 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -210,6 +210,7 @@ Separate Extraction Bourdoncle.bourdoncle Smtpredicate.check_smt_total + GiblePargen.abstract_sequence_top_inc Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index 4095977..7dd1c97 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -347,13 +347,13 @@ Definition remember_expr_inc (fop : pred_op * forest) (lst: list (resource * pre let (pred, f) := fop in match i with | RBnop => lst - | RBop p op rl r => (Reg r, (NE.map (fun x => (dfltp p ∧ pred ∧ fst x, snd x)) - (seq_app (pred_ret (Eop op)) (merge (list_translation rl f))))) :: lst - | RBload p chunk addr rl r => (Reg r, (NE.map (fun x => (dfltp p ∧ pred ∧ fst x, snd x)) + | RBop p op rl r => (Reg r, (app_predicated (dfltp p ∧ pred) (NE.singleton (Ptrue, Ebase (Reg 1))) ( + (seq_app (pred_ret (Eop op)) (merge (list_translation rl f)))))) :: lst + | RBload p chunk addr rl r => (Reg r, (app_predicated (dfltp p ∧ pred) (NE.singleton (Ptrue, Ebase (Reg 1))) ( (seq_app (seq_app (pred_ret (Eload chunk addr)) (merge (list_translation rl f))) - (f #r Mem)))) :: lst + (f #r Mem))))) :: lst | RBstore p chunk addr rl r => lst | RBsetpred p' c args p => lst | RBexit p c => lst @@ -365,7 +365,7 @@ Definition remember_expr_m_inc (fop : pred_op * forest) (lst: list pred_expr) (i | RBnop => lst | RBop p op rl r => lst | RBload p chunk addr rl r => lst - | RBstore p chunk addr rl r => (NE.map (fun x => (dfltp p ∧ pred ∧ fst x, snd x)) + | RBstore p chunk addr rl r => (app_predicated (dfltp p ∧ pred) (NE.singleton (Ptrue, Ebase Mem)) (seq_app (seq_app (flap2 (seq_app (pred_ret Estore) @@ -490,6 +490,15 @@ Definition schedule_oracle (bb: SeqBB.t) (bbt: ParBB.t) : bool := | _, _ => false end. +Definition schedule_oracle_inc (bb: SeqBB.t) (bbt: ParBB.t) : bool := + match abstract_sequence_top_inc bb, abstract_sequence_top_inc (concat (concat bbt)) with + | Some (bb', reg_expr, m_expr), Some (bbt', reg_expr_t, m_expr_t) => + check nil bb' bbt' && empty_trees bb bbt + && check_evaluability1 reg_expr reg_expr_t + && check_evaluability2 m_expr m_expr_t + | _, _ => false + end. + Definition check_scheduled_trees := beq2 schedule_oracle. Ltac solve_scheduled_trees_correct := diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index afa554c..1b5e505 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -57,6 +57,15 @@ Proof. inv Heqp1. now inv H. Qed. +Lemma equiv_update_top_inc: + forall i p f l lm p' f' l' lm', + update_top_inc (p, f, l, lm) i = Some (p', f', l', lm') -> + update (p, f) i = Some (p', f'). +Proof. + intros. unfold update_top_inc, Option.bind2, Option.ret in *. repeat destr. + inv Heqp1. now inv H. +Qed. + Lemma remember_expr_eq : forall l i f, remember_expr f (map snd l) i = map snd (GiblePargen.remember_expr f l i). @@ -64,6 +73,14 @@ Proof. induction l; destruct i; auto. Qed. +Lemma remember_expr_eq_inc : + forall l i f, + remember_expr_inc f (map snd l) i = map snd (GiblePargen.remember_expr_inc f l i). +Proof. + unfold remember_expr_inc, GiblePargen.remember_expr_inc. + induction l; destruct i; cbn; intros; repeat destruct_match; auto. +Qed. + Lemma equiv_update'_top: forall i p f l lm p' f' l' lm', update_top (p, f, l, lm) i = Some (p', f', l', lm') -> @@ -73,6 +90,15 @@ Proof. inv Heqp1. inv H. repeat f_equal. apply remember_expr_eq. Qed. +Lemma equiv_update'_top_inc: + forall i p f l lm p' f' l' lm', + update_top_inc (p, f, l, lm) i = Some (p', f', l', lm') -> + update'_inc (p, f, map snd l, lm) i = Some (p', f', map snd l', lm'). +Proof. + intros. unfold update'_inc, update_top_inc, Option.bind2, Option.ret in *. repeat destr. + inv Heqp1. inv H. repeat f_equal. apply remember_expr_eq_inc. +Qed. + Lemma equiv_fold_update'_top: forall i p f l lm p' f' l' lm', mfold_left update_top i (Some (p, f, l, lm)) = Some (p', f', l', lm') -> @@ -86,6 +112,19 @@ Proof. intros. rewrite H0. eapply IHi. rewrite HB in H. eauto. Qed. +Lemma equiv_fold_update'_top_inc: + forall i p f l lm p' f' l' lm', + mfold_left update_top_inc i (Some (p, f, l, lm)) = Some (p', f', l', lm') -> + mfold_left update'_inc i (Some (p, f, map snd l, lm)) = Some (p', f', map snd l', lm'). +Proof. + induction i; cbn -[update_top_inc update'_inc] in *; intros. + - inv H; auto. + - exploit OptionExtra.mfold_left_Some; eauto; + intros [[[[p_mid f_mid] l_mid] lm_mid] HB]. + exploit equiv_update'_top_inc; try eassumption. + intros. rewrite H0. eapply IHi. rewrite HB in H. eauto. +Qed. + Lemma equiv_fold_update_top: forall i p f l lm p' f' l' lm', mfold_left update_top i (Some (p, f, l, lm)) = Some (p', f', l', lm') -> @@ -99,6 +138,19 @@ Proof. intros. rewrite H0. eapply IHi. rewrite HB in H. eauto. Qed. +Lemma equiv_fold_update_top_inc: + forall i p f l lm p' f' l' lm', + mfold_left update_top_inc 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_top_inc update] in *; intros. + - inv H; auto. + - exploit OptionExtra.mfold_left_Some; eauto; + intros [[[[p_mid f_mid] l_mid] lm_mid] HB]. + exploit equiv_update_top_inc; try eassumption. + intros. rewrite H0. eapply IHi. rewrite HB in H. eauto. +Qed. + Lemma top_implies_abstract_sequence : forall y f l1 l2, abstract_sequence_top y = Some (f, l1, l2) -> @@ -111,6 +163,18 @@ Proof. erewrite equiv_fold_update_top by eauto. auto. Qed. +Lemma top_implies_abstract_sequence_inc : + forall y f l1 l2, + abstract_sequence_top_inc y = Some (f, l1, l2) -> + abstract_sequence y = Some f. +Proof. + unfold abstract_sequence, abstract_sequence_top_inc; intros. + unfold Option.bind in *. repeat destr. + inv H. + unfold Option.map in *|-. repeat destr. subst. inv Heqo. + erewrite equiv_fold_update_top_inc by eauto. auto. +Qed. + Lemma top_implies_abstract_sequence' : forall y f l1 l2, abstract_sequence_top y = Some (f, l1, l2) -> @@ -124,6 +188,19 @@ Proof. setoid_rewrite H. cbn. setoid_rewrite Heqm. auto. Qed. +Lemma top_implies_abstract_sequence'_inc : + forall y f l1 l2, + abstract_sequence_top_inc y = Some (f, l1, l2) -> + abstract_sequence'_inc y = Some (f, map snd l1, l2). +Proof. + unfold abstract_sequence'_inc, abstract_sequence_top_inc; intros. + unfold Option.bind in *|-. repeat destr. + inv H. + unfold Option.map in *|-. repeat destr. subst. inv Heqo. + exploit equiv_fold_update'_top_inc; eauto; intros. + setoid_rewrite H. cbn. setoid_rewrite Heqm. auto. +Qed. + Definition state_lessdef := GiblePargenproofEquiv.match_states. Definition match_prog (prog : GibleSeq.program) (tprog : GiblePar.program) := @@ -537,6 +614,30 @@ it states that we can execute the forest. eapply NE.Forall_forall in HFRL; eauto. Qed. + Lemma eval_forest_gather_predicates_fold_inc : + forall G A B a_sem i0 sp ge x p f p' f' pe pe_val preds preds' l l_m l' l_m', + OptionExtra.mfold_left update_top_inc x (Some (p, f, l, l_m)) = Some (p', f', l', l_m') -> + OptionExtra.mfold_left gather_predicates x (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) -> preds ! pred = Some tt) pe -> + sem_pred_expr f'.(forest_preds) a_sem (mk_ctx i0 sp ge) pe pe_val. + Proof. + induction x. + - intros * HF; cbn in *. now inv HF. + - intros * HFOLD1 HFOLD2 HSEM HFRL. + cbn -[update] in *. + exploit OptionExtra.mfold_left_Some. eapply HFOLD1. + intros [[[[p_mid f_mid] l_mid] l_m_mid] HSTATE]. + rewrite HSTATE in HFOLD1. + exploit OptionExtra.mfold_left_Some. eapply HFOLD2. + intros [preds_mid HPRED]. rewrite HPRED in HFOLD2. + unfold Option.bind2, Option.ret in HSTATE; repeat destr; subst. inv HSTATE. + eapply IHx; eauto using eval_forest_gather_predicates. + eapply NE.Forall_forall; intros. + eapply gather_predicates_in; eauto. + eapply NE.Forall_forall in HFRL; eauto. + Qed. + Lemma abstract_sequence_evaluable_fold2 : forall x sp i i' i0 cf p f l l_m p' f' l' l_m' preds preds', sem (mk_ctx i0 sp ge) f (i, Some cf) -> @@ -648,6 +749,126 @@ it states that we can execute the forest. gather_predicates_in_forest, gather_predicates_update_constant. Qed. + Opaque app_predicated. + + Lemma abstract_sequence_evaluable_fold2_inc : + forall x sp i i' i0 cf p f l l_m p' f' l' l_m' preds preds', + sem (mk_ctx i0 sp ge) f (i, Some cf) -> + sem (mk_ctx i0 sp ge) f' (i', Some cf) -> + eval_predf (is_ps i) p = false -> + mfold_left gather_predicates x (Some preds) = Some preds' -> + all_preds_in f preds -> + (forall in_pred : Predicate.predicate, PredIn in_pred p -> preds ! in_pred = Some tt) -> + OptionExtra.mfold_left update_top_inc x (Some (p, f, l, l_m)) = Some (p', f', l', l_m') -> + evaluable_pred_list (mk_ctx i0 sp ge) f'.(forest_preds) (map snd l) -> + evaluable_pred_list (mk_ctx i0 sp ge) f'.(forest_preds) (map snd l'). + Proof. + induction x; intros * HSEM HSEM2 HPRED HGATHER HALL HPIN **. + - inv H. auto. + - exploit abstr_fold_falsy. apply HSEM. + eapply equiv_fold_update_top_inc; eauto. eauto. intros HSEM3. cbn -[update] in *. exploit OptionExtra.mfold_left_Some. eassumption. + intros [[[[p_mid f_mid] l_mid] l_m_mid] HBIND]. + rewrite HBIND in H. unfold Option.bind2, Option.ret in HBIND; repeat destr; subst. + inv HBIND. + exploit OptionExtra.mfold_left_Some. eapply HGATHER. + intros [preds_mid HGATHER0]. rewrite HGATHER0 in HGATHER. + unfold evaluable_pred_list in *; intros. + eapply IHx. 7: { eauto. } + + eapply abstr_fold_falsy. eapply HSEM. instantiate (3 := (a :: nil)). + cbn -[update]. eauto. auto. + + eauto. + + destruct i. eapply sem_update_falsy_input; eauto. + + eauto. + + eapply gather_predicates_in_forest; eauto. + + eapply gather_predicates_update_constant; eauto. + + intros. + { destruct a; cbn -[gather_predicates update seq_app remember_expr_inc remember_expr_m_inc] in *; eauto. + - inv H2; eauto. exists (is_rs i0)!!1. inv HSEM3. inv H5. + eapply AbstrSemIdent.sem_pred_expr_app_predicated_false. repeat constructor. eauto. + rewrite eval_predf_Pand. cbn in *. rewrite HPRED. auto with bool. + - inv H2; eauto. exists (is_rs i0)!!1. inv HSEM3. inv H5. + eapply AbstrSemIdent.sem_pred_expr_app_predicated_false. repeat constructor. eauto. + rewrite eval_predf_Pand. cbn in *. rewrite HPRED. auto with bool. + } + + eauto. + Qed. + + Lemma abstract_sequence_evaluable_fold_inc : + forall x sp i i' ti' i0 cf p f l l_m p' f' l' l_m' preds preds', + SeqBB.step ge sp (Iexec i) x (Iterm ti' cf) -> + state_lessdef i' ti' -> + sem (mk_ctx i0 sp ge) f (i, None) -> + sem (mk_ctx i0 sp ge) f' (i', Some cf) -> + eval_predf (is_ps i) p = true -> + GiblePargenproofCommon.valid_mem (is_mem i0) (is_mem i) -> + mfold_left gather_predicates x (Some preds) = Some preds' -> + all_preds_in f preds -> + (forall in_pred : Predicate.predicate, PredIn in_pred p -> preds ! in_pred = Some tt) -> + OptionExtra.mfold_left update_top_inc x (Some (p, f, l, l_m)) = Some (p', f', l', l_m') -> + evaluable_pred_list (mk_ctx i0 sp ge) f'.(forest_preds) (map snd l) -> + evaluable_pred_list (mk_ctx i0 sp ge) f'.(forest_preds) (map snd l'). + Proof. + induction x; cbn -[update seq_app remember_expr_inc remember_expr_m_inc]; intros * ? HLESSDEF HSEM HSEM2 HPRED HVALID_MEM HGATHER HALL HPREDALL **. + - inv H0. auto. + - exploit OptionExtra.mfold_left_Some. eassumption. + intros [[[[p_mid f_mid] l_mid] l_m_mid] HBIND]. + rewrite HBIND in H0. unfold Option.bind2, Option.ret in HBIND; repeat destr; subst. + inv HBIND. + exploit OptionExtra.mfold_left_Some. eapply HGATHER. + intros [preds_mid HGATHER0]. rewrite HGATHER0 in HGATHER. + inv H. + + unfold evaluable_pred_list; intros. exploit IHx. + eauto. eauto. eapply sem_update_instr; eauto. + eauto. eapply eval_predf_update_true; eauto. + transitivity (is_mem i); auto. eapply sem_update_valid_mem; eauto. + eauto. eapply gather_predicates_in_forest; eauto. eapply gather_predicates_update_constant; eauto. + eauto. unfold evaluable_pred_list in *; intros. + { destruct a; cbn -[gather_predicates update seq_app remember_expr_inc remember_expr_m_inc] in *; eauto. + - inv H2; eauto. + exploit sem_update_instr; eauto. intros. inv H2. inv H5. specialize (H2 r). + inv HSEM. inv H8. + exploit gather_predicates_in_forest; eauto. instantiate (1:=Reg r). intros HPRED_IN. + unfold update, Option.bind in Heqo. destruct_match; try discriminate. inv Heqo. + rewrite forest_reg_gss in H2. + exploit eval_forest_gather_predicates_fold_inc. eauto. eauto. apply H2. + eapply NE.Forall_forall; intros. + eapply NE.Forall_forall in HPRED_IN; eauto. + rewrite forest_reg_gss. auto. intros HSEMEXEC. + inv HSEM2. inv H13. exploit AbstrSemIdent.sem_pred_expr_prune_predicated2. eauto. + apply HSEMEXEC. eassumption. + intros HSEM_APP. + case_eq (eval_predf pr'1 (dfltp o ∧ p_mid)); intros. + + exists rs'!!r. eapply AbstrSemIdent.sem_pred_expr_app_predicated; eauto. + eapply AbstrSemIdent.sem_pred_expr_app_predicated2; eauto. + + exists (is_rs i0)!!1. eapply AbstrSemIdent.sem_pred_expr_app_predicated_false; eauto. + repeat constructor. + - inv H2; eauto. + exploit sem_update_instr; eauto. intros. inv H2. inv H5. specialize (H2 r). + inv HSEM. inv H8. + exploit gather_predicates_in_forest; eauto. instantiate (1:=Reg r). intros HPRED_IN. + unfold update, Option.bind in Heqo. destruct_match; try discriminate. inv Heqo. + rewrite forest_reg_gss in H2. + exploit eval_forest_gather_predicates_fold_inc. eauto. eauto. apply H2. + eapply NE.Forall_forall; intros. + eapply NE.Forall_forall in HPRED_IN; eauto. + rewrite forest_reg_gss. auto. intros HSEMEXEC. + inv HSEM2. inv H13. exploit AbstrSemIdent.sem_pred_expr_prune_predicated2. eauto. + apply HSEMEXEC. eassumption. + intros HSEM_APP. + case_eq (eval_predf pr'1 (dfltp o ∧ p_mid)); intros. + + exists rs'!!r. eapply AbstrSemIdent.sem_pred_expr_app_predicated; eauto. + eapply AbstrSemIdent.sem_pred_expr_app_predicated2; eauto. + + exists (is_rs i0)!!1. eapply AbstrSemIdent.sem_pred_expr_app_predicated_false; eauto. + repeat constructor. + } + eauto. auto. + + unfold evaluable_pred_list in *; intros. + inversion H5; subst. + exploit sem_update_instr_term; eauto; intros [HSEM3 HEVAL_PRED]. + eapply abstract_sequence_evaluable_fold2_inc; eauto using + gather_predicates_in_forest, gather_predicates_update_constant. + Qed. + Lemma abstract_sequence_evaluable_fold2_m : forall x sp i i' i0 cf p f l l_m p' f' l' l_m' preds preds', sem (mk_ctx i0 sp ge) f (i, Some cf) -> @@ -741,6 +962,103 @@ it states that we can execute the forest. gather_predicates_in_forest, gather_predicates_update_constant. Qed. + Lemma abstract_sequence_evaluable_fold2_m_inc : + forall x sp i i' i0 cf p f l l_m p' f' l' l_m' preds preds', + sem (mk_ctx i0 sp ge) f (i, Some cf) -> + sem (mk_ctx i0 sp ge) f' (i', Some cf) -> + eval_predf (is_ps i) p = false -> + mfold_left gather_predicates x (Some preds) = Some preds' -> + all_preds_in f preds -> + (forall in_pred : Predicate.predicate, PredIn in_pred p -> preds ! in_pred = Some tt) -> + OptionExtra.mfold_left update_top_inc x (Some (p, f, l, l_m)) = Some (p', f', l', l_m') -> + evaluable_pred_list_m (mk_ctx i0 sp ge) f'.(forest_preds) l_m -> + evaluable_pred_list_m (mk_ctx i0 sp ge) f'.(forest_preds) l_m'. + Proof. + induction x; intros * HSEM HSEM2 HPRED HGATHER HALL HPIN **. + - inv H. auto. + - exploit abstr_fold_falsy. apply HSEM. + eapply equiv_fold_update_top_inc; eauto. eauto. intros HSEM3. cbn -[update] in *. exploit OptionExtra.mfold_left_Some. eassumption. + intros [[[[p_mid f_mid] l_mid] l_m_mid] HBIND]. + rewrite HBIND in H. unfold Option.bind2, Option.ret in HBIND; repeat destr; subst. + inv HBIND. + exploit OptionExtra.mfold_left_Some. eapply HGATHER. + intros [preds_mid HGATHER0]. rewrite HGATHER0 in HGATHER. + unfold evaluable_pred_list_m in *; intros. + eapply IHx. 7: { eauto. } + + eapply abstr_fold_falsy. eapply HSEM. instantiate (3 := (a :: nil)). + cbn -[update]. eauto. auto. + + eauto. + + destruct i. eapply sem_update_falsy_input; eauto. + + eauto. + + eapply gather_predicates_in_forest; eauto. + + eapply gather_predicates_update_constant; eauto. + + intros. + { destruct a; cbn -[gather_predicates update seq_app remember_expr_inc remember_expr_m_inc] in *; eauto. + - inv H2; eauto. exists (is_mem i0). inv HSEM3. inv H5. + eapply AbstrSemIdent.sem_pred_expr_app_predicated_false. repeat constructor. eauto. + rewrite eval_predf_Pand. cbn in *. rewrite HPRED. auto with bool. + } + + eauto. + Qed. + + Lemma abstract_sequence_evaluable_fold_m_inc : + forall x sp i i' ti' i0 cf p f l l_m p' f' l' l_m' preds preds', + SeqBB.step ge sp (Iexec i) x (Iterm ti' cf) -> + state_lessdef i' ti' -> + sem (mk_ctx i0 sp ge) f (i, None) -> + sem (mk_ctx i0 sp ge) f' (i', Some cf) -> + eval_predf (is_ps i) p = true -> + GiblePargenproofCommon.valid_mem (is_mem i0) (is_mem i) -> + mfold_left gather_predicates x (Some preds) = Some preds' -> + all_preds_in f preds -> + (forall in_pred : Predicate.predicate, PredIn in_pred p -> preds ! in_pred = Some tt) -> + OptionExtra.mfold_left update_top_inc x (Some (p, f, l, l_m)) = Some (p', f', l', l_m') -> + evaluable_pred_list_m (mk_ctx i0 sp ge) f'.(forest_preds) l_m -> + evaluable_pred_list_m (mk_ctx i0 sp ge) f'.(forest_preds) l_m'. + Proof. + induction x; cbn -[update seq_app remember_expr_inc remember_expr_m_inc]; intros * ? HLESSDEF HSEM HSEM2 HPRED HVALID_MEM HGATHER HALL HPREDALL **. + - inv H0. auto. + - exploit OptionExtra.mfold_left_Some. eassumption. + intros [[[[p_mid f_mid] l_mid] l_m_mid] HBIND]. + rewrite HBIND in H0. unfold Option.bind2, Option.ret in HBIND; repeat destr; subst. + inv HBIND. + exploit OptionExtra.mfold_left_Some. eapply HGATHER. + intros [preds_mid HGATHER0]. rewrite HGATHER0 in HGATHER. + inv H. + + unfold evaluable_pred_list_m; intros. exploit IHx. + eauto. eauto. eapply sem_update_instr; eauto. + eauto. eapply eval_predf_update_true; eauto. + transitivity (is_mem i); auto. eapply sem_update_valid_mem; eauto. + eauto. eapply gather_predicates_in_forest; eauto. eapply gather_predicates_update_constant; eauto. + eauto. unfold evaluable_pred_list_m in *; intros. + { destruct a; cbn -[gather_predicates update seq_app remember_expr_inc remember_expr_m_inc] in *; eauto. + - inv H2; eauto. + exploit sem_update_instr; eauto. intros. inv H2. inv H5. specialize (H2 r). + inv HSEM. inv H8. + exploit gather_predicates_in_forest; eauto. instantiate (1:=Mem). intros HPRED_IN. + unfold update, Option.bind in Heqo. destruct_match; try discriminate. inv Heqo. + rewrite forest_reg_gss in H11. + exploit eval_forest_gather_predicates_fold_inc. eauto. eauto. apply H11. + eapply NE.Forall_forall; intros. + eapply NE.Forall_forall in HPRED_IN; eauto. + rewrite forest_reg_gss. auto. intros HSEMEXEC. + inv HSEM2. inv H13. exploit AbstrSemIdent.sem_pred_expr_prune_predicated2. eauto. + apply HSEMEXEC. eassumption. + intros HSEM_APP. + case_eq (eval_predf pr'1 (dfltp o ∧ p_mid)); intros. + + exists m'. eapply AbstrSemIdent.sem_pred_expr_app_predicated; eauto. + eapply AbstrSemIdent.sem_pred_expr_app_predicated2; eauto. + + exists (is_mem i0). eapply AbstrSemIdent.sem_pred_expr_app_predicated_false; eauto. + repeat constructor. + } + eauto. auto. + + unfold evaluable_pred_list in *; intros. + inversion H5; subst. + exploit sem_update_instr_term; eauto; intros [HSEM3 HEVAL_PRED]. + eapply abstract_sequence_evaluable_fold2_m_inc; eauto using + gather_predicates_in_forest, gather_predicates_update_constant. + Qed. + (*| Proof sketch: If I can execute the list of instructions, then every single forest element that is added to the forest will be evaluable too. This then @@ -767,6 +1085,25 @@ have been evaluable. - cbn; unfold evaluable_pred_list; inversion 1. Qed. + Lemma abstract_sequence_evaluable_inc : + forall sp x i i' ti' cf f l0 l, + SeqBB.step ge sp (Iexec i) x (Iterm ti' cf) -> + state_lessdef i' ti' -> + sem {| ctx_is := i; ctx_sp := sp; ctx_ge := ge |} f (i', Some cf) -> + abstract_sequence_top_inc x = Some (f, l0, l) -> + evaluable_pred_list (mk_ctx i sp ge) f.(forest_preds) (map snd l0). + Proof. + intros * ? HLESSDEF **. unfold abstract_sequence_top_inc in *. + unfold Option.bind, Option.map in H1; repeat destr. + inv H1. inv Heqo. + eapply abstract_sequence_evaluable_fold_inc; eauto; auto. + - apply sem_empty. + - reflexivity. + - apply all_preds_in_empty. + - inversion 1. + - cbn; unfold evaluable_pred_list; inversion 1. + Qed. + Lemma abstract_sequence_evaluable_m : forall sp x i i' ti' cf f l0 l, SeqBB.step ge sp (Iexec i) x (Iterm ti' cf) -> @@ -786,6 +1123,25 @@ have been evaluable. - cbn; unfold evaluable_pred_list; inversion 1. Qed. + Lemma abstract_sequence_evaluable_m_inc : + forall sp x i i' ti' cf f l0 l, + SeqBB.step ge sp (Iexec i) x (Iterm ti' cf) -> + state_lessdef i' ti' -> + sem {| ctx_is := i; ctx_sp := sp; ctx_ge := ge |} f (i', Some cf) -> + abstract_sequence_top_inc x = Some (f, l0, l) -> + evaluable_pred_list_m (mk_ctx i sp ge) f.(forest_preds) l. + Proof. + intros * ? HLESSDEF **. unfold abstract_sequence_top_inc in *. + unfold Option.bind, Option.map in H1; repeat destr. + inv H1. inv Heqo. + eapply abstract_sequence_evaluable_fold_m_inc; eauto; auto. + - apply sem_empty. + - reflexivity. + - apply all_preds_in_empty. + - inversion 1. + - cbn; unfold evaluable_pred_list; inversion 1. + Qed. + Lemma check_evaluability1_evaluable : forall G (ctx: @Abstr.ctx G) l1 l2 f ps, (forall x : positive, sem_pexpr ctx (get_forest_p' x f) ps !! x) -> @@ -936,6 +1292,50 @@ have been evaluable. etransitivity; eauto. Qed. + Lemma schedule_oracle_correct_inc: + forall x y sp i i' ti cf, + schedule_oracle_inc x y = true -> + SeqBB.step ge sp (Iexec i) x (Iterm i' cf) -> + state_lessdef i ti -> + exists ti', ParBB.step tge sp (Iexec ti) y (Iterm ti' cf) + /\ state_lessdef i' ti'. + Proof. + unfold schedule_oracle_inc; intros. repeat (destruct_match; try discriminate). simplify. + exploit top_implies_abstract_sequence_inc; [eapply Heqo|]; intros. + exploit top_implies_abstract_sequence'_inc; eauto; intros. + exploit abstr_sequence_correct; eauto; simplify. + exploit local_abstr_check_correct2; eauto. + { constructor. eapply ge_preserved_refl. reflexivity. } +(* { inv H. inv H8. exists pr'. intros x0. specialize (H x0). auto. } *) + simplify. + exploit abstr_seq_reverse_correct_inc; eauto. + { inv H8. inv H14. + eapply check_evaluability1_evaluable. + eauto. eauto. + eapply evaluable_same_preds. unfold check in *. simplify. eauto. + eapply evaluable_same_state; eauto. + eapply abstract_sequence_evaluable_inc. eauto. symmetry; eauto. + eapply sem_correct; eauto. + { constructor. constructor; auto. symmetry; auto. } + eauto. + } + { inv H8. inv H14. + eapply check_evaluability2_evaluable. + eauto. eauto. + eapply evaluable_same_preds_m. unfold check in *. simplify. eauto. + eapply evaluable_same_state_m; eauto. + eapply abstract_sequence_evaluable_m_inc. eauto. symmetry; eauto. + eapply sem_correct; eauto. + { constructor. constructor; auto. symmetry; auto. } + eauto. + } + reflexivity. simplify. + exploit seqbb_step_parbb_step; eauto; intros. + econstructor; split; eauto. + etransitivity; eauto. + etransitivity; eauto. + Qed. + Lemma step_cf_correct : forall cf ts s s' t, GibleSeq.step_cf_instr ge s cf t s' -> diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v index 43e97a6..659a683 100644 --- a/src/hls/GiblePargenproofBackward.v +++ b/src/hls/GiblePargenproofBackward.v @@ -76,16 +76,42 @@ Definition remember_expr (f : forest) (lst: list pred_expr) (i : instr): list pr | RBexit p c => lst end. +Definition remember_expr_inc (fop : pred_op * forest) (lst: list pred_expr) (i : instr): list pred_expr := + let (pred, f) := fop in + match i with + | RBnop => lst + | RBop p op rl r => (app_predicated (dfltp p ∧ pred) (NE.singleton (Ptrue, Ebase (Reg 1))) ( + (seq_app (pred_ret (Eop op)) (merge (list_translation rl f))))) :: lst + | RBload p chunk addr rl r => (app_predicated (dfltp p ∧ pred) (NE.singleton (Ptrue, Ebase (Reg 1))) ( + (seq_app + (seq_app (pred_ret (Eload chunk addr)) + (merge (list_translation rl f))) + (f #r Mem)))) :: lst + | RBstore p chunk addr rl r => 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 update'_inc (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_inc (p, f) l i, remember_expr_m_inc (p, f) lm i)) (update (p, f) i). + 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 abstract_sequence'_inc (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'_inc b (Some (Ptrue, empty, nil, nil)))). + Section CORRECTNESS. Context (prog: GibleSeq.program) (tprog : GiblePar.program). @@ -106,6 +132,19 @@ Proof. eapply IHi; eauto. Qed. +Lemma equiv_update_inc: + forall i p f l lm p' f' l' lm', + mfold_left update'_inc 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. + Lemma equiv_update1: forall i p f l lm p' f' l' lm', update' (p, f, l, lm) i = Some (p', f', l', lm') -> @@ -115,6 +154,15 @@ Proof. now inv H. Qed. +Lemma equiv_update1_inc: + forall i p f l lm p' f' l' lm', + update'_inc (p, f, l, lm) i = Some (p', f', l', lm') -> + update (p, f) i = Some (p', f'). +Proof. + intros. unfold update'_inc, Option.bind2, Option.ret in *. repeat destr. + now inv H. +Qed. + Lemma equiv_update1'': forall i p f l lm p' f' l' lm' lp lp', update'' (p, f, l, lm, lp) i = Some (p', f', l', lm', lp') -> @@ -148,6 +196,18 @@ Definition evaluable_pred_expr {G} (ctx: @Abstr.ctx G) pr p := Definition evaluable_pred_expr_m {G} (ctx: @Abstr.ctx G) pr p := exists r, sem_pred_expr pr sem_mem ctx p r. +Definition cond_evaluable_pred_expr {G} (ctx: @Abstr.ctx G) pr ps cond p := + eval_predf ps cond = true -> + exists r, sem_pred_expr pr sem_value ctx p r. + +Definition cond_evaluable_pred_expr_m {G} (ctx: @Abstr.ctx G) pr ps cond p := + eval_predf ps cond = true -> + exists r, sem_pred_expr pr sem_mem ctx p r. + +Definition evaluable_forest {G} (ctx: @Abstr.ctx G) pr f := + (forall x, evaluable_pred_expr ctx pr (f #r (Reg x))) + /\ evaluable_pred_expr_m ctx pr (f #r Mem). + Definition evaluable_pred_list {G} ctx pr l := forall p, In p l -> @@ -472,11 +532,25 @@ Proof. unfold remember_expr; destruct a; eauto using in_cons. Qed. +Lemma remember_expr_in_inc : + forall x l f a, + In x l -> In x (remember_expr_inc f l a). +Proof. + unfold remember_expr_inc; destruct a; repeat destruct_match; 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. + unfold remember_expr_m; destruct a; eauto using in_cons. +Qed. + +Lemma remember_expr_in_m_inc : + forall x l f a, + In x l -> In x (remember_expr_m_inc f l a). +Proof. + unfold remember_expr_m_inc; destruct a; repeat destruct_match; eauto using in_cons. Qed. Lemma in_mfold_left_abstr : @@ -495,6 +569,22 @@ Proof. auto using remember_expr_in. Qed. +Lemma in_mfold_left_abstr_inc : + forall instrs p f l p' f' l' x lm lm', + mfold_left update'_inc instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> + In x l -> In x l'. +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. + destruct a; auto; apply in_cons; auto. +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') -> @@ -511,6 +601,22 @@ Proof. auto using remember_expr_in_m. Qed. +Lemma in_mfold_left_abstr_m_inc: + forall instrs p f l p' f' l' x lm lm', + mfold_left update'_inc 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 remember_expr_inc remember_expr_m_inc] 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.bind, Option.bind2, Option.ret in *; repeat destr. inv H1. + destruct a; auto. apply in_cons; auto. +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) -> @@ -615,6 +721,34 @@ Proof. unfold evaluable_pred_expr_m. eauto. Qed. +(* Lemma in_forest_evaluable_inc : *) +(* forall G sp ge i' cf instrs p f l p' f' l' x i0 lm lm', *) +(* mfold_left update'_inc 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)). *) +(* 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. *) + +(* Lemma in_forest_evaluable_m_inc : *) +(* forall G sp ge i' cf instrs p f l p' f' l' i0 lm lm', *) +(* mfold_left update'_inc 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. *) + Definition pe_preds_in {A} (x: predicated A) preds := NE.Forall (fun x => forall pred, PredIn pred (fst x) -> PTree.get pred preds = Some tt) x. @@ -1346,6 +1480,20 @@ Proof. eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3''; eauto. Qed. +Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval3'_inc : + forall A B G a_sem instrs p f p' f' i0 sp ge preds preds' pe pe_val l l' lm lm', + update'_inc (p, f, l, lm) instrs = Some (p', f', l', lm') -> + gather_predicates preds instrs = 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) -> preds ! pred = Some tt) pe -> + sem_pred_expr f.(forest_preds) a_sem (mk_ctx i0 sp ge) pe pe_val. +Proof. + intros. + unfold update'_inc, Option.bind2, Option.ret in H; repeat destr. + inversion H; subst. + eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3''; eauto. +Qed. + 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 lm lm', mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> @@ -1369,6 +1517,29 @@ Proof. eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3'; eauto. Qed. +Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval3_inc : + 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'_inc 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) -> preds ! pred = Some tt) pe -> + sem_pred_expr f.(forest_preds) a_sem (mk_ctx i0 sp ge) pe pe_val. +Proof. + induction instrs; [crush|]. + intros. cbn -[update remember_expr_inc remember_expr_m_inc] in H,H0. + exploit OptionExtra.mfold_left_Some. eapply 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; eauto. + apply NE.Forall_forall. intros [p_op aval] YIN ypred YPREDIN. + apply NE.Forall_forall with (x:=(p_op, aval)) in H2; auto. cbn [fst snd] in *. + specialize (H2 ypred YPREDIN). + eapply gather_predicates_in; eassumption. + intros HSEM. + eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3'_inc; eauto. +Qed. + Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval2 : 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') -> @@ -1383,6 +1554,20 @@ Proof. eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3; eauto. Qed. +Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval2_inc : + forall G instrs p f l p' f' l' i0 sp ge preds preds' pe lm lm', + mfold_left update'_inc 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) + -> PTree.get pred preds = Some tt) pe -> + evaluable_pred_expr (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_inc; 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') -> @@ -1397,6 +1582,20 @@ Proof. eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3; eauto. Qed. +Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval4_inc : + forall G instrs p f l p' f' l' i0 sp ge preds preds' pe lm lm', + mfold_left update'_inc 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_inc; 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. @@ -1419,6 +1618,24 @@ Proof. unfold Option.bind2, Option.ret in *. repeat destr. inv Heqp1. inv HBIND. eauto. Qed. +Lemma abstr_seq_revers_correct_fold_sem_pexpr_inc : + forall instrs p f l p' f' l' preds preds' lm lm', + mfold_left update'_inc 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. + induction instrs; try solve [crush]. + intros. cbn -[update] in *. + exploit OptionExtra.mfold_left_Some. apply H. intros [[[[p_mid f_mid] l_mid] lm_mid] HBIND]. + exploit OptionExtra.mfold_left_Some. apply H0. intros [ptree_mid HGATHER]. + rewrite HBIND in H. rewrite HGATHER in H0. + exploit IHinstrs; eauto. eapply gather_predicates_in; eauto. + intros. rewrite <- H2. + unfold "#p". unfold get_forest_p'. erewrite abstr_seq_revers_correct_fold_sem_pexpr_sem2; eauto. + unfold Option.bind2, Option.ret in *. repeat destr. inv Heqp1. inv HBIND. eauto. +Qed. + (*| This lemma states that predicates are always evaluable, given that the output forest is also evaluable. This is true because gather_predicates ensures that @@ -1482,6 +1699,60 @@ Proof. eauto. inv H1; eauto. Qed. +Lemma update_rev_gather_constant_inc: + forall G i preds i0 sp ge f p l lm p' f' l' lm' preds' ps, + (forall p, preds ! p = None -> @sem_pexpr G (mk_ctx i0 sp ge) (f #p p) (ps !! p)) -> + update'_inc (p, f, l, lm) i = Some (p', f', l', lm') -> + gather_predicates preds i = Some preds' -> + (forall p, preds' ! p = None -> sem_pexpr (mk_ctx i0 sp ge) (f' #p p) (ps !! p)). +Proof. + unfold update'_inc, gather_predicates; destruct i; intros; unfold Option.bind, Option.bind2, Option.ret in *; + repeat destr. + - inv H0. inv H1. inv Heqo. eauto. + - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *; + repeat destr; inv Heqo1; inv H4. destruct o. inv H1. eapply gather_predicates_fold3 in H2. eauto. inv H1; eauto. + - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *; + repeat destr; inv Heqo1; inv H4. inv Heqo0. destruct o. inv H1. eapply gather_predicates_fold3 in H2. + eauto. inv H1; eauto. + - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *; + repeat destr; inv Heqo1; inv H4. inv Heqo0. destruct o. inv H1. eapply gather_predicates_fold3 in H2. + eauto. inv H1; eauto. + - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *. repeat destr. inv Heqo1. inv H4. + destruct (peq p1 p); subst. inv H1. rewrite PTree.gss in H2. discriminate. + rewrite forest_pred_gso by auto. inv H1. rewrite PTree.gso in H2 by auto. + destruct o. eapply gather_predicates_fold3 in H2. eauto. eauto. + - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *; + repeat destr; inv Heqo1; inv H4. inv Heqo0. destruct o. inv H1. eapply gather_predicates_fold3 in H2. + eauto. inv H1; eauto. +Qed. + +Lemma update_rev_gather_constant2_inc: + forall G i preds i0 sp ge f p l lm p' f' l' lm' preds' ps, + (forall p, preds ! p = None -> @sem_pexpr G (mk_ctx i0 sp ge) (f #p p) ps) -> + update'_inc (p, f, l, lm) i = Some (p', f', l', lm') -> + gather_predicates preds i = Some preds' -> + (forall p, preds' ! p = None -> sem_pexpr (mk_ctx i0 sp ge) (f' #p p) ps). +Proof. + unfold update'_inc, gather_predicates; destruct i; intros; unfold Option.bind, Option.bind2, Option.ret in *; + repeat destr. + - inv H0. inv H1. inv Heqo. eauto. + - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *; + repeat destr; inv Heqo1; inv H4. destruct o. inv H1. eapply gather_predicates_fold3 in H2. eauto. inv H1; eauto. + - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *; + repeat destr; inv Heqo1; inv H4. inv Heqo0. destruct o. inv H1. eapply gather_predicates_fold3 in H2. + eauto. inv H1; eauto. + - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *; + repeat destr; inv Heqo1; inv H4. inv Heqo0. destruct o. inv H1. eapply gather_predicates_fold3 in H2. + eauto. inv H1; eauto. + - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *. repeat destr. inv Heqo1. inv H4. + destruct (peq p1 p); subst. inv H1. rewrite PTree.gss in H2. discriminate. + rewrite forest_pred_gso by auto. inv H1. rewrite PTree.gso in H2 by auto. + destruct o. eapply gather_predicates_fold3 in H2. eauto. eauto. + - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *; + repeat destr; inv Heqo1; inv H4. inv Heqo0. destruct o. inv H1. eapply gather_predicates_fold3 in H2. + eauto. inv H1; eauto. +Qed. + Definition PMapmap {A} (f: positive -> A -> A) (m: PMap.t A): PMap.t A := (fst m, PTree.map f (snd m)). @@ -1607,6 +1878,57 @@ Proof. econstructor. constructor; eauto. Qed. +Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval_inc : + forall G instrs p f l p' f' l' i0 sp ge preds preds' ps' lm lm', + (forall p, preds ! p = None -> sem_pexpr (mk_ctx i0 sp ge) (f #p p) ((is_ps i0) !! p)) -> + mfold_left update'_inc instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> + mfold_left gather_predicates instrs (Some preds) = Some preds' -> + sem_predset (@mk_ctx G i0 sp ge) f' ps' -> + exists ps, sem_predset (mk_ctx i0 sp ge) f ps. +Proof. + induction instrs. + - intros * YH **. cbn in *. inv H. inv H0. eauto. + - intros * YH **. cbn -[update remember_expr_inc remember_expr_m_inc] in *. + exploit OptionExtra.mfold_left_Some. apply H. intros [[[[p_mid f_mid] l_mid] lm_mid] HBIND]. + exploit OptionExtra.mfold_left_Some. apply H0. intros [ptree_mid HGATHER]. + rewrite HBIND in H. rewrite HGATHER in H0. + exploit IHinstrs. 3: { eauto. } 3: { eauto. } eapply update_rev_gather_constant_inc; eauto. + eauto. eauto. + intros [ps_mid HSEM_MID]. + (* destruct (preds ! p0) eqn:?. destruct u. eapply gather_predicates_in in HGATHER; eauto. *) + (* rewrite HGATHER in H2. discriminate. *) + unfold Option.bind2, Option.bind, Option.ret in *; repeat destr. inv HBIND. + destruct a; cbn in *. + + inv Heqo. inv HGATHER. eauto. + + unfold Option.bind2, Option.bind, Option.ret in *; repeat destr. + generalize dependent Heqo; repeat destr; intros Heqo; inv Heqo. + inv HSEM_MID. + econstructor. constructor; eauto. + + unfold Option.bind2, Option.bind, Option.ret in *; repeat destr. + generalize dependent Heqo; repeat destr; intros Heqo; inv Heqo. + inv HSEM_MID. + econstructor. constructor; eauto. + + unfold Option.bind2, Option.bind, Option.ret in *; repeat destr. + generalize dependent Heqo; repeat destr; intros Heqo; inv Heqo. + inv HSEM_MID. + econstructor. constructor; eauto. + + unfold Option.bind2, Option.bind, Option.ret in *; repeat destr. inv HGATHER. + generalize dependent Heqo; repeat destr; intros Heqo; inv Heqo. + exists (mask_pred_map preds (is_ps i0) ps_mid). + econstructor; intros. + destruct (peq x p0); subst. + * destruct o; [assert (YX: preds ! p0 = None) by (eapply gather_predicates_fold3; eauto)|]; + rewrite mask_pred_map_not_in_pred; auto. + * inv HSEM_MID. specialize (H2 x). rewrite forest_pred_gso in H2 by auto. + destruct (preds ! x) eqn:HDESTR. + -- destruct u3. now rewrite mask_pred_map_in_pred. + -- rewrite mask_pred_map_not_in_pred; auto. + + unfold Option.bind2, Option.bind, Option.ret in *; repeat destr. + generalize dependent Heqo; repeat destr; intros Heqo; inv Heqo. + inv HSEM_MID. + econstructor. constructor; eauto. +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 preds preds' lm lm' ps', @@ -1795,6 +2117,346 @@ Proof. Unshelve. all: exact nil. Qed. +Lemma eval_app_predicated : + forall G (ctx: @Abstr.ctx G) (a b: predicated expression) p f_p ps c, + (forall x0 : positive, sem_pexpr ctx (get_forest_p' x0 f_p) ps !! x0) -> + evaluable_pred_expr ctx f_p (app_predicated p c a) -> + evaluable_pred_expr ctx f_p b -> + evaluable_pred_expr ctx f_p (app_predicated p b a). +Proof. + intros * HPred HEvalR HEvalL. + inv HEvalR. inv HEvalL. + case_eq (eval_predf ps p); intros. + - exists x. apply sem_pred_expr_app_predicated with (ps:=ps); auto. + eapply sem_pred_expr_app_predicated2; eauto. + - exists x0. apply sem_pred_expr_app_predicated_false with (ps:=ps); auto. +Qed. + +Lemma eval_prune_predicated : + forall G (ctx: @Abstr.ctx G) (a b: predicated expression) f_p ps, + (forall x0 : positive, sem_pexpr ctx (get_forest_p' x0 f_p) ps !! x0) -> + prune_predicated a = Some b -> + evaluable_pred_expr ctx f_p a -> + evaluable_pred_expr ctx f_p b. +Proof. + intros * HPred Hprune HEval. inv HEval. + exists x. eapply sem_pred_expr_prune_predicated; eauto. +Qed. + +Lemma eval_app_predicated_m : + forall G (ctx: @Abstr.ctx G) (a b: predicated expression) p f_p ps c, + (forall x0 : positive, sem_pexpr ctx (get_forest_p' x0 f_p) ps !! x0) -> + evaluable_pred_expr_m ctx f_p (app_predicated p c a) -> + evaluable_pred_expr_m ctx f_p b -> + evaluable_pred_expr_m ctx f_p (app_predicated p b a). +Proof. + intros * HPred HEvalR HEvalL. + inv HEvalR. inv HEvalL. + case_eq (eval_predf ps p); intros. + - exists x. apply sem_pred_expr_app_predicated with (ps:=ps); auto. + eapply sem_pred_expr_app_predicated2; eauto. + - exists x0. apply sem_pred_expr_app_predicated_false with (ps:=ps); auto. +Qed. + +Lemma eval_prune_predicated_m : + forall G (ctx: @Abstr.ctx G) (a b: predicated expression) f_p ps, + (forall x0 : positive, sem_pexpr ctx (get_forest_p' x0 f_p) ps !! x0) -> + prune_predicated a = Some b -> + evaluable_pred_expr_m ctx f_p a -> + evaluable_pred_expr_m ctx f_p b. +Proof. + intros * HPred Hprune HEval. inv HEval. + exists x. eapply sem_pred_expr_prune_predicated; eauto. +Qed. + +Lemma eval_forest_update_inc : + forall sp i i0 p p' f f' l l' lm lm' f_p ps, + (forall x0 : positive, sem_pexpr (mk_ctx i0 sp ge) (get_forest_p' x0 f_p) ps !! x0) -> + update'_inc (p, f, l, lm) i = Some (p', f', l', lm') -> + evaluable_pred_list (mk_ctx i0 sp ge) f_p l' -> + evaluable_pred_list_m (mk_ctx i0 sp ge) f_p lm' -> + evaluable_forest (mk_ctx i0 sp ge) f_p f -> + evaluable_forest (mk_ctx i0 sp ge) f_p f'. +Proof. + destruct i; intros * Hpred **; cbn -[app_predicated seq_app] in *; unfold Option.ret, Option.bind2, Option.bind in *; repeat (destruct_match; try easy; []). + - inv H; auto. + - inv H. inv Heqo1. inv H2. + constructor. + 2: { + inv H3. exists x. rewrite forest_reg_gso by discriminate. auto. + } + intro x. destruct (peq x r); subst. + 2: { + rewrite forest_reg_gso; auto. unfold not; intros. inv H2. contradiction. + } + rewrite forest_reg_gss. + unfold evaluable_pred_list in *. + exploit eval_app_predicated. eauto. eapply H0. constructor. eauto. + eapply H. instantiate (1:=r). intros. + eapply eval_prune_predicated; eauto. + - inv H. inv Heqo0. inv H2. + constructor. + 2: { + inv H3. exists x. rewrite forest_reg_gso by discriminate. auto. + } + intro x. destruct (peq x r); subst. + 2: { + rewrite forest_reg_gso; auto. unfold not; intros. inv H2. contradiction. + } + rewrite forest_reg_gss. + unfold evaluable_pred_list in *. + exploit eval_app_predicated. eauto. eapply H0. constructor. eauto. + eapply H. instantiate (1:=r). intros. + eapply eval_prune_predicated; eauto. + - inv Heqo0. inv H. inv H2. + constructor; intros. + rewrite forest_reg_gso by discriminate. auto. + rewrite forest_reg_gss. + exploit eval_app_predicated_m. eauto. apply H1. constructor. eauto. + apply H3. + intros. eapply eval_prune_predicated_m; eauto. + - inv Heqo0. inv H. inv H2. constructor; intros; rewrite forest_pred_reg; eauto. + - inv Heqo0. inv H. inv H2. constructor; intros; rewrite forest_exit_regs; auto. +Qed. + +Lemma abstr_seq_reverse_correct_fold_inc : + forall sp instrs i0 i i' ti cf f' l p p' l' f preds preds' lm lm' ps', + (forall in_pred, PredIn in_pred p -> preds ! in_pred = Some tt) -> + (forall p : positive, preds ! p = None -> sem_pexpr (mk_ctx i0 sp ge) f #p p (is_ps i0) !! p) -> + 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'_inc 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_predset (mk_ctx i0 sp ge) f' ps' -> + sem (mk_ctx i0 sp ge) f' (i', Some cf) -> + state_lessdef i ti -> + evaluable_forest (mk_ctx i0 sp ge) f'.(forest_preds) f -> + exists ti', + SeqBB.step ge sp (Iexec ti) instrs (Iterm ti' cf) + /\ state_lessdef i' ti'. +Proof. + induction instrs; intros * YPREDSIN YPREDNONE YVALID YALL YEVAL Y3 Y YGATHER Y0 YEVALUABLE YSEM_FINAL Y1 Y2 HEval. + - 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 |}) + by reflexivity. + now eapply sem_det in X; [| exact Y1 | exact Y3 ]. + - cbn -[update'_inc] 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). + pose proof H as Hupdate'_inc. + unfold update'_inc, Option.bind2, Option.ret in H. repeat destr. + inv H. + + 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_inc; eauto. + (* unfold evaluable_pred_list in Y0. eapply in_forest_evaluable; eauto. *) + inv YSEM_FINAL. + eapply eval_forest_update_inc; eauto. + unfold evaluable_pred_list. intros. eapply Y0. + eapply in_mfold_left_abstr_inc; eauto. + unfold evaluable_pred_list_m. intros. eapply YEVALUABLE. + eapply in_mfold_left_abstr_m_inc; eauto. + eapply gather_predicates_in_forest in YALL; eauto. + unfold all_preds_in in 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. 6: { eauto. } eapply gather_predicates_update_constant; eauto. + eapply update_rev_gather_constant; eauto. + unfold update', Option.bind2, Option.ret. rewrite Heqo; auto. + 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. eauto. symmetry. + eapply state_lessdef_state_equiv; eauto. + inv YSEM_FINAL. eapply eval_forest_update_inc; eauto. + unfold evaluable_pred_list. intros. eapply Y0. + eapply in_mfold_left_abstr_inc; eauto. + unfold evaluable_pred_list_m. intros. eapply YEVALUABLE. + eapply in_mfold_left_abstr_m_inc; 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_inc; eauto. + inv YSEM_FINAL. + eapply eval_forest_update_inc; eauto. + unfold evaluable_pred_list. intros. eapply Y0. + eapply in_mfold_left_abstr_inc; eauto. + unfold evaluable_pred_list_m. intros. eapply YEVALUABLE. + eapply in_mfold_left_abstr_m_inc; eauto. + eapply gather_predicates_in_forest in YALL; eauto. + unfold all_preds_in in 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. 6: { eauto. } eapply gather_predicates_update_constant; eauto. + eapply update_rev_gather_constant; eauto. + unfold update', Option.bind2, Option.ret. rewrite Heqo; auto. + 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. eauto. symmetry. + eapply state_lessdef_state_equiv; eauto. + inv YSEM_FINAL. eapply eval_forest_update_inc; eauto. + unfold evaluable_pred_list. intros. eapply Y0. + eapply in_mfold_left_abstr_inc; eauto. + unfold evaluable_pred_list_m. intros. eapply YEVALUABLE. + eapply in_mfold_left_abstr_m_inc; 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_inc; eauto. + + inv YSEM_FINAL. + eapply eval_forest_update_inc; eauto. + unfold evaluable_pred_list. intros. eapply Y0. + eapply in_mfold_left_abstr_inc; eauto. + unfold evaluable_pred_list_m. intros. eapply YEVALUABLE. + eapply in_mfold_left_abstr_m_inc; eauto. + + eapply gather_predicates_in_forest in YALL; eauto. + unfold all_preds_in in 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. 6: { eauto. } eapply gather_predicates_update_constant; eauto. + eapply update_rev_gather_constant; eauto. + unfold update', Option.bind2, Option.ret. rewrite Heqo; auto. + 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. eauto. symmetry. + eapply state_lessdef_state_equiv; eauto. + + inv YSEM_FINAL. eapply eval_forest_update_inc; eauto. + unfold evaluable_pred_list. intros. eapply Y0. + eapply in_mfold_left_abstr_inc; eauto. + unfold evaluable_pred_list_m. intros. eapply YEVALUABLE. + eapply in_mfold_left_abstr_m_inc; eauto. + + intros [ti' [YHH HLD]]. + exists ti'; split; eauto. econstructor; eauto. + + exploit abstr_seq_revers_correct_fold_sem_pexpr_eval_inc. + 2: { eauto. } + eapply update_rev_gather_constant; eauto. + unfold update', Option.bind2, Option.ret. rewrite Heqo; auto. + eauto. + 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. + 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. 6: { eauto. } eapply gather_predicates_update_constant; eauto. + eapply update_rev_gather_constant; eauto. + unfold update', Option.bind2, Option.ret. rewrite Heqo; auto. + 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. eauto. symmetry. + eapply state_lessdef_state_equiv; eauto. + + inv YSEM_FINAL. eapply eval_forest_update_inc; eauto. + unfold evaluable_pred_list. intros. eapply Y0. + eapply in_mfold_left_abstr_inc; eauto. + unfold evaluable_pred_list_m. intros. eapply YEVALUABLE. + eapply in_mfold_left_abstr_m_inc; eauto. + + intros [ti' [YHH HLD]]. + exists ti'; split; eauto. econstructor; eauto. + + case_eq (eval_predf (is_ps i) (dfltp o)); intros. + * 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_inc; eauto. cbn. auto. + intros. eapply sem_det in Y1; eauto. inv Y1. inv H7. + eexists. split. constructor. eauto. transitivity i. + symmetry; auto. auto. reflexivity. + * exploit evaluable_pred_expr_exists_RBexit; eauto; intros 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. 6: { eauto. } eapply gather_predicates_update_constant; eauto. + eapply update_rev_gather_constant; eauto. + unfold update', Option.bind2, Option.ret. rewrite Heqo; auto. + 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. + + inv YSEM_FINAL. eapply eval_forest_update_inc; eauto. + unfold evaluable_pred_list. intros. eapply Y0. + eapply in_mfold_left_abstr_inc; eauto. + unfold evaluable_pred_list_m. intros. eapply YEVALUABLE. + eapply in_mfold_left_abstr_m_inc; eauto. + + intros [ti' [YHH HLD]]. + exists ti'; split; eauto. econstructor; eauto. + Unshelve. all: exact nil. +Qed. + Lemma sem_empty : forall G (ctx: @Abstr.ctx G), sem ctx empty (ctx_is ctx, None). @@ -1834,6 +2496,32 @@ Proof. intros; repeat constructor. Qed. +Lemma abstr_seq_reverse_correct_inc: + forall sp x i i' ti cf x' l lm, + abstract_sequence'_inc 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 (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. unfold abstract_sequence'_inc in H. + unfold Option.map, Option.bind in H. repeat destr. inv H. inv Heqo. + pose proof H2 as X. inv X. + eapply abstr_seq_reverse_correct_fold_inc; + try eassumption; try reflexivity; auto using sem_empty, all_preds_in_empty. + inversion 1. + intros; repeat constructor. + unfold evaluable_forest; split. + - intros. unfold "#r". cbn. rewrite RTree.gempty. + unfold evaluable_pred_expr. eexists. constructor. constructor. + constructor. + - intros. unfold "#r". cbn. rewrite RTree.gempty. + unfold evaluable_pred_expr_m. eexists. constructor. constructor. + constructor. +Qed. + (*| Proof Sketch: diff --git a/src/hls/PrintAbstr.ml b/src/hls/PrintAbstr.ml index e1341b1..857b89c 100644 --- a/src/hls/PrintAbstr.ml +++ b/src/hls/PrintAbstr.ml @@ -81,9 +81,22 @@ let print_forest_exit pp f = fprintf pp "------------------- Exit -------------------\n"; print_predicated_exit pp f +let print_evaluability_list pp = function + | [] -> () + | r -> (fprintf pp "------------------- Eval -------------------\n"; + fprintf pp "["; List.iter (fun x -> fprintf pp "%a = %a\n" res (fst x) print_predicated (snd x)) r; fprintf pp "]"; + ) + +let print_evaluability_list2 pp = function + | [] -> () + | r -> (fprintf pp "------------------- Eval2 -------------------\n"; + fprintf pp "["; List.iter (fun x -> fprintf pp "%a\n" print_predicated x) r; fprintf pp "]"; + ) + let print_forest pp f = fprintf pp "#############################################\n"; fprintf pp "%a\n%a\n%a\n" print_forest_regs f.forest_regs print_forest_preds f.forest_preds print_forest_exit f.forest_exit + -- cgit