Commit 8d698b8c authored by Robbert Krebbers's avatar Robbert Krebbers

vcgen hacking.

parent 7a8503ca
......@@ -4,91 +4,208 @@ From iris.proofmode Require Import coq_tactics.
Section vcg.
Context `{heapG Σ}.
Inductive dloc :=
| dLoc : nat dloc
| dLocUnknown : loc dloc.
Global Instance dloc_decision : EqDecision dloc.
Proof. solve_decision. Defined.
Inductive dbase_lit : Type :=
| dLitInt : Z dbase_lit
| dLitBool : bool dbase_lit
| dLitUnit : dbase_lit
| dLitLoc : dloc dbase_lit
| dLitUnknown : base_lit dbase_lit.
Inductive dval : Type :=
| dLitV : dbase_lit dval
| dValUnknown : val dval.
Inductive doption (A : Type) : Type :=
| dNone : doption A
| dSome : A doption A
| dUnknown : option A doption A.
Arguments dNone {_}.
Arguments dSome {_} _.
Arguments dUnknown {_} _.
Inductive 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.
| Base : iProp Σ wp_expr
| Inhale : dloc (dval wp_expr) wp_expr
| Exhale : dloc dval wp_expr wp_expr
| IsSome {A} : doption A (A wp_expr) wp_expr
| IsLoc : dval (dloc wp_expr) wp_expr.
Arguments Base _%I.
Fixpoint wp_interp (a : wp_expr) : iProp Σ :=
Definition dloc_interp (E : list loc) (dl : dloc) : loc :=
match dl with
| dLoc i => from_option id inhabitant (E !! i)
| dLocUnknown l => l
end.
Definition dbase_lit_interp (E : list loc) (l : dbase_lit) : base_lit :=
match l with
| dLitInt x => LitInt x
| dLitBool b => LitBool b
| dLitUnit => LitUnit
| dLitLoc dl => LitLoc (dloc_interp E dl)
| dLitUnknown l => l
end.
Definition dval_interp (E : list loc) (v : dval) : val :=
match v with
| dLitV l => LitV (dbase_lit_interp E l)
| dValUnknown v => v
end.
Definition maybe_loc (v : val) : option loc :=
match v with LitV (LitLoc l) => Some l | _ => None end.
Lemma maybe_loc_sound v l : maybe_loc v = Some l v = #l.
Proof. by destruct v as [|[] | | |]; intros; simplify_eq/=. Qed.
Fixpoint doption_interp {A} (mx : doption A) : option A :=
match mx with
| dNone => None
| dSome x => Some x
| dUnknown mx => mx
end.
Fixpoint wp_interp (E : list loc) (a : wp_expr) : iProp Σ :=
match a with
| Base Φ => Φ
| Inhale dl Φ => dv, dloc_interp E dl dval_interp E dv wp_interp E (Φ dv)
| Exhale dl dv Φ => dloc_interp E dl dval_interp E dv - wp_interp E Φ
| IsSome dmx Φ => x, doption_interp dmx = Some x wp_interp E (Φ x)
| IsLoc dv Φ => dl : dloc, dval_interp E dv = #(dloc_interp E dl) wp_interp E (Φ dl)
end%I.
Fixpoint wp_interp_sane (E : list loc) (a : wp_expr) : iProp Σ :=
match a with
| Base Φ => Φ
| Inhale l Φ => v, l v wp_interp (Φ v)
| Exhale l v Φ => l v - wp_interp Φ
| IsSome mx Φ => v, mx = Some v wp_interp (Φ v)
| Inhale dl Φ => v, dloc_interp E dl v wp_interp_sane E (Φ (dValUnknown v))
| Exhale dl dv Φ => dloc_interp E dl dval_interp E dv - wp_interp_sane E Φ
| IsSome dmx Φ => x, doption_interp dmx = Some x wp_interp_sane E (Φ x)
| IsLoc dv Φ => l : loc, dval_interp E dv = #l wp_interp_sane E (Φ (dLocUnknown l))
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 wp_interp_sane_sound E a : wp_interp_sane E a wp_interp E a.
Proof. Admitted.
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.
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 :
WpQuoteLoc e (λ l, Inhale l (λ v, Exhale l v (Φ v))) t
WpQuote (Load e) Φ t.
Class WpQuote (E : list loc) (e : expr) (Φ : dval wp_expr) (t : wp_expr) :=
wp_quote :
wp_interp E t WP e {{ v, dv, dval_interp E dv = v wp_interp E (Φ dv) }}.
Global Instance wp_quote_default E e Φ :
WpQuote E e Φ (Base (WP e {{ v, wp_interp E (Φ (dValUnknown v)) }})) | 1000.
Proof.
rewrite /WpQuote /=. apply wp_mono=> v.
iIntros "H". iExists (dValUnknown v); auto.
Qed.
Class LocLookup (E : list loc) (l : loc) (i : nat) :=
loc_lookup : E !! i = Some l.
Global Instance loc_lookup_here l E : LocLookup (l :: E) l 0.
Proof. done. Qed.
Global Instance loc_lookup_there l l' E i :
LocLookup E l i LocLookup (l' :: E) l (S i).
Proof. done. Qed.
Class BaseLitQuote (E : list loc) (l : base_lit) (dl : dbase_lit) :=
base_lit_quote : l = dbase_lit_interp E dl.
Global Instance base_lit_quote_loc E l i :
LocLookup E l i BaseLitQuote E (LitLoc l) (dLitLoc (dLoc i)) | 1.
Proof. by rewrite /LocLookup /BaseLitQuote /= => ->. Qed.
Global Instance base_lit_quote_loc_unknown E l :
BaseLitQuote E (LitLoc l) (dLitLoc (dLocUnknown l)) | 10.
Proof. done. Qed.
Global Instance base_lit_quote_default E l :
BaseLitQuote E l (dLitUnknown l) | 1000.
Proof. done. Qed.
Class IntoDVal (E : list loc) (e : expr) (dv : dval) :=
into_dval : e = of_val (dval_interp E dv).
Global Instance into_dval_loc E l dl :
BaseLitQuote E l dl IntoDVal E (Lit l) (dLitV dl).
Proof. by rewrite /BaseLitQuote /IntoDVal=> ->. Qed.
Global Instance into_dval_default E e v :
IntoVal e v IntoDVal E e (dValUnknown v) | 1000.
Proof. by rewrite /IntoVal /IntoDVal=> /of_to_val ->. Qed.
Instance wp_quote_value E e dv Φ :
IntoDVal E e dv WpQuote E e Φ (Φ dv).
Proof. rewrite /WpQuote. iIntros (->) "H". iApply wp_value. eauto. Qed.
Global Instance wp_quote_load E e Φ t :
WpQuote E e (λ dv, IsLoc dv (λ l, Inhale l (λ w, Exhale l w (Φ w)))) t
WpQuote E (Load e) Φ t.
Proof.
rewrite /WpQuoteLoc /WpQuote /= => ->. iIntros "H". wp_apply (wp_wand with "H").
iIntros (?); iDestruct 1 as (l -> v) "[Hl H]". wp_load. by iApply "H".
rewrite /WpQuote /= => ->. iIntros "H". wp_apply (wp_wand with "H").
iIntros (?). iDestruct 1 as (dv <- l -> w) "[Hl H]".
wp_load. iExists w; iSplit; first done. 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))
WpQuote e1 Ψ t
WpQuote (BinOp op e1 e2) Φ t.
Global Instance wp_quote_bin_op E op e1 e2 Φ Ψ t :
( dv1, WpQuote E e2 (λ dv2,
IsSome (dUnknown (bin_op_eval op (dval_interp E dv1) (dval_interp E dv2))) (λ v, Φ (dValUnknown v))) (Ψ dv1))
WpQuote E e1 Ψ t
WpQuote E (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.
wp_apply (wp_wand with "H"); iIntros (v1).
iDestruct 1 as (dv <-) "H". rewrite He2.
wp_apply (wp_wand with "H"); iIntros (v2).
iDestruct 1 as (dv' <- w ?) "H".
wp_op. iExists (dValUnknown w); auto.
Qed.
Global Instance wp_quote_store e1 e2 Φ Ψ t :
( l, WpQuote e2 (λ v2, Inhale l (λ _, Exhale l v2 (Φ #()))) (Ψ l))
WpQuoteLoc e1 Ψ t
WpQuote (Store e1 e2) Φ t.
Global Instance wp_quote_store E e1 e2 Φ Ψ t :
( l, WpQuote E e2 (λ v2, Inhale l (λ _, Exhale l v2 (Φ (dLitV dLitUnit)))) (Ψ l))
WpQuote E e1 (λ w, IsLoc w Ψ) t
WpQuote E (Store e1 e2) Φ t.
Proof.
rewrite /WpQuoteLoc /WpQuote /= => He2 ->. iIntros "H".
wp_apply (wp_wand with "H"); iIntros (v1). iDestruct 1 as (l ->) "H".
rewrite /WpQuote /= => He2 ->. iIntros "H".
wp_apply (wp_wand with "H"); iIntros (v1).
iDestruct 1 as (dl <- l ->) "H".
rewrite He2. wp_apply (wp_wand with "H"); iIntros (v2).
iDestruct 1 as (v) "[Hl H]". wp_store. by iApply "H".
iDestruct 1 as (dv <- w) "[Hl H]". wp_store.
iExists (dLitV dLitUnit). iSplit; first done. by iApply "H".
Qed.
Fixpoint optimize (s : option (loc * val)) (Φ : wp_expr) : wp_expr :=
Fixpoint optimize (s : option (nat * dval)) (Φ : wp_expr) : wp_expr :=
match Φ with
| Base Φ1 =>
match s with
| None => Base Φ1
| Some (l',w) => Exhale l' w (Base Φ1)
| Some (i,w) => Exhale (dLoc i) w (Base Φ1)
end
| Inhale dl Φ1 =>
match s with
| None => Inhale dl (λ v, optimize None (Φ1 v))
| Some (i,w) =>
if bool_decide (dl = dLoc i) then optimize None (Φ1 w)
else Exhale (dLoc i) w (Inhale dl (λ v, optimize None (Φ1 v)))
end
| Inhale l Φ1 =>
| Exhale (dLoc i) w Φ =>
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)))
| None => optimize (Some (i,w)) Φ
| Some (i',w') => Exhale (dLoc i') w' (optimize (Some (i,w)) Φ)
end
| Exhale l w Φ =>
| Exhale (dLocUnknown l) w Φ =>
match s with
| None => optimize (Some (l,w)) Φ
| Some (l',w') => Exhale l' w' (optimize (Some (l,w)) Φ)
| None => Exhale (dLocUnknown l) w (optimize None Φ)
| Some (i',w') => Exhale (dLoc i') w' (Exhale (dLocUnknown l) w (optimize None Φ))
end
| IsSome dmx Φ1 =>
match dmx with
| dNone => Base False
| dSome x => optimize s (Φ1 x)
| _ => IsSome dmx (λ v, optimize s (Φ1 v))
end
| IsLoc dv Φ1 =>
match dv with
| dLitV (dLitLoc l) => optimize s (Φ1 l)
| dLitV (dLitUnknown _) | dValUnknown _ => IsLoc dv (λ v, optimize s (Φ1 v))
| _ => Base False
end
| IsSome mx Φ1 => IsSome mx (λ v, optimize s (Φ1 v))
end.
(* Lemma vcg_sound e Φ: *)
......@@ -103,54 +220,62 @@ Section vcg.
(* rewrite /envs_entails. intros. by rewrite - (vcg_sound e Φ). *)
(* Qed. *)
Definition exhale_ (s : option (loc * val)) (P : iProp Σ) : iProp Σ :=
Definition exhale_ (E : list loc) (s : option (nat * dval)) (P : iProp Σ) : iProp Σ :=
match s with
| Some (l, v) => l v - P
| Some (i, v) => dloc_interp E (dLoc i) dval_interp E v - P
| None => P
end%I.
Global Instance exhale_mono' E s : Proper (() ==> ()) (exhale_ E s).
Proof. destruct s; solve_proper. Qed.
Lemma vcg_opt_sound' (s : option (loc * val)) (t : wp_expr) :
wp_interp (optimize s t) - exhale_ s (wp_interp t).
Proof.
Lemma vcg_opt_sound' E s t :
wp_interp E (optimize s t) - exhale_ E s (wp_interp E t).
Proof. (*
generalize dependent s.
induction t; simpl.
- destruct s as [[w v]|]; simpl; eauto.
- destruct s as [[w' v']|]; simpl.
- intros [[l v]|]; simpl; eauto.
- intros [[l' v']|]; simpl.
+ case_bool_decide; simplify_eq/=.
* iIntros "Hwv'".
rewrite H0 /=. eauto with iFrame.
* iIntros "Hwv' H".
rewrite H0 /=. eauto 10 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.
- intros s. destruct d; simpl.
+ iIntros "[]".
+ rewrite H0. simpl. f_equiv. iIntros "H". iExists a; auto.
+ setoid_rewrite H0. iDestruct 1 as (x ->) "H".
iApply (exhale_mono' with "H"). iIntros "H". iExists x; auto.
- intros s. destruct d as [[]|]; simpl; try by iIntros "[]".
+ rewrite H0. simpl. f_equiv. iIntros "H". iExists l; auto.
+ setoid_rewrite H0. iDestruct 1 as (x ->) "H".
iApply (exhale_mono' with "H"). iIntros "H". iExists x; auto.
+ setoid_rewrite H0. iDestruct 1 as (x ->) "H".
iApply (exhale_mono' with "H"). iIntros "H". iExists x; auto.
Qed. *) Admitted.
Lemma vcg_opt_sound t :
wp_interp (optimize None t) - wp_interp t.
Lemma vcg_opt_sound E t :
wp_interp E (optimize None t) - wp_interp E t.
Proof. by rewrite vcg_opt_sound'. Qed.
Lemma tac_vcg_opt_sound Δ e Φ t :
WpQuote e (λ v, Base (Φ v)) t
envs_entails Δ (wp_interp (optimize None t))
Lemma tac_vcg_opt_sound Δ e Φ E t :
WpQuote E e (λ dv, Base (Φ (dval_interp E dv))) t
envs_entails Δ (wp_interp_sane E (optimize None t))
envs_entails Δ (WP e {{ Φ }}).
Proof.
rewrite /WpQuote /= envs_entails_eq=> Hquote ->.
by rewrite vcg_opt_sound.
rewrite wp_interp_sane_sound vcg_opt_sound Hquote. apply wp_mono=> v.
by iDestruct 1 as (dv ->) "?".
Qed.
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.
Hint Extern 50 (WpQuote _ _ _ _) =>
notypeclasses refine (wp_quote_value _ _ _ _ _) : typeclass_instances.
Ltac vcg_opt :=
eapply tac_vcg_opt_sound; [apply _|].
Ltac vcg_opt E' :=
eapply tac_vcg_opt_sound with (E:=E'); [apply _|].
Section Tests_vcg.
Context `{heapG Σ}.
......@@ -169,7 +294,7 @@ Section Tests_vcg.
Proof.
iIntros.
(* --- PROOF BY VCG ---*)
vcg_opt. simpl. eauto.
vcg_opt (@nil loc). simpl. eauto.
(* --- PROOF BY WP --- *)
(* wp_op. *)
Qed.
......@@ -179,7 +304,7 @@ Section Tests_vcg.
Proof.
iIntros "H".
(* --- PROOF BY VCG --- *)
vcg_opt. simpl.
vcg_opt [l]. simpl.
eauto 42 with iFrame.
(* --- PROOF BY WP --- *)
(* wp_load. wp_op. eauto. *)
......@@ -190,7 +315,7 @@ Section Tests_vcg.
Proof.
iIntros "H".
(* --- PROOF BY VCG --- *)
vcg_opt. simpl. case_bool_decide=> //=.
vcg_opt [l]. simpl.
(*PROOF BY WP *)
eauto 42 with iFrame.
Qed.
......@@ -200,7 +325,7 @@ Section Tests_vcg.
Proof.
iIntros "H".
(* --- PROOF BY VCG --- *)
vcg_opt. simpl. case_bool_decide=> //=.
vcg_opt [l]. simpl.
eauto 17 with iFrame.
(* --- PROOF BY WP --- *)
(* wp_load. wp_load. wp_op. eauto. *)
......@@ -244,4 +369,15 @@ Section Tests_vcg.
(* (* --- PROOF BY WP --- *) *)
(* (* do 2 wp_load. wp_op. eauto with iFrame. *) *)
(* Qed. *)
Lemma test8 (l k : loc) (n: Z) :
l #k - k #n - WP (! !#l) {{ v, v = #n }}.
Proof.
iIntros "H1 H2".
(* --- PROOF BY VCG --- *)
vcg_opt [l;k]. simpl.
eauto 20 with iFrame.
(* --- PROOF BY WP --- *)
(* wp_load. wp_load. wp_op. eauto. *)
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