Commit 1662c1dc authored by Robbert Krebbers's avatar Robbert Krebbers

Tactic iFrame (without args) that tries to frame all spatial hyps.

parent d3b14aca
Pipeline #1233 passed with stage
......@@ -89,7 +89,7 @@ Proof.
iDestruct (big_sepS_delete _ _ i with "HPΨ") as "[HΨ HPΨ]"; first done.
iDestruct ("HQR" with "HΨ") as "[HR1 HR2]".
rewrite -assoc_L !big_sepS_fn_insert'; [|abstract set_solver ..].
by iFrame "HR1 HR2".
by iFrame.
- rewrite -assoc_L !big_sepS_fn_insert; [|abstract set_solver ..]. eauto.
Qed.
......@@ -105,7 +105,7 @@ Proof.
iPvs (saved_prop_alloc (F:=idCF) _ P) as {γ} "#?".
iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
as {γ'} "[#? Hγ']"; eauto.
{ iNext. rewrite /barrier_inv /=. iFrame "Hl".
{ iNext. rewrite /barrier_inv /=. iFrame.
iExists (const P). rewrite !big_sepS_singleton /=. eauto. }
iAssert (barrier_ctx γ' l P)%I as "#?".
{ rewrite /barrier_ctx. by repeat iSplit. }
......@@ -117,7 +117,7 @@ Proof.
auto using sts.closed_op, i_states_closed, low_states_closed;
abstract set_solver. }
iPvsIntro. rewrite /recv /send. iSplitL "Hr".
- iExists γ', P, P, γ. iFrame "Hr". auto.
- iExists γ', P, P, γ. iFrame. auto.
- auto.
Qed.
......@@ -146,7 +146,7 @@ Proof.
wp_load. destruct p.
- (* a Low state. The comparison fails, and we recurse. *)
iExists (State Low I), {[ Change i ]}; iSplit; [done|iSplitL "Hl Hr"].
{ iNext. rewrite {2}/barrier_inv /=. by iFrame "Hl". }
{ iNext. rewrite {2}/barrier_inv /=. by iFrame. }
iIntros "Hγ".
iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "=>[Hγ]" as "Hγ".
{ iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
......@@ -161,7 +161,7 @@ Proof.
{ 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". auto.
iExists Ψ; iFrame. auto.
+ iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by auto.
iIntros "_". wp_op=> ?; simplify_eq/=; wp_if.
iPvsIntro. iApply "HΦ". iApply "HQR". by iRewrite "Heq".
......@@ -182,7 +182,7 @@ Proof.
iExists ({[Change i1; Change i2 ]}).
iSplit; [by eauto using split_step|iSplitL].
- iNext. rewrite {2}/barrier_inv /=. iFrame "Hl".
iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame "Hr HQR". auto.
iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame; auto.
- iIntros "Hγ".
iAssert (sts_ownS γ (i_states i1) {[Change i1]}
sts_ownS γ (i_states i2) {[Change i2]})%I with "=>[-]" as "[Hγ1 Hγ2]".
......@@ -192,15 +192,15 @@ Proof.
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"; auto.
+ iExists γ, P, R2, i2. iFrame "Hγ2 Hi2"; auto.
+ iExists γ, P, R1, i1. iFrame; auto.
+ iExists γ, P, R2, i2. iFrame; auto.
Qed.
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)".
iExists γ, P, Q, i; iFrame "Hctx Hγ Hi".
iExists γ, P, Q, i. iFrame "Hctx Hγ Hi".
iIntros "> HQ". by iApply "HP"; iApply "HP1".
Qed.
......
......@@ -56,7 +56,7 @@ Proof.
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) with "[-HΦ]") as "#?"; first done.
{ iIntros ">". iExists false. by iFrame "Hl HR". }
{ iIntros ">". iExists false. by iFrame. }
iPvsIntro. iApply "HΦ". iExists N, γ; eauto.
Qed.
......@@ -79,6 +79,6 @@ Lemma release_spec R l (Φ : val → iProp) :
Proof.
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γ".
wp_store. iFrame "HΦ". iNext. iExists false. by iFrame.
Qed.
End proof.
......@@ -61,13 +61,13 @@ Proof.
wp_let. wp_alloc l as "Hl". wp_let.
iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done.
iPvs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done.
{ iNext. iExists (InjLV #0). iFrame "Hl"; eauto. }
{ iNext. iExists (InjLV #0). iFrame; eauto. }
wp_apply wp_fork. iSplitR "Hf".
- wp_seq. iPvsIntro. iApply "HΦ"; rewrite /join_handle. eauto.
- wp_focus (f _). iApply wp_wand_l; iFrame "Hf"; iIntros {v} "Hv".
iInv N as {v'} "[Hl _]"; first wp_done.
wp_store. iSplit; [iNext|done].
iExists (InjRV v); iFrame "Hl"; eauto.
iExists (InjRV v); iFrame; eauto.
Qed.
Lemma join_spec (Ψ : val iProp) l (Φ : val iProp) :
......@@ -76,11 +76,11 @@ 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]".
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- iSplitL "Hl"; [iNext; iExists _; iFrame "Hl"; eauto|].
- iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
wp_case. wp_seq. iApply ("IH" with "Hγ Hv").
- iDestruct "Hinv" as {v'} "[% [HΨ|Hγ']]"; subst.
+ iSplitL "Hl Hγ".
{ iNext. iExists _; iFrame "Hl"; eauto. }
{ iNext. iExists _; iFrame; eauto. }
wp_case. wp_let. iPvsIntro. by iApply "Hv".
+ iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].
Qed.
......
......@@ -67,8 +67,8 @@ Section auth.
iPvs (own_alloc_strong (Auth (Excl' a) a) _ G) as {γ} "[% Hγ]"; first done.
iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
iPvs (inv_alloc N _ (auth_inv γ φ) with "[-Hγ']"); first done.
{ iNext. iExists a. by iFrame "Hφ". }
iPvsIntro; iExists γ. iSplit; first by iPureIntro. by iFrame "Hγ'".
{ iNext. iExists a. by iFrame. }
iPvsIntro; iExists γ. iSplit; first by iPureIntro. by iFrame.
Qed.
Lemma auth_alloc N E a :
......@@ -107,7 +107,7 @@ Section auth.
iPvs (own_update _ with "Hγ") as "[Hγ Hγf]".
{ apply (auth_local_update_l L); tauto. }
iPvsIntro. iSplitL "Hφ Hγ"; last by iApply "HΨ".
iNext. iExists (L a b). by iFrame "Hφ".
iNext. iExists (L a b). by iFrame.
Qed.
Lemma auth_fsa' L `{!LocalUpdate Lv L} E N (Ψ : V iPropG Λ Σ) γ a :
......
......@@ -109,7 +109,7 @@ Proof.
iNext. iExists (<[γ:=Q]> Φ); iSplit.
- iNext. iRewrite "HeqP". by rewrite big_sepM_fn_insert'.
- rewrite (big_sepM_fn_insert (λ _ _ P', _ _ _ P' _ _ (_ _ P')))%I //.
iFrame "Hf Hγ'". eauto.
iFrame; eauto.
Qed.
Lemma box_delete f P Q γ :
......@@ -124,7 +124,7 @@ Proof.
as "[[Hγ' #[HγΦ ?]] ?]"; first done.
iDestruct (box_own_agree γ Q (Φ γ) with "[#]") as "HeqQ"; first by eauto.
iDestruct (box_own_auth_agree γ b false with "[#]")
as "%"; subst; first by iFrame "Hγ".
as "%"; subst; first by iFrame.
iSplitL "Hγ"; last iSplit.
- iExists false; eauto.
- iNext. iRewrite "HeqP". iRewrite "HeqQ". by rewrite -big_sepM_delete.
......@@ -141,12 +141,12 @@ Proof.
iDestruct (big_sepM_delete _ f _ false with "Hf")
as "[[Hγ' #[HγΦ Hinv']] ?]"; first done; iTimeless "Hγ'".
iPvs (box_own_auth_update _ γ b' false true with "[Hγ Hγ']")
as "[Hγ Hγ']"; first by iFrame "Hγ".
as "[Hγ Hγ']"; first by iFrame.
iPvsIntro; iNext; iSplitL "Hγ HQ"; first (iExists true; by iFrame "Hγ HQ").
iExists Φ; iSplit.
- by rewrite big_sepM_insert_override.
- rewrite -insert_delete big_sepM_insert ?lookup_delete //.
iFrame "Hγ'"; eauto.
iFrame; eauto.
Qed.
Lemma box_empty f P Q γ :
......@@ -159,15 +159,15 @@ Proof.
iDestruct (big_sepM_delete _ f with "Hf")
as "[[Hγ' #[HγΦ Hinv']] ?]"; first done; iTimeless "Hγ'".
iDestruct (box_own_auth_agree γ b true with "[#]")
as "%"; subst; first by iFrame "Hγ".
as "%"; subst; first by iFrame.
iFrame "HQ".
iPvs (box_own_auth_update _ γ with "[Hγ Hγ']")
as "[Hγ Hγ']"; first by iFrame "Hγ".
as "[Hγ Hγ']"; first by iFrame.
iPvsIntro; iNext; iSplitL "Hγ"; first (iExists false; by repeat iSplit).
iExists Φ; iSplit.
- by rewrite big_sepM_insert_override.
- rewrite -insert_delete big_sepM_insert ?lookup_delete //.
iFrame "Hγ'"; eauto.
iFrame; eauto.
Qed.
Lemma box_fill_all f P Q : box N f P P ={N}=> box N (const true <$> f) P.
......@@ -181,8 +181,8 @@ Proof.
iAlways; iIntros {γ b' ?} "[(Hγ' & #$ & #$) HΦ]".
iInv N as {b} "[Hγ _]"; iTimeless "Hγ".
iPvs (box_own_auth_update _ γ with "[Hγ Hγ']")
as "[Hγ $]"; first by iFrame "Hγ".
iPvsIntro; iNext; iExists true. by iFrame "HΦ Hγ".
as "[Hγ $]"; first by iFrame.
iPvsIntro; iNext; iExists true. by iFrame.
Qed.
Lemma box_empty_all f P Q :
......@@ -197,10 +197,10 @@ Proof.
assert (true = b) as <- by eauto.
iInv N as {b} "(Hγ & _ & HΦ)"; iTimeless "Hγ".
iDestruct (box_own_auth_agree γ b true with "[#]")
as "%"; subst; first by iFrame "Hγ".
as "%"; subst; first by iFrame.
iPvs (box_own_auth_update _ γ true true false with "[Hγ Hγ']")
as "[Hγ $]"; first by iFrame "Hγ".
iPvsIntro; iNext. iFrame "HΦ". iExists false. iFrame "Hγ"; eauto. }
as "[Hγ $]"; first by iFrame.
iPvsIntro; iNext. iFrame "HΦ". iExists false. iFrame; eauto. }
iPvsIntro; iSplitL "HΦ".
- rewrite eq_iff later_iff big_sepM_later. by iApply "HeqP".
- iExists Φ; iSplit; by rewrite big_sepM_fmap.
......
......@@ -86,7 +86,7 @@ Section sts.
{ apply sts_auth_valid; set_solver. }
iExists γ; iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ $]".
iPvs (inv_alloc N _ (sts_inv γ φ) with "[Hφ Hγ]") as "#?"; auto.
iNext. iExists s. by iFrame "Hφ".
iNext. iExists s. by iFrame.
Qed.
Context {V} (fsa : FSA Λ (globalF Σ) V) `{!FrameShiftAssertion fsaV fsa}.
......@@ -111,7 +111,7 @@ Section sts.
iPvs (own_update with "Hγ") as "Hγ"; first eauto using sts_update_auth.
iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ Hγf]".
iPvsIntro; iSplitL "Hφ Hγ"; last by iApply "HΨ".
iNext; iExists s'; by iFrame "Hφ".
iNext; iExists s'; by iFrame.
Qed.
Lemma sts_fsa E N (Ψ : V iPropG Λ Σ) γ s0 T :
......
......@@ -376,6 +376,17 @@ Tactic Notation "iFrame" constr(Hs) :=
end
in let Hs := words Hs in go Hs.
Tactic Notation "iFrame" :=
let rec go Hs :=
match Hs with
| [] => idtac
| ?H :: ?Hs => try iFrame H; go Hs
end in
match goal with
| |- of_envs ?Δ _ =>
let Hs := eval cbv in (env_dom_list (env_spatial Δ)) in go Hs
end.
Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
eapply tac_combine with _ _ _ H1 _ _ H2 _ _ H _;
[env_cbv; reflexivity || fail "iCombine:" H1 "not found"
......
......@@ -67,15 +67,15 @@ Proof.
iIntros {v} "HP"; iDestruct "HP" as {x} "HP". wp_let.
iPvs (one_shot_init _ _ x with "Hγ") as "Hx".
iApply signal_spec; iFrame "Hs"; iSplit; last done.
iExists x; by iSplitL "Hx".
iExists x; auto.
- iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split.
iPvs (recv_split with "Hr") as "[H1 H2]"; first done.
wp_apply (wp_par _ _ (λ _, barrier_res γ Ψ1)%I
(λ _, barrier_res γ Ψ2)%I); first done.
iSplit; [done|]; iSplitL "H1"; [|iSplitL "H2"].
+ by iApply worker_spec; iSplitL "H1".
+ by iApply worker_spec; iSplitL "H2".
+ by iIntros {v1 v2} "? >".
- iIntros {_ v} "[_ H]"; iPoseProof (Q_res_join with "H"). by iNext; iExists γ.
+ iApply worker_spec; auto.
+ iApply worker_spec; auto.
+ auto.
- iIntros {_ v} "[_ H]"; iPoseProof (Q_res_join with "H"). auto.
Qed.
End proof.
......@@ -59,8 +59,8 @@ Proof.
iAssert ( v, l v ((v = InjLV #0 own γ OneShotPending)
n : Z, v = InjRV #n own γ (Shot (DecAgree n))))%I with "[-]" as "Hv".
{ iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as {m} "[Hl Hγ]".
+ iExists (InjLV #0). iFrame "Hl". eauto.
+ iExists (InjRV #m). iFrame "Hl". eauto. }
+ iExists (InjLV #0). iFrame. eauto.
+ iExists (InjRV #m). iFrame. eauto. }
iDestruct "Hv" as {v} "[Hl Hv]". wp_load.
iAssert (one_shot_inv γ l (v = InjLV #0 n : Z,
v = InjRV #n own γ (Shot (DecAgree n))))%I with "[-]" as "[$ #Hv]".
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment