From 78026c97881e4500fd3e46283f2e59e5e57973fb Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 21 May 2023 15:46:15 +0100 Subject: Add proofs about RBexit --- src/hls/GiblePargenproofBackward.v | 65 ++++++++++++++++++++++++++++++++++++-- 1 file changed, 63 insertions(+), 2 deletions(-) diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v index 911cd9b..3434eba 100644 --- a/src/hls/GiblePargenproofBackward.v +++ b/src/hls/GiblePargenproofBackward.v @@ -438,6 +438,27 @@ Proof. easy. Qed. +Lemma evaluable_pred_expr_exists_RBexit : + forall sp i ti p cf, + eval_predf (is_ps i) (dfltp p) = false -> + state_lessdef i ti -> + step_instr ge sp (Iexec ti) (RBexit p cf) (Iexec ti). +Proof. + intros. constructor. destruct p; [|now cbn in *]. + inv H0. constructor. erewrite <- eval_predf_pr_equiv; eauto. +Qed. + +Lemma evaluable_pred_expr_exists_RBexit2 : + forall sp i ti p cf, + eval_predf (is_ps i) (dfltp p) = true -> + state_lessdef i ti -> + step_instr ge sp (Iexec ti) (RBexit p cf) (Iterm ti cf). +Proof. + intros. econstructor. + inv H0. cbn. destruct p; try constructor. + erewrite <- eval_predf_pr_equiv; eauto. +Qed. + Lemma remember_expr_in : forall x l f a, In x l -> In x (remember_expr f l a). @@ -784,8 +805,48 @@ Proof. eapply state_lessdef_state_equiv; eauto. intros [ti' [YHH HLD]]. exists ti'; split; eauto. econstructor; eauto. - + admit. - + admit. + + exploit evaluable_pred_expr_exists_RBsetpred; eauto. admit. + 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. + + case_eq (eval_predf (is_ps i) (dfltp o)); intros. + * admit. + * exploit evaluable_pred_expr_exists_RBexit; eauto; intros HSTEP. + instantiate (1:=cf) 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. Lemma sem_empty : -- cgit