From b1ca2f1a6159a313e259a697826380962d7cfa48 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 24 Oct 2021 19:59:31 +0100 Subject: Continue on semantics preservation proof --- src/hls/Abstr.v | 376 +++++++++++++++++++++++++++----------------------------- 1 file changed, 178 insertions(+), 198 deletions(-) (limited to 'src/hls/Abstr.v') diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index 626269f..ec8fd36 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -16,12 +16,6 @@ * along with this program. If not, see . *) -Require Import Coq.Classes.RelationClasses. -Require Import Coq.Classes.DecidableClass. -Require Import Coq.Setoids.Setoid. -Require Import Coq.Classes.SetoidClass. -Require Import Coq.Classes.SetoidDec. - Require Import compcert.backend.Registers. Require Import compcert.common.AST. Require Import compcert.common.Globalenvs. @@ -218,9 +212,6 @@ Then, to make recursion over expressions easier, expression_list is also defined that enables mutual recursive definitions over the datatypes. |*) -Definition unsat p := forall a, sat_predicate p a = false. -Definition sat p := exists a, sat_predicate p a = true. - Inductive expression : Type := | Ebase : resource -> expression | Eop : Op.operation -> expression_list -> expression @@ -420,6 +411,7 @@ Inductive sem_pred_expr {B: Type} (sem: ctx -> expression -> B -> Prop): | sem_pred_expr_single : forall ctx e pr v, eval_predf (ctx_ps ctx) pr = true -> + sem ctx e v -> sem_pred_expr sem ctx (NE.singleton (pr, e)) v . @@ -577,11 +569,11 @@ Fixpoint norm_expression (max: predicate) (pe: pred_expr) (h: hash_tree) end end. -Definition mk_pred_stmnt' pr_op e p_e := (¬ p_e ∨ Pvar (true, e)) ∧ pr_op. +Definition mk_pred_stmnt' e p_e := ¬ p_e ∨ Plit (true, e). -Definition mk_pred_stmnt t := PTree.fold mk_pred_stmnt' t T. +Definition mk_pred_stmnt t := PTree.fold (fun x a b => mk_pred_stmnt' a b ∧ x) t T. -Definition mk_pred_stmnt_l (t: list (predicate * pred_op)) := fold_left (fun x => uncurry (mk_pred_stmnt' x)) t T. +Definition mk_pred_stmnt_l (t: list (predicate * pred_op)) := fold_left (fun x a => uncurry mk_pred_stmnt' a ∧ x) t T. Definition encode_expression max pe h := let (tree, h) := norm_expression max pe h in @@ -601,7 +593,7 @@ Definition encode_expression max pe h := Fixpoint max_predicate (p: pred_op) : positive := match p with - | Pvar (b, p) => p + | Plit (b, p) => p | Ptrue => 1 | Pfalse => 1 | Pand a b => Pos.max (max_predicate a) (max_predicate b) @@ -633,153 +625,7 @@ Inductive similar {A B} : @ctx A -> @ctx B -> Prop := ge_preserved ge tge -> similar (mk_ctx rs ps mem sp ge) (mk_ctx rs ps mem sp tge). -Lemma unsat_correct1 : - forall a b c, - unsat (Pand a b) -> - sat_predicate a c = true -> - sat_predicate b c = false. -Proof. - unfold unsat in *. intros. - simplify. specialize (H c). - apply andb_false_iff in H. inv H. rewrite H0 in H1. discriminate. - auto. -Qed. - -Lemma unsat_correct2 : - forall a b c, - unsat (Pand a b) -> - sat_predicate b c = true -> - sat_predicate a c = false. -Proof. - unfold unsat in *. intros. - simplify. specialize (H c). - apply andb_false_iff in H. inv H. auto. rewrite H0 in H1. discriminate. -Qed. - -Lemma unsat_not a: unsat (a ∧ (¬ a)). -Proof. - unfold unsat; simplify. - rewrite negate_correct. - auto with bool. -Qed. - -Lemma unsat_commut a b: unsat (a ∧ b) -> unsat (b ∧ a). -Proof. unfold unsat; simplify; eauto with bool. Qed. - -Lemma sat_dec a: {sat a} + {unsat a}. -Proof. - unfold sat, unsat. - destruct (sat_pred a). - intros. left. destruct s. - exists (Sat.interp_alist x). auto. - intros. tauto. -Qed. - -Definition sat_equiv p1 p2 := forall c, sat_predicate p1 c = sat_predicate p2 c. - -Lemma equiv_symm : forall a b, sat_equiv a b -> sat_equiv b a. -Proof. crush. Qed. - -Lemma equiv_trans : forall a b c, sat_equiv a b -> sat_equiv b c -> sat_equiv a c. -Proof. crush. Qed. - -Lemma equiv_refl : forall a, sat_equiv a a. -Proof. crush. Qed. - -Instance Equivalence_SAT : Equivalence sat_equiv := - { Equivalence_Reflexive := equiv_refl ; - Equivalence_Symmetric := equiv_symm ; - Equivalence_Transitive := equiv_trans ; - }. - -Instance Setoid_SAT : Setoid pred_op := - { equiv := sat_equiv; }. - -Lemma sat_imp_equiv : - forall a b, - unsat (a ∧ ¬ b ∨ ¬ a ∧ b) -> sat_equiv a b. -Proof. - unfold unsat, sat_equiv. intros. specialize (H c); simplify. - rewrite negate_correct in *. - destruct (sat_predicate b c) eqn:X; - destruct (sat_predicate a c) eqn:X2; - crush. -Qed. - -Lemma sat_predicate_and : - forall a b c, - sat_predicate (a ∧ b) c = sat_predicate a c && sat_predicate b c. -Proof. crush. Qed. - -Lemma sat_predicate_or : - forall a b c, - sat_predicate (a ∨ b) c = sat_predicate a c || sat_predicate b c. -Proof. crush. Qed. - -Lemma sat_equiv2 : - forall a b, - equiv a b -> unsat (a ∧ ¬ b ∨ ¬ a ∧ b). -Proof. - unfold unsat, equiv; simplify. - repeat rewrite negate_correct. - repeat rewrite H. - rewrite andb_negb_r. - rewrite andb_negb_l. auto. -Qed. - -Lemma sat_equiv3 : - forall a b, - unsat (a ∧ ¬ b ∨ b ∧ ¬ a) -> sat_equiv a b. -Proof. - unfold unsat, sat_equiv. intros. specialize (H c); simplify. - rewrite negate_correct in *. - destruct (sat_predicate b c) eqn:X; - destruct (sat_predicate a c) eqn:X2; - crush. -Qed. - -Lemma sat_equiv4 : - forall a b, - a == b -> unsat (a ∧ ¬ b ∨ b ∧ ¬ a). -Proof. - unfold unsat, equiv; simplify. - repeat rewrite negate_correct. - repeat rewrite H. - rewrite andb_negb_r. auto. -Qed. - -Definition equiv_check p1 p2 := - match sat_pred_simple (p1 ∧ ¬ p2 ∨ p2 ∧ ¬ p1) with - | None => true - | _ => false - end. - -Lemma equiv_check_correct : - forall p1 p2, equiv_check p1 p2 = true -> equiv p1 p2. -Proof. - unfold equiv_check. unfold sat_pred_simple. intros. - destruct_match; try discriminate; []. - destruct_match. destruct_match. discriminate. - eapply sat_equiv3; eauto. -Qed. - -Lemma equiv_check_correct2 : - forall p1 p2, equiv p1 p2 -> equiv_check p1 p2 = true. -Proof. - unfold equiv_check, equiv, sat_pred_simple. intros. - destruct_match; auto. destruct_match; try discriminate. destruct_match. - simplify. - apply sat_equiv4 in H. unfold unsat in H. simplify. - clear Heqs. rewrite H in e. discriminate. -Qed. - -Lemma equiv_check_dec : - forall p1 p2, equiv_check p1 p2 = true <-> equiv p1 p2. -Proof. - intros; split; eauto using equiv_check_correct, equiv_check_correct2. -Qed. - -Definition beq_pred_expr (bound: nat) (pe1 pe2: pred_expr) : bool := +Definition beq_pred_expr_once (pe1 pe2: pred_expr) : bool := match pe1, pe2 with (*| PEsingleton None e1, PEsingleton None e2 => beq_expression e1 e2 | PEsingleton (Some p1) e1, PEsingleton (Some p2) e2 => @@ -804,17 +650,76 @@ Definition beq_pred_expr (bound: nat) (pe1 pe2: pred_expr) : bool := equiv_check p1 p2 end. -Definition check := Rtree.beq (beq_pred_expr 10000). +Definition forall_ptree {A:Type} (f:positive->A->bool) (m:Maps.PTree.t A) : bool := + Maps.PTree.fold (fun (res: bool) (i: positive) (x: A) => res && f i x) m true. + +Ltac boolInv := + match goal with + | [ H: _ && _ = true |- _ ] => + destruct (andb_prop _ _ H); clear H; boolInv + | [ H: proj_sumbool _ = true |- _ ] => + generalize (proj_sumbool_true _ H); clear H; + let EQ := fresh in (intro EQ; try subst; boolInv) + | _ => + idtac + end. + +Remark ptree_forall: + forall (A: Type) (f: positive -> A -> bool) (m: Maps.PTree.t A), + Maps.PTree.fold (fun (res: bool) (i: positive) (x: A) => res && f i x) m true = true -> + forall i x, Maps.PTree.get i m = Some x -> f i x = true. +Proof. + intros. + set (f' := fun (res: bool) (i: positive) (x: A) => res && f i x). + set (P := fun (m: Maps.PTree.t A) (res: bool) => + res = true -> Maps.PTree.get i m = Some x -> f i x = true). + assert (P m true). + rewrite <- H. fold f'. apply Maps.PTree_Properties.fold_rec. + unfold P; intros. rewrite <- H1 in H4. auto. + red; intros. rewrite Maps.PTree.gempty in H2. discriminate. + unfold P; intros. unfold f' in H4. boolInv. + rewrite Maps.PTree.gsspec in H5. destruct (peq i k). + subst. inv H5. auto. + apply H3; auto. + red in H1. auto. +Qed. + +Lemma forall_ptree_true: + forall (A: Type) (f: positive -> A -> bool) (m: Maps.PTree.t A), + forall_ptree f m = true -> + forall i x, Maps.PTree.get i m = Some x -> f i x = true. +Proof. + apply ptree_forall. +Qed. + +Definition tree_equiv_check_el (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 ⟂ + end. + +Definition tree_equiv_check_None_el (np2: PTree.t pred_op) (n: positive) (p: pred_op): bool := + match np2 ! n with + | Some p' => true + | None => equiv_check p ⟂ + end. + +Definition beq_pred_expr (pe1 pe2: pred_expr) : bool := + let max := Pos.max (max_pred_expr pe1) (max_pred_expr pe2) in + let (np1, h) := norm_expression max pe1 (PTree.empty _) in + let (np2, h') := norm_expression max pe2 h in + forall_ptree (tree_equiv_check_el np2) np1 + && forall_ptree (tree_equiv_check_None_el np1) np2. + +Definition check := Rtree.beq beq_pred_expr. Compute (check (empty # (Reg 2) <- - ((((Pand (Pvar (true, 4)) (¬ (Pvar (true, 4))))), (Ebase (Reg 9))) ::| - (NE.singleton (((Pvar (true, 2))), (Ebase (Reg 3)))))) - (empty # (Reg 2) <- (NE.singleton (((Por (Pvar (true, 2)) (Pand (Pvar (true, 3)) (¬ (Pvar (true, 3)))))), + ((((Pand (Plit (true, 4)) (¬ (Plit (true, 4))))), (Ebase (Reg 9))) ::| + (NE.singleton (((Plit (true, 2))), (Ebase (Reg 3)))))) + (empty # (Reg 2) <- (NE.singleton (((Por (Plit (true, 2)) (Pand (Plit (true, 3)) (¬ (Plit (true, 3)))))), (Ebase (Reg 3)))))). -Lemma inj_asgn_eg : - forall a b, - (a =? b)%nat = (a =? a)%nat -> a = b. +Lemma inj_asgn_eg : forall a b, (a =? b)%nat = (a =? a)%nat -> a = b. Proof. intros. destruct (Nat.eq_dec a b); subst. auto. apply Nat.eqb_neq in n. @@ -837,11 +742,11 @@ Lemma negb_inj: negb a = negb b -> a = b. Proof. destruct a, b; crush. Qed. -Lemma sat_predicate_Pvar_inj : +Lemma sat_predicate_Plit_inj : forall p1 p2, - equiv (Pvar p1) (Pvar p2) -> p1 = p2. + Plit p1 == Plit p2 -> p1 = p2. Proof. - unfold equiv. simplify. destruct p1, p2. + simplify. destruct p1, p2. destruct b, b0. assert (p = p0). { apply Pos2Nat.inj. eapply inj_asgn. eauto. } solve [subst; auto]. exfalso; eapply inj_asgn_false; eauto. @@ -866,18 +771,33 @@ Definition ind_preds_l t := sat_predicate p1 c = true -> sat_predicate p2 c = false. +(*Lemma pred_equivalence_Some' : + forall ta tb e pe pe', + list_norepet (map fst ta) -> + list_norepet (map fst tb) -> + In (e, pe) ta -> + In (e, pe') tb -> + fold_right (fun p a => mk_pred_stmnt' (fst p) (snd p) ∧ a) T ta == + fold_right (fun p a => mk_pred_stmnt' (fst p) (snd p) ∧ a) T tb -> + pe == pe'. +Proof. + induction ta as [|hd tl Hta]; try solve [crush]. + - intros * NRP1 NRP2 IN1 IN2 FOLD. inv NRP1. inv IN1. + simpl in FOLD. + Lemma pred_equivalence_Some : forall (ta tb: PTree.t pred_op) e pe pe', ta ! e = Some pe -> tb ! e = Some pe' -> - equiv (mk_pred_stmnt ta) (mk_pred_stmnt tb) -> - equiv pe pe'. + mk_pred_stmnt ta == mk_pred_stmnt tb -> + pe == pe'. Proof. - intros * SMEA SMEB EQ. + intros * SMEA SMEB EQ. unfold mk_pred_stmnt in *. + repeat rewrite PTree.fold_spec in EQ. Lemma pred_equivalence_None : forall (ta tb: PTree.t pred_op) e pe, - equiv (mk_pred_stmnt ta) (mk_pred_stmnt tb) -> + (mk_pred_stmnt ta) == (mk_pred_stmnt tb) -> ta ! e = Some pe -> tb ! e = None -> equiv pe ⟂. @@ -892,7 +812,7 @@ Proof. intros * EQ SME. destruct (tb ! e) eqn:HTB. { right. econstructor. split; eauto. eapply pred_equivalence_Some; eauto. } { left. eapply pred_equivalence_None; eauto. } -Qed. +Qed.*) Section CORRECT. @@ -973,30 +893,90 @@ Section CORRECT. #[local] Opaque PTree.set. - Lemma check_correct_sem_value: - forall x x' v v' n, - beq_pred_expr n x x' = true -> - sem_pred_expr sem_value ictx x v -> - sem_pred_expr sem_value octx x' v' -> - v = v'. + Lemma exists_norm_expr : + forall x pe expr m t h h', + NE.In (pe, expr) x -> + norm_expression m x h = (t, h') -> + exists e, t ! e = Some pe /\ h' ! e = Some expr. + Proof. + Admitted. + + Lemma exists_norm_expr2 : + forall e x pe expr m t h h', + t ! e = Some pe -> + h' ! e = Some expr -> + norm_expression m x h = (t, h') -> + NE.In (pe, expr) x. + Proof. + Admitted. + + Lemma exists_norm_expr3 : + forall e x pe expr m t h h', + t ! e = None -> + norm_expression m x h = (t, h') -> + ~ NE.In (pe, expr) x. Proof. - unfold beq_pred_expr. intros. repeat (destruct_match; try discriminate; []); subst. - unfold sat_pred_simple in *. - repeat destruct_match; try discriminate; []; subst. - assert (X: unsat (Por (Pand p (Pnot p0)) (Pand p0 (Pnot p)))) by eauto. - pose proof (sat_equiv2 _ _ X). - destruct x, x'; simplify. - repeat destruct_match; try discriminate; []. inv Heqp0. inv H0. inv H1. - inv Heqp - - apply sat_predicate_Pvar_inj in H2; subst. - - assert (e0 = e1) by (eapply hash_present_eq; eauto); subst. - eauto using sem_value_det. - - admit. - - admit. - - admit. - Admitted. + Admitted. + + Lemma norm_expr_In : + forall A B sem ctx x pe expr v, + @sem_pred_expr A B sem ctx x v -> + NE.In (pe, expr) x -> + eval_predf (ctx_ps ctx) pe = true -> + sem ctx expr v. + Proof. Admitted. + + Section SEM_PRED. + + Context (B: Type). + Context (isem: @ctx fd -> expression -> B -> Prop). + Context (osem: @ctx tfd -> expression -> B -> Prop). + Context (SEMSIM: forall e v v', isem ictx e v -> osem octx e v' -> v = v'). + + Lemma check_correct_sem_value: + forall x x' v v', + beq_pred_expr x x' = true -> + sem_pred_expr isem ictx x v -> + sem_pred_expr osem octx x' v' -> + v = v'. + Proof. + induction x. + - intros. + unfold beq_pred_expr in *. intros. repeat (destruct_match; try discriminate; []); subst. + inv H0. + pose Heqp as X. + eapply exists_norm_expr in X; [|constructor]. + Opaque norm_expression. simplify. Transparent norm_expression. + destruct (t0 ! x) eqn:?. + { eapply forall_ptree_true in H0; eauto. unfold tree_equiv_check_el in *. rewrite Heqo in H0. + apply equiv_check_dec in H0. + eapply exists_norm_expr2 in Heqo. + 3: { eauto. } + 2: { admit. } + eapply norm_expr_In in Heqo; eauto. + inv HSIM; simplify. setoid_rewrite H0 in H3. eassumption. + } + { + } + eapply exists_norm_expr in Heqp. + unfold sat_pred_simple in *. + repeat destruct_match; try discriminate; []; subst. + assert (X: unsat (Por (Pand p (Pnot p0)) (Pand p0 (Pnot p)))) by eauto. + pose proof (sat_equiv2 _ _ X). + destruct x, x'; simplify. + repeat destruct_match; try discriminate; []. inv Heqp0. inv H0. inv H1. + inv Heqp + + apply sat_predicate_Pvar_inj in H2; subst. + + assert (e0 = e1) by (eapply hash_present_eq; eauto); subst. + eauto using sem_value_det. + - admit. + - admit. + - admit. + Admitted. + + End SEM_PRED. Lemma check_correct: forall (fa fb : forest) ctx ctx' i, similar ctx ctx' -> -- cgit