JPYCv2 形式検証

外観

JPYC.upgradeToAndCall_auth ​

名称・種別 ​

  • 名称: JPYC.upgradeToAndCall_auth
  • 種別: theorem
  • モジュール: JpycFormalVerification.UpgradeabilityTheorems
  • ソース: JpycFormalVerification/UpgradeabilityTheorems.lean:300-303
  • 概要: upgradeToAndCall によるアップグレード認可は owner のみが行える（権限）。
  • 仕様: 対象

型シグネチャ ​

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

upgradeToAndCall の成功は、呼び出し元がオーナーだったことを含意する、というアップグレード認可の定理です。

和訳 docstring ​

アップグレード認可。 upgradeToAndCall でアップグレードを認可できるのはオーナーのみ。

解説 ​

何を述べているか。 upgradeToAndCall が成功したなら s.owner = ctx.sender です。upgradeToAndCall_ok の第 1 成分を取り出します。

直感。 「upgradeToAndCall でアップグレードできた ⇒ オーナーだった」。アップグレード経路の認可が _authorizeUpgrade（onlyOwner）に集約されていることの帰結です。

なぜ安全性に効くか。 プロキシのロジック差し替えという最も強力な操作を、オーナーだけに許す保証です。鍵を握るオーナー以外は、実装を乗っ取れません。

図解 ​

Lean ソースコード ​

lean
/-- **Upgrade authorization.** Only the owner can authorize an upgrade via
`upgradeToAndCall`. -/
theorem upgradeToAndCall_auth {s s' : State} {ctx : CallContext} {impl : Address}
    (h : upgradeToAndCall s ctx impl = .ok s') : s.owner = ctx.sender := (upgradeToAndCall_ok h).1

依存 ​