From 9b92a3cfa989b27109b81e1c8ace85b4ef34f7e2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 4 Mar 2017 16:23:55 +0100
Subject: [PATCH] Make box a definition and prove it contractive
This also allows us to get rid of ctx_eq
---
.gitlab-ci.yml | 1 +
theories/typing/examples/lazy_lft.v | 12 +++--
theories/typing/examples/unbox.v | 3 +-
theories/typing/function.v | 14 ++---
theories/typing/option.v | 5 +-
theories/typing/own.v | 83 +++++++++++++++++++++--------
theories/typing/type.v | 34 +-----------
theories/typing/type_context.v | 7 ++-
theories/typing/unsafe/spawn.v | 7 ++-
9 files changed, 92 insertions(+), 74 deletions(-)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 48e98f8a..12d26b50 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -21,6 +21,7 @@ lrust-coq8.6:
only:
- master
- ci
+ - /^ralf/ci//
artifacts:
paths:
- build-time.txt
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index 6960ab83..33661cdc 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -29,16 +29,20 @@ Section lazy_lft.
iApply type_new; [solve_typing|]. iIntros (g). simpl_subst.
iApply type_int. iIntros (v42). simpl_subst.
iApply type_assign; [solve_typing|by eapply write_own|].
- iApply (type_assign _ (&shr{α}_)); [solve_typing..|by eapply write_own|].
- iApply type_assign; [solve_typing|by eapply write_own|].
+ (* FIXME somehow this fails nowadays if we don't give the own_ptr hints. *)
+ iApply (type_assign (own_ptr _ _) (&shr{α} _)); [solve_typing..|by eapply write_own|].
+ iApply (type_assign (own_ptr _ _)); [solve_typing|by eapply write_own|].
iApply type_deref; [solve_typing|apply: read_own_copy|done|]. iIntros (t0'). simpl_subst.
iApply type_letpath; [solve_typing|]. iIntros (dummy). simpl_subst.
iApply type_int. iIntros (v23). simpl_subst.
iApply type_assign; [solve_typing|by eapply write_own|].
- iApply (type_assign _ (&shr{α}int)); [solve_typing..|by eapply write_own|].
+ iApply (type_assign _ (&shr{α} int)); [solve_typing..|by eapply write_own|].
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_endlft; [solve_typing..|].
- iApply (type_delete (Î [&shr{_}_;&shr{_}_])%T); [solve_typing..|].
+ iApply (type_delete (Î [&shr{_}_;&shr{_}_])%T).
+ { (* FIXME how on earth has this ever worked? It's also really slow even now. *)
+ eapply tctx_extract_merge_own_prod; first done. solve_typing. }
+ { solve_typing. } { solve_typing. }
iApply type_delete; [solve_typing..|].
iApply type_delete; [solve_typing..|].
iApply (type_jump [_]); solve_typing.
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index 78a3b34b..755b290e 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -19,7 +19,8 @@ Section unbox.
iApply type_deref; [solve_typing..|by apply read_own_move|done|].
iIntros (b'); simpl_subst.
iApply type_deref_uniq_own; [solve_typing..|]. iIntros (bx); simpl_subst.
- iApply type_letalloc_1; [solve_typing..|]. iIntros (r). simpl_subst.
+ (* FIXME: For some reason, Coq prefers to type this as &shr{α}. *)
+ iApply (type_letalloc_1 (&uniq{α} _)); [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_delete; [solve_typing..|].
iApply (type_jump [_]); solve_typing.
Qed.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 6786f64e..eb1d163e 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -16,7 +16,7 @@ Section fn.
â–¡ typed_body (E x) []
[kâ—cont([], λ v : vec _ 1, [v!!!0 â— box (ty x)])]
(zip_with (TCtx_hasty ∘ of_val) xl
- ((λ ty, box ty) <$> (vec_to_list (tys x))))
+ (box <$> (vec_to_list (tys x))))
(subst_v (fb::kb::xb) (RecV fb (kb::xb) e:::k:::xl) e))%I |}.
Next Obligation.
iIntros (E tys ty tid vl) "H". iDestruct "H" as (fb kb xb e ?) "[% _]". by subst.
@@ -43,7 +43,7 @@ Section fn.
{ intros Hprop. apply Hprop, list_fmap_ne; last first.
- eapply Forall2_impl; first exact: Htys. intros.
apply dist_later_dist, type_dist2_dist_later. done.
- - intros ty1 ty2 Hty12. rewrite (ty_size_ne _ _ _ Hty12). by rewrite Hty12. }
+ - apply _. }
clear. intros n tid p i x y. rewrite list_dist_lookup=>Hxy.
specialize (Hxy i). destruct (x !! i) as [tyx|], (y !! i) as [tyy|];
inversion_clear Hxy; last done.
@@ -193,7 +193,7 @@ Section typing.
elctx_sat E L (E' x) →
typed_body E L [k â—cont(L, λ v : vec _ 1, (v!!!0 â— box (ty x)) :: T)]
((p â— fn E' tys ty) ::
- zip_with TCtx_hasty ps ((λ ty, box ty) <$> (vec_to_list (tys x))) ++
+ zip_with TCtx_hasty ps (box <$> (vec_to_list (tys x))) ++
T)
(call: p ps → k).
Proof.
@@ -236,7 +236,7 @@ Section typing.
(p ◠fn E' tys ty)%TC ∈ T →
elctx_sat E L (E' x) →
tctx_extract_ctx E L (zip_with TCtx_hasty ps
- ((λ ty, box ty) <$> vec_to_list (tys x))) T T' →
+ (box <$> vec_to_list (tys x))) T T' →
(k â—cont(L, T''))%CC ∈ C →
(∀ ret : val, tctx_incl E L ((ret ◠box (ty x))::T') (T'' [# ret])) →
typed_body E L C T (call: p ps → k).
@@ -255,7 +255,7 @@ Section typing.
(p ◠fn E' tys ty)%TC ∈ T →
elctx_sat E L (E' x) →
tctx_extract_ctx E L (zip_with TCtx_hasty ps
- ((λ ty, box ty) <$> vec_to_list (tys x))) T T' →
+ (box <$> vec_to_list (tys x))) T T' →
(∀ ret : val, typed_body E L C ((ret ◠box (ty x))::T') (subst' b ret e)) -∗
typed_body E L C T (letcall: b := p ps in e).
Proof.
@@ -293,7 +293,7 @@ Section typing.
typed_body (E' x) [] [k â—cont([], λ v : vec _ 1, [v!!!0 â— box (ty x)])]
((f â— fn E' tys ty) ::
zip_with (TCtx_hasty ∘ of_val) args
- ((λ ty, box ty) <$> vec_to_list (tys x)) ++ T)
+ (box <$> vec_to_list (tys x)) ++ T)
(subst_v (fb :: BNamed "return" :: argsb) (f ::: k ::: args) e)) -∗
typed_instruction_ty E L T ef (fn E' tys ty).
Proof.
@@ -317,7 +317,7 @@ Section typing.
□ (∀ x k (args : vec val (length argsb)),
typed_body (E' x) [] [k â—cont([], λ v : vec _ 1, [v!!!0 â— box (ty x)])]
(zip_with (TCtx_hasty ∘ of_val) args
- ((λ ty, box ty) <$> vec_to_list (tys x)) ++ T)
+ (box <$> vec_to_list (tys x)) ++ T)
(subst_v (BNamed "return" :: argsb) (k ::: args) e)) -∗
typed_instruction_ty E L T ef (fn E' tys ty).
Proof.
diff --git a/theories/typing/option.v b/theories/typing/option.v
index 7aea21c9..6c95105c 100644
--- a/theories/typing/option.v
+++ b/theories/typing/option.v
@@ -59,7 +59,10 @@ Section option.
iApply (type_jump [_]); solve_typing.
+ left. iApply type_letalloc_n; [solve_typing|by apply read_own_move|]. iIntros (r).
simpl_subst.
- iApply (type_delete (Î [uninit _;uninit _;uninit _])); [solve_typing..|].
+ iApply (type_delete (Î [uninit _;uninit _;uninit _])).
+ { (* FIXME how on earth has this ever worked? *)
+ eapply tctx_extract_merge_own_prod; first done. solve_typing. }
+ { solve_typing. } { solve_typing. }
iApply type_delete; [solve_typing..|].
iApply (type_jump [_]); solve_typing.
Qed.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 25eba634..2f8543c5 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -96,38 +96,35 @@ Section own.
by iApply (ty.(ty_shr_mono) with "Hκ").
Qed.
- Lemma own_type_incl n ty1 ty2 :
- type_incl ty1 ty2 -∗ type_incl (own_ptr n ty1) (own_ptr n ty2).
+ 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.
- iIntros "(#Hsz & #Ho & #Hs)". iSplit; first done. iSplit; iAlways.
+ iIntros "#Heq (#Hsz & #Ho & #Hs)". iSplit; first done. iSplit; iAlways.
- iIntros (?[|[[| |]|][]]) "H"; try done. simpl.
iDestruct "H" as "[Hmt H†]". iDestruct "Hmt" as (vl') "[Hmt Hown]". iNext.
iDestruct ("Ho" with "Hown") as "Hown". iDestruct ("Hsz") as %<-.
- iFrame. iExists _. iFrame.
+ iDestruct "Heq" as %->. iFrame. iExists _. iFrame.
- iIntros (???) "H". iDestruct "H" as (l') "[Hfb #Hvs]".
iExists l'. iFrame. iIntros "!#". iIntros (F' q) "% Htok".
iMod ("Hvs" with "[%] Htok") as "Hvs'". done. iModIntro. iNext.
iMod "Hvs'" as "[Hshr $]". iApply ("Hs" with "Hshr").
Qed.
- Global Instance own_mono E L :
- Proper (ctx_eq E L ==> subtype E L ==> subtype E L) own_ptr.
+ Global Instance own_mono E L n :
+ Proper (subtype E L ==> subtype E L) (own_ptr n).
Proof.
- intros n1 n2 Hn12 ty1 ty2 Hincl. iIntros.
- iDestruct (Hn12 with "[] []") as %->; [done..|].
- iApply own_type_incl. iApply Hincl; done.
+ intros ty1 ty2 Hincl. iIntros.
+ iApply own_type_incl; first by auto. iApply Hincl; auto.
Qed.
Lemma own_mono' E L n1 n2 ty1 ty2 :
- ctx_eq E L n1 n2 → subtype E L ty1 ty2 →
- subtype E L (own_ptr n1 ty1) (own_ptr n2 ty2).
- Proof. intros. by apply own_mono. Qed.
- Global Instance own_proper E L :
- Proper (ctx_eq E L ==> eqtype E L ==> eqtype E L) own_ptr.
- Proof. intros ??? ??[]; split; by apply own_mono. Qed.
+ n1 = n2 → subtype E L ty1 ty2 → subtype E L (own_ptr n1 ty1) (own_ptr n2 ty2).
+ Proof. intros -> *. by apply own_mono. Qed.
+ Global Instance own_proper E L n :
+ Proper (eqtype E L ==> eqtype E L) (own_ptr n).
+ Proof. intros ??[]; split; by apply own_mono. Qed.
Lemma own_proper' E L n1 n2 ty1 ty2 :
- ctx_eq E L n1 n2 → eqtype E L ty1 ty2 →
- eqtype E L (own_ptr n1 ty1) (own_ptr n2 ty2).
- Proof. intros. by apply own_proper. Qed.
+ n1 = n2 → eqtype E L ty1 ty2 → eqtype E L (own_ptr n1 ty1) (own_ptr n2 ty2).
+ Proof. intros -> *. by apply own_proper. Qed.
Global Instance own_type_contractive n : TypeContractive (own_ptr n).
Proof. solve_type_proper. Qed.
@@ -153,8 +150,48 @@ Section own.
Qed.
End own.
-(* TODO: Make box a proper type with subtyping, contractivity, ... *)
-Notation box ty := (own_ptr ty.(ty_size) ty).
+Section box.
+ Context `{typeG Σ}.
+
+ Definition box ty := own_ptr ty.(ty_size) ty.
+
+ Lemma box_type_incl ty1 ty2 :
+ ▷ type_incl ty1 ty2 -∗ type_incl (box ty1) (box ty2).
+ Proof.
+ iIntros "#Hincl". iApply own_type_incl; last done.
+ iDestruct "Hincl" as "(? & _ & _)". done.
+ Qed.
+
+ Global Instance box_mono E L :
+ Proper (subtype E L ==> subtype E L) box.
+ Proof.
+ intros ty1 ty2 Hincl. iIntros. iApply box_type_incl. iApply Hincl; auto.
+ Qed.
+ Lemma box_mono' E L ty1 ty2 :
+ subtype E L ty1 ty2 → subtype E L (box ty1) (box ty2).
+ Proof. intros. by apply box_mono. Qed.
+ Global Instance box_proper E L :
+ Proper (eqtype E L ==> eqtype E L) box.
+ Proof. intros ??[]; split; by apply box_mono. Qed.
+ Lemma box_proper' E L ty1 ty2 :
+ eqtype E L ty1 ty2 → eqtype E L (box ty1) (box ty2).
+ Proof. intros. by apply box_proper. Qed.
+
+ Global Instance box_type_contractive : TypeContractive box.
+ Proof. solve_type_proper. Qed.
+
+ Global Instance box_ne : NonExpansive box.
+ Proof. apply type_contractive_ne, _. Qed.
+
+(* For now, we use the instances inherited from own_ptr. *)
+(* Global Instance box_send ty :
+ Send ty → Send (box ty).
+ Proof. apply _. Qed.
+
+ Global Instance box_sync ty :
+ Sync ty → Sync (box ty).
+ Proof. apply _. Qed. *)
+End box.
Section typing.
Context `{typeG Σ}.
@@ -203,7 +240,7 @@ Section typing.
Closed (x :b: []) e →
0 ≤ n →
(∀ (v : val) (n' := Z.to_nat n),
- typed_body E L C ((v ◠box (uninit n')) :: T) (subst' x v e)) -∗
+ typed_body E L C ((v ◠own_ptr n' (uninit n')) :: T) (subst' x v e)) -∗
typed_body E L C T (let: x := new [ #n ] in e).
Proof. iIntros. iApply type_let; [by apply type_new_instr|solve_typing..]. Qed.
@@ -222,7 +259,7 @@ Section typing.
Lemma type_delete_instr {E L} ty (n : Z) p :
Z.of_nat (ty.(ty_size)) = n →
- typed_instruction E L [p ◠box ty] (delete [ #n; p])%E (λ _, []).
+ typed_instruction E L [p ◠own_ptr ty.(ty_size) ty] (delete [ #n; p])%E (λ _, []).
Proof.
iIntros (<- tid eq) "#LFT $ $ $ Hp". rewrite tctx_interp_singleton.
wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
@@ -298,7 +335,7 @@ Section typing.
Qed.
End typing.
-Hint Resolve own_mono' own_proper' : lrust_typing.
+Hint Resolve own_mono' own_proper' box_mono' box_proper' : lrust_typing.
Hint Extern 100 (_ ≤ _) => simpl; lia : lrust_typing.
Hint Extern 100 (@eq Z _ _) => simpl; lia : lrust_typing.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index c9eb2985..706f7b2c 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -510,35 +510,9 @@ Section subtyping.
- iApply (H23 with "[] []"); done.
Qed.
- (* Conditional equality (intended to be used with sizes) *)
- (* TODO RJ: I'd really like to get rid of this definition. *)
- Definition ctx_eq {A} (x1 x2 : A) : Prop :=
- elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌠-∗ ⌜x1 = x2âŒ.
- Lemma ctx_eq_refl {A} (x : A) : ctx_eq x x.
- Proof. by iIntros "_ _". Qed.
- Global Instance ctx_eq_equivalent {A} : Equivalence (@ctx_eq A).
- Proof.
- split.
- - by iIntros (?) "_ _".
- - iIntros (x y Hxy) "HE HL". by iDestruct (Hxy with "HE HL") as %->.
- - iIntros (x y z Hxy Hyz) "HE HL".
- iDestruct (Hxy with "HE HL") as %->. by iApply (Hyz with "HE HL").
- Qed.
-
Lemma equiv_subtype ty1 ty2 : ty1 ≡ ty2 → subtype ty1 ty2.
Proof. unfold subtype, type_incl=>EQ. setoid_rewrite EQ. apply subtype_refl. Qed.
- Global Instance ty_size_subtype : Proper (subtype ==> ctx_eq) ty_size.
- Proof. iIntros (?? Hst) "HE HL". iDestruct (Hst with "HE HL") as "[$ ?]". Qed.
- Global Instance ty_size_subtype_flip : Proper (flip subtype ==> ctx_eq) ty_size.
- Proof. by intros ?? ->. Qed.
- Lemma ty_size_subtype' ty1 ty2 :
- subtype ty1 ty2 → ctx_eq (ty_size ty1) (ty_size ty2).
- Proof. apply ty_size_subtype. Qed.
- Lemma ty_size_subtype_flip' ty1 ty2 :
- subtype ty2 ty1 → ctx_eq (ty_size ty1) (ty_size ty2).
- Proof. apply ty_size_subtype_flip. Qed.
-
(* TODO: The prelude should have a symmetric closure. *)
Definition eqtype (ty1 ty2 : type) : Prop :=
subtype ty1 ty2 ∧ subtype ty2 ty1.
@@ -586,9 +560,6 @@ Section subtyping.
- intros ??? H1 H2. split; etrans; (apply H1 || apply H2).
Qed.
- Global Instance ty_size_proper_eq : Proper (eqtype ==> ctx_eq) ty_size.
- Proof. by intros ?? [-> _]. Qed.
-
Lemma subtype_simple_type (st1 st2 : simple_type) :
(∀ tid vl, elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌠-∗
st1.(st_own) tid vl -∗ st2.(st_own) tid vl) →
@@ -617,6 +588,5 @@ Section weakening.
Qed.
End weakening.
-Hint Resolve subtype_refl eqtype_refl ctx_eq_refl ty_size_subtype'
- ty_size_subtype_flip': lrust_typing.
-Hint Opaque ctx_eq subtype eqtype : lrust_typing.
+Hint Resolve subtype_refl eqtype_refl : lrust_typing.
+Hint Opaque subtype eqtype : lrust_typing.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 92ef13e3..4cd8f82d 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -346,5 +346,8 @@ Hint Opaque tctx_extract_ctx tctx_extract_hasty tctx_extract_blocked
(* In general, we want reborrowing to be tried before subtyping, so
that we get the extraction. However, in the case the types match
exactly, we want to NOT use reborrowing. Therefore, we add
- [tctx_extract_hasty_here_eq] as a hint with a very low cost. *)
-Hint Resolve tctx_extract_hasty_here_eq | 2 : lrust_typing.
+ [tctx_extract_hasty_here_eq] as a hint with a very low cost.
+ Furthermore, we add it as an external hint to get better unification
+ behavior. *)
+Hint Extern 2 (tctx_extract_hasty _ _ _ _ ((_ â— _) :: _) _) =>
+ apply tctx_extract_hasty_here_eq : lrust_typing.
diff --git a/theories/typing/unsafe/spawn.v b/theories/typing/unsafe/spawn.v
index beb525a3..5c950c99 100644
--- a/theories/typing/unsafe/spawn.v
+++ b/theories/typing/unsafe/spawn.v
@@ -27,7 +27,7 @@ Section join_handle.
Next Obligation. iIntros (?) "**"; auto. Qed.
Lemma join_handle_subtype ty1 ty2 :
- type_incl ty1 ty2 -∗ type_incl (join_handle ty1) (join_handle ty2).
+ ▷ type_incl ty1 ty2 -∗ type_incl (join_handle ty1) (join_handle ty2).
Proof.
iIntros "#Hincl". iSplit; first done. iSplit; iAlways.
- iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
@@ -129,9 +129,8 @@ Section spawn.
destruct c' as [[|c'|]|]; try done. iDestruct "Hc'" as (ty') "[#Hsub Hc']".
iApply (join_spec with "Hc'"). iNext. iIntros "* Hret".
rewrite tctx_interp_singleton tctx_hasty_val.
- iPoseProof "Hsub" as "Hsz". iDestruct "Hsz" as "[% _]".
- iDestruct (own_type_incl with "Hsub") as "(_ & Hincl & _)".
- iApply "Hincl". rewrite -H. done. }
+ iDestruct (box_type_incl with "[$Hsub]") as "(_ & Hincl & _)".
+ iApply "Hincl". done. }
iIntros (r); simpl_subst. iApply type_delete; [solve_typing..|].
iApply (type_jump [_]); solve_typing.
Qed.
--
GitLab