这篇文章介绍了在Coq中形式化x86架构子集的工作，利用依赖类型、类型类和符号简化了x86语义模型。作者通过具体函数表示位、字节和内存，并将其映射到数学对象以进行定理证明。该模型支持传统汇编语法，并利用Coq定义实现强大的"宏"功能，包括条件、循环、局部变量和带参数的过程。汇编代码可在Coq中生成十六进制字节序列，并具备正确性定理，将机器码与适用于程序验证的分离逻辑公式相关联。

论文标题：Coq：全球最佳宏汇编器？

作者与机构：

• Andrew Kennedy 与 Nick Benton（微软研究院）
• Jonas B. Jensen（哥本哈根IT大学）
• Pierre-Evariste Dagand（斯特拉斯克莱德大学）

摘要：

本文描述了一个基于Coq的x86架构子集的形式化模型。模型的核心在于简洁性：通过依赖类型、类型类和符号系统，我们重新设计了x86语义，打破了其复杂性的固有印象。我们使用可计算的函数在Coq内部直接建模位、字节和内存，并将具体表示映射到SSR EFLECT库中的数学对象（如自然数和模2^n整数）以证明定理。此外，我们通过符号系统支持在Coq中直接编写传统汇编代码语法（包括词法作用域标签）。普通的Coq定义可作为强大的“宏”功能，支持从简单的条件分支、循环到栈分配的局部变量和带参数的函数。汇编代码可在Coq内汇编，生成十六进制字节序列。汇编器具备一个正确性定理，将内存中的机器码与适用于程序验证的分离逻辑公式关联。

主要贡献：

1. 建模：

   • 使用依赖类型、类型类和符号系统，实现了x86机器代码的简洁形式化。
   • 通过布尔元组表示位向量，直接定义算术操作为可计算的Coq函数，同时利用SSR EFLECT库的数学对象（如自然数和模2^n整数）证明定理。
   • 提出抽象的读写器单子（monadic）处理，支持二进制格式描述和往返性质证明的复用。
   • 执行语义的简洁性得益于单子语法和指令类型的精细分解。

2. 汇编：

   • 在Coq内部完全生成代码的创新方法：
     • 通过符号和隐式强制转换实现与标准Intel语法兼容的汇编语法。
     • 支持词法作用域标签，基于高阶抽象语法（HOAS）构建控制结构和函数调用约定等已验证的抽象。
     • 证明指令解码器是编码器的左逆，且汇编器保留程序正确性证明。
   • 展示了如何基于第三方Kleene代数理论构建正则表达式的验证编译器。

示例与应用：

• 阶乘计算：通过Coq汇编生成机器码，调用外部printf函数输出结果。
• 游戏《生命》：完全用Coq编写的汇编代码生成可启动的CD镜像。
• 正则表达式编译器：利用Kleene代数理论，将正则表达式编译为x86机器码，验证其正确性。

技术亮点：

• 位与字节的建模：使用依赖类型精确表示不同长度的位向量（如8位字节、32位双字）。
• 内存模型：基于前缀树（trie）实现高效的部分映射，支持32位地址到字节的映射。
• 单子抽象：通过Reader和Writer单子统一处理解码、编码和执行语义，支持多种解释方式（函数式、命令式、逻辑式）。
• 指令集形式化：通过依赖类型和精细分解，定义x86指令的子集，确保每个合法指令均有明确的编码。

汇编器实现：

• 标签处理：通过两遍汇编（计算标签地址+生成代码）支持词法作用域标签。
• 宏系统：利用Coq定义实现结构化控制（如循环、条件分支）和函数调用约定抽象。
• 正确性证明：验证指令编码与解码的往返性质，以及汇编器生成的代码符合分离逻辑规范。

案例研究：

• 常数乘法优化：生成移位和加法指令序列，替代乘法指令，并验证其正确性。
• 调用约定抽象：根据cdecl、stdcall和fastcall约定自动生成调用序列和函数框架。
• 正则表达式匹配：通过DFA编译生成x86代码，验证其行为与正则语义一致，应用于浮点数识别。

讨论与相关工作：

• 对比了与CompCert、RockSalt、Bedrock等项目的异同，强调Coq在统一建模、编程和验证中的优势。
• 指出依赖类型和符号系统在实现领域特定语言（DSL）中的潜力，以及验证驱动的抽象如何推动模块化设计。

结论：

Coq作为一个多功能证明助手，为低级编程提供了独特的集成环境，支持从形式化建模到代码生成和验证的全流程。尽管在性能和工具链方面仍有改进空间，但其在构建高可信软件组件方面的潜力已得到充分展示。

这篇评论主要围绕Coq（现称Rocq）作为汇编语言工具的应用和潜力展开讨论，观点如下：

1. 高度认可Coq在安全关键系统中的应用价值

   • 作者addaon认为这是读过最重要的论文之一，特别适用于需要证明汇编代码语义属性的高可靠性系统（如汽车、航空电子）。
     引用："being able to work in an environment where I could prove semantic properties of assembly code is pretty close to my dream"
     引用："the incremental cost of going to assembly seems minor, if there's even a small payback in time to demonstrate correctness"

2. Coq的严谨性对编译器设计和AI的潜在益处

   • quanto分享在研究生课程中用Coq编写编译器的经历，认为其严谨性对这类任务很有帮助，并思考AI计算图是否也能受益。
     引用："The Coq language's rigor really helps with something like this"
     引用："I wonder if AI's compute graph would benefit from a language-level rigor as of Coq"

3. 对Coq作为汇编工具的实际功能提出疑问

   • mmastrac质疑其语法是否足够可靠，并询问是否能证明更大块汇编代码的行为。
     引用："It's a bit of an awkward syntax to get a reliable assembler"
     引用："could I use it to prove that a block of assembly is equivalent to a given set of operations?"

4. 其他相关观点

   • asdefghyk强调x86架构的复杂性需要强大的汇编工具；anthk则认为Lisp也能轻松实现类似Coq的严谨性。
     引用："The x86 architecture and instruction set is complex - so it absolutely needs a powerful assembler"
     引用："A Lisp can mimic Prolog and the rigour of Coq with ease"

（注：所有评论均无评分，kragen的评论仅提供论文链接，未包含实质性观点）