diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-07-11 15:45:59 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-07-11 16:25:09 +0100 |
commit | 93117b6e766c25c5aeecdc20a963d5114fb91e59 (patch) | |
tree | 60e77f4d09548b3fa077d96e7d0e26fd8b0ad1ef | |
parent | 6cdb6490437b9e609afbf5e8749b24d31c02fce1 (diff) | |
download | vericert-93117b6e766c25c5aeecdc20a963d5114fb91e59.tar.gz vericert-93117b6e766c25c5aeecdc20a963d5114fb91e59.zip |
Add equivalence classes
-rw-r--r-- | .gitignore | 1 | ||||
-rw-r--r-- | Makefile | 6 | ||||
-rw-r--r-- | debug/dune | 6 | ||||
-rw-r--r-- | debug/vericertTest.ml | 206 | ||||
-rw-r--r-- | src/hls/GiblePargen.v | 23 | ||||
-rw-r--r-- | src/hls/GiblePargenproof.v | 2 | ||||
-rw-r--r-- | src/hls/GiblePargenproofCommon.v | 25 | ||||
-rw-r--r-- | src/hls/GiblePargenproofEquiv.v | 343 | ||||
-rw-r--r-- | src/hls/GiblePargenproofForward.v | 99 | ||||
-rw-r--r-- | src/hls/Predicate.v | 33 |
10 files changed, 552 insertions, 192 deletions
@@ -45,7 +45,6 @@ _build /docs/html .DS_Store -debug/* # CompCert *.rtl.* @@ -55,6 +55,12 @@ install: doc/vericert.1 install -d $(PREFIX)/share/man/man1 install -C -m 644 $< $(PREFIX)/share/man/man1 +install-test: # doc/vericert.1 + sed -i'' -e 's/arch=verilog/arch=x86/' _build/default/driver/compcert.ini + install -d $(PREFIX)/bin + install -C -m 644 _build/default/driver/compcert.ini $(PREFIX)/bin + install -C _build/default/debug/VericertTest.exe $(PREFIX)/bin/vericert-test + proof: Makefile.coq $(MAKE) -f Makefile.coq @rm -f src/extraction/STAMP diff --git a/debug/dune b/debug/dune new file mode 100644 index 0000000..e47c832 --- /dev/null +++ b/debug/dune @@ -0,0 +1,6 @@ +(include_subdirs no) + +(executable + (name VericertTest) + (libraries vericert) + (flags (:standard -warn-error -A -w -8-9-16-20-26-27-32..36-39-41-44..45-50-60-67))) diff --git a/debug/vericertTest.ml b/debug/vericertTest.ml new file mode 100644 index 0000000..4d4e55f --- /dev/null +++ b/debug/vericertTest.ml @@ -0,0 +1,206 @@ +open Vericert + +open AST +open Abstr +open BinNums +open Coqlib +open Datatypes +open Errors +open GiblePargenproofEquiv +open List0 +open Maps +open Optionmonad +open Predicate +open GiblePargen +open Integers +open Op +open Printf + +let schedule_oracle l bb bbt = + match abstract_sequence_top bb with + | Some p -> + let (p0, m_expr) = p in + let (bb', reg_expr) = p0 in + (match abstract_sequence_top (concat (concat bbt)) with + | Some p1 -> + let (p2, m_expr_t) = p1 in + let (bbt', reg_expr_t) = p2 in + printf "F1:\n%a\n" PrintAbstr.print_forest bb'; + printf "F2:\n%a\n" PrintAbstr.print_forest bbt'; flush stdout; + (&&) + ((&&) ((&&) (if check l bb' bbt' then true else (Printf.printf "Failed 1\n"; false)) (empty_trees bb bbt)) + (if (check_evaluability1 reg_expr reg_expr_t) then true else (Printf.printf "Failed 12\n"; false))) + (if check_evaluability2 m_expr m_expr_t then true else (Printf.printf "Failed 13\n"; false)) + | None -> (printf "FAILED1\n"; false)) + | None -> (printf "FAILED2\n"; false) + +(** val check_scheduled_trees : + GibleSeq.SeqBB.t PTree.t -> GiblePar.ParBB.t PTree.t -> bool **) + +let z = Camlcoq.Z.of_sint +let int n = Int.repr (z n) +let reg = Camlcoq.P.of_int +let pred = Camlcoq.P.of_int +let node = Camlcoq.P.of_int +let plit b p = Plit (b, pred p) + +let const p d c: Gible.instr = RBop (p, Ointconst (z c), [], reg d) +let add p d1 r1 r2: Gible.instr = RBop (p, Olea (Aindexed2 (z 0)), [reg r1; reg r2], reg d1) +let mul p d1 r1 r2: Gible.instr = RBop (p, Omul, [reg r1; reg r2], reg d1) +let div p d1 r1 r2: Gible.instr = RBop (p, Odiv, [reg r1; reg r2], reg d1) +let seteq p d1 r1 r2: Gible.instr = RBsetpred (p, Ccomp Ceq, [reg r1; reg r2], pred d1) +let sett p d1 r1: Gible.instr = RBsetpred (p, Ccompimm (Ceq, int 0), [reg r1], pred d1) +let goto p n: Gible.instr = RBexit (p, (RBgoto (node n))) + +let () = + (* (if schedule_oracle [] *) + (* [ add None 2 1 4; *) + (* seteq (Some (plit true 1)) 3 4 2; *) + (* add (Some (plit true 1)) 1 2 4; *) + (* mul (Some (Pand (plit false 1, plit false 2))) 3 1 1; *) + (* mul (Some (plit true 2)) 3 1 4; *) + (* goto (Some (plit true 2)) 10; *) + (* mul (Some (plit false 2)) 3 3 3; *) + (* goto None 10; *) + (* ] *) + (* [ [ [ mul (Some (Pand (plit false 1, plit false 2))) 3 1 1; ]; *) + (* [ add None 2 1 4; *) + (* add (Some (plit true 1)) 1 2 4; *) + (* seteq (Some (plit true 1)) 3 4 2; ] ]; *) + (* [ [ mul (Some (plit true 2)) 3 1 4; ]; *) + (* [ mul (Some (plit false 2)) 3 3 3; ]; *) + (* [ goto None 10; ] *) + (* ] *) + (* ] *) + (* then Printf.printf "Passed 1\n" *) + (* else Printf.printf "Failed 1\n"); *) + (* (if schedule_oracle [] *) + (* [ seteq (Some (plit true 1)) 2 1 2; *) + (* goto None 10; *) + (* ] *) + (* [ [ [ goto (Some (plit false 1)) 10; *) + (* seteq None 2 1 2; *) + (* goto None 10; *) + (* ] ] ] *) + (* then Printf.printf "Passed 1\n" *) + (* else Printf.printf "Failed 1\n"); *) + (* (if schedule_oracle [] *) + (* [ seteq None 2 1 2; *) + (* seteq None 3 1 2; *) + (* seteq (Some (Por (plit true 2, plit false 3))) 4 1 3; *) + (* ] *) + (* [ [ [ seteq None 2 1 2; *) + (* seteq None 3 1 2; *) + (* seteq None 4 1 3; *) + (* ] ] ] *) + (* then Printf.printf "Passed 1\n" *) + (* else Printf.printf "Failed 1\n"); *) + (* (if schedule_oracle [] *) + (* [ sett (Some (plit false 1)) 2 1; *) + (* div (Some (plit true 1)) 1 2 3; *) + (* ] *) + (* [ [ [ div (Some (plit true 1)) 1 2 3; *) + (* sett (Some (plit false 1)) 2 1; *) + (* ] ] ] *) + (* then Printf.printf "Passed 1\n" *) + (* else Printf.printf "Failed 1\n"); *) + (if schedule_oracle [] + [ const (Some (plit true 1)) 1 0; + const (Some (Por (plit true 1, plit false 1))) 1 1; + ] + [ [ [ const None 1 1; + ] ] ] + then Printf.printf "Passed 1\n" + else Printf.printf "Failed 1\n"); + (* (if schedule_oracle [(pred 3, pred 2)] *) + (* [ add None 2 1 4; *) + (* seteq None 1 10 11; *) + (* add (Some (plit true 1)) 1 2 4; *) + (* seteq (Some (plit true 1)) 2 12 13; *) + (* mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; *) + (* goto (Some (Pand (plit true 1, plit true 2))) 10; *) + (* mul (Some (Pand (plit true 1, plit false 2))) 3 3 3; *) + (* goto (Some (Pand (plit true 1, plit false 2))) 10; *) + (* seteq (Some (plit false 1)) 3 12 13; *) + (* mul (Some (Pand (plit false 1, plit true 3))) 3 1 4; *) + (* goto (Some (Pand (plit false 1, plit true 3))) 10; *) + (* mul (Some (Pand (plit false 1, plit false 3))) 3 1 1; *) + (* mul (Some (Pand (plit false 1, plit false 3))) 3 3 3; *) + (* goto (Some (Pand (plit false 1, plit false 3))) 10; *) + (* ] *) + (* [ [ [ seteq None 1 10 11; *) + (* add None 2 1 4; *) + (* seteq (Some (plit false 1)) 3 12 13; *) + (* seteq (Some (plit true 1)) 2 12 13; *) + (* add (Some (plit true 1)) 1 2 4; *) + (* mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; *) + (* mul (Some (Pand (plit true 1, plit false 2))) 3 3 3; *) + (* mul (Some (Pand (plit false 1, plit true 2))) 3 1 4; *) + (* mul (Some (Pand (plit false 1, plit false 2))) 3 1 1; *) + (* mul (Some (Pand (plit false 1, plit false 2))) 3 3 3; *) + (* goto None 10; *) + (* ] ] ] *) + (* then Printf.printf "Passed 110\n" *) + (* else Printf.printf "Failed 102\n"); *) + (* (if schedule_oracle [(pred 3, pred 2)] *) + (* [ add None 2 1 4; *) + (* seteq None 1 10 11; *) + (* add (Some (plit true 1)) 1 2 4; *) + (* seteq (Some (plit true 1)) 2 12 13; *) + (* mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; *) + (* goto (Some (Pand (plit true 1, plit true 2))) 10; *) + (* mul (Some (Pand (plit true 1, plit false 2))) 5 3 3; *) + (* goto (Some (Pand (plit true 1, plit false 2))) 10; *) + (* seteq (Some (plit false 1)) 3 12 13; *) + (* mul (Some (Pand (plit false 1, plit true 3))) 3 1 4; *) + (* goto (Some (Pand (plit false 1, plit true 3))) 10; *) + (* mul (Some (Pand (plit false 1, plit false 3))) 3 1 1; *) + (* mul (Some (Pand (plit false 1, plit false 3))) 5 3 3; *) + (* goto (Some (Pand (plit false 1, plit false 3))) 10; *) + (* ] *) + (* [ [ [ seteq None 1 10 11; *) + (* add None 2 1 4; *) + (* seteq (Some (plit false 1)) 3 12 13; *) + (* seteq (Some (plit true 1)) 2 12 13; *) + (* add (Some (plit true 1)) 1 2 4; *) + (* mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; *) + (* mul (Some (Pand (plit false 1, plit true 2))) 3 1 4; *) + (* mul (Some (Pand (plit false 1, plit false 2))) 3 1 1; *) + (* mul (Some (Pand (plit true 1, plit false 2))) 5 3 3; *) + (* mul (Some (Pand (plit false 1, plit false 2))) 5 3 3; *) + (* goto None 10; *) + (* ] ] ] *) + (* then Printf.printf "Passed 110\n" *) + (* else Printf.printf "Failed 102\n"); *) + (* (if schedule_oracle [(pred 3, pred 2)] *) + (* [ *) + (* seteq None 1 10 11; *) + (* seteq None 3 12 13; *) + (* seteq None 2 12 13; *) + (* add None 2 1 4; *) + (* mul (Some (Pand (plit false 1, plit false 3))) 3 1 1; *) + (* mul (Some (Pand (plit false 1, plit false 3))) 5 3 3; *) + (* goto (Some (Pand (plit false 1, plit false 3))) 10; *) + (* mul (Some (Pand (plit false 1, plit true 3))) 3 1 4; *) + (* goto (Some (Pand (plit false 1, plit true 3))) 10; *) + (* add (Some (plit true 1)) 1 2 4; *) + (* mul (Some (Pand (plit true 1, plit false 2))) 5 3 3; *) + (* goto (Some (Pand (plit true 1, plit false 2))) 10; *) + (* mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; *) + (* goto (Some (Pand (plit true 1, plit true 2))) 10; *) + (* ] *) + (* [ [ [ seteq None 1 10 11; *) + (* seteq None 3 12 13; *) + (* seteq None 2 12 13; *) + (* mul (Some (Pand (plit false 1, plit false 2))) 3 1 1; *) + (* add None 2 1 4; *) + (* add (Some (plit true 1)) 1 2 4; *) + (* mul (Some (Pand (plit false 1, plit true 2))) 3 1 4; *) + (* mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; *) + (* mul (Some (Pand (plit false 1, plit false 2))) 5 3 3; *) + (* mul (Some (Pand (plit true 1, plit false 2))) 5 3 3; *) + (* goto None 10; *) + (* ] ] ] *) + (* then Printf.printf "Passed 110\n" *) + (* else Printf.printf "Failed 102\n") *) + diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index 3cf2401..57e067d 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -221,23 +221,6 @@ Definition is_initial_pred_and_notin (f: forest) (p: positive) (p_next: pred_op) | _ => false end. -Definition predicated_not_in {A} (p: Gible.predicate) (l: predicated A): bool := - NE.fold_right (fun (a: pred_op * A) (b: bool) => - b && negb (predin peq p (fst a)) - ) true l. - -Definition predicated_not_in_pred_expr (p: Gible.predicate) (tree: RTree.t pred_expr) := - PTree.fold (fun b _ a => - b && predicated_not_in p a - ) tree true. - -Definition predicated_not_in_pred_eexpr (p: Gible.predicate) (l: pred_eexpr) := - predicated_not_in p l. - -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. @@ -422,21 +405,21 @@ Definition check_evaluability1 a b := forallb (fun be => existsb (fun ae => resource_eq (fst ae) (fst be) - && HN.beq_pred_expr (snd ae) (snd be) + && HN.beq_pred_expr nil (snd ae) (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 + forallb (fun be => existsb (fun ae => HN.beq_pred_expr nil ae be && 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 | Some (bb', reg_expr, m_expr), Some (bbt', reg_expr_t, m_expr_t) => - check bb' bbt' && empty_trees bb bbt + check nil bb' bbt' && empty_trees bb bbt && check_evaluability1 reg_expr reg_expr_t && check_evaluability2 m_expr m_expr_t | _, _ => false diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index ca2d8a2..afa554c 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -813,6 +813,7 @@ have been evaluable. inversion_clear XX as [v HSEM]. exists v. eapply HN.beq_pred_expr_correct_top; eauto using check_mutexcl_correct. + auto. Qed. Lemma check_evaluability2_evaluable : @@ -836,6 +837,7 @@ have been evaluable. inversion_clear HIN' as [v HSEM]. exists v. eapply HN.beq_pred_expr_correct_top; eauto using check_mutexcl_correct. + auto. Qed. Lemma evaluable_same_preds : diff --git a/src/hls/GiblePargenproofCommon.v b/src/hls/GiblePargenproofCommon.v index 345836f..9254a3b 100644 --- a/src/hls/GiblePargenproofCommon.v +++ b/src/hls/GiblePargenproofCommon.v @@ -210,31 +210,6 @@ Proof. econstructor. split. constructor. right. eauto. auto. Qed. -Definition predicated_not_inP {A} (p: Gible.predicate) (l: predicated A) := - forall op e, NE.In (op, e) l -> ~ PredIn p op. - -Lemma predicated_not_inP_cons : - forall A p (a: (pred_op * A)) l, - predicated_not_inP p (NE.cons a l) -> - predicated_not_inP p l. -Proof. - unfold predicated_not_inP; intros. eapply H. econstructor. right; eauto. -Qed. - -Lemma predicated_not_inP_equiv : - forall A (a: predicated A) p, - predicated_not_in p a = true -> predicated_not_inP p a. -Proof. - induction a. - - intros. cbn in *. unfold predicated_not_inP; intros. - unfold not; intros. inv H0. cbn in *. - destruct (predin peq p op) eqn:?; try discriminate. eapply predin_PredIn in H1. - rewrite H1 in Heqb. discriminate. - - intros. cbn in H. eapply andb_prop in H. inv H. eapply IHa in H0. - unfold predicated_not_inP in *; intros. inv H. inv H3; cbn in *; eauto. - unfold not; intros. eapply predin_PredIn in H. now rewrite H in H1. -Qed. - Lemma truthy_dec: forall ps a, truthy ps a \/ falsy ps a. Proof. diff --git a/src/hls/GiblePargenproofEquiv.v b/src/hls/GiblePargenproofEquiv.v index ee1c11c..df14e31 100644 --- a/src/hls/GiblePargenproofEquiv.v +++ b/src/hls/GiblePargenproofEquiv.v @@ -1177,62 +1177,65 @@ Module HashExprNorm(HS: Hashable). 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 := + 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 p p' - | None => equiv_check p ⟂ + | Some p' => equiv_check_eq_list eq_list p p' + | None => equiv_check_eq_list eq_list p ⟂ end. - Definition tree_equiv_check_None_el (np2: PTree.t pred_op) (n: positive) (p: pred_op): bool := + 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 p ⟂ + | None => equiv_check_eq_list eq_list p ⟂ end. - Definition beq_pred_expr (pe1 pe2: predicated HS.t) : bool := + 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 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. + forall_ptree (tree_equiv_check_el eq_list np2) np1 + && forall_ptree (tree_equiv_check_None_el eq_list np1) np2. Lemma beq_pred_expr_correct: - forall np1 np2 e p p', - forall_ptree (tree_equiv_check_el np2) np1 = true -> + forall eq_list np1 np2 e p p' c, + sat_predicate (eq_list_to_pred_op eq_list) c = true -> + forall_ptree (tree_equiv_check_el eq_list np2) np1 = true -> np1 ! e = Some p -> np2 ! e = Some p' -> - p == p'. + sat_predicate p c = sat_predicate p' c. Proof. - intros. + intros * HEQ **. eapply forall_ptree_true in H; try eassumption. unfold tree_equiv_check_el in H. - rewrite H1 in H. now apply equiv_check_correct. + rewrite H1 in H. now eapply equiv_check_eq_list_correct; eauto. Qed. Lemma beq_pred_expr_correct2: - forall np1 np2 e p, - forall_ptree (tree_equiv_check_el np2) np1 = true -> + forall eq_list np1 np2 e p c, + sat_predicate (eq_list_to_pred_op eq_list) c = true -> + forall_ptree (tree_equiv_check_el eq_list np2) np1 = true -> np1 ! e = Some p -> np2 ! e = None -> - p == ⟂. + sat_predicate p c = sat_predicate ⟂ c. Proof. - intros. + intros * HEQ **. eapply forall_ptree_true in H; try eassumption. unfold tree_equiv_check_el in H. - rewrite H1 in H. now apply equiv_check_correct. + rewrite H1 in H. now eapply equiv_check_eq_list_correct; eauto. Qed. Lemma beq_pred_expr_correct3: - forall np1 np2 e p, - forall_ptree (tree_equiv_check_None_el np1) np2 = true -> + forall eq_list np1 np2 e p c, + sat_predicate (eq_list_to_pred_op eq_list) c = true -> + forall_ptree (tree_equiv_check_None_el eq_list np1) np2 = true -> np1 ! e = None -> np2 ! e = Some p -> - p == ⟂. + sat_predicate p c = sat_predicate ⟂ c. Proof. - intros. + intros * HEQ **. 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. + rewrite H0 in H. now eapply equiv_check_eq_list_correct; eauto. Qed. Section PRED_PROOFS. @@ -1434,14 +1437,15 @@ Module HashExprNorm(HS: Hashable). Qed. Lemma beq_pred_expr_correct_top: - forall p1 p2 v + forall eq_list p1 p2 v (MUTEXCL1: predicated_mutexcl p1) (MUTEXCL2: predicated_mutexcl p2), - beq_pred_expr p1 p2 = true -> + eval_predf ps (eq_list_to_pred_op eq_list) = true -> + beq_pred_expr eq_list p1 p2 = true -> sem_pred_expr f a_sem ctx p1 v -> sem_pred_expr f a_sem ctx p2 v. Proof. - unfold beq_pred_expr; intros. + unfold beq_pred_expr; intros * MUTEXCL1 MUTEXCL2 HEQ **. destruct_match; subst; auto. repeat (destruct_match; []). symmetry in H. apply andb_true_eq in H. inv H. @@ -1453,24 +1457,26 @@ Module HashExprNorm(HS: Hashable). 3: { eauto. } 2: { unfold H.wf_hash_table; intros. now rewrite PTree.gempty in H3. } inv H0. destruct (t0 ! e) eqn:?. - - assert (pr == p) by eauto using beq_pred_expr_correct. + - (* assert (pr == p) by admit. (* eauto using beq_pred_expr_correct. *) *) assert (sem_pexpr ctx (from_pred_op f p) true). - { eapply sem_pexpr_eval; eauto. eapply sem_pexpr_eval_inv in H3; eauto. } - econstructor. apply H7. eauto. eauto. + { eapply sem_pexpr_eval; eauto. eapply sem_pexpr_eval_inv in H3; eauto. + unfold eval_predf in *. erewrite <- beq_pred_expr_correct; eauto. } + econstructor. apply H0. eauto. eauto. eapply norm_expression_in; eauto. - - assert (pr == ⟂) by eauto using beq_pred_expr_correct2. + - assert (eval_predf ps pr = eval_predf ps ⟂) by (unfold eval_predf; eauto using beq_pred_expr_correct2). eapply sem_pexpr_eval_inv in H3; eauto. now rewrite H0 in H3. Qed. Lemma beq_pred_expr_correct_top2: - forall p1 p2 v + forall eq_list p1 p2 v (MUTEXCL1: predicated_mutexcl p1) (MUTEXCL2: predicated_mutexcl p2), - beq_pred_expr p1 p2 = true -> + (eval_predf ps (eq_list_to_pred_op eq_list) = true) -> + beq_pred_expr eq_list p1 p2 = true -> sem_pred_expr f a_sem ctx p2 v -> sem_pred_expr f a_sem ctx p1 v. Proof. - unfold beq_pred_expr; intros. + unfold beq_pred_expr; intros * MUTEXCL1 MUTEXCL2 HEQ **. destruct_match; subst; auto. repeat (destruct_match; []). symmetry in H. apply andb_true_eq in H. inv H. @@ -1484,7 +1490,7 @@ Module HashExprNorm(HS: Hashable). 3: { eauto. } 2: { auto. } inv H0. destruct (t ! e) eqn:?. - - assert (p == pr) by eauto using beq_pred_expr_correct. + - assert (eval_predf ps p = eval_predf ps pr) by (unfold eval_predf; eauto using beq_pred_expr_correct). assert (sem_pexpr ctx (from_pred_op f p) true). { eapply sem_pexpr_eval; eauto. eapply sem_pexpr_eval_inv in H3; eauto. } econstructor. apply H7. eauto. eauto. @@ -1493,7 +1499,7 @@ Module HashExprNorm(HS: Hashable). now rewrite PTree.gempty in YH. eauto. simplify. exploit norm_expression_in. 2: { eauto. } auto. eauto. intros. crush. - - assert (pr == ⟂) by eauto using beq_pred_expr_correct3. + - assert (eval_predf ps pr = eval_predf ps ⟂) by (unfold eval_predf; eauto using beq_pred_expr_correct3). eapply sem_pexpr_eval_inv in H3; eauto. now rewrite H0 in H3. Qed. @@ -1614,14 +1620,35 @@ Proof. eapply forall_ptree_true in H; eauto using check_mutexcl_correct. Qed. -Definition check f1 f2 := - RTree.beq HN.beq_pred_expr f1.(forest_regs) f2.(forest_regs) +Definition remove_all {A} := + fold_left (fun (a: PTree.t A) b => PTree.remove b a). + +Definition predicated_not_in {A} (p: Gible.predicate) (l: predicated A): bool := + NE.fold_right (fun (a: pred_op * A) (b: bool) => + b && negb (predin peq p (fst a)) + ) true l. + +Definition predicated_not_in_pred_expr (p: Gible.predicate) (tree: RTree.t pred_expr) := + PTree.fold (fun b _ a => + b && predicated_not_in p a + ) tree true. + +Definition predicated_not_in_pred_eexpr (p: Gible.predicate) (l: pred_eexpr) := + predicated_not_in p l. + +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 check (eq_list: list (positive * positive)) f1 f2 := + RTree.beq (HN.beq_pred_expr eq_list) 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) + && EHN.beq_pred_expr eq_list f1.(forest_exit) 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). + && 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). Lemma sem_pexpr_forward_eval1 : forall A ctx f_p ps, @@ -2086,9 +2113,9 @@ Proof. Qed. Lemma tree_beq_pred_expr : - forall a b x, - RTree.beq HN.beq_pred_expr (forest_regs a) (forest_regs b) = true -> - HN.beq_pred_expr a #r x b #r x = true. + forall eq_list a b x, + RTree.beq (HN.beq_pred_expr eq_list) (forest_regs a) (forest_regs b) = true -> + HN.beq_pred_expr eq_list a #r x b #r x = true. Proof. intros. unfold "#r" in *. apply PTree.beq_correct with (x := (R_indexed.index x)) in H. @@ -2098,14 +2125,227 @@ Proof. unfold HN.beq_pred_expr. destruct_match; auto. Qed. +Definition predicated_not_inP {A} (p: Gible.predicate) (l: predicated A) := + forall op e, NE.In (op, e) l -> ~ PredIn p op. + +Lemma predicated_not_inP_cons : + forall A p (a: (pred_op * A)) l, + predicated_not_inP p (NE.cons a l) -> + predicated_not_inP p l. +Proof. + unfold predicated_not_inP; intros. eapply H. econstructor. right; eauto. +Qed. + +Lemma predicated_not_inP_equiv : + forall A (a: predicated A) p, + predicated_not_in p a = true -> predicated_not_inP p a. +Proof. + induction a. + - intros. cbn in *. unfold predicated_not_inP; intros. + unfold not; intros. inv H0. cbn in *. + destruct (predin peq p op) eqn:?; try discriminate. eapply predin_PredIn in H1. + rewrite H1 in Heqb. discriminate. + - intros. cbn in H. eapply andb_prop in H. inv H. eapply IHa in H0. + unfold predicated_not_inP in *; intros. inv H. inv H3; cbn in *; eauto. + unfold not; intros. eapply predin_PredIn in H. now rewrite H in H1. +Qed. + +Lemma pred_fold_true' : + forall A l pred y, + fold_left (fun a (p : positive * predicated A) => a && predicated_not_in pred (snd p)) l y = true -> + y = true. +Proof. + induction l; crush. + exploit IHl; try eassumption; intros. + eapply andb_prop in H0; tauto. +Qed. + +Lemma pred_fold_true : + forall A pred l p y, + fold_left (fun (a : bool) (p : positive * predicated A) => a && predicated_not_in pred (snd p)) l y = true -> + y = true -> + list_norepet (map fst l) -> + In p l -> + predicated_not_in pred (snd p) = true. +Proof. + induction l; crush. + inv H1. inv H2. + - cbn in *. now eapply pred_fold_true' in H. + - cbn in *; eapply IHl; try eassumption. + eapply pred_fold_true'; eauto. +Qed. + +Lemma pred_not_in_forestP : + forall pred f, + predicated_not_in_forest pred f = true -> + forall x, predicated_not_inP pred (f #r x). +Proof. + unfold predicated_not_in_forest, predicated_not_in_pred_expr; intros. + destruct (RTree.get x (forest_regs f)) eqn:?. + - eapply andb_prop in H. inv H. rewrite PTree.fold_spec in H0. + unfold RTree.get in Heqo. + exploit pred_fold_true. eauto. auto. apply PTree.elements_keys_norepet. + apply PTree.elements_correct; eauto. + intros. eapply predicated_not_inP_equiv. unfold "#r". + unfold RTree.get. rewrite Heqo. auto. + - unfold "#r". rewrite Heqo. unfold predicated_not_inP; intros. + inv H0. inversion 1. +Qed. + +Lemma pred_not_in_forest_exitP : + forall pred f, + predicated_not_in_forest pred f = true -> + predicated_not_inP pred (forest_exit f). +Proof. + intros. + eapply predicated_not_inP_equiv. unfold predicated_not_in_forest in H. + eapply andb_prop in H; tauto. +Qed. + +Lemma sem_pexpr_not_in : + forall G (ctx: @ctx G) p0 ps p e b, + ~ PredIn p p0 -> + sem_pexpr ctx (from_pred_op ps p0) b -> + sem_pexpr ctx (from_pred_op (PTree.set p e ps) p0) b. +Proof. + induction p0; auto; intros. + - cbn. destruct p. unfold get_forest_p'. + assert (p0 <> p) by + (unfold not; intros; apply H; subst; constructor). + rewrite PTree.gso; auto. + - cbn in *. + assert (X: ~ PredIn p p0_1 /\ ~ PredIn p p0_2) by + (split; unfold not; intros; apply H; constructor; tauto). + inversion_clear X as [X1 X2]. + inv H0. inv H4. + specialize (IHp0_1 _ p e _ X1 H0). constructor. tauto. + specialize (IHp0_2 _ p e _ X2 H0). constructor. tauto. + constructor; auto. + - cbn in *. + assert (X: ~ PredIn p p0_1 /\ ~ PredIn p p0_2) by + (split; unfold not; intros; apply H; constructor; tauto). + inversion_clear X as [X1 X2]. + inv H0. inv H4. + specialize (IHp0_1 _ p e _ X1 H0). constructor. tauto. + specialize (IHp0_2 _ p e _ X2 H0). constructor. tauto. + constructor; auto. +Qed. + +Lemma sem_pexpr_not_in2 : + forall G (ctx: @ctx G) p0 ps p b, + ~ PredIn p p0 -> + sem_pexpr ctx (from_pred_op ps p0) b -> + sem_pexpr ctx (from_pred_op (PTree.remove p ps) p0) b. +Proof. + induction p0; auto; intros. + - cbn. destruct p. unfold get_forest_p'. + assert (p0 <> p) by + (unfold not; intros; apply H; subst; constructor). + rewrite PTree.gro; auto. + - cbn in *. + assert (X: ~ PredIn p p0_1 /\ ~ PredIn p p0_2) by + (split; unfold not; intros; apply H; constructor; tauto). + inversion_clear X as [X1 X2]. + inv H0. inv H4. + specialize (IHp0_1 _ p _ X1 H0). constructor. tauto. + specialize (IHp0_2 _ p _ X2 H0). constructor. tauto. + constructor; auto. + - cbn in *. + assert (X: ~ PredIn p p0_1 /\ ~ PredIn p p0_2) by + (split; unfold not; intros; apply H; constructor; tauto). + inversion_clear X as [X1 X2]. + inv H0. inv H4. + specialize (IHp0_1 _ p _ X1 H0). constructor. tauto. + specialize (IHp0_2 _ p _ X2 H0). constructor. tauto. + constructor; auto. +Qed. + +Lemma sem_pred_not_in : + forall A B G (ctx: @ctx G) (s: @Abstr.ctx G -> A -> B -> Prop) l v p e ps, + sem_pred_expr ps s ctx l v -> + predicated_not_inP p l -> + sem_pred_expr (PTree.set p e ps) s ctx l v. +Proof. + induction l. + - intros. unfold predicated_not_inP in H0. + destruct a. constructor. apply sem_pexpr_not_in. + eapply H0. econstructor. inv H. auto. inv H. auto. + - intros. inv H. constructor. unfold predicated_not_inP in H0. + eapply sem_pexpr_not_in. eapply H0. constructor. left. eauto. + auto. auto. + apply sem_pred_expr_cons_false. apply sem_pexpr_not_in. eapply H0. + constructor. tauto. auto. auto. + eapply IHl. eauto. eapply predicated_not_inP_cons; eauto. +Qed. + +Lemma sem_pred_not_in2 : + forall A B G (ctx: @ctx G) (s: @Abstr.ctx G -> A -> B -> Prop) l v p ps, + sem_pred_expr ps s ctx l v -> + predicated_not_inP p l -> + sem_pred_expr (PTree.remove p ps) s ctx l v. +Proof. + induction l. + - intros. unfold predicated_not_inP in H0. + destruct a. constructor. apply sem_pexpr_not_in2. + eapply H0. econstructor. inv H. auto. inv H. auto. + - intros. inv H. constructor. unfold predicated_not_inP in H0. + eapply sem_pexpr_not_in2. eapply H0. constructor. left. eauto. + auto. auto. + apply sem_pred_expr_cons_false. apply sem_pexpr_not_in2. eapply H0. + constructor. tauto. auto. auto. + eapply IHl. eauto. eapply predicated_not_inP_cons; eauto. +Qed. + +Lemma remove_all_sem_pred_expr : + forall A B G (ctx: @Abstr.ctx G) (s: @Abstr.ctx G -> A -> B -> Prop) l a y v, + sem_pred_expr a s ctx y v -> + Forall (fun x => predicated_not_inP x y) l -> + sem_pred_expr (remove_all l a) s ctx y v. +Proof. + induction l; cbn; auto; intros. + inv H0. eapply IHl; eauto. + apply sem_pred_not_in2; auto. +Qed. + +Lemma eval_predf_eq_list : + forall G (ictx: @ctx G) a pr' eq_list t, + (forall x : positive, sem_pexpr ictx a #p x pr' !! x) -> + forallb (fun x : positive * positive => beq_pred_pexpr a #p (fst x) a #p (snd x)) eq_list = true -> + eval_predf pr' t = true -> + eval_predf pr' + (fold_left + (fun (a0 : Predicate.pred_op) (b0 : Predicate.predicate * Predicate.predicate) => + a0 ∧ ((Plit (true, fst b0) ∨ Plit (false, snd b0)) ∧ (Plit (true, snd b0) ∨ Plit (false, fst b0)))) eq_list t) = + true. +Proof. + induction eq_list; auto; intros. + eapply IHeq_list; [auto| |]. + cbn in H0. apply andb_prop in H0; tauto. + rewrite eval_predf_Pand. rewrite H1; cbn -[eval_predf]. + cbn in H0. apply andb_prop in H0. inv H0. + eapply sem_pexpr_beq_correct' with (ctx := ictx) in H2. + assert (eval_predf pr' (Plit (true, fst a0)) = eval_predf pr' (Plit (true, snd a0))). + remember (eval_predf pr' (Plit (true, fst a0))). symmetry in Heqb. + eapply sem_pexpr_eval in Heqb; eauto. + apply sem_pexprF_correct2 in Heqb. cbn in Heqb. unfold "#p" in *. rewrite H2 in Heqb. + replace (get_forest_p' (snd a0) (forest_preds a)) + with (from_pred_op (forest_preds a) (Plit (true, snd a0))) in Heqb by auto. + apply sem_pexprF_correct in Heqb. eapply sem_pexpr_eval_inv in Heqb. eauto. + eauto. + destruct (eval_predf pr' (Plit (true, fst a0))) eqn:?; + destruct (eval_predf pr' (Plit (true, snd a0))) eqn:?; crush. + cbn in *. setoid_rewrite Heqb. setoid_rewrite Heqb0; auto. + cbn in *. setoid_rewrite Heqb. setoid_rewrite Heqb0; auto. +Qed. + Section CORRECT. Context {FUN TFUN: Type}. Context (ictx: @ctx FUN) (octx: @ctx TFUN) (HSIM: similar ictx octx). Lemma abstr_check_correct : - forall i' a b cf, - check a b = true -> + forall eq_list i' a b cf, + check eq_list a b = true -> sem ictx a (i', cf) -> exists ti', sem octx b (ti', cf) /\ match_states i' ti'. Proof. @@ -2113,28 +2353,37 @@ Proof. assert (EVALUABLE: (exists ps, forall x, sem_pexpr ictx (get_forest_p' x (forest_preds a)) ps !! x)). { inv H0. inv H4. eauto. } unfold check in H. simplify. - inv H0. inv H10. inv H11. + inv H0. inv H11. inv H12. eexists; split; constructor; auto. - constructor. intros. eapply sem_pred_exec_beq_correct; eauto. + (* eapply remove_all_sem_pred_expr; eauto. *) + (* 2: { eapply Forall_forall; intros. eapply forallb_forall in H3; eauto. eapply pred_not_in_forestP; eauto. } *) eapply sem_pred_expr_corr; eauto. now apply sem_value_corr. eapply HN.beq_pred_expr_correct_top; eauto. { unfold "#r"; destruct_match; eauto using check_mutexcl_tree_correct, predicated_singleton. } { unfold "#r"; destruct_match; eauto using check_mutexcl_tree_correct, predicated_singleton. } - eapply tree_beq_pred_expr; eauto. + 2: { eapply tree_beq_pred_expr; eauto. } + unfold eq_list_to_pred_op. eapply eval_predf_eq_list; eauto. - (* This is where three-valued logic would be needed. *) constructor. intros. apply sem_pexpr_beq_correct with (p1 := a #p x0). apply tree_beq_pred_pexpr; auto. apply sem_pexpr_corr with (ictx:=ictx); auto. - eapply sem_pred_exec_beq_correct; eauto. + (* eapply remove_all_sem_pred_expr; eauto. *) + (* 2: { eapply Forall_forall; intros. eapply forallb_forall in H3; eauto. eapply pred_not_in_forestP; eauto. } *) eapply sem_pred_expr_corr; eauto. now apply sem_mem_corr. eapply HN.beq_pred_expr_correct_top; eauto. { unfold "#r"; destruct_match; eauto using check_mutexcl_tree_correct, predicated_singleton. } { unfold "#r"; destruct_match; eauto using check_mutexcl_tree_correct, predicated_singleton. } - eapply tree_beq_pred_expr; eauto. + 2: { eapply tree_beq_pred_expr; eauto. } + unfold eq_list_to_pred_op. eapply eval_predf_eq_list; eauto. - eapply sem_pred_exec_beq_correct; eauto. + (* eapply remove_all_sem_pred_expr; eauto. *) + (* 2: { eapply Forall_forall; intros. eapply forallb_forall in H3; eauto. eapply pred_not_in_forest_exitP; eauto. } *) eapply sem_pred_expr_corr; eauto. now apply sem_exit_corr. eapply EHN.beq_pred_expr_correct_top; eauto using check_mutexcl_correct. + unfold eq_list_to_pred_op. eapply eval_predf_eq_list; eauto. Qed. (*| diff --git a/src/hls/GiblePargenproofForward.v b/src/hls/GiblePargenproofForward.v index 946a243..48fe922 100644 --- a/src/hls/GiblePargenproofForward.v +++ b/src/hls/GiblePargenproofForward.v @@ -273,105 +273,6 @@ all be evaluable. + auto. Qed. - Lemma sem_pexpr_not_in : - forall G (ctx: @ctx G) p0 ps p e b, - ~ PredIn p p0 -> - sem_pexpr ctx (from_pred_op ps p0) b -> - sem_pexpr ctx (from_pred_op (PTree.set p e ps) p0) b. - Proof. - induction p0; auto; intros. - - cbn. destruct p. unfold get_forest_p'. - assert (p0 <> p) by - (unfold not; intros; apply H; subst; constructor). - rewrite PTree.gso; auto. - - cbn in *. - assert (X: ~ PredIn p p0_1 /\ ~ PredIn p p0_2) by - (split; unfold not; intros; apply H; constructor; tauto). - inversion_clear X as [X1 X2]. - inv H0. inv H4. - specialize (IHp0_1 _ p e _ X1 H0). constructor. tauto. - specialize (IHp0_2 _ p e _ X2 H0). constructor. tauto. - constructor; auto. - - cbn in *. - assert (X: ~ PredIn p p0_1 /\ ~ PredIn p p0_2) by - (split; unfold not; intros; apply H; constructor; tauto). - inversion_clear X as [X1 X2]. - inv H0. inv H4. - specialize (IHp0_1 _ p e _ X1 H0). constructor. tauto. - specialize (IHp0_2 _ p e _ X2 H0). constructor. tauto. - constructor; auto. - Qed. - - Lemma sem_pred_not_in : - forall A B G (ctx: @ctx G) (s: @Abstr.ctx G -> A -> B -> Prop) l v p e ps, - sem_pred_expr ps s ctx l v -> - predicated_not_inP p l -> - sem_pred_expr (PTree.set p e ps) s ctx l v. - Proof. - induction l. - - intros. unfold predicated_not_inP in H0. - destruct a. constructor. apply sem_pexpr_not_in. - eapply H0. econstructor. inv H. auto. inv H. auto. - - intros. inv H. constructor. unfold predicated_not_inP in H0. - eapply sem_pexpr_not_in. eapply H0. constructor. left. eauto. - auto. auto. - apply sem_pred_expr_cons_false. apply sem_pexpr_not_in. eapply H0. - constructor. tauto. auto. auto. - eapply IHl. eauto. eapply predicated_not_inP_cons; eauto. - Qed. - - Lemma pred_fold_true' : - forall A l pred y, - fold_left (fun a (p : positive * predicated A) => a && predicated_not_in pred (snd p)) l y = true -> - y = true. - Proof. - induction l; crush. - exploit IHl; try eassumption; intros. - eapply andb_prop in H0; tauto. - Qed. - - Lemma pred_fold_true : - forall A pred l p y, - fold_left (fun (a : bool) (p : positive * predicated A) => a && predicated_not_in pred (snd p)) l y = true -> - y = true -> - list_norepet (map fst l) -> - In p l -> - predicated_not_in pred (snd p) = true. - Proof. - induction l; crush. - inv H1. inv H2. - - cbn in *. now eapply pred_fold_true' in H. - - cbn in *; eapply IHl; try eassumption. - eapply pred_fold_true'; eauto. - Qed. - - Lemma pred_not_in_forestP : - forall pred f, - predicated_not_in_forest pred f = true -> - forall x, predicated_not_inP pred (f #r x). - Proof. - unfold predicated_not_in_forest, predicated_not_in_pred_expr; intros. - destruct (RTree.get x (forest_regs f)) eqn:?. - - eapply andb_prop in H. inv H. rewrite PTree.fold_spec in H0. - unfold RTree.get in Heqo. - exploit pred_fold_true. eauto. auto. apply PTree.elements_keys_norepet. - apply PTree.elements_correct; eauto. - intros. eapply predicated_not_inP_equiv. unfold "#r". - unfold RTree.get. rewrite Heqo. auto. - - unfold "#r". rewrite Heqo. unfold predicated_not_inP; intros. - inv H0. inversion 1. - Qed. - - Lemma pred_not_in_forest_exitP : - forall pred f, - predicated_not_in_forest pred f = true -> - predicated_not_inP pred (forest_exit f). - Proof. - intros. - eapply predicated_not_inP_equiv. unfold predicated_not_in_forest in H. - eapply andb_prop in H; tauto. - Qed. - Lemma sem_update_Isetpred: forall A (ctx: @ctx A) f pr p0 c args b rs m, predicated_mutexcl (seq_app (pred_ret (PEsetpred c)) (merge (list_translation args f))) -> diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v index 86e992a..d4bc80a 100644 --- a/src/hls/Predicate.v +++ b/src/hls/Predicate.v @@ -740,6 +740,17 @@ Proof. intros. tauto. Qed. +Definition eq_list_to_pred_op (eq_list: list (positive * positive)): pred_op := + fold_left (fun a b => a ∧ ((Plit (true, fst b) ∨ Plit (false, snd b)) + ∧ (Plit (true, snd b) ∨ Plit (false, fst b)))) + eq_list T. + +Definition equiv_check_eq_list eq_list p1 p2 := + match sat_pred_simple (simplify (¬ (eq_list_to_pred_op eq_list) ∨ (p1 ∧ ¬ p2 ∨ p2 ∧ ¬ p1))) with + | None => true + | _ => false + end. + Definition equiv_check p1 p2 := match sat_pred_simple (simplify (p1 ∧ ¬ p2 ∨ p2 ∧ ¬ p1)) with | None => true @@ -759,6 +770,28 @@ Proof. rewrite <- simplify_correct. eauto. Qed. +Lemma equiv_check_eq_list_correct : + forall eq_list p1 p2, + equiv_check_eq_list eq_list p1 p2 = true -> + forall c, sat_predicate (eq_list_to_pred_op eq_list) c = true -> + sat_predicate p1 c = sat_predicate p2 c. +Proof. + unfold equiv_check_eq_list. unfold sat_pred_simple. intros. + destruct_match; try discriminate; []. + destruct_match. destruct_match. discriminate. + assert (negb (sat_predicate (eq_list_to_pred_op eq_list) c) = false) + by (rewrite H0; auto). + clear Heqs. + specialize (e c). + rewrite simplify_correct in e. rewrite sat_predicate_or in e. rewrite <- negate_correct in H1. + rewrite H1 in e. rewrite orb_false_l in e. + destruct (sat_predicate p1 c) eqn:X; + destruct (sat_predicate p2 c) eqn:X2; + crush. + rewrite negate_correct in *. rewrite X in *. rewrite X2 in *. auto. + rewrite negate_correct in *. rewrite X in *. rewrite X2 in *. auto. +Qed. + Opaque simplify. Opaque simplify'. |