Commit e16140cf authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ralf/prophecy' into 'master'

Prophecy variables

See merge request FP/iris-coq!173
parents 7041c043 4d57af6b
......@@ -19,6 +19,11 @@ Changes in and extensions of the theory:
experimental.
* [#] The adequacy statement for weakest preconditions now also involves the
final state.
* [#] Add the notion of an "observation" to the language interface, so that
every reduction step can optionally be marked with an event, and an execution
trace has a matching list of events. Change WP so that it is told the entire
future trace of observations from the beginning. Use this in heap_lang to
implement prophecy variables.
* [#] The Löb rule is now a derived rule; it follows from later-intro, later
being contractive and the fact that we can take fixpoints of contractive
functions.
......
......@@ -87,12 +87,14 @@ theories/heap_lang/notation.v
theories/heap_lang/proofmode.v
theories/heap_lang/adequacy.v
theories/heap_lang/total_adequacy.v
theories/heap_lang/proph_map.v
theories/heap_lang/lib/spawn.v
theories/heap_lang/lib/par.v
theories/heap_lang/lib/assert.v
theories/heap_lang/lib/lock.v
theories/heap_lang/lib/spin_lock.v
theories/heap_lang/lib/ticket_lock.v
theories/heap_lang/lib/coin_flip.v
theories/heap_lang/lib/counter.v
theories/heap_lang/lib/atomic_heap.v
theories/heap_lang/lib/increment.v
......
From iris.program_logic Require Export weakestpre adequacy.
From iris.algebra Require Import auth.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang Require Import proofmode notation proph_map.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Class heapPreG Σ := HeapPreG {
heap_preG_iris :> invPreG Σ;
heap_preG_heap :> gen_heapPreG loc val Σ
heap_preG_heap :> gen_heapPreG loc val Σ;
heap_preG_proph :> proph_mapPreG proph_id val Σ
}.
Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val].
Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val; proph_mapΣ proph_id val].
Instance subG_heapPreG {Σ} : subG heapΣ Σ heapPreG Σ.
Proof. solve_inG. Qed.
......@@ -17,8 +18,10 @@ 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 (?) "".
iMod (gen_heap_init σ) as (?) "Hh".
iModIntro. iExists gen_heap_ctx. iFrame "Hh".
iApply (Hwp (HeapG _ _ _)).
intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
iMod (gen_heap_init σ.(heap)) as (?) "Hh".
iMod (proph_map_init κs σ.(used_proph_id)) as (?) "Hp".
iModIntro.
iExists (λ σ κs, (gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph_id))%I). iFrame.
iApply (Hwp (HeapG _ _ _ _)).
Qed.
This diff is collapsed.
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation par.
Set Default Proof Using "Type".
(** Nondeterminism and Speculation:
Implementing "Late choice versus early choice" example from
Logical Relations for Fine-Grained Concurrency by Turon et al. (POPL'13) *)
Definition rand: val :=
λ: "_",
let: "y" := ref #false in
Fork ("y" <- #true) ;;
!"y".
Definition earlyChoice: val :=
λ: "x",
let: "r" := rand #() in
"x" <- #0 ;;
"r".
Definition lateChoice: val :=
λ: "x",
let: "p" := NewProph in
"x" <- #0 ;;
let: "r" := rand #() in
resolve_proph: "p" to: "r" ;;
"r".
Section coinflip.
Context `{!heapG Σ}.
Local Definition N := nroot .@ "coin".
Lemma rand_spec :
{{{ True }}} rand #() {{{ (b : bool), RET #b; True }}}.
Proof.
iIntros (Φ) "_ HP".
wp_lam. wp_alloc l as "Hl". wp_lam.
iMod (inv_alloc N _ ( (b: bool), l #b)%I with "[Hl]") as "#Hinv"; first by eauto.
wp_apply wp_fork.
- iInv N as (b) ">Hl". wp_store. iModIntro. iSplitL; eauto.
- wp_lam. iInv N as (b) ">Hl". wp_load. iModIntro. iSplitL "Hl"; first by eauto.
iApply "HP". done.
Qed.
Lemma earlyChoice_spec (x: loc) :
<<< x - >>>
earlyChoice #x
@
<<< (b: bool), x #0, RET #b >>>.
Proof.
iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
wp_apply rand_spec; first done.
iIntros (b) "_". wp_let.
wp_bind (_ <- _)%E.
iMod "AU" as "[Hl [_ Hclose]]".
iDestruct "Hl" as (v) "Hl".
wp_store.
iMod ("Hclose" with "[Hl]") as "HΦ"; first by eauto.
iModIntro. wp_seq. done.
Qed.
Definition val_to_bool (v : option val) : bool :=
match v with
| Some (LitV (LitBool b)) => b
| _ => true
end.
Lemma lateChoice_spec (x: loc) :
<<< x - >>>
lateChoice #x
@
<<< (b: bool), x #0, RET #b >>>.
Proof.
iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
wp_apply wp_new_proph; first done.
iIntros (v p) "Hp".
wp_let.
wp_bind (_ <- _)%E.
iMod "AU" as "[Hl [_ Hclose]]".
iDestruct "Hl" as (v') "Hl".
wp_store.
iMod ("Hclose" $! (val_to_bool v) with "[Hl]") as "HΦ"; first by eauto.
iModIntro. wp_seq. wp_apply rand_spec; try done.
iIntros (b') "_". wp_let.
wp_apply (wp_resolve_proph with "Hp").
iIntros (->). wp_seq. done.
Qed.
End coinflip.
This diff is collapsed.
......@@ -8,6 +8,7 @@ Delimit Scope val_scope with V.
Coercion LitInt : Z >-> base_lit.
Coercion LitBool : bool >-> base_lit.
Coercion LitLoc : loc >-> base_lit.
Coercion LitProphecy : proph_id >-> base_lit.
Coercion App : expr >-> Funclass.
Coercion of_val : val >-> expr.
......@@ -155,3 +156,5 @@ Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
(Match e0 BAnon e1 x%bind e2)
(e0, e1, x, e2 at level 200, only parsing) : expr_scope.
Notation "'resolve_proph:' p 'to:' v" := (ResolveProph p v) (at level 100) : expr_scope.
From iris.algebra Require Import auth gmap.
From iris.base_logic.lib Require Export own.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
Definition proph_map (P V : Type) `{Countable P} := gmap P (option V).
Definition proph_val_list (P V : Type) := list (P * V).
Definition proph_mapUR (P V : Type) `{Countable P} : ucmraT :=
gmapUR P $ exclR $ optionC $ leibnizC V.
Definition to_proph_map {P V} `{Countable P} (pvs : proph_map P V) : proph_mapUR P V :=
fmap (λ v, Excl (v : option (leibnizC V))) pvs.
(** The CMRA we need. *)
Class proph_mapG (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapG {
proph_map_inG :> inG Σ (authR (proph_mapUR P V));
proph_map_name : gname
}.
Arguments proph_map_name {_ _ _ _ _} _ : assert.
Class proph_mapPreG (P V : Type) (Σ : gFunctors) `{Countable P} :=
{ proph_map_preG_inG :> inG Σ (authR (proph_mapUR P V)) }.
Definition proph_mapΣ (P V : Type) `{Countable P} : gFunctors :=
#[GFunctor (authR (proph_mapUR P V))].
Instance subG_proph_mapPreG {Σ P V} `{Countable P} :
subG (proph_mapΣ P V) Σ proph_mapPreG P V Σ.
Proof. solve_inG. Qed.
Section definitions.
Context `{pG : proph_mapG P V Σ}.
(** The first resolve for [p] in [pvs] *)
Definition first_resolve (pvs : proph_val_list P V) (p : P) :=
(map_of_list pvs : gmap P V) !! p.
Definition first_resolve_in_list (R : proph_map P V) pvs :=
p v, p dom (gset _) R
first_resolve pvs p = Some v
R !! p = Some (Some v).
Definition proph_map_auth (R : proph_map P V) : iProp Σ :=
own (proph_map_name pG) ( (to_proph_map R)).
Definition proph_map_ctx (pvs : proph_val_list P V) (ps : gset P) : iProp Σ :=
( R, first_resolve_in_list R pvs
dom (gset _) R ps
proph_map_auth R)%I.
Definition proph_def (p : P) (v: option V) : iProp Σ :=
own (proph_map_name pG) ( {[ p := Excl (v : option $ leibnizC V) ]}).
Definition proph_aux : seal (@proph_def). by eexists. Qed.
Definition proph := proph_aux.(unseal).
Definition proph_eq :
@proph = @proph_def := proph_aux.(seal_eq).
End definitions.
Section first_resolve.
Context {P V : Type} `{Countable P}.
Implicit Type pvs : proph_val_list P V.
Implicit Type p : P.
Implicit Type v : V.
Implicit Type R : proph_map P V.
Lemma first_resolve_insert pvs p R :
first_resolve_in_list R pvs
p dom (gset _) R
first_resolve_in_list (<[p := first_resolve pvs p]> R) pvs.
Proof.
intros Hf Hnotin p' v' Hp'. rewrite (dom_insert_L R p) in Hp'.
erewrite elem_of_union in Hp'. destruct Hp' as [->%elem_of_singleton | Hin] => [->].
- by rewrite lookup_insert.
- rewrite lookup_insert_ne; first auto. by intros ->.
Qed.
Lemma first_resolve_delete pvs p v R :
first_resolve_in_list R ((p, v) :: pvs)
first_resolve_in_list (delete p R) pvs.
Proof.
intros Hfr p' v' Hpin Heq. rewrite dom_delete_L in Hpin. rewrite /first_resolve in Heq.
apply elem_of_difference in Hpin as [Hpin Hne%not_elem_of_singleton].
erewrite <- lookup_insert_ne in Heq; last done. rewrite lookup_delete_ne; eauto.
Qed.
Lemma first_resolve_eq R p v w pvs :
first_resolve_in_list R ((p, v) :: pvs)
R !! p = Some w
w = Some v.
Proof.
intros Hfr Hlookup. specialize (Hfr p v (elem_of_dom_2 _ _ _ Hlookup)).
rewrite /first_resolve lookup_insert in Hfr. rewrite Hfr in Hlookup; last done.
inversion Hlookup. done.
Qed.
End first_resolve.
Section to_proph_map.
Context (P V : Type) `{Countable P}.
Implicit Types p : P.
Implicit Types R : proph_map P V.
Lemma to_proph_map_valid R : to_proph_map R.
Proof. intros l. rewrite lookup_fmap. by case (R !! l). Qed.
Lemma to_proph_map_insert p v R :
to_proph_map (<[p := v]> R) = <[p := Excl (v: option (leibnizC V))]> (to_proph_map R).
Proof. by rewrite /to_proph_map fmap_insert. Qed.
Lemma to_proph_map_delete p R :
to_proph_map (delete p R) = delete p (to_proph_map R).
Proof. by rewrite /to_proph_map fmap_delete. Qed.
Lemma lookup_to_proph_map_None R p :
R !! p = None to_proph_map R !! p = None.
Proof. by rewrite /to_proph_map lookup_fmap=> ->. Qed.
Lemma proph_map_singleton_included R p v :
{[p := Excl v]} to_proph_map R R !! p = Some v.
Proof.
rewrite singleton_included=> -[v' []].
rewrite /to_proph_map lookup_fmap fmap_Some_equiv=> -[v'' [Hp ->]].
intros [=->]%Some_included_exclusive%leibniz_equiv_iff; first done; last done.
apply excl_exclusive.
Qed.
End to_proph_map.
Lemma proph_map_init `{proph_mapPreG P V PVS} pvs ps :
(|==> _ : proph_mapG P V PVS, proph_map_ctx pvs ps)%I.
Proof.
iMod (own_alloc ( to_proph_map )) as (γ) "Hh".
{ apply: auth_auth_valid. exact: to_proph_map_valid. }
iModIntro. iExists (ProphMapG P V PVS _ _ _ γ), . iSplit; last by iFrame.
iPureIntro. split =>//.
Qed.
Section proph_map.
Context `{proph_mapG P V Σ}.
Implicit Types p : P.
Implicit Types v : option V.
Implicit Types R : proph_map P V.
(** General properties of mapsto *)
Global Instance proph_timeless p v : Timeless (proph p v).
Proof. rewrite proph_eq /proph_def. apply _. Qed.
Lemma proph_map_alloc R p v :
p dom (gset _) R
proph_map_auth R == proph_map_auth (<[p := v]> R) proph p v.
Proof.
iIntros (Hp) "HR". rewrite /proph_map_ctx proph_eq /proph_def.
iMod (own_update with "HR") as "[HR Hl]".
{ eapply auth_update_alloc,
(alloc_singleton_local_update _ _ (Excl $ (v : option (leibnizC _))))=> //.
apply lookup_to_proph_map_None. apply (iffLR (not_elem_of_dom _ _) Hp). }
iModIntro. rewrite /proph_map_auth to_proph_map_insert. iFrame.
Qed.
Lemma proph_map_remove R p v :
proph_map_auth R - proph p v == proph_map_auth (delete p R).
Proof.
iIntros "HR Hp". rewrite /proph_map_ctx proph_eq /proph_def.
rewrite /proph_map_auth to_proph_map_delete. iApply (own_update_2 with "HR Hp").
apply auth_update_dealloc, (delete_singleton_local_update _ _ _).
Qed.
Lemma proph_map_valid R p v : proph_map_auth R - proph p v - R !! p = Some v.
Proof.
iIntros "HR Hp". rewrite /proph_map_ctx proph_eq /proph_def.
iDestruct (own_valid_2 with "HR Hp")
as %[HH%proph_map_singleton_included _]%auth_valid_discrete_2; auto.
Qed.
End proph_map.
......@@ -35,7 +35,9 @@ Inductive expr :=
| Load (e : expr)
| Store (e1 : expr) (e2 : expr)
| CAS (e0 : expr) (e1 : expr) (e2 : expr)
| FAA (e1 : expr) (e2 : expr).
| FAA (e1 : expr) (e2 : expr)
| NewProph
| ResolveProph (e1 : expr) (e2 : expr).
Fixpoint to_expr (e : expr) : heap_lang.expr :=
match e with
......@@ -60,6 +62,8 @@ Fixpoint to_expr (e : expr) : heap_lang.expr :=
| Store e1 e2 => heap_lang.Store (to_expr e1) (to_expr e2)
| CAS e0 e1 e2 => heap_lang.CAS (to_expr e0) (to_expr e1) (to_expr e2)
| FAA e1 e2 => heap_lang.FAA (to_expr e1) (to_expr e2)
| NewProph => heap_lang.NewProph
| ResolveProph e1 e2 => heap_lang.ResolveProph (to_expr e1) (to_expr e2)
end.
Ltac of_expr e :=
......@@ -94,6 +98,10 @@ Ltac of_expr e :=
constr:(CAS e0 e1 e2)
| heap_lang.FAA ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(FAA e1 e2)
| heap_lang.NewProph =>
constr:(NewProph)
| heap_lang.ResolveProph ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(ResolveProph e1 e2)
| to_expr ?e => e
| of_val ?v => constr:(Val v (of_val v) (to_of_val v))
| language.of_val ?v => constr:(Val v (of_val v) (to_of_val v))
......@@ -108,10 +116,10 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
| Val _ _ _ | ClosedExpr _ => true
| Var x => bool_decide (x X)
| Rec f x e => is_closed (f :b: x :b: X) e
| Lit _ => true
| Lit _ | NewProph => true
| UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
is_closed X e
| App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 =>
| App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 | ResolveProph e1 e2 =>
is_closed X e1 && is_closed X e2
| If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
is_closed X e0 && is_closed X e1 && is_closed X e2
......@@ -171,6 +179,8 @@ Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
| Store e1 e2 => Store (subst x es e1) (subst x es e2)
| CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
| FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
| NewProph => NewProph
| ResolveProph e1 e2 => ResolveProph (subst x es e1) (subst x es e2)
end.
Lemma to_expr_subst x er e :
to_expr (subst x er e) = heap_lang.subst x (to_expr er) (to_expr e).
......@@ -190,6 +200,8 @@ Definition is_atomic (e : expr) :=
| Fork _ => true
(* Make "skip" atomic *)
| App (Rec _ _ (Lit _)) (Lit _) => true
| NewProph => true
| ResolveProph e1 e2 => bool_decide (is_Some (to_val e1) is_Some (to_val e2))
| _ => false
end.
Lemma is_atomic_correct s e : is_atomic e Atomic s (to_expr e).
......@@ -293,4 +305,6 @@ Ltac reshape_expr e tac :=
| CAS ?e0 ?e1 ?e2 => go (CasRCtx e0 e1 :: K) e2
| FAA ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (FaaLCtx v2 :: K) e1)
| FAA ?e1 ?e2 => go (FaaRCtx e1 :: K) e2
| ResolveProph ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (ProphLCtx v2 :: K) e1)
| ResolveProph ?e1 ?e2 => go (ProphRCtx e1 :: K) e2
end in go (@nil ectx_item) e.
......@@ -6,10 +6,12 @@ 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".
iModIntro. iExists gen_heap_ctx; iFrame.
iApply (Hwp (HeapG _ _ _)).
iMod (gen_heap_init σ.(heap)) as (?) "Hh".
iMod (proph_map_init [] σ.(used_proph_id)) as (?) "Hp".
iModIntro.
iExists (λ σ κs, (gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph_id))%I). iFrame.
iApply (Hwp (HeapG _ _ _ _)).
Qed.
This diff is collapsed.
This diff is collapsed.
......@@ -16,51 +16,51 @@ 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 }})
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) "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 (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 }})
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 (?) "?".
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 :
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 σ1 = σ2)
(|={E,E'}=> e2 efs σ, head_step e1 σ e2 σ efs
( σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs κ = [] σ1 = σ2)
(|={E,E'}=> κ e2 efs σ, head_step e1 σ κ e2 σ efs
WP e2 @ s; E {{ Φ }} [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E {{ Φ }}.
Proof using Hinh.
iIntros (??) "H". iApply wp_lift_pure_step; [|by eauto|].
{ by destruct s; auto. }
iApply (step_fupd_wand with "H"); iIntros "H".
iIntros (????). iApply "H"; eauto.
iIntros (?????). iApply "H"; eauto.
Qed.
Lemma wp_lift_pure_head_stuck E Φ e :
......@@ -70,72 +70,73 @@ Lemma wp_lift_pure_head_stuck E Φ e :
WP e @ E ?{{ Φ }}%I.
Proof using Hinh.
iIntros (?? Hstuck). iApply wp_lift_head_stuck; [done|done|].
iIntros (σ) "_". iMod (fupd_intro_mask' E ) as "_"; first set_solver.
iIntros (σ κs) "_". iMod (fupd_intro_mask' E ) as "_"; first set_solver.
by auto.
Qed.
Lemma wp_lift_atomic_head_step_fupd {s E1 E2 Φ} e1 :
to_val e1 = None
( σ1, state_interp σ1 ={E1}=
( σ1 κ κs, state_interp σ1 (κ ++ κs) ={E1}=
head_reducible e1 σ1
e2 σ2 efs, head_step e1 σ1 e2 σ2 efs ={E1,E2}=
state_interp σ2
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) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
iSplit; first by destruct s; auto. iIntros (e2 σ2 efs) "%".
iApply "H"; auto.
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, 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
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) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
iSplit; first by destruct s; auto. iNext. iIntros (e2 σ2 efs) "%".
iApply "H"; auto.
iIntros (σ1 κ κs) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.