JPYCv2 形式検証

外観

形式手法 入門・用語集 ​

このページは、JPYCv2（FiatTokenV2）の 形式検証カタログ を、形式手法に なじみのない読者でも読み解けるようにするための入門ガイドです。専門知識がなくて も、各宣言（定義・定理）のページで何が語られているのかを理解できることを目標と しています。

1. このカタログは何か ​

JPYCv2 は、Ethereum 上で動く日本円ステーブルコイン（JPYC）のスマートコントラクト です。お金を扱うため、「バグがないこと」が極めて重要です。

通常の開発では テスト によって品質を担保します。テストは「いくつかの具体的な 入力を試して、期待どおりに動くか」を確認します。しかしテストは 試した入力 しか カバーできません。

このプロジェクトでは 形式検証（formal verification） という、より強力な方法を 使います。形式検証は「考えうる すべての 入力に対して、ある性質が必ず成り立つ」 ことを、数学の証明として厳密に示します。証明は Lean 4 という証明支援系 （proof assistant）でコンピュータがチェックするため、人間の見落としが入り込みませ ん。

  • テスト：「この入力では大丈夫だった」（有限個の確認）
  • 形式検証：「どんな入力でも大丈夫である」（数学的な保証）

📌 重要： Lean は lake build の時点で証明をすべて検査します。証明に穴 （sorry）があったり、論理が破綻していたりすると、ビルドが 失敗 します。 つまり「ビルドが通っている」こと自体が「証明が完結している」ことの証拠です。

2. モデル化の基本方針 ​

私たちは Solidity のコントラクトをそのまま検証できるわけではありません。そこで、 コントラクトの挙動を Lean の世界に 忠実に写し取った「モデル」 を作ります。

  • 写し取る粒度は 「Solidity の文（statement）レベル」 です。各 external 関数の 制御フロー、require / modifier のガード、mapping へのアクセス、msg.sender の使い方を 1 対 1 で再現します。
  • すべての Lean 定義には、対応する Solidity ソースの ファイル:行 を注釈として 付けています（カタログ各ページの「対応 Solidity ソースコード」欄）。
  • EVM のバイトコード・ガス・ストレージのスロット配置といった低レイヤは 対象外 として抽象化します（詳しくは §9）。

3. コア用語集 ​

ここからは、カタログのページに頻出する基本概念を、ひとつずつ説明します。

3.1 State（状態） ​

State は、コントラクトのストレージ（保存領域）をまるごと写し取った構造体です。 残高 balances、許可額 allowed、各種ロール（owner など）、paused フラグ、 署名管理の情報などを、すべてフィールドとして持ちます。

Solidity の mapping(address => uint256) のように「キーが無ければ 0」という マッピングは、Lean では 全域関数（Address → U256）として表現します。「まだ 書き込んでいないアドレスは残高 0」という意味です。

3.2 U256 と BitVec（機械語） ​

Solidity の uint256 は「256 ビットの符号なし整数」です。これを Lean では U256 := BitVec 256（256 ビットのビット列）として表します。uint8 は U8、 bytes32 は Bytes32 です。

ポイントは、BitVec は 固定長 なので、普通の整数と違って「桁あふれ（オーバー フロー）」が起こりうる、ということです。

3.3 Except と revert モデル（成功と失敗） ​

Ethereum のトランザクションは、途中で条件を満たさないと revert（巻き戻し） します。revert すると、それまでの状態変更はすべて 無かったこと になります。

これを Lean では Except（例外つきの結果）で表現します。各 external 関数は

State → CallContext → Args → Except Error State

という型を持ちます。意味は次のとおりです。

  • 成功した場合：Except.ok 新しいState（.ok ＝ 正常終了）
  • revert した場合：Except.error e（.error ＝ 失敗）。e は失敗理由 （Error）で、e.revertMessage が オンチェーンのエラー文字列をそのまま 返し ます（例："Pausable: paused"）。

「revert したら状態は変わらない」という性質も、思い込みではなく 定理として証 明 しています（各関数の *_revert_noop）。

3.4 checked 演算 add? / sub?（あふれ検知つきの足し算・引き算） ​

Solidity 0.8 以降は、整数演算でオーバーフロー / アンダーフローが起きると自動的に revert します。これをモデル化したのが add?（足し算）と sub?（引き算）です。

  • add? a b：a + b が 256 ビットに収まれば .ok (a+b)、あふれるなら .error arithmeticOverflow
  • sub? a b：b ≤ a なら .ok (a-b)、b > a（マイナスになる）なら .error arithmeticUnderflow

「？」の付いた演算は「失敗するかもしれない演算」という目印です。残高や供給量の 更新は必ずこの checked 演算を通すので、勝手に桁あふれして数字が壊れることはあり ません。

3.5 CallContext（呼び出しの文脈） ​

CallContext は、Solidity でいう msg.sender（呼び出し元アドレス）や、 block.timestamp（現在時刻）、block.chainid（チェーン ID）などをまとめたもの です。権限チェックや署名の有効期限の判定に使います。

3.6 WF（well-formedness 不変条件） ​

