Reverting to old (stronger) definition of atomicity
In Iris 3.0 the definition of atomicity was changed to its new definition, i.e., roughly: e
is atomic if for any e'
such that e
reduces to e'
we have that e'
is stuck.
The old definition was: e
is atomic if for any e'
such that e
reduces to e'
we have that e'
is a value.
These two definition differ (the new version is strictly weaker) in cases where we are reasoning about facts that unlike WP
do not guarantee safety, e.g., IC
(if convergent predicates).