maintain-formal-verification-skill

形式検証スキルを保守する

Codex では、このスキルに従う前に、スキルごとの注意事項も含めてプラットフォームの対応表を読んでください。

GitHub Copilot では、このスキルに従う前に、スキルごとの注意事項も含めてプラットフォームの対応表を読んでください。

Muse では、このスキルに従う前に、スキルごとの注意事項も含めてプラットフォームの対応表を読んでください。

形式検証は、記述対象の性質を証明します。コードが変更されても検証が更新されなければ、もはや存在しないコードを記述したまま、検証に通り続けることがあります。これは証明のように見えるため、危険な状態です。このスキルは、/create-formal-verification-skill が生成した形式検証スキルや、名前を指定したコードに対してモデルチェッカー、証明器、またはコードレベルの検証ツールを実行するプロジェクトローカルのスキルを保守するための手順です。プロジェクトローカルのスキルは、エージェントがそのスキルを使う際に行う変更を扱います。このスキルは、そのスキルを使わずに行われたマージや編集、そして多くのコミットを経て積み重なった乖離を扱います。

結果

各チェックに結果を 1 つ付け、どれに該当するかを示してください。

• 同期済み：前回の同期以降に、チェックの記述対象を変える変更はなく、チェックに通ります。
• 更新済み：コードが変更され、検証が新しいコードを記述するようになり、チェックに通ります。
• バグ：検証は現在のコードを記述しており、コードが性質を満たしていません。これはコードに関する指摘であり、乖離ではありません。
• ブロック：チェックを再び適合させられなかったか、実行できませんでした。理由を正確に示してください。

更新済みとバグの両方に該当することもあります。更新によって検証が再びコードを記述するようになり、そのうえで性質が満たされない場合です。

編集範囲

編集するのは検証に限ります。つまり、モデル、ハーネス、プロパティファイル、形式検証スキルそのものです。ユーザーから依頼がない限り、実行中に製品コードを編集してはいけません。現在のコードでプロパティが失敗した場合、通すためにプロパティやモデルを弱めてはいけません。その失敗を報告してください。

手順

1. チェックを見つけます。 形式検証スキルに固定の名前はありません。そのため、名前ではなく機能から探します。つまり、名前を指定したコードに対してモデルチェッカー、証明器、または別の検証ツールを実行するプロジェクトスキルです。/create-verification-skill が作成するプロジェクトの verify スキルはアプリを操作するものであり、該当しません。見つかったもの、またはユーザーが指定したものをすべて読みます。各チェックについて、プロパティ、対象コード、境界と前提条件、実行コマンド、そしてそのコードを記述していることが最後に確認されたコミットを記録します。形式検証スキルが存在しない場合は、そこで終了し、/create-formal-verification-skill を案内してください。スキルに同期時のコミットが記録されていない場合は、検証ファイルを最後に変更したコミットを使い、そのことを明記してください。

2. 現状のまま実行します。 何かを変更する前に、各チェックを一度実行し、結果を記録してください。ここで合格しても、コードが正しいとは限りません。古い記述が依然として成り立っていることを示すだけです。ここでの失敗は、乖離かバグの可能性があります。手順 5 までは、どちらかを判断しないでください。

3. 対象コードの変更をすべて確認します。 同期コミットから現在のコミットまで、対象ファイルの差分を確認し、各コミットメッセージも読みます。移動したコードも確認します。対象の関数が名前を変えたり、分割されたり、別のファイルに移動したりしていても、引き続き対象コードです。また、チェックが保護する状態に触れる新しいコードも確認します。たとえば、同じフィールドに書き込む新しい関数などです。変更ごとに、次のいずれに当たるかを判断します。

   • 影響なし。 変更によって、検証で説明されている内容は何も変わりません。たとえば、書式、コメント、検証対象外のコードパスなどです。コミットメッセージではなく、モデルまたはハーネスに照らして確認します。
   • 検証がコードを説明しなくなっています。 ひとつの不可分なアクションだった手順がふたつに分かれた、分岐が追加または削除された、チェックが移動した、保護対象の状態に至る新しい経路が追加された、あるいは値の範囲が変わった場合です。モデルまたはハーネスを変更する必要があります。
   • 意図的に仕様が変わっています。 変更によってコードが保証する内容が変わり、その意図が変更箇所の証拠によって示されています。証拠には、ドキュメントコメント、テスト、変更履歴、コミットメッセージなどがあります。プロパティを変更し、その証拠を明記する必要があります。
   • 仕様が破られている可能性があります。 コードが変更されているのに、仕様が変わったことを示す証拠がありません。その後に失敗が発生した場合は、バグ候補として扱います。

4. 結果ではなくコードに基づいて更新します。 変更された各部分が、レビュアーが開いて確認できるコードを再び指すようにモデルまたはハーネスを変更します。また、コード内の不可分なステップひとつを、検証でもひとつのステップとして扱います。再実行する前に、コードに基づいて更新を記述します。チェックに合格しやすくなるように更新内容を調整してはいけません。プロパティは、意図的に仕様が変わった場合に限り変更します。古い記述、新しい記述、証拠を記録します。変更によって不適切にならない限り、境界値は維持します。境界値を下げる必要がある場合は、レポートにその理由を記載します。

5. 再実行し、各結果を判定します。

   • 合格： チェックが失敗する能力を失った記述でも、合格できる状態です。新しいチェックを削除したり、新しいステップの順序を入れ替えたりするなど、プロパティが防ごうとしている方法で新しいコードを壊し、チェックがそれを検出することを確認します。その後、変更を元に戻します。
   • 失敗： 反例を実際のコードで一つずつ再現します。あるステップがコード上で起こり得ない場合、検証が誤っています。検証を修正し、何が誤っていたかを記載します。すべてのステップが実際に起こり得る場合は、バグです。バグを導入したコミットを特定し、コード内で使われている言葉に沿って、反例を一連のステップとして説明し、被害を一文で述べます。実際のコードに対する簡単なテストや再現でバグが示された場合は、その証拠をレポートに追加します。製品コードにはコミットしません。

6. 形式検証スキルを更新します。 各チェックが対象とするコード、コマンド、境界値、前提条件、同期コミットを更新します。同期コミットは、確認したコミットに設定します。ブロックされたチェックの同期コミットは移動せず、その旨をレポートに記載します。その後、次のエージェントと同じ手順で形式検証スキルを一度実行し、手順が引き続き実行できることを確認します。

レポート

チェックごとに、ユーザーに次の内容を伝えます。

• 結果と、確認したコミット。
• 検証で何を変更したか、その理由。変更ごとに、コードの構造が変わったためか、証拠を伴う意図的な仕様変更のためかを簡潔に説明します。
• 再実行の結果と、更新後のチェックが引き続き失敗を検出できることを示すために行った変更。
• 各バグについて、平易な言葉での説明。コード内の言葉に沿った反例の各ステップ、被害、バグを導入したコミット。
• 検証で引き続き対象外となっている内容。対象に含めるべきなのに含まれていない新しいコードも記載します。

検証のずれによる失敗と、コードのバグによる失敗を明確に区別します。更新前は合格していたチェックが更新後に失敗した場合、以前の合格は古い記述に基づくものだったと明記します。

検証の更新は、製品の修正とは分けて独立した変更として行います。