Skip to content

GitLab

Commit a0dfafa6 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 797d2d16 a3ef214f
Hide whitespace changes
Inline Side-by-side
algebra/upred_big_op.v
View file @ a0dfafa6
......@@ -244,6 +244,12 @@ Section list.
by rewrite sep_elim_r sep_elim_l.
Qed.
Lemma big_sepL_elem_of (Φ : A → uPred M) l x :
x ∈ l → ([★ list] y ∈ l, Φ y) ⊢ Φ x.
Proof.
intros [i ?]%elem_of_list_lookup; eauto using (big_sepL_lookup (λ _, Φ)).
Qed.
Lemma big_sepL_fmap {B} (f : A → B) (Φ : nat → B → uPred M) l :
([★ list] k↦y ∈ f <$> l, Φ k y) ⊣⊢ ([★ list] k↦y ∈ l, Φ k (f y)).
Proof. by rewrite /uPred_big_sepL imap_fmap. Qed.
......@@ -302,12 +308,18 @@ Section list.
by rewrite -always_wand_impl always_elim wand_elim_l.
Qed.
Global Instance big_sepL_persistent Φ m :
(∀ k x, PersistentP (Φ k x)) → PersistentP ([★ list] k↦x ∈ m, Φ k x).
Global Instance big_sepL_nil_persistent Φ :
PersistentP ([★ list] k↦x ∈ [], Φ k x).
Proof. rewrite /uPred_big_sepL. apply _. Qed.
Global Instance big_sepL_persistent Φ l :
(∀ k x, PersistentP (Φ k x)) → PersistentP ([★ list] k↦x ∈ l, Φ k x).
Proof. rewrite /uPred_big_sepL. apply _. Qed.
Global Instance big_sepL_timeless Φ m :
(∀ k x, TimelessP (Φ k x)) → TimelessP ([★ list] k↦x ∈ m, Φ k x).
Global Instance big_sepL_nil_timeless Φ :
TimelessP ([★ list] k↦x ∈ [], Φ k x).
Proof. rewrite /uPred_big_sepL. apply _. Qed.
Global Instance big_sepL_timeless Φ l :
(∀ k x, TimelessP (Φ k x)) → TimelessP ([★ list] k↦x ∈ l, Φ k x).
Proof. rewrite /uPred_big_sepL. apply _. Qed.
End list.
......@@ -462,10 +474,16 @@ Section gmap.
by rewrite -always_wand_impl always_elim wand_elim_l.
Qed.
Global Instance big_sepM_empty_persistent Φ :
PersistentP ([★ map] k↦x ∈ ∅, Φ k x).
Proof. rewrite /uPred_big_sepM map_to_list_empty. apply _. Qed.
Global Instance big_sepM_persistent Φ m :
(∀ k x, PersistentP (Φ k x)) → PersistentP ([★ map] k↦x ∈ m, Φ k x).
Proof. intros. apply big_sep_persistent, fmap_persistent=>-[??] /=; auto. Qed.
Global Instance big_sepM_nil_timeless Φ :
TimelessP ([★ map] k↦x ∈ ∅, Φ k x).
Proof. rewrite /uPred_big_sepM map_to_list_empty. apply _. Qed.
Global Instance big_sepM_timeless Φ m :
(∀ k x, TimelessP (Φ k x)) → TimelessP ([★ map] k↦x ∈ m, Φ k x).
Proof. intro. apply big_sep_timeless, fmap_timeless=> -[??] /=; auto. Qed.
......@@ -590,10 +608,14 @@ Section gset.
by rewrite -always_wand_impl always_elim wand_elim_l.
Qed.
Global Instance big_sepS_empty_persistent Φ : PersistentP ([★ set] x ∈ ∅, Φ x).
Proof. rewrite /uPred_big_sepS elements_empty. apply _. Qed.
Global Instance big_sepS_persistent Φ X :
(∀ x, PersistentP (Φ x)) → PersistentP ([★ set] x ∈ X, Φ x).
Proof. rewrite /uPred_big_sepS. apply _. Qed.
Global Instance big_sepS_nil_timeless Φ : TimelessP ([★ set] x ∈ ∅, Φ x).
Proof. rewrite /uPred_big_sepS elements_empty. apply _. Qed.
Global Instance big_sepS_timeless Φ X :
(∀ x, TimelessP (Φ x)) → TimelessP ([★ set] x ∈ X, Φ x).
Proof. rewrite /uPred_big_sepS. apply _. Qed.
......
heap_lang/lifting.v
View file @ a0dfafa6
......@@ -53,14 +53,14 @@ Proof.
iApply (wp_lift_atomic_head_step (Alloc (of_val v)) σ); eauto.
iFrame "HP". iNext. iIntros (v2 σ2 ef) "[% HP]". inv_head_step.
match goal with H: _ = of_val v2 |- _ => apply (inj of_val (LitV _)) in H end.
subst v2. iSplit; last done. iApply "HΦ"; by iSplit.
subst v2. iSplit. iApply "HΦ"; by iSplit. by iApply big_sepL_nil.
Qed.
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 σ []) ?right_id; eauto 10.
intros. rewrite -(wp_lift_atomic_det_head_step' σ v σ); eauto 10.
intros; inv_head_step; eauto 10.
Qed.
......@@ -69,8 +69,7 @@ Lemma wp_store_pst E σ l v v' Φ :
▷ ownP σ ★ ▷ (ownP (<[l:=v]>σ) ={E}=★ Φ (LitV LitUnit))
⊢ WP Store (Lit (LitLoc l)) (of_val v) @ E {{ Φ }}.
Proof.
intros. rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) [])
?right_id; eauto.
intros. rewrite-(wp_lift_atomic_det_head_step' σ (LitV LitUnit) (<[l:=v]>σ)); eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -79,8 +78,7 @@ Lemma wp_cas_fail_pst E σ l v1 v2 v' Φ :
▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ (LitV $ LitBool false))
⊢ WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ [])
?right_id; eauto.
intros. rewrite -(wp_lift_atomic_det_head_step' σ (LitV $ LitBool false) σ); eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -89,8 +87,8 @@ Lemma wp_cas_suc_pst E σ l v1 v2 Φ :
▷ ownP σ ★ ▷ (ownP (<[l:=v2]>σ) ={E}=★ Φ (LitV $ LitBool true))
⊢ 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]>σ) []) ?right_id //; eauto 10.
intros. rewrite -(wp_lift_atomic_det_head_step' σ (LitV $ LitBool true)
(<[l:=v2]>σ)); eauto 10.
intros; inv_head_step; eauto.
Qed.
......@@ -99,7 +97,7 @@ 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) [e]) //=; eauto.
- by rewrite later_sep -(wp_value_pvs _ _ (Lit _)) // right_id.
- by rewrite later_sep -(wp_value_pvs _ _ (Lit _)) // big_sepL_singleton.
- intros; inv_head_step; eauto.
Qed.
......@@ -109,8 +107,8 @@ Lemma wp_rec E f x erec e1 e2 Φ :
Closed (f :b: x :b: []) erec →
▷ 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)) []) //= ?right_id; eauto.
intros -> [v2 ?] ?. rewrite -(wp_lift_pure_det_head_step' (App _ _)
(subst' x e2 (subst' f (Rec f x erec) erec))); eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -119,8 +117,8 @@ Lemma wp_un_op E op e v v' Φ :
un_op_eval op v = Some v' →
▷ (|={E}=> Φ v') ⊢ WP UnOp op e @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (of_val v') [])
?right_id -?wp_value_pvs'; eauto.
intros. rewrite -(wp_lift_pure_det_head_step' (UnOp op _) (of_val v'))
-?wp_value_pvs'; eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -129,22 +127,22 @@ Lemma wp_bin_op E op e1 e2 v1 v2 v' Φ :
bin_op_eval op v1 v2 = Some v' →
▷ (|={E}=> Φ v') ⊢ WP BinOp op e1 e2 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (of_val v') [])
?right_id -?wp_value_pvs'; eauto.
intros. rewrite -(wp_lift_pure_det_head_step' (BinOp op _ _) (of_val v'))
-?wp_value_pvs'; eauto.
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 []) ?right_id; eauto.
rewrite -(wp_lift_pure_det_head_step' (If _ _ _) e1); eauto.
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 []) ?right_id; eauto.
rewrite -(wp_lift_pure_det_head_step' (If _ _ _) e2); eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -152,8 +150,8 @@ 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 [])
?right_id -?wp_value_pvs; eauto.
intros ? [v2 ?].
rewrite -(wp_lift_pure_det_head_step' (Fst _) e1) -?wp_value_pvs; eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -161,8 +159,8 @@ 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 [])
?right_id -?wp_value_pvs; eauto.
intros [v1 ?] ?.
rewrite -(wp_lift_pure_det_head_step' (Snd _) e2) -?wp_value_pvs; eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -170,8 +168,8 @@ Lemma wp_case_inl E e0 e1 e2 Φ :
is_Some (to_val e0) →
▷ 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) []) ?right_id; eauto.
intros [v0 ?].
rewrite -(wp_lift_pure_det_head_step' (Case _ _ _) (App e1 e0)); eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -179,8 +177,8 @@ Lemma wp_case_inr E e0 e1 e2 Φ :
is_Some (to_val e0) →
▷ 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) []) ?right_id; eauto.
intros [v0 ?].
rewrite -(wp_lift_pure_det_head_step' (Case _ _ _) (App e2 e0)); eauto.
intros; inv_head_step; eauto.
Qed.
End lifting.
program_logic/adequacy.v
View file @ a0dfafa6
......@@ -36,16 +36,11 @@ Implicit Types Φs : list (val Λ → iProp Σ).
Notation world σ := (wsat ★ ownE ⊤ ★ ownP_auth σ)%I.
Definition wptp (t : list (expr Λ)) := ([★] (flip (wp ⊤) (λ _, True) <$> t))%I.
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.
Notation wptp t := ([★ list] ef ∈ t, WP ef {{ _, True }})%I.
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).
world σ1 ★ WP e1 {{ Φ }} =r=> ▷ |=r=> ◇ (world σ2 ★ WP e2 {{ Φ }} ★ wptp 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. }
......@@ -64,9 +59,9 @@ 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.
rewrite wptp_app. iFrame "Ht". iApply wp_step; try iFrame; eauto.
rewrite big_sepL_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.
rewrite !big_sepL_app !big_sepL_cons big_sepL_app.
iDestruct "Ht" as "($ & He' & $)"; iFrame "He".
iApply wp_step; try iFrame; eauto.
Qed.
......@@ -123,8 +118,7 @@ Proof.
intros ? He2. rewrite wptp_steps //; rewrite (Nat_iter_S_r (S n)). apply rvs_iter_mono.
iDestruct 1 as (e2' t2') "(% & Hw & H & Htp)"; simplify_eq.
apply elem_of_cons in He2 as [<-|?]; first (iApply wp_safe; by iFrame "Hw H").
iApply wp_safe. iFrame "Hw".
iApply (big_sep_elem_of with "Htp"); apply elem_of_list_fmap; eauto.
iApply wp_safe. iFrame "Hw". by iApply (big_sepL_elem_of with "Htp").
Qed.
Lemma wptp_invariance n e1 e2 t1 t2 σ1 σ2 I φ Φ :
......@@ -153,12 +147,12 @@ Proof.
eapply (adequacy (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
rewrite Nat_iter_S. iVs (iris_alloc σ) as (?) "(?&?&?&Hσ)".
iVsIntro. iNext. iApply wptp_result; eauto.
iFrame. iSplitL; auto. by iApply Hwp.
iFrame. iSplitL. by iApply Hwp. by iApply big_sepL_nil.
- intros t2 σ2 e2 [n ?]%rtc_nsteps ?.
eapply (adequacy (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
rewrite Nat_iter_S. iVs (iris_alloc σ) as (?) "(Hw & HE & Hσ & Hσf)".
iVsIntro. iNext. iApply wptp_safe; eauto.
iFrame "Hw HE Hσ". iSplitL; auto. by iApply Hwp.
iFrame "Hw HE Hσ". iSplitL. by iApply Hwp. by iApply big_sepL_nil.
Qed.
Theorem wp_invariance Σ `{irisPreG Λ Σ} e σ1 t2 σ2 I φ Φ :
......@@ -172,5 +166,5 @@ Proof.
rewrite Nat_iter_S. iVs (iris_alloc σ1) as (?) "(Hw & HE & ? & Hσ)".
rewrite pvs_eq in Hwp.
iVs (Hwp _ with "Hσ [Hw HE]") as ">(? & ? & ? & ?)"; first by iFrame.
iVsIntro. iNext. iApply wptp_invariance; eauto. by iFrame.
iVsIntro. iNext. iApply wptp_invariance; eauto. iFrame. by iApply big_sepL_nil.
Qed.
program_logic/ectx_lifting.v
View file @ a0dfafa6
......@@ -20,7 +20,7 @@ Lemma wp_lift_head_step E Φ e1 :
to_val e1 = None →
(|={E,∅}=> ∃ σ1, ■ head_reducible e1 σ1 ★ ▷ ownP σ1 ★
▷ ∀ e2 σ2 efs, ■ head_step e1 σ1 e2 σ2 efs ★ ownP σ2
={∅,E}=★ WP e2 @ E {{ Φ }} ★ wp_fork efs)
={∅,E}=★ WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
⊢ WP e1 @ E {{ Φ }}.
Proof.
iIntros (?) "H". iApply (wp_lift_step E); try done.
......@@ -33,7 +33,8 @@ Lemma wp_lift_pure_head_step E Φ e1 :
to_val e1 = None →
(∀ σ1, head_reducible e1 σ1) →
(∀ σ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)
(▷ ∀ e2 efs σ, ■ head_step e1 σ e2 σ efs →
WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
⊢ WP e1 @ E {{ Φ }}.
Proof.
iIntros (???) "H". iApply wp_lift_pure_step; eauto. iNext.
......@@ -44,7 +45,8 @@ Lemma wp_lift_atomic_head_step {E Φ} e1 σ1 :
atomic e1 →
head_reducible e1 σ1 →
▷ ownP σ1 ★ ▷ (∀ v2 σ2 efs,
■ head_step e1 σ1 (of_val v2) σ2 efs ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork efs)
■ head_step e1 σ1 (of_val v2) σ2 efs ∧ ownP σ2 -★
(|={E}=> Φ v2) ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
⊢ WP e1 @ E {{ Φ }}.
Proof.
iIntros (??) "[? H]". iApply wp_lift_atomic_step; eauto. iFrame. iNext.
......@@ -56,13 +58,36 @@ Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 efs :
head_reducible e1 σ1 →
(∀ 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 {{ Φ }}.
▷ ownP σ1 ★ ▷ (ownP σ2 -★
(|={E}=> Φ v2) ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
⊢ WP e1 @ E {{ Φ }}.
Proof. eauto using wp_lift_atomic_det_step. Qed.
Lemma wp_lift_atomic_det_head_step' {E Φ e1} σ1 v2 σ2 :
atomic e1 →
head_reducible e1 σ1 →
(∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
▷ ownP σ1 ★ ▷ (ownP σ2 ={E}=★ Φ v2) ⊢ WP e1 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_atomic_det_head_step σ1 v2 σ2 [])
?big_sepL_nil ?right_id; eauto.
Qed.
Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 efs :
to_val e1 = None →
(∀ σ1, head_reducible e1 σ1) →
(∀ σ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 {{ Φ }}.
(∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
▷ (WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
⊢ WP e1 @ E {{ Φ }}.
Proof. eauto using wp_lift_pure_det_step. Qed.
Lemma wp_lift_pure_det_head_step' {E Φ} e1 e2 :
to_val e1 = None →
(∀ σ1, head_reducible e1 σ1) →
(∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
Qed.
End wp.
program_logic/lifting.v
View file @ a0dfafa6
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ownership.
From iris.algebra Require Export upred_big_op.
From iris.proofmode Require Import pviewshifts.
Section lifting.
......@@ -14,7 +15,7 @@ Lemma wp_lift_step E Φ e1 :
to_val e1 = None →
(|={E,∅}=> ∃ σ1, ■ reducible e1 σ1 ★ ▷ ownP σ1 ★
▷ ∀ e2 σ2 efs, ■ prim_step e1 σ1 e2 σ2 efs ★ ownP σ2
={∅,E}=★ WP e2 @ E {{ Φ }} ★ wp_fork efs)
={∅,E}=★ WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
⊢ WP e1 @ E {{ Φ }}.
Proof.
iIntros (?) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
......@@ -29,7 +30,8 @@ Lemma wp_lift_pure_step E Φ e1 :
to_val e1 = None →
(∀ σ1, reducible e1 σ1) →
(∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
(▷ ∀ e2 efs σ, ■ prim_step e1 σ e2 σ efs → WP e2 @ E {{ Φ }} ★ wp_fork efs)
(▷ ∀ e2 efs σ, ■ prim_step e1 σ e2 σ efs →
WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
⊢ WP e1 @ E {{ Φ }}.
Proof.
iIntros (He Hsafe Hstep) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
......@@ -43,8 +45,8 @@ Qed.
Lemma wp_lift_atomic_step {E Φ} e1 σ1 :
atomic e1 →
reducible e1 σ1 →
▷ ownP σ1 ★ ▷ (∀ v2 σ2 efs,
■ prim_step e1 σ1 (of_val v2) σ2 efs ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork efs)
▷ ownP σ1 ★ ▷ (∀ v2 σ2 efs, ■ prim_step e1 σ1 (of_val v2) σ2 efs ∧ ownP σ2 -★
(|={E}=> Φ v2) ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
⊢ WP e1 @ E {{ Φ }}.
Proof.
iIntros (Hatomic ?) "[Hσ H]".
......@@ -62,7 +64,9 @@ Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs :
reducible e1 σ1 →
(∀ e2' σ2' efs', prim_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 {{ Φ }}.
▷ ownP σ1 ★ ▷ (ownP σ2 -★
(|={E}=> Φ v2) ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
⊢ WP e1 @ E {{ Φ }}.
Proof.
iIntros (?? Hdet) "[Hσ1 Hσ2]". iApply (wp_lift_atomic_step _ σ1); try done.
iFrame. iNext. iIntros (v2' σ2' efs') "[% Hσ2']".
......@@ -73,7 +77,8 @@ Lemma wp_lift_pure_det_step {E Φ} e1 e2 efs :
to_val e1 = None →
(∀ σ1, reducible e1 σ1) →
(∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
▷ (WP e2 @ E {{ Φ }} ★ wp_fork efs) ⊢ WP e1 @ E {{ Φ }}.
▷ (WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
⊢ WP e1 @ E {{ Φ }}.
Proof.
iIntros (?? Hpuredet) "?". iApply (wp_lift_pure_step E); try done.
by intros; eapply Hpuredet. iNext. by iIntros (e' efs' σ (_&->&->)%Hpuredet).
......
program_logic/weakestpre.v
View file @ a0dfafa6
......@@ -15,7 +15,7 @@ Definition wp_pre `{irisG Λ Σ}
ownP_auth σ1 ={E,∅}=★ ■ reducible e1 σ1 ★
▷ ∀ e2 σ2 efs, ■ prim_step e1 σ1 e2 σ2 efs ={∅,E}=★
ownP_auth σ2 ★ wp E e2 Φ ★
[★] (flip (wp ⊤) (λ _, True) <$> efs)))%I.
[★ list] ef ∈ efs, wp ⊤ ef (λ _, True)))%I.
Local Instance wp_pre_contractive `{irisG Λ Σ} : Contractive wp_pre.
Proof.
......@@ -24,7 +24,7 @@ Proof.
apply pvs_ne, sep_ne, later_contractive; auto=> i ?.
apply forall_ne=> e2; apply forall_ne=> σ2; apply forall_ne=> efs.
apply wand_ne, pvs_ne, sep_ne, sep_ne; auto; first by apply Hwp.
eapply big_sep_ne, list_fmap_ext_ne=> ef. by apply Hwp.
apply big_sepL_ne=> ? ef. by apply Hwp.
Qed.
Definition wp_def `{irisG Λ Σ} :
......@@ -50,8 +50,6 @@ Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'WP' e {{ v , Q } }") : uPred_scope.
Notation wp_fork efs := ([★] (flip (wp ⊤) (λ _, True) <$> efs))%I.
Section wp.
Context `{irisG Λ Σ}.
Implicit Types P : iProp Σ.
......
tests/atomic.v
View file @ a0dfafa6
From iris.program_logic Require Export hoare weakestpre.
From iris.program_logic Require Export pviewshifts.
From iris.program_logic Require Import ownership.
From iris.program_logic Require Export hoare weakestpre pviewshifts ownership.
From iris.algebra Require Import upred_big_op.
From iris.prelude Require Export coPset.
From iris.proofmode Require Import tactics pviewshifts weakestpre.
Import uPred.
Section atomic.
Context `{irisG Λ Σ}.
(* <x, α> e @ E_i, E_o <v, β x v> *)
Definition atomic_triple {A: Type}
Context `{irisG Λ Σ} {A: Type}.
(* logically atomic triple: <x, α> e @ E_i, E_o <v, β x v> *)
Definition atomic_triple
(α: A → iProp Σ)
(β: A → val _ → iProp Σ)
(Ei Eo: coPset)
......@@ -20,14 +19,32 @@ Section atomic.
(∀ v, β x v ={Ei, Eo}=★ Q x v))
) -★ {{ P }} e @ ⊤ {{ v, (∃ x: A, Q x v) }})%I.
Arguments atomic_triple {_} _ _ _ _ _.
(* Weakest-pre version of the above one. Also weaker in some sense *)
Definition atomic_triple_wp
(α: A → iProp Σ)
(β: A → val _ → iProp Σ)
(Ei Eo: coPset)
(e: expr _) : iProp Σ :=
(∀ P Q, (P ={Eo, Ei}=> ∃ x,
α x ★
((α x ={Ei, Eo}=★ P) ∧
(∀ v, β x v ={Ei, Eo}=★ Q x v))
) -★ P -★ WP e @ ⊤ {{ v, (∃ x, Q x v) }})%I.
Lemma atomic_triple_weaken α β Ei Eo e:
atomic_triple α β Ei Eo e ⊢ atomic_triple_wp α β Ei Eo e.
Proof.
iIntros "H". iIntros (P Q) "Hvs Hp".
by iApply ("H" $! P Q with "Hvs").
Qed.
Arguments atomic_triple {_} _ _ _ _.
End atomic.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import invariants tactics.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang Require Export lang proofmode notation.
From iris.proofmode Require Import invariants.
Section demo.
Section incr.
Context `{!heapG Σ} (N : namespace).
Definition incr: val :=
......@@ -74,7 +91,7 @@ Section demo.
iVs ("Hvs'" with "[Hl]") as "HP"; first by iFrame.
iVsIntro. wp_if. by iApply "IH".
Qed.
End demo.
End incr.
From iris.heap_lang.lib Require Import par.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment