検証する実装を、どう確かめるか
票の抜けを検出するはずのプログラムに、票の抜けを見逃すバグがあったらどうなるでしょうか。暗号の仕組みが正しくても、チェックの呼び忘れや画面の判定ミスで誤って Verified と表示してしまう可能性があります。
そこで、既知の失敗を再現するテスト、さまざまな入力を作って試すテスト、条件を満たす限り成り立つことを数学的に示すモデルを組み合わせています。
| 方法 | 例 | 得られる確認 |
|---|---|---|
| 手書きのテスト | 必須チェックを一つ失敗させる | その場合に成功表示にならない |
| Property-based Testing | 票や Merkle ツリーの大きさ・順番を変えて多数生成する | 試した入力で仕様上の性質が崩れない |
| Lean による証明 | 最終判定を抽象モデルで定義する | そのモデルでは、完全成功なら必須チェックがすべて成功している |
三つは異なる穴を探します。手書きテストは経験した失敗を確実に残せます。生成テストは人が思い付かなかった組み合わせを探せます。Lean は抽象モデルの条件を証明できますが、そのモデルと実際の TypeScript・Rust が対応するかは、さらにテストで照合する必要があります。
特に防ぎたいのは、証拠が不足しているのに成功を表示することと、秘密を含むファイルを配布してしまうことです。これらは一つの関数だけでは決まらないため、単体テストから画面を通すテストまで を使って確認します。