AMO-Lean：在 Lean 4 中通过等式饱和实现形式验证优化

我们使用 Lean 和形式验证进行的实验继续取得成果。

为了进一步提升我们的技术和经验，我们着手研究是否可以将 Lean 的优势应用于更高级的主题：编译器优化。

传统的经过验证的编译器侧重于对已编写的 C 代码进行语义保留，从而限制了它们执行彻底的算法优化的能力。

另一方面，特定领域的代码生成器可以生成非常高效的代码，但缺乏集成到证明助手中的形式正确性保证。

在我们对 Lean 编程语言的探索中，我们开始构建一个结合了两种传统的优化引擎：该系统将来自 Mathlib 的代数定理编译成重写规则，这些规则为一个纯函数式的等式饱和引擎提供支持，并发出带有 SIMD 内联函数的 C 代码，以及形式可追溯性注解。

最终成果是 AMO-Lean，一个经过验证的优化器，可以将 Lean 4 中编写的数学规范转换为具有形式正确性保证的优化后的 C 和 Rust 代码。

每个应用过的转换都有一个对应的 Lean 证明，并且发出的代码可以根据经过形式验证的逻辑进行审计。

在本文中，我们将讨论 AMO-Lean 的架构和流水线，这是对自动形式优化的首次尝试。

1. 提升到类型理论的代数 DSL

什么是 DSL 以及为什么我们需要它

DSL（特定领域语言）是一种为特定领域或上下文设计的编程语言，与 Rust 或 C 等通用语言不同。DSL 不需要处理线程、I/O 或内存管理——它只需要精确地表达其领域的操作。为了换取这种限制，它获得了一个属性：编译器可以详尽地推理用它编写的程序，因为可能的程序空间是有限且结构化的。

在 AMO-Lean 中，DSL 是一个名为 MatExpr 的 Lean 4 归纳类型；主要是因为此探索始于将形式验证的思想应用于优化 Lean 程序规范的可能性，这些规范涉及矩阵、线性代数以及最终的 FRI 协议的元素。然后，MatExpr 是整个系统在其上运行的中间表示：重写规则应用于它，然后将其转换为 C 代码。此 DSL 中的程序不描述如何计算，例如，变换或执行向量加法——它描述了什么变换，作为代数公式。优化器负责推导如何。

对于熟悉 Rust 中 enum 的读者来说，Lean 归纳类型在概念上是相似的：它定义了一个封闭类型，其中包含一组有限的变体（称为构造函数）。不同之处在于，在 Lean 中，构造函数可以按值索引——矩阵维度是类型的一部分，而不是运行时数据。例如，AMO-Lean 的 DSL 定义了 MatExpr α m n：一个系数类型为 α 的矩阵表达式，具有 m 行和 n 列。实现的一些构造函数是

inductive MatExpr (α : Type) : Nat → Nat → Type where
  | identity (n : Nat) : MatExpr α n n             -- I_n
  | dft (n : Nat) : MatExpr α n n                  -- Symbolic DFT
  | ntt (n p : Nat) : MatExpr α n n                -- NTT over Z_p
  | twiddle (n k : Nat) : MatExpr α n n            -- Twiddle factors
  | perm : Perm n → MatExpr α n n                  -- Permutation
  | kron : MatExpr α m₁ n₁ → MatExpr α m₂ n₂      -- A ⊗ B
         → MatExpr α (m₁ * m₂) (n₁ * n₂)
  | compose : MatExpr α m k → MatExpr α k n        -- A · B
            → MatExpr α m n
  | add : MatExpr α m n → MatExpr α m n            -- A + B
        → MatExpr α m n
  -- ... and others

关于 Lean 4 的一个值得注意的特征是，维度是类型的一部分：compose 只接受内部维度为 kk 的矩阵——Am×k⋅Bk×nAm×k⋅Bk×n。Lean 会在编译时拒绝具有不兼容维度的组合。这在 Rust enum 中是不可能表达的，除非求助于 PhantomData 和复杂的 trait bounds。

