JPYCv2 形式検証

外観

JPYC.unAllowlist_unauthorized ​

名称・種別 ​

  • 名称: JPYC.unAllowlist_unauthorized
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:610-613
  • 概要: allowlister でない呼び出し元の unAllowlist は revert する（権限・revert形）。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ {s : JPYC.State} {ctx : JPYC.CallContext} {account : JPYC.Address}, Ne ctx.sender s.allowlister → Eq (JPYC.unAllowlist s ctx account) (Except.error JPYC.Error.notAllowlister)

呼び出し元がallowlisterでなければ、unAllowlist は notAllowlister で revert する、という認可（revert 形）定理です。

和訳 docstring ​

認可（revert）。 allowlister 以外の unAllowlist 呼び出しは revert する。

解説 ​

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

直感。 *_auth の対偶を、具体的なエラー名つきで述べたものです。「権限がなければ、ちょうどこのエラーで弾かれる」を保証します。

なぜ安全性に効くか。 権限のない呼び出しが「失敗する」だけでなく「正しい理由で失敗する」ことまで固定します。エラーコードが Solidity の require メッセージと 1:1 対応していることの裏付けにもなります。

図解 ​

Lean ソースコード ​

lean
/-- **Authorization (revert).** A non-allowlister caller reverts `unAllowlist`. -/
theorem unAllowlist_unauthorized {s : State} {ctx : CallContext} {account : Address}
    (h : ctx.sender ≠ s.allowlister) : unAllowlist s ctx account = .error .notAllowlister := by
  unfold unAllowlist onlyAllowlister req; rw [if_neg h]; rfl

依存 ​