Operational semantics of pre-drop-elab code?

[RalfJung]

How do we describe the exact semantics of pre-drop-elab code, and what is the specification for drop elab correctness?

This recently came up in rust-lang/rust#91029 (Cc @arielb1 @JakobDegen), but seems to warrant a separate thread in this repo. Broadly speaking there are two options:

1. There is a direct operational semantics for pre-drop-elab code. Drop elaboration is just an optimization (or transformation into a different language dialect), and is allowed to be a strict refinement of the original code (i.e., it can lose some UB).
2. Drop elaboration defines the semantics, i.e., "semantics by elaboration" (similar to how we plan to define a lot of surface Rust semantics by elaboration into something like MiniRust).

If the answer is (1), then Miri should be changed to (by default) run pre-drop-elab MIR directly using their semantics. But what exactly would those semantics be? They'd definitely involve magic tables storing drop flags.

One important point to figure out as part of this discussion is: is the current drop elaboration already suitable as a definition, or are there some cases where it is a strict refinement of the original semantics?