Change the precedence of ⊢ to be the same as →, and the precedence of ⊣⊢ to

be the same as .

This is a fairly intrusive change, but at least makes notations more
consistent, and often shorter because fewer parentheses are needed. Note
parent d2b00f17
 ... ... @@ -136,7 +136,7 @@ Lemma to_agree_car n (x : agree A) : ✓{n} x → to_agree (x n) ≡{n}≡ x. Proof. intros [??]; split; naive_solver eauto using agree_valid_le. Qed. (** Internalized properties *) Lemma agree_equivI {M} a b : (to_agree a ≡ to_agree b) ⊣⊢ (a ≡ b : uPred M). Lemma agree_equivI {M} a b : to_agree a ≡ to_agree b ⊣⊢ (a ≡ b : uPred M). Proof. uPred.unseal. do 2 split. by intros [? Hv]; apply (Hv n). apply: to_agree_ne. Qed. ... ...
 ... ... @@ -164,14 +164,14 @@ Canonical Structure authUR := (** Internalized properties *) Lemma auth_equivI {M} (x y : auth A) : (x ≡ y) ⊣⊢ (authoritative x ≡ authoritative y ∧ own x ≡ own y : uPred M). x ≡ y ⊣⊢ (authoritative x ≡ authoritative y ∧ own x ≡ own y : uPred M). Proof. by uPred.unseal. Qed. Lemma auth_validI {M} (x : auth A) : (✓ x) ⊣⊢ (match authoritative x with | Excl' a => (∃ b, a ≡ own x ⋅ b) ∧ ✓ a | None => ✓ own x | ExclBot' => False end : uPred M). ✓ x ⊣⊢ (match authoritative x with | Excl' a => (∃ b, a ≡ own x ⋅ b) ∧ ✓ a | None => ✓ own x | ExclBot' => False end : uPred M). Proof. uPred.unseal. by destruct x as [[[]|]]. Qed. Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b. ... ...
 ... ... @@ -236,22 +236,22 @@ Proof. rewrite /Persistent /=. inversion_clear 1; by repeat constructor. Qed. (** Internalized properties *) Lemma csum_equivI {M} (x y : csum A B) : (x ≡ y) ⊣⊢ (match x, y with | Cinl a, Cinl a' => a ≡ a' | Cinr b, Cinr b' => b ≡ b' | CsumBot, CsumBot => True | _, _ => False end : uPred M). x ≡ y ⊣⊢ (match x, y with | Cinl a, Cinl a' => a ≡ a' | Cinr b, Cinr b' => b ≡ b' | CsumBot, CsumBot => True | _, _ => False end : uPred M). Proof. uPred.unseal; do 2 split; first by destruct 1. by destruct x, y; try destruct 1; try constructor. Qed. Lemma csum_validI {M} (x : csum A B) : (✓ x) ⊣⊢ (match x with | Cinl a => ✓ a | Cinr b => ✓ b | CsumBot => False end : uPred M). ✓ x ⊣⊢ (match x with | Cinl a => ✓ a | Cinr b => ✓ b | CsumBot => False end : uPred M). Proof. uPred.unseal. by destruct x. Qed. (** Updates *) ... ...
 ... ... @@ -102,11 +102,11 @@ Proof. split. apply _. by intros []. Qed. (** Internalized properties *) Lemma excl_equivI {M} (x y : excl A) : (x ≡ y) ⊣⊢ (match x, y with | Excl a, Excl b => a ≡ b | ExclBot, ExclBot => True | _, _ => False end : uPred M). x ≡ y ⊣⊢ (match x, y with | Excl a, Excl b => a ≡ b | ExclBot, ExclBot => True | _, _ => False end : uPred M). Proof. uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor. Qed. ... ...
 ... ... @@ -153,7 +153,7 @@ Proof. intros. by apply frac_validN_inv_l with 0 y, cmra_valid_validN. Qed. (** Internalized properties *) Lemma frac_equivI {M} (x y : frac A) : (x ≡ y) ⊣⊢ (frac_perm x = frac_perm y ∧ frac_car x ≡ frac_car y : uPred M). x ≡ y ⊣⊢ (frac_perm x = frac_perm y ∧ frac_car x ≡ frac_car y : uPred M). Proof. by uPred.unseal. Qed. Lemma frac_validI {M} (x : frac A) : ✓ x ⊣⊢ (■ (frac_perm x ≤ 1)%Qc ∧ ✓ frac_car x : uPred M). ... ...
 ... ... @@ -171,9 +171,9 @@ Canonical Structure gmapUR := UCMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin gmap_ucmra_mixin. (** Internalized properties *) Lemma gmap_equivI {M} m1 m2 : (m1 ≡ m2) ⊣⊢ (∀ i, m1 !! i ≡ m2 !! i : uPred M). Lemma gmap_equivI {M} m1 m2 : m1 ≡ m2 ⊣⊢ (∀ i, m1 !! i ≡ m2 !! i : uPred M). Proof. by uPred.unseal. Qed. Lemma gmap_validI {M} m : (✓ m) ⊣⊢ (∀ i, ✓ (m !! i) : uPred M). Lemma gmap_validI {M} m : ✓ m ⊣⊢ (∀ i, ✓ (m !! i) : uPred M). Proof. by uPred.unseal. Qed. End cmra. ... ...
 ... ... @@ -139,9 +139,9 @@ Section iprod_cmra. UCMRAT (iprod B) iprod_cofe_mixin iprod_cmra_mixin iprod_ucmra_mixin. (** Internalized properties *) Lemma iprod_equivI {M} g1 g2 : (g1 ≡ g2) ⊣⊢ (∀ i, g1 i ≡ g2 i : uPred M). Lemma iprod_equivI {M} g1 g2 : g1 ≡ g2 ⊣⊢ (∀ i, g1 i ≡ g2 i : uPred M). Proof. by uPred.unseal. Qed. Lemma iprod_validI {M} g : (✓ g) ⊣⊢ (∀ i, ✓ g i : uPred M). Lemma iprod_validI {M} g : ✓ g ⊣⊢ (∀ i, ✓ g i : uPred M). Proof. by uPred.unseal. Qed. (** Properties of iprod_insert. *) ... ...
 ... ... @@ -227,9 +227,9 @@ Section cmra. Qed. (** Internalized properties *) Lemma list_equivI {M} l1 l2 : (l1 ≡ l2) ⊣⊢ (∀ i, l1 !! i ≡ l2 !! i : uPred M). Lemma list_equivI {M} l1 l2 : l1 ≡ l2 ⊣⊢ (∀ i, l1 !! i ≡ l2 !! i : uPred M). Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed. Lemma list_validI {M} l : (✓ l) ⊣⊢ (∀ i, ✓ (l !! i) : uPred M). Lemma list_validI {M} l : ✓ l ⊣⊢ (∀ i, ✓ (l !! i) : uPred M). Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed. End cmra. ... ...
 ... ... @@ -196,22 +196,22 @@ Proof. rewrite /Persistent /=. inversion_clear 1; by repeat constructor. Qed. (** Internalized properties *) Lemma one_shot_equivI {M} (x y : one_shot A) : (x ≡ y) ⊣⊢ (match x, y with | OneShotPending, OneShotPending => True | Shot a, Shot b => a ≡ b | OneShotBot, OneShotBot => True | _, _ => False end : uPred M). x ≡ y ⊣⊢ (match x, y with | OneShotPending, OneShotPending => True | Shot a, Shot b => a ≡ b | OneShotBot, OneShotBot => True | _, _ => False end : uPred M). Proof. uPred.unseal; do 2 split; first by destruct 1. by destruct x, y; try destruct 1; try constructor. Qed. Lemma one_shot_validI {M} (x : one_shot A) : (✓ x) ⊣⊢ (match x with | Shot a => ✓ a | OneShotBot => False | _ => True end : uPred M). ✓ x ⊣⊢ (match x with | Shot a => ✓ a | OneShotBot => False | _ => True end : uPred M). Proof. uPred.unseal. by destruct x. Qed. (** Updates *) ... ...
