From 898f8957fe7c21486c4d68c231469b0e476ce26b Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 25 Jan 2017 02:24:43 +0100
Subject: [PATCH] (Im)mutable borrowing of refcells.
Other changes:
- Get rid of * spec pattern (deprecated in iris trunk)
- Make freeable_sz opaque (and simplifiy some proofs because of this)
- Refact option_as_mut and cell
- Prove lft_glb_acc, for gettings tokens of an intersections from tokens of its components
- Add some support for the = operator for ints in the proof mode
---
opam.pins | 2 +-
theories/lang/derived.v | 24 +-
theories/lang/heap.v | 2 +-
theories/lang/notation.v | 4 +-
theories/lang/proofmode.v | 1 +
theories/lang/races.v | 2 -
theories/lifetime/frac_borrow.v | 4 +-
theories/lifetime/lifetime.v | 8 +-
theories/lifetime/lifetime_sig.v | 2 +
theories/lifetime/model/accessors.v | 6 +-
theories/lifetime/model/borrow.v | 2 +-
theories/lifetime/model/primitive.v | 71 ++---
theories/lifetime/model/raw_reborrow.v | 2 +-
theories/typing/borrow.v | 6 +-
theories/typing/cont.v | 10 +-
theories/typing/cont_context.v | 10 +-
theories/typing/examples/option_as_mut.v | 18 +-
theories/typing/function.v | 14 +-
theories/typing/lft_contexts.v | 14 +-
theories/typing/own.v | 12 +-
theories/typing/product.v | 4 +-
theories/typing/product_split.v | 4 +-
theories/typing/programs.v | 12 +-
theories/typing/shr_bor.v | 2 +-
theories/typing/soundness.v | 2 +-
theories/typing/sum.v | 2 +-
theories/typing/type.v | 4 +-
theories/typing/type_context.v | 5 +-
theories/typing/type_sum.v | 18 +-
theories/typing/uniq_bor.v | 8 +-
theories/typing/unsafe/cell.v | 30 +--
theories/typing/unsafe/refcell.v | 313 +++++++++++++++++++----
32 files changed, 427 insertions(+), 191 deletions(-)
diff --git a/opam.pins b/opam.pins
index 6338c398..ccdcb41f 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq da56bbb0f26f4f77fe28efea60f81f06d8a2ac59
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 939b747baa303ca3e2e1538cfd76fccd900596cf
diff --git a/theories/lang/derived.v b/theories/lang/derived.v
index f72861cf..a84188b1 100644
--- a/theories/lang/derived.v
+++ b/theories/lang/derived.v
@@ -104,17 +104,33 @@ Lemma wp_le E (n1 n2 : Z) P Φ :
(n2 < n1 → P -∗ ▷ Φ (LitV false)) →
P -∗ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
Proof.
- iIntros (Hl Hg) "HP". iApply wp_fupd.
+ iIntros (Hl Hg) "HP".
destruct (bool_decide_reflect (n1 ≤ n2)); [rewrite Hl //|rewrite Hg; last omega];
clear Hl Hg; (iApply wp_bin_op_pure; first by econstructor); iNext; iIntros (?? Heval);
inversion_clear Heval; [rewrite bool_decide_true //|rewrite bool_decide_false //].
Qed.
+Lemma wp_eq_int E (n1 n2 : Z) P Φ :
+ (n1 = n2 → P -∗ ▷ Φ (LitV true)) →
+ (n1 ≠n2 → P -∗ ▷ Φ (LitV false)) →
+ P -∗ WP BinOp EqOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
+Proof.
+ iIntros (Hl Hg) "HP".
+ destruct (bool_decide_reflect (n1 = n2)); [rewrite Hl //|rewrite Hg //];
+ clear Hl Hg; iApply wp_bin_op_pure; subst.
+ - intros. apply BinOpEqTrue. constructor.
+ - iNext; iIntros (?? Heval). inversion_clear Heval. done. by inversion H.
+ - intros. apply BinOpEqFalse. by constructor.
+ - iNext; iIntros (?? Heval). inversion_clear Heval. by inversion H. done.
+Qed.
+
+(* TODO : wp_eq for locations, if needed. *)
+
Lemma wp_offset E l z Φ :
▷ Φ (LitV $ LitLoc $ shift_loc l z) -∗
WP BinOp OffsetOp (Lit $ LitLoc l) (Lit $ LitInt z) @ E {{ Φ }}.
Proof.
- iIntros "HP". iApply wp_fupd. iApply wp_bin_op_pure; first by econstructor.
+ iIntros "HP". iApply wp_bin_op_pure; first by econstructor.
iNext. iIntros (?? Heval). inversion_clear Heval. done.
Qed.
@@ -122,7 +138,7 @@ Lemma wp_plus E z1 z2 Φ :
▷ Φ (LitV $ LitInt $ z1 + z2) -∗
WP BinOp PlusOp (Lit $ LitInt z1) (Lit $ LitInt z2) @ E {{ Φ }}.
Proof.
- iIntros "HP". iApply wp_fupd. iApply wp_bin_op_pure; first by econstructor.
+ iIntros "HP". iApply wp_bin_op_pure; first by econstructor.
iNext. iIntros (?? Heval). inversion_clear Heval. done.
Qed.
@@ -130,7 +146,7 @@ Lemma wp_minus E z1 z2 Φ :
▷ Φ (LitV $ LitInt $ z1 - z2) -∗
WP BinOp MinusOp (Lit $ LitInt z1) (Lit $ LitInt z2) @ E {{ Φ }}.
Proof.
- iIntros "HP". iApply wp_fupd. iApply wp_bin_op_pure; first by econstructor.
+ iIntros "HP". iApply wp_bin_op_pure; first by econstructor.
iNext. iIntros (?? Heval). inversion_clear Heval. done.
Qed.
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index f27dbff4..c48e4b1c 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -379,7 +379,7 @@ Section heap.
- iNext. iExists σ', _. subst σ'. iFrame. iPureIntro.
rewrite HvlLen Nat2Z.id. auto using heap_freeable_rel_init_mem.
- rewrite heap_freeable_eq /heap_freeable_def. iApply "HΦ".
- iSplit; first auto. iFrame. by rewrite heap_mapsto_vec_combine.
+ iSplitR; first auto. iFrame. by rewrite heap_mapsto_vec_combine.
Qed.
Lemma heap_free_vs l vl σ :
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index 982ee436..8af1b8f3 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -27,7 +27,7 @@ Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : expr_scope.
Notation "'case:' e0 'of' el" := (Case e0%E el%E)
(at level 102, e0, el at level 150) : expr_scope.
Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
- (only parsing, at level 200, e1, e2, e3 at level 150) : expr_scope.
+ (only parsing, at level 102, e1, e2, e3 at level 150) : expr_scope.
Notation "()" := LitUnit : val_scope.
Notation "! e" := (Read Na1Ord e%E) (at level 9, format "! e") : expr_scope.
Notation "!ˢᶜ e" := (Read ScOrd e%E) (at level 9, format "!ˢᶜ e") : expr_scope.
@@ -37,6 +37,8 @@ Notation "e1 - e2" := (BinOp MinusOp e1%E e2%E)
(at level 50, left associativity) : expr_scope.
Notation "e1 ≤ e2" := (BinOp LeOp e1%E e2%E)
(at level 70) : expr_scope.
+Notation "e1 = e2" := (BinOp EqOp e1%E e2%E)
+ (at level 70) : expr_scope.
(* The unicode ↠is already part of the notation "_ ↠_; _" for bind. *)
Notation "e1 <-ˢᶜ e2" := (Write ScOrd e1%E e2%E)
(at level 80) : expr_scope.
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index c606d13e..43aae5c7 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -91,6 +91,7 @@ Tactic Notation "wp_op" :=
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| BinOp LeOp _ _ => wp_bind_core K; apply wp_le; wp_finish
+ | BinOp EqOp _ _ => wp_bind_core K; apply wp_eq_int; wp_finish
| BinOp OffsetOp _ _ =>
wp_bind_core K; etrans; [|eapply wp_offset; try fast_done]; wp_finish
| BinOp PlusOp _ _ =>
diff --git a/theories/lang/races.v b/theories/lang/races.v
index c0b8b497..1ba1a13f 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -102,8 +102,6 @@ Lemma next_access_head_reducible_state e σ a l :
| (FreeAcc, _) => ∃ v ls, σ !! l = Some (ls, v)
end.
Proof.
-(* assert (Hrefl : ∀ l, ~lit_neq σ l l).
- { intros ? Hneq. inversion Hneq; done. } *)
intros Ha (e'&σ'&ef&Hstep) Hrednonstuck. destruct Ha; inv_head_step; eauto.
- destruct n; first by eexists. exfalso. eapply Hrednonstuck; last done.
eapply CasStuckS; done.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index d144e141..c0684b54 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -42,13 +42,13 @@ Section frac_bor.
iIntros (?) "#LFT Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done.
iMod (bor_acc_atomic_strong with "LFT Hφ") as "[H|[H†Hclose]]". done.
- iDestruct "H" as (κ') "(#Hκκ' & Hφ & Hclose)".
- iMod ("Hclose" with "*[-] []") as "Hφ"; last first.
+ iMod ("Hclose" with "[-] []") as "Hφ"; last first.
{ iExists γ, κ'. iFrame "#". iApply (bor_share with "Hφ"). done. }
{ iIntros "!>Hφ H†!>". iNext. iDestruct "Hφ" as (q') "(Hφ & _ & [%|Hκ])". by subst.
iDestruct "Hκ" as (q'') "[_ Hκ]".
iDestruct (lft_tok_dead with "Hκ H†") as "[]". }
iExists 1%Qp. iFrame. eauto.
- - iMod ("Hclose" with "*") as "_"; last first.
+ - iMod "Hclose" as "_"; last first.
iExists γ, κ. iSplitR. by iApply lft_incl_refl.
iMod (bor_fake with "LFT H†"). done. by iApply bor_share.
Qed.
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index bae90946..9b24ff4a 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -25,7 +25,7 @@ Lemma bor_acc_cons E q κ P :
Proof.
iIntros (?) "#LFT HP Htok".
iMod (bor_acc_strong with "LFT HP Htok") as (κ') "(#Hκκ' & $ & Hclose)"; first done.
- iIntros "!>*HQ HPQ". iMod ("Hclose" with "*HQ [HPQ]") as "[Hb $]".
+ iIntros "!>*HQ HPQ". iMod ("Hclose" with "HQ [HPQ]") as "[Hb $]".
- iNext. iIntros "? _". by iApply "HPQ".
- iApply (bor_shorten with "Hκκ' Hb").
Qed.
@@ -36,7 +36,7 @@ Lemma bor_acc E q κ P :
Proof.
iIntros (?) "#LFT HP Htok".
iMod (bor_acc_cons with "LFT HP Htok") as "($ & Hclose)"; first done.
- iIntros "!>HP". iMod ("Hclose" with "*HP []") as "[$ $]"; auto.
+ iIntros "!>HP". iMod ("Hclose" with "HP []") as "[$ $]"; auto.
Qed.
Lemma bor_or E κ P Q :
@@ -54,7 +54,7 @@ Proof.
iIntros (?) "#LFT Hb".
iMod (bor_acc_atomic_cons with "LFT Hb") as "[H|[H†Hclose]]"; first done.
- iDestruct "H" as "[HP Hclose]". iModIntro. iNext.
- iApply ("Hclose" with "* HP"). by iIntros "!> $".
+ iApply ("Hclose" with "HP"). by iIntros "!> $".
- iIntros "!> !>". iMod "Hclose" as "_". by iApply (bor_fake with "LFT").
Qed.
@@ -64,7 +64,7 @@ Lemma bor_later_tok E q κ P :
Proof.
iIntros (?) "#LFT Hb Htok".
iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose]"; first done.
- iModIntro. iNext. iApply ("Hclose" with "* HP []"). by iIntros "!> $".
+ iModIntro. iNext. iApply ("Hclose" with "HP []"). by iIntros "!> $".
Qed.
Lemma bor_persistent P `{!PersistentP P} E κ :
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 0da0470f..b2c21ac8 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -126,6 +126,8 @@ Module Type lifetime_sig.
(* Because Coq's module system is horrible, we have to repeat properties of lft_incl here
unless we want to prove them twice (both here and in model.primitive) *)
+ Parameter lft_glb_acc : ∀ κ κ' q q', q.[κ] -∗ q'.[κ'] -∗
+ ∃ q'', q''.[κ ∪ κ'] ∗ (q''.[κ ∪ κ'] -∗ q.[κ] ∗ q'.[κ']).
Parameter lft_le_incl : ∀ κ κ', κ' ⊆ κ → (κ ⊑ κ')%I.
Parameter lft_incl_refl : ∀ κ, (κ ⊑ κ)%I.
Parameter lft_incl_trans : ∀ κ κ' κ'', κ ⊑ κ' -∗ κ' ⊑ κ'' -∗ κ ⊑ κ''.
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 82b9e942..b3b74823 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -65,7 +65,7 @@ Proof.
iApply fupd_mask_mono; last iMod ("HvsQ" with "HQ H†") as "HP". solve_ndisj.
iModIntro. iAssert (â–· Pb)%I with "[HPb HP]" as "HPb".
{ iNext. iRewrite "HEQ". iFrame. }
- iApply ("Hvs" with "* Hinv HPb H†").
+ iApply ("Hvs" with "Hinv HPb H†").
Qed.
(** Indexed borrow *)
@@ -276,7 +276,7 @@ Proof.
iIntros (?) "#LFT HP".
iMod (bor_acc_atomic_strong with "LFT HP") as "[H|[??]]"; first done.
- iLeft. iDestruct "H" as (κ') "(#Hκκ' & $ & Hclose)". iIntros "!>*HQ HPQ".
- iMod ("Hclose" with "* HQ [HPQ]") as "Hb".
+ iMod ("Hclose" with "HQ [HPQ]") as "Hb".
+ iNext. iIntros "? _". by iApply "HPQ".
+ iApply (bor_shorten with "Hκκ' Hb").
- iRight. by iFrame.
@@ -289,7 +289,7 @@ Lemma bor_acc_atomic E κ P :
Proof.
iIntros (?) "#LFT HP".
iMod (bor_acc_atomic_cons with "LFT HP") as "[[HP Hclose]|[? ?]]"; first done.
- - iLeft. iIntros "!> {$HP} HP". iMod ("Hclose" with "* HP []"); auto.
+ - iLeft. iIntros "!> {$HP} HP". iMod ("Hclose" with "HP []"); auto.
- iRight. by iFrame.
Qed.
End accessors.
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 1f220cda..77e8b588 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -48,7 +48,7 @@ Proof.
iExists P. rewrite -uPred.iff_refl. auto.
+ clear -HE. iIntros "!> H†".
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
- iDestruct ("HIlookup" with "* HI") as %Hκ.
+ iDestruct ("HIlookup" with "HI") as %Hκ.
iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinv Hclose']".
{ by apply elem_of_dom. }
rewrite /lft_dead; iDestruct "H†" as (Λ) "[% #H†]".
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index b7e5bb90..33cd454c 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -303,6 +303,28 @@ Global Instance idx_bor_own_as_fractional i q :
Proof. split. done. apply _. Qed.
(** Lifetime inclusion *)
+Lemma lft_incl_acc E κ κ' q :
+ ↑lftN ⊆ E →
+ κ ⊑ κ' -∗ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
+Proof.
+ rewrite /lft_incl.
+ iIntros (?) "#[H _] Hq". iApply fupd_mask_mono; first done.
+ iMod ("H" with "Hq") as (q') "[Hq' Hclose]". iExists q'.
+ iIntros "{$Hq'} !> Hq". iApply fupd_mask_mono; first done. by iApply "Hclose".
+Qed.
+
+Lemma lft_incl_dead E κ κ' : ↑lftN ⊆ E → κ ⊑ κ' -∗ [†κ'] ={E}=∗ [†κ].
+Proof.
+ rewrite /lft_incl.
+ iIntros (?) "#[_ H] Hq". iApply fupd_mask_mono; first done. by iApply "H".
+Qed.
+
+Lemma lft_incl_intro κ κ' :
+ □ ((∀ q, lft_tok q κ ={↑lftN}=∗ ∃ q',
+ lft_tok q' κ' ∗ (lft_tok q' κ' ={↑lftN}=∗ lft_tok q κ)) ∗
+ (lft_dead κ' ={↑lftN}=∗ lft_dead κ)) -∗ κ ⊑ κ'.
+Proof. reflexivity. Qed.
+
Lemma lft_le_incl κ κ' : κ' ⊆ κ → (κ ⊑ κ')%I.
Proof.
iIntros (->%gmultiset_union_difference) "!#". iSplitR.
@@ -318,25 +340,32 @@ Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' -∗ κ' ⊑ κ'' -∗ κ ⊑ κ''.
Proof.
rewrite /lft_incl. iIntros "#[H1 H1†] #[H2 H2†] !#". iSplitR.
- iIntros (q) "Hκ".
- iMod ("H1" with "*Hκ") as (q') "[Hκ' Hclose]".
- iMod ("H2" with "*Hκ'") as (q'') "[Hκ'' Hclose']".
+ iMod ("H1" with "Hκ") as (q') "[Hκ' Hclose]".
+ iMod ("H2" with "Hκ'") as (q'') "[Hκ'' Hclose']".
iExists q''. iIntros "{$Hκ''} !> Hκ''".
iMod ("Hclose'" with "Hκ''") as "Hκ'". by iApply "Hclose".
- iIntros "H†". iMod ("H2†" with "H†"). by iApply "H1†".
Qed.
+Lemma lft_glb_acc κ κ' q q' :
+ q.[κ] -∗ q'.[κ'] -∗ ∃ q'', q''.[κ ∪ κ'] ∗ (q''.[κ ∪ κ'] -∗ q.[κ] ∗ q'.[κ']).
+Proof.
+ iIntros "Hκ Hκ'".
+ destruct (Qp_lower_bound q q') as (qq & q0 & q'0 & -> & ->).
+ iExists qq. rewrite -lft_tok_sep.
+ iDestruct "Hκ" as "[$$]". iDestruct "Hκ'" as "[$$]". auto.
+Qed.
+
Lemma lft_incl_glb κ κ' κ'' : κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ∪ κ''.
Proof.
rewrite /lft_incl. iIntros "#[H1 H1†] #[H2 H2†]!#". iSplitR.
- iIntros (q) "[Hκ'1 Hκ'2]".
- iMod ("H1" with "*Hκ'1") as (q') "[Hκ' Hclose']".
- iMod ("H2" with "*Hκ'2") as (q'') "[Hκ'' Hclose'']".
- destruct (Qp_lower_bound q' q'') as (qq & q'0 & q''0 & -> & ->).
- iExists qq. rewrite -lft_tok_sep.
- iDestruct "Hκ'" as "[$ Hκ']". iDestruct "Hκ''" as "[$ Hκ'']".
- iIntros "!> [Hκ'0 Hκ''0]".
- iMod ("Hclose'" with "[$Hκ' $Hκ'0]") as "$".
- iApply "Hclose''". iFrame.
+ iMod ("H1" with "Hκ'1") as (q') "[Hκ' Hclose']".
+ iMod ("H2" with "Hκ'2") as (q'') "[Hκ'' Hclose'']".
+ iDestruct (lft_glb_acc with "Hκ' Hκ''") as (qq) "[Hqq Hclose]".
+ iExists qq. iFrame. iIntros "!> Hqq".
+ iDestruct ("Hclose" with "Hqq") as "[Hκ' Hκ'']".
+ iMod ("Hclose'" with "Hκ'") as "$". by iApply "Hclose''".
- rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
Qed.
@@ -350,28 +379,6 @@ Proof.
iApply lft_le_incl. apply gmultiset_union_subseteq_r.
Qed.
-Lemma lft_incl_acc E κ κ' q :
- ↑lftN ⊆ E →
- κ ⊑ κ' -∗ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
-Proof.
- rewrite /lft_incl.
- iIntros (?) "#[H _] Hq". iApply fupd_mask_mono; first done.
- iMod ("H" with "* Hq") as (q') "[Hq' Hclose]". iExists q'.
- iIntros "{$Hq'} !> Hq". iApply fupd_mask_mono; first done. by iApply "Hclose".
-Qed.
-
-Lemma lft_incl_dead E κ κ' : ↑lftN ⊆ E → κ ⊑ κ' -∗ [†κ'] ={E}=∗ [†κ].
-Proof.
- rewrite /lft_incl.
- iIntros (?) "#[_ H] Hq". iApply fupd_mask_mono; first done. by iApply "H".
-Qed.
-
-Lemma lft_incl_intro κ κ' :
- □ ((∀ q, lft_tok q κ ={↑lftN}=∗ ∃ q',
- lft_tok q' κ' ∗ (lft_tok q' κ' ={↑lftN}=∗ lft_tok q κ)) ∗
- (lft_dead κ' ={↑lftN}=∗ lft_dead κ)) -∗ κ ⊑ κ'.
-Proof. reflexivity. Qed.
-
(** Basic rules about borrows *)
Lemma raw_bor_iff_proper i P P' : ▷ □ (P ↔ P') -∗ raw_bor i P -∗ raw_bor i P'.
Proof.
diff --git a/theories/lifetime/model/raw_reborrow.v b/theories/lifetime/model/raw_reborrow.v
index a3be4ed6..4d749720 100644
--- a/theories/lifetime/model/raw_reborrow.v
+++ b/theories/lifetime/model/raw_reborrow.v
@@ -181,7 +181,7 @@ Proof.
iFrame. }
clear dependent A I Pb Pb' Pi. iModIntro. iIntros "H†".
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
- iDestruct ("HIlookup" with "* HI") as %Hκ'.
+ iDestruct ("HIlookup" with "HI") as %Hκ'.
iDestruct (big_sepS_delete _ _ κ' with "Hinv") as "[Hκinv' Hinv]";
first by apply elem_of_dom.
rewrite {1}/lft_inv; iDestruct "Hκinv'" as "[[Halive >%]|[Hdead >%]]".
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index f43fa84a..6ff47693 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -56,7 +56,7 @@ Section borrow.
iDestruct "H↦" as ([|[[|l'|]|][]]) "[>H↦ Hown]"; try iDestruct "Hown" as ">[]".
iDestruct "Hown" as "[Hown H†]". rewrite heap_mapsto_vec_singleton -wp_fupd. wp_read.
iMod ("Hclose'" $! (l↦#l' ∗ freeable_sz n (ty_size ty) l' ∗ _)%I
- with "*[H↦ Hown H†][]") as "[Hbor Htok]"; last 1 first.
+ with "[H↦ Hown H†][]") as "[Hbor Htok]"; last 1 first.
- iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
iMod ("Hclose" with "Htok") as "($ & $)".
@@ -87,7 +87,7 @@ Section borrow.
(try iDestruct "Hown" as "[]"). iDestruct "Hown" as (l') "#[H↦b #Hown]".
iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
iApply (wp_fupd_step _ (_∖_) with "[Hown Htok2]"); try done.
- - iApply ("Hown" with "* [%] Htok2"). set_solver+.
+ - iApply ("Hown" with "[%] Htok2"). set_solver+.
- iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
iMod ("Hclose" with "[Htok1 Htok2]") as "($ & $)"; first by iFrame.
@@ -156,7 +156,7 @@ Section borrow.
{ iApply (lft_incl_glb with "Hincl []"). iApply lft_incl_refl. }
iMod (lft_incl_acc with "Hincl' Htok2") as (q2) "[Htok2 Hclose'']". solve_ndisj.
iApply (wp_fupd_step _ (_∖_) with "[Hown Htok2]"); try done.
- - iApply ("Hown" with "* [%] Htok2"). set_solver+.
+ - iApply ("Hown" with "[%] Htok2"). set_solver+.
- iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
iMod ("Hclose''" with "Htok2") as "Htok2".
iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index fd373132..7e579382 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -15,8 +15,8 @@ Section typing.
Proof.
iIntros (HC Hincl) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT".
iMod (Hincl with "LFT HE HL HT") as "(HE & HL & HT)".
- iSpecialize ("HC" with "HE * []"); first done.
- rewrite -{3}(vec_to_list_of_list args). iApply ("HC" with "* Htl HL HT").
+ iSpecialize ("HC" with "HE []"); first done.
+ rewrite -{3}(vec_to_list_of_list args). iApply ("HC" with "Htl HL HT").
Qed.
Lemma type_cont argsb L1 (T' : vec val (length argsb) → _) E L2 C T econt e2 kb :
@@ -28,13 +28,13 @@ Section typing.
Proof.
iIntros (Hc1 Hc2 He2 Hecont) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT". iApply wp_let'.
{ simpl. rewrite decide_left. done. }
- iModIntro. iApply (He2 with "* HEAP LFT Htl HE HL [HC] HT"). clear He2.
+ iModIntro. iApply (He2 with "HEAP LFT Htl HE HL [HC] HT"). clear He2.
iIntros "HE". iLöb as "IH". iIntros (x) "H".
- iDestruct "H" as %[->|?]%elem_of_cons; last by iApply ("HC" with "HE *").
+ iDestruct "H" as %[->|?]%elem_of_cons; last by iApply ("HC" with "HE").
iIntros (args) "Htl HL HT". iApply wp_rec; try done.
{ rewrite Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
{ by rewrite -(subst_v_eq (_ :: _) (RecV _ _ _ ::: _)). }
- iNext. iApply (Hecont with "* HEAP LFT Htl HE HL [HC] HT").
+ iNext. iApply (Hecont with "HEAP LFT Htl HE HL [HC] HT").
by iApply "IH".
Qed.
End typing.
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index 67c01c7d..e09992b7 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -73,7 +73,7 @@ Section cont_context.
Proof.
rewrite /cctx_interp. iIntros "H". iIntros ([k L n T]) "%".
iIntros (args) "HL HT". iMod "H".
- by iApply ("H" $! (k â—cont(L, T)%CC) with "[%] * HL HT").
+ by iApply ("H" $! (k â—cont(L, T)%CC) with "[%] HL HT").
Qed.
Definition cctx_incl (E : elctx) (C1 C2 : cctx): Prop :=
@@ -92,7 +92,7 @@ Section cont_context.
Lemma incl_cctx_incl E C1 C2 : C1 ⊆ C2 → cctx_incl E C2 C1.
Proof.
rewrite /cctx_incl /cctx_interp. iIntros (HC1C2 tid ?) "_ H HE * %".
- iApply ("H" with "HE * [%]"). by apply HC1C2.
+ iApply ("H" with "HE [%]"). by apply HC1C2.
Qed.
Lemma cctx_incl_cons_match E k L n (T1 T2 : vec val n → tctx) C1 C2 :
@@ -104,11 +104,11 @@ Section cont_context.
- iIntros (args) "Htl HL HT".
iMod (HT1T2 with "LFT HE HL HT") as "(HE & HL & HT)".
iSpecialize ("H" with "HE").
- iApply ("H" $! (_ â—cont(_, _))%CC with "[%] * Htl HL HT").
+ iApply ("H" $! (_ â—cont(_, _))%CC with "[%] Htl HL HT").
constructor.
- - iApply (HC1C2 with "LFT [H] HE * [%]"); last done.
+ - iApply (HC1C2 with "LFT [H] HE [%]"); last done.
iIntros "HE". iIntros (x') "%".
- iApply ("H" with "HE * [%]"). by apply elem_of_cons; auto.
+ iApply ("H" with "HE [%]"). by apply elem_of_cons; auto.
Qed.
Lemma cctx_incl_nil E C : cctx_incl E C [].
diff --git a/theories/typing/examples/option_as_mut.v b/theories/typing/examples/option_as_mut.v
index 38df7ab7..ae5c951b 100644
--- a/theories/typing/examples/option_as_mut.v
+++ b/theories/typing/examples/option_as_mut.v
@@ -6,9 +6,11 @@ Section option_as_mut.
Definition option_as_mut : val :=
funrec: <> ["o"] :=
- let: "o'" := !"o" in case: !"o'" of
- [ let: "r" := new [ #2 ] in "r" <-{Σ 0} ();; "k" ["r"];
- let: "r" := new [ #2 ] in "r" <-{Σ 1} "o'" +ₗ #1;; "k" ["r"] ]
+ let: "o'" := !"o" in
+ let: "r" := new [ #2 ] in
+ case: !"o'" of
+ [ "r" <-{Σ 0} ();; "k" ["r"];
+ "r" <-{Σ 1} "o'" +ₗ #1;; "k" ["r"] ]
cont: "k" ["r"] :=
delete [ #1; "o"];; "return" ["r"].
@@ -20,12 +22,12 @@ Section option_as_mut.
eapply (type_cont [_] [] (λ r, [o ◠_; r!!!0 ◠_])%TC) ; [solve_typing..| |].
- intros k. simpl_subst.
eapply type_deref; [solve_typing..|apply read_own_move|done|]=>o'. simpl_subst.
- eapply type_case_uniq; [solve_typing..|]. constructor; last constructor; last constructor.
- + left. eapply type_new; [solve_typing..|]. intros r. simpl_subst.
- eapply (type_sum_assign_unit [unit; &uniq{α}τ]%T); [solve_typing..|by apply write_own|done|].
+ eapply type_new; [solve_typing..|]. intros r. simpl_subst.
+ eapply type_case_uniq; [solve_typing..|].
+ constructor; last constructor; last constructor; left.
+ + eapply (type_sum_assign_unit [unit; &uniq{α}τ]%T); [solve_typing..|by apply write_own|done|].
eapply (type_jump [_]); solve_typing.
- + left. eapply type_new; [solve_typing..|]. intros r. simpl_subst.
- eapply (type_sum_assign [unit; &uniq{α}τ]%T); [solve_typing..|by apply write_own|done|].
+ + eapply (type_sum_assign [unit; &uniq{α}τ]%T); [solve_typing..|by apply write_own|done|].
eapply (type_jump [_]); solve_typing.
- move=>/= k r. inv_vec r=>r. simpl_subst.
eapply type_delete; [solve_typing..|].
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 3808821a..84625161 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -79,13 +79,13 @@ Section typing.
iExists fb, kb, xb, e, _. iSplit. done. iSplit. done. iNext.
rewrite /typed_body. iIntros "* !# * #HEAP _ Htl HE HL HC HT".
iDestruct (elctx_interp_persist with "HE") as "#HEp".
- iMod (HE with "HE0 HL0 * HE") as (qE') "[HE' Hclose]". done.
- iApply ("Hf" with "* HEAP LFT Htl HE' HL [HC Hclose] [HT]").
+ iMod (HE with "HE0 HL0 HE") as (qE') "[HE' Hclose]". done.
+ iApply ("Hf" with "HEAP LFT Htl HE' HL [HC Hclose] [HT]").
- iIntros "HE'". unfold cctx_interp. iIntros (elt) "Helt".
iDestruct "Helt" as %->%elem_of_list_singleton. iIntros (ret) "Htl HL HT".
iMod ("Hclose" with "HE'") as "HE".
iSpecialize ("HC" with "HE"). unfold cctx_elt_interp.
- iApply ("HC" $! (_ â—cont(_, _)%CC) with "[%] * Htl HL >").
+ iApply ("HC" $! (_ â—cont(_, _)%CC) with "[%] Htl HL >").
{ by apply elem_of_list_singleton. }
rewrite /tctx_interp !big_sepL_singleton /=.
iDestruct "HT" as (v) "[HP Hown]". iExists v. iFrame "HP".
@@ -107,7 +107,7 @@ Section typing.
specialize (Htys x). eapply Forall2_lookup_lr in Htys; try done.
assert (Hst : subtype (E0 ++ E x) L0 (box ty2') (box ty1'))
by by rewrite ->Htys.
- iDestruct (Hst with "* [] [] []") as "(_ & #Ho & _)"; [done| |done|].
+ iDestruct (Hst with "[] [] []") as "(_ & #Ho & _)"; [done| |done|].
{ rewrite /elctx_interp_0 big_sepL_app. by iSplit. }
by iApply "Ho".
Qed.
@@ -177,7 +177,7 @@ Section typing.
wp_bind p. iApply (wp_hasty with "Hf"). iIntros (v) "% Hf".
iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = kâŒ):::
vmap (λ ty (v : val), tctx_elt_interp tid (v ◠box ty)) (tys x))%I
- with "* [Hargs]"); first wp_done.
+ with "[Hargs]"); first wp_done.
- rewrite /= big_sepL_cons. iSplitR "Hargs"; first by iApply wp_value'.
clear dependent ty k p.
rewrite /tctx_interp vec_to_list_map !zip_with_fmap_r
@@ -198,7 +198,7 @@ Section typing.
+ iIntros "HE'". iApply fupd_cctx_interp. iMod ("Hclose" with "HE'") as "[HE HL]".
iSpecialize ("HC" with "HE"). iModIntro. iIntros (y) "IN".
iDestruct "IN" as %->%elem_of_list_singleton. iIntros (args) "Htl _ Hret".
- iSpecialize ("HC" with "* []"); first by (iPureIntro; apply elem_of_list_singleton).
+ iSpecialize ("HC" with "[]"); first by (iPureIntro; apply elem_of_list_singleton).
iApply ("HC" $! args with "Htl HL").
rewrite tctx_interp_singleton tctx_interp_cons. iFrame.
+ rewrite /tctx_interp vec_to_list_map !zip_with_fmap_r
@@ -273,7 +273,7 @@ Section typing.
{ simpl. rewrite decide_left. done. }
iExists fb, _, argsb, e, _. iSplit. done. iSplit. done. iNext. clear qE.
iIntros (x k args) "!#". iIntros (tid' qE) "_ _ Htl HE HL HC HT'".
- iApply (Hbody with "* HEAP LFT Htl HE HL HC").
+ iApply (Hbody with "HEAP LFT Htl HE HL HC").
rewrite tctx_interp_cons tctx_interp_app. iFrame "HT' IH".
by iApply sendc_change_tid.
Qed.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 7f91f578..c650b359 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -256,8 +256,8 @@ Section lft_contexts.
iInduction Hκs as [|κ κs Hκ ?] "IH" forall (qE qL').
- iExists 1%Qp. iFrame. iSplitR; last by auto. iApply lft_tok_static.
- iDestruct "HL1" as "[HL1 HL2]". iDestruct "HE" as "[HE1 HE2]".
- iMod (Hκ with "* HE1 HL1") as (q') "[Htok' Hclose]". done.
- iMod ("IH" with "* HE2 HL2") as (q'') "[Htok'' Hclose']".
+ iMod (Hκ with "HE1 HL1") as (q') "[Htok' Hclose]". done.
+ iMod ("IH" with "HE2 HL2") as (q'') "[Htok'' Hclose']".
destruct (Qp_lower_bound q' q'') as (q0 & q'2 & q''2 & -> & ->).
iExists q0. rewrite -lft_tok_sep. iDestruct "Htok'" as "[$ Hr']".
iDestruct "Htok''" as "[$ Hr'']". iIntros "!>[Hκ Hfold]".
@@ -361,8 +361,8 @@ Section elctx_incl.
split.
- iIntros (???) "_ _ * ?". iExists _. iFrame. eauto.
- iIntros (x y z Hxy Hyz ??) "#HE #HL * HE1".
- iMod (Hxy with "HE HL * HE1") as (qy) "[HE1 Hclose1]"; first done.
- iMod (Hyz with "HE HL * HE1") as (qz) "[HE1 Hclose2]"; first done.
+ iMod (Hxy with "HE HL HE1") as (qy) "[HE1 Hclose1]"; first done.
+ iMod (Hyz with "HE HL HE1") as (qz) "[HE1 Hclose2]"; first done.
iModIntro. iExists qz. iFrame "HE1". iIntros "HE1".
iApply ("Hclose1" with ">"). iApply "Hclose2". done.
Qed.
@@ -381,8 +381,8 @@ Section elctx_incl.
Proof.
iIntros (?? HE1 ?? HE2 ??) "#HE #HL *". rewrite {1}/elctx_interp big_sepL_app.
iIntros "[HE1 HE2]".
- iMod (HE1 with "HE HL * HE1") as (q1) "[HE1 Hclose1]"; first done.
- iMod (HE2 with "HE HL * HE2") as (q2) "[HE2 Hclose2]"; first done.
+ iMod (HE1 with "HE HL HE1") as (q1) "[HE1 Hclose1]"; first done.
+ iMod (HE2 with "HE HL HE2") as (q2) "[HE2 Hclose2]"; first done.
destruct (Qp_lower_bound q1 q2) as (q & ? & ? & -> & ->).
iModIntro. iExists q. rewrite /elctx_interp !big_sepL_app.
iDestruct "HE1" as "[$ HE1]". iDestruct "HE2" as "[$ HE2]".
@@ -430,7 +430,7 @@ Section elctx_incl.
iDestruct (elctx_interp_persist with "HE1") as "#HE1'".
iDestruct (Hκκ' with "[HE HE1'] HL") as "#Hκκ'".
{ rewrite /elctx_interp_0 big_sepL_app. auto. }
- iMod (HE2 with "HE HL * HE1") as (qE2) "[HE2 Hclose']". done.
+ iMod (HE2 with "HE HL HE1") as (qE2) "[HE2 Hclose']". done.
iExists qE2. rewrite /elctx_interp big_sepL_cons /=. iFrame "∗#".
iIntros "!> [_ HE2']". by iApply "Hclose'".
Qed.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 343c6178..ebb7114c 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -41,6 +41,8 @@ Section own.
rewrite /= -Qcmult_plus_distr_l -Z2Qc_inj_add /Z.add. do 3 f_equal. lia.
Qed.
+ Global Opaque freeable_sz.
+
Program Definition own_ptr (n : nat) (ty : type) :=
{| ty_size := 1;
ty_own tid vl :=
@@ -90,7 +92,7 @@ Section own.
iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros "!# *% Htok".
iApply (step_fupd_mask_mono F _ _ (F∖↑shrN∖↑lftN)). set_solver. set_solver.
iMod (lft_incl_acc with "Hκ Htok") as (q') "[Htok Hclose]"; first set_solver.
- iMod ("Hvs" with "* [%] Htok") as "Hvs'". set_solver. iModIntro. iNext.
+ iMod ("Hvs" with "[%] Htok") as "Hvs'". set_solver. iModIntro. iNext.
iMod "Hvs'" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
by iApply (ty.(ty_shr_mono) with "LFT Hκ").
Qed.
@@ -99,18 +101,18 @@ Section own.
Proper (ctx_eq E L ==> subtype E L ==> subtype E L) own_ptr.
Proof.
intros n1 n2 Hn12 ty1 ty2 Hincl. iIntros. iSplit; first done.
- iDestruct (Hincl with "* [] [] []") as "(_ & #Ho & #Hs)"; [done..|clear Hincl].
+ iDestruct (Hincl with "[] [] []") as "(_ & #Ho & #Hs)"; [done..|clear Hincl].
iSplit; iAlways.
- iIntros (?[|[[| |]|][]]) "H"; try iDestruct "H" as "[]". simpl.
iDestruct "H" as "[Hmt H†]". iDestruct "Hmt" as (vl') "[Hmt Hown]". iNext.
iDestruct (ty_size_eq with "Hown") as %<-.
- iDestruct ("Ho" with "* Hown") as "Hown".
+ iDestruct ("Ho" with "Hown") as "Hown".
iDestruct (ty_size_eq with "Hown") as %<-.
iDestruct (Hn12 with "[] [] []") as %->; [done..|]. iFrame.
iExists _. by iFrame.
- iIntros (???) "H". iDestruct "H" as (l') "[Hfb #Hvs]".
iExists l'. iFrame. iIntros "!#". iIntros (F' q) "% Htok".
- iMod ("Hvs" with "* [%] Htok") as "Hvs'". done. iModIntro. iNext.
+ iMod ("Hvs" with "[%] Htok") as "Hvs'". done. iModIntro. iNext.
iMod "Hvs'" as "[Hshr $]". iApply ("Hs" with "Hshr").
Qed.
Lemma own_mono' E L n1 n2 ty1 ty2 :
@@ -148,7 +150,7 @@ Section own.
Proof.
iIntros (Hsync κ tid1 tid2 l) "H". iDestruct "H" as (l') "[Hm #Hshr]".
iExists _. iFrame "Hm". iAlways. iIntros (F q) "% Htok".
- iMod ("Hshr" with "* [] Htok") as "Hfin"; first done. iModIntro. iNext.
+ iMod ("Hshr" with "[] Htok") as "Hfin"; first done. iModIntro. iNext.
iClear "Hshr". (* FIXME: Using "{HShr} [HShr $]" for the intro pattern in the following line doesn't work. *)
iMod "Hfin" as "[Hshr $]". by iApply Hsync.
Qed.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 661380a5..6a43961e 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -80,8 +80,8 @@ Section product.
Proper (subtype E L ==> subtype E L ==> subtype E L) product2.
Proof.
iIntros (ty11 ty12 H1 ty21 ty22 H2). iIntros.
- iDestruct (H1 with "* [] [] []") as "(% & #Ho1 & #Hs1)"; [done..|]. clear H1.
- iDestruct (H2 with "* [] [] []") as "(% & #Ho2 & #Hs2)"; [done..|]. clear H2.
+ iDestruct (H1 with "[] [] []") as "(% & #Ho1 & #Hs1)"; [done..|]. clear H1.
+ iDestruct (H2 with "[] [] []") as "(% & #Ho2 & #Hs2)"; [done..|]. clear H2.
iSplit; first by (iPureIntro; simpl; f_equal). iSplit; iAlways.
- iIntros (??) "H". iDestruct "H" as (vl1 vl2) "(% & Hown1 & Hown2)".
iExists _, _. iSplit. done. iSplitL "Hown1".
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index a47facfe..825605e6 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -46,7 +46,7 @@ Section product_split.
iDestruct (Hloc with "Hty") as %[l [=->]].
iAssert (tctx_elt_interp tid (p +â‚— #0 â— ptr ty)) with "[Hty]" as "$".
{ iExists #l. iSplit; last done. simpl; by rewrite Hp shift_loc_0. }
- iMod ("IH" with "* HE HL [Htyl]") as "($ & $ & Htyl)".
+ iMod ("IH" with "HE HL [Htyl]") as "($ & $ & Htyl)".
{ rewrite tctx_interp_singleton //. }
iClear "IH". rewrite (hasty_ptr_offsets_offset l) // -plus_n_O //.
Qed.
@@ -74,7 +74,7 @@ Section product_split.
assert (eqtype E L (ptr ty) (ptr (product2 ty unit))) as [Hincl _].
{ rewrite right_id. done. }
iDestruct (Hincl with "LFT HE' HL'") as "#(_ & #Heq & _)". by iApply "Heq". }
- iMod ("IH" with "* [] HE HL [Htyl]") as "(HE & HL & Htyl)"; first done.
+ iMod ("IH" with "[] HE HL [Htyl]") as "(HE & HL & Htyl)"; first done.
{ change (ty_size ty) with (0+ty_size ty)%nat at 1.
rewrite plus_comm -hasty_ptr_offsets_offset //. }
iClear "IH". iMod (Hmerge with "LFT HE HL [Hty Htyl]") as "($ & $ & ?)";
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index acd60687..b0b14236 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -183,12 +183,12 @@ Section typing_rules.
rewrite tctx_interp_cons tctx_interp_singleton. iIntros "[Hp1 Hp2]".
wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "% Hown1".
wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "_ Hown2".
- iMod (Hwrt with "* [] LFT HE HL Hown1") as (l vl) "([% %] & Hl & Hclose)"; first done.
+ iMod (Hwrt with "[] LFT HE HL Hown1") as (l vl) "([% %] & Hl & Hclose)"; first done.
subst v1. iDestruct (ty_size_eq with "Hown2") as "#Hsz". iDestruct "Hsz" as %Hsz.
rewrite <-Hsz in *. destruct vl as [|v[|]]; try done.
rewrite heap_mapsto_vec_singleton. iApply wp_fupd. wp_write.
rewrite -heap_mapsto_vec_singleton.
- iMod ("Hclose" with "* [Hl Hown2]") as "($ & $ & Hown)".
+ iMod ("Hclose" with "[Hl Hown2]") as "($ & $ & Hown)".
{ iExists _. iFrame. }
rewrite tctx_interp_singleton tctx_hasty_val' //.
Qed.
@@ -208,7 +208,7 @@ Section typing_rules.
iIntros (Hsz Hread) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL Hp".
rewrite tctx_interp_singleton. wp_bind p. iApply (wp_hasty with "Hp").
iIntros (v) "% Hown".
- iMod (Hread with "* [] LFT Htl HE HL Hown") as
+ iMod (Hread with "[] LFT Htl HE HL Hown") as
(l vl q) "(% & Hl & Hown & Hclose)"; first done.
subst v. iDestruct (ty_size_eq with "Hown") as "#>%". rewrite ->Hsz in *.
destruct vl as [|v [|]]; try done.
@@ -242,9 +242,9 @@ Section typing_rules.
iIntros (Φ) "(#HEAP & #LFT & Htl & [HE1 HE2] & [HL1 HL2] & [Hp1 Hp2]) HΦ".
wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "% Hown1".
wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "% Hown2".
- iMod ("Hwrt" with "* [] LFT HE1 HL1 Hown1")
+ iMod ("Hwrt" with "[] LFT HE1 HL1 Hown1")
as (l1 vl1) "([% %] & Hl1 & Hcl1)"; first done.
- iMod ("Hread" with "* [] LFT Htl HE2 HL2 Hown2")
+ iMod ("Hread" with "[] LFT Htl HE2 HL2 Hown2")
as (l2 vl2 q2) "(% & Hl2 & Hown2 & Hcl2)"; first done.
iDestruct (ty_size_eq with "Hown2") as "#>%". subst v1 v2. iApply wp_fupd.
iApply (wp_memcpy with "[$HEAP $Hl1 $Hl2]"); first done; try congruence; [].
@@ -261,7 +261,7 @@ Section typing_rules.
(λ _, [p1 ◠ty1'; p2 ◠ty2']%TC).
Proof.
iIntros (Hsz Hwrt Hread) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HT".
- iApply (type_memcpy_iris with "[] [] * [$HEAP $LFT $Htl $HE $HL HT]"); try done.
+ iApply (type_memcpy_iris with "[] [] [$HEAP $LFT $Htl $HE $HL HT]"); try done.
(* TODO: This is kind of silly, why can't I iApply the assumptions directly? *)
{ iPoseProof Hwrt as "Hwrt". done. }
{ iPoseProof Hread as "Hread". done. }
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 6e92e902..a0c649a9 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -24,7 +24,7 @@ Section shr_bor.
intros κ1 κ2 Hκ ty1 ty2 Hty. apply subtype_simple_type.
iIntros (? [|[[]|][]]) "#LFT #HE #HL H"; try iDestruct "H" as "[]".
iDestruct (Hκ with "HE HL") as "#Hκ". iApply (ty2.(ty_shr_mono) with "LFT Hκ").
- iDestruct (Hty with "* [] [] []") as "(_ & _ & #Hs1)"; [done..|clear Hty].
+ iDestruct (Hty with "[] [] []") as "(_ & _ & #Hs1)"; [done..|clear Hty].
by iApply "Hs1".
Qed.
Global Instance shr_mono_flip E L :
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 502f7efc..d67353e0 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -40,7 +40,7 @@ Section type_soundness.
iIntros "!# #HEAP". iMod lft_init as (?) "#LFT". done.
iMod na_alloc as (tid) "Htl". set (Htype := TypeG _ _ _ _ _).
wp_bind (of_val main). iApply (wp_wand with "[Htl]").
- iApply (Hmain _ $! tid 1%Qp with "* HEAP LFT Htl [] [] []").
+ iApply (Hmain _ $! tid 1%Qp with "HEAP LFT Htl [] [] []").
{ by rewrite /elctx_interp big_sepL_nil. }
{ by rewrite /llctx_interp big_sepL_nil. }
{ by rewrite tctx_interp_nil. }
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index af2abac3..0c28c7f3 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -131,7 +131,7 @@ Section sum.
by erewrite <-Forall2_length. }
edestruct @Forall2_lookup_l as (ty2 & Hl2 & Hty2); [done..|].
rewrite (nth_lookup_Some tyl2 _ _ ty2) //.
- by iApply (Hty2 with "* [] []"). }
+ by iApply (Hty2 with "[] []"). }
clear -Hleq. iSplit; last iSplit.
- simpl. by rewrite Hleq.
- iAlways. iIntros (tid vl) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
diff --git a/theories/typing/type.v b/theories/typing/type.v
index e2114448..6a45388f 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -448,10 +448,10 @@ Section subtyping.
subtype st1 st2.
Proof.
intros Hst. iIntros. iSplit; first done. iSplit; iAlways.
- - iIntros. iApply (Hst with "* [] [] []"); done.
+ - iIntros. iApply (Hst with "[] [] []"); done.
- iIntros (???) "H".
iDestruct "H" as (vl) "[Hf Hown]". iExists vl. iFrame "Hf".
- by iApply (Hst with "* [] [] []").
+ by iApply (Hst with "[] [] []").
Qed.
End subtyping.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 824d0bde..b84b52da 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -112,7 +112,7 @@ Section type_context.
Proof.
iIntros "Hty HΦ". iDestruct "Hty" as (v) "[% Hown]".
iApply (wp_wand with "[]"). { iApply wp_eval_path. done. }
- iIntros (v') "%". subst v'. iApply ("HΦ" with "* [] Hown"). by auto.
+ iIntros (v') "%". subst v'. iApply ("HΦ" with "[] Hown"). by auto.
Qed.
Lemma closed_hasty tid p ty : tctx_elt_interp tid (p â— ty) -∗ ⌜Closed [] pâŒ.
@@ -243,8 +243,7 @@ Section type_context.
iDestruct (elctx_interp_persist with "HE") as "#HE'".
iDestruct (llctx_interp_persist with "HL") as "#HL'".
iFrame "HE HL". iDestruct "H" as (v) "[% H]". iExists _. iFrame "%".
- iDestruct (Hst with "* [] [] []") as "(_ & #Ho & _)"; [done..|].
- iApply ("Ho" with "*"). done.
+ iDestruct (Hst with "[] [] []") as "(_ & #Ho & _)"; [done..|by iApply "Ho"].
Qed.
(* Extracting from a type context. *)
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 92828b31..e08e89b7 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -39,10 +39,8 @@ Section case.
+ iFrame. iExists _. iFrame.
+ rewrite -EQlen app_length minus_plus -(shift_loc_assoc_nat _ 1).
iFrame. iExists _. iFrame. rewrite uninit_own. auto.
- - assert (EQf:=freeable_sz_split n 1). simpl in EQf. rewrite -EQf. clear EQf.
- rewrite -EQlen app_length -freeable_sz_split. iFrame.
- iExists (#i :: vl' ++ vl''). iNext.
- rewrite heap_mapsto_vec_cons heap_mapsto_vec_app.
+ - rewrite -EQlen app_length -(Nat.add_1_l (_+_)) -!freeable_sz_split. iFrame.
+ iExists (#i :: vl' ++ vl''). iNext. rewrite heap_mapsto_vec_cons heap_mapsto_vec_app.
iFrame. iExists i, vl', vl''. rewrite /= app_length nth_lookup EQty. auto.
Qed.
@@ -90,7 +88,7 @@ Section case.
iMod ("Hclose" with "Htok") as "[HE HL]".
iApply (Hety with "HEAP LFT Hna HE HL HC").
rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //. iFrame.
- - iMod ("Hclose'" with "* [H↦i H↦vl' H↦vl'' Hown] []") as "[Hb Htok]";
+ - iMod ("Hclose'" with "[H↦i H↦vl' H↦vl'' Hown] []") as "[Hb Htok]";
[|by iIntros "!>$"|].
{ iExists (#i::vl'++vl'').
rewrite heap_mapsto_vec_cons heap_mapsto_vec_app -EQlen. iFrame. iNext.
@@ -153,7 +151,7 @@ Section case.
iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
iApply (wp_hasty with "Hp1"). iIntros (v1 Hv1) "Hty1".
- iMod (Hw with "* [] LFT HE HL Hty1") as (l vl) "(H & H↦ & Hw)"=>//=.
+ iMod (Hw with "[] LFT HE HL Hty1") as (l vl) "(H & H↦ & Hw)"=>//=.
destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl]".
wp_write. wp_bind p1. iApply (wp_wand with "[]"); first by iApply (wp_eval_path).
@@ -189,7 +187,7 @@ Section case.
Proof.
iIntros (Hty Hw) "!# * #HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hty".
- iMod (Hw with "* [] LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)". done.
+ iMod (Hw with "[] LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)". done.
simpl. destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
rewrite heap_mapsto_vec_cons -wp_fupd. iDestruct "H↦" as "[H↦0 H↦vl]".
wp_write. rewrite tctx_interp_singleton tctx_hasty_val' //.
@@ -222,12 +220,12 @@ Section case.
iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
iApply (wp_hasty with "Hp1"). iIntros (v1 Hv1) "Hty1".
- iMod (Hw with "* [] LFT HE1 HL1 Hty1") as (l1 vl1) "(H & H↦ & Hw)"=>//=.
+ iMod (Hw with "[] LFT HE1 HL1 Hty1") as (l1 vl1) "(H & H↦ & Hw)"=>//=.
destruct vl1 as [|? vl1]; iDestruct "H" as %[[= Hlen] ->].
rewrite heap_mapsto_vec_cons -wp_fupd. iDestruct "H↦" as "[H↦0 H↦vl1]". wp_write.
wp_bind p1. iApply (wp_wand with "[]"); first by iApply (wp_eval_path). iIntros (? ->).
wp_op. wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2 Hv2) "Hty2".
- iMod (Hr with "* [] LFT Htl HE2 HL2 Hty2") as (l2 vl2 q) "(% & H↦2 & Hty & Hr)"=>//=.
+ iMod (Hr with "[] LFT Htl HE2 HL2 Hty2") as (l2 vl2 q) "(% & H↦2 & Hty & Hr)"=>//=.
subst. assert (ty.(ty_size) ≤ length vl1).
{ revert i Hty. rewrite Hlen. clear. induction tyl=>//= -[|i] /=.
- intros [= ->]. lia.
@@ -247,7 +245,7 @@ Section case.
- iExists _. iFrame.
Qed.
- Lemma type_sum_assign_memcpy {E L} tyl i ty1 ty2 ty n ty1' ty2' C T T' p1 p2 e:
+ Lemma type_sum_memcpy {E L} tyl i ty1 ty2 ty n ty1' ty2' C T T' p1 p2 e:
Closed [] e →
0 ≤ i →
tctx_extract_ctx E L [p1 ◠ty1; p2 ◠ty2] T T' →
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 8680f75d..c8825792 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -52,7 +52,7 @@ Section uniq_bor.
iIntros "!# * % Htok".
iApply (step_fupd_mask_mono F _ _ (F∖↑shrN∖↑lftN)); try set_solver.
iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]"; first set_solver.
- iMod ("Hvs" with "* [%] Htok") as "Hvs'". set_solver. iModIntro. iNext.
+ iMod ("Hvs" with "[%] Htok") as "Hvs'". set_solver. iModIntro. iNext.
iMod "Hvs'" as "[#Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
by iApply (ty_shr_mono with "LFT Hκ0").
Qed.
@@ -61,7 +61,7 @@ Section uniq_bor.
Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) uniq_bor.
Proof.
intros κ1 κ2 Hκ ty1 ty2 Hty%eqtype_unfold. iIntros. iSplit; first done.
- iDestruct (Hty with "* [] [] []") as "(_ & #Ho & #Hs)"; [done..|clear Hty].
+ iDestruct (Hty with "[] [] []") as "(_ & #Ho & #Hs)"; [done..|clear Hty].
iDestruct (Hκ with "[] []") as "#Hκ"; [done..|]. iSplit; iAlways.
- iIntros (? [|[[]|][]]) "H"; try iDestruct "H" as "[]".
iApply (bor_shorten with "Hκ"). iApply bor_iff_proper; last done.
@@ -71,7 +71,7 @@ Section uniq_bor.
{ iApply lft_glb_mono. done. iApply lft_incl_refl. }
iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'. iIntros "{$Hbor}!# %%% Htok".
iMod (lft_incl_acc with "Hincl' Htok") as (q') "[Htok Hclose]"; first set_solver.
- iMod ("Hupd" with "* [%] Htok") as "Hupd'"; try done. iModIntro. iNext.
+ iMod ("Hupd" with "[%] Htok") as "Hupd'"; try done. iModIntro. iNext.
iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
iApply ty_shr_mono; [done..|]. by iApply "Hs".
Qed.
@@ -105,7 +105,7 @@ Section uniq_bor.
Proof.
iIntros (Hsync κ' tid1 tid2 l) "H". iDestruct "H" as (l') "[Hm #Hshr]".
iExists l'. iFrame "Hm". iAlways. iIntros (F q) "% Htok".
- iMod ("Hshr" with "* [] Htok") as "Hfin"; first done. iClear "Hshr".
+ iMod ("Hshr" with "[] Htok") as "Hfin"; first done. iClear "Hshr".
iModIntro. iNext. iMod "Hfin" as "[Hshr $]". iApply Hsync. done.
Qed.
End uniq_bor.
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index 240459f6..efa1bb6f 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -88,8 +88,7 @@ Section typing.
iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
Qed.
- (* Same for the other direction.
- FIXME : this does not exist in Rust.*)
+ (* The other direction: getting ownership out of a cell. *)
Definition cell_into_inner : val := funrec: <> ["x"] := "return" ["x"].
Lemma cell_into_inner_type ty :
@@ -101,6 +100,19 @@ Section typing.
iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
Qed.
+ Definition cell_get_mut : val :=
+ funrec: <> ["x"] := "return" ["x"].
+
+ Lemma cell_get_mut_type `(!Copy ty) :
+ typed_instruction_ty [] [] [] cell_get_mut
+ (fn (λ α, [☀α])%EL (λ α, [# &uniq{α} (cell ty)])%T (λ α, &uniq{α} ty)%T).
+ Proof.
+ apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
+ eapply (type_jump [_]). solve_typing. rewrite /tctx_incl /=.
+ iIntros (???) "_ $$". rewrite !tctx_interp_singleton /tctx_elt_interp /=.
+ by iIntros "$".
+ Qed.
+
(* Reading from a cell *)
Definition cell_get ty : val :=
funrec: <> ["x"] :=
@@ -162,20 +174,6 @@ Section typing.
eapply type_delete; [solve_typing..|].
eapply (type_jump [_]); solve_typing.
Qed.
-
- (* Reading from a cell *)
- Definition cell_get_mut : val :=
- funrec: <> ["x"] := "return" ["x"].
-
- Lemma cell_get_mut_type `(!Copy ty) :
- typed_instruction_ty [] [] [] cell_get_mut
- (fn (λ α, [☀α])%EL (λ α, [# &uniq{α} (cell ty)])%T (λ α, &uniq{α} ty)%T).
- Proof.
- apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
- eapply (type_jump [_]). solve_typing. rewrite /tctx_incl /=.
- iIntros (???) "_ $$". rewrite !tctx_interp_singleton /tctx_elt_interp /=.
- by iIntros "$".
- Qed.
End typing.
Hint Resolve cell_mono' cell_proper' : lrust_typing.
diff --git a/theories/typing/unsafe/refcell.v b/theories/typing/unsafe/refcell.v
index 52682739..d3757007 100644
--- a/theories/typing/unsafe/refcell.v
+++ b/theories/typing/unsafe/refcell.v
@@ -1,3 +1,4 @@
+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.
@@ -33,10 +34,10 @@ Section refcell_inv.
(∃ st, l ↦ #(Z_of_refcell_st st) ∗ own γ (◠st) ∗
match st return _ with
| None => &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)
- | Some (Cinr ({|agree_car := ν|}, q, n)) =>
- ∃ q', ⌜(q + q')%Qp = 1%Qp⌠∗ q'.[ν] ∗
- ty.(ty_shr) (α ∪ ν) tid (shift_loc l 1) ∗
- ([†ν] ={lftE}=∗ &{α}(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
end)%I.
@@ -44,7 +45,7 @@ Section refcell_inv.
Proper (dist n ==> dist n) (refcell_inv tid l γ α).
Proof.
intros ty1 ty2 Hty. unfold refcell_inv.
- repeat (f_contractive || f_equiv || apply Hty).
+ repeat (f_contractive || f_equiv || apply Hty || apply dist_S).
Qed.
Lemma refcell_inv_proper E L tid l γ α1 α2 ty1 ty2 :
@@ -63,12 +64,14 @@ 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 [[|[[]]|]|]; try done;
last by iApply "Hb".
- iDestruct "H" as (q') "(Heq & Htok & Hs & H†)". iExists q'. iFrame. iSplitL "Hs".
+ iDestruct "H" as (q' ν) "(Hag & Heq & Htok & Hs & Hh)". iExists q', ν.
+ iFrame. iSplitL "Hs".
- iApply (ty_shr_mono); first done; last by iApply "Hshr".
by iApply lft_glb_mono; [iApply Hα|iApply lft_incl_refl].
- - iIntros "?". iApply ("Hb" with ">"). by iApply "H†".
+ - iIntros "H†". iMod ("Hh" with "H†") as "Hh". iModIntro. iNext. iMod "Hh".
+ by iApply "Hb".
Qed.
End refcell_inv.
@@ -104,29 +107,26 @@ Section refcell.
iMod (bor_acc_cons with "LFT Hn Htok") as "[H Hclose]". done.
iAssert ((q / 2).[κ] ∗ ▷ ∃ γ, refcell_inv tid l γ κ ty)%I with ">[-Hclose]"
as "[$ HQ]"; last first.
- { iMod ("Hclose" with "* HQ []") as "[Hb $]".
+ { iMod ("Hclose" with "HQ []") as "[Hb $]".
- iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(? & _ & _)".
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] _]". done.
+ - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
iMod (own_alloc
(◠Some (Cinr (to_agree (ν : leibnizC _), (1/2)%Qp, n)))) as (γ) "Hst".
{ by apply auth_auth_valid. }
- destruct (Qp_lower_bound (1/2) (q/2)) as (q' & q1 & q2 & H12 & ->). rewrite H12.
- iDestruct "Htok'" as "[Htok' $]". iDestruct "Htok1" as "[Htok1 Htok1']".
- iApply (fupd_mask_mono lftE). done.
iMod (rebor _ _ (κ ∪ ν) with "LFT [] Hvl") as "[Hvl Hh]". done.
{ iApply lft_le_incl. apply gmultiset_union_subseteq_l. }
- iMod (ty_share _ _ (κ ∪ ν) _ _ q' with "LFT Hvl [Htok' Htok1]")
- as "[Hshr Htok]". done.
- { rewrite -lft_tok_sep. iFrame. }
- rewrite -lft_tok_sep. iDestruct "Htok" as "[$ Htok]".
- iExists γ, _. iFrame "Hst Hn". iExists _. iIntros "{$Htok2 $Hshr}!>!>".
- rewrite -H12 Qp_div_2. iSplit; first done. iIntros "H†". iApply "Hh".
- rewrite -lft_dead_or. auto.
+ 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ν".
+ 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.
@@ -274,8 +274,6 @@ Section ref.
Proof. intros. by eapply ref_proper. Qed.
End ref.
-Definition refcell_refmutN := refcellN .@ "refmut".
-
Section refmut.
Context `{typeG Σ, refcellG Σ}.
Local Hint Extern 1000 (_ ⊆ _) => set_solver : ndisj.
@@ -334,7 +332,7 @@ Section refmut.
- iIntros "!# * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]". set_solver.
{ iApply lft_glb_mono. iApply lft_incl_refl. done. }
- iMod ("H" with "* [] Htok") as "Hshr". done. iModIntro. iNext.
+ iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
iApply ty_shr_mono; try done. iApply lft_glb_mono. iApply lft_incl_refl. done.
Qed.
@@ -368,7 +366,7 @@ Section refmut.
iDestruct "H" as "[$ #H]". iIntros "!# * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]". set_solver.
{ iApply lft_glb_mono. done. iApply lft_incl_refl. }
- iMod ("H" with "* [] Htok") as "Hshr". done. iModIntro. iNext.
+ iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
iApply ty_shr_mono; try done. iApply lft_glb_mono. done. iApply lft_incl_refl.
by iApply "Hs".
@@ -405,32 +403,33 @@ Section refcell_functions.
Lemma refcell_new_type ty :
typed_instruction_ty [] [] [] (refcell_new ty)
- (fn (λ _, [])%EL (λ _, [# ty]) (λ _:(), refcell ty)).
+ (fn (λ _, []) (λ _, [# ty]) (λ _:(), refcell ty)).
Proof.
apply type_fn; [apply _..|]. move=>/= _ ret arg. inv_vec arg=>x. simpl_subst.
eapply type_new; [solve_typing..|].
iIntros (r) "!# * #HEAP #LFT Hna HE HL Hk HT". simpl_subst.
rewrite (Nat2Z.id (S ty.(ty_size))) tctx_interp_cons
tctx_interp_singleton !tctx_hasty_val.
- rewrite cctx_interp_singleton. iDestruct ("Hk" with "HE") as "Hret".
iDestruct "HT" as "[Hr Hx]".
- destruct x as [[]|]; try iDestruct "Hx" as "[]". iDestruct "Hx" as "[Hx Hx†]".
+ destruct x as [[|lx|]|]; try iDestruct "Hx" as "[]". iDestruct "Hx" as "[Hx Hx†]".
iDestruct "Hx" as (vl) "[Hx↦ Hx]".
- destruct r as [[]|]; try iDestruct "Hr" as "[]". iDestruct "Hr" as "[Hr Hr†]".
- iDestruct "Hr" as (vl') "Hr". rewrite uninit_own. iDestruct "Hr" as "[Hr↦ >SZ]".
- destruct vl' as [|]; iDestruct "SZ" as %[=]. rewrite heap_mapsto_vec_cons.
- iDestruct "Hr↦" as "[Hr↦0 Hr↦1]". wp_op. rewrite shift_loc_0. wp_write. wp_op.
- iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
+ destruct r as [[|lr|]|]; try iDestruct "Hr" as "[]". iDestruct "Hr" as "[Hr Hr†]".
+ iDestruct "Hr" as (vl') "Hr". rewrite uninit_own.
+ iDestruct "Hr" as "[Hr↦ >SZ]". destruct vl' as [|]; iDestruct "SZ" as %[=].
+ rewrite heap_mapsto_vec_cons. iDestruct "Hr↦" as "[Hr↦0 Hr↦1]". wp_op.
+ rewrite shift_loc_0. wp_write. wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
wp_bind (_ <-{_} !_)%E. iApply (wp_memcpy with "[$HEAP $Hr↦1 $Hx↦]"); [done..|].
- iIntros "!> [Hr↦1 Hx↦]". wp_seq. wp_bind (delete _).
- rewrite freeable_sz_full. iApply (wp_delete with "[$HEAP $Hx↦ Hx†]"); [by auto..| |].
- { by rewrite Hsz. }
- iIntros "!>_". wp_seq. iApply ("Hret" $! [# #_] with "Hna HL").
- rewrite tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
- iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame "Hr↦0 ∗". auto.
+ iIntros "!> [Hr↦1 Hx↦]". wp_seq.
+ iApply (type_delete _ _ [ #lx â— box (uninit (ty_size ty)); #lr â— box (refcell ty)]%TC
+ with "HEAP LFT Hna HE HL Hk [-]"); [solve_typing..| |]; last first.
+ { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
+ iSplitL "Hx↦".
+ - iExists _. rewrite uninit_own. auto.
+ - iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. auto. }
+ eapply (type_jump [ #_]); solve_typing.
Qed.
- (* The other direction. *)
+ (* The other direction: getting ownership out of a refcell. *)
Definition refcell_into_inner ty : val :=
funrec: <> ["x"] :=
let: "r" := new [ #ty.(ty_size)] in
@@ -439,29 +438,241 @@ Section refcell_functions.
Lemma refcell_into_inner_type ty :
typed_instruction_ty [] [] [] (refcell_into_inner ty)
- (fn (λ _, [])%EL (λ _, [# refcell ty]) (λ _:(), ty)).
+ (fn (λ _, []) (λ _, [# refcell ty]) (λ _:(), ty)).
Proof.
apply type_fn; [apply _..|]. move=>/= _ ret arg. inv_vec arg=>x. simpl_subst.
eapply type_new; [solve_typing..|].
iIntros (r) "!# * #HEAP #LFT Hna HE HL Hk HT". simpl_subst.
rewrite (Nat2Z.id (ty.(ty_size))) tctx_interp_cons
tctx_interp_singleton !tctx_hasty_val.
- rewrite cctx_interp_singleton. iDestruct ("Hk" with "HE") as "Hret".
- iDestruct "HT" as "[Hr Hx]". destruct x as [[]|]; try iDestruct "Hx" as "[]".
- iDestruct "Hx" as "[Hx Hx†]". rewrite freeable_sz_full.
+ iDestruct "HT" as "[Hr Hx]". destruct x as [[|lx|]|]; try iDestruct "Hx" as "[]".
+ iDestruct "Hx" as "[Hx Hx†]".
iDestruct "Hx" as ([|[[]|]vl]) "[Hx↦ Hx]"; try iDestruct "Hx" as ">[]".
- destruct r as [[]|]; try iDestruct "Hr" as "[]". iDestruct "Hr" as "[Hr Hr†]".
- iDestruct "Hr" as (vl') "Hr". rewrite freeable_sz_full uninit_own heap_mapsto_vec_cons.
+ destruct r as [[|lr|]|]; try iDestruct "Hr" as "[]". iDestruct "Hr" as "[Hr Hr†]".
+ iDestruct "Hr" as (vl') "Hr". rewrite uninit_own heap_mapsto_vec_cons.
iDestruct "Hr" as "[Hr↦ >%]". iDestruct "Hx↦" as "[Hx↦0 Hx↦1]". wp_op.
iDestruct "Hx" as "[% Hx]". iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
wp_bind (_ <-{_} !_)%E. iApply (wp_memcpy with "[$HEAP $Hr↦ $Hx↦1]"); [done..|].
- iIntros "!> [Hr↦ Hx↦1]". wp_seq. wp_bind (delete _).
- iApply (wp_delete _ _ _ (_::_) with "[$HEAP Hx↦0 Hx↦1 Hx†]").
- done. { by rewrite -Hsz. } { rewrite heap_mapsto_vec_cons -Hsz. iFrame. }
- iIntros "!>_". wp_seq. iApply ("Hret" $! [# #_] with "Hna HL").
- rewrite tctx_interp_singleton !tctx_hasty_val' //=. rewrite /= freeable_sz_full.
- iFrame. iExists _. iFrame.
+ iIntros "!> [Hr↦ Hx↦1]". wp_seq.
+ iApply (type_delete _ _ [ #lx â— box (uninit (S (ty_size ty))); #lr â— box ty]%TC
+ with "HEAP LFT Hna HE HL Hk [-]"); [solve_typing..| |]; last first.
+ { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
+ iSplitR "Hr↦ Hx".
+ - iExists (_::_). rewrite heap_mapsto_vec_cons uninit_own -Hsz. iFrame. auto.
+ - iExists vl. iFrame. }
+ eapply (type_jump [ #_]); solve_typing.
+ Qed.
+
+ Definition refcell_get_mut : val :=
+ funrec: <> ["x"] :=
+ let: "x'" := !"x" in
+ "x" <- "x'" +â‚— #1;;
+ "return" ["x"].
+
+ Lemma refcell_get_mut_type ty :
+ typed_instruction_ty [] [] [] refcell_get_mut
+ (fn (λ α, [☀α])%EL (λ α, [# &uniq{α} (refcell ty)])%T (λ α, &uniq{α} ty)%T).
+ Proof.
+ apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
+ eapply type_deref; [solve_typing..|by eapply read_own_move|done|]=>x'. simpl_subst.
+ iIntros "!# * #HEAP #LFT Hna HE HL HC HT".
+ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+ iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try iDestruct "Hx'" as "[]".
+ iAssert (&{α} (∃ (z : Z), lx' ↦ #z ∗ ⌜-1 ≤ zâŒ) ∗
+ (&uniq{α} ty).(ty_own) tid [ #(shift_loc lx' 1)])%I with ">[Hx']" as "[_ Hx']".
+ { iApply bor_sep; [done..|]. iApply (bor_proper with "Hx'"). iSplit.
+ - iIntros "[H1 H2]". iDestruct "H1" as (z) "[??]". iDestruct "H2" as (vl) "[??]".
+ iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. iFrame.
+ - iIntros "H". iDestruct "H" as ([|[[| |z]|]vl]) "[H↦ H]"; try iDestruct "H" as "[]".
+ rewrite heap_mapsto_vec_cons.
+ iDestruct "H" as "[H1 H2]". iDestruct "H↦" as "[H↦1 H↦2]".
+ iSplitL "H1 H↦1"; eauto. iExists _. iFrame. }
+ destruct x as [[|lx|]|]; try iDestruct "Hx" as "[]". iDestruct "Hx" as "[Hx Hx†]".
+ iDestruct "Hx" as (vl) "[Hx↦ Hx]". rewrite uninit_own. wp_op.
+ iApply (type_assign _ _ _ _
+ [ #lx ◠box (uninit 1); #(shift_loc lx' 1) ◠&uniq{α}ty]%TC
+ with "HEAP LFT Hna HE HL HC [-]");
+ [solve_typing..|by apply write_own| |]; last first.
+ { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
+ iNext. iExists _. rewrite uninit_own. iFrame. }
+ eapply (type_jump [ #_]); solve_typing.
+ Qed.
+
+ (* Shared borrowing. *)
+ Definition refcell_try_borrow : val :=
+ funrec: <> ["x"] :=
+ let: "r" := new [ #3 ] in
+ let: "x'" := !"x" in
+ let: "n" := !"x'" in
+ if: "n" ≤ #-1 then
+ "r" <-{Σ 1} ();;
+ "k" ["r"]
+ else
+ "x'" <- "n" + #1;;
+ let: "ref" := new [ #2 ] in
+ "ref" <- "x'" +â‚— #1;;
+ "ref" +â‚— #1 <- "x'";;
+ "r" <-{2,Σ 0} !"ref";;
+ delete [ #2; "ref"];;
+ "k" ["r"]
+ cont: "k" ["r"] :=
+ delete [ #1; "x"];; "return" ["r"].
+
+ Lemma refcell_try_borrow_type ty :
+ typed_instruction_ty [] [] [] refcell_try_borrow
+ (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, Σ[ref α ty; unit])%T).
+ Proof.
+ apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
+ eapply (type_cont [_] [] (λ r, [x ◠box (&shr{α} refcell ty);
+ r!!!0 ◠box Σ[ref α ty; unit]])%TC);
+ [solve_typing..|intros k|move=>/= k arg; inv_vec arg=>r]; simpl_subst; last first.
+ { eapply type_delete; [solve_typing..|].
+ eapply (type_jump [_]); solve_typing. }
+ eapply type_new; [solve_typing..|]=>r. simpl_subst.
+ eapply type_deref; [solve_typing..|apply read_own_copy, _|done|].
+ iIntros (x') "!# * #HEAP #LFT Hna HE HL Hk HT". simpl_subst.
+ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+ iDestruct "HT" as "(Hx & Hx' & Hr)".
+ destruct x' as [[|lx|]|]; try iDestruct "Hx'" as "[]".
+ iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
+ rewrite {1}/elctx_interp big_sepL_singleton.
+ iMod (lft_incl_acc with "Hαβ HE") as (qβ) "[[Hβtok1 Hβtok2] Hclose]". done.
+ iMod (na_bor_acc with "LFT Hinv Hβtok1 Hna") as "(INV & Hna & Hclose')"; try done.
+ iDestruct "INV" as (st) "(Hlx & Hownst & Hst)". wp_read. wp_let. wp_op=>?; wp_if.
+ - iMod ("Hclose'" with "[Hlx Hownst Hst] Hna") as "[Hβtok1 Hna]";
+ first by iExists st; iFrame.
+ iAssert (elctx_interp [☀α] qE)%I with ">[Hclose Hβtok1 Hβtok2]" as "HE".
+ { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
+ iApply (type_sum_assign_unit [ref α ty; unit] _ _ _ _
+ [ x ◠box (&shr{α}(refcell ty)); r ◠box (uninit 3) ]%TC
+ with "HEAP LFT Hna HE HL Hk");
+ [solve_typing..|by eapply write_own|done| |]; first last.
+ { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
+ simpl. eapply (type_jump [_]); solve_typing.
+ - wp_op. 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.
+ iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
+ ty_shr ty (β ∪ ν) tid (shift_loc lx 1) ∗
+ own γ (◯ reading_st qν ν) ∗ 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†)".
+ 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|].
+ - 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.
+ - 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 ν)).
+ rewrite right_id. iExists _, _. iFrame "Htok1 Hreading".
+ iDestruct (lft_glb_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
+ iMod (rebor _ _ (β ∪ ν) with "LFT [] Hst") as "[Hst Hh]". done.
+ { 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. }
+ 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. }
+ iApply (type_sum_memcpy [ref α ty; unit] _ _ _ _ _ _ _ _
+ [ x ◠box (&shr{α}(refcell ty)); r ◠box (uninit 3); #lref ◠box (ref α ty)]%TC
+ with "HEAP LFT Hna HE HL Hk");
+ [solve_typing..|by eapply write_own|by eapply read_own_move|done|done| |];
+ first last.
+ { 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 "∗#". iApply ty_shr_mono; try by auto.
+ iApply lft_glb_mono. done. iApply lft_incl_refl. }
+ simpl. eapply type_delete; [solve_typing..|]. eapply (type_jump [_]); solve_typing.
Qed.
+ (* Unique borrowing. *)
+ Definition refcell_try_borrow_mut : val :=
+ funrec: <> ["x"] :=
+ let: "r" := new [ #3 ] in
+ let: "x'" := !"x" in
+ let: "n" := !"x'" in
+ if: "n" = #0 then
+ "x'" <- #(-1);;
+ let: "ref" := new [ #2 ] in
+ "ref" <- "x'" +â‚— #1;;
+ "ref" +â‚— #1 <- "x'";;
+ "r" <-{2,Σ 0} !"ref";;
+ delete [ #2; "ref"];;
+ "k" ["r"]
+ else
+ "r" <-{Σ 1} ();;
+ "k" ["r"]
+ cont: "k" ["r"] :=
+ delete [ #1; "x"];; "return" ["r"].
+ Lemma refcell_try_borrow_mut_type ty :
+ typed_instruction_ty [] [] [] refcell_try_borrow_mut
+ (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, Σ[refmut α ty; unit])%T).
+ Proof.
+ apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
+ eapply (type_cont [_] [] (λ r, [x ◠box (&shr{α} refcell ty);
+ r!!!0 ◠box Σ[refmut α ty; unit]])%TC);
+ [solve_typing..|intros k|move=>/= k arg; inv_vec arg=>r]; simpl_subst; last first.
+ { eapply type_delete; [solve_typing..|].
+ eapply (type_jump [_]); solve_typing. }
+ eapply type_new; [solve_typing..|]=>r. simpl_subst.
+ eapply type_deref; [solve_typing..|apply read_own_copy, _|done|].
+ iIntros (x') "!# * #HEAP #LFT Hna HE HL Hk HT". simpl_subst.
+ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+ iDestruct "HT" as "(Hx & Hx' & Hr)".
+ destruct x' as [[|lx|]|]; try iDestruct "Hx'" as "[]".
+ iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
+ rewrite {1}/elctx_interp big_sepL_singleton.
+ iMod (lft_incl_acc with "Hαβ HE") as (qβ) "[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.
+ - 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.
+ 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.
+ 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] _ _ _ _ _ _ _ _
+ [ x ◠box (&shr{α}(refcell ty)); r ◠box (uninit 3); #lref ◠box (refmut α ty)]%TC
+ with "HEAP LFT Hna HE HL Hk");
+ [solve_typing..|by eapply write_own|by eapply read_own_move|done|done| |];
+ first last.
+ { 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 "∗#". }
+ simpl. eapply type_delete; [solve_typing..|]. eapply (type_jump [_]); solve_typing.
+ - iMod ("Hclose'" with "[Hlx Hownst Hst] 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. }
+ iApply (type_sum_assign_unit [refmut α ty; unit] _ _ _ _
+ [ x ◠box (&shr{α}(refcell ty)); r ◠box (uninit 3) ]%TC
+ with "HEAP LFT Hna HE HL Hk");
+ [solve_typing..|by eapply write_own|done| |]; first last.
+ { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
+ simpl. eapply (type_jump [_]); solve_typing.
+ Qed.
End refcell_functions.
--
GitLab