theories/lifetime/raw_reborrow.v → lifetime/model/reborrow.v

-From lrust.lifetime Require Export primitive.
-From lrust.lifetime Require Import faking.
-From iris.algebra Require Import csum auth frac gmap dec_agree gset.
-From iris.base_logic Require Import big_op.
+From lrust.lifetime Require Import borrow accessors.
+From iris.algebra Require Import csum auth frac gmap agree gset numbers.
 From iris.base_logic.lib Require Import boxes.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
+From iris.prelude Require Import options.
 
-Section rebor.
-Context `{invG Σ, lftG Σ}.
+Section reborrow.
+Context `{!invGS Σ, !lftGS Σ userE}.
 Implicit Types κ : lft.
 
 (* Notice that taking lft_inv for both κ and κ' already implies
    κ ≠ κ'.  Still, it is probably more instructing to require
    κ ⊂ κ' in this lemma (as opposed to just κ ⊆ κ'), and it
    should not increase the burden on the user. *)
-Lemma raw_bor_unnest E q A I Pb Pi P κ i κ' :
+Lemma raw_bor_unnest E A I Pb Pi P κ i κ' :
   ↑borN ⊆ E →
-  let Iinv := (own_ilft_auth I ∗ ▷?q lft_inv A κ)%I in
+  let Iinv := (own_ilft_auth I ∗ ▷ lft_inv A κ)%I in
   κ ⊂ κ' →
   lft_alive_in A κ' →
-  Iinv -∗ idx_bor_own 1 (κ, i) -∗ slice borN i P -∗ ▷?q lft_bor_alive κ' Pb -∗
-  ▷?q lft_vs κ' (idx_bor_own 1 (κ, i) ∗ Pb) Pi ={E}=∗ ∃ Pb',
-    Iinv ∗ raw_bor κ' P ∗ ▷?q lft_bor_alive κ' Pb' ∗ ▷?q lft_vs κ' Pb' Pi.
+  Iinv -∗ idx_bor_own 1 (κ, i) -∗ slice borN i P -∗ ▷ lft_bor_alive κ' Pb -∗
+  ▷ lft_vs κ' (idx_bor_own 1 (κ, i) ∗ Pb) Pi ={E}=∗ ∃ Pb',
+    Iinv ∗ raw_bor κ' P ∗ ▷ lft_bor_alive κ' Pb' ∗ ▷ lft_vs κ' Pb' Pi.
 Proof.
   iIntros (? Iinv Hκκ' Haliveκ') "(HI & Hκ) Hi #Hislice Hκalive' Hvs".
   rewrite lft_vs_unfold. iDestruct "Hvs" as (n) "[>Hn● Hvs]".
   iMod (own_cnt_update with "Hn●") as "[Hn● H◯]".
