diff --git a/_CoqProject b/_CoqProject
index efa22df0b379fcbc57f62958b0a08d4ef434bb18..b08a7535e0d039a2ef95bc6ce722fbbb2e8802cf 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -10,7 +10,7 @@ theories/lifetime/borrow.v
theories/lifetime/reborrow.v
theories/lifetime/shr_borrow.v
theories/lifetime/frac_borrow.v
-theories/lifetime/tl_borrow.v
+theories/lifetime/na_borrow.v
theories/lang/adequacy.v
theories/lang/derived.v
theories/lang/heap.v
@@ -25,6 +25,14 @@ theories/lang/wp_tactics.v
theories/typing/type.v
theories/typing/type_incl.v
theories/typing/perm.v
-theories/typing/perm_incl.v
theories/typing/typing.v
theories/typing/lft_contexts.v
+theories/typing/own.v
+theories/typing/uniq_bor.v
+theories/typing/shr_bor.v
+theories/typing/product.v
+theories/typing/product_split.v
+theories/typing/sum.v
+theories/typing/bool.v
+theories/typing/int.v
+theories/typing/function.v
diff --git a/theories/lifetime/tl_borrow.v b/theories/lifetime/na_borrow.v
similarity index 100%
rename from theories/lifetime/tl_borrow.v
rename to theories/lifetime/na_borrow.v
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
new file mode 100644
index 0000000000000000000000000000000000000000..639dab97bc8199412af3fff3fae63f09d54cac19
--- /dev/null
+++ b/theories/typing/bool.v
@@ -0,0 +1,24 @@
+From iris.proofmode Require Import tactics.
+From lrust.typing Require Export type.
+From lrust.typing Require Import typing.
+
+Section bool.
+ Context `{iris_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
diff --git a/theories/typing/function.v b/theories/typing/function.v
new file mode 100644
index 0000000000000000000000000000000000000000..7aa2e14d2575b5b6c601d22c4e755c17225abbe8
--- /dev/null
+++ b/theories/typing/function.v
@@ -0,0 +1,121 @@
+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 `{iris_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.
diff --git a/theories/typing/int.v b/theories/typing/int.v
new file mode 100644
index 0000000000000000000000000000000000000000..73724f218648f6354a68105f79db56d79df0191e
--- /dev/null
+++ b/theories/typing/int.v
@@ -0,0 +1,54 @@
+From iris.proofmode Require Import tactics.
+From lrust.typing Require Export type.
+From lrust.typing Require Import typing bool.
+
+Section int.
+ Context `{iris_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
diff --git a/theories/typing/own.v b/theories/typing/own.v
new file mode 100644
index 0000000000000000000000000000000000000000..ea688034df9978a6291992bde3f266a988415d65
--- /dev/null
+++ b/theories/typing/own.v
@@ -0,0 +1,154 @@
+From iris.proofmode Require Import tactics.
+From lrust.lifetime Require Import borrow frac_borrow.
+From lrust.typing Require Export type.
+From lrust.typing Require Import type_incl typing product.
+
+Section own.
+ Context `{iris_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 own (q : Qp) (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 [ty_incl_own].
+
+ Since this assertion is timeless, this should not cause
+ problems. *)
+ (∃ l:loc, ⌜vl = [ #l ]⌠∗ ▷ l ↦∗: ty.(ty_own) tid ∗ ▷ †{q}l…ty.(ty_size))%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.
+
+ Lemma ty_incl_own Ï ty1 ty2 q :
+ ty_incl Ï ty1 ty2 → ty_incl Ï (own q ty1) (own q ty2).
+ Proof.
+ iIntros (Hincl tid) "#LFT H/=". iMod (Hincl with "LFT H") as "[#Howni #Hshri]".
+ iModIntro. iSplit; iIntros "!#*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.
+ - iDestruct "H" as (l') "[Hfb #Hvs]". iSplit; last done. iExists l'. iFrame.
+ iIntros "!#". iIntros (q' F) "% Hκ".
+ iMod ("Hvs" with "* [%] Hκ") as "Hvs'". done. iModIntro. iNext.
+ iMod "Hvs'" as "[Hshr $]". by iDestruct ("Hshri" with "* Hshr") as "[$ _]".
+ Qed.
+
+ Lemma typed_alloc Ï (n : nat):
+ 0 < n → typed_step_ty Ï (Alloc #n) (own 1 (Î (replicate n uninit))).
+ Proof.
+ iIntros (Hn tid) "!#(#HEAP&_&_&$)". wp_alloc l vl as "H↦" "H†". iIntros "!>".
+ 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 ->; last done.
+ clear. simpl. induction n. done. rewrite /= IHn //.
+ Qed.
+
+ Lemma typed_free ty (ν : expr):
+ typed_step (ν ◠own 1 ty) (Free #ty.(ty_size) ν) (λ _, 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 ">%". wp_free; eauto.
+ Qed.
+
+ Lemma update_strong ty1 ty2 q:
+ ty1.(ty_size) = ty2.(ty_size) →
+ update ty1 (λ ν, ν ◠own q ty2)%P (λ ν, ν ◠own q 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 q:
+ Copy ty → consumes ty (λ ν, ν ◠own q ty)%P (λ ν, ν ◠own q 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 q:
+ consumes ty (λ ν, ν ◠own q ty)%P
+ (λ ν, ν ◠own q (Π(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.
\ No newline at end of file
diff --git a/theories/typing/perm.v b/theories/typing/perm.v
index 7e88e51a27fd4afcc50f1b6ff08bf6cbfb6e83e9..e44f9e1687b516a06847a37ede361b9ae42ef882 100644
--- a/theories/typing/perm.v
+++ b/theories/typing/perm.v
@@ -1,17 +1,13 @@
From iris.proofmode Require Import tactics.
From lrust.typing Require Export type.
-From lrust.lang Require Export proofmode.
-From lrust.lifetime Require Import frac_borrow.
-
-Delimit Scope perm_scope with P.
-Bind Scope perm_scope with perm.
-
-Module Perm.
+From lrust.lang Require Export proofmode notation.
+From lrust.lifetime Require Import borrow frac_borrow.
Section perm.
-
Context `{iris_typeG Σ}.
+ Definition perm {Σ} := thread_id → iProp Σ.
+
Fixpoint eval_expr (ν : expr) : option val :=
match ν with
| BinOp ProjOp e (Lit (LitInt n)) =>
@@ -47,11 +43,18 @@ Section perm.
Global Instance top : Top (@perm Σ) :=
λ _, True%I.
-End perm.
+ Definition perm_incl (Ï1 Ï2 : perm) :=
+ ∀ tid, lft_ctx -∗ Ï1 tid ={⊤}=∗ Ï2 tid.
+
+ Global Instance perm_equiv : Equiv perm :=
+ λ Ï1 Ï2, perm_incl Ï1 Ï2 ∧ perm_incl Ï2 Ï1.
-End Perm.
+ Definition borrowing κ (Ï Ï1 Ï2 : perm) :=
+ ∀ tid, lft_ctx -∗ Ï tid -∗ Ï1 tid ={⊤}=∗ Ï2 tid ∗ extract κ Ï1 tid.
+End perm.
-Import Perm.
+Delimit Scope perm_scope with P.
+Bind Scope perm_scope with perm.
Notation "ν ◠ty" := (has_type ν%E ty)
(at level 75, right associativity) : perm_scope.
@@ -70,15 +73,21 @@ Notation "∃ x .. y , P" :=
Infix "∗" := sep (at level 80, right associativity) : perm_scope.
-Section duplicable.
+Infix "⇒" := perm_incl (at level 95, no associativity) : C_scope.
+Notation "(⇒)" := perm_incl (only parsing) : C_scope.
+Notation "Ï1 ⇔ Ï2" := (equiv (A:=perm) Ï1%P Ï2%P)
+ (at level 95, no associativity) : C_scope.
+Notation "(⇔)" := (equiv (A:=perm)) (only parsing) : C_scope.
+
+Section duplicable.
Context `{iris_typeG Σ}.
Class Duplicable (Ï : @perm Σ) :=
duplicable_persistent tid : PersistentP (Ï tid).
Global Existing Instance duplicable_persistent.
- Global Instance has_type_dup v ty : ty.(ty_dup) → Duplicable (v ◠ty).
+ Global Instance has_type_dup v ty : Copy ty → Duplicable (v ◠ty).
Proof. intros Hdup tid. apply _. Qed.
Global Instance lft_incl_dup κ κ' : Duplicable (κ ⊑ κ').
@@ -90,12 +99,9 @@ Section duplicable.
Global Instance top_dup : Duplicable ⊤.
Proof. intros tid. apply _. Qed.
-
End duplicable.
-
Section has_type.
-
Context `{iris_typeG Σ}.
Lemma has_type_value (v : val) ty tid :
@@ -121,5 +127,95 @@ Section has_type.
- wp_bind e. simpl in EQν. destruct (eval_expr e) as [[[|l|]|]|]; try done.
iApply ("IH" with "[] [HΦ]"). done. simpl. wp_op. inversion EQν. eauto.
Qed.
+End has_type.
+
+Section perm_incl.
+ Context `{iris_typeG Σ}.
+
+ (* Properties *)
+ Global Instance perm_incl_preorder : PreOrder (⇒).
+ Proof.
+ split.
+ - iIntros (? tid) "H". eauto.
+ - iIntros (??? H12 H23 tid) "#LFT H". iApply (H23 with "LFT >").
+ by iApply (H12 with "LFT").
+ Qed.
-End has_type.
\ No newline at end of file
+ Global Instance perm_equiv_equiv : Equivalence (⇔).
+ Proof.
+ split.
+ - by split.
+ - by intros x y []; split.
+ - intros x y z [] []. split; by transitivity y.
+ Qed.
+
+ Global Instance perm_incl_proper :
+ Proper ((⇔) ==> (⇔) ==> iff) (⇒).
+ Proof. intros ??[??]??[??]; split; intros ?; by simplify_order. Qed.
+
+ Global Instance perm_sep_proper :
+ Proper ((⇔) ==> (⇔) ==> (⇔)) (sep).
+ Proof.
+ intros ??[A B]??[C D]; split; iIntros (tid) "#LFT [A B]".
+ iMod (A with "LFT A") as "$". iApply (C with "LFT B").
+ iMod (B with "LFT A") as "$". iApply (D with "LFT B").
+ Qed.
+
+ Lemma uPred_equiv_perm_equiv Ï Î¸ : (∀ tid, Ï tid ⊣⊢ θ tid) → (Ï â‡” θ).
+ Proof. intros Heq. split=>tid; rewrite Heq; by iIntros. Qed.
+
+ Lemma perm_incl_top Ï : Ï â‡’ ⊤.
+ Proof. iIntros (tid) "H". eauto. Qed.
+
+ Lemma perm_incl_frame_l Ï Ï1 Ï2 : Ï1 ⇒ Ï2 → Ï âˆ— Ï1 ⇒ Ï âˆ— Ï2.
+ Proof. iIntros (HÏ tid) "#LFT [$?]". by iApply (HÏ with "LFT"). Qed.
+
+ Lemma perm_incl_frame_r Ï Ï1 Ï2 :
+ Ï1 ⇒ Ï2 → Ï1 ∗ Ï â‡’ Ï2 ∗ Ï.
+ Proof. iIntros (HÏ tid) "#LFT [?$]". by iApply (HÏ with "LFT"). Qed.
+
+ Lemma perm_incl_exists_intro {A} P x : P x ⇒ ∃ x : A, P x.
+ Proof. iIntros (tid) "_ H!>". by iExists x. Qed.
+
+ Global Instance perm_sep_assoc : Assoc (⇔) sep.
+ Proof. intros ???; split. by iIntros (tid) "_ [$[$$]]". by iIntros (tid) "_ [[$$]$]". Qed.
+
+ Global Instance perm_sep_comm : Comm (⇔) sep.
+ Proof. intros ??; split; by iIntros (tid) "_ [$$]". Qed.
+
+ Global Instance perm_top_right_id : RightId (⇔) ⊤ sep.
+ Proof. intros Ï; split. by iIntros (tid) "_ [? _]". by iIntros (tid) "_ $". Qed.
+
+ Global Instance perm_top_left_id : LeftId (⇔) ⊤ sep.
+ Proof. intros Ï. by rewrite comm right_id. Qed.
+
+ Lemma perm_incl_duplicable Ï (_ : Duplicable Ï) : Ï â‡’ Ï âˆ— Ï.
+ Proof. iIntros (tid) "_ #H!>". by iSplit. Qed.
+
+ Lemma perm_tok_plus κ q1 q2 :
+ tok κ q1 ∗ tok κ q2 ⇔ tok κ (q1 + q2).
+ Proof. rewrite /tok /sep /=; split; by iIntros (tid) "_ [$$]". Qed.
+
+ Lemma perm_lftincl_refl κ : ⊤ ⇒ κ ⊑ κ.
+ Proof. iIntros (tid) "_ _!>". iApply lft_incl_refl. Qed.
+
+ Lemma perm_lftincl_trans κ1 κ2 κ3 : κ1 ⊑ κ2 ∗ κ2 ⊑ κ3 ⇒ κ1 ⊑ κ3.
+ Proof. iIntros (tid) "_ [#?#?]!>". iApply (lft_incl_trans with "[] []"); auto. Qed.
+
+ Lemma borrowing_perm_incl κ Ï Ï1 Ï2 θ :
+ borrowing κ Ï Ï1 Ï2 → Ï âˆ— κ ∋ θ ∗ Ï1 ⇒ Ï2 ∗ κ ∋ (θ ∗ Ï1).
+ Proof.
+ iIntros (Hbor tid) "LFT (HÏ&Hθ&HÏ1)". iMod (Hbor with "LFT HÏ HÏ1") as "[$ HÏ1]".
+ iIntros "!>#H†". iSplitL "Hθ". by iApply "Hθ". by iApply "HÏ1".
+ Qed.
+
+ Lemma lftincl_borrowing κ κ' q : borrowing κ ⊤ q.[κ'] (κ ⊑ κ').
+ Proof.
+ iIntros (tid) "#LFT _ Htok". iApply (fupd_mask_mono (↑lftN)). done.
+ iMod (bor_create with "LFT [$Htok]") as "[Hbor Hclose]". done.
+ iMod (bor_fracture (λ q', (q * q').[κ'])%I with "LFT [Hbor]") as "Hbor". done.
+ { by rewrite Qp_mult_1_r. }
+ iSplitL "Hbor". iApply (frac_bor_incl with "LFT Hbor").
+ iIntros "!>H". by iMod ("Hclose" with "H") as ">$".
+ Qed.
+End perm_incl.
diff --git a/theories/typing/product.v b/theories/typing/product.v
new file mode 100644
index 0000000000000000000000000000000000000000..5cd811cee01c479c0a13764b0ed80bfabc0d83ca
--- /dev/null
+++ b/theories/typing/product.v
@@ -0,0 +1,188 @@
+From iris.proofmode Require Import tactics.
+From lrust.lifetime Require Import borrow frac_borrow.
+From lrust.typing Require Export type.
+From lrust.typing Require Import perm type_incl.
+
+Section product.
+ Context `{iris_typeG Σ}.
+
+ Program Definition unit : type :=
+ {| st_size := 0; st_own tid vl := ⌜vl = []âŒ%I |}.
+ Next Obligation. iIntros (tid vl) "%". simpl. by subst. Qed.
+
+ Lemma split_prod_mt tid ty1 ty2 q l :
+ (l ↦∗{q}: λ vl,
+ ∃ vl1 vl2, ⌜vl = vl1 ++ vl2⌠∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I
+ ⊣⊢ l ↦∗{q}: ty1.(ty_own) tid ∗ shift_loc l ty1.(ty_size) ↦∗{q}: ty2.(ty_own) tid.
+ Proof.
+ iSplit; iIntros "H".
+ - iDestruct "H" as (vl) "[H↦ H]". iDestruct "H" as (vl1 vl2) "(% & H1 & H2)".
+ subst. rewrite heap_mapsto_vec_app. iDestruct "H↦" as "[H↦1 H↦2]".
+ iDestruct (ty_size_eq with "H1") as %->.
+ iSplitL "H1 H↦1"; iExists _; iFrame.
+ - iDestruct "H" as "[H1 H2]". iDestruct "H1" as (vl1) "[H↦1 H1]".
+ iDestruct "H2" as (vl2) "[H↦2 H2]". iExists (vl1 ++ vl2).
+ rewrite heap_mapsto_vec_app. iDestruct (ty_size_eq with "H1") as %->.
+ iFrame. iExists _, _. by iFrame.
+ Qed.
+
+ Program Definition product2 (ty1 ty2 : type) :=
+ {| ty_size := ty1.(ty_size) + ty2.(ty_size);
+ ty_own tid vl := (∃ vl1 vl2,
+ ⌜vl = vl1 ++ vl2⌠∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I;
+ ty_shr κ tid E l :=
+ (∃ E1 E2, ⌜E1 ⊥ E2 ∧ E1 ⊆ E ∧ E2 ⊆ E⌠∗
+ ty1.(ty_shr) κ tid E1 l ∗
+ ty2.(ty_shr) κ tid E2 (shift_loc l ty1.(ty_size)))%I |}.
+ Next Obligation.
+ iIntros (ty1 ty2 tid vl) "H". iDestruct "H" as (vl1 vl2) "(% & H1 & H2)".
+ subst. rewrite app_length !ty_size_eq.
+ iDestruct "H1" as %->. iDestruct "H2" as %->. done.
+ Qed.
+ Next Obligation.
+ intros ty1 ty2 E N κ l tid q ??. iIntros "#LFT /=H Htok".
+ rewrite split_prod_mt.
+ iMod (bor_sep with "LFT H") as "[H1 H2]". set_solver.
+ iMod (ty1.(ty_share) _ (N .@ 1) with "LFT H1 Htok") as "[? Htok]". solve_ndisj. done.
+ iMod (ty2.(ty_share) _ (N .@ 2) with "LFT H2 Htok") as "[? $]". solve_ndisj. done.
+ iModIntro. iExists (↑N .@ 1). iExists (↑N .@ 2). iFrame.
+ iPureIntro. split. solve_ndisj. split; apply nclose_subseteq.
+ Qed.
+ Next Obligation.
+ intros ty1 ty2 κ κ' tid E E' l ?. iIntros "#LFT /= #H⊑ H".
+ iDestruct "H" as (N1 N2) "(% & H1 & H2)". iExists N1, N2.
+ iSplit. iPureIntro. set_solver.
+ iSplitL "H1"; by iApply (ty_shr_mono with "LFT H⊑").
+ Qed.
+
+ Global Program Instance product2_copy `(!Copy ty1) `(!Copy ty2) :
+ Copy (product2 ty1 ty2).
+ Next Obligation.
+ intros ty1 ? ty2 ? κ tid E F l q ?. iIntros "#LFT H [[Htok1 Htok2] Htl]".
+ iDestruct "H" as (E1 E2) "(% & H1 & H2)".
+ assert (F = E1 ∪ E2 ∪ F∖(E1 ∪ E2)) as ->.
+ { rewrite -union_difference_L; set_solver. }
+ repeat setoid_rewrite na_own_union; first last.
+ set_solver. set_solver. set_solver. set_solver.
+ iDestruct "Htl" as "[[Htl1 Htl2] $]".
+ iMod (@copy_shr_acc with "LFT H1 [$Htok1 $Htl1]") as (q1) "[H1 Hclose1]". set_solver.
+ iMod (@copy_shr_acc with "LFT H2 [$Htok2 $Htl2]") as (q2) "[H2 Hclose2]". set_solver.
+ destruct (Qp_lower_bound q1 q2) as (qq & q'1 & q'2 & -> & ->). iExists qq.
+ iDestruct "H1" as (vl1) "[H↦1 H1]". iDestruct "H2" as (vl2) "[H↦2 H2]".
+ rewrite !split_prod_mt.
+ iAssert (â–· ⌜length vl1 = ty1.(ty_size)âŒ)%I with "[#]" as ">%".
+ { iNext. by iApply ty_size_eq. }
+ iAssert (â–· ⌜length vl2 = ty2.(ty_size)âŒ)%I with "[#]" as ">%".
+ { iNext. by iApply ty_size_eq. }
+ iDestruct "H↦1" as "[H↦1 H↦1f]". iDestruct "H↦2" as "[H↦2 H↦2f]".
+ iIntros "!>". iSplitL "H↦1 H1 H↦2 H2".
+ - iNext. iSplitL "H↦1 H1". iExists vl1. by iFrame. iExists vl2. by iFrame.
+ - iIntros "[H1 H2]".
+ iDestruct "H1" as (vl1') "[H↦1 H1]". iDestruct "H2" as (vl2') "[H↦2 H2]".
+ iAssert (â–· ⌜length vl1' = ty1.(ty_size)âŒ)%I with "[#]" as ">%".
+ { iNext. by iApply ty_size_eq. }
+ iAssert (â–· ⌜length vl2' = ty2.(ty_size)âŒ)%I with "[#]" as ">%".
+ { iNext. by iApply ty_size_eq. }
+ iCombine "H↦1" "H↦1f" as "H↦1". iCombine "H↦2" "H↦2f" as "H↦2".
+ rewrite !heap_mapsto_vec_op; try by congruence.
+ iDestruct "H↦1" as "[_ H↦1]". iDestruct "H↦2" as "[_ H↦2]".
+ iMod ("Hclose1" with "[H1 H↦1]") as "[$$]". by iExists _; iFrame.
+ iMod ("Hclose2" with "[H2 H↦2]") as "[$$]". by iExists _; iFrame. done.
+ Qed.
+
+ Definition product := fold_right product2 unit.
+End product.
+
+Arguments product : simpl never.
+Notation Î := product.
+
+Section typing.
+ Context `{iris_typeG Σ}.
+
+ (* We have the additional hypothesis that Ï should be duplicable.
+ The only way I can see to circumvent this limitation is to deeply
+ embed permissions (and their inclusion). Not sure this is worth it. *)
+ Lemma ty_incl_prod2 Ï ty11 ty12 ty21 ty22 :
+ Duplicable Ï â†’ ty_incl Ï ty11 ty12 → ty_incl Ï ty21 ty22 →
+ ty_incl Ï (product2 ty11 ty21) (product2 ty12 ty22).
+ Proof.
+ iIntros (HÏ Hincl1 Hincl2 tid) "#LFT #HÏ".
+ iMod (Hincl1 with "LFT HÏ") as "[#Ho1#Hs1]".
+ iMod (Hincl2 with "LFT HÏ") as "[#Ho2#Hs2]".
+ iSplitL; iIntros "!>!#*H/=".
+ - iDestruct "H" as (vl1 vl2) "(% & H1 & H2)". iExists _, _. iSplit. done.
+ iSplitL "H1". iApply ("Ho1" with "H1"). iApply ("Ho2" with "H2").
+ - iDestruct "H" as (E1 E2) "(% & H1 & H2)".
+ iDestruct ("Hs1" with "*H1") as "[H1 EQ]". iDestruct ("Hs2" with "*H2") as "[H2 %]".
+ iDestruct "EQ" as %->. iSplit; last by iPureIntro; f_equal.
+ iExists _, _. by iFrame.
+ Qed.
+
+ Lemma ty_incl_prod Ï tyl1 tyl2 :
+ Duplicable Ï â†’ Forall2 (ty_incl Ï) tyl1 tyl2 → ty_incl Ï (Î tyl1) (Î tyl2).
+ Proof. intros HÏ HFA. induction HFA. done. by apply ty_incl_prod2. Qed.
+
+ Lemma ty_incl_prod2_assoc1 Ï ty1 ty2 ty3 :
+ ty_incl Ï (product2 ty1 (product2 ty2 ty3)) (product2 (product2 ty1 ty2) ty3).
+ Proof.
+ iIntros (tid) "_ _!>". iSplit; iIntros "!#/=*H".
+ - iDestruct "H" as (vl1 vl') "(% & Ho1 & H)".
+ iDestruct "H" as (vl2 vl3) "(% & Ho2 & Ho3)". subst.
+ iExists _, _. iSplit. by rewrite assoc. iFrame. iExists _, _. by iFrame.
+ - iDestruct "H" as (E1 E2') "(% & Hs1 & H)".
+ iDestruct "H" as (E2 E3) "(% & Hs2 & Hs3)". rewrite shift_loc_assoc_nat.
+ iSplit; last by rewrite assoc.
+ iExists (E1 ∪ E2), E3. iSplit. by iPureIntro; set_solver. iFrame.
+ iExists E1, E2. iSplit. by iPureIntro; set_solver. by iFrame.
+ Qed.
+
+ Lemma ty_incl_prod2_assoc2 Ï ty1 ty2 ty3 :
+ ty_incl Ï (product2 (product2 ty1 ty2) ty3) (product2 ty1 (product2 ty2 ty3)).
+ Proof.
+ iIntros (tid) "_ _!>". iSplit; iIntros "!#/=*H".
+ - iDestruct "H" as (vl1 vl') "(% & H & Ho3)".
+ iDestruct "H" as (vl2 vl3) "(% & Ho1 & Ho2)". subst.
+ iExists _, _. iSplit. by rewrite -assoc. iFrame. iExists _, _. by iFrame.
+ - iDestruct "H" as (E1' E3) "(% & H & Hs3)".
+ iDestruct "H" as (E1 E2) "(% & Hs1 & Hs2)". rewrite shift_loc_assoc_nat.
+ iSplit; last by rewrite assoc.
+ iExists E1, (E2 ∪ E3). iSplit. by iPureIntro; set_solver. iFrame.
+ iExists E2, E3. iSplit. by iPureIntro; set_solver. by iFrame.
+ Qed.
+
+ Lemma ty_incl_prod_flatten Ï tyl1 tyl2 tyl3 :
+ ty_incl Ï (Î (tyl1 ++ Î tyl2 :: tyl3))
+ (Î (tyl1 ++ tyl2 ++ tyl3)).
+ Proof.
+ apply (ty_incl_weaken _ ⊤). apply perm_incl_top.
+ induction tyl1; last by apply (ty_incl_prod2 _ _ _ _ _ _).
+ induction tyl2 as [|ty tyl2 IH]; simpl.
+ - iIntros (tid) "#LFT _". iSplitL; iIntros "/=!>!#*H".
+ + iDestruct "H" as (vl1 vl2) "(% & % & Ho)". subst. done.
+ + iDestruct "H" as (E1 E2) "(% & H1 & Ho)". iSplit; last done.
+ rewrite shift_loc_0. iApply (ty_shr_mono with "LFT [] Ho"). set_solver.
+ iApply lft_incl_refl.
+ - etransitivity. apply ty_incl_prod2_assoc2.
+ eapply (ty_incl_prod2 _ _ _ _ _ _). done. apply IH.
+ Qed.
+
+ Lemma ty_incl_prod_unflatten Ï tyl1 tyl2 tyl3 :
+ ty_incl Ï (Î (tyl1 ++ tyl2 ++ tyl3))
+ (Î (tyl1 ++ Î tyl2 :: tyl3)).
+ Proof.
+ apply (ty_incl_weaken _ ⊤). apply perm_incl_top.
+ induction tyl1; last by apply (ty_incl_prod2 _ _ _ _ _ _).
+ induction tyl2 as [|ty tyl2 IH]; simpl.
+ - iIntros (tid) "#LFT _". iMod (bor_create with "LFT []") as "[Hbor _]".
+ done. instantiate (1:=True%I). by auto. instantiate (1:=static).
+ iMod (bor_fracture (λ _, True%I) with "LFT Hbor") as "#Hbor". done.
+ iSplitL; iIntros "/=!>!#*H".
+ + iExists [], vl. iFrame. auto.
+ + iSplit; last done. iExists ∅, E. iSplit. iPureIntro; set_solver.
+ rewrite shift_loc_0. iFrame. iExists []. iSplit; last auto.
+ setoid_rewrite heap_mapsto_vec_nil.
+ iApply (frac_bor_shorten with "[] Hbor"). iApply lft_incl_static.
+ - etransitivity; last apply ty_incl_prod2_assoc1.
+ eapply (ty_incl_prod2 _ _ _ _ _ _). done. apply IH.
+ Qed.
+End typing.
diff --git a/theories/typing/perm_incl.v b/theories/typing/product_split.v
similarity index 50%
rename from theories/typing/perm_incl.v
rename to theories/typing/product_split.v
index e57137d489d97dcef794005996bc31491dfac444..83b0406a8283984ec589e8f6e22c975108ee0b1d 100644
--- a/theories/typing/perm_incl.v
+++ b/theories/typing/product_split.v
@@ -1,116 +1,17 @@
From Coq Require Import Qcanon.
-From iris.base_logic Require Import big_op.
-From lrust.typing Require Export type perm.
-From lrust.lifetime Require Import borrow frac_borrow reborrow.
-
-Import Perm Types.
-
-Section defs.
+From iris.proofmode Require Import tactics.
+From lrust.lifetime Require Import borrow frac_borrow.
+From lrust.typing Require Export type.
+From lrust.typing Require Import type_incl typing product own uniq_bor shr_bor.
+Section product_split.
Context `{iris_typeG Σ}.
- (* Definitions *)
- Definition perm_incl (Ï1 Ï2 : perm) :=
- ∀ tid, lft_ctx -∗ Ï1 tid ={⊤}=∗ Ï2 tid.
-
- Global Instance perm_equiv : Equiv perm :=
- λ Ï1 Ï2, perm_incl Ï1 Ï2 ∧ perm_incl Ï2 Ï1.
-
- Definition borrowing κ (Ï Ï1 Ï2 : perm) :=
- ∀ tid, lft_ctx -∗ Ï tid -∗ Ï1 tid ={⊤}=∗ Ï2 tid ∗ (κ ∋ Ï1)%P tid.
-
-End defs.
-
-Infix "⇒" := perm_incl (at level 95, no associativity) : C_scope.
-Notation "(⇒)" := perm_incl (only parsing) : C_scope.
-
-Notation "Ï1 ⇔ Ï2" := (equiv (A:=perm) Ï1%P Ï2%P)
- (at level 95, no associativity) : C_scope.
-Notation "(⇔)" := (equiv (A:=perm)) (only parsing) : C_scope.
-
-Section props.
-
- Context `{iris_typeG Σ}.
-
- (* Properties *)
- Global Instance perm_incl_preorder : PreOrder (⇒).
- Proof.
- split.
- - iIntros (? tid) "H". eauto.
- - iIntros (??? H12 H23 tid) "#LFT H". iApply (H23 with "LFT >").
- by iApply (H12 with "LFT").
- Qed.
-
- Global Instance perm_equiv_equiv : Equivalence (⇔).
- Proof.
- split.
- - by split.
- - by intros x y []; split.
- - intros x y z [] []. split; by transitivity y.
- Qed.
-
- Global Instance perm_incl_proper :
- Proper ((⇔) ==> (⇔) ==> iff) (⇒).
- Proof. intros ??[??]??[??]; split; intros ?; by simplify_order. Qed.
-
- Global Instance perm_sep_proper :
- Proper ((⇔) ==> (⇔) ==> (⇔)) (sep).
- Proof.
- intros ??[A B]??[C D]; split; iIntros (tid) "#LFT [A B]".
- iMod (A with "LFT A") as "$". iApply (C with "LFT B").
- iMod (B with "LFT A") as "$". iApply (D with "LFT B").
- Qed.
-
- Lemma uPred_equiv_perm_equiv Ï Î¸ : (∀ tid, Ï tid ⊣⊢ θ tid) → (Ï â‡” θ).
- Proof. intros Heq. split=>tid; rewrite Heq; by iIntros. Qed.
-
- Lemma perm_incl_top Ï : Ï â‡’ ⊤.
- Proof. iIntros (tid) "H". eauto. Qed.
-
- Lemma perm_incl_frame_l Ï Ï1 Ï2 : Ï1 ⇒ Ï2 → Ï âˆ— Ï1 ⇒ Ï âˆ— Ï2.
- Proof. iIntros (HÏ tid) "#LFT [$?]". by iApply (HÏ with "LFT"). Qed.
-
- Lemma perm_incl_frame_r Ï Ï1 Ï2 :
- Ï1 ⇒ Ï2 → Ï1 ∗ Ï â‡’ Ï2 ∗ Ï.
- Proof. iIntros (HÏ tid) "#LFT [?$]". by iApply (HÏ with "LFT"). Qed.
-
- Lemma perm_incl_exists_intro {A} P x : P x ⇒ ∃ x : A, P x.
- Proof. iIntros (tid) "_ H!>". by iExists x. Qed.
-
- Global Instance perm_sep_assoc : Assoc (⇔) sep.
- Proof. intros ???; split. by iIntros (tid) "_ [$[$$]]". by iIntros (tid) "_ [[$$]$]". Qed.
-
- Global Instance perm_sep_comm : Comm (⇔) sep.
- Proof. intros ??; split; by iIntros (tid) "_ [$$]". Qed.
-
- Global Instance perm_top_right_id : RightId (⇔) ⊤ sep.
- Proof. intros Ï; split. by iIntros (tid) "_ [? _]". by iIntros (tid) "_ $". Qed.
-
- Global Instance perm_top_left_id : LeftId (⇔) ⊤ sep.
- Proof. intros Ï. by rewrite comm right_id. Qed.
-
- Lemma perm_incl_duplicable Ï (_ : Duplicable Ï) : Ï â‡’ Ï âˆ— Ï.
- Proof. iIntros (tid) "_ #H!>". by iSplit. Qed.
-
- Lemma perm_tok_plus κ q1 q2 :
- tok κ q1 ∗ tok κ q2 ⇔ tok κ (q1 + q2).
- Proof. rewrite /tok /sep /=; split; by iIntros (tid) "_ [$$]". Qed.
-
- Lemma perm_lftincl_refl κ : ⊤ ⇒ κ ⊑ κ.
- Proof. iIntros (tid) "_ _!>". iApply lft_incl_refl. Qed.
-
- Lemma perm_lftincl_trans κ1 κ2 κ3 : κ1 ⊑ κ2 ∗ κ2 ⊑ κ3 ⇒ κ1 ⊑ κ3.
- Proof. iIntros (tid) "_ [#?#?]!>". iApply (lft_incl_trans with "[] []"); auto. Qed.
-
- Lemma perm_incl_share q ν κ ty :
- ν ◠&uniq{κ} ty ∗ q.[κ] ⇒ ν ◠&shr{κ} ty ∗ q.[κ].
- Proof.
- iIntros (tid) "#LFT [Huniq [Htok $]]". unfold has_type.
- destruct (eval_expr ν); last by iDestruct "Huniq" as "[]".
- iDestruct "Huniq" as (l) "[% Hown]".
- iMod (ty.(ty_share) _ lrustN with "LFT Hown Htok") as "[Hown $]"; [solve_ndisj|done|].
- iIntros "!>/=". eauto.
- Qed.
+ Fixpoint combine_offs (tyl : list type) (accu : nat) :=
+ match tyl with
+ | [] => []
+ | ty :: q => (ty, accu) :: combine_offs q (accu + ty.(ty_size))
+ end.
Lemma perm_split_own_prod2 ty1 ty2 (q1 q2 : Qp) ν :
ν ◠own (q1 + q2) (product2 ty1 ty2) ⇔
@@ -140,12 +41,6 @@ Section props.
iDestruct "EQ" as %->. iFrame. iExists vl1, vl2. iFrame. auto.
Qed.
- Fixpoint combine_offs (tyl : list type) (accu : nat) :=
- match tyl with
- | [] => []
- | ty :: q => (ty, accu) :: combine_offs q (accu + ty.(ty_size))
- end.
-
Lemma perm_split_own_prod tyl (q : Qp) (ql : list Qp) ν :
length tyl = length ql →
foldr (λ (q : Qp) acc, q + acc)%Qc 0%Qc ql = q →
@@ -210,13 +105,15 @@ Section props.
⊤ (combine_offs tyl 0).
Proof.
transitivity (ν +ₗ #0%nat ◠&uniq{κ}Πtyl)%P.
- { iIntros (tid) "_ H/=". rewrite /has_type /=. destruct (eval_expr ν)=>//.
+ { iIntros (tid) "_ H/=". rewrite /has_type /=.
+ destruct (eval_expr ν)=>//.
iDestruct "H" as (l) "[Heq H]". iDestruct "Heq" as %[=->].
rewrite shift_loc_0 /=. eauto. }
generalize 0%nat. induction tyl as [|ty tyl IH]=>offs. by iIntros (tid) "_ H/=".
etransitivity. apply perm_split_uniq_bor_prod2.
- iIntros (tid) "#LFT /=[$ H]". iApply (IH with "LFT"). rewrite /has_type /=.
- destruct (eval_expr ν) as [[[]|]|]=>//=. by rewrite shift_loc_assoc_nat.
+ iIntros (tid) "#LFT /=[$ H]". iApply (IH with "LFT").
+ rewrite /has_type /=. destruct (eval_expr ν) as [[[]|]|]=>//=.
+ by rewrite shift_loc_assoc_nat.
Qed.
Lemma perm_split_shr_bor_prod2 ty1 ty2 κ ν :
@@ -240,7 +137,8 @@ Section props.
⊤ (combine_offs tyl 0).
Proof.
transitivity (ν +ₗ #0%nat ◠&shr{κ}Πtyl)%P.
- { iIntros (tid) "#LFT H/=". rewrite /has_type /=. destruct (eval_expr ν)=>//.
+ { iIntros (tid) "#LFT H/=". rewrite /has_type /=.
+ destruct (eval_expr ν)=>//.
iDestruct "H" as (l) "[Heq H]". iDestruct "Heq" as %[=->].
rewrite shift_loc_0 /=. iExists _. by iFrame "∗%". }
generalize 0%nat. induction tyl as [|ty tyl IH]=>offs. by iIntros (tid) "_ H/=".
@@ -248,58 +146,4 @@ Section props.
iIntros (tid) "#LFT /=[$ H]". iApply (IH with "LFT"). rewrite /has_type /=.
destruct (eval_expr ν) as [[[]|]|]=>//=. by rewrite shift_loc_assoc_nat.
Qed.
-
- Lemma rebor_shr_perm_incl κ κ' ν ty :
- κ ⊑ κ' ∗ ν ◠&shr{κ'}ty ⇒ ν ◠&shr{κ}ty.
- Proof.
- iIntros (tid) "#LFT [#Hord #Hκ']". unfold has_type.
- destruct (eval_expr ν) as [[[|l|]|]|];
- try by (iDestruct "Hκ'" as "[]" || iDestruct "Hκ'" as (l) "[% _]").
- iDestruct "Hκ'" as (l') "[EQ Hκ']". iDestruct "EQ" as %[=]. subst l'.
- iModIntro. iExists _. iSplit. done. by iApply (ty_shr_mono with "LFT Hord Hκ'").
- Qed.
-
- Lemma borrowing_perm_incl κ Ï Ï1 Ï2 θ :
- borrowing κ Ï Ï1 Ï2 → Ï âˆ— κ ∋ θ ∗ Ï1 ⇒ Ï2 ∗ κ ∋ (θ ∗ Ï1).
- Proof.
- iIntros (Hbor tid) "LFT (HÏ&Hθ&HÏ1)". iMod (Hbor with "LFT HÏ HÏ1") as "[$ HÏ1]".
- iIntros "!>#H†". iSplitL "Hθ". by iApply "Hθ". by iApply "HÏ1".
- Qed.
-
- Lemma own_uniq_borrowing ν q ty κ :
- borrowing κ ⊤ (ν ◠own q ty) (ν ◠&uniq{κ} ty).
- Proof.
- iIntros (tid) "#LFT _ Hown". unfold has_type.
- destruct (eval_expr ν) as [[[|l|]|]|];
- try by (iDestruct "Hown" as "[]" || iDestruct "Hown" as (l) "[% _]").
- iDestruct "Hown" as (l') "[EQ [Hown Hf]]". iDestruct "EQ" as %[=]. subst l'.
- iApply (fupd_mask_mono (↑lftN)). done.
- iMod (bor_create with "LFT Hown") as "[Hbor Hext]". done.
- iSplitL "Hbor". by simpl; eauto.
- iIntros "!>#H†". iExists _. iMod ("Hext" with "H†") as "$". by iFrame.
- Qed.
-
- Lemma rebor_uniq_borrowing κ κ' ν ty :
- borrowing κ (κ ⊑ κ') (ν ◠&uniq{κ'}ty) (ν ◠&uniq{κ}ty).
- Proof.
- iIntros (tid) "#LFT #Hord H". unfold has_type.
- destruct (eval_expr ν) as [[[|l|]|]|];
- try by (iDestruct "H" as "[]" || iDestruct "H" as (l) "[% _]").
- iDestruct "H" as (l') "[EQ H]". iDestruct "EQ" as %[=]. subst l'.
- iApply (fupd_mask_mono (↑lftN)). done.
- iMod (rebor with "LFT Hord H") as "[H Hextr]". done.
- iModIntro. iSplitL "H". iExists _. by eauto.
- iIntros "H†". iExists _. by iMod ("Hextr" with "H†") as "$".
- Qed.
-
- Lemma lftincl_borrowing κ κ' q : borrowing κ ⊤ q.[κ'] (κ ⊑ κ').
- Proof.
- iIntros (tid) "#LFT _ Htok". iApply (fupd_mask_mono (↑lftN)). done.
- iMod (bor_create with "LFT [$Htok]") as "[Hbor Hclose]". done.
- iMod (bor_fracture (λ q', (q * q').[κ'])%I with "LFT [Hbor]") as "Hbor". done.
- { by rewrite Qp_mult_1_r. }
- iSplitL "Hbor". iApply (frac_bor_incl with "LFT Hbor").
- iIntros "!>H". by iMod ("Hclose" with "H") as ">$".
- Qed.
-
-End props.
+End product_split.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
new file mode 100644
index 0000000000000000000000000000000000000000..2de7fbda62ee51aca0e1e38cd59471bdb64fa804
--- /dev/null
+++ b/theories/typing/shr_bor.v
@@ -0,0 +1,116 @@
+From iris.proofmode Require Import tactics.
+From lrust.lifetime Require Import frac_borrow.
+From lrust.typing Require Export type.
+From lrust.typing Require Import perm type_incl typing own uniq_bor.
+
+Section shr_bor.
+ Context `{iris_typeG Σ}.
+
+ Program Definition shr_bor (κ : lft) (ty : type) : type :=
+ {| st_size := 1;
+ st_own tid vl :=
+ (∃ (l:loc), ⌜vl = [ #l ]⌠∗ ty.(ty_shr) κ tid (↑lrustN) l)%I |}.
+ Next Obligation.
+ iIntros (κ ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
+ Qed.
+
+End shr_bor.
+
+Notation "&shr{ κ } ty" := (shr_bor κ ty)
+ (format "&shr{ κ } ty", at level 20, right associativity) : lrust_type_scope.
+
+Section typing.
+ Context `{iris_typeG Σ}.
+
+ Lemma perm_incl_share q ν κ ty :
+ ν ◠&uniq{κ} ty ∗ q.[κ] ⇒ ν ◠&shr{κ} ty ∗ q.[κ].
+ Proof.
+ iIntros (tid) "#LFT [Huniq [Htok $]]". unfold has_type.
+ destruct (eval_expr ν); last by iDestruct "Huniq" as "[]".
+ iDestruct "Huniq" as (l) "[% Hown]".
+ iMod (ty.(ty_share) _ lrustN with "LFT Hown Htok") as "[Hown $]"; [solve_ndisj|done|].
+ iIntros "!>/=". eauto.
+ Qed.
+
+ Lemma rebor_shr_perm_incl κ κ' ν ty :
+ κ ⊑ κ' ∗ ν ◠&shr{κ'}ty ⇒ ν ◠&shr{κ}ty.
+ Proof.
+ iIntros (tid) "#LFT [#Hord #Hκ']". unfold has_type.
+ destruct (eval_expr ν) as [[[|l|]|]|];
+ try by (iDestruct "Hκ'" as "[]" || iDestruct "Hκ'" as (l) "[% _]").
+ iDestruct "Hκ'" as (l') "[EQ Hκ']". iDestruct "EQ" as %[=]. subst l'.
+ iModIntro. iExists _. iSplit. done. by iApply (ty_shr_mono with "LFT Hord Hκ'").
+ Qed.
+
+ Lemma lft_incl_ty_incl_shr_bor ty κ1 κ2 :
+ ty_incl (κ1 ⊑ κ2) (&shr{κ2}ty) (&shr{κ1}ty).
+ Proof.
+ iIntros (tid) "#LFT #Hincl!>". iSplit; iIntros "!#*H".
+ - iDestruct "H" as (l) "(% & H)". subst. iExists _.
+ iSplit. done. by iApply (ty.(ty_shr_mono) with "LFT Hincl").
+ - iDestruct "H" as (vl) "#[Hfrac Hty]". iSplit; last done.
+ iExists vl. iFrame "#". iNext.
+ iDestruct "Hty" as (l0) "(% & Hty)". subst. iExists _. iSplit. done.
+ by iApply (ty_shr_mono with "LFT Hincl Hty").
+ Qed.
+
+ Lemma consumes_copy_shr_bor ty κ κ' q:
+ Copy ty →
+ consumes ty (λ ν, ν ◠&shr{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
+ (λ ν, ν ◠&shr{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
+ Proof.
+ iIntros (? ν tid Φ E ?) "#LFT (H◠& #H⊑ & Htok) 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 #Hshr]". iDestruct "Heq" as %[=->].
+ iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
+ rewrite (union_difference_L (↑lrustN) ⊤); last done.
+ setoid_rewrite ->na_own_union; try set_solver. iDestruct "Htl" as "[Htl ?]".
+ iMod (copy_shr_acc with "LFT Hshr [$Htok $Htl]") as (q'') "[H↦ Hclose']"; try set_solver.
+ iDestruct "H↦" as (vl) "[>H↦ #Hown]".
+ iAssert (â–· ⌜length vl = ty_size tyâŒ)%I with "[#]" as ">%".
+ by rewrite ty.(ty_size_eq).
+ iModIntro. iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦".
+ iMod ("Hclose'" with "[H↦]") as "[Htok $]". iExists _; by iFrame.
+ iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
+ Qed.
+
+ Lemma typed_deref_shr_bor_own ty ν κ κ' q q':
+ typed_step (ν ◠&shr{κ} own q' ty ∗ κ' ⊑ κ ∗ q.[κ'])
+ (!ν)
+ (λ v, v ◠&shr{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
+ Proof.
+ iIntros (tid) "!#(#HEAP & #LFT & (H◠& #H⊑ & Htok) & $)". wp_bind ν.
+ 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↦]". iDestruct "Heq" as %[=->].
+ iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[[Htok1 Htok2] Hclose]". done.
+ iDestruct "H↦" as (vl) "[H↦b #Hown]".
+ iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
+ iApply (wp_fupd_step _ (⊤∖↑lrustN) with "[Hown Htok2]"); try done.
+ - iApply ("Hown" with "* [%] Htok2"). set_solver.
+ - wp_read. iIntros "!>[Hshr ?]". iFrame "H⊑".
+ iSplitL "Hshr"; first by iExists _; auto. iApply ("Hclose" with ">").
+ iFrame. iApply "Hclose'". auto.
+ Qed.
+
+ Lemma typed_deref_shr_bor_bor ty ν κ κ' κ'' q:
+ typed_step (ν ◠&shr{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ q.[κ] ∗ κ' ⊑ κ'')
+ (!ν)
+ (λ v, v ◠&shr{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
+ Proof.
+ iIntros (tid) "!#(#HEAP & #LFT & (H◠& #H⊑1 & Htok & #H⊑2) & $)". wp_bind ν.
+ 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 Hshr]".
+ iDestruct "Heq" as %[=->]. iDestruct "Hshr" as (l') "[H↦ Hown]".
+ iMod (lft_incl_acc with "H⊑1 Htok") as (q') "[[Htok1 Htok2] Hclose]". done.
+ iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
+ iAssert (κ' ⊑ κ'' ∪ κ')%I as "#H⊑3".
+ { iApply (lft_incl_glb with "H⊑2 []"). iApply lft_incl_refl. }
+ iMod (lft_incl_acc with "H⊑3 Htok2") as (q''') "[Htok Hclose'']". done.
+ iApply (wp_fupd_step _ (_∖_) with "[Hown Htok]"); try done.
+ - iApply ("Hown" with "* [%] Htok"). set_solver.
+ - wp_read. iIntros "!>[Hshr Htok]". iFrame "H⊑1". iSplitL "Hshr".
+ + iExists _. iSplitR. done. by iApply (ty_shr_mono with "LFT H⊑3 Hshr").
+ + iApply ("Hclose" with ">"). iMod ("Hclose'" with "[$H↦]") as "$".
+ by iMod ("Hclose''" with "Htok") as "$".
+ Qed.
+End typing.
\ No newline at end of file
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
new file mode 100644
index 0000000000000000000000000000000000000000..cc1b14fd6a84f5e75c545fff69a9c06cab47d3e1
--- /dev/null
+++ b/theories/typing/sum.v
@@ -0,0 +1,160 @@
+From iris.proofmode Require Import tactics.
+From lrust.lifetime Require Import borrow frac_borrow.
+From lrust.typing Require Export type.
+From lrust.typing Require Import type_incl.
+
+Section sum.
+ Context `{iris_typeG Σ}.
+
+ (* [emp] cannot be defined using [ty_of_st], because the least we
+ would be able to prove from its [ty_shr] would be [â–· False], but
+ we really need [False] to prove [ty_incl_emp]. *)
+ Program Definition emp :=
+ {| ty_size := 0; ty_own tid vl := False%I; ty_shr κ tid E l := False%I |}.
+ Next Obligation. iIntros (tid vl) "[]". Qed.
+ Next Obligation.
+ iIntros (????????) "#LFT Hb Htok".
+ iMod (bor_exists with "LFT Hb") as (vl) "Hb". set_solver.
+ iMod (bor_sep with "LFT Hb") as "[_ Hb]". set_solver.
+ iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]". set_solver.
+ Qed.
+ Next Obligation. intros. iIntros "_ _ []". Qed.
+ Global Instance emp_empty : Empty type := emp.
+
+ Global Program Instance emp_copy : Copy emp.
+ Next Obligation. intros. iIntros "_ []". Qed.
+
+ Lemma split_sum_mt l tid q tyl :
+ (l ↦∗{q}: λ vl,
+ ∃ (i : nat) vl', ⌜vl = #i :: vl'⌠∗ ty_own (nth i tyl ∅) tid vl')%I
+ ⊣⊢ ∃ (i : nat), l ↦{q} #i ∗ shift_loc l 1 ↦∗{q}: ty_own (nth i tyl ∅) tid.
+ Proof.
+ iSplit; iIntros "H".
+ - iDestruct "H" as (vl) "[Hmt Hown]". iDestruct "Hown" as (i vl') "[% Hown]".
+ subst. iExists i. iDestruct (heap_mapsto_vec_cons with "Hmt") as "[$ Hmt]".
+ iExists vl'. by iFrame.
+ - iDestruct "H" as (i) "[Hmt1 Hown]". iDestruct "Hown" as (vl) "[Hmt2 Hown]".
+ iExists (#i::vl). rewrite heap_mapsto_vec_cons. iFrame. eauto.
+ Qed.
+
+ Class LstTySize (n : nat) (tyl : list type) :=
+ size_eq : Forall ((= n) ∘ ty_size) tyl.
+ Instance LstTySize_nil n : LstTySize n nil := List.Forall_nil _.
+ Lemma LstTySize_cons n ty tyl :
+ ty.(ty_size) = n → LstTySize n tyl → LstTySize n (ty :: tyl).
+ Proof. intros. constructor; done. Qed.
+
+ Lemma sum_size_eq n tid i tyl vl {Hn : LstTySize n tyl} :
+ ty_own (nth i tyl ∅) tid vl -∗ ⌜length vl = nâŒ.
+ Proof.
+ iIntros "Hown". iDestruct (ty_size_eq with "Hown") as %->.
+ revert Hn. rewrite /LstTySize List.Forall_forall /= =>Hn.
+ edestruct nth_in_or_default as [| ->]. by eauto.
+ iDestruct "Hown" as "[]".
+ Qed.
+
+ Program Definition sum {n} (tyl : list type) {_:LstTySize n tyl} :=
+ {| ty_size := S n;
+ ty_own tid vl :=
+ (∃ (i : nat) vl', ⌜vl = #i :: vl'⌠∗ (nth i tyl ∅).(ty_own) tid vl')%I;
+ ty_shr κ tid N l :=
+ (∃ (i : nat), (&frac{κ} λ q, l ↦{q} #i) ∗
+ (nth i tyl ∅).(ty_shr) κ tid N (shift_loc l 1))%I
+ |}.
+ Next Obligation.
+ iIntros (n tyl Hn tid vl) "Hown". iDestruct "Hown" as (i vl') "(%&Hown)".
+ subst. simpl. by iDestruct (sum_size_eq with "Hown") as %->.
+ Qed.
+ Next Obligation.
+ intros n tyl Hn E N κ l tid q ??. iIntros "#LFT Hown Htok". rewrite split_sum_mt.
+ iMod (bor_exists with "LFT Hown") as (i) "Hown". set_solver.
+ iMod (bor_sep with "LFT Hown") as "[Hmt Hown]". set_solver.
+ iMod ((nth i tyl ∅).(ty_share) with "LFT Hown Htok") as "[#Hshr $]"; try done.
+ iMod (bor_fracture with "LFT [-]") as "H"; last by eauto. set_solver. iFrame.
+ Qed.
+ Next Obligation.
+ intros n tyl Hn κ κ' tid E E' l ?. iIntros "#LFT #Hord H".
+ iDestruct "H" as (i) "[Hown0 Hown]". iExists i. iSplitL "Hown0".
+ by iApply (frac_bor_shorten with "Hord").
+ iApply ((nth i tyl ∅).(ty_shr_mono) with "LFT Hord"); last done. done.
+ Qed.
+
+ (* TODO : Make the Forall parameter a typeclass *)
+ Global Program Instance sum_copy `(LstTySize n tyl) :
+ Forall Copy tyl → Copy (sum tyl).
+ Next Obligation.
+ intros n tyl Hn HFA tid vl.
+ cut (∀ i vl', PersistentP (ty_own (nth i tyl ∅) tid vl')). by apply _.
+ intros. apply @copy_persistent. edestruct nth_in_or_default as [| ->];
+ [by eapply List.Forall_forall| apply _].
+ Qed.
+ Next Obligation.
+ intros n tyl Hn HFA κ tid E F l q ?.
+ iIntros "#LFT #H[[Htok1 Htok2] Htl]".
+ setoid_rewrite split_sum_mt. iDestruct "H" as (i) "[Hshr0 Hshr]".
+ iMod (frac_bor_acc with "LFT Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver.
+ iMod (@copy_shr_acc _ _ (nth i tyl ∅) with "LFT Hshr [Htok2 $Htl]")
+ as (q'2) "[Hownq Hclose']"; try done.
+ { edestruct nth_in_or_default as [| ->]; last by apply _.
+ by eapply List.Forall_forall. }
+ destruct (Qp_lower_bound q'1 q'2) as (q' & q'01 & q'02 & -> & ->).
+ rewrite -{1}heap_mapsto_vec_prop_op; last (by intros; apply sum_size_eq, Hn).
+ iDestruct "Hownq" as "[Hownq1 Hownq2]". iDestruct "Hown" as "[Hown1 Hown2]".
+ iExists q'. iModIntro. iSplitL "Hown1 Hownq1".
+ - iNext. iExists i. by iFrame.
+ - iIntros "H". iDestruct "H" as (i') "[Hown1 Hownq1]".
+ iCombine "Hown1" "Hown2" as "Hown". rewrite heap_mapsto_op.
+ iDestruct "Hown" as "[>#Hi Hown]". iDestruct "Hi" as %[= ->%Z_of_nat_inj].
+ iMod ("Hclose" with "Hown") as "$".
+ iCombine "Hownq1" "Hownq2" as "Hownq".
+ rewrite heap_mapsto_vec_prop_op; last (by intros; apply sum_size_eq, Hn).
+ by iApply "Hclose'".
+ Qed.
+
+End sum.
+
+Existing Instance LstTySize_nil.
+Hint Extern 1 (LstTySize _ (_ :: _)) =>
+ apply LstTySize_cons; [compute; reflexivity|] : typeclass_instances.
+
+
+(* Σ is commonly used for the current functor. So it cannot be defined
+ as Î for products. We stick to the following form. *)
+Notation "Σ[ ty1 ; .. ; tyn ]" :=
+ (sum (cons ty1 (..(cons tyn nil)..))) : lrust_type_scope.
+
+Section incl.
+ Context `{iris_typeG Σ}.
+
+ Lemma ty_incl_emp Ï ty : ty_incl Ï âˆ… ty.
+ Proof. iIntros (tid) "_ _!>". iSplit; iIntros "!#*/=[]". Qed.
+
+ Lemma ty_incl_sum Ï n tyl1 tyl2 (_ : LstTySize n tyl1) (_ : LstTySize n tyl2) :
+ Duplicable Ï â†’ Forall2 (ty_incl Ï) tyl1 tyl2 →
+ ty_incl Ï (sum tyl1) (sum tyl2).
+ Proof.
+ iIntros (DUP FA tid) "#LFT #HÏ". rewrite /sum /=. iSplitR "".
+ - assert (Hincl : lft_ctx -∗ Ï tid ={⊤}=∗
+ (□ ∀ i vl, (nth i tyl1 ∅%T).(ty_own) tid vl
+ → (nth i tyl2 ∅%T).(ty_own) tid vl)).
+ { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
+ - iIntros "_ _!>*!#". eauto.
+ - iIntros "#LFT #HÏ". iMod (IH with "LFT HÏ") as "#IH".
+ iMod (Hincl with "LFT HÏ") as "[#Hh _]".
+ iIntros "!>*!#*Hown". destruct i as [|i]. by iApply "Hh". by iApply "IH". }
+ iMod (Hincl with "LFT HÏ") as "#Hincl". iIntros "!>!#*H".
+ iDestruct "H" as (i vl') "[% Hown]". subst. iExists _, _. iSplit. done.
+ by iApply "Hincl".
+ - assert (Hincl : lft_ctx -∗ Ï tid ={⊤}=∗
+ (□ ∀ i κ E l, (nth i tyl1 ∅%T).(ty_shr) κ tid E l
+ → (nth i tyl2 ∅%T).(ty_shr) κ tid E l)).
+ { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
+ - iIntros "#LFT _!>*!#". eauto.
+ - iIntros "#LFT #HÏ".
+ iMod (IH with "LFT HÏ") as "#IH". iMod (Hincl with "LFT HÏ") as "[_ #Hh]".
+ iIntros "!>*!#*Hown". destruct i as [|i]; last by iApply "IH".
+ by iDestruct ("Hh" $! _ _ _ with "Hown") as "[$ _]". }
+ iMod (Hincl with "LFT HÏ") as "#Hincl". iIntros "!>!#*H". iSplit; last done.
+ iDestruct "H" as (i) "[??]". iExists _. iSplit. done. by iApply "Hincl".
+ Qed.
+End incl.
\ No newline at end of file
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 1ead6901876028ef759489100257faaa68afdbd5..32990b8dcbe93e19e09e9bcfc21227b58663d76d 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -1,8 +1,5 @@
-From Coq Require Import Qcanon.
-From iris.base_logic Require Import big_op.
From iris.base_logic.lib Require Export na_invariants.
-From iris.program_logic Require Import hoare.
-From lrust.lang Require Export heap notation.
+From lrust.lang Require Import heap.
From lrust.lifetime Require Import borrow frac_borrow reborrow.
Class iris_typeG Σ := Iris_typeG {
@@ -15,469 +12,97 @@ Class iris_typeG Σ := Iris_typeG {
Definition mgmtE := ↑lftN.
Definition lrustN := nroot .@ "lrust".
-(* [perm] is defined here instead of perm.v in order to define [cont] *)
-Definition perm {Σ} := thread_id → iProp Σ.
-
Section type.
-
-Context `{iris_typeG Σ}.
-
-Record type :=
- { ty_size : nat;
- ty_dup : bool;
- ty_own : thread_id → list val → iProp Σ;
- ty_shr : lft → thread_id → coPset → loc → iProp Σ;
-
- ty_dup_persistent tid vl : ty_dup → PersistentP (ty_own tid vl);
- ty_shr_persistent κ tid E l : PersistentP (ty_shr κ tid E l);
-
- ty_size_eq tid vl : ty_own tid vl -∗ ⌜length vl = ty_sizeâŒ;
- (* The mask for starting the sharing does /not/ include the
- namespace N, for allowing more flexibility for the user of
- this type (typically for the [own] type). AFAIK, there is no
- fundamental reason for this.
-
- This should not be harmful, since sharing typically creates
- invariants, which does not need the mask. Moreover, it is
- more consistent with thread-local tokens, which we do not
- give any. *)
- ty_share E N κ l tid q : mgmtE ⊥ ↑N → mgmtE ⊆ E →
- lft_ctx -∗ &{κ} (l ↦∗: ty_own tid) -∗ q.[κ] ={E}=∗ ty_shr κ tid (↑N) l ∗ q.[κ];
- ty_shr_mono κ κ' tid E E' l : E ⊆ E' →
- lft_ctx -∗ κ' ⊑ κ -∗ ty_shr κ tid E l -∗ ty_shr κ' tid E' l;
- ty_shr_acc κ tid E F l q :
- ty_dup → mgmtE ∪ F ⊆ E →
- lft_ctx -∗ ty_shr κ tid F l -∗
- q.[κ] ∗ na_own tid F ={E}=∗ ∃ q', ▷l ↦∗{q'}: ty_own tid ∗
- (▷l ↦∗{q'}: ty_own tid ={E}=∗ q.[κ] ∗ na_own tid F)
- }.
-Global Existing Instances ty_shr_persistent ty_dup_persistent.
-
-(* We are repeating the typeclass parameter here jsut to make sure
- that simple_type does depend on it. Otherwise, the coercion defined
- bellow will not be acceptable by Coq. *)
-Record simple_type `{iris_typeG Σ} :=
- { st_size : nat;
- st_own : thread_id → list val → iProp Σ;
-
- st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = st_sizeâŒ;
- st_own_persistent tid vl : PersistentP (st_own tid vl) }.
-Global Existing Instance st_own_persistent.
-
-Program Definition ty_of_st (st : simple_type) : type :=
- {| ty_size := st.(st_size); ty_dup := true;
- ty_own := st.(st_own);
-
- (* [st.(st_own) tid vl] needs to be outside of the fractured
- borrow, otherwise I do not know how to prove the shr part of
- [lft_incl_ty_incl_shared_borrow]. *)
- ty_shr := λ κ tid _ l,
- (∃ vl, (&frac{κ} λ q, l ↦∗{q} vl) ∗ ▷ st.(st_own) tid vl)%I
- |}.
-Next Obligation. intros. apply st_size_eq. Qed.
-Next Obligation.
- intros st E N κ l tid q ? ?. iIntros "#LFT Hmt Htok".
- iMod (bor_exists with "LFT Hmt") as (vl) "Hmt". set_solver.
- iMod (bor_sep with "LFT Hmt") as "[Hmt Hown]". set_solver.
- iMod (bor_persistent with "LFT Hown Htok") as "[Hown $]". set_solver.
- iMod (bor_fracture with "LFT [Hmt]") as "Hfrac"; last first.
- { iExists vl. by iFrame. }
- done. set_solver.
-Qed.
-Next Obligation.
- intros st κ κ' tid E E' l ?. iIntros "#LFT #Hord H".
- iDestruct "H" as (vl) "[Hf Hown]".
- iExists vl. iFrame. by iApply (frac_bor_shorten with "Hord").
-Qed.
-Next Obligation.
- intros st κ tid E F l q ??. iIntros "#LFT #Hshr[Hlft $]".
- iDestruct "Hshr" as (vl) "[Hf Hown]".
- iMod (frac_bor_acc with "LFT Hf Hlft") as (q') "[Hmt Hclose]"; first set_solver.
- iModIntro. iExists _. iDestruct "Hmt" as "[Hmt1 Hmt2]". iSplitL "Hmt1".
- - iNext. iExists _. by iFrame.
- - iIntros "Hmt1". iDestruct "Hmt1" as (vl') "[Hmt1 #Hown']".
- iAssert (â–· ⌜length vl = length vl'âŒ)%I as ">%".
- { iNext.
- iDestruct (st_size_eq with "Hown") as %->.
- iDestruct (st_size_eq with "Hown'") as %->. done. }
- iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op // Qp_div_2.
- iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose".
-Qed.
-
-End type.
-
-Coercion ty_of_st : simple_type >-> type.
-
-Hint Extern 0 (Is_true _.(ty_dup)) =>
- exact I || assumption : typeclass_instances.
-
-Delimit Scope lrust_type_scope with T.
-Bind Scope lrust_type_scope with type.
-
-Module Types.
-Section types.
-
Context `{iris_typeG Σ}.
- (* [emp] cannot be defined using [ty_of_st], because the least we
- would be able to prove from its [ty_shr] would be [â–· False], but
- we really need [False] to prove [ty_incl_emp]. *)
- Program Definition emp :=
- {| ty_size := 0; ty_dup := true;
- ty_own tid vl := False%I; ty_shr κ tid E l := False%I |}.
- Next Obligation. iIntros (tid vl) "[]". Qed.
- Next Obligation.
- iIntros (????????) "#LFT Hb Htok".
- iMod (bor_exists with "LFT Hb") as (vl) "Hb". set_solver.
- iMod (bor_sep with "LFT Hb") as "[_ Hb]". set_solver.
- iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]". set_solver.
- Qed.
- Next Obligation. intros. iIntros "_ _ []". Qed.
- Next Obligation. intros. iIntros "_ []". Qed.
-
- Program Definition unit : type :=
- {| st_size := 0; st_own tid vl := ⌜vl = []âŒ%I |}.
- Next Obligation. iIntros (tid vl) "%". simpl. by subst. Qed.
-
- 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.
-
- 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.
-
- Program Definition own (q : Qp) (ty : type) :=
- {| ty_size := 1; ty_dup := false;
- 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 [ty_incl_own].
-
- Since this assertion is timeless, this should not cause
- problems. *)
- (∃ l:loc, ⌜vl = [ #l ]⌠∗ ▷ l ↦∗: ty.(ty_own) tid ∗ ▷ †{q}l…ty.(ty_size))%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. done. Qed.
- 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.
- Next Obligation. done. Qed.
-
- Program Definition uniq_bor (κ:lft) (ty:type) :=
- {| ty_size := 1; ty_dup := false;
- ty_own tid vl :=
- (∃ l:loc, ⌜vl = [ #l ]⌠∗ &{κ} l ↦∗: ty.(ty_own) tid)%I;
- ty_shr κ' tid E l :=
- (∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
- □ ∀ q' F, ⌜E ∪ mgmtE ⊆ F⌠→ q'.[κ∪κ']
- ={F, F∖E∖↑lftN}▷=∗ ty.(ty_shr) (κ∪κ') tid E l' ∗ q'.[κ∪κ'])%I
- |}.
- Next Obligation. done. Qed.
- Next Obligation.
- iIntros (q ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
- Qed.
- Next Obligation.
- move=> κ 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_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "Hbf". set_solver.
- rewrite {1}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_unnest _ _ _ (l' ↦∗: ty_own ty tid)%I with "LFT [Hbtok]") as "Hb".
- { set_solver. } { iApply bor_unfold_idx. eauto. }
- iModIntro. iNext. iMod "Hb".
- iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]"; try done. set_solver.
- iApply "Hclose". eauto.
- - iMod ("Hclose" with "[]") as "_". by eauto.
- iApply step_fupd_mask_mono; last by eauto. done. set_solver.
- Qed.
- Next Obligation.
- intros κ0 ty κ κ' tid E E' l ?. iIntros "#LFT #Hκ #H".
- iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0∪κ' ⊑ κ0∪κ)%I as "#Hκ0".
- { iApply (lft_incl_glb with "[] []").
- - iApply lft_le_incl. apply gmultiset_union_subseteq_l.
- - iApply (lft_incl_trans with "[] Hκ").
- iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
- iExists l'. iSplit. by iApply (frac_bor_shorten with "[]").
- iIntros "!#". iIntros (q F) "% Htok".
- iApply (step_fupd_mask_mono F _ _ (F∖E∖ ↑lftN)). set_solver. set_solver.
- iMod (lft_incl_acc with "Hκ0 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_shr_mono with "LFT Hκ0").
- Qed.
- Next Obligation. done. Qed.
-
- Program Definition shared_bor (κ : lft) (ty : type) : type :=
- {| st_size := 1;
- st_own tid vl :=
- (∃ (l:loc), ⌜vl = [ #l ]⌠∗ ty.(ty_shr) κ tid (↑lrustN) l)%I |}.
- Next Obligation.
- iIntros (κ ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
- Qed.
-
- Lemma split_prod_mt tid ty1 ty2 q l :
- (l ↦∗{q}: λ vl,
- ∃ vl1 vl2, ⌜vl = vl1 ++ vl2⌠∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I
- ⊣⊢ l ↦∗{q}: ty1.(ty_own) tid ∗ shift_loc l ty1.(ty_size) ↦∗{q}: ty2.(ty_own) tid.
- Proof.
- iSplit; iIntros "H".
- - iDestruct "H" as (vl) "[H↦ H]". iDestruct "H" as (vl1 vl2) "(% & H1 & H2)".
- subst. rewrite heap_mapsto_vec_app. iDestruct "H↦" as "[H↦1 H↦2]".
- iDestruct (ty_size_eq with "H1") as %->.
- iSplitL "H1 H↦1"; iExists _; iFrame.
- - iDestruct "H" as "[H1 H2]". iDestruct "H1" as (vl1) "[H↦1 H1]".
- iDestruct "H2" as (vl2) "[H↦2 H2]". iExists (vl1 ++ vl2).
- rewrite heap_mapsto_vec_app. iDestruct (ty_size_eq with "H1") as %->.
- iFrame. iExists _, _. by iFrame.
- Qed.
+ Record type :=
+ { ty_size : nat;
+ ty_own : thread_id → list val → iProp Σ;
+ ty_shr : lft → thread_id → coPset → loc → iProp Σ;
+
+ ty_shr_persistent κ tid E l : PersistentP (ty_shr κ tid E l);
+
+ ty_size_eq tid vl : ty_own tid vl -∗ ⌜length vl = ty_sizeâŒ;
+ (* The mask for starting the sharing does /not/ include the
+ namespace N, for allowing more flexibility for the user of
+ this type (typically for the [own] type). AFAIK, there is no
+ fundamental reason for this.
+
+ This should not be harmful, since sharing typically creates
+ invariants, which does not need the mask. Moreover, it is
+ more consistent with thread-local tokens, which we do not
+ give any. *)
+ ty_share E N κ l tid q : mgmtE ⊥ ↑N → mgmtE ⊆ E →
+ lft_ctx -∗ &{κ} (l ↦∗: ty_own tid) -∗ q.[κ] ={E}=∗ ty_shr κ tid (↑N) l ∗ q.[κ];
+ ty_shr_mono κ κ' tid E E' l : E ⊆ E' →
+ lft_ctx -∗ κ' ⊑ κ -∗ ty_shr κ tid E l -∗ ty_shr κ' tid E' l
+ }.
+ Global Existing Instances ty_shr_persistent.
+
+ Class Copy (t : type) := {
+ copy_persistent tid vl : PersistentP (t.(ty_own) tid vl);
+ copy_shr_acc κ tid E F l q :
+ mgmtE ∪ F ⊆ E →
+ lft_ctx -∗ t.(ty_shr) κ tid F l -∗
+ q.[κ] ∗ na_own tid F ={E}=∗ ∃ q', ▷l ↦∗{q'}: t.(ty_own) tid ∗
+ (▷l ↦∗{q'}: t.(ty_own) tid ={E}=∗ q.[κ] ∗ na_own tid F)
+ }.
+ Global Existing Instances copy_persistent.
- Program Definition product2 (ty1 ty2 : type) :=
- {| ty_size := ty1.(ty_size) + ty2.(ty_size);
- ty_dup := ty1.(ty_dup) && ty2.(ty_dup);
- ty_own tid vl := (∃ vl1 vl2,
- ⌜vl = vl1 ++ vl2⌠∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I;
- ty_shr κ tid E l :=
- (∃ E1 E2, ⌜E1 ⊥ E2 ∧ E1 ⊆ E ∧ E2 ⊆ E⌠∗
- ty1.(ty_shr) κ tid E1 l ∗
- ty2.(ty_shr) κ tid E2 (shift_loc l ty1.(ty_size)))%I |}.
- Next Obligation. intros ty1 ty2 tid vl [Hdup1 Hdup2]%andb_True. apply _. Qed.
- Next Obligation.
- iIntros (ty1 ty2 tid vl) "H". iDestruct "H" as (vl1 vl2) "(% & H1 & H2)".
- subst. rewrite app_length !ty_size_eq.
- iDestruct "H1" as %->. iDestruct "H2" as %->. done.
- Qed.
- Next Obligation.
- intros ty1 ty2 E N κ l tid q ??. iIntros "#LFT /=H Htok".
- rewrite split_prod_mt.
- iMod (bor_sep with "LFT H") as "[H1 H2]". set_solver.
- iMod (ty1.(ty_share) _ (N .@ 1) with "LFT H1 Htok") as "[? Htok]". solve_ndisj. done.
- iMod (ty2.(ty_share) _ (N .@ 2) with "LFT H2 Htok") as "[? $]". solve_ndisj. done.
- iModIntro. iExists (↑N .@ 1). iExists (↑N .@ 2). iFrame.
- iPureIntro. split. solve_ndisj. split; apply nclose_subseteq.
- Qed.
- Next Obligation.
- intros ty1 ty2 κ κ' tid E E' l ?. iIntros "#LFT /= #H⊑ H".
- iDestruct "H" as (N1 N2) "(% & H1 & H2)". iExists N1, N2.
- iSplit. iPureIntro. set_solver.
- iSplitL "H1"; by iApply (ty_shr_mono with "LFT H⊑").
- Qed.
- Next Obligation.
- intros ty1 ty2 κ tid E F l q [Hdup1 Hdup2]%andb_True ?.
- iIntros "#LFT H[[Htok1 Htok2] Htl]". iDestruct "H" as (E1 E2) "(% & H1 & H2)".
- assert (F = E1 ∪ E2 ∪ F∖(E1 ∪ E2)) as ->.
- { rewrite -union_difference_L; set_solver. }
- repeat setoid_rewrite na_own_union; first last.
- set_solver. set_solver. set_solver. set_solver.
- iDestruct "Htl" as "[[Htl1 Htl2] $]".
- iMod (ty1.(ty_shr_acc) with "LFT H1 [$Htok1 $Htl1]") as (q1) "[H1 Hclose1]".
- done. set_solver.
- iMod (ty2.(ty_shr_acc) with "LFT H2 [$Htok2 $Htl2]") as (q2) "[H2 Hclose2]".
- done. set_solver.
- destruct (Qp_lower_bound q1 q2) as (qq & q'1 & q'2 & -> & ->). iExists qq.
- iDestruct "H1" as (vl1) "[H↦1 H1]". iDestruct "H2" as (vl2) "[H↦2 H2]".
- rewrite !split_prod_mt.
- iAssert (â–· ⌜length vl1 = ty1.(ty_size)âŒ)%I with "[#]" as ">%".
- { iNext. by iApply ty_size_eq. }
- iAssert (â–· ⌜length vl2 = ty2.(ty_size)âŒ)%I with "[#]" as ">%".
- { iNext. by iApply ty_size_eq. }
- iDestruct "H↦1" as "[H↦1 H↦1f]". iDestruct "H↦2" as "[H↦2 H↦2f]".
- iIntros "!>". iSplitL "H↦1 H1 H↦2 H2".
- - iNext. iSplitL "H↦1 H1". iExists vl1. by iFrame. iExists vl2. by iFrame.
- - iIntros "[H1 H2]".
- iDestruct "H1" as (vl1') "[H↦1 H1]". iDestruct "H2" as (vl2') "[H↦2 H2]".
- iAssert (â–· ⌜length vl1' = ty1.(ty_size)âŒ)%I with "[#]" as ">%".
- { iNext. by iApply ty_size_eq. }
- iAssert (â–· ⌜length vl2' = ty2.(ty_size)âŒ)%I with "[#]" as ">%".
- { iNext. by iApply ty_size_eq. }
- iCombine "H↦1" "H↦1f" as "H↦1". iCombine "H↦2" "H↦2f" as "H↦2".
- rewrite !heap_mapsto_vec_op; try by congruence.
- iDestruct "H↦1" as "[_ H↦1]". iDestruct "H↦2" as "[_ H↦2]".
- iMod ("Hclose1" with "[H1 H↦1]") as "[$$]". by iExists _; iFrame.
- iMod ("Hclose2" with "[H2 H↦2]") as "[$$]". by iExists _; iFrame. done.
- Qed.
+ (* We are repeating the typeclass parameter here jsut to make sure
+ that simple_type does depend on it. Otherwise, the coercion defined
+ bellow will not be acceptable by Coq. *)
+ Record simple_type `{iris_typeG Σ} :=
+ { st_size : nat;
+ st_own : thread_id → list val → iProp Σ;
- Definition product := fold_right product2 unit.
+ st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = st_sizeâŒ;
+ st_own_persistent tid vl : PersistentP (st_own tid vl) }.
- Lemma split_sum_mt l tid q tyl :
- (l ↦∗{q}: λ vl,
- ∃ (i : nat) vl', ⌜vl = #i :: vl'⌠∗ ty_own (nth i tyl emp) tid vl')%I
- ⊣⊢ ∃ (i : nat), l ↦{q} #i ∗ shift_loc l 1 ↦∗{q}: ty_own (nth i tyl emp) tid.
- Proof.
- iSplit; iIntros "H".
- - iDestruct "H" as (vl) "[Hmt Hown]". iDestruct "Hown" as (i vl') "[% Hown]".
- subst. iExists i. iDestruct (heap_mapsto_vec_cons with "Hmt") as "[$ Hmt]".
- iExists vl'. by iFrame.
- - iDestruct "H" as (i) "[Hmt1 Hown]". iDestruct "Hown" as (vl) "[Hmt2 Hown]".
- iExists (#i::vl). rewrite heap_mapsto_vec_cons. iFrame. eauto.
- Qed.
+ Global Existing Instance st_own_persistent.
- Class LstTySize (n : nat) (tyl : list type) :=
- size_eq : Forall ((= n) ∘ ty_size) tyl.
- Instance LstTySize_nil n : LstTySize n nil := List.Forall_nil _.
- Lemma LstTySize_cons n ty tyl :
- ty.(ty_size) = n → LstTySize n tyl → LstTySize n (ty :: tyl).
- Proof. intros. constructor; done. Qed.
+ Program Definition ty_of_st (st : simple_type) : type :=
+ {| ty_size := st.(st_size); ty_own := st.(st_own);
- Lemma sum_size_eq n tid i tyl vl {Hn : LstTySize n tyl} :
- ty_own (nth i tyl emp) tid vl -∗ ⌜length vl = nâŒ.
- Proof.
- iIntros "Hown". iDestruct (ty_size_eq with "Hown") as %->.
- revert Hn. rewrite /LstTySize List.Forall_forall /= =>Hn.
- edestruct nth_in_or_default as [| ->]. by eauto.
- iDestruct "Hown" as "[]".
- Qed.
-
- Program Definition sum {n} (tyl : list type) {_:LstTySize n tyl} :=
- {| ty_size := S n; ty_dup := forallb ty_dup tyl;
- ty_own tid vl :=
- (∃ (i : nat) vl', ⌜vl = #i :: vl'⌠∗ (nth i tyl emp).(ty_own) tid vl')%I;
- ty_shr κ tid N l :=
- (∃ (i : nat), (&frac{κ} λ q, l ↦{q} #i) ∗
- (nth i tyl emp).(ty_shr) κ tid N (shift_loc l 1))%I
+ (* [st.(st_own) tid vl] needs to be outside of the fractured
+ borrow, otherwise I do not know how to prove the shr part of
+ [lft_incl_ty_incl_shr_borrow]. *)
+ ty_shr := λ κ tid _ l,
+ (∃ vl, (&frac{κ} λ q, l ↦∗{q} vl) ∗ ▷ st.(st_own) tid vl)%I
|}.
+ Next Obligation. intros. apply st_size_eq. Qed.
Next Obligation.
- intros n tyl Hn tid vl Hdup%Is_true_eq_true.
- cut (∀ i vl', PersistentP (ty_own (nth i tyl emp) tid vl')). apply _.
- intros. apply ty_dup_persistent. edestruct nth_in_or_default as [| ->]; last done.
- rewrite ->forallb_forall in Hdup. auto using Is_true_eq_left.
- Qed.
- Next Obligation.
- iIntros (n tyl Hn tid vl) "Hown". iDestruct "Hown" as (i vl') "(%&Hown)".
- subst. simpl. by iDestruct (sum_size_eq with "Hown") as %->.
- Qed.
- Next Obligation.
- intros n tyl Hn E N κ l tid q ??. iIntros "#LFT Hown Htok". rewrite split_sum_mt.
- iMod (bor_exists with "LFT Hown") as (i) "Hown". set_solver.
- iMod (bor_sep with "LFT Hown") as "[Hmt Hown]". set_solver.
- iMod ((nth i tyl emp).(ty_share) with "LFT Hown Htok") as "[#Hshr $]"; try done.
- iMod (bor_fracture with "LFT [-]") as "H"; last by eauto. set_solver. iFrame.
+ intros st E N κ l tid q ? ?. iIntros "#LFT Hmt Htok".
+ iMod (bor_exists with "LFT Hmt") as (vl) "Hmt". set_solver.
+ iMod (bor_sep with "LFT Hmt") as "[Hmt Hown]". set_solver.
+ iMod (bor_persistent with "LFT Hown Htok") as "[Hown $]". set_solver.
+ iMod (bor_fracture with "LFT [Hmt]") as "Hfrac"; last first.
+ { iExists vl. by iFrame. }
+ done. set_solver.
Qed.
Next Obligation.
- intros n tyl Hn κ κ' tid E E' l ?. iIntros "#LFT #Hord H".
- iDestruct "H" as (i) "[Hown0 Hown]". iExists i. iSplitL "Hown0".
- by iApply (frac_bor_shorten with "Hord").
- iApply ((nth i tyl emp).(ty_shr_mono) with "LFT Hord"); last done. done.
+ intros st κ κ' tid E E' l ?. iIntros "#LFT #Hord H".
+ iDestruct "H" as (vl) "[Hf Hown]".
+ iExists vl. iFrame. by iApply (frac_bor_shorten with "Hord").
Qed.
- Next Obligation.
- intros n tyl Hn κ tid E F l q Hdup%Is_true_eq_true ?.
- iIntros "#LFT #H[[Htok1 Htok2] Htl]".
- setoid_rewrite split_sum_mt. iDestruct "H" as (i) "[Hshr0 Hshr]".
- iMod (frac_bor_acc with "LFT Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver.
- iMod ((nth i tyl emp).(ty_shr_acc) with "LFT Hshr [Htok2 $Htl]")
- as (q'2) "[Hownq Hclose']"; try done.
- { edestruct nth_in_or_default as [| ->]; last done.
- rewrite ->forallb_forall in Hdup. auto using Is_true_eq_left. }
- destruct (Qp_lower_bound q'1 q'2) as (q' & q'01 & q'02 & -> & ->).
- rewrite -{1}heap_mapsto_vec_prop_op; last (by intros; apply sum_size_eq, Hn).
- iDestruct "Hownq" as "[Hownq1 Hownq2]". iDestruct "Hown" as "[Hown1 Hown2]".
- iExists q'. iModIntro. iSplitL "Hown1 Hownq1".
- - iNext. iExists i. by iFrame.
- - iIntros "H". iDestruct "H" as (i') "[Hown1 Hownq1]".
- iCombine "Hown1" "Hown2" as "Hown". rewrite heap_mapsto_op.
- iDestruct "Hown" as "[>#Hi Hown]". iDestruct "Hi" as %[= ->%Z_of_nat_inj].
- iMod ("Hclose" with "Hown") as "$".
- iCombine "Hownq1" "Hownq2" as "Hownq".
- rewrite heap_mapsto_vec_prop_op; last (by intros; apply sum_size_eq, Hn).
- by iApply "Hclose'".
- Qed.
-
- Program Definition uninit : type :=
- {| st_size := 1; st_own tid vl := ⌜length vl = 1%natâŒ%I |}.
- Next Obligation. done. Qed.
- Program Definition cont {n : nat} (Ï : vec val n → @perm Σ) :=
- {| ty_size := 1; ty_dup := false;
- 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. done. Qed.
+ Global Program Instance ty_of_st_copy st : Copy (ty_of_st st).
Next Obligation.
- iIntros (n Ï tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
+ intros st κ tid E F l q ?. iIntros "#LFT #Hshr[Hlft $]".
+ iDestruct "Hshr" as (vl) "[Hf Hown]".
+ iMod (frac_bor_acc with "LFT Hf Hlft") as (q') "[Hmt Hclose]"; first set_solver.
+ iModIntro. iExists _. iDestruct "Hmt" as "[Hmt1 Hmt2]". iSplitL "Hmt1".
+ - iNext. iExists _. by iFrame.
+ - iIntros "Hmt1". iDestruct "Hmt1" as (vl') "[Hmt1 #Hown']".
+ iAssert (â–· ⌜length vl = length vl'âŒ)%I as ">%".
+ { iNext. iDestruct (st_size_eq with "Hown") as %->.
+ iDestruct (st_size_eq with "Hown'") as %->. done. }
+ iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op // Qp_div_2.
+ iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose".
Qed.
- Next Obligation. intros. by iIntros "_ _ $". Qed.
- Next Obligation. intros. by iIntros "_ _ _". Qed.
- Next Obligation. done. 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.
-
-End types.
-
-End Types.
-
-Existing Instance Types.LstTySize_nil.
-Hint Extern 1 (Types.LstTySize _ (_ :: _)) =>
- apply Types.LstTySize_cons; [compute; reflexivity|] : typeclass_instances.
-
-Import Types.
+End type.
-Notation "∅" := emp : lrust_type_scope.
-Notation "&uniq{ κ } ty" := (uniq_bor κ ty)
- (format "&uniq{ κ } ty", at level 20, right associativity) : lrust_type_scope.
-Notation "&shr{ κ } ty" := (shared_bor κ ty)
- (format "&shr{ κ } ty", at level 20, right associativity) : lrust_type_scope.
+Coercion ty_of_st : simple_type >-> type.
-Arguments product : simpl never.
-Notation Î := product.
-(* Σ is commonly used for the current functor. So it cannot be defined
- as Î for products. We stick to the following form. *)
-Notation "Σ[ ty1 ; .. ; tyn ]" :=
- (sum (cons ty1 (..(cons tyn nil)..))) : lrust_type_scope.
+Delimit Scope lrust_type_scope with T.
+Bind Scope lrust_type_scope with type.
diff --git a/theories/typing/type_incl.v b/theories/typing/type_incl.v
index 8fa5349e57d544f3374515552ae9f783b35ab5a2..2bae7738ef1b882f813a74e55b4ea7f9258f9097 100644
--- a/theories/typing/type_incl.v
+++ b/theories/typing/type_incl.v
@@ -1,12 +1,9 @@
From iris.base_logic Require Import big_op.
From iris.program_logic Require Import hoare.
-From lrust.typing Require Export type perm_incl.
+From lrust.typing Require Export type perm.
From lrust.lifetime Require Import frac_borrow borrow.
-Import Types.
-
Section ty_incl.
-
Context `{iris_typeG Σ}.
Definition ty_incl (Ï : perm) (ty1 ty2 : type) :=
@@ -19,9 +16,6 @@ Section ty_incl.
is still included in any other. *)
ty2.(ty_shr) κ tid E l ∗ ⌜ty1.(ty_size) = ty2.(ty_size)âŒ).
- Global Instance ty_incl_refl Ï : Reflexive (ty_incl Ï).
- Proof. iIntros (ty tid) "_ _!>". iSplit; iIntros "!#"; eauto. Qed.
-
Lemma ty_incl_trans Ï Î¸ ty1 ty2 ty3 :
ty_incl Ï ty1 ty2 → ty_incl θ ty2 ty3 → ty_incl (Ï âˆ— θ) ty1 ty3.
Proof.
@@ -43,226 +37,15 @@ Section ty_incl.
Global Instance ty_incl_preorder Ï: Duplicable Ï â†’ PreOrder (ty_incl Ï).
Proof.
- split. apply _.
- eauto using ty_incl_weaken, ty_incl_trans, perm_incl_duplicable.
- Qed.
-
- Lemma ty_incl_emp Ï ty : ty_incl Ï âˆ… ty.
- Proof. iIntros (tid) "_ _!>". iSplit; iIntros "!#*/=[]". Qed.
-
- Lemma ty_incl_own Ï ty1 ty2 q :
- ty_incl Ï ty1 ty2 → ty_incl Ï (own q ty1) (own q ty2).
- Proof.
- iIntros (Hincl tid) "#LFT H/=". iMod (Hincl with "LFT H") as "[#Howni #Hshri]".
- iModIntro. iSplit; iIntros "!#*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.
- - iDestruct "H" as (l') "[Hfb #Hvs]". iSplit; last done. iExists l'. iFrame.
- iIntros "!#". iIntros (q' F) "% Hκ".
- iMod ("Hvs" with "* [%] Hκ") as "Hvs'". done. iModIntro. iNext.
- iMod "Hvs'" as "[Hshr $]". by iDestruct ("Hshri" with "* Hshr") as "[$ _]".
- Qed.
-
- Lemma lft_incl_ty_incl_uniq_bor ty κ1 κ2 :
- ty_incl (κ1 ⊑ κ2) (&uniq{κ2}ty) (&uniq{κ1}ty).
- Proof.
- iIntros (tid) "#LFT #Hincl!>". iSplit; iIntros "!#*H".
- - iDestruct "H" as (l) "[% Hown]". subst. iExists _. iSplit. done.
- by iApply (bor_shorten with "Hincl").
- - iAssert (κ1 ∪ κ ⊑ κ2 ∪ κ)%I as "#Hincl'".
- { iApply (lft_incl_glb with "[] []").
- - iApply (lft_incl_trans with "[] Hincl"). iApply lft_le_incl.
- apply gmultiset_union_subseteq_l.
- - iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
- iSplitL; last done. iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'.
- iFrame. iIntros "!#". iIntros (q' F) "% Htok".
- iMod (lft_incl_acc with "Hincl' Htok") as (q'') "[Htok Hclose]". set_solver.
- iMod ("Hupd" with "* [%] Htok") as "Hupd'"; try done. iModIntro. iNext.
- iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
- by iApply (ty_shr_mono with "LFT Hincl' H").
- Qed.
-
- Lemma lft_incl_ty_incl_shared_bor ty κ1 κ2 :
- ty_incl (κ1 ⊑ κ2) (&shr{κ2}ty) (&shr{κ1}ty).
- Proof.
- iIntros (tid) "#LFT #Hincl!>". iSplit; iIntros "!#*H".
- - iDestruct "H" as (l) "(% & H)". subst. iExists _.
- iSplit. done. by iApply (ty.(ty_shr_mono) with "LFT Hincl").
- - iDestruct "H" as (vl) "#[Hfrac Hty]". iSplit; last done.
- iExists vl. iFrame "#". iNext.
- iDestruct "Hty" as (l0) "(% & Hty)". subst. iExists _. iSplit. done.
- by iApply (ty_shr_mono with "LFT Hincl Hty").
- Qed.
-
- (* We have the additional hypothesis that Ï should be duplicable.
- The only way I can see to circumvent this limitation is to deeply
- embed permissions (and their inclusion). Not sure this is worth it. *)
- Lemma ty_incl_prod2 Ï ty11 ty12 ty21 ty22 :
- Duplicable Ï â†’ ty_incl Ï ty11 ty12 → ty_incl Ï ty21 ty22 →
- ty_incl Ï (product2 ty11 ty21) (product2 ty12 ty22).
- Proof.
- iIntros (HÏ Hincl1 Hincl2 tid) "#LFT #HÏ".
- iMod (Hincl1 with "LFT HÏ") as "[#Ho1#Hs1]".
- iMod (Hincl2 with "LFT HÏ") as "[#Ho2#Hs2]".
- iSplitL; iIntros "!>!#*H/=".
- - iDestruct "H" as (vl1 vl2) "(% & H1 & H2)". iExists _, _. iSplit. done.
- iSplitL "H1". iApply ("Ho1" with "H1"). iApply ("Ho2" with "H2").
- - iDestruct "H" as (E1 E2) "(% & H1 & H2)".
- iDestruct ("Hs1" with "*H1") as "[H1 EQ]". iDestruct ("Hs2" with "*H2") as "[H2 %]".
- iDestruct "EQ" as %->. iSplit; last by iPureIntro; f_equal.
- iExists _, _. by iFrame.
- Qed.
-
- Lemma ty_incl_prod Ï tyl1 tyl2 :
- Duplicable Ï â†’ Forall2 (ty_incl Ï) tyl1 tyl2 → ty_incl Ï (Î tyl1) (Î tyl2).
- Proof. intros HÏ HFA. induction HFA. done. by apply ty_incl_prod2. Qed.
-
- Lemma ty_incl_prod2_assoc1 Ï ty1 ty2 ty3 :
- ty_incl Ï (product2 ty1 (product2 ty2 ty3)) (product2 (product2 ty1 ty2) ty3).
- Proof.
- iIntros (tid) "_ _!>". iSplit; iIntros "!#/=*H".
- - iDestruct "H" as (vl1 vl') "(% & Ho1 & H)".
- iDestruct "H" as (vl2 vl3) "(% & Ho2 & Ho3)". subst.
- iExists _, _. iSplit. by rewrite assoc. iFrame. iExists _, _. by iFrame.
- - iDestruct "H" as (E1 E2') "(% & Hs1 & H)".
- iDestruct "H" as (E2 E3) "(% & Hs2 & Hs3)". rewrite shift_loc_assoc_nat.
- iSplit; last by rewrite assoc.
- iExists (E1 ∪ E2), E3. iSplit. by iPureIntro; set_solver. iFrame.
- iExists E1, E2. iSplit. by iPureIntro; set_solver. by iFrame.
- Qed.
-
- Lemma ty_incl_prod2_assoc2 Ï ty1 ty2 ty3 :
- ty_incl Ï (product2 (product2 ty1 ty2) ty3) (product2 ty1 (product2 ty2 ty3)).
- Proof.
- iIntros (tid) "_ _!>". iSplit; iIntros "!#/=*H".
- - iDestruct "H" as (vl1 vl') "(% & H & Ho3)".
- iDestruct "H" as (vl2 vl3) "(% & Ho1 & Ho2)". subst.
- iExists _, _. iSplit. by rewrite -assoc. iFrame. iExists _, _. by iFrame.
- - iDestruct "H" as (E1' E3) "(% & H & Hs3)".
- iDestruct "H" as (E1 E2) "(% & Hs1 & Hs2)". rewrite shift_loc_assoc_nat.
- iSplit; last by rewrite assoc.
- iExists E1, (E2 ∪ E3). iSplit. by iPureIntro; set_solver. iFrame.
- iExists E2, E3. iSplit. by iPureIntro; set_solver. by iFrame.
- Qed.
-
- Lemma ty_incl_prod_flatten Ï tyl1 tyl2 tyl3 :
- ty_incl Ï (Î (tyl1 ++ Î tyl2 :: tyl3))
- (Î (tyl1 ++ tyl2 ++ tyl3)).
- Proof.
- apply (ty_incl_weaken _ ⊤). apply perm_incl_top.
- induction tyl1; last by apply (ty_incl_prod2 _ _ _ _ _ _).
- induction tyl2 as [|ty tyl2 IH]; simpl.
- - iIntros (tid) "#LFT _". iSplitL; iIntros "/=!>!#*H".
- + iDestruct "H" as (vl1 vl2) "(% & % & Ho)". subst. done.
- + iDestruct "H" as (E1 E2) "(% & H1 & Ho)". iSplit; last done.
- rewrite shift_loc_0. iApply (ty_shr_mono with "LFT [] Ho"). set_solver.
- iApply lft_incl_refl.
- - etransitivity. apply ty_incl_prod2_assoc2.
- eapply (ty_incl_prod2 _ _ _ _ _ _). done. apply IH.
- Qed.
-
- Lemma ty_incl_prod_unflatten Ï tyl1 tyl2 tyl3 :
- ty_incl Ï (Î (tyl1 ++ tyl2 ++ tyl3))
- (Î (tyl1 ++ Î tyl2 :: tyl3)).
- Proof.
- apply (ty_incl_weaken _ ⊤). apply perm_incl_top.
- induction tyl1; last by apply (ty_incl_prod2 _ _ _ _ _ _).
- induction tyl2 as [|ty tyl2 IH]; simpl.
- - iIntros (tid) "#LFT _". iMod (bor_create with "LFT []") as "[Hbor _]".
- done. instantiate (1:=True%I). by auto. instantiate (1:=static).
- iMod (bor_fracture (λ _, True%I) with "LFT Hbor") as "#Hbor". done.
- iSplitL; iIntros "/=!>!#*H".
- + iExists [], vl. iFrame. auto.
- + iSplit; last done. iExists ∅, E. iSplit. iPureIntro; set_solver.
- rewrite shift_loc_0. iFrame. iExists []. iSplit; last auto.
- setoid_rewrite heap_mapsto_vec_nil.
- iApply (frac_bor_shorten with "[] Hbor"). iApply lft_incl_static.
- - etransitivity; last apply ty_incl_prod2_assoc1.
- eapply (ty_incl_prod2 _ _ _ _ _ _). done. apply IH.
- Qed.
-
- Lemma ty_incl_sum Ï n tyl1 tyl2 (_ : LstTySize n tyl1) (_ : LstTySize n tyl2) :
- Duplicable Ï â†’ Forall2 (ty_incl Ï) tyl1 tyl2 →
- ty_incl Ï (sum tyl1) (sum tyl2).
- Proof.
- iIntros (DUP FA tid) "#LFT #HÏ". rewrite /sum /=. iSplitR "".
- - assert (Hincl : lft_ctx -∗ Ï tid ={⊤}=∗
- (□ ∀ i vl, (nth i tyl1 ∅%T).(ty_own) tid vl
- → (nth i tyl2 ∅%T).(ty_own) tid vl)).
- { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
- - iIntros "_ _!>*!#". eauto.
- - iIntros "#LFT #HÏ". iMod (IH with "LFT HÏ") as "#IH".
- iMod (Hincl with "LFT HÏ") as "[#Hh _]".
- iIntros "!>*!#*Hown". destruct i as [|i]. by iApply "Hh". by iApply "IH". }
- iMod (Hincl with "LFT HÏ") as "#Hincl". iIntros "!>!#*H".
- iDestruct "H" as (i vl') "[% Hown]". subst. iExists _, _. iSplit. done.
- by iApply "Hincl".
- - assert (Hincl : lft_ctx -∗ Ï tid ={⊤}=∗
- (□ ∀ i κ E l, (nth i tyl1 ∅%T).(ty_shr) κ tid E l
- → (nth i tyl2 ∅%T).(ty_shr) κ tid E l)).
- { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
- - iIntros "#LFT _!>*!#". eauto.
- - iIntros "#LFT #HÏ".
- iMod (IH with "LFT HÏ") as "#IH". iMod (Hincl with "LFT HÏ") as "[_ #Hh]".
- iIntros "!>*!#*Hown". destruct i as [|i]; last by iApply "IH".
- by iDestruct ("Hh" $! _ _ _ with "Hown") as "[$ _]". }
- iMod (Hincl with "LFT HÏ") as "#Hincl". iIntros "!>!#*H". iSplit; last done.
- iDestruct "H" as (i) "[??]". iExists _. iSplit. done. by iApply "Hincl".
- 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".
+ split.
+ - iIntros (ty tid) "_ _!>". iSplit; iIntros "!#"; eauto.
+ - eauto using ty_incl_weaken, ty_incl_trans, perm_incl_duplicable.
Qed.
Lemma ty_incl_perm_incl Ï ty1 ty2 ν :
ty_incl Ï ty1 ty2 → Ï âˆ— ν â— ty1 ⇒ ν â— ty2.
Proof.
iIntros (Hincl tid) "#LFT [HÏ Hty1]". iMod (Hincl with "LFT HÏ") as "[#Hownincl _]".
- unfold Perm.has_type. destruct (Perm.eval_expr ν); last done. by iApply "Hownincl".
+ unfold has_type. destruct (eval_expr ν); last done. by iApply "Hownincl".
Qed.
-
End ty_incl.
\ No newline at end of file
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index 1d02d44c3d9b8702bd7d8f1b8840110b4b0500e7..03a84abed9c2969fc594f53996b399b143f7a81f 100644
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -2,12 +2,10 @@ From iris.program_logic Require Import hoare.
From iris.base_logic Require Import big_op.
From lrust.lang Require Export notation memcpy.
From lrust.typing Require Export type perm.
-From lrust Require Import typing.perm_incl lang.proofmode.
+From lrust.lang Require Import proofmode.
From lrust.lifetime Require Import frac_borrow reborrow borrow creation.
-Import Types Perm.
Section typing.
-
Context `{iris_typeG Σ}.
(* TODO : good notations for [typed_step] and [typed_step_ty] ? *)
@@ -35,101 +33,12 @@ Section typing.
iApply Hwt. iFrame "∗#".
Qed.
- Lemma typed_bool Ï (b:Datatypes.bool): typed_step_ty Ï #b bool.
- Proof. iIntros (tid) "!#(_&_&_&$)". wp_value. by iExists _. Qed.
-
- Lemma typed_int Ï (z:Datatypes.nat) :
- typed_step_ty Ï #z int.
- Proof. iIntros (tid) "!#(_&_&_&$)". wp_value. by iExists _. 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.
-
Lemma typed_valuable (ν : expr) ty:
typed_step_ty (ν ◠ty) ν ty.
Proof.
iIntros (tid) "!#(_&_&H&$)". iApply (has_type_wp with "[$H]"). by iIntros (v) "_ $".
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.
-
Lemma typed_newlft Ï:
typed_step Ï Newlft (λ _, ∃ α, 1.[α] ∗ α ∋ top)%P.
Proof.
@@ -147,31 +56,6 @@ Section typing.
iIntros "!>H†". by iApply fupd_mask_mono; last iApply "Hextr".
Qed.
- Lemma typed_alloc Ï (n : nat):
- 0 < n → typed_step_ty Ï (Alloc #n) (own 1 (Î (replicate n uninit))).
- Proof.
- iIntros (Hn tid) "!#(#HEAP&_&_&$)". wp_alloc l vl as "H↦" "H†". iIntros "!>".
- 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 ->; last done.
- clear. simpl. induction n. done. rewrite /= IHn //.
- Qed.
-
- Lemma typed_free ty (ν : expr):
- typed_step (ν ◠own 1 ty) (Free #ty.(ty_size) ν) (λ _, 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 ">%". wp_free; eauto.
- Qed.
-
Definition consumes (ty : type) (Ï1 Ï2 : expr → perm) : Prop :=
∀ ν tid Φ E, mgmtE ∪ ↑lrustN ⊆ E →
lft_ctx -∗ Ï1 ν tid -∗ na_own tid ⊤ -∗
@@ -181,76 +65,6 @@ Section typing.
-∗ Φ #l)
-∗ WP ν @ E {{ Φ }}.
- Lemma consumes_copy_own ty q:
- ty.(ty_dup) → consumes ty (λ ν, ν ◠own q ty)%P (λ ν, ν ◠own q 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 q:
- consumes ty (λ ν, ν ◠own q ty)%P
- (λ ν, ν ◠own q (Π(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.
-
- Lemma consumes_copy_uniq_bor ty κ κ' q:
- ty.(ty_dup) →
- consumes ty (λ ν, ν ◠&uniq{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
- (λ ν, ν ◠&uniq{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
- Proof.
- iIntros (? ν tid Φ E ?) "#LFT (H◠& #H⊑ & Htok) 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↦]". iDestruct "Heq" as %[=->].
- iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
- iMod (bor_acc with "LFT H↦ Htok") as "[H↦ Hclose']". set_solver.
- 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↦".
- iMod ("Hclose'" with "[H↦]") as "[H↦ Htok]". by iExists _; iFrame.
- iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
- Qed.
-
- Lemma consumes_copy_shr_bor ty κ κ' q:
- ty.(ty_dup) →
- consumes ty (λ ν, ν ◠&shr{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
- (λ ν, ν ◠&shr{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
- Proof.
- iIntros (? ν tid Φ E ?) "#LFT (H◠& #H⊑ & Htok) 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 #Hshr]". iDestruct "Heq" as %[=->].
- iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
- rewrite (union_difference_L (↑lrustN) ⊤); last done.
- setoid_rewrite ->na_own_union; try set_solver. iDestruct "Htl" as "[Htl ?]".
- iMod (ty_shr_acc with "LFT Hshr [$Htok $Htl]") as (q'') "[H↦ Hclose']"; try set_solver.
- iDestruct "H↦" as (vl) "[>H↦ #Hown]".
- iAssert (â–· ⌜length vl = ty_size tyâŒ)%I with "[#]" as ">%".
- by rewrite ty.(ty_size_eq).
- iModIntro. iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦".
- iMod ("Hclose'" with "[H↦]") as "[Htok $]". iExists _; by iFrame.
- iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
- Qed.
-
Lemma typed_deref ty Ï1 Ï2 (ν:expr) :
ty.(ty_size) = 1%nat → consumes ty Ï1 Ï2 →
typed_step (Ï1 ν) (!ν) (λ v, v â— ty ∗ Ï2 ν)%P.
@@ -262,91 +76,6 @@ Section typing.
iMod "Hupd" as "[$ Hclose]". by iApply "Hclose".
Qed.
- Lemma typed_deref_uniq_bor_own ty ν κ κ' q q':
- typed_step (ν ◠&uniq{κ} own q' ty ∗ κ' ⊑ κ ∗ q.[κ'])
- (!ν)
- (λ v, v ◠&uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
- Proof.
- iIntros (tid) "!#(#HEAP & #LFT & (H◠& #H⊑ & Htok) & $)". wp_bind ν.
- 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↦]". iDestruct "Heq" as %[=->].
- iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[Htok Hclose]". done.
- iMod (bor_acc_cons with "LFT H↦ Htok") as "[H↦ Hclose']". done.
- iDestruct "H↦" as (vl) "[>H↦ Hown]". iDestruct "Hown" as (l') "(>% & Hown & H†)".
- subst. rewrite heap_mapsto_vec_singleton. wp_read.
- iMod ("Hclose'" with "*[H↦ Hown H†][]") as "[Hbor Htok]"; last 1 first.
- - iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
- iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
- iMod ("Hclose" with "Htok") as "$". iFrame "#". iExists _. eauto.
- - iFrame "H↦ H†Hown".
- - iIntros "!>(?&?&?)!>". iNext. iExists _.
- rewrite -heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame.
- Qed.
-
- Lemma typed_deref_shr_bor_own ty ν κ κ' q q':
- typed_step (ν ◠&shr{κ} own q' ty ∗ κ' ⊑ κ ∗ q.[κ'])
- (!ν)
- (λ v, v ◠&shr{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
- Proof.
- iIntros (tid) "!#(#HEAP & #LFT & (H◠& #H⊑ & Htok) & $)". wp_bind ν.
- 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↦]". iDestruct "Heq" as %[=->].
- iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[[Htok1 Htok2] Hclose]". done.
- iDestruct "H↦" as (vl) "[H↦b #Hown]".
- iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
- iApply (wp_fupd_step _ (⊤∖↑lrustN) with "[Hown Htok2]"); try done.
- - iApply ("Hown" with "* [%] Htok2"). set_solver.
- - wp_read. iIntros "!>[Hshr ?]". iFrame "H⊑".
- iSplitL "Hshr"; first by iExists _; auto. iApply ("Hclose" with ">").
- iFrame. iApply "Hclose'". auto.
- Qed.
-
- Lemma typed_deref_uniq_bor_bor ty ν κ κ' κ'' q:
- typed_step (ν ◠&uniq{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ q.[κ] ∗ κ' ⊑ κ'')
- (!ν)
- (λ v, v ◠&uniq{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
- Proof.
- iIntros (tid) "!#(#HEAP & #LFT & (H◠& #H⊑1 & Htok & #H⊑2) & $)". wp_bind ν.
- 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↦]". iDestruct "Heq" as %[=->].
- iMod (lft_incl_acc with "H⊑1 Htok") as (q'') "[Htok Hclose]". done.
- iMod (bor_exists with "LFT H↦") as (vl) "Hbor". done.
- iMod (bor_sep with "LFT Hbor") as "[H↦ Hbor]". done.
- iMod (bor_exists with "LFT Hbor") as (l') "Hbor". done.
- iMod (bor_sep with "LFT Hbor") as "[Heq Hbor]". done.
- iMod (bor_persistent with "LFT Heq Htok") as "[>% Htok]". done. subst.
- iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
- rewrite heap_mapsto_vec_singleton.
- iApply (wp_fupd_step _ (⊤∖↑lftN) with "[Hbor]"); try done.
- by iApply (bor_unnest with "LFT Hbor").
- wp_read. iIntros "!> Hbor". iFrame "#". iSplitL "Hbor".
- - iExists _. iSplitR; first by auto. iApply (bor_shorten with "[] Hbor").
- iApply (lft_incl_glb with "H⊑2"). iApply lft_incl_refl.
- - iApply ("Hclose" with ">"). by iMod ("Hclose'" with "[$H↦]") as "[_ $]".
- Qed.
-
- Lemma typed_deref_shr_bor_bor ty ν κ κ' κ'' q:
- typed_step (ν ◠&shr{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ q.[κ] ∗ κ' ⊑ κ'')
- (!ν)
- (λ v, v ◠&shr{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
- Proof.
- iIntros (tid) "!#(#HEAP & #LFT & (H◠& #H⊑1 & Htok & #H⊑2) & $)". wp_bind ν.
- 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 Hshr]".
- iDestruct "Heq" as %[=->]. iDestruct "Hshr" as (l') "[H↦ Hown]".
- iMod (lft_incl_acc with "H⊑1 Htok") as (q') "[[Htok1 Htok2] Hclose]". done.
- iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
- iAssert (κ' ⊑ κ'' ∪ κ')%I as "#H⊑3".
- { iApply (lft_incl_glb with "H⊑2 []"). iApply lft_incl_refl. }
- iMod (lft_incl_acc with "H⊑3 Htok2") as (q''') "[Htok Hclose'']". done.
- iApply (wp_fupd_step _ (_∖_) with "[Hown Htok]"); try done.
- - iApply ("Hown" with "* [%] Htok"). set_solver.
- - wp_read. iIntros "!>[Hshr Htok]". iFrame "H⊑1". iSplitL "Hshr".
- + iExists _. iSplitR. done. by iApply (ty_shr_mono with "LFT H⊑3 Hshr").
- + iApply ("Hclose" with ">"). iMod ("Hclose'" with "[$H↦]") as "$".
- by iMod ("Hclose''" with "Htok") as "$".
- Qed.
-
Definition update (ty : type) (Ï1 Ï2 : expr → perm) : Prop :=
∀ ν tid Φ E, mgmtE ∪ (↑lrustN) ⊆ E →
lft_ctx -∗ Ï1 ν tid -∗
@@ -355,34 +84,6 @@ Section typing.
∀ vl', l ↦∗ vl' ∗ â–· (ty.(ty_own) tid vl') ={E}=∗ Ï2 ν tid) -∗ Φ #l) -∗
WP ν @ E {{ Φ }}.
- Lemma update_strong ty1 ty2 q:
- ty1.(ty_size) = ty2.(ty_size) →
- update ty1 (λ ν, ν ◠own q ty2)%P (λ ν, ν ◠own q 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 update_weak ty q κ κ':
- update ty (λ ν, ν ◠&uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
- (λ ν, ν ◠&uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
- Proof.
- iIntros (ν tid Φ E ?) "#LFT (H◠& #H⊑ & Htok) 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↦)". iDestruct "Heq" as %[=->].
- iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
- iMod (bor_acc with "LFT H↦ Htok") as "[H↦ Hclose']". set_solver.
- iDestruct "H↦" as (vl) "[>H↦ Hown]". rewrite ty.(ty_size_eq).
- iDestruct "Hown" as ">%". iApply "HΦ". iFrame "∗%#". iIntros (vl') "[H↦ Hown]".
- iMod ("Hclose'" with "[H↦ Hown]") as "[Hbor Htok]". by iExists _; iFrame.
- iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
- Qed.
-
Lemma typed_assign Ï1 Ï2 ty ν1 ν2:
ty.(ty_size) = 1%nat → update ty Ï1 Ï2 →
typed_step (Ï1 ν1 ∗ ν2 â— ty) (ν1 <- ν2) (λ _, Ï2 ν1).
@@ -433,15 +134,4 @@ Section typing.
iApply wp_bind. iApply wp_wand_r. iSplitL. iApply He; iFrame "∗#".
iIntros (v) "[Hθ Htl]". iApply HK. iFrame "∗#".
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 typing.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
new file mode 100644
index 0000000000000000000000000000000000000000..a7238d10e6513c74964b2a5909a8c17ccbf3eabe
--- /dev/null
+++ b/theories/typing/uniq_bor.v
@@ -0,0 +1,189 @@
+From iris.proofmode Require Import tactics.
+From lrust.lifetime Require Import borrow reborrow frac_borrow.
+From lrust.typing Require Export type.
+From lrust.typing Require Import perm type_incl typing own.
+
+Section uniq_bor.
+ Context `{iris_typeG Σ}.
+
+ Program Definition uniq_bor (κ:lft) (ty:type) :=
+ {| ty_size := 1;
+ ty_own tid vl :=
+ (∃ l:loc, ⌜vl = [ #l ]⌠∗ &{κ} l ↦∗: ty.(ty_own) tid)%I;
+ ty_shr κ' tid E l :=
+ (∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
+ □ ∀ q' F, ⌜E ∪ mgmtE ⊆ F⌠→ q'.[κ∪κ']
+ ={F, F∖E∖↑lftN}▷=∗ 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=> κ 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_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "Hbf". set_solver.
+ rewrite {1}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_unnest _ _ _ (l' ↦∗: ty_own ty tid)%I with "LFT [Hbtok]") as "Hb".
+ { set_solver. } { iApply bor_unfold_idx. eauto. }
+ iModIntro. iNext. iMod "Hb".
+ iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]"; try done. set_solver.
+ iApply "Hclose". eauto.
+ - iMod ("Hclose" with "[]") as "_". by eauto.
+ iApply step_fupd_mask_mono; last by eauto. done. set_solver.
+ Qed.
+ Next Obligation.
+ intros κ0 ty κ κ' tid E E' l ?. iIntros "#LFT #Hκ #H".
+ iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0∪κ' ⊑ κ0∪κ)%I as "#Hκ0".
+ { iApply (lft_incl_glb with "[] []").
+ - iApply lft_le_incl. apply gmultiset_union_subseteq_l.
+ - iApply (lft_incl_trans with "[] Hκ").
+ iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
+ iExists l'. iSplit. by iApply (frac_bor_shorten with "[]").
+ iIntros "!#". iIntros (q F) "% Htok".
+ iApply (step_fupd_mask_mono F _ _ (F∖E∖ ↑lftN)). set_solver. set_solver.
+ iMod (lft_incl_acc with "Hκ0 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_shr_mono with "LFT Hκ0").
+ Qed.
+
+End uniq_bor.
+
+Notation "&uniq{ κ } ty" := (uniq_bor κ ty)
+ (format "&uniq{ κ } ty", at level 20, right associativity) : lrust_type_scope.
+
+Section typing.
+ Context `{iris_typeG Σ}.
+
+ Lemma own_uniq_borrowing ν q ty κ :
+ borrowing κ ⊤ (ν ◠own q ty) (ν ◠&uniq{κ} ty).
+ Proof.
+ iIntros (tid) "#LFT _ Hown". unfold has_type.
+ destruct (eval_expr ν) as [[[|l|]|]|];
+ try by (iDestruct "Hown" as "[]" || iDestruct "Hown" as (l) "[% _]").
+ iDestruct "Hown" as (l') "[EQ [Hown Hf]]". iDestruct "EQ" as %[=]. subst l'.
+ iApply (fupd_mask_mono (↑lftN)). done.
+ iMod (bor_create with "LFT Hown") as "[Hbor Hext]". done.
+ iSplitL "Hbor". by simpl; eauto.
+ iIntros "!>#H†". iExists _. iMod ("Hext" with "H†") as "$". by iFrame.
+ Qed.
+
+ Lemma rebor_uniq_borrowing κ κ' ν ty :
+ borrowing κ (κ ⊑ κ') (ν ◠&uniq{κ'}ty) (ν ◠&uniq{κ}ty).
+ Proof.
+ iIntros (tid) "#LFT #Hord H". unfold has_type.
+ destruct (eval_expr ν) as [[[|l|]|]|];
+ try by (iDestruct "H" as "[]" || iDestruct "H" as (l) "[% _]").
+ iDestruct "H" as (l') "[EQ H]". iDestruct "EQ" as %[=]. subst l'.
+ iApply (fupd_mask_mono (↑lftN)). done.
+ iMod (rebor with "LFT Hord H") as "[H Hextr]". done.
+ iModIntro. iSplitL "H". iExists _. by eauto.
+ iIntros "H†". iExists _. by iMod ("Hextr" with "H†") as "$".
+ Qed.
+
+ Lemma lft_incl_ty_incl_uniq_bor ty κ1 κ2 :
+ ty_incl (κ1 ⊑ κ2) (&uniq{κ2}ty) (&uniq{κ1}ty).
+ Proof.
+ iIntros (tid) "#LFT #Hincl!>". iSplit; iIntros "!#*H".
+ - iDestruct "H" as (l) "[% Hown]". subst. iExists _. iSplit. done.
+ by iApply (bor_shorten with "Hincl").
+ - iAssert (κ1 ∪ κ ⊑ κ2 ∪ κ)%I as "#Hincl'".
+ { iApply (lft_incl_glb with "[] []").
+ - iApply (lft_incl_trans with "[] Hincl"). iApply lft_le_incl.
+ apply gmultiset_union_subseteq_l.
+ - iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
+ iSplitL; last done. iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'.
+ iFrame. iIntros "!#". iIntros (q' F) "% Htok".
+ iMod (lft_incl_acc with "Hincl' Htok") as (q'') "[Htok Hclose]". set_solver.
+ iMod ("Hupd" with "* [%] Htok") as "Hupd'"; try done. iModIntro. iNext.
+ iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
+ by iApply (ty_shr_mono with "LFT Hincl' H").
+ Qed.
+
+ Lemma consumes_copy_uniq_bor `(!Copy ty) κ κ' q:
+ consumes ty (λ ν, ν ◠&uniq{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
+ (λ ν, ν ◠&uniq{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
+ Proof.
+ iIntros (ν tid Φ E ?) "#LFT (H◠& #H⊑ & Htok) 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↦]". iDestruct "Heq" as %[=->].
+ iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
+ iMod (bor_acc with "LFT H↦ Htok") as "[H↦ Hclose']". set_solver.
+ 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↦".
+ iMod ("Hclose'" with "[H↦]") as "[H↦ Htok]". by iExists _; iFrame.
+ iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
+ Qed.
+
+ Lemma typed_deref_uniq_bor_own ty ν κ κ' q q':
+ typed_step (ν ◠&uniq{κ} own q' ty ∗ κ' ⊑ κ ∗ q.[κ'])
+ (!ν)
+ (λ v, v ◠&uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
+ Proof.
+ iIntros (tid) "!#(#HEAP & #LFT & (H◠& #H⊑ & Htok) & $)". wp_bind ν.
+ 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↦]". iDestruct "Heq" as %[=->].
+ iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[Htok Hclose]". done.
+ iMod (bor_acc_cons with "LFT H↦ Htok") as "[H↦ Hclose']". done.
+ iDestruct "H↦" as (vl) "[>H↦ Hown]". iDestruct "Hown" as (l') "(>% & Hown & H†)".
+ subst. rewrite heap_mapsto_vec_singleton. wp_read.
+ iMod ("Hclose'" with "*[H↦ Hown H†][]") as "[Hbor Htok]"; last 1 first.
+ - iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
+ iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
+ iMod ("Hclose" with "Htok") as "$". iFrame "#". iExists _. eauto.
+ - iFrame "H↦ H†Hown".
+ - iIntros "!>(?&?&?)!>". iNext. iExists _.
+ rewrite -heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame.
+ Qed.
+
+ Lemma typed_deref_uniq_bor_bor ty ν κ κ' κ'' q:
+ typed_step (ν ◠&uniq{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ q.[κ] ∗ κ' ⊑ κ'')
+ (!ν)
+ (λ v, v ◠&uniq{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
+ Proof.
+ iIntros (tid) "!#(#HEAP & #LFT & (H◠& #H⊑1 & Htok & #H⊑2) & $)". wp_bind ν.
+ 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↦]". iDestruct "Heq" as %[=->].
+ iMod (lft_incl_acc with "H⊑1 Htok") as (q'') "[Htok Hclose]". done.
+ iMod (bor_exists with "LFT H↦") as (vl) "Hbor". done.
+ iMod (bor_sep with "LFT Hbor") as "[H↦ Hbor]". done.
+ iMod (bor_exists with "LFT Hbor") as (l') "Hbor". done.
+ iMod (bor_sep with "LFT Hbor") as "[Heq Hbor]". done.
+ iMod (bor_persistent with "LFT Heq Htok") as "[>% Htok]". done. subst.
+ iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
+ rewrite heap_mapsto_vec_singleton.
+ iApply (wp_fupd_step _ (⊤∖↑lftN) with "[Hbor]"); try done.
+ by iApply (bor_unnest with "LFT Hbor").
+ wp_read. iIntros "!> Hbor". iFrame "#". iSplitL "Hbor".
+ - iExists _. iSplitR; first by auto. iApply (bor_shorten with "[] Hbor").
+ iApply (lft_incl_glb with "H⊑2"). iApply lft_incl_refl.
+ - iApply ("Hclose" with ">"). by iMod ("Hclose'" with "[$H↦]") as "[_ $]".
+ Qed.
+
+ Lemma update_weak ty q κ κ':
+ update ty (λ ν, ν ◠&uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
+ (λ ν, ν ◠&uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
+ Proof.
+ iIntros (ν tid Φ E ?) "#LFT (H◠& #H⊑ & Htok) 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↦)". iDestruct "Heq" as %[=->].
+ iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
+ iMod (bor_acc with "LFT H↦ Htok") as "[H↦ Hclose']". set_solver.
+ iDestruct "H↦" as (vl) "[>H↦ Hown]". rewrite ty.(ty_size_eq).
+ iDestruct "Hown" as ">%". iApply "HΦ". iFrame "∗%#". iIntros (vl') "[H↦ Hown]".
+ iMod ("Hclose'" with "[H↦ Hown]") as "[Hbor Htok]". by iExists _; iFrame.
+ iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
+ Qed.
+End typing.
\ No newline at end of file