From 3f715e03e3c3791af7d4e595d946b84d825d94f4 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 16 Sep 2016 17:09:55 +0200
Subject: [PATCH] Borrowing judgement.
---
perm_incl.v | 95 ++++++++++++++++++++++++++++++++++++++++++++++++++++-
1 file changed, 94 insertions(+), 1 deletion(-)
diff --git a/perm_incl.v b/perm_incl.v
index 41855a1d..01824cbd 100644
--- a/perm_incl.v
+++ b/perm_incl.v
@@ -16,6 +16,9 @@ Section defs.
Global Instance perm_equiv : Equiv perm :=
λ ρ1 ρ2, perm_incl ρ1 ρ2 ∧ perm_incl ρ2 ρ1.
+ Definition borrowing κ (ρ ρ1 ρ2 : perm) :=
+ ∀ tid, lft κ ⊢ ρ tid -★ ρ1 tid ={⊤}=★ ρ2 tid ★ κ ∋ ρ1 tid.
+
End defs.
Infix "⇒" := perm_incl (at level 95, no associativity) : C_scope.
@@ -153,7 +156,7 @@ Section props.
{ destruct ql as [|q0 ql]; last done. destruct q. simpl in *. by subst. }
destruct v as [[[|l|]|]|];
try by (destruct tyl as [|ty0 tyl], ql as [|q0 ql]; try done;
- by split; iIntros (tid) "H";
+ by split; iIntros (tid) "H"; try done;
[iDestruct "H" as (l) "[% _]" || iDestruct "H" as "[]" |
iDestruct "H" as "[[]_]"]).
destruct (@exists_last _ ql) as (ql'&q0&->). done.
@@ -176,4 +179,94 @@ Section props.
by iSplit; iIntros "[$[$[$[$$]]]]".
Qed.
+ Lemma perm_split_uniq_borrow_prod tyl κ v :
+ v ◁ &uniq{κ} (product tyl) ⇒
+ foldr (λ tyoffs acc,
+ proj_valuable (Z.of_nat (tyoffs.2)) v ◁ &uniq{κ} (tyoffs.1) ★ acc)%P
+ ⊤ (combine_offs tyl 0).
+ Proof.
+ intros tid.
+ destruct v as [[[|l|]|]|];
+ iIntros "H"; try iDestruct "H" as "[]";
+ iDestruct "H" as (l0) "[EQ H]"; iDestruct "EQ" as %[=]. subst l0.
+ rewrite split_prod_mt. iRevert "H".
+ induction (combine_offs tyl 0) as [|[ty offs] ll IH]. by auto.
+ iIntros "H". rewrite big_sepL_cons /=.
+ iVs (lft_borrow_split with "H") as "[H0 H]". set_solver.
+ iVs (IH with "[] H") as "$". done.
+ iVsIntro. iExists _. eauto.
+ Qed.
+
+ Lemma perm_split_shr_borrow_prod tyl κ v :
+ v ◁ &shr{κ} (product tyl) ⇒
+ foldr (λ tyoffs acc,
+ proj_valuable (Z.of_nat (tyoffs.2)) v ◁ &shr{κ} (tyoffs.1) ★ acc)%P
+ ⊤ (combine_offs tyl 0).
+ Proof.
+ intros tid.
+ destruct v as [[[|l|]|]|];
+ iIntros "H"; try iDestruct "H" as "[]";
+ iDestruct "H" as (l0) "[EQ H]"; iDestruct "EQ" as %[=]. subst l0.
+ simpl. iVsIntro. iRevert "H".
+ change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat). generalize O at 2.
+ induction (combine_offs tyl 0) as [|[ty offs] ll IH]. by auto.
+ iIntros (i) "H". rewrite big_sepL_cons /=. iDestruct "H" as "[H0 H]".
+ setoid_rewrite <-Nat.add_succ_comm. iDestruct (IH with "[] H") as "$". done.
+ iExists _. iSplit. done. admit.
+ (* FIXME : namespaces problem. *)
+ Admitted.
+
+ Lemma borrowing_perm_incl κ ρ ρ1 ρ2 θ :
+ borrowing κ ρ ρ1 ρ2 → ρ ★ κ ∋ θ ★ ρ1 ⇒ ρ2 ★ κ ∋ (θ ★ ρ1).
+ Proof.
+ iIntros (Hbor tid) "(Hρ&Hθ&Hρ1)".
+ iVs (Hbor with "[#] Hρ Hρ1") as "[$ ?]". by iApply lft_extract_lft.
+ iApply lft_extract_combine. set_solver. by iFrame.
+ Qed.
+
+ Lemma own_uniq_borrowing v q ty κ :
+ borrowing κ ⊤ (v ◁ own q ty) (v ◁ &uniq{κ} ty).
+ Proof.
+ iIntros (tid) "#Hκ _ Hown".
+ destruct v as [[[|l|]|]|];
+ try by (iDestruct "Hown" as "[]" || iDestruct "Hown" as (l) "[% _]").
+ iDestruct "Hown" as (l') "[EQ [Hf Hown]]". iDestruct "EQ" as %[=]. subst l'.
+ iVs (lft_borrow_create with "Hκ Hown") as "[Hbor Hextract]". done.
+ iSplitL "Hbor". by simpl; eauto.
+ assert ((Some #l ◁ own q ty)%P tid ⊣⊢
+ ▷ †{q}l…ty_size ty ★ ▷ l ↦★: ty_own ty tid) as ->.
+ { iSplit; iIntros "H/=".
+ - iDestruct "H" as (l') "[EQ [Hf Hown]]". iDestruct "EQ" as %[=]. subst l'.
+ by iFrame.
+ - iExists _. eauto. }
+ iVs (lft_borrow_create with "Hκ Hf") as "[_ Hf]". done.
+ iVs (lft_extract_combine with "[-]"). done. by iFrame.
+ (* FIXME : extraction needs to be monotone in some sense to
+ remove the later. *)
+ admit.
+ Admitted.
+
+ Lemma reborrow_uniq_borrowing κ κ' v ty :
+ borrowing κ (κ ⊑ κ') (v ◁ &uniq{κ'}ty) (v ◁ &uniq{κ}ty).
+ Proof.
+ iIntros (tid) "_ #Hord H".
+ destruct v as [[[|l|]|]|];
+ try by (iDestruct "H" as "[]" || iDestruct "H" as (l) "[% _]").
+ iDestruct "H" as (l') "[EQ H]". iDestruct "EQ" as %[=]. subst l'.
+ iVs (lft_reborrow with "Hord H") as "[H Hextr]". done.
+ iVsIntro. iSplitL "H". iExists _. by eauto.
+ iApply (lft_extract_proper with "Hextr").
+ iSplit; iIntros "H/=".
+ - iDestruct "H" as (l') "[EQ H]". iDestruct "EQ" as %[=]. by subst l'.
+ - iExists _. eauto.
+ Qed.
+
+ Lemma lftincl_borrowing κ κ' q : borrowing κ ⊤ [κ']{q} (κ ⊑ κ').
+ Proof.
+ iIntros (tid) "#Hκ #Hord [Htok #Hκ']".
+ iVs (lft_mkincl' with "[#] Htok") as "[$ H]". done. by iFrame "#".
+ iVs (lft_borrow_create with "Hκ []") as "[_ H']". done. by iNext; iApply "Hκ'".
+ iApply lft_extract_combine. done. by iFrame.
+ Qed.
+
End props.
--
GitLab