.gitignore

@@ -13,3 +13,4 @@ build-dep/
 Makefile.coq
 Makefile.coq.conf
 .coqdeps.d
+_opam

.gitlab-ci.yml

@@ -35,10 +35,6 @@ build-coq.8.7.2:
   <<: *template
   variables:
     OPAM_PINS: "coq version 8.7.2"
-    TIMING_PROJECT: "lambda-rust"
-    TIMING_CONF: "coq-8.7.2"
-  tags:
-  - fp-timing
 
 build-coq.dev:
   <<: *template

Missing.md

+Missing APIs from the types we cover (APIs have been added after this formalization was done)
+
+# Cell
+
+* Structural conversion for slices.  The matching operations in our model would be
+  `&mut Cell<(A, B)>` -> `(&mut Cell<A>, &mut Cell<B>)` and
+  `&Cell<(A, B)>` -> `(&Cell<A>, &Cell<B>)`.
+
+# RefCell
+
+* RefMut::split: https://github.com/rust-lang/rust/pull/51466

_CoqProject

@@ -46,26 +46,25 @@ theories/typing/cont.v
 theories/typing/function.v
 theories/typing/typing.v
 theories/typing/soundness.v
-theories/typing/lib/cell.v
-theories/typing/lib/diverging_static.v
-theories/typing/lib/fake_shared.v
-theories/typing/lib/option.v
 theories/typing/lib/panic.v
-theories/typing/lib/swap.v
-theories/typing/lib/take_mut.v
+theories/typing/lib/option.v
+theories/typing/lib/fake_shared.v
+theories/typing/lib/cell.v
 theories/typing/lib/spawn.v
 theories/typing/lib/join.v
+theories/typing/lib/diverging_static.v
+theories/typing/lib/take_mut.v
+theories/typing/lib/rc/rc.v
+theories/typing/lib/rc/weak.v
 theories/typing/lib/arc.v
 theories/typing/lib/mutex/mutex.v
 theories/typing/lib/mutex/mutexguard.v
-theories/typing/lib/rc/rc.v
-theories/typing/lib/rc/weak.v
-theories/typing/lib/refcell/refcell_code.v
 theories/typing/lib/refcell/refcell.v
+theories/typing/lib/refcell/ref.v
+theories/typing/lib/refcell/refmut.v
+theories/typing/lib/refcell/refcell_code.v
 theories/typing/lib/refcell/ref_code.v
 theories/typing/lib/refcell/refmut_code.v
-theories/typing/lib/refcell/refmut.v
-theories/typing/lib/refcell/ref.v
 theories/typing/lib/rwlock/rwlock.v
 theories/typing/lib/rwlock/rwlockreadguard.v
 theories/typing/lib/rwlock/rwlockwriteguard.v

theories/lifetime/lifetime_sig.v

@@ -47,7 +47,8 @@ Module Type lifetime_sig.
   End defs.
 
   (** Notation *)
-  Notation "q .[ κ ]" := (lft_tok q κ) (format "q .[ κ ]", at level 0) : bi_scope.
+  Notation "q .[ κ ]" := (lft_tok q κ)
+      (format "q .[ κ ]", at level 0) : bi_scope.
   Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): bi_scope.
 
   Notation "&{ κ }" := (bor κ) (format "&{ κ }") : bi_scope.

theories/lifetime/model/accessors.v

 From lrust.lifetime Require Export primitive.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import csum auth frac gmap agree gset.
-From iris.bi Require Import big_op.
 Set Default Proof Using "Type".
 
 Section accessors.

theories/lifetime/model/borrow.v

 From lrust.lifetime Require Export primitive.
 From lrust.lifetime Require Export faking.
 From iris.algebra Require Import csum auth frac gmap agree gset.
-From iris.bi Require Import big_op.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type*".
 

theories/lifetime/model/borrow_sep.v

 From lrust.lifetime Require Export primitive.
 From lrust.lifetime Require Export faking reborrow.
 From iris.algebra Require Import csum auth frac gmap agree.
-From iris.bi Require Import big_op.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type*".
 

theories/lifetime/model/creation.v

 From lrust.lifetime Require Export primitive.
 From lrust.lifetime Require Import faking.
 From iris.algebra Require Import csum auth frac gmap agree gset.
-From iris.bi Require Import big_op.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type*".
 

theories/lifetime/model/definitions.v

 From iris.algebra Require Import csum auth frac gmap agree gset.
