Prop349: specify "as if" semantics
This came out of a discussion with @mikeperry about prop349.
I would like prop349 to specify "as-if" semantics. That is, implementations should behave "as if" the specified state machines existed. This way, we are not forced into a single correct implementation strategy for getting the code right.
I'm happy to make this change; I'm making this ticket so I don't forget, and so I can point at it and ask Mike if it's cool.