JPYC.blocklist

名称・種別

名称: JPYC.blocklist
種別: def
モジュール: JpycFormalVerification.AccessControl
ソース: JpycFormalVerification/AccessControl.lean:132-136
概要: blocklist(account)：account をブロックリスト登録する関数（blocklister 限定）。
仕様: 対象外

型シグネチャ

lean

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

State・CallContext・対象 account を受け取り、ブロックリスト管理者だけが指定アカウントをブロックリストに載せる関数です。

和訳 docstring

account をブロックリストに追加する（v1/Blocklistable.sol:86-89）。

解説

何を述べているか。 Blocklistable.blocklist です。onlyBlocklister を通過した呼び出しだけが、blocklisted[account] を 1 に設定します。

直感。 制裁対象や不正アカウントを「凍結リスト」に登録します。登録後、そのアカウントは送金も受領もできなくなります。

なぜ安全性に効くか。 ブロックされたアカウントは notBlocklisted ガードに引っかかり、transfer / transferFrom / mint / burn のいずれにも参加できません（transfer_not_blocklisted 群が対偶を証明）。登録権限を blocklister に限定し（blocklist_auth）、フラグが確かに 1 になること（blocklist_sets）を保証します。

図解

Lean ソースコード

lean

/-- `blocklist(account)` — `v1/Blocklistable.sol:86-89`. -/
def blocklist (s : State) (ctx : CallContext) (account : Address) :
    Except Error State := do
  onlyBlocklister s ctx
  pure (s.setBlocklisted account 1)

対応 Solidity ソースコード

reference/JPYCv2/contracts/v1/Blocklistable.sol:86-89

solidity

function blocklist(address _account) external onlyBlocklister {
    blocklisted[_account] = 1;
    emit Blocklisted(_account);
}

JPYC.blocklist ​

名称・種別 ​

型シグネチャ ​

和訳 docstring ​

解説 ​

図解 ​

Lean ソースコード ​

対応 Solidity ソースコード ​

依存 ​