Finish mutual exclusivity check

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].