作为矩阵代数中的因式分解的优化

要理解所选的 DSL，首先必须了解 SPIRAL，这是卡内基梅隆大学的一个历史悠久的项目，它解决了一个具体问题：为线性变换（FFT、NTT、DCT、WHT）生成高度优化的代码，而无需手动编写实现。核心思想是，所有这些变换都可以表示为结构化稀疏矩阵的特殊乘积，并且优化——重新排序操作、向量化、改善缓存局部性——等价于在这些矩阵上应用代数恒等式。SPIRAL 的洞察力在于，大小为 NN 的 FFT 不是一种算法：它是一种通过 Kronecker 乘积的因式分解， 这是一个神秘的想法，经受住了时间的考验，现在在现代应用程序中找到了位置。如果 AA 是 m×mm×m，而 BB 是 n×nn×n，则 A⊗BA⊗B 是一个 (mn)×(mn)(mn)×(mn) 矩阵，它将 AA 应用于“块”，并将 BB 应用于每个块内。 Cooley-Tukey 恒等式明确地说明了这一点：

DFTmn=(DFTm⊗In)⋅Tmnn⋅(Im⊗DFTn)⋅LmnnDFTmn=(DFTm⊗In)⋅Tnmn⋅(Im⊗DFTn)⋅Lnmn

这表示：要计算大小为 m×nm×n 的 DFT，应用步长排列 (LL)，然后在连续块上应用 mm 个 DFTnDFTn 副本 (Im⊗DFTnIm⊗DFTn)，然后乘以 twiddle 因子 (TT)，然后在步长组上应用 nn 个 DFTmDFTm 副本 (DFTm⊗InDFTm⊗In)。

每个因子都是具有可利用结构的稀疏矩阵。就代码和计算机而言，Im⊗AnIm⊗An 是一个 for 循环，其中 mm 次迭代将 AA 应用于大小为 nn 的连续段；或者 Am⊗InAm⊗In 是相同的操作，但具有交错（步长）数据。运算符 LmnnLnmn（步长排列）对内存重排序进行建模。具体来说，它将索引 ii 映射到 (imodm)⋅n+⌊i/m⌋(imodm)⋅n+⌊i/m⌋，这是以行优先顺序存储的 m×nm×n 矩阵的转置。

由于我们正在寻找一种能够验证 FRI 代码的前瞻性形式优化器，因此 SPIRAL 成为一个自然且有吸引力的候选者，并采用了它的一些原则：

1. 表示：变换是矩阵公式，而不是命令式代码。
2. 通过代数重写进行优化：优化意味着应用恒等式（Cooley-Tukey、步长分解、Kronecker 分布）。
3. 降级流水线：代数公式被降级为具有显式循环的 Σ-SPL 中间表示，并从那里降级为带有 SIMD 的 C。

可以通过 AMO-Lean 克服的一个问题来解释 AMO-Lean 的贡献之一：在 SPIRAL 中，代数恒等式是编译器中硬编码的公理（用 GAP/OCaml 编写）。如果一个恒等式有错误，编译器会静默地生成不正确的代码。但是对于我们的形式优化器，每个恒等式都是 Lean 4 内核验证的定理，正如我们所讨论的，逻辑错误会在编译时被捕获。

在撰写本文时，有一个例外：由于 Lean 4 内核对索引归纳类型的分割器的限制，置换的张量积需要计算上可验证的公理 (applyIndex_tensor_eq)。该公理声明 applyIndex (tensor p q) i 计算的结果与辅助函数 applyTensorDirect 相同——两个定义在算法上是相同的，但 Lean 无法自动生成用于对索引类型 Perm n 进行模式匹配的方程。该公理由 #eval 为系统中使用的所有具体大小进行了详尽的验证。

2. 那么，你如何进行形式化的优化呢？

基本对象：e-graphs

