diff options
Diffstat (limited to 'src/hls/GiblePargenproofCommon.v')
-rw-r--r-- | src/hls/GiblePargenproofCommon.v | 264 |
1 files changed, 264 insertions, 0 deletions
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 <git@yannherklotz.com> + * + * 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 <https://www.gnu.org/licenses/>. + *) + +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. |