From 9e7ddb930c3a9fe53095906587d753c417fdfbe1 Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org> Date: Thu, 10 Nov 2016 12:56:39 +0100 Subject: [PATCH] Fix the type of products. --- theories/perm.v | 2 +- theories/perm_incl.v | 190 +++++++++++++++++++------------- theories/type.v | 253 +++++++++++++++++-------------------------- theories/type_incl.v | 133 ++++++++++++++--------- theories/typing.v | 43 +++----- 5 files changed, 315 insertions(+), 306 deletions(-) diff --git a/theories/perm.v b/theories/perm.v index e268dacd..52f9eb2e 100644 --- a/theories/perm.v +++ b/theories/perm.v @@ -51,7 +51,7 @@ End Perm. Import Perm. -Notation "v â— ty" := (has_type v ty) +Notation "ν â— ty" := (has_type ν%E ty) (at level 75, right associativity) : perm_scope. Notation "κ ∋ Ï" := (extract κ Ï) diff --git a/theories/perm_incl.v b/theories/perm_incl.v index cca2d892..d236d6bd 100644 --- a/theories/perm_incl.v +++ b/theories/perm_incl.v @@ -109,86 +109,129 @@ Section props. destruct (eval_expr ν); last by iDestruct "Huniq" as "[]". iDestruct "Huniq" as (l) "[% Hown]". iMod (ty.(ty_share) _ lrustN with "Hown Htok") as "[Hown $]". - apply disjoint_union_l; solve_ndisj. done. iModIntro. - simpl. eauto. + apply disjoint_union_l; solve_ndisj. done. iIntros "!>/=". eauto. Qed. - Lemma split_own_prod tyl (q0: Qp) (ql : list Qp) (l : loc) tid : - length tyl = length ql → - (own (foldr Qp_plus q0 ql) (Î tyl)).(ty_own) tid [ #l] ⊣⊢ - â–· †{q0}(shift_loc l (0 + (Î tyl).(ty_size))%nat)…0 ∗ - [∗ list] qtyoffs ∈ (combine ql (combine_offs tyl 0)), - (own (qtyoffs.1) (qtyoffs.2.1)).(ty_own) - tid [ #(shift_loc l (qtyoffs.2.2))]. + Lemma perm_split_own_prod2 ty1 ty2 (q1 q2 : Qp) ν : + ν â— own (q1 + q2) (product2 ty1 ty2) ⇔ + ν â— own q1 ty1 ∗ ν +â‚— #ty1.(ty_size) â— own q2 ty2. Proof. - intros Hlen. - assert (REW: ∀ (l : loc) (Φ : loc → iProp Σ), - Φ l ⊣⊢ (∃ l0:loc, [ #l] = [ #l0] ∗ Φ l0)). - { intros l0 Φ. iSplit; iIntros "H". eauto. - iDestruct "H" as (l') "[Heq H]". iDestruct "Heq" as %[=]. subst. done. } - setoid_rewrite <-REW. clear REW. - rewrite big_sepL_sepL assoc split_prod_mt big_sepL_later. apply uPred.sep_proper. - - rewrite -{1}(shift_loc_0_nat l). generalize 0%nat at -3. revert ql Hlen. - induction tyl as [|ty tyl IH]; intros [|q ql] [=] offs. - + by rewrite big_sepL_nil !right_id. - + rewrite -heap_freeable_op_eq uPred.later_sep shift_loc_assoc_nat IH // - Nat.add_assoc big_sepL_cons. - iSplit; by iIntros "($&$&$)". - - generalize 0%nat. revert ql Hlen. - induction tyl as [|ty tyl IH]; intros [|q ql] [=] offs. done. - rewrite !big_sepL_cons IH //. + rewrite /has_type /own /sep /=. + destruct (eval_expr ν) as [[[]|?]|]; last first; split; iIntros (tid) "H/="; + (try by iDestruct "H" as "[_ []]"); (try by iDestruct "H" as (l) "[% _]"). + { by auto. } + - iDestruct "H" as (l') "(EQ & H & H†)". iDestruct "EQ" as %[=<-]. + iDestruct "H" as (vl) "[H↦ H]". iDestruct "H" as (vl1 vl2) "(>% & H1 & H2)". + subst. rewrite heap_mapsto_vec_app -heap_freeable_op_eq. + iDestruct "H†" as "[H†1 H†2]". iDestruct "H↦" as "[H↦1 H↦2]". + iAssert (â–· (length vl1 = ty_size ty1))%I with "[#]" as ">EQ". + { iNext. by iApply ty_size_eq. } + iDestruct "EQ" as %->. iSplitL "H↦1 H†1 H1". + + iExists _. iSplitR. done. iFrame. iExists _. by iFrame. + + iExists _. iSplitR. done. iFrame. iExists _. by iFrame. + - iDestruct "H" as "[H1 H2]". + iDestruct "H1" as (l') "(EQ & H↦1 & H†1)". iDestruct "EQ" as %[=<-]. + iDestruct "H2" as (l') "(EQ & H↦2 & H†2)". iDestruct "EQ" as %[=<-]. + iExists l. iSplitR. done. rewrite -heap_freeable_op_eq. 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. + iAssert (â–· (length vl1 = ty_size ty1))%I with "[#]" as ">EQ". + { iNext. by iApply ty_size_eq. } + iDestruct "EQ" as %->. iFrame. iExists vl1, vl2. iFrame. auto. Qed. + Fixpoint combine_offs (tyl : list type) (accu : nat) := + match tyl with + | [] => [] + | ty :: q => (ty, accu) :: combine_offs q (accu + ty.(ty_size)) + end. + Lemma perm_split_own_prod tyl (q : Qp) (ql : list Qp) ν : length tyl = length ql → foldr (λ (q : Qp) acc, q + acc)%Qc 0%Qc ql = q → ν â— own q (Î tyl) ⇔ foldr (λ qtyoffs acc, - (ν +â‚— #(qtyoffs.2.2:nat))%E â— own (qtyoffs.1) (qtyoffs.2.1) ∗ acc) + ν +â‚— #(qtyoffs.2.2:nat) â— own (qtyoffs.1) (qtyoffs.2.1) ∗ acc) ⊤ (combine ql (combine_offs tyl 0)). Proof. - intros Hlen Hq. assert (ql ≠[]). - { destruct ql as [|q0 ql]; last done. destruct q. simpl in *. by subst. } - unfold has_type. simpl eval_expr. destruct (eval_expr ν) as [[[|l|]|]|]; - try by (destruct tyl as [|ty0 tyl], ql as [|q0 ql]; try done; - by split; iIntros (tid) "H"; try done; - [iDestruct "H" as (l) "[% _]" || iDestruct "H" as "[]" | - iDestruct "H" as "[[]_]"]). - destruct (@exists_last _ ql) as (ql'&q0&->); first done. - apply uPred_equiv_perm_equiv=>tid. - assert (foldr Qp_plus (q0/2) (ql' ++ [q0/2]) = q)%Qp as <-. - { destruct q as [q ?]. apply Qp_eq. simpl in *. subst. clear. induction ql'. - by rewrite /fold_right /app Qp_div_2 Qcplus_0_r. by rewrite /= IHql'. } - rewrite /has_type /from_option split_own_prod ?Hlen ?app_length //. - clear -Hlen. revert ql' Hlen. generalize 0%nat at -2. - induction tyl as [|ty tyl IH]; destruct ql' as [|q ql']; intros [= Hlen]; try done. - - destruct tyl; last done. clear IH Hlen. - rewrite big_sepL_singleton /= /sep !right_id comm uPred.sep_exist_r. - apply uPred.exist_proper=>l0. - rewrite -{3}(Qp_div_2 q0) -{3}(right_id O plus ty.(ty_size)) - -heap_freeable_op_eq uPred.later_sep -!assoc. - iSplit; iIntros "[#Eq[?[??]]]"; iFrame "# ∗"; - iDestruct "Eq" as %[=]; subst; rewrite shift_loc_assoc_nat //. - - rewrite /= big_sepL_cons /sep -IH // !uPred.sep_exist_r uPred.sep_exist_l. - apply uPred.exist_proper=>l0. rewrite -!assoc /=. - by iSplit; iIntros "[$[$[$[$$]]]]". + revert q tyl ν. induction ql as [|q0 [|q1 ql] IH]=>q tyl ν Hlen Hq. + { destruct q. intros. simpl in *. by subst. } + - destruct tyl as [|ty0 [|ty1 tyl]]; try done. simpl in *. + assert (q0 = q) as ->. { apply Qp_eq. by rewrite -Hq Qcplus_0_r. } + rewrite /has_type /sep /=. + destruct (eval_expr ν) as [[[]|]|]; split; iIntros (tid) "H/="; + (try by iDestruct "H" as "[[] _]"); (try by iDestruct "H" as (l) "[% _]"); + (try by auto); rewrite (shift_loc_0 l) Nat.add_0_r. + + iSplitL; last done. iExists _. iSplitR. done. + iDestruct "H" as (l') "[Heq [H↦ H†]]". iDestruct "Heq" as %[=<-]. + iDestruct "H↦" as (vl) "[H↦ H]". + iDestruct "H" as (vl1 vl2) "(>% & Hown & >%)". subst. + rewrite app_nil_r. iFrame. iExists _. by iFrame. + + iExists l. iSplitR. done. + iDestruct "H" as "[H _]". iDestruct "H" as (l') "[Heq [H↦ H†]]". + iDestruct "Heq" as %[=<-]. iFrame. iDestruct "H↦" as (vl) "[H↦ Hown]". + iExists vl. iFrame. iExists vl, []. iFrame. rewrite app_nil_r. auto. + - destruct tyl as [|ty0 tyl]. done. + assert (Hpos : (0 < foldr (λ (q : Qp) acc, (q + acc)%Qc) 0%Qc (q1 :: ql))%Qc). + { apply Qcplus_pos_nonneg. apply Qp_prf. clear. induction ql. done. + apply Qcplus_nonneg_nonneg. apply Qclt_le_weak, Qp_prf. done. } + assert (q = q0 + mk_Qp _ Hpos)%Qp as ->. by by apply Qp_eq; rewrite -Hq. + injection Hlen; intro Hlen'. rewrite perm_split_own_prod2 IH //. + apply perm_sep_proper. + + rewrite /has_type /sep /=. + destruct (eval_expr ν) as [[[]|]|]; split; iIntros (tid) "H/="; + (try by iDestruct "H" as "[]"); (try by iDestruct "H" as (l) "[% _]"); + (try by auto); by rewrite shift_loc_0. + + cut (length tyl = length (q1 :: ql)); last done. clear. revert tyl. + generalize 0%nat. induction (q1 :: ql)=>offs -[|ty tyl] Hlen //. + apply perm_sep_proper. + * rewrite /has_type /sep /=. + destruct (eval_expr ν) as [[[]|]|]; split; iIntros (tid) "H/="; + (try by iDestruct "H" as "[]"); (try by iDestruct "H" as (l) "[% _]"); + (try by auto); by rewrite shift_loc_assoc_nat (comm plus). + * etransitivity. apply IHl. by injection Hlen. do 3 f_equiv. lia. + Qed. + + Lemma perm_split_uniq_borrow_prod2 ty1 ty2 κ ν : + ν â— &uniq{κ} (product2 ty1 ty2) ⇒ + ν â— &uniq{κ} ty1 ∗ ν +â‚— #(ty1.(ty_size)) â— &uniq{κ} ty2. + Proof. + rewrite /has_type /sep /product2 /=. + destruct (eval_expr ν) as [[[|l|]|]|]; + iIntros (tid) "H"; try iDestruct "H" as "[]"; + iDestruct "H" as (l0) "[EQ H]"; iDestruct "EQ" as %[=<-]. + rewrite /= split_prod_mt. iMod (borrow_split with "H") as "[H1 H2]". + set_solver. iSplitL "H1"; eauto. Qed. Lemma perm_split_uniq_borrow_prod tyl κ ν : ν â— &uniq{κ} (Î tyl) ⇒ foldr (λ tyoffs acc, - (ν +â‚— #(tyoffs.2:nat))%E â— &uniq{κ} (tyoffs.1) ∗ acc)%P + ν +â‚— #(tyoffs.2:nat) â— &uniq{κ} (tyoffs.1) ∗ acc)%P ⊤ (combine_offs tyl 0). Proof. - intros tid. unfold has_type. simpl eval_expr. + transitivity (ν +â‚— #0%nat â— &uniq{κ}Î tyl)%P. + { iIntros (tid) "H/=". rewrite /has_type /=. destruct (eval_expr ν)=>//. + iDestruct "H" as (l) "[Heq H]". iDestruct "Heq" as %[=->]. + rewrite shift_loc_0 /=. eauto. } + generalize 0%nat. induction tyl as [|ty tyl IH]=>offs. by iIntros (tid) "H/=". + etransitivity. apply perm_split_uniq_borrow_prod2. + iIntros (tid) "/=[$ H]". iApply IH. rewrite /has_type /=. + destruct (eval_expr ν) as [[[]|]|]=>//=. by rewrite shift_loc_assoc_nat. + Qed. + + Lemma perm_split_shr_borrow_prod2 ty1 ty2 κ ν : + ν â— &shr{κ} (product2 ty1 ty2) ⇒ + ν â— &shr{κ} ty1 ∗ ν +â‚— #(ty1.(ty_size)) â— &shr{κ} ty2. + Proof. + rewrite /has_type /sep /product2 /=. destruct (eval_expr ν) as [[[|l|]|]|]; - iIntros "H"; try iDestruct "H" as "[]"; - iDestruct "H" as (l0) "[EQ H]"; iDestruct "EQ" as %[=]. subst l0. - rewrite split_prod_mt. - iInduction (combine_offs tyl 0) as [|[ty offs] ll] "IH". by auto. - rewrite big_sepL_cons /=. - iMod (borrow_split with "H") as "[H0 H]". set_solver. - iMod ("IH" with "H") as "$". iModIntro. iExists _. eauto. + iIntros (tid) "H"; try iDestruct "H" as "[]"; + iDestruct "H" as (l0) "(EQ & H)"; iDestruct "EQ" as %[=<-]. + iDestruct "H" as (E1 E2) "(% & H1 & H2)". + iSplitL "H1"; iExists _; (iSplitR; [done|]); iApply (ty_shr_mono with "[]"); + try by iFrame. + set_solver. iApply lft_incl_refl. set_solver. iApply lft_incl_refl. Qed. Lemma perm_split_shr_borrow_prod tyl κ ν : @@ -197,19 +240,15 @@ Section props. (ν +â‚— #(tyoffs.2:nat))%E â— &shr{κ} (tyoffs.1) ∗ acc)%P ⊤ (combine_offs tyl 0). Proof. - intros tid. unfold has_type. simpl eval_expr. - destruct (eval_expr ν) as [[[|l|]|]|]; - iIntros "H"; try iDestruct "H" as "[]"; - iDestruct "H" as (l0) "[EQ H]"; iDestruct "EQ" as %[=]. subst l0. - simpl. iModIntro. - change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat). - generalize O at 2; intro i. - iInduction (combine_offs tyl 0) as [|[ty offs] ll] "IH" forall (i). by auto. - rewrite big_sepL_cons /=. iDestruct "H" as "[H0 H]". - setoid_rewrite <-Nat.add_succ_comm. iDestruct ("IH" $! (S i) with "H") as "$". - iExists _. iSplit. done. admit. - (* FIXME : namespaces problem. *) - Admitted. + transitivity (ν +â‚— #0%nat â— &shr{κ}Î tyl)%P. + { iIntros (tid) "H/=". rewrite /has_type /=. destruct (eval_expr ν)=>//. + iDestruct "H" as (l) "[Heq H]". iDestruct "Heq" as %[=->]. + rewrite shift_loc_0 /=. iExists _. by iFrame "∗%". } + generalize 0%nat. induction tyl as [|ty tyl IH]=>offs. by iIntros (tid) "H/=". + etransitivity. apply perm_split_shr_borrow_prod2. + iIntros (tid) "/=[$ H]". iApply IH. rewrite /has_type /=. + destruct (eval_expr ν) as [[[]|]|]=>//=. by rewrite shift_loc_assoc_nat. + Qed. Lemma reborrow_shr_perm_incl κ κ' ν ty : κ ⊑ κ' ∗ ν â— &shr{κ'}ty ⇒ ν â— &shr{κ}ty. @@ -218,8 +257,7 @@ Section props. destruct (eval_expr ν) as [[[|l|]|]|]; try by (iDestruct "Hκ'" as "[]" || iDestruct "Hκ'" as (l) "[% _]"). iDestruct "Hκ'" as (l') "[EQ Hκ']". iDestruct "EQ" as %[=]. subst l'. - iModIntro. iExists _. iSplit. done. - by iApply (ty_shr_mono with "Hord Hκ'"). + iModIntro. iExists _. iSplit. done. by iApply (ty_shr_mono with "Hord Hκ'"). Qed. Lemma borrowing_perm_incl κ Ï Ï1 Ï2 θ : @@ -235,7 +273,7 @@ Section props. iIntros (tid) "_ Hown". unfold has_type. destruct (eval_expr ν) as [[[|l|]|]|]; try by (iDestruct "Hown" as "[]" || iDestruct "Hown" as (l) "[% _]"). - iDestruct "Hown" as (l') "[EQ [Hf Hown]]". iDestruct "EQ" as %[=]. subst l'. + iDestruct "Hown" as (l') "[EQ [Hown Hf]]". iDestruct "EQ" as %[=]. subst l'. iApply (fupd_mask_mono lftN). done. iMod (borrow_create with "Hown") as "[Hbor Hext]". done. iSplitL "Hbor". by simpl; eauto. diff --git a/theories/type.v b/theories/type.v index b5d228ac..0e93d48f 100644 --- a/theories/type.v +++ b/theories/type.v @@ -1,3 +1,4 @@ +From Coq Require Import Qcanon. From iris.base_logic Require Import big_op. From iris.base_logic.lib Require Export thread_local. From iris.program_logic Require Import hoare. @@ -23,10 +24,10 @@ Context `{iris_typeG Σ}. Record type := { ty_size : nat; ty_dup : bool; ty_own : thread_id → list val → iProp Σ; - ty_shr : lifetime → thread_id → namespace → loc → iProp Σ; + ty_shr : lifetime → thread_id → coPset → loc → iProp Σ; ty_dup_persistent tid vl : ty_dup → PersistentP (ty_own tid vl); - ty_shr_persistent κ tid N l : PersistentP (ty_shr κ tid N l); + ty_shr_persistent κ tid E l : PersistentP (ty_shr κ tid E l); ty_size_eq tid vl : ty_own tid vl ⊢ length vl = ty_size; (* The mask for starting the sharing does /not/ include the @@ -40,13 +41,13 @@ Record type := give any. *) ty_share E N κ l tid q : mgmtE ⊥ nclose N → mgmtE ⊆ E → &{κ} (l ↦∗: ty_own tid) ⊢ q.[κ] ={E}=∗ ty_shr κ tid N l ∗ q.[κ]; - ty_shr_mono κ κ' tid N l : - κ' ⊑ κ ⊢ ty_shr κ tid N l → ty_shr κ' tid N l; - ty_shr_acc κ tid E N l q : - ty_dup → mgmtE ∪ nclose N ⊆ E → - ty_shr κ tid N l ⊢ - q.[κ] ∗ tl_own tid N ={E}=∗ ∃ q', â–·l ↦∗{q'}: ty_own tid ∗ - (â–·l ↦∗{q'}: ty_own tid ={E}=∗ q.[κ] ∗ tl_own tid N) + ty_shr_mono κ κ' tid E E' l : E ⊆ E' → + κ' ⊑ κ ⊢ ty_shr κ tid E l -∗ ty_shr κ' tid E' l; + ty_shr_acc κ tid E F l q : + ty_dup → mgmtE ∪ F ⊆ E → + ty_shr κ tid F l ⊢ + q.[κ] ∗ tl_own tid F ={E}=∗ ∃ q', â–·l ↦∗{q'}: ty_own tid ∗ + (â–·l ↦∗{q'}: ty_own tid ={E}=∗ q.[κ] ∗ tl_own tid F) }. Global Existing Instances ty_shr_persistent ty_dup_persistent. @@ -82,11 +83,11 @@ Next Obligation. done. set_solver. Qed. Next Obligation. - iIntros (st κ κ' tid N l) "#Hord H". iDestruct "H" as (vl) "[Hf Hown]". + intros st κ κ' tid E E' l ?. iIntros "#Hord H". iDestruct "H" as (vl) "[Hf Hown]". iExists vl. iFrame. by iApply (frac_borrow_shorten with "Hord"). Qed. Next Obligation. - intros st κ tid N E l q ??. iIntros "#Hshr[Hlft $]". + intros st κ tid E F l q ??. iIntros "#Hshr[Hlft $]". iDestruct "Hshr" as (vl) "[Hf Hown]". iMod (frac_borrow_acc with "[] Hf Hlft") as (q') "[Hmt Hclose]"; first set_solver. @@ -119,7 +120,7 @@ Section types. we really need [False] to prove [ty_incl_emp]. *) Program Definition emp := {| ty_size := 0; ty_dup := true; - ty_own tid vl := False%I; ty_shr κ tid N l := False%I |}. + ty_own tid vl := False%I; ty_shr κ tid E l := False%I |}. Next Obligation. iIntros (tid vl) "[]". Qed. Next Obligation. iIntros (????????) "Hb Htok". @@ -127,7 +128,7 @@ Section types. iMod (borrow_split with "Hb") as "[_ Hb]". set_solver. iMod (borrow_persistent with "Hb Htok") as "[>[] _]". set_solver. Qed. - Next Obligation. iIntros (?????) "_ []". Qed. + Next Obligation. intros. iIntros "_ []". Qed. Next Obligation. intros. iIntros "[]". Qed. Program Definition unit : type := @@ -142,8 +143,6 @@ Section types. {| st_size := 1; st_own tid vl := (∃ z:Z, vl = [ #z ])%I |}. Next Obligation. iIntros (tid vl) "H". iDestruct "H" as (z) "%". by subst. Qed. - (* TODO own and uniq_borrow are very similar. They could probably - somehow share some bits.. *) Program Definition own (q : Qp) (ty : type) := {| ty_size := 1; ty_dup := false; ty_own tid vl := @@ -153,11 +152,10 @@ Section types. Since this assertion is timeless, this should not cause problems. *) - (∃ l:loc, vl = [ #l ] ∗ â–· †{q}l…ty.(ty_size) - ∗ â–· l ↦∗: ty.(ty_own) tid)%I; - ty_shr κ tid N l := + (∃ l:loc, vl = [ #l ] ∗ â–· l ↦∗: ty.(ty_own) tid ∗ â–· †{q}l…ty.(ty_size))%I; + ty_shr κ tid E l := (∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗ - ∀ q', â–¡ (q'.[κ] ={mgmtE ∪ N, mgmtE}â–·=∗ ty.(ty_shr) κ tid N l' ∗ q'.[κ]))%I + ∀ q', â–¡ (q'.[κ] ={mgmtE ∪ E, mgmtE}â–·=∗ ty.(ty_shr) κ tid E l' ∗ q'.[κ]))%I |}. Next Obligation. done. Qed. Next Obligation. @@ -171,7 +169,7 @@ Section types. iMod (borrow_split with "Hb2") as "[EQ Hb2]". set_solver. iMod (borrow_persistent with "EQ Htok") as "[>% $]". set_solver. subst. rewrite heap_mapsto_vec_singleton. - iMod (borrow_split with "Hb2") as "[_ Hb2]". set_solver. + iMod (borrow_split with "Hb2") as "[Hb2 _]". set_solver. iMod (borrow_fracture (λ q, l ↦{q} #l')%I with "Hb1") as "Hbf". set_solver. rewrite /borrow. iDestruct "Hb2" as (i) "(#Hpb&Hpbown)". iMod (inv_alloc N _ (idx_borrow_own 1 i ∨ ty_shr ty κ tid N l')%I @@ -190,14 +188,15 @@ Section types. - iIntros "!>". iNext. iMod ("Hclose" with "[]") as "_"; by eauto. Qed. Next Obligation. - iIntros (_ ty κ κ' tid N l) "#Hκ #H". iDestruct "H" as (l') "[Hfb Hvs]". + intros _ ty κ κ' tid E E' l ?. iIntros "#Hκ #H". iDestruct "H" as (l') "[Hfb Hvs]". iExists l'. iSplit. by iApply (frac_borrow_shorten with "[]"). iIntros (q') "!#Htok". + iApply step_fupd_mask_mono. reflexivity. apply union_preserving_l. eassumption. iMod (lft_incl_acc with "Hκ Htok") as (q'') "[Htok Hclose]". set_solver. iMod ("Hvs" $! q'' with "Htok") as "Hvs'". iIntros "!>". iNext. iMod "Hvs'" as "[Hshr Htok]". iMod ("Hclose" with "Htok"). iFrame. - by iApply (ty.(ty_shr_mono) with "Hκ"). + iApply (ty.(ty_shr_mono) with "Hκ"); last done. done. Qed. Next Obligation. done. Qed. @@ -205,10 +204,10 @@ Section types. {| ty_size := 1; ty_dup := false; ty_own tid vl := (∃ l:loc, vl = [ #l ] ∗ &{κ} l ↦∗: ty.(ty_own) tid)%I; - ty_shr κ' tid N l := + ty_shr κ' tid E l := (∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗ ∀ q', â–¡ (q'.[κ â‹… κ'] - ={mgmtE ∪ N, mgmtE}â–·=∗ ty.(ty_shr) (κ⋅κ') tid N l' ∗ q'.[κ⋅κ']))%I + ={mgmtE ∪ E, mgmtE}â–·=∗ ty.(ty_shr) (κ⋅κ') tid E l' ∗ q'.[κ⋅κ']))%I |}. Next Obligation. done. Qed. Next Obligation. @@ -239,162 +238,110 @@ Section types. - iIntros "!>". iNext. iMod ("Hclose" with "[]") as "_"; by eauto. Qed. Next Obligation. - iIntros (κ0 ty κ κ' tid N l) "#Hκ #H". iDestruct "H" as (l') "[Hfb Hvs]". - iAssert (κ0⋅κ' ⊑ κ0⋅κ) as "#Hκ0". + intros κ0 ty κ κ' tid E E' l ?. iIntros "#Hκ #H". + iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0⋅κ' ⊑ κ0⋅κ) as "#Hκ0". { iApply lft_incl_lb. iSplit. - iApply lft_le_incl. by exists κ'. - iApply lft_incl_trans. iSplit; last done. iApply lft_le_incl. exists κ0. apply (comm _). } iExists l'. iSplit. by iApply (frac_borrow_shorten with "[]"). iIntros (q) "!#Htok". + iApply step_fupd_mask_mono. reflexivity. apply union_preserving_l. eassumption. iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]". set_solver. iMod ("Hvs" $! q' with "Htok") as "Hclose'". iIntros "!>". iNext. iMod "Hclose'" as "[#Hshr Htok]". iMod ("Hclose" with "Htok") as "$". - by iApply (ty_shr_mono with "Hκ0"). + iApply (ty_shr_mono with "Hκ0"); last done. done. Qed. Next Obligation. done. Qed. Program Definition shared_borrow (κ : lifetime) (ty : type) : type := {| st_size := 1; - st_own tid vl := (∃ l:loc, vl = [ #l ] ∗ ty.(ty_shr) κ tid lrustN l)%I |}. + st_own tid vl := + (∃ (l:loc), vl = [ #l ] ∗ ty.(ty_shr) κ tid lrustN l)%I |}. Next Obligation. iIntros (κ ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst. Qed. - Fixpoint combine_offs (tyl : list type) (accu : nat) := - match tyl with - | [] => [] - | ty :: q => (ty, accu) :: combine_offs q (accu + ty.(ty_size)) - end. - - Lemma list_ty_type_eq tid (tyl : list type) (vll : list (list val)) : - length tyl = length vll → - ([∗ list] tyvl ∈ combine tyl vll, ty_own (tyvl.1) tid (tyvl.2)) - ⊢ length (concat vll) = sum_list_with ty_size tyl. - Proof. - revert vll; induction tyl as [|ty tyq IH]; destruct vll; - iIntros (EQ) "Hown"; try done. - rewrite big_sepL_cons app_length /=. iDestruct "Hown" as "[Hown Hownq]". - iDestruct (ty.(ty_size_eq) with "Hown") as %->. - iDestruct (IH with "[-]") as %->; auto. - Qed. - - Lemma split_prod_mt tid tyl l q : + Lemma split_prod_mt tid ty1 ty2 q l : (l ↦∗{q}: λ vl, - ∃ vll, vl = concat vll ∗ length tyl = length vll - ∗ [∗ list] tyvl ∈ combine tyl vll, ty_own (tyvl.1) tid (tyvl.2))%I - ⊣⊢ [∗ list] tyoffs ∈ combine_offs tyl 0, - shift_loc l (tyoffs.2) ↦∗{q}: ty_own (tyoffs.1) tid. - Proof. - rewrite -{1}(shift_loc_0_nat l). generalize 0%nat. - induction tyl as [|ty tyl IH]=>/= offs. - - iSplit; iIntros "_". by iApply big_sepL_nil. - iExists []. iSplit. by iApply heap_mapsto_vec_nil. - iExists []. repeat iSplit; try done. by iApply big_sepL_nil. - - rewrite big_sepL_cons -IH. iSplit. - + iIntros "H". iDestruct "H" as (vl) "[Hmt H]". - iDestruct "H" as ([|vl0 vll]) "(%&Hlen&Hown)"; - iDestruct "Hlen" as %Hlen; inversion Hlen; subst. - rewrite big_sepL_cons heap_mapsto_vec_app/=. - iDestruct "Hmt" as "[Hmth Hmtq]"; iDestruct "Hown" as "[Hownh Hownq]". - iDestruct (ty.(ty_size_eq) with "Hownh") as %->. - iSplitL "Hmth Hownh". iExists vl0. by iFrame. - iExists (concat vll). iSplitL "Hmtq"; last by eauto. - by rewrite shift_loc_assoc_nat. - + iIntros "[Hmth H]". iDestruct "H" as (vl) "[Hmtq H]". - iDestruct "H" as (vll) "(%&Hlen&Hownq)". subst. - iDestruct "Hmth" as (vlh) "[Hmth Hownh]". iDestruct "Hlen" as %->. - iExists (vlh ++ concat vll). - rewrite heap_mapsto_vec_app shift_loc_assoc_nat. - iDestruct (ty.(ty_size_eq) with "Hownh") as %->. iFrame. - iExists (vlh :: vll). rewrite big_sepL_cons. iFrame. auto. - Qed. - - Fixpoint nat_rec_shift {A : Type} (x : A) (f : nat → A → A) (n0 n : nat) := - match n with - | O => x - | S n => f n0 (nat_rec_shift x f (S n0) n) - end. - - Lemma split_prod_namespace tid (N : namespace) n : - ∃ E, (tl_own tid N ⊣⊢ tl_own tid E - ∗ nat_rec_shift True (λ i P, tl_own tid (N .@ i) ∗ P) 0%nat n) - ∧ (∀ i, i < 0 → nclose (N .@ i) ⊆ E)%nat. + ∃ vl1 vl2, vl = vl1 ++ vl2 ∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I + ⊣⊢ l ↦∗{q}: ty1.(ty_own) tid ∗ shift_loc l ty1.(ty_size) ↦∗{q}: ty2.(ty_own) tid. Proof. - generalize 0%nat. induction n as [|n IH]. - - eexists. split. by rewrite right_id. intros. apply nclose_subseteq. - - intros i. destruct (IH (S i)) as [E [IH1 IH2]]. - eexists (E ∖ (N .@ i))%I. split. - + simpl. rewrite IH1 assoc -tl_own_union; last set_solver. - f_equiv; last done. f_equiv. rewrite (comm union). - apply union_difference_L. apply IH2. lia. - + intros. assert (i0 ≠i)%nat by lia. solve_ndisj. + iSplit; iIntros "H". + - iDestruct "H" as (vl) "[H↦ H]". iDestruct "H" as (vl1 vl2) "(% & H1 & H2)". + subst. rewrite heap_mapsto_vec_app. iDestruct "H↦" as "[H↦1 H↦2]". + iDestruct (ty_size_eq with "H1") as %->. + iSplitL "H1 H↦1"; iExists _; iFrame. + - iDestruct "H" as "[H1 H2]". iDestruct "H1" as (vl1) "[H↦1 H1]". + iDestruct "H2" as (vl2) "[H↦2 H2]". iExists (vl1 ++ vl2). + rewrite heap_mapsto_vec_app. iDestruct (ty_size_eq with "H1") as %->. + iFrame. iExists _, _. by iFrame. Qed. - Program Definition product (tyl : list type) := - {| ty_size := sum_list_with ty_size tyl; ty_dup := forallb ty_dup tyl; - ty_own tid vl := - (∃ vll, vl = concat vll ∗ length tyl = length vll ∗ - [∗ list] tyvl ∈ combine tyl vll, tyvl.1.(ty_own) tid (tyvl.2))%I; - ty_shr κ tid N l := - ([∗ list] i ↦ tyoffs ∈ combine_offs tyl 0, - tyoffs.1.(ty_shr) κ tid (N .@ i) (shift_loc l (tyoffs.2)))%I - |}. - Next Obligation. - intros tyl tid vl Hfa. - cut (∀ vll, PersistentP ([∗ list] tyvl ∈ combine tyl vll, - ty_own (tyvl.1) tid (tyvl.2))). by apply _. - clear vl. induction tyl as [|ty tyl IH]=>[|[|vl vll]]; try by apply _. - edestruct andb_prop_elim as [Hduph Hdupq]. by apply Hfa. - rewrite /PersistentP /= big_sepL_cons. - iIntros "?". by iApply persistentP. - Qed. + Program Definition product2 (ty1 ty2 : type) := + {| ty_size := ty1.(ty_size) + ty2.(ty_size); + ty_dup := ty1.(ty_dup) && ty2.(ty_dup); + ty_own tid vl := (∃ vl1 vl2, + vl = vl1 ++ vl2 ∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I; + ty_shr κ tid E l := + (∃ E1 E2, â– (E1 ⊥ E2 ∧ E1 ⊆ E ∧ E2 ⊆ E) ∗ + ty1.(ty_shr) κ tid E1 l ∗ + ty2.(ty_shr) κ tid E2 (shift_loc l ty1.(ty_size)))%I |}. + Next Obligation. intros ty1 ty2 tid vl [Hdup1 Hdup2]%andb_True. apply _. Qed. Next Obligation. - iIntros (tyl tid vl) "Hown". iDestruct "Hown" as (vll) "(%&%&Hown)". - subst. by iApply (list_ty_type_eq with "Hown"). + iIntros (ty1 ty2 tid vl) "H". iDestruct "H" as (vl1 vl2) "(% & H1 & H2)". + subst. rewrite app_length !ty_size_eq. + iDestruct "H1" as %->. iDestruct "H2" as %->. done. Qed. Next Obligation. - intros tyl E N κ l tid q ??. rewrite split_prod_mt. - change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat). generalize O at 3. - induction (combine_offs tyl 0) as [|[ty offs] ll IH]. - - iIntros (?) "_$!>". by rewrite big_sepL_nil. - - iIntros (i) "Hown Htoks". rewrite big_sepL_cons. - iMod (borrow_split with "Hown") as "[Hownh Hownq]". set_solver. - iMod (IH (S i)%nat with "Hownq Htoks") as "[#Hshrq Htoks]". - iMod (ty.(ty_share) _ (N .@ (i+0)%nat) with "Hownh Htoks") as "[#Hshrh $]". - solve_ndisj. done. - iModIntro. rewrite big_sepL_cons. iFrame "#". - iApply big_sepL_mono; last done. intros. by rewrite /= Nat.add_succ_r. + intros ty1 ty2 E N κ l tid q ??. iIntros "/=H Htok". + rewrite split_prod_mt. + iMod (borrow_split with "H") as "[H1 H2]". set_solver. + iMod (ty1.(ty_share) _ (N .@ 1) with "H1 Htok") as "[? Htok]". solve_ndisj. done. + iMod (ty2.(ty_share) _ (N .@ 2) with "H2 Htok") as "[? $]". solve_ndisj. done. + iModIntro. iExists (N .@ 1). iExists (N .@ 2). iFrame. + iPureIntro. split. solve_ndisj. split; apply nclose_subseteq. Qed. Next Obligation. - iIntros (tyl κ κ' tid N l) "#Hκ #H". iApply big_sepL_impl. - iSplit; last done. iIntros "!#*/=_#H'". by iApply (ty_shr_mono with "Hκ"). + intros ty1 ty2 κ κ' tid E E' l ?. iIntros "/=#H⊑ H". + iDestruct "H" as (N1 N2) "(% & H1 & H2)". iExists N1, N2. + iSplit. iPureIntro. set_solver. + iSplitL "H1"; by iApply (ty_shr_mono with "H⊑"). Qed. Next Obligation. - intros tyl κ tid E N l q DUP ?. setoid_rewrite split_prod_mt. generalize 0%nat. - change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat). - destruct (split_prod_namespace tid N (length tyl)) as [Ef [EQ _]]. - setoid_rewrite ->EQ. clear EQ. generalize 0%nat. - revert q. induction tyl as [|tyh tyq IH]. - - iIntros (q i offs) "_$!>". iExists 1%Qp. rewrite big_sepL_nil. auto. - - simpl in DUP. destruct (andb_prop_elim _ _ DUP) as [DUPh DUPq]. simpl. - iIntros (q i offs) "#Hshr([Htokh Htokq]&Htlf&Htlh&Htlq)". - rewrite big_sepL_cons Nat.add_0_r. - iDestruct "Hshr" as "[Hshrh Hshrq]". setoid_rewrite <-Nat.add_succ_comm. - iMod (IH with "Hshrq [$Htokq $Htlf $Htlq]") as (q'q) "[Hownq Hcloseq]". - iMod (tyh.(ty_shr_acc) with "Hshrh [$Htokh $Htlh]") as (q'h) "[Hownh Hcloseh]". - by pose proof (nclose_subseteq N i); set_solver. - destruct (Qp_lower_bound q'h q'q) as (q' & q'0h & q'0q & -> & ->). - iExists q'. iModIntro. rewrite big_sepL_cons. - rewrite -heap_mapsto_vec_prop_op; last apply ty_size_eq. - iDestruct "Hownh" as "[$ Hownh1]". - rewrite (big_sepL_proper (λ _ x, _ ↦∗{_}: _)%I); last first. - { intros. rewrite -heap_mapsto_vec_prop_op; last apply ty_size_eq. - instantiate (1:=λ _ y, _). simpl. reflexivity. } - rewrite big_sepL_sepL. iDestruct "Hownq" as "[$ Hownq1]". - iIntros "[Hh Hq]". rewrite (lft_own_split κ q). - iMod ("Hcloseh" with "[$Hh $Hownh1]") as "[$$]". iApply "Hcloseq". by iFrame. + intros ty1 ty2 κ tid E F l q [Hdup1 Hdup2]%andb_True ?. + iIntros "H[[Htok1 Htok2] Htl]". iDestruct "H" as (E1 E2) "(% & H1 & H2)". + assert (F = E1 ∪ E2 ∪ F∖(E1 ∪ E2)) as ->. + { rewrite -union_difference_L; set_solver. } + repeat setoid_rewrite tl_own_union; first last. + set_solver. set_solver. set_solver. set_solver. + iDestruct "Htl" as "[[Htl1 Htl2] $]". + iMod (ty1.(ty_shr_acc) with "H1 [$Htok1 $Htl1]") as (q1) "[H1 Hclose1]". set_solver. + iMod (ty2.(ty_shr_acc) with "H2 [$Htok2 $Htl2]") as (q2) "[H2 Hclose2]". set_solver. + destruct (Qp_lower_bound q1 q2) as (qq & q'1 & q'2 & -> & ->). iExists qq. + iDestruct "H1" as (vl1) "[H↦1 H1]". iDestruct "H2" as (vl2) "[H↦2 H2]". + rewrite -!heap_mapsto_vec_op_eq !split_prod_mt. + iAssert (â–· (length vl1 = ty1.(ty_size)))%I with "[#]" as ">%". + { iNext. by iApply ty_size_eq. } + iAssert (â–· (length vl2 = ty2.(ty_size)))%I with "[#]" as ">%". + { iNext. by iApply ty_size_eq. } + iDestruct "H↦1" as "[H↦1 H↦1f]". iDestruct "H↦2" as "[H↦2 H↦2f]". + iIntros "!>". iSplitL "H↦1 H1 H↦2 H2". + - iNext. iSplitL "H↦1 H1". iExists vl1. by iFrame. iExists vl2. by iFrame. + - iIntros "[H1 H2]". + iDestruct "H1" as (vl1') "[H↦1 H1]". iDestruct "H2" as (vl2') "[H↦2 H2]". + iAssert (â–· (length vl1' = ty1.(ty_size)))%I with "[#]" as ">%". + { iNext. by iApply ty_size_eq. } + iAssert (â–· (length vl2' = ty2.(ty_size)))%I with "[#]" as ">%". + { iNext. by iApply ty_size_eq. } + iCombine "H↦1" "H↦1f" as "H↦1". iCombine "H↦2" "H↦2f" as "H↦2". + rewrite !heap_mapsto_vec_op; try by congruence. + iDestruct "H↦1" as "[_ H↦1]". iDestruct "H↦2" as "[_ H↦2]". + iMod ("Hclose1" with "[H1 H↦1]") as "[$$]". by iExists _; iFrame. + iMod ("Hclose2" with "[H2 H↦2]") as "[$$]". by iExists _; iFrame. done. Qed. + Definition product (tyl : list type) := fold_right product2 unit tyl. + Lemma split_sum_mt l tid q tyl : (l ↦∗{q}: λ vl, ∃ (i : nat) vl', vl = #i :: vl' ∗ ty_own (nth i tyl emp) tid vl')%I @@ -450,13 +397,13 @@ Section types. iMod (borrow_fracture with "[-]") as "H"; last by eauto. set_solver. iFrame. Qed. Next Obligation. - intros n tyl Hn κ κ' tid N l. iIntros "#Hord H". + intros n tyl Hn κ κ' tid E E' l ?. iIntros "#Hord H". iDestruct "H" as (i) "[Hown0 Hown]". iExists i. iSplitL "Hown0". by iApply (frac_borrow_shorten with "Hord"). - by iApply ((nth i tyl emp).(ty_shr_mono) with "Hord"). + iApply ((nth i tyl emp).(ty_shr_mono) with "Hord"); last done. done. Qed. Next Obligation. - intros n tyl Hn κ tid E N l q Hdup%Is_true_eq_true ?. + intros n tyl Hn κ tid E F l q Hdup%Is_true_eq_true ?. iIntros "#H[[Htok1 Htok2] Htl]". setoid_rewrite split_sum_mt. iDestruct "H" as (i) "[Hshr0 Hshr]". iMod (frac_borrow_acc with "[] Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver. diff --git a/theories/type_incl.v b/theories/type_incl.v index 8d78a7fa..7f3c8251 100644 --- a/theories/type_incl.v +++ b/theories/type_incl.v @@ -52,7 +52,7 @@ Section ty_incl. Proof. iIntros (Hincl tid) "H/=". iMod (Hincl with "H") as "[#Howni #Hshri]". iModIntro. iSplit; iIntros "!#*H". - - iDestruct "H" as (l) "(%&H†&Hmt)". subst. iExists _. iSplit. done. + - iDestruct "H" as (l) "(%&Hmt&H†)". subst. iExists _. iSplit. done. iDestruct "Hmt" as (vl') "[Hmt Hown]". iNext. iDestruct (ty_size_eq with "Hown") as %<-. iDestruct ("Howni" $! _ with "Hown") as "Hown". @@ -81,76 +81,107 @@ Section ty_incl. iMod (lft_incl_acc with "Hincl' Htok") as (q'') "[Htok Hclose]". set_solver. iMod ("Hupd" with "*Htok") as "Hupd'". iModIntro. iNext. iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$". - iApply (ty_shr_mono with "Hincl' H"). + by iApply (ty_shr_mono with "Hincl' H"). Qed. Lemma lft_incl_ty_incl_shared_borrow ty κ1 κ2 : ty_incl (κ1 ⊑ κ2) (&shr{κ2}ty) (&shr{κ1}ty). Proof. iIntros (tid) "#Hincl!>". iSplit; iIntros "!#*H". - - iDestruct "H" as (l) "[% Hown]". subst. iExists _. iSplit. done. - by iApply (ty.(ty_shr_mono) with "Hincl"). + - iDestruct "H" as (l) "(% & H)". subst. iExists _. + iSplit. done. by iApply (ty.(ty_shr_mono) with "Hincl"). - iDestruct "H" as (vl) "#[Hfrac Hty]". iSplit; last done. iExists vl. iFrame "#". iNext. - iDestruct "Hty" as (l0) "[% Hty]". subst. iExists _. iSplit. done. + iDestruct "Hty" as (l0) "(% & Hty)". subst. iExists _. iSplit. done. by iApply (ty_shr_mono with "Hincl Hty"). Qed. (* We have the additional hypothesis that Ï should be duplicable. The only way I can see to circumvent this limitation is to deeply embed permissions (and their inclusion). Not sure this is worth it. *) + Lemma ty_incl_prod2 Ï ty11 ty12 ty21 ty22 : + Duplicable Ï â†’ ty_incl Ï ty11 ty12 → ty_incl Ï ty21 ty22 → + ty_incl Ï (product2 ty11 ty21) (product2 ty12 ty22). + Proof. + iIntros (HÏ Hincl1 Hincl2 tid) "#HÏ". + iMod (Hincl1 with "HÏ") as "[#Ho1#Hs1]". iMod (Hincl2 with "HÏ") as "[#Ho2#Hs2]". + iSplitL; iIntros "!>!#*H/=". + - iDestruct "H" as (vl1 vl2) "(% & H1 & H2)". iExists _, _. iSplit. done. + iSplitL "H1". iApply ("Ho1" with "H1"). iApply ("Ho2" with "H2"). + - iDestruct "H" as (E1 E2) "(% & H1 & H2)". + iDestruct ("Hs1" with "*H1") as "[H1 EQ]". iDestruct ("Hs2" with "*H2") as "[H2 %]". + iDestruct "EQ" as %->. iSplit; last by iPureIntro; f_equal. + iExists _, _. by iFrame. + Qed. + Lemma ty_incl_prod Ï tyl1 tyl2 : Duplicable Ï â†’ Forall2 (ty_incl Ï) tyl1 tyl2 → ty_incl Ï (Î tyl1) (Î tyl2). + Proof. intros HÏ HFA. induction HFA. done. by apply ty_incl_prod2. Qed. + + Lemma ty_incl_prod2_assoc1 Ï ty1 ty2 ty3 : + ty_incl Ï (product2 ty1 (product2 ty2 ty3)) (product2 (product2 ty1 ty2) ty3). + Proof. + iIntros (tid) "_!>". iSplit; iIntros "!#/=*H". + - iDestruct "H" as (vl1 vl') "(% & Ho1 & H)". + iDestruct "H" as (vl2 vl3) "(% & Ho2 & Ho3)". subst. + iExists _, _. iSplit. by rewrite assoc. iFrame. iExists _, _. by iFrame. + - iDestruct "H" as (E1 E2') "(% & Hs1 & H)". + iDestruct "H" as (E2 E3) "(% & Hs2 & Hs3)". rewrite shift_loc_assoc_nat. + iSplit; last by rewrite assoc. + iExists (E1 ∪ E2), E3. iSplit. by iPureIntro; set_solver. iFrame. + iExists E1, E2. iSplit. by iPureIntro; set_solver. by iFrame. + Qed. + + Lemma ty_incl_prod2_assoc2 Ï ty1 ty2 ty3 : + ty_incl Ï (product2 (product2 ty1 ty2) ty3) (product2 ty1 (product2 ty2 ty3)). Proof. - intros HÏ HFA. iIntros (tid) "#HÏ". iSplitL "". - - assert (Himpl : Ï tid ={⊤}=∗ - â–¡ (∀ vll, length tyl1 = length vll → - ([∗ list] tyvl ∈ combine tyl1 vll, ty_own (tyvl.1) tid (tyvl.2)) - → ([∗ list] tyvl ∈ combine tyl2 vll, ty_own (tyvl.1) tid (tyvl.2)))). - { induction HFA as [|ty1 ty2 tyl1 tyl2 Hincl HFA IH]. - - iIntros "_!>!#* _ _". by rewrite big_sepL_nil. - - iIntros "#HÏ". iMod (IH with "HÏ") as "#Hqimpl". - iMod (Hincl with "HÏ") as "[#Hhimpl _]". - iIntros "!>!#*%". destruct vll as [|vlh vllq]. done. - rewrite !big_sepL_cons. - iIntros "[Hh Hq]". iSplitL "Hh". by iApply "Hhimpl". - iApply ("Hqimpl" with "[] Hq"). iPureIntro. simpl in *. congruence. } - iMod (Himpl with "HÏ") as "#Himpl". iIntros "!>!#*H". - iDestruct "H" as (vll) "(%&%&H)". iExists _. iSplit. done. iSplit. - by rewrite -(Forall2_length _ _ _ HFA). by iApply ("Himpl" with "[] H"). - - rewrite /Î /=. iRevert "HÏ". generalize O; intros offs. - change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat). generalize O; intros i. - iInduction HFA as [|ty1 ty2 tyl1 tyl2 Hincl HFA] "IH" forall (i offs). - + iIntros "_!>!#*_/=". rewrite big_sepL_nil. eauto. - + iIntros "#HÏ". iMod ("IH" $! _ _ with "[]") as "#Hqimpl"; try done. - iMod (Hincl with "HÏ") as "[_ #Hhimpl]". iIntros "!>!#*". - rewrite !big_sepL_cons. iIntros "[Hh Hq]". - setoid_rewrite <-Nat.add_succ_comm. - iDestruct ("Hhimpl" $! _ _ _ with "Hh") as "[$ %]". - replace ty2.(ty_size) with ty1.(ty_size) by done. - iDestruct ("Hqimpl" $! _ _ _ with "Hq") as "[$ %]". - iIntros "!%/=". congruence. - Qed. - - Lemma ty_incl_prod_cons_l Ï ty tyl : - ty_incl Ï (Î (ty :: tyl)) (Î [ty ; Î tyl]). - Proof. - iIntros (tid) "_!>". iSplit; iIntros "!#/=". - - iIntros (vl) "H". iDestruct "H" as ([|vlh vllq]) "(%&%&H)". done. subst. - iExists [_;_]. iSplit. by rewrite /= app_nil_r. iSplit. done. - rewrite !big_sepL_cons big_sepL_nil right_id. iDestruct "H" as "[$ H]". - iExists _. repeat iSplit; try done. iPureIntro. simpl in *; congruence. - - iIntros (κ E l) "H". iSplit; last (iPureIntro; lia). - rewrite !big_sepL_cons big_sepL_nil right_id. iDestruct "H" as "[$ H]". - (* FIXME : namespaces do not match. *) - admit. - Admitted. - - (* TODO, depends on [ty_incl_prod_cons_l] *) + iIntros (tid) "_!>". iSplit; iIntros "!#/=*H". + - iDestruct "H" as (vl1 vl') "(% & H & Ho3)". + iDestruct "H" as (vl2 vl3) "(% & Ho1 & Ho2)". subst. + iExists _, _. iSplit. by rewrite -assoc. iFrame. iExists _, _. by iFrame. + - iDestruct "H" as (E1' E3) "(% & H & Hs3)". + iDestruct "H" as (E1 E2) "(% & Hs1 & Hs2)". rewrite shift_loc_assoc_nat. + iSplit; last by rewrite assoc. + iExists E1, (E2 ∪ E3). iSplit. by iPureIntro; set_solver. iFrame. + iExists E2, E3. iSplit. by iPureIntro; set_solver. by iFrame. + Qed. + Lemma ty_incl_prod_flatten Ï tyl1 tyl2 tyl3 : ty_incl Ï (Î (tyl1 ++ Î tyl2 :: tyl3)) (Î (tyl1 ++ tyl2 ++ tyl3)). - Admitted. + Proof. + apply (ty_incl_weaken _ ⊤). apply perm_incl_top. + induction tyl1; last by apply (ty_incl_prod2 _ _ _ _ _ _). + induction tyl2 as [|ty tyl2 IH]; simpl. + - iIntros (tid) "_". iSplitL; iIntros "/=!>!#*H". + + iDestruct "H" as (vl1 vl2) "(% & % & Ho)". subst. done. + + iDestruct "H" as (E1 E2) "(% & H1 & Ho)". iSplit; last done. + rewrite shift_loc_0. iApply (ty_shr_mono with "[] Ho"). set_solver. + iApply lft_incl_refl. + - etransitivity. apply ty_incl_prod2_assoc2. + eapply (ty_incl_prod2 _ _ _ _ _ _). done. apply IH. + Qed. + + Lemma ty_incl_prod_unflatten Ï tyl1 tyl2 tyl3 : + ty_incl Ï (Î (tyl1 ++ tyl2 ++ tyl3)) + (Î (tyl1 ++ Î tyl2 :: tyl3)). + Proof. + apply (ty_incl_weaken _ ⊤). apply perm_incl_top. + induction tyl1; last by apply (ty_incl_prod2 _ _ _ _ _ _). + induction tyl2 as [|ty tyl2 IH]; simpl. + - iIntros (tid) "_". + iMod (borrow_create with "[]") as "[Hbor _]". + done. instantiate (1:=True%I). by auto. instantiate (1:=static). + iMod (borrow_fracture (λ _, True%I) with "Hbor") as "#Hbor". done. + iSplitL; iIntros "/=!>!#*H". + + iExists [], vl. iFrame. auto. + + iSplit; last done. iExists ∅, E. iSplit. iPureIntro; set_solver. + rewrite shift_loc_0. iFrame. iExists []. iSplit; last auto. + setoid_rewrite heap_mapsto_vec_nil. + iApply (frac_borrow_shorten with "[] Hbor"). iApply lft_incl_static. + - etransitivity; last apply ty_incl_prod2_assoc1. + eapply (ty_incl_prod2 _ _ _ _ _ _). done. apply IH. + Qed. Lemma ty_incl_sum Ï n tyl1 tyl2 (_ : LstTySize n tyl1) (_ : LstTySize n tyl2) : Duplicable Ï â†’ Forall2 (ty_incl Ï) tyl1 tyl2 → diff --git a/theories/typing.v b/theories/typing.v index a334f3ad..f797361a 100644 --- a/theories/typing.v +++ b/theories/typing.v @@ -150,17 +150,14 @@ Section typing. 0 < n → typed_step_ty Ï (Alloc #n) (own 1 (Î (replicate n uninit))). Proof. iIntros (Hn tid) "!#(#HEAP&_&$)". wp_alloc l vl as "H↦" "H†". iIntros "!>". - iExists _. iSplit. done. iNext. rewrite Nat2Z.id. iSplitL "H†". - - assert (ty_size (Î (replicate n uninit)) = n) as ->; last done. - clear. simpl. induction n. done. rewrite /= IHn //. + iExists _. iSplit. done. iNext. rewrite Nat2Z.id. iSplitR "H†". - iExists vl. iFrame. match goal with H : Z.of_nat n = Z.of_nat (length vl) |- _ => rename H into Hlen end. clear Hn. apply (inj Z.of_nat) in Hlen. subst. - iInduction vl as [|v vl] "IH". - + iExists []. rewrite big_sepL_nil. auto. - + iDestruct "IH" as (vll) "(% & % & ?)". subst. iExists ([_]::_). iSplit. done. - iSplit. iIntros "/=!%"; congruence. - rewrite /= big_sepL_cons. by iSplit. + iInduction vl as [|v vl] "IH". done. + iExists [v], vl. iSplit. done. by iSplit. + - assert (ty_size (Î (replicate n uninit)) = n) as ->; last done. + clear. simpl. induction n. done. rewrite /= IHn //. Qed. Lemma typed_free ty (ν : expr): @@ -169,7 +166,7 @@ Section typing. iIntros (tid) "!#(#HEAP&Hâ—&$)". wp_bind ν. iApply (has_type_wp with "[$Hâ—]"). iIntros (v) "[_ Hâ—]!>". rewrite has_type_value. - iDestruct "Hâ—" as (l) "(Hv & >H†& H↦∗:)". iDestruct "Hv" as %[=->]. + iDestruct "Hâ—" as (l) "(Hv & H↦∗: & >H†)". iDestruct "Hv" as %[=->]. iDestruct "H↦∗:" as (vl) "[>H↦ Hown]". rewrite ty_size_eq. iDestruct "Hown" as ">%". wp_free; eauto. Qed. @@ -188,7 +185,7 @@ Section typing. Proof. iIntros (? ν tid Φ E ?) "(Hâ— & Htl & HΦ)". iApply (has_type_wp with "[- $Hâ—]"). iIntros (v) "[Hνv Hâ—]". iDestruct "Hνv" as %Hνv. - rewrite has_type_value. iDestruct "Hâ—" as (l) "[Heq [>H†H↦]]". + rewrite has_type_value. iDestruct "Hâ—" as (l) "(Heq & H↦ & >H†)". iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ #Hown]". iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">%". by rewrite ty.(ty_size_eq). @@ -202,21 +199,17 @@ Section typing. Proof. iIntros (ν tid Φ E ?) "(Hâ— & Htl & HΦ)". iApply (has_type_wp with "[- $Hâ—]"). iIntros (v) "[Hνv Hâ—]". iDestruct "Hνv" as %Hνv. - rewrite has_type_value. iDestruct "Hâ—" as (l) "(Heq & >H†& H↦)". + rewrite has_type_value. iDestruct "Hâ—" as (l) "(Heq & H↦ & >H†)". iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ Hown]". iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">Hlen". by rewrite ty.(ty_size_eq). iDestruct "Hlen" as %Hlen. iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦!>". - rewrite /has_type Hνv. iExists _. iSplit. done. iSplitL "H†". + rewrite /has_type Hνv. iExists _. iSplit. done. iSplitR "H†". + - rewrite -Hlen. iExists vl. iIntros "{$H↦}!>". clear. + iInduction vl as [|v vl] "IH". done. + iExists [v], vl. iSplit. done. by iSplit. - assert (ty_size (Î (replicate (ty_size ty) uninit)) = ty_size ty) as ->; last by auto. clear. induction ty.(ty_size). done. simpl in *. congruence. - - rewrite -Hlen. iExists vl. iIntros "{$H↦}!>". clear. - iInduction vl as [|v vl] "IH". - + iExists []. rewrite big_sepL_nil. auto. - + iDestruct "IH" as (vll) "(% & % & IH)". iExists ([v]::vll). iSplit; last iSplit. - * iIntros "!%/=". congruence. - * iIntros "!%/=". congruence. - * rewrite big_sepL_cons. iFrame "#". done. Qed. Lemma consumes_copy_uniq_borrow ty κ κ' q: @@ -262,8 +255,8 @@ Section typing. typed_step (Ï1 ν) (!ν) (λ v, v â— ty ∗ Ï2 ν)%P. Proof. iIntros (Hsz Hconsumes tid) "!#[#HEAP[??]]". wp_bind ν. - iApply Hconsumes. done. iFrame. iIntros (l vl q) "(%&%&H↦&Hupd)". - iMod "Hupd". rewrite ->Hsz in *. destruct vl as [|v [|]]; try done. + iApply Hconsumes. done. iFrame. iIntros (l vl q) "(%&%&H↦&>Hupd)". + rewrite ->Hsz in *. destruct vl as [|v [|]]; try done. rewrite heap_mapsto_vec_singleton. wp_read. rewrite /sep has_type_value. iMod "Hupd" as "[$ Hclose]". by iApply "Hclose". Qed. @@ -278,9 +271,9 @@ Section typing. rewrite has_type_value. iDestruct "Hâ—" as (l) "[Heq H↦]". iDestruct "Heq" as %[=->]. iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[Htok Hclose]". done. iMod (borrow_acc_strong with "H↦ Htok") as "[H↦ Hclose']". done. - iDestruct "H↦" as (vl) "[>H↦ Hown]". iDestruct "Hown" as (l') "(>% & H†& Hown)". + iDestruct "H↦" as (vl) "[>H↦ Hown]". iDestruct "Hown" as (l') "(>% & Hown & H†)". subst. rewrite heap_mapsto_vec_singleton. wp_read. - iMod ("Hclose'" with "*[H↦ H†Hown]") as "[Hbor Htok]"; last first. + iMod ("Hclose'" with "*[H↦ Hown H†]") as "[Hbor Htok]"; last first. - iMod (borrow_split with "Hbor") as "[_ Hbor]". done. iMod (borrow_split with "Hbor") as "[_ Hbor]". done. iMod ("Hclose" with "Htok") as "$". iFrame "#". iExists _. eauto. @@ -360,7 +353,7 @@ Section typing. iMod ("Hclose''" with "Htok") as "Htok". iMod ("Hclose'" with "[$H↦]") as "Htok'". iMod ("Hclose" with "[$Htok $Htok']") as "$". iFrame "#". iExists _. - iSplitL. done. iApply (ty_shr_mono with "H⊑3 Hshr"). + iSplitL. done. by iApply (ty_shr_mono with "H⊑3 Hshr"). Qed. Definition update (ty : type) (Ï1 Ï2 : expr → perm) : Prop := @@ -378,7 +371,7 @@ Section typing. Proof. iIntros (Hsz ν tid Φ E ?) "[Hâ— HΦ]". iApply (has_type_wp with "[- $Hâ—]"). iIntros (v) "[Hνv Hâ—]". iDestruct "Hνv" as %Hνv. - rewrite has_type_value. iDestruct "Hâ—" as (l) "(Heq & >H†& H↦)". + rewrite has_type_value. iDestruct "Hâ—" as (l) "(Heq & H↦ & >H†)". iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]". rewrite ty2.(ty_size_eq) -Hsz. iDestruct "Hown" as ">%". iApply "HΦ". iFrame "∗%". iIntros (vl') "[H↦ Hown']!>". rewrite /has_type Hνv. -- GitLab