编译器前向模拟

前向模拟跟着源程序的录像向前播放。源每走一格，目标可以走一格、展开成数格，或在源格只是被优化掉的静默行政动作时暂时不走。关系 $R$ 不要求两边寄存器和临时量同名，只要求目标状态仍正确表示源状态的可观察部分。

良基度量是一只不能无限下降的沙漏。它允许有限次零步匹配，又阻止证明者把真正的无限工作都藏成“目标无需行动”。度量必须随每次停顿严格下降；只说优化最终会赶上，或使用普通自然数但不证明下降，都没有完成进展责任。

源语言把 “skip; c” 先走一步化为 $c$，目标在编译时已删除 skip。令 $R({\mathrm{skip}}^n;c,q)$ 表示 $q$ 是 $c$ 的目标代码，并取 $\mu =n$。源删除一个前导 skip 时，目标零步，度量从 $n$ 降到 $n-1$；源开始执行 $c$ 后，目标走相应实步。因为自然数良基，不可能无限次用同一目标状态掩盖源进展。

指令展开则给出正步例。源一步执行 $r:=(x+4)\times 8$，目标先执行 $t:=x+4$ 再左移三位；若两层都按 $w$ 位模算术解释，两个目标步的组合与源一步同值。关系在中间状态可以记住“已算出 $x+4$、尚未移位”的阶段索引，最后恢复主状态关系。

反例揭示包含方向：源初态只有一条标为 $a$ 的边到返回 $0$；目标除同一条边外还多一条 $b$ 边到返回 $1$。每个源步仍能在目标匹配，所以前向模拟成立，但目标新增了行为 $b,1$，不满足目标行为包含于源。若目标语义确定且源语义具相应 receptiveness，并满足事件与终态条件，可由标准定理把前向模拟转成后向模拟；缺少这些假设时不得宣称二者等价。

前向模拟易按源语义规则归纳：每种源指令只需展示目标生成代码怎样走到相关状态。多个阶段的前向模拟可在迹拼接与停顿度量兼容时复合；中间层若隐藏事件，复合前必须证明事件投影一致。

CompCert 的许多单个 pass 使用这种源步到目标多步的证明形状，再利用源的 receptiveness 与目标的 determinacy 等元性质取得整编译器需要的行为改进结论。编译器后向模拟公理库编译器后向模拟Compiler backward simulation · Backward simulation proof for compilers · 编译正确性的后向模拟从目标执行步反向要求源语义给出同迹匹配，以直接排除编译结果新增源程序不允许的行为。直接从目标步出发，证明义务和处理非确定性的方式不同；两者互为对照，而非无条件同义词。

有限终止执行可对源步数归纳，连接每段目标 $\stackrel{t}{\Rightarrow }$；无限执行则还要证明这些有限匹配能形成一条无限目标路径，且不会在某个有限目标前缀后只靠关系选择“重新开始”。正步条件或良基停顿度量正是这项提升的关键。迹上若允许 silent 事件擦除，还需证明投影与拼接相容。