From 78bf23944859007862e3a2d06cfe8e33ed331b3b Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 9 Dec 2016 13:56:39 +0100
Subject: [PATCH] Define subtyping, and prove subtyping for some types.
TODO : functions, sums. But these types need to be redefined properly.
---
theories/lifetime/derived.v | 12 ++++
theories/typing/bool.v | 2 +-
theories/typing/int.v | 2 +-
theories/typing/lft_contexts.v | 4 +-
theories/typing/own.v | 33 +++++----
theories/typing/product.v | 102 ++++++++++++++-------------
theories/typing/product_split.v | 15 ++--
theories/typing/shr_bor.v | 41 +++++++----
theories/typing/type.v | 51 ++++++++++++--
theories/typing/typing.v | 3 +-
theories/typing/uniq_bor.v | 121 +++++++++++++++++++++-----------
11 files changed, 254 insertions(+), 132 deletions(-)
diff --git a/theories/lifetime/derived.v b/theories/lifetime/derived.v
index b524fcae..9d933ae4 100644
--- a/theories/lifetime/derived.v
+++ b/theories/lifetime/derived.v
@@ -47,6 +47,17 @@ Proof.
iModIntro. iNext. iApply ("Hclose" with "* HP []"). by iIntros "!> $".
Qed.
+Lemma bor_iff (P Q : iProp Σ) E κ :
+ ↑lftN ⊆ E →
+ lft_ctx -∗ ▷ □ (P ↔ Q) -∗ &{κ}P ={E}=∗ &{κ}Q.
+Proof.
+ iIntros (?) "#LFT #Heq Hb".
+ iMod (bor_acc_atomic_cons with "LFT Hb") as "[[HP Hclose]|[H†Hclose]]". done.
+ - iApply ("Hclose" with "[HP] []").
+ by iApply "Heq". by iIntros "!>HQ!>"; iApply "Heq".
+ - iMod "Hclose". by iApply (bor_fake with "LFT").
+Qed.
+
Lemma bor_persistent P `{!PersistentP P} E κ q :
↑lftN ⊆ E →
lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
@@ -56,6 +67,7 @@ Proof.
by iMod ("Hob" with "HP") as "[_ $]".
Qed.
+
Lemma lft_incl_static κ : (κ ⊑ static)%I.
Proof.
iIntros "!#". iSplitR.
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 639dab97..41440f80 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -1,6 +1,6 @@
From iris.proofmode Require Import tactics.
From lrust.typing Require Export type.
-From lrust.typing Require Import typing.
+From lrust.typing Require Import typing perm.
Section bool.
Context `{iris_typeG Σ}.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 73724f21..7c4f8c06 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -1,6 +1,6 @@
From iris.proofmode Require Import tactics.
From lrust.typing Require Export type.
-From lrust.typing Require Import typing bool.
+From lrust.typing Require Import typing bool perm.
Section int.
Context `{iris_typeG Σ}.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 961cde5f..88eb4bb8 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -4,7 +4,6 @@ From iris.base_logic.lib Require Import fractional.
From lrust.lifetime Require Export derived.
Section lft_contexts.
-
Context `{invG Σ, lftG Σ}.
Implicit Type (κ : lft).
@@ -77,6 +76,9 @@ Section lft_contexts.
(* Lifetime inclusion *)
+ (* There does not seem to be a need in the type system for
+ "equivalence" of lifetimes. If so, TODO : add it, and the
+ corresponding [Proper] instances for the relevent types. *)
Definition incl κ κ' : Prop :=
∀ qE qL, lectx_interp E qE -∗ llctx_interp L qL -∗ κ ⊑ κ'.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 5ac4a286..20c0cdf7 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -2,8 +2,9 @@ From Coq Require Import Qcanon.
From iris.proofmode Require Import tactics.
From lrust.lifetime Require Import borrow frac_borrow.
From lrust.lang Require Export new_delete.
+From lrust.lang Require Import heap.
From lrust.typing Require Export type.
-From lrust.typing Require Import type_incl typing product.
+From lrust.typing Require Import typing product perm.
Section own.
Context `{iris_typeG Σ}.
@@ -49,7 +50,7 @@ Section own.
ty_own tid vl :=
(* 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 [ty_incl_own].
+ prevent us to prove [subtype_own].
Since this assertion is timeless, this should not cause
problems. *)
@@ -98,23 +99,31 @@ Section own.
by iApply (ty.(ty_shr_mono) with "LFT Hκ").
Qed.
- Lemma ty_incl_own n ty1 ty2 Ï :
- ty_incl Ï ty1 ty2 → ty_incl Ï (own n ty1) (own n ty2).
+ Global Instance own_mono E L n :
+ Proper (subtype E L ==> subtype E L) (own n).
Proof.
- iIntros (Hincl tid) "#LFT H/=". iMod (Hincl with "LFT H") as "[#Howni #Hshri]".
- iModIntro. iSplit; iIntros "!#*H".
- - iDestruct "H" as (l) "(%&Hmt&H†)". subst. iExists _. iSplit. done.
- iDestruct "Hmt" as (vl') "[Hmt Hown]". iNext.
+ intros ty1 ty2 Hincl. split.
+ - done.
+ - iIntros (qE qL) "#LFT HE HL *".
+ iDestruct (Hincl.(subtype_own _ _ _ _) with "LFT HE HL") as "#Howni".
+ iIntros "{HE HL} !# * H". 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".
+ iDestruct ("Howni" with "* Hown") as "Hown".
iDestruct (ty_size_eq with "Hown") as %<-. iFrame.
iExists _. by iFrame.
- - iDestruct "H" as (l') "[Hfb #Hvs]". iSplit; last done. iExists l'. iFrame.
- iIntros "!#". iIntros (q' F) "% Hκ".
+ - iIntros (qE qL) "#LFT HE HL *".
+ iDestruct (Hincl.(subtype_shr _ _ _ _) with "LFT HE HL") as "#Hshri".
+ iIntros "{HE HL} !# * H". iDestruct "H" as (l') "[Hfb #Hvs]".
+ iExists l'. iFrame. iIntros "!#". iIntros (q' F') "% Hκ".
iMod ("Hvs" with "* [%] Hκ") as "Hvs'". done. iModIntro. iNext.
- iMod "Hvs'" as "[Hshr $]". by iDestruct ("Hshri" with "* Hshr") as "[$ _]".
+ iMod "Hvs'" as "[Hshr $]". iApply ("Hshri" with "* Hshr").
Qed.
+ Global Instance own_proper E L n :
+ Proper (eqtype E L ==> eqtype E L) (own n).
+ Proof. intros ?? Heq. split; f_equiv; apply Heq. Qed.
+
Lemma typed_new Ï (n : nat):
0 ≤ n → typed_step_ty Ï (new [ #n]%E) (own n (Î (replicate n uninit))).
Proof.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 5cd811ce..e9aae329 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -55,6 +55,27 @@ Section product.
iSplitL "H1"; by iApply (ty_shr_mono with "LFT H⊑").
Qed.
+ Global Instance product2_mono E L:
+ Proper (subtype E L ==> subtype E L ==> subtype E L) product2.
+ Proof.
+ iIntros (ty11 ty12 H1 ty21 ty22 H2). split.
+ - by rewrite /= (subtype_sz _ _ _ _ H1) (subtype_sz _ _ _ _ H2).
+ - iIntros (??) "#LFT HE HL".
+ iDestruct (subtype_own _ _ _ _ H1 with "LFT HE HL") as "#H1".
+ iDestruct (subtype_own _ _ _ _ H2 with "LFT HE HL") as "#H2".
+ iIntros "{HE HL}!# * H". iDestruct "H" as (vl1 vl2) "(% & Hown1 & Hown2)".
+ iExists _, _. iSplit. done. by iSplitL "Hown1"; [iApply "H1"|iApply "H2"].
+ - iIntros (??) "#LFT HE HL".
+ iDestruct (subtype_shr _ _ _ _ H1 with "LFT HE HL") as "#H1".
+ iDestruct (subtype_shr _ _ _ _ H2 with "LFT HE HL") as "#H2".
+ iIntros "{HE HL}!# * H". iDestruct "H" as (vl1 vl2) "(% & #Hshr1 & #Hshr2)".
+ iExists _, _. iSplit. done. erewrite subtype_sz; last done.
+ by iSplit; [iApply "H1"|iApply "H2"].
+ Qed.
+ Global Instance product2_proper E L:
+ Proper (eqtype E L ==> eqtype E L ==> eqtype E L) product2.
+ Proof. by intros ??[]??[]; split; apply product2_mono. Qed.
+
Global Program Instance product2_copy `(!Copy ty1) `(!Copy ty2) :
Copy (product2 ty1 ty2).
Next Obligation.
@@ -91,6 +112,10 @@ Section product.
Qed.
Definition product := fold_right product2 unit.
+
+ (* Given that in practice, product will be used with concrete lists,
+ there should be no need to declare [Copy] and [Proper] instances
+ for [product]. *)
End product.
Arguments product : simpl never.
@@ -99,28 +124,7 @@ Notation Î := product.
Section typing.
Context `{iris_typeG Σ}.
- (* 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) "#LFT #HÏ".
- iMod (Hincl1 with "LFT HÏ") as "[#Ho1#Hs1]".
- iMod (Hincl2 with "LFT 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.
+ (* FIXME : do we still need this (flattening and unflattening)? *)
Lemma ty_incl_prod2_assoc1 Ï ty1 ty2 ty3 :
ty_incl Ï (product2 ty1 (product2 ty2 ty3)) (product2 (product2 ty1 ty2) ty3).
@@ -154,35 +158,37 @@ Section typing.
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) "#LFT _". 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 "LFT [] Ho"). set_solver.
- iApply lft_incl_refl.
- - etransitivity. apply ty_incl_prod2_assoc2.
- eapply (ty_incl_prod2 _ _ _ _ _ _). done. apply IH.
- Qed.
+ Admitted.
+ (* 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) "#LFT _". 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 "LFT [] 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) "#LFT _". iMod (bor_create with "LFT []") as "[Hbor _]".
- done. instantiate (1:=True%I). by auto. instantiate (1:=static).
- iMod (bor_fracture (λ _, True%I) with "LFT 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_bor_shorten with "[] Hbor"). iApply lft_incl_static.
- - etransitivity; last apply ty_incl_prod2_assoc1.
- eapply (ty_incl_prod2 _ _ _ _ _ _). done. apply IH.
- Qed.
+ Admitted.
+ (* 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) "#LFT _". iMod (bor_create with "LFT []") as "[Hbor _]". *)
+ (* done. instantiate (1:=True%I). by auto. instantiate (1:=static). *)
+ (* iMod (bor_fracture (λ _, True%I) with "LFT 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_bor_shorten with "[] Hbor"). iApply lft_incl_static. *)
+ (* - etransitivity; last apply ty_incl_prod2_assoc1. *)
+ (* eapply (ty_incl_prod2 _ _ _ _ _ _). done. apply IH. *)
+ (* Qed. *)
End typing.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 63039819..826b7249 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -76,9 +76,10 @@ Section product_split.
rewrite /has_type /sep /product2 /=.
destruct (eval_expr ν) as [[[|l|]|]|];
iIntros (tid) "#LFT H"; try iDestruct "H" as "[]";
- iDestruct "H" as (l0) "[EQ H]"; iDestruct "EQ" as %[=<-].
- rewrite /= split_prod_mt. iMod (bor_sep with "LFT H") as "[H1 H2]".
- set_solver. iSplitL "H1"; eauto.
+ iDestruct "H" as (l0 P) "[[EQ #HPiff] HP]"; iDestruct "EQ" as %[=<-].
+ 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. iSplitL "H1"; iExists _, _; erewrite <-uPred.iff_refl; auto.
Qed.
Lemma perm_split_uniq_bor_prod tyl κ ν :
@@ -88,10 +89,10 @@ Section product_split.
⊤ (combine_offs tyl 0).
Proof.
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. }
+ { iIntros (tid) "LFT H/=". rewrite /has_type /=. destruct (eval_expr ν)=>//.
+ iDestruct "H" as (l P) "[[Heq #HPiff] HP]". iDestruct "Heq" as %[=->].
+ iMod (bor_iff with "LFT [] HP") as "H". set_solver. by eauto.
+ iExists _, _; erewrite <-uPred.iff_refl, shift_loc_0; auto. }
generalize 0%nat. induction tyl as [|ty tyl IH]=>offs. by iIntros (tid) "_ H/=".
etransitivity. apply perm_split_uniq_bor_prod2.
iIntros (tid) "#LFT /=[$ H]". iApply (IH with "LFT").
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 2de7fbda..7a06f36d 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -1,7 +1,7 @@
From iris.proofmode Require Import tactics.
From lrust.lifetime Require Import frac_borrow.
From lrust.typing Require Export type.
-From lrust.typing Require Import perm type_incl typing own uniq_bor.
+From lrust.typing Require Import perm lft_contexts typing own uniq_bor.
Section shr_bor.
Context `{iris_typeG Σ}.
@@ -14,6 +14,28 @@ Section shr_bor.
iIntros (κ ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
Qed.
+ Global Instance subtype_shr_mono E L :
+ Proper (flip (incl E L) ==> subtype E L ==> subtype E L) shr_bor.
+ Proof.
+ intros κ1 κ2 Hκ ty1 ty2 Hty. split.
+ - done.
+ - iIntros (qE qL) "#LFT HE HL *". iDestruct (Hκ with "HE HL") as "#Hκ".
+ iDestruct (subtype_shr _ _ _ _ Hty with "LFT HE HL") as "#Hty".
+ iIntros "{HE HL}!#*H". iDestruct "H" as (l) "(% & H)". subst. iExists _.
+ iSplit. done. by iApply (ty2.(ty_shr_mono) with "LFT Hκ"); last iApply "Hty".
+ - iIntros (qE qL) "#LFT HE HL *". iDestruct (Hκ with "HE HL") as "#Hκ".
+ iDestruct (subtype_shr _ _ _ _ Hty with "LFT HE HL") as "#Hst".
+ iIntros "{HE HL}!#*H". iDestruct "H" as (vl) "#[Hfrac Hty]".
+ iExists vl. iFrame "#". iNext.
+ iDestruct "Hty" as (l0) "(% & Hty)". subst. iExists _. iSplit. done.
+ by iApply (ty_shr_mono with "LFT Hκ"); last iApply "Hst".
+ Qed.
+ Global Instance subtype_shr_mono' E L :
+ Proper (incl E L ==> flip (subtype E L) ==> flip (subtype E L)) shr_bor.
+ Proof. intros ??????. by apply subtype_shr_mono. Qed.
+ Global Instance subtype_shr_proper E L κ :
+ Proper (eqtype E L ==> eqtype E L) (shr_bor κ).
+ Proof. intros ??[]. by split; apply subtype_shr_mono. Qed.
End shr_bor.
Notation "&shr{ κ } ty" := (shr_bor κ ty)
@@ -27,8 +49,9 @@ Section typing.
Proof.
iIntros (tid) "#LFT [Huniq [Htok $]]". unfold has_type.
destruct (eval_expr ν); last by iDestruct "Huniq" as "[]".
- iDestruct "Huniq" as (l) "[% Hown]".
- iMod (ty.(ty_share) _ lrustN with "LFT Hown Htok") as "[Hown $]"; [solve_ndisj|done|].
+ iDestruct "Huniq" as (l P) "[[% #HPiff] HP]".
+ iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
+ iMod (ty.(ty_share) _ lrustN with "LFT H↦ Htok") as "[Hown $]"; [solve_ndisj|done|].
iIntros "!>/=". eauto.
Qed.
@@ -42,18 +65,6 @@ Section typing.
iModIntro. iExists _. iSplit. done. by iApply (ty_shr_mono with "LFT Hord Hκ'").
Qed.
- Lemma lft_incl_ty_incl_shr_bor ty κ1 κ2 :
- ty_incl (κ1 ⊑ κ2) (&shr{κ2}ty) (&shr{κ1}ty).
- Proof.
- iIntros (tid) "#LFT #Hincl!>". iSplit; iIntros "!#*H".
- - iDestruct "H" as (l) "(% & H)". subst. iExists _.
- iSplit. done. by iApply (ty.(ty_shr_mono) with "LFT Hincl").
- - iDestruct "H" as (vl) "#[Hfrac Hty]". iSplit; last done.
- iExists vl. iFrame "#". iNext.
- iDestruct "Hty" as (l0) "(% & Hty)". subst. iExists _. iSplit. done.
- by iApply (ty_shr_mono with "LFT Hincl Hty").
- Qed.
-
Lemma consumes_copy_shr_bor ty κ κ' q:
Copy ty →
consumes ty (λ ν, ν ◠&shr{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 873d2628..d40dc121 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -1,6 +1,7 @@
From iris.base_logic.lib Require Export na_invariants.
From lrust.lang Require Import heap.
From lrust.lifetime Require Import borrow frac_borrow reborrow.
+From lrust.typing Require Import lft_contexts.
Class iris_typeG Σ := Iris_typeG {
type_heapG :> heapG Σ;
@@ -15,10 +16,12 @@ Definition lrustN := nroot .@ "lrust".
Section type.
Context `{iris_typeG Σ}.
+ Definition thread_id := na_inv_pool_name.
+
Record type :=
{ ty_size : nat;
- ty_own : na_inv_pool_name → list val → iProp Σ;
- ty_shr : lft → na_inv_pool_name → coPset → loc → iProp Σ;
+ ty_own : thread_id → list val → iProp Σ;
+ ty_shr : lft → thread_id → coPset → loc → iProp Σ;
ty_shr_persistent κ tid E l : PersistentP (ty_shr κ tid E l);
@@ -54,7 +57,7 @@ Section type.
bellow will not be acceptable by Coq. *)
Record simple_type `{iris_typeG Σ} :=
{ st_size : nat;
- st_own : na_inv_pool_name → list val → iProp Σ;
+ st_own : thread_id → list val → iProp Σ;
st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = st_sizeâŒ;
st_own_persistent tid vl : PersistentP (st_own tid vl) }.
@@ -66,7 +69,7 @@ Section type.
(* [st.(st_own) tid vl] needs to be outside of the fractured
borrow, otherwise I do not know how to prove the shr part of
- [lft_incl_ty_incl_shr_borrow]. *)
+ [subtype_shr_mono]. *)
ty_shr := λ κ tid _ l,
(∃ vl, (&frac{κ} λ q, l ↦∗{q} vl) ∗ ▷ st.(st_own) tid vl)%I
|}.
@@ -106,3 +109,43 @@ Coercion ty_of_st : simple_type >-> type.
Delimit Scope lrust_type_scope with T.
Bind Scope lrust_type_scope with type.
+
+Section subtyping.
+ Context `{iris_typeG Σ} (E : lectx) (L : llctx).
+
+ Record subtype (ty1 ty2 : type) : Prop :=
+ { subtype_sz : ty1.(ty_size) = ty2.(ty_size);
+ subtype_own qE qL :
+ lft_ctx -∗ lectx_interp E qE -∗ llctx_interp L qL -∗
+ □ ∀ tid vl, ty1.(ty_own) tid vl → ty2.(ty_own) tid vl;
+ subtype_shr qE qL :
+ lft_ctx -∗ lectx_interp E qE -∗ llctx_interp L qL -∗
+ □ ∀ κ tid F l, ty1.(ty_shr) κ tid F l → ty2.(ty_shr) κ tid F l }.
+
+ Global Instance subtype_preorder : PreOrder subtype.
+ Proof.
+ split.
+ - intros ty. split; [done| |]; iIntros (? ?) "_ _ _ !# * $".
+ - intros ty1 ty2 ty3 H1 H2. split.
+ + etrans. eapply H1. eapply H2.
+ + iIntros (? ?) "#LFT HE HL".
+ iDestruct (subtype_own _ _ H1 with "LFT HE HL") as "#H1".
+ iDestruct (subtype_own _ _ H2 with "LFT HE HL") as "#H2".
+ iIntros "{HE HL} !# * ?". iApply "H2". by iApply "H1".
+ + iIntros (? ?) "#LFT HE HL".
+ iDestruct (subtype_shr _ _ H1 with "LFT HE HL") as "#H1".
+ iDestruct (subtype_shr _ _ H2 with "LFT HE HL") as "#H2".
+ iIntros "{HE HL} !# * ?". iApply "H2". by iApply "H1".
+ Qed.
+
+ Definition eqtype (ty1 ty2 : type) : Prop :=
+ subtype ty1 ty2 ∧ subtype ty2 ty1.
+
+ Global Instance subtype_equivalence : Equivalence eqtype.
+ Proof.
+ split.
+ - split; done.
+ - intros ?? Heq; split; apply Heq.
+ - intros ??? H1 H2. split; etrans; (apply H1 || apply H2).
+ Qed.
+End subtyping.
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index 03a84abe..6d5fdc3e 100644
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -1,7 +1,8 @@
From iris.program_logic Require Import hoare.
From iris.base_logic Require Import big_op.
From lrust.lang Require Export notation memcpy.
-From lrust.typing Require Export type perm.
+From lrust.typing Require Export type.
+From lrust.typing Require Import perm.
From lrust.lang Require Import proofmode.
From lrust.lifetime Require Import frac_borrow reborrow borrow creation.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index a7238d10..ad6ca09c 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -1,30 +1,34 @@
From iris.proofmode Require Import tactics.
From lrust.lifetime Require Import borrow reborrow frac_borrow.
+From lrust.lang Require Import heap.
From lrust.typing Require Export type.
-From lrust.typing Require Import perm type_incl typing own.
+From lrust.typing Require Import perm lft_contexts typing own.
Section uniq_bor.
Context `{iris_typeG Σ}.
Program Definition uniq_bor (κ:lft) (ty:type) :=
{| ty_size := 1;
+ (* We quantify over [P]s so that the Proper lemma
+ (wrt. subtyping) works without an update. *)
ty_own tid vl :=
- (∃ l:loc, ⌜vl = [ #l ]⌠∗ &{κ} l ↦∗: ty.(ty_own) tid)%I;
+ (∃ (l:loc) P, (⌜vl = [ #l ]⌠∗ □ (P ↔ l ↦∗: ty.(ty_own) tid)) ∗ &{κ} P)%I;
ty_shr κ' tid E l :=
(∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
□ ∀ q' F, ⌜E ∪ mgmtE ⊆ F⌠→ q'.[κ∪κ']
={F, F∖E∖↑lftN}▷=∗ ty.(ty_shr) (κ∪κ') tid E l' ∗ q'.[κ∪κ'])%I
|}.
Next Obligation.
- iIntros (q ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
+ iIntros (q ty tid vl) "H". iDestruct "H" as (l P) "[[% _] _]". by subst.
Qed.
Next Obligation.
move=> κ ty E N κ' l tid q' ??/=. 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 with "LFT EQ Htok") as "[>% $]". set_solver. subst.
+ 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 with "LFT H Htok") as "[[>% #HPiff] $]". set_solver. subst.
rewrite heap_mapsto_vec_singleton.
iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "Hbf". set_solver.
rewrite {1}bor_unfold_idx. iDestruct "Hb2" as (i) "[#Hpb Hpbown]".
@@ -33,9 +37,10 @@ Section uniq_bor.
iExists l'. iIntros "!>{$Hbf}!#". iIntros (q'' F) "% Htok".
iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- - iMod (bor_unnest _ _ _ (l' ↦∗: ty_own ty tid)%I with "LFT [Hbtok]") as "Hb".
+ - iMod (bor_unnest _ _ _ P with "LFT [Hbtok]") as "Hb".
{ set_solver. } { iApply bor_unfold_idx. eauto. }
iModIntro. iNext. iMod "Hb".
+ iMod (bor_iff with "LFT [] Hb") as "Hb". set_solver. by eauto.
iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]"; try done. set_solver.
iApply "Hclose". eauto.
- iMod ("Hclose" with "[]") as "_". by eauto.
@@ -57,6 +62,41 @@ Section uniq_bor.
by iApply (ty_shr_mono with "LFT Hκ0").
Qed.
+ Global Instance subtype_uniq_mono E L :
+ Proper (flip (incl E L) ==> eqtype E L ==> subtype E L) uniq_bor.
+ Proof.
+ intros κ1 κ2 Hκ ty1 ty2 [Hty1 Hty2]. split.
+ - done.
+ - iIntros (qE qL) "#LFT HE HL *". iDestruct (Hκ with "HE HL") as "#Hκ".
+ iDestruct (subtype_own _ _ _ _ Hty1 with "LFT HE HL") as "#Hty1".
+ iDestruct (subtype_own _ _ _ _ Hty2 with "LFT HE HL") as "#Hty2".
+ iIntros "{HE HL} !# * H". iDestruct "H" as (l P) "[[% #HPiff] Hown]". subst.
+ iExists _, _. iSplitR; last by iApply (bor_shorten with "Hκ"). iSplit. done.
+ iIntros "!#". iSplit; iIntros "H".
+ + iDestruct ("HPiff" with "H") as (vl) "[??]". iExists vl. iFrame.
+ by iApply "Hty1".
+ + iDestruct "H" as (vl) "[??]". iApply "HPiff". iExists vl. iFrame.
+ by iApply "Hty2".
+ - iIntros (qE qL) "#LFT HE HL *". iDestruct (Hκ with "HE HL") as "#Hκ".
+ iDestruct (subtype_shr _ _ _ _ Hty1 with "LFT HE HL") as "#Hty".
+ iIntros "{HE HL} !# * H". iAssert (κ2 ∪ κ ⊑ κ1 ∪ κ)%I as "#Hincl'".
+ { iApply (lft_incl_glb with "[] []").
+ - iApply (lft_incl_trans with "[] Hκ"). iApply lft_le_incl.
+ apply gmultiset_union_subseteq_l.
+ - iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
+ iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'. iIntros "{$Hbor}!#".
+ iIntros (q' F') "% Htok".
+ iMod (lft_incl_acc with "Hincl' Htok") as (q'') "[Htok Hclose]". set_solver.
+ iMod ("Hupd" with "* [%] Htok") as "Hupd'"; try done. iModIntro. iNext.
+ iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
+ iApply (ty_shr_mono with "LFT Hincl'"); last by iApply "Hty". done.
+ Qed.
+ Global Instance subtype_uniq_mono' E L :
+ Proper (incl E L ==> eqtype E L ==> flip (subtype E L)) uniq_bor.
+ Proof. intros ??????. apply subtype_uniq_mono. done. by symmetry. Qed.
+ Global Instance subtype_uniq_proper E L κ :
+ Proper (eqtype E L ==> eqtype E L) (uniq_bor κ).
+ Proof. split; by apply subtype_uniq_mono. Qed.
End uniq_bor.
Notation "&uniq{ κ } ty" := (uniq_bor κ ty)
@@ -73,8 +113,8 @@ Section typing.
try by (iDestruct "Hown" as "[]" || iDestruct "Hown" as (l) "[% _]").
iDestruct "Hown" as (l') "[EQ [Hown Hf]]". iDestruct "EQ" as %[=]. subst l'.
iApply (fupd_mask_mono (↑lftN)). done.
- iMod (bor_create with "LFT Hown") as "[Hbor Hext]". done.
- iSplitL "Hbor". by simpl; eauto.
+ iMod (bor_create with "LFT Hown") as "[Hbor Hext]". done. iSplitL "Hbor".
+ { iExists _, _. erewrite <-uPred.iff_refl. auto. }
iIntros "!>#H†". iExists _. iMod ("Hext" with "H†") as "$". by iFrame.
Qed.
@@ -83,31 +123,15 @@ Section typing.
Proof.
iIntros (tid) "#LFT #Hord H". unfold has_type.
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'.
+ try by (iDestruct "H" as "[]" || iDestruct "H" as (l P) "[[% _] _]").
+ iDestruct "H" as (l' P) "[[EQ #HPiff] H]". iDestruct "EQ" as %[=]. subst l'.
iApply (fupd_mask_mono (↑lftN)). done.
+ iMod (bor_iff with "LFT [] H") as "H". done. by eauto.
iMod (rebor with "LFT Hord H") as "[H Hextr]". done.
- iModIntro. iSplitL "H". iExists _. by eauto.
- iIntros "H†". iExists _. by iMod ("Hextr" with "H†") as "$".
- Qed.
-
- Lemma lft_incl_ty_incl_uniq_bor ty κ1 κ2 :
- ty_incl (κ1 ⊑ κ2) (&uniq{κ2}ty) (&uniq{κ1}ty).
- Proof.
- iIntros (tid) "#LFT #Hincl!>". iSplit; iIntros "!#*H".
- - iDestruct "H" as (l) "[% Hown]". subst. iExists _. iSplit. done.
- by iApply (bor_shorten with "Hincl").
- - iAssert (κ1 ∪ κ ⊑ κ2 ∪ κ)%I as "#Hincl'".
- { iApply (lft_incl_glb with "[] []").
- - iApply (lft_incl_trans with "[] Hincl"). iApply lft_le_incl.
- apply gmultiset_union_subseteq_l.
- - iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
- iSplitL; last done. iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'.
- iFrame. iIntros "!#". iIntros (q' F) "% Htok".
- iMod (lft_incl_acc with "Hincl' Htok") as (q'') "[Htok Hclose]". set_solver.
- iMod ("Hupd" with "* [%] Htok") as "Hupd'"; try done. iModIntro. iNext.
- iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
- by iApply (ty_shr_mono with "LFT Hincl' H").
+ iModIntro. iSplitL "H".
+ - iExists _, _. erewrite <-uPred.iff_refl. auto.
+ - iIntros "H†". iExists _, _. iMod ("Hextr" with "H†") as "$".
+ iSplitR. done. iIntros "!>!#". apply uPred.iff_refl.
Qed.
Lemma consumes_copy_uniq_bor `(!Copy ty) κ κ' q:
@@ -116,7 +140,9 @@ Section typing.
Proof.
iIntros (ν tid Φ E ?) "#LFT (H◠& #H⊑ & Htok) 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↦]". iDestruct "Heq" as %[=->].
+ rewrite has_type_value. iDestruct "Hâ—" as (l' P) "[[Heq #HPiff] HP]".
+ iDestruct "Heq" as %[=->].
+ iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
iMod (bor_acc with "LFT H↦ Htok") as "[H↦ Hclose']". set_solver.
iDestruct "H↦" as (vl) "[>H↦ #Hown]".
@@ -124,7 +150,8 @@ Section typing.
by rewrite ty.(ty_size_eq).
iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦".
iMod ("Hclose'" with "[H↦]") as "[H↦ Htok]". by iExists _; iFrame.
- iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
+ iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv.
+ iExists _, _. erewrite <-uPred.iff_refl. auto.
Qed.
Lemma typed_deref_uniq_bor_own ty ν κ κ' q q':
@@ -134,15 +161,18 @@ Section typing.
Proof.
iIntros (tid) "!#(#HEAP & #LFT & (H◠& #H⊑ & Htok) & $)". wp_bind ν.
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↦]". iDestruct "Heq" as %[=->].
+ rewrite has_type_value. iDestruct "Hâ—" as (l P) "[[Heq #HPiff] HP]".
+ iDestruct "Heq" as %[=->].
+ iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[Htok Hclose]". done.
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.
iMod ("Hclose'" with "*[H↦ Hown H†][]") as "[Hbor Htok]"; last 1 first.
- iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
- iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
- iMod ("Hclose" with "Htok") as "$". iFrame "#". iExists _. eauto.
+ iMod (bor_sep _ _ _ (l' ↦∗: ty_own ty tid) with "LFT Hbor") as "[_ Hbor]". done.
+ iMod ("Hclose" with "Htok") as "$". iFrame "#". iExists _, _.
+ iFrame. iSplitR. done. by rewrite -uPred.iff_refl.
- iFrame "H↦ H†Hown".
- iIntros "!>(?&?&?)!>". iNext. iExists _.
rewrite -heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame.
@@ -155,19 +185,23 @@ Section typing.
Proof.
iIntros (tid) "!#(#HEAP & #LFT & (H◠& #H⊑1 & Htok & #H⊑2) & $)". wp_bind ν.
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↦]". iDestruct "Heq" as %[=->].
+ rewrite has_type_value. iDestruct "Hâ—" as (l P) "[[Heq #HPiff] HP]".
+ iDestruct "Heq" as %[=->].
+ iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
iMod (lft_incl_acc with "H⊑1 Htok") as (q'') "[Htok Hclose]". done.
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.
- iMod (bor_sep with "LFT Hbor") as "[Heq Hbor]". done.
- iMod (bor_persistent with "LFT Heq Htok") as "[>% Htok]". done. subst.
+ iMod (bor_exists with "LFT Hbor") as (P') "Hbor". done.
+ iMod (bor_sep with "LFT Hbor") as "[H Hbor]". done.
+ iMod (bor_persistent with "LFT H Htok") as "[[>% #HP'iff] Htok]". done. subst.
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 "#". iSplitL "Hbor".
- - iExists _. iSplitR; first by auto. iApply (bor_shorten with "[] Hbor").
+ - iExists _, _. iSplitR. by auto.
+ iApply (bor_shorten with "[] Hbor").
iApply (lft_incl_glb with "H⊑2"). iApply lft_incl_refl.
- iApply ("Hclose" with ">"). by iMod ("Hclose'" with "[$H↦]") as "[_ $]".
Qed.
@@ -178,12 +212,15 @@ Section typing.
Proof.
iIntros (ν tid Φ E ?) "#LFT (H◠& #H⊑ & Htok) 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↦)". iDestruct "Heq" as %[=->].
+ rewrite has_type_value. iDestruct "Hâ—" as (l P) "[[Heq #HPiff] HP]".
+ iDestruct "Heq" as %[=->].
+ iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
iMod (bor_acc with "LFT H↦ Htok") as "[H↦ Hclose']". set_solver.
iDestruct "H↦" as (vl) "[>H↦ Hown]". rewrite ty.(ty_size_eq).
iDestruct "Hown" as ">%". iApply "HΦ". iFrame "∗%#". iIntros (vl') "[H↦ Hown]".
iMod ("Hclose'" with "[H↦ Hown]") as "[Hbor Htok]". by iExists _; iFrame.
- iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
+ iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv.
+ iExists _, _. erewrite <-uPred.iff_refl. auto.
Qed.
End typing.
\ No newline at end of file
--
GitLab