翻译验证

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

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

取字宽 $w\ge 3$，常量 $2,3,5,6$ 均可合法编码，加法与乘法都取模 $2^w$。源块先执行 $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 接受错误翻译。随机测试源、目标在若干输入相等可以协助筛错，却没有给出对所有输入和路径的可靠性定理。

一个能完整运行的有限位算术验证器 ​

下面把通用契约收紧到可以穷举的片段，给出验证器的全部义务。它不需要证书，等价于取 $c=()$。源、目标都使用同一语言 ${\mathcal{I}}_w$，字宽 $w\ge 1$，输入为固定顺序的 $k$ 个 $w$ 位数。令

值类型只有 ${\mathbb{B}}_w$ 与 Bool。加、减、乘均取模 $2^w$；相等按位串相等，${<}_u$ 按上述非负整数比较。这个约定与标准固定大小位向量的加、乘和无符号比较一致。[2] 不包含除法、内存、调用、异常、poison、undef 或溢出标志；全部允许的原语都是全定义函数。

程序是有限基本块表和一个入口。每个变量有固定声明类型，每条普通指令为

算术与比较的两个输入均为 ${\mathbb{B}}_w$；比较结果为 Bool。常量带类型，位常量须在 ${\mathbb{B}}_w$ 内。每块末尾恰有一个终结指令：goto L、br b L R 或 return x，其中 $b$ 为 Bool，返回 $x$ 为 ${\mathbb{B}}_w$。块内按顺序求值，分支只执行选中的后继。允许对同名变量重复赋值，也允许两程序拥有不同的块数和临时量；并不先假定它们已是 SSA。

良构检查不能只查操作码 ​

Check(P) 依次完成以下有限检查，任何失败都返回拒绝原因。

1. 检查语法、变量和块标识唯一声明、正字宽、合法常量、操作码和指令类型；输入声明及返回类型与共同接口一致。
2. 入口标识必须属于块表，因此块表非空；每个跳转目标都存在。由入口遍历能到达全部块。对全部边做拓扑排序理路拓扑排序Topological sort给有向无环图顶点排列线性次序，使每条边从前指向后。，若有环则拒绝。没有后继的块必须以 return 结束，不能默默掉到文件末尾。
3. 按拓扑次序检查每次读取前已确定赋值。入口的已定义集合为输入变量。其他块 $B$ 的入口集合为

扫描普通指令时，先检查全部右侧变量在当前集合，再加入左侧；末尾分支和返回的读取也要检查。所得集合即 $D_{\mathrm{out}}(B)$。全部块可达且图无环，保证非入口块的前驱集合非空、各前驱集合已计算。类型声明本身不等于已赋值，不能拿“变量表里有它”替代这个交集检查。

这套 definite-assignment 检查可以保守地拒绝只在不可行语法路径上未赋值的程序；本页接受的片段明确定义为通过上述检查的程序，不宣称识别所有语义上安全的图。

执行引理。 对每个通过 Check 的程序和每个合法输入，Run(P,input) 都有且只有一个返回值。证明按拓扑执行路径归纳：入口输入有值；若实际从 $A$ 进入 $B$，交集中的变量都属于 $D_{\mathrm{out}}(A)$，因而已有值。指令类型正确且原语全定义，逐条执行不阻塞；布尔分支唯一选边。每次跨块使拓扑编号严格增加，所以至多访问块数那么多个块，最终只能到 return。每块指令有限，执行整体终止。

可以把这一引理对应的解释器写成

Run(P, input):                  // P has already passed Check
    env := bind(P.inputs, input)
    block := P.entry
    repeat:
        for instr in P[block].ordinary:
            env[instr.dst] := EvalPrimitive(instr, env, P.width)
        match P[block].terminator:
            return x: return env[x]
            goto L:   block := L
            br b L R: block := (L if env[b] else R)

EvalPrimitive 对上面七类指令逐项解释，算术写回时取模；程序里的重复循环是解释器控制结构，不表示被解释图含环。终止证明来自拓扑编号，不能以任意燃料耗尽后返回一个默认数字代替它。

验证器与接受可靠性 ​

固定词典序枚举全部 ${\mathbb{B}}_w^k$。同接口程序的验证器为

Validate(P, Q):
    if interfaces differ: return reject("interface")
    if Check(P) fails or Check(Q) fails:
        return reject("outside the checked fragment")
    for input in all tuples in B_w^k, in lexicographic order:
        source := Run(P, input)
        target := Run(Q, input)
        if source != target:
            return reject(input, source, target)
    return accept

