JPYC.allowlist

名称・種別

名称: JPYC.allowlist
種別: def
モジュール: JpycFormalVerification.AccessControl
ソース: JpycFormalVerification/AccessControl.lean:212-217
概要: allowlist(account)：account を許可登録する関数（allowlister 限定）。
仕様: 対象外

型シグネチャ

lean

JPYC.State → JPYC.CallContext → JPYC.Address → Except JPYC.Error JPYC.State

State・CallContext・対象 account を受け取り、停止中でなければ許可リスト管理者が指定アカウントを許可リストに載せる関数です。

和訳 docstring

account を許可リストに追加する（v2/FiatTokenV2.sol:616-623）。

解説

何を述べているか。 FiatTokenV2.allowlist です。whenNotPaused と onlyAllowlister を通過した呼び出しが、allowlisted[account] を 1 に設定します。

直感。 「大口送金（上限額超）を許される特別なアカウント」を登録します。JPYC では 1 回あたり allowlistLimitAmount（10 万トークン）を超える送金・発行に、送り手の許可リスト登録が必要です。

なぜ安全性に効くか。 許可リストは checkAllowlist ガードと組み合わさり、上限超の送金を「登録済みアカウントだけ」に制限します（transfer_above_cap_allowlisted 群が対偶を証明）。登録権限を allowlister に限定し（allowlist_auth）、効果（allowlist_sets）を保証します。

図解

Lean ソースコード

lean

/-- `allowlist(account)` — `v2/FiatTokenV2.sol:616-623`. -/
def allowlist (s : State) (ctx : CallContext) (account : Address) :
    Except Error State := do
  whenNotPaused s
  onlyAllowlister s ctx
  pure (s.setAllowlisted account 1)

対応 Solidity ソースコード

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:616-623

solidity

function allowlist(address _account)
    external
    whenNotPaused
    onlyAllowlister
{
    allowlisted[_account] = 1;
    emit Allowlisted(_account);
}

JPYC.allowlist ​

名称・種別 ​

型シグネチャ ​

和訳 docstring ​

解説 ​

図解 ​

Lean ソースコード ​

対応 Solidity ソースコード ​

依存 ​