形式优化是通过将等式饱和技术应用于 e-graphs 来实现的。为了理解这一切的含义，首先必须了解我们想要解决的问题。

考虑一个具有两个规则的优化器：a×1→aa×1→a 和 a×(b+c)→a×b+a×ca×(b+c)→a×b+a×c。给定表达式 x×(1+y)x×(1+y)，传统的重写器必须选择首先应用哪个规则。如果它应用分配律，它会得到 x×1+x×yx×1+x×y，然后可以简化为 x+x×yx+x×y。但是，如果另一个规则直接简化了 1+y1+y，那么首先进行分配的决定可能不是最优的。问题在于，传统的重写是破坏性的：应用规则会丢弃原始表达式。结果取决于应用顺序，并且找到最佳顺序通常是一个指数搜索问题。

E-Graphs 通过同时表示表达式的所有等效形式来提供更好的解决方案。它是一种数据结构，用于存储分组到等价类中的一组表达式：如果两个表达式已被证明相等，则它们属于同一类。

具体来说，E-Graph 有两个组成部分：

1. E-Nodes：表示操作。a+ba+b 的 e-node 存储运算符 + 和对 aa 和 bb 类的引用（而不是对具体节点的引用）。这是关键：由于子节点指向类，而不是指向特定表达式，因此单个 + 的 e-node 隐式地表示这些类的任何一对代表的总和。

2. E-Classes：已被证明等效的 e-nodes 的集合。当重写规则确定 e1=e2e1=e2 时，e1e1 和 e2e2 的 e-nodes 将合并到同一类中。

等式饱和然后是详尽地应用所有重写规则的过程，直到没有产生新的等价物或超过限制。结果不是最佳表达式——它是一个包含所有已发现的等效表达式的 E-Graph；我们将其称为“饱和 E-Graph”。具体来说，这通过一个纯函数运行 (Saturate.lean)：

def saturate (g : EGraph) (rules : List RewriteRule)
    (config : SaturationConfig) : SaturationResult

E-Graph 进入，饱和的 E-Graph 出来。每次迭代都会将所有规则应用于所有类，实例化匹配的右侧，合并相应的类，并恢复不变量。当达到固定点或超过节点/迭代次数的可配置限制时，该过程终止。

随后的提取阶段会根据预先选择的成本模型选择最佳的一个。

这是对我们实现形式化优化背后思想的总体描述：存在与 Lean 和 C 的局限性相关的明显方面，必须加以考虑。

Lean 理解数学，但不理解内存。E-Graphs 的标准参考实现是用 Rust 编写的 egg。egg 使用 Vec<T>，索引作为隐式指针，利用 Rust 的受控可变性来实现有效的合并操作。但是，在 Lean 4（一种纯函数式语言）中实现相同的结构提出了独特的设计挑战。Lean 保证了引用纯度：没有可观察的突变、没有指针、没有别名。这使得 Lean 内核能够验证证明，但这也意味着必须仔细设计循环或密集链接的数据结构，以避免对内存管理造成过大的压力。

为了做到这一点，AMO-Lean 避免了递归归纳结构（节点树、链表），这将是 Lean 中的惯用选择。相反，它使用带有整数索引的平面哈希表的架构——在概念上更接近 ECS（实体-组件-系统），而不是函数图：现在节点是平面数据：它们对操作及其子类型进行编码，不包含递归子结构。E-nodes 现在包含等效的表达式，从而可以通过整数标识符比较来实现 O(1)O(1) 等价性检查。这些等价类通过 union-find 进行管理。Lean 4 在内部实现了一种引用计数机制：当 Array 只有一个所有者（refcount = 1）时，像 set! 这样的操作会就地进行修改，而无需复制。这为 union-find 使用模式提供了与可变情况相当的性能，其中数组在函数中按顺序修改。

此架构避免了堆中的循环，并保持了 Lean 内核所需的引用纯度。矩阵 E-Graph (EGraph/Vector.lean) 使用相同的 MatENodeOp 节点扩展了这种设计，这些节点包括 Kronecker 乘积、置换、twisted 因子和转置运算作为一流的变体。

