Commit 0b7b5ad0 authored by Marianna Rapoport's avatar Marianna Rapoport Committed by Ralf Jung
Browse files

Finalizing general (not prophecy specific) support for observations

- Removing head of list of observations after each reduction step in definition of wp
- Adding support for observations to state_interp and world
- Applying Ralf's suggestions to previous commit (e.g. replacing /\ and -> with unicode characters)
parent 936eeb48
......@@ -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
......
......@@ -17,8 +17,8 @@ Definition heap_adequacy Σ `{heapPreG Σ} s e σ φ :
( `{heapG Σ}, WP e @ s; {{ v, ⌜φ v }}%I)
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
iMod (gen_heap_init σ) as (?) "Hh".
iModIntro. iExists gen_heap_ctx. iFrame "Hh".
iModIntro. iExists (fun σ _ => gen_heap_ctx σ). iFrame "Hh".
iApply (Hwp (HeapG _ _ _)).
Qed.
......@@ -108,7 +108,7 @@ Inductive val :=
Bind Scope val_scope with val.
Inductive observation := prophecy_observation_todo.
Definition observation := Empty val.
Fixpoint of_val (v : val) : expr :=
match v with
......
......@@ -14,7 +14,7 @@ Class heapG Σ := HeapG {
Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
iris_invG := heapG_invG;
state_interp := gen_heap_ctx
state_interp σ κs := gen_heap_ctx σ
}.
(** Override the notations so that scopes and coercions work out *)
......@@ -112,6 +112,7 @@ Proof.
iApply wp_lift_pure_det_head_step; [eauto|intros; inv_head_step; eauto|].
iModIntro; iNext; iIntros "!> /= {$He}". by iApply wp_value.
Qed.
Lemma twp_fork s E e Φ :
WP e @ s; [{ _, True }] - Φ (LitV LitUnit) - WP Fork e @ s; E [{ Φ }].
Proof.
......@@ -126,8 +127,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) "Hσ !>"; iSplit; first by eauto.
iNext; iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iIntros (σ1 κs) "Hσ !>"; iSplit; first by eauto.
iNext; iIntros (κ κs' 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.
......@@ -136,8 +137,8 @@ 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) "Hσ !>"; iSplit; first by eauto.
iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iIntros (σ1 κs) "Hσ !>"; iSplit; first by eauto.
iIntros (κ κs' 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,18 +147,18 @@ 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) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto.
iNext; iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma twp_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 twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto.
iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
......@@ -167,8 +168,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) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto 6. iNext; iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto 6. iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
......@@ -178,8 +179,8 @@ Lemma twp_store s E l v' e v :
Proof.
iIntros (<- Φ) "Hl HΦ".
iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto 6. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto 6. iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
......@@ -191,8 +192,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) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (κ v2' σ2 efs Hstep); inv_head_step.
iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (κ κs' 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 :
......@@ -202,8 +203,8 @@ Lemma twp_cas_fail s E l q v' e1 v1 e2 :
Proof.
iIntros (<- [v2 <-] ?? Φ) "Hl HΦ".
iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
......@@ -214,8 +215,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) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (κ v2' σ2 efs Hstep); inv_head_step.
iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
......@@ -226,8 +227,8 @@ Lemma twp_cas_suc s E l e1 v1 e2 v2 :
Proof.
iIntros (<- <- ? Φ) "Hl HΦ".
iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
......@@ -239,8 +240,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) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (κ v2' σ2 efs Hstep); inv_head_step.
iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
......@@ -251,8 +252,8 @@ Lemma twp_faa s E l i1 e2 i2 :
Proof.
iIntros (<- Φ) "Hl HΦ".
iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
......
......@@ -40,6 +40,7 @@ Proof.
rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
rewrite HΔ' -lifting.wp_pure_step_later //.
Qed.
Lemma tac_twp_pure `{heapG Σ} Δ s E e1 e2 φ Φ :
PureExec φ e1 e2
φ
......
......@@ -4,12 +4,15 @@ From iris.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
(* TODO (MR) re-introduce lemma after we prove twp_total *)
(*
Definition heap_total Σ `{heapPreG Σ} s e σ φ :
(∀ `{heapG Σ}, WP e @ s; ⊤ [{ v, ⌜φ v⌝ }]%I) →
sn erased_step ([e], σ).
Proof.
intros Hwp; eapply (twp_total _ _); iIntros (?) "".
intros Hwp; eapply (twp_total _ _) with (κs := []); iIntros (?) "".
iMod (gen_heap_init σ) as (?) "Hh".
iModIntro. iExists gen_heap_ctx; iFrame.
iModIntro. iExists (fun σ _ => gen_heap_ctx σ); iFrame.
iApply (Hwp (HeapG _ _ _)).
Qed.
*)
......@@ -66,50 +66,50 @@ Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ iProp Σ.
Implicit Types Φs : list (val Λ iProp Σ).
Notation world' E σ := (wsat ownE E state_interp σ)%I (only parsing).
Notation world σ := (world' σ) (only parsing).
Notation world' E σ κs := (wsat ownE E state_interp σ κs)%I (only parsing).
Notation world σ κs := (world' σ κs) (only parsing).
Notation wptp s t := ([ list] ef t, WP ef @ s; {{ _, True }})%I.
Lemma wp_step s E e1 σ1 κ e2 σ2 efs Φ :
Lemma wp_step s E e1 σ1 κ κs e2 σ2 efs Φ :
prim_step e1 σ1 κ e2 σ2 efs
world' E σ1 WP e1 @ s; E {{ Φ }}
== |==> (world' E σ2 WP e2 @ s; E {{ Φ }} wptp s efs).
world' E σ1 (cons_obs κ κs) WP e1 @ s; E {{ Φ }}
== |==> (world' E σ2 κs WP e2 @ s; E {{ Φ }} wptp s 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" $! κ 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" $! κ κs e2 σ2 efs with "[//] [$Hw $HE]") as ">(Hw & HE & H)".
iIntros "!> !>". by iMod ("H" with "[$Hw $HE]") as ">($ & $ & $)".
Qed.
(* should we be able to say that κs = κ :: κs'? *)
Lemma wptp_step s e1 t1 t2 κ σ1 σ2 Φ :
Lemma wptp_step s e1 t1 t2 κ κs σ1 σ2 Φ :
step (e1 :: t1,σ1) κ (t2, σ2)
world σ1 WP e1 @ s; {{ Φ }} wptp s t1
world σ1 (cons_obs κ κs) WP e1 @ s; {{ Φ }} wptp s t1
== e2 t2',
t2 = e2 :: t2' |==> (world σ2 WP e2 @ s; {{ Φ }} wptp s t2').
t2 = e2 :: t2' |==> (world σ2 κs WP e2 @ s; {{ Φ }} wptp s t2').
Proof.
iIntros (Hstep) "(HW & He & Ht)".
destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=.
- iExists e2', (t2' ++ efs); iSplitR; first by eauto.
- iExists e2', (t2' ++ efs). iSplitR; first by eauto.
iFrame "Ht". iApply wp_step; eauto with iFrame.
- iExists e, (t1' ++ e2' :: t2' ++ efs); iSplitR; first eauto.
iDestruct "Ht" as "($ & He' & $)". iFrame "He".
iApply wp_step; eauto with iFrame.
Qed.
Lemma wptp_steps s n e1 t1 κs t2 σ1 σ2 Φ :
Lemma wptp_steps s n e1 t1 κs κs' t2 σ1 σ2 Φ :
nsteps n (e1 :: t1, σ1) κs (t2, σ2)
world σ1 WP e1 @ s; {{ Φ }} wptp s t1
world σ1 (κs ++ κs') WP e1 @ s; {{ Φ }} wptp s t1
Nat.iter (S n) (λ P, |==> P) ( e2 t2',
t2 = e2 :: t2' world σ2 WP e2 @ s; {{ Φ }} wptp s t2').
t2 = e2 :: t2' world σ2 κs' WP e2 @ s; {{ Φ }} wptp s t2').
Proof.
revert e1 t1 κs t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 κs t2 σ1 σ2 /=.
revert e1 t1 κs κs' t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 κs κs' t2 σ1 σ2 /=.
{ inversion_clear 1; iIntros "?"; eauto 10. }
iIntros (Hsteps) "H". inversion_clear Hsteps as [|?? [t1' σ1']].
iMod (wptp_step with "H") as (e1' t1'') "[% H]"; first eauto; simplify_eq.
iModIntro; iNext; iMod "H" as ">?". by iApply IH.
rewrite /cons_obs. rewrite <- app_assoc.
iMod (wptp_step with "H") as (e1' t1'') "[% H]"; first by eauto; simplify_eq.
subst. iModIntro; iNext; iMod "H" as ">H". by iApply IH.
Qed.
Lemma bupd_iter_laterN_mono n P Q `{!Plain Q} :
......@@ -125,9 +125,11 @@ Proof.
by rewrite bupd_frame_l {1}(later_intro R) -later_sep IH.
Qed.
Lemma wptp_result s n e1 t1 κs v2 t2 σ1 σ2 φ :
Lemma wptp_result s n e1 t1 κs κs' v2 t2 σ1 σ2 φ :
nsteps n (e1 :: t1, σ1) κs (of_val v2 :: t2, σ2)
world σ1 WP e1 @ s; {{ v, σ, state_interp σ ={,}= ⌜φ v σ⌝ }} wptp s t1
world σ1 (κs ++ κs')
WP e1 @ s; {{ v, σ, state_interp σ κs' ={,}= ⌜φ v σ⌝ }}
wptp s t1
^(S (S n)) ⌜φ v2 σ2.
Proof.
intros. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono.
......@@ -137,8 +139,8 @@ Proof.
iMod ("H" with "Hσ [$]") as ">(_ & _ & $)".
Qed.
Lemma wp_safe E e σ Φ :
world' E σ - WP e @ E {{ Φ }} == is_Some (to_val e) reducible e σ⌝.
Lemma wp_safe E e σ κs Φ :
world' E σ κs - WP e @ E {{ Φ }} == is_Some (to_val e) reducible e σ⌝.
Proof.
rewrite wp_unfold /wp_pre. iIntros "(Hw&HE&Hσ) H".
destruct (to_val e) as [v|] eqn:?.
......@@ -147,9 +149,9 @@ Proof.
iIntros "!> !> !%". by right.
Qed.
Lemma wptp_safe n e1 κs e2 t1 t2 σ1 σ2 Φ :
Lemma wptp_safe n e1 κs κs' e2 t1 t2 σ1 σ2 Φ :
nsteps n (e1 :: t1, σ1) κs (t2, σ2) e2 t2
world σ1 WP e1 {{ Φ }} wptp NotStuck t1
world σ1 (κs ++ κs') WP e1 {{ Φ }} wptp NotStuck t1
^(S (S n)) is_Some (to_val e2) reducible e2 σ2.
Proof.
intros ? He2. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono.
......@@ -159,9 +161,9 @@ Proof.
- iMod (wp_safe with "Hw [Htp]") as "$". by iApply (big_sepL_elem_of with "Htp").
Qed.
Lemma wptp_invariance s n e1 κs e2 t1 t2 σ1 σ2 φ Φ :
Lemma wptp_invariance s n e1 κs κs' e2 t1 t2 σ1 σ2 φ Φ :
nsteps n (e1 :: t1, σ1) κs (t2, σ2)
(state_interp σ2 ={,}= ⌜φ⌝) world σ1 WP e1 @ s; {{ Φ }} wptp s t1
(state_interp σ2 κs' ={,}= ⌜φ⌝) world σ1 (κs ++ κs') WP e1 @ s; {{ Φ }} wptp s t1
^(S (S n)) ⌜φ⌝.
Proof.
intros ?. rewrite wptp_steps // bupd_iter_frame_l laterN_later.
......@@ -173,68 +175,70 @@ Qed.
End adequacy.
Theorem wp_strong_adequacy Σ Λ `{invPreG Σ} s e σ φ :
( `{Hinv : invG Σ},
(|={}=> stateI : state Λ iProp Σ,
let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
stateI σ WP e @ s; {{ v, σ, stateI σ ={,}= ⌜φ v σ⌝ }})%I)
( `{Hinv : invG Σ} κs,
(|={}=> stateI : state Λ list (observation Λ) iProp Σ,
let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI in
stateI σ κs WP e @ s; {{ v, σ, stateI σ [] ={,}= ⌜φ v σ⌝ }})%I)
adequate s e σ φ.
Proof.
intros Hwp; split.
- intros t2 σ2 v2 [n [κs ?]]%erased_steps_nsteps.
eapply (soundness (M:=iResUR Σ) _ (S (S n))).
iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _).
iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _ κs).
rewrite {1}uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
iDestruct "Hwp" as (Istate) "[HI Hwp]".
iApply (@wptp_result _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
iApply (@wptp_result _ _ (IrisG _ _ _ Hinv Istate) _ _ _ _ _ []); last first.
rewrite app_nil_r. all: eauto with iFrame.
- destruct s; last done. intros t2 σ2 e2 _ [n [κs ?]]%erased_steps_nsteps ?.
eapply (soundness (M:=iResUR Σ) _ (S (S n))).
iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _).
iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _ κs).
rewrite uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
iDestruct "Hwp" as (Istate) "[HI Hwp]".
iApply (@wptp_safe _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
iApply (@wptp_safe _ _ (IrisG _ _ _ Hinv Istate) _ _ _ []); last first.
rewrite app_nil_r. all: eauto with iFrame.
Qed.
Theorem wp_adequacy Σ Λ `{invPreG Σ} s e σ φ :
( `{Hinv : invG Σ},
(|={}=> stateI : state Λ iProp Σ,
let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
stateI σ WP e @ s; {{ v, ⌜φ v }})%I)
( `{Hinv : invG Σ} κs,
(|={}=> stateI : state Λ list (observation Λ) iProp Σ,
let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI in
stateI σ κs WP e @ s; {{ v, ⌜φ v }})%I)
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp. apply (wp_strong_adequacy Σ _)=> Hinv.
intros Hwp. apply (wp_strong_adequacy Σ _)=> Hinv κs.
iMod Hwp as (stateI) "[Hσ H]". iExists stateI. iIntros "{$Hσ} !>".
iApply (wp_wand with "H"). iIntros (v ? σ') "_".
iMod (fupd_intro_mask' ) as "_"; auto.
Qed.
Theorem wp_invariance Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
( `{Hinv : invG Σ},
(|={}=> stateI : state Λ iProp Σ,
let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
stateI σ1 WP e @ s; {{ _, True }} (stateI σ2 ={,}= ⌜φ⌝))%I)
( `{Hinv : invG Σ} κs κs',
(|={}=> stateI : state Λ list (observation Λ) iProp Σ,
let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI in
stateI σ1 (κs ++ κs') WP e @ s; {{ _, True }} (stateI σ2 κs' ={,}= ⌜φ⌝))%I)
rtc erased_step ([e], σ1) (t2, σ2)
φ.
Proof.
intros Hwp [n [κs ?]]%erased_steps_nsteps.
eapply (soundness (M:=iResUR Σ) _ (S (S n))).
iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _).
iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _ κs []).
rewrite {1}uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
iDestruct "Hwp" as (Istate) "(HIstate & Hwp & Hclose)".
iApply (@wptp_invariance _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
iApply (@wptp_invariance _ _ (IrisG _ _ _ Hinv Istate)); eauto with iFrame.
Qed.
(* An equivalent version that does not require finding [fupd_intro_mask'], but
can be confusing to use. *)
Corollary wp_invariance' Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
( `{Hinv : invG Σ},
(|={}=> stateI : state Λ iProp Σ,
let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
stateI σ1 WP e @ s; {{ _, True }} (stateI σ2 - E, |={,E}=> ⌜φ⌝))%I)
( `{Hinv : invG Σ} κs κs',
(|={}=> stateI : state Λ list (observation Λ) iProp Σ,
let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI in
stateI σ1 κs WP e @ s; {{ _, True }} (stateI σ2 κs' - E, |={,E}=> ⌜φ⌝))%I)
rtc erased_step ([e], σ1) (t2, σ2)
φ.
Proof.
intros Hwp. eapply wp_invariance; first done.
intros Hinv. iMod (Hwp Hinv) as (stateI) "(? & ? & Hφ)".
intros Hinv κs κs'. iMod (Hwp Hinv) as (stateI) "(? & ? & Hφ)".
iModIntro. iExists stateI. iFrame. iIntros "Hσ".
iDestruct ("Hφ" with "Hσ") as (E) ">Hφ".
iMod (fupd_intro_mask') as "_"; last by iModIntro. solve_ndisj.
......
......@@ -16,7 +16,7 @@ Section ectx_language_mixin.
Context (empty_ectx : ectx).
Context (comp_ectx : ectx ectx ectx).
Context (fill : ectx expr expr).
Context (head_step : expr state option observation -> expr state list expr Prop).
Context (head_step : expr state option observation expr state list expr Prop).
Record EctxLanguageMixin := {
mixin_to_of_val v : to_val (of_val v) = Some v;
......@@ -55,7 +55,7 @@ Structure ectxLanguage := EctxLanguage {
empty_ectx : ectx;
comp_ectx : ectx ectx ectx;
fill : ectx expr expr;
head_step : expr state option observation -> expr state list expr Prop;
head_step : expr state option observation expr state list expr Prop;
ectx_language_mixin :
EctxLanguageMixin of_val to_val empty_ectx comp_ectx fill head_step
......@@ -210,7 +210,7 @@ Section ectx_language.
Lemma det_head_step_pure_exec (P : Prop) e1 e2 :
( σ, P head_reducible e1 σ)
( σ1 κ e2' σ2 efs,
P head_step e1 σ1 κ e2' σ2 efs κ = None /\ σ1 = σ2 e2=e2' efs = [])
P head_step e1 σ1 κ e2' σ2 efs κ = None σ1 = σ2 e2=e2' efs = [])
PureExec P e1 e2.
Proof.
intros Hp1 Hp2. split.
......
......@@ -16,43 +16,43 @@ Hint Resolve head_stuck_stuck.
Lemma wp_lift_head_step_fupd {s E Φ} e1 :
to_val e1 = None
( σ1, state_interp σ1 ={E,}=
( σ1 κs, state_interp σ1 κs ={E,}=
head_reducible e1 σ1
κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={,,E}=
state_interp σ2 WP e2 @ s; E {{ Φ }} [ list] ef efs, WP ef @ s; {{ _, True }})
κ κ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 }})
WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_step_fupd=>//. iIntros (σ1) "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 (κ e2 σ2 efs) "%".
iSplit; first by destruct s; eauto. iIntros (κ κs' e2 σ2 efs [Hstep ->]).
iApply "H"; eauto.
Qed.
Lemma wp_lift_head_step {s E Φ} e1 :
to_val e1 = None
( σ1, state_interp σ1 ={E,}=
( σ1 κs, state_interp σ1 κs ={E,}=
head_reducible e1 σ1
κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={,E}=
state_interp σ2 WP e2 @ s; E {{ Φ }} [ list] ef efs, WP ef @ s; {{ _, True }})
κ κ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 }})
WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_head_step_fupd; [done|]. iIntros (?) "?".
iMod ("H" with "[$]") as "[$ H]". iIntros "!>" (κ e2 σ2 efs ?) "!> !>". by iApply "H".
iIntros (?) "H". iApply wp_lift_head_step_fupd; [done|]. iIntros (??) "?".
iMod ("H" with "[$]") as "[$ H]". iIntros "!>" (κ κs' e2 σ2 efs ?) "!> !>". by iApply "H".
Qed.
Lemma wp_lift_head_stuck E Φ e :
to_val e = None
sub_redexes_are_values e
( σ, state_interp σ ={E,}= head_stuck e σ⌝)
( σ κs, state_interp σ κs ={E,}= head_stuck e σ⌝)
WP e @ E ?{{ Φ }}.
Proof.
iIntros (??) "H". iApply wp_lift_stuck; first done.
iIntros (σ) "Hσ". iMod ("H" with "Hσ") as "%". by auto.
iIntros (σ κs) "Hσ". iMod ("H" with "Hσ") as "%". by auto.
Qed.
Lemma wp_lift_pure_head_step {s E E' Φ} e1 :
( σ1, head_reducible e1 σ1)
( σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs κ = None /\ σ1 = σ2)
( σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs κ = None σ1 = σ2)
(|={E,E'}=> κ e2 efs σ<