This diff is collapsed.
 ... ... @@ -83,9 +83,9 @@ Proof. - etrans; eauto. Qed. Lemma big_and_app Ps Qs : [∧] (Ps ++ Qs) ⊣⊢ ([∧] Ps ∧ [∧] Qs). Lemma big_and_app Ps Qs : [∧] (Ps ++ Qs) ⊣⊢ [∧] Ps ∧ [∧] Qs. Proof. induction Ps as [|?? IH]; by rewrite /= ?left_id -?assoc ?IH. Qed. Lemma big_sep_app Ps Qs : [★] (Ps ++ Qs) ⊣⊢ ([★] Ps ★ [★] Qs). Lemma big_sep_app Ps Qs : [★] (Ps ++ Qs) ⊣⊢ [★] Ps ★ [★] Qs. Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed. Lemma big_and_contains Ps Qs : Qs `contains` Ps → [∧] Ps ⊢ [∧] Qs. ... ... @@ -113,7 +113,7 @@ Section gmap. Lemma big_sepM_mono Φ Ψ m1 m2 : m2 ⊆ m1 → (∀ k x, m2 !! k = Some x → Φ k x ⊢ Ψ k x) → ([★ map] k ↦ x ∈ m1, Φ k x) ⊢ ([★ map] k ↦ x ∈ m2, Ψ k x). ([★ map] k ↦ x ∈ m1, Φ k x) ⊢ [★ map] k ↦ x ∈ m2, Ψ k x. Proof. intros HX HΦ. trans ([★ map] k↦x ∈ m2, Φ k x)%I. - by apply big_sep_contains, fmap_contains, map_to_list_contains. ... ... @@ -152,12 +152,12 @@ Section gmap. Lemma big_sepM_insert Φ m i x : m !! i = None → ([★ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ (Φ i x ★ [★ map] k↦y ∈ m, Φ k y). ([★ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ Φ i x ★ [★ map] k↦y ∈ m, Φ k y. Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed. Lemma big_sepM_delete Φ m i x : m !! i = Some x → ([★ map] k↦y ∈ m, Φ k y) ⊣⊢ (Φ i x ★ [★ map] k↦y ∈ delete i m, Φ k y). ([★ map] k↦y ∈ m, Φ k y) ⊣⊢ Φ i x ★ [★ map] k↦y ∈ delete i m, Φ k y. Proof. intros. rewrite -big_sepM_insert ?lookup_delete //. by rewrite insert_delete insert_id. ... ... @@ -204,7 +204,7 @@ Section gmap. Lemma big_sepM_sepM Φ Ψ m : ([★ map] k↦x ∈ m, Φ k x ★ Ψ k x) ⊣⊢ (([★ map] k↦x ∈ m, Φ k x) ★ ([★ map] k↦x ∈ m, Ψ k x)). ⊣⊢ ([★ map] k↦x ∈ m, Φ k x) ★ ([★ map] k↦x ∈ m, Ψ k x). Proof. rewrite /uPred_big_sepM. induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //. ... ... @@ -212,7 +212,7 @@ Section gmap. Qed. Lemma big_sepM_later Φ m : (▷ [★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, ▷ Φ k x). ▷ ([★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, ▷ Φ k x). Proof. rewrite /uPred_big_sepM. induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //. ... ... @@ -228,7 +228,7 @@ Section gmap. Qed. Lemma big_sepM_always_if p Φ m : (□?p [★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, □?p Φ k x). □?p ([★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, □?p Φ k x). Proof. destruct p; simpl; auto using big_sepM_always. Qed. Lemma big_sepM_forall Φ m : ... ... @@ -249,7 +249,7 @@ Section gmap. Qed. Lemma big_sepM_impl Φ Ψ m : (□ (∀ k x, m !! k = Some x → Φ k x → Ψ k x) ∧ [★ map] k↦x ∈ m, Φ k x) □ (∀ k x, m !! k = Some x → Φ k x → Ψ k x) ∧ ([★ map] k↦x ∈ m, Φ k x) ⊢ [★ map] k↦x ∈ m, Ψ k x. Proof. rewrite always_and_sep_l. do 2 setoid_rewrite always_forall. ... ... @@ -267,7 +267,7 @@ Section gset. Lemma big_sepS_mono Φ Ψ X Y : Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊢ Ψ x) → ([★ set] x ∈ X, Φ x) ⊢ ([★ set] x ∈ Y, Ψ x). ([★ set] x ∈ X, Φ x) ⊢ [★ set] x ∈ Y, Ψ x. Proof. intros HX HΦ. trans ([★ set] x ∈ Y, Φ x)%I. - by apply big_sep_contains, fmap_contains, elements_contains. ... ... @@ -315,7 +315,7 @@ Section gset. Proof. apply (big_sepS_fn_insert (λ y, id)). Qed. Lemma big_sepS_delete Φ X x : x ∈ X → ([★ set] y ∈ X, Φ y) ⊣⊢ (Φ x ★ [★ set] y ∈ X ∖ {[ x ]}, Φ y). x ∈ X → ([★ set] y ∈ X, Φ y) ⊣⊢ Φ x ★ [★ set] y ∈ X ∖ {[ x ]}, Φ y. Proof. intros. rewrite -big_sepS_insert; last set_solver. by rewrite -union_difference_L; last set_solver. ... ... @@ -328,21 +328,21 @@ Section gset. Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed. Lemma big_sepS_sepS Φ Ψ X : ([★ set] y ∈ X, Φ y ★ Ψ y) ⊣⊢ (([★ set] y ∈ X, Φ y) ★ [★ set] y ∈ X, Ψ y). ([★ set] y ∈ X, Φ y ★ Ψ y) ⊣⊢ ([★ set] y ∈ X, Φ y) ★ ([★ set] y ∈ X, Ψ y). Proof. rewrite /uPred_big_sepS. induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id. by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _ ★ _)%I]comm -!assoc. Qed. Lemma big_sepS_later Φ X : (▷ [★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, ▷ Φ y). Lemma big_sepS_later Φ X : ▷ ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, ▷ Φ y). Proof. rewrite /uPred_big_sepS. induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True. by rewrite later_sep IH. Qed. Lemma big_sepS_always Φ X : (□ [★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □ Φ y). Lemma big_sepS_always Φ X : □ ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □ Φ y). Proof. rewrite /uPred_big_sepS. induction (elements X) as [|x l IH]; csimpl; first by rewrite ?always_const. ... ... @@ -350,7 +350,7 @@ Section gset. Qed. Lemma big_sepS_always_if q Φ X : (□?q [★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □?q Φ y). □?q ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □?q Φ y). Proof. destruct q; simpl; auto using big_sepS_always. Qed. Lemma big_sepS_forall Φ X : ... ... @@ -369,7 +369,7 @@ Section gset. Qed. Lemma big_sepS_impl Φ Ψ X : (□ (∀ x, ■ (x ∈ X) → Φ x → Ψ x) ∧ [★ set] x ∈ X, Φ x) ⊢ [★ set] x ∈ X, Ψ x. □ (∀ x, ■ (x ∈ X) → Φ x → Ψ x) ∧ ([★ set] x ∈ X, Φ x) ⊢ [★ set] x ∈ X, Ψ x. Proof. rewrite always_and_sep_l always_forall. setoid_rewrite always_impl; setoid_rewrite always_const. ... ...
 ... ... @@ -86,7 +86,7 @@ Module uPred_reflection. Section uPred_reflection. Qed. Lemma cancel_entails Σ e1 e2 e1' e2' ns : cancel ns e1 = Some e1' → cancel ns e2 = Some e2' → eval Σ e1' ⊢ eval Σ e2' → eval Σ e1 ⊢ eval Σ e2. (eval Σ e1' ⊢ eval Σ e2') → eval Σ e1 ⊢ eval Σ e2. Proof. intros ??. rewrite !eval_flatten. rewrite (flatten_cancel e1 e1' ns) // (flatten_cancel e2 e2' ns) //; csimpl. ... ...
 ... ... @@ -77,8 +77,8 @@ Proof. solve_proper. Qed. (** Helper lemmas *) Lemma ress_split i i1 i2 Q R1 R2 P I : i ∈ I → i1 ∉ I → i2 ∉ I → i1 ≠ i2 → (saved_prop_own i Q ★ saved_prop_own i1 R1 ★ saved_prop_own i2 R2 ★ (Q -★ R1 ★ R2) ★ ress P I) saved_prop_own i Q ★ saved_prop_own i1 R1 ★ saved_prop_own i2 R2 ★ (Q -★ R1 ★ R2) ★ ress P I ⊢ ress P ({[i1;i2]} ∪ I ∖ {[i]}). Proof. iIntros {????} "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as {Ψ} "[HPΨ HΨ]". ... ... @@ -97,7 +97,7 @@ Qed. (** Actual proofs *) Lemma newbarrier_spec (P : iProp) (Φ : val → iProp) : heapN ⊥ N → (heap_ctx heapN ★ ∀ l, recv l P ★ send l P -★ Φ #l) heap_ctx heapN ★ (∀ l, recv l P ★ send l P -★ Φ #l) ⊢ WP newbarrier #() {{ Φ }}. Proof. iIntros {HN} "[#? HΦ]". ... ... @@ -124,7 +124,7 @@ Proof. Qed. Lemma signal_spec l P (Φ : val → iProp) : (send l P ★ P ★ Φ #()) ⊢ WP signal #l {{ Φ }}. send l P ★ P ★ Φ #() ⊢ WP signal #l {{ Φ }}. Proof. rewrite /signal /send /barrier_ctx. iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as {γ} "[#(%&Hh&Hsts) Hγ]". wp_let. ... ... @@ -139,7 +139,7 @@ Proof. Qed. Lemma wait_spec l P (Φ : val → iProp) : (recv l P ★ (P -★ Φ #())) ⊢ WP wait #l {{ Φ }}. recv l P ★ (P -★ Φ #()) ⊢ WP wait #l {{ Φ }}. Proof. rename P into R; rewrite /recv /barrier_ctx. iIntros "[Hr HΦ]"; iDestruct "Hr" as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)". ... ... @@ -200,7 +200,7 @@ Proof. by iIntros "> ?". Qed. Lemma recv_weaken l P1 P2 : (P1 -★ P2) ⊢ (recv l P1 -★ recv l P2). Lemma recv_weaken l P1 P2 : (P1 -★ P2) ⊢ recv l P1 -★ recv l P2. Proof. rewrite /recv. iIntros "HP HP1"; iDestruct "HP1" as {γ P Q i} "(#Hctx&Hγ&Hi&HP1)". ... ... @@ -208,7 +208,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. ... ...
 ... ... @@ -17,7 +17,7 @@ Lemma barrier_spec (heapN N : namespace) : (∀ l P, {{ send l P ★ P }} signal #l {{ _, True }}) ∧ (∀ 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, (P -★ Q) ⊢ (recv l P -★ recv l Q)). (∀ l P Q, (P -★ Q) ⊢ recv l P -★ recv l Q). Proof. intros HN. exists (λ l, CofeMor (recv heapN N l)), (λ l, CofeMor (send heapN N l)). ... ...
 ... ... @@ -51,8 +51,7 @@ Qed. Lemma newlock_spec N (R : iProp) Φ : heapN ⊥ N → (heap_ctx heapN ★ R ★ (∀ l, is_lock l R -★ Φ #l)) ⊢ WP newlock #() {{ Φ }}. heap_ctx heapN ★ R ★ (∀ l, is_lock l R -★ Φ #l) ⊢ WP newlock #() {{ Φ }}. Proof. iIntros {?} "(#Hh & HR & HΦ)". rewrite /newlock. wp_seq. iApply wp_pvs. wp_alloc l as "Hl". ... ... @@ -63,7 +62,7 @@ Proof. Qed. Lemma acquire_spec l R (Φ : val → iProp) : (is_lock l R ★ (locked l R -★ R -★ Φ #())) ⊢ WP acquire #l {{ Φ }}. is_lock l R ★ (locked l R -★ R -★ Φ #()) ⊢ WP acquire #l {{ Φ }}. Proof. iIntros "[Hl HΦ]". iDestruct "Hl" as {N γ} "(%&#?&#?)". iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E. ... ... @@ -77,7 +76,7 @@ Proof. Qed. Lemma release_spec R l (Φ : val → iProp) : (locked l R ★ R ★ Φ #()) ⊢ WP release #l {{ Φ }}. locked l R ★ R ★ Φ #() ⊢ WP release #l {{ Φ }}. Proof. iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as {N γ} "(% & #? & #? & Hγ)". rewrite /release. wp_let. iInv N as {b} "[Hl _]". ... ...
 ... ... @@ -54,7 +54,7 @@ Proof. solve_proper. Qed. Lemma spawn_spec (Ψ : val → iProp) e (f : val) (Φ : val → iProp) : to_val e = Some f → heapN ⊥ N → (heap_ctx heapN ★ WP f #() {{ Ψ }} ★ ∀ l, join_handle l Ψ -★ Φ #l) heap_ctx heapN ★ WP f #() {{ Ψ }} ★ (∀ l, join_handle l Ψ -★ Φ #l) ⊢ WP spawn e {{ Φ }}. Proof. iIntros {<-%of_to_val ?} "(#Hh&Hf&HΦ)". rewrite /spawn. ... ... @@ -72,7 +72,7 @@ Proof. Qed. Lemma join_spec (Ψ : val → iProp) l (Φ : val → iProp) : (join_handle l Ψ ★ ∀ v, Ψ v -★ Φ v) ⊢ WP join #l {{ Φ }}. 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 {v} "[Hl Hinv]". ... ...
 ... ... @@ -18,11 +18,11 @@ Proof. by rewrite /SepDestruct heap_mapsto_op_split. Qed. Lemma tac_wp_alloc Δ Δ' N E j e v Φ : to_val e = Some v → Δ ⊢ heap_ctx N → nclose N ⊆ E → (Δ ⊢ heap_ctx N) → nclose N ⊆ E → StripLaterEnvs Δ Δ' → (∀ l, ∃ Δ'', envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧ Δ'' ⊢ Φ (LitV (LitLoc l))) → (Δ'' ⊢ Φ (LitV (LitLoc l)))) → Δ ⊢ WP Alloc e @ E {{ Φ }}. Proof. intros ???? HΔ. rewrite -wp_alloc // -always_and_sep_l. ... ... @@ -33,10 +33,10 @@ Proof. Qed. Lemma tac_wp_load Δ Δ' N E i l q v Φ : Δ ⊢ heap_ctx N → nclose N ⊆ E → (Δ ⊢ heap_ctx N) → nclose N ⊆ E → StripLaterEnvs Δ Δ' → envs_lookup i Δ' = Some (false, l ↦{q} v)%I → Δ' ⊢ Φ v → (Δ' ⊢ Φ v) → Δ ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}. Proof. intros. rewrite -wp_load // -always_and_sep_l. apply and_intro; first done. ... ... @@ -46,11 +46,11 @@ Qed. Lemma tac_wp_store Δ Δ' Δ'' N E i l v e v' Φ : to_val e = Some v' → Δ ⊢ heap_ctx N → nclose N ⊆ E → (Δ ⊢ heap_ctx N) → nclose N ⊆ E → StripLaterEnvs Δ Δ' → envs_lookup i Δ' = Some (false, l ↦ v)%I → envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' → Δ'' ⊢ Φ (LitV LitUnit) → Δ ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}. (Δ'' ⊢ Φ (LitV LitUnit)) → Δ ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}. Proof. 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. ... ... @@ -59,10 +59,10 @@ Qed. Lemma tac_wp_cas_fail Δ Δ' N E i l q v e1 v1 e2 v2 Φ : to_val e1 = Some v1 → to_val e2 = Some v2 → Δ ⊢ heap_ctx N → nclose N ⊆ E → (Δ ⊢ heap_ctx N) → nclose N ⊆ E → StripLaterEnvs Δ Δ' → envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 → Δ' ⊢ Φ (LitV (LitBool false)) → (Δ' ⊢ Φ (LitV (LitBool false))) → Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}. Proof. intros. rewrite -wp_cas_fail // -always_and_sep_l. apply and_intro; first done. ... ... @@ -72,11 +72,11 @@ Qed. 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 → (Δ ⊢ heap_ctx N) → nclose N ⊆ E → StripLaterEnvs Δ Δ' → 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 {{ Φ }}. (Δ'' ⊢ Φ (LitV (LitBool true))) → Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}. Proof. intros; subst. rewrite -wp_cas_suc // -always_and_sep_l. apply and_intro; first done. ... ...
 ... ... @@ -56,7 +56,7 @@ Proof. by rewrite -Permutation_middle /= big_op_app. Qed. Lemma wp_adequacy_steps P Φ k n e1 t2 σ1 σ2 r1 : P ⊢ WP e1 {{ Φ }} → (P ⊢ WP e1 {{ Φ }}) → nsteps step k ([e1],σ1) (t2,σ2) → 1 < n → wsat (k + n) ⊤ σ1 r1 → P (k + n) r1 → ... ... @@ -70,7 +70,7 @@ Qed. Lemma wp_adequacy_own Φ e1 t2 σ1 m σ2 : ✓ m → (ownP σ1 ★ ownG m) ⊢ WP e1 {{ Φ }} → (ownP σ1 ★ ownG m ⊢ WP e1 {{ Φ }}) → rtc step ([e1],σ1) (t2,σ2) → ∃ rs2 Φs', wptp 2 t2 (Φ :: Φs') rs2 ∧ wsat 2 ⊤ σ2 (big_op rs2). Proof. ... ... @@ -85,7 +85,7 @@ Qed. Theorem wp_adequacy_result E φ e v t2 σ1 m σ2 : ✓ m → (ownP σ1 ★ ownG m) ⊢ WP e @ E {{ v', ■ φ v' }} → (ownP σ1 ★ ownG m ⊢ WP e @ E {{ v', ■ φ v' }}) → rtc step ([e], σ1) (of_val v :: t2, σ2) → φ v. Proof. ... ... @@ -111,7 +111,7 @@ Qed. Lemma wp_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2 : ✓ m → (ownP σ1 ★ ownG m) ⊢ WP e1 @ E {{ Φ }} → (ownP σ1 ★ ownG m ⊢ WP e1 @ E {{ Φ }}) → rtc step ([e1], σ1) (t2, σ2) → e2 ∈ t2 → (is_Some (to_val e2) ∨ reducible e2 σ2). Proof. ... ... @@ -129,7 +129,7 @@ Qed. (* Connect this up to the threadpool-semantics. *) Theorem wp_adequacy_safe E Φ e1 t2 σ1 m σ2 : ✓ m → (ownP σ1 ★ ownG m) ⊢ WP e1 @ E {{ Φ }} → (ownP σ1 ★ ownG m ⊢ WP e1 @ E {{ Φ }}) → rtc step ([e1], σ1) (t2, σ2) → Forall (λ e, is_Some (to_val e)) t2 ∨ ∃ t3 σ3, step (t2, σ2) (t3, σ3). Proof. ... ...
 ... ... @@ -75,7 +75,8 @@ Section auth. ✓ a → nclose N ⊆ E → ▷ φ a ={E}=> ∃ γ, auth_ctx γ N φ ∧ auth_own γ a. Proof. iIntros {??} "Hφ". iPvs (auth_alloc_strong N E a ∅ with "Hφ") as {γ} "[_ ?]"; [done..|]. iIntros {??} "Hφ". iPvs (auth_alloc_strong N E a ∅ with "Hφ") as {γ} "[_ ?]"; [done..|]. by iExists γ. Qed. ... ... @@ -86,7 +87,7 @@ Section auth. Lemma auth_fsa E N (Ψ : V → iPropG Λ Σ) γ a : fsaV → nclose N ⊆ E → (auth_ctx γ N φ ★ ▷ auth_own γ a ★ ∀ a', auth_ctx γ N φ ★ ▷ auth_own γ a ★ (∀ a', ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★ fsa (E ∖ nclose N) (λ x, ∃ L Lv (Hup : LocalUpdate Lv L), ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★ ... ... @@ -111,11 +112,11 @@ Section auth. Lemma auth_fsa' L `{!LocalUpdate Lv L} E N (Ψ : V → iPropG Λ Σ) γ a : fsaV → nclose N ⊆ E → (auth_ctx γ N φ ★ ▷ auth_own γ a ★ (∀ a', auth_ctx γ N φ ★ ▷ auth_own γ a ★ (∀ a', ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★ fsa (E ∖ nclose N) (λ x, ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★ (auth_own γ (L a) -★ Ψ x)))) (auth_own γ (L a) -★ Ψ x))) ⊢ fsa E Ψ. Proof. iIntros {??} "(#Ha & Hγf & HΨ)"; iApply (auth_fsa E N Ψ γ a); auto. ... ...
 ... ... @@ -61,7 +61,7 @@ Instance box_own_auth_timeless γ Proof. apply own_timeless, pair_timeless; apply _. Qed. Lemma box_own_auth_agree γ b1 b2 : (box_own_auth γ (● Excl' b1) ★ box_own_auth γ (◯ Excl' b2)) ⊢ (b1 = b2). box_own_auth γ (● Excl' b1) ★ box_own_auth γ (◯ Excl' b2) ⊢ b1 =