allow opening invariants around typed_read_end and typed_write_end

theories/typing/atomic_bool.v

@@ -83,36 +83,29 @@ Section programs.
         T v (atomic_bool it PT PF) (t2mt (b @ boolean it))
       )
     ) -∗
-    typed_read_end true l β (atomic_bool it PT PF) (IntOp it) T.
+    typed_read_end true ⊤ l β (atomic_bool it PT PF) (IntOp it) T.
   Proof.
-    unfold destruct_hint. iIntros "HT Hl". destruct β.
-    - iDestruct "Hl" as "[%b [Hl Hif]]".
-      iApply fupd_mask_intro => //. iIntros "Hclose".
-      iDestruct (ty_aligned (IntOp _) MCNone with "Hl") as %?; [done|].
-      iDestruct (ty_deref (IntOp _) MCNone with "Hl") as (v) "[Hl #Hv]"; [done|].
-      iDestruct (ty_size_eq (IntOp _) MCNone with "Hv") as %?; [done|].
-      iExists _, _, _, (t2mt (b @ boolean it)).
-      iFrame "∗Hv". do 2 iSplitR => //=.
-      iIntros "!# %st Hl Hb". iMod "Hclose". iModIntro.
-      iExists _. iDestruct ("HT" with "Hif") as "[Hif $]".
-      iSplitR. { by iApply ty_memcast_compat_copy. }
-      iExists b. iFrame. by iApply (ty_ref (IntOp _) MCNone with "[] Hl Hv").
-    - iDestruct "Hl" as (Hly) "#Hinv".
-      iInv "Hinv" as (b) "[>Hl Hif]" "Hclose".
-      iApply fupd_mask_intro. set_solver. iIntros "Hclose2".
-      iDestruct (ty_aligned (IntOp _) MCNone with "Hl") as %?; [done|].
-      iDestruct (ty_deref (IntOp _) MCNone with "Hl") as (?) "[Hmt #Hv]"; [done|].
-      iDestruct (ty_size_eq (IntOp _) MCNone with "Hv") as %?; [done|].
-      iExists _, _, _, (t2mt (b @ boolean it)). iFrame "Hmt Hv".
-      iSplit; [done|]. iSplit; [done|].
-      iIntros "!# %st Hl Hb". iDestruct ("HT" with "Hif") as "[Hif HT]".
-      iMod "Hclose2" as "_". iExists _. iFrame.
-      iMod ("Hclose" with "[-]"). { iExists b. iModIntro. iFrame. by iApply (ty_ref (IntOp _) MCNone with "[] Hl Hv"). }
-      iModIntro. iSplit; [|by iSplit].
-      by iApply ty_memcast_compat_copy.
+    unfold destruct_hint. iIntros "HT".
+    iApply typed_read_end_mono_strong; [done|]. destruct β.
+    - iIntros "[%b [Hl Hif]] !>". iExists _, _, True%I. iFrame. iSplitR; [done|].
+      unshelve iApply (type_read_copy with "[HT Hif]"). { apply _. } simpl.
+      iSplit; [done|]. iSplit; [done|]. iIntros (v) "_ Hl Hv".
+      iDestruct ("HT" with "Hif") as "[Hif HT]". iExists _, _. iFrame "HT Hv".
+      iExists _. by iFrame.
+    - iIntros "[%Hly #Hinv] !>".
+      iExists Own, tytrue, True%I. iSplit; [done|]. iSplit; [done|].
+      iInv "Hinv" as (b) "[>Hl Hif]".
+      iApply typed_read_end_mono_strong; [done|]. iIntros "_ !>".
+      iExists _, _, _. iFrame.
+      unshelve iApply (type_read_copy with "[-]"). { apply _. } simpl.
+      iSplit; [done|]. iSplit; [iPureIntro; solve_ndisj|]. iIntros (v) "Hif Hl #Hv !>".
+      iDestruct ("HT" with "Hif") as "[Hif HT]". iExists tytrue, (t2mt tytrue).
+      iSplit; [done|]. iSplit; [ done |]. iModIntro.
+      iSplitL "Hl Hif". { iExists _. by iFrame. }
+      iIntros "_ _ _ !>". iExists _, _. iFrame "∗Hv". by iSplit.
   Qed.
   Global Instance type_read_atomic_bool_inst l β it PT PF:
