diff --git a/tests/heap_lang.v b/tests/heap_lang.v index 61d0e81a54c0c4a08971ce95362fbfe68a682b4e..0d93617243d23e00a0f86e06747292644b30a9e3 100644 --- a/tests/heap_lang.v +++ b/tests/heap_lang.v @@ -116,6 +116,13 @@ Section tests. P -∗ (∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}. Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed. + Lemma wp_cas l v : + val_is_unboxed v → + l ↦ v -∗ WP CAS #l v v {{ _, True }}. + Proof. + iIntros (?) "?". wp_cas as ? | ?. done. done. + Qed. + End tests. Section printing_tests. diff --git a/theories/heap_lang/lib/atomic_heap.v b/theories/heap_lang/lib/atomic_heap.v index 9de110430c2391ff9789cd62b8731dd50c72a9c0..ad3f079a38ab3281c597ca7b9ed075d1ccbbcd12 100644 --- a/theories/heap_lang/lib/atomic_heap.v +++ b/theories/heap_lang/lib/atomic_heap.v @@ -33,11 +33,15 @@ Structure atomic_heap {Σ} `{!heapG Σ} := AtomicHeap { (λ v, mapsto l 1 v) (λ v (_:()), mapsto l 1 w) (λ _ _, #()%V); + (* 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 → + IntoVal e1 w1 → IntoVal e2 w2 → val_is_unboxed w1 → atomic_wp (cas (#l, e1, e2))%E ⊤ ⊤ - (λ v, ⌜vals_cas_compare_safe v w1⌝ ∗ mapsto l 1 v)%I + (λ v, mapsto l 1 v)%I (λ v (_:()), if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v) (λ v _, #(if decide (v = w1) then true else false)%V); }. @@ -88,16 +92,16 @@ Section proof. Qed. Lemma primitive_cas_spec (l : loc) e1 e2 (w1 w2 : val) : - IntoVal e1 w1 → IntoVal e2 w2 → + IntoVal e1 w1 → IntoVal e2 w2 → val_is_unboxed w1 → atomic_wp (primitive_cas (#l, e1, e2))%E ⊤ ⊤ - (λ v, ⌜vals_cas_compare_safe v w1⌝ ∗ l ↦ v)%I + (λ v, l ↦ v)%I (λ v (_:()), if decide (v = w1) then l ↦ w2 else l ↦ v)%I (λ v _, #(if decide (v = w1) then true else false)%V). Proof. - iIntros (<- <- Q Φ) "? AU". wp_let. repeat wp_proj. - iMod (aupd_acc with "AU") as (v) "[[% H↦] [_ Hclose]]"; first solve_ndisj. - destruct (decide (v = w1)) as [Hv|Hv]; [wp_cas_suc|wp_cas_fail]; + iIntros (<- <- ? Q Φ) "? AU". wp_let. repeat wp_proj. + iMod (aupd_acc with "AU") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj. + destruct (decide (v = w1)) as [<-|Hv]; [wp_cas_suc|wp_cas_fail]; iMod ("Hclose" \$! () with "H↦") as "HΦ"; by iApply "HΦ". Qed. diff --git a/theories/heap_lang/lib/increment.v b/theories/heap_lang/lib/increment.v index b92acccd5269ddea4cb1e28a09d584c050e81c19..4640f7c0167214e2bc091b1c408e6280dae655ae 100644 --- a/theories/heap_lang/lib/increment.v +++ b/theories/heap_lang/lib/increment.v @@ -35,13 +35,12 @@ Section increment. iIntros ([]) "\$ !> AU !> HQ". (* Now go on *) wp_let. wp_op. wp_bind (aheap.(cas) _)%I. - wp_apply (cas_spec with "[HQ]"); first by iAccu. + wp_apply (cas_spec with "[HQ]"); first done; first by iAccu. (* Prove the atomic shift for CAS *) iAuIntro. iApply (aacc_aupd with "AU"); first done. iIntros (x') "H↦". - iApply (aacc_intro with "[H↦]"); [solve_ndisj| |iSplit]. - { iFrame. simpl. auto. } - { iIntros "[_ \$] !> \$ !> //". } + iApply (aacc_intro with "[H↦]"); [solve_ndisj|done|iSplit]. + { eauto 10 with iFrame. } iIntros ([]) "H↦ !>". destruct (decide (#x' = #x)) as [[= ->]|Hx]. - iRight. iExists (). iFrame. iIntros "HΦ !> HQ". diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v index a718a6633e79c147d1d472872cf1e220dd950eaf..58b7feee3a272384df955d67546f7f7ce47e4d16 100644 --- a/theories/heap_lang/proofmode.v +++ b/theories/heap_lang/proofmode.v @@ -221,10 +221,49 @@ Proof. rewrite right_id. by apply sep_mono_r, wand_mono. Qed. +Lemma tac_wp_cas Δ Δ' Δ'' s E i K l v e1 v1 e2 v2 Φ : + IntoVal e1 v1 → IntoVal e2 v2 → + MaybeIntoLaterNEnvs 1 Δ Δ' → + envs_lookup i Δ' = Some (false, l ↦ v)%I → + envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' → + vals_cas_compare_safe v v1 → + (v = v1 → envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ s; E {{ Φ }})) → + (v ≠ v1 → envs_entails Δ' (WP fill K (Lit (LitBool false)) @ s; E {{ Φ }})) → + envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}). +Proof. + rewrite envs_entails_eq=> ?????? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne]. + - rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc. + rewrite into_laterN_env_sound -later_sep /= {1}envs_simple_replace_sound //; simpl. + apply later_mono, sep_mono_r. rewrite right_id. apply wand_mono; auto. + - rewrite -wp_bind. eapply wand_apply. + { eapply wp_cas_fail; eauto. by eexists. } + rewrite into_laterN_env_sound -later_sep /= {1}envs_lookup_split //; simpl. + apply later_mono, sep_mono_r. apply wand_mono; auto. +Qed. +Lemma tac_twp_cas Δ Δ' s E i K l v e1 v1 e2 v2 Φ : + IntoVal e1 v1 → IntoVal e2 v2 → + envs_lookup i Δ = Some (false, l ↦ v)%I → + envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ = Some Δ' → + vals_cas_compare_safe v v1 → + (v = v1 → envs_entails Δ' (WP fill K (Lit (LitBool true)) @ s; E [{ Φ }])) → + (v ≠ v1 → envs_entails Δ (WP fill K (Lit (LitBool false)) @ s; E [{ Φ }])) → + envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E [{ Φ }]). +Proof. + rewrite envs_entails_eq=> ????? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne]. + - rewrite -twp_bind. eapply wand_apply; first exact: twp_cas_suc. + rewrite /= {1}envs_simple_replace_sound //; simpl. + apply sep_mono_r. rewrite right_id. apply wand_mono; auto. + - rewrite -twp_bind. eapply wand_apply. + { eapply twp_cas_fail; eauto. by eexists. } + rewrite /= {1}envs_lookup_split //; simpl. + apply sep_mono_r. apply wand_mono; auto. +Qed. + Lemma tac_wp_cas_fail Δ Δ' s E i K l q v e1 v1 e2 Φ : IntoVal e1 v1 → AsVal e2 → MaybeIntoLaterNEnvs 1 Δ Δ' → - envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 → vals_cas_compare_safe v v1 → + envs_lookup i Δ' = Some (false, l ↦{q} v)%I → + v ≠ v1 → vals_cas_compare_safe v v1 → envs_entails Δ' (WP fill K (Lit (LitBool false)) @ s; E {{ Φ }}) → envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}). Proof. @@ -235,7 +274,8 @@ Proof. Qed. Lemma tac_twp_cas_fail Δ s E i K l q v e1 v1 e2 Φ : IntoVal e1 v1 → AsVal e2 → - envs_lookup i Δ = Some (false, l ↦{q} v)%I → v ≠ v1 → vals_cas_compare_safe v v1 → + envs_lookup i Δ = Some (false, l ↦{q} v)%I → + v ≠ v1 → vals_cas_compare_safe v v1 → envs_entails Δ (WP fill K (Lit (LitBool false)) @ s; E [{ Φ }]) → envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E [{ Φ }]). Proof. @@ -247,25 +287,29 @@ Qed. Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v e1 v1 e2 v2 Φ : IntoVal e1 v1 → IntoVal e2 v2 → MaybeIntoLaterNEnvs 1 Δ Δ' → - envs_lookup i Δ' = Some (false, l ↦ v)%I → v = v1 → vals_cas_compare_safe v v1 → + envs_lookup i Δ' = Some (false, l ↦ v)%I → envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' → + v = v1 → val_is_unboxed v → envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ s; E {{ Φ }}) → envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}). Proof. rewrite envs_entails_eq=> ????????; subst. - rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc. + rewrite -wp_bind. eapply wand_apply. + { eapply wp_cas_suc; eauto. by left. } rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl. rewrite right_id. by apply later_mono, sep_mono_r, wand_mono. Qed. Lemma tac_twp_cas_suc Δ Δ' s E i K l v e1 v1 e2 v2 Φ : IntoVal e1 v1 → IntoVal e2 v2 → - envs_lookup i Δ = Some (false, l ↦ v)%I → v = v1 → vals_cas_compare_safe v v1 → + envs_lookup i Δ = Some (false, l ↦ v)%I → envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ = Some Δ' → + v = v1 → val_is_unboxed v → envs_entails Δ' (WP fill K (Lit (LitBool true)) @ s; E [{ Φ }]) → envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E [{ Φ }]). Proof. rewrite envs_entails_eq. intros; subst. - rewrite -twp_bind. eapply wand_apply; first exact: twp_cas_suc. + rewrite -twp_bind. eapply wand_apply. + { eapply twp_cas_suc; eauto. by left. } rewrite envs_simple_replace_sound //; simpl. rewrite right_id. by apply sep_mono_r, wand_mono. Qed. @@ -392,6 +436,36 @@ Tactic Notation "wp_store" := | _ => fail "wp_store: not a 'wp'" end. +Tactic Notation "wp_cas" "as" simple_intropattern(H1) "|" simple_intropattern(H2) := + let solve_mapsto _ := + let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in + iAssumptionCore || fail "wp_cas: cannot find" l "↦ ?" in + iStartProof; + lazymatch goal with + | |- envs_entails _ (wp ?s ?E ?e ?Q) => + first + [reshape_expr e ltac:(fun K e' => + eapply (tac_wp_cas _ _ _ _ _ _ K); [iSolveTC|iSolveTC|..]) + |fail 1 "wp_cas: cannot find 'CAS' in" e]; + [iSolveTC + |solve_mapsto () + |pm_reflexivity + |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *) + |intros H1; wp_expr_simpl; try wp_value_head + |intros H2; wp_expr_simpl; try wp_value_head] + | |- envs_entails _ (twp ?E ?e ?Q) => + first + [reshape_expr e ltac:(fun K e' => + eapply (tac_twp_cas _ _ _ _ _ K); [iSolveTC|iSolveTC|..]) + |fail 1 "wp_cas: cannot find 'CAS' in" e]; + [solve_mapsto () + |pm_reflexivity + |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *) + |intros H1; wp_expr_simpl; try wp_value_head + |intros H2; wp_expr_simpl; try wp_value_head] + | _ => fail "wp_cas: not a 'wp'" + end. + Tactic Notation "wp_cas_fail" := let solve_mapsto _ := let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in @@ -406,7 +480,7 @@ Tactic Notation "wp_cas_fail" := [iSolveTC |solve_mapsto () |try congruence - |try (fast_done || left; fast_done || right; fast_done) (* vals_cas_compare_safe *) + |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *) |simpl; try wp_value_head] | |- envs_entails _ (twp ?s ?E ?e ?Q) => first @@ -415,7 +489,7 @@ Tactic Notation "wp_cas_fail" := |fail 1 "wp_cas_fail: cannot find 'CAS' in" e]; [solve_mapsto () |try congruence - |try (fast_done || left; fast_done || right; fast_done) (* vals_cas_compare_safe *) + |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *) |wp_expr_simpl; try wp_value_head] | _ => fail "wp_cas_fail: not a 'wp'" end. @@ -433,9 +507,9 @@ Tactic Notation "wp_cas_suc" := |fail 1 "wp_cas_suc: cannot find 'CAS' in" e]; [iSolveTC |solve_mapsto () - |try congruence - |try (fast_done || left; fast_done || right; fast_done) (* vals_cas_compare_safe *) |pm_reflexivity + |try congruence + |try fast_done (* vals_cas_compare_safe *) |simpl; try wp_value_head] | |- envs_entails _ (twp ?E ?e ?Q) => first @@ -443,9 +517,9 @@ Tactic Notation "wp_cas_suc" := eapply (tac_twp_cas_suc _ _ _ _ _ K); [iSolveTC|iSolveTC|..]) |fail 1 "wp_cas_suc: cannot find 'CAS' in" e]; [solve_mapsto () - |try congruence - |try (fast_done || left; fast_done || right; fast_done) (* vals_cas_compare_safe *) |pm_reflexivity + |try congruence + |try fast_done (* vals_cas_compare_safe *) |wp_expr_simpl; try wp_value_head] | _ => fail "wp_cas_suc: not a 'wp'" end. diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v index 20abcb4fc6d5550a654e2a3e82e5cbbd26898e53..2ccfba251032b1299db668b16ec3bcbbefce27d9 100644 --- a/theories/proofmode/coq_tactics.v +++ b/theories/proofmode/coq_tactics.v @@ -65,18 +65,27 @@ Proof. apply envs_lookup_sound'. Qed. Lemma envs_lookup_persistent_sound Δ i P : envs_lookup i Δ = Some (true,P) → of_envs Δ ⊢ □ P ∗ of_envs Δ. Proof. intros ?%(envs_lookup_sound' _ false). by destruct Δ. Qed. +Lemma envs_lookup_sound_2 Δ i p P : + envs_wf Δ → envs_lookup i Δ = Some (p,P) → + □?p P ∗ of_envs (envs_delete true i p Δ) ⊢ of_envs Δ. +Proof. + rewrite /envs_lookup /of_envs=>Hwf ?. rewrite [⌜envs_wf Δ⌝%I]pure_True // left_id. + destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=. + - rewrite (env_lookup_perm Γp) //= intuitionistically_and + and_sep_intuitionistically and_elim_r. + cancel [□ P]%I. solve_sep_entails. + - destruct (Γs !! i) eqn:?; simplify_eq/=. + rewrite (env_lookup_perm Γs) //= and_elim_r. + cancel [P]. solve_sep_entails. +Qed. Lemma envs_lookup_split Δ i p P : envs_lookup i Δ = Some (p,P) → of_envs Δ ⊢ □?p P ∗ (□?p P -∗ of_envs Δ). Proof. - rewrite /envs_lookup /of_envs=>?. apply pure_elim_l=> Hwf. - destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=. - - rewrite pure_True // left_id (env_lookup_perm Γp) //= - intuitionistically_and and_sep_intuitionistically. - cancel [□ P]%I. apply wand_intro_l. solve_sep_entails. - - destruct (Γs !! i) eqn:?; simplify_eq/=. - rewrite (env_lookup_perm Γs) //=. rewrite pure_True // left_id. - cancel [P]. apply wand_intro_l. solve_sep_entails. + intros. apply pure_elim with (envs_wf Δ). + { rewrite of_envs_eq. apply and_elim_l. } + intros. rewrite {1}envs_lookup_sound//. + apply sep_mono_r. apply wand_intro_l, envs_lookup_sound_2; done. Qed. Lemma envs_lookup_delete_sound Δ Δ' rp i p P : @@ -198,6 +207,17 @@ Lemma envs_simple_replace_sound Δ Δ' i p P Γ : of_envs Δ ⊢ □?p P ∗ ((if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'). Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed. +Lemma envs_simple_replace_maybe_sound Δ Δ' i p P Γ : + envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' → + of_envs Δ ⊢ □?p P ∗ (((if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ') ∧ (□?p P -∗ of_envs Δ)). +Proof. + intros. apply pure_elim with (envs_wf Δ). + { rewrite of_envs_eq. apply and_elim_l. } + intros. rewrite {1}envs_lookup_sound//. apply sep_mono_r, and_intro. + - rewrite envs_simple_replace_sound'//. + - apply wand_intro_l, envs_lookup_sound_2; done. +Qed. + Lemma envs_simple_replace_singleton_sound Δ Δ' i p P j Q : envs_lookup i Δ = Some (p,P) → envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' →