Commit db6938b7 authored by Hai Dang's avatar Hai Dang
Browse files

Use more IPM features

parent c5e9e125
......@@ -123,7 +123,7 @@ Lemma iwp_alloc E n 𝓥:
(l ↦∗ repeat # (Z.to_nat n)
[ list] i seq 0 (Z.to_nat n), meta_token (l >> i) ) 𝓥'.(cur) }}}.
Proof.
iIntros (SUB ? Φ) ">#Seen HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (SUB ? Φ) ">Seen HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 ? κ κs ?) "Hσ".
iMod (hist_interp_seen_wf _ _ _ SUB with "Hσ Seen") as "[Hσ [%WF %HC]]".
iModIntro. iSplit; [iPureIntro|iNext].
......@@ -143,7 +143,7 @@ Proof.
by rewrite -Z2Nat.inj_pos Z2Pos.id.
rewrite Eqn. iFrame.
inversion_clear PStep. rewrite Eqn /= in ALLOC.
rewrite cell_list_fmap big_sepL_fmap /=. iClear "Seen".
rewrite cell_list_fmap big_sepL_fmap /=.
rewrite (_:∀ n l, (l ↦∗{1} repeat # n)
[ list] k_ seq 0 n, ((l >> k) #)); last first.
{ clear. induction n=>/= l.
......@@ -154,8 +154,8 @@ Proof.
+ apply list_eq=>i. rewrite !list_lookup_fmap.
destruct (decide (i < n)%nat).
* rewrite !lookup_seq_lt //. * rewrite !lookup_seq_ge //; lia. }
iCombine "Hists" "Hars" as "Hists". iCombine "Hists" "Haws" as "Hists".
iCombine "Hists" "Hnas" as "Hists". rewrite -4!big_sepL_sep monPred_at_big_sepL.
iCombine "Hists Hars Haws Hnas" as "Hists".
rewrite -4!big_sepL_sep monPred_at_big_sepL.
iApply (big_sepL_mono with "Hists").
move => n1 n2 /lookup_seq [/= -> Lt].
destruct (lookup_lt_is_Some_2 𝑚s n1) as [𝑚 Eq𝑚];
......@@ -164,7 +164,7 @@ Proof.
(alloc_step_mem_lookup _ _ _ _ _ _ _ ALLOC 𝑚
(elem_of_list_lookup_2 _ _ _ Eq𝑚)).
have EqVal := alloc_step_AVal _ _ _ _ _ _ _ ALLOC _ _ Eq𝑚.
iIntros "((((Hist & Meta & %) & ar) & aw) & na)".
iIntros "((Hist & Meta & %) & ar & aw & na)".
rewrite meta_token_eq. iFrame "Meta".
iExists _, _. iSplitL "Hist ar aw na".
+ iExists ,,. iFrame. iPureIntro.
......@@ -290,8 +290,8 @@ Proof.
iDestruct (hist_ctx_read with "Hσ hist") as "#VS".
assert ( tr, ot = Some tr 𝑚s = []) as [tr [? ?]].
{ inversion_clear DRFPost. by eexists. } subst ot 𝑚s.
iDestruct ("VS" $! (mkGB 𝓢' 𝓝' M') with "[%] ana") as "[FACTS VS1]"; [done|].
iClear "VS". iMod ("VS1" with "Hσ") as "(Hσ' & seen' & ana')".
iDestruct ("VS" $! (mkGB 𝓢' 𝓝' M') with "[%] ana") as "{VS} [FACTS VS]"; [done|].
iMod ("VS" with "Hσ") as "(Hσ' & seen' & ana')".
iMod ("HClose" with "Hσ'") as "$".
iModIntro; iSplit; [done|].
iDestruct "FACTS" as %(LEV&?&t&m&?&Eqv&RH&?).
......@@ -431,17 +431,17 @@ Proof.
iIntros (v2 σ2 efs Hstep); inv_head_step.
assert ( 𝑚, ot = None 𝑚s = [𝑚]) as [𝑚 [? ?]].
{ inversion_clear DRFPost. by eexists. } subst ot 𝑚s.
iDestruct ("VS" $! (mkGB 𝓢' 𝓝' M') with "[%] aw") as (C' t' [Ext1 Ext2]) "VS1".
iDestruct ("VS" $! (mkGB 𝓢' 𝓝' M') with "[%] aw") as (C' t' [Ext1 Ext2]) "{VS} VS".
{ split; [done|]. split; last split; last split;
[..|done|split]; [..|by inversion DRFPost|by inversion DRFPost|done].
assert (DRF: drf_pre σ1.(na) 𝓥 σ1.(mem) (event.Write l v o)).
{ eapply (DRFPre _ _ []); eauto. constructor. by apply to_of_val. }
by inversion DRF. }
iClear "VS". iSpecialize ("HΦ" $! 𝓥' C' t' with "[%]"); [done|].
iMod "HΦ" as "HΦ". iIntros "!> !>". iMod "HΦ" as "HΦ".
iSpecialize ("HΦ" $! 𝓥' C' t' with "[%]"); [done|].
iMod "HΦ". iIntros "!> !>". iMod "HΦ".
(* accessing hist_ctx *)
iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
iMod ("VS1" with "Hσ hist") as "(Hσ' & hist' & aw & seen')".
iMod ("VS" with "Hσ hist") as "(Hσ' & hist' & aw & seen')".
iDestruct (hist_ctx_hist_good with "Hσ' hist'") as %WFC'.
iMod ("HClose" with "Hσ'") as "$".
(* done accessing hist_ctx *)
......@@ -624,8 +624,8 @@ Proof.
- iClear "VSC".
assert ( tr, ot = Some tr 𝑚s = []) as [tr [? ?]].
{ inversion_clear DRFPost. by eexists. } subst ot 𝑚s.
iDestruct ("VSR" $! (mkGB 𝓢' 𝓝' M') with "[%] [ar]") as "[FACTS VS1]";
[done|by rewrite decide_True|..]. iClear "VSR".
iDestruct ("VSR" $! (mkGB 𝓢' 𝓝' M') with "[%] [ar]") as "[FACTS VS] {VSR}";
[done|by rewrite decide_True|..].
iDestruct "FACTS" as %(Ext & ? & t & m & Eqm & Eqvo & RH & ?).
iSpecialize ("HΦ" $! false _ _ _ C with "[%]").
{ split; [done|]. do 2 eexists. do 4 (split; [done|]). split; [|left].
......@@ -634,21 +634,21 @@ Proof.
- repeat split; auto.
eapply (atw_local_mono _ ws ws); [done| |apply ATW]. by solve_lat. }
iDestruct "HΦ" as (P) "(P & _ & HΦ)".
iSpecialize ("HΦ" with "[%] P"); [done|]. iMod "HΦ" as "HΦ".
iIntros "!> !>". iMod "HΦ" as "HΦ".
iSpecialize ("HΦ" with "[%] P"); [done|]. iMod "HΦ".
iIntros "!> !>". iMod "HΦ".
(* accessing hist_ctx *)
iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
iMod ("VS1" with "Hσ") as "[Hσ' [seen' ar]]". rewrite decide_True; [|done].
iMod ("VS" with "Hσ") as "[Hσ' [seen' ar]]". rewrite decide_True; [|done].
iMod ("HClose" with "Hσ'") as "$". iModIntro. iSplitL "";[done|].
by iApply ("HΦ" with "seen' hist ar na aw").
- iClear "VSR".
assert ( tr 𝑚, ot = Some tr 𝑚s = [𝑚]) as [tr [𝑚 [? ?]]].
{ inversion_clear DRFPost. by do 2 eexists. } subst ot 𝑚s.
iDestruct ("VSC" $! (mkGB 𝓢' 𝓝' M') with "[%] ar aw") as (C') "[FACTS VS1]".
iDestruct ("VSC" $! (mkGB 𝓢' 𝓝' M') with "[%] ar aw") as (C') "[FACTS VS] {VSC}".
{ split; [done|]. split; last split; last split;
[..|done|done|split]; [..|by inversion DRFPost|done].
eapply (DRFPre _ _ []); eauto. eapply CasSucS; eauto. by apply to_of_val. }
iClear "VSC". iDestruct "FACTS" as
iDestruct "FACTS" as
%(GH&t'&m'&𝓥x&Eqm&?&?&Extx&RH&m&?&EQT&?&?&?&?&?&?&?&?&RLX&ACQ&WH).
have ?: atw_local l (ws {[𝑚.(mto)]}) (Vw 𝓥'.(cur)).
{ by eapply write_helper_atw_local; eauto. }
......@@ -663,20 +663,20 @@ Proof.
| H : lit_eq _ _ _ |- _ => inversion H as [| |lr|lr]; clear H
end.
+ iMod ("HΦ" with "[%//] P") as "HΦ".
iIntros "!> !>". iMod "HΦ" as "HΦ".
iIntros "!> !>". iMod "HΦ".
(* accessing hist_ctx *)
iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
iMod ("VS1" with "Hσ hist") as "(Hσ' & hist' & at' & aw' & seen')".
iMod ("VS" with "Hσ hist") as "(Hσ' & hist' & at' & aw' & seen')".
iDestruct (hist_ctx_hist_good with "Hσ' hist'") as %WFC'.
iMod ("HClose" with "Hσ'") as "$".
(* done accessing hist_ctx *)
iModIntro. iSplit; [done|]. rewrite EQT.
by iApply ("HΦ" with "seen' hist' at' na aw' [%]").
+ iMod ("HΦ" with "[%] P") as "HΦ"; [done|].
iIntros "!> !>". iMod "HΦ" as "HΦ".
iIntros "!> !>". iMod "HΦ".
(* accessing hist_ctx *)
iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
iMod ("VS1" with "Hσ hist") as "(Hσ' & hist' & at' & aw' & seen')".
iMod ("VS" with "Hσ hist") as "(Hσ' & hist' & at' & aw' & seen')".
iDestruct (hist_ctx_hist_good with "Hσ' hist'") as %WFC'.
iMod ("HClose" with "Hσ'") as "$".
(* done accessing hist_ctx *)
......
......@@ -563,8 +563,8 @@ Section hist.
Proof.
iDestruct 1 as (hF V Vc) "(_ & _ & _ & _ & _ & _ & oA & wf)".
iDestruct "wf" as %(_ & ? & ? & ?).
rewrite seen_eq. iIntros "oV". iCombine "oA" "oV" as "oA".
iDestruct (own_valid with "oA")
rewrite seen_eq. iIntros "oV".
iDestruct (own_valid_2 with "oA oV")
as %[Le%latT_included _]%auth_both_valid_discrete. simpl in Le.
iPureIntro. apply closed_tview_acq_inv. by rewrite Le.
Qed.
......@@ -1038,20 +1038,17 @@ Section hist.
iMod (gen_heap_update with "own1 hist") as "[$ hist]".
iApply (mapsto_persist with "hist").
- iDestruct (hist_ctx_atread_full with "[$oar $atr]") as %Eqrs.
rewrite atread_eq. iCombine "oar" "atr" as "oar".
rewrite -own_op own_update; [eauto|apply auth_update].
rewrite /= to_atr_insert EqLoc shift_0.
rewrite atread_eq -own_op. iApply (own_update_2 with "oar atr").
apply auth_update. rewrite /= to_atr_insert EqLoc shift_0.
eapply (singleton_local_update), exclusive_local_update; [|done].
by apply to_atr_lookup_r_Some.
- iDestruct (hist_ctx_atwrite_agree_1 with "[$oaw $atw]") as %Eqrs.
rewrite atwrite_eq. iCombine "oaw" "atw" as "oaw".
rewrite -own_op own_update; [eauto|apply auth_update].
rewrite /= to_atw_insert EqLoc shift_0.
rewrite atwrite_eq -own_op. iApply (own_update_2 with "oaw atw").
apply auth_update. rewrite /= to_atw_insert EqLoc shift_0.
eapply singleton_local_update; [done|by apply exclusive_local_update].
- iDestruct (hist_ctx_naread_full with "[$ona $nar]") as %Eqrs.
rewrite naread_eq. iCombine "ona" "nar" as "ona".
rewrite -own_op own_update; [eauto|apply auth_update].
rewrite /= to_nar_insert EqLoc shift_0.
rewrite naread_eq -own_op. iApply (own_update_2 with "ona nar").
apply auth_update. rewrite /= to_nar_insert EqLoc shift_0.
eapply singleton_local_update, exclusive_local_update; [|done].
by apply to_nar_lookup_r_Some.
Qed.
......@@ -1157,7 +1154,7 @@ Section hist.
iDestruct (hist_ctx_hist_good with "ctx hist") as %WFC.
iDestruct "ctx" as (hF V Vc) "(Hhσ & HhF & Hna & Haw & Har & Hsc & HV & HF)".
iDestruct "HF" as %(WF & HhF & HC & LE).
iIntros "!#" (𝓥 𝓥' 𝑚 o tr (Eql & STEP & ALL & CLOSED)). subst l.
iIntros "!>" (𝓥 𝓥' 𝑚 o tr (Eql & STEP & ALL & CLOSED)). subst l.
have EXT: 𝓥 𝓥' by eapply read_step_tview_sqsubseteq.
iSplitL "".
- iPureIntro. split; [done|]. inversion_clear STEP.
......@@ -1187,8 +1184,8 @@ Section hist.
iDestruct (hist_ctx_naread_included with "[$oA $or]") as %SUB.
destruct (𝓝 !! l) as [[?? rsm]|] eqn:Eql; last first.
{ by rewrite (view_lookup_nr' _ _ _ Eql) in SUB. }
rewrite naread_eq. iCombine "oA" "or" as "oAr". rewrite -own_op.
iApply (own_update with "oAr"). apply auth_update.
rewrite naread_eq -own_op. iApply (own_update_2 with "oA or").
apply auth_update.
rewrite (to_nar_add_nread_id _ _ _ rsm); last by eapply view_lookup_nr.
eapply singleton_local_update; first by eapply to_nar_lookup_Some.
by apply (frac_lat_local_update _ _ rsm rs {[tr]}).
......@@ -1220,8 +1217,8 @@ Section hist.
iDestruct (hist_ctx_atread_included with "[$oA $or]") as %SUB.
destruct (𝓝 !! l) as [[??? rsm]|] eqn:Eql; last first.
{ by rewrite (view_lookup_ar' _ _ _ Eql) in SUB. }
rewrite atread_eq. iCombine "oA" "or" as "oAr". rewrite -own_op.
iApply (own_update with "oAr"). apply auth_update.
rewrite atread_eq -own_op.
iApply (own_update_2 with "oA or"). apply auth_update.
rewrite (to_atr_add_aread_id _ _ _ rsm); last by eapply view_lookup_ar.
eapply singleton_local_update; first by eapply to_atr_lookup_Some.
by apply (frac_lat_local_update _ _ rsm rs {[tr]}).
......@@ -1262,13 +1259,13 @@ Section hist.
Proof.
iIntros "ctx hist".
iDestruct (hist_ctx_read_msg with "ctx hist") as "#VS".
iIntros "!#" (σ' 𝓥 𝓥' v o q' tr rs (STEP & DRF & ALL & CLOSED)).
iIntros "!>" (σ' 𝓥 𝓥' v o q' tr rs (STEP & DRF & ALL & CLOSED)).
inversion STEP. subst; clear STEP. simpl in *.
iDestruct ("VS" $! 𝓥 𝓥' 𝑚 o tr with "[//]") as "[Ext VS1]". iClear "VS".
iDestruct ("VS" $! 𝓥 𝓥' 𝑚 o tr with "[//]") as "{VS} [Ext VS]".
iDestruct "Ext" as %[? [? [? [? ?]]]]. iIntros "or".
iSplitR "VS1 or".
iSplitR "VS or".
- iPureIntro. do 2 (split; [done|]). by exists 𝑚.(mto), 𝑚.(mbase).
- iIntros "Hσ". iMod ("VS1" with "Hσ") as "[Hσ $]".
- iIntros "Hσ". iMod ("VS" with "Hσ") as "[Hσ $]".
inversion_clear DRF. inversion_clear DRF0.
case_decide; destruct POST as [POST1 POST2]; destruct σ'; simpl in *; subst.
+ iApply (hist_ctx_atread_update with "Hσ or").
......@@ -1302,7 +1299,7 @@ Section hist.
iDestruct (hist_own_hist_cut with "own hist") as %[t [Eqt [EqC [? [? [? ?]]]]]].
iDestruct (hist_own_to_hist_lookup with "own hist") as %EqC'.
iDestruct (hist_own_lookup with "own hist") as %EqCL.
iIntros "!#" (o 𝑚 Vr M2 L1 L2 𝓝1 𝓝2
iIntros "!>" (o 𝑚 Vr M2 L1 L2 𝓝1 𝓝2
(EQLOC & WRITE & DRFR & DRFP & ALL & LE & ISVAL)).
iSplitL "".
{ iPureIntro. inversion_clear WRITE. inversion_clear WRITE0.
......@@ -1343,8 +1340,8 @@ Section hist.
iDestruct (hist_ctx_atwrite_agree with "[$oA $ow]") as %SUB.
destruct (𝓝 !! l) as [[? rsm]|] eqn:Eql; last first.
{ by rewrite (view_lookup_aw' _ _ _ Eql) in SUB. }
rewrite atwrite_eq. iCombine "oA" "ow" as "oAw". rewrite -own_op.
iApply (own_update with "oAw"). apply auth_update.
rewrite atwrite_eq -own_op.
iApply (own_update_2 with "oA ow"). apply auth_update.
rewrite (to_atw_add_awrite_id _ _ _ rs); last done.
eapply singleton_local_update; first by eapply to_atw_lookup_Some.
by apply exclusive_local_update.
......@@ -1394,7 +1391,7 @@ Section hist.
iDestruct (hist_ctx_hist_cut with "ctx hist") as %[? [? [t [? [EqC HL]]]]].
iDestruct "ctx" as (hF V Vc) "(Hhσ & HhF & Hna & Haw & Har & Hsc & HV & #HF)".
iDestruct (hist_ctx_write_vs σ.(mem) Vc l C with "Hhσ hist") as "#VS".
iIntros "!#" (𝑚 v o σ' Vr 𝓥 𝓥' ws
iIntros "!>" (𝑚 v o σ' Vr 𝓥 𝓥' ws
(EQLOC & WRITE & DRFR & DRFP & ALL & CLOSED & EQv & EQSC)).
iIntros "ATW".
subst l. iExists _. iSplitL "VS".
......@@ -1406,14 +1403,14 @@ Section hist.
iPureIntro. do 3 (split; [done|]). split; [|by inversion WRITE].
rewrite EqC cell_cut_lookup_None -memory_lookup_cell. left.
by apply (write_step_addins_fresh _ _ _ _ _ _ _ WRITE), WF.
- iIntros "ctx hist". iClear "HF VS".
- iIntros "{HF VS} ctx hist".
iDestruct "ctx" as (hF' V' Vc') "(Hhσ & HhF & Hna & Haw & Hat & Hsc & HV & HF)".
iDestruct "HF" as %(WF & HhF & HC & LE).
iDestruct (hist_ctx_write_vs σ.(mem) Vc' 𝑚.(mloc) C with "Hhσ hist") as "#VS".
iDestruct ("VS" $! o 𝑚 with "[%]") as "[FACT VS1]".
{ rewrite EQv. do 5 (split; [done|]). done. } iClear "VS".
iDestruct ("VS" $! o 𝑚 with "[%]") as "{VS} [FACT VS]".
{ rewrite EQv. do 5 (split; [done|]). done. }
iDestruct "FACT" as %(Eq & ? & LE' & WF𝑚).
iMod ("VS1" with "Hhσ hist") as "[Hσ' $]". iClear "VS1".
iMod ("VS" with "Hhσ hist") as "{VS} [Hσ' $]".
iMod (own_lat_auth_update_join _ _ 𝓥'.(acq) with "HV") as "[HV' HV]".
iDestruct (seen_own_join with "HV") as "$".
iAssert (|==> own hist_atwrite_name ( to_atw σ'.(na))
......@@ -1461,7 +1458,7 @@ Section hist.
Proof.
iIntros "ctx hist".
iDestruct (hist_ctx_write_msg with "ctx hist") as "#VS".
iIntros "!#" (σ' 𝓥 𝓥' 𝑚 v o ws (STEP & DRFR & DRFP & ALL & EQL & CLOSED)) "AT".
iIntros "!>" (σ' 𝓥 𝓥' 𝑚 v o ws (STEP & DRFR & DRFP & ALL & EQL & CLOSED)) "AT".
inversion STEP. subst; clear STEP. simpl in *.
iDestruct ("VS" $! 𝑚 v o (mkGB σ'.(sc) σ'.(na) σ'.(mem)) with "[%] AT")
as (C') "[Ext VS1]"; [done|].
......@@ -1530,20 +1527,20 @@ Section hist.
{ iIntros (tr).
iApply (hist_ctx_write_vs σ.(mem) (add_aread_id Vc l tr) l C with "[Hhσ] hist").
by rewrite mem_cut_add_aread_id. }
iIntros "!#" (σ' 𝓥1 𝓥2 𝓥3 𝓝2 𝑚1 𝑚2 or ow tr vr vw).
iIntros "!>" (σ' 𝓥1 𝓥2 𝓥3 𝓝2 𝑚1 𝑚2 or ow tr vr vw).
iIntros (qr rs ws) "FACT AR AW".
iDestruct "FACT" as %(EqL1 & EqL2 & ALL & InM & Eqvr & Eqvw & RS & DRFR
& WS & DRFWR & DRFWP & RLXR & RLXW & EQSC & WF').
iDestruct ("VSR" $! 𝓥1 𝓥2 𝑚1 or tr with "[%//]") as "[FACT _]". iClear "VSR".
iDestruct ("VSR" $! 𝓥1 𝓥2 𝑚1 or tr with "[%//]") as "[FACT _] {VSR}".
have ALL2: alloc_local l C 𝓥2.(cur).
{ eapply alloc_local_mono; [done|..|by rewrite -EqL1].
by eapply read_step_tview_sqsubseteq. }
iDestruct ("VS" $! tr ow 𝑚2 _ _ 𝓥2 𝓥3 𝓝2 σ'.(na) with "[%]") as "[FACT2 _]".
iDestruct ("VS" $! tr ow 𝑚2 _ _ 𝓥2 𝓥3 𝓝2 σ'.(na) with "[%]") as "[FACT2 _] {VS}".
{ do 3 (split; [done|]). split; [by rewrite EqL2|]; split; [done|].
split; [|by rewrite Eqvw].
clear -DRFR RLXR LE EqL1. inversion DRFR.
rewrite (decide_True _ _ RLXR) in POST. destruct POST.
subst. by apply add_aread_id_mono. } iClear "VS".
subst. by apply add_aread_id_mono. }
iDestruct "FACT" as %(Ext1 & GH & Eqt1 & RH & ?).
iDestruct "FACT2" as %(EqCut & ADD & LE' & WF2).
rewrite /C' 2!(decide_True _ _ RLXW) in ADD.
......@@ -1558,14 +1555,14 @@ Section hist.
iDestruct "HF" as %(WF & ? & InM' & LE).
iDestruct (hist_ctx_write_vs σ.(mem) (add_aread_id Vc' l tr) l C
with "[Hhσ] hist") as "#VS"; [by rewrite mem_cut_add_aread_id|].
iDestruct ("VS" $! ow 𝑚2 _ _ 𝓥2 𝓥3 𝓝2 σ'.(na) with "[%]") as "[FACT2 VSW]".
iDestruct ("VS" $! ow 𝑚2 _ _ 𝓥2 𝓥3 𝓝2 σ'.(na) with "[%]") as "{VS} [FACT2 VS]".
{ do 3 (split; [done|]). split; [by rewrite EqL2|]. split; [done|].
split; [|by rewrite Eqvw].
clear -DRFR RLXR LE EqL1. inversion DRFR.
rewrite (decide_True _ _ RLXR) in POST. destruct POST.
subst. by apply add_aread_id_mono. } iClear "VS".
iMod ("VSW" with "[Hhσ] hist") as "[Hhσ' hist]".
{ by rewrite mem_cut_add_aread_id. } iClear "VSW".
subst. by apply add_aread_id_mono. }
iMod ("VS" with "[Hhσ] hist") as "[Hhσ' hist] {VS}".
{ by rewrite mem_cut_add_aread_id. }
rewrite 3!(decide_True _ _ RLXW).
iFrame "hist". iMod (hist_ctx_atread_update_1 with "Har AR") as "[Har' $]".
iMod (hist_ctx_atwrite_update_1 with "Haw AW") as "[Haw' $]".
......@@ -1627,14 +1624,14 @@ Section hist.
iDestruct (hist_ctx_cas_msg with "ctx hist") as "#VS".
iDestruct (hist_ctx_wf_state with "ctx") as %WFσ.
iDestruct (hist_ctx_hist_loc_cell_wf with "ctx hist") as %WFL.
iIntros "!#" (σ' 𝓥 𝓥' vr vw or ow q tr 𝑚 rs ws).
iIntros "!>" (σ' 𝓥 𝓥' vr vw or ow q tr 𝑚 rs ws).
iIntros ((STEP & DRFR & DRFP & ALL & EQL & CLOSED & RLXR & RLXW)) "AR AW".
have ? := machine_step_global_wf _ _ _ _ _ _ _ STEP DRFR DRFP WFσ CLOSED.
inversion STEP. subst; clear STEP.
inversion_clear DRFP. inversion_clear DRF. simplify_eq.
set 𝓝2 := (add_aread_id (na σ) (mloc 𝑚) tr). destruct POST as [POST1 POST2].
iDestruct ("VS" $! (mkGB σ'.(sc) σ'.(na) σ'.(mem)) 𝓥 𝓥2 𝓥' 𝓝2 𝑚1 𝑚 with "[%] AR AW")
as (C') "[FACTS VSW]".
as (C') "{VS} [FACTS VS]".
{ rewrite SAME. do 7 (split; [done|]). split.
{ constructor. by rewrite (decide_True _ _ RLXR). } split; [done|]. split.
{ inversion_clear DRFR. inversion_clear DRFW.
......@@ -1644,7 +1641,7 @@ Section hist.
- rewrite add_aread_id_eqw AllW.
by eapply view_sqsubseteq, read_step_tview_sqsubseteq. } split.
{ constructor. by rewrite decide_True. } do 2 (split; [done|]).
by destruct σ'. } iClear "VS".
by destruct σ'. }
iDestruct "FACTS" as %(Ext1 & Ext2 & GC & Eq1 & RH & Eq2 & EqC' & INS & WH).
assert (NEQ: default 𝑚1.(mbase).(mrel) !!w 𝑚.(mloc) Some (mto 𝑚)).
{ destruct 𝑚1.(mbase).(mrel) as [Vm1|] eqn:EqVm1.
......
......@@ -353,8 +353,8 @@ Section na_props.
Lemma own_loc_na_pred_iff_proper l q Φ1 Φ2 :
( vl, Φ1 vl Φ2 vl) - (l ↦∗{q}: Φ1 l ↦∗{q}: Φ2).
Proof.
iIntros "#HΦ !#".
iSplit; iIntros; iApply (own_loc_na_pred_wand with "[-]"); try done; [|];
iIntros "#HΦ !>".
iSplit; iIntros; iApply (own_loc_na_pred_wand with "[-]"); try done;
iIntros; by iApply "HΦ".
Qed.
......
......@@ -600,9 +600,7 @@ Proof.
- iDestruct 1 as (t) "[#Eq _]". iModIntro.
iSplit; iExists t; by iFrame "Eq".
- iDestruct 1 as (t) "[#Eq F]". iSplitR ""; iExists t; by iFrame "Eq". }
iIntros (t' [] v') "(_ & TCP' & Eq)".
iDestruct (acq_exist with "Eq") as (t) "Eq".
iDestruct (acq_pure_elim with "Eq") as %Eq. subst v'. iClear "Eq".
iIntros (t' [] v') "(_ & TCP' & %t & ->)".
wp_let. wp_op. wp_op.
rewrite Z.add_mod_idemp_l; [|lia].
wp_let.
......
......@@ -207,8 +207,8 @@ Proof.
wp_op. rewrite shift_0.
(* open shared invariant *)
iMod (view_inv_acc_base' with "[$Inv $vTok1]") as "(vTok1 & INV)"; [done|].
iDestruct "INV" as (Vb) "[INV Close]". iClear "Inv".
iMod (view_inv_acc_base' with "[$Inv $vTok1]") as "(vTok1 & INV) {Inv}"; [done|].
iDestruct "INV" as (Vb) "[INV Close]".
rewrite {1}mp_inv_reclaim'_eq.
iDestruct "INV" as (ζ' b t0 V0) "[Pts _]".
rewrite view_join_later. iDestruct "Pts" as ">Pts".
......@@ -235,10 +235,11 @@ Proof.
wp_op. rewrite shift_0.
(* open shared invariant *)
iMod (view_inv_acc_base' with "[$Inv $vTok2]") as "(vTok2 & INV)"; [done|].
iDestruct "INV" as (Vb) "[INV Close]". iClear "Inv".
iMod (view_inv_acc_base' with "[$Inv $vTok2]") as "(vTok2 & INV) {Inv}"; [done|].
iDestruct "INV" as (Vb) "[INV Close]".
rewrite {1}mp_inv_reclaim'_eq.
iDestruct "INV" as (ζ' b t0 V0) "[Pts Own]".
(* TODO: IntoLater for view join *)
rewrite view_join_later. iDestruct "Pts" as ">Pts".
(* actual read *)
......
......@@ -432,7 +432,7 @@ Proof.
|by left|by right|by right| |].
{ iSplitL ""; [done|]. iSplitL "".
{ (* prove that s is alive *)
iIntros "!# _".
iIntros "!> _".
iMod (GPS_iPP_own_loc_prim _ _ _ _ _ _ _ _
( msqueQN q msqueLN s γt) with "PPs") as (C) "own";
[solve_ndisj|done|].
......
......@@ -358,7 +358,7 @@ Proof.
with "[$PPs' $Hs1 Hn Hd P H†]");
[solve_ndisj|done|done|solve_ndisj|solve_ndisj|by left|by left|by right|..].
{ iSplitL ""; last iSplitL ""; last iSplitL "".
- iIntros "!# Hs1 !>". rewrite acq_subjective own_loc_na_own_loc_prim.
- iIntros "!> Hs1 !>". rewrite acq_subjective own_loc_na_own_loc_prim.
iDestruct "Hs1" as (C) "Hs1". iExists _, _. iNext. iFrame "Hs1".
- iIntros "!> !>" (t0 [] v0 _). by iApply Head_is_comparable_loc.
- iIntros (t0 [] _). iSplitL ""; first iSplitL ""; [|iSplitL ""|..].
......@@ -464,7 +464,7 @@ Proof.
with "[$PPs' $Hs1 Hs2]");
[solve_ndisj|done|done|by left|by right|by left|..].
{ iSplitL ""; last iSplitL ""; last iSplitL ""; [..|by iFrame "Hs2"].
- iIntros "!# Hs1 !>". iExists _, #h'. by iFrame "Hs1".
- iIntros "!> Hs1 !>". iExists _, #h'. by iFrame "Hs1".
- iIntros "!> !>" (t0 [] v0 _). by iApply Head_is_comparable_loc.
- rewrite /= -(bi.True_sep' ( _, _)%I).
iApply (rel_sep_objectively with "[$rTrue]").
......
......@@ -238,7 +238,7 @@ Section PP.
with "[> Inv H𝓥3 VS PP']" as "[Inv H𝓥3]".
{ destruct OW; subst o; simpl.
- rewrite rel_mod_eq. iDestruct "VS" as (𝓥F) "[H𝓥F VS]".
iDestruct (own_lat_auth_max with "[$H𝓥3 $H𝓥F]") as %H𝓥F. iClear "H𝓥F".
iDestruct (own_lat_auth_max with "[$H𝓥3 $H𝓥F]") as "%H𝓥F {H𝓥F}".
rewrite view_at_unfold_2 (monPred_mono _ _ _ (frel_mono _ _ H𝓥F)).
assert (Le3: 𝓥3.(frel) V').
{ etrans; [|by apply LeV]. simpl. by f_equiv. }
......@@ -562,7 +562,7 @@ Section PP.
Pr P Q Q1 Q2 R _ _ _ E E (λ _, E)
with "[$R $Inv $Pr HPr $Comp VS $P] Post"); [done..|].
iSplitL "HPr".
- iIntros "!# Pr". iMod ("HPr" with "Pr") as (qr vr) "Pr".
- iIntros "!> Pr". iMod ("HPr" with "Pr") as (qr vr) "Pr".
iIntros "!>". iExists qr.
iPoseProof (own_loc_na_own_loc_prim with "Pr") as (Cr) "Pr".
iExists Cr. by iApply monPred_subjectively_intro.
......
......@@ -193,7 +193,7 @@ Section SingleWriter.
iDestruct "ex2" as (?) "ex2". rewrite monPred_at_embed.
iExists tx. iFrame "Prt Le".
iDestruct (ExWrite_frac_agree with "ex1 ex2") as %?. subst tx'.
by iCombine "ex1" "ex2" as "$".
by iCombine "ex1 ex2" as "$".
Qed.
Lemma GPS_SWSharedReaders_join t1 t2 s1 s2 v1 v2 q1 q2 γ:
......@@ -237,9 +237,8 @@ Section SingleWriter.
GPS_SWWriter t1 s1 v1 γ - GPS_SWSharedReader t2 s2 v2 q2 γ - False.
Proof.
rewrite GPS_SWWriter_eq GPS_SWSharedReader_eq.
iDestruct 1 as (?) "(_ & (_ & Ex1) & _)".
iDestruct 1 as (?) "(_ & Ex2 & _)". iCombine "Ex1" "Ex2" as "Ex".
iDestruct (own_valid with "Ex") as %[_ [[VAL _]%auth_frag_valid_1 _]].
iDestruct 1 as (?) "(_ & (_ & Ex1) & _)". iDestruct 1 as (?) "(_ & Ex2 & _)".
iDestruct (own_valid_2 with "Ex1 Ex2") as %[_ [[VAL _]%auth_frag_valid_1 _]].
simpl in VAL. exfalso. rewrite -> frac_valid in VAL.
by apply Qp_not_add_le_l in VAL.
Qed.
......@@ -664,7 +663,7 @@ Section SingleWriter.
{ iMod ("IW" $! (Vx Va) with "Fx") as "[I $]".
destruct OW; subst o; simpl.
- rewrite rel_mod_eq. iDestruct "F" as (𝓥F) "[H𝓥F F]".
iDestruct (own_lat_auth_max with "[$H𝓥3 $H𝓥F]") as %H𝓥F. iClear "H𝓥F".
iDestruct (own_lat_auth_max with "[$H𝓥3 $H𝓥F]") as "%H𝓥F {H𝓥F}".
rewrite view_at_unfold_2 (monPred_mono _ _ _ (frel_mono _ _ H𝓥F)).
assert (Le3: 𝓥3.(frel) V').
{ etrans; [|by apply LeV]. simpl. by f_equiv. }
......@@ -872,7 +871,7 @@ Section SingleWriter.
{ iDestruct "ex" as (tx') "ex". iExists tx'. iFrame "ex". iExists _,_,_.
iFrame "naV R". iPureIntro. by eapply seen_local_mono. }
iSplit; [rewrite bi.and_elim_l|by rewrite bi.and_elim_r]. rewrite Ext5.
iIntros (? ?) "F". iMod ("VS" with "F") as "(% & W & $)".
iIntros (??) "F". iMod ("VS" with "F") as "(% & W & $)".
iModIntro. iSplit. { iPureIntro. rewrite /Vo. solve_lat. }
rewrite GPS_SWSharedWriter_eq. iDestruct "W" as (?) "(Prt & W & MAX)".
iExists _. iFrame "Prt W MAX".
......@@ -935,7 +934,7 @@ Section SingleWriter.
- rewrite bi.and_elim_l. rewrite (monPred_mono _ _ _ Ext3').
iIntros (? Ext4) "P". iSpecialize ("VS" with "P").
iSplit; [rewrite bi.and_elim_l|by rewrite bi.and_elim_r].
iIntros (? ?) "F". iMod ("VS" with "F") as "(% & W & $)".
iIntros (??) "F". iMod ("VS" with "F") as "(% & W & $)".
iModIntro. iSplit. { iPureIntro. rewrite /Vo. solve_lat. }
rewrite GPS_SWSharedWriter_eq. iDestruct "W" as (?) "(Prt & W & MAX)".
iExists _. by iFrame "Prt W MAX".
......
......@@ -289,8 +289,7 @@ Section Properties.
Lemma exwr_update γ t t':
gps_ownA_E γ t - exwr γ t 1%Qp == gps_ownA_E γ t' exwr γ t' 1%Qp.
Proof.
iIntros "oE ox". iCombine "oE ox" as "oEx".
iMod (own_update with "oEx") as "[$ $]"; [|done].
iIntros "oE ox". iMod (own_update_2 with "oE ox") as "[$ $]"; [|done].
apply prod_update; [by rewrite /= left_id|]. apply prod_update; [|done].
by apply frac_auth_update_1.
Qed.
......@@ -315,8 +314,8 @@ Section Properties.
Lemma Writer_Exclusive γ ζ1 ζ2 :
Writer γ ζ1 - Writer γ ζ2 - False.
Proof.
iIntros "Writer1 Writer2". iCombine "Writer1" "Writer2" as "oW".
by iDestruct (own_valid with "oW") as %[[]%auth_frag_valid_1].
iIntros "W1 W2".
by iDestruct (own_valid_2 with "W1 W2") as %[[]%auth_frag_valid_1].
Qed.
Lemma Writer_exact γ ζ ζ': gps_ownA_M γ ζ - Writer γ ζ' - ⌜ζ = ζ'.
......@@ -372,10 +371,8 @@ Section Properties.
Lemma naWrite_agree γ (V1 V2: view) rs1 rs2 :
naWrite γ V1 rs1 - naWrite γ V2 rs2 - V1 = V2 rs1 = rs2.