-    TypedReadEnd true l β (atomic_bool it PT PF) (IntOp it) | 10 :=
+    TypedReadEnd true ⊤ l β (atomic_bool it PT PF) (IntOp it) | 10 :=
     λ T, i2p (type_read_atomic_bool l β it PT PF T).
 
   Lemma type_write_atomic_bool l β it PT PF v ty `{!Movable ty} T:
@@ -122,37 +115,30 @@ Section programs.
         T (atomic_bool it PT PF)
       )
     ) -∗
-    typed_write_end true (IntOp it) v ty l β (atomic_bool it PT PF) T.
+    typed_write_end true ⊤ (IntOp it) v ty l β (atomic_bool it PT PF) T.
   Proof.
-    iIntros "[%bnew Hsub] Hl Hv".
+    iIntros "[%bnew Hsub]". iApply typed_write_end_mono_strong; [done|].
+    iIntros "Hv Hl". iModIntro.
     iDestruct ("Hsub" with "Hv") as "(#Hnew&Hif_new&HT)".
-    iDestruct (ty_size_eq _ MCNone with "Hnew") as "$"; [done|].
     destruct β.
     - iDestruct "Hl" as "[%bold [Hl Hif_old]]".
-      iApply fupd_mask_intro => //. iIntros "Hc".
-      iDestruct (ty_aligned (IntOp _) MCNone with "Hl") as %?; [done|].
-      iDestruct (ty_deref (IntOp _) MCNone with "Hl") as (vb) "[Hmt Hold]"; [done|].
-      iDestruct (ty_size_eq (IntOp _) MCNone with "Hold") as %?; [done|].
-      iSplitL "Hmt". by iExists _; iFrame.
-      iIntros "!# Hl". iMod "Hc". iModIntro.
-      iExists _. iFrame. iExists bnew. iFrame.
-      iApply (@ty_ref with "[] Hl") => //. done.
-    - iDestruct "Hl" as (?) "#Hinv".
-      iInv "Hinv" as (b) "[>Hmt Hif]" "Hc".
-      iApply fupd_mask_intro; first solve_ndisj.
-      iIntros "Hc2".
-      iDestruct (ty_aligned (IntOp _) MCNone with "Hmt") as %?; [done|].
-      iDestruct (ty_deref (IntOp _) MCNone with "Hmt") as (?) "[Hmt #Hv]"; [done|].
-      iDestruct (ty_size_eq (IntOp _) MCNone with "Hv") as %?; [done|].
-      iSplitL "Hmt". { iExists _; by iFrame. }
-      iIntros "!# Hl". iMod "Hc2".
-      iMod ("Hc" with "[Hif_new Hl]").
-      { iModIntro. iExists bnew. iFrame. by iApply (ty_ref (IntOp _) MCNone with "[] Hl Hnew"). }
-      iModIntro. iExists _. iFrame. by iSplit.
-      Unshelve. apply: MCNone.
+      iExists (t2mt (_ @ boolean it)), _, _, True%I. iFrame "∗". iSplitR; [done|]. iSplitR; [done|].
+      unshelve iApply type_write_own_copy. { apply _. }
+      iSplit; [done|]. iSplit; [done|].
+      iIntros "Hv _ Hl !>". iExists _. iFrame "HT". iExists _. by iFrame.
+    - iExists (t2mt tytrue), Own, tytrue, True%I. iSplit; [done|]. iSplit; [done|]. iSplit; [done|].
+      iDestruct "Hl" as (?) "#Hinv".
+      iInv "Hinv" as (b) "[>Hmt Hif]".
+      iApply typed_write_end_mono_strong; [done|]. iIntros "_ _". iModIntro.
+      iExists (t2mt _), _, _, True%I. iFrame. iSplitR; [done|]. iSplitR; [done|].
+      unshelve iApply type_write_own_copy. { apply _. }
+      iSplit; [done|]. iSplit; [done|].
+      iIntros "Hv _ Hl !>". iExists tytrue. iSplit; [done|]. iModIntro.
+      iSplitL "Hif_new Hl". { iExists _. by iFrame. }
+      iIntros "_ _ !>". iExists _. iFrame "HT". by iSplit.
   Qed.
   Global Instance type_write_atomic_bool_inst l β it PT PF v ty `{!Movable ty}:
