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

Get rid of phi predicates everywhere

parent 6b5ee4fa
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
heap_lang/lifting.v
+ 4
− 8
View file @ 72e8f63c
......@@ -29,14 +29,10 @@ Lemma wp_alloc_pst E σ e v Φ :
⊢ WP Alloc e @ E {{ Φ }}.
Proof.
iIntros {?} "[HP HΦ]".
(* TODO: This works around ssreflect bug #22. *)
set (φ (e' : expr []) σ' ef := ∃ l,
ef = None ∧ e' = Lit (LitLoc l) ∧ σ' = <[l:=v]>σ ∧ σ !! l = None).
iApply (wp_lift_atomic_head_step (Alloc e) φ σ); try (by simpl; eauto);
[by intros; subst φ; inv_head_step; eauto 8|].
iFrame "HP". iNext. iIntros {v2 σ2 ef} "[Hφ HP]".
iDestruct "Hφ" as %(l & -> & [= <-]%of_to_val_flip & -> & ?); simpl.
iSplit; last done. iApply "HΦ"; by iSplit.
iApply (wp_lift_atomic_head_step (Alloc e) σ); try (by simpl; eauto).
iFrame "HP". iNext. iIntros {v2 σ2 ef} "[% HP]". inv_head_step.
match goal with H: _ = of_val v2 |- _ => apply (inj of_val (LitV _)) in H end.
subst v2. iSplit; last done. iApply "HΦ"; by iSplit.
Qed.
Lemma wp_load_pst E σ l v Φ :
......
program_logic/ectx_lifting.v
+ 14
− 9
View file @ 72e8f63c
......@@ -31,22 +31,27 @@ Proof.
iApply "Hwp". by eauto.
Qed.
Lemma wp_lift_pure_head_step E (φ : expr → option expr → Prop) Φ e1 :
Lemma wp_lift_pure_head_step E Φ e1 :
to_val e1 = None →
(∀ σ1, head_reducible e1 σ1) →
(∀ σ1 e2 σ2 ef, head_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
(▷ ∀ e2 ef, ■ φ e2 ef → WP e2 @ E {{ Φ }} ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
Proof. eauto using wp_lift_pure_step. Qed.
(∀ σ1 e2 σ2 ef, head_step e1 σ1 e2 σ2 ef → σ1 = σ2) →
(▷ ∀ e2 ef σ, ■ head_step e1 σ e2 σ ef → WP e2 @ E {{ Φ }} ★ wp_fork ef)
⊢ WP e1 @ E {{ Φ }}.
Proof.
iIntros {???} "H". iApply wp_lift_pure_step; eauto. iNext.
iIntros {????}. iApply "H". eauto.
Qed.
Lemma wp_lift_atomic_head_step {E Φ} e1
(φ : expr → state → option expr → Prop) σ1 :
Lemma wp_lift_atomic_head_step {E Φ} e1 σ1 :
atomic e1 →
head_reducible e1 σ1 →
(∀ e2 σ2 ef, head_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
▷ ownP σ1 ★ ▷ (∀ v2 σ2 ef,
■ φ (of_val v2) σ2 ef ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef)
■ head_step e1 σ1 (of_val v2) σ2 ef ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef)
⊢ WP e1 @ E {{ Φ }}.
Proof. eauto using wp_lift_atomic_step. Qed.
Proof.
iIntros {??} "[? H]". iApply wp_lift_atomic_step; eauto. iFrame. iNext.
iIntros {???} "[% ?]". iApply "H". eauto.
Qed.
Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 ef :
atomic e1 →
......
program_logic/hoare_lifting.v
+ 27
− 32
View file @ 72e8f63c
......@@ -20,37 +20,35 @@ Implicit Types Ψ : val Λ → iProp Λ Σ.
Lemma ht_lift_step E1 E2 P Pσ1 Φ1 Φ2 Ψ e1 :
E2 ⊆ E1 → to_val e1 = None →
(P ={E1,E2}=> ∃ σ1, ■ reducible e1 σ1 ∧
▷ ownP σ1 ★ ▷ Pσ1 σ1) ∧
(∀ σ1 e2 σ2 ef, ■ prim_step e1 σ1 e2 σ2 ef ★ ownP σ2 ★ Pσ1 σ1
={E2,E1}=> Φ1 e2 σ2 ef ★ Φ2 e2 σ2 ef) ∧
(∀ e2 σ2 ef, {{ Φ1 e2 σ2 ef }} e2 @ E1 {{ Ψ }}) ∧
(∀ e2 σ2 ef, {{ Φ2 e2 σ2 ef }} ef ?@ ⊤ {{ _, True }})
(P ={E1,E2}=> ∃ σ1, ■ reducible e1 σ1 ∧ ▷ ownP σ1 ★ ▷ Pσ1 σ1) ∧
(∀ σ1 e2 σ2 ef, ■ prim_step e1 σ1 e2 σ2 ef ★ ownP σ2 ★ Pσ1 σ1
={E2,E1}=> Φ1 e2 σ2 ef ★ Φ2 e2 σ2 ef) ∧
(∀ e2 σ2 ef, {{ Φ1 e2 σ2 ef }} e2 @ E1 {{ Ψ }}) ∧
(∀ e2 σ2 ef, {{ Φ2 e2 σ2 ef }} ef ?@ ⊤ {{ _, True }})
⊢ {{ P }} e1 @ E1 {{ Ψ }}.
Proof.
iIntros {??} "#(#Hvs&HΦ&He2&Hef) ! HP".
iApply (wp_lift_step E1 E2 _ e1); auto.
iPvs ("Hvs" with "HP") as {σ1} "(%&Hσ&HP)"; first set_solver.
iPvsIntro. iExists σ1. repeat iSplit. by eauto. iFrame.
iNext. iIntros {e2 σ2 ef} "[#Hφ Hown]".
iSpecialize ("HΦ" $! σ1 e2 σ2 ef with "[-]"). by iFrame "Hφ HP Hown".
iNext. iIntros {e2 σ2 ef} "[#Hstep Hown]".
iSpecialize ("HΦ" $! σ1 e2 σ2 ef with "[-]"). by iFrame "Hstep HP Hown".
iPvs "HΦ" as "[H1 H2]"; first by set_solver. iPvsIntro. iSplitL "H1".
- by iApply "He2".
- destruct ef as [e|]; last done. by iApply ("Hef" $! _ _ (Some e)).
Qed.
Lemma ht_lift_atomic_step
E (φ : expr Λ → state Λ → option (expr Λ) → Prop) P e1 σ1 :
Lemma ht_lift_atomic_step E P e1 σ1 :
atomic e1 →
reducible e1 σ1 →
(∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
(∀ e2 σ2 ef, {{ ■ φ e2 σ2 ef ★ P }} ef ?@ ⊤ {{ _, True }}) ⊢
{{ ▷ ownP σ1 ★ ▷ P }} e1 @ E {{ v, ∃ σ2 ef, ownP σ2 ★ ■ φ (of_val v) σ2 ef }}.
(∀ e2 σ2 ef, {{ ■ prim_step e1 σ1 e2 σ2 ef ★ P }} ef ?@ ⊤ {{ _, True }}) ⊢
{{ ▷ ownP σ1 ★ ▷ P }} e1 @ E {{ v, ∃ σ2 ef, ownP σ2
★ ■ prim_step e1 σ1 (of_val v) σ2 ef }}.
Proof.
iIntros {? Hsafe Hstep} "#Hef".
set (φ' (_:state Λ) e σ ef := is_Some (to_val e) ∧ φ e σ ef).
iIntros {? Hsafe} "#Hef".
iApply (ht_lift_step E E _ (λ σ1', P ∧ σ1 = σ1')%I
(λ e2 σ2 ef, ownP σ2 ★ ■ (φ' σ1 e2 σ2 ef))%I (λ e2 σ2 ef, ■ φ e2 σ2 ef ★ P)%I);
(λ e2 σ2 ef, ownP σ2 ★ ■ (is_Some (to_val e2) ∧ prim_step e1 σ1 e2 σ2 ef))%I
(λ e2 σ2 ef, ■ prim_step e1 σ1 e2 σ2 ef ★ P)%I);
try by (eauto using atomic_not_val).
repeat iSplit.
- iIntros "![Hσ1 HP]". iExists σ1. iPvsIntro.
......@@ -62,35 +60,32 @@ Proof.
- done.
Qed.
Lemma ht_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) P P' Ψ e1 :
Lemma ht_lift_pure_step E P P' Ψ e1 :
to_val e1 = None →
(∀ σ1, reducible e1 σ1) →
(∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
(∀ e2 ef, {{ ■ φ e2 ef ★ P }} e2 @ E {{ Ψ }}) ∧
(∀ e2 ef, {{ ■ φ e2 ef ★ P' }} ef ?@ ⊤ {{ _, True }})
(∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2) →
(∀ e2 ef σ, {{ ■ prim_step e1 σ e2 σ ef ★ P }} e2 @ E {{ Ψ }}) ∧
(∀ e2 ef σ, {{ ■ prim_step e1 σ e2 σ ef ★ P' }} ef ?@ ⊤ {{ _, True }})
⊢ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}.
Proof.
iIntros {? Hsafe Hstep} "[#He2 #Hef] ! HP".
iApply (wp_lift_pure_step E φ _ e1); auto.
iNext; iIntros {e2 ef Hφ}. iDestruct "HP" as "[HP HP']"; iSplitL "HP".
iIntros {? Hsafe Hpure} "[#He2 #Hef] ! HP". iApply wp_lift_pure_step; auto.
iNext; iIntros {e2 ef σ Hstep}. iDestruct "HP" as "[HP HP']"; iSplitL "HP".
- iApply "He2"; by iSplit.
- destruct ef as [e|]; last done.
iApply ("Hef" $! _ (Some e)); by iSplit.
- destruct ef as [e|]; last done. iApply ("Hef" $! _ (Some e)); by iSplit.
Qed.
Lemma ht_lift_pure_det_step
E (φ : expr Λ → option (expr Λ) → Prop) P P' Ψ e1 e2 ef :
Lemma ht_lift_pure_det_step E P P' Ψ e1 e2 ef :
to_val e1 = None →
(∀ σ1, reducible e1 σ1) →
(∀ σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ ef = ef')→
{{ P }} e2 @ E {{ Ψ }} ∧ {{ P' }} ef ?@ ⊤ {{ _, True }}
⊢ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}.
Proof.
iIntros {? Hsafe Hdet} "[#He2 #Hef]".
iApply (ht_lift_pure_step _ (λ e2' ef', e2 = e2' ∧ ef = ef')); eauto.
iSplit; iIntros {e2' ef'}.
- iIntros "! [#He ?]"; iDestruct "He" as %[-> ->]. by iApply "He2".
iIntros {? Hsafe Hpuredet} "[#He2 #Hef]".
iApply ht_lift_pure_step; eauto. by intros; eapply Hpuredet.
iSplit; iIntros {e2' ef' σ}.
- iIntros "! [% ?]". edestruct Hpuredet as (_&->&->). done. by iApply "He2".
- destruct ef' as [e'|]; last done.
iIntros "! [#He ?]"; iDestruct "He" as %[-> ->]. by iApply "Hef".
iIntros "! [% ?]". edestruct Hpuredet as (_&->&->). done. by iApply "Hef".
Qed.
End lifting.
program_logic/lifting.v
+ 14
− 17
View file @ 72e8f63c
......@@ -40,17 +40,18 @@ Proof.
exists r1', r2'; split_and?; try done. by uPred.unseal; intros ? ->.
Qed.
Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Φ e1 :
Lemma wp_lift_pure_step E Φ e1 :
to_val e1 = None →
(∀ σ1, reducible e1 σ1) →
(∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
(▷ ∀ e2 ef, ■ φ e2 ef → WP e2 @ E {{ Φ }} ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
(∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2) →
(▷ ∀ e2 ef σ, ■ prim_step e1 σ e2 σ ef → WP e2 @ E {{ Φ }} ★ wp_fork ef)
⊢ WP e1 @ E {{ Φ }}.
Proof.
intros He Hsafe Hstep; rewrite wp_eq; uPred.unseal.
split=> n r ? Hwp; constructor; auto.
intros k Ef σ1 rf ???; split; [done|]. destruct n as [|n]; first lia.
intros e2 σ2 ef ?; destruct (Hstep σ1 e2 σ2 ef); auto; subst.
destruct (Hwp e2 ef k r) as (r1&r2&Hr&?&?); auto.
destruct (Hwp e2 ef σ1 k r) as (r1&r2&Hr&?&?); auto.
exists r1,r2; split_and?; try done.
- rewrite -Hr; eauto using wsat_le.
- uPred.unseal; by intros ? ->.
......@@ -59,16 +60,14 @@ Qed.
(** Derived lifting lemmas. *)
Import uPred.
Lemma wp_lift_atomic_step {E Φ} e1
(φ : expr Λ → state Λ → option (expr Λ) → Prop) σ1 :
Lemma wp_lift_atomic_step {E Φ} e1 σ1 :
atomic e1 →
reducible e1 σ1 →
(∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
▷ ownP σ1 ★ ▷ (∀ v2 σ2 ef,
■ φ (of_val v2) σ2 ef ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef)
■ prim_step e1 σ1 (of_val v2) σ2 ef ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef)
⊢ WP e1 @ E {{ Φ }}.
Proof.
iIntros {???} "[Hσ1 Hwp]". iApply (wp_lift_step E E _ e1); auto using atomic_not_val.
iIntros {??} "[Hσ1 Hwp]". iApply (wp_lift_step E E _ e1); auto using atomic_not_val.
iPvsIntro. iExists σ1. repeat iSplit; eauto 10 using atomic_step.
iFrame. iNext. iIntros {e2 σ2 ef} "[% Hσ2]".
edestruct @atomic_step as [v2 Hv%of_to_val]; eauto. subst e2.
......@@ -80,13 +79,12 @@ Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 ef :
atomic e1 →
reducible e1 σ1 →
(∀ e2' σ2' ef', prim_step e1 σ1 e2' σ2' ef' →
σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') →
σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') →
▷ ownP σ1 ★ ▷ (ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
Proof.
iIntros {???} "[Hσ1 Hσ2]". iApply (wp_lift_atomic_step _ (λ e2' σ2' ef',
σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') σ1); try done. iFrame. iNext.
iIntros {v2' σ2' ef'} "[#Hφ Hσ2']". rewrite to_of_val.
iDestruct "Hφ" as %(->&[= ->]&->). by iApply "Hσ2".
iIntros {?? Hdet} "[Hσ1 Hσ2]". iApply (wp_lift_atomic_step _ σ1); try done.
iFrame. iNext. iIntros {v2' σ2' ef'} "[% Hσ2']".
edestruct Hdet as (->&->%of_to_val%(inj of_val)&->). done. by iApply "Hσ2".
Qed.
Lemma wp_lift_pure_det_step {E Φ} e1 e2 ef :
......@@ -95,8 +93,7 @@ Lemma wp_lift_pure_det_step {E Φ} e1 e2 ef :
(∀ σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ ef = ef')→
▷ (WP e2 @ E {{ Φ }} ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
Proof.
iIntros {???} "?".
iApply (wp_lift_pure_step E (λ e2' ef', e2 = e2' ∧ ef = ef')); try done.
iNext. by iIntros {e' ef' [-> ->] }.
iIntros {?? Hpuredet} "?". iApply (wp_lift_pure_step E); try done.
by intros; eapply Hpuredet. iNext. by iIntros {e' ef' σ (_&->&->)%Hpuredet}.
Qed.
End lifting.
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