用 LLM 实现证明自动化：Lean 中构建 Zstandard 解压器的实践

我一直对像 Coq、Rocq 和 Lean 这样的依赖类型语言情有独钟。它们提供了一个可能性：拥有一个能够编码并强制执行任意微妙不变量的类型系统。这种东西，在普通语言里，充其量也不过是注释，而且随着团队规模的增长，很快就会丢失。随后你就会遇到微妙的误解和不完全兼容的组件。通常这些组件已经长到一定规模，当问题被发现时，要对其进行统一调整是一个让人疲惫的任务。也许，依赖类型引诱地告诉你，你可以正式地书写这些不变量，并让机器检查它们。

（顺便说一句，Coq 改名字了！多年前，我记得在普林斯顿参加 Coq 会议时，我曾试图建议，在讲英语的世界里，有一门叫做 Coq 的编程语言是一个障碍。当时我觉得观众并不同意。我还开玩笑说，那里的许多演讲听起来就像提利昂·兰尼斯特的演讲，因为有这么多的 Coq 和 Hoare。这是一个非常精彩和恰当的玩笑，虽然完全没被理解，因为它发生在那部剧的最终季之前，而我们集体选择性地忘记了它。）

问题一直在于，强大的类型系统能力伴随着巨大的证明工作量。我可以肯定地证明，自己曾整天在证明一些相当简单的事情。实际上，做证明是很有趣的：它具有挑战性、互动性，并且有明确的目标。但天哪，这确实非常耗费时间，尤其是像我这样不知道自己在做什么的人。还有一种周期性的、令人恼火的经历，那就是在许多小时的努力结束时，你发现你尝试证明的目标实际上是错误的。经典结果：https://trustworthy.systems/publications/nicta_full_text/7371.pdf，这里是 seL4 项目的回顾，他们发现，即使项目规模足够大，使工程师积累了大量经验，他们花在证明上的时间仍然大约是设计和实现时间的十倍。最终，他们的证明代码行数比 C 代码多出了 20 倍以上。

这种额外开销使得使用依赖类型语言进行编程变得极为小众。它也促使人们尝试自动化它。我略有了解的一种尝试是 F*，系统尝试让 SMT 求解器自动完成义务。这对简单情况当然有效，但很容易制造出会让 SMT 求解器陷入无尽运行状态的情形，让你怀疑它是否能完成。我见过经常使用这些语言的人不得不培养一种第六感，来判断什么会让求解器满意，然后围绕这个去设计一切。这可能有帮助，但在某种程度上，它把问题转化为神秘主义：最终你是在侍奉一个复杂而善变的神。

一个关键事实是，至少在理论上，一旦语句是正确的，其证明的内容是无关紧要的：只有证明的存在才重要。这并不完全正确，因为有两个复杂因素：首先，是 seL4 团队所说的“证明工程学”：需要结构化证明，以减少在代码更改后重新对齐所需的工作量。其次，足够复杂的证明甚至可以导致类型检查器崩溃并消耗大量内存。

现在我们有了大型语言模型（LLM），结合证明无关性，它承诺成为一种非常强大的证明自动化工具。通过足够的自动化，你或许不需要过多担心证明工程学。你仍然需要避免让类型检查器崩溃，但根据我有限的测试，LLM 可以避免这一点。潜在地，LLM 可能会让依赖类型系统变得极其实用。我想尝试一下，所以用 Lean 构建了一个 Zstandard 解压器，主要也是因为我对 Zstandard 感到好奇。

Zstandard 似乎正在赢得取代 gzip 作为标准压缩工具的竞争。它是另一种 LZ77 风格的压缩器，但它提供了更好的熵编码和精心设计，使其能够实现非常令人印象深刻的解压速度。它永远不会像 bzip2 那样美丽，但 Burrows–Wheeler 变换的闪亮优雅在面对显著的实际优势时并不算什么：

（测量是在标准参考计算机上进行的，即作者当时使用的设备。请注意纵轴为对数刻度：gzip 和 Zstandard 属于它们自己的速度类别。这是一台苹果机器，苹果的 gzip 尤其优化；在其他地方 gzip 可能会更慢。）