-    TypedWriteEnd true (IntOp it) v ty l β (atomic_bool it PT PF) | 10 :=
+    TypedWriteEnd true ⊤ (IntOp it) v ty l β (atomic_bool it PT PF) | 10 :=
     λ T, i2p (type_write_atomic_bool l β it PT PF v ty T).
 
   Lemma type_cas_atomic_bool (l : loc) β it PT PF lexp Pexp vnew Pnew T:

theories/typing/automation.v

@@ -65,8 +65,8 @@ Ltac convert_to_i2p_tac P ::=
   | typed_if ?ot ?v ?ty ?T1 ?T2 => uconstr:(((_ : TypedIf _ _ _) _ _).(i2p_proof))
   | typed_switch ?v ?ty ?it ?m ?ss ?def ?fn ?ls ?fr ?Q => uconstr:(((_ : TypedSwitch _ _ _) _ _ _ _ _ _ _).(i2p_proof))
   | typed_assert ?ot ?v ?ty ?s ?fn ?ls ?fr ?Q => uconstr:(((_ : TypedAssert _ _ _) _ _ _ _ _).(i2p_proof))
-  | typed_read_end ?a ?l ?β ?ty ?ly ?T => uconstr:(((_ : TypedReadEnd _ _ _ _ _) _).(i2p_proof))
-  | typed_write_end ?a ?ot ?v1 ?ty1 ?l2 ?β2 ?ty2 ?T => uconstr:(((_ : TypedWriteEnd _ _ _ _ _ _ _) _).(i2p_proof))
+  | typed_read_end ?a ?E ?l ?β ?ty ?ly ?T => uconstr:(((_ : TypedReadEnd _ _ _ _ _ _) _).(i2p_proof))
+  | typed_write_end ?a ?E ?ot ?v1 ?ty1 ?l2 ?β2 ?ty2 ?T => uconstr:(((_ : TypedWriteEnd _ _ _ _ _ _ _ _) _).(i2p_proof))
   | typed_addr_of_end ?l ?β ?ty ?T => uconstr:(((_ : TypedAddrOfEnd _ _ _) _).(i2p_proof))
   | typed_cas ?ot ?v1 ?P1 ?v2 ?P2 ?v3 ?P3 ?T => uconstr:(((_ : TypedCas _ _ _ _ _ _ _) _).(i2p_proof))
   | typed_annot_expr ?n ?a ?v ?P ?T => uconstr:(((_ : TypedAnnotExpr _ _ _ _) _) .(i2p_proof))

theories/typing/bytes.v

@@ -230,24 +230,24 @@ Section uninit.
     iExists _. by iFrame.
   Qed.
 
-  Lemma type_read_move_copy T l ty ot a `{!Movable ty}:
+  Lemma type_read_move_copy T E l ty ot a `{!Movable ty}:
     (⌜ty.(ty_has_op_type) ot MCCopy⌝ ∗ ∀ v, T v (uninit (ot_layout ot)) (t2mt ty)) -∗
-      typed_read_end a l Own ty ot T.
+      typed_read_end a E l Own ty ot T.
   Proof.
