From 899343189f60966ff161c9d5dac9caae5a28102e Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 24 May 2023 18:58:22 +0100 Subject: Finish gather_predicate proofs --- src/hls/GiblePargenproofBackward.v | 519 +++++++++++++++++++++++++++++++++++-- 1 file changed, 502 insertions(+), 17 deletions(-) (limited to 'src/hls') diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v index 7a830be..3fc6c52 100644 --- a/src/hls/GiblePargenproofBackward.v +++ b/src/hls/GiblePargenproofBackward.v @@ -633,19 +633,13 @@ Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval : exists ps, sem_predset (mk_ctx i0 sp ge) f ps. Proof. Admitted. -Definition all_preds_in f preds := - (forall x, NE.Forall (fun x => forall pred, PredIn pred (fst x) - -> PTree.get pred preds = Some tt) (f #r x)) - /\ NE.Forall (fun x => forall pred, PredIn pred (fst x) - -> PTree.get pred preds = Some tt) f.(forest_exit). +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. -Lemma gather_predicates_in_forest : - forall p i f p' f' preds preds', - update (p, f) i = Some (p', f') -> - gather_predicates preds i = Some preds' -> - all_preds_in f preds -> - all_preds_in f' preds'. -Proof. Admitted. +Definition all_preds_in f preds := + forall x, NE.Forall (fun x => forall pred, PredIn pred (fst x) + -> PTree.get pred preds = Some tt) (f #r x). Lemma gather_predicates_fold: forall l preds x, @@ -658,6 +652,18 @@ Proof. rewrite PTree.gso; eauto. Qed. +Lemma gather_predicates_fold2: + forall l preds x, + In x l -> + (fold_right (fun x0 : positive => PTree.set x0 tt) preds l) ! x = Some tt. +Proof. + induction l; crush. + destruct (peq x a); subst. + { rewrite PTree.gss; auto. } + rewrite PTree.gso; eauto. + eapply IHl. now inv H. +Qed. + Lemma gather_predicates_in : forall i preds preds' x, gather_predicates preds i = Some preds' -> @@ -670,6 +676,486 @@ Proof. apply gather_predicates_fold; auto. Qed. +Lemma filter_predicated_in_pred : + forall A (x y: predicated A) f preds, + NE.filter f x = Some y -> + pe_preds_in x preds -> + pe_preds_in y preds. +Proof. + induction x; intros. + - cbn in *. destr. inv H. auto. + - cbn in *. destruct_match; cbn in *. destruct_match. + + inv H. inv H0. constructor; auto. eapply IHx; eauto. + + inv H. inv H0; constructor; auto. + + inv H0. eauto. +Qed. + +Transparent deep_simplify. + +Lemma deep_simplify_in : + forall pop pred, + PredIn pred (deep_simplify peq pop) -> + PredIn pred pop. +Proof. + induction pop; intros; cbn in *; auto. + - constructor. + destruct (PredIn_decidable _ pred (deep_simplify peq pop1) peq); [intuition|]. + destruct (PredIn_decidable _ pred (deep_simplify peq pop2) peq); [intuition|]. + repeat destruct_match; try solve [contradiction | inv H; inv H1; contradiction]. + - constructor. + destruct (PredIn_decidable _ pred (deep_simplify peq pop1) peq); [intuition|]. + destruct (PredIn_decidable _ pred (deep_simplify peq pop2) peq); [intuition|]. + repeat destruct_match; try solve [contradiction | inv H; inv H1; contradiction]. +Qed. + +Lemma map_in_pred : + forall A B (x: predicated A) f preds (g: A -> B), + pe_preds_in x preds -> + (forall pop pred, PredIn pred (f pop) -> PredIn pred pop) -> + pe_preds_in (NE.map (fun x0 => (f (fst x0), g (snd x0))) x) preds. +Proof. + induction x. + - inversion 1; subst. constructor; intros. specialize (H1 pred). apply H1. eauto. + - intros. inv H. constructor; eauto. eapply IHx; eauto. +Qed. + +Lemma map_in_pred2 : + forall A B (x: predicated A) f preds (g: A -> B), + pe_preds_in x preds -> + (forall pop pred, PredIn pred (f pop) -> preds ! pred = Some tt) -> + pe_preds_in (NE.map (fun x0 => (f (fst x0), g (snd x0))) x) preds. +Proof. + induction x. + - intros. inv H. cbn. constructor. intros. cbn in *. eapply H0; eauto. + - intros. inv H. constructor; eauto. eapply IHx; eauto. +Qed. + +Lemma map_in_pred3 : + forall A B (x: predicated A) f preds (g: A -> B), + pe_preds_in x preds -> + (forall pop pred, PredIn pred (f pop) -> PredIn pred pop \/ preds ! pred = Some tt) -> + pe_preds_in (NE.map (fun x0 => (f (fst x0), g (snd x0))) x) preds. +Proof. + induction x. + - intros. inv H. cbn. constructor; intros. cbn in *. eapply H0 in H. inv H; eauto. + - intros. inv H. constructor; eauto. intros. cbn in H. eapply H0 in H. inv H; eauto. + eapply IHx; eauto. +Qed. + +Lemma map_in_pred4 : + forall A B (x: predicated A) (f: (pred_op * A) -> (pred_op * B)) preds, + pe_preds_in x preds -> + (forall a pop pred, PredIn pred (fst (f (pop, a))) -> PredIn pred pop + \/ preds ! pred = Some tt) -> + pe_preds_in (NE.map f x) preds. +Proof. + induction x. + - intros. inv H. cbn. constructor; intros. destruct a. apply H0 in H. inv H; auto. + - intros. inv H. cbn. constructor; intros. destruct a. apply H0 in H. inv H; auto. + eapply IHx; eauto. +Qed. + +Lemma app_in_pred : + forall A (a b: predicated A) preds, + pe_preds_in a preds -> + pe_preds_in b preds -> + pe_preds_in (NE.app a b) preds. +Proof. + intros. unfold pe_preds_in in *. + apply NE.Forall_forall; intros. eapply NE.in_NEapp5 in H1. inv H1. + - eapply NE.Forall_forall in H; eauto. + - eapply NE.Forall_forall in H0; eauto. +Qed. + +Lemma prune_predicated_in_pred : + forall A (x y: predicated A) preds, + prune_predicated x = Some y -> + pe_preds_in x preds -> + pe_preds_in y preds. +Proof. + intros. unfold prune_predicated in *. + eapply filter_predicated_in_pred in H. eauto. + eapply map_in_pred with (f := deep_simplify peq) (g := fun x => x); auto. + apply deep_simplify_in. +Qed. + +Lemma predin_negate : + forall A preds (pred: A), + PredIn pred preds -> + PredIn pred (negate preds). +Proof. + induction preds. + - cbn. repeat destr. inv Heqp0; intros. inv H. constructor. + - inversion 1. + - inversion 1. + - inversion 1; subst. clear H. inv H1. cbn. + constructor. eauto. cbn. constructor. eauto. + - inversion 1; subst. clear H. inv H1. cbn. + constructor. eauto. cbn. constructor. eauto. +Qed. + +Lemma predin_negate2 : + forall A preds (pred: A), + PredIn pred (negate preds) -> + PredIn pred preds. +Proof. + induction preds. + - cbn. repeat destr. inv Heqp0; intros. inv H. constructor. + - inversion 1. + - inversion 1. + - inversion 1; subst. clear H. inv H1. cbn. + constructor. eauto. cbn. constructor. eauto. + - inversion 1; subst. clear H. inv H1. cbn. + constructor. eauto. cbn. constructor. eauto. +Qed. + +Lemma app_predicated_in_pred : + forall A (a: predicated A) b p preds, + pe_preds_in a preds -> + pe_preds_in b preds -> + (forall in_pred, PredIn in_pred p -> preds ! in_pred = Some tt) -> + pe_preds_in (app_predicated p a b) preds. +Proof. + unfold app_predicated. unfold app_predicated; intros. + eapply app_in_pred. + apply map_in_pred3 with (f := (fun x => Pand (negate p) x)) (g := (fun x => x)); auto. + intros. inv H2. inv H4; auto. right. eapply H1. apply predin_negate2; auto. + apply map_in_pred3 with (f := (fun x => Pand p x)) (g := (fun x => x)); auto. + intros. inv H2. inv H4; auto. +Qed. + +Lemma predicated_map_in_pred : + forall A B (a: predicated A) preds (f: A -> B), + pe_preds_in a preds -> + pe_preds_in (predicated_map f a) preds. +Proof. + unfold predicated_map; intros. + apply map_in_pred with (f := fun x => x) (g := f); auto. +Qed. + +(* Lemma non_empty_prod_cons : *) +(* forall A (a: A) r b, *) +(* NE.non_empty_prod (NE.cons a r) b = . *) + +Lemma map_in_pred5: + forall A B p preds, + pe_preds_in (NE.map fst p) preds -> + pe_preds_in (NE.map snd p) preds -> + pe_preds_in (NE.map (fun x : Predicate.pred_op * A * (Predicate.pred_op * B) => + let (y, y0) := x in let (a, b1) := y in let (c, d) := y0 in (a ∧ c, (b1, d))) p) preds. +Proof. + induction p; crush; repeat destr. + - inv H. inv H0. constructor; intros. inv H. inv H3; auto. + - inv Heqp0. inv H. inv H0. constructor. intros. inv H. inv H1; auto. + eapply IHp; eauto. +Qed. + +Lemma predicated_prod_in_pred : + forall A B (a: predicated A) (b: predicated B) preds, + pe_preds_in a preds -> + pe_preds_in b preds -> + pe_preds_in (predicated_prod a b) preds. +Proof. + unfold predicated_prod; induction a; induction b; crush; repeat destr. + - constructor. cbn. inversion 1; subst. inv H3. inv H. eauto. inv H0; eauto. + - inv Heqp0. constructor; cbn; intros. inv H1. inv H3. inv H; auto. inv H0; auto. + inv H0; eauto. eapply IHb; eauto. + - inv Heqp0. inv H0. inv H. constructor; eauto. cbn; intros. inv H. inv H1; eauto. + eapply IHa; eauto. constructor. eauto. + - inv H. inv H0. constructor; cbn; intros. inv H. inv H1; eauto. + rewrite NE.app_NEmap. apply app_in_pred. + eapply map_in_pred5. + { clear IHb. clear IHa. clear H4. clear H2. generalize dependent b. + induction b; crush. + - constructor; auto. + - inv H5. constructor; auto. eapply IHb; eauto. + } + { clear IHb. clear IHa. clear H4. clear H2. generalize dependent b. + induction b; crush. + inv H5. constructor; auto. eapply IHb; eauto. + } + eapply IHa; eauto. constructor; eauto. +Qed. + +Lemma seq_app_prod_in_pred : + forall A B (a: predicated (A -> B)) (b: predicated A) preds, + pe_preds_in a preds -> + pe_preds_in b preds -> + pe_preds_in (seq_app a b) preds. +Proof. + intros. unfold seq_app. eapply predicated_map_in_pred. + eapply predicated_prod_in_pred; auto. +Qed. + +Lemma cons_pred_expr_in : + forall a b preds, + pe_preds_in a preds -> + pe_preds_in b preds -> + pe_preds_in (cons_pred_expr a b) preds. +Proof. Admitted. + +Lemma cons_fold_in: + forall n s preds, + pe_preds_in s preds -> + NE.Forall (fun n' => pe_preds_in n' preds) n -> + pe_preds_in (GiblePargenproofEquiv.NE.fold_right cons_pred_expr s n) preds. +Proof. + induction n; crush. + - inv H0. eapply cons_pred_expr_in; auto. + - inv H0. eapply cons_pred_expr_in; auto. +Qed. + +Lemma to_list_in : + forall A l n (x: A), + NE.of_list l = Some n -> In x l -> NE.In x n. +Proof. + induction l; crush. + inv H0. destruct l. inv H. constructor. destr. inv H. constructor; tauto. + destruct l. inv H1. destr. inv H. inv H1. econstructor. right. + eapply IHl; auto. constructor. auto. constructor. right. eapply IHl; auto. + apply in_cons; auto. +Qed. + +Lemma to_list_in2 : + forall A l n (x: A), + NE.of_list l = Some n -> NE.In x n -> In x l. +Proof. + induction l; crush. + inv H0. destruct l. inv H. destr. inv H. + inv H1; try tauto. right. eapply IHl; eauto. + destruct l. inv H. tauto. + destruct_match. inv H. inv H. +Qed. + +Lemma merge_preds_in : + forall a preds, + Forall (fun x => pe_preds_in x preds) a -> + pe_preds_in (merge a) preds. +Proof. + unfold merge; intros. destruct_match; cbn. + - eapply cons_fold_in; auto. constructor. inversion 1. + apply NE.Forall_forall; intros. eapply Forall_forall in H. + 2: { eapply to_list_in2; eauto. } auto. + - constructor; inversion 1. +Qed. + +Lemma list_translation_in : + forall f preds, + all_preds_in f preds -> + forall args, Forall (fun x : predicated expression => pe_preds_in x preds) (list_translation args f). +Proof. + induction args. + - cbn. constructor. + - cbn. constructor; auto. unfold all_preds_in in H. eapply H. +Qed. + +Lemma pe_preds_in_fold: + forall A l preds x, + pe_preds_in x preds -> + @pe_preds_in A x (fold_right (fun x0 : positive => PTree.set x0 tt) preds l). +Proof. + unfold pe_preds_in; intros. apply NE.Forall_forall; intros. + eapply NE.Forall_forall in H; eauto. apply gather_predicates_fold; eauto. +Qed. + +Lemma pred_in_pred_uses: + forall A (p: A) pop, + PredIn p pop -> + In p (predicate_use pop). +Proof. + induction pop; crush. + - destr. inv Heqp1. inv H. now constructor. + - inv H. + - inv H. + - apply in_or_app. inv H. inv H1; intuition. + - apply in_or_app. inv H. inv H1; intuition. +Qed. + +Lemma pe_preds_in_flap2: + forall A B C f a b preds, + pe_preds_in f preds -> + pe_preds_in (@flap2 A B C f a b) preds. +Proof. + unfold flap2; intros. + eapply map_in_pred4; auto. +Qed. + +#[local] Opaque seq_app. +Lemma gather_predicates_RBop : + forall p f pred op args dst p' f' preds preds', + update (p, f) (RBop (Some pred) op args dst) = Some (p', f') -> + gather_predicates preds (RBop (Some pred) op args dst) = Some preds' -> + (forall in_pred, PredIn in_pred p -> preds ! in_pred = Some tt) -> + all_preds_in f preds -> + all_preds_in f' preds'. +Proof. + intros. cbn in *. unfold Option.bind in *; repeat destr. inv H. + inv H0. unfold all_preds_in in *; intros. + apply NE.Forall_forall; intros. + destruct (resource_eq (Reg dst) x). + { subst. rewrite forest_reg_gss in H. + eapply prune_predicated_in_pred in Heqo. + instantiate (1:=(fold_right (fun x : positive => PTree.set x tt) preds (predicate_use pred))) in Heqo. + unfold pe_preds_in in Heqo. eapply NE.Forall_forall in Heqo; eauto. + eapply app_predicated_in_pred. + eapply pe_preds_in_fold. + specialize (H2 (Reg dst)). unfold pe_preds_in. + apply NE.Forall_forall; intros. eapply NE.Forall_forall in H2; eauto. + eapply seq_app_prod_in_pred. unfold pred_ret. constructor; inversion 1. + eapply pe_preds_in_fold. + eapply merge_preds_in. + apply list_translation_in. + eauto. + intros. inv H3. inv H5. + eapply gather_predicates_fold2; eauto. + apply pred_in_pred_uses; auto. + eapply gather_predicates_fold; eauto. + } + rewrite forest_reg_gso in H by auto. + apply gather_predicates_fold; auto. + specialize (H2 x). eapply NE.Forall_forall in H2; eauto. +Qed. + +Lemma gather_predicates_RBload : + forall p f pred chunk addr args dst p' f' preds preds', + update (p, f) (RBload (Some pred) chunk addr args dst) = Some (p', f') -> + gather_predicates preds (RBload (Some pred) chunk addr args dst) = Some preds' -> + (forall in_pred, PredIn in_pred p -> preds ! in_pred = Some tt) -> + all_preds_in f preds -> + all_preds_in f' preds'. +Proof. + intros. cbn in *. unfold Option.bind in *; repeat destr. inv H. + inv H0. unfold all_preds_in in *; intros. + apply NE.Forall_forall; intros. + destruct (resource_eq (Reg dst) x). + { subst. rewrite forest_reg_gss in H. + eapply prune_predicated_in_pred in Heqo. + instantiate (1:=(fold_right (fun x : positive => PTree.set x tt) preds (predicate_use pred))) in Heqo. + unfold pe_preds_in in Heqo. eapply NE.Forall_forall in Heqo; eauto. + eapply app_predicated_in_pred. + eapply pe_preds_in_fold. + specialize (H2 (Reg dst)). unfold pe_preds_in. + apply NE.Forall_forall; intros. eapply NE.Forall_forall in H2; eauto. + eapply seq_app_prod_in_pred. + eapply seq_app_prod_in_pred. + unfold pred_ret. constructor; inversion 1. + eapply pe_preds_in_fold. + eapply merge_preds_in. + apply list_translation_in. eauto. + unfold pe_preds_in; intros. eapply NE.Forall_forall; intros. + specialize (H2 Mem). eapply NE.Forall_forall in H2; eauto. + eapply gather_predicates_fold; eauto. + intros. inv H3. inv H5. + eapply gather_predicates_fold2; eauto. + apply pred_in_pred_uses; auto. + eapply gather_predicates_fold; eauto. + } + rewrite forest_reg_gso in H by auto. + apply gather_predicates_fold; auto. + specialize (H2 x). eapply NE.Forall_forall in H2; eauto. +Qed. + +Lemma gather_predicates_RBstore : + forall p f pred chunk addr args src p' f' preds preds', + update (p, f) (RBstore (Some pred) chunk addr args src) = Some (p', f') -> + gather_predicates preds (RBstore (Some pred) chunk addr args src) = Some preds' -> + (forall in_pred, PredIn in_pred p -> preds ! in_pred = Some tt) -> + all_preds_in f preds -> + all_preds_in f' preds'. +Proof. + intros. cbn in *. unfold Option.bind in *; repeat destr. inv H. + inv H0. unfold all_preds_in in *; intros. + apply NE.Forall_forall; intros. + destruct (resource_eq Mem x). + { subst. rewrite forest_reg_gss in H. + eapply prune_predicated_in_pred in Heqo. + instantiate (1:=(fold_right (fun x : positive => PTree.set x tt) preds (predicate_use pred))) in Heqo. + unfold pe_preds_in in Heqo. eapply NE.Forall_forall in Heqo; eauto. + eapply app_predicated_in_pred. + eapply pe_preds_in_fold. + specialize (H2 Mem). unfold pe_preds_in. + apply NE.Forall_forall; intros. eapply NE.Forall_forall in H2; eauto. + eapply seq_app_prod_in_pred. + eapply seq_app_prod_in_pred. + apply pe_preds_in_flap2. + eapply seq_app_prod_in_pred. + unfold pred_ret. constructor; inversion 1. + eapply pe_preds_in_fold. eapply H2. + eapply pe_preds_in_fold. + eapply merge_preds_in. + apply list_translation_in. eauto. + eapply pe_preds_in_fold. eapply H2. + intros. inv H3. inv H5. + eapply gather_predicates_fold2; eauto. + apply pred_in_pred_uses; auto. + eapply gather_predicates_fold; eauto. + } + rewrite forest_reg_gso in H by auto. + apply gather_predicates_fold; auto. + specialize (H2 x). eapply NE.Forall_forall in H2; eauto. +Qed. + +Lemma gather_predicates_RBsetpred : + forall p f pred args cond pset p' f' preds preds', + update (p, f) (RBsetpred (Some pred) cond args pset) = Some (p', f') -> + gather_predicates preds (RBsetpred (Some pred) cond args pset) = Some preds' -> + (forall in_pred, PredIn in_pred p -> preds ! in_pred = Some tt) -> + all_preds_in f preds -> + all_preds_in f' preds'. +Proof. + intros. cbn in *. unfold Option.bind in *; repeat destr. inv H. + inv H0. unfold all_preds_in in *; intros. + rewrite forest_pred_reg. + eapply pe_preds_in_fold. eapply H2. +Qed. + +Lemma forest_exit_regs : + forall f n r, + (f <-e n) #r r = f #r r. +Proof. + unfold "<-e", "#r"; intros. + repeat destruct_match; crush. +Qed. + +Lemma gather_predicates_RBexit : + forall p f pred cf p' f' preds preds', + update (p, f) (RBexit (Some pred) cf) = Some (p', f') -> + gather_predicates preds (RBexit (Some pred) cf) = Some preds' -> + (forall in_pred, PredIn in_pred p -> preds ! in_pred = Some tt) -> + all_preds_in f preds -> + all_preds_in f' preds'. +Proof. + intros. cbn in *. unfold Option.bind in *; repeat destr. inv H. + inv H0. unfold all_preds_in in *; intros. + rewrite forest_exit_regs. + eapply pe_preds_in_fold. eapply H2. +Qed. + +Transparent seq_app. + +Lemma gather_predicates_in_forest : + forall p i f p' f' preds preds', + update (p, f) i = Some (p', f') -> + gather_predicates preds i = Some preds' -> + all_preds_in f preds -> + all_preds_in f' preds'. +Proof. + intros. + destruct i; intros; cbn in *; + unfold Option.bind, Option.ret, Option.bind2 in *; + generalize H; repeat destr; inversion 1; subst; clear H. + - inv H0; auto. + - clear H2. destruct o. + + unfold all_preds_in in *; intros. + apply NE.Forall_forall; intros. + destruct (resource_eq (Reg r) x). + { subst. rewrite forest_reg_gss in H. + inv H0. } + rewrite forest_reg_gso in H by auto. inv H0. + eapply NE.Forall_forall in H1; eauto. + specialize (H1 _ H2). apply gather_predicates_fold; auto. + + inversion H0; subst; auto. + Lemma sem_pexpr_eval_predin: forall G pr ps ps' (ctx: @Abstr.ctx G) b, (forall pred, PredIn pred pr -> ps' ! pred = ps ! pred) -> @@ -879,7 +1365,7 @@ Proof. eapply abstr_seq_revers_correct_fold_sem_pexpr_eval2; eauto. unfold evaluable_pred_list in Y0. eapply in_forest_evaluable; eauto. eapply gather_predicates_in_forest in YALL; eauto. - unfold all_preds_in in YALL. inv YALL. eauto. + unfold all_preds_in in YALL. eauto. intros [ti_mid HSTEP]. pose proof Y3 as YH. @@ -903,7 +1389,7 @@ Proof. eapply abstr_seq_revers_correct_fold_sem_pexpr_eval2; eauto. unfold evaluable_pred_list in Y0. eapply in_forest_evaluable; eauto. eapply gather_predicates_in_forest in YALL; eauto. - unfold all_preds_in in YALL. inv YALL. eauto. + unfold all_preds_in in YALL. eauto. intros [ti_mid HSTEP]. pose proof Y3 as YH. @@ -927,7 +1413,7 @@ Proof. eapply abstr_seq_revers_correct_fold_sem_pexpr_eval4; eauto. unfold evaluable_pred_list in Y0. eapply in_forest_evaluable_m; eauto. eapply gather_predicates_in_forest in YALL; eauto. - unfold all_preds_in in YALL. inv YALL. eauto. + unfold all_preds_in in YALL. eauto. intros [ti_mid HSTEP]. pose proof Y3 as YH. @@ -1020,9 +1506,8 @@ Qed. Lemma all_preds_in_empty: all_preds_in empty (PTree.empty unit). Proof. - unfold all_preds_in; split; intros; apply NE.Forall_forall; intros. + unfold all_preds_in; intros; apply NE.Forall_forall; intros. - rewrite get_empty in H. inv H. inv H0. - - cbn in *. inv H. inv H0. Qed. Lemma abstr_seq_reverse_correct: -- cgit