From 0259f8016708ac2f4da828a4579f703be926a082 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sun, 22 Jan 2017 14:05:41 +0100
Subject: [PATCH] Use pattern matching for defining some types. This make some
proof simpler.
---
theories/typing/bool.v | 21 +++++----
theories/typing/borrow.v | 51 +++++++++++-----------
theories/typing/int.v | 46 ++++++++++----------
theories/typing/own.v | 65 ++++++++++++++--------------
theories/typing/product_split.v | 76 ++++++++++++++-------------------
theories/typing/shr_bor.v | 40 ++++++++---------
theories/typing/type_sum.v | 37 +++++++---------
theories/typing/uniq_bor.v | 69 +++++++++++++++---------------
theories/typing/unsafe/cell.v | 24 +++++------
9 files changed, 207 insertions(+), 222 deletions(-)
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 1277ca81..c1f228b0 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -8,11 +8,16 @@ Section bool.
Context `{typeG Σ}.
Program Definition bool : type :=
- {| st_own tid vl := (∃ z:bool, ⌜vl = [ #z ]âŒ)%I |}.
- Next Obligation. iIntros (tid vl) "H". iDestruct "H" as (z) "%". by subst. Qed.
+ {| st_own tid vl :=
+ match vl return _ with
+ | [ #(LitInt (0|1))] => True
+ | _ => False
+ end%I |}.
+ Next Obligation. intros ? [|[[| |[|[]|]]|] []]; try iIntros "[]"; auto. Qed.
+ Next Obligation. intros ? [|[[| |[|[]|]]|] []]; apply _. Qed.
Global Instance bool_send : Send bool.
- Proof. iIntros (tid1 tid2 vl). done. Qed.
+ Proof. done. Qed.
End bool.
Section typing.
@@ -22,7 +27,7 @@ Section typing.
typed_instruction_ty E L [] #b bool.
Proof.
iAlways. iIntros (tid qE) "_ _ $ $ $ _". wp_value.
- rewrite tctx_interp_singleton tctx_hasty_val. iExists _. done.
+ rewrite tctx_interp_singleton tctx_hasty_val. by destruct b.
Qed.
Lemma type_bool (b : Datatypes.bool) E L C T x e :
@@ -40,10 +45,10 @@ Section typing.
Proof.
iIntros (Hp He1 He2) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT".
iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "#Hp".
- wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
- iDestruct "Hown" as (b) "Hv". iDestruct "Hv" as %[=->].
- destruct b; wp_if.
- - iApply (He1 with "HEAP LFT Htl HE HL HC HT").
+ wp_bind p. iApply (wp_hasty with "Hp").
+ iIntros ([[| |[|[]|]]|]) "_ H1"; try iDestruct "H1" as "[]";
+ (iApply wp_case; [done..|iNext]).
- iApply (He2 with "HEAP LFT Htl HE HL HC HT").
+ - iApply (He1 with "HEAP LFT Htl HE HL HC HT").
Qed.
End typing.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 3f114dc3..0d04c3ed 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -17,12 +17,11 @@ Section borrow.
Proof.
iIntros (tid ??) "#LFT $ $ H".
rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
- iDestruct "H" as (v) "[% Hown]". iDestruct "Hown" as (l) "(EQ & Hmt & ?)".
- iDestruct "EQ" as %[=->]. iMod (bor_create with "LFT Hmt") as "[Hbor Hext]". done.
+ iDestruct "H" as ([[]|]) "[% Hown]"; try iDestruct "Hown" as "[]".
+ iDestruct "Hown" as "[Hmt ?]". iMod (bor_create with "LFT Hmt") as "[Hbor Hext]". done.
iModIntro. iSplitL "Hbor".
- - iExists _. iSplit. done. iExists _, _. erewrite <-uPred.iff_refl. eauto.
- - iExists _. iSplit. done. iIntros "H†". iExists _. iFrame. iSplitR. by eauto.
- by iMod ("Hext" with "H†") as "$".
+ - iExists _. iSplit. done. iExists _. erewrite <-uPred.iff_refl. eauto.
+ - iExists _. iSplit. done. iIntros "H†". by iMod ("Hext" with "H†") as "$".
Qed.
Lemma tctx_extract_hasty_borrow E L p n ty ty' κ T :
@@ -51,21 +50,21 @@ Section borrow.
iIntros (Hκ) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp".
rewrite tctx_interp_singleton.
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
- wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
- iDestruct "Hown" as (l P) "[[Heq #HPiff] HP]". iDestruct "Heq" as %[=->].
+ wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown";
+ (try iDestruct "Hown" as "[]"). iDestruct "Hown" as (P) "[#HPiff HP]".
iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
iMod (bor_acc_cons with "LFT H↦ Htok") as "[H↦ Hclose']". done.
- iDestruct "H↦" as (vl) "[>H↦ Hown]". iDestruct "Hown" as (l') "(>% & Hown & H†)".
- subst. rewrite heap_mapsto_vec_singleton. wp_read.
+ iDestruct "H↦" as ([|[[|l'|]|][]]) "[>H↦ Hown]"; try iDestruct "Hown" as ">[]".
+ iDestruct "Hown" as "[Hown H†]". rewrite heap_mapsto_vec_singleton. wp_read.
iMod ("Hclose'" with "*[H↦ Hown H†][]") as "[Hbor Htok]"; last 1 first.
- iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
iMod (bor_sep _ _ _ (l' ↦∗: ty_own ty tid) with "LFT Hbor") as "[_ Hbor]". done.
iMod ("Hclose" with "Htok") as "($ & $)".
- rewrite tctx_interp_singleton tctx_hasty_val' //. iExists _, _.
- iFrame. iSplitR. done. rewrite -uPred.iff_refl. auto.
+ rewrite tctx_interp_singleton tctx_hasty_val' //. iExists _.
+ erewrite <-uPred.iff_refl. auto.
- iFrame "H↦ H†Hown".
- iIntros "!>(?&?&?)!>". iNext. iExists _.
- rewrite -heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame.
+ rewrite -heap_mapsto_vec_singleton. iFrame. by iFrame.
Qed.
Lemma type_deref_uniq_own {E L} κ x p e n ty C T T' :
@@ -85,16 +84,15 @@ Section borrow.
iIntros (Hκ) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp".
rewrite tctx_interp_singleton.
iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
- wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
- iDestruct "Hown" as (l) "[Heq #H↦]". iDestruct "Heq" as %[=->].
- iDestruct "H↦" as (vl) "[H↦b #Hown]".
+ wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown";
+ (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+.
- wp_read. iIntros "!>[#Hshr Htok2]".
iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
iMod ("Hclose" with "[Htok1 Htok2]") as "($ & $)"; first by iFrame.
- rewrite tctx_interp_singleton tctx_hasty_val' //. iExists _. auto.
+ rewrite tctx_interp_singleton tctx_hasty_val' //. auto.
Qed.
Lemma type_deref_shr_own {E L} κ x p e n ty C T T' :
@@ -116,25 +114,25 @@ Section borrow.
iPoseProof (Hincl with "[#] [#]") as "Hincl".
{ by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
- wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
- iDestruct "Hown" as (l P) "[[Heq #HPiff] HP]". iDestruct "Heq" as %[=->].
+ wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown";
+ try iDestruct "Hown" as "[]". iDestruct "Hown" as (P) "[#HPiff HP]".
iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
iMod (bor_exists with "LFT H↦") as (vl) "Hbor". done.
iMod (bor_sep with "LFT Hbor") as "[H↦ Hbor]". done.
- iMod (bor_exists with "LFT Hbor") as (l') "Hbor". done.
+ destruct vl as [|[[]|][]];
+ try by iMod (bor_persistent_tok with "LFT Hbor Htok") as "[>[] _]".
iMod (bor_exists with "LFT Hbor") as (P') "Hbor". done.
iMod (bor_sep with "LFT Hbor") as "[H Hbor]". done.
- iMod (bor_persistent_tok with "LFT H Htok") as "[[>% #HP'iff] Htok]". done. subst.
+ iMod (bor_persistent_tok with "LFT H Htok") as "[#HP'iff Htok]". done.
iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
rewrite heap_mapsto_vec_singleton.
iApply (wp_fupd_step _ (⊤∖↑lftN) with "[Hbor]"); try done.
by iApply (bor_unnest with "LFT Hbor").
- wp_read. iIntros "!> Hbor". iFrame "#".
+ wp_read. iIntros "!> Hbor".
iMod ("Hclose'" with "[H↦]") as "[H↦ Htok]"; first by auto.
iMod ("Hclose" with "Htok") as "($ & $)".
rewrite tctx_interp_singleton tctx_hasty_val' //.
- iExists _, _. iSplitR; first by auto.
- iApply (bor_shorten with "[] Hbor").
+ iExists _. iSplitR; first by auto. iApply (bor_shorten with "[] Hbor").
iApply (lft_incl_glb with "Hincl"). iApply lft_incl_refl.
Qed.
@@ -156,9 +154,8 @@ Section borrow.
iPoseProof (Hincl with "[#] [#]") as "Hincl".
{ by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
- wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
- iDestruct "Hown" as (l) "[Heq Hshr]".
- iDestruct "Heq" as %[=->]. iDestruct "Hshr" as (l') "[H↦ Hown]".
+ wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hshr";
+ try iDestruct "Hshr" as "[]". iDestruct "Hshr" as (l') "[H↦ Hown]".
iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
iAssert (κ ⊑ κ' ∪ κ)%I as "#Hincl'".
{ iApply (lft_incl_glb with "Hincl []"). iApply lft_incl_refl. }
@@ -169,7 +166,7 @@ Section borrow.
iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
iMod ("Hclose" with "[Htok1 Htok2]") as "($ & $)"; first by iFrame.
rewrite tctx_interp_singleton tctx_hasty_val' //.
- iExists _. iSplitR. done. by iApply (ty_shr_mono with "LFT Hincl' Hshr").
+ by iApply (ty_shr_mono with "LFT Hincl' Hshr").
Qed.
Lemma type_deref_shr_uniq {E L} κ κ' x p e ty C T T' :
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 637fb1e5..d4384fe9 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -7,11 +7,16 @@ Section int.
Context `{typeG Σ}.
Program Definition int : type :=
- {| st_own tid vl := (∃ z:Z, ⌜vl = [ #z ]âŒ)%I |}.
- Next Obligation. iIntros (tid vl) "H". iDestruct "H" as (z) "%". by subst. Qed.
+ {| st_own tid vl :=
+ match vl return _ with
+ | [ #(LitInt z)] => True
+ | _ => False
+ end%I |}.
+ Next Obligation. intros ? [|[[]|] []]; try iIntros "[]". auto. Qed.
+ Next Obligation. intros ? [|[[]|] []]; apply _. Qed.
Global Instance int_send : Send int.
- Proof. iIntros (tid1 tid2 vl). done. Qed.
+ Proof. done. Qed.
End int.
Section typing.
@@ -21,7 +26,7 @@ Section typing.
typed_instruction_ty E L [] #z int.
Proof.
iAlways. iIntros (tid qE) "_ _ $ $ $ _". wp_value.
- rewrite tctx_interp_singleton tctx_hasty_val. iExists _. done.
+ by rewrite tctx_interp_singleton tctx_hasty_val.
Qed.
Lemma type_int (z : Z) E L C T x e :
@@ -37,12 +42,11 @@ Section typing.
Proof.
iAlways. iIntros (tid qE) "_ _ $ $ $". 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".
- iDestruct "Hown1" as (z1) "EQ". iDestruct "EQ" as %[=->].
- iDestruct "Hown2" as (z2) "EQ". iDestruct "EQ" as %[=->].
- wp_op. rewrite tctx_interp_singleton tctx_hasty_val' //.
- iExists _. done.
+ wp_bind p1. iApply (wp_hasty with "Hp1").
+ iIntros ([[]|]) "_ H1"; try iDestruct "H1" as "[]".
+ wp_bind p2. iApply (wp_hasty with "Hp2").
+ iIntros ([[]|]) "_ H2"; try iDestruct "H2" as "[]".
+ wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //.
Qed.
Lemma type_plus E L C T T' p1 p2 x e :
@@ -59,12 +63,11 @@ Section typing.
Proof.
iAlways. iIntros (tid qE) "_ _ $ $ $". 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".
- iDestruct "Hown1" as (z1) "EQ". iDestruct "EQ" as %[=->].
- iDestruct "Hown2" as (z2) "EQ". iDestruct "EQ" as %[=->].
- wp_op. rewrite tctx_interp_singleton tctx_hasty_val' //.
- iExists _. done.
+ wp_bind p1. iApply (wp_hasty with "Hp1").
+ iIntros ([[]|]) "_ H1"; try iDestruct "H1" as "[]".
+ wp_bind p2. iApply (wp_hasty with "Hp2").
+ iIntros ([[]|]) "_ H2"; try iDestruct "H2" as "[]".
+ wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //.
Qed.
Lemma type_minus E L C T T' p1 p2 x e :
@@ -81,12 +84,11 @@ Section typing.
Proof.
iAlways. iIntros (tid qE) "_ _ $ $ $". 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".
- iDestruct "Hown1" as (z1) "EQ". iDestruct "EQ" as %[=->].
- iDestruct "Hown2" as (z2) "EQ". iDestruct "EQ" as %[=->].
- wp_op; intros _; rewrite tctx_interp_singleton tctx_hasty_val' //;
- iExists _; done.
+ wp_bind p1. iApply (wp_hasty with "Hp1").
+ iIntros ([[]|]) "_ H1"; try iDestruct "H1" as "[]".
+ wp_bind p2. iApply (wp_hasty with "Hp2").
+ iIntros ([[]|]) "_ H2"; try iDestruct "H2" as "[]".
+ wp_op; intros _; by rewrite tctx_interp_singleton tctx_hasty_val' //.
Qed.
Lemma type_le E L C T T' p1 p2 x e :
diff --git a/theories/typing/own.v b/theories/typing/own.v
index f4fe9539..343c6178 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -44,29 +44,29 @@ Section own.
Program Definition own_ptr (n : nat) (ty : type) :=
{| ty_size := 1;
ty_own tid vl :=
+ match vl return _ with
+ | [ #(LitLoc l) ] =>
(* We put a later in front of the †{q}, because we cannot use
[ty_size_eq] on [ty] at step index 0, which would in turn
prevent us to prove [subtype_own].
Since this assertion is timeless, this should not cause
problems. *)
- (∃ l:loc, ⌜vl = [ #l ]⌠∗ ▷ l ↦∗: ty.(ty_own) tid ∗
- â–· freeable_sz n ty.(ty_size) l)%I;
+ ▷ l ↦∗: ty.(ty_own) tid ∗ ▷ freeable_sz n ty.(ty_size) l
+ | _ => False
+ end%I;
ty_shr κ tid l :=
(∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
□ (∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ] ={F,F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) κ tid l' ∗ q.[κ]))%I
|}.
- Next Obligation.
- iIntros (q ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
- Qed.
+ Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H"; try iDestruct "H" as "[]". Qed.
Next Obligation.
move=>n ty N κ l tid ?? /=. iIntros "#LFT Hshr Htok".
iMod (bor_exists with "LFT Hshr") as (vl) "Hb". set_solver.
iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]". set_solver.
- iMod (bor_exists with "LFT Hb2") as (l') "Hb2". set_solver.
- iMod (bor_sep with "LFT Hb2") as "[EQ Hb2]". set_solver.
- iMod (bor_persistent_tok with "LFT EQ Htok") as "[>% $]". set_solver.
- iExists l'. subst. rewrite heap_mapsto_vec_singleton.
+ destruct vl as [|[[|l'|]|][]];
+ try (iMod (bor_persistent_tok with "LFT Hb2 Htok") as "[>[]_]"; set_solver).
+ iFrame. iExists l'. rewrite heap_mapsto_vec_singleton.
iMod (bor_sep with "LFT Hb2") as "[Hb2 _]". set_solver.
iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "$". set_solver.
rewrite bor_unfold_idx. iDestruct "Hb2" as (i) "(#Hpb&Hpbown)".
@@ -101,8 +101,8 @@ Section own.
intros n1 n2 Hn12 ty1 ty2 Hincl. iIntros. iSplit; first done.
iDestruct (Hincl with "* [] [] []") as "(_ & #Ho & #Hs)"; [done..|clear Hincl].
iSplit; iAlways.
- - iIntros (??) "H". iDestruct "H" as (l) "(%&Hmt&H†)". subst.
- iExists _. iSplit. done. iDestruct "Hmt" as (vl') "[Hmt Hown]". iNext.
+ - 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 (ty_size_eq with "Hown") as %<-.
@@ -138,9 +138,9 @@ Section own.
Global Instance own_send n ty :
Send ty → Send (own_ptr n ty).
Proof.
- iIntros (Hsend tid1 tid2 vl) "H". iDestruct "H" as (l) "[% [Hm H†]]". subst vl.
- iExists _. iSplit; first done. iFrame "H†". iNext.
- iApply (heap_mapsto_pred_wand with "Hm"). iIntros (vl) "?". by iApply Hsend.
+ iIntros (Hsend tid1 tid2 [|[[| |]|][]]) "H"; try done.
+ iDestruct "H" as "[Hm $]". iNext. iApply (heap_mapsto_pred_wand with "Hm").
+ iIntros (vl) "?". by iApply Hsend.
Qed.
Global Instance own_sync n ty :
@@ -163,32 +163,31 @@ Section typing.
Lemma write_own {E L} ty ty' n :
ty.(ty_size) = ty'.(ty_size) → typed_write E L (own_ptr n ty') ty (own_ptr n ty).
Proof.
- iIntros (Hsz) "!#". iIntros (p tid F qE qL ?) "_ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
- iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
- iDestruct (ty_size_eq with "Hown") as "#>%". iModIntro.
- iExists _, _. iFrame "H↦".
- iSplit; first by rewrite Hsz. iIntros "Hown' !>".
- iExists _. iSplit; first done. rewrite Hsz. iFrame.
+ iIntros (Hsz) "!#". iIntros ([[]|] tid F qE qL ?) "_ $ $ Hown";
+ try iDestruct "Hown" as "[]". rewrite /= Hsz. iDestruct "Hown" as "[H↦ $]".
+ iDestruct "H↦" as (vl) "[>H↦ Hown]". iDestruct (ty_size_eq with "Hown") as "#>%".
+ iExists _, _. iFrame "H↦". auto.
Qed.
Lemma read_own_copy E L ty n :
Copy ty → typed_read E L (own_ptr n ty) ty (own_ptr n ty).
Proof.
- iIntros (Hsz) "!#". iIntros (p tid F qE qL ?) "_ $ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
- iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ #Hown]". iModIntro.
- iExists l, _, _. iSplit; first done. iFrame "∗#". iIntros "Hl !>".
- iExists _. iSplit; first done. iFrame "H†". iExists _. by iFrame.
+ iIntros (Hsz) "!#". iIntros ([[]|] tid F qE qL ?) "_ $ $ $ Hown";
+ try iDestruct "Hown" as "[]".
+ iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ #Hown]".
+ iExists l, _, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !>".
+ iExists _. auto.
Qed.
Lemma read_own_move E L ty n :
typed_read E L (own_ptr n ty) ty (own_ptr n $ uninit ty.(ty_size)).
Proof.
- iAlways. iIntros (p tid F qE qL ?) "_ $ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
- iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
+ iAlways. iIntros ([[]|] tid F qE qL ?) "_ $ $ $ Hown";
+ try iDestruct "Hown" as "[]".
+ iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
iDestruct (ty_size_eq with "Hown") as "#>%".
- iModIntro. iExists l, vl, _. iSplit; first done. iFrame "∗#". iIntros "Hl !>".
- iExists _. iSplit; first done. iFrame "H†". iExists _. iFrame.
- iApply uninit_own. auto.
+ iExists l, vl, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !> !>".
+ iExists _. iFrame. by iApply uninit_own.
Qed.
Lemma type_new_instr {E L} (n : Z) :
@@ -199,7 +198,7 @@ Section typing.
intros. iAlways. iIntros (tid q) "#HEAP #LFT $ $ $ _".
iApply (wp_new with "HEAP"); try done. iModIntro.
iIntros (l vl) "(% & H†& Hlft)". subst. rewrite tctx_interp_singleton tctx_hasty_val.
- iExists _. iSplit; first done. iNext. rewrite freeable_sz_full Z2Nat.id //. iFrame.
+ iNext. rewrite freeable_sz_full Z2Nat.id //. iFrame.
iExists vl. iFrame. by rewrite Nat2Z.id uninit_own.
Qed.
@@ -209,7 +208,7 @@ Section typing.
(∀ (v : val) (n' := Z.to_nat n),
typed_body E L C ((v ◠box (uninit n')) :: T) (subst' x v e)) →
typed_body E L C T (let: x := new [ #n ] in e).
- Proof. intros. eapply type_let. done. by apply type_new_instr. solve_typing. done. Qed.
+ Proof. intros. eapply type_let; [done|by apply type_new_instr|solve_typing..]. Qed.
Lemma type_new_subtype ty E L C T x (n : Z) e :
Closed (x :b: []) e →
@@ -231,8 +230,8 @@ Section typing.
typed_instruction E L [p ◠box ty] (delete [ #n; p])%E (λ _, []).
Proof.
iIntros (<-) "!#". iIntros (tid eq) "#HEAP #LFT $ $ $ Hp". rewrite tctx_interp_singleton.
- wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
- iDestruct "Hown" as (l) "(Hv & H↦∗: & >H†)". iDestruct "Hv" as %[=->].
+ wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown";
+ try iDestruct "Hown" as "[]". iDestruct "Hown" as "[H↦∗: >H†]".
iDestruct "H↦∗:" as (vl) "[>H↦ Hown]". rewrite tctx_interp_nil.
iDestruct (ty_size_eq with "Hown") as "#>EQ". iDestruct "EQ" as %<-.
iApply (wp_delete with "[-]"); try (by auto); [].
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 80b4f865..fc08cf18 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -90,17 +90,16 @@ Section product_split.
Proof.
iIntros (tid q1 q2) "#LFT $ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
- iDestruct "H" as (v) "[Hp H]". iDestruct "Hp" as %Hp. iDestruct "H" as (l) "(EQ & H & >H†)".
- iDestruct "EQ" as %[=->]. iDestruct "H" as (vl) "[>H↦ H]".
+ iDestruct "H" as ([[]|]) "[#Hp H]"; try iDestruct "H" as "[]".
+ iDestruct "H" as "[H >H†]". iDestruct "H" as (vl) "[>H↦ H]".
iDestruct "H" as (vl1 vl2) "(>% & H1 & H2)". subst.
rewrite heap_mapsto_vec_app -freeable_sz_split.
iDestruct "H†" as "[H†1 H†2]". iDestruct "H↦" as "[H↦1 H↦2]".
iDestruct (ty_size_eq with "H1") as "#>EQ".
iDestruct "EQ" as %->. iSplitL "H↦1 H†1 H1".
- + iExists _. iSplitR. done. iExists _. iFrame. iSplitL ""; first done.
- iExists _. iFrame. done.
- + iExists _. iSplitR. simpl. by rewrite Hp. iExists _. iFrame. iSplitR; first done.
- iExists _. iFrame. done.
+ + iExists _. iFrame "#∗". iExists _. by iFrame.
+ + iExists _. iSplitR; first (by simpl; iDestruct "Hp" as %->).
+ iFrame. iExists _. by iFrame.
Qed.
Lemma tctx_merge_own_prod2 E L p n ty1 ty2 :
@@ -109,22 +108,15 @@ Section product_split.
Proof.
iIntros (tid q1 q2) "#LFT $ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
- iDestruct "H" as "[H1 H2]". iDestruct "H1" as (v1) "(Hp1 & H1)".
- iDestruct "Hp1" as %Hp1. iDestruct "H1" as (l) "(EQ & H↦1 & H†1)".
- iDestruct "EQ" as %[=->]. iDestruct "H2" as (v2) "(Hp2 & H2)".
- rewrite /= Hp1. iDestruct "Hp2" as %[=<-]. iDestruct "H2" as (l') "(EQ & H↦2 & H†2)".
- iDestruct "EQ" as %[=<-]. iExists #l. iSplitR; first done. iExists l.
- iSplitR; first done. rewrite -freeable_sz_split. iFrame.
+ iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "(Hp1 & H1)";
+ try iDestruct "H1" as "[]". iDestruct "H1" as "(H↦1 & H†1)".
+ iDestruct "H2" as (v2) "(Hp2 & H2)". simpl. iDestruct "Hp1" as %HÏ1.
+ rewrite HÏ1. iDestruct "Hp2" as %[=<-]. iDestruct "H2" as "[H↦2 H†2]".
+ iExists #l. iSplitR; first done. rewrite /= -freeable_sz_split. iFrame.
iDestruct "H↦1" as (vl1) "[H↦1 H1]". iDestruct "H↦2" as (vl2) "[H↦2 H2]".
iExists (vl1 ++ vl2). rewrite heap_mapsto_vec_app. iFrame.
- iDestruct (ty_size_eq with "H1") as "#>EQ".
- iDestruct "EQ" as %->. iFrame. iExists vl1, vl2. iFrame. auto.
- Qed.
-
- Lemma own_is_ptr n ty tid (vl : list val) :
- ty_own (own_ptr n ty) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]âŒ.
- Proof.
- iIntros "H". iDestruct "H" as (l) "[% _]". iExists l. done.
+ iDestruct (ty_size_eq with "H1") as "#>EQ". iDestruct "EQ" as %->.
+ iFrame. iExists vl1, vl2. iFrame. auto 10.
Qed.
Lemma tctx_split_own_prod E L n tyl p :
@@ -132,7 +124,7 @@ Section product_split.
Proof.
apply tctx_split_ptr_prod.
- intros. apply tctx_split_own_prod2.
- - intros. apply own_is_ptr.
+ - intros ??[|[[]|][]]; try iIntros "[]". eauto.
Qed.
Lemma tctx_merge_own_prod E L n tyl :
@@ -143,7 +135,7 @@ Section product_split.
intros. apply tctx_merge_ptr_prod; try done.
- apply _.
- intros. apply tctx_merge_own_prod2.
- - intros. apply own_is_ptr.
+ - intros ??[|[[]|][]]; try iIntros "[]". eauto.
Qed.
(** Unique borrows *)
@@ -153,13 +145,13 @@ Section product_split.
Proof.
iIntros (tid q1 q2) "#LFT $ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
- iDestruct "H" as (v) "[Hp H]". iDestruct "Hp" as %Hp.
- iDestruct "H" as (l P) "[[EQ #HPiff] HP]". iDestruct "EQ" as %[=->].
+ iDestruct "H" as ([[]|]) "[Hp H]"; try iDestruct "H" as "[]". iDestruct "Hp" as %Hp.
+ iDestruct "H" as (P) "[#HPiff HP]".
iMod (bor_iff with "LFT [] HP") as "Hown". set_solver. by eauto.
rewrite /= split_prod_mt. iMod (bor_sep with "LFT Hown") as "[H1 H2]".
set_solver. rewrite /tctx_elt_interp /=.
iSplitL "H1"; iExists _; (iSplitR; first by rewrite Hp);
- iExists _, _; erewrite <-uPred.iff_refl; auto.
+ iExists _; erewrite <-uPred.iff_refl; auto.
Qed.
Lemma tctx_merge_uniq_prod2 E L p κ ty1 ty2 :
@@ -168,22 +160,21 @@ Section product_split.
Proof.
iIntros (tid q1 q2) "#LFT $ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
- iDestruct "H" as "[H1 H2]". iDestruct "H1" as (v1) "(Hp1 & H1)".
- iDestruct "Hp1" as %Hp1. iDestruct "H1" as (l P) "[[EQ #HPiff] HP]".
- iDestruct "EQ" as %[=->].
+ iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 H1]";
+ try iDestruct "H1" as "[]". iDestruct "Hp1" as %Hp1.
+ iDestruct "H1" as (P) "[#HPiff HP]".
iMod (bor_iff with "LFT [] HP") as "Hown1". set_solver. by eauto.
iDestruct "H2" as (v2) "(Hp2 & H2)". rewrite /= Hp1. iDestruct "Hp2" as %[=<-].
- iDestruct "H2" as (l' Q) "[[EQ #HQiff] HQ]". iDestruct "EQ" as %[=<-].
+ iDestruct "H2" as (Q) "[#HQiff HQ]".
iMod (bor_iff with "LFT [] HQ") as "Hown2". set_solver. by eauto.
- iExists #l. iSplitR; first done. iExists l, _. iSplitR.
- { iSplitR; first done. erewrite <-uPred.iff_refl; auto. }
+ iExists #l. iFrame "%". iExists _. erewrite <-uPred.iff_refl; auto. iSplitR. done.
rewrite split_prod_mt. iApply (bor_combine with "LFT Hown1 Hown2"). set_solver.
Qed.
Lemma uniq_is_ptr κ ty tid (vl : list val) :
ty_own (&uniq{κ} ty) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]âŒ.
Proof.
- iIntros "H". iDestruct "H" as (l P) "[[% _] _]". iExists l. done.
+ iIntros "H". destruct vl as [|[[]|][]]; try iDestruct "H" as "[]". eauto.
Qed.
Lemma tctx_split_uniq_prod E L κ tyl p :
@@ -213,10 +204,9 @@ Section product_split.
Proof.
iIntros (tid q1 q2) "#LFT $ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
- iDestruct "H" as (v) "[Hp H]". iDestruct "Hp" as %Hp.
- iDestruct "H" as (l) "[EQ [H1 H2]]". iDestruct "EQ" as %[=->].
- iSplitL "H1"; iExists _; (iSplitR; first by rewrite /= Hp);
- iExists _; iSplitR; done.
+ iDestruct "H" as ([[]|]) "[Hp H]"; try iDestruct "H" as "[]".
+ iDestruct "H" as "[H1 H2]". iDestruct "Hp" as %Hp.
+ by iSplitL "H1"; iExists _; (iSplitR; first by rewrite /= Hp).
Qed.
Lemma tctx_merge_shr_prod2 E L p κ ty1 ty2 :
@@ -225,19 +215,17 @@ Section product_split.
Proof.
iIntros (tid q1 q2) "#LFT $ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
- iDestruct "H" as "[H1 H2]". iDestruct "H1" as (v1) "(Hp1 & H1)".
- iDestruct "Hp1" as %Hp1. iDestruct "H1" as (l) "[EQ Hown1]".
- iDestruct "EQ" as %[=->]. iDestruct "H2" as (v2) "(Hp2 & H2)".
- rewrite /= Hp1. iDestruct "Hp2" as %[=<-].
- iDestruct "H2" as (l') "[EQ Hown2]". iDestruct "EQ" as %[=<-].
- iExists #l. iSplitR; first done. iExists l. iSplitR; first done.
- by iFrame.
+ iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 Hown1]";
+ try iDestruct "Hown1" as "[]". iDestruct "Hp1" as %Hp1.
+ iDestruct "H2" as ([[]|]) "[Hp2 Hown2]"; try iDestruct "Hown2" as "[]".
+ rewrite /= Hp1. iDestruct "Hp2" as %[=<-].
+ iExists #l. by iFrame.
Qed.
Lemma shr_is_ptr κ ty tid (vl : list val) :
ty_own (&shr{κ} ty) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]âŒ.
Proof.
- iIntros "H". iDestruct "H" as (l) "[% _]". iExists l. done.
+ iIntros "H". destruct vl as [|[[]|][]]; try iDestruct "H" as "[]". eauto.
Qed.
Lemma tctx_split_shr_prod E L κ tyl p :
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index aa617b18..6e92e902 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -8,18 +8,22 @@ Section shr_bor.
Context `{typeG Σ}.
Program Definition shr_bor (κ : lft) (ty : type) : type :=
- {| st_own tid vl := (∃ (l:loc), ⌜vl = [ #l ]⌠∗ ty.(ty_shr) κ tid l)%I |}.
+ {| st_own tid vl :=
+ match vl return _ with
+ | [ #(LitLoc l) ] => ty.(ty_shr) κ tid l
+ | _ => False
+ end%I |}.
Next Obligation.
- iIntros (κ ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
+ iIntros (κ ty tid [|[[]|][]]) "H"; try iDestruct "H" as "[]". done.
Qed.
+ Next Obligation. intros κ ty tid [|[[]|][]]; apply _. Qed.
Global Instance shr_mono E L :
Proper (flip (lctx_lft_incl E L) ==> subtype E L ==> subtype E L) shr_bor.
Proof.
intros κ1 κ2 Hκ ty1 ty2 Hty. apply subtype_simple_type.
- iIntros (??) "#LFT #HE #HL H". iDestruct (Hκ with "HE HL") as "#Hκ".
- iDestruct "H" as (l) "(% & H)". subst. iExists _. iSplit. done.
- iApply (ty2.(ty_shr_mono) with "LFT Hκ").
+ 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].
by iApply "Hs1".
Qed.
@@ -41,8 +45,7 @@ Section shr_bor.
Global Instance shr_send κ ty :
Sync ty → Send (shr_bor κ ty).
Proof.
- iIntros (Hsync tid1 tid2 vl) "H". iDestruct "H" as (l) "[% Hshr]".
- iExists _. iSplit; first done. by iApply Hsync.
+ iIntros (Hsync tid1 tid2 [|[[]|][]]) "H"; try iDestruct "H" as "[]". by iApply Hsync.
Qed.
End shr_bor.
@@ -69,28 +72,25 @@ Section typing.
iDestruct (llctx_interp_persist with "HL") as "#HL'". iFrame "HE HL".
iDestruct (Hκκ' with "HE' HL'") as "Hκκ'".
rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
- iDestruct "H" as (v) "[% #H]". iDestruct "H" as (l) "[EQ Hshr]".
- iDestruct "EQ" as %[=->]. simpl. iModIntro. iSplit.
- - iExists _. iSplit. done. iExists _. iSplit. done.
- by iApply (ty_shr_mono with "LFT Hκκ' Hshr").
- - iExists _. iSplit. done. iIntros "_". iIntros "!>".
- iExists _. auto.
+ iDestruct "H" as ([[]|]) "[% #Hshr]"; try iDestruct "Hshr" as "[]".
+ iModIntro. iSplit.
+ - iExists _. iSplit. done. by iApply (ty_shr_mono with "LFT Hκκ' Hshr").
+ - iExists _. auto.
Qed.
Lemma read_shr E L κ ty :
Copy ty → lctx_lft_alive E L κ → typed_read E L (&shr{κ}ty) ty (&shr{κ}ty).
Proof.
- iIntros (Hcopy Halive) "!#". iIntros (v tid F qE qL ?) "#LFT Htl HE HL Hown".
+ iIntros (Hcopy Halive) "!#". iIntros ([[]|] tid F qE qL ?) "#LFT Htl HE HL #Hshr";
+ try iDestruct "Hshr" as "[]".
iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first set_solver.
- iDestruct "Hown" as (l) "[EQ #Hshr]". iDestruct "EQ" as %[=->].
- assert (↑shrN ⊆ (↑lrustN : coPset)) by solve_ndisj. (* set_solver needs some help. *)
+ assert (↑shrN ⊆ (↑lrustN : coPset)) by solve_ndisj. (* set_solver needs some help. *)
iMod (copy_shr_acc with "LFT Hshr Htl Hκ") as (q') "(Htl & H↦ & Hcl)".
{ set_solver. } { rewrite ->shr_locsE_shrN. set_solver. }
iDestruct "H↦" as (vl) "[>Hmt #Hown]". iModIntro. iExists _, _, _.
- iSplit; first done. iFrame "∗#". iIntros "Hmt".
- iMod ("Hcl" with "Htl [Hmt]") as "[$ Hκ]".
- { iExists _. iFrame "∗#". }
- iMod ("Hclose" with "Hκ") as "[$ $]". iExists _. auto.
+ iFrame "∗#". iSplit; first done. iIntros "Hmt".
+ iMod ("Hcl" with "Htl [Hmt]") as "[$ Hκ]"; first by iExists _; iFrame.
+ iApply ("Hclose" with "Hκ").
Qed.
End typing.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 7fe48853..419447bb 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -17,8 +17,8 @@ Section case.
Proof.
iIntros (Hel) "!#". iIntros (tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
- iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hp".
- iDestruct "Hp" as (l) "[EQ [H↦ Hf]]". iDestruct "EQ" as %[=->].
+ iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp";
+ try iDestruct "Hp" as "[]". iDestruct "Hp" as "[H↦ Hf]".
iDestruct "H↦" as (vl) "[H↦ Hown]".
iDestruct "Hown" as (i vl' vl'') "(>% & >EQlen & Hown)". subst.
simpl ty_size. iDestruct "EQlen" as %[=EQlen]. rewrite -EQlen. simpl length.
@@ -34,14 +34,12 @@ Section case.
rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //; iFrame "HT".
- iDestruct (ty.(ty_size_eq) with "Hown") as %<-.
iSplitL "H↦i Hfi"; last iSplitR "H↦vl'' Hfvl''".
- + rewrite shift_loc_0. iExists _. iFrame. iSplit. done. iExists [ #i].
- rewrite heap_mapsto_vec_singleton.
+ + rewrite shift_loc_0. iFrame. iExists [ #i]. rewrite heap_mapsto_vec_singleton.
iFrame. iExists [_], []. auto.
- + iExists _. iFrame. iSplit. done. iExists _. iFrame.
+ + iFrame. iExists _. iFrame.
+ rewrite -EQlen app_length minus_plus -(shift_loc_assoc_nat _ 1).
- iExists _. iFrame. iSplit. done. iExists _. iFrame. rewrite uninit_own. auto.
- - iExists _. iSplit. done.
- assert (EQf:=freeable_sz_split n 1). simpl in EQf. rewrite -EQf. clear EQf.
+ 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.
@@ -67,9 +65,8 @@ Section case.
Proof.
iIntros (Halive Hel) "!#". iIntros (tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
- iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hp".
- iDestruct "Hp" as (l P) "[[EQ HP] Hb]". iDestruct "EQ" as %[=->].
- iMod (bor_iff with "LFT HP Hb") as "Hb". done.
+ iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try iDestruct "Hp" as "[]".
+ iDestruct "Hp" as (P) "[HP Hb]". iMod (bor_iff with "LFT HP Hb") as "Hb". done.
iMod (Halive with "HE HL") as (q) "[Htok Hclose]". done.
iMod (bor_acc_cons with "LFT Hb Htok") as "[H↦ Hclose']". done.
iDestruct "H↦" as (vl) "[H↦ Hown]".
@@ -94,7 +91,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 "HT".
- iExists _, _. iFrame. iSplit. done. iSplit; iIntros "!>!#$".
+ iExists _. erewrite <-uPred.iff_refl. auto.
- iMod ("Hclose'" with "* [H↦i H↦vl' H↦vl'' Hown] []") as "[Hb Htok]";
[|by iIntros "!>$"|].
{ iExists (#i::vl'++vl'').
@@ -103,7 +100,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 "HT".
- iExists _, _. iFrame. iSplit. done. iSplit; iIntros "!>!#$".
+ iExists _. erewrite <-uPred.iff_refl. auto.
Qed.
Lemma type_case_uniq E L C T T' p κ tyl el :
@@ -124,9 +121,8 @@ Section case.
Proof.
iIntros (Halive Hel) "!#". iIntros (tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
- iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hp".
- iDestruct "Hp" as (l) "[EQ Hl]". iDestruct "EQ" as %[=->].
- iDestruct "Hl" as (i) "[#Hb Hshr]".
+ iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try iDestruct "Hp" as "[]".
+ iDestruct "Hp" as (i) "[#Hb Hshr]".
iMod (Halive with "HE HL") as (q) "[Htok Hclose]". done.
iMod (frac_bor_acc with "LFT Hb Htok") as (q') "[[H↦i H↦vl''] Hclose']". done.
rewrite nth_lookup.
@@ -136,9 +132,8 @@ Section case.
iMod ("Hclose'" with "[$H↦i $H↦vl'']") as "Htok".
iMod ("Hclose" with "Htok") as "[HE HL]".
destruct Hety as [Hety|Hety]; iApply (Hety with "HEAP LFT Hna HE HL HC");
- rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //; iFrame "HT".
- - iExists _. auto.
- - iExists _. iSplit. done. iExists i. rewrite nth_lookup EQty /=. auto.
+ rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //; iFrame.
+ iExists _. rewrite ->nth_lookup, EQty. auto.
Qed.
Lemma type_case_shr E L C T p κ tyl el :
@@ -237,8 +232,8 @@ Section case.
iApply wp_seq. done. iNext. 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)"=>//=. subst.
- assert (ty.(ty_size) ≤ length vl1).
+ 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.
- specialize (IHtyl i). intuition lia. }
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index b7393c44..5a40d780 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -19,25 +19,28 @@ Section uniq_bor.
The trouble with this definition is that bor_unnest as proven is too
weak. The original unnesting with open borrows was strong enough. *)
ty_own tid vl :=
- (∃ (l:loc) P, (⌜vl = [ #l ]⌠∗ ▷ □ (P ↔ l ↦∗: ty.(ty_own) tid)) ∗ &{κ} P)%I;
+ match vl return _ with
+ | [ #(LitLoc l) ] =>
+ ∃ P, ▷ □ (P ↔ l ↦∗: ty.(ty_own) tid) ∗ &{κ} P
+ | _ => False
+ end%I;
ty_shr κ' tid l :=
(∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
□ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ∪κ']
={F, F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) (κ∪κ') tid l' ∗ q.[κ∪κ'])%I
|}.
Next Obligation.
- iIntros (q ty tid vl) "H". iDestruct "H" as (l P) "[[% _] _]". by subst.
+ iIntros (q ty tid [|[[]|][]]) "H"; try iDestruct "H" as "[]". done.
Qed.
Next Obligation.
move=> κ ty N κ' l tid ??/=. iIntros "#LFT Hshr Htok".
- iMod (bor_exists with "LFT Hshr") as (vl) "Hb". set_solver.
- iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]". set_solver.
- iMod (bor_exists with "LFT Hb2") as (l') "Hb2". set_solver.
+ iMod (bor_exists with "LFT Hshr") as ([|[[|l'|]|][]]) "Hb"; first set_solver;
+ (iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]"; first set_solver);
+ try (iMod (bor_persistent_tok with "LFT Hb2 Htok") as "[>[] _]"; set_solver).
iMod (bor_exists with "LFT Hb2") as (P) "Hb2". set_solver.
iMod (bor_sep with "LFT Hb2") as "[H Hb2]". set_solver.
- iMod (bor_persistent_tok with "LFT H Htok") as "[[>% #HPiff] Htok]". set_solver.
- iFrame "Htok". iExists l'.
- subst. rewrite heap_mapsto_vec_singleton.
+ iMod (bor_persistent_tok with "LFT H Htok") as "[#HPiff $]". set_solver.
+ iExists l'. subst. rewrite heap_mapsto_vec_singleton.
iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "$". set_solver.
rewrite {1}bor_unfold_idx. iDestruct "Hb2" as (i) "[#Hpb Hpbown]".
iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty (κ∪κ') tid l')%I
@@ -78,13 +81,12 @@ Section uniq_bor.
iDestruct (Hty2 with "* [] [] []") as "(_ & #Ho2 & #Hs2)"; [done..|clear Hty2].
iDestruct (Hκ with "[] []") as "#Hκ"; [done..|].
iSplit; iAlways.
- - iIntros (??) "H". iDestruct "H" as (l P) "[[% #HPiff] Hown]". subst.
- iExists _, _. iSplitR; last by iApply (bor_shorten with "Hκ"). iSplit. done.
- iNext. iIntros "!#". iSplit; iIntros "H".
- + iDestruct ("HPiff" with "H") as (vl) "[??]". iExists vl. iFrame.
- by iApply "Ho1".
- + iDestruct "H" as (vl) "[??]". iApply "HPiff". iExists vl. iFrame.
- by iApply "Ho2".
+ - iIntros (? [|[[]|][]]) "H"; try iDestruct "H" as "[]".
+ iDestruct "H" as (P) "[#HPiff Hown]". iExists _.
+ iSplitR; last by iApply (bor_shorten with "Hκ"). iNext.
+ iIntros "!#". iSplit; iIntros "H".
+ + iDestruct ("HPiff" with "H") as (vl) "[??]". iExists vl. iFrame. by iApply "Ho1".
+ + iDestruct "H" as (vl) "[??]". iApply "HPiff". iExists vl. iFrame. by iApply "Ho2".
- iIntros (κ ??) "H". iAssert (κ2 ∪ κ ⊑ κ1 ∪ κ)%I as "#Hincl'".
{ iApply (lft_incl_glb with "[] []").
- iApply (lft_incl_trans with "[] Hκ"). iApply lft_le_incl.
@@ -116,13 +118,12 @@ Section uniq_bor.
Global Instance uniq_send κ ty :
Send ty → Send (uniq_bor κ ty).
Proof.
- iIntros (Hsend tid1 tid2 vl) "H". iDestruct "H" as (l P) "[[% #HPiff] H]".
- iExists _, _. iFrame "H". iSplit; first done. iNext. iAlways. iSplit.
+ iIntros (Hsend tid1 tid2 [|[[]|][]]) "H"; try iDestruct "H" as "[]".
+ iDestruct "H" as (P) "[#HPiff H]". iExists _. iFrame. iNext. iAlways. iSplit.
- iIntros "HP". iApply (heap_mapsto_pred_wand with "[HP]").
- { by iApply "HPiff". }
- clear dependent vl. iIntros (vl) "?". by iApply Hsend.
+ { by iApply "HPiff". } { iIntros (vl). by iApply Hsend. }
- iIntros "HP". iApply "HPiff". iApply (heap_mapsto_pred_wand with "HP").
- clear dependent vl. iIntros (vl) "?". by iApply Hsend.
+ iIntros (vl). by iApply Hsend.
Qed.
Global Instance uniq_sync κ ty :
@@ -155,12 +156,11 @@ Section typing.
iIntros (Hκ ???) "#LFT HE HL Huniq".
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; [try done..|].
rewrite !tctx_interp_singleton /=.
- iDestruct "Huniq" as (v) "[% Huniq]".
- iDestruct "Huniq" as (l P) "[[% #HPiff] HP]".
+ iDestruct "Huniq" as ([[]|]) "[% Huniq]"; try iDestruct "Huniq" as "[]".
+ iDestruct "Huniq" as (P) "[#HPiff HP]".
iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
iMod (ty.(ty_share) with "LFT H↦ Htok") as "[Hown Htok]"; [solve_ndisj|].
- iMod ("Hclose" with "Htok") as "[$ $]". iExists _. iFrame "%".
- iIntros "!>/=". eauto.
+ iMod ("Hclose" with "Htok") as "[$ $]". iExists _. by iFrame "%∗".
Qed.
Lemma tctx_reborrow_uniq E L p ty κ κ' :
@@ -172,12 +172,13 @@ Section typing.
iDestruct (llctx_interp_persist with "HL") as "#HL'". iFrame "HE HL".
iDestruct (Hκκ' with "HE' HL'") as "Hκκ'".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
- iDestruct "H" as (v) "[% Hown]". iDestruct "Hown" as (l P) "[[EQ #Hiff] Hb]".
- iDestruct "EQ" as %[=->]. iMod (bor_iff with "LFT [] Hb") as "Hb". done. by eauto.
+ iDestruct "H" as ([[]|]) "[% Hown]"; try iDestruct "Hown" as "[]".
+ iDestruct "Hown" as (P) "[#Hiff Hb]".
+ iMod (bor_iff with "LFT [] Hb") as "Hb". done. by eauto.
iMod (rebor with "LFT Hκκ' Hb") as "[Hb Hext]". done. iModIntro. iSplitL "Hb".
- - iExists _. iSplit. done. iExists _, _. erewrite <-uPred.iff_refl. eauto.
+ - iExists _. iSplit. done. iExists _. erewrite <-uPred.iff_refl. eauto.
- iExists _. iSplit. done. iIntros "#H†". iMod ("Hext" with "H†") as "Hb".
- iExists _, _. erewrite <-uPred.iff_refl. eauto.
+ iExists _. erewrite <-uPred.iff_refl. eauto.
Qed.
(* When sharing during extraction, we do the (arbitrary) choice of
@@ -222,9 +223,9 @@ Section typing.
Lemma read_uniq E L κ ty :
Copy ty → lctx_lft_alive E L κ → typed_read E L (&uniq{κ}ty) ty (&uniq{κ}ty).
Proof.
- iIntros (Hcopy Halive) "!#". iIntros (v tid F qE qL ?) "#LFT Htl HE HL Hown".
+ iIntros (Hcopy Halive) "!#". iIntros ([[]|] tid F qE qL ?) "#LFT Htl HE HL Hown";
+ try iDestruct "Hown" as "[]". iDestruct "Hown" as (P) "[#HP H↦]".
iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first set_solver.
- iDestruct "Hown" as (l P) "[[EQ #HP] H↦]". iDestruct "EQ" as %[=->].
iMod (bor_iff with "LFT [] H↦") as "H↦". set_solver. by eauto.
iMod (bor_acc with "LFT H↦ Hκ") as "[H↦ Hclose']"; first set_solver.
iDestruct "H↦" as (vl) "[>H↦ #Hown]".
@@ -232,15 +233,15 @@ Section typing.
iExists _, _, _. iSplit; first done. iFrame "∗#". iIntros "H↦".
iMod ("Hclose'" with "[H↦]") as "[H↦ Htok]". by iExists _; iFrame.
iMod ("Hclose" with "Htok") as "($ & $ & $)".
- iExists _, _. erewrite <-uPred.iff_refl. auto.
+ iExists _. erewrite <-uPred.iff_refl. auto.
Qed.
Lemma write_uniq E L κ ty :
lctx_lft_alive E L κ → typed_write E L (&uniq{κ}ty) ty (&uniq{κ}ty).
Proof.
- iIntros (Halive) "!#". iIntros (p tid F qE qL ?) "#LFT HE HL Hown".
+ iIntros (Halive) "!#". iIntros ([[]|] tid F qE qL ?) "#LFT HE HL Hown";
+ try iDestruct "Hown" as "[]". iDestruct "Hown" as (P) "[#HP H↦]".
iMod (Halive with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
- iDestruct "Hown" as (l P) "[[EQ #HP] H↦]". iDestruct "EQ" as %[=->].
iMod (bor_iff with "LFT [] H↦") as "H↦". set_solver. by eauto.
iMod (bor_acc with "LFT H↦ Htok") as "[H↦ Hclose']". set_solver.
iDestruct "H↦" as (vl) "[>H↦ Hown]". rewrite ty.(ty_size_eq).
@@ -248,7 +249,7 @@ Section typing.
iFrame. iIntros "Hown". iDestruct "Hown" as (vl') "[H↦ Hown]".
iMod ("Hclose'" with "[H↦ Hown]") as "[Hbor Htok]". by iExists _; iFrame.
iMod ("Hclose" with "Htok") as "($ & $ & $)".
- iExists _, _. erewrite <-uPred.iff_refl. auto.
+ iExists _. erewrite <-uPred.iff_refl. auto.
Qed.
End typing.
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index 679a50a8..f01a36be 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -129,10 +129,10 @@ Section typing.
(* Writing to a cell *)
Definition cell_set ty : val :=
funrec: <> ["c"; "x"] :=
- let: "c'" := !"c" in
- "c'" <-{ty.(ty_size)} !"x";;
- let: "r" := new [ #0 ] in
- delete [ #1; "c"] ;; delete [ #ty.(ty_size); "x"] ;; "return" ["r"].
+ let: "c'" := !"c" in
+ "c'" <-{ty.(ty_size)} !"x";;
+ let: "r" := new [ #0 ] in
+ delete [ #1; "c"] ;; delete [ #ty.(ty_size); "x"] ;; "return" ["r"].
Lemma cell_set_type ty :
typed_instruction_ty [] [] [] (cell_set ty)
@@ -140,17 +140,16 @@ Section typing.
Proof.
apply type_fn; try apply _. move=> /= α ret arg. inv_vec arg=>c x. simpl_subst.
eapply type_deref; [solve_typing..|by apply read_own_move|done|].
- intros c'. simpl_subst.
- eapply type_let with (T1 := [c' â— _; x â— _]%TC)
- (T2 := λ _, [c' ◠&shr{α} cell ty;
+ intros d. simpl_subst.
+ eapply type_let with (T1 := [d â— _; x â— _]%TC)
+ (T2 := λ _, [d ◠&shr{α} cell ty;
x â— box (uninit ty.(ty_size))]%TC); try solve_typing; [|].
{ (* The core of the proof: Showing that the assignment is safe. *)
iAlways. iIntros (tid qE) "#HEAP #LFT Htl HE $".
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
- iIntros "[Hc' Hx]". rewrite {1}/elctx_interp big_opL_singleton /=.
- iDestruct "Hc'" as (l) "[EQ #Hshr]". iDestruct "EQ" as %[=->].
- iDestruct "Hshr" as (P) "[#HP #Hshr]".
- iDestruct "Hx" as (l') "[EQ [Hown >H†]]". iDestruct "EQ" as %[=->].
+ iIntros "[Hd Hx]". rewrite {1}/elctx_interp big_opL_singleton /=.
+ destruct d as [[]|]; try iDestruct "Hd" as "[]". iDestruct "Hd" as (P) "[#HP #Hshr]".
+ destruct x as [[]|]; try iDestruct "Hx" as "[]". iDestruct "Hx" as "[Hown >H†]".
iDestruct "Hown" as (vl') "[>H↦' Hown']".
iMod (na_bor_acc with "LFT Hshr HE Htl") as "(Hown & Htl & Hclose)"; [solve_ndisj..|].
iDestruct ("HP" with "Hown") as (vl) "[>H↦ Hown]".
@@ -163,8 +162,7 @@ Section typing.
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //.
iSplitR; iModIntro.
- iExists _. simpl. eauto.
- - iExists _. iSplit; first done. iFrame. iExists _. iFrame.
- rewrite uninit_own. auto. }
+ - iFrame. iExists _. iFrame. rewrite uninit_own. auto. }
intros v. simpl_subst. clear v.
eapply type_new; [solve_typing..|].
intros r. simpl_subst.
--
GitLab