AutoVerusは40時間の証明執筆を3回のLLM呼び出しに変える。秘訣は諦めるタイミングを知ることだ。
AutoVerusはLLMエージェントのネットワークを用いてRustコードのVerus正しさ証明を生成し、SMTソルバーのフィードバックによって駆動される生成・修復・ dischargeループにより、90%以上の証明義務を自動化する。
形式的検証で最も難しいのは、検証器そのものではない。証明を書くことだ。 熟練のRustエンジニアにMicrosoft…
rust
9 posts
LLMはRustコードを生成できる。形式的証明は全く別の問題だ。
大規模言語モデルは驚くほど質の高いRustコードを書くが、形式的証明を求めると、不変条件を幻覚で見つけ、どの検証器も受け付けない構文をでっち上げる。それらが実際に正しい部分、壊れる部分、それでも使う方法を解説する。
LLMはコンパイルできても通るRustを書ける。しかし、すべての可能な入力に対してコードが正しいことを保証する形式的証明を書くのは、今のところ信頼できない。…
一行の証明も書かずに Rust コードの正しさを証明できるが、状態空間が代償となる
Kani のようなモデル検査ツールを使えば、形式的証明の代わりに表明で Rust の性質を検証できる。問題は、ループの境界が小さくないときに何が起きるかだ。
一行の証明も書かずに Rust コードの正しさを証明できる。その仕事をするのがモデル検査器であり、現時点で Rust に最も実用的なものは AWS が開発した Kani だ。通常の Rust の表明を書けばよい。Kani…
依存ライブラリがディスク上の任意のファイルを読める。cap-std は許可を求めさせる
Rust の標準ライブラリはあらゆる依存ライブラリに対して、暗黙的なファイルシステム権限を付与する。cap-std はそれを能力ベースの API に置き換え、コードがパスを開く前にそのアクセス権を証明することを強制する。
依存ツリーのどのクレートも、 を開いたり、 ディレクトリに書き込んだり、プロジェクト内のすべてのファイルを列挙したりできる。Rust の標準ライブラリは許可を求めない。 を呼べるコードなら、オペレーティングシステムが許すあらゆるパスに触れる権限を持つものとして扱う。 cap-std はこの前提を覆す。Rust の…
throw するのをやめて、エラーを返すべきか
例外を投げると、型システムから失敗の経路が見えなくなる。明示的なエラー返却がコードをより正直にする理由と、それを苦痛なく導入する方法。
関数のシグネチャは を返すと言っている。嘘だ。実際には を返すか、爆発するかのどちらかだ。型システムはその後者の分岐を知らない。 これが例外ベースのエラーハンドリングの根本的な不誠実さだ。すべての…
Rustのnewtypeで、誤った状態をコンパイル時に無償で表現不能にする
1フィールドのラッパー構造体が、1バイトのオーバーヘッドも増やさずに単位混在バグや型の混同を防ぐ。
のユーザIDを、注文IDを期待する関数に渡しても、Rustは文句を言わない。両方とも だ。コンパイラは同じ型を見ているので、助けてくれない。実行時に気づく。通常は本番環境で、通常は安全だと思っていたリファクタリングの後だ。 これこそが、newtypeが存在する理由、つまり排除すべきバグの類型だ。…
RustでMutation Testingは機能する——ただしコンパイル時間が悲鳴を上げる
cargo-mutantsは、コードを検証したふりをしているテストを見つけ出す。Rustでのmutation testingの仕組み、何が捉えられるのか、そしてコンパイル時間のコストに見合う価値があるかを解説する。
100%のline coverageがある。すべての分岐が実行されている。すべての関数が呼ばれている。それなのに、誰かが価格ロジックのをに変えてテストを実行しても、すべて通ってしまう。…
Rustのプロパティベーステストが単体テストでは見逃すバグを見つける
例ベースのテストは思いついた入力だけをカバーする。プロパティベースのテストはランダムデータを生成し、不変条件を検証し、失敗を最小の反例まで縮小する。
関数を書いた。 と でテストして、パスした。リリースした。 ユーザーが1要素のスライスを渡すと、関数はそれを黙って落とす。Issueが立つ。テストファイルを見つめながら、こんな当たり前のことにどうして気づかなかったのかと思う。…
Rustのランタイムcontractsはリリースビルドで無料にできるが、コンパイラは勝手にやってくれない
Rustはdebug assertionsを自動で除去するが、本物のdesign-by-contractにはdebug_assert!以上のものが必要だ。リリースバイナリーから完全に消えるゼロコストのランタイムcontractsを作る方法を紹介する。
Rustは開発中にランタイムcontractsを強制し、リリースビルドから完全に消し去ることができる。ただし、この言語はcontractsを第一級の概念として扱っていない。ビルディングブロックは手に入るが、自分で配線を引く必要がある。…