Commit 18d899e1 authored by Robbert Krebbers's avatar Robbert Krebbers

Generalize the Iris language to forking off multiple threads.

This generalization is surprisingly easy in Iris 3.0, so I could not
resist not doing it :).
parent 6acc1682
Pipeline #2572 passed with stage
in 4 minutes and 14 seconds
......@@ -225,53 +225,53 @@ Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
| _, _, _ => None
end.
Inductive head_step : expr state expr state option (expr) Prop :=
Inductive head_step : expr state 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' σ None
head_step (App (Rec f x e1) e2) σ e' σ []
| UnOpS op l l' σ :
un_op_eval op l = Some l'
head_step (UnOp op (Lit l)) σ (Lit l') σ None
head_step (UnOp op (Lit l)) σ (Lit l') σ []
| BinOpS op l1 l2 l' σ :
bin_op_eval op l1 l2 = Some l'
head_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ None
head_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ []
| IfTrueS e1 e2 σ :
head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ None
head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ []
| IfFalseS e1 e2 σ :
head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ None
head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ []
| FstS e1 v1 e2 v2 σ :
to_val e1 = Some v1 to_val e2 = Some v2
head_step (Fst (Pair e1 e2)) σ e1 σ None
head_step (Fst (Pair e1 e2)) σ e1 σ []
| SndS e1 v1 e2 v2 σ :
to_val e1 = Some v1 to_val e2 = Some v2
head_step (Snd (Pair e1 e2)) σ e2 σ None
head_step (Snd (Pair e1 e2)) σ e2 σ []
| CaseLS e0 v0 e1 e2 σ :
to_val e0 = Some v0
head_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ None
head_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ []
| CaseRS e0 v0 e1 e2 σ :
to_val e0 = Some v0
head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ None
head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ []
| ForkS e σ:
head_step (Fork e) σ (Lit LitUnit) σ (Some e)
head_step (Fork e) σ (Lit LitUnit) σ [e]
| AllocS e v σ l :
to_val e = Some v σ !! l = None
head_step (Alloc e) σ (Lit $ LitLoc l) (<[l:=v]>σ) None
head_step (Alloc e) σ (Lit $ LitLoc l) (<[l:=v]>σ) []
| LoadS l v σ :
σ !! l = Some v
head_step (Load (Lit $ LitLoc l)) σ (of_val v) σ None
head_step (Load (Lit $ LitLoc l)) σ (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]>σ) None
head_step (Store (Lit $ LitLoc l) e) σ (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
head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool false) σ None
head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool false) σ []
| CasSucS l e1 v1 e2 v2 σ :
to_val e1 = Some v1 to_val e2 = Some v2
σ !! l = Some v1
head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) [].
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
......@@ -294,11 +294,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_stuck e1 σ1 e2 σ2 ef : head_step e1 σ1 e2 σ2 ef to_val e1 = None.
Lemma val_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 ef :
head_step (fill_item Ki e) σ1 e2 σ2 ef 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 :
......@@ -313,7 +313,7 @@ Qed.
Lemma alloc_fresh e v σ :
let l := fresh (dom _ σ) in
to_val e = Some v head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) None.
to_val e = Some v head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) [].
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
(** Closed expressions *)
......
......@@ -10,7 +10,7 @@ Section lifting.
Context `{irisG heap_lang Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
Implicit Types ef : option expr.
Implicit Types efs : list expr.
(** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
Lemma wp_bind {E e} K Φ :
......@@ -38,7 +38,7 @@ Lemma wp_load_pst E σ l v Φ :
σ !! l = Some v
ownP σ (ownP σ ={E}= Φ v) WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_atomic_det_head_step σ v σ None) ?right_id //;
intros. rewrite -(wp_lift_atomic_det_head_step σ v σ []) ?right_id //;
last (by intros; inv_head_step; eauto using to_of_val). solve_atomic.
Qed.
......@@ -48,7 +48,7 @@ Lemma wp_store_pst E σ l v v' Φ :
WP Store (Lit (LitLoc l)) (of_val v) @ E {{ Φ }}.
Proof.
intros ?.
rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) None)
rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) [])
?right_id //; last (by intros; inv_head_step; eauto). solve_atomic.
Qed.
......@@ -58,7 +58,7 @@ Lemma wp_cas_fail_pst E σ l v1 v2 v' Φ :
WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Φ }}.
Proof.
intros ??.
rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ None)
rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ [])
?right_id //; last (by intros; inv_head_step; eauto). solve_atomic.
Qed.
......@@ -68,7 +68,7 @@ Lemma wp_cas_suc_pst E σ l v1 v2 Φ :
WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Φ }}.
Proof.
intros ?. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool true)
(<[l:=v2]>σ) None) ?right_id //; last (by intros; inv_head_step; eauto).
(<[l:=v2]>σ) []) ?right_id //; last (by intros; inv_head_step; eauto).
solve_atomic.
Qed.
......@@ -76,9 +76,9 @@ Qed.
Lemma wp_fork E e Φ :
(|={E}=> Φ (LitV LitUnit)) WP e {{ _, True }} WP Fork e @ E {{ Φ }}.
Proof.
rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) (Some e)) //=;
rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=;
last by intros; inv_head_step; eauto.
rewrite later_sep -(wp_value_pvs _ _ (Lit _)) //.
by rewrite later_sep -(wp_value_pvs _ _ (Lit _)) // right_id.
Qed.
Lemma wp_rec E f x erec e1 e2 Φ :
......@@ -88,7 +88,7 @@ Lemma wp_rec E f x erec e1 e2 Φ :
WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }} WP App e1 e2 @ E {{ Φ }}.
Proof.
intros -> [v2 ?] ?. rewrite -(wp_lift_pure_det_head_step (App _ _)
(subst' x e2 (subst' f (Rec f x erec) erec)) None) //= ?right_id;
(subst' x e2 (subst' f (Rec f x erec) erec)) []) //= ?right_id;
intros; inv_head_step; eauto.
Qed.
......@@ -96,7 +96,7 @@ Lemma wp_un_op E op l l' Φ :
un_op_eval op l = Some l'
(|={E}=> Φ (LitV l')) WP UnOp op (Lit l) @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (Lit l') None)
intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (Lit l') [])
?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
Qed.
......@@ -104,21 +104,21 @@ Lemma wp_bin_op E op l1 l2 l' Φ :
bin_op_eval op l1 l2 = Some l'
(|={E}=> Φ (LitV l')) WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
Proof.
intros Heval. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (Lit l') None)
intros Heval. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (Lit l') [])
?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
Qed.
Lemma wp_if_true E e1 e2 Φ :
WP e1 @ E {{ Φ }} WP If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}.
Proof.
rewrite -(wp_lift_pure_det_head_step (If _ _ _) e1 None)
rewrite -(wp_lift_pure_det_head_step (If _ _ _) e1 [])
?right_id //; intros; inv_head_step; eauto.
Qed.
Lemma wp_if_false E e1 e2 Φ :
WP e2 @ E {{ Φ }} WP If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
Proof.
rewrite -(wp_lift_pure_det_head_step (If _ _ _) e2 None)
rewrite -(wp_lift_pure_det_head_step (If _ _ _) e2 [])
?right_id //; intros; inv_head_step; eauto.
Qed.
......@@ -126,7 +126,7 @@ Lemma wp_fst E e1 v1 e2 Φ :
to_val e1 = Some v1 is_Some (to_val e2)
(|={E}=> Φ v1) WP Fst (Pair e1 e2) @ E {{ Φ }}.
Proof.
intros ? [v2 ?]. rewrite -(wp_lift_pure_det_head_step (Fst _) e1 None)
intros ? [v2 ?]. rewrite -(wp_lift_pure_det_head_step (Fst _) e1 [])
?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
Qed.
......@@ -134,7 +134,7 @@ Lemma wp_snd E e1 e2 v2 Φ :
is_Some (to_val e1) to_val e2 = Some v2
(|={E}=> Φ v2) WP Snd (Pair e1 e2) @ E {{ Φ }}.
Proof.
intros [v1 ?] ?. rewrite -(wp_lift_pure_det_head_step (Snd _) e2 None)
intros [v1 ?] ?. rewrite -(wp_lift_pure_det_head_step (Snd _) e2 [])
?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
Qed.
......@@ -143,7 +143,7 @@ Lemma wp_case_inl E e0 e1 e2 Φ :
WP App e1 e0 @ E {{ Φ }} WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
Proof.
intros [v0 ?]. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
(App e1 e0) None) ?right_id //; intros; inv_head_step; eauto.
(App e1 e0) []) ?right_id //; intros; inv_head_step; eauto.
Qed.
Lemma wp_case_inr E e0 e1 e2 Φ :
......@@ -151,6 +151,6 @@ Lemma wp_case_inr E e0 e1 e2 Φ :
WP App e2 e0 @ E {{ Φ }} WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
Proof.
intros [v0 ?]. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
(App e2 e0) None) ?right_id //; intros; inv_head_step; eauto.
(App e2 e0) []) ?right_id //; intros; inv_head_step; eauto.
Qed.
End lifting.
......@@ -312,7 +312,7 @@ Tactic Notation "do_head_step" tactic3(tac) :=
try match goal with |- head_reducible _ _ => eexists _, _, _ end;
simpl;
match goal with
| |- head_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
| |- head_step ?e1 ?σ1 ?e2 ?σ2 ?efs =>
first [apply alloc_fresh|econstructor];
(* solve [to_val] side-conditions *)
first [rewrite ?to_of_val; reflexivity|simpl_subst; tac; fast_done]
......
......@@ -20,11 +20,11 @@ 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_safe e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&ef&?)];
destruct (adequate_safe 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'' ++ option_list ef), σ3; econstructor; eauto.
right; exists (t2' ++ e3 :: t2'' ++ efs), σ3; econstructor; eauto.
Qed.
Section adequacy.
......@@ -42,19 +42,17 @@ Lemma wptp_cons e t : wptp (e :: t) ⊣⊢ WP e {{ _, True }} ★ wptp t.
Proof. done. Qed.
Lemma wptp_app t1 t2 : wptp (t1 ++ t2) wptp t1 wptp t2.
Proof. by rewrite /wptp fmap_app big_sep_app. Qed.
Lemma wptp_fork ef : wptp (option_list ef) wp_fork ef.
Proof. destruct ef; by rewrite /wptp /= ?right_id. Qed.
Lemma wp_step e1 σ1 e2 σ2 ef Φ :
prim_step e1 σ1 e2 σ2 ef
world σ1 WP e1 {{ Φ }} =r=> |=r=> (world σ2 WP e2 {{ Φ }} wp_fork ef).
Lemma wp_step e1 σ1 e2 σ2 efs Φ :
prim_step e1 σ1 e2 σ2 efs
world σ1 WP e1 {{ Φ }} =r=> |=r=> (world σ2 WP e2 {{ Φ }} wp_fork efs).
Proof.
rewrite {1}wp_unfold /wp_pre. iIntros (Hstep) "[(Hw & HE & Hσ) [H|[_ H]]]".
{ iDestruct "H" as (v) "[% _]". apply val_stuck in Hstep; simplify_eq. }
rewrite pvs_eq /pvs_def.
iVs ("H" $! σ1 with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame.
iVsIntro; iNext.
iVs ("H" $! e2 σ2 ef with "[%] [Hw HE]")
iVs ("H" $! e2 σ2 efs with "[%] [Hw HE]")
as ">($ & $ & $ & $)"; try iFrame; eauto.
Qed.
......@@ -64,11 +62,11 @@ Lemma wptp_step e1 t1 t2 σ1 σ2 Φ :
=r=> e2 t2', t2 = e2 :: t2' |=r=> (world σ2 WP e2 {{ Φ }} wptp t2').
Proof.
iIntros (Hstep) "(HW & He & Ht)".
destruct Hstep as [e1' σ1' e2' σ2' ef [|? t1'] t2' ?? Hstep]; simplify_eq/=.
- iExists e2', (t2' ++ option_list ef); iSplitR; first eauto.
rewrite wptp_app wptp_fork. iFrame "Ht". iApply wp_step; try iFrame; eauto.
- iExists e, (t1' ++ e2' :: t2' ++ option_list ef); iSplitR; first eauto.
rewrite !wptp_app !wptp_cons wptp_app wptp_fork.
destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=.
- iExists e2', (t2' ++ efs); iSplitR; first eauto.
rewrite wptp_app. iFrame "Ht". iApply wp_step; try iFrame; eauto.
- iExists e, (t1' ++ e2' :: t2' ++ efs); iSplitR; first eauto.
rewrite !wptp_app !wptp_cons wptp_app.
iDestruct "Ht" as "($ & He' & $)"; iFrame "He".
iApply wp_step; try iFrame; eauto.
Qed.
......
......@@ -11,11 +11,11 @@ Class EctxLanguage (expr val ectx state : Type) := {
empty_ectx : ectx;
comp_ectx : ectx ectx ectx;
fill : ectx expr expr;
head_step : expr state expr state option expr Prop;
head_step : expr state expr state list expr Prop;
to_of_val v : to_val (of_val v) = Some v;
of_to_val e v : to_val e = Some v of_val v = e;
val_stuck e1 σ1 e2 σ2 ef : head_step e1 σ1 e2 σ2 ef to_val e1 = None;
val_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs to_val e1 = None;
fill_empty e : fill empty_ectx e = e;
fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e;
......@@ -28,10 +28,10 @@ Class EctxLanguage (expr val ectx state : Type) := {
ectx_positive K1 K2 :
comp_ectx K1 K2 = empty_ectx K1 = empty_ectx K2 = empty_ectx;
step_by_val K K' e1 e1' σ1 e2 σ2 ef :
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 ef
head_step e1' σ1 e2 σ2 efs
exists K'', K' = comp_ectx K K'';
}.
......@@ -57,16 +57,16 @@ Section ectx_language.
Implicit Types (e : expr) (K : ectx).
Definition head_reducible (e : expr) (σ : state) :=
e' σ' ef, head_step e σ e' σ' ef.
e' σ' efs, head_step e σ e' σ' efs.
Inductive prim_step (e1 : expr) (σ1 : state)
(e2 : expr) (σ2 : state) (ef : option expr) : Prop :=
(e2 : expr) (σ2 : state) (efs : list expr) : Prop :=
Ectx_step K e1' e2' :
e1 = fill K e1' e2 = fill K e2'
head_step e1' σ1 e2' σ2 ef prim_step e1 σ1 e2 σ2 ef.
head_step e1' σ1 e2' σ2 efs prim_step e1 σ1 e2 σ2 efs.
Lemma val_prim_stuck e1 σ1 e2 σ2 ef :
prim_step e1 σ1 e2 σ2 ef to_val e1 = None.
Lemma val_prim_stuck e1 σ1 e2 σ2 efs :
prim_step e1 σ1 e2 σ2 efs to_val e1 = None.
Proof. intros [??? -> -> ?]; eauto using fill_not_val, val_stuck. Qed.
Canonical Structure ectx_lang : language := {|
......@@ -78,29 +78,29 @@ Section ectx_language.
|}.
(* Some lemmas about this language *)
Lemma head_prim_step e1 σ1 e2 σ2 ef :
head_step e1 σ1 e2 σ2 ef prim_step e1 σ1 e2 σ2 ef.
Lemma head_prim_step e1 σ1 e2 σ2 efs :
head_step e1 σ1 e2 σ2 efs prim_step e1 σ1 e2 σ2 efs.
Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed.
Lemma head_prim_reducible e σ : head_reducible e σ reducible e σ.
Proof. intros (e'&σ'&ef&?). eexists e', σ', ef. by apply head_prim_step. Qed.
Proof. intros (e'&σ'&efs&?). eexists e', σ', efs. by apply head_prim_step. Qed.
Lemma ectx_language_atomic e :
( σ e' σ' ef, head_step e σ e' σ' ef is_Some (to_val e'))
( σ e' σ' efs, head_step e σ e' σ' efs is_Some (to_val e'))
( K e', e = fill K e' to_val e' = None K = empty_ectx)
atomic e.
Proof.
intros Hatomic_step Hatomic_fill σ e' σ' ef [K e1' e2' -> -> Hstep].
intros Hatomic_step Hatomic_fill σ e' σ' efs [K e1' e2' -> -> Hstep].
assert (K = empty_ectx) as -> by eauto 10 using val_stuck.
rewrite fill_empty. eapply Hatomic_step. by rewrite fill_empty.
Qed.
Lemma head_reducible_prim_step e1 σ1 e2 σ2 ef :
head_reducible e1 σ1 prim_step e1 σ1 e2 σ2 ef
head_step e1 σ1 e2 σ2 ef.
Lemma head_reducible_prim_step e1 σ1 e2 σ2 efs :
head_reducible e1 σ1 prim_step e1 σ1 e2 σ2 efs
head_step e1 σ1 e2 σ2 efs.
Proof.
intros (e2''&σ2''&ef''&?) [K e1' e2' -> -> Hstep].
destruct (step_by_val K empty_ectx e1' (fill K e1') σ1 e2'' σ2'' ef'')
intros (e2''&σ2''&efs''&?) [K e1' e2' -> -> Hstep].
destruct (step_by_val K empty_ectx e1' (fill K e1') σ1 e2'' σ2'' efs'')
as [K' [-> _]%symmetry%ectx_positive];
eauto using fill_empty, fill_not_val, val_stuck.
by rewrite !fill_empty.
......@@ -114,7 +114,7 @@ Section ectx_language.
- intros ????? [K' e1' e2' Heq1 Heq2 Hstep].
by exists (comp_ectx K K') e1' e2'; rewrite ?Heq1 ?Heq2 ?fill_comp.
- intros e1 σ1 e2 σ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep].
destruct (step_by_val K K'' e1 e1'' σ1 e2'' σ2 ef) as [K' ->]; eauto.
destruct (step_by_val K K'' e1 e1'' σ1 e2'' σ2 efs) as [K' ->]; eauto.
rewrite -fill_comp in Heq1; apply (inj (fill _)) in Heq1.
exists (fill K' e2''); rewrite -fill_comp; split; auto.
econstructor; eauto.
......
......@@ -19,21 +19,21 @@ Proof. apply: weakestpre.wp_bind. Qed.
Lemma wp_lift_head_step E Φ e1 :
to_val e1 = None
(|={E,}=> σ1, head_reducible e1 σ1 ownP σ1
e2 σ2 ef, head_step e1 σ1 e2 σ2 ef ownP σ2
={,E}= WP e2 @ E {{ Φ }} wp_fork ef)
e2 σ2 efs, head_step e1 σ1 e2 σ2 efs ownP σ2
={,E}= WP e2 @ E {{ Φ }} wp_fork efs)
WP e1 @ E {{ Φ }}.
Proof.
iIntros (?) "H". iApply (wp_lift_step E); try done.
iVs "H" as (σ1) "(%&Hσ1&Hwp)". iVsIntro. iExists σ1.
iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 ef) "[% ?]".
iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 efs) "[% ?]".
iApply "Hwp". by eauto.
Qed.
Lemma wp_lift_pure_head_step E Φ e1 :
to_val e1 = None
( σ1, head_reducible e1 σ1)
( σ1 e2 σ2 ef, head_step e1 σ1 e2 σ2 ef σ1 = σ2)
( e2 ef σ, head_step e1 σ e2 σ ef WP e2 @ E {{ Φ }} wp_fork ef)
( σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs σ1 = σ2)
( e2 efs σ, head_step e1 σ e2 σ efs WP e2 @ E {{ Φ }} wp_fork efs)
WP e1 @ E {{ Φ }}.
Proof.
iIntros (???) "H". iApply wp_lift_pure_step; eauto. iNext.
......@@ -43,26 +43,26 @@ Qed.
Lemma wp_lift_atomic_head_step {E Φ} e1 σ1 :
atomic e1
head_reducible e1 σ1
ownP σ1 ( v2 σ2 ef,
head_step e1 σ1 (of_val v2) σ2 ef ownP σ2 - (|={E}=> Φ v2) wp_fork ef)
ownP σ1 ( v2 σ2 efs,
head_step e1 σ1 (of_val v2) σ2 efs ownP σ2 - (|={E}=> Φ v2) wp_fork efs)
WP e1 @ E {{ Φ }}.
Proof.
iIntros (??) "[? H]". iApply wp_lift_atomic_step; eauto. iFrame. iNext.
iIntros (???) "[% ?]". iApply "H". eauto.
Qed.
Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 ef :
Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 efs :
atomic e1
head_reducible e1 σ1
( e2' σ2' ef', head_step e1 σ1 e2' σ2' ef'
σ2 = σ2' to_val e2' = Some v2 ef = ef')
ownP σ1 (ownP σ2 - (|={E}=> Φ v2) wp_fork ef) WP e1 @ E {{ Φ }}.
( e2' σ2' efs', head_step e1 σ1 e2' σ2' efs'
σ2 = σ2' to_val e2' = Some v2 efs = efs')
ownP σ1 (ownP σ2 - (|={E}=> Φ v2) wp_fork efs) WP e1 @ E {{ Φ }}.
Proof. eauto using wp_lift_atomic_det_step. Qed.
Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 ef :
Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 efs :
to_val e1 = None
( σ1, head_reducible e1 σ1)
( σ1 e2' σ2 ef', head_step e1 σ1 e2' σ2 ef' σ1 = σ2 e2 = e2' ef = ef')
(WP e2 @ E {{ Φ }} wp_fork ef) WP e1 @ E {{ Φ }}.
( σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' σ1 = σ2 e2 = e2' efs = efs')
(WP e2 @ E {{ Φ }} wp_fork efs) WP e1 @ E {{ Φ }}.
Proof. eauto using wp_lift_pure_det_step. Qed.
End wp.
......@@ -9,11 +9,11 @@ Class EctxiLanguage (expr val ectx_item state : Type) := {
of_val : val expr;
to_val : expr option val;
fill_item : ectx_item expr expr;
head_step : expr state expr state option expr Prop;
head_step : expr state expr state list expr Prop;
to_of_val v : to_val (of_val v) = Some v;
of_to_val e v : to_val e = Some v of_val v = e;
val_stuck e1 σ1 e2 σ2 ef : head_step e1 σ1 e2 σ2 ef to_val e1 = None;
val_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs to_val e1 = None;
fill_item_inj Ki :> Inj (=) (=) (fill_item Ki);
fill_item_val Ki e : is_Some (to_val (fill_item Ki e)) is_Some (to_val e);
......@@ -21,8 +21,8 @@ Class EctxiLanguage (expr val ectx_item state : Type) := {
to_val e1 = None to_val e2 = None
fill_item Ki1 e1 = fill_item Ki2 e2 Ki1 = Ki2;
head_ctx_step_val Ki e σ1 e2 σ2 ef :
head_step (fill_item Ki e) σ1 e2 σ2 ef is_Some (to_val e);
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);
}.
Arguments of_val {_ _ _ _ _} _.
......@@ -60,8 +60,8 @@ Section ectxi_language.
(* When something does a step, and another decomposition of the same expression
has a non-val [e] in the hole, then [K] is a left sub-context of [K'] - in
other words, [e] also contains the reducible expression *)
Lemma step_by_val K K' e1 e1' σ1 e2 σ2 ef :
fill K e1 = fill K' e1' to_val e1 = None head_step e1' σ1 e2 σ2 ef
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
exists K'', K' = K ++ K''. (* K `prefix_of` K' *)
Proof.
intros Hfill Hred Hnval; revert K' Hfill.
......
......@@ -6,10 +6,10 @@ Structure language := Language {
state : Type;
of_val : val expr;
to_val : expr option val;
prim_step : expr state expr state option expr Prop;
prim_step : expr state expr state list expr Prop;
to_of_val v : to_val (of_val v) = Some v;
of_to_val e v : to_val e = Some v of_val v = e;
val_stuck e σ e' σ' ef : prim_step e σ e' σ' ef to_val e = None
val_stuck e σ e' σ' efs : prim_step e σ e' σ' efs to_val e = None
}.
Arguments of_val {_} _.
Arguments to_val {_} _.
......@@ -29,31 +29,31 @@ Section language.
Implicit Types v : val Λ.
Definition reducible (e : expr Λ) (σ : state Λ) :=
e' σ' ef, prim_step e σ e' σ' ef.
e' σ' efs, prim_step e σ e' σ' efs.
Definition atomic (e : expr Λ) : Prop :=
σ e' σ' ef, prim_step e σ e' σ' ef is_Some (to_val e').
σ e' σ' efs, prim_step e σ e' σ' efs is_Some (to_val e').
Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
| step_atomic e1 σ1 e2 σ2 ef t1 t2 :
| step_atomic e1 σ1 e2 σ2 efs t1 t2 :
ρ1 = (t1 ++ e1 :: t2, σ1)
ρ2 = (t1 ++ e2 :: t2 ++ option_list ef, σ2)
prim_step e1 σ1 e2 σ2 ef
ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2)
prim_step e1 σ1 e2 σ2 efs
step ρ1 ρ2.
Lemma of_to_val_flip v e : of_val v = e to_val e = Some v.
Proof. intros <-. by rewrite to_of_val. Qed.
Lemma reducible_not_val e σ : reducible e σ to_val e = None.
Proof. intros (?&?&?&?); eauto using val_stuck. Qed.
Global Instance: Inj (=) (=) (@of_val Λ).
Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
End language.
Class LanguageCtx (Λ : language) (K : expr Λ expr Λ) := {
fill_not_val e :