当然，有些规则会威胁到无限期地增长 E-Graph。交换律 (a+b→b+aa+b→b+a) 应用一次会产生一个新的表达式；再次应用，它会重新生成原始表达式；依此类推，在一个无限循环中。AMO-Lean 在 Optimize.lean 中实现了两种策略：

1. 定向规则：每个 OptRule 都有一个分类（.reducing、.structural、.expanding）和一个 costDelta，用于估计该规则是否减少或增加了表达式的成本。默认情况下，只有减少规则位于安全集中。
2. 规范排序：对于可交换操作，确定性结构哈希 (exprHash) 对操作数施加首选排序：如果 hash(a) > hash(b)，则仅存储 a + b，而不是 b + a。这消除了对双向交换律规则的需求。权衡是明确的：牺牲了理论上的完整性（E-Graph 不会探索所有可能的交换形式），以换取保证的终止。实际上，对于我们所针对的信号处理优化，这种权衡是可以接受的。

3. 元编程的作用

在大多数编译器中，优化 (x×0→0x×0→0, 因式分解, 分配律) 是编译器代码中的隐式假设。如果规则不正确，编译器会默默地生成错误的代码。编译器中没有机制来证明转换保留了程序的含义。在 AMO-Lean 中，每个重写规则都有一个对应的 Lean 定理，用于证明指称语义的保留。而将这些定理连接到优化器的机制（将形式证明转换为可执行规则的机制）是元编程 monad MetaM，它允许访问元变量上下文，即当前声明的元变量集以及分配给它们的值。

经过验证的规则的结构

如 VerifiedRules.lean 中所定义，规则包括：

1. 一个语法模式 (LHS → RHS)。
2. 一个语义等式的形式定理：

∀,env,;eval(env,LHS)=eval(env,RHS)∀,env,;eval(env,LHS)=eval(env,RHS)

例如，分配律：

theorem distrib_left_correct (env : VarId → Int) (a b c : Expr Int) :
    eval env (.mul a (.add b c)) =
    eval env (.add (.mul a b) (.mul a c)) := by
  simp only [eval]
  ring

这个证明的结构具有代表性。eval 函数是 DSL 的指称语义：它将语法表达式 (Expr Int) 转换为其在给定变量环境下的语义值 (Int)。simp only [eval] 展开了 eval 的递归定义，将两边都简化为整数上的纯算术表达式。ring 策略（由 Mathlib 提供）自动关闭目标，因为生成的等式是环恒等式。

更简单的证明（涉及 0 和 1 的恒等式）直接使用 Mathlib 引理；环属性（分配律、结合律）用 ring 关闭。幂证明需要在列表上进行归纳。AMO-Lean 不重新实现算术：它导入现有的 Mathlib 引理并将它们用作正确性的基础。

MetaM：它是什么以及它启用了什么

自动将定理转换为重写规则的能力是将 AMO-Lean 与仅仅拥有证明的传统优化器区分开来的组件。为了理解为什么这很重要，请考虑另一种选择：如果没有元编程，每个优化器规则都会手动编写两次：一次作为 E-Graph 的 Pattern → Pattern，一次作为正确性证明的定理。如果这两个定义不同——如果模式说 a * (b + c) → a*b + a*c，但定理证明了其他内容——那么系统是不一致的，而没有人注意到。这正是形式验证应该防止的那种微妙错误。

如前所述，MetaM 是 Lean 4 的元编程 monad，它封装了一种计算模式；在这种情况下，MetaM 封装了有权访问 Lean 的编译器内部状态 的计算。具体来说，在 MetaM 中运行的函数可以：

• 查询环境：访问当前上下文中加载的所有定义、定理和公理。这包括所有 Mathlib。函数 getConstInfo name 按名称返回任何常量的完整声明——它的类型、它的主体、它的宇宙级别。

