From 7fca095891d314b5000ebdfd6b3f1f404cb6e0e9 Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Fri, 15 Nov 2024 10:23:13 +0100
Subject: [PATCH] Change state update to take in two mask

---
 theories/coneris/error_rules.v                |   4 +-
 .../coneris/examples/random_counter/impl1.v   |   2 +-
 .../coneris/examples/random_counter/impl2.v   |   2 +-
 .../coneris/examples/random_counter/impl3.v   |   2 +-
 .../examples/random_counter/random_counter.v  |   3 +-
 theories/coneris/lib/hocap_flip.v             |   2 +-
 theories/coneris/lib/hocap_rand.v             |   2 +-
 theories/coneris/wp_update.v                  | 120 ++++++++----------
 8 files changed, 64 insertions(+), 73 deletions(-)

diff --git a/theories/coneris/error_rules.v b/theories/coneris/error_rules.v
index a6d91b22..0243044b 100644
--- a/theories/coneris/error_rules.v
+++ b/theories/coneris/error_rules.v
@@ -1154,7 +1154,7 @@ Qed.
   Lemma state_update_presample_iterM_exp E α N ns p (ε1 : R) (ε2 : list (fin (S N)) → R) :
     (∀ n, 0<=ε2 n)%R ->
     (SeriesC (λ n, if (length n =? p) then (1/((S N)^ p)) * ε2 n else 0%R )<= ε1)%R →
