JPYCv2 形式検証

外観

JPYC.upgradeTo ​

名称・種別 ​

  • 名称: JPYC.upgradeTo
  • 種別: def
  • モジュール: JpycFormalVerification.Upgradeability
  • ソース: JpycFormalVerification/Upgradeability.lean:131-139
  • 概要: upgradeTo(newImplementation)：_authorizeUpgrade(onlyOwner) を通すアップグレード入口（slot 書き込みは対象外）。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.State → JPYC.CallContext → JPYC.Address → Except JPYC.Error JPYC.State

UUPS の upgradeTo エントリポイントです。_authorizeUpgrade（= onlyOwner）を通せば成功しますが、実装スロット書き込みはスコープ外なので、モデル上の状態は変わりません。

和訳 docstring ​

upgradeTo(newImplementation)（upgradeability/UUPSUpgradeable.sol:82-85）。onlyProxy（抽象化・常に通過）の後 _authorizeUpgrade、実装スロット書き込みはスコープ外なので認可通過後のモデル状態は不変。

解説 ​

何を述べているか。 upgradeTo(newImplementation)（upgradeability/UUPSUpgradeable.sol:82-85）の写しです。onlyProxy（抽象化＝常に通過）の後に authorizeUpgrade を呼びます。実装スロットへ書き込む _upgradeToAndCallUUPS は スコープ外 なので、認可が通った後のモデル状態は元のまま（pure s）です。

直感。 「プロキシの実装（ロジック）を新しいアドレスに差し替える」操作です。本モデルが捉えるのは、その差し替えを 誰が認可できるか という一点 ―― すなわち onlyOwner のゲートです。実際のスロット書き換えやアップグレード後の delegatecall は EVM ストレージ配置に踏み込むため、明示的に対象外としています。

なぜ安全性に効くか。 upgradeTo_auth（成功 ⇒ オーナー）と upgradeTo_unauthorized（非オーナーは notOwner）として、アップグレード経路がオーナーに閉じていることが証明されています。upgradeTo がモデル状態を変えないこと（upgradeTo_ok）から、WF・供給保存も自明に保たれます。

図解 ​

Lean ソースコード ​

lean
/-- `upgradeTo(newImplementation)` —
`upgradeability/UUPSUpgradeable.sol:82-85`. `onlyProxy` (abstracted, always
passing) precedes `_authorizeUpgrade`; `_upgradeToAndCallUUPS` (the
implementation-slot write) is out of scope, so the modeled state is unchanged
once `_authorizeUpgrade` passes. -/
def upgradeTo (s : State) (ctx : CallContext) (newImplementation : Address) :
    Except Error State := do
  authorizeUpgrade s ctx newImplementation
  pure s

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/upgradeability/UUPSUpgradeable.sol:82-85

solidity
function upgradeTo(address newImplementation) external virtual onlyProxy {
    _authorizeUpgrade(newImplementation);
    _upgradeToAndCallUUPS(newImplementation, new bytes(0), false);
}

依存 ​