well-formed stores
some simplifications in operational semantics:

pt_step does not modify store