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

2026-11-09

Lean 4で書いて証明した関数をRustから呼べるようにする、lean-rsを作りました。逆向きに、Rustで書いた関数の性質をLeanで証明することもできます。リポジトリはconao3/lean-rsで、ライセンスはApache-2.0です。 crates.ioには lean-rust の名前で公開していて、この記事は0.2.1で動かした結果をもとに書いています。

lean-rsはLeanのコンパイラの中間表現をRustのソースに変換します。生成したRustはcargoだけでビルドでき、LeanのtoolchainもLeanのCのruntimeも要りません。先日紹介したlean-cljはLeanの関数をClojureから呼ぶもので、lean-rsはその仕組みをRustに移したものです。

conao3/lean-rsLean 4 to Rust: run Lean functions from Rust, embed Lean in Rust with lean!, and verify Rust functions in Lean on top of AeneasRustStar

3つの使い方

lean-rsの使い方は3つあります。

Rustのファイルの中にLeanで関数と定理を書き、Rustから呼ぶ。 lean! マクロを使う。
既存のlakeのプロジェクトを、Rustのmoduleの集まりに変換する。CLIを使う。
Rustで書いた関数をLeanのモデルに変換し、その性質をLeanで証明する。 #[lean_rust::model] と cargo lean-rust を使う。

1と2はLeanからRustへ、3はRustからLeanへの向きです。

LeanでRustの関数を書く

Cargo.toml に2つのcrateを追加し、 build.rs で lean-rust-build を呼びます。

[dependencies]
lean-rust = "0.2.1"

[build-dependencies]
lean-rust-build = "0.2.1"

// build.rs
fn main() {
    lean_rust_build::Builder::new().compile().unwrap();
}

lean! の中にはLeanのソースを文字列のまま書きます。

lean_rust::lean! {
    pub mod arith;
    r#"
    def double (n : Nat) : Nat := n + n

    theorem double_eq (n : Nat) : double n = 2 * n := by
      unfold double; omega

    structure Account where
      owner : String
      balance : Nat
    deriving DecidableEq

    def deposit (a : Account) (n : Nat) : Account :=
      { a with balance := a.balance + n }
    "#
}

fn main() {
    println!("{}", arith::double(21u64.into()));
    let a = arith::Account { owner: "ann".to_string(), balance: 10u64.into() };
    println!("{:?}", arith::deposit(a, 5u64.into()));
}

double_eq は、 double の定義を展開してから omega で等式を示しています。 omega は自然数と整数の線形算術を解くタクティクです。 cargo build を実行すると、build scriptがブロックをLeanのソースに書き出して lake build を実行し、定理の証明を検査します。検査が通ると、ブロックの関数がmodule arith のRustの関数になります。 Leanの Nat は任意精度の lean_rust::Nat に、structureの Account はRustのstructになります。

$ cargo run -q
42
Account { owner: "ann", balance: 15 }

証明が通らなければ、ビルドが失敗します。定理の右辺を 3 * n に書き換えてビルドすると、次のエラーになります。

warning: demo@0.1.0: src/main.rs:7:22: error: omega could not prove the goal:
warning: demo@0.1.0:   a possible counterexample may satisfy the constraints
warning: demo@0.1.0:     a ≥ 1
warning: demo@0.1.0:   where
warning: demo@0.1.0:    a := ↑n
error: failed to run custom build command for `demo v0.1.0 (/path/to/demo)`

src/main.rs:7:22 は omega を書いた位置です。 lean-rsは、Leanが報告した行と列を、Rustのファイルの中の位置に直して表示します。

初めてブロックをビルドするときは、Lean 4.35.0の lake と lean-rust のCLIが PATH に要ります。 lake はelanで、CLIはnixで入れられます。

$ nix profile install github:conao3/lean-rs#lean-rust

生成したRustのコードは .lean-rust/cache/ に保存され、ブロックを変えなければ2回目からはLeanを呼ばずにこれを使います。キャッシュをリポジトリにcommitしておけば、Leanの入っていないCIでも、crates.ioからcrateを取得した利用者の環境でもビルドできます。 lean! マクロは生成済みのファイルを include! するだけなので、rust-analyzerがマクロを展開するときにLeanは動きません。

Leanの型とRustの型は次のように対応します。

