replikativ/ansatz 来源: https://github.com/replikativ/ansatz

Ansatz 写 Clojure。证明其正确性。作为普通 JVM 代码运行。

Clojars 项目 (https://clojars.org/org.replikativ/ansatz)
CircleCI (https://circleci.com/gh/replikativ/ansatz)
最近提交 (https://github.com/replikativ/ansatz/commits/main)

Ansatz 是一个基于归纳构造演算 (https://en.wikipedia.org/wiki/Calculus_of_inductive_constructions) (CIC) 构建的 Clojure 验证编程库——与 Lean 4 (https://lean-lang.org/) 使用的是相同的类型论。它在 Java 中实现了 Lean 4 的内核，针对 Mathlib (https://leanprover-community.github.io/mathlib4_docs/)（21 万+ 定理，64.8 万声明）和 CSLib (https://github.com/leanprover/cslib)（已验证算法）进行类型检查，并将已验证的函数编译为普通的 Clojure/JVM 代码。

如果你已经在使用 malli (https://github.com/metosin/malli) 检测的 Clojure，那么 Ansatz 是渐进式的下一步：你的 m/=> 模式成为内核类型签名，你的函数变成机器可证明的，并且它们仍然作为普通 Clojure 运行。

相同内核，不同表面。 Ansatz 共享 Lean 4 的 CIC 内核——在 Ansatz 中验证的证明在 Lean 4 中同样有效，反之亦然。证明可以导出为 Lean 4 语法。差异在于表面的语言：Lean 4 使用自己的语法；Ansatz 使用 Clojure 的 s 表达式并在 JVM 上运行。详见 Lean 4 for Clojurians 以获得完整比较、翻译指南和学习路径。

``clojure (require ’[ansatz.core :as a] ’[malli.core :as m]) (a/load-init!) ;; 零配置：jar 中捆绑的 Lean Init 环境

;; 渐进式入门：保留你的 malli 模式，将 defn 改为 a/defn。 ;; 模式成为内核类型；函数经过机器验证， ;; 仍然编译为普通的 Clojure fn。 (m/=> add2 [:=> [:cat :int :int] :int]) (a/defn add2 [x y] (match x Nat Nat (zero y) (succ [k] (+ 1 (add2 k y))))) (add2 20 22) ;; => 42

;; [:map …] 模式成为命名字段记录：关键字访问是内核验证的， ;; 运行时值仍然是普通的 Clojure map (m/=> dot [:=> [:cat [:map [:x :int] [:y :int]]] :int]) (a/defn dot [p] (+ (:x p) (:y p))) (dot {:x 2 :y 3}) ;; => 5

;; 细化：[:int {:min 1}] 参数在内核类型中携带其界限作为 Prop (Subtype) ;; ——在函数体中仍然直接被用作数字 (m/=> pred [:=> [:cat [:int {:min 1}]] :int]) (a/defn pred [n] (- n 1))

;; 差分检查：编译后的运行时 ≡ 在模式生成的输入上的内核求值 ;; ——捕获类型正确但与源不符的精化错误 (require ’[ansatz.malli :as am]) (am/check-verified! ’my.ns ’add2 :runs 25) ;; => {:runs 25 :ok 25} ``

超越模式，完整的 CIC 类型——这里是经过验证的合并，内核证明终止（字典序的 sizeOf 测度，自动猜测并嵌入到内核项中）：

``clojure (a/defn merge [xs :- (List Nat), ys :- (List Nat)] (List Nat) (match xs (List Nat) (List Nat) (nil ys) (cons [x xs’] (match ys (List Nat) (List Nat) (nil (cons x xs’)) (cons [y ys’] (if (<= x y) (cons x (merge xs’ (cons y ys’))) (cons y (merge (cons x xs’) ys’))))))))

;; 也可以使用显式拼写： ;; :termination-by (+ (sizeOf xs) (sizeOf ys)) 或 [(sizeOf xs) (sizeOf ys)]

;; 运行它——这是一个普通的 Clojure 函数 (merge ’(1 3 5) ’(2 4 6)) ;; => (1 2 3 4 5 6)

;; 结构编译为 Clojure defrecord (a/structure Point [] (x Nat) (y Nat)) (->Point 3 4) ;; => #user.Point{:x 3, :y 4} (:x (->Point 3 4)) ;; => 3 ``

已验证的数据结构——定义类型，通过模式匹配实现，证明性质：

``clojure ;; 定义你自己的类型（类似 Clojure 记录，但经过类型检查） (a/inductive RBColor [] (red) (black))

(a/inductive RBTree [α Type] (leaf) (node [color RBColor] [left (RBTree α)] [key α] [right (RBTree α)]))

;; 带递归的模式匹配——内核检查终止 ;; ih_left 和 ih_right 是归纳假设（递归结果） (a/defn rb-size [t :- (RBTree Nat)] Nat (match t (RBTree Nat) Nat (leaf 0) (node [color left key right] (+ 1 (+ ih_left ih_right)))))

;; 用于 BST 查找的嵌套匹配——引用外部参数 k (a/defn rb-member [t :- (RBTree Nat), k :- Nat] Bool (match t (RBTree Nat) Bool (leaf false) (node [color left key right] (match (< k key) Bool Bool (true ih_left) ;; 递归进入左子树 (false (match (== k key) Bool Bool (true true) ;; 找到了 (false ih_right))))))) ;; 递归进入右子树

;; 验证过的常量（构造函数是项位置上的普通常量） (a/defn tree [] (RBTree Nat) (RBTree.node Nat RBColor.black (RBTree.node Nat RBColor.red (RBTree.leaf Nat) 2 (RBTree.leaf Nat)) 4 (RBTree.node Nat RBColor.red (RBTree.leaf Nat) 6 (RBTree.leaf Nat))))

;; 所有验证过的函数编译为普通 Clojure 并在 JVM 上运行 (rb-size tree) ;; => 3 (rb-member tree 4) ;; => true (rb-member tree 42) ;; => false ``

证明性质——从简单的定义相等性到自动化推理：

``clojure ;; 最简单的证明：rb-size(leaf) 根据定义为 0。 ;; (rfl) = “自反性” —— 两边归约为相同的东西。 (a/theorem leaf-size-zero [] (= Nat (rb-size (RBTree.leaf Nat)) 0) (rfl))

;; (omega) 自动求解自然数上的线性算术。 ;; 它看到：目标是 (rb-size l) ≤ 1 + (rb-size l) + (rb-size r) ;; 然后关闭它，因为对于所有自然数，x ≤ 1 + x + y。 (a/theorem left-le-size [c :- RBColor, l :- (RBTree Nat), k :- Nat, r :- (RBTree Nat)] (<= Nat (rb-size l) (+ 1 (+ (rb-size l) (rb-size r)))) (omega))

;; 以下证明使用 examples/ 中的定义（llen, lmap, Sorted, ;; insertSorted, balance1, ValidRB —— 参见 verified_list.clj, sorting.clj, rbtree.clj）。 ;; 归纳 + grind：列表性质的标准模式。 ;; (induction l) 分为两个目标： ;; 1. 基础情况：llen (lmap f []) = llen [] —— 两边都是 0 ;; 2. 归纳：llen (lmap f (x::xs)) = llen (x::xs) ;; 归纳假设：llen (lmap f xs) = llen xs ;; (grind “lmap” “llen”) 告诉 grind 使用 lmap 和 llen 的等式定理 ;; （例如 llen.eq_2: llen(x::xs) = 1 + llen xs）。 ;; 它展开一步，看到 1 + llen(lmap f xs) = 1 + llen xs， ;; 然后通过归纳假设的 congruence 关闭。 (a/theorem map-preserves-len [f :- (arrow Nat Nat), l :- (List Nat)] (= Nat (llen (lmap f l)) (llen l)) (induction l) (all_goals (grind “lmap” “llen”)))

;; Sorted 是一个索引的归纳类型：Sorted [] | Sorted [a] | Sorted (a::b::tl) when a≤b。 ;; (induction h) 对 h : Sorted l 给出 3 个目标（每个构造器一个）。 ;; (grind “insertSorted”) 使用 insertSorted 的等式定理展开它， ;; 在 ≤ 比较上分支，应用构造器，使用 omega 处理算术， ;; 并在递归情况下使用归纳假设。 (a/theorem insert-preserves [x :- Nat, l :- (List Nat), h :- (Sorted l)] (Sorted (insertSorted x l)) (induction h) (grind “insertSorted”))

;; balance1 有 7 个分支（来自颜色 + 子树形状的嵌套模式匹配）。 ;; (cases hl) 将 ValidRB(l) 拆分为 leaf 或 node。 ;; (simp “balance1”) 使用 balance1 的等式定理为每个分支展开它。 ;; (grind) 然后应用 ValidRB 构造器并从上下文中匹配子证明。 ;; 中间几行进一步对颜色、子树形状和内部颜色进行拆分， ;; 以暴露左左旋转情况（唯一重构树的分支）。 (a/theorem balance1-preserves-valid [l :- (RBTree Nat), v :- Nat, r :- (RBTree Nat), hl :- (ValidRB l), hr :- (ValidRB r)] (ValidRB (balance1 l v r)) (cases hl) ;; leaf 还是 node? (all_goals (try (simp “balance1”))) ;; 通过等式定理展开 (all_goals (try (grind))) ;; 关闭简单情况 (all_goals (try (cases c))) ;; 红色还是黑色？ (all_goals (try (cases l))) ;; 左子树形状 (all_goals (try (cases color))) ;; 内部节点颜色（检测 LL 旋转） (all_goals (try (cases hl))) ;; 分解内部 ValidRB 证明 (all_goals (try (simp “balance1”))) ;; 展开旋转情况 (all_goals (try (grind)))) ;; 关闭所有剩余目标 ``

请参阅 examples/ 以获取完整可运行示例：

• verified_list.clj — 经过验证的列表库（map, filter, append, length）以及 10+ 个已证明的性质 + 插入排序正确性
• sorting.clj — 经过验证的归并排序、结构、阶乘（CSLib 启发）
• rbtree.clj — 经过验证的红黑树，带有平衡不变量证明（grind + 手动版本）
• gradient_descent.clj — 经过验证的 GD 收敛速度证明
• metaprogramming.clj — 自定义策略、精化器、simproc

刚接触验证式编程？ 从 教程 开始——这是一份实践指南，教你如何定义函数、编写证明以及使用 grind，无需任何定理证明经验。

已经了解 Lean 4？参见 Lean 4 for Clojurians 获取语法翻译指南。

工作原理（面向 Clojure 开发者）

Ansatz 向 Clojure 添加了以下基本元素：

1. a/defn — 类似 defn，但经过类型检查。内核验证你的函数与其类型签名匹配。对于非结构模式（归并排序、阶乘），通过 :termination-by 支持良好基础的递归。编译后的输出是普通的 Clojure fn。

2. a/theorem — 声明一个性质并使用策略进行证明。策略是逐步构建证明的命令。(grind "defn-name") 策略通过 E-graph 同余闭包和情况拆分自动化了大多数证明。手动控制：(apply lemma)，(induction x)，(cases h)，(omega)，(simp "lemma")。内核验证最终的证明项。

3. a/inductive — 定义代数数据类型，支持穷举模式匹配。内核生成一个确保终止的递归子。

4. a/structure — 定义记录类型，编译为 Clojure defrecord。字段可通过关键字访问：(:x point)。内核验证的投影自动生成。

关键思想：Lean 4 的 Mathlib 库拥有 21 万以上的已证明定理（代数、分析、拓扑）。Ansatz 让你可以在 Clojure 证明中使用这些定理。当你写 (apply mul_le_of_le_one_left) 时，你正在应用一个在 Mathlib 中证明并由内核验证的定理。证明是可移植的——Ansatz 可以导出为 Lean 4 语法，并且 Lean 4 的证明可以导入到 Ansatz 中。

特性

• 已验证函数 — 使用 CIC 类型定义函数，证明性质，以 JVM 速度运行
• 可选的 Malli 模式作为签名 — 渐进式类型入门：保留你的 (m/=> f [:=> [:cat :int :int] :int]) 声明，将 defn 改为 a/defn；模式成为内核签名。集合→List；[:map [:x :int] ...]→合成的命名字段记录（关键字访问 (:x p) 精化为内核投影，运行时值保持为普通 Clojure map）；[:int {:min k}]→Subtype 细化，其参数仍然可以直接用作数字（引用自动强制转换为 .val，细化保留在绑定器中用于证明）。ansatz.malli/check-verified! 添加了生成式差分检查——模式生成的输入同时通过编译后的运行时和内核求值器，必须一致，这防范了内核无法看到的类型正确但不符合源代码的精化错误类别。malli 惰性加载；核心没有硬依赖
• Grind 策略 — 通过持久化 E-graph 和同余闭包、命题传播器（And/Or/Not/Eq/ite）、E-matching 用于引理实例化、构造器注入/辨别以及理论求解器集成实现自动化推理
• 内核强制终止 — 每个递归定义在内核项中都携带其终止证明：结构递归、:termination-by 测度（标量、字典序 [m n]——Ackermann 可验证、(sizeOf xs) 用于数据结构）、自动测度猜测以及 loop/recur；非终止定义被拒绝，带有可操作错误（^:partial 是显式受信任的逃生口）
• 一个 lean4 风格的精化器 — fvar/mvar 精化，包含隐式参数和宇宙推断，适用于函数体、签名、测度、定理声明和策略参数；Clojure 宏（->，when，and/or，你自己的）默认展开并组合
• 结构 — a/structure 编译为 defrecord，支持关键字访问和美化打印
• 泛型类型 — 通过自动精化实现隐式类型参数推断（多态构造器无需显式类型注释）
• Lean 4 Mathlib + CSLib — 64.8 万 Mathlib 声明 + CSLib 已验证算法
• 策略证明 — apply，simp，omega，ring，grind，assumption，induction，cases 等
• 实例合成 — 自动类型类解析，带表格化回溯
• 编译输出 — 验证过的 defn 编译为普通 Clojure fn，具有参数感知的平坦调用
• 可扩展 — register-elaborator! 是 lean4 macro_rules 风格的（你的函数将参数形式映射为替换表面形式，精化器处理其余部分）；还有自定义策略和 simproc，具有完整的内核访问权限
• 不可变的证明状态 — 通过 Clojure 持久数据结构实现自由回溯

快速开始

先决条件

• Java 21+（用于外部函数 API / 内存映射）
• Clojure CLI (https://clojure.org/guides/install_clojure) 1.12+

安装

添加到 deps.edn：

clojure {:deps {org.replikativ/ansatz {:mvn/version "0.1.0-SNAPSHOT"}}}

设置 Mathlib 存储

Ansatz 需要一个 Lean 4 Mathlib 声明的存储。有一个单命令的设置脚本：

自动化设置（推荐）

``bash

需要：Lean 4 (elan), Java 21+, Clojure CLI

./scripts/setup-mathlib.sh ``

这会克隆 lean4export 和 mathlib4（如果不存在），导出 Mathlib 为保留 mdata 的 NDJSON，生成实例注册表，并导入到持久存储根目录下的 Ansatz 存储中（$ANSATZ_STORE_DIR → $XDG_DATA_HOME/ansatz/stores → ~/.local/share/ansatz/stores；传递一个显式目录作为第一个参数以覆盖）。首次运行约需 20 分钟。避免使用 /tmp//var/tmp 作为存储——systemd-tmpfiles 会清理它们；之前存在的旧存储位于 /var/tmp/ansatz- 在加载时仍会自动找到。

要通过内核重新检查已导入的存储：

bash clj -M -e ' (require (quote [ansatz.export.storage :as s])) (let [store (s/open-store ((requiring-resolve (quote ansatz.store/resolve-existing)) "mathlib"))] (try (prn (s/verify-from-store! store "mathlib" :verbose? true :timeout-ms 300000)) (finally (s/close-store store)))) '

权威的全语料检查使用 PSS 支持的存储。导入的存储验证器使用比交互式策略调用更高的燃料默认值，因为完整的 Mathlib 包含超过 2000 万内核步骤的合法声明。如需与打过补丁的 Lean 4 构建进行跟踪级比较，请参见 doc/kernel-validation.md。

手动设置

如果你更喜欢逐步操作：

``bash

1. 克隆并构建 lean4export (https://github.com/leanprover/lean4export)

git clone https://github.com/leanprover/lean4export.git ../lean4export cd ../lean4export && lake build

2. 导出 Mathlib 为 NDJSON（约 5 分钟，约 5GB）

保留 mdata 以便导入的声明更接近 Lean 内核跟踪空间。

cd ../mathlib4 lake env ../lean4export/.lake/build/bin/lean4export –export-mdata Mathlib > ../ansatz/test-data/mathlib.ndjson

3. 从 Mathlib 生成实例注册表（约 2 分钟）

lake env lean DumpInstances.lean

生成 instances.tsv

cp instances.tsv ../ansatz/resources/instances.tsv

4. 导入到 Ansatz 存储（约 15 分钟）

cd ../ansatz clj -M -e ’ (require (quote [ansatz.export.storage :as s])) (def store (s/open-store ((requiring-resolve (quote ansatz.store/store-dir)) “mathlib”))) (s/import-ndjson-streaming! store “test-data/mathlib.ndjson” “mathlib” :verbose? true) ’ ``

设置 CSLib 存储（已验证算法）

CSLib (https://github.com/leanprover/cslib) 提供了经过验证的算法和数据结构。设置脚本 ./scripts/setup-cslib.sh 会自动处理：

bash ./scripts/setup-cslib.sh

这会将 CSLib 导出为 NDJSON 并导入到 ansatz-store 目录下的 cslib 存储中。完成后，你可以通过 (ansatz.export.storage/open-store "cslib") 加载它。

许可证

Copyright © 2024-2025 Christian Weilbach, Paul Johannesson, contributors (https://github.com/replikativ/ansatz/graphs/contributors)

在 Eclipse Public License 2.0 (https://opensource.org/licenses/EPL-2.0) 下分发。

有关详细信息，请参见 LICENSE。