add wp_cas tactic that performs case distinction; weaken logatm heap to be easier to use

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.

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.
 

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".

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.

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 Δ' →