Conao3 Notes

Lean 4で証明した関数をClojureから呼べるlean-cljを作った

Lean 4で書いて証明した関数をClojureから呼び、Clojureで書いた関数の性質をLeanで証明するためのライブラリとしてlean-cljを作りました。 リポジトリはconao3/lean-cljで、ライセンスはApache-2.0です。 Clojarsに io.github.conao3/lean-clj として公開していて、この記事は0.3.0をもとに書いています。

lean-cljはLeanのコンパイラの中間表現 (IR) をClojureのソースに変換します。 JVMの上では、LeanのC backendがビルドするのと同じプログラムから型と証明を消したものが動きます。

conao3/lean-cljLean 4 IR to Clojure backend and Lean embedded in Clojure via S-expressionsClojureStar

3つの使い方

lean-cljには次の3つの使い方があります。

img

  1. Clojureのファイルの中にLeanで関数と定理を書き、Clojureから呼ぶ ( deflean )。
  2. 既存のLeanのプロジェクト (lakeのプロジェクト) を、Clojureのnamespaceの集まりに変換する (CLI)。
  3. Clojureで書いた関数をLeanのモデルに変換し、その性質をLeanで証明する ( lean-clj.typed )。

1と2はLeanからClojureへの向き、3はClojureからLeanへの向きです。 以下、この順に例を挙げます。

Leanで書いてClojureから呼ぶ

deps.edn にlean-cljを追加します。

{:deps {io.github.conao3/lean-clj {:mvn/version "0.3.0"}}}

deflean のブロックを最初に展開するときは、Lean 4.35.0 ( lean と lake ) と lean-clj のCLIが PATH に要ります。 CLIはnixでインストールできます。

$ nix profile install github:conao3/lean-clj/v0.3.0

deflean の本体にはLeanの構文をS式にしたものを書きます。

(ns demo.core
  (:refer-clojure :exclude [double])
  (:require [lean-clj.core :refer [deflean]]))

(deflean arith
  (def double [n Nat] Nat
    (+ n n))

  (theorem double_eq [n Nat] (= (double n) (* 2 n))
    (by (unfold double) omega))

  (structure Account [owner String balance Nat])

  (def deposit [a Account n Nat] Account
    (with a {:balance (+ (.balance a) n)})))

def で関数を、 theorem で定理を定義し、 (by ...) の中に証明を書きます。 double_eq では、 double の定義を展開してから、自然数と整数の線形算術を解くタクティク omega で等式を示しています。 namespaceを読み込むと、lean-cljはブロックをLeanのソースに変換して lake build を実行し、証明まで検査します。 検査が通ると、ブロックの関数がそのnamespaceのClojureの関数になります。 structureの値はkeywordをkeyに持つmapとして受け渡します。

(double 21)                                ;=> 42
(deposit {:owner "ann" :balance 10} 5)     ;=> {:owner "ann", :balance 15}

証明が通らないと、namespaceのコンパイルが止まります。 定理の右辺を (* 3 n) に書き換えてnamespaceを読み込むと、次のエラーになります。

Syntax error macroexpanding deflean at (demo/wrong.clj:5:1).
lean-clj: Lean rejected deflean arith
error: demo/wrong.clj:9: deflean arith:3:75: omega could not prove the goal:
a possible counterexample may satisfy the constraints
  a ≥ 1
where
 a := ↑n

Lean source of the block:
   1 | def double (n : Nat) : Nat := (n + n)
   2 |
   3 | theorem double_eq (n : Nat) : ((double n) = (3 * n)) := (by unfold double; omega)

エラーのメッセージにはClojureのファイルと行 ( demo/wrong.clj:9 ) と、ブロックから作ったLeanのソースが含まれます。

S式で書けない構文は (lean "...") でLeanのソースを文字列のまま混ぜて書けます。 サンプルのword-countは、 do 記法の関数をこの形で書いています。 生成したClojureのコードは .lean-clj/cache/ に保存されます。 ブロックを変えなければ、2回目からはLeanを呼ばずにキャッシュから展開するので、キャッシュをリポジトリに入れておけばLeanの無い環境でも動きます。

LeanのプロジェクトをClojureのnamespaceにする