Zstandard（由 Yann Collet 开发，基于 Jarek Duda 的开创性 ANS 工作：https://en.wikipedia.org/wiki/Asymmetric_numeral_systems）有一个 RFC：https://www.rfc-editor.org/rfc/rfc8878，但它相当简略。它包含实现解压器所需的所有信息，但除非你已经非常熟悉压缩，否则我认为需要反复阅读几次才能理解其中的内容。我至少读了第 4.1 节六遍，才觉得对其有了不错的理解。在此过程中较晚的时候，我发现我的同事 Nigel Tao 写的关于 Zstandard 的说明比我原本打算写的要好得多。所以，如果你想理解 Zstandard，你应该阅读那篇文章。我这里只会解释最有趣的部分，熵编码器，并结合一些关于 Lean 的推广。

Zstandard 使用 Huffman 树，但它也有一种名为 FSE 的高压缩熵编码器。FSE 是一个状态机。状态的数量多于符号，每个符号获得的状态数量比例反映其在数据流中出现的概率。因此，如果某个符号预计出现的概率为 50%，它将获得大约 50% 的状态。每个状态有三个值：该状态的符号、在该状态下从比特流中读取的比特数，以及加到这些比特上的基准状态编号以获得下一个状态。现在，如果你记得，Huffman 树的问题在于它们只能使用整数位，而这些状态也读取整数位。但技巧是，如果你希望为某个符号读取 1.5 比特，那么它的一半状态读取 1 位，另一半状态读取 2 位。这样平均就达到了目标。状态表不会被传输。RFC 规定了一种从符号概率列表构建表的算法，因此只需要传输概率即可。

让我们做一个例子。假设我们有四个符号，并且我们将使用16个状态。那么我们必须将符号概率近似为16分之一的形式。（如果你想更准确地近似概率，你可以使用更多的状态；实际上zstd从不使用少于32个状态。）

任何符号都可以跟随任何其他符号，而且一个符号可能只有一个状态。因此每个符号必须能够到达每个状态。看看状态三，它是符号D的唯一状态。因为它是唯一的，所以它必须读取四位，这足以编码任何其他状态。但是，如果你看一个像B的符号，它的状态只要求你读取一位或两位。然而，16个可能的下一个状态集合正好在B符号的那些状态之间划分。因此，对于任何特定状态，恰好有一个B符号的状态可以到达它。

再考虑符号B，我们说它的概率是5/16。编码该符号的理想比特数是 -log₂(5/16) = 1.68。有三个B符号状态读取两位，两个位读取一位。状态的使用频率并不相等，并且按使用频率加权后，平均值几乎正好匹配量化概率的正确值。如果你想更精确地捕捉真实的符号概率，可以使用更大的表。

核心技巧是，通过给更常见的符号分配多个状态，编码器不仅选择一个符号：它还选择该符号要落入的状态，这个选择将信息传递到下一个符号。这就是信息的分数比特所在。但这个熵编码器仍然只是基于表的，因此运行非常快。

问题在于你不能向前工作。假设你想编码 C、D。你从哪个 C 状态开始？嗯，D 只有一个状态，所以它必须是可以到达那个状态的 C 状态。如果 D 有多个状态，那么你就需要考虑 D 之后的内容，以知道你需要哪一个。FSE 强制你从序列的末尾开始，向后工作。（这也不算太糟糕，因为通常你需要知道整个序列才能计算符号概率。）此外，Zstandard 压缩器因此是从后往前编码符号，但输出是增量写入的，所以解压器必须定位到块的末尾并倒着读取比特以整理它！这就涉及到格式的更广泛的细节，我在这里不打算涵盖；参见 Nigel 的文章：https://nigeltao.github.io/blog/2022/zstandard-part-1-concepts.html。

基本熵编码器不关心符号间的概率。也就是说，它们不能利用英文中 Q 字母后面通常跟随 U 字母这一事实。必须有其他编码在利用这些冗余。在 Zstandard 中，这是一种传统的 Lempel–Ziv 结构，它编码字面字节或对先前解码数据的反向引用。所以 FSE 主要用于高效地编码这些反向引用的偏移量和长度。

