Commit 46e20e91 authored by Ralf Jung's avatar Ralf Jung

get rid of observations in ownP, they just make porting harder

parent 0acafd48
......@@ -5,69 +5,58 @@ From iris.algebra Require Import auth.
From iris.proofmode Require Import tactics classes.
Set Default Proof Using "Type".
Class ownPG' (Λstate Λobservation: Type) (Σ : gFunctors) := OwnPG {
Class ownPG' (Λstate Λobservation : Type) (Σ : gFunctors) := OwnPG {
ownP_invG : invG Σ;
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
ownP_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))));
ownP_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_state_name ( (Excl' (σ:leibnizC Λstate)))
own ownP_obs_name ( (Excl' (κs:leibnizC (list Λobservation)))))%I
state_interp σ κs := (own ownP_name ( (Excl' (σ:leibnizC Λstate))))%I
}.
Global Opaque iris_invG.
Definition ownPΣ (Λstate Λobservation : Type) : gFunctors :=
Definition ownPΣ (Λstate : Type) : gFunctors :=
#[invΣ;
GFunctor (authR (optionUR (exclR (leibnizC Λstate))));
GFunctor (authR (optionUR (exclR (leibnizC (list Λobservation)))))].
GFunctor (authR (optionUR (exclR (leibnizC Λstate))))].
Class ownPPreG' (Λstate Λobservation : Type) (Σ : gFunctors) : Set := IrisPreG {
Class ownPPreG' (Λstate : Type) (Σ : gFunctors) : Set := IrisPreG {
ownPPre_invG :> invPreG Σ;
ownPPre_state_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))));
ownPPre_obs_inG :> inG Σ (authR (optionUR (exclR (leibnizC (list Λobservation)))))
ownPPre_state_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))))
}.
Notation ownPPreG Λ Σ := (ownPPreG' (state Λ) (observation Λ) Σ).
Notation ownPPreG Λ Σ := (ownPPreG' (state Λ) Σ).
Instance subG_ownPΣ {Λstate Λobservation Σ} : subG (ownPΣ Λstate Λobservation) Σ ownPPreG' Λstate Λobservation Σ.
Instance subG_ownPΣ {Λstate Σ} : subG (ownPΣ Λstate) Σ ownPPreG' Λstate Σ.
Proof. solve_inG. Qed.
(** Ownership *)
Definition ownP_state `{ownPG' Λstate Λobservation Σ} (σ : Λstate) : iProp Σ :=
own ownP_state_name ( (Excl' (σ:leibnizC Λstate))).
Definition ownP `{ownPG' Λstate Λobservation Σ} (σ : Λstate) : iProp Σ :=
own ownP_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.
Typeclasses Opaque ownP.
Instance: Params (@ownP) 3.
(* Adequacy *)
Theorem ownP_adequacy Σ `{ownPPreG Λ Σ} s e σ φ :
( `{ownPG Λ Σ} κs, ownP_state σ ownP_obs κs WP e @ s; {{ v, ⌜φ v }})
( `{ownPG Λ Σ}, ownP σ WP e @ s; {{ v, ⌜φ v }})
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp. apply (wp_adequacy Σ _).
iIntros (? κs).
iMod (own_alloc ( (Excl' (σ : leibnizC _)) (Excl' σ)))
as (γσ) "[Hσ Hσf]"; first done.
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.
own γσ ( (Excl' (σ:leibnizC _))))%I.
iFrame "Hσ".
iApply (Hwp (OwnPG _ _ _ _ _ γσ)). rewrite /ownP. iFrame.
Qed.
Theorem ownP_invariance Σ `{ownPPreG Λ Σ} s e σ1 t2 σ2 φ :
( `{ownPG Λ Σ} κs,
ownP_state σ1 ownP_obs κs ={}= WP e @ s; {{ _, True }}
|={,}=> σ' κs', ownP_state σ' ownP_obs κs' ⌜φ σ')
( `{ownPG Λ Σ},
ownP σ1 ={}= WP e @ s; {{ _, True }}
|={,}=> σ', ownP σ' ⌜φ σ')
rtc erased_step ([e], σ1) (t2, σ2)
φ σ2.
Proof.
......@@ -75,14 +64,12 @@ Proof.
iIntros (? κs κs').
iMod (own_alloc ( (Excl' (σ1 : leibnizC _)) (Excl' σ1)))
as (γσ) "[Hσ Hσf]"; first done.
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.
own γσ ( (Excl' (σ:leibnizC _))))%I.
iFrame "Hσ".
iMod (Hwp (OwnPG _ _ _ _ _ γσ) with "[Hσf]") as "[$ H]";
first by rewrite /ownP; iFrame.
iIntros "!> Hσ". iMod "H" as (σ2') "[Hσf %]". rewrite/ownP.
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.
Qed.
......@@ -95,65 +82,54 @@ Section lifting.
Implicit Types e : expr Λ.
Implicit Types Φ : val Λ iProp Σ.
Lemma ownP_eq σ1 σ2 κs1 κs2 : state_interp σ1 κs1 - ownP_state σ2 - ownP_obs κs2 - ⌜σ1 = σ2 κs1 = κs2.
Lemma ownP_eq σ1 σ2 κs : state_interp σ1 κs - ownP σ2 - ⌜σ1 = σ2.
Proof.
iIntros "[Hσ● Hκs●] Hσ◯ Hκs◯". rewrite /ownP_state /ownP_obs.
iIntros "Hσ● Hσ◯". rewrite /ownP.
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_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_state_twice σ1 σ2 : ownP σ1 ownP σ2 False.
Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
Global Instance ownP_timeless σ : Timeless (@ownP (state Λ) (observation Λ) Σ _ σ).
Proof. rewrite /ownP; 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_state σ1 ownP_obs κs
κ κs' e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs κs = κ ++ κs' -
ownP_state σ2 ownP_obs κs'
(|={E,}=> σ1, 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
={,E}= WP e2 @ s; E {{ Φ }} [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E {{ Φ }}.
Proof.
iIntros "H". destruct (to_val e1) as [v|] eqn:EQe1.
- apply of_to_val in EQe1 as <-. iApply fupd_wp.
iMod "H" as (σ1 κs) "[Hred _]"; iDestruct "Hred" as %Hred.
iMod "H" as (σ1) "[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σκs".
iMod "H" as (σ1' κs' ?) "[>Hσf [>Hκsf H]]".
iDestruct (ownP_eq with "Hσκs Hσf Hκsf") as %[<- <-].
iMod "H" as (σ1' ?) "[>Hσf H]".
iDestruct (ownP_eq with "Hσκs Hσf") as %<-.
iModIntro; iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs Hstep).
iDestruct "Hσκs" as "[Hσ Hκs]".
rewrite /ownP_state /ownP_obs.
iDestruct "Hσκs" as "Hσ". rewrite /ownP.
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.
iFrame "Hσ". iApply ("H" with "[]"); eauto with iFrame.
Qed.
Lemma ownP_lift_stuck E Φ e :
(|={E,}=> σ κs, stuck e σ⌝ (ownP_state σ ownP_obs κs))
(|={E,}=> σ, stuck e σ⌝ (ownP σ))
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 κs) "[H _]". iDestruct "H" as %[Hnv _]. exfalso.
iMod "H" as (σ1) "[H _]". iDestruct "H" as %[Hnv _]. exfalso.
by rewrite to_of_val in Hnv.
- 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 %[-> _].
iMod "H" as (σ1') "(% & >Hσf)".
by iDestruct (ownP_eq with "Hσ Hσf") as %->.
Qed.
Lemma ownP_lift_pure_step `{Inhabited (state Λ)} s E Φ e1 :
......@@ -173,46 +149,46 @@ Section lifting.
Qed.
(** Derived lifting lemmas. *)
Lemma ownP_lift_atomic_step {s E Φ} e1 σ1 κs :
Lemma ownP_lift_atomic_step {s E Φ} e1 σ1 :
(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 = κ ++ κs' -
ownP_state σ2 - ownP_obs κs' -
( (ownP σ1)
κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs -
ownP σ2 -
from_option Φ False (to_val e2) [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "[[Hσ Hκs] H]"; iApply ownP_lift_step.
iIntros (?) "[ H]"; iApply ownP_lift_step.
iMod (fupd_intro_mask' E ) as "Hclose"; first set_solver.
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..|].
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..|].
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 κ κs v2 σ2 efs :
Lemma ownP_lift_atomic_det_step {s E Φ e1} σ1 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_state σ1 ownP_obs (κ ++ κs)) (ownP_state σ2 - ownP_obs κs -
σ2 = σ2' to_val e2' = Some v2 efs = efs')
(ownP σ1) (ownP σ2 -
Φ v2 [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E {{ Φ }}.
Proof.
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'").
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&->); first done. rewrite Hval.
iApply ("Hσ2" with "Hσ2'").
Qed.
Lemma ownP_lift_atomic_det_step_no_fork {s E e1} σ1 κ κs v2 σ2 :
Lemma ownP_lift_atomic_det_step_no_fork {s E e1} σ1 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_state σ1 ownP_obs (κ ++ κs)) }}} e1 @ s; E {{{ RET v2; ownP_state σ2 ownP_obs κs}}}.
σ2 = σ2' to_val e2' = Some v2 [] = efs')
{{{ (ownP σ1) }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}.
Proof.
intros. rewrite -(ownP_lift_atomic_det_step σ1 κ κs v2 σ2 []); [|done..].
intros. rewrite -(ownP_lift_atomic_det_step σ1 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.
iSplitL "Hs"; first by iFrame. iModIntro. iIntros "Hσ2". iApply "Hs'". iFrame.
Qed.
Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
......@@ -245,26 +221,26 @@ Section ectx_lifting.
Hint Resolve head_stuck_stuck.
Lemma ownP_lift_head_step s E Φ e1 :
(|={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 = κ ++ κs' -
ownP_state σ2 - ownP_obs κs'
(|={E,}=> σ1, head_reducible e1 σ1 (ownP σ1)
κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs -
ownP σ2
={,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 κs ?) "[>[Hσ1 Hκs] Hwp]". iModIntro. iExists σ1, κs. iSplit.
iMod "H" as (σ1 ?) "[>Hσ1 Hwp]". iModIntro. iExists σ1. iSplit.
{ destruct s; try by eauto using reducible_not_val. }
iFrame. iNext. iIntros (κ κs' e2 σ2 efs [? ->]) "[Hσ2 Hκs']".
iFrame. iNext. iIntros (κ e2 σ2 efs ?) "Hσ2".
iApply ("Hwp" with "[] Hσ2"); eauto.
Qed.
Lemma ownP_lift_head_stuck E Φ e :
sub_redexes_are_values e
(|={E,}=> σ κs, head_stuck e σ⌝ (ownP_state σ ownP_obs κs))
(|={E,}=> σ, head_stuck e σ⌝ (ownP σ))
WP e @ E ?{{ Φ }}.
Proof.
iIntros (?) "H". iApply ownP_lift_stuck. iMod "H" as (σ κs) "[% >[Hσ Hκs]]".
iExists σ, κs. iModIntro. by auto with iFrame.
iIntros (?) "H". iApply ownP_lift_stuck. iMod "H" as (σ) "[% >Hσ]".
iExists σ. iModIntro. by auto with iFrame.
Qed.
Lemma ownP_lift_pure_head_step s E Φ e1 :
......@@ -279,35 +255,37 @@ Section ectx_lifting.
iNext. iIntros (?????). iApply "H"; eauto.
Qed.
Lemma ownP_lift_atomic_head_step {s E Φ} e1 σ1 κs :
Lemma ownP_lift_atomic_head_step {s E Φ} e1 σ1 :
head_reducible e1 σ1
(ownP_state σ1 ownP_obs κs) ( κ κs' e2 σ2 efs,
head_step e1 σ1 κ e2 σ2 efs κs = κ ++ κs' - ownP_state σ2 - ownP_obs κs' -
(ownP σ1) ( κ e2 σ2 efs,
head_step e1 σ1 κ e2 σ2 efs - ownP σ2 -
from_option Φ False (to_val e2) [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "[Hst H]". iApply ownP_lift_atomic_step; eauto.
{ by destruct s; eauto using reducible_not_val. }
iSplitL "Hst"; first done.
iNext. iIntros (????? [? ->]) "Hσ ?". iApply ("H" with "[] Hσ"); eauto.
iNext. iIntros (???? ?) "Hσ". iApply ("H" with "[] Hσ"); eauto.
Qed.
Lemma ownP_lift_atomic_det_head_step {s E Φ e1} σ1 κ κs v2 σ2 efs :
Lemma ownP_lift_atomic_det_head_step {s E Φ e1} σ1 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_state σ1 ownP_obs (κ ++ κs)) (ownP_state σ2 - ownP_obs κs -
Φ v2 [ list] ef efs, WP ef @ s; {{ _, True }})
σ2 = σ2' to_val e2' = Some v2 efs = efs')
(ownP σ1) (ownP σ2 -
Φ v2 [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E {{ Φ }}.
Proof.
intros Hr Hs. destruct s; apply ownP_lift_atomic_det_step; eauto using reducible_not_val.
intros Hr Hs.
destruct s; apply ownP_lift_atomic_det_step; eauto using reducible_not_val;
intros; eapply Hs; eauto 10.
Qed.
Lemma ownP_lift_atomic_det_head_step_no_fork {s E e1} σ1 κ κs v2 σ2 :
Lemma ownP_lift_atomic_det_head_step_no_fork {s E e1} σ1 κ 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_state σ1 ownP_obs (κ ++ κs)) }}} e1 @ s; E {{{ RET v2; ownP_state σ2 ownP_obs κs }}}.
{{{ (ownP σ1) }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}.
Proof.
intros ???; apply ownP_lift_atomic_det_step_no_fork; last naive_solver.
by destruct s; eauto using reducible_not_val.
......
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