JPYC.isMinter

名称・種別

• 名称: JPYC.isMinter
• 種別: def
• モジュール: JpycFormalVerification.AccessControl
• ソース: JpycFormalVerification/AccessControl.lean:240-241
• 概要: isMinter(account)：minter かどうかを返す読み取り専用ビュー。
• 仕様: 対象外

型シグネチャ

JPYC.State → JPYC.Address → Bool

State とアドレス account を受け取り、そのアカウントがミンター登録済みかを Bool で返します。

和訳 docstring

account がミンター登録済みかを返す（v2/FiatTokenV2.sol:148-150）。

解説

何を述べているか。 FiatTokenV2.isMinter です。真偽値マッピング minters[account] をそのまま返します。

直感。 状態を 読むだけ の関数（Solidity の view）で、書き込みは一切しません。返り値はミンターなら true、そうでなければ false です。

なぜ安全性に効くか。 これ自体は状態を変えないので安全性の主役ではありませんが、ガードや他の証明が参照する「観測値」を定義します。たとえばブロック判定・許可リスト判定・ミンター判定は、対応するフラグマッピングをこの形で読み出します。

図解

Lean ソースコード

/-- `isMinter(account)` — `v2/FiatTokenV2.sol:148-150`. -/
def isMinter (s : State) (account : Address) : Bool := s.minters account

対応 Solidity ソースコード

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:148-150

function isMinter(address account) external view returns (bool) {
    return minters[account];
}

依存

• JPYC.Address
• JPYC.State