diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index be7d944a05055c28ce94f77ad80de5b091b07453..f4e850ad4c511d2c1fe1564d32db8659ffb2a7a1 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -37,32 +37,20 @@ Definition upgrade : val :=
else "upgrade" ["l"].
Definition drop_weak : val :=
- rec: "drop" ["l"; "dealloc"] :=
+ rec: "drop" ["l"] :=
let: "weak" := !ˢᶜ("l" +ₗ #1) in
- if: CAS ("l" +â‚— #1) "weak" ("weak" - #1) then
- if: "weak" = #1 then "dealloc" [] else #()
- else "drop" ["l"; "dealloc"].
+ if: CAS ("l" +â‚— #1) "weak" ("weak" - #1) then "weak" = #1
+ else "drop" ["l"].
Definition drop_arc : val :=
- rec: "drop_arc" ["l"; "drop"; "dealloc"] :=
+ rec: "drop" ["l"] :=
let: "strong" := !ˢᶜ"l" in
- if: CAS "l" "strong" ("strong" - #1) then
- if: "strong" = #1 then
- "drop" [];;
- drop_weak ["l"; "dealloc"]
- else #()
- else "drop_arc" ["l"; "drop"; "dealloc"].
+ if: CAS "l" "strong" ("strong" - #1) then "strong" = #1
+ else "drop" ["l"].
Definition try_unwrap : val :=
λ: ["l"], CAS "l" #1 #0.
-Definition try_unwrap_full : val :=
- λ: ["l"],
- if: CAS "l" #1 #0 then
- if: !ˢᶜ("l" +ₗ #1) = #1 then #0
- else "l" <- #1;; #1
- else #2.
-
Definition is_unique : val :=
λ: ["l"],
if: CAS ("l" +â‚— #1) #1 #(-1) then
@@ -73,6 +61,13 @@ Definition is_unique : val :=
else
#false.
+Definition try_unwrap_full : val :=
+ λ: ["l"],
+ if: CAS "l" #1 #0 then
+ if: !ˢᶜ("l" +ₗ #1) = #1 then "l" <- #1;; #0
+ else #1
+ else #2.
+
(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
@@ -124,10 +119,6 @@ Section def.
Definition weak_tok_acc (γ : gname) P E : iProp Σ :=
(□ (P ={E,∅}=∗ weak_tok γ ∗ (weak_tok γ ={∅,E}=∗ P)))%I.
- Definition dealloc_spec l (dealloc : val) P : iProp Σ :=
- ({{{ P ∗ l ↦ #0 ∗ shift_loc l 1 ↦ #0 ∗ P2}}} dealloc []
- {{{ RET #(); P }}})%I.
-
Definition drop_spec (drop : val) P : iProp Σ :=
({{{ P ∗ P1 1 }}} drop [] {{{ RET #(); P ∗ P2 }}})%I.
End def.
@@ -221,12 +212,12 @@ Section arc.
iMod ("Hclose1" with "[Hl Hw Hâ— HP1']") as "_".
{ iExists _. iFrame. iExists _. rewrite /= [xH â‹… _]comm_L. iFrame.
rewrite [(q / 2)%Qp â‹… _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2 left_id_L. auto. }
- iModIntro. wp_apply (wp_if _ true). wp_value. iApply "HΦ". iFrame.
+ iModIntro. wp_case. iApply "HΦ". iFrame.
- wp_apply (wp_cas_int_fail with "Hl"); [done|congruence|]. iIntros "Hl".
iMod ("Hclose2" with "Hown") as "HP". iModIntro.
iMod ("Hclose1" with "[-HP HΦ]") as "_".
{ iExists _. iFrame. iExists q. auto with iFrame. }
- iModIntro. wp_apply (wp_if _ false). iApply ("IH" with "HP HΦ").
+ iModIntro. wp_case. iApply ("IH" with "HP HΦ").
Qed.
Lemma downgrade_spec (γ : gname) (l : loc) (P : iProp Σ) :
@@ -257,18 +248,18 @@ Section arc.
iMod ("Hclose1" with "[-Hown' HP HΦ]") as "_".
{ iExists _. iFrame. iExists _.
rewrite Z.add_comm (Nat2Z.inj_add 1). auto with iFrame. }
- iModIntro. wp_apply (wp_if _ true). wp_value. iApply "HΦ". iFrame.
+ iModIntro. wp_case. iApply "HΦ". iFrame.
- destruct wlock.
+ iDestruct "Hl1" as "[Hl1 >%]". subst.
wp_apply (wp_cas_int_fail with "Hl1"); [done..|].
iIntros "Hl1". iMod ("Hclose1" with "[-HP HΦ]") as "_".
{ iExists _. auto with iFrame. }
- iModIntro. wp_apply (wp_if _ false). iApply ("IH" with "HP HΦ").
+ iModIntro. wp_case. iApply ("IH" with "HP HΦ").
+ wp_apply (wp_cas_int_fail with "Hl1"); [done| |].
{ contradict Hw. split=>//. apply SuccNat2Pos.inj. lia. }
iIntros "Hl1". iMod ("Hclose1" with "[-HP HΦ]") as "_".
{ iExists _. auto with iFrame. }
- iModIntro. wp_apply (wp_if _ false). iApply ("IH" with "HP HΦ").
+ iModIntro. wp_case. iApply ("IH" with "HP HΦ").
Qed.
Lemma weak_tok_auth_val γ st :
@@ -321,10 +312,10 @@ Section arc.
destruct (decide (w = w')) as [<-|].
- wp_apply (wp_cas_int_suc with "H↦"); first done. iIntros "H↦".
iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "H↦"). iModIntro.
- wp_apply (wp_if _ true). wp_value. by iApply "HΦ".
+ wp_case. by iApply "HΦ".
- wp_apply (wp_cas_int_fail with "H↦"); try done. iIntros "H↦".
iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "H↦") as "Hown".
- iModIntro. wp_apply (wp_if _ false). by iApply ("IH" with "Hown").
+ iModIntro. wp_case. by iApply ("IH" with "Hown").
Qed.
Lemma upgrade_spec (γ : gname) (l : loc) (P : iProp Σ) :
@@ -368,18 +359,18 @@ Section arc.
+ wp_apply (wp_cas_int_suc with "H↦"); first done. iIntros "H↦".
iDestruct "Hclose" as "[Hclose _]".
iMod ("Hclose" with "[//] H↦") as (q) "(?&?&?)". iModIntro.
- wp_apply (wp_if _ true). wp_value. iApply "HΦ". iFrame.
+ wp_case. iApply "HΦ". iFrame.
+ wp_apply (wp_cas_int_fail with "H↦"); try done. iIntros "H↦".
iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "H↦") as "Hown".
- iModIntro. wp_apply (wp_if _ false). by iApply ("IH" with "Hown").
+ iModIntro. wp_case. by iApply ("IH" with "Hown").
Qed.
- Lemma drop_weak_spec (dealloc : val) (γ : gname) (l : loc) P :
- is_arc P1 P2 N γ l -∗ dealloc_spec P2 l dealloc P -∗
- {{{ P ∗ weak_tok γ }}} drop_weak [ #l; dealloc] {{{ RET #() ; P }}}.
+ Lemma drop_weak_spec (γ : gname) (l : loc) :
+ is_arc P1 P2 N γ l -∗
+ {{{ weak_tok γ }}} drop_weak [ #l]
+ {{{ (b : bool), RET #b ; if b then P2 ∗ l ↦ #0 ∗ shift_loc l 1 ↦ #0 else True }}}.
Proof.
- iIntros "#INV #Hdealloc !# * [HP Hown] HΦ". iLöb as "IH". wp_rec. wp_op.
- wp_bind (!ˢᶜ_)%E.
+ iIntros "#INV !# * Hown HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
iAssert (□ (weak_tok γ ={⊤,⊤ ∖ ↑N}=∗ ∃ w : Z, shift_loc l 1 ↦ #w ∗
(shift_loc l 1 ↦ #(w - 1) ={⊤ ∖ ↑N,⊤}=∗ ⌜w ≠1⌠∨
▷ P2 ∗ l ↦ #0 ∗ shift_loc l 1 ↦ #0) ∧
@@ -418,26 +409,39 @@ Section arc.
iMod ("Hproto" with "Hown") as (w') "[Hw Hclose]". destruct (decide (w = w')) as [<-|?].
- wp_apply (wp_cas_int_suc with "Hw"); first done. iIntros "Hw".
iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hw") as "HP2". iModIntro.
- wp_apply (wp_if _ true). wp_op=>[->|?]; wp_if; last by iApply "HΦ".
- iDestruct "HP2" as "[%|(? & ? & ? )]"; first done.
- iApply ("Hdealloc" with "[-HΦ]"); iFrame.
+ wp_case. wp_op=>[->|?]; iApply "HΦ"=>//.
+ by iDestruct "HP2" as "[%|$]".
- wp_apply (wp_cas_int_fail with "Hw"); try done. iIntros "Hw".
- iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hw") as "Hown". iModIntro.
- wp_apply (wp_if _ false). by iApply ("IH" with "HP Hown").
+ iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hw") as "Hown".
+ iModIntro. wp_case. by iApply ("IH" with "Hown").
+ Qed.
+
+ Lemma close_last_strong γ l :
+ is_arc P1 P2 N γ l -∗ own γ (◯ (Some (Cinr (Excl ())), 0%nat)) -∗ P2
+ ={⊤}=∗ weak_tok γ.
+ Proof.
+ iIntros "INV Hâ—¯ HP2". iInv N as ([st ?]) "[>Hâ— H]" "Hclose".
+ iDestruct (own_valid_2 with "Hâ— Hâ—¯")
+ as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_valid_discrete_2.
+ simpl in Hincl. destruct Hincl as (?&?&[=<-]&->&[?|[]%exclusive_included]);
+ try done; try apply _. setoid_subst.
+ iMod (own_update_2 with "Hâ— Hâ—¯") as "[Hâ— $]".
+ { apply auth_update, prod_local_update', (op_local_update _ _ 1%nat)=>//.
+ apply delete_option_local_update, _. }
+ iApply "Hclose". iExists _. by iFrame.
Qed.
- Lemma drop_arc_spec (drop dealloc : val) (γ : gname) (q: Qp) (l : loc) P :
- is_arc P1 P2 N γ l -∗ drop_spec P1 P2 drop P -∗ dealloc_spec P2 l dealloc P -∗
- {{{ P ∗ arc_tok γ q ∗ P1 q }}} drop_arc [ #l; drop; dealloc]
- {{{ RET #() ; P }}}.
+ Lemma drop_arc_spec (γ : gname) (q: Qp) (l : loc) :
+ is_arc P1 P2 N γ l -∗
+ {{{ arc_tok γ q ∗ P1 q }}} drop_arc [ #l]
+ {{{ (b : bool), RET #b ; if b then P1 1 ∗ (P2 ={⊤}=∗ weak_tok γ) else True }}}.
Proof using HP1.
- iIntros "#INV #Hdrop #Hdealloc !# * (HP & Hown & HP1) HΦ". iLöb as "IH".
+ iIntros "#INV !# * [Hown HP1] HΦ". iLöb as "IH".
wp_rec. wp_bind (!ˢᶜ_)%E. iInv N as (st) "[>H◠H]" "Hclose".
iDestruct (arc_tok_auth_val with "Hâ— Hown") as %(?& s &?&?&[-> _]).
iDestruct "H" as (?) "(? & ? & ? & ?)". wp_read.
- iMod ("Hclose" with "[-HP Hown HP1 HΦ]") as "_". { iExists _. auto with iFrame. }
- iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _).
- iInv N as (st) "[>Hâ— H]" "Hclose".
+ iMod ("Hclose" with "[-Hown HP1 HΦ]") as "_". { iExists _. auto with iFrame. }
+ iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _). iInv N as (st) "[>Hâ— H]" "Hclose".
iDestruct (arc_tok_auth_val with "Hâ— Hown") as %(q' & s' & wl & w &[-> Hqq']).
iDestruct "H" as (q'') "(>Hq'' & HP1' & Hs & Hw)". iDestruct "Hq''" as %Hq''.
destruct (decide (s = s')) as [<-|?].
@@ -449,32 +453,21 @@ Section arc.
etrans; first apply cancel_local_update_empty, _.
by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
iMod ("Hclose" with "[Hâ— Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
- iModIntro. wp_apply (wp_if _ true). wp_op=>[_|//]; wp_if.
- rewrite -{1}Hq''. wp_apply ("Hdrop" with "[$HP1 $HP1' $HP]"). iIntros "[HP HP2]".
- wp_seq. iApply (drop_weak_spec with "INV Hdealloc [> -HΦ] HΦ").
- iInv N as ([st ?]) "[>Hâ— H]" "Hclose".
- iDestruct (own_valid_2 with "Hâ— Hâ—¯")
- as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_valid_discrete_2.
- simpl in Hincl. destruct Hincl as (?&?&[=<-]&->&[?|[]%exclusive_included]);
- try done; try apply _. setoid_subst.
- iMod (own_update_2 with "Hâ— Hâ—¯") as "[Hâ— $]".
- { apply auth_update, prod_local_update', (op_local_update _ _ 1%nat)=>//.
- apply delete_option_local_update, _. }
- iFrame. iApply "Hclose". iExists _. by iFrame.
+ iModIntro. wp_case. iApply wp_fupd. wp_op=>[_|//].
+ iApply ("HΦ"). rewrite -{2}Hq''. iFrame. by iApply close_last_strong.
+ destruct Hqq' as [? ->].
rewrite -[in (_, _)](Pos.succ_pred s) // -[wl in Cinl (_, wl)]left_id
-Pos.add_1_l -2!pair_op -Cinl_op Some_op.
iMod (own_update_2 _ _ _ _ with "Hâ— Hown") as "Hâ—".
{ apply auth_update_dealloc, prod_local_update_1, @cancel_local_update_empty, _. }
- iMod ("Hclose" with "[- HΦ HP]") as "_".
+ iMod ("Hclose" with "[- HΦ]") as "_".
{ iExists _. iFrame. iExists (q + q'')%Qp. iFrame. iSplit; last by destruct s.
iIntros "!> !%". rewrite assoc -Hq''. f_equal. apply comm, _. }
- iModIntro. wp_apply (wp_if _ true). wp_op. by intros [=->]. intros _.
- wp_if. by iApply "HΦ".
+ iModIntro. wp_case. wp_op=>[|_]. by intros [=->]. by iApply "HΦ".
- wp_apply (wp_cas_int_fail with "Hs"); [done|congruence|]. iIntros "Hs".
- iSpecialize ("IH" with "HP Hown HP1 HΦ").
+ iSpecialize ("IH" with "Hown HP1 HΦ").
iMod ("Hclose" with "[- IH]") as "_"; first by iExists _; auto with iFrame.
- by iApply (wp_if _ false).
+ iModIntro. by wp_case.
Qed.
Lemma try_unwrap_spec (γ : gname) (q: Qp) (l : loc) :
@@ -493,16 +486,7 @@ Section arc.
etrans; first apply cancel_local_update_empty, _.
by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
iMod ("Hclose" with "[Hâ— Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
- iApply ("HΦ" $! true). rewrite -{1}Hq''. iFrame. iIntros "!> HP2".
- iInv N as ([st ?]) "[>Hâ— H]" "Hclose".
- iDestruct (own_valid_2 with "Hâ— Hâ—¯")
- as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_valid_discrete_2.
- simpl in Hincl. destruct Hincl as (?&?&[=<-]&->&[?|[]%exclusive_included]);
- try done; try apply _. setoid_subst.
- iMod (own_update_2 with "Hâ— Hâ—¯") as "[Hâ— $]".
- { apply auth_update, prod_local_update', (op_local_update _ _ 1%nat)=>//.
- apply delete_option_local_update, _. }
- iApply "Hclose". iExists _. by iFrame.
+ iApply ("HΦ" $! true). rewrite -{1}Hq''. iFrame. by iApply close_last_strong.
- wp_apply (wp_cas_int_fail with "Hs"); [done|congruence|]. iIntros "Hs".
iMod ("Hclose" with "[-Hown HP1 HΦ]") as "_"; first by iExists _; auto with iFrame.
iApply ("HΦ" $! false). by iFrame.
@@ -523,18 +507,17 @@ Section arc.
- iDestruct "Hw" as "[Hw %]". subst.
iApply (wp_cas_int_fail with "Hw")=>//. iNext. iIntros "Hw".
iMod ("Hclose" with "[-HΦ Hown HP1]") as "_"; first by iExists _; eauto with iFrame.
- iModIntro. iApply (wp_if _ false). iModIntro. wp_value. iApply "HΦ". iFrame.
+ iModIntro. wp_case. iApply "HΦ". iFrame.
- iApply (wp_cas_int_fail with "Hw"); [done|lia|]. iNext. iIntros "Hw".
iMod ("Hclose" with "[-HΦ Hown HP1]") as "_"; first by iExists _; eauto with iFrame.
- iModIntro. iApply (wp_if _ false). iModIntro. wp_value. iApply "HΦ". iFrame.
+ iModIntro. wp_case. iApply "HΦ". iFrame.
- iApply (wp_cas_int_suc with "Hw")=>//. iNext. iIntros "Hw".
iMod (own_update_2 with "Hâ— Hown") as "[Hâ— Hâ—¯]".
{ by apply auth_update, prod_local_update_1, option_local_update,
csum_local_update_l, prod_local_update_2,
(alloc_option_local_update (Excl ())). }
iMod ("Hclose" with "[-HΦ HP1 H◯]") as "_"; first by iExists _; eauto with iFrame.
- iModIntro. iApply (wp_if _ true). iNext. wp_bind (!ˢᶜ_)%E.
- iInv N as ([st ?]) "[>Hâ— H]" "Hclose".
+ iModIntro. wp_case. wp_bind (!ˢᶜ_)%E. iInv N as ([st ?]) "[>H◠H]" "Hclose".
iDestruct (own_valid_2 with "Hâ— Hâ—¯") as
%[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_valid_discrete_2.
simpl in Hincl. destruct Hincl as (? & ? & [=<-] & -> & [|Hincl]); last first.
@@ -568,6 +551,52 @@ Section arc.
iModIntro. wp_seq. wp_op=>[_|//]. wp_let. wp_op. wp_write. iApply "HΦ".
iDestruct "Hq" as %<-. iFrame.
Qed.
+
+ Lemma try_unwrap_full_spec (γ : gname) (q: Qp) (l : loc) :
+ is_arc P1 P2 N γ l -∗
+ {{{ arc_tok γ q ∗ P1 q }}} try_unwrap_full [ #l]
+ {{{ (x : fin 3), RET #x ;
+ match x : nat with
+ (* No other reference : we get everything. *)
+ | 0%nat => l ↦ #1 ∗ shift_loc l 1 ↦ #1 ∗ P1 1
+ (* No other strong, but there are weaks : we get P1,
+ plus the option to get a weak if we pay P1. *)
+ | 1%nat => P1 1 ∗ (P2 ={⊤}=∗ weak_tok γ)
+ (* There are other strong : we get back what we gave at the first place. *)
+ | _ (* 2 *) => arc_tok γ q ∗ P1 q
+ end }}}.
+ Proof using HP1.
+ iIntros "#INV !# * [Hown HP1] HΦ". wp_rec. wp_bind (CAS _ _ _).
+ iInv N as (st) "[>Hâ— H]" "Hclose".
+ iDestruct (arc_tok_auth_val with "Hâ— Hown") as %(q' & s & wl & w &[-> Hqq']).
+ iDestruct "H" as (q'') "(>Hq'' & HP1' & Hs & Hw)". iDestruct "Hq''" as %Hq''.
+ destruct (decide (s = xH)) as [->|?].
+ - wp_apply (wp_cas_int_suc with "Hs")=>//. iIntros "Hs".
+ destruct Hqq' as [<- ->]. iMod (own_update_2 with "Hâ— Hown") as "[Hâ— Hâ—¯]".
+ { apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
+ etrans; first apply cancel_local_update_empty, _.
+ by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
+ iCombine "HP1" "HP1'" as "HP1". rewrite Hq''. clear Hq'' q''.
+ iMod ("Hclose" with "[Hâ— Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
+ clear w. iModIntro. wp_case. wp_op. wp_bind (!ˢᶜ_)%E.
+ iInv N as ([st w']) "[>Hâ— H]" "Hclose".
+ iDestruct (own_valid_2 with "Hâ— Hâ—¯")
+ as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_valid_discrete_2.
+ simpl in Hincl. destruct Hincl as (?&?&[=<-]&->&[?|[]%exclusive_included]);
+ [|by apply _|done]. setoid_subst. iDestruct "H" as "[Hl Hl1]".
+ wp_read. destruct w'.
+ + iMod (own_update_2 with "Hâ— Hâ—¯") as "Hâ—".
+ { apply auth_update_dealloc, prod_local_update_1,
+ delete_option_local_update, _. }
+ iMod ("Hclose" with "[Hâ—]") as "_"; first by iExists _; iFrame. iModIntro.
+ wp_op=>[_|//]. wp_if. wp_write. iApply ("HΦ" $! 0%fin). iFrame.
+ + iMod ("Hclose" with "[Hâ— Hl Hl1]") as "_"; first by iExists _; do 2 iFrame.
+ iModIntro. wp_op; [lia|intros _]. wp_if. iApply ("HΦ" $! 1%fin). iFrame.
+ by iApply close_last_strong.
+ - wp_apply (wp_cas_int_fail with "Hs"); [done|congruence|]. iIntros "Hs".
+ iMod ("Hclose" with "[Hâ— Hs Hw HP1']") as "_"; first by iExists _; auto with iFrame.
+ iModIntro. wp_case. iApply ("HΦ" $! 2%fin). iFrame.
+ Qed.
End arc.
Typeclasses Opaque is_arc arc_tok weak_tok.
\ No newline at end of file
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index 10cbd72913d817e0de7010b6788bb37f386ef456..2b47b30c6efa250573df3f2f3b1d8b54f39dcfa7 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -22,6 +22,7 @@ Ltac wp_done :=
| |- language.to_val _ = Some _ => solve_to_val
| |- Forall _ [] => fast_by apply List.Forall_nil
| |- Forall _ (_ :: _) => apply List.Forall_cons; wp_done
+ | |- _ ≤ _ => lia
| _ => fast_done
end.
@@ -119,7 +120,7 @@ Tactic Notation "wp_case" :=
lazymatch goal with
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
- | Case _ _ _ =>
+ | Case _ _ =>
wp_bind_core K;
etrans; [|eapply wp_case; wp_done];
simpl_subst; wp_finish
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 98a939c1a034eaf6fcc50d7f124f654b04e829e8..579d513cabb4e29c715aba0e9f9caf2145a698aa 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -8,7 +8,7 @@ From lrust.typing Require Export type.
From lrust.typing Require Import typing option.
Set Default Proof Using "Type".
-(* TODO : get_mut make_mut weak_count strong_count *)
+(* TODO : make_mut weak_count strong_count *)
Definition arcN := lrustN .@ "arc".
Definition arc_invN := arcN .@ "inv".
@@ -649,9 +649,12 @@ Section arc.
let: "r" := new [ #(option ty).(ty_size) ] in
let: "arc'" := !"arc" in
"r" <-{Σ none} ();;
- drop_arc ["arc'";
- λ: [], "r" <-{ty.(ty_size),Σ some} !("arc'" +ₗ #2);
- λ: [], delete [ #(2 + ty.(ty_size)); "arc'" ]];;
+ (if: drop_arc ["arc'"] then
+ "r" <-{ty.(ty_size),Σ some} !("arc'" +ₗ #2);;
+ if: drop_weak ["arc'"] then
+ delete [ #(2 + ty.(ty_size)); "arc'" ]
+ else #()
+ else #());;
delete [ #1; "arc"];; return: ["r"].
Lemma arc_drop_type ty `{!TyWf ty} :
@@ -667,29 +670,35 @@ Section arc.
iAssert (shared_arc_own rc' ty tid)%I with "[>Hrc']" as "Hrc'".
{ iDestruct "Hrc'" as "[?|$]"; last done. iApply arc_own_share; solve_ndisj. }
iDestruct "Hrc'" as (γ ν q) "(#Hpersist & Htok & Hν)".
- wp_bind (drop_arc _). erewrite <-2!(of_to_val (λ: [], _)%E); [|solve_to_val..].
- iApply (drop_arc_spec with "[] [] [] [Hν Hr Htok]");
- [by iDestruct "Hpersist" as "[$?]"| | |by iSplitL "Hr"; [iApply "Hr"|iFrame]|].
- { iIntros "/= !# * [Hr Hν] HΦ". unlock. destruct r as [[]|]=>//=. wp_lam.
+ wp_bind (drop_arc _). iApply (drop_arc_spec with "[] [$Htok Hν]");
+ [by iDestruct "Hpersist" as "[$?]"|done|].
+ iNext. iIntros (b) "Hdrop". wp_bind (if: _ then _ else _)%E.
+ iApply (wp_wand _ _ (λ _, ty_own (box (option ty)) tid [r])%I with "[Hdrop Hr]").
+ { unlock. destruct b; wp_if=>//. destruct r as [[]|]=>//=.
iDestruct "Hr" as "[Hr ?]". iDestruct "Hr" as ([|d vl]) "[H↦ Hown]";
- first by iDestruct "Hown" as (???) "[% ?]".
+ first by iDestruct "Hown" as (???) "[>% ?]".
rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦1]".
iDestruct "Hpersist" as "(? & ? & H†)". wp_bind (_ <- _)%E.
- iSpecialize ("H†" with "Hν").
+ iDestruct "Hdrop" as "[Hν Hdrop]". iSpecialize ("H†" with "Hν").
iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); try solve_ndisj.
iDestruct "Hown" as (???) "(_ & Hlen & _)". wp_write. iIntros "(#Hν & Hown & H†)!>".
wp_seq. wp_op. wp_op. iDestruct "Hown" as (?) "[H↦ Hown]".
iDestruct (ty_size_eq with "Hown") as %?. rewrite Max.max_0_r.
iDestruct "Hlen" as %[= ?]. iApply (wp_memcpy with "[$H↦1 $H↦]"); [congruence..|].
- iNext. iIntros "[? Hrc']". iApply "HΦ". iFrame. iSplitR "Hrc'"; last by eauto.
- iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. iExists 1%nat, _, [].
- iFrame. rewrite app_nil_r. iSplit; first by auto. rewrite /= Max.max_0_r. auto. }
- { iIntros "/= !# * [Hr [H↦0 [H↦1 [H†H]]]] HΦ". wp_lam.
- iDestruct "H" as (vl) "[H↦ Heq]". iDestruct "Heq" as %Heq. rewrite -Heq.
- iApply (wp_delete _ _ _ (_::_::vl) with "[H↦0 H↦1 H↦ H†]");
- [simpl; lia| |iIntros "!> _"; by iApply "HΦ"].
- rewrite !heap_mapsto_vec_cons shift_loc_assoc. auto with iFrame. }
- iIntros "!> Hr". wp_seq.
+ iNext. iIntros "[? Hrc']". wp_seq. iMod ("Hdrop" with "[Hrc' H†]") as "Htok".
+ { unfold P2. auto with iFrame. }
+ wp_apply (drop_weak_spec with "[//] Htok"). iIntros ([]); last first.
+ { iIntros "_". wp_if. iFrame. iExists (_::_). rewrite heap_mapsto_vec_cons.
+ iFrame. iExists 1%nat, _, []. rewrite /= right_id_L Max.max_0_r.
+ auto 10 with iFrame. }
+ iIntros "([H†H1] & H2 & H3)". iDestruct "H1" as (vl') "[H1 Heq]".
+ iDestruct "Heq" as %<-. wp_if.
+ wp_apply (wp_delete _ _ _ (_::_::vl') with "[H1 H2 H3 H†]"). lia.
+ { rewrite 2!heap_mapsto_vec_cons shift_loc_assoc. auto with iFrame. }
+ iFrame. iIntros "_". iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame.
+ iExists 1%nat, _, []. rewrite right_id_L. iFrame. iSplit; [by auto|simpl].
+ auto with lia. }
+ iIntros (?) "Hr". wp_seq.
(* Finish up the proof. *)
iApply (type_type _ _ _ [ rcx â— box (uninit 1); r â— box (option ty) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
@@ -703,7 +712,8 @@ Section arc.
funrec: <> ["arc"] :=
let: "r" := new [ #0] in
let: "arc'" := !"arc" in
- drop_weak ["arc'"; λ: [], delete [ #(2 + ty.(ty_size)); "arc'" ]];;
+ (if: drop_weak ["arc'"] then delete [ #(2 + ty.(ty_size)); "arc'" ]
+ else #());;
delete [ #1; "arc"];; return: ["r"].
Lemma weak_drop_type ty `{!TyWf ty} :
@@ -716,15 +726,14 @@ Section arc.
iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock. destruct rc' as [[|rc'|]|]=>//=.
iDestruct "Hrc'" as (γ ν) "[#Hpersist Htok]". wp_bind (drop_weak _).
- erewrite <-(of_to_val (λ: [], _)%E); [|solve_to_val..].
- iApply (drop_weak_spec _ _ _ _ _ _ True with "[] [] [Htok]");
- [by iDestruct "Hpersist" as "[$?]"| |by auto|].
- { iIntros "/= !# * [_ [H↦0 [H↦1 [H†H]]]] HΦ". wp_lam.
- iDestruct "H" as (vl) "[H↦ Heq]". iDestruct "Heq" as %Heq. rewrite -Heq.
- iApply (wp_delete _ _ _ (_::_::vl) with "[H↦0 H↦1 H↦ H†]");
- [simpl; lia| |iIntros "!> _"; by iApply "HΦ"].
- rewrite !heap_mapsto_vec_cons shift_loc_assoc. auto with iFrame. }
- iIntros "!> _". wp_seq.
+ iApply (drop_weak_spec with "[] [Htok]"); [by iDestruct "Hpersist" as "[$?]"|by auto|].
+ iIntros "!> * Hdrop". wp_bind (if: _ then _ else _)%E.
+ iApply (wp_wand _ _ (λ _, True)%I with "[Hdrop]").
+ { destruct b; wp_if=>//. iDestruct "Hdrop" as "((? & H↦) & ? & ?)".
+ iDestruct "H↦" as (vl) "[? Heq]". iDestruct "Heq" as %<-.
+ wp_apply (wp_delete _ _ _ (_::_::vl) with "[-]"); [lia| |done].
+ rewrite !heap_mapsto_vec_cons shift_loc_assoc. iFrame. auto. }
+ iIntros (?) "_". wp_seq.
(* Finish up the proof. *)
iApply (type_type _ _ _ [ rcx â— box (uninit 1); r â— box unit ]
with "[] LFT HE Hna HL Hk [-]"); last first.
@@ -743,7 +752,8 @@ Section arc.
(* Return content *)
"r" <-{ty.(ty_size),Σ 0} !("arc'" +ₗ #2);;
(* Decrement the "strong weak reference" *)
- drop_weak ["arc'"; λ: [], delete [ #(2 + ty.(ty_size)); "arc'" ]];;
+ (if: drop_weak ["arc'"] then delete [ #(2 + ty.(ty_size)); "arc'" ]
+ else #());;
delete [ #1; "arc"];; return: ["r"]
else
"r" <-{Σ 1} "arc'";;
@@ -780,14 +790,14 @@ Section arc.
iApply (wp_memcpy with "[$Hr1 $Hrc']"); rewrite ?firstn_length_le; try lia.
iIntros "!> [Hr1 Hrc']". wp_seq. wp_bind (drop_weak _).
iMod ("Hend" with "[$H†Hrc']") as "Htok"; first by eauto.
- erewrite <-(of_to_val (λ: [], _)%E); [|solve_to_val..].
- iApply (drop_weak_spec _ _ _ _ _ _ True with "Ha [] [Htok]"); [|by auto|].
- { iIntros "/= !# * [_ [H↦0 [H↦1 [H†H]]]] HΦ". wp_lam.
- iDestruct "H" as (vl1) "[H↦ Heq]". iDestruct "Heq" as %Heq. rewrite -Heq.
- iApply (wp_delete _ _ _ (_::_::vl1) with "[H↦0 H↦1 H↦ H†]");
- [simpl; lia| |iIntros "!> _"; by iApply "HΦ"].
- rewrite !heap_mapsto_vec_cons shift_loc_assoc. auto with iFrame. }
- iIntros "!> _". wp_seq.
+ iApply (drop_weak_spec with "Ha Htok").
+ iIntros "!> * Hdrop". wp_bind (if: _ then _ else _)%E.
+ iApply (wp_wand _ _ (λ _, True)%I with "[Hdrop]").
+ { destruct b; wp_if=>//. iDestruct "Hdrop" as "((? & H↦) & ? & ?)".
+ iDestruct "H↦" as (vl') "[? Heq]". iDestruct "Heq" as %<-.
+ wp_apply (wp_delete _ _ _ (_::_::vl') with "[-]"); [lia| |done].
+ rewrite !heap_mapsto_vec_cons shift_loc_assoc. iFrame. auto. }
+ iIntros (?) "_". wp_seq.
iApply (type_type _ _ _ [ rcx ◠box (uninit 1); #r ◠box (Σ[ ty; arc ty ]) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock.
@@ -807,4 +817,245 @@ Section arc.
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
+
+ Definition arc_get_mut : val :=
+ funrec: <> ["arc"] :=
+ let: "r" := new [ #2 ] in
+ let: "arc'" := !"arc" in
+ let: "arc''" := !"arc'" in
+ if: is_unique ["arc''"] then
+ Skip;;
+ (* Return content *)
+ "r" <-{Σ some} "arc''" +ₗ #2;;
+ delete [ #1; "arc"];; return: ["r"]
+ else
+ "r" <-{Σ none} ();;
+ delete [ #1; "arc"];; return: ["r"].
+
+ Lemma arc_get_mut_type ty `{!TyWf ty} :
+ typed_val arc_get_mut (fn(∀ α, ∅; &uniq{α} arc ty) → option (&uniq{α}ty)).
+ Proof.
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (α Ï ret arg). inv_vec arg=>rcx. simpl_subst.
+ iApply (type_new 2); [solve_typing..|]; iIntros (r); simpl_subst.
+ iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+ iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
+ rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock. destruct rc' as [[|rc'|]|]=>//=.
+ iMod (lctx_lft_alive_tok α with "HE HL") as (q) "(Hα & HL & Hclose1)";
+ [solve_typing..|].
+ iMod (bor_exists with "LFT Hrc'") as (rcvl) "Hrc'"=>//.
+ iMod (bor_sep with "LFT Hrc'") as "[Hrc'↦ Hrc]"=>//.
+ destruct rcvl as [|[[|rc|]|][|]]; try by
+ iMod (bor_persistent_tok with "LFT Hrc Hα") as "[>[] ?]".
+ rewrite heap_mapsto_vec_singleton.
+ iMod (bor_acc with "LFT Hrc'↦ Hα") as "[Hrc'↦ Hclose2]"=>//. wp_read.
+ iMod ("Hclose2" with "Hrc'↦") as "[_ Hα]".
+ iMod (bor_acc_cons with "LFT Hrc Hα") as "[Hrc Hclose2]"=>//. wp_let.
+ iAssert (shared_arc_own rc ty tid)%I with "[>Hrc]" as "Hrc".
+ { iDestruct "Hrc" as "[Hrc|$]"=>//. by iApply arc_own_share. }
+ iDestruct "Hrc" as (γ ν q') "[#(Hi & Hs & #Hc) Htoks]".
+ wp_apply (is_unique_spec with "Hi Htoks"). iIntros ([]) "H"; wp_if.
+ - iDestruct "H" as "(Hrc & Hrc1 & Hν)". iSpecialize ("Hc" with "Hν"). wp_bind Skip.
+ iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); try solve_ndisj.
+ wp_seq. iIntros "(#Hν & Hown & H†) !>". wp_seq.
+ iMod ("Hclose2" with "[Hrc Hrc1 H†] Hown") as "[Hb Hα]".
+ { iIntros "!> Hown !>". iLeft. iFrame. }
+ iMod ("Hclose1" with "Hα HL") as "HL".
+ iApply (type_type _ _ _ [ rcx ◠box (uninit 1); #rc +ₗ #2 ◠&uniq{α}ty;
+ r â— box (uninit 2) ]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
+ tctx_hasty_val' //. unlock. iFrame. }
+ iApply (type_sum_assign (option (&uniq{α}ty))); [solve_typing..|].
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing.
+ - iMod ("Hclose2" with "[] [H]") as "[_ Hα]";
+ [by iIntros "!> H"; iRight; iApply "H"|iExists _, _, _; iFrame "∗#"|].
+ iMod ("Hclose1" with "Hα HL") as "HL".
+ iApply (type_type _ _ _ [ rcx â— box (uninit 1); r â— box (uninit 2) ]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. unlock. iFrame. }
+ iApply (type_sum_unit (option (&uniq{α}ty))); [solve_typing..|].
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing.
+ Qed.
+
+ Definition arc_make_mut (ty : type) (clone : val) : val :=
+ funrec: <> ["arc"] :=
+ let: "r" := new [ #1 ] in
+ let: "arc'" := !"arc" in
+ let: "arc''" := !"arc'" in
+ (case: try_unwrap_full ["arc''"] of
+ [ "r" <- "arc''" +â‚— #2;;
+ delete [ #1; "arc"];; return: ["r"];
+
+ let: "rcbox" := new [ #(2 + ty.(ty_size))%nat ] in
+ "rcbox" +â‚— #0 <- #1;;
+ "rcbox" +â‚— #1 <- #1;;
+ "rcbox" +â‚— #2 <-{ty.(ty_size)} !"arc''" +â‚— #2;;
+ "arc'" <- "rcbox";;
+ "r" <- "rcbox" +â‚— #2;;
+ delete [ #1; "arc"];; return: ["r"];
+
+ letalloc: "x" <- "arc''" +â‚— #2 in
+ letcall: "c" := clone ["x"]%E in (* FIXME : why do I need %E here ? *)
+ let: "rcbox" := new [ #(2 + ty.(ty_size))%nat ] in
+ "rcbox" +â‚— #0 <- #1;;
+ "rcbox" +â‚— #1 <- #1;;
+ "rcbox" +â‚— #2 <-{ty.(ty_size)} !"c";;
+ delete [ #ty.(ty_size); "c"];;
+ let: "arc''" := !"arc'" in
+ "arc'" <- "rcbox";;
+ letalloc: "rcold" <- "arc''" in
+ (* FIXME : here, we are dropping the old arc pointer. In the
+ case another strong reference has been dropped while
+ cloning, it is possible that we are actually dropping the
+ last reference here. This means that we may have to drop an
+ instance of [ty] here. Instead, we simply forget it. *)
+ let: "drop" := arc_drop ty in
+ letcall: "content" := "drop" ["rcold"]%E in
+ delete [ #(option ty).(ty_size); "content"];;
+ "r" <- "rcbox" +â‚— #2;;
+ delete [ #1; "arc"];; return: ["r"]
+ ]).
+
+ Lemma arc_make_mut_type ty `{!TyWf ty} clone :
+ typed_val clone (fn(∀ α, ∅; &shr{α} ty) → ty) →
+ typed_val (arc_make_mut ty clone) (fn(∀ α, ∅; &uniq{α} arc ty) → &uniq{α} ty).
+ Proof.
+ intros Hclone E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (α Ï ret arg). inv_vec arg=>rcx. simpl_subst.
+ iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
+ iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+ iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
+ rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock. destruct rc' as [[|rc'|]|]=>//=.
+ iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)";
+ [solve_typing..|].
+ iMod (bor_acc_cons with "LFT Hrc' Hα1") as "[Hrc' Hclose2]"=>//.
+ iDestruct "Hrc'" as (rcvl) "[Hrc'↦ Hrc]".
+ destruct rcvl as [|[[|rc|]|][|]]; try by iDestruct "Hrc" as ">[]".
+ rewrite heap_mapsto_vec_singleton. wp_read.
+ iAssert (shared_arc_own rc ty tid)%I with "[>Hrc]" as "Hrc".
+ { iDestruct "Hrc" as "[Hrc|$]"=>//. by iApply arc_own_share. }
+ iDestruct "Hrc" as (γ ν q') "[#(Hi & Hs & #Hc) Htoks]". wp_let.
+ wp_apply (try_unwrap_full_spec with "Hi Htoks"). iIntros (x).
+ pose proof (fin_to_nat_lt x). destruct (fin_to_nat x) as [|[|[]]]; last lia.
+ - iIntros "(Hrc0 & Hrc1 & HP1)". wp_case. wp_bind (_ +â‚— _)%E.
+ iSpecialize ("Hc" with "HP1").
+ iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); [solve_ndisj..|].
+ wp_op. iIntros "(#Hν & Hrc2 & H†)". iModIntro.
+ iMod ("Hclose2" with "[Hrc'↦ Hrc0 Hrc1 H†] Hrc2") as "[Hb Hα1]".
+ { iIntros "!> Hrc2". iExists [_]. rewrite heap_mapsto_vec_singleton.
+ iFrame. iLeft. by iFrame. }
+ iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
+ iApply (type_type _ _ _ [ rcx ◠box (uninit 1); #(shift_loc rc 2) ◠&uniq{α}ty;
+ r â— box (uninit 1) ]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
+ tctx_hasty_val' //. unlock. iFrame. }
+ iApply type_assign; [solve_typing..|].
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing.
+ - iIntros "[Hν Hweak]". wp_case. iSpecialize ("Hc" with "Hν"). wp_bind (new _).
+ iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); [solve_ndisj..|].
+ wp_apply wp_new=>//. iIntros (l vl) "(Hlen & H†& Hlvl) (#Hν & Hown & H†') !>".
+ iDestruct "Hlen" as %Hlen. destruct vl as [|?[|]]; simpl in Hlen; try lia.
+ wp_let. wp_op. rewrite !heap_mapsto_vec_cons shift_loc_assoc shift_loc_0.
+ iDestruct "Hlvl" as "(Hrc0 & Hrc1 & Hrc2)". wp_write. wp_op. wp_write.
+ wp_op. wp_op. iDestruct "Hown" as (vl) "[H↦ Hown]".
+ iDestruct (ty_size_eq with "Hown") as %Hlen'.
+ wp_apply (wp_memcpy with "[$Hrc2 $H↦]"); [lia..|].
+ iIntros "[H↦ H↦']". wp_seq. wp_write.
+ iMod ("Hclose2" $! (shift_loc l 2 ↦∗: ty_own ty tid)%I
+ with "[Hrc'↦ Hrc0 Hrc1 H†] [H↦ Hown]") as "[Hb Hα1]"; [|by auto with iFrame|].
+ { iIntros "!> H↦". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
+ iLeft. iFrame. iDestruct "H†" as "[?|%]"=>//.
+ by rewrite /Z.to_nat Pos2Nat.inj_succ SuccNat2Pos.id_succ. }
+ iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
+ iApply (type_type _ _ _ [ rcx ◠box (uninit 1); (#l +ₗ #2) ◠&uniq{α}ty;
+ r â— box (uninit 1) ]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
+ tctx_hasty_val' //. unlock. iFrame. }
+ iApply type_assign; [solve_typing..|].
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing.
+ - iIntros "[Htok Hν]". wp_case. wp_apply wp_new=>//.
+ iIntros (l [|?[]]) "/= (% & H†& Hl)"; try lia. wp_let. wp_op.
+ rewrite heap_mapsto_vec_singleton. wp_write. wp_let. wp_bind (of_val clone).
+ iApply (wp_wand with "[Hna]").
+ { iApply (Hclone _ [] with "LFT HE Hna");
+ rewrite /llctx_interp /tctx_interp //. }
+ clear Hclone clone. iIntros (clone) "(Hna & _ & [Hclone _])".
+ rewrite tctx_hasty_val. simpl.
+ iDestruct "Hclone" as (fb kb xb ecl ?) "(Heq & % & Hclone)".
+ iDestruct "Heq" as %[=->]. destruct xb as [|?[]]=>//. wp_rec.
+ iMod (lft_create with "LFT") as (β) "[Hβ #Hβ†]"=>//.
+ iMod (bor_create _ β with "LFT Hα2") as "[Hαβ Hα2]"=>//.
+ iMod (bor_fracture (λ q', (q / 2 * q').[α])%I with "LFT [Hαβ]") as "Hαβ'"=>//.
+ { by rewrite Qp_mult_1_r. }
+ iDestruct (frac_bor_lft_incl with "LFT Hαβ'") as "#Hαβ". iClear "Hαβ'".
+ iDestruct "Hs" as "[Hs|Hν']"; last by iDestruct (lft_tok_dead with "Hν Hν'") as "[]".
+ iMod (bor_create _ β with "LFT Hν") as "[Hνβ Hν]"=>//.
+ iMod (bor_fracture (λ q, (q' * q).[ν])%I with "LFT [Hνβ]") as "Hνβ'"=>//.
+ { by rewrite Qp_mult_1_r. }
+ iDestruct (frac_bor_lft_incl with "LFT Hνβ'") as "#Hνβ". iClear "Hνβ'".
+ erewrite <-!(of_to_val (λ: ["_r"], _)%E); [|solve_to_val..].
+ set (K := LamV ["_r"]%RustB _).
+ iApply ("Hclone" $! β β K [# #l] tid with "LFT [] Hna [Hβ] [-H†Hl]")=>/=;
+ last 1 first.
+ { rewrite /tctx_interp big_sepL_singleton tctx_hasty_val' //. simpl.
+ rewrite /= freeable_sz_full. iFrame. iExists [_].
+ rewrite heap_mapsto_vec_singleton /=. iFrame.
+ iApply (ty_shr_mono with "Hνβ Hs"). }
+ { refine ((λ HE : elctx_sat ((β ⊑ₑ α)::_) [] _, _) _).
+ iApply (HE 1%Qp with "[] [$Hαβ $HE]"); by rewrite /llctx_interp. solve_typing. }
+ { rewrite /llctx_interp big_sepL_singleton. iExists β. iFrame "∗#".
+ rewrite left_id //. }
+ rewrite /K /=. clear K. iIntros (?). rewrite elem_of_list_singleton.
+ iIntros "%". subst. iIntros (cl) "Hna Hβ Hcl". inv_vec cl=>cl. simpl. wp_let.
+ rewrite [llctx_interp [β ⊑ₗ []] 1]/llctx_interp big_sepL_singleton.
+ iDestruct "Hβ" as (β') "(Hβeq & Hβ & Hβend)". rewrite /= left_id.
+ iDestruct "Hβeq" as %<-. wp_bind Skip. iSpecialize ("Hβend" with "Hβ").
+ iApply wp_mask_mono; last iApply (wp_step_fupd with "Hβend"); [solve_ndisj..|].
+ wp_seq. iIntros "#Hβ !>". wp_seq. wp_rec.
+ iMod ("Hα2" with "Hβ") as "Hα2". iMod ("Hν" with "Hβ") as "Hν".
+ wp_apply wp_new=>//. iIntros (l' vl) "(% & Hl'†& Hl')". wp_let. wp_op.
+ rewrite shift_loc_0. destruct vl as [|?[|??]]; simpl in *; try lia.
+ rewrite !heap_mapsto_vec_cons shift_loc_assoc.
+ iDestruct "Hl'" as "(Hl' & Hl'1 & Hl'2)". wp_write. wp_op. wp_write. wp_op.
+ rewrite tctx_interp_singleton tctx_hasty_val.
+ destruct cl as [[|cl|]|]; try by iDestruct "Hcl" as "[]".
+ iDestruct "Hcl" as "[Hcl Hcl†]". iDestruct "Hcl" as (vl) "[>Hcl↦ Hown]".
+ iDestruct (ty_size_eq with "Hown") as "#>%".
+ wp_apply (wp_memcpy with "[$Hl'2 $Hcl↦]"); [lia..|]. iIntros "[Hl'2 Hcl↦]".
+ wp_seq. rewrite freeable_sz_full.
+ wp_apply (wp_delete with "[$Hcl↦ Hcl†]");
+ [lia|by replace (length vl) with (ty.(ty_size))|].
+ iIntros "_". wp_seq. wp_read. wp_let. wp_write.
+ iMod ("Hclose2" $! (shift_loc l' 2 ↦∗: ty_own ty tid)%I with
+ "[Hrc'↦ Hl' Hl'1 Hl'†] [Hl'2 Hown]") as "[Hl' Hα1]".
+ { iIntros "!> H". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
+ iLeft. iFrame. iDestruct "Hl'†" as "[?|%]"=>//.
+ by rewrite /Z.to_nat Pos2Nat.inj_succ SuccNat2Pos.id_succ. }
+ { iExists _. iFrame. }
+ iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
+ iApply (type_type _ _ _ [ #rc ◠arc ty; #l' +ₗ #2 ◠&uniq{α}ty;
+ r â— box (uninit 1); rcx â— box (uninit 1) ]
+ with "[] LFT HE Hna HL Hk [-]"); last first.
+ { rewrite 3!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
+ !tctx_hasty_val' //. unlock. iFrame. iRight.
+ iExists _, _, _. iFrame "∗#". }
+ iApply type_letalloc_1; [solve_typing..|]. iIntros (rcold). simpl_subst.
+ iApply type_let. apply arc_drop_type. solve_typing. iIntros (drop). simpl_subst.
+ iApply (type_letcall ()); try solve_typing.
+ { (* FIXME : solve_typing should be able to do this. *)
+ move=>Ï' /=. change (ty_outlives_E (option ty) Ï') with (ty_outlives_E ty Ï').
+ solve_typing. }
+ iIntros (content). simpl_subst.
+ iApply type_delete; [solve_typing..|].
+ iApply type_assign; [solve_typing..|].
+ iApply type_delete; [solve_typing..|].
+ iApply type_jump; solve_typing.
+ Qed.
End arc.
\ No newline at end of file
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 8b12b139f1edff33220c2a57c5a185220f4455cf..923943cc6b6fee5c3d10c27c3903b16ec636fbd4 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -47,7 +47,8 @@ Section rc.
- The weak state, meaning that there only exists weak references. The
authoritative state is something like (None, weak), where weak is the
number of weak references.
- - The dead state, meaning that no reference exist anymore.
+ - The dead state, meaning that no reference exist anymore. The
+ authoritat state is something like (None, 0).
Note that when we are in the living or dropping states, the weak reference
count stored in the heap is actually one plus the actual number of weak
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 7362d596d4a0eace986b261c4732a225ba5d4072..2fa0c52efc3f3a11ac8eea7e8be3e777202957ac 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -214,8 +214,7 @@ Section rwlock_functions.
iExists _. iFrame. iExists _, _. iSplitR; first done. iFrame "#∗".
rewrite Qp_div_2. iSplitL; last done.
iIntros "!> Hν". iApply "Hh". rewrite -lft_dead_or. auto. }
- iMod ("Hclose''" with "[$INV]") as "Hβtok1".
- iApply (wp_if _ true). iIntros "!>!>".
+ iMod ("Hclose''" with "[$INV]") as "Hβtok1". iModIntro. wp_case.
iMod ("Hclose'" with "[$]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iApply (type_type _ _ _
[ x ◠box (&shr{α}(rwlock ty)); r ◠box (uninit 2);
@@ -229,8 +228,8 @@ Section rwlock_functions.
simpl. iApply type_jump; solve_typing.
+ iApply (wp_cas_int_fail with "Hlx"); try done. iNext. iIntros "Hlx".
iMod ("Hclose''" with "[Hlx Hownst Hst]") as "Hβtok1"; first by iExists _; iFrame.
- iModIntro. iApply (wp_if _ false). iNext.
- iMod ("Hclose'" with "[$]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
+ iModIntro. wp_case. iMod ("Hclose'" with "[$]") as "Hα".
+ iMod ("Hclose" with "Hα HL") as "HL".
iSpecialize ("Hk" with "[]"); first solve_typing.
iApply ("Hk" $! [#] with "Hna HL").
rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
@@ -278,7 +277,7 @@ Section rwlock_functions.
iNext. iIntros "Hlx".
iMod ("Hclose''" with "[Hlx Hownst Hst]") as "Hβtok"; first by iExists _; iFrame.
iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
- iModIntro. iApply (wp_if _ false). iNext.
+ iModIntro. wp_case.
iApply (type_type _ _ _
[ x ◠box (&shr{α}(rwlock ty)); r ◠box (uninit 2) ]
with "[] LFT HE Hna HL Hk"); first last.
@@ -290,7 +289,7 @@ Section rwlock_functions.
iMod (own_update with "Hownst") as "[Hownst ?]".
{ by eapply auth_update_alloc, (op_local_update_discrete _ _ writing_st). }
iMod ("Hclose''" with "[Hlx Hownst]") as "Hβtok". { iExists _. iFrame. }
- iModIntro. iApply (wp_if _ true). iNext. iMod ("Hclose'" with "Hβtok") as "Hα".
+ iModIntro. wp_case. iMod ("Hclose'" with "Hβtok") as "Hα".
iMod ("Hclose" with "Hα HL") as "HL".
iApply (type_type _ _ _
[ x ◠box (&shr{α}(rwlock ty)); r ◠box (uninit 2);