create-formal-verification-skill

形式検証スキルを作成する

テストで確認できるのは、誰かが書こうと考えたケースです。形式検証では、定めた範囲内のあらゆるケースを確認します。モデルにおけるすべてのステップ順序、上限までのすべての入力、あるいはすべての入力が対象です。このスキルでは、リポジトリ内で形式検証が最も重要な箇所を見つけ、その箇所の特性を1つ検証し、次のエージェントがその特性に照らして変更を確認できる、プロジェクト固有のスキルを残します。このスキルは、作業の途中で初めて読み、あなたの作業を見たことがないエージェントにもわかるように書いてください。ユーザーが検証言語を学ばなくても、結果を信頼して行動に移せるようにする必要があります。

コードから対象を選ぶ

コードベースを根拠に回答し、観察できないことだけをユーザーに尋ねてください。ユーザーが領域やバグを指定している場合は、そこから始めます。

良い対象とは、コードが約束していることのうち、破られるとユーザーに害が及び、しかもその原因となるケースをテストで確認できることがほとんどないものです。リポジトリで最も重要な対象を選び、検証しやすさだけで選ばないでください。

問いに応じてツールを選ぶ

モデルチェッカー、証明支援系、SMT を利用する検証ツール、その他のツールの中から、最小のコストで問いに答えられるものを選びます。イベントが望ましくない順序で発生するかを調べる場合は、設計を小さなモデルで表すモデルチェッカーが通常適しており、あらゆる言語でのデフォルトは TLA+ です。メモリ安全性、オーバーフロー、データ構造の不変条件のように、コード自体があらゆる入力に対して正しく動作するかを調べる場合は、通常、コード上で動作する検証ツールが適しています。この言語で動作する検証ツールがなければ、その旨を伝え、関数の手書きモデルではなく、生成した入力で実際のコードをテストしてください。上限では不十分で、すべてのサイズで成り立つ必要がある特性は、証明が必要になる場合があります。リポジトリの開発者がインストールして実行できるツールを優先し、それを選んだ理由もユーザーに伝えてください。

優れたスキルの条件

• コードに忠実であること。 モデルや証明のすべての部分が、レビュアーが開いて確認できるコードに対応していること。検証で不可分な1ステップとして扱う処理は、コード上でも不可分な1ステップであること。名前はこのリポジトリから選ぶこと。
• 失敗を検出できること。 一度も失敗を確認したことのないチェックでは、何も証明できません。チェック対象のコードからチェックを削除したり、ステップの順序を入れ替えたりした壊れたバリアントで、各特性が失敗することを示してください。
• 検出結果をそのまま報告すること。 現在のコードが特性に違反している場合は、コードで使われている用語で反例を報告してください。合格させるために特性やモデルを弱めてはならず、ユーザーから依頼されない限り、プロダクトコードも変更しないでください。
• 範囲を正直に伝えること。 何を、どの上限と仮定の下で検証したか、何を対象外としたかを伝えてください。合格が保証するのはモデルまたは上限の範囲であり、システム全体ではありません。
• ツールなしでも読めること。 特性と、それが破られた場合の被害を、それぞれ平易な1文で述べてください。反例は、コード上の用語で短いステップの列として説明してください。
• 再実行が手軽であること。 コマンドは1つにし、ツールのバージョンを再現可能にして、次のエージェントが関連する変更のたびに使える短い実行時間にしてください。
• コードと歩調を合わせること。 各チェックが対象とするファイルと関数、および検証内容を最後に確認したコミットを記録してください。そのコミット以降に対象コードが変更されている場合、次のエージェントが検証を再確認する必要があるとわかるようにしてください。

verify スキルを作成する

対象領域の名前と、使用するタイミングを記載したフロントマター付きのプロジェクトローカルなスキルを作成してください。フロントマターがないと、スキルは登録されません。スキルだけを読んだ次のエージェントが、変更が検証対象のコードに影響するかどうかを判断し、チェックを実行し、実際のバグとモデル化の誤りを見分け、意図した変更に合わせて検証を更新できる必要があります。カバレッジ記録と同期コミットをスキルに記載し、検証が新しいコミットのコードを反映していると確認できてから、同期コミットを先に進めるよう次のエージェントに伝えてください。このリポジトリで実際に使われているコマンド、パス、用語を使い、プレースホルダーは残さないでください。

チェックが TLA+ モデルの場合は、次のエージェントに、すべての結果を pstack の statechart スキルで読むよう伝えてください。これは、チェッカーが見つけた各不変条件違反について、最短経路を平易な言葉で示し、変更によってどの違反が修正されたかを示します。チェックに合格すると、statechart スキルがシステムの状態遷移を図にします。statechart スキルは名前で参照してください。コマンド、オプション、ファイルパスはリリースやマシンによって異なるため、生成するスキルやスクリプトには一切コピーしないでください。

引き継ぐ前に実証する

生成したスキルに従い、次のエージェントとして、実際のコードのプロパティを壊す一時的な変更で一度実行してください。チェックで問題を検出できなければなりません。その後、一時的な変更を取り消し、チェックが元の状態、つまり合格する状態、または報告する指摘事項だけで失敗する状態に戻っていることを確認してください。一度も実行されていない verify スキルは草案です。スキルが問題を検出できない場合や、手順が実行できない場合は、一時的な変更ではなく、スキルまたは検証を修正してください。

引き継ぎ

何を検証したか、どのツールを使い、その理由は何か、検証の範囲、チェックで見つかった内容を平易な言葉で、実行方法、そして対象外の内容をユーザーに伝えてください。近接する対象が見つかった場合に限り、2つ目の対象を提案してください。検証を再確認せずに変更した後で検証を整合させるには、/maintain-formal-verification-skill を参照するようユーザーに案内してください。