-    iIntros "[% HT] Hl".
-    iApply fupd_mask_intro => //. iIntros "Hclose".
+    rewrite /typed_read_end. iIntros "[% HT] Hl".
+    iApply fupd_mask_intro; [destruct a; solve_ndisj|]. iIntros "Hclose".
     iDestruct (ty_aligned with "Hl") as %?; [done|].
     iDestruct (ty_deref with "Hl") as (v) "[Hl Hv]"; [done|].
     iDestruct (ty_size_eq with "Hv") as %?; [done|].
-    iExists _, _, _, (t2mt _). iFrame. do 2 iSplit => //=.
+    iExists _, _, (t2mt _). iFrame. do 2 iSplit => //=.
     iIntros "!# %st Hl Hv". iMod "Hclose". iModIntro.
     iDestruct (ty_memcast_compat_copy with "Hv") as "Hv"; [done|].
-    iExists (t2mt ty). iFrame. iSplitR "HT"; [|done].
+    iExists _, (t2mt ty). iFrame. iSplitR "HT"; [|done].
     iExists _. iFrame. iPureIntro. split_and! => //. by apply: Forall_true.
   Qed.
-  Global Instance type_read_move_copy_inst l ty ot a `{!Movable ty} :
-    TypedReadEnd a l Own ty ot | 70 :=
-    λ T, i2p (type_read_move_copy T l ty ot a).
+  Global Instance type_read_move_copy_inst l E ty ot a `{!Movable ty} :
+    TypedReadEnd a E l Own ty ot | 70 :=
+    λ T, i2p (type_read_move_copy T E l ty ot a).
 End uninit.
 
 Notation "uninit< ly >" := (uninit ly) (only printing, format "'uninit<' ly '>'") : printing_sugar.

theories/typing/locked.v

@@ -64,7 +64,7 @@ Section type.
   Next Obligation. iIntros (A γ n x ty ? ot mt v ?) "Hl". by iApply ty_aligned. Qed.
   Next Obligation. iIntros (A γ n x ty ? ot mt v ?) "Hl". by iApply ty_size_eq. Qed.
   Next Obligation. iIntros (A γ n x ty ? ot mt l ?) "Hl". by iApply ty_deref. Qed.
-  Next Obligation. iIntros (A γ n x ty ? ot mt l ? ?) "Hl". by iApply ty_ref. Qed.
+  Next Obligation. iIntros (A γ n x ty ? ot mt l ? ?). by iApply ty_ref. Qed.
   Next Obligation. iIntros (A γ n x ty ? v ot mt st ?) "Hl". by iApply ty_memcast_compat. Qed.
 
   Lemma tylocked_simplify_hyp_place A γ n x (ty : A → type) T l:

theories/typing/optional.v

@@ -125,7 +125,7 @@ Section optional.
   Proof.
     iIntros (v) "[Heq P] H". rewrite /ty_own_val /=. iDestruct "Heq" as %->.
     iDestruct "H" as "[[?H] | [??]]"; last (iRight; by iFrame).
-    iLeft. iFrame. iApply (simple_subsume_val with "P H").
+    iLeft. iFrame. iApply (@simple_subsume_val with "P H").
   Qed.
 
   Lemma subsume_optional_optty_ref b ty optty l β T:
@@ -444,14 +444,14 @@ Section optionalO.
     TypedBinOp v1 (v1 ◁ᵥ b @ optionalO ty optty)%I v2 (v2 ◁ᵥ optty) (NeOp i32) ot1 ot2 :=
     λ T, i2p (type_neq_optionalO A v1 v2 ty optty ot1 ot2 T b).
 
-  Lemma read_optionalO_case A l b (ty : A → type) optty ly (T : val → type → _) a:
-    destruct_hint (DHintDestruct _ b) DestructHintOptionalO (typed_read_end a l Own (if b is Some x then ty x else optty) ly T) -∗
-      typed_read_end a l Own (b @ optionalO ty optty) ly T.
+  Lemma read_optionalO_case A E l b (ty : A → type) optty ly (T : val → type → _) a:
+    destruct_hint (DHintDestruct _ b) DestructHintOptionalO (typed_read_end a E l Own (if b is Some x then ty x else optty) ly T) -∗
+      typed_read_end a E l Own (b @ optionalO ty optty) ly T.
   Proof. by destruct b. Qed.
   (* This should be tried very late *)
