Make CAS slightly more realistic

This restricts CAS to only be able to compare literals with literals, NONEV with NONEV and NONEV with SOMEV for a literal.

In particular, we can no longer CAS pairs.

added 1 commit

• 8ae0c062 - move option notation to lang.v so we can use it to define CAS compare safety

Compare with previous version

added 1 commit

• 6ac4c4eb - move option notation to lang.v so we can use it to define CAS compare safety

Compare with previous version

LGTM modulo the issue about reporting an error.

added 1 commit

• e97bbfe6 - wp_cas_fail/succ: Report error when proving vals_cas_compare_safe; fast_done is enough

Compare with previous version

resolved all discussions

added 1 commit

• 01663351 - wp_cas_fail/succ: Report error when proving vals_cas_compare_safe; fast_done is enough

Compare with previous version

Like this?

added 1 commit

• 43838a40 - test 'not a CAS' error message as well

Compare with previous version

LGTM.

I'm kind of interested if this break any existing developments, where one uses CAS in the wrong way ;).

But that's probably for the best!

I originally wanted to allow only SOMEV #l where l: loc, that turned out to break tests/one_shot.v... so I decided not to make it quite that realistic. ;)

mentioned in commit 6b0f3bfb

merged

I think this is a reasonable compromise indeed.

iris-examples broke: https://gitlab.mpi-sws.org/FP/iris-examples/-/jobs/15397

Couldn't look into it yet though.

By the way, shouldn't we change normal equality in the same way?

Wouldn't say so. This is a pure operation where non-atomically comparing by iterating over the structure is just fine.

Ok, let me more clear: shouldn't we make sure that equality can only be used in an atomic way when both operands satisfy the same condition as we have for CAS now.

Equality testing is pure. Whether it is atomic or not is not observable.