Commit d3b14aca authored by Robbert Krebbers's avatar Robbert Krebbers

Auto hints for the proof mode.

parent 658e90f3
Pipeline #1232 passed with stage
......@@ -166,7 +166,7 @@ Section heap.
iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
rewrite of_heap_singleton_op //. iFrame "Hl". iNext.
iIntros "$". by iSplit.
iIntros "$"; eauto.
Qed.
Lemma wp_store N E l v' e v Φ :
......@@ -195,7 +195,7 @@ Section heap.
iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
rewrite of_heap_singleton_op //. iFrame "Hl". iNext.
iIntros "$". by iSplit.
iIntros "$"; eauto.
Qed.
Lemma wp_cas_suc N E l e1 v1 e2 v2 Φ :
......
......@@ -90,8 +90,7 @@ Proof.
iDestruct ("HQR" with "HΨ") as "[HR1 HR2]".
rewrite -assoc_L !big_sepS_fn_insert'; [|abstract set_solver ..].
by iFrame "HR1 HR2".
- rewrite -assoc_L !big_sepS_fn_insert; [|abstract set_solver ..].
by repeat iSplit.
- rewrite -assoc_L !big_sepS_fn_insert; [|abstract set_solver ..]. eauto.
Qed.
(** Actual proofs *)
......@@ -107,8 +106,7 @@ Proof.
iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
as {γ'} "[#? Hγ']"; eauto.
{ iNext. rewrite /barrier_inv /=. iFrame "Hl".
iExists (const P). rewrite !big_sepS_singleton /=.
iSplit; [|done]. by iIntros "> ?". }
iExists (const P). rewrite !big_sepS_singleton /=. eauto. }
iAssert (barrier_ctx γ' l P)%I as "#?".
{ rewrite /barrier_ctx. by repeat iSplit. }
iAssert (sts_ownS γ' (i_states γ) {[Change γ]}
......@@ -119,8 +117,8 @@ 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". repeat iSplit; auto. by iIntros "> ?".
- iExists γ'. by iSplit.
- iExists γ', P, P, γ. iFrame "Hr". auto.
- auto.
Qed.
Lemma signal_spec l P (Φ : val iProp) :
......@@ -132,7 +130,7 @@ Proof.
wp_store. destruct p; [|done].
iExists (State High I), ( : set token).
iSplit; [iPureIntro; by eauto using signal_step|].
iSplitR "HΦ"; [iNext|by iIntros "?"].
iSplitR "HΦ"; [iNext|by auto].
rewrite {2}/barrier_inv /ress /=; iFrame "Hl".
iDestruct "Hr" as {Ψ} "[Hr Hsp]"; iExists Ψ; iFrame "Hsp".
iIntros "> _"; by iApply "Hr".
......@@ -152,7 +150,7 @@ Proof.
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. }
wp_op=> ?; simplify_eq; wp_if. iApply ("IH" with "Hγ [HQR] HΦ"). by iNext.
wp_op=> ?; simplify_eq; wp_if. iApply ("IH" with "Hγ [HQR] HΦ"). auto.
- (* a High state: the comparison succeeds, and we perform a transition and
return to the client *)
iExists (State High (I {[ i ]})), ( : set token).
......@@ -163,8 +161,8 @@ 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". by iIntros "> _".
+ iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by iSplit.
iExists Ψ; iFrame "Hsp". 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".
Qed.
......@@ -184,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". by repeat iSplit.
iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame "Hr HQR". 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]".
......@@ -194,10 +192,8 @@ 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". repeat iSplit; auto.
by iIntros "> ?".
+ iExists γ, P, R2, i2. iFrame "Hγ2 Hi2". repeat iSplit; auto.
by iIntros "> ?".
+ iExists γ, P, R1, i1. iFrame "Hγ1 Hi1"; auto.
+ iExists γ, P, R2, i2. iFrame "Hγ2 Hi2"; auto.
Qed.
Lemma recv_weaken l P1 P2 : (P1 - P2) recv l P1 - recv l P2.
......
......@@ -22,10 +22,9 @@ Proof.
intros HN.
exists (λ l, CofeMor (recv heapN N l)), (λ l, CofeMor (send heapN N l)).
split_and?; simpl.
- iIntros {P} "#? ! _". iApply (newbarrier_spec _ _ P); first done.
iSplit; [done|]; iIntros {l} "?"; iExists l; by iSplit.
- iIntros {P} "#? ! _". iApply (newbarrier_spec _ _ P); eauto.
- iIntros {l P} "! [Hl HP]". by iApply signal_spec; iFrame "Hl HP".
- iIntros {l P} "! Hl". iApply wait_spec; iFrame "Hl". by iIntros "?".
- iIntros {l P} "! Hl". iApply wait_spec; iFrame "Hl"; eauto.
- intros; by apply recv_split.
- apply recv_weaken.
Qed.
......
......@@ -45,8 +45,7 @@ Proof. apply _. Qed.
Lemma locked_is_lock l R : locked l R is_lock l R.
Proof.
iIntros "Hl"; iDestruct "Hl" as {N γ} "(?&?&?&_)".
iExists N, γ; by repeat iSplit.
rewrite /is_lock. iIntros "Hl"; iDestruct "Hl" as {N γ} "(?&?&?&_)". eauto.
Qed.
Lemma newlock_spec N (R : iProp) Φ :
......@@ -58,7 +57,7 @@ Proof.
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". }
iPvsIntro. iApply "HΦ". iExists N, γ. by repeat iSplit.
iPvsIntro. iApply "HΦ". iExists N, γ; eauto.
Qed.
Lemma acquire_spec l R (Φ : val iProp) :
......@@ -68,11 +67,11 @@ Proof.
iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E.
iInv N as { [] } "[Hl HR]".
- wp_cas_fail. iSplitL "Hl".
+ iNext. iExists true. by iSplit.
+ iNext. iExists true; eauto.
+ wp_if. by iApply "IH".
- wp_cas_suc. iDestruct "HR" as "[Hγ HR]". iSplitL "Hl".
+ iNext. iExists true. by iSplit.
+ wp_if. iApply ("HΦ" with "[-HR] HR"). iExists N, γ. by repeat iSplit.
+ iNext. iExists true; eauto.
+ wp_if. iApply ("HΦ" with "[-HR] HR"). iExists N, γ; eauto.
Qed.
Lemma release_spec R l (Φ : val iProp) :
......
......@@ -61,14 +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". by iLeft. }
{ iNext. iExists (InjLV #0). iFrame "Hl"; eauto. }
wp_apply wp_fork. iSplitR "Hf".
- wp_seq. iPvsIntro. iApply "HΦ"; rewrite /join_handle.
iSplit; first done. iExists γ. iFrame "Hγ"; by iSplit.
- 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"; iRight; iExists v; iSplit; [done|by iLeft].
iExists (InjRV v); iFrame "Hl"; eauto.
Qed.
Lemma join_spec (Ψ : val iProp) l (Φ : val iProp) :
......@@ -77,12 +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"; by iLeft|].
- iSplitL "Hl"; [iNext; iExists _; iFrame "Hl"; eauto|].
wp_case. wp_seq. iApply ("IH" with "Hγ Hv").
- iDestruct "Hinv" as {v'} "[% [HΨ|Hγ']]"; subst.
+ iSplitL "Hl Hγ".
{ iNext. iExists _; iFrame "Hl"; iRight.
iExists _; iSplit; [done|by iRight]. }
{ iNext. iExists _; iFrame "Hl"; eauto. }
wp_case. wp_let. iPvsIntro. by iApply "Hv".
+ iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].
Qed.
......
......@@ -104,12 +104,12 @@ Proof.
rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
iDestruct "Hdom" as % ?%not_elem_of_dom.
iPvs (inv_alloc N _ (box_slice_inv γ Q) with "[Hγ]") as "#Hinv"; first done.
{ iNext. iExists false. by repeat iSplit. }
{ iNext. iExists false; eauto. }
iPvsIntro; iExists γ; repeat iSplit; auto.
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γ'". by iSplit.
iFrame "Hf Hγ'". eauto.
Qed.
Lemma box_delete f P Q γ :
......@@ -122,13 +122,13 @@ Proof.
iInv N as {b} "(Hγ & #HγQ &_)"; iPvsIntro; iNext.
iDestruct (big_sepM_delete _ f _ false with "Hf")
as "[[Hγ' #[HγΦ ?]] ?]"; first done.
iDestruct (box_own_agree γ Q (Φ γ) with "[#]") as "HeqQ"; first by iSplit.
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γ".
iSplitL "Hγ"; last iSplit.
- iExists false; repeat iSplit; auto.
- iExists false; eauto.
- iNext. iRewrite "HeqP". iRewrite "HeqQ". by rewrite -big_sepM_delete.
- iExists Φ; by iSplit; [iNext|].
- iExists Φ; eauto.
Qed.
Lemma box_fill f γ P Q :
......@@ -146,7 +146,7 @@ Proof.
iExists Φ; iSplit.
- by rewrite big_sepM_insert_override.
- rewrite -insert_delete big_sepM_insert ?lookup_delete //.
iFrame "Hγ'". by repeat iSplit.
iFrame "Hγ'"; eauto.
Qed.
Lemma box_empty f P Q γ :
......@@ -167,7 +167,7 @@ Proof.
iExists Φ; iSplit.
- by rewrite big_sepM_insert_override.
- rewrite -insert_delete big_sepM_insert ?lookup_delete //.
iFrame "Hγ'". by repeat iSplit.
iFrame "Hγ'"; eauto.
Qed.
Lemma box_fill_all f P Q : box N f P P ={N}=> box N (const true <$> f) P.
......@@ -200,7 +200,7 @@ Proof.
as "%"; subst; first by iFrame "Hγ".
iPvs (box_own_auth_update _ γ true true false with "[Hγ Hγ']")
as "[Hγ $]"; first by iFrame "Hγ".
iPvsIntro; iNext. iFrame "HΦ". iExists false. by iFrame "Hγ"; iSplit. }
iPvsIntro; iNext. iFrame "HΦ". iExists false. iFrame "Hγ"; eauto. }
iPvsIntro; iSplitL "HΦ".
- rewrite eq_iff later_iff big_sepM_later. by iApply "HeqP".
- iExists Φ; iSplit; by rewrite big_sepM_fmap.
......
......@@ -42,7 +42,7 @@ Proof.
iPvs (pvs_openI' with "Hi") as "HP"; [set_solver..|].
iPvsIntro. iSplitL "HP"; first done. iIntros "HP".
iPvs (pvs_closeI' _ _ P with "[HP]"); [set_solver|iSplit; done|set_solver|].
iPvsIntro. done.
done.
Qed.
(** Invariants can be opened around any frame-shifting assertion. This is less
......@@ -54,11 +54,11 @@ Proof.
iIntros {??} "[Hinv HΨ]".
iDestruct (inv_open E N P with "Hinv") as {E'} "[% Hvs]"; first done.
iApply (fsa_open_close E E'); auto; first set_solver.
iPvs "Hvs" as "[HP Hvs]";first set_solver.
iPvs "Hvs" as "[HP Hvs]"; first set_solver.
(* TODO: How do I do sth. like [iSpecialize "HΨ HP"]? *)
iPvsIntro. iApply (fsa_mask_weaken _ (E N)); first set_solver.
iApply fsa_wand_r. iSplitR "Hvs"; first by iApply "HΨ".
simpl. iIntros {v} "[HP HΨ]". iPvs ("Hvs" with "HP"); first set_solver.
by iPvsIntro.
done.
Qed.
End inv.
......@@ -770,4 +770,20 @@ Tactic Notation "iRewrite" "-" open_constr(t) "in" constr(H) :=
(* Make sure that by and done solve trivial things in proof mode *)
Hint Extern 0 (of_envs _ _) => by iPureIntro.
Hint Extern 0 (of_envs _ _) => iAssumption.
Hint Extern 0 (of_envs _ _) => progress iIntros.
Hint Resolve uPred.eq_refl'. (* Maybe make an [iReflexivity] tactic *)
(* We should be able to write [Hint Extern 1 (of_envs _ ⊢ (_ ★ _)%I) => ...],
but then [eauto] mysteriously fails. See bug 4762 *)
Hint Extern 1 (of_envs _ _) =>
match goal with
| |- _ (_ _)%I => iSplit
| |- _ (_ _)%I => iSplit
| |- _ ( _)%I => iNext
| |- _ ( _)%I => iClear "*"; iAlways
| |- _ ( _, _)%I => iExists _
end.
Hint Extern 1 (of_envs _ _) =>
match goal with |- _ (_ _)%I => iLeft end.
Hint Extern 1 (of_envs _ _) =>
match goal with |- _ (_ _)%I => iRight end.
......@@ -59,14 +59,14 @@ 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". iLeft; by iSplit.
+ iExists (InjRV #m). iFrame "Hl". iRight; iExists m; by iSplit. }
+ iExists (InjLV #0). iFrame "Hl". eauto.
+ iExists (InjRV #m). iFrame "Hl". 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]".
{ iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as {m} "[% ?]"; subst.
+ iSplit. iLeft; by iSplitL "Hl". by iLeft.
+ iSplit. iRight; iExists m; by iSplitL "Hl". iRight; iExists m; by iSplit. }
+ iSplit. iLeft; by iSplitL "Hl". eauto.
+ iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
wp_let. iPvsIntro. iIntros "!". wp_seq.
iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as {m} "[% Hγ']"; subst.
{ wp_case. wp_seq. by iPvsIntro. }
......@@ -76,9 +76,8 @@ Proof.
wp_load.
iCombine "Hγ" "Hγ'" as "Hγ".
iDestruct (own_valid with "#Hγ") as %[=->]%dec_agree_op_inv.
iSplitL "Hl"; [iRight; iExists m; by iSplit|].
wp_case. wp_let. iApply wp_assert'. wp_op=>?; simplify_eq/=.
iSplit. done. by iNext.
iSplitL "Hl"; [iRight; by eauto|].
wp_case. wp_let. iApply wp_assert'. wp_op=>?; simplify_eq/=; eauto.
Qed.
Lemma hoare_one_shot (Φ : val iProp) :
......
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