Lean	Rust
`Nat` 、 `Int`	任意精度の `lean_rust::Nat` 、 `lean_rust::Int`
`UInt8` 〜 `UInt64` 、 `Int8` 〜 `Int64`	`u8` 〜 `u64` 、 `i8` 〜 `i64`
`String`	`String`
`List α` 、 `Array α`	`Vec<T>`
`Option α` 、 `Except ε α`	`Option<T>` 、 `Result<T, E>`
structure、inductive	生成した `struct` 、 `enum`
`IO α`	`std::io::Result<T>`

型の変数を持つ関数は、 rust_instances largest [Nat, String] のように型を指定すると、Rustのgenericな関数になります。呼べるのは指定した型だけです。

lakeのプロジェクトをRustのmoduleにする

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

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

project generate は lake build で証明を検査してから、moduleごとにRustのファイルを書き出します。

$ lean-rust project generate --lake-dir lean --output-dir src/generated

公開している関数は名前をsnake_caseにしたRustの関数になります。

mod generated;
use generated::roman;

fn main() {
    assert_eq!(roman::to_roman(1994u64.into()), "MCMXCIV");
    assert_eq!(roman::from_roman("MMXXVI"), Some(2026u64.into()));
    assert_eq!(roman::from_roman("hello"), None);
}

src/generated/ は普通のRustのファイルなので、commitしておけば使う側にLeanは要りません。

Rustの関数をLeanで証明する

3つ目の使い方では、実装をRustで書き、その性質をLeanで証明します。 RustからLeanへの変換にはCharonとAeneasを使います。 Charonがrustcから関数の中間表現を取り出し、AeneasがそれをLeanの関数に変換します。この変換で得たLeanの関数を、以下ではモデルと呼びます。

例として、2つの u32 のうち大きい方を返す max_u32 を証明します。示すのは、 max_u32 がLeanで書いたspecの max と等しいことと、結果が両方の引数以上であることです。 specは lean! で書いたLeanの関数で、型にはAeneasのモデルの型を使います。 u32 に当たる型は Std.U32 です。

lean_rust::lean! {
    #[lean(imports = ["Aeneas"])]
    pub mod bits;
    r#"
    open Aeneas Aeneas.Std

    def max (a b : Std.U32) : Std.U32 := if a.val ≤ b.val then b else a

    def max_bound (a b r : Std.U32) : Bool := decide (a.val ≤ r.val ∧ b.val ≤ r.val)
    "#
}

#[lean_rust::model(refines = bits::max, ensures(bound = bits::max_bound))]
pub fn max_u32(a: u32, b: u32) -> u32 {
    if a <= b { b } else { a }
}

refines = bits::max は、 max_u32 がすべての入力で bits::max と同じ値を返すという主張です。 ensures(bound = bits::max_bound) は、結果が max_bound を満たすという主張です。 specをRustのpathで指すので、名前や引数の型を間違えるとrustcがエラーにします。

cargo lean-rust extract は、CharonとAeneasでモデルを作り、主張ごとに証明すべきLeanの命題を書き出します。この記事ではこの命題を義務と呼びます。証明はcrateの lean/Proofs/ にLeanで書きます。

theorem max_u32.proof.refines : max_u32.obligation.refines := by
  intro a b
  unfold max_u32 _root_.bits.max
  by_cases h : a.val ≤ b.val <;> simp [UScalar.le_equiv, h]

cargo lean-rust check は証明を検査し、義務ごとの状態を lean-rust.lock に記録します。サンプルのverified-rustでは、ビットを数えるループと挿入ソートを含め、すべての義務を証明してあります。

$ cargo lean-rust status
crate::bits::popcount_fast
  refines  proved    axioms: Classical.choice, Quot.sound, propext
crate::bits::max_u32
  refines  proved    axioms: Quot.sound, propext
  bound    proved    axioms: Classical.choice, Quot.sound, propext
crate::sort::insert_sorted
  sorted  proved    axioms: Classical.choice, Quot.sound, propext
  perm    proved    axioms: Classical.choice, Quot.sound, propext

axioms の列には、証明が使った公理が並びます。 sorry で証明を飛ばした義務は sorry 、Leanの標準の3つ以外の公理を使った義務は axioms と表示されます。

普段のビルドにLeanもnightlyも要らない

Charonは自前のnightlyのRustで動きますが、Charonを呼ぶのは cargo lean-rust extract だけです。普段の cargo build はstableのRustで動き、lockfileと今のソースを比べて、抽出したときから関数が変わっていないかを確かめます。 max_u32 の <= を < に書き換えてビルドすると、証明が古くなったことを警告します。

