Allow comparing even more values in CAS by making things more consistent

tests/heap_lang.ref

@@ -68,11 +68,6 @@
     let: "val2" := fun2 "val1" in
     let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
   {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}
-"not_cas_compare_safe"
-     : string
-The command has indeed failed with message:
-Ltac call to "wp_cas_suc" failed.
-Tactic failure: wp_cas_suc: Values are not safe to compare for CAS.
 "not_cas"
      : string
 The command has indeed failed with message:

tests/heap_lang.v

@@ -166,13 +166,6 @@ End printing_tests.
 Section error_tests.
   Context `{heapG Σ}.
 
-  Check "not_cas_compare_safe".
-  Lemma not_cas_compare_safe (l : loc) (v : val) :
-    l ↦ v -∗ WP CAS #l v v {{ _, True }}.
-  Proof.
-    iIntros "H↦". Fail wp_cas_suc.
-  Abort.
-
   Check "not_cas".
   Lemma not_cas :
     (WP #() {{ _, True }})%I.

theories/heap_lang/lang.v

@@ -68,9 +68,6 @@ Inductive expr :=
 
 Bind Scope expr_scope with expr.
 
-Notation NONE := (InjL (Lit LitUnit)) (only parsing).
-Notation SOME x := (InjR x) (only parsing).
-
 Fixpoint is_closed (X : list string) (e : expr) : bool :=
   match e with
   | Var x => bool_decide (x ∈ X)
@@ -99,9 +96,6 @@ Inductive val :=
 
 Bind Scope val_scope with val.
 
-Notation NONEV := (InjLV (LitV LitUnit)) (only parsing).
-Notation SOMEV x := (InjRV x) (only parsing).
-
 Fixpoint of_val (v : val) : expr :=
   match v with
   | RecV f x e => Rec f x e
@@ -122,6 +116,38 @@ Fixpoint to_val (e : expr) : option val :=
   | _ => None
   end.
 
+(** We assume the following encoding of values to 64-bit words: The least 3
+significant bits of every word are a "tag", and we have 61 bits of payload,
+which is enough if all pointers are 8-byte-aligned (common on 64bit
+architectures). The tags have the following meaning:
+
+0: Payload is the data for a LitV (LitInt _).
+1: Payload is the data for a InjLV (LitV (LitInt _)).
+2: Payload is the data for a InjRV (LitV (LitInt _)).
+3: Payload is the data for a LitV (LitLoc _).
+4: Payload is the data for a InjLV (LitV (LitLoc _)).
+4: Payload is the data for a InjRV (LitV (LitLoc _)).
+6: Payload is one of the following finitely many values, which 61 bits are more
+   than enough to encode:
+   LitV LitUnit, InjLV (LitV LitUnit), InjRV (LitV LitUnit),
+   LitV (LitBool _), InjLV (LitV (LitBool _)), InjRV (LitV (LitBool _)).
+7: Value is boxed, i.e., payload is a pointer to some read-only memory area on
+   the heap which stores whether this is a RecV, PairV, InjLV or InjRV and the
+   relevant data for those cases. However, the boxed representation is never
+   used if any of the above representations could be used.
+
+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 val_is_unboxed (v : val) : Prop :=
+  match v with
+  | LitV _ => True
+  | InjLV (LitV _) => True
+  | InjRV (LitV _) => True
+  | _ => False
+  end.
+
 (** The state: heaps of vals. *)
 Definition state := gmap loc val.
 
@@ -367,53 +393,13 @@ Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
   | _, _ => None
   end.
 
-(** Return whether it is possible to use CAS to compare vl (current value) with
-v1 (netest value).
-
-We assume the following encoding of values to 64-bit words: The least 3
-significant bits of every word are a "tag", and we have 61 bits of payload,
-which is enough if all pointers are 8-byte-aligned (commong on 64bit
-architectures). The tags have the following meaning:
-
-0: Payload is one of the following finitely many values, which 61 bits are more
-   than enough to encode: LitV LitUnit, LitV (LitBool _), NONEV, SOMEV (LitV
-   LitUnit), SOMEV (LitV (LitBool _)).
-1: Payload is the data for a LitV (LitInt _).
-2: Payload is the data for a SOMEV (LitV (LitInt _)).
-3: Payload is the data for a LitV (LitLoc _).
-4: Payload is the data for a SOMEV (LitV (LitLoc _)).
-5: Value is boxed, i.e., payload is a pointer to some read-only memory area on
-   the heap which stores whether this is a RecV, PairV, InjLV or InjRV and the
-   relevant data for those cases. However, the boxed representation is never
-   used if any of the above representations could be used.
-6: Unused.
-7: Unused.
-
-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. It also justifies the comparisons allowed for CAS: Whenever
-[vals_cas_compare_safe vl v1] holds, equality of the one-word representation of
-[vl] and [v1] is equivalent to equality of the abstract value represented. This
-is clear for [LitV _ == LitV _] and [SOMEV (LitV _) == SOMEV (LitV _)] because
-none of these are boxed. For [NONEV == v], we can't actually atomically load and
-compare the data for boxed values, but that's okay because we only have to know
-if they are equal to [NONEV] which is distinct from all boxed values.
- *)
+(** CAS just compares the word-sized representation of the two values, it cannot
+look 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_cas_compare_safe (vl v1 : val) : Prop :=
-  match vl, v1 with
-  (* We allow comparing literals with each other, also when wrapped in a SOMEV. *)
-  | LitV _, LitV _ => True
-  | SOMEV (LitV _), SOMEV (LitV _) => True
-  (* We allow comparing NONEV to anything. *)
-  | NONEV, _ => True
-  | _, NONEV => True
-  (* We don't allow comparing anything else. *)
-  | _, _ => False
-  end.
-(** Just a sanity check. *)
-Lemma vals_cas_compare_safe_sym vl v1 :
-  vals_cas_compare_safe vl v1 → vals_cas_compare_safe v1 vl.
-Proof. rewrite /vals_cas_compare_safe. repeat case_match; done. Qed.
+  val_is_unboxed vl ∨ val_is_unboxed v1.
+Arguments vals_cas_compare_safe !_ !_ /.
 
 Inductive head_step : expr → state → expr → state → list (expr) → Prop :=
   | BetaS f x e1 e2 v2 e' σ :

theories/heap_lang/lib/increment.v

@@ -39,7 +39,8 @@ Section increment.
     (* Prove the atomic shift for CAS *)
     iAuIntro. iApply (aacc_aupd with "AU"); first done.
     iIntros (x') "H↦".
-    iApply (aacc_intro with "[H↦]"); [solve_ndisj|simpl;by auto with iFrame|iSplit].
+    iApply (aacc_intro with "[H↦]"); [solve_ndisj| |iSplit].
+    { iFrame. simpl. auto. }
     { iIntros "[_ $] !> $ !> //". }
     iIntros ([]) "H↦ !>".
     destruct (decide (#x' = #x)) as [[= ->]|Hx].

theories/heap_lang/notation.v

@@ -144,6 +144,12 @@ Notation "e1 || e2" :=
   (If e1%E (Lit (LitBool true)) e2%E) (only parsing) : expr_scope.
 
 (** Notations for option *)
+Notation NONE := (InjL (Lit LitUnit)) (only parsing).
+Notation SOME x := (InjR x) (only parsing).
+
+Notation NONEV := (InjLV (LitV LitUnit)) (only parsing).
+Notation SOMEV x := (InjRV x) (only parsing).
+
 Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
   (Match e0 BAnon e1 x%bind e2)
   (e0, e1, x, e2 at level 200, only parsing) : expr_scope.

theories/heap_lang/proofmode.v

@@ -406,7 +406,7 @@ Tactic Notation "wp_cas_fail" :=
     [iSolveTC
     |solve_mapsto ()
     |try congruence
-    |fast_done || fail "wp_cas_fail: Values are not safe to compare for CAS"
+    |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 +415,7 @@ Tactic Notation "wp_cas_fail" :=
       |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
     [solve_mapsto ()
     |try congruence
-    |fast_done || fail "wp_cas_fail: Values are not safe to compare for CAS"
+    |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.
@@ -434,7 +434,7 @@ Tactic Notation "wp_cas_suc" :=
     [iSolveTC
     |solve_mapsto ()
     |try congruence
-    |fast_done || fail "wp_cas_suc: Values are not safe to compare for CAS"
+    |try (fast_done || left; fast_done || right; fast_done) (* vals_cas_compare_safe *)
     |pm_reflexivity
     |simpl; try wp_value_head]
   | |- envs_entails _ (twp ?E ?e ?Q) =>
@@ -444,7 +444,7 @@ Tactic Notation "wp_cas_suc" :=
       |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
     [solve_mapsto ()
     |try congruence
-    |fast_done || fail "wp_cas_suc: Values are not safe to compare for CAS"
+    |try (fast_done || left; fast_done || right; fast_done) (* vals_cas_compare_safe *)
     |pm_reflexivity
     |wp_expr_simpl; try wp_value_head]
   | _ => fail "wp_cas_suc: not a 'wp'"