better support for view shift with mismatching masks

iris/base_logic/lib/fancy_updates.v

@@ -65,7 +65,7 @@ Lemma fupd_plain_soundness `{!invPreG Σ} E1 E2 (P: iProp Σ) `{!Plain P} :
 Proof.
   iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hinv) "[Hw HE]".
   iAssert (|={⊤,E2}=> P)%I as "H".
-  { iMod fupd_intro_mask'; last iApply Hfupd. done. }
+  { iMod Hfupd as "[_ $]". done. }
   rewrite uPred_fupd_eq /uPred_fupd_def.
   iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
 Qed.

iris/base_logic/lib/invariants.v

@@ -140,8 +140,8 @@ Section inv.
     rewrite inv_eq. iIntros (??) "#HinvP #HinvQ !>"; iIntros (E ?).
     iMod ("HinvP" with "[%]") as "[$ HcloseP]"; first set_solver.
     iMod ("HinvQ" with "[%]") as "[$ HcloseQ]"; first set_solver.
-    iMod (fupd_intro_mask' _ (E ∖ ↑N)) as "Hclose"; first set_solver.
-    iIntros "!> [HP HQ]".
+    iApply fupd_intro_adjust_mask; first set_solver.
+    iIntros "Hclose [HP HQ]".
     iMod "Hclose" as %_. iMod ("HcloseQ" with "HQ") as %_. by iApply "HcloseP".
   Qed.
 

iris/bi/lib/atomic.v

@@ -55,9 +55,9 @@ Section definition.
     Eo1 ⊆ Eo2 →
     atomic_acc Eo1 Ei α P β Φ -∗ atomic_acc Eo2 Ei α P β Φ.
   Proof.
-    iIntros (HE) "Hstep".
-    iMod fupd_intro_mask' as "Hclose1"; first done.
-    iMod "Hstep" as (x) "[Hα Hclose2]". iIntros "!>". iExists x.
+    iIntros (HE) "Hstep". rewrite /atomic_acc.
+    iMod "Hstep" as "[Hclose Hstep]".
+    iDestruct "Hstep" as (x) "[Hα Hclose2]". iIntros "!>". iExists x.
     iFrame. iSplitWith "Hclose2".
     - iIntros "Hα". iMod ("Hclose2" with "Hα") as "$". done.
     - iIntros (y) "Hβ". iMod ("Hclose2" with "Hβ") as "$". done.
@@ -311,7 +311,7 @@ Section lemmas.
     atomic_acc Eo Ei α P β Φ).
   Proof.
     iIntros (? x) "Hα Hclose".
-    iMod fupd_intro_mask' as "Hclose'"; last iModIntro; first set_solver.
+    iApply fupd_intro_adjust_mask; first done. iIntros "Hclose'".
     iExists x. iFrame. iSplitWith "Hclose".
     - iIntros "Hα". iMod "Hclose'" as "_". iApply "Hclose". done.
     - iIntros (y) "Hβ". iMod "Hclose'" as "_". iApply "Hclose". done.
@@ -330,7 +330,7 @@ Section lemmas.
        to happen only if one argument is a constructor. *)
     iIntros (_) "Hinner >Hacc". iDestruct "Hacc" as (x') "[Hα' Hclose]".
     iMod ("Hinner" with "Hα'") as (x) "[Hα Hclose']".
