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/GiblePargenproofForward.v | 191 +------------------------------------- 1 file changed, 1 insertion(+), 190 deletions(-) (limited to 'src/hls/GiblePargenproofForward.v') 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