-  Global Instance read_optionalO_case_inst A l b (ty : A → type) optty ly a:
-    TypedReadEnd a l Own (b @ optionalO ty optty) ly | 1001 :=
-    λ T, i2p (read_optionalO_case A l b ty optty ly T a).
+  Global Instance read_optionalO_case_inst A E l b (ty : A → type) optty ly a:
+    TypedReadEnd a E l Own (b @ optionalO ty optty) ly | 1001 :=
+    λ T, i2p (read_optionalO_case A E l b ty optty ly T a).
 
 
   Global Instance strip_guarded_optionalO A x E1 E2 (ty : A → type) ty' optty β `{!∀ y, StripGuarded β E1 E2 (ty y) (ty' y)}:

theories/typing/singleton.v

@@ -69,54 +69,54 @@ Section value.
     SimplifyHypPlace l Own (value ot v)%I (Some 50%N) | 20 :=
     λ T, i2p (value_merge v l ot T).
 
-  Lemma type_read_move T l ty ot a `{!Movable ty} `{!CanSolve (ty.(ty_has_op_type) ot MCId)}:
+  Lemma type_read_move T l ty ot a E `{!Movable ty} `{!CanSolve (ty.(ty_has_op_type) ot MCId)}:
     (∀ v, T v (value ot v) (t2mt ty)) -∗
-      typed_read_end a l Own ty ot T.
+      typed_read_end a E l Own ty ot T.
   Proof.
-    unfold CanSolve in *. iIntros "HT Hl".
-    iApply fupd_mask_intro => //. iIntros "Hclose".
+    unfold CanSolve, typed_read_end in *. iIntros "HT Hl".
+    iApply fupd_mask_intro; [destruct a; solve_ndisj|]. iIntros "Hclose".
     iDestruct (ty_aligned with "Hl") as %?; [done|].
     iDestruct (ty_deref with "Hl") as (v) "[Hl Hv]"; [done|].
     iDestruct (ty_size_eq with "Hv") as %?; [done|].
     iDestruct (ty_memcast_compat_id with "Hv") as %Hid; [done|].
-    iExists _, _, _, (t2mt _). iFrame. do 2 iSplit => //=.
+    iExists _, _, (t2mt _). iFrame. do 2 iSplit => //=.
     iIntros "!# %st Hl Hv". iMod "Hclose".
-    iExists (t2mt ty). rewrite Hid. iFrame "Hv". iSplitR "HT" => //.
+    iExists _, (t2mt ty). rewrite Hid. iFrame "Hv". iSplitR "HT" => //.
     by iFrame.
   Qed.
   (* This needs to be a Hint Extern because the CanSolve depends on Movable *)
-  Global Definition type_read_move_inst l ty ot a `{!Movable ty} `{!CanSolve (ty.(ty_has_op_type) ot MCId)}:
-    TypedReadEnd a l Own ty ot :=
-    λ T, i2p (type_read_move T l ty ot a).
+  Global Definition type_read_move_inst l ty ot a E `{!Movable ty} `{!CanSolve (ty.(ty_has_op_type) ot MCId)}:
+    TypedReadEnd a E l Own ty ot :=
+    λ T, i2p (type_read_move T l ty ot a E).
 
   (* TODO: this constraint on the layout is too strong, we only need
   that the length is the same and the alignment is lower. Adapt when necessary. *)
-  Lemma type_write_own a ty `{!Movable ty} T l2 ty2 v `{!Movable ty2} ot `{!CanSolve (ty.(ty_has_op_type) ot MCId)}:
+  Lemma type_write_own a ty `{!Movable ty} T E l2 ty2 v `{!Movable ty2} ot `{!CanSolve (ty.(ty_has_op_type) ot MCId)}:
     ⌜ty2.(ty_has_op_type) (UntypedOp (ot_layout ot)) MCNone⌝ ∗ (∀ v', v ◁ᵥ ty -∗ v' ◁ᵥ ty2 -∗ T (value ot v)) -∗