-    iMod (fupd_intro_mask') as "Hclose''"; last iModIntro; first done.
+    iApply fupd_intro_adjust_mask; first done. iIntros "Hclose''".
     iExists x. iFrame. iSplitWith "Hclose'".
     - iIntros "Hα". iMod "Hclose''" as "_".
       iMod ("Hclose'" with "Hα") as "[Hβ' HPas]".

iris/bi/updates.v

@@ -283,6 +283,17 @@ Section fupd_derived.
     (Q -∗ (|={E2,E3}=> P)) → (|={E1,E2}=> Q) -∗ (|={E1,E3}=> P).
   Proof. intros ->. rewrite fupd_trans //. Qed.
 
+  Lemma fupd_intro_adjust_mask E1 E2 P:
+    E2 ⊆ E1 →
+    ((|={E2,E1}=> emp) -∗ P) -∗ |={E1,E2}=> P.
+  Proof.
+    intros HE.
+    (* Get an [emp] so we can apply [fupd_intro_mask']. *)
+    rewrite -[X in (X -∗ _)](right_id emp%I).
+    rewrite {2}(fupd_intro_mask' E1 E2) //.
+    rewrite fupd_frame_l. apply fupd_mono. rewrite wand_elim_l. done.
+  Qed.
+
   Lemma fupd_mask_frame_r E1 E2 Ef P :
     E1 ## Ef → (|={E1,E2}=> P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P.
   Proof.

iris/program_logic/ectx_lifting.v

@@ -62,8 +62,7 @@ Lemma wp_lift_pure_head_stuck E Φ e :
   ⊢ WP e @ E ?{{ Φ }}.
 Proof using Hinh.
   iIntros (?? Hstuck). iApply wp_lift_head_stuck; [done|done|].
-  iIntros (σ κs n) "_". iMod (fupd_intro_mask' E ∅) as "_"; first set_solver.
-  by auto.
+  iIntros (σ κs n) "_". iApply fupd_intro_adjust_mask; by auto with set_solver.
 Qed.
 
 Lemma wp_lift_atomic_head_step_fupd {s E1 E2 Φ} e1 :

iris/program_logic/lifting.v

@@ -61,7 +61,7 @@ Proof.
   iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
   { specialize (Hsafe inhabitant). destruct s; eauto using reducible_not_val. }
   iIntros (σ1 κ κs n) "Hσ". iMod "H".
-  iMod fupd_intro_mask' as "Hclose"; last iModIntro; first by set_solver. iSplit.
+  iApply fupd_intro_adjust_mask; first set_solver. iIntros "Hclose". iSplit.
   { iPureIntro. destruct s; done. }
   iNext. iIntros (e2 σ2 efs ?).
   destruct (Hstep κ σ1 e2 σ2 efs) as (-> & <- & ->); auto.
@@ -76,7 +76,7 @@ Proof.
   iIntros (Hstuck) "_". iApply wp_lift_stuck.
   - destruct(to_val e) as [v|] eqn:He; last done.
     rewrite -He. by case: (Hstuck inhabitant).
-  - iIntros (σ κs n) "_". by iMod (fupd_intro_mask' E ∅) as "_"; first set_solver.
+  - iIntros (σ κs n) "_". iApply fupd_intro_adjust_mask; auto with set_solver.
 Qed.
 
 (* Atomic steps don't need any mask-changing business here, one can
@@ -94,8 +94,8 @@ Proof.
   iIntros (?) "H".
   iApply (wp_lift_step_fupd s E1 _ e1)=>//; iIntros (σ1 κ κs n) "Hσ1".
   iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
-  iMod (fupd_intro_mask' E1 ∅) as "Hclose"; first set_solver.
-  iIntros "!>" (e2 σ2 efs ?). iMod "Hclose" as "_".
+  iApply fupd_intro_adjust_mask; first set_solver.
+  iIntros "Hclose" (e2 σ2 efs ?). iMod "Hclose" as "_".
   iMod ("H" $! e2 σ2 efs with "[#]") as "H"; [done|].
   iMod (fupd_intro_mask' E2 ∅) as "Hclose"; [set_solver|]. iIntros "!> !>".
   iMod "Hclose" as "_". iMod "H" as "($ & HQ & $)".

iris/program_logic/ownp.v

@@ -146,8 +146,8 @@ Section lifting.
     iIntros (Hsafe Hstep) "H"; iApply wp_lift_step.
     { specialize (Hsafe inhabitant). destruct s; last done.
       by eapply reducible_not_val. }
-    iIntros (σ1 κ κs n) "Hσ". iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
-    iModIntro; iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs ?).
+    iIntros (σ1 κ κs n) "Hσ". iApply fupd_intro_adjust_mask; first set_solver.
+    iIntros "Hclose". iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs ?).
     destruct (Hstep σ1 κ e2 σ2 efs); auto; subst.
     by iMod "Hclose"; iModIntro; iFrame; iApply "H".
   Qed.
@@ -162,8 +162,8 @@ Section lifting.
     ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
     iIntros (?) "[Hσ H]"; iApply ownP_lift_step.
-    iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
-    iModIntro; iExists σ1; iFrame; iSplit; first by destruct s.
+    iApply fupd_intro_adjust_mask; first set_solver.
+    iIntros "Hclose". iExists σ1; iFrame; iSplit; first by destruct s.
     iNext; iIntros (κ e2 σ2 efs ?) "Hσ".
     iDestruct ("H" $! κ e2 σ2 efs with "[] [Hσ]") as "[HΦ $]"; [by eauto..|].
     destruct (to_val e2) eqn:?; last by iExFalso.

iris/program_logic/total_lifting.v

@@ -35,7 +35,7 @@ Proof.
   iIntros (Hsafe Hstep) ">H". iApply twp_lift_step.
   { eapply reducible_not_val, reducible_no_obs_reducible, (Hsafe inhabitant). }
   iIntros (σ1 κs n) "Hσ".
-  iMod fupd_intro_mask' as "Hclose"; last iModIntro; first by set_solver. iSplit.
+  iApply fupd_intro_adjust_mask; first by set_solver. iIntros "Hclose". iSplit.
   { iPureIntro. destruct s; auto. }
   iIntros (κ e2 σ2 efs ?). destruct (Hstep σ1 κ e2 σ2 efs) as (->&<-&->); auto.
   iMod "Hclose" as "_". iModIntro.
@@ -58,8 +58,8 @@ Proof.
   iIntros (?) "H".
   iApply (twp_lift_step _ E _ e1)=>//; iIntros (σ1 κs n) "Hσ1".
   iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
-  iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
-  iIntros "!>" (κ e2 σ2 efs) "%". iMod "Hclose" as "_".
+  iApply fupd_intro_adjust_mask; first set_solver.
+  iIntros "Hclose" (κ e2 σ2 efs) "%". iMod "Hclose" as "_".
   iMod ("H" $! κ e2 σ2 efs with "[#]") as "($ & $ & HΦ & $)"; first by eauto.
   destruct (to_val e2) eqn:?; last by iExFalso.
   iApply twp_value; last done. by apply of_to_val.

iris/program_logic/total_weakestpre.v

@@ -115,8 +115,8 @@ Proof.
   iIntros "!>" (e E1 Φ) "IH"; iIntros (E2 Ψ HE) "HΦ".
   rewrite !twp_unfold /twp_pre. destruct (to_val e) as [v|] eqn:?.
   { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
-  iIntros (σ1 κs n) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
-  iMod ("IH" with "[$]") as "[% IH]".
+  iIntros (σ1 κs n) "Hσ".
+  iMod ("IH" with "[$]") as "[Hclose [% IH]]".
   iModIntro; iSplit; [by destruct s1, s2|]. iIntros (κ e2 σ2 efs Hstep).
   iMod ("IH" with "[//]") as (?) "(Hσ & IH & IHefs)"; auto.
   iMod "Hclose" as "_"; iModIntro.

iris/program_logic/weakestpre.v

@@ -101,8 +101,8 @@ Proof.
   rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:?.
   { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
-  iIntros (σ1 κ κs n) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
-  iMod ("H" with "[$]") as "[% H]".
+  iIntros (σ1 κ κs n) "Hσ".
+  iMod ("H" with "[$]") as "[Hclose [% H]]".
   iModIntro. iSplit; [by destruct s1, s2|]. iIntros (e2 σ2 efs Hstep).
   iMod ("H" with "[//]") as "H". iIntros "!> !>".
   iMod "H" as "(Hσ & H & Hefs)".

iris/proofmode/class_instances_updates.v

@@ -178,4 +178,16 @@ Proof.
   iMod ("Hinner" with "Hα") as "[Hβ Hfin]".
   iMod ("Hclose" with "Hβ") as "Hγ". by iApply "Hfin".
 Qed.
+
+Global Instance elim_modal_fupd_fupd_adjust_mask `{!BiFUpd PROP} p E1 E1' E2 E2' P Q :
+  ElimModal (E1' ⊆ E1) p false
+    (|={E1',E2'}=> P) ((|={E1',E1}=> emp) ∗ P)
+    (|={E1,E2}=> Q) (|={E2',E2}=> Q) | 20.
+Proof.
+  rewrite /ElimModal /= intuitionistically_if_elim.
+  iIntros (HE) "[HP Hcont]".
+  iMod fupd_intro_mask' as "Hclose"; first exact HE.
+  iMod "HP" as "HP". iApply "Hcont". iSplitR "HP"; done.
+Qed.
+
 End class_instances_updates.