warning: verified-rust@0.1.0: lean-rust: crate::bits::max_u32: 2 obligations are stale (crate::bits::max_u32 changed since `cargo lean-rust extract`)

Cargo.toml の [package.metadata.lean-rust] に require = "proved" を書くと、証明の済んでいない義務があるときにビルドが失敗します。環境変数 LEAN_RUST_REQUIRE=proved でも同じ動作になるので、CIではこちらを使います。

証明を書く前にテストで間違いを見つける

#[lean_rust::model] は、Rustの関数とspecを同じ入力で呼んで結果を比べるテストを生成します。入力はproptestが作ります。 specはLeanの関数をRustにコンパイルしたものなので、テストと証明で同じ定義を使えます。 max_u32 を小さい方を返すように書き換えて cargo test を実行すると、次のように失敗します。

Test failed: the function returned 0, and the spec bits::max returned 1 at samples/verified-rust/src/bits.rs:17.
minimal failing input: __args = (
    0,
    1,
)

メッセージには、関数とspecがそれぞれ返した値と、食い違いの出た最小の入力が出ます。

証明したRustの実装をLeanから呼ぶ

refines の証明が通ると、 cargo lean-rust check はLeanの @[csimp] の補題を書き出します。ただし、引数に仮定を置く requires を付けた関数は対象外です。 @[csimp] を付けた補題は、2つの関数が等しいことの証明を根拠に、コンパイル時に一方を他方へ置き換えることをLeanに許します。 lean-rsはこの補題でspecの bits::max をRustの max_u32 に置き換えるので、Leanの側で max を呼んでも、実行されるのはRustの関数です。仕様をLeanで素直に書き、速い実装をRustで書いて、等しいことを証明してから差し替えられます。

仕組み

lean-rsが生成するRustは、LeanのC backendが書き出すCのコードを、そのままRustに写したものです。 runtimeのcrateの lean-rust-runtime はLeanの lean.h と同じobjectの配置と参照カウントをRustで実装しています。生成コードは、参照カウントが1の値を複製せずにその場で書き換えます。そのため、 Array の更新などの性能の特性はC backendと変わりません。 deposit の生成コードにも、 lean_is_exclusive で Account の参照カウントが1かを確かめて、1なら同じobjectを書き換える分岐があります。

x_3 = rt::lean_ctor_get(x_1, 0);
x_4 = rt::lean_ctor_get(x_1, 1);
x_12 = (!rt::lean_is_exclusive(x_1)) as u8;

C backendは、関数の中で分岐が合流する先と自己末尾呼び出しを goto で書きます。 Rustには goto が無いので、lean-rsは関数の本体を loop の中の match にし、ブロックの番号を書き換えて continue することで goto を表しています。

RustからLeanの関数を呼ぶには、C backendの出力とLeanのruntimeをリンクして、FFIで呼ぶ方法もあります。 lean-sysなどがこの方法で、ビルドにも実行にもLeanのtoolchainが要ります。 lean-rsはruntimeをRustで書き直したので、Cのライブラリとのリンクが要らず、実行時に要るのはRustだけです。生成コードの内部は unsafe な関数ですが、公開する関数はRustの値を受け渡す安全な関数です。 IO も、ファイル、ディレクトリ、環境変数、子プロセスなどCのruntimeと同じ範囲を実装しました。 OSのエラーはCのruntimeと同じ文面の IO.Error になります。

lean-rsが生成したRustは、LeanのC backendでビルドしたプログラムと同じ出力を返します。整数、浮動小数点数、文字列、リスト、配列、クロージャ、ファイルや子プロセスの IO などを使うテスト用のLeanのコードを両方で実行し、標準出力と標準エラーが1文字も違わないことをCIで確かめています。

できないこと

参照カウントはatomicでなく、 Task は作った場所で同期に実行します。
runtimeをビルドできるのはLinuxとmacOSだけです。
#[lean_rust::model] で検証できるのは、Aeneasが扱えるRustだけです。 unsafe 、内部可変性、並行処理を含む関数は検証できません。
2つのmoduleが同じLeanの型を使うと、Rustの型も2つできます。 uses で結んだブロックの間では、型を共有します。

おわりに

lean-rsはcrates.ioの lean-rust から入手できます。 samples/stepsには、最初の lean! のブロックからgenericな関数の検証まで、機能を1つずつ紹介する17段のサンプルがあります。 Issue / PR大歓迎です。