Commit 6356ef03 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Merge branch 'value_constructor' into 'master'

A specific constructor for injecting values in expressions

See merge request FP/iris-coq!175
parents 1f796221 3e0931ea
......@@ -31,6 +31,13 @@ Changes in and extensions of the theory:
See `heap_lang/lib/increment.v` for an example.
* [#] heap_lang now uses right-to-left evaluation order. This makes it
significantly easier to write specifications of curried functions.
* [#] heap_lang values are now injected in heap_lang expressions via a specific
constructor of the expr inductive type. This simplifies much the tactical
infrastructure around the language. In particular, this allow us to get rid
the reflexion mechanism that was needed for proving closedness, atomicity and
"valueness" of a term. The price to pay is the addition of new
"administrative" reductions in the operational semantics of the language.
Changes in Coq:
......@@ -85,6 +92,9 @@ Changes in Coq:
changed `AsVal` to be usable for rewriting via the `[v <-]` destruct pattern.
* `wp_fork` is now written in curried form.
* `PureExec`/`wp_pure` now supports taking multiple steps at once.
* A new tactic, `wp_pures`, executes as many pure steps as possible, excluding
steps that would require unlocking subterms. Every impure wp_ tactic executes
this tactic before doing anything else.
## Iris 3.1.0 (released 2017-12-19)
......
......@@ -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,20 @@
--------------------------------------∗
True
"wp_nonclosed_value"
: string
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 +118,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 (#() #()).
......@@ -27,8 +27,8 @@ Section tests.
Lemma heap_e_spec E : WP heap_e @ E {{ v, v = #2 }}%I.
Proof.
iIntros "". rewrite /heap_e. Show.
wp_alloc l as "?". wp_let. wp_load. Show.
wp_op. wp_store. by wp_load.
wp_alloc l as "?". wp_load. Show.
wp_store. by wp_load.
Qed.
Definition heap_e2 : expr :=
......@@ -39,8 +39,8 @@ Section tests.
Lemma heap_e2_spec E : WP heap_e2 @ E [{ v, v = #2 }]%I.
Proof.
iIntros "". rewrite /heap_e2.
wp_alloc l as "Hl". Show. wp_let. wp_alloc l'. wp_let.
wp_load. wp_op. wp_store. wp_load. done.
wp_alloc l as "Hl". Show. wp_alloc l'.
wp_load. wp_store. wp_load. done.
Qed.
Definition heap_e3 : expr :=
......@@ -60,8 +60,8 @@ Section tests.
Lemma heap_e4_spec : WP heap_e4 [{ v, v = #1 }]%I.
Proof.
rewrite /heap_e4. wp_alloc l. wp_alloc l'. wp_let.
wp_alloc l''. wp_let. by repeat wp_load.
rewrite /heap_e4. wp_alloc l. wp_alloc l'.
wp_alloc l''. by repeat wp_load.
Qed.
Definition heap_e5 : expr :=
......@@ -69,8 +69,8 @@ Section tests.
Lemma heap_e5_spec E : WP heap_e5 @ E [{ v, v = #13 }]%I.
Proof.
rewrite /heap_e5. wp_alloc l. wp_alloc l'. wp_let.
wp_op. wp_load. wp_faa. do 2 wp_load. wp_op. done.
rewrite /heap_e5. wp_alloc l. wp_alloc l'.
wp_load. wp_faa. do 2 wp_load. by wp_pures.
Qed.
Definition heap_e6 : val := λ: "v", "v" = "v".
......@@ -92,8 +92,7 @@ Section tests.
Proof.
iIntros (Hn) "HΦ".
iInduction (Z.gt_wf n2 n1) as [n1' _] "IH" forall (Hn).
wp_rec. wp_let. wp_op. wp_let.
wp_op; case_bool_decide; wp_if.
wp_rec. wp_pures. case_bool_decide; wp_if.
- iApply ("IH" with "[%] [%] HΦ"); omega.
- by assert (n1' = n2 - 1) as -> by omega.
Qed.
......@@ -101,16 +100,15 @@ Section tests.
Lemma Pred_spec n E Φ : Φ #(n - 1) - WP Pred #n @ E [{ Φ }].
Proof.
iIntros "HΦ". wp_lam.
wp_op. case_bool_decide; wp_if.
- wp_op. wp_op.
wp_apply FindPred_spec; first omega.
wp_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
wp_op. case_bool_decide.
- wp_apply FindPred_spec; first omega. wp_pures.
by replace (n - 1) with (- (-n + 2 - 1)) by omega.
- wp_apply FindPred_spec; eauto with omega.
Qed.
Lemma Pred_user E :
WP let: "x" := Pred #42 in Pred "x" @ E [{ v, v = #40 }]%I.
Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
Proof. iIntros "". wp_apply Pred_spec. by wp_apply Pred_spec. Qed.
Lemma wp_apply_evar e P :
P - ( Q Φ, Q - WP e {{ Φ }}) - WP e {{ _, True }}.
......@@ -131,6 +129,11 @@ Section tests.
WP Alloc #0 {{ _, True }}%I.
Proof. wp_alloc l as "_". Show. done. Qed.
Check "wp_nonclosed_value".
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.
......@@ -183,7 +186,7 @@ Section error_tests.
Check "not_cas".
Lemma not_cas :
(WP #() {{ _, True }})%I.
(WP #() #() {{ _, True }})%I.
Proof.
Fail wp_cas_suc.
Abort.
......
......@@ -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_load. 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_load. wp_load. 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. wp_lam. wp_alloc l as "Hl".
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_pures. iModIntro. iApply "Hf"; iSplit.
- iIntros (n) "!#". wp_lam. wp_pures.
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,18 +70,17 @@ 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.
iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
{ by wp_match. }
wp_match. wp_bind (! _)%E.
iModIntro. wp_pures. iIntros "!#". wp_lam.
iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']";
subst; wp_match; [done|].
wp_bind (! _)%E.
iInv N as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]".
{ by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. }
wp_load. Show.
iDestruct (own_valid_2 with "Hγ Hγ'") as %?%agree_op_invL'; subst.
iModIntro. iSplitL "Hl".
{ iNext; iRight; by eauto. }
wp_match. iApply wp_assert.
wp_op. by case_bool_decide.
wp_apply wp_assert. wp_pures. by case_bool_decide.
Qed.
Lemma ht_one_shot (Φ : val iProp Σ) :
......@@ -92,8 +91,7 @@ Lemma ht_one_shot (Φ : val → iProp Σ) :
}}.
Proof.
iIntros "!# _". iApply wp_one_shot. iIntros (f1 f2) "[#Hf1 #Hf2]"; iSplit.
- iIntros (n) "!# _". wp_proj. iApply "Hf1".
- iIntros "!# _". wp_proj.
iApply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
- iIntros (n) "!# _". wp_apply "Hf1".
- iIntros "!# _". wp_apply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
Qed.
End proof.
......@@ -42,13 +42,11 @@ Proof.
iIntros (Φ) "[Hl Ht] HΦ".
iInduction t as [n'|tl ? tr] "IH" forall (v l n Φ); simpl; wp_rec; wp_let.
- iDestruct "Ht" as "%"; subst.
wp_match. wp_load. wp_op. wp_store.
wp_load. wp_store.
by iApply ("HΦ" with "[$Hl]").
- iDestruct "Ht" as (ll lr vl vr ->) "(Hll & Htl & Hlr & Htr)".
wp_match. wp_proj. wp_load.
wp_apply ("IH" with "Hl Htl"). iIntros "[Hl Htl]".
wp_seq. wp_proj. wp_load.
wp_apply ("IH1" with "Hl Htr"). iIntros "[Hl Htr]".
wp_load. wp_apply ("IH" with "Hl Htl"). iIntros "[Hl Htl]".
wp_load. wp_apply ("IH1" with "Hl Htr"). iIntros "[Hl Htr]".
iApply "HΦ". iSplitL "Hl".
{ by replace (sum tl + sum tr + n) with (sum tr + (sum tl + n)) by omega. }
iExists ll, lr, vl, vr. by iFrame.
......@@ -58,8 +56,8 @@ 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_apply (sum_loop_wp with "[$Hl $Ht]").
rewrite Z.add_0_r.
iIntros "[Hl Ht]". wp_seq. wp_load. by iApply "HΦ".
iIntros "[Hl Ht]". wp_load. by iApply "HΦ".
Qed.
This diff is collapsed.
......@@ -9,16 +9,18 @@ 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} :
WP e @ E [{ v, v = #true Φ #() }] - WP assert: e @ E [{ Φ }].
Lemma twp_assert `{heapG Σ} E (Φ : val iProp Σ) e :
WP e @ E [{ v, v = #true Φ #() }] -
WP assert (LamV BAnon e)%V @ E [{ Φ }].
Proof.
iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
iIntros "HΦ". 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} :
WP e @ E {{ v, v = #true Φ #() }} - WP assert: e @ E {{ Φ }}.
Lemma wp_assert `{heapG Σ} E (Φ : val iProp Σ) e :
WP e @ E {{ v, v = #true Φ #() }} -
WP assert (LamV BAnon e)%V @ E {{ Φ }}.
Proof.
iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
iIntros "HΦ". 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".
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_pures. iInv N as (b) ">Hl". wp_load. iModIntro. iSplitL "Hl"; first by eauto.
iApply "HP". done.
Qed.
......@@ -83,8 +82,8 @@ Section coinflip.
iDestruct "Hl" as (v') "Hl".
wp_store.
iMod ("Hclose" $! (val_to_bool v) with "[Hl]") as "HΦ"; first by eauto.
iModIntro. wp_seq. wp_apply rand_spec; try done.
iIntros (b') "_". wp_let.
iModIntro. wp_apply rand_spec; try done.
iIntros (b') "_".
wp_apply (wp_resolve_proph with "Hp").
iIntros (->). wp_seq. 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. }
......@@ -49,7 +49,7 @@ Section mono_proof.
iDestruct "Hl" as (γ) "[#? Hγf]".
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
wp_let. wp_op.
wp_pures.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
destruct (decide (c' = c)) as [->|].
- iDestruct (own_valid_2 with "Hγ Hγf")
......@@ -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. }
......@@ -126,7 +126,7 @@ Section contrib_spec.
iIntros (Φ) "[#? Hγf] HΦ". iLöb as "IH". wp_rec.
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
wp_let. wp_op.
wp_pures.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
destruct (decide (c' = c)) as [->|].
- iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
......@@ -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,14 +23,13 @@ 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|].
(* Prove the atomic update for CAS *)
iAuIntro. iApply (aacc_aupd with "AU"); first done.
......@@ -57,10 +56,9 @@ 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.
iIntros "Hl". wp_apply store_spec; first by iAccu.
(* Prove the atomic update for store *)
iAuIntro. iApply (aacc_aupd_commit with "AU"); first done.
iIntros (x) "H↦".
......@@ -86,7 +84,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".
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 □. *)
......@@ -97,7 +95,7 @@ Section increment_client.
(* The continuation: From after the atomic triple to the postcondition of the WP *)
done.
}
wp_apply wp_par.
wp_apply par_spec; wp_pures.
- iAssumption.
- iAssumption.
- iIntros (??) "_ !>". done.
......
......@@ -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,25 @@ 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Φ". 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 _).