From 68895af33411978425f074587bbb95f8b86d83fd Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 26 Jul 2022 08:11:42 +0100 Subject: Update lemmas with new update function --- src/hls/GiblePargenproof.v | 163 +++++++++++++++++++++++++++++++++++---------- 1 file changed, 128 insertions(+), 35 deletions(-) (limited to 'src/hls/GiblePargenproof.v') diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index 68d14fa..2c677c3 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -1156,20 +1156,22 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. rewrite eval_predf_negate. rewrite H0. auto. Qed. -(* Lemma sem_update_instr : - forall f i' i'' a sp p i, + Lemma sem_update_instr : + forall f i' i'' a sp p i p' f', sem (mk_ctx i sp ge) f (i', None) -> step_instr ge sp (Iexec i') a (Iexec i'') -> - sem (mk_ctx i sp ge) (snd (update (p, f) a)) (i'', None). + update (Some (p, f)) a = Some (p', f') -> + sem (mk_ctx i sp ge) f' (i'', None). Proof. Admitted. Lemma sem_update_instr_term : - forall f i' i'' a sp i cf p p', + forall f i' i'' a sp i cf p p' p'' f', sem (mk_ctx i sp ge) f (i', None) -> step_instr ge sp (Iexec i') (RBexit p cf) (Iterm i'' cf) -> - sem (mk_ctx i sp ge) (snd (update (p', f) a)) (i'', Some cf) - /\ falsy (is_ps i'') (fst (update (p', f) a)). - Proof. Admitted.*) + update (Some (p', f)) a = Some (p'', f') -> + sem (mk_ctx i sp ge) f' (i'', Some cf) + /\ eval_apred (mk_ctx i sp ge) p'' false. + Proof. Admitted. Lemma step_instr_lessdef : forall sp a i i' ti, @@ -1225,28 +1227,98 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. constructor. auto. Qed. -(* Lemma falsy_update : - forall f a ps, - falsy ps (fst f) -> - falsy ps (fst (update f a)). + (* Inductive is_predicate_expr: expression -> Prop := *) + (* | is_predicate_expr_Epredset : *) + (* forall c a, is_predicate_expr (Esetpred c a) *) + (* | is_predicate_expr_Ebase : *) + (* forall p, is_predicate_expr (Ebase (Pred p)). *) + + (* Inductive apred_wf: apred_op -> Prop := *) + (* | apred_wf_Plit: forall b p, *) + (* is_predicate_expr p -> *) + (* apred_wf (Plit (b, p)) *) + (* | apred_wf_Ptrue: apred_wf Ptrue *) + (* | apred_wf_Pfalse: apred_wf Pfalse *) + (* | apred_wf_Pand: forall a b, *) + (* apred_wf a -> apred_wf b -> apred_wf (a ∧ b) *) + (* | apred_wf_Por: forall a b, *) + (* apred_wf a -> apred_wf b -> apred_wf (a ∨ b). *) + + Lemma apred_and_false1 : + forall A ctx a b c, + @eval_apred A ctx a false -> + @eval_apred A ctx b c -> + eval_apred ctx (a ∧ b) false. + Proof. + intros. + replace false with (false && c) by auto. + constructor; auto. + Qed. + + Lemma apred_and_false2 : + forall A ctx a b c, + @eval_apred A ctx a c -> + eval_apred ctx b false -> + eval_apred ctx (a ∧ b) false. Proof. - destruct f; destruct a; inversion 1; subst; crush. - rewrite <- H1. constructor. unfold Option.default. destruct o0. - rewrite eval_predf_Pand. rewrite H0. crush. crush. + intros. + replace false with (c && false) by eauto with bool. + constructor; auto. Qed. + #[local] Opaque simplify. + + Lemma apred_simplify: + forall A ctx a b, + @eval_apred A ctx a b -> + @eval_apred A ctx (simplify a) b. + Proof. Admitted. + + Lemma exists_get_pred_eval : + forall A ctx f p, + exists c, @eval_apred A ctx (get_pred' f p) c. + Proof. + induction p; crush; try solve [econstructor; constructor; eauto]. + destruct_match. inv Heqp0. econstructor. + unfold apredicated_to_apred_op. + Admitted. (*probably not provable.*) + + Lemma falsy_update : + forall A f a ctx p f', + @eval_apred A ctx (fst f) false -> + update (Some f) a = Some (p, f') -> + eval_apred ctx p false. + Proof. + destruct f; destruct a; inversion 1; subst; crush; + destruct_match; simplify; auto; + unfold Option.bind, Option.bind2 in *; + repeat (destruct_match; try discriminate; []); simplify; auto. + apply apred_simplify. eapply apred_and_false2; eauto. admit. + apply apred_simplify. eapply apred_and_false2; eauto. admit. + constructor; auto. + constructor; auto. + constructor; auto. + constructor; auto. + constructor; auto. + rewrite H2. + apply apred_simplify. eapply apred_and_false2; eauto. admit. + apply apred_simplify. eapply apred_and_false2; eauto. admit. + Unshelve. all: exact true. + Admitted. + Lemma abstr_fold_falsy : - forall x i0 sp cf i f, - sem (mk_ctx i0 sp ge) (snd f) (i, cf) -> - falsy (is_ps i) (fst f) -> - sem (mk_ctx i0 sp ge) (snd (fold_left update x f)) (i, cf). + forall x i0 sp cf i f p p' f', + sem (mk_ctx i0 sp ge) f (i, cf) -> + eval_apred (mk_ctx i0 sp ge) p false -> + fold_left update x (Some (p, f)) = Some (p', f') -> + sem (mk_ctx i0 sp ge) f' (i, cf). Proof. induction x; crush. eapply IHx. destruct a; destruct f; crush; try solve [eapply app_predicated_sem; eauto; apply combined_falsy; auto]. - now apply falsy_update. - Qed.*) + (* now apply falsy_update. *) + (* Qed. *) Admitted. Lemma state_lessdef_sem : forall i sp f i' ti cf, @@ -1255,25 +1327,43 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. exists ti', sem (mk_ctx ti sp ge) f (ti', cf) /\ state_lessdef i' ti'. Proof. Admitted. + Lemma update_Some : + forall x n y, + fold_left update x n = Some y -> + exists n', n = Some n'. + Proof. + induction x; crush. + econstructor; eauto. + exploit IHx; eauto; simplify. + unfold update, Option.bind2, Option.bind in H1. + repeat (destruct_match; try discriminate); econstructor; eauto. + Qed. + + #[local] Opaque update. + Lemma abstr_fold_correct : - forall sp x i i' i'' cf f f', + forall sp x i i' i'' cf f p f', SeqBB.step ge sp (Iexec i') x (Iterm i'' cf) -> sem (mk_ctx i sp ge) (snd f) (i', None) -> - fold_left update x (Some f) = Some f' -> + fold_left update x (Some f) = Some (p, f') -> forall ti, state_lessdef i ti -> - exists ti', sem (mk_ctx ti sp ge) (snd f') (ti', Some cf) + exists ti', sem (mk_ctx ti sp ge) f' (ti', Some cf) /\ state_lessdef i'' ti'. Proof. induction x; simplify; inv H. - (*- destruct f; exploit IHx; eauto; eapply sem_update_instr; eauto. - - destruct f. inversion H5; subst. - exploit state_lessdef_sem; eauto; intros. inv H. inv H2. - exploit step_instr_lessdef_term; eauto; intros. inv H2. inv H4. - exploit sem_update_instr_term; eauto; intros. inv H4. - eexists; split. eapply abstr_fold_falsy; eauto. - auto. - Qed.*) Admitted. + - destruct f. exploit update_Some; eauto; intros. simplify. + rewrite H3 in H1. destruct x0. + exploit IHx; eauto. eapply sem_update_instr; eauto. + - destruct f. + exploit state_lessdef_sem; eauto; intros. simplify. + exploit step_instr_lessdef_term; eauto; intros. simplify. + inv H6. exploit update_Some; eauto; simplify. destruct x2. + exploit sem_update_instr_term; eauto; simplify. + eexists; split. + eapply abstr_fold_falsy; eauto. + rewrite H6 in H1. eauto. auto. + Qed. Lemma sem_regset_empty : forall A ctx, @sem_regset A ctx empty (ctx_rs ctx). @@ -1309,9 +1399,12 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. exists ti', sem (mk_ctx ti sp ge) x' (ti', Some cf) /\ state_lessdef i'' ti'. Proof. - (*unfold abstract_sequence. intros; eapply abstr_fold_correct; eauto. + unfold abstract_sequence. intros. unfold Option.map in H0. + destruct_match; try easy. + destruct p; simplify. + eapply abstr_fold_correct; eauto. simplify. eapply sem_empty. - Qed.*) Admitted. + Qed. Lemma abstr_check_correct : forall sp i i' a b cf ti, @@ -1339,7 +1432,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. exists ti', ParBB.step tge sp (Iexec ti) y (Iterm ti' cf) /\ state_lessdef i' ti'. Proof. - (*unfold schedule_oracle; intros. simplify. + unfold schedule_oracle; intros. repeat (destruct_match; try discriminate). simplify. exploit abstr_sequence_correct; eauto; simplify. exploit abstr_check_correct; eauto. apply state_lessdef_refl. simplify. exploit abstr_seq_reverse_correct; eauto. apply state_lessdef_refl. simplify. @@ -1347,7 +1440,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. econstructor; split; eauto. etransitivity; eauto. etransitivity; eauto. - Qed.*) Admitted. + Qed. Lemma step_cf_correct : forall cf ts s s' t, -- cgit