JPYCv2 形式検証

外観

JPYC.initializeV1_not_reinitializable ​

名称・種別 ​

  • 名称: JPYC.initializeV1_not_reinitializable
  • 種別: theorem
  • モジュール: JpycFormalVerification.UpgradeabilityTheorems
  • ソース: JpycFormalVerification/UpgradeabilityTheorems.lean:93-106
  • 概要: 一度成功後、結果状態への 2 回目の initializeV1 は常に alreadyInitialized で revert する（再初期化不可）。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {O : JPYC.SigOracle} {s s' : JPYC.State} {ctx : JPYC.CallContext} {self : JPYC.Address} {tokenName tokenSymbol tokenCurrency : String} {tokenDecimals : JPYC.U8} {newMinterAdmin newPauser newBlocklister newRescuer newOwner : JPYC.Address}, Eq (JPYC.initializeV1 O s ctx self tokenName tokenSymbol tokenCurrency tokenDecimals newMinterAdmin newPauser newBlocklister newRescuer newOwner) (Except.ok s') → ∀ {ctx₂ : JPYC.CallContext} {self₂ : JPYC.Address} {name₂ symbol₂ currency₂ : String} {decimals₂ : JPYC.U8} {minterAdmin₂ pauser₂ blocklister₂ rescuer₂ owner₂ : JPYC.Address}, Eq (JPYC.initializeV1 O s' ctx₂ self₂ name₂ symbol₂ currency₂ decimals₂ minterAdmin₂ pauser₂ blocklister₂ rescuer₂ owner₂) (Except.error JPYC.Error.alreadyInitialized)

initializeV1 が一度成功したら、その結果状態に対する二度目の initializeV1 は（引数・文脈に関わらず）必ず alreadyInitialized で revert する、という 再初期化不可能 の定理です。

和訳 docstring ​

再初期化不可能。 成功した initializeV1 の後、二度目の initializeV1 は（呼び出し元・引数・文脈に関わらず）常に alreadyInitialized で revert する。

解説 ​

何を述べているか。 initializeV1 が成功して s' になったあと、s' に対する二度目の initializeV1（別の引数・別の文脈でもよい）は常に Except.error .alreadyInitialized を返します。証明は initializeV1_sets_version で s' の版数が 1 であることを使い、initializeV1_already_initialized を適用します（1 ≠ 0）。

直感。 「初期化は、宇宙でただ一度だけ」。一度ラッチが上がれば、誰がどんな引数で再挑戦しても二度と通りません。

なぜ安全性に効くか。 これが初期化の 一回限り性 の総まとめです。攻撃者が初期化を再実行してロールを乗っ取る、という典型的なプロキシ攻撃が原理的に不可能であることを示します。

図解 ​

Lean ソースコード ​

lean
/-- **Re-initialization impossible.** After any successful `initializeV1`, a second
`initializeV1` on the resulting state always reverts with `alreadyInitialized`
(regardless of caller, arguments, or block context). -/
theorem initializeV1_not_reinitializable {O : SigOracle} {s s' : State} {ctx : CallContext}
    {self : Address} {tokenName tokenSymbol tokenCurrency : String} {tokenDecimals : U8}
    {newMinterAdmin newPauser newBlocklister newRescuer newOwner : Address}
    (h : initializeV1 O s ctx self tokenName tokenSymbol tokenCurrency tokenDecimals
      newMinterAdmin newPauser newBlocklister newRescuer newOwner = .ok s')
    {ctx₂ : CallContext} {self₂ : Address} {name₂ symbol₂ currency₂ : String} {decimals₂ : U8}
    {minterAdmin₂ pauser₂ blocklister₂ rescuer₂ owner₂ : Address} :
    initializeV1 O s' ctx₂ self₂ name₂ symbol₂ currency₂ decimals₂
      minterAdmin₂ pauser₂ blocklister₂ rescuer₂ owner₂ = .error .alreadyInitialized := by
  apply initializeV1_already_initialized
  rw [initializeV1_sets_version h]; decide

依存 ​