diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-05-06 13:33:32 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-06 13:33:32 +0100 |
commit | 4290ead0dfdda0400dae528b66a38fe39dbbb18e (patch) | |
tree | fec8638473548508a143650da99283656f7aee76 /src/hls/Abstr.v | |
parent | 3e1aab82d0e14bdd120515a6e098c1c63e73427e (diff) | |
download | vericert-4290ead0dfdda0400dae528b66a38fe39dbbb18e.tar.gz vericert-4290ead0dfdda0400dae528b66a38fe39dbbb18e.zip |
Add check for mutexcl and fix top-level proof
Diffstat (limited to 'src/hls/Abstr.v')
-rw-r--r-- | src/hls/Abstr.v | 371 |
1 files changed, 47 insertions, 324 deletions
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index cd2d3d2..9c52d45 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -1339,12 +1339,12 @@ Section SEM_PRED_EXEC. End SEM_PRED_EXEC. -Module HashExprNorm(H: Hashable). - Module H := HashTree(H). +Module HashExprNorm(HS: Hashable). + Module H := HashTree(HS). Definition norm_tree: Type := PTree.t pred_op * H.hash_tree. - Fixpoint norm_expression (max: predicate) (pe: predicated H.t) (h: H.hash_tree) + Fixpoint norm_expression (max: predicate) (pe: predicated HS.t) (h: H.hash_tree) : norm_tree := match pe with | NE.singleton (p, e) => @@ -1372,18 +1372,18 @@ Module HashExprNorm(H: Hashable). let (tree, h) := norm_expression max pe h in (mk_pred_stmnt tree, h). - Definition pred_expr_dec: forall pe1 pe2: predicated H.t, + Definition pred_expr_dec: forall pe1 pe2: predicated HS.t, {pe1 = pe2} + {pe1 <> pe2}. Proof. - pose proof H.eq_dec as X. + pose proof HS.eq_dec as X. pose proof (Predicate.eq_dec peq). pose proof (NE.eq_dec _ X). - assert (forall a b: pred_op * H.t, {a = b} + {a <> b}) + assert (forall a b: pred_op * HS.t, {a = b} + {a <> b}) by decide equality. decide equality. Defined. - Definition beq_pred_expr' (pe1 pe2: predicated H.t) : bool := + Definition beq_pred_expr' (pe1 pe2: predicated HS.t) : bool := if pred_expr_dec pe1 pe2 then true else let (p1, h) := encode_expression 1%positive pe1 (PTree.empty _) in let (p2, h') := encode_expression 1%positive pe2 h in @@ -1415,7 +1415,7 @@ Module HashExprNorm(H: Hashable). | None => equiv_check p ⟂ end. - Definition beq_pred_expr (pe1 pe2: predicated H.t) : bool := + Definition beq_pred_expr (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 @@ -1466,12 +1466,12 @@ Module HashExprNorm(H: Hashable). Context {G B: Type}. Context (f: PTree.t pred_pexpr). Context (ps: PMap.t bool). - Context (a_sem: @Abstr.ctx G -> H.t -> B -> Prop). + Context (a_sem: @Abstr.ctx G -> HS.t -> B -> Prop). Context (ctx: @Abstr.ctx G). Context (F_EVALULABLE: forall x, sem_pexpr ctx (get_forest_p' x f) ps !! x). - Variant sem_pred_tree: PTree.t H.t -> PTree.t pred_op -> B -> Prop := + Variant sem_pred_tree: PTree.t HS.t -> PTree.t pred_op -> B -> Prop := | sem_pred_tree_intro : forall expr e v et pt pr, sem_pexpr ctx (from_pred_op f pr) true -> @@ -1551,9 +1551,9 @@ Module HashExprNorm(H: Hashable). Qed. Definition pred_Ht_dec : - forall x y: pred_op * H.t, {x = y} + {x <> y}. + forall x y: pred_op * HS.t, {x = y} + {x <> y}. Proof. - pose proof H.eq_dec. + pose proof HS.eq_dec. pose proof (@Predicate.eq_dec positive peq). decide equality. Defined. @@ -1745,10 +1745,31 @@ End HashExprNorm. Module HN := HashExprNorm(HashExpr). Module EHN := HashExprNorm(EHashExpr). +Definition and_list {A} (p: list (@Predicate.pred_op A)): @Predicate.pred_op A := + fold_left Pand p T. + +Definition or_list {A} (p: list (@Predicate.pred_op A)): @Predicate.pred_op A := + fold_left Por p ⟂. + +Definition check_mutexcl {A} (pe: predicated A) := + let preds := map fst (NE.to_list pe) in + let pairs := map (fun x => x → or_list (remove (Predicate.eq_dec peq) x preds)) preds in + match sat_pred_simple (simplify (negate (and_list pairs))) with + | None => true + | _ => false + end. + +Definition check_mutexcl_tree {A} (f: PTree.t (predicated A)) := + forall_ptree (fun _ => check_mutexcl) f. + Definition check f1 f2 := - RTree.beq beq_pred_expr f1.(forest_regs) f2.(forest_regs) + RTree.beq HN.beq_pred_expr f1.(forest_regs) f2.(forest_regs) && PTree.beq beq_pred_pexpr f1.(forest_preds) f2.(forest_preds) - && beq_pred_eexpr f1.(forest_exit) f2.(forest_exit). + && EHN.beq_pred_expr f1.(forest_exit) f2.(forest_exit) + && check_mutexcl_tree f1.(forest_regs) + && check_mutexcl_tree f2.(forest_regs) + && check_mutexcl f1.(forest_exit) + && check_mutexcl f2.(forest_exit). Lemma sem_pexpr_forward_eval1 : forall A ctx f_p ps, @@ -1803,305 +1824,6 @@ Proof. intros; destruct b; eauto using sem_pexpr_forward_eval1, sem_pexpr_forward_eval2. Qed. -Lemma norm_expression_sem_pred : - forall A B f sem ctx pe v, - sem_pred_expr f sem ctx pe v -> - (forall x : positive, sem_pexpr ctx (get_forest_p' x f) (ctx_ps ctx) !! x) -> - forall pt et et' max, - predicated_mutexcl pe -> - max_pred_expr pe <= max -> - HN.norm_expression max pe et = (pt, et') -> - @sem_pred_tree A B sem ctx et' pt v. -Proof. - induction 1; crush; repeat (destruct_match; []); try destruct_match; - match goal with - | H: (_, _) = (_, _) |- _ => inv H - end. - { econstructor. 3: { apply PTree.gss. } - 2: { eassumption. } - { simplify. pose proof Heqp as Y1. apply hash_value_in in Y1. - eapply norm_expr_constant in Heqn; [|eassumption]. eapply sem_pexpr_forward_eval in H. - rewrite eval_predf_Por. rewrite H. eauto with bool. assumption. } -(* { apply hash_value_in in Heqp. eapply norm_expr_constant in Heqp0; eauto. } - } - { econstructor; eauto. apply PTree.gss. - apply hash_value_in in Heqp. - eapply norm_expr_constant in Heqp0; eauto. - } - { assert (sem_pred_tree sem0 ctx0 et' t v). - eapply IHsem_pred_expr. - eapply predicated_cons; eauto. - instantiate (1 := max). lia. - eassumption. - inv H3. - destruct (Pos.eq_dec e0 h); subst. rewrite H6 in Heqo. simplify. - econstructor; try apply PTree.gss; eauto. - unfold eval_predf in *. simplify. auto with bool. - econstructor; eauto. now rewrite PTree.gso. - } - { assert (X: sem_pred_tree sem0 ctx0 et' t v). - eapply IHsem_pred_expr. - eapply predicated_cons; eauto. - instantiate (1 := max). lia. - eassumption. - inv X. - destruct (Pos.eq_dec e0 h); crush. - econstructor; eauto. now rewrite PTree.gso. - } - { econstructor; eauto. apply PTree.gss. - eapply hash_value_in; eassumption. - } -Qed.*) Admitted. - -Lemma norm_expression_sem_pred2 : - forall A B f sem ctx v pt et et', - @sem_pred_tree A B sem ctx et' pt v -> - (forall x : positive, sem_pexpr ctx (get_forest_p' x f) (ctx_ps ctx) !! x) -> - forall pe, - predicated_mutexcl pe -> - HN.norm_expression (max_pred_expr pe) pe et = (pt, et') -> - sem_pred_expr f sem ctx pe v. -Proof. Admitted. - - - - #[local] Opaque PTree.set. - - Lemma exists_norm_expr : - forall x pe expr m t h h', - NE.In (pe, expr) x -> - HN.norm_expression m x h = (t, h') -> - 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', - t ! e = None -> - norm_expression m x h = (t, h') -> - ~ NE.In (pe, expr) x. - Proof. - Abort.*) - -(* 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 -> - NE.In (pe, expr) x -> - eval_predf (ctx_ps ctx) pe = true -> - sem ctx expr v. - Proof. Admitted. - - Lemma norm_expr_forall_impl : - forall m x h t h' e1 e2 p1 p2, - predicated_mutexcl x -> - norm_expression m x h = (t, h') -> - t ! e1 = Some p1 -> t ! e2 = Some p2 -> e1 <> e2 -> - p1 ⇒ ¬ p2. - Admitted. - - Lemma norm_expr_replace : - forall A B sem ctx x pe expr v, - @sem_pred_expr A B sem ctx x v -> - 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 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. - - Context (B: Type). - Context {FUN TFUN: Type}. - Context (ictx: @ctx FUN) (octx: @ctx TFUN) (HSIM: similar ictx octx). - - Context (isem: @ctx FUN -> expression -> B -> Prop). - Context (osem: @ctx TFUN -> expression -> B -> Prop). - Context (SEMSIM: forall e v v', isem ictx e v -> osem octx e v' -> v = v'). - - Ltac simplify' l := intros; unfold_constants; cbn -[l] in *; - repeat (nicify_hypotheses; nicify_goals; kill_bools; substpp); - cbn -[l] in *. - - Lemma check_correct_sem_value: - forall x x' v v' t t' h h', - beq_pred_expr x x' = true -> - predicated_mutexcl x -> predicated_mutexcl x' -> - HN.norm_expression (Pos.max (max_pred_expr x) (max_pred_expr x')) x (PTree.empty _) = (t, h) -> - HN.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 using HSIM SEMSIM. - intros. inv H4. inv H5. - destruct (Pos.eq_dec e e0); subst. - { eapply norm_expr_constant in H3; [|eassumption]. - assert (expr = expr0) by (setoid_rewrite H3 in H12; crush); subst. - eapply SEMSIM; eauto. } - { destruct (t ! e0) eqn:?. - { assert (p == pr0). - { unfold beq_pred_expr in H. - destruct_match. subst. assert (t = t') by admit. subst. setoid_rewrite Heqo in H11. inv H11. - reflexivity. - repeat (destruct_match; []). - (*rewrite Heqp1 in H3. inv H3. - simplify. - eapply forall_ptree_true in H2. 2: { eapply Heqo. } - unfold tree_equiv_check_el in H2. rewrite H11 in H2. - now apply equiv_check_correct in H2. } - pose proof H0. eapply norm_expr_forall_impl in H0; [| | | |eassumption]; try eassumption. - unfold "⇒" in H0. unfold eval_predf in *. apply H0 in H6. - rewrite negate_correct in H6. apply negb_true_iff in H6. - inv HSIM. match goal with H: match_states _ _ |- _ => inv H end. - unfold ctx_ps, ctx_mem, ctx_rs in *. simplify. - pose proof eval_predf_pr_equiv pr0 ps ps' H17. unfold eval_predf in *. - rewrite H5 in H6. crush. - } - { unfold beq_pred_expr in H. repeat (destruct_match; []). inv H2. - rewrite Heqp0 in H3. inv H3. simplify. - eapply forall_ptree_true in H3. 2: { eapply H11. } - unfold tree_equiv_check_None_el in H3. - rewrite Heqo in H3. apply equiv_check_correct in H3. rewrite H3 in H4. - unfold eval_predf in H4. crush. } } - Qed.*) Admitted. - - Lemma check_correct_sem_value2: - forall f x x' v v', - (forall x : positive, sem_pexpr ictx (get_forest_p' x f) (ctx_ps ictx) !! x) -> - (forall x : positive, sem_pexpr octx (get_forest_p' x f) (ctx_ps octx) !! x) -> - beq_pred_expr x x' = true -> - predicated_mutexcl x -> - predicated_mutexcl x' -> - sem_pred_expr f isem ictx x v -> - sem_pred_expr f osem octx x' v' -> - v = v'. - Proof. - intros * FRL1 FRL2 **. pose proof H. - unfold beq_pred_expr in H. intros. repeat (destruct_match; try discriminate; []). - eapply check_correct_sem_value; try eassumption. admit. admit. - eapply norm_expression_sem_pred; eauto. (*lia.*) admit. admit. - eapply norm_expression_sem_pred; eauto. (*lia.*) admit. admit. - Admitted. - - Lemma check_correct_sem_value3: - forall f x x' v v', - beq_pred_expr x x' = true -> - sem_pred_expr f isem ictx x v -> - sem_pred_expr f osem octx x' v' -> - v = v'. - Proof. - induction x. - - intros * BEQ SEM1 SEM2. - unfold beq_pred_expr in *. - destruct_match; subst. (* det argument *) admit. - repeat (destruct_match; try discriminate; []); subst. - rename Heqn0 into HNORM1. - rename Heqn1 into HNORM2. - inv SEM1. rename H0 into HEVAL. rename H2 into ISEM. - pose HNORM1 as X. - eapply exists_norm_expr in X; [|constructor]. - cbn in *. simplify. -(* simplify' norm_expression.*) - rename H0 into HT1. - rename H1 into HH1. - rename H into HFORALL1. - rename H2 into HFORALL2. - destruct (t0 ! x) eqn:DSTR. -(* { eapply forall_ptree_true in HT1; eauto. unfold tree_equiv_check_el in *. rewrite DSTR in HT1. - apply equiv_check_dec in HT1. - eapply exists_norm_expr2 in DSTR; try solve [eapply norm_expr_constant; eassumption | eassumption]. - eapply norm_expr_In in DSTR; try eassumption. eauto. - inv HSIM; simplify. now setoid_rewrite <- HT1. - } - { - eapply forall_ptree_true in HT1; [|eassumption]. - unfold tree_equiv_check_el in *. rewrite DSTR in HT1. apply equiv_check_dec in HT1. - now setoid_rewrite HT1 in HEVAL. - } - - intros. unfold beq_pred_expr in H. intros. repeat (destruct_match; try discriminate; []); subst. - destruct a. - inv H0. - { pose Heqp as X. eapply exists_norm_expr in X; [|constructor; tauto]. simplify' norm_expression. - eapply forall_ptree_true in H0; [|eassumption]. - destruct (t0 ! x0) eqn:DSTR. - { - unfold tree_equiv_check_el in H0. rewrite DSTR in H0. apply equiv_check_dec in H0. - eapply exists_norm_expr2 in DSTR; try solve [eapply norm_expr_constant; eassumption | eassumption]. - eapply norm_expr_In in DSTR; try eassumption; eauto. - rewrite <- H0. inv HSIM; eauto. - } - { - unfold tree_equiv_check_el in *. rewrite DSTR in H0. apply equiv_check_dec in H0. - now rewrite H0 in H7. - } - } - { (* This is the inductive argument, which says that if the element is in the list, then - taking it out will result in two equivalent lists, otherwise just taking the current element - results in equivalent lists.*) - simplify' norm_expression. eapply exists_norm_expr in Heqp; [|constructor]; eauto. - simplify' norm_expression. - eapply forall_ptree_true in H0; [|eassumption]. - unfold tree_equiv_check_el in H0. - destruct (t0 ! x0) eqn:DSTR. - { - apply equiv_check_dec in H0. - eapply exists_norm_expr2 in DSTR; try solve [eapply norm_expr_constant; eassumption | eassumption]. - } - } - Admitted.*) Abort. - - End SEM_PRED. - - Section SEM_PRED_CORR. - - Context {B: Type}. - Context {FUN TFUN: Type}. - Context (ictx: @ctx FUN) (octx: @ctx TFUN) (HSIM: similar ictx octx). - - Context (isem: @ctx FUN -> expression -> B -> Prop). - Context (osem: @ctx TFUN -> expression -> B -> Prop). - Context (SEMCORR: forall e v, isem ictx e v -> osem octx e v). - -(* Lemma sem_pred_tree_corr: - forall x x' v t t' h h', - beq_pred_expr x x' = true -> - predicated_mutexcl x -> predicated_mutexcl x' -> - 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. - Proof using SEMCORR. Admitted.*) - - Lemma check_correct: forall (fa fb : forest) i i', - check fa fb = true -> - sem ictx fa i -> - sem octx fb i' -> - match_states (fst i) (fst i') /\ snd i = snd i'. - Proof using HSIM. - Admitted. - - Lemma check_correct2: - forall (fa fb : forest) i, - check fa fb = true -> - sem ictx fa i -> - exists i', sem octx fb i' /\ match_states (fst i) (fst i') /\ snd i = snd i'. - Proof. Admitted. - - End SEM_PRED_CORR. - Lemma get_empty: forall r, empty#r r = NE.singleton (Ptrue, Ebase r). Proof. unfold "#r"; intros. rewrite RTree.gempty. trivial. Qed. @@ -2348,31 +2070,31 @@ Qed. Lemma sem_expr_beq_correct : forall pt a b v, - beq_pred_expr a b = true -> + HN.beq_pred_expr a b = true -> sem_pred_expr pt sem_value ctx a v -> sem_pred_expr pt sem_value ctx b v. Proof. - intros. unfold beq_pred_expr in H. destruct_match; subst; auto. + intros. unfold HN.beq_pred_expr in H. destruct_match; subst; auto. repeat (destruct_match; []). simplify. Admitted. Lemma sem_expr_beq_correct_mem : forall pt a b v, - beq_pred_expr a b = true -> + HN.beq_pred_expr a b = true -> sem_pred_expr pt sem_mem ctx a v -> sem_pred_expr pt sem_mem ctx b v. Proof. Admitted. Lemma sem_expr_beq_correct_exit : forall pt a b v, - beq_pred_eexpr a b = true -> + EHN.beq_pred_expr a b = true -> sem_pred_expr pt sem_exit ctx a v -> sem_pred_expr pt sem_exit ctx b v. Proof. Admitted. Lemma sem_eexpr_beq_correct : forall pt a b v, - beq_pred_eexpr a b = true -> + EHN.beq_pred_expr a b = true -> sem_pred_expr pt sem_exit ctx a v -> sem_pred_expr pt sem_exit ctx b v. Proof. Admitted. @@ -2392,14 +2114,15 @@ Qed. Lemma tree_beq_pred_expr : forall a b x, - RTree.beq beq_pred_expr (forest_regs a) (forest_regs b) = true -> - beq_pred_expr a #r x b #r x = true. + RTree.beq HN.beq_pred_expr (forest_regs a) (forest_regs b) = true -> + HN.beq_pred_expr a #r x b #r x = true. Proof. - intros. unfold "#r". + intros. unfold "#r" in *. apply PTree.beq_correct with (x := (R_indexed.index x)) in H. - unfold RTree.get in *. + unfold RTree.get in *. + unfold pred_expr in *. destruct_match; destruct_match; auto. - unfold beq_pred_expr. destruct_match; auto. + unfold HN.beq_pred_expr. destruct_match; auto. Qed. Section CORRECT. @@ -2414,7 +2137,7 @@ Lemma abstr_check_correct : exists ti', sem octx b (ti', cf) /\ match_states i' ti'. Proof. intros. unfold check in H. simplify. - inv H0. inv H5. inv H6. + inv H0. inv H9. inv H10. eexists. split. { constructor. - constructor. intros. |