• 检查表达式的内部表示：在 Lean 中，所有内容——类型、术语、证明——都表示为 Lean.Expr 类型的值。像 a + b = b + a 这样的表达式在内部是 @Eq 对类型的应用，其子表达式是带有类型参数和类型类实例的 @HAdd.hAdd 的应用。MetaM 允许导航此结构、分解它和重建它。

• 打开量词：像 ∀ (a b : α), a + b = b + a 这样的定理在其内部表示中是 Lean.Expr.forallE 的链。函数 forallTelescope 同时打开所有量词，为每个量词创建新的自由变量并公开等式主体。这允许检查结论的 LHS 和 RHS，而无需手动解析 forallE 链。

• 解析元变量：instantiateMVars 将表达式中的待定元变量（未知数）替换为它们的赋值。这是必要的，因为 Lean 的 elaborator 可能会在增量精化期间使元变量未解析。

应用

模块 Meta/CompileRules.lean 定义了一个 monad 转换器 ConvertM := StateT ConvertState MetaM，它将 MetaM 与其自己的状态（用于变量跟踪）相结合。将定理转换为重写规则的完整管道是：

1. 获取定理的类型：我们首先检索声明：定理的类型是它的陈述——例如，distrib_left_correct 的类型是 ∀ env a b c, eval env (.mul a (.add b c)) = eval env (.add (.mul a b) (.mul a c))。

2. 打开量词：forallTelescope type fun args body 打开所有 ∀ 并公开 body，这是一个等式 Eq lhs rhs。

3. 提取 LHS 和 RHS：extractEqualityFromExpr 使用 e.eq? - 一个 MetaM 助手，可以识别结构 @Eq.{u} α lhs rhs - 来获取等式的两边。

4. 转换为模式：程序递归地遍历 LHS（和 RHS）的 Lean.Expr，识别已知函数的应用。

5. 发出规则：结果是一个 RewriteRule，其中包含名称、LHS 模式和 RHS 模式，可以被 E-Graph 使用。

所有这些都通过 #compile_rules 命令调用：

#compile_rules [distrib_left_correct, mul_one_right_correct, add_zero_left_correct]

该命令迭代名称，为每个名称执行管道，并发出带有诊断日志的已编译规则。如果定理没有预期的形式（不是等式，或使用不支持的运算符），它会发出警告而不是静默失败。

优点

重申一下，这种方法的一个优点是结构一致性：E-Graph 应用的规则是从证明其正确性的相同定理中机械地提取的。在“优化器认为正确的事物”和“经过形式证明的事物”之间不存在差异的可能性。如果有人修改 Mathlib 或项目中的定理，#compile_rules 会自动提取新版本。

此外，MetaM 为从 Mathlib 中的等式定理生成重写规则打开了大门，而无需手动干预。 当前的 #compile_rules 管道支持标量 DSL 运算符（加法、乘法、Expr Int 上的求幂）；将其扩展到矩阵级 DSL 运算符——Kronecker 乘积、排列、对角缩放——正在进行中。在标量域中，任何采用由这些运算符构建的表达式之间的等式形式的 Mathlib 恒等式都是 E-Graph 的潜在优化规则。

重写器的正确性

中心正确性定理 (Correctness.lean) 分层结构：

1. applyFirst_sound：如果列表中的所有规则都保留语义，则应用第一个匹配的规则也会保留语义。
2. rewriteBottomUp_sound：自下而上的重写保留语义（通过对表达式的结构归纳）。
3. rewriteToFixpoint_sound：迭代到固定点保留语义（通过对 fuel 的归纳）。
4. simplify_sound：主简化函数保留语义，将之前的引理与 algebraicRules_sound 组合起来。

此结果已针对标量重写器进行了正式证明。对于 E-Graph 引擎，正确性简化为各个规则的正确性：由于在饱和期间应用的每个规则都具有独立的证明，并且 merge 操作仅添加等价物而不破坏节点，因此提取的结果保留了输入的语义。E-Graph 的这种组合论证的完整形式化工作正在进行中。