$k=0$ 时枚举恰含一个空元组，不能误实现为零次检查。输入总数为 $2^{wk}$，每次执行由引理终止，故验证器对每个有限输入程序都终止。它可能极慢，但这里没有把抽样、超时或“尚未找到反例”写成接受。

定理是

任取 $\mathbf{x}$。完整枚举必访问它；接受说明该轮两返回值相等，而执行引理保证比较的是两程序的真实唯一观察。对所有输入量化即得定理。这里每个输入的行为集合都是单元素“正常返回该位串”，所以相等尤其蕴含目标行为包含于源行为。没有偷偷漏证发散：无环、无调用、全定义指令及良构性已经排除了片段内的发散和错误。

反过来，对两个通过 Check 且同接口的程序，若所有输入返回值都相等，则枚举从不走拒绝分支，最终接受。因此该验证器在所声明片段内既可靠又完备。通用程序等价的不可判定性不妨碍这个有限结果；若把片段换成一般程序，不能再照搬此结论。[1]

十六个输入中的溢出反例 ​

取 $w=4,k=1$。下列源程序 $P$ 的 1,3,7,15 都是四位常量；为简洁，立即数可直接出现在算术右侧，等价于先用常量指令绑定。

P.E: y := x + 1; b := (y <_u x); br b T F
P.T: return 7
P.F: z := y * 3; return z

同样，return 7 是把常量绑定到新临时量再返回的简写。因为 $x$ 只有 $0,\dots ,15$，$x\le 14$ 时 $y=x+1>x$，$x=15$ 时 $y=0<x$。因此正确候选 $Q$ 可以改写条件并展开乘法：

Q.E: b := (x = 15); br b T F
Q.T: return 7
Q.F: t := x * 3; z := t + 3; return z

加法和乘法同在模16环中，$(x+1)3=3x+3(\mathrm{mod}16)$，所以两个分支均相同。验证器会穷举16项后接受。现在考虑错误候选 $Q_{\mathrm{bad}}$：优化器误认为“加一总使无符号数增大”，直接删除 true 分支，只返回 $3x+3(\mathrm{mod}16)$。

表只展示六项，验证器实际检查全部16项，首次差异为 (input=15, source=7, target=0)。这同时说明边界输入必须进入枚举、无符号比较不能当作整数不溢出比较，以及相同 CFG 不是接受的前提：错误候选即使只剩一个块，仍可解析、检查和拒绝。

另一种拒绝发生在执行之前。例如目标的一条分支跳往不存在的块，或在某个前驱没有给返回变量赋值，Check 就拒绝；这不是一个“两个返回值不等”的见证。应区分结构/接口不支持与已找到语义反例，两个理由都不能作为发布许可。

证明与实现的信任边界 ​

上述证明覆盖的是给定的数学检查器与解释器。具体实现还需忠实完成解析、字宽与模运算、CFG 和赋值检查、完整元组枚举及结果比较，并确保最终使用的正是检查过的程序对象。若用宿主有符号溢出、错误移位或浮点数代替精确位运算，正文的代数证明不能补救实现偏差。

循环交换的实际IR检查器理路循环交换Loop interchange · Loop permutation · 循环置换置换矩形循环的嵌套顺序，生成实际For代码，再以实例一一覆盖与依赖边方向验证每次变换。提供另一种已限定接口：固定尺寸和视图，重新核全部实例一一覆盖与数组冲突边前向，利用相邻独立交换证明对所有整数初始内存保持终态。它不枚举内存值；目标循环、尺寸或视图变更后须重新验证。循环分块理路循环分块Loop tiling · Loop blocking · 循环铺块以块循环和裁边循环覆盖每个迭代点，再检查跨块依赖；生成可运行的非整除分块代码，分开证明覆盖、语义与性能条件。还必须生成并核查min裁边，不能用覆盖正确代替跨块顺序正确。

实际验证器可用符号执行与求解器缩短穷举；这会引入新的公式生成和求解结果可信性义务。预算耗尽只能拒绝或返回明确的未知结果，不能接受。工业 IR 中的内存、poison、UB、异常、外部调用与循环也要各自进入语义与证明；这里给出的16输入检查没有声称覆盖它们。文献中的经过证明的验证器，进一步把检查器的可靠性在证明助理中机械化；本页的纸面证明与可复算算法不冒称已做那项机械化工作。[1]

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

逐阶段组合还要求阶段一的目标语义与阶段二当作源语义的版本完全一致，包括整数宽度、外部事件、调用约定和 UB 解释。两个 checker 即使各自可靠，若通过不同解析器理解同一中间文件，集合包含也无法首尾相接。