Commit b2a210fe authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents f8078dc2 7dbf98f4
Pipeline #975 passed with stage
*.vo
*.vio
*.v.d
*.glob
*.cache
......
......@@ -35,6 +35,7 @@ prelude/decidable.v
prelude/list.v
prelude/error.v
prelude/functions.v
prelude/hlist.v
algebra/option.v
algebra/cmra.v
algebra/cmra_big_op.v
......@@ -72,7 +73,7 @@ program_logic/hoare.v
program_logic/language.v
program_logic/ectx_language.v
program_logic/ectxi_language.v
program_logic/ectx_weakestpre.v
program_logic/ectx_lifting.v
program_logic/ghost_ownership.v
program_logic/global_functor.v
program_logic/saved_prop.v
......
......@@ -467,8 +467,6 @@ Lemma const_elim φ Q R : Q ⊢ ■ φ → (φ → Q ⊢ R) → Q ⊢ R.
Proof.
unseal; intros HQP HQR; split=> n x ??; apply HQR; first eapply HQP; eauto.
Qed.
Lemma False_elim P : False P.
Proof. by unseal; split=> n x ?. Qed.
Lemma and_elim_l P Q : (P Q) P.
Proof. by unseal; split=> n x ? [??]. Qed.
Lemma and_elim_r P Q : (P Q) Q.
......@@ -496,7 +494,7 @@ Lemma exist_intro {A} {Ψ : A → uPred M} a : Ψ a ⊢ (∃ a, Ψ a).
Proof. unseal; split=> n x ??; by exists a. Qed.
Lemma exist_elim {A} (Φ : A uPred M) Q : ( a, Φ a Q) ( a, Φ a) Q.
Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed.
Lemma eq_refl {A : cofeT} (a : A) P : P (a a).
Lemma eq_refl {A : cofeT} (a : A) : True (a a).
Proof. unseal; by split=> n x ??; simpl. Qed.
Lemma eq_rewrite {A : cofeT} a b (Ψ : A uPred M) P
`{HΨ : n, Proper (dist n ==> dist n) Ψ} : P (a b) P Ψ a P Ψ b.
......@@ -512,6 +510,8 @@ Proof.
Qed.
(* Derived logical stuff *)
Lemma False_elim P : False P.
Proof. by apply (const_elim False). Qed.
Lemma True_intro P : P True.
Proof. by apply const_intro. Qed.
Lemma and_elim_l' P Q R : P R (P Q) R.
......@@ -679,10 +679,13 @@ Lemma const_elim_r φ Q R : (φ → Q ⊢ R) → (Q ∧ ■ φ) ⊢ R.
Proof. intros; apply const_elim with φ; eauto. Qed.
Lemma const_equiv (φ : Prop) : φ ( φ) True.
Proof. intros; apply (anti_symm _); auto using const_intro. Qed.
Lemma eq_refl' {A : cofeT} (a : A) P : P (a a).
Proof. rewrite (True_intro P). apply eq_refl. Qed.
Hint Resolve eq_refl'.
Lemma equiv_eq {A : cofeT} P (a b : A) : a b P (a b).
Proof. intros ->; apply eq_refl. Qed.
Proof. by intros ->. Qed.
Lemma eq_sym {A : cofeT} (a b : A) : (a b) (b a).
Proof. apply (eq_rewrite a b (λ b, b a)%I); auto using eq_refl. solve_proper. Qed.
Proof. apply (eq_rewrite a b (λ b, b a)%I); auto. solve_proper. Qed.
(* BI connectives *)
Lemma sep_mono P P' Q Q' : P Q P' Q' (P P') (Q Q').
......@@ -898,7 +901,7 @@ Proof.
apply (anti_symm ()); auto using always_elim.
apply (eq_rewrite a b (λ b, (a b))%I); auto.
{ intros n; solve_proper. }
rewrite -(eq_refl a True) always_const; auto.
rewrite -(eq_refl a) always_const; auto.
Qed.
Lemma always_and_sep P Q : ( (P Q)) ( (P Q)).
Proof. apply (anti_symm ()); auto using always_and_sep_1. Qed.
......@@ -1174,5 +1177,5 @@ Hint Resolve and_intro and_elim_l' and_elim_r' : I.
Hint Resolve always_mono : I.
Hint Resolve sep_elim_l' sep_elim_r' sep_mono : I.
Hint Immediate True_intro False_elim : I.
Hint Immediate iff_refl eq_refl : I.
Hint Immediate iff_refl eq_refl' : I.
End uPred.
......@@ -20,7 +20,7 @@ Implicit Types Φ : val → iProp heap_lang Σ.
Lemma wp_lam E x ef e v Φ :
to_val e = Some v
WP subst' x e ef @ E {{ Φ }} WP App (Lam x ef) e @ E {{ Φ }}.
Proof. intros. by rewrite -wp_rec. Qed.
Proof. intros. by rewrite -(wp_rec _ BAnon) //. Qed.
Lemma wp_let E x e1 e2 v Φ :
to_val e1 = Some v
......
......@@ -120,8 +120,7 @@ Section heap.
Global Instance heap_mapsto_timeless l q v : TimelessP (l {q} v).
Proof. rewrite /heap_mapsto. apply _. Qed.
Lemma heap_mapsto_op_eq l q1 q2 v :
(l {q1} v l {q2} v) (l {q1+q2} v).
Lemma heap_mapsto_op_eq l q1 q2 v : (l {q1} v l {q2} v) l {q1+q2} v.
Proof. by rewrite -auth_own_op op_singleton Frac_op dec_agree_idemp. Qed.
Lemma heap_mapsto_op l q1 q2 v1 v2 :
......@@ -135,8 +134,7 @@ Section heap.
rewrite option_validI frac_validI discrete_valid. by apply const_elim_r.
Qed.
Lemma heap_mapsto_op_split l q v :
(l {q} v) (l {q/2} v l {q/2} v).
Lemma heap_mapsto_op_split l q v : l {q} v (l {q/2} v l {q/2} v).
Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
(** Weakest precondition *)
......@@ -146,10 +144,8 @@ Section heap.
Proof.
iIntros {??} "[#Hinv HΦ]". rewrite /heap_ctx.
iPvs (auth_empty heap_name) as "Hheap".
(* TODO: change [auth_fsa] to single turnstile and use [iApply] *)
apply (auth_fsa heap_inv (wp_fsa (Alloc e)))
with N heap_name ; simpl; eauto with I.
iFrame "Hheap". iIntros {h}. rewrite [ h]left_id.
iApply (auth_fsa heap_inv (wp_fsa (Alloc e)) _ N); simpl; eauto.
iFrame "Hinv Hheap". iIntros {h}. rewrite [ h]left_id.
iIntros "[% Hheap]". rewrite /heap_inv.
iApply wp_alloc_pst; first done. iFrame "Hheap". iNext.
iIntros {l} "[% Hheap]". iExists (op {[ l := Frac 1 (DecAgree v) ]}), _, _.
......@@ -162,66 +158,57 @@ Section heap.
Lemma wp_load N E l q v Φ :
nclose N E
(heap_ctx N l {q} v (l {q} v - Φ v)) WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
(heap_ctx N l {q} v (l {q} v - Φ v))
WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Proof.
iIntros {?} "[#Hinv [Hmapsto HΦ]]". rewrite /heap_ctx /heap_mapsto.
apply (auth_fsa' heap_inv (wp_fsa _) id)
with N heap_name {[ l := Frac q (DecAgree v) ]}; simpl; eauto with I.
iFrame "Hmapsto". iIntros {h} "[% Hheap]". rewrite /heap_inv.
iIntros {?} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
iApply (auth_fsa' heap_inv (wp_fsa _) id _ N _
heap_name {[ l := Frac q (DecAgree v) ]}); simpl; eauto.
iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
rewrite of_heap_singleton_op //. iFrame "Hheap". iNext.
rewrite of_heap_singleton_op //. iFrame "Hl". iNext.
iIntros "$". by iSplit.
Qed.
Lemma wp_store N E l v' e v P Φ :
to_val e = Some v
P heap_ctx N nclose N E
P ( l v' (l v - Φ (LitV LitUnit)))
P WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Lemma wp_store N E l v' e v Φ :
to_val e = Some v nclose N E
(heap_ctx N l v' (l v - Φ (LitV LitUnit)))
WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv=> ??? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v)) l))
with N heap_name {[ l := Frac 1 (DecAgree v') ]}; simpl; eauto with I.
rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc; apply const_elim_sep_l=> ?.
rewrite -(wp_store_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
rewrite /heap_inv alter_singleton insert_insert !of_heap_singleton_op; eauto.
rewrite const_equiv; last naive_solver.
apply sep_mono_r, later_mono, wand_intro_l. by rewrite left_id -later_intro.
iIntros {??} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
iApply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v)) l) _
N _ heap_name {[ l := Frac 1 (DecAgree v') ]}); simpl; eauto.
iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
rewrite alter_singleton insert_insert !of_heap_singleton_op; eauto.
iFrame "Hl". iNext. iIntros "$". iFrame "HΦ". iPureIntro; naive_solver.
Qed.
Lemma wp_cas_fail N E l q v' e1 v1 e2 v2 P Φ :
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 WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Lemma wp_cas_fail N E l q v' e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2 v' v1 nclose N E
(heap_ctx N l {q} v' (l {q} v' - Φ (LitV (LitBool false))))
WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv=>????? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) id)
with N heap_name {[ l := Frac q (DecAgree v') ]}; simpl; eauto 10 with I.
rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc; apply const_elim_sep_l=> ?.
rewrite -(wp_cas_fail_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
rewrite const_equiv // left_id.
rewrite /heap_inv !of_heap_singleton_op //.
apply sep_mono_r, later_mono, wand_intro_l. by rewrite -later_intro.
iIntros {????} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
iApply (auth_fsa' heap_inv (wp_fsa _) id _ N _
heap_name {[ l := Frac q (DecAgree v') ]}); simpl; eauto 10.
iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
rewrite of_heap_singleton_op //. iFrame "Hl". iNext.
iIntros "$". by iSplit.
Qed.
Lemma wp_cas_suc N E l e1 v1 e2 v2 P Φ :
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 WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Lemma wp_cas_suc N E l e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2 nclose N E
(heap_ctx N l v1 (l v2 - Φ (LitV (LitBool true))))
WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv=> ???? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v2)) l))
with N heap_name {[ l := Frac 1 (DecAgree v1) ]}; simpl; eauto 10 with I.
rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc; apply const_elim_sep_l=> ?.
rewrite -(wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))) //;
last by rewrite lookup_insert.
rewrite /heap_inv alter_singleton insert_insert !of_heap_singleton_op; eauto.
rewrite lookup_insert const_equiv; last naive_solver.
apply sep_mono_r, later_mono, wand_intro_l. by rewrite left_id -later_intro.
iIntros {???} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
iApply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v2)) l)
_ N _ heap_name {[ l := Frac 1 (DecAgree v1) ]}); simpl; eauto 10.
iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //.
rewrite alter_singleton insert_insert !of_heap_singleton_op; eauto.
iFrame "Hl". iNext. iIntros "$". iFrame "HΦ". iPureIntro; naive_solver.
Qed.
End heap.
......@@ -119,8 +119,6 @@ Arguments PairV _%V _%V.
Arguments InjLV _%V.
Arguments InjRV _%V.
Definition signal : val := RecV BAnon (BNamed "x") (Store (Var "x") (Lit (LitInt 1))).
Fixpoint of_val (v : val) : expr [] :=
match v with
| RecV f x e => Rec f x e
......
......@@ -4,3 +4,4 @@ Definition newbarrier : val := λ: <>, ref #0.
Definition signal : val := λ: "x", '"x" <- #1.
Definition wait : val :=
rec: "wait" "x" := if: !'"x" = #1 then #() else '"wait" '"x".
Global Opaque newbarrier signal wait.
......@@ -82,14 +82,14 @@ Lemma ress_split i i1 i2 Q R1 R2 P I :
ress P ({[i1]} ({[i2]} (I {[i]}))).
Proof.
iIntros {????} "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as {Ψ} "[HPΨ HΨ]".
iDestruct (big_sepS_delete _ _ i) "HΨ" as "[#HΨi HΨ]"; first done.
iDestruct (big_sepS_delete _ _ i with "HΨ") as "[#HΨi HΨ]"; first done.
iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ".
- iPoseProof (saved_prop_agree i Q (Ψ i)) "#" as "Heq"; first by iSplit.
iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize "HPΨ" "HP".
iDestruct (big_sepS_delete _ _ i) "HPΨ" as "[HΨ HPΨ]"; first done.
iDestruct "HQR" "HΨ" as "[HR1 HR2]".
rewrite !big_sepS_insert''; [|set_solver ..]. by iFrame "HR1 HR2".
- rewrite !big_sepS_insert'; [|set_solver ..]. by repeat iSplit.
- iPoseProof (saved_prop_agree i Q (Ψ i) with "#") as "Heq"; first by iSplit.
iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize ("HPΨ" with "HP").
iDestruct (big_sepS_delete _ _ i with "HPΨ") as "[HΨ HPΨ]"; first done.
iDestruct ("HQR" with "HΨ") as "[HR1 HR2]".
rewrite !big_sepS_insert''; [|abstract set_solver ..]. by iFrame "HR1 HR2".
- rewrite !big_sepS_insert'; [|abstract set_solver ..]. by repeat iSplit.
Qed.
(** Actual proofs *)
......@@ -102,8 +102,8 @@ Proof.
rewrite /newbarrier. wp_seq. iApply wp_pvs. wp_alloc l as "Hl".
iApply "HΦ".
iPvs (saved_prop_alloc (F:=idCF) _ P) as {γ} "#?".
iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}))
"-" as {γ'} "[#? Hγ']"; eauto.
iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "-")
as {γ'} "[#? Hγ']"; eauto.
{ iNext. rewrite /barrier_inv /=. iFrame "Hl".
iExists (const P). rewrite !big_sepS_singleton /=.
iSplit; [|done]. by iIntros "> ?". }
......@@ -113,9 +113,9 @@ Proof.
sts_ownS γ' low_states {[Send]})%I as "[Hr Hs]" with "-".
{ iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
+ set_solver.
+ iApply sts_own_weaken "Hγ'";
+ iApply (sts_own_weaken with "Hγ'");
auto using sts.closed_op, i_states_closed, low_states_closed;
set_solver. }
abstract set_solver. }
iPvsIntro. rewrite /recv /send. iSplitL "Hr".
- iExists γ', P, P, γ. iFrame "Hr". repeat iSplit; auto. by iIntros "> ?".
- iExists γ'. by iSplit.
......@@ -132,7 +132,7 @@ Proof.
iSplit; [iPureIntro; by eauto using signal_step|].
iSplitR "HΦ"; [iNext|by iIntros "?"].
rewrite {2}/barrier_inv /ress /=; iFrame "Hl".
iDestruct "Hr" as {Ψ} "[? Hsp]"; iExists Ψ; iFrame "Hsp".
iDestruct "Hr" as {Ψ} "[Hr Hsp]"; iExists Ψ; iFrame "Hsp".
iIntros "> _"; by iApply "Hr".
Qed.
......@@ -149,20 +149,20 @@ Proof.
{ iNext. rewrite {2}/barrier_inv /=. by iFrame "Hl". }
iIntros "Hγ".
iPvsAssert (sts_ownS γ (i_states i) {[Change i]})%I as "Hγ" with "[Hγ]".
{ iApply sts_own_weaken "Hγ"; eauto using i_states_closed. }
wp_op=> ?; simplify_eq; wp_if. iApply "IH" "Hγ [HQR] HΦ". by iNext.
{ iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
wp_op=> ?; simplify_eq; wp_if. iApply ("IH" with "Hγ [HQR] HΦ"). by iNext.
- (* a High state: the comparison succeeds, and we perform a transition and
return to the client *)
iExists (State High (I {[ i ]})), ( : set token).
iSplit; [iPureIntro; by eauto using wait_step|].
iDestruct "Hr" as {Ψ} "[HΨ Hsp]".
iDestruct (big_sepS_delete _ _ i) "Hsp" as "[#HΨi Hsp]"; first done.
iDestruct (big_sepS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done.
iAssert ( Ψ i Π★{set (I {[i]})} Ψ)%I as "[HΨ HΨ']" with "[HΨ]".
{ iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". }
iSplitL "HΨ' Hl Hsp"; [iNext|].
+ rewrite {2}/barrier_inv /=; iFrame "Hl".
iExists Ψ; iFrame "Hsp". by iIntros "> _".
+ iPoseProof (saved_prop_agree i Q (Ψ i)) "#" as "Heq"; first by iSplit.
+ iPoseProof (saved_prop_agree i Q (Ψ i) with "#") as "Heq"; first by iSplit.
iIntros "_". wp_op=> ?; simplify_eq/=; wp_if.
iPvsIntro. iApply "HΦ". iApply "HQR". by iRewrite "Heq".
Qed.
......@@ -176,7 +176,7 @@ Proof.
iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
iPvs (saved_prop_alloc_strong _ (R1: %CF iProp) I) as {i1} "[% #Hi1]".
iPvs (saved_prop_alloc_strong _ (R2: %CF iProp) (I {[i1]}))
as {i2} "[Hi2' #Hi2]"; iPure "Hi2'" as Hi2; iPvsIntro.
as {i2} "[Hi2' #Hi2]"; iDestruct "Hi2'" as %Hi2; iPvsIntro.
rewrite ->not_elem_of_union, elem_of_singleton in Hi2; destruct Hi2.
iExists (State p ({[i1]} ({[i2]} (I {[i]})))).
iExists ({[Change i1 ]} {[ Change i2 ]}).
......@@ -188,8 +188,9 @@ Proof.
sts_ownS γ (i_states i2) {[Change i2]})%I as "[Hγ1 Hγ2]" with "-".
{ iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
+ set_solver.
+ iApply sts_own_weaken "Hγ"; eauto using sts.closed_op, i_states_closed.
set_solver. }
+ iApply (sts_own_weaken with "Hγ");
eauto using sts.closed_op, i_states_closed.
abstract set_solver. }
iPvsIntro; iSplitL "Hγ1"; rewrite /recv /barrier_ctx.
+ iExists γ, P, R1, i1. iFrame "Hγ1 Hi1". repeat iSplit; auto.
by iIntros "> ?".
......@@ -205,8 +206,7 @@ Proof.
iIntros "> HQ". by iApply "HP"; iApply "HP1".
Qed.
Lemma recv_mono l P1 P2 :
P1 P2 recv l P1 recv l P2.
Lemma recv_mono l P1 P2 : P1 P2 recv l P1 recv l P2.
Proof.
intros HP%entails_wand. apply wand_entails. rewrite HP. apply recv_weaken.
Qed.
......
......@@ -5,8 +5,10 @@ Import uPred.
Definition newlock : val := λ: <>, ref #false.
Definition acquire : val :=
rec: "lock" "l" := if: CAS '"l" #false #true then #() else '"lock" '"l".
rec: "acquire" "l" :=
if: CAS '"l" #false #true then #() else '"acquire" '"l".
Definition release : val := λ: "l", '"l" <- #false.
Global Opaque newlock acquire release.
(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
......@@ -55,8 +57,8 @@ Proof.
iIntros {?} "(#Hh & HR & HΦ)". rewrite /newlock.
wp_seq. iApply wp_pvs. wp_alloc l as "Hl".
iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done.
iPvs (inv_alloc N _ (lock_inv γ l R)) "-[HΦ]" as "#?"; first done.
{ iNext. iExists false. by iFrame "Hl HR". }
iPvs (inv_alloc N _ (lock_inv γ l R) with "-[HΦ]") as "#?"; first done.
{ iIntros ">". iExists false. by iFrame "Hl HR". }
iPvsIntro. iApply "HΦ". iExists N, γ. by repeat iSplit.
Qed.
......@@ -65,23 +67,20 @@ Lemma acquire_spec l R (Φ : val → iProp) :
Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as {N γ} "(%&#?&#?)".
iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E.
iInv N as "Hinv". iDestruct "Hinv" as {b} "[Hl HR]"; destruct b.
iInv N as { [] } "[Hl HR]".
- wp_cas_fail. iSplitL "Hl".
+ iNext. iExists true. by iSplit.
+ wp_if. by iApply "IH".
- wp_cas_suc. iDestruct "HR" as "[Hγ HR]". iSplitL "Hl".
+ iNext. iExists true. by iSplit.
+ wp_if. iPvsIntro. iApply "HΦ" "-[HR] HR". iExists N, γ. by repeat iSplit.
+ wp_if. iApply ("HΦ" with "-[HR] HR"). iExists N, γ. by repeat iSplit.
Qed.
Lemma release_spec R l (Φ : val iProp) :
(locked l R R Φ #()) WP release #l {{ Φ }}.
Proof.
iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as {N γ} "(%&#?&#?&Hγ)".
rewrite /release. wp_let.
iInv N as "Hinv". iDestruct "Hinv" as {b} "[Hl Hγ']"; destruct b.
- wp_store. iFrame "HΦ". iNext. iExists false. by iFrame "Hl HR Hγ".
- wp_store. iDestruct "Hγ'" as "[Hγ' _]".
iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct own_valid "Hγ" as "%".
iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as {N γ} "(% & #? & #? & Hγ)".
rewrite /release. wp_let. iInv N as {b} "[Hl _]".
wp_store. iFrame "HΦ". iNext. iExists false. by iFrame "Hl HR Hγ".
Qed.
End proof.
......@@ -14,7 +14,7 @@ Infix "||" := Par : expr_scope.
Instance do_wexpr_par {X Y} (H : X `included` Y) : WExpr H par par := _.
Instance do_wsubst_par {X Y} x es (H : X `included` x :: Y) :
WSubst x es H par par := do_wsubst_closed _ x es H _.
Typeclasses Opaque par.
Global Opaque par.
Section proof.
Context {Σ : gFunctors} `{!heapG Σ, !spawnG Σ}.
......@@ -32,7 +32,7 @@ Proof.
iIntros {l} "Hl". wp_let. wp_proj. wp_focus (f2 _).
iApply wp_wand_l; iFrame "Hf2"; iIntros {v} "H2". wp_let.
wp_apply join_spec; iFrame "Hl". iIntros {w} "H1".
iSpecialize "HΦ" "-"; first by iSplitL "H1". by wp_let.
iSpecialize ("HΦ" with "* -"); first by iSplitL "H1". by wp_let.
Qed.
Lemma wp_par (Ψ1 Ψ2 : val iProp) (e1 e2 : expr []) (Φ : val iProp) :
......
......@@ -13,6 +13,7 @@ Definition join : val :=
InjR "x" => '"x"
| InjL <> => '"join" '"c"
end.
Global Opaque spawn join.
(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
......@@ -57,15 +58,15 @@ Lemma spawn_spec (Ψ : val → iProp) e (f : val) (Φ : val → iProp) :
WP spawn e {{ Φ }}.
Proof.
iIntros {<-%of_to_val ?} "(#Hh&Hf&HΦ)". rewrite /spawn.
wp_let; wp_alloc l as "Hl"; wp_let.
wp_let. wp_alloc l as "Hl". wp_let.
iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done.
iPvs (inv_alloc N _ (spawn_inv γ l Ψ)) "[Hl]" as "#?"; first done.
iPvs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done.
{ iNext. iExists (InjLV #0). iFrame "Hl". by iLeft. }
wp_apply wp_fork. iSplitR "Hf".
- wp_seq. iPvsIntro. iApply "HΦ"; rewrite /join_handle. iSplit; first done.
iExists γ. iFrame "Hγ"; by iSplit.
- wp_seq. iPvsIntro. iApply "HΦ"; rewrite /join_handle.
iSplit; first done. iExists γ. iFrame "Hγ"; by iSplit.
- wp_focus (f _). iApply wp_wand_l; iFrame "Hf"; iIntros {v} "Hv".
iInv N as "Hinv"; first wp_done; iDestruct "Hinv" as {v'} "[Hl _]".
iInv N as {v'} "[Hl _]"; first wp_done.
wp_store. iSplit; [iNext|done].
iExists (InjRV v); iFrame "Hl"; iRight; iExists v; iSplit; [done|by iLeft].
Qed.
......@@ -74,17 +75,16 @@ Lemma join_spec (Ψ : val → iProp) l (Φ : val → iProp) :
(join_handle l Ψ v, Ψ v - Φ v) WP join #l {{ Φ }}.
Proof.
rewrite /join_handle; iIntros "[[% H] Hv]"; iDestruct "H" as {γ} "(#?&Hγ&#?)".
iLöb as "IH". wp_rec. wp_focus (! _)%E.
iInv N as "Hinv"; iDestruct "Hinv" as {v} "[Hl Hinv]".
iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv N as {v} "[Hl Hinv]".
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- iSplitL "Hl"; [iNext; iExists _; iFrame "Hl"; by iLeft|].
wp_case. wp_seq. iApply "IH" "Hγ Hv".
wp_case. wp_seq. iApply ("IH" with "Hγ Hv").
- iDestruct "Hinv" as {v'} "[% [HΨ|Hγ']]"; subst.
+ iSplitL "Hl Hγ".
{ iNext. iExists _; iFrame "Hl"; iRight.
iExists _; iSplit; [done|by iRight]. }
wp_case. wp_let. iPvsIntro. by iApply "Hv".
+ iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct own_valid "Hγ" as "%".
+ iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].
Qed.
End proof.
......
From iris.program_logic Require Export ectx_weakestpre.
From iris.program_logic Require Import ownership. (* for ownP *)
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ownership ectx_lifting. (* for ownP *)
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import tactics.
From iris.proofmode Require Import weakestpre.
......@@ -86,22 +86,16 @@ Proof.
rewrite later_sep -(wp_value _ _ (Lit _)) //.
Qed.
Lemma wp_rec E f x e1 e2 v Φ :
to_val e2 = Some v
WP subst' x e2 (subst' f (Rec f x e1) e1) @ E {{ Φ }}
WP App (Rec f x e1) e2 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_head_step (App _ _)
(subst' x e2 (subst' f (Rec f x e1) e1)) None) //= ?right_id;
intros; inv_head_step; eauto.
Qed.
Lemma wp_rec' E f x erec e1 e2 v2 Φ :
Lemma wp_rec E f x erec e1 e2 v2 Φ :
e1 = Rec f x erec
to_val e2 = Some v2
WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }}
WP App e1 e2 @ E {{ Φ }}.
Proof. intros ->. apply wp_rec. Qed.
Proof.
intros -> ?. rewrite -(wp_lift_pure_det_head_step (App _ _)
(subst' x e2 (subst' f (Rec f x erec) erec)) None) //= ?right_id;
intros; inv_head_step; eauto.
Qed.
Lemma wp_un_op E op l l' Φ :
un_op_eval op l = Some l'
......
......@@ -33,7 +33,7 @@ Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : expr_scope.
Notation "' x" := (Var x) (at level 8, format "' x") : expr_scope.
Notation "^ v" := (of_val' v%V) (at level 8, format "^ v") : expr_scope.
Notation "^ e" := (wexpr' e) (at level 8, format "^ e") : expr_scope.
(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first. *)
......
......@@ -52,7 +52,7 @@ Lemma tac_wp_store Δ Δ' Δ'' N E i l v e v' Φ :
envs_simple_replace i false (Esnoc Enil i (l v')) Δ' = Some Δ''
Δ'' Φ (LitV LitUnit) Δ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Proof.
intros. eapply wp_store; eauto.
intros. rewrite -wp_store // -always_and_sep_l. apply and_intro; first done.
rewrite strip_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
......@@ -65,114 +65,134 @@ Lemma tac_wp_cas_fail Δ Δ' N E i l q v e1 v1 e2 v2 Φ :
Δ' Φ (LitV (LitBool false))
Δ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
intros. eapply wp_cas_fail; eauto.
intros. rewrite -wp_cas_fail // -always_and_sep_l. apply and_intro; first done.
rewrite strip_later_env_sound -later_sep envs_lookup_split //; simpl.
by apply later_mono, sep_mono_r, wand_mono.
Qed.
Lemma tac_wp_cas_suc Δ Δ' Δ'' N E i l e1 v1 e2 v2 Φ :
Lemma tac_wp_cas_suc Δ Δ' Δ'' N E i l v e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2
Δ heap_ctx N nclose N E
StripLaterEnvs Δ Δ'
envs_lookup i Δ' = Some (false, l v1)%I
envs_lookup i Δ' = Some (false, l v)%I v = v1
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ''
Δ'' Φ (LitV (LitBool true)) Δ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
intros. eapply wp_cas_suc; eauto.
intros; subst.
rewrite -wp_cas_suc // -always_and_sep_l. apply and_intro; first done.
rewrite strip_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
End heap.
Tactic Notation "wp_apply" open_constr(lem) :=
match goal with
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
wp_bind K; iApply lem; try iNext)
end.
Tactic Notation "wp_apply" open_constr(lem) constr(Hs) :=
match goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
wp_bind K; iApply lem Hs; try iNext)
| _ => fail "wp_apply: not a 'wp'"
end.
Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
match goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| Alloc ?e =>
wp_bind K; eapply tac_wp_alloc with _ _ H _;
[wp_done || fail 2 "wp_alloc:" e "not a value"
|iAssumption || fail 2 "wp_alloc: cannot find heap_ctx"
|done || eauto with ndisj
|apply _
|intros l; eexists; split;
[env_cbv; reflexivity || fail 2 "wp_alloc:" H "not fresh"
|wp_finish]]
end)
lazymatch goal with
| |- _ wp ?E ?e ?Q =>
first
[reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with Alloc _ => wp_bind K end)
|fail 1 "wp_alloc: cannot find 'Alloc' in" e];
eapply tac_wp_alloc with _ _ H _;
[let e' := match goal with |- to_val ?e' = _ => e' end in
wp_done || fail "wp_alloc:" e' "not a value"