作为一种实际的保障措施，该代码包含一个审计函数，该函数在编译时验证每个优化器规则是否都有对应的定理。如果经过验证的规则计数与预期值不匹配，则 #guard 指令会使构建失败，从而确保没有规则在没有证明的情况下意外添加到优化器。

4. 代码生成、成本模型和证明锚点

从代数到硅

此时，E-Graph 在 MatExpr 上运行，这是一种用于代数推理的优秀语言，但没有说明内存布局、循环结构或硬件。另一方面，生成的 C 代码必须准确地描述要读取和写入哪些内存地址、以什么顺序以及使用什么指令。必须有东西弥合这个差距——而且桥梁不能是非正式的，因为这正是隐藏着细微错误的地方。Kronecker 乘积 Im⊗AnIm⊗An 作为代数看起来很简单，但它的实现需要在块连续和步长访问模式之间进行选择，每种模式都有不同的缓存行为。

代码生成遵循 SPIRAL 的三阶段设计，每个阶段都用可执行性换取抽象性：

1. MatExpr → Σ-SPL (Sigma/Basic.lean)：矩阵公式被降级为 Σ-SPL 中间表示，该表示显式地对内存访问模式进行建模。Kronecker 乘积 In⊗AmIn⊗Am 转换为循环：Σn−1i=0(Si,m⋅A⋅Gi,m)Σi=0n−1(Si,m⋅A⋅Gi,m)，其中 GG 是收集（以步长读取），而 SS 是分散（以步长写入）。组合 A⋅BA⋅B 成为具有临时缓冲区的顺序评估。这一阶段是代数与记忆相遇的地方。

2. Σ-SPL → 扩展的 Σ-SPL (Sigma/Expand.lean)：符号内核扩展为基本标量运算。DFT22 变为 y0 = x0 + x1, y1 = x0 - x1。Poseidon S-box x5x5 变为 t = x*x; t = t*t; y = t*x — 通过平方链进行三次乘法。输出是 SSA 形式的直线代码。

3. Σ-SPL → C (Sigma/CodeGen.lean, Sigma/SIMD.lean)：最终代码以标量 C 或 SIMD 内联函数发出。Σ-SPL 中的循环变为 for 循环；临时缓冲区变为局部数组；收集/分散模式变为索引内存访问。向量化遵循 SPIRAL 原则：A⊗IνA⊗Iν（其中 νν 是 SIMD 宽度）易于向量化 —— 每个标量运算都变为 SIMD 运算。

从 MatExpr 到 Σ-SPL 的降级有一个形式正确性定理 (lowering_algebraic_correct in AlgebraicSemantics.lean)，该定理声明运行降级后的代码产生的结果与直接评估原始矩阵表达式的结果相同。已经为 19 个 MatExpr 构造函数中的 18 个证明了这个定理；剩余的情况（Kronecker 乘积）需要证明 adjustBlock/adjustStride 内存访问模式仍在进行中。

成本模型和提取

一旦 E-Graph 饱和，系统就包含等效实现的叠加。原始表达式和重写规则发现的所有表达式都共存于图中。提取“最佳”需要一个标准：这就是成本模型。

MatCostModel 是一个可参数化的 SIMD 感知结构（在我们的例子中，成本被分配给 NTT 实现中执行的每个操作，但这一部分对于不同的视角、评估和应用程序是完全可定制的）。作为示例，

1. 符号运算的成本为零。 dft 1024 节点本身不生成任何代码 —— 它将在以后的流水线阶段扩展。在 E-Graph 中为其分配零成本意味着提取器永远不会优先选择过早扩展而不是分解表示。这保留了 SPIRAL 需要的 O(logN)O(log⁡N) 结构。

