Rust の篩型検査器 Flux を試してみる
この記事は、はてなエンジニア 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。
篩型（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 は、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:論文の著者は一部共通しているようです
ヒューリスティックコンテストのスコアを Mackerel に投稿してみる
Mackerel 開発チームで Web アプリケーションエンジニアをしている 
id:mds_boy です。
今回は、ヒューリスティックコンテストに取り組む過程のスコアや実行時間を Mackerel に投稿してみようと思います。
この記事は、Mackerel Advent Calendar 2023 の 12/5 分の記事です。 qiita.com
ヒューリスティックコンテストとは
ヒューリスティックコンテストとは、最適解を出すことが困難な問題に対し、可能な限りよい解を出力するプログラムを作成するコンテストのことです。マラソンマッチと呼ばれることもあります。最近では AtCoder で開催されている AHC（AtCoder Heuristic Contest）が有名だと思います。
ヒューリスティックコンテストの開催期間は、短いものだと（アルゴリズム系のコンテストと同じく）数時間、長いものだと数週間に渡るものもあります。 特に長期間に渡るコンテストでは、次にどんな改善をするかを決めるために、過去の改善によりどんな結果が得られたかしっかり分析することも重要となります。 今回はそのための手段として、スコアや実行時間を Mackerel に投稿し、可視化を行ってみようと思います。
ヒューリスティックコンテストのスコアを Mackerel に投稿
題材として、以前開催された AHC026 を採用することにします*1。
AHC では、ビジュアライザとして Web版と Rust ソースコードが配布されるローカル版の2つが存在します。
ローカル版は、入力ファイルと、その入力ファイルを実装したプログラムに渡すことで得られる出力ファイルを受け取り、スコアを出力したり、動作が確認できるHTMLファイルを生成する仕組みです。
今回は、ローカル版で用意されたスコア計算の関数を呼び出し、指定した入出力に対するスコアを計算してMackerel に投稿する実装をRust で書いてみることにします。
今回採用した AHC026 のローカル版ビジュアライザ実装は、問題文ページの「ツール(入力ジェネレータ・ビジュアライザ)」で配布されています。
このビジュアライザ実装のsrc/binディレクトリに、新たにpost_mackerel.rsのようなファイルを追加し、実装を行います。
Mackerel では、公式 API が用意されています。 今回は、Rust で Mackerel に簡単にメトリックを投稿するための API クライアントライブラリとして、mackerel-client-rs を使ってみます。
では、投稿したいメトリックについて考えてみましょう。 コンテストで重要なのは、直接順位計算に関わるスコアと、制限時間の存在する実行時間でしょう *2。 というわけで、スコアと実行時間の2つのグラフを用意することにします。 それ以外にも可視化すると良さそうな情報があったら、随時追加していくと良いと思います。
また、Mackerel では1つのグラフに複数の系列が投稿でき、比較することができます。 今回ならば、テストケースごとのスコアや実行時間の差を知りたいところです。 他と比べてスコアが伸びなかったり時間がかかるテストケースがあった場合は、そのテストケースでの様子をビジュアライザで確認することで、バグの発見や更なる改善に繋げられるでしょう。
実装
では、実装を見て行きましょう。
前述した通り、配布されたビジュアライザ実装のsrc/binディレクトリに実装した Rust コードを追加します。
Cargo.tomlの[dependencies]には次のライブラリを追加しておきます。
mackerel_client = "0.5.0"
async-std = { version = "1.12.0", features = ["attributes", "tokio1"] }
スコアと時間をテストケースごとに投稿するコードは次のようになります。
（コンテストということもありunwrapを多用してしまっていますが、本来はしっかりエラー処理をすべきです）
use mackerel_client::{ metric::{MetricValue, ServiceMetricValue}, *, }; use std::time; struct PostMetric { test_i: usize, score: i64, execSec: f32, } fn getNowUnixTime() -> u64 { time::SystemTime::now() .duration_since(time::UNIX_EPOCH) .unwrap() .as_secs() } async fn post_mackerel(post_metrics: Vec<PostMetric>) { let client = Client::new("<API KEY>"); let mut serviceMetricValue = Vec::new(); for post_metric in &post_metrics { serviceMetricValue.push(ServiceMetricValue { name: format!("score.{}", post_metric.test_i), value: MetricValue { time: getNowUnixTime(), value: post_metric.score as f64, }, }); serviceMetricValue.push(ServiceMetricValue { name: format!("execSec.{}", post_metric.test_i), value: MetricValue { time: getNowUnixTime(), value: post_metric.execSec as f64, }, }); } client .post_service_metric_values("AHC".to_string(), serviceMetricValue) .await .unwrap(); }
構造体PostMetricsはテストケース番号とスコア、実行時間を持ちます。
関数post_mackerelはVec<PostMetric>を受け取り、各テストケースのスコアと実行時間をサービスメトリックのvalueとして現在時刻timeと共に投稿しています。
次に、テストケースごとにスコアや実行時間を計算して関数post_mackerelに渡す、main関数を実装します。
use tools::*; #[async_std::main] async fn main() { let n_total_test = 100; let n_run_test = 10; let mut post_metrics: Vec<PostMetrics> = Vec::new(); for i in 0..n_run_test { let test_i = n_total_test / n_run_test * i; let in_file = format!("in/{:04}.txt", test_i); let out_file = format!("out/{:04}.txt", test_i); // let now = time::Instant::now(); { use std::fs::File; use std::process::Command; let program = "../AHC026/target/debug/main"; let _ = Command::new(program) .stdin(File::open(&in_file).unwrap()) .stdout(File::create(&out_file).unwrap()) .output() .unwrap(); } let execSec = now.elapsed().as_secs_f32(); // let input = std::fs::read_to_string(&in_file).unwrap_or_else(|_| { eprintln!("no such file: {}", in_file); std::process::exit(1) }); let output = std::fs::read_to_string(&out_file).unwrap_or_else(|_| { eprintln!("no such file: {}", out_file); std::process::exit(1) }); let input = parse_input(&input); let out = parse_output(&input, &output); let (score, _) = match out { Ok(out) => compute_score(&input, &out), Err(err) => (0, err), }; post_metrics.push(PostMetrics { test_i, score, execSec, }); } post_mackerel(post_metrics).await; }
main関数では、100のテストケースのうち0、10、20……に対してスコアと実行時間を計算してpost_metricsにpushして行き、最後にpost_mackerelを呼び出します。
各テストケースでは、入力ファイルと出力ファイルを指定して、作成したプログラムの実行ファイル（ここでは../AHC026/target/debug/main）を実行します。これで得た結果を元に、スコアを計算しています。
*3
コンテストで使ってみる
実際にAHC026に少し取り組んでみて、スコアや実行時間がどんな形で見えるか試してみました。
最初のスコア (score) のメトリックを見ると、1つのテストケースだけ正の得点で、他が0点となっていますね。 これは、コンテスト開始直後、サンプルケースから1つの入力のみに対応した出力をそのまま行うプログラムを最初に用意したためです。
その後、他のテストケースでも正の得点を得るまでに割と時間が掛かってしまっています。 これは、当初愚直に実装しようと思ったものの、あまりに効率が悪いのではと考えて効率的な実装を試してしまったためですね。 とりあえずスコアが出る実装を用意してビジュアライザの動きを見ることでわかることも多いので、愚直に実装することを迷わずにいたいです。
このように、投稿したスコアのグラフはコンテスト中に利用できるだけでなく、どの動きが良くどの動きが良くなかったかを後で復習する際にも活用することができそうです。 その際は、グラフアノテーション機能を利用して、特に良かった、悪かったポイントをメモしておくのも良いでしょう。
また、今回は*4テストケースごとのスコアや実行時間の差はあまり見て取れませんでしたが、特に長期のコンテストの場合はその辺りの差が見て取れる場合もあるかもしれません。
まとめ
この記事では、ヒューリスティックコンテストのスコアや実行時間を Mackerel に投稿してみました。 流石に数時間のコンテストでは難しいかもしれませんが、数週間に渡るものなら早い段階で投稿できる環境を整えるのも現実的な気がしました。 また、1人ではなく（ISUCONのような）複数人で取り組むようなタイプのコンテストだと、よりみんなで共通した見やすい情報を持てる価値が高いため、競技中や復習にうまく利用できそうです。
Mackerel は監視を行うためのサービスですが、使い方次第では自分自身の過去の行動を記録し、振り返るためにも活用することができます。 今後も色々な使い方を試して行きたいですね。
Mackerel Advent Calendar 2023、明日の担当は 
id:minemuracoffee さんです。
はてなリモートインターンシップ2021に参加しました
夏休みに3週間ほどはてなリモートインターンシップ2021に参加したので、参加記を書いていこうと思います。今年のはてなインターンは、前半1週間が講義パート、後半2週間が実践パートという構成でした。
講義パート
前半1週間の講義パートでは、Webサービス開発・運用について幅広い分野の講義を受け、課題に取り組みました。Kubernetesやマイクロサービスの講義は課題と繋がっていて、実践を通じて学ぶことができました。（例年通りなら講義資料が公開されたりするかもしれません）
実践パート
後半2週間の実践パートでは、事前の希望通りブックマークチームに配属されました！
配属されてからは、チームの方々や同じく配属された id:Mackyson さんと相談して、候補の中から取り組む課題を決定しました。
課題が決まると、まずはプランナーやデザイナーの方を含めたチーム全体で機能の詳細について相談し、取り組む方針や流れを決めていきました。仕様や進め方はこういう風に決まっていくんだなぁというのが体験できました。
序盤のタスクは id:Mackyson さんとペアプロの形式で進めていき、途中からは各々で作業を進めていきました。
技術スタックのページにもあるように、はてなブックマークの開発では主にScalaとPerlが使用されており、僕はScalaで記述されている箇所をメインで担当しました。Scalaは大学の課題などで触れた程度でしたが、業務でも関数型風に綺麗に書けている部分があったりして、やはり書き心地が良いなぁと思いました。
また、困ったときにはメンターやチームの方々にたくさん相談に乗っていただき、大変助かりました。
事前のタスク分割とスケジュール見積もりがしっかりしていたおかげか、実装はそれなりにスケジュール通りに進みました。僕は途中学会発表などで抜け出したりしましたが、ほぼ予定通りに動作確認、リリースまで行くことができました。
というわけで、追加した機能がこちら↓
記事にある通り、自分のブックマークを検索した際に、日付やブックマーク数での並び替え、検索対象の指定を行える機能です。タイトルで検索したのに本文の文字列が引っ掛かってしまうとか、大昔にブックマークした記事を見つけたい、なんてときに便利だと思います。
個人的にもこっそり使っているサービスなので、改善できたことがとても嬉しいです。便利になったのでもっと使おうと思います！
また、リリース後、特に目立った不具合がなかったことも良かったです。
最後に
企画の調整から実装、テスト、動作確認、リリースまでの、
最大限のサポートをしてくださったメンターやチームの方々には本当に感謝しています。ありがとうございました！
