There is an unsaved comment in progress. You will lose your changes if you continue. Are you sure you want to reopen the work item?
Currently, _(by_claim c, e) can be used only to read nonvolatile fields. We should be able to use it to also read volatile fields; indeed, we should be able to use it to read through an arbitrary pointer. The translation would just be
_(assert \forall \state s1,s2; \at(s1,\active_claim(c) && \full_stop()) && \at(s2,\active_claim(c) && \full_stop()) ==> \at(s1,e) == \at(s2,e))