2. 成本按 SIMD 宽度缩放。 Twiddle 因子和逐元素运算 (elemwise) 的成本除以 simdWidth。这反映了 AVX2 向量乘法以一条指令的成本处理 4 个元素。结果是：当将 simdWidth 从 4 更改为 8 时，提取器会自动选择具有更大内部并行性的因式分解。

3. 标量回退惩罚。 scalarPenalty := 1000 是一种显式的反模式：如果 E-Graph 包含需要标量扩展（没有向量化）的变体，则提取器会不惜一切代价避免它。这可以在不需要负面规则的情况下引导搜索。

现在提取算法是一个自下而上的迭代分析 (computeCosts)：对于每个 e-class，每个节点的成本都被评估为 localCost + Σ childCosts，并记录最低成本的节点。该过程迭代直到收敛或最多 100 次迭代，这是必要的，因为类之间的依赖关系可能是循环的。

此设计具有一个值得明确说明的属性：成本模型是唯一会影响结果质量的未经验证的组件。 重写规则已经过正式证明——从 E-Graph 中提取的任何表达式在语义上都是正确的。但是，生成的代码的最优性完全取决于反映硬件现实的成本。不正确的成本模型会产生正确但缓慢的代码。

证明锚点

AMO-Lean 在生成的代码中引入了证明锚点的概念。

发出的 C 代码包括结构化注释，用于记录每个块的先决条件、后置条件和不变量：

// PROOF_ANCHOR: fri_fold_parametric
// Preconditions:
// - n > 0
// - even, odd, out are non-null
// - out does not alias even or odd (required for restrict)
// Postconditions:
// - forall i in [0, n): out[i] == even[i] + alpha * odd[i]\
// - output array is fully initialized\

这些注解创建了一个可追溯性链，将 Lean 中验证的代数变换连接到已发出代码的特定块。它们不是可执行的断言，也不是二进制文件的端到端形式验证——它们是结构化的文档，旨在方便人工审计以及未来与静态验证工具的集成。

与特别的注释不同的是，Proof Anchors 是由代码生成管道系统地生成的（由代码生成配置中的 includeProofAnchors 标志控制），并遵循可解析的格式，使外部工具能够提取它们并对照 Lean 项目的定理进行交叉引用。

如果一个经过验证的二进制文件不可审计，那么它就是毫无用处的。Proof Anchors 是 AMO-Lean 的机制，用于使形式证明和执行代码之间的距离可审计。

5. 当前状态以及我们在信任圈中的位置

AMO-Lean 的架构——类型化的 DSL、带有已验证规则的 E-Graph、可参数化的成本模型以及带有可追溯性的代码生成管道——并非特定于矩阵域。

这些组件是可分离的，AMO-Lean 实例化的模式是通用的：

1. 将 DSL 定义为 Lean 的归纳类型（具有指称语义）。
2. 将重写规则编写为语义保留定理。
3. 通过 MetaM 将这些规则编译为 E-Graph。
4. 进行饱和，使用成本模型进行提取，并发出代码。

要将此方法应用于不同的领域，只需用另一个 DSL 替换 MatExpr 并编写相应的规则即可。

E-Graph、union-find、hashconsing、饱和和提取是通用的——它们对领域没有任何假设，除了节点有子节点和成本。

这种架构很有前景，我们期待着使其成熟并扩展其应用。

最直接的候选领域是存在已知代数恒等式，并且“最佳”实现取决于上下文（硬件、输入大小、所需精度）的领域。

已验证的编译不是一个单独的问题——它是一个信任差距链，不同的项目侧重于链中的不同环节。

例如，Peregrine 为从证明辅助工具中进行代码提取提供了一个统一的、经过验证的中间端。给定一个已经在 Agda、Lean 或 Rocq 中编写并证明正确的程序，Peregrine 通过一个名为 λ□ (lambda box) 的经过验证的中间表示将其编译为可执行语言（CakeML、C、Rust、OCaml）。它关注的是忠实保留：确保类型和证明擦除不会改变程序的语义。

