语义保持的编译器阶段

语义保持不是要求源、目标逐条指令相同，而是要求外部观察者无法看到契约禁止的新结果。优化可以删除临时量、合并基本块或把一条指令扩成数步；状态形状和步数因此不同。证明需要一座桥，把两边状态及若干步对应起来，最终比较完整行为。

“保持”也不总是双向相等。源语言可能允许表达式求值顺序的多种结果，编译器固定其中一种，这是减少非确定性，仍满足目标行为包含于源行为。反过来，若目标新增一个崩溃结果，即使它还保留所有正常结果，也破坏上述精化方向。

设源 IR 的常量计算分两步：

这里假定 $t,x,y$ 是不同的变量；$\rho (x)$ 是初态中 $x$ 的值，第二次更新必须保留第一次写入的 $t$。常量折叠、传播并删除死临时量后，目标直接含 $y:=5\times x;\mathrm{return}y$。若整数运算均为同一宽度的模运算且赋值无可见事件，源的第一步可由目标零步匹配，第二步由一次目标步匹配，随后返回相同位串。

两边最终环境并不完全相同：源更新了 $t$，目标可能没有。因此状态关系应要求可观察变量相等，并允许死临时量 $t$ 不同；若后续又读取 $t$，这个忽略就不合法。减少内部步能够保持观察，依赖的是“该临时量此后确实不用”的条件，而不只是算术恒等式。

边界例取 $0\times \mathrm{load}(p)\mapsto 0$。在纯数学中等式成立；若读取 $p$ 可能越界 trap、触发 volatile 设备或参与原子顺序，目标删除了源的可见事件或错误，便不是同一契约下的语义保持。类似地，把有符号除法替换为右移可能对负数采用不同舍入方向，几个正数测试全部通过也无法覆盖反例。

回归测试只检查有限输入和有限运行。即使一百万次测试都相等，也不能推出所有状态、路径、发散执行与环境交互上的集合包含。测试适合发现实现错误，语义定理则量化全部合法程序和执行；两者作用互补，不能互相改名。

未定义行为还必须说明采用哪种放宽。若采用本文的“已产生事件前缀之后任意延续”模型，源在第十步越界，并不允许目标抹去前九步已经规定的可见事件。若某语言规范直接对任何会触发 UB 的整个执行不作要求，则不能从规范推出这种前缀保证。精化定理必须固定其中一种解释；不能把一个模型中的前缀结论自动推广到所有 C 编译器契约。

若每个阶段 $C_i$ 都在相容观察下满足行为精化，则集合包含的传递性给出整条编译流水线

组合要求相邻 IR 对事件、返回和错误的编码一致；一层把 trap 当事件、下一层把它当 UB，会让形式上可复合的符号失去实际含义。

常用证明方法包括编译器前向模拟公理库编译器前向模拟Compiler forward simulation · Forward simulation proof for compilers · 编译正确性的前向模拟以源状态到目标状态的关系逐步匹配每个源执行步，并用正步进展或良基度量约束静默停顿。、编译器后向模拟公理库编译器后向模拟Compiler backward simulation · Backward simulation proof for compilers · 编译正确性的后向模拟从目标执行步反向要求源语义给出同迹匹配，以直接排除编译结果新增源程序不允许的行为。、逻辑关系和翻译验证公理库翻译验证Translation validation · Per-run translation validation · 编译翻译验证对每次编译产生的源程序、目标程序或证书运行可靠检查器，以实例化地建立本次翻译的语义保持。。它们是建立语义保持的不同证据接口，并不等于性质本身。选择方法应由确定性、非确定性、内部停顿与阶段实现的可信边界决定。