Commit 14206553 authored by Robbert Krebbers's avatar Robbert Krebbers

Curry everything in heap_lang/lib and tests.

parent 925a9169
...@@ -9,7 +9,7 @@ Definition assert : val := ...@@ -9,7 +9,7 @@ Definition assert : val :=
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope. Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
Lemma wp_assert `{heapG Σ} E (Φ : val iProp Σ) e `{!Closed [] e} : Lemma wp_assert `{heapG Σ} E (Φ : val iProp Σ) e `{!Closed [] e} :
WP e @ E {{ v, v = #true Φ #() }} WP assert: e @ E {{ Φ }}. WP e @ E {{ v, v = #true Φ #() }} - WP assert: e @ E {{ Φ }}.
Proof. Proof.
iIntros "HΦ". rewrite /assert. wp_let. wp_seq. iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
iApply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if. iApply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
......
...@@ -73,11 +73,11 @@ Proof. solve_proper. Qed. ...@@ -73,11 +73,11 @@ Proof. solve_proper. Qed.
(** Helper lemmas *) (** Helper lemmas *)
Lemma ress_split i i1 i2 Q R1 R2 P I : Lemma ress_split i i1 i2 Q R1 R2 P I :
i I i1 I i2 I i1 i2 i I i1 I i2 I i1 i2
saved_prop_own i Q saved_prop_own i1 R1 saved_prop_own i2 R2 saved_prop_own i Q - saved_prop_own i1 R1 - saved_prop_own i2 R2 -
(Q - R1 R2) ress P I (Q - R1 R2) - ress P I -
ress P ({[i1;i2]} I {[i]}). ress P ({[i1;i2]} I {[i]}).
Proof. Proof.
iIntros (????) "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as (Ψ) "[HPΨ HΨ]". iIntros (????) "#HQ #H1 #H2 HQR"; iDestruct 1 as (Ψ) "[HPΨ HΨ]".
iDestruct (big_sepS_delete _ _ i with "HΨ") as "[#HΨi HΨ]"; first done. iDestruct (big_sepS_delete _ _ i with "HΨ") as "[#HΨi HΨ]"; first done.
iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ". iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ".
- iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by iSplit. - iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by iSplit.
...@@ -175,7 +175,7 @@ Proof. ...@@ -175,7 +175,7 @@ Proof.
{[Change i1; Change i2 ]} with "[-]") as "Hγ". {[Change i1; Change i2 ]} with "[-]") as "Hγ".
{ iSplit; first by eauto using split_step. { iSplit; first by eauto using split_step.
rewrite {2}/barrier_inv /=. iNext. iFrame "Hl". rewrite {2}/barrier_inv /=. iNext. iFrame "Hl".
iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame; auto. } by iApply (ress_split with "HQ Hi1 Hi2 HQR"). }
iAssert (sts_ownS γ (i_states i1) {[Change i1]} iAssert (sts_ownS γ (i_states i1) {[Change i1]}
sts_ownS γ (i_states i2) {[Change i2]})%I with ">[-]" as "[Hγ1 Hγ2]". sts_ownS γ (i_states i2) {[Change i2]})%I with ">[-]" as "[Hγ1 Hγ2]".
{ iApply sts_ownS_op; eauto using i_states_closed, low_states_closed. { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
...@@ -190,8 +190,7 @@ Qed. ...@@ -190,8 +190,7 @@ Qed.
Lemma recv_weaken l P1 P2 : (P1 - P2) - recv l P1 - recv l P2. Lemma recv_weaken l P1 P2 : (P1 - P2) - recv l P1 - recv l P2.
Proof. Proof.
rewrite /recv. rewrite /recv. iIntros "HP". iDestruct 1 as (γ P Q i) "(#Hctx&Hγ&Hi&HP1)".
iIntros "HP HP1"; iDestruct "HP1" as (γ P Q i) "(#Hctx&Hγ&Hi&HP1)".
iExists γ, P, Q, i. iFrame "Hctx Hγ Hi". iExists γ, P, Q, i. iFrame "Hctx Hγ Hi".
iNext. iIntros "HQ". by iApply "HP"; iApply "HP1". iNext. iIntros "HQ". by iApply "HP"; iApply "HP1".
Qed. Qed.
......
...@@ -14,7 +14,7 @@ Lemma barrier_spec (N : namespace) : ...@@ -14,7 +14,7 @@ Lemma barrier_spec (N : namespace) :
( l P, {{ send l P P }} signal #l {{ _, True }}) ( l P, {{ send l P P }} signal #l {{ _, True }})
( l P, {{ recv l P }} wait #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.
exists (λ l, CofeMor (recv N l)), (λ l, CofeMor (send N l)). exists (λ l, CofeMor (recv N l)), (λ l, CofeMor (send N l)).
split_and?; simpl. split_and?; simpl.
......
...@@ -15,7 +15,7 @@ Structure lock Σ `{!heapG Σ} := Lock { ...@@ -15,7 +15,7 @@ Structure lock Σ `{!heapG Σ} := Lock {
is_lock_ne N γ lk n: Proper (dist n ==> dist n) (is_lock N γ lk); is_lock_ne N γ lk n: Proper (dist n ==> dist n) (is_lock N γ lk);
is_lock_persistent N γ lk R : PersistentP (is_lock N γ lk R); is_lock_persistent N γ lk R : PersistentP (is_lock N γ lk R);
locked_timeless γ : TimelessP (locked γ); locked_timeless γ : TimelessP (locked γ);
locked_exclusive γ : locked γ locked γ False; locked_exclusive γ : locked γ - locked γ - False;
(* -- operation specs -- *) (* -- operation specs -- *)
newlock_spec N (R : iProp Σ) : newlock_spec N (R : iProp Σ) :
{{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock N γ lk R }}}; {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock N γ lk R }}};
......
...@@ -21,11 +21,11 @@ Context `{!heapG Σ, !spawnG Σ}. ...@@ -21,11 +21,11 @@ Context `{!heapG Σ, !spawnG Σ}.
This is why these are not Texan triples. *) 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
(WP f1 #() {{ Ψ1 }} WP f2 #() {{ Ψ2 }} WP f1 #() {{ Ψ1 }} - WP f2 #() {{ Ψ2 }} -
v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V) ( v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V) -
WP par e {{ Φ }}. WP par e {{ Φ }}.
Proof. Proof.
iIntros (?) "(Hf1 & Hf2 & HΦ)". iIntros (?) "Hf1 Hf2 HΦ".
rewrite /par. wp_value. wp_let. wp_proj. rewrite /par. wp_value. wp_let. wp_proj.
wp_apply (spawn_spec parN with "Hf1"); try wp_done; try solve_ndisj. wp_apply (spawn_spec parN with "Hf1"); try wp_done; try solve_ndisj.
iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _). iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
...@@ -36,11 +36,11 @@ Qed. ...@@ -36,11 +36,11 @@ Qed.
Lemma wp_par (Ψ1 Ψ2 : val iProp Σ) Lemma wp_par (Ψ1 Ψ2 : val iProp Σ)
(e1 e2 : expr) `{!Closed [] e1, Closed [] e2} (Φ : val iProp Σ) : (e1 e2 : expr) `{!Closed [] e1, Closed [] e2} (Φ : val iProp Σ) :
(WP e1 {{ Ψ1 }} WP e2 {{ Ψ2 }} WP e1 {{ Ψ1 }} - WP e2 {{ Ψ2 }} -
v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V) ( v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V) -
WP e1 ||| e2 {{ Φ }}. WP e1 ||| e2 {{ Φ }}.
Proof. Proof.
iIntros "(H1 & H2 & H)". iApply (par_spec Ψ1 Ψ2 with "[- $H]"); try wp_done. iIntros "H1 H2 H". iApply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]"); try wp_done.
iSplitL "H1"; by wp_let. by wp_let. by wp_let. auto.
Qed. Qed.
End proof. End proof.
...@@ -30,8 +30,8 @@ Section proof. ...@@ -30,8 +30,8 @@ Section proof.
Definition locked (γ : gname): iProp Σ := own γ (Excl ()). Definition locked (γ : gname): iProp Σ := own γ (Excl ()).
Lemma locked_exclusive (γ : gname) : locked γ locked γ False. Lemma locked_exclusive (γ : gname) : locked γ - locked γ - False.
Proof. rewrite /locked -own_op own_valid. by iIntros (?). Qed. Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l). Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
......
...@@ -46,11 +46,11 @@ Section proof. ...@@ -46,11 +46,11 @@ Section proof.
Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ := Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
( lo ln : loc, ( lo ln : loc,
lk = (#lo, #ln)%V inv N (lock_inv γ lo ln R))%I. lk = (#lo, #ln)%V inv N (lock_inv γ lo ln R))%I.
Definition issued (γ : gname) (lk : val) (x : nat) (R : iProp Σ) : iProp Σ := Definition issued (γ : gname) (lk : val) (x : nat) (R : iProp Σ) : iProp Σ :=
( lo ln: loc, ( lo ln: loc,
lk = (#lo, #ln)%V inv N (lock_inv γ lo ln R) lk = (#lo, #ln)%V inv N (lock_inv γ lo ln R)
own γ ( (, GSet {[ x ]})))%I. own γ ( (, GSet {[ x ]})))%I.
Definition locked (γ : gname) : iProp Σ := ( o, own γ ( (Excl' o, )))%I. Definition locked (γ : gname) : iProp Σ := ( o, own γ ( (Excl' o, )))%I.
...@@ -65,10 +65,10 @@ Section proof. ...@@ -65,10 +65,10 @@ Section proof.
Global Instance locked_timeless γ : TimelessP (locked γ). Global Instance locked_timeless γ : TimelessP (locked γ).
Proof. apply _. Qed. Proof. apply _. Qed.
Lemma locked_exclusive (γ : gname) : (locked γ locked γ False)%I. Lemma locked_exclusive (γ : gname) : locked γ - locked γ - False.
Proof. Proof.
iIntros "[H1 H2]". iDestruct "H1" as (o1) "H1". iDestruct "H2" as (o2) "H2". iDestruct 1 as (o1) "H1". iDestruct 1 as (o2) "H2".
iCombine "H1" "H2" as "H". iDestruct (own_valid with "H") as %[[] _]. iDestruct (own_valid_2 with "H1 H2") as %[[] _].
Qed. Qed.
Lemma newlock_spec (R : iProp Σ) : Lemma newlock_spec (R : iProp Σ) :
......
...@@ -18,39 +18,38 @@ Section client. ...@@ -18,39 +18,38 @@ Section client.
Definition y_inv (q : Qp) (l : loc) : iProp Σ := Definition y_inv (q : Qp) (l : loc) : iProp Σ :=
( f : val, l {q} f n : Z, WP f #n {{ v, v = #(n + 42) }})%I. ( f : val, l {q} f n : Z, WP f #n {{ v, v = #(n + 42) }})%I.
Lemma y_inv_split q l : y_inv q l (y_inv (q/2) l y_inv (q/2) l). Lemma y_inv_split q l : y_inv q l - (y_inv (q/2) l y_inv (q/2) l).
Proof. Proof.
iDestruct 1 as (f) "[[Hl1 Hl2] #Hf]". iDestruct 1 as (f) "[[Hl1 Hl2] #Hf]".
iSplitL "Hl1"; iExists f; by iSplitL; try iAlways. iSplitL "Hl1"; iExists f; by iSplitL; try iAlways.
Qed. Qed.
Lemma worker_safe q (n : Z) (b y : loc) : Lemma worker_safe q (n : Z) (b y : loc) :
recv N b (y_inv q y) WP worker n #b #y {{ _, True }}. recv N b (y_inv q y) - WP worker n #b #y {{ _, True }}.
Proof. Proof.
iIntros "Hrecv". wp_lam. wp_let. iIntros "Hrecv". wp_lam. wp_let.
wp_apply (wait_spec with "[- $Hrecv]"). iDestruct 1 as (f) "[Hy #Hf]". wp_apply (wait_spec with "Hrecv"). iDestruct 1 as (f) "[Hy #Hf]".
wp_seq. wp_load. wp_seq. wp_load.
iApply (wp_wand with "[]"). iApply "Hf". by iIntros (v) "_". iApply (wp_wand with "[]"). iApply "Hf". by iIntros (v) "_".
Qed. Qed.
Lemma client_safe : True WP client {{ _, True }}. Lemma client_safe : WP client {{ _, True }}%I.
Proof. Proof.
iIntros ""; rewrite /client. wp_alloc y as "Hy". wp_let. iIntros ""; rewrite /client. wp_alloc y as "Hy". wp_let.
wp_apply (newbarrier_spec N (y_inv 1 y)). wp_apply (newbarrier_spec N (y_inv 1 y)).
iIntros (l) "[Hr Hs]". wp_let. iIntros (l) "[Hr Hs]". wp_let.
iApply (wp_par (λ _, True%I) (λ _, True%I)). iSplitL "Hy Hs". iApply (wp_par (λ _, True%I) (λ _, True%I) with "[Hy Hs] [Hr]"); last auto.
- (* The original thread, the sender. *) - (* The original thread, the sender. *)
wp_store. iApply (signal_spec with "[-]"); last by iNext; auto. wp_store. iApply (signal_spec with "[-]"); last by iNext; auto.
iSplitR "Hy"; first by eauto. iSplitR "Hy"; first by eauto.
iExists _; iSplitL; [done|]. iAlways; iIntros (n). wp_let. by wp_op. iExists _; iSplitL; [done|]. iAlways; iIntros (n). wp_let. by wp_op.
- (* The two spawned threads, the waiters. *) - (* The two spawned threads, the waiters. *)
iSplitL; [|by iIntros (_ _) "_ !>"].
iDestruct (recv_weaken with "[] Hr") as "Hr". iDestruct (recv_weaken with "[] Hr") as "Hr".
{ iIntros "Hy". by iApply (y_inv_split with "Hy"). } { iIntros "Hy". by iApply (y_inv_split with "Hy"). }
iMod (recv_split with "Hr") as "[H1 H2]"; first done. iMod (recv_split with "Hr") as "[H1 H2]"; first done.
iApply (wp_par (λ _, True%I) (λ _, True%I)). iApply (wp_par (λ _, True%I) (λ _, True%I) with "[H1] [H2]"); last auto.
iSplitL "H1"; [|iSplitL "H2"; [|by iIntros (_ _) "_ !>"]]; + by iApply worker_safe.
by iApply worker_safe. + by iApply worker_safe.
Qed. Qed.
End client. End client.
...@@ -60,8 +59,7 @@ Let Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ]. ...@@ -60,8 +59,7 @@ Let Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ].
Lemma client_adequate σ : adequate client σ (λ _, True). Lemma client_adequate σ : adequate client σ (λ _, True).
Proof. Proof.
apply (heap_adequacy Σ)=> ?. apply (heap_adequacy Σ)=> ?. apply (client_safe (nroot .@ "barrier")).
apply (client_safe (nroot .@ "barrier")); auto with ndisj.
Qed. Qed.
End ClosedProofs. End ClosedProofs.
......
...@@ -12,7 +12,7 @@ Section LiftingTests. ...@@ -12,7 +12,7 @@ Section LiftingTests.
Definition heap_e : expr := Definition heap_e : expr :=
let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x". let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
Lemma heap_e_spec E : True WP heap_e @ E {{ v, v = #2 }}. Lemma heap_e_spec E : WP heap_e @ E {{ v, v = #2 }}%I.
Proof. Proof.
iIntros "". rewrite /heap_e. iIntros "". rewrite /heap_e.
wp_alloc l. wp_let. wp_load. wp_op. wp_store. by wp_load. wp_alloc l. wp_let. wp_load. wp_op. wp_store. by wp_load.
...@@ -23,7 +23,7 @@ Section LiftingTests. ...@@ -23,7 +23,7 @@ Section LiftingTests.
let: "y" := ref #1 in let: "y" := ref #1 in
"x" <- !"x" + #1 ;; !"x". "x" <- !"x" + #1 ;; !"x".
Lemma heap_e2_spec E : True WP heap_e2 @ E {{ v, v = #2 }}. Lemma heap_e2_spec E : WP heap_e2 @ E {{ v, v = #2 }}%I.
Proof. Proof.
iIntros "". rewrite /heap_e2. iIntros "". rewrite /heap_e2.
wp_alloc l. wp_let. wp_alloc l'. wp_let. wp_alloc l. wp_let. wp_alloc l'. wp_let.
...@@ -40,7 +40,7 @@ Section LiftingTests. ...@@ -40,7 +40,7 @@ Section LiftingTests.
Lemma FindPred_spec n1 n2 E Φ : Lemma FindPred_spec n1 n2 E Φ :
n1 < n2 n1 < n2
Φ #(n2 - 1) WP FindPred #n2 #n1 @ E {{ Φ }}. Φ #(n2 - 1) - WP FindPred #n2 #n1 @ E {{ Φ }}.
Proof. Proof.
iIntros (Hn) "HΦ". iLöb as "IH" forall (n1 Hn). iIntros (Hn) "HΦ". iLöb as "IH" forall (n1 Hn).
wp_rec. wp_let. wp_op. wp_let. wp_op=> ?; wp_if. wp_rec. wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
...@@ -48,7 +48,7 @@ Section LiftingTests. ...@@ -48,7 +48,7 @@ Section LiftingTests.
- by assert (n1 = n2 - 1) as -> by omega. - by assert (n1 = n2 - 1) as -> by omega.
Qed. Qed.
Lemma Pred_spec n E Φ : Φ #(n - 1) WP Pred #n @ E {{ Φ }}. Lemma Pred_spec n E Φ : Φ #(n - 1) - WP Pred #n @ E {{ Φ }}.
Proof. Proof.
iIntros "HΦ". wp_lam. wp_op=> ?; wp_if. iIntros "HΦ". wp_lam. wp_op=> ?; wp_if.
- wp_op. wp_op. - wp_op. wp_op.
...@@ -62,5 +62,5 @@ Section LiftingTests. ...@@ -62,5 +62,5 @@ Section LiftingTests.
Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed. Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
End LiftingTests. End LiftingTests.
Lemma heap_e_adequate σ : adequate heap_e σ (λ v, v = #2). Lemma heap_e_adequate σ : adequate heap_e σ (= #2).
Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed. Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed.
...@@ -31,29 +31,28 @@ Definition barrier_res γ (Φ : X → iProp Σ) : iProp Σ := ...@@ -31,29 +31,28 @@ Definition barrier_res γ (Φ : X → iProp Σ) : iProp Σ :=
( x, own γ (Shot x) Φ x)%I. ( x, own γ (Shot x) Φ x)%I.
Lemma worker_spec e γ l (Φ Ψ : X iProp Σ) `{!Closed [] e} : Lemma worker_spec e γ l (Φ Ψ : X iProp Σ) `{!Closed [] e} :
recv N l (barrier_res γ Φ) ( x, {{ Φ x }} e {{ _, Ψ x }}) recv N l (barrier_res γ Φ) - ( x, {{ Φ x }} e {{ _, Ψ x }}) -
WP wait #l ;; e {{ _, barrier_res γ Ψ }}. WP wait #l ;; e {{ _, barrier_res γ Ψ }}.
Proof. Proof.
iIntros "[Hl #He]". wp_apply (wait_spec with "[- $Hl]"); simpl. iIntros "Hl #He". wp_apply (wait_spec with "[- $Hl]"); simpl.
iDestruct 1 as (x) "[#Hγ Hx]". iDestruct 1 as (x) "[#Hγ Hx]".
wp_seq. iApply (wp_wand with "[Hx]"); [by iApply "He"|]. wp_seq. iApply (wp_wand with "[Hx]"); [by iApply "He"|].
iIntros (v) "?"; iExists x; by iSplit. iIntros (v) "?"; iExists x; by iSplit.
Qed. Qed.
Context (P : iProp Σ) (Φ Φ1 Φ2 Ψ Ψ1 Ψ2 : X -n> iProp Σ). Context (P : iProp Σ) (Φ Φ1 Φ2 Ψ Ψ1 Ψ2 : X -n> iProp Σ).
Context {Φ_split : x, Φ x (Φ1 x Φ2 x)}. Context {Φ_split : x, Φ x - (Φ1 x Φ2 x)}.
Context {Ψ_join : x, (Ψ1 x Ψ2 x) Ψ x}. Context {Ψ_join : x, Ψ1 x - Ψ2 x - Ψ x}.
Lemma P_res_split γ : barrier_res γ Φ barrier_res γ Φ1 barrier_res γ Φ2. Lemma P_res_split γ : barrier_res γ Φ - barrier_res γ Φ1 barrier_res γ Φ2.
Proof. Proof.
iDestruct 1 as (x) "[#Hγ Hx]". iDestruct 1 as (x) "[#Hγ Hx]".
iDestruct (Φ_split with "Hx") as "[H1 H2]". by iSplitL "H1"; iExists x; iSplit. iDestruct (Φ_split with "Hx") as "[H1 H2]". by iSplitL "H1"; iExists x; iSplit.
Qed. Qed.
Lemma Q_res_join γ : barrier_res γ Ψ1 barrier_res γ Ψ2 barrier_res γ Ψ. Lemma Q_res_join γ : barrier_res γ Ψ1 - barrier_res γ Ψ2 - barrier_res γ Ψ.
Proof. Proof.
iIntros "[Hγ Hγ']"; iDestruct 1 as (x) "[#Hγ Hx]"; iDestruct 1 as (x') "[#Hγ' Hx']".
iDestruct "Hγ" as (x) "[#Hγ Hx]"; iDestruct "Hγ'" as (x') "[#Hγ' Hx']".
iAssert ( (x x'))%I as "Hxx". iAssert ( (x x'))%I as "Hxx".
{ iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'". { iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'".
rewrite own_valid csum_validI /= agree_validI agree_equivI uPred.later_equivI /=. rewrite own_valid csum_validI /= agree_validI agree_equivI uPred.later_equivI /=.
...@@ -62,23 +61,22 @@ Proof. ...@@ -62,23 +61,22 @@ Proof.
{ by split; intro; simpl; symmetry; apply iProp_fold_unfold. } { by split; intro; simpl; symmetry; apply iProp_fold_unfold. }
rewrite !cFunctor_compose. iNext. by iRewrite "Hγ2". } rewrite !cFunctor_compose. iNext. by iRewrite "Hγ2". }
iNext. iRewrite -"Hxx" in "Hx'". iNext. iRewrite -"Hxx" in "Hx'".
iExists x; iFrame "Hγ". iApply Ψ_join; by iSplitL "Hx". iExists x; iFrame "Hγ". iApply (Ψ_join with "Hx Hx'").
Qed. Qed.
Lemma client_spec_new eM eW1 eW2 `{!Closed [] eM, !Closed [] eW1, !Closed [] eW2} : Lemma client_spec_new eM eW1 eW2 `{!Closed [] eM, !Closed [] eW1, !Closed [] eW2} :
P P -
{{ P }} eM {{ _, x, Φ x }} {{ P }} eM {{ _, x, Φ x }} -
( x, {{ Φ1 x }} eW1 {{ _, Ψ1 x }}) ( x, {{ Φ1 x }} eW1 {{ _, Ψ1 x }}) -
( x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }}) ( x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }}) -
WP client eM eW1 eW2 {{ _, γ, barrier_res γ Ψ }}. WP client eM eW1 eW2 {{ _, γ, barrier_res γ Ψ }}.
Proof. Proof.
iIntros "/= (HP & #He & #He1 & #He2)"; rewrite /client. iIntros "/= HP #He #He1 #He2"; rewrite /client.
iMod (own_alloc (Pending : one_shotR Σ F)) as (γ) "Hγ"; first done. iMod (own_alloc (Pending : one_shotR Σ F)) as (γ) "Hγ"; first done.
wp_apply (newbarrier_spec N (barrier_res γ Φ)); auto. wp_apply (newbarrier_spec N (barrier_res γ Φ)); auto.
iIntros (l) "[Hr Hs]". iIntros (l) "[Hr Hs]".
set (workers_post (v : val) := (barrier_res γ Ψ1 barrier_res γ Ψ2)%I). set (workers_post (v : val) := (barrier_res γ Ψ1 barrier_res γ Ψ2)%I).
wp_let. wp_apply (wp_par (λ _, True)%I workers_post). wp_let. wp_apply (wp_par (λ _, True)%I workers_post with "[HP Hs Hγ] [Hr]").
iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
- wp_bind eM. iApply (wp_wand with "[HP]"); [by iApply "He"|]. - wp_bind eM. iApply (wp_wand with "[HP]"); [by iApply "He"|].
iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let. iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let.
iMod (own_update with "Hγ") as "Hx". iMod (own_update with "Hγ") as "Hx".
...@@ -87,11 +85,11 @@ Proof. ...@@ -87,11 +85,11 @@ Proof.
iExists x; auto. iExists x; auto.
- iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split. - iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split.
iMod (recv_split with "Hr") as "[H1 H2]"; first done. iMod (recv_split with "Hr") as "[H1 H2]"; first done.
wp_apply (wp_par (λ _, barrier_res γ Ψ1)%I (λ _, barrier_res γ Ψ2)%I). wp_apply (wp_par (λ _, barrier_res γ Ψ1)%I
iSplitL "H1"; [|iSplitL "H2"]. (λ _, barrier_res γ Ψ2)%I with "[H1] [H2]").
+ iApply worker_spec; auto. + iApply (worker_spec with "H1"); auto.
+ iApply worker_spec; auto. + iApply (worker_spec with "H2"); auto.
+ auto. + auto.
- iIntros (_ v) "[_ H]". iDestruct (Q_res_join with "H") as "?". auto. - iIntros (_ v) "[_ [H1 H2]]". iDestruct (Q_res_join with "H1 H2") as "?". auto.
Qed. Qed.
End proof. End proof.
...@@ -26,11 +26,11 @@ Definition rev : val := ...@@ -26,11 +26,11 @@ Definition rev : val :=
end. end.
Lemma rev_acc_wp hd acc xs ys (Φ : val iProp Σ) : Lemma rev_acc_wp hd acc xs ys (Φ : val iProp Σ) :
is_list hd xs is_list acc ys is_list hd xs - is_list acc ys -
( w, is_list w (reverse xs ++ ys) - Φ w) ( w, is_list w (reverse xs ++ ys) - Φ w) -
WP rev hd acc {{ Φ }}. WP rev hd acc {{ Φ }}.
Proof. Proof.
iIntros "(Hxs & Hys & HΦ)". iIntros "Hxs Hys HΦ".
iLöb as "IH" forall (hd acc xs ys Φ). wp_rec. wp_let. iLöb as "IH" forall (hd acc xs ys Φ). wp_rec. wp_let.
destruct xs as [|x xs]; iSimplifyEq. destruct xs as [|x xs]; iSimplifyEq.
- wp_match. by iApply "HΦ". - wp_match. by iApply "HΦ".
...@@ -42,11 +42,11 @@ Proof. ...@@ -42,11 +42,11 @@ Proof.
Qed. Qed.
Lemma rev_wp hd xs (Φ : val iProp Σ) : Lemma rev_wp hd xs (Φ : val iProp Σ) :
is_list hd xs ( w, is_list w (reverse xs) - Φ w) is_list hd xs - ( w, is_list w (reverse xs) - Φ w) -
WP rev hd (InjL #()) {{ Φ }}. WP rev hd (InjL #()) {{ Φ }}.
Proof. Proof.
iIntros "[Hxs HΦ]". iIntros "Hxs HΦ".
iApply (rev_acc_wp hd NONEV xs [] with "[- $Hxs]"). iApply (rev_acc_wp hd NONEV xs [] with "Hxs [%]")=> //.
iSplit; first done. iIntros (w). rewrite right_id_L. iApply "HΦ". iIntros (w). rewrite right_id_L. iApply "HΦ".
Qed. Qed.
End list_reverse. End list_reverse.
...@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics. ...@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Import invariants. From iris.base_logic.lib Require Import invariants.
Lemma demo_0 {M : ucmraT} (P Q : uPred M) : Lemma demo_0 {M : ucmraT} (P Q : uPred M) :
(P Q) ( x, x = 0 x = 1) (Q P). (P Q) - ( x, x = 0 x = 1) (Q P).
Proof. Proof.
iIntros "#H #H2". iIntros "#H #H2".
(* should remove the disjunction "H" *) (* should remove the disjunction "H" *)
...@@ -37,8 +37,9 @@ Proof. ...@@ -37,8 +37,9 @@ Proof.
Qed. Qed.
Lemma demo_2 (M : ucmraT) (P1 P2 P3 P4 Q : uPred M) (P5 : nat uPredC M):