diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-05-25 13:40:53 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-25 13:40:53 +0100 |
commit | de8cc640dc5753df86bba7e6762df0058c475d55 (patch) | |
tree | cf0af33204d644b2431cc93ab5d0746de33ff8e8 /src/hls | |
parent | 899343189f60966ff161c9d5dac9caae5a28102e (diff) | |
download | vericert-de8cc640dc5753df86bba7e6762df0058c475d55.tar.gz vericert-de8cc640dc5753df86bba7e6762df0058c475d55.zip |
Finish predicate inclusion proofs
Diffstat (limited to 'src/hls')
-rw-r--r-- | src/hls/GiblePargenproofBackward.v | 147 |
1 files changed, 99 insertions, 48 deletions
diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v index 3fc6c52..5662215 100644 --- a/src/hls/GiblePargenproofBackward.v +++ b/src/hls/GiblePargenproofBackward.v @@ -690,8 +690,7 @@ Proof. + inv H0. eauto. Qed. -Transparent deep_simplify. - +#[local] Transparent deep_simplify. Lemma deep_simplify_in : forall pop pred, PredIn pred (deep_simplify peq pop) -> @@ -707,6 +706,25 @@ Proof. destruct (PredIn_decidable _ pred (deep_simplify peq pop2) peq); [intuition|]. repeat destruct_match; try solve [contradiction | inv H; inv H1; contradiction]. Qed. +Opaque deep_simplify. + +#[local] Transparent simplify. +Lemma simplify_in : + forall pop (pred: positive), + PredIn pred (simplify pop) -> + PredIn pred pop. +Proof. + induction pop; intros; cbn in *; auto. + - constructor. + destruct (PredIn_decidable _ pred (simplify pop1) peq); [intuition|]. + destruct (PredIn_decidable _ pred (simplify pop2) peq); [intuition|]. + repeat destruct_match; try solve [contradiction | inv H; inv H1; contradiction]. + - constructor. + destruct (PredIn_decidable _ pred (simplify pop1) peq); [intuition|]. + destruct (PredIn_decidable _ pred (simplify pop2) peq); [intuition|]. + repeat destruct_match; try solve [contradiction | inv H; inv H1; contradiction]. +Qed. +Opaque simplify. Lemma map_in_pred : forall A B (x: predicated A) f preds (g: A -> B), @@ -980,22 +998,32 @@ Proof. eapply map_in_pred4; auto. Qed. +Definition option_predicate_use (p: option pred_op) := + match p with + | Some p' => predicate_use p' + | None => nil + end. + #[local] Opaque seq_app. Lemma gather_predicates_RBop : forall p f pred op args dst p' f' preds preds', - update (p, f) (RBop (Some pred) op args dst) = Some (p', f') -> - gather_predicates preds (RBop (Some pred) op args dst) = Some preds' -> + update (p, f) (RBop pred op args dst) = Some (p', f') -> + gather_predicates preds (RBop pred op args dst) = Some preds' -> (forall in_pred, PredIn in_pred p -> preds ! in_pred = Some tt) -> all_preds_in f preds -> all_preds_in f' preds'. Proof. - intros. cbn in *. unfold Option.bind in *; repeat destr. inv H. + intros. cbn in *. unfold Option.bind in *; generalize dependent H; + repeat destr; intros H. inv H. inv H0. unfold all_preds_in in *; intros. apply NE.Forall_forall; intros. + assert (YX: (fold_right (fun x : positive => PTree.set x tt) preds (option_predicate_use pred)) = preds'). + { destruct pred. cbn. inv H3; auto. cbn. inv H3. auto. } subst. + clear H3. destruct (resource_eq (Reg dst) x). { subst. rewrite forest_reg_gss in H. eapply prune_predicated_in_pred in Heqo. - instantiate (1:=(fold_right (fun x : positive => PTree.set x tt) preds (predicate_use pred))) in Heqo. + instantiate (1:=(fold_right (fun x : positive => PTree.set x tt) preds (option_predicate_use pred))) in Heqo. unfold pe_preds_in in Heqo. eapply NE.Forall_forall in Heqo; eauto. eapply app_predicated_in_pred. eapply pe_preds_in_fold. @@ -1008,7 +1036,7 @@ Proof. eauto. intros. inv H3. inv H5. eapply gather_predicates_fold2; eauto. - apply pred_in_pred_uses; auto. + destruct pred; cbn in *. apply pred_in_pred_uses; auto. inv H3. eapply gather_predicates_fold; eauto. } rewrite forest_reg_gso in H by auto. @@ -1018,19 +1046,23 @@ Qed. Lemma gather_predicates_RBload : forall p f pred chunk addr args dst p' f' preds preds', - update (p, f) (RBload (Some pred) chunk addr args dst) = Some (p', f') -> - gather_predicates preds (RBload (Some pred) chunk addr args dst) = Some preds' -> + update (p, f) (RBload pred chunk addr args dst) = Some (p', f') -> + gather_predicates preds (RBload pred chunk addr args dst) = Some preds' -> (forall in_pred, PredIn in_pred p -> preds ! in_pred = Some tt) -> all_preds_in f preds -> all_preds_in f' preds'. Proof. - intros. cbn in *. unfold Option.bind in *; repeat destr. inv H. + intros. cbn in *. unfold Option.bind in *; generalize dependent H; + repeat destr; intros H. inv H. inv H0. unfold all_preds_in in *; intros. apply NE.Forall_forall; intros. + assert (YX: (fold_right (fun x : positive => PTree.set x tt) preds (option_predicate_use pred)) = preds'). + { destruct pred. cbn. inv H3; auto. cbn. inv H3. auto. } subst. + clear H3. destruct (resource_eq (Reg dst) x). { subst. rewrite forest_reg_gss in H. eapply prune_predicated_in_pred in Heqo. - instantiate (1:=(fold_right (fun x : positive => PTree.set x tt) preds (predicate_use pred))) in Heqo. + instantiate (1:=(fold_right (fun x : positive => PTree.set x tt) preds (option_predicate_use pred))) in Heqo. unfold pe_preds_in in Heqo. eapply NE.Forall_forall in Heqo; eauto. eapply app_predicated_in_pred. eapply pe_preds_in_fold. @@ -1047,7 +1079,7 @@ Proof. eapply gather_predicates_fold; eauto. intros. inv H3. inv H5. eapply gather_predicates_fold2; eauto. - apply pred_in_pred_uses; auto. + destruct pred; cbn in *; [apply pred_in_pred_uses; auto | inversion H3]. eapply gather_predicates_fold; eauto. } rewrite forest_reg_gso in H by auto. @@ -1057,19 +1089,23 @@ Qed. Lemma gather_predicates_RBstore : forall p f pred chunk addr args src p' f' preds preds', - update (p, f) (RBstore (Some pred) chunk addr args src) = Some (p', f') -> - gather_predicates preds (RBstore (Some pred) chunk addr args src) = Some preds' -> + update (p, f) (RBstore pred chunk addr args src) = Some (p', f') -> + gather_predicates preds (RBstore pred chunk addr args src) = Some preds' -> (forall in_pred, PredIn in_pred p -> preds ! in_pred = Some tt) -> all_preds_in f preds -> all_preds_in f' preds'. Proof. - intros. cbn in *. unfold Option.bind in *; repeat destr. inv H. + intros. cbn in *. unfold Option.bind in *; generalize dependent H; + repeat destr; intros H. inv H. inv H0. unfold all_preds_in in *; intros. apply NE.Forall_forall; intros. + assert (YX: (fold_right (fun x : positive => PTree.set x tt) preds (option_predicate_use pred)) = preds'). + { destruct pred. cbn. inv H3; auto. cbn. inv H3. auto. } subst. + clear H3. destruct (resource_eq Mem x). { subst. rewrite forest_reg_gss in H. eapply prune_predicated_in_pred in Heqo. - instantiate (1:=(fold_right (fun x : positive => PTree.set x tt) preds (predicate_use pred))) in Heqo. + instantiate (1:=(fold_right (fun x : positive => PTree.set x tt) preds (option_predicate_use pred))) in Heqo. unfold pe_preds_in in Heqo. eapply NE.Forall_forall in Heqo; eauto. eapply app_predicated_in_pred. eapply pe_preds_in_fold. @@ -1087,7 +1123,7 @@ Proof. eapply pe_preds_in_fold. eapply H2. intros. inv H3. inv H5. eapply gather_predicates_fold2; eauto. - apply pred_in_pred_uses; auto. + destruct pred; cbn in *; [apply pred_in_pred_uses; auto | inversion H3]. eapply gather_predicates_fold; eauto. } rewrite forest_reg_gso in H by auto. @@ -1097,15 +1133,16 @@ Qed. Lemma gather_predicates_RBsetpred : forall p f pred args cond pset p' f' preds preds', - update (p, f) (RBsetpred (Some pred) cond args pset) = Some (p', f') -> - gather_predicates preds (RBsetpred (Some pred) cond args pset) = Some preds' -> + update (p, f) (RBsetpred pred cond args pset) = Some (p', f') -> + gather_predicates preds (RBsetpred pred cond args pset) = Some preds' -> (forall in_pred, PredIn in_pred p -> preds ! in_pred = Some tt) -> all_preds_in f preds -> all_preds_in f' preds'. Proof. - intros. cbn in *. unfold Option.bind in *; repeat destr. inv H. - inv H0. unfold all_preds_in in *; intros. - rewrite forest_pred_reg. + intros. cbn in *. unfold Option.bind in *; generalize dependent H; + repeat destr; inversion 1; subst; clear H. + inv H0. unfold all_preds_in in *; intros. destruct pred; cbn in *; + rewrite forest_pred_reg; auto. eapply pe_preds_in_fold. eapply H2. Qed. @@ -1119,42 +1156,54 @@ Qed. Lemma gather_predicates_RBexit : forall p f pred cf p' f' preds preds', - update (p, f) (RBexit (Some pred) cf) = Some (p', f') -> - gather_predicates preds (RBexit (Some pred) cf) = Some preds' -> + update (p, f) (RBexit pred cf) = Some (p', f') -> + gather_predicates preds (RBexit pred cf) = Some preds' -> (forall in_pred, PredIn in_pred p -> preds ! in_pred = Some tt) -> all_preds_in f preds -> all_preds_in f' preds'. Proof. - intros. cbn in *. unfold Option.bind in *; repeat destr. inv H. - inv H0. unfold all_preds_in in *; intros. - rewrite forest_exit_regs. + intros. cbn in *. unfold Option.bind in *; generalize dependent H; + repeat destr; inversion 1; subst; clear H. + inv H0. unfold all_preds_in in *; intros. destruct pred; cbn in *. inv H3. + rewrite forest_exit_regs; auto. eapply pe_preds_in_fold. eapply H2. + inv H3. rewrite forest_exit_regs. auto. Qed. Transparent seq_app. Lemma gather_predicates_in_forest : forall p i f p' f' preds preds', + (forall in_pred, PredIn in_pred p -> preds ! in_pred = Some tt) -> update (p, f) i = Some (p', f') -> gather_predicates preds i = Some preds' -> all_preds_in f preds -> all_preds_in f' preds'. Proof. - intros. - destruct i; intros; cbn in *; - unfold Option.bind, Option.ret, Option.bind2 in *; - generalize H; repeat destr; inversion 1; subst; clear H. - - inv H0; auto. - - clear H2. destruct o. - + unfold all_preds_in in *; intros. - apply NE.Forall_forall; intros. - destruct (resource_eq (Reg r) x). - { subst. rewrite forest_reg_gss in H. - inv H0. } - rewrite forest_reg_gso in H by auto. inv H0. - eapply NE.Forall_forall in H1; eauto. - specialize (H1 _ H2). apply gather_predicates_fold; auto. - + inversion H0; subst; auto. + intros. destruct i. + - inv H0; inv H1; auto. + - eapply gather_predicates_RBop; eauto. + - eapply gather_predicates_RBload; eauto. + - eapply gather_predicates_RBstore; eauto. + - eapply gather_predicates_RBsetpred; eauto. + - eapply gather_predicates_RBexit; eauto. +Qed. + +Lemma gather_predicates_update_constant : + forall p f i p' f' preds preds', + (forall in_pred, PredIn in_pred p -> preds ! in_pred = Some tt) -> + gather_predicates preds i = Some preds' -> + update (p, f) i = Some (p', f') -> + (forall in_pred, PredIn in_pred p' -> preds' ! in_pred = Some tt). +Proof. + intros. destruct i; try solve [exploit gather_predicates_in; eauto; cbn in *; + unfold Option.bind in *; repeat destr; inv H0; inv H1; try (eapply H; eauto)]. + cbn in *; unfold Option.bind in *; repeat destr. inv H1. apply simplify_in in H2. + inv H2. inv H3. + - destruct o; cbn in *; [|inv H1]. inv H0. apply predin_negate2 in H1. + eapply gather_predicates_fold2. now apply pred_in_pred_uses. + - exploit gather_predicates_in; eauto. instantiate (1:=RBexit o c); auto. +Qed. Lemma sem_pexpr_eval_predin: forall G pr ps ps' (ctx: @Abstr.ctx G) b, @@ -1324,6 +1373,7 @@ Proof. split; intros; inv H; constructor; auto. Qed. (* [[id:5e6486bb-fda2-4558-aed8-243a9698de85]] *) Lemma abstr_seq_reverse_correct_fold : forall sp instrs i0 i i' ti cf f' l p p' l' f preds preds' lm lm' ps', + (forall in_pred, PredIn in_pred p -> preds ! in_pred = Some tt) -> valid_mem (is_mem i0) (is_mem i) -> all_preds_in f preds -> eval_predf (is_ps i) p = true -> @@ -1339,7 +1389,7 @@ Lemma abstr_seq_reverse_correct_fold : SeqBB.step ge sp (Iexec ti) instrs (Iterm ti' cf) /\ state_lessdef i' ti'. Proof. - induction instrs; intros * YVALID YALL YEVAL Y3 Y YGATHER Y0 YEVALUABLE YSEM_FINAL Y1 Y2. + induction instrs; intros * YPREDSIN YVALID YALL YEVAL Y3 Y YGATHER Y0 YEVALUABLE YSEM_FINAL Y1 Y2. - cbn in *. inv Y. assert (X: similar {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |}) @@ -1375,7 +1425,7 @@ Proof. 2: { symmetry. econstructor; try eassumption; auto. } inv YHSTEP. inv H1. exploit sem_update_instr. auto. eauto. eauto. eauto. eauto. auto. intros. - exploit IHinstrs. 4: { eauto. } + exploit IHinstrs. 5: { eauto. } eapply gather_predicates_update_constant; eauto. cbn in YVALID. transitivity m'; auto. replace m' with (is_mem {| is_rs := rs; Gible.is_ps := ps; Gible.is_mem := m' |}) by auto. eapply sem_update_valid_mem; eauto. @@ -1399,7 +1449,7 @@ Proof. 2: { symmetry. econstructor; try eassumption; auto. } inv YHSTEP. inv H1. exploit sem_update_instr. auto. eauto. eauto. eauto. eauto. auto. intros. - exploit IHinstrs. 4: { eauto. } + exploit IHinstrs. 5: { eauto. } eapply gather_predicates_update_constant; eauto. cbn in YVALID. transitivity m'; auto. replace m' with (is_mem {| is_rs := rs; Gible.is_ps := ps; Gible.is_mem := m' |}) by auto. eapply sem_update_valid_mem; eauto. @@ -1423,7 +1473,7 @@ Proof. 2: { symmetry. econstructor; try eassumption; auto. } inv YHSTEP. inv H1. exploit sem_update_instr. auto. eauto. eauto. eauto. eauto. auto. intros. - exploit IHinstrs. 4: { eauto. } + exploit IHinstrs. 5: { eauto. } eapply gather_predicates_update_constant; eauto. cbn in YVALID. transitivity m'; auto. replace m' with (is_mem {| is_rs := rs; Gible.is_ps := ps; Gible.is_mem := m' |}) by auto. eapply sem_update_valid_mem; eauto. @@ -1444,7 +1494,7 @@ Proof. 2: { symmetry. econstructor; try eassumption; auto. } inv YHSTEP. inv H1. exploit sem_update_instr. auto. eauto. eauto. eauto. eauto. auto. intros. - exploit IHinstrs. 4: { eauto. } + exploit IHinstrs. 5: { eauto. } eapply gather_predicates_update_constant; eauto. cbn in YVALID. transitivity m'; auto. replace m' with (is_mem {| is_rs := rs; Gible.is_ps := ps; Gible.is_mem := m' |}) by auto. eapply sem_update_valid_mem; eauto. @@ -1477,7 +1527,7 @@ Proof. 2: { symmetry. econstructor; try eassumption; auto. } inv YHSTEP. inv H2. exploit sem_update_instr. auto. eauto. eauto. eauto. eapply Heqo. eauto. auto. intros. - exploit IHinstrs. 4: { eauto. } + exploit IHinstrs. 5: { eauto. } eapply gather_predicates_update_constant; eauto. cbn in YVALID. transitivity m'; auto. replace m' with (is_mem {| is_rs := rs; Gible.is_ps := ps; Gible.is_mem := m' |}) by auto. cbn. inv H4. @@ -1525,6 +1575,7 @@ Proof. unfold Option.map, Option.bind in H. repeat destr. inv H. inv Heqo. eapply abstr_seq_reverse_correct_fold; try eassumption; try reflexivity; auto using sem_empty, all_preds_in_empty. + inversion 1. Qed. (*| |