Commit 02001691 authored by Robbert Krebbers's avatar Robbert Krebbers

Allow framing in negated specialization pattern.

parent a1be30d3
Pipeline #2910 passed with stage
in 9 minutes and 25 seconds
......@@ -225,8 +225,7 @@ _specification patterns_ to express splitting of hypotheses:
all persistent hypotheses. The spatial hypotheses among `H1 ... Hn` will be
consumed. Hypotheses may be prefixed with a `$`, which results in them being
framed in the generated goal.
- `[-H1 ... Hn]` : negated form of the above pattern. This pattern does not
accept hypotheses prefixed with a `$`.
- `[-H1 ... Hn]` : negated form of the above pattern.
- `>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
is a modality, in which case the modality will be kept in the generated goal
for the premise will be wrapped into the modality.
......
......@@ -13,6 +13,5 @@ Lemma wp_assert `{heapG Σ} E (Φ : val → iProp Σ) e `{!Closed [] e} :
WP e @ E {{ v, v = #true Φ #() }} WP assert: e @ E {{ Φ }}.
Proof.
iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
iApply wp_wand_r; iFrame "HΦ"; iIntros (v) "[% ?]"; subst.
wp_if. done.
iApply (wp_wand_r with "[- $HΦ]"). iIntros (v) "[% ?]"; subst. by wp_if.
Qed.
......@@ -24,10 +24,10 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp
Proof.
iIntros (?) "(#Hh&Hf1&Hf2&HΦ)".
rewrite /par. wp_value. iModIntro. wp_let. wp_proj.
wp_apply (spawn_spec parN); try wp_done; try solve_ndisj; iFrame "Hf1 Hh".
iNext. iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
iApply wp_wand_l; iFrame "Hf2"; iIntros (v) "H2". wp_let.
wp_apply join_spec; iFrame "Hl". iNext. iIntros (w) "H1".
wp_apply (spawn_spec parN with "[- $Hh $Hf1]"); try wp_done; try solve_ndisj.
iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
iApply (wp_wand_r with "[- $Hf2]"); iIntros (v) "H2". wp_let.
wp_apply (join_spec with "[- $Hl]"). iIntros (w) "H1".
iSpecialize ("HΦ" with "* [-]"); first by iSplitL "H1". by wp_let.
Qed.
......@@ -37,7 +37,7 @@ Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ)
v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V)
WP e1 || e2 {{ Φ }}.
Proof.
iIntros "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2); try wp_done.
iFrame "Hh H". iSplitL "H1"; by wp_let.
iIntros "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2 with "[- $Hh $H]"); try wp_done.
iSplitL "H1"; by wp_let.
Qed.
End proof.
......@@ -58,7 +58,7 @@ Proof.
{ iNext. iExists NONEV. iFrame; eauto. }
wp_apply wp_fork; simpl. iSplitR "Hf".
- iModIntro. wp_seq. iModIntro. iApply "HΦ". rewrite /join_handle. eauto.
- wp_bind (f _). iApply wp_wand_l. iFrame "Hf"; iIntros (v) "Hv".
- wp_bind (f _). iApply (wp_wand_r with "[ $Hf]"); iIntros (v) "Hv".
iInv N as (v') "[Hl _]" "Hclose".
wp_store. iApply "Hclose". iNext. iExists (SOMEV v). iFrame. eauto.
Qed.
......
......@@ -73,8 +73,8 @@ Section proof.
Lemma acquire_spec γ lk R :
{{{ is_lock γ lk R }}} acquire lk {{{; #(), locked γ R }}}.
Proof.
iIntros (Φ) "[#Hl HΦ]". iLöb as "IH". wp_rec. wp_bind (try_acquire _).
iApply try_acquire_spec. iFrame "#". iSplit.
iIntros (Φ) "[#Hl HΦ]". iLöb as "IH". wp_rec.
wp_apply (try_acquire_spec with "[- $Hl]"). iSplit.
- iIntros "Hlked HR". wp_if. iModIntro. iApply "HΦ"; iFrame.
- wp_if. iApply ("IH" with "[HΦ]"). auto.
Qed.
......@@ -87,7 +87,6 @@ Section proof.
rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
Qed.
End proof.
Definition spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
......
......@@ -71,7 +71,6 @@ with parse_goal (ts : list token) (g : spec_goal)
parse_goal ts (SpecGoal (spec_goal_modal g) (spec_goal_negate g)
(spec_goal_frame g) (s :: spec_goal_hyps g)) k
| TFrame :: TName s :: ts =>
guard (¬spec_goal_negate g);
parse_goal ts (SpecGoal (spec_goal_modal g) (spec_goal_negate g)
(s :: spec_goal_frame g) (spec_goal_hyps g)) k
| TBracketR :: ts =>
......
......@@ -308,7 +308,7 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
|(*goal*)
|go H1 pats]
| SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs) :: ?pats =>
let Hs' := eval cbv in (Hs_frame ++ Hs) in
let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
eapply tac_specialize_assert with _ _ _ H1 _ lr Hs' _ _ _ _;
[env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
......@@ -1085,7 +1085,7 @@ Tactic Notation "iAssertCore" open_constr(Q) "with" constr(Hs) "as" tactic(tac)
|apply _ || fail "iAssert:" Q "not persistent"
|tac H]
| [SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs)] =>
let Hs' := eval compute in (Hs_frame ++ Hs) in
let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
eapply tac_assert with _ _ _ lr Hs' H Q _;
[match m with
| false => apply elim_modal_dummy
......
......@@ -29,28 +29,26 @@ Section client.
heap_ctx recv N b (y_inv q y) WP worker n #b #y {{ _, True }}.
Proof.
iIntros "[#Hh Hrecv]". wp_lam. wp_let.
wp_apply wait_spec; iFrame "Hrecv".
iNext. iDestruct 1 as (f) "[Hy #Hf]".
wp_apply (wait_spec with "[- $Hrecv]"). iDestruct 1 as (f) "[Hy #Hf]".
wp_seq. wp_load.
iApply wp_wand_r; iSplitR; [iApply "Hf"|by iIntros (v) "_"].
iApply wp_wand_r. iSplitR; [iApply "Hf"|by iIntros (v) "_"].
Qed.
Lemma client_safe : heapN N heap_ctx WP client {{ _, True }}.
Proof.
iIntros (?) "#Hh"; rewrite /client. wp_alloc y as "Hy". wp_let.
wp_apply (newbarrier_spec N (y_inv 1 y)); first done.
iFrame "Hh". iNext. iIntros (l) "[Hr Hs]". wp_let.
iApply (wp_par (λ _, True%I) (λ _, True%I)). iFrame "Hh".
iSplitL "Hy Hs".
wp_apply (newbarrier_spec N (y_inv 1 y) with "[- $Hh]"); first done.
iIntros (l) "[Hr Hs]". wp_let.
iApply (wp_par (λ _, True%I) (λ _, True%I) with "[-$Hh]"). iSplitL "Hy Hs".
- (* The original thread, the sender. *)
wp_store. iApply signal_spec; iFrame "Hs"; iSplitL "Hy"; [|by eauto].
wp_store. iApply (signal_spec with "[- $Hs]"). iSplitL "Hy"; [|by eauto].
iExists _; iSplitL; [done|]. iAlways; iIntros (n). wp_let. by wp_op.
- (* The two spawned threads, the waiters. *)
iSplitL; [|by iIntros (_ _) "_ !>"].
iDestruct (recv_weaken with "[] Hr") as "Hr".
{ iIntros "Hy". by iApply (y_inv_split with "Hy"). }
iMod (recv_split with "Hr") as "[H1 H2]"; first done.
iApply (wp_par (λ _, True%I) (λ _, True%I)). iFrame "Hh".
iApply (wp_par (λ _, True%I) (λ _, True%I) with "[- $Hh]").
iSplitL "H1"; [|iSplitL "H2"; [|by iIntros (_ _) "_ !>"]];
iApply worker_safe; by iSplit.
Qed.
......
......@@ -35,8 +35,8 @@ Lemma worker_spec e γ l (Φ Ψ : X → iProp Σ) `{!Closed [] e} :
recv N l (barrier_res γ Φ) ( x, {{ Φ x }} e {{ _, Ψ x }})
WP wait #l ;; e {{ _, barrier_res γ Ψ }}.
Proof.
iIntros "[Hl #He]". wp_apply wait_spec; simpl; iFrame "Hl".
iNext. iDestruct 1 as (x) "[#Hγ Hx]".
iIntros "[Hl #He]". wp_apply (wait_spec with "[- $Hl]"); simpl.
iDestruct 1 as (x) "[#Hγ Hx]".
wp_seq. iApply wp_wand_l. iSplitR; [|by iApply "He"].
iIntros (v) "?"; iExists x; by iSplit.
Qed.
......@@ -76,21 +76,21 @@ Lemma client_spec_new eM eW1 eW2 `{!Closed [] eM, !Closed [] eW1, !Closed [] eW2
Proof.
iIntros (HN) "/= (#Hh&HP&#He&#He1&#He2)"; rewrite /client.
iMod (own_alloc (Pending : one_shotR Σ F)) as (γ) "Hγ"; first done.
wp_apply (newbarrier_spec N (barrier_res γ Φ)); auto.
iFrame "Hh". iNext. iIntros (l) "[Hr Hs]".
wp_apply (newbarrier_spec N (barrier_res γ Φ) with "[- $Hh]"); auto.
iIntros (l) "[Hr Hs]".
set (workers_post (v : val) := (barrier_res γ Ψ1 barrier_res γ Ψ2)%I).
wp_let. wp_apply (wp_par (λ _, True)%I workers_post); iFrame "Hh".
wp_let. wp_apply (wp_par (λ _, True)%I workers_post with "[- $Hh]").
iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
- wp_bind eM. iApply wp_wand_l; iSplitR "HP"; [|by iApply "He"].
iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let.
iMod (own_update with "Hγ") as "Hx".
{ by apply (cmra_update_exclusive (Shot x)). }
iApply signal_spec; iFrame "Hs"; iSplitR ""; last auto.
iApply (signal_spec with "[- $Hs]"). iSplitR ""; last auto.
iExists x; auto.
- iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split.
iMod (recv_split with "Hr") as "[H1 H2]"; first done.
wp_apply (wp_par (λ _, barrier_res γ Ψ1)%I
(λ _, barrier_res γ Ψ2)%I); iFrame "Hh".
(λ _, barrier_res γ Ψ2)%I with "[-$Hh]").
iSplitL "H1"; [|iSplitL "H2"].
+ iApply worker_spec; auto.
+ iApply worker_spec; auto.
......
......@@ -47,7 +47,7 @@ Lemma rev_wp hd xs (Φ : val → iProp Σ) :
WP rev hd (InjL #()) {{ Φ }}.
Proof.
iIntros "(#Hh & Hxs & HΦ)".
iApply (rev_acc_wp hd NONEV xs []); iFrame "Hh Hxs".
iApply (rev_acc_wp hd NONEV xs [] with "[- $Hh $Hxs]").
iSplit; first done. iIntros (w). rewrite right_id_L. iApply "HΦ".
Qed.
End list_reverse.
......@@ -94,6 +94,6 @@ Proof.
iIntros (f1 f2) "[#Hf1 #Hf2]"; iSplit.
- iIntros (n) "!# _". wp_proj. iApply "Hf1".
- iIntros "!# _". wp_proj.
iApply wp_wand_l; iFrame "Hf2". by iIntros (v) "#? !# _".
iApply (wp_wand_r with "[- $Hf2]"). by iIntros (v) "#? !# _".
Qed.
End proof.
......@@ -62,7 +62,7 @@ Lemma sum_wp `{!heapG Σ} v t Φ :
Proof.
iIntros "(#Hh & Ht & HΦ)". rewrite /sum' /=.
wp_let. wp_alloc l as "Hl". wp_let.
wp_apply sum_loop_wp; iFrame "Hh Ht Hl".
wp_apply (sum_loop_wp with "[- $Hh $Ht $Hl]").
rewrite Z.add_0_r.
iIntros "Hl Ht". wp_seq. wp_load. by iApply "HΦ".
Qed.
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