Skip to content

GitLab

I
Iris
Commit 4ec14182 authored by Ralf Jung's avatar Ralf Jung
Browse files
Options

tweak WP def.n and fix eauto in heap_lang

parent f7991ef5
Show whitespace changes
Inline Side-by-side
Showing with 124 additions and 145 deletions
theories/heap_lang/lang.v
View file @ 4ec14182
......@@ -167,6 +167,7 @@ Definition val_is_unboxed (v : val) : Prop :=
(** The state: heaps of vals. *)
Definition state : Type := gmap loc val * gset proph.
Implicit Type σ : state.
(** Equality and other typeclass stuff *)
Lemma to_of_val v : to_val (of_val v) = Some v.
......
theories/heap_lang/lifting.v
View file @ 4ec14182
......@@ -48,11 +48,15 @@ Ltac inv_head_step :=
end.
Local Hint Extern 0 (atomic _ _) => solve_atomic.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _; simpl.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl.
Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl.
Local Hint Constructors head_step.
Local Hint Resolve alloc_fresh.
(* [simpl apply] is too stupid, so we need extern hints here. *)
Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasSucS.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasFailS.
Local Hint Extern 0 (head_step (Alloc _) _ _ _ _ _) => apply alloc_fresh.
Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_fresh.
Local Hint Resolve to_of_val.
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
......@@ -134,10 +138,8 @@ Lemma wp_alloc s E e v :
{{{ True }}} Alloc e @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
Proof.
iIntros (<- Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>"; iSplit.
(* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
{ iPureIntro. repeat eexists. by apply alloc_fresh. }
iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
iIntros (σ1 κ κs) "[Hσ Hκs] !>"; iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
......@@ -146,9 +148,7 @@ Lemma twp_alloc s E e v :
[[{ True }]] Alloc e @ s; E [[{ l, RET LitV (LitLoc l); l ↦ v }]].
Proof.
iIntros (<- Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>"; iSplit.
(* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
{ iPureIntro. repeat eexists. by apply alloc_fresh. }
iIntros (σ1 κs) "[Hσ Hκs] !>"; iSplit; first by eauto.
iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
......@@ -158,9 +158,8 @@ Lemma wp_load s E l q v :
{{{ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ s; E {{{ RET v; l ↦{q} v }}}.
Proof.
iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto.
iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma twp_load s E l q v :
......@@ -168,8 +167,7 @@ Lemma twp_load s E l q v :
Proof.
iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto.
iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
......@@ -179,11 +177,8 @@ Lemma wp_store s E l v' e v :
Proof.
iIntros (<- Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit.
(* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
{ iPureIntro. repeat eexists. constructor; eauto. }
iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
Qed.
......@@ -194,10 +189,7 @@ Proof.
iIntros (<- Φ) "Hl HΦ".
iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit.
(* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
{ iPureIntro. repeat eexists. constructor; eauto. }
iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
......@@ -209,8 +201,8 @@ Lemma wp_cas_fail s E l q v' e1 v1 e2 :
Proof.
iIntros (<- [v2 <-] ?? Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma twp_cas_fail s E l q v' e1 v1 e2 :
......@@ -232,11 +224,8 @@ Lemma wp_cas_suc s E l e1 v1 e2 v2 :
Proof.
iIntros (<- <- ? Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit.
(* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
{ iPureIntro. repeat eexists. by econstructor. }
iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
Qed.
......@@ -248,10 +237,7 @@ Proof.
iIntros (<- <- ? Φ) "Hl HΦ".
iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit.
(* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
{ iPureIntro. repeat eexists. by econstructor. }
iIntros (κ v2' σ2 efs Hstep); inv_head_step.
iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
......@@ -263,11 +249,8 @@ Lemma wp_faa s E l i1 e2 i2 :
Proof.
iIntros (<- Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit.
(* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
{ iPureIntro. repeat eexists. by constructor. }
iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
Qed.
......@@ -279,10 +262,7 @@ Proof.
iIntros (<- Φ) "Hl HΦ".
iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit.
(* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
{ iPureIntro. repeat eexists. by constructor. }
iIntros (κ v2' σ2 efs Hstep); inv_head_step.
iSplit; first by eauto. iIntros (κ e2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
......@@ -292,12 +272,10 @@ Lemma wp_new_proph :
{{{ True }}} NewProph {{{ v (p : proph), RET (LitV (LitProphecy p)); p ⥱ v }}}.
Proof.
iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR". iSplit.
(* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
{ iPureIntro. repeat eexists. by apply new_proph_fresh. }
unfold cons_obs. simpl.
iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]). inv_head_step.
iMod ((@proph_map_alloc _ _ _ _ _ _ _ p) with "HR") as "[HR Hp]".
iIntros (σ1 κ κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
iMod (@proph_map_alloc with "HR") as "[HR Hp]".
{ intro Hin. apply (iffLR (elem_of_subseteq _ _) Hdom) in Hin. done. }
iModIntro; iSplit=> //. iFrame. iSplitL "HR".
- iExists _. iSplit; last done.
......@@ -313,12 +291,11 @@ Lemma wp_resolve_proph e1 e2 p v w:
{{{ p ⥱ v }}} ResolveProph e1 e2 {{{ RET (LitV LitUnit); ⌜v = Some w⌝ }}}.
Proof.
iIntros (<- <- Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
iDestruct (@proph_map_valid with "HR Hp") as %Hlookup. iSplit.
(* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
{ iPureIntro. repeat eexists. by constructor. }
unfold cons_obs. simpl.
iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step. iApply fupd_frame_l.
iIntros (σ1 κ κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
iDestruct (@proph_map_valid with "HR Hp") as %Hlookup.
iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. iApply fupd_frame_l.
iSplit=> //. iFrame.
iMod (@proph_map_remove with "HR Hp") as "Hp". iModIntro.
iSplitR "HΦ".
......
theories/program_logic/adequacy.v
View file @ 4ec14182
......@@ -78,8 +78,8 @@ Lemma wp_step s E e1 σ1 κ κs e2 σ2 efs Φ :
Proof.
rewrite {1}wp_unfold /wp_pre. iIntros (?) "[(Hw & HE & Hσ) H]".
rewrite (val_stuck e1 σ1 κ e2 σ2 efs) // uPred_fupd_eq.
iMod ("H" $! σ1 _ with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame.
iMod ("H" $! κ κs e2 σ2 efs with "[//] [$Hw $HE]") as ">(Hw & HE & H)".
iMod ("H" $! σ1 with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame.
iMod ("H" $! e2 σ2 efs with "[//] [$Hw $HE]") as ">(Hw & HE & H)".
iIntros "!> !>". by iMod ("H" with "[$Hw $HE]") as ">($ & $ & $)".
Qed.
......@@ -145,7 +145,7 @@ Proof.
rewrite wp_unfold /wp_pre. iIntros "(Hw&HE&Hσ) H".
destruct (to_val e) as [v|] eqn:?.
{ iIntros "!> !> !%". left. by exists v. }
rewrite uPred_fupd_eq. iMod ("H" with "Hσ [-]") as ">(?&?&%&?)"; first by iFrame.
rewrite uPred_fupd_eq. iMod ("H" $! _ None with "Hσ [-]") as ">(?&?&%&?)"; first by iFrame.
iIntros "!> !> !%". by right.
Qed.
......
theories/program_logic/ectx_lifting.v
View file @ 4ec14182
......@@ -16,28 +16,28 @@ Hint Resolve head_stuck_stuck.
Lemma wp_lift_head_step_fupd {s E Φ} e1 :
to_val e1 = None →
(∀ σ1 κs, state_interp σ1 κs ={E,∅}=∗
(∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E,∅}=∗
⌜head_reducible e1 σ1⌝ ∗
∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={∅,∅,E}▷=∗
state_interp σ2 κs' ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
state_interp σ2 κs ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_step_fupd=>//. iIntros (σ1 κs) "Hσ".
iIntros (?) "H". iApply wp_lift_step_fupd=>//. iIntros (σ1 κ κs) "Hσ".
iMod ("H" with "Hσ") as "[% H]"; iModIntro.
iSplit; first by destruct s; eauto. iIntros (κ κs' e2 σ2 efs [Hstep ->]).
iSplit; first by destruct s; eauto. iIntros (e2 σ2 efs Hstep).
iApply "H"; eauto.
Qed.
Lemma wp_lift_head_step {s E Φ} e1 :
to_val e1 = None →
(∀ σ1 κs, state_interp σ1 κs ={E,∅}=∗
(∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E,∅}=∗
⌜head_reducible e1 σ1⌝ ∗
▷ ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={∅,E}=∗
state_interp σ2 κs' ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
state_interp σ2 κs ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_head_step_fupd; [done|]. iIntros (??) "?".
iMod ("H" with "[$]") as "[$ H]". iIntros "!>" (κ κs' e2 σ2 efs ?) "!> !>". by iApply "H".
iIntros (?) "H". iApply wp_lift_head_step_fupd; [done|]. iIntros (???) "?".
iMod ("H" with "[$]") as "[$ H]". iIntros "!>" (e2 σ2 efs ?) "!> !>". by iApply "H".
Qed.
Lemma wp_lift_head_stuck E Φ e :
......@@ -76,61 +76,61 @@ Qed.
Lemma wp_lift_atomic_head_step_fupd {s E1 E2 Φ} e1 :
to_val e1 = None →
(∀ σ1 κs, state_interp σ1 κs ={E1}=∗
(∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E1}=∗
⌜head_reducible e1 σ1⌝ ∗
∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E1,E2}▷=∗
state_interp σ2 κs' ∗
∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
state_interp σ2 κs ∗
from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E1 {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
iIntros (σ1 κs) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
iSplit; first by destruct s; auto. iIntros (κ κs' e2 σ2 efs [Hstep ->]).
iIntros (σ1 κ κs) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
iSplit; first by destruct s; auto. iIntros (e2 σ2 efs Hstep).
iApply "H"; eauto.
Qed.
Lemma wp_lift_atomic_head_step {s E Φ} e1 :
to_val e1 = None →
(∀ σ1 κs, state_interp σ1 κs ={E}=∗
(∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E}=∗
⌜head_reducible e1 σ1⌝ ∗
▷ ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E}=∗
state_interp σ2 κs' ∗
▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
state_interp σ2 κs ∗
from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
iIntros (σ1 κs) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
iSplit; first by destruct s; auto. iNext. iIntros (κ κs' e2 σ2 efs [Hstep ->]).
iIntros (σ1 κ κs) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
iSplit; first by destruct s; auto. iNext. iIntros (e2 σ2 efs Hstep).
iApply "H"; eauto.
Qed.
Lemma wp_lift_atomic_head_step_no_fork_fupd {s E1 E2 Φ} e1 :
Lemma wp_lift_atomic__head_step_no_fork_fupd {s E1 E2 Φ} e1 :
to_val e1 = None →
(∀ σ1 κs, state_interp σ1 κs ={E1}=∗
(∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E1}=∗
⌜head_reducible e1 σ1⌝ ∗
∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E1,E2}▷=∗
⌜efs = []⌝ ∗ state_interp σ2 κs' ∗ from_option Φ False (to_val e2))
∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
⌜efs = []⌝ ∗ state_interp σ2 κs ∗ from_option Φ False (to_val e2))
⊢ WP e1 @ s; E1 {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_atomic_head_step_fupd; [done|].
iIntros (σ1 κs) "Hσ1". iMod ("H" $! σ1 κs with "Hσ1") as "[$ H]"; iModIntro.
iIntros (κ κs' v2 σ2 efs [Hstep ->]).
iMod ("H" $! κ κs' v2 σ2 efs with "[# //]") as "H".
iIntros (σ1 κ κs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
iIntros (v2 σ2 efs Hstep).
iMod ("H" $! v2 σ2 efs with "[# //]") as "H".
iIntros "!> !>". iMod "H" as "(% & $ & $)"; subst; auto.
Qed.
Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e1 :
to_val e1 = None →
(∀ σ1 κs, state_interp σ1 κs ={E}=∗
(∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E}=∗
⌜head_reducible e1 σ1⌝ ∗
▷ ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E}=∗
⌜efs = []⌝ ∗ state_interp σ2 κs' ∗ from_option Φ False (to_val e2))
▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
⌜efs = []⌝ ∗ state_interp σ2 κs ∗ from_option Φ False (to_val e2))
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto.
iIntros (σ1 κs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
iNext; iIntros (κ κs' v2 σ2 efs Hstep).
iMod ("H" $! κ κs' v2 σ2 efs with "[# //]") as "(% & $ & $)". subst; auto.
iIntros (σ1 κ κs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
iNext; iIntros (v2 σ2 efs Hstep).
iMod ("H" $! v2 σ2 efs with "[# //]") as "(% & $ & $)". subst; auto.
Qed.
Lemma wp_lift_pure_det_head_step {s E E' Φ} e1 e2 efs :
......
theories/program_logic/lifting.v
View file @ 4ec14182
......@@ -15,15 +15,15 @@ Hint Resolve reducible_no_obs_reducible.
Lemma wp_lift_step_fupd s E Φ e1 :
to_val e1 = None →
(∀ σ1 κs, state_interp σ1 κs ={E,∅}=∗
(∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E,∅}=∗
⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={∅,∅,E}▷=∗
state_interp σ2 κs' ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
state_interp σ2 κs ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1 κs) "Hσ".
rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1 κ κs) "Hσ".
iMod ("H" with "Hσ") as "(%&H)". iModIntro. iSplit. by destruct s.
iIntros (????? [? ->]). iApply "H". eauto.
iIntros (????). iApply "H". eauto.
Qed.
Lemma wp_lift_stuck E Φ e :
......@@ -31,21 +31,21 @@ Lemma wp_lift_stuck E Φ e :
(∀ σ κs, state_interp σ κs ={E,∅}=∗ ⌜stuck e σ⌝)
⊢ WP e @ E ?{{ Φ }}.
Proof.
rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1 κs) "Hσ".
rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1 κ κs) "Hσ".
iMod ("H" with "Hσ") as %[? Hirr]. iModIntro. iSplit; first done.
iIntros (κ ? e2 σ2 efs [? ->]). by case: (Hirr κ e2 σ2 efs).
iIntros (e2 σ2 efs ?). by case: (Hirr κ e2 σ2 efs).
Qed.
(** Derived lifting lemmas. *)
Lemma wp_lift_step s E Φ e1 :
to_val e1 = None →
(∀ σ1 κs, state_interp σ1 κs ={E,∅}=∗
(∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E,∅}=∗
⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
▷ ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={∅,E}=∗
state_interp σ2 κs' ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
state_interp σ2 κs ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_step_fupd; [done|]. iIntros (??) "Hσ".
iIntros (?) "H". iApply wp_lift_step_fupd; [done|]. iIntros (???) "Hσ".
iMod ("H" with "Hσ") as "[$ H]". iIntros "!> * % !>". by iApply "H".
Qed.
......@@ -59,10 +59,10 @@ Proof.
iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
{ specialize (Hsafe inhabitant). destruct s; last done.
by eapply reducible_not_val. }
iIntros (σ1 κs) "Hσ". iMod "H".
iIntros (σ1 κ κs) "Hσ". iMod "H".
iMod fupd_intro_mask' as "Hclose"; last iModIntro; first by set_solver. iSplit.
{ iPureIntro. destruct s; done. }
iNext. iIntros (κ κs' e2 σ2 efs [Hstep' ->]).
iNext. iIntros (e2 σ2 efs Hstep').
destruct (Hstep κ σ1 e2 σ2 efs); auto; subst; clear Hstep.
iMod "Hclose" as "_". iFrame "Hσ". iMod "H". iApply "H"; auto.
Qed.
......@@ -82,18 +82,18 @@ Qed.
use the generic lemmas here. *)
Lemma wp_lift_atomic_step_fupd {s E1 E2 Φ} e1 :
to_val e1 = None →
(∀ σ1 κs, state_interp σ1 κs ={E1}=∗
(∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E1}=∗
⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E1,E2}▷=∗
state_interp σ2 κs' ∗
∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
state_interp σ2 κs ∗
from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E1 {{ Φ }}.
Proof.
iIntros (?) "H". iApply (wp_lift_step_fupd s E1 _ e1)=>//; iIntros (σ1 κs) "Hσ1".
iIntros (?) "H". iApply (wp_lift_step_fupd s E1 _ e1)=>//; iIntros (σ1 κ κs) "Hσ1".
iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
iMod (fupd_intro_mask' E1 ∅) as "Hclose"; first set_solver.
iIntros "!>" (κ κs' e2 σ2 efs ?). iMod "Hclose" as "_".
iMod ("H" $! κ κs' e2 σ2 efs with "[#]") as "H"; [done|].
iIntros "!>" (e2 σ2 efs ?). iMod "Hclose" as "_".
iMod ("H" $! e2 σ2 efs with "[#]") as "H"; [done|].
iMod (fupd_intro_mask' E2 ∅) as "Hclose"; [set_solver|]. iIntros "!> !>".
iMod "Hclose" as "_". iMod "H" as "($ & HΦ & $)".
destruct (to_val e2) eqn:?; last by iExFalso.
......@@ -102,16 +102,16 @@ Qed.
Lemma wp_lift_atomic_step {s E Φ} e1 :
to_val e1 = None →
(∀ σ1 κs, state_interp σ1 κs ={E}=∗
(∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E}=∗
⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
▷ ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E}=∗
state_interp σ2 κs' ∗
▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
state_interp σ2 κs ∗
from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
iIntros (??) "?". iMod ("H" with "[$]") as "[$ H]".
iIntros "!> *". iIntros ([Hstep ->]) "!> !>".
iIntros (???) "?". iMod ("H" with "[$]") as "[$ H]".
iIntros "!> *". iIntros (Hstep) "!> !>".
by iApply "H".
Qed.
......
theories/program_logic/ownp.v
View file @ 4ec14182
......@@ -128,9 +128,10 @@ 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σκ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 ->]).
- 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 (e2 σ2 efs Hstep).
iDestruct "Hσκs" as "[Hσ Hκs]".
rewrite /ownP_state /ownP_obs.
iMod (own_update_2 with "Hσ Hσf") as "[Hσ Hσf]".
......@@ -138,7 +139,7 @@ Section lifting.
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 _))). }
by apply: (exclusive_local_update _ (Excl (κs:leibnizC _))). }
iFrame "Hσ Hκs". iApply ("H" with "[]"); eauto with iFrame.
Qed.
......@@ -165,8 +166,8 @@ Section lifting.
iIntros (Hsafe Hstep) "H"; iApply wp_lift_step.
{ specialize (Hsafe inhabitant). destruct s; last done.
by eapply reducible_not_val. }
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 [??]).
iIntros (σ1 κ κs) "Hσ". iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
iModIntro; iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs ?).
destruct (Hstep σ1 κ e2 σ2 efs); auto; subst.
by iMod "Hclose"; iModIntro; iFrame; iApply "H".
Qed.
......
theories/program_logic/total_weakestpre.v
View file @ 4ec14182
......@@ -188,9 +188,9 @@ Lemma twp_wp s E e Φ : WP e @ s; E [{ Φ }] -∗ WP e @ s; E {{ Φ }}.
Proof.
iIntros "H". iLöb as "IH" forall (E e Φ).
rewrite wp_unfold twp_unfold /wp_pre /twp_pre. destruct (to_val e) as [v|]=>//.
iIntros (σ1 κs) "Hσ". iMod ("H" with "Hσ") as "[% H]". iIntros "!>". iSplitR.
iIntros (σ1 κ κs) "Hσ". iMod ("H" with "Hσ") as "[% H]". iIntros "!>". iSplitR.
{ destruct s; last done. eauto using reducible_no_obs_reducible. }
iIntros (κ κs' e2 σ2 efs [Hstep ->]). iMod ("H" $! _ _ _ _ Hstep) as "(% & Hst & H & Hfork)".
iIntros (e2 σ2 efs Hstep). iMod ("H" $! _ _ _ _ Hstep) as "(% & Hst & H & Hfork)".
subst κ. iFrame "Hst".
iApply step_fupd_intro; [set_solver+|]. iNext.
iSplitL "H". by iApply "IH". iApply (@big_sepL_impl with "[$Hfork]").
......
theories/program_logic/weakestpre.v
View file @ 4ec14182
......@@ -17,11 +17,11 @@ Definition wp_pre `{irisG Λ Σ} (s : stuckness)
coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
match to_val e1 with
| Some v => |={E}=> Φ v
| None => ∀ σ1 κs,
state_interp σ1 κs ={E,∅}=∗ ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
∀ κ (κs' : list (observation Λ)) e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={∅,∅,E}▷=∗
state_interp σ2 κs' ∗ wp E e2 Φ ∗
[∗ list] ef ∈ efs, wp ⊤ ef (λ _, True)
| None => ∀ σ1 κ κs, </