diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-09-17 12:09:25 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-09-17 12:09:25 +0100 |
commit | 6a74d2e648903e54300f276a024e396978629b30 (patch) | |
tree | 09ca1e0a809df82c01338d313857a4562bdf8f74 /src/hls/GiblePargenproofEquiv.v | |
parent | c9d0a0bea2f547a9706e9524f20baf9778df805a (diff) | |
download | vericert-6a74d2e648903e54300f276a024e396978629b30.tar.gz vericert-6a74d2e648903e54300f276a024e396978629b30.zip |
Add unhashed functions for comparisons
Diffstat (limited to 'src/hls/GiblePargenproofEquiv.v')
-rw-r--r-- | src/hls/GiblePargenproofEquiv.v | 47 |
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, |