Skip to content
Snippets Groups Projects
Commit 3a4b14b9 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Merge current Iris trunk.

parent 43555090
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 310 additions and 311 deletions
iris @ 5e3835f8
Compare bb5e21f2...5e3835f8
Subproject commit bb5e21f21fd1b5be820005eb53750f84270ab4ec
Subproject commit 5e3835f807768f42f77b6cc33bca039b8274a586
theories/heap.v
+ 83
− 84
View file @ 3a4b14b9
This diff is collapsed.
theories/lifetime.v
+ 51
− 51
View file @ 3a4b14b9
......@@ -38,7 +38,7 @@ Section defs.
own toks_name (◯ (Cinl <$> omap (Qp_nat_mul q) κ)).
Definition lft_dead (κ : lifetime) : iProp Σ :=
(∃ Λ, ■ (∃ n, κ !! Λ = Some (S n)) ★
(∃ Λ, ■ (∃ n, κ !! Λ = Some (S n)) ∗
own toks_name (◯ {[ Λ := Cinr () ]}))%I.
End defs.
......@@ -53,7 +53,7 @@ Parameter lft_idx_borrow_persist: ∀ `{lifetimeG Σ} (i : gname), iProp Σ.
Parameter lft_idx_borrow_own : ∀ `{lifetimeG Σ} (i : gname), iProp Σ.
Definition lft_borrow `{lifetimeG Σ} (κ : lifetime) (P : iProp Σ) : iProp Σ :=
(∃ i, lft_idx_borrow κ i P ★ lft_idx_borrow_own i)%I.
(∃ i, lft_idx_borrow κ i P ∗ lft_idx_borrow_own i)%I.
(*** Notations *)
......@@ -104,7 +104,7 @@ Section lft.
Proof. solve_proper. Qed.
(** Basic rules about lifetimes *)
Lemma lft_own_op q κ1 κ2 : q.[κ1] ★ q.[κ2] ⊣⊢ q.[κ1 ⋅ κ2].
Lemma lft_own_op q κ1 κ2 : q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⋅ κ2].
Proof.
rewrite /lft_own -own_op. f_equiv. constructor. done. move=>Λ /=.
rewrite lookup_op !lookup_fmap !lookup_omap lookup_op.
......@@ -126,7 +126,7 @@ Section lft.
Qed.
Lemma lft_own_frac_op κ q q':
(q + q').[κ] ⊣⊢ q.[κ] ★ q'.[κ].
(q + q').[κ] ⊣⊢ q.[κ] ∗ q'.[κ].
Proof.
rewrite /lft_own -own_op -auth_frag_op. f_equiv. constructor. done. simpl.
intros Λ. rewrite lookup_op !lookup_fmap !lookup_omap. apply reflexive_eq.
......@@ -138,33 +138,33 @@ Section lft.
(* FIXME : merging begin and end. *)
Axiom lft_create :
∀ `(nclose lftN ⊆ E), True ={E}=★ ∃ κ, 1.[κ] ★ □ (1.[κ] ={⊤,∅}▷=★ [†κ]).
∀ `(nclose lftN ⊆ E), True ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={⊤,∅}▷=∗ [†κ]).
Axiom lft_idx_borrow_persist_upd :
∀ `(nclose lftN ⊆ E) i, lft_idx_borrow_own i ={E}=★ lft_idx_borrow_persist i.
∀ `(nclose lftN ⊆ E) i, lft_idx_borrow_own i ={E}=∗ lft_idx_borrow_persist i.
Axiom lft_idx_borrow_own_acc :
∀ `(nclose lftN ⊆ E) q κ i P,
lft_idx_borrow κ i P ⊢ lft_idx_borrow_own i ★ q.[κ] ={E}=★ ▷ P ★
(▷ P ={E}=★ lft_idx_borrow_own i ★ q.[κ]).
lft_idx_borrow κ i P ⊢ lft_idx_borrow_own i ∗ q.[κ] ={E}=∗ ▷ P ∗
(▷ P ={E}=∗ lft_idx_borrow_own i ∗ q.[κ]).
Axiom lft_idx_borrow_persist_acc :
∀ `(nclose lftN ⊆ E) q κ i P,
lft_idx_borrow κ i P ⊢ lft_idx_borrow_persist i -★
q.[κ] ={E,E∖lftN}=★ ▷ P ★ (▷ P ={E∖lftN,E}=★ q.[κ]).
lft_idx_borrow κ i P ⊢ lft_idx_borrow_persist i -∗
q.[κ] ={E,E∖lftN}=∗ ▷ P ∗ (▷ P ={E∖lftN,E}=∗ q.[κ]).
(** Basic borrows *)
Axiom lft_borrow_create :
∀ `(nclose lftN ⊆ E) κ P, ▷ P ={E}=★ &{κ} P ★ κ ∋ ▷ P.
∀ `(nclose lftN ⊆ E) κ P, ▷ P ={E}=∗ &{κ} P ∗ κ ∋ ▷ P.
Axiom lft_borrow_split :
∀ `(nclose lftN ⊆ E) κ P Q, &{κ}(P ★ Q) ={E}=★ &{κ}P ★ &{κ}Q.
∀ `(nclose lftN ⊆ E) κ P Q, &{κ}(P ∗ Q) ={E}=∗ &{κ}P ∗ &{κ}Q.
Axiom lft_borrow_combine :
∀ `(nclose lftN ⊆ E) κ P Q, &{κ}P ★ &{κ}Q ={E}=★ &{κ}(P ★ Q).
∀ `(nclose lftN ⊆ E) κ P Q, &{κ}P ∗ &{κ}Q ={E}=∗ &{κ}(P ∗ Q).
Axiom lft_borrow_acc_strong :
∀ `(nclose lftN ⊆ E) q κ P,
&{κ}P ⊢ q.[κ] ={E}=★ ▷ P ★
∀ Q, ▷ Q ★ ▷([†κ] ★ ▷Q ={⊤ ∖ nclose lftN}=★ ▷ P) ={E}=★ &{κ}Q ★ q.[κ].
&{κ}P ⊢ q.[κ] ={E}=∗ ▷ P ∗
∀ Q, ▷ Q ∗ ▷([†κ] ∗ ▷Q ={⊤ ∖ nclose lftN}=∗ ▷ P) ={E}=∗ &{κ}Q ∗ q.[κ].
Axiom lft_reborrow_static :
∀ `(nclose lftN ⊆ E) κ κ' P, κ ≼ κ' →
&{κ}P ={E}=★ &{κ'}P ★ κ' ∋ &{κ}P.
&{κ}P ={E}=∗ &{κ'}P ∗ κ' ∋ &{κ}P.
(* FIXME : the document says that we need κ tokens here. Why so?
Why not κ' tokens also?*)
Axiom lft_borrow_unnest :
......@@ -172,16 +172,16 @@ Section lft.
(** Extraction *)
Axiom lft_extract_split :
∀ `(nclose lftN ⊆ E) κ P Q, κ ∋ (P ★ Q) ={E}=★ κ ∋ P ★ κ ∋ Q.
∀ `(nclose lftN ⊆ E) κ P Q, κ ∋ (P ∗ Q) ={E}=∗ κ ∋ P ∗ κ ∋ Q.
Axiom lft_extract_combine :
∀ `(nclose lftN ⊆ E) κ P Q, κ ∋ P ★ κ ∋ Q ={E}=★ κ ∋ (P ★ Q).
Axiom lft_extract_out : ∀ `(nclose lftN ⊆ E) κ P, [†κ] ⊢ κ ∋ P ={E}=★ P.
Axiom lft_extract_contravar : ∀ κ P Q, (P -★ Q) ★ κ ∋ P ⊢ κ ∋ Q.
∀ `(nclose lftN ⊆ E) κ P Q, κ ∋ P ∗ κ ∋ Q ={E}=∗ κ ∋ (P ∗ Q).
Axiom lft_extract_out : ∀ `(nclose lftN ⊆ E) κ P, [†κ] ⊢ κ ∋ P ={E}=∗ P.
Axiom lft_extract_contravar : ∀ κ P Q, (P -∗ Q) ∗ κ ∋ P ⊢ κ ∋ Q.
Axiom lft_extract_mono : ∀ κ κ' P, κ' ≼ κ → κ ∋ P ⊢ κ' ∋ P.
(*** Derived lemmas *)
Lemma lft_own_dead q κ : q.[κ] ★ [† κ] ⊢ False.
Lemma lft_own_dead q κ : q.[κ] ∗ [† κ] ⊢ False.
Proof.
rewrite /lft_own /lft_dead.
iIntros "[Hl Hr]". iDestruct "Hr" as (Λ) "[HΛ Hr]".
......@@ -191,13 +191,13 @@ Section lft.
by rewrite lookup_op lookup_singleton lookup_fmap lookup_omap HΛ.
Qed.
Lemma lft_own_static q : True ==★ q.[static].
Lemma lft_own_static q : True ==∗ q.[static].
Proof.
rewrite /lft_own /static omap_empty fmap_empty.
apply (own_empty (A:=lft_tokUR) toks_name).
Qed.
Lemma lft_own_split κ q : q.[κ] ⊣⊢ (q/2).[κ] ★ (q/2).[κ].
Lemma lft_own_split κ q : q.[κ] ⊣⊢ (q/2).[κ] ∗ (q/2).[κ].
Proof. by rewrite -lft_own_frac_op Qp_div_2. Qed.
Global Instance into_and_lft_own_half κ q :
......@@ -229,7 +229,7 @@ Section lft.
Proof. by rewrite /FromSep lft_own_op. Qed.
Lemma lft_borrow_acc E q κ P : nclose lftN ⊆ E →
&{κ}P ⊢ q.[κ] ={E}=★ ▷ P ★ (▷ P ={E}=★ &{κ}P ★ q.[κ]).
&{κ}P ⊢ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
Proof.
iIntros (?) "HP Htok".
iMod (lft_borrow_acc_strong with "HP Htok") as "[HP Hclose]". done.
......@@ -238,7 +238,7 @@ Section lft.
Lemma lft_borrow_exists {A} `(nclose lftN ⊆ E)
κ q (Φ : A → iProp Σ) {_:Inhabited A}:
&{κ}(∃ x, Φ x) ⊢ q.[κ] ={E}=★ ∃ x, &{κ}Φ x ★ q.[κ].
&{κ}(∃ x, Φ x) ⊢ q.[κ] ={E}=∗ ∃ x, &{κ}Φ x ∗ q.[κ].
Proof.
iIntros "Hb Htok".
iMod (lft_borrow_acc_strong with "Hb Htok") as "[HΦ Hob]". done.
......@@ -246,14 +246,14 @@ Section lft.
Qed.
Lemma lft_borrow_or `(nclose lftN ⊆ E) κ q P Q:
&{κ}(P ∨ Q) ⊢ q.[κ] ={E}=★ (&{κ}P ∨ &{κ}Q) ★ q.[κ].
&{κ}(P ∨ Q) ⊢ q.[κ] ={E}=∗ (&{κ}P ∨ &{κ}Q) ∗ q.[κ].
Proof.
iIntros "H Htok". rewrite uPred.or_alt.
iMod (lft_borrow_exists with "H Htok") as ([]) "[H $]"; auto.
Qed.
Lemma lft_borrow_persistent `(nclose lftN ⊆ E) `{PersistentP _ P} κ q:
&{κ}P ⊢ q.[κ] ={E}=★ ▷ P ★ q.[κ].
&{κ}P ⊢ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
Proof.
iIntros "Hb Htok".
iMod (lft_borrow_acc with "Hb Htok") as "[#HP Hob]". done.
......@@ -267,7 +267,7 @@ Typeclasses Opaque lft_borrow.
(*** Inclusion and shortening. *)
Definition lft_incl `{lifetimeG Σ} κ κ' : iProp Σ :=
(□ ∀ q, q.[κ] ={lftN}=★ ∃ q', q'.[κ'] ★ (q'.[κ'] ={lftN}=★ q.[κ]))%I.
(□ ∀ q, q.[κ] ={lftN}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={lftN}=∗ q.[κ]))%I.
Infix "⊑" := lft_incl (at level 60, right associativity) : C_scope.
......@@ -277,7 +277,7 @@ Section incl.
Global Instance lft_incl_persistent κ κ': PersistentP (κ ⊑ κ') := _.
Lemma lft_incl_acc `(nclose lftN ⊆ E) κ κ' q:
κ ⊑ κ' ⊢ q.[κ] ={E}=★ ∃ q', q'.[κ'] ★ (q'.[κ'] ={E}=★ q.[κ]).
κ ⊑ κ' ⊢ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
Proof.
iIntros "#H Hq". iApply fupd_mask_mono. eassumption.
iMod ("H" with "*Hq") as (q') "[Hq' Hclose]". iExists q'.
......@@ -293,7 +293,7 @@ Section incl.
Lemma lft_incl_relf κ : True ⊢ κ ⊑ κ.
Proof. by apply lft_le_incl. Qed.
Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' ★ κ' ⊑ κ'' ⊢ κ ⊑ κ''.
Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' ∗ κ' ⊑ κ'' ⊢ κ ⊑ κ''.
Proof.
unfold lft_incl. iIntros "[#H1 #H2]!#*Hκ".
iMod ("H1" with "*Hκ") as (q') "[Hκ' Hclose]".
......@@ -303,15 +303,15 @@ Section incl.
Qed.
Axiom lft_idx_borrow_shorten :
∀ κ κ' i P, κ ⊑ κ' ⊢ lft_idx_borrow κ' i P -★ lft_idx_borrow κ i P.
∀ κ κ' i P, κ ⊑ κ' ⊢ lft_idx_borrow κ' i P -∗ lft_idx_borrow κ i P.
Lemma lft_borrow_shorten κ κ' P: κ ⊑ κ' ⊢ &{κ'}P -★ &{κ}P.
Lemma lft_borrow_shorten κ κ' P: κ ⊑ κ' ⊢ &{κ'}P -∗ &{κ}P.
Proof.
iIntros "H⊑ H". unfold lft_borrow. iDestruct "H" as (i) "[??]".
iExists i. iFrame. by iApply (lft_idx_borrow_shorten with "H⊑").
Qed.
Lemma lft_incl_lb κ κ' κ'' : κ ⊑ κ' ★ κ ⊑ κ'' ⊢ κ ⊑ κ' ⋅ κ''.
Lemma lft_incl_lb κ κ' κ'' : κ ⊑ κ' ∗ κ ⊑ κ'' ⊢ κ ⊑ κ' ⋅ κ''.
Proof.
iIntros "[#H⊑1 #H⊑2]!#". iIntros (q). iIntros "[Hκ'1 Hκ'2]".
iMod ("H⊑1" with "*Hκ'1") as (q') "[Hκ' Hclose']".
......@@ -331,12 +331,12 @@ Section incl.
Qed.
Lemma lft_reborrow `(nclose lftN ⊆ E) P κ κ':
κ' ⊑ κ ⊢ &{κ}P ={E}=★ &{κ'}P ★ κ' ∋ &{κ}P.
κ' ⊑ κ ⊢ &{κ}P ={E}=∗ &{κ'}P ∗ κ' ∋ &{κ}P.
Proof.
iIntros "#H⊑ HP". iMod (lft_reborrow_static with "HP") as "[Hκ' H∋]".
done. by exists κ'.
iDestruct (lft_borrow_shorten with "[H⊑] Hκ'") as "$".
{ iApply lft_incl_lb. iSplit. done. iApply lft_incl_relf. }
{ iApply lft_incl_lb. iSplit. done. iIntros "!#*". iApply lft_incl_relf. }
iApply lft_extract_mono; last by iFrame; auto. exists κ. by rewrite comm.
Qed.
......@@ -348,7 +348,7 @@ Typeclasses Opaque lft_incl.
(** Shared borrows *)
Definition lft_shr_borrow `{lifetimeG Σ} κ (P : iProp Σ) :=
(∃ i, lft_idx_borrow κ i P ★ lft_idx_borrow_persist i)%I.
(∃ i, lft_idx_borrow κ i P ∗ lft_idx_borrow_persist i)%I.
Notation "&shr{ κ } P" := (lft_shr_borrow κ P)
(format "&shr{ κ } P", at level 20, right associativity) : uPred_scope.
......@@ -360,21 +360,21 @@ Section shared_borrows.
Proof. solve_proper. Qed.
Global Instance lft_shr_borrow_persistent : PersistentP (&shr{κ} P) := _.
Lemma lft_borrow_share `(nclose lftN ⊆ E) κ : &{κ}P ={E}=★ &shr{κ}P.
Lemma lft_borrow_share `(nclose lftN ⊆ E) κ : &{κ}P ={E}=∗ &shr{κ}P.
Proof.
iIntros "HP". unfold lft_borrow. iDestruct "HP" as (i) "(#?&Hown)".
iExists i. iMod (lft_idx_borrow_persist_upd with "[$Hown]"). done. by auto.
Qed.
Lemma lft_shr_borrow_acc `(nclose lftN ⊆ E) q κ :
&shr{κ}P ⊢ q.[κ] ={E,E∖lftN}=★ ▷P ★ (▷P ={E∖lftN,E}=★ q.[κ]).
&shr{κ}P ⊢ q.[κ] ={E,E∖lftN}=∗ ▷P ∗ (▷P ={E∖lftN,E}=∗ q.[κ]).
Proof.
iIntros "#HP Hκ". iDestruct "HP" as (i) "(#Hidx&#Hpers)".
iMod (lft_idx_borrow_persist_acc with "Hidx Hpers Hκ") as "[$H]". done.
iApply "H".
Qed.
Lemma lft_shr_borrow_shorten κ κ': κ ⊑ κ' ⊢ &shr{κ'}P -★ &shr{κ}P.
Lemma lft_shr_borrow_shorten κ κ': κ ⊑ κ' ⊢ &shr{κ'}P -∗ &shr{κ}P.
Proof.
iIntros "#H⊑ H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
by iApply (lft_idx_borrow_shorten with "H⊑").
......@@ -386,8 +386,8 @@ Typeclasses Opaque lft_shr_borrow.
(** Fractured borrows *)
Definition lft_frac_borrow `{lifetimeG Σ} κ (Φ : Qp → iProp Σ) :=
(∃ γ κ', κ ⊑ κ' ★ &shr{κ'} ∃ q, Φ q ★ own γ q ★
(q = 1%Qp ∨ ∃ q', (q + q')%Qp = 1%Qp ★ q'.[κ']))%I.
(∃ γ κ', κ ⊑ κ' ∗ &shr{κ'} ∃ q, Φ q ∗ own γ q ∗
(q = 1%Qp ∨ ∃ q', (q + q')%Qp = 1%Qp ∗ q'.[κ']))%I.
Notation "&frac{ κ } P" := (lft_frac_borrow κ P)
(format "&frac{ κ } P", at level 20, right associativity) : uPred_scope.
......@@ -396,7 +396,7 @@ Section frac_borrow.
Context `{lifetimeG Σ}.
Lemma lft_borrow_fracture `(nclose lftN ⊆ E) q κ φ:
&{κ}(φ 1%Qp) ★ q.[κ] ={E}=★ &frac{κ}φ ★ q.[κ].
&{κ}(φ 1%Qp) ∗ q.[κ] ={E}=∗ &frac{κ}φ ∗ q.[κ].
Proof.
iIntros "[Hφ Hκ]". iMod (own_alloc 1%Qp) as (γ) "?". done.
iMod (lft_borrow_acc_strong with "Hφ Hκ") as "[Hφ Hclose]". done.
......@@ -410,8 +410,8 @@ Section frac_borrow.
Qed.
Lemma lft_frac_borrow_acc `(nclose lftN ⊆ E) q κ φ:
□ (∀ q1 q2, φ (q1+q2)%Qp ↔ φ q1 ★ φ q2) ⊢
&frac{κ}φ -★ q.[κ] ={E}=★ ∃ q', ▷ φ q' ★ (▷ φ q' ={E}=★ q.[κ]).
□ (∀ q1 q2, φ (q1+q2)%Qp ↔ φ q1 ∗ φ q2) ⊢
&frac{κ}φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ φ q' ∗ (▷ φ q' ={E}=∗ q.[κ]).
Proof.
iIntros "#Hφ Hfrac Hκ". unfold lft_frac_borrow.
iDestruct "Hfrac" as (γ κ') "#[#Hκκ' Hshr]".
......@@ -420,7 +420,7 @@ Section frac_borrow.
iDestruct "H" as (qφ) "(Hφqφ & >Hown & Hq)".
destruct (Qp_lower_bound (qκ'/2) (qφ/2)) as (qq & qκ'0 & qφ0 & Hqκ' & Hqφ).
iExists qq.
iAssert (▷ φ qq ★ ▷ φ (qφ0 + qφ / 2))%Qp%I with "[Hφqφ]" as "[$ Hqφ]".
iAssert (▷ φ qq ∗ ▷ φ (qφ0 + qφ / 2))%Qp%I with "[Hφqφ]" as "[$ Hqφ]".
{ iNext. rewrite -{1}(Qp_div_2 qφ) {1}Hqφ. iApply "Hφ". by rewrite assoc. }
rewrite -{1}(Qp_div_2 qφ) {1}Hqφ -assoc {1}Hqκ'.
iDestruct "Hκ2" as "[Hκq Hκqκ0]". iDestruct "Hown" as "[Hownq Hown]".
......@@ -455,7 +455,7 @@ Section frac_borrow.
iApply "Hclose". rewrite -{2}(Qp_div_2 qκ') {2}Hqκ' !lft_own_frac_op. by iFrame.
Qed.
Lemma lft_frac_borrow_shorten κ κ' φ: κ ⊑ κ' ⊢ &frac{κ'}φ -★ &frac{κ}φ.
Lemma lft_frac_borrow_shorten κ κ' φ: κ ⊑ κ' ⊢ &frac{κ'}φ -∗ &frac{κ}φ.
Proof.
iIntros "Hκκ' H". iDestruct "H" as (γ κ0) "[H⊑?]". iExists γ, κ0. iFrame.
iApply lft_incl_trans. iFrame.
......@@ -469,7 +469,7 @@ Typeclasses Opaque lft_frac_borrow.
Definition lft_tl_borrow `{lifetimeG Σ, thread_localG Σ}
(κ : lifetime) (tid : thread_id) (N : namespace) (P : iProp Σ) :=
(∃ i, lft_idx_borrow κ i P ★ tl_inv tid N (lft_idx_borrow_own i))%I.
(∃ i, lft_idx_borrow κ i P ∗ tl_inv tid N (lft_idx_borrow_own i))%I.
Notation "&tl{ κ | tid | N } P" := (lft_tl_borrow κ tid N P)
(format "&tl{ κ | tid | N } P", at level 20, right associativity) : uPred_scope.
......@@ -485,7 +485,7 @@ Section tl_borrows.
intros P1 P2 EQ. apply uPred.exist_proper. intros i. by rewrite EQ.
Qed.
Lemma lft_borrow_tl κ `(nclose lftN ⊆ E): &{κ}P ={E}=★ &tl{κ|tid|N}P.
Lemma lft_borrow_tl κ `(nclose lftN ⊆ E): &{κ}P ={E}=∗ &tl{κ|tid|N}P.
Proof.
iIntros "HP". unfold lft_borrow. iDestruct "HP" as (i) "[#? Hown]".
iExists i. iFrame "#". iApply (tl_inv_alloc tid E N with "[Hown]"). auto.
......@@ -493,8 +493,8 @@ Section tl_borrows.
Lemma lft_tl_borrow_acc q κ E F :
nclose lftN ⊆ E → nclose tlN ⊆ E → nclose N ⊆ F →
&tl{κ|tid|N}P ⊢ q.[κ] ★ tl_own tid F ={E}=★ ▷P ★ tl_own tid (F ∖ N) ★
(▷P ★ tl_own tid (F ∖ N) ={E}=★ q.[κ] ★ tl_own tid F).
&tl{κ|tid|N}P ⊢ q.[κ] ∗ tl_own tid F ={E}=∗ ▷P ∗ tl_own tid (F ∖ N) ∗
(▷P ∗ tl_own tid (F ∖ N) ={E}=∗ q.[κ] ∗ tl_own tid F).
Proof.
iIntros (???) "#HP[Hκ Htlown]".
iDestruct "HP" as (i) "(#Hpers&#Hinv)".
......@@ -504,7 +504,7 @@ Section tl_borrows.
iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame.
Qed.
Lemma lft_tl_borrow_shorten κ κ': κ ⊑ κ' ⊢ &tl{κ'|tid|N}P -★ &tl{κ|tid|N}P.
Lemma lft_tl_borrow_shorten κ κ': κ ⊑ κ' ⊢ &tl{κ'|tid|N}P -∗ &tl{κ|tid|N}P.
Proof.
iIntros "Hκκ' H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
iApply (lft_idx_borrow_shorten with "Hκκ' H").
......
theories/lifting.v
+ 29
− 31
View file @ 3a4b14b9
......@@ -25,12 +25,12 @@ Proof. exact: weakestpre.wp_bind. Qed.
Lemma wp_alloc_pst E σ n:
0 < n →
{{{ ▷ ownP σ }}} Alloc (Lit $ LitInt n) @ E
{{{ l σ'; LitV $ LitLoc l,
■ (∀ m, σ !! (shift_loc l m) = None) ★
■ (∃ vl, n = length vl ∧ init_mem l vl σ = σ') ★
{{{ l σ', RET LitV $ LitLoc l;
■ (∀ m, σ !! (shift_loc l m) = None) ∗
■ (∃ vl, n = length vl ∧ init_mem l vl σ = σ') ∗
ownP σ' }}}.
Proof.
iIntros (? Φ) "[HP HΦ]". iApply (wp_lift_atomic_head_step _ σ); eauto.
iIntros (? Φ) "HP HΦ". iApply (wp_lift_atomic_head_step _ σ); eauto.
iFrame "HP". iNext. iIntros (v2 σ2 ef) "[% HP]". inv_head_step.
rewrite big_sepL_nil right_id. by iApply "HΦ"; iFrame; eauto.
Qed.
......@@ -39,36 +39,36 @@ Lemma wp_free_pst E σ l n :
0 < n →
(∀ m, is_Some (σ !! (shift_loc l m)) ↔ (0 ≤ m < n)) →
{{{ ▷ ownP σ }}} Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E
{{{ ; LitV $ LitUnit, ownP (free_mem l (Z.to_nat n) σ) }}}.
{{{ RET LitV $ LitUnit; ownP (free_mem l (Z.to_nat n) σ) }}}.
Proof.
iIntros (???) "[HP HΦ]". iApply (wp_lift_atomic_head_step _ σ); eauto.
iIntros (???) "HP HΦ". iApply (wp_lift_atomic_head_step _ σ); eauto.
iFrame "HP". iNext. iIntros (v2 σ2 ef) "[% HP]". inv_head_step.
rewrite big_sepL_nil right_id. by iApply "HΦ".
Qed.
Lemma wp_read_sc_pst E σ l n v :
σ !! l = Some (RSt n, v) →
{{{ ▷ ownP σ }}} Read ScOrd (Lit $ LitLoc l) @ E {{{ ; v, ownP σ }}}.
{{{ ▷ ownP σ }}} Read ScOrd (Lit $ LitLoc l) @ E {{{ RET v; ownP σ }}}.
Proof.
iIntros (??) "[?HΦ]". iApply wp_lift_atomic_det_head_step; eauto.
iIntros (??) "?HΦ". iApply wp_lift_atomic_det_head_step; eauto.
by intros; inv_head_step; eauto using to_of_val.
rewrite big_sepL_nil right_id; iFrame. iNext. iIntros "?!>". by iApply "HΦ".
rewrite big_sepL_nil right_id; iFrame.
Qed.
Lemma wp_read_na2_pst E σ l n v :
σ !! l = Some(RSt $ S n, v) →
{{{ ▷ ownP σ }}} Read Na2Ord (Lit $ LitLoc l) @ E
{{{ ; v, ownP (<[l:=(RSt n, v)]>σ) }}}.
{{{ RET v; ownP (<[l:=(RSt n, v)]>σ) }}}.
Proof.
iIntros (??) "[?HΦ]". iApply wp_lift_atomic_det_head_step; eauto.
iIntros (??) "?HΦ". iApply wp_lift_atomic_det_head_step; eauto.
by intros; inv_head_step; eauto using to_of_val.
rewrite big_sepL_nil right_id; iFrame. iNext. iIntros "?!>". by iApply "HΦ".
rewrite big_sepL_nil right_id; iFrame.
Qed.
Lemma wp_read_na1_pst E l Φ :
(|={E,∅}=> ∃ σ n v, σ !! l = Some(RSt $ n, v) ∧
▷ ownP σ ★
▷ (ownP (<[l:=(RSt $ S n, v)]>σ) ={∅,E}=★
▷ ownP σ ∗
▷ (ownP (<[l:=(RSt $ S n, v)]>σ) ={∅,E}=∗
WP Read Na2Ord (Lit $ LitLoc l) @ E {{ Φ }}))
⊢ WP Read Na1Ord (Lit $ LitLoc l) @ E {{ Φ }}.
Proof.
......@@ -81,27 +81,25 @@ Qed.
Lemma wp_write_sc_pst E σ l v v' :
σ !! l = Some (RSt 0, v') →
{{{ ▷ ownP σ }}} Write ScOrd (Lit $ LitLoc l) (of_val v) @ E
{{{ ; LitV LitUnit, ownP (<[l:=(RSt 0, v)]>σ) }}}.
{{{ RET LitV LitUnit; ownP (<[l:=(RSt 0, v)]>σ) }}}.
Proof.
iIntros (??) "[?HΦ]". iApply wp_lift_atomic_det_head_step; eauto.
iIntros (??) "?HΦ". iApply wp_lift_atomic_det_head_step; eauto.
by intros; inv_head_step; eauto. rewrite big_sepL_nil right_id; iFrame.
iNext. iIntros "?!>". by iApply "HΦ".
Qed.
Lemma wp_write_na2_pst E σ l v v' :
σ !! l = Some(WSt, v') →
{{{ ▷ ownP σ }}} Write Na2Ord (Lit $ LitLoc l) (of_val v) @ E
{{{ ; LitV LitUnit, ownP (<[l:=(RSt 0, v)]>σ) }}}.
{{{ RET LitV LitUnit; ownP (<[l:=(RSt 0, v)]>σ) }}}.
Proof.
iIntros (??) "[?HΦ]". iApply wp_lift_atomic_det_head_step; eauto.
by intros; inv_head_step; eauto.
rewrite big_sepL_nil right_id; iFrame. iNext. iIntros "?!>". by iApply "HΦ".
iIntros (??) "?HΦ". iApply wp_lift_atomic_det_head_step; eauto.
by intros; inv_head_step; eauto. rewrite big_sepL_nil right_id; iFrame.
Qed.
Lemma wp_write_na1_pst E l v Φ :
(|={E,∅}=> ∃ σ v', σ !! l = Some(RSt 0, v') ∧
▷ ownP σ ★
▷ (ownP (<[l:=(WSt, v')]>σ) ={∅,E}=★
▷ ownP σ ∗
▷ (ownP (<[l:=(WSt, v')]>σ) ={∅,E}=∗
WP Write Na2Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }}))
⊢ WP Write Na1Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }}.
Proof.
......@@ -116,11 +114,11 @@ Lemma wp_cas_fail_pst E σ l n e1 v1 v2 vl :
σ !! l = Some (RSt n, vl) →
value_eq σ v1 vl = Some false →
{{{ ▷ ownP σ }}} CAS (Lit $ LitLoc l) e1 (of_val v2) @ E
{{{ ; LitV $ LitInt 0, ownP σ }}}.
{{{ RET LitV $ LitInt 0; ownP σ }}}.
Proof.
iIntros (?%of_to_val ???) "[HP HΦ]". subst.
iIntros (?%of_to_val ???) "HP HΦ". subst.
iApply wp_lift_atomic_det_head_step; eauto. by intros; inv_head_step; eauto.
iFrame. iNext. rewrite big_sepL_nil right_id. iIntros "?!>". by iApply "HΦ".
iFrame. iNext. rewrite big_sepL_nil right_id. iIntros "?". by iApply "HΦ".
Qed.
Lemma wp_cas_suc_pst E σ l e1 v1 v2 vl :
......@@ -128,18 +126,18 @@ Lemma wp_cas_suc_pst E σ l e1 v1 v2 vl :
σ !! l = Some (RSt 0, vl) →
value_eq σ v1 vl = Some true →
{{{ ▷ ownP σ }}} CAS (Lit $ LitLoc l) e1 (of_val v2) @ E
{{{ ; LitV $ LitInt 1, ownP (<[l:=(RSt 0, v2)]>σ) }}}.
{{{ RET LitV $ LitInt 1; ownP (<[l:=(RSt 0, v2)]>σ) }}}.
Proof.
iIntros (?%of_to_val ???) "[HP HΦ]". subst.
iIntros (?%of_to_val ???) "HP HΦ". subst.
iApply wp_lift_atomic_det_head_step; eauto. by intros; inv_head_step; eauto.
iFrame. iNext. rewrite big_sepL_nil right_id. iIntros "?!>". by iApply "HΦ".
iFrame. iNext. rewrite big_sepL_nil right_id. iIntros "?". by iApply "HΦ".
Qed.
(** Base axioms for core primitives of the language: Stateless reductions *)
Lemma wp_fork E e :
{{{ ▷ WP e {{ _, True }} }}} Fork e @ E {{{ ; LitV LitUnit, True }}}.
{{{ ▷ WP e {{ _, True }} }}} Fork e @ E {{{ RET LitV LitUnit; True }}}.
Proof.
iIntros (?) "[?HΦ]". iApply wp_lift_pure_det_head_step; eauto.
iIntros (?) "?HΦ". iApply wp_lift_pure_det_head_step; eauto.
by intros; inv_head_step; eauto. iNext.
rewrite big_sepL_singleton. iFrame. iApply wp_value. done. by iApply "HΦ".
Qed.
......
theories/memcpy.v
+ 2
− 2
View file @ 3a4b14b9
......@@ -20,9 +20,9 @@ Notation "e1 <-[ i ]{ n } ! e2" :=
Lemma wp_memcpy `{heapG Σ} E l1 l2 vl1 vl2 q n:
nclose heapN ⊆ E →
length vl1 = n → length vl2 = n →
{{{ heap_ctx ★ l1 ↦★ vl1 ★ l2 ↦★{q} vl2 }}}
{{{ heap_ctx ∗ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
#l1 <-{n} !#l2 @ E
{{{; #(), l1 ↦★ vl2 ★ l2 ↦★{q} vl2 }}}.
{{{; #(), l1 ↦∗ vl2 ∗ l2 ↦∗{q} vl2 }}}.
Proof.
iIntros (? Hvl1 Hvl2 Φ) "[(#Hinv & Hl1 & Hl2) HΦ]".
iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec. wp_op=> ?; wp_if.
......
theories/perm.v
+ 5
− 5
View file @ 3a4b14b9
......@@ -27,7 +27,7 @@ Section perm.
λ tid, (κ ∋ ρ tid)%I.
Definition tok (κ : lifetime) (q : Qp) : perm :=
λ _, ([κ]{q} ★ lft κ)%I.
λ _, ([κ]{q} ∗ lft κ)%I.
Definition incl (κ κ' : lifetime) : perm :=
λ _, (κ ⊑ κ')%I.
......@@ -36,7 +36,7 @@ Section perm.
λ tid, (∃ x, P x tid)%I.
Definition sep (ρ1 ρ2 : perm) : @perm Σ :=
λ tid, (ρ1 tid ★ ρ2 tid)%I.
λ tid, (ρ1 tid ∗ ρ2 tid)%I.
Global Instance top : Top (@perm Σ) :=
λ _, True%I.
......@@ -60,7 +60,7 @@ Infix "⊑" := incl (at level 70) : perm_scope.
Notation "∃ x .. y , P" :=
(exist (λ x, .. (exist (λ y, P)) ..)) : perm_scope.
Infix "★" := sep (at level 80, right associativity) : perm_scope.
Infix "∗" := sep (at level 80, right associativity) : perm_scope.
Section duplicable.
......@@ -77,7 +77,7 @@ Section duplicable.
Proof. intros tid. apply _. Qed.
Global Instance sep_dup P Q :
Duplicable P → Duplicable Q → Duplicable (P ★ Q).
Duplicable P → Duplicable Q → Duplicable (P ∗ Q).
Proof. intros HP HQ tid. apply _. Qed.
Global Instance top_dup : Duplicable ⊤.
......@@ -98,7 +98,7 @@ Section has_type.
Qed.
Lemma has_type_wp E (ν : expr) ty tid (Φ : val -> iProp _) :
(ν ◁ ty)%P tid ★ (∀ (v : val), eval_expr ν = Some v ★ (v ◁ ty)%P tid ={E}=★ Φ v)
(ν ◁ ty)%P tid ∗ (∀ (v : val), eval_expr ν = Some v ∗ (v ◁ ty)%P tid ={E}=∗ Φ v)
⊢ WP ν @ E {{ Φ }}.
Proof.
iIntros "[H◁ HΦ]". setoid_rewrite has_type_value. unfold has_type.
......
theories/perm_incl.v
+ 17
− 17
View file @ 3a4b14b9
......@@ -10,13 +10,13 @@ Section defs.
(* Definitions *)
Definition perm_incl (ρ1 ρ2 : perm) :=
∀ tid, ρ1 tid ={⊤}=★ ρ2 tid.
∀ tid, ρ1 tid ={⊤}=∗ ρ2 tid.
Global Instance perm_equiv : Equiv perm :=
λ ρ1 ρ2, perm_incl ρ1 ρ2 ∧ perm_incl ρ2 ρ1.
Definition borrowing κ (ρ ρ1 ρ2 : perm) :=
∀ tid, lft κ ⊢ ρ tid -★ ρ1 tid ={⊤}=★ ρ2 tid ★ κ ∋ ρ1 tid.
∀ tid, lft κ ⊢ ρ tid -∗ ρ1 tid ={⊤}=∗ ρ2 tid ∗ κ ∋ ρ1 tid.
End defs.
......@@ -65,11 +65,11 @@ Section props.
Lemma perm_incl_top ρ : ρ ⇒ ⊤.
Proof. iIntros (tid) "H". eauto. Qed.
Lemma perm_incl_frame_l ρ ρ1 ρ2 : ρ1 ⇒ ρ2 → ρ ★ ρ1 ⇒ ρ ★ ρ2.
Lemma perm_incl_frame_l ρ ρ1 ρ2 : ρ1 ⇒ ρ2 → ρ ∗ ρ1 ⇒ ρ ∗ ρ2.
Proof. iIntros (Hρ tid) "[$?]". by iApply Hρ. Qed.
Lemma perm_incl_frame_r ρ ρ1 ρ2 :
ρ1 ⇒ ρ2 → ρ1 ★ ρ ⇒ ρ2 ★ ρ.
ρ1 ⇒ ρ2 → ρ1 ∗ ρ ⇒ ρ2 ∗ ρ.
Proof. iIntros (Hρ tid) "[?$]". by iApply Hρ. Qed.
Lemma perm_incl_exists_intro {A} P x : P x ⇒ ∃ x : A, P x.
......@@ -87,11 +87,11 @@ Section props.
Global Instance perm_top_left_id : LeftId (⇔) ⊤ sep.
Proof. intros ρ. by rewrite comm right_id. Qed.
Lemma perm_incl_duplicable ρ (_ : Duplicable ρ) : ρ ⇒ ρ ★ ρ.
Lemma perm_incl_duplicable ρ (_ : Duplicable ρ) : ρ ⇒ ρ ∗ ρ.
Proof. iIntros (tid) "#H!>". by iSplit. Qed.
Lemma perm_tok_plus κ q1 q2 :
tok κ q1 ★ tok κ q2 ⇔ tok κ (q1 + q2).
tok κ q1 ∗ tok κ q2 ⇔ tok κ (q1 + q2).
Proof.
rewrite /tok /sep /=; split; intros tid; rewrite -lft_own_op;
iIntros "[[$$]H]!>". by iDestruct "H" as "[$?]". by auto.
......@@ -100,11 +100,11 @@ Section props.
Lemma perm_lftincl_refl κ : ⊤ ⇒ κ ⊑ κ.
Proof. iIntros (tid) "_!>". iApply lft_incl_refl. Qed.
Lemma perm_lftincl_trans κ1 κ2 κ3 : κ1 ⊑ κ2 ★ κ2 ⊑ κ3 ⇒ κ1 ⊑ κ3.
Lemma perm_lftincl_trans κ1 κ2 κ3 : κ1 ⊑ κ2 ∗ κ2 ⊑ κ3 ⇒ κ1 ⊑ κ3.
Proof. iIntros (tid) "[#?#?]!>". iApply lft_incl_trans. auto. Qed.
Lemma perm_incl_share q ν κ ty :
ν ◁ &uniq{κ} ty ★ [κ]{q} ⇒ ν ◁ &shr{κ} ty ★ [κ]{q}.
ν ◁ &uniq{κ} ty ∗ [κ]{q} ⇒ ν ◁ &shr{κ} ty ∗ [κ]{q}.
Proof.
iIntros (tid) "[Huniq [Htok $]]". unfold has_type.
destruct (eval_expr ν); last by iDestruct "Huniq" as "[]".
......@@ -117,14 +117,14 @@ Section props.
Lemma split_own_prod tyl (q0: Qp) (ql : list Qp) (l : loc) tid :
length tyl = length ql →
(own (foldr Qp_plus q0 ql) (Π tyl)).(ty_own) tid [ #l] ⊣⊢
▷ †{q0}(shift_loc l (0 + (Π tyl).(ty_size))%nat)…0 ★
[★ list] qtyoffs ∈ (combine ql (combine_offs tyl 0)),
▷ †{q0}(shift_loc l (0 + (Π tyl).(ty_size))%nat)…0 ∗
[∗ list] qtyoffs ∈ (combine ql (combine_offs tyl 0)),
(own (qtyoffs.1) (qtyoffs.2.1)).(ty_own)
tid [ #(shift_loc l (qtyoffs.2.2))].
Proof.
intros Hlen.
assert (REW: ∀ (l : loc) (Φ : loc → iProp Σ),
Φ l ⊣⊢ (∃ l0:loc, [ #l] = [ #l0] ★ Φ l0)).
Φ l ⊣⊢ (∃ l0:loc, [ #l] = [ #l0] ∗ Φ l0)).
{ intros l0 Φ. iSplit; iIntros "H". eauto.
iDestruct "H" as (l') "[Heq H]". iDestruct "Heq" as %[=]. subst. done. }
setoid_rewrite <-REW. clear REW.
......@@ -145,7 +145,7 @@ Section props.
foldr (λ (q : Qp) acc, q + acc)%Qc 0%Qc ql = q →
ν ◁ own q (Π tyl) ⇔
foldr (λ qtyoffs acc,
(ν +ₗ #(qtyoffs.2.2:nat))%E ◁ own (qtyoffs.1) (qtyoffs.2.1) ★ acc)
(ν +ₗ #(qtyoffs.2.2:nat))%E ◁ own (qtyoffs.1) (qtyoffs.2.1) ∗ acc)
⊤ (combine ql (combine_offs tyl 0)).
Proof.
intros Hlen Hq. assert (ql ≠ []).
......@@ -168,7 +168,7 @@ Section props.
apply uPred.exist_proper=>l0.
rewrite -{3}(Qp_div_2 q0) -{3}(right_id O plus ty.(ty_size))
-heap_freeable_op_eq uPred.later_sep -!assoc.
iSplit; iIntros "[#Eq[?[??]]]"; iFrame "# ★";
iSplit; iIntros "[#Eq[?[??]]]"; iFrame "# ∗";
iDestruct "Eq" as %[=]; subst; rewrite shift_loc_assoc_nat //.
- rewrite /= big_sepL_cons /sep -IH // !uPred.sep_exist_r uPred.sep_exist_l.
apply uPred.exist_proper=>l0. rewrite -!assoc /=.
......@@ -178,7 +178,7 @@ Section props.
Lemma perm_split_uniq_borrow_prod tyl κ ν :
ν ◁ &uniq{κ} (Π tyl) ⇒
foldr (λ tyoffs acc,
(ν +ₗ #(tyoffs.2:nat))%E ◁ &uniq{κ} (tyoffs.1) ★ acc)%P
(ν +ₗ #(tyoffs.2:nat))%E ◁ &uniq{κ} (tyoffs.1) ∗ acc)%P
⊤ (combine_offs tyl 0).
Proof.
intros tid. unfold has_type. simpl eval_expr.
......@@ -195,7 +195,7 @@ Section props.
Lemma perm_split_shr_borrow_prod tyl κ ν :
ν ◁ &shr{κ} (Π tyl) ⇒
foldr (λ tyoffs acc,
(ν +ₗ #(tyoffs.2:nat))%E ◁ &shr{κ} (tyoffs.1) ★ acc)%P
(ν +ₗ #(tyoffs.2:nat))%E ◁ &shr{κ} (tyoffs.1) ∗ acc)%P
⊤ (combine_offs tyl 0).
Proof.
intros tid. unfold has_type. simpl eval_expr.
......@@ -213,7 +213,7 @@ Section props.
Admitted.
Lemma borrowing_perm_incl κ ρ ρ1 ρ2 θ :
borrowing κ ρ ρ1 ρ2 → ρ ★ κ ∋ θ ★ ρ1 ⇒ ρ2 ★ κ ∋ (θ ★ ρ1).
borrowing κ ρ ρ1 ρ2 → ρ ∗ κ ∋ θ ∗ ρ1 ⇒ ρ2 ∗ κ ∋ (θ ∗ ρ1).
Proof.
iIntros (Hbor tid) "(Hρ&Hθ&Hρ1)".
iMod (Hbor with "[#] Hρ Hρ1") as "[$ ?]". by iApply lft_extract_lft.
......@@ -251,7 +251,7 @@ Section props.
Qed.
Lemma reborrow_shr_perm_incl κ κ' ν ty :
κ ⊑ κ' ★ ν ◁ &shr{κ'}ty ⇒ ν ◁ &shr{κ}ty.
κ ⊑ κ' ∗ ν ◁ &shr{κ'}ty ⇒ ν ◁ &shr{κ}ty.
Proof.
iIntros (tid) "[#Hord #Hκ']". unfold has_type.
destruct (eval_expr ν) as [[[|l|]|]|];
......
theories/proofmode.v
+ 17
− 15
View file @ 3a4b14b9
......@@ -17,20 +17,20 @@ Global Instance into_and_mapsto l q v :
Proof. by rewrite /IntoAnd heap_mapsto_op_split. Qed.
Global Instance into_and_mapsto_vec l q vl :
IntoAnd false (l ↦★{q} vl) (l ↦★{q/2} vl) (l ↦★{q/2} vl).
IntoAnd false (l ↦∗{q} vl) (l ↦∗{q/2} vl) (l ↦∗{q/2} vl).
Proof. by rewrite /IntoAnd heap_mapsto_vec_op_split. Qed.
Lemma tac_wp_alloc Δ Δ' E j1 j2 n Φ :
(Δ ⊢ heap_ctx) → nclose heapN ⊆ E → 0 < n →
IntoLaterEnvs Δ Δ' →
(∀ l vl, n = length vl → ∃ Δ'',
envs_app false (Esnoc (Esnoc Enil j1 (l ↦★ vl)) j2 (†l…(Z.to_nat n))) Δ'
envs_app false (Esnoc (Esnoc Enil j1 (l ↦∗ vl)) j2 (†l…(Z.to_nat n))) Δ'
= Some Δ'' ∧
(Δ'' ⊢ |={E}=> Φ (LitV $ LitLoc l))) →
Δ ⊢ WP Alloc (Lit $ LitInt n) @ E {{ Φ }}.
Proof.
intros ???? HΔ. rewrite -wp_fupd -wp_alloc // -always_and_sep_l.
apply and_intro; first done.
intros ???? HΔ. rewrite -wp_fupd. eapply wand_apply; first exact:wp_alloc.
rewrite -always_and_sep_l. apply and_intro; first done.
rewrite into_later_env_sound; apply later_mono, forall_intro=> l;
apply forall_intro=> vl. apply wand_intro_l. rewrite -assoc.
apply pure_elim_sep_l=> Hn. apply wand_elim_r'.
......@@ -41,7 +41,7 @@ Qed.
Lemma tac_wp_free Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
(Δ ⊢ heap_ctx) → nclose heapN ⊆ E → n = length vl →
IntoLaterEnvs Δ Δ' →
envs_lookup i1 Δ' = Some (false, l ↦★ vl)%I →
envs_lookup i1 Δ' = Some (false, l ↦∗ vl)%I →
envs_delete i1 false Δ' = Δ'' →
envs_lookup i2 Δ'' = Some (false, †l…n')%I →
envs_delete i2 false Δ'' = Δ''' →
......@@ -49,8 +49,8 @@ Lemma tac_wp_free Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
(Δ''' ⊢ |={E}=> Φ (LitV LitUnit)) →
Δ ⊢ WP Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E {{ Φ }}.
Proof.
intros ?? -> ?? <- ? <- -> HΔ.
rewrite -wp_fupd -wp_free // -!assoc -always_and_sep_l.
intros ?? -> ?? <- ? <- -> HΔ. rewrite -wp_fupd.
eapply wand_apply; first exact:wp_free. rewrite -!assoc -always_and_sep_l.
apply and_intro; first done.
rewrite into_later_env_sound -!later_sep; apply later_mono.
do 2 (rewrite envs_lookup_sound' //). by rewrite HΔ wand_True.
......@@ -64,12 +64,12 @@ Lemma tac_wp_read Δ Δ' E i l q v o Φ :
Δ ⊢ WP Read o (Lit $ LitLoc l) @ E {{ Φ }}.
Proof.
intros ??[->| ->]???.
- rewrite -wp_fupd -wp_read_na // -!assoc -always_and_sep_l.
apply and_intro; first done.
- rewrite -wp_fupd. eapply wand_apply; first exact:wp_read_na.
rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
by apply later_mono, sep_mono_r, wand_mono.
- rewrite -wp_fupd -wp_read_sc // -!assoc -always_and_sep_l.
apply and_intro; first done.
- rewrite -wp_fupd. eapply wand_apply; first exact:wp_read_sc.
rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
by apply later_mono, sep_mono_r, wand_mono.
Qed.
......@@ -84,10 +84,12 @@ Lemma tac_wp_write Δ Δ' Δ'' E i l v e v' o Φ :
Δ ⊢ WP Write o (Lit $ LitLoc l) e @ E {{ Φ }}.
Proof.
intros ???[->| ->]????.
- rewrite -wp_fupd -wp_write_na // -!assoc -always_and_sep_l. apply and_intro; first done.
- rewrite -wp_fupd. eapply wand_apply; first by apply wp_write_na.
rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
- rewrite -wp_fupd -wp_write_sc // -!assoc -always_and_sep_l. apply and_intro; first done.
- rewrite -wp_fupd. eapply wand_apply; first by apply wp_write_sc.
rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
......@@ -135,8 +137,8 @@ Tactic Notation "wp_free" :=
|solve_ndisj
|try fast_done
|apply _
|let l := match goal with |- _ = Some (_, (?l ↦★ _)%I) => l end in
iAssumptionCore || fail "wp_free: cannot find" l "↦★ ?"
|let l := match goal with |- _ = Some (_, (?l ↦∗ _)%I) => l end in
iAssumptionCore || fail "wp_free: cannot find" l "↦∗ ?"
|env_cbv; reflexivity
|let l := match goal with |- _ = Some (_, († ?l … _)%I) => l end in
iAssumptionCore || fail "wp_free: cannot find †" l "… ?"
......
theories/type.v
+ 38
− 38
View file @ 3a4b14b9
......@@ -33,14 +33,14 @@ Record type `{heapG Σ, lifetimeG Σ, thread_localG Σ} :=
more consistent with thread-local tokens, which we do not
give any. *)
ty_share E N κ l tid q : mgmtE ⊥ nclose N → mgmtE ⊆ E →
&{κ} (l ↦★: ty_own tid) ⊢ [κ]{q} ={E}=★ ty_shr κ tid N l ★ [κ]{q};
&{κ} (l ↦∗: ty_own tid) ⊢ [κ]{q} ={E}=∗ ty_shr κ tid N l ∗ [κ]{q};
ty_shr_mono κ κ' tid N l :
κ' ⊑ κ ⊢ ty_shr κ tid N l → ty_shr κ' tid N l;
ty_shr_acc κ tid E N l q :
ty_dup → mgmtE ∪ nclose N ⊆ E →
ty_shr κ tid N l ⊢
[κ]{q} ★ tl_own tid N ={E}=★ ∃ q', ▷l ↦★{q'}: ty_own tid ★
(▷l ↦★{q'}: ty_own tid ={E}=★ [κ]{q} ★ tl_own tid N)
[κ]{q} ∗ tl_own tid N ={E}=∗ ∃ q', ▷l ↦∗{q'}: ty_own tid ∗
(▷l ↦∗{q'}: ty_own tid ={E}=∗ [κ]{q} ∗ tl_own tid N)
}.
Global Existing Instances ty_shr_persistent ty_dup_persistent.
......@@ -61,7 +61,7 @@ Program Coercion ty_of_st `{heapG Σ, lifetimeG Σ, thread_localG Σ}
borrow, otherwise I do not knwo how to prove the shr part of
[lft_incl_ty_incl_shared_borrow]. *)
ty_shr := λ κ tid _ l,
(∃ vl, (&frac{κ} λ q, l ↦★{q} vl) ★ ▷ st.(st_own) tid vl)%I
(∃ vl, (&frac{κ} λ q, l ↦∗{q} vl) ∗ ▷ st.(st_own) tid vl)%I
|}.
Next Obligation. intros. apply st_size_eq. Qed.
Next Obligation.
......@@ -142,11 +142,11 @@ Section types.
Since this assertion is timeless, this should not cause
problems. *)
(∃ l:loc, vl = [ #l ] ★ ▷ †{q}l…ty.(ty_size)
★ ▷ l ↦★: ty.(ty_own) tid)%I;
(∃ l:loc, vl = [ #l ] ∗ ▷ †{q}l…ty.(ty_size)
∗ ▷ l ↦∗: ty.(ty_own) tid)%I;
ty_shr κ tid N l :=
(∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ★
∀ q', □ ([κ]{q'} ={mgmtE ∪ N, mgmtE}▷=★ ty.(ty_shr) κ tid N l' ★ [κ]{q'}))%I
(∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
∀ q', □ ([κ]{q'} ={mgmtE ∪ N, mgmtE}▷=∗ ty.(ty_shr) κ tid N l' ∗ [κ]{q'}))%I
|}.
Next Obligation. done. Qed.
Next Obligation.
......@@ -169,7 +169,7 @@ Section types.
iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
replace ((mgmtE ∪ N) ∖ N) with mgmtE by set_solver.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- iAssert (&{κ}▷ l' ↦★: ty_own ty tid)%I with "[Hbtok]" as "Hb".
- iAssert (&{κ}▷ l' ↦∗: ty_own ty tid)%I with "[Hbtok]" as "Hb".
{ iApply lft_borrow_persist. eauto. }
iMod (lft_borrow_open with "Hb Htok") as "[Hown Hob]". set_solver.
iIntros "!>". iNext.
......@@ -194,11 +194,11 @@ Section types.
Program Definition uniq_borrow (κ:lifetime) (ty:type) :=
{| ty_size := 1; ty_dup := false;
ty_own tid vl :=
(∃ l:loc, vl = [ #l ] ★ &{κ} l ↦★: ty.(ty_own) tid)%I;
(∃ l:loc, vl = [ #l ] ∗ &{κ} l ↦∗: ty.(ty_own) tid)%I;
ty_shr κ' tid N l :=
(∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ★
∀ q' κ'', □ (κ'' ⊑ κ ★ κ'' ⊑ κ' ★ [κ'']{q'}
={mgmtE ∪ N, mgmtE}▷=★ ty.(ty_shr) κ'' tid N l' ★ [κ'']{q'}))%I
(∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
∀ q' κ'', □ (κ'' ⊑ κ ∗ κ'' ⊑ κ' ∗ [κ'']{q'}
={mgmtE ∪ N, mgmtE}▷=∗ ty.(ty_shr) κ'' tid N l' ∗ [κ'']{q'}))%I
|}.
Next Obligation. done. Qed.
Next Obligation.
......@@ -222,8 +222,8 @@ Section types.
iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
replace ((mgmtE ∪ N) ∖ N) with mgmtE by set_solver.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- iAssert (&{κ''}&{κ} l' ↦★: ty_own ty tid)%I with "[Hbtok]" as "Hb".
{ iApply lft_borrow_persist. iExists κ0, i. iFrame "★ #".
- iAssert (&{κ''}&{κ} l' ↦∗: ty_own ty tid)%I with "[Hbtok]" as "Hb".
{ iApply lft_borrow_persist. iExists κ0, i. iFrame "∗ #".
iApply lft_incl_trans. eauto. }
iMod (lft_borrow_open with "Hb Htok") as "[Hown Hob]". set_solver.
iIntros "!>". iNext.
......@@ -255,7 +255,7 @@ Section types.
Program Definition shared_borrow (κ : lifetime) (ty : type) : type :=
{| st_size := 1;
st_own tid vl := (∃ l:loc, vl = [ #l ] ★ ty.(ty_shr) κ tid lrustN l)%I |}.
st_own tid vl := (∃ l:loc, vl = [ #l ] ∗ ty.(ty_shr) κ tid lrustN l)%I |}.
Next Obligation.
iIntros (κ ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
Qed.
......@@ -268,7 +268,7 @@ Section types.
Lemma list_ty_type_eq tid (tyl : list type) (vll : list (list val)) :
length tyl = length vll →
([★ list] tyvl ∈ combine tyl vll, ty_own (tyvl.1) tid (tyvl.2))
([∗ list] tyvl ∈ combine tyl vll, ty_own (tyvl.1) tid (tyvl.2))
⊢ length (concat vll) = sum_list_with ty_size tyl.
Proof.
revert vll; induction tyl as [|ty tyq IH]; destruct vll;
......@@ -279,11 +279,11 @@ Section types.
Qed.
Lemma split_prod_mt tid tyl l q :
(l ↦★{q}: λ vl,
∃ vll, vl = concat vll ★ length tyl = length vll
★ [★ list] tyvl ∈ combine tyl vll, ty_own (tyvl.1) tid (tyvl.2))%I
⊣⊢ [★ list] tyoffs ∈ combine_offs tyl 0,
shift_loc l (tyoffs.2) ↦★{q}: ty_own (tyoffs.1) tid.
(l ↦∗{q}: λ vl,
∃ vll, vl = concat vll ∗ length tyl = length vll
∗ [∗ list] tyvl ∈ combine tyl vll, ty_own (tyvl.1) tid (tyvl.2))%I
⊣⊢ [∗ list] tyoffs ∈ combine_offs tyl 0,
shift_loc l (tyoffs.2) ↦∗{q}: ty_own (tyoffs.1) tid.
Proof.
rewrite -{1}(shift_loc_0_nat l). generalize 0%nat.
induction tyl as [|ty tyl IH]=>/= offs.
......@@ -317,7 +317,7 @@ Section types.
Lemma split_prod_namespace tid (N : namespace) n :
∃ E, (tl_own tid N ⊣⊢ tl_own tid E
★ nat_rec_shift True (λ i P, tl_own tid (N .@ i) ★ P) 0%nat n)
∗ nat_rec_shift True (λ i P, tl_own tid (N .@ i) ∗ P) 0%nat n)
∧ (∀ i, i < 0 → nclose (N .@ i) ⊆ E)%nat.
Proof.
generalize 0%nat. induction n as [|n IH].
......@@ -333,15 +333,15 @@ Section types.
Program Definition product (tyl : list type) :=
{| ty_size := sum_list_with ty_size tyl; ty_dup := forallb ty_dup tyl;
ty_own tid vl :=
(∃ vll, vl = concat vll ★ length tyl = length vll ★
[★ list] tyvl ∈ combine tyl vll, tyvl.1.(ty_own) tid (tyvl.2))%I;
(∃ vll, vl = concat vll ∗ length tyl = length vll ∗
[∗ list] tyvl ∈ combine tyl vll, tyvl.1.(ty_own) tid (tyvl.2))%I;
ty_shr κ tid N l :=
([★ list] i ↦ tyoffs ∈ combine_offs tyl 0,
([∗ list] i ↦ tyoffs ∈ combine_offs tyl 0,
tyoffs.1.(ty_shr) κ tid (N .@ i) (shift_loc l (tyoffs.2)))%I
|}.
Next Obligation.
intros tyl tid vl Hfa.
cut (∀ vll, PersistentP ([★ list] tyvl ∈ combine tyl vll,
cut (∀ vll, PersistentP ([∗ list] tyvl ∈ combine tyl vll,
ty_own (tyvl.1) tid (tyvl.2))). by apply _.
clear vl. induction tyl as [|ty tyl IH]=>[|[|vl vll]]; try by apply _.
edestruct andb_prop_elim as [Hduph Hdupq]. by apply Hfa.
......@@ -387,7 +387,7 @@ Section types.
iExists q'. iModIntro. rewrite big_sepL_cons.
rewrite -heap_mapsto_vec_prop_op; last apply ty_size_eq.
iDestruct "Hownh" as "[$ Hownh1]".
rewrite (big_sepL_proper (λ _ x, _ ↦★{_}: _)%I); last first.
rewrite (big_sepL_proper (λ _ x, _ ↦∗{_}: _)%I); last first.
{ intros. rewrite -heap_mapsto_vec_prop_op; last apply ty_size_eq.
instantiate (1:=λ _ y, _). simpl. reflexivity. }
rewrite big_sepL_sepL. iDestruct "Hownq" as "[$ Hownq1]".
......@@ -397,9 +397,9 @@ Section types.
Qed.
Lemma split_sum_mt l tid q tyl :
(l ↦★{q}: λ vl,
∃ (i : nat) vl', vl = #i :: vl' ★ ty_own (nth i tyl emp) tid vl')%I
⊣⊢ ∃ (i : nat), l ↦{q} #i ★ shift_loc l 1 ↦★{q}: ty_own (nth i tyl emp) tid.
(l ↦∗{q}: λ vl,
∃ (i : nat) vl', vl = #i :: vl' ∗ ty_own (nth i tyl emp) tid vl')%I
⊣⊢ ∃ (i : nat), l ↦{q} #i ∗ shift_loc l 1 ↦∗{q}: ty_own (nth i tyl emp) tid.
Proof.
iSplit; iIntros "H".
- iDestruct "H" as (vl) "[Hmt Hown]". iDestruct "Hown" as (i vl') "(%&Hown)". subst.
......@@ -428,9 +428,9 @@ Section types.
Program Definition sum {n} (tyl : list type) {_:LstTySize n tyl} :=
{| ty_size := S n; ty_dup := forallb ty_dup tyl;
ty_own tid vl :=
(∃ (i : nat) vl', vl = #i :: vl' ★ (nth i tyl emp).(ty_own) tid vl')%I;
(∃ (i : nat) vl', vl = #i :: vl' ∗ (nth i tyl emp).(ty_own) tid vl')%I;
ty_shr κ tid N l :=
(∃ (i : nat), (&frac{κ} λ q, l ↦{q} #i) ★
(∃ (i : nat), (&frac{κ} λ q, l ↦{q} #i) ∗
(nth i tyl emp).(ty_shr) κ tid N (shift_loc l 1))%I
|}.
Next Obligation.
......@@ -489,9 +489,9 @@ Section types.
Program Definition cont {n : nat} (ρ : vec val n → @perm Σ) :=
{| ty_size := 1; ty_dup := false;
ty_own tid vl := (∃ f, vl = [f] ★
∀ vl, ρ vl tid -★ tl_own tid ⊤
-★ WP f (map of_val vl) {{λ _, False}})%I;
ty_own tid vl := (∃ f, vl = [f] ∗
∀ vl, ρ vl tid -∗ tl_own tid ⊤
-∗ WP f (map of_val vl) {{λ _, False}})%I;
ty_shr κ tid N l := True%I |}.
Next Obligation. done. Qed.
Next Obligation.
......@@ -507,8 +507,8 @@ Section types.
needs a Send closure). *)
Program Definition fn {A n} (ρ : A -> vec val n → @perm Σ) : type :=
{| st_size := 1;
st_own tid vl := (∃ f, vl = [f] ★ ∀ x vl,
{{ ρ x vl tid ★ tl_own tid ⊤ }} f (map of_val vl) {{λ _, False}})%I |}.
st_own tid vl := (∃ f, vl = [f] ∗ ∀ x vl,
{{ ρ x vl tid ∗ tl_own tid ⊤ }} f (map of_val vl) {{λ _, False}})%I |}.
Next Obligation.
iIntros (x n ρ tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
Qed.
......
theories/type_incl.v
+ 12
− 12
View file @ 3a4b14b9
......@@ -9,20 +9,20 @@ Section ty_incl.
Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
Definition ty_incl (ρ : perm) (ty1 ty2 : type) :=
∀ tid, ρ tid ={⊤}=★
(□ ∀ vl, ty1.(ty_own) tid vl → ty2.(ty_own) tid vl) ★
∀ tid, ρ tid ={⊤}=∗
(□ ∀ vl, ty1.(ty_own) tid vl → ty2.(ty_own) tid vl) ∗
(□ ∀ κ E l, ty1.(ty_shr) κ tid E l →
(* [ty_incl] needs to prove something about the length of the
object when it is shared. We place this property under the
hypothesis that [ty2.(ty_shr)] holds, so that the [!] type
is still included in any other. *)
ty2.(ty_shr) κ tid E l ★ ty1.(ty_size) = ty2.(ty_size)).
ty2.(ty_shr) κ tid E l ∗ ty1.(ty_size) = ty2.(ty_size)).
Global Instance ty_incl_refl ρ : Reflexive (ty_incl ρ).
Proof. iIntros (ty tid) "_!>". iSplit; iIntros "!#"; eauto. Qed.
Lemma ty_incl_trans ρ θ ty1 ty2 ty3 :
ty_incl ρ ty1 ty2 → ty_incl θ ty2 ty3 → ty_incl (ρ ★ θ) ty1 ty3.
ty_incl ρ ty1 ty2 → ty_incl θ ty2 ty3 → ty_incl (ρ ∗ θ) ty1 ty3.
Proof.
iIntros (H12 H23 tid) "[H1 H2]".
iMod (H12 with "H1") as "[#H12 #H12']".
......@@ -93,10 +93,10 @@ Section ty_incl.
Duplicable ρ → Forall2 (ty_incl ρ) tyl1 tyl2 → ty_incl ρ (Π tyl1) (Π tyl2).
Proof.
intros Hρ HFA. iIntros (tid) "#Hρ". iSplitL "".
- assert (Himpl : ρ tid ={⊤}=★
- assert (Himpl : ρ tid ={⊤}=∗
□ (∀ vll, length tyl1 = length vll →
([★ list] tyvl ∈ combine tyl1 vll, ty_own (tyvl.1) tid (tyvl.2))
→ ([★ list] tyvl ∈ combine tyl2 vll, ty_own (tyvl.1) tid (tyvl.2)))).
([∗ list] tyvl ∈ combine tyl1 vll, ty_own (tyvl.1) tid (tyvl.2))
→ ([∗ list] tyvl ∈ combine tyl2 vll, ty_own (tyvl.1) tid (tyvl.2)))).
{ induction HFA as [|ty1 ty2 tyl1 tyl2 Hincl HFA IH].
- iIntros "_!>!#* _ _". by rewrite big_sepL_nil.
- iIntros "#Hρ". iMod (IH with "Hρ") as "#Hqimpl".
......@@ -147,7 +147,7 @@ Section ty_incl.
ty_incl ρ (sum tyl1) (sum tyl2).
Proof.
iIntros (DUP FA tid) "#Hρ". rewrite /sum /=. iSplitR "".
- assert (Hincl : ρ tid ={⊤}=★
- assert (Hincl : ρ tid ={⊤}=∗
(□ ∀ i vl, (nth i tyl1 ∅%T).(ty_own) tid vl
→ (nth i tyl2 ∅%T).(ty_own) tid vl)).
{ clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
......@@ -157,7 +157,7 @@ Section ty_incl.
iMod (Hincl with "Hρ") as "#Hincl". iIntros "!>!#*H".
iDestruct "H" as (i vl') "[% Hown]". subst. iExists _, _. iSplit. done.
by iApply "Hincl".
- assert (Hincl : ρ tid ={⊤}=★
- assert (Hincl : ρ tid ={⊤}=∗
(□ ∀ i κ E l, (nth i tyl1 ∅%T).(ty_shr) κ tid E l
→ (nth i tyl2 ∅%T).(ty_shr) κ tid E l)).
{ clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
......@@ -197,7 +197,7 @@ Section ty_incl.
Admitted.
Lemma ty_incl_cont {n} ρ ρ1 ρ2 :
Duplicable ρ → (∀ vl : vec val n, ρ ★ ρ2 vl ⇒ ρ1 vl) →
Duplicable ρ → (∀ vl : vec val n, ρ ∗ ρ2 vl ⇒ ρ1 vl) →
ty_incl ρ (cont ρ1) (cont ρ2).
Proof.
iIntros (? Hρ1ρ2 tid) "#Hρ!>". iSplit; iIntros "!#*H"; last by auto.
......@@ -207,7 +207,7 @@ Section ty_incl.
Qed.
Lemma ty_incl_fn {A n} ρ ρ1 ρ2 :
Duplicable ρ → (∀ (x : A) (vl : vec val n), ρ ★ ρ2 x vl ⇒ ρ1 x vl) →
Duplicable ρ → (∀ (x : A) (vl : vec val n), ρ ∗ ρ2 x vl ⇒ ρ1 x vl) →
ty_incl ρ (fn ρ1) (fn ρ2).
Proof.
iIntros (? Hρ1ρ2 tid) "#Hρ!>". iSplit; iIntros "!#*#H".
......@@ -242,7 +242,7 @@ Section ty_incl.
Qed.
Lemma ty_incl_perm_incl ρ ty1 ty2 ν :
ty_incl ρ ty1 ty2 → ρ ★ ν ◁ ty1 ⇒ ν ◁ ty2.
ty_incl ρ ty1 ty2 → ρ ∗ ν ◁ ty1 ⇒ ν ◁ ty2.
Proof.
iIntros (Hincl tid) "[Hρ Hty1]". iMod (Hincl with "Hρ") as "[#Hownincl _]".
unfold Perm.has_type. destruct (Perm.eval_expr ν); last done. by iApply "Hownincl".
......
theories/typing.v
+ 55
− 55
View file @ 3a4b14b9
......@@ -10,24 +10,24 @@ Section typing.
(* TODO : good notations for [typed_step] and [typed_step_ty] ? *)
Definition typed_step (ρ : perm) e (θ : val → perm) :=
∀ tid, {{ heap_ctx ★ ρ tid ★ tl_own tid ⊤ }} e
{{ v, θ v tid ★ tl_own tid ⊤ }}.
∀ tid, {{ heap_ctx ∗ ρ tid ∗ tl_own tid ⊤ }} e
{{ v, θ v tid ∗ tl_own tid ⊤ }}.
Definition typed_step_ty (ρ : perm) e ty :=
typed_step ρ e (λ ν, ν ◁ ty)%P.
Definition typed_program (ρ : perm) e :=
∀ tid, {{ heap_ctx ★ ρ tid ★ tl_own tid ⊤ }} e {{ _, False }}.
∀ tid, {{ heap_ctx ∗ ρ tid ∗ tl_own tid ⊤ }} e {{ _, False }}.
Lemma typed_frame ρ e θ ξ:
typed_step ρ e θ → typed_step (ρ ★ ξ) e (λ ν, θ ν ★ ξ)%P.
typed_step ρ e θ → typed_step (ρ ∗ ξ) e (λ ν, θ ν ∗ ξ)%P.
Proof.
iIntros (Hwt tid) "!#(#HEAP&[?$]&?)". iApply Hwt. by iFrame.
Qed.
Lemma typed_step_exists {A} ρ θ e ξ:
(∀ x:A, typed_step (ρ ★ θ x) e ξ) →
typed_step (ρ ★ ∃ x, θ x) e ξ.
(∀ x:A, typed_step (ρ ∗ θ x) e ξ) →
typed_step (ρ ∗ ∃ x, θ x) e ξ.
Proof.
iIntros (Hwt tid) "!#(#HEAP&[Hρ Hθ]&?)". iDestruct "Hθ" as (x) "Hθ".
iApply Hwt. by iFrame.
......@@ -44,7 +44,7 @@ Section typing.
length xl = n →
(∀ (a : A) (vl : vec val n) (fv : val) e',
subst_l xl (map of_val vl) e = Some e' →
typed_program (fv ◁ fn θ ★ (θ a vl) ★ ρ) (subst' f fv e')) →
typed_program (fv ◁ fn θ ∗ (θ a vl) ∗ ρ) (subst' f fv e')) →
typed_step_ty ρ (Rec f xl e) (fn θ).
Proof.
iIntros (Hn He tid) "!#(#HEAP&#Hρ&$)".
......@@ -57,14 +57,14 @@ Section typing.
iApply wp_rec; try done.
{ apply List.Forall_forall=>?. rewrite in_map_iff=>-[?[<- _]].
rewrite to_of_val. eauto. }
iNext. iApply He. done. iFrame "★#". by rewrite has_type_value.
iNext. iApply He. done. iFrame "∗#". by rewrite has_type_value.
Qed.
Lemma typed_cont {n} `{Closed (f :b: xl +b+ []) e} ρ θ :
length xl = n →
(∀ (fv : val) (vl : vec val n) e',
subst_l xl (map of_val vl) e = Some e' →
typed_program (fv ◁ cont (λ vl, ρ ★ θ vl)%P ★ (θ vl) ★ ρ) (subst' f fv e')) →
typed_program (fv ◁ cont (λ vl, ρ ∗ θ vl)%P ∗ (θ vl) ∗ ρ) (subst' f fv e')) →
typed_step_ty ρ (Rec f xl e) (cont θ).
Proof.
iIntros (Hn He tid) "!#(#HEAP&Hρ&$)". specialize (He (RecV f xl e)).
......@@ -77,7 +77,7 @@ Section typing.
iApply wp_rec; try done.
{ apply List.Forall_forall=>?. rewrite in_map_iff=>-[?[<- _]].
rewrite to_of_val. eauto. }
iNext. iApply He. done. iFrame "★#". rewrite has_type_value.
iNext. iApply He. done. iFrame "∗#". rewrite has_type_value.
iExists _. iSplit. done. iIntros (vl') "[Hρ Hθ] Htl".
iDestruct ("IH" with "Hρ") as (f') "[Hf' IH']".
iDestruct "Hf'" as %[=<-]. iApply ("IH'" with "Hθ Htl").
......@@ -91,7 +91,7 @@ Section typing.
Lemma typed_plus e1 e2 ρ1 ρ2:
typed_step_ty ρ1 e1 int → typed_step_ty ρ2 e2 int →
typed_step_ty (ρ1 ★ ρ2) (e1 + e2) int.
typed_step_ty (ρ1 ∗ ρ2) (e1 + e2) int.
Proof.
unfold typed_step_ty, typed_step. setoid_rewrite has_type_value.
iIntros (He1 He2 tid) "!#(#HEAP&[H1 H2]&?)".
......@@ -104,7 +104,7 @@ Section typing.
Lemma typed_minus e1 e2 ρ1 ρ2:
typed_step_ty ρ1 e1 int → typed_step_ty ρ2 e2 int →
typed_step_ty (ρ1 ★ ρ2) (e1 - e2) int.
typed_step_ty (ρ1 ∗ ρ2) (e1 - e2) int.
Proof.
unfold typed_step_ty, typed_step. setoid_rewrite has_type_value.
iIntros (He1 He2 tid) "!#(#HEAP&[H1 H2]&?)".
......@@ -117,7 +117,7 @@ Section typing.
Lemma typed_le e1 e2 ρ1 ρ2:
typed_step_ty ρ1 e1 int → typed_step_ty ρ2 e2 int →
typed_step_ty (ρ1 ★ ρ2) (e1 ≤ e2) bool.
typed_step_ty (ρ1 ∗ ρ2) (e1 ≤ e2) bool.
Proof.
unfold typed_step_ty, typed_step. setoid_rewrite has_type_value.
iIntros (He1 He2 tid) "!#(#HEAP&[H1 H2]&?)".
......@@ -129,7 +129,7 @@ Section typing.
Qed.
Lemma typed_newlft ρ:
typed_step ρ Newlft (λ _, ∃ α, [α]{1} ★ α ∋ top)%P.
typed_step ρ Newlft (λ _, ∃ α, [α]{1} ∗ α ∋ top)%P.
Proof.
iIntros (tid) "!#(_&_&$)". wp_value. iMod lft_begin as (α) "[?#?]". done.
iMod (lft_borrow_create with "[][]") as "[_?]". done. done.
......@@ -137,10 +137,10 @@ Section typing.
Qed.
Lemma typed_endlft κ ρ:
typed_step (κ ∋ ρ ★ [κ]{1}) Endlft (λ _, ρ)%P.
typed_step (κ ∋ ρ ∗ [κ]{1}) Endlft (λ _, ρ)%P.
Proof.
iIntros (tid) "!#(_&[Hextr [Htok #Hlft]]&$)". wp_bind (#() ;; #())%E.
iApply (wp_wand_r _ _ (λ _, _ ★ True)%I). iSplitR "Hextr".
iApply (wp_wand_r _ _ (λ _, _ ∗ True)%I). iSplitR "Hextr".
iApply (wp_frame_step_l with "[-]"); try done.
iDestruct (lft_end with "Hlft Htok") as "$". by wp_seq.
iIntros (v) "[#Hκ _]". iMod (lft_extract_out with "Hκ Hextr"). done.
......@@ -161,18 +161,18 @@ Section typing.
iIntros (tid) "!#(#HEAP&H◁&$)". wp_bind ν.
iApply (has_type_wp with "[$H◁]"). iIntros (v) "[_ H◁]!>".
rewrite has_type_value.
iDestruct "H◁" as (l) "(Hv & >H† & H↦★:)". iDestruct "Hv" as %[=->].
iDestruct "H↦★:" as (vl) "[>H↦ Hown]".
iDestruct "H◁" as (l) "(Hv & >H† & H↦∗:)". iDestruct "Hv" as %[=->].
iDestruct "H↦∗:" as (vl) "[>H↦ Hown]".
rewrite ty_size_eq. iDestruct "Hown" as ">%". wp_free; eauto.
Qed.
Definition consumes (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
∀ ν tid Φ E, mgmtE ∪ lrustN ⊆ E →
ρ1 ν tid ★ tl_own tid ⊤ ★
ρ1 ν tid ∗ tl_own tid ⊤ ∗
(∀ (l:loc) vl q,
(length vl = ty.(ty_size) ★ eval_expr ν = Some #l ★ l ↦★{q} vl ★
|={E}▷=> (ty.(ty_own) tid vl ★ (l ↦★{q} vl ={E}=★ ρ2 ν tid ★ tl_own tid ⊤)))
-★ Φ #l)
(length vl = ty.(ty_size) ∗ eval_expr ν = Some #l ∗ l ↦∗{q} vl ∗
|={E}▷=> (ty.(ty_own) tid vl ∗ (l ↦∗{q} vl ={E}=∗ ρ2 ν tid ∗ tl_own tid ⊤)))
-∗ Φ #l)
⊢ WP ν @ E {{ Φ }}.
Lemma consumes_copy_own ty q:
......@@ -184,7 +184,7 @@ Section typing.
iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ #Hown]".
iAssert (▷ (length vl = ty_size ty))%I with "[#]" as ">%".
by rewrite ty.(ty_size_eq).
iApply "HΦ". iFrame "★#%". iIntros "!>!>!>H↦!>".
iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦!>".
rewrite /has_type Hνv. iExists _. iSplit. done. iFrame. iExists vl. eauto.
Qed.
......@@ -197,14 +197,14 @@ Section typing.
iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
iAssert (▷ (length vl = ty_size ty))%I with "[#]" as ">%".
by rewrite ty.(ty_size_eq).
iApply "HΦ". iFrame "★#%". iIntros "!>!>!>H↦!>".
iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦!>".
rewrite /has_type Hνv. iExists _. iSplit. done. iFrame. iExists vl. eauto.
Qed.
Lemma consumes_copy_uniq_borrow ty κ κ' q:
ty.(ty_dup) →
consumes ty (λ ν, ν ◁ &uniq{κ}ty ★ κ' ⊑ κ ★ [κ']{q})%P
(λ ν, ν ◁ &uniq{κ}ty ★ κ' ⊑ κ ★ [κ']{q})%P.
consumes ty (λ ν, ν ◁ &uniq{κ}ty ∗ κ' ⊑ κ ∗ [κ']{q})%P
(λ ν, ν ◁ &uniq{κ}ty ∗ κ' ⊑ κ ∗ [κ']{q})%P.
Proof.
iIntros (? ν tid Φ E ?) "((H◁ & #H⊑ & Htok & #Hκ') & Htl & HΦ)".
iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
......@@ -214,7 +214,7 @@ Section typing.
iDestruct "H↦" as (vl) "[>H↦ #Hown]".
iAssert (▷ (length vl = ty_size ty))%I with "[#]" as ">%".
by rewrite ty.(ty_size_eq).
iApply "HΦ". iFrame "★#%". iIntros "!>!>!>H↦".
iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦".
iMod (lft_borrow_close with "[H↦] Hclose'") as "[H↦ Htok]". set_solver.
{ iExists _. by iFrame. }
iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
......@@ -222,8 +222,8 @@ Section typing.
Lemma consumes_copy_shr_borrow ty κ κ' q:
ty.(ty_dup) →
consumes ty (λ ν, ν ◁ &shr{κ}ty ★ κ' ⊑ κ ★ [κ']{q})%P
(λ ν, ν ◁ &shr{κ}ty ★ κ' ⊑ κ ★ [κ']{q})%P.
consumes ty (λ ν, ν ◁ &shr{κ}ty ∗ κ' ⊑ κ ∗ [κ']{q})%P
(λ ν, ν ◁ &shr{κ}ty ∗ κ' ⊑ κ ∗ [κ']{q})%P.
Proof.
iIntros (? ν tid Φ E ?) "((H◁ & #H⊑ & [Htok #Hκ']) & Htl & HΦ)".
iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
......@@ -236,14 +236,14 @@ Section typing.
iDestruct "H↦" as (vl) "[>H↦ #Hown]".
iAssert (▷ (length vl = ty_size ty))%I with "[#]" as ">%".
by rewrite ty.(ty_size_eq).
iModIntro. iApply "HΦ". iFrame "★#%". iIntros "!>!>!>H↦".
iModIntro. iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦".
iMod ("Hclose'" with "[H↦]") as "[Htok $]". iExists _; by iFrame.
iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
Qed.
Lemma typed_deref ty ρ1 ρ2 (ν:expr) :
ty.(ty_size) = 1%nat → consumes ty ρ1 ρ2 →
typed_step (ρ1 ν) (!ν) (λ v, v ◁ ty ★ ρ2 ν)%P.
typed_step (ρ1 ν) (!ν) (λ v, v ◁ ty ∗ ρ2 ν)%P.
Proof.
iIntros (Hsz Hconsumes tid) "!#[#HEAP[??]]". wp_bind ν.
iApply Hconsumes. done. iFrame. iIntros (l vl q) "(%&%&H↦&Hupd)".
......@@ -253,9 +253,9 @@ Section typing.
Qed.
Lemma typed_deref_uniq_borrow_own ty ν κ κ' q q':
typed_step (ν ◁ &uniq{κ} own q' ty ★ κ' ⊑ κ ★ [κ']{q})
typed_step (ν ◁ &uniq{κ} own q' ty ∗ κ' ⊑ κ ∗ [κ']{q})
(!ν)
(λ v, v ◁ &uniq{κ} ty ★ κ' ⊑ κ ★ [κ']{q})%P.
(λ v, v ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ [κ']{q})%P.
Proof.
iIntros (tid) "!#(#HEAP & (H◁ & #H⊑ & Htok & #Hκ') & $)". wp_bind ν.
iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
......@@ -275,9 +275,9 @@ Section typing.
Qed.
Lemma typed_deref_shr_borrow_own ty ν κ κ' q q':
typed_step (ν ◁ &shr{κ} own q' ty ★ κ' ⊑ κ ★ [κ']{q})
typed_step (ν ◁ &shr{κ} own q' ty ∗ κ' ⊑ κ ∗ [κ']{q})
(!ν)
(λ v, v ◁ &shr{κ} ty ★ κ' ⊑ κ ★ [κ']{q})%P.
(λ v, v ◁ &shr{κ} ty ∗ κ' ⊑ κ ∗ [κ']{q})%P.
Proof.
iIntros (tid) "!#(#HEAP & (H◁ & #H⊑ & Htok & #Hκ') & $)". wp_bind ν.
iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
......@@ -288,7 +288,7 @@ Section typing.
{ iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; auto. }
iSpecialize ("Hown" $! _ with "Htok2").
iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose'"; last first.
- iApply (wp_frame_step_l _ heapN _ (λ v, l ↦{q'''} v ★ v = #vl)%I); try done.
- iApply (wp_frame_step_l _ heapN _ (λ v, l ↦{q'''} v ∗ v = #vl)%I); try done.
iSplitL "Hown"; last by wp_read; eauto.
iApply step_fupd_mask_mono; last iApply (step_fupd_mask_frame_r _ _ heapN);
last iApply "Hown"; (set_solver || rewrite !disjoint_union_l; solve_ndisj).
......@@ -299,9 +299,9 @@ Section typing.
Qed.
Lemma typed_deref_uniq_borrow_borrow ty ν κ κ' κ'' q:
typed_step (ν ◁ &uniq{κ'} &uniq{κ''} ty ★ κ ⊑ κ' ★ [κ]{q} ★ κ' ⊑ κ'')
typed_step (ν ◁ &uniq{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ [κ]{q} ∗ κ' ⊑ κ'')
(!ν)
(λ v, v ◁ &uniq{κ'} ty ★ κ ⊑ κ' ★ [κ]{q})%P.
(λ v, v ◁ &uniq{κ'} ty ∗ κ ⊑ κ' ∗ [κ]{q})%P.
Proof.
iIntros (tid) "!#(#HEAP & (H◁ & #H⊑1 & [Htok #Hκ'] & #H⊑2) & $)". wp_bind ν.
iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
......@@ -322,9 +322,9 @@ Section typing.
Qed.
Lemma typed_deref_shr_borrow_borrow ty ν κ κ' κ'' q:
typed_step (ν ◁ &shr{κ'} &uniq{κ''} ty ★ κ ⊑ κ' ★ [κ]{q} ★ κ' ⊑ κ'')
typed_step (ν ◁ &shr{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ [κ]{q} ∗ κ' ⊑ κ'')
(!ν)
(λ v, v ◁ &shr{κ'} ty ★ κ ⊑ κ' ★ [κ]{q})%P.
(λ v, v ◁ &shr{κ'} ty ∗ κ ⊑ κ' ∗ [κ]{q})%P.
Proof.
iIntros (tid) "!#(#HEAP & (H◁ & #H⊑1 & [Htok #Hκ'] & #H⊑2) & $)". wp_bind ν.
iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
......@@ -335,7 +335,7 @@ Section typing.
{ iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; auto. }
iSpecialize ("Hown" $! _ _ with "[$H⊑2 $Htok2]"). iApply lft_incl_refl.
iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose'"; last first.
- iApply (wp_frame_step_l _ heapN _ (λ v, l ↦{q''} v ★ v = #l')%I); try done.
- iApply (wp_frame_step_l _ heapN _ (λ v, l ↦{q''} v ∗ v = #l')%I); try done.
iSplitL "Hown"; last by wp_read; eauto.
iApply step_fupd_mask_mono; last iApply (step_fupd_mask_frame_r _ _ heapN);
last iApply "Hown"; (set_solver || rewrite !disjoint_union_l; solve_ndisj).
......@@ -346,11 +346,11 @@ Section typing.
Definition update (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
∀ ν tid Φ E, mgmtE ∪ lrustN ⊆ E →
ρ1 ν tid ★
ρ1 ν tid ∗
(∀ (l:loc) vl,
(length vl = ty.(ty_size) ★ eval_expr ν = Some #l ★ l ↦★ vl ★
∀ vl', l ↦★ vl' ★ ▷ (ty.(ty_own) tid vl') ={E}=★ ρ2 ν tid)
-★ Φ #l)
(length vl = ty.(ty_size) ∗ eval_expr ν = Some #l ∗ l ↦∗ vl ∗
∀ vl', l ↦∗ vl' ∗ ▷ (ty.(ty_own) tid vl') ={E}=∗ ρ2 ν tid)
-∗ Φ #l)
⊢ WP ν @ E {{ Φ }}.
Lemma update_strong ty1 ty2 q:
......@@ -361,14 +361,14 @@ Section typing.
iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & >H† & H↦)".
iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
rewrite ty2.(ty_size_eq) -Hsz. iDestruct "Hown" as ">%". iApply "HΦ". iFrame "★%".
rewrite ty2.(ty_size_eq) -Hsz. iDestruct "Hown" as ">%". iApply "HΦ". iFrame "∗%".
iIntros (vl') "[H↦ Hown']!>". rewrite /has_type Hνv.
iExists _. iSplit. done. iFrame. iExists _. iFrame.
Qed.
Lemma update_weak ty q κ κ':
update ty (λ ν, ν ◁ &uniq{κ} ty ★ κ' ⊑ κ ★ [κ']{q})%P
(λ ν, ν ◁ &uniq{κ} ty ★ κ' ⊑ κ ★ [κ']{q})%P.
update ty (λ ν, ν ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ [κ']{q})%P
(λ ν, ν ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ [κ']{q})%P.
Proof.
iIntros (ν tid Φ E ?) "[(H◁ & #H⊑ & Htok & #Hκ) HΦ]".
iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
......@@ -376,7 +376,7 @@ Section typing.
iMod (lft_incl_trade with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
iMod (lft_borrow_open with "H↦ Htok") as "[H↦ Hclose']". set_solver.
iDestruct "H↦" as (vl) "[>H↦ Hown]". rewrite ty.(ty_size_eq).
iDestruct "Hown" as ">%". iApply "HΦ". iFrame "★%#". iIntros (vl') "[H↦ Hown]".
iDestruct "Hown" as ">%". iApply "HΦ". iFrame "∗%#". iIntros (vl') "[H↦ Hown]".
iMod (lft_borrow_close with "[H↦ Hown] Hclose'") as "[Hbor Htok]". set_solver.
{ iExists _. iFrame. }
iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
......@@ -384,7 +384,7 @@ Section typing.
Lemma typed_assign ρ1 ρ2 ty ν1 ν2:
ty.(ty_size) = 1%nat → update ty ρ1 ρ2 →
typed_step (ρ1 ν1 ★ ν2 ◁ ty) (ν1 <- ν2) (λ _, ρ2 ν1).
typed_step (ρ1 ν1 ∗ ν2 ◁ ty) (ν1 <- ν2) (λ _, ρ2 ν1).
Proof.
iIntros (Hsz Hupd tid) "!#(#HEAP & [Hρ1 H◁] & $)". wp_bind ν1.
iApply Hupd. done. iFrame. iIntros (l vl) "(%&%&H↦&Hupd)".
......@@ -396,14 +396,14 @@ Section typing.
Lemma typed_memcpy ρ1 ρ1' ρ2 ρ2' ty ν1 ν2:
update ty ρ1' ρ1 → consumes ty ρ2' ρ2 →
typed_step (ρ1' ν1 ★ ρ2' ν2) (ν1 <-{ty.(ty_size)} !ν2) (λ _, ρ1 ν1 ★ ρ2 ν2)%P.
typed_step (ρ1' ν1 ∗ ρ2' ν2) (ν1 <-{ty.(ty_size)} !ν2) (λ _, ρ1 ν1 ∗ ρ2 ν2)%P.
Proof.
iIntros (Hupd Hcons tid) "!#(#HEAP&[H1 H2]&Htl)". wp_bind ν1.
iApply (Hupd with "[- $H1]"). done.
iIntros (l vl) "(% & % & H↦ & Hupd)". wp_bind ν2.
iApply (Hcons with "[- $H2 $Htl]"). done.
iIntros (l' vl' q) "(% & % & H↦' & Hcons)". iApply wp_fupd.
iMod "Hcons". iApply wp_memcpy; last iFrame "★#"; try done. iNext.
iMod "Hcons". iApply wp_memcpy; last iFrame "∗#"; try done. iNext.
iIntros "[H↦ H↦']". iMod "Hcons" as "[Hown' Hcons]".
iMod ("Hcons" with "H↦'") as "[$$]". iApply "Hupd". by iFrame.
Qed.
......@@ -416,8 +416,8 @@ Section typing.
Qed.
Lemma typed_program_exists {A} ρ θ e:
(∀ x:A, typed_program (ρ ★ θ x) e) →
typed_program (ρ ★ ∃ x, θ x) e.
(∀ x:A, typed_program (ρ ∗ θ x) e) →
typed_program (ρ ∗ ∃ x, θ x) e.
Proof.
iIntros (Hwt tid) "!#(#HEAP & [Hρ Hθ] & ?)". iDestruct "Hθ" as (x) "Hθ".
iApply Hwt. by iFrame.
......@@ -435,7 +435,7 @@ Section typing.
Lemma typed_if ρ e1 e2 ν:
typed_program ρ e1 → typed_program ρ e2 →
typed_program (ρ ★ ν ◁ bool) (if: ν then e1 else e2).
typed_program (ρ ∗ ν ◁ bool) (if: ν then e1 else e2).
Proof.
iIntros (He1 He2 tid) "!#(#HEAP & [Hρ H◁] & Htl)".
wp_bind ν. iApply has_type_wp. iFrame. iIntros (v) "[% H◁]!>".
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment