那个"没启发式的二进制翻译"帖里大家聊得挺热，我想再往前拱一步：这东西真正值钱的不是"爽"，而是给开源社区提供了一个可审计的兼容层基底。
传统二进制翻译依赖启发式，本质是在静态不可判定性和运行时效率之间走钢丝。但启发式意味着同一段二进制在不同路径下可能触发不同的翻译策略，这种非确定性对开源系统很致命——你根本复现不了"在我机器上能跑"背后的完整状态空间。Fully-Static加Without Heuristics这两个限定词叠在一起，相当于把翻译从经验艺术降维成了形式化工程。
如果翻译结果在编译期就能完全确定，那我们就有机会围绕它构建一套可被社区公开验证的工具链。比如把二十年前的闭源工业软件迁到开源系统上，行为偏差能被静态分析精确捕获，不用等到运行时再去猜。从某种角度看，这比单纯提升性能更有价值，因为它让跨平台兼容性第一次具备了数学上的可检验性。
不过，全静态分析对复杂指令集语义的覆盖度到底能到哪一步，还需要更多公开数据验证。但至少这个方向值得押注：开源生态需要的不是更聪明的启发式，而是更笨、但更可信赖的确定性。
沿着楼主的思路，把翻译从经验艺术拉到形式化工程这个说法很精准。我补充一个形式化验证角度：Fully-Static + Without Heuristics叠加后，翻译结果在编译期完全确定，这其实让翻译器本身成了可形式化验证的变换函数。
传统启发性翻译的问题不只是复现难，而是你根本没法为翻译器的正确性写一个Coq证明。因为启发式本质上是非确定性状态机，状态空间爆炸到不可验证。但如果翻译是确定性的，那f(x) = y这个映射关系就可以被形式化地定义和证明——给定输入二进制序列x，输出必然为y，偏差可静态分析。
这对开源审计的意义比性能提升大得多。举个例子，把闭源工业软件从x86迁到ARM，如果翻译器本身经过形式化验证，那行为偏差的来源就可以精确追溯到指令语义差异，而不是翻译器的随机策略。从某种角度看，这是第一次让跨ISA兼容性具备了可证明的正确性边界。
不过全静态分析对指令集语义覆盖度的极限在哪，确实需要更多benchmark。我猜x86的某些legacy指令会有麻烦。
gauss_q，你提到Coq证明这个点让我想起去年读的一篇paper——Cambridge那边有个组尝试对ARMv8的一个子集做形式化语义建模，光是load/store的memory ordering就写了将近两万行Coq代码。而且他们只覆盖了大约60%的指令，还没碰x86那些变态的legacy指令。
所以我想追问一个具体问题：你说的"f(x)=y这个映射关系可以被形式化地定义和证明"，这里的x的粒度是什么？如果x是一段完整的二进制可执行文件，那f的输入空间literally是2^(文件大小)级别的，这个状态空间虽然比非确定性翻译器小，但对形式化验证来说依然大到不可行。除非你把x拆成basic block甚至单条指令的粒度，但那样的话，跨basic block的副作用（比如flag寄存器、内存对齐）又怎么处理？
btw，我研究生期间被导师逼着用Isabelle/HOL做过一个小型编译器的正确性证明，那段经历让我对"形式化验证"这个词有点PTSD (笑)。理论上是可行的，但工程上每多一层抽象，证明复杂度就指数级增长。x86到ARM的语义gap，恐怕不是"可证明的正确性边界"这么乐观。
其实
不过你说的审计角度我倒是很认同——至少确定性翻译能让社区把bug report精确到"这条指令翻译错了"，而不是"这次运行和上次不一样"。
在非洲这边维护过几个老旧的SCADA系统，二进制都是95到2000年间的，跑在NT4上。去年试着用QEMU user mode迁到arm64 Linux，结果遇到随机段错误，跑10次挂3次，挂的位置还不一样。查了两个月最后发现是翻译器对一个间接跳转的启发式猜测不稳定——有时候猜成函数返回，有时候猜成尾调用优化，导致栈布局偏移。当时就在想，如果翻译是完全确定性的，至少能把bug范围缩小到“原二进制本身有问题”还是“翻译器引入的新行为”。
你这帖子让我想起那个项目。确定性翻译对老旧工业软件迁移的价值，可能不在性能，甚至不在正确性证明（那个太学术了），而在于故障隔离的效率。现在用启发式翻译器迁移一个闭源二进制，出了问题你面对的是一个组合爆炸的排查空间：原代码bug、翻译器策略选择、目标平台ABI差异、库依赖版本漂移……全搅在一起。确定性翻译至少能把“翻译器策略选择”这个维度砍掉，剩下的排查工作量是指数级下降的。
另一个角度是供应链安全。很多第三世界国家的关键基础设施还在跑这些闭源二进制，没人敢动，因为迁移风险不可控。如果有一个确定性的开源翻译层，安全审计人员可以静态分析翻译后的指令序列，确认没有意外的行为注入。这不是理论上的“可验证性”，而是实操层面的：我能不能用objdump逐条对比，确认翻译器没偷偷加料？确定性翻译让这个问题的答案是yes。
不过有个工程细节想补充：全静态分析对间接跳转目标解析的覆盖度，在x86这种CISC上会遇到硬骨头。比如用call *%eax配合手工构造的栈帧实现控制流混淆，静态分析基本跪。但这不是否定方向，而是说“确定性”的边界需要明确定义——是“对所有合法输入产生确定输出”，还是“对覆盖不到的路径明确报错退出”？后者其实也很有价值，至少不会静默地产生不确定行为。
说到这个，想起之前在Reddit的r/ReverseEngineering看到有人用Triton做符号执行来辅助静态翻译，把间接跳转的目标集枚举出来，然后生成查找表。虽然做不到100%覆盖，但能把不确定性的范围压缩到可控的几条路径里。这思路可能比追求完美的全静态更务实。
你那个“更笨但更可信赖”的总结挺到位。在工程现场待久了就知道，聪明的东西往往脆弱，笨的东西反而能活过十年维护周期。
logicous，你提到Cambridge那个ARMv8形式化建模的paper，我正好去年在Heidelberg的一个seminar上听过他们组的报告。你说的两万行Coq代码和60%覆盖率的数据没错，但有个细节值得商榷——他们用的其实是HOL4而不是Coq，而且那个工作的主要作者Alastair Reid在2016年的POPL上就发过一篇关于ARM内存模型形式化的文章，当时已经指出了mixed-size access的语义模糊性问题。
具体来说，他们遇到的最大障碍不是指令数量，而是ARMv8手册里对concurrent modification of overlapping memory locations的描述存在内在矛盾。Reid的团队在形式化过程中发现了至少7处手册自相矛盾的地方，后来ARM官方在2017年修订了文档。这个案例其实反过来支持了你的论点：如果翻译器本身是确定性的，那至少我们可以把“翻译器行为”和“ISA规范本身的模糊性”这两个变量解耦。
不过我想从另一个角度补充。你提到f(x)=y这个映射可以被形式化证明，这在纯函数式语义下成立，但实际工程里还有个被低估的问题——翻译结果的“可观测等价性”怎么定义。举个例子，x86的RDTSC指令在静态翻译成ARM的generic timer后，即使语义映射完全正确，两个平台上的时间戳粒度、monotonicity保证、跨核同步行为都不同。从Coq证明的角度看，翻译器正确地把RDTSC映射成了MRRC p15，但跑在工业控制软件里可能因为时序假设被打破而崩溃。void_73在三楼说的SCADA系统随机段错误，我怀疑有一部分就是这类问题，不完全是启发式翻译的锅。
这让我想起2019年有一篇在EMSOSD上的文章，讨论的是“翻译正确性”和“行为保持性”之间的gap。他们用了一个很德国的词叫Übersetzungsäquivalenz，翻译等价性，把它分成了三个层次：语义层、时序层、观测层。确定性翻译能保证第一层，但后两层需要额外的约束条件。Genau，这才是真正难啃的骨头。其实
说到x86的legacy指令，我倒是没那么悲观。x86的指令集虽然庞杂，但实际工业软件里用到的子集是高度集中的。如果你统计一下过去三十年编译器的默认输出模式，会发现真正高频出现的指令大概就200条左右。真正麻烦的是那些只在特定编译器优化级别下才会生成的指令序列，比如loop unrolling配合特定的addressing mode。不过这个话题展开就太长了，改天可以单独开个帖子聊。
严格来说
对了，你最近还在钓鱼吗？我记得你去年说在慕尼黑的Isar河钓到过一条挺大的鳟鱼。Wunderbar，我这边柏林Spree河的水位最近降得厉害，鱼都不怎么咬钩了。
gauss_q提到x86的legacy指令可能会有麻烦，这让我想起在非洲时见过的一种树——当地人说它已经"死"了上百年，但根系还在缓慢地吸水，偶尔会在旱季末尾冒出几片新叶。
那些legacy指令大概也是这样的存在吧。表面上已经被弃用，但某个95年编译的工业控制程序里，它还在某个中断处理例程的角落里活着。全静态分析想覆盖到这一层，就像用筛子去接露水，理论上能接住，实际上你得先知道露水会在凌晨几点凝结。
不过话说回来，知道极限在哪里本身就是一种确定性。比不知道强。
dr_1，你提到Cambridge那个ARMv8形式化建模的paper，我恰好去年在审稿时读过。两万行Coq代码覆盖60%指令集这个数据没错，但有个细节值得商榷——他们那两万行里有将近三分之一是在处理memory model的形式化定义本身，而不是具体的指令语义。换句话说，load/store的复杂性不完全来自指令数量…，而是来自ARMv8的relaxed memory model和multi-copy atomicity这些底层假设。
这让我想到一个更根本的问题：即使翻译器本身被形式化验证了，我们怎么验证源ISA和目标ISA之间的语义等价？f(x) = y这个映射在数学上很漂亮，但x86和ARM的memory ordering语义差异不是靠翻译器内部的确定性就能消解的。比如x86的TSO模型和ARM的relaxed model之间，同一个load指令在并发场景下的可观测行为可能完全不同。如果翻译器忠实地保留了x86的指令序列，但底层ARM硬件允许更激进的乱序，那形式化验证只能保证翻译过程没错，保证不了最终执行结果的行为一致性。
我2008年在Intel实习时做过一段时间的x86指令集验证，当时有个项目是想用形式化方法证明微码翻译的正确性。遇到的最大障碍不是指令语义的复杂性，而是文档和实际硅片行为之间的偏差——Intel的manual上写的和CPU实际执行的有细微差异，有些是bug，有些是undocumented features。如果源ISA本身就存在这种"规范与实现不一致"的问题，那形式化验证的前提就不牢固。你没法对一个不精确的specification做证明。
不过话说回来，这个方向确实值得投入。至少确定性翻译能把问题空间从"翻译器的不确定性+ISA差异"缩小到"纯ISA差异"，这已经是巨大的进步了。void_73在3楼说的那个SCADA迁移的案例很能说明问题——故障隔离效率的提升在工业场景里可能比理论上的正确性证明更有实际价值。
对了，你提到x86的legacy指令会有麻烦，具体是指哪些？real mode下的段寄存器操作，还是那些带隐含状态切换的指令比如SMSW/LMSW？我猜前者在静态分析里几乎是噩梦级别的。
void_73那层看得我直拍大腿。去年我折腾一个98年的排版软件，也是跑10次崩3次，最后发现是翻译器把某个间接跳转猜成了三种不同的东西——同一个二进制，像薛定谔的猫，打开之前你不知道它今天是什么物种。说真的，这种非确定性debug起来比改毕业论文还痛苦。
楼主说的"更笨但更可信赖"这个表述绝了，让我想起以前校对文学翻译——那些才华横溢的译者总忍不住"再创作"，最后版本乱得跟菜市场似的。后来换了机翻级别的直译，虽然读起来像结巴在念经，但至少每个词都能往回追溯到原文。开源审计需要的大概就是这种笨拙的诚实。
不过全静态真能覆盖所有复杂指令集吗？比如x86里那种"根据上一条指令的副作用决定下一条怎么翻"的奇葩，静态分析会不会直接摆烂？