WF（ill-formed の反対、「整合している」状態）は、状態が満たすべき 健全性の前提 です。具体的には：

  • blocklisted / allowlisted / authorizationStates といった「フラグ」は、 ガス節約のため uint256 で持っていますが、値は必ず 0 か 1 であること。
  • initializedVersion（初期化バージョン）は 0・1・2 のいずれか であること。

すべての状態変更関数は「WF を保つ」ことが証明されています（*_wf）。つまり、 正規の操作だけを行っている限り、状態が壊れた値（フラグが 2 など）になることは ありません。

3.7 SupplyConserved（供給保存） ​

このプロジェクトの 中心的な安全性 です。

SupplyConserved s  :⇔  s.totalSupply = （全アカウントの balances の総和）

つまり「記録上の総供給量」と「実際に配られている残高の合計」が常に一致する、 ということです。transfer / transferFrom は総供給を変えず、mint は増やし、 burn は減らしますが、いずれの場合も この等式が崩れない ことを証明していま す（*_conserves）。お金が勝手に湧いたり消えたりしない、という保証です。

3.8 SigOracle（署名オラクル） ​

permit（EIP-2612）や transferWithAuthorization（EIP-3009）は、電子署名を使い ます。署名の検証には Ethereum の ecrecover（署名から署名者アドレスを復元する関 数）が必要ですが、その 内部実装の正しさはこのプロジェクトの対象外 です。

そこで、署名まわりを SigOracle（信頼できる「神託」）として抽象化します。重要なの は、安全性の定理が 「どんなオラクルであっても成り立つ」 ように書かれている点で す（オラクルを variable として全称化）。これは「署名検証が具体的に何を返そうと、 リプレイ防止や有効期限チェックといった性質は崩れない」ことを意味します。

3.9 frame（フレーム性）と no-op on revert ​

  • frame（フレーム性）：ある操作が、関係のないアカウント の残高などを変え ないこと。例えば transfer from to は、from・to 以外のアカウント残高に一切 影響しません（transfer_frame）。
  • no-op on revert：revert したときは状態がまったく変わらないこと （*_revert_noop）。EVM のロールバックを State.afterCall でモデル化しています。

4. 定理が「証明すること」と「証明しないこと」 ​

形式検証の価値は、何を保証し、何を保証しないか を明確にできる点にあります。

✅ 証明していること（モデル上で） ​

  • 制御フローの忠実性：各 external 関数のガード（require / modifier）が ソースと 1 対 1 で再現されている。
  • 権限（authorization）：特権機能は対応するロール保有者しか成功させられない （*_auth / *_unauthorized）。
  • 算術の安全性：残高・供給・許可額の更新は checked 演算を通り、桁あふれで 壊れない。
  • 不変条件の保存：あらゆる操作が WF と SupplyConserved を保つ。
  • リプレイ防止 / 一回限り性：permit の nonce 増加、EIP-3009 の authorization 使用済みマーク、キャンセル後の使用不可（*_no_replay ほか）。
  • 有効期限・受取人チェック：署名の有効ウィンドウ、receiveWithAuthorization の to == msg.sender など。
  • revert 時の状態不変、フレーム性、自己送金の安全性 など。

各性質と対応する定理の一覧は verification-report.md の「Property ↔ theorem map」 にまとまっています。

❌ 証明していないこと（スコープ外・前提） ​

  • EVM バイトコード / ガス / リエントランシ（オペコードレベルの挙動）。
  • delegatecall のストレージ・スロット配置とプロキシのストレージ衝突。UUPS の フェーズは「論理的な（アクセス制御の）性質」のみを証明し、スロット配置は抽象化 しています。
  • ecrecover の内部実装。信頼できる署名オラクル（SigOracle）として扱います。

⚠️ これらは「危険である」という意味ではなく、「このモデルの 証明の範囲外 として明示的に切り出している」という意味です。前提と限界を正直に示すこと自体が、 監査品質（audit-grade）の検証における重要な作法です。

5. カタログ各ページの読み方 ​

カタログの各ページ（宣言ごと）は、次の順序で構成されています。

欄内容
名称・種別宣言の完全修飾名と種別（def / theorem / structure …）
型シグネチャその宣言の型（定理なら「主張している命題」そのもの）
和訳 docstring原文（英語）docstring の日本語訳
丁寧な和文解説直感・背景・なぜ安全性に効くか（非専門家向け）
図解制御フロー・状態遷移・依存関係などの Mermaid 図
Lean ソースコード定義（定理なら証明本文も含む）
対応 Solidity ソースコード元コントラクトの該当箇所（ファイル:行）
依存この宣言が参照している関連宣言へのリンク

定理ページの「型シグネチャ」は、その定理が証明している主張そのもの です。読み 方のコツは、→（ならば）、∀（すべての…について）、=（等しい）といった記号を 日本語の文として読み下すことです。たとえば

∀ {a b c}, add? a b = .ok c → sub? c b = .ok a

は、「どんな a, b, c についても、a + b が c として成功するならば、c - b は a として成功する」と読みます（足したら引いて戻る、という round-trip）。

6. もっと知りたい人へ ​