-    typed_write_end a ot v ty l2 Own ty2 T.
+    typed_write_end a E ot v ty l2 Own ty2 T.
   Proof.
-    unfold CanSolve in *. iDestruct 1 as (?) "HT". iIntros "Hl Hv".
+    unfold CanSolve, typed_write_end in *. iDestruct 1 as (?) "HT". iIntros "Hl Hv".
     iDestruct (ty_aligned with "Hl") as %?; [done|].
     iDestruct (ty_deref with "Hl") as (v') "[Hl Hv']"; [done|].
     iDestruct (ty_size_eq with "Hv") as %?; [done|].
     iDestruct (ty_size_eq with "Hv'") as %?; [done|].
     iDestruct (ty_memcast_compat_id with "Hv") as %Hid; [done|].
-    iApply fupd_mask_intro => //. iIntros "Hmask".
+    iApply fupd_mask_intro; [destruct a; solve_ndisj|]. iIntros "Hmask".
     iSplit; [done|]. iSplitL "Hl". { iExists _. by iFrame. }
     iIntros "!# Hl". iMod "Hmask". iModIntro.
     iExists _. iDestruct ("HT" with "Hv Hv'") as "$". by iFrame.
   Qed.
   (* This needs to be a Hint Extern because the CanSolve depends on Movable *)
-  Global Definition type_write_own_inst a ty `{!Movable ty} l2 ty2 v `{!Movable ty2} ot `{!CanSolve (ty.(ty_has_op_type) ot MCId)}:
-    TypedWriteEnd a ot v ty l2 Own ty2 :=
-    λ T, i2p (type_write_own a ty T l2 ty2 v ot).
+  Global Definition type_write_own_inst a ty `{!Movable ty} E l2 ty2 v `{!Movable ty2} ot `{!CanSolve (ty.(ty_has_op_type) ot MCId)}:
+    TypedWriteEnd a E ot v ty l2 Own ty2 :=
+    λ T, i2p (type_write_own a ty T E l2 ty2 v ot).
 End value.
 Notation "value< ot , v >" := (value ot v) (only printing, format "'value<' ot ',' v '>'") : printing_sugar.
 
-Global Hint Extern 50 (TypedReadEnd _ _ Own _ _) =>
-  unshelve notypeclasses refine (type_read_move_inst _ _ _ _ ) : typeclass_instances.
-Global Hint Extern 50 (TypedWriteEnd _ _ _ _ _ Own _) =>
-  unshelve notypeclasses refine (type_write_own_inst _ _ _ _ _ _) : typeclass_instances.
+Global Hint Extern 50 (TypedReadEnd _ _ _ Own _ _) =>
+  unshelve notypeclasses refine (type_read_move_inst _ _ _ _ _ ) : typeclass_instances.
+Global Hint Extern 50 (TypedWriteEnd _ _ _ _ _ _ Own _) =>
+  unshelve notypeclasses refine (type_write_own_inst _ _ _ _ _ _ _) : typeclass_instances.
 
 
 Section at_value.
@@ -228,33 +228,35 @@ Section place.
     TypedPlace P l β1 ty1 | 1000 :=
     λ T, i2p (typed_place_simpl P l ty1 β1 T n).
 
-  Lemma typed_read_end_simpl l β ty ly n T {SH:SimplifyHyp (l ◁ₗ{β} ty) (Some n)} a:
+  Lemma typed_read_end_simpl E l β ty ly n T {SH:SimplifyHyp (l ◁ₗ{β} ty) (Some n)} a:
     (SH (find_in_context (FindLoc l) (λ '(β2, ty2),
-        typed_read_end a l β2 ty2 ly (λ v ty' ty3, l ◁ₗ{β2} ty' -∗ T v (place l) ty3)))).(i2p_P) -∗
-    typed_read_end a l β ty ly T.
+        typed_read_end a E l β2 ty2 ly (λ v ty' ty3, l ◁ₗ{β2} ty' -∗ T v (place l) ty3)))).(i2p_P) -∗
+    typed_read_end a E l β ty ly T.
   Proof.
