Commit 4f0198fb authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Turn locations into literals.

This gets rid of the (ambiguous) notation %l, because we can declare
LitLoc as a coercion. It also shortens the code.
parent 310ee9d1
...@@ -142,7 +142,7 @@ Section heap. ...@@ -142,7 +142,7 @@ Section heap.
Lemma wp_alloc N E e v P Φ : Lemma wp_alloc N E e v P Φ :
to_val e = Some v to_val e = Some v
P heap_ctx N nclose N E P heap_ctx N nclose N E
P ( l, l v - Φ (LocV l)) P ( l, l v - Φ (LitV (LitLoc l)))
P WP Alloc e @ E {{ Φ }}. P WP Alloc e @ E {{ Φ }}.
Proof. Proof.
rewrite /heap_ctx /heap_inv=> ??? HP. rewrite /heap_ctx /heap_inv=> ??? HP.
...@@ -168,7 +168,7 @@ Section heap. ...@@ -168,7 +168,7 @@ Section heap.
Lemma wp_load N E l q v P Φ : Lemma wp_load N E l q v P Φ :
P heap_ctx N nclose N E P heap_ctx N nclose N E
P ( l {q} v (l {q} v - Φ v)) P ( l {q} v (l {q} v - Φ v))
P WP Load (Loc l) @ E {{ Φ }}. P WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Proof. Proof.
rewrite /heap_ctx /heap_inv=> ?? HPΦ. rewrite /heap_ctx /heap_inv=> ?? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) id) apply (auth_fsa' heap_inv (wp_fsa _) id)
...@@ -185,7 +185,7 @@ Section heap. ...@@ -185,7 +185,7 @@ Section heap.
to_val e = Some v to_val e = Some v
P heap_ctx N nclose N E P heap_ctx N nclose N E
P ( l v' (l v - Φ (LitV LitUnit))) P ( l v' (l v - Φ (LitV LitUnit)))
P WP Store (Loc l) e @ E {{ Φ }}. P WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Proof. Proof.
rewrite /heap_ctx /heap_inv=> ??? HPΦ. rewrite /heap_ctx /heap_inv=> ??? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v)) l)) apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v)) l))
...@@ -202,7 +202,7 @@ Section heap. ...@@ -202,7 +202,7 @@ Section heap.
to_val e1 = Some v1 to_val e2 = Some v2 v' v1 to_val e1 = Some v1 to_val e2 = Some v2 v' v1
P heap_ctx N nclose N E P heap_ctx N nclose N E
P ( l {q} v' (l {q} v' - Φ (LitV (LitBool false)))) P ( l {q} v' (l {q} v' - Φ (LitV (LitBool false))))
P WP CAS (Loc l) e1 e2 @ E {{ Φ }}. P WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof. Proof.
rewrite /heap_ctx /heap_inv=>????? HPΦ. rewrite /heap_ctx /heap_inv=>????? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) id) apply (auth_fsa' heap_inv (wp_fsa _) id)
...@@ -219,7 +219,7 @@ Section heap. ...@@ -219,7 +219,7 @@ Section heap.
to_val e1 = Some v1 to_val e2 = Some v2 to_val e1 = Some v1 to_val e2 = Some v2
P heap_ctx N nclose N E P heap_ctx N nclose N E
P ( l v1 (l v2 - Φ (LitV (LitBool true)))) P ( l v1 (l v2 - Φ (LitV (LitBool true))))
P WP CAS (Loc l) e1 e2 @ E {{ Φ }}. P WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof. Proof.
rewrite /heap_ctx /heap_inv=> ???? HPΦ. rewrite /heap_ctx /heap_inv=> ???? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v2)) l)) apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v2)) l))
......
...@@ -9,7 +9,7 @@ Open Scope Z_scope. ...@@ -9,7 +9,7 @@ Open Scope Z_scope.
Definition loc := positive. (* Really, any countable type. *) Definition loc := positive. (* Really, any countable type. *)
Inductive base_lit : Set := Inductive base_lit : Set :=
| LitInt (n : Z) | LitBool (b : bool) | LitUnit. | LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc).
Inductive un_op : Set := Inductive un_op : Set :=
| NegOp | MinusUnOp. | NegOp | MinusUnOp.
Inductive bin_op : Set := Inductive bin_op : Set :=
...@@ -80,7 +80,6 @@ Inductive expr (X : list string) := ...@@ -80,7 +80,6 @@ Inductive expr (X : list string) :=
(* Concurrency *) (* Concurrency *)
| Fork (e : expr X) | Fork (e : expr X)
(* Heap *) (* Heap *)
| Loc (l : loc)
| Alloc (e : expr X) | Alloc (e : expr X)
| Load (e : expr X) | Load (e : expr X)
| Store (e1 : expr X) (e2 : expr X) | Store (e1 : expr X) (e2 : expr X)
...@@ -102,7 +101,6 @@ Arguments InjL {_} _%E. ...@@ -102,7 +101,6 @@ Arguments InjL {_} _%E.
Arguments InjR {_} _%E. Arguments InjR {_} _%E.
Arguments Case {_} _%E _%E _%E. Arguments Case {_} _%E _%E _%E.
Arguments Fork {_} _%E. Arguments Fork {_} _%E.
Arguments Loc {_} _.
Arguments Alloc {_} _%E. Arguments Alloc {_} _%E.
Arguments Load {_} _%E. Arguments Load {_} _%E.
Arguments Store {_} _%E _%E. Arguments Store {_} _%E _%E.
...@@ -113,8 +111,7 @@ Inductive val := ...@@ -113,8 +111,7 @@ Inductive val :=
| LitV (l : base_lit) | LitV (l : base_lit)
| PairV (v1 v2 : val) | PairV (v1 v2 : val)
| InjLV (v : val) | InjLV (v : val)
| InjRV (v : val) | InjRV (v : val).
| LocV (l : loc).
Bind Scope val_scope with val. Bind Scope val_scope with val.
Delimit Scope val_scope with V. Delimit Scope val_scope with V.
...@@ -131,7 +128,6 @@ Fixpoint of_val (v : val) : expr [] := ...@@ -131,7 +128,6 @@ Fixpoint of_val (v : val) : expr [] :=
| PairV v1 v2 => Pair (of_val v1) (of_val v2) | PairV v1 v2 => Pair (of_val v1) (of_val v2)
| InjLV v => InjL (of_val v) | InjLV v => InjL (of_val v)
| InjRV v => InjR (of_val v) | InjRV v => InjR (of_val v)
| LocV l => Loc l
end. end.
Fixpoint to_val (e : expr []) : option val := Fixpoint to_val (e : expr []) : option val :=
...@@ -141,7 +137,6 @@ Fixpoint to_val (e : expr []) : option val := ...@@ -141,7 +137,6 @@ Fixpoint to_val (e : expr []) : option val :=
| Pair e1 e2 => v1 to_val e1; v2 to_val e2; Some (PairV v1 v2) | Pair e1 e2 => v1 to_val e1; v2 to_val e2; Some (PairV v1 v2)
| InjL e => InjLV <$> to_val e | InjL e => InjLV <$> to_val e
| InjR e => InjRV <$> to_val e | InjR e => InjRV <$> to_val e
| Loc l => Some (LocV l)
| _ => None | _ => None
end. end.
...@@ -217,7 +212,6 @@ Program Fixpoint wexpr {X Y} (H : X `included` Y) (e : expr X) : expr Y := ...@@ -217,7 +212,6 @@ Program Fixpoint wexpr {X Y} (H : X `included` Y) (e : expr X) : expr Y :=
| InjR e => InjR (wexpr H e) | InjR e => InjR (wexpr H e)
| Case e0 e1 e2 => Case (wexpr H e0) (wexpr H e1) (wexpr H e2) | Case e0 e1 e2 => Case (wexpr H e0) (wexpr H e1) (wexpr H e2)
| Fork e => Fork (wexpr H e) | Fork e => Fork (wexpr H e)
| Loc l => Loc l
| Alloc e => Alloc (wexpr H e) | Alloc e => Alloc (wexpr H e)
| Load e => Load (wexpr H e) | Load e => Load (wexpr H e)
| Store e1 e2 => Store (wexpr H e1) (wexpr H e2) | Store e1 e2 => Store (wexpr H e1) (wexpr H e2)
...@@ -260,7 +254,6 @@ Program Fixpoint wsubst {X Y} (x : string) (es : expr []) ...@@ -260,7 +254,6 @@ Program Fixpoint wsubst {X Y} (x : string) (es : expr [])
| Case e0 e1 e2 => | Case e0 e1 e2 =>
Case (wsubst x es H e0) (wsubst x es H e1) (wsubst x es H e2) Case (wsubst x es H e0) (wsubst x es H e1) (wsubst x es H e2)
| Fork e => Fork (wsubst x es H e) | Fork e => Fork (wsubst x es H e)
| Loc l => Loc l
| Alloc e => Alloc (wsubst x es H e) | Alloc e => Alloc (wsubst x es H e)
| Load e => Load (wsubst x es H e) | Load e => Load (wsubst x es H e)
| Store e1 e2 => Store (wsubst x es H e1) (wsubst x es H e2) | Store e1 e2 => Store (wsubst x es H e1) (wsubst x es H e2)
...@@ -322,21 +315,21 @@ Inductive head_step : expr [] → state → expr [] → state → option (expr [ ...@@ -322,21 +315,21 @@ Inductive head_step : expr [] → state → expr [] → state → option (expr [
head_step (Fork e) σ (Lit LitUnit) σ (Some e) head_step (Fork e) σ (Lit LitUnit) σ (Some e)
| AllocS e v σ l : | AllocS e v σ l :
to_val e = Some v σ !! l = None to_val e = Some v σ !! l = None
head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None head_step (Alloc e) σ (Lit $ LitLoc l) (<[l:=v]>σ) None
| LoadS l v σ : | LoadS l v σ :
σ !! l = Some v σ !! l = Some v
head_step (Load (Loc l)) σ (of_val v) σ None head_step (Load (Lit $ LitLoc l)) σ (of_val v) σ None
| StoreS l e v σ : | StoreS l e v σ :
to_val e = Some v is_Some (σ !! l) to_val e = Some v is_Some (σ !! l)
head_step (Store (Loc l) e) σ (Lit LitUnit) (<[l:=v]>σ) None head_step (Store (Lit $ LitLoc l) e) σ (Lit LitUnit) (<[l:=v]>σ) None
| CasFailS l e1 v1 e2 v2 vl σ : | CasFailS l e1 v1 e2 v2 vl σ :
to_val e1 = Some v1 to_val e2 = Some v2 to_val e1 = Some v1 to_val e2 = Some v2
σ !! l = Some vl vl v1 σ !! l = Some vl vl v1
head_step (CAS (Loc l) e1 e2) σ (Lit $ LitBool false) σ None head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool false) σ None
| CasSucS l e1 v1 e2 v2 σ : | CasSucS l e1 v1 e2 v2 σ :
to_val e1 = Some v1 to_val e2 = Some v2 to_val e1 = Some v1 to_val e2 = Some v2
σ !! l = Some v1 σ !! l = Some v1
head_step (CAS (Loc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None. head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
(** Atomic expressions *) (** Atomic expressions *)
Definition atomic (e: expr []) : bool := Definition atomic (e: expr []) : bool :=
...@@ -470,7 +463,7 @@ Qed. ...@@ -470,7 +463,7 @@ Qed.
Lemma alloc_fresh e v σ : Lemma alloc_fresh e v σ :
let l := fresh (dom _ σ) in let l := fresh (dom _ σ) in
to_val e = Some v head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None. to_val e = Some v head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) None.
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed. Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
(** Equality and other typeclass stuff *) (** Equality and other typeclass stuff *)
...@@ -497,7 +490,6 @@ Fixpoint expr_beq {X Y} (e : expr X) (e' : expr Y) : bool := ...@@ -497,7 +490,6 @@ Fixpoint expr_beq {X Y} (e : expr X) (e' : expr Y) : bool :=
expr_beq e0 e0' && expr_beq e1 e1' && expr_beq e2 e2' expr_beq e0 e0' && expr_beq e1 e1' && expr_beq e2 e2'
| Fst e, Fst e' | Snd e, Snd e' | InjL e, InjL e' | InjR e, InjR e' | | Fst e, Fst e' | Snd e, Snd e' | InjL e, InjL e' | InjR e, InjR e' |
Fork e, Fork e' | Alloc e, Alloc e' | Load e, Load e' => expr_beq e e' Fork e, Fork e' | Alloc e, Alloc e' | Load e, Load e' => expr_beq e e'
| Loc l, Loc l' => bool_decide (l = l')
| _, _ => false | _, _ => false
end. end.
Lemma expr_beq_correct {X} (e1 e2 : expr X) : expr_beq e1 e2 e1 = e2. Lemma expr_beq_correct {X} (e1 e2 : expr X) : expr_beq e1 e2 e1 = e2.
...@@ -525,7 +517,7 @@ Program Instance heap_ectxi_lang : ...@@ -525,7 +517,7 @@ Program Instance heap_ectxi_lang :
EctxiLanguage EctxiLanguage
(heap_lang.expr []) heap_lang.val heap_lang.ectx_item heap_lang.state := {| (heap_lang.expr []) heap_lang.val heap_lang.ectx_item heap_lang.state := {|
of_val := heap_lang.of_val; to_val := heap_lang.to_val; of_val := heap_lang.of_val; to_val := heap_lang.to_val;
fill_item := heap_lang.fill_item; fill_item := heap_lang.fill_item;
atomic := heap_lang.atomic; head_step := heap_lang.head_step; atomic := heap_lang.atomic; head_step := heap_lang.head_step;
|}. |}.
Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val, Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
......
...@@ -27,7 +27,7 @@ Section client. ...@@ -27,7 +27,7 @@ Section client.
Lemma worker_safe q (n : Z) (b y : loc) : Lemma worker_safe q (n : Z) (b y : loc) :
(heap_ctx heapN recv heapN N b (y_inv q y)) (heap_ctx heapN recv heapN N b (y_inv q y))
WP worker n (%b) (%y) {{ _, True }}. WP worker n #b #y {{ _, True }}.
Proof. Proof.
iIntros "[#Hh Hrecv]". wp_lam. wp_let. iIntros "[#Hh Hrecv]". wp_lam. wp_let.
wp_apply wait_spec; iFrame "Hrecv". wp_apply wait_spec; iFrame "Hrecv".
......
...@@ -95,7 +95,7 @@ Qed. ...@@ -95,7 +95,7 @@ Qed.
(** Actual proofs *) (** Actual proofs *)
Lemma newbarrier_spec (P : iProp) (Φ : val iProp) : Lemma newbarrier_spec (P : iProp) (Φ : val iProp) :
heapN N heapN N
(heap_ctx heapN l, recv l P send l P - Φ (%l)) (heap_ctx heapN l, recv l P send l P - Φ #l)
WP newbarrier #() {{ Φ }}. WP newbarrier #() {{ Φ }}.
Proof. Proof.
iIntros {HN} "[#? HΦ]". iIntros {HN} "[#? HΦ]".
...@@ -121,7 +121,7 @@ Proof. ...@@ -121,7 +121,7 @@ Proof.
Qed. Qed.
Lemma signal_spec l P (Φ : val iProp) : Lemma signal_spec l P (Φ : val iProp) :
(send l P P Φ #()) WP signal (%l) {{ Φ }}. (send l P P Φ #()) WP signal #l {{ Φ }}.
Proof. Proof.
rewrite /signal /send /barrier_ctx. rewrite /signal /send /barrier_ctx.
iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as {γ} "[#(%&Hh&Hsts) Hγ]". wp_let. iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as {γ} "[#(%&Hh&Hsts) Hγ]". wp_let.
...@@ -136,7 +136,7 @@ Proof. ...@@ -136,7 +136,7 @@ Proof.
Qed. Qed.
Lemma wait_spec l P (Φ : val iProp) : Lemma wait_spec l P (Φ : val iProp) :
(recv l P (P - Φ #())) WP wait (%l) {{ Φ }}. (recv l P (P - Φ #())) WP wait #l {{ Φ }}.
Proof. Proof.
rename P into R; rewrite /recv /barrier_ctx. rename P into R; rewrite /recv /barrier_ctx.
iIntros "[Hr HΦ]"; iDestruct "Hr" as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)". iIntros "[Hr HΦ]"; iDestruct "Hr" as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
......
...@@ -14,9 +14,9 @@ Lemma barrier_spec (heapN N : namespace) : ...@@ -14,9 +14,9 @@ Lemma barrier_spec (heapN N : namespace) :
heapN N heapN N
recv send : loc iProp -n> iProp, recv send : loc iProp -n> iProp,
( P, heap_ctx heapN {{ True }} newbarrier #() {{ v, ( P, heap_ctx heapN {{ True }} newbarrier #() {{ v,
l : loc, v = LocV l recv l P send l P }}) l : loc, v = #l recv l P send l P }})
( l P, {{ send l P P }} signal (LocV l) {{ _, True }}) ( l P, {{ send l P P }} signal #l {{ _, True }})
( l P, {{ recv l P }} wait (LocV l) {{ _, P }}) ( l P, {{ recv l P }} wait #l {{ _, P }})
( l P Q, recv l (P Q) ={N}=> recv l P recv l Q) ( l P Q, recv l (P Q) ={N}=> recv l P recv l Q)
( l P Q, (P - Q) (recv l P - recv l Q)). ( l P Q, (P - Q) (recv l P - recv l Q)).
Proof. Proof.
......
...@@ -49,7 +49,7 @@ Qed. ...@@ -49,7 +49,7 @@ Qed.
Lemma newlock_spec N (R : iProp) Φ : Lemma newlock_spec N (R : iProp) Φ :
heapN N heapN N
(heap_ctx heapN R ( l, is_lock l R - Φ (LocV l))) (heap_ctx heapN R ( l, is_lock l R - Φ #l))
WP newlock #() {{ Φ }}. WP newlock #() {{ Φ }}.
Proof. Proof.
iIntros {?} "(#Hh & HR & HΦ)". rewrite /newlock. iIntros {?} "(#Hh & HR & HΦ)". rewrite /newlock.
...@@ -61,7 +61,7 @@ Proof. ...@@ -61,7 +61,7 @@ Proof.
Qed. Qed.
Lemma acquire_spec l R (Φ : val iProp) : Lemma acquire_spec l R (Φ : val iProp) :
(is_lock l R (locked l R - R - Φ #())) WP acquire (%l) {{ Φ }}. (is_lock l R (locked l R - R - Φ #())) WP acquire #l {{ Φ }}.
Proof. Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as {N γ} "(%&#?&#?)". iIntros "[Hl HΦ]". iDestruct "Hl" as {N γ} "(%&#?&#?)".
iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E. iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E.
...@@ -75,7 +75,7 @@ Proof. ...@@ -75,7 +75,7 @@ Proof.
Qed. Qed.
Lemma release_spec R l (Φ : val iProp) : Lemma release_spec R l (Φ : val iProp) :
(locked l R R Φ #()) WP release (%l) {{ Φ }}. (locked l R R Φ #()) WP release #l {{ Φ }}.
Proof. Proof.
iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as {N γ} "(%&#?&#?&Hγ)". iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as {N γ} "(%&#?&#?&Hγ)".
rewrite /release. wp_let. rewrite /release. wp_let.
......
...@@ -53,7 +53,7 @@ Proof. solve_proper. Qed. ...@@ -53,7 +53,7 @@ Proof. solve_proper. Qed.
Lemma spawn_spec (Ψ : val iProp) e (f : val) (Φ : val iProp) : Lemma spawn_spec (Ψ : val iProp) e (f : val) (Φ : val iProp) :
to_val e = Some f to_val e = Some f
heapN N heapN N
(heap_ctx heapN WP f #() {{ Ψ }} l, join_handle l Ψ - Φ (%l)) (heap_ctx heapN WP f #() {{ Ψ }} l, join_handle l Ψ - Φ #l)
WP spawn e {{ Φ }}. WP spawn e {{ Φ }}.
Proof. Proof.
iIntros {<-%of_to_val ?} "(#Hh&Hf&HΦ)". rewrite /spawn. iIntros {<-%of_to_val ?} "(#Hh&Hf&HΦ)". rewrite /spawn.
...@@ -71,7 +71,7 @@ Proof. ...@@ -71,7 +71,7 @@ Proof.
Qed. Qed.
Lemma join_spec (Ψ : val iProp) l (Φ : val iProp) : Lemma join_spec (Ψ : val iProp) l (Φ : val iProp) :
(join_handle l Ψ v, Ψ v - Φ v) WP join (%l) {{ Φ }}. (join_handle l Ψ v, Ψ v - Φ v) WP join #l {{ Φ }}.
Proof. Proof.
rewrite /join_handle; iIntros "[[% H] Hv]"; iDestruct "H" as {γ} "(#?&Hγ&#?)". rewrite /join_handle; iIntros "[[% H] Hv]"; iDestruct "H" as {γ} "(#?&Hγ&#?)".
iLöb as "IH". wp_rec. wp_focus (! _)%E. iLöb as "IH". wp_rec. wp_focus (! _)%E.
......
...@@ -25,13 +25,13 @@ Proof. exact: weakestpre.wp_bind. Qed. ...@@ -25,13 +25,13 @@ 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]>σ) - Φ (LocV 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Φ]".
(* TODO: This works around ssreflect bug #22. *) (* TODO: This works around ssreflect bug #22. *)
set (φ (e' : expr []) σ' ef := l, set (φ (e' : expr []) σ' ef := l,
ef = None e' = Loc l σ' = <[l:=v]>σ σ !! l = None). ef = None e' = Lit (LitLoc l) σ' = <[l:=v]>σ σ !! l = None).
iApply (wp_lift_atomic_head_step (Alloc e) φ σ); try (by simpl; eauto); iApply (wp_lift_atomic_head_step (Alloc e) φ σ); try (by simpl; eauto);
[by intros; subst φ; inv_head_step; eauto 8|]. [by intros; subst φ; inv_head_step; eauto 8|].
iFrame "HP". iNext. iIntros {v2 σ2 ef} "[% HP]". iFrame "HP". iNext. iIntros {v2 σ2 ef} "[% HP]".
...@@ -42,7 +42,7 @@ Qed. ...@@ -42,7 +42,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 (Loc 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.
...@@ -51,7 +51,7 @@ Qed. ...@@ -51,7 +51,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 (Loc 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)
?right_id //; last (by intros; inv_head_step; eauto); simpl; by eauto. ?right_id //; last (by intros; inv_head_step; eauto); simpl; by eauto.
...@@ -60,7 +60,7 @@ Qed. ...@@ -60,7 +60,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 (Loc 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)
?right_id //; last (by intros; inv_head_step; eauto); ?right_id //; last (by intros; inv_head_step; eauto);
...@@ -70,7 +70,7 @@ Qed. ...@@ -70,7 +70,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 (Loc 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)
(<[l:=v2]>σ) None) ?right_id //; last (by intros; inv_head_step; eauto); (<[l:=v2]>σ) None) ?right_id //; last (by intros; inv_head_step; eauto);
......
...@@ -19,20 +19,20 @@ Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q)) ...@@ -19,20 +19,20 @@ Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q))
Coercion LitInt : Z >-> base_lit. Coercion LitInt : Z >-> base_lit.
Coercion LitBool : bool >-> base_lit. Coercion LitBool : bool >-> base_lit.
Coercion LitLoc : loc >-> base_lit.
Coercion App : expr >-> Funclass. Coercion App : expr >-> Funclass.
Coercion of_val : val >-> expr. Coercion of_val : val >-> expr.
Coercion BNamed : string >-> binder. Coercion BNamed : string >-> binder.
Notation "<>" := BAnon : binder_scope. Notation "<>" := BAnon : binder_scope.
(* No scope for the values, does not conflict and scope is often not inferred properly. *) (* No scope for the values, does not conflict and scope is often not inferred
properly. *)
Notation "# l" := (LitV l%Z%V) (at level 8, format "# l"). Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
Notation "% l" := (LocV l) (at level 8, format "% l").
Notation "# l" := (LitV l%Z%V) (at level 8, format "# l") : val_scope.
Notation "% l" := (LocV l) (at level 8, format "% l") : val_scope.
Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : expr_scope. Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : expr_scope.
Notation "% l" := (Loc l) (at level 8, format "% l") : expr_scope.
Check of_val'.
Notation "' x" := (Var x) (at level 8, format "' x") : expr_scope. Notation "' x" := (Var x) (at level 8, format "' x") : expr_scope.
Notation "^ v" := (of_val' v%V) (at level 8, format "^ v") : expr_scope. Notation "^ v" := (of_val' v%V) (at level 8, format "^ v") : expr_scope.
......