From 03c9ddd36d51822600e2d2d2fea5392c050db766 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 16 Mar 2020 15:18:01 +0100
Subject: [PATCH] update dependencies; fix for coercion removal
---
opam | 2 +-
theories/lifetime/lifetime.v | 4 +-
theories/lifetime/lifetime_sig.v | 10 ++---
theories/lifetime/model/primitive.v | 10 ++---
theories/typing/borrow.v | 8 ++--
theories/typing/cont.v | 2 +-
theories/typing/function.v | 4 +-
theories/typing/int.v | 6 +--
theories/typing/own.v | 14 +++----
theories/typing/programs.v | 33 +++++++--------
theories/typing/shr_bor.v | 2 +-
theories/typing/type.v | 2 +-
theories/typing/type_context.v | 8 ++--
theories/typing/type_sum.v | 62 +++++++++++++++--------------
theories/typing/uniq_bor.v | 4 +-
15 files changed, 87 insertions(+), 84 deletions(-)
diff --git a/opam b/opam
index 705e3802..94bfe07b 100644
--- a/opam
+++ b/opam
@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
"""
depends: [
- "coq-iris" { (= "dev.2020-03-10.6.79f576aa") | (= "dev") }
+ "coq-iris" { (= "dev.2020-03-16.0.62be0a86") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 9d9c54da..6f08298d 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -186,7 +186,7 @@ Proof.
- iApply (bor_fake with "LFT"); [done|]. rewrite -lft_dead_or. auto.
Qed.
-Lemma lft_incl_static κ : (κ ⊑ static)%I.
+Lemma lft_incl_static κ : ⊢ κ ⊑ static.
Proof.
iApply lft_incl_intro. iIntros "!#". iSplitR.
- iIntros (q) "?". iExists 1%Qp. iSplitR. by iApply lft_tok_static. auto.
@@ -194,7 +194,7 @@ Proof.
Qed.
Lemma lft_intersect_list_elem_of_incl κs κ :
- κ ∈ κs → (lft_intersect_list κs ⊑ κ)%I.
+ κ ∈ κs → ⊢ lft_intersect_list κs ⊑ κ.
Proof.
induction 1 as [|???? IH].
- iApply lft_intersect_incl_l.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 72b263c8..8ae5bd7e 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -89,7 +89,7 @@ Module Type lifetime_sig.
Parameter lft_tok_sep : ∀ q κ1 κ2, q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2].
Parameter lft_dead_or : ∀ κ1 κ2, [†κ1] ∨ [†κ2] ⊣⊢ [† κ1 ⊓ κ2].
Parameter lft_tok_dead : ∀ q κ, q.[κ] -∗ [† κ] -∗ False.
- Parameter lft_tok_static : ∀ q, q.[static]%I.
+ Parameter lft_tok_static : ∀ q, ⊢ q.[static].
Parameter lft_dead_static : [† static] -∗ False.
Parameter lft_create : ∀ E, ↑lftN ⊆ E →
@@ -134,9 +134,9 @@ Module Type lifetime_sig.
unless we want to prove them twice (both here and in model.primitive) *)
Parameter lft_intersect_acc : ∀ κ κ' q q', q.[κ] -∗ q'.[κ'] -∗
∃ q'', q''.[κ ⊓ κ'] ∗ (q''.[κ ⊓ κ'] -∗ q.[κ] ∗ q'.[κ']).
- Parameter lft_intersect_incl_l : ∀ κ κ', (κ ⊓ κ' ⊑ κ)%I.
- Parameter lft_intersect_incl_r : ∀ κ κ', (κ ⊓ κ' ⊑ κ')%I.
- Parameter lft_incl_refl : ∀ κ, (κ ⊑ κ)%I.
+ Parameter lft_intersect_incl_l : ∀ κ κ', ⊢ κ ⊓ κ' ⊑ κ.
+ Parameter lft_intersect_incl_r : ∀ κ κ', ⊢ κ ⊓ κ' ⊑ κ'.
+ Parameter lft_incl_refl : ∀ κ, ⊢ κ ⊑ κ.
Parameter lft_incl_trans : ∀ κ κ' κ'', κ ⊑ κ' -∗ κ' ⊑ κ'' -∗ κ ⊑ κ''.
Parameter lft_incl_glb : ∀ κ κ' κ'', κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ⊓ κ''.
Parameter lft_intersect_mono : ∀ κ1 κ1' κ2 κ2',
@@ -154,5 +154,5 @@ Module Type lifetime_sig.
Global Declare Instance subG_lftPreG Σ : subG lftΣ Σ → lftPreG Σ.
Parameter lft_init : ∀ `{!invG Σ, !lftPreG Σ} E, ↑lftN ⊆ E →
- (|={E}=> ∃ _ : lftG Σ, lft_ctx)%I.
+ ⊢ |={E}=> ∃ _ : lftG Σ, lft_ctx.
End lifetime_sig.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 1d1d3a55..74dab275 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -19,7 +19,7 @@ Proof.
Qed.
Lemma lft_init `{!lftPreG Σ} E :
- ↑lftN ⊆ E → (|={E}=> ∃ _ : lftG Σ, lft_ctx)%I.
+ ↑lftN ⊆ E → ⊢ |={E}=> ∃ _ : lftG Σ, lft_ctx.
Proof.
iIntros (?). rewrite /lft_ctx.
iMod (own_alloc (● ∅ : authR alftUR)) as (γa) "Ha"; first by apply auth_auth_valid.
@@ -280,7 +280,7 @@ Proof.
move: Hvalid=> /auth_frag_valid /=; by rewrite op_singleton singleton_valid.
Qed.
-Lemma lft_tok_static q : q.[static]%I.
+Lemma lft_tok_static q : ⊢ q.[static].
Proof. by rewrite /lft_tok big_sepMS_empty. Qed.
Lemma lft_dead_static : [† static] -∗ False.
@@ -326,7 +326,7 @@ Lemma lft_incl_intro κ κ' :
([†κ'] ={↑lftN}=∗ [†κ])) -∗ κ ⊑ κ'.
Proof. reflexivity. Qed.
-Lemma lft_intersect_incl_l κ κ': (κ ⊓ κ' ⊑ κ)%I.
+Lemma lft_intersect_incl_l κ κ': ⊢ κ ⊓ κ' ⊑ κ.
Proof.
unfold lft_incl. iIntros "!#". iSplitR.
- iIntros (q). rewrite <-lft_tok_sep. iIntros "[H Hf]". iExists q. iFrame.
@@ -334,10 +334,10 @@ Proof.
- iIntros "? !>". iApply lft_dead_or. auto.
Qed.
-Lemma lft_intersect_incl_r κ κ': (κ ⊓ κ' ⊑ κ')%I.
+Lemma lft_intersect_incl_r κ κ': ⊢ κ ⊓ κ' ⊑ κ'.
Proof. rewrite comm. apply lft_intersect_incl_l. Qed.
-Lemma lft_incl_refl κ : (κ ⊑ κ)%I.
+Lemma lft_incl_refl κ : ⊢ κ ⊑ κ.
Proof. unfold lft_incl. iIntros "!#"; iSplitR; auto 10 with iFrame. Qed.
Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' -∗ κ' ⊑ κ'' -∗ κ ⊑ κ''.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 7557c5de..da1434ef 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -84,7 +84,7 @@ Section borrow.
Lemma type_deref_uniq_own_instr {E L} κ p n ty :
lctx_lft_alive E L κ →
- typed_instruction_ty E L [p ◁ &uniq{κ}(own_ptr n ty)] (!p) (&uniq{κ} ty).
+ ⊢ typed_instruction_ty E L [p ◁ &uniq{κ}(own_ptr n ty)] (!p) (&uniq{κ} ty).
Proof.
iIntros (Hκ tid) "#LFT HE $ HL Hp".
rewrite tctx_interp_singleton.
@@ -114,7 +114,7 @@ Section borrow.
Lemma type_deref_shr_own_instr {E L} κ p n ty :
lctx_lft_alive E L κ →
- typed_instruction_ty E L [p ◁ &shr{κ}(own_ptr n ty)] (!p) (&shr{κ} ty).
+ ⊢ typed_instruction_ty E L [p ◁ &shr{κ}(own_ptr n ty)] (!p) (&shr{κ} ty).
Proof.
iIntros (Hκ tid) "#LFT HE $ HL Hp".
rewrite tctx_interp_singleton.
@@ -140,7 +140,7 @@ Section borrow.
Lemma type_deref_uniq_uniq_instr {E L} κ κ' p ty :
lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
- typed_instruction_ty E L [p ◁ &uniq{κ}(&uniq{κ'}ty)] (!p) (&uniq{κ} ty).
+ ⊢ typed_instruction_ty E L [p ◁ &uniq{κ}(&uniq{κ'}ty)] (!p) (&uniq{κ} ty).
Proof.
iIntros (Hκ Hincl tid) "#LFT #HE $ HL Hp".
rewrite tctx_interp_singleton.
@@ -172,7 +172,7 @@ Section borrow.
Lemma type_deref_shr_uniq_instr {E L} κ κ' p ty :
lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
- typed_instruction_ty E L [p ◁ &shr{κ}(&uniq{κ'}ty)] (!p) (&shr{κ}ty).
+ ⊢ typed_instruction_ty E L [p ◁ &shr{κ}(&uniq{κ'}ty)] (!p) (&shr{κ}ty).
Proof.
iIntros (Hκ Hincl tid) "#LFT HE $ HL Hp". rewrite tctx_interp_singleton.
iDestruct (Hincl with "HL HE") as "#Hincl".
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 12a6374d..74a23f0f 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -14,7 +14,7 @@ Section typing.
Forall2 (λ a av, to_val a = Some av ∨ a = of_val av) args argsv →
k ◁cont(L, T') ∈ C →
tctx_incl E L T (T' (list_to_vec argsv)) →
- typed_body E L C T (k args).
+ ⊢ typed_body E L C T (k args).
Proof.
iIntros (Hargs HC Hincl tid) "#LFT #HE Hna HL HC HT".
iMod (Hincl with "LFT HE HL HT") as "(HL & HT)".
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 53cabf07..f673180d 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -318,7 +318,7 @@ Section typing.
{A} (fp : A → fn_params (length ps)) (k : val) x :
Forall (lctx_lft_alive E L) κs →
(∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> κs) ++ E) L ((fp x).(fp_E) ϝ)) →
- typed_body E L [k ◁cont(L, λ v : vec _ 1, ((v!!!0%fin:val) ◁ box (fp x).(fp_ty)) :: T)]
+ ⊢ typed_body E L [k ◁cont(L, λ v : vec _ 1, ((v!!!0%fin:val) ◁ box (fp x).(fp_ty)) :: T)]
((p ◁ fn fp) ::
zip_with TCtx_hasty ps (box <$> vec_to_list (fp x).(fp_tys)) ++
T)
@@ -344,7 +344,7 @@ Section typing.
(box <$> vec_to_list (fp x).(fp_tys))) T T' →
k ◁cont(L, T'') ∈ C →
(∀ ret : val, tctx_incl E L ((ret ◁ box (fp x).(fp_ty))::T') (T'' [# ret])) →
- typed_body E L C T (call: p ps → k).
+ ⊢ typed_body E L C T (call: p ps → k).
Proof.
intros Hfn HL HE HTT' HC HT'T''.
rewrite -typed_body_mono /flip; last done; first by eapply type_call'.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 0b3d8e1c..56b2cf33 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -37,7 +37,7 @@ Section typing.
Proof. iIntros. iApply type_let; [apply type_int_instr|solve_typing|done]. Qed.
Lemma type_plus_instr E L p1 p2 :
- typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 + p2) int.
+ ⊢ typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 + p2) int.
Proof.
iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
@@ -53,7 +53,7 @@ Section typing.
Proof. iIntros. iApply type_let; [iApply type_plus_instr|solve_typing|done]. Qed.
Lemma type_minus_instr E L p1 p2 :
- typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 - p2) int.
+ ⊢ typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 - p2) int.
Proof.
iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
@@ -69,7 +69,7 @@ Section typing.
Proof. iIntros. iApply type_let; [apply type_minus_instr|solve_typing|done]. Qed.
Lemma type_le_instr E L p1 p2 :
- typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 ≤ p2) bool.
+ ⊢ typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 ≤ p2) bool.
Proof.
iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index f55191b3..484a8187 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -219,7 +219,7 @@ Section typing.
(** Typing *)
Lemma write_own {E L} ty ty' n :
- ty.(ty_size) = ty'.(ty_size) → typed_write E L (own_ptr n ty') ty (own_ptr n ty).
+ ty.(ty_size) = ty'.(ty_size) → ⊢ typed_write E L (own_ptr n ty') ty (own_ptr n ty).
Proof.
iIntros (Hsz) "!#". iIntros ([[]|] tid F qL ?) "_ _ $ Hown"; try done.
rewrite /= Hsz. iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
@@ -227,7 +227,7 @@ Section typing.
Qed.
Lemma read_own_copy E L ty n :
- Copy ty → typed_read E L (own_ptr n ty) ty (own_ptr n ty).
+ Copy ty → ⊢ typed_read E L (own_ptr n ty) ty (own_ptr n ty).
Proof.
iIntros (Hsz) "!#". iIntros ([[]|] tid F qL ?) "_ _ $ $ Hown"; try done.
iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ #Hown]".
@@ -236,7 +236,7 @@ Section typing.
Qed.
Lemma read_own_move E L ty n :
- typed_read E L (own_ptr n ty) ty (own_ptr n $ uninit ty.(ty_size)).
+ ⊢ typed_read E L (own_ptr n ty) ty (own_ptr n $ uninit ty.(ty_size)).
Proof.
iAlways. iIntros ([[]|] tid F qL ?) "_ _ $ $ Hown"; try done.
iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
@@ -247,8 +247,8 @@ Section typing.
Lemma type_new_instr {E L} (n : Z) :
0 ≤ n →
- let n' := Z.to_nat n in
- typed_instruction_ty E L [] (new [ #n ]%E) (own_ptr n' (uninit n')).
+ ⊢ let n' := Z.to_nat n in
+ typed_instruction_ty E L [] (new [ #n ]%E) (own_ptr n' (uninit n')).
Proof.
iIntros (? tid) "#LFT #HE $ $ _".
iApply wp_new; try done. iModIntro.
@@ -281,7 +281,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 ◁ own_ptr ty.(ty_size) ty] (delete [ #n; p])%E (λ _, []).
+ ⊢ typed_instruction E L [p ◁ own_ptr ty.(ty_size) ty] (delete [ #n; p])%E (λ _, []).
Proof.
iIntros (<- tid) "#LFT #HE $ $ Hp". rewrite tctx_interp_singleton.
wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
@@ -328,7 +328,7 @@ Section typing.
Lemma type_letalloc_n {E L} ty ty1 ty2 C T T' (x : string) p e :
Closed [] p → Closed (x :b: []) e →
tctx_extract_hasty E L p ty1 T T' →
- typed_read E L ty1 ty ty2 →
+ (⊢ typed_read E L ty1 ty ty2) →
(∀ (v : val),
typed_body E L C ((v ◁ own_ptr (ty.(ty_size)) ty)::(p ◁ ty2)::T') (subst x v e)) -∗
typed_body E L C T (letalloc: x <-{ty.(ty_size)} !p in e).
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 56e7e825..1e0f4630 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -83,7 +83,7 @@ Definition typed_instruction_ty `{!typeG Σ} (E : elctx) (L : llctx) (T : tctx)
Arguments typed_instruction_ty {_ _} _ _ _ _%E _%T.
Definition typed_val `{!typeG Σ} (v : val) (ty : type) : Prop :=
- ∀ E L, typed_instruction_ty E L [] (of_val v) ty.
+ ∀ E L, ⊢ typed_instruction_ty E L [] (of_val v) ty.
Arguments typed_val _ _ _%V _%T.
Section typing_rules.
@@ -98,8 +98,8 @@ Section typing_rules.
(* TODO: Proof a version of this that substitutes into a compatible context...
if we really want to do that. *)
Lemma type_equivalize_lft E L C T κ1 κ2 e :
- typed_body ((κ1 ⊑ₑ κ2) :: (κ2 ⊑ₑ κ1) :: E) L C T e →
- typed_body E ((κ1 ⊑ₗ [κ2]) :: L) C T e.
+ (⊢ typed_body ((κ1 ⊑ₑ κ2) :: (κ2 ⊑ₑ κ1) :: E) L C T e) →
+ ⊢ typed_body E ((κ1 ⊑ₗ [κ2]) :: L) C T e.
Proof.
iIntros (He tid) "#LFT #HE Htl [Hκ HL] HC HT".
iMod (lctx_equalize_lft with "LFT Hκ") as "[Hκ1 Hκ2]".
@@ -128,7 +128,7 @@ Section typing_rules.
for the following hypothesis. *)
Lemma type_let E L T T' T1 T2 C xb e e' :
Closed (xb :b: []) e' →
- typed_instruction E L T1 e T2 →
+ (⊢ typed_instruction E L T1 e T2) →
tctx_extract_ctx E L T1 T T' →
(∀ v : val, typed_body E L C (T2 v ++ T') (subst' xb v e')) -∗
typed_body E L C T (let: xb := e in e').
@@ -139,7 +139,7 @@ Section typing_rules.
Lemma type_seq E L T T' T1 T2 C e e' :
Closed [] e' →
- typed_instruction E L T1 e (λ _, T2) →
+ (⊢ typed_instruction E L T1 e (λ _, T2)) →
tctx_extract_ctx E L T1 T T' →
typed_body E L C (T2 ++ T') e' -∗
typed_body E L C T (e ;; e').
@@ -174,7 +174,7 @@ Section typing_rules.
Qed.
Lemma type_path_instr {E L} p ty :
- typed_instruction_ty E L [p ◁ ty] p ty.
+ ⊢ typed_instruction_ty E L [p ◁ ty] p ty.
Proof.
iIntros (?) "_ _ $$ [? _]".
iApply (wp_hasty with "[-]"). done. iIntros (v) "_ Hv".
@@ -189,8 +189,8 @@ Section typing_rules.
Proof. iIntros. iApply type_let; [by apply type_path_instr|solve_typing|done]. Qed.
Lemma type_assign_instr {E L} ty ty1 ty1' p1 p2 :
- typed_write E L ty1 ty ty1' →
- typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <- p2) (λ _, [p1 ◁ ty1']).
+ (⊢ typed_write E L ty1 ty ty1') →
+ (⊢ typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <- p2) (λ _, [p1 ◁ ty1'])).
Proof.
iIntros (Hwrt tid) "#LFT #HE $ HL".
rewrite tctx_interp_cons tctx_interp_singleton. iIntros "[Hp1 Hp2]".
@@ -209,14 +209,14 @@ Section typing_rules.
Lemma type_assign {E L} ty1 ty ty1' C T T' p1 p2 e:
Closed [] e →
tctx_extract_ctx E L [p1 ◁ ty1; p2 ◁ ty] T T' →
- typed_write E L ty1 ty ty1' →
+ (⊢ typed_write E L ty1 ty ty1') →
typed_body E L C ((p1 ◁ ty1') :: T') e -∗
typed_body E L C T (p1 <- p2 ;; e).
Proof. iIntros. by iApply type_seq; first apply type_assign_instr. Qed.
Lemma type_deref_instr {E L} ty ty1 ty1' p :
- ty.(ty_size) = 1%nat → typed_read E L ty1 ty ty1' →
- typed_instruction E L [p ◁ ty1] (!p) (λ v, [p ◁ ty1'; v ◁ ty]).
+ ty.(ty_size) = 1%nat → (⊢ typed_read E L ty1 ty ty1') →
+ (⊢ typed_instruction E L [p ◁ ty1] (!p) (λ v, [p ◁ ty1'; v ◁ ty])).
Proof.
iIntros (Hsz Hread tid) "#LFT #HE Htl HL Hp".
rewrite tctx_interp_singleton. wp_bind p. iApply (wp_hasty with "Hp").
@@ -234,7 +234,7 @@ Section typing_rules.
Lemma type_deref {E L} ty1 C T T' ty ty1' x p e:
Closed (x :b: []) e →
tctx_extract_hasty E L p ty1 T T' →
- typed_read E L ty1 ty ty1' →
+ (⊢ typed_read E L ty1 ty ty1') →
ty.(ty_size) = 1%nat →
(∀ (v : val), typed_body E L C ((p ◁ ty1') :: (v ◁ ty) :: T') (subst' x v e)) -∗
typed_body E L C T (let: x := !p in e).
@@ -267,8 +267,9 @@ Section typing_rules.
Lemma type_memcpy_instr {E L} ty ty1 ty1' ty2 ty2' (n : Z) p1 p2 :
Z.of_nat (ty.(ty_size)) = n →
- typed_write E L ty1 ty ty1' → typed_read E L ty2 ty ty2' →
- typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2] (p1 <-{n} !p2)
+ (⊢ typed_write E L ty1 ty ty1') →
+ (⊢ typed_read E L ty2 ty ty2') →
+ ⊢ typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2] (p1 <-{n} !p2)
(λ _, [p1 ◁ ty1'; p2 ◁ ty2']).
Proof.
iIntros (Hsz Hwrt Hread tid) "#LFT #HE Htl HL HT".
@@ -282,8 +283,8 @@ Section typing_rules.
Lemma type_memcpy {E L} ty ty1 ty2 (n : Z) C T T' ty1' ty2' p1 p2 e:
Closed [] e →
tctx_extract_ctx E L [p1 ◁ ty1; p2 ◁ ty2] T T' →
- typed_write E L ty1 ty ty1' →
- typed_read E L ty2 ty ty2' →
+ (⊢ typed_write E L ty1 ty ty1') →
+ (⊢ typed_read E L ty2 ty ty2') →
Z.of_nat (ty.(ty_size)) = n →
typed_body E L C ((p1 ◁ ty1') :: (p2 ◁ ty2') :: T') e -∗
typed_body E L C T (p1 <-{n} !p2;; e).
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 4a447451..b866efaf 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -82,7 +82,7 @@ Section typing.
Qed.
Lemma read_shr E L κ ty :
- Copy ty → lctx_lft_alive E L κ → typed_read E L (&shr{κ}ty) ty (&shr{κ}ty).
+ Copy ty → lctx_lft_alive E L κ → ⊢ typed_read E L (&shr{κ}ty) ty (&shr{κ}ty).
Proof.
iIntros (Hcopy Halive) "!#".
iIntros ([[]|] tid F qL ?) "#LFT #HE Htl HL #Hshr"; try done.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index f37ede51..c969d758 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -546,7 +546,7 @@ Section subtyping.
Global Instance type_incl_persistent ty1 ty2 : Persistent (type_incl ty1 ty2) := _.
- Lemma type_incl_refl ty : type_incl ty ty.
+ Lemma type_incl_refl ty : ⊢ type_incl ty ty.
Proof. iSplit; first done. iSplit; iAlways; iIntros; done. Qed.
Lemma type_incl_trans ty1 ty2 ty3 :
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index e56f40df..b73bd978 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -36,7 +36,7 @@ Section type_context.
Proof. destruct v. done. simpl. rewrite (decide_left _). done. Qed.
Lemma wp_eval_path E p v :
- eval_path p = Some v → (WP p @ E {{ v', ⌜v' = v⌝ }})%I.
+ eval_path p = Some v → ⊢ WP p @ E {{ v', ⌜v' = v⌝ }}.
Proof.
revert v; induction p; intros v; try done.
{ intros [=]. by iApply wp_value. }
@@ -119,18 +119,18 @@ Section type_context.
Proof. intros ???. by apply big_opL_permutation. Qed.
Lemma tctx_interp_cons tid x T :
- tctx_interp tid (x :: T) ≡ (tctx_elt_interp tid x ∗ tctx_interp tid T)%I.
+ tctx_interp tid (x :: T) ⊣⊢ (tctx_elt_interp tid x ∗ tctx_interp tid T).
Proof. done. Qed.
Lemma tctx_interp_app tid T1 T2 :
- tctx_interp tid (T1 ++ T2) ≡ (tctx_interp tid T1 ∗ tctx_interp tid T2)%I.
+ tctx_interp tid (T1 ++ T2) ⊣⊢ (tctx_interp tid T1 ∗ tctx_interp tid T2).
Proof. rewrite /tctx_interp big_sepL_app //. Qed.
Definition tctx_interp_nil tid :
tctx_interp tid [] = True%I := eq_refl _.
Lemma tctx_interp_singleton tid x :
- tctx_interp tid [x] ≡ tctx_elt_interp tid x.
+ tctx_interp tid [x] ⊣⊢ tctx_elt_interp tid x.
Proof. rewrite /tctx_interp /= right_id //. Qed.
(** Copy typing contexts *)
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index cf00d06c..127ecbf6 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -10,11 +10,12 @@ Section case.
(* FIXME : have a iris version of Forall2. *)
Lemma type_case_own' E L C T p n tyl el :
Forall2 (λ ty e,
- typed_body E L C ((p +ₗ #0 ◁ own_ptr n (uninit 1)) :: (p +ₗ #1 ◁ own_ptr n ty) ::
+ (⊢ typed_body E L C ((p +ₗ #0 ◁ own_ptr n (uninit 1)) :: (p +ₗ #1 ◁ own_ptr n ty) ::
(p +ₗ #(S (ty.(ty_size))) ◁
- own_ptr n (uninit (max_list_with ty_size tyl - ty_size ty))) :: T) e ∨
- typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T) e) tyl el →
- typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T) (case: !p of el).
+ own_ptr n (uninit (max_list_with ty_size tyl - ty_size ty))) :: T) e) ∨
+ (⊢ typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T) e))
+ tyl el →
+ ⊢ typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T) (case: !p of el).
Proof.
iIntros (Hel tid) "#LFT #HE Hna HL HC HT". wp_bind p.
rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
@@ -47,19 +48,20 @@ Section case.
Lemma type_case_own E L C T T' p n tyl el :
tctx_extract_hasty E L p (own_ptr n (sum tyl)) T T' →
Forall2 (λ ty e,
- typed_body E L C ((p +ₗ #0 ◁ own_ptr n (uninit 1)) :: (p +ₗ #1 ◁ own_ptr n ty) ::
+ (⊢ typed_body E L C ((p +ₗ #0 ◁ own_ptr n (uninit 1)) :: (p +ₗ #1 ◁ own_ptr n ty) ::
(p +ₗ #(S (ty.(ty_size))) ◁
- own_ptr n (uninit (max_list_with ty_size tyl - ty_size ty))) :: T') e ∨
- typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T') e) tyl el →
- typed_body E L C T (case: !p of el).
+ own_ptr n (uninit (max_list_with ty_size tyl - ty_size ty))) :: T') e) ∨
+ (⊢ typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T') e))
+ tyl el →
+ ⊢ typed_body E L C T (case: !p of el).
Proof. unfold tctx_extract_hasty=>->. apply type_case_own'. Qed.
Lemma type_case_uniq' E L C T p κ tyl el :
lctx_lft_alive E L κ →
Forall2 (λ ty e,
- typed_body E L C ((p +ₗ #1 ◁ &uniq{κ}ty) :: T) e ∨
- typed_body E L C ((p ◁ &uniq{κ}(sum tyl)) :: T) e) tyl el →
- typed_body E L C ((p ◁ &uniq{κ}(sum tyl)) :: T) (case: !p of el).
+ (⊢ typed_body E L C ((p +ₗ #1 ◁ &uniq{κ}ty) :: T) e) ∨
+ (⊢ typed_body E L C ((p ◁ &uniq{κ}(sum tyl)) :: T) e)) tyl el →
+ ⊢ typed_body E L C ((p ◁ &uniq{κ}(sum tyl)) :: T) (case: !p of el).
Proof.
iIntros (Halive Hel tid) "#LFT #HE Hna HL HC HT". wp_bind p.
rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
@@ -102,17 +104,17 @@ Section case.
tctx_extract_hasty E L p (&uniq{κ}(sum tyl)) T T' →
lctx_lft_alive E L κ →
Forall2 (λ ty e,
- typed_body E L C ((p +ₗ #1 ◁ &uniq{κ}ty) :: T') e ∨
- typed_body E L C ((p ◁ &uniq{κ}(sum tyl)) :: T') e) tyl el →
- typed_body E L C T (case: !p of el).
+ (⊢ typed_body E L C ((p +ₗ #1 ◁ &uniq{κ}ty) :: T') e) ∨
+ (⊢ typed_body E L C ((p ◁ &uniq{κ}(sum tyl)) :: T') e)) tyl el →
+ ⊢ typed_body E L C T (case: !p of el).
Proof. unfold tctx_extract_hasty=>->. apply type_case_uniq'. Qed.
Lemma type_case_shr' E L C T p κ tyl el:
lctx_lft_alive E L κ →
Forall2 (λ ty e,
- typed_body E L C ((p +ₗ #1 ◁ &shr{κ}ty) :: T) e ∨
- typed_body E L C ((p ◁ &shr{κ}(sum tyl)) :: T) e) tyl el →
- typed_body E L C ((p ◁ &shr{κ}(sum tyl)) :: T) (case: !p of el).
+ (⊢ typed_body E L C ((p +ₗ #1 ◁ &shr{κ}ty) :: T) e) ∨
+ (⊢ typed_body E L C ((p ◁ &shr{κ}(sum tyl)) :: T) e)) tyl el →
+ ⊢ typed_body E L C ((p ◁ &shr{κ}(sum tyl)) :: T) (case: !p of el).
Proof.
iIntros (Halive Hel tid) "#LFT #HE Hna HL HC HT". wp_bind p.
rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
@@ -134,8 +136,8 @@ Section case.
Lemma type_case_shr E L C T p κ tyl el :
p ◁ &shr{κ}(sum tyl) ∈ T →
lctx_lft_alive E L κ →
- Forall2 (λ ty e, typed_body E L C ((p +ₗ #1 ◁ &shr{κ}ty) :: T) e) tyl el →
- typed_body E L C T (case: !p of el).
+ Forall2 (λ ty e, ⊢ typed_body E L C ((p +ₗ #1 ◁ &shr{κ}ty) :: T) e) tyl el →
+ ⊢ typed_body E L C T (case: !p of el).
Proof.
intros. rewrite ->copy_elem_of_tctx_incl; last done; last apply _.
apply type_case_shr'; first done. eapply Forall2_impl; first done. auto.
@@ -143,8 +145,8 @@ Section case.
Lemma type_sum_assign_instr {E L} (i : nat) ty1 tyl ty ty2 p1 p2 :
tyl !! i = Some ty →
- typed_write E L ty1 (sum tyl) ty2 →
- typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <-{Σ i} p2) (λ _, [p1 ◁ ty2]).
+ (⊢ typed_write E L ty1 (sum tyl) ty2) →
+ ⊢ typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <-{Σ i} p2) (λ _, [p1 ◁ ty2]).
Proof.
iIntros (Hty Hw tid) "#LFT #HE $ HL Hp".
rewrite tctx_interp_cons tctx_interp_singleton.
@@ -173,7 +175,7 @@ Section case.
sty = sum tyl →
tctx_extract_ctx E L [p1 ◁ ty1; p2 ◁ ty] T T' →
tyl !! (Z.to_nat i) = Some ty →
- typed_write E L ty1 sty ty1' →
+ (⊢ typed_write E L ty1 sty ty1') →
typed_body E L C ((p1 ◁ ty1') :: T') e -∗
typed_body E L C T (p1 <-{Σ i} p2 ;; e).
Proof.
@@ -183,8 +185,8 @@ Section case.
Lemma type_sum_unit_instr {E L} (i : nat) tyl ty1 ty2 p :
tyl !! i = Some unit →
- typed_write E L ty1 (sum tyl) ty2 →
- typed_instruction E L [p ◁ ty1] (p <-{Σ i} ()) (λ _, [p ◁ ty2]).
+ (⊢ typed_write E L ty1 (sum tyl) ty2) →
+ ⊢ typed_instruction E L [p ◁ ty1] (p <-{Σ i} ()) (λ _, [p ◁ ty2]).
Proof.
iIntros (Hty Hw tid) "#LFT #HE $ HL Hp". rewrite tctx_interp_singleton.
wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hty".
@@ -202,7 +204,7 @@ Section case.
sty = sum tyl →
tctx_extract_hasty E L p ty1 T T' →
tyl !! (Z.to_nat i) = Some unit →
- typed_write E L ty1 sty ty1' →
+ (⊢ typed_write E L ty1 sty ty1') →
typed_body E L C ((p ◁ ty1') :: T') e -∗
typed_body E L C T (p <-{Σ i} () ;; e).
Proof.
@@ -212,9 +214,9 @@ Section case.
Lemma type_sum_memcpy_instr {E L} (i : nat) tyl ty1 ty1' ty2 ty2' ty p1 p2 :
tyl !! i = Some ty →
- typed_write E L ty1 (sum tyl) ty1' →
- typed_read E L ty2 ty ty2' →
- typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2]
+ (⊢ typed_write E L ty1 (sum tyl) ty1') →
+ (⊢ typed_read E L ty2 ty ty2') →
+ ⊢ typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2]
(p1 <-{ty.(ty_size),Σ i} !p2) (λ _, [p1 ◁ ty1'; p2 ◁ ty2']).
Proof.
iIntros (Hty Hw Hr tid) "#LFT #HE Htl [HL1 HL2] Hp".
@@ -253,8 +255,8 @@ Section case.
sty = sum tyl →
tctx_extract_ctx E L [p1 ◁ ty1; p2 ◁ ty2] T T' →
tyl !! (Z.to_nat i) = Some ty →
- typed_write E L ty1 sty ty1' →
- typed_read E L ty2 ty ty2' →
+ (⊢ typed_write E L ty1 sty ty1') →
+ (⊢ typed_read E L ty2 ty ty2') →
Z.of_nat (ty.(ty_size)) = n →
typed_body E L C ((p1 ◁ ty1') :: (p2 ◁ ty2') :: T') e -∗
typed_body E L C T (p1 <-{n,Σ i} !p2 ;; e).
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index d796d3f8..e1290e81 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -129,7 +129,7 @@ Section typing.
Qed.
Lemma read_uniq E L κ ty :
- Copy ty → lctx_lft_alive E L κ → typed_read E L (&uniq{κ}ty) ty (&uniq{κ}ty).
+ Copy ty → lctx_lft_alive E L κ → ⊢ typed_read E L (&uniq{κ}ty) ty (&uniq{κ}ty).
Proof.
iIntros (Hcopy Halive) "!#".
iIntros ([[]|] tid F qL ?) "#LFT #HE Htl HL Hown"; try done.
@@ -143,7 +143,7 @@ Section typing.
Qed.
Lemma write_uniq E L κ ty :
- lctx_lft_alive E L κ → typed_write E L (&uniq{κ}ty) ty (&uniq{κ}ty).
+ lctx_lft_alive E L κ → ⊢ typed_write E L (&uniq{κ}ty) ty (&uniq{κ}ty).
Proof.
iIntros (Halive) "!#".
iIntros ([[]|] tid F qL ?) "#LFT HE HL Hown"; try done.
--
GitLab