Commit 9646293e authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

A specific constructor for injecting values in expressions

We add a specific constructor to the type of expressions for injecting
values in expressions.

The advantage are :
- Values can be assumed to be always closed when performing
  substitutions (even though they could contain free variables, but it
  turns out it does not cause any problem in the proofs in
  practice). This means that we no longer need the `Closed` typeclass
  and everything that comes with it (all the reflection-based machinery
  contained in tactics.v is no longer necessary). I have not measured
  anything, but I guess this would have a significant performance
  impact.

- There is only one constructor for values. As a result, the AsVal and
  IntoVal typeclasses are no longer necessary: an expression which is
  a value will always unify with `Val _`, and therefore lemmas can be
  stated using this constructor.

Of course, this means that there are two ways of writing such a thing
as "The pair of integers 1 and 2": Either by using the value
constructor applied to the pair represented as a value, or by using
the expression pair constructor. So we add reduction rules that
transform reduced pair, injection and closure expressions into values.
At first, this seems weird, because of the redundancy. But in fact,
this has some meaning, since the machine migth actually be doing
something to e.g., allocate the pair or the closure.

These additional steps of computation show up in the proofs, and some
additional wp_* tactics need to be called.
parent 1f796221
......@@ -81,6 +81,7 @@ theories/program_logic/total_lifting.v
theories/program_logic/total_ectx_lifting.v
theories/program_logic/atomic.v
theories/heap_lang/lang.v
theories/heap_lang/metatheory.v
theories/heap_lang/tactics.v
theories/heap_lang/lifting.v
theories/heap_lang/notation.v
......
......@@ -50,6 +50,18 @@
--------------------------------------∗
True
The command has indeed failed with message:
Ltac call to "wp_pure (open_constr)" failed.
Tactic failure: wp_pure: cannot find ?y in (Var "x") or
?y is not a redex.
1 subgoal
Σ : gFunctors
H : heapG Σ
============================
--------------------------------------∗
WP "x" {{ _, True }}
1 subgoal
Σ : gFunctors
......@@ -104,4 +116,4 @@
: string
The command has indeed failed with message:
Ltac call to "wp_cas_suc" failed.
Tactic failure: wp_cas_suc: cannot find 'CAS' in (#())%E.
Tactic failure: wp_cas_suc: cannot find 'CAS' in (Val #()).
......@@ -131,6 +131,10 @@ Section tests.
WP Alloc #0 {{ _, True }}%I.
Proof. wp_alloc l as "_". Show. done. Qed.
Lemma wp_nonclosed_value :
WP let: "x" := #() in (λ: "y", "x")%V #() {{ _, True }}%I.
Proof. wp_let. wp_lam. Fail wp_pure _. Show. Abort.
End tests.
Section printing_tests.
......
......@@ -82,14 +82,14 @@ Section list_reverse.
destruct xs as [|x xs]; iSimplifyEq.
- (* nil *) by wp_match.
- (* cons *) iDestruct "Hxs" as (l hd') "(% & Hx & Hxs)"; iSimplifyEq.
wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_store.
wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_pair. wp_store.
rewrite reverse_cons -assoc.
iApply ("IH" $! hd' (InjRV #l) xs (x :: ys) with "Hxs [Hx Hys]").
iExists l, acc; by iFrame.
Qed.
Lemma rev_ht hd xs :
{{ is_list hd xs }} rev hd NONE {{ w, is_list w (reverse xs) }}.
{{ is_list hd xs }} rev hd NONEV {{ w, is_list w (reverse xs) }}.
Proof.
iIntros "!# Hxs". rewrite -(right_id_L [] (++) (reverse xs)).
iApply (rev_acc_ht hd NONEV with "[Hxs]"); simpl; by iFrame.
......@@ -204,7 +204,7 @@ Section counter_proof.
Lemma newcounter_spec :
{{ True }} newcounter #() {{ v, l, v = #l C l 0 }}.
Proof.
iIntros "!# _ /=". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
iIntros "!# _ /=". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
iMod (own_alloc (Auth 0)) as (γ) "Hγ"; first done.
rewrite (auth_frag_op 0 0) //; iDestruct "Hγ" as "[Hγ Hγf]".
set (N:= nroot .@ "counter").
......@@ -242,7 +242,7 @@ Section counter_proof.
{{ C l n }} read #l {{ v, m : nat, v = #m n m C l m }}.
Proof.
iIntros "!# Hl /=". iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
rewrite /read /=. wp_let. Show. iApply wp_inv_open; last iFrame "Hinv"; auto.
rewrite /read /=. wp_lam. Show. iApply wp_inv_open; last iFrame "Hinv"; auto.
iDestruct 1 as (c) "[Hl Hγ]". wp_load. Show.
iDestruct (own_valid γ (Frag n Auth c) with "[-]") as % ?%auth_frag_valid.
{ iApply own_op. by iFrame. }
......
......@@ -23,11 +23,11 @@
"Hys" : is_list acc ys
"HΦ" : ∀ w : val, is_list w ys -∗ Φ w
--------------------------------------∗
WP match: InjL #() with
WP match: InjLV #() with
InjL <> => acc
| InjR "l" =>
let: "tmp1" := Fst ! "l" in
let: "tmp2" := Snd ! "l" in
"l" <- ("tmp1", acc);; (rev "tmp2") (InjL #())
"l" <- ("tmp1", acc);; (rev "tmp2") (InjLV #())
end [{ v, Φ v }]
......@@ -36,14 +36,14 @@ Proof.
iSimplifyEq; wp_rec; wp_let.
- Show. wp_match. by iApply "HΦ".
- iDestruct "Hxs" as (l hd' ->) "[Hx Hxs]".
wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_store.
wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_pair. wp_store.
iApply ("IH" $! hd' (SOMEV #l) (x :: ys) with "Hxs [Hx Hys]"); simpl.
{ iExists l, acc; by iFrame. }
iIntros (w). rewrite cons_middle assoc -reverse_cons. iApply "HΦ".
Qed.
Lemma rev_wp hd xs :
[[{ is_list hd xs }]] rev hd NONE [[{ w, RET w; is_list w (reverse xs) }]].
[[{ is_list hd xs }]] rev hd NONEV [[{ w, RET w; is_list w (reverse xs) }]].
Proof.
iIntros (Φ) "Hxs HΦ".
iApply (rev_acc_wp hd NONEV xs [] with "[$Hxs //]").
......
......@@ -35,7 +35,7 @@
"Hγ" : own γ (Shot m')
--------------------------------------∗
|={⊤ ∖ ↑N}=> ▷ one_shot_inv γ l
∗ WP match: InjR #m' with
∗ WP match: InjRV #m' with
InjL <> => assert: #false
| InjR "m" => assert: #m = "m"
end {{ _, True }}
......
......@@ -43,12 +43,12 @@ Lemma wp_one_shot (Φ : val → iProp Σ) :
WP one_shot_example #() {{ Φ }}.
Proof.
iIntros "Hf /=". pose proof (nroot .@ "N") as N.
rewrite -wp_fupd /one_shot_example /=. wp_seq. wp_alloc l as "Hl". wp_let.
rewrite -wp_fupd /one_shot_example /=. wp_lam. wp_inj. wp_alloc l as "Hl". wp_let.
iMod (own_alloc Pending) as (γ) "Hγ"; first done.
iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
{ iNext. iLeft. by iSplitL "Hl". }
iModIntro. iApply "Hf"; iSplit.
- iIntros (n) "!#". wp_let.
wp_closure. wp_closure. wp_pair. iModIntro. iApply "Hf"; iSplit.
- iIntros (n) "!#". wp_lam. wp_inj. wp_inj.
iInv N as ">[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]".
+ iMod (own_update with "Hγ") as "Hγ".
{ by apply cmra_update_exclusive with (y:=Shot n). }
......@@ -56,7 +56,7 @@ Proof.
iModIntro. iNext; iRight; iExists n; by iFrame.
+ wp_cas_fail. iSplitL; last eauto.
rewrite /one_shot_inv; eauto 10.
- iIntros "!# /=". wp_seq. wp_bind (! _)%E.
- iIntros "!# /=". wp_lam. wp_bind (! _)%E.
iInv N as ">Hγ".
iAssert ( v, l v ((v = NONEV own γ Pending)
n : Z, v = SOMEV #n own γ (Shot n)))%I with "[Hγ]" as "Hv".
......@@ -70,7 +70,7 @@ Proof.
+ Show. iSplit. iLeft; by iSplitL "Hl". eauto.
+ iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
iSplitL "Hinv"; first by eauto.
iModIntro. wp_let. iIntros "!#". wp_seq.
iModIntro. wp_let. wp_closure. iIntros "!#". wp_lam.
iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
{ by wp_match. }
wp_match. wp_bind (! _)%E.
......
......@@ -58,7 +58,7 @@ Lemma sum_wp `{!heapG Σ} v t :
[[{ is_tree v t }]] sum' v [[{ RET #(sum t); is_tree v t }]].
Proof.
iIntros (Φ) "Ht HΦ". rewrite /sum' /=.
wp_let. wp_alloc l as "Hl". wp_let.
wp_lam. wp_alloc l as "Hl". wp_let.
wp_apply (sum_loop_wp with "[$Hl $Ht]").
rewrite Z.add_0_r.
iIntros "[Hl Ht]". wp_seq. wp_load. by iApply "HΦ".
......
This diff is collapsed.
......@@ -9,16 +9,16 @@ Definition assert : val :=
(* just below ;; *)
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
Lemma twp_assert `{heapG Σ} E (Φ : val iProp Σ) e `{!Closed [] e} :
Lemma twp_assert `{heapG Σ} E (Φ : val iProp Σ) e :
WP e @ E [{ v, v = #true Φ #() }] - WP assert: e @ E [{ Φ }].
Proof.
iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
iIntros "HΦ". rewrite /assert. wp_closure. wp_lam. wp_lam.
wp_apply (twp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
Qed.
Lemma wp_assert `{heapG Σ} E (Φ : val iProp Σ) e `{!Closed [] e} :
Lemma wp_assert `{heapG Σ} E (Φ : val iProp Σ) e :
WP e @ E {{ v, v = #true Φ #() }} - WP assert: e @ E {{ Φ }}.
Proof.
iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
iIntros "HΦ". rewrite /assert. wp_closure. wp_lam. wp_lam.
wp_apply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
Qed.
......@@ -21,21 +21,20 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
AsFractional (mapsto l q v) (λ q, mapsto l q v) q;
mapsto_agree l q1 q2 v1 v2 :> mapsto l q1 v1 - mapsto l q2 v2 - v1 = v2;
(* -- operation specs -- *)
alloc_spec e v :
IntoVal e v {{{ True }}} alloc e {{{ l, RET #l; mapsto l 1 v }}};
alloc_spec (v : val) :
{{{ True }}} alloc v {{{ l, RET #l; mapsto l 1 v }}};
load_spec (l : loc) :
<<< (v : val) q, mapsto l q v >>> load #l @ <<< mapsto l q v, RET v >>>;
store_spec (l : loc) (e : expr) (w : val) :
IntoVal e w
<<< v, mapsto l 1 v >>> store #l e @
store_spec (l : loc) (w : val) :
<<< v, mapsto l 1 v >>> store #l w @
<<< mapsto l 1 w, RET #() >>>;
(* This spec is slightly weaker than it could be: It is sufficient for [w1]
*or* [v] to be unboxed. However, by writing it this way the [val_is_unboxed]
is outside the atomic triple, which makes it much easier to use -- and the
spec is still good enough for all our applications. *)
cas_spec (l : loc) (e1 e2 : expr) (w1 w2 : val) :
IntoVal e1 w1 IntoVal e2 w2 val_is_unboxed w1
<<< v, mapsto l 1 v >>> cas #l e1 e2 @
cas_spec (l : loc) (w1 w2 : val) :
val_is_unboxed w1
<<< v, mapsto l 1 v >>> cas #l w1 w2 @
<<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
RET #(if decide (v = w1) then true else false) >>>;
}.
......@@ -72,39 +71,38 @@ Definition primitive_cas : val :=
Section proof.
Context `{!heapG Σ}.
Lemma primitive_alloc_spec e v :
IntoVal e v {{{ True }}} primitive_alloc e {{{ l, RET #l; l v }}}.
Lemma primitive_alloc_spec (v : val) :
{{{ True }}} primitive_alloc v {{{ l, RET #l; l v }}}.
Proof.
iIntros (<- Φ) "_ HΦ". wp_let. wp_alloc l. iApply "HΦ". done.
iIntros (Φ) "_ HΦ". wp_lam. wp_alloc l. iApply "HΦ". done.
Qed.
Lemma primitive_load_spec (l : loc) :
<<< (v : val) q, l {q} v >>> primitive_load #l @
<<< l {q} v, RET v >>>.
Proof.
iIntros (Q Φ) "? AU". wp_let.
iIntros (Q Φ) "? AU". wp_lam.
iMod "AU" as (v q) "[H↦ [_ Hclose]]".
wp_load. iMod ("Hclose" with "H↦") as "HΦ". by iApply "HΦ".
Qed.
Lemma primitive_store_spec (l : loc) (e : expr) (w : val) :
IntoVal e w
<<< v, l v >>> primitive_store #l e @
Lemma primitive_store_spec (l : loc) (w : val) :
<<< v, l v >>> primitive_store #l w @
<<< l w, RET #() >>>.
Proof.
iIntros (<- Q Φ) "? AU". wp_lam. wp_let.
iIntros (Q Φ) "? AU". wp_lam. wp_let.
iMod "AU" as (v) "[H↦ [_ Hclose]]".
wp_store. iMod ("Hclose" with "H↦") as "HΦ". by iApply "HΦ".
Qed.
Lemma primitive_cas_spec (l : loc) e1 e2 (w1 w2 : val) :
IntoVal e1 w1 IntoVal e2 w2 val_is_unboxed w1
Lemma primitive_cas_spec (l : loc) (w1 w2 : val) :
val_is_unboxed w1
<<< (v : val), l v >>>
primitive_cas #l e1 e2 @
primitive_cas #l w1 w2 @
<<< if decide (v = w1) then l w2 else l v,
RET #(if decide (v = w1) then true else false) >>>.
Proof.
iIntros (<- <- ? Q Φ) "? AU". wp_lam. wp_let. wp_let.
iIntros (? Q Φ) "? AU". wp_lam. wp_let. wp_let.
iMod "AU" as (v) "[H↦ [_ Hclose]]".
destruct (decide (v = w1)) as [<-|Hv]; [wp_cas_suc|wp_cas_fail];
iMod ("Hclose" with "H↦") as "HΦ"; by iApply "HΦ".
......
......@@ -36,12 +36,11 @@ Section coinflip.
Lemma rand_spec :
{{{ True }}} rand #() {{{ (b : bool), RET #b; True }}}.
Proof.
iIntros (Φ) "_ HP".
wp_lam. wp_alloc l as "Hl". wp_lam.
iIntros (Φ) "_ HP". wp_lam. wp_alloc l as "Hl". wp_let.
iMod (inv_alloc N _ ( (b: bool), l #b)%I with "[Hl]") as "#Hinv"; first by eauto.
wp_apply wp_fork.
- iInv N as (b) ">Hl". wp_store. iModIntro. iSplitL; eauto.
- wp_lam. iInv N as (b) ">Hl". wp_load. iModIntro. iSplitL "Hl"; first by eauto.
- wp_seq. iInv N as (b) ">Hl". wp_load. iModIntro. iSplitL "Hl"; first by eauto.
iApply "HP". done.
Qed.
......
......@@ -35,7 +35,7 @@ Section mono_proof.
Lemma newcounter_mono_spec :
{{{ True }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
Proof.
iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
iMod (own_alloc ( (O:mnat) (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
{ iNext. iExists 0%nat. by iFrame. }
......@@ -71,7 +71,7 @@ Section mono_proof.
{{{ mcounter l j }}} read #l {{{ i, RET #i; j i%nat mcounter l i }}}.
Proof.
iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "[#Hinv Hγf]".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]".
rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]".
wp_load.
iDestruct (own_valid_2 with "Hγ Hγf")
as %[?%mnat_included _]%auth_valid_discrete_2.
......@@ -112,7 +112,7 @@ Section contrib_spec.
{{{ True }}} newcounter #()
{{{ γ l, RET #l; ccounter_ctx γ l ccounter γ 1 0 }}}.
Proof.
iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
iMod (own_alloc (! O%nat ! 0%nat)) as (γ) "[Hγ Hγ']"; first done.
iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
{ iNext. iExists 0%nat. by iFrame. }
......@@ -144,7 +144,7 @@ Section contrib_spec.
{{{ c, RET #c; n c%nat ccounter γ q n }}}.
Proof.
iIntros (Φ) "[#? Hγf] HΦ".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]". wp_load.
rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]". wp_load.
iDestruct (own_valid_2 with "Hγ Hγf") as % ?%frac_auth_included_total%nat_included.
iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
iApply ("HΦ" with "[-]"); rewrite /ccounter; eauto 10.
......@@ -155,7 +155,7 @@ Section contrib_spec.
{{{ n, RET #n; ccounter γ 1 n }}}.
Proof.
iIntros (Φ) "[#? Hγf] HΦ".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]". wp_load.
rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]". wp_load.
iDestruct (own_valid_2 with "Hγ Hγf") as % <-%frac_auth_agreeL.
iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
by iApply "HΦ".
......
......@@ -23,15 +23,14 @@ Section increment.
Lemma incr_spec (l: loc) :
<<< (v : Z), l #v >>> incr #l @ <<< l #(v + 1), RET #v >>>.
Proof.
iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH". wp_let.
iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH". wp_lam.
wp_apply load_spec; first by iAccu.
(* Prove the atomic update for load *)
iAuIntro. iApply (aacc_aupd_abort with "AU"); first done.
iIntros (x) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
iIntros "$ !> AU !> _".
(* Now go on *)
wp_let. wp_op. wp_bind (CAS _ _ _)%I.
wp_apply cas_spec; [done|iAccu|].
wp_let. wp_op. wp_apply cas_spec; [done|iAccu|].
(* Prove the atomic update for CAS *)
iAuIntro. iApply (aacc_aupd with "AU"); first done.
iIntros (x') "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
......@@ -57,7 +56,7 @@ Section increment.
weak_incr #l @
<<< v = v' l #(v + 1), RET #v >>>.
Proof.
iIntros "Hl". iApply wp_atomic_intro. iIntros (Φ) "AU". wp_let.
iIntros "Hl". iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
wp_apply (atomic_wp_seq $! (load_spec _) with "Hl").
iIntros "Hl". wp_let. wp_op.
wp_apply store_spec; first by iAccu.
......@@ -86,7 +85,7 @@ Section increment_client.
Lemma incr_client_safe (x: Z):
WP incr_client #x {{ _, True }}%I.
Proof using Type*.
wp_let. wp_alloc l as "Hl". wp_let.
wp_lam. wp_alloc l as "Hl". wp_let.
iMod (inv_alloc nroot _ (x':Z, l #x')%I with "[Hl]") as "#Hinv"; first eauto.
(* FIXME: I am only using persistent stuff, so I should be allowed
to move this to the persisten context even without the additional □. *)
......
......@@ -6,12 +6,12 @@ Import uPred.
Definition parN : namespace := nroot .@ "par".
Definition par : val :=
λ: "fs",
let: "handle" := spawn (Fst "fs") in
let: "v2" := Snd "fs" #() in
λ: "e1" "e2",
let: "handle" := spawn "e1" in
let: "v2" := "e2" #() in
let: "v1" := join "handle" in
("v1", "v2").
Notation "e1 ||| e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope.
Notation "e1 ||| e2" := (par (λ: <>, e1)%E (λ: <>, e2)%E) : expr_scope.
Section proof.
Local Set Default Proof Using "Type*".
......@@ -21,28 +21,26 @@ Context `{!heapG Σ, !spawnG Σ}.
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 Σ) :
IntoVal e (f1,f2)
Lemma par_spec (Ψ1 Ψ2 : val iProp Σ) (f1 f2 : val) (Φ : val iProp Σ) :
WP f1 #() {{ Ψ1 }} - WP f2 #() {{ Ψ2 }} -
( v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V) -
WP par e {{ Φ }}.
WP par f1 f2 {{ Φ }}.
Proof.
iIntros (<-) "Hf1 Hf2 HΦ".
rewrite /par /=. wp_let. wp_proj.
iIntros "Hf1 Hf2 HΦ".
rewrite /par /=. wp_lam. wp_let.
wp_apply (spawn_spec parN with "Hf1").
iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
iApply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
iIntros (l) "Hl". wp_let. wp_bind (f2 _).
wp_apply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
wp_apply (join_spec with "[$Hl]"). iIntros (w) "H1".
iSpecialize ("HΦ" with "[-]"); first by iSplitL "H1". by wp_let.
iSpecialize ("HΦ" with "[-]"); first by iSplitL "H1". wp_let. by wp_pair.
Qed.
Lemma wp_par (Ψ1 Ψ2 : val iProp Σ)
(e1 e2 : expr) `{!Closed [] e1, Closed [] e2} (Φ : val iProp Σ) :
Lemma wp_par (Ψ1 Ψ2 : val iProp Σ) (e1 e2 : expr) (Φ : val iProp Σ) :
WP e1 {{ Ψ1 }} - WP e2 {{ Ψ2 }} -
( v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V) -
WP e1 ||| e2 {{ Φ }}.
Proof.
iIntros "H1 H2 H". iApply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]").
by wp_let. by wp_let. auto.
iIntros "H1 H2 H". do 2 wp_closure.
iApply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]"); [by wp_lam..|auto].
Qed.
End proof.
......@@ -49,13 +49,13 @@ Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) :
{{{ WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}.
Proof.
iIntros (<- Φ) "Hf HΦ". rewrite /spawn /=.
wp_let. wp_alloc l as "Hl". wp_let.
wp_lam. wp_inj. wp_alloc l as "Hl". wp_let.
iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
{ iNext. iExists NONEV. iFrame; eauto. }
wp_apply (wp_fork with "[Hf]").
- iNext. wp_bind (f _). iApply (wp_wand with "Hf"); iIntros (v) "Hv".
iInv N as (v') "[Hl _]".
wp_inj. iInv N as (v') "[Hl _]".
wp_store. iSplitL; last done. iIntros "!> !>". iExists (SOMEV v). iFrame. eauto.
- wp_seq. iApply "HΦ". rewrite /join_handle. eauto.
Qed.
......
......@@ -83,7 +83,7 @@ Section proof.
Proof.
iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
iDestruct "Hlock" as (l ->) "#Hinv".
rewrite /release /=. wp_let. iInv N as (b) "[Hl _]".
rewrite /release /=. wp_lam. iInv N as (b) "[Hl _]".
wp_store. iSplitR "HΦ"; last by iApply "HΦ".
iModIntro. iNext. iExists false. by iFrame.
Qed.
......
......@@ -73,14 +73,14 @@ Section proof.
Lemma newlock_spec (R : iProp Σ) :
{{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
Proof.
iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=.
wp_seq. wp_alloc ln as "Hln". wp_alloc lo as "Hlo".
iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=. repeat wp_proj.
wp_lam. wp_alloc ln as "Hln". wp_alloc lo as "Hlo".
iMod (own_alloc ( (Excl' 0%nat, GSet ) (Excl' 0%nat, GSet ))) as (γ) "[Hγ Hγ']".
{ by rewrite -auth_both_op. }
iMod (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
{ iNext. rewrite /lock_inv.
iExists 0%nat, 0%nat. iFrame. iLeft. by iFrame. }
iModIntro. iApply ("HΦ" $! (#lo, #ln)%V γ). iExists lo, ln. eauto.
wp_pair. iModIntro. iApply ("HΦ" $! (#lo, #ln)%V γ). iExists lo, ln. eauto.
Qed.
Lemma wait_loop_spec γ lk x R :
......@@ -137,7 +137,7 @@ Section proof.
Proof.
iIntros (Φ) "(Hl & Hγ & HR) HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
iDestruct "Hγ" as (o) "Hγo".
wp_let. wp_proj. wp_bind (! _)%E.
wp_lam. wp_proj. wp_bind (! _)%E.
iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)".
wp_load.
iDestruct (own_valid_2 with "Hauth Hγo") as
......
This diff is collapsed.
From iris.heap_lang Require Export lang.
From stdpp Require Import gmap.
(* This file contains some metatheory about the heap_lang language,
which is not needed for verifying programs. *)
(* Closed expressions and values. *)
Fixpoint is_closed_expr (X : list string) (e : expr) : bool :=
match e with
| Val v => is_closed_val v
| Var x => bool_decide (x X)
| Rec f x e => is_closed_expr (f :b: x :b: X) e
| UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
is_closed_expr X e
| App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2
| ResolveProph e1 e2 =>
is_closed_expr X e1 && is_closed_expr X e2
| If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
is_closed_expr X e0 && is_closed_expr X e1 && is_closed_expr X e2
| NewProph => true
end
with is_closed_val (v : val) : bool :=
match v with
| LitV _ => true
| RecV f x e => is_closed_expr (f :b: x :b: []) e
| PairV v1 v2 => is_closed_val v1 && is_closed_val v2
| InjLV v | InjRV v => is_closed_val v
end.
Lemma is_closed_weaken X Y e : is_closed_expr X e X Y is_closed_expr Y e.
Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.
Lemma is_closed_weaken_nil X e : is_closed_expr [] e is_closed_expr X e.
Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
Lemma is_closed_subst X e x v :
is_closed_val v is_closed_expr (x :: X) e is_closed_expr X (subst x v e).
Proof.
intros Hv. revert X.
induction e=> X /= ?; destruct_and?; split_and?; simplify_option_eq;
try match goal with
| H : ¬(_ _) |- _ => apply not_and_l in H as [?%dec_stable|?%dec_stable]
end; eauto using is_closed_weaken with set_solver.
Qed.
Lemma is_closed_subst' X e x v :
is_closed_val v is_closed_expr (x :b: X) e is_closed_expr X (subst' x v e).
Proof. destruct x; eauto using is_closed_subst. Qed.
(* Substitution *)
Lemma subst_is_closed X e x es : is_closed_expr X e x X subst x es e = e.
Proof.
revert X. induction e=> X /=; rewrite ?bool_decide_spec ?andb_True=> ??;
repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
Qed.
Lemma subst_is_closed_nil e x v : is_closed_expr [] e subst x v e = e.
Proof. intros. apply subst_is_closed with []; set_solver. Qed.
Lemma subst_subst e x v v' :
subst x v (subst x v' e) = subst x v' e.
Proof.
intros. induction e; simpl; try (f_equal; by auto);
simplify_option_eq; auto using subst_is_closed_nil with f_equal.
Qed.
Lemma subst_subst' e x v v' :
subst' x v (subst' x v' e) = subst' x v' e.
Proof. destruct x; simpl; auto using subst_subst. Qed.