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

Dereferencing and dropping a RefMut.

parent 6c83f2c8
No related branches found
No related tags found
No related merge requests found
......@@ -57,3 +57,4 @@ theories/typing/unsafe/refcell/ref.v
theories/typing/unsafe/refcell/refmut.v
theories/typing/unsafe/refcell/refcell_code.v
theories/typing/unsafe/refcell/ref_code.v
theories/typing/unsafe/refcell/refmut_code.v
......@@ -13,35 +13,33 @@ Section ref_functions.
Lemma refcell_inv_reading_inv tid l γ α ty q ν :
refcell_inv tid l γ α ty -∗
own γ ( reading_st q ν) -∗
q' q'' n, l #(Zpos n)
own γ ( Some (Cinr (to_agree ν, q', n)) reading_st q ν)
(q' + q'' = 1)%Qp (q q')%Qc q''.[ν]
(q' : Qp) n, l #(Zpos n) (q q')%Qc
own γ ( Some (to_agree ν, Cinr (q', n)) reading_st q ν)
ty.(ty_shr) (α ν) tid (shift_loc l 1)
((1).[ν] ={, lftN}▷=∗ &{α} shift_loc l 1 ↦∗: ty_own ty tid).
((1).[ν] ={, lftN}▷=∗ &{α} shift_loc l 1 ↦∗: ty_own ty tid)
q'', (q' + q'' = 1)%Qp q''.[ν].
Proof.
iIntros "INV H◯".
iDestruct "INV" as (st) "(H↦lrc & H● & INV)".
iAssert ( q' n, st Some (Cinr (to_agree ν, q', n)) q q'⌝%Qc)%I with
iAssert ( q' n, st Some (to_agree ν, Cinr (q', n)) q q'⌝%Qc)%I with
"[#]" as (q' n) "[Hst %]".
{ iDestruct (own_valid_2 with "H● H◯") as %[[[=]|
(? & st' & [=<-] & -> & [Heq|Hle])]%option_included Hv]%auth_valid_discrete_2.
- iExists q, xH. iSplit; iPureIntro. by constructor. done.
(? & [agν st'] & [=<-] & -> & [Heq|Hle])]%option_included Hv]%auth_valid_discrete_2.
- iExists q, xH. iSplit; iPureIntro. by constructor. done.
- iClear "∗#".
revert Hle Hv=>/csum_included [ -> // | [[?[?[//]]] | [?[st''[Heq[-> Hle]]]]]].
revert Heq. intros [= <-]. destruct st'' as [[ag q'] n].
revert Hle=>/Some_included_2 /Some_pair_included
[/Some_pair_included_total_1 [/agree_included Heq Hqq'] _] [[Hag _] _].
revert Hle Hv=>/prod_included [/= /agree_included Hag /csum_included
[-> [//] | [[?[?[//]]] | [?[[q' n] [Heq [-> Hle]]]]]]] [Hagok _].
revert Heq. intros [= <-]. revert Hle=>/prod_included [/= Hqq' _].
iExists q', n. iSplit.
+ iPureIntro. do 4 constructor; last done.
apply agree_op_inv. by rewrite comm -Heq.
+ revert Hqq'. by intros [<-%leibniz_equiv|?%frac_included_weak]%Some_included. }
+ iPureIntro. rewrite (agree_op_inv agν) //. by rewrite comm -Hag.
+ by revert Hqq'=>/frac_included_weak. }
iDestruct "Hst" as %[st' [-> Hst']]%equiv_Some_inv_r'.
destruct st' as [|[[]]|]; try by inversion Hst'. apply (inj Cinr), (inj2 pair) in Hst'.
destruct Hst' as [[Hst' <-%leibniz_equiv]%(inj2 pair) <-%leibniz_equiv].
simpl. setoid_rewrite <-Hst'. clear Hst'.
iDestruct "INV" as (q'' ν') "(Hag & Hq'q'' & Hν & INV)".
destruct st' as [?[|[]|]]; destruct Hst' as [Hag Hst']; try by inversion Hst'.
apply (inj Cinr), (inj2 pair) in Hst'.
destruct Hst' as [<-%leibniz_equiv <-%leibniz_equiv]. simpl in *.
setoid_rewrite <-Hag. iDestruct "INV" as (ν') "(Hag & Hν & Hshr & Hq')".
iDestruct "Hag" as %<-%(inj to_agree)%leibniz_equiv.
iDestruct "Hq'q''" as %Hq'q''. iExists _, _, _. rewrite own_op. iFrame. auto.
iExists q', n. rewrite own_op. by iFrame.
Qed.
(* Cloning a ref. We need to increment the counter. *)
......@@ -77,12 +75,12 @@ Section ref_functions.
rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iMod "H↦" as "[H↦1 H↦2]". wp_read. wp_let.
iDestruct (refcell_inv_reading_inv with "INV H◯")
as (q' q'' n) "(H↦lrc & [H● H◯] & Hq'q'' & [Hν1 Hν2] & INV)".
wp_read. wp_let. wp_op. wp_write. iDestruct "Hq'q''" as %[Hq'q'' _].
iMod (own_update with "H●") as "[H● ?]".
as (q' n) "(H↦lrc & _ & [H● H◯] & Hshr' & H† & Hq')".
wp_read. wp_let. wp_op. wp_write. iDestruct "Hq'" as (q'') "(Hq'q'' & Hν1 & Hν2)".
iDestruct "Hq'q''" as %Hq'q''. iMod (own_update with "H●") as "[H● ?]".
{ apply auth_update_alloc,
(op_local_update_discrete _ _ (reading_st (q''/2)%Qp ν))=>-[[Hagv _]_].
split; [split|done].
(op_local_update_discrete _ _ (reading_st (q''/2)%Qp ν))=>-[Hagv _].
split; [|split; last done].
- by rewrite /= agree_idemp.
- change ((q''/2+q')%Qp 1%Qp)%Qc. rewrite -Hq'q'' comm -{2}(Qp_div_2 q'').
apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q''/2)%Qp).
......@@ -93,9 +91,11 @@ Section ref_functions.
wp_let. wp_bind (_ <-{_} !_)%E. iApply (wp_memcpy with "[$Hlr $H↦]"); [done..|].
iIntros "!>[Hlr H↦]". wp_seq.
iMod ("Hcloseα2" with "[$H◯] Hna") as "[Hα2 Hna]".
iMod ("Hcloseδ" with "[H↦lrc H● Hν1 INV] Hna") as "[Hδ Hna]".
{ iExists _. rewrite Z.add_comm. iFrame. iExists _, _. iFrame. simpl.
rewrite agree_idemp (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto. }
iMod ("Hcloseδ" with "[H↦lrc H● Hν1 Hshr' H†] Hna") as "[Hδ Hna]".
{ iExists _. rewrite Z.add_comm. iFrame. iExists _. iFrame. iSplitR.
- rewrite /= agree_idemp. auto.
- iExists _. iFrame.
rewrite (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto. }
iMod ("Hcloseβ" with "Hδ") as "Hβ". iMod ("Hcloseα1" with "[$H↦]") as "Hα1".
iAssert (elctx_interp [ α; β] qE) with "[Hα1 Hα2 Hβ]" as "HE".
{ rewrite /elctx_interp big_sepL_cons big_sepL_singleton. iFrame. }
......@@ -173,29 +173,28 @@ Section ref_functions.
iMod (lft_incl_acc with "Hαβ Hα") as () "[Hβ Hcloseα]". done.
iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hcloseβ)"; [done..|].
iDestruct (refcell_inv_reading_inv with "INV [$H◯]")
as (q' q'' n) "(H↦lrc & H●◯ & >% & Hν' & Hshr & Hend)".
as (q' n) "(H↦lrc & >% & H●◯ & Hshr & H & Hq')". iDestruct "Hq'" as (q'') ">[% Hν']".
wp_read. wp_let. wp_op. wp_write.
iAssert (|={, lftN}▷=> refcell_inv tid lrc γ β ty')%I
with "[H↦lrc H●◯ Hν Hν' Hshr Hend]" as "INV".
{ iDestruct (own_valid with "H●◯")
as %[[Heq%(inj Cinr)|Hincl%csum_included]%Some_included Hv]%auth_valid_discrete_2.
- destruct Heq as [[_ ?%leibniz_equiv]?%leibniz_equiv]. simpl in *. subst.
with "[H↦lrc H●◯ Hν Hν' Hshr H]" as "INV".
{ iDestruct (own_valid with "H●◯") as %[[ _ [Heq%(inj Cinr)|Hincl%csum_included]
%Some_included]%Some_pair_included [_ Hv]]%auth_valid_discrete_2.
- destruct Heq as [?%leibniz_equiv ?%leibniz_equiv]. simpl in *. subst.
iExists None. iFrame. iMod (own_update with "H●◯") as "$".
{ apply auth_update_dealloc. rewrite -(right_id None op (Some _)).
apply op_local_update_cancellable_empty, _. }
iApply "Hend". replace 1%Qp with (q'+q'')%Qp by naive_solver. iFrame.
- destruct Hincl as [[=]|[(?&?&[=]&?)|(?&?&[=<-]&[=<-]&[[[ag q0]n']EQ])]].
rewrite EQ. destruct EQ as [[EQag ?%leibniz_equiv]?%leibniz_equiv].
simpl in *. subst.
iApply "H†". replace 1%Qp with (q'+q'')%Qp by naive_solver. iFrame.
- destruct Hincl as [ [=] |[ (?&?&[=]&?) | (?&?&[=<-]&[=<-]&[[q0 n']EQ]) ]].
destruct EQ as [?%leibniz_equiv ?%leibniz_equiv]. simpl in *. subst.
iAssert (lrc #(Z.pos n'))%I with "[H↦lrc]" as "H↦lrc".
{ destruct n'; [|done..]. by rewrite /= Pos.pred_double_succ. }
iExists (Some (Cinr (ag, q0, n'))). iFrame. iMod (own_update with "H●◯") as "$".
{ apply auth_update_dealloc. rewrite -Cinr_op Some_op.
iExists (Some (_, Cinr (q0, n'))). iFrame. iMod (own_update with "H●◯") as "$".
{ apply auth_update_dealloc.
rewrite -(agree_idemp (to_agree _)) -pair_op -Cinr_op -pair_op Some_op.
apply (op_local_update_cancellable_empty (reading_st q ν)), _. }
iExists (q+q'')%Qp, ν. iFrame. iApply step_fupd_intro; first done. iIntros "!>".
iSplit; iPureIntro.
+ apply agree_op_inv. by rewrite comm -EQag.
+ rewrite assoc (comm _ q0 q). by intuition. }
iExists ν. iFrame. iApply step_fupd_intro; first done. iIntros "!>".
iSplitR; first done. iExists (q+q'')%Qp. iFrame.
by rewrite assoc (comm _ q0 q). }
wp_bind Endlft. iApply (wp_fupd_step with "INV"); [done..|]. wp_seq.
iIntros "INV !>". wp_seq. iMod ("Hcloseβ" with "[$INV] Hna") as "[Hβ Hna]".
iMod ("Hcloseα" with "Hβ") as "Hα".
......
......@@ -6,20 +6,21 @@ From lrust.typing Require Import typing.
Set Default Proof Using "Type".
Definition refcell_stR :=
optionUR (csumR (exclR unitC) (prodR (prodR (agreeR lftC) fracR) positiveR)).
optionUR (prodR (agreeR lftC) (csumR (exclR unitC) (prodR fracR positiveR))).
Class refcellG Σ :=
RefCellG :> inG Σ (authR refcell_stR).
Definition Z_of_refcell_st (st : refcell_stR) : Z :=
match st with
| None => 0
| Some (Cinr (_, _, n)) => Zpos n
| Some (_, Cinr (_, n)) => Zpos n
| Some _ => -1
end.
Definition reading_st (q : frac) (ν : lft) : refcell_stR :=
Some (Cinr (to_agree ν, q, xH)).
Definition writing_st : refcell_stR := Some (Cinl (Excl ())).
Some (to_agree ν, Cinr (q, xH)).
Definition writing_st (ν : lft) : refcell_stR :=
Some (to_agree ν, Cinl (Excl ())).
Definition refcellN := lrustN .@ "refcell".
Definition refcell_invN := refcellN .@ "inv".
......@@ -30,12 +31,19 @@ Section refcell_inv.
Definition refcell_inv tid (l : loc) (γ : gname) (α : lft) ty : iProp Σ :=
( st, l #(Z_of_refcell_st st) own γ ( st)
match st return _ with
| None => &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)
| Some (Cinr (agν, q, n)) =>
q' ν, agν to_agree ν (q + q')%Qp = 1%Qp q'.[ν]
ty.(ty_shr) (α ν) tid (shift_loc l 1)
(1.[ν] ={, ⊤∖↑lftN}▷=∗ &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid))
| Some _ => True
| None =>
(* Not borrowed. *)
&{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)
| Some (agν, st) =>
ν, agν to_agree ν
(1.[ν] ={, ⊤∖↑lftN}▷=∗ &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid))
match st with
| Cinr (q, n) =>
(* Immutably borrowed. *)
ty.(ty_shr) (α ν) tid (shift_loc l 1)
q', (q + q')%Qp = 1%Qp q'.[ν]
| _ => (* Mutably borrowed. *) True
end
end)%I.
Global Instance refcell_inv_ne n tid l γ α :
......@@ -60,11 +68,12 @@ Section refcell_inv.
iSplit; iIntros "!>!#H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
iFrame; by iApply "Hown". }
iDestruct "H" as (st) "H"; iExists st;
iDestruct "H" as "($&$&H)"; destruct st as [[|[[]]|]|]; try done;
iDestruct "H" as "($&$&H)"; destruct st as [[agν st]|]; try done;
last by iApply "Hb".
iDestruct "H" as (q' ν) "(Hag & Heq & Htok & Hs & Hh)". iExists q', ν.
iDestruct ("Hshr" with "Hs") as "$". iFrame. iIntros "H†".
iMod ("Hh" with "H†") as "Hh". iModIntro. iNext. iMod "Hh". by iApply "Hb".
iDestruct "H" as (ν) "(Hag & Hh & H)". iExists ν. iFrame. iSplitL "Hh".
{ iIntros "Hν". iMod ("Hh" with "Hν") as "Hh". iModIntro. iNext.
iMod "Hh". by iApply "Hb". }
destruct st as [|[]|]; try done. iDestruct "H" as "[H $]". by iApply "Hshr".
Qed.
End refcell_inv.
......@@ -102,26 +111,27 @@ Section refcell.
as "[$ HQ]"; last first.
{ iMod ("Hclose" with "HQ []") as "[Hb $]".
- iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(? & _ & _)".
iExists _. iIntros "{$H}!%". destruct st as [[|[[]?]|]|]; simpl; lia.
iExists _. iIntros "{$H}!%". destruct st as [[?[|[]|]]|]; simpl; lia.
- iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
iExists κ, γ. iSplitR. by iApply lft_incl_refl. by iApply bor_na. }
clear dependent n. iDestruct "H" as ([|n|[]]) "[Hn >%]"; try lia.
- iFrame. iMod (own_alloc ( None)) as (γ) "Hst". done. iExists γ, None. by iFrame.
- iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
iMod (own_alloc ( Some (Cinr (to_agree ν, (1/2)%Qp, n)))) as (γ) "Hst".
iMod (own_alloc ( Some (to_agree ν, Cinr ((1/2)%Qp, n)))) as (γ) "Hst".
{ by apply auth_auth_valid. }
iMod (rebor _ _ (κ ν) with "LFT [] Hvl") as "[Hvl Hh]". done.
{ iApply lft_le_incl. apply gmultiset_union_subseteq_l. }
iDestruct (lft_glb_acc with "Htok' Htok1") as (q') "[Htok Hclose]".
iMod (ty_share with "LFT Hvl Htok") as "[Hshr Htok]". done.
iDestruct ("Hclose" with "Htok") as "[$ Htok]".
iExists γ, _. iFrame "Hst Hn". iExists _, _. iIntros "{$Htok2 $Hshr}!>!>".
rewrite Qp_div_2. iSplit; first done. iSplit; first done. iIntros "Hν".
iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
iExists γ, _. iFrame "Hst Hn". iExists _. iIntros "{$Hshr}".
iSplitR; first by auto. iSplitR "Htok2"; last first.
{ iExists _. iFrame. rewrite Qp_div_2. auto. }
iIntros "!> !> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
iApply fupd_mask_mono; last iApply "Hh". done. rewrite -lft_dead_or. auto.
- iMod (own_alloc ( Some (Cinl (Excl ())))) as (γ) "Hst".
{ by apply auth_auth_valid. }
iFrame. iExists _, _. by iFrame.
- iMod (own_alloc ( writing_st static)) as (γ) "Hst". { by apply auth_auth_valid. }
iFrame. iExists _, _. iFrame. iExists _. iSplitR; first by auto.
iIntros "!>!> _". iApply step_fupd_intro; auto.
Qed.
Next Obligation.
iIntros (?????) "LFT #Hκ H". iDestruct "H" as (α γ) "[#??]".
......
......@@ -176,21 +176,22 @@ Section refcell_functions.
ty_shr ty (β ν) tid (shift_loc lx 1)
own γ ( reading_st ν) refcell_inv tid lx γ β ty)%I
with ">[Hlx Hownst Hst Hβtok2]" as (q' ν) "(Hβtok2 & Hν & Hshr & Hreading & INV)".
{ destruct st as [[|[[agν q] n]|]|]; try done.
- iDestruct "Hst" as (q' ν) "(Hag & #Hqq' & [Hν1 Hν2] & #Hshr & H†)".
{ destruct st as [[agν [|[q n]|]]|]; try done.
- iDestruct "Hst" as (ν) "(Hag & H† & #Hshr & Hst)".
iDestruct "Hst" as (q') "(#Hqq' & [Hν1 Hν2])".
iExists _, _. iFrame "Hν1". iDestruct "Hag" as %Hag. iDestruct "Hqq'" as %Hqq'.
iMod (own_update with "Hownst") as "[Hownst ?]".
{ apply auth_update_alloc,
(op_local_update_discrete _ _ (reading_st (q'/2)%Qp ν))=>-[[Hagv _]_].
split; [split|].
(op_local_update_discrete _ _ (reading_st (q'/2)%Qp ν))=>-[Hagv _].
split; [|split].
- by rewrite -Hag /= agree_idemp.
- change ((q'/2+q)%Qp 1%Qp)%Qc. rewrite -Hqq' comm -{2}(Qp_div_2 q').
apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q'/2)%Qp).
apply Qcplus_le_mono_r, Qp_ge_0.
- done. }
iFrame "∗#". iExists _. rewrite Z.add_comm /=. iFrame. iExists _, _. iFrame.
rewrite /= Hag agree_idemp (comm Qp_plus) (assoc Qp_plus) Qp_div_2
(comm Qp_plus). auto.
iFrame "∗#". iExists _. rewrite Z.add_comm /=. iFrame. iExists _. iFrame.
iSplitR; first by rewrite /= Hag agree_idemp. iFrame "Hshr". iExists _. iFrame.
rewrite (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto.
- iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
auth_update_alloc, (op_local_update_discrete _ _ (reading_st (1/2)%Qp ν)).
......@@ -200,9 +201,10 @@ Section refcell_functions.
{ iApply lft_le_incl. apply gmultiset_union_subseteq_l. }
iMod (ty_share with "LFT Hst Htok") as "[#Hshr Htok]". done. iFrame "Hshr".
iDestruct ("Hclose" with "Htok") as "[$ Htok2]". iExists _. iFrame.
iExists _, _. iFrame. rewrite Qp_div_2. iSplitR; first done. iSplitR; first done.
iIntros "{$Hshr} !> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro.
iNext. iMod "Hν". iApply "Hh". rewrite -lft_dead_or. auto. }
iExists _. iSplitR; first done. iFrame "Hshr". iSplitR "Htok2".
+ iIntros "!> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro.
iNext. iMod "Hν". iApply "Hh". rewrite -lft_dead_or. auto.
+ iExists _. iFrame. by rewrite Qp_div_2. }
iMod ("Hclose'" with "[$INV] Hna") as "[Hβtok1 Hna]".
iAssert (elctx_interp [α] qE)%I with ">[Hclose Hβtok1 Hβtok2]" as "HE".
{ rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
......@@ -259,17 +261,22 @@ Section refcell_functions.
rewrite {1}/elctx_interp big_sepL_singleton.
iMod (lft_incl_acc with "Hαβ HE") as () "[Hβtok Hclose]". done.
iMod (na_bor_acc with "LFT Hinv Hβtok Hna") as "(INV & Hna & Hclose')"; try done.
iDestruct "INV" as (st) "(Hlx & Hownst & Hst)". wp_read. wp_let. wp_op=>?; wp_if.
iDestruct "INV" as (st) "(Hlx & Hownst & Hb)". wp_read. wp_let. wp_op=>?; wp_if.
- wp_write. wp_bind (new _). iApply wp_new; [done..|]. iNext.
iIntros (lref vl) "(EQ & H† & Hlref)". iDestruct "EQ" as %?%(inj Z.of_nat 2%nat).
destruct vl as [|?[|?[]]]; try done. wp_let.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iDestruct "Hlref" as "[Hlref0 Hlref1]". wp_op. wp_write. wp_op. wp_write.
destruct st as [[|[[]]|]|]; try done.
destruct st as [[?[|[]|]]|]; try done.
iMod (lft_create with "LFT") as (ν) "[Htok #Hhν]". done.
iMod (own_update with "Hownst") as "[Hownst ?]".
{ apply auth_update_alloc, (op_local_update_discrete _ _ writing_st)=>//. }
iMod ("Hclose'" with "[Hlx Hownst] Hna") as "[Hβtok Hna]";
first by iExists _; iFrame.
{ by eapply auth_update_alloc, (op_local_update_discrete _ _ (writing_st ν)). }
iMod (rebor _ _ (β ν) with "LFT [] Hb") as "[Hb Hbh]". done.
{ iApply lft_le_incl. apply gmultiset_union_subseteq_l. }
iMod ("Hclose'" with "[Hlx Hownst Hbh] Hna") as "[Hβtok Hna]".
{ iExists _. iFrame. iExists ν. iSplit; first by auto. iNext. iSplitL; last by auto.
iIntros "Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
iApply "Hbh". rewrite -lft_dead_or. auto. }
iAssert (elctx_interp [α] qE)%I with ">[Hclose Hβtok]" as "HE".
{ rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
iApply (type_sum_memcpy [refmut α ty; unit] _ _ _ _ _ _ _ _
......@@ -280,9 +287,10 @@ Section refcell_functions.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
iExists [_; _]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iFrame. iExists _, _, _. iFrame "∗#". }
iFrame. iExists _, _, _, _. iFrame "#∗". iApply (bor_shorten with "[] [$Hb]").
iApply lft_glb_mono; first done. iApply lft_incl_refl. }
simpl. eapply type_delete; [solve_typing..|]. eapply (type_jump [_]); solve_typing.
- iMod ("Hclose'" with "[Hlx Hownst Hst] Hna") as "[Hβtok Hna]";
- iMod ("Hclose'" with "[Hlx Hownst Hb] Hna") as "[Hβtok Hna]";
first by iExists st; iFrame.
iAssert (elctx_interp [α] qE)%I with ">[Hclose Hβtok]" as "HE".
{ rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
......
......@@ -15,9 +15,9 @@ Section refmut.
ty_own tid vl :=
match vl return _ with
| [ #(LitLoc lv); #(LitLoc lrc) ] =>
γ β ty', &{β}(lv ↦∗: ty.(ty_own) tid)
ν γ β ty', &{α ν}(lv ↦∗: ty.(ty_own) tid)
α β &na{β, tid, refcell_invN}(refcell_inv tid lrc γ β ty')
own γ ( writing_st)
1.[ν] own γ ( writing_st ν)
| _ => False
end;
ty_shr κ tid l :=
......@@ -35,10 +35,16 @@ Section refmut.
iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". done.
destruct vl as [|[[|lv|]|][|[[|lrc|]|][]]];
try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
iMod (bor_exists with "LFT Hb") as (ν) "Hb". done.
iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
iMod (bor_exists with "LFT Hb") as (β) "Hb". done.
iMod (bor_exists with "LFT Hb") as (ty') "Hb". done.
rewrite (assoc _ _ (α β)%I). iMod (bor_sep with "LFT Hb") as "[Hb _]". done.
rewrite (assoc _ _ (α β)%I). iMod (bor_sep with "LFT Hb") as "[Hb H]". done.
rewrite (comm _ (1).[ν])%I. rewrite (assoc _ _ _ (1).[ν])%I.
iMod (bor_sep with "LFT H") as "[_ H]". done.
iMod (bor_fracture (λ q, (1 * q).[ν])%I with "LFT [H]") as "H". done.
{ by rewrite Qp_mult_1_l. }
iDestruct (frac_bor_lft_incl _ _ 1 with "LFT H") as "#Hκν". iClear "H".
iMod (bor_sep with "LFT Hb") as "[Hb Hαβ]". done.
iMod (bor_persistent_tok with "LFT Hαβ Htok") as "[#Hαβ $]". done.
iExists _, _. iFrame "H↦". rewrite {1}bor_unfold_idx.
......@@ -52,7 +58,9 @@ Section refmut.
{ iApply bor_unfold_idx. eauto. }
iModIntro. iNext. iMod "Hb".
iMod (ty.(ty_share) with "LFT [Hb] Htok") as "[#Hshr $]". solve_ndisj.
{ iApply bor_shorten; last done. iApply lft_glb_mono. done. iApply lft_incl_refl. }
{ iApply bor_shorten; last done. rewrite -assoc.
iApply lft_glb_mono; first by iApply lft_incl_refl.
iApply lft_incl_glb; first done. iApply lft_incl_refl. }
iMod ("Hclose" with "[]") as "_"; auto.
- iMod ("Hclose" with "[]") as "_". by eauto.
iApply step_fupd_intro. set_solver. auto.
......@@ -88,10 +96,11 @@ Section refmut.
iSplit; [|iSplit; iAlways].
- done.
- iIntros (tid [|[[]|][|[[]|][]]]); try iIntros "[]". iIntros "H".
iDestruct "H" as (γ β ty') "(Hb & #H⊑ & #Hinv & Hown)".
iExists γ, β, ty'. iFrame "∗#". iSplit.
+ iApply bor_iff; last done.
iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]";
iDestruct "H" as (ν γ β ty') "(Hb & #H⊑ & #Hinv & Hν & Hown)".
iExists ν, γ, β, ty'. iFrame "∗#". iSplit.
+ iApply bor_shorten; last iApply bor_iff; last done.
* iApply lft_glb_mono; first done. iApply lft_incl_refl.
* iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]";
iExists vl; iFrame; by iApply "Ho".
+ by iApply lft_incl_trans.
- iIntros (κ tid l) "H". iDestruct "H" as (lv lrc) "H". iExists lv, lrc.
......
From Coq.QArith Require Import Qcanon.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth csum frac agree.
From iris.base_logic Require Import big_op fractional.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Import typing.
From lrust.typing.unsafe.refcell Require Import refcell refmut.
Set Default Proof Using "Type".
Section refmut_functions.
Context `{typeG Σ, refcellG Σ}.
(* TODO : map, when we will have a nice story about closures. *)
(* Turning a refmut into a shared borrow. *)
Definition refmut_deref : val :=
funrec: <> ["x"] :=
let: "x'" := !"x" in
let: "r'" := !"x'" in
letalloc: "r" <- "r'" in
delete [ #1; "x"];; "return" ["r"].
Lemma refmut_deref_type ty :
typed_instruction_ty [] [] [] refmut_deref
(fn (fun '(α, β) => [α; β; α β])%EL
(fun '(α, β) => [# &shr{α}(refmut β ty)]%T)
(fun '(α, β) => &shr{α}ty)%T).
Proof.
apply type_fn; [apply _..|]. move=>/= [α β] ret arg. inv_vec arg=>x. simpl_subst.
eapply type_deref; [solve_typing..|by apply read_own_move|done|]=>x'.
iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hx Hx']".
destruct x' as [[|lx'|]|]; try iDestruct "Hx'" as "[]".
iDestruct "Hx'" as (lv lrc) "#(Hfrac & #Hshr)".
rewrite {1}/elctx_interp 2!big_sepL_cons big_sepL_singleton.
iDestruct "HE" as "([Hα1 Hα2] & Hβ & #Hαβ)".
iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". done.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iDestruct (lft_glb_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
wp_bind (!(LitV lx'))%E. iApply (wp_fupd_step with "[Hα2β]");
[done| |by iApply ("Hshr" with "[] Hα2β")|]; first done.
iMod "H↦" as "[H↦1 H↦2]". wp_read. iIntros "[#Hshr' Hα2β]!>". wp_let.
iDestruct ("Hcloseβα2" with "Hα2β") as "[Hβ Hα2]".
iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1".
iAssert (elctx_interp [ α; β; α β] qE) with "[Hα1 Hα2 Hβ Hαβ]" as "HE".
{ rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
iApply (type_letalloc_1 (&shr{α}ty) _
[ x box (uninit 1); #lv &shr{α}ty]%TC with "LFT Hna HE HL Hk");
[solve_typing..| |]; first last.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
iFrame. iApply (ty_shr_mono with "LFT [] Hshr'"). iApply lft_incl_glb; first done.
iApply lft_incl_refl. }
intros r. simpl_subst. eapply type_delete; [solve_typing..|].
eapply (type_jump [_]); solve_typing.
Qed.
(* Turning a refmut into a unique borrow. *)
Definition refmut_derefmut : val :=
funrec: <> ["x"] :=
let: "x'" := !"x" in
let: "r'" := !"x'" in
letalloc: "r" <- "r'" in
delete [ #1; "x"];; "return" ["r"].
Lemma refmut_derefmut_type ty :
typed_instruction_ty [] [] [] refmut_deref
(fn (fun '(α, β) => [α; β; α β])%EL
(fun '(α, β) => [# &uniq{α}(refmut β ty)]%T)
(fun '(α, β) => &uniq{α}ty)%T).
Proof.
apply type_fn; [apply _..|]. move=>/= [α β] ret arg. inv_vec arg=>x. simpl_subst.
eapply type_deref; [solve_typing..|by apply read_own_move|done|]=>x'.
iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hx Hx']".
rewrite {1}/elctx_interp 2!big_sepL_cons big_sepL_singleton.
iDestruct "HE" as "(Hα & Hβ & #Hαβ)".
destruct x' as [[|lx'|]|]; try iDestruct "Hx'" as "[]".
iMod (bor_exists with "LFT Hx'") as (vl) "H". done.
iMod (bor_sep with "LFT H") as "[H↦ H]". done.
destruct vl as [|[[|lv|]|][|[[|lrc|]|][]]];
try by iMod (bor_persistent_tok with "LFT H Hα") as "[>[] _]".
iMod (bor_exists with "LFT H") as (ν) "H". done.
iMod (bor_exists with "LFT H") as (γ) "H". done.
iMod (bor_exists with "LFT H") as (δ) "H". done.
iMod (bor_exists with "LFT H") as (ty') "H". done.
iMod (bor_sep with "LFT H") as "[Hb H]". done.
iMod (bor_sep with "LFT H") as "[Hβδ H]". done.
iMod (bor_persistent_tok with "LFT Hβδ Hα") as "[#Hβδ Hα]". done.
rewrite (comm _ (1).[ν])%I. rewrite (assoc _ _ _ (1).[ν])%I.
iMod (bor_sep with "LFT H") as "[_ H]". done.
iMod (bor_fracture (λ q, (1 * q).[ν])%I with "LFT [H]") as "H". done.
{ by rewrite Qp_mult_1_l. }
iDestruct (frac_bor_lft_incl _ _ 1 with "LFT H") as "#Hαν". iClear "H".
rewrite heap_mapsto_vec_cons. iMod (bor_sep with "LFT H↦") as "[H↦ _]". done.
iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]". done.
wp_bind (!(LitV lx'))%E. iApply (wp_fupd_step with "[Hb]");
[done| |by iApply (bor_unnest with "LFT Hb")|]; first done.
wp_read. iIntros "Hb !>". wp_let.
iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]".
iAssert (elctx_interp [ α; β; α β] qE) with "[Hα Hβ Hαβ]" as "HE".
{ rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
iApply (type_letalloc_1 (&uniq{α}ty) _
[ x box (uninit 1); #lv &uniq{α}ty]%TC with "LFT Hna HE HL Hk");
[solve_typing..| |]; first last.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
iFrame. iApply (bor_shorten with "[] Hb").
by iApply lft_incl_glb; [iApply lft_incl_glb|iApply lft_incl_refl]. }
intros r. simpl_subst. eapply type_delete; [solve_typing..|].
eapply (type_jump [_]); solve_typing.
Qed.
(* Dropping a refmut and set the count to 0 in the corresponding refcell. *)
Definition refmut_drop : val :=
funrec: <> ["x"] :=
let: "rc" := !("x" + #1) in
"rc" <- #0;;
Endlft;;
delete [ #2; "x"];;
let: "r" := new [ #0] in "return" ["r"].
Lemma refmut_drop_type ty :
typed_instruction_ty [] [] [] refmut_drop
(fn (fun α => [α])%EL (fun α => [# refmut α ty]) (fun α => unit)).
Proof.
apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
iIntros "!# * #LFT Hna Hα HL Hk Hx".
rewrite {1}/elctx_interp big_sepL_singleton tctx_interp_singleton tctx_hasty_val.
destruct x as [[|lx|]|]; try iDestruct "Hx" as "[]". iDestruct "Hx" as "[Hx Hx†]".
iDestruct "Hx" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Hx"; try iDestruct "Hx" as "[_ >[]]".
rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iDestruct "Hx" as "[[Hx↦1 Hx↦2] Hx]". wp_op. wp_read. wp_let.
iDestruct "Hx" as (ν γ β ty') "(Hb & #Hαβ & #Hinv & Hν & H◯)".
iMod (lft_incl_acc with "Hαβ Hα") as () "[Hβ Hcloseα]". done.
iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hcloseβ)"; [done..|].
iDestruct "INV" as (st) "(H↦lrc & H● & INV)". wp_write.
iDestruct (own_valid_2 with "H● H◯") as %[[[=]| (? & [agν st'] & [=<-] & -> &
[[Hag Heq]|[_ Hle]%prod_included])]%option_included []]%auth_valid_discrete_2;
last first.
{ by destruct (exclusive_included (Cinl (Excl ())) st'). }
setoid_subst. iDestruct "INV" as (ν') "(Hνν' & H† & _)".
iDestruct "Hνν'" as %<-%(inj to_agree)%leibniz_equiv.
wp_bind Endlft. iApply (wp_fupd_step with "[H† Hν]");
[done| |iApply ("H†" with "Hν")|]; first done.
wp_seq. iIntros "{Hb} Hb !>".
iMod ("Hcloseβ" with ">[H↦lrc H● H◯ Hb] Hna") as "[Hβ Hna]".
{ iExists None. iFrame. iMod (own_update_2 with "H● H◯") as "$"; last done.
apply auth_update_dealloc. rewrite -(right_id None _ (Some _)).
apply op_local_update_cancellable_empty, _. }
iMod ("Hcloseα" with "Hβ") as "Hα". wp_seq.
iAssert (elctx_interp [ α] qE) with "[Hα]" as "HE".
{ by rewrite /elctx_interp big_sepL_singleton. }
iApply (type_delete _ _ [ #lx box (uninit 2)]%TC with "LFT Hna HE HL Hk");
[solve_typing..| |]; first last.
{ rewrite tctx_interp_singleton tctx_hasty_val' //. iFrame. iExists [ #lv;#lrc].
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton uninit_own. iFrame. auto. }
eapply type_new; [solve_typing..|]=>r. simpl_subst.
eapply (type_jump [_]); solve_typing.
Qed.
End refmut_functions.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment