lean-ritsuryoは、日本の法令が定める期間と税額の計算をLean 4で書き、条文どおりに計算することを証明したライブラリです。これをlean-rsでRustに変換して、Rustのcrateと、ブラウザだけで計算するWebページにしました。リポジトリはconao3/rust-ritsuryoで、ライセンスはApache-2.0です。crateはcrates.ioに ritsuryo の名前で公開しています。

ブラウザで計算する

Webページは次のURLで開けます。

https://conao3.github.io/rust-ritsuryo/

期間の満了日や祝日、所得税、相続税、消費税など、lean-ritsuryoのCLIと同じ計算をフォームから使えます。上の画像は、2025年分の課税総所得金額が500万円のときの所得税を計算したところです。納める額は584,500円になりました。計算はブラウザの中で行うので、入力はどこにも送りません。

Rustから呼ぶ

Cargo.toml に ritsuryo を追加すると、Rustから同じ計算を呼べます。

[dependencies]
ritsuryo = "0.1.0"
serde_json = "1"

use serde_json::json;

fn main() {
    let out = ritsuryo::invoke(
        "income-tax",
        "compute-tax",
        &json!({"TaxYear": 2025, "TaxableIncome": 5_000_000}),
    )
    .unwrap();
    println!("{}", out["Result"]);

    for h in ritsuryo::holiday::holidays(2027).iter().take(3) {
        println!("{}/{} {}", h.month, h.day, h.name);
    }
}

$ cargo run -q
{"DefenseTax":0,"IncomeTax":572500,"Payable":584500,"ReconstructionTax":12022,"Total":584522}
1/1 元日
1/11 成人の日
2/11 建国記念の日

invoke はCLIのサブコマンドとパラメータをそのまま受け取り、CLIが出力するものと同じJSONを返します。祝日や所得税のようによく使う計算には、引数と戻り値にRustの型を使う関数も用意しました。

Leanが入っていなくても、cargoだけでビルドできます。

仕組み

変換の入力には、Rustに出す関数だけを書いたLeanのmoduleを1つ置いています。lean-rsはこのmoduleを、そこから呼ばれるlean-ritsuryoの関数まで含めてRustのコードにします。

lean-ritsuryoのCLIは、ファイルや標準出力などのIOを扱う部分と計算の部分が分かれています。計算の部分はIOを使わない関数なので、そのままRustとブラウザから呼べます。

WebページはこのcrateをWebAssemblyにして、GitHub Pagesの静的なページから呼んでいます。lean-rsのruntimeはWebAssemblyでも動き、ファイル操作のようにIOを使う処理はエラーを返します。lean-ritsuryoの計算はIOを使わないので、そのまま動きます。

Rustのコードを作るときは、lean-ritsuryoの証明も含めてLeanのパッケージをビルドします。証明が通らない計算は、Rustのコードになりません。ただし、証明が保証するのはLeanの定義です。Rustのコードが同じ計算をすることは、lean-rsの変換が正しいことに頼っています。