翻译验证

与其证明一座巨大工厂永远不会装错零件，翻译验证在每件成品出厂时核对它与订单。优化器可以使用复杂启发式甚至外部求解器，只要每次输出都附带足够证据，简单检查器就能确认这一个源—目标对没有新增行为。

这种分工把“找到优化”和“检查优化”分开。前者可不完备、依赖性能技巧，后者力求小、确定且有可靠性证明。它特别适合搜索算法复杂、但候选结果的验证条件清晰的阶段，例如寄存器着色、指令调度或局部等价检查。

源块先执行 $t:=2+3$，再执行 $y:=t\times x$；目标直接执行 $y:=5\times x$。证书把源入口关联到目标入口，并把源完成第一步、满足 $t=5$ 的状态仍关联到目标入口。checker 可计算位向量恒等式 $2+3=5$，确认源第一步是静默停顿，再检查双方乘法一步产生相同 $y$ 与内存。对任意 $x$，这组局部义务闭合，就得到本次变换的模拟。

若优化器误产出 $y:=6\times x$，取 $x=1$ 即破坏关系，可靠 checker 应拒绝。若目标重排了异常边而证书格式只描述正常 CFG，checker 即使验证所有普通块也不能推出完整语义；异常、trap、调用与发散必须在状态关系和边覆盖中出现。

边界还包括算法覆盖率。一个只理解常量折叠的验证器可能拒绝完全正确的循环展开，这是只影响完备性的假阴性。真正危险的是破坏 soundness 的假阳性：checker 接受错误翻译。随机测试源、目标在若干输入相等可以协助筛错，却没有给出对所有输入和路径的可靠性定理。

翻译验证不等于验证整个编译器。它证明的是“每个被接受的输出正确”；若构建脚本允许绕过 validator、证书与二进制配错，或拒绝后仍使用目标，端到端保证就断裂。部署流程必须把 accept 绑定到确切的源、目标、配置与语义版本。

验证器可采用前向模拟公理库编译器前向模拟Compiler forward simulation · Forward simulation proof for compilers · 编译正确性的前向模拟以源状态到目标状态的关系逐步匹配每个源执行步，并用正步进展或良基度量约束静默停顿。证书、后向模拟公理库编译器后向模拟Compiler backward simulation · Backward simulation proof for compilers · 编译正确性的后向模拟从目标执行步反向要求源语义给出同迹匹配，以直接排除编译结果新增源程序不允许的行为。证书、SMT 可证等价或专用校验条件。不同方法仍要落到同一观察契约。验证多个阶段时，可以逐阶段检查并组合精化，也可对源与最终目标做全局验证；前者定位清楚，后者可能发现跨阶段对应，但证书更难生成。

逐阶段组合还要求阶段一的目标语义与阶段二当作源语义的版本完全一致，包括整数宽度、外部事件、调用约定和 UB 解释。两个 checker 即使各自可靠，若通过不同解析器理解同一中间文件，集合包含也无法首尾相接。验证器的完备性仍非安全要求：正确优化被拒绝只影响可用性；但拒绝路径必须真的停止或回退到已验证结果。