diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-05-19 18:11:53 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-19 18:11:53 +0100 |
commit | c79d1a9dcd5a1ac6bc10492380a77fafa780e7d6 (patch) | |
tree | 44a91ab0a55e6deffd98e7cd387a16a57759d73b /src | |
parent | 3be880b441a4d2926c6b14b7bb25a04209fbbca6 (diff) | |
download | vericert-c79d1a9dcd5a1ac6bc10492380a77fafa780e7d6.tar.gz vericert-c79d1a9dcd5a1ac6bc10492380a77fafa780e7d6.zip |
Prepare work on evaluability of instructions
Diffstat (limited to 'src')
-rw-r--r-- | src/hls/Gible.v | 111 | ||||
-rw-r--r-- | src/hls/GiblePargenproofBackward.v | 57 | ||||
-rw-r--r-- | src/hls/GiblePargenproofCommon.v | 36 |
3 files changed, 133 insertions, 71 deletions
diff --git a/src/hls/Gible.v b/src/hls/Gible.v index d04c78a..b7959be 100644 --- a/src/hls/Gible.v +++ b/src/hls/Gible.v @@ -265,18 +265,6 @@ Inductive eval_pred: | eval_pred_none: forall i i', eval_pred None i i' i'. -Section RELABSTR. - - Context {A B : Type} (ge : Genv.t A B). - -(*| -.. index:: - triple: semantics; RTLBlockInstr; instruction - -Step Instruction -============================= -|*) - Definition truthyb (ps: predset) (p: option pred_op) := match p with | None => true @@ -313,6 +301,77 @@ Variant instr_falsy (ps: predset): instr -> Prop := instr_falsy ps (RBexit (Some p) cf) . +Inductive state_equiv : instr_state -> instr_state -> Prop := +| match_states_intro: + forall ps ps' rs rs' m m', + (forall x, rs !! x = rs' !! x) -> + (forall x, ps !! x = ps' !! x) -> + m = m' -> + state_equiv (mk_instr_state rs ps m) (mk_instr_state rs' ps' m'). + +Lemma state_equiv_refl x : state_equiv x x. +Proof. destruct x; constructor; crush. Qed. + +Lemma state_equiv_commut x y : state_equiv x y -> state_equiv y x. +Proof. inversion 1; constructor; crush. Qed. + +Lemma state_equiv_trans x y z : + state_equiv x y -> state_equiv y z -> state_equiv x z. +Proof. repeat inversion 1; constructor; crush. Qed. + +#[global] Instance state_equiv_Equivalence : Equivalence state_equiv := + { Equivalence_Reflexive := state_equiv_refl ; + Equivalence_Symmetric := state_equiv_commut ; + Equivalence_Transitive := state_equiv_trans ; }. + +Lemma match_states_list : + forall A (rs: Regmap.t A) rs', + (forall r, rs !! r = rs' !! r) -> + forall l, rs ## l = rs' ## l. +Proof. induction l; crush. Qed. + +Lemma truthy_match_state : + forall ps ps' p, + (forall x, ps !! x = ps' !! x) -> + truthy ps p -> + truthy ps' p. +Proof. + intros; destruct p; inv H0; constructor; auto. + erewrite eval_predf_pr_equiv; eauto. +Qed. + +Lemma falsy_match_state : + forall ps ps' p, + (forall x, ps !! x = ps' !! x) -> + falsy ps p -> + falsy ps' p. +Proof. + intros; destruct p; inv H0; constructor; auto. + erewrite eval_predf_pr_equiv; eauto. +Qed. + +Lemma PTree_matches : + forall A (v: A) res rs rs', + (forall r, rs !! r = rs' !! r) -> + forall x, (Regmap.set res v rs) !! x = (Regmap.set res v rs') !! x. +Proof. + intros; destruct (Pos.eq_dec x res); subst; + [ repeat rewrite Regmap.gss by auto + | repeat rewrite Regmap.gso by auto ]; auto. +Qed. + +Section RELABSTR. + + Context {A B : Type} (ge : Genv.t A B). + +(*| +.. index:: + triple: semantics; RTLBlockInstr; instruction + +Step Instruction +============================= +|*) + Variant step_instr: val -> istate -> instr -> istate -> Prop := | exec_RBnop: forall sp ist, @@ -353,6 +412,34 @@ Variant step_instr: val -> istate -> instr -> istate -> Prop := step_instr sp (Iexec st) i (Iexec st) . +Lemma step_exists: + forall sp i instr i' ti, + step_instr sp (Iexec i) instr (Iexec i') -> + state_equiv i ti -> + exists ti', + step_instr sp (Iexec ti) instr (Iexec ti') + /\ state_equiv i' ti'. +Proof. + inversion_clear 1; subst; intros. + - econstructor; split; eauto. constructor. + - destruct ti; cbn in *. inv H. econstructor. split. + econstructor. erewrite match_states_list; eauto. + eapply truthy_match_state; eauto. constructor; auto. + eapply PTree_matches; auto. + - inv H; cbn in *. eexists; split. econstructor. + erewrite match_states_list; eauto. eauto. + eapply truthy_match_state; eauto. constructor; auto. + eapply PTree_matches; auto. + - inv H; cbn in *. eexists; split. econstructor. + erewrite match_states_list; eauto. rewrite <- H6. eauto. + eapply truthy_match_state; eauto. constructor; auto. + - inv H. econstructor. split. econstructor. erewrite match_states_list; eauto. + eapply truthy_match_state; eauto. constructor; auto. + eapply PTree_matches; auto. + - inv H0; exists ti; split; auto; + repeat constructor; inv H; erewrite eval_predf_pr_equiv; eauto. +Qed. + End RELABSTR. (*| diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v index db0df19..b4442a8 100644 --- a/src/hls/GiblePargenproofBackward.v +++ b/src/hls/GiblePargenproofBackward.v @@ -31,6 +31,7 @@ Require Import vericert.hls.GiblePar. Require Import vericert.hls.Gible. Require Import vericert.hls.GiblePargenproofEquiv. Require Import vericert.hls.GiblePargenproofCommon. +Require Import vericert.hls.GiblePargenproofForward. Require Import vericert.hls.GiblePargen. Require Import vericert.hls.Predicate. Require Import vericert.hls.Abstr. @@ -130,9 +131,8 @@ Definition evaluable_pred_list {G} ctx pr l := (* unfold evaluable_pred_expr in H1. Admitted. *) Lemma evaluable_pred_expr_exists : - 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 -> + forall sp f i0 exit_p exit_p' f' i ti p op args dst, + eval_predf (is_ps i) exit_p = true -> valid_mem (is_mem i0) (is_mem i) -> update (exit_p, f) (RBop p op args dst) = Some (exit_p', f') -> sem (mk_ctx i0 sp ge) f (i, None) -> @@ -141,19 +141,22 @@ Lemma evaluable_pred_expr_exists : exists ti', step_instr ge sp (Iexec ti) (RBop p op args dst) (Iexec ti'). Proof. - intros * HPRED HEVAL VALID_MEM **. cbn -[seq_app] in H. unfold Option.bind in H. destr. inv H. - destruct ti. + intros * HEVAL VALID_MEM **. cbn -[seq_app] in H. unfold Option.bind in H. destr. inv H. + assert (HPRED': sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f (is_ps i)) + by now inv H0. + inversion_clear HPRED' as [? ? ? HPRED]. + destruct ti as [is_trs is_tps is_tm]. 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. cbn in HPRED. - pose proof (truthy_dec pr p) as YH. inversion_clear YH as [YH'|YH']. - - assert (eval_predf pr (dfltp p ∧ exit_p') = true). + exploit sem_pred_expr_prune_predicated2; eauto; intros. + pose proof (truthy_dec (is_ps i) p) as YH. inversion_clear YH as [YH'|YH']. + - assert (eval_predf (is_ps i) (dfltp p ∧ exit_p') = true). { pose proof (truthy_dflt _ _ YH'). rewrite eval_predf_Pand. rewrite H1. now rewrite HEVAL. } 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. + destruct i as [is_rs_1 is_ps_1 is_m_1]. 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. @@ -164,18 +167,18 @@ Proof. + cbn in *. eapply eval_operation_valid_pointer. symmetry; eauto. unfold ctx_mem in H14. cbn in H14. erewrite <- match_states_list; eauto. + inv H0. - assert (sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f pr) + assert (sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f (is_ps_1)) by (now constructor). pose proof (sem_predset_det _ _ ltac:(reflexivity) _ _ _ H0 H17). - assert (truthy is_ps0 p). + assert (truthy is_ps_1 p). { eapply truthy_match_state; eassumption. } eapply truthy_match_state; eassumption. - inv YH'. cbn -[seq_app] in H. - assert (eval_predf pr (p0 ∧ exit_p') = false). + assert (eval_predf (is_ps i) (p0 ∧ exit_p') = false). { rewrite eval_predf_Pand. now rewrite H1. } eapply sem_pred_expr_app_predicated_false2 in H; eauto. eexists. eapply exec_RB_falsy. constructor. auto. cbn. - assert (sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f pr) + assert (sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f (is_ps i)) by (now constructor). inv H0. pose proof (sem_predset_det _ _ ltac:(reflexivity) _ _ _ H4 H8). inv H2. @@ -302,6 +305,8 @@ 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, + valid_mem (is_mem i0) (is_mem i) -> + eval_predf (is_ps i) p = true -> sem (mk_ctx i0 sp ge) f (i, None) -> mfold_left update' instrs (Some (p, f, l)) = Some (p', f', l') -> evaluable_pred_list (mk_ctx i0 sp ge) f'.(forest_preds) l' -> @@ -311,12 +316,12 @@ Lemma abstr_seq_reverse_correct_fold : SeqBB.step ge sp (Iexec ti) instrs (Iterm ti' cf) /\ state_lessdef i' ti'. Proof. - induction instrs; intros * Y3 Y Y0 Y1 Y2. + induction instrs; intros * YVALID YEVAL Y3 Y Y0 Y1 Y2. - cbn in *. inv Y. - assert (similar {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} - {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |}) + 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 H; [| eapply Y1 | eapply Y3 ]. + now eapply sem_det in X; [| exact Y1 | exact Y3 ]. - cbn -[update] in Y. pose proof Y as YX. apply OptionExtra.mfold_left_Some in YX. inv YX. @@ -330,18 +335,24 @@ Proof. by admit; destruct H as (pred & op & args & dst & EQ); subst a. exploit evaluable_pred_expr_exists; eauto. + (* I have the pred already from sem. *) - admit. admit. admit. intros [t step]. + intros [ti_mid HSTEP]. (* unfold evaluable_pred_list in Y0. *) (* instantiate (1 := forest_preds f'). *) (* eapply in_forest_evaluable; eauto. *) (* (* provable using evaluability in list *) intros [t step]. *) - exploit IHinstrs. 2: { eapply Y. } eauto. auto. eauto. reflexivity. - intros (ti_mid' & Hseq & Hstate). - assert (state_lessdef ti_mid t) by admit. - exists ti_mid'; split; auto. - econstructor; eauto. + 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. 3: { eauto. } admit. admit. eauto. admit. eauto. symmetry. + instantiate (1:=ti_mid). admit. intros [ti' [YHH HLD]]. + exists ti'; split; eauto. econstructor; eauto. Admitted. Lemma sem_empty : diff --git a/src/hls/GiblePargenproofCommon.v b/src/hls/GiblePargenproofCommon.v index 8d8e0a2..22b5978 100644 --- a/src/hls/GiblePargenproofCommon.v +++ b/src/hls/GiblePargenproofCommon.v @@ -221,44 +221,8 @@ Proof. unfold predicated_not_inP; intros. eapply H. econstructor. right; eauto. Qed. -Lemma match_states_list : - forall A (rs: Regmap.t A) rs', - (forall r, rs !! r = rs' !! r) -> - forall l, rs ## l = rs' ## l. -Proof. induction l; crush. Qed. - -Lemma PTree_matches : - forall A (v: A) res rs rs', - (forall r, rs !! r = rs' !! r) -> - forall x, (Regmap.set res v rs) !! x = (Regmap.set res v rs') !! x. -Proof. - intros; destruct (Pos.eq_dec x res); subst; - [ repeat rewrite Regmap.gss by auto - | repeat rewrite Regmap.gso by auto ]; auto. -Qed. - Lemma truthy_dec: forall ps a, truthy ps a \/ falsy ps a. Proof. destruct a; try case_eq (eval_predf ps p); intuition (constructor; auto). Qed. - -Lemma truthy_match_state : - forall ps ps' p, - (forall x, ps !! x = ps' !! x) -> - truthy ps p -> - truthy ps' p. -Proof. - intros; destruct p; inv H0; constructor; auto. - erewrite eval_predf_pr_equiv; eauto. -Qed. - -Lemma falsy_match_state : - forall ps ps' p, - (forall x, ps !! x = ps' !! x) -> - falsy ps p -> - falsy ps' p. -Proof. - intros; destruct p; inv H0; constructor; auto. - erewrite eval_predf_pr_equiv; eauto. -Qed. |