Allow comparing even more values in CAS by adding non-determinism

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: Represents 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.

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

This also changes the wp_cas tactics to not just give up when CAS-safety cannot be proven, but instead open a goal. That's more convenient if the user e.g. needs to do destruct to prove that goal.