diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-12-01 22:30:29 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-12-01 22:30:29 +0000 |
commit | cb5e9fd36a3adaecd3dde461f6f2c7fe5e0e743a (patch) | |
tree | 31906785572d25f2cece5126fac2a1aa95aa1fe7 /src/hls/GiblePargenproof.v | |
parent | a8c196130327073d04efb04c1c23f3bc7ae5951b (diff) | |
download | vericert-cb5e9fd36a3adaecd3dde461f6f2c7fe5e0e743a.tar.gz vericert-cb5e9fd36a3adaecd3dde461f6f2c7fe5e0e743a.zip |
Add todo
Diffstat (limited to 'src/hls/GiblePargenproof.v')
-rw-r--r-- | src/hls/GiblePargenproof.v | 239 |
1 files changed, 163 insertions, 76 deletions
diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index e531fd3..28da296 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -994,10 +994,77 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. eapply sem_pred_expr_predicated_prod; eauto. Qed. + + Lemma evaluable_singleton : + forall A B ctx fp r, + @all_evaluable A B ctx fp (NE.singleton (T, r)). + Proof. + unfold all_evaluable, evaluable; intros. + inv H. simpl. exists true. constructor. + Qed. + +Lemma evaluable_negate : + forall G (ctx: @ctx G) p, + evaluable ctx p -> + evaluable ctx (¬ p). +Proof. + induction p; intros. + - destruct p. cbn in *. inv H. + exists (negb x). constructor. inv H0. + rewrite negb_if. now rewrite negb_involutive. + - repeat econstructor. + - repeat econstructor. + - cbn. exploit IHp1. inv H. inv H0. econstructor. eauto. + intros. exploit IHp2. inv H. inv H1. econstructor. eauto. + intros. inv H0. inv H1. econstructor. econstructor; eauto. + - cbn. exploit IHp1. inv H. inv H0. econstructor. eauto. + intros. exploit IHp2. inv H. inv H1. econstructor. eauto. + intros. inv H0. inv H1. econstructor. econstructor; eauto. +Qed. + +Lemma predicated_evaluable : + forall G (ctx: @ctx G) ps (p: pred_op), + pred_forest_evaluable ctx ps -> + evaluable ctx (from_pred_op ps p). +Proof. + unfold pred_forest_evaluable; intros. induction p; intros; cbn. + - repeat destruct_match; subst; unfold get_forest_p'. + destruct_match. eapply H; eauto. econstructor. constructor. constructor. + eapply evaluable_negate. + destruct_match. eapply H; eauto. econstructor. constructor. constructor. + - repeat econstructor. + - repeat econstructor. + - inv IHp1. inv IHp2. econstructor. constructor; eauto. + - inv IHp1. inv IHp2. econstructor. constructor; eauto. +Qed. + +Lemma predicated_evaluable_all : + forall A G (ctx: @ctx G) ps (p: predicated A), + pred_forest_evaluable ctx ps -> + all_evaluable ctx ps p. +Proof. + unfold all_evaluable; intros. + eapply predicated_evaluable. eauto. +Qed. + +Lemma predicated_evaluable_all_list : + forall A G (ctx: @ctx G) ps (p: list (predicated A)), + pred_forest_evaluable ctx ps -> + Forall (all_evaluable ctx ps) p. +Proof. + induction p. + - intros. constructor. + - intros. constructor; eauto. apply predicated_evaluable_all; auto. +Qed. + +Hint Resolve evaluable_singleton : core. +Hint Resolve predicated_evaluable : core. +Hint Resolve predicated_evaluable_all : core. +Hint Resolve predicated_evaluable_all_list : core. + Lemma sem_pred_expr_fold_right : forall A pr ctx s a a' s' - (ALLEVAL: all_evaluable ctx pr s) - (ALLEVAL2: Forall (all_evaluable ctx pr) (NE.to_list a)), + (PRED: pred_forest_evaluable ctx pr), sem_pred_expr pr sem_ident ctx s s' -> Forall2 (sem_pred_expr pr sem_ident ctx) (NE.to_list a) (of_elist a') -> @sem_pred_expr A _ _ pr sem_ident ctx (NE.fold_right cons_pred_expr s a) (Eapp a' s'). @@ -1005,9 +1072,8 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. induction a; crush. inv H0. inv H5. destruct a'; crush. destruct a'; crush. inv H3. eapply sem_pred_expr_cons_pred_expr; eauto. inv H0. destruct a'; crush. inv H3. - eapply sem_pred_expr_cons_pred_expr; eauto. admit. - eapply IHa; eauto. admit. - Admitted. + eapply sem_pred_expr_cons_pred_expr; eauto. + Qed. Lemma sem_pred_expr_fold_right2 : forall A pr ctx s a a' s', @@ -1104,22 +1170,15 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. rewrite Eapp_right_nil. auto. Qed. - Lemma evaluable_singleton : - forall A B ctx fp r, - @all_evaluable A B ctx fp (NE.singleton (T, r)). - Proof. - unfold all_evaluable, evaluable; intros. - inv H. simpl. exists true. constructor. - Qed. - Lemma sem_merge_list : - forall A ctx f rs ps m args, + forall A ctx f rs ps m args + (EVALF: forest_evaluable ctx f), sem ctx f ((mk_instr_state rs ps m), None) -> @sem_pred_expr A _ _ (forest_preds f) sem_val_list ctx (merge (list_translation args f)) (rs ## args). Proof. induction args; crush. cbn. constructor; constructor. - unfold merge. specialize (IHargs H). + unfold merge. specialize (IHargs EVALF H). eapply sem_pred_expr_ident2 in IHargs. inversion_clear IHargs as [l_ [HSEM HVAL]]. destruct_match; [|exfalso; eapply NEof_list_contra; eauto]. @@ -1145,13 +1204,12 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. intro REGI'; inversion_clear REGI' as [r' [SEMr SEMr']]. apply sem_pred_expr_ident with (l_ := Econs a' l_); [|constructor; auto]. replace (Econs a' l_) with (Eapp (Econs a' l_) Enil) by (now apply Eapp_right_nil). - apply sem_pred_expr_fold_right. apply evaluable_singleton. - admit. + apply sem_pred_expr_fold_right; eauto. repeat constructor. cbn. constructor; eauto. erewrite NEof_list_to_list; eauto. eapply sem_pred_expr_merge2; auto. - Admitted. + Qed. Lemma sem_pred_expr_list_translation : forall G ctx args f i, @@ -1312,10 +1370,10 @@ Lemma all_evaluable_predicated_prod : all_evaluable ctx ps (predicated_prod a b). Proof. intros. unfold all_evaluable; intros. - unfold predicated_prod in *. exploit all_evaluable_map_and; eauto. - intros. eapply all_evaluable_non_empty_prod. 3: { eauto. } - eauto. eauto. -Qed. + unfold predicated_prod in *. exploit all_evaluable_map_and. + 2: { eauto. } + intros. 2: { eauto. } +Admitted. (* Requires simple lemma to prove, but this lemma is not needed. *) Lemma cons_pred_expr_evaluable : forall G (ctx: @ctx G) ps a b, @@ -1339,50 +1397,6 @@ Proof. - inv H. specialize (IHn H3). now eapply cons_pred_expr_evaluable. Qed. -Lemma evaluable_negate : - forall G (ctx: @ctx G) p, - evaluable ctx p -> - evaluable ctx (¬ p). -Proof. - induction p; intros. - - destruct p. cbn in *. inv H. - exists (negb x). constructor. inv H0. - rewrite negb_if. now rewrite negb_involutive. - - repeat econstructor. - - repeat econstructor. - - cbn. exploit IHp1. inv H. inv H0. econstructor. eauto. - intros. exploit IHp2. inv H. inv H1. econstructor. eauto. - intros. inv H0. inv H1. econstructor. econstructor; eauto. - - cbn. exploit IHp1. inv H. inv H0. econstructor. eauto. - intros. exploit IHp2. inv H. inv H1. econstructor. eauto. - intros. inv H0. inv H1. econstructor. econstructor; eauto. -Qed. - -Lemma predicated_evaluable : - forall G (ctx: @ctx G) ps (p: pred_op), - pred_forest_evaluable ctx ps -> - evaluable ctx (from_pred_op ps p). -Proof. - unfold pred_forest_evaluable; intros. induction p; intros; cbn. - - repeat destruct_match; subst; unfold get_forest_p'. - destruct_match. eapply H; eauto. econstructor. constructor. constructor. - eapply evaluable_negate. - destruct_match. eapply H; eauto. econstructor. constructor. constructor. - - repeat econstructor. - - repeat econstructor. - - inv IHp1. inv IHp2. econstructor. constructor; eauto. - - inv IHp1. inv IHp2. econstructor. constructor; eauto. -Qed. - -Lemma predicated_evaluable_all : - forall A G (ctx: @ctx G) ps (p: predicated A), - pred_forest_evaluable ctx ps -> - all_evaluable ctx ps p. -Proof. - unfold all_evaluable; intros. - eapply predicated_evaluable. eauto. -Qed. - Lemma merge_all_evaluable : forall G (ctx: @ctx G) ps, pred_forest_evaluable ctx ps -> @@ -1432,9 +1446,7 @@ all be evaluable. exploit sem_pred_expr_ident2; [eapply HMEM|]. intros H; inversion_clear H as [x' [HS' HV']]. eapply sem_pred_expr_seq_app_val; eauto. - { eapply predicated_evaluable_all; eauto. } { eapply sem_pred_expr_seq_app; eauto. - - eapply predicated_evaluable_all; eauto. - eapply sem_pred_expr_merge; eauto. - apply sem_pred_expr_pred_ret. } @@ -1466,6 +1478,11 @@ all be evaluable. 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' -> @@ -1605,9 +1622,7 @@ all be evaluable. intros TMP; inversion_clear TMP as [x' [HS' HV']]. eapply sem_pred_expr_ident. eapply sem_pred_expr_seq_app; eauto. - eapply predicated_evaluable_all; eauto. eapply sem_pred_expr_seq_app; eauto. - eapply predicated_evaluable_all; eauto. eapply sem_pred_expr_pred_ret. econstructor; eauto. Qed. @@ -1731,7 +1746,7 @@ all be evaluable. eapply sem_pred_expr_ident2 in HRES. inversion_clear HRES as [r2 [HRES1 HRES2]]. apply exists_sem_pred in H. inversion_clear H as [r' [HNE HVAL]]. - exploit sem_merge_list. eauto. instantiate (2 := args). intro HSPE. eapply sem_pred_expr_ident2 in HSPE. + exploit sem_merge_list. eauto. eapply SEM2. instantiate (2 := args). intro HSPE. eapply sem_pred_expr_ident2 in HSPE. inversion_clear HSPE as [l_ [HSPE1 HSPE2]]. eapply sem_pred_expr_prune_predicated; eauto. eapply sem_pred_expr_app_predicated. @@ -1870,6 +1885,48 @@ all be evaluable. Admitted. (* This only needs the addition of the property that any setpreds will not contain the predicate in the name. *) + Lemma forest_evaluable_regset : + forall A f (ctx: @ctx A) n x, + forest_evaluable ctx f -> + forest_evaluable ctx f #r x <- n. + Proof. + unfold forest_evaluable, pred_forest_evaluable; intros. + eapply H. eauto. + Qed. + + Lemma eval_predf_update_evaluable : + forall A (ctx: @ctx A) curr_p next_p f f_next instr, + update (curr_p, f) instr = Some (next_p, f_next) -> + forest_evaluable ctx f -> + evaluable ctx (from_pred_op (forest_preds f) curr_p) -> + forest_evaluable ctx f_next. + Proof. + destruct instr; intros; cbn in *. + - inversion H; subst; auto. + - unfold Option.bind in *. destruct_match; try easy. + inversion_clear H. eapply forest_evaluable_regset; auto. + - unfold Option.bind in *. destruct_match; try easy. + inversion_clear H. eapply forest_evaluable_regset; auto. + - unfold Option.bind in *. destruct_match; try easy. + inversion_clear H. eapply forest_evaluable_regset; auto. + - unfold Option.bind in *. destruct_match; crush. + unfold forest_evaluable, pred_forest_evaluable. + intros. cbn in *. + destruct (peq i p); subst; [rewrite PTree.gss in H; inversion_clear H + | rewrite PTree.gso in H by auto; eapply H0; eassumption]. + (*TODO*) + - unfold Option.bind in *. destruct_match; try easy. + inversion_clear H. eapply forest_evaluable_regset; auto. + Admitted. + + Lemma sem_update_valid_mem : + forall i i' i'' curr_p next_p f f_next instr sp, + update (curr_p, f) instr = Some (next_p, f_next) -> + step_instr ge sp (Iexec i') instr (Iexec i'') -> + sem (mk_ctx i sp ge) f (i', None) -> + valid_mem (is_mem i') (is_mem i''). + Proof. Admitted. + Lemma eval_predf_lessdef : forall p a b, state_lessdef a b -> @@ -1886,8 +1943,27 @@ all be evaluable. now erewrite IHp2 by eassumption. Qed. + Lemma abstr_fold_evaluable : + forall A (ctx: @ctx A) x f f' curr_p p, + mfold_left update x (Some (curr_p, f)) = Some (p, f') -> + forest_evaluable ctx f -> + forest_evaluable ctx f'. + Proof. + induction x as [| x xs IHx ]. + - cbn in *; inversion 1; auto. + - intros. + replace (mfold_left update (x :: xs) (Some (curr_p, f)) = Some (p, f')) + with (mfold_left update xs (update (curr_p, f) x) = Some (p, f')) in H by auto. + exploit mfold_left_update_Some. eassumption. + inversion_clear 1 as [y SOME]. destruct y. rewrite SOME in H. + eapply IHx; [eassumption|]. + eauto using eval_predf_update_evaluable. + Qed. + Lemma abstr_fold_correct : - forall sp x i i' i'' cf f p f' curr_p, + forall sp x i i' i'' cf f p f' curr_p + (FEVAL: forest_evaluable (mk_ctx i sp ge) f) + (VALID: valid_mem (is_mem i) (is_mem i')), SeqBB.step ge sp (Iexec i') x (Iterm i'' cf) -> sem (mk_ctx i sp ge) f (i', None) -> eval_predf (is_ps i') curr_p = true -> @@ -1895,15 +1971,22 @@ all be evaluable. forall ti, state_lessdef i ti -> exists ti', sem (mk_ctx ti sp ge) f' (ti', Some cf) - /\ state_lessdef i'' ti'. + /\ state_lessdef i'' ti' + /\ forest_evaluable (mk_ctx i sp ge) f' + /\ valid_mem (is_mem i) (is_mem i''). Proof. induction x as [| x xs IHx ]; intros; cbn -[update] in *; inv H; cbn [fst snd] in *. - (* inductive case *) exploit mfold_left_update_Some; eauto; intros Hexists; inversion Hexists as [[curr_p_inter f_inter] EXEQ]; clear Hexists. exploit eval_predf_update_true; eauto; intros EVALTRUE. - rewrite EXEQ in H2. eapply IHx in H2; eauto; cbn [fst snd] in *. - eapply sem_update_instr; eauto. + rewrite EXEQ in H2. eapply IHx in H2; cbn [fst snd] in *. + eauto. + eapply eval_predf_update_evaluable; eauto. + transitivity (is_mem i'); auto. + eapply sem_update_valid_mem; eauto. + eauto. + eapply sem_update_instr; eauto. eauto. eauto. - (* terminal case *) exploit mfold_left_update_Some; eauto; intros Hexists; inversion Hexists as [[curr_p_inter f_inter] EXEQ]; clear Hexists. rewrite EXEQ in H2. @@ -1913,7 +1996,11 @@ all be evaluable. erewrite eval_predf_lessdef in H1 by eassumption. exploit sem_update_instr_term; eauto; intros [A B]. exists v2. split. inv Hi2. - eapply abstr_fold_falsy; try eassumption. auto. + eapply abstr_fold_falsy; try eassumption. + split; auto. + split. + + exploit IHx. + 6: { eauto. } Qed. Lemma sem_regset_empty : |