Commit 340e8204 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris + get rid of iAlways.

parent 1b31e552
Pipeline #33099 passed with stage
in 31 minutes and 18 seconds
......@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
"""
depends: [
"coq-iris" { (= "dev.2020-07-15.1.6ae02201") | (= "dev") }
"coq-iris" { (= "dev.2020-07-22.0.1e8432a9") | (= "dev") }
]
build: [make "-j%{jobs}%"]
......
......@@ -268,25 +268,25 @@ Section arc.
iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _). iInv N as (st) "[>H● H]" "Hclose1".
iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
iDestruct (arc_tok_auth_val with "H● Hown") as %(?&strong'&?&?&[-> _]).
iDestruct "H" as (q) "(>#Hq & [HP1 HP1'] & Hl & Hw)". iDestruct "Hq" as %Hq.
iDestruct "H" as (qq) "(>#Hq & [HP1 HP1'] & Hl & Hw)". iDestruct "Hq" as %Hq.
destruct (decide (strong = strong')) as [->|?].
- wp_apply (wp_cas_int_suc with "Hl"). iIntros "Hl".
iMod (own_update with "H●") as "[H● Hown']".
{ apply auth_update_alloc, prod_local_update_1,
(op_local_update_discrete _ _ (Some (Cinl ((q/2)%Qp, 1%positive, None))))
(op_local_update_discrete _ _ (Some (Cinl ((qq/2)%Qp, 1%positive, None))))
=>-[/= Hqa ?]. split;[split|]=>//=; last by rewrite left_id.
apply frac_valid'. rewrite -Hq comm_L -{2}(Qp_div_2 q).
apply frac_valid'. rewrite -Hq comm_L -{2}(Qp_div_2 qq).
apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp).
apply Qcplus_le_mono_r, Qp_ge_0. }
iMod ("Hclose2" with "Hown") as "HP". iModIntro.
iMod ("Hclose1" with "[Hl Hw H● HP1']") as "_".
{ iExists _. iFrame. iExists _. rewrite /= [xH _]comm_L. iFrame.
rewrite [(q / 2)%Qp _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2 left_id_L. auto. }
rewrite [(qq / 2)%Qp _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2 left_id_L. auto. }
iModIntro. wp_case. iApply "HΦ". iFrame.
- wp_apply (wp_cas_int_fail with "Hl"); [congruence|]. iIntros "Hl".
iMod ("Hclose2" with "Hown") as "HP". iModIntro.
iMod ("Hclose1" with "[-HP HΦ]") as "_".
{ iExists _. iFrame. iExists q. auto with iFrame. }
{ iExists _. iFrame. iExists qq. auto with iFrame. }
iModIntro. wp_case. iApply ("IH" with "HP HΦ").
Qed.
......@@ -309,7 +309,7 @@ Section arc.
iApply fupd_wp. iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
iDestruct (arc_tok_auth_val with "H● Hown") as %(?&?& wlock & weak' &[-> _]).
iMod ("Hclose2" with "Hown") as "HP". iModIntro.
iDestruct "H" as (q) "(>Heq & HP1 & Hl & Hl1)". iDestruct "Heq" as %Heq.
iDestruct "H" as (qq) "(>Heq & HP1 & Hl & Hl1)". iDestruct "Heq" as %Heq.
destruct (decide (weak = weak' wlock = None)) as [[<- ->]|Hw].
- wp_apply (wp_cas_int_suc with "Hl1"). iIntros "Hl1".
iMod (own_update with "H●") as "[H● Hown']".
......@@ -509,7 +509,7 @@ Section arc.
iIntros "#INV !# * [Hown HP1] HΦ". iLöb as "IH".
wp_rec. wp_bind (!ˢᶜ_)%E. iInv N as (st) "[>H● H]" "Hclose".
iDestruct (arc_tok_auth_val with "H● Hown") as %(?& s &?&?&[-> _]).
iDestruct "H" as (?) "(? & ? & ? & ?)". wp_read.
iDestruct "H" as (x') "(? & ? & ? & ?)". wp_read.
iMod ("Hclose" with "[-Hown HP1 HΦ]") as "_". { iExists _. auto with iFrame. }
iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _). iInv N as (st) "[>H● H]" "Hclose".
iDestruct (arc_tok_auth_val with "H● Hown") as %(q' & s' & wl & w &[-> Hqq']).
......
......@@ -36,7 +36,7 @@ Section proof.
Proof.
iIntros "#HR !#". iSplit; iIntros "Hlck"; iApply (lock_proto_iff with "[HR] Hlck").
- done.
- iAlways; iSplit; iIntros; by iApply "HR".
- iModIntro; iSplit; iIntros; by iApply "HR".
Qed.
(** The main proofs. *)
......
......@@ -140,7 +140,7 @@ Lemma wp_alloc E (n : Z) :
{{{ l (sz: nat), RET LitV $ LitLoc l; n = sz lsz l ↦∗ repeat (LitV LitPoison) sz }}}.
Proof.
iIntros (? Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 ???) "Hσ !>"; iSplit; first by auto.
iIntros (σ1 κ κs n') "Hσ !>"; iSplit; first by auto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iMod (heap_alloc with "Hσ") as "[Hσ Hl]"; [done..|].
iModIntro; iSplit=> //. iFrame.
......@@ -154,7 +154,7 @@ Lemma wp_free E (n:Z) l vl :
{{{ RET LitV LitPoison; True }}}.
Proof.
iIntros (? Φ) "[>Hmt >Hf] HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 ???) "Hσ".
iIntros (σ1 κ κs n') "Hσ".
iMod (heap_free _ _ _ n with "Hσ Hmt Hf") as "(% & % & Hσ)"=>//.
iModIntro; iSplit; first by auto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
......@@ -166,7 +166,7 @@ Lemma wp_read_sc E l q v :
{{{ RET v; l {q} v }}}.
Proof.
iIntros (?) ">Hv HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 ???) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[n ?].
iIntros (σ1 κ κs n) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[m ?].
iModIntro; iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
......@@ -176,15 +176,15 @@ Lemma wp_read_na E l q v :
{{{ l {q} v }}} Read Na1Ord (Lit $ LitLoc l) @ E
{{{ RET v; l {q} v }}}.
Proof.
iIntros (Φ) ">Hv HΦ". iApply wp_lift_head_step; auto. iIntros (σ1 ???) "Hσ".
iMod (heap_read_na with "Hσ Hv") as (n) "(% & Hσ & Hσclose)".
iIntros (Φ) ">Hv HΦ". iApply wp_lift_head_step; auto. iIntros (σ1 κ κs n) "Hσ".
iMod (heap_read_na with "Hσ Hv") as (m) "(% & Hσ & Hσclose)".
iMod (fupd_intro_mask' _ ) as "Hclose"; first set_solver.
iModIntro; iSplit; first by eauto.
iNext; iIntros (e2 σ2 efs Hstep); inv_head_step. iMod "Hclose" as "_".
iModIntro. iFrame "Hσ". iSplit; last done.
clear dependent σ1 n.
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 ???) "Hσ". iMod ("Hσclose" with "Hσ") as (n) "(% & Hσ & Hv)".
iIntros (σ1 κ' κs' n') "Hσ". iMod ("Hσclose" with "Hσ") as (n) "(% & Hσ & Hv)".
iModIntro; iSplit; first by eauto.
iNext; iIntros (e2 σ2 efs Hstep) "!>"; inv_head_step.
iFrame "Hσ". iSplit; [done|]. by iApply "HΦ".
......@@ -196,7 +196,7 @@ Lemma wp_write_sc E l e v v' :
{{{ RET LitV LitPoison; l v }}}.
Proof.
iIntros (<- Φ) ">Hv HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 ???) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
iIntros (σ1 κ κs n) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
iMod (heap_write _ _ _ v with "Hσ Hv") as "[Hσ Hv]".
iModIntro; iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
......@@ -209,14 +209,14 @@ Lemma wp_write_na E l e v v' :
{{{ RET LitV LitPoison; l v }}}.
Proof.
iIntros (<- Φ) ">Hv HΦ".
iApply wp_lift_head_step; auto. iIntros (σ1 ???) "Hσ".
iApply wp_lift_head_step; auto. iIntros (σ1 κ κs n) "Hσ".
iMod (heap_write_na with "Hσ Hv") as "(% & Hσ & Hσclose)".
iMod (fupd_intro_mask' _ ) as "Hclose"; first set_solver.
iModIntro; iSplit; first by eauto.
iNext; iIntros (e2 σ2 efs Hstep); inv_head_step. iMod "Hclose" as "_".
iModIntro. iFrame "Hσ". iSplit; last done.
clear dependent σ1. iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 ???) "Hσ". iMod ("Hσclose" with "Hσ") as "(% & Hσ & Hv)".
iIntros (σ1 κ' κs' n') "Hσ". iMod ("Hσclose" with "Hσ") as "(% & Hσ & Hv)".
iModIntro; iSplit; first by eauto.
iNext; iIntros (e2 σ2 efs Hstep) "!>"; inv_head_step.
iFrame "Hσ". iSplit; [done|]. by iApply "HΦ".
......@@ -230,7 +230,7 @@ Lemma wp_cas_int_fail E l q z1 e2 lit2 zl :
Proof.
iIntros (<- ? Φ) ">Hv HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 ???) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[n ?].
iIntros (σ1 κ κs n) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[m ?].
iModIntro; iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; inv_lit.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
......@@ -244,7 +244,7 @@ Lemma wp_cas_suc E l lit1 e2 lit2 :
Proof.
iIntros (<- ? Φ) ">Hv HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 ???) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
iIntros (σ1 κ κs n) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
iModIntro; iSplit; first (destruct lit1; by eauto).
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; [inv_lit|].
iMod (heap_write with "Hσ Hv") as "[$ Hv]".
......@@ -274,7 +274,7 @@ Lemma wp_cas_loc_fail E l q q' q1 l1 v1' e2 lit2 l' vl' :
Proof.
iIntros (<- ? Φ) "(>Hl & >Hl' & >Hl1) HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 ???) "Hσ". iDestruct (heap_read with "Hσ Hl") as %[nl ?].
iIntros (σ1 κ κs n) "Hσ". iDestruct (heap_read with "Hσ Hl") as %[nl ?].
iDestruct (heap_read with "Hσ Hl'") as %[nl' ?].
iDestruct (heap_read with "Hσ Hl1") as %[nl1 ?].
iModIntro; iSplit; first by eauto.
......@@ -292,7 +292,7 @@ Lemma wp_cas_loc_nondet E l l1 e2 l2 ll :
Proof.
iIntros (<- Φ) ">Hv HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 ???) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
iIntros (σ1 κ κs n) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
iModIntro; iSplit; first (destruct (decide (ll = l1)) as [->|]; by eauto).
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; last lia.
- inv_lit. iModIntro; iSplit; [done|]; iFrame "Hσ".
......@@ -313,7 +313,7 @@ Proof.
[done|solve_exec_safe|solve_exec_puredet|].
iApply wp_value. by iApply Hpost.
- iApply wp_lift_atomic_head_step_no_fork; subst=>//.
iIntros (σ1 ???) "Hσ1". iModIntro. inv_head_step.
iIntros (σ1 κ κs n') "Hσ1". iModIntro. inv_head_step.
iSplitR.
{ iPureIntro. repeat eexists. econstructor. eapply BinOpEqFalse. by auto. }
(* We need to do a little gymnastics here to apply Hne now and strip away a
......
......@@ -30,7 +30,7 @@ Section frac_bor.
( q, φ q φ' q) - &frac{κ} φ - &frac{κ} φ'.
Proof.
iIntros "#Hφφ' H". iDestruct "H" as (γ κ') "[? Hφ]". iExists γ, κ'. iFrame.
iApply (at_bor_iff with "[Hφφ'] Hφ"). iNext. iAlways.
iApply (at_bor_iff with "[Hφφ'] Hφ"). iNext. iModIntro.
iSplit; iIntros "H"; iDestruct "H" as (q) "[H ?]"; iExists q; iFrame; by iApply "Hφφ'".
Qed.
......@@ -137,7 +137,7 @@ End frac_bor.
Lemma frac_bor_lft_incl `{!invG Σ, !lftG Σ, !frac_borG Σ} κ κ' q:
lft_ctx - &frac{κ}(λ q', (q * q').[κ']) - κ κ'.
Proof.
iIntros "#LFT#Hbor". iApply lft_incl_intro. iAlways. iSplitR.
iIntros "#LFT#Hbor". iApply lft_incl_intro. iModIntro. iSplitR.
- iIntros (q') "Hκ'".
iMod (frac_bor_acc with "LFT Hbor Hκ'") as (q'') "[>? Hclose]". done.
iExists _. iFrame. iIntros "!>Hκ'". iApply "Hclose". auto.
......
......@@ -111,7 +111,7 @@ Qed.
Lemma bor_iff_proper κ P P': (P P') - (&{κ}P &{κ}P').
Proof.
iIntros "#HP !#". iSplit; iIntros "?"; iApply bor_iff; try done.
iNext. iAlways. iSplit; iIntros "?"; iApply "HP"; done.
iNext. iModIntro. iSplit; iIntros "?"; iApply "HP"; done.
Qed.
Lemma bor_later E κ P :
......
......@@ -120,7 +120,7 @@ Proof.
iAssert (&{κ}(P Q))%I with "[H◯ Hslice]" as "$".
{ rewrite /bor /raw_bor /idx_bor_own. iExists (κ1 κ2).
iSplit; first by iApply (lft_incl_glb with "Hκ1 Hκ2").
iExists γ. iFrame. iExists _. iFrame. iNext. iAlways.
iExists γ. iFrame. iExists _. iFrame. iNext. iModIntro.
by iSplit; iIntros "[HP HQ]"; iSplitL "HP"; (iApply "HPP'" || iApply "HQQ'"). }
iApply "Hclose". iExists A, I. iFrame. rewrite big_sepS_later.
iApply "Hclose'". iLeft. iFrame "%". iExists Pb, Pi. iFrame. iExists _.
......
......@@ -71,7 +71,7 @@ Proof.
pose (Kalive := filter (lft_alive_in A) K).
destruct (decide (Kalive = )) as [HKalive|].
{ iModIntro. rewrite /Iinv. iFrame.
iApply (@big_sepS_impl with "[$HK]"); iAlways.
iApply (@big_sepS_impl with "[$HK]"); iModIntro.
rewrite /lft_inv. iIntros (κ Hκ) "[[[_ %]|[$ _]] _]". set_solver. }
destruct (minimal_exists_L () Kalive)
as (κ & [Hκalive HκK]%elem_of_filter & Hκmin); first done.
......@@ -122,7 +122,7 @@ Proof.
{ iNext. rewrite /lfts_inv /own_alft_auth.
iExists (<[Λ:=true]>A), I. rewrite /to_alftUR fmap_insert; iFrame.
iApply (@big_sepS_impl with "[$Hinv]").
iAlways. rewrite /lft_inv. iIntros (κ ?) "[[Hκ %]|[Hκ %]]".
iModIntro. rewrite /lft_inv. iIntros (κ ?) "[[Hκ %]|[Hκ %]]".
- iLeft. iFrame "Hκ". iPureIntro. by apply lft_alive_in_insert.
- iRight. iFrame "Hκ". iPureIntro. by apply lft_dead_in_insert. }
iModIntro; iExists {[ Λ ]}.
......
......@@ -386,14 +386,14 @@ Lemma raw_bor_iff i P P' : ▷ □ (P ↔ P') -∗ raw_bor i P -∗ raw_bor i P'
Proof.
iIntros "#HPP' HP". unfold raw_bor. iDestruct "HP" as (s) "[HiP HP]".
iExists s. iFrame. iDestruct "HP" as (P0) "[#Hiff ?]". iExists P0. iFrame.
iNext. iAlways. iSplit; iIntros.
iNext. iModIntro. iSplit; iIntros.
by iApply "HPP'"; iApply "Hiff". by iApply "Hiff"; iApply "HPP'".
Qed.
Lemma idx_bor_iff κ i P P' : (P P') - &{κ,i}P - &{κ,i}P'.
Proof.
unfold idx_bor. iIntros "#HPP' [$ HP]". iDestruct "HP" as (P0) "[#HP0P Hs]".
iExists P0. iFrame. iNext. iAlways. iSplit; iIntros.
iExists P0. iFrame. iNext. iModIntro. iSplit; iIntros.
by iApply "HPP'"; iApply "HP0P". by iApply "HP0P"; iApply "HPP'".
Qed.
......
......@@ -276,7 +276,7 @@ Section typing.
+ iApply "HE'". iIntros "{$# Hf Hinh HE' LFT HE %}".
iInduction κs as [|κ κs] "IH"=> //=. iSplitL.
{ iApply lft_incl_trans; first done. iApply lft_intersect_incl_l. }
iApply "IH". iAlways. iApply lft_incl_trans; first done.
iApply "IH". iModIntro. iApply lft_incl_trans; first done.
iApply lft_intersect_incl_r.
+ iSplitL; last done. iExists ϝ. iSplit; first by rewrite /= left_id.
iFrame "#∗".
......
......@@ -151,7 +151,7 @@ Section arc.
Next Obligation.
iIntros (ty κ κ' tid l) "#Hincl H". iDestruct "H" as (l') "[#Hl #Hshr]".
iExists _. iSplit; first by iApply frac_bor_shorten.
iAlways. iIntros (F q) "% Htok".
iModIntro. iIntros (F q) "% Htok".
iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose]"; first solve_ndisj.
iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
......@@ -178,7 +178,7 @@ Section arc.
type_incl ty1 ty2 - type_incl (arc ty1) (arc ty2).
Proof.
iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
iSplit; first done. iSplit; iAlways.
iSplit; first done. iSplit; iModIntro.
- iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
iDestruct "Hvl" as "[(Hl1 & Hl2 & H† & Hc) | Hvl]".
{ iLeft. iFrame. iDestruct "Hsz" as %->.
......@@ -266,7 +266,7 @@ Section arc.
Next Obligation.
iIntros (ty κ κ' tid l) "#Hincl H". iDestruct "H" as (l') "[#Hl #Hshr]".
iExists _. iSplit; first by iApply frac_bor_shorten.
iAlways. iIntros (F q) "% Htok".
iModIntro. iIntros (F q) "% Htok".
iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose]"; first solve_ndisj.
iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
......@@ -291,7 +291,7 @@ Section arc.
type_incl ty1 ty2 - type_incl (weak ty1) (weak ty2).
Proof.
iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
iSplit; first done. iSplit; iAlways.
iSplit; first done. iSplit; iModIntro.
- iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
iDestruct "Hvl" as (γ ν) "(#Hpersist & Htk)".
iExists _, _. iFrame "#∗". by iApply arc_persist_type_incl.
......@@ -783,9 +783,9 @@ Section arc.
{ iIntros "_". wp_if. unlock. iFrame. iExists (_::_). rewrite heap_mapsto_vec_cons.
iFrame. iExists 1%nat, _, []. rewrite /= right_id_L Max.max_0_r.
auto 10 with iFrame. }
iIntros "([H† H1] & H2 & H3)". iDestruct "H1" as (vl') "[H1 Heq]".
iIntros "([H† H1] & H2 & H3)". iDestruct "H1" as (vl1) "[H1 Heq]".
iDestruct "Heq" as %<-. wp_if.
wp_apply (wp_delete _ _ _ (_::_::vl') with "[H1 H2 H3 H†]").
wp_apply (wp_delete _ _ _ (_::_::vl1) with "[H1 H2 H3 H†]").
{ simpl. lia. }
{ rewrite 2!heap_mapsto_vec_cons shift_loc_assoc. auto with iFrame. }
iFrame. iIntros "_". iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame.
......
......@@ -39,7 +39,7 @@ Section cell.
iDestruct ("EQ" with "HE") as "(% & #Hown & #Hshr)".
iSplit; [done|iSplit; iIntros "!# * H"].
- iApply ("Hown" with "H").
- iApply na_bor_iff; last done. iNext; iAlways; iSplit; iIntros "H";
- iApply na_bor_iff; last done. iNext; iModIntro; iSplit; iIntros "H";
iDestruct "H" as (vl) "[??]"; iExists vl; iFrame; by iApply "Hown".
Qed.
Lemma cell_mono' E L ty1 ty2 : eqtype E L ty1 ty2 subtype E L (cell ty1) (cell ty2).
......
......@@ -101,7 +101,7 @@ Section mutex.
iExists _. iFrame "Hincl". iApply (at_bor_iff with "[] Hshr"). iNext.
iApply lock_proto_iff_proper. iApply bor_iff_proper. iNext.
iApply heap_mapsto_pred_iff_proper.
iAlways; iIntros; iSplit; iIntros; by iApply "Howni".
iModIntro; iIntros; iSplit; iIntros; by iApply "Howni".
Qed.
Global Instance mutex_proper E L :
......@@ -122,7 +122,7 @@ Section mutex.
iExists _. iFrame "Hincl". iApply (at_bor_iff with "[] Hshr"). iNext.
iApply lock_proto_iff_proper. iApply bor_iff_proper. iNext.
iApply heap_mapsto_pred_iff_proper.
iAlways; iIntros; iSplit; iIntros; by iApply send_change_tid.
iModIntro; iIntros; iSplit; iIntros; by iApply send_change_tid.
Qed.
End mutex.
......
......@@ -91,7 +91,7 @@ Section mguard.
intros α1 α2 Hα ty1 ty2 Hty. generalize Hty. rewrite eqtype_unfold. iIntros (Hty' q) "HL".
iDestruct (Hty' with "HL") as "#Hty". clear Hty'. iDestruct (Hα with "HL") as "#Hα".
iIntros "!# #HE". iDestruct ("Hα" with "HE") as "{Hα} Hα".
iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs) {HE Hty}". iSplit; [done|iSplit; iAlways].
iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs) {HE Hty}". iSplit; [done|iSplit; iModIntro].
- iIntros (tid [|[[]|][]]) "H"; try done. simpl.
iDestruct "H" as (β) "(#H⊑ & #Hinv & Hown)".
iExists β. iFrame. iSplit; last iSplit.
......@@ -100,10 +100,10 @@ Section mguard.
iApply (at_bor_iff with "[] Hinv"). iNext.
iApply lock_proto_iff_proper. iApply bor_iff_proper. iNext.
iApply heap_mapsto_pred_iff_proper.
iAlways; iIntros; iSplit; iIntros; by iApply "Ho".
iModIntro; iIntros; iSplit; iIntros; by iApply "Ho".
+ iApply bor_iff; last done. iNext.
iApply heap_mapsto_pred_iff_proper.
iAlways; iIntros; iSplit; iIntros; by iApply "Ho".
iModIntro; iIntros; iSplit; iIntros; by iApply "Ho".
- iIntros (κ tid l) "H". iDestruct "H" as (l') "H". iExists l'.
iDestruct "H" as "[$ #H]". iIntros "!# * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
......
......@@ -184,7 +184,7 @@ Section rc.
Next Obligation.
iIntros (ty κ κ' tid l) "#Hincl H". iDestruct "H" as (l') "[#Hl #Hshr]".
iExists _. iSplit; first by iApply frac_bor_shorten.
iAlways. iIntros (F q) "% Htok".
iModIntro. iIntros (F q) "% Htok".
iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose]"; first solve_ndisj.
iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
......@@ -211,7 +211,7 @@ Section rc.
type_incl ty1 ty2 - type_incl (rc ty1) (rc ty2).
Proof.
iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
iSplit; first done. iSplit; iAlways.
iSplit; first done. iSplit; iModIntro.
- iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
iDestruct "Hvl" as "[(Hl1 & Hl2 & H† & Hc) | Hvl]".
{ iLeft. iFrame. iDestruct "Hsz" as %->.
......@@ -689,7 +689,7 @@ Section code.
iApply (type_cont [] [ϝ ⊑ₗ []]
(λ _, [rcx box (uninit 1); r box (Σ[ ty; rc ty ])])) ;
[solve_typing..| |]; last first.
{ simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
{ simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing. }
iIntros (k). simpl_subst.
......@@ -784,7 +784,7 @@ Section code.
iApply (type_cont [] [ϝ ⊑ₗ []]
(λ _, [rcx box (uninit 1); r box (option ty)]));
[solve_typing..| |]; last first.
{ simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
{ simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing. }
iIntros (k). simpl_subst.
......@@ -874,7 +874,7 @@ Section code.
iApply (type_cont [] [ϝ ⊑ₗ []]
(λ _, [rcx box (uninit 1); r box (option $ &uniq{α}ty)]));
[solve_typing..| |]; last first.
{ simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
{ simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing. }
iIntros (k). simpl_subst.
......@@ -1006,7 +1006,7 @@ Section code.
iApply (type_cont [] [ϝ ⊑ₗ []]
(λ _, [rcx box (uninit 1); r box (&uniq{α}ty)]));
[solve_typing..| |]; last first.
{ simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
{ simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing. }
iIntros (k). simpl_subst.
......
......@@ -57,7 +57,7 @@ Section weak.
Next Obligation.
iIntros (ty κ κ' tid l) "#Hincl H". iDestruct "H" as (l') "[#Hl #Hshr]".
iExists _. iSplit; first by iApply frac_bor_shorten.
iAlways. iIntros (F q) "% Htok".
iModIntro. iIntros (F q) "% Htok".
iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose]"; first solve_ndisj.
iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
......@@ -82,7 +82,7 @@ Section weak.
type_incl ty1 ty2 - type_incl (weak ty1) (weak ty2).
Proof.
iIntros "#Hincl". iPoseProof "Hincl" as "(Hsz & #Hoincl & #Hsincl)".
iSplit; first done. iSplit; iAlways.
iSplit; first done. iSplit; iModIntro.
- iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
iDestruct "Hvl" as (γ ν) "(#Hpersist & Htok)".
iExists _, _. iFrame "Htok". by iApply rc_persist_type_incl.
......@@ -132,7 +132,7 @@ Section code.
iApply (type_cont [] [ϝ ⊑ₗ []]
(λ _, [w box (&shr{α}(weak ty)); r box (option (rc ty))])) ;
[solve_typing..| |]; last first.
{ simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
{ simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing. }
iIntros (k). simpl_subst.
......@@ -380,7 +380,7 @@ Section code.
iIntros (_ ϝ ret arg). inv_vec arg=>w. simpl_subst.
iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [w box (uninit 1)]));
[solve_typing..| |]; last first.
{ simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
{ simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing. }
......
......@@ -83,7 +83,7 @@ Section ref.
iIntros (α1 α2 Hα ty1 ty2 Hty q) "HL".
iDestruct (Hty with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iAlways].
iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iModIntro].
- done.
- iIntros (tid [|[[]|][|[[]|][]]]) "H"=>//=.
iDestruct "H" as (ν q' γ β ty') "(#Hshr & #H⊑ & #Hinv & Htok & Hown)".
......
......@@ -317,8 +317,8 @@ Section ref_functions.
iDestruct ("Hclose3" with "Hαν") as "[Hα Hν]".
iMod ("Hclose2" with "Hϝ HL") as "HL".
wp_rec. iDestruct "Hr" as "[Hr Hr†]".
iDestruct "Hr" as (?) "[Hr H]". iDestruct "H" as (vl1 ? ->) "[#Hr1' H]".
iDestruct "H" as (vl2 ? ->) "[#Hr2' ->]".
iDestruct "Hr" as (?) "[Hr H]". iDestruct "H" as (vl1 vl1' ->) "[#Hr1' H]".
iDestruct "H" as (vl2 vl2' ->) "[#Hr2' ->]".
destruct vl1 as [|[[|lr1|]|] []], vl2 as [|[[|lr2|]|] []]=>//=.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iDestruct "Hr" as "[Hr1 Hr2]". wp_read. wp_let. wp_op. wp_read. wp_let.
......@@ -330,15 +330,15 @@ Section ref_functions.
iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hclosena)"; [done..|].
wp_seq. wp_op. wp_read.
iDestruct (refcell_inv_reading_inv with "INV Hγ")
as (q' n) "(H↦lrc & _ & [H● H◯] & H† & Hq' & Hshr')".
iDestruct "Hq'" as (q'') "(Hq'q'' & Hν1 & Hν2)".
iDestruct "Hq'q''" as %Hq'q''. iMod (own_update with "H●") as "[H● ?]".
as (q1 n) "(H↦lrc & _ & [H● H◯] & H† & Hq1 & Hshr')".
iDestruct "Hq1" as (q2) "(Hq1q2 & Hν1 & Hν2)".
iDestruct "Hq1q2" as %Hq1q2. iMod (own_update with "H●") as "[H● ?]".
{ apply auth_update_alloc,
(op_local_update_discrete _ _ (reading_stR (q''/2)%Qp ν))=>-[Hagv _].
(op_local_update_discrete _ _ (reading_stR (q2/2)%Qp ν))=>-[Hagv _].
split; [split|done].
- by rewrite /= agree_idemp.
- apply frac_valid'. rewrite -Hq'q'' comm -{2}(Qp_div_2 q'').
apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q''/2)%Qp).
- apply frac_valid'. rewrite -Hq1q2 comm -{2}(Qp_div_2 q2).
apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q2/2)%Qp).
apply Qcplus_le_mono_r, Qp_ge_0. }
wp_let. wp_read. wp_let. wp_op. wp_write.
wp_apply (wp_delete _ _ _ [_; _] with "[Href↦1 Href↦2 Href†]")=>//.
......
......@@ -81,7 +81,7 @@ Section refcell_inv.
iAssert ( (&{α}((l + 1) ↦∗: ty_own ty1 tid) -
&{α}((l + 1) ↦∗: ty_own ty2 tid)))%I as "#Hb".
{ iIntros "!# H". iApply bor_iff; last done.
iNext; iAlways; iSplit; iIntros "H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
iNext; iModIntro; iSplit; iIntros "H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
iFrame; by iApply "Hown". }
iDestruct "H" as (st) "H"; iExists st;
iDestruct "H" as "($&$&H)"; destruct st as [[[[ν rw] q' ] n]|]; try done;
......@@ -192,7 +192,7 @@ Section refcell.
- iPureIntro. simpl. congruence.
- destruct vl as [|[[]|]]=>//=. by iApply "Hown".
- simpl. iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
iApply na_bor_iff; last done. iNext; iAlways; iSplit; iIntros "H".
iApply na_bor_iff; last done. iNext; iModIntro; iSplit; iIntros "H".
by iApply "Hty1ty2". by iApply "Hty2ty1".
Qed.
Lemma refcell_mono' E L ty1 ty2 :
......
......@@ -88,14 +88,14 @@ Section refmut.
intros α1 α2 Hα ty1 ty2. rewrite eqtype_unfold=>Hty. iIntros (q) "HL".
iDestruct (Hty with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iAlways].
iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iModIntro].
- done.
- iIntros (tid [|[[]|][|[[]|][]]]) "H"=>//=.
iDestruct "H" as (ν γ q' β ty') "(Hb & #H⊑ & #Hinv & Hν & Hown)".
iExists ν, γ, q', β, ty'. iFrame "∗#". iSplit.
+ iApply bor_shorten; last iApply bor_iff; last done.
* iApply lft_intersect_mono; first done. iApply lft_incl_refl.
* iNext; iAlways; iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
* iNext; iModIntro; iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
iExists vl; iFrame; by iApply "Ho".
+ by iApply lft_incl_trans.
- iIntros (κ tid l) "H /=". iDestruct "H" as (lv lrc) "H". iExists lv, lrc.
......
......@@ -287,8 +287,8 @@ Section refmut_functions.
iDestruct ("Hclose3" with "Hαν") as "[Hα Hν]".
iMod ("Hclose2" with "Hϝ HL") as "HL".
wp_rec. iDestruct "Hr" as "[Hr Hr†]".
iDestruct "Hr" as (?) "[Hr H]". iDestruct "H" as (vl1 ? ->) "[Hr1' H]".
iDestruct "H" as (vl2 ? ->) "[Hr2' ->]".