From 3be880b441a4d2926c6b14b7bb25a04209fbbca6 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 19 May 2023 12:51:39 +0100 Subject: Finish evaluability proof of RBop --- src/hls/AbstrSemIdent.v | 7 +- src/hls/GiblePargenproofBackward.v | 60 ++++++--- src/hls/GiblePargenproofCommon.v | 264 +++++++++++++++++++++++++++++++++++++ src/hls/GiblePargenproofEquiv.v | 26 ++++ src/hls/GiblePargenproofForward.v | 191 +-------------------------- 5 files changed, 338 insertions(+), 210 deletions(-) create mode 100644 src/hls/GiblePargenproofCommon.v (limited to 'src/hls') diff --git a/src/hls/AbstrSemIdent.v b/src/hls/AbstrSemIdent.v index 0cc8e9d..36c3ffc 100644 --- a/src/hls/AbstrSemIdent.v +++ b/src/hls/AbstrSemIdent.v @@ -96,10 +96,10 @@ Proof. Lemma sem_pred_expr_app_predicated_false2 : forall f_p y x v p ps, - sem_pred_expr f_p sem ctx (app_predicated p y x) v -> + sem_pred_expr f_p a_sem ctx (app_predicated p y x) v -> (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) -> eval_predf ps p = false -> - sem_pred_expr f_p sem ctx y v. + sem_pred_expr f_p a_sem ctx y v. Admitted. Lemma sem_pred_expr_pred_ret : @@ -601,7 +601,8 @@ Proof. rewrite Eapp_right_nil. auto. Qed. -Lemma sem_merge_list : (* [[id:f307d227-d0e9-49a0-823f-2d7e0db76972]] *) +(* [[id:f307d227-d0e9-49a0-823f-2d7e0db76972]] *) +Lemma sem_merge_list : forall f rs ps m args, sem ctx f ((mk_instr_state rs ps m), None) -> sem_pred_expr (forest_preds f) sem_val_list ctx diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v index 718eb66..db0df19 100644 --- a/src/hls/GiblePargenproofBackward.v +++ b/src/hls/GiblePargenproofBackward.v @@ -30,6 +30,7 @@ Require Import vericert.hls.GibleSeq. Require Import vericert.hls.GiblePar. Require Import vericert.hls.Gible. Require Import vericert.hls.GiblePargenproofEquiv. +Require Import vericert.hls.GiblePargenproofCommon. Require Import vericert.hls.GiblePargen. Require Import vericert.hls.Predicate. Require Import vericert.hls.Abstr. @@ -132,30 +133,55 @@ Lemma evaluable_pred_expr_exists : forall sp pr f i0 exit_p exit_p' f' i ti p op args dst, (forall x, sem_pexpr (mk_ctx i0 sp ge) (get_forest_p' x f'.(forest_preds)) (pr !! x)) -> eval_predf pr exit_p = true -> + valid_mem (is_mem i0) (is_mem i) -> update (exit_p, f) (RBop p op args dst) = Some (exit_p', f') -> sem (mk_ctx i0 sp ge) f (i, None) -> evaluable_pred_expr (mk_ctx i0 sp ge) f'.(forest_preds) (f' #r (Reg dst)) -> state_lessdef i ti -> - exists ti', step_instr ge sp (Iexec ti) (RBop p op args dst) (Iexec ti'). + exists ti', + step_instr ge sp (Iexec ti) (RBop p op args dst) (Iexec ti'). Proof. - intros * HPRED HEVAL **. cbn -[seq_app] in H. unfold Option.bind in H. destr. inv H. + intros * HPRED HEVAL VALID_MEM **. cbn -[seq_app] in H. unfold Option.bind in H. destr. inv H. destruct ti. unfold evaluable_pred_expr in H1. destruct H1 as (r & Heval). rewrite forest_reg_gss in Heval. - exploit sem_pred_expr_prune_predicated2; eauto; intros. - assert (eval_predf pr (dfltp p ∧ exit_p') = true) by admit. - exploit sem_pred_expr_app_predicated2; eauto; intros. - exploit sem_pred_expr_seq_app_val2; eauto; simplify. - unfold pred_ret in *. inv H4. inv H12. - destruct i. exploit sem_merge_list; eauto; intros. - instantiate (1 := args) in H4. - eapply sem_pred_expr_ident2 in H4. simplify. - exploit sem_pred_expr_ident_det. eapply H5. eapply H4. - intros. subst. exploit sem_pred_expr_ident. eapply H5. eapply H8. - intros. - - econstructor. econstructor. - Admitted. + exploit sem_pred_expr_prune_predicated2; eauto; intros. cbn in HPRED. + pose proof (truthy_dec pr p) as YH. inversion_clear YH as [YH'|YH']. + - assert (eval_predf pr (dfltp p ∧ exit_p') = true). + { pose proof (truthy_dflt _ _ YH'). rewrite eval_predf_Pand. + rewrite H1. now rewrite HEVAL. } + exploit sem_pred_expr_app_predicated2; eauto; intros. + exploit sem_pred_expr_seq_app_val2; eauto; simplify. + unfold pred_ret in *. inv H4. inv H12. + destruct i. exploit sem_merge_list; eauto; intros. + instantiate (1 := args) in H4. + eapply sem_pred_expr_ident2 in H4. simplify. + exploit sem_pred_expr_ident_det. eapply H5. eapply H4. + intros. subst. inv H7. + eapply sem_val_list_det in H8; eauto; [|reflexivity]. subst. + inv H2. + econstructor. constructor. + + cbn in *. eapply eval_operation_valid_pointer. symmetry; eauto. + unfold ctx_mem in H14. cbn in H14. erewrite <- match_states_list; eauto. + + inv H0. + assert (sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f pr) + by (now constructor). + pose proof (sem_predset_det _ _ ltac:(reflexivity) _ _ _ H0 H17). + assert (truthy is_ps0 p). + { eapply truthy_match_state; eassumption. } + eapply truthy_match_state; eassumption. + - inv YH'. cbn -[seq_app] in H. + assert (eval_predf pr (p0 ∧ exit_p') = false). + { rewrite eval_predf_Pand. now rewrite H1. } + eapply sem_pred_expr_app_predicated_false2 in H; eauto. + eexists. eapply exec_RB_falsy. constructor. auto. cbn. + assert (sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f pr) + by (now constructor). + inv H0. pose proof (sem_predset_det _ _ ltac:(reflexivity) _ _ _ H4 H8). + inv H2. + erewrite <- eval_predf_pr_equiv by exact H16. + now erewrite <- eval_predf_pr_equiv by exact H0. +Qed. Lemma remember_expr_in : forall x l f a, @@ -289,7 +315,7 @@ Proof. - cbn in *. inv Y. assert (similar {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |}) - by auto using similar_refl. + by reflexivity. now eapply sem_det in H; [| eapply Y1 | eapply Y3 ]. - cbn -[update] in Y. pose proof Y as YX. diff --git a/src/hls/GiblePargenproofCommon.v b/src/hls/GiblePargenproofCommon.v new file mode 100644 index 0000000..8d8e0a2 --- /dev/null +++ b/src/hls/GiblePargenproofCommon.v @@ -0,0 +1,264 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2023 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +Require Import compcert.backend.Registers. +Require Import compcert.common.AST. +Require Import compcert.common.Errors. +Require Import compcert.common.Linking. +Require Import compcert.common.Globalenvs. +Require Import compcert.common.Memory. +Require Import compcert.common.Values. +Require Import compcert.lib.Maps. + +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.GibleSeq. +Require Import vericert.hls.GiblePar. +Require Import vericert.hls.Gible. +Require Import vericert.hls.GiblePargenproofEquiv. +Require Import vericert.hls.GiblePargen. +Require Import vericert.hls.Predicate. +Require Import vericert.hls.Abstr. +Require Import vericert.hls.AbstrSemIdent. +Require Import vericert.common.Monad. + +Module Import OptionExtra := MonadExtra(Option). + +#[local] Open Scope positive. +#[local] Open Scope forest. +#[local] Open Scope pred_op. + +#[local] Opaque simplify. +#[local] Opaque deep_simplify. + +#[local] Ltac destr := destruct_match; try discriminate; []. + +Lemma storev_valid_pointer1 : + forall chunk m m' s d b z, + Mem.storev chunk m s d = Some m' -> + Mem.valid_pointer m b z = true -> + Mem.valid_pointer m' b z = true. +Proof using. + intros. unfold Mem.storev in *. destruct_match; try discriminate; subst. + apply Mem.valid_pointer_nonempty_perm. apply Mem.valid_pointer_nonempty_perm in H0. + eapply Mem.perm_store_1; eauto. +Qed. + +Lemma storev_valid_pointer2 : + forall chunk m m' s d b z, + Mem.storev chunk m s d = Some m' -> + Mem.valid_pointer m' b z = true -> + Mem.valid_pointer m b z = true. +Proof using. + intros. unfold Mem.storev in *. destruct_match; try discriminate; subst. + apply Mem.valid_pointer_nonempty_perm. apply Mem.valid_pointer_nonempty_perm in H0. + eapply Mem.perm_store_2; eauto. +Qed. + +Definition valid_mem m m' := + forall b z, Mem.valid_pointer m b z = Mem.valid_pointer m' b z. + +#[global] Program Instance valid_mem_Equivalence : Equivalence valid_mem. +Next Obligation. unfold valid_mem; auto. Qed. (* Reflexivity *) +Next Obligation. unfold valid_mem; auto. Qed. (* Symmetry *) +Next Obligation. unfold valid_mem; eauto. Qed. (* Transitity *) + +Lemma storev_valid_pointer : + forall chunk m m' s d, + Mem.storev chunk m s d = Some m' -> + valid_mem m m'. +Proof using. + unfold valid_mem. symmetry. + intros. destruct (Mem.valid_pointer m b z) eqn:?; + eauto using storev_valid_pointer1. + apply not_true_iff_false. + apply not_true_iff_false in Heqb0. + eauto using storev_valid_pointer2. +Qed. + +Lemma storev_cmpu_bool : + forall m m' c v v0, + valid_mem m m' -> + Val.cmpu_bool (Mem.valid_pointer m) c v v0 = Val.cmpu_bool (Mem.valid_pointer m') c v v0. +Proof using. + unfold valid_mem. + intros. destruct v, v0; crush. + { destruct_match; crush. + destruct_match; crush. + destruct_match; crush. + apply orb_true_iff in H1. + inv H1. rewrite H in H2. rewrite H2 in Heqb1. + simplify. rewrite H0 in Heqb1. crush. + rewrite H in H2. rewrite H2 in Heqb1. + rewrite H0 in Heqb1. crush. + destruct_match; auto. simplify. + apply orb_true_iff in H1. + inv H1. rewrite <- H in H2. rewrite H2 in Heqb1. + simplify. rewrite H0 in Heqb1. crush. + rewrite <- H in H2. rewrite H2 in Heqb1. + rewrite H0 in Heqb1. crush. } + + { destruct_match; crush. + destruct_match; crush. + destruct_match; crush. + apply orb_true_iff in H1. + inv H1. rewrite H in H2. rewrite H2 in Heqb1. + simplify. rewrite H0 in Heqb1. crush. + rewrite H in H2. rewrite H2 in Heqb1. + rewrite H0 in Heqb1. crush. + destruct_match; auto. simplify. + apply orb_true_iff in H1. + inv H1. rewrite <- H in H2. rewrite H2 in Heqb1. + simplify. rewrite H0 in Heqb1. crush. + rewrite <- H in H2. rewrite H2 in Heqb1. + rewrite H0 in Heqb1. crush. } + + { destruct_match; auto. destruct_match; auto; crush. + { destruct_match; crush. + { destruct_match; crush. + setoid_rewrite H in H0; eauto. + setoid_rewrite H in H1; eauto. + rewrite H0 in Heqb. rewrite H1 in Heqb; crush. + } + { destruct_match; crush. + setoid_rewrite H in Heqb0; eauto. + rewrite H0 in Heqb0. rewrite H1 in Heqb0; crush. } } + { destruct_match; crush. + { destruct_match; crush. + setoid_rewrite H in H0; eauto. + setoid_rewrite H in H1; eauto. + rewrite H0 in Heqb0. rewrite H1 in Heqb0; crush. + } + { destruct_match; crush. + setoid_rewrite H in Heqb0; eauto. + rewrite H0 in Heqb0. rewrite H1 in Heqb0; crush. } } } +Qed. + +Lemma storev_eval_condition : + forall m m' c rs, + valid_mem m m' -> + Op.eval_condition c rs m = Op.eval_condition c rs m'. +Proof using. + intros. destruct c; crush. + destruct rs; crush. + destruct rs; crush. + destruct rs; crush. + eapply storev_cmpu_bool; eauto. + destruct rs; crush. + destruct rs; crush. + eapply storev_cmpu_bool; eauto. +Qed. + +Lemma eval_operation_valid_pointer : + forall A B (ge: Genv.t A B) sp op args m m' v, + valid_mem m m' -> + Op.eval_operation ge sp op args m' = Some v -> + Op.eval_operation ge sp op args m = Some v. +Proof. + intros * VALID OP. destruct op; auto. + - destruct cond; auto; cbn in *. + + repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto. + + repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto. + - destruct c; auto; cbn in *. + + repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto. + + repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto. +Qed. + +Lemma bb_memory_consistency_eval_operation : + forall A B (ge: Genv.t A B) sp state i state' args op v, + step_instr ge sp (Iexec state) i (Iexec state') -> + Op.eval_operation ge sp op args (is_mem state) = Some v -> + Op.eval_operation ge sp op args (is_mem state') = Some v. +Proof. + inversion_clear 1; intro EVAL; auto. + cbn in *. + eapply eval_operation_valid_pointer. unfold valid_mem. symmetry. + eapply storev_valid_pointer; eauto. + auto. +Qed. + +Lemma truthy_dflt : + forall ps p, + truthy ps p -> eval_predf ps (dfltp p) = true. +Proof. intros. destruct p; cbn; inv H; auto. Qed. + +Lemma exists_sem_pred : + forall A B C (ctx: @ctx A) s pr r v, + @sem_pred_expr A B C pr s ctx r v -> + exists r', + NE.In r' r /\ s ctx (snd r') v. +Proof. + induction r; crush. + - inv H. econstructor. split. constructor. auto. + - inv H. + + econstructor. split. constructor. left; auto. auto. + + exploit IHr; eauto. intros HH. inversion_clear HH as [x HH']. inv HH'. + 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 match_states_list : + forall A (rs: Regmap.t A) rs', + (forall r, rs !! r = rs' !! r) -> + forall l, rs ## l = rs' ## l. +Proof. induction l; crush. Qed. + +Lemma PTree_matches : + forall A (v: A) res rs rs', + (forall r, rs !! r = rs' !! r) -> + forall x, (Regmap.set res v rs) !! x = (Regmap.set res v rs') !! x. +Proof. + intros; destruct (Pos.eq_dec x res); subst; + [ repeat rewrite Regmap.gss by auto + | repeat rewrite Regmap.gso by auto ]; auto. +Qed. + +Lemma truthy_dec: + forall ps a, truthy ps a \/ falsy ps a. +Proof. + destruct a; try case_eq (eval_predf ps p); intuition (constructor; auto). +Qed. + +Lemma truthy_match_state : + forall ps ps' p, + (forall x, ps !! x = ps' !! x) -> + truthy ps p -> + truthy ps' p. +Proof. + intros; destruct p; inv H0; constructor; auto. + erewrite eval_predf_pr_equiv; eauto. +Qed. + +Lemma falsy_match_state : + forall ps ps' p, + (forall x, ps !! x = ps' !! x) -> + falsy ps p -> + falsy ps' p. +Proof. + intros; destruct p; inv H0; constructor; auto. + erewrite eval_predf_pr_equiv; eauto. +Qed. diff --git a/src/hls/GiblePargenproofEquiv.v b/src/hls/GiblePargenproofEquiv.v index 5f589a7..b63f2fd 100644 --- a/src/hls/GiblePargenproofEquiv.v +++ b/src/hls/GiblePargenproofEquiv.v @@ -342,6 +342,11 @@ Proof. - transitivity ist'; auto. Qed. +#[global] Instance similar_Equivalence {A} : Equivalence (@similar A A) := + { Equivalence_Reflexive := similar_refl A ; + Equivalence_Symmetric := similar_commut A A ; + Equivalence_Transitive := @similar_trans A A A ; }. + Module HashExpr' <: MiniDecidableType. Definition t := expression. Definition eq_dec := expression_dec. @@ -745,6 +750,27 @@ Section CORRECT. - inv H0; inv H1; eauto; exploit sem_pexpr_det; eauto; discriminate. Qed. + Lemma sem_predset_det: + forall f ps ps', + sem_predset ictx f ps -> + sem_predset octx f ps' -> + forall x, ps !! x = ps' !! x. + Proof. + intros. inv H. inv H0. eauto using sem_pexpr_det. + Qed. + + Lemma sem_regset_det: + forall f rs rs', + sem_regset ictx f rs -> + sem_regset octx f rs' -> + forall x, rs !! x = rs' !! x. + Proof. + intros. inv H. inv H0. + specialize (H1 x). specialize (H x). + eapply sem_pred_expr_det in H1; eauto. + exact sem_value_det. + Qed. + Lemma sem_det : forall p i cf i' cf', sem ictx p (i, cf) -> diff --git a/src/hls/GiblePargenproofForward.v b/src/hls/GiblePargenproofForward.v index 1d59216..bd18855 100644 --- a/src/hls/GiblePargenproofForward.v +++ b/src/hls/GiblePargenproofForward.v @@ -30,6 +30,7 @@ Require Import vericert.hls.GibleSeq. Require Import vericert.hls.GiblePar. Require Import vericert.hls.Gible. Require Import vericert.hls.GiblePargenproofEquiv. +Require Import vericert.hls.GiblePargenproofCommon. Require Import vericert.hls.GiblePargen. Require Import vericert.hls.Predicate. Require Import vericert.hls.Abstr. @@ -80,22 +81,6 @@ Lemma check_dest_l_dec i r : {check_dest_l i r = true} + {check_dest_l i r = false}. Proof. destruct (check_dest_l i r); tauto. Qed. -Lemma match_states_list : - forall A (rs: Regmap.t A) rs', - (forall r, rs !! r = rs' !! r) -> - forall l, rs ## l = rs' ## l. -Proof. induction l; crush. Qed. - -Lemma PTree_matches : - forall A (v: A) res rs rs', - (forall r, rs !! r = rs' !! r) -> - forall x, (Regmap.set res v rs) !! x = (Regmap.set res v rs') !! x. -Proof. - intros; destruct (Pos.eq_dec x res); subst; - [ repeat rewrite Regmap.gss by auto - | repeat rewrite Regmap.gso by auto ]; auto. -Qed. - Section CORRECTNESS. Context (prog: GibleSeq.program) (tprog : GiblePar.program). @@ -147,155 +132,6 @@ all be evaluable. econstructor; eauto. Qed. - Lemma storev_valid_pointer1 : - forall chunk m m' s d b z, - Mem.storev chunk m s d = Some m' -> - Mem.valid_pointer m b z = true -> - Mem.valid_pointer m' b z = true. - Proof using. - intros. unfold Mem.storev in *. destruct_match; try discriminate; subst. - apply Mem.valid_pointer_nonempty_perm. apply Mem.valid_pointer_nonempty_perm in H0. - eapply Mem.perm_store_1; eauto. - Qed. - - Lemma storev_valid_pointer2 : - forall chunk m m' s d b z, - Mem.storev chunk m s d = Some m' -> - Mem.valid_pointer m' b z = true -> - Mem.valid_pointer m b z = true. - Proof using. - intros. unfold Mem.storev in *. destruct_match; try discriminate; subst. - apply Mem.valid_pointer_nonempty_perm. apply Mem.valid_pointer_nonempty_perm in H0. - eapply Mem.perm_store_2; eauto. - Qed. - - Definition valid_mem m m' := - forall b z, Mem.valid_pointer m b z = Mem.valid_pointer m' b z. - - #[global] Program Instance valid_mem_Equivalence : Equivalence valid_mem. - Next Obligation. unfold valid_mem; auto. Qed. (* Reflexivity *) - Next Obligation. unfold valid_mem; auto. Qed. (* Symmetry *) - Next Obligation. unfold valid_mem; eauto. Qed. (* Transitity *) - - Lemma storev_valid_pointer : - forall chunk m m' s d, - Mem.storev chunk m s d = Some m' -> - valid_mem m m'. - Proof using. - unfold valid_mem. symmetry. - intros. destruct (Mem.valid_pointer m b z) eqn:?; - eauto using storev_valid_pointer1. - apply not_true_iff_false. - apply not_true_iff_false in Heqb0. - eauto using storev_valid_pointer2. - Qed. - - Lemma storev_cmpu_bool : - forall m m' c v v0, - valid_mem m m' -> - Val.cmpu_bool (Mem.valid_pointer m) c v v0 = Val.cmpu_bool (Mem.valid_pointer m') c v v0. - Proof using. - unfold valid_mem. - intros. destruct v, v0; crush. - { destruct_match; crush. - destruct_match; crush. - destruct_match; crush. - apply orb_true_iff in H1. - inv H1. rewrite H in H2. rewrite H2 in Heqb1. - simplify. rewrite H0 in Heqb1. crush. - rewrite H in H2. rewrite H2 in Heqb1. - rewrite H0 in Heqb1. crush. - destruct_match; auto. simplify. - apply orb_true_iff in H1. - inv H1. rewrite <- H in H2. rewrite H2 in Heqb1. - simplify. rewrite H0 in Heqb1. crush. - rewrite <- H in H2. rewrite H2 in Heqb1. - rewrite H0 in Heqb1. crush. } - - { destruct_match; crush. - destruct_match; crush. - destruct_match; crush. - apply orb_true_iff in H1. - inv H1. rewrite H in H2. rewrite H2 in Heqb1. - simplify. rewrite H0 in Heqb1. crush. - rewrite H in H2. rewrite H2 in Heqb1. - rewrite H0 in Heqb1. crush. - destruct_match; auto. simplify. - apply orb_true_iff in H1. - inv H1. rewrite <- H in H2. rewrite H2 in Heqb1. - simplify. rewrite H0 in Heqb1. crush. - rewrite <- H in H2. rewrite H2 in Heqb1. - rewrite H0 in Heqb1. crush. } - - { destruct_match; auto. destruct_match; auto; crush. - { destruct_match; crush. - { destruct_match; crush. - setoid_rewrite H in H0; eauto. - setoid_rewrite H in H1; eauto. - rewrite H0 in Heqb. rewrite H1 in Heqb; crush. - } - { destruct_match; crush. - setoid_rewrite H in Heqb0; eauto. - rewrite H0 in Heqb0. rewrite H1 in Heqb0; crush. } } - { destruct_match; crush. - { destruct_match; crush. - setoid_rewrite H in H0; eauto. - setoid_rewrite H in H1; eauto. - rewrite H0 in Heqb0. rewrite H1 in Heqb0; crush. - } - { destruct_match; crush. - setoid_rewrite H in Heqb0; eauto. - rewrite H0 in Heqb0. rewrite H1 in Heqb0; crush. } } } - Qed. - - Lemma storev_eval_condition : - forall m m' c rs, - valid_mem m m' -> - Op.eval_condition c rs m = Op.eval_condition c rs m'. - Proof using. - intros. destruct c; crush. - destruct rs; crush. - destruct rs; crush. - destruct rs; crush. - eapply storev_cmpu_bool; eauto. - destruct rs; crush. - destruct rs; crush. - eapply storev_cmpu_bool; eauto. - Qed. - - Lemma eval_operation_valid_pointer : - forall A B (ge: Genv.t A B) sp op args m m' v, - valid_mem m m' -> - Op.eval_operation ge sp op args m' = Some v -> - Op.eval_operation ge sp op args m = Some v. - Proof. - intros * VALID OP. destruct op; auto. - - destruct cond; auto; cbn in *. - + repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto. - + repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto. - - destruct c; auto; cbn in *. - + repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto. - + repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto. - Qed. - - Lemma bb_memory_consistency_eval_operation : - forall A B (ge: Genv.t A B) sp state i state' args op v, - step_instr ge sp (Iexec state) i (Iexec state') -> - Op.eval_operation ge sp op args (is_mem state) = Some v -> - Op.eval_operation ge sp op args (is_mem state') = Some v. - Proof. - inversion_clear 1; intro EVAL; auto. - cbn in *. - eapply eval_operation_valid_pointer. unfold valid_mem. symmetry. - eapply storev_valid_pointer; eauto. - auto. - Qed. - - Lemma truthy_dflt : - forall ps p, - truthy ps p -> eval_predf ps (dfltp p) = true. - Proof. intros. destruct p; cbn; inv H; auto. Qed. - Lemma sem_update_Istore : forall A rs args m v f ps ctx addr a0 chunk m' v', Op.eval_addressing (ctx_ge ctx) (ctx_sp ctx) addr rs ## args = Some a0 -> @@ -393,20 +229,6 @@ all be evaluable. + auto. Qed. - Lemma exists_sem_pred : - forall A B C (ctx: @ctx A) s pr r v, - @sem_pred_expr A B C pr s ctx r v -> - exists r', - NE.In r' r /\ s ctx (snd r') v. - Proof. - induction r; crush. - - inv H. econstructor. split. constructor. auto. - - inv H. - + econstructor. split. constructor. left; auto. auto. - + exploit IHr; eauto. intros HH. inversion_clear HH as [x HH']. inv HH'. - econstructor. split. constructor. right. eauto. auto. - Qed. - Lemma sem_update_Istore_top: forall A f p p' f' rs m pr res args p0 state addr a chunk m', Op.eval_addressing (ctx_ge state) (ctx_sp state) addr rs ## args = Some a -> @@ -451,17 +273,6 @@ all be evaluable. + 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 sem_pexpr_not_in : forall G (ctx: @ctx G) p0 ps p e b, ~ PredIn p p0 -> -- cgit