Commit d6e6d71e by Ralf Jung

### Bring back wp_bindi

`I know we don't use it.  Stating theorems also serves to document things, and IMHO this one is informative.  It also costs us nothing.`
parent f400f576
 ... @@ -148,6 +148,7 @@ Section heap. ... @@ -148,6 +148,7 @@ Section heap. Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed. Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed. (** Weakest precondition *) (** Weakest precondition *) (* FIXME: try to reduce usage of wp_pvs. We're losing view shifts here. *) Lemma wp_alloc N E e v Φ : Lemma wp_alloc N E e v Φ : to_val e = Some v → nclose N ⊆ E → to_val e = Some v → nclose N ⊆ E → heap_ctx N ★ ▷ (∀ l, l ↦ v ={E}=★ Φ (LitV (LitLoc l))) ⊢ WP Alloc e @ E {{ Φ }}. heap_ctx N ★ ▷ (∀ l, l ↦ v ={E}=★ Φ (LitV (LitLoc l))) ⊢ WP Alloc e @ E {{ Φ }}. ... ...
 ... @@ -17,6 +17,11 @@ Lemma wp_bind {E e} K Φ : ... @@ -17,6 +17,11 @@ 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 → ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!