何が保証され、何が保証されないか
コード・証明・実行系の信頼の境界を読みます。
20.1 何を検査しているかを明示する
形式検証では、証明が実際に何を主張しているかを、厳密に読む必要があります。たとえば sort_correct は、ソートの性質を述べていますが、メモリ使用量・計算時間・外部ライブラリの動作までは保証しません。
| 対象 | どのように扱われるか |
|---|---|
| 証明項が命題の型を持つか | 証明カーネルが検査 |
| 帰納法で表した一般的な性質 | 命題と証明項に従って検査 |
| 実行側の所有権・借用 | 別の静的な使用規則で検査 |
| ネイティブ実行系・バックエンド | その実装を信頼する部分が残る |
extern で呼ぶ外部関数 | 宣言と実体の対応を、別途信頼する |
| 任意の実行の時間・メモリの上限 | 個別の証明や、ホストの制限が必要 |
20.2 check の成功の読み方
tauto check が成功しても、「プログラム全体が完全に安全」という断定にはなりません。検査した宣言の中で、どの仮定を使い、どの純粋な関数について何を示したかが大切です。axiom や extern の扱いも、信頼の境界に含まれます。
どの宣言がどの公理に依存しているかは、--json で確認できます。
tauto check examples/proofs.taut --json
出力の各宣言には、使った公理の一覧（axioms）が付きます。公理に頼らない宣言は、空のリストです。第 14 章の not_not は ["em"] になります。
20.3 実行時の型との対応
証明の世界の Nat は、理論上は任意に大きな自然数です。実行や抽出の場では、固定幅の整数で表されることがあります。上限を超える値が現れるプログラムでは、証明の世界の演算と実行環境の演算が食い違う可能性を、考える必要があります。
同様に、参照カウントによる shared な値は、条件によっては、循環参照のために解放できなくなる可能性があります。「所有権を検査する」ことと「資源のリークが一切ない」ことを、同じに考えないでください。
20.4 信頼の境界を小さくするには
実務的には、次の順序が有効です。
- 純粋な中心のロジックを、小さな関数として設計する。
- その関数の不変条件を証明する。
- 実行側が、同じ関数を呼ぶようにする。
- 境界をテストし、監査する。
証明の効果を最大にしながら、証明だけではカバーできない箇所を把握できます。
演習 20.1：sort が正しいことの証明と、ファイルから入力を読み取る機能の安全性は、別の問題です。その理由を説明してください。