-From iris.bi Require Import big_op.
 From lrust.lifetime.model Require Import boxes.
 From lrust.lifetime Require Export lifetime_sig.
 From gpfsl.lang Require Export lattice_cmra.

theories/lifetime/model/faking.v

 From lrust.lifetime.model Require Export primitive.
 From iris.algebra Require Import csum auth frac gmap agree gset.
-From iris.bi Require Import big_op.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type*".
 

theories/lifetime/model/primitive.v

@@ -76,9 +76,6 @@ Qed.
 Global Instance own_bor_into_sep κ x x1 x2 :
   IsOp x x1 x2 → IntoSep (own_bor  κ x) (own_bor κ x1) (own_bor κ x2).
 Proof. rewrite /IsOp /IntoSep=>->. by rewrite own_bor_op. Qed.
-Global Instance own_bor_into_and κ x x1 x2 p :
-  IsOp x x1 x2 → IntoAnd p (own_bor  κ x) (own_bor κ x1) (own_bor κ x2).
-Proof. rewrite /IsOp /IntoAnd=>->. by rewrite own_bor_op sep_and. Qed.
 Lemma own_bor_valid κ x : own_bor κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
 Lemma own_bor_valid_2 κ x y : own_bor κ x -∗ own_bor κ y -∗ ✓ (x ⋅ y).
@@ -110,11 +107,8 @@ Proof.
 Qed.
 Global Instance own_cnt_into_sep κ x x1 x2 :
   IsOp x x1 x2 → IntoSep (own_cnt κ x) (own_cnt κ x1) (own_cnt κ x2).
-Proof. rewrite /IsOp /IntoSep=> /leibniz_equiv_iff->. by rewrite -own_cnt_op. Qed.
-Global Instance own_cnt_into_and κ x x1 x2 p :
-  IsOp x x1 x2 → IntoAnd p (own_cnt κ x) (own_cnt κ x1) (own_cnt κ x2).
 Proof.
-  rewrite /IsOp /IntoAnd=> /leibniz_equiv_iff->. by rewrite own_cnt_op sep_and.
+  rewrite /IsOp /IntoSep=> /leibniz_equiv_iff->. by rewrite -own_cnt_op.
 Qed.
 Lemma own_cnt_valid κ x : own_cnt κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
@@ -147,11 +141,8 @@ Proof.
 Qed.
 Global Instance own_inh_into_sep κ x x1 x2 :
   IsOp x x1 x2 → IntoSep (own_inh κ x) (own_inh κ x1) (own_inh κ x2).
-Proof. rewrite /IsOp /IntoSep=> /leibniz_equiv_iff->. by rewrite -own_inh_op. Qed.
-Global Instance own_inh_into_and κ x x1 x2 p :
-  IsOp x x1 x2 → IntoAnd p (own_inh κ x) (own_inh κ x1) (own_inh κ x2).
 Proof.
-  rewrite /IsOp /IntoAnd=> /leibniz_equiv_iff->. by rewrite own_inh_op sep_and.
+  rewrite /IsOp /IntoSep=> /leibniz_equiv_iff->. by rewrite -own_inh_op.
 Qed.
 Lemma own_inh_valid κ x : own_inh κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.

theories/lifetime/model/reborrow.v

 From lrust.lifetime Require Import borrow accessors.
 From iris.algebra Require Import csum auth frac gmap agree gset.
-From iris.bi Require Import big_op.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type*".
 

theories/typing/function.v

@@ -407,7 +407,7 @@ Section typing.
                      (subst_v (fb :: BNamed "return" :: argsb) (f ::: k ::: args) e)) -∗
     typed_instruction_ty E L T ef (fn fp).
   Proof.
-    iIntros (<- ->) "#Hbody". iIntros (tid) "#LFT _ $ $ #HT". iApply wp_value.
+    iIntros (<- ->) "#Hbody /=". iIntros (tid) "#LFT _ $ $ #HT". iApply wp_value.
     rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
     { unlock. rewrite /= decide_left. done. }
     iExists fb, _, argsb, e, _. iSplit. done. iSplit. done. iNext.

theories/typing/lib/cell.v

 From iris.proofmode Require Import tactics.
-From iris.bi Require Import big_op.
 From lrust.lang Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Export type.

theories/typing/lib/fake_shared.v

