Lean による形式化
「完全成功と判定したなら、必須チェックはすべて成功している」。これは、いくつかのテストケースだけでなく、判定規則そのものについて確かめたい性質です。
Lean 4 では判定規則を数学的なモデルとして定義し、このような性質を証明します。証明の対象はそのモデルです。実際に動く TypeScript や Rust との対応は、モデルから作ったテストケースを使って別に確認します。
票が抜けていないことを式で表す
掲示板の各位置は、「有効票として採用された」「提示されたが採用されなかった」「提示されなかった」の三つに分かれます。ゲストプログラム の票数を、Lean では自然数のモデルで表します。
validVotes ≤ seenIndicesCount ≤ treeSize
missingSlots = treeSize - seenIndicesCount
invalidPresentedSlots = seenIndicesCount - validVotes
excludedSlots = missingSlots + invalidPresentedSlots
この関係から、excludedSlots = 0 なら、未提示の位置も、提示されたのに採用されなかった位置もなく、validVotes = seenIndicesCount = treeSize と示せます。B の一票を入力から抜いた S1 なら missingSlots が増えるので、この条件を満たせません。
ゲストのモデルは、単に数を置くだけでなく、票を一件ずつ処理します。範囲外・重複インデックスを拒否し、初めて現れた位置を提示済みにした後、選択肢、コミットメント、包含証明を調べ、採用した票を加算します。この処理順序の下で、見た位置が重複せず範囲内にあり、採用数が提示位置数を超えないことを証明します。
証明している性質
| 領域 | 主張 | 代表的な定理 |
|---|---|---|
| ジャーナル | 上記の計数関係の下で、除外ゼロなら採用数・提示位置数・全位置数が一致する | slot_partition_total、excluded_zero_implies_no_slot_loss |
| 最終判定 | 完全成功なら必須チェックが成功し、未知のチェックがない | fully_verified_implies_all_required_success、fully_verified_implies_no_unknown_checks |
| 入力コミットメント | 票を並べ替えても、定めた順序で同じ符号化になる | canonical_encoding_permutation_invariant |
| ビットマップ | 下位ビットから詰めた長さと、取り出すビットが定義に一致する | pack_bits_length、pack_bits_get_bit |
| ゲスト集計 | 票を順に処理しても、候補別集計と採用数の関係が保たれる | processVotes_fold_invariant、accepted_votes_count_tally |
| 完全性 | ゲストモデルの除外ゼロから、未提示・不採用位置がないと導ける | zero_exclusion_guest_model_complete |
| 整数の上限 | 入力上限の下で、各カウンターが Rust の u32 に収まる | no_overflow_under_guest_bounds |
整数の証明では、treeSize と提示レコード数がそれぞれ 1,000,000 以下であることを仮定します。候補ごとの得票数も 1,000,000 以下になることは、その仮定から導かれる結論です。Rust の集計経路も入力上限を検査し、加算時のオーバーフローを拒否します。
モデルは formal/StarkBallotFormal/ の JournalCounts.lean、VerificationSummary.lean、InputCommitment.lean、Bitmap.lean、GuestModel.lean にあります。チェックの型などは Basic.lean が定義します。
実装との接続
モデルで正しいと示した規則と、実装した規則が違っていれば、モデルの証明だけではバグを防げません。そこで Lean から入力と期待結果の組を生成し、同じ入力を TypeScript・Rust に与えます。
flowchart TB M["Lean のモデル"] --> P["性質の証明"] M --> V["入力と期待結果を生成"] V --> T["TypeScript と照合"] V --> R["Rust と照合"]
生成するファイルは次の六つです。保存先は docs/formal/generated-vectors/ です。
| ファイル | 照合先 |
|---|---|
verification-summary-cases.json | TypeScript の最終判定 |
verification-display-cases.json | TypeScript の共有表示ルール |
check-definitions.json | チェック ID・分類・役割・必須条件 |
input-commitment-cases.json | TypeScript と Rust の票の順序・ハッシュ前のバイト列 |
bitmap-cases.json | TypeScript と Rust のビット配置・関連処理 |
guest-model-cases.json | 本番ゲストと処理を共有する Rust の検査経路 |
生成元は formal/Scripts/EmitTestVectors.lean です。各ファイルの種類、フィールド、モデル上限と実装定数の一致、内容の SHA-256 を消費側で調べ、古い値や別種のデータを受け入れないようにしています。内容のハッシュは、自身のハッシュ欄を除き、キー順を再帰的に揃えた空白なし JSON から計算します。
この照合が確認するのは生成ケースの対応です。Rust ゲスト全体や画面描画全体を形式的に証明したことにはなりません。また、SHA-256、RISC Zero、コンパイラーや実行環境の正しさは、このモデルから導く結論ではなく前提です。
証明と生成物を点検する
docs/formal/formal-report.json に主張と前提を、formal-audit.json に定理のハッシュ、公理への依存、証明の点検結果、保存した生成ファイル全体のハッシュを記録します。ファイル全体のハッシュと、前節の JSON 内容のハッシュは計算対象が違います。
証明に未完成を許す sorry や、手書きのプロジェクト固有公理はありません。定理の依存は #print axioms で調べます。ビットを取り出す pack_bits_get_bit では有限の組み合わせを native_decide で計算しており、その生成された判定用公理も依存先として記録します。
| コマンド | 行うこと |
|---|---|
pnpm formal:build | Lean のビルド |
pnpm formal:report / pnpm formal:report:check | 主張・前提の出力 / 最新性確認 |
pnpm formal:vectors / pnpm formal:vectors:check | テストケースの出力 / 最新性確認 |
pnpm formal:audit / pnpm formal:audit:check | 証明・生成物の点検記録の出力 / 最新性確認 |
pnpm formal:test:ts | TypeScript と生成ケースの照合 |
pnpm formal:verify | 上記の検査と生成 JSON の整形確認をまとめて実行 |
Rust の生成ケース照合は Rust テストのワークフローで実行します。公開ソースを作る前にも Lean をビルドして pnpm formal:verify を実行するため、生成物が古い状態や照合に失敗する状態では公開処理を進められません。