JPYCv2 形式検証

外観

JPYC.authorizeUpgrade_unauthorized ​

名称・種別 ​

  • 名称: JPYC.authorizeUpgrade_unauthorized
  • 種別: theorem
  • モジュール: JpycFormalVerification.UpgradeabilityTheorems
  • ソース: JpycFormalVerification/UpgradeabilityTheorems.lean:257-261
  • 概要: owner でない呼び出し元は _authorizeUpgrade で notOwner により拒否される（権限・revert形）。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {s : JPYC.State} {ctx : JPYC.CallContext} {impl : JPYC.Address}, Ne s.owner ctx.sender → Eq (JPYC.authorizeUpgrade s ctx impl) (Except.error JPYC.Error.notOwner)

呼び出し元がオーナーでなければ、authorizeUpgrade は notOwner で revert する、という認可（revert）の定理です。

和訳 docstring ​

認可（revert）。 非オーナーの _authorizeUpgrade は notOwner で revert する。

解説 ​

何を述べているか。 s.owner ≠ ctx.sender のとき、authorizeUpgrade は Except.error .notOwner を返します。onlyOwner ガードを偽側（req_neg）に倒すだけです。

直感。 authorizeUpgrade_auth の対偶を、具体的なエラー名つきで述べたものです。「オーナーでなければ、ちょうど notOwner で弾かれる」。

なぜ安全性に効くか。 非オーナーによるアップグレード認可が「正しい理由で失敗する」ことを固定します。悪意ある第三者が実装を差し替える経路が閉じていることの、エラーレベルの裏付けです。

図解 ​

Lean ソースコード ​

lean
/-- **Authorization (revert).** A non-owner caller is rejected by
`_authorizeUpgrade` with `notOwner`. -/
theorem authorizeUpgrade_unauthorized {s : State} {ctx : CallContext} {impl : Address}
    (h : s.owner ≠ ctx.sender) : authorizeUpgrade s ctx impl = .error .notOwner := by
  unfold authorizeUpgrade onlyOwner; exact req_neg h

依存 ​