语义保持的编译器阶段

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

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

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

常量折叠目标直接含 $y:=5\times x$。若整数运算均为同一宽度的模运算且赋值无可见事件，源的第一步可由目标零步匹配，第二步由一次目标步匹配，最终返回相同位串。这里减少内部步不影响观察，但证明必须使用状态关系忽略死临时量 $t$。

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

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

源程序已触发 UB 与“编译器提前制造 UB”也要区分。若某输入的源执行在第十步才越界，目标不能在第一步、尚未匹配前九步可见事件时任意行动。行为顶部只从已到达 UB 的相关状态开始放宽；在此之前，模拟仍要保存事件前缀与状态不变量。

若每个阶段 $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 · 编译翻译验证对每次编译产生的源程序、目标程序或证书运行可靠检查器，以实例化地建立本次翻译的语义保持。。它们是建立语义保持的不同证据接口，并不等于性质本身。选择方法应由确定性、非确定性、内部停顿与阶段实现的可信边界决定。