Commit 288dbd0c authored by Ralf Jung's avatar Ralf Jung

bump Iris and fix logrel

parent 34b978b5
Pipeline #12563 passed with stage
in 6 minutes and 13 seconds
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
"coq-iris" { (= "dev.2018-10-05.4.464c2449") | (= "dev") }
"coq-iris" { (= "dev.2018-10-22.3.4842a060") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......@@ -94,32 +94,32 @@ Module F_mu.
Definition state : Type := ().
Inductive head_step : expr state expr state list expr Prop :=
Inductive head_step : expr state list Empty_set expr state list expr Prop :=
(* β *)
| BetaS e1 e2 v2 σ :
to_val e2 = Some v2
head_step (App (Lam e1) e2) σ e1.[e2/] σ []
head_step (App (Lam e1) e2) σ [] e1.[e2/] σ []
(* Products *)
| 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)) σ [] 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)) σ [] e2 σ []
(* Sums *)
| CaseLS e0 v0 e1 e2 σ :
to_val e0 = Some v0
head_step (Case (InjL e0) e1 e2) σ e1.[e0/] σ []
head_step (Case (InjL e0) e1 e2) σ [] e1.[e0/] σ []
| CaseRS e0 v0 e1 e2 σ :
to_val e0 = Some v0
head_step (Case (InjR e0) e1 e2) σ e2.[e0/] σ []
head_step (Case (InjR e0) e1 e2) σ [] e2.[e0/] σ []
(* Recursive Types *)
| Unfold_Fold e v σ :
to_val e = Some v
head_step (Unfold (Fold e)) σ e σ []
head_step (Unfold (Fold e)) σ [] e σ []
(* Polymorphic Types *)
| TBeta e σ :
head_step (TApp (TLam e)) σ e σ [].
head_step (TApp (TLam e)) σ [] e σ [].
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
......@@ -140,12 +140,12 @@ Module F_mu.
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
Proof. destruct Ki; intros ???; simplify_eq; auto with f_equal. 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 ef :
head_step e1 σ1 κ e2 σ2 ef 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 ef :
head_step (fill_item Ki e) σ1 κ e2 σ2 ef is_Some (to_val e).
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; eauto. Qed.
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
......@@ -158,7 +158,7 @@ Module F_mu.
end; auto.
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 lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
......
......@@ -10,13 +10,13 @@ Section lang_rules.
Ltac inv_head_step :=
repeat match goal with
| 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
end.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl.
Local Hint Constructors head_step.
Local Hint Resolve to_of_val.
......
......@@ -4,20 +4,20 @@ From iris.program_logic Require Import adequacy.
Theorem soundness Σ `{invPreG Σ} e τ e' thp σ σ' :
( `{irisG F_mu_lang Σ}, [] e : τ)
rtc step ([e], σ) (thp, σ') e' thp
rtc erased_step ([e], σ) (thp, σ') e' thp
is_Some (to_val e') reducible e' σ'.
Proof.
intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto).
eapply (wp_adequacy Σ); eauto.
iIntros (Hinv). iModIntro. iExists (λ _, True%I). iSplit=> //.
iIntros (Hinv ?). iModIntro. iExists (λ _ _, True%I). iSplit=> //.
rewrite -(empty_env_subst e).
set (HΣ := IrisG _ _ Hinv (λ _, True)%I).
set (HΣ := IrisG _ _ _ Hinv (λ _ _, True)%I).
iApply (wp_wand with "[]"). iApply Hlog; eauto. by iApply interp_env_nil. auto.
Qed.
Corollary type_soundness e τ e' thp σ σ' :
[] e : τ
rtc step ([e], σ) (thp, σ') e' thp
rtc erased_step ([e], σ) (thp, σ') e' thp
is_Some (to_val e') reducible e' σ'.
Proof.
intros ??. set (Σ := invΣ).
......
......@@ -139,8 +139,8 @@ Qed.
Definition ctx_refines (Γ : list type)
(e e' : expr) (τ : type) := K thp σ v,
typed_ctx K Γ τ [] TUnit
rtc step ([fill_ctx K e], ) (of_val v :: thp, σ)
thp' σ' v', rtc step ([fill_ctx K e'], ) (of_val v' :: thp', σ').
rtc erased_step ([fill_ctx K e], ) (of_val v :: thp, σ)
thp' σ' v', rtc erased_step ([fill_ctx K e'], ) (of_val v' :: thp', σ').
Notation "Γ ⊨ e '≤ctx≤' e' : τ" :=
(ctx_refines Γ e e' τ) (at level 74, e, e', τ at next level).
......
......@@ -126,42 +126,42 @@ Module F_mu_ref.
Definition state : Type := gmap loc val.
Inductive head_step : expr state expr state list expr Prop :=
Inductive head_step : expr state list Empty_set expr state list expr Prop :=
(* β *)
| BetaS e1 e2 v2 σ :
to_val e2 = Some v2
head_step (App (Lam e1) e2) σ e1.[e2/] σ []
head_step (App (Lam e1) e2) σ [] e1.[e2/] σ []
(* Products *)
| 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)) σ [] 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)) σ [] e2 σ []
(* Sums *)
| CaseLS e0 v0 e1 e2 σ :
to_val e0 = Some v0
head_step (Case (InjL e0) e1 e2) σ e1.[e0/] σ []
head_step (Case (InjL e0) e1 e2) σ [] e1.[e0/] σ []
| CaseRS e0 v0 e1 e2 σ :
to_val e0 = Some v0
head_step (Case (InjR e0) e1 e2) σ e2.[e0/] σ []
head_step (Case (InjR e0) e1 e2) σ [] e2.[e0/] σ []
(* Recursive Types *)
| Unfold_Fold e v σ :
to_val e = Some v
head_step (Unfold (Fold e)) σ e σ []
head_step (Unfold (Fold e)) σ [] e σ []
(* Polymorphic Types *)
| TBeta e σ :
head_step (TApp (TLam e)) σ e σ []
head_step (TApp (TLam e)) σ [] e σ []
(* Reference Types *)
| AllocS e v σ l :
to_val e = Some v σ !! l = None
head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) []
head_step (Alloc e) σ [] (Loc l) (<[l:=v]>σ) []
| LoadS l v σ :
σ !! l = Some v
head_step (Load (Loc l)) σ (of_val v) σ []
head_step (Load (Loc l)) σ [] (of_val v) σ []
| StoreS l e v σ :
to_val e = Some v is_Some (σ !! l)
head_step (Store (Loc l) e) σ (Unit) (<[l:=v]>σ) [].
head_step (Store (Loc l) e) σ [] (Unit) (<[l:=v]>σ) [].
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
......@@ -182,12 +182,12 @@ Module F_mu_ref.
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
Proof. destruct Ki; intros ???; simplify_eq; auto with f_equal. 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 ef :
head_step e1 σ1 κ e2 σ2 ef 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 ef :
head_step (fill_item Ki e) σ1 κ e2 σ2 ef is_Some (to_val e).
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; eauto. Qed.
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
......@@ -202,10 +202,10 @@ Module F_mu_ref.
Lemma alloc_fresh e v σ :
let l := fresh (dom (gset loc) σ) in
to_val e = Some v head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) [].
to_val e = Some v head_step (Alloc e) σ [] (Loc l) (<[l:=v]>σ) [].
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. 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 lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
......
......@@ -14,7 +14,7 @@ Class heapG Σ := HeapG {
Instance heapG_irisG `{heapG Σ} : irisG F_mu_ref_lang Σ := {
iris_invG := heapG_invG;
state_interp := gen_heap_ctx
state_interp σ κs := gen_heap_ctx σ
}.
Global Opaque iris_invG.
......@@ -43,13 +43,13 @@ Section lang_rules.
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
end.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl.
Local Hint Constructors head_step.
Local Hint Resolve alloc_fresh.
......@@ -62,7 +62,7 @@ Section lang_rules.
Proof.
iIntros (<- Φ) "_ HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>"; iSplit; first by auto.
iIntros (σ1 ??) "Hσ !>"; iSplit; first by auto.
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Φ".
......@@ -72,7 +72,7 @@ Section lang_rules.
{{{ l {q} v }}} Load (Loc l) @ 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 ??) "Hσ !>". 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Φ".
......@@ -85,7 +85,7 @@ Section lang_rules.
Proof.
iIntros (<-%of_to_val Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iIntros (σ1 ??) "Hσ !>". 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=>//. by iApply "HΦ".
......
......@@ -14,7 +14,7 @@ Class cfgSG Σ := CFGSG { cfg_inG :> inG Σ (authR cfgUR); cfg_name : gname }.
Definition spec_ctx `{cfgSG Σ} (ρ : cfg F_mu_ref_lang) : iProp Σ :=
( e, σ, own cfg_name ( (Excl' e, to_gen_heap σ))
rtc step ρ ([e],σ))%I.
rtc erased_step ρ ([e],σ))%I.
Definition spec_inv `{cfgSG Σ} `{invG Σ} (ρ : cfg F_mu_ref_lang) : iProp Σ :=
inv specN (spec_ctx ρ).
......@@ -50,14 +50,14 @@ Section cfg.
Local Hint Resolve to_of_val.
(** Conversion to tpools and back *)
Lemma step_insert_no_fork K e σ e' σ' :
head_step e σ e' σ' [] step ([fill K e], σ) ([fill K e'], σ').
Proof. intros Hst. eapply (step_atomic _ _ _ _ _ _ [] [] []); eauto.
Lemma step_insert_no_fork K e σ κ e' σ' :
head_step e σ κ e' σ' [] erased_step ([fill K e], σ) ([fill K e'], σ').
Proof. intros Hst. eexists. eapply (step_atomic _ _ _ _ _ _ _ [] [] []); eauto.
by apply: Ectx_step'.
Qed.
Lemma step_pure E ρ K e e' :
( σ, head_step e σ e' σ [])
( σ, head_step e σ [] e' σ [])
nclose specN E
spec_inv ρ fill K e ={E}= fill K e'.
Proof.
......
......@@ -10,15 +10,15 @@ Class heapPreG Σ := HeapPreG {
Theorem soundness Σ `{heapPreG Σ} e τ e' thp σ σ' :
( `{heapG Σ}, [] e : τ)
rtc step ([e], σ) (thp, σ') e' thp
rtc erased_step ([e], σ) (thp, σ') e' thp
is_Some (to_val e') reducible e' σ'.
Proof.
intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto).
eapply (wp_adequacy Σ _); eauto.
iIntros (Hinv).
iIntros (Hinv ?).
iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh".
{ apply (auth_auth_valid _ (to_gen_heap_valid _ _ σ)). }
iModIntro. iExists (λ σ, own γ ( to_gen_heap σ)); iFrame.
iModIntro. iExists (λ σ _, own γ ( to_gen_heap σ)); iFrame.
set (HeapΣ := (HeapG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
iApply (wp_wand with "[]").
- rewrite -(empty_env_subst e).
......@@ -28,7 +28,7 @@ Qed.
Corollary type_soundness e τ e' thp σ σ' :
[] e : τ
rtc step ([e], σ) (thp, σ') e' thp
rtc erased_step ([e], σ) (thp, σ') e' thp
is_Some (to_val e') reducible e' σ'.
Proof.
intros ??. set (Σ := #[invΣ ; gen_heapΣ loc val]).
......
......@@ -7,14 +7,14 @@ From iris_examples.logrel.F_mu_ref Require Import soundness.
Lemma basic_soundness Σ `{heapPreG Σ, inG Σ (authR cfgUR)}
e e' τ v thp hp :
( `{heapG Σ, cfgSG Σ}, [] e log e' : τ)
rtc step ([e], ) (of_val v :: thp, hp)
( thp' hp' v', rtc step ([e'], ) (of_val v' :: thp', hp')).
rtc erased_step ([e], ) (of_val v :: thp, hp)
( thp' hp' v', rtc erased_step ([e'], ) (of_val v' :: thp', hp')).
Proof.
intros Hlog Hsteps.
cut (adequate NotStuck e (λ _ _, thp' h v, rtc step ([e'], ) (of_val v :: thp', h))).
cut (adequate NotStuck e (λ _ _, thp' h v, rtc erased_step ([e'], ) (of_val v :: thp', h))).
{ destruct 1; naive_solver. }
eapply (wp_adequacy Σ); first by apply _.
iIntros (Hinv).
iIntros (Hinv ?).
iMod (own_alloc ( to_gen_heap )) as (γ) "Hh".
{ apply (auth_auth_valid _ (to_gen_heap_valid _ _ )). }
iMod (own_alloc ( (Excl' e', )
......@@ -26,7 +26,7 @@ Proof.
rewrite /to_gen_heap fin_maps.map_fmap_empty.
iFrame. }
set (HeapΣ := HeapG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ)).
iExists (λ σ, own γ ( to_gen_heap σ)); iFrame.
iExists (λ σ _, own γ ( to_gen_heap σ)); iFrame.
iApply wp_fupd. iApply (wp_wand with "[-]").
- iPoseProof (Hlog _ _ with "[$Hcfg]") as "Hrel".
{ iApply (@logrel_binary.interp_env_nil Σ HeapΣ). }
......
......@@ -191,8 +191,8 @@ Definition ctx_refines (Γ : list type)
typed Γ e τ typed Γ e' τ
K thp σ v,
typed_ctx K Γ τ [] TUnit
rtc step ([fill_ctx K e], ) (of_val v :: thp, σ)
thp' σ' v', rtc step ([fill_ctx K e'], ) (of_val v' :: thp', σ').
rtc erased_step ([fill_ctx K e], ) (of_val v :: thp, σ)
thp' σ' v', rtc erased_step ([fill_ctx K e'], ) (of_val v' :: thp', σ').
Notation "Γ ⊨ e '≤ctx≤' e' : τ" :=
(ctx_refines Γ e e' τ) (at level 74, e, e', τ at next level).
......
......@@ -172,62 +172,62 @@ Module F_mu_ref_conc.
Definition state : Type := gmap loc val.
Inductive head_step : expr state expr state list expr Prop :=
Inductive head_step : expr state list Empty_set expr state list expr Prop :=
(* β *)
| BetaS e1 e2 v2 σ :
to_val e2 = Some v2
head_step (App (Rec e1) e2) σ e1.[(Rec e1), e2/] σ []
head_step (App (Rec e1) e2) σ [] e1.[(Rec e1), e2/] σ []
(* Products *)
| 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)) σ [] 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)) σ [] e2 σ []
(* Sums *)
| CaseLS e0 v0 e1 e2 σ :
to_val e0 = Some v0
head_step (Case (InjL e0) e1 e2) σ e1.[e0/] σ []
head_step (Case (InjL e0) e1 e2) σ [] e1.[e0/] σ []
| CaseRS e0 v0 e1 e2 σ :
to_val e0 = Some v0
head_step (Case (InjR e0) e1 e2) σ e2.[e0/] σ []
head_step (Case (InjR e0) e1 e2) σ [] e2.[e0/] σ []
(* nat bin op *)
| BinOpS op a b σ :
head_step (BinOp op (#n a) (#n b)) σ (of_val (binop_eval op a b)) σ []
head_step (BinOp op (#n a) (#n b)) σ [] (of_val (binop_eval op a b)) σ []
(* If then else *)
| IfFalse e1 e2 σ :
head_step (If (# false) e1 e2) σ e2 σ []
head_step (If (# false) e1 e2) σ [] e2 σ []
| IfTrue e1 e2 σ :
head_step (If (# true) e1 e2) σ e1 σ []
head_step (If (# true) e1 e2) σ [] e1 σ []
(* Recursive Types *)
| Unfold_Fold e v σ :
to_val e = Some v
head_step (Unfold (Fold e)) σ e σ []
head_step (Unfold (Fold e)) σ [] e σ []
(* Polymorphic Types *)
| TBeta e σ :
head_step (TApp (TLam e)) σ e σ []
head_step (TApp (TLam e)) σ [] e σ []
(* Concurrency *)
| ForkS e σ:
head_step (Fork e) σ Unit σ [e]
head_step (Fork e) σ [] Unit σ [e]
(* Reference Types *)
| AllocS e v σ l :
to_val e = Some v σ !! l = None
head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) []
head_step (Alloc e) σ [] (Loc l) (<[l:=v]>σ) []
| LoadS l v σ :
σ !! l = Some v
head_step (Load (Loc l)) σ (of_val v) σ []
head_step (Load (Loc l)) σ [] (of_val v) σ []
| StoreS l e v σ :
to_val e = Some v is_Some (σ !! l)
head_step (Store (Loc l) e) σ Unit (<[l:=v]>σ) []
head_step (Store (Loc l) e) σ [] Unit (<[l:=v]>σ) []
(* Compare and swap *)
| 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 (Loc l) e1 e2) σ (# false) σ []
head_step (CAS (Loc l) e1 e2) σ [] (# false) σ []
| CasSucS l e1 v1 e2 v2 σ :
to_val e1 = Some v1 to_val e2 = Some v2
σ !! l = Some v1
head_step (CAS (Loc l) e1 e2) σ (# true) (<[l:=v2]>σ) [].
head_step (CAS (Loc l) e1 e2) σ [] (# true) (<[l:=v2]>σ) [].
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
......@@ -248,12 +248,12 @@ Module F_mu_ref_conc.
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
Proof. destruct Ki; intros ???; simplify_eq; auto with f_equal. 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 κs e2 σ2 ef :
head_step e1 σ1 κs e2 σ2 ef 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 κs e2 σ2 ef :
head_step (fill_item Ki e) σ1 κs e2 σ2 ef is_Some (to_val e).
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; eauto. Qed.
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
......@@ -268,10 +268,10 @@ Module F_mu_ref_conc.
Lemma alloc_fresh e v σ :
let l := fresh (dom (gset loc) σ) in
to_val e = Some v head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) [].
to_val e = Some v head_step (Alloc e) σ [] (Loc l) (<[l:=v]>σ) [].
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. 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 κs e2 σ2 efs : head_step e1 σ1 κs e2 σ2 efs to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.
Lemma lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
......
......@@ -16,7 +16,7 @@ Class heapIG Σ := HeapIG {
Instance heapIG_irisG `{heapIG Σ} : irisG F_mu_ref_conc_lang Σ := {
iris_invG := heapI_invG;
state_interp := gen_heap_ctx
state_interp σ κs := gen_heap_ctx σ
}.
Global Opaque iris_invG.
......@@ -38,14 +38,14 @@ Section lang_rules.
| H : to_val _ = Some _ |- _ => apply of_to_val in H
| H : _ = of_val ?v |- _ =>
is_var v; destruct v; first[discriminate H|injection H as 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
end.
Local Hint Extern 0 (atomic _) => solve_atomic.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl.
Local Hint Constructors head_step.
Local Hint Resolve alloc_fresh.
......@@ -57,7 +57,7 @@ Section lang_rules.
{{{ True }}} Alloc e @ E {{{ l, RET (LocV l); l ↦ᵢ v }}}.
Proof.
iIntros (<- Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>"; iSplit; first by auto.
iIntros (σ1 ??) "Hσ !>"; iSplit; first by auto.
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Φ".
......@@ -67,7 +67,7 @@ Section lang_rules.
{{{ l ↦ᵢ{q} v }}} Load (Loc l) @ 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 ??) "Hσ !>". 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Φ".
......@@ -80,7 +80,7 @@ Section lang_rules.
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 ??) "Hσ !>". 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=>//. by iApply "HΦ".
......@@ -93,7 +93,7 @@ Section lang_rules.
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 ??) "Hσ !>". 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Φ".
......@@ -106,7 +106,7 @@ Section lang_rules.
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 ??) "Hσ !>". 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=>//. by iApply "HΦ".
......
......@@ -31,7 +31,7 @@ Section definitionsS.
Definition spec_inv (ρ : cfg F_mu_ref_conc_lang) : iProp Σ :=
( tp σ, own cfg_name ( (to_tpool tp, to_gen_heap σ))
rtc step ρ (tp,σ))%I.
rtc erased_step ρ (tp,σ))%I.
Definition spec_ctx (ρ : cfg F_mu_ref_conc_lang) : iProp Σ :=
inv specN (spec_inv ρ).
......@@ -135,24 +135,24 @@ Section cfg.
Local Hint Resolve to_tpool_insert'.
Local Hint Resolve tpool_singleton_included.
Lemma step_insert K tp j e σ e' σ' efs :
tp !! j = Some (fill K e) head_step e σ e' σ' efs
step (tp, σ) (<[j:=fill K e']> tp ++ efs, σ').
Lemma step_insert K tp j e σ κ e' σ' efs :
tp !! j = Some (fill K e) head_step e σ κ e' σ' efs
erased_step (tp, σ) (<[j:=fill K e']> tp ++ efs, σ').
Proof.
intros. rewrite -(take_drop_middle tp j (fill K e)) //.
rewrite insert_app_r_alt take_length_le ?Nat.sub_diag /=;
eauto using lookup_lt_Some, Nat.lt_le_incl.
rewrite -(assoc_L (++)) /=.
rewrite -(assoc_L (++)) /=. eexists.
eapply step_atomic; eauto. by apply: Ectx_step'.
Qed.
Lemma step_insert_no_fork K tp j e σ e' σ' :
tp !! j = Some (fill K e) head_step e σ e' σ' []
step (tp, σ) (<[j:=fill K e']> tp, σ').
Lemma step_insert_no_fork K tp j e σ κ e' σ' :
tp !! j = Some (fill K e) head_step e σ κ e' σ' []
erased_step (tp, σ) (<[j:=fill K e']> tp, σ').
Proof. rewrite -(right_id_L [] (++) (<[_:=_]>_)). by apply step_insert. Qed.
Lemma step_pure E ρ j K e e' :
( σ, head_step e σ e' σ [])
( σ, head_step e σ [] e' σ [])
nclose specN E
spec_ctx ρ j fill K e ={E}= j fill K e'.
Proof.
......
......@@ -7,13 +7,13 @@ From iris_examples.logrel.F_mu_ref_conc Require Import soundness_unary.
Lemma basic_soundness Σ `{heapPreIG Σ, inG Σ (authR cfgUR)}
e e' τ v thp hp :
( `{heapIG Σ, cfgSG Σ}, [] e log e' : τ)
rtc step ([e], ) (of_val v :: thp, hp)
( thp' hp' v', rtc step ([e'], ) (of_val v' :: thp', hp')).
rtc erased_step ([e], ) (of_val v :: thp, hp)
( thp' hp' v', rtc erased_step ([e'], ) (of_val v' :: thp', hp')).
Proof.