-  { apply auth_update_alloc, (nat_local_update _ 0 (S n) 1); omega. }
+  { apply auth_update_alloc, (nat_local_update _ 0 (S n) 1); lia. }
   rewrite {1}/raw_bor /idx_bor_own /=.
   iDestruct (own_bor_auth with "HI Hi") as %?.
   assert (κ ⊆ κ') by (by apply strict_include).
@@ -35,14 +34,14 @@ Proof.
     iDestruct "Hκ" as (Pb' Pi') "(Hκalive&Hvs'&Hinh')".
   rewrite {2}/lft_bor_alive; iDestruct "Hκalive" as (B) "(Hbox & >HB● & HB)".
   iDestruct (own_bor_valid_2 with "HB● Hi")
-    as %[HB%to_borUR_included _]%auth_valid_discrete_2.
-  iMod (slice_empty with "Hislice Hbox") as "[HP Hbox]"; first done.
+    as %[HB%to_borUR_included _]%auth_both_valid_discrete.
+  iMod (slice_empty _ _ true with "Hislice Hbox") as "[HP Hbox]"; first done.
   { by rewrite lookup_fmap HB. }
   iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
-  { eapply auth_update, singleton_local_update,
-     (exclusive_local_update _ (1%Qp, DecAgree (Bor_rebor κ'))); last done.
+  { eapply auth_update, singleton_local_update; last eapply
+     (exclusive_local_update _ (1%Qp, to_agree (Bor_rebor κ'))); last done.
     rewrite /to_borUR lookup_fmap. by rewrite HB. }
-  iAssert (▷?q lft_inv A κ)%I with "[H◯ HB● HB Hvs' Hinh' Hbox]" as "Hκ".
+  iAssert (▷ lft_inv A κ)%I with "[H◯ HB● HB Hvs' Hinh' Hbox]" as "Hκ".
   { iNext. rewrite /lft_inv. iLeft.
     iSplit; last by eauto using lft_alive_in_subseteq.
     rewrite lft_inv_alive_unfold. iExists Pb', Pi'. iFrame "Hvs' Hinh'".
@@ -50,19 +49,18 @@ Proof.
     rewrite /to_borUR !fmap_insert. iFrame "Hbox HB●".
     iDestruct (@big_sepM_delete with "HB") as "[_ HB]"; first done.
     rewrite (big_sepM_delete _ (<[_:=_]>_) i); last by rewrite lookup_insert.
-    rewrite -insert_delete delete_insert ?lookup_delete //=. iFrame; auto. }
+    rewrite -insert_delete_insert delete_insert ?lookup_delete //=. iFrame; auto. }
   clear B HB Pb' Pi'.
   rewrite {1}/lft_bor_alive. iDestruct "Hκalive'" as (B) "(Hbox & >HB● & HB)".
-  iMod (slice_insert_full with "HP Hbox")
+  iMod (slice_insert_full _ _ true with "HP Hbox")
     as (j) "(HBj & #Hjslice & Hbox)"; first done.
   iDestruct "HBj" as %HBj; move: HBj; rewrite lookup_fmap fmap_None=> HBj.
   iMod (own_bor_update with "HB●") as "[HB● Hj]".
   { apply auth_update_alloc,
-     (alloc_singleton_local_update _ j (1%Qp, DecAgree Bor_in)); last done.
+     (alloc_singleton_local_update _ j (1%Qp, to_agree Bor_in)); last done.
     rewrite /to_borUR lookup_fmap. by rewrite HBj. }
-  iModIntro. iExists (P ∗ Pb)%I. rewrite /Iinv. iFrame "HI". iFrame.
-  iSplitL "Hj".
-  { rewrite /raw_bor /idx_bor_own. iExists j. by iFrame. }
+  iModIntro. iExists (P ∗ Pb)%I. rewrite /Iinv. iFrame "HI Hκ". iSplitL "Hj".
+  { iExists j. iFrame. iExists P. rewrite -(bi.iff_refl emp). auto. }
   iSplitL "Hbox HB● HB".
   { rewrite /lft_bor_alive. iNext. iExists (<[j:=Bor_in]> B).
     rewrite /to_borUR !fmap_insert big_sepM_insert //. iFrame.
@@ -70,124 +68,117 @@ Proof.
   clear dependent Iinv I.
   iNext. rewrite lft_vs_unfold. iExists (S n). iFrame "Hn●".
   iIntros (I) "Hinv [HP HPb] #Hκ†".
-  rewrite {1}lft_vs_inv_unfold; iDestruct "Hinv" as "(Hκdead' & HI & Hinv)".
-  iDestruct (own_bor_auth with "HI Hi") as %?%elem_of_dom.
+  rewrite {1}lft_vs_inv_unfold; iDestruct "Hinv" as "(HI & Hinv)".
+  iDestruct (own_bor_auth with "HI Hi") as %?%(elem_of_dom (D:=gset lft)).
   iDestruct (@big_sepS_delete with "Hinv") as "[Hκalive Hinv]"; first done.
   rewrite lft_inv_alive_unfold.
-  iDestruct ("Hκalive" with "[%]") as (Pb' Pi') "(Hκalive&Hvs'&Hinh)"; first done.
+  iDestruct ("Hκalive" with "[//]") as (Pb' Pi') "(Hκalive&Hvs'&Hinh)".
   rewrite /lft_bor_alive; iDestruct "Hκalive" as (B') "(Hbox & HB● & HB)".
-  iDestruct (own_bor_valid_2 with "HB● Hi") 
-    as %[HB%to_borUR_included _]%auth_valid_discrete_2.
+  iDestruct (own_bor_valid_2 with "HB● Hi")
+    as %[HB%to_borUR_included _]%auth_both_valid_discrete.
   iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
   { eapply auth_update, singleton_local_update,
-     (exclusive_local_update _ (1%Qp, DecAgree Bor_in)); last done.
+     (exclusive_local_update _ (1%Qp, to_agree Bor_in)); last done.
     rewrite /to_borUR lookup_fmap. by rewrite HB. }
   iMod (slice_fill _ _ false with "Hislice HP Hbox")
-     as "Hbox"; first by solve_ndisj.
+     as "Hbox".
+  { set_solver+. }
   { by rewrite lookup_fmap HB. }
   iDestruct (@big_sepM_delete with "HB") as "[Hcnt HB]"; first done.
-  rewrite /=; iDestruct "Hcnt" as "[% H1◯]".
-  iMod ("Hvs" $! I with "[Hκdead' HI Hinv Hvs' Hinh HB● Hbox HB]
-                         [$HPb Hi] Hκ†") as "($ & $ & Hcnt')".
-  { rewrite lft_vs_inv_unfold. iFrame "Hκdead' HI".
-    iApply (big_sepS_delete _ (dom (gset lft) I) with "[- $Hinv]"); first done.
+  rewrite /=. iDestruct "Hcnt" as "[% H1◯]".
+  iMod ("Hvs" $! I with "[HI Hinv Hvs' Hinh HB● Hbox HB]
+                         [$HPb $Hi] Hκ†") as "($ & $ & Hcnt')".
+  { rewrite lft_vs_inv_unfold. iFrame "HI".
+    iApply (big_sepS_delete _ (dom I) with "[- $Hinv]"); first done.
     iIntros (_). rewrite lft_inv_alive_unfold.
     iExists Pb', Pi'. iFrame "Hvs' Hinh". rewrite /lft_bor_alive.
     iExists (<[i:=Bor_in]>B'). rewrite /to_borUR !fmap_insert. iFrame.
-    rewrite -insert_delete big_sepM_insert ?lookup_delete //=. by iFrame. }
-  { rewrite /raw_bor /idx_bor_own /=. auto. }
-  iModIntro. rewrite -[S n]Nat.add_1_l -nat_op_plus auth_frag_op own_cnt_op.
+    rewrite -insert_delete_insert big_sepM_insert ?lookup_delete //=. by iFrame. }
+  iModIntro. rewrite -[S n]Nat.add_1_l -nat_op auth_frag_op own_cnt_op.
   by iFrame.
 Qed.
 
-Lemma raw_bor_unnest' E q A I Pb Pi P κ κ' :
-  ↑borN ⊆ E →
-  let Iinv := (
-    own_ilft_auth I ∗
-    ▷?q [∗ set] κ ∈ dom _ I ∖ {[κ']}, lft_inv A κ)%I in
-  κ ⊆ κ' →
-  lft_alive_in A κ' →
-  Iinv -∗ raw_bor κ P -∗ ▷?q lft_bor_alive κ' Pb -∗
-  ▷?q lft_vs κ' (raw_bor κ P ∗ Pb) Pi ={E}=∗ ∃ Pb',
-    Iinv ∗ raw_bor κ' P ∗ ▷?q lft_bor_alive κ' Pb' ∗ ▷?q lft_vs κ' Pb' Pi.
+Lemma raw_idx_bor_unnest E κ κ' i P :
+  ↑lftN ⊆ E → κ ⊂ κ' →
+  lft_ctx -∗ slice borN i P -∗ raw_bor κ' (idx_bor_own 1 (κ, i))
+  ={E}=∗ raw_bor κ' P.
 Proof.
-  iIntros (? Iinv Hκκ' Haliveκ') "(HI & Hinv) Hraw Hκalive' Hvs".
-  destruct (decide (κ = κ')) as [<-|Hκneq].
-  { iModIntro. iExists Pb. rewrite /Iinv. iFrame "HI Hinv Hκalive' Hraw".
-    iApply (lft_vs_cons with "[]"); last done.
-    iIntros "(Hdead & HPb)".
-    iMod (raw_bor_fake _ false _ P with "Hdead") as "[Hdead Hraw]"; first solve_ndisj.
-    by iFrame. }
-  assert (κ ⊂ κ') by (by apply strict_spec_alt).
-  iDestruct (raw_bor_inI with "HI Hraw") as %HI.
-  iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinv Hclose]".
-  { rewrite elem_of_difference elem_of_dom not_elem_of_singleton. done. }
-  rewrite {1}/raw_bor. iDestruct "Hraw" as (i) "[Hi #Hislice]".
-  iMod (raw_bor_unnest with "[$HI $Hinv] Hi Hislice Hκalive' [Hvs]") as (Pb') "([HI Hκ] & ? & ? & ?)"; [done..| |].
-  { iApply (lft_vs_cons with "[]"); last done.
-    iIntros "[$ [>? $]]". iModIntro. iNext. rewrite /raw_bor.
-    iExists i. by iFrame. }
-  iExists Pb'. iModIntro. iFrame. iNext. by iApply "Hclose".
+  iIntros (? Hκκ') "#LFT #Hs Hraw".
+  iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
+  iDestruct (raw_bor_inI with "HI Hraw") as %HI'.
+  rewrite (big_sepS_delete _ _ κ') ?elem_of_dom // [_ A κ']/lft_inv.
+  iDestruct "Hinv" as "[[[Hinvκ >%]|[Hinvκ >%]] Hinv]"; last first.
+  { rewrite /lft_inv_dead. iDestruct "Hinvκ" as (Pi) "[Hbordead H]".
+    iMod (raw_bor_fake with "Hbordead") as "[Hbordead $]"; first solve_ndisj.
+    iApply "Hclose". iExists _, _. iFrame.
+    rewrite (big_opS_delete _ (dom _) κ') ?elem_of_dom // /lft_inv /lft_inv_dead.
+    auto 10 with iFrame. }
+  rewrite {1}/raw_bor. iDestruct "Hraw" as (i') "[Hbor H]".
+  iDestruct "H" as (P') "[#HP' #Hs']".
+  rewrite lft_inv_alive_unfold /lft_bor_alive [in _ _ (κ', i')]/idx_bor_own.
+  iDestruct "Hinvκ" as (Pb Pi) "(Halive & Hvs & Hinh)".
+  iDestruct "Halive" as (B) "(Hbox & >H● & HB)".
+  iDestruct (own_bor_valid_2 with "H● Hbor")
+    as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
+  iMod (slice_empty _ _ true with "Hs' Hbox") as "[Hidx Hbox]";
+    first solve_ndisj.
+  { by rewrite lookup_fmap EQB. }
+  iAssert (▷ idx_bor_own 1 (κ, i))%I with "[Hidx]" as ">Hidx"; [by iApply "HP'"|].
+  iDestruct (own_bor_auth with "HI [Hidx]") as %HI; [by rewrite /idx_bor_own|].
+  iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinvκ Hclose']";
+    first by rewrite elem_of_difference elem_of_dom not_elem_of_singleton;
+    eauto using strict_ne.
+  iMod (slice_delete_empty with "Hs' Hbox") as (Pb') "[#HeqPb' Hbox]";
+    [solve_ndisj|by apply lookup_insert|].
+  iMod (own_bor_update_2 with "H● Hbor") as "H●".
+  { apply auth_update_dealloc, delete_singleton_local_update. apply _. }
+  iMod (raw_bor_unnest with "[$HI $Hinvκ] Hidx Hs [Hbox H● HB] [Hvs]")
+    as (Pb'') "HH"; [solve_ndisj|done|done| | |].
+  { rewrite /lft_bor_alive (big_sepM_delete _ B i') //. iDestruct "HB" as "[_ HB]".
+    iExists (delete i' B). rewrite -fmap_delete. iFrame.
+    rewrite fmap_delete -insert_delete_insert delete_insert ?lookup_delete //=. }
+  { iNext. iApply (lft_vs_cons with "[] Hvs"). iIntros "[??] _ !>". iNext.
+    iRewrite "HeqPb'". iFrame. by iApply "HP'". }
+  iDestruct "HH" as "([HI Hinvκ] & $ & Halive & Hvs)".
+  iApply "Hclose". iExists _, _. iFrame.
+  rewrite (big_opS_delete _ (dom _) κ') ?elem_of_dom //.
+  iDestruct ("Hclose'" with "Hinvκ") as "$".
+  rewrite /lft_inv lft_inv_alive_unfold. auto 10 with iFrame.
 Qed.
 
-Lemma raw_rebor E κ κ' P :
+Lemma raw_bor_shorten E κ κ' P :
   ↑lftN ⊆ E → κ ⊆ κ' →
-  lft_ctx -∗ raw_bor κ P ={E}=∗
-    raw_bor κ' P ∗ ([†κ'] ={E}=∗ raw_bor κ P).
+  lft_ctx -∗ raw_bor κ P ={E}=∗ raw_bor κ' P.
 Proof.
-  rewrite /lft_ctx. iIntros (??) "#LFT Hκ".
-  destruct (decide (κ = κ')) as [<-|Hκneq].
-  { iFrame. iIntros "!> #Hκ†". by iApply (raw_bor_fake' with "LFT Hκ†"). }
+  iIntros (? Hκκ') "#LFT Hbor".
+  destruct (decide (κ = κ')) as [<-|Hκneq]; [by iFrame|].
   assert (κ ⊂ κ') by (by apply strict_spec_alt).
-  iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  iMod (ilft_create _ _ κ' with "HA HI Hinv") as (A' I') "(% & HA & HI & Hinv)".
-  clear A I; rename A' into A; rename I' into I.
-  iDestruct (big_sepS_delete _ _ κ' with "Hinv") as "[Hκinv' Hinv]";
-    first by apply elem_of_dom.
-  rewrite {1}/lft_inv; iDestruct "Hκinv'" as "[[? >%]|[Hdead >%]]"; last first.
-  { rewrite /lft_inv_dead; iDestruct "Hdead" as (Pi) "(Hdead & >H● & Hinh)".
-    iMod (raw_bor_fake _ true _ P with "Hdead") as "[Hdead $]"; first solve_ndisj.
-    iMod ("Hclose" with "[-Hκ]") as "_"; last auto.
-    iNext. rewrite {2}/lfts_inv. iExists A, I. iFrame "HA HI".
-    iApply (big_sepS_delete _ _ κ'); first by apply elem_of_dom.
-    iFrame "Hinv". rewrite /lft_inv /lft_inv_dead. iRight.
-    iSplit; last done. iExists Pi. by iFrame. }
-  rewrite lft_inv_alive_unfold; iDestruct "Hκinv'" as (Pb Pi) "(Hbor & Hvs & Hinh)".
-  rewrite {1}/raw_bor. iDestruct "Hκ" as (i) "[Hi #Hislice]".
-  iMod (lft_inh_extend _ _ (idx_bor_own 1 (κ, i)) with "Hinh")
-    as "(Hinh & HIlookup & Hinh_close)"; first solve_ndisj.
-  iDestruct (own_bor_auth with "HI [Hi]") as %?.
-  { by rewrite /idx_bor_own. }
-  iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hκ Hκclose]".
-  { by rewrite elem_of_difference elem_of_dom not_elem_of_singleton. }
-  iMod (raw_bor_unnest _ true _ _ _ (idx_bor_own 1 (κ, i) ∗ Pi)%I
-    with "[$HI $Hκ] Hi Hislice Hbor [Hvs]")
-    as (Pb') "([HI Hκ] & $ & Halive & Hvs)"; [solve_ndisj|done|done|..].
-  { iNext. by iApply lft_vs_frame. }
-  iDestruct ("Hκclose" with "Hκ") as "Hinv".
-  iMod ("Hclose" with "[HA HI Hinv Halive Hinh Hvs]") as "_".
-  { iNext. rewrite {2}/lfts_inv. iExists A, I. iFrame "HA HI".
-    iApply (big_sepS_delete _ _ κ'); first by apply elem_of_dom. iFrame "Hinv".
-    rewrite /lft_inv. iLeft. iSplit; last done.
-    rewrite lft_inv_alive_unfold. iExists Pb', (idx_bor_own 1 (κ, i) ∗ Pi)%I.
-    iFrame. }
-  clear dependent A I Pb Pb' Pi. iModIntro. iIntros "H†".
-  iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  iDestruct ("HIlookup" with "* HI") as %Hκ'.
-  iDestruct (big_sepS_delete _ _ κ' with "Hinv") as "[Hκinv' Hinv]";
-    first by apply elem_of_dom.
-  rewrite {1}/lft_inv; iDestruct "Hκinv'" as "[[Halive >%]|[Hdead >%]]".
-  - (* the same proof is in bor_fake and bor_create *)
-    rewrite /lft_dead; iDestruct "H†" as (Λ) "[% #H†]".
-    iDestruct (own_alft_auth_agree A Λ false with "HA H†") as %EQAΛ.
-    unfold lft_alive_in in *. naive_solver.
-  - rewrite /lft_inv_dead; iDestruct "Hdead" as (Pi) "(Hdead & Hcnt & Hinh)".
-    iMod ("Hinh_close" $! Pi with "Hinh") as (Pi') "(Heq & >Hbor & Hinh)".
-    iMod ("Hclose" with "[HA HI Hinv Hdead Hinh Hcnt]") as "_".
-    { iNext. rewrite /lfts_inv. iExists A, I. iFrame "HA HI".
-      iApply (big_sepS_delete _ _ κ'); first by apply elem_of_dom. iFrame "Hinv".
-      rewrite /lft_inv /lft_inv_dead. iRight. iSplit; last done.
-      iExists Pi'. iFrame. }
-    iModIntro. rewrite /raw_bor. iExists i. by iFrame.
+  rewrite [_ κ P]/raw_bor. iDestruct "Hbor" as (s) "[Hbor Hs]".
+  iDestruct "Hs" as (P') "[#HP'P #Hs]".
+  iMod (raw_bor_create _ κ' with "LFT Hbor") as "[Hbor _]"; [done|].
+  iApply (raw_bor_iff with "HP'P"). by iApply raw_idx_bor_unnest.
+Qed.
+
+Lemma idx_bor_unnest E κ κ' i P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{κ,i} P -∗ &{κ'}(idx_bor_own 1 i) ={E}=∗ &{κ ⊓ κ'} P.
+Proof.
+  iIntros (?) "#LFT #HP Hbor".
+  rewrite [(&{κ'}_)%I]/bor. iDestruct "Hbor" as (κ'0) "[#Hκ'κ'0 Hbor]".
+  destruct (decide (κ'0 = static)) as [->|Hκ'0].
+  { iMod (bor_acc_strong with "LFT [Hbor] []") as (?) "(_ & Hbor & _)";
+      [done| |iApply (lft_tok_static 1)|].
+    - rewrite /bor. iExists static. iFrame. iApply lft_incl_refl.
+    - iDestruct "Hbor" as ">Hbor".
+      iApply bor_shorten; [|by rewrite bor_unfold_idx; auto].
+      iApply lft_intersect_incl_l. }
+  rewrite /idx_bor /bor. destruct i as [κ0 i].
+  iDestruct "HP" as "[Hκκ0 HP]". iDestruct "HP" as (P') "[HPP' HP']".
+  iMod (raw_bor_shorten _ _ (κ0 ⊓ κ'0) with "LFT Hbor") as "Hbor";
+    [done|by apply gmultiset_disj_union_subseteq_r|].
+  iMod (raw_idx_bor_unnest with "LFT HP' Hbor") as "Hbor";
+    [done|by apply gmultiset_disj_union_subset_l|].
+  iExists _. iDestruct (raw_bor_iff with "HPP' Hbor") as "$".
+    by iApply lft_intersect_mono.
 Qed.
-End rebor.
+End reborrow.

theories/lifetime/na_borrow.v → lifetime/na_borrow.v

-From lrust.lifetime Require Export derived.
+From lrust.lifetime Require Export lifetime.
 From iris.base_logic.lib Require Export na_invariants.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
+From iris.prelude Require Import options.
 
-Definition na_bor `{invG Σ, lftG Σ, na_invG Σ}
+Definition na_bor `{!invGS Σ, !lftGS Σ userE, !na_invG Σ}
            (κ : lft) (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ) :=
   (∃ i, &{κ,i}P ∗ na_inv tid N (idx_bor_own 1 i))%I.
 
-Notation "&na{ κ , tid , N } P" := (na_bor κ tid N P)
-  (format "&na{ κ , tid , N } P", at level 20, right associativity) : uPred_scope.
+Notation "&na{ κ , tid , N }" := (na_bor κ tid N)
+    (format "&na{ κ , tid , N }") : bi_scope.
 
 Section na_bor.
-  Context `{invG Σ, lftG Σ, na_invG Σ}
+  Context `{!invGS Σ, !lftGS Σ userE, !na_invG Σ}
           (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ).
 
-  Global Instance na_bor_persistent κ : PersistentP (&na{κ,tid,N} P) := _.
-  Global Instance na_bor_proper κ :
-    Proper ((⊣⊢) ==> (⊣⊢)) (na_bor κ tid N).
+  Global Instance na_bor_ne κ n : Proper (dist n ==> dist n) (na_bor κ tid N).
+  Proof. solve_proper. Qed.
+  Global Instance na_bor_contractive κ : Contractive (na_bor κ tid N).
+  Proof. solve_contractive. Qed.
+  Global Instance na_bor_proper κ : Proper ((⊣⊢) ==> (⊣⊢)) (na_bor κ tid N).
+  Proof. solve_proper. Qed.
+
+  Lemma na_bor_iff κ P' :
+    ▷ □ (P ↔ P') -∗ &na{κ, tid, N} P -∗ &na{κ, tid, N} P'.
   Proof.
-    intros P1 P2 EQ. apply uPred.exist_proper. intros i. by rewrite EQ.
+    iIntros "HPP' H". iDestruct "H" as (i) "[HP ?]". iExists i. iFrame.
+    iApply (idx_bor_iff with "HPP' HP").
   Qed.
 
+  Global Instance na_bor_persistent κ : Persistent (&na{κ,tid,N} P) := _.
+
   Lemma bor_na κ E : ↑lftN ⊆ E → &{κ}P ={E}=∗ &na{κ,tid,N}P.
   Proof.
     iIntros (?) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "[#? Hown]".
     iExists i. iFrame "#". iApply (na_inv_alloc tid E N with "[Hown]"). auto.
   Qed.
 
-  Lemma na_bor_acc q κ E :
-    ↑lftN ⊆ E → ↑N ⊆ E →
-    lft_ctx -∗ &na{κ,tid,N}P -∗ q.[κ] -∗ na_own tid E ={E}=∗
-            ▷P ∗ na_own tid (E ∖ ↑N) ∗
-            (▷P -∗ na_own tid (E ∖ ↑N) ={E}=∗ q.[κ] ∗ na_own tid E).
+  Lemma na_bor_acc q κ E F :
+    ↑lftN ⊆ E → ↑N ⊆ E → ↑N ⊆ F →
+    lft_ctx -∗ &na{κ,tid,N}P -∗ q.[κ] -∗ na_own tid F ={E}=∗
+            ▷P ∗ na_own tid (F ∖ ↑N) ∗
+            (▷P -∗ na_own tid (F ∖ ↑N) ={E}=∗ q.[κ] ∗ na_own tid F).
   Proof.
-    iIntros (??) "#LFT#HP Hκ Hnaown".
+    iIntros (???) "#LFT#HP Hκ Hnaown".
     iDestruct "HP" as (i) "(#Hpers&#Hinv)".
-    iMod (na_inv_open with "Hinv Hnaown") as "(>Hown&Hnaown&Hclose)"; try done.
-    iMod (idx_bor_acc with "LFT Hpers Hown Hκ") as "[HP Hclose']". done.
-    iIntros "{$HP $Hnaown}!>HP Hnaown".
+    iMod (na_inv_acc with "Hinv Hnaown") as "(>Hown&Hnaown&Hclose)"; try done.
+    iMod (idx_bor_acc with "LFT Hpers Hown Hκ") as "[HP Hclose']"; first done.
+    iIntros "{$HP $Hnaown} !> HP Hnaown".
     iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame.
   Qed.
 
   Lemma na_bor_shorten κ κ': κ ⊑ κ' -∗ &na{κ',tid,N}P -∗ &na{κ,tid,N}P.
   Proof.
-    iIntros "Hκκ' H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
+    iIntros "Hκκ' H". iDestruct "H" as (i) "[H ?]". iExists i. iFrame.
     iApply (idx_bor_shorten with "Hκκ' H").
   Qed.
 
+  Lemma na_bor_fake E κ: ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &na{κ,tid,N}P.
+  Proof.
+    iIntros (?) "#LFT#H†". iApply (bor_na with "[>]"); first done.
+    by iApply (bor_fake with "LFT H†").
+  Qed.
 End na_bor.
 
-Typeclasses Opaque na_bor.
+Global Typeclasses Opaque na_bor.

make-package

+#!/bin/bash
+set -e
+# Helper script to build and/or install just one package out of this repository.
+# Assumes that all the other packages it depends on have been installed already!
+
+PROJECT="$1"
+shift
+
+COQFILE="_CoqProject.$PROJECT"
+MAKEFILE="Makefile.package.$PROJECT"
+
+if ! grep -E -q "^$PROJECT/" _CoqProject; then
+    echo "No files in $PROJECT/ found in _CoqProject; this does not seem to be a valid project name."
+    exit 1
+fi
+
+# Generate _CoqProject file and Makefile
+rm -f "$COQFILE"
+# Get the right "-Q" line.
+grep -E "^-Q $PROJECT[ /]" _CoqProject >> "$COQFILE"
+# Get everything until the first empty line except for the "-Q" lines.
+sed -n '/./!q;p' _CoqProject | grep -E -v "^-Q " >> "$COQFILE"
+# Get the files.
+grep -E "^$PROJECT/" _CoqProject >> "$COQFILE"
+# Now we can run coq_makefile.
+"${COQBIN}coq_makefile" -f "$COQFILE" -o "$MAKEFILE"
+
+# Run build
+make -f "$MAKEFILE" "$@"
+
+# Cleanup
+rm -f ".$MAKEFILE.d" "$MAKEFILE"*

opam

-opam-version: "1.2"
-name: "coq-lambda-rust"
-version: "dev"
-maintainer: "Ralf Jung <jung@mpi-sws.org>"
-authors: "The RustBelt Team"
-homepage: "http://plv.mpi-sws.org/rustbelt/"
-bug-reports: "https://gitlab.mpi-sws.org/FP/lambdaRust-coq/issues"
-license: "BSD"
-dev-repo: "https://gitlab.mpi-sws.org/FP/lambdaRust-coq.git"
-build: [
-  [make "-j%{jobs}%"]
-]
-install: [make "install"]
-remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
-depends: [
-  "coq-iris"
-]

opam.pins

-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq b72a3301d7ff957cfbb06d06bba85fb4ee9a2c39

theories/lang/derived.v

-From lrust.lang Require Export lifting.
-From iris.proofmode Require Import tactics.
-Import uPred.
-
-(** Define some derived forms, and derived lemmas about them. *)
-Notation Lam xl e := (Rec BAnon xl e).
-Notation Let x e1 e2 := (App (Lam [x] e2) [e1]).
-Notation Seq e1 e2 := (Let BAnon e1 e2).
-Notation LamV xl e := (RecV BAnon xl e).
-Notation LetCtx x e2 := (AppRCtx (LamV [x] e2) [] []).
-Notation SeqCtx e2 := (LetCtx BAnon e2).
-Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
-Coercion lit_of_bool : bool >-> base_lit.
-Notation If e0 e1 e2 := (Case e0 [e2;e1]).
-Definition Newlft := Lit LitUnit.
-Definition Endlft := Skip.
-
-Section derived.
-Context `{ownPG lrust_lang Σ}.
-Implicit Types P Q : iProp Σ.
-Implicit Types Φ : val → iProp Σ.
-
-(** Proof rules for the sugar *)
-Lemma wp_lam E xl e e' el Φ :
-  Forall (λ ei, is_Some (to_val ei)) el →
-  Closed (xl +b+ []) e →
-  subst_l xl el e = Some e' →
-  ▷ WP e' @ E {{ Φ }} -∗ WP App (Lam xl e) el @ E {{ Φ }}.
-Proof. iIntros (???) "?". by iApply (wp_rec _ _ BAnon). Qed.
-
-Lemma wp_let E x e1 e2 v Φ :
-  to_val e1 = Some v →
-  Closed (x :b: []) e2 →
-  ▷ WP subst' x e1 e2 @ E {{ Φ }} -∗ WP Let x e1 e2 @ E {{ Φ }}.
-Proof. eauto using wp_lam. Qed.
-
-Lemma wp_seq E e1 e2 v Φ :
-  to_val e1 = Some v →
-  Closed [] e2 →
-  ▷ WP e2 @ E {{ Φ }} -∗ WP Seq e1 e2 @ E {{ Φ }}.
-Proof. iIntros (??) "?". by iApply (wp_let _ BAnon). Qed.
-
-Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) -∗ WP Skip @ E {{ Φ }}.
-Proof. iIntros. iApply wp_seq. done. iNext. by iApply wp_value. Qed.
-
-Lemma wp_le E (n1 n2 : Z) P Φ :
-  (n1 ≤ n2 → P -∗ ▷ |={E}=> Φ (LitV true)) →
-  (n2 < n1 → P -∗ ▷ |={E}=> Φ (LitV false)) →
-  P -∗ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
-Proof.
-  iIntros (Hl Hg) "HP". iApply wp_fupd.
-  destruct (bool_decide_reflect (n1 ≤ n2)); [rewrite Hl //|rewrite Hg; last omega];
-    clear Hl Hg; (iApply wp_bin_op_pure; first by econstructor); iNext; iIntros (?? Heval);
-    inversion_clear Heval; [rewrite bool_decide_true //|rewrite bool_decide_false //].
-Qed.
-
-Lemma wp_offset E l z Φ :
-  ▷ (|={E}=> Φ (LitV $ LitLoc $ shift_loc l z)) -∗
-    WP BinOp OffsetOp (Lit $ LitLoc l) (Lit $ LitInt z) @ E {{ Φ }}.
-Proof.
-  iIntros "HP". iApply wp_fupd. iApply wp_bin_op_pure; first by econstructor.
-  iNext. iIntros (?? Heval). inversion_clear Heval. done.
-Qed.
-
-Lemma wp_plus E z1 z2 Φ :
-  ▷ (|={E}=> Φ (LitV $ LitInt $ z1 + z2)) -∗
-    WP BinOp PlusOp (Lit $ LitInt z1) (Lit $ LitInt z2) @ E {{ Φ }}.
-Proof.
-  iIntros "HP". iApply wp_fupd. iApply wp_bin_op_pure; first by econstructor.
-  iNext. iIntros (?? Heval). inversion_clear Heval. done.
-Qed.
-
-Lemma wp_minus E z1 z2 Φ :
-  ▷ (|={E}=> Φ (LitV $ LitInt $ z1 - z2)) -∗
-    WP BinOp MinusOp (Lit $ LitInt z1) (Lit $ LitInt z2) @ E {{ Φ }}.
-Proof.
-  iIntros "HP". iApply wp_fupd. iApply wp_bin_op_pure; first by econstructor.
-  iNext. iIntros (?? Heval). inversion_clear Heval. done.
-Qed.
-
-(* TODO: Add lemmas for equality test. *)
-
-Lemma wp_if E (b : bool) e1 e2 Φ :
-  (if b then ▷ WP e1 @ E {{ Φ }} else ▷ WP e2 @ E {{ Φ }})%I -∗
-  WP If (Lit b) e1 e2 @ E {{ Φ }}.
-Proof. iIntros "?". by destruct b; iApply wp_case. Qed.
-End derived.

theories/lang/lifting.v

-From iris.program_logic Require Export weakestpre ownp.
-From iris.program_logic Require Import ectx_lifting.
-From lrust.lang Require Export lang.
-From lrust.lang Require Import tactics.
-From iris.proofmode Require Import tactics.
-Import uPred.
-Local Hint Extern 0 (head_reducible _ _) => do_head_step eauto 2.
-
-(* TODO : as for heap_lang, directly use a global heap invariant. *)
-
-Section lifting.
-Context `{ownPG lrust_lang Σ}.
-Implicit Types P Q : iProp Σ.
-Implicit Types ef : option expr.
-
-(** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
-Lemma wp_bind {E e} K Φ :
-  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} -∗ WP fill K e @ E {{ Φ }}.
-Proof. exact: wp_ectx_bind. Qed.
-
-Lemma wp_bindi {E e} Ki Φ :
-  WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} -∗
-     WP fill_item Ki e @ E {{ Φ }}.
-Proof. exact: weakestpre.wp_bind. Qed.
-
-(** Base axioms for core primitives of the language: Stateful reductions. *)
-Lemma wp_alloc_pst E σ n:
-  0 < n →
-  {{{ ▷ ownP σ }}} Alloc (Lit $ LitInt n) @ E
-  {{{ l σ', RET LitV $ LitLoc l;
-      ⌜∀ m, σ !! (shift_loc l m) = None⌝ ∗
-      ⌜∃ vl, n = length vl ∧ init_mem l vl σ = σ'⌝ ∗
-      ownP σ' }}}.
-Proof.
-  iIntros (? Φ) "HP HΦ". iApply (ownP_lift_atomic_head_step _ σ); eauto.
-  iFrame "HP". iNext. iIntros (v2 σ2 ef) "% HP". inv_head_step.
-  rewrite big_sepL_nil right_id. by iApply "HΦ"; iFrame; eauto.
-Qed.
-
-Lemma wp_free_pst E σ l n :
-  0 < n →
-  (∀ m, is_Some (σ !! (shift_loc l m)) ↔ (0 ≤ m < n)) →
-  {{{ ▷ ownP σ }}} Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E
-  {{{ RET LitV $ LitUnit; ownP (free_mem l (Z.to_nat n) σ) }}}.
-Proof.
-  iIntros (???)  "HP HΦ". iApply (ownP_lift_atomic_head_step _ σ); eauto.
-  iFrame "HP". iNext. iIntros (v2 σ2 ef) "% HP". inv_head_step.
-  rewrite big_sepL_nil right_id. by iApply "HΦ".
-Qed.
-
-Lemma wp_read_sc_pst E σ l n v :
-  σ !! l = Some (RSt n, v) →
-  {{{ ▷ ownP σ }}} Read ScOrd (Lit $ LitLoc l) @ E {{{ RET v; ownP σ }}}.
-Proof.
-  iIntros (??) "?HΦ". iApply ownP_lift_atomic_det_head_step; eauto.
-  by intros; inv_head_step; eauto using to_of_val.
-  rewrite big_sepL_nil right_id; iFrame.
-Qed.
-
-Lemma wp_read_na2_pst E σ l n v :
-  σ !! l = Some(RSt $ S n, v) →
-  {{{ ▷ ownP σ }}} Read Na2Ord (Lit $ LitLoc l) @ E
-  {{{ RET v; ownP (<[l:=(RSt n, v)]>σ) }}}.
-Proof.
-  iIntros (??) "?HΦ". iApply ownP_lift_atomic_det_head_step; eauto.
-  by intros; inv_head_step; eauto using to_of_val.
-  rewrite big_sepL_nil right_id; iFrame.
-Qed.
-
-Lemma wp_read_na1_pst E l Φ :
-  (|={E,∅}=> ∃ σ n v, ⌜σ !! l = Some(RSt $ n, v)⌝ ∧
-     ▷ ownP σ ∗
-     ▷ (ownP (<[l:=(RSt $ S n, v)]>σ) ={∅,E}=∗
-          WP Read Na2Ord (Lit $ LitLoc l) @ E {{ Φ }})) -∗
-  WP Read Na1Ord (Lit $ LitLoc l) @ E {{ Φ }}.
-Proof.
-  iIntros "HΦP". iApply (ownP_lift_head_step E); auto.
-  iMod "HΦP" as (σ n v) "(%&HΦ&HP)". iModIntro. iExists σ. iSplit. done. iFrame.
-  iNext. iIntros (e2 σ2 ef) "% HΦ". inv_head_step.
-  rewrite big_sepL_nil right_id. iApply ("HP" with "HΦ").
-Qed.
-
-Lemma wp_write_sc_pst E σ l v v' :
-  σ !! l = Some (RSt 0, v') →
-  {{{ ▷ ownP σ }}} Write ScOrd (Lit $ LitLoc l) (of_val v) @ E
-  {{{ RET LitV LitUnit; ownP (<[l:=(RSt 0, v)]>σ) }}}.
-Proof.
-  iIntros (??) "?HΦ". iApply ownP_lift_atomic_det_head_step; eauto.
-  by intros; inv_head_step; eauto. rewrite big_sepL_nil right_id; iFrame.
-Qed.
-
-Lemma wp_write_na2_pst E σ l v v' :
-  σ !! l = Some(WSt, v') →
-  {{{ ▷ ownP σ }}} Write Na2Ord (Lit $ LitLoc l) (of_val v) @ E
-  {{{ RET LitV LitUnit; ownP (<[l:=(RSt 0, v)]>σ) }}}.
-Proof.
-  iIntros (??) "?HΦ". iApply ownP_lift_atomic_det_head_step; eauto.
-  by intros; inv_head_step; eauto. rewrite big_sepL_nil right_id; iFrame.
-Qed.
-
-Lemma wp_write_na1_pst E l v Φ :
-  (|={E,∅}=> ∃ σ v', ⌜σ !! l = Some(RSt 0, v')⌝ ∧
-     ▷ ownP σ ∗
-     ▷ (ownP (<[l:=(WSt, v')]>σ) ={∅,E}=∗
-       WP Write Na2Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }})) -∗
-  WP Write Na1Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }}.
-Proof.
-  iIntros "HΦP". iApply (ownP_lift_head_step E); auto.
-  iMod "HΦP" as (σ v') "(%&HΦ&HP)". iModIntro. iExists σ. iSplit. done. iFrame.
-  iNext. iIntros (e2 σ2 ef) "% HΦ". inv_head_step.
-  rewrite big_sepL_nil right_id. iApply ("HP" with "HΦ").
-Qed.
-
-Lemma wp_cas_pst E n σ l e1 lit1 lit2 litl :
-  to_val e1 = Some $ LitV lit1 →
-  σ !! l = Some (RSt n, LitV litl) →
-  (lit_eq σ lit1 litl ∨ lit_neq σ lit1 litl) →
-  (lit_eq σ lit1 litl → n = 0%nat) →
-  {{{ ▷ ownP σ }}} CAS (Lit $ LitLoc l) e1 (Lit lit2) @ E
-  {{{ b, RET LitV $ lit_of_bool b;
-      if b is true then ⌜lit_eq σ lit1 litl⌝ ∗ ownP (<[l:=(RSt 0, LitV lit2)]>σ)
-      else ⌜lit_neq σ lit1 litl⌝ ∗ ownP σ }}}.
-Proof.
-  iIntros (?%of_to_val ? Hdec Hn ?) "HP HΦ". subst.
-  iApply ownP_lift_atomic_head_step; eauto.
-  { destruct Hdec as [Heq|Hneq].
-    - specialize (Hn Heq). subst. do 3 eexists. by eapply CasSucS.
-    - do 3 eexists. by eapply CasFailS. }
-  iFrame. iNext. iIntros (e2 σ2 efs Hs) "Ho".
-  inv_head_step; rewrite big_sepL_nil right_id.
-  - iApply ("HΦ" $! false). eauto.
-  - iApply ("HΦ" $! true). eauto.
-  - exfalso. refine (_ (Hn _)); last done. intros. omega.
-Qed.
-
-(** Base axioms for core primitives of the language: Stateless reductions *)
-Lemma wp_fork E e :
-  {{{ ▷ WP e {{ _, True }} }}} Fork e @ E {{{ RET LitV LitUnit; True }}}.
-Proof.
-  iIntros (?) "?HΦ". iApply ownP_lift_pure_det_head_step; eauto.
-  by intros; inv_head_step; eauto. iNext.
-  rewrite big_sepL_singleton. iFrame. iApply wp_value. done. by iApply "HΦ".
-Qed.
-
-Lemma wp_rec E e f xl erec erec' el Φ :
-  e = Rec f xl erec → (* to avoids recursive calls being unfolded *)
-  Forall (λ ei, is_Some (to_val ei)) el →
-  Closed (f :b: xl +b+ []) erec →
-  subst_l xl el erec = Some erec' →
-  ▷ WP subst' f e erec' @ E {{ Φ }} -∗
-  WP App e el @ E {{ Φ }}.
-Proof.
-  iIntros (-> ???) "?". iApply ownP_lift_pure_det_head_step; subst; eauto.
-  by intros; inv_head_step; eauto. iNext. rewrite big_sepL_nil. by iFrame.
-Qed.
-
-Lemma wp_bin_op_heap E σ op l1 l2 l' :
-  bin_op_eval σ op l1 l2 l' →
-  {{{ ▷ ownP σ }}} BinOp op (Lit l1) (Lit l2) @ E
-  {{{ l'', RET LitV l''; ⌜bin_op_eval σ op l1 l2 l''⌝ ∗ ownP σ }}}.
-Proof.
-  iIntros (? Φ) "HP HΦ". iApply ownP_lift_atomic_head_step; eauto.
-  iFrame "HP". iNext. iIntros (e2 σ2 efs Hs) "Ho".
-  inv_head_step; rewrite big_sepL_nil right_id.
-  iApply "HΦ". eauto.
-Qed.
-
-Lemma wp_bin_op_pure E op l1 l2 l' :
-  (∀ σ, bin_op_eval σ op l1 l2 l') →
-  {{{ True }}} BinOp op (Lit l1) (Lit l2) @ E
-  {{{ l'' σ, RET LitV l''; ⌜bin_op_eval σ op l1 l2 l''⌝ }}}.
-Proof.
-  iIntros (? Φ) "HΦ". iApply ownP_lift_pure_head_step; eauto.
-  { intros. inv_head_step. done. }
-  iNext. iIntros (e2 efs σ Hs).
-  inv_head_step; rewrite big_sepL_nil right_id.
-  rewrite -wp_value //. iApply "HΦ". eauto.
-Qed.
-
-Lemma wp_case E i e el Φ :
-  0 ≤ i →
-  nth_error el (Z.to_nat i) = Some e →
-  ▷ WP e @ E {{ Φ }} -∗ WP Case (Lit $ LitInt i) el @ E {{ Φ }}.
-Proof.
-  iIntros (??) "?". iApply ownP_lift_pure_det_head_step; eauto.
-  by intros; inv_head_step; eauto. iNext. rewrite big_sepL_nil. by iFrame.
-Qed.
-End lifting.

theories/lang/new_delete.v

-From iris.base_logic.lib Require Import namespaces.
-From lrust.lang Require Export notation.
-From lrust.lang Require Import heap proofmode.
-
-Definition new : val :=
-  λ: ["n"],
-    if: "n" ≤ #0 then #((42%positive, 1337):loc)
-    else Alloc "n".
-Opaque new.
-
-Definition delete : val :=
-  λ: ["n"; "loc"],
-    if: "n" ≤ #0 then #()
-    else Free "n" "loc".
-Opaque delete.
-
-Section specs.
-  Context `{heapG Σ}.
-
-  Lemma wp_new E n:
-    ↑heapN ⊆ E → 0 ≤ n →
-    {{{ heap_ctx }}} new [ #n ] @ E
-    {{{ l vl, RET LitV $ LitLoc l;
-        ⌜n = length vl⌝ ∗ (†l…(Z.to_nat n) ∨ ⌜n = 0⌝) ∗ l ↦∗ vl }}}.
-  Proof.
-    iIntros (? ? Φ) "#Hinv HΦ". wp_lam. wp_op; intros ?.
-    - wp_if. assert (n = 0) as -> by lia. iApply ("HΦ" $! _ []).
-      rewrite heap_mapsto_vec_nil. auto.
-    - wp_if. wp_alloc l vl as "H↦" "H†". iApply  "HΦ". iFrame. auto.
-  Qed.
-
-  Lemma wp_delete E (n:Z) l vl :
-    ↑heapN ⊆ E → n = length vl →
-    {{{ heap_ctx ∗ l ↦∗ vl ∗ (†l…(length vl) ∨ ⌜n = 0⌝) }}}
-      delete [ #n; #l] @ E
-    {{{ RET LitV LitUnit; True }}}.
-  Proof.
-    iIntros (? ? Φ) "(#Hinv & H↦ & [H†|%]) HΦ";
-      wp_lam; wp_op; intros ?; try lia; wp_if; try wp_free; by iApply "HΦ".
-  Qed.
-End specs.
\ No newline at end of file

theories/lang/notation.v

-From lrust.lang Require Export derived.
-
-Coercion LitInt : Z >-> base_lit.
-Coercion LitLoc : loc >-> base_lit.
-
-Coercion App : expr >-> Funclass.
-Coercion of_val : val >-> expr.
-
-Coercion Var : string >-> expr.
-
-Coercion BNamed : string >-> binder.
-Notation "<>" := BAnon : lrust_binder_scope.
-
-(* No scope for the values, does not conflict and scope is often not inferred
-properly. *)
-Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
-Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : expr_scope.
-
-(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
-    first. *)
-Notation "'case:' e0 'of' [ e1 , .. , en ]" :=
-  (Case e0%E (cons e1%E .. (cons en%E nil) ..))
-  (e0, e1, en at level 200) : expr_scope.
-Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
-  (at level 200, e1, e2, e3 at level 200) : expr_scope.
-Notation "()" := LitUnit : val_scope.
-Notation "! e" := (Read Na1Ord e%E)
-  (at level 9, right associativity) : expr_scope.
-Notation "!ˢᶜ e" := (Read ScOrd e%E)
-  (at level 9, right associativity) : expr_scope.
-Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E)
-  (at level 50, left associativity) : expr_scope.
-Notation "e1 - e2" := (BinOp MinusOp e1%E e2%E)
-  (at level 50, left associativity) : expr_scope.
-Notation "e1 ≤ e2" := (BinOp LeOp e1%E e2%E)
-  (at level 70) : expr_scope.
-(* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
-Notation "e1 <-ˢᶜ e2" := (Write ScOrd e1%E e2%E)
-  (at level 80) : expr_scope.
-Notation "e1 <- e2" := (Write Na1Ord e1%E e2%E)
-  (at level 80) : expr_scope.
-Notation "'rec:' f [ x1 ; .. ; xn ] := e" :=
-  (Rec f%RustB ( @cons binder x1%RustB ( .. (@cons binder xn%RustB nil) ..)) e%E)
-  (at level 102, f at level 1, x1 at level 1, xn at level 1, e at level 200) : expr_scope.
-Notation "'rec:' f [ x1 ; .. ; xn ] := e" :=
-  (RecV f%RustB ( @cons binder x1%RustB ( .. (@cons binder xn%RustB nil) ..)) e%E)
-  (at level 102, f at level 1, x1 at level 1, xn at level 1, e at level 200) : val_scope.
-Notation "'rec:' f [ ] := e" := (Rec f%RustB nil e%E)
-  (at level 102, f at level 1, e at level 200) : expr_scope.
-Notation "'rec:' f [ ] := e" := (RecV f%RustB nil e%E)
-  (at level 102, f at level 1, e at level 200) : val_scope.
-Notation "e1 +ₗ e2" := (BinOp OffsetOp e1%E e2%E)
-  (at level 50, left associativity) : expr_scope.
-
-(** Derived notions, in order of declaration. The notations for let and seq
-are stated explicitly instead of relying on the Notations Let and Seq as
-defined above. This is needed because App is now a coercion, and these
-notations are otherwise not pretty printed back accordingly. *)
-Notation "λ: [ x1 ; .. ; xn ] , e" :=
-  (Lam ( @cons binder x1%RustB ( .. (@cons binder xn%RustB nil) ..)) e%E)
-  (at level 102, x1 at level 1, xn at level 1, e at level 200) : expr_scope.
-Notation "λ: [ x1 ; .. ; xn ] , e" :=
-  (LamV ( @cons binder x1%RustB ( .. (@cons binder xn%RustB nil) ..)) e%E)
-  (at level 102, x1 at level 1, xn at level 1, e at level 200) : val_scope.
-Notation "λ: [ ] , e" := (Lam nil e%E)
-  (at level 102, e at level 200) : expr_scope.
-Notation "λ: [ ] , e" := (LamV nil e%E)
-  (at level 102, e at level 200) : val_scope.
-
-Notation "'let:' x := e1 'in' e2" := (Lam [x%RustB] e2%E [e1%E])
-  (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
-Notation "e1 ;; e2" := (Lam [BAnon] e2%E [e1%E])
-  (at level 100, e2 at level 200, format "e1  ;;  e2") : expr_scope.
-(* These are not actually values, but we want them to be pretty-printed. *)
-Notation "'let:' x := e1 'in' e2" := (LamV [x%RustB] e2%E [e1%E])
-  (at level 102, x at level 1, e1, e2 at level 200) : val_scope.
-Notation "e1 ;; e2" := (LamV [BAnon] e2%E [e1%E])
-  (at level 100, e2 at level 200, format "e1  ;;  e2") : val_scope.
-
-Notation "e1 <-[ i ] '☇'" := (e1 <- #i)%E
-  (only parsing, at level 80) : expr_scope.
-Notation "e1 <-[ i ] e2" := (e1<-[i] ☇ ;; e1+ₗ#1 <- e2)%E
- (at level 80) : expr_scope.

theories/lang/proofmode.v

-From iris.proofmode Require Import coq_tactics.
-From iris.proofmode Require Export tactics.
-From iris.base_logic Require Import namespaces.
-From lrust.lang Require Export wp_tactics heap.
-Import uPred.
-
-Ltac wp_strip_later ::= iNext.
-
-Section heap.
-Context `{heapG Σ}.
-Implicit Types P Q : iProp Σ.
-Implicit Types Φ : val → iProp Σ.
-Implicit Types Δ : envs (iResUR Σ).
-
-Lemma tac_wp_alloc Δ Δ' E j1 j2 n Φ :
-  (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → 0 < n →
-  IntoLaterNEnvs 1 Δ Δ' →
-  (∀ l vl, n = length vl → ∃ Δ'',
-    envs_app false (Esnoc (Esnoc Enil j1 (l ↦∗ vl)) j2 (†l…(Z.to_nat n))) Δ'
-      = Some Δ'' ∧
-    (Δ'' ⊢ |={E}=> Φ (LitV $ LitLoc l))) →
-  Δ ⊢ WP Alloc (Lit $ LitInt n) @ E {{ Φ }}.
-Proof.
-  intros ???? HΔ. rewrite -wp_fupd. eapply wand_apply; first exact:wp_alloc.
-  rewrite -always_and_sep_l. apply and_intro; first done.
-  rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l;
-  apply forall_intro=> vl. apply wand_intro_l. rewrite -assoc.
-  apply pure_elim_sep_l=> Hn. apply wand_elim_r'.
-  destruct (HΔ l vl) as (Δ''&?&HΔ'). done.
-  rewrite envs_app_sound //; simpl. by rewrite right_id HΔ'.
-Qed.
-
-Lemma tac_wp_free Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
-  (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → n = length vl →
-  IntoLaterNEnvs 1 Δ Δ' →
-  envs_lookup i1 Δ' = Some (false, l ↦∗ vl)%I →
-  envs_delete i1 false Δ' = Δ'' →
-  envs_lookup i2 Δ'' = Some (false, †l…n')%I →
-  envs_delete i2 false Δ'' = Δ''' →
-  n' = length vl →
-  (Δ''' ⊢ |={E}=> Φ (LitV LitUnit)) →
-  Δ ⊢ WP Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E {{ Φ }}.
-Proof.
-  intros ?? -> ?? <- ? <- -> HΔ. rewrite -wp_fupd.
-  eapply wand_apply; first exact:wp_free. rewrite -!assoc -always_and_sep_l.
-  apply and_intro; first done.
-  rewrite into_laterN_env_sound -!later_sep; apply later_mono.
-  do 2 (rewrite envs_lookup_sound' //). by rewrite HΔ wand_True.
-Qed.
-
-Lemma tac_wp_read Δ Δ' E i l q v o Φ :
-  (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → o = Na1Ord ∨ o = ScOrd →
-  IntoLaterNEnvs 1 Δ Δ' →
-  envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
-  (Δ' ⊢ |={E}=> Φ v) →
-  Δ ⊢ WP Read o (Lit $ LitLoc l) @ E {{ Φ }}.
-Proof.
-  intros ??[->| ->]???.
-  - rewrite -wp_fupd. eapply wand_apply; first exact:wp_read_na.
-    rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
-    rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
-      by apply later_mono, sep_mono_r, wand_mono.
-  - rewrite -wp_fupd. eapply wand_apply; first exact:wp_read_sc.
-    rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
-    rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
-      by apply later_mono, sep_mono_r, wand_mono.
-Qed.
-
-Lemma tac_wp_write Δ Δ' Δ'' E i l v e v' o Φ :
-  to_val e = Some v' →
-  (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → o = Na1Ord ∨ o = ScOrd →
-  IntoLaterNEnvs 1 Δ Δ' →
-  envs_lookup i Δ' = Some (false, l ↦ v)%I →
-  envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
-  (Δ'' ⊢ |={E}=> Φ (LitV LitUnit)) →
-  Δ ⊢ WP Write o (Lit $ LitLoc l) e @ E {{ Φ }}.
-Proof.
-  intros ???[->| ->]????.
-  - rewrite -wp_fupd. eapply wand_apply; first by apply wp_write_na.
-    rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
-    rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
-    rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
-  - rewrite -wp_fupd. eapply wand_apply; first by apply wp_write_sc.
-    rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
-    rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
-    rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
-Qed.
-End heap.
-
-Tactic Notation "wp_apply" open_constr(lem) :=
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    wp_bind_core K; iApply lem; try iNext)
-  | _ => fail "wp_apply: not a 'wp'"
-  end.
-
-Tactic Notation "wp_alloc" ident(l) ident(vl) "as" constr(H) constr(Hf) :=
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
-    first
-      [reshape_expr e ltac:(fun K e' =>
-         match eval hnf in e' with Alloc _ => wp_bind_core K end)
-      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
-    eapply tac_wp_alloc with _ H Hf;
-      [iAssumption || fail "wp_alloc: cannot find heap_ctx"
-      |solve_ndisj
-      |try fast_done
-      |apply _
-      |first [intros l vl ? | fail 1 "wp_alloc:" l "or" vl "not fresh"];
-        eexists; split;
-          [env_cbv; reflexivity || fail "wp_alloc:" H "or" Hf "not fresh"
-          |wp_finish]]
-  | _ => fail "wp_alloc: not a 'wp'"
-  end.
-
-Tactic Notation "wp_alloc" ident(l) ident(vl) :=
-  let H := iFresh in let Hf := iFresh in wp_alloc l vl as H Hf.
-
-Tactic Notation "wp_free" :=
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
-    first
-      [reshape_expr e ltac:(fun K e' =>
-         match eval hnf in e' with Free _ _ => wp_bind_core K end)
-      |fail 1 "wp_free: cannot find 'Free' in" e];
-    eapply tac_wp_free;
-      [iAssumption || fail "wp_free: cannot find heap_ctx"
-      |solve_ndisj
-      |try fast_done
-      |apply _
-      |let l := match goal with |- _ = Some (_, (?l ↦∗ _)%I) => l end in
-       iAssumptionCore || fail "wp_free: cannot find" l "↦∗ ?"
-      |env_cbv; reflexivity
-      |let l := match goal with |- _ = Some (_, († ?l … _)%I) => l end in
-       iAssumptionCore || fail "wp_free: cannot find †" l "… ?"
-      |env_cbv; reflexivity
-      |try fast_done
-      |wp_finish]
-  | _ => fail "wp_free: not a 'wp'"
-  end.
-
-Tactic Notation "wp_read" :=
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
-    first
-      [reshape_expr e ltac:(fun K e' =>
-         match eval hnf in e' with Read _ _ => wp_bind_core K end)
-      |fail 1 "wp_read: cannot find 'Read' in" e];
-    eapply tac_wp_read;
-      [iAssumption || fail "wp_read: cannot find heap_ctx"
-      |solve_ndisj
-      |(right; fast_done) || (left; fast_done) ||
-       fail "wp_read: order is neither Na2Ord nor ScOrd"
-      |apply _
-      |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
-       iAssumptionCore || fail "wp_read: cannot find" l "↦ ?"
-      |wp_finish]
-  | _ => fail "wp_read: not a 'wp'"
-  end.
-
-Tactic Notation "wp_write" :=
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
-    first
-      [reshape_expr e ltac:(fun K e' =>
-         match eval hnf in e' with Write _ _ _ => wp_bind_core K end)
-      |fail 1 "wp_write: cannot find 'Write' in" e];
-    eapply tac_wp_write;
-      [let e' := match goal with |- to_val ?e' = _ => e' end in
-       wp_done || fail "wp_write:" e' "not a value"
-      |iAssumption || fail "wp_write: cannot find heap_ctx"
-      |solve_ndisj
-      |(right; fast_done) || (left; fast_done) ||
-       fail "wp_write: order is neither Na2Ord nor ScOrd"
-      |apply _
-      |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
-       iAssumptionCore || fail "wp_write: cannot find" l "↦ ?"
-      |env_cbv; reflexivity
-      |wp_finish]
-  | _ => fail "wp_write: not a 'wp'"
-  end.

theories/lang/wp_tactics.v

-From lrust.lang Require Export tactics derived.
-Import uPred.
-
-(** wp-specific helper tactics *)
-Ltac wp_bind_core K :=
-  lazymatch eval hnf in K with
-  | [] => idtac
-  | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
-  end.
-
-(* FIXME : the [reflexivity] tactic is not able to solve trivial
-   reflexivity proofs, while [exact (reflexivity _)] does. *)
-Ltac wp_done :=
-  rewrite /= ?to_of_val;
-  match goal with
-  | |- _ = _ => exact (reflexivity _)
-  | |- Forall _ [] => fast_by apply List.Forall_nil
-  | |- Forall _ (_ :: _) => apply List.Forall_cons; wp_done
-  | |- is_Some (Some ?v) => exists v; reflexivity
-  | |- _ => fast_done
-  end.
-
-(* sometimes, we will have to do a final view shift, so only apply
-pvs_intro if we obtain a consecutive wp *)
-Ltac wp_strip_pvs :=
-  lazymatch goal with
-  | |- _ ⊢ |={?E}=> _ =>
-    etrans; [|apply fupd_intro];
-    match goal with |- _ ⊢ wp E _ _ => simpl | _ => fail end
-  end.
-
-Ltac wp_value_head := etrans; [|eapply wp_value_fupd; wp_done]; lazy beta.
-
-Ltac wp_strip_later := idtac. (* a hook to be redefined later *)
-
-Ltac wp_seq_head :=
-  lazymatch goal with
-  | |- _ ⊢ wp ?E (Seq _ _) ?Q =>
-    etrans; [|eapply wp_seq; wp_done]; wp_strip_later
-  end.
-
-Ltac wp_finish := intros_revert ltac:(
-  rewrite /= ?to_of_val;
-  try wp_strip_later;
-  repeat lazymatch goal with
-  | |- _ ⊢ wp ?E (Seq _ _) ?Q =>
-     etrans; [|eapply wp_seq; wp_done]; wp_strip_later
-  | |- _ ⊢ wp ?E _ ?Q => wp_value_head
-  | |- _ ⊢ |={_}=> _ => wp_strip_pvs
-  end).
-
-Tactic Notation "wp_value" :=
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    wp_bind_core K; wp_value_head) || fail "wp_value: cannot find value in" e
-  | _ => fail "wp_value: not a wp"
-  end.
-
-Tactic Notation "wp_rec" :=
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with App ?e1 _ =>
-(* hnf does not reduce through an of_val *)
-(*      match eval hnf in e1 with Rec _ _ _ => *)
-    wp_bind_core K; etrans; [|eapply wp_rec; wp_done]; simpl_subst; wp_finish
-(*      end *) end) || fail "wp_rec: cannot find 'Rec' in" e
-  | _ => fail "wp_rec: not a 'wp'"
-  end.
-
-Tactic Notation "wp_lam" :=
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with App ?e1 _ =>
-(*    match eval hnf in e1 with Rec BAnon _ _ => *)
-    wp_bind_core K; etrans; [|eapply wp_lam; wp_done]; simpl_subst; wp_finish
-(*    end *) end) || fail "wp_lam: cannot find 'Lam' in" e
-  | _ => fail "wp_lam: not a 'wp'"
-  end.
-
-Tactic Notation "wp_let" := wp_lam.
-Tactic Notation "wp_seq" := wp_let.
-
-Tactic Notation "wp_op" :=
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with
-    | BinOp LeOp _ _ => wp_bind_core K; apply wp_le; wp_finish
-    | BinOp OffsetOp _ _ =>
-       wp_bind_core K; etrans; [|eapply wp_offset; try fast_done]; wp_finish
-    | BinOp PlusOp _ _ =>
-       wp_bind_core K; etrans; [|eapply wp_plus; try fast_done]; wp_finish
-    | BinOp MinusOp _ _ =>
-       wp_bind_core K; etrans; [|eapply wp_minus; try fast_done]; wp_finish
-    end) || fail "wp_op: cannot find 'BinOp' in" e
-  | _ => fail "wp_op: not a 'wp'"
-  end.
-
-Tactic Notation "wp_if" :=
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with
-    | If _ _ _ =>
-      wp_bind_core K;
-      etrans; [|eapply wp_if]; wp_finish
-    end) || fail "wp_if: cannot find 'If' in" e
-  | _ => fail "wp_if: not a 'wp'"
-  end.
-
-Tactic Notation "wp_case" :=
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with
-    | Case _ _ _ =>
-      wp_bind_core K;
-      etrans; [|eapply wp_case; wp_done];
-      simpl_subst; wp_finish
-    end) || fail "wp_case: cannot find 'Case' in" e
-  | _ => fail "wp_case: not a 'wp'"
-  end.
-
-Tactic Notation "wp_bind" open_constr(efoc) :=
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match e' with
-    | efoc => unify e' efoc; wp_bind_core K
-    end) || fail "wp_bind: cannot find" efoc "in" e
-  | _ => fail "wp_bind: not a 'wp'"
-  end.

theories/lifetime/derived.v

-From lrust.lifetime Require Export primitive accessors faking.
-From lrust.lifetime Require Export raw_reborrow.
-From iris.proofmode Require Import tactics.
-(* TODO: the name derived makes no sense: reborrow/bor_unnest, which is proven
-in the model, depends on this file. *)
-
-Section derived.
-Context `{invG Σ, lftG Σ}.
-Implicit Types κ : lft.
-
-Lemma bor_exists {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
-Proof.
-  iIntros (?) "#LFT Hb".
-  iMod (bor_acc_atomic_cons with "LFT Hb") as "[H|[H† >_]]"; first done.
-  - iDestruct "H" as "[HΦ Hclose]". iDestruct "HΦ" as (x) "HΦ".
-    iExists x. iApply ("Hclose" with "HΦ"). iIntros "!> ?"; eauto.
-  - iExists inhabitant. by iApply (bor_fake with "LFT").
-Qed.
-
-Lemma bor_or E κ P Q :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
-Proof.
-  iIntros (?) "#LFT H". rewrite uPred.or_alt.
-  iMod (bor_exists with "LFT H") as ([]) "H"; auto.
-Qed.
-
-Lemma bor_later E κ P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ}(▷ P) ={E,E∖↑lftN}▷=∗ &{κ}P.
-Proof.
-  iIntros (?) "#LFT Hb".
-  iMod (bor_acc_atomic_cons with "LFT Hb") as "[H|[H† Hclose]]"; first done.
-  - iDestruct "H" as "[HP  Hclose]". iModIntro. iNext.
-    iApply ("Hclose" with "* HP"). by iIntros "!> $".
-  - iIntros "!> !>". iMod "Hclose" as "_". by iApply (bor_fake with "LFT").
-Qed.
-
-Lemma bor_later_tok E q κ P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ}(▷ P) -∗ q.[κ] ={E}▷=∗ &{κ}P ∗ q.[κ].
-Proof.
-  iIntros (?) "#LFT Hb Htok".
-  iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose]"; first done.
-  iModIntro. iNext. iApply ("Hclose" with "* HP []"). by iIntros "!> $".
-Qed.
-
-Lemma bor_iff (P Q : iProp Σ) E κ :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ ▷ □ (P ↔ Q) -∗ &{κ}P ={E}=∗ &{κ}Q.
-Proof.
-  iIntros (?) "#LFT #Heq Hb".
-  iMod (bor_acc_atomic_cons with "LFT Hb") as "[[HP Hclose]|[H† Hclose]]". done.
-  - iApply ("Hclose" with "[HP] []").
-      by iApply "Heq". by iIntros "!>HQ!>"; iApply "Heq".
-  - iMod "Hclose". by iApply (bor_fake with "LFT").
-Qed.
-
-Lemma bor_persistent P `{!PersistentP P} E κ q :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
-Proof.
-  iIntros (?) "#LFT Hb Htok".
-  iMod (bor_acc with "LFT Hb Htok") as "[#HP Hob]"; first done.
-  by iMod ("Hob" with "HP") as "[_ $]".
-Qed.
-
-
-Lemma lft_incl_static κ : (κ ⊑ static)%I.
-Proof.
-  iIntros "!#". iSplitR.
-  - iIntros (q) "?". iExists 1%Qp. iSplitR. by iApply lft_tok_static. auto.
-  - iIntros "Hst". by iDestruct (lft_dead_static with "Hst") as "[]".
-Qed.
-End derived.

theories/lifetime/frac_borrow.v

-From Coq Require Import Qcanon.
-From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import lib.fractional.
-From iris.algebra Require Import frac.
-From lrust.lifetime Require Export shr_borrow .
-
-Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
-
-Definition frac_bor `{invG Σ, lftG Σ, frac_borG Σ} κ (Φ : Qp → iProp Σ) :=
-  (∃ γ κ', κ ⊑ κ' ∗ &shr{κ'} ∃ q, Φ q ∗ own γ q ∗
-                       (⌜q = 1%Qp⌝ ∨ ∃ q', ⌜(q + q' = 1)%Qp⌝ ∗ q'.[κ']))%I.
-Notation "&frac{ κ } P" := (frac_bor κ P)
-  (format "&frac{ κ } P", at level 20, right associativity) : uPred_scope.
-
-Section frac_bor.
-  Context `{invG Σ, lftG Σ, frac_borG Σ}.
-  Implicit Types E : coPset.
-
-  Global Instance frac_bor_proper :
-    Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (frac_bor κ).
-  Proof. solve_proper. Qed.
-  Global Instance frac_bor_persistent : PersistentP (&frac{κ}Φ) := _.
-
-  Lemma bor_fracture φ E κ :
-    ↑lftN ⊆ E → lft_ctx -∗ &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
-  Proof.
-    iIntros (?) "#LFT Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done.
-    iMod (bor_acc_atomic_strong with "LFT Hφ") as "[H|[H† Hclose]]". done.
-    - iDestruct "H" as (κ') "(#Hκκ' & Hφ & Hclose)".
-      iMod ("Hclose" with "*[-] []") as "Hφ"; last first.
-      { iExists γ, κ'. iFrame "#". iApply (bor_share with "Hφ"). done. }
-      { iIntros "!>HΦ H†!>". iNext. iDestruct "HΦ" as (q') "(HΦ & _ & [%|Hκ])". by subst.
-        iDestruct "Hκ" as (q'') "[_ Hκ]".
-        iDestruct (lft_tok_dead with "Hκ H†") as "[]". }
-      iExists 1%Qp. iFrame. eauto.
-    - iMod ("Hclose" with "*") as "_"; last first.
-      iExists γ, κ. iSplitR. by iApply lft_incl_refl.
-      iMod (bor_fake with "LFT H†"). done. by iApply bor_share.
-  Qed.
-
-  Lemma frac_bor_atomic_acc E κ φ :
-    ↑lftN ⊆ E →
-    lft_ctx -∗ &frac{κ}φ ={E,E∖↑lftN}=∗ (∃ q, ▷ φ q ∗ (▷ φ q ={E∖↑lftN,E}=∗ True))
-                                      ∨ [†κ] ∗ |={E∖↑lftN,E}=> True.
-  Proof.
-    iIntros (?) "#LFT #Hφ". iDestruct "Hφ" as (γ κ') "[Hκκ' Hshr]".
-    iMod (shr_bor_acc with "LFT Hshr") as "[[Hφ Hclose]|[H† Hclose]]". done.
-    - iLeft. iDestruct "Hφ" as (q) "(Hφ & Hγ & H)". iExists q. iFrame.
-      iIntros "!>Hφ". iApply "Hclose". iExists q. iFrame.
-    - iRight. iMod "Hclose" as "_". iMod (lft_incl_dead with "Hκκ' H†") as "$". done.
-      iApply fupd_intro_mask. set_solver. done.
-  Qed.
-
-  Lemma frac_bor_acc' E q κ Φ:
-    ↑lftN ⊆ E →
-    lft_ctx -∗ □ (∀ q1 q2, Φ (q1+q2)%Qp ↔ Φ q1 ∗ Φ q2) -∗
-    &frac{κ}Φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ Φ q' ∗ (▷ Φ q' ={E}=∗ q.[κ]).
-  Proof.
-    iIntros (?) "#LFT #HΦ Hfrac Hκ". unfold frac_bor.
-    iDestruct "Hfrac" as (γ κ') "#[#Hκκ' Hshr]".
-    iMod (lft_incl_acc with "Hκκ' Hκ") as (qκ') "[[Hκ1 Hκ2] Hclose]". done.
-    iMod (shr_bor_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']". done.
-    iDestruct "H" as (qΦ) "(HΦqΦ & >Hown & Hq)".
-    destruct (Qp_lower_bound (qκ'/2) (qΦ/2)) as (qq & qκ'0 & qΦ0 & Hqκ' & HqΦ).
-    iExists qq.
-    iAssert (▷ Φ qq ∗ ▷ Φ (qΦ0 + qΦ / 2))%Qp%I with "[HΦqΦ]" as "[$ HqΦ]".
-    { iNext. rewrite -{1}(Qp_div_2 qΦ) {1}HqΦ. iApply "HΦ". by rewrite assoc. }
-    rewrite -{1}(Qp_div_2 qΦ) {1}HqΦ -assoc {1}Hqκ'.
-    iDestruct "Hκ2" as "[Hκq Hκqκ0]". iDestruct "Hown" as "[Hownq Hown]".
-    iMod ("Hclose'" with "[HqΦ Hq Hown Hκq]") as "Hκ1".
-    { iNext. iExists _. iFrame. iRight. iDestruct "Hq" as "[%|Hq]".
-      - subst. iExists qq. iIntros "{$Hκq}!%".
-        by rewrite (comm _ qΦ0) -assoc (comm _ qΦ0) -HqΦ Qp_div_2.
-      - iDestruct "Hq" as (q') "[% Hq'κ]". iExists (qq + q')%Qp.
-        iIntros "{$Hκq $Hq'κ}!%". by rewrite assoc (comm _ _ qq) assoc -HqΦ Qp_div_2. }
-    clear HqΦ qΦ qΦ0. iIntros "!>HqΦ".
-    iMod (shr_bor_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']". done.
-    iDestruct "H" as (qΦ) "(HΦqΦ & >Hown & >[%|Hq])".
-    { subst. iCombine "Hown" "Hownq" as "Hown".
-      by iDestruct (own_valid with "Hown") as %Hval%Qp_not_plus_q_ge_1. }
-    iDestruct "Hq" as (q') "[HqΦq' Hq'κ]". iCombine "Hown" "Hownq" as "Hown".
-    iDestruct (own_valid with "Hown") as %Hval. iDestruct "HqΦq'" as %HqΦq'.
-    assert (0 < q'-qq ∨ qq = q')%Qc as [Hq'q|<-].
-    { change (qΦ + qq ≤ 1)%Qc in Hval. apply Qp_eq in HqΦq'. simpl in Hval, HqΦq'.
-      rewrite <-HqΦq', <-Qcplus_le_mono_l in Hval. apply Qcle_lt_or_eq in Hval.
-      destruct Hval as [Hval|Hval].
-      by left; apply ->Qclt_minus_iff. right; apply Qp_eq, Qc_is_canon. by rewrite Hval. }
-    - assert (q' = mk_Qp _ Hq'q + qq)%Qp as ->. { apply Qp_eq. simpl. ring. }
-      iDestruct "Hq'κ" as "[Hq'qκ Hqκ]".
-      iMod ("Hclose'" with "[HqΦ HΦqΦ Hown Hq'qκ]") as "Hqκ2".
-      { iNext. iExists (qΦ + qq)%Qp. iFrame. iSplitR "Hq'qκ". by iApply "HΦ"; iFrame.
-        iRight. iExists _. iIntros "{$Hq'qκ}!%".
-        revert HqΦq'. rewrite !Qp_eq. move=>/=<-. ring. }
-      iApply "Hclose". iFrame. rewrite Hqκ'. by iFrame.
-    - iMod ("Hclose'" with "[HqΦ HΦqΦ Hown]") as "Hqκ2".
-      { iNext. iExists (qΦ ⋅ qq)%Qp. iFrame. iSplitL. by iApply "HΦ"; iFrame. auto. }
-      iApply "Hclose". iFrame. rewrite Hqκ'. by iFrame.
-  Qed.
-
-  Lemma frac_bor_acc E q κ `{Fractional _ Φ} :
-    ↑lftN ⊆ E →
-    lft_ctx -∗ &frac{κ}Φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ Φ q' ∗ (▷ Φ q' ={E}=∗ q.[κ]).
-  Proof.
-    iIntros (?) "LFT". iApply (frac_bor_acc' with "LFT"). done.
-    iIntros "!#*". rewrite fractional. iSplit; auto.
-  Qed.
-
-  Lemma frac_bor_shorten κ κ' Φ: κ ⊑ κ' -∗ &frac{κ'}Φ -∗ &frac{κ}Φ.
-  Proof.
-    iIntros "Hκκ' H". iDestruct "H" as (γ κ0) "[#H⊑ ?]". iExists γ, κ0. iFrame.
-    iApply (lft_incl_trans with "Hκκ' []"). auto.
-  Qed.
-
-  Lemma frac_bor_incl κ κ' q:
-    lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
-  Proof.
-    iIntros "#LFT#Hbor!#". iSplitR.
-    - iIntros (q') "Hκ'".
-      iMod (frac_bor_acc with "LFT Hbor Hκ'") as (q'') "[>? Hclose]". done.
-      iExists _. iFrame. iIntros "!>Hκ'". iApply "Hclose". auto.
-    - iIntros "H†'".
-      iMod (frac_bor_atomic_acc with "LFT Hbor") as "[H|[$ $]]". done.
-      iDestruct "H" as (q') "[>Hκ' _]".
-      iDestruct (lft_tok_dead with "Hκ' H†'") as "[]".
-  Qed.
-
-End frac_bor.
-
-Typeclasses Opaque frac_bor.

theories/lifetime/reborrow.v

-From lrust.lifetime Require Export borrow derived.
-From lrust.lifetime Require Import raw_reborrow accessors.
-From iris.algebra Require Import csum auth frac gmap dec_agree gset.
-From iris.base_logic Require Import big_op.
-From iris.base_logic.lib Require Import boxes.
-From iris.proofmode Require Import tactics.
-
-Section reborrow.
-Context `{invG Σ, lftG Σ}.
-Implicit Types κ : lft.
-
-Lemma rebor E κ κ' P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
-Proof.
-  iIntros (?) "#LFT #H⊑". rewrite {1}/bor; iDestruct 1 as (κ'') "[#H⊑' Hκ'']".
-  iMod (raw_rebor _ _ (κ' ∪ κ'') with "LFT Hκ''") as "[Hκ'' Hclose]"; first done.
-  { apply gmultiset_union_subseteq_r. }
-  iModIntro. iSplitL "Hκ''".
-  - rewrite /bor. iExists (κ' ∪ κ''). iFrame "Hκ''".
-    iApply (lft_incl_glb with "[]"); first iApply lft_incl_refl.
-    by iApply (lft_incl_trans with "H⊑").
-  - iIntros "Hκ†". iMod ("Hclose" with "[Hκ†]") as "Hκ''".
-    { iApply lft_dead_or; auto. }
-    iModIntro. rewrite /bor. eauto. 
-Qed.
-
-Lemma bor_unnest E κ κ' P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ∪ κ'} P.
-Proof.
-  iIntros (?) "#LFT Hκ". rewrite {2}/bor.
-  iMod (bor_exists with "LFT Hκ") as (κ0) "Hκ"; first done.
-  iMod (bor_sep with "LFT Hκ") as "[Hκ⊑ Hκ]"; first done.
-  rewrite {2}/bor; iDestruct "Hκ" as (κ0') "[#Hκ'⊑ Hκ]".
-  iMod (bor_acc_atomic with "LFT Hκ⊑") as "[[#Hκ⊑ Hclose]|[#H† Hclose]]"; first done; last first.
-  { iModIntro. iNext. iMod "Hclose" as "_". iApply (bor_fake with "LFT"); first done.
-    iApply lft_dead_or. iRight. done. }
-  iMod ("Hclose" with "Hκ⊑") as "_".
-  set (κ'' := κ0 ∪ κ0').
-  iMod (raw_rebor _ _ κ'' with "LFT Hκ") as "[Hκ _]"; first done.
-  { apply gmultiset_union_subseteq_r. }
-  iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  iMod (ilft_create _ _ κ'' with "HA HI Hinv") as (A' I') "(% & HA & HI & Hinv)".
-  clear A I; rename A' into A; rename I' into I.
-  iDestruct (big_sepS_delete _ _ κ'' with "Hinv") as "[Hκ'' Hinv]";
-    first by apply elem_of_dom.
-  rewrite {1}/lft_inv; iDestruct "Hκ''" as "[[Hinv' >%]|[Hdead >Hdeadin]]"; last first.
-  { iDestruct "Hdeadin" as %Hdeadin. iMod (lft_dead_in_tok with "HA") as "[HA #H†]"; first done.
-    iMod ("Hclose" with "[-]") as "_".
-    { rewrite /lfts_inv. iExists A, I. iFrame "HA HI".
-      iApply (big_sepS_delete _ _ κ''); first by apply elem_of_dom.
-      iNext; iFrame "Hinv". rewrite /lft_inv. iRight. iSplit; auto. }
-    iMod (fupd_intro_mask') as "Hclose"; last iModIntro; first solve_ndisj.
-    iNext. iMod "Hclose" as "_".
-    iApply (bor_fake with "LFT >"); first done.
-    iApply (lft_incl_dead with "[] H†"); first done.
-    by iApply (lft_incl_mono with "Hκ⊑"). }
-  rewrite {1}/raw_bor /idx_bor_own /=; iDestruct "Hκ" as (i) "[Hi #Hislice]".
-  rewrite lft_inv_alive_unfold;
-    iDestruct "Hinv'" as (Pb Pi) "(Halive & Hvs & Hinh)".
-  rewrite /lft_bor_alive; iDestruct "Halive" as (B) "(Hbox & >HB● & HB)".
-  iDestruct (own_bor_valid_2 with "HB● Hi")
-    as %[HB%to_borUR_included _]%auth_valid_discrete_2.
-  iMod (slice_delete_full _ _ true with "Hislice Hbox") as (Pb') "(HP & #EQ & Hbox)"; first solve_ndisj.
-  {  by rewrite lookup_fmap HB. }
-  iMod (own_bor_update_2 with "HB● Hi") as "HB●".
-  { apply auth_update_dealloc, delete_singleton_local_update. apply _. }
-  iMod (fupd_intro_mask') as "Hclose'"; last iModIntro; first solve_ndisj.
-  iNext. iMod "Hclose'" as "_".
-  iAssert (lft_bor_alive κ'' Pb') with "[Hbox HB● HB]" as "Halive".
-  { rewrite /lft_bor_alive. iExists (delete i B).
-    rewrite fmap_delete. iFrame "Hbox". iSplitL "HB●".
-    - rewrite /to_borUR fmap_delete. done.
-    - rewrite big_sepM_delete; last done. iDestruct "HB" as "[_ $]". }
-  iMod (raw_bor_unnest' _ false with "[$HI $Hinv] HP Halive [Hvs]") as (Pb'') "([HI Hinv] & HP & Halive & Hvs)";
-    [solve_ndisj|exact: gmultiset_union_subseteq_l|done| |].
-  { (* TODO: Use iRewrite supporting cotnractive rewriting. *)
-    iApply (lft_vs_cons with "[]"); last done.
-     iIntros "[$ Hbor]". iModIntro. iNext. by iRewrite "EQ". }
-  iMod ("Hclose" with "[-HP]") as "_".
-  { iNext. simpl. rewrite /lfts_inv. iExists A, I. iFrame.
-    rewrite (big_sepS_delete _ (dom _ I) κ''); last by apply elem_of_dom.
-    iFrame. rewrite /lft_inv lft_inv_alive_unfold. iLeft.
-    iFrame "%". iExists Pb'', Pi. iFrame. }
-  iModIntro. rewrite /bor. iExists κ''. iFrame. subst κ''.
-  by iApply (lft_incl_mono with "Hκ⊑").
-Qed.
-
-End reborrow.

theories/lifetime/shr_borrow.v

-From iris.algebra Require Import gmap auth frac.
-From iris.proofmode Require Import tactics.
-From lrust.lifetime Require Export derived.
-
-(** Shared bors  *)
-Definition shr_bor `{invG Σ, lftG Σ} κ (P : iProp Σ) :=
-  (∃ i, &{κ,i}P ∗ inv lftN (∃ q, idx_bor_own q i))%I.
-Notation "&shr{ κ } P" := (shr_bor κ P)
-  (format "&shr{ κ } P", at level 20, right associativity) : uPred_scope.
-
-Section shared_bors.
-  Context `{invG Σ, lftG Σ} (P : iProp Σ).
-
-  Global Instance shr_bor_proper :
-    Proper ((⊣⊢) ==> (⊣⊢)) (shr_bor κ).
-  Proof. solve_proper. Qed.
-  Global Instance shr_bor_persistent : PersistentP (&shr{κ} P) := _.
-
-  Lemma bor_share E κ : ↑lftN ⊆ E → &{κ}P ={E}=∗ &shr{κ}P.
-  Proof.
-    iIntros (?) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "(#?&Hown)".
-    iExists i. iFrame "#". iApply inv_alloc. auto.
-  Qed.
-
-  Lemma shr_bor_acc E κ :
-    ↑lftN ⊆ E →
-    lft_ctx -∗ &shr{κ}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
-               [†κ] ∗ |={E∖↑lftN,E}=> True.
-  Proof.
-    iIntros (?) "#LFT #HP". iDestruct "HP" as (i) "(#Hidx&#Hinv)".
-    iInv lftN as (q') ">[Hq'0 Hq'1]" "Hclose".
-    iMod ("Hclose" with "[Hq'1]") as "_". by eauto.
-    iMod (idx_bor_atomic_acc with "LFT Hidx Hq'0") as "[[HP Hclose]|[H† Hclose]]". done.
-    - iLeft. iFrame. iIntros "!>HP". by iMod ("Hclose" with "HP").
-    - iRight. iFrame. iIntros "!>". by iMod "Hclose".
-  Qed.
-
-  Lemma shr_bor_acc_tok E q κ :
-    ↑lftN ⊆ E →
-    lft_ctx -∗ &shr{κ}P -∗ q.[κ] ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ q.[κ]).
-  Proof.
-    iIntros (?) "#LFT #Hshr Hκ".
-    iMod (shr_bor_acc with "LFT Hshr") as "[[$ Hclose]|[H† _]]". done.
-    - iIntros "!>HP". by iMod ("Hclose" with "HP").
-    - iDestruct (lft_tok_dead with "Hκ H†") as "[]".
-  Qed.
-
-  Lemma shr_bor_shorten κ κ': κ ⊑ κ' -∗ &shr{κ'}P -∗ &shr{κ}P.
-  Proof.
-    iIntros "#H⊑ H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
-      by iApply (idx_bor_shorten with "H⊑").
-  Qed.
-
-End shared_bors.
-
-Typeclasses Opaque shr_bor.

theories/typing/bool.v

-From iris.proofmode Require Import tactics.
-From lrust.typing Require Export type.
-From lrust.typing Require Import typing perm.
-
-Section bool.
-  Context `{typeG Σ}.
-
-  Program Definition bool : type :=
-    {| st_size := 1; st_own tid vl := (∃ z:bool, ⌜vl = [ #z ]⌝)%I |}.
-  Next Obligation. iIntros (tid vl) "H". iDestruct "H" as (z) "%". by subst. Qed.
-
-  Lemma typed_bool ρ (b:Datatypes.bool): typed_step_ty ρ #b bool.
-  Proof. iIntros (tid) "!#(_&_&_&$)". wp_value. by iExists _. Qed.
-
-  Lemma typed_if ρ e1 e2 ν:
-    typed_program ρ e1 → typed_program ρ e2 →
-    typed_program (ρ ∗ ν ◁ bool) (if: ν then e1 else e2).
-  Proof.
-    iIntros (He1 He2 tid) "!#(#HEAP & #LFT & [Hρ H◁] & Htl)".
-    wp_bind ν. iApply (has_type_wp with "H◁"). iIntros (v) "% H◁!>".
-    rewrite has_type_value. iDestruct "H◁" as (b) "Heq". iDestruct "Heq" as %[= ->].
-    wp_if. destruct b; iNext. iApply He1; iFrame "∗#". iApply He2; iFrame "∗#".
-  Qed.
-End bool.
\ No newline at end of file

theories/typing/function.v

-From iris.proofmode Require Import tactics.
-From iris.program_logic Require Import hoare.
-From lrust.lifetime Require Import borrow.
-From lrust.typing Require Export type.
-From lrust.typing Require Import type_incl typing.
-
-Section fn.
-  Context `{typeG Σ}.
-
-  Program Definition cont {n : nat} (ρ : vec val n → @perm Σ) :=
-    {| ty_size := 1;
-       ty_own tid vl := (∃ f, ⌜vl = [f]⌝ ∗
-          ∀ vl, ρ vl tid -∗ na_own tid ⊤
-                 -∗ WP f (map of_val vl) {{λ _, False}})%I;
-       ty_shr κ tid N l := True%I |}.
-  Next Obligation.
-    iIntros (n ρ tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
-  Qed.
-  Next Obligation. intros. by iIntros "_ _ $". Qed.
-  Next Obligation. intros. by iIntros "_ _ _". Qed.
-
-  (* TODO : For now, functions are not Send. This means they cannot be
-     called in another thread than the one that created it.  We will
-     need Send functions when dealing with multithreading ([fork]
-     needs a Send closure). *)
-  Program Definition fn {A n} (ρ : A -> vec val n → @perm Σ) : type :=
-    {| st_size := 1;
-       st_own tid vl := (∃ f, ⌜vl = [f]⌝ ∗ ∀ x vl,
-         {{ ρ x vl tid ∗ na_own tid ⊤ }} f (map of_val vl) {{λ _, False}})%I |}.
-  Next Obligation.
-    iIntros (x n ρ tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
-  Qed.
-
-  Lemma ty_incl_cont {n} ρ ρ1 ρ2 :
-    Duplicable ρ → (∀ vl : vec val n, ρ ∗ ρ2 vl ⇒ ρ1 vl) →
-    ty_incl ρ (cont ρ1) (cont ρ2).
-  Proof.
-    iIntros (? Hρ1ρ2 tid) "#LFT #Hρ!>". iSplit; iIntros "!#*H"; last by auto.
-    iDestruct "H" as (f) "[% Hwp]". subst. iExists _. iSplit. done.
-    iIntros (vl) "Hρ2 Htl". iApply ("Hwp" with ">[-Htl] Htl").
-    iApply (Hρ1ρ2 with "LFT"). by iFrame.
-  Qed.
-
-  Lemma ty_incl_fn {A n} ρ ρ1 ρ2 :
-    Duplicable ρ → (∀ (x : A) (vl : vec val n), ρ ∗ ρ2 x vl ⇒ ρ1 x vl) →
-    ty_incl ρ (fn ρ1) (fn ρ2).
-  Proof.
-    iIntros (? Hρ1ρ2 tid) "#LFT #Hρ!>". iSplit; iIntros "!#*#H".
-    - iDestruct "H" as (f) "[% Hwp]". subst. iExists _. iSplit. done.
-      iIntros (x vl) "!#[Hρ2 Htl]". iApply ("Hwp" with ">").
-      iFrame. iApply (Hρ1ρ2 with "LFT"). by iFrame.
-    - iSplit; last done. simpl. iDestruct "H" as (vl0) "[? Hvl]".
-      iExists vl0. iFrame "#". iNext. iDestruct "Hvl" as (f) "[% Hwp]".
-      iExists f. iSplit. done. iIntros (x vl) "!#[Hρ2 Htl]".
-      iApply ("Hwp" with ">"). iFrame. iApply (Hρ1ρ2 with "LFT >"). by iFrame.
-  Qed.
-
-  Lemma ty_incl_fn_cont {A n} ρ ρf (x : A) :
-    ty_incl ρ (fn ρf) (cont (n:=n) (ρf x)).
-  Proof.
-    iIntros (tid) "#LFT _!>". iSplit; iIntros "!#*H"; last by iSplit.
-    iDestruct "H" as (f) "[%#H]". subst. iExists _. iSplit. done.
-    iIntros (vl) "Hρf Htl". iApply "H". by iFrame.
-  Qed.
-
-  Lemma ty_incl_fn_specialize {A B n} (f : A → B) ρ ρfn :
-    ty_incl ρ (fn (n:=n) ρfn) (fn (ρfn ∘ f)).
-  Proof.
-    iIntros (tid) "_ _!>". iSplit; iIntros "!#*H".
-    - iDestruct "H" as (fv) "[%#H]". subst. iExists _. iSplit. done.
-      iIntros (x vl). by iApply "H".
-    - iSplit; last done.
-      iDestruct "H" as (fvl) "[?Hown]". iExists _. iFrame. iNext.
-      iDestruct "Hown" as (fv) "[%H]". subst. iExists _. iSplit. done.
-      iIntros (x vl). by iApply "H".
-  Qed.
-
-  Lemma typed_fn {A n} `{Duplicable _ ρ, Closed (f :b: xl +b+ []) e} θ :
-    length xl = n →
-    (∀ (a : A) (vl : vec val n) (fv : val) e',
-        subst_l xl (map of_val vl) e = Some e' →
-        typed_program (fv ◁ fn θ ∗ (θ a vl) ∗ ρ) (subst' f fv e')) →
-    typed_step_ty ρ (Rec f xl e) (fn θ).
-  Proof.
-    iIntros (Hn He tid) "!#(#HEAP&#LFT&#Hρ&$)".
-    assert (Rec f xl e = RecV f xl e) as -> by done. iApply wp_value'.
-    rewrite has_type_value.
-    iLöb as "IH". iExists _. iSplit. done. iIntros (a vl) "!#[Hθ?]".
-    assert (is_Some (subst_l xl (map of_val vl) e)) as [e' He'].
-    { clear -Hn. revert xl Hn e. induction vl=>-[|x xl] //=. by eauto.
-      intros ? e. edestruct IHvl as [e' ->]. congruence. eauto. }
-    iApply wp_rec; try done.
-    { apply List.Forall_forall=>?. rewrite in_map_iff=>-[?[<- _]].
-      rewrite to_of_val. eauto. }
-    iNext. iApply He. done. iFrame "∗#". by rewrite has_type_value.
-  Qed.
-
-  Lemma typed_cont {n} `{Closed (f :b: xl +b+ []) e} ρ θ :
-    length xl = n →
-    (∀ (fv : val) (vl : vec val n) e',
-        subst_l xl (map of_val vl) e = Some e' →
-        typed_program (fv ◁ cont (λ vl, ρ ∗ θ vl)%P ∗ (θ vl) ∗ ρ) (subst' f fv e')) →
-    typed_step_ty ρ (Rec f xl e) (cont θ).
-  Proof.
-    iIntros (Hn He tid) "!#(#HEAP&#LFT&Hρ&$)". specialize (He (RecV f xl e)).
-    assert (Rec f xl e = RecV f xl e) as -> by done. iApply wp_value'.
-    rewrite has_type_value.
-    iLöb as "IH". iExists _. iSplit. done. iIntros (vl) "Hθ ?".
-    assert (is_Some (subst_l xl (map of_val vl) e)) as [e' He'].
-    { clear -Hn. revert xl Hn e. induction vl=>-[|x xl] //=. by eauto.
-      intros ? e. edestruct IHvl as [e' ->]. congruence. eauto. }
-    iApply wp_rec; try done.
-    { apply List.Forall_forall=>?. rewrite in_map_iff=>-[?[<- _]].
-      rewrite to_of_val. eauto. }
-    iNext. iApply He. done. iFrame "∗#". rewrite has_type_value.
-    iExists _. iSplit. done. iIntros (vl') "[Hρ Hθ] Htl".
-    iDestruct ("IH" with "Hρ") as (f') "[Hf' IH']".
-    iDestruct "Hf'" as %[=<-]. iApply ("IH'" with "Hθ Htl").
-  Qed.
-
-End fn.

theories/typing/int.v

-From iris.proofmode Require Import tactics.
-From lrust.typing Require Export type.
-From lrust.typing Require Import typing bool perm.
-
-Section int.
-  Context `{typeG Σ}.
-
-  Program Definition int : type :=
-    {| st_size := 1; st_own tid vl := (∃ z:Z, ⌜vl = [ #z ]⌝)%I |}.
-  Next Obligation. iIntros (tid vl) "H". iDestruct "H" as (z) "%". by subst. Qed.
-
-  Lemma typed_int ρ (z:Datatypes.nat) :
-    typed_step_ty ρ #z int.
-  Proof. iIntros (tid) "!#(_&_&_&$)". wp_value. by iExists _. Qed.
-
-  Lemma typed_plus e1 e2 ρ1 ρ2:
-    typed_step_ty ρ1 e1 int → typed_step_ty ρ2 e2 int →
-    typed_step_ty (ρ1 ∗ ρ2) (e1 + e2) int.
-  Proof.
-    unfold typed_step_ty, typed_step. setoid_rewrite has_type_value.
-    iIntros (He1 He2 tid) "!#(#HEAP&#ĽFT&[H1 H2]&?)".
-    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply He1; iFrame "∗#".
-    iIntros (v1) "[Hv1?]". iDestruct "Hv1" as (z1) "Hz1". iDestruct "Hz1" as %[=->].
-    wp_bind e2. iApply wp_wand_r. iSplitL. iApply He2; iFrame "∗#".
-    iIntros (v2) "[Hv2$]". iDestruct "Hv2" as (z2) "Hz2". iDestruct "Hz2" as %[=->].
-    wp_op. by iExists _.
-  Qed.
-
-  Lemma typed_minus e1 e2 ρ1 ρ2:
-    typed_step_ty ρ1 e1 int → typed_step_ty ρ2 e2 int →
-    typed_step_ty (ρ1 ∗ ρ2) (e1 - e2) int.
-  Proof.
-    unfold typed_step_ty, typed_step. setoid_rewrite has_type_value.
-    iIntros (He1 He2 tid) "!#(#HEAP&#LFT&[H1 H2]&?)".
-    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply He1; iFrame "∗#".
-    iIntros (v1) "[Hv1?]". iDestruct "Hv1" as (z1) "Hz1". iDestruct "Hz1" as %[=->].
-    wp_bind e2. iApply wp_wand_r. iSplitL. iApply He2; iFrame "∗#".
-    iIntros (v2) "[Hv2$]". iDestruct "Hv2" as (z2) "Hz2". iDestruct "Hz2" as %[=->].
-    wp_op. by iExists _.
-  Qed.
-
-  Lemma typed_le e1 e2 ρ1 ρ2:
-    typed_step_ty ρ1 e1 int → typed_step_ty ρ2 e2 int →
-    typed_step_ty (ρ1 ∗ ρ2) (e1 ≤ e2) bool.
-  Proof.
-    unfold typed_step_ty, typed_step. setoid_rewrite has_type_value.
-    iIntros (He1 He2 tid) "!#(#HEAP&#LFT&[H1 H2]&?)".
-    wp_bind e1. iApply wp_wand_r. iSplitR "H2". iApply He1; iFrame "∗#".
-    iIntros (v1) "[Hv1?]". iDestruct "Hv1" as (z1) "Hz1". iDestruct "Hz1" as %[=->].
-    wp_bind e2. iApply wp_wand_r. iSplitL. iApply He2; iFrame "∗#".
-    iIntros (v2) "[Hv2$]". iDestruct "Hv2" as (z2) "Hz2". iDestruct "Hz2" as %[=->].
-    wp_op; intros _; by iExists _.
-  Qed.
-End int.
\ No newline at end of file

theories/typing/lft_contexts.v

-From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import big_op.
-From iris.base_logic.lib Require Import fractional.
-From lrust.lifetime Require Export derived.
-
-Section lft_contexts.
-  Context `{invG Σ, lftG Σ}.
-  Implicit Type (κ : lft).
-
-  (* External lifetime contexts. *)
-
-  Inductive lectx_elt : Type :=
-  | LECtx_Alive κ
-  | LECtx_Incl κ κ'.
-  Definition lectx := list lectx_elt.
-
-  Definition lectx_elt_interp (x : lectx_elt) (q : Qp) : iProp Σ :=
-    match x with
-    | LECtx_Alive κ => q.[κ]
-    | LECtx_Incl κ κ' => κ ⊑ κ'
-    end%I.
-  Global Instance lectx_elt_interp_fractional x:
-    Fractional (lectx_elt_interp x).
-  Proof. destruct x; unfold lectx_elt_interp; apply _. Qed.
-  Typeclasses Opaque lectx_elt_interp.
-
-  Definition lectx_interp (E : lectx) (q : Qp) : iProp Σ :=
-    ([∗ list] x ∈ E, lectx_elt_interp x q)%I.
-  Global Instance lectx_interp_fractional E:
-    Fractional (lectx_interp E).
-  Proof. intros ??. rewrite -big_sepL_sepL. by setoid_rewrite <-fractional. Qed.
-  Global Instance lectx_interp_as_fractional E q:
-    AsFractional (lectx_interp E q) (lectx_interp E) q.
-  Proof. done. Qed.
-  Global Instance lectx_interp_permut:
-    Proper ((≡ₚ) ==> eq ==> (⊣⊢)) lectx_interp.
-  Proof. intros ????? ->. by apply big_opL_permutation. Qed.
-  Typeclasses Opaque lectx_interp.
-
-  (* Local lifetime contexts. *)
-
-  Definition llctx_elt : Type := lft * list lft.
-  Definition llctx := list llctx_elt.
-
-  Definition llctx_elt_interp (x : llctx_elt) (q : Qp) : iProp Σ :=
-    let κ' := foldr (∪) static (x.2) in
-    (∃ κ0, ⌜x.1 = κ' ∪ κ0⌝ ∗ q.[κ0] ∗ □ (1.[x.1] ={⊤,⊤∖↑lftN}▷=∗ [†x.1]))%I.
-  Global Instance llctx_elt_interp_fractional x :
-    Fractional (llctx_elt_interp x).
-  Proof.
-    destruct x as [κ κs]. iIntros (q q'). iSplit; iIntros "H".
-    - iDestruct "H" as (κ0) "(% & [Hq Hq'] & #?)".
-      iSplitL "Hq"; iExists _; by iFrame "∗%".
-    - iDestruct "H" as "[Hq Hq']".
-      iDestruct "Hq" as (κ0) "(% & Hq & #?)".
-      iDestruct "Hq'" as (κ0') "(% & Hq' & #?)". simpl in *.
-      rewrite (inj (union (foldr (∪) static κs)) κ0' κ0); last congruence.
-      iExists κ0. by iFrame "∗%".
-  Qed.
-  Typeclasses Opaque llctx_elt_interp.
-
-  Definition llctx_interp (L : llctx) (q : Qp) : iProp Σ :=
-    ([∗ list] x ∈ L, llctx_elt_interp x q)%I.
-  Global Instance llctx_interp_fractional L:
-    Fractional (llctx_interp L).
-  Proof. intros ??. rewrite -big_sepL_sepL. by setoid_rewrite <-fractional. Qed.
-  Global Instance llctx_interp_as_fractional L q:
-    AsFractional (llctx_interp L q) (llctx_interp L) q.
-  Proof. done. Qed.
-  Global Instance llctx_interp_permut:
-    Proper ((≡ₚ) ==> eq ==> (⊣⊢)) llctx_interp.
-  Proof. intros ????? ->. by apply big_opL_permutation. Qed.
-  Typeclasses Opaque llctx_interp.
-
-  Context (E : lectx) (L : llctx).
-
-  (* Lifetime inclusion *)
-
-  (* There does not seem to be a need in the type system for
-     "equivalence" of lifetimes. If so, TODO : add it, and the
-     corresponding [Proper] instances for the relevent types. *)
-  Definition incl κ κ' : Prop :=
-    ∀ qE qL, lectx_interp E qE -∗ llctx_interp L qL -∗ κ ⊑ κ'.
-
-  Global Instance incl_preorder : PreOrder incl.
-  Proof.
-    split.
-    - iIntros (???) "_ _". iApply lft_incl_refl.
-    - iIntros (??? H1 H2 ??) "HE HL". iApply (lft_incl_trans with "[#] [#]").
-      iApply (H1 with "HE HL"). iApply (H2 with "HE HL").
-  Qed.
-
-  Lemma incl_static κ : incl κ static.
-  Proof. iIntros (??) "_ _". iApply lft_incl_static. Qed.
-
-  Lemma incl_local κ κ' κs : (κ, κs) ∈ L → κ' ∈ κs → incl κ κ'.
-  Proof.
-    intros ? Hκ'κs ??. rewrite /llctx_interp /llctx_elt_interp big_sepL_elem_of //.
-    iIntros "_ H". iDestruct "H" as (κ0) "[H _]". simpl. iDestruct "H" as %->.
-    iApply lft_le_incl. etrans; last by apply gmultiset_union_subseteq_l.
-    clear -Hκ'κs. induction Hκ'κs.
-    - apply gmultiset_union_subseteq_l.
-    - etrans. done. apply gmultiset_union_subseteq_r.
-  Qed.
-
-  Lemma incl_external κ κ' : LECtx_Incl κ κ' ∈ E → incl κ κ'.
-  Proof.
-    intros ???. rewrite /lectx_interp /lectx_elt_interp big_sepL_elem_of //.
-      by iIntros "$ _".
-  Qed.
-
-  (* Lifetime aliveness *)
-
-  Definition alive (κ : lft) : Prop :=
-    ∀ F qE qL, ⌜↑lftN ⊆ F⌝ -∗ lectx_interp E qE -∗ llctx_interp L qL ={F}=∗
-          ∃ q', q'.[κ] ∗ (q'.[κ] ={F}=∗ lectx_interp E qE ∗ llctx_interp L qL).
-
-  Lemma alive_static : alive static.
-  Proof.
-    iIntros (F qE qL) "%$$". iExists 1%Qp. iSplitL. by iApply lft_tok_static. auto.
-  Qed.
-
-  Lemma alive_llctx κ κs: (κ, κs) ∈ L → Forall alive κs → alive κ.
-  Proof.
-    iIntros ([i HL]%elem_of_list_lookup_1 Hκs F qE qL) "% HE HL".
-    iDestruct "HL" as "[HL1 HL2]". rewrite {2}/llctx_interp /llctx_elt_interp.
-    iDestruct (big_sepL_lookup_acc with "HL2") as "[Hκ Hclose]". done.
-    iDestruct "Hκ" as (κ0) "(EQ & Htok & #Hend)". simpl. iDestruct "EQ" as %->.
-    iAssert (∃ q', q'.[foldr union static κs] ∗
-      (q'.[foldr union static κs] ={F}=∗ lectx_interp E qE ∗ llctx_interp L (qL / 2)))%I
-      with ">[HE HL1]" as "H".
-    { move:(qL/2)%Qp=>qL'. clear HL. iClear "Hend".
-      iInduction Hκs as [|κ κs Hκ ?] "IH" forall (qE qL').
-      - iExists 1%Qp. iFrame. iSplitR; last by auto. iApply lft_tok_static.
-      - iDestruct "HL1" as "[HL1 HL2]". iDestruct "HE" as "[HE1 HE2]".
-        iMod (Hκ with "* [%] HE1 HL1") as (q') "[Htok' Hclose]". done.
-        iMod ("IH" with "* HE2 HL2") as (q'') "[Htok'' Hclose']".
-        destruct (Qp_lower_bound q' q'') as (q0 & q'2 & q''2 & -> & ->).
-        iExists q0. rewrite -lft_tok_sep. iDestruct "Htok'" as "[$ Hr']".
-        iDestruct "Htok''" as "[$ Hr'']". iIntros "!>[Hκ Hfold]".
-        iMod ("Hclose" with "[$Hκ $Hr']") as "[$$]". iApply "Hclose'". iFrame. }
-    iDestruct "H" as (q') "[Htok' Hclose']". rewrite -{5}(Qp_div_2 qL).
-    destruct (Qp_lower_bound q' (qL/2)) as (q0 & q'2 & q''2 & -> & ->).
-    iExists q0. rewrite -(lft_tok_sep q0). iDestruct "Htok" as "[$ Htok]".
-    iDestruct "Htok'" as "[$ Htok']". iIntros "!>[Hfold Hκ0]".
-    iMod ("Hclose'" with "[$Hfold $Htok']") as "[$$]".
-    rewrite /llctx_interp /llctx_elt_interp. iApply "Hclose". iExists κ0. iFrame. auto.
-  Qed.
-
-  Lemma alive_lectx κ: LECtx_Alive κ ∈ E → alive κ.
-  Proof.
-    iIntros ([i HE]%elem_of_list_lookup_1 F qE qL) "% HE $ !>".
-    rewrite /lectx_interp /lectx_elt_interp.
-    iDestruct (big_sepL_lookup_acc with "HE") as "[Hκ Hclose]". done.
-    iExists qE. iFrame. iIntros "?!>". by iApply "Hclose".
-  Qed.
-
-  Lemma alive_incl κ κ': alive κ → incl κ κ' → alive κ'.
-  Proof.
-    iIntros (Hal Hinc F qE qL) "% HE HL".
-    iAssert (κ ⊑ κ')%I with "[#]" as "#Hincl". by iApply (Hinc with "HE HL").
-    iMod (Hal with "[%] HE HL") as (q') "[Htok Hclose]". done.
-    iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose']". done.
-    iExists q''. iIntros "{$Htok}!>Htok". iApply ("Hclose" with ">").
-    by iApply "Hclose'".
-  Qed.
-
-  (* External lifetime context satisfiability *)
-
-  Definition lectx_sat E' : Prop :=
-    ∀ qE qL F, ⌜↑lftN ⊆ F⌝ -∗ lectx_interp E qE -∗ llctx_interp L qL ={F}=∗
-      ∃ qE', lectx_interp E' qE' ∗
-       (lectx_interp E' qE' ={F}=∗ lectx_interp E qE ∗ llctx_interp L qL).
-
-  Lemma lectx_sat_nil : lectx_sat [].
-  Proof.
-    iIntros (qE qL F) "%$$". iExists 1%Qp. rewrite /lectx_interp big_sepL_nil. auto.
-  Qed.
-
-  Lemma lectx_sat_alive E' κ :
-    alive κ → lectx_sat E' → lectx_sat (LECtx_Alive κ :: E').
-  Proof.
-    iIntros (Hκ HE' qE qL F) "% [HE1 HE2] [HL1 HL2]".
-    iMod (Hκ with "[%] HE1 HL1") as (q) "[Htok Hclose]". done.
-    iMod (HE' with "[%] HE2 HL2") as (q') "[HE' Hclose']". done.
-    destruct (Qp_lower_bound q q') as (q0 & q2 & q'2 & -> & ->). iExists q0.
-    rewrite {5 6}/lectx_interp big_sepL_cons /=.
-    iDestruct "Htok" as "[$ Htok]". iDestruct "HE'" as "[Hf HE']".
-    iSplitL "Hf". by rewrite /lectx_interp.
-    iIntros "!>[Htok' ?]". iMod ("Hclose" with "[$Htok $Htok']") as "[$$]".
-    iApply "Hclose'". iFrame. by rewrite /lectx_interp.
-  Qed.
-
-  Lemma lectx_sat_incl E' κ κ' :
-    incl κ κ' → lectx_sat E' → lectx_sat (LECtx_Incl κ κ' :: E').
-  Proof.
-    iIntros (Hκκ' HE' qE qL F) "% HE HL".
-    iAssert (κ ⊑ κ')%I with "[#]" as "#Hincl". by iApply (Hκκ' with "HE HL").
-    iMod (HE' with "[%] HE HL") as (q) "[HE' Hclose']". done.
-    iExists q. rewrite {1 2 4 5}/lectx_interp big_sepL_cons /=.
-    iIntros "{$Hincl $HE'}!>[_ ?]". by iApply "Hclose'".
-  Qed.
-End lft_contexts.
\ No newline at end of file

theories/typing/own.v

-From Coq Require Import Qcanon.
-From iris.proofmode Require Import tactics.
-From lrust.lifetime Require Import borrow frac_borrow.
-From lrust.lang Require Export new_delete.
-From lrust.lang Require Import heap.
-From lrust.typing Require Export type.
-From lrust.typing Require Import typing product perm.
-
-Section own.
-  Context `{typeG Σ}.
-
-  (* Even though it does not seem too natural to put this here, it is
-     the only place where it is used. *)
-  Program Definition uninit : type :=
-    {| st_size := 1; st_own tid vl := ⌜length vl = 1%nat⌝%I |}.
-  Next Obligation. done. Qed.
-
-  Program Definition freeable_sz (n : nat) (sz : nat) (l : loc) : iProp Σ :=
-    match sz, n return _ with
-    | 0%nat, _ => True
-    | _, 0%nat => False
-    | sz, n => †{mk_Qp (sz / n) _}l…sz
-    end%I.
-  Next Obligation. intros _ _ _ sz0 ? n ?. by apply Qcmult_pos_pos. Qed.
-  Global Instance freable_sz_timeless n sz l : TimelessP (freeable_sz n sz l).
-  Proof. destruct sz, n; apply _. Qed.
-
-  Lemma freeable_sz_full n l : freeable_sz n n l ⊣⊢ (†{1}l…n ∨ ⌜Z.of_nat n = 0⌝)%I.
-  Proof.
-    destruct n.
-    - iSplit; iIntros "H /="; auto.
-    - assert (Z.of_nat (S n) = 0 ↔ False) as -> by done. rewrite right_id.
-      rewrite /freeable_sz (proj2 (Qp_eq (mk_Qp _ _) 1)) //= Qcmult_inv_r //.
-  Qed.
-
-  Lemma freeable_sz_split n sz1 sz2 l :
-    freeable_sz n sz1 l ∗ freeable_sz n sz2 (shift_loc l sz1) ⊣⊢
-                freeable_sz n (sz1 + sz2) l.
-  Proof.
-    destruct sz1; [|destruct sz2;[|rewrite /freeable_sz plus_Sn_m; destruct n]].
-    - by rewrite left_id shift_loc_0.
-    - by rewrite right_id Nat.add_0_r.
-    - iSplit. by iIntros "[[]?]". by iIntros "[]".
-    - rewrite heap_freeable_op_eq. f_equiv. apply Qp_eq.
-      rewrite /= -Qcmult_plus_distr_l -Z2Qc_inj_add /Z.add. do 3 f_equal. lia.
-  Qed.
-
-  Program Definition own (n : nat) (ty : type) :=
-    {| ty_size := 1;
-       ty_own tid vl :=
-         (* We put a later in front of the †{q}, because we cannot use
-            [ty_size_eq] on [ty] at step index 0, which would in turn
-            prevent us to prove [subtype_own].
-
-            Since this assertion is timeless, this should not cause
-            problems. *)
-         (∃ l:loc, ⌜vl = [ #l ]⌝ ∗ ▷ l ↦∗: ty.(ty_own) tid ∗
-                   ▷ freeable_sz n ty.(ty_size) l)%I;
-       ty_shr κ tid E l :=
-         (∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
-            □ (∀ q' F, ⌜E ∪ mgmtE ⊆ F⌝ →
-                 q'.[κ] ={F,F∖E}▷=∗ ty.(ty_shr) κ tid E l' ∗ q'.[κ]))%I
-    |}.
-  Next Obligation.
-    iIntros (q ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
-  Qed.
-  Next Obligation.
-    move=> q ty E N κ l tid q' ?? /=. iIntros "#LFT Hshr Htok".
-    iMod (bor_exists with "LFT Hshr") as (vl) "Hb". set_solver.
-    iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]". set_solver.
-    iMod (bor_exists with "LFT Hb2") as (l') "Hb2". set_solver.
-    iMod (bor_sep with "LFT Hb2") as "[EQ Hb2]". set_solver.
-    iMod (bor_persistent with "LFT EQ Htok") as "[>% $]". set_solver. subst.
-    rewrite heap_mapsto_vec_singleton.
-    iMod (bor_sep with "LFT Hb2") as "[Hb2 _]". set_solver.
-    iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "Hbf". set_solver.
-    rewrite bor_unfold_idx. iDestruct "Hb2" as (i) "(#Hpb&Hpbown)".
-    iMod (inv_alloc N _ (idx_bor_own 1 i ∨ ty_shr ty κ tid (↑N) l')%I
-         with "[Hpbown]") as "#Hinv"; first by eauto.
-    iExists l'. iIntros "!>{$Hbf}!#". iIntros (q'' F) "% Htok".
-    iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
-    iDestruct "INV" as "[>Hbtok|#Hshr]".
-    - iMod (bor_later_tok with "LFT [Hbtok] Htok") as "H". set_solver.
-      { rewrite bor_unfold_idx. eauto. }
-      iModIntro. iNext. iMod "H" as "[Hb Htok]".
-      iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]". done. set_solver.
-      iApply "Hclose". auto.
-    - iModIntro. iNext. iMod ("Hclose" with "[]") as "_"; by eauto.
-  Qed.
-  Next Obligation.
-    intros _ ty κ κ' tid E E' l ?. iIntros "#LFT #Hκ #H".
-    iDestruct "H" as (l') "[Hfb #Hvs]".
-    iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros "!#".
-    iIntros (q' F) "% Htok".
-    iApply (step_fupd_mask_mono F _ _ (F∖E)). set_solver. set_solver.
-    iMod (lft_incl_acc with "Hκ Htok") as (q'') "[Htok Hclose]". set_solver.
-    iMod ("Hvs" with "* [%] Htok") as "Hvs'". set_solver. iModIntro. iNext.
-    iMod "Hvs'" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
-      by iApply (ty.(ty_shr_mono) with "LFT Hκ").
-  Qed.
-
-  Global Instance own_mono E L n :
-    Proper (subtype E L ==> subtype E L) (own n).
-  Proof.
-    intros ty1 ty2 Hincl. split.
-    - done.
-    - iIntros (qE qL) "#LFT HE HL *".
-      iDestruct (Hincl.(subtype_own _ _ _ _) with "LFT HE HL") as "#Howni".
-      iIntros "{HE HL} !# * H". iDestruct "H" as (l) "(%&Hmt&H†)". subst.
-      iExists _. iSplit. done. iDestruct "Hmt" as (vl') "[Hmt Hown]". iNext.
-      iDestruct (ty_size_eq with "Hown") as %<-.
-      iDestruct ("Howni" with "* Hown") as "Hown".
-      iDestruct (ty_size_eq with "Hown") as %<-. iFrame.
-      iExists _. by iFrame.
-    - iIntros (qE qL) "#LFT HE HL *".
-      iDestruct (Hincl.(subtype_shr _ _ _ _) with "LFT HE HL") as "#Hshri".
-      iIntros "{HE HL} !# * H". iDestruct "H" as (l') "[Hfb #Hvs]".
-      iExists l'. iFrame. iIntros "!#". iIntros (q' F') "% Hκ".
-      iMod ("Hvs" with "* [%] Hκ") as "Hvs'". done. iModIntro. iNext.
-      iMod "Hvs'" as "[Hshr $]". iApply ("Hshri" with "* Hshr").
-  Qed.
-
-  Global Instance own_proper E L n :
-    Proper (eqtype E L ==> eqtype E L) (own n).
-  Proof. intros ?? Heq. split; f_equiv; apply Heq. Qed.
-
-  Lemma typed_new ρ (n : nat):
-    0 ≤ n → typed_step_ty ρ (new [ #n]%E) (own n (Π(replicate n uninit))).
-  Proof.
-    iIntros (Hn tid) "!#(#HEAP&_&_&$)". iApply (wp_new with "HEAP"); try done.
-    iIntros "!>*(% & H† & H↦)". iExists _. iSplit. done. iNext.
-    rewrite Nat2Z.id. iSplitR "H†".
-    - iExists vl. iFrame.
-      match goal with H : Z.of_nat n = Z.of_nat (length vl) |- _ => rename H into Hlen end.
-      clear Hn. apply (inj Z.of_nat) in Hlen. subst.
-      iInduction vl as [|v vl] "IH". done.
-      iExists [v], vl. iSplit. done. by iSplit.
-    - assert (ty_size (Π (replicate n uninit)) = n) as ->.
-      { clear. induction n; rewrite //= IHn //. }
-      by rewrite freeable_sz_full.
-  Qed.
-
-  Lemma typed_delete ty (ν : expr):
-    typed_step (ν ◁ own ty.(ty_size) ty) (delete [ #ty.(ty_size); ν])%E (λ _, top).
-  Proof.
-    iIntros (tid) "!#(#HEAP&_&H◁&$)". wp_bind ν.
-    iApply (has_type_wp with "[$H◁]"). iIntros (v) "_ H◁ !>".
-    rewrite has_type_value.
-    iDestruct "H◁" as (l) "(Hv & H↦∗: & >H†)". iDestruct "Hv" as %[=->].
-    iDestruct "H↦∗:" as (vl) "[>H↦ Hown]".
-    rewrite ty_size_eq. iDestruct "Hown" as ">Hown". iDestruct "Hown" as %<-.
-    iApply (wp_delete with "[-]"); try by auto.
-    rewrite freeable_sz_full. by iFrame.
-  Qed.
-
-  Lemma update_strong ty1 ty2 n:
-    ty1.(ty_size) = ty2.(ty_size) →
-    update ty1 (λ ν, ν ◁ own n ty2)%P (λ ν, ν ◁ own n ty1)%P.
-  Proof.
-    iIntros (Hsz ν tid Φ E ?) "_ H◁ HΦ". iApply (has_type_wp with "H◁").
-    iIntros (v) "Hνv H◁". iDestruct "Hνv" as %Hνv.
-    rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & H↦ & >H†)".
-    iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
-    rewrite ty2.(ty_size_eq) -Hsz. iDestruct "Hown" as ">%". iApply "HΦ". iFrame "∗%".
-    iIntros (vl') "[H↦ Hown']!>". rewrite /has_type Hνv.
-    iExists _. iSplit. done. iFrame. iExists _. iFrame.
-  Qed.
-
-  Lemma consumes_copy_own ty n:
-    Copy ty → consumes ty (λ ν, ν ◁ own n ty)%P (λ ν, ν ◁ own n ty)%P.
-  Proof.
-    iIntros (? ν tid Φ E ?) "_ H◁ Htl HΦ". iApply (has_type_wp with "H◁").
-    iIntros (v) "Hνv H◁". iDestruct "Hνv" as %Hνv.
-    rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & H↦ & >H†)".
-    iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ #Hown]".
-    iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">%".
-      by rewrite ty.(ty_size_eq).
-    iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦!>".
-    rewrite /has_type Hνv. iExists _. iSplit. done. iFrame. iExists vl. eauto.
-  Qed.
-
-  Lemma consumes_move ty n:
-    consumes ty (λ ν, ν ◁ own n ty)%P
-             (λ ν, ν ◁ own n (Π(replicate ty.(ty_size) uninit)))%P.
-  Proof.
-    iIntros (ν tid Φ E ?) "_ H◁ Htl HΦ". iApply (has_type_wp with "H◁").
-    iIntros (v) "Hνv H◁". iDestruct "Hνv" as %Hνv.
-    rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & H↦ & >H†)".
-    iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
-    iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">Hlen".
-      by rewrite ty.(ty_size_eq). iDestruct "Hlen" as %Hlen.
-    iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦!>".
-    rewrite /has_type Hνv. iExists _. iSplit. done. iSplitR "H†".
-    - rewrite -Hlen. iExists vl. iIntros "{$H↦}!>". clear.
-      iInduction vl as [|v vl] "IH". done.
-      iExists [v], vl. iSplit. done. by iSplit.
-    - assert (ty_size (Π (replicate (ty_size ty) uninit)) = ty_size ty) as ->; last by auto.
-      clear. induction ty.(ty_size). done. by apply (f_equal S).
-  Qed.
-End own.