From 7c354ddb851b7f148a90fcb9e77f5449f092004e Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sat, 12 Mar 2016 11:32:49 +0100 Subject: [PATCH] change some lfiting lemmas to make it clear why they are called 'atomic' --- docs/derived.tex | 8 ++++---- heap_lang/lang.v | 2 +- heap_lang/lifting.v | 24 ++++++++++++++---------- program_logic/lifting.v | 30 ++++++++++++++++-------------- 4 files changed, 35 insertions(+), 29 deletions(-) diff --git a/docs/derived.tex b/docs/derived.tex index ffb5e05e..2df76084 100644 --- a/docs/derived.tex +++ b/docs/derived.tex @@ -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. \begin{mathparpagebreakable} \infer[wp-lift-atomic-step] - {\toval(\expr_1) = \bot \and + {\atomic(\expr_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)} - {\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}} + \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_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] - {\toval(\expr_1) = \bot \and + {\atomic(\expr_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'} {\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}} diff --git a/heap_lang/lang.v b/heap_lang/lang.v index 3d63e057..b8af3555 100644 --- a/heap_lang/lang.v +++ b/heap_lang/lang.v @@ -447,7 +447,7 @@ Proof. end; auto with f_equal. 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. Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki). diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v index 4cbc79cd..c95e71f2 100644 --- a/heap_lang/lifting.v +++ b/heap_lang/lifting.v @@ -25,16 +25,18 @@ Lemma wp_alloc_pst E σ e v Φ : ⊢ WP Alloc e @ E {{ Φ }}. Proof. (* TODO RJ: This works around ssreflect bug #22. *) - intros. set (φ v' σ' ef := ∃ l, - ef = None ∧ v' = LocV l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None). + intros. set (φ (e' : expr []) σ' ef := ∃ l, + ef = None ∧ e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None). 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 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. rewrite always_and_sep_l -assoc -always_and_sep_l. - apply const_elim_l=>-[l [-> [-> [-> ?]]]]. - by rewrite (forall_elim l) right_id const_equiv // left_id wand_elim_r. + apply const_elim_l=>-[l [-> [Hl [-> ?]]]]. + 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. 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 {{ Φ }}. Proof. 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. 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 {{ Φ }}. Proof. 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. 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 {{ Φ }}. Proof. 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. 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 {{ Φ }}. Proof. 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. (** Base axioms for core primitives of the language: Stateless reductions *) diff --git a/program_logic/lifting.v b/program_logic/lifting.v index e50e2513..edade4d9 100644 --- a/program_logic/lifting.v +++ b/program_logic/lifting.v @@ -61,40 +61,42 @@ Qed. Import uPred. Lemma wp_lift_atomic_step {E Φ} e1 - (φ : val Λ → state Λ → option (expr Λ) → Prop) σ1 : - to_val e1 = None → + (φ : expr Λ → state Λ → option (expr Λ) → Prop) σ1 : + atomic e1 → reducible e1 σ1 → (∀ e2 σ2 ef, - prim_step e1 σ1 e2 σ2 ef → ∃ v2, to_val e2 = Some v2 ∧ φ v2 σ2 ef) → - (▷ ownP σ1 ★ ▷ ∀ v2 σ2 ef, ■ φ v2 σ2 ef ∧ ownP σ2 -★ Φ v2 ★ wp_fork ef) + prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) → + (▷ ownP σ1 ★ ▷ ∀ v2 σ2 ef, ■ φ (of_val v2) σ2 ef ∧ ownP σ2 -★ Φ v2 ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}. Proof. - intros. rewrite -(wp_lift_step E E (λ e2 σ2 ef, ∃ v2, - to_val e2 = Some v2 ∧ φ v2 σ2 ef) _ e1 σ1) //; []. + intros. rewrite -(wp_lift_step E E (λ e2 σ2 ef, + 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. apply forall_intro=>e2'; apply forall_intro=>σ2'. apply forall_intro=>ef; apply wand_intro_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 (forall_elim v2') (forall_elim σ2') (forall_elim ef) const_equiv //. - by rewrite left_id wand_elim_r -(wp_value _ _ e2' v2'). + rewrite (forall_elim v2) (forall_elim σ2') (forall_elim ef) const_equiv //. + rewrite left_id wand_elim_r -(wp_value _ _ e2' v2) //. + by erewrite of_to_val. Qed. Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 ef : - to_val e1 = None → + atomic e1 → reducible e1 σ1 → (∀ e2' σ2' ef', prim_step e1 σ1 e2' σ2' ef' → σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') → (▷ ownP σ1 ★ ▷ (ownP σ2 -★ Φ v2 ★ wp_fork ef)) ⊢ WP e1 @ E {{ Φ }}. Proof. - intros. rewrite -(wp_lift_atomic_step _ (λ v2' σ2' ef', - σ2 = σ2' ∧ v2 = v2' ∧ ef = ef') σ1) //; last naive_solver. + intros. rewrite -(wp_lift_atomic_step _ (λ e2' σ2' ef', + σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') σ1) //. apply sep_mono, later_mono; first done. apply forall_intro=>e2'; apply forall_intro=>σ2'; apply forall_intro=>ef'. apply wand_intro_l. - rewrite always_and_sep_l -assoc -always_and_sep_l. - apply const_elim_l=>-[-> [-> ->]] /=. by rewrite wand_elim_r. + rewrite always_and_sep_l -assoc -always_and_sep_l to_of_val. + apply const_elim_l=>-[-> [[->] ->]] /=. by rewrite wand_elim_r. Qed. Lemma wp_lift_pure_det_step {E Φ} e1 e2 ef : -- GitLab