-    iIntros "SH Hl". iDestruct (i2p_proof with "SH Hl") as ([β2 ty2]) "[Hl HP]".
-    iMod ("HP" with "Hl") as (q v ty' ty3 ? ?) "(Hl & Hv & HP)". iIntros "!#".
-    iExists _, _, _, _. iFrame "Hl Hv". do 2 (iSplit;[done|]).  iIntros "!# %st Hl Hv".
-    iMod ("HP" with "Hl Hv") as (ty4) "(Hv & Hl & HT)". iModIntro. iExists _. iFrame.
-    iSplitR; last by iApply "HT". done.
+    iIntros "SH". iApply typed_read_end_mono_strong; [done|]. iIntros "Hl !>".
+    iDestruct (i2p_proof with "SH Hl") as ([β2 ty2]) "[Hl HP]" => /=.
+    iExists _, _, True%I. iFrame. iSplit; [done|].
+    iApply (typed_read_end_wand with "HP"). iIntros (v ty1 ty2') "HT _ Hl Hv !>".
+    iExists (place l), _. iFrame. iSplit; [done|]. by iApply "HT".
   Qed.
-  Global Instance typed_read_end_simpl_inst l β ty ly n a `{!SimplifyHyp (l ◁ₗ{β} ty) (Some n)}:
-    TypedReadEnd a l β ty ly | 1000 :=
-    λ T, i2p (typed_read_end_simpl l β ty ly n T a).
+  Global Instance typed_read_end_simpl_inst E l β ty ly n a `{!SimplifyHyp (l ◁ₗ{β} ty) (Some n)}:
+    TypedReadEnd a E l β ty ly | 1000 :=
+    λ T, i2p (typed_read_end_simpl E l β ty ly n T a).
 
-  Lemma typed_write_end_simpl b ot v ty1 `{!Movable ty1} l β ty2 n T {SH:SimplifyHyp (l ◁ₗ{β} ty2) (Some n)}:
+  Lemma typed_write_end_simpl b E ot v ty1 `{!Movable ty1} l β ty2 n T {SH:SimplifyHyp (l ◁ₗ{β} ty2) (Some n)}:
     (SH (find_in_context (FindLoc l) (λ '(β3, ty3),
-        typed_write_end b ot v ty1 l β3 ty3 (λ ty', l ◁ₗ{β3} ty' -∗ T (place l))))).(i2p_P) -∗
-    typed_write_end b ot v ty1 l β ty2 T.
+        typed_write_end b E ot v ty1 l β3 ty3 (λ ty', l ◁ₗ{β3} ty' -∗ T (place l))))).(i2p_P) -∗
+    typed_write_end b E ot v ty1 l β ty2 T.
   Proof.
