Commit 2709c37e authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Change order of premises in heap.v to instantiate evars earlier.

parent 67102cc5
...@@ -109,12 +109,12 @@ Section heap. ...@@ -109,12 +109,12 @@ Section heap.
(** Weakest precondition *) (** Weakest precondition *)
Lemma wp_alloc N E e v P Φ : Lemma wp_alloc N E e v P Φ :
to_val e = Some v nclose N E to_val e = Some v
P heap_ctx N P heap_ctx N nclose N E
P ( l, l v - Φ (LocV l)) P ( l, l v - Φ (LocV l))
P || Alloc e @ E {{ Φ }}. P || Alloc e @ E {{ Φ }}.
Proof. Proof.
rewrite /heap_ctx /heap_inv heap_mapsto_eq=> ?? Hctx HP. rewrite /heap_ctx /heap_inv heap_mapsto_eq=> ??? HP.
trans (|={E}=> auth_own heap_name P)%I. trans (|={E}=> auth_own heap_name P)%I.
{ by rewrite -pvs_frame_r -(auth_empty _ E) left_id. } { by rewrite -pvs_frame_r -(auth_empty _ E) left_id. }
apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e))) apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e)))
...@@ -135,12 +135,11 @@ Section heap. ...@@ -135,12 +135,11 @@ Section heap.
Qed. Qed.
Lemma wp_load N E l v P Φ : Lemma wp_load N E l v P Φ :
nclose N E P heap_ctx N nclose N E
P heap_ctx N
P ( l v (l v - Φ v)) P ( l v (l v - Φ v))
P || Load (Loc l) @ E {{ Φ }}. P || Load (Loc l) @ E {{ Φ }}.
Proof. Proof.
rewrite /heap_ctx /heap_inv heap_mapsto_eq=>HN ? HPΦ. rewrite /heap_ctx /heap_inv heap_mapsto_eq=> ?? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) id) apply (auth_fsa' heap_inv (wp_fsa _) id)
with N heap_name {[ l := Excl v ]}; simpl; eauto with I. with N heap_name {[ l := Excl v ]}; simpl; eauto with I.
rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l. rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
...@@ -153,12 +152,12 @@ Section heap. ...@@ -153,12 +152,12 @@ Section heap.
Qed. Qed.
Lemma wp_store N E l v' e v P Φ : Lemma wp_store N E l v' e v P Φ :
to_val e = Some v nclose N E to_val e = Some v
P heap_ctx N P heap_ctx N nclose N E
P ( l v' (l v - Φ (LitV LitUnit))) P ( l v' (l v - Φ (LitV LitUnit)))
P || Store (Loc l) e @ E {{ Φ }}. P || Store (Loc l) e @ E {{ Φ }}.
Proof. Proof.
rewrite /heap_ctx /heap_inv heap_mapsto_eq=>? HN ? HPΦ. rewrite /heap_ctx /heap_inv heap_mapsto_eq=> ??? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v) l)) apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v) l))
with N heap_name {[ l := Excl v' ]}; simpl; eauto with I. with N heap_name {[ l := Excl v' ]}; simpl; eauto with I.
rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l. rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
...@@ -173,12 +172,11 @@ Section heap. ...@@ -173,12 +172,11 @@ Section heap.
Lemma wp_cas_fail N E l v' e1 v1 e2 v2 P Φ : Lemma wp_cas_fail N E l v' e1 v1 e2 v2 P Φ :
to_val e1 = Some v1 to_val e2 = Some v2 v' v1 to_val e1 = Some v1 to_val e2 = Some v2 v' v1
nclose N E P heap_ctx N nclose N E
P heap_ctx N
P ( l v' (l v' - Φ (LitV (LitBool false)))) P ( l v' (l v' - Φ (LitV (LitBool false))))
P || Cas (Loc l) e1 e2 @ E {{ Φ }}. P || Cas (Loc l) e1 e2 @ E {{ Φ }}.
Proof. Proof.
rewrite /heap_ctx /heap_inv heap_mapsto_eq=>??? HN ? HPΦ. rewrite /heap_ctx /heap_inv heap_mapsto_eq=>????? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) id) apply (auth_fsa' heap_inv (wp_fsa _) id)
with N heap_name {[ l := Excl v' ]}; simpl; eauto 10 with I. with N heap_name {[ l := Excl v' ]}; simpl; eauto 10 with I.
rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l. rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
...@@ -192,12 +190,11 @@ Section heap. ...@@ -192,12 +190,11 @@ Section heap.
Lemma wp_cas_suc N E l e1 v1 e2 v2 P Φ : Lemma wp_cas_suc N E l e1 v1 e2 v2 P Φ :
to_val e1 = Some v1 to_val e2 = Some v2 to_val e1 = Some v1 to_val e2 = Some v2
nclose N E P heap_ctx N nclose N E
P heap_ctx N
P ( l v1 (l v2 - Φ (LitV (LitBool true)))) P ( l v1 (l v2 - Φ (LitV (LitBool true))))
P || Cas (Loc l) e1 e2 @ E {{ Φ }}. P || Cas (Loc l) e1 e2 @ E {{ Φ }}.
Proof. Proof.
rewrite /heap_ctx /heap_inv heap_mapsto_eq=> ?? HN ? HPΦ. rewrite /heap_ctx /heap_inv heap_mapsto_eq=> ???? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v2) l)) apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v2) l))
with N heap_name {[ l := Excl v1 ]}; simpl; eauto 10 with I. with N heap_name {[ l := Excl v1 ]}; simpl; eauto 10 with I.
rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l. rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
......
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