"as if" is what semantically identical means. As I further clarified: "All observable and defined side effects should be identical otherwise you have a compiler bug."

The output program does what the input source code does. The abstraction is a precise translation and non-leaky, it just admits multiple possible internals. That does not make the translation any less precise.