From 3fce6f56c1aad7163972322d499a0f9e8d876bcf Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 5 Jun 2023 18:34:48 +0100 Subject: Work towards proving evaluability --- src/hls/GiblePargen.v | 36 +++++++++--- src/hls/GiblePargenproof.v | 115 ++++++++++++++++++++++++++++++++++++- src/hls/GiblePargenproofBackward.v | 56 +++++++++--------- 3 files changed, 169 insertions(+), 38 deletions(-) (limited to 'src') diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index 8e8c9b5..4b95cf2 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -289,11 +289,11 @@ Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest Some (new_p, f <-e pruned) end. -Definition remember_expr (f : forest) (lst: list pred_expr) (i : instr): list pred_expr := +Definition remember_expr (f : forest) (lst: list (resource * pred_expr)) (i : instr): list (resource * pred_expr) := match i with | RBnop => lst - | RBop p op rl r => (f #r (Reg r)) :: lst - | RBload p chunk addr rl r => (f #r (Reg r)) :: lst + | RBop p op rl r => (Reg r, f #r (Reg r)) :: lst + | RBload p chunk addr rl r => (Reg r, f #r (Reg r)) :: lst | RBstore p chunk addr rl r => lst | RBsetpred p' c args p => lst | RBexit p c => lst @@ -309,6 +309,11 @@ Definition remember_expr_m (f : forest) (lst: list pred_expr) (i : instr): list | RBexit p c => lst end. +(*| +Not actually needed, because there is a better way to show that a predicate is +evaluable. +|*) + Definition remember_expr_p (f : forest) (lst: list pred_op) (i : instr): list pred_op := match i with | RBnop => lst @@ -319,11 +324,11 @@ Definition remember_expr_p (f : forest) (lst: list pred_op) (i : instr): list pr | 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) := +Definition update_top (s: pred_op * forest * list (resource * pred_expr) * list pred_expr) (i: instr): option (pred_op * forest * list (resource * 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'' (s: pred_op * forest * list pred_expr * list pred_expr * list pred_op) (i: instr): option (pred_op * forest * list pred_expr * list pred_expr * list pred_op) := +Definition update'' (s: pred_op * forest * list (resource * pred_expr) * list pred_expr * list pred_op) (i: instr): option (pred_op * forest * list (resource * pred_expr) * list pred_expr * list pred_op) := let '(p, f, l, lm, lp) := s in Option.bind2 (fun p' f' => Option.ret (p', f', remember_expr f l i, remember_expr_m f lm i, remember_expr_p f lp i)) (update (p, f) i). @@ -347,11 +352,11 @@ Definition gather_predicates (preds : PTree.t unit) (i : instr): option (PTree.t | _ => Some preds end. -Definition abstract_sequence' (b : list instr) : option (forest * list pred_expr * list pred_expr) := +Definition abstract_sequence_top (b : list instr) : option (forest * list (resource * 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)))). + (mfold_left update_top b (Some (Ptrue, empty, nil, nil)))). (*Compute match update (T, mk_forest (PTree.empty _) (PTree.empty _) (NE.singleton (T, EEbase))) (RBop None Op.Odiv (1::2::nil) 3) with @@ -404,10 +409,23 @@ Definition empty_trees (bb: SeqBB.t) (bbt: ParBB.t) : bool := | _ => true end. +Definition check_evaluability1 a b := + forallb (fun be => + existsb (fun ae => + resource_eq (fst ae) (fst be) + && HN.beq_pred_expr (snd ae) (snd be) + ) a + ) b. + +Definition check_evaluability2 a b := + forallb (fun be => existsb (fun ae => HN.beq_pred_expr ae be) a) b. + Definition schedule_oracle (bb: SeqBB.t) (bbt: ParBB.t) : bool := - match abstract_sequence bb, abstract_sequence (concat (concat bbt)) with - | Some bb', Some bbt' => + match abstract_sequence_top bb, abstract_sequence_top (concat (concat bbt)) with + | Some (bb', reg_expr, m_expr), Some (bbt', reg_expr_t, m_expr_t) => check bb' bbt' && empty_trees bb bbt + && check_evaluability1 reg_expr reg_expr_t + && check_evaluability2 m_expr m_expr_t | _, _ => false end. diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index a27edd5..d956fcb 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -48,6 +48,91 @@ Module Import OptionExtra := MonadExtra(Option). Ltac destr := destruct_match; try discriminate; []. +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') -> + update (p, f) i = Some (p', f'). +Proof. + intros. unfold update_top, 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). +Proof. + induction l; destruct i; 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') -> + update' (p, f, map snd l, lm) i = Some (p', f', map snd l', lm'). +Proof. + intros. unfold update', update_top, Option.bind2, Option.ret in *. repeat destr. + inv Heqp1. inv H. repeat f_equal. apply remember_expr_eq. +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') -> + mfold_left update' i (Some (p, f, map snd l, lm)) = Some (p', f', map snd l', lm'). +Proof. + induction i; cbn -[update_top 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; 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') -> + mfold_left update i (Some (p, f)) = Some (p', f'). +Proof. + induction i; cbn -[update_top 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; try eassumption. + intros. rewrite H0. eapply IHi. rewrite HB in H. eauto. +Qed. + +Lemma spec_abstract_sequence_top : + mfold_left + fun (s : pred_op * forest * list pred_expr * list pred_expr) (i : instr) => + let + '(p, f, l, lm) := s in + Option.bind2 (fun (p' : pred_op) (f' : forest) => Option.ret (p', f', , remember_expr_m f lm i)) + (update (p, f) i) + : pred_op * forest * list pred_expr * list pred_expr -> instr -> option (pred_op * forest * list pred_expr * list pred_expr). + +Lemma top_implies_abstract_sequence : + forall y f l1 l2, + abstract_sequence_top y = Some (f, l1, l2) -> + abstract_sequence y = Some f. +Proof. + unfold abstract_sequence, abstract_sequence_top; intros. + unfold Option.bind in *. repeat destr. + inv H. + unfold Option.map in *|-. repeat destr. subst. inv Heqo. + erewrite equiv_fold_update_top by eauto. auto. +Qed. + +Lemma top_implies_abstract_sequence' : + forall y f l1 l2, + abstract_sequence_top y = Some (f, l1, l2) -> + abstract_sequence' y = Some (f, map snd l1, l2). +Proof. + unfold abstract_sequence', abstract_sequence_top; intros. + unfold Option.bind in *|-. repeat destr. + inv H. + unfold Option.map in *|-. repeat destr. subst. inv Heqo. + exploit equiv_fold_update'_top; 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) := @@ -415,6 +500,31 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. eapply IHx; eauto. Qed. + Lemma abstract_sequence_evaluable : + forall sp x i i' cf f l0 l, + SeqBB.step ge sp (Iexec i) x (Iterm i' cf) -> + abstract_sequence_top x = Some (f, l0, l) -> + evaluable_pred_list (mk_ctx i sp ge) f.(forest_preds) (map snd l0). + Proof. + induction x; cbn; intros. + - inv H0. inv H. + - exploit top_implies_abstract_sequence; eauto; intros. inv H. inv H7; eauto. + + unfold abstract_sequence_top, Option.bind, Option.map in *. + repeat destr; subst. inv H0. inv Heqo. + unfold evaluable_pred_list; intros. + unfold evaluable_pred_expr. + exploit OptionExtra.mfold_left_Some. eapply Heqm1. + intros [[[[p_mid f_mid] l_mid] lm_mid] HB]. inv HB. + + Lemma abstract_sequence_evaluable_m : + forall sp x i i' cf f l0 l, + SeqBB.step ge sp (Iexec i) x (Iterm i' cf) -> + abstract_sequence_top x = Some (f, l0, l) -> + evaluable_pred_list_m (mk_ctx i sp ge) f.(forest_preds) l. + Proof. Admitted. + +(* abstract_sequence_top x = Some (f, l0, l) -> *) + Lemma schedule_oracle_correct : forall x y sp i i' ti cf, schedule_oracle x y = true -> @@ -424,12 +534,15 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. /\ state_lessdef i' ti'. Proof. unfold schedule_oracle; intros. repeat (destruct_match; try discriminate). simplify. + exploit top_implies_abstract_sequence; [eapply Heqo|]; intros. + exploit top_implies_abstract_sequence'; 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; eauto. admit. admit. admit. admit. reflexivity. simplify. + exploit abstr_seq_reverse_correct; eauto. + admit. reflexivity. simplify. exploit seqbb_step_parbb_step; eauto; intros. econstructor; split; eauto. etransitivity; eauto. diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v index 815f005..af9f3b4 100644 --- a/src/hls/GiblePargenproofBackward.v +++ b/src/hls/GiblePargenproofBackward.v @@ -66,6 +66,26 @@ the translation goes from GiblePar to Abstr, whereas the correctness proof is needed from Abstr to GiblePar to get the proper direction of the proof. |*) +Definition remember_expr (f : forest) (lst: list pred_expr) (i : instr): list pred_expr := + match i with + | RBnop => lst + | RBop p op rl r => (f #r (Reg r)) :: lst + | RBload p chunk addr rl r => (f #r (Reg r)) :: 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 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)))). + Section CORRECTNESS. Context (prog: GibleSeq.program) (tprog : GiblePar.program). @@ -86,15 +106,6 @@ Proof. eapply IHi; eauto. 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') -> - update' (p, f, l, lm) i = Some (p', f', l', lm'). -Proof. - intros. unfold update', update'', Option.bind2, Option.ret in *. repeat destr. - inv Heqp1. now inv H. -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') -> @@ -113,24 +124,13 @@ Proof. inv Heqp1. now inv H. Qed. -Lemma equiv_update': - forall i p f l lm p' f' l' lm' lp lp', - mfold_left update'' i (Some (p, f, l, lm, lp)) = Some (p', f', l', lm', lp') -> - mfold_left update' i (Some (p, f, l, lm)) = Some (p', f', l', lm'). -Proof. - induction i; cbn -[update'' update'] in *; intros. - - inv H; auto. - - exploit OptionExtra.mfold_left_Some; eauto; - intros [[[[[p_mid f_mid] l_mid] lm_mid] lp_mid] HB]. - exploit equiv_update1'; try eassumption. - intros. rewrite H0. eapply IHi. rewrite HB in H. eauto. -Qed. -Lemma equiv_update'': - forall i p f l lm p' f' l' lm' lp lp', - mfold_left update'' i (Some (p, f, l, lm, lp)) = Some (p', f', l', lm', lp') -> - mfold_left update i (Some (p, f)) = Some (p', f'). -Proof. eauto using equiv_update', equiv_update. Qed. + +(* Lemma equiv_update'': *) +(* forall i p f l lm p' f' l' lm' lp lp', *) +(* mfold_left update'' i (Some (p, f, l, lm, lp)) = Some (p', f', l', lm', lp') -> *) +(* mfold_left update i (Some (p, f)) = Some (p', f'). *) +(* Proof. eauto using equiv_update', equiv_update. Qed. *) Definition i_state (s: istate): instr_state := match s with @@ -1818,11 +1818,10 @@ Proof. Qed. Lemma abstr_seq_reverse_correct: - forall sp x i i' ti cf x' l lm ps', + forall sp x i i' ti cf x' l lm, abstract_sequence' 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_predset {| ctx_is := i; ctx_sp := sp; ctx_ge := ge |} x' ps' -> 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) @@ -1830,6 +1829,7 @@ Lemma abstr_seq_reverse_correct: Proof. intros. unfold abstract_sequence' 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; try eassumption; try reflexivity; auto using sem_empty, all_preds_in_empty. inversion 1. -- cgit