From 22bff972550beffd1ea84ef1b6dc6911f646a115 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 24 Mar 2017 08:26:18 +0100
Subject: [PATCH] TyWf typeclass for describing lifetime constraints derived
from the syntactic structure of types.
---
theories/typing/bool.v | 2 +
theories/typing/examples/get_x.v | 2 +-
theories/typing/examples/init_prod.v | 3 +-
theories/typing/examples/lazy_lft.v | 3 +-
theories/typing/examples/rebor.v | 2 +-
theories/typing/examples/unbox.v | 2 +-
theories/typing/fixpoint.v | 19 +++
theories/typing/function.v | 42 +++---
theories/typing/int.v | 2 +
theories/typing/lft_contexts.v | 36 +++--
theories/typing/lib/cell.v | 22 +--
theories/typing/lib/fake_shared_box.v | 8 +-
theories/typing/lib/option.v | 8 +-
theories/typing/lib/rc.v | 43 +++---
theories/typing/lib/refcell/ref.v | 3 +
theories/typing/lib/refcell/ref_code.v | 122 ++++++++--------
theories/typing/lib/refcell/refcell.v | 3 +
theories/typing/lib/refcell/refcell_code.v | 20 +--
theories/typing/lib/refcell/refmut.v | 3 +
theories/typing/lib/refcell/refmut_code.v | 130 +++++++++---------
theories/typing/lib/rwlock/rwlock.v | 3 +
theories/typing/lib/rwlock/rwlock_code.v | 20 +--
theories/typing/lib/rwlock/rwlockreadguard.v | 3 +
.../typing/lib/rwlock/rwlockreadguard_code.v | 15 +-
theories/typing/lib/rwlock/rwlockwriteguard.v | 3 +
.../typing/lib/rwlock/rwlockwriteguard_code.v | 26 ++--
theories/typing/lib/spawn.v | 26 ++--
theories/typing/own.v | 10 +-
theories/typing/product.v | 3 +
theories/typing/shr_bor.v | 3 +
theories/typing/soundness.v | 4 +-
theories/typing/sum.v | 5 +
theories/typing/type.v | 67 ++++++++-
theories/typing/uninit.v | 5 +-
theories/typing/uniq_bor.v | 3 +
35 files changed, 404 insertions(+), 267 deletions(-)
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 0f6eee22..db1825ad 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -16,6 +16,8 @@ Section bool.
Next Obligation. intros ? [|[[| |[|[]|]]|] []]; auto. Qed.
Next Obligation. intros ? [|[[| |[|[]|]]|] []]; apply _. Qed.
+ Global Instance bool_wf : TyWf bool := { ty_lfts := []; ty_wf_E := [] }.
+
Global Instance bool_send : Send bool.
Proof. done. Qed.
End bool.
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 909052bc..0c0d96ed 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -12,7 +12,7 @@ Section get_x.
delete [ #1; "p"] ;; "return" ["r"].
Lemma get_x_type :
- typed_val get_x (fn(∀ α, λ Ï, [Ï âŠ‘ α]; &uniq{α} Î [int; int]) → &shr{α} int).
+ typed_val get_x (fn(∀ α, ∅; &uniq{α} Π[int; int]) → &shr{α} int).
(* FIXME: The above is pretty-printed with some explicit scope annotations,
and without using 'typed_instruction_ty'. I think that's related to
the list notation that we added to %TC. *)
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index 2d33668a..b13fe440 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -12,8 +12,7 @@ Section init_prod.
"r" +â‚— #0 <- "x'";; "r" +â‚— #1 <- "y'";;
delete [ #1; "x"] ;; delete [ #1; "y"] ;; return: ["r"].
- Lemma init_prod_type :
- typed_val init_prod (fn(λ Ï, []; int, int) → Î [int;int]).
+ Lemma init_prod_type : typed_val init_prod (fn(∅; int, int) → Π[int;int]).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([] Ï ret p). inv_vec p=>x y. simpl_subst.
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index 75e581ca..12d8c295 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -17,8 +17,7 @@ Section lazy_lft.
let: "r" := new [ #0] in
Endlft;; delete [ #2; "t"];; delete [ #1; "f"];; delete [ #1; "g"];; "return" ["r"].
- Lemma lazy_lft_type :
- typed_val lazy_lft (fn(λ Ï, []) → unit).
+ Lemma lazy_lft_type : typed_val lazy_lft (fn(∅) → unit).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([] Ï ret p). inv_vec p. simpl_subst.
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index f098582d..a434296c 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -17,7 +17,7 @@ Section rebor.
delete [ #1; "x"] ;; "return" ["r"].
Lemma rebor_type :
- typed_val rebor (fn(λ Ï, []; Î [int; int], Î [int; int]) → int).
+ typed_val rebor (fn(∅; Π[int; int], Π[int; int]) → int).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([] Ï ret p). inv_vec p=>t1 t2. simpl_subst.
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index 07049ade..586e2aa8 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -12,7 +12,7 @@ Section unbox.
delete [ #1; "b"] ;; "return" ["r"].
Lemma ubox_type :
- typed_val unbox (fn(∀ α, λ Ï, [Ï âŠ‘ α]; &uniq{α}box (Î [int; int])) → &uniq{α} int).
+ typed_val unbox (fn(∀ α, ∅; &uniq{α}box (Π[int; int])) → &uniq{α} int).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α Ï ret b). inv_vec b=>b. simpl_subst.
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index a3bd0cc2..847cac84 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -16,6 +16,25 @@ Section fixpoint_def.
Qed.
Definition type_fixpoint : type := fixpointK 2 T.
+
+ (* The procedure for computing ty_lfts and ty_wf_E for fixpoints is
+ the following:
+ - We do a first pass for computing [ty_lfts].
+ - In a second pass, we compute [ty_wf_E], by using the result of the
+ first pass.
+ I believe this gives the right sets for all types that we can define in
+ Rust, but I do not have any proof of this.
+ TODO : investigate this in more detail. *)
+ Global Instance type_fixpoint_wf `{∀ `{!TyWf ty}, TyWf (T ty)} : TyWf type_fixpoint :=
+ let lfts :=
+ let _ : TyWf type_fixpoint := {| ty_lfts := []; ty_wf_E := [] |} in
+ (T type_fixpoint).(ty_lfts)
+ in
+ let wf_E :=
+ let _ : TyWf type_fixpoint := {| ty_lfts := lfts; ty_wf_E := [] |} in
+ (T type_fixpoint).(ty_wf_E)
+ in
+ {| ty_lfts := lfts; ty_wf_E := wf_E |}.
End fixpoint_def.
Lemma type_fixpoint_ne `{typeG Σ} (T1 T2 : type → type)
diff --git a/theories/typing/function.v b/theories/typing/function.v
index a2cfc11c..b788a600 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -8,7 +8,12 @@ Set Default Proof Using "Type".
Section fn.
Context `{typeG Σ} {A : Type} {n : nat}.
- Record fn_params := FP' { fp_tys : vec type n; fp_ty : type; fp_E : lft → elctx }.
+ Record fn_params := FP { fp_E : lft → elctx; fp_tys : vec type n; fp_ty : type }.
+
+ Definition FP_wf E (tys : vec type n) `{!TyWfLst tys} ty `{!TyWf ty} :=
+ FP (λ Ï, E Ï ++ tys.(tyl_wf_E) ++ tys.(tyl_outlives_E) Ï ++
+ ty.(ty_wf_E) ++ ty.(ty_outlives_E) Ï)
+ tys ty.
Program Definition fn (fp : A → fn_params) : type :=
{| st_own tid vl := (∃ fb kb xb e H,
@@ -23,6 +28,14 @@ Section fn.
iIntros (fp tid vl) "H". iDestruct "H" as (fb kb xb e ?) "[% _]". by subst.
Qed.
+ (* FIXME : This definition is less restrictive than the one used in
+ Rust. In Rust, the type of parameters are taken into account for
+ well-formedness, and all the liftime constrains relating a
+ generalized liftime are ignored. For simplicity, we ignore all of
+ them, but this is not very faithful. *)
+ Global Instance fn_wf fp : TyWf (fn fp) :=
+ { ty_lfts := []; ty_wf_E := [] }.
+
Global Instance fn_send fp : Send (fn fp).
Proof. iIntros (tid1 tid2 vl). done. Qed.
@@ -47,8 +60,9 @@ Section fn.
Proof. intros ?? HR ??->. apply HR. Qed.
Global Instance FP_proper R :
- Proper (flip (Forall2 R : relation (vec _ _)) ==> R ==>
- pointwise_relation lft eq ==> fn_params_rel R) FP'.
+ Proper (pointwise_relation lft eq ==>
+ flip (Forall2 R : relation (vec _ _)) ==> R ==>
+ fn_params_rel R) FP.
Proof. by split; [|split]. Qed.
Global Instance fn_type_contractive n' :
@@ -98,12 +112,6 @@ End fn.
Arguments fn_params {_ _} _.
-(* The parameter of [FP'] are in the wrong order in order to make sure
- that type-checking is done in that order, so that the [ELCtx_Alive]
- is taken as a coercion. We reestablish the intuitive order with
- [FP] *)
-Notation FP E tys ty := (FP' tys ty E).
-
(* We use recursive notation for binders as well, to allow patterns
like '(a, b) to be used. In practice, only one binder is ever used,
but using recursive binders is the only way to make Coq accept
@@ -112,22 +120,24 @@ Notation FP E tys ty := (FP' tys ty E).
printing. Once on 8.6pl1, this should work. *)
Notation "'fn(∀' x .. x' ',' E ';' T1 ',' .. ',' TN ')' '→' R" :=
(fn (λ x, (.. (λ x',
- FP E%EL (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..)%T R%T)..)))
+ FP_wf E%EL (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..)%T R%T)..)))
(at level 99, R at level 200, x binder, x' binder,
format "'fn(∀' x .. x' ',' E ';' T1 ',' .. ',' TN ')' '→' R") : lrust_type_scope.
Notation "'fn(∀' x .. x' ',' E ')' '→' R" :=
- (fn (λ x, (.. (λ x', FP E%EL Vector.nil R%T)..)))
+ (fn (λ x, (.. (λ x', FP_wf E%EL Vector.nil R%T)..)))
(at level 99, R at level 200, x binder, x' binder,
format "'fn(∀' x .. x' ',' E ')' '→' R") : lrust_type_scope.
Notation "'fn(' E ';' T1 ',' .. ',' TN ')' '→' R" :=
- (fn (λ _:(), FP E%EL (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..) R%T))
+ (fn (λ _:(), FP_wf E%EL (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..) R%T))
(at level 99, R at level 200,
format "'fn(' E ';' T1 ',' .. ',' TN ')' '→' R") : lrust_type_scope.
Notation "'fn(' E ')' '→' R" :=
- (fn (λ _:(), FP E%EL Vector.nil R%T))
+ (fn (λ _:(), FP_wf E%EL Vector.nil R%T))
(at level 99, R at level 200,
format "'fn(' E ')' '→' R") : lrust_type_scope.
+Instance elctx_empty : Empty (lft → elctx) := λ Ï, [].
+
Section typing.
Context `{typeG Σ}.
@@ -191,7 +201,7 @@ Section typing.
Proof.
intros fp1 fp2 Hfp. apply fn_subtype=>x Ï. destruct (Hfp x) as (Htys & Hty & HE).
split; last split.
- - rewrite (HE Ï). apply elctx_sat_app_weaken_l, elctx_sat_refl.
+ - rewrite (HE Ï). solve_typing.
- eapply Forall2_impl; first eapply Htys. intros ??.
eapply subtype_weaken; last done. by apply submseteq_inserts_r.
- eapply subtype_weaken, Hty; last done. by apply submseteq_inserts_r.
@@ -202,11 +212,11 @@ Section typing.
eqtype E0 L0) fn.
Proof.
intros fp1 fp2 Hfp. split; eapply fn_subtype=>x Ï; destruct (Hfp x) as (Htys & Hty & HE); (split; last split).
- - rewrite (HE Ï). apply elctx_sat_app_weaken_l, elctx_sat_refl.
+ - rewrite (HE Ï). solve_typing.
- eapply Forall2_impl; first eapply Htys. intros t1 t2 Ht.
eapply subtype_weaken; last apply Ht; last done. by apply submseteq_inserts_r.
- eapply subtype_weaken; last apply Hty; last done. by apply submseteq_inserts_r.
- - rewrite (HE Ï). apply elctx_sat_app_weaken_l, elctx_sat_refl.
+ - rewrite (HE Ï). solve_typing.
- symmetry in Htys. eapply Forall2_impl; first eapply Htys. intros t1 t2 Ht.
eapply subtype_weaken; last apply Ht; last done. by apply submseteq_inserts_r.
- eapply subtype_weaken; last apply Hty; last done. by apply submseteq_inserts_r.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 520901b9..93e879ce 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -15,6 +15,8 @@ Section int.
Next Obligation. intros ? [|[[]|] []]; auto. Qed.
Next Obligation. intros ? [|[[]|] []]; apply _. Qed.
+ Global Instance int_wf : TyWf int := { ty_lfts := []; ty_wf_E := [] }.
+
Global Instance int_send : Send int.
Proof. done. Qed.
End int.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 6ad7b8d0..5c16ddf5 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -114,6 +114,9 @@ Section lft_contexts.
Definition lctx_lft_eq κ κ' : Prop :=
lctx_lft_incl κ κ' ∧ lctx_lft_incl κ' κ.
+ Lemma lctx_lft_incl_incl κ κ' : lctx_lft_incl κ κ' → lctx_lft_incl κ κ'.
+ Proof. done. Qed.
+
Lemma lctx_lft_incl_relf κ : lctx_lft_incl κ κ.
Proof. iIntros (qL) "_ !# _". iApply lft_incl_refl. Qed.
@@ -300,26 +303,12 @@ Arguments lctx_lft_incl {_ _ _} _%EL _%LL _ _.
Arguments lctx_lft_eq {_ _ _} _%EL _%LL _ _.
Arguments lctx_lft_alive {_ _ _} _%EL _%LL _.
Arguments elctx_sat {_ _ _} _%EL _%LL _%EL.
+Arguments lctx_lft_incl_incl {_ _ _ _%EL _%LL} _ _.
Arguments lctx_lft_alive_tok {_ _ _ _%EL _%LL} _ _ _.
-Lemma elctx_sat_cons_weaken `{invG Σ, lftG Σ} e0 E E' L :
- elctx_sat E L E' → elctx_sat (e0 :: E) L E'.
-Proof.
- iIntros (HE' ?) "HL". iDestruct (HE' with "HL") as "#HE'".
- iClear "∗". iIntros "!# #[_ HE]". iApply "HE'". done.
-Qed.
-
-Lemma elctx_sat_app_weaken_l `{invG Σ, lftG Σ} E0 E E' L :
- elctx_sat E L E' → elctx_sat (E0 ++ E) L E'.
-Proof. induction E0=>//= ?. auto using elctx_sat_cons_weaken. Qed.
-
-Lemma elctx_sat_app_weaken_r `{invG Σ, lftG Σ} E0 E E' L :
- elctx_sat E L E' → elctx_sat (E ++ E0) L E'.
-Proof.
- intros ?. rewrite /elctx_sat /elctx_interp.
- setoid_rewrite (big_opL_permutation _ (E++E0)); try apply Permutation_app_comm.
- by apply elctx_sat_app_weaken_l.
-Qed.
+Lemma elctx_sat_submseteq `{invG Σ, lftG Σ} E E' L :
+ E' ⊆+ E → elctx_sat E L E'.
+Proof. iIntros (HE' ?) "_ !# H". by iApply big_sepL_submseteq. Qed.
Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
Hint Resolve of_val_unlock : lrust_typing.
@@ -328,8 +317,15 @@ Hint Resolve
lctx_lft_incl_external'
lctx_lft_alive_static lctx_lft_alive_local lctx_lft_alive_external
elctx_sat_nil elctx_sat_lft_incl elctx_sat_app elctx_sat_refl
+ submseteq_cons submseteq_inserts_l submseteq_inserts_r
: lrust_typing.
-Hint Resolve elctx_sat_cons_weaken elctx_sat_app_weaken_l elctx_sat_app_weaken_r
- | 100 : lrust_typing.
+
+Hint Resolve elctx_sat_submseteq | 100 : lrust_typing.
+
+(* FIXME : I would prefer using a [Hint Resolve <-] for this, but
+ unfortunately, this is not preserved across modules. See:
+ https://coq.inria.fr/bugs/show_bug.cgi?id=5189
+ This should be fixed in the next version of Coq. *)
+Hint Extern 1 (_ ∈ _ ++ _) => apply <- @elem_of_app : lrust_typing.
Hint Opaque elctx_sat lctx_lft_alive lctx_lft_incl : lrust_typing.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 06c092ad..1de6c057 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -21,6 +21,9 @@ Section cell.
iIntros (ty ?? tid l) "#H⊑ H". by iApply (na_bor_shorten with "H⊑").
Qed.
+ Global Instance cell_wf ty `{!TyWf ty} : TyWf (cell ty) :=
+ { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
Global Instance cell_type_ne : TypeNonExpansive cell.
Proof. solve_type_proper. Qed.
@@ -85,8 +88,7 @@ Section typing.
(* Constructing a cell. *)
Definition cell_new : val := funrec: <> ["x"] := return: ["x"].
- Lemma cell_new_type ty :
- typed_val cell_new (fn(λ _, []; ty) → cell ty).
+ Lemma cell_new_type ty `{!TyWf ty} : typed_val cell_new (fn(∅; ty) → cell ty).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (_ Ï ret arg). inv_vec arg=>x. simpl_subst.
@@ -97,8 +99,8 @@ Section typing.
(* The other direction: getting ownership out of a cell. *)
Definition cell_into_inner : val := funrec: <> ["x"] := return: ["x"].
- Lemma cell_into_inner_type ty :
- typed_val cell_into_inner (fn(λ _, []; cell ty) → ty).
+ Lemma cell_into_inner_type ty `{!TyWf ty} :
+ typed_val cell_into_inner (fn(∅; cell ty) → ty).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (_ Ï ret arg). inv_vec arg=>x. simpl_subst.
@@ -109,8 +111,8 @@ Section typing.
Definition cell_get_mut : val :=
funrec: <> ["x"] := return: ["x"].
- Lemma cell_get_mut_type ty :
- typed_val cell_get_mut (fn(∀ α, λ Ï, [Ï âŠ‘ α]; &uniq{α} (cell ty)) → &uniq{α} ty).
+ Lemma cell_get_mut_type ty `{!TyWf ty} :
+ typed_val cell_get_mut (fn(∀ α, ∅; &uniq{α} (cell ty)) → &uniq{α} ty).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
@@ -126,8 +128,8 @@ Section typing.
letalloc: "r" <-{ty.(ty_size)} !"x'" in
delete [ #1; "x"];; return: ["r"].
- Lemma cell_get_type `(!Copy ty) :
- typed_val (cell_get ty) (fn(∀ α, λ Ï, [Ï âŠ‘ α]; &shr{α} (cell ty)) → ty).
+ Lemma cell_get_type ty `{!TyWf ty} `(!Copy ty) :
+ typed_val (cell_get ty) (fn(∀ α, ∅; &shr{α} (cell ty)) → ty).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
@@ -146,8 +148,8 @@ Section typing.
"c'" <-{ty.(ty_size)} !"x";;
delete [ #1; "c"] ;; delete [ #ty.(ty_size); "x"] ;; return: ["r"].
- Lemma cell_replace_type ty :
- typed_val (cell_replace ty) (fn(∀ α, λ Ï, [Ï âŠ‘ α]; &shr{α} cell ty, ty) → ty).
+ Lemma cell_replace_type ty `{!TyWf ty} :
+ typed_val (cell_replace ty) (fn(∀ α, ∅; &shr{α} cell ty, ty) → ty).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α Ï ret arg). inv_vec arg=>c x. simpl_subst.
diff --git a/theories/typing/lib/fake_shared_box.v b/theories/typing/lib/fake_shared_box.v
index 2d5487ed..f2523481 100644
--- a/theories/typing/lib/fake_shared_box.v
+++ b/theories/typing/lib/fake_shared_box.v
@@ -9,17 +9,15 @@ Section fake_shared_box.
Definition fake_shared_box : val :=
funrec: <> ["x"] := Skip ;; return: ["x"].
- Lemma cell_replace_type ty :
+ Lemma fake_shared_box_type ty `{!TyWf ty} :
typed_val fake_shared_box
- (fn (fun '(α, β) => FP (λ Ï, [Ï âŠ‘ α; α ⊑ β]%EL)
- [# &shr{α}(&shr{β} ty)] (&shr{α}box ty))).
+ (fn (fun '(α, β) => FP_wf ∅ [# &shr{α}(&shr{β} ty)] (&shr{α}box ty))).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] Ï ret arg). inv_vec arg=>x. simpl_subst.
iIntros (tid) "#LFT #HE Hna HL Hk HT".
rewrite tctx_interp_singleton tctx_hasty_val.
- rewrite {1}/elctx_interp big_sepL_cons big_sepL_singleton.
- iDestruct "HE" as "(Hβ & #Hαβ)".
+ iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
iAssert (▷ ty_own (own_ptr 1 (&shr{α} box ty)) tid [x])%I with "[HT]" as "HT".
{ destruct x as [[|l|]|]=>//=. iDestruct "HT" as "[H $]".
iNext. iDestruct "H" as ([|[[]|][]]) "[H↦ H]"; try done.
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index 68ab6ea0..9b6594b0 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -22,9 +22,9 @@ Section option.
cont: "k" [] :=
delete [ #1; "o"];; return: ["r"].
- Lemma option_as_mut_type Ï„ :
+ Lemma option_as_mut_type Ï„ `{!TyWf Ï„} :
typed_val
- option_as_mut (fn(∀ α, (λ Ï, [Ï âŠ‘ α]); &uniq{α} (option Ï„)) → option (&uniq{α}Ï„)).
+ option_as_mut (fn(∀ α, ∅; &uniq{α} (option τ)) → option (&uniq{α}τ)).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α Ï ret p).
inv_vec p=>o. simpl_subst.
@@ -53,8 +53,8 @@ Section option.
delete [ #(S Ï„.(ty_size)); "o"];; delete [ #Ï„.(ty_size); "def"];;
return: ["r"]].
- Lemma option_unwrap_or_type Ï„ :
- typed_val (option_unwrap_or Ï„) (fn((λ Ï, []); option Ï„, Ï„) → Ï„).
+ Lemma option_unwrap_or_type Ï„ `{!TyWf Ï„} :
+ typed_val (option_unwrap_or τ) (fn(∅; option τ, τ) → τ).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([] Ï ret p). inv_vec p=>o def. simpl_subst.
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index ccb80f73..68759c9e 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -89,10 +89,13 @@ Section rc.
iModIntro. iNext. iAssert X with "[>HP]" as "HX".
{ iDestruct "HP" as "[[Hl' [H†Hown]]|$]"; last done.
iMod (lft_create with "LFT") as (ν) "[[Hν1 Hν2] #Hν†]"; first solve_ndisj.
- (* TODO: We should consider changing the statement of bor_create to dis-entangle the two masks such that this is no longer necessary. *)
+ (* TODO: We should consider changing the statement of
+ bor_create to dis-entangle the two masks such that this is no
+ longer necessary. *)
iApply (fupd_mask_mono (↑lftN)); first solve_ndisj.
iMod (bor_create with "LFT Hown") as "[HP HPend]"; first solve_ndisj.
- iMod (own_alloc (◠Some ((1/2)%Qp, 1%positive) ⋅ ◯ Some ((1/2)%Qp, 1%positive))) as (γ) "[Ha Hf]".
+ iMod (own_alloc (â— Some ((1/2)%Qp, 1%positive) â‹…
+ ◯ Some ((1/2)%Qp, 1%positive))) as (γ) "[Ha Hf]".
{ apply auth_valid_discrete_2. done. }
iMod (na_inv_alloc tid _ _ (rc_inv tid ν γ l' ty) with "[Ha Hν2 Hl' H†HPend]").
{ rewrite /rc_inv. iExists (Some (_, _)). iFrame. iExists _. iFrame "#∗".
@@ -134,6 +137,9 @@ Section rc.
- by iApply na_bor_shorten.
Qed.
+ Global Instance rc_wf ty `{!TyWf ty} : TyWf (rc ty) :=
+ { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
Global Instance rc_type_contractive : TypeContractive rc.
Proof.
constructor;
@@ -148,8 +154,10 @@ Section rc.
Lemma rc_subtype ty1 ty2 :
type_incl ty1 ty2 -∗ type_incl (rc ty1) (rc ty2).
Proof.
- iIntros "#Hincl". iPoseProof "Hincl" as "Hincl2". iDestruct "Hincl2" as "(#Hsz & #Hoincl & #Hsincl)".
- (* FIXME: Would be nice to have an easier way to duplicate destructed things. Maybe iPoseProof with a destruct pattern? *)
+ iIntros "#Hincl". iPoseProof "Hincl" as "Hincl2".
+ iDestruct "Hincl2" as "(#Hsz & #Hoincl & #Hsincl)".
+ (* FIXME: Would be nice to have an easier way to duplicate
+ destructed things. Maybe iPoseProof with a destruct pattern? *)
iSplit; first done. iSplit; iAlways.
- iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
iDestruct "Hvl" as "[(Hl & H†& Hc) | Hvl]".
@@ -178,7 +186,6 @@ Section rc.
Global Instance rc_proper E L :
Proper (eqtype E L ==> eqtype E L) rc.
Proof. intros ??[]. by split; apply rc_mono. Qed.
-
End rc.
Section code.
@@ -247,8 +254,8 @@ Section code.
"rc" +â‚— #0 <- "rcbox";;
delete [ #ty.(ty_size); "x"];; return: ["rc"].
- Lemma rc_new_type ty :
- typed_val (rc_new ty) (fn(λ _, []; ty) → rc ty).
+ Lemma rc_new_type ty `{!TyWf ty} :
+ typed_val (rc_new ty) (fn(∅; ty) → rc ty).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (_ Ï ret arg). inv_vec arg=>x. simpl_subst.
@@ -286,8 +293,8 @@ Section code.
"rc2" <- "rc''";;
delete [ #1; "rc" ];; return: ["rc2"].
- Lemma rc_clone_type ty :
- typed_val rc_clone (fn(∀ α, λ Ï, [Ï âŠ‘ α]; &shr{α} rc ty) → rc ty).
+ Lemma rc_clone_type ty `{!TyWf ty} :
+ typed_val rc_clone (fn(∀ α, ∅; &shr{α} rc ty) → rc ty).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
@@ -326,7 +333,7 @@ Section code.
iMod ("Hclose3" with "[$Hrctok] Hna") as "[Hα1 Hna]".
iMod ("Hclose2" with "[Hrc◠Hl' Hl'†Hνtok2 Hν†$Hna]") as "Hna".
{ iExists _. iFrame "Hrcâ—". iExists _. rewrite Z.add_comm. iFrame "∗ Hνend".
- rewrite [_ â‹… _]comm frac_op' -assoc Qp_div_2. auto. }
+ rewrite [_ â‹… _]comm frac_op' -[(_ + _)%Qp]assoc. rewrite Qp_div_2. auto. }
iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
(* Finish up the proof. *)
iApply (type_type _ _ _ [ x ◠box (&shr{α} rc ty); #lrc2 ◠box (rc ty)]%TC
@@ -345,8 +352,8 @@ Section code.
"x" <- (!"rc'" +â‚— #1);;
delete [ #1; "rc" ];; return: ["x"].
- Lemma rc_deref_type ty :
- typed_val rc_deref (fn(∀ α, λ Ï, [Ï âŠ‘ α]; &shr{α} rc ty) → &shr{α} ty).
+ Lemma rc_deref_type ty `{!TyWf ty} :
+ typed_val rc_deref (fn(∀ α, ∅; &shr{α} rc ty) → &shr{α} ty).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α Ï ret arg). inv_vec arg=>rcx. simpl_subst.
@@ -395,8 +402,8 @@ Section code.
cont: "k" [] :=
delete [ #1; "rc"];; return: ["r"].
- Lemma rc_try_unwrap_type ty :
- typed_val (rc_try_unwrap ty) (fn(λ _, []; rc ty) → Σ[ ty; rc ty ]).
+ Lemma rc_try_unwrap_type ty `{!TyWf ty} :
+ typed_val (rc_try_unwrap ty) (fn(∅; rc ty) → Σ[ ty; rc ty ]).
Proof.
(* TODO: There is a *lot* of duplication between this proof and the one for drop. *)
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
@@ -463,8 +470,8 @@ Section code.
cont: "k" [] :=
delete [ #1; "rc"];; return: ["x"].
- Lemma rc_drop_type ty :
- typed_val (rc_drop ty) (fn(λ _, []; rc ty) → option ty).
+ Lemma rc_drop_type ty `{!TyWf ty} :
+ typed_val (rc_drop ty) (fn(∅; rc ty) → option ty).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (_ Ï ret arg). inv_vec arg=>rcx. simpl_subst.
@@ -534,8 +541,8 @@ Section code.
cont: "k" [] :=
delete [ #1; "rc"];; return: ["x"].
- Lemma rc_get_mut_type ty :
- typed_val rc_get_mut (fn(∀ α, λ Ï, [Ï âŠ‘ α]; &uniq{α} rc ty) → option (&uniq{α} ty)).
+ Lemma rc_get_mut_type ty `{!TyWf ty} :
+ typed_val rc_get_mut (fn(∀ α, ∅; &uniq{α} rc ty) → option (&uniq{α} ty)).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α Ï ret arg). inv_vec arg=>rcx. simpl_subst.
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index 785cf6af..dfa8aec0 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -68,6 +68,9 @@ Section ref.
- by iApply na_bor_shorten.
Qed.
+ Global Instance ref_wf α ty `{!TyWf ty} : TyWf (ref α ty) :=
+ { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+
Global Instance ref_type_contractive α : TypeContractive (ref α).
Proof. solve_type_proper. Qed.
Global Instance ref_ne α : NonExpansive (ref α).
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index e71822ae..9f7c86c5 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -54,16 +54,13 @@ Section ref_functions.
(* FIXME : using λ instead of fun triggers an anomaly.
See: https://coq.inria.fr/bugs/show_bug.cgi?id=5326 *)
- Lemma ref_clone_type ty :
- typed_val ref_clone
- (fn (fun '(α, β) => FP (λ Ï, [Ï âŠ‘ α; α ⊑ β]%EL)
- [# &shr{α}(ref β ty)]%T (ref β ty)%T)).
+ Lemma ref_clone_type ty `{!TyWf ty} :
+ typed_val ref_clone (fn (fun '(α, β) =>
+ FP_wf ∅ [# &shr{α}(ref β ty)]%T (ref β ty)%T)).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (x').
-
-Typeclasses Opaque llctx_interp.
iIntros (tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
@@ -119,10 +116,9 @@ Typeclasses Opaque llctx_interp.
letalloc: "r" <- "r'" in
delete [ #1; "x"];; return: ["r"].
- Lemma ref_deref_type ty :
+ Lemma ref_deref_type ty `{!TyWf ty} :
typed_val ref_deref
- (fn (fun '(α, β) => FP (λ Ï, [Ï âŠ‘ α; α ⊑ β]%EL)
- [# &shr{α}(ref β ty)]%T (&shr{α}ty)%T)).
+ (fn (fun '(α, β) => FP_wf ∅ [# &shr{α}(ref β ty)]%T (&shr{α}ty)%T)).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] Ï ret arg). inv_vec arg=>x. simpl_subst.
@@ -136,12 +132,12 @@ Typeclasses Opaque llctx_interp.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iMod "H↦" as "[H↦1 H↦2]". wp_read. wp_let.
iMod ("Hcloseα" with "[$H↦1 $H↦2]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
+ iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
iApply (type_type _ _ _
[ x ◠box (&shr{α} ref β ty); #lv ◠&shr{α}ty]%TC
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
- iFrame. iApply (ty_shr_mono with "[] Hshr"). iApply lft_incl_glb; last done.
- rewrite /elctx_interp. iDestruct "HE" as "(_ & $ & _)". }
+ iFrame. iApply (ty_shr_mono with "[] Hshr"). by iApply lft_incl_glb. }
iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
@@ -157,8 +153,8 @@ Typeclasses Opaque llctx_interp.
delete [ #2; "x"];;
let: "r" := new [ #0] in return: ["r"].
- Lemma ref_drop_type ty :
- typed_val ref_drop (fn(∀ α, (λ Ï, [Ï âŠ‘ α]); ref α ty) → unit).
+ Lemma ref_drop_type ty `{!TyWf ty} :
+ typed_val ref_drop (fn(∀ α, ∅; ref α ty) → unit).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
@@ -210,67 +206,73 @@ Typeclasses Opaque llctx_interp.
(* Apply a function within the ref, typically for accessing a component. *)
Definition ref_map : val :=
funrec: <> ["ref"; "f"; "env"] :=
- withcont: "k":
- let: "x'" := !"ref" in
let: "f'" := !"f" in
+ Newlft;;
+ let: "x'" := !"ref" in
letalloc: "x" <- "x'" in
letcall: "r" := "f'" ["env"; "x"]%E in
- let: "r'" := !"r" in
+ let: "r'" := !"r" in delete [ #1; "r"];;
+ Endlft;;
"ref" <- "r'";;
- delete [ #1; "f"];; "k" []
- cont: "k" [] :=
- return: ["ref"].
+ delete [ #1; "f"];; return: ["ref"].
- Lemma ref_map_type ty1 ty2 envty E :
+ Lemma ref_map_type ty1 ty2 envty `{!TyWf ty1, !TyWf ty2, !TyWf envty} :
typed_val ref_map
- (fn(∀ β, [β]%EL ++ E;
- ref β ty1, fn(∀ α, [α]%EL ++ E; envty, &shr{α}ty1) → &shr{α}ty2, envty)
+ (fn(∀ β, ∅; ref β ty1, fn(∀ α, ∅; envty, &shr{α}ty1) → &shr{α}ty2, envty)
→ ref β ty2).
Proof.
- intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
+ intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α Ï ret arg).
inv_vec arg=>ref f env. simpl_subst.
- iIntros (tid qE) "#LFT Hna HE HL Hk HT".
- rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
- iDestruct "HT" as "(Href & Hf & Henv)".
- destruct ref as [[|lref|]|]; try done. iDestruct "Href" as "[Href Href†]".
+ iApply type_deref; [solve_typing..|]. iIntros (f'). simpl_subst.
+ iApply (type_newlft [Ï]). iIntros (κ tid) "#LFT #HE Hna HL Hk (Hf & #Hf' & Href & Henv)".
+ rewrite (tctx_hasty_val _ ref). destruct ref as [[|lref|]|]; try done.
+ iDestruct "Href" as "[Href Href†]".
iDestruct "Href" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Href";
try iDestruct "Href" as "[_ >[]]".
rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
iDestruct "Href" as (ν qν γ β ty') "(#Hshr & #Hαβ & #Hinv & >Hν & Hγ)".
- rewrite -(freeable_sz_split _ 1 1). iDestruct "Href†" as "[Href†1 Href†2]".
- destruct (Qp_lower_bound qE qν) as (q & qE' & qν' & -> & ->).
- iDestruct (@fractional_split with "HE") as "[[Hα HE] HE']".
- iDestruct "Hν" as "[Hν Hν']".
- remember (RecV "k" [] (ret [ LitV lref])%E)%V as k eqn:EQk.
- iApply (wp_let' _ _ _ _ k). { subst. solve_to_val. } simpl_subst.
- iApply (type_type ((α ⊓ ν) :: E)%EL []
- [k â—cont([], λ _:vec val 0, [ #lref â— own_ptr 2 (&shr{α ⊓ ν}ty2)])]%CC
- [ f ◠box (fn(∀ α, [α]%EL ++ E; envty, &shr{α}ty1) → &shr{α}ty2);
- #lref ◠own_ptr 2 (&shr{α ⊓ ν}ty1); env ◠box envty ]%TC
- with "[] LFT Hna [$HE Hα Hν] HL [Hk HE' Hν' Href↦2 Hγ Href†2]"); first last.
- { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
- iFrame. iApply tctx_hasty_val'. done. iFrame. iExists [_].
- rewrite heap_mapsto_vec_singleton. by iFrame. }
- { rewrite !cctx_interp_singleton /=. iIntros "HE". iIntros (args) "Hna HL HT".
- inv_vec args. subst. simpl. wp_rec. iDestruct "HE" as "[Hαν HE]".
- iDestruct (lft_tok_sep with "Hαν") as "[Hα Hν]".
- iSpecialize ("Hk" with "[$HE' $Hα $HE]").
- iApply ("Hk" $! [# #lref] with "Hna HL").
- rewrite !tctx_interp_singleton !tctx_hasty_val' //.
- iDestruct "HT" as "[Href Ḥref†2]".
- rewrite /= -(freeable_sz_split _ 1 1). iFrame.
- iDestruct "Href" as ([|[[|lv'|]|] [|]]) "[H↦ Href]"; auto.
- iExists [ #lv'; #lrc].
- rewrite (heap_mapsto_vec_cons _ _ _ [_]) !heap_mapsto_vec_singleton. iFrame.
- iExists ν, (q+qν')%Qp. eauto 10 with iFrame. }
- { rewrite /= -lft_tok_sep. iFrame. }
- iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
- iApply type_deref; [solve_typing..|]. iIntros (f'). simpl_subst.
- iApply type_letalloc_1; [solve_typing..|]. iIntros (x). simpl_subst.
- iApply (type_letcall); [simpl; solve_typing..|]. iIntros (r). simpl_subst.
- iApply type_deref; [solve_typing..|]. iIntros (r'). simpl_subst.
- iApply type_assign; [solve_typing..|].
+ wp_read. wp_let. wp_apply wp_new; first done.
+ iIntros (lx [|? []]) "(% & H†& Hlx)"; try (simpl in *; lia).
+ rewrite heap_mapsto_vec_singleton. wp_let. wp_write.
+ match goal with | |- context [(WP (_ [?k']) {{_, _}})%I] =>
+ assert (∃ k, to_val k' = Some k) as [k EQk] by (eexists; solve_to_val) end.
+ iApply (wp_let' _ _ _ _ k _ EQk). simpl_subst. iNext.
+ iDestruct (lctx_lft_incl_incl κ α with "HL HE") as "#Hκα"; [solve_typing..|].
+ iMod (bor_create _ κ (qν).[ν] with "LFT [$Hν]") as "[Hb Hν]"; first done.
+ iAssert (κ ⊑ α ⊓ ν)%I with "[>Hb]" as "#Hκν".
+ { iApply (lft_incl_glb with "Hκα"). iApply (frac_bor_lft_incl with "LFT").
+ iApply (bor_fracture with "LFT [> -]"); first done. rewrite /= Qp_mult_1_r //. }
+ iApply (type_type ((κ ⊑ α ⊓ ν) :: (α ⊓ ν ⊑ α) :: _)%EL _
+ [k â—cont(_, λ x:vec val 1, [ x!!!0 â— box (&shr{α ⊓ ν}ty2)])]%CC
+ [ f' ◠fn(∀ α, ∅; envty, &shr{α}ty1) → &shr{α}ty2;
+ #lx ◠box (&shr{α ⊓ ν}ty1); env ◠box envty ]%TC
+ with "[] LFT [] Hna HL [-H†Hlx Henv]"); swap 1 2; swap 3 4.
+ { iSplitL; last iSplitL; [done|iApply lft_intersect_incl_l|iApply "HE"]. }
+ { iApply (type_call (α ⊓ ν)); solve_typing. }
+ { iFrame "∗#". iApply tctx_hasty_val'; first done. rewrite -freeable_sz_full.
+ iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. auto. }
+ iIntros (? ->%elem_of_list_singleton arg) "Hna HL Hr". inv_vec arg=>r.
+ apply of_to_val in EQk. rewrite EQk. iApply wp_rec; try (done || apply _).
+ { repeat econstructor. by rewrite to_of_val. } simpl_subst.
+ rewrite /tctx_interp big_sepL_singleton (tctx_hasty_val _ r) ownptr_own.
+ iDestruct "Hr" as (lr vr) "(% & Hlr & Hvr & H†)". subst. inv_vec vr=>r'. iNext.
+ rewrite heap_mapsto_vec_singleton. wp_read. wp_let.
+ wp_apply (wp_delete _ _ _ [_] with "[Hlr H†]"). done.
+ { rewrite heap_mapsto_vec_singleton freeable_sz_full. iFrame. }
+ iIntros "_". wp_seq. wp_bind Endlft. iDestruct "HL" as "[Hκ HL]".
+ iDestruct "Hκ" as (κ') "(% & Hκ' & #Hκ'†)". simpl in *. subst κ.
+ iSpecialize ("Hκ'†" with "Hκ'").
+ iApply wp_mask_mono; last iApply (wp_step_fupd with "Hκ'†"); auto with ndisj.
+ wp_seq. iIntros "Hκ'†!>". iMod ("Hν" with "[Hκ'†]") as "Hν";
+ first by rewrite -lft_dead_or; auto. wp_seq. wp_write.
+ iApply (type_type _ _ _
+ [ f ◠box (fn(∀ α, ∅; envty, &shr{α}ty1) → &shr{α}ty2);
+ #lref ◠box (ref α ty2) ]%TC
+ with "[] LFT HE Hna HL Hk"); first last.
+ { iFrame. rewrite big_sepL_singleton tctx_hasty_val. iExists _. iSplit. done.
+ iFrame. iExists [_;_]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+ iFrame. destruct r' as [[]|]=>//=. auto 10 with iFrame. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 4bfb076b..f34f6305 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -156,6 +156,9 @@ Section refcell.
iExists _, _. iFrame. iApply lft_incl_trans; auto.
Qed.
+ Global Instance refcell_wf ty `{!TyWf ty} : TyWf (refcell ty) :=
+ { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
Global Instance refcell_type_ne : TypeNonExpansive refcell.
Proof.
constructor;
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index eb8c3090..6f986424 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -19,8 +19,8 @@ Section refcell_functions.
"r" +â‚— #1 <-{ty.(ty_size)} !"x";;
delete [ #ty.(ty_size) ; "x"];; return: ["r"].
- Lemma refcell_new_type ty :
- typed_val (refcell_new ty) (fn(λ Ï, []; ty) → refcell ty).
+ Lemma refcell_new_type ty `{!TyWf ty} :
+ typed_val (refcell_new ty) (fn(∅; ty) → refcell ty).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (_ Ï ret arg). inv_vec arg=>x. simpl_subst.
@@ -54,8 +54,8 @@ Section refcell_functions.
Leaving them away is inconsistent with `let ... := !"x" +â‚— #1`. *)
delete [ #(S ty.(ty_size)) ; "x"];; return: ["r"].
- Lemma refcell_into_inner_type ty :
- typed_val (refcell_into_inner ty) (fn(λ Ï, []; refcell ty) → ty).
+ Lemma refcell_into_inner_type ty `{!TyWf ty} :
+ typed_val (refcell_into_inner ty) (fn(∅; refcell ty) → ty).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (_ Ï ret arg). inv_vec arg=>x. simpl_subst.
@@ -88,9 +88,9 @@ Section refcell_functions.
"x" <- "x'" +â‚— #1;;
return: ["x"].
- Lemma refcell_get_mut_type ty :
+ Lemma refcell_get_mut_type ty `{!TyWf ty} :
typed_val refcell_get_mut
- (fn(∀ α, λ Ï, [Ï âŠ‘ α]; &uniq{α} (refcell ty)) → &uniq{α} ty)%T.
+ (fn(∀ α, ∅; &uniq{α} (refcell ty)) → &uniq{α} ty)%T.
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
@@ -139,9 +139,9 @@ Section refcell_functions.
cont: "k" [] :=
delete [ #1; "x"];; return: ["r"].
- Lemma refcell_try_borrow_type ty :
+ Lemma refcell_try_borrow_type ty `{!TyWf ty} :
typed_val refcell_try_borrow
- (fn(∀ α, λ Ï, [Ï âŠ‘ α] ; &shr{α}(refcell ty)) → option (ref α ty)).
+ (fn(∀ α, ∅; &shr{α}(refcell ty)) → option (ref α ty)).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
@@ -246,9 +246,9 @@ Section refcell_functions.
cont: "k" [] :=
delete [ #1; "x"];; return: ["r"].
- Lemma refcell_try_borrow_mut_type ty :
+ Lemma refcell_try_borrow_mut_type ty `{!TyWf ty} :
typed_val refcell_try_borrow_mut
- (fn(∀ α, λ Ï, [Ï âŠ‘ α]; &shr{α}(refcell ty)) → option (refmut α ty))%T.
+ (fn(∀ α, ∅; &shr{α}(refcell ty)) → option (refmut α ty))%T.
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index 7f12fb47..98a2abe3 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -72,6 +72,9 @@ Section refmut.
iApply ty_shr_mono; try done. iApply lft_intersect_mono. iApply lft_incl_refl. done.
Qed.
+ Global Instance refmut_wf α ty `{!TyWf ty} : TyWf (refmut α ty) :=
+ { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+
Global Instance refmut_type_contractive α : TypeContractive (refmut α).
Proof. solve_type_proper. Qed.
Global Instance refmut_ne α : NonExpansive (refmut α).
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index af9e25be..e2649e7c 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -18,10 +18,9 @@ Section refmut_functions.
letalloc: "r" <- "r'" in
delete [ #1; "x"];; return: ["r"].
- Lemma refmut_deref_type ty :
- typed_val refmut_deref
- (fn (fun '(α, β) => FP (λ Ï, [Ï âŠ‘ α; α ⊑ β]%EL)
- [# &shr{α}(refmut β ty)]%T (&shr{α}ty))).
+ Lemma refmut_deref_type ty `{!TyWf ty} :
+ typed_val refmut_deref (fn (fun '(α, β) =>
+ FP_wf ∅ [# &shr{α}(refmut β ty)]%T (&shr{α}ty))).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] Ï ret arg). inv_vec arg=>x. simpl_subst.
@@ -43,11 +42,12 @@ Section refmut_functions.
iDestruct ("Hcloseβα2" with "Hα2β") as "[Hβ Hα2]".
iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1".
iMod ("Hclose''" with "Hβ HL") as "HL". iMod ("Hclose'" with "[$] HL") as "HL".
+ iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
iApply (type_type _ _ _ [ x ◠box (&shr{α} refmut β ty); #lv ◠&shr{α}ty]%TC
with "[] LFT HE Hna HL Hk"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
iFrame. iApply (ty_shr_mono with "[] Hshr'").
- iApply lft_incl_glb; last iApply lft_incl_refl. iDestruct "HE" as "(_ & $ & _)". }
+ by iApply lft_incl_glb; last iApply lft_incl_refl. }
iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
@@ -61,10 +61,9 @@ Section refmut_functions.
letalloc: "r" <- "r'" in
delete [ #1; "x"];; return: ["r"].
- Lemma refmut_derefmut_type ty :
- typed_val refmut_derefmut
- (fn (fun '(α, β) => FP (λ Ï, [Ï âŠ‘ α; α ⊑ β]%EL) [# &uniq{α}(refmut β ty)]%T
- (&uniq{α}ty)%T)).
+ Lemma refmut_derefmut_type ty `{!TyWf ty} :
+ typed_val refmut_derefmut (fn (fun '(α, β) =>
+ FP_wf ∅ [# &uniq{α}(refmut β ty)]%T (&uniq{α}ty)%T)).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] Ï ret arg). inv_vec arg=>x. simpl_subst.
@@ -96,12 +95,12 @@ Section refmut_functions.
[done| |by iApply (bor_unnest with "LFT Hb")|]; first done.
wp_read. iIntros "Hb !>". wp_let.
iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]". iMod ("Hclose'" with "Hα HL") as "HL".
+ iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
iApply (type_type _ _ _ [ x ◠box (uninit 1); #lv ◠&uniq{α}ty]%TC
with "[] LFT HE Hna HL Hk"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
iFrame. iApply (bor_shorten with "[] Hb").
- iApply lft_incl_glb; [iApply lft_incl_glb|iApply lft_incl_refl]; last done.
- iDestruct "HE" as "(_ & $ & _)". }
+ by iApply lft_incl_glb; [iApply lft_incl_glb|iApply lft_incl_refl]. }
iApply (type_letalloc_1 (&uniq{α}ty)); [solve_typing..|].
iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
@@ -116,8 +115,8 @@ Section refmut_functions.
delete [ #2; "x"];;
let: "r" := new [ #0] in return: ["r"].
- Lemma refmut_drop_type ty :
- typed_val refmut_drop (fn(∀ α, (λ Ï, [Ï âŠ‘ α]); refmut α ty) → unit).
+ Lemma refmut_drop_type ty `{!TyWf ty} :
+ typed_val refmut_drop (fn(∀ α, ∅; refmut α ty) → unit).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
@@ -159,69 +158,74 @@ Section refmut_functions.
(* Apply a function within the refmut, typically for accessing a component. *)
Definition refmut_map : val :=
funrec: <> ["ref"; "f"; "env"] :=
- withcont: "k":
- let: "x'" := !"ref" in
let: "f'" := !"f" in
+ Newlft;;
+ let: "x'" := !"ref" in
letalloc: "x" <- "x'" in
letcall: "r" := "f'" ["env"; "x"]%E in
- let: "r'" := !"r" in
+ let: "r'" := !"r" in delete [ #1; "r"];;
+ Endlft;;
"ref" <- "r'";;
- delete [ #1; "f"];; "k" []
- cont: "k" [] :=
- return: ["ref"].
+ delete [ #1; "f"];; return: ["ref"].
- Lemma refmut_map_type ty1 ty2 envty E :
+ Lemma refmut_map_type ty1 ty2 envty `{!TyWf ty1, !TyWf ty2, !TyWf envty} :
typed_val refmut_map
- (fn(∀ β, [β]%EL ++ E; refmut β ty1,
- fn(∀ α, [α]%EL ++ E; envty, &uniq{α} ty1) → &uniq{α} ty2,
- envty)
+ (fn(∀ β, ∅; refmut β ty1,
+ fn(∀ α, ∅; envty, &uniq{α} ty1) → &uniq{α} ty2, envty)
→ refmut β ty2).
Proof.
- intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
- iIntros (α ret arg). inv_vec arg=>ref f env. simpl_subst.
- iIntros (tid qE) "#LFT Hna HE HL Hk HT".
- rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
- iDestruct "HT" as "(Href & Hf & Henv)".
- destruct ref as [[|lref|]|]; try done. iDestruct "Href" as "[Href Href†]".
+ intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α Ï ret arg).
+ inv_vec arg=>ref f env. simpl_subst.
+ iApply type_deref; [solve_typing..|]. iIntros (f'). simpl_subst.
+ iApply (type_newlft [Ï]). iIntros (κ tid) "#LFT #HE Hna HL Hk (Hf & #Hf' & Href & Henv)".
+ rewrite (tctx_hasty_val _ ref). destruct ref as [[|lref|]|]; try done.
+ iDestruct "Href" as "[Href Href†]".
iDestruct "Href" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Href";
try iDestruct "Href" as "[_ >[]]".
rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
iDestruct "Href" as (ν γ β ty') "(Hbor & #Hαβ & #Hinv & >Hν & Hγ)".
- rewrite -(freeable_sz_split _ 1 1). iDestruct "Href†" as "[Href†1 Href†2]".
- destruct (Qp_lower_bound qE 1) as (q & qE' & qν' & -> & EQ1).
- rewrite [in (_).[ν]%I] EQ1.
- iDestruct (@fractional_split with "HE") as "[[Hα HE] HE']".
- iDestruct "Hν" as "[Hν Hν']".
- remember (RecV "k" [] (ret [ LitV lref])%E)%V as k eqn:EQk.
- iApply (wp_let' _ _ _ _ k). { subst. solve_to_val. } simpl_subst.
- iApply (type_type ((α ⊓ ν) :: E)%EL []
- [k â—cont([], λ _:vec val 0, [ #lref â— own_ptr 2 (&uniq{α ⊓ ν}ty2)])]%CC
- [ f ◠box (fn(∀ α, [α]%EL ++ E; envty, &uniq{α}ty1) → &uniq{α}ty2);
- #lref ◠own_ptr 2 (&uniq{α ⊓ ν}ty1); env ◠box envty ]%TC
- with "[] LFT Hna [$HE Hα Hν] HL [Hk HE' Hν' Href↦2 Hγ Href†2]"); first last.
- { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
- iFrame. iApply tctx_hasty_val'. done. iFrame. iExists [_].
- rewrite heap_mapsto_vec_singleton. by iFrame. }
- { rewrite !cctx_interp_singleton /=. iIntros "HE". iIntros (args) "Hna HL HT".
- inv_vec args. subst. simpl. wp_rec. iDestruct "HE" as "[Hαν HE]".
- iDestruct (lft_tok_sep with "Hαν") as "[Hα Hν]".
- iSpecialize ("Hk" with "[$HE' $Hα $HE]").
- iApply ("Hk" $! [# #lref] with "Hna HL").
- rewrite !tctx_interp_singleton !tctx_hasty_val' //.
- iDestruct "HT" as "[Href Ḥref†2]".
- rewrite /= -(freeable_sz_split _ 1 1). iFrame.
- iDestruct "Href" as ([|[[|lv'|]|] [|]]) "[H↦ Href]"; auto.
- iExists [ #lv'; #lrc].
- rewrite (heap_mapsto_vec_cons _ _ _ [_]) !heap_mapsto_vec_singleton. iFrame.
- iExists ν. rewrite /= EQ1. eauto 20 with iFrame. }
- { rewrite /= -lft_tok_sep. iFrame. }
- iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
- iApply type_deref; [solve_typing..|]. iIntros (f'). simpl_subst.
- iApply type_letalloc_1; [solve_typing..|]. iIntros (x). simpl_subst.
- iApply (type_letcall); [simpl; solve_typing..|]. iIntros (r). simpl_subst.
- iApply type_deref; [solve_typing..|]. iIntros (r'). simpl_subst.
- iApply type_assign; [solve_typing..|].
+ wp_read. wp_let. wp_apply wp_new; first done.
+ iIntros (lx [|? []]) "(% & H†& Hlx)"; try (simpl in *; lia).
+ rewrite heap_mapsto_vec_singleton. wp_let. wp_write.
+ match goal with | |- context [(WP (_ [?k']) {{_, _}})%I] =>
+ assert (∃ k, to_val k' = Some k) as [k EQk] by (eexists; solve_to_val) end.
+ iApply (wp_let' _ _ _ _ k _ EQk). simpl_subst. iNext.
+ iDestruct (lctx_lft_incl_incl κ α with "HL HE") as "#Hκα"; [solve_typing..|].
+ iMod (bor_create _ κ (1).[ν] with "LFT [$Hν]") as "[Hb Hν]"; first done.
+ iAssert (κ ⊑ α ⊓ ν)%I with "[>Hb]" as "#Hκν".
+ { iApply (lft_incl_glb with "Hκα"). iApply (frac_bor_lft_incl with "LFT").
+ iApply (bor_fracture with "LFT [> -]"); first done. rewrite /= Qp_mult_1_r //. }
+ iApply (type_type ((κ ⊑ α ⊓ ν) :: (α ⊓ ν ⊑ α) :: _)%EL _
+ [k â—cont(_, λ x:vec val 1, [ x!!!0 â— box (&uniq{α ⊓ ν}ty2)])]%CC
+ [ f' ◠fn(∀ α, ∅; envty, &uniq{α}ty1) → &uniq{α}ty2;
+ #lx ◠box (&uniq{α ⊓ ν}ty1); env ◠box envty ]%TC
+ with "[] LFT [] Hna HL [-H†Hlx Henv Hbor]"); swap 1 2; swap 3 4.
+ { iSplitL; last iSplitL; [done|iApply lft_intersect_incl_l|iApply "HE"]. }
+ { iApply (type_call (α ⊓ ν)); solve_typing. }
+ { iFrame "∗#". iApply tctx_hasty_val'; first done. rewrite -freeable_sz_full.
+ iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. auto with iFrame. }
+ iIntros (? ->%elem_of_list_singleton arg) "Hna HL Hr". inv_vec arg=>r.
+ apply of_to_val in EQk. rewrite EQk. iApply wp_rec; try (done || apply _).
+ { repeat econstructor. by rewrite to_of_val. } simpl_subst.
+ rewrite /tctx_interp big_sepL_singleton (tctx_hasty_val _ r) ownptr_own.
+ iDestruct "Hr" as (lr vr) "(% & Hlr & Hvr & H†)". subst. inv_vec vr=>r'. iNext.
+ rewrite heap_mapsto_vec_singleton. wp_read. wp_let.
+ wp_apply (wp_delete _ _ _ [_] with "[Hlr H†]"). done.
+ { rewrite heap_mapsto_vec_singleton freeable_sz_full. iFrame. }
+ iIntros "_". wp_seq. wp_bind Endlft. iDestruct "HL" as "[Hκ HL]".
+ iDestruct "Hκ" as (κ') "(% & Hκ' & #Hκ'†)". simpl in *. subst κ.
+ iSpecialize ("Hκ'†" with "Hκ'").
+ iApply wp_mask_mono; last iApply (wp_step_fupd with "Hκ'†"); auto with ndisj.
+ wp_seq. iIntros "Hκ'†!>". iMod ("Hν" with "[Hκ'†]") as "Hν";
+ first by rewrite -lft_dead_or; auto. wp_seq. wp_write.
+ iApply (type_type _ _ _
+ [ f ◠box (fn(∀ α, ∅; envty, &uniq{α}ty1) → &uniq{α}ty2);
+ #lref ◠box (refmut α ty2) ]%TC
+ with "[] LFT HE Hna HL Hk"); first last.
+ { iFrame. rewrite big_sepL_singleton tctx_hasty_val. iExists _. iSplit. done.
+ iFrame. iExists [_;_]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+ iFrame. destruct r' as [[]|]=>//=. auto 10 with iFrame. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index fe5b772d..db17b3e5 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -149,6 +149,9 @@ Section rwlock.
iExists _, _. iFrame. iApply lft_incl_trans; auto.
Qed.
+ Global Instance join_handle_wf ty `{!TyWf ty} : TyWf (rwlock ty) :=
+ { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
Global Instance rwlock_type_ne : TypeNonExpansive rwlock.
Proof.
constructor;
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 408778d9..1298abb5 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -19,8 +19,8 @@ Section rwlock_functions.
"r" +â‚— #1 <-{ty.(ty_size)} !"x";;
delete [ #ty.(ty_size) ; "x"];; return: ["r"].
- Lemma rwlock_new_type ty :
- typed_val (rwlock_new ty) (fn(λ Ï, []; ty) → rwlock ty).
+ Lemma rwlock_new_type ty `{!TyWf ty} :
+ typed_val (rwlock_new ty) (fn(∅; ty) → rwlock ty).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (_ ret Ï arg). inv_vec arg=>x. simpl_subst.
@@ -55,8 +55,8 @@ Section rwlock_functions.
"r" <-{ty.(ty_size)} !("x" +â‚— #1);;
delete [ #(S ty.(ty_size)) ; "x"];; return: ["r"].
- Lemma rwlock_into_inner_type ty :
- typed_val (rwlock_into_inner ty) (fn(λ Ï, [] ; rwlock ty) → ty).
+ Lemma rwlock_into_inner_type ty `{!TyWf ty} :
+ typed_val (rwlock_into_inner ty) (fn(∅; rwlock ty) → ty).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (_ ret Ï arg). inv_vec arg=>x. simpl_subst.
@@ -89,8 +89,8 @@ Section rwlock_functions.
"x" <- "x'" +â‚— #1;;
return: ["x"].
- Lemma rwlock_get_mut_type ty :
- typed_val rwlock_get_mut (fn(∀ α, λ Ï, [Ï âŠ‘ α]; &uniq{α} (rwlock ty)) → &uniq{α} ty).
+ Lemma rwlock_get_mut_type ty `{!TyWf ty} :
+ typed_val rwlock_get_mut (fn(∀ α, ∅; &uniq{α} (rwlock ty)) → &uniq{α} ty).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
@@ -139,9 +139,9 @@ Section rwlock_functions.
cont: "k" [] :=
delete [ #1; "x"];; return: ["r"].
- Lemma rwlock_try_read_type ty :
+ Lemma rwlock_try_read_type ty `{!TyWf ty} :
typed_val rwlock_try_read
- (fn(∀ α, λ Ï, [Ï âŠ‘ α]; &shr{α}(rwlock ty)) → option (rwlockreadguard α ty)).
+ (fn(∀ α, ∅; &shr{α}(rwlock ty)) → option (rwlockreadguard α ty)).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
@@ -254,9 +254,9 @@ Section rwlock_functions.
cont: "k" ["r"] :=
delete [ #1; "x"];; return: ["r"].
- Lemma rwlock_try_write_type ty :
+ Lemma rwlock_try_write_type ty `{!TyWf ty} :
typed_val rwlock_try_write
- (fn(∀ α, λ Ï, [Ï âŠ‘ α]; &shr{α}(rwlock ty)) → option (rwlockwriteguard α ty)).
+ (fn(∀ α, ∅; &shr{α}(rwlock ty)) → option (rwlockwriteguard α ty)).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index e023b7a3..3f44a88e 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -61,6 +61,9 @@ Section rwlockreadguard.
iApply lft_incl_refl.
Qed.
+ Global Instance rwlockreadguard_wf α ty `{!TyWf ty} : TyWf (rwlockreadguard α ty) :=
+ { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+
Global Instance rwlockreadguard_type_contractive α : TypeContractive (rwlockreadguard α).
Proof.
constructor;
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 4fb1418b..e53896fc 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -18,10 +18,9 @@ Section rwlockreadguard_functions.
letalloc: "r" <- "r'" in
delete [ #1; "x"];; return: ["r"].
- Lemma rwlockreadguard_deref_type ty :
+ Lemma rwlockreadguard_deref_type ty `{!TyWf ty} :
typed_val rwlockreadguard_deref
- (fn (fun '(α, β) => FP (λ Ï, [Ï âŠ‘ α; α ⊑ β]%EL)
- [# &shr{α}(rwlockreadguard β ty)] (&shr{α}ty))).
+ (fn (fun '(α, β) => FP_wf ∅ [# &shr{α}(rwlockreadguard β ty)] (&shr{α}ty))).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] Ï ret arg). inv_vec arg=>x. simpl_subst.
@@ -34,12 +33,13 @@ Section rwlockreadguard_functions.
iMod (frac_bor_acc with "LFT Hfrac Hα") as (qlx') "[H↦ Hcloseα]". done.
rewrite heap_mapsto_vec_singleton. wp_read. wp_op. wp_let.
iMod ("Hcloseα" with "[$H↦]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
+ iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
iApply (type_type _ _ _ [ x ◠box (&shr{α} rwlockreadguard β ty);
#(shift_loc l' 1) ◠&shr{α}ty]%TC
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
- iFrame. iApply (ty_shr_mono with "[] Hshr"). iApply lft_incl_glb.
- by iDestruct "HE" as "(_ & $ & _)". by iApply lft_incl_refl. }
+ iFrame. iApply (ty_shr_mono with "[] Hshr"). iApply lft_incl_glb; first done.
+ by iApply lft_incl_refl. }
iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
@@ -58,9 +58,8 @@ Section rwlockreadguard_functions.
let: "r" := new [ #0] in return: ["r"]
else "loop" [].
- Lemma rwlockreadguard_drop_type ty :
- typed_val rwlockreadguard_drop
- (fn(∀ α, λ Ï, [Ï âŠ‘ α]; rwlockreadguard α ty) → unit).
+ Lemma rwlockreadguard_drop_type ty `{!TyWf ty} :
+ typed_val rwlockreadguard_drop (fn(∀ α, ∅; rwlockreadguard α ty) → unit).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index b71f6c76..7003099d 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -61,6 +61,9 @@ Section rwlockwriteguard.
iApply ty_shr_mono; try done. iApply lft_intersect_mono. iApply lft_incl_refl. done.
Qed.
+ Global Instance rwlockwriteguard_wf α ty `{!TyWf ty} : TyWf (rwlockwriteguard α ty) :=
+ { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+
Global Instance rwlockwriteguard_type_contractive α : TypeContractive (rwlockwriteguard α).
Proof.
constructor;
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index ba11a3a3..7ccd5321 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -18,10 +18,9 @@ Section rwlockwriteguard_functions.
letalloc: "r" <- "r'" in
delete [ #1; "x"];; return: ["r"].
- Lemma rwlockwriteguard_deref_type ty :
+ Lemma rwlockwriteguard_deref_type ty `{!TyWf ty} :
typed_val rwlockwriteguard_deref
- (fn (fun '(α, β) => FP (λ Ï, [Ï âŠ‘ α; α ⊑ β]%EL)
- [# &shr{α}(rwlockwriteguard β ty)] (&shr{α}ty))).
+ (fn (fun '(α, β) => FP_wf ∅ [# &shr{α}(rwlockwriteguard β ty)] (&shr{α}ty))).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] Ï ret arg). inv_vec arg=>x. simpl_subst.
@@ -43,12 +42,13 @@ Section rwlockwriteguard_functions.
iDestruct ("Hcloseβα2" with "Hα2β") as "[Hβ Hα2]".
iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1". iMod ("Hclose'" with "Hβ HL") as "HL".
iMod ("Hclose" with "[$] HL") as "HL".
+ iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
iApply (type_type _ _ _ [ x ◠box (&shr{α} rwlockwriteguard β ty);
#(shift_loc l' 1) ◠&shr{α}ty]%TC
with "[] LFT HE Hna HL Hk"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
- iFrame. iApply (ty_shr_mono with "[] Hshr'"). iApply lft_incl_glb.
- by iDestruct "HE" as "(_ & $ & _)". by iApply lft_incl_refl. }
+ iFrame. iApply (ty_shr_mono with "[] Hshr'"). iApply lft_incl_glb; first done.
+ by iApply lft_incl_refl. }
iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
@@ -62,10 +62,9 @@ Section rwlockwriteguard_functions.
letalloc: "r" <- "r'" in
delete [ #1; "x"];; return: ["r"].
- Lemma rwlockwriteguard_derefmut_type ty :
+ Lemma rwlockwriteguard_derefmut_type ty `{!TyWf ty} :
typed_val rwlockwriteguard_derefmut
- (fn (fun '(α, β) => FP (λ Ï, [Ï âŠ‘ α; α ⊑ β]%EL)
- [# &uniq{α}(rwlockwriteguard β ty)] (&uniq{α}ty))).
+ (fn (fun '(α, β) => FP_wf ∅ [# &uniq{α}(rwlockwriteguard β ty)] (&uniq{α}ty))).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] Ï ret arg). inv_vec arg=>x. simpl_subst.
@@ -89,12 +88,12 @@ Section rwlockwriteguard_functions.
[done| |by iApply (bor_unnest with "LFT Hb")|]; first done.
wp_read. iIntros "Hb !>". wp_op. wp_let.
iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]". iMod ("Hclose" with "Hα HL") as "HL".
+ iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
iApply (type_type _ _ _ [ x ◠box (uninit 1); #(shift_loc l 1) ◠&uniq{α}ty]%TC
with "[] LFT HE Hna HL Hk"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
iFrame. iApply (bor_shorten with "[] Hb"). iApply lft_incl_glb.
- by iApply lft_incl_trans; first iDestruct "HE" as "(_ & $ & _)".
- by iApply lft_incl_refl. }
+ by iApply lft_incl_trans. by iApply lft_incl_refl. }
iApply (type_letalloc_1 (&uniq{α}ty)); [solve_typing..|].
iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
@@ -108,9 +107,9 @@ Section rwlockwriteguard_functions.
delete [ #1; "x"];;
let: "r" := new [ #0] in return: ["r"].
- Lemma rwlockwriteguard_drop_type ty :
+ Lemma rwlockwriteguard_drop_type ty `{!TyWf ty} :
typed_val rwlockwriteguard_drop
- (fn(∀ α, λ Ï, [Ï âŠ‘ α]; rwlockwriteguard α ty) → unit).
+ (fn(∀ α, ∅; rwlockwriteguard α ty) → unit).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
@@ -120,7 +119,8 @@ Section rwlockwriteguard_functions.
iDestruct "HT" as "[Hx Hx']".
destruct x' as [[|lx'|]|]; try done. simpl.
iDestruct "Hx'" as (γ β) "(Hx' & #Hαβ & #Hinv & H◯)".
- iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
+ iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)";
+ [solve_typing..|].
iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
wp_bind (#lx' <-ˢᶜ #0)%E.
iMod (shr_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|].
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index fcaa8747..d2a67fab 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -26,6 +26,9 @@ Section join_handle.
Next Obligation. iIntros "* _ _ _ $". auto. Qed.
Next Obligation. iIntros (?) "**"; auto. Qed.
+ Global Instance join_handle_wf ty `{!TyWf ty} : TyWf (join_handle ty) :=
+ { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
Lemma join_handle_subtype ty1 ty2 :
▷ type_incl ty1 ty2 -∗ type_incl (join_handle ty1) (join_handle ty2).
Proof.
@@ -67,8 +70,10 @@ Section spawn.
letalloc: "r" <- "join" in
delete [ #1; "f"];; return: ["r"].
- Lemma spawn_type `(!Send envty, !Send retty) :
- typed_val spawn (fn(λ _, []; fn(λ _, [] ; envty) → retty, envty) → join_handle retty).
+ Lemma spawn_type envty retty `{!TyWf envty, !TyWf retty}
+ `(!Send envty, !Send retty) :
+ let E Ï := envty.(ty_outlives_E) static ++ retty.(ty_outlives_E) static in
+ typed_val spawn (fn(E; fn(∅; envty) → retty, envty) → join_handle retty).
Proof. (* FIXME: typed_instruction_ty is not used for printing. *)
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (_ Ï ret arg). inv_vec arg=>f env. simpl_subst.
@@ -84,13 +89,13 @@ Section spawn.
iIntros "?". iExists retty. iFrame. iApply type_incl_refl. }
iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let.
(* FIXME this is horrible. *)
- assert (Hcall := type_call' [] [] [] f' [] [env:expr] (λ _:(), FP (λ _, []) [# envty] retty)).
+ refine (let Hcall := type_call' _ [] [] f' [] [env:expr]
+ (λ _:(), FP_wf ∅ [# envty] retty) in _).
specialize (Hcall (rec: "_k" ["r"] := finish [ #c; "r"])%V ()).
erewrite of_val_unlock in Hcall; last done.
- iApply (Hcall with "LFT [] Htl [] [Hfin]").
+ iApply (Hcall with "LFT HE Htl [] [Hfin]").
- constructor.
- - intros. apply elctx_sat_nil.
- - rewrite /elctx_interp big_sepL_nil. done.
+ - solve_typing.
- rewrite /llctx_interp big_sepL_nil. done.
- rewrite /cctx_interp. iIntros "* Hin".
iDestruct "Hin" as %Hin%elem_of_list_singleton. subst x.
@@ -98,9 +103,8 @@ Section spawn.
wp_rec. iApply (finish_spec with "[$Hfin Hret]"); last auto.
rewrite tctx_interp_singleton tctx_hasty_val. by iApply @send_change_tid.
- rewrite tctx_interp_cons tctx_interp_singleton. iSplitL "Hf'".
- + rewrite !tctx_hasty_val.
- iApply @send_change_tid. done.
- + rewrite !tctx_hasty_val. iApply @send_change_tid. done. }
+ + rewrite !tctx_hasty_val. by iApply @send_change_tid.
+ + rewrite !tctx_hasty_val. by iApply @send_change_tid. }
iIntros (v). simpl_subst.
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_assign; [solve_typing..|].
@@ -114,8 +118,8 @@ Section spawn.
let: "r" := join ["c'"] in
delete [ #1; "c"];; return: ["r"].
- Lemma join_type retty :
- typed_val join (fn(λ _, []; join_handle retty) → retty).
+ Lemma join_type retty `{!TyWf retty} :
+ typed_val join (fn(∅; join_handle retty) → retty).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (_ Ï ret arg). inv_vec arg=>c. simpl_subst.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 76a252ae..1fee0f12 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -63,8 +63,8 @@ Section own.
end%I;
ty_shr κ tid l :=
(∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
- □ (∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ] ={F,F∖↑shrN}▷=∗ ty.(ty_shr) κ tid l' ∗ q.[κ]))%I
- |}.
+ □ (∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ] ={F,F∖↑shrN}▷=∗
+ ty.(ty_shr) κ tid l' ∗ q.[κ]))%I |}.
Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H". Qed.
Next Obligation.
move=>n ty N κ l tid ?? /=. iIntros "#LFT Hshr Htok".
@@ -88,6 +88,9 @@ Section own.
by iApply (ty.(ty_shr_mono) with "Hκ").
Qed.
+ Global Instance own_ptr_wf n ty `{!TyWf ty} : TyWf (own_ptr n ty) :=
+ { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
Lemma own_type_incl n m ty1 ty2 :
▷ ⌜n = m⌠-∗ ▷ type_incl ty1 ty2 -∗ type_incl (own_ptr n ty1) (own_ptr m ty2).
Proof.
@@ -186,7 +189,8 @@ Section util.
Lemma ownptr_own n ty tid v :
(own_ptr n ty).(ty_own) tid [v] ⊣⊢
- ∃ (l : loc) (vl : vec val ty.(ty_size)), ⌜v = #l⌠∗ ▷ l ↦∗ vl ∗ ▷ ty.(ty_own) tid vl ∗ ▷ freeable_sz n ty.(ty_size) l.
+ ∃ (l : loc) (vl : vec val ty.(ty_size)),
+ ⌜v = #l⌠∗ ▷ l ↦∗ vl ∗ ▷ ty.(ty_own) tid vl ∗ ▷ freeable_sz n ty.(ty_size) l.
Proof.
iSplit.
- iIntros "Hown". destruct v as [[|l|]|]; try done.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 50c7427b..a51abc53 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -148,6 +148,9 @@ Section product.
Definition product := foldr product2 unit0.
Definition unit := product [].
+ Global Instance product_wf tyl `{!TyWfLst tyl} : TyWf (product tyl) :=
+ { ty_lfts := tyl.(tyl_lfts); ty_wf_E := tyl.(tyl_wf_E) }.
+
Global Instance product_type_ne n: Proper (Forall2 (type_dist2 n) ==> type_dist2 n) product.
Proof. intros ??. induction 1=>//=. by f_equiv. Qed.
Global Instance product_ne : NonExpansive product.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 311dad58..a7cad9b8 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -16,6 +16,9 @@ Section shr_bor.
Next Obligation. by iIntros (κ ty tid [|[[]|][]]) "H". Qed.
Next Obligation. intros κ ty tid [|[[]|][]]; apply _. Qed.
+ Global Instance shr_bor_wf κ ty `{!TyWf ty} : TyWf (shr_bor κ ty) :=
+ { ty_lfts := [κ]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) κ }.
+
Global Instance shr_mono E L :
Proper (flip (lctx_lft_incl E L) ==> subtype E L ==> subtype E L) shr_bor.
Proof.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 38166586..42ba0dbb 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -23,7 +23,7 @@ Proof. solve_inG. Qed.
Section type_soundness.
Definition exit_cont : val := λ: [<>], #().
- Definition main_type `{typeG Σ} := (fn(λ Ï, []) → unit)%T.
+ Definition main_type `{typeG Σ} := (fn(∅) → unit)%T.
Theorem type_soundness `{typePreG Σ} (main : val) σ t :
(∀ `{typeG Σ}, typed_val main main_type) →
@@ -53,7 +53,7 @@ Section type_soundness.
iMod (lft_create with "LFT") as (Ï) "HÏ". done.
iApply ("Hmain" $! () Ï exit_cont [#] tid with "LFT [] Htl [HÏ] []");
last by rewrite tctx_interp_nil.
- { by rewrite /elctx_interp /=. }
+ { by rewrite /elctx_interp /= big_sepL_nil. }
{ rewrite /llctx_interp big_sepL_singleton. iExists Ï. iFrame. by rewrite /= left_id. }
rewrite cctx_interp_singleton. simpl. iIntros (args) "_ _".
inv_vec args. iIntros (x) "_ /=". by wp_lam.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index e48d0aea..45048331 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -20,6 +20,8 @@ Section sum.
Qed.
Next Obligation. iIntros (κ κ' tid l) "#Hord []". Qed.
+ Global Instance emp_wf : TyWf emp := { ty_lfts := []; ty_wf_E := [] }.
+
Global Instance emp_empty : Empty type := emp.
Global Instance emp_copy : Copy ∅.
@@ -92,6 +94,9 @@ Section sum.
- iApply ((nth i tyl ∅).(ty_shr_mono) with "Hord"); done.
Qed.
+ Global Instance sum_wf tyl `{!TyWfLst tyl} : TyWf (sum tyl) :=
+ { ty_lfts := tyl.(tyl_lfts); ty_wf_E := tyl.(tyl_wf_E) }.
+
Global Instance sum_type_ne n : Proper (Forall2 (type_dist2 n) ==> type_dist2 n) sum.
Proof.
intros x y EQ.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index b0ad75ff..401392ae 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -53,6 +53,61 @@ Instance: Params (@ty_shr) 2.
Arguments ty_own {_ _} _ _ !_ /.
+Class TyWf `{typeG Σ} (ty : type) := { ty_lfts : list lft; ty_wf_E : elctx }.
+Arguments ty_lfts {_ _} _ {_}.
+Arguments ty_wf_E {_ _} _ {_}.
+
+Definition ty_outlives_E `{typeG Σ} ty `{!TyWf ty} (κ : lft) : elctx :=
+ (λ α, κ ⊑ α)%EL <$> ty.(ty_lfts).
+
+Lemma ty_outlives_E_elctx_sat `{typeG Σ} E L ty `{!TyWf ty} α β :
+ ty.(ty_outlives_E) β ⊆+ E →
+ lctx_lft_incl E L α β →
+ elctx_sat E L (ty.(ty_outlives_E) α).
+Proof.
+ unfold ty_outlives_E. induction ty.(ty_lfts) as [|κ l IH]=>/= Hsub Hαβ.
+ - solve_typing.
+ - apply elctx_sat_lft_incl.
+ + etrans; first done. eapply lctx_lft_incl_external, elem_of_submseteq, Hsub.
+ set_solver.
+ + apply IH, Hαβ. etrans; last done. by apply submseteq_cons.
+Qed.
+
+Inductive TyWfLst `{typeG Σ} : list type → Type :=
+| tyl_wf_nil : TyWfLst []
+| tyl_wf_cons ty tyl `{!TyWf ty, !TyWfLst tyl} : TyWfLst (ty::tyl).
+Existing Class TyWfLst.
+Existing Instances tyl_wf_nil tyl_wf_cons.
+
+Fixpoint tyl_lfts `{typeG Σ} tyl {WF : TyWfLst tyl} : list lft :=
+ match WF with
+ | tyl_wf_nil => []
+ | tyl_wf_cons ty tyl _ _ => ty.(ty_lfts) ++ tyl.(tyl_lfts)
+ end.
+
+Fixpoint tyl_wf_E `{typeG Σ} tyl {WF : TyWfLst tyl} : elctx :=
+ match WF with
+ | tyl_wf_nil => []
+ | tyl_wf_cons ty tyl _ _ => ty.(ty_wf_E) ++ tyl.(tyl_wf_E)
+ end.
+
+Fixpoint tyl_outlives_E `{typeG Σ} tyl {WF : TyWfLst tyl} (κ : lft) : elctx :=
+ match WF with
+ | tyl_wf_nil => []
+ | tyl_wf_cons ty tyl _ _ => ty.(ty_outlives_E) κ ++ tyl.(tyl_outlives_E) κ
+ end.
+
+Lemma tyl_outlives_E_elctx_sat `{typeG Σ} E L tyl {WF : TyWfLst tyl} α β :
+ tyl.(tyl_outlives_E) β ⊆+ E →
+ lctx_lft_incl E L α β →
+ elctx_sat E L (tyl.(tyl_outlives_E) α).
+Proof.
+ induction WF as [|???? IH]=>/=.
+ - solve_typing.
+ - intros. apply elctx_sat_app, IH; [eapply ty_outlives_E_elctx_sat| |]=>//;
+ (etrans; [|done]); solve_typing.
+Qed.
+
Record simple_type `{typeG Σ} :=
{ st_own : thread_id → list val → iProp Σ;
st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = 1%natâŒ;
@@ -194,8 +249,7 @@ Section ofe.
Global Instance ty_of_st_ne : NonExpansive ty_of_st.
Proof.
- intros n ?? EQ. constructor. done. simpl.
- - intros tid l. apply EQ.
+ intros n ?? EQ. constructor; try apply EQ. done.
- simpl. intros; repeat f_equiv. apply EQ.
Qed.
Global Instance ty_of_st_proper : Proper ((≡) ==> (≡)) ty_of_st.
@@ -515,8 +569,8 @@ Section subtyping.
iClear "∗". iIntros "!# #HE".
iApply (type_incl_trans with "[#]"). by iApply "H12". by iApply "H23".
Qed.
-
- Lemma subtype_Forall2_llctx E L tys1 tys2 qL :
+
+ Lemma subtype_Forall2_llctx E L tys1 tys2 qL :
Forall2 (subtype E L) tys1 tys2 →
llctx_interp L qL -∗ □ (elctx_interp E -∗
[∗ list] tys ∈ (zip tys1 tys2), type_incl (tys.1) (tys.2)).
@@ -584,7 +638,7 @@ Section subtyping.
Qed.
Lemma subtype_simple_type E L (st1 st2 : simple_type) :
- (∀ qL, llctx_interp L qL -∗ □ (elctx_interp E -∗
+ (∀ qL, llctx_interp L qL -∗ □ (elctx_interp E -∗
∀ tid vl, st1.(st_own) tid vl -∗ st2.(st_own) tid vl)) →
subtype E L st1 st2.
Proof.
@@ -608,7 +662,7 @@ End subtyping.
Section type_util.
Context `{typeG Σ}.
-
+
Lemma heap_mapsto_ty_own l ty tid :
l ↦∗: ty_own ty tid ⊣⊢ ∃ (vl : vec val ty.(ty_size)), l ↦∗ vl ∗ ty_own ty tid vl.
Proof.
@@ -621,5 +675,6 @@ Section type_util.
End type_util.
+Hint Resolve ty_outlives_E_elctx_sat tyl_outlives_E_elctx_sat : lrust_typing.
Hint Resolve subtype_refl eqtype_refl : lrust_typing.
Hint Opaque subtype eqtype : lrust_typing.
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index 294fb372..b8852230 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -17,7 +17,7 @@ Section uninit.
Î (replicate n uninit_1).
Lemma uninit0_sz n : ty_size (uninit0 n) = n.
- Proof. induction n. done. simpl. by f_equal. Qed.
+ Proof. induction n=>//=. by f_equal. Qed.
(* We redefine uninit as an alias of uninit0, so that the size
computes directly to [n] *)
@@ -28,6 +28,9 @@ Section uninit.
Next Obligation. intros. by apply ty_share. Qed.
Next Obligation. intros. by apply ty_shr_mono. Qed.
+ Global Instance uninit_wf n : TyWf (uninit n) :=
+ { ty_lfts := []; ty_wf_E := [] }.
+
Global Instance uninit_copy n : Copy (uninit n).
Proof.
destruct (product_copy (replicate n uninit_1)) as [A B].
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 722c74e2..e8f07a2d 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -43,6 +43,9 @@ Section uniq_bor.
by iApply (ty_shr_mono with "Hκ0").
Qed.
+ Global Instance uniq_bor_wf κ ty `{!TyWf ty} : TyWf (uniq_bor κ ty) :=
+ { ty_lfts := [κ]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) κ }.
+
Global Instance uniq_mono E L :
Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) uniq_bor.
Proof.
--
GitLab