From e9f748f8e302f4d9977661e9c51ddaf5410bdec6 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 25 Jun 2023 17:53:22 +0100 Subject: Finish mutual exclusivity check --- src/common/NonEmpty.v | 30 ++++++++- src/hls/GiblePargen.v | 16 +++-- src/hls/GiblePargenproofBackward.v | 4 +- src/hls/GiblePargenproofEquiv.v | 127 +++++++++++++++++++++++++++++++------ src/hls/GiblePargenproofForward.v | 4 +- 5 files changed, 150 insertions(+), 31 deletions(-) diff --git a/src/common/NonEmpty.v b/src/common/NonEmpty.v index 24a29a3..01456d0 100644 --- a/src/common/NonEmpty.v +++ b/src/common/NonEmpty.v @@ -97,7 +97,7 @@ Inductive In {A: Type} (x: A) : non_empty A -> Prop := Ltac inv X := inversion X; clear X; subst. -Lemma in_dec: +Definition in_dec: forall A (a: A) (l: non_empty A), (forall a b: A, {a = b} + {a <> b}) -> {In a l} + {~ In a l}. @@ -338,3 +338,31 @@ Proof. + exists a; split; auto; constructor; tauto. + exploit IHn; eauto; simplify. exists x0; split; auto; constructor; tauto. Qed. + +Fixpoint norepet_check {A} eq_dec (ne: non_empty A) := + match ne with + | singleton a => true + | a ::| b => + if in_dec A a b eq_dec then false + else norepet_check eq_dec b + end. + +Lemma norepet_check_correct : + forall A eq_dec ne, + @norepet_check A eq_dec ne = true -> + norepet ne. +Proof. + induction ne; intros; [constructor|]. + cbn in H. destruct_match; [discriminate|]. + constructor; auto. +Qed. + +Lemma to_list_in : + forall A ne (x: A), + In x ne -> + List.In x (to_list ne). +Proof. + induction ne. + - intros. inv H. cbn; tauto. + - intros; cbn. inv H. inv H1; eauto. +Qed. diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index 25531a8..3cf2401 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -238,6 +238,12 @@ Definition predicated_not_in_forest (p: Gible.predicate) (f: forest) := predicated_not_in_pred_expr p f.(forest_regs) && predicated_not_in p f.(forest_exit). +Definition pred_expr_dec: forall a b: pred_op * pred_expression, {a = b} + {a <> b}. +Proof. + intros. destruct a, b. + apply pred_pexpression_dec. +Defined. + Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest) := let (pred, f) := fop in match i with @@ -279,7 +285,7 @@ Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest → from_predicated true f.(forest_preds) predicated) ∧ (from_pred_op f.(forest_preds) (¬ (dfltp p') ∨ ¬ pred) → (f #p p)) in - do _ <- assert_ (check_mutexcl predicated); + do _ <- assert_ (check_mutexcl pred_expr_dec predicated); do _ <- assert_ (predicated_not_in_forest p f); do _ <- assert_ (is_initial_pred_and_notin f p pred); do _ <- assert_ (match sat_pred_simple (¬ from_predicated_inv predicated) with None => true | Some _ => false end); @@ -417,15 +423,15 @@ Definition check_evaluability1 a b := existsb (fun ae => resource_eq (fst ae) (fst be) && HN.beq_pred_expr (snd ae) (snd be) - && check_mutexcl (snd ae) - && check_mutexcl (snd be) + && check_mutexcl HN.pred_Ht_dec (snd ae) + && check_mutexcl HN.pred_Ht_dec (snd be) ) a ) b. Definition check_evaluability2 a b := forallb (fun be => existsb (fun ae => HN.beq_pred_expr ae be - && check_mutexcl ae - && check_mutexcl be) a) b. + && check_mutexcl HN.pred_Ht_dec ae + && check_mutexcl HN.pred_Ht_dec be) a) b. Definition schedule_oracle (bb: SeqBB.t) (bbt: ParBB.t) : bool := match abstract_sequence_top bb, abstract_sequence_top (concat (concat bbt)) with diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v index 4b14234..43e97a6 100644 --- a/src/hls/GiblePargenproofBackward.v +++ b/src/hls/GiblePargenproofBackward.v @@ -361,7 +361,7 @@ Proof. exploit from_predicated_sem_pred_expr2. 3: eauto. { eauto. } - { unfold assert_ in Heqo. clear Heqo2. destr. now eapply check_mutexcl_correct. } + { unfold assert_ in Heqo. clear Heqo2. destr. eauto using check_mutexcl_correct. } { unfold assert_ in Heqo2. repeat destr. unfold sat_pred_simple in Heqo3. destruct (sat_pred_tseytin (¬ from_predicated_inv (seq_app (pred_ret (PEsetpred c)) (merge (list_translation args f))))); [destruct s; discriminate|]. rewrite <- negb_involutive. symmetry. rewrite <- negb_involutive. rewrite <- eval_predf_negate. f_equal. eauto. @@ -406,7 +406,7 @@ Proof. exploit from_predicated_sem_pred_expr2. 3: eauto. { eauto. } - { unfold assert_ in Heqo. clear Heqo2. destr. now apply check_mutexcl_correct. } + { unfold assert_ in Heqo. clear Heqo2. destr. eauto using check_mutexcl_correct. } { unfold assert_ in Heqo2. repeat destr. unfold sat_pred_simple in Heqo3. destruct (sat_pred_tseytin (¬ from_predicated_inv (seq_app (pred_ret (PEsetpred c)) (merge (list_translation args f))))); [destruct s; discriminate|]. rewrite <- negb_involutive. symmetry. rewrite <- negb_involutive. rewrite <- eval_predf_negate. f_equal. eauto. diff --git a/src/hls/GiblePargenproofEquiv.v b/src/hls/GiblePargenproofEquiv.v index 20b43be..91688a0 100644 --- a/src/hls/GiblePargenproofEquiv.v +++ b/src/hls/GiblePargenproofEquiv.v @@ -234,6 +234,15 @@ Proof. eauto using beq_pred_expression_correct2. Defined. +Lemma pred_pexpression_dec: + forall (e1 e2: pred_expression) (p1 p2: pred_op), + {(p1, e1) = (p2, e2)} + {(p1, e1) <> (p2, e2)}. +Proof. + pose proof (Predicate.eq_dec peq). + pose proof (pred_expression_dec). + decide equality. +Defined. + Lemma exit_expression_refl: forall e, beq_exit_expression e e = true. Proof. destruct e; crush; destruct_match; crush. Qed. @@ -437,7 +446,7 @@ Lemma existsh : forall ap1, exists h p1, hash_predicate 1 ap1 h = (p1, h). -Proof. Admitted. +Proof. Abort. Lemma aequiv_refl : forall a, sat_aequiv a a. Proof. @@ -1495,33 +1504,109 @@ End HashExprNorm. Module HN := HashExprNorm(HashExpr). Module EHN := HashExprNorm(EHashExpr). -Definition check_mutexcl {A} (pe: predicated A) := - let preds := map fst (NE.to_list pe) in - let pairs := map (fun x => x → negate (or_list (remove (Predicate.eq_dec peq) x preds))) preds in - match sat_pred_simple (simplify (negate (and_list pairs))) with - | None => true - | _ => false - end. +Definition check_mutexcl {A} eq_dec (pe: predicated A) := + if NE.norepet_check eq_dec pe then + let lpe := NE.to_list pe in + let pairs := map (fun x => fst x → negate (or_list (map fst (remove eq_dec x lpe)))) lpe in + match sat_pred_simple (simplify (negate (and_list pairs))) with + | None => true + | _ => false + end + else false. (* Import ListNotations. *) (* Compute deep_simplify peq (and_list (map (fun x => x → negate (or_list (remove (Predicate.eq_dec peq) x [Plit (true, 2)]))) [Plit (true, 2)])). *) +Lemma and_list_correct': + forall l a t, + sat_predicate (fold_left Pand l t) a = true -> + Forall (fun p => sat_predicate p a = true) l /\ sat_predicate t a = true. +Proof. + induction l. + - cbn; intros. split; auto. + - cbn; intros. + exploit IHl; eauto. simplify; auto. +Qed. + +Lemma and_list_correct: + forall l a, + sat_predicate (and_list l) a = true -> + Forall (fun p => sat_predicate p a = true) l. +Proof. intros. eapply and_list_correct'; eauto. Qed. + +Lemma or_list_correct': + forall l a t, + sat_predicate (fold_left Por l t) a = false -> + Forall (fun p => sat_predicate p a = false) l /\ sat_predicate t a = false. +Proof. + induction l. + - cbn; intros. split; auto. + - cbn; intros. + exploit IHl; eauto. simplify; auto. +Qed. + +Lemma or_list_correct: + forall a l, + sat_predicate (or_list l) a = false -> + Forall (fun p => sat_predicate p a = false) l. +Proof. intros. eapply or_list_correct'; eauto. Qed. + Lemma check_mutexcl_correct: - forall A (pe: predicated A), - check_mutexcl pe = true -> + forall A eq_dec (pe: predicated A), + check_mutexcl eq_dec pe = true -> predicated_mutexcl pe. -Proof. Admitted. +Proof. + unfold predicated_mutexcl, check_mutexcl; intros. + repeat (destruct_match; try discriminate; []); subst. + unfold sat_pred_simple in Heqo. + destruct_match; [destruct s; discriminate|]. + clear H Heqo Heqs. + unfold "⇒"; split; intros. + specialize (e c). + rewrite simplify_correct in e. + rewrite negate_correct in e. + replace false with (negb true) in e by auto. + apply negb_inj in e. + apply and_list_correct in e. + eapply Forall_forall in e. + 2: { + instantiate (1 := (fun x0 : Predicate.pred_op * A => + fst x0 → ¬ or_list (map fst (remove eq_dec x0 (NE.to_list pe)))) x); + auto using in_map, NE.to_list_in. + } + unfold "→" in e. cbn in e. + rewrite negate_correct in e. setoid_rewrite H2 in e. cbn in e. + rewrite negate_correct in e. + replace true with (negb false) in e by auto. + apply negb_inj in e. + rewrite negate_correct. replace true with (negb false) by auto. + f_equal. apply or_list_correct in e. + eapply Forall_forall in e. + 2: { + instantiate (1 := fst y); auto using in_map, in_in_remove, NE.to_list_in. + } + auto. + eauto using NE.norepet_check_correct. +Qed. Lemma check_mutexcl_singleton : - check_mutexcl (NE.singleton (T, EEbase)) = true. -Proof. crush. Qed. + forall A eq_dec (a: A), check_mutexcl eq_dec (NE.singleton (T, a)) = true. +Proof. + unfold check_mutexcl; cbn -[simplify]; intros. + destruct_match; auto. + unfold sat_pred_simple in Heqo. destruct_match; try discriminate. + destruct s. inv Heqo. clear Heqs. + rewrite simplify_correct in e. cbn in e. + rewrite ! negate_correct in e. rewrite negb_involutive in e. + destruct_match; auto. +Qed. -Definition check_mutexcl_tree {A} (f: PTree.t (predicated A)) := - forall_ptree (fun _ => check_mutexcl) f. +Definition check_mutexcl_tree {A} eq_dec (f: PTree.t (predicated A)) := + forall_ptree (fun _ => check_mutexcl eq_dec) f. Lemma check_mutexcl_tree_correct: - forall A (f: PTree.t (predicated A)) i pe, - check_mutexcl_tree f = true -> + forall A eq_dec (f: PTree.t (predicated A)) i pe, + check_mutexcl_tree eq_dec f = true -> f ! i = Some pe -> predicated_mutexcl pe. Proof. @@ -1533,10 +1618,10 @@ Definition check f1 f2 := RTree.beq HN.beq_pred_expr f1.(forest_regs) f2.(forest_regs) && PTree.beq beq_pred_pexpr f1.(forest_preds) f2.(forest_preds) && EHN.beq_pred_expr f1.(forest_exit) f2.(forest_exit) - && check_mutexcl_tree f1.(forest_regs) - && check_mutexcl_tree f2.(forest_regs) - && check_mutexcl f1.(forest_exit) - && check_mutexcl f2.(forest_exit). + && check_mutexcl_tree HN.pred_Ht_dec f1.(forest_regs) + && check_mutexcl_tree HN.pred_Ht_dec f2.(forest_regs) + && check_mutexcl EHN.pred_Ht_dec f1.(forest_exit) + && check_mutexcl EHN.pred_Ht_dec f2.(forest_exit). Lemma sem_pexpr_forward_eval1 : forall A ctx f_p ps, diff --git a/src/hls/GiblePargenproofForward.v b/src/hls/GiblePargenproofForward.v index 3d0f7d5..946a243 100644 --- a/src/hls/GiblePargenproofForward.v +++ b/src/hls/GiblePargenproofForward.v @@ -421,7 +421,7 @@ all be evaluable. apply sem_pexpr_Pand. destruct b. constructor. right. eapply sem_update_Isetpred; eauto. - { unfold assert_ in Heqo. destr. auto using check_mutexcl_correct. } + { unfold assert_ in Heqo. destr. eauto using check_mutexcl_correct. } constructor. constructor. replace false with (negb true) by auto. apply sem_pexpr_negate. inv TRUTHY. constructor. cbn. eapply sem_pexpr_eval. inv PRED. eauto. auto. @@ -429,7 +429,7 @@ all be evaluable. apply sem_pexpr_negate. eapply sem_pexpr_eval. inv PRED. eauto. auto. eapply sem_update_Isetpred; eauto. - { unfold assert_ in Heqo. destr. auto using check_mutexcl_correct. } + { unfold assert_ in Heqo. destr. eauto using check_mutexcl_correct. } constructor. constructor. constructor. replace true with (negb false) by auto. apply sem_pexpr_negate. eapply sem_pexpr_eval. inv PRED. eauto. inv TRUTHY. auto. cbn -[eval_predf]. -- cgit