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

Use the new validity notations. Curry more things.

parent 81e21a53
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 116 additions and 117 deletions
iris @ 243fdd13
Compare 36c5a842...243fdd13
Subproject commit 36c5a84241841fadffaee32c710680b3c0d88eb0
Subproject commit 243fdd139ccdf1370e5b186650e4323d5e73e54b
theories/derived.v
+ 9
− 9
View file @ 3abc933b
......@@ -25,35 +25,35 @@ Lemma wp_lam E xl e e' el Φ :
Forall (λ ei, is_Some (to_val ei)) el →
Closed (xl +b+ []) e →
subst_l xl el e = Some e' →
▷ WP e' @ E {{ Φ }} ⊢ WP App (Lam xl e) el @ E {{ Φ }}.
▷ WP e' @ E {{ Φ }} -∗ WP App (Lam xl e) el @ E {{ Φ }}.
Proof. iIntros (???) "?". by iApply (wp_rec _ _ BAnon). Qed.
Lemma wp_let E x e1 e2 v Φ :
to_val e1 = Some v →
Closed (x :b: []) e2 →
▷ WP subst' x e1 e2 @ E {{ Φ }} ⊢ WP Let x e1 e2 @ E {{ Φ }}.
▷ WP subst' x e1 e2 @ E {{ Φ }} -∗ WP Let x e1 e2 @ E {{ Φ }}.
Proof. eauto using wp_lam. Qed.
Lemma wp_seq E e1 e2 v Φ :
to_val e1 = Some v →
Closed [] e2 →
▷ WP e2 @ E {{ Φ }} ⊢ WP Seq e1 e2 @ E {{ Φ }}.
▷ WP e2 @ E {{ Φ }} -∗ WP Seq e1 e2 @ E {{ Φ }}.
Proof. iIntros (??) "?". by iApply (wp_let _ BAnon). Qed.
Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊢ WP Skip @ E {{ Φ }}.
Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) -∗ WP Skip @ E {{ Φ }}.
Proof. iIntros. iApply wp_seq. done. iNext. by iApply wp_value. Qed.
Lemma wp_le E (n1 n2 : Z) P Φ :
(n1 ≤ n2 → P ⊢ ▷ |={E}=> Φ (LitV true)) →
(n2 < n1 → P ⊢ ▷ |={E}=> Φ (LitV false)) →
P ⊢ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
(n1 ≤ n2 → P -∗ ▷ |={E}=> Φ (LitV true)) →
(n2 < n1 → P -∗ ▷ |={E}=> Φ (LitV false)) →
P -∗ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
Proof.
intros. rewrite -wp_bin_op //; [].
destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega.
Qed.
Lemma wp_if E (b : bool) e1 e2 Φ :
(if b then ▷ WP e1 @ E {{ Φ }} else ▷ WP e2 @ E {{ Φ }})%I
⊢ WP If (Lit b) e1 e2 @ E {{ Φ }}.
(if b then ▷ WP e1 @ E {{ Φ }} else ▷ WP e2 @ E {{ Φ }})%I -∗
WP If (Lit b) e1 e2 @ E {{ Φ }}.
Proof. iIntros "?". by destruct b; iApply wp_case. Qed.
End derived.
theories/frac_borrow.v
+ 8
− 8
View file @ 3abc933b
......@@ -22,7 +22,7 @@ Section frac_borrow.
Global Instance frac_borrow_persistent : PersistentP (&frac{κ}Φ) := _.
Lemma borrow_fracture φ E κ :
↑lftN ⊆ E → lft_ctx ⊢ &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
↑lftN ⊆ E → lft_ctx -∗ &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
Proof.
iIntros (?) "#LFT Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done.
iMod (borrow_acc_atomic_strong with "LFT Hφ") as "[[Hφ Hclose]|[H† Hclose]]". done.
......@@ -40,7 +40,7 @@ Section frac_borrow.
Lemma frac_borrow_atomic_acc E κ φ :
↑lftN ⊆ E →
lft_ctx ⊢ &frac{κ}φ ={E,E∖↑lftN}=∗ (∃ q, ▷ φ q ∗ (▷ φ q ={E∖↑lftN,E}=∗ True))
lft_ctx -∗ &frac{κ}φ ={E,E∖↑lftN}=∗ (∃ q, ▷ φ q ∗ (▷ φ q ={E∖↑lftN,E}=∗ True))
∨ [†κ] ∗ |={E∖↑lftN,E}=> True.
Proof.
iIntros (?) "#LFT #Hφ". iDestruct "Hφ" as (γ κ') "[Hκκ' Hshr]".
......@@ -53,7 +53,7 @@ Section frac_borrow.
Lemma frac_borrow_acc_strong E q κ Φ:
↑lftN ⊆ E →
lft_ctx ⊢ □ (∀ q1 q2, Φ (q1+q2)%Qp ↔ Φ q1 ∗ Φ q2) -∗
lft_ctx -∗ □ (∀ q1 q2, Φ (q1+q2)%Qp ↔ Φ q1 ∗ Φ q2) -∗
&frac{κ}Φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ Φ q' ∗ (▷ Φ q' ={E}=∗ q.[κ]).
Proof.
iIntros (?) "#LFT #HΦ Hfrac Hκ". unfold frac_borrow.
......@@ -99,20 +99,20 @@ Section frac_borrow.
Lemma frac_borrow_acc E q κ `{Fractional _ Φ} :
↑lftN ⊆ E →
lft_ctx ⊢ &frac{κ}Φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ Φ q' ∗ (▷ Φ q' ={E}=∗ q.[κ]).
lft_ctx -∗ &frac{κ}Φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ Φ q' ∗ (▷ Φ q' ={E}=∗ q.[κ]).
Proof.
iIntros (?) "LFT". iApply (frac_borrow_acc_strong with "LFT"). done.
iIntros "!#*". rewrite fractional. iSplit; auto.
Qed.
Lemma frac_borrow_shorten κ κ' Φ: κ ⊑ κ' ⊢ &frac{κ'}Φ -∗ &frac{κ}Φ.
Lemma frac_borrow_shorten κ κ' Φ: κ ⊑ κ' -∗ &frac{κ'}Φ -∗ &frac{κ}Φ.
Proof.
iIntros "Hκκ' H". iDestruct "H" as (γ κ0) "[H⊑?]". iExists γ, κ0. iFrame.
iApply lft_incl_trans. iFrame.
iIntros "Hκκ' H". iDestruct "H" as (γ κ0) "[#H⊑ ?]". iExists γ, κ0. iFrame.
iApply (lft_incl_trans with "Hκκ' []"). auto.
Qed.
Lemma frac_borrow_incl κ κ' q:
lft_ctx ⊢ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
Proof.
iIntros "#LFT#Hbor!#". iSplitR.
- iIntros (q') "Hκ'".
......
theories/heap.v
+ 3
− 3
View file @ 3abc933b
......@@ -187,7 +187,7 @@ Section heap.
Qed.
Lemma heap_mapsto_vec_prop_op l q1 q2 n (Φ : list val → iProp Σ) :
(∀ vl, Φ vl ⊢ ⌜length vl = n⌝) →
(∀ vl, Φ vl -∗ ⌜length vl = n⌝) →
l ↦∗{q1}: Φ ∗ l ↦∗{q2}: (λ vl, ⌜length vl = n⌝) ⊣⊢ l ↦∗{q1+q2}: Φ.
Proof.
intros Hlen. iSplit.
......@@ -396,7 +396,7 @@ Section heap.
Qed.
Lemma heap_mapsto_lookup l ls q v σ:
own heap_name (● to_heap σ) ⊢
own heap_name (● to_heap σ) -∗
own heap_name (◯ {[ l := (q, to_lock_stateR ls, DecAgree v) ]}) -∗
⌜∃ n' : nat,
σ !! l = Some (match ls with RSt n => RSt (n+n') | WSt => WSt end, v)⌝.
......@@ -414,7 +414,7 @@ Section heap.
Qed.
Lemma heap_mapsto_lookup_1 l ls v σ:
own heap_name (● to_heap σ) ⊢
own heap_name (● to_heap σ) -∗
own heap_name (◯ {[ l := (1%Qp, to_lock_stateR ls, DecAgree v) ]}) -∗
⌜σ !! l = Some (ls, v)⌝.
Proof.
......
theories/lifetime.v
+ 32
− 32
View file @ 3abc933b
......@@ -71,7 +71,7 @@ Hint Unfold lifetime : typeclass_instances.
Section lft.
Context `{invG Σ, lifetimeG Σ}.
Axiom lft_ctx_alloc : True ={∅}=∗ lft_ctx.
Axiom lft_ctx_alloc : (|={∅}=> lft_ctx)%I.
(*** PersitentP, TimelessP, Proper and Fractional instances *)
......@@ -140,41 +140,41 @@ Section lft.
Axiom idx_borrow_acc :
∀ `(↑lftN ⊆ E) q κ i P,
lft_ctx ⊢ idx_borrow κ i P -∗ idx_borrow_own 1 i
lft_ctx -∗ idx_borrow κ i P -∗ idx_borrow_own 1 i
-∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ idx_borrow_own 1 i ∗ q.[κ]).
Axiom idx_borrow_atomic_acc :
∀ `(↑lftN ⊆ E) q κ i P,
lft_ctx ⊢ idx_borrow κ i P -∗ idx_borrow_own q i
lft_ctx -∗ idx_borrow κ i P -∗ idx_borrow_own q i
={E,E∖↑lftN}=∗
▷ P ∗ (▷ P ={E∖↑lftN,E}=∗ idx_borrow_own q i) ∨
[†κ] ∗ (|={E∖↑lftN,E}=> idx_borrow_own q i).
(** Basic borrows *)
Axiom borrow_create :
∀ `(↑lftN ⊆ E) κ P, lft_ctx ⊢ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
Axiom borrow_fake : ∀ `(↑lftN ⊆ E) κ P, lft_ctx ⊢ [†κ] ={E}=∗ &{κ}P.
∀ `(↑lftN ⊆ E) κ P, lft_ctx -∗ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
Axiom borrow_fake : ∀ `(↑lftN ⊆ E) κ P, lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
Axiom borrow_split :
∀ `(↑lftN ⊆ E) κ P Q, lft_ctx ⊢ &{κ}(P ∗ Q) ={E}=∗ &{κ}P ∗ &{κ}Q.
∀ `(↑lftN ⊆ E) κ P Q, lft_ctx -∗ &{κ}(P ∗ Q) ={E}=∗ &{κ}P ∗ &{κ}Q.
Axiom borrow_combine :
∀ `(↑lftN ⊆ E) κ P Q, lft_ctx ⊢ &{κ}P -∗ &{κ}Q ={E}=∗ &{κ}(P ∗ Q).
∀ `(↑lftN ⊆ E) κ P Q, lft_ctx -∗ &{κ}P -∗ &{κ}Q ={E}=∗ &{κ}(P ∗ Q).
Axiom borrow_acc_strong :
∀ `(↑lftN ⊆ E) q κ P,
lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗
lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗
∀ Q, ▷ Q ∗ ▷([†κ] -∗ ▷Q ={⊤ ∖ ↑lftN}=∗ ▷ P) ={E}=∗ &{κ}Q ∗ q.[κ].
Axiom borrow_acc_atomic_strong :
∀ `(↑lftN ⊆ E) κ P,
lft_ctx ⊢ &{κ}P ={E,E∖↑lftN}=∗
lft_ctx -∗ &{κ}P ={E,E∖↑lftN}=∗
(▷ P ∗ ∀ Q, ▷ Q ∗ ▷([†κ] -∗ ▷Q ={⊤ ∖ ↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ}Q) ∨
[†κ] ∗ |={E∖↑lftN,E}=> True.
Axiom borrow_reborrow' :
∀ `(↑lftN ⊆ E) κ κ' P, κ ≼ κ' →
lft_ctx ⊢ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
lft_ctx -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
Axiom borrow_unnest :
∀ `(↑lftN ⊆ E) κ κ' P, lft_ctx ⊢ &{κ'}&{κ}P ={E, E∖↑lftN}▷=∗ &{κ ⋅ κ'}P.
∀ `(↑lftN ⊆ E) κ κ' P, lft_ctx -∗ &{κ'}&{κ}P ={E, E∖↑lftN}▷=∗ &{κ ⋅ κ'}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]".
......@@ -184,13 +184,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 : (|==> q.[static])%I.
Proof.
rewrite /lft_own /static omap_empty fmap_empty.
apply (own_empty lft_tokUR lft_toks_name).
Qed.
Lemma lft_not_dead_static : [† static] ⊢ False.
Lemma lft_not_dead_static : [† static] -∗ False.
Proof.
rewrite /lft_dead /static. setoid_rewrite lookup_empty.
iIntros "HΛ". iDestruct "HΛ" as (Λ) "[% _]". naive_solver.
......@@ -206,7 +206,7 @@ Section lft.
Lemma borrow_acc E q κ P :
↑lftN ⊆ E →
lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
Proof.
iIntros (?) "#LFT HP Htok".
iMod (borrow_acc_strong with "LFT HP Htok") as "[HP Hclose]". done.
......@@ -215,7 +215,7 @@ Section lft.
Lemma borrow_exists {A} E κ (Φ : A → iProp Σ) {_:Inhabited A}:
↑lftN ⊆ E →
lft_ctx ⊢ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
Proof.
iIntros (?) "#LFT Hb".
iMod (borrow_acc_atomic_strong with "LFT Hb") as "[[HΦ Hclose]|[H† Hclose]]". done.
......@@ -224,7 +224,7 @@ Section lft.
Qed.
Lemma borrow_or E κ P Q:
↑lftN ⊆ E → lft_ctx ⊢ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
↑lftN ⊆ E → lft_ctx -∗ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
Proof.
iIntros (?) "#LFT H". rewrite uPred.or_alt.
iMod (borrow_exists with "LFT H") as ([]) "H"; auto.
......@@ -232,7 +232,7 @@ Section lft.
Lemma borrow_persistent E `{PersistentP _ P} κ q:
↑lftN ⊆ E →
lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
Proof.
iIntros (?) "#LFT Hb Htok".
iMod (borrow_acc with "LFT Hb Htok") as "[#HP Hob]". done.
......@@ -249,7 +249,7 @@ Definition lft_incl `{invG Σ, lifetimeG Σ} κ κ' : iProp Σ :=
(□((∀ q, q.[κ] ={↑lftN}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={↑lftN}=∗ q.[κ])) ∗
([†κ'] ={↑lftN}=∗ [†κ])))%I.
Infix "⊑" := lft_incl (at level 60) : C_scope.
Infix "⊑" := lft_incl (at level 60) : uPred_scope.
Section incl.
Context `{invG Σ, lifetimeG Σ}.
......@@ -258,31 +258,31 @@ Section incl.
Lemma lft_incl_acc E κ κ' q:
↑lftN ⊆ E →
κ ⊑ κ' ⊢ 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'.
iIntros "{$Hq'}!>Hq". iApply fupd_mask_mono. eassumption. by iApply "Hclose".
Qed.
Lemma lft_incl_dead E κ κ': ↑lftN ⊆ E → κ ⊑ κ' ⊢ [†κ'] ={E}=∗ [†κ].
Lemma lft_incl_dead E κ κ': ↑lftN ⊆ E → κ ⊑ κ' -∗ [†κ'] ={E}=∗ [†κ].
Proof.
iIntros (?) "#[_ H] Hq". iApply fupd_mask_mono. eassumption. by iApply "H".
Qed.
Lemma lft_le_incl κ κ': κ' ≼ κ → True ⊢ κ ⊑ κ'.
Lemma lft_le_incl κ κ': κ' ≼ κ → (κ ⊑ κ')%I.
Proof.
iIntros ([κ0 ->%leibniz_equiv]) "!#". iSplitR.
- iIntros (q) "[Hκ' Hκ0]". iExists q. iIntros "!>{$Hκ'}Hκ'!>". by iSplitR "Hκ0".
- iIntros "?!>". iApply lft_dead_or. auto.
Qed.
Lemma lft_incl_refl κ : True ⊢ κ ⊑ κ.
Lemma lft_incl_refl κ : (κ ⊑ κ)%I.
Proof. by apply lft_le_incl. Qed.
Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' ∗ κ' ⊑ κ'' ⊢ κ ⊑ κ''.
Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' -∗ κ' ⊑ κ'' -∗ κ ⊑ κ''.
Proof.
unfold lft_incl. iIntros "[#[H1 H1†] #[H2 H2†]]!#". iSplitR.
unfold lft_incl. iIntros "#[H1 H1†] #[H2 H2†]!#". iSplitR.
- iIntros (q) "Hκ".
iMod ("H1" with "*Hκ") as (q') "[Hκ' Hclose]".
iMod ("H2" with "*Hκ'") as (q'') "[Hκ'' Hclose']".
......@@ -292,17 +292,17 @@ Section incl.
Qed.
Axiom idx_borrow_shorten :
∀ κ κ' i P, κ ⊑ κ' ⊢ idx_borrow κ' i P -∗ idx_borrow κ i P.
∀ κ κ' i P, κ ⊑ κ' -∗ idx_borrow κ' i P -∗ idx_borrow κ i P.
Lemma borrow_shorten κ κ' P: κ ⊑ κ' ⊢ &{κ'}P -∗ &{κ}P.
Lemma borrow_shorten κ κ' P: κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
Proof.
iIntros "H⊑ H". unfold borrow. iDestruct "H" as (i) "[??]".
iExists i. iFrame. by iApply (idx_borrow_shorten with "H⊑").
Qed.
Lemma lft_incl_lb κ κ' κ'' : κ ⊑ κ' ∗ κ ⊑ κ'' ⊢ κ ⊑ κ' ⋅ κ''.
Lemma lft_incl_lb κ κ' κ'' : κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ⋅ κ''.
Proof.
iIntros "[#[H1 H1†] #[H2 H2†]]!#". iSplitR.
iIntros "#[H1 H1†] #[H2 H2†]!#". iSplitR.
- iIntros (q) "[Hκ'1 Hκ'2]".
iMod ("H1" with "*Hκ'1") as (q') "[Hκ' Hclose']".
iMod ("H2" with "*Hκ'2") as (q'') "[Hκ'' Hclose'']".
......@@ -314,7 +314,7 @@ Section incl.
- rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
Qed.
Lemma lft_incl_static κ : True ⊢ κ ⊑ static.
Lemma lft_incl_static κ : (κ ⊑ static)%I.
Proof.
iIntros "!#". iSplitR.
- iIntros (q) "?". iExists 1%Qp. iSplitR. by iApply lft_own_static. auto.
......@@ -322,12 +322,12 @@ Section incl.
Qed.
Lemma reborrow E P κ κ':
↑lftN ⊆ E → lft_ctx ⊢ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
Proof.
iIntros (?) "#LFT #H⊑ HP".
iMod (borrow_reborrow' with "LFT HP") as "[Hκ' H∋]". done. by exists κ'.
iDestruct (borrow_shorten with "[H⊑] Hκ'") as "$".
{ iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl. }
{ iApply (lft_incl_lb with "[] []"). done. iApply lft_incl_refl. }
iIntros "!>Hκ'". iApply ("H∋" with "[Hκ']"). iApply lft_dead_or. auto.
Qed.
......
theories/lifting.v
+ 10
− 10
View file @ 3abc933b
......@@ -13,11 +13,11 @@ Implicit Types ef : option expr.
(** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
Lemma wp_bind {E e} K Φ :
WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} -∗ WP fill K e @ E {{ Φ }}.
Proof. exact: wp_ectx_bind. Qed.
Lemma wp_bindi {E e} Ki Φ :
WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} ⊢
WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} -∗
WP fill_item Ki e @ E {{ Φ }}.
Proof. exact: weakestpre.wp_bind. Qed.
......@@ -69,8 +69,8 @@ Lemma wp_read_na1_pst E l Φ :
(|={E,∅}=> ∃ σ n v, ⌜σ !! l = Some(RSt $ n, v)⌝ ∧
▷ ownP σ ∗
▷ (ownP (<[l:=(RSt $ S n, v)]>σ) ={∅,E}=∗
WP Read Na2Ord (Lit $ LitLoc l) @ E {{ Φ }}))
⊢ WP Read Na1Ord (Lit $ LitLoc l) @ E {{ Φ }}.
WP Read Na2Ord (Lit $ LitLoc l) @ E {{ Φ }})) -∗
WP Read Na1Ord (Lit $ LitLoc l) @ E {{ Φ }}.
Proof.
iIntros "HΦP". iApply (wp_lift_head_step E); auto.
iMod "HΦP" as (σ n v) "(%&HΦ&HP)". iModIntro. iExists σ. iSplit. done. iFrame.
......@@ -100,8 +100,8 @@ Lemma wp_write_na1_pst E l v Φ :
(|={E,∅}=> ∃ σ v', ⌜σ !! l = Some(RSt 0, v')⌝ ∧
▷ 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 {{ Φ }}.
WP Write Na2Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }})) -∗
WP Write Na1Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }}.
Proof.
iIntros "HΦP". iApply (wp_lift_head_step E); auto.
iMod "HΦP" as (σ v') "(%&HΦ&HP)". iModIntro. iExists σ. iSplit. done. iFrame.
......@@ -147,8 +147,8 @@ Lemma wp_rec E e f xl erec erec' el Φ :
Forall (λ ei, is_Some (to_val ei)) el →
Closed (f :b: xl +b+ []) erec →
subst_l xl el erec = Some erec' →
▷ WP subst' f e erec' @ E {{ Φ }}
⊢ WP App e el @ E {{ Φ }}.
▷ WP subst' f e erec' @ E {{ Φ }} -∗
WP App e el @ E {{ Φ }}.
Proof.
iIntros (-> ???) "?". iApply wp_lift_pure_det_head_step; subst; eauto.
by intros; inv_head_step; eauto. iNext. rewrite big_sepL_nil. by iFrame.
......@@ -156,7 +156,7 @@ Qed.
Lemma wp_bin_op E op l1 l2 l' Φ :
bin_op_eval op l1 l2 = Some l' →
▷ (|={E}=> Φ (LitV l')) ⊢ WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
▷ (|={E}=> Φ (LitV l')) -∗ WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_pure_det_head_step; eauto.
by intros; inv_head_step; eauto.
......@@ -166,7 +166,7 @@ Qed.
Lemma wp_case E i e el Φ :
0 ≤ i →
nth_error el (Z.to_nat i) = Some e →
▷ WP e @ E {{ Φ }} ⊢ WP Case (Lit $ LitInt i) el @ E {{ Φ }}.
▷ WP e @ E {{ Φ }} -∗ WP Case (Lit $ LitInt i) el @ E {{ Φ }}.
Proof.
iIntros (??) "?". iApply wp_lift_pure_det_head_step; eauto.
by intros; inv_head_step; eauto. iNext. rewrite big_sepL_nil. by iFrame.
......
theories/perm.v
+ 5
− 4
View file @ 3abc933b
......@@ -105,12 +105,13 @@ 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)
⊢ WP ν @ E {{ Φ }}.
(ν ◁ 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.
iIntros "H◁ HΦ". setoid_rewrite has_type_value. unfold has_type.
destruct (eval_expr ν) eqn:EQν; last by iDestruct "H◁" as "[]". simpl.
iMod ("HΦ" $! v with "[$H◁]") as "HΦ". done.
iMod ("HΦ" $! v with "[] H◁") as "HΦ". done.
iInduction ν as [| | |[] e ? [|[]| | | | | | | | | |] _| | | | | | | |] "IH"
forall (Φ v EQν); try done.
- inversion EQν. subst. wp_value. auto.
......
theories/perm_incl.v
+ 3
− 3
View file @ 3abc933b
......@@ -10,13 +10,13 @@ Section defs.
(* Definitions *)
Definition perm_incl (ρ1 ρ2 : perm) :=
∀ tid, lft_ctx ⊢ ρ1 tid ={⊤}=∗ ρ2 tid.
∀ tid, lft_ctx -∗ ρ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_ctx ⊢ ρ tid -∗ ρ1 tid ={⊤}=∗ ρ2 tid ∗ (κ ∋ ρ1)%P tid.
∀ tid, lft_ctx -∗ ρ tid -∗ ρ1 tid ={⊤}=∗ ρ2 tid ∗ (κ ∋ ρ1)%P tid.
End defs.
......@@ -99,7 +99,7 @@ Section props.
Proof. iIntros (tid) "_ _!>". iApply lft_incl_refl. Qed.
Lemma perm_lftincl_trans κ1 κ2 κ3 : κ1 ⊑ κ2 ∗ κ2 ⊑ κ3 ⇒ κ1 ⊑ κ3.
Proof. iIntros (tid) "_ [#?#?]!>". iApply lft_incl_trans. auto. Qed.
Proof. iIntros (tid) "_ [#?#?]!>". iApply (lft_incl_trans with "[] []"); auto. Qed.
Lemma perm_incl_share q ν κ ty :
ν ◁ &uniq{κ} ty ∗ q.[κ] ⇒ ν ◁ &shr{κ} ty ∗ q.[κ].
......
theories/shr_borrow.v
+ 3
− 3
View file @ 3abc933b
......@@ -24,7 +24,7 @@ Section shared_borrows.
Lemma shr_borrow_acc E κ :
↑lftN ⊆ E →
lft_ctx ⊢ &shr{κ}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
lft_ctx -∗ &shr{κ}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
[†κ] ∗ |={E∖↑lftN,E}=> True.
Proof.
iIntros (?) "#LFT #HP". iDestruct "HP" as (i) "(#Hidx&#Hinv)".
......@@ -38,7 +38,7 @@ Section shared_borrows.
Lemma shr_borrow_acc_tok E q κ :
↑lftN ⊆ E →
lft_ctx ⊢ &shr{κ}P -∗ q.[κ] ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ q.[κ]).
lft_ctx -∗ &shr{κ}P -∗ q.[κ] ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ q.[κ]).
Proof.
iIntros (?) "#LFT #Hshr Hκ".
iMod (shr_borrow_acc with "LFT Hshr") as "[[$ Hclose]|[H† _]]". done.
......@@ -46,7 +46,7 @@ Section shared_borrows.
- iDestruct (lft_own_dead with "Hκ H†") as "[]".
Qed.
Lemma shr_borrow_shorten κ κ': κ ⊑ κ' ⊢ &shr{κ'}P -∗ &shr{κ}P.
Lemma shr_borrow_shorten κ κ': κ ⊑ κ' -∗ &shr{κ'}P -∗ &shr{κ}P.
Proof.
iIntros "#H⊑ H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
by iApply (idx_borrow_shorten with "H⊑").
......
theories/tl_borrow.v
+ 2
− 2
View file @ 3abc933b
......@@ -28,7 +28,7 @@ Section tl_borrow.
Lemma tl_borrow_acc q κ E F :
↑lftN ⊆ E → ↑tlN ⊆ E → ↑N ⊆ F →
lft_ctx ⊢ &tl{κ|tid|N}P -∗ q.[κ] -∗ tl_own tid F ={E}=∗
lft_ctx -∗ &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.
......@@ -40,7 +40,7 @@ Section tl_borrow.
iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame.
Qed.
Lemma tl_borrow_shorten κ κ': κ ⊑ κ' ⊢ &tl{κ'|tid|N}P -∗ &tl{κ|tid|N}P.
Lemma tl_borrow_shorten κ κ': κ ⊑ κ' -∗ &tl{κ'|tid|N}P -∗ &tl{κ|tid|N}P.
Proof.
iIntros "Hκκ' H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
iApply (idx_borrow_shorten with "Hκκ' H").
......
theories/type.v
+ 9
− 9
View file @ 3abc933b
......@@ -30,7 +30,7 @@ Record type :=
ty_dup_persistent tid vl : ty_dup → PersistentP (ty_own tid vl);
ty_shr_persistent κ tid E l : PersistentP (ty_shr κ tid E l);
ty_size_eq tid vl : ty_own tid vl ⊢ ⌜length vl = ty_size⌝;
ty_size_eq tid vl : ty_own tid vl -∗ ⌜length vl = ty_size⌝;
(* The mask for starting the sharing does /not/ include the
namespace N, for allowing more flexibility for the user of
this type (typically for the [own] type). AFAIK, there is no
......@@ -41,12 +41,12 @@ Record type :=
more consistent with thread-local tokens, which we do not
give any. *)
ty_share E N κ l tid q : mgmtE ⊥ ↑N → mgmtE ⊆ E →
lft_ctx ⊢ &{κ} (l ↦∗: ty_own tid) -∗ q.[κ] ={E}=∗ ty_shr κ tid (↑N) l ∗ q.[κ];
lft_ctx -∗ &{κ} (l ↦∗: ty_own tid) -∗ q.[κ] ={E}=∗ ty_shr κ tid (↑N) l ∗ q.[κ];
ty_shr_mono κ κ' tid E E' l : E ⊆ E' →
lft_ctx ⊢ κ' ⊑ κ -∗ ty_shr κ tid E l -∗ ty_shr κ' tid E' l;
lft_ctx -∗ κ' ⊑ κ -∗ ty_shr κ tid E l -∗ ty_shr κ' tid E' l;
ty_shr_acc κ tid E F l q :
ty_dup → mgmtE ∪ F ⊆ E →
lft_ctx ⊢ ty_shr κ tid F l -∗
lft_ctx -∗ ty_shr κ tid F l -∗
q.[κ] ∗ tl_own tid F ={E}=∗ ∃ q', ▷l ↦∗{q'}: ty_own tid ∗
(▷l ↦∗{q'}: ty_own tid ={E}=∗ q.[κ] ∗ tl_own tid F)
}.
......@@ -59,7 +59,7 @@ Record simple_type `{iris_typeG Σ} :=
{ st_size : nat;
st_own : thread_id → list val → iProp Σ;
st_size_eq tid vl : st_own tid vl ⊢ ⌜length vl = st_size⌝;
st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = st_size⌝;
st_own_persistent tid vl : PersistentP (st_own tid vl) }.
Global Existing Instance st_own_persistent.
......@@ -244,10 +244,10 @@ Section types.
Qed.
Next Obligation.
intros κ0 ty κ κ' tid E E' l ?. iIntros "#LFT #Hκ #H".
iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0⋅κ' ⊑ κ0⋅κ) as "#Hκ0".
{ iApply lft_incl_lb. iSplit.
iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0⋅κ' ⊑ κ0⋅κ)%I as "#Hκ0".
{ iApply (lft_incl_lb with "[] []").
- iApply lft_le_incl. by exists κ'.
- iApply lft_incl_trans. iSplit; last done.
- iApply (lft_incl_trans with "[] Hκ").
iApply lft_le_incl. exists κ0. apply (comm _). }
iExists l'. iSplit. by iApply (frac_borrow_shorten with "[]"). iIntros (q) "!#Htok".
iApply step_fupd_mask_mono. reflexivity. apply union_preserving_l. eassumption.
......@@ -368,7 +368,7 @@ Section types.
Proof. intros. constructor; done. Qed.
Lemma sum_size_eq n tid i tyl vl {Hn : LstTySize n tyl} :
ty_own (nth i tyl emp) tid vl ⊢ ⌜length vl = n⌝.
ty_own (nth i tyl emp) tid vl -∗ ⌜length vl = n⌝.
Proof.
iIntros "Hown". iDestruct (ty_size_eq with "Hown") as %->.
revert Hn. rewrite /LstTySize List.Forall_forall /= =>Hn.
......
theories/type_incl.v
+ 7
− 8
View file @ 3abc933b
......@@ -9,7 +9,7 @@ Section ty_incl.
Context `{iris_typeG Σ}.
Definition ty_incl (ρ : perm) (ty1 ty2 : type) :=
∀ tid, lft_ctx ⊢ ρ tid ={⊤}=∗
∀ tid, lft_ctx -∗ ρ 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
......@@ -19,7 +19,7 @@ Section ty_incl.
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.
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.
......@@ -74,10 +74,9 @@ Section ty_incl.
iIntros (tid) "#LFT #Hincl!>". iSplit; iIntros "!#*H".
- iDestruct "H" as (l) "[% Hown]". subst. iExists _. iSplit. done.
by iApply (borrow_shorten with "Hincl").
- iAssert (κ1 ⋅ κ ⊑ κ2 ⋅ κ) as "#Hincl'".
{ iApply lft_incl_lb. iSplit.
- iApply lft_incl_trans. iSplit; last done.
iApply lft_le_incl. by exists κ.
- iAssert (κ1 ⋅ κ ⊑ κ2 ⋅ κ)%I as "#Hincl'".
{ iApply (lft_incl_lb with "[] []").
- iApply (lft_incl_trans with "[] Hincl"). iApply lft_le_incl. by exists κ.
- iApply lft_le_incl. exists κ1. by apply (comm _). }
iSplitL; last done. iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'.
iFrame. iIntros (q') "!#Htok".
......@@ -191,7 +190,7 @@ Section ty_incl.
ty_incl ρ (sum tyl1) (sum tyl2).
Proof.
iIntros (DUP FA tid) "#LFT #Hρ". rewrite /sum /=. iSplitR "".
- assert (Hincl : lft_ctx ⊢ ρ tid ={⊤}=∗
- assert (Hincl : lft_ctx -∗ ρ 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].
......@@ -202,7 +201,7 @@ Section ty_incl.
iMod (Hincl with "LFT Hρ") as "#Hincl". iIntros "!>!#*H".
iDestruct "H" as (i vl') "[% Hown]". subst. iExists _, _. iSplit. done.
by iApply "Hincl".
- assert (Hincl : lft_ctx ⊢ ρ tid ={⊤}=∗
- assert (Hincl : lft_ctx -∗ ρ 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].
......
theories/typing.v
+ 24
− 25
View file @ 3abc933b
......@@ -87,7 +87,7 @@ Section typing.
Lemma typed_valuable (ν : expr) ty:
typed_step_ty (ν ◁ ty) ν ty.
Proof.
iIntros (tid) "!#(_&_&H&$)". iApply (has_type_wp with "[$H]"). by iIntros (v) "[_$]".
iIntros (tid) "!#(_&_&H&$)". iApply (has_type_wp with "[$H]"). by iIntros (v) "_ $".
Qed.
Lemma typed_plus e1 e2 ρ1 ρ2:
......@@ -165,7 +165,7 @@ Section typing.
typed_step (ν ◁ own 1 ty) (Free #ty.(ty_size) ν) (λ _, top).
Proof.
iIntros (tid) "!#(#HEAP&_&H◁&$)". wp_bind ν.
iApply (has_type_wp with "[$H◁]"). iIntros (v) "[_ H◁]!>".
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]".
......@@ -174,7 +174,7 @@ Section typing.
Definition consumes (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
∀ ν tid Φ E, mgmtE ∪ ↑lrustN ⊆ E →
lft_ctx ⊢ ρ1 ν tid -∗ tl_own tid ⊤ -∗
lft_ctx -∗ ρ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 ⊤)))
......@@ -184,8 +184,8 @@ Section typing.
Lemma consumes_copy_own ty q:
ty.(ty_dup) → consumes ty (λ ν, ν ◁ own q ty)%P (λ ν, ν ◁ own q ty)%P.
Proof.
iIntros (? ν tid Φ E ?) "_ H◁ Htl HΦ". iApply (has_type_wp with "[- $H◁]").
iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
iIntros (? ν tid Φ E ?) "_ H◁ Htl HΦ". iApply (has_type_wp with "H◁").
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]".
iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">%".
......@@ -198,8 +198,8 @@ Section typing.
consumes ty (λ ν, ν ◁ own q ty)%P
(λ ν, ν ◁ own q (Π(replicate ty.(ty_size) uninit)))%P.
Proof.
iIntros (ν tid Φ E ?) "_ H◁ Htl HΦ". iApply (has_type_wp with "[- $H◁]").
iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
iIntros (ν tid Φ E ?) "_ H◁ Htl HΦ". iApply (has_type_wp with "H◁").
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]".
iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">Hlen".
......@@ -219,7 +219,7 @@ Section typing.
(λ ν, ν ◁ &uniq{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
Proof.
iIntros (? ν tid Φ E ?) "#LFT (H◁ & #H⊑ & Htok) Htl HΦ".
iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁". iDestruct "Hνv" as %Hνv.
rewrite has_type_value. iDestruct "H◁" as (l') "[Heq H↦]". iDestruct "Heq" as %[=->].
iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
iMod (borrow_acc with "LFT H↦ Htok") as "[H↦ Hclose']". set_solver.
......@@ -237,7 +237,7 @@ Section typing.
(λ ν, ν ◁ &shr{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
Proof.
iIntros (? ν tid Φ E ?) "#LFT (H◁ & #H⊑ & Htok) Htl HΦ".
iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁". iDestruct "Hνv" as %Hνv.
rewrite has_type_value. iDestruct "H◁" as (l') "[Heq #Hshr]". iDestruct "Heq" as %[=->].
iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
rewrite (union_difference_L (↑lrustN) ⊤); last done.
......@@ -268,7 +268,7 @@ Section typing.
(λ v, v ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
Proof.
iIntros (tid) "!#(#HEAP & #LFT & (H◁ & #H⊑ & Htok) & $)". wp_bind ν.
iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁!>". iDestruct "Hνv" as %Hνv.
rewrite has_type_value. iDestruct "H◁" as (l) "[Heq H↦]". iDestruct "Heq" as %[=->].
iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[Htok Hclose]". done.
iMod (borrow_acc_strong with "LFT H↦ Htok") as "[H↦ Hclose']". done.
......@@ -288,7 +288,7 @@ Section typing.
(λ v, v ◁ &shr{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
Proof.
iIntros (tid) "!#(#HEAP & #LFT & (H◁ & #H⊑ & Htok) & $)". wp_bind ν.
iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁!>". iDestruct "Hνv" as %Hνv.
rewrite has_type_value. iDestruct "H◁" as (l) "[Heq #H↦]". iDestruct "Heq" as %[=->].
iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[[Htok1 Htok2] Hclose]". done.
iDestruct "H↦" as (vl) "[H↦b Hown]".
......@@ -311,7 +311,7 @@ Section typing.
(λ v, v ◁ &uniq{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
Proof.
iIntros (tid) "!#(#HEAP & #LFT & (H◁ & #H⊑1 & Htok & #H⊑2) & $)". wp_bind ν.
iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁!>". iDestruct "Hνv" as %Hνv.
rewrite has_type_value. iDestruct "H◁" as (l) "[Heq H↦]". iDestruct "Heq" as %[=->].
iMod (lft_incl_acc with "H⊑1 Htok") as (q'') "[Htok Hclose]". done.
iMod (borrow_exists with "LFT H↦") as (vl) "Hbor". done.
......@@ -329,7 +329,7 @@ Section typing.
iMod ("Hclose'" with "[$H↦]") as "[H↦ Htok]".
iMod ("Hclose" with "Htok") as "$". iFrame "#".
iExists _. iSplitR. done. iApply (borrow_shorten with "[] Hbor").
iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl.
iApply (lft_incl_lb with "H⊑2"). iApply lft_incl_refl.
Qed.
Lemma typed_deref_shr_borrow_borrow ty ν κ κ' κ'' q:
......@@ -338,13 +338,13 @@ Section typing.
(λ v, v ◁ &shr{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
Proof.
iIntros (tid) "!#(#HEAP & #LFT & (H◁ & #H⊑1 & Htok & #H⊑2) & $)". wp_bind ν.
iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁!>". iDestruct "Hνv" as %Hνv.
rewrite has_type_value. iDestruct "H◁" as (l) "[Heq Hshr]".
iDestruct "Heq" as %[=->]. iDestruct "Hshr" as (l') "[H↦ Hown]".
iMod (lft_incl_acc with "H⊑1 Htok") as (q') "[[Htok1 Htok2] Hclose]". done.
iMod (frac_borrow_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
iAssert (κ' ⊑ κ'' ⋅ κ') as "#H⊑3".
{ iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl. }
iAssert (κ' ⊑ κ'' ⋅ κ')%I as "#H⊑3".
{ iApply (lft_incl_lb with "H⊑2 []"). iApply lft_incl_refl. }
iMod (lft_incl_acc with "H⊑3 Htok2") as (q''') "[Htok Hclose'']". done.
iSpecialize ("Hown" $! _ with "Htok").
iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose' Hclose''"; last first.
......@@ -361,19 +361,18 @@ Section typing.
Definition update (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
∀ ν tid Φ E, mgmtE ∪ (↑lrustN) ⊆ E →
lft_ctx ⊢ ρ1 ν tid -∗
lft_ctx -∗ ρ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)
-∗ WP ν @ E {{ Φ }}.
∀ vl', l ↦∗ vl' ∗ ▷ (ty.(ty_own) tid vl') ={E}=∗ ρ2 ν tid) -∗ Φ #l) -∗
WP ν @ E {{ Φ }}.
Lemma update_strong ty1 ty2 q:
ty1.(ty_size) = ty2.(ty_size) →
update ty1 (λ ν, ν ◁ own q ty2)%P (λ ν, ν ◁ own q ty1)%P.
Proof.
iIntros (Hsz ν tid Φ E ?) "_ H◁ HΦ". iApply (has_type_wp with "[- $H◁]").
iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
iIntros (Hsz ν tid Φ E ?) "_ H◁ HΦ". iApply (has_type_wp with "H◁").
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 "∗%".
......@@ -386,7 +385,7 @@ Section typing.
(λ ν, ν ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
Proof.
iIntros (ν tid Φ E ?) "#LFT (H◁ & #H⊑ & Htok) HΦ".
iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁". iDestruct "Hνv" as %Hνv.
rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & H↦)". iDestruct "Heq" as %[=->].
iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
iMod (borrow_acc with "LFT H↦ Htok") as "[H↦ Hclose']". set_solver.
......@@ -403,7 +402,7 @@ Section typing.
iIntros (Hsz Hupd tid) "!#(#HEAP & #LFT & [Hρ1 H◁] & $)". wp_bind ν1.
iApply (Hupd with "LFT Hρ1"). done. iFrame. iIntros (l vl) "(%&%&H↦&Hupd)".
rewrite ->Hsz in *. destruct vl as [|v[|]]; try done.
wp_bind ν2. iApply (has_type_wp with "[- $H◁]"). iIntros (v') "[% H◁]!>".
wp_bind ν2. iApply (has_type_wp with "H◁"). iIntros (v') "% H◁!>".
rewrite heap_mapsto_vec_singleton. wp_write.
rewrite -heap_mapsto_vec_singleton has_type_value. iApply "Hupd". by iFrame.
Qed.
......@@ -452,7 +451,7 @@ Section typing.
typed_program (ρ ∗ ν ◁ bool) (if: ν then e1 else e2).
Proof.
iIntros (He1 He2 tid) "!#(#HEAP & #LFT & [Hρ H◁] & Htl)".
wp_bind ν. iApply has_type_wp. iFrame. iIntros (v) "[% H◁]!>".
wp_bind ν. iApply (has_type_wp with "H◁"). iIntros (v) "% H◁!>".
rewrite has_type_value. iDestruct "H◁" as (b) "Heq". iDestruct "Heq" as %[= ->].
wp_if. destruct b; iNext. iApply He1; iFrame "∗#". iApply He2; iFrame "∗#".
Qed.
......
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