Commit 3643ac1d authored by Ralf Jung's avatar Ralf Jung
Browse files

update dependencies; fix for wp_finish changes

parent 33ea6d51
Pipeline #40885 passed with stage
in 19 minutes and 8 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.2020-11-26.2.03b317f4") | (= "dev") }
"coq-iris-heap-lang" { (= "dev.2020-12-04.7.68955c65") | (= "dev") }
]
......@@ -190,7 +190,7 @@ Section cwp_rules.
Proof.
iIntros "Hwp". rewrite cwp_eq /cwp_def. wp_apply (wp_wand with "Hwp").
iIntros (v) "HΦ". wp_lam. wp_pures.
iIntros (γ env l I) "#Hlock Hres #Heq". wp_pures. iFrame.
iIntros "!>" (γ env l I) "#Hlock Hres #Heq". wp_pures. by iFrame.
Qed.
Lemma cwp_bind (f : val) (e : expr) R Φ :
......@@ -200,7 +200,7 @@ Section cwp_rules.
iIntros "Hwp". rewrite cwp_eq /cwp_def.
wp_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).
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 (v) "H". iApply ("H" with "Hflock Hres Heq").
......@@ -211,7 +211,7 @@ Section cwp_rules.
CWP c_atomic ev @ R {{ Φ }}.
Proof.
iIntros "Hwp". rewrite cwp_eq /cwp_def. wp_lam. wp_pures.
iIntros (γ env l I) "#Hlock1 Hres #Heq1". wp_pures.
iIntros "!>" (γ env l I) "#Hlock1 Hres #Heq1". wp_pures.
wp_apply (acquire_flock_spec with "[$]").
iIntros "Hfl".
iMod (flocked_inv_acc with "Hfl") as "[HI Hcl]"; first done.
......@@ -236,7 +236,7 @@ Section cwp_rules.
iMod ("Hcl" with "[HR Henv]") as "Hflocked".
{ iNext. iRewrite "Heq1". iFrame. }
wp_apply (release_cancel_spec with "[$Hlock1 $Hflocked]").
iIntros "$". wp_pures. iFrame.
iIntros "$". wp_pures. by iFrame.
Qed.
Lemma cwp_atomic_env (ev : val) R Φ :
......@@ -245,7 +245,7 @@ Section cwp_rules.
CWP c_atomic_env ev @ R {{ Φ }}.
Proof.
iIntros "Hwp". rewrite cwp_eq /cwp_def. wp_lam. wp_pures.
iIntros (γ env l I) "#Hlock Hres #Heq". wp_pures.
iIntros "!>" (γ env l I) "#Hlock Hres #Heq". wp_pures.
wp_apply (acquire_flock_spec with "[$]").
iIntros "Hfl".
iMod (flocked_inv_acc with "Hfl") as "[HI Hcl]"; first done.
......@@ -258,7 +258,7 @@ Section cwp_rules.
iRewrite "Heq" in "Hcl".
iMod ("Hcl" with "[$HR $Henv]") as "Hflocked".
wp_apply (release_cancel_spec with "[$Hlock $Hflocked]").
iIntros "$". wp_pures. iFrame.
iIntros "$". wp_pures. by iFrame.
Qed.
Lemma cwp_par Ψ1 Ψ2 e1 e2 R Φ :
......@@ -272,7 +272,7 @@ Section cwp_rules.
iIntros (ev2) "Hwp2".
wp_apply (wp_wand with "Hwp1").
iIntros (ev1) "Hwp1". wp_lam. wp_pures.
iIntros (γ env l I) "#Hlock Hres #Heq". wp_pures.
iIntros "!>" (γ env l I) "#Hlock Hres #Heq". wp_pures.
pose (I' := fmap (λ πR, ((πR.1/2)%Qp,πR.2)) I).
iAssert (flock_resources γ I' flock_resources γ I')%I with "[Hres]" as "[Hres1 Hres2]".
{ rewrite /flock_resources -big_sepM_sep.
......@@ -345,7 +345,7 @@ Section cwp_run.
with "Hlock [Henv Hσ]") as (ρ) "[_ Hres]"; first done.
{ iNext. iExists , . iFrame. iPureIntro; set_solver. }
wp_let.
iMod (wp_value_inv with "Hwp") as "Hwp".
rewrite wp_value_fupd. iMod "Hwp" as "Hwp".
iApply (wp_wand with "[Hwp Hres]").
- iApply ("Hwp" $! _ _ _ {[ρ := (1%Qp,_)]} with "Hlock [Hres] []").
+ rewrite /flock_resources big_sepM_singleton //.
......
......@@ -263,7 +263,7 @@ Section proofs.
iIntros "!>" (w1 w2) "H1 H2 !>". cwp_pures.
iDestruct ("HΦ" with "H1 H2") as (n -> ?) "HΦ".
cwp_apply wp_assert. wp_op. rewrite bool_decide_true; last lia.
iSplit; first done. iNext. cwp_pures.
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).
......@@ -299,8 +299,8 @@ 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; iSplit; first done. iNext.
wp_apply wp_assert; wp_pures; iSplit; first done. iNext.
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.
iAssert ( Ψ (n : nat), n length ws
(is_mset env X - Ψ #()) - WP c_free_check env #(cloc_base cl) #n {{ Ψ }})%I
......@@ -316,7 +316,7 @@ Section proofs.
{ destruct (HX (#(cloc_base cl), #n)%V) as (cl'&[= <-]&?); first done.
destruct (Hlocked n); first by (apply lookup_lt_is_Some_2; lia).
destruct cl; simplify_eq/=. by rewrite /cloc_plus /= Z.add_0_r. }
wp_op. iSplit; first done. iNext; wp_pures.
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.
iIntros "!> {$HΦ}". iExists X, _.
......@@ -390,7 +390,7 @@ Section proofs.
{ rewrite /is_loc_nonnull /=; eauto. }
iIntros "Hlocks /=".
rewrite bool_decide_false //.
wp_op. iSplit; first done. iNext; wp_seq.
wp_op. iModIntro. iSplit; first done. iNext; wp_seq.
wp_load; wp_match.
iEval (rewrite -(Z2Nat.id (cloc_offset cl)) //).
iApply wp_fupd.
......
......@@ -57,7 +57,7 @@ Section mset.
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 "// _".
rewrite bool_decide_false /=; last set_solver. wp_op; iSplit=> //; iIntros "!>".
rewrite bool_decide_false /=; last set_solver. wp_op; iModIntro; iSplit=> //; iIntros "!>".
wp_seq. wp_apply (lcons_spec with "[//]"); iIntros (hd' ?). wp_store.
iApply "HΦ". iExists l, hd', (v :: vs). iFrame "Hl".
rewrite NoDup_cons. iPureIntro; set_solver.
......
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