Commit 01d95642 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris (wp_apply).

parent 94c0f0db
Pipeline #41266 failed with stage
in 13 minutes and 28 seconds
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
depends: [
"coq-iris-heap-lang" { (= "dev.2021-01-25.1.21b7ffa1") | (= "dev") }
"coq-iris-heap-lang" { (= "dev.2021-01-26.0.a26cf167") | (= "dev") }
]
......@@ -188,7 +188,7 @@ Section cwp_rules.
Lemma cwp_ret e R Φ :
WP e {{ Φ }} - CWP c_ret e @ R {{ Φ }}.
Proof.
iIntros "Hwp". rewrite cwp_eq /cwp_def. wp_apply (wp_wand with "Hwp").
iIntros "Hwp". rewrite cwp_eq /cwp_def. wp_smart_apply (wp_wand with "Hwp").
iIntros (v) "HΦ". wp_lam. wp_pures.
iIntros "!>" (γ env l I) "#Hlock Hres #Heq". wp_pures. by iFrame.
Qed.
......@@ -198,11 +198,11 @@ Section cwp_rules.
CWP c_bind e f @ R {{ Φ }}.
Proof.
iIntros "Hwp". rewrite cwp_eq /cwp_def.
wp_apply (wp_wand with "Hwp"). iIntros (ev) "Hwp".
wp_smart_apply (wp_wand with "Hwp"). iIntros (ev) "Hwp".
wp_lam. wp_pures.
iIntros "!>" (γ env l I) "#Hflock Hres #Heq". wp_pures. wp_bind (ev env l).
iApply (wp_wand with "[Hwp Hres]"). iApply ("Hwp" with "Hflock Hres Heq").
iIntros (w) "[Hwp Hres]". wp_let. wp_apply (wp_wand with "Hwp").
iIntros (w) "[Hwp Hres]". wp_let. wp_smart_apply (wp_wand with "Hwp").
iIntros (v) "H". iApply ("H" with "Hflock Hres Heq").
Qed.
......@@ -212,18 +212,18 @@ Section cwp_rules.
Proof.
iIntros "Hwp". rewrite cwp_eq /cwp_def. wp_lam. wp_pures.
iIntros "!>" (γ env l I) "#Hlock1 Hres #Heq1". wp_pures.
wp_apply (acquire_flock_spec with "[$]").
wp_smart_apply (acquire_flock_spec with "[$]").
iIntros "Hfl".
iMod (flocked_inv_acc with "Hfl") as "[HI Hcl]"; first done.
iRewrite "Heq1" in "HI".
iDestruct "HI" as "[Henv HR]".
wp_pures; simpl.
iDestruct ("Hwp" with "HR") as (Q) "[HQ Hwp]".
wp_apply (newflock_spec cmonadN); first done.
wp_smart_apply (newflock_spec cmonadN); first done.
iIntros (k γ') "#Hlock2".
iMod (flock_res_alloc_cofinite _ _ _ (env_inv env Q)%I with "Hlock2 [$HQ $Henv]") as (ρ) "[_ Hres]"; first done.
wp_let.
wp_apply (wp_wand with "Hwp"); iIntros (ev') "Hwp". wp_bind (ev' _ _).
wp_smart_apply (wp_wand with "Hwp"); iIntros (ev') "Hwp". wp_bind (ev' _ _).
iApply (wp_wand with "[Hwp Hres]").
- iApply ("Hwp" $! _ _ _ {[ρ:=(1%Qp,_)]} with "Hlock2 [Hres] []").
+ rewrite /flock_resources big_sepM_singleton //.
......@@ -235,7 +235,7 @@ Section cwp_rules.
iDestruct ("HR" with "HQ") as "[HR HΦ]".
iMod ("Hcl" with "[HR Henv]") as "Hflocked".
{ iNext. iRewrite "Heq1". iFrame. }
wp_apply (release_cancel_spec with "[$Hlock1 $Hflocked]").
wp_smart_apply (release_cancel_spec with "[$Hlock1 $Hflocked]").
iIntros "$". wp_pures. by iFrame.
Qed.
......@@ -246,18 +246,18 @@ Section cwp_rules.
Proof.
iIntros "Hwp". rewrite cwp_eq /cwp_def. wp_lam. wp_pures.
iIntros "!>" (γ env l I) "#Hlock Hres #Heq". wp_pures.
wp_apply (acquire_flock_spec with "[$]").
wp_smart_apply (acquire_flock_spec with "[$]").
iIntros "Hfl".
iMod (flocked_inv_acc with "Hfl") as "[HI Hcl]"; first done.
iRewrite "Heq" in "HI".
iDestruct "HI" as "[Henv HR]".
wp_pures; simpl.
iSpecialize ("Hwp" with "Henv HR").
wp_apply (wp_wand with "Hwp").
wp_smart_apply (wp_wand with "Hwp").
iIntros (w) "[Henv [HR HΦ]]". wp_pures.
iRewrite "Heq" in "Hcl".
iMod ("Hcl" with "[$HR $Henv]") as "Hflocked".
wp_apply (release_cancel_spec with "[$Hlock $Hflocked]").
wp_smart_apply (release_cancel_spec with "[$Hlock $Hflocked]").
iIntros "$". wp_pures. by iFrame.
Qed.
......@@ -268,9 +268,9 @@ Section cwp_rules.
CWP e1 ||| e2 @ R {{ Φ }}.
Proof.
iIntros "Hwp1 Hwp2 HΦ". rewrite cwp_eq /cwp_def.
wp_apply (wp_wand with "Hwp2").
wp_smart_apply (wp_wand with "Hwp2").
iIntros (ev2) "Hwp2".
wp_apply (wp_wand with "Hwp1").
wp_smart_apply (wp_wand with "Hwp1").
iIntros (ev1) "Hwp1". wp_lam. wp_pures.
iIntros "!>" (γ env l I) "#Hlock Hres #Heq". wp_pures.
pose (I' := fmap (λ πR, ((πR.1/2)%Qp,πR.2)) I).
......@@ -339,7 +339,7 @@ Section cwp_run.
iMod locking_heap_init as (?) "Hσ".
pose (amg := AMonadG Σ _ _ _ _).
iSpecialize ("Hwp" $! amg). rewrite cwp_eq /cwp_def.
wp_apply (newflock_spec cmonadN); first done.
wp_smart_apply (newflock_spec cmonadN); first done.
iIntros (k γ') "#Hlock". iApply wp_fupd.
iMod (flock_res_alloc_cofinite _ _ _ (env_inv env)%I
with "Hlock [Henv Hσ]") as (ρ) "[_ Hres]"; first done.
......
......@@ -266,7 +266,7 @@ Section proofs.
iModIntro. iSplit; first done. iNext. cwp_pures.
iApply cwp_atomic_env.
iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "$". wp_pures.
wp_apply (lreplicate_spec with "[//]"); iIntros (ll Hll).
wp_smart_apply (lreplicate_spec with "[//]"); iIntros (ll Hll).
wp_alloc l as "Hl".
iMod (full_locking_heap_alloc_upd with "Hσ Hl")
as (?) "(Hσ & Hinfo & Hl)"; first done.
......@@ -299,17 +299,17 @@ Section proofs.
iMod (full_locking_heap_free_upd with "Hσ Hinfo Hcl")
as (ll Hoff Hl) "[Hl Hclose]".
wp_load. wp_pures. rewrite Hoff.
wp_apply wp_assert; wp_pures; iModIntro; iSplit; first done. iNext.
wp_apply wp_assert; wp_pures; iModIntro; iSplit; first done. iNext.
wp_pures. wp_apply (llength_spec with "[//]"); iIntros "_"; wp_pures.
wp_smart_apply wp_assert; wp_pures; iModIntro; iSplit; first done. iNext.
wp_smart_apply wp_assert; wp_pures; iModIntro; iSplit; first done. iNext.
wp_pures. wp_smart_apply (llength_spec with "[//]"); iIntros "_"; wp_pures.
iAssert ( Ψ (n : nat), n length ws
(is_mset env X - Ψ #()) - WP c_free_check env #(cloc_base cl) #n {{ Ψ }})%I
with "[Hlocks]" as "Hcheck".
{ iIntros (Ψ n Hn) "HΨ". iInduction n as [|n] "IH" forall (Ψ Hn).
{ wp_lam; wp_pures. by iApply "HΨ". }
wp_lam; wp_pures. wp_apply wp_assert.
wp_lam; wp_pures. wp_smart_apply wp_assert.
rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
wp_apply (mset_member_spec with "Hlocks").
wp_smart_apply (mset_member_spec with "Hlocks").
{ intros v Hv. rewrite /is_loc_nonnull. destruct (HX v Hv) as (cl'&->&?); eauto. }
{ rewrite /is_loc_nonnull /=; eauto. }
iIntros "Hlocks"; case_bool_decide.
......@@ -318,7 +318,7 @@ Section proofs.
destruct cl; simplify_eq/=. by rewrite /cloc_plus /= Z.add_0_r. }
wp_op. iModIntro. iSplit; first done. iNext; wp_pures.
iApply ("IH" with "[%] Hlocks HΨ"). lia. }
wp_apply ("Hcheck" with "[//]"); iIntros "Hlock". wp_pures. wp_store.
wp_smart_apply ("Hcheck" with "[//]"); iIntros "Hlock". wp_pures. wp_store.
iIntros "!> {$HΦ}". iExists X, _.
iFrame "Hlock". iSplit; last by iApply "Hclose".
iPureIntro; intros w Hw. destruct (HX _ Hw) as (cl'&Hcl&Hin).
......@@ -351,14 +351,14 @@ Section proofs.
{ intros Hcl. destruct (HX _ Hcl) as (cl'&[=]%cloc_to_of_val&?). naive_solver. }
iMod (full_locking_heap_store_upd with "Hσ Hl") as (k ll vs Hl Hi) "[Hl Hclose]".
wp_pures. rewrite cloc_to_val_eq. wp_pures.
wp_apply (mset_add_spec with "[$]").
wp_smart_apply (mset_add_spec with "[$]").
{ intros v Hv. rewrite /is_loc_nonnull. destruct (HX v Hv) as (cl'&->&?); eauto. }
{ rewrite /is_loc_nonnull /=; eauto. }
{ done. }
iIntros "Hlocks /="; wp_pures.
wp_load; wp_pures.
iEval (rewrite -(Z2Nat.id (cloc_offset cl)) //).
wp_apply (linsert_spec with "[//]"); [eauto|]. iIntros (ll' Hl').
wp_smart_apply (linsert_spec with "[//]"); [eauto|]. iIntros (ll' Hl').
iApply wp_fupd. wp_store.
iMod ("Hclose" $! _ LLvl with "[//] Hl") as "[Hσ Hl]".
iMod ("HΦ" with "Hl") as "HΦ".
......@@ -385,7 +385,7 @@ Section proofs.
{ intros Hcl. destruct (HX _ Hcl) as (?&[=]%cloc_to_of_val&?); naive_solver. }
iMod (full_locking_heap_load_upd with "Hσ Hl") as (k ll vs Hl Hi) "[Hl Hclose]".
wp_pures. rewrite cloc_to_val_eq. wp_pures.
wp_apply wp_assert. wp_apply (mset_member_spec with "Hlocks").
wp_smart_apply wp_assert. wp_smart_apply (mset_member_spec with "Hlocks").
{ intros v Hv'. rewrite /is_loc_nonnull. destruct (HX v Hv') as (cl'&->&?); eauto. }
{ rewrite /is_loc_nonnull /=; eauto. }
iIntros "Hlocks /=".
......@@ -394,7 +394,7 @@ Section proofs.
wp_load; wp_match.
iEval (rewrite -(Z2Nat.id (cloc_offset cl)) //).
iApply wp_fupd.
wp_apply (llookup_spec with "[//]"); [done|]; iIntros "_".
wp_smart_apply (llookup_spec with "[//]"); [done|]; iIntros "_".
iDestruct ("Hclose" with "Hl") as "[Hσ Hl]".
iMod ("HΦ" with "Hl") as "[$ $]".
iIntros "!> !>". iExists X, _. by iFrame.
......@@ -419,7 +419,7 @@ Section proofs.
iIntros "HΦ". iApply cwp_atomic_env.
iIntros (env). iDestruct (1) as (X σ _) "[Hlocks Hσ]".
iIntros "$". iApply wp_fupd.
wp_apply (mset_clear_spec with "Hlocks"); iIntros "Hlocks".
wp_smart_apply (mset_clear_spec with "Hlocks"); iIntros "Hlocks".
rewrite U_eq. iDestruct "HΦ" as (us) "[Hus H]".
iInduction us as [|[ul [uq uv]] us] "IH" using gmultiset_ind forall (σ); simpl.
- iModIntro. iSplitR "H Hus".
......@@ -465,7 +465,7 @@ Section proofs.
cwp_pures. iApply cwp_bind.
cwp_apply cwp_atomic_env; iIntros (env) "Henv $". iApply wp_fupd.
iDestruct "Henv" as (X σ HX) "[Hlocks Hσ]". wp_pures.
wp_apply (lreplicate_spec 1 with "[//]"); iIntros (ll Hll).
wp_smart_apply (lreplicate_spec 1 with "[//]"); iIntros (ll Hll).
wp_alloc l as "Hl".
iMod (full_locking_heap_alloc_upd with "Hσ Hl") as (?) "(Hσ & Hinfo & Hl)"=> //=.
iDestruct "Hl" as "[Hl _]".
......
......@@ -90,7 +90,7 @@ Proof.
iInduction vs as [|v' vs] "IH" forall (hd i Hi Hl); destruct i as [|i]=> //; simplify_eq/=.
{ wp_lam. wp_pures. by iApply (lhead_spec with "[//]"). }
wp_lam. wp_pures.
wp_apply (ltail_spec with "[//]"); iIntros (hd' ?). wp_let.
wp_smart_apply (ltail_spec with "[//]"); iIntros (hd' ?). wp_let.
wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l. by iApply "IH".
Qed.
......@@ -100,14 +100,14 @@ Lemma linsert_spec i hd vs v :
Proof.
iIntros ([w Hi] Φ Hl) "HΦ".
iInduction vs as [|v' vs] "IH" forall (hd i Hi Hl Φ); destruct i as [|i]=> //; simplify_eq/=.
{ wp_lam. wp_pures. wp_apply (ltail_spec with "[//]"). iIntros (hd' ?).
{ wp_lam. wp_pures. wp_smart_apply (ltail_spec with "[//]"). iIntros (hd' ?).
wp_let. by iApply (lcons_spec with "[//]"). }
wp_lam; wp_pures.
wp_apply (ltail_spec with "[//]"); iIntros (hd' ?). wp_let.
wp_smart_apply (ltail_spec with "[//]"); iIntros (hd' ?). wp_let.
wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
wp_apply ("IH" with "[//] [//]"). iIntros (hd'' ?). wp_let.
wp_apply (lhead_spec with "[//]"); iIntros "_".
by wp_apply (lcons_spec with "[//]").
wp_smart_apply ("IH" with "[//] [//]"). iIntros (hd'' ?). wp_let.
wp_smart_apply (lhead_spec with "[//]"); iIntros "_".
by wp_smart_apply (lcons_spec with "[//]").
Qed.
Lemma llist_member_spec `{!CmpSpec R cmp} hd vs v :
......@@ -120,7 +120,7 @@ Proof.
iInduction Hvs as [|v' vs] "IH" forall (hd Hl); simplify_eq/=.
{ wp_lam; wp_pures. by iApply "HΦ". }
destruct Hl as (hd'&->&?). wp_lam; wp_pures.
wp_apply (cmp_spec with "[]"); [auto|]; iIntros (_).
wp_smart_apply (cmp_spec with "[]"); [auto|]; iIntros (_).
iEval (rewrite bool_decide_decide). destruct (decide _) as [->|?]; wp_if.
{ rewrite (bool_decide_true (_ _ :: _)); last by left. by iApply "HΦ". }
wp_proj. wp_let. iApply ("IH" with "[//]").
......@@ -137,7 +137,7 @@ Proof.
iApply (lnil_spec with "[//]"). iApply "HΦ". }
wp_lam; wp_pures.
rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
wp_apply "IH"; iIntros (hd' Hl). wp_let. by iApply (lcons_spec with "[//]").
wp_smart_apply "IH"; iIntros (hd' Hl). wp_let. by iApply (lcons_spec with "[//]").
Qed.
Lemma llength_spec hd vs :
......@@ -147,7 +147,7 @@ Proof.
iInduction vs as [|v' vs] "IH" forall (hd Hl Φ); simplify_eq/=.
{ wp_lam. wp_match. by iApply "HΦ". }
destruct Hl as (hd'&->&?). wp_lam. wp_match. wp_proj.
wp_apply ("IH" $! hd' with "[//]"); iIntros "_ /=". wp_op.
wp_smart_apply ("IH" $! hd' with "[//]"); iIntros "_ /=". wp_op.
rewrite (Nat2Z.inj_add 1). by iApply "HΦ".
Qed.
End lists.
......@@ -27,7 +27,7 @@ Section mset.
Lemma mset_create_spec :
{{{ True }}} mset_create #() {{{ x, RET x; is_mset x }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam. wp_apply (lnil_spec with "[//]").
iIntros (Φ) "_ HΦ". wp_lam. wp_smart_apply (lnil_spec with "[//]").
iIntros (hd ?); simplify_eq/=. wp_alloc l as "Hl". iApply "HΦ".
iExists l, _, []. iFrame "Hl". by rewrite /= NoDup_nil.
Qed.
......@@ -41,7 +41,7 @@ Section mset.
iIntros (HX Hv Φ) "Hmut HΦ".
iDestruct "Hmut" as (l hd vs (->&->&?&?)) "Hl". apply set_Forall_list_to_set in HX.
wp_lam; wp_pures. wp_load. wp_let.
wp_apply (llist_member_spec with "[//]"); iIntros "// _".
wp_smart_apply (llist_member_spec with "[//]"); iIntros "// _".
rewrite (bool_decide_iff _ (v vs)); last set_solver.
iApply "HΦ". iExists l, hd, vs; auto.
Qed.
......@@ -55,10 +55,10 @@ Section mset.
Proof.
iIntros (HX Hv ? Φ) "Hmut HΦ".
iDestruct "Hmut" as (l hd vs (->&->&?&?)) "Hl". apply set_Forall_list_to_set in HX.
wp_lam. wp_pures. wp_load. wp_let. wp_apply wp_assert.
wp_apply (llist_member_spec with "[//]"); iIntros "// _".
wp_lam. wp_pures. wp_load. wp_let. wp_smart_apply wp_assert.
wp_smart_apply (llist_member_spec with "[//]"); iIntros "// _".
rewrite bool_decide_false /=; last set_solver. wp_op; iModIntro; iSplit=> //; iIntros "!>".
wp_seq. wp_apply (lcons_spec with "[//]"); iIntros (hd' ?). wp_store.
wp_seq. wp_smart_apply (lcons_spec with "[//]"); iIntros (hd' ?). wp_store.
iApply "HΦ". iExists l, hd', (v :: vs). iFrame "Hl".
rewrite NoDup_cons. iPureIntro; set_solver.
Qed.
......@@ -67,7 +67,7 @@ Section mset.
{{{ is_mset x X }}} mset_clear x {{{ RET #(); is_mset x }}}.
Proof.
iIntros (Φ) "Hmut HΦ". iDestruct "Hmut" as (l hd vs (->&->&?&?)) "Hl".
wp_lam. wp_apply (lnil_spec with "[//]").
wp_lam. wp_smart_apply (lnil_spec with "[//]").
iIntros (hd' ?); simplify_eq/=. wp_store. iApply "HΦ".
iExists l, _, []. iFrame "Hl". by rewrite /= NoDup_nil.
Qed.
......
Supports Markdown
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