Alternative definition of contextual refinement

See merge request !5

Prior to this change there was a bit of a mess in handling of types on
which you can do `CAS` and which you can compare by equality.
This change adds typing rules that allow `CAS` on any unboxed types.

Revert "Bump Iris (persistent mapsto)."

This reverts commit 7e770ada.