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だけでビルドできます。

仕組み

lean-ritsuryoとRustのあいだには、Rustに出す関数だけを書いたLeanのmoduleを1つ置いています。 lean-rsはこのmoduleを、呼ばれるlean-ritsuryoの関数まで含めてRustのファイルにします。

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

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

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