Skip to content
Snippets Groups Projects
Commit f207080e authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Update type system wrt new lifetime logic.

parent 3a4b14b9
No related branches found
No related tags found
No related merge requests found
Pipeline #
Expand all Hide whitespace changes
Inline Side-by-side
theories/lifetime.v
+ 206
− 154
View file @ f207080e
This diff is collapsed.
theories/memcpy.v
+ 2
− 2
View file @ f207080e
......@@ -22,9 +22,9 @@ Lemma wp_memcpy `{heapG Σ} E l1 l2 vl1 vl2 q n:
length vl1 = n → length vl2 = n →
{{{ heap_ctx ∗ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
#l1 <-{n} !#l2 @ E
{{{; #(), l1 ↦∗ vl2 ∗ l2 ↦∗{q} vl2 }}}.
{{{ RET #(); l1 ↦∗ vl2 ∗ l2 ↦∗{q} vl2 }}}.
Proof.
iIntros (? Hvl1 Hvl2 Φ) "[(#Hinv & Hl1 & Hl2) HΦ]".
iIntros (? Hvl1 Hvl2 Φ) "(#Hinv & Hl1 & Hl2) HΦ".
iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec. wp_op=> ?; wp_if.
- iApply "HΦ". assert (n = O) by lia; subst.
destruct vl1, vl2; try discriminate. by iFrame.
......
theories/perm.v
+ 4
− 4
View file @ f207080e
......@@ -24,10 +24,10 @@ Section perm.
from_option (λ v, ty.(ty_own) tid [v]) False%I (eval_expr ν).
Definition extract (κ : lifetime) (ρ : perm) : perm :=
λ tid, (κ ∋ ρ tid)%I.
λ tid, ([†κ] ={lftN}=∗ ▷ ρ tid)%I.
Definition tok (κ : lifetime) (q : Qp) : perm :=
λ _, ([κ]{q} ∗ lft κ)%I.
λ _, q.[κ]%I.
Definition incl (κ κ' : lifetime) : perm :=
λ _, (κ ⊑ κ')%I.
......@@ -53,9 +53,9 @@ Notation "v ◁ ty" := (has_type v ty)
Notation "κ ∋ ρ" := (extract κ ρ)
(at level 75, right associativity) : perm_scope.
Notation "[ κ ]{ q }" := (tok κ q) (format "[ κ ]{ q }") : perm_scope.
Notation "q .[ κ ]" := (tok κ q) (format "q .[ κ ]", at level 0) : perm_scope.
Infix "⊑" := incl (at level 70) : perm_scope.
Infix "⊑" := incl (at level 60) : perm_scope.
Notation "∃ x .. y , P" :=
(exist (λ x, .. (exist (λ y, P)) ..)) : perm_scope.
......
theories/perm_incl.v
+ 37
− 27
View file @ f207080e
......@@ -16,7 +16,7 @@ Section defs.
λ ρ1 ρ2, perm_incl ρ1 ρ2 ∧ perm_incl ρ2 ρ1.
Definition borrowing κ (ρ ρ1 ρ2 : perm) :=
∀ tid, lft κ ⊢ ρ tid -∗ ρ1 tid ={⊤}=∗ ρ2 tid ∗ κ ∋ ρ1 tid.
∀ tid, ρ tid ⊢ ρ1 tid ={⊤}=∗ ρ2 tid ∗ (κ ∋ ρ1)%P tid.
End defs.
......@@ -93,8 +93,7 @@ Section props.
Lemma perm_tok_plus κ q1 q2 :
tok κ q1 ∗ tok κ q2 ⇔ tok κ (q1 + q2).
Proof.
rewrite /tok /sep /=; split; intros tid; rewrite -lft_own_op;
iIntros "[[$$]H]!>". by iDestruct "H" as "[$?]". by auto.
rewrite /tok /sep /=; split; iIntros (tid) "?"; rewrite lft_own_frac_op //.
Qed.
Lemma perm_lftincl_refl κ : ⊤ ⇒ κ ⊑ κ.
......@@ -104,7 +103,7 @@ Section props.
Proof. iIntros (tid) "[#?#?]!>". iApply lft_incl_trans. auto. Qed.
Lemma perm_incl_share q ν κ ty :
ν ◁ &uniq{κ} ty ∗ [κ]{q} ⇒ ν ◁ &shr{κ} ty ∗ [κ]{q}.
ν ◁ &uniq{κ} ty ∗ q.[κ] ⇒ ν ◁ &shr{κ} ty ∗ q.[κ].
Proof.
iIntros (tid) "[Huniq [Htok $]]". unfold has_type.
destruct (eval_expr ν); last by iDestruct "Huniq" as "[]".
......@@ -188,7 +187,7 @@ Section props.
rewrite split_prod_mt.
iInduction (combine_offs tyl 0) as [|[ty offs] ll] "IH". by auto.
rewrite big_sepL_cons /=.
iMod (lft_borrow_split with "H") as "[H0 H]". set_solver.
iMod (borrow_split with "H") as "[H0 H]". set_solver.
iMod ("IH" with "H") as "$". iModIntro. iExists _. eauto.
Qed.
......@@ -215,39 +214,37 @@ Section props.
Lemma borrowing_perm_incl κ ρ ρ1 ρ2 θ :
borrowing κ ρ ρ1 ρ2 → ρ ∗ κ ∋ θ ∗ ρ1 ⇒ ρ2 ∗ κ ∋ (θ ∗ ρ1).
Proof.
iIntros (Hbor tid) "(Hρ&Hθ&Hρ1)".
iMod (Hbor with "[#] Hρ Hρ1") as "[$ ?]". by iApply lft_extract_lft.
iApply lft_extract_combine. set_solver. by iFrame.
iIntros (Hbor tid) "(Hρ&Hθ&Hρ1)". iMod (Hbor with "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) "#Hκ _ Hown". unfold has_type.
iIntros (tid) "_ Hown". unfold has_type.
destruct (eval_expr ν) as [[[|l|]|]|];
try by (iDestruct "Hown" as "[]" || iDestruct "Hown" as (l) "[% _]").
iDestruct "Hown" as (l') "[EQ [Hf Hown]]". iDestruct "EQ" as %[=]. subst l'.
iMod (lft_borrow_create with "Hκ Hown") as "[Hbor Hext]". done.
iApply (fupd_mask_mono lftN). done.
iMod (borrow_create with "Hown") as "[Hbor Hext]". done.
iSplitL "Hbor". by simpl; eauto.
iMod (lft_borrow_create with "Hκ Hf") as "[_ Hf]". done.
iMod (lft_extract_combine with "[$Hext $Hf]"). done.
iModIntro. iApply lft_extract_mono; last done.
iIntros "H/=". iExists _. iSplit. done. by iDestruct "H" as "[$$]".
iMod (borrow_create with "Hf") as "[_ Hf]". done.
iIntros "!>#H†".
iMod ("Hext" with "H†") as "Hext". iMod ("Hf" with "H†") as "Hf". iIntros "!>/=".
iExists _. iFrame. auto.
Qed.
Lemma reborrow_uniq_borrowing κ κ' ν ty :
borrowing κ (κ ⊑ κ') (ν ◁ &uniq{κ'}ty) (ν ◁ &uniq{κ}ty).
Proof.
iIntros (tid) "_ #Hord H". unfold has_type.
iIntros (tid) "#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'.
iMod (lft_reborrow with "Hord H") as "[H Hextr]". done.
iApply (fupd_mask_mono lftN). done.
iMod (reborrow with "Hord H") as "[H Hextr]". done.
iModIntro. iSplitL "H". iExists _. by eauto.
iApply (lft_extract_proper with "Hextr").
iSplit; iIntros "H/=".
- iDestruct "H" as (l') "[EQ H]". iDestruct "EQ" as %[=]. by subst l'.
- iExists _. eauto.
iIntros "H†". iMod ("Hextr" with "H†"). simpl. auto.
Qed.
Lemma reborrow_shr_perm_incl κ κ' ν ty :
......@@ -261,12 +258,25 @@ Section props.
by iApply (ty_shr_mono with "Hord Hκ'").
Qed.
Lemma lftincl_borrowing κ κ' q : borrowing κ ⊤ [κ']{q} (κ ⊑ κ').
Proof.
iIntros (tid) "#Hκ #Hord [Htok #Hκ']".
iMod (lft_mkincl' with "[#] Htok") as "[$ H]". done. by iFrame "#".
iMod (lft_borrow_create with "Hκ []") as "[_ H']". done. by iNext; iApply "Hκ'".
iApply lft_extract_combine. done. by iFrame.
Qed.
(* TODO *)
(* Lemma lftincl_borrowing κ κ' q : borrowing κ ⊤ q.[κ'] (κ ⊑ κ'). *)
(* Proof. *)
(* iIntros (tid) "_ Htok". iApply fupd_mask_mono. done. *)
(* iDestruct "Htok" as "[Htok1 Htok2]". *)
(* iMod (borrow_create with "[Htok1]") as "[Hbor Hclose]". reflexivity. *)
(* { iIntros "!>". iExact "Htok1". } *)
(* iMod (borrow_fracture (λ q', (q / 2 * q').[κ'])%I with "[Hbor $Htok2]") *)
(* as "[Hbor Htok]". done. *)
(* { by rewrite Qp_mult_1_r. } *)
(* iIntros "{$Htok}!>". iSplitL "Hbor". *)
(* iApply frac_borrow_incl. done. frac_borrow_incl *)
(* iExact "Hclose". iFrame. *)
(* iMod (frac_borrow_incl with "[-]"). *)
(* iMod (lft_mkincl' with "[#] Htok") as "[$ H]". done. by iFrame "#". *)
(* iMod (lft_borrow_create with "Hκ []") as "[_ H']". done. by iNext; iApply "Hκ'". *)
(* iApply lft_extract_combine. done. by iFrame. *)
(* Qed. *)
End props.
theories/type.v
+ 70
− 78
View file @ f207080e
......@@ -33,14 +33,14 @@ Record type `{heapG Σ, lifetimeG Σ, thread_localG Σ} :=
more consistent with thread-local tokens, which we do not
give any. *)
ty_share E N κ l tid q : mgmtE ⊥ nclose N → mgmtE ⊆ E →
&{κ} (l ↦∗: ty_own tid) ⊢ [κ]{q} ={E}=∗ ty_shr κ tid N l ∗ [κ]{q};
&{κ} (l ↦∗: ty_own tid) ⊢ q.[κ] ={E}=∗ ty_shr κ tid N l ∗ q.[κ];
ty_shr_mono κ κ' tid N l :
κ' ⊑ κ ⊢ ty_shr κ tid N l → ty_shr κ' tid N l;
ty_shr_acc κ tid E N l q :
ty_dup → mgmtE ∪ nclose N ⊆ E →
ty_shr κ tid N l ⊢
[κ]{q} ∗ tl_own tid N ={E}=∗ ∃ q', ▷l ↦∗{q'}: ty_own tid ∗
(▷l ↦∗{q'}: ty_own tid ={E}=∗ [κ]{q} ∗ tl_own tid N)
q.[κ] ∗ tl_own tid N ={E}=∗ ∃ q', ▷l ↦∗{q'}: ty_own tid ∗
(▷l ↦∗{q'}: ty_own tid ={E}=∗ q.[κ] ∗ tl_own tid N)
}.
Global Existing Instances ty_shr_persistent ty_dup_persistent.
......@@ -66,20 +66,22 @@ Program Coercion ty_of_st `{heapG Σ, lifetimeG Σ, thread_localG Σ}
Next Obligation. intros. apply st_size_eq. Qed.
Next Obligation.
intros Σ ??? st E N κ l tid q ??. iIntros "Hmt Htok".
iMod (lft_borrow_exists with "Hmt Htok") as (vl) "[Hmt Htok]". set_solver.
iMod (lft_borrow_split with "Hmt") as "[Hmt Hown]". set_solver.
iMod (lft_borrow_persistent with "Hown Htok") as "[Hown $]". set_solver.
iExists vl. iFrame. by iApply lft_borrow_fracture.
iMod (borrow_exists with "Hmt Htok") as (vl) "[Hmt Htok]". set_solver.
iMod (borrow_split with "Hmt") as "[Hmt Hown]". set_solver.
iMod (borrow_persistent with "Hown Htok") as "[Hown Htok]". set_solver.
iMod (borrow_fracture with "[Hmt $Htok]") as "[Hfrac $]"; last first.
{ iExists vl. by iFrame. }
done. set_solver.
Qed.
Next Obligation.
intros Σ???. iIntros (st κ κ' tid N l) "#Hord H".
iDestruct "H" as (vl) "[Hf Hown]".
iExists vl. iFrame. by iApply (lft_frac_borrow_incl with "Hord").
iExists vl. iFrame. by iApply (frac_borrow_shorten with "Hord").
Qed.
Next Obligation.
intros Σ??? st κ tid N E l q ??. iIntros "#Hshr[Hlft $]".
iDestruct "Hshr" as (vl) "[Hf Hown]".
iMod (lft_frac_borrow_open with "[] Hf Hlft") as (q') "[Hmt Hclose]";
iMod (frac_borrow_acc with "[] Hf Hlft") as (q') "[Hmt Hclose]";
first set_solver.
- iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_vec_op_eq.
iSplit; auto.
......@@ -112,9 +114,9 @@ Section types.
Next Obligation. iIntros (tid vl) "[]". Qed.
Next Obligation.
iIntros (????????) "Hb Htok".
iMod (lft_borrow_exists with "Hb Htok") as (vl) "[Hb Htok]". set_solver.
iMod (lft_borrow_split with "Hb") as "[_ Hb]". set_solver.
iMod (lft_borrow_persistent with "Hb Htok") as "[>[] _]". set_solver.
iMod (borrow_exists with "Hb Htok") as (vl) "[Hb Htok]". set_solver.
iMod (borrow_split with "Hb") as "[_ Hb]". set_solver.
iMod (borrow_persistent with "Hb Htok") as "[>[] _]". set_solver.
Qed.
Next Obligation. iIntros (?????) "_ []". Qed.
Next Obligation. intros. iIntros "[]". Qed.
......@@ -146,7 +148,7 @@ Section types.
∗ ▷ l ↦∗: ty.(ty_own) tid)%I;
ty_shr κ tid N l :=
(∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
∀ q', □ ([κ]{q'} ={mgmtE ∪ N, mgmtE}▷=∗ ty.(ty_shr) κ tid N l' ∗ [κ]{q'}))%I
∀ q', □ (q'.[κ] ={mgmtE ∪ N, mgmtE}▷=∗ ty.(ty_shr) κ tid N l' ∗ q'.[κ]))%I
|}.
Next Obligation. done. Qed.
Next Obligation.
......@@ -154,36 +156,36 @@ Section types.
Qed.
Next Obligation.
move=> q ty E N κ l tid q' ?? /=. iIntros "Hshr Htok".
iMod (lft_borrow_exists with "Hshr Htok") as (vl) "[Hb Htok]". set_solver.
iMod (lft_borrow_split with "Hb") as "[Hb1 Hb2]". set_solver.
iMod (lft_borrow_exists with "Hb2 Htok") as (l') "[Hb2 Htok]". set_solver.
iMod (lft_borrow_split with "Hb2") as "[EQ Hb2]". set_solver.
iMod (lft_borrow_persistent with "EQ Htok") as "[>% Htok]". set_solver. subst.
iMod (borrow_exists with "Hshr Htok") as (vl) "[Hb Htok]". set_solver.
iMod (borrow_split with "Hb") as "[Hb1 Hb2]". set_solver.
iMod (borrow_exists with "Hb2 Htok") as (l') "[Hb2 Htok]". set_solver.
iMod (borrow_split with "Hb2") as "[EQ Hb2]". set_solver.
iMod (borrow_persistent with "EQ Htok") as "[>% Htok]". set_solver. subst.
rewrite heap_mapsto_vec_singleton.
iMod (lft_borrow_split with "Hb2") as "[_ Hb2]". set_solver.
iMod (lft_borrow_fracture _ _ (λ q, l ↦{q} #l')%I with "Hb1") as "Hbf".
rewrite lft_borrow_persist. iDestruct "Hb2" as (κ0 i) "(#Hord&#Hpb&Hpbown)".
iMod (inv_alloc N _ (lft_pers_borrow_own i κ0 ∨ ty_shr ty κ tid N l')%I
iMod (borrow_split with "Hb2") as "[_ Hb2]". set_solver.
iMod (borrow_fracture (λ q, l ↦{q} #l')%I with "[$Hb1 $Htok]") as "[Hbf $]".
set_solver.
rewrite /borrow. iDestruct "Hb2" as (i) "(#Hpb&Hpbown)".
iMod (inv_alloc N _ (idx_borrow_own 1 i ∨ ty_shr ty κ tid N l')%I
with "[Hpbown]") as "#Hinv"; first by eauto.
iIntros "!>{$Htok}". iExists l'. iFrame. iIntros (q'') "!#Htok".
iExists l'. iIntros "!>{$Hbf}". iIntros (q'') "!#Htok".
iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
replace ((mgmtE ∪ N) ∖ N) with mgmtE by set_solver.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- iAssert (&{κ}▷ l' ↦∗: ty_own ty tid)%I with "[Hbtok]" as "Hb".
{ iApply lft_borrow_persist. eauto. }
iMod (lft_borrow_open with "Hb Htok") as "[Hown Hob]". set_solver.
{ rewrite /borrow. iExists i. eauto. }
iMod (borrow_acc_strong with "Hb Htok") as "[Hown Hclose']". set_solver.
iIntros "!>". iNext.
iMod (lft_borrow_close_stronger with "Hown Hob []") as "[Hb Htok]".
set_solver. eauto 10.
iMod ("Hclose'" with "*[Hown]") as "[Hb Htok]". iFrame. by iIntros "!>[?$]".
iMod (ty.(ty_share) with "Hb Htok") as "[#Hshr Htok]"; try done.
iMod ("Hclose" with "[]") as "_"; by eauto.
- iIntros "!>". iNext. iMod ("Hclose" with "[]") as "_"; by eauto.
Qed.
Next Obligation.
iIntros (_ ty κ κ' tid N l) "#Hκ #H". iDestruct "H" as (l') "[Hfb Hvs]".
iExists l'. iSplit. by iApply (lft_frac_borrow_incl with "[]").
iExists l'. iSplit. by iApply (frac_borrow_shorten with "[]").
iIntros (q') "!#Htok".
iMod (lft_incl_trade with "Hκ Htok") as (q'') "[Htok Hclose]". set_solver.
iMod (lft_incl_acc with "Hκ Htok") as (q'') "[Htok Hclose]". set_solver.
iMod ("Hvs" $! q'' with "Htok") as "Hvs'".
iIntros "!>". iNext. iMod "Hvs'" as "[Hshr Htok]".
iMod ("Hclose" with "Htok"). iFrame.
......@@ -197,8 +199,8 @@ Section types.
(∃ l:loc, vl = [ #l ] ∗ &{κ} l ↦∗: ty.(ty_own) tid)%I;
ty_shr κ' tid N l :=
(∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
∀ q' κ'', □ (κ'' ⊑ κ ∗ κ'' ⊑ κ' ∗ [κ'']{q'}
={mgmtE ∪ N, mgmtE}▷=∗ ty.(ty_shr) κ'' tid N l' ∗ [κ'']{q'}))%I
∀ q', □ (q'.[κ ⋅ κ']
={mgmtE ∪ N, mgmtE}▷=∗ ty.(ty_shr) (κ⋅κ') tid N l' ∗ q'.[κ⋅κ']))%I
|}.
Next Obligation. done. Qed.
Next Obligation.
......@@ -206,50 +208,41 @@ Section types.
Qed.
Next Obligation.
move=> κ ty E N κ' l tid q' ??/=. iIntros "Hshr Htok".
iMod (lft_borrow_exists with "Hshr Htok") as (vl) "[Hb Htok]". set_solver.
iMod (lft_borrow_split with "Hb") as "[Hb1 Hb2]". set_solver.
iMod (lft_borrow_exists with "Hb2 Htok") as (l') "[Hb2 Htok]". set_solver.
iMod (lft_borrow_split with "Hb2") as "[EQ Hb2]". set_solver.
iMod (lft_borrow_persistent with "EQ Htok") as "[>% Htok]". set_solver. subst.
iMod (borrow_exists with "Hshr Htok") as (vl) "[Hb Htok]". set_solver.
iMod (borrow_split with "Hb") as "[Hb1 Hb2]". set_solver.
iMod (borrow_exists with "Hb2 Htok") as (l') "[Hb2 Htok]". set_solver.
iMod (borrow_split with "Hb2") as "[EQ Hb2]". set_solver.
iMod (borrow_persistent with "EQ Htok") as "[>% Htok]". set_solver. subst.
rewrite heap_mapsto_vec_singleton.
iMod (lft_borrow_fracture _ _ (λ q, l ↦{q} #l')%I with "Hb1") as "Hbf".
rewrite lft_borrow_persist.
iDestruct "Hb2" as (κ0 i) "(#Hord&#Hpb&Hpbown)".
iMod (inv_alloc N _ (lft_pers_borrow_own i κ0 ∨ ty_shr ty κ' tid N l')%I
iMod (borrow_fracture (λ q, l ↦{q} #l')%I with "[$Hb1 $Htok]")
as "[Hbf $]". set_solver.
rewrite {1}/borrow. iDestruct "Hb2" as (i) "[#Hpb Hpbown]".
iMod (inv_alloc N _ (idx_borrow_own 1 i ∨ ty_shr ty (κ⋅κ') tid N l')%I
with "[Hpbown]") as "#Hinv"; first by eauto.
iIntros "!>{$Htok}". iExists l'. iFrame.
iIntros (q'' κ'') "!#(#Hκ''κ & #Hκ''κ' & Htok)".
iExists l'. iIntros "!>{$Hbf}". iIntros (q'') "!#Htok".
iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
replace ((mgmtE ∪ N) ∖ N) with mgmtE by set_solver.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- iAssert (&{κ''}&{κ} l' ↦∗: ty_own ty tid)%I with "[Hbtok]" as "Hb".
{ iApply lft_borrow_persist. iExists κ0, i. iFrame "∗ #".
iApply lft_incl_trans. eauto. }
iMod (lft_borrow_open with "Hb Htok") as "[Hown Hob]". set_solver.
iIntros "!>". iNext.
iMod (lft_borrow_unnest with "Hκ''κ [$Hown $Hob]") as "[Htok Hb]". set_solver.
- iAssert (&{κ'}&{κ} l' ↦∗: ty_own ty tid)%I with "[Hbtok]" as "Hb".
{ rewrite /borrow. eauto. }
iMod (borrow_unnest with "Hb") as "Hb". set_solver.
iIntros "!>". iNext. iMod "Hb".
iMod (ty.(ty_share) with "Hb Htok") as "[#Hshr Htok]"; try done.
iMod ("Hclose" with "[]") as "_".
(* FIXME : the "global sharing protocol" that we used for [own]
does not work here, because we do not know at the beginning
at which lifetime we will need the sharing.
This seems somewhat similar to the RefCell problem: we would
need a lifetime that would be the union of κ and κ'. *)
admit.
by eauto.
- iIntros "!>". iNext. iMod ("Hclose" with "[]") as "_". by eauto.
iIntros "!>{$Htok}". by iApply (ty.(ty_shr_mono) with "Hκ''κ'").
Admitted.
iMod ("Hclose" with "[]") as "_". eauto. by iFrame.
- iIntros "!>". iNext. iMod ("Hclose" with "[]") as "_"; by eauto.
Qed.
Next Obligation.
iIntros (κ0 ty κ κ' tid N l) "#Hκ #H". iDestruct "H" as (l') "[Hfb Hvs]".
iExists l'. iSplit. by iApply (lft_frac_borrow_incl with "[]").
iIntros (q' κ'') "!#(#Hκ0 & #Hκ' & Htok)".
iMod ("Hvs" $! q' κ'' with "[Htok]") as "Hclose".
{ iFrame. iSplit. done. iApply lft_incl_trans. eauto. }
iIntros "!>". iNext. iMod "Hclose" as "[Hshr Htok]".
iIntros "!>{$Htok}". iApply (ty.(ty_shr_mono) with "[] Hshr").
iApply lft_incl_refl.
iAssert (κ0⋅κ' ⊑ κ0⋅κ) as "#Hκ0".
{ iApply lft_incl_lb. iSplit.
- iApply lft_le_incl. by exists κ'.
- iApply lft_incl_trans. iSplit; last done.
iApply lft_le_incl. exists κ0. apply (comm _). }
iExists l'. iSplit. by iApply (frac_borrow_shorten with "[]"). iIntros (q) "!#Htok".
iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]". set_solver.
iMod ("Hvs" $! q' with "Htok") as "Hclose'". iIntros "!>". iNext.
iMod "Hclose'" as "[#Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
by iApply (ty_shr_mono with "Hκ0").
Qed.
Next Obligation. done. Qed.
......@@ -358,7 +351,7 @@ Section types.
induction (combine_offs tyl 0) as [|[ty offs] ll IH].
- iIntros (?) "_$!>". by rewrite big_sepL_nil.
- iIntros (i) "Hown Htoks". rewrite big_sepL_cons.
iMod (lft_borrow_split with "Hown") as "[Hownh Hownq]". set_solver.
iMod (borrow_split with "Hown") as "[Hownh Hownq]". set_solver.
iMod (IH (S i)%nat with "Hownq Htoks") as "[#Hshrq Htoks]".
iMod (ty.(ty_share) _ (N .@ (i+0)%nat) with "Hownh Htoks") as "[#Hshrh $]".
solve_ndisj. done.
......@@ -392,8 +385,7 @@ Section types.
instantiate (1:=λ _ y, _). simpl. reflexivity. }
rewrite big_sepL_sepL. iDestruct "Hownq" as "[$ Hownq1]".
iIntros "[Hh Hq]". rewrite (lft_own_split κ q).
iMod ("Hcloseh" with "[$Hh $Hownh1]") as "($&$)".
iApply "Hcloseq". by iFrame.
iMod ("Hcloseh" with "[$Hh $Hownh1]") as "[$$]". iApply "Hcloseq". by iFrame.
Qed.
Lemma split_sum_mt l tid q tyl :
......@@ -402,10 +394,10 @@ Section types.
⊣⊢ ∃ (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.
- 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)".
- iDestruct "H" as (i) "[Hmt1 Hown]". iDestruct "Hown" as (vl) "[Hmt2 Hown]".
iExists (#i::vl). rewrite heap_mapsto_vec_cons. iFrame. eauto.
Qed.
......@@ -445,22 +437,22 @@ Section types.
Qed.
Next Obligation.
intros n tyl Hn E N κ l tid q ??. iIntros "Hown Htok". rewrite split_sum_mt.
iMod (lft_borrow_exists with "Hown Htok") as (i) "[Hown Htok]". set_solver.
iMod (lft_borrow_split with "Hown") as "[Hmt Hown]". set_solver.
iMod ((nth i tyl emp).(ty_share) with "Hown Htok") as "[#Hshr $]"; try done.
iExists i. iFrame "#". by iApply lft_borrow_fracture.
iMod (borrow_exists with "Hown Htok") as (i) "[Hown Htok]". set_solver.
iMod (borrow_split with "Hown") as "[Hmt Hown]". set_solver.
iMod ((nth i tyl emp).(ty_share) with "Hown Htok") as "[#Hshr Htok]"; try done.
iMod (borrow_fracture with "[-]") as "[H $]"; last by eauto. set_solver. iFrame.
Qed.
Next Obligation.
intros n tyl Hn κ κ' tid N l. iIntros "#Hord H".
iDestruct "H" as (i) "[Hown0 Hown]". iExists i. iSplitL "Hown0".
by iApply (lft_frac_borrow_incl with "Hord").
by iApply (frac_borrow_shorten with "Hord").
by iApply ((nth i tyl emp).(ty_shr_mono) with "Hord").
Qed.
Next Obligation.
intros n tyl Hn κ tid E N l q Hdup%Is_true_eq_true ?.
iIntros "#H[[Htok1 Htok2] Htl]".
setoid_rewrite split_sum_mt. iDestruct "H" as (i) "[Hshr0 Hshr]".
iMod (lft_frac_borrow_open with "[] Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver.
iMod (frac_borrow_acc with "[] Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver.
{ iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; eauto. }
iMod ((nth i tyl emp).(ty_shr_acc) with "Hshr [Htok2 $Htl]")
as (q'2) "[Hownq Hclose']"; try done.
......
theories/type_incl.v
+ 13
− 3
View file @ f207080e
......@@ -70,9 +70,19 @@ Section ty_incl.
Proof.
iIntros (tid) "#Hincl!>". iSplit; iIntros "!#*H".
- iDestruct "H" as (l) "[% Hown]". subst. iExists _. iSplit. done.
by iApply (lft_borrow_incl with "Hincl").
- admit. (* TODO : fix the definition before *)
Admitted.
by iApply (borrow_shorten with "Hincl").
- iAssert (κ1 ⋅ κ ⊑ κ2 ⋅ κ) as "#Hincl'".
{ iApply lft_incl_lb. iSplit.
- iApply lft_incl_trans. iSplit; last done.
iApply lft_le_incl. by exists κ.
- iApply lft_le_incl. exists κ1. by apply (comm _). }
iSplitL; last done. iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'.
iFrame. iIntros (q') "!#Htok".
iMod (lft_incl_acc with "Hincl' Htok") as (q'') "[Htok Hclose]". set_solver.
iMod ("Hupd" with "*Htok") as "Hupd'". iModIntro. iNext.
iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
iApply (ty_shr_mono with "Hincl' H").
Qed.
Lemma lft_incl_ty_incl_shared_borrow ty κ1 κ2 :
ty_incl (κ1 ⊑ κ2) (&shr{κ2}ty) (&shr{κ1}ty).
......
theories/typing.v
+ 75
− 74
View file @ f207080e
......@@ -129,23 +129,24 @@ Section typing.
Qed.
Lemma typed_newlft ρ:
typed_step ρ Newlft (λ _, ∃ α, [α]{1} ∗ α ∋ top)%P.
typed_step ρ Newlft (λ _, ∃ α, 1.[α] ∗ α ∋ top)%P.
Proof.
iIntros (tid) "!#(_&_&$)". wp_value. iMod lft_begin as (α) "[?#?]". done.
iMod (lft_borrow_create with "[][]") as "[_?]". done. done.
2:by iExists α; iFrame. eauto.
iIntros (tid) "!#(_&_&$)". wp_value. iMod lft_create as (α) "[?#?]". done.
iExists α. iFrame. iApply fupd_mask_mono. done.
iMod (borrow_create with "[]") as "[_?]". reflexivity. 2:by iIntros "!>". eauto.
Qed.
Lemma typed_endlft κ ρ:
typed_step (κ ∋ ρ ∗ [κ]{1}) Endlft (λ _, ρ)%P.
Proof.
iIntros (tid) "!#(_&[Hextr [Htok #Hlft]]&$)". wp_bind (#() ;; #())%E.
iApply (wp_wand_r _ _ (λ _, _ ∗ True)%I). iSplitR "Hextr".
iApply (wp_frame_step_l with "[-]"); try done.
iDestruct (lft_end with "Hlft Htok") as "$". by wp_seq.
iIntros (v) "[#Hκ _]". iMod (lft_extract_out with "Hκ Hextr"). done.
by wp_seq.
Qed.
(* TODO : lifetime ending permission. *)
(* Lemma typed_endlft κ ρ: *)
(* typed_step (κ ∋ ρ ∗ 1.[κ]) Endlft (λ _, ρ)%P. *)
(* Proof. *)
(* iIntros (tid) "!#(_&[Hextr Htok]&$)". wp_bind (#() ;; #())%E. *)
(* iApply (wp_wand_r _ _ (λ _, _ ∗ True)%I). iSplitR "Hextr". *)
(* iApply (wp_frame_step_l with "[-]"); try done. *)
(* iDestruct (lft_end with "Hlft Htok") as "$". by wp_seq. *)
(* iIntros (v) "[#Hκ _]". iMod (lft_extract_out with "Hκ Hextr"). done. *)
(* by wp_seq. *)
(* Qed. *)
Lemma typed_alloc ρ (n : nat):
0 < n → typed_step_ty ρ (Alloc #n) (own 1 (uninit n)).
......@@ -203,35 +204,33 @@ Section typing.
Lemma consumes_copy_uniq_borrow ty κ κ' q:
ty.(ty_dup) →
consumes ty (λ ν, ν ◁ &uniq{κ}ty ∗ κ' ⊑ κ ∗ [κ']{q})%P
(λ ν, ν ◁ &uniq{κ}ty ∗ κ' ⊑ κ ∗ [κ']{q})%P.
consumes ty (λ ν, ν ◁ &uniq{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
(λ ν, ν ◁ &uniq{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
Proof.
iIntros (? ν tid Φ E ?) "((H◁ & #H⊑ & Htok & #Hκ') & Htl & HΦ)".
iIntros (? ν tid Φ E ?) "((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_trade with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
iMod (lft_borrow_open with "H↦ Htok") as "[H↦ Hclose']". set_solver.
iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
iMod (borrow_acc with "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 (lft_borrow_close with "[H↦] Hclose'") as "[H↦ Htok]". set_solver.
{ iExists _. by iFrame. }
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_borrow ty κ κ' q:
ty.(ty_dup) →
consumes ty (λ ν, ν ◁ &shr{κ}ty ∗ κ' ⊑ κ ∗ [κ']{q})%P
(λ ν, ν ◁ &shr{κ}ty ∗ κ' ⊑ κ ∗ [κ']{q})%P.
consumes ty (λ ν, ν ◁ &shr{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
(λ ν, ν ◁ &shr{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
Proof.
iIntros (? ν tid Φ E ?) "((H◁ & #H⊑ & [Htok #Hκ']) & Htl & HΦ)".
iIntros (? ν tid Φ E ?) "((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_trade with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
rewrite (union_difference_L (nclose lrustN) ⊤); last done.
setoid_rewrite ->tl_own_union; try set_solver.
iDestruct "Htl" as "[Htl ?]".
setoid_rewrite ->tl_own_union; try set_solver. iDestruct "Htl" as "[Htl ?]".
iMod (ty_shr_acc with "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 ">%".
......@@ -253,38 +252,36 @@ Section typing.
Qed.
Lemma typed_deref_uniq_borrow_own ty ν κ κ' q q':
typed_step (ν ◁ &uniq{κ} own q' ty ∗ κ' ⊑ κ ∗ [κ']{q})
typed_step (ν ◁ &uniq{κ} own q' ty ∗ κ' ⊑ κ ∗ q.[κ'])
(!ν)
(λ v, v ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ [κ']{q})%P.
(λ v, v ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
Proof.
iIntros (tid) "!#(#HEAP & (H◁ & #H⊑ & Htok & #Hκ') & $)". wp_bind ν.
iIntros (tid) "!#(#HEAP & (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_trade with "H⊑ Htok") as (q'') "[Htok Hclose]". done.
iMod (lft_borrow_open with "H↦ Htok") as "[H↦ Hclose']". done.
iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[Htok Hclose]". done.
iMod (borrow_acc_strong with "H↦ Htok") as "[H↦ Hclose']". done.
iDestruct "H↦" as (vl) "[>H↦ Hown]". iDestruct "Hown" as (l') "(>% & H† & Hown)".
subst. rewrite heap_mapsto_vec_singleton. wp_read.
iMod (lft_borrow_close_stronger with "[H↦ H† Hown] Hclose' []") as "[Hbor Htok]";
first done; first 2 last.
- iMod (lft_borrow_split with "Hbor") as "[_ Hbor]". done.
iMod (lft_borrow_split with "Hbor") as "[_ Hbor]". done.
iMod ("Hclose'" with "*[H↦ H† Hown]") as "[Hbor Htok]"; last first.
- iMod (borrow_split with "Hbor") as "[_ Hbor]". done.
iMod (borrow_split with "Hbor") as "[_ Hbor]". done.
iMod ("Hclose" with "Htok") as "$". iFrame "#". iExists _. eauto.
- by iFrame "H↦ H†".
- iIntros "!>(?&?&?)!>". iNext. iExists _.
- iIntros "{$H↦ $H† $Hown}!>[_(?&?&?)]!>". iNext. iExists _.
rewrite -heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame.
Qed.
Lemma typed_deref_shr_borrow_own ty ν κ κ' q q':
typed_step (ν ◁ &shr{κ} own q' ty ∗ κ' ⊑ κ ∗ [κ']{q})
typed_step (ν ◁ &shr{κ} own q' ty ∗ κ' ⊑ κ ∗ q.[κ'])
(!ν)
(λ v, v ◁ &shr{κ} ty ∗ κ' ⊑ κ ∗ [κ']{q})%P.
(λ v, v ◁ &shr{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
Proof.
iIntros (tid) "!#(#HEAP & (H◁ & #H⊑ & Htok & #Hκ') & $)". wp_bind ν.
iIntros (tid) "!#(#HEAP & (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_trade with "H⊑ Htok") as (q'') "[[Htok1 Htok2] Hclose]". done.
iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[[Htok1 Htok2] Hclose]". done.
iDestruct "H↦" as (vl) "[H↦b Hown]".
iMod (lft_frac_borrow_open with "[] H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
iMod (frac_borrow_acc with "[] H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
{ iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; auto. }
iSpecialize ("Hown" $! _ with "Htok2").
iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose'"; last first.
......@@ -299,49 +296,54 @@ Section typing.
Qed.
Lemma typed_deref_uniq_borrow_borrow ty ν κ κ' κ'' q:
typed_step (ν ◁ &uniq{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ [κ]{q} ∗ κ' ⊑ κ'')
typed_step (ν ◁ &uniq{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ q.[κ] ∗ κ' ⊑ κ'')
(!ν)
(λ v, v ◁ &uniq{κ'} ty ∗ κ ⊑ κ' ∗ [κ]{q})%P.
(λ v, v ◁ &uniq{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
Proof.
iIntros (tid) "!#(#HEAP & (H◁ & #H⊑1 & [Htok #Hκ'] & #H⊑2) & $)". wp_bind ν.
iIntros (tid) "!#(#HEAP & (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_trade with "H⊑1 Htok") as (q'') "[Htok Hclose]". done.
iMod (lft_borrow_exists with "H↦ Htok") as (vl) "[Hbor Htok]". done.
iMod (lft_borrow_split with "Hbor") as "[H↦ Hbor]". done.
iMod (lft_borrow_exists with "Hbor Htok") as (l') "[Hbor Htok]". done.
iMod (lft_borrow_split with "Hbor") as "[Heq Hbor]". done.
iMod (lft_borrow_persistent with "Heq Htok") as "[>% [Htok1 Htok2]]". done. subst.
iMod (lft_borrow_open with "H↦ Htok1") as "[>H↦ Hclose']". done.
iMod (lft_borrow_open with "Hbor Htok2") as "[Hbor Hclose'']". done.
iMod (lft_incl_acc with "H⊑1 Htok") as (q'') "[Htok Hclose]". done.
iMod (borrow_exists with "H↦ Htok") as (vl) "[Hbor Htok]". done.
iMod (borrow_split with "Hbor") as "[H↦ Hbor]". done.
iMod (borrow_exists with "Hbor Htok") as (l') "[Hbor Htok]". done.
iMod (borrow_split with "Hbor") as "[Heq Hbor]". done.
iMod (borrow_unnest with "Hbor") as "Hbor". done.
iMod (borrow_persistent with "Heq Htok") as "[>% Htok]". done. subst.
iMod (borrow_acc with "H↦ Htok") as "[>H↦ Hclose']". done.
rewrite heap_mapsto_vec_singleton. wp_read.
iMod (lft_borrow_close with "[$H↦] Hclose'") as "[_ Htok1]". done.
iMod (lft_borrow_unnest with "H⊑2 [$Hbor $Hclose'']") as "[Htok2 Hbor]". done.
iMod ("Hclose" with "[$Htok1 $Htok2]") as "$".
iFrame "#". iExists _. eauto.
iMod ("Hclose'" with "[$H↦]") as "[H↦ Htok]".
iMod ("Hclose" with "Htok") as "$". iFrame "#".
iMod "Hbor". iExists _. iSplitR. done. iApply (borrow_shorten with "[] Hbor").
iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl.
Qed.
Lemma typed_deref_shr_borrow_borrow ty ν κ κ' κ'' q:
typed_step (ν ◁ &shr{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ [κ]{q} ∗ κ' ⊑ κ'')
typed_step (ν ◁ &shr{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ q.[κ] ∗ κ' ⊑ κ'')
(!ν)
(λ v, v ◁ &shr{κ'} ty ∗ κ ⊑ κ' ∗ [κ]{q})%P.
(λ v, v ◁ &shr{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
Proof.
iIntros (tid) "!#(#HEAP & (H◁ & #H⊑1 & [Htok #Hκ'] & #H⊑2) & $)". wp_bind ν.
iIntros (tid) "!#(#HEAP & (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_trade with "H⊑1 Htok") as (q') "[[Htok1 Htok2] Hclose]". done.
iMod (lft_frac_borrow_open with "[] H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
iMod (lft_incl_acc with "H⊑1 Htok") as (q') "[[Htok1 Htok2] Hclose]". done.
iMod (frac_borrow_acc with "[] H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
{ iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; auto. }
iSpecialize ("Hown" $! _ _ with "[$H⊑2 $Htok2]"). iApply lft_incl_refl.
iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose'"; last first.
iAssert (κ' ⊑ κ'' ⋅ κ') as "#H⊑3".
{ iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl. }
iMod (lft_incl_acc with "H⊑3 Htok2") as (q''') "[Htok Hclose'']". done.
iSpecialize ("Hown" $! _ with "Htok").
iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose' Hclose''"; last first.
- iApply (wp_frame_step_l _ heapN _ (λ v, l ↦{q''} v ∗ v = #l')%I); try done.
iSplitL "Hown"; last by wp_read; eauto.
iApply step_fupd_mask_mono; last iApply (step_fupd_mask_frame_r _ _ heapN);
last iApply "Hown"; (set_solver || rewrite !disjoint_union_l; solve_ndisj).
- iIntros (v) "([#Hshr Htok] & H↦ & %)". subst.
iMod ("Hclose''" with "Htok") as "Htok".
iMod ("Hclose'" with "[$H↦]") as "Htok'".
iMod ("Hclose" with "[$Htok $Htok']") as "$". iFrame "#". iExists _. eauto.
iMod ("Hclose" with "[$Htok $Htok']") as "$". iFrame "#". iExists _.
iSplitL. done. iApply (ty_shr_mono with "H⊑3 Hshr").
Qed.
Definition update (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
......@@ -367,18 +369,17 @@ Section typing.
Qed.
Lemma update_weak ty q κ κ':
update ty (λ ν, ν ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ [κ']{q})%P
(λ ν, ν ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ [κ']{q})%P.
update ty (λ ν, ν ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
(λ ν, ν ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
Proof.
iIntros (ν tid Φ E ?) "[(H◁ & #H⊑ & Htok & #Hκ) HΦ]".
iIntros (ν tid Φ E ?) "[(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_trade with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
iMod (lft_borrow_open with "H↦ Htok") as "[H↦ Hclose']". set_solver.
iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
iMod (borrow_acc with "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 (lft_borrow_close with "[H↦ Hown] Hclose'") as "[Hbor Htok]". set_solver.
{ iExists _. iFrame. }
iMod ("Hclose'" with "[H↦ Hown]") as "[Hbor Htok]". by iExists _; iFrame.
iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
Qed.
......@@ -403,7 +404,7 @@ Section typing.
iIntros (l vl) "(% & % & H↦ & Hupd)". wp_bind ν2.
iApply (Hcons with "[- $H2 $Htl]"). done.
iIntros (l' vl' q) "(% & % & H↦' & Hcons)". iApply wp_fupd.
iMod "Hcons". iApply wp_memcpy; last iFrame "∗#"; try done. iNext.
iMod "Hcons". iApply (wp_memcpy with "[$HEAP $H↦' $H↦]"); try done. iNext.
iIntros "[H↦ H↦']". iMod "Hcons" as "[Hown' Hcons]".
iMod ("Hcons" with "H↦'") as "[$$]". iApply "Hupd". by iFrame.
Qed.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment