JPYC.unBlocklist_unauthorized

名称・種別

名称: JPYC.unBlocklist_unauthorized
種別: theorem
モジュール: JpycFormalVerification.AccessControlTheorems
ソース: JpycFormalVerification/AccessControlTheorems.lean:275-277
概要: blocklister でない呼び出し元の unBlocklist は notBlocklister で revert する。
仕様: 対象

型シグネチャ

lean

∀ {s : JPYC.State} {ctx : JPYC.CallContext} {account : JPYC.Address}, Ne ctx.sender s.blocklister → Eq (JPYC.unBlocklist s ctx account) (Except.error JPYC.Error.notBlocklister)

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

解説

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

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

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

図解

Lean ソースコード

lean

theorem unBlocklist_unauthorized {s : State} {ctx : CallContext} {account : Address}
    (h : ctx.sender ≠ s.blocklister) : unBlocklist s ctx account = .error .notBlocklister := by
  unfold unBlocklist onlyBlocklister req; rw [if_neg h]; rfl

JPYC.unBlocklist_unauthorized ​

名称・種別 ​

型シグネチャ ​

解説 ​

図解 ​

Lean ソースコード ​

依存 ​

JPYC.unBlocklist_unauthorized

名称・種別

型シグネチャ

解説

図解

Lean ソースコード

依存