diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v index 579e9239c1e4472ac268e0991453c928708fd1a1..c71a4b675a05c02c98a71e38f9d0c9318bb31af1 100644 --- a/heap_lang/lib/counter.v +++ b/heap_lang/lib/counter.v @@ -5,6 +5,8 @@ From iris.proofmode Require Import invariants ghost_ownership coq_tactics. From iris.heap_lang Require Import proofmode notation. Import uPred. +Definition counterN : namespace := nroot .@ "counter". + Definition newcounter : val := λ: <>, ref #0. Definition inc : val := rec: "inc" "l" := @@ -26,19 +28,17 @@ Local Notation iProp := (iPropG heap_lang Σ). Definition counter_inv (l : loc) (n : mnat) : iProp := (l ↦ #n)%I. Definition counter (l : loc) (n : nat) : iProp := - (∃ N γ, heapN ⊥ N ∧ heap_ctx ∧ - auth_ctx γ N (counter_inv l) ∧ auth_own γ (n:mnat))%I. + (∃ γ, heap_ctx ∧ auth_ctx γ counterN (counter_inv l) ∧ auth_own γ (n:mnat))%I. (** The main proofs. *) Global Instance counter_persistent l n : PersistentP (counter l n). Proof. apply _. Qed. -Lemma newcounter_spec N (R : iProp) Φ : - heapN ⊥ N → +Lemma newcounter_spec (R : iProp) Φ : heap_ctx ★ (∀ l, counter l 0 -★ Φ #l) ⊢ WP newcounter #() {{ Φ }}. Proof. - iIntros (?) "[#Hh HΦ]". rewrite /newcounter. wp_seq. wp_alloc l as "Hl". - iPvs (auth_alloc (counter_inv l) N _ (O:mnat) with "[Hl]") + iIntros "[#Hh HΦ]". rewrite /newcounter. wp_seq. wp_alloc l as "Hl". + iPvs (auth_alloc (counter_inv l) counterN _ (O:mnat) with "[Hl]") as (γ) "[#? Hγ]"; try by auto. iPvsIntro. iApply "HΦ". rewrite /counter; eauto 10. Qed. @@ -47,13 +47,13 @@ Lemma inc_spec l j (Φ : val → iProp) : counter l j ★ (counter l (S j) -★ Φ #()) ⊢ WP inc #l {{ Φ }}. Proof. iIntros "[Hl HΦ]". iLöb as "IH". wp_rec. - iDestruct "Hl" as (N γ) "(% & #? & #Hγ & Hγf)". + iDestruct "Hl" as (γ) "(#Hh & #Hγ & Hγf)". wp_focus (! _)%E. - iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto with fsaV. + iApply (auth_fsa (counter_inv l) (wp_fsa _) _ counterN); auto with fsaV. iIntros "{\$Hγ \$Hγf}"; iIntros (j') "[% Hl] /="; rewrite {2}/counter_inv. wp_load; iPvsIntro; iExists j; iSplit; [done|iIntros "{\$Hl} Hγf"]. wp_let; wp_op. wp_focus (CAS _ _ _). - iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto with fsaV. + iApply (auth_fsa (counter_inv l) (wp_fsa _) _ counterN); auto with fsaV. iIntros "{\$Hγ \$Hγf}"; iIntros (j'') "[% Hl] /="; rewrite {2}/counter_inv. destruct (decide (j `max` j'' = j `max` j')) as [Hj|Hj]. - wp_cas_suc; first (by do 3 f_equal); iPvsIntro. @@ -62,7 +62,7 @@ Proof. rewrite {2}/counter_inv !mnat_op_max (Nat.max_l (S _)); last abstract lia. rewrite Nat2Z.inj_succ -Z.add_1_l. iIntros "{\$Hl} Hγf". wp_if. - iPvsIntro; iApply "HΦ"; iExists N, γ; repeat iSplit; eauto. + iPvsIntro; iApply "HΦ"; iExists γ; repeat iSplit; eauto. iApply (auth_own_mono with "Hγf"). apply mnat_included. abstract lia. - wp_cas_fail; first (rewrite !mnat_op_max; by intros [= ?%Nat2Z.inj]). iPvsIntro. iExists j; iSplit; [done|iIntros "{\$Hl} Hγf"]. @@ -73,9 +73,9 @@ Lemma read_spec l j (Φ : val → iProp) : counter l j ★ (∀ i, ■ (j ≤ i)%nat → counter l i -★ Φ #i) ⊢ WP read #l {{ Φ }}. Proof. - iIntros "[Hc HΦ]". iDestruct "Hc" as (N γ) "(% & #? & #Hγ & Hγf)". + iIntros "[Hc HΦ]". iDestruct "Hc" as (γ) "(#Hh & #Hγ & Hγf)". rewrite /read. wp_let. - iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto with fsaV. + iApply (auth_fsa (counter_inv l) (wp_fsa _) _ counterN); auto with fsaV. iIntros "{\$Hγ \$Hγf}"; iIntros (j') "[% Hl] /=". wp_load; iPvsIntro; iExists (j `max` j'); iSplit. { iPureIntro; apply mnat_local_update; abstract lia. } diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v index 777abe5676d7479e2358918d5e0c638cdfe4afba..a9b4f3a18779dbcef00bcf26f5d354516ae5ac95 100644 --- a/heap_lang/lib/lock.v +++ b/heap_lang/lib/lock.v @@ -3,6 +3,8 @@ From iris.proofmode Require Import invariants ghost_ownership. From iris.heap_lang Require Import proofmode notation. Import uPred. +Definition lockN : namespace := nroot .@ "lock". + Definition newlock : val := λ: <>, ref #false. Definition acquire : val := rec: "acquire" "l" := @@ -25,11 +27,10 @@ Definition lock_inv (γ : gname) (l : loc) (R : iProp) : iProp := (∃ b : bool, l ↦ #b ★ if b then True else own γ (Excl ()) ★ R)%I. Definition is_lock (l : loc) (R : iProp) : iProp := - (∃ N γ, heapN ⊥ N ∧ heap_ctx ∧ inv N (lock_inv γ l R))%I. + (∃ γ, heap_ctx ∧ inv lockN (lock_inv γ l R))%I. Definition locked (l : loc) (R : iProp) : iProp := - (∃ N γ, heapN ⊥ N ∧ heap_ctx ∧ - inv N (lock_inv γ l R) ∧ own γ (Excl ()))%I. + (∃ γ, heap_ctx ∧ inv lockN (lock_inv γ l R) ∧ own γ (Excl ()))%I. Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l). Proof. solve_proper. Qed. @@ -43,39 +44,38 @@ Global Instance is_lock_persistent l R : PersistentP (is_lock l R). Proof. apply _. Qed. Lemma locked_is_lock l R : locked l R ⊢ is_lock l R. -Proof. rewrite /is_lock. iDestruct 1 as (N γ) "(?&?&?&_)"; eauto. Qed. +Proof. rewrite /is_lock. iDestruct 1 as (γ) "(?&?&_)"; eauto. Qed. -Lemma newlock_spec N (R : iProp) Φ : - heapN ⊥ N → +Lemma newlock_spec (R : iProp) Φ : heap_ctx ★ R ★ (∀ l, is_lock l R -★ Φ #l) ⊢ WP newlock #() {{ Φ }}. Proof. - iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock. + iIntros "(#Hh & HR & HΦ)". rewrite /newlock. wp_seq. wp_alloc l as "Hl". iPvs (own_alloc (Excl ())) as (γ) "Hγ"; first done. - iPvs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?"; first done. + iPvs (inv_alloc lockN _ (lock_inv γ l R) with "[-HΦ]") as "#?"; first done. { iIntros ">". iExists false. by iFrame. } - iPvsIntro. iApply "HΦ". iExists N, γ; eauto. + iPvsIntro. iApply "HΦ". iExists γ; eauto. Qed. Lemma acquire_spec l R (Φ : val → iProp) : is_lock l R ★ (locked l R -★ R -★ Φ #()) ⊢ WP acquire #l {{ Φ }}. Proof. - iIntros "[Hl HΦ]". iDestruct "Hl" as (N γ) "(%&#?&#?)". + iIntros "[Hl HΦ]". iDestruct "Hl" as (γ) "[#Hh #?]". iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E. - iInv N as ([]) "[Hl HR]". + iInv lockN as ([]) "[Hl HR]". - wp_cas_fail. iPvsIntro; iSplitL "Hl". + iNext. iExists true; eauto. + wp_if. by iApply "IH". - wp_cas_suc. iPvsIntro. iDestruct "HR" as "[Hγ HR]". iSplitL "Hl". + iNext. iExists true; eauto. - + wp_if. iApply ("HΦ" with "[-HR] HR"). iExists N, γ; eauto. + + wp_if. iApply ("HΦ" with "[-HR] HR"). iExists γ; eauto. Qed. Lemma release_spec R l (Φ : val → iProp) : locked l R ★ R ★ Φ #() ⊢ WP release #l {{ Φ }}. Proof. - iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as (N γ) "(% & #? & #? & Hγ)". - rewrite /release. wp_let. iInv N as (b) "[Hl _]". + iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as (γ) "(#Hh & #? & Hγ)". + rewrite /release. wp_let. iInv lockN as (b) "[Hl _]". wp_store. iPvsIntro. iFrame "HΦ". iNext. iExists false. by iFrame. Qed. End proof. diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v index 25259889d92a614f03297cec9aa631ecdf4bcb01..7efd44ee5662fd2c8184db127021af93554d9d79 100644 --- a/heap_lang/lib/par.v +++ b/heap_lang/lib/par.v @@ -12,16 +12,16 @@ Notation "e1 || e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope. Global Opaque par. Section proof. -Context `{!heapG Σ, !spawnG Σ} (N : namespace). +Context `{!heapG Σ, !spawnG Σ}. Local Notation iProp := (iPropG heap_lang Σ). Lemma par_spec (Ψ1 Ψ2 : val → iProp) e (f1 f2 : val) (Φ : val → iProp) : - heapN ⊥ N → to_val e = Some (f1,f2)%V → + to_val e = Some (f1,f2)%V → (heap_ctx ★ WP f1 #() {{ Ψ1 }} ★ WP f2 #() {{ Ψ2 }} ★ ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V) ⊢ WP par e {{ Φ }}. Proof. - iIntros (??) "(#Hh&Hf1&Hf2&HΦ)". + iIntros (?) "(#Hh&Hf1&Hf2&HΦ)". rewrite /par. wp_value. iPvsIntro. wp_let. wp_proj. wp_apply spawn_spec; try wp_done. iFrame "Hf1 Hh". iIntros (l) "Hl". wp_let. wp_proj. wp_focus (f2 _). @@ -32,12 +32,11 @@ Qed. Lemma wp_par (Ψ1 Ψ2 : val → iProp) (e1 e2 : expr) `{!Closed [] e1, Closed [] e2} (Φ : val → iProp) : - heapN ⊥ N → (heap_ctx ★ WP e1 {{ Ψ1 }} ★ WP e2 {{ Ψ2 }} ★ ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V) ⊢ WP e1 || e2 {{ Φ }}. Proof. - iIntros (?) "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2); try wp_done. + iIntros "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2); try wp_done. iFrame "Hh H". iSplitL "H1"; by wp_let. Qed. End proof. diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v index 4c2617a7f09960df3b8926fb3318df376b1d8b6e..6e34021d0bd94215381824886ad56ba89388db3b 100644 --- a/heap_lang/lib/spawn.v +++ b/heap_lang/lib/spawn.v @@ -3,6 +3,8 @@ From iris.proofmode Require Import invariants ghost_ownership. From iris.heap_lang Require Import proofmode notation. Import uPred. +Definition spawnN : namespace := nroot .@ "spawn". + Definition spawn : val := λ: "f", let: "c" := ref NONE in @@ -28,7 +30,7 @@ Proof. destruct H as (?&?). split. apply: inGF_inG. Qed. (** Now we come to the Iris part of the proof. *) Section proof. -Context `{!heapG Σ, !spawnG Σ} (N : namespace). +Context `{!heapG Σ, !spawnG Σ}. Local Notation iProp := (iPropG heap_lang Σ). Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp) : iProp := @@ -36,8 +38,7 @@ Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp) : iProp := ∃ v, lv = SOMEV v ★ (Ψ v ∨ own γ (Excl ()))))%I. Definition join_handle (l : loc) (Ψ : val → iProp) : iProp := - (heapN ⊥ N ★ ∃ γ, heap_ctx ★ own γ (Excl ()) ★ - inv N (spawn_inv γ l Ψ))%I. + (∃ γ, heap_ctx ★ own γ (Excl ()) ★ inv spawnN (spawn_inv γ l Ψ))%I. Typeclasses Opaque join_handle. @@ -51,19 +52,18 @@ Proof. solve_proper. Qed. (** The main proofs. *) Lemma spawn_spec (Ψ : val → iProp) e (f : val) (Φ : val → iProp) : to_val e = Some f → - heapN ⊥ N → heap_ctx ★ 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. + iPvs (inv_alloc spawnN _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done. { iNext. iExists NONEV. 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". - iInv N as (v') "[Hl _]". + iInv spawnN as (v') "[Hl _]". wp_store. iPvsIntro. iSplit; [iNext|done]. iExists (SOMEV v). iFrame. eauto. Qed. @@ -71,8 +71,8 @@ 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γ&#?)". - iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv N as (v) "[Hl Hinv]". + rewrite /join_handle; iIntros "[H Hv]". iDestruct "H" as (γ) "(#?&Hγ&#?)". + iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv spawnN as (v) "[Hl Hinv]". wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst. - iPvsIntro; iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|]. wp_match. iApply ("IH" with "Hγ Hv"). diff --git a/tests/barrier_client.v b/tests/barrier_client.v index fcc682e31e15168e887e6b1d2cbbda10558ca18a..ae0d5df08505a7e75841cb1f226ebb37d937ce72 100644 --- a/tests/barrier_client.v +++ b/tests/barrier_client.v @@ -41,8 +41,8 @@ Section client. iIntros (?) "#Hh"; rewrite /client. wp_alloc y as "Hy". wp_let. wp_apply (newbarrier_spec N (y_inv 1 y)); first done. iFrame "Hh". iIntros (l) "[Hr Hs]". wp_let. - iApply (wp_par N (λ _, True%I) (λ _, True%I)); first done. - iFrame "Hh". iSplitL "Hy Hs". + iApply (wp_par (λ _, True%I) (λ _, True%I)). iFrame "Hh". + iSplitL "Hy Hs". - (* The original thread, the sender. *) wp_store. iApply signal_spec; iFrame "Hs"; iSplit; [|done]. iExists _; iSplitL; [done|]. iAlways; iIntros (n). wp_let. by wp_op. @@ -51,8 +51,8 @@ Section client. iDestruct (recv_weaken with "[] Hr") as "Hr". { iIntros "Hy". by iApply (y_inv_split with "Hy"). } iPvs (recv_split with "Hr") as "[H1 H2]"; first done. - iApply (wp_par N (λ _, True%I) (λ _, True%I)); eauto. - iFrame "Hh"; iSplitL "H1"; [|iSplitL "H2"; [|by iIntros (_ _) "_ >"]]; + iApply (wp_par (λ _, True%I) (λ _, True%I)). iFrame "Hh". + iSplitL "H1"; [|iSplitL "H2"; [|by iIntros (_ _) "_ >"]]; iApply worker_safe; by iSplit. Qed. End client. diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v index 795d6d0a696d8c1d667770dab1009fd97ce0b4dd..44b6be39033067723c81cc8dae6a93b89a2109d8 100644 --- a/tests/joining_existentials.v +++ b/tests/joining_existentials.v @@ -77,8 +77,7 @@ Proof. wp_apply (newbarrier_spec N (barrier_res γ Φ)); auto. iFrame "Hh". iIntros (l) "[Hr Hs]". set (workers_post (v : val) := (barrier_res γ Ψ1 ★ barrier_res γ Ψ2)%I). - wp_let. wp_apply (wp_par _ (λ _, True)%I workers_post); - try iFrame "Hh"; first done. + wp_let. wp_apply (wp_par (λ _, True)%I workers_post); iFrame "Hh". iSplitL "HP Hs Hγ"; [|iSplitL "Hr"]. - wp_focus eM. iApply wp_wand_l; iSplitR "HP"; [|by iApply "He"]. iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let. @@ -88,8 +87,8 @@ Proof. iExists x; auto. - iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split. iPvs (recv_split with "Hr") as "[H1 H2]"; first done. - wp_apply (wp_par _ (λ _, barrier_res γ Ψ1)%I - (λ _, barrier_res γ Ψ2)%I); try iFrame "Hh"; first done. + wp_apply (wp_par (λ _, barrier_res γ Ψ1)%I + (λ _, barrier_res γ Ψ2)%I); iFrame "Hh". iSplitL "H1"; [|iSplitL "H2"]. + iApply worker_spec; auto. + iApply worker_spec; auto.