Commit 642acba9 authored by Dan Frumin's avatar Dan Frumin
Browse files

WIP: optimization correctness

parent 075f1b72
......@@ -110,23 +110,83 @@ Section vcg.
| 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}}.
Proof.
Admitted.
(* Lemma vcg_sound e Φ: *)
(* wp_interp (vcg e (λ v, Base (Φ v))) ⊢ WP e {{v, Φ v}}. *)
(* Proof. *)
(* Admitted. *)
Lemma tac_vcg_sound Δ e Φ :
envs_entails Δ (wp_interp (vcg e (λ v, Base (Φ v))))
envs_entails Δ (WP e {{ Φ }}).
Proof. rewrite /envs_entails. intros. by rewrite - (vcg_sound e Φ).
Qed.
(* Lemma tac_vcg_sound Δ e Φ : *)
(* envs_entails Δ (wp_interp (vcg e (λ v, Base (Φ v)))) → *)
(* envs_entails Δ (WP e {{ Φ }}). *)
(* Proof. *)
(* rewrite /envs_entails. intros. by rewrite - (vcg_sound e Φ). *)
(* Qed. *)
Definition exhale_ (s : option (val * 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
| None => P
end.
Definition isloc (s : option (val * val)) : iProp Σ :=
match s with
| Some (w, _) => ( (l : loc), w = #l)%I
| None => True%I
end.
Lemma vcg_opt_sound' (s : option (val * val)) (t : wp_expr) :
wp_interp (optimize s t) - isloc s - 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. *)
Lemma vcg_opt_sound t :
wp_interp (optimize None t) - wp_interp t.
Proof. Admitted.
Lemma tac_vcg_opt Δ e Φ t :
Lemma tac_vcg_opt_sound Δ e Φ t :
WpQuote e (λ v, Base (Φ v)) t
envs_entails Δ (wp_interp (optimize None t))
envs_entails Δ (WP e {{ Φ }}).
......@@ -144,7 +204,7 @@ 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.
(* Ltac wp_vcg := eapply tac_vcg_sound; vcg_cbv. *)
Declare Reduction vcg_opt_cbv := cbv [ wp_interp optimize vcg ].
......@@ -172,7 +232,8 @@ Section Tests_vcg.
Lemma test1: WP #21 + #21 {{ v, v = #42 }}%I.
Proof.
iIntros.
(* --- PROOF BY VCG ---*) wp_vcg.
(* --- PROOF BY VCG ---*)
eapply tac_vcg_opt_sound. apply _. simpl.
eauto.
(* --- PROOF BY WP --- *)
(* wp_op. *)
......@@ -182,7 +243,7 @@ Section Tests_vcg.
l #21 - WP (!#l + #21) {{ v, l #21 v = #42}}.
Proof.
iIntros "H".
(* --- PROOF BY VCG --- *) eapply tac_vcg_opt. apply _. simpl.
(* --- PROOF BY VCG --- *) eapply tac_vcg_opt_sound. apply _. simpl.
eauto 42 with iFrame.
(* --- PROOF BY WP --- *)
(* wp_load. wp_op. eauto. *)
......@@ -192,59 +253,58 @@ Section Tests_vcg.
l #n - WP (#l <- !#l + #1) {{ _, l #(n + 1) }}.
Proof.
iIntros "H".
(* --- PROOF BY VCG --- *) (* wp_opt_vcg. admit.
eauto 17 with iFrame.
(* --- PROOF BY VCG --- *)
(*PROOF BY WP *)
(* wp_load. wp_op. wp_store. done. *)
Qed. *) Admitted.
wp_load. wp_op. wp_store. done.
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. apply _. simpl.
case_bool_decide; simplify_eq/=.
(* --- PROOF BY VCG --- *) eapply tac_vcg_opt_sound. 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 }}.
Proof.
iIntros "H".
(* --- PROOF BY VCG --- *) wp_opt_vcg.
eauto 29 with iFrame.
(* --- PROOF BY WP --- *)
(* wp_load. do 4 (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 }}. *)
(* Proof. *)
(* iIntros "H". *)
(* (* --- PROOF BY VCG --- *) *)
(* (* eauto 29 with iFrame. *) *)
(* (* --- PROOF BY WP --- *) *)
(* wp_load. do 4 (wp_load; wp_op). eauto. *)
(* Qed. *)
Lemma test6 (l1 l2: loc) (n m: Z) :
l1 #n - l2 #m - WP (!#l1 + !#l2) {{ 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.
(* Lemma test6 (l1 l2: loc) (n m: Z) : *)
(* l1 ↦ #n -∗ l2 ↦ #m -∗ WP (!#l1 + !#l2) {{ 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. *)
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
(* 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.
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