JPYCv2 形式検証

外観

JPYC.initializeV2_locks_initializeV1 ​

名称・種別 ​

  • 名称: JPYC.initializeV2_locks_initializeV1
  • 種別: theorem
  • モジュール: JpycFormalVerification.UpgradeabilityTheorems
  • ソース: JpycFormalVerification/UpgradeabilityTheorems.lean:221-230
  • 概要: initializeV2 成功後は V1 の initializeV1 も恒久的に締め出される（ラッチが 2≠0）。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {O : JPYC.SigOracle} {s s' : JPYC.State} {ctx : JPYC.CallContext}, Eq (JPYC.initializeV2 O s ctx) (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)

initializeV2 が成功した後は、V1 の initializeV1 も恒久的にロックされる（alreadyInitialized で revert）、という 初期化の完全ロック の定理です。

和訳 docstring ​

初期化の完全ロック。 成功した initializeV2 の後は、V1 の initializeV1 も恒久的にロックされる（ラッチが 2 ≠ 0）。

解説 ​

何を述べているか。 initializeV2 が成功して s' になったあと、s' に対する initializeV1（任意の引数・文脈）は常に Except.error .alreadyInitialized を返します。initializeV2_sets_version で版数が 2 であることを使い、initializeV1_already_initialized を適用します（2 ≠ 0）。

直感。 「V2 まで進んだら、最初の初期化にすら戻れない」。ラッチは 0 → 1 → 2 と単調に進むだけで、決して巻き戻りません。

なぜ安全性に効くか。 初期化ラッチが 一方向 であることの総まとめです。アップグレード後にコントラクトを “未初期化” に見せかけて V1 初期化からやり直す、といった攻撃の余地がないことを示します。

図解 ​

Lean ソースコード ​

lean
/-- **Initializer fully locked.** After a successful `initializeV2`, even the V1
`initializeV1` is permanently locked out (the latch is `2 ≠ 0`). -/
theorem initializeV2_locks_initializeV1 {O : SigOracle} {s s' : State} {ctx : CallContext}
    (h : initializeV2 O s ctx = .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 [initializeV2_sets_version h]; decide

依存 ​