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

WIP.

parent de9fc5a6
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/typing/borrow.v
+ 7
− 9
View file @ e6cb690a
......@@ -15,7 +15,7 @@ Section borrow.
Lemma tctx_borrow E L p n ty κ :
tctx_incl E L [p ◁ own_ptr n ty] [p ◁ &uniq{κ}ty; p ◁{κ} own_ptr n ty].
Proof.
iIntros (tid ??) "#LFT $ $ H".
iIntros (tid ?) "#LFT _ $ H".
rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
iDestruct "H" as ([[]|]) "[% Hown]"; try done. iDestruct "Hown" as "[Hmt ?]".
iMod (bor_create with "LFT Hmt") as "[Hbor Hext]". done.
......@@ -47,7 +47,7 @@ Section borrow.
lctx_lft_alive E L κ →
typed_instruction_ty E L [p ◁ &uniq{κ} own_ptr n ty] (!p) (&uniq{κ} ty).
Proof.
iIntros (Hκ tid qE) "#LFT $ HE HL Hp".
iIntros (Hκ tid) "#LFT HE $ HL Hp".
rewrite tctx_interp_singleton.
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
......@@ -77,7 +77,7 @@ Section borrow.
lctx_lft_alive E L κ →
typed_instruction_ty E L [p ◁ &shr{κ} own_ptr n ty] (!p) (&shr{κ} ty).
Proof.
iIntros (Hκ tid qE) "#LFT $ HE HL Hp".
iIntros (Hκ tid) "#LFT HE $ HL Hp".
rewrite tctx_interp_singleton.
iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
......@@ -103,10 +103,9 @@ Section borrow.
lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
typed_instruction_ty E L [p ◁ &uniq{κ} &uniq{κ'} ty] (!p) (&uniq{κ} ty).
Proof.
iIntros (Hκ Hincl tid qE) "#LFT $ HE HL Hp".
iIntros (Hκ Hincl tid) "#LFT #HE $ HL Hp".
rewrite tctx_interp_singleton.
iPoseProof (Hincl with "[#] [#]") as "Hincl".
{ by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
iDestruct (Hincl with "HL HE") as "#Hincl".
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
iMod (bor_exists with "LFT Hown") as (vl) "Hbor". done.
......@@ -137,9 +136,8 @@ Section borrow.
lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
typed_instruction_ty E L [p ◁ &shr{κ} &uniq{κ'} ty] (!p) (&shr{κ} ty).
Proof.
iIntros (Hκ Hincl tid qE) "#LFT $ HE HL Hp". rewrite tctx_interp_singleton.
iPoseProof (Hincl with "[#] [#]") as "Hincl".
{ by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
iIntros (Hκ Hincl tid) "#LFT HE $ HL Hp". rewrite tctx_interp_singleton.
iDestruct (Hincl with "HL HE") as "#Hincl".
iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hshr"; try done.
iDestruct "Hshr" as (l') "[H↦ Hown]".
......
theories/typing/fixpoint.v
+ 1
− 1
View file @ e6cb690a
......@@ -74,7 +74,7 @@ Section fixpoint.
Proof.
unfold eqtype, subtype, type_incl.
setoid_rewrite <-fixpointK_unfold; [| by apply type_contractive_ne, _..].
split; iIntros "_ _"; (iSplit; first done); iSplit; iIntros "!#*$".
split; iIntros (qL) "_ !# _"; (iSplit; first done); iSplit; iIntros "!#*$".
Qed.
End fixpoint.
......
theories/typing/product_split.v
+ 17
− 18
View file @ e6cb690a
......@@ -37,16 +37,16 @@ Section product_split.
(∀ tid ty vl, (ptr ty).(ty_own) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]⌝) →
∀ p, tctx_incl E L [p ◁ ptr $ product tyl] (hasty_ptr_offsets p ptr tyl 0).
Proof.
iIntros (Hsplit Hloc p tid q1 q2) "#LFT HE HL H".
iIntros (Hsplit Hloc p tid q) "#LFT #HE HL H".
iInduction tyl as [|ty tyl IH] "IH" forall (p).
{ iFrame "HE HL". rewrite tctx_interp_nil. done. }
rewrite product_cons. iMod (Hsplit with "LFT HE HL H") as "(HE & HL & H)".
{ rewrite tctx_interp_nil. auto. }
rewrite product_cons. iMod (Hsplit with "LFT HE HL H") as "(HL & H)".
cbn -[tctx_elt_interp]. rewrite tctx_interp_cons tctx_interp_singleton tctx_interp_cons.
iDestruct "H" as "[Hty Htyl]". iDestruct "Hty" as (v) "[Hp Hty]". iDestruct "Hp" as %Hp.
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 "HL [Htyl]") as "($ & Htyl)".
{ rewrite tctx_interp_singleton //. }
iClear "IH". rewrite (hasty_ptr_offsets_offset l) // -plus_n_O //.
Qed.
......@@ -59,7 +59,7 @@ Section product_split.
(∀ tid ty vl, (ptr ty).(ty_own) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]⌝) →
∀ p, tctx_incl E L (hasty_ptr_offsets p ptr tyl 0) [p ◁ ptr $ product tyl].
Proof.
iIntros (Hptr Htyl Hmerge Hloc p tid q1 q2) "#LFT HE HL H".
iIntros (Hptr Htyl Hmerge Hloc p tid q) "#LFT #HE HL H".
iInduction tyl as [|ty tyl IH] "IH" forall (p Htyl); first done.
rewrite product_cons. rewrite /= tctx_interp_singleton tctx_interp_cons.
iDestruct "H" as "[Hty Htyl]". iDestruct "Hty" as (v) "[Hp Hty]".
......@@ -68,16 +68,15 @@ Section product_split.
{ move:Hp. simpl. clear. destruct (eval_path p); last done.
destruct v; try done. destruct l0; try done. rewrite shift_loc_0. done. }
clear Hp. destruct tyl.
{ iDestruct (elctx_interp_persist with "HE") as "#HE'".
iDestruct (llctx_interp_persist with "HL") as "#HL'". iFrame "HE HL".
iClear "IH Htyl". iExists #l. rewrite product_nil. iSplitR; first done.
assert (eqtype E L (ptr ty) (ptr (product2 ty unit))) as [Hincl _].
{ assert (eqtype E L (ptr ty) (ptr (product2 ty unit))) as [Hincl _].
{ rewrite right_id. done. }
iDestruct (Hincl with "HE' HL'") as "#(_ & #Heq & _)". by iApply "Heq". }
iMod ("IH" with "[] HE HL [Htyl]") as "(HE & HL & Htyl)"; first done.
iDestruct (Hincl with "HL HE") as "#(_ & #Heq & _)".
iFrame. iClear "IH Htyl". iExists #l. rewrite product_nil. iSplitR; first done.
by iApply "Heq". }
iMod ("IH" with "[] HL [Htyl]") as "(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 "($ & $ & ?)";
iClear "IH". iMod (Hmerge with "LFT HE HL [Hty Htyl]") as "($ & ?)";
last by rewrite tctx_interp_singleton.
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton. iFrame.
iExists #l. iSplit; done.
......@@ -88,7 +87,7 @@ Section product_split.
tctx_incl E L [p ◁ own_ptr n $ product2 ty1 ty2]
[p ◁ own_ptr n ty1; p +ₗ #ty1.(ty_size) ◁ own_ptr n ty2].
Proof.
iIntros (tid q1 q2) "#LFT $ $ H".
iIntros (tid q) "#LFT _ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
iDestruct "H" as ([[]|]) "[#Hp H]"; try done.
iDestruct "H" as "[H >H†]". iDestruct "H" as (vl) "[>H↦ H]".
......@@ -106,7 +105,7 @@ Section product_split.
tctx_incl E L [p ◁ own_ptr n ty1; p +ₗ #ty1.(ty_size) ◁ own_ptr n ty2]
[p ◁ own_ptr n $ product2 ty1 ty2].
Proof.
iIntros (tid q1 q2) "#LFT $ $ H".
iIntros (tid q) "#LFT _ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "(Hp1 & H1)"; try done.
iDestruct "H1" as "(H↦1 & H†1)".
......@@ -143,7 +142,7 @@ Section product_split.
tctx_incl E L [p ◁ &uniq{κ} product2 ty1 ty2]
[p ◁ &uniq{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &uniq{κ} ty2].
Proof.
iIntros (tid q1 q2) "#LFT $ $ H".
iIntros (tid q) "#LFT _ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
iDestruct "H" as ([[]|]) "[Hp H]"; try done. iDestruct "Hp" as %Hp.
rewrite /= split_prod_mt. iMod (bor_sep with "LFT H") as "[H1 H2]".
......@@ -155,7 +154,7 @@ Section product_split.
tctx_incl E L [p ◁ &uniq{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &uniq{κ} ty2]
[p ◁ &uniq{κ} product2 ty1 ty2].
Proof.
iIntros (tid q1 q2) "#LFT $ $ H".
iIntros (tid q) "#LFT _ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 H1]"; try done.
iDestruct "Hp1" as %Hp1. iDestruct "H2" as (v2) "(Hp2 & H2)". rewrite /= Hp1.
......@@ -192,7 +191,7 @@ Section product_split.
tctx_incl E L [p ◁ &shr{κ} product2 ty1 ty2]
[p ◁ &shr{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &shr{κ} ty2].
Proof.
iIntros (tid q1 q2) "#LFT $ $ H".
iIntros (tid q) "#LFT _ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
iDestruct "H" as ([[]|]) "[Hp H]"; try iDestruct "H" as "[]".
iDestruct "H" as "[H1 H2]". iDestruct "Hp" as %Hp.
......@@ -203,7 +202,7 @@ Section product_split.
tctx_incl E L [p ◁ &shr{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &shr{κ} ty2]
[p ◁ &shr{κ} product2 ty1 ty2].
Proof.
iIntros (tid q1 q2) "#LFT $ $ H".
iIntros (tid q) "#LFT _ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 Hown1]"; try done.
iDestruct "Hp1" as %Hp1. iDestruct "H2" as ([[]|]) "[Hp2 Hown2]"; try done.
......
theories/typing/shr_bor.v
+ 8
− 9
View file @ e6cb690a
......@@ -20,9 +20,11 @@ Section shr_bor.
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 (? [|[[]|][]]) "#HE #HL H"; try done.
iDestruct (Hκ with "HE HL") as "#Hκ". iApply (ty2.(ty_shr_mono) with "Hκ").
iDestruct (Hty with "[] []") as "(_ & _ & #Hs1)"; [done..|clear Hty].
iIntros (?) "/= HL". iDestruct (Hκ with "HL") as "#Hincl".
iDestruct (Hty with "HL") as "#Hty". iIntros "!# #HE".
iIntros (? [|[[]|][]]) "H"; try done. iDestruct ("Hincl" with "HE") as "#Hκ".
iApply (ty2.(ty_shr_mono) with "Hκ").
iDestruct ("Hty" with "HE") as "(_ & _ & #Hs1)"; [done..|clear Hty].
by iApply "Hs1".
Qed.
Global Instance shr_mono_flip E L :
......@@ -64,11 +66,8 @@ Section typing.
lctx_lft_incl E L κ' κ →
tctx_incl E L [p ◁ &shr{κ}ty] [p ◁ &shr{κ'}ty; p ◁{κ} &shr{κ}ty].
Proof.
iIntros (Hκκ' tid ??) "#LFT HE HL H".
iDestruct (elctx_interp_persist with "HE") as "#HE'".
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.
iIntros (Hκκ' tid ?) "#LFT #HE HL H". iDestruct (Hκκ' with "HL HE") as "#Hκκ'".
iFrame. rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
iDestruct "H" as ([[]|]) "[% #Hshr]"; try done. iModIntro. iSplit.
- iExists _. iSplit. done. by iApply (ty_shr_mono with "Hκκ' Hshr").
- iExists _. auto.
......@@ -78,7 +77,7 @@ Section typing.
Copy ty → lctx_lft_alive E L κ → typed_read E L (&shr{κ}ty) ty (&shr{κ}ty).
Proof.
iIntros (Hcopy Halive) "!#".
iIntros ([[]|] tid F qE qL ?) "#LFT Htl HE HL #Hshr"; try done.
iIntros ([[]|] tid F qL ?) "#LFT #HE Htl HL #Hshr"; try done.
iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first set_solver.
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)".
......
theories/typing/uniq_bor.v
+ 10
− 11
View file @ e6cb690a
......@@ -46,9 +46,11 @@ Section uniq_bor.
Global Instance uniq_mono E L :
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 (Hκ with "[] []") as "#Hκ"; [done..|]. iSplit; iAlways.
intros κ1 κ2 Hκ ty1 ty2. rewrite eqtype_unfold=>Hty. iIntros (?) "HL".
iDestruct (Hty with "HL") as "#Hty". iDestruct (Hκ with "HL") as "#Hκ".
iIntros "!# #HE". iSplit; first done.
iDestruct ("Hty" with "HE") as "(_ & #Ho & #Hs)"; [done..|clear Hty].
iSpecialize ("Hκ" with "HE"). iSplit; iAlways.
- iIntros (? [|[[]|][]]) "H"; try done.
iApply (bor_shorten with "Hκ"). iApply bor_iff; last done.
iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]";
......@@ -109,7 +111,7 @@ Section typing.
Lemma tctx_share E L p κ ty :
lctx_lft_alive E L κ → tctx_incl E L [p ◁ &uniq{κ}ty] [p ◁ &shr{κ}ty].
Proof.
iIntros (Hκ ???) "#LFT HE HL Huniq".
iIntros (Hκ ??) "#LFT #HE HL Huniq".
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; [try done..|].
rewrite !tctx_interp_singleton /=.
iDestruct "Huniq" as ([[]|]) "[% Huniq]"; try done.
......@@ -121,11 +123,8 @@ Section typing.
lctx_lft_incl E L κ' κ →
tctx_incl E L [p ◁ &uniq{κ}ty] [p ◁ &uniq{κ'}ty; p ◁{κ'} &uniq{κ}ty].
Proof.
iIntros (Hκκ' tid ??) "#LFT HE HL H".
iDestruct (elctx_interp_persist with "HE") as "#HE'".
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.
iIntros (Hκκ' tid ?) "#LFT HE HL H". iDestruct (Hκκ' with "HL HE") as "#Hκκ'".
iFrame. rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
iDestruct "H" as ([[]|]) "[% Hb]"; try done.
iMod (rebor with "LFT Hκκ' Hb") as "[Hb Hext]". done. iModIntro.
iSplitL "Hb"; iExists _; auto.
......@@ -174,7 +173,7 @@ Section typing.
Copy ty → lctx_lft_alive E L κ → typed_read E L (&uniq{κ}ty) ty (&uniq{κ}ty).
Proof.
iIntros (Hcopy Halive) "!#".
iIntros ([[]|] tid F qE qL ?) "#LFT Htl HE HL Hown"; try done.
iIntros ([[]|] tid F qL ?) "#LFT #HE Htl HL Hown"; try done.
iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first set_solver.
iMod (bor_acc with "LFT Hown Hκ") as "[H↦ Hclose']"; first set_solver.
iDestruct "H↦" as (vl) "[>H↦ #Hown]".
......@@ -188,7 +187,7 @@ Section typing.
lctx_lft_alive E L κ → typed_write E L (&uniq{κ}ty) ty (&uniq{κ}ty).
Proof.
iIntros (Halive) "!#".
iIntros ([[]|] tid F qE qL ?) "#LFT HE HL Hown"; try done.
iIntros ([[]|] tid F qL ?) "#LFT HE HL Hown"; try done.
iMod (Halive with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
iMod (bor_acc with "LFT Hown Htok") as "[H↦ Hclose']". set_solver.
iDestruct "H↦" as (vl) "[>H↦ Hown]". rewrite ty.(ty_size_eq).
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment