Commit d68e6434 by Léon Gondelman

prove wp_interp_sane_sound and fix the proof of vcg_opt_sound'

parent 8d698b8c
 ... ... @@ -7,6 +7,7 @@ Section vcg. Inductive dloc := | dLoc : nat → dloc | dLocUnknown : loc → dloc. Global Instance dloc_decision : EqDecision dloc. Proof. solve_decision. Defined. ... ... @@ -25,6 +26,7 @@ Section vcg. | dNone : doption A | dSome : A → doption A | dUnknown : option A → doption A. Arguments dNone {_}. Arguments dSome {_} _. Arguments dUnknown {_} _. ... ... @@ -58,11 +60,6 @@ Section vcg. | 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 ... ... @@ -73,27 +70,46 @@ Section vcg. 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 Φ | 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) | 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 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)) | 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. Lemma wp_interp_sane_sound E a : wp_interp_sane E a ⊢ wp_interp E a. Proof. Admitted. Proof. generalize dependent E. induction a. - done. - simpl. iIntros (E) "He". iDestruct "He" as (v) "[H1 H2]". iExists (dValUnknown v). simpl. iFrame. by iApply H0. - simpl. iIntros (E) "He H". iApply IHa. by iApply "He". - simpl. iIntros (E) "He". iDestruct "He" as (v) "[H1 H2]". iExists v. iFrame. by iApply H0. - simpl. iIntros (E) "He". iDestruct "He" as (l) "[H1 H2]". iExists (dLocUnknown l). simpl. iFrame. by iApply H0. Qed. 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) }}. 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. ... ... @@ -104,29 +120,36 @@ Section vcg. 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. ... ... @@ -143,9 +166,11 @@ Section vcg. 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 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)) → 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. ... ... @@ -158,7 +183,8 @@ Section vcg. Qed. Global Instance wp_quote_store E e1 e2 Φ Ψ t : (∀ l, WpQuote E e2 (λ v2, Inhale l (λ _, Exhale l v2 (Φ (dLitV dLitUnit)))) (Ψ l)) → (∀ 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. ... ... @@ -192,7 +218,8 @@ Section vcg. | Exhale (dLocUnknown l) w Φ => match s with | None => Exhale (dLocUnknown l) w (optimize None Φ) | Some (i',w') => Exhale (dLoc i') w' (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 ... ... @@ -203,7 +230,8 @@ Section vcg. | IsLoc dv Φ1 => match dv with | dLitV (dLitLoc l) => optimize s (Φ1 l) | dLitV (dLitUnknown _) | dValUnknown _ => IsLoc dv (λ v, optimize s (Φ1 v)) | dLitV (dLitUnknown _) | dValUnknown _ => IsLoc dv (λ v, optimize s (Φ1 v)) | _ => Base False end end. ... ... @@ -220,17 +248,19 @@ Section vcg. (* rewrite /envs_entails. intros. by rewrite - (vcg_sound e Φ). *) (* Qed. *) Definition exhale_ (E : list loc) (s : option (nat * dval)) (P : iProp Σ) : iProp Σ := Definition exhale_ (E : list loc) (s : option (nat * dval)) (P : iProp Σ) : iProp Σ := match s with | 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' E s t : wp_interp E (optimize s t) -∗ exhale_ E s (wp_interp E t). Proof. (* Proof. generalize dependent s. induction t; simpl. - intros [[l v]|]; simpl; eauto. ... ... @@ -241,20 +271,25 @@ Section vcg. * 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. + iIntros "H1 H2 H3". destruct d; simpl; rewrite IHt; by iApply ("H1" with "[\$]"). + iIntros "H1 H2". destruct d; simpl; rewrite IHt; by iApply ("H1" with "[\$]"). - 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. - intros s. 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. iApply (exhale_mono' with "H2"). iIntros "H". iExists dl; auto. + iIntros "H". iDestruct "H" as (dl) "[% H2]". simplify_eq. rewrite H0. iApply (exhale_mono' with "H2"). iIntros "H". iExists dl; auto. Qed. Lemma vcg_opt_sound E t : wp_interp E (optimize None t) -∗ wp_interp E t. ... ... @@ -280,16 +315,6 @@ Ltac vcg_opt E' := Section Tests_vcg. Context `{heapG Σ}. (* Variable (l k: loc) (n: Z) (Φ: val → iProp Σ). *) (* Eval simpl in vcg (!#l + !#k) (λ v : val, Base (Φ v))%I. *) (* Eval simpl in optimize (vcg (!#l + !#l) (λ v : val, Base (Φ v)))%I. *) (* Eval simpl in wp_interp (vcg (!#l + !#l) (λ v : val, Base (Φ v))%I). *) (* Eval simpl in *) (* (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. ... ... @@ -315,9 +340,8 @@ Section Tests_vcg. Proof. iIntros "H". (* --- PROOF BY VCG --- *) vcg_opt [l]. simpl. vcg_opt [l]. simpl. eauto 42 with iFrame. (*PROOF BY WP *) eauto 42 with iFrame. Qed. Lemma test4 (l: loc) (n: Z) : ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!