CertiCoq 是一个经过验证的编译器，它将 Gallina（Coq 的规范语言）编译为 Clight（C 的一个子集，可由 CompCert 编译）。它的管道应用标准的编译器优化（内联、闭包转换、死代码消除），并具有经过机器检查的正确性证明。与 CompCert 结合使用，它可以产生从 Coq 到汇编的完全验证链。

Peregrine 和 CertiCoq 都接受一个程序并忠实地编译它。AMO-Lean 接受一个规范并派生出一个程序。

给定代数公式 DFTNDFTN，AMO-Lean 通过等式饱和发现 Cooley-Tukey 蝴蝶分解，并使用 SIMD 内联函数将其降低到 C——Peregrine 和 CertiCoq 都没有尝试进行这种质的转换，因为它不是它们的工作。相反，AMO-Lean 不验证 C 编译器或提取机制：它验证生成 C 源代码的代数变换。

这些工具是可组合的。AMO-Lean 生成有意简单的 C（约 300 行，热路径中没有动态分配，没有函数指针，没有递归）——正是 CompCert 能够很好地处理的子集。原则上，完全验证的链是可能的：AMO-Lean 保证代数优化保留数学规范的语义；CompCert 保证 C 编译器保留生成的源代码的语义。总之，它们将弥合从数学规范到已验证二进制文件的信任差距。

明确地说明什么是经过形式验证的，什么不是，这一点很重要：AMO-lean 仍然有很长的路要走。

AMO-Lean 并不声称或旨在成为 CompCert 级别的端到端验证编译器。

这两个工具弥合了信任链中的不同差距：CompCert 保证 C 编译器在生成机器代码时保留源代码的语义；

AMO-Lean 保证生成 C 源代码的代数变换保留数学规范的语义，并且原则上它们是可组合的。

AMO-Lean 提供的是一个优化器，其中代数变换——最容易出现细微错误的部分——经过形式验证，并具有明确的可追溯性，直至发出的代码。

它的架构是可移植的：类型化的 DSL + 经过验证的规则 + E-Graph + 成本模型的模式不假定矩阵结构。

优化提取（OOPSLA 2024）、学习成本模型（ASPLOS 2025）和用于自动定理证明的 E-Graphs（POPL 2026）的最新进展表明，此处描述的技术与编译器、形式验证和机器学习领域的积极研究方向相一致。

源代码可在 https://github.com/lambdaclass/amo-lean 获取。

参考文献

• Willsey et al., egg: Fast and Extensible Equality Saturation, POPL 2021
• Franchetti et al., SPIRAL: Code Generation for DSP Transforms, Proceedings of the IEEE, 2005
• Zhang et al., egglog: Better Together: Unifying Datalog and Equality Saturation, PLDI 2023
• Goharshady et al., Fast and Optimal Extraction for Sparse Equality Graphs, OOPSLA 2024
• Cai et al., SmoothE: Differentiable E-Graph Extraction, ASPLOS 2025
• Yang et al., TENSAT: Equality Saturation for Tensor Graph Superoptimization, MLSys 2021
• Rossel et al., Towards Pen-and-Paper-Style Equational Reasoning in ITPs by Equality Saturation, POPL 2026
• Wang et al., SPORES: Sum-Product Optimization via Relational Equality Saturation, VLDB 2020
• Panchekha et al., Herbie: Automatically Improving Floating Point Accuracy, PLDI 2015
• Singher & Itzhaky, Easter Egg: Equality Reasoning Based on E-Graphs with Multiple Assumptions, FMCAD 2024
• Suciu et al., Semantic Foundations of Equality Saturation, ICDT 2025
• Yang et al., LeanDojo: Theorem Proving with Retrieval-Augmented Language Models, NeurIPS 2023
• Koehler et al., Guided Equality Saturation, POPL 2024
• Harvey, Faster arithmetic for number-theoretic transforms, Journal of Symbolic Computation, 2014

• 原文链接： blog.lambdaclass.com/amo...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～