Commit 274209c2 authored by Robbert Krebbers's avatar Robbert Krebbers Committed by Ralf Jung

Make nclose an explicit coercion.

We do this by introducing a type class UpClose with notation ↑.

The reason for this change is as follows: since `nclose : namespace
→ coPset` is declared as a coercion, the notation `nclose N ⊆ E` was
pretty printed as `N ⊆ E`. However, `N ⊆ E` could not be typechecked
because type checking goes from left to right, and as such would look
for an instance `SubsetEq namespace`, which causes the right hand side
to be ill-typed.
parent f072ab70
...@@ -128,10 +128,10 @@ Section auth. ...@@ -128,10 +128,10 @@ Section auth.
Qed. Qed.
Lemma auth_open E N γ a : Lemma auth_open E N γ a :
nclose N E N E
auth_ctx γ N f φ auth_own γ a ={E,EN}= t, auth_ctx γ N f φ auth_own γ a ={E,EN}= t,
a f t φ t u b, a f t φ t u b,
(f t, a) ~l~> (f u, b) φ u ={EN,E}= auth_own γ b. (f t, a) ~l~> (f u, b) φ u ={EN,E}= auth_own γ b.
Proof. Proof.
iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose". iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
(* The following is essentially a very trivial composition of the accessors (* The following is essentially a very trivial composition of the accessors
......
...@@ -105,7 +105,7 @@ Proof. ...@@ -105,7 +105,7 @@ Proof.
Qed. Qed.
Lemma box_delete E f P Q γ : Lemma box_delete E f P Q γ :
nclose N E N E
f !! γ = Some false f !! γ = Some false
slice N γ Q box N f P ={E}= P', slice N γ Q box N f P ={E}= P',
(P (Q P')) box N (delete γ f) P'. (P (Q P')) box N (delete γ f) P'.
...@@ -125,7 +125,7 @@ Proof. ...@@ -125,7 +125,7 @@ Proof.
Qed. Qed.
Lemma box_fill E f γ P Q : Lemma box_fill E f γ P Q :
nclose N E N E
f !! γ = Some false f !! γ = Some false
slice N γ Q Q box N f P ={E}= box N (<[γ:=true]> f) P. slice N γ Q Q box N f P ={E}= box N (<[γ:=true]> f) P.
Proof. Proof.
...@@ -144,7 +144,7 @@ Proof. ...@@ -144,7 +144,7 @@ Proof.
Qed. Qed.
Lemma box_empty E f P Q γ : Lemma box_empty E f P Q γ :
nclose N E N E
f !! γ = Some true f !! γ = Some true
slice N γ Q box N f P ={E}= Q box N (<[γ:=false]> f) P. slice N γ Q box N f P ={E}= Q box N (<[γ:=false]> f) P.
Proof. Proof.
...@@ -164,7 +164,7 @@ Proof. ...@@ -164,7 +164,7 @@ Proof.
Qed. Qed.
Lemma box_fill_all E f P : Lemma box_fill_all E f P :
nclose N E N E
box N f P P ={E}= box N (const true <$> f) P. box N f P P ={E}= box N (const true <$> f) P.
Proof. Proof.
iIntros (?) "[H HP]"; iDestruct "H" as (Φ) "[#HeqP Hf]". iIntros (?) "[H HP]"; iDestruct "H" as (Φ) "[#HeqP Hf]".
...@@ -181,7 +181,7 @@ Proof. ...@@ -181,7 +181,7 @@ Proof.
Qed. Qed.
Lemma box_empty_all E f P : Lemma box_empty_all E f P :
nclose N E N E
map_Forall (λ _, (true =)) f map_Forall (λ _, (true =)) f
box N f P ={E}= P box N (const false <$> f) P. box N f P ={E}= P box N (const false <$> f) P.
Proof. Proof.
......
...@@ -51,8 +51,7 @@ Section proofs. ...@@ -51,8 +51,7 @@ Section proofs.
iMod (inv_alloc N _ (P own γ 1%Qp)%I with "[HP]"); eauto. iMod (inv_alloc N _ (P own γ 1%Qp)%I with "[HP]"); eauto.
Qed. Qed.
Lemma cinv_cancel E N γ P : Lemma cinv_cancel E N γ P : N E cinv N γ P cinv_own γ 1 ={E}= P.
nclose N E cinv N γ P cinv_own γ 1 ={E}= P.
Proof. Proof.
rewrite /cinv. iIntros (?) "#Hinv Hγ". rewrite /cinv. iIntros (?) "#Hinv Hγ".
iInv N as "[$|>Hγ']" "Hclose"; first iApply "Hclose"; eauto. iInv N as "[$|>Hγ']" "Hclose"; first iApply "Hclose"; eauto.
...@@ -60,8 +59,8 @@ Section proofs. ...@@ -60,8 +59,8 @@ Section proofs.
Qed. Qed.
Lemma cinv_open E N γ p P : Lemma cinv_open E N γ p P :
nclose N E N E
cinv N γ P cinv_own γ p ={E,EN}= P cinv_own γ p ( P ={EN,E}= True). cinv N γ P cinv_own γ p ={E,EN}= P cinv_own γ p ( P ={E∖↑N,E}= True).
Proof. Proof.
rewrite /cinv. iIntros (?) "#Hinv Hγ". rewrite /cinv. iIntros (?) "#Hinv Hγ".
iInv N as "[$|>Hγ']" "Hclose". iInv N as "[$|>Hγ']" "Hclose".
......
...@@ -6,7 +6,7 @@ Import uPred. ...@@ -6,7 +6,7 @@ Import uPred.
(** Derived forms and lemmas about them. *) (** Derived forms and lemmas about them. *)
Definition inv_def `{invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ := Definition inv_def `{invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
( i, i nclose N ownI i P)%I. ( i, i N ownI i P)%I.
Definition inv_aux : { x | x = @inv_def }. by eexists. Qed. Definition inv_aux : { x | x = @inv_def }. by eexists. Qed.
Definition inv {Σ i} := proj1_sig inv_aux Σ i. Definition inv {Σ i} := proj1_sig inv_aux Σ i.
Definition inv_eq : @inv = @inv_def := proj2_sig inv_aux. Definition inv_eq : @inv = @inv_def := proj2_sig inv_aux.
...@@ -30,8 +30,8 @@ Proof. rewrite inv_eq /inv; apply _. Qed. ...@@ -30,8 +30,8 @@ Proof. rewrite inv_eq /inv; apply _. Qed.
Lemma inv_alloc N E P : P ={E}= inv N P. Lemma inv_alloc N E P : P ={E}= inv N P.
Proof. Proof.
rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros "HP [Hw $]". rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros "HP [Hw $]".
iMod (ownI_alloc ( nclose N) P with "[HP Hw]") as (i) "(% & $ & ?)"; auto. iMod (ownI_alloc ( N) P with "[HP Hw]") as (i) "(% & $ & ?)"; auto.
- intros Ef. exists (coPpick (nclose N coPset.of_gset Ef)). - intros Ef. exists (coPpick ( N coPset.of_gset Ef)).
rewrite -coPset.elem_of_of_gset comm -elem_of_difference. rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
apply coPpick_elem_of=> Hfin. apply coPpick_elem_of=> Hfin.
eapply nclose_infinite, (difference_finite_inv _ _), Hfin. eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
...@@ -41,19 +41,19 @@ Proof. ...@@ -41,19 +41,19 @@ Proof.
Qed. Qed.
Lemma inv_open E N P : Lemma inv_open E N P :
nclose N E inv N P ={E,EN}= P ( P ={EN,E}= True). N E inv N P ={E,E∖↑N}= P ( P ={E∖↑N,E}= True).
Proof. Proof.
rewrite inv_eq /inv_def fupd_eq /fupd_def; iDestruct 1 as (i) "[Hi #HiP]". rewrite inv_eq /inv_def fupd_eq /fupd_def; iDestruct 1 as (i) "[Hi #HiP]".
iDestruct "Hi" as % ?%elem_of_subseteq_singleton. iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
rewrite {1 4}(union_difference_L (nclose N) E) // ownE_op; last set_solver. rewrite {1 4}(union_difference_L ( N) E) // ownE_op; last set_solver.
rewrite {1 5}(union_difference_L {[ i ]} (nclose N)) // ownE_op; last set_solver. rewrite {1 5}(union_difference_L {[ i ]} ( N)) // ownE_op; last set_solver.
iIntros "(Hw & [HE $] & $) !> !>". iIntros "(Hw & [HE $] & $) !> !>".
iDestruct (ownI_open i P with "[$Hw $HE $HiP]") as "($ & $ & HD)". iDestruct (ownI_open i P with "[$Hw $HE $HiP]") as "($ & $ & HD)".
iIntros "HP [Hw $] !> !>". iApply ownI_close; by iFrame. iIntros "HP [Hw $] !> !>". iApply ownI_close; by iFrame.
Qed. Qed.
Lemma inv_open_timeless E N P `{!TimelessP P} : Lemma inv_open_timeless E N P `{!TimelessP P} :
nclose N E inv N P ={E,EN}= P (P ={EN,E}= True). N E inv N P ={E,E∖↑N}= P (P ={E∖↑N,E}= True).
Proof. Proof.
iIntros (?) "Hinv". iMod (inv_open with "Hinv") as "[>HP Hclose]"; auto. iIntros (?) "Hinv". iMod (inv_open with "Hinv") as "[>HP Hclose]"; auto.
iIntros "!> {$HP} HP". iApply "Hclose"; auto. iIntros "!> {$HP} HP". iApply "Hclose"; auto.
......
...@@ -16,7 +16,7 @@ Definition ndot_eq : @ndot = @ndot_def := proj2_sig ndot_aux. ...@@ -16,7 +16,7 @@ Definition ndot_eq : @ndot = @ndot_def := proj2_sig ndot_aux.
Definition nclose_def (N : namespace) : coPset := coPset_suffixes (encode N). Definition nclose_def (N : namespace) : coPset := coPset_suffixes (encode N).
Definition nclose_aux : { x | x = @nclose_def }. by eexists. Qed. Definition nclose_aux : { x | x = @nclose_def }. by eexists. Qed.
Coercion nclose := proj1_sig nclose_aux. Instance nclose : UpClose namespace coPset := proj1_sig nclose_aux.
Definition nclose_eq : @nclose = @nclose_def := proj2_sig nclose_aux. Definition nclose_eq : @nclose = @nclose_def := proj2_sig nclose_aux.
Infix ".@" := ndot (at level 19, left associativity) : C_scope. Infix ".@" := ndot (at level 19, left associativity) : C_scope.
...@@ -27,31 +27,34 @@ Instance ndisjoint : Disjoint namespace := λ N1 N2, nclose N1 ⊥ nclose N2. ...@@ -27,31 +27,34 @@ Instance ndisjoint : Disjoint namespace := λ N1 N2, nclose N1 ⊥ nclose N2.
Section namespace. Section namespace.
Context `{Countable A}. Context `{Countable A}.
Implicit Types x y : A. Implicit Types x y : A.
Implicit Types N : namespace.
Implicit Types E : coPset.
Global Instance ndot_inj : Inj2 (=) (=) (=) (@ndot A _ _). Global Instance ndot_inj : Inj2 (=) (=) (=) (@ndot A _ _).
Proof. intros N1 x1 N2 x2; rewrite !ndot_eq=> ?; by simplify_eq. Qed. Proof. intros N1 x1 N2 x2; rewrite !ndot_eq=> ?; by simplify_eq. Qed.
Lemma nclose_nroot : nclose nroot = . Lemma nclose_nroot : nroot = .
Proof. rewrite nclose_eq. by apply (sig_eq_pi _). Qed. Proof. rewrite nclose_eq. by apply (sig_eq_pi _). Qed.
Lemma encode_nclose N : encode N nclose N. Lemma encode_nclose N : encode N N.
Proof. Proof.
rewrite nclose_eq. rewrite nclose_eq.
by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _). by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _).
Qed. Qed.
Lemma nclose_subseteq N x : nclose (N .@ x) nclose N. Lemma nclose_subseteq N x : N .@ x (N : coPset).
Proof. Proof.
intros p; rewrite nclose_eq /nclose !ndot_eq !elem_coPset_suffixes. intros p; rewrite nclose_eq /nclose !ndot_eq !elem_coPset_suffixes.
intros [q ->]. destruct (list_encode_suffix N (ndot_def N x)) as [q' ?]. intros [q ->]. destruct (list_encode_suffix N (ndot_def N x)) as [q' ?].
{ by exists [encode x]. } { by exists [encode x]. }
by exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal. by exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal.
Qed. Qed.
Lemma nclose_subseteq' E N x : nclose N E nclose (N .@ x) E.
Lemma nclose_subseteq' E N x : N E N .@ x E.
Proof. intros. etrans; eauto using nclose_subseteq. Qed. Proof. intros. etrans; eauto using nclose_subseteq. Qed.
Lemma ndot_nclose N x : encode (N .@ x) nclose N. Lemma ndot_nclose N x : encode (N .@ x) N.
Proof. apply nclose_subseteq with x, encode_nclose. Qed. Proof. apply nclose_subseteq with x, encode_nclose. Qed.
Lemma nclose_infinite N : ¬set_finite (nclose N). Lemma nclose_infinite N : ¬set_finite ( N : coPset).
Proof. rewrite nclose_eq. apply coPset_suffixes_infinite. Qed. Proof. rewrite nclose_eq. apply coPset_suffixes_infinite. Qed.
Lemma ndot_ne_disjoint N x y : x y N .@ x N .@ y. Lemma ndot_ne_disjoint N x y : x y N .@ x N .@ y.
...@@ -61,19 +64,18 @@ Section namespace. ...@@ -61,19 +64,18 @@ Section namespace.
revert Hqy. by intros [= ?%encode_inj]%list_encode_suffix_eq. revert Hqy. by intros [= ?%encode_inj]%list_encode_suffix_eq.
Qed. Qed.
Lemma ndot_preserve_disjoint_l N E x : nclose N E nclose (N .@ x) E. Lemma ndot_preserve_disjoint_l N E x : N E N .@ x E.
Proof. intros. pose proof (nclose_subseteq N x). set_solver. Qed. Proof. intros. pose proof (nclose_subseteq N x). set_solver. Qed.
Lemma ndot_preserve_disjoint_r N E x : E nclose N E nclose (N .@ x). Lemma ndot_preserve_disjoint_r N E x : E N E N .@ x.
Proof. intros. by apply symmetry, ndot_preserve_disjoint_l. Qed. Proof. intros. by apply symmetry, ndot_preserve_disjoint_l. Qed.
Lemma ndisj_subseteq_difference N E F : Lemma ndisj_subseteq_difference N E F : E N E F E F N.
E nclose N E F E F nclose N.
Proof. set_solver. Qed. Proof. set_solver. Qed.
End namespace. End namespace.
(* The hope is that registering these will suffice to solve most goals (* The hope is that registering these will suffice to solve most goals
of the form [N1 ⊥ N2] and those of the form [N1 ⊆ E ∖ N2 ∖ .. ∖ Nn]. *) of the form [N1 ⊥ N2] and those of the form [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn]. *)
Hint Resolve ndisj_subseteq_difference : ndisj. Hint Resolve ndisj_subseteq_difference : ndisj.
Hint Extern 0 (_ _) => apply ndot_ne_disjoint; congruence : ndisj. Hint Extern 0 (_ _) => apply ndot_ne_disjoint; congruence : ndisj.
Hint Resolve ndot_preserve_disjoint_l : ndisj. Hint Resolve ndot_preserve_disjoint_l : ndisj.
......
...@@ -117,10 +117,10 @@ Section sts. ...@@ -117,10 +117,10 @@ Section sts.
Proof. by apply sts_accS. Qed. Proof. by apply sts_accS. Qed.
Lemma sts_openS E N γ S T : Lemma sts_openS E N γ S T :
nclose N E N E
sts_ctx γ N φ sts_ownS γ S T ={E,EN}= s, sts_ctx γ N φ sts_ownS γ S T ={E,EN}= s,
s S φ s s' T', s S φ s s' T',
sts.steps (s, T) (s', T') φ s' ={EN,E}= sts_own γ s' T'. sts.steps (s, T) (s', T') φ s' ={EN,E}= sts_own γ s' T'.
Proof. Proof.
iIntros (?) "[#? Hγf]". rewrite /sts_ctx. iInv N as "Hinv" "Hclose". iIntros (?) "[#? Hγf]". rewrite /sts_ctx. iInv N as "Hinv" "Hclose".
(* The following is essentially a very trivial composition of the accessors (* The following is essentially a very trivial composition of the accessors
...@@ -135,9 +135,9 @@ Section sts. ...@@ -135,9 +135,9 @@ Section sts.
Qed. Qed.
Lemma sts_open E N γ s0 T : Lemma sts_open E N γ s0 T :
nclose N E N E
sts_ctx γ N φ sts_own γ s0 T ={E,EN}= s, sts_ctx γ N φ sts_own γ s0 T ={E,EN}= s,
sts.frame_steps T s0 s φ s s' T', sts.frame_steps T s0 s φ s s' T',
sts.steps (s, T) (s', T') φ s' ={EN,E}= sts_own γ s' T'. sts.steps (s, T) (s', T') φ s' ={EN,E}= sts_own γ s' T'.
Proof. by apply sts_openS. Qed. Proof. by apply sts_openS. Qed.
End sts. End sts.
...@@ -16,7 +16,7 @@ Section defs. ...@@ -16,7 +16,7 @@ Section defs.
own tid (CoPset E, ). own tid (CoPset E, ).
Definition tl_inv (tid : thread_id) (N : namespace) (P : iProp Σ) : iProp Σ := Definition tl_inv (tid : thread_id) (N : namespace) (P : iProp Σ) : iProp Σ :=
( i, i nclose N ( i, i N
inv tlN (P own tid (, GSet {[i]}) tl_own tid {[i]}))%I. inv tlN (P own tid (, GSet {[i]}) tl_own tid {[i]}))%I.
End defs. End defs.
...@@ -57,8 +57,8 @@ Section proofs. ...@@ -57,8 +57,8 @@ Section proofs.
iMod (own_empty (prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty". iMod (own_empty (prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty".
iMod (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]". iMod (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
{ apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)). { apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)).
apply (gset_disj_alloc_empty_updateP_strong' (λ i, i nclose N)). apply (gset_disj_alloc_empty_updateP_strong' (λ i, i N)).
intros Ef. exists (coPpick (nclose N coPset.of_gset Ef)). intros Ef. exists (coPpick ( N coPset.of_gset Ef)).
rewrite -coPset.elem_of_of_gset comm -elem_of_difference. rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
apply coPpick_elem_of=> Hfin. apply coPpick_elem_of=> Hfin.
eapply nclose_infinite, (difference_finite_inv _ _), Hfin. eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
...@@ -70,14 +70,14 @@ Section proofs. ...@@ -70,14 +70,14 @@ Section proofs.
Qed. Qed.
Lemma tl_inv_open tid tlE E N P : Lemma tl_inv_open tid tlE E N P :
nclose tlN tlE nclose N E tlN tlE N E
tl_inv tid N P tl_own tid E ={tlE}= P tl_own tid (E N) tl_inv tid N P tl_own tid E ={tlE}= P tl_own tid (E∖↑N)
( P tl_own tid (E N) ={tlE}= tl_own tid E). ( P tl_own tid (E∖↑N) ={tlE}= tl_own tid E).
Proof. Proof.
rewrite /tl_inv. iIntros (??) "#Htlinv Htoks". rewrite /tl_inv. iIntros (??) "#Htlinv Htoks".
iDestruct "Htlinv" as (i) "[% Hinv]". iDestruct "Htlinv" as (i) "[% Hinv]".
rewrite {1 4}(union_difference_L (nclose N) E) //. rewrite {1 4}(union_difference_L (N) E) //.
rewrite {1 5}(union_difference_L {[i]} (nclose N)) ?tl_own_union; [|set_solver..]. rewrite {1 5}(union_difference_L {[i]} (N)) ?tl_own_union; [|set_solver..].
iDestruct "Htoks" as "[[Htoki $] $]". iDestruct "Htoks" as "[[Htoki $] $]".
iInv tlN as "[[$ >Hdis]|>Htoki2]" "Hclose". iInv tlN as "[[$ >Hdis]|>Htoki2]" "Hclose".
- iMod ("Hclose" with "[Htoki]") as "_"; first auto. - iMod ("Hclose" with "[Htoki]") as "_"; first auto.
......
...@@ -69,13 +69,13 @@ Proof. ...@@ -69,13 +69,13 @@ Proof.
Qed. Qed.
Lemma vs_inv N E P Q R : Lemma vs_inv N E P Q R :
nclose N E inv N R ( R P ={E nclose N}=> R Q) P ={E}=> Q. N E inv N R ( R P ={E∖↑N}=> R Q) P ={E}=> Q.
Proof. Proof.
iIntros (?) "#[? Hvs] !# HP". iInv N as "HR" "Hclose". iIntros (?) "#[? Hvs] !# HP". iInv N as "HR" "Hclose".
iMod ("Hvs" with "[HR HP]") as "[? $]"; first by iFrame. iMod ("Hvs" with "[HR HP]") as "[? $]"; first by iFrame.
by iApply "Hclose". by iApply "Hclose".
Qed. Qed.
Lemma vs_alloc N P : P ={N}=> inv N P. Lemma vs_alloc N P : P ={N}=> inv N P.
Proof. iIntros "!# HP". by iApply inv_alloc. Qed. Proof. iIntros "!# HP". by iApply inv_alloc. Qed.
End vs. End vs.
...@@ -130,7 +130,7 @@ Section heap. ...@@ -130,7 +130,7 @@ Section heap.
(** Weakest precondition *) (** Weakest precondition *)
Lemma wp_alloc E e v : Lemma wp_alloc E e v :
to_val e = Some v nclose heapN E to_val e = Some v heapN E
{{{ heap_ctx }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l v }}}. {{{ heap_ctx }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l v }}}.
Proof. Proof.
iIntros (<-%of_to_val ? Φ) "#Hinv HΦ". rewrite /heap_ctx. iIntros (<-%of_to_val ? Φ) "#Hinv HΦ". rewrite /heap_ctx.
...@@ -144,7 +144,7 @@ Section heap. ...@@ -144,7 +144,7 @@ Section heap.
Qed. Qed.
Lemma wp_load E l q v : Lemma wp_load E l q v :
nclose heapN E heapN E
{{{ heap_ctx l {q} v }}} Load (Lit (LitLoc l)) @ E {{{ heap_ctx l {q} v }}} Load (Lit (LitLoc l)) @ E
{{{ RET v; l {q} v }}}. {{{ RET v; l {q} v }}}.
Proof. Proof.
...@@ -157,7 +157,7 @@ Section heap. ...@@ -157,7 +157,7 @@ Section heap.
Qed. Qed.
Lemma wp_store E l v' e v : Lemma wp_store E l v' e v :
to_val e = Some v nclose heapN E to_val e = Some v heapN E
{{{ heap_ctx l v' }}} Store (Lit (LitLoc l)) e @ E {{{ heap_ctx l v' }}} Store (Lit (LitLoc l)) e @ E
{{{ RET LitV LitUnit; l v }}}. {{{ RET LitV LitUnit; l v }}}.
Proof. Proof.
...@@ -173,7 +173,7 @@ Section heap. ...@@ -173,7 +173,7 @@ Section heap.
Qed. Qed.
Lemma wp_cas_fail E l q v' e1 v1 e2 v2 : Lemma wp_cas_fail E l q v' e1 v1 e2 v2 :
to_val e1 = Some v1 to_val e2 = Some v2 v' v1 nclose heapN E to_val e1 = Some v1 to_val e2 = Some v2 v' v1 heapN E
{{{ heap_ctx l {q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E {{{ heap_ctx l {q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
{{{ RET LitV (LitBool false); l {q} v' }}}. {{{ RET LitV (LitBool false); l {q} v' }}}.
Proof. Proof.
...@@ -186,7 +186,7 @@ Section heap. ...@@ -186,7 +186,7 @@ Section heap.
Qed. Qed.
Lemma wp_cas_suc E l e1 v1 e2 v2 : Lemma wp_cas_suc E l e1 v1 e2 v2 :
to_val e1 = Some v1 to_val e2 = Some v2 nclose heapN E to_val e1 = Some v1 to_val e2 = Some v2 heapN E
{{{ heap_ctx l v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E {{{ heap_ctx l v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
{{{ RET LitV (LitBool true); l v2 }}}. {{{ RET LitV (LitBool true); l v2 }}}.
Proof. Proof.
......
...@@ -162,7 +162,7 @@ Proof. ...@@ -162,7 +162,7 @@ Proof.
Qed. Qed.
Lemma recv_split E l P1 P2 : Lemma recv_split E l P1 P2 :
nclose N E recv l (P1 P2) ={E}= recv l P1 recv l P2. N E recv l (P1 P2) ={E}= recv l P1 recv l P2.
Proof. Proof.
rename P1 into R1; rename P2 into R2. rewrite {1}/recv /barrier_ctx. rename P1 into R1; rename P2 into R2. rewrite {1}/recv /barrier_ctx.
iIntros (?). iDestruct 1 as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)". iIntros (?). iDestruct 1 as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
......
...@@ -14,7 +14,7 @@ Lemma barrier_spec (N : namespace) : ...@@ -14,7 +14,7 @@ Lemma barrier_spec (N : namespace) :
{{ v, l : loc, v = #l recv l P send l P }}) {{ v, l : loc, v = #l recv l P send l P }})
( l P, {{ send l P P }} signal #l {{ _, True }}) ( l P, {{ send l P P }} signal #l {{ _, True }})
( l P, {{ recv l P }} wait #l {{ _, P }}) ( l P, {{ recv l P }} wait #l {{ _, P }})
( l P Q, recv l (P Q) ={N}=> recv l P recv l Q) ( l P Q, recv l (P Q) ={N}=> recv l P recv l Q)
( l P Q, (P - Q) recv l P - recv l Q). ( l P Q, (P - Q) recv l P - recv l Q).
Proof. Proof.
intros HN. intros HN.
......
...@@ -18,7 +18,7 @@ Proof. by rewrite /IntoAnd heap_mapsto_op_eq Qp_div_2. Qed. ...@@ -18,7 +18,7 @@ Proof. by rewrite /IntoAnd heap_mapsto_op_eq Qp_div_2. Qed.
Lemma tac_wp_alloc Δ Δ' E j e v Φ : Lemma tac_wp_alloc Δ Δ' E j e v Φ :
to_val e = Some v to_val e = Some v
(Δ heap_ctx) nclose heapN E (Δ heap_ctx) heapN E
IntoLaterEnvs Δ Δ' IntoLaterEnvs Δ Δ'
( l, Δ'', ( l, Δ'',
envs_app false (Esnoc Enil j (l v)) Δ' = Some Δ'' envs_app false (Esnoc Enil j (l v)) Δ' = Some Δ''
...@@ -33,7 +33,7 @@ Proof. ...@@ -33,7 +33,7 @@ Proof.
Qed. Qed.
Lemma tac_wp_load Δ Δ' E i l q v Φ : Lemma tac_wp_load Δ Δ' E i l q v Φ :
(Δ heap_ctx) nclose heapN E (Δ heap_ctx) heapN E
IntoLaterEnvs Δ Δ' IntoLaterEnvs Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I envs_lookup i Δ' = Some (false, l {q} v)%I
(Δ' Φ v) (Δ' Φ v)
...@@ -47,7 +47,7 @@ Qed. ...@@ -47,7 +47,7 @@ Qed.
Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ : Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ :
to_val e = Some v' to_val e = Some v'
(Δ heap_ctx) nclose heapN E (Δ heap_ctx) heapN E
IntoLaterEnvs Δ Δ' IntoLaterEnvs Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I envs_lookup i Δ' = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v')) Δ' = Some Δ'' envs_simple_replace i false (Esnoc Enil i (l v')) Δ' = Some Δ''
...@@ -62,7 +62,7 @@ Qed. ...@@ -62,7 +62,7 @@ Qed.
Lemma tac_wp_cas_fail Δ Δ' E i l q v e1 v1 e2 v2 Φ : Lemma tac_wp_cas_fail Δ Δ' E i l q v e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2 to_val e1 = Some v1 to_val e2 = Some v2
(Δ heap_ctx) nclose heapN E (Δ heap_ctx) heapN E
IntoLaterEnvs Δ Δ' IntoLaterEnvs Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I v v1 envs_lookup i Δ' = Some (false, l {q} v)%I v v1
(Δ' Φ (LitV (LitBool false))) (Δ' Φ (LitV (LitBool false)))
...@@ -76,7 +76,7 @@ Qed. ...@@ -76,7 +76,7 @@ Qed.
Lemma tac_wp_cas_suc Δ Δ' Δ'' E i l v e1 v1 e2 v2 Φ : Lemma tac_wp_cas_suc Δ Δ' Δ'' E i l v e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2 to_val e1 = Some v1 to_val e2 = Some v2
(Δ heap_ctx) nclose heapN E (Δ heap_ctx) heapN E
IntoLaterEnvs Δ Δ' IntoLaterEnvs Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I v = v1 envs_lookup i Δ' = Some (false, l v)%I v = v1