JPYCv2 形式検証

外観

JPYC.authorizeUpgrade ​

名称・種別 ​

  • 名称: JPYC.authorizeUpgrade
  • 種別: def
  • モジュール: JpycFormalVerification.Upgradeability
  • ソース: JpycFormalVerification/Upgradeability.lean:124-129
  • 概要: _authorizeUpgrade：onlyOwner ゲートだけを持つ空本体のアップグレード認可関数。
  • 仕様: 対象外

型シグネチャ ​

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

UUPS のアップグレード認可フック _authorizeUpgrade です。本体は空で、onlyOwner ガードだけを行います（成功なら ()、非オーナーなら revert）。

和訳 docstring ​

_authorizeUpgrade(newImplementation)（v2/FiatTokenV2.sol:566-570、internal override onlyOwner {}）。onlyOwner ゲートの背後の空本体なので、観測可能な効果は認可チェックのみ。

解説 ​

何を述べているか。 _authorizeUpgrade(newImplementation)（v2/FiatTokenV2.sol:566-570、internal override onlyOwner {}）の写しです。本体は空で、観測可能な効果は onlyOwner による認可チェックだけです。新実装アドレスの引数は使われません（_newImplementation）。

直感。 「アップグレードを許可してよいのは誰か」を決める、UUPS の 唯一の認可ゲート です。OpenZeppelin の UUPS パターンでは、この空フックをオーバーライドして認可ポリシーを差し込みます。JPYC はここに onlyOwner を置き、「オーナーだけがアップグレードを認可できる」と定めています。

なぜ安全性に効くか。 authorizeUpgrade_auth（成功 ⇒ オーナーが呼んだ）と authorizeUpgrade_unauthorized（非オーナーは notOwner で revert）として、アップグレード権限がオーナーに閉じていることが証明されています。プロキシのロジック差し替えは最も強力な操作なので、この一点の認可が極めて重要です。なお、ERC-1967 実装スロットへの書き込みや onlyProxy 検査は EVM ストレージ配置に依存するため スコープ外（モデルでは状態不変）です（「証明しないこと」）。

図解 ​

Lean ソースコード ​

lean
/-- `_authorizeUpgrade(newImplementation)` — `v2/FiatTokenV2.sol:566-570`:
`internal override onlyOwner {}`. An empty body behind the `onlyOwner` gate, so
the only observable effect is the authorization check. -/
def authorizeUpgrade (s : State) (ctx : CallContext) (_newImplementation : Address) :
    Except Error Unit :=
  onlyOwner s ctx

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:566-570

solidity
function _authorizeUpgrade(address newImplementation)
    internal
    override
    onlyOwner
{}

依存 ​