Commit 086cc92c authored by Robbert Krebbers's avatar Robbert Krebbers

Use round braces instead of curly braces in proof mode tactics.

The intropattern {H} also meant clear (both in ssreflect, and the logic
part of the introduction pattern).
parent 6d2e61e1
...@@ -153,13 +153,13 @@ Section heap. ...@@ -153,13 +153,13 @@ Section heap.
to_val e = Some v nclose N E to_val e = Some v nclose N E
heap_ctx N ( l, l v ={E}= Φ (LitV (LitLoc l))) WP Alloc e @ E {{ Φ }}. heap_ctx N ( l, l v ={E}= Φ (LitV (LitLoc l))) WP Alloc e @ E {{ Φ }}.
Proof. Proof.
iIntros {??} "[#Hinv HΦ]". rewrite /heap_ctx. iIntros (??) "[#Hinv HΦ]". rewrite /heap_ctx.
iPvs (auth_empty heap_name) as "Hheap". iPvs (auth_empty heap_name) as "Hheap".
iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto. iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
iFrame "Hinv Hheap". iIntros {h}. rewrite left_id. iFrame "Hinv Hheap". iIntros (h). rewrite left_id.
iIntros "[% Hheap]". rewrite /heap_inv. iIntros "[% Hheap]". rewrite /heap_inv.
iApply wp_alloc_pst; first done. iFrame "Hheap". iNext. iApply wp_alloc_pst; first done. iFrame "Hheap". iNext.
iIntros {l} "[% Hheap]"; iPvsIntro; iExists {[ l := (1%Qp, DecAgree v) ]}. iIntros (l) "[% Hheap]"; iPvsIntro; iExists {[ l := (1%Qp, DecAgree v) ]}.
rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None. rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None.
iFrame "Hheap". iSplitR; first iPureIntro. iFrame "Hheap". iSplitR; first iPureIntro.
{ by apply alloc_unit_singleton_local_update; first apply of_heap_None. } { by apply alloc_unit_singleton_local_update; first apply of_heap_None. }
...@@ -171,10 +171,10 @@ Section heap. ...@@ -171,10 +171,10 @@ Section heap.
heap_ctx N l {q} v (l {q} v ={E}= Φ v) heap_ctx N l {q} v (l {q} v ={E}= Φ v)
WP Load (Lit (LitLoc l)) @ E {{ Φ }}. WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Proof. Proof.
iIntros {?} "[#Hh [Hl HΦ]]". iIntros (?) "[#Hh [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def. rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto. iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv. iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert. iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
rewrite of_heap_singleton_op //. iFrame "Hl". rewrite of_heap_singleton_op //. iFrame "Hl".
iIntros "> Hown". iPvsIntro. iExists _; iSplit; first done. iIntros "> Hown". iPvsIntro. iExists _; iSplit; first done.
...@@ -186,10 +186,10 @@ Section heap. ...@@ -186,10 +186,10 @@ Section heap.
heap_ctx N l v' (l v ={E}= Φ (LitV LitUnit)) heap_ctx N l v' (l v ={E}= Φ (LitV LitUnit))
WP Store (Lit (LitLoc l)) e @ E {{ Φ }}. WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Proof. Proof.
iIntros {??} "[#Hh [Hl HΦ]]". iIntros (??) "[#Hh [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def. rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto. iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv. iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //. iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl". rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
iIntros "> Hown". iPvsIntro. iExists {[l := (1%Qp, DecAgree v)]}; iSplit. iIntros "> Hown". iPvsIntro. iExists {[l := (1%Qp, DecAgree v)]}; iSplit.
...@@ -202,10 +202,10 @@ Section heap. ...@@ -202,10 +202,10 @@ Section heap.
heap_ctx N l {q} v' (l {q} v' ={E}= Φ (LitV (LitBool false))) heap_ctx N l {q} v' (l {q} v' ={E}= Φ (LitV (LitBool false)))
WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}. WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof. Proof.
iIntros {????} "[#Hh [Hl HΦ]]". iIntros (????) "[#Hh [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def. rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10. iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10.
iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv. iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //. iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
rewrite of_heap_singleton_op //. iFrame "Hl". rewrite of_heap_singleton_op //. iFrame "Hl".
iIntros "> Hown". iPvsIntro. iExists _; iSplit; first done. iIntros "> Hown". iPvsIntro. iExists _; iSplit; first done.
...@@ -217,10 +217,10 @@ Section heap. ...@@ -217,10 +217,10 @@ Section heap.
heap_ctx N l v1 (l v2 ={E}= Φ (LitV (LitBool true))) heap_ctx N l v1 (l v2 ={E}= Φ (LitV (LitBool true)))
WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}. WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof. Proof.
iIntros {???} "[#Hh [Hl HΦ]]". iIntros (???) "[#Hh [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def. rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10. iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10.
iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv. iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //. iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //.
rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl". rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
iIntros "> Hown". iPvsIntro. iExists {[l := (1%Qp, DecAgree v2)]}; iSplit. iIntros "> Hown". iPvsIntro. iExists {[l := (1%Qp, DecAgree v2)]}; iSplit.
......
...@@ -81,7 +81,7 @@ Lemma ress_split i i1 i2 Q R1 R2 P I : ...@@ -81,7 +81,7 @@ Lemma ress_split i i1 i2 Q R1 R2 P I :
(Q - R1 R2) ress P I (Q - R1 R2) ress P I
ress P ({[i1;i2]} I {[i]}). ress P ({[i1;i2]} I {[i]}).
Proof. Proof.
iIntros {????} "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as {Ψ} "[HPΨ HΨ]". iIntros (????) "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as (Ψ) "[HPΨ HΨ]".
iDestruct (big_sepS_delete _ _ i with "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Ψ". iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ".
- iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by iSplit. - iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by iSplit.
...@@ -99,12 +99,12 @@ Lemma newbarrier_spec (P : iProp) (Φ : val → iProp) : ...@@ -99,12 +99,12 @@ Lemma newbarrier_spec (P : iProp) (Φ : val → iProp) :
heap_ctx heapN ( l, recv l P send l P - Φ #l) heap_ctx heapN ( l, recv l P send l P - Φ #l)
WP newbarrier #() {{ Φ }}. WP newbarrier #() {{ Φ }}.
Proof. Proof.
iIntros {HN} "[#? HΦ]". iIntros (HN) "[#? HΦ]".
rewrite /newbarrier. wp_seq. wp_alloc l as "Hl". rewrite /newbarrier. wp_seq. wp_alloc l as "Hl".
iApply "HΦ". iApply "HΦ".
iPvs (saved_prop_alloc (F:=idCF) _ P) as {γ} "#?". iPvs (saved_prop_alloc (F:=idCF) _ P) as (γ) "#?".
iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]") iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
as {γ'} "[#? Hγ']"; eauto. as (γ') "[#? Hγ']"; eauto.
{ iNext. rewrite /barrier_inv /=. iFrame. { iNext. rewrite /barrier_inv /=. iFrame.
iExists (const P). rewrite !big_sepS_singleton /=. eauto. } iExists (const P). rewrite !big_sepS_singleton /=. eauto. }
iAssert (barrier_ctx γ' l P)%I as "#?". iAssert (barrier_ctx γ' l P)%I as "#?".
...@@ -125,14 +125,14 @@ Lemma signal_spec l P (Φ : val → iProp) : ...@@ -125,14 +125,14 @@ Lemma signal_spec l P (Φ : val → iProp) :
send l P P Φ #() WP signal #l {{ Φ }}. send l P P Φ #() WP signal #l {{ Φ }}.
Proof. Proof.
rewrite /signal /send /barrier_ctx. rewrite /signal /send /barrier_ctx.
iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as {γ} "[#(%&Hh&Hsts) Hγ]". wp_let. iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as (γ) "[#(%&Hh&Hsts) Hγ]". wp_let.
iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]". iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
wp_store. iPvsIntro. destruct p; [|done]. wp_store. iPvsIntro. destruct p; [|done].
iExists (State High I), ( : set token). iExists (State High I), ( : set token).
iSplit; [iPureIntro; by eauto using signal_step|]. iSplit; [iPureIntro; by eauto using signal_step|].
iSplitR "HΦ"; [iNext|by auto]. iSplitR "HΦ"; [iNext|by auto].
rewrite {2}/barrier_inv /ress /=; iFrame "Hl". rewrite {2}/barrier_inv /ress /=; iFrame "Hl".
iDestruct "Hr" as {Ψ} "[Hr Hsp]"; iExists Ψ; iFrame "Hsp". iDestruct "Hr" as (Ψ) "[Hr Hsp]"; iExists Ψ; iFrame "Hsp".
iIntros "> _"; by iApply "Hr". iIntros "> _"; by iApply "Hr".
Qed. Qed.
...@@ -140,7 +140,7 @@ Lemma wait_spec l P (Φ : val → iProp) : ...@@ -140,7 +140,7 @@ Lemma wait_spec l P (Φ : val → iProp) :
recv l P (P - Φ #()) WP wait #l {{ Φ }}. recv l P (P - Φ #()) WP wait #l {{ Φ }}.
Proof. Proof.
rename P into R; rewrite /recv /barrier_ctx. rename P into R; rewrite /recv /barrier_ctx.
iIntros "[Hr HΦ]"; iDestruct "Hr" as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)". iIntros "[Hr HΦ]"; iDestruct "Hr" as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
iLöb as "IH". wp_rec. wp_focus (! _)%E. iLöb as "IH". wp_rec. wp_focus (! _)%E.
iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]". iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
wp_load. iPvsIntro. destruct p. wp_load. iPvsIntro. destruct p.
...@@ -155,7 +155,7 @@ Proof. ...@@ -155,7 +155,7 @@ Proof.
return to the client *) return to the client *)
iExists (State High (I {[ i ]})), ( : set token). iExists (State High (I {[ i ]})), ( : set token).
iSplit; [iPureIntro; by eauto using wait_step|]. iSplit; [iPureIntro; by eauto using wait_step|].
iDestruct "Hr" as {Ψ} "[HΨ Hsp]". iDestruct "Hr" as (Ψ) "[HΨ Hsp]".
iDestruct (big_sepS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done. iDestruct (big_sepS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done.
iAssert ( Ψ i [ set] j I {[i]}, Ψ j)%I with "[HΨ]" as "[HΨ HΨ']". iAssert ( Ψ i [ set] j I {[i]}, Ψ j)%I with "[HΨ]" as "[HΨ HΨ']".
{ iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". } { iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". }
...@@ -171,12 +171,12 @@ Lemma recv_split E l P1 P2 : ...@@ -171,12 +171,12 @@ Lemma recv_split E l P1 P2 :
nclose N E recv l (P1 P2) ={E}=> recv l P1 recv l P2. nclose 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)".
iApply pvs_trans'. iApply pvs_trans'.
iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]". 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 _ (R1: %CF iProp) I) as (i1) "[% #Hi1]".
iPvs (saved_prop_alloc_strong _ (R2: %CF iProp) (I {[i1]})) iPvs (saved_prop_alloc_strong _ (R2: %CF iProp) (I {[i1]}))
as {i2} "[Hi2' #Hi2]"; iDestruct "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. rewrite ->not_elem_of_union, elem_of_singleton in Hi2; destruct Hi2.
iExists (State p ({[i1; i2]} I {[i]})). iExists (State p ({[i1; i2]} I {[i]})).
iExists ({[Change i1; Change i2 ]}). iExists ({[Change i1; Change i2 ]}).
...@@ -199,7 +199,7 @@ Qed. ...@@ -199,7 +199,7 @@ 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. Proof.
rewrite /recv. rewrite /recv.
iIntros "HP HP1"; iDestruct "HP1" as {γ P Q i} "(#Hctx&Hγ&Hi&HP1)". iIntros "HP HP1"; iDestruct "HP1" as (γ P Q i) "(#Hctx&Hγ&Hi&HP1)".
iExists γ, P, Q, i. iFrame "Hctx Hγ Hi". iExists γ, P, Q, i. iFrame "Hctx Hγ Hi".
iIntros "> HQ". by iApply "HP"; iApply "HP1". iIntros "> HQ". by iApply "HP"; iApply "HP1".
Qed. Qed.
......
...@@ -22,9 +22,9 @@ Proof. ...@@ -22,9 +22,9 @@ Proof.
intros HN. intros HN.
exists (λ l, CofeMor (recv heapN N l)), (λ l, CofeMor (send heapN N l)). exists (λ l, CofeMor (recv heapN N l)), (λ l, CofeMor (send heapN N l)).
split_and?; simpl. split_and?; simpl.
- iIntros {P} "#? ! _". iApply (newbarrier_spec _ _ P); eauto. - iIntros (P) "#? ! _". iApply (newbarrier_spec _ _ P); eauto.
- iIntros {l P} "! [Hl HP]". by iApply signal_spec; iFrame "Hl HP". - iIntros (l P) "! [Hl HP]". by iApply signal_spec; iFrame "Hl HP".
- iIntros {l P} "! Hl". iApply wait_spec; iFrame "Hl"; eauto. - iIntros (l P) "! Hl". iApply wait_spec; iFrame "Hl"; eauto.
- intros; by apply recv_split. - intros; by apply recv_split.
- apply recv_weaken. - apply recv_weaken.
Qed. Qed.
......
...@@ -38,9 +38,9 @@ Lemma newcounter_spec N (R : iProp) Φ : ...@@ -38,9 +38,9 @@ Lemma newcounter_spec N (R : iProp) Φ :
heapN N heapN N
heap_ctx heapN ( l, counter l 0 - Φ #l) WP newcounter #() {{ Φ }}. heap_ctx heapN ( l, counter l 0 - Φ #l) WP newcounter #() {{ Φ }}.
Proof. Proof.
iIntros {?} "[#Hh HΦ]". rewrite /newcounter. wp_seq. wp_alloc l as "Hl". iIntros (?) "[#Hh HΦ]". rewrite /newcounter. wp_seq. wp_alloc l as "Hl".
iPvs (auth_alloc (counter_inv l) N _ (O:mnat) with "[Hl]") iPvs (auth_alloc (counter_inv l) N _ (O:mnat) with "[Hl]")
as {γ} "[#? Hγ]"; try by auto. as (γ) "[#? Hγ]"; try by auto.
iPvsIntro. iApply "HΦ". rewrite /counter; eauto 10. iPvsIntro. iApply "HΦ". rewrite /counter; eauto 10.
Qed. Qed.
...@@ -48,13 +48,13 @@ Lemma inc_spec l j (Φ : val → iProp) : ...@@ -48,13 +48,13 @@ Lemma inc_spec l j (Φ : val → iProp) :
counter l j (counter l (S j) - Φ #()) WP inc #l {{ Φ }}. counter l j (counter l (S j) - Φ #()) WP inc #l {{ Φ }}.
Proof. Proof.
iIntros "[Hl HΦ]". iLöb as "IH". wp_rec. iIntros "[Hl HΦ]". iLöb as "IH". wp_rec.
iDestruct "Hl" as {N γ} "(% & #? & #Hγ & Hγf)". iDestruct "Hl" as (N γ) "(% & #? & #Hγ & Hγf)".
wp_focus (! _)%E; iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto. wp_focus (! _)%E; iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto.
iIntros "{$Hγ $Hγf}"; iIntros {j'} "[% Hl] /="; rewrite {2}/counter_inv. iIntros "{$Hγ $Hγf}"; iIntros (j') "[% Hl] /="; rewrite {2}/counter_inv.
wp_load; iPvsIntro; iExists j; iSplit; [done|iIntros "{$Hl} Hγf"]. wp_load; iPvsIntro; iExists j; iSplit; [done|iIntros "{$Hl} Hγf"].
wp_let; wp_op. wp_let; wp_op.
wp_focus (CAS _ _ _); iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto. wp_focus (CAS _ _ _); iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto.
iIntros "{$Hγ $Hγf}"; iIntros {j''} "[% Hl] /="; rewrite {2}/counter_inv. iIntros "{$Hγ $Hγf}"; iIntros (j'') "[% Hl] /="; rewrite {2}/counter_inv.
destruct (decide (j `max` j'' = j `max` j')) as [Hj|Hj]. destruct (decide (j `max` j'' = j `max` j')) as [Hj|Hj].
- wp_cas_suc; first (by do 3 f_equal); iPvsIntro. - wp_cas_suc; first (by do 3 f_equal); iPvsIntro.
iExists (1 + j `max` j')%nat; iSplit. iExists (1 + j `max` j')%nat; iSplit.
...@@ -73,9 +73,9 @@ Lemma read_spec l j (Φ : val → iProp) : ...@@ -73,9 +73,9 @@ Lemma read_spec l j (Φ : val → iProp) :
counter l j ( i, (j i)%nat counter l i - Φ #i) counter l j ( i, (j i)%nat counter l i - Φ #i)
WP read #l {{ Φ }}. WP read #l {{ Φ }}.
Proof. Proof.
iIntros "[Hc HΦ]". iDestruct "Hc" as {N γ} "(% & #? & #Hγ & Hγf)". iIntros "[Hc HΦ]". iDestruct "Hc" as (N γ) "(% & #? & #Hγ & Hγf)".
rewrite /read. wp_let. iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto. rewrite /read. wp_let. iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto.
iIntros "{$Hγ $Hγf}"; iIntros {j'} "[% Hl] /=". iIntros "{$Hγ $Hγf}"; iIntros (j') "[% Hl] /=".
wp_load; iPvsIntro; iExists (j `max` j'); iSplit. wp_load; iPvsIntro; iExists (j `max` j'); iSplit.
{ iPureIntro; apply mnat_local_update; abstract lia. } { iPureIntro; apply mnat_local_update; abstract lia. }
rewrite !mnat_op_max -Nat.max_assoc Nat.max_idempotent; iIntros "{$Hl} Hγf". rewrite !mnat_op_max -Nat.max_assoc Nat.max_idempotent; iIntros "{$Hl} Hγf".
......
...@@ -44,15 +44,15 @@ Global Instance is_lock_persistent l R : PersistentP (is_lock l R). ...@@ -44,15 +44,15 @@ Global Instance is_lock_persistent l R : PersistentP (is_lock l R).
Proof. apply _. Qed. Proof. apply _. Qed.
Lemma locked_is_lock l R : locked l R is_lock l R. Lemma locked_is_lock l R : locked l R is_lock l R.
Proof. rewrite /is_lock. iDestruct 1 as {N γ} "(?&?&?&_)"; eauto. Qed. Proof. rewrite /is_lock. iDestruct 1 as (N γ) "(?&?&?&_)"; eauto. Qed.
Lemma newlock_spec N (R : iProp) Φ : Lemma newlock_spec N (R : iProp) Φ :
heapN N 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. Proof.
iIntros {?} "(#Hh & HR & HΦ)". rewrite /newlock. iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock.
wp_seq. wp_alloc l as "Hl". wp_seq. wp_alloc l as "Hl".
iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done. iPvs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iPvs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?"; first done. iPvs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?"; first done.
{ iIntros ">". iExists false. by iFrame. } { iIntros ">". iExists false. by iFrame. }
iPvsIntro. iApply "HΦ". iExists N, γ; eauto. iPvsIntro. iApply "HΦ". iExists N, γ; eauto.
...@@ -61,9 +61,9 @@ Qed. ...@@ -61,9 +61,9 @@ Qed.
Lemma acquire_spec l R (Φ : val iProp) : 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. Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as {N γ} "(%&#?&#?)". iIntros "[Hl HΦ]". iDestruct "Hl" as (N γ) "(%&#?&#?)".
iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E. iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E.
iInv N as { [] } "[Hl HR]". iInv N as ([]) "[Hl HR]".
- wp_cas_fail. iPvsIntro; iSplitL "Hl". - wp_cas_fail. iPvsIntro; iSplitL "Hl".
+ iNext. iExists true; eauto. + iNext. iExists true; eauto.
+ wp_if. by iApply "IH". + wp_if. by iApply "IH".
...@@ -75,8 +75,8 @@ Qed. ...@@ -75,8 +75,8 @@ Qed.
Lemma release_spec R l (Φ : val iProp) : Lemma release_spec R l (Φ : val iProp) :
locked l R R Φ #() WP release #l {{ Φ }}. locked l R R Φ #() WP release #l {{ Φ }}.
Proof. Proof.
iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as {N γ} "(% & #? & #? & Hγ)". iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as (N γ) "(% & #? & #? & Hγ)".
rewrite /release. wp_let. iInv N as {b} "[Hl _]". rewrite /release. wp_let. iInv N as (b) "[Hl _]".
wp_store. iPvsIntro. iFrame "HΦ". iNext. iExists false. by iFrame. wp_store. iPvsIntro. iFrame "HΦ". iNext. iExists false. by iFrame.
Qed. Qed.
End proof. End proof.
...@@ -27,12 +27,12 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp) e (f1 f2 : val) (Φ : val → iProp) : ...@@ -27,12 +27,12 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp) e (f1 f2 : val) (Φ : val → iProp) :
v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V) v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V)
WP par e {{ Φ }}. WP par e {{ Φ }}.
Proof. Proof.
iIntros {??} "(#Hh&Hf1&Hf2&HΦ)". iIntros (??) "(#Hh&Hf1&Hf2&HΦ)".
rewrite /par. wp_value. iPvsIntro. wp_let. wp_proj. rewrite /par. wp_value. iPvsIntro. wp_let. wp_proj.
wp_apply spawn_spec; try wp_done. iFrame "Hf1 Hh". wp_apply spawn_spec; try wp_done. iFrame "Hf1 Hh".
iIntros {l} "Hl". wp_let. wp_proj. wp_focus (f2 _). iIntros (l) "Hl". wp_let. wp_proj. wp_focus (f2 _).
iApply wp_wand_l; iFrame "Hf2"; iIntros {v} "H2". wp_let. iApply wp_wand_l; iFrame "Hf2"; iIntros (v) "H2". wp_let.
wp_apply join_spec; iFrame "Hl". iIntros {w} "H1". wp_apply join_spec; iFrame "Hl". iIntros (w) "H1".
iSpecialize ("HΦ" with "* [-]"); first by iSplitL "H1". by wp_let. iSpecialize ("HΦ" with "* [-]"); first by iSplitL "H1". by wp_let.
Qed. Qed.
...@@ -42,7 +42,7 @@ Lemma wp_par (Ψ1 Ψ2 : val → iProp) (e1 e2 : expr []) (Φ : val → iProp) : ...@@ -42,7 +42,7 @@ Lemma wp_par (Ψ1 Ψ2 : val → iProp) (e1 e2 : expr []) (Φ : val → iProp) :
v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V) v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V)
WP e1 || e2 {{ Φ }}. WP e1 || e2 {{ Φ }}.
Proof. Proof.
iIntros {?} "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2); auto. iIntros (?) "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2); auto.
iFrame "Hh H". iSplitL "H1"; by wp_let. iFrame "Hh H". iSplitL "H1"; by wp_let.
Qed. Qed.
End proof. End proof.
...@@ -56,15 +56,15 @@ Lemma spawn_spec (Ψ : val → iProp) e (f : val) (Φ : val → iProp) : ...@@ -56,15 +56,15 @@ Lemma spawn_spec (Ψ : val → iProp) e (f : val) (Φ : val → iProp) :
heap_ctx heapN WP f #() {{ Ψ }} ( l, join_handle l Ψ - Φ #l) heap_ctx heapN WP f #() {{ Ψ }} ( l, join_handle l Ψ - Φ #l)
WP spawn e {{ Φ }}. WP spawn e {{ Φ }}.
Proof. Proof.
iIntros {<-%of_to_val ?} "(#Hh & Hf & HΦ)". rewrite /spawn. 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 (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iPvs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done. iPvs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done.
{ iNext. iExists (InjLV #0). iFrame; eauto. } { iNext. iExists (InjLV #0). iFrame; eauto. }
wp_apply wp_fork. iSplitR "Hf". wp_apply wp_fork. iSplitR "Hf".
- iPvsIntro. wp_seq. iPvsIntro. iApply "HΦ". rewrite /join_handle. eauto. - iPvsIntro. wp_seq. iPvsIntro. iApply "HΦ". rewrite /join_handle. eauto.
- wp_focus (f _). iApply wp_wand_l. iFrame "Hf"; iIntros {v} "Hv". - wp_focus (f _). iApply wp_wand_l. iFrame "Hf"; iIntros (v) "Hv".
iInv N as {v'} "[Hl _]"; first wp_done. iInv N as (v') "[Hl _]"; first wp_done.
wp_store. iPvsIntro. iSplit; [iNext|done]. wp_store. iPvsIntro. iSplit; [iNext|done].
iExists (InjRV v). iFrame. eauto. iExists (InjRV v). iFrame. eauto.
Qed. Qed.
...@@ -72,12 +72,12 @@ Qed. ...@@ -72,12 +72,12 @@ Qed.
Lemma join_spec (Ψ : val iProp) l (Φ : val iProp) : 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. Proof.
rewrite /join_handle; iIntros "[[% H] Hv]". iDestruct "H" as {γ} "(#?&Hγ&#?)". 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]". iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv N as (v) "[Hl Hinv]".
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst. wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- iPvsIntro; iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|]. - iPvsIntro; iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
wp_match. iApply ("IH" with "Hγ Hv"). wp_match. iApply ("IH" with "Hγ Hv").
- iDestruct "Hinv" as {v'} "[% [HΨ|Hγ']]"; simplify_eq/=. - iDestruct "Hinv" as (v') "[% [HΨ|Hγ']]"; simplify_eq/=.
+ iPvsIntro; iSplitL "Hl Hγ". + iPvsIntro; iSplitL "Hl Hγ".
{ iNext. iExists _; iFrame; eauto. } { iNext. iExists _; iFrame; eauto. }
wp_match. by iApply "Hv". wp_match. by iApply "Hv".
......
...@@ -28,9 +28,9 @@ Lemma wp_alloc_pst E σ e v Φ : ...@@ -28,9 +28,9 @@ Lemma wp_alloc_pst E σ e v Φ :
ownP σ ( l, σ !! l = None ownP (<[l:=v]>σ) ={E}= Φ (LitV (LitLoc l))) ownP σ ( l, σ !! l = None ownP (<[l:=v]>σ) ={E}= Φ (LitV (LitLoc l)))
WP Alloc e @ E {{ Φ }}. WP Alloc e @ E {{ Φ }}.
Proof. Proof.
iIntros {?} "[HP HΦ]". iIntros (?) "[HP HΦ]".
iApply (wp_lift_atomic_head_step (Alloc e) σ); try (by simpl; eauto). iApply (wp_lift_atomic_head_step (Alloc e) σ); try (by simpl; eauto).
iFrame "HP". iNext. iIntros {v2 σ2 ef} "[% HP]". inv_head_step. iFrame "HP". iNext. iIntros (v2 σ2 ef) "[% HP]". inv_head_step.
match goal with H: _ = of_val v2 |- _ => apply (inj of_val (LitV _)) in H end. match goal with H: _ = of_val v2 |- _ => apply (inj of_val (LitV _)) in H end.
subst v2. iSplit; last done. iApply "HΦ"; by iSplit. subst v2. iSplit; last done. iApply "HΦ"; by iSplit.
Qed. Qed.
......
...@@ -70,8 +70,8 @@ Section auth. ...@@ -70,8 +70,8 @@ Section auth.
a nclose N E a nclose N E
φ a ={E}=> γ, (γ G) auth_ctx γ N φ auth_own γ a. φ a ={E}=> γ, (γ G) auth_ctx γ N φ auth_own γ a.
Proof. Proof.
iIntros {??} "Hφ". rewrite /auth_own /auth_ctx. iIntros (??) "Hφ". rewrite /auth_own /auth_ctx.
iPvs (own_alloc_strong (Auth (Excl' a) a) _ G) as {γ} "[% Hγ]"; first done. iPvs (own_alloc_strong (Auth (Excl' a) a) _ G) as (γ) "[% Hγ]"; first done.
iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']". iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
iPvs (inv_alloc N _ (auth_inv γ φ) with "[-Hγ']"); first done. iPvs (inv_alloc N _ (auth_inv γ φ) with "[-Hγ']"); first done.
{ iNext. iExists a. by iFrame. } { iNext. iExists a. by iFrame. }
...@@ -82,8 +82,8 @@ Section auth. ...@@ -82,8 +82,8 @@ Section auth.
a nclose N E a nclose N E
φ a ={E}=> γ, auth_ctx γ N φ auth_own γ a. φ a ={E}=> γ, auth_ctx γ N φ auth_own γ a.
Proof. Proof.
iIntros {??} "Hφ". iIntros (??) "Hφ".