Commit e2a3396a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Some clean up.

parent 7c3cbd4e
...@@ -17,15 +17,10 @@ Lemma wp_bind {E e} K Φ : ...@@ -17,15 +17,10 @@ Lemma wp_bind {E e} K Φ :
WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} WP fill K e @ E {{ Φ }}. WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} WP fill K e @ E {{ Φ }}.
Proof. exact: wp_ectx_bind. Qed. Proof. exact: wp_ectx_bind. Qed.
Lemma wp_bindi {E e} Ki Φ :
WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }}
WP fill_item Ki e @ E {{ Φ }}.
Proof. exact: weakestpre.wp_bind. Qed.
(** Base axioms for core primitives of the language: Stateful reductions. *) (** Base axioms for core primitives of the language: Stateful reductions. *)
Lemma wp_alloc_pst E σ e v Φ : Lemma wp_alloc_pst E σ e v Φ :
to_val e = Some v to_val e = Some v
( ownP σ ( l, σ !! l = None ownP (<[l:=v]>σ) - Φ (LitV (LitLoc l)))) ownP σ ( l, σ !! l = None ownP (<[l:=v]>σ) - Φ (LitV (LitLoc l)))
WP Alloc e @ E {{ Φ }}. WP Alloc e @ E {{ Φ }}.
Proof. Proof.
iIntros {?} "[HP HΦ]". iIntros {?} "[HP HΦ]".
...@@ -41,7 +36,7 @@ Qed. ...@@ -41,7 +36,7 @@ Qed.
Lemma wp_load_pst E σ l v Φ : Lemma wp_load_pst E σ l v Φ :
σ !! l = Some v σ !! l = Some v
( ownP σ (ownP σ - Φ v)) WP Load (Lit (LitLoc l)) @ E {{ Φ }}. ownP σ (ownP σ - Φ v) WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Proof. Proof.
intros. rewrite -(wp_lift_atomic_det_head_step σ v σ None) ?right_id //; intros. rewrite -(wp_lift_atomic_det_head_step σ v σ None) ?right_id //;
last (by intros; inv_head_step; eauto using to_of_val); simpl; by eauto. last (by intros; inv_head_step; eauto using to_of_val); simpl; by eauto.
...@@ -49,7 +44,7 @@ Qed. ...@@ -49,7 +44,7 @@ Qed.
Lemma wp_store_pst E σ l e v v' Φ : Lemma wp_store_pst E σ l e v v' Φ :
to_val e = Some v σ !! l = Some v' to_val e = Some v σ !! l = Some v'
( ownP σ (ownP (<[l:=v]>σ) - Φ (LitV LitUnit))) ownP σ (ownP (<[l:=v]>σ) - Φ (LitV LitUnit))
WP Store (Lit (LitLoc l)) e @ E {{ Φ }}. WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Proof. Proof.
intros. rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) None) intros. rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) None)
...@@ -58,7 +53,7 @@ Qed. ...@@ -58,7 +53,7 @@ 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' Φ :
to_val e1 = Some v1 to_val e2 = Some v2 σ !! l = Some v' v' v1 to_val e1 = Some v1 to_val e2 = Some v2 σ !! l = Some v' v' v1
( ownP σ (ownP σ - Φ (LitV $ LitBool false))) ownP σ (ownP σ - Φ (LitV $ LitBool false))
WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}. WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof. Proof.
intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ None) intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ None)
...@@ -68,7 +63,7 @@ Qed. ...@@ -68,7 +63,7 @@ Qed.
Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ : Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2 σ !! l = Some v1 to_val e1 = Some v1 to_val e2 = Some v2 σ !! l = Some v1
( ownP σ (ownP (<[l:=v2]>σ) - Φ (LitV $ LitBool true))) ownP σ (ownP (<[l:=v2]>σ) - Φ (LitV $ LitBool true))
WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}. WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof. Proof.
intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool true) intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool true)
...@@ -78,7 +73,7 @@ Qed. ...@@ -78,7 +73,7 @@ Qed.
(** Base axioms for core primitives of the language: Stateless reductions *) (** Base axioms for core primitives of the language: Stateless reductions *)
Lemma wp_fork E e Φ : Lemma wp_fork E e Φ :
( Φ (LitV LitUnit) WP e {{ _, True }}) WP Fork e @ E {{ Φ }}. Φ (LitV LitUnit) WP e {{ _, True }} WP Fork e @ E {{ Φ }}.
Proof. Proof.
rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) (Some e)) //=; rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) (Some e)) //=;
last by intros; inv_head_step; eauto. last by intros; inv_head_step; eauto.
...@@ -88,8 +83,7 @@ Qed. ...@@ -88,8 +83,7 @@ Qed.
Lemma wp_rec E f x erec e1 e2 v2 Φ : Lemma wp_rec E f x erec e1 e2 v2 Φ :
e1 = Rec f x erec e1 = Rec f x erec
to_val e2 = Some v2 to_val e2 = Some v2
WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }} WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }} WP App e1 e2 @ E {{ Φ }}.
WP App e1 e2 @ E {{ Φ }}.
Proof. Proof.
intros -> ?. rewrite -(wp_lift_pure_det_head_step (App _ _) intros -> ?. rewrite -(wp_lift_pure_det_head_step (App _ _)
(subst' x e2 (subst' f (Rec f x erec) erec)) None) //= ?right_id; (subst' x e2 (subst' f (Rec f x erec) erec)) None) //= ?right_id;
......
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