heap_lang has always had a compare-and-set operation that just returns a bool indicating success or failure. In contrast, the typical operation provided in "real" languages is compare-and-swap, which returns the old value. Compare-and-set can be written with compare-and-swap, but not vice versa. So I propose we change heap_lang's primitive to be a compare-and-swap instead.

We need this in a case study to faithfully model RDCSS.

The advantage of this is that giving this operation a spec as a single Hoare triple is actually less annoying because one does not need to write the decision thing twice (see atomic_heap.v). This also merges the two reduction rules for CAS into one, so now we finally have exactly one rule per primitive.

The disadvantage is that CAS l v1 v2 = v1 (which is the way to test if the swap happened) is not atomic, so some proofs need adjustment. I tried giving this operation a "logically atomic" spec (not using the full logically atomic triples but the simpler ones that don't support aborts, which makes the spec strictly stronger and much easier to use), but while conceptually helpful it doesn't actually help with the Coq proofs (see counter.v).