From b68e1e078c2829fb04e4721d13432d0e82a1e0e9 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 5 May 2023 18:43:12 +0100 Subject: Finish forward and backward proofs for predicated proof --- src/hls/Abstr.v | 688 ++++++++++++++++++++++++++++++++------------- src/hls/GiblePargenproof.v | 90 ------ src/hls/Predicate.v | 8 - 3 files changed, 499 insertions(+), 287 deletions(-) (limited to 'src/hls') diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index 76c3746..c489df2 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -756,158 +756,18 @@ Fixpoint hash_predicate (max: predicate) (ap: pred_pexpr) (h: PHT.hash_tree) end. Definition predicated_mutexcl {A: Type} (pe: predicated A): Prop := - forall x y, NE.In x pe -> NE.In y pe -> x <> y -> fst x ⇒ ¬ fst y. + (forall x y, NE.In x pe -> NE.In y pe -> x <> y -> fst x ⇒ ¬ fst y) + /\ NE.norepet pe. Lemma predicated_cons : forall A (a: pred_op * A) x, predicated_mutexcl (a ::| x) -> predicated_mutexcl x. Proof. - unfold predicated_mutexcl; intros. - apply H; auto; constructor; tauto. + unfold predicated_mutexcl; intros. inv H. inv H1. split; auto. + intros. apply H0; auto; constructor; tauto. Qed. -Module HashExprNorm(H: Hashable). - Module H := HashTree(H). - - Definition norm_tree: Type := PTree.t pred_op * H.hash_tree. - - Fixpoint norm_expression (max: predicate) (pe: predicated H.t) (h: H.hash_tree) - : norm_tree := - match pe with - | NE.singleton (p, e) => - let (hashed_e, h') := H.hash_value max e h in - (PTree.set hashed_e p (PTree.empty _), h') - | (p, e) ::| pr => - let (hashed_e, h') := H.hash_value max e h in - let (norm_pr, h'') := norm_expression max pr h' in - match norm_pr ! hashed_e with - | Some pr_op => - (PTree.set hashed_e (pr_op ∨ p) norm_pr, h'') - | None => - (PTree.set hashed_e p norm_pr, h'') - end - end. - - Definition mk_pred_stmnt' (e: predicate) p_e := ¬ p_e ∨ Plit (true, e). - - Definition mk_pred_stmnt t := PTree.fold (fun x a b => mk_pred_stmnt' a b ∧ x) t T. - - Definition mk_pred_stmnt_l (t: list (predicate * pred_op)) := - fold_left (fun x a => uncurry mk_pred_stmnt' a ∧ x) t T. - - Definition encode_expression max pe h := - let (tree, h) := norm_expression max pe h in - (mk_pred_stmnt tree, h). - - Definition pred_expr_dec: forall pe1 pe2: predicated H.t, - {pe1 = pe2} + {pe1 <> pe2}. - Proof. - pose proof H.eq_dec as X. - pose proof (Predicate.eq_dec peq). - pose proof (NE.eq_dec _ X). - assert (forall a b: pred_op * H.t, {a = b} + {a <> b}) - by decide equality. - decide equality. - Defined. - - Definition beq_pred_expr' (pe1 pe2: predicated H.t) : bool := - if pred_expr_dec pe1 pe2 then true else - let (p1, h) := encode_expression 1%positive pe1 (PTree.empty _) in - let (p2, h') := encode_expression 1%positive pe2 h in - equiv_check p1 p2. - - Lemma mk_pred_stmnt_equiv' : - forall l l' e p, - mk_pred_stmnt_l l == mk_pred_stmnt_l l' -> - In (e, p) l -> - list_norepet (map fst l) -> - (exists p', In (e, p') l' /\ p == p') - \/ ~ In e (map fst l') /\ p == ⟂. - Proof. Abort. - - Lemma mk_pred_stmnt_equiv : - forall tree tree', - mk_pred_stmnt tree == mk_pred_stmnt tree'. - Proof. Abort. - - Definition tree_equiv_check_el (np2: PTree.t pred_op) (n: positive) (p: pred_op): bool := - match np2 ! n with - | Some p' => equiv_check p p' - | None => equiv_check p ⟂ - end. - - Definition tree_equiv_check_None_el (np2: PTree.t pred_op) (n: positive) (p: pred_op): bool := - match np2 ! n with - | Some p' => true - | None => equiv_check p ⟂ - end. - - Definition beq_pred_expr (pe1 pe2: predicated H.t) : bool := - if pred_expr_dec pe1 pe2 then true else - let (np1, h) := norm_expression 1 pe1 (PTree.empty _) in - let (np2, h') := norm_expression 1 pe2 h in - forall_ptree (tree_equiv_check_el np2) np1 - && forall_ptree (tree_equiv_check_None_el np1) np2. - - Lemma beq_pred_expr_correct: - forall np1 np2 e p p', - forall_ptree (tree_equiv_check_el np2) np1 = true -> - np1 ! e = Some p -> - np2 ! e = Some p' -> - p == p'. - Proof. - intros. - eapply forall_ptree_true in H; try eassumption. - unfold tree_equiv_check_el in H. - rewrite H1 in H. now apply equiv_check_correct. - Qed. - - Lemma beq_pred_expr_correct2: - forall np1 np2 e p, - forall_ptree (tree_equiv_check_el np2) np1 = true -> - np1 ! e = Some p -> - np2 ! e = None -> - p == ⟂. - Proof. - intros. - eapply forall_ptree_true in H; try eassumption. - unfold tree_equiv_check_el in H. - rewrite H1 in H. now apply equiv_check_correct. - Qed. - - Lemma beq_pred_expr_correct3: - forall np1 np2 e p, - forall_ptree (tree_equiv_check_None_el np1) np2 = true -> - np1 ! e = None -> - np2 ! e = Some p -> - p == ⟂. - Proof. - intros. - eapply forall_ptree_true in H; try eassumption. - unfold tree_equiv_check_None_el in H. - rewrite H0 in H. now apply equiv_check_correct. - Qed. - - Variant sem_pred_tree {A B: Type} (pr: PTree.t pred_pexpr) (sem: ctx -> H.t -> B -> Prop): - @ctx A -> PTree.t H.t -> PTree.t pred_op -> B -> Prop := - | sem_pred_tree_intro : - forall ctx expr e v et pt, - eval_predf (ctx_ps ctx) pr = true -> - sem ctx expr v -> - pt ! e = Some pr -> - et ! e = Some expr -> - sem_pred_tree sem ctx et pt v. - - Lemma exec_tree_exec_non_empty : - forall (s) - sem_pred_tree s - -End HashExprNorm. - -Module HN := HashExprNorm(HashExpr). -Module EHN := HashExprNorm(EHashExpr). - (* Lemma norm_expr_constant : @@ -961,46 +821,6 @@ Lemma norm_expr_mutexcl : p ⇒ ¬ p'. Proof. Abort.*) -Lemma sem_pexpr_negate : - forall A ctx p b, - sem_pexpr ctx p b -> - @sem_pexpr A ctx (¬ p) (negb b). -Proof. - induction p; crush. - - destruct_match. destruct b0; crush. inv Heqp0. - constructor. inv H. rewrite negb_involutive. auto. - constructor. inv H. auto. - - inv H. constructor. - - inv H. constructor. - - inv H. inv H3. - + apply IHp1 in H. solve [constructor; auto]. - + apply IHp2 in H. solve [constructor; auto]. - + apply IHp1 in H2. apply IHp2 in H4. solve [constructor; auto]. - - inv H. inv H3. - + apply IHp1 in H. solve [constructor; auto]. - + apply IHp2 in H. solve [constructor; auto]. - + apply IHp1 in H2. apply IHp2 in H4. solve [constructor; auto]. -Qed. - -Lemma sem_pexpr_negate2 : - forall A ctx p b, - @sem_pexpr A ctx (¬ p) (negb b) -> - sem_pexpr ctx p b. -Proof. - induction p; crush. - - destruct_match. destruct b0; crush. inv Heqp0. - constructor. inv H. rewrite negb_involutive in *. auto. - constructor. inv H. auto. - - inv H. destruct b; try discriminate. constructor. - - inv H. destruct b; try discriminate. constructor. - - inv H. destruct b; try discriminate. - + constructor. inv H1; eauto. - + destruct b; try discriminate. constructor; eauto. - - inv H. destruct b; try discriminate. - + constructor. inv H1; eauto. - + destruct b; try discriminate. constructor; eauto. -Qed. - Definition pred_expr_eqb: forall pe1 pe2: pred_expr, {pe1 = pe2} + {pe1 <> pe2}. Proof. @@ -1026,11 +846,6 @@ Definition beq_pred_pexpr (pe1 pe2: pred_pexpr): bool := let (np2, h') := hash_predicate 1 pe2 h in equiv_check np1 np2. -Definition check f1 f2 := - RTree.beq beq_pred_expr f1.(forest_regs) f2.(forest_regs) - && PTree.beq beq_pred_pexpr f1.(forest_preds) f2.(forest_preds) - && beq_pred_eexpr f1.(forest_exit) f2.(forest_exit). - Lemma inj_asgn_eg : forall a b, (a =? b)%positive = (a =? a)%positive -> a = b. Proof. intros. destruct (peq a b); subst. @@ -1344,6 +1159,501 @@ Section CORRECT. End CORRECT. +Section SEM_PRED_EXEC. + + Context (A: Type). + Context (ctx: @Abstr.ctx A). + + Lemma sem_pexpr_negate : + forall p b, + sem_pexpr ctx p b -> + sem_pexpr ctx (¬ p) (negb b). + Proof. + induction p; crush. + - destruct_match. destruct b0; crush. inv Heqp0. + constructor. inv H. rewrite negb_involutive. auto. + constructor. inv H. auto. + - inv H. constructor. + - inv H. constructor. + - inv H. inv H3. + + apply IHp1 in H. solve [constructor; auto]. + + apply IHp2 in H. solve [constructor; auto]. + + apply IHp1 in H2. apply IHp2 in H4. solve [constructor; auto]. + - inv H. inv H3. + + apply IHp1 in H. solve [constructor; auto]. + + apply IHp2 in H. solve [constructor; auto]. + + apply IHp1 in H2. apply IHp2 in H4. solve [constructor; auto]. + Qed. + + Lemma sem_pexpr_negate2 : + forall p b, + sem_pexpr ctx (¬ p) (negb b) -> + sem_pexpr ctx p b. + Proof. + induction p; crush. + - destruct_match. destruct b0; crush. inv Heqp0. + constructor. inv H. rewrite negb_involutive in *. auto. + constructor. inv H. auto. + - inv H. destruct b; try discriminate. constructor. + - inv H. destruct b; try discriminate. constructor. + - inv H. destruct b; try discriminate. + + constructor. inv H1; eauto. + + destruct b; try discriminate. constructor; eauto. + - inv H. destruct b; try discriminate. + + constructor. inv H1; eauto. + + destruct b; try discriminate. constructor; eauto. + Qed. + + Lemma sem_pexpr_evaluable : + forall f_p ps, + (forall x, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) -> + forall p, exists b, sem_pexpr ctx (from_pred_op f_p p) b. + Proof. + induction p; crush. + - destruct_match. inv Heqp0. destruct b. econstructor. eauto. + econstructor. eapply sem_pexpr_negate. eauto. + - econstructor. constructor. + - econstructor. constructor. + - destruct x0, x; solve [eexists; constructor; auto]. + - destruct x0, x; solve [eexists; constructor; auto]. + Qed. + + Lemma sem_pexpr_eval1 : + forall f_p ps, + (forall x, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) -> + forall p, + eval_predf ps p = false -> + sem_pexpr ctx (from_pred_op f_p p) false. + Proof. + induction p; crush. + - destruct_match. inv Heqp0. + destruct b. + + cbn in H0. rewrite <- H0. eauto. + + replace false with (negb true) by auto. + apply sem_pexpr_negate. cbn in H0. + apply negb_true_iff in H0. rewrite negb_involutive in H0. + rewrite <- H0. eauto. + - constructor. + - rewrite eval_predf_Pand in H0. + apply andb_false_iff in H0. inv H0. eapply IHp1 in H1. + pose proof (sem_pexpr_evaluable _ _ H p2) as EVAL. + inversion_clear EVAL as [x EVAL2]. + replace false with (false && x) by auto. + constructor; auto. + eapply IHp2 in H1. + pose proof (sem_pexpr_evaluable _ _ H p1) as EVAL. + inversion_clear EVAL as [x EVAL2]. + replace false with (x && false) by eauto with bool. + apply sem_pexpr_Pand; auto. + - rewrite eval_predf_Por in H0. + apply orb_false_iff in H0. inv H0. + replace false with (false || false) by auto. + apply sem_pexpr_Por; auto. + Qed. + + Lemma sem_pexpr_eval2 : + forall f_p ps, + (forall x, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) -> + forall p, + eval_predf ps p = true -> + sem_pexpr ctx (from_pred_op f_p p) true. + Proof. + induction p; crush. + - destruct_match. inv Heqp0. + destruct b. + + cbn in H0. rewrite <- H0. eauto. + + replace true with (negb false) by auto. + apply sem_pexpr_negate. cbn in H0. + apply negb_true_iff in H0. + rewrite <- H0. eauto. + - constructor. + - rewrite eval_predf_Pand in H0. + apply andb_true_iff in H0. inv H0. + replace true with (true && true) by auto. + constructor; auto. + - rewrite eval_predf_Por in H0. + apply orb_true_iff in H0. inv H0. eapply IHp1 in H1. + pose proof (sem_pexpr_evaluable _ _ H p2) as EVAL. + inversion_clear EVAL as [x EVAL2]. + replace true with (true || x) by auto. + apply sem_pexpr_Por; auto. + eapply IHp2 in H1. + pose proof (sem_pexpr_evaluable _ _ H p1) as EVAL. + inversion_clear EVAL as [x EVAL2]. + replace true with (x || true) by eauto with bool. + apply sem_pexpr_Por; auto. + Qed. + + Lemma sem_pexpr_eval : + forall f_p ps b, + (forall x, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) -> + forall p, + eval_predf ps p = b -> + sem_pexpr ctx (from_pred_op f_p p) b. + Proof. + intros; destruct b; eauto using sem_pexpr_eval1, sem_pexpr_eval2. + Qed. + + Lemma sem_pexpr_eval_inv : + forall f_p ps b, + (forall x, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) -> + forall p, + sem_pexpr ctx (from_pred_op f_p p) b -> + eval_predf ps p = b. + Proof. + induction p; intros. + - cbn in H0. destruct_match. destruct b0; cbn in *. + + specialize (H p0). eapply sem_pexpr_det; eauto. apply similar_refl. + + rewrite <- negb_involutive in H0. apply sem_pexpr_negate2 in H0. + symmetry; apply negb_sym. eapply sem_pexpr_det; eauto. + apply similar_refl. + - now inv H0. + - now inv H0. + - inv H0; try inv H4; rewrite eval_predf_Pand. + + apply IHp1 in H0. rewrite H0. auto. + + apply IHp2 in H0. rewrite H0. auto with bool. + + apply IHp2 in H5. apply IHp1 in H3. rewrite H3. rewrite H5. auto. + - inv H0; try inv H4; rewrite eval_predf_Por. + + apply IHp1 in H0. rewrite H0. auto. + + apply IHp2 in H0. rewrite H0. auto with bool. + + apply IHp2 in H5. apply IHp1 in H3. rewrite H3. rewrite H5. auto. + Qed. + + Context {C B: Type}. + Context (f: PTree.t pred_pexpr). + Context (ps: PMap.t bool). + Context (a_sem: @Abstr.ctx A -> C -> B -> Prop). + + Context (F_EVALULABLE: forall x, sem_pexpr ctx (get_forest_p' x f) ps !! x). + + Lemma sem_pexpr_equiv : + forall p1 p2 b, + p1 == p2 -> + sem_pexpr ctx (from_pred_op f p1) b -> + sem_pexpr ctx (from_pred_op f p2) b. + Proof. + intros. + eapply sem_pexpr_eval_inv in H0; eauto. + eapply sem_pexpr_eval; eauto. + Qed. + +End SEM_PRED_EXEC. + +Module HashExprNorm(H: Hashable). + Module H := HashTree(H). + + Definition norm_tree: Type := PTree.t pred_op * H.hash_tree. + + Fixpoint norm_expression (max: predicate) (pe: predicated H.t) (h: H.hash_tree) + : norm_tree := + match pe with + | NE.singleton (p, e) => + let (hashed_e, h') := H.hash_value max e h in + (PTree.set hashed_e p (PTree.empty _), h') + | (p, e) ::| pr => + let (hashed_e, h') := H.hash_value max e h in + let (norm_pr, h'') := norm_expression max pr h' in + match norm_pr ! hashed_e with + | Some pr_op => + (PTree.set hashed_e (pr_op ∨ p) norm_pr, h'') + | None => + (PTree.set hashed_e p norm_pr, h'') + end + end. + + Definition mk_pred_stmnt' (e: predicate) p_e := ¬ p_e ∨ Plit (true, e). + + Definition mk_pred_stmnt t := PTree.fold (fun x a b => mk_pred_stmnt' a b ∧ x) t T. + + Definition mk_pred_stmnt_l (t: list (predicate * pred_op)) := + fold_left (fun x a => uncurry mk_pred_stmnt' a ∧ x) t T. + + Definition encode_expression max pe h := + let (tree, h) := norm_expression max pe h in + (mk_pred_stmnt tree, h). + + Definition pred_expr_dec: forall pe1 pe2: predicated H.t, + {pe1 = pe2} + {pe1 <> pe2}. + Proof. + pose proof H.eq_dec as X. + pose proof (Predicate.eq_dec peq). + pose proof (NE.eq_dec _ X). + assert (forall a b: pred_op * H.t, {a = b} + {a <> b}) + by decide equality. + decide equality. + Defined. + + Definition beq_pred_expr' (pe1 pe2: predicated H.t) : bool := + if pred_expr_dec pe1 pe2 then true else + let (p1, h) := encode_expression 1%positive pe1 (PTree.empty _) in + let (p2, h') := encode_expression 1%positive pe2 h in + equiv_check p1 p2. + + Lemma mk_pred_stmnt_equiv' : + forall l l' e p, + mk_pred_stmnt_l l == mk_pred_stmnt_l l' -> + In (e, p) l -> + list_norepet (map fst l) -> + (exists p', In (e, p') l' /\ p == p') + \/ ~ In e (map fst l') /\ p == ⟂. + Proof. Abort. + + Lemma mk_pred_stmnt_equiv : + forall tree tree', + mk_pred_stmnt tree == mk_pred_stmnt tree'. + Proof. Abort. + + Definition tree_equiv_check_el (np2: PTree.t pred_op) (n: positive) (p: pred_op): bool := + match np2 ! n with + | Some p' => equiv_check p p' + | None => equiv_check p ⟂ + end. + + Definition tree_equiv_check_None_el (np2: PTree.t pred_op) (n: positive) (p: pred_op): bool := + match np2 ! n with + | Some p' => true + | None => equiv_check p ⟂ + end. + + Definition beq_pred_expr (pe1 pe2: predicated H.t) : bool := + if pred_expr_dec pe1 pe2 then true else + let (np1, h) := norm_expression 1 pe1 (PTree.empty _) in + let (np2, h') := norm_expression 1 pe2 h in + forall_ptree (tree_equiv_check_el np2) np1 + && forall_ptree (tree_equiv_check_None_el np1) np2. + + Lemma beq_pred_expr_correct: + forall np1 np2 e p p', + forall_ptree (tree_equiv_check_el np2) np1 = true -> + np1 ! e = Some p -> + np2 ! e = Some p' -> + p == p'. + Proof. + intros. + eapply forall_ptree_true in H; try eassumption. + unfold tree_equiv_check_el in H. + rewrite H1 in H. now apply equiv_check_correct. + Qed. + + Lemma beq_pred_expr_correct2: + forall np1 np2 e p, + forall_ptree (tree_equiv_check_el np2) np1 = true -> + np1 ! e = Some p -> + np2 ! e = None -> + p == ⟂. + Proof. + intros. + eapply forall_ptree_true in H; try eassumption. + unfold tree_equiv_check_el in H. + rewrite H1 in H. now apply equiv_check_correct. + Qed. + + Lemma beq_pred_expr_correct3: + forall np1 np2 e p, + forall_ptree (tree_equiv_check_None_el np1) np2 = true -> + np1 ! e = None -> + np2 ! e = Some p -> + p == ⟂. + Proof. + intros. + eapply forall_ptree_true in H; try eassumption. + unfold tree_equiv_check_None_el in H. + rewrite H0 in H. now apply equiv_check_correct. + Qed. + + Section PRED_PROOFS. + + Context {G B: Type}. + Context (f: PTree.t pred_pexpr). + Context (ps: PMap.t bool). + Context (a_sem: @Abstr.ctx G -> H.t -> B -> Prop). + Context (ctx: @Abstr.ctx G). + + Context (F_EVALULABLE: forall x, sem_pexpr ctx (get_forest_p' x f) ps !! x). + + Variant sem_pred_tree: PTree.t H.t -> PTree.t pred_op -> B -> Prop := + | sem_pred_tree_intro : + forall expr e v et pt pr, + sem_pexpr ctx (from_pred_op f pr) true -> + a_sem ctx expr v -> + pt ! e = Some pr -> + et ! e = Some expr -> + sem_pred_tree et pt v. + + Lemma norm_expression_wf : + forall pe et pt h, + H.wf_hash_table h -> + norm_expression 1 pe h = (pt, et) -> + H.wf_hash_table et. + Proof. Admitted. + + Lemma norm_expression_in : + forall pe et pt h x y, + H.wf_hash_table h -> + norm_expression 1 pe h = (pt, et) -> + h ! x = Some y -> + et ! x = Some y. + Proof. Admitted. + + Lemma norm_expression_in2 : + forall pe et pt h x y, + H.wf_hash_table h -> + norm_expression 1 pe h = (pt, et) -> + h ! x = Some y -> + et ! x = Some y. + Proof. Admitted. + + Lemma sem_pred_expr_in_true : + forall pe v, + sem_pred_expr f a_sem ctx pe v -> + exists p e, NE.In (p, e) pe + /\ sem_pexpr ctx (from_pred_op f p) true + /\ a_sem ctx e v. + Proof. + induction pe; crush. + - inv H. do 2 eexists; split; try split; eauto. constructor. + - inv H. + + do 2 eexists; split; try split; eauto. constructor; tauto. + + exploit IHpe; eauto. simplify. + do 2 eexists; split; try split; eauto. constructor; tauto. + Qed. + + Definition pred_Ht_dec : + forall x y: pred_op * H.t, {x = y} + {x <> y}. + Proof. + pose proof H.eq_dec. + pose proof (@Predicate.eq_dec positive peq). + decide equality. + Defined. + + Lemma sem_pred_mutexcl : + forall pe p t v, + predicated_mutexcl ((p, t) ::| pe) -> + sem_pred_expr f a_sem ctx pe v -> + sem_pexpr ctx (from_pred_op f p) false. + Proof. + intros. unfold predicated_mutexcl in H. + exploit sem_pred_expr_in_true; eauto; simplify. + unfold "⇒" in *. inv H5. + destruct (pred_Ht_dec (x, x0) (p, t)); subst. + { inv e; exfalso; apply H7; auto. } + assert (NE.In (x, x0) ((p, t) ::| pe)) by (constructor; tauto). + assert (NE.In (p, t) ((p, t) ::| pe)) by (constructor; tauto). + pose proof (H3 _ _ H H5 n). + assert (forall c, eval_predf c x = true -> eval_predf c (¬ p) = true) + by eauto. + eapply sem_pexpr_eval_inv in H1; eauto. + eapply sem_pexpr_eval; eauto. apply H9 in H1. + unfold eval_predf in *. rewrite negate_correct in H1. + symmetry in H1. apply negb_sym in H1. auto. + Qed. + + Lemma exec_tree_exec_pe : + forall pe et pt v h + (MUTEXCL: predicated_mutexcl pe), + H.wf_hash_table h -> + norm_expression 1 pe h = (pt, et) -> + sem_pred_tree et pt v -> + sem_pred_expr f a_sem ctx pe v. + Proof. + induction pe; simplify; repeat (destruct_match; try discriminate; []). + - inv Heqp. inv H0. inv H1. + destruct (peq e h0); subst. + 2: { rewrite PTree.gso in H3 by auto. + rewrite PTree.gempty in H3. discriminate. } + assert (expr = t). + { apply H.hash_value_in in Heqp0. rewrite H4 in Heqp0. now inv Heqp0. } + subst. constructor; auto. rewrite PTree.gss in H3. inv H3; auto. + - inv Heqp. inv H1. destruct_match; inv H0; destruct (peq h0 e); subst. + + rewrite PTree.gss in H4. inv H4. inv H2. inv H1. + * exploit IHpe. eauto using predicated_cons. + eapply H.wf_hash_table_distr; eauto. eauto. + econstructor. eauto. eauto. eauto. eauto. intros. + assert (sem_pexpr ctx (from_pred_op f p) false) + by (eapply sem_pred_mutexcl; eauto). + eapply sem_pred_expr_cons_false; auto. + * assert (et ! e = Some t). + { eapply norm_expression_in. eapply H.wf_hash_table_distr; eauto. + eauto. apply H.hash_value_in in Heqp0. auto. } + rewrite H1 in H5. inv H5. + constructor; auto. + + exploit IHpe. eauto using predicated_cons. + eapply H.wf_hash_table_distr; eauto. eauto. + econstructor. eauto. eauto. rewrite PTree.gso in H4; eauto. auto. + intros. + assert (sem_pexpr ctx (from_pred_op f p) false) + by (eapply sem_pred_mutexcl; eauto). + eapply sem_pred_expr_cons_false; auto. + + rewrite PTree.gss in H4. inv H4. + econstructor; auto. + assert (et ! e = Some t). + { eapply norm_expression_in. eapply H.wf_hash_table_distr; eauto. + eauto. apply H.hash_value_in in Heqp0. auto. } + rewrite H0 in H5; inv H5. auto. + + rewrite PTree.gso in H4 by auto. + exploit IHpe. eauto using predicated_cons. + eapply H.wf_hash_table_distr; eauto. eauto. + econstructor. eauto. eauto. eauto. eauto. intros. + assert (sem_pexpr ctx (from_pred_op f p) false) + by (eapply sem_pred_mutexcl; eauto). + eapply sem_pred_expr_cons_false; auto. + Qed. + + Lemma exec_pe_exec_tree : + forall pe et pt v h + (MUTEXCL: predicated_mutexcl pe), + H.wf_hash_table h -> + norm_expression 1 pe h = (pt, et) -> + sem_pred_expr f a_sem ctx pe v -> + sem_pred_tree et pt v. + Proof. + induction pe; simplify; repeat (destruct_match; try discriminate; []). + - inv H0. inv H1. econstructor; eauto. apply PTree.gss. + eapply H.hash_value_in; eauto. + - inv H1. + + destruct_match. + * inv H0. econstructor. + 2: { eauto. } + 2: { apply PTree.gss. } + constructor; tauto. + eapply norm_expression_in. eapply H.wf_hash_table_distr; eauto. + eauto. eapply H.hash_value_in; eauto. + * inv H0. econstructor. eauto. eauto. apply PTree.gss. + eapply norm_expression_in. eapply H.wf_hash_table_distr; eauto. + eauto. eapply H.hash_value_in; eauto. + + destruct_match. + * inv H0. exploit IHpe. + eauto using predicated_cons. + eapply H.wf_hash_table_distr; eauto. + eauto. eauto. intros. inv H0. + destruct (peq e h0); subst. + -- rewrite H3 in Heqo. inv Heqo. + econstructor. + 3: { apply PTree.gss. } + constructor; tauto. eauto. auto. + -- econstructor. eauto. eauto. rewrite PTree.gso by eauto. auto. + auto. + * inv H0. exploit IHpe. + eauto using predicated_cons. + eapply H.wf_hash_table_distr; eauto. + eauto. eauto. intros. inv H0. + destruct (peq e h0); subst. + -- rewrite H3 in Heqo; discriminate. + -- econstructor; eauto. rewrite PTree.gso by auto. auto. + Qed. + + End PRED_PROOFS. + +End HashExprNorm. + +Module HN := HashExprNorm(HashExpr). +Module EHN := HashExprNorm(EHashExpr). + +Definition check f1 f2 := + RTree.beq beq_pred_expr f1.(forest_regs) f2.(forest_regs) + && PTree.beq beq_pred_pexpr f1.(forest_preds) f2.(forest_preds) + && beq_pred_eexpr f1.(forest_exit) f2.(forest_exit). + Lemma sem_pexpr_forward_eval1 : forall A ctx f_p ps, (forall x, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) -> diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index 6bfc654..caad4b5 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -552,96 +552,6 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. rewrite eval_predf_negate. rewrite H0. auto. Qed. - Lemma sem_pexpr_evaluable : - forall A ctx f_p ps, - (forall x, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) -> - forall p, exists b, @sem_pexpr A ctx (from_pred_op f_p p) b. - Proof. - induction p; crush. - - destruct_match. inv Heqp0. destruct b. econstructor. eauto. - econstructor. eapply sem_pexpr_negate. eauto. - - econstructor. constructor. - - econstructor. constructor. - - destruct x0, x; solve [eexists; constructor; auto]. - - destruct x0, x; solve [eexists; constructor; auto]. - Qed. - - Lemma sem_pexpr_eval1 : - forall A ctx f_p ps, - (forall x, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) -> - forall p, - eval_predf ps p = false -> - @sem_pexpr A ctx (from_pred_op f_p p) false. - Proof. - induction p; crush. - - destruct_match. inv Heqp0. - destruct b. - + cbn in H0. rewrite <- H0. eauto. - + replace false with (negb true) by auto. - apply sem_pexpr_negate. cbn in H0. - apply negb_true_iff in H0. rewrite negb_involutive in H0. - rewrite <- H0. eauto. - - constructor. - - rewrite eval_predf_Pand in H0. - apply andb_false_iff in H0. inv H0. eapply IHp1 in H1. - pose proof (sem_pexpr_evaluable _ _ _ _ H p2) as EVAL. - inversion_clear EVAL as [x EVAL2]. - replace false with (false && x) by auto. - constructor; auto. - eapply IHp2 in H1. - pose proof (sem_pexpr_evaluable _ _ _ _ H p1) as EVAL. - inversion_clear EVAL as [x EVAL2]. - replace false with (x && false) by eauto with bool. - apply sem_pexpr_Pand; auto. - - rewrite eval_predf_Por in H0. - apply orb_false_iff in H0. inv H0. - replace false with (false || false) by auto. - apply sem_pexpr_Por; auto. - Qed. - - Lemma sem_pexpr_eval2 : - forall A ctx f_p ps, - (forall x, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) -> - forall p, - eval_predf ps p = true -> - @sem_pexpr A ctx (from_pred_op f_p p) true. - Proof. - induction p; crush. - - destruct_match. inv Heqp0. - destruct b. - + cbn in H0. rewrite <- H0. eauto. - + replace true with (negb false) by auto. - apply sem_pexpr_negate. cbn in H0. - apply negb_true_iff in H0. - rewrite <- H0. eauto. - - constructor. - - rewrite eval_predf_Pand in H0. - apply andb_true_iff in H0. inv H0. - replace true with (true && true) by auto. - constructor; auto. - - rewrite eval_predf_Por in H0. - apply orb_true_iff in H0. inv H0. eapply IHp1 in H1. - pose proof (sem_pexpr_evaluable _ _ _ _ H p2) as EVAL. - inversion_clear EVAL as [x EVAL2]. - replace true with (true || x) by auto. - apply sem_pexpr_Por; auto. - eapply IHp2 in H1. - pose proof (sem_pexpr_evaluable _ _ _ _ H p1) as EVAL. - inversion_clear EVAL as [x EVAL2]. - replace true with (x || true) by eauto with bool. - apply sem_pexpr_Por; auto. - Qed. - - Lemma sem_pexpr_eval : - forall A ctx f_p ps b, - (forall x, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) -> - forall p, - eval_predf ps p = b -> - @sem_pexpr A ctx (from_pred_op f_p p) b. - Proof. - intros; destruct b; eauto using sem_pexpr_eval1, sem_pexpr_eval2. - Qed. - Lemma sem_pred_expr_NEapp : forall A B C sem f_p ctx a b v, sem_pred_expr f_p sem ctx a v -> diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v index 08ce47b..f99fa4f 100644 --- a/src/hls/Predicate.v +++ b/src/hls/Predicate.v @@ -737,14 +737,6 @@ Proof. rewrite <- simplify_correct. eauto. Qed. -Lemma equiv_check_destr : - forall p1 p2 p1' p2', - Pand p1 p2 == Pand p1' p2' -> - p1 == p1' /\ p2 == p2' - \/ p1 == p2' /\ p2 == p1'. -Proof. - induction p1. intros; cbn in *; unfold sat_equiv in *; cbn in *. - Opaque simplify. Opaque simplify'. -- cgit