WIP.

theories/typing/lft_contexts.v

@@ -176,8 +176,16 @@ Section lft_contexts.
   Lemma lctx_lft_alive_tok κ F q :
     ↑lftN ⊆ F →
     lctx_lft_alive κ → elctx_interp E -∗ llctx_interp L q ={F}=∗
-      ∃ q', q'.[κ] ∗ llctx_interp L (q / 2) ∗ (q'.[κ] ={F}=∗ llctx_interp L (q / 2)).
-  Proof. iIntros (? Hal) "#HE [$ HL]". by iApply Hal. Qed.
+      ∃ q', q'.[κ] ∗ llctx_interp L q' ∗
+                   (q'.[κ] -∗ llctx_interp L q' ={F}=∗ llctx_interp L q).
+  Proof.
+    iIntros (? Hal) "#HE [HL1 HL2]".
+    iMod (Hal with "HE HL1") as (q') "[Htok Hclose]"; first done.
+    destruct (Qp_lower_bound (q/2) q') as (qq & q0  & q'0 & Hq & ->). rewrite Hq.
+    iExists qq. iDestruct "HL2" as "[$ HL]". iDestruct "Htok" as "[$ Htok]".
+    iIntros "!> Htok' HL'". iCombine "HL'" "HL" as "HL". rewrite -Hq. iFrame.
+    iApply "Hclose". iFrame.
+  Qed.
 
   Lemma lctx_lft_alive_static : lctx_lft_alive static.
   Proof.

theories/typing/lib/refcell/ref_code.v

@@ -64,15 +64,14 @@ Section ref_functions.
     iApply type_deref; [solve_typing..|]. iIntros (x').
 
 Typeclasses Opaque llctx_interp.
-    iIntros (tid) "#LFT HE Hna [HL1 HL2] Hk HT".
-
-
-    simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
     iDestruct "Hx'" as (ν q γ δ ty' lv lrc) "#(Hαν & Hfrac & Hshr & Hβδ & Hinv & H◯inv)".
     wp_op.
-    iMod (lctx_lft_alive_tok _ _ β with "HE HL") as (q') "[Hβ Hclose1]"; [solve_typing..|].
+    iMod (lctx_lft_alive_tok _ _ β with "HE HL") as (qβ) "(Hβ & HL & Hclose)"; [solve_typing..|].
+    iMod (lctx_lft_alive_tok _ _ α with "HE HL") as (qα) "(Hα & HL & Hclose')";
+      [solve_typing..|].
     iMod (lft_incl_acc with "Hβδ Hβ") as (qδ) "[Hδ Hcloseβ]". done.
     iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". done.
     iMod (na_bor_acc with "LFT Hinv Hδ Hna") as "(INV & Hna & Hcloseδ)"; [done..|].