JPYC.configureMinter_sets
名称・種別
- 名称:
JPYC.configureMinter_sets - 種別: theorem
- モジュール:
JpycFormalVerification.AccessControlTheorems - ソース:
JpycFormalVerification/AccessControlTheorems.lean:350-356 - 概要: configureMinter は minter を許容額付きで有効化、removeMinter は無効化し許容額を 0 にする（効果）。
- 仕様: 対象
型シグネチャ
lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {minter : JPYC.Address} {amount : JPYC.U256}, Eq (JPYC.configureMinter s ctx minter amount) (Except.ok s') → And (Eq (s'.minters minter) Bool.true) (Eq (s'.minterAllowed minter) amount)configureMinter の成功は、そのミンターを有効化し（minters = true）、許可量を amount に設定する、という効果定理です。
和訳 docstring
効果。 configureMinter はミンターを有効化して許可量を設定し、removeMinter は無効化して許可量を 0 にする。
解説
何を述べているか。 configureMinter が成功すると s'.minters minter = true かつ s'.minterAllowed minter = amount です。configureMinter_ok と setMinter_minters_self / setMinterAllowed_self から従います。
直感。 「発行枠を付与したら、フラグと枠の両方がちゃんと設定される」を確認します。
なぜ安全性に効くか。 付与された枠 amount が正しく記録されることで、mint の上限検査（mint_minterAllowed）が意味を持ちます。発行量の制御が設定どおりに効く根拠です。
図解
Lean ソースコード
lean
/-- **Effect.** `configureMinter` enables the minter with the given allowance;
`removeMinter` disables it and zeroes the allowance. -/
theorem configureMinter_sets {s s' : State} {ctx : CallContext} {minter : Address} {amount : U256}
(h : configureMinter s ctx minter amount = .ok s') :
s'.minters minter = true ∧ s'.minterAllowed minter = amount := by
obtain ⟨_, _, rfl⟩ := configureMinter_ok h
exact ⟨setMinter_minters_self s minter true, setMinterAllowed_self _ minter amount⟩