Commit 7a8503ca authored by Robbert Krebbers's avatar Robbert Krebbers

Fix optimization.

parent 642acba9
......@@ -5,22 +5,24 @@ Section vcg.
Context `{heapG Σ}.
Inductive wp_expr :=
| Base : iProp Σ wp_expr
| Inhale : val (val wp_expr) wp_expr
| Exhale : val val wp_expr wp_expr
| IsSome : option val (val wp_expr) wp_expr.
| Base : iProp Σ wp_expr
| Inhale : loc (val wp_expr) wp_expr
| Exhale : loc val wp_expr wp_expr
| IsSome : option val (val wp_expr) wp_expr.
Arguments Base _%I.
Fixpoint wp_interp (a: wp_expr) : iProp Σ :=
Fixpoint wp_interp (a : wp_expr) : iProp Σ :=
match a with
| Base Φ => Φ
| Inhale w Φ => (l:loc) v, w = #l l v wp_interp (Φ v)
| Exhale w v Φ => (l:loc), w = #l (l v - wp_interp Φ)
| Inhale l Φ => v, l v wp_interp (Φ v)
| Exhale l v Φ => l v - wp_interp Φ
| IsSome mx Φ => v, mx = Some v wp_interp (Φ v)
end%I.
Class WpQuote (e : expr) (Φ : val wp_expr) (t : wp_expr) :=
wp_quote : wp_interp t WP e {{ v, wp_interp (Φ v) }}.
Class WpQuoteLoc (e : expr) (Φ : loc wp_expr) (t : wp_expr) :=
wp_quote_loc : wp_interp t WP e {{ v, l : loc, v = #l wp_interp (Φ l) }}.
Lemma tac_wp_quote Δ e Φ t :
WpQuote e (λ v, Base (Φ v)) t
......@@ -31,16 +33,20 @@ Section vcg.
Global Instance wp_quote_default e Φ :
WpQuote e Φ (Base (WP e {{ v, wp_interp (Φ v) }})) | 1000.
Proof. by rewrite /WpQuote. Qed.
Instance wp_quote_value e v Φ :
IntoVal e v WpQuote e Φ (Φ v).
Proof. rewrite /WpQuote. iIntros (<-%of_to_val) "H". by iApply wp_value. Qed.
Instance wp_quote_loc_loc l Φ :
WpQuoteLoc (Lit (LitLoc l)) Φ (Φ l).
Proof. rewrite /WpQuoteLoc. iIntros "H". iApply wp_value. eauto. Qed.
Global Instance wp_quote_load e Φ t :
WpQuote e (λ l, Inhale l (λ v, Exhale l v (Φ v))) t
WpQuoteLoc e (λ l, Inhale l (λ v, Exhale l v (Φ v))) t
WpQuote (Load e) Φ t.
Proof.
rewrite /WpQuote /= => ->. iIntros "H". wp_apply (wp_wand with "H").
iIntros (?); iDestruct 1 as (l v ->) "[Hl H]".
iDestruct "H" as (k [= ->]) "H /=". wp_load. by iApply "H".
rewrite /WpQuoteLoc /WpQuote /= => ->. iIntros "H". wp_apply (wp_wand with "H").
iIntros (?); iDestruct 1 as (l -> v) "[Hl H]". wp_load. by iApply "H".
Qed.
Global Instance wp_quote_bin_op op e1 e2 Φ Ψ t :
( v1, WpQuote e2 (λ v2, IsSome (bin_op_eval op v1 v2) Φ) (Ψ v1))
......@@ -54,45 +60,16 @@ Section vcg.
Qed.
Global Instance wp_quote_store e1 e2 Φ Ψ t :
( l, WpQuote e2 (λ v2, Inhale l (λ _, Exhale l v2 (Φ #()))) (Ψ l))
WpQuote e1 Ψ t
WpQuoteLoc e1 Ψ t
WpQuote (Store e1 e2) Φ t.
Proof.
rewrite /WpQuote /= => He2 ->. iIntros "H".
wp_apply (wp_wand with "H"); iIntros (v1) "H". rewrite He2.
wp_apply (wp_wand with "H"); iIntros (v2). iDestruct 1 as (l v ->) "[Hl H]".
iDestruct "H" as (?) "[% H]". simplify_eq/=.
wp_store. by iApply "H".
rewrite /WpQuoteLoc /WpQuote /= => He2 ->. iIntros "H".
wp_apply (wp_wand with "H"); iIntros (v1). iDestruct 1 as (l ->) "H".
rewrite He2. wp_apply (wp_wand with "H"); iIntros (v2).
iDestruct 1 as (v) "[Hl H]". wp_store. by iApply "H".
Qed.
Fixpoint vcg (e: expr) (Φ: val wp_expr) : wp_expr :=
match e with
| BinOp op e1 e2 =>
vcg e1 (λ v1, vcg e2 (λ v2, IsSome (bin_op_eval op v1 v2) Φ))
| Store e1 e2 =>
vcg e1 (λ l,
vcg e2 (λ v,
Inhale l (λ _, Exhale l v (Φ #()))))
| Load e1 =>
vcg e1 (λ l, Inhale l (λ v, Exhale l v (Φ v)))
| Lit (LitInt n) => Φ #n
| Lit (LitLoc l) => Φ #l
| _ => Base (WP e {{ v, wp_interp (Φ v)}})
end%I.
(*
Fixpoint optimize (Φ : wp_expr) : wp_expr :=
match Φ with
| Base Φ1 => Φ
| Inhale w Φ1 => Inhale w (λ v, optimize (Φ1 v))
| Exhale l1 w (Inhale l2 Φ1) =>
if bool_decide (l1 = l2) then optimize (Φ1 w)
else Exhale l1 w (Inhale l2 (λ v, optimize (Φ1 v)))
| Exhale w v Φ1 => Exhale w v (optimize Φ1)
| IsSome mx Φ1 => IsSome mx (λ v, optimize (Φ1 v))
end.
*)
Fixpoint optimize (s : option (val * val)) (Φ : wp_expr) : wp_expr :=
Fixpoint optimize (s : option (loc * val)) (Φ : wp_expr) : wp_expr :=
match Φ with
| Base Φ1 =>
match s with
......@@ -106,7 +83,11 @@ Section vcg.
if bool_decide (l = l') then optimize None (Φ1 w)
else Exhale l' w (Inhale l (λ v, optimize None (Φ1 v)))
end
| Exhale l w Φ => optimize (Some (l,w)) Φ
| Exhale l w Φ =>
match s with
| None => optimize (Some (l,w)) Φ
| Some (l',w') => Exhale l' w' (optimize (Some (l,w)) Φ)
end
| IsSome mx Φ1 => IsSome mx (λ v, optimize s (Φ1 v))
end.
......@@ -122,69 +103,36 @@ Section vcg.
(* rewrite /envs_entails. intros. by rewrite - (vcg_sound e Φ). *)
(* Qed. *)
Definition exhale_ (s : option (val * val)) (P : iProp Σ) : iProp Σ :=
Definition exhale_ (s : option (loc * val)) (P : iProp Σ) : iProp Σ :=
match s with
(* | Some (w, v) => (l ↦ v -∗ P)%I *)
| Some (LitV (LitLoc l), v) => (l v - P)%I
| Some _ => True%I
| Some (l, v) => l v - P
| None => P
end.
Definition isloc (s : option (val * val)) : iProp Σ :=
match s with
| Some (w, _) => ( (l : loc), w = #l)%I
| None => True%I
end.
end%I.
Lemma vcg_opt_sound' (s : option (val * val)) (t : wp_expr) :
wp_interp (optimize s t) - isloc s - exhale_ s (wp_interp t).
Lemma vcg_opt_sound' (s : option (loc * val)) (t : wp_expr) :
wp_interp (optimize s t) - exhale_ s (wp_interp t).
Proof.
generalize dependent s.
induction t; simpl.
- destruct s as [[w v]|]; simpl; eauto.
iDestruct 1 as (l) "[% H]". simplify_eq/=.
iIntros "_". done.
- destruct s as [[w' v']|]; simpl.
+ case_bool_decide; simplify_eq/=.
* iIntros "Hwv'".
rewrite H0 /=.
iDestruct 1 as (l) "%". simplify_eq/=.
iIntros "Hl". iExists _,_; iSplit; eauto; iFrame.
by iApply "Hwv'".
* iDestruct 1 as (?) "[% H]". simplify_eq/=.
iDestruct 1 as (l) "%". simplify_eq/=.
iIntros "Hl".
iDestruct ("H" with "Hl") as (l' ?) "[% [Hl' H]]".
iExists _,_; iSplit; eauto; iFrame.
rewrite H0. by iApply "H".
+ iDestruct 1 as (l ?) "[% [Hl H]]". simplify_eq/=.
iIntros "_". iExists l,_; iFrame. iSplit; eauto.
rewrite H0. by iApply "H".
- intros [[w' v']|]; simpl.
+ iIntros "H".
iDestruct 1 as (l) "%". simplify_eq/=.
iIntros "Hl".
rewrite IHt /=.
iDestruct ("H" with "[]").
iIntros "H"
(* + case_bool_decide; simplify_eq/=. *)
(* * destruct w'; eauto. *)
(* destruct l; eauto. *)
(* rewrite H0. simpl. *)
(* iIntros "Hwv' Hl". iExists _,_; iSplit; iFrame. done. *)
(* * iDestruct 1 as (l) "[% H]". *)
(* simplify_eq/=. *)
(* iIntros "Hl". iDestruct ("H" with "Hl") as (l' ?) "[% [Hl' H]]". *)
(* simplify_eq/=. *)
(* iExists l',_; iFrame. iSplit; eauto. by rewrite H0. *)
(* + iDestruct 1 as (l ?) "[% [Hl H]]". *)
(* simplify_eq/=. *)
(* iExists l,_; iFrame. iSplit; eauto. by rewrite H0. *)
rewrite H0 /=. eauto with iFrame.
* iIntros "H1 H2". setoid_rewrite H0. by iApply "H1".
+ iDestruct 1 as (v) "[Hl H]". iExists v. rewrite H0. iFrame.
- intros [[l' v']|]; simpl.
+ iIntros "H1 H2 H3". rewrite IHt. by iApply ("H1" with "[$]").
+ rewrite IHt /=. done.
- intros [[l' v']|]; simpl.
+ iDestruct 1 as (v ->) "H". iIntros "Hl". rewrite H0 /=.
iExists v; iSplit; first done. by iApply "H".
+ iDestruct 1 as (v ->) "H". rewrite H0 /=. iExists v. auto.
Qed.
Lemma vcg_opt_sound t :
wp_interp (optimize None t) - wp_interp t.
Proof. Admitted.
Proof. by rewrite vcg_opt_sound'. Qed.
Lemma tac_vcg_opt_sound Δ e Φ t :
WpQuote e (λ v, Base (Φ v)) t
......@@ -198,22 +146,11 @@ End vcg.
Hint Extern 50 (WpQuote _ _ _) =>
notypeclasses refine (wp_quote_value _ _ _ _) : typeclass_instances.
Hint Extern 50 (WpQuoteLoc _ _ _) =>
notypeclasses refine (wp_quote_loc_loc _ _) : typeclass_instances.
Declare Reduction vcg_cbv := cbv [ wp_interp vcg ].
Ltac vcg_cbv :=
match goal with
|- ?u => let v := eval vcg_cbv in u in change v
end.
(* Ltac wp_vcg := eapply tac_vcg_sound; vcg_cbv. *)
Declare Reduction vcg_opt_cbv := cbv [ wp_interp optimize vcg ].
Ltac vcg_opt_cbv :=
match goal with
|- ?u => let v := eval vcg_opt_cbv in u in change v
end.
Ltac wp_opt_vcg := eapply tac_vcg_opt_sound; vcg_opt_cbv;
repeat (case_bool_decide; simplify_eq).
Ltac vcg_opt :=
eapply tac_vcg_opt_sound; [apply _|].
Section Tests_vcg.
Context `{heapG Σ}.
......@@ -228,13 +165,11 @@ Section Tests_vcg.
(* (vcg (#l <- ! #l + #1) (λ _ : val, Base (l ↦ #(n + 1))))%I. *)
(* Eval simpl in vcg (#21 + #21) (λ v, Base (⌜ v = #42⌝)%I). *)
Lemma test1: WP #21 + #21 {{ v, v = #42 }}%I.
Proof.
iIntros.
(* --- PROOF BY VCG ---*)
eapply tac_vcg_opt_sound. apply _. simpl.
eauto.
vcg_opt. simpl. eauto.
(* --- PROOF BY WP --- *)
(* wp_op. *)
Qed.
......@@ -243,7 +178,8 @@ Section Tests_vcg.
l #21 - WP (!#l + #21) {{ v, l #21 v = #42}}.
Proof.
iIntros "H".
(* --- PROOF BY VCG --- *) eapply tac_vcg_opt_sound. apply _. simpl.
(* --- PROOF BY VCG --- *)
vcg_opt. simpl.
eauto 42 with iFrame.
(* --- PROOF BY WP --- *)
(* wp_load. wp_op. eauto. *)
......@@ -253,17 +189,18 @@ Section Tests_vcg.
l #n - WP (#l <- !#l + #1) {{ _, l #(n + 1) }}.
Proof.
iIntros "H".
(* --- PROOF BY VCG --- *)
(* --- PROOF BY VCG --- *)
vcg_opt. simpl. case_bool_decide=> //=.
(*PROOF BY WP *)
wp_load. wp_op. wp_store. done.
eauto 42 with iFrame.
Qed.
Lemma test4 (l: loc) (n: Z) :
l #n - WP (!#l + !#l) {{ v, v = #(n + n) l #n }}.
Proof.
iIntros "H".
(* --- PROOF BY VCG --- *) eapply tac_vcg_opt_sound. apply _. simpl.
case_bool_decide; simplify_eq/=.
(* --- PROOF BY VCG --- *)
vcg_opt. simpl. case_bool_decide=> //=.
eauto 17 with iFrame.
(* --- PROOF BY WP --- *)
(* wp_load. wp_load. wp_op. eauto. *)
......
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