Commit a10e080f authored by Léon Gondelman's avatar Léon Gondelman
Browse files

clean up in the vcgen (deleting lemmas about optimizer which is already gone)

parent 642186f8
......@@ -248,16 +248,8 @@ Section vcg_spec.
- simpl. intros E. by apply U_mono.
Qed.
(*
Lemma mapsto_star_list_spec E m t :
wp_interp E (mapsto_star_list m t) -∗ denv_interp E m ∗ wp_interp E t.
Proof.
Admitted.
(* unfold env_ps_dv_interp.
induction s as [| [i [[x q] w]] s']; simpl.
- by iIntros "$ _".
- iIntros "[H1 H2]". iFrame "H1". by iApply (IHs' with "H2").
Qed. *)
Lemma mapsto_wand_list_spec E m t :
wp_interp E (mapsto_wand_list m t) - denv_interp E m - wp_interp E t.
......@@ -275,8 +267,8 @@ Section vcg_spec.
denv_interp E m -
denv_interp E mIn
awp (dcexpr_interp E de) R (λ v, v = dval_interp E dv denv_interp E mOut).
Proof.
revert m mIn mOut dv. induction de;
Proof. Admitted.
(* revert m mIn mOut dv. induction de;
iIntros (m mIn mOut dv Hsp) "Hm"; simplify_eq/=.
- iFrame. iApply awp_ret. wp_value_head. iSplit; eauto. unfold denv_interp. done.
- specialize (IHde m).
......@@ -352,14 +344,14 @@ Section vcg_spec.
iIntros (v) "[-> HmOut2]".
iSplit; first done.
rewrite -denv_merge_interp. iFrame.
Qed.
Qed. *)
Lemma vcg_wp_correct R E m de Φ :
denv_interp E m -
wp_interp E (vcg_wp E m de R Φ) -
awp (dcexpr_interp E de) R
(λ v, ∃ dv m', ⌜dval_interp E dv = v⌝ ∧ wp_interp E (Φ m' dv)).
Proof. (*
(λ v, E' dv m', dval_interp E dv = v wp_interp E (Φ E' m' dv)).
Proof. Admitted. (*
revert Φ m. induction de; intros Φ m.
- iIntros "Hd". iApply awp_ret. wp_value_head. eauto.
- iIntros "Hawp". iApply (awp_wand with "Hawp"). iIntros (v) "H".
......@@ -490,90 +482,6 @@ Section vcg_spec.
rewrite wp_interp_sane_sound. iExists _,_; iFrame; eauto.
Qed.
*)
Admitted.
Lemma optimize_sound (m: denv) E (Φ: wp_expr) :
denv_interp E m -∗
wp_interp E (optimize m Φ) -∗
wp_interp E Φ.
Proof. (*
generalize dependent m.
induction Φ; simpl; intros m.
- rewrite mapsto_wand_list_spec /=; done.
- destruct d as [i|l]; iIntros "Hwp Hm".
+ remember (denv_delete_frac i m) as Hdl.
destruct Hdl as [[[m' q] dv]|]; last first.
{ simpl. iDestruct "Hwp" as (q dv) "H".
iExists q, dv. iDestruct "H" as "[Hl Hwp]". iFrame. rewrite H0. by iApply "Hwp". }
iExists q, dv.
rewrite -(denv_delete_frac_interp _ i m) //.
iDestruct "Hm" as "[Hm' Hdv]". rewrite H0. iSpecialize ("Hwp" with "Hm'"). iFrame.
+ simpl. iDestruct "Hwp" as (q dv) "[Hl Hdv]".
rewrite H0. iExists _,_; iFrame; by iApply "Hdv".
- destruct d as [i|l]; iIntros "Hwp Hm".
+ destruct (denv_delete_full i m) as [[m' dv]|] eqn:Hdl; last first.
{ simpl. iDestruct "Hwp" as (dv) "H".
iExists dv. iDestruct "H" as "[Hl Hwp]". iFrame. rewrite H0. by iApply "Hwp". }
iExists dv.
rewrite -(denv_delete_full_interp _ i m) //.
iDestruct "Hm" as "[Hm' Hdv]". rewrite H0. iSpecialize ("Hwp" with "Hm'"). iFrame.
+ simpl. iDestruct "Hwp" as (dv) "[Hl Hdv]".
rewrite H0. iExists _; iFrame; by iApply "Hdv".
- destruct d as [i|?].
+ case_bool_decide; simplify_eq/=. (* location found *)
* (* q = 1 *)
destruct (denv_delete_full i m) as [[m' dv]|] eqn:Hdl; last first.
{ simpl. iIntros "[Hl Hdv]".
rewrite IHΦ. iIntros "Hm". iFrame. by iApply "Hdv". }
case_bool_decide; simplify_eq/=; simpl; last first.
{ simpl. iIntros "[Hl Hdv]".
rewrite IHΦ. iIntros "Hm". iFrame. by iApply "Hdv". }
rewrite -(denv_delete_full_interp _ i m) //.
rewrite IHΦ. iIntros "Hdv".
iIntros "[Hm' Hi]". iFrame.
iSplitL "Hi"; last by iApply "Hdv".
by iApply mapsto_downgrade.
* (* q <> 1 *)
destruct (denv_delete_frac i m) as [[[m' q'] dv']|] eqn:Hdl; last first.
{ simpl. iIntros "[Hl Hdv]".
rewrite IHΦ. iIntros "Hm". iFrame. by iApply "Hdv". }
case_bool_decide; simplify_eq/=; last first.
{ simpl. iIntros "[Hl Hdv]".
rewrite IHΦ. iIntros "Hm". iFrame. by iApply "Hdv". }
case_bool_decide; simplify_eq/=; simpl; last first.
{ simpl. iIntros "[Hl Hdv]".
rewrite IHΦ. iIntros "Hm". iFrame. by iApply "Hdv". }
rewrite IHΦ. iIntros "Hdv'".
rewrite -(denv_delete_frac_interp _ i m) //.
iIntros "[Hm Hi]". iFrame.
iSplitL "Hi"; last by iApply "Hdv'".
by iApply mapsto_downgrade.
+ (* location wasn't found *)
simpl. iIntros "[Hl Hdv]".
rewrite IHΦ. iIntros "Hm". iFrame. by iApply "Hdv".
- destruct d as [i|?].
+ rewrite IHΦ. iIntros "HΦ Hm Hi".
rewrite denv_insert_interp. iApply "HΦ". iFrame.
+ simpl. iIntros "HΦ Hm Hl".
rewrite IHΦ. iApply ("HΦ" with "Hl Hm").
- destruct d; simpl.
+ iIntros "[]".
+ rewrite H0. f_equiv. iIntros "H"; iExists a; auto.
+ iIntros "H". iDestruct "H" as (dl) "[% H2]". simplify_eq.
rewrite H0. iIntros "H". iSpecialize ("H2" with "H"). eauto.
- destruct d; simpl; try by iIntros "[]".
+ destruct d; simpl; try by iIntros "[]".
* rewrite H0. f_equiv. iIntros "H". iExists d; auto.
* iIntros "H". iDestruct "H" as (dl) "[% H2]". simplify_eq.
rewrite H0. iIntros "H". iSpecialize ("H2" with "H"). eauto.
+ iIntros "H". iDestruct "H" as (dl) "[% H2]". simplify_eq.
rewrite H0. iIntros "H". iSpecialize ("H2" with "H"). eauto.
- iIntros "HΦ Hm".
rewrite IHΦ. iDestruct (denv_unlock_interp with "Hm") as "Hm".
iModIntro. by iApply "HΦ".
*)
Admitted.
*)
Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E dce :
MapstoListFromEnv Γs_in Γs_out Γls
......@@ -587,21 +495,6 @@ Section vcg_spec.
Proof.
Admitted.
(*
Lemma tac_vcg_opt_sound Γs_in Γs_out Γls Γp m c e R Φ E dce :
MapstoListFromEnv Γs_in Γs_out Γls →
E = penv_to_known_locs Γls →
ListOfMapsto Γls E m →
IntoDCexpr E e dce →
environments.envs_entails (environments.Envs Γp Γs_out c)
(wp_interp_sane E (optimize m (vcg_wp E m dce R (λ _ dv, Base (Φ (dval_interp E dv)))))) →
environments.envs_entails (environments.Envs Γp Γs_in c) (awp e R Φ).
Proof.
intros ???? Hgoal. eapply tac_vcg_sound; try eassumption.
revert Hgoal. rewrite environments.envs_entails_eq. intros ->.
rewrite wp_interp_sane_sound optimize_sound. done.
Qed.
*)
End vcg_spec.
Arguments wp_interp : simpl never.
......@@ -613,13 +506,3 @@ Ltac vcg_solver :=
| apply _ (* ListOfMapsto Γls E m *)
| apply _ (* IntoDCexpr E e dce *)
| simpl ].
(*
Ltac vcg_opt_solver :=
eapply tac_vcg_opt_sound;
[ apply _ (* MapstoListFromEnv Γs_in Γs_out Γls *)
| compute; reflexivity (* E = penv_to_known_locs Γls *)
| apply _ (* ListOfMapsto Γls E m *)
| apply _ (* IntoDCexpr E e dce *)
| simpl ].
*)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment