【ImperialViolet相关文章】

长久以来，ImperialViolet一直对像Rocq（原Coq）和Lean这样的依赖类型语言情有独钟。它们提供了一种能编码并强制实施任意微妙不变量的类型系统，而在常规语言中，这类东西最多只能以注释形式存在，且随团队规模扩大易被遗忘，进而出现误解和组件契合问题。依赖类型似乎在诱惑着人们正式编写这些不变量，让机器来检查。

顺便说一句，Coq改名了。多年前在普林斯顿的一次Coq会议上，ImperialViolet曾建议，在英语环境中，使用名为Coq的编程语言会是一个障碍，当时听众并不认同。ImperialViolet还开玩笑说，那里的许多演讲听起来像提利昂·兰尼斯特的演讲，可惜没人get到，因为那时候该剧最后一季还没播出。

【依赖类型语言的证明难题】

强大的类型系统往往伴随着巨大的证明工作量。ImperialViolet自己曾花一整天证明简单事情，证明过程有趣但耗时，还可能出现努力后发现目标错误的情况。seL4项目回顾报告显示，工程师花在证明上的时间约是设计和实现时间的10倍，证明代码行数是C代码行数的20倍还多。

这种开销使使用依赖类型语言编程成为小众行为，促使人们尝试将证明过程自动化。ImperialViolet对F*有一定了解，在F*中，系统试图用SMT求解器自动完成证明义务，但容易构造出让求解器陷入困境的情况，使用者需培养直觉围绕求解器编写代码，这在某种程度上把问题变成了玄学。

虽然理论上命题正确时证明内容无关紧要，但存在两个复杂因素：一是seL4团队所说的“证明工程”，需对证明进行结构设计以减少代码更改后重新调整证明的工作量；二是过于复杂的证明会导致类型检查器崩溃并消耗大量内存。

【大语言模型带来的转机】

现在有了大语言模型（LLMs），结合证明无关性，它们有望成为强大的证明自动化形式。有足够自动化后，或许不用太担心证明工程，且根据ImperialViolet有限的测试，LLMs可以避免让类型检查器崩溃，潜在地让依赖类型系统变得实用多了。

于是，ImperialViolet用Lean编写了一个Zstandard解压缩器，部分原因是对Zstandard好奇。Zstandard似乎正在赢得取代gzip成为标准压缩工具的竞争，它是LZ77风格的压缩器，有更好的熵编码和精心设计，解压缩速度出色。虽然它不如bzip2优美，但实际优势明显。

这些测量是在标准参考计算机（即作者当时使用的苹果设备）上进行的，注意y轴是对数刻度，gzip和Zstandard在速度方面表现突出，不过苹果的gzip经过了特别优化，其他设备上的gzip可能会慢一些。

Zstandard由Yann Collet开发，基于Jarek Duda的开创性ANS工作，有一个RFC，但内容简洁，除非对压缩技术非常熟悉，否则可能需反复阅读才能理解。ImperialViolet的同事Nigel Tao写了一篇关于Zstandard的精彩文章，如果想了解Zstandard，应该去读那篇文章，ImperialViolet在这里只解释最有趣的部分——熵编码器，并结合一些对Lean的介绍。

【熵编码器的工作原理】

熵编码器的工作是用最少的比特数对概率不均匀的符号序列进行编码。经典的熵编码器是霍夫曼编码器，它构建一棵二叉树，符号位于叶子节点，通过简单算法生成最优前缀树。霍夫曼树速度快，但缺点是每个符号只能使用整数个比特，会造成一定的浪费。

Zstandard使用霍夫曼树，还有一种压缩率更高的熵编码器——有限状态熵编码器（FSE）。FSE是一种状态机，状态数量比符号数量多，每个符号分配到的状态比例反映其在数据流中出现的概率。每个状态有三个值：对应的符号、从比特流中读取的比特数以及一个基线状态数，将其与读取的比特数相加得到下一个状态。

通过为更常见的符号分配多个状态，编码器不仅选择一个符号，还选择该符号要进入的状态，这个选择会将信息传递到下一个符号，这就是分数比特信息的去向。而且这种熵编码器基于表，运行速度非常快。

但FSE不能正向工作，必须从序列的末尾开始反向工作。此外，Zstandard压缩器按反向顺序编码符号，但会逐步写入输出，所以解压缩器必须定位到块的末尾，反向读取比特才能将其还原。基本的熵编码器不考虑符号间的概率关系，在Zstandard中，是一种传统的Lempel–Ziv结构来利用这些冗余信息，FSE主要用于高效编码反向引用的偏移量和长度。

【Lean语言的特点与应用】

Lean是一种依赖类型语言，用例子阐述这个概念更合适。比如一个从流中读取n个字节的函数，类型系统知道返回的字节数组长度是n；还有一个返回两个数字和一个字节数组的函数，对数字和数组长度有特定要求。

Lean目前主要作为陈述和证明数学定理的形式语言，《代码中的证明》这本书简短而精彩地讲述了Lean的发展历程。Lean和Haskell一样是纯函数式语言，但有一些特性使其作为编程语言可能更方便。首先，Lean是严格求值的，而Haskell是惰性求值的，严格求值让程序性能更易预测；其次，Lean有很棒的“语法糖”，单子 `do` 表示法包含 `for` 循环、`return` 语句和 `break` 语句，可进行命令式编程；最后，Lean有一个优化机制，只要对象的引用计数为1，就会对其进行可变更新，但Lean没有线性类型系统的相关特性，可能会影响性能。

在ImperialViolet编写的zstd解码器中有一个例子，关注数组索引处，Lean可以证明数组不为空，这是通过相关定理和信息推断出来的。ImperialViolet根据RFC实现了FSE表构造算法，在Lean中还可以证明该函数的通用性质，现在有几个大语言模型可以在大约20分钟内自动完成这些证明，而且只使用每月20美元订阅配额的一小部分，明年这可能就会成为标配。不过，ImperialViolet在进行证明时需要更改表生成代码，Lean团队正在改进这一点。

将依赖类型和大语言模型结合并非新想法，但在日常软件工程中应用这种结合的工作还不多，还需要更多实践经验。非常强的类型可能会放大更改的影响范围，Lean是高级语言，并不适用于所有场景，ImperialViolet编写的简单Zstandard解码器比命令行工具 `zstd` 慢10倍。尽管如此，证明自动化已经到来，有了一种新型的编程语言可供使用，这很令人兴奋！ImperialViolet不会发布代码，因为大语言模型可能比他做得更好，这一灵感来自于lean - zip。

【补充：经过验证的汇编代码】

AWS开发了LNSym，这是一个AArch64的语义和模拟器，也许可以用它来证明某些函数的优化汇编实现与其Lean版本的等价性，然后在运行时使用汇编代码，让大语言模型进行优化而不引入功能错误。经过验证的汇编代码在加密实现中已经很常见，但现在也许可以变得“廉价”。

ImperialViolet花了一些时间（主要借助大语言模型）来尝试这个想法，仓库中的小popcount示例使用了 `bv_decide`，但这个示例需要的内存超过了系统所能提供的，对于非常小的函数是可行的，可以为小型Lean函数获得等价性证明，然后在运行时调用它们，但ImperialViolet和几个大语言模型都无法将其扩展到更大的规模。