JPYCv2 形式検証

外観

JPYC.authorizeUpgrade_auth ​

名称・種別 ​

  • 名称: JPYC.authorizeUpgrade_auth
  • 種別: theorem
  • モジュール: JpycFormalVerification.UpgradeabilityTheorems
  • ソース: JpycFormalVerification/UpgradeabilityTheorems.lean:252-255
  • 概要: _authorizeUpgrade は owner のときのみ成功する（権限）。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {s : JPYC.State} {ctx : JPYC.CallContext} {impl : JPYC.Address}, Eq (JPYC.authorizeUpgrade s ctx impl) (Except.ok Unit.unit) → Eq s.owner ctx.sender

authorizeUpgrade の成功は、呼び出し元がオーナーだったこと（s.owner = ctx.sender）を含意する、という認可定理です。

和訳 docstring ​

認可。 _authorizeUpgrade はオーナーのみが成功できる。

解説 ​

何を述べているか。 authorizeUpgrade が成功（.ok ()）したなら s.owner = ctx.sender、すなわち呼び出し元がオーナー本人だったことが導けます。authorizeUpgrade は onlyOwner そのものなので、req_ok で通過条件を取り出します。

直感。 「アップグレード認可が通った ⇒ オーナーが呼んだ」。UUPS の認可フックの中身が onlyOwner であることの、定理としての表れです。

なぜ安全性に効くか。 プロキシのアップグレードという最強の操作を、オーナーに閉じ込めます。これがアップグレード経路全体（upgradeTo / upgradeToAndCall）の認可の根です。

図解 ​

Lean ソースコード ​

lean
/-- **Authorization.** `_authorizeUpgrade` succeeds only for the owner. -/
theorem authorizeUpgrade_auth {s : State} {ctx : CallContext} {impl : Address}
    (h : authorizeUpgrade s ctx impl = .ok ()) : s.owner = ctx.sender := by
  unfold authorizeUpgrade onlyOwner at h; exact req_ok h

依存 ​