Commit 76a7d9a2 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Lifting lemmas : make the initial state appear under an existential under the...

Lifting lemmas : make the initial state appear under an existential under the view shift. This is still sound, but slightly more expressive.
parent 13117f43
Pipeline #1889 skipped
(** Some derived lemmas for ectx-based languages *)
From iris.program_logic Require Export ectx_language weakestpre lifting.
From iris.program_logic Require Import ownership.
From iris.proofmode Require Import weakestpre.
Section wp.
Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
......@@ -18,14 +19,19 @@ Lemma wp_ectx_bind {E e} K Φ :
Proof. apply: weakestpre.wp_bind. Qed.
Lemma wp_lift_head_step E1 E2
(φ : expr state option expr Prop) Φ e1 σ1 :
(φ : expr state option expr Prop) Φ e1 :
E2 E1 to_val e1 = None
head_reducible e1 σ1
( e2 σ2 ef, head_step e1 σ1 e2 σ2 ef φ e2 σ2 ef)
(|={E1,E2}=> ownP σ1 e2 σ2 ef,
( φ e2 σ2 ef ownP σ2) ={E2,E1}= WP e2 @ E1 {{ Φ }} wp_fork ef)
(|={E1,E2}=> σ1,
head_reducible e1 σ1
( e2 σ2 ef, head_step e1 σ1 e2 σ2 ef φ e2 σ2 ef)
ownP σ1 e2 σ2 ef,
( φ e2 σ2 ef ownP σ2) ={E2,E1}= WP e2 @ E1 {{ Φ }} wp_fork ef)
WP e1 @ E1 {{ Φ }}.
Proof. eauto using wp_lift_step. Qed.
Proof.
iIntros {??} "H". iApply (wp_lift_step E1 E2 φ); try done.
iPvs "H" as {σ1} "(%&%&Hσ1&?)". set_solver. iPvsIntro. iExists σ1.
repeat iSplit; eauto. by iFrame.
Qed.
Lemma wp_lift_pure_head_step E (φ : expr option expr Prop) Φ e1 :
to_val e1 = None
......
......@@ -19,23 +19,24 @@ Implicit Types P Q R : iProp Λ Σ.
Implicit Types Ψ : val Λ iProp Λ Σ.
Lemma ht_lift_step E1 E2
(φ : expr Λ state Λ option (expr Λ) Prop) P P' Φ1 Φ2 Ψ e1 σ1 :
(φ : expr Λ state Λ option (expr Λ) Prop) P P' Φ1 Φ2 Ψ e1 :
E2 E1 to_val e1 = None
reducible e1 σ1
( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef φ e2 σ2 ef)
(P ={E1,E2}=> ownP σ1 P')
(P ={E1,E2}=> σ1,
reducible e1 σ1
( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef φ e2 σ2 ef)
ownP σ1 P')
( e2 σ2 ef, φ e2 σ2 ef ownP σ2 P' ={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 {?? Hsafe Hstep} "#(#Hvs&HΦ&He2&Hef) ! HP".
iApply (wp_lift_step E1 E2 φ _ e1 σ1); auto.
iPvs ("Hvs" with "HP") as "[Hσ HP]"; first set_solver.
iPvsIntro. iNext. iSplitL "Hσ"; [done|iIntros {e2 σ2 ef} "[#Hφ Hown]"].
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; eauto. iFrame.
iNext. iIntros {e2 σ2 ef} "[#Hφ Hown]".
iSpecialize ("HΦ" $! e2 σ2 ef with "[-]"). by iFrame "Hφ HP Hown".
iPvs "HΦ" as "[H1 H2]"; first by set_solver.
iPvsIntro. iSplitL "H1".
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.
......@@ -51,11 +52,11 @@ Proof.
iIntros {? Hsafe Hstep} "#Hef".
set (φ' e σ ef := is_Some (to_val e) φ e σ ef).
iApply (ht_lift_step E E φ' _ P
(λ e2 σ2 ef, ownP σ2 (φ' e2 σ2 ef))%I
(λ e2 σ2 ef, φ e2 σ2 ef P)%I);
try by (rewrite /φ'; eauto using atomic_not_val, atomic_step).
(λ e2 σ2 ef, ownP σ2 (φ' e2 σ2 ef))%I (λ e2 σ2 ef, φ e2 σ2 ef P)%I);
try by (eauto using atomic_not_val).
repeat iSplit.
- by iIntros "! ?".
- iIntros "![Hσ1 HP]". iExists σ1. iPvsIntro. unfold φ'.
repeat iSplit; eauto using atomic_step. by iFrame.
- iIntros {e2 σ2 ef} "! (#Hφ&Hown&HP)"; iPvsIntro.
iSplitL "Hown". by iSplit. iSplit. by iDestruct "Hφ" as %[_ ?]. done.
- iIntros {e2 σ2 ef} "! [Hown #Hφ]"; iDestruct "Hφ" as %[[v2 <-%of_to_val] ?].
......
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import wsat ownership.
From iris.proofmode Require Import pviewshifts.
Local Hint Extern 10 (_ _) => omega.
Local Hint Extern 100 (_ _) => set_solver.
Local Hint Extern 10 ({_} _) =>
......@@ -18,18 +19,19 @@ Implicit Types Φ : val Λ → iProp Λ Σ.
Notation wp_fork ef := (default True ef (flip (wp ) (λ _, True)))%I.
Lemma wp_lift_step E1 E2
(φ : expr Λ state Λ option (expr Λ) Prop) Φ e1 σ1 :
(φ : expr Λ state Λ option (expr Λ) Prop) Φ e1 :
E2 E1 to_val e1 = None
reducible e1 σ1
( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef φ e2 σ2 ef)
(|={E1,E2}=> ownP σ1 e2 σ2 ef,
( φ e2 σ2 ef ownP σ2) ={E2,E1}= WP e2 @ E1 {{ Φ }} wp_fork ef)
(|={E1,E2}=> σ1,
reducible e1 σ1
( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef φ e2 σ2 ef)
ownP σ1 e2 σ2 ef,
( φ e2 σ2 ef ownP σ2) ={E2,E1}= WP e2 @ E1 {{ Φ }} wp_fork ef)
WP e1 @ E1 {{ Φ }}.
Proof.
intros ? He Hsafe Hstep. rewrite pvs_eq wp_eq.
uPred.unseal; split=> n r ? Hvs; constructor; auto.
intros k Ef σ1' rf ???; destruct (Hvs (S k) Ef σ1' rf)
as (r'&(r1&r2&?&?&Hwp)&Hws); auto; clear Hvs; cofe_subst r'.
intros ? He. rewrite pvs_eq wp_eq.
uPred.unseal; split=> n r ? Hvs; constructor; auto. intros k Ef σ1' rf ???.
destruct (Hvs (S k) Ef σ1' rf) as (r'&(σ1&Hsafe&Hstep&r1&r2&?&?&Hwp)&Hws);
auto; clear Hvs; cofe_subst r'.
destruct (wsat_update_pst k (E2 Ef) σ1 σ1' r1 (r2 rf)) as [-> Hws'].
{ apply equiv_dist. rewrite -(ownP_spec k); auto. }
{ by rewrite assoc. }
......@@ -64,24 +66,18 @@ Lemma wp_lift_atomic_step {E Φ} e1
(φ : expr Λ state Λ option (expr Λ) Prop) σ1 :
atomic e1
reducible e1 σ1
( e2 σ2 ef,
prim_step e1 σ1 e2 σ2 ef φ e2 σ2 ef)
( 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)
WP e1 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_step E E (λ e2 σ2 ef,
is_Some (to_val e2) φ e2 σ2 ef) _ e1 σ1) //;
try by (eauto using atomic_not_val, atomic_step).
rewrite -pvs_intro. apply sep_mono, later_mono; first done.
apply forall_intro=>e2'; apply forall_intro=>σ2'.
apply forall_intro=>ef; apply wand_intro_l.
rewrite always_and_sep_l -assoc -always_and_sep_l.
apply pure_elim_l=>-[[v2 Hv] ?] /=.
rewrite -pvs_intro -wp_pvs.
rewrite (forall_elim v2) (forall_elim σ2') (forall_elim ef) pure_equiv //.
rewrite left_id wand_elim_r -(wp_value _ _ e2' v2) //.
by erewrite of_to_val.
iIntros {???} "[Hσ1 Hwp]". iApply (wp_lift_step E E (λ e2 σ2 ef,
is_Some (to_val e2) φ e2 σ2 ef) _ e1); auto using atomic_not_val.
iApply pvs_intro. iExists σ1. repeat iSplit; eauto using atomic_step.
iFrame. iNext. iIntros {e2 σ2 ef} "[#He2 Hσ2]".
iDestruct "He2" as %[[v2 Hv%of_to_val]?]. subst e2.
iDestruct ("Hwp" $! v2 σ2 ef with "[Hσ2]") as "[HΦ ?]". by eauto.
iFrame. iPvs "HΦ". iPvsIntro. iApply wp_value; auto using to_of_val.
Qed.
Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 ef :
......@@ -91,13 +87,10 @@ Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 ef :
σ2 = σ2' to_val e2' = Some v2 ef = ef')
ownP σ1 (ownP σ2 - (|={E}=> Φ v2) wp_fork ef) WP e1 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_atomic_step _ (λ e2' σ2' ef',
σ2 = σ2' to_val e2' = Some v2 ef = ef') σ1) //.
apply sep_mono, later_mono; first done.
apply forall_intro=>e2'; apply forall_intro=>σ2'; apply forall_intro=>ef'.
apply wand_intro_l.
rewrite always_and_sep_l -assoc -always_and_sep_l to_of_val.
apply pure_elim_l=>-[-> [[->] ->]] /=. by rewrite wand_elim_r.
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".
Qed.
Lemma wp_lift_pure_det_step {E Φ} e1 e2 ef :
......@@ -106,9 +99,8 @@ 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.
intros.
rewrite -(wp_lift_pure_step E (λ e2' ef', e2 = e2' ef = ef') _ e1) //=.
apply later_mono, forall_intro=>e'; apply forall_intro=>ef'.
by apply impl_intro_l, pure_elim_l=>-[-> ->].
iIntros {???} "?".
iApply (wp_lift_pure_step E (λ e2' ef', e2 = e2' ef = ef')); try done.
iNext. by iIntros {e' ef' [-> ->] }.
Qed.
End lifting.
Markdown is supported
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