@@ -25,7 +25,7 @@ Section fake_shared.
       { iApply frac_bor_iff; last done. iIntros "!>!# *".
         rewrite heap_mapsto_vec_singleton. iSplit; auto. }
       iDestruct "H" as "#H". iIntros "!# * % $". iApply step_fupd_intro. set_solver.
-      by iApply ty_shr_mono. }
+      simpl. by iApply ty_shr_mono. }
     do 2 wp_seq.
     iApply (type_type [] _ _ [ x ◁ box (&shr{α}(box ty)) ]
             with "[] LFT [] Hna HL Hk [HT]"); last first.

theories/typing/lib/join.v

 From iris.proofmode Require Import tactics.
-From iris.bi Require Import big_op.
 From lrust.lang Require Import spawn.
 From lrust.typing Require Export type.
 From lrust.typing Require Import typing.

theories/typing/lib/mutex/mutexguard.v

@@ -202,8 +202,8 @@ Section code.
       delete [ #1; "g"];; return: ["r"].
 
   Lemma mutexguard_derefmut_type ty `{!TyWf ty} :
-    typed_val mutexguard_derefmut (fn (fun '(α, β) =>
-      FP_wf ∅ [# &uniq{α}(mutexguard β ty)]%T (&uniq{α}ty)%T)).
+    typed_val mutexguard_derefmut
+              (fn(∀ '(α, β), ∅; &uniq{α}(mutexguard β ty)) → &uniq{α}ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>g. simpl_subst.
@@ -244,8 +244,8 @@ Section code.
   Definition mutexguard_deref : val := mutexguard_derefmut.
 
   Lemma mutexguard_deref_type ty `{!TyWf ty} :
-    typed_val mutexguard_derefmut (fn (fun '(α, β) =>
-      FP_wf ∅ [# &shr{α}(mutexguard β ty)]%T (&shr{α}ty)%T)).
+    typed_val mutexguard_derefmut
+              (fn(∀ '(α, β), ∅; &shr{α}(mutexguard β ty)) → &shr{α}ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>g. simpl_subst.

theories/typing/lib/refcell/ref.v

@@ -25,7 +25,7 @@ Section ref.
          | [ #(LitLoc lv);  #(LitLoc lrc) ] =>
            ∃ ν q γ β ty', ty.(ty_shr) (α ⊓ ν) tid lv ∗
              α ⊑ β ∗ &na{β, tid, refcell_invN}(refcell_inv tid lrc γ β ty') ∗
-             q.[ν] ∗ ⎡own γ (◯ reading_st q ν)⎤
+             q.[ν] ∗ ⎡own γ (◯ reading_stR q ν)⎤
          | _ => False
          end;
        ty_shr κ tid l :=
@@ -33,7 +33,7 @@ Section ref.
              κ ⊑ ν ∗ &frac{κ} (λ q, l↦∗{q} [ #lv; #lrc]) ∗
              ▷ ty.(ty_shr) (α ⊓ ν) tid lv ∗
              ▷ (α ⊑ β) ∗ ▷ &na{β, tid, refcell_invN}(refcell_inv tid lrc γ β ty') ∗
-             &na{κ, tid, refcell_refN}⎡own γ (◯ reading_st q ν)⎤ |}%I.
+             &na{κ, tid, refcell_refN}⎡own γ (◯ reading_stR q ν)⎤ |}%I.
   Next Obligation. iIntros (???[|[[]|][|[[]|][]]]) "?"; auto. Qed.
   Next Obligation.
     iIntros (α ty E κ l tid q ?) "#LFT Hb Htok".

theories/typing/lib/refcell/ref_code.v

@@ -11,34 +11,27 @@ Section ref_functions.
 
   Lemma refcell_inv_reading_inv tid l γ α ty q ν :
     refcell_inv tid l γ α ty -∗
-    ⎡own γ (◯ reading_st q ν)⎤ -∗
+    ⎡own γ (◯ reading_stR q ν)⎤ -∗
     ∃ (q' : Qp) n, l ↦ #(Zpos n) ∗ ⌜(q ≤ q')%Qc⌝ ∗
-            ⎡own γ (● Some (to_agree ν, Cinr (q', n)) ⋅ ◯ reading_st q ν)⎤ ∗
-            ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
+            ⎡own γ (● (refcell_st_to_R $ Some (ν, false, q', n)) ⋅ ◯ reading_stR q ν)⎤ ∗
             ((1).[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ &{α}((l +ₗ 1) ↦∗: ty_own ty tid)) ∗
-            ∃ q'', ⌜(q' + q'' = 1)%Qp⌝ ∗ q''.[ν].
+            (∃ q'', ⌜(q' + q'' = 1)%Qp⌝ ∗ q''.[ν]) ∗
+            ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1).
   Proof.
     iIntros "INV H◯".
     iDestruct "INV" as (st) "(H↦lrc & H● & INV)".
-    iAssert (∃ q' n, st ≡ Some (to_agree ν, Cinr (q', n)) ∗ ⌜q ≤ q'⌝%Qc)%I with
-       "[#]" as (q' n) "[Hst %]".
-    { iDestruct (own_valid_2 with "H● H◯") as %[[[=]|
-       (? & [agν st'] & [=<-] & -> & [Heq|Hle])]%option_included Hv]%auth_valid_discrete_2.
-      - iExists q, xH. iSplit; iPureIntro. by constructor. done.
-      - iClear "∗#".
-        revert Hle Hv=>/prod_included [/= /agree_included Hag /csum_included
-              [-> [//] | [[?[?[//]]] | [?[[q' n] [Heq [-> Hle]]]]]]] [Hagok _].
-        revert Heq. intros [= <-]. revert Hle=>/prod_included [/= Hqq' _].
-        iExists q', n. iSplit.
-        + iPureIntro. rewrite (agree_op_inv agν) //. by rewrite comm -Hag.
-        + by revert Hqq'=>/frac_included_weak. }
-    iDestruct "Hst" as %[st' [-> Hst']]%equiv_Some_inv_r'.
-    destruct st' as [?[|[]|]]; destruct Hst' as [Hag Hst']; try by inversion Hst'.
-    apply (inj Cinr), (inj2 pair) in Hst'.
-    destruct Hst' as [<-%leibniz_equiv <-%leibniz_equiv]. simpl in *.
-    setoid_rewrite <-Hag. iDestruct "INV" as (ν') "(Hag & Hν & Hshr & Hq')".
-    iDestruct "Hag" as %<-%(inj to_agree)%leibniz_equiv.
-    iExists q', n. rewrite own_op. by iFrame.
+    iAssert (∃ q' n, st ≡ Some (ν, false, q', n) ∗ ⌜q ≤ q'⌝%Qc)%I with
+       "[#]" as (q' n) "[%%]".
+    { destruct st as [[[[??]?]?]|];
+      iDestruct (own_valid_2 with "H● H◯")
+        as %[[[=]|(?&[[? q'] n]&[=<-]&[=]&[[[Eq_ag ?%leibniz_equiv]_]|Hle])]
+               %option_included Hv]%auth_valid_discrete_2; simpl in *; subst.
+      - apply (inj to_agree), (inj2 pair) in Eq_ag.
+        destruct Eq_ag. setoid_subst. eauto.
+      - revert Hle=> /prod_included [/= /prod_included
+                  [/= /to_agree_included [/= ??] /frac_included_weak ?] _].
+        setoid_subst. eauto. }
+    setoid_subst. iExists q', n. rewrite own_op. by iFrame.
   Qed.
 
   (* Cloning a ref. We need to increment the counter. *)
@@ -51,11 +44,9 @@ Section ref_functions.
       letalloc: "r" <-{2} !"x'" in
       delete [ #1; "x"];; return: ["r"].
 
-  (* FIXME : using λ instead of fun triggers an anomaly.
-     See: https://coq.inria.fr/bugs/show_bug.cgi?id=5326 *)
   Lemma ref_clone_type ty `{!TyWf ty} :
-    typed_val ref_clone (fn (fun '(α, β) =>
-                FP_wf ∅ [# &shr{α}(ref β ty)]%T (ref β ty)%T)).
+    typed_val ref_clone (fn(∀ '(α, β), ∅; &shr{α}(ref β ty)) → ref β ty).
+
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -75,12 +66,12 @@ Section ref_functions.
     rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
     iMod "H↦" as "[H↦1 H↦2]". wp_read. wp_let.
     iDestruct (refcell_inv_reading_inv with "INV H◯")
-      as (q' n) "(H↦lrc & _ & [H● H◯] & Hshr' & H† & Hq')".
+      as (q' n) "(H↦lrc & _ & [H● H◯] & H† & Hq' & Hshr')".
     wp_read. wp_let. wp_op. wp_write. iDestruct "Hq'" as (q'') "(Hq'q'' & Hν1 & Hν2)".
     iDestruct "Hq'q''" as %Hq'q''. iMod (own_update with "H●") as "[H● ?]".
     { apply auth_update_alloc,
-         (op_local_update_discrete _ _ (reading_st (q''/2)%Qp ν))=>-[Hagv _].
-      split; [|split; last done].
+         (op_local_update_discrete _ _ (reading_stR (q''/2)%Qp ν))=>-[Hagv _].
+      split; [split|done].
       - by rewrite /= agree_idemp.
       - apply frac_valid'. rewrite -Hq'q'' comm -{2}(Qp_div_2 q'').
         apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q''/2)%Qp).
@@ -91,9 +82,8 @@ Section ref_functions.
     wp_let. wp_apply (wp_memcpy with "[$Hlr $H↦]"); [done..|].
     iIntros "[Hlr H↦]". wp_seq. iMod ("Hcloseα2" with "[$H◯] Hna") as "[Hα1 Hna]".
     iMod ("Hcloseδ" with "[H↦lrc H● Hν1 Hshr' H†] Hna") as "[Hδ Hna]".
-    { iExists _. rewrite Z.add_comm. iFrame. iExists _. iFrame. iSplitR.
-      - rewrite /= agree_idemp. auto.
-      - iExists _. iFrame.
+    { iExists (Some (_, false, _, _)). rewrite Z.add_comm -Some_op !pair_op agree_idemp.
+      iFrame. iExists _. iFrame.
       rewrite (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto. }
     iMod ("Hcloseβ" with "Hδ") as "Hβ". iMod ("Hcloseα1" with "[$H↦]") as "Hα2".
     iMod ("Hclose'" with "[$Hα1 $Hα2] HL") as "HL". iMod ("Hclose" with "Hβ HL") as "HL".
@@ -117,7 +107,7 @@ Section ref_functions.
 
   Lemma ref_deref_type ty `{!TyWf ty} :
     typed_val ref_deref
-      (fn (fun '(α, β) => FP_wf ∅ [# &shr{α}(ref β ty)]%T (&shr{α}ty)%T)).
+      (fn(∀ '(α, β), ∅; &shr{α}(ref β ty)) → &shr{α}ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -167,27 +157,27 @@ Section ref_functions.
     iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
     iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hcloseβ)"; [done..|].
     iDestruct (refcell_inv_reading_inv with "INV [$H◯]")
-      as (q' n) "(H↦lrc & >% & H●◯ & Hshr & H† & Hq')". iDestruct "Hq'" as (q'') ">[% Hν']".
+      as (q' n) "(H↦lrc & >% & H●◯ & H† & Hq' & Hshr)".
+    iDestruct "Hq'" as (q'') ">[% Hν']".
     wp_read. wp_let. wp_op. wp_write.
     iAssert (|={↑lftN ∪ ↑histN,↑histN}▷=> refcell_inv tid lrc γ β ty')%I
       with "[H↦lrc H●◯ Hν Hν' Hshr H†]" as "INV".
-    { iDestruct (own_valid with "H●◯") as %[[ _ [Heq%(inj Cinr)|Hincl%csum_included]
-        %Some_included]%Some_pair_included [_ Hv]]%auth_valid_discrete_2.
-      - destruct Heq as [?%leibniz_equiv ?%leibniz_equiv]. simpl in *. subst.
+    { iDestruct (own_valid with "H●◯") as
+          %[[[[_ ?]?]|[[_ [q0 Hq0]]%prod_included [n' Hn']]%prod_included]
+              %Some_included _]%auth_valid_discrete_2.
+      - simpl in *. setoid_subst.
         iExists None. iFrame. iMod (own_update with "H●◯") as "$".
         { apply auth_update_dealloc. rewrite -(right_id None op (Some _)).
           apply cancel_local_update_unit, _. }
         iApply "H†". replace 1%Qp with (q'+q'')%Qp by naive_solver. iFrame.
-      - destruct Hincl as [ [=] |[ (?&?&[=]&?) | (?&?&[=<-]&[=<-]&[[q0 n']EQ]) ]].
-        destruct EQ as [?%leibniz_equiv ?%leibniz_equiv]. simpl in *. subst.
-        iAssert (lrc ↦ #(Z.pos n'))%I with "[H↦lrc]" as "H↦lrc".
+      - simpl in *. setoid_subst. iExists (Some (ν, false, q0, n')). iFrame.
+        iAssert (lrc ↦ #(Z.pos n'))%I with "[H↦lrc]" as "$".
         { destruct n'; [|done..]. by rewrite /= Pos.pred_double_succ. }
-        iExists (Some (_, Cinr (q0, n'))). iFrame. iMod (own_update with "H●◯") as "$".
+        iMod (own_update with "H●◯") as "$".
         { apply auth_update_dealloc.
-          rewrite -(agree_idemp (to_agree _)) -pair_op -Cinr_op -pair_op Some_op.
-          apply (cancel_local_update_unit (reading_st q ν)), _. }
-        iExists ν. iFrame. iApply step_fupd_intro; first set_solver. iIntros "!>".
-        iSplitR; first done. iExists (q+q'')%Qp. iFrame.
+          rewrite -(agree_idemp (to_agree _)) -!pair_op Some_op.
+          apply (cancel_local_update_unit (reading_stR q ν)), _. }
+        iApply step_fupd_intro; first set_solver. iExists (q+q'')%Qp. iFrame.
         by rewrite assoc (comm _ q0 q). }
     wp_bind Endlft. iApply (wp_mask_mono _ (↑lftN ∪ ↑histN)); first done.
     iApply (wp_step_fupd with "INV"); [set_solver..|]. wp_seq.
@@ -259,4 +249,115 @@ Section ref_functions.
       iFrame. destruct r' as [[]|]=>//=. auto 10 with iFrame. }
     iApply type_jump; solve_typing.
   Qed.
+
+  (* Apply a function within the ref, and create two ref,
+     typically for splitting the reference. *)
+  Definition ref_map_split (call_once : val) : val :=
+    funrec: <> ["ref"; "f"] :=
+      let: "call_once" := call_once in
+      let: "x'" := !"ref" in
+
+      letalloc: "x" <- "x'" in
+      letcall: "r" := "call_once" ["f"; "x"]%E in
+      let: "a" := !"r" in
+      let: "b" := !("r" +ₗ #1) in
+      delete [ #2; "r"];;
+
+      let: "rc" := !("ref" +ₗ #1) in
+      let: "n" := !"rc" in
+      "rc" <- "n" + #1;;
+
+      delete [ #2; "ref"];;
+
+      let: "refs" := new [ #4 ] in
+      "refs" <- "a";;
+      "refs" +ₗ #1 <- "rc";;
+      "refs" +ₗ #2 <- "b";;
+      "refs" +ₗ #3 <- "rc";;
+
+      return: ["refs"].
+
+  Lemma ref_map_split_type ty ty1 ty2 call_once fty
+        `{!TyWf ty, !TyWf ty1, !TyWf ty2, !TyWf fty} :
+    (* fty : for<'a>, FnOnce(&'a ty) -> (&'a ty1, &'a ty2),
+       as witnessed by the impl call_once *)
+    typed_val call_once
+              (fn(∀ α, ∅; fty, &shr{α}ty) → Π[&shr{α}ty1; &shr{α}ty2]) →
+    typed_val (ref_map_split call_once)
+              (fn(∀ α, ∅; ref α ty, fty) → Π[ref α ty1; ref α ty2]).
+  Proof.
+    intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
+       inv_vec arg=>ref env. simpl_subst.
+    iApply type_let; [apply Hf | solve_typing |]. iIntros (f'). simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk (#Hf' & Href & Henv & _)".
+    rewrite (tctx_hasty_val _ ref). destruct ref as [[|lref|]|]; try done.
+    iDestruct "Href" as "[Href Href†]".
+    iDestruct "Href" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Href";
+      try iDestruct "Href" as "[_ >[]]".
+    rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+    iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
+    iDestruct "Href" as (ν qν γ β ty') "(#Hshr & #Hαβ & #Hinv & >Hν & Hγ)".
+    wp_read. wp_let. wp_apply wp_new; [done..|].
+    iIntros (lx) "(H† & Hlx)". rewrite heap_mapsto_vec_singleton.
+    wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
+    iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
+    iMod (lctx_lft_alive_tok ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
+    iDestruct (lft_intersect_acc with "Hα Hν") as (?) "[Hαν Hclose3]".
+    iDestruct (lft_intersect_acc with "Hαν Hϝ") as (?) "[Hανϝ Hclose4]".
+    rewrite -[ϝ in (α ⊓ ν) ⊓ ϝ](right_id_L static (⊓)).
+    iApply (type_call_iris _ [α ⊓ ν; ϝ] (α ⊓ ν) [_; _]
+       with "LFT HE Hna [Hανϝ] Hf' [$Henv Hlx H†]"); [solve_typing|done| |].
+    { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
+      iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. by iFrame. }
+    iIntros ([[|r|]|]) "Hna Hανϝ Hr //".
+    iDestruct ("Hclose4" with "Hανϝ") as "[Hαν Hϝ]".
+    iDestruct ("Hclose3" with "Hαν") as "[Hα Hν]".
+    iMod ("Hclose2" with "Hϝ HL") as "HL".
+    wp_rec. iDestruct "Hr" as "[Hr Hr†]".
+    iDestruct "Hr" as (?) "[Hr H]". iDestruct "H" as (vl1 ? ->) "[#Hr1' H]".
+    iDestruct "H" as (vl2 ? ->) "[#Hr2' ->]".
+    destruct vl1 as [|[[|lr1|]|] []], vl2 as [|[[|lr2|]|] []]=>//=.
+    rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+    iDestruct "Hr" as "[Hr1 Hr2]". wp_read. wp_let. wp_op. wp_read. wp_let.
+    wp_apply (wp_delete _ _ _ _ [_; _] with "[Hr1 Hr2 Hr†]")=>//.
+    { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton /= freeable_sz_full.
+      iFrame. }
+    iIntros "_".
+    iMod (lft_incl_acc  with "Hαβ Hα") as (?) "[Hβ Hβclose]". done.
+    iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hclosena)"; [done..|].
+    wp_seq. wp_op. wp_read.
+    iDestruct (refcell_inv_reading_inv with "INV Hγ")
+      as (q' n) "(H↦lrc & _ & [H● H◯] & H† & Hq' & Hshr')".
+    iDestruct "Hq'" as (q'') "(Hq'q'' & Hν1 & Hν2)".
+    iDestruct "Hq'q''" as %Hq'q''. iMod (own_update with "H●") as "[H● ?]".
+    { apply auth_update_alloc,
+         (op_local_update_discrete _ _ (reading_stR (q''/2)%Qp ν))=>-[Hagv _].
+      split; [split|done].
+      - by rewrite /= agree_idemp.
+      - apply frac_valid'. rewrite -Hq'q'' comm -{2}(Qp_div_2 q'').
+        apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q''/2)%Qp).
+        apply Qcplus_le_mono_r, Qp_ge_0. }
+    wp_let. wp_read. wp_let. wp_op. wp_write.
+    wp_apply (wp_delete _ _ _ _ [_; _] with "[Href↦1 Href↦2 Href†]")=>//.
+    { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton /= freeable_sz_full.
+      iFrame. }
+    iIntros "_". wp_seq. wp_apply wp_new; [done..|]. iIntros (lrefs) "[Hrefs† Hrefs]".
+    rewrite 3!heap_mapsto_vec_cons heap_mapsto_vec_singleton. wp_let.
+    iDestruct "Hrefs" as "(Hrefs1 & Hrefs2 & Hrefs3 & Hrefs4)".
+    rewrite !shift_loc_assoc. wp_write. do 3 (wp_op; wp_write).
+    iMod ("Hclosena" with "[H↦lrc H● Hν1 Hshr' H†] Hna") as "[Hβ Hna]".
+    { iExists (Some (_, false, _, _)). rewrite Z.add_comm -Some_op !pair_op agree_idemp.
+      iFrame. iExists _. iFrame.
+      rewrite (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto. }
+    iMod ("Hβclose" with "Hβ") as "Hα". iMod ("Hclose1" with "Hα HL") as "HL".
+    iApply (type_type _ [_] _ [ #lrefs ◁ box (Π[ref α ty1; ref α ty2]) ]
+       with "[] LFT HE Hna HL Hk"); first last.
+    { rewrite tctx_interp_singleton tctx_hasty_val' //= -freeable_sz_full.
+      iFrame. iExists [_;_;_;_].
+      rewrite 3!heap_mapsto_vec_cons heap_mapsto_vec_singleton !shift_loc_assoc.
+      iFrame. iExists [_;_], [_;_]. iSplit=>//=.
+      iSplitL "Hν H◯"; [by auto 10 with iFrame|]. iExists [_;_], [].
+      iSplitR=>//=. rewrite right_id. auto 20 with iFrame. }
+    iApply type_jump; solve_typing.
+  Qed.
 End ref_functions.