-     α ↪N (N; ns) -∗ ↯ ε1 -∗ state_update E (∃ n, α ↪N (N; ns ++ (fin_to_nat <$> n)) ∗
+     α ↪N (N; ns) -∗ ↯ ε1 -∗ state_update E E (∃ n, α ↪N (N; ns ++ (fin_to_nat <$> n)) ∗
                                                   ↯ (ε2 n) ∗
                                                   ⌜length n = p⌝
                                ).
@@ -1196,7 +1196,7 @@ Qed.
   Lemma state_update_presample_exp E α N ns (ε1 : R) (ε2 : fin (S N) → R) :
     (∀ n, 0<=ε2 n)%R ->
     (SeriesC (λ n, 1 / (S N) * ε2 n)%R <= ε1)%R →
-    α ↪N (N; ns) -∗ ↯ ε1 -∗ state_update E (∃ n, α ↪N (N; ns ++ [fin_to_nat n]) ∗ ↯ (ε2 n)).
+    α ↪N (N; ns) -∗ ↯ ε1 -∗ state_update E E (∃ n, α ↪N (N; ns ++ [fin_to_nat n]) ∗ ↯ (ε2 n)).
   Proof.
     rewrite state_update_unseal/state_update_def.
     iIntros (Hpos Hsum) "Hα Hε".
diff --git a/theories/coneris/examples/random_counter/impl1.v b/theories/coneris/examples/random_counter/impl1.v
index b741e114..0c86a057 100644
--- a/theories/coneris/examples/random_counter/impl1.v
+++ b/theories/coneris/examples/random_counter/impl1.v
@@ -135,7 +135,7 @@ Section impl1.
     is_counter1 N c γ1 -∗
     rand_tapes (L:=L) α (3%nat, ns) -∗
     ↯ ε  -∗
-    state_update E (∃ n, ↯ (ε2 n) ∗ rand_tapes (L:=L) α (3%nat, ns++[fin_to_nat n])).
+    state_update E E (∃ n, ↯ (ε2 n) ∗ rand_tapes (L:=L) α (3%nat, ns++[fin_to_nat n])).
   Proof.
     iIntros (Hsubset Hpos Hineq) "#Hinv Hfrag Herr".
     iMod (rand_tapes_presample with "[$][$]") as "(%&$&$)"; try done.
diff --git a/theories/coneris/examples/random_counter/impl2.v b/theories/coneris/examples/random_counter/impl2.v
index 131bcd65..7ed61889 100644
--- a/theories/coneris/examples/random_counter/impl2.v
+++ b/theories/coneris/examples/random_counter/impl2.v
@@ -274,7 +274,7 @@ Section impl2.
     is_counter2 N c γ1  -∗
     (flip_tapes (L:=L) α (expander ns) ∗ ⌜Forall (λ x, x<4) ns⌝) -∗
     ↯ ε  -∗
-    state_update E (∃ n, ↯ (ε2 n) ∗
+    state_update E E (∃ n, ↯ (ε2 n) ∗
                          (flip_tapes (L:=L) α (expander (ns++[fin_to_nat n])) ∗ ⌜Forall (λ x, x<4) (ns++[fin_to_nat n])⌝)).
   Proof.
     iIntros (Hsubset Hpos Hineq) "#Hinv' [Hfrag %Hforall] Herr".
diff --git a/theories/coneris/examples/random_counter/impl3.v b/theories/coneris/examples/random_counter/impl3.v
index bc289dbf..b5ce5cdb 100644
--- a/theories/coneris/examples/random_counter/impl3.v
+++ b/theories/coneris/examples/random_counter/impl3.v
@@ -122,7 +122,7 @@ Section impl3.
     is_counter3 N c γ1 -∗
     (∃ ls, ⌜filter filter_f ls = ns⌝ ∗ rand_tapes (L:=L) α (4, ls)) -∗
     ↯ ε  -∗
-    state_update E (∃ n, ↯ (ε2 n) ∗
+    state_update E E (∃ n, ↯ (ε2 n) ∗
                          (∃ ls, ⌜filter filter_f ls = (ns++[fin_to_nat n])⌝ ∗ rand_tapes (L:=L) α (4, ls))).
   Proof.
     iIntros (Hsubset Hpos Hineq) "#Hinv Hfrag Herr".
diff --git a/theories/coneris/examples/random_counter/random_counter.v b/theories/coneris/examples/random_counter/random_counter.v
index 143b9bc7..3d1797d9 100644
--- a/theories/coneris/examples/random_counter/random_counter.v
+++ b/theories/coneris/examples/random_counter/random_counter.v
@@ -53,7 +53,7 @@ Class random_counter `{!conerisGS Σ} := RandCounter
   is_counter(L:=L) N c γ  -∗
   counter_tapes (L:=L) α (ns) -∗
   ↯ ε  -∗
-  state_update E (∃ n, ↯ (ε2 n) ∗ counter_tapes (L:=L) α (ns ++ [fin_to_nat n]));
+  state_update E E (∃ n, ↯ (ε2 n) ∗ counter_tapes (L:=L) α (ns ++ [fin_to_nat n]));
 
   counter_content_auth_exclusive {L : counterG Σ} γ z1 z2:
     counter_content_auth (L:=L) γ z1 -∗ counter_content_auth (L:=L) γ z2 -∗ False;
@@ -148,7 +148,6 @@ Section lemmas.
     - iDestruct "H" as "(%ε & %ε2 & Herr & %Hpos & %Hineq & Hrest)".
       iMod (counter_tapes_presample _ _ _ _ _ _ _ (λ x, ε2 (fin_to_nat x)) with "[//][$][$Herr]") as "(%n & Herr & ?)"; try done.
       { rewrite SeriesC_finite_foldr/=. lra. }
-      iModIntro.
       iMod (fupd_mask_frame _ (E) ∅ (E∖↑N) with "[Hrest Herr]") as "H"; first set_solver.
       + iMod ("Hrest" with "[$]") as "H". iModIntro.
         replace (_∖_∪_) with E; first (iModIntro; iExact "H").
diff --git a/theories/coneris/lib/hocap_flip.v b/theories/coneris/lib/hocap_flip.v
index 27d80ea1..ff5aed8f 100644
--- a/theories/coneris/lib/hocap_flip.v
+++ b/theories/coneris/lib/hocap_flip.v
@@ -41,7 +41,7 @@ Class flip_spec `{!conerisGS Σ} := FlipSpec
     (* is_flip (L:=L) N γ -∗ *)
     flip_tapes (L:=L) α (ns) -∗
     ↯ ε  -∗
-    state_update E (∃ n, ↯ (ε2 n) ∗ flip_tapes (L:=L) α (ns ++ [n]));
+    state_update E E (∃ n, ↯ (ε2 n) ∗ flip_tapes (L:=L) α (ns ++ [n]));
 
   (** * Program specs *)
   (* flip_inv_create_spec {L : flipG Σ} N E: *)
diff --git a/theories/coneris/lib/hocap_rand.v b/theories/coneris/lib/hocap_rand.v
index 5fe7681d..345d52df 100644
--- a/theories/coneris/lib/hocap_rand.v
+++ b/theories/coneris/lib/hocap_rand.v
@@ -45,7 +45,7 @@ Class rand_spec `{!conerisGS Σ} := RandSpec
   (* is_rand(L:=L) N γ -∗ *)
   rand_tapes (L:=L) α (tb, ns) -∗
   ↯ ε  -∗
-  state_update E (∃ n, ↯ (ε2 n) ∗ rand_tapes (L:=L) α (tb, ns ++ [fin_to_nat n]));
+  state_update E E (∃ n, ↯ (ε2 n) ∗ rand_tapes (L:=L) α (tb, ns ++ [fin_to_nat n]));
     
 
   (** * Program specs *)
diff --git a/theories/coneris/wp_update.v b/theories/coneris/wp_update.v
index b56d9dc8..23d95ac2 100644
--- a/theories/coneris/wp_update.v
+++ b/theories/coneris/wp_update.v
@@ -240,11 +240,11 @@ End wp_update.
 
 Section state_update.
   Context `{!conerisGS Σ}.
-  Definition state_update_def E P:=
+  Definition state_update_def E1 E2 P:=
     (∀ σ1 ε1,
-       state_interp σ1 ∗ err_interp ε1 ={E, ∅}=∗
+       state_interp σ1 ∗ err_interp ε1 ={E1, ∅}=∗
        state_step_coupl σ1 ε1 (λ σ2 ε2,
-                                 |={∅, E}=> state_interp σ2 ∗ err_interp ε2 ∗ P
+                                 |={∅, E2}=> state_interp σ2 ∗ err_interp ε2 ∗ P
          )
     )%I.
   
@@ -254,7 +254,7 @@ Section state_update.
   Proof. rewrite -state_update_aux.(seal_eq) //. Qed.
 
   Lemma wp_update_state_update E P:
-    state_update E P -∗ wp_update E P.
+    state_update E E P -∗ wp_update E P.
   Proof.
     rewrite state_update_unseal/state_update_def.
     iIntros.
@@ -262,7 +262,7 @@ Section state_update.
   Qed.
 
   Lemma state_update_ret E P:
-    P -∗ state_update E P.
+    P -∗ state_update E E P.
   Proof. 
     rewrite state_update_unseal/state_update_def.
     iIntros.
@@ -274,11 +274,11 @@ Section state_update.
   Qed.
 
   Global Instance from_modal_state_update_state_update P E :
-    FromModal True modality_id (state_update E P) (state_update E P) P.
+    FromModal True modality_id (state_update E E P) (state_update E E P) P.
   Proof. iIntros (_) "HP /=". by iApply state_update_ret. Qed.
     
-  Lemma state_update_mono_fupd E1 E2 P:
-    E1 ⊆ E2 -> (|={E2,E1}=> state_update E1 (|={E1, E2}=> P)) -∗ state_update E2 P.
+  Lemma state_update_mono_fupd E1 E2 E3 P:
+    E1 ⊆ E2 -> (|={E2,E1}=> state_update E1 E3 P) -∗ state_update E2 E3 P.
   Proof.
     rewrite state_update_unseal/state_update_def.
     iIntros (Hsubseteq) "Hvs".
@@ -286,12 +286,12 @@ Section state_update.
     iMod ("Hvs" with "[$]") as ">?".
     iModIntro.
     iApply (state_step_coupl_mono with "[][$]").
-    iIntros (??) ">(?&?&>?)". by iFrame.
+    iIntros (??) ">(?&?&?)". by iFrame.
   Qed.
 
   
-  Lemma state_update_mono E P Q:
-    (P={E}=∗Q) -∗ state_update E P -∗ state_update E Q.
+  Lemma state_update_mono E1 E2 P Q:
+    (P={E2}=∗Q) -∗ state_update E1 E2 P -∗ state_update E1 E2 Q.
   Proof.
     rewrite state_update_unseal/state_update_def.
     iIntros "Hvs H".
@@ -305,20 +305,24 @@ Section state_update.
   Qed.
   
   Lemma state_update_mono_fupd' E1 E2 P:
-    E1 ⊆ E2 -> (state_update E1 P) -∗ state_update E2 P.
+    E1 ⊆ E2 -> (state_update E1 E1 P) -∗ state_update E2 E2 P.
   Proof.
-    iIntros.
+    iIntros (?) "H".
     iApply state_update_mono_fupd; first done.
     iApply fupd_mask_intro; first done.
     iIntros "Hclose".
-    iApply (state_update_mono with "[Hclose][$]").
+    rewrite state_update_unseal/state_update_def.
     iIntros.
+    iMod ("H" with "[$]") as "H".
     iModIntro.
+    iApply (state_step_coupl_bind with "[Hclose][$]").
+    iIntros (??) "H". iApply state_step_coupl_ret.
+    iMod "H".
     by iMod "Hclose".
   Qed.
   
-  Lemma state_update_fupd E P:
-    (|={E}=> state_update E P) -∗ state_update E P.
+  Lemma state_update_fupd E1 E2 P:
+    (|={E1}=> state_update E1 E2 P) -∗ state_update E1 E2 P.
   Proof.
     iIntros "H".
     iApply state_update_mono_fupd; first done.
@@ -329,7 +333,7 @@ Section state_update.
 
   
   Lemma state_update_epsilon_err E:
-    ⊢ state_update E (∃ ε, ⌜(0<ε)%R⌝ ∗ ↯ ε).
+    ⊢ state_update E E (∃ ε, ⌜(0<ε)%R⌝ ∗ ↯ ε).
   Proof.
     rewrite state_update_unseal/state_update_def.
     iIntros (? ε) "[Hstate Herr]".
@@ -349,8 +353,8 @@ Section state_update.
     lra.
   Qed.
   
-  Lemma state_update_fupd_change E1 E2 P Q:
-    (|={E1, E2}=> P) -∗ (P-∗ state_update E2 (|={E2, E1}=> Q)) -∗ state_update E1 Q.
+  Lemma state_update_fupd_change E1 E2 E3 P Q:
+    (|={E1, E2}=> P) -∗ (P-∗ state_update E2 E3 Q) -∗ state_update E1 E3 Q.
   Proof.
     iIntros "H1 H2".
     rewrite state_update_unseal/state_update_def.
@@ -360,12 +364,12 @@ Section state_update.
     iModIntro.
     iApply state_step_coupl_mono; last done.
     simpl.
-    iIntros (??) ">(?&?&>?)".
+    iIntros (??) ">(?&?&?)".
     by iFrame.
   Qed.
 
-  Global Instance elim_modal_bupd_state_update p E P Q :
-    ElimModal True p false (|==> P) P (state_update E Q) (state_update E Q).
+  Global Instance elim_modal_bupd_state_update p E1 E2 P Q :
+    ElimModal True p false (|==> P) P (state_update E1 E2 Q) (state_update E1 E2 Q).
   Proof.
     intros ?.
     rewrite bi.intuitionistically_if_elim/=.
@@ -376,10 +380,10 @@ Section state_update.
     by iApply "H2".
   Qed.
   
-  Global Instance elim_modal_fupd_state_update p E1 E2 P Q :
+  Global Instance elim_modal_fupd_state_update p E1 E2 E3 P Q :
     ElimModal (True) p false
             (|={E1,E2}=> P) P
-            (state_update E1 Q) (state_update E2 (|={E2, E1}=> Q)).
+            (state_update E1 E3 Q) (state_update E2 E3 Q).
   Proof.
     intros ?.
     rewrite bi.intuitionistically_if_elim/=.
@@ -387,8 +391,8 @@ Section state_update.
     iApply (state_update_fupd_change with "[$][$]").
   Qed.
   
-  Lemma state_update_bind E P Q:
-    state_update E P ∗ (P -∗ state_update E Q) ⊢ state_update E Q.
+  Lemma state_update_bind E1 E2 E3 P Q:
+    state_update E1 E2 P ∗ (P -∗ state_update E2 E3 Q) ⊢ state_update E1 E3 Q.
   Proof.
     rewrite state_update_unseal/state_update_def.
     iIntros "[H1 H2]" (??) "[??]".
@@ -401,26 +405,18 @@ Section state_update.
     by iMod ("H2" with "[$][$]").
   Qed.
 
-  Global Instance elim_modal_state_update_state_update p E1 E2 P Q :
-    ElimModal (E1 ⊆ E2) p false (state_update E1 Q) Q (state_update E2 P) (state_update E2 P).
+  Global Instance elim_modal_state_update_state_update p E1 E2 E3 P Q :
+    ElimModal (True) p false (state_update E1 E2 Q) Q (state_update E1 E3 P) (state_update E2 E3 P).
   Proof.
-    iIntros (?) "[H1 H2]".
+    iIntros (_) "[H1 H2]".
     rewrite bi.intuitionistically_if_elim.
     iApply state_update_mono_fupd; first exact.
     iApply fupd_mask_intro; first exact; iIntros "Hclose".
     iApply state_update_bind; iFrame.
-    iIntros.
-    iApply (state_update_fupd_change with "[$]").
-    iIntros.
-    iDestruct ("H2" with "[$]") as "H".
-    iApply (state_update_mono); last done.
-    iIntros.
-    iModIntro.
-    by iApply fupd_mask_intro_subseteq.
   Qed.
  
   Global Instance elim_modal_state_update_wp_update p E1 E2 P Q :
-    ElimModal (E1 ⊆ E2) p false (state_update E1 Q) Q (wp_update E2 P) (wp_update E2 P).
+    ElimModal (E1 ⊆ E2) p false (state_update E1 E1 Q) Q (wp_update E2 P) (wp_update E2 P).
   Proof.
     (* rewrite state_update_unseal/state_update_def. *)
     iIntros (?) "[H1 H2]".
@@ -435,41 +431,39 @@ Section state_update.
     - iDestruct (bi.intuitionistically_elim with "[$]") as "H1".
       iMod "H1".
       iMod "Hclose" as "_".
-      iModIntro.
-      by iApply fupd_mask_intro_subseteq.
+      by iModIntro.
     - iMod "H1".
       iMod "Hclose" as "_".
-      iModIntro.
-      by iApply fupd_mask_intro_subseteq.
+      by iModIntro.
   Qed.
   
   Global Instance elim_modal_state_update_wp e Φ p E1 E2 P :
-    ElimModal (E1 ⊆ E2) p false (state_update E1 P) P (WP e @ E2 {{ Φ }}) (WP e @ E2 {{ Φ }}).
+    ElimModal (E1 ⊆ E2) p false (state_update E1 E1 P) P (WP e @ E2 {{ Φ }}) (WP e @ E2 {{ Φ }}).
   Proof.
     destruct p.
     all: iIntros (?); simpl; iIntros "[H1 H2]".
     1: iDestruct (bi.intuitionistically_elim with "[$]") as "H1".
     all: iDestruct (state_update_mono_fupd with "[H1]") as "H1"; first exact;
       last (iDestruct (wp_update_state_update with "[$]") as "H1"; iMod "H1"; by iApply "H2").
-    all: iApply fupd_mask_intro; first exact; iIntros "Hclose"; iMod "H1"; iModIntro; by iMod "Hclose".
+    all: iApply fupd_mask_intro; first exact; iIntros "Hclose"; iMod "H1"; iMod "Hclose"; by iModIntro.
   Qed.
 
   Lemma state_update_wp E P e Φ:
-    (state_update E P) -∗ (P -∗ WP e @ E {{Φ}}) -∗ WP e @ E {{Φ}}.
+    (state_update E E P) -∗ (P -∗ WP e @ E {{Φ}}) -∗ WP e @ E {{Φ}}.
   Proof.
     iIntros ">? H".
     by iApply "H".
   Qed.
 
-  Global Instance is_except_0_state_update E Q : IsExcept0 (state_update E Q).
+  Global Instance is_except_0_state_update E1 E2 Q : IsExcept0 (state_update E1 E2 Q).
   Proof.
     rewrite /IsExcept0.
     iIntros.
-    iApply (state_update_fupd E Q). by rewrite -except_0_fupd -fupd_intro.
+    iApply (state_update_fupd E1 E2 Q). by rewrite -except_0_fupd -fupd_intro.
   Qed.
 
-  Lemma state_update_frame_l R E P :
-    R ∗ state_update E P ⊢ state_update E (P ∗ R).
+  Lemma state_update_frame_l R E1 E2 P :
+    R ∗ state_update E1 E2 P ⊢ state_update E1 E2 (P ∗ R).
   Proof.
     iIntros "[HR H]".
     iMod "H".
@@ -478,7 +472,7 @@ Section state_update.
   Qed.
 
   Global Instance frame_state_update p E R P Q:
-    Frame p R P Q → Frame p R (state_update E P) (state_update E Q).
+    Frame p R P Q → Frame p R (state_update E E P) (state_update E E Q).
   Proof.
     rewrite /Frame=> HR.
     rewrite state_update_frame_l.
@@ -488,7 +482,7 @@ Section state_update.
   Qed.
 
   Global Instance from_pure_bupd_state_update b E P φ :
-    FromPure b P φ → FromPure b (state_update E P) φ.
+    FromPure b P φ → FromPure b (state_update E E P) φ.
   Proof.
     rewrite /FromPure=> HP.
     iIntros "H !>".
@@ -496,7 +490,7 @@ Section state_update.
   Qed.
 
   Global Instance into_wand_state_update p q E R P Q :
-    IntoWand false false R P Q → IntoWand p q (state_update E R) (state_update E P) (state_update E Q).
+    IntoWand false false R P Q → IntoWand p q (state_update E E R) (state_update E E P) (state_update E E Q).
   Proof.
     rewrite /IntoWand /= => HR.
     rewrite !bi.intuitionistically_if_elim.
@@ -504,7 +498,7 @@ Section state_update.
   Qed.
 
   Global Instance into_wand_bupd_persistent_state_update p q E R P Q :
-    IntoWand false q R P Q → IntoWand p q (state_update E R) P (state_update E Q).
+    IntoWand false q R P Q → IntoWand p q (state_update E E R) P (state_update E E Q).
   Proof.
     rewrite /IntoWand /= => HR. rewrite bi.intuitionistically_if_elim.
     iIntros ">HR HP !>".
@@ -512,7 +506,7 @@ Section state_update.
   Qed.
 
   Global Instance into_wand_bupd_args_state_update p q E R P Q :
-    IntoWand p false R P Q → IntoWand' p q R (state_update E P) (state_update E Q).
+    IntoWand p false R P Q → IntoWand' p q R (state_update E E P) (state_update E E Q). 
   Proof.
     rewrite /IntoWand' /IntoWand /= => ->.
     rewrite bi.intuitionistically_if_elim.
@@ -523,7 +517,7 @@ Section state_update.
   Qed.
 
   Global Instance from_sep_bupd_state_update E P Q1 Q2 :
-    FromSep P Q1 Q2 → FromSep (state_update E P) (state_update E Q1) (state_update E Q2).
+    FromSep P Q1 Q2 → FromSep (state_update E E P) (state_update E E Q1) (state_update E E Q2).
   Proof.
     rewrite /FromSep=> HP.
     iIntros "[>HQ1 >HQ2] !>".
@@ -531,7 +525,7 @@ Section state_update.
   Qed.
 
   Global Instance from_exist_state_update {B} P E (Φ : B → iProp Σ) :
-    FromExist P Φ → FromExist (state_update E P) (λ b, state_update E (Φ b))%I.
+    FromExist P Φ → FromExist (state_update E E P) (λ b, state_update E E (Φ b))%I.
   Proof.
     rewrite /FromExist => HP.
     iIntros "[%x >Hx] !>".
@@ -539,7 +533,7 @@ Section state_update.
   Qed.
 
   Global Instance into_forall_state_update {B} P E (Φ : B → iProp Σ) :
-    IntoForall P Φ → IntoForall (state_update E P) (λ b, state_update E (Φ b))%I.
+    IntoForall P Φ → IntoForall (state_update E E P) (λ b, state_update E E (Φ b))%I.
   Proof.
     rewrite /IntoForall=>HP.
     iIntros "> H" (b) "!>".
@@ -547,32 +541,30 @@ Section state_update.
   Qed.
 
   Global Instance from_assumption_state_update p E P Q :
-    FromAssumption p P Q → KnownRFromAssumption p P (state_update E Q).
+    FromAssumption p P Q → KnownRFromAssumption p P (state_update E E Q).
   Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. iApply state_update_ret. Qed.
 
 
   (** state_update works for allocation of invariants and ghost resources *)
   Lemma state_update_inv_alloc E P N:
-    ▷ P -∗ state_update E (inv N P).
+    ▷ P -∗ state_update E E (inv N P).
   Proof.
     iIntros "HP".
     by iMod (inv_alloc with "[$]").
   Qed.
 
   Lemma state_update_inv_acc P E I N:
-    ↑N ⊆ E -> inv N I -∗ (▷I -∗ state_update (E∖↑N) (P∗▷I)) -∗ state_update E P.
+    ↑N ⊆ E -> inv N I -∗ (▷I -∗ state_update (E∖↑N) (E∖↑N) (P∗▷I)) -∗ state_update E E P.
   Proof.
     iIntros (Hsubset) "#Hinv H".
     iInv "Hinv" as "?" "Hclose".
     iMod ("H" with "[$]") as "[??]".
-    iFrame. iMod ("Hclose" with "[$]") as "_".
-    iModIntro.
-    iApply fupd_mask_intro_subseteq; [set_solver|done].
+    iFrame. by iMod ("Hclose" with "[$]") as "_".
   Qed.
   
   Context {A : cmra} `{i : inG Σ A}.
   Lemma state_update_ra_alloc E (a:A):
-    ✓ a -> ⊢ state_update E (∃ γ, own γ a).
+    ✓ a -> ⊢ state_update E E (∃ γ, own γ a).
   Proof.
     iIntros "%H".
     by iMod (own_alloc).