Add unhashed functions for comparisons

1 files changed, 47 insertions, 0 deletions

diff --git a/src/hls/GiblePargenproofEquiv.v b/src/hls/GiblePargenproofEquiv.v
index df14e31..262e9d5 100644
--- a/src/hls/GiblePargenproofEquiv.v
+++ b/src/hls/GiblePargenproofEquiv.v
@@ -1177,18 +1177,37 @@ Module HashExprNorm(HS: Hashable).
       mk_pred_stmnt tree == mk_pred_stmnt tree'.
   Proof. Abort.
 
+  Definition equiv_check_unhashed (pe1 pe2: pred_pexpr) :=
+    if pred_pexpr_eqb pe1 pe2 then true else
+    let (np1, h) := TVL.hash_predicate (transf_pred_op (simplify pe1)) (Maps.PTree.empty _) in
+    let (np2, h') := TVL.hash_predicate (transf_pred_op (simplify pe2)) h in
+    STV.check_smt_total (TV.equiv np1 np2).
+
   Definition tree_equiv_check_el eq_list (np2: PTree.t pred_op) (n: positive) (p: pred_op): bool :=
     match np2 ! n with
     | Some p' => equiv_check_eq_list eq_list p p'
     | None => equiv_check_eq_list eq_list p ⟂
     end.
 
+  Definition tree_equiv_check_el_unhashed (pexpr pexpr': PTree.t pred_pexpr) 
+      (np2: PTree.t pred_op) (n: positive) (p: pred_op): bool :=
+    match np2 ! n with
+    | Some p' => equiv_check_unhashed (from_pred_op pexpr p) (from_pred_op pexpr' p')
+    | None => equiv_check_unhashed (from_pred_op pexpr p) ⟂
+    end.
+
   Definition tree_equiv_check_None_el eq_list (np2: PTree.t pred_op) (n: positive) (p: pred_op): bool :=
     match np2 ! n with
     | Some p' => true
     | None => equiv_check_eq_list eq_list p ⟂
     end.
 
+  Definition tree_equiv_check_None_el_unhashed (pexpr pexpr': PTree.t pred_pexpr) (np2: PTree.t pred_op) (n: positive) (p: pred_op): bool :=
+    match np2 ! n with
+    | Some p' => true
+    | None => equiv_check_unhashed (from_pred_op pexpr p) ⟂
+    end.
+
   Definition beq_pred_expr eq_list (pe1 pe2: predicated HS.t) : bool :=
     if pred_expr_dec pe1 pe2 then true else
     let (np1, h) := norm_expression 1 pe1 (PTree.empty _) in
@@ -1196,6 +1215,13 @@ Module HashExprNorm(HS: Hashable).
     forall_ptree (tree_equiv_check_el eq_list np2) np1
     && forall_ptree (tree_equiv_check_None_el eq_list np1) np2.
 
+  Definition beq_pred_expr_unhashed (preds preds': PTree.t pred_pexpr) (pe1 pe2: predicated HS.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_unhashed preds preds' np2) np1
+    && forall_ptree (tree_equiv_check_None_el_unhashed preds preds' np1) np2.
+
   Lemma beq_pred_expr_correct:
     forall eq_list np1 np2 e p p' c,
       sat_predicate (eq_list_to_pred_op eq_list) c = true ->
@@ -1520,6 +1546,14 @@ Definition check_mutexcl {A} eq_dec (pe: predicated A) :=
     end
   else false.
 
+Definition check_mutexcl_unhashed {A} eq_dec (preds: PTree.t pred_pexpr) (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
+    let (np1, h) := TVL.hash_predicate (transf_pred_op (from_pred_op preds (simplify (and_list pairs)))) (Maps.PTree.empty _) in
+    STV.check_smt_total np1
+  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)])). *)
 
@@ -1610,6 +1644,9 @@ Qed.
 Definition check_mutexcl_tree {A} eq_dec (f: PTree.t (predicated A)) :=
   forall_ptree (fun _ => check_mutexcl eq_dec) f.
 
+Definition check_mutexcl_tree_unhashed {A} eq_dec preds (f: PTree.t (predicated A)) :=
+  forall_ptree (fun _ => check_mutexcl_unhashed preds eq_dec) f.
+
 Lemma check_mutexcl_tree_correct:
   forall A eq_dec (f: PTree.t (predicated A)) i pe,
     check_mutexcl_tree eq_dec f = true ->
@@ -1649,6 +1686,16 @@ Definition check (eq_list: list (positive * positive)) f1 f2 :=
   && check_mutexcl EHN.pred_Ht_dec f1.(forest_exit)
   && check_mutexcl EHN.pred_Ht_dec f2.(forest_exit)
   && (forallb (fun x => beq_pred_pexpr (f1 #p (fst x)) (f1 #p (snd x))) eq_list).
+  
+Definition check_unhashed (eq_list: list (positive * positive)) f1 f2 :=
+  RTree.beq (HN.beq_pred_expr_unhashed f1.(forest_preds) f2.(forest_preds)) f1.(forest_regs) f2.(forest_regs)
+  && PTree.beq beq_pred_pexpr f1.(forest_preds) f2.(forest_preds)
+  && EHN.beq_pred_expr_unhashed f1.(forest_preds) f2.(forest_preds) f1.(forest_exit) f2.(forest_exit)
+  && check_mutexcl_tree_unhashed f1.(forest_preds) HN.pred_Ht_dec f1.(forest_regs)
+  && check_mutexcl_tree_unhashed f2.(forest_preds) HN.pred_Ht_dec f2.(forest_regs)
+  && check_mutexcl_unhashed EHN.pred_Ht_dec f1.(forest_preds) f1.(forest_exit)
+  && check_mutexcl_unhashed EHN.pred_Ht_dec f2.(forest_preds) f2.(forest_exit)
+  && (forallb (fun x => beq_pred_pexpr (f1 #p (fst x)) (f1 #p (snd x))) eq_list).
 
 Lemma sem_pexpr_forward_eval1 :
   forall A ctx f_p ps,