Commit 7c354ddb authored by Ralf Jung's avatar Ralf Jung

change some lfiting lemmas to make it clear why they are called 'atomic'

parent 0dbb9032
Pipeline #330 passed with stage
...@@ -208,13 +208,13 @@ The following rules can be derived for Hoare triples. ...@@ -208,13 +208,13 @@ The following rules can be derived for Hoare triples.
We can derive some specialized forms of the lifting axioms for the operational semantics. We can derive some specialized forms of the lifting axioms for the operational semantics.
\begin{mathparpagebreakable} \begin{mathparpagebreakable}
\infer[wp-lift-atomic-step] \infer[wp-lift-atomic-step]
{\toval(\expr_1) = \bot \and {\atomic(\expr_1) \and
\red(\expr_1, \state_1) \and \red(\expr_1, \state_1) \and
\All \expr_2, \state_2, \expr_f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \Exists\val_2. \toval(\expr_2) = \val_2 \land \pred(\val_2,\state_2,\expr_f)} \All \expr_2, \state_2, \expr_f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \pred(\expr_2,\state_2,\expr_f)}
{\later\ownPhys{\state_1} * \later\All \val, \state_2, \expr_f. \pred(\val, \state_2, \expr_f) \land \ownPhys{\state_2} \wand \prop * \wpre{\expr_f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\val.\prop}} {\later\ownPhys{\state_1} * \later\All \val_2, \state_2, \expr_f. \pred(\ofval(\val), \state_2, \expr_f) \land \ownPhys{\state_2} \wand \prop[\val_2/\var] * \wpre{\expr_f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
\infer[wp-lift-atomic-det-step] \infer[wp-lift-atomic-det-step]
{\toval(\expr_1) = \bot \and {\atomic(\expr_1) \and
\red(\expr_1, \state_1) \and \red(\expr_1, \state_1) \and
\All \expr'_2, \state'_2, \expr_f'. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \state_2 = \state_2' \land \toval(\expr_2') = \val_2 \land \expr_f = \expr_f'} \All \expr'_2, \state'_2, \expr_f'. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \state_2 = \state_2' \land \toval(\expr_2') = \val_2 \land \expr_f = \expr_f'}
{\later\ownPhys{\state_1} * \later(\ownPhys{\state_2} \wand \prop[\val_2/\var] * \wpre{\expr_f}[\top]{\Ret\any.\TRUE}) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} {\later\ownPhys{\state_1} * \later(\ownPhys{\state_2} \wand \prop[\val_2/\var] * \wpre{\expr_f}[\top]{\Ret\any.\TRUE}) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
......
...@@ -447,7 +447,7 @@ Proof. ...@@ -447,7 +447,7 @@ Proof.
end; auto with f_equal. end; auto with f_equal.
Qed. Qed.
Instance: Inj (=) (=) of_val. Instance of_val_inj : Inj (=) (=) of_val.
Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed. Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki). Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
......
...@@ -25,16 +25,18 @@ Lemma wp_alloc_pst E σ e v Φ : ...@@ -25,16 +25,18 @@ Lemma wp_alloc_pst E σ e v Φ :
WP Alloc e @ E {{ Φ }}. WP Alloc e @ E {{ Φ }}.
Proof. Proof.
(* TODO RJ: This works around ssreflect bug #22. *) (* TODO RJ: This works around ssreflect bug #22. *)
intros. set (φ v' σ' ef := l, intros. set (φ (e' : expr []) σ' ef := l,
ef = None v' = LocV l σ' = <[l:=v]>σ σ !! l = None). ef = None e' = Loc l σ' = <[l:=v]>σ σ !! l = None).
rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ; rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ;
last by intros; inv_step; eauto 8. last (by intros; inv_step; eauto 8); last (by simpl; eauto).
apply sep_mono, later_mono; first done. apply sep_mono, later_mono; first done.
apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef. apply forall_intro=>v2; apply forall_intro=>σ2; apply forall_intro=>ef.
apply wand_intro_l. apply wand_intro_l.
rewrite always_and_sep_l -assoc -always_and_sep_l. rewrite always_and_sep_l -assoc -always_and_sep_l.
apply const_elim_l=>-[l [-> [-> [-> ?]]]]. apply const_elim_l=>-[l [-> [Hl [-> ?]]]].
by rewrite (forall_elim l) right_id const_equiv // left_id wand_elim_r. rewrite (forall_elim l) right_id const_equiv // left_id wand_elim_r.
rewrite -(of_to_val (Loc l) (LocV l)) // in Hl. apply of_val_inj in Hl.
by subst.
Qed. Qed.
Lemma wp_load_pst E σ l v Φ : Lemma wp_load_pst E σ l v Φ :
...@@ -42,7 +44,7 @@ Lemma wp_load_pst E σ l v Φ : ...@@ -42,7 +44,7 @@ Lemma wp_load_pst E σ l v Φ :
( ownP σ (ownP σ - Φ v)) WP Load (Loc l) @ E {{ Φ }}. ( ownP σ (ownP σ - Φ v)) WP Load (Loc l) @ E {{ Φ }}.
Proof. Proof.
intros. rewrite -(wp_lift_atomic_det_step σ v σ None) ?right_id //; intros. rewrite -(wp_lift_atomic_det_step σ v σ None) ?right_id //;
last by intros; inv_step; eauto using to_of_val. last (by intros; inv_step; eauto using to_of_val); simpl; by eauto.
Qed. Qed.
Lemma wp_store_pst E σ l e v v' Φ : Lemma wp_store_pst E σ l e v v' Φ :
...@@ -51,7 +53,7 @@ Lemma wp_store_pst E σ l e v v' Φ : ...@@ -51,7 +53,7 @@ Lemma wp_store_pst E σ l e v v' Φ :
WP Store (Loc l) e @ E {{ Φ }}. WP Store (Loc l) e @ E {{ Φ }}.
Proof. Proof.
intros. rewrite -(wp_lift_atomic_det_step σ (LitV LitUnit) (<[l:=v]>σ) None) intros. rewrite -(wp_lift_atomic_det_step σ (LitV LitUnit) (<[l:=v]>σ) None)
?right_id //; last by intros; inv_step; eauto. ?right_id //; last (by intros; inv_step; eauto); simpl; by eauto.
Qed. Qed.
Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ : Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ :
...@@ -60,7 +62,8 @@ Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ : ...@@ -60,7 +62,8 @@ Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ :
WP CAS (Loc l) e1 e2 @ E {{ Φ }}. WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
Proof. Proof.
intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool false) σ None) intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool false) σ None)
?right_id //; last by intros; inv_step; eauto. ?right_id //; last (by intros; inv_step; eauto);
simpl; split_and?; by eauto.
Qed. Qed.
Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ : Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ :
...@@ -69,7 +72,8 @@ Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ : ...@@ -69,7 +72,8 @@ Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ :
WP CAS (Loc l) e1 e2 @ E {{ Φ }}. WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
Proof. Proof.
intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool true) intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool true)
(<[l:=v2]>σ) None) ?right_id //; last by intros; inv_step; eauto. (<[l:=v2]>σ) None) ?right_id //; last (by intros; inv_step; eauto);
simpl; split_and?; by eauto.
Qed. Qed.
(** Base axioms for core primitives of the language: Stateless reductions *) (** Base axioms for core primitives of the language: Stateless reductions *)
......
...@@ -61,40 +61,42 @@ Qed. ...@@ -61,40 +61,42 @@ Qed.
Import uPred. Import uPred.
Lemma wp_lift_atomic_step {E Φ} e1 Lemma wp_lift_atomic_step {E Φ} e1
(φ : val Λ state Λ option (expr Λ) Prop) σ1 : (φ : expr Λ state Λ option (expr Λ) Prop) σ1 :
to_val e1 = None atomic e1
reducible e1 σ1 reducible e1 σ1
( e2 σ2 ef, ( e2 σ2 ef,
prim_step e1 σ1 e2 σ2 ef v2, to_val e2 = Some v2 φ v2 σ2 ef) prim_step e1 σ1 e2 σ2 ef φ e2 σ2 ef)
( ownP σ1 v2 σ2 ef, φ v2 σ2 ef ownP σ2 - Φ v2 wp_fork ef) ( ownP σ1 v2 σ2 ef, φ (of_val v2) σ2 ef ownP σ2 - Φ v2 wp_fork ef)
WP e1 @ E {{ Φ }}. WP e1 @ E {{ Φ }}.
Proof. Proof.
intros. rewrite -(wp_lift_step E E (λ e2 σ2 ef, v2, intros. rewrite -(wp_lift_step E E (λ e2 σ2 ef,
to_val e2 = Some v2 φ v2 σ2 ef) _ e1 σ1) //; []. is_Some (to_val e2) φ e2 σ2 ef) _ e1 σ1) //;
try by (eauto using atomic_not_val, atomic_step).
rewrite -pvs_intro. apply sep_mono, later_mono; first done. rewrite -pvs_intro. apply sep_mono, later_mono; first done.
apply forall_intro=>e2'; apply forall_intro=>σ2'. apply forall_intro=>e2'; apply forall_intro=>σ2'.
apply forall_intro=>ef; apply wand_intro_l. apply forall_intro=>ef; apply wand_intro_l.
rewrite always_and_sep_l -assoc -always_and_sep_l. rewrite always_and_sep_l -assoc -always_and_sep_l.
apply const_elim_l=>-[v2' [Hv ?]] /=. apply const_elim_l=>-[[v2 Hv] ?] /=.
rewrite -pvs_intro. rewrite -pvs_intro.
rewrite (forall_elim v2') (forall_elim σ2') (forall_elim ef) const_equiv //. rewrite (forall_elim v2) (forall_elim σ2') (forall_elim ef) const_equiv //.
by rewrite left_id wand_elim_r -(wp_value _ _ e2' v2'). rewrite left_id wand_elim_r -(wp_value _ _ e2' v2) //.
by erewrite of_to_val.
Qed. Qed.
Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 ef : Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 ef :
to_val e1 = None atomic e1
reducible e1 σ1 reducible e1 σ1
( e2' σ2' ef', prim_step e1 σ1 e2' σ2' ef' ( e2' σ2' ef', prim_step e1 σ1 e2' σ2' ef'
σ2 = σ2' to_val e2' = Some v2 ef = ef') σ2 = σ2' to_val e2' = Some v2 ef = ef')
( ownP σ1 (ownP σ2 - Φ v2 wp_fork ef)) WP e1 @ E {{ Φ }}. ( ownP σ1 (ownP σ2 - Φ v2 wp_fork ef)) WP e1 @ E {{ Φ }}.
Proof. Proof.
intros. rewrite -(wp_lift_atomic_step _ (λ v2' σ2' ef', intros. rewrite -(wp_lift_atomic_step _ (λ e2' σ2' ef',
σ2 = σ2' v2 = v2' ef = ef') σ1) //; last naive_solver. σ2 = σ2' to_val e2' = Some v2 ef = ef') σ1) //.
apply sep_mono, later_mono; first done. apply sep_mono, later_mono; first done.
apply forall_intro=>e2'; apply forall_intro=>σ2'; apply forall_intro=>ef'. apply forall_intro=>e2'; apply forall_intro=>σ2'; apply forall_intro=>ef'.
apply wand_intro_l. apply wand_intro_l.
rewrite always_and_sep_l -assoc -always_and_sep_l. rewrite always_and_sep_l -assoc -always_and_sep_l to_of_val.
apply const_elim_l=>-[-> [-> ->]] /=. by rewrite wand_elim_r. apply const_elim_l=>-[-> [[->] ->]] /=. by rewrite wand_elim_r.
Qed. Qed.
Lemma wp_lift_pure_det_step {E Φ} e1 e2 ef : Lemma wp_lift_pure_det_step {E Φ} e1 e2 ef :
......
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