让我们谈谈 Lean！上面我说它是一种依赖类型语言，而这个概念通过例子比通过复杂定义更易阐明。所以这里有一个函数的类型，它从流中读取 n 个字节，如果没有异常，它返回一个字节数组，类型系统知道这个数组正好是 n 个字节长。

这是一个函数，它返回两个数字和一个字节数组，使得第一个数字是素数，两个数字的和可以被六整除，并且字节数组的长度至少与两个数字中较小的那个数字一样长。

那不是任何人真正需要的类型。它只是用来展示你可以把这个玩得多疯狂。依赖类型语言足以编码非常复杂的数学结构，而 Lean 目前的主要用途是作为陈述和证明数学的形式化语言。最近的一本书《代码中的证明》：https://www.quantabooks.org/books/the-proof-in-the-code/，简明且写得很好地阐述了 Lean 的发展故事。作者确实在几段文字中对构造性数学进行了彻底的曲解，但除此之外，我还是很喜欢它！

Lean 是一种像 Haskell 一样的纯函数式语言，尽管它有一些特性使其作为编程语言可能更方便。首先，Lean 是严格求值的，而 Haskell 是惰性求值。严格求值意味着函数的参数在调用之前就会被求值，而在 Haskell 中，参数的求值被推迟，直到实际需要该值时才进行。因此，在 Haskell 中，可以自由地编写开销较大的表达式并传入函数，因为它们只有在被实际使用时才会被计算。但这也意味着计算可能在程序中出现非常出乎意料的地方。这是一个有争议的话题，虽然我欣赏惰性求值的优雅，但它确实会让程序性能难以预测。

接下来，Lean 还有一些不错的语法糖：https://lean-lang.org/papers/do.pdf。它的单子 do 记法包含 for 循环、return 语句和 break 语句。如果你想以命令式风格编程，你完全可以相当合理地做到这一点！

最后，Lean 有一个优化，它会对对象进行可变更新，只要它们的引用计数等于一。因此，只要你小心不要在别的地方持有它的引用，你可以像在命令式语言中一样高效地原地修改数组。不幸的是，据我所知，Lean 并没有线性类型系统的任何方面，因此它不会帮助你确保对一个值只有单一引用。这是一个比较棘手的问题，看似微小的代码调整就可能因为在某个不起眼的地方持有对大数组的引用而彻底破坏性能。但这确实意味着，如果你想优化某个东西的性能，你有更多的工具可用。

这里是一个例子，来自我草拟的 zstd 解码器：

关注第 9 行。这有一个数组索引，这正是隐含不变量存在的地方：blockBytes 最好不要为空！在 C 语言类语言中，这种情况下会产生未定义行为。现代语言会在运行时抛出异常，或者只提供一个可选值来避免这种情况。Lean 提供了另一种选择：证明它不为空。这就是第 10 行所做的事情。blockBytes.property 表明它的长度与请求读取的长度相同，即恰好是 blockHeader.contentSize 字节。blockHeader.contentSize_rle 是这样定义的：

这是一个证明，当类型为 rle 时，contentSize 总是为一。有了这些事实，Lean 就可以推导出其余部分。

这是一个非常简短的证明，我自己也可能能弄明白，但我们可以设定更高的目标：

我实现了 RFC 中的 FSE 表构建算法。RFC 为它提供了“测试向量”：三个示例输出：https://datatracker.ietf.org/doc/html/rfc8878#section-appendix.a，给定概率。显然，这些会用于单元测试。但在 Lean 中，我们也可以证明该函数的普遍属性：

假设表构建函数在给定“accuracy”常量和符号概率列表时，会生成一个值，那么：

