From 5ce66be3e9bf7f978acb10ccbda8a0a8f334d611 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Tue, 14 Sep 2021 21:23:52 +0200
Subject: [PATCH] Update dependency
---
coq-lambda-rust.opam | 2 +-
theories/lang/arc.v | 24 ++++++++++++------------
theories/lang/lock.v | 6 +++---
theories/lang/memcpy.v | 2 +-
theories/lang/spawn.v | 8 ++++----
theories/lang/swap.v | 2 +-
theories/logic/gps.v | 16 ++++++++--------
theories/typing/cont_context.v | 2 +-
theories/typing/function.v | 8 ++++----
theories/typing/lib/rc/rc.v | 2 +-
theories/typing/programs.v | 6 +++---
theories/typing/type_context.v | 6 ++++--
12 files changed, 43 insertions(+), 41 deletions(-)
diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index d9d81aeb..e0929c29 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
"""
depends: [
- "coq-gpfsl" { (= "dev.2021-09-07.0.7adc00e0") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2021-09-14.0.013913bf") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index 4cdbd4c3..af6184c4 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -695,7 +695,7 @@ Section arc.
Lemma strong_count_spec γi γs γw γsw l t v (P : vProp) tid :
is_arc P1 P2 N γi γs γw γsw l -∗ strong_arc_acc l t γi γs γw γsw P (⊤ ∖ ↑N) -∗
{{{ GPS_SWReader l t () v γs ∗ P }}}
- strong_count [ #l] in tid
+ strong_count [ #l] @ tid; ⊤
{{{ (c : Z), RET #c; P ∗ ⌜0 < c⌠}}}.
Proof.
iIntros "#INV #Hacc !# * [#RR HP] HΦ". iLöb as "IH". wp_rec.
@@ -748,7 +748,7 @@ Section arc.
strong_arc_acc l ts γi γs γw γsw P (⊤ ∖ ↑N) -∗
GPS_SWReader (l >> 1) t () v γw -∗
{{{ P }}}
- weak_count [ #l] in tid
+ weak_count [ #l] @ tid; ⊤
{{{ (c : Z), RET #c; P ∗ ⌜-1 ≤ c⌠}}}.
Proof.
iIntros "#INV #Hacc #RR !# * HP HΦ". iLöb as "IH". wp_rec. wp_op.
@@ -808,7 +808,7 @@ Section arc.
is_arc P1 P2 N γi γs γw γsw l -∗ strong_arc_acc l t γi γs γw γsw P (⊤ ∖ ↑N) -∗
(∃ t' v', GPS_SWReader (l >> 1) t' () v' γw) -∗
GPS_SWReader l t () v γs -∗
- {{{ P }}} clone_arc [ #l] in tid
+ {{{ P }}} clone_arc [ #l] @ tid; ⊤
{{{ t' q', RET #☠; P ∗ strong_arc t' q' l γi γs γw γsw ∗ P1 q' }}}.
Proof.
iIntros "#INV #Hacc #WR #RR !# * HP HΦ". iLöb as "IH". wp_rec.
@@ -1031,7 +1031,7 @@ Section arc.
Lemma downgrade_spec γi γs γw γsw l t v ts (P : vProp) tid:
is_arc P1 P2 N γi γs γw γsw l -∗ strong_arc_acc l ts γi γs γw γsw P (⊤ ∖ ↑N) -∗
GPS_SWReader (l >> 1) t () v γw -∗
- {{{ P }}} downgrade [ #l] in tid
+ {{{ P }}} downgrade [ #l] @ tid; ⊤
{{{ t' q', RET #☠; P ∗ weak_arc t' q' l γi γs γw γsw }}}.
Proof.
iIntros "#INV #Hacc #WR !# * HP HΦ". iLöb as "IH". wp_rec. wp_op.
@@ -1201,7 +1201,7 @@ Section arc.
is_arc P1 P2 N γi γs γw γsw l -∗ weak_arc_acc l t γi γs γw γsw P (⊤ ∖ ↑N) -∗
(∃ t' v', GPS_SWReader l t' () v' γs) -∗
GPS_SWReader (l >> 1) t () v γw -∗
- {{{ P }}} clone_weak [ #l] in tid
+ {{{ P }}} clone_weak [ #l] @ tid; ⊤
{{{ t' q', RET #☠; P ∗ weak_arc t' q' l γi γs γw γsw }}}.
Proof.
iIntros "#INV #Hacc #SR #WR !# * HP HΦ". iLöb as "IH". wp_rec. wp_op.
@@ -1388,7 +1388,7 @@ Section arc.
is_arc P1 P2 N γi γs γw γsw l -∗ weak_arc_acc l tw γi γs γw γsw P (⊤ ∖ ↑N) -∗
(∃ t' v', GPS_SWReader (l >> 1) t' () v' γw) -∗
GPS_SWReader l t () v γs -∗
- {{{ P }}} upgrade [ #l] in tid
+ {{{ P }}} upgrade [ #l] @ tid; ⊤
{{{ (b : bool) q, RET #b;
P ∗ if b then ∃ ts, strong_arc ts q l γi γs γw γsw ∗ P1 q else True }}}.
Proof.
@@ -1553,7 +1553,7 @@ Section arc.
Lemma drop_weak_spec γi γs γw γsw l q tid :
histN ## N → is_arc P1 P2 N γi γs γw γsw l -∗
- {{{ (∃ tw, weak_arc tw q l γi γs γw γsw) }}} drop_weak [ #l] in tid
+ {{{ (∃ tw, weak_arc tw q l γi γs γw γsw) }}} drop_weak [ #l] @ tid; ⊤
{{{ (b : bool), RET #b ; if b then P2 ∗ l ↦ #0 ∗ (l >> 1) ↦ #0 else True }}}.
Proof.
iIntros (?) "#INV !# * HP HΦ". iLöb as "IH". wp_rec. wp_op.
@@ -1811,7 +1811,7 @@ Section arc.
Lemma drop_fake_spec γi γs γw γsw l tid :
histN ## N → is_arc P1 P2 N γi γs γw γsw l -∗
- {{{ fake_arc l γi γs γw γsw ∗ P2 }}} drop_weak [ #l] in tid
+ {{{ fake_arc l γi γs γw γsw ∗ P2 }}} drop_weak [ #l] @ tid; ⊤
{{{ (b : bool), RET #b ; if b then P2 ∗ l ↦ #0 ∗ (l >> 1) ↦ #0 else True }}}.
Proof.
iIntros (?) "#INV !# * [HP HP2] HΦ". iLöb as "IH". wp_rec. wp_op.
@@ -2031,7 +2031,7 @@ Section arc.
Lemma drop_arc_spec {HPn: HP2} γi γs γw γsw l q tid :
histN ## N → is_arc P1 P2 N γi γs γw γsw l -∗
{{{ (∃ ts, strong_arc ts q l γi γs γw γsw) ∗ P1 q }}}
- drop_arc [ #l] in tid
+ drop_arc [ #l] @ tid; ⊤
{{{ (b : bool), RET #b ;
if b then P1 1 ∗ fake_arc l γi γs γw γsw else True }}}.
Proof.
@@ -2252,7 +2252,7 @@ Section arc.
Lemma try_unwrap_spec {HPn: HP2} γi γs γw γsw l q tid :
histN ## N → is_arc P1 P2 N γi γs γw γsw l -∗
- {{{ (∃ t, strong_arc t q l γi γs γw γsw) ∗ P1 q }}} try_unwrap [ #l] in tid
+ {{{ (∃ t, strong_arc t q l γi γs γw γsw) ∗ P1 q }}} try_unwrap [ #l] @ tid; ⊤
{{{ (b : bool), RET #b ;
if b then P1 1 ∗ fake_arc l γi γs γw γsw
else (∃ t, strong_arc t q l γi γs γw γsw) ∗ P1 q }}}.
@@ -2380,7 +2380,7 @@ Section arc.
Lemma is_unique_spec {HPn: HP2} γi γs γw γsw l q tid :
histN ## N → is_arc P1 P2 N γi γs γw γsw l -∗
{{{ (∃ t, strong_arc t q l γi γs γw γsw) ∗ P1 q }}}
- is_unique [ #l] in tid
+ is_unique [ #l] @ tid; ⊤
{{{ (b : bool), RET #b ;
if b then l ↦ #1 ∗ (l >> 1) ↦ #1 ∗ P1 1
else (∃ t, strong_arc t q l γi γs γw γsw) ∗ P1 q }}}.
@@ -2605,7 +2605,7 @@ Section arc.
Lemma try_unwrap_full_spec {HPn : HP2} γi γs γw γsw l q tid :
histN ## N → is_arc P1 P2 N γi γs γw γsw l -∗
{{{ (∃ t, strong_arc t q l γi γs γw γsw) ∗ P1 q }}}
- try_unwrap_full [ #l] in tid
+ try_unwrap_full [ #l] @ tid; ⊤
{{{ (x : fin 3), RET #x ;
match x : nat with
(* No other reference : we get everything. *)
diff --git a/theories/lang/lock.v b/theories/lang/lock.v
index a4f987f3..f6d61187 100644
--- a/theories/lang/lock.v
+++ b/theories/lang/lock.v
@@ -111,7 +111,7 @@ Section proof.
Lemma try_acquire_spec N l γ κ R q tid E
(DISJ: histN ## N) (SUB1: ↑N ⊆ E) (SUB2 :↑lftN ⊆ E) (SUB3: ↑histN ⊆ E) :
⎡ lft_ctx ⎤ -∗
- {{{ lock_proto N l γ κ R ∗ (q).[κ] }}} try_acquire [ #l ] in tid @ E
+ {{{ lock_proto N l γ κ R ∗ (q).[κ] }}} try_acquire [ #l ] @ tid; E
{{{ b, RET #b; (if b is true then R else True) ∗ (q).[κ] }}}.
Proof.
iIntros "#LFT !#" (Φ) "[#Hproto Htok] HΦ". wp_rec.
@@ -144,7 +144,7 @@ Section proof.
(DISJ: histN ## N) (SUB1: ↑N ⊆ E) (SUB2 :↑lftN ⊆ E) (SUB3: ↑histN ⊆ E) :
⎡ lft_ctx ⎤ -∗
{{{ lock_proto N l γ κ R ∗ (q).[κ] }}}
- acquire [ #l ] in tid @ E
+ acquire [ #l ] @ tid; E
{{{ RET #☠; R ∗ (q).[κ] }}}.
Proof.
iIntros "#LFT !#" (Φ) "[#Hproto Htok] HΦ". iLöb as "IH". wp_rec.
@@ -158,7 +158,7 @@ Section proof.
(DISJ: histN ## N) (SUB1: ↑N ⊆ E) (SUB2 :↑lftN ⊆ E) (SUB3: ↑histN ⊆ E) :
⎡ lft_ctx ⎤ -∗
{{{ R ∗ lock_proto N l γ κ R ∗ (q).[κ] }}}
- release [ #l ] in tid @ E
+ release [ #l ] @ tid; E
{{{ RET #☠; (q).[κ] }}}.
Proof.
iIntros "#LFT !#" (Φ) "(HR & #Hproto & Htok) HΦ". wp_let.
diff --git a/theories/lang/memcpy.v b/theories/lang/memcpy.v
index aa3f254f..9920e71b 100644
--- a/theories/lang/memcpy.v
+++ b/theories/lang/memcpy.v
@@ -22,7 +22,7 @@ Notation "e1 <-{ n ',Σ' i } ! e2" :=
Lemma wp_memcpy `{!noprolG Σ} tid E l1 l2 vl1 vl2 q (n : Z):
↑histN ⊆ E → Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
{{{ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
- #l1 <-{n} !#l2 in tid @ E
+ #l1 <-{n} !#l2 @ tid; E
{{{ RET #☠; l1 ↦∗ vl2 ∗ l2 ↦∗{q} vl2 }}}.
Proof.
iIntros (? Hvl1 Hvl2 Φ) "(Hl1 & Hl2) HΦ".
diff --git a/theories/lang/spawn.v b/theories/lang/spawn.v
index a5e4797c..4c98f13b 100644
--- a/theories/lang/spawn.v
+++ b/theories/lang/spawn.v
@@ -86,8 +86,8 @@ Proof. solve_proper. Qed.
(** The main proofs. *)
Lemma spawn_spec Ψ e (f : val) tid :
IntoVal e f →
- {{{ ∀ γc γe c tid', finish_handle γc γe c Ψ -∗ WP f [ #c] in tid' {{ _, True }} }}}
- spawn [e] in tid
+ {{{ ∀ γc γe c tid', finish_handle γc γe c Ψ -∗ WP f [ #c] @ tid'; ⊤ {{ _, True }} }}}
+ spawn [e] @ tid; ⊤
{{{ γc γe c, RET #c; join_handle γc γe c Ψ }}}.
Proof.
iIntros (<- Φ) "Hf HΦ". rewrite /spawn /=.
@@ -107,7 +107,7 @@ Qed.
Lemma finish_spec Ψ c v γc γe tid
(DISJ1: (↑histN) ## (↑N : coPset)) (DISJ2: (↑escrowN) ## (↑N : coPset)) :
{{{ finish_handle γc γe c Ψ ∗ Ψ v }}}
- finish [ #c; v] in tid
+ finish [ #c; v] @ tid; ⊤
{{{ RET #☠; True }}}.
Proof.
iIntros (Φ) "[Hfin HΨ] HΦ".
@@ -127,7 +127,7 @@ Qed.
Lemma join_spec Ψ c γc γe tid
(DISJ1: (↑histN) ## (↑N : coPset)) (DISJ2: (↑escrowN) ## (↑N : coPset)) :
- {{{ join_handle γc γe c Ψ }}} join [ #c] in tid {{{ v, RET v; Ψ v }}}.
+ {{{ join_handle γc γe c Ψ }}} join [ #c] @ tid; ⊤ {{{ v, RET v; Ψ v }}}.
Proof.
iIntros (Φ) "H HΦ".
iDestruct "H" as (γi Ψ' t) "(R & (H†& He) & Hj & #HΨ')".
diff --git a/theories/lang/swap.v b/theories/lang/swap.v
index 30a59564..abef3ec3 100644
--- a/theories/lang/swap.v
+++ b/theories/lang/swap.v
@@ -13,7 +13,7 @@ Definition swap : val :=
Lemma wp_swap `{!noprolG Σ} tid E l1 l2 vl1 vl2 (n : Z):
↑histN ⊆ E → Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
{{{ l1 ↦∗ vl1 ∗ l2 ↦∗ vl2 }}}
- swap [ #l1; #l2; #n] in tid @ E
+ swap [ #l1; #l2; #n] @ tid; E
{{{ RET #☠; l1 ↦∗ vl2 ∗ l2 ↦∗ vl1 }}}.
Proof.
iIntros (? Hvl1 Hvl2 Φ) "(Hl1 & Hl2) HΦ".
diff --git a/theories/logic/gps.v b/theories/logic/gps.v
index 0581f1c6..fc832ef3 100644
--- a/theories/logic/gps.v
+++ b/theories/logic/gps.v
@@ -58,7 +58,7 @@ Lemma GPS_aSP_Read IP IPC l κ q R (o: memOrder) t s v γ tid E
IP true l γ t' s' v' ∗ R t' s' v') ∧
(IPC l γ t' s' v' ={E ∖ ↑N}=∗
IPC l γ t' s' v' ∗ R t' s' v'))) }}}
- Read o #l in tid @ E
+ Read o #l @ tid; E
{{{ t' s' v', RET v'; ⌜s ⊑ s' ∧ t ⊑ t'âŒ
∗ GPS_aSP_Reader IP IPC l κ t' s' v' γ ∗ (q).[κ]
∗ if decide (AcqRel ⊑ o)%stdpp then R t' s' v' else ▽{tid} R t' s' v' }}}.
@@ -80,7 +80,7 @@ Lemma GPS_aSP_SWWrite IP IPC l κ q R o t s s' v v' γ tid E
{{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_aSP_Writer IP IPC l κ t s v γ
∗ ▷ (if decide (AcqRel ⊑ o)%stdpp then WVS else △{tid} WVS)
∗ ▷ <obj> (IP true l γ t s v ={E ∖ ↑N}=∗ IPC l γ t s v ∗ R) }}}
- Write o #l v' in tid @ E
+ Write o #l v' @ tid; E
{{{ t', RET #☠; ⌜(t < t')%positive⌠∗ GPS_aSP_Writer IP IPC l κ t' s' v' γ
∗ (q).[κ] ∗ R }}}.
Proof.
@@ -102,7 +102,7 @@ Lemma GPS_aSP_SWWrite_rel IP IPC l κ q Q Q1 Q2 t s s' v v' γ tid E
|={E ∖ ↑N}=> (IP true l γ t' s' v' ∗ Q t'))%I in
{{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_aSP_Writer IP IPC l κ t s v γ
∗ ▷ WVS ∗ ▷ <obj> (IP true l γ t s v ={E ∖ ↑N}=∗ Q1 ∗ Q2) }}}
- #l <-ʳᵉˡ v' in tid @ E
+ #l <-ʳᵉˡ v' @ tid; E
{{{ t', RET #☠; ⌜(t < t')%positive⌠∗ GPS_aSP_Reader IP IPC l κ t' s' v' γ
∗ (q).[κ] ∗ Q t' }}}.
Proof.
@@ -142,7 +142,7 @@ Lemma GPS_aSP_SharedWriter_CAS_int_weak
∗ (▷ VSC)
∗ (if decide (AcqRel ⊑ ow)%stdpp then VS else △{tid} VS)
∗ (if decide (AcqRel ⊑ ow)%stdpp then P else △{tid} P) }}}
- CAS #l #vr vw orf or ow in tid @ E
+ CAS #l #vr vw orf or ow @ tid; E
{{{ (b: bool) t' s' (v': lit), RET #b;
(q).[κ] ∗ ⌜s ⊑ s'âŒ
∗ ( (⌜b = true ∧ v' = LitInt vr ∧ (t < t')%positiveâŒ
@@ -191,7 +191,7 @@ Lemma GPS_aSP_SharedWriter_CAS_int_strong
∗ (▷ VSC)
∗ (if decide (AcqRel ⊑ ow)%stdpp then VS else △{tid} VS)
∗ (if decide (AcqRel ⊑ ow)%stdpp then P else △{tid} P) }}}
- CAS #l #vr vw orf or ow in tid @ E
+ CAS #l #vr vw orf or ow @ tid; E
{{{ (b: bool) t' s' (v': lit), RET #b;
(q).[κ] ∗ ⌜s ⊑ s'âŒ
∗ ( (⌜b = true ∧ v' = LitInt vr ∧ (t < t')%positiveâŒ
@@ -282,7 +282,7 @@ Lemma GPS_aPP_Read IP l κ q R (o: memOrder) t s v γ tid E
IP false l γ t' s' v' ∗ R t' s' v') ∧
(IP true l γ t' s' v' ={E ∖ ↑N}=∗
IP true l γ t' s' v' ∗ R t' s' v'))) }}}
- Read o #l in tid @ E
+ Read o #l @ tid; E
{{{ t' s' v', RET v'; ⌜s ⊑ s' ∧ t ⊑ t'⌠∗ GPS_aPP IP l κ t' s' v' γ ∗ (q).[κ]
∗ if decide (AcqRel ⊑ o)%stdpp then R t' s' v' else ▽{tid} R t' s' v' }}}.
Proof.
@@ -304,7 +304,7 @@ Lemma GPS_aPP_Write IP l κ q (o: memOrder) t v v' s s' γ tid E
GPS_PP_Local l t' s' v' γ ={E ∖ ↑N}=∗ IP true l γ t' s' v')%I in
{{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_aPP IP l κ t s v γ
∗ ▷ if decide (AcqRel ⊑ o)%stdpp then VS else △{tid} VS }}}
- Write o #l v' in tid @ E
+ Write o #l v' @ tid; E
{{{ t', RET #☠; GPS_aPP IP l κ t' s' v' γ ∗ (q).[κ] }}}.
Proof.
iIntros (VS Φ) "(#LFT & Htok & #[Hlc Hshr] & VS) Post".
@@ -341,7 +341,7 @@ Lemma GPS_aPP_CAS_int_simple IP l κ q t s v (vr: Z) (vw: val) orf or ow γ
∗ ▷ VSC
∗ (if decide (AcqRel ⊑ ow)%stdpp then VS else △{tid} VS)
∗ (if decide (AcqRel ⊑ ow)%stdpp then P else △{tid} P ) }}}
- CAS #l #vr vw orf or ow in tid @ E
+ CAS #l #vr vw orf or ow @ tid; E
{{{ (b: bool) t' s' (v': lit), RET #b;
(q).[κ] ∗ ⌜s ⊑ s'âŒ
∗ ( (⌜b = true ∧ v' = LitInt vr ∧ (t < t')%positiveâŒ
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index d6923a31..6ce090e3 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -25,7 +25,7 @@ Section cont_context.
let '(k â—cont(L, T)) := x in
(∀ args, na_own tid top -∗
llctx_interp qmax L -∗ tctx_interp tid (T args) -∗
- WP k (base.of_val <$> (args : list _)) in tid
+ WP k (base.of_val <$> (args : list _)) @ tid; ⊤
{{ _, cont_postcondition }})%I.
Definition cctx_interp (tid : type.thread_id) (qmax: Qp) (C : cctx) : vProp Σ :=
(∀ (x : cctx_elt), ⌜x ∈ C⌠-∗ cctx_elt_interp tid qmax x)%I.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index efef50ee..3faa1a71 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -248,8 +248,8 @@ Section typing.
tctx_elt_interp tid y) -∗
(∀ ret, na_own tid top -∗ llctx_interp_noend qmax L qL -∗ qκs.[lft_intersect_list κs] -∗
(box (fp x).(fp_ty)).(ty_own) tid [ret] -∗
- WP k [of_val ret] in tid {{ _, cont_postcondition }}) -∗
- WP (call: p ps → k) in tid {{ _, cont_postcondition }}.
+ WP k [of_val ret] @ tid; ⊤ {{ _, cont_postcondition }}) -∗
+ WP (call: p ps → k) @ tid; ⊤ {{ _, cont_postcondition }}.
Proof.
iIntros (HE [k' <-]) "#LFT #HE Htl HL Hκs Hf Hargs Hk".
wp_apply (wp_hasty with "Hf"); [done|]. iIntros (v) "% Hf".
@@ -318,8 +318,8 @@ Section typing.
tctx_elt_interp tid y) -∗
(∀ ret, na_own tid top -∗ qκs.[lft_intersect_list κs] -∗
(box (fp x).(fp_ty)).(ty_own) tid [ret] -∗
- WP k [of_val ret] in tid {{ _, cont_postcondition }}) -∗
- WP (call: f ps → k) in tid {{ _, cont_postcondition }}.
+ WP k [of_val ret] @ tid; ⊤ {{ _, cont_postcondition }}) -∗
+ WP (call: f ps → k) @ tid; ⊤ {{ _, cont_postcondition }}.
Proof.
iIntros (HE Hk') "#LFT #HE Htl Hκs Hf Hargs Hk". rewrite -tctx_hasty_val.
iApply (type_call_iris' with "LFT HE Htl [] Hκs Hf Hargs [Hk]"); [done..| |].
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index f23113f4..d3c5b194 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -248,7 +248,7 @@ Section code.
Lemma rc_check_unique ty F tid (l : loc) :
↑rc_invN ⊆ F →
{{{ na_own tid F ∗ ty_own (rc ty) tid [ #l ] }}}
- !#l in tid
+ !#l @ tid; ⊤
{{{ strong, RET #(Zpos strong); l ↦ #(Zpos strong) ∗
(((⌜strong = 1%positive⌠∗
(∃ weak : Z, (l +ₗ 1) ↦ #weak ∗
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index d7c12c47..999858e7 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -14,7 +14,7 @@ Section typing.
(e : expr) : vPropI Σ :=
(∀ tid (qmax : Qp), ⎡lft_ctx⎤ -∗ elctx_interp E -∗ na_own tid ⊤ -∗ llctx_interp qmax L -∗
cctx_interp tid qmax C -∗ tctx_interp tid T -∗
- WP e in tid {{ _, cont_postcondition }})%I.
+ WP e @ tid; ⊤ {{ _, cont_postcondition }})%I.
Global Arguments typed_body _ _ _ _ _%E.
Global Instance typed_body_llctx_permut E :
@@ -62,7 +62,7 @@ Section typing.
(T1 : tctx) (e : expr) (T2 : val → tctx) : vPropI Σ :=
(∀ tid qmax, ⎡lft_ctx⎤ -∗ elctx_interp E -∗ na_own tid ⊤ -∗
llctx_interp qmax L -∗ tctx_interp tid T1 -∗
- WP e in tid {{ v, na_own tid ⊤ ∗
+ WP e @ tid; ⊤ {{ v, na_own tid ⊤ ∗
llctx_interp qmax L ∗ tctx_interp tid (T2 v) }})%I.
Global Arguments typed_instruction _ _ _ _%E _.
@@ -306,7 +306,7 @@ Section typing_rules.
typed_write E L ty1 ty ty1' -∗ typed_read E L ty2 ty ty2' -∗
{{{ ⎡lft_ctx⎤ ∗ elctx_interp E ∗ na_own tid ⊤ ∗ llctx_interp_noend qmax L qL ∗
tctx_elt_interp tid (p1 ◠ty1) ∗ tctx_elt_interp tid (p2 ◠ty2) }}}
- (p1 <-{n} !p2) in tid
+ (p1 <-{n} !p2) @ tid; ⊤
{{{ RET #☠; na_own tid ⊤ ∗ llctx_interp_noend qmax L qL ∗
tctx_elt_interp tid (p1 ◠ty1') ∗ tctx_elt_interp tid (p2 ◠ty2') }}}.
Proof.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index f45b11d1..2cf6c9db 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -6,6 +6,8 @@ Set Default Proof Using "Type".
Definition path := expr.
Bind Scope expr_scope with path.
+Global Instance wp_path `{!noprolG Σ} : Wp (vPropI Σ) path val thread_id := wp'.
+
(* TODO: Consider making this a pair of a path and the rest. We could
then e.g. formulate tctx_elt_hasty_path more generally. *)
Inductive tctx_elt `{!typeG Σ} : Type :=
@@ -37,7 +39,7 @@ Section type_context.
Proof. destruct v. done. simpl. rewrite (decide_True_pi _). done. Qed.
Lemma wp_eval_path E tid p v (SUB : ↑histN ⊆ E) :
- eval_path p = Some v → ⊢ WP p in tid @ E {{ v', ⌜v' = v⌠}}.
+ eval_path p = Some v → ⊢ WP p @ tid; E {{ v', ⌜v' = v⌠}}.
Proof.
revert v; induction p; intros v; cbn -[to_val];
try (intros <-%of_to_val; by iApply wp_value).
@@ -99,7 +101,7 @@ Section type_context.
Lemma wp_hasty E tid p ty Φ (SUB : ↑histN ⊆ E) :
tctx_elt_interp tid (p ◠ty) -∗
(∀ v, ⌜eval_path p = Some v⌠-∗ ty.(ty_own) tid [v] -∗ Φ v) -∗
- WP p in tid @ E {{ Φ }}.
+ WP p @ tid; E {{ Φ }}.
Proof.
iIntros "Hty HΦ". iDestruct "Hty" as (v) "[% Hown]".
iApply (wp_wand with "[]"). { by iApply wp_eval_path. }
--
GitLab