Commit 93765638 authored by Ralf Jung's avatar Ralf Jung

remark a TODO for later

parent 795d9e57
......@@ -21,6 +21,8 @@ Lemma wp_alloc_pst E σ e v Q :
(ownP σ ( l, (σ !! l = None) ownP (<[l:=v]>σ) - Q (LocV l)))
wp E (Alloc e) Q.
Proof.
(* TODO RJ: Without the set, ssreflect rewrite doesn't work. Figure out why or
reprot a bug. *)
intros. set (φ v' σ' := l, v' = LocV l σ' = <[l:=v]>σ σ !! l = None).
rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ;
last by intros; inv_step; eauto 8.
......
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