这些是优化解码内部循环所需要的微妙假设，也是弱类型系统中只能是隐含的或仅作注释的事情。证明像这样的强声明是 seL4 回顾中描述的 10 倍努力的一部分，也是依赖类型在常规软件中采用的主要障碍。现在有几种大语言模型（LLM）可以在大约 20 分钟内自动完成，而且只使用每月 20 美元订阅额度的一小部分。明年这很可能会成为基本要求。我必须承认，在这样做时他们需要修改生成表格的代码：我使用了太多的 Id.run（即进入命令式模式），这对证明机制来说更难处理。（但 Lean 正在研究这个问题：https://lean-lang.org/doc/tutorials/4.33.0-rc1/mvcgen/。）我确认了证明类型检查通过，并且没有任何 sorry s。

将依赖类型和大语言模型结合起来并不是一个新想法，但在将这种组合应用于日常软件工程方面做得并不多。可能需要更多的经验。非常强的类型可以放大更改的范围，因为它们必须传播到所有派生类型中。或许在更大的系统中，证明工作量扩展得不好，即使是现代的 LLM 也跟不上。Lean 是一种高级语言，并不适合所有情况。（我的玩具 Zstandard 解码器比命令行下的 zstd 慢 10 倍。）不过，证明自动化现在已经到来，从实际角度讲，我们可以使用一种新的编程语言类型。这令人兴奋！

（我没有发布代码，因为坦白说，对于像这样的小型、明确的案例，LLM 很可能比我做得更好。我这样做是为了稍微学习一下 Lean，并不将我的探索作为示范。这受到 lean-zip 的启发：https://github.com/kim-em/lean-zip，它功能更多，包括压缩器，并且证明了往返处理！）

AWS 制作了 LNSym：https://github.com/leanprover/LNSym：一个用于 AArch64 的语义和模拟器。这很酷。也许我们可以用它来展示一些函数的优化汇编实现与它们的 Lean 对应实现之间的等价性，然后在运行时使用这些汇编代码？这样我们就可以让大语言模型在优化上尽情发挥，而它们不会引入任何功能性错误。经过验证的汇编在加密实现中已经有很多经验，但现在也许可以廉价实现？

我投入了一些（主要是大语言模型的）时间尝试这个。小型 popcount 示例：https://github.com/leanprover/LNSym/blob/main/Proofs/Popcount32.lean 使用了 bv_decide，这是一个认证 SAT 求解器，而该示例所需的内存超过了我的系统，这并不乐观。微小函数是可以工作的，而且有可能得到微小 Lean 函数的等价性证明，然后使用 extern：https://lean-lang.org/doc/reference/latest/Run-Time-Code/Foreign-Function-Interface/#The-Lean-Language-Reference--Run-Time-Code--Foreign-Function-Interface--The-Lean-ABI 在运行时调用它们！但我和几个大语言模型都无法让它进一步扩展。

I've long had a soft spot for dependently-typed languages like Coq Rocq and Lean. They offer the possibility of a type system capable of encoding and enforcing arbitrarily subtle invariants. The sort of thing that, in regular languages, ends up (at best) as a comment, and which quickly gets lost as the size of the team grows. Then you get subtle misunderstandings and components that don't quite fit together. It's often the case that those components have grown to a sufficient size that, when the problem is noticed, aligning either of them is a wearying prospect. Perhaps, say dependent types seductively, you could write those invariants formally and have a machine check them.

