Commit 936eeb48 authored by Marianna Rapoport's avatar Marianna Rapoport Committed by Ralf Jung
Browse files

Adding initial support for observations to the definition of wp for later prophecy support

parent 53f179de
......@@ -108,6 +108,8 @@ Inductive val :=
Bind Scope val_scope with val.
Inductive observation := prophecy_observation_todo.
Fixpoint of_val (v : val) : expr :=
match v with
| RecV f x e => Rec f x e
......@@ -199,7 +201,7 @@ Proof.
end) (λ l, match l with
| (inl (inl n), None) => LitInt n | (inl (inr b), None) => LitBool b
| (inr (inl ()), None) => LitUnit | (inr (inr l), None) => LitLoc l
| (_, Some p) => LitProphecy p
| (_, Some p) => LitProphecy p
end) _); by intros [].
Qed.
Instance un_op_finite : Countable un_op.
......@@ -415,62 +417,61 @@ Definition vals_cas_compare_safe (vl v1 : val) : Prop :=
val_is_unboxed vl val_is_unboxed v1.
Arguments vals_cas_compare_safe !_ !_ /.
Inductive head_step : expr state expr state list (expr) Prop :=
Inductive head_step : expr state option observation -> expr state list (expr) Prop :=
| BetaS f x e1 e2 v2 e' σ :
to_val e2 = Some v2
Closed (f :b: x :b: []) e1
e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1)
head_step (App (Rec f x e1) e2) σ e' σ []
head_step (App (Rec f x e1) e2) σ None e' σ []
| UnOpS op e v v' σ :
to_val e = Some v
un_op_eval op v = Some v'
head_step (UnOp op e) σ (of_val v') σ []
head_step (UnOp op e) σ None (of_val v') σ []
| BinOpS op e1 e2 v1 v2 v' σ :
to_val e1 = Some v1 to_val e2 = Some v2
bin_op_eval op v1 v2 = Some v'
head_step (BinOp op e1 e2) σ (of_val v') σ []
head_step (BinOp op e1 e2) σ None (of_val v') σ []
| IfTrueS e1 e2 σ :
head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ []
head_step (If (Lit $ LitBool true) e1 e2) σ None e1 σ []
| IfFalseS e1 e2 σ :
head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ []
head_step (If (Lit $ LitBool false) e1 e2) σ None e2 σ []
| FstS e1 v1 e2 v2 σ :
to_val e1 = Some v1 to_val e2 = Some v2
head_step (Fst (Pair e1 e2)) σ e1 σ []
head_step (Fst (Pair e1 e2)) σ None e1 σ []
| SndS e1 v1 e2 v2 σ :
to_val e1 = Some v1 to_val e2 = Some v2
head_step (Snd (Pair e1 e2)) σ e2 σ []
head_step (Snd (Pair e1 e2)) σ None e2 σ []
| CaseLS e0 v0 e1 e2 σ :
to_val e0 = Some v0
head_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ []
head_step (Case (InjL e0) e1 e2) σ None (App e1 e0) σ []
| CaseRS e0 v0 e1 e2 σ :
to_val e0 = Some v0
head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ []
head_step (Case (InjR e0) e1 e2) σ None (App e2 e0) σ []
| ForkS e σ:
head_step (Fork e) σ (Lit LitUnit) σ [e]
head_step (Fork e) σ None (Lit LitUnit) σ [e]
| AllocS e v σ l :
to_val e = Some v σ !! l = None
head_step (Alloc e) σ (Lit $ LitLoc l) (<[l:=v]>σ) []
head_step (Alloc e) σ None (Lit $ LitLoc l) (<[l:=v]>σ) []
| LoadS l v σ :
σ !! l = Some v
head_step (Load (Lit $ LitLoc l)) σ (of_val v) σ []
head_step (Load (Lit $ LitLoc l)) σ None (of_val v) σ []
| StoreS l e v σ :
to_val e = Some v is_Some (σ !! l)
head_step (Store (Lit $ LitLoc l) e) σ (Lit LitUnit) (<[l:=v]>σ) []
head_step (Store (Lit $ LitLoc l) e) σ None (Lit LitUnit) (<[l:=v]>σ) []
| CasFailS l e1 v1 e2 v2 vl σ :
to_val e1 = Some v1 to_val e2 = Some v2
σ !! l = Some vl vl v1
vals_cas_compare_safe vl v1
head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool false) σ []
head_step (CAS (Lit $ LitLoc l) e1 e2) σ None (Lit $ LitBool false) σ []
| CasSucS l e1 v1 e2 v2 σ :
to_val e1 = Some v1 to_val e2 = Some v2
σ !! l = Some v1
vals_cas_compare_safe v1 v1
head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) []
head_step (CAS (Lit $ LitLoc l) e1 e2) σ None (Lit $ LitBool true) (<[l:=v2]>σ) []
| FaaS l i1 e2 i2 σ :
to_val e2 = Some (LitV (LitInt i2))
σ !! l = Some (LitV (LitInt i1))
head_step (FAA (Lit $ LitLoc l) e2) σ (Lit $ LitInt i1) (<[l:=LitV (LitInt (i1 + i2))]>σ) [].
head_step (FAA (Lit $ LitLoc l) e2) σ None (Lit $ LitInt i1) (<[l:=LitV (LitInt (i1 + i2))]>σ) [].
(** Basic properties about the language *)
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
......@@ -480,11 +481,11 @@ Lemma fill_item_val Ki e :
is_Some (to_val (fill_item Ki e)) is_Some (to_val e).
Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
Lemma val_head_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs to_val e1 = None.
Lemma val_head_stuck e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.
Lemma head_ctx_step_val Ki e σ1 e2 σ2 efs :
head_step (fill_item Ki e) σ1 e2 σ2 efs is_Some (to_val e).
Lemma head_ctx_step_val Ki e σ1 κ e2 σ2 efs :
head_step (fill_item Ki e) σ1 κ e2 σ2 efs is_Some (to_val e).
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
......@@ -499,7 +500,7 @@ Qed.
Lemma alloc_fresh e v σ :
let l := fresh (dom (gset loc) σ) in
to_val e = Some v head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) [].
to_val e = Some v head_step (Alloc e) σ None (Lit (LitLoc l)) (<[l:=v]>σ) [].
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
(* Misc *)
......
......@@ -35,7 +35,7 @@ Ltac inv_head_step :=
repeat match goal with
| _ => progress simplify_map_eq/= (* simplify memory stuff *)
| H : to_val _ = Some _ |- _ => apply of_to_val in H
| H : head_step ?e _ _ _ _ |- _ =>
| H : head_step ?e _ _ _ _ _ |- _ =>
try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
and can thus better be avoided. *)
inversion H; subst; clear H
......@@ -48,7 +48,7 @@ Local Hint Constructors head_step.
Local Hint Resolve alloc_fresh.
Local Hint Resolve to_of_val.
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
Local Ltac solve_exec_safe := intros; subst; do 4 eexists; econstructor; eauto.
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
Local Ltac solve_pure_exec :=
unfold IntoVal in *;
......@@ -109,14 +109,14 @@ Lemma wp_fork s E e Φ :
WP e @ s; {{ _, True }} - Φ (LitV LitUnit) - WP Fork e @ s; E {{ Φ }}.
Proof.
iIntros "He HΦ".
iApply wp_lift_pure_det_head_step; [auto|intros; inv_head_step; eauto|].
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.
iIntros "He HΦ".
iApply twp_lift_pure_det_head_step; [auto|intros; inv_head_step; eauto|].
iApply twp_lift_pure_det_head_step; [eauto|intros; inv_head_step; eauto|].
iIntros "!> /= {$He}". by iApply twp_value.
Qed.
......@@ -126,8 +126,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 auto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iIntros (σ1) "Hσ !>"; 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.
......@@ -136,8 +136,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 auto.
iIntros (v2 σ2 efs Hstep); inv_head_step.
iIntros (σ1) "Hσ !>"; 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=> //. iFrame. by iApply "HΦ".
Qed.
......@@ -148,7 +148,7 @@ 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.
iNext; iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma twp_load s E l q v :
......@@ -157,7 +157,7 @@ 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 (κ v2 σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
......@@ -168,7 +168,7 @@ 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.
iSplit; first by eauto 6. iNext; iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
......@@ -179,7 +179,7 @@ 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.
iSplit; first by eauto 6. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
......@@ -192,7 +192,7 @@ 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.
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 :
......@@ -203,7 +203,7 @@ 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.
iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
......@@ -215,7 +215,7 @@ 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.
iSplit; first by eauto. iNext; iIntros (κ v2' σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
......@@ -227,7 +227,7 @@ 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.
iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
......@@ -240,7 +240,7 @@ 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.
iSplit; first by eauto. iNext; iIntros (κ v2' σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
......@@ -252,7 +252,7 @@ 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.
iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
......
......@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
Definition heap_total Σ `{heapPreG Σ} s e σ φ :
( `{heapG Σ}, WP e @ s; [{ v, ⌜φ v }]%I)
sn step ([e], σ).
sn erased_step ([e], σ).
Proof.
intros Hwp; eapply (twp_total _ _); iIntros (?) "".
iMod (gen_heap_init σ) as (?) "Hh".
......
......@@ -37,26 +37,26 @@ Qed.
Record adequate {Λ} (s : stuckness) (e1 : expr Λ) (σ1 : state Λ)
(φ : val Λ state Λ Prop) := {
adequate_result t2 σ2 v2 :
rtc step ([e1], σ1) (of_val v2 :: t2, σ2) φ v2 σ2;
rtc erased_step ([e1], σ1) (of_val v2 :: t2, σ2) φ v2 σ2;
adequate_not_stuck t2 σ2 e2 :
s = NotStuck
rtc step ([e1], σ1) (t2, σ2)
rtc erased_step ([e1], σ1) (t2, σ2)
e2 t2 (is_Some (to_val e2) reducible e2 σ2)
}.
Theorem adequate_tp_safe {Λ} (e1 : expr Λ) t2 σ1 σ2 φ :
adequate NotStuck e1 σ1 φ
rtc step ([e1], σ1) (t2, σ2)
Forall (λ e, is_Some (to_val e)) t2 t3 σ3, step (t2, σ2) (t3, σ3).
rtc erased_step ([e1], σ1) (t2, σ2)
Forall (λ e, is_Some (to_val e)) t2 κ t3 σ3, step (t2, σ2) κ (t3, σ3).
Proof.
intros Had ?.
destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|].
apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2).
destruct (adequate_not_stuck NotStuck e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&efs&?)];
destruct (adequate_not_stuck NotStuck e1 σ1 φ Had t2 σ2 e2) as [?|(κ&e3&σ3&efs&?)];
rewrite ?eq_None_not_Some; auto.
{ exfalso. eauto. }
destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
right; exists (t2' ++ e3 :: t2'' ++ efs), σ3; econstructor; eauto.
right; exists κ, (t2' ++ e3 :: t2'' ++ efs), σ3; econstructor; eauto.
Qed.
Section adequacy.
......@@ -71,39 +71,41 @@ Notation world σ := (world' ⊤ σ) (only parsing).
Notation wptp s t := ([ list] ef t, WP ef @ s; {{ _, True }})%I.
Lemma wp_step s E e1 σ1 e2 σ2 efs Φ :
prim_step e1 σ1 e2 σ2 efs
Lemma wp_step s E e1 σ1 κ 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).
Proof.
rewrite {1}wp_unfold /wp_pre. iIntros (?) "[(Hw & HE & Hσ) H]".
rewrite (val_stuck e1 σ1 e2 σ2 efs) // uPred_fupd_eq.
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" $! κ e2 σ2 efs with "[//] [$Hw $HE]") as ">(Hw & HE & H)".
iIntros "!> !>". by iMod ("H" with "[$Hw $HE]") as ">($ & $ & $)".
Qed.
Lemma wptp_step s e1 t1 t2 σ1 σ2 Φ :
step (e1 :: t1,σ1) (t2, σ2)
(* should we be able to say that κs = κ :: κs'? *)
Lemma wptp_step s e1 t1 t2 κ σ1 σ2 Φ :
step (e1 :: t1,σ1) κ (t2, σ2)
world σ1 WP e1 @ s; {{ Φ }} wptp s t1
== e2 t2', t2 = e2 :: t2' |==> (world σ2 WP e2 @ s; {{ Φ }} wptp s t2').
== e2 t2',
t2 = e2 :: t2' |==> (world σ2 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 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 t2 σ1 σ2 Φ :
nsteps step n (e1 :: t1, σ1) (t2, σ2)
Lemma wptp_steps s n e1 t1 κs t2 σ1 σ2 Φ :
nsteps n (e1 :: t1, σ1) κs (t2, σ2)
world σ1 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').
Proof.
revert e1 t1 t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 t2 σ1 σ2 /=.
revert e1 t1 κs t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 κ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.
......@@ -123,8 +125,8 @@ Proof.
by rewrite bupd_frame_l {1}(later_intro R) -later_sep IH.
Qed.
Lemma wptp_result s n e1 t1 v2 t2 σ1 σ2 φ :
nsteps step n (e1 :: t1, σ1) (of_val v2 :: t2, σ2)
Lemma wptp_result s n e1 t1 κ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
^(S (S n)) ⌜φ v2 σ2.
Proof.
......@@ -145,8 +147,8 @@ Proof.
iIntros "!> !> !%". by right.
Qed.
Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ :
nsteps step n (e1 :: t1, σ1) (t2, σ2) e2 t2
Lemma wptp_safe n e1 κs e2 t1 t2 σ1 σ2 Φ :
nsteps n (e1 :: t1, σ1) κs (t2, σ2) e2 t2
world σ1 WP e1 {{ Φ }} wptp NotStuck t1
^(S (S n)) is_Some (to_val e2) reducible e2 σ2.
Proof.
......@@ -157,8 +159,8 @@ Proof.
- iMod (wp_safe with "Hw [Htp]") as "$". by iApply (big_sepL_elem_of with "Htp").
Qed.
Lemma wptp_invariance s n e1 e2 t1 t2 σ1 σ2 φ Φ :
nsteps step n (e1 :: t1, σ1) (t2, σ2)
Lemma wptp_invariance s n e1 κ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
^(S (S n)) ⌜φ⌝.
Proof.
......@@ -178,13 +180,13 @@ Theorem wp_strong_adequacy Σ Λ `{invPreG Σ} s e σ φ :
adequate s e σ φ.
Proof.
intros Hwp; split.
- intros t2 σ2 v2 [n ?]%rtc_nsteps.
- 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 _).
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.
- destruct s; last done. intros t2 σ2 e2 _ [n ?]%rtc_nsteps ?.
- 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 _).
rewrite uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
......@@ -210,10 +212,10 @@ Theorem wp_invariance Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
(|={}=> stateI : state Λ iProp Σ,
let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
stateI σ1 WP e @ s; {{ _, True }} (stateI σ2 ={,}= ⌜φ⌝))%I)
rtc step ([e], σ1) (t2, σ2)
rtc erased_step ([e], σ1) (t2, σ2)
φ.
Proof.
intros Hwp [n ?]%rtc_nsteps.
intros Hwp [n [κs ?]]%erased_steps_nsteps.
eapply (soundness (M:=iResUR Σ) _ (S (S n))).
iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _).
rewrite {1}uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
......@@ -228,7 +230,7 @@ Corollary wp_invariance' Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
(|={}=> stateI : state Λ iProp Σ,
let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
stateI σ1 WP e @ s; {{ _, True }} (stateI σ2 - E, |={,E}=> ⌜φ⌝))%I)
rtc step ([e], σ1) (t2, σ2)
rtc erased_step ([e], σ1) (t2, σ2)
φ.
Proof.
intros Hwp. eapply wp_invariance; first done.
......
......@@ -10,19 +10,19 @@ structure. Use the coercion [LanguageOfEctx] as defined in the bottom of this
file for doing that. *)
Section ectx_language_mixin.
Context {expr val ectx state : Type}.
Context {expr val ectx state observation : Type}.
Context (of_val : val expr).
Context (to_val : expr option val).
Context (empty_ectx : ectx).
Context (comp_ectx : ectx ectx ectx).
Context (fill : ectx expr expr).
Context (head_step : expr state 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;
mixin_of_to_val e v : to_val e = Some v of_val v = e;
mixin_val_head_stuck e1 σ1 e2 σ2 efs :
head_step e1 σ1 e2 σ2 efs to_val e1 = None;
mixin_val_head_stuck e1 σ1 κ e2 σ2 efs :
head_step e1 σ1 κ e2 σ2 efs to_val e1 = None;
mixin_fill_empty e : fill empty_ectx e = e;
mixin_fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e;
......@@ -35,10 +35,10 @@ Section ectx_language_mixin.
mixin_ectx_positive K1 K2 :
comp_ectx K1 K2 = empty_ectx K1 = empty_ectx K2 = empty_ectx;
mixin_step_by_val K K' e1 e1' σ1 e2 σ2 efs :
mixin_step_by_val K K' e1 e1' σ1 κ e2 σ2 efs :
fill K e1 = fill K' e1'
to_val e1 = None
head_step e1' σ1 e2 σ2 efs
head_step e1' σ1 κ e2 σ2 efs
K'', K' = comp_ectx K K'';
}.
End ectx_language_mixin.
......@@ -48,25 +48,26 @@ Structure ectxLanguage := EctxLanguage {
val : Type;
ectx : Type;
state : Type;
observation : Type;
of_val : val expr;
to_val : expr option val;
empty_ectx : ectx;
comp_ectx : ectx ectx ectx;
fill : ectx expr expr;
head_step : expr state 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
}.
Arguments EctxLanguage {_ _ _ _ _ _ _ _ _ _} _.
Arguments EctxLanguage {_ _ _ _ _ _ _ _ _ _ _} _.
Arguments of_val {_} _%V.
Arguments to_val {_} _%E.
Arguments empty_ectx {_}.
Arguments comp_ectx {_} _ _.
Arguments fill {_} _ _%E.
Arguments head_step {_} _%E _ _%E _ _.
Arguments head_step {_} _%E _ _ _%E _ _.
(* From an ectx_language, we can construct a language. *)
Section ectx_language.
......@@ -76,7 +77,7 @@ Section ectx_language.
Implicit Types K : ectx Λ.
(* Only project stuff out of the mixin that is not also in language *)
Lemma val_head_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs to_val e1 = None.
Lemma val_head_stuck e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs to_val e1 = None.
Proof. apply ectx_language_mixin. Qed.
Lemma fill_empty e : fill empty_ectx e = e.
Proof. apply ectx_language_mixin. Qed.
......@@ -89,17 +90,17 @@ Section ectx_language.
Lemma ectx_positive K1 K2 :
comp_ectx K1 K2 = empty_ectx K1 = empty_ectx K2 = empty_ectx.
Proof. apply ectx_language_mixin. Qed.
Lemma step_by_val K K' e1 e1' σ1 e2 σ2 efs :
Lemma step_by_val K K' e1 e1' σ1 κ e2 σ2 efs :
fill K e1 = fill K' e1'
to_val e1 = None
head_step e1' σ1 e2 σ2 efs
head_step e1' σ1 κ e2 σ2 efs
K'', K' = comp_ectx K K''.
Proof. apply ectx_language_mixin. Qed.