Merge branch 'ralf/eq' into 'master'

heap_lang: Make binary "=" operator partial, to sync with CmpXchg

Closes #248

See merge request iris!283

tests/heap_lang.v

@@ -76,8 +76,9 @@ Section tests.
 
   Definition heap_e6 : val := λ: "v", "v" = "v".
 
-  Lemma heap_e6_spec (v : val) : (WP heap_e6 v {{ w, ⌜ w = #true ⌝ }})%I.
-  Proof. wp_lam. wp_op. by case_bool_decide. Qed.
+  Lemma heap_e6_spec (v : val) :
+    val_is_unboxed v → (WP heap_e6 v {{ w, ⌜ w = #true ⌝ }})%I.
+  Proof. intros ?. wp_lam. wp_op. by case_bool_decide. Qed.
 
   Definition heap_e7 : val := λ: "v", CmpXchg "v" #0 #1.
 

theories/heap_lang/lang.v

@@ -61,7 +61,7 @@ Open Scope Z_scope.
 Definition proph_id := positive.
 
 Inductive base_lit : Set :=
-  | LitInt (n : Z) | LitBool (b : bool) | LitUnit
+  | LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitErased
   | LitLoc (l : loc) | LitProphecy (p: proph_id).
 Inductive un_op : Set :=
   | NegOp | MinusUnOp.
@@ -151,38 +151,33 @@ Ignoring (as usual) the fact that we have to fit the infinite Z/loc into 61
 bits, this means every value is machine-word-sized and can hence be atomically
 read and written.  Also notice that the sets of boxed and unboxed values are
 disjoint. *)
+Definition lit_is_unboxed (l: base_lit) : Prop :=
+  match l with
+  (** Disallow comparing (erased) prophecies with (erased) prophecies, by
+  considering them boxed. *)
+  | LitProphecy _ | LitErased => False
+  | _ => True
+  end.
 Definition val_is_unboxed (v : val) : Prop :=
   match v with
-  | LitV _ => True
-  | InjLV (LitV _) => True
-  | InjRV (LitV _) => True
+  | LitV l => lit_is_unboxed l
+  | InjLV (LitV l) => lit_is_unboxed l
+  | InjRV (LitV l) => lit_is_unboxed l
   | _ => False
   end.
 
-(** CmpXchg just compares the word-sized representation of two values, it cannot
-look into boxed data.  This works out fine if at least one of the to-be-compared
+Instance lit_is_unboxed_dec l : Decision (lit_is_unboxed l).
+Proof. destruct l; simpl; exact (decide _). Defined.
+Instance val_is_unboxed_dec v : Decision (val_is_unboxed v).
+Proof. destruct v as [ | | | [] | [] ]; simpl; exact (decide _). Defined.
+
+(** We just compare the word-sized representation of two values, without looking
+into boxed data.  This works out fine if at least one of the to-be-compared
 values is unboxed (exploiting the fact that an unboxed and a boxed value can
 never be equal because these are disjoint sets). *)
-Definition vals_cmpxchg_compare_safe (vl v1 : val) : Prop :=
+Definition vals_compare_safe (vl v1 : val) : Prop :=
   val_is_unboxed vl ∨ val_is_unboxed v1.
-Arguments vals_cmpxchg_compare_safe !_ !_ /.
-
-(** We don't compare the logical program values, but we first normalize them
-to make sure that prophecies are treated like unit.
-Also all functions become the same, but still distinct from anything else. *)
-Definition lit_for_compare (l : base_lit) : base_lit :=
-  match l with
-  | LitProphecy p => LitUnit
-  | l => l
-  end.
-Fixpoint val_for_compare (v : val) : val :=
-  match v with
-  | LitV l => LitV (lit_for_compare l)
-  | PairV v1 v2 => PairV (val_for_compare v1) (val_for_compare v2)
-  | InjLV v => InjLV (val_for_compare v)
-  | InjRV v => InjRV (val_for_compare v)
-  | RecV f x e => RecV BAnon BAnon (Val $ LitV $ LitUnit)
-  end.
+Arguments vals_compare_safe !_ !_ /.
 
 (** The state: heaps of vals. *)
 Record state : Type := {
@@ -263,12 +258,18 @@ Proof. solve_decision. Defined.
 Instance base_lit_countable : Countable base_lit.
 Proof.
  refine (inj_countable' (λ l, match l with
-  | LitInt n => (inl (inl n), None) | LitBool b => (inl (inr b), None)
-  | LitUnit => (inr (inl ()), None) | LitLoc l => (inr (inr l), None)
-  | LitProphecy p => (inr (inl ()), Some p)
+  | LitInt n => (inl (inl n), None)
+  | LitBool b => (inl (inr b), None)
+  | LitUnit => (inr (inl false), None)
+  | LitErased => (inr (inl true), None)
+  | LitLoc l => (inr (inr l), None)
+  | LitProphecy p => (inr (inl false), Some p)
   end) (λ l, match l with
-  | (inl (inl n), None) => LitInt n | (inl (inr b), None) => LitBool b
-  | (inr (inl ()), None) => LitUnit | (inr (inr l), None) => LitLoc l
+  | (inl (inl n), None) => LitInt n
+  | (inl (inr b), None) => LitBool b
+  | (inr (inl false), None) => LitUnit
+  | (inr (inl true), None) => LitErased
+  | (inr (inr l), None) => LitLoc l
   | (_, Some p) => LitProphecy p
   end) _); by intros [].
 Qed.
@@ -519,7 +520,10 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
 Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
   if decide (op = EqOp) then
     (* Crucially, this compares the same way as [CmpXchg]! *)
-    Some $ LitV $ LitBool $ bool_decide (val_for_compare v1 = val_for_compare v2)
+    if decide (vals_compare_safe v1 v2) then
+      Some $ LitV $ LitBool $ bool_decide (v1 = v2)
+    else
+      None
   else
     match v1, v2 with
     | LitV (LitInt n1), LitV (LitInt n2) => LitV <$> bin_op_eval_int op n1 n2
@@ -635,10 +639,10 @@ Inductive head_step : expr → state → list observation → expr → state →
                (Val $ LitV LitUnit) (state_upd_heap <[l:=v]> σ)
                []
   | CmpXchgS l v1 v2 vl σ b :
-     vals_cmpxchg_compare_safe vl v1 →
      σ.(heap) !! l = Some vl →
      (* Crucially, this compares the same way as [EqOp]! *)
-     b = bool_decide (val_for_compare vl = val_for_compare v1) →
+     vals_compare_safe vl v1 →
+     b = bool_decide (vl = v1) →
      head_step (CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
                []
                (Val $ PairV vl (LitV $ LitBool b)) (if b then state_upd_heap <[l:=v2]> σ else σ)

theories/heap_lang/lib/atomic_heap.v

@@ -37,8 +37,8 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
   cmpxchg_spec (l : loc) (w1 w2 : val) :
     val_is_unboxed w1 →
     <<< ∀ v, mapsto l 1 v >>> cmpxchg #l w1 w2 @ ⊤
-    <<< if decide (val_for_compare v = val_for_compare w1) then mapsto l 1 w2 else mapsto l 1 v,
-        RET (v, #if decide (val_for_compare v = val_for_compare w1) then true else false) >>>;
+    <<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
+        RET (v, #if decide (v = w1) then true else false) >>>;
 }.
 Arguments atomic_heap _ {_}.
 
@@ -68,8 +68,8 @@ Section derived.
   Lemma cas_spec (l : loc) (w1 w2 : val) :
     val_is_unboxed w1 →
     <<< ∀ v, mapsto l 1 v >>> CAS #l w1 w2 @ ⊤
-    <<< if decide (val_for_compare v = val_for_compare w1) then mapsto l 1 w2 else mapsto l 1 v,
-        RET #if decide (val_for_compare v = val_for_compare w1) then true else false >>>.
+    <<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
+        RET #if decide (v = w1) then true else false >>>.
   Proof.
     iIntros (? Φ) "AU". awp_apply cmpxchg_spec; first done.
     iApply (aacc_aupd_commit with "AU"); first done.
@@ -119,12 +119,12 @@ Section proof.
     val_is_unboxed w1 →
     <<< ∀ (v : val), l ↦ v >>>
       primitive_cmpxchg #l w1 w2 @ ⊤
-    <<< if decide (val_for_compare v = val_for_compare w1) then l ↦ w2 else l ↦ v,
-        RET (v, #if decide (val_for_compare v = val_for_compare w1) then true else false) >>>.
+    <<< if decide (v = w1) then l ↦ w2 else l ↦ v,
+        RET (v, #if decide (v = w1) then true else false) >>>.
   Proof.
     iIntros (? Φ) "AU". wp_lam. wp_pures.
     iMod "AU" as (v) "[H↦ [_ Hclose]]".
-    destruct (decide (val_for_compare v = val_for_compare w1)) as [Heq|Hne];
+    destruct (decide (v = w1)) as [Heq|Hne];
       [wp_cmpxchg_suc|wp_cmpxchg_fail];
     iMod ("Hclose" with "H↦") as "HΦ"; done.
   Qed.

theories/heap_lang/lifting.v

@@ -161,8 +161,19 @@ Instance pure_unop op v v' :
 Proof. solve_pure_exec. Qed.
 
 Instance pure_binop op v1 v2 v' :
-  PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op (Val v1) (Val v2)) (Val v').
+  PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op (Val v1) (Val v2)) (Val v') | 10.
 Proof. solve_pure_exec. Qed.
+(* Higher-priority instance for EqOp. *)
+Instance pure_eqop v1 v2 :
+  PureExec (vals_compare_safe v1 v2) 1
+    (BinOp EqOp (Val v1) (Val v2))
+    (Val $ LitV $ LitBool $ bool_decide (v1 = v2)) | 1.
+Proof.
+  intros Hcompare.
+  cut (bin_op_eval EqOp v1 v2 = Some $ LitV $ LitBool $ bool_decide (v1 = v2)).
+  { intros. revert Hcompare. solve_pure_exec. }
+  rewrite /bin_op_eval /= decide_True //.
+Qed.
 
 Instance pure_if_true e1 e2 : PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
 Proof. solve_pure_exec. Qed.
@@ -375,7 +386,7 @@ Proof.
 Qed.
 
 Lemma wp_cmpxchg_fail s E l q v' v1 v2 :
-  val_for_compare v' ≠ val_for_compare v1 → vals_cmpxchg_compare_safe v' v1 →
+  v' ≠ v1 → vals_compare_safe v' v1 →
   {{{ ▷ l ↦{q} v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
   {{{ RET PairV v' (LitV $ LitBool false); l ↦{q} v' }}}.
 Proof.
@@ -386,7 +397,7 @@ Proof.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 Lemma twp_cmpxchg_fail s E l q v' v1 v2 :
-  val_for_compare v' ≠ val_for_compare v1 → vals_cmpxchg_compare_safe v' v1 →
+  v' ≠ v1 → vals_compare_safe v' v1 →
   [[{ l ↦{q} v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
   [[{ RET PairV v' (LitV $ LitBool false); l ↦{q} v' }]].
 Proof.
@@ -398,7 +409,7 @@ Proof.
 Qed.
 
 Lemma wp_cmpxchg_suc s E l v1 v2 v' :
-  val_for_compare v' = val_for_compare v1 → vals_cmpxchg_compare_safe v' v1 →
+  v' = v1 → vals_compare_safe v' v1 →
   {{{ ▷ l ↦ v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
   {{{ RET PairV v' (LitV $ LitBool true); l ↦ v2 }}}.
 Proof.
@@ -410,7 +421,7 @@ Proof.
   iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
 Qed.
 Lemma twp_cmpxchg_suc s E l v1 v2 v' :
-  val_for_compare v' = val_for_compare v1 → vals_cmpxchg_compare_safe v' v1 →
+  v' = v1 → vals_compare_safe v' v1 →
   [[{ l ↦ v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
   [[{ RET PairV v' (LitV $ LitBool true); l ↦ v2 }]].
 Proof.
@@ -534,7 +545,7 @@ Proof.
 Qed.
 
 Lemma wp_resolve_cmpxchg_suc s E l (p : proph_id) (pvs : list (val * val)) v1 v2 v :
-  vals_cmpxchg_compare_safe v1 v1 →
+  vals_compare_safe v1 v1 →
   {{{ proph p pvs ∗ ▷ l ↦ v1 }}}
     Resolve (CmpXchg #l v1 v2) #p v @ s; E
   {{{ RET (v1, #true) ; ∃ pvs', ⌜pvs = ((v1, #true)%V, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦ v2 }}}.
@@ -547,7 +558,7 @@ Proof.
 Qed.
 
 Lemma wp_resolve_cmpxchg_fail s E l (p : proph_id) (pvs : list (val * val)) q v' v1 v2 v :
-  val_for_compare v' ≠ val_for_compare v1 → vals_cmpxchg_compare_safe v' v1 →
+  v' ≠ v1 → vals_compare_safe v' v1 →
   {{{ proph p pvs ∗ ▷ l ↦{q} v' }}}
     Resolve (CmpXchg #l v1 v2) #p v @ s; E
   {{{ RET (v', #false) ; ∃ pvs', ⌜pvs = ((v', #false)%V, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦{q} v' }}}.
@@ -582,7 +593,7 @@ Proof.
 Qed.
 
 Lemma wp_load_offset_vec s E l sz (off : fin sz) (vs : vec val sz) :
-  {{{ ▷ l ↦∗ vs }}} ! #(l +ₗ off) @ s; E {{{ RET (vs !!! off); l ↦∗ vs }}}.
+  {{{ ▷ l ↦∗ vs }}} ! #(l +ₗ off) @ s; E {{{ RET vs !!! off; l ↦∗ vs }}}.
 Proof. apply wp_load_offset. by apply vlookup_lookup. Qed.
 
 Lemma wp_store_offset s E l off vs v :
@@ -604,8 +615,8 @@ Qed.
 
 Lemma wp_cmpxchg_suc_offset s E l off vs v' v1 v2 :
   vs !! off = Some v' →
-  val_for_compare v' = val_for_compare v1 →
-  vals_cmpxchg_compare_safe v' v1 →
+  v' = v1 →
+  vals_compare_safe v' v1 →
   {{{ ▷ l ↦∗ vs }}}
     CmpXchg #(l +ₗ off) v1 v2 @ s; E
   {{{ RET (v', #true); l ↦∗ <[off:=v2]> vs }}}.
@@ -617,8 +628,8 @@ Proof.
 Qed.
 
 Lemma wp_cmpxchg_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
-  val_for_compare (vs !!! off) = val_for_compare v1 →
-  vals_cmpxchg_compare_safe (vs !!! off) v1 →
+  vs !!! off = v1 →
+  vals_compare_safe (vs !!! off) v1 →
   {{{ ▷ l ↦∗ vs }}}
     CmpXchg #(l +ₗ off) v1 v2 @ s; E
   {{{ RET (vs !!! off, #true); l ↦∗ vinsert off v2 vs }}}.
@@ -629,8 +640,8 @@ Qed.
 
 Lemma wp_cmpxchg_fail_offset s E l off vs v0 v1 v2 :
   vs !! off = Some v0 →
-  val_for_compare v0 ≠ val_for_compare v1 →
-  vals_cmpxchg_compare_safe v0 v1 →
+  v0 ≠ v1 →
+  vals_compare_safe v0 v1 →
   {{{ ▷ l ↦∗ vs }}}
     CmpXchg #(l +ₗ off) v1 v2 @ s; E
   {{{ RET (v0, #false); l ↦∗ vs }}}.
@@ -644,8 +655,8 @@ Proof.
 Qed.
 
 Lemma wp_cmpxchg_fail_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
-  val_for_compare (vs !!! off) ≠ val_for_compare v1 →
-  vals_cmpxchg_compare_safe (vs !!! off) v1 →
+  vs !!! off ≠ v1 →
+  vals_compare_safe (vs !!! off) v1 →
   {{{ ▷ l ↦∗ vs }}}
     CmpXchg #(l +ₗ off) v1 v2 @ s; E
   {{{ RET (vs !!! off, #false); l ↦∗ vs }}}.

theories/heap_lang/proofmode.v

@@ -65,6 +65,12 @@ Ltac wp_finish :=
   pm_prettify.        (* prettify ▷s caused by [MaybeIntoLaterNEnvs] and
                          λs caused by wp_value *)
 
+Ltac solve_vals_compare_safe :=
+  (* The first branch is for when we have [vals_compare_safe] in the context.
+     The other two branches are for when either one of the branches reduces to
+     [True] or we have it in the context. *)
+  fast_done || (left; fast_done) || (right; fast_done).
+
 (** The argument [efoc] can be used to specify the construct that should be
 reduced. For example, you can write [wp_pure (EIf _ _ _)], which will search
 for an [EIf _ _ _] in the expression, and reduce it.
@@ -81,7 +87,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
       unify e' efoc;
       eapply (tac_wp_pure _ _ _ _ (fill K e'));
       [iSolveTC                       (* PureExec *)
-      |try fast_done                  (* The pure condition for PureExec *)
+      |try solve_vals_compare_safe    (* The pure condition for PureExec -- handles trivial goals, including [vals_compare_safe] *)
       |iSolveTC                       (* IntoLaters *)
       |wp_finish                      (* new goal *)
       ])
@@ -282,15 +288,15 @@ Lemma tac_wp_cmpxchg Δ Δ' Δ'' s E i K l v v1 v2 Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
-  vals_cmpxchg_compare_safe v v1 →
-  (val_for_compare v = val_for_compare v1 →
+  vals_compare_safe v v1 →
+  (v = v1 →
    envs_entails Δ'' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E {{ Φ }})) →
-  (val_for_compare v ≠ val_for_compare v1 →
+  (v ≠ v1 →
    envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E {{ Φ }})) →
   envs_entails Δ (WP fill K (CmpXchg (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}).
 Proof.
   rewrite envs_entails_eq=> ???? Hsuc Hfail.
-  destruct (decide (val_for_compare v = val_for_compare v1)) as [Heq|Hne].
+  destruct (decide (v = v1)) as [Heq|Hne].
   - rewrite -wp_bind. eapply wand_apply.
     { eapply wp_cmpxchg_suc; eauto. }
     rewrite into_laterN_env_sound -later_sep /= {1}envs_simple_replace_sound //; simpl.
@@ -303,15 +309,15 @@ Qed.
 Lemma tac_twp_cmpxchg Δ Δ' s E i K l v v1 v2 Φ :
   envs_lookup i Δ = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ = Some Δ' →
-  vals_cmpxchg_compare_safe v v1 →
-  (val_for_compare v = val_for_compare v1 →
+  vals_compare_safe v v1 →
+  (v = v1 →
    envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E [{ Φ }])) →
-  (val_for_compare v ≠ val_for_compare v1 →
+  (v ≠ v1 →
    envs_entails Δ (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E [{ Φ }])) →
   envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
 Proof.
   rewrite envs_entails_eq=> ??? Hsuc Hfail.
-  destruct (decide (val_for_compare v = val_for_compare v1)) as [Heq|Hne].
+  destruct (decide (v = v1)) as [Heq|Hne].
   - rewrite -twp_bind. eapply wand_apply.
     { eapply twp_cmpxchg_suc; eauto. }
     rewrite /= {1}envs_simple_replace_sound //; simpl.
@@ -325,7 +331,7 @@ Qed.
 Lemma tac_wp_cmpxchg_fail Δ Δ' s E i K l q v v1 v2 Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
-  val_for_compare v ≠ val_for_compare v1 → vals_cmpxchg_compare_safe v v1 →
+  v ≠ v1 → vals_compare_safe v v1 →
   envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E {{ Φ }}) →
   envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E {{ Φ }}).
 Proof.
@@ -336,7 +342,7 @@ Proof.
 Qed.
 Lemma tac_twp_cmpxchg_fail Δ s E i K l q v v1 v2 Φ :
   envs_lookup i Δ = Some (false, l ↦{q} v)%I →
-  val_for_compare v ≠ val_for_compare v1 → vals_cmpxchg_compare_safe v v1 →
+  v ≠ v1 → vals_compare_safe v v1 →
   envs_entails Δ (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E [{ Φ }]) →
   envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
 Proof.
@@ -349,7 +355,7 @@ Lemma tac_wp_cmpxchg_suc Δ Δ' Δ'' s E i K l v v1 v2 Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
-  val_for_compare v = val_for_compare v1 → vals_cmpxchg_compare_safe v v1 →
+  v = v1 → vals_compare_safe v v1 →
   envs_entails Δ'' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E {{ Φ }}) →
   envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E {{ Φ }}).
 Proof.
@@ -362,7 +368,7 @@ Qed.
 Lemma tac_twp_cmpxchg_suc Δ Δ' s E i K l v v1 v2 Φ :
   envs_lookup i Δ = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ = Some Δ' →
-  val_for_compare v = val_for_compare v1 → vals_cmpxchg_compare_safe v v1 →
+  v = v1 → vals_compare_safe v v1 →
   envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E [{ Φ }]) →
   envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
 Proof.
@@ -530,12 +536,6 @@ Tactic Notation "wp_store" :=
   | _ => fail "wp_store: not a 'wp'"
   end.
 
-Ltac solve_vals_cmpxchg_compare_safe :=
-  (* The first branch is for when we have [vals_cmpxchg_compare_safe] in the context.
-     The other two branches are for when either one of the branches reduces to
-     [True] or we have it in the context. *)
-  fast_done || (left; fast_done) || (right; fast_done).
-
 Tactic Notation "wp_cmpxchg" "as" simple_intropattern(H1) "|" simple_intropattern(H2) :=
   let solve_mapsto _ :=
     let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
@@ -549,7 +549,7 @@ Tactic Notation "wp_cmpxchg" "as" simple_intropattern(H1) "|" simple_intropatter
     [iSolveTC
     |solve_mapsto ()
     |pm_reflexivity
-    |try solve_vals_cmpxchg_compare_safe
+    |try solve_vals_compare_safe
     |intros H1; wp_finish
     |intros H2; wp_finish]
   | |- envs_entails _ (twp ?E ?e ?Q) =>
@@ -558,7 +558,7 @@ Tactic Notation "wp_cmpxchg" "as" simple_intropattern(H1) "|" simple_intropatter
       |fail 1 "wp_cmpxchg: cannot find 'CmpXchg' in" e];
     [solve_mapsto ()
     |pm_reflexivity
-    |try solve_vals_cmpxchg_compare_safe
+    |try solve_vals_compare_safe
     |intros H1; wp_finish
     |intros H2; wp_finish]
   | _ => fail "wp_cmpxchg: not a 'wp'"
@@ -577,7 +577,7 @@ Tactic Notation "wp_cmpxchg_fail" :=
     [iSolveTC
     |solve_mapsto ()
     |try (simpl; congruence) (* value inequality *)
-    |try solve_vals_cmpxchg_compare_safe
+    |try solve_vals_compare_safe
     |wp_finish]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
@@ -585,7 +585,7 @@ Tactic Notation "wp_cmpxchg_fail" :=
       |fail 1 "wp_cmpxchg_fail: cannot find 'CmpXchg' in" e];
     [solve_mapsto ()
     |try (simpl; congruence) (* value inequality *)
-    |try solve_vals_cmpxchg_compare_safe
+    |try solve_vals_compare_safe
     |wp_finish]
   | _ => fail "wp_cmpxchg_fail: not a 'wp'"
   end.
@@ -604,7 +604,7 @@ Tactic Notation "wp_cmpxchg_suc" :=
     |solve_mapsto ()
     |pm_reflexivity
     |try (simpl; congruence) (* value equality *)
-    |try solve_vals_cmpxchg_compare_safe
+    |try solve_vals_compare_safe
     |wp_finish]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
@@ -613,7 +613,7 @@ Tactic Notation "wp_cmpxchg_suc" :=
     [solve_mapsto ()
     |pm_reflexivity
     |try (simpl; congruence) (* value equality *)
-    |try solve_vals_cmpxchg_compare_safe
+    |try solve_vals_compare_safe
     |wp_finish]
   | _ => fail "wp_cmpxchg_suc: not a 'wp'"
   end.