(p.s. Coq changed its name! I remember many years ago at a Coq conference in Princeton, I tried suggesting that, in an English-speaking world, having a programming language called Coq was an impediment. I don't think the audience agreed at the time. I also joked that many of the talks there sounded like a speech by Tyrion Lannister, there being so many Coqs and Hoares. A joke that was hilarious and timely, even though it fell completely flat, coming as it did before the final season of that show and our collective memory-holing of it.)

The problem has always been that with great type-system power comes great proof effort. I can certainly attest to entire days spent proving really quite simple things. Doing proofs is actually quite fun: it's challenging, interactive, and there's a clear goal. But gosh, does it take a lot of time, especially if, like me, you don't know what you're doing. There's also the periodic, galling experience, at the end of many hours of effort, where you realise that the goal that you're trying to prove is, in fact, false . The classic result：https://trustworthy.systems/publications/nicta_full_text/7371.pdf here is the retrospective from the seL4 effort that found that, even though the project was large enough for the engineers to develop considerable experience, they spent about 10 times as much time proving as they did designing and implementing. They ended up with more than 20 times as many lines of proof code as they did C code.

That overhead has made programming in dependently-typed languages extremely niche. It has also spurred people to try and automate it away. The attempt I'm passingly familiar with is F*, where the system tries to have an SMT solver automatically discharge the obligations. That certainly works for simple cases, but it's very easy to craft something that causes the SMT solver to go off into space and run for hours, leaving you wondering whether it's ever going to finish. I've seen that people who use these languages a lot have to develop a sixth sense for what is going to make the solver happy, and then craft everything around that. It can help, but to an extent it converts the problem into mysticism: you end up serving a complex and fickle god.

A critical fact is that, at least in theory, once the statement is correct, the contents of its proof are irrelevant: only its existence matters. This is not entirely true because of two complicating factors: first, what the seL4 group called “proof engineering”: the need to structure proofs so that the effort of realigning them after code changes is reduced. And, second, sufficiently complicated proofs can cause even type checkers to blow up and consume vast amounts of memory.

We now have LLMs which, combined with proof irrelevance, promise to be an extremely capable form of proof automation. With sufficient amounts of automation perhaps you don't need to worry about proof engineering nearly so much. You still need to avoid blowing up the type checker but, in my limited tests, LLMs can avoid that. Potentially, LLMs suddenly make dependent-type systems dramatically more practical. I wanted to play around with this so built a Zstandard decompressor in Lean, mostly because I was also curious about Zstandard.

Zstandard seems like it's winning the competition to replace gzip as the canonical compression utility. It's another LZ77-style compressor, but it offers better entropy coding and a careful design that allows it to achieve very impressive decompression speeds. It will never be as beautiful as bzip2, but the shining elegance of the Burrows–Wheeler transform doesn't count for too much in the face of significant practical advantages:

(Measurements taken on the standard reference computer, i.e. whatever the author was using at the time. And note the log scale on the y-axis: gzip and Zstandard are in their own speed class. This is an Apple machine and Apple's gzip is especially optimised; expect gzip to be slower elsewhere.)

Zstandard (by Yann Collet, building on the seminal ANS：https://en.wikipedia.org/wiki/Asymmetric_numeral_systems work by Jarek Duda) has an RFC：https://www.rfc-editor.org/rfc/rfc8878, but it is quite terse. It contains all the information you need to implement a decompressor, but unless you're already quite familiar with compression, I think you'll need to re-read it a few times to understand what's going on. I, at least, had to read section 4.1 half a dozen times before I felt that I had a decent grasp of it. Too late into this process, I discovered that my colleague, Nigel Tao, has written a better write-up of Zstandard than I was going to manage anyway. So, if you want to understand Zstandard, you should read that. I'm just going to give an explanation of the most interesting bit, the entropy encoder, and mix that in with some evangelism about Lean.

Zstandard uses Huffman trees, but it also has a higher-compression entropy encoder called FSE. FSE is a state machine. There are more states than symbols, and each symbol gets a fraction of the states that mirrors its probability of occurrence in the stream. So if there's some symbol that is expected to appear 50% of the time, it gets ~50% of the states. Each state has three values: the symbol for that state, a number of bits to read from the bitstream when in that state, and a baseline state number that is added to those bits to get the next state. Now, if you recall, the problem with Huffman trees was that they could only use a whole number of bits, and these states also read a whole number of bits. But the trick is that if you are aiming to read one and a half bits for a given symbol, then half of its states will read one bit and half of them will read two bits. Then you hit your target on average . The table of states is never transmitted. The RFC prescribes an algorithm for building the table from a list of symbol probabilities, and so only the probabilities need to be transmitted.

Let's do an example. Let's say we have four symbols and we're going to use 16 states. So we have to approximate the symbol probabilities in terms of 16ths. (If you want a more accurate approximation of the probabilities, you can use a larger number of states; zstd actually never uses fewer than 32 states.)

Any symbol may follow any other symbol, and a symbol might only have a single state. So every symbol must be able to reach every state. Take a look at state three, which is the only state for symbol D. Because it's the only one, it has to read four bits, which is sufficient to encode any other state. But if you look at a symbol like B, its states only demand that you read one or two bits. However, the set of 16 possible next states is exactly partitioned between those states for symbol B. So, for any particular state, there is exactly one state for symbol B that can reach it.

Again, consider symbol B, which we said had a probability of 5/16. The ideal number of bits to encode that symbol is -log 2 (5/16) = 1.68. There are three symbol B states that read two bits and two that read one bit. The states aren't used equally often and, weighted by how often they're used, the average comes out to almost exactly the right value for the quantised probabilities. If you want to capture the true symbol probabilities with more accuracy, use a bigger table.

The central trick is that, by giving multiple states to more common symbols, the encoder doesn't just pick a symbol: it also picks which of that symbol's states to land in, and that choice carries information forward to the next symbol. That's where the fractional bits of information go. But this entropy encoder is still just table based, and so it runs very quickly.

The wrinkle is that you can't work forwards. Assume that you want to encode C, D. Which C state do you start in? Well, D only has one state so it has to be the C state which can reach that one. If D had multiple states then you would need to worry about what came after D to know which of those you needed. FSE forces you to start at the end of the sequence and work backwards. (That's not too bad because you usually need to know the whole sequence in order to calculate the symbol probabilities anyway.) Furthermore, a Zstandard compressor thus encodes symbols back-to-front, but writes output incrementally, so the decompressor has to seek to the end of a block and read the bits backwards in order to straighten it out! That's getting into broader details of the format that I'm not going to cover; see Nigel's piece：https://nigeltao.github.io/blog/2022/zstandard-part-1-concepts.html.

Basic entropy encoders do not care about inter-symbol probabilities. I.e. they can't use the fact that the letter Q is disproportionately followed by the letter U (in English). There has to be some other encoding that is exploiting those redundancies. In Zstandard, that's a traditional Lempel–Ziv structure where it encodes either literal bytes or back references to previously decoded data. So FSE is primarily used for efficiently encoding these back reference offsets and lengths.

Let's talk about Lean! Above I said that it's a dependently-typed language, and that is a concept better articulated in examples than in a complicated definition. So here's the type of a function that reads n bytes from a stream and, if it doesn't throw, returns a byte array that the type system knows is n bytes long.

Here is a function that returns two numbers and a byte array such that the first number is prime, the sum of the two numbers is divisible by six, and the byte array is at least as long as the smaller of those two numbers.

That is not a type that anyone will ever need. It's just demonstrating that you can go as wild with this as you want. Dependently-typed languages are sufficient to encode even very complicated mathematical structures, and Lean's dominant use at the moment is as a formal language for stating and proving mathematics. The recent book, The Proof in the Code ：https://www.quantabooks.org/books/the-proof-in-the-code/, is a short, well-written articulation of the story of how Lean came to be. The author does completely butcher constructive mathematics for a few paragraphs but, other than that, I enjoyed it!

Lean is a purely functional language like Haskell, although it has a few properties that make it potentially a lot more convenient as a programming language. Firstly, Lean is strict, while Haskell is lazy. Strictness means that arguments to functions are evaluated before the call happens, whereas in Haskell the evaluation of arguments is deferred until the value is actually required. So in Haskell it's free to write expensive expressions and pass them into functions, because they'll only actually be computed if they end up being used. But it also means that computation can happen in very surprising places in the program. This is a contentious topic but, while I appreciate the elegance of laziness, boy, it can make the performance of programs hard to reason about.

Next, Lean has some nice helpings of sugar：https://lean-lang.org/papers/do.pdf. Its monadic do notation contains for loops and return statements and break statements. If you want to program in an imperative style, you can do so pretty reasonably!

Lastly, Lean has an optimisation where it will make mutating updates to objects as long as their reference count is equal to one. So you can mutate an array in place as efficiently as in an imperative language, as long as you are careful not to have a reference to it someplace else. Unfortunately, Lean does not have any aspects of a linear type system that I'm aware of, so it does not help you in ensuring that there is only a single reference to a value. It's a bit of a sharp edge that a seemingly minor tweak to the code can completely crater its performance by holding on to a reference to a large array somewhere inconspicuous. But it does mean that if you are trying to optimise the performance of something, you have a lot more tools at your disposal.

Here's an example of some of this, from the zstd decoder I sketched:

Focus on line 9. There's an array index there, which is exactly the sort of place that implicit invariants live: blockBytes had better not be empty! C-like languages will give you undefined behaviour in that case. Modern languages will throw at run-time, or only give you an optional value to avoid that. Lean has another option: prove that it's not empty. That's what line 10 does. blockBytes.property is the fact that it's as long as the requested read, i.e. exactly blockHeader.contentSize bytes long. blockHeader.contentSize_rle is this:

That's a proof that, when the type is rle , the contentSize is always one. With those facts, Lean can figure out the rest.

It's a really short proof and probably I could have figured that out myself, but we can aim much higher:

I wrote an implementation of the FSE table construction algorithm from the RFC. The RFC contains “test vectors” for it: three sample outputs：https://datatracker.ietf.org/doc/html/rfc8878#section-appendix.a from given probabilities. Obviously those go into unit tests. But, in Lean, we can also prove universal properties of the function:

Assuming that the table construction function, when given the “accuracy” constant and a list of symbol probabilities, produces a value, then:

These are the subtle assumptions that an optimised decoding inner-loop requires, and things that can only ever be implicit or mere comments in weaker type systems. Proving strong statements like that is part of the 10× effort that the seL4 retrospective described, and a major barrier to the adoption of dependent types in regular software. Several LLMs can do it automatically now in about 20 minutes, and using only a fraction of a $20/month subscription quota. It'll probably be table-stakes next year. I must admit that they needed to change the table-generating code when doing so: I had used too much Id.run (i.e. dropping into imperative mode) and that's harder for the proof machinery to work with. (But Lean are working on it：https://lean-lang.org/doc/tutorials/4.33.0-rc1/mvcgen/.) I confirmed that the proofs type-check and that there are no sorry s.

Combining dependent types and LLMs is not a new idea, but not much has been done on applying the combination to quotidian software engineering. Lots more experience would be needed. Very strong types can amplify the scope of changes as they have to be propagated out through all the derived types. Perhaps the proof effort scales poorly in larger systems, such that even modern LLMs can't keep up. Lean is a high-level language, and that's not suited to everything. (My toy Zstandard decoder is 10× slower than zstd on the command line.) Still, proof automation is here now and we, practically speaking, have a new type of programming language available to us. That's exciting!

(I'm not publishing the code because, frankly, for a small, well-defined case such as this, the LLMs can probably do a better job than I did. I did this to learn Lean a little and I don't hold my explorations up as an exemplar. This was inspired by lean-zip：https://github.com/kim-em/lean-zip which does much more, includes a compressor, and proves round-tripping!)

AWS made LNSym：https://github.com/leanprover/LNSym: a semantics and simulator for AArch64. That's cool. Perhaps we could use it to show equivalence between an optimised assembly implementation of some functions, and their Lean counterparts, and then use the assembly code at run-time? Then we could let LLMs rip at optimisation and they couldn't introduce any functional bugs. Verified assembly is well-trodden in crypto implementations, but perhaps now it could be cheap ?

I put some (mostly LLM) time into trying this. The small popcount example：https://github.com/leanprover/LNSym/blob/main/Proofs/Popcount32.lean from the repo uses bv_decide , which is a certifying SAT solver, and that example requires more memory than my system has, which doesn't bode well. Tiny functions do work, and it is possible to get an equivalence proof to tiny Lean functions, and then to use extern：https://lean-lang.org/doc/reference/latest/Run-Time-Code/Foreign-Function-Interface/#The-Lean-Language-Reference--Run-Time-Code--Foreign-Function-Interface--The-Lean-ABI to call them at run-time! But I, and a few LLMs, couldn't get it to scale any further.