JPYCv2 形式検証

外観

JPYC.initializeV1_already_initialized ​

名称・種別 ​

  • 名称: JPYC.initializeV1_already_initialized
  • 種別: theorem
  • モジュール: JpycFormalVerification.UpgradeabilityTheorems
  • ソース: JpycFormalVerification/UpgradeabilityTheorems.lean:82-91
  • 概要: 初期化済み状態（version≠0）からの initializeV1 は alreadyInitialized で revert する。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {O : JPYC.SigOracle} {s : JPYC.State} {ctx : JPYC.CallContext} {self : JPYC.Address} {tokenName tokenSymbol tokenCurrency : String} {tokenDecimals : JPYC.U8} {newMinterAdmin newPauser newBlocklister newRescuer newOwner : JPYC.Address}, Ne s.initializedVersion 0 → Eq (JPYC.initializeV1 O s ctx self tokenName tokenSymbol tokenCurrency tokenDecimals newMinterAdmin newPauser newBlocklister newRescuer newOwner) (Except.error JPYC.Error.alreadyInitialized)

すでに初期化済み（initializedVersion ≠ 0）の状態からは、initializeV1 は alreadyInitialized で revert する、という二重実行ガード（revert）の定理です。

和訳 docstring ​

二重実行ガード（revert）。 初期化済み状態からの initializeV1 は alreadyInitialized で revert する（先頭ガードが落ちる）。

解説 ​

何を述べているか。 s.initializedVersion ≠ 0 のとき、initializeV1 は本体に一切触れず Except.error .alreadyInitialized を返します。先頭ガードの if を偽側（req_neg）に倒すだけです。

直感。 「すでに初期化されていれば、初期化はちょうどこのエラーで弾かれる」。initializeV1_requires_uninitialized の対偶を、具体的なエラー名つきで述べたものです。

なぜ安全性に効くか。 再初期化攻撃が「失敗する」だけでなく「正しい理由で失敗する」ことを固定します。UUPS プロキシで実装の初期化が乗っ取られないという保証の、エラーレベルの裏付けです。

図解 ​

Lean ソースコード ​

lean
/-- **Double-execution guard (revert).** From any already-initialized state
(`initializedVersion ≠ 0`), `initializeV1` reverts with `alreadyInitialized` — the
very first guard fails. -/
theorem initializeV1_already_initialized {O : SigOracle} {s : State} {ctx : CallContext}
    {self : Address} {tokenName tokenSymbol tokenCurrency : String} {tokenDecimals : U8}
    {newMinterAdmin newPauser newBlocklister newRescuer newOwner : Address}
    (h : s.initializedVersion ≠ 0) :
    initializeV1 O s ctx self tokenName tokenSymbol tokenCurrency tokenDecimals
      newMinterAdmin newPauser newBlocklister newRescuer newOwner = .error .alreadyInitialized := by
  unfold initializeV1; rw [req_neg h]; rfl

依存 ​