JPYC.removeMinter_clears

名称・種別

名称: JPYC.removeMinter_clears
種別: theorem
モジュール: JpycFormalVerification.AccessControlTheorems
ソース: JpycFormalVerification/AccessControlTheorems.lean:357-361
概要: 成功した removeMinter は minter を無効化し許容額を 0 にする（効果）。
仕様: 対象

型シグネチャ

lean

∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {minter : JPYC.Address}, Eq (JPYC.removeMinter s ctx minter) (Except.ok s') → And (Eq (s'.minters minter) Bool.false) (Eq (s'.minterAllowed minter) 0)

removeMinter の成功は、そのミンターを無効化し（minters = false）、許可量を 0 にする、という効果定理です。

解説

何を述べているか。 removeMinter が成功すると s'.minters minter = false かつ s'.minterAllowed minter = 0 です。removeMinter_ok と setMinter_minters_self / setMinterAllowed_self から従います。

直感。 「発行権限を剝奪したら、フラグも残枠も消える」を確認します。

なぜ安全性に効くか。 残枠まで 0 にすることで、無効化したミンターが（再登録なしに）こっそり発行を続けられないことを保証します。

図解

Lean ソースコード

lean

theorem removeMinter_clears {s s' : State} {ctx : CallContext} {minter : Address}
    (h : removeMinter s ctx minter = .ok s') :
    s'.minters minter = false ∧ s'.minterAllowed minter = 0 := by
  obtain ⟨_, rfl⟩ := removeMinter_ok h
  exact ⟨setMinter_minters_self s minter false, setMinterAllowed_self _ minter 0⟩

JPYC.removeMinter_clears ​

名称・種別 ​

型シグネチャ ​

解説 ​

図解 ​

Lean ソースコード ​

依存 ​

JPYC.removeMinter_clears

名称・種別

型シグネチャ

解説

図解

Lean ソースコード

依存