Commit a5ff7225 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

WIP on optimize.

parent e5c2be44
......@@ -9,6 +9,7 @@ Section vcg.
| Inhale : val (val wp_expr) wp_expr
| Exhale : val val wp_expr wp_expr
| IsSome : option val (val wp_expr) wp_expr.
Arguments Base _%I.
Fixpoint wp_interp (a: wp_expr) : iProp Σ :=
match a with
......@@ -18,6 +19,40 @@ Section vcg.
| 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) }}.
Lemma tac_wp_quote Δ e Φ t :
WpQuote e (λ v, Base (Φ v)) t
envs_entails Δ (wp_interp t)
envs_entails Δ (WP e {{ Φ }}).
Proof. by rewrite /WpQuote /= envs_entails_eq=> ->. Qed.
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.
Global Instance wp_quote_load e Φ t :
WpQuote 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".
Qed.
Global Instance wp_quote_bin_op op e1 e2 Φ t t' :
( v1, WpQuote e2 (λ v2, IsSome (bin_op_eval op v1 v2) Φ) (t v1))
WpQuote e1 t t'
WpQuote (BinOp op 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 (v ?) "H".
by wp_op.
Qed.
Fixpoint vcg (e: expr) (Φ: val wp_expr) : wp_expr :=
match e with
| BinOp op e1 e2 =>
......@@ -33,6 +68,7 @@ Section vcg.
| _ => Base (WP e {{ v, wp_interp (Φ v)}})
end%I.
(*
Fixpoint optimize (Φ : wp_expr) : wp_expr :=
match Φ with
| Base Φ1 => Φ
......@@ -43,10 +79,30 @@ Section vcg.
| 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 :=
match Φ with
| Base Φ1 =>
match s with
| None => Base Φ1
| Some (l',w) => Exhale l' w (Base Φ1)
end
| Inhale l Φ1 =>
match s with
| None => Inhale l (λ v, optimize None (Φ1 v))
| Some (l',w) =>
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)) Φ
| IsSome mx Φ1 => IsSome mx (λ v, optimize s (Φ1 v))
end.
Lemma vcg_sound e Φ:
wp_interp (vcg e (λ v, Base (Φ v))) WP e {{v, Φ v}}.
wp_interp (vcg e (λ v, Base (Φ v))) WP e {{v, Φ v}}.
Proof.
Admitted.
Lemma tac_vcg_sound Δ e Φ :
......@@ -55,18 +111,22 @@ Section vcg.
Proof. rewrite /envs_entails. intros. by rewrite - (vcg_sound e Φ).
Qed.
Lemma vcg_opt_sound e Φ:
wp_interp (optimize (vcg e (λ v, Base (Φ v)))) WP e {{v, Φ v}}.
Admitted.
Lemma vcg_opt_sound t :
wp_interp (optimize None t) - wp_interp t.
Proof. Admitted.
Lemma tac_vcg_opt_sound Δ e Φ :
envs_entails Δ (wp_interp (optimize (vcg e (λ v, Base (Φ v)))))
Lemma tac_vcg_opt Δ e Φ t :
WpQuote e (λ v, Base (Φ v)) t
envs_entails Δ (wp_interp (optimize None t))
envs_entails Δ (WP e {{ Φ }}).
Proof. rewrite /envs_entails. intros. by rewrite -(vcg_opt_sound e Φ).
Proof.
rewrite /WpQuote /= envs_entails_eq=> Hquote ->.
by rewrite vcg_opt_sound.
Qed.
End vcg.
Hint Extern 50 (WpQuote _ _ _) =>
notypeclasses refine (wp_quote_value _ _ _ _) : typeclass_instances.
Declare Reduction vcg_cbv := cbv [ wp_interp vcg ].
Ltac vcg_cbv :=
......@@ -82,7 +142,7 @@ Ltac vcg_opt_cbv :=
|- ?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;
try case_bool_decide; simplify_eq.
repeat (case_bool_decide; simplify_eq).
Section Tests_vcg.
Context `{heapG Σ}.
......@@ -111,7 +171,7 @@ Section Tests_vcg.
l #21 - WP (!#l + #21) {{ v, l #21 v = #42}}.
Proof.
iIntros "H".
(* --- PROOF BY VCG --- *) wp_vcg.
(* --- PROOF BY VCG --- *) eapply tac_vcg_opt. apply _. simpl.
eauto 42 with iFrame.
(* --- PROOF BY WP --- *)
(* wp_load. wp_op. eauto. *)
......@@ -121,23 +181,23 @@ Section Tests_vcg.
l #n - WP (#l <- !#l + #1) {{ _, l #(n + 1) }}.
Proof.
iIntros "H".
(* --- PROOF BY VCG --- *) wp_vcg.
(* --- PROOF BY VCG --- *) (* wp_opt_vcg. admit.
eauto 17 with iFrame.
(*PROOF BY WP *)
(* wp_load. wp_op. wp_store. done. *)
Qed.
Qed. *) Admitted.
Lemma test4 (l: loc) (n: Z) :
l #n - WP (!#l + !#l) {{ v, v = #(n + n) l #n }}.
Proof.
iIntros "H".
(* --- PROOF BY VCG --- *) wp_opt_vcg.
(* --- PROOF BY VCG --- *) eapply tac_vcg_opt. apply _. simpl.
case_bool_decide; simplify_eq/=.
eauto 17 with iFrame.
(* --- PROOF BY WP --- *)
(* wp_load. wp_load. wp_op. eauto. *)
Qed.
Lemma test5 (l: loc) (n: Z) :
l #n - WP (!#l + !#l + !#l + !#l)
{{ v, v = #(n + n + n + n) l #n }}.
......@@ -154,13 +214,26 @@ Section Tests_vcg.
Proof.
iIntros "Hl1 Hl2".
(* --- PROOF BY VCG --- *) wp_opt_vcg.
- iCombine "Hl1" "Hl2" as "Habsurd". admit.
- by iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[].
- eauto 42 with iFrame.
iExists l1, #n. iSplit; first done.
iSplitL "Hl1"; first done.
eauto 15 with iFrame.
(* --- PROOF BY WP --- *)
(* do 2 wp_load. wp_op. eauto with iFrame. *)
Admitted.
Qed.
Lemma test7 (l1 l2: loc) (n m: Z) :
l1 #n - l2 #m - WP (!#l1 + !#l2 + !#l1) {{ v, v = #(n + m) l1 #n l2 #m }}.
Proof.
iIntros "Hl1 Hl2".
(* --- PROOF BY VCG --- *) wp_opt_vcg.
- by iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[].
- eauto 42 with iFrame.
iExists l1, #n. iSplit; first done.
iSplitL "Hl1"; first done.
eauto 15 with iFrame.
(* --- PROOF BY WP --- *)
(* do 2 wp_load. wp_op. eauto with iFrame. *)
Qed.
End Tests_vcg.
\ No newline at end of file
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