Commit e354bede authored by Ralf Jung's avatar Ralf Jung

New notation for Texan triple postconditions: Use 'RET' as keyword to indicate the return value

This should make theme asier to parse, "{{{ v, v; l |-> v }}}" looks rather funny.
parent 8d2d3ac3
...@@ -122,7 +122,7 @@ Section heap. ...@@ -122,7 +122,7 @@ Section heap.
(** Weakest precondition *) (** Weakest precondition *)
Lemma wp_alloc E e v : Lemma wp_alloc E e v :
to_val e = Some v nclose heapN E to_val e = Some v nclose heapN E
{{{ heap_ctx }}} Alloc e @ E {{{ l; LitV (LitLoc l), l v }}}. {{{ heap_ctx }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l v }}}.
Proof. Proof.
iIntros (<-%of_to_val ? Φ) "#Hinv HΦ". rewrite /heap_ctx. iIntros (<-%of_to_val ? Φ) "#Hinv HΦ". rewrite /heap_ctx.
iMod (auth_empty heap_name) as "Ha". iMod (auth_empty heap_name) as "Ha".
...@@ -137,7 +137,7 @@ Section heap. ...@@ -137,7 +137,7 @@ Section heap.
Lemma wp_load E l q v : Lemma wp_load E l q v :
nclose heapN E nclose heapN E
{{{ heap_ctx l {q} v }}} Load (Lit (LitLoc l)) @ E {{{ heap_ctx l {q} v }}} Load (Lit (LitLoc l)) @ E
{{{; v, l {q} v }}}. {{{ RET v; l {q} v }}}.
Proof. Proof.
iIntros (? Φ) "[#Hinv >Hl] HΦ". iIntros (? Φ) "[#Hinv >Hl] HΦ".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def. rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
...@@ -150,7 +150,7 @@ Section heap. ...@@ -150,7 +150,7 @@ Section heap.
Lemma wp_store E l v' e v : Lemma wp_store E l v' e v :
to_val e = Some v nclose heapN E to_val e = Some v nclose heapN E
{{{ heap_ctx l v' }}} Store (Lit (LitLoc l)) e @ E {{{ heap_ctx l v' }}} Store (Lit (LitLoc l)) e @ E
{{{; LitV LitUnit, l v }}}. {{{ RET LitV LitUnit; l v }}}.
Proof. Proof.
iIntros (<-%of_to_val ? Φ) "[#Hinv >Hl] HΦ". iIntros (<-%of_to_val ? Φ) "[#Hinv >Hl] HΦ".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def. rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
...@@ -166,7 +166,7 @@ Section heap. ...@@ -166,7 +166,7 @@ Section heap.
Lemma wp_cas_fail E l q v' e1 v1 e2 v2 : Lemma wp_cas_fail E l q v' e1 v1 e2 v2 :
to_val e1 = Some v1 to_val e2 = Some v2 v' v1 nclose heapN E to_val e1 = Some v1 to_val e2 = Some v2 v' v1 nclose heapN E
{{{ heap_ctx l {q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E {{{ heap_ctx l {q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
{{{; LitV (LitBool false), l {q} v' }}}. {{{ RET LitV (LitBool false); l {q} v' }}}.
Proof. Proof.
iIntros (<-%of_to_val <-%of_to_val ?? Φ) "[#Hinv >Hl] HΦ". iIntros (<-%of_to_val <-%of_to_val ?? Φ) "[#Hinv >Hl] HΦ".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def. rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
...@@ -179,7 +179,7 @@ Section heap. ...@@ -179,7 +179,7 @@ Section heap.
Lemma wp_cas_suc E l e1 v1 e2 v2 : Lemma wp_cas_suc E l e1 v1 e2 v2 :
to_val e1 = Some v1 to_val e2 = Some v2 nclose heapN E to_val e1 = Some v1 to_val e2 = Some v2 nclose heapN E
{{{ heap_ctx l v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E {{{ heap_ctx l v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
{{{; LitV (LitBool true), l v2 }}}. {{{ RET LitV (LitBool true); l v2 }}}.
Proof. Proof.
iIntros (<-%of_to_val <-%of_to_val ? Φ) "[#Hinv >Hl] HΦ". iIntros (<-%of_to_val <-%of_to_val ? Φ) "[#Hinv >Hl] HΦ".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def. rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
......
...@@ -92,7 +92,7 @@ Qed. ...@@ -92,7 +92,7 @@ Qed.
(** Actual proofs *) (** Actual proofs *)
Lemma newbarrier_spec (P : iProp Σ) : Lemma newbarrier_spec (P : iProp Σ) :
heapN N heapN N
{{{ heap_ctx }}} newbarrier #() {{{ l; #l, recv l P send l P }}}. {{{ heap_ctx }}} newbarrier #() {{{ l, RET #l; recv l P send l P }}}.
Proof. Proof.
iIntros (HN Φ) "#? HΦ". iIntros (HN Φ) "#? HΦ".
rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl". rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl".
...@@ -117,7 +117,7 @@ Proof. ...@@ -117,7 +117,7 @@ Proof.
Qed. Qed.
Lemma signal_spec l P : Lemma signal_spec l P :
{{{ send l P P }}} signal #l {{{; #(), True }}}. {{{ send l P P }}} signal #l {{{ RET #(); True }}}.
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.
...@@ -133,7 +133,7 @@ Proof. ...@@ -133,7 +133,7 @@ Proof.
Qed. Qed.
Lemma wait_spec l P: Lemma wait_spec l P:
{{{ recv l P }}} wait #l {{{ ; #(), P }}}. {{{ recv l P }}} wait #l {{{ RET #(); P }}}.
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)".
......
...@@ -35,7 +35,7 @@ Section mono_proof. ...@@ -35,7 +35,7 @@ Section mono_proof.
Lemma newcounter_mono_spec (R : iProp Σ) : Lemma newcounter_mono_spec (R : iProp Σ) :
heapN N heapN N
{{{ heap_ctx }}} newcounter #() {{{ l; #l, mcounter l 0 }}}. {{{ heap_ctx }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
Proof. Proof.
iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl". iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
iMod (own_alloc ( (O:mnat) (O:mnat))) as (γ) "[Hγ Hγ']"; first done. iMod (own_alloc ( (O:mnat) (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
...@@ -45,7 +45,7 @@ Section mono_proof. ...@@ -45,7 +45,7 @@ Section mono_proof.
Qed. Qed.
Lemma inc_mono_spec l n : Lemma inc_mono_spec l n :
{{{ mcounter l n }}} inc #l {{{; #(), mcounter l (S n) }}}. {{{ mcounter l n }}} inc #l {{{ RET #(); mcounter l (S n) }}}.
Proof. Proof.
iIntros (Φ) "Hl HΦ". iLöb as "IH". wp_rec. iIntros (Φ) "Hl HΦ". iLöb as "IH". wp_rec.
iDestruct "Hl" as (γ) "(% & #? & #Hinv & Hγf)". iDestruct "Hl" as (γ) "(% & #? & #Hinv & Hγf)".
...@@ -70,7 +70,7 @@ Section mono_proof. ...@@ -70,7 +70,7 @@ Section mono_proof.
Qed. Qed.
Lemma read_mono_spec l j : Lemma read_mono_spec l j :
{{{ mcounter l j }}} read #l {{{ i; #i, (j i)%nat mcounter l i }}}. {{{ mcounter l j }}} read #l {{{ i, RET #i; (j i)%nat mcounter l i }}}.
Proof. Proof.
iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "(% & #? & #Hinv & Hγf)". iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "(% & #? & #Hinv & Hγf)".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load. rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
...@@ -112,7 +112,7 @@ Section contrib_spec. ...@@ -112,7 +112,7 @@ Section contrib_spec.
Lemma newcounter_contrib_spec (R : iProp Σ) : Lemma newcounter_contrib_spec (R : iProp Σ) :
heapN N heapN N
{{{ heap_ctx }}} newcounter #() {{{ heap_ctx }}} newcounter #()
{{{ γ l; #l, ccounter_ctx γ l ccounter γ 1 0 }}}. {{{ γ l, RET #l; ccounter_ctx γ l ccounter γ 1 0 }}}.
Proof. Proof.
iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl". iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
iMod (own_alloc ( (Some (1%Qp, O%nat)) (Some (1%Qp, 0%nat)))) iMod (own_alloc ( (Some (1%Qp, O%nat)) (Some (1%Qp, 0%nat))))
...@@ -124,7 +124,7 @@ Section contrib_spec. ...@@ -124,7 +124,7 @@ Section contrib_spec.
Lemma inc_contrib_spec γ l q n : Lemma inc_contrib_spec γ l q n :
{{{ ccounter_ctx γ l ccounter γ q n }}} inc #l {{{ ccounter_ctx γ l ccounter γ q n }}} inc #l
{{{; #(), ccounter γ q (S n) }}}. {{{ RET #(); ccounter γ q (S n) }}}.
Proof. Proof.
iIntros (Φ) "(#(%&?&?) & Hγf) HΦ". iLöb as "IH". wp_rec. iIntros (Φ) "(#(%&?&?) & Hγf) HΦ". iLöb as "IH". wp_rec.
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
...@@ -145,7 +145,7 @@ Section contrib_spec. ...@@ -145,7 +145,7 @@ Section contrib_spec.
Lemma read_contrib_spec γ l q n : Lemma read_contrib_spec γ l q n :
{{{ ccounter_ctx γ l ccounter γ q n }}} read #l {{{ ccounter_ctx γ l ccounter γ q n }}} read #l
{{{ c; #c, (n c)%nat ccounter γ q n }}}. {{{ c, RET #c; (n c)%nat ccounter γ q n }}}.
Proof. Proof.
iIntros (Φ) "(#(%&?&?) & Hγf) HΦ". iIntros (Φ) "(#(%&?&?) & Hγf) HΦ".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load. rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
...@@ -157,7 +157,7 @@ Section contrib_spec. ...@@ -157,7 +157,7 @@ Section contrib_spec.
Lemma read_contrib_spec_1 γ l n : Lemma read_contrib_spec_1 γ l n :
{{{ ccounter_ctx γ l ccounter γ 1 n }}} read #l {{{ ccounter_ctx γ l ccounter γ 1 n }}} read #l
{{{ n; #n, ccounter γ 1 n }}}. {{{ n, RET #n; ccounter γ 1 n }}}.
Proof. Proof.
iIntros (Φ) "(#(%&?&?) & Hγf) HΦ". iIntros (Φ) "(#(%&?&?) & Hγf) HΦ".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load. rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
......
...@@ -18,11 +18,11 @@ Structure lock Σ `{!heapG Σ} := Lock { ...@@ -18,11 +18,11 @@ Structure lock Σ `{!heapG Σ} := Lock {
(* -- operation specs -- *) (* -- operation specs -- *)
newlock_spec N (R : iProp Σ) : newlock_spec N (R : iProp Σ) :
heapN N heapN N
{{{ heap_ctx R }}} newlock #() {{{ lk γ; lk, is_lock N γ lk R }}}; {{{ heap_ctx R }}} newlock #() {{{ lk γ, RET lk; is_lock N γ lk R }}};
acquire_spec N γ lk R : acquire_spec N γ lk R :
{{{ is_lock N γ lk R }}} acquire lk {{{; #(), locked γ R }}}; {{{ is_lock N γ lk R }}} acquire lk {{{ RET #(); locked γ R }}};
release_spec N γ lk R : release_spec N γ lk R :
{{{ is_lock N γ lk R locked γ R }}} release lk {{{; #(), True }}} {{{ is_lock N γ lk R locked γ R }}} release lk {{{ RET #(); True }}}
}. }.
Arguments newlock {_ _} _. Arguments newlock {_ _} _.
......
...@@ -16,6 +16,10 @@ Global Opaque par. ...@@ -16,6 +16,10 @@ Global Opaque par.
Section proof. Section proof.
Context `{!heapG Σ, !spawnG Σ}. Context `{!heapG Σ, !spawnG Σ}.
(* Notice that this allows us to strip a later *after* the two Ψ have been
brought together. That is strictly stronger than first stripping a later
and then merging them, as demonstrated by [tests/joining_existentials.v].
This is why these are not Texan triples. *)
Lemma par_spec (Ψ1 Ψ2 : val iProp Σ) e (f1 f2 : val) (Φ : val iProp Σ) : Lemma par_spec (Ψ1 Ψ2 : val iProp Σ) e (f1 f2 : val) (Φ : val iProp Σ) :
to_val e = Some (f1,f2)%V to_val e = Some (f1,f2)%V
(heap_ctx WP f1 #() {{ Ψ1 }} WP f2 #() {{ Ψ2 }} (heap_ctx WP f1 #() {{ Ψ1 }} WP f2 #() {{ Ψ2 }}
......
...@@ -49,7 +49,7 @@ Proof. solve_proper. Qed. ...@@ -49,7 +49,7 @@ Proof. solve_proper. Qed.
Lemma spawn_spec (Ψ : val iProp Σ) e (f : val) : Lemma spawn_spec (Ψ : val iProp Σ) e (f : val) :
to_val e = Some f to_val e = Some f
heapN N heapN N
{{{ heap_ctx WP f #() {{ Ψ }} }}} spawn e {{{ l; #l, join_handle l Ψ }}}. {{{ heap_ctx WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}.
Proof. Proof.
iIntros (<-%of_to_val ? Φ) "(#Hh & Hf) HΦ". rewrite /spawn /=. iIntros (<-%of_to_val ? Φ) "(#Hh & Hf) HΦ". rewrite /spawn /=.
wp_let. wp_alloc l as "Hl". wp_let. wp_let. wp_alloc l as "Hl". wp_let.
...@@ -64,7 +64,7 @@ Proof. ...@@ -64,7 +64,7 @@ Proof.
Qed. Qed.
Lemma join_spec (Ψ : val iProp Σ) l : Lemma join_spec (Ψ : val iProp Σ) l :
{{{ join_handle l Ψ }}} join #l {{{ v; v, Ψ v }}}. {{{ join_handle l Ψ }}} join #l {{{ v, RET v; Ψ v }}}.
Proof. Proof.
rewrite /join_handle; iIntros (Φ) "[% H] HΦ". iDestruct "H" as (γ) "(#?&Hγ&#?)". rewrite /join_handle; iIntros (Φ) "[% H] HΦ". iDestruct "H" as (γ) "(#?&Hγ&#?)".
iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]" "Hclose". iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]" "Hclose".
......
...@@ -47,7 +47,7 @@ Section proof. ...@@ -47,7 +47,7 @@ Section proof.
Lemma newlock_spec (R : iProp Σ): Lemma newlock_spec (R : iProp Σ):
heapN N heapN N
{{{ heap_ctx R }}} newlock #() {{{ lk γ; lk, is_lock γ lk R }}}. {{{ heap_ctx R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
Proof. Proof.
iIntros (? Φ) "[#Hh HR] HΦ". rewrite -wp_fupd /newlock /=. iIntros (? Φ) "[#Hh HR] HΦ". rewrite -wp_fupd /newlock /=.
wp_seq. wp_alloc l as "Hl". wp_seq. wp_alloc l as "Hl".
...@@ -59,7 +59,7 @@ Section proof. ...@@ -59,7 +59,7 @@ Section proof.
Lemma try_acquire_spec γ lk R : Lemma try_acquire_spec γ lk R :
{{{ is_lock γ lk R }}} try_acquire lk {{{ is_lock γ lk R }}} try_acquire lk
{{{b; #b, if b is true then locked γ R else True }}}. {{{ b, RET #b; if b is true then locked γ R else True }}}.
Proof. Proof.
iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l) "(% & #? & % & #?)". subst. iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l) "(% & #? & % & #?)". subst.
wp_rec. iInv N as ([]) "[Hl HR]" "Hclose". wp_rec. iInv N as ([]) "[Hl HR]" "Hclose".
...@@ -71,7 +71,7 @@ Section proof. ...@@ -71,7 +71,7 @@ Section proof.
Qed. Qed.
Lemma acquire_spec γ lk R : Lemma acquire_spec γ lk R :
{{{ is_lock γ lk R }}} acquire lk {{{; #(), locked γ R }}}. {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ R }}}.
Proof. Proof.
iIntros (Φ) "#Hl HΦ". iLöb as "IH". wp_rec. iIntros (Φ) "#Hl HΦ". iLöb as "IH". wp_rec.
wp_apply (try_acquire_spec with "Hl"). iIntros ([]). wp_apply (try_acquire_spec with "Hl"). iIntros ([]).
...@@ -80,7 +80,7 @@ Section proof. ...@@ -80,7 +80,7 @@ Section proof.
Qed. Qed.
Lemma release_spec γ lk R : Lemma release_spec γ lk R :
{{{ is_lock γ lk R locked γ R }}} release lk {{{; #(), True }}}. {{{ is_lock γ lk R locked γ R }}} release lk {{{ RET #(); True }}}.
Proof. Proof.
iIntros (Φ) "(Hlock & Hlocked & HR) HΦ". iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
iDestruct "Hlock" as (l) "(% & #? & % & #?)". subst. iDestruct "Hlock" as (l) "(% & #? & % & #?)". subst.
......
...@@ -76,7 +76,7 @@ Section proof. ...@@ -76,7 +76,7 @@ Section proof.
Lemma newlock_spec (R : iProp Σ) : Lemma newlock_spec (R : iProp Σ) :
heapN N heapN N
{{{ heap_ctx R }}} newlock #() {{{ lk γ; lk, is_lock γ lk R }}}. {{{ heap_ctx R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
Proof. Proof.
iIntros (HN Φ) "(#Hh & HR) HΦ". rewrite -wp_fupd /newlock /=. iIntros (HN Φ) "(#Hh & HR) HΦ". rewrite -wp_fupd /newlock /=.
wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln". wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln".
...@@ -89,7 +89,7 @@ Section proof. ...@@ -89,7 +89,7 @@ Section proof.
Qed. Qed.
Lemma wait_loop_spec γ lk x R : Lemma wait_loop_spec γ lk x R :
{{{ issued γ lk x R }}} wait_loop #x lk {{{; #(), locked γ R }}}. {{{ issued γ lk x R }}} wait_loop #x lk {{{ RET #(); locked γ R }}}.
Proof. Proof.
iIntros (Φ) "Hl HΦ". iDestruct "Hl" as (lo ln) "(% & #? & % & #? & Ht)". iIntros (Φ) "Hl HΦ". iDestruct "Hl" as (lo ln) "(% & #? & % & #? & Ht)".
iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E. iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E.
...@@ -110,7 +110,7 @@ Section proof. ...@@ -110,7 +110,7 @@ Section proof.
Qed. Qed.
Lemma acquire_spec γ lk R : Lemma acquire_spec γ lk R :
{{{ is_lock γ lk R }}} acquire lk {{{; #(), locked γ R }}}. {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ R }}}.
Proof. Proof.
iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)". iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)".
iLöb as "IH". wp_rec. wp_bind (! _)%E. subst. wp_proj. iLöb as "IH". wp_rec. wp_bind (! _)%E. subst. wp_proj.
...@@ -141,7 +141,7 @@ Section proof. ...@@ -141,7 +141,7 @@ Section proof.
Qed. Qed.
Lemma release_spec γ lk R : Lemma release_spec γ lk R :
{{{ is_lock γ lk R locked γ R }}} release lk {{{; #(), True }}}. {{{ is_lock γ lk R locked γ R }}} release lk {{{ RET #(); True }}}.
Proof. Proof.
iIntros (Φ) "(Hl & Hγ & HR) HΦ". iIntros (Φ) "(Hl & Hγ & HR) HΦ".
iDestruct "Hl" as (lo ln) "(% & #? & % & #?)"; subst. iDestruct "Hl" as (lo ln) "(% & #? & % & #?)"; subst.
......
...@@ -48,7 +48,7 @@ Proof. exact: weakestpre.wp_bind. Qed. ...@@ -48,7 +48,7 @@ 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 σ v : Lemma wp_alloc_pst E σ v :
{{{ ownP σ }}} Alloc (of_val v) @ E {{{ ownP σ }}} Alloc (of_val v) @ E
{{{ l; LitV (LitLoc l), σ !! l = None ownP (<[l:=v]>σ) }}}. {{{ l, RET LitV (LitLoc l); σ !! l = None ownP (<[l:=v]>σ) }}}.
Proof. Proof.
iIntros (Φ) "HP HΦ". iIntros (Φ) "HP HΦ".
iApply (wp_lift_atomic_head_step (Alloc (of_val v)) σ); eauto. iApply (wp_lift_atomic_head_step (Alloc (of_val v)) σ); eauto.
...@@ -59,7 +59,7 @@ Qed. ...@@ -59,7 +59,7 @@ Qed.
Lemma wp_load_pst E σ l v : Lemma wp_load_pst E σ l v :
σ !! l = Some v σ !! l = Some v
{{{ ownP σ }}} Load (Lit (LitLoc l)) @ E {{{; v, ownP σ }}}. {{{ ownP σ }}} Load (Lit (LitLoc l)) @ E {{{ RET v; ownP σ }}}.
Proof. Proof.
intros ? Φ. apply (wp_lift_atomic_det_head_step' σ v σ); eauto. intros ? Φ. apply (wp_lift_atomic_det_head_step' σ v σ); eauto.
intros; inv_head_step; eauto. intros; inv_head_step; eauto.
...@@ -68,7 +68,7 @@ Qed. ...@@ -68,7 +68,7 @@ Qed.
Lemma wp_store_pst E σ l v v' : Lemma wp_store_pst E σ l v v' :
σ !! l = Some v' σ !! l = Some v'
{{{ ownP σ }}} Store (Lit (LitLoc l)) (of_val v) @ E {{{ ownP σ }}} Store (Lit (LitLoc l)) (of_val v) @ E
{{{; LitV LitUnit, ownP (<[l:=v]>σ) }}}. {{{ RET LitV LitUnit; ownP (<[l:=v]>σ) }}}.
Proof. Proof.
intros. apply (wp_lift_atomic_det_head_step' σ (LitV LitUnit) (<[l:=v]>σ)); eauto. intros. apply (wp_lift_atomic_det_head_step' σ (LitV LitUnit) (<[l:=v]>σ)); eauto.
intros; inv_head_step; eauto. intros; inv_head_step; eauto.
...@@ -77,7 +77,7 @@ Qed. ...@@ -77,7 +77,7 @@ Qed.
Lemma wp_cas_fail_pst E σ l v1 v2 v' : Lemma wp_cas_fail_pst E σ l v1 v2 v' :
σ !! l = Some v' v' v1 σ !! l = Some v' v' v1
{{{ ownP σ }}} CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{{ ownP σ }}} CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E
{{{; LitV $ LitBool false, ownP σ }}}. {{{ RET LitV $ LitBool false; ownP σ }}}.
Proof. Proof.
intros. apply (wp_lift_atomic_det_head_step' σ (LitV $ LitBool false) σ); eauto. intros. apply (wp_lift_atomic_det_head_step' σ (LitV $ LitBool false) σ); eauto.
intros; inv_head_step; eauto. intros; inv_head_step; eauto.
...@@ -86,7 +86,7 @@ Qed. ...@@ -86,7 +86,7 @@ Qed.
Lemma wp_cas_suc_pst E σ l v1 v2 : Lemma wp_cas_suc_pst E σ l v1 v2 :
σ !! l = Some v1 σ !! l = Some v1
{{{ ownP σ }}} CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{{ ownP σ }}} CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E
{{{; LitV $ LitBool true, ownP (<[l:=v2]>σ) }}}. {{{ RET LitV $ LitBool true; ownP (<[l:=v2]>σ) }}}.
Proof. Proof.
intros. apply (wp_lift_atomic_det_head_step' σ (LitV $ LitBool true) intros. apply (wp_lift_atomic_det_head_step' σ (LitV $ LitBool true)
(<[l:=v2]>σ)); eauto. (<[l:=v2]>σ)); eauto.
......
...@@ -65,7 +65,7 @@ Lemma wp_lift_atomic_det_head_step' {E e1} σ1 v2 σ2 : ...@@ -65,7 +65,7 @@ Lemma wp_lift_atomic_det_head_step' {E e1} σ1 v2 σ2 :
head_reducible e1 σ1 head_reducible e1 σ1
( e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' ( e2' σ2' efs', head_step e1 σ1 e2' σ2' efs'
σ2 = σ2' to_val e2' = Some v2 [] = efs') σ2 = σ2' to_val e2' = Some v2 [] = efs')
{{{ ownP σ1 }}} e1 @ E {{{; v2, ownP σ2 }}}. {{{ ownP σ1 }}} e1 @ E {{{ RET v2; ownP σ2 }}}.
Proof. Proof.
intros. rewrite -(wp_lift_atomic_det_head_step σ1 v2 σ2 []); [|done..]. intros. rewrite -(wp_lift_atomic_det_head_step σ1 v2 σ2 []); [|done..].
rewrite big_sepL_nil right_id. by apply uPred.wand_intro_r. rewrite big_sepL_nil right_id. by apply uPred.wand_intro_r.
......
...@@ -68,43 +68,43 @@ Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q)) ...@@ -68,43 +68,43 @@ Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q))
format "'WP' e {{ v , Q } }") : uPred_scope. format "'WP' e {{ v , Q } }") : uPred_scope.
(* Texan triples *) (* Texan triples *)
Notation "'{{{' P } } } e {{{ x .. y ; pat , Q } } }" := Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ, ( Φ,
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e {{ Φ }})%I P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e {{ Φ }})%I
(at level 20, x closed binder, y closed binder, (at level 20, x closed binder, y closed binder,
format "{{{ P } } } e {{{ x .. y ; pat , Q } } }") : uPred_scope. format "{{{ P } } } e {{{ x .. y , RET pat ; Q } } }") : uPred_scope.
Notation "'{{{' P } } } e @ E {{{ x .. y ; pat , Q } } }" := Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ, ( Φ,
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E {{ Φ }})%I P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E {{ Φ }})%I
(at level 20, x closed binder, y closed binder, (at level 20, x closed binder, y closed binder,
format "{{{ P } } } e @ E {{{ x .. y ; pat , Q } } }") : uPred_scope. format "{{{ P } } } e @ E {{{ x .. y , RET pat ; Q } } }") : uPred_scope.
Notation "'{{{' P } } } e {{{ ; pat , Q } } }" := Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
( Φ, P - (Q - Φ pat%V) - WP e {{ Φ }})%I ( Φ, P - (Q - Φ pat%V) - WP e {{ Φ }})%I
(at level 20, (at level 20,
format "{{{ P } } } e {{{ ; pat , Q } } }") : uPred_scope. format "{{{ P } } } e {{{ RET pat ; Q } } }") : uPred_scope.
Notation "'{{{' P } } } e @ E {{{ ; pat , Q } } }" := Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
( Φ, P - (Q - Φ pat%V) - WP e @ E {{ Φ }})%I ( Φ, P - (Q - Φ pat%V) - WP e @ E {{ Φ }})%I
(at level 20, (at level 20,
format "{{{ P } } } e @ E {{{ ; pat , Q } } }") : uPred_scope. format "{{{ P } } } e @ E {{{ RET pat ; Q } } }") : uPred_scope.
Notation "'{{{' P } } } e {{{ x .. y ; pat , Q } } }" := Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ : _ uPred _, ( Φ : _ uPred _,
P ( x, .. ( y, Q - Φ pat%V) .. ) - WP e {{ Φ }}) P ( x, .. ( y, Q - Φ pat%V) .. ) - WP e {{ Φ }})
(at level 20, x closed binder, y closed binder, (at level 20, x closed binder, y closed binder,
format "{{{ P } } } e {{{ x .. y ; pat , Q } } }") : C_scope. format "{{{ P } } } e {{{ x .. y , RET pat ; Q } } }") : C_scope.
Notation "'{{{' P } } } e @ E {{{ x .. y ; pat , Q } } }" := Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ : _ uPred _, ( Φ : _ uPred _,
P ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E {{ Φ }}) P ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E {{ Φ }})
(at level 20, x closed binder, y closed binder, (at level 20, x closed binder, y closed binder,
format "{{{ P } } } e @ E {{{ x .. y ; pat , Q } } }") : C_scope. format "{{{ P } } } e @ E {{{ x .. y , RET pat ; Q } } }") : C_scope.
Notation "'{{{' P } } } e {{{ ; pat , Q } } }" := Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
( Φ : _ uPred _, P (Q - Φ pat%V) - WP e {{ Φ }})