diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-10-27 20:22:23 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-10-27 20:22:23 +0100 |
commit | 41c39c25fbb4620a24cb159059662331689d1905 (patch) | |
tree | 5b2a26bf0d78a734b8ce7df6f3e58eaf0ab87261 /src | |
parent | e51e42283ac9f1f0a80c989ebca7d52eb35f08d3 (diff) | |
download | vericert-41c39c25fbb4620a24cb159059662331689d1905.tar.gz vericert-41c39c25fbb4620a24cb159059662331689d1905.zip |
Add intermediate step in proof of sem pres
Diffstat (limited to 'src')
-rw-r--r-- | src/hls/Abstr.v | 106 | ||||
-rw-r--r-- | src/hls/Predicate.v | 26 |
2 files changed, 108 insertions, 24 deletions
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index fd7c910..607b61e 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -743,6 +743,57 @@ Definition tree_equiv_check_None_el (np2: PTree.t pred_op) (n: positive) (p: pre | None => equiv_check p ⟂ end. +Variant sem_pred_tree {A B: Type} (sem: ctx -> expression -> B -> Prop): + @ctx A -> PTree.t expression -> PTree.t pred_op -> B -> Prop := +| sem_pred_tree_intro : + forall ctx expr e pr v et pt, + eval_predf (ctx_ps ctx) pr = true -> + sem ctx expr v -> + pt ! e = Some pr -> + et ! e = Some expr -> + sem_pred_tree sem ctx et pt v. + +Variant predicated_mutexcl {A: Type} : predicated A -> Prop := +| predicated_mutexcl_intros : forall pe, + (forall x y, NE.In x pe -> NE.In y pe -> x <> y -> fst x ⇒ ¬ fst y) -> + predicated_mutexcl pe. + +Lemma norm_expression_sem_pred : + forall A B sem ctx pe v, + sem_pred_expr sem ctx pe v -> + forall pt et et', + predicated_mutexcl pe -> + norm_expression (max_pred_expr pe) pe et = (pt, et') -> + @sem_pred_tree A B sem ctx et' pt v. +Proof. + induction 1; crush; repeat (destruct_match; []); try destruct_match. + { inv H2. econstructor. 3: { apply PTree.gss. } + 2: { eassumption. } + { unfold eval_predf in *. simplify. rewrite H. auto with bool. } + { admit. } + } + { inv H2. econstructor; eauto. apply PTree.gss. admit. + } + { inv H2. + assert (sem_pred_tree sem0 ctx0 et' t v). + eapply IHsem_pred_expr. + admit. + admit. + admit. + } + { admit. } + { admit. } +Admitted. + +Lemma norm_expression_sem_pred2 : + forall A B sem ctx v pt et et', + @sem_pred_tree A B sem ctx et' pt v -> + forall pe, + predicated_mutexcl pe -> + norm_expression (max_pred_expr pe) pe et = (pt, et') -> + sem_pred_expr sem ctx pe v. +Proof. Admitted. + 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 @@ -936,18 +987,8 @@ Section CORRECT. 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. + exists e pe', t ! e = Some pe' /\ pe ⇒ pe' /\ h' ! e = Some expr. + Proof. Admitted. (* Lemma exists_norm_expr3 : forall e x pe expr m t h h', @@ -964,6 +1005,14 @@ Section CORRECT. h' ! e = Some p. Proof. Admitted. + Lemma norm_expr_implies : + forall x m h t h' e expr p, + norm_expression m x h = (t, h') -> + h' ! e = Some expr -> + t ! e = Some p -> + exists p', NE.In (p', expr) x /\ p' ⇒ p. + Proof. Admitted. + Lemma norm_expr_In : forall A B sem ctx x pe expr v, @sem_pred_expr A B sem ctx x v -> @@ -972,22 +1021,21 @@ Section CORRECT. sem ctx expr v. Proof. Admitted. - Lemma norm_expr_Extract : + Lemma norm_expr_replace : 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 = false -> @sem_pred_expr A B sem ctx (NE.replace pred_expr_item_eq (pe, expr) (⟂, expr) x) v. - Proof. - induction x. - { simplify. destruct_match; auto. destruct a. - unfold pred_expr_item_eq in Heqb. simplify. - destruct (equiv_dec pe p) eqn:?; try easy. - rewrite e0 in H1. - inv H. crush. - } - { simplify. - } + Proof using. + induction x; simplify; destruct_match; auto; destruct a; + unfold pred_expr_item_eq in Heqb; simplify; + try (destruct (equiv_dec pe p) eqn:?; [|discriminate]; []). + - rewrite e0 in H0; inv H; crush. + - apply beq_expression_correct in H2; subst; + pose proof H0; rewrite e0 in H2; + apply sem_pred_expr_cons_false; auto; inv H; crush. + - inv H; constructor; auto; now apply sem_pred_expr_cons_false. + Qed. Section SEM_PRED. @@ -1001,6 +1049,16 @@ Section CORRECT. cbn -[l] in *. Lemma check_correct_sem_value: + forall x x' v v' t t' h h', + beq_pred_expr x x' = true -> + norm_expression (Pos.max (max_pred_expr x) (max_pred_expr x')) x (PTree.empty _) = (t, h) -> + norm_expression (Pos.max (max_pred_expr x) (max_pred_expr x')) x' h = (t', h') -> + sem_pred_tree isem ictx h' t v -> + sem_pred_tree osem octx h' t' v' -> + v = v'. + Proof. + + Lemma check_correct_sem_value: forall x x' v v', beq_pred_expr x x' = true -> sem_pred_expr isem ictx x v -> diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v index ec558c6..dc70010 100644 --- a/src/hls/Predicate.v +++ b/src/hls/Predicate.v @@ -417,3 +417,29 @@ Instance DecidableSATSetoid : DecidableSetoid SATSetoid := #[global] Instance SATSetoidEqDec : EqDec SATSetoid := equiv_check_decidable2. + +Definition Pimplies p p' := ¬ p ∨ p'. + +Notation "A → B" := (Pimplies A B) (at level 30) : pred_op. + +Definition implies p p' := + forall c, sat_predicate p c = true -> sat_predicate p' c = true. + +Notation "A ⇒ B" := (implies A B) (at level 35) : pred_op. + +Lemma Pimplies_implies: forall p p', (p → p') ∧ p ⇒ p'. +Proof. + unfold "→", "⇒"; simplify. + apply orb_prop in H0. inv H0; auto. rewrite negate_correct in H. + apply negb_true_iff in H. crush. +Qed. + +#[global] +Instance PimpliesProper : Proper (equiv ==> equiv ==> equiv) Pimplies. +Proof. + unfold Proper, "==>". simplify. unfold "→". + intros. + unfold sat_equiv in *. intros. + simplify. repeat rewrite negate_correct. rewrite H0. rewrite H. + auto. +Qed. |