JPYCv2 形式検証

外観

JPYC.upgradeToAndCall ​

名称・種別 ​

  • 名称: JPYC.upgradeToAndCall
  • 種別: def
  • モジュール: JpycFormalVerification.Upgradeability
  • ソース: JpycFormalVerification/Upgradeability.lean:141-148
  • 概要: upgradeToAndCall(newImplementation,data)：upgradeTo に後続 delegatecall を加えた入口（slot/呼び出しは対象外）。
  • 仕様: 対象外

型シグネチャ ​

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

UUPS の upgradeToAndCall エントリポイントです。upgradeTo と同様にオーナー認可だけがモデル化対象で、アップグレード後の delegatecall はスコープ外。状態は変わりません。

和訳 docstring ​

upgradeToAndCall(newImplementation, data)（upgradeability/UUPSUpgradeable.sol:95-103）。upgradeTo と同様、認可後のモデル状態は不変。アップグレード後の data の delegatecall はスコープ外。

解説 ​

何を述べているか。 upgradeToAndCall(newImplementation, data)（upgradeability/UUPSUpgradeable.sol:95-103）の写しです。upgradeTo と同じく authorizeUpgrade（= onlyOwner）を通し、認可後のモデル状態は元のまま（pure s）です。アップグレード後に data を delegatecall する部分は スコープ外 です。

直感。 「実装を差し替え、続けて初期化用の関数呼び出し（data）も実行する」操作です。upgradeTo に “アップグレード直後のコールバック” を足したものと考えられます。やはりモデルが捉えるのは認可ゲート（onlyOwner）の一点です。

なぜ安全性に効くか。 upgradeToAndCall_auth（成功 ⇒ オーナー）と upgradeToAndCall_unauthorized（非オーナーは notOwner）として、こちらの経路もオーナーに閉じていることが証明されています。モデル状態を変えないこと（upgradeToAndCall_ok）から WF・供給保存も保たれます。

図解 ​

Lean ソースコード ​

lean
/-- `upgradeToAndCall(newImplementation, data)` —
`upgradeability/UUPSUpgradeable.sol:95-103`. As `upgradeTo`, plus a post-upgrade
`delegatecall` of `data` that is out of scope; the modeled state is unchanged once
`_authorizeUpgrade` passes. -/
def upgradeToAndCall (s : State) (ctx : CallContext) (newImplementation : Address) :
    Except Error State := do
  authorizeUpgrade s ctx newImplementation
  pure s

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/upgradeability/UUPSUpgradeable.sol:95-103

solidity
function upgradeToAndCall(address newImplementation, bytes memory data)
    external
    payable
    virtual
    onlyProxy
{
    _authorizeUpgrade(newImplementation);
    _upgradeToAndCallUUPS(newImplementation, data, true);
}

依存 ​