What is the operational spec for use expressions?

[RalfJung]

Looking at rust-lang/rust#139088 there seem to be some non-trivial things going on, with optimizations removing calls to user-defined functions, which is usually a no-go. We should figure out a solid story here and then ensure the implementation is consistent with that. If the story involves non-determinism (which seems likely), we should enable Miri to explore all non-deterministic options.

Tracking issue: rust-lang/rust#132290

Cc @spastorino @rust-lang/opsem