JPYCv2 形式検証

外観

JPYC.unAllowlist_clears ​

名称・種別 ​

  • 名称: JPYC.unAllowlist_clears
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:619-621
  • 概要: 成功した unAllowlist は許可登録フラグを 0 に戻す（効果）。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {account : JPYC.Address}, Eq (JPYC.unAllowlist s ctx account) (Except.ok s') → Eq (s'.allowlisted account) 0

unAllowlist の成功は allowlisted[account] = 0 をもたらす、という効果定理です。

解説 ​

何を述べているか。 unAllowlist が成功した結果状態では allowlisted[account] = 0 です。unAllowlist_ok と setAllowlisted_self から従います。

直感。 「特権を剝奪したら、ちゃんとフラグが 0 に戻る」を確認します。

なぜ安全性に効くか。 解除が確実にフラグを下ろすことで、剝奪後のアカウントが上限超の送金を続けられないことを保証します。

図解 ​

Lean ソースコード ​

lean
theorem unAllowlist_clears {s s' : State} {ctx : CallContext} {account : Address}
    (h : unAllowlist s ctx account = .ok s') : s'.allowlisted account = 0 := by
  obtain ⟨_, rfl⟩ := unAllowlist_ok h; exact setAllowlisted_self s account 0

依存 ​