Commit ffa92c50 authored by Robbert Krebbers's avatar Robbert Krebbers

Introduce notation || e @ E {{ Φ }} for weakest pre.

parent 01eb6f6a
......@@ -146,7 +146,7 @@ Section proof.
Lemma newchan_spec (P : iProp) (Φ : val iProp) :
(heap_ctx heapN l, recv l P send l P - Φ (LocV l))
wp (newchan '()) Φ.
|| newchan '() {{ Φ }}.
Proof.
rewrite /newchan. wp_rec. (* TODO: wp_seq. *)
rewrite -wp_pvs. wp> eapply wp_alloc; eauto with I ndisj.
......@@ -196,7 +196,7 @@ Section proof.
Qed.
Lemma signal_spec l P (Φ : val iProp) :
heapN N (send l P P Φ '()) wp (signal (LocV l)) Φ.
heapN N (send l P P Φ '()) || signal (LocV l) {{ Φ }}.
Proof.
intros Hdisj. rewrite /signal /send /barrier_ctx. rewrite sep_exist_r.
apply exist_elim=>γ. wp_rec. (* FIXME wp_let *)
......@@ -226,12 +226,12 @@ Section proof.
Qed.
Lemma wait_spec l P (Φ : val iProp) :
heapN N (recv l P (P - Φ '())) wp (wait (LocV l)) Φ.
heapN N (recv l P (P - Φ '())) || wait (LocV l) {{ Φ }}.
Proof.
Abort.
Lemma split_spec l P1 P2 Φ :
(recv l (P1 P2) (recv l P1 recv l P2 - Φ '())) wp Skip Φ.
(recv l (P1 P2) (recv l P1 recv l P2 - Φ '())) || Skip {{ Φ }}.
Proof.
Abort.
......
......@@ -17,44 +17,47 @@ Implicit Types Φ : val → iProp heap_lang Σ.
(** Proof rules for the sugar *)
Lemma wp_lam' E x ef e v Φ :
to_val e = Some v wp E (subst ef x v) Φ wp E (App (Lam x ef) e) Φ.
to_val e = Some v
|| subst ef x v @ E {{ Φ }} || App (Lam x ef) e @ E {{ Φ }}.
Proof. intros. by rewrite -wp_rec' ?subst_empty. Qed.
Lemma wp_let' E x e1 e2 v Φ :
to_val e1 = Some v wp E (subst e2 x v) Φ wp E (Let x e1 e2) Φ.
to_val e1 = Some v
|| subst e2 x v @ E {{ Φ }} || Let x e1 e2 @ E {{ Φ }}.
Proof. apply wp_lam'. Qed.
Lemma wp_seq E e1 e2 Φ : wp E e1 (λ _, wp E e2 Φ) wp E (Seq e1 e2) Φ.
Lemma wp_seq E e1 e2 Φ :
|| e1 @ E {{ λ _, || e2 @ E {{ Φ }} }} || Seq e1 e2 @ E {{ Φ }}.
Proof.
rewrite -(wp_bind [LetCtx "" e2]). apply wp_mono=>v.
by rewrite -wp_let' //= ?to_of_val ?subst_empty.
Qed.
Lemma wp_skip E Φ : (Φ (LitV LitUnit)) wp E Skip Φ.
Lemma wp_skip E Φ : Φ (LitV LitUnit) || Skip @ E {{ Φ }}.
Proof. rewrite -wp_seq -wp_value // -wp_value //. Qed.
Lemma wp_le E (n1 n2 : Z) P Φ :
(n1 n2 P Φ (LitV $ LitBool true))
(n2 < n1 P Φ (LitV $ LitBool false))
P wp E (BinOp LeOp (Lit $ LitInt n1) (Lit $ LitInt n2)) Φ.
(n1 n2 P Φ (LitV (LitBool true)))
(n2 < n1 P Φ (LitV (LitBool false)))
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.
Qed.
Lemma wp_lt E (n1 n2 : Z) P Φ :
(n1 < n2 P Φ (LitV $ LitBool true))
(n2 n1 P Φ (LitV $ LitBool false))
P wp E (BinOp LtOp (Lit $ LitInt n1) (Lit $ LitInt n2)) Φ.
(n1 < n2 P Φ (LitV (LitBool true)))
(n2 n1 P Φ (LitV (LitBool false)))
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.
Qed.
Lemma wp_eq E (n1 n2 : Z) P Φ :
(n1 = n2 P Φ (LitV $ LitBool true))
(n1 n2 P Φ (LitV $ LitBool false))
P wp E (BinOp EqOp (Lit $ LitInt n1) (Lit $ LitInt n2)) Φ.
(n1 = n2 P Φ (LitV (LitBool true)))
(n1 n2 P Φ (LitV (LitBool false)))
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.
......
......@@ -65,7 +65,7 @@ Section heap.
(** Allocation *)
Lemma heap_alloc E N σ :
authG heap_lang Σ heapRA nclose N E
ownP σ (|={E}=> (_ : heapG Σ), heap_ctx N Π★{map σ} heap_mapsto).
ownP σ (|={E}=> _ : heapG Σ, heap_ctx N Π★{map σ} heap_mapsto).
Proof.
intros. rewrite -{1}(from_to_heap σ). etransitivity.
{ rewrite [ownP _]later_intro.
......@@ -100,7 +100,7 @@ Section heap.
to_val e = Some v nclose N E
P heap_ctx N
P ( l, l v - Φ (LocV l))
P wp E (Alloc e) Φ.
P || Alloc e @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? Hctx HP.
transitivity (|={E}=> auth_own heap_name P)%I.
......@@ -127,7 +127,7 @@ Section heap.
nclose N E
P heap_ctx N
P ( l v (l v - Φ v))
P wp E (Load (Loc l)) Φ.
P || Load (Loc l) @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv /heap_mapsto=>HN ? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) id)
......@@ -146,7 +146,7 @@ Section heap.
to_val e = Some v nclose N E
P heap_ctx N
P ( l v' (l v - Φ (LitV LitUnit)))
P wp E (Store (Loc l) e) Φ.
P || Store (Loc l) e @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv /heap_mapsto=>? HN ? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v) l))
......@@ -167,7 +167,7 @@ Section heap.
nclose N E
P heap_ctx N
P ( l v' (l v' - Φ (LitV (LitBool false))))
P wp E (Cas (Loc l) e1 e2) Φ.
P || Cas (Loc l) e1 e2 @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv /heap_mapsto=>??? HN ? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) id)
......@@ -187,7 +187,7 @@ Section heap.
nclose N E
P heap_ctx N
P ( l v1 (l v2 - Φ (LitV (LitBool true))))
P wp E (Cas (Loc l) e1 e2) Φ.
P || Cas (Loc l) e1 e2 @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? HN ? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v2) l))
......
......@@ -16,18 +16,14 @@ Implicit Types ef : option expr.
(** Bind. *)
Lemma wp_bind {E e} K Φ :
wp E e (λ v, wp E (fill K (of_val v)) Φ) wp E (fill K e) Φ.
Proof. apply weakestpre.wp_bind. Qed.
Lemma wp_bindi {E e} Ki Φ :
wp E e (λ v, wp E (fill_item Ki (of_val v)) Φ) wp E (fill_item Ki 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)))
wp E (Alloc e) Φ.
|| Alloc e @ E {{ Φ }}.
Proof.
(* TODO RJ: This works around ssreflect bug #22. *)
intros. set (φ v' σ' ef := l,
......@@ -44,7 +40,7 @@ Qed.
Lemma wp_load_pst E σ l v Φ :
σ !! l = Some v
(ownP σ (ownP σ - Φ v)) wp E (Load (Loc l)) Φ.
(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.
......@@ -52,7 +48,8 @@ Qed.
Lemma wp_store_pst E σ l e v v' Φ :
to_val e = Some v σ !! l = Some v'
(ownP σ (ownP (<[l:=v]>σ) - Φ (LitV LitUnit))) wp E (Store (Loc l) e) Φ.
(ownP σ (ownP (<[l:=v]>σ) - Φ (LitV LitUnit)))
|| 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.
......@@ -60,7 +57,8 @@ 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))) wp E (Cas (Loc l) e1 e2) Φ.
(ownP σ (ownP σ - Φ (LitV $ LitBool false)))
|| 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.
......@@ -69,15 +67,15 @@ 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)))
wp E (Cas (Loc l) e1 e2) Φ.
|| 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.
intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool true)
(<[l:=v2]>σ) None) ?right_id //; last by intros; inv_step; eauto.
Qed.
(** Base axioms for core primitives of the language: Stateless reductions *)
Lemma wp_fork E e Φ :
( Φ (LitV LitUnit) wp (Σ:=Σ) e (λ _, True)) wp E (Fork 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.
......@@ -88,7 +86,8 @@ Qed.
The final version is defined in substitution.v. *)
Lemma wp_rec' E f x e1 e2 v Φ :
to_val e2 = Some v
wp E (subst (subst e1 f (RecV f x e1)) x v) Φ wp E (App (Rec f x e1) e2) Φ.
|| subst (subst e1 f (RecV f x e1)) x v @ E {{ Φ }}
|| App (Rec f x e1) e2 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_step (App _ _)
(subst (subst e1 f (RecV f x e1)) x v) None) ?right_id //=;
......@@ -97,7 +96,7 @@ Qed.
Lemma wp_un_op E op l l' Φ :
un_op_eval op l = Some l'
Φ (LitV l') wp E (UnOp op (Lit l)) Φ.
Φ (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.
......@@ -105,21 +104,21 @@ Qed.
Lemma wp_bin_op E op l1 l2 l' Φ :
bin_op_eval op l1 l2 = Some l'
Φ (LitV l') wp E (BinOp op (Lit l1) (Lit l2)) Φ.
Φ (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 Φ :
wp E e1 Φ wp E (If (Lit $ LitBool true) e1 e2) Φ.
|| 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 Φ :
wp E e2 Φ wp E (If (Lit $ LitBool false) e1 e2) Φ.
|| 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.
......@@ -127,7 +126,7 @@ Qed.
Lemma wp_fst E e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2
Φ v1 wp E (Fst $ Pair e1 e2) Φ.
Φ 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.
......@@ -135,7 +134,7 @@ Qed.
Lemma wp_snd E e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2
Φ v2 wp E (Snd $ Pair e1 e2) Φ.
Φ 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.
......@@ -143,7 +142,7 @@ Qed.
Lemma wp_case_inl' E e0 v0 x1 e1 x2 e2 Φ :
to_val e0 = Some v0
wp E (subst e1 x1 v0) Φ wp E (Case (InjL e0) x1 e1 x2 e2) Φ.
|| subst e1 x1 v0 @ E {{ Φ }} || Case (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _)
(subst e1 x1 v0) None) ?right_id //; intros; inv_step; eauto.
......@@ -151,7 +150,7 @@ Qed.
Lemma wp_case_inr' E e0 v0 x1 e1 x2 e2 Φ :
to_val e0 = Some v0
wp E (subst e2 x2 v0) Φ wp E (Case (InjR e0) x1 e1 x2 e2) Φ.
|| subst e2 x2 v0 @ E {{ Φ }} || Case (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _)
(subst e2 x2 v0) None) ?right_id //; intros; inv_step; eauto.
......
From heap_lang Require Export derived.
(* What about Arguments for hoare triples?. *)
Arguments wp {_ _} _ _%L _.
Notation "|| e @ E {{ Φ } }" := (wp E e%L Φ)
(at level 20, e, Φ at level 200,
format "|| e @ E {{ Φ } }") : uPred_scope.
Notation "|| e {{ Φ } }" := (wp e%L Φ)
(at level 20, e, Φ at level 200,
format "|| e {{ Φ } }") : uPred_scope.
Coercion LitInt : Z >-> base_lit.
Coercion LitBool : bool >-> base_lit.
......
......@@ -26,10 +26,10 @@ to be unfolded. For example, consider the rule [wp_rec'] from below:
<<
Definition foo : val := rec: "f" "x" := ... .
Lemma wp_rec' E e1 f x erec e2 v Q :
Lemma wp_rec E e1 f x erec e2 v Φ :
e1 = Rec f x erec →
to_val e2 = Some v →
wp E (gsubst (gsubst erec f e1) x e2) Q ⊑ wp E (App e1 e2) Q.
|| gsubst (gsubst erec f e1) x e2 @ E {{ Φ }} ⊑ || App e1 e2 @ E {{ Φ }}.
>>
We ensure that [e1] is substituted instead of [RecV f x erec]. So, for example
......@@ -123,7 +123,7 @@ Hint Resolve to_of_val.
Lemma wp_rec E e1 f x erec e2 v Φ :
e1 = Rec f x erec
to_val e2 = Some v
wp E (gsubst (gsubst erec f e1) x e2) Φ wp E (App e1 e2) Φ.
|| gsubst (gsubst erec f e1) x e2 @ E {{ Φ }} || App e1 e2 @ E {{ Φ }}.
Proof.
intros -> <-%of_to_val.
rewrite (gsubst_correct _ _ (RecV _ _ _)) gsubst_correct.
......@@ -131,21 +131,22 @@ Proof.
Qed.
Lemma wp_lam E x ef e v Φ :
to_val e = Some v wp E (gsubst ef x e) Φ wp E (App (Lam x ef) e) Φ.
to_val e = Some v
|| gsubst ef x e @ E {{ Φ }} || App (Lam x ef) e @ E {{ Φ }}.
Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_lam'. Qed.
Lemma wp_let E x e1 e2 v Φ :
to_val e1 = Some v wp E (gsubst e2 x e1) Φ wp E (Let x e1 e2) Φ.
to_val e1 = Some v
|| gsubst e2 x e1 @ E {{ Φ }} || Let x e1 e2 @ E {{ Φ }}.
Proof. apply wp_lam. Qed.
Lemma wp_case_inl E e0 v0 x1 e1 x2 e2 Φ :
to_val e0 = Some v0
wp E (gsubst e1 x1 e0) Φ wp E (Case (InjL e0) x1 e1 x2 e2) Φ.
|| gsubst e1 x1 e0 @ E {{ Φ }} || Case (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_case_inl'. Qed.
Lemma wp_case_inr E e0 v0 x1 e1 x2 e2 Φ :
to_val e0 = Some v0
wp E (gsubst e2 x2 e0) Φ wp E (Case (InjR e0) x1 e1 x2 e2) Φ.
|| gsubst e2 x2 e0 @ E {{ Φ }} || Case (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_case_inr'. Qed.
End wp.
......@@ -29,7 +29,8 @@ Section LiftingTests.
Definition heap_e : expr :=
let: "x" := ref '1 in "x" <- !"x" + '1;; !"x".
Lemma heap_e_spec E N : nclose N E heap_ctx N wp E heap_e (λ v, v = '2).
Lemma heap_e_spec E N :
nclose N E heap_ctx N || heap_e @ E {{ λ v, v = '2 }}.
Proof.
rewrite /heap_e=>HN. rewrite -(wp_mask_weaken N E) //.
wp> eapply wp_alloc; eauto. apply forall_intro=>l; apply wand_intro_l.
......@@ -48,7 +49,7 @@ Section LiftingTests.
if: "x" '0 then -FindPred (-"x" + '2) '0 else FindPred "x" '0.
Lemma FindPred_spec n1 n2 E Φ :
( (n1 < n2) Φ '(n2 - 1)) wp E (FindPred 'n2 'n1) Φ.
( (n1 < n2) Φ '(n2 - 1)) || FindPred 'n2 'n1 @ E {{ Φ }}.
Proof.
revert n1; apply löb_all_1=>n1.
rewrite (comm uPred_and ( _)%I) assoc; apply const_elim_r=>?.
......@@ -62,7 +63,7 @@ Section LiftingTests.
- wp_value. assert (n1 = n2 - 1) as -> by omega; auto with I.
Qed.
Lemma Pred_spec n E Φ : Φ (LitV (n - 1)) wp E (Pred 'n)%L Φ.
Lemma Pred_spec n E Φ : Φ (LitV (n - 1)) || Pred 'n @ E {{ Φ }}.
Proof.
wp_rec>; apply later_mono; wp_bin_op=> ?; wp_if.
- wp_un_op. wp_bin_op.
......@@ -73,7 +74,7 @@ Section LiftingTests.
Qed.
Lemma Pred_user E :
True wp (Σ:=globalF Σ) E (let: "x" := Pred '42 in Pred "x") (λ v, v = '40).
(True : iProp) || let: "x" := Pred '42 in Pred "x" @ E {{ λ v, v = '40 }}.
Proof.
intros. ewp> apply Pred_spec. wp_rec. ewp> apply Pred_spec. auto with I.
Qed.
......
From program_logic Require Export weakestpre viewshifts.
Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ)
(e : expr Λ) (Φ : val Λ iProp Λ Σ) : iProp Λ Σ := ( (P wp E e Φ))%I.
(e : expr Λ) (Φ : val Λ iProp Λ Σ) : iProp Λ Σ :=
( (P || e @ E {{ Φ }}))%I.
Instance: Params (@ht) 3.
Notation "{{ P } } e @ E {{ Φ } }" := (ht E P e Φ)
......@@ -37,7 +38,7 @@ Global Instance ht_mono' E :
Proper (flip () ==> eq ==> pointwise_relation _ () ==> ()) (@ht Λ Σ E).
Proof. by intros P P' HP e ? <- Φ Φ' HΦ; apply ht_mono. Qed.
Lemma ht_alt E P Φ e : (P wp 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 - wp (E nclose N) e (λ v, P Φ v))
R wp 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).
......
......@@ -24,8 +24,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}=> wp E2 e2 Φ wp_fork ef)
wp E2 e1 Φ.
( φ e2 σ2 ef ownP σ2) - |={E1,E2}=> || e2 @ E2 {{ Φ }} wp_fork ef)
|| e1 @ E2 {{ Φ }}.
Proof.
intros ? He Hsafe Hstep n r ? Hvs; constructor; auto.
intros rf k Ef σ1' ???; destruct (Hvs rf (S k) Ef σ1')
......@@ -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 wp E e2 Φ wp_fork ef) wp E e1 Φ.
( e2 ef, φ e2 ef || e2 @ E {{ Φ }} wp_fork ef) || e1 @ E {{ Φ }}.
Proof.
intros He Hsafe Hstep n r ? Hwp; constructor; auto.
intros rf k Ef σ1 ???; split; [done|]. destruct n as [|n]; first lia.
......@@ -65,7 +65,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)
wp E e1 Φ.
|| e1 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_step E E (λ e2 σ2 ef, v2,
to_val e2 = Some v2 φ v2 σ2 ef) _ e1 σ1) //; [].
......@@ -84,7 +84,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)) wp E e1 Φ.
(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.
......@@ -99,7 +99,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')
(wp E e2 Φ wp_fork ef) wp E e1 Φ.
(|| e2 @ E {{ Φ }} wp_fork ef) || e1 @ E {{ Φ }}.
Proof.
intros.
rewrite -(wp_lift_pure_step E (λ e2' ef', e2 = e2' ef = ef') _ e1) //=.
......
......@@ -51,6 +51,13 @@ Next Obligation.
Qed.
Instance: Params (@wp) 4.
Notation "|| e @ E {{ Φ } }" := (wp E e Φ)
(at level 20, e, Φ at level 200,
format "|| e @ E {{ Φ } }") : uPred_scope.
Notation "|| e {{ Φ } }" := (wp e Φ)
(at level 20, e, Φ at level 200,
format "|| e {{ Φ } }") : uPred_scope.
Section wp.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P : iProp Λ Σ.
......@@ -81,7 +88,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) wp E1 e Φ wp E2 e Ψ.
E1 E2 ( v, Φ v Ψ v) || e @ E1 {{ Φ }} || e @ E2 {{ Ψ }}.
Proof.
intros HE HΦ n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r.
destruct 2 as [n' r v HpvsQ|n' r e1 ? Hgo].
......@@ -95,19 +102,20 @@ Proof.
exists r2, r2'; split_and?; [rewrite HE'|eapply IH|]; eauto.
Qed.
Lemma wp_value_inv E Φ v n r : wp E (of_val v) Φ n r (|={E}=> Φ v)%I n r.
Lemma wp_value_inv E Φ v n r :
|| of_val v @ E {{ Φ }}%I n r (|={E}=> Φ v)%I n r.
Proof.
by inversion 1 as [|??? He]; [|rewrite ?to_of_val in He]; simplify_eq.
Qed.
Lemma wp_step_inv E Ef Φ e k n σ r rf :
to_val e = None 0 < k < n E Ef =
wp E e Φ n r wsat (S k) (E Ef) σ (r rf)
|| e @ E {{ Φ }}%I n r wsat (S k) (E Ef) σ (r rf)
wp_go (E Ef) (λ e, wp E e Φ) (λ e, wp e (λ _, True%I)) k rf e σ.
Proof. intros He; destruct 3; [by rewrite ?to_of_val in He|eauto]. Qed.
Lemma wp_value' E Φ v : Φ v wp E (of_val v) Φ.
Lemma wp_value' E Φ v : Φ v || of_val v @ E {{ Φ }}.
Proof. by constructor; apply pvs_intro. Qed.
Lemma pvs_wp E e Φ : (|={E}=> wp E e Φ) wp E e Φ.
Lemma pvs_wp E e Φ : (|={E}=> || e @ E {{ Φ }}) || e @ E {{ Φ }}.
Proof.
intros n r ? Hvs.
destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
......@@ -117,7 +125,7 @@ Proof.
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 Φ : wp E e (λ v, |={E}=> Φ v) wp E e Φ.
Lemma wp_pvs E e Φ : || e @ E {{ λ v, |={E}=> Φ v }} || e @ E {{ Φ }}.
Proof.
intros n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r Hr HΦ.
destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
......@@ -129,7 +137,8 @@ Proof.
exists r2, r2'; split_and?; [|apply (IH k)|]; auto.
Qed.
Lemma wp_atomic E1 E2 e Φ :
E2 E1 atomic e (|={E1,E2}=> wp E2 e (λ v, |={E2,E1}=> Φ v)) wp E1 e Φ.
E2 E1 atomic e
(|={E1,E2}=> || e @ E2 {{ λ v, |={E2,E1}=> Φ v }}) || e @ E1 {{ Φ }}.