https://mds-boy.hatenablog.com/entry/2025/01/15/000000

この記事は、はてなエンジニア Advent Calendar 2024 の 1/15 の記事です。Flux という Rust の篩型検査ツールについて軽く紹介していきます。 developer.hatenastaff.com

導入

Rust では、コンパイル時にゼロ除算が検知された場合にはコンパイルエラーとなり、明らかなゼロ除算は防ぐことができます。

let x = 10 / 0;
// error: this operation will panic at runtime

しかし、これはコンパイル時に検知できる場合のみです。割る数が実行時に決まる値（例えば入力値）だった場合は、コンパイル時に検知することはできません。 0が与えられると、ゼロ除算でパニックが発生するでしょう。

let a = input(); // 何らかの入力を取る関数

let x = 10 / a;
// thread 'main' panicked at ...
// attempt to divided by zero

このような場合、Rust では Option 型を返すchecked_divを利用するという手段があります。 doc.rust-lang.org

let a = input(); // 何らかの入力を取る関数

let opt_x = checked_div(10, a);
if let Some(x) = opt_x {
    ...
}

これで実行時のゼロ除算を回避することができます。

しかし、事前にバリデーションをして0を弾いている場合など、コンパイル時に検証できないだけでそもそもゼロ除算が起こりえないはずの状況もあるでしょう。

ここで、除算関数の引数の型を正整数型（0を含まない整数型）とすることができれば、安全に除算を行え、戻り値の Option 型を処理する必要もなくなります。この正整数型の表現などに使えるのが、篩型（Refinement Types）です。

Flux の紹介

Flux は、Rust に篩型を追加し、その型検査を行えるツールです。論文は Flux: Liquid Types for Rust になります。例えば Haskell にも、LiquidHaskell という同種の篩型検査ツールがあります*1。

github.com

篩型（Refinement Types）とは、述語（真か偽に評価される式）を真とするような値だけを取る型のこと。例えば、正の整数型を引数に取る除算関数safe_divは、Flux では次のように定義できます。

#[flux::sig(fn(i32, i32{v: 0 < v}) -> i32)]
fn safe_div(x: i32, y:i32) -> i32 {
    x / y
}

ここで、safe_divは Rust のソースコードでは単にi32を取るだけの関数として定義されています。

コメントとして書かれた#[flux::sig(...)]が Flux の記述であり、i32{v: 0 < v}が正整数型を表現したものです。述語{v: 0 < v}を満たすようなi32の値vだけを引数として取ることが記述されています。

インストール

flux-rs.github.io

Flux は、liquid-fixpointとz3のパスを通した上で、flux を clone してcargo xtask installするとインストールできます。

z3は、算術の命題などを解くことができるSMTソルバです。引数として渡した値が篩型の述語を満たしているかどうか（満たさない場合があるか）を、このz3を使って検証しているというわけです。

オンライン実行環境も用意されていますが、サンプルがエラーになったりしてやや不安定な印象なのでインストールするのがオススメです。　

使い方

例えば、静的な assert 関数は、次のように定義できます。

#[flux_rs::sig(fn (b:bool[true]))]
pub fn assert(b:bool) {
    if !b { panic!("assertion failed") }
}

この assert 関数は、分岐に基づくような assert も（推論可能な範囲で）静的に行うことができます。

fn test(){
    assert(2 + 2 == 4); // ok
    assert(2 + 2 == 5); // fails to type check

    let a = input(); // 何らかの入力を取る関数
    if a >= 10 {
        assert(a >= 10); // ok
        assert(a < 10); // fails to type check
    }
}

また、Rust では引数の型に&mutを付けることで、可変参照を受け取ることができます。可変参照は、文字通り参照先の変数の値が可変な参照で、関数内で変数の値を変更したいときに用いられます。

この場合、篩型の制約は引数として渡されるときも、関数の中でも満たしている必要があります。つまり、可変参照の差し先の変数の値が、関数を呼び終わっても制約を満たしていることが保証されるということです。

#[flux_rs::sig(fn (p: &mut i32{v:0 <= v}))]
fn incr(p: &mut i32) {
  *p += 1
}

fn test(){
    let a = 10;
    incr(&mut a);
    incr(&mut a);
}

一度incrに渡したaが正（0 <= vを満たす値v）であることが保証され、またincrに渡すことができます。

まとめ

簡単ですが、Rust で篩型検査を行えるツール Flux を紹介しました。

ソースコードへの変更が不要で、コメントのみで検証が可能という点から、導入自体は比較的やりやすそうです。一方で、Rust において想定しない引数が渡ってくる可能性のある場合にはOptionやResultを返せば十分であり、またスマートコンストラクタのような方法も存在するので、有効なケースはすぐ思い付く限りではそう多くなさそうに思います。また、素朴に書いただけではSMTソルバによる推論ができない場合もあり、その辺りも今後に期待です。

篩型に限らず、型での表現力を増してコンパイル時に検証できることを増やす方向性は色々ありそうなので、その辺りは今後も注目して行きたいですね。

*1:論文の著者は一部共通しているようです