-    iIntros "SH Hl Hv". iDestruct (i2p_proof with "SH Hl") as ([β3 ty3]) "[Hl HP]".
-    iMod ("HP" with "Hl Hv") as "[$ [$ HP]]". iIntros "!# !# Hl".
-    iMod ("HP" with "Hl") as (ty') "[Hl HT]". iModIntro. iExists _. iSplitR; last by iApply "HT". done.
+    iIntros "SH". iApply typed_write_end_mono_strong; [done|]. iIntros "Hv Hl !>".
+    iDestruct (i2p_proof with "SH Hl") as ([β2' ty2']) "[Hl HP]" => /=.
+    iExists (t2mt _), _, _, True%I. iFrame. iSplit; [done|].
+    iApply (typed_write_end_wand with "HP"). iIntros (ty3) "HT _ Hl !>".
+    iExists (place l). iSplit; [done|]. by iApply "HT".
   Qed.
-  Global Instance typed_write_end_simpl_inst b ot v ty1 `{!Movable ty1} l β ty2 n `{!SimplifyHyp (l ◁ₗ{β} ty2) (Some n)}:
-    TypedWriteEnd b ot v ty1 l β ty2 | 1000 :=
-    λ T, i2p (typed_write_end_simpl b ot v ty1 l β ty2 n T).
+  Global Instance typed_write_end_simpl_inst b E ot v ty1 `{!Movable ty1} l β ty2 n `{!SimplifyHyp (l ◁ₗ{β} ty2) (Some n)}:
+    TypedWriteEnd b E ot v ty1 l β ty2 | 1000 :=
+    λ T, i2p (typed_write_end_simpl b E ot v ty1 l β ty2 n T).
 
 End place.
 Notation "place< l >" := (place l) (only printing, format "'place<' l '>'") : printing_sugar.

theories/typing/type.v

@@ -118,6 +118,7 @@ We will need an additional parameter
 
 Definition shrN : namespace := nroot.@"shrN".
 Definition mtN : namespace := nroot.@"mtN".
+Definition mtE : coPset := ↑mtN.
 Inductive own_state : Type :=
 | Own | Shr.
 Definition own_state_min (β1 β2 : own_state) : own_state :=
@@ -275,6 +276,7 @@ Class Movable `{!typeG Σ} (t : type) := {
 }.
 Arguments ty_has_op_type {_ _} _ {_}.
 Arguments ty_own_val {_ _} _ {_} : simpl never.
+Global Hint Mode Movable + + ! : typeclass_instances.
 
 (* Lift Movable to lists.  We cannot use `Forall` because that one is restricted to Prop. *)
 Inductive MovableLst `{typeG Σ} : list type → Type :=
@@ -282,6 +284,7 @@ Inductive MovableLst `{typeG Σ} : list type → Type :=
 | ml_cons ty tyl `{!Movable ty, !MovableLst tyl} : MovableLst (ty::tyl).
 Existing Class MovableLst.
 Existing Instances ml_nil ml_cons.
+Global Hint Mode MovableLst + + ! : typeclass_instances.
 
 (* movable type *)
 Record mtype `{!typeG Σ} : Type := {
@@ -388,7 +391,7 @@ End movable.
 Class Copyable `{!typeG Σ} (ty : type) `{!Movable ty} := {
   copy_own_persistent v : Persistent (ty.(ty_own_val) v);
   copy_shr_acc E ot l :
-    ↑mtN ⊆ E → ty.(ty_has_op_type) ot MCCopy →
+    mtE ⊆ E → ty.(ty_has_op_type) ot MCCopy →
     ty.(ty_own) Shr l ={E}=∗ ⌜l `has_layout_loc` ot_layout ot⌝ ∗
        (* TODO: the closing conjuct does not make much sense with True *)
        ∃ q' vl, l ↦{q'} vl ∗ ▷ ty.(ty_own_val) vl ∗ (▷l ↦{q'} vl ={E}=∗ True)
@@ -465,6 +468,20 @@ Notation "'own' l ∶ ty" := (ty_own ty Own l) (at level 100, only printing) : p
 Notation "'shr' l ∶ ty" := (ty_own ty Shr l) (at level 100, only printing) : printing_sugar.
 Notation "v ∶ ty" := (ty_own_val ty v) (at level 200, only printing) : printing_sugar.
 
+(*** tytrue *)
+Section true.
+  Context `{!typeG Σ}.
+  (** tytrue is a dummy type that all values and locations have. *)
+  Program Definition tytrue : type := {|
+    ty_own _ _ := True%I
+  |}.
+  Next Obligation. iIntros (???) "?". done. Qed.
+  Global Program Instance tytrue_movable : Movable tytrue := {|
+    ty_has_op_type _ _ := False;
+    ty_own_val _ := True%I;
+  |}.
+  Solve Obligations with done.
+End true.
 (*** refinement types *)
 Record rtype `{!typeG Σ} := {
   rty_type : Type;