Commit 86bacab9 by Ralf Jung

change wp notation

parent d535d95f
 ... ... @@ -15,7 +15,7 @@ Section client. Local Notation iProp := (iPropG heap_lang Σ). Definition y_inv q y : iProp := (∃ f : val, y ↦{q} f ★ □ ∀ n : Z, || f #n {{ λ v, v = #(n + 42) }})%I. (∃ f : val, y ↦{q} f ★ □ ∀ n : Z, #> f #n {{ λ v, v = #(n + 42) }})%I. Lemma y_inv_split q y : y_inv q y ⊑ (y_inv (q/2) y ★ y_inv (q/2) y). ... ... @@ -27,7 +27,7 @@ Section client. Lemma worker_safe q (n : Z) (b y : loc) : (heap_ctx heapN ★ recv heapN N b (y_inv q y)) ⊑ || worker n (%b) (%y) {{ λ _, True }}. ⊑ #> worker n (%b) (%y) {{ λ _, True }}. Proof. rewrite /worker. wp_lam. wp_let. ewp apply wait_spec. rewrite comm. apply sep_mono_r. apply wand_intro_l. ... ... @@ -41,7 +41,7 @@ Section client. Qed. Lemma client_safe : heapN ⊥ N → heap_ctx heapN ⊑ || client {{ λ _, True }}. heapN ⊥ N → heap_ctx heapN ⊑ #> client {{ λ _, True }}. Proof. intros ?. rewrite /client. (ewp eapply wp_alloc); eauto with I. strip_later. apply forall_intro=>y. ... ... @@ -51,7 +51,7 @@ Section client. apply sep_mono_r. apply forall_intro=>b. apply wand_intro_l. wp_let. ewp eapply wp_fork. rewrite [heap_ctx _]always_sep_dup !assoc [(_ ★ heap_ctx _)%I]comm. rewrite [(|| _ {{ _ }} ★ _)%I]comm -!assoc assoc. apply sep_mono;last first. rewrite [(#> _ {{ _ }} ★ _)%I]comm -!assoc assoc. apply sep_mono;last first. { (* The original thread, the sender. *) wp_seq. (ewp eapply wp_store); eauto with I. strip_later. rewrite assoc [(_ ★ y ↦ _)%I]comm. apply sep_mono_r, wand_intro_l. ... ...
 ... ... @@ -126,7 +126,7 @@ Qed. Lemma newbarrier_spec (P : iProp) (Φ : val → iProp) : heapN ⊥ N → (heap_ctx heapN ★ ∀ l, recv l P ★ send l P -★ Φ (%l)) ⊑ || newbarrier #() {{ Φ }}. ⊑ #> newbarrier #() {{ Φ }}. Proof. intros HN. rewrite /newbarrier. wp_seq. rewrite -wp_pvs. wp eapply wp_alloc; eauto with I ndisj. ... ... @@ -172,7 +172,7 @@ Proof. Qed. Lemma signal_spec l P (Φ : val → iProp) : (send l P ★ P ★ Φ #()) ⊑ || signal (%l) {{ Φ }}. (send l P ★ P ★ Φ #()) ⊑ #> signal (%l) {{ Φ }}. Proof. rewrite /signal /send /barrier_ctx. rewrite sep_exist_r. apply exist_elim=>γ. rewrite -!assoc. apply const_elim_sep_l=>?. wp_let. ... ... @@ -199,7 +199,7 @@ Proof. Qed. Lemma wait_spec l P (Φ : val → iProp) : (recv l P ★ (P -★ Φ #())) ⊑ || wait (%l) {{ Φ }}. (recv l P ★ (P -★ Φ #())) ⊑ #> wait (%l) {{ Φ }}. Proof. rename P into R. wp_rec. rewrite {1}/recv /barrier_ctx. rewrite !sep_exist_r. ... ...
 ... ... @@ -19,36 +19,36 @@ Implicit Types Φ : val → iProp heap_lang Σ. (** Proof rules for the sugar *) Lemma wp_lam E x ef e v Φ : to_val e = Some v → ▷ || subst' x e ef @ E {{ Φ }} ⊑ || App (Lam x ef) e @ E {{ Φ }}. ▷ #> subst' x e ef @ E {{ Φ }} ⊑ #> App (Lam x ef) e @ E {{ Φ }}. Proof. intros. by rewrite -wp_rec. Qed. Lemma wp_let E x e1 e2 v Φ : to_val e1 = Some v → ▷ || subst' x e1 e2 @ E {{ Φ }} ⊑ || Let x e1 e2 @ E {{ Φ }}. ▷ #> subst' x e1 e2 @ E {{ Φ }} ⊑ #> Let x e1 e2 @ E {{ Φ }}. Proof. apply wp_lam. Qed. Lemma wp_seq E e1 e2 v Φ : to_val e1 = Some v → ▷ || e2 @ E {{ Φ }} ⊑ || Seq e1 e2 @ E {{ Φ }}. ▷ #> e2 @ E {{ Φ }} ⊑ #> Seq e1 e2 @ E {{ Φ }}. Proof. intros ?. by rewrite -wp_let. Qed. Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊑ || Skip @ E {{ Φ }}. Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊑ #> Skip @ E {{ Φ }}. Proof. rewrite -wp_seq // -wp_value //. Qed. Lemma wp_match_inl E e0 v0 x1 e1 x2 e2 Φ : to_val e0 = Some v0 → ▷ || subst' x1 e0 e1 @ E {{ Φ }} ⊑ || Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}. ▷ #> subst' x1 e0 e1 @ E {{ Φ }} ⊑ #> Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}. Proof. intros. by rewrite -wp_case_inl // -[X in _ ⊑ X]later_intro -wp_let. Qed. Lemma wp_match_inr E e0 v0 x1 e1 x2 e2 Φ : to_val e0 = Some v0 → ▷ || subst' x2 e0 e2 @ E {{ Φ }} ⊑ || Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}. ▷ #> subst' x2 e0 e2 @ E {{ Φ }} ⊑ #> Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}. Proof. intros. by rewrite -wp_case_inr // -[X in _ ⊑ X]later_intro -wp_let. Qed. Lemma wp_le E (n1 n2 : Z) P Φ : (n1 ≤ n2 → P ⊑ ▷ Φ (LitV (LitBool true))) → (n2 < n1 → P ⊑ ▷ Φ (LitV (LitBool false))) → P ⊑ || BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}. P ⊑ #> BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}. Proof. intros. rewrite -wp_bin_op //; []. destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega. ... ... @@ -57,7 +57,7 @@ Qed. Lemma wp_lt E (n1 n2 : Z) P Φ : (n1 < n2 → P ⊑ ▷ Φ (LitV (LitBool true))) → (n2 ≤ n1 → P ⊑ ▷ Φ (LitV (LitBool false))) → P ⊑ || BinOp LtOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}. P ⊑ #> BinOp LtOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}. Proof. intros. rewrite -wp_bin_op //; []. destruct (bool_decide_reflect (n1 < n2)); by eauto with omega. ... ... @@ -66,7 +66,7 @@ Qed. Lemma wp_eq E (n1 n2 : Z) P Φ : (n1 = n2 → P ⊑ ▷ Φ (LitV (LitBool true))) → (n1 ≠ n2 → P ⊑ ▷ Φ (LitV (LitBool false))) → P ⊑ || BinOp EqOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}. P ⊑ #> BinOp EqOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}. Proof. intros. rewrite -wp_bin_op //; []. destruct (bool_decide_reflect (n1 = n2)); by eauto with omega. ... ...
 ... ... @@ -141,7 +141,7 @@ Section heap. to_val e = Some v → P ⊑ heap_ctx N → nclose N ⊆ E → P ⊑ (▷ ∀ l, l ↦ v -★ Φ (LocV l)) → P ⊑ || Alloc e @ E {{ Φ }}. P ⊑ #> Alloc e @ E {{ Φ }}. Proof. rewrite /heap_ctx /heap_inv=> ??? HP. trans (|={E}=> auth_own heap_name ∅ ★ P)%I. ... ... @@ -166,7 +166,7 @@ Section heap. Lemma wp_load N E l q v P Φ : P ⊑ heap_ctx N → nclose N ⊆ E → P ⊑ (▷ l ↦{q} v ★ ▷ (l ↦{q} v -★ Φ v)) → P ⊑ || Load (Loc l) @ E {{ Φ }}. P ⊑ #> Load (Loc l) @ E {{ Φ }}. Proof. rewrite /heap_ctx /heap_inv=> ?? HPΦ. apply (auth_fsa' heap_inv (wp_fsa _) id) ... ... @@ -183,7 +183,7 @@ Section heap. to_val e = Some v → P ⊑ heap_ctx N → nclose N ⊆ E → P ⊑ (▷ l ↦ v' ★ ▷ (l ↦ v -★ Φ (LitV LitUnit))) → P ⊑ || Store (Loc l) e @ E {{ Φ }}. P ⊑ #> Store (Loc l) e @ E {{ Φ }}. Proof. rewrite /heap_ctx /heap_inv=> ??? HPΦ. apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v)) l)) ... ... @@ -200,7 +200,7 @@ Section heap. to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 → P ⊑ heap_ctx N → nclose N ⊆ E → P ⊑ (▷ l ↦{q} v' ★ ▷ (l ↦{q} v' -★ Φ (LitV (LitBool false)))) → P ⊑ || Cas (Loc l) e1 e2 @ E {{ Φ }}. P ⊑ #> Cas (Loc l) e1 e2 @ E {{ Φ }}. Proof. rewrite /heap_ctx /heap_inv=>????? HPΦ. apply (auth_fsa' heap_inv (wp_fsa _) id) ... ... @@ -217,7 +217,7 @@ Section heap. to_val e1 = Some v1 → to_val e2 = Some v2 → P ⊑ heap_ctx N → nclose N ⊆ E → P ⊑ (▷ l ↦ v1 ★ ▷ (l ↦ v2 -★ Φ (LitV (LitBool true)))) → P ⊑ || Cas (Loc l) e1 e2 @ E {{ Φ }}. P ⊑ #> Cas (Loc l) e1 e2 @ E {{ Φ }}. Proof. rewrite /heap_ctx /heap_inv=> ???? HPΦ. apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v2)) l)) ... ...
 ... ... @@ -16,14 +16,14 @@ Implicit Types ef : option (expr []). (** Bind. *) Lemma wp_bind {E e} K Φ : || e @ E {{ λ v, || fill K (of_val v) @ E {{ Φ }}}} ⊑ || fill K e @ E {{ Φ }}. #> e @ E {{ λ v, #> fill K (of_val v) @ E {{ Φ }}}} ⊑ #> fill K e @ E {{ Φ }}. Proof. apply weakestpre.wp_bind. Qed. (** Base axioms for core primitives of the language: Stateful reductions. *) Lemma wp_alloc_pst E σ e v Φ : to_val e = Some v → (▷ ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) -★ Φ (LocV l))) ⊑ || Alloc e @ E {{ Φ }}. ⊑ #> Alloc e @ E {{ Φ }}. Proof. (* TODO RJ: This works around ssreflect bug #22. *) intros. set (φ v' σ' ef := ∃ l, ... ... @@ -40,7 +40,7 @@ Qed. Lemma wp_load_pst E σ l v Φ : σ !! l = Some v → (▷ ownP σ ★ ▷ (ownP σ -★ Φ v)) ⊑ || Load (Loc l) @ E {{ Φ }}. (▷ ownP σ ★ ▷ (ownP σ -★ Φ v)) ⊑ #> Load (Loc l) @ E {{ Φ }}. Proof. intros. rewrite -(wp_lift_atomic_det_step σ v σ None) ?right_id //; last by intros; inv_step; eauto using to_of_val. ... ... @@ -49,7 +49,7 @@ Qed. Lemma wp_store_pst E σ l e v v' Φ : to_val e = Some v → σ !! l = Some v' → (▷ ownP σ ★ ▷ (ownP (<[l:=v]>σ) -★ Φ (LitV LitUnit))) ⊑ || Store (Loc l) e @ E {{ Φ }}. ⊑ #> Store (Loc l) e @ E {{ Φ }}. Proof. intros. rewrite -(wp_lift_atomic_det_step σ (LitV LitUnit) (<[l:=v]>σ) None) ?right_id //; last by intros; inv_step; eauto. ... ... @@ -58,7 +58,7 @@ Qed. Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ : to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v' → v' ≠ v1 → (▷ ownP σ ★ ▷ (ownP σ -★ Φ (LitV \$ LitBool false))) ⊑ || Cas (Loc l) e1 e2 @ E {{ Φ }}. ⊑ #> Cas (Loc l) e1 e2 @ E {{ Φ }}. Proof. intros. rewrite -(wp_lift_atomic_det_step σ (LitV \$ LitBool false) σ None) ?right_id //; last by intros; inv_step; eauto. ... ... @@ -67,7 +67,7 @@ Qed. Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ : to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v1 → (▷ ownP σ ★ ▷ (ownP (<[l:=v2]>σ) -★ Φ (LitV \$ LitBool true))) ⊑ || Cas (Loc l) e1 e2 @ E {{ Φ }}. ⊑ #> Cas (Loc l) e1 e2 @ E {{ Φ }}. Proof. intros. rewrite -(wp_lift_atomic_det_step σ (LitV \$ LitBool true) (<[l:=v2]>σ) None) ?right_id //; last by intros; inv_step; eauto. ... ... @@ -75,7 +75,7 @@ Qed. (** Base axioms for core primitives of the language: Stateless reductions *) Lemma wp_fork E e Φ : (▷ Φ (LitV LitUnit) ★ ▷ || e {{ λ _, True }}) ⊑ || Fork e @ E {{ Φ }}. (▷ Φ (LitV LitUnit) ★ ▷ #> e {{ λ _, True }}) ⊑ #> Fork e @ E {{ Φ }}. Proof. rewrite -(wp_lift_pure_det_step (Fork e) (Lit LitUnit) (Some e)) //=; last by intros; inv_step; eauto. ... ... @@ -84,8 +84,8 @@ Qed. Lemma wp_rec E f x e1 e2 v Φ : to_val e2 = Some v → ▷ || subst' x e2 (subst' f (Rec f x e1) e1) @ E {{ Φ }} ⊑ || App (Rec f x e1) e2 @ E {{ Φ }}. ▷ #> subst' x e2 (subst' f (Rec f x e1) e1) @ E {{ Φ }} ⊑ #> App (Rec f x e1) e2 @ E {{ Φ }}. Proof. intros. rewrite -(wp_lift_pure_det_step (App _ _) (subst' x e2 (subst' f (Rec f x e1) e1)) None) //= ?right_id; ... ... @@ -95,13 +95,13 @@ Qed. Lemma wp_rec' E f x erec e1 e2 v2 Φ : e1 = Rec f x erec → to_val e2 = Some v2 → ▷ || subst' x e2 (subst' f e1 erec) @ E {{ Φ }} ⊑ || App e1 e2 @ E {{ Φ }}. ▷ #> subst' x e2 (subst' f e1 erec) @ E {{ Φ }} ⊑ #> App e1 e2 @ E {{ Φ }}. Proof. intros ->. apply wp_rec. Qed. Lemma wp_un_op E op l l' Φ : un_op_eval op l = Some l' → ▷ Φ (LitV l') ⊑ || UnOp op (Lit l) @ E {{ Φ }}. ▷ Φ (LitV l') ⊑ #> UnOp op (Lit l) @ E {{ Φ }}. Proof. intros. rewrite -(wp_lift_pure_det_step (UnOp op _) (Lit l') None) ?right_id -?wp_value //; intros; inv_step; eauto. ... ... @@ -109,21 +109,21 @@ Qed. Lemma wp_bin_op E op l1 l2 l' Φ : bin_op_eval op l1 l2 = Some l' → ▷ Φ (LitV l') ⊑ || BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}. ▷ Φ (LitV l') ⊑ #> BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}. Proof. intros Heval. rewrite -(wp_lift_pure_det_step (BinOp op _ _) (Lit l') None) ?right_id -?wp_value //; intros; inv_step; eauto. Qed. Lemma wp_if_true E e1 e2 Φ : ▷ || e1 @ E {{ Φ }} ⊑ || If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}. ▷ #> e1 @ E {{ Φ }} ⊑ #> If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}. Proof. rewrite -(wp_lift_pure_det_step (If _ _ _) e1 None) ?right_id //; intros; inv_step; eauto. Qed. Lemma wp_if_false E e1 e2 Φ : ▷ || e2 @ E {{ Φ }} ⊑ || If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}. ▷ #> e2 @ E {{ Φ }} ⊑ #> If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}. Proof. rewrite -(wp_lift_pure_det_step (If _ _ _) e2 None) ?right_id //; intros; inv_step; eauto. ... ... @@ -131,7 +131,7 @@ Qed. Lemma wp_fst E e1 v1 e2 v2 Φ : to_val e1 = Some v1 → to_val e2 = Some v2 → ▷ Φ v1 ⊑ || Fst (Pair e1 e2) @ E {{ Φ }}. ▷ Φ v1 ⊑ #> Fst (Pair e1 e2) @ E {{ Φ }}. Proof. intros. rewrite -(wp_lift_pure_det_step (Fst _) e1 None) ?right_id -?wp_value //; intros; inv_step; eauto. ... ... @@ -139,7 +139,7 @@ Qed. Lemma wp_snd E e1 v1 e2 v2 Φ : to_val e1 = Some v1 → to_val e2 = Some v2 → ▷ Φ v2 ⊑ || Snd (Pair e1 e2) @ E {{ Φ }}. ▷ Φ v2 ⊑ #> Snd (Pair e1 e2) @ E {{ Φ }}. Proof. intros. rewrite -(wp_lift_pure_det_step (Snd _) e2 None) ?right_id -?wp_value //; intros; inv_step; eauto. ... ... @@ -147,7 +147,7 @@ Qed. Lemma wp_case_inl E e0 v0 e1 e2 Φ : to_val e0 = Some v0 → ▷ || App e1 e0 @ E {{ Φ }} ⊑ || Case (InjL e0) e1 e2 @ E {{ Φ }}. ▷ #> App e1 e0 @ E {{ Φ }} ⊑ #> Case (InjL e0) e1 e2 @ E {{ Φ }}. Proof. intros. rewrite -(wp_lift_pure_det_step (Case _ _ _) (App e1 e0) None) ?right_id //; intros; inv_step; eauto. ... ... @@ -155,7 +155,7 @@ Qed. Lemma wp_case_inr E e0 v0 e1 e2 Φ : to_val e0 = Some v0 → ▷ || App e2 e0 @ E {{ Φ }} ⊑ || Case (InjR e0) e1 e2 @ E {{ Φ }}. ▷ #> App e2 e0 @ E {{ Φ }} ⊑ #> Case (InjR e0) e1 e2 @ E {{ Φ }}. Proof. intros. rewrite -(wp_lift_pure_det_step (Case _ _ _) (App e2 e0) None) ?right_id //; intros; inv_step; eauto. ... ...
 ... ... @@ -2,7 +2,7 @@ From program_logic Require Export weakestpre viewshifts. Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ) (e : expr Λ) (Φ : val Λ → iProp Λ Σ) : iProp Λ Σ := (□ (P → || e @ E {{ Φ }}))%I. (□ (P → #> e @ E {{ Φ }}))%I. Instance: Params (@ht) 3. Notation "{{ P } } e @ E {{ Φ } }" := (ht E P e Φ) ... ... @@ -38,7 +38,7 @@ Global Instance ht_mono' E : Proper (flip (⊑) ==> eq ==> pointwise_relation _ (⊑) ==> (⊑)) (@ht Λ Σ E). Proof. solve_proper. Qed. Lemma ht_alt E P Φ e : (P ⊑ || e @ E {{ Φ }}) → {{ P }} e @ E {{ Φ }}. Lemma ht_alt E P Φ e : (P ⊑ #> e @ E {{ Φ }}) → {{ P }} e @ E {{ Φ }}. Proof. intros; rewrite -{1}always_const. apply: always_intro. apply impl_intro_l. by rewrite always_const right_id. ... ...
 ... ... @@ -64,8 +64,8 @@ Proof. intros. by apply: (inv_fsa pvs_fsa). Qed. Lemma wp_open_close E e N P Φ R : atomic e → nclose N ⊆ E → R ⊑ inv N P → R ⊑ (▷ P -★ || e @ E ∖ nclose N {{ λ v, ▷ P ★ Φ v }}) → R ⊑ || e @ E {{ Φ }}. R ⊑ (▷ P -★ #> e @ E ∖ nclose N {{ λ v, ▷ P ★ Φ v }}) → R ⊑ #> e @ E {{ Φ }}. Proof. intros. by apply: (inv_fsa (wp_fsa e)). Qed. Lemma inv_alloc N P : ▷ P ⊑ pvs N N (inv N P). ... ...
 ... ... @@ -23,8 +23,8 @@ Lemma wp_lift_step E1 E2 reducible e1 σ1 → (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) → (|={E2,E1}=> ▷ ownP σ1 ★ ▷ ∀ e2 σ2 ef, (■ φ e2 σ2 ef ∧ ownP σ2) -★ |={E1,E2}=> || e2 @ E2 {{ Φ }} ★ wp_fork ef) ⊑ || e1 @ E2 {{ Φ }}. (■ φ e2 σ2 ef ∧ ownP σ2) -★ |={E1,E2}=> #> e2 @ E2 {{ Φ }} ★ wp_fork ef) ⊑ #> e1 @ E2 {{ Φ }}. Proof. intros ? He Hsafe Hstep. rewrite pvs_eq wp_eq. uPred.unseal; split=> n r ? Hvs; constructor; auto. ... ... @@ -45,7 +45,7 @@ Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Φ e1 : to_val e1 = None → (∀ σ1, reducible e1 σ1) → (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) → (▷ ∀ e2 ef, ■ φ e2 ef → || e2 @ E {{ Φ }} ★ wp_fork ef) ⊑ || e1 @ E {{ Φ }}. (▷ ∀ e2 ef, ■ φ e2 ef → #> e2 @ E {{ Φ }} ★ wp_fork ef) ⊑ #> e1 @ E {{ Φ }}. Proof. intros He Hsafe Hstep; rewrite wp_eq; uPred.unseal. split=> n r ? Hwp; constructor; auto. ... ... @@ -67,7 +67,7 @@ Lemma wp_lift_atomic_step {E Φ} e1 (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → ∃ v2, to_val e2 = Some v2 ∧ φ v2 σ2 ef) → (▷ ownP σ1 ★ ▷ ∀ v2 σ2 ef, ■ φ v2 σ2 ef ∧ ownP σ2 -★ Φ v2 ★ wp_fork ef) ⊑ || e1 @ E {{ Φ }}. ⊑ #> e1 @ E {{ Φ }}. Proof. intros. rewrite -(wp_lift_step E E (λ e2 σ2 ef, ∃ v2, to_val e2 = Some v2 ∧ φ v2 σ2 ef) _ e1 σ1) //; []. ... ... @@ -86,7 +86,7 @@ Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 ef : reducible e1 σ1 → (∀ e2' σ2' ef', prim_step e1 σ1 e2' σ2' ef' → σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') → (▷ ownP σ1 ★ ▷ (ownP σ2 -★ Φ v2 ★ wp_fork ef)) ⊑ || e1 @ E {{ Φ }}. (▷ ownP σ1 ★ ▷ (ownP σ2 -★ Φ v2 ★ wp_fork ef)) ⊑ #> e1 @ E {{ Φ }}. Proof. intros. rewrite -(wp_lift_atomic_step _ (λ v2' σ2' ef', σ2 = σ2' ∧ v2 = v2' ∧ ef = ef') σ1) //; last naive_solver. ... ... @@ -101,7 +101,7 @@ Lemma wp_lift_pure_det_step {E Φ} e1 e2 ef : to_val e1 = None → (∀ σ1, reducible e1 σ1) → (∀ σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ ef = ef')→ ▷ (|| e2 @ E {{ Φ }} ★ wp_fork ef) ⊑ || e1 @ E {{ Φ }}. ▷ (#> e2 @ E {{ Φ }} ★ wp_fork ef) ⊑ #> e1 @ E {{ Φ }}. Proof. intros. rewrite -(wp_lift_pure_step E (λ e2' ef', e2 = e2' ∧ ef = ef') _ e1) //=. ... ...
 ... ... @@ -57,12 +57,12 @@ Definition wp_eq : @wp = @wp_def := proj2_sig wp_aux. Arguments wp {_ _} _ _ _. Instance: Params (@wp) 4. Notation "|| e @ E {{ Φ } }" := (wp E e Φ) Notation "#> e @ E {{ Φ } }" := (wp E e Φ) (at level 20, e, Φ at level 200, format "|| e @ E {{ Φ } }") : uPred_scope. Notation "|| e {{ Φ } }" := (wp ⊤ e Φ) format "#> e @ E {{ Φ } }") : uPred_scope. Notation "#> e {{ Φ } }" := (wp ⊤ e Φ) (at level 20, e, Φ at level 200, format "|| e {{ Φ } }") : uPred_scope. format "#> e {{ Φ } }") : uPred_scope. Section wp. Context {Λ : language} {Σ : rFunctor}. ... ... @@ -93,7 +93,7 @@ Proof. by intros Φ Φ' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist. Qed. Lemma wp_mask_frame_mono E1 E2 e Φ Ψ : E1 ⊆ E2 → (∀ v, Φ v ⊑ Ψ v) → || e @ E1 {{ Φ }} ⊑ || e @ E2 {{ Ψ }}. E1 ⊆ E2 → (∀ v, Φ v ⊑ Ψ v) → #> e @ E1 {{ Φ }} ⊑ #> e @ E2 {{ Ψ }}. Proof. rewrite wp_eq. intros HE HΦ; split=> n r. revert e r; induction n as [n IH] using lt_wf_ind=> e r. ... ... @@ -121,9 +121,9 @@ Proof. intros He; destruct 3; [by rewrite ?to_of_val in He|eauto]. Qed. Lemma wp_value' E Φ v : Φ v ⊑ || of_val v @ E {{ Φ }}. Lemma wp_value' E Φ v : Φ v ⊑ #> of_val v @ E {{ Φ }}. Proof. rewrite wp_eq. split=> n r; constructor; by apply pvs_intro. Qed. Lemma pvs_wp E e Φ : (|={E}=> || e @ E {{ Φ }}) ⊑ || e @ E {{ Φ }}. Lemma pvs_wp E e Φ : (|={E}=> #> e @ E {{ Φ }}) ⊑ #> e @ E {{ Φ }}. Proof. rewrite wp_eq. split=> n r ? Hvs. destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|]. ... ... @@ -133,7 +133,7 @@ Proof. rewrite pvs_eq in Hvs. destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto. eapply wp_step_inv with (S k) r'; eauto. Qed. Lemma wp_pvs E e Φ : || e @ E {{ λ v, |={E}=> Φ v }} ⊑ || e @ E {{ Φ }}. Lemma wp_pvs E e Φ : #> e @ E {{ λ v, |={E}=> Φ v }} ⊑ #> e @ E {{ Φ }}. Proof. rewrite wp_eq. split=> n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r Hr HΦ. ... ... @@ -147,7 +147,7 @@ Proof. Qed. Lemma wp_atomic E1 E2 e Φ : E2 ⊆ E1 → atomic e → (|={E1,E2}=> || e @ E2 {{ λ v, |={E2,E1}=> Φ v }}) ⊑ || e @ E1 {{ Φ }}. (|={E1,E2}=> #> e @ E2 {{ λ v, |={E2,E1}=> Φ v }}) ⊑ #> e @ E1 {{ Φ }}. Proof. rewrite wp_eq pvs_eq. intros ? He; split=> n r ? Hvs; constructor. eauto using atomic_not_val. intros rf k Ef σ1 ???. ... ... @@ -164,7 +164,7 @@ Proof. - by rewrite -assoc. - constructor; apply pvs_intro; auto. Qed. Lemma wp_frame_r E e Φ R : (|| e @ E {{ Φ }} ★ R) ⊑ || e @ E {{ λ v, Φ v ★ R }}. Lemma wp_frame_r E e Φ R : (#> e @ E {{ Φ }} ★ R) ⊑ #> e @ E {{ λ v, Φ v ★ R }}. Proof. rewrite wp_eq. uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&?). revert Hvalid. rewrite Hr; clear Hr; revert e r Hwp. ... ... @@ -183,7 +183,7 @@ Proof. - apply IH; eauto using uPred_weaken. Qed. Lemma wp_frame_later_r E e Φ R : to_val e = None → (|| e @ E {{ Φ }} ★ ▷ R) ⊑ || e @ E {{ λ v, Φ v ★ R }}. to_val e = None → (#> e @ E {{ Φ }} ★ ▷ R) ⊑ #> e @ E {{ λ v, Φ v ★ R }}. Proof. rewrite wp_eq. intros He; uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&?). revert Hvalid; rewrite Hr; clear Hr. ... ... @@ -199,7 +199,7 @@ Proof. eapply uPred_weaken with n rR; eauto. Qed. Lemma wp_bind `{LanguageCtx Λ K} E e Φ : || e @ E {{ λ v, || K (of_val v) @ E {{ Φ }} }} ⊑ || K e @ E {{ Φ }}. #> e @ E {{ λ v, #> K (of_val v) @ E {{ Φ }} }} ⊑ #> K e @ E {{ Φ }}. Proof. rewrite wp_eq. split=> n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r ?. ... ... @@ -218,44 +218,44 @@ Qed. (** * Derived rules *) Import uPred. Lemma wp_mono E e Φ Ψ : (∀ v, Φ v ⊑ Ψ v) → || e @ E {{ Φ }} ⊑ || e @ E {{ Ψ }}. Lemma wp_mono E e Φ Ψ : (∀ v, Φ v ⊑ Ψ v) → #> e @ E {{ Φ }} ⊑ #> e @ E {{ Ψ }}. Proof. by apply wp_mask_frame_mono. Qed. Global Instance wp_mono' E e : Proper (pointwise_relation _ (⊑) ==> (⊑)) (@wp Λ Σ E e). Proof. by intros Φ Φ' ?; apply wp_mono. Qed. Lemma wp_strip_pvs E e P Φ : P ⊑ || e @ E {{ Φ }} → (|={E}=> P) ⊑ || e @ E {{ Φ }}. P ⊑ #> e @ E {{ Φ }} → (|={E}=> P) ⊑ #> e @ E {{ Φ }}. Proof. move=>->. by rewrite pvs_wp. Qed. Lemma wp_value E Φ e v : to_val e = Some v → Φ v ⊑ || e @ E {{ Φ }}. Lemma wp_value E Φ e v : to_val e = Some v → Φ v ⊑ #> e @ E {{ Φ }}. Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed. Lemma wp_value_pvs E Φ e v : to_val e = Some v → (|={E}=> Φ v) ⊑ || e @ E {{ Φ }}. to_val e = Some v → (|={E}=> Φ v) ⊑ #> e @ E {{ Φ }}. Proof. intros. rewrite -wp_pvs. rewrite -wp_value //. Qed. Lemma wp_frame_l E e Φ R : (R ★ || e @ E {{ Φ }}) ⊑ || e @ E {{ λ v, R ★ Φ v }}. Lemma wp_frame_l E e Φ R : (R ★ #> e @ E {{ Φ }}) ⊑ #> e @ E {{ λ v, R ★ Φ v }}. Proof. setoid_rewrite (comm _ R); apply wp_frame_r. Qed. Lemma wp_frame_later_l E e Φ R : to_val e = None → (▷ R ★ || e @ E {{ Φ }}) ⊑ || e @ E {{ λ v, R ★ Φ v }}. to_val e = None → (▷ R ★ #> e @ E {{ Φ }}) ⊑ #> e @ E {{ λ v, R ★ Φ v }}. Proof. rewrite (comm _ (▷ R)%I); setoid_rewrite (comm _ R). apply wp_frame_later_r. Qed. Lemma wp_always_l E e Φ R `{!AlwaysStable R} : (R ∧ || e @ E {{ Φ }}) ⊑ || e @ E {{ λ v, R ∧ Φ v }}. (R ∧ #> e @ E {{ Φ }}) ⊑ #> e @ E {{ λ v, R ∧ Φ v }}. Proof. by setoid_rewrite (always_and_sep_l _ _); rewrite wp_frame_l. Qed.