Come up with a story for non-atomic, non-pure expressions
We currently have very poor support for expressions that depend on the state (either changing it, on only being safe for some states), and that do not reduce to a value in a single step - that are not atomic. We cannot use the atomic rule around them, so once ownership of the physical state has been put into an invariant, such expressions cannot be given a triple. Ouch.
@robbertkrebbers mentioned that such expressions do come up in languages he has studied. For example, calling a function will both push a stackframe (which is part of the global state) and expand the function body - the operation is hence neither atomic nor pure.
The best proposal on the table so far is to further strengthen (and complicate) the lifting lemmas, and make it possible for them to pull the physical state out of an invariant. That's kind of ugly though, it would mean that these lemmas deal with both the "physical state change" aspect of the reduction, and the "atomicity" aspect. The atomic rule of consequence can probably not be derived from this, and would remain a primitive. It would also be much nicer to use: The lifting lemmas "open" an invariant only around the first reduction step of an expression, not around the entire triple, so we don't even have nice notation for them.