Commit a3ef214f authored by Robbert Krebbers's avatar Robbert Krebbers

Use the big op over lists in the definition of weakestpre.

This also removes the double use of the name 'wp_fork' in both
program_logic/weakestpre and heap_lang/lifting.
parent 42b08240
Pipeline #2653 passed with stage
in 8 minutes and 59 seconds
......@@ -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.
......@@ -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.
......@@ -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.
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).
......
......@@ -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 Σ.
......
Markdown is supported
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