lakeのプロジェクトとして書いたLeanのコードも、CLIでClojureのnamespaceに変換できます。 サンプルのroman-numeralsは、整数とローマ数字の変換をLeanで書き、1〜999の数をローマ数字にして戻すと元の数になることを証明しています。

def toRoman (n : Nat) : String := toRomanAux (n + 13) numerals n

def fromRoman (s : String) : Option Nat :=
  if s.isEmpty then none else fromRomanAux s.toList

theorem roundtrip : ∀ n, n < 1000 → fromRoman (toRoman n) = if n = 0 then none else some n := by
  decide +kernel

lake build で証明を検査したあと、CLIでmoduleをnamespaceに変換します。

$ lean-clj module generate-namespace --module-name Roman --namespace roman.core \
    --search-path lean/.lake/build/lib/lean --output-file src/roman/core.clj

公開している関数は名前をkebab-caseにしたClojureの関数になります。 Option の値は some の中身か nil になります。

(require '[roman.core :as roman])

(roman/to-roman 1994)        ;=> "MCMXCIV"
(roman/from-roman "MMXXVI")  ;=> 2026
(roman/from-roman "hello")   ;=> nil

生成した src/roman/core.clj は普通のClojureのファイルなので、リポジトリにcommitすれば、使う側にLeanは要りません。 プロジェクトのmoduleをまとめて変換するときは lean-clj project generate を使います。

Clojureで書いてLeanで証明する

3つ目の使い方では、実装をClojureで書きます。 次の例では、0からnまでの和を閉じた式で計算するClojureの関数が、和の定義どおりに再帰するLeanの仕様と等しいことを証明します。

(ns demo.sum
  (:require [lean-clj.core :refer [deflean]]
            [lean-clj.typed :as lt]))

(lt/defn sum-to-fast [n Nat] Nat
  (quot (* n (inc n)) 2))

(deflean sums
  (clojure sum-to-fast)

  (def sum-to [n Nat] Nat
    (match n
      0 0
      (+ k 1) (+ (sum-to k) (+ k 1))))

  (theorem two-sum-to [n Nat] (= (* 2 (sum-to n)) (* n (+ n 1)))
    (by (on-all (induction n) (simp only [sum-to Nat.mul_add Nat.add_mul] at *) omega)))

  (theorem sum-to-fast-eq [n Nat] (= (sum-to-fast n) (sum-to n))
    (by (simp only [sum-to-fast Clj.quot_nat Clj.mul_nat Clj.inc_nat])
        "have := twoSumTo n"
        omega))

  (theorem ^{:attrs [csimp]} sum-to-eq [] (= (the (-> Nat Nat) sum-to) sum-to-fast)
    (by (funext n) (exact (.symm (sum-to-fast-eq n))))))

lt/defn は普通のClojureの関数を定義し、引数と戻り値のLeanの型 (signature) をvarに記録します。 ブロックの中の (clojure sum-to-fast) は、その関数をLeanの定義に変換します。 この記事では、変換したLeanの定義をモデルと呼びます。 quot や inc のような clojure.core の関数のモデルは、lean-cljに同梱したLeanのライブラリ Clj にあります。

sum-to-eq に付けた @[csimp] は、 sum-to をコンパイルするときに sum-to-fast へ置き換えることをLeanに許す属性です。 置き換えてよい根拠は、2つの関数が等しいという証明です。 そのため、Clojureから sum-to を呼ぶと、再帰ではなくClojureの sum-to-fast が実行されます。

(sum-to 1000000)  ;=> 500000500000

この形はLeanで書く証明付きの日付と税計算で紹介したlean-ritsuryoの書き方を、Clojureの実装に当てはめたものです。 実装と仕様の関係ごとに、次のサンプルがあります。

実装と仕様の関係 lean-cljでの書き方 サンプル
仕様をそのまま実行する deflean の定義を呼ぶ todo-cli
速い実装がすべての入力で仕様と一致する 等しいことを証明し、 @[csimp] で置き換える verified-clojure ( sum-to )
速い実装が仮定のもとで仕様と一致する 仮定付きで証明し、仮定を満たす呼び出し側が実装を呼ぶ sorted-search
実装が結果の条件を満たす 条件を定理にして証明する verified-clojure (挿入ソート)、inventory

本物の関数とモデルを生成テストで比べる

証明が示すのはモデルの性質です。 モデルの挙動がClojureの関数と食い違っていれば、本物の関数では成り立たない定理も証明できてしまいます。 そこで、 lt/check を使って本物の関数とモデルを同じ入力で呼び、結果を比べます。

(lt/check #'sum-to-fast {:seed 1})
;=> {:result true, :pass? true, :num-tests 100, :time-elapsed-ms 7, :seed 1}

lt/check はsignatureから、テストの入力を作るtest.checkのgeneratorを生成します。 結果が食い違ったときは、引数と両方の戻り値を :counterexample に入れて返します。 lt/defcheck を使うと、同じ検査を clojure.test のテストとして定義できます。 lean-cljのテストでも、 Clj のモデルを clojure.core の関数と生成テストで照合していて、照合の表は156行あります。

定理はClojureの関数が値を返す呼び出しについて成り立ちます。 Long のoverflow、0での除算、範囲外のindexのように例外を投げる呼び出しは、モデルの対象外です。

生成テストで見つかったモデルの誤り

照合の生成テストで、モデルの誤りがいくつも見つかりました。 誤りの一部は、本物の関数では成り立たない定理を証明できるものでした。

多相の関数の真偽

次の member? は、任意の型 α のリスト xs に x があるかを調べます。

(lt/defn member?
  [(implicit α Type) (inst (BEq α)) x α xs (List α)]
  Bool
  (if-let [y (first xs)]
    (or (= x y) (member? x (rest xs)))
    false))

Clojureの if-let は、束縛した値が false か nil のときにelseの分岐を取ります。 そのため、 false だけのリストで false を探すと false を返します。

(member? 1 [1])          ;=> true
(member? false [false])  ;=> false

以前のモデルは、型の変数 α の値を真偽の判定で常に真として扱っていました。 Nat や String の値はClojureでも常に真なので、多くの型ではこの扱いで結果がClojureと同じになります。 しかし α = Bool のときは false が偽になるので、モデルとClojureの関数の結果が食い違います。 このモデルでは、「先頭に x があれば member? は true を返す」という次の定理が、すべての α について証明できました。

(theorem member-head [(implicit α Type) (inst (BEq α)) (inst (LawfulBEq α)) (inst (Clj.Truthy α)) x α xs (List α)]
  (= (member? x (cons x xs)) true)
  (by (rw [member?]) simp))

x = false のとき、Clojureの関数は false を返すので、この定理は本物の関数では成り立ちません。

いまのモデルは、型の変数ごとに [Clj.Truthy α] というinstanceを引数に取り、 α に入る具体的な型のinstanceで値の真偽を決めます。 同じ定理を証明しようとすると、 x が真であることを示すゴールが残り、証明が失敗します。

error: demo/member.clj:15: deflean proofs:3:128: unsolved goals
...
x : α
xs : List α
⊢ Clj.truthy x = true

サンプルのgeneric-searchは、 nil だけを偽とする if-some で member? を書き、同じ定理を証明しています。

そのほかの誤り

ほかにも、生成テストで次の3つのClojureの挙動がモデルと食い違いました。

(:k {:k nil} 0)                  ;=> nil
(str [12345678901234567890N])    ;=> "[12345678901234567890N]"
(get [0 1] 4294967297)           ;=> 1
  • (:k m default) は、keyがあって値が nil なら nil を返します。defaultを返すのはkeyが無いときだけです。モデルは nil のときにもdefaultを返していました。
  • str はvectorの中の BigInt に N を付けます。モデルは N を付けていませんでした。generatorは Long に収まらない整数も作るので、この違いが見つかりました。
  • vectorの get は、indexを int の下位32 bitに切り詰めます。 4294967297 は 2^32 + 1 なので、index 1の要素を返します。

どれも、モデルをClojureの挙動に合わせて直しました。

作らなかったもの

Long のoverflowまで含めて、関数が例外を投げないことも証明するモード ( ^:total ) は作りませんでした。 このモードでは、式全体を Option のような例外を表す型の計算として書き直す必要があります。 この書き直しをLeanの do 記法で行うと、評価の順序がClojureと食い違います。

def half (n : Nat) : Option Nat :=
  if n % 2 == 0 then some (n / 2) else none

def g (n : Nat) : Option Bool := do
  pure (n == 1 || (← half n) == 0)

#eval g 1  -- none

Clojureの (or (= n 1) ...) は、 n が1なら右辺を評価せずに true を返します。 Leanは (← half n) を式の外へ出して先に実行するので、右辺の half 1 が失敗し、 g 1 は none になります。 and や or のように途中で評価をやめる式を、すべてClojureと同じ順序で書き直す必要があり、このモードは変換の手間に見合わないと判断しました。

overflowを避けるには任意精度の +' の系列を使い、見つけるには lt/check に :throws :fail を渡して、例外を投げる入力を失敗として数えます。

仕組み

生成するコードの形式には、JavaのソースやJVMのバイトコードではなくClojureのソースを選びました。 Leanの Array はClojureの永続ベクタと意味が合い、要素の更新がO(log n) で済みます。 Nat の計算は +' で BigInt に切り替わり、Leanのクロージャは IFn を実装したClojureの値にできます。 JITがバイトコードを最適化するので、バイトコードを直接生成しても速さの利点は小さいと考えました。

実行時に動くのはJVMだけです。 Leanが動くのは deflean のブロックを展開するときと、CLIでモジュールを変換するときだけで、実行時はLeanのCのruntimeの代わりに、その関数をClojureで書き直したruntimeを使います。 LeanのプロセスもFFIも別のヒープもないので、2つのruntimeのあいだで状態を共有する場面はありません。 Clojureと生成したコードのあいだで受け渡す値はどれもimmutableです。 Leanの可変な状態はClojureの仕組みで動きます。 IO.Ref はatom、 Task はfuture、 Thunk はdelayになり、標準出力は *out* に書くので binding で差し替えられます。

生成したClojureが正しいことは、LeanのC backendとの差分テストで確かめています。 同じテスト用の関数を、C backendがビルドした実行ファイルと、生成したClojureの両方で実行し、出力の182行を比べます。 浮動小数点数の無限大を、Cは inf 、Javaは Infinity と表示する違いも、このテストで見つかりました。

生成したコードが、JVMの1メソッドあたり64KBという上限を超えたこともありました。 LeanのIRのjoin point (関数の中で複数の分岐が合流する先) を呼び出し箇所ごとに展開していたため、生成したコードが36,000行に膨らみ、 Std.Format の関数の読み込みが「Method code too large!」で失敗しました。 いまは呼び出しが1か所のjoin pointだけを展開し、2か所以上のものは letfn にしています。 自己末尾呼び出しは loop と recur に、相互再帰は trampoline にして、スタックを積まずに実行します。

Clojureの型のライブラリとの関係

Clojureには、clojure.spec、malli、Plumatic Schemaのように、値を実行時に検査するスキーマのライブラリがあります。 これらは値を検査する述語を組み合わせて書く仕組みで、型の変数を持たず、mapは既定で開いていて、整数の固定精度と任意精度を区別しません。 Typed Clojureとclj-kondoの型検査は、それぞれ独自の型の言語と、 clojure.core の関数の型の注釈を持っています。

lean-cljでは型をLeanで書き、その型からmalliのスキーマ、test.checkのgenerator、clj-kondoの型を生成します。 deflean で定義したstructure Account からは、次のmalliのスキーマができます。

(require '[lean-clj.types :as t])

(t/malli-schema 'Account)
;=> [:map {:closed true} [:owner :string] [:balance [:and integer? [:>= 0]]]]

Nat は0以上の整数に、structureは同じkeyを持つ閉じたmapになります。 証明を書かなくても、signatureからこれらを使えます (サンプルのtyped-schemas)。

近い領域のプロジェクトに、whiloさんのansatzがあります。 ansatzはLeanのカーネルをJavaで実装し、JVMだけで型の検査を済ませます。 lean-cljは本物のLeanで検査し、Leanの構文と標準ライブラリ、既存のlakeのプロジェクトをそのまま使います。 その代わり、 deflean の初回の展開にはLeanのtoolchainが要ります。

おわりに

lean-cljはClojarsの io.github.conao3/lean-clj から入手できます。 samplesには使い方ごとの小さなサンプルがあり、 deflean はtodo-cliから、Clojureの関数の検証はverified-clojureから読むのがおすすめです。 Issue / PR大歓迎です。