JPYCv2 形式検証

外観

JPYC.updateAllowlister_unauthorized ​

名称・種別 ​

  • 名称: JPYC.updateAllowlister_unauthorized
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:804-807
  • 概要: owner でない呼び出し元は updateAllowlister を notOwner で revert する（権限・revert形）。
  • 仕様: 対象

型シグネチャ ​

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

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

和訳 docstring ​

認可（revert）。 オーナー以外の呼び出しは updateAllowlister を notOwner で revert する。

解説 ​

何を述べているか。 updateAllowlister（allowlister ロールの付け替え）の onlyOwner 検査が 最初のガード であるため、呼び出し元がオーナーでないとき、関数は本体に一切触れずに Except.error .notOwner を返します。証明はガードの if を偽側（if_neg）に倒すだけです。

直感。 updateAllowlister_auth（成功 ⇒ 呼び出し元 = オーナー）の対偶を、具体的なエラー名つきで述べたものです。transferOwnership_unauthorized と同型のロール回転・負側定理で、これでロール回転 4 関数すべての負側が揃います。

なぜ安全性に効くか。 権限のない呼び出しが「正しい理由（notOwner）で失敗する」ことまで固定します。オーナーだけが allowlister（V2 の許可リスト管理者）を付け替えられることの裏付けです。

図解 ​

Lean ソースコード ​

lean
/-- **Authorization (revert).** A non-owner caller reverts `updateAllowlister` with `notOwner`. -/
theorem updateAllowlister_unauthorized {s : State} {ctx : CallContext} {newAllowlister : Address}
    (h : s.owner ≠ ctx.sender) : updateAllowlister s ctx newAllowlister = .error .notOwner := by
  unfold updateAllowlister onlyOwner req; rw [if_neg h]; rfl

依存 ​