Commit 77ba610d authored by Ralf Jung's avatar Ralf Jung

lib/spawn: make proofs more readable / steppable

parent 745b4422
Pipeline #2119 passed with stage
......@@ -56,23 +56,23 @@ Lemma spawn_spec (Ψ : val → iProp) e (f : val) (Φ : val → iProp) :
heap_ctx heapN WP f #() {{ Ψ }} ( l, join_handle l Ψ - Φ #l)
WP spawn e {{ Φ }}.
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.
iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done.
iPvs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done.
{ iNext. iExists (InjLV #0). iFrame; eauto. }
wp_apply wp_fork. iSplitR "Hf".
- iPvsIntro. wp_seq. iPvsIntro. iApply "HΦ"; rewrite /join_handle. eauto.
- wp_focus (f _). iApply wp_wand_l; iFrame "Hf"; iIntros {v} "Hv".
- iPvsIntro. wp_seq. iPvsIntro. iApply "HΦ". rewrite /join_handle. eauto.
- wp_focus (f _). iApply wp_wand_l. iFrame "Hf"; iIntros {v} "Hv".
iInv N as {v'} "[Hl _]"; first wp_done.
wp_store. iPvsIntro; iSplit; [iNext|done].
iExists (InjRV v); iFrame; eauto.
wp_store. iPvsIntro. iSplit; [iNext|done].
iExists (InjRV v). iFrame. eauto.
Qed.
Lemma join_spec (Ψ : val iProp) l (Φ : val iProp) :
join_handle l Ψ ( v, Ψ v - Φ v) WP join #l {{ Φ }}.
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. iInv N as {v} "[Hl Hinv]".
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- iPvsIntro; iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment