Skip to content
GitLab
Commit 8eea9afe authored by Marianna Rapoport's avatar Marianna Rapoport Committed by Ralf Jung
Browse files

Proving ownp.v and including it back into the build

parent 7a6f4567
Hide whitespace changes
Inline Side-by-side
_CoqProject
View file @ 8eea9afe
......@@ -76,7 +76,7 @@ theories/program_logic/language.v
theories/program_logic/ectx_language.v
theories/program_logic/ectxi_language.v
theories/program_logic/ectx_lifting.v
#theories/program_logic/ownp.v
theories/program_logic/ownp.v
theories/program_logic/total_lifting.v
theories/program_logic/total_ectx_lifting.v
theories/program_logic/atomic.v
......
theories/program_logic/ownp.v
View file @ 8eea9afe
......@@ -7,24 +7,29 @@ Set Default Proof Using "Type".
Class ownPG' (Λstate Λobservation: Type) (Σ : gFunctors) := OwnPG {
ownP_invG : invG Σ;
ownP_inG :> inG Σ (authR (optionUR (exclR (prodC (leibnizC Λstate) (leibnizC (list Λobservation))))));
ownP_name : gname;
ownP_state_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))));
ownP_obs_inG :> inG Σ (authR (optionUR (exclR (leibnizC (list Λobservation)))));
ownP_state_name : gname;
ownP_obs_name : gname
}.
Notation ownPG Λ Σ := (ownPG' (state Λ) (observation Λ) Σ).
Instance ownPG_irisG `{ownPG' Λstate Λobservation Σ} : irisG' Λstate Λobservation Σ := {
iris_invG := ownP_invG;
state_interp σ κs := own ownP_name (● (Excl' ((σ:leibnizC Λstate), (κs:leibnizC (list Λobservation)))))
state_interp σ κs := (own ownP_state_name (● (Excl' (σ:leibnizC Λstate))) ∗
own ownP_obs_name (● (Excl' (κs:leibnizC (list Λobservation)))))%I
}.
Global Opaque iris_invG.
Definition ownPΣ (Λstate Λobservation : Type) : gFunctors :=
#[invΣ;
GFunctor (authUR (optionUR (exclR (prodC (leibnizC Λstate) (leibnizC (list Λobservation))))))].
GFunctor (authR (optionUR (exclR (leibnizC Λstate))));
GFunctor (authR (optionUR (exclR (leibnizC (list Λobservation)))))].
Class ownPPreG' (Λstate Λobservation : Type) (Σ : gFunctors) : Set := IrisPreG {
ownPPre_invG :> invPreG Σ;
ownPPre_inG :> inG Σ (authR (optionUR (exclR (prodC (leibnizC Λstate) (leibnizC (list Λobservation))))))
ownPPre_state_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))));
ownPPre_obs_inG :> inG Σ (authR (optionUR (exclR (leibnizC (list Λobservation)))))
}.
Notation ownPPreG Λ Σ := (ownPPreG' (state Λ) (observation Λ) Σ).
......@@ -32,40 +37,54 @@ Instance subG_ownPΣ {Λstate Λobservation Σ} : subG (ownPΣ Λstate Λobserva
Proof. solve_inG. Qed.
(** Ownership *)
Definition ownP `{ownPG' Λstate Λobservation Σ} (σ : Λstate) (κs : list Λobservation) : iProp Σ :=
own ownP_name (◯ (Excl' (σ, κs))).
Typeclasses Opaque ownP.
Instance: Params (@ownP) 3.
Definition ownP_state `{ownPG' Λstate Λobservation Σ} (σ : Λstate) : iProp Σ :=
own ownP_state_name (◯ (Excl' (σ:leibnizC Λstate))).
Definition ownP_obs `{ownPG' Λstate Λobservation Σ} (κs: list Λobservation) : iProp Σ :=
own ownP_obs_name (◯ (Excl' (κs:leibnizC (list Λobservation)))).
Typeclasses Opaque ownP_state ownP_obs.
Instance: Params (@ownP_state) 3.
Instance: Params (@ownP_obs) 3.
(* Adequacy *)
Theorem ownP_adequacy Σ `{ownPPreG Λ Σ} s e σ φ :
(∀ `{ownPG Λ Σ} κs, ownP σ κs ⊢ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
(∀ `{ownPG Λ Σ} κs, ownP_state σ ∗ ownP_obs κs ⊢ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp. apply (wp_adequacy Σ _).
iIntros (? κs). iMod (own_alloc (● (Excl' (σ : leibnizC _, κs : leibnizC _)) ⋅ ◯ (Excl' (σ, κs))))
iIntros (? κs).
iMod (own_alloc (● (Excl' (σ : leibnizC _)) ⋅ ◯ (Excl' σ)))
as (γσ) "[Hσ Hσf]"; first done.
iModIntro. iExists (λ σ κs, own γσ (● (Excl' (σ:leibnizC _, κs:leibnizC _)))). iFrame "Hσ".
iApply (Hwp (OwnPG _ _ _ _ _ γσ)). by rewrite /ownP.
iMod (own_alloc (● (Excl' (κs : leibnizC _)) ⋅ ◯ (Excl' κs)))
as (γκs) "[Hκs Hκsf]"; first done.
iModIntro. iExists (λ σ κs,
own γσ (● (Excl' (σ:leibnizC _))) ∗ own γκs (● (Excl' (κs:leibnizC _))))%I.
iFrame "Hσ Hκs".
iApply (Hwp (OwnPG _ _ _ _ _ _ γσ γκs)). rewrite /ownP_state /ownP_obs. iFrame.
Qed.
Theorem ownP_invariance Σ `{ownPPreG Λ Σ} s e σ1 t2 σ2 φ :
(∀ `{ownPG Λ Σ} κs,
ownP σ1 κs ={⊤}=∗ WP e @ s; ⊤ {{ _, True }} ∗ |={⊤,∅}=> ∃ σ' κs', ownP σ' κs' ∧ ⌜φ σ'⌝) →
ownP_state σ1 ∗ ownP_obs κs ={⊤}=∗ WP e @ s; ⊤ {{ _, True }} ∗
|={⊤,∅}=> ∃ σ' κs', ownP_state σ' ∗ ownP_obs κs' ∧ ⌜φ σ'⌝) →
rtc erased_step ([e], σ1) (t2, σ2) →
φ σ2.
Proof.
intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //.
iIntros (? κs κs').
iMod (own_alloc (● (Excl' ((σ1 : leibnizC _, κs ++ κs' : leibnizC _))) ⋅ ◯ (Excl' (σ1, κs ++ κs'))))
iMod (own_alloc (● (Excl' (σ1 : leibnizC _)) ⋅ ◯ (Excl' σ1)))
as (γσ) "[Hσ Hσf]"; first done.
iExists (λ σ κs', own γσ (● (Excl' (σ:leibnizC _, κs':leibnizC _)))). iFrame "Hσ".
iMod (Hwp (OwnPG _ _ _ _ _ γσ) with "[Hσf]") as "[$ H]"; first by rewrite /ownP.
iIntros "!> Hσ". iMod "H" as (σ2' κs'') "[Hσf %]". rewrite/ownP.
iMod (own_alloc (● (Excl' (κs ++ κs' : leibnizC _)) ⋅ ◯ (Excl' (κs ++ κs'))))
as (γκs) "[Hκs Hκsf]"; first done.
iExists (λ σ κs',
own γσ (● (Excl' (σ:leibnizC _))) ∗ own γκs (● (Excl' (κs':leibnizC _))))%I.
iFrame "Hσ Hκs".
iMod (Hwp (OwnPG _ _ _ _ _ _ γσ γκs) with "[Hσf Hκsf]") as "[$ H]";
first by rewrite /ownP_state /ownP_obs; iFrame.
iIntros "!> [Hσ Hκs]". iMod "H" as (σ2' κs'') "[Hσf [Hκsf %]]". rewrite/ownP_state /ownP_obs.
iDestruct (own_valid_2 with "Hσ Hσf") as %[Hp _]%auth_valid_discrete_2.
pose proof (Excl_included _ _ Hp) as Hp'. apply leibniz_equiv in Hp'. inversion Hp'; subst. auto.
(* TODO (MR) inline this proof in introduction pattern? *)
Qed.
......@@ -76,22 +95,31 @@ Section lifting.
Implicit Types e : expr Λ.
Implicit Types Φ : val Λ → iProp Σ.
Lemma ownP_eq σ1 σ2 κs1 κs2 : state_interp σ1 κs1 -∗ ownP σ2 κs2 -∗ ⌜σ1 = σ2 ∧ κs1 = κs2⌝.
Lemma ownP_eq σ1 σ2 κs1 κs2 : state_interp σ1 κs1 -∗ ownP_state σ2 -∗ ownP_obs κs2 -∗ ⌜σ1 = σ2 ∧ κs1 = κs2⌝.
Proof.
iIntros "Hσ1 Hσ2"; rewrite/ownP.
iDestruct (own_valid_2 with "Hσ1 Hσ2")
as %[Hp _]%auth_valid_discrete_2.
pose proof (Excl_included _ _ Hp) as Hp'. apply leibniz_equiv in Hp'. inversion Hp'; subst. auto.
(* TODO (MR) inline this proof in introduction pattern? *)
iIntros "[Hσ● Hκs●] Hσ◯ Hκs◯". rewrite /ownP_state /ownP_obs.
iDestruct (own_valid_2 with "Hσ● Hσ◯")
as %[Hps _]%auth_valid_discrete_2.
iDestruct (own_valid_2 with "Hκs● Hκs◯")
as %[Hpo _]%auth_valid_discrete_2.
pose proof (leibniz_equiv _ _ (Excl_included _ _ Hps)) as ->.
pose proof (leibniz_equiv _ _ (Excl_included _ _ Hpo)) as ->.
done.
Qed.
Lemma ownP_twice σ1 σ2 κs1 κs2 : ownP σ1 κs1 ∗ ownP σ2 κs2 ⊢ False.
Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
Global Instance ownP_timeless σ κs : Timeless (@ownP (state Λ) (observation Λ) Σ _ σ κs).
Proof. rewrite /ownP; apply _. Qed.
Lemma ownP_state_twice σ1 σ2 : ownP_state σ1 ∗ ownP_state σ2 ⊢ False.
Proof. rewrite /ownP_state -own_op own_valid. by iIntros (?). Qed.
Lemma ownP_obs_twice κs1 κs2 : ownP_obs κs1 ∗ ownP_obs κs2 ⊢ False.
Proof. rewrite /ownP_obs -own_op own_valid. by iIntros (?). Qed.
Global Instance ownP_state_timeless σ : Timeless (@ownP_state (state Λ) (observation Λ) Σ _ σ).
Proof. rewrite /ownP_state; apply _. Qed.
Global Instance ownP_obs_timeless κs : Timeless (@ownP_obs (state Λ) (observation Λ) Σ _ κs).
Proof. rewrite /ownP_obs; apply _. Qed.
Lemma ownP_lift_step s E Φ e1 :
(|={E,∅}=> ∃ σ1 κs, ⌜if s is NotStuck then reducible e1 σ1 else to_val e1 = None⌝ ∗ ▷ ownP σ1 κs ∗
▷ ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ -∗ ownP σ2 κs'
(|={E,∅}=> ∃ σ1 κs, ⌜if s is NotStuck then reducible e1 σ1 else to_val e1 = None⌝ ∗
▷ ownP_state σ1 ∗ ▷ ownP_obs κs ∗
▷ ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ -∗
ownP_state σ2 ∗ ownP_obs κs'
={∅,E}=∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
......@@ -100,26 +128,31 @@ Section lifting.
iMod "H" as (σ1 κs) "[Hred _]"; iDestruct "Hred" as %Hred.
destruct s; last done. apply reducible_not_val in Hred.
move: Hred; by rewrite to_of_val.
- iApply wp_lift_step; [done|]; iIntros (σ1 κs) "Hσ".
iMod "H" as (σ1' κs' ?) "[>Hσf H]". iDestruct (ownP_eq with "Hσ Hσf") as %[-> ->].
- iApply wp_lift_step; [done|]; iIntros (σ1 κs) "Hσκs".
iMod "H" as (σ1' κs' ?) "[>Hσf [>Hκsf H]]". iDestruct (ownP_eq with "Hσκs Hσf Hκsf") as %[-> ->].
iModIntro; iSplit; [by destruct s|]; iNext; iIntros (κ κs'' e2 σ2 efs [Hstep ->]).
rewrite /ownP; iMod (own_update_2 with "Hσ Hσf") as "[Hσ Hσf]".
{ apply auth_update. apply option_local_update.
(exclusive_local_update _ (Excl (σ2, _))). }
iFrame "Hσ". iApply ("H" with "[]"); eauto.
iDestruct "Hσκs" as "[Hσ Hκs]".
rewrite /ownP_state /ownP_obs.
iMod (own_update_2 with "Hσ Hσf") as "[Hσ Hσf]".
{ apply auth_update. apply: option_local_update.
by apply: (exclusive_local_update _ (Excl σ2)). }
iMod (own_update_2 with "Hκs Hκsf") as "[Hκs Hκsf]".
{ apply auth_update. apply: option_local_update.
by apply: (exclusive_local_update _ (Excl (κs'':leibnizC _))). }
iFrame "Hσ Hκs". iApply ("H" with "[]"); eauto with iFrame.
Qed.
Lemma ownP_lift_stuck E Φ e :
(|={E,∅}=> ∃ σ, ⌜stuck e σ⌝ ∗ ▷ ownP σ)
(|={E,∅}=> ∃ σ κs, ⌜stuck e σ⌝ ∗ ▷ (ownP_state σ ∗ ownP_obs κs))
⊢ WP e @ E ?{{ Φ }}.
Proof.
iIntros "H". destruct (to_val e) as [v|] eqn:EQe.
- apply of_to_val in EQe as <-. iApply fupd_wp.
iMod "H" as (σ1) "[H _]". iDestruct "H" as %[Hnv _]. exfalso.
iMod "H" as (σ1 κs) "[H _]". iDestruct "H" as %[Hnv _]. exfalso.
by rewrite to_of_val in Hnv.
- iApply wp_lift_stuck; [done|]. iIntros (σ1) "Hσ".
iMod "H" as (σ1') "(% & >Hσf)".
by iDestruct (ownP_eq with "Hσ Hσf") as %→.
- iApply wp_lift_stuck; [done|]. iIntros (σ1 κs) "Hσ".
iMod "H" as (σ1' κs') "(% & >[Hσf Hκsf])".
by iDestruct (ownP_eq with "Hσ Hσf Hκsf") as %[-> _].
Qed.
Lemma ownP_lift_pure_step `{Inhabited (state Λ)} s E Φ e1 :
......@@ -132,49 +165,53 @@ Section lifting.
iIntros (Hsafe Hstep) "H"; iApply wp_lift_step.
{ specialize (Hsafe inhabitant). destruct s; last done.
by eapply reducible_not_val. }
iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
iModIntro; iSplit; [by destruct s|]; iNext; iIntros (κ e2 σ2 efs ?).
iIntros (σ1 κs) "Hσ". iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
iModIntro; iSplit; [by destruct s|]; iNext; iIntros (κ κs' e2 σ2 efs [??]).
destruct (Hstep σ1 κ e2 σ2 efs); auto; subst.
by iMod "Hclose"; iModIntro; iFrame; iApply "H".
Qed.
(** Derived lifting lemmas. *)
Lemma ownP_lift_atomic_step {s E Φ} e1 σ1 :
Lemma ownP_lift_atomic_step {s E Φ} e1 σ1 κs :
(if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
(▷ ownP σ1 ∗ ▷ ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ -∗ ownP σ2 -∗
(▷ (ownP_state σ1 ∗ ownP_obs κs) ∗
▷ ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ -∗
ownP_state σ2 -∗ ownP_obs κs' -∗
from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "[Hσ H]"; iApply ownP_lift_step.
iIntros (?) "[[Hσ Hκs] H]"; iApply ownP_lift_step.
iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
iModIntro; iExists σ1; iFrame; iSplit; first by destruct s.
iNext; iIntros (κ e2 σ2 efs) "% Hσ".
iDestruct ("H" $! κ e2 σ2 efs with "[] [Hσ]") as "[HΦ $]"; [by eauto..|].
iModIntro; iExists σ1, κs; iFrame; iSplit; first by destruct s.
iNext; iIntros (κ κs' e2 σ2 efs [??]) "[Hσ Hκs]".
iDestruct ("H" $! κ κs' e2 σ2 efs with "[] [Hσ] [Hκs]") as "[HΦ $]"; [by eauto..|].
destruct (to_val e2) eqn:?; last by iExFalso.
iMod "Hclose"; iApply wp_value; last done. by apply of_to_val.
Qed.
Lemma ownP_lift_atomic_det_step {s E Φ e1} σ1 v2 σ2 efs :
Lemma ownP_lift_atomic_det_step {s E Φ e1} σ1 κ κs v2 σ2 efs :
(if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
(∀ κ e2' σ2' efs', prim_step e1 σ1 κ e2' σ2' efs' →
σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
▷ ownP σ1 ∗ ▷ (ownP σ2 -∗
(∀ κ' e2' σ2' efs', prim_step e1 σ1 κ' e2' σ2' efs' →
κ = κ' ∧ σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
▷ (ownP_state σ1 ∗ ownP_obs (cons_obs κ κs)) ∗ ▷ (ownP_state σ2 -∗ ownP_obs κs -∗
Φ v2 ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (? Hdet) "[Hσ1 Hσ2]"; iApply ownP_lift_atomic_step; try done.
iFrame; iNext; iIntros (κ e2' σ2' efs') "% Hσ2'".
edestruct Hdet as (→&Hval&→). done. by rewrite Hval; iApply "Hσ2".
iIntros (? Hdet) "[[Hσ1 Hκs] Hσ2]"; iApply ownP_lift_atomic_step; try done.
iFrame; iNext; iIntros (κ' κs' e2' σ2' efs' (? & Heq)) "Hσ2' Hκs'".
edestruct (Hdet κ') as (->&->&Hval&->); first done. rewrite Hval. apply app_inv_head in Heq as ->.
iApply ("Hσ2" with "Hσ2' Hκs'").
Qed.
Lemma ownP_lift_atomic_det_step_no_fork {s E e1} σ1 v2 σ2 :
Lemma ownP_lift_atomic_det_step_no_fork {s E e1} σ1 κ κs v2 σ2 :
(if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
(∀ κ e2' σ2' efs', prim_step e1 σ1 κ e2' σ2' efs' →
σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
{{{ ▷ ownP σ1 }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}.
(∀ κ' e2' σ2' efs', prim_step e1 σ1 κ' e2' σ2' efs' →
κ = κ' ∧ σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
{{{ ▷ (ownP_state σ1 ∗ ownP_obs (cons_obs κ κs)) }}} e1 @ s; E {{{ RET v2; ownP_state σ2 ∗ ownP_obs κs}}}.
Proof.
intros. rewrite -(ownP_lift_atomic_det_step σ1 v2 σ2 []); [|done..].
rewrite big_sepL_nil right_id. by apply bi.wand_intro_r.
intros. rewrite -(ownP_lift_atomic_det_step σ1 κ κs v2 σ2 []); [|done..].
rewrite big_sepL_nil right_id. apply bi.wand_intro_r. iIntros "[Hs Hs']".
iSplitL "Hs"; first by iFrame. iModIntro. iIntros "Hσ2 Hκs". iApply "Hs'". iFrame.
Qed.
Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
......@@ -184,7 +221,7 @@ Section lifting.
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (? Hpuredet) "?"; iApply ownP_lift_pure_step=>//.
naive_solver. by iNext; iIntros (κ e' efs' σ (→&_&→&→)%Hpuredet).
naive_solver. by iNext; iIntros (κ e' efs' σ (->&_&->&->)%Hpuredet).
Qed.
Lemma ownP_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E Φ} e1 e2 :
......@@ -207,25 +244,26 @@ Section ectx_lifting.
Hint Resolve head_stuck_stuck.
Lemma ownP_lift_head_step s E Φ e1 :
(|={E,∅}=> ∃ σ1, ⌜head_reducible e1 σ1⌝ ∗ ▷ ownP σ1 ∗
▷ ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ -∗ ownP σ2
(|={E,∅}=> ∃ σ1 κs, ⌜head_reducible e1 σ1⌝ ∗ ▷ (ownP_state σ1 ∗ ownP_obs κs) ∗
▷ ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ -∗
ownP_state σ2 -∗ ownP_obs κs'
={∅,E}=∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
iIntros "H". iApply ownP_lift_step.
iMod "H" as (σ1 ?) "[Hσ1 Hwp]". iModIntro. iExists σ1. iSplit.
iMod "H" as (σ1 κs ?) "[>[Hσ1 Hκs] Hwp]". iModIntro. iExists σ1, κs. iSplit.
{ destruct s; try by eauto using reducible_not_val. }
iFrame. iNext. iIntros (κ e2 σ2 efs) "% ?".
iApply ("Hwp" with "[]"); eauto.
iFrame. iNext. iIntros (κ κs' e2 σ2 efs [? ->]) "[Hσ2 Hκs']".
iApply ("Hwp" with "[] Hσ2"); eauto.
Qed.
Lemma ownP_lift_head_stuck E Φ e :
sub_redexes_are_values e →
(|={E,∅}=> ∃ σ, ⌜head_stuck e σ⌝ ∗ ▷ ownP σ)
(|={E,∅}=> ∃ σ κs, ⌜head_stuck e σ⌝ ∗ ▷ (ownP_state σ ∗ ownP_obs κs))
⊢ WP e @ E ?{{ Φ }}.
Proof.
iIntros (?) "H". iApply ownP_lift_stuck. iMod "H" as (σ) "[% >Hσ]".
iExists σ. by auto.
iIntros (?) "H". iApply ownP_lift_stuck. iMod "H" as (σ κs) "[% >[Hσ Hκs]]".
iExists σ, κs. iModIntro. by auto with iFrame.
Qed.
Lemma ownP_lift_pure_head_step s E Φ e1 :
......@@ -240,34 +278,35 @@ Section ectx_lifting.
iNext. iIntros (?????). iApply "H"; eauto.
Qed.
Lemma ownP_lift_atomic_head_step {s E Φ} e1 σ1 :
Lemma ownP_lift_atomic_head_step {s E Φ} e1 σ1 κs :
head_reducible e1 σ1 →
▷ ownP σ1 ∗ ▷ (∀ κ e2 σ2 efs,
⌜head_step e1 σ1 κ e2 σ2 efs⌝ -∗ ownP σ2 -∗
▷ (ownP_state σ1 ∗ ownP_obs κs) ∗ ▷ (∀ κ κs' e2 σ2 efs,
⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ -∗ ownP_state σ2 -∗ ownP_obs κs' -∗
from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "[? H]". iApply ownP_lift_atomic_step; eauto.
iIntros (?) "[Hst H]". iApply ownP_lift_atomic_step; eauto.
{ by destruct s; eauto using reducible_not_val. }
iFrame. iNext. iIntros (????) "% ?". iApply ("H" with "[]"); eauto.
iSplitL "Hst"; first done.
iNext. iIntros (????? [? ->]) "Hσ ?". iApply ("H" with "[] Hσ"); eauto.
Qed.
Lemma ownP_lift_atomic_det_head_step {s E Φ e1} σ1 v2 σ2 efs :
Lemma ownP_lift_atomic_det_head_step {s E Φ e1} σ1 κ κs v2 σ2 efs :
head_reducible e1 σ1 →
(∀ κ e2' σ2' efs', head_step e1 σ1 κ e2' σ2' efs' →
σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
▷ ownP σ1 ∗ ▷ (ownP σ2 -∗ Φ v2 ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
(∀ κ' e2' σ2' efs', head_step e1 σ1 κ' e2' σ2' efs' →
κ = κ' ∧ σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
▷ (ownP_state σ1 ∗ ownP_obs (cons_obs κ κs)) ∗ ▷ (ownP_state σ2 -∗ ownP_obs κs -∗
Φ v2 ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
intros. destruct s; apply ownP_lift_atomic_det_step; try naive_solver.
eauto using reducible_not_val.
intros Hr Hs. destruct s; apply ownP_lift_atomic_det_step; eauto using reducible_not_val.
Qed.
Lemma ownP_lift_atomic_det_head_step_no_fork {s E e1} σ1 v2 σ2 :
Lemma ownP_lift_atomic_det_head_step_no_fork {s E e1} σ1 κ κs v2 σ2 :
head_reducible e1 σ1 →
(∀ κ e2' σ2' efs', head_step e1 σ1 κ e2' σ2' efs' →
σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
{{{ ▷ ownP σ1 }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}.
(∀ κ' e2' σ2' efs', head_step e1 σ1 κ' e2' σ2' efs' →
κ = κ' ∧ σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
{{{ ▷ (ownP_state σ1 ∗ ownP_obs (cons_obs κ κs)) }}} e1 @ s; E {{{ RET v2; ownP_state σ2 ∗ ownP_obs κs }}}.
Proof.
intros ???; apply ownP_lift_atomic_det_step_no_fork; last naive_solver.
by destruct s